internlm/Lean-Github huggingface dataset:
Theorem: BVExpr.bitblast.go_decl_eq
Proof state before:
case h2.a
w idx w✝ : Nat
op : BVUnOp
expr : BVExpr w✝
ih :
  ∀ (aig : AIG BVBit) (h1 : idx < aig.decls.size) (h2 : idx < (go aig expr).val.aig.decls.size),
    (go aig expr).val.aig.decls[idx] = aig.decls[idx]
aig : AIG BVBit
h1 : idx < aig.decls.size
n✝ : Nat
h2 : idx < (go aig (un (BVUnOp.rotateLeft n✝) expr)).val.aig.decls.size
⊢ aig.decls.size ≤ (go aig expr).val.aig.decls.size
Tactic:
exact (go aig expr).property
Proof state after:
no goals
Theorem: BVExpr.bitblast.go_decl_eq
Proof state before:
w idx w✝ : Nat
op : BVUnOp
expr : BVExpr w✝
ih :
  ∀ (aig : AIG BVBit) (h1 : idx < aig.decls.size) (h2 : idx < (go aig expr).val.aig.decls.size),
    (go aig expr).val.aig.decls[idx] = aig.decls[idx]
aig : AIG BVBit
h1 : idx < aig.decls.size
n✝ : Nat
h2 : idx < (go aig (un (BVUnOp.rotateRight n✝) expr)).val.aig.decls.size
⊢ (go aig (un (BVUnOp.rotateRight n✝) expr)).val.aig.decls[idx] = aig.decls[idx]
Tactic:
dsimp [go]
Proof state after:
w idx w✝ : Nat
op : BVUnOp
expr : BVExpr w✝
ih :
  ∀ (aig : AIG BVBit) (h1 : idx < aig.decls.size) (h2 : idx < (go aig expr).val.aig.decls.size),
    (go aig expr).val.aig.decls[idx] = aig.decls[idx]
aig : AIG BVBit
h1 : idx < aig.decls.size
n✝ : Nat
h2 : idx < (go aig (un (BVUnOp.rotateRight n✝) expr)).val.aig.decls.size
⊢ (blastRotateRight (go aig expr).1.aig { stream := (go aig expr).1.stream, distance := n✝ }).aig.decls[idx] =
    aig.decls[idx]
Theorem: BVExpr.bitblast.go_decl_eq
Proof state before:
w idx w✝ : Nat
op : BVUnOp
expr : BVExpr w✝
ih :
  ∀ (aig : AIG BVBit) (h1 : idx < aig.decls.size) (h2 : idx < (go aig expr).val.aig.decls.size),
    (go aig expr).val.aig.decls[idx] = aig.decls[idx]
aig : AIG BVBit
h1 : idx < aig.decls.size
n✝ : Nat
h2 : idx < (go aig (un (BVUnOp.rotateRight n✝) expr)).val.aig.decls.size
⊢ (blastRotateRight (go aig expr).1.aig { stream := (go aig expr).1.stream, distance := n✝ }).aig.decls[idx] =
    aig.decls[idx]
Tactic:
rw [AIG.LawfulStreamOperator.decl_eq (f := blastRotateRight)]
Proof state after:
w idx w✝ : Nat
op : BVUnOp
expr : BVExpr w✝
ih :
  ∀ (aig : AIG BVBit) (h1 : idx < aig.decls.size) (h2 : idx < (go aig expr).val.aig.decls.size),
    (go aig expr).val.aig.decls[idx] = aig.decls[idx]
aig : AIG BVBit
h1 : idx < aig.decls.size
n✝ : Nat
h2 : idx < (go aig (un (BVUnOp.rotateRight n✝) expr)).val.aig.decls.size
⊢ (go aig expr).1.aig.decls[idx] = aig.decls[idx]

case h1
w idx w✝ : Nat
op : BVUnOp
expr : BVExpr w✝
ih :
  ∀ (aig : AIG BVBit) (h1 : idx < aig.decls.size) (h2 : idx < (go aig expr).val.aig.decls.size),
    (go aig expr).val.aig.decls[idx] = aig.decls[idx]
aig : AIG BVBit
h1 : idx < aig.decls.size
n✝ : Nat
h2 : idx < (go aig (un (BVUnOp.rotateRight n✝) expr)).val.aig.decls.size
⊢ idx < (go aig expr).1.aig.decls.size
Theorem: BVExpr.bitblast.go_decl_eq
Proof state before:
w idx w✝ : Nat
op : BVUnOp
expr : BVExpr w✝
ih :
  ∀ (aig : AIG BVBit) (h1 : idx < aig.decls.size) (h2 : idx < (go aig expr).val.aig.decls.size),
    (go aig expr).val.aig.decls[idx] = aig.decls[idx]
