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

State before:
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
⊢ cache1.IsExtensionBy cache3 new1 hnew1
Tactic:
apply IsExtensionBy.mk
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), cache1.marks[idx] = true → cache3.marks[idx] = true

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[new1] = true

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

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[new1] = true
Tactic:
. intro idx hidx hmarked
  apply h23.extension
  . apply h12.extension
    . exact hmarked
    . omega
  . omega
State after:
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[new1] = true

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[new1] = true
Tactic:
. apply h23.extension
  . exact h12.trueAt
  . omega
State after:
no goals

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
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

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
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

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
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

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
State after:
no goals

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
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

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
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

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
State after:
no goals

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
State after:
no goals

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
State after:
no goals

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
State after:
no goals

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[new1] = true
Tactic:
apply h23.extension
State after:
case trueAt.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
⊢ cache2.marks[new1] = true

case trueAt.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
⊢ new1 < aig.decls.size

State before:
case trueAt.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
⊢ cache2.marks[new1] = true

case trueAt.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
⊢ new1 < aig.decls.size
Tactic:
. exact h12.trueAt
State after:
case trueAt.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
⊢ new1 < aig.decls.size

State before:
case trueAt.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
⊢ new1 < aig.decls.size
Tactic:
. omega
State after:
no goals

State before:
case trueAt.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
⊢ cache2.marks[new1] = true
Tactic:
exact h12.trueAt
State after:
no goals

State before:
case trueAt.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
⊢ new1 < aig.decls.size
Tactic:
omega
State after:
no goals