internlm/Lean-Github huggingface dataset:
Theorem: Decl.atomToCNF_eval
Proof state before:
α✝ : Type
output a : α✝
assign : α✝ → Bool
⊢ CNF.eval assign (atomToCNF output a) = (assign output == assign a)
Tactic:
simp only [atomToCNF, CNF.eval_succ, CNF.Clause.eval_succ, Bool.beq_true, Bool.beq_false,
  CNF.Clause.eval_nil, Bool.or_false, CNF.eval_nil, Bool.and_true]
Proof state after:
α✝ : Type
output a : α✝
assign : α✝ → Bool
⊢ ((assign output || !assign a) && (!assign output || assign a)) = (assign output == assign a)
Theorem: Decl.atomToCNF_eval
Proof state before:
α✝ : Type
output a : α✝
assign : α✝ → Bool
⊢ ((assign output || !assign a) && (!assign output || assign a)) = (assign output == assign a)
Tactic:
cases assign output <;> cases assign a <;> decide
Proof state after:
no goals
Theorem: Decl.gateToCNF_eval
Proof state before:
α✝ : Type
output lhs rhs : α✝
linv rinv : Bool
assign : α✝ → Bool
⊢ CNF.eval assign (gateToCNF output lhs rhs linv rinv) =
    (assign output == (xor (assign lhs) linv && xor (assign rhs) rinv))
Tactic:
simp [gateToCNF, CNF.eval, CNF.Clause.eval]
Proof state after:
α✝ : Type
output lhs rhs : α✝
linv rinv : Bool
assign : α✝ → Bool
⊢ ((!assign output || assign lhs == !linv) &&
      ((!assign output || assign rhs == !rinv) && (assign output || (assign lhs == linv || assign rhs == rinv)))) =
    (assign output == (xor (assign lhs) linv && xor (assign rhs) rinv))
Theorem: Decl.gateToCNF_eval
Proof state before:
α✝ : Type
output lhs rhs : α✝
linv rinv : Bool
assign : α✝ → Bool
⊢ ((!assign output || assign lhs == !linv) &&
      ((!assign output || assign rhs == !rinv) && (assign output || (assign lhs == linv || assign rhs == rinv)))) =
    (assign output == (xor (assign lhs) linv && xor (assign rhs) rinv))
Tactic:
cases assign output
  <;> cases assign lhs
    <;> cases assign rhs
      <;> cases linv
        <;> cases rinv
          <;> decide
Proof state after:
no goals
Theorem: AIG.toCNF.projectLeftAssign_property
Proof state before:
aig✝ : AIG Nat
assign : aig✝.CNFVar → Bool
x : Nat
⊢ projectLeftAssign assign x = assign (Sum.inl x)
Tactic:
simp [projectLeftAssign]
Proof state after:
no goals
Theorem: AIG.toCNF.projectRightAssign_property
Proof state before:
aig✝ : AIG Nat
assign : aig✝.CNFVar → Bool
x : Nat
hx : x < aig✝.decls.size
⊢ projectRightAssign assign x hx = assign (Sum.inr ⟨x, hx⟩)
Tactic:
simp [projectRightAssign]
Proof state after:
no goals
Theorem: AIG.toCNF.satAssignment_inl
Proof state before:
aig : AIG Nat
assign1 : Nat → Bool
x : Nat
⊢ cnfSatAssignment aig assign1 (Sum.inl x) = assign1 x
Tactic:
simp [cnfSatAssignment, mixAssigns]
Proof state after:
no goals
Theorem: AIG.toCNF.satAssignment_inr
Proof state before:
aig : AIG Nat
assign1 : Nat → Bool
x : Fin aig.decls.size
⊢ cnfSatAssignment aig assign1 (Sum.inr x) = ⟦{ aig := aig, ref := { gate := ↑x, hgate := ⋯ } }, assign1⟧
Tactic:
simp [cnfSatAssignment, mixAssigns]
Proof state after:
no goals
Theorem: AIG.toCNF.Cache.Inv_init
Proof state before:
aig : AIG Nat
⊢ (mkArray aig.decls.size false).size = aig.decls.size
Tactic:
simp
Proof state after:
no goals
Theorem: AIG.toCNF.Cache.Inv_init
Proof state before:
aig : AIG Nat
⊢ ∀ (lhs rhs : Nat) (linv rinv : Bool) (idx : Nat) (hbound : idx < aig.decls.size),
    (mkArray aig.decls.size false)[idx] = true →
      ∀ (heq : aig.decls[idx] = Decl.gate lhs rhs linv rinv),
        (mkArray aig.decls.size false)[lhs] = true ∧ (mkArray aig.decls.size false)[rhs] = true