aig : AIG BVBit
h1 : idx < aig.decls.size
n✝ : Nat
h2 : idx < (go aig (un (BVUnOp.rotateRight n✝) expr)).val.aig.decls.size
⊢ (go aig expr).1.aig.decls[idx] = aig.decls[idx]

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

case h2.a
w idx w✝ : Nat
op : BVUnOp
expr : BVExpr w✝
ih :
  ∀ (aig : AIG BVBit) (h1 : idx < aig.decls.size) (h2 : idx < (go aig expr).val.aig.decls.size),
    (go aig expr).val.aig.decls[idx] = aig.decls[idx]
aig : AIG BVBit
h1 : idx < aig.decls.size
n✝ : Nat
h2 : idx < (go aig (un (BVUnOp.rotateRight n✝) expr)).val.aig.decls.size
⊢ ?h2.m ≤ (go aig expr).val.aig.decls.size

case h2.m
w idx w✝ : Nat
op : BVUnOp
expr : BVExpr w✝
ih :
  ∀ (aig : AIG BVBit) (h1 : idx < aig.decls.size) (h2 : idx < (go aig expr).val.aig.decls.size),
    (go aig expr).val.aig.decls[idx] = aig.decls[idx]
aig : AIG BVBit
h1 : idx < aig.decls.size
n✝ : Nat
h2 : idx < (go aig (un (BVUnOp.rotateRight n✝) expr)).val.aig.decls.size
⊢ Nat
Theorem: BVExpr.bitblast.go_decl_eq
Proof state before:
case h2.a
w idx w✝ : Nat
op : BVUnOp
expr : BVExpr w✝
ih :
  ∀ (aig : AIG BVBit) (h1 : idx < aig.decls.size) (h2 : idx < (go aig expr).val.aig.decls.size),
    (go aig expr).val.aig.decls[idx] = aig.decls[idx]
aig : AIG BVBit
h1 : idx < aig.decls.size
n✝ : Nat
h2 : idx < (go aig (un (BVUnOp.rotateRight n✝) expr)).val.aig.decls.size
⊢ idx < ?h2.m

case h2.a
w idx w✝ : Nat
op : BVUnOp
expr : BVExpr w✝
ih :
  ∀ (aig : AIG BVBit) (h1 : idx < aig.decls.size) (h2 : idx < (go aig expr).val.aig.decls.size),
    (go aig expr).val.aig.decls[idx] = aig.decls[idx]
aig : AIG BVBit
h1 : idx < aig.decls.size
n✝ : Nat
h2 : idx < (go aig (un (BVUnOp.rotateRight n✝) expr)).val.aig.decls.size
⊢ ?h2.m ≤ (go aig expr).val.aig.decls.size

case h2.m
w idx w✝ : Nat
op : BVUnOp
expr : BVExpr w✝
ih :
  ∀ (aig : AIG BVBit) (h1 : idx < aig.decls.size) (h2 : idx < (go aig expr).val.aig.decls.size),
    (go aig expr).val.aig.decls[idx] = aig.decls[idx]
aig : AIG BVBit
h1 : idx < aig.decls.size
n✝ : Nat
h2 : idx < (go aig (un (BVUnOp.rotateRight n✝) expr)).val.aig.decls.size
⊢ Nat
Tactic:
. exact h1
Proof state after:
case h2.a
w idx w✝ : Nat
op : BVUnOp
expr : BVExpr w✝
ih :
  ∀ (aig : AIG BVBit) (h1 : idx < aig.decls.size) (h2 : idx < (go aig expr).val.aig.decls.size),
    (go aig expr).val.aig.decls[idx] = aig.decls[idx]
aig : AIG BVBit
h1 : idx < aig.decls.size
n✝ : Nat
h2 : idx < (go aig (un (BVUnOp.rotateRight n✝) expr)).val.aig.decls.size
⊢ aig.decls.size ≤ (go aig expr).val.aig.decls.size
Theorem: BVExpr.bitblast.go_decl_eq
Proof state before:
case h2.a
w idx w✝ : Nat
op : BVUnOp
expr : BVExpr w✝
ih :
  ∀ (aig : AIG BVBit) (h1 : idx < aig.decls.size) (h2 : idx < (go aig expr).val.aig.decls.size),
    (go aig expr).val.aig.decls[idx] = aig.decls[idx]
