internlm/Lean-Github huggingface dataset:
Theorem: AIG.toCNF.Cache.IsExtensionBy_trans_right
Proof state before:
case extension
aig : AIG Nat
cnf1 cnf2 cnf3 : CNF aig.CNFVar
new1 : Nat
hnew1 : new1 < aig.decls.size
new2 : Nat
hnew2 : new2 < aig.decls.size
cache1 : Cache aig cnf1
cache2 : Cache aig cnf2
cache3 : Cache aig cnf3
h12 : cache1.IsExtensionBy cache2 new1 hnew1
h23 : cache2.IsExtensionBy cache3 new2 hnew2
⊢ ∀ (idx : Nat) (hidx : idx < aig.decls.size), cache1.marks[idx] = true → cache3.marks[idx] = true
Tactic:
intro idx hidx hmarked
Proof state after:
case extension
aig : AIG Nat
cnf1 cnf2 cnf3 : CNF aig.CNFVar
new1 : Nat
hnew1 : new1 < aig.decls.size
new2 : Nat
hnew2 : new2 < aig.decls.size
cache1 : Cache aig cnf1
cache2 : Cache aig cnf2
cache3 : Cache aig cnf3
h12 : cache1.IsExtensionBy cache2 new1 hnew1
h23 : cache2.IsExtensionBy cache3 new2 hnew2
idx : Nat
hidx : idx < aig.decls.size
hmarked : cache1.marks[idx] = true
⊢ cache3.marks[idx] = true
Theorem: AIG.toCNF.Cache.IsExtensionBy_trans_right
Proof state before:
case extension
aig : AIG Nat
cnf1 cnf2 cnf3 : CNF aig.CNFVar
new1 : Nat
hnew1 : new1 < aig.decls.size
new2 : Nat
hnew2 : new2 < aig.decls.size
cache1 : Cache aig cnf1
cache2 : Cache aig cnf2
cache3 : Cache aig cnf3
h12 : cache1.IsExtensionBy cache2 new1 hnew1
h23 : cache2.IsExtensionBy cache3 new2 hnew2
idx : Nat
hidx : idx < aig.decls.size
hmarked : cache1.marks[idx] = true
⊢ cache3.marks[idx] = true
Tactic:
apply h23.extension
Proof state after:
case extension.a
aig : AIG Nat
cnf1 cnf2 cnf3 : CNF aig.CNFVar
new1 : Nat
hnew1 : new1 < aig.decls.size
new2 : Nat
hnew2 : new2 < aig.decls.size
cache1 : Cache aig cnf1
cache2 : Cache aig cnf2
cache3 : Cache aig cnf3
h12 : cache1.IsExtensionBy cache2 new1 hnew1
h23 : cache2.IsExtensionBy cache3 new2 hnew2
idx : Nat
hidx : idx < aig.decls.size
hmarked : cache1.marks[idx] = true
⊢ cache2.marks[idx] = true

case extension.hidx
aig : AIG Nat
cnf1 cnf2 cnf3 : CNF aig.CNFVar
new1 : Nat
hnew1 : new1 < aig.decls.size
new2 : Nat
hnew2 : new2 < aig.decls.size
cache1 : Cache aig cnf1
cache2 : Cache aig cnf2
cache3 : Cache aig cnf3
h12 : cache1.IsExtensionBy cache2 new1 hnew1
h23 : cache2.IsExtensionBy cache3 new2 hnew2
idx : Nat
hidx : idx < aig.decls.size
hmarked : cache1.marks[idx] = true
⊢ idx < aig.decls.size
Theorem: AIG.toCNF.Cache.IsExtensionBy_trans_right
Proof state before:
case extension.a
aig : AIG Nat
cnf1 cnf2 cnf3 : CNF aig.CNFVar
new1 : Nat
hnew1 : new1 < aig.decls.size
new2 : Nat
hnew2 : new2 < aig.decls.size
cache1 : Cache aig cnf1
cache2 : Cache aig cnf2
cache3 : Cache aig cnf3
h12 : cache1.IsExtensionBy cache2 new1 hnew1
h23 : cache2.IsExtensionBy cache3 new2 hnew2
idx : Nat
hidx : idx < aig.decls.size
hmarked : cache1.marks[idx] = true
⊢ cache2.marks[idx] = true

