internlm/Lean-Github huggingface dataset:
Theorem: BVExpr.bitblast.go_decl_eq
Proof state before:
case zeroExtend.h2.a
w✝¹ idx w✝ w : 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 (zeroExtend w 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 signExtend
w✝¹ idx w✝ w : 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 (signExtend w inner)).val.aig.decls.size
⊢ (go aig (signExtend w inner)).val.aig.decls[idx] = aig.decls[idx]
Tactic:
dsimp [go]
Proof state after:
case signExtend
w✝¹ idx w✝ w : 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 (signExtend w inner)).val.aig.decls.size
⊢ (blastSignExtend (go aig inner).1.aig { w := w✝, stream := (go aig inner).1.stream }).aig.decls[idx] = aig.decls[idx]
Theorem: BVExpr.bitblast.go_decl_eq
Proof state before:
case signExtend
w✝¹ idx w✝ w : 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 (signExtend w inner)).val.aig.decls.size
⊢ (blastSignExtend (go aig inner).1.aig { w := w✝, stream := (go aig inner).1.stream }).aig.decls[idx] = aig.decls[idx]
Tactic:
rw [AIG.LawfulStreamOperator.decl_eq (f := blastSignExtend)]
Proof state after:
case signExtend
w✝¹ idx w✝ w : 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 (signExtend w inner)).val.aig.decls.size
⊢ (go aig inner).1.aig.decls[idx] = aig.decls[idx]

case signExtend.h1
w✝¹ idx w✝ w : 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 (signExtend w inner)).val.aig.decls.size
⊢ idx < (go aig inner).1.aig.decls.size
Theorem: BVExpr.bitblast.go_decl_eq
Proof state before:
case signExtend
w✝¹ idx w✝ w : 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 (signExtend w inner)).val.aig.decls.size
⊢ (go aig inner).1.aig.decls[idx] = aig.decls[idx]

case signExtend.h1
w✝¹ idx w✝ w : 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 (signExtend w inner)).val.aig.decls.size
⊢ idx < (go aig inner).1.aig.decls.size
Tactic:
rw [ih]
Proof state after:
case signExtend.h2
w✝¹ idx w✝ w : 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 (signExtend w inner)).val.aig.decls.size
⊢ idx < (go aig inner).val.aig.decls.size
Theorem: BVExpr.bitblast.go_decl_eq
Proof state before:
case signExtend.h2
w✝¹ idx w✝ w : 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 (signExtend w 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 signExtend.h2.a
w✝¹ idx w✝ w : 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 (signExtend w inner)).val.aig.decls.size
⊢ idx < ?signExtend.h2.m

case signExtend.h2.a
w✝¹ idx w✝ w : 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 (signExtend w inner)).val.aig.decls.size
⊢ ?signExtend.h2.m ≤ (go aig inner).val.aig.decls.size

case signExtend.h2.m
w✝¹ idx w✝ w : 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 (signExtend w inner)).val.aig.decls.size
⊢ Nat
Theorem: BVExpr.bitblast.go_decl_eq
Proof state before:
case signExtend.h2.a
w✝¹ idx w✝ w : 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 (signExtend w inner)).val.aig.decls.size
⊢ idx < ?signExtend.h2.m

case signExtend.h2.a
w✝¹ idx w✝ w : 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 (signExtend w inner)).val.aig.decls.size
⊢ ?signExtend.h2.m ≤ (go aig inner).val.aig.decls.size

case signExtend.h2.m
w✝¹ idx w✝ w : 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 (signExtend w inner)).val.aig.decls.size
⊢ Nat
Tactic:
. exact h1
Proof state after:
case signExtend.h2.a
w✝¹ idx w✝ w : 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 (signExtend w 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 signExtend.h2.a
w✝¹ idx w✝ w : 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 (signExtend w 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 signExtend.h2.a
w✝¹ idx w✝ w : 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 (signExtend w inner)).val.aig.decls.size
⊢ idx < ?signExtend.h2.m
Tactic:
exact h1
Proof state after:
no goals
Theorem: BVExpr.bitblast.go_decl_eq
Proof state before:
case signExtend.h2.a
w✝¹ idx w✝ w : 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 (signExtend w 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 append
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.append rhs)).val.aig.decls[idx] = aig.decls[idx]
Tactic:
dsimp [go]
Proof state after:
case append
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
⊢ (blastAppend (go (go aig lhs).1.aig rhs).1.aig
            (AppendTarget.mk ((go aig lhs).1.stream.cast ⋯) (go (go aig lhs).1.aig rhs).1.stream ⋯)).aig.decls[idx] =
    aig.decls[idx]
Theorem: BVExpr.bitblast.go_decl_eq
Proof state before:
case append
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
⊢ (blastAppend (go (go aig lhs).1.aig rhs).1.aig
            (AppendTarget.mk ((go aig lhs).1.stream.cast ⋯) (go (go aig lhs).1.aig rhs).1.stream ⋯)).aig.decls[idx] =
    aig.decls[idx]
Tactic:
rw [AIG.LawfulStreamOperator.decl_eq (f := blastAppend)]
Proof state after:
case append
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 (go aig lhs).1.aig rhs).1.aig.decls[idx] = aig.decls[idx]

case append.h1
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 < (go (go aig lhs).1.aig rhs).1.aig.decls.size
Theorem: BVExpr.bitblast.go_decl_eq
Proof state before:
case append
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 (go aig lhs).1.aig rhs).1.aig.decls[idx] = aig.decls[idx]

case append.h1
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 < (go (go aig lhs).1.aig rhs).1.aig.decls.size
Tactic:
rw [rih, lih]
Proof state after:
case append.h2
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 < (go aig lhs).val.aig.decls.size

case append.h2
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 < (go (go aig lhs).1.aig rhs).val.aig.decls.size
Theorem: BVExpr.bitblast.go_decl_eq
Proof state before:
case append.h2
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 < (go aig lhs).val.aig.decls.size

case append.h2
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 < (go (go aig lhs).1.aig rhs).val.aig.decls.size
Tactic:
. apply Nat.lt_of_lt_of_le
  . exact h1
  . exact (bitblast.go aig lhs).property
Proof state after:
case append.h2
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 < (go (go aig lhs).1.aig rhs).val.aig.decls.size
Theorem: BVExpr.bitblast.go_decl_eq
Proof state before:
case append.h2
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 < (go (go aig lhs).1.aig rhs).val.aig.decls.size
Tactic:
. apply Nat.lt_of_lt_of_le
  . exact h1
  . 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
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 < (go aig lhs).val.aig.decls.size
Tactic:
apply Nat.lt_of_lt_of_le
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
⊢ 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 aig lhs).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
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 aig lhs).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 aig lhs).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 aig lhs).val.aig.decls.size
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
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
Tactic:
exact h1
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 aig lhs).val.aig.decls.size
Tactic:
exact (bitblast.go aig lhs).property
Proof state after:
no goals
Theorem: BVExpr.bitblast.go_decl_eq
Proof state before:
case append.h2
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 < (go (go aig lhs).1.aig rhs).val.aig.decls.size
Tactic:
apply Nat.lt_of_lt_of_le
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
⊢ 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