NAND in the De Morgan basis

One AND gate followed by one NOT gate implements NAND. The construction uses the existing single-gate and sequential circuit constructors, so its size counts both gates.

Main definitions

• Cslib.Circuits.Boolean.nandCircuit: the two-gate NAND circuit.

Main results

• Cslib.Circuits.Boolean.eval_nandCircuit: Boolean NAND semantics.
• Cslib.Circuits.Boolean.size_nandCircuit: exactly two gates.

References

• S. Arora, B. Barak, Computational Complexity: A Modern Approach, Section 6.1

def Cslib.Circuits.Boolean.nandCircuit : Circuit signature 2 1

NAND, implemented by one AND gate followed by one NOT gate.

@[simp]

theorem Cslib.Circuits.Boolean.eval_nandCircuit (x : Fin 2 → Bool) (j : Fin 1) : nandCircuit.eval interpretation x j = !(x 0 && x 1)

@[simp]

theorem Cslib.Circuits.Boolean.size_nandCircuit : nandCircuit.size = 2