Theorem: AIG.toCNF.Cache.Inv_init (LeanSAT/AIG/CNF.lean)

State before:
aig : AIG Nat
⊢ (mkArray aig.decls.size false).size = aig.decls.size
Tactic:
simp
State after:
no goals

State before:
aig : AIG Nat
⊢ ∀ (lhs rhs : Nat) (linv rinv : Bool) (idx : Nat) (hbound : idx < aig.decls.size),
    (mkArray aig.decls.size false)[idx] = true →
      ∀ (heq : aig.decls[idx] = Decl.gate lhs rhs linv rinv),
        (mkArray aig.decls.size false)[lhs] = true ∧ (mkArray aig.decls.size false)[rhs] = true
Tactic:
intro lhs rhs linv rinv idx hbound hmarked heq
State after:
aig : AIG Nat
lhs rhs : Nat
linv rinv : Bool
idx : Nat
hbound : idx < aig.decls.size
hmarked : (mkArray aig.decls.size false)[idx] = true
heq : aig.decls[idx] = Decl.gate lhs rhs linv rinv
⊢ (mkArray aig.decls.size false)[lhs] = true ∧ (mkArray aig.decls.size false)[rhs] = true

State before:
aig : AIG Nat
lhs rhs : Nat
linv rinv : Bool
idx : Nat
hbound : idx < aig.decls.size
hmarked : (mkArray aig.decls.size false)[idx] = true
heq : aig.decls[idx] = Decl.gate lhs rhs linv rinv
⊢ (mkArray aig.decls.size false)[lhs] = true ∧ (mkArray aig.decls.size false)[rhs] = true
Tactic:
simp at hmarked
State after:
no goals

State before:
aig : AIG Nat
⊢ ∀ (assign : aig.CNFVar → Bool),
    CNF.eval assign [] = true →
      ∀ (idx : Nat) (hbound : idx < aig.decls.size),
        (mkArray aig.decls.size false)[idx] = true →
          ⟦{ aig := aig, ref := { gate := idx, hgate := hbound } }, projectLeftAssign assign⟧ =
            projectRightAssign assign idx hbound
Tactic:
intro assign _ idx hbound hmark
State after:
aig : AIG Nat
assign : aig.CNFVar → Bool
_heval✝ : CNF.eval assign [] = true
idx : Nat
hbound : idx < aig.decls.size
hmark : (mkArray aig.decls.size false)[idx] = true
⊢ ⟦{ aig := aig, ref := { gate := idx, hgate := hbound } }, projectLeftAssign assign⟧ =
    projectRightAssign assign idx hbound

State before:
aig : AIG Nat
assign : aig.CNFVar → Bool
_heval✝ : CNF.eval assign [] = true
idx : Nat
hbound : idx < aig.decls.size
hmark : (mkArray aig.decls.size false)[idx] = true
⊢ ⟦{ aig := aig, ref := { gate := idx, hgate := hbound } }, projectLeftAssign assign⟧ =
    projectRightAssign assign idx hbound
Tactic:
simp at hmark
State after:
no goals