internlm/Lean-Github huggingface dataset:
Theorem: BVExpr.bitblast.go_decl_eq
Proof state before:
case append.h2.a
w idx l✝ r✝ : Nat
lhs : BVExpr l✝
rhs : BVExpr r✝
lih :
  ∀ (aig : AIG BVBit) (h1 : idx < aig.decls.size) (h2 : idx < (go aig lhs).val.aig.decls.size),
    (go aig lhs).val.aig.decls[idx] = aig.decls[idx]
rih :
  ∀ (aig : AIG BVBit) (h1 : idx < aig.decls.size) (h2 : idx < (go aig rhs).val.aig.decls.size),
    (go aig rhs).val.aig.decls[idx] = aig.decls[idx]
aig : AIG BVBit
h1 : idx < aig.decls.size
h2 : idx < (go aig (lhs.append rhs)).val.aig.decls.size
⊢ idx < ?append.h2.m

case append.h2.a
w idx l✝ r✝ : Nat
lhs : BVExpr l✝
rhs : BVExpr r✝
lih :
  ∀ (aig : AIG BVBit) (h1 : idx < aig.decls.size) (h2 : idx < (go aig lhs).val.aig.decls.size),
    (go aig lhs).val.aig.decls[idx] = aig.decls[idx]
rih :
  ∀ (aig : AIG BVBit) (h1 : idx < aig.decls.size) (h2 : idx < (go aig rhs).val.aig.decls.size),
    (go aig rhs).val.aig.decls[idx] = aig.decls[idx]
aig : AIG BVBit
h1 : idx < aig.decls.size
h2 : idx < (go aig (lhs.append rhs)).val.aig.decls.size
⊢ ?append.h2.m ≤ (go (go aig lhs).1.aig rhs).val.aig.decls.size

case append.h2.m
w idx l✝ r✝ : Nat
lhs : BVExpr l✝
rhs : BVExpr r✝
lih :
  ∀ (aig : AIG BVBit) (h1 : idx < aig.decls.size) (h2 : idx < (go aig lhs).val.aig.decls.size),
    (go aig lhs).val.aig.decls[idx] = aig.decls[idx]
rih :
  ∀ (aig : AIG BVBit) (h1 : idx < aig.decls.size) (h2 : idx < (go aig rhs).val.aig.decls.size),
    (go aig rhs).val.aig.decls[idx] = aig.decls[idx]
aig : AIG BVBit
h1 : idx < aig.decls.size
h2 : idx < (go aig (lhs.append rhs)).val.aig.decls.size
⊢ Nat
Tactic:
. exact h1
Proof state after:
case append.h2.a
w idx l✝ r✝ : Nat
lhs : BVExpr l✝
rhs : BVExpr r✝
lih :
  ∀ (aig : AIG BVBit) (h1 : idx < aig.decls.size) (h2 : idx < (go aig lhs).val.aig.decls.size),
    (go aig lhs).val.aig.decls[idx] = aig.decls[idx]
rih :
  ∀ (aig : AIG BVBit) (h1 : idx < aig.decls.size) (h2 : idx < (go aig rhs).val.aig.decls.size),
    (go aig rhs).val.aig.decls[idx] = aig.decls[idx]
aig : AIG BVBit
h1 : idx < aig.decls.size
h2 : idx < (go aig (lhs.append rhs)).val.aig.decls.size
⊢ aig.decls.size ≤ (go (go aig lhs).1.aig rhs).val.aig.decls.size
Theorem: BVExpr.bitblast.go_decl_eq
Proof state before:
case append.h2.a
w idx l✝ r✝ : Nat
lhs : BVExpr l✝
rhs : BVExpr r✝
lih :
  ∀ (aig : AIG BVBit) (h1 : idx < aig.decls.size) (h2 : idx < (go aig lhs).val.aig.decls.size),
    (go aig lhs).val.aig.decls[idx] = aig.decls[idx]
rih :
  ∀ (aig : AIG BVBit) (h1 : idx < aig.decls.size) (h2 : idx < (go aig rhs).val.aig.decls.size),
    (go aig rhs).val.aig.decls[idx] = aig.decls[idx]
aig : AIG BVBit
h1 : idx < aig.decls.size
h2 : idx < (go aig (lhs.append rhs)).val.aig.decls.size
⊢ aig.decls.size ≤ (go (go aig lhs).1.aig rhs).val.aig.decls.size
Tactic:
. apply Nat.le_trans
  . exact (bitblast.go aig lhs).property
  . exact (go (go aig lhs).1.aig rhs).property
