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

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

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