case extension.hidx
aig : AIG Nat
cnf1 cnf2 cnf3 : CNF aig.CNFVar
new1 : Nat
hnew1 : new1 < aig.decls.size
new2 : Nat
hnew2 : new2 < aig.decls.size
cache1 : Cache aig cnf1
cache2 : Cache aig cnf2
cache3 : Cache aig cnf3
h12 : cache1.IsExtensionBy cache2 new1 hnew1
h23 : cache2.IsExtensionBy cache3 new2 hnew2
idx : Nat
hidx : idx < aig.decls.size
hmarked : cache1.marks[idx] = true
⊢ idx < aig.decls.size
Tactic:
. apply h12.extension
  . exact hmarked
  . omega
Proof state after:
case extension.hidx
aig : AIG Nat
cnf1 cnf2 cnf3 : CNF aig.CNFVar
new1 : Nat
hnew1 : new1 < aig.decls.size
new2 : Nat
hnew2 : new2 < aig.decls.size
cache1 : Cache aig cnf1
cache2 : Cache aig cnf2
cache3 : Cache aig cnf3
h12 : cache1.IsExtensionBy cache2 new1 hnew1
h23 : cache2.IsExtensionBy cache3 new2 hnew2
idx : Nat
hidx : idx < aig.decls.size
hmarked : cache1.marks[idx] = true
⊢ idx < aig.decls.size
Theorem: AIG.toCNF.Cache.IsExtensionBy_trans_right
Proof state before:
case extension.hidx
aig : AIG Nat
cnf1 cnf2 cnf3 : CNF aig.CNFVar
new1 : Nat
hnew1 : new1 < aig.decls.size
new2 : Nat
hnew2 : new2 < aig.decls.size
cache1 : Cache aig cnf1
cache2 : Cache aig cnf2
cache3 : Cache aig cnf3
h12 : cache1.IsExtensionBy cache2 new1 hnew1
h23 : cache2.IsExtensionBy cache3 new2 hnew2
idx : Nat
hidx : idx < aig.decls.size
hmarked : cache1.marks[idx] = true
⊢ idx < aig.decls.size
Tactic:
. omega
Proof state after:
no goals
Theorem: AIG.toCNF.Cache.IsExtensionBy_trans_right
Proof state before:
case extension.a
aig : AIG Nat
cnf1 cnf2 cnf3 : CNF aig.CNFVar
new1 : Nat
hnew1 : new1 < aig.decls.size
new2 : Nat
hnew2 : new2 < aig.decls.size
cache1 : Cache aig cnf1
cache2 : Cache aig cnf2
cache3 : Cache aig cnf3
h12 : cache1.IsExtensionBy cache2 new1 hnew1
h23 : cache2.IsExtensionBy cache3 new2 hnew2
idx : Nat
hidx : idx < aig.decls.size
hmarked : cache1.marks[idx] = true
⊢ cache2.marks[idx] = true
Tactic:
apply h12.extension
Proof state after:
case extension.a.a
aig : AIG Nat
cnf1 cnf2 cnf3 : CNF aig.CNFVar
new1 : Nat
hnew1 : new1 < aig.decls.size
new2 : Nat
hnew2 : new2 < aig.decls.size
cache1 : Cache aig cnf1
cache2 : Cache aig cnf2
cache3 : Cache aig cnf3
h12 : cache1.IsExtensionBy cache2 new1 hnew1
h23 : cache2.IsExtensionBy cache3 new2 hnew2
idx : Nat
hidx : idx < aig.decls.size
hmarked : cache1.marks[idx] = true
⊢ cache1.marks[idx] = true

case extension.a.hidx
aig : AIG Nat
cnf1 cnf2 cnf3 : CNF aig.CNFVar
new1 : Nat
hnew1 : new1 < aig.decls.size
new2 : Nat
hnew2 : new2 < aig.decls.size
cache1 : Cache aig cnf1
cache2 : Cache aig cnf2
cache3 : Cache aig cnf3
h12 : cache1.IsExtensionBy cache2 new1 hnew1
h23 : cache2.IsExtensionBy cache3 new2 hnew2
idx : Nat
hidx : idx < aig.decls.size
hmarked : cache1.marks[idx] = true
⊢ idx < aig.decls.size
Theorem: AIG.toCNF.Cache.IsExtensionBy_trans_right
Proof state before:
case extension.a.a
aig : AIG Nat
cnf1 cnf2 cnf3 : CNF aig.CNFVar
new1 : Nat
hnew1 : new1 < aig.decls.size
new2 : Nat
hnew2 : new2 < aig.decls.size
cache1 : Cache aig cnf1
cache2 : Cache aig cnf2
cache3 : Cache aig cnf3
h12 : cache1.IsExtensionBy cache2 new1 hnew1
h23 : cache2.IsExtensionBy cache3 new2 hnew2
idx : Nat
hidx : idx < aig.decls.size
hmarked : cache1.marks[idx] = true
⊢ cache1.marks[idx] = true