Proof state after:
no goals
Theorem: BVExpr.bitblast.go_decl_eq
Proof state before:
case append.h2.a
w idx l✝ r✝ : Nat
lhs : BVExpr l✝
rhs : BVExpr r✝
lih :
  ∀ (aig : AIG BVBit) (h1 : idx < aig.decls.size) (h2 : idx < (go aig lhs).val.aig.decls.size),
    (go aig lhs).val.aig.decls[idx] = aig.decls[idx]
rih :
  ∀ (aig : AIG BVBit) (h1 : idx < aig.decls.size) (h2 : idx < (go aig rhs).val.aig.decls.size),
    (go aig rhs).val.aig.decls[idx] = aig.decls[idx]
aig : AIG BVBit
h1 : idx < aig.decls.size
h2 : idx < (go aig (lhs.append rhs)).val.aig.decls.size
⊢ aig.decls.size ≤ (go (go aig lhs).1.aig rhs).val.aig.decls.size
Tactic:
apply Nat.le_trans
Proof state after:
case append.h2.a.a
w idx l✝ r✝ : Nat
lhs : BVExpr l✝
rhs : BVExpr r✝
lih :
  ∀ (aig : AIG BVBit) (h1 : idx < aig.decls.size) (h2 : idx < (go aig lhs).val.aig.decls.size),
    (go aig lhs).val.aig.decls[idx] = aig.decls[idx]
rih :
  ∀ (aig : AIG BVBit) (h1 : idx < aig.decls.size) (h2 : idx < (go aig rhs).val.aig.decls.size),
    (go aig rhs).val.aig.decls[idx] = aig.decls[idx]
aig : AIG BVBit
h1 : idx < aig.decls.size
h2 : idx < (go aig (lhs.append rhs)).val.aig.decls.size
⊢ aig.decls.size ≤ ?append.h2.a.m

case append.h2.a.a
w idx l✝ r✝ : Nat
lhs : BVExpr l✝
rhs : BVExpr r✝
lih :
  ∀ (aig : AIG BVBit) (h1 : idx < aig.decls.size) (h2 : idx < (go aig lhs).val.aig.decls.size),
    (go aig lhs).val.aig.decls[idx] = aig.decls[idx]
rih :
  ∀ (aig : AIG BVBit) (h1 : idx < aig.decls.size) (h2 : idx < (go aig rhs).val.aig.decls.size),
    (go aig rhs).val.aig.decls[idx] = aig.decls[idx]
aig : AIG BVBit
h1 : idx < aig.decls.size
h2 : idx < (go aig (lhs.append rhs)).val.aig.decls.size
⊢ ?append.h2.a.m ≤ (go (go aig lhs).1.aig rhs).val.aig.decls.size

case append.h2.a.m
w idx l✝ r✝ : Nat
lhs : BVExpr l✝
rhs : BVExpr r✝
lih :
  ∀ (aig : AIG BVBit) (h1 : idx < aig.decls.size) (h2 : idx < (go aig lhs).val.aig.decls.size),
    (go aig lhs).val.aig.decls[idx] = aig.decls[idx]
rih :
  ∀ (aig : AIG BVBit) (h1 : idx < aig.decls.size) (h2 : idx < (go aig rhs).val.aig.decls.size),
    (go aig rhs).val.aig.decls[idx] = aig.decls[idx]
aig : AIG BVBit
h1 : idx < aig.decls.size
h2 : idx < (go aig (lhs.append rhs)).val.aig.decls.size
⊢ Nat
Theorem: BVExpr.bitblast.go_decl_eq
Proof state before:
case append.h2.a.a
w idx l✝ r✝ : Nat
lhs : BVExpr l✝
rhs : BVExpr r✝
lih :
  ∀ (aig : AIG BVBit) (h1 : idx < aig.decls.size) (h2 : idx < (go aig lhs).val.aig.decls.size),
    (go aig lhs).val.aig.decls[idx] = aig.decls[idx]
rih :
  ∀ (aig : AIG BVBit) (h1 : idx < aig.decls.size) (h2 : idx < (go aig rhs).val.aig.decls.size),
    (go aig rhs).val.aig.decls[idx] = aig.decls[idx]
aig : AIG BVBit
h1 : idx < aig.decls.size
h2 : idx < (go aig (lhs.append rhs)).val.aig.decls.size
⊢ aig.decls.size ≤ ?append.h2.a.m

case append.h2.a.a
w idx l✝ r✝ : Nat
lhs : BVExpr l✝
rhs : BVExpr r✝
lih :
  ∀ (aig : AIG BVBit) (h1 : idx < aig.decls.size) (h2 : idx < (go aig lhs).val.aig.decls.size),
    (go aig lhs).val.aig.decls[idx] = aig.decls[idx]
