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

State before:
aig : AIG Nat
cnf1 cnf2 : CNF aig.CNFVar
cache1 : Cache aig cnf1
cache2 : Cache aig cnf2
idx : Nat
hbound : idx < cache1.marks.size
h : cache2.marks = cache1.marks.set ⟨idx, hbound⟩ true
⊢ idx < aig.decls.size
Tactic:
have := cache1.hmarks
State after:
aig : AIG Nat
cnf1 cnf2 : CNF aig.CNFVar
cache1 : Cache aig cnf1
cache2 : Cache aig cnf2
idx : Nat
hbound : idx < cache1.marks.size
h : cache2.marks = cache1.marks.set ⟨idx, hbound⟩ true
this : cache1.marks.size = aig.decls.size
⊢ idx < aig.decls.size

State before:
aig : AIG Nat
cnf1 cnf2 : CNF aig.CNFVar
cache1 : Cache aig cnf1
cache2 : Cache aig cnf2
idx : Nat
hbound : idx < cache1.marks.size
h : cache2.marks = cache1.marks.set ⟨idx, hbound⟩ true
this : cache1.marks.size = aig.decls.size
⊢ idx < aig.decls.size
Tactic:
omega
State after:
no goals

State before:
aig : AIG Nat
cnf1 cnf2 : CNF aig.CNFVar
cache1 : Cache aig cnf1
cache2 : Cache aig cnf2
idx : Nat
hbound : idx < cache1.marks.size
h : cache2.marks = cache1.marks.set ⟨idx, hbound⟩ true
⊢ cache1.IsExtensionBy cache2 idx ⋯
Tactic:
apply IsExtensionBy.mk
State after:
case extension
aig : AIG Nat
cnf1 cnf2 : CNF aig.CNFVar
cache1 : Cache aig cnf1
cache2 : Cache aig cnf2
idx : Nat
hbound : idx < cache1.marks.size
h : cache2.marks = cache1.marks.set ⟨idx, hbound⟩ true
⊢ ∀ (idx_1 : Nat) (hidx : idx_1 < aig.decls.size), cache1.marks[idx_1] = true → cache2.marks[idx_1] = true

case trueAt
aig : AIG Nat
cnf1 cnf2 : CNF aig.CNFVar
cache1 : Cache aig cnf1
cache2 : Cache aig cnf2
idx : Nat
hbound : idx < cache1.marks.size
h : cache2.marks = cache1.marks.set ⟨idx, hbound⟩ true
⊢ cache2.marks[idx] = true

State before:
case extension
aig : AIG Nat
cnf1 cnf2 : CNF aig.CNFVar
cache1 : Cache aig cnf1
cache2 : Cache aig cnf2
idx : Nat
hbound : idx < cache1.marks.size
h : cache2.marks = cache1.marks.set ⟨idx, hbound⟩ true
⊢ ∀ (idx_1 : Nat) (hidx : idx_1 < aig.decls.size), cache1.marks[idx_1] = true → cache2.marks[idx_1] = true

case trueAt
aig : AIG Nat
cnf1 cnf2 : CNF aig.CNFVar
cache1 : Cache aig cnf1
cache2 : Cache aig cnf2
idx : Nat
hbound : idx < cache1.marks.size
h : cache2.marks = cache1.marks.set ⟨idx, hbound⟩ true
⊢ cache2.marks[idx] = true
Tactic:
. intro idx hidx hmark
  simp [Array.getElem_set, hmark, h]
State after:
case trueAt
aig : AIG Nat
cnf1 cnf2 : CNF aig.CNFVar
cache1 : Cache aig cnf1
cache2 : Cache aig cnf2
idx : Nat
hbound : idx < cache1.marks.size
h : cache2.marks = cache1.marks.set ⟨idx, hbound⟩ true
⊢ cache2.marks[idx] = true

State before:
case trueAt
aig : AIG Nat
cnf1 cnf2 : CNF aig.CNFVar
cache1 : Cache aig cnf1
cache2 : Cache aig cnf2
idx : Nat
hbound : idx < cache1.marks.size
h : cache2.marks = cache1.marks.set ⟨idx, hbound⟩ true
⊢ cache2.marks[idx] = true
Tactic:
. simp[h]
State after:
no goals

State before:
case extension
aig : AIG Nat
cnf1 cnf2 : CNF aig.CNFVar
cache1 : Cache aig cnf1
cache2 : Cache aig cnf2
idx : Nat
hbound : idx < cache1.marks.size
h : cache2.marks = cache1.marks.set ⟨idx, hbound⟩ true
⊢ ∀ (idx_1 : Nat) (hidx : idx_1 < aig.decls.size), cache1.marks[idx_1] = true → cache2.marks[idx_1] = true
Tactic:
intro idx hidx hmark
State after:
case extension
aig : AIG Nat
cnf1 cnf2 : CNF aig.CNFVar
cache1 : Cache aig cnf1
cache2 : Cache aig cnf2
idx✝ : Nat
hbound : idx✝ < cache1.marks.size
h : cache2.marks = cache1.marks.set ⟨idx✝, hbound⟩ true
idx : Nat
hidx : idx < aig.decls.size
hmark : cache1.marks[idx] = true
⊢ cache2.marks[idx] = true

State before:
case extension
aig : AIG Nat
cnf1 cnf2 : CNF aig.CNFVar
cache1 : Cache aig cnf1
cache2 : Cache aig cnf2
idx✝ : Nat
hbound : idx✝ < cache1.marks.size
h : cache2.marks = cache1.marks.set ⟨idx✝, hbound⟩ true
idx : Nat
hidx : idx < aig.decls.size
hmark : cache1.marks[idx] = true
⊢ cache2.marks[idx] = true
Tactic:
simp [Array.getElem_set, hmark, h]
State after:
no goals

State before:
case trueAt
aig : AIG Nat
cnf1 cnf2 : CNF aig.CNFVar
cache1 : Cache aig cnf1
cache2 : Cache aig cnf2
idx : Nat
hbound : idx < cache1.marks.size
h : cache2.marks = cache1.marks.set ⟨idx, hbound⟩ true
⊢ cache2.marks[idx] = true
Tactic:
simp[h]
State after:
no goals