aig : AIG BVBit
h1 : idx < aig.decls.size
n✝ : Nat
h2 : idx < (go aig (un (BVUnOp.rotateRight n✝) expr)).val.aig.decls.size
⊢ aig.decls.size ≤ (go aig expr).val.aig.decls.size
Tactic:
. exact (go aig expr).property
Proof state after:
no goals
Theorem: BVExpr.bitblast.go_decl_eq
Proof state before:
case h2.a
w idx w✝ : Nat
op : BVUnOp
expr : BVExpr w✝
ih :
  ∀ (aig : AIG BVBit) (h1 : idx < aig.decls.size) (h2 : idx < (go aig expr).val.aig.decls.size),
    (go aig expr).val.aig.decls[idx] = aig.decls[idx]
aig : AIG BVBit
h1 : idx < aig.decls.size
n✝ : Nat
h2 : idx < (go aig (un (BVUnOp.rotateRight n✝) expr)).val.aig.decls.size
⊢ idx < ?h2.m
Tactic:
exact h1
Proof state after:
no goals
Theorem: BVExpr.bitblast.go_decl_eq
Proof state before:
case h2.a
w idx w✝ : Nat
op : BVUnOp
expr : BVExpr w✝
ih :
  ∀ (aig : AIG BVBit) (h1 : idx < aig.decls.size) (h2 : idx < (go aig expr).val.aig.decls.size),
    (go aig expr).val.aig.decls[idx] = aig.decls[idx]
aig : AIG BVBit
h1 : idx < aig.decls.size
n✝ : Nat
h2 : idx < (go aig (un (BVUnOp.rotateRight n✝) expr)).val.aig.decls.size
⊢ aig.decls.size ≤ (go aig expr).val.aig.decls.size
Tactic:
exact (go aig expr).property
Proof state after:
no goals
Theorem: BVExpr.bitblast.go_decl_eq
Proof state before:
w idx w✝ : Nat
op : BVUnOp
expr : BVExpr w✝
ih :
  ∀ (aig : AIG BVBit) (h1 : idx < aig.decls.size) (h2 : idx < (go aig expr).val.aig.decls.size),
    (go aig expr).val.aig.decls[idx] = aig.decls[idx]
aig : AIG BVBit
h1 : idx < aig.decls.size
n✝ : Nat
h2 : idx < (go aig (un (BVUnOp.arithShiftRightConst n✝) expr)).val.aig.decls.size
⊢ (go aig (un (BVUnOp.arithShiftRightConst n✝) expr)).val.aig.decls[idx] = aig.decls[idx]
Tactic:
dsimp [go]
Proof state after:
w idx w✝ : Nat
op : BVUnOp
expr : BVExpr w✝
ih :
  ∀ (aig : AIG BVBit) (h1 : idx < aig.decls.size) (h2 : idx < (go aig expr).val.aig.decls.size),
    (go aig expr).val.aig.decls[idx] = aig.decls[idx]
aig : AIG BVBit
h1 : idx < aig.decls.size
n✝ : Nat
h2 : idx < (go aig (un (BVUnOp.arithShiftRightConst n✝) expr)).val.aig.decls.size
⊢ (blastArithShiftRightConst (go aig expr).1.aig { stream := (go aig expr).1.stream, distance := n✝ }).aig.decls[idx] =
    aig.decls[idx]
Theorem: BVExpr.bitblast.go_decl_eq
Proof state before:
w idx w✝ : Nat
op : BVUnOp
expr : BVExpr w✝
ih :
  ∀ (aig : AIG BVBit) (h1 : idx < aig.decls.size) (h2 : idx < (go aig expr).val.aig.decls.size),
    (go aig expr).val.aig.decls[idx] = aig.decls[idx]
aig : AIG BVBit
h1 : idx < aig.decls.size
n✝ : Nat
h2 : idx < (go aig (un (BVUnOp.arithShiftRightConst n✝) expr)).val.aig.decls.size
⊢ (blastArithShiftRightConst (go aig expr).1.aig { stream := (go aig expr).1.stream, distance := n✝ }).aig.decls[idx] =
    aig.decls[idx]