rih :
  ∀ (aig : AIG BVBit) (h1 : idx < aig.decls.size) (h2 : idx < (go aig rhs).val.aig.decls.size),
    (go aig rhs).val.aig.decls[idx] = aig.decls[idx]
aig : AIG BVBit
h1 : idx < aig.decls.size
h2 : idx < (go aig (lhs.append rhs)).val.aig.decls.size
⊢ ?append.h2.a.m ≤ (go (go aig lhs).1.aig rhs).val.aig.decls.size

case append.h2.a.m
w idx l✝ r✝ : Nat
lhs : BVExpr l✝
rhs : BVExpr r✝
lih :
  ∀ (aig : AIG BVBit) (h1 : idx < aig.decls.size) (h2 : idx < (go aig lhs).val.aig.decls.size),
    (go aig lhs).val.aig.decls[idx] = aig.decls[idx]
rih :
  ∀ (aig : AIG BVBit) (h1 : idx < aig.decls.size) (h2 : idx < (go aig rhs).val.aig.decls.size),
    (go aig rhs).val.aig.decls[idx] = aig.decls[idx]
aig : AIG BVBit
h1 : idx < aig.decls.size
h2 : idx < (go aig (lhs.append rhs)).val.aig.decls.size
⊢ Nat
Tactic:
. exact (bitblast.go aig lhs).property
Proof state after:
case append.h2.a.a
w idx l✝ r✝ : Nat
lhs : BVExpr l✝
rhs : BVExpr r✝
lih :
  ∀ (aig : AIG BVBit) (h1 : idx < aig.decls.size) (h2 : idx < (go aig lhs).val.aig.decls.size),
    (go aig lhs).val.aig.decls[idx] = aig.decls[idx]
rih :
  ∀ (aig : AIG BVBit) (h1 : idx < aig.decls.size) (h2 : idx < (go aig rhs).val.aig.decls.size),
    (go aig rhs).val.aig.decls[idx] = aig.decls[idx]
aig : AIG BVBit
h1 : idx < aig.decls.size
h2 : idx < (go aig (lhs.append rhs)).val.aig.decls.size
⊢ (go aig lhs).val.aig.decls.size ≤ (go (go aig lhs).1.aig rhs).val.aig.decls.size
Theorem: BVExpr.bitblast.go_decl_eq
Proof state before:
case append.h2.a.a
w idx l✝ r✝ : Nat
lhs : BVExpr l✝
rhs : BVExpr r✝
lih :
  ∀ (aig : AIG BVBit) (h1 : idx < aig.decls.size) (h2 : idx < (go aig lhs).val.aig.decls.size),
    (go aig lhs).val.aig.decls[idx] = aig.decls[idx]
rih :
  ∀ (aig : AIG BVBit) (h1 : idx < aig.decls.size) (h2 : idx < (go aig rhs).val.aig.decls.size),
    (go aig rhs).val.aig.decls[idx] = aig.decls[idx]
aig : AIG BVBit
h1 : idx < aig.decls.size
h2 : idx < (go aig (lhs.append rhs)).val.aig.decls.size
⊢ (go aig lhs).val.aig.decls.size ≤ (go (go aig lhs).1.aig rhs).val.aig.decls.size
Tactic:
. exact (go (go aig lhs).1.aig rhs).property
Proof state after:
no goals
Theorem: BVExpr.bitblast.go_decl_eq
Proof state before:
case append.h2.a.a
w idx l✝ r✝ : Nat
lhs : BVExpr l✝
rhs : BVExpr r✝
lih :
  ∀ (aig : AIG BVBit) (h1 : idx < aig.decls.size) (h2 : idx < (go aig lhs).val.aig.decls.size),
    (go aig lhs).val.aig.decls[idx] = aig.decls[idx]
rih :
  ∀ (aig : AIG BVBit) (h1 : idx < aig.decls.size) (h2 : idx < (go aig rhs).val.aig.decls.size),
    (go aig rhs).val.aig.decls[idx] = aig.decls[idx]
aig : AIG BVBit
h1 : idx < aig.decls.size
h2 : idx < (go aig (lhs.append rhs)).val.aig.decls.size
⊢ aig.decls.size ≤ ?append.h2.a.m
Tactic:
exact (bitblast.go aig lhs).property
Proof state after:
no goals
Theorem: BVExpr.bitblast.go_decl_eq
Proof state before:
case append.h2.a.a
w idx l✝ r✝ : Nat
lhs : BVExpr l✝
rhs : BVExpr r✝
lih :
  ∀ (aig : AIG BVBit) (h1 : idx < aig.decls.size) (h2 : idx < (go aig lhs).val.aig.decls.size),
    (go aig lhs).val.aig.decls[idx] = aig.decls[idx]