case extension.a.hidx
aig : AIG Nat
cnf1 cnf2 cnf3 : CNF aig.CNFVar
new1 : Nat
hnew1 : new1 < aig.decls.size
new2 : Nat
hnew2 : new2 < aig.decls.size
cache1 : Cache aig cnf1
cache2 : Cache aig cnf2
cache3 : Cache aig cnf3
h12 : cache1.IsExtensionBy cache2 new1 hnew1
h23 : cache2.IsExtensionBy cache3 new2 hnew2
idx : Nat
hidx : idx < aig.decls.size
hmarked : cache1.marks[idx] = true
⊢ idx < aig.decls.size
Tactic:
. exact hmarked
Proof state after:
case extension.a.hidx
aig : AIG Nat
cnf1 cnf2 cnf3 : CNF aig.CNFVar
new1 : Nat
hnew1 : new1 < aig.decls.size
new2 : Nat
hnew2 : new2 < aig.decls.size
cache1 : Cache aig cnf1
cache2 : Cache aig cnf2
cache3 : Cache aig cnf3
h12 : cache1.IsExtensionBy cache2 new1 hnew1
h23 : cache2.IsExtensionBy cache3 new2 hnew2
idx : Nat
hidx : idx < aig.decls.size
hmarked : cache1.marks[idx] = true
⊢ idx < aig.decls.size
Theorem: AIG.toCNF.Cache.IsExtensionBy_trans_right
Proof state before:
case extension.a.hidx
aig : AIG Nat
cnf1 cnf2 cnf3 : CNF aig.CNFVar
new1 : Nat
hnew1 : new1 < aig.decls.size
new2 : Nat
hnew2 : new2 < aig.decls.size
cache1 : Cache aig cnf1
cache2 : Cache aig cnf2
cache3 : Cache aig cnf3
h12 : cache1.IsExtensionBy cache2 new1 hnew1
h23 : cache2.IsExtensionBy cache3 new2 hnew2
idx : Nat
hidx : idx < aig.decls.size
hmarked : cache1.marks[idx] = true
⊢ idx < aig.decls.size
Tactic:
. omega
Proof state after:
no goals
Theorem: AIG.toCNF.Cache.IsExtensionBy_trans_right
Proof state before:
case extension.a.a
aig : AIG Nat
cnf1 cnf2 cnf3 : CNF aig.CNFVar
new1 : Nat
hnew1 : new1 < aig.decls.size
new2 : Nat
hnew2 : new2 < aig.decls.size
cache1 : Cache aig cnf1
cache2 : Cache aig cnf2
cache3 : Cache aig cnf3
h12 : cache1.IsExtensionBy cache2 new1 hnew1
h23 : cache2.IsExtensionBy cache3 new2 hnew2
idx : Nat
hidx : idx < aig.decls.size
hmarked : cache1.marks[idx] = true
⊢ cache1.marks[idx] = true
Tactic:
exact hmarked
Proof state after:
no goals
Theorem: AIG.toCNF.Cache.IsExtensionBy_trans_right
Proof state before:
case extension.a.hidx
aig : AIG Nat
cnf1 cnf2 cnf3 : CNF aig.CNFVar
new1 : Nat
hnew1 : new1 < aig.decls.size
new2 : Nat
hnew2 : new2 < aig.decls.size
cache1 : Cache aig cnf1
cache2 : Cache aig cnf2
cache3 : Cache aig cnf3
h12 : cache1.IsExtensionBy cache2 new1 hnew1
h23 : cache2.IsExtensionBy cache3 new2 hnew2
idx : Nat
hidx : idx < aig.decls.size
hmarked : cache1.marks[idx] = true
⊢ idx < aig.decls.size
Tactic:
omega
Proof state after:
no goals
Theorem: AIG.toCNF.Cache.IsExtensionBy_trans_right
Proof state before:
case extension.hidx
aig : AIG Nat
cnf1 cnf2 cnf3 : CNF aig.CNFVar
new1 : Nat
hnew1 : new1 < aig.decls.size
new2 : Nat
hnew2 : new2 < aig.decls.size
cache1 : Cache aig cnf1
cache2 : Cache aig cnf2
cache3 : Cache aig cnf3
h12 : cache1.IsExtensionBy cache2 new1 hnew1
h23 : cache2.IsExtensionBy cache3 new2 hnew2
idx : Nat
hidx : idx < aig.decls.size
hmarked : cache1.marks[idx] = true
⊢ idx < aig.decls.size
Tactic:
omega
Proof state after:
no goals
Theorem: AIG.toCNF.Cache.IsExtensionBy_trans_right
Proof state before:
case trueAt
aig : AIG Nat
cnf1 cnf2 cnf3 : CNF aig.CNFVar
new1 : Nat
hnew1 : new1 < aig.decls.size
new2 : Nat
hnew2 : new2 < aig.decls.size
cache1 : Cache aig cnf1
cache2 : Cache aig cnf2
cache3 : Cache aig cnf3
h12 : cache1.IsExtensionBy cache2 new1 hnew1
h23 : cache2.IsExtensionBy cache3 new2 hnew2
⊢ cache3.marks[new2] = true
Tactic:
exact h23.trueAt
Proof state after:
no goals
Theorem: AIG.toCNF.Cache.IsExtensionBy_rfl
Proof state before:
aig : AIG Nat
cnf : CNF aig.CNFVar
idx : Nat
omega : idx < aig.decls.size
cache : Cache aig cnf
h : idx < cache.marks.size
hmarked : cache.marks[idx] = true
⊢ cache.IsExtensionBy cache idx ⋯
Tactic:
apply IsExtensionBy.mk
Proof state after:
case extension
aig : AIG Nat
cnf : CNF aig.CNFVar
idx : Nat
omega : idx < aig.decls.size
cache : Cache aig cnf
h : idx < cache.marks.size
hmarked : cache.marks[idx] = true
⊢ ∀ (idx_1 : Nat) (hidx : idx_1 < aig.decls.size), cache.marks[idx_1] = true → cache.marks[idx_1] = true

