Theorem: Decl.gateToCNF_eval (LeanSAT/AIG/CNF.lean)

State before:
α✝ : Type
output lhs rhs : α✝
linv rinv : Bool
assign : α✝ → Bool
⊢ CNF.eval assign (gateToCNF output lhs rhs linv rinv) =
    (assign output == (xor (assign lhs) linv && xor (assign rhs) rinv))
Tactic:
simp [gateToCNF, CNF.eval, CNF.Clause.eval]
State after:
α✝ : Type
output lhs rhs : α✝
linv rinv : Bool
assign : α✝ → Bool
⊢ ((!assign output || assign lhs == !linv) &&
      ((!assign output || assign rhs == !rinv) && (assign output || (assign lhs == linv || assign rhs == rinv)))) =
    (assign output == (xor (assign lhs) linv && xor (assign rhs) rinv))

State before:
α✝ : Type
output lhs rhs : α✝
linv rinv : Bool
assign : α✝ → Bool
⊢ ((!assign output || assign lhs == !linv) &&
      ((!assign output || assign rhs == !rinv) && (assign output || (assign lhs == linv || assign rhs == rinv)))) =
    (assign output == (xor (assign lhs) linv && xor (assign rhs) rinv))
Tactic:
cases assign output
  <;> cases assign lhs
    <;> cases assign rhs
      <;> cases linv
        <;> cases rinv
          <;> decide
State after:
no goals