rih :
  ∀ (aig : AIG BVBit) (h1 : idx < aig.decls.size) (h2 : idx < (go aig rhs).val.aig.decls.size),
    (go aig rhs).val.aig.decls[idx] = aig.decls[idx]
aig : AIG BVBit
h1 : idx < aig.decls.size
h2 : idx < (go aig (lhs.append rhs)).val.aig.decls.size
⊢ (go aig lhs).val.aig.decls.size ≤ (go (go aig lhs).1.aig rhs).val.aig.decls.size
Tactic:
exact (go (go aig lhs).1.aig rhs).property
Proof state after:
no goals
Theorem: BVExpr.bitblast.go_decl_eq
Proof state before:
case extract
w idx w✝ hi lo : Nat
inner : BVExpr w✝
ih :
  ∀ (aig : AIG BVBit) (h1 : idx < aig.decls.size) (h2 : idx < (go aig inner).val.aig.decls.size),
    (go aig inner).val.aig.decls[idx] = aig.decls[idx]
aig : AIG BVBit
h1 : idx < aig.decls.size
h2 : idx < (go aig (extract hi lo inner)).val.aig.decls.size
⊢ (go aig (extract hi lo inner)).val.aig.decls[idx] = aig.decls[idx]
Tactic:
dsimp [go]
Proof state after:
case extract
w idx w✝ hi lo : Nat
inner : BVExpr w✝
ih :
  ∀ (aig : AIG BVBit) (h1 : idx < aig.decls.size) (h2 : idx < (go aig inner).val.aig.decls.size),
    (go aig inner).val.aig.decls[idx] = aig.decls[idx]
aig : AIG BVBit
h1 : idx < aig.decls.size
h2 : idx < (go aig (extract hi lo inner)).val.aig.decls.size
⊢ (blastExtract (go aig inner).1.aig (ExtractTarget.mk (go aig inner).1.stream hi lo ⋯)).aig.decls[idx] = aig.decls[idx]
Theorem: BVExpr.bitblast.go_decl_eq
Proof state before:
case extract
w idx w✝ hi lo : Nat
inner : BVExpr w✝
ih :
  ∀ (aig : AIG BVBit) (h1 : idx < aig.decls.size) (h2 : idx < (go aig inner).val.aig.decls.size),
    (go aig inner).val.aig.decls[idx] = aig.decls[idx]
aig : AIG BVBit
h1 : idx < aig.decls.size
h2 : idx < (go aig (extract hi lo inner)).val.aig.decls.size
⊢ (blastExtract (go aig inner).1.aig (ExtractTarget.mk (go aig inner).1.stream hi lo ⋯)).aig.decls[idx] = aig.decls[idx]
Tactic:
rw [AIG.LawfulStreamOperator.decl_eq (f := blastExtract)]
Proof state after:
case extract
w idx w✝ hi lo : Nat
inner : BVExpr w✝
ih :
  ∀ (aig : AIG BVBit) (h1 : idx < aig.decls.size) (h2 : idx < (go aig inner).val.aig.decls.size),
    (go aig inner).val.aig.decls[idx] = aig.decls[idx]
aig : AIG BVBit
h1 : idx < aig.decls.size
h2 : idx < (go aig (extract hi lo inner)).val.aig.decls.size
⊢ (go aig inner).1.aig.decls[idx] = aig.decls[idx]

case extract.h1
w idx w✝ hi lo : Nat
inner : BVExpr w✝
ih :
  ∀ (aig : AIG BVBit) (h1 : idx < aig.decls.size) (h2 : idx < (go aig inner).val.aig.decls.size),
    (go aig inner).val.aig.decls[idx] = aig.decls[idx]
aig : AIG BVBit
h1 : idx < aig.decls.size
h2 : idx < (go aig (extract hi lo inner)).val.aig.decls.size
⊢ idx < (go aig inner).1.aig.decls.size
Theorem: BVExpr.bitblast.go_decl_eq
Proof state before:
case extract
w idx w✝ hi lo : Nat
inner : BVExpr w✝
ih :
  ∀ (aig : AIG BVBit) (h1 : idx < aig.decls.size) (h2 : idx < (go aig inner).val.aig.decls.size),
    (go aig inner).val.aig.decls[idx] = aig.decls[idx]
aig : AIG BVBit
h1 : idx < aig.decls.size
h2 : idx < (go aig (extract hi lo inner)).val.aig.decls.size
⊢ (go aig inner).1.aig.decls[idx] = aig.decls[idx]

