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

State before:
aig : AIG Nat
new1 : Nat
hnew1 : new1 < aig.decls.size
new2 : Nat
hnew2 : new2 < aig.decls.size
state1 state2 state3 : State aig
h12 : state1.IsExtensionBy state2 new1 hnew1
h23 : state2.IsExtensionBy state3 new2 hnew2
⊢ state1.IsExtensionBy state3 new1 hnew1
Tactic:
apply  Cache.IsExtensionBy_trans_left
State after:
case h12
aig : AIG Nat
new1 : Nat
hnew1 : new1 < aig.decls.size
new2 : Nat
hnew2 : new2 < aig.decls.size
state1 state2 state3 : State aig
h12 : state1.IsExtensionBy state2 new1 hnew1
h23 : state2.IsExtensionBy state3 new2 hnew2
⊢ state1.cache.IsExtensionBy ?cache2 new1 hnew1

case h23
aig : AIG Nat
new1 : Nat
hnew1 : new1 < aig.decls.size
new2 : Nat
hnew2 : new2 < aig.decls.size
state1 state2 state3 : State aig
h12 : state1.IsExtensionBy state2 new1 hnew1
h23 : state2.IsExtensionBy state3 new2 hnew2
⊢ ?cache2.IsExtensionBy state3.cache ?new2 ?hnew2

case cnf2
aig : AIG Nat
new1 : Nat
hnew1 : new1 < aig.decls.size
new2 : Nat
hnew2 : new2 < aig.decls.size
state1 state2 state3 : State aig
h12 : state1.IsExtensionBy state2 new1 hnew1
h23 : state2.IsExtensionBy state3 new2 hnew2
⊢ CNF aig.CNFVar

case new2
aig : AIG Nat
new1 : Nat
hnew1 : new1 < aig.decls.size
new2 : Nat
hnew2 : new2 < aig.decls.size
state1 state2 state3 : State aig
h12 : state1.IsExtensionBy state2 new1 hnew1
h23 : state2.IsExtensionBy state3 new2 hnew2
⊢ Nat

case hnew2
aig : AIG Nat
new1 : Nat
hnew1 : new1 < aig.decls.size
new2 : Nat
hnew2 : new2 < aig.decls.size
state1 state2 state3 : State aig
h12 : state1.IsExtensionBy state2 new1 hnew1
h23 : state2.IsExtensionBy state3 new2 hnew2
⊢ ?new2 < aig.decls.size

case cache2
aig : AIG Nat
new1 : Nat
hnew1 : new1 < aig.decls.size
new2 : Nat
hnew2 : new2 < aig.decls.size
state1 state2 state3 : State aig
h12 : state1.IsExtensionBy state2 new1 hnew1
h23 : state2.IsExtensionBy state3 new2 hnew2
⊢ Cache aig ?cnf2

State before:
case h12
aig : AIG Nat
new1 : Nat
hnew1 : new1 < aig.decls.size
new2 : Nat
hnew2 : new2 < aig.decls.size
state1 state2 state3 : State aig
h12 : state1.IsExtensionBy state2 new1 hnew1
h23 : state2.IsExtensionBy state3 new2 hnew2
⊢ state1.cache.IsExtensionBy ?cache2 new1 hnew1

case h23
aig : AIG Nat
new1 : Nat
hnew1 : new1 < aig.decls.size
new2 : Nat
hnew2 : new2 < aig.decls.size
state1 state2 state3 : State aig
h12 : state1.IsExtensionBy state2 new1 hnew1
h23 : state2.IsExtensionBy state3 new2 hnew2
⊢ ?cache2.IsExtensionBy state3.cache ?new2 ?hnew2

case cnf2
aig : AIG Nat
new1 : Nat
hnew1 : new1 < aig.decls.size
new2 : Nat
hnew2 : new2 < aig.decls.size
state1 state2 state3 : State aig
h12 : state1.IsExtensionBy state2 new1 hnew1
h23 : state2.IsExtensionBy state3 new2 hnew2
⊢ CNF aig.CNFVar

case new2
aig : AIG Nat
new1 : Nat
hnew1 : new1 < aig.decls.size
new2 : Nat
hnew2 : new2 < aig.decls.size
state1 state2 state3 : State aig
h12 : state1.IsExtensionBy state2 new1 hnew1
h23 : state2.IsExtensionBy state3 new2 hnew2
⊢ Nat