Tactic:
rw [AIG.LawfulStreamOperator.decl_eq (f := blastArithShiftRightConst)]
Proof state after:
w idx w✝ : Nat
op : BVUnOp
expr : BVExpr w✝
ih :
  ∀ (aig : AIG BVBit) (h1 : idx < aig.decls.size) (h2 : idx < (go aig expr).val.aig.decls.size),
    (go aig expr).val.aig.decls[idx] = aig.decls[idx]
aig : AIG BVBit
h1 : idx < aig.decls.size
n✝ : Nat
h2 : idx < (go aig (un (BVUnOp.arithShiftRightConst n✝) expr)).val.aig.decls.size
⊢ (go aig expr).1.aig.decls[idx] = aig.decls[idx]

case h1
w idx w✝ : Nat
op : BVUnOp
expr : BVExpr w✝
ih :
  ∀ (aig : AIG BVBit) (h1 : idx < aig.decls.size) (h2 : idx < (go aig expr).val.aig.decls.size),
    (go aig expr).val.aig.decls[idx] = aig.decls[idx]
aig : AIG BVBit
h1 : idx < aig.decls.size
n✝ : Nat
h2 : idx < (go aig (un (BVUnOp.arithShiftRightConst n✝) expr)).val.aig.decls.size
⊢ idx < (go aig expr).1.aig.decls.size
Theorem: BVExpr.bitblast.go_decl_eq
Proof state before:
w idx w✝ : Nat
op : BVUnOp
expr : BVExpr w✝
ih :
  ∀ (aig : AIG BVBit) (h1 : idx < aig.decls.size) (h2 : idx < (go aig expr).val.aig.decls.size),
    (go aig expr).val.aig.decls[idx] = aig.decls[idx]
aig : AIG BVBit
h1 : idx < aig.decls.size
n✝ : Nat
h2 : idx < (go aig (un (BVUnOp.arithShiftRightConst n✝) expr)).val.aig.decls.size
⊢ (go aig expr).1.aig.decls[idx] = aig.decls[idx]

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

case h2.a
w idx w✝ : Nat
op : BVUnOp
expr : BVExpr w✝
ih :
  ∀ (aig : AIG BVBit) (h1 : idx < aig.decls.size) (h2 : idx < (go aig expr).val.aig.decls.size),
    (go aig expr).val.aig.decls[idx] = aig.decls[idx]
aig : AIG BVBit
h1 : idx < aig.decls.size
n✝ : Nat
h2 : idx < (go aig (un (BVUnOp.arithShiftRightConst n✝) expr)).val.aig.decls.size
⊢ ?h2.m ≤ (go aig expr).val.aig.decls.size

case h2.m
w idx w✝ : Nat
op : BVUnOp
expr : BVExpr w✝
ih :
  ∀ (aig : AIG BVBit) (h1 : idx < aig.decls.size) (h2 : idx < (go aig expr).val.aig.decls.size),
    (go aig expr).val.aig.decls[idx] = aig.decls[idx]
aig : AIG BVBit
h1 : idx < aig.decls.size
n✝ : Nat
h2 : idx < (go aig (un (BVUnOp.arithShiftRightConst n✝) expr)).val.aig.decls.size
⊢ Nat
Theorem: BVExpr.bitblast.go_decl_eq
Proof state before:
case h2.a
w idx w✝ : Nat
op : BVUnOp
expr : BVExpr w✝
ih :
  ∀ (aig : AIG BVBit) (h1 : idx < aig.decls.size) (h2 : idx < (go aig expr).val.aig.decls.size),
    (go aig expr).val.aig.decls[idx] = aig.decls[idx]
aig : AIG BVBit
h1 : idx < aig.decls.size
n✝ : Nat
h2 : idx < (go aig (un (BVUnOp.arithShiftRightConst n✝) expr)).val.aig.decls.size
⊢ idx < ?h2.m

case h2.a
w idx w✝ : Nat
op : BVUnOp
expr : BVExpr w✝
ih :
  ∀ (aig : AIG BVBit) (h1 : idx < aig.decls.size) (h2 : idx < (go aig expr).val.aig.decls.size),
    (go aig expr).val.aig.decls[idx] = aig.decls[idx]
aig : AIG BVBit
h1 : idx < aig.decls.size
n✝ : Nat
h2 : idx < (go aig (un (BVUnOp.arithShiftRightConst n✝) expr)).val.aig.decls.size
⊢ ?h2.m ≤ (go aig expr).val.aig.decls.size

case h2.m
w idx w✝ : Nat
op : BVUnOp
expr : BVExpr w✝
ih :
  ∀ (aig : AIG BVBit) (h1 : idx < aig.decls.size) (h2 : idx < (go aig expr).val.aig.decls.size),
    (go aig expr).val.aig.decls[idx] = aig.decls[idx]