case extract.h1
w idx w✝ hi lo : Nat
inner : BVExpr w✝
ih :
  ∀ (aig : AIG BVBit) (h1 : idx < aig.decls.size) (h2 : idx < (go aig inner).val.aig.decls.size),
    (go aig inner).val.aig.decls[idx] = aig.decls[idx]
aig : AIG BVBit
h1 : idx < aig.decls.size
h2 : idx < (go aig (extract hi lo inner)).val.aig.decls.size
⊢ idx < (go aig inner).1.aig.decls.size
Tactic:
rw [ih]
Proof state after:
case extract.h2
w idx w✝ hi lo : Nat
inner : BVExpr w✝
ih :
  ∀ (aig : AIG BVBit) (h1 : idx < aig.decls.size) (h2 : idx < (go aig inner).val.aig.decls.size),
    (go aig inner).val.aig.decls[idx] = aig.decls[idx]
aig : AIG BVBit
h1 : idx < aig.decls.size
h2 : idx < (go aig (extract hi lo inner)).val.aig.decls.size
⊢ idx < (go aig inner).val.aig.decls.size
Theorem: BVExpr.bitblast.go_decl_eq
Proof state before:
case extract.h2
w idx w✝ hi lo : Nat
inner : BVExpr w✝
ih :
  ∀ (aig : AIG BVBit) (h1 : idx < aig.decls.size) (h2 : idx < (go aig inner).val.aig.decls.size),
    (go aig inner).val.aig.decls[idx] = aig.decls[idx]
aig : AIG BVBit
h1 : idx < aig.decls.size
h2 : idx < (go aig (extract hi lo inner)).val.aig.decls.size
⊢ idx < (go aig inner).val.aig.decls.size
Tactic:
apply Nat.lt_of_lt_of_le
Proof state after:
case extract.h2.a
w idx w✝ hi lo : Nat
inner : BVExpr w✝
ih :
  ∀ (aig : AIG BVBit) (h1 : idx < aig.decls.size) (h2 : idx < (go aig inner).val.aig.decls.size),
    (go aig inner).val.aig.decls[idx] = aig.decls[idx]
aig : AIG BVBit
h1 : idx < aig.decls.size
h2 : idx < (go aig (extract hi lo inner)).val.aig.decls.size
⊢ idx < ?extract.h2.m

case extract.h2.a
w idx w✝ hi lo : Nat
inner : BVExpr w✝
ih :
  ∀ (aig : AIG BVBit) (h1 : idx < aig.decls.size) (h2 : idx < (go aig inner).val.aig.decls.size),
    (go aig inner).val.aig.decls[idx] = aig.decls[idx]
aig : AIG BVBit
h1 : idx < aig.decls.size
h2 : idx < (go aig (extract hi lo inner)).val.aig.decls.size
⊢ ?extract.h2.m ≤ (go aig inner).val.aig.decls.size

case extract.h2.m
w idx w✝ hi lo : Nat
inner : BVExpr w✝
ih :
  ∀ (aig : AIG BVBit) (h1 : idx < aig.decls.size) (h2 : idx < (go aig inner).val.aig.decls.size),
    (go aig inner).val.aig.decls[idx] = aig.decls[idx]
aig : AIG BVBit
h1 : idx < aig.decls.size
h2 : idx < (go aig (extract hi lo inner)).val.aig.decls.size
⊢ Nat
Theorem: BVExpr.bitblast.go_decl_eq
Proof state before:
case extract.h2.a
w idx w✝ hi lo : Nat
inner : BVExpr w✝
ih :
  ∀ (aig : AIG BVBit) (h1 : idx < aig.decls.size) (h2 : idx < (go aig inner).val.aig.decls.size),
    (go aig inner).val.aig.decls[idx] = aig.decls[idx]
aig : AIG BVBit
h1 : idx < aig.decls.size
h2 : idx < (go aig (extract hi lo inner)).val.aig.decls.size
⊢ idx < ?extract.h2.m

case extract.h2.a
w idx w✝ hi lo : Nat
inner : BVExpr w✝
ih :
  ∀ (aig : AIG BVBit) (h1 : idx < aig.decls.size) (h2 : idx < (go aig inner).val.aig.decls.size),
    (go aig inner).val.aig.decls[idx] = aig.decls[idx]
aig : AIG BVBit
h1 : idx < aig.decls.size
h2 : idx < (go aig (extract hi lo inner)).val.aig.decls.size
⊢ ?extract.h2.m ≤ (go aig inner).val.aig.decls.size

case extract.h2.m
w idx w✝ hi lo : Nat
inner : BVExpr w✝
ih :
  ∀ (aig : AIG BVBit) (h1 : idx < aig.decls.size) (h2 : idx < (go aig inner).val.aig.decls.size),
    (go aig inner).val.aig.decls[idx] = aig.decls[idx]
