Theorem: AIG.toCNF.State.Inv_constToCNF (LeanSAT/AIG/CNF.lean)

State before:
upper : Nat
aig : AIG Nat
h : upper < aig.decls.size
b : Bool
heq : aig.decls[upper] = Decl.const b
⊢ Inv (Decl.constToCNF (Sum.inr ⟨upper, h⟩) b)
Tactic:
intro assign1
State after:
upper : Nat
aig : AIG Nat
h : upper < aig.decls.size
b : Bool
heq : aig.decls[upper] = Decl.const b
assign1 : Nat → Bool
⊢ (Decl.constToCNF (Sum.inr ⟨upper, h⟩) b).sat (cnfSatAssignment aig assign1)

State before:
upper : Nat
aig : AIG Nat
h : upper < aig.decls.size
b : Bool
heq : aig.decls[upper] = Decl.const b
assign1 : Nat → Bool
⊢ (Decl.constToCNF (Sum.inr ⟨upper, h⟩) b).sat (cnfSatAssignment aig assign1)
Tactic:
simp [CNF.sat, denote_idx_const heq]
State after:
no goals