boolean_circuit_eval_demorgan_and

theoremverified

For any Boolean circuits c₁ and c₂ on n variables and any input assignment x : Fin n → Bool, evaluating the negation of their conjunction BooleanCircuit.not (BooleanCircuit.and c₁ c₂) on x equals evaluating the disjunction of their negations BooleanCircuit.or (BooleanCircuit.not c₁) (BooleanCircuit.not c₂) on x.

Statement

theorem boolean_circuit_eval_demorgan_and {n : Nat} (c₁ c₂ : BooleanCircuit n) (x : Fin n → Bool) : boolean_circuit_eval (BooleanCircuit.not (BooleanCircuit.and c₁ c₂)) x = boolean_circuit_eval (BooleanCircuit.or (BooleanCircuit.not c₁) (BooleanCircuit.not c₂)) x

Source

Arora & Barak, Section 6.1

Verified

10 Sep 2026

Axioms

propext

Built on 2

BooleanCircuitA Boolean circuit with n inputs over the standard De Morgan basis, with constructors for input variables indexed by Fin n, Boolean…
boolean_circuit_evalEvaluates a Boolean circuit c with n inputs on a variable truth assignment x : Fin n → Bool, by structural recursion: variables look up…

Read back from the Lean

For every natural number n, any two Boolean circuits c₁ and c₂ with n inputs, and every input assignment x : Fin n → Bool, the evaluation of the circuit (BooleanCircuit.not (BooleanCircuit.and c₁ c₂)) on x equals the evaluation of the circuit (BooleanCircuit.or (BooleanCircuit.not c₁) (BooleanCircuit.not c₂)) on x.

Written by a model that saw only the Lean, never the English above. If the two disagree, that is worth a challenge.

Lean source view module on GitHub

/-- De Morgan's law for circuit evaluation: the negation of an AND circuit equals the OR of the negated circuits. -/
theorem boolean_circuit_eval_demorgan_and {n : Nat} (c₁ c₂ : BooleanCircuit n) (x : Fin n → Bool) : boolean_circuit_eval (BooleanCircuit.not (BooleanCircuit.and c₁ c₂)) x = boolean_circuit_eval (BooleanCircuit.or (BooleanCircuit.not c₁) (BooleanCircuit.not c₂)) x := by
  simp [boolean_circuit_eval]

Discuss this result Challenge it