aig : AIG BVBit
h1 : idx < aig.decls.size
h2 : idx < (go aig (extract hi lo inner)).val.aig.decls.size
⊢ Nat
Tactic:
. exact h1
Proof state after:
case extract.h2.a
w idx w✝ hi lo : Nat
inner : BVExpr w✝
ih :
  ∀ (aig : AIG BVBit) (h1 : idx < aig.decls.size) (h2 : idx < (go aig inner).val.aig.decls.size),
    (go aig inner).val.aig.decls[idx] = aig.decls[idx]
aig : AIG BVBit
h1 : idx < aig.decls.size
h2 : idx < (go aig (extract hi lo inner)).val.aig.decls.size
⊢ aig.decls.size ≤ (go aig inner).val.aig.decls.size
Theorem: BVExpr.bitblast.go_decl_eq
Proof state before:
case extract.h2.a
w idx w✝ hi lo : Nat
inner : BVExpr w✝
ih :
  ∀ (aig : AIG BVBit) (h1 : idx < aig.decls.size) (h2 : idx < (go aig inner).val.aig.decls.size),
    (go aig inner).val.aig.decls[idx] = aig.decls[idx]
aig : AIG BVBit
h1 : idx < aig.decls.size
h2 : idx < (go aig (extract hi lo inner)).val.aig.decls.size
⊢ aig.decls.size ≤ (go aig inner).val.aig.decls.size
Tactic:
. exact (go aig inner).property
Proof state after:
no goals
Theorem: BVExpr.bitblast.go_decl_eq
Proof state before:
case extract.h2.a
w idx w✝ hi lo : Nat
inner : BVExpr w✝
ih :
  ∀ (aig : AIG BVBit) (h1 : idx < aig.decls.size) (h2 : idx < (go aig inner).val.aig.decls.size),
    (go aig inner).val.aig.decls[idx] = aig.decls[idx]
aig : AIG BVBit
h1 : idx < aig.decls.size
h2 : idx < (go aig (extract hi lo inner)).val.aig.decls.size
⊢ idx < ?extract.h2.m
Tactic:
exact h1
Proof state after:
no goals
Theorem: BVExpr.bitblast.go_decl_eq
Proof state before:
case extract.h2.a
w idx w✝ hi lo : Nat
inner : BVExpr w✝
ih :
  ∀ (aig : AIG BVBit) (h1 : idx < aig.decls.size) (h2 : idx < (go aig inner).val.aig.decls.size),
    (go aig inner).val.aig.decls[idx] = aig.decls[idx]
aig : AIG BVBit
h1 : idx < aig.decls.size
h2 : idx < (go aig (extract hi lo inner)).val.aig.decls.size
⊢ aig.decls.size ≤ (go aig inner).val.aig.decls.size
Tactic:
exact (go aig inner).property
Proof state after:
no goals
Theorem: BVExpr.bitblast_decl_eq
Proof state before:
w : Nat
aig : AIG BVBit
expr : BVExpr w
⊢ ∀ (idx : Nat) (h1 : idx < aig.decls.size) (h2 : idx < (bitblast aig expr).aig.decls.size),
    (bitblast aig expr).aig.decls[idx] = aig.decls[idx]