aig : AIG BVBit
h1 : idx < aig.decls.size
n✝ : Nat
h2 : idx < (go aig (un (BVUnOp.arithShiftRightConst n✝) expr)).val.aig.decls.size
⊢ Nat
Tactic:
. exact h1
Proof state after:
case h2.a
w idx w✝ : Nat
op : BVUnOp
expr : BVExpr w✝
ih :
  ∀ (aig : AIG BVBit) (h1 : idx < aig.decls.size) (h2 : idx < (go aig expr).val.aig.decls.size),
    (go aig expr).val.aig.decls[idx] = aig.decls[idx]
aig : AIG BVBit
h1 : idx < aig.decls.size
n✝ : Nat
h2 : idx < (go aig (un (BVUnOp.arithShiftRightConst n✝) expr)).val.aig.decls.size
⊢ aig.decls.size ≤ (go aig expr).val.aig.decls.size
Theorem: BVExpr.bitblast.go_decl_eq
Proof state before:
case h2.a
w idx w✝ : Nat
op : BVUnOp
expr : BVExpr w✝
ih :
  ∀ (aig : AIG BVBit) (h1 : idx < aig.decls.size) (h2 : idx < (go aig expr).val.aig.decls.size),
    (go aig expr).val.aig.decls[idx] = aig.decls[idx]
aig : AIG BVBit
h1 : idx < aig.decls.size
n✝ : Nat
h2 : idx < (go aig (un (BVUnOp.arithShiftRightConst n✝) expr)).val.aig.decls.size
⊢ aig.decls.size ≤ (go aig expr).val.aig.decls.size
Tactic:
. exact (go aig expr).property
Proof state after:
no goals
Theorem: BVExpr.bitblast.go_decl_eq
Proof state before:
case h2.a
w idx w✝ : Nat
op : BVUnOp
expr : BVExpr w✝
ih :
  ∀ (aig : AIG BVBit) (h1 : idx < aig.decls.size) (h2 : idx < (go aig expr).val.aig.decls.size),
    (go aig expr).val.aig.decls[idx] = aig.decls[idx]
aig : AIG BVBit
h1 : idx < aig.decls.size
n✝ : Nat
h2 : idx < (go aig (un (BVUnOp.arithShiftRightConst n✝) expr)).val.aig.decls.size
⊢ idx < ?h2.m
Tactic:
exact h1
Proof state after:
no goals
Theorem: BVExpr.bitblast.go_decl_eq
Proof state before:
case h2.a
w idx w✝ : Nat
op : BVUnOp
expr : BVExpr w✝
ih :
  ∀ (aig : AIG BVBit) (h1 : idx < aig.decls.size) (h2 : idx < (go aig expr).val.aig.decls.size),
    (go aig expr).val.aig.decls[idx] = aig.decls[idx]
aig : AIG BVBit
h1 : idx < aig.decls.size
n✝ : Nat
h2 : idx < (go aig (un (BVUnOp.arithShiftRightConst n✝) expr)).val.aig.decls.size
⊢ aig.decls.size ≤ (go aig expr).val.aig.decls.size
Tactic:
exact (go aig expr).property
Proof state after:
no goals
Theorem: BVExpr.bitblast.go_decl_eq
Proof state before:
case zeroExtend
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
⊢ (go aig (zeroExtend w inner)).val.aig.decls[idx] = aig.decls[idx]
Tactic:
dsimp [go]
Proof state after:
case zeroExtend
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
⊢ (blastZeroExtend (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 zeroExtend
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
⊢ (blastZeroExtend (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 := blastZeroExtend)]
Proof state after:
case zeroExtend
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
⊢ (go aig inner).1.aig.decls[idx] = aig.decls[idx]

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

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

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
⊢ ?zeroExtend.h2.m ≤ (go aig inner).val.aig.decls.size

case zeroExtend.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 (zeroExtend w inner)).val.aig.decls.size
⊢ Nat
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
⊢ idx < ?zeroExtend.h2.m

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
⊢ ?zeroExtend.h2.m ≤ (go aig inner).val.aig.decls.size

case zeroExtend.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 (zeroExtend w inner)).val.aig.decls.size
⊢ Nat
Tactic:
. exact h1
Proof state after:
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
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 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
⊢ idx < ?zeroExtend.h2.m
Tactic:
exact h1
Proof state after:
no goals