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

State before:
upper lhs rhs : Nat
linv rinv : Bool
aig : AIG Nat
h : upper < aig.decls.size
heq : aig.decls[upper] = Decl.gate lhs rhs linv rinv
⊢ lhs < aig.decls.size
Tactic:
have := aig.inv upper lhs rhs linv rinv h heq
State after:
upper lhs rhs : Nat
linv rinv : Bool
aig : AIG Nat
h : upper < aig.decls.size
heq : aig.decls[upper] = Decl.gate lhs rhs linv rinv
this : lhs < upper ∧ rhs < upper
⊢ lhs < aig.decls.size

State before:
upper lhs rhs : Nat
linv rinv : Bool
aig : AIG Nat
h : upper < aig.decls.size
heq : aig.decls[upper] = Decl.gate lhs rhs linv rinv
this : lhs < upper ∧ rhs < upper
⊢ lhs < aig.decls.size
Tactic:
omega
State after:
no goals

State before:
upper lhs rhs : Nat
linv rinv : Bool
aig : AIG Nat
h : upper < aig.decls.size
heq : aig.decls[upper] = Decl.gate lhs rhs linv rinv
⊢ rhs < aig.decls.size
Tactic:
have := aig.inv upper lhs rhs linv rinv h heq
State after:
upper lhs rhs : Nat
linv rinv : Bool
aig : AIG Nat
h : upper < aig.decls.size
heq : aig.decls[upper] = Decl.gate lhs rhs linv rinv
this : lhs < upper ∧ rhs < upper
⊢ rhs < aig.decls.size

State before:
upper lhs rhs : Nat
linv rinv : Bool
aig : AIG Nat
h : upper < aig.decls.size
heq : aig.decls[upper] = Decl.gate lhs rhs linv rinv
this : lhs < upper ∧ rhs < upper
⊢ rhs < aig.decls.size
Tactic:
omega
State after:
no goals

State before:
upper lhs rhs : Nat
linv rinv : Bool
aig : AIG Nat
h : upper < aig.decls.size
heq : aig.decls[upper] = Decl.gate lhs rhs linv rinv
⊢ Inv (Decl.gateToCNF (Sum.inr ⟨upper, h⟩) (Sum.inr ⟨lhs, ⋯⟩) (Sum.inr ⟨rhs, ⋯⟩) linv rinv)
Tactic:
intro assign1
State after:
upper lhs rhs : Nat
linv rinv : Bool
aig : AIG Nat
h : upper < aig.decls.size
heq : aig.decls[upper] = Decl.gate lhs rhs linv rinv
assign1 : Nat → Bool
⊢ (Decl.gateToCNF (Sum.inr ⟨upper, h⟩) (Sum.inr ⟨lhs, ⋯⟩) (Sum.inr ⟨rhs, ⋯⟩) linv rinv).sat
    (cnfSatAssignment aig assign1)

State before:
upper lhs rhs : Nat
linv rinv : Bool
aig : AIG Nat
h : upper < aig.decls.size
heq : aig.decls[upper] = Decl.gate lhs rhs linv rinv
assign1 : Nat → Bool
⊢ (Decl.gateToCNF (Sum.inr ⟨upper, h⟩) (Sum.inr ⟨lhs, ⋯⟩) (Sum.inr ⟨rhs, ⋯⟩) linv rinv).sat
    (cnfSatAssignment aig assign1)
Tactic:
simp [CNF.sat, denote_idx_gate heq]
State after:
no goals