Tactic:
intros
Proof state after:
w : Nat
aig : AIG BVBit
expr : BVExpr w
idx✝ : Nat
h1✝ : idx✝ < aig.decls.size
h2✝ : idx✝ < (bitblast aig expr).aig.decls.size
⊢ (bitblast aig expr).aig.decls[idx✝] = aig.decls[idx✝]
Theorem: BVExpr.bitblast_decl_eq
Proof state before:
w : Nat
aig : AIG BVBit
expr : BVExpr w
idx✝ : Nat
h1✝ : idx✝ < aig.decls.size
h2✝ : idx✝ < (bitblast aig expr).aig.decls.size
⊢ (bitblast aig expr).aig.decls[idx✝] = aig.decls[idx✝]
Tactic:
unfold bitblast
Proof state after:
w : Nat
aig : AIG BVBit
expr : BVExpr w
idx✝ : Nat
h1✝ : idx✝ < aig.decls.size
h2✝ : idx✝ < (bitblast aig expr).aig.decls.size
⊢ (bitblast.go aig expr).val.aig.decls[idx✝] = aig.decls[idx✝]
Theorem: BVExpr.bitblast_decl_eq
Proof state before:
w : Nat
aig : AIG BVBit
expr : BVExpr w
idx✝ : Nat
h1✝ : idx✝ < aig.decls.size
h2✝ : idx✝ < (bitblast aig expr).aig.decls.size
⊢ (bitblast.go aig expr).val.aig.decls[idx✝] = aig.decls[idx✝]
Tactic:
apply bitblast.go_decl_eq
Proof state after:
no goals
Theorem: bitvec_AndOrXor_2595
Proof state before:
⊢ ∀ (a b : BitVec 64), a &&& b ^^^ (a ||| b) = a ^^^ b
Tactic:
intros
Proof state after:
a✝ b✝ : BitVec 64
⊢ a✝ &&& b✝ ^^^ (a✝ ||| b✝) = a✝ ^^^ b✝
Theorem: bitvec_AndOrXor_2595
Proof state before:
a✝ b✝ : BitVec 64
⊢ a✝ &&& b✝ ^^^ (a✝ ||| b✝) = a✝ ^^^ b✝
Tactic:
bv_decide
Proof state after:
no goals
Theorem: bitvec_AndOrXor_794
Proof state before:
⊢ ∀ (a b : BitVec 64), (b.slt a && a != b) = b.slt a
Tactic:
intros
Proof state after:
a✝ b✝ : BitVec 64
⊢ (b✝.slt a✝ && a✝ != b✝) = b✝.slt a✝
Theorem: bitvec_AndOrXor_794
Proof state before:
a✝ b✝ : BitVec 64
⊢ (b✝.slt a✝ && a✝ != b✝) = b✝.slt a✝
Tactic:
bv_decide
Proof state after:
no goals
Theorem: bitvec_InstCombineShift__279
Proof state before:
⊢ ∀ (X C : BitVec 64), X >>> C <<< C = X &&& (-1) <<< C
Tactic:
intros
Proof state after:
X✝ C✝ : BitVec 64
⊢ X✝ >>> C✝ <<< C✝ = X✝ &&& (-1) <<< C✝
Theorem: bitvec_InstCombineShift__279
Proof state before:
X✝ C✝ : BitVec 64
⊢ X✝ >>> C✝ <<< C✝ = X✝ &&& (-1) <<< C✝
Tactic:
bv_decide
Proof state after:
no goals
Theorem: BVExpr.bitblast.blastVar.go_le_size
Proof state before:
w : Nat
aig : AIG BVBit
idx : Nat
s : aig.RefStream idx
a : Nat
hidx : idx ≤ w
⊢ aig.decls.size ≤ (go w aig idx s a hidx).aig.decls.size
Tactic:
unfold go
Proof state after:
w : Nat
aig : AIG BVBit
idx : Nat
s : aig.RefStream idx
a : Nat
hidx : idx ≤ w
⊢ aig.decls.size ≤
    (if hidx : idx < w then
            let res := aig.mkAtomCached (BVBit.mk a ⟨idx, hidx⟩);
            let aig_1 := res.aig;
            let bitRef := res.ref;
            let s := s.cast ⋯;
            let s := s.pushRef bitRef;
            go w aig_1 (idx + 1) s a ⋯
          else
            let_fun hidx := ⋯;
            { aig := aig, stream := hidx ▸ s }).aig.decls.size
Theorem: BVExpr.bitblast.blastVar.go_le_size
Proof state before:
w : Nat
aig : AIG BVBit
idx : Nat
s : aig.RefStream idx
a : Nat
hidx : idx ≤ w
⊢ aig.decls.size ≤
    (if hidx : idx < w then
            let res := aig.mkAtomCached (BVBit.mk a ⟨idx, hidx⟩);
            let aig_1 := res.aig;
            let bitRef := res.ref;
            let s := s.cast ⋯;
            let s := s.pushRef bitRef;
            go w aig_1 (idx + 1) s a ⋯
          else
            let_fun hidx := ⋯;
            { aig := aig, stream := hidx ▸ s }).aig.decls.size
Tactic:
split
Proof state after:
case isTrue
w : Nat
aig : AIG BVBit
idx : Nat
s : aig.RefStream idx
a : Nat
hidx : idx ≤ w
h✝ : idx < w
⊢ aig.decls.size ≤
    (let res := aig.mkAtomCached (BVBit.mk a ⟨idx, h✝⟩);
          let aig_1 := res.aig;
          let bitRef := res.ref;
          let s := s.cast ⋯;
          let s := s.pushRef bitRef;
          go w aig_1 (idx + 1) s a ⋯).aig.decls.size

case isFalse
w : Nat
aig : AIG BVBit
idx : Nat
s : aig.RefStream idx
a : Nat
hidx : idx ≤ w
h✝ : ¬idx < w
⊢ aig.decls.size ≤
    (let_fun hidx := ⋯;
          { aig := aig, stream := hidx ▸ s }).aig.decls.size
