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

State before:
aig✝ : AIG Nat
cnf1 cnf2 : CNF aig✝.CNFVar
h1 : Inv cnf1
h2 : Inv cnf2
⊢ Inv (cnf1 ++ cnf2)
Tactic:
intro assign1
State after:
aig✝ : AIG Nat
cnf1 cnf2 : CNF aig✝.CNFVar
h1 : Inv cnf1
h2 : Inv cnf2
assign1 : Nat → Bool
⊢ (cnf1 ++ cnf2).sat (cnfSatAssignment aig✝ assign1)

State before:
aig✝ : AIG Nat
cnf1 cnf2 : CNF aig✝.CNFVar
h1 : Inv cnf1
h2 : Inv cnf2
assign1 : Nat → Bool
⊢ (cnf1 ++ cnf2).sat (cnfSatAssignment aig✝ assign1)
Tactic:
specialize h1 assign1
State after:
aig✝ : AIG Nat
cnf1 cnf2 : CNF aig✝.CNFVar
h2 : Inv cnf2
assign1 : Nat → Bool
h1 : cnf1.sat (cnfSatAssignment aig✝ assign1)
⊢ (cnf1 ++ cnf2).sat (cnfSatAssignment aig✝ assign1)

State before:
aig✝ : AIG Nat
cnf1 cnf2 : CNF aig✝.CNFVar
h2 : Inv cnf2
assign1 : Nat → Bool
h1 : cnf1.sat (cnfSatAssignment aig✝ assign1)
⊢ (cnf1 ++ cnf2).sat (cnfSatAssignment aig✝ assign1)
Tactic:
specialize h2 assign1
State after:
aig✝ : AIG Nat
cnf1 cnf2 : CNF aig✝.CNFVar
assign1 : Nat → Bool
h1 : cnf1.sat (cnfSatAssignment aig✝ assign1)
h2 : cnf2.sat (cnfSatAssignment aig✝ assign1)
⊢ (cnf1 ++ cnf2).sat (cnfSatAssignment aig✝ assign1)

State before:
aig✝ : AIG Nat
cnf1 cnf2 : CNF aig✝.CNFVar
assign1 : Nat → Bool
h1 : cnf1.sat (cnfSatAssignment aig✝ assign1)
h2 : cnf2.sat (cnfSatAssignment aig✝ assign1)
⊢ (cnf1 ++ cnf2).sat (cnfSatAssignment aig✝ assign1)
Tactic:
simp [CNF.sat] at h1 h2 ⊢
State after:
aig✝ : AIG Nat
cnf1 cnf2 : CNF aig✝.CNFVar
assign1 : Nat → Bool
h1 : CNF.eval (cnfSatAssignment aig✝ assign1) cnf1 = true
h2 : CNF.eval (cnfSatAssignment aig✝ assign1) cnf2 = true
⊢ CNF.eval (cnfSatAssignment aig✝ assign1) cnf1 = true ∧ CNF.eval (cnfSatAssignment aig✝ assign1) cnf2 = true

State before:
aig✝ : AIG Nat
cnf1 cnf2 : CNF aig✝.CNFVar
assign1 : Nat → Bool
h1 : CNF.eval (cnfSatAssignment aig✝ assign1) cnf1 = true
h2 : CNF.eval (cnfSatAssignment aig✝ assign1) cnf2 = true
⊢ CNF.eval (cnfSatAssignment aig✝ assign1) cnf1 = true ∧ CNF.eval (cnfSatAssignment aig✝ assign1) cnf2 = true
Tactic:
constructor <;> assumption
State after:
no goals