Boolean-nor
Formalization and verification of a circuit
for boolean negated (inclusive) disjunction.
Given two field elements x and y representing booleans
(i.e. such that each field element is either 0 or 1;
see boolean-assert),
their negated (inclusive) disjunction z is obtained via
a multiplication of the form
which defines z to be 1 if both x and y are 0, otherwise 0.
Thus, z is boolean (0 or 1) if both x and y are.
This has the same form as boolean-and,
but with the operand booleans negated (see boolean-not).
Subtopics
- Boolean-nor-spec
- Specification of the circuit.
- Boolean-nor-circuit
- Construction of the circuit.
- Boolean-nor-correctness
- Correctness of the circuit.
- Boolean-nor-lifting
- Lifting of the circuit to a predicate.