Theorem: BVExpr.bitblast.blastVar.go_le_size
Proof state before:
case isTrue
w : Nat
aig : AIG BVBit
idx : Nat
s : aig.RefStream idx
a : Nat
hidx : idx ≤ w
h✝ : idx < w
⊢ aig.decls.size ≤
    (let res := aig.mkAtomCached (BVBit.mk a ⟨idx, h✝⟩);
          let aig_1 := res.aig;
          let bitRef := res.ref;
          let s := s.cast ⋯;
          let s := s.pushRef bitRef;
          go w aig_1 (idx + 1) s a ⋯).aig.decls.size

case isFalse
w : Nat
aig : AIG BVBit
idx : Nat
s : aig.RefStream idx
a : Nat
hidx : idx ≤ w
h✝ : ¬idx < w
⊢ aig.decls.size ≤
    (let_fun hidx := ⋯;
          { aig := aig, stream := hidx ▸ s }).aig.decls.size
Tactic:
. dsimp
  refine Nat.le_trans ?_ (by apply go_le_size)
  apply AIG.LawfulOperator.le_size
Proof state after:
case isFalse
w : Nat
aig : AIG BVBit
idx : Nat
s : aig.RefStream idx
a : Nat
hidx : idx ≤ w
h✝ : ¬idx < w
⊢ aig.decls.size ≤
    (let_fun hidx := ⋯;
          { aig := aig, stream := hidx ▸ s }).aig.decls.size
Theorem: BVExpr.bitblast.blastVar.go_le_size
Proof state before:
case isFalse
w : Nat
aig : AIG BVBit
idx : Nat
s : aig.RefStream idx
a : Nat
hidx : idx ≤ w
h✝ : ¬idx < w
⊢ aig.decls.size ≤
    (let_fun hidx := ⋯;
          { aig := aig, stream := hidx ▸ s }).aig.decls.size
Tactic:
. simp
Proof state after:
no goals
Theorem: BVExpr.bitblast.blastVar.go_le_size
Proof state before:
case isTrue
w : Nat
aig : AIG BVBit
idx : Nat
s : aig.RefStream idx
a : Nat
hidx : idx ≤ w
h✝ : idx < w
⊢ aig.decls.size ≤
    (let res := aig.mkAtomCached (BVBit.mk a ⟨idx, h✝⟩);
          let aig_1 := res.aig;
          let bitRef := res.ref;
          let s := s.cast ⋯;
          let s := s.pushRef bitRef;
          go w aig_1 (idx + 1) s a ⋯).aig.decls.size
Tactic:
dsimp
Proof state after:
case isTrue
w : Nat
aig : AIG BVBit
idx : Nat
s : aig.RefStream idx
a : Nat
hidx : idx ≤ w
h✝ : idx < w
⊢ aig.decls.size ≤
    (go w (aig.mkAtomCached (BVBit.mk a ⟨idx, h✝⟩)).aig (idx + 1)
            ((s.cast ⋯).pushRef (aig.mkAtomCached (BVBit.mk a ⟨idx, h✝⟩)).ref) a ⋯).aig.decls.size
Theorem: BVExpr.bitblast.blastVar.go_le_size
Proof state before:
case isTrue
w : Nat
aig : AIG BVBit
idx : Nat
s : aig.RefStream idx
a : Nat
hidx : idx ≤ w
h✝ : idx < w
⊢ aig.decls.size ≤
    (go w (aig.mkAtomCached (BVBit.mk a ⟨idx, h✝⟩)).aig (idx + 1)
            ((s.cast ⋯).pushRef (aig.mkAtomCached (BVBit.mk a ⟨idx, h✝⟩)).ref) a ⋯).aig.decls.size
Tactic:
refine Nat.le_trans ?_ (by apply go_le_size)
Proof state after:
case isTrue
w : Nat
aig : AIG BVBit
idx : Nat
s : aig.RefStream idx
a : Nat
hidx : idx ≤ w
h✝ : idx < w
⊢ aig.decls.size ≤ (aig.mkAtomCached (BVBit.mk a ⟨idx, h✝⟩)).aig.decls.size
Theorem: BVExpr.bitblast.blastVar.go_le_size
Proof state before:
case isTrue
w : Nat
aig : AIG BVBit
idx : Nat
s : aig.RefStream idx
a : Nat
hidx : idx ≤ w
h✝ : idx < w
⊢ aig.decls.size ≤ (aig.mkAtomCached (BVBit.mk a ⟨idx, h✝⟩)).aig.decls.size
Tactic:
apply AIG.LawfulOperator.le_size
Proof state after:
no goals