case hnew2
aig : AIG Nat
new1 : Nat
hnew1 : new1 < aig.decls.size
new2 : Nat
hnew2 : new2 < aig.decls.size
state1 state2 state3 : State aig
h12 : state1.IsExtensionBy state2 new1 hnew1
h23 : state2.IsExtensionBy state3 new2 hnew2
⊢ ?new2 < aig.decls.size

case cache2
aig : AIG Nat
new1 : Nat
hnew1 : new1 < aig.decls.size
new2 : Nat
hnew2 : new2 < aig.decls.size
state1 state2 state3 : State aig
h12 : state1.IsExtensionBy state2 new1 hnew1
h23 : state2.IsExtensionBy state3 new2 hnew2
⊢ Cache aig ?cnf2
Tactic:
. exact h12
State after:
case h23
aig : AIG Nat
new1 : Nat
hnew1 : new1 < aig.decls.size
new2 : Nat
hnew2 : new2 < aig.decls.size
state1 state2 state3 : State aig
h12 : state1.IsExtensionBy state2 new1 hnew1
h23 : state2.IsExtensionBy state3 new2 hnew2
⊢ state2.cache.IsExtensionBy state3.cache ?new2 ?hnew2

case new2
aig : AIG Nat
new1 : Nat
hnew1 : new1 < aig.decls.size
new2 : Nat
hnew2 : new2 < aig.decls.size
state1 state2 state3 : State aig
h12 : state1.IsExtensionBy state2 new1 hnew1
h23 : state2.IsExtensionBy state3 new2 hnew2
⊢ Nat

case hnew2
aig : AIG Nat
new1 : Nat
hnew1 : new1 < aig.decls.size
new2 : Nat
hnew2 : new2 < aig.decls.size
state1 state2 state3 : State aig
h12 : state1.IsExtensionBy state2 new1 hnew1
h23 : state2.IsExtensionBy state3 new2 hnew2
⊢ ?new2 < aig.decls.size

State before:
case h23
aig : AIG Nat
new1 : Nat
hnew1 : new1 < aig.decls.size
new2 : Nat
hnew2 : new2 < aig.decls.size
state1 state2 state3 : State aig
h12 : state1.IsExtensionBy state2 new1 hnew1
h23 : state2.IsExtensionBy state3 new2 hnew2
⊢ state2.cache.IsExtensionBy state3.cache ?new2 ?hnew2

case new2
aig : AIG Nat
new1 : Nat
hnew1 : new1 < aig.decls.size
new2 : Nat
hnew2 : new2 < aig.decls.size
state1 state2 state3 : State aig
h12 : state1.IsExtensionBy state2 new1 hnew1
h23 : state2.IsExtensionBy state3 new2 hnew2
⊢ Nat

case hnew2
aig : AIG Nat
new1 : Nat
hnew1 : new1 < aig.decls.size
new2 : Nat
hnew2 : new2 < aig.decls.size
state1 state2 state3 : State aig
h12 : state1.IsExtensionBy state2 new1 hnew1
h23 : state2.IsExtensionBy state3 new2 hnew2
⊢ ?new2 < aig.decls.size
Tactic:
. exact h23
State after:
no goals

State before:
case h12
aig : AIG Nat
new1 : Nat
hnew1 : new1 < aig.decls.size
new2 : Nat
hnew2 : new2 < aig.decls.size
state1 state2 state3 : State aig
h12 : state1.IsExtensionBy state2 new1 hnew1
h23 : state2.IsExtensionBy state3 new2 hnew2
⊢ state1.cache.IsExtensionBy ?cache2 new1 hnew1
Tactic:
exact h12
State after:
no goals

State before:
case h23
aig : AIG Nat
new1 : Nat
hnew1 : new1 < aig.decls.size
new2 : Nat
hnew2 : new2 < aig.decls.size
state1 state2 state3 : State aig
h12 : state1.IsExtensionBy state2 new1 hnew1
h23 : state2.IsExtensionBy state3 new2 hnew2
⊢ state2.cache.IsExtensionBy state3.cache ?new2 ?hnew2
Tactic:
exact h23
State after:
no goals