case trueAt
aig : AIG Nat
cnf : CNF aig.CNFVar
idx : Nat
omega : idx < aig.decls.size
cache : Cache aig cnf
h : idx < cache.marks.size
hmarked : cache.marks[idx] = true
⊢ cache.marks[idx] = true
Theorem: AIG.toCNF.Cache.IsExtensionBy_rfl
Proof state before:
case extension
aig : AIG Nat
cnf : CNF aig.CNFVar
idx : Nat
omega : idx < aig.decls.size
cache : Cache aig cnf
h : idx < cache.marks.size
hmarked : cache.marks[idx] = true
⊢ ∀ (idx_1 : Nat) (hidx : idx_1 < aig.decls.size), cache.marks[idx_1] = true → cache.marks[idx_1] = true

case trueAt
aig : AIG Nat
cnf : CNF aig.CNFVar
idx : Nat
omega : idx < aig.decls.size
cache : Cache aig cnf
h : idx < cache.marks.size
hmarked : cache.marks[idx] = true
⊢ cache.marks[idx] = true
Tactic:
. intros
  assumption
Proof state after:
case trueAt
aig : AIG Nat
cnf : CNF aig.CNFVar
idx : Nat
omega : idx < aig.decls.size
cache : Cache aig cnf
h : idx < cache.marks.size
hmarked : cache.marks[idx] = true
⊢ cache.marks[idx] = true
Theorem: AIG.toCNF.Cache.IsExtensionBy_rfl
Proof state before:
case trueAt
aig : AIG Nat
cnf : CNF aig.CNFVar
idx : Nat
omega : idx < aig.decls.size
cache : Cache aig cnf
h : idx < cache.marks.size
hmarked : cache.marks[idx] = true
⊢ cache.marks[idx] = true
Tactic:
. exact hmarked
Proof state after:
no goals
Theorem: AIG.toCNF.Cache.IsExtensionBy_rfl
Proof state before:
case extension
aig : AIG Nat
cnf : CNF aig.CNFVar
idx : Nat
omega : idx < aig.decls.size
cache : Cache aig cnf
h : idx < cache.marks.size
hmarked : cache.marks[idx] = true
⊢ ∀ (idx_1 : Nat) (hidx : idx_1 < aig.decls.size), cache.marks[idx_1] = true → cache.marks[idx_1] = true
Tactic:
intros
Proof state after:
case extension
aig : AIG Nat
cnf : CNF aig.CNFVar
idx : Nat
omega : idx < aig.decls.size
cache : Cache aig cnf
h : idx < cache.marks.size
hmarked : cache.marks[idx] = true
idx✝ : Nat
hidx✝ : idx✝ < aig.decls.size
a✝ : cache.marks[idx✝] = true
⊢ cache.marks[idx✝] = true
Theorem: AIG.toCNF.Cache.IsExtensionBy_rfl
Proof state before:
case extension
aig : AIG Nat
cnf : CNF aig.CNFVar
idx : Nat
omega : idx < aig.decls.size
cache : Cache aig cnf
h : idx < cache.marks.size
hmarked : cache.marks[idx] = true
idx✝ : Nat
hidx✝ : idx✝ < aig.decls.size
a✝ : cache.marks[idx✝] = true
⊢ cache.marks[idx✝] = true
Tactic:
assumption
Proof state after:
no goals
Theorem: AIG.toCNF.Cache.IsExtensionBy_rfl
Proof state before:
case trueAt
aig : AIG Nat
cnf : CNF aig.CNFVar
idx : Nat
omega : idx < aig.decls.size
cache : Cache aig cnf
h : idx < cache.marks.size
hmarked : cache.marks[idx] = true
⊢ cache.marks[idx] = true
Tactic:
exact hmarked
Proof state after:
no goals
Theorem: AIG.toCNF.Cache.IsExtensionBy_set
Proof 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
Proof 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
Theorem: AIG.toCNF.Cache.IsExtensionBy_set
Proof 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
Proof state after:
no goals
Theorem: AIG.toCNF.Cache.IsExtensionBy_set
Proof 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
Proof 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
Theorem: AIG.toCNF.Cache.IsExtensionBy_set
Proof 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]
Proof 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
Theorem: AIG.toCNF.Cache.IsExtensionBy_set
Proof 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]
Proof state after:
no goals
Theorem: AIG.toCNF.Cache.IsExtensionBy_set
Proof 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
Proof 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
Theorem: AIG.toCNF.Cache.IsExtensionBy_set
Proof 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]
Proof state after:
no goals
Theorem: AIG.toCNF.Cache.IsExtensionBy_set
Proof 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]
Proof state after:
no goals
Theorem: AIG.toCNF.State.Inv_nil
Proof state before:
aig : AIG Nat
⊢ Inv []
Tactic:
simp [State.Inv]
Proof state after:
no goals
Theorem: AIG.toCNF.State.Inv_append
Proof state before:
aig✝ : AIG Nat
cnf1 cnf2 : CNF aig✝.CNFVar
h1 : Inv cnf1
h2 : Inv cnf2
⊢ Inv (cnf1 ++ cnf2)
Tactic:
intro assign1
Proof 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)
Theorem: AIG.toCNF.State.Inv_append
Proof 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
Proof 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)
Theorem: AIG.toCNF.State.Inv_append
Proof 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
Proof 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)
Theorem: AIG.toCNF.State.Inv_append
Proof 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 ⊢
Proof 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
Theorem: AIG.toCNF.State.Inv_append
Proof 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
Proof state after:
no goals
Theorem: AIG.toCNF.State.Inv_constToCNF
Proof state before:
upper : Nat
aig : AIG Nat
h : upper < aig.decls.size
b : Bool
heq : aig.decls[upper] = Decl.const b
⊢ Inv (Decl.constToCNF (Sum.inr ⟨upper, h⟩) b)
Tactic:
intro assign1
Proof state after:
upper : Nat
aig : AIG Nat
h : upper < aig.decls.size
b : Bool
heq : aig.decls[upper] = Decl.const b
assign1 : Nat → Bool
⊢ (Decl.constToCNF (Sum.inr ⟨upper, h⟩) b).sat (cnfSatAssignment aig assign1)
Theorem: AIG.toCNF.State.Inv_constToCNF
Proof state before:
upper : Nat
aig : AIG Nat
h : upper < aig.decls.size
b : Bool
heq : aig.decls[upper] = Decl.const b
assign1 : Nat → Bool
⊢ (Decl.constToCNF (Sum.inr ⟨upper, h⟩) b).sat (cnfSatAssignment aig assign1)
Tactic:
simp [CNF.sat, denote_idx_const heq]
Proof state after:
no goals
Theorem: AIG.toCNF.State.Inv_atomToCNF
Proof 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
Proof 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)
Theorem: AIG.toCNF.State.Inv_atomToCNF
Proof 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]
Proof state after:
no goals
Theorem: AIG.toCNF.State.Inv_gateToCNF
Proof 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
Proof 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
Theorem: AIG.toCNF.State.Inv_gateToCNF
Proof 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
Proof state after:
no goals
Theorem: AIG.toCNF.State.Inv_gateToCNF
Proof 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
Proof 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
Theorem: AIG.toCNF.State.Inv_gateToCNF
Proof 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
Proof state after:
no goals
Theorem: AIG.toCNF.State.Inv_gateToCNF
Proof 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
Proof 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)
Theorem: AIG.toCNF.State.Inv_gateToCNF
Proof 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]
Proof state after:
no goals