		Search-engine friendly clone of the ACL2 documentation.

Field-eq

Formalization and verification of a circuit for field non-equality.

Given two field elements x and y, their equality can be checked, and put into a boolean result z, by negating the non-equality of x and y:

\begin{array}{l}
     \mathit{field_neq}(x,y,w) \\
     \mathit{boolean_not}(w,z)
     \end{array}