Tactic:
intro lhs rhs linv rinv idx hbound hmarked heq
Proof state after:
aig : AIG Nat
lhs rhs : Nat
linv rinv : Bool
idx : Nat
hbound : idx < aig.decls.size
hmarked : (mkArray aig.decls.size false)[idx] = true
heq : aig.decls[idx] = Decl.gate lhs rhs linv rinv
⊢ (mkArray aig.decls.size false)[lhs] = true ∧ (mkArray aig.decls.size false)[rhs] = true
Theorem: AIG.toCNF.Cache.Inv_init
Proof state before:
aig : AIG Nat
lhs rhs : Nat
linv rinv : Bool
idx : Nat
hbound : idx < aig.decls.size
hmarked : (mkArray aig.decls.size false)[idx] = true
heq : aig.decls[idx] = Decl.gate lhs rhs linv rinv
⊢ (mkArray aig.decls.size false)[lhs] = true ∧ (mkArray aig.decls.size false)[rhs] = true
Tactic:
simp at hmarked
Proof state after:
no goals
Theorem: AIG.toCNF.Cache.Inv_init
Proof state before:
aig : AIG Nat
⊢ ∀ (assign : aig.CNFVar → Bool),
    CNF.eval assign [] = true →
      ∀ (idx : Nat) (hbound : idx < aig.decls.size),
        (mkArray aig.decls.size false)[idx] = true →
          ⟦{ aig := aig, ref := { gate := idx, hgate := hbound } }, projectLeftAssign assign⟧ =
            projectRightAssign assign idx hbound
Tactic:
intro assign _ idx hbound hmark
Proof state after:
aig : AIG Nat
assign : aig.CNFVar → Bool
_heval✝ : CNF.eval assign [] = true
idx : Nat
hbound : idx < aig.decls.size
hmark : (mkArray aig.decls.size false)[idx] = true
⊢ ⟦{ aig := aig, ref := { gate := idx, hgate := hbound } }, projectLeftAssign assign⟧ =
    projectRightAssign assign idx hbound
Theorem: AIG.toCNF.Cache.Inv_init
Proof state before:
aig : AIG Nat
assign : aig.CNFVar → Bool
_heval✝ : CNF.eval assign [] = true
idx : Nat
hbound : idx < aig.decls.size
hmark : (mkArray aig.decls.size false)[idx] = true
⊢ ⟦{ aig := aig, ref := { gate := idx, hgate := hbound } }, projectLeftAssign assign⟧ =
    projectRightAssign assign idx hbound
Tactic:
simp at hmark
Proof state after:
no goals
Theorem: AIG.toCNF.Cache.IsExtensionBy_trans_left
Proof 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
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), 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
Theorem: AIG.toCNF.Cache.IsExtensionBy_trans_left
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

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
Proof 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
Theorem: AIG.toCNF.Cache.IsExtensionBy_trans_left
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[new1] = true
Tactic:
. apply h23.extension
  . exact h12.trueAt
  . omega
Proof state after:
no goals
Theorem: AIG.toCNF.Cache.IsExtensionBy_trans_left
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_left
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_left
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_left
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_left
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_left
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_left
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_left
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_left
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_left
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_left
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[new1] = true
Tactic:
apply h23.extension
Proof 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
Theorem: AIG.toCNF.Cache.IsExtensionBy_trans_left
Proof 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
Proof 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
Theorem: AIG.toCNF.Cache.IsExtensionBy_trans_left
Proof 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
Proof state after:
no goals
Theorem: AIG.toCNF.Cache.IsExtensionBy_trans_left
Proof 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
Proof state after:
no goals
Theorem: AIG.toCNF.Cache.IsExtensionBy_trans_left
Proof 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
Proof state after:
no goals
Theorem: AIG.toCNF.Cache.IsExtensionBy_trans_right
Proof 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 new2 hnew2
Tactic:
apply IsExtensionBy.mk
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), 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[new2] = 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), 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[new2] = true
Tactic:
. intro idx hidx hmarked
  apply h23.extension
  . apply h12.extension
    . exact hmarked
    . omega
  . omega
Proof 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[new2] = true
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