internlm/Lean-Github huggingface dataset:
Theorem: BVExpr.bitblast.go_denote_eq_eval_getLsb
Proof state before:
case signExtend.inl
w : Nat
assign : Assignment
originalWidth v : Nat
inner : BVExpr originalWidth
ih :
  ∀ (aig : AIG BVBit) (idx : Nat) (hidx : idx < originalWidth),
    ⟦{ aig := (go aig inner).val.aig, ref := (go aig inner).val.stream.getRef idx hidx }, assign.toAIGAssignment⟧ =
      (eval assign inner).getLsb idx
aig : AIG BVBit
idx : Nat
hidx : idx < v
res : RefStreamEntry BVBit v
hgo : blastZeroExtend (go aig inner).1.aig { w := originalWidth, stream := (go aig inner).1.stream } = res
this : 0 ≤ originalWidth
heq : 0 = originalWidth
⊢ ⟦{ aig := (blastZeroExtend (go aig inner).1.aig { w := originalWidth, stream := (go aig inner).1.stream }).aig,
        ref :=
          (blastZeroExtend (go aig inner).1.aig { w := originalWidth, stream := (go aig inner).1.stream }).stream.getRef
            idx hidx },
      assign.toAIGAssignment⟧ =
    (BitVec.zeroExtend v (eval assign inner)).getLsb idx
Tactic:
simp only [blastZeroExtend_eq_eval_getLsb, ih, dite_eq_ite, Bool.if_false_right,
  BitVec.getLsb_zeroExtend, hidx, decide_True, Bool.true_and, Bool.and_iff_right_iff_imp,
  decide_eq_true_eq]
Proof state after:
case signExtend.inl
w : Nat
assign : Assignment
originalWidth v : Nat
inner : BVExpr originalWidth
ih :
  ∀ (aig : AIG BVBit) (idx : Nat) (hidx : idx < originalWidth),
    ⟦{ aig := (go aig inner).val.aig, ref := (go aig inner).val.stream.getRef idx hidx }, assign.toAIGAssignment⟧ =
      (eval assign inner).getLsb idx
aig : AIG BVBit
idx : Nat
hidx : idx < v
res : RefStreamEntry BVBit v
hgo : blastZeroExtend (go aig inner).1.aig { w := originalWidth, stream := (go aig inner).1.stream } = res
this : 0 ≤ originalWidth
heq : 0 = originalWidth
⊢ (eval assign inner).getLsb idx = true → idx < originalWidth
Theorem: BVExpr.bitblast.go_denote_eq_eval_getLsb
Proof state before:
case signExtend.inl
w : Nat
assign : Assignment
originalWidth v : Nat
inner : BVExpr originalWidth
ih :
  ∀ (aig : AIG BVBit) (idx : Nat) (hidx : idx < originalWidth),
    ⟦{ aig := (go aig inner).val.aig, ref := (go aig inner).val.stream.getRef idx hidx }, assign.toAIGAssignment⟧ =
      (eval assign inner).getLsb idx
aig : AIG BVBit
idx : Nat
hidx : idx < v
res : RefStreamEntry BVBit v
hgo : blastZeroExtend (go aig inner).1.aig { w := originalWidth, stream := (go aig inner).1.stream } = res
this : 0 ≤ originalWidth
heq : 0 = originalWidth
⊢ (eval assign inner).getLsb idx = true → idx < originalWidth
Tactic:
apply BitVec.lt_of_getLsb
Proof state after:
no goals
Theorem: BVExpr.bitblast.go_denote_eq_eval_getLsb
Proof state before:
case signExtend.inl
w : Nat
assign : Assignment
originalWidth v : Nat
inner : BVExpr originalWidth
ih :
  ∀ (aig : AIG BVBit) (idx : Nat) (hidx : idx < originalWidth),
    ⟦{ aig := (go aig inner).val.aig, ref := (go aig inner).val.stream.getRef idx hidx }, assign.toAIGAssignment⟧ =
      (eval assign inner).getLsb idx
aig : AIG BVBit
idx : Nat
hidx : idx < v
res : RefStreamEntry BVBit v
hgo : blastZeroExtend (go aig inner).1.aig { w := originalWidth, stream := (go aig inner).1.stream } = res
this : 0 ≤ originalWidth
heq : 0 = originalWidth
⊢ (eval assign inner).msb = false
Tactic:
subst heq
Proof state after:
case signExtend.inl
w : Nat
assign : Assignment
v : Nat
aig : AIG BVBit
idx : Nat
hidx : idx < v
res : RefStreamEntry BVBit v
inner : BVExpr 0
ih :
  ∀ (aig : AIG BVBit) (idx : Nat) (hidx : idx < 0),
    ⟦{ aig := (go aig inner).val.aig, ref := (go aig inner).val.stream.getRef idx hidx }, assign.toAIGAssignment⟧ =
      (eval assign inner).getLsb idx
hgo : blastZeroExtend (go aig inner).1.aig { w := 0, stream := (go aig inner).1.stream } = res
this : 0 ≤ 0
⊢ (eval assign inner).msb = false
Theorem: BVExpr.bitblast.go_denote_eq_eval_getLsb
Proof state before:
case signExtend.inl
w : Nat
assign : Assignment
v : Nat
aig : AIG BVBit
idx : Nat
hidx : idx < v
res : RefStreamEntry BVBit v
inner : BVExpr 0
ih :
  ∀ (aig : AIG BVBit) (idx : Nat) (hidx : idx < 0),
    ⟦{ aig := (go aig inner).val.aig, ref := (go aig inner).val.stream.getRef idx hidx }, assign.toAIGAssignment⟧ =
      (eval assign inner).getLsb idx
hgo : blastZeroExtend (go aig inner).1.aig { w := 0, stream := (go aig inner).1.stream } = res
this : 0 ≤ 0
⊢ (eval assign inner).msb = false
Tactic:
rw [BitVec.msb_zero_length]
Proof state after:
no goals
Theorem: BVExpr.bitblast.go_denote_eq_eval_getLsb
Proof state before:
case signExtend.inl.htarget
w : Nat
assign : Assignment
originalWidth v : Nat
inner : BVExpr originalWidth
ih :
  ∀ (aig : AIG BVBit) (idx : Nat) (hidx : idx < originalWidth),
    ⟦{ aig := (go aig inner).val.aig, ref := (go aig inner).val.stream.getRef idx hidx }, assign.toAIGAssignment⟧ =
      (eval assign inner).getLsb idx
aig : AIG BVBit
idx : Nat
hidx : idx < v
res : RefStreamEntry BVBit v
hgo : blastSignExtend (go aig inner).1.aig { w := originalWidth, stream := (go aig inner).1.stream } = res
this : 0 ≤ originalWidth
heq : 0 = originalWidth
⊢ { w := originalWidth, stream := (go aig inner).1.stream }.w = 0
Tactic:
simp [heq]
Proof state after:
no goals
Theorem: BVExpr.bitblast.go_denote_eq_eval_getLsb
Proof state before:
case signExtend.inr
w : Nat
assign : Assignment
originalWidth v : Nat
inner : BVExpr originalWidth
ih :
  ∀ (aig : AIG BVBit) (idx : Nat) (hidx : idx < originalWidth),
    ⟦{ aig := (go aig inner).val.aig, ref := (go aig inner).val.stream.getRef idx hidx }, assign.toAIGAssignment⟧ =
      (eval assign inner).getLsb idx
aig : AIG BVBit
idx : Nat
hidx : idx < v
res : RefStreamEntry BVBit v
hgo : blastSignExtend (go aig inner).1.aig { w := originalWidth, stream := (go aig inner).1.stream } = res
this : 0 ≤ originalWidth
hlt : 0 < originalWidth
⊢ ⟦{ aig := res.aig, ref := res.stream.getRef idx hidx }, assign.toAIGAssignment⟧ =
    (eval assign (signExtend v inner)).getLsb idx
Tactic:
rw [← hgo]
Proof state after:
case signExtend.inr
w : Nat
assign : Assignment
originalWidth v : Nat
inner : BVExpr originalWidth
ih :
  ∀ (aig : AIG BVBit) (idx : Nat) (hidx : idx < originalWidth),
    ⟦{ aig := (go aig inner).val.aig, ref := (go aig inner).val.stream.getRef idx hidx }, assign.toAIGAssignment⟧ =
      (eval assign inner).getLsb idx
aig : AIG BVBit
idx : Nat
hidx : idx < v
res : RefStreamEntry BVBit v
hgo : blastSignExtend (go aig inner).1.aig { w := originalWidth, stream := (go aig inner).1.stream } = res
this : 0 ≤ originalWidth
hlt : 0 < originalWidth
⊢ ⟦{ aig := (blastSignExtend (go aig inner).1.aig { w := originalWidth, stream := (go aig inner).1.stream }).aig,
        ref :=
          (blastSignExtend (go aig inner).1.aig { w := originalWidth, stream := (go aig inner).1.stream }).stream.getRef
            idx hidx },
      assign.toAIGAssignment⟧ =
    (eval assign (signExtend v inner)).getLsb idx
Theorem: BVExpr.bitblast.go_denote_eq_eval_getLsb
Proof state before:
case signExtend.inr
w : Nat
assign : Assignment
originalWidth v : Nat
inner : BVExpr originalWidth
ih :
  ∀ (aig : AIG BVBit) (idx : Nat) (hidx : idx < originalWidth),
    ⟦{ aig := (go aig inner).val.aig, ref := (go aig inner).val.stream.getRef idx hidx }, assign.toAIGAssignment⟧ =
      (eval assign inner).getLsb idx
aig : AIG BVBit
idx : Nat
hidx : idx < v
res : RefStreamEntry BVBit v
hgo : blastSignExtend (go aig inner).1.aig { w := originalWidth, stream := (go aig inner).1.stream } = res
this : 0 ≤ originalWidth
hlt : 0 < originalWidth
⊢ ⟦{ aig := (blastSignExtend (go aig inner).1.aig { w := originalWidth, stream := (go aig inner).1.stream }).aig,
        ref :=
          (blastSignExtend (go aig inner).1.aig { w := originalWidth, stream := (go aig inner).1.stream }).stream.getRef
            idx hidx },
      assign.toAIGAssignment⟧ =
    (eval assign (signExtend v inner)).getLsb idx
Tactic:
rw [blastSignExtend_eq_eval_getLsb]
Proof state after:
case signExtend.inr
w : Nat
assign : Assignment
originalWidth v : Nat
inner : BVExpr originalWidth
ih :
  ∀ (aig : AIG BVBit) (idx : Nat) (hidx : idx < originalWidth),
    ⟦{ aig := (go aig inner).val.aig, ref := (go aig inner).val.stream.getRef idx hidx }, assign.toAIGAssignment⟧ =
      (eval assign inner).getLsb idx
aig : AIG BVBit
idx : Nat
hidx : idx < v
res : RefStreamEntry BVBit v
hgo : blastSignExtend (go aig inner).1.aig { w := originalWidth, stream := (go aig inner).1.stream } = res
this : 0 ≤ originalWidth
hlt : 0 < originalWidth
⊢ (if hidx : idx < { w := originalWidth, stream := (go aig inner).1.stream }.w then
      ⟦{ aig := (go aig inner).1.aig,
          ref := { w := originalWidth, stream := (go aig inner).1.stream }.stream.getRef idx hidx },
        assign.toAIGAssignment⟧
    else
      ⟦{ aig := (go aig inner).1.aig,
          ref :=
            { w := originalWidth, stream := (go aig inner).1.stream }.stream.getRef
              ({ w := originalWidth, stream := (go aig inner).1.stream }.w - 1) ⋯ },
        assign.toAIGAssignment⟧) =
    (eval assign (signExtend v inner)).getLsb idx

case signExtend.inr.htarget
w : Nat
assign : Assignment
originalWidth v : Nat
inner : BVExpr originalWidth
ih :
  ∀ (aig : AIG BVBit) (idx : Nat) (hidx : idx < originalWidth),
    ⟦{ aig := (go aig inner).val.aig, ref := (go aig inner).val.stream.getRef idx hidx }, assign.toAIGAssignment⟧ =
      (eval assign inner).getLsb idx
aig : AIG BVBit
idx : Nat
hidx : idx < v
res : RefStreamEntry BVBit v
hgo : blastSignExtend (go aig inner).1.aig { w := originalWidth, stream := (go aig inner).1.stream } = res
this : 0 ≤ originalWidth
hlt : 0 < originalWidth
⊢ 0 < { w := originalWidth, stream := (go aig inner).1.stream }.w
Theorem: BVExpr.bitblast.go_denote_eq_eval_getLsb
Proof state before:
case signExtend.inr
w : Nat
assign : Assignment
originalWidth v : Nat
inner : BVExpr originalWidth
ih :
  ∀ (aig : AIG BVBit) (idx : Nat) (hidx : idx < originalWidth),
    ⟦{ aig := (go aig inner).val.aig, ref := (go aig inner).val.stream.getRef idx hidx }, assign.toAIGAssignment⟧ =
      (eval assign inner).getLsb idx
aig : AIG BVBit
idx : Nat
hidx : idx < v
res : RefStreamEntry BVBit v
hgo : blastSignExtend (go aig inner).1.aig { w := originalWidth, stream := (go aig inner).1.stream } = res
this : 0 ≤ originalWidth
hlt : 0 < originalWidth
⊢ (if h : idx < originalWidth then
      ⟦{ aig := (go aig inner).1.aig, ref := (go aig inner).1.stream.getRef idx ⋯ }, assign.toAIGAssignment⟧
    else
      ⟦{ aig := (go aig inner).1.aig, ref := (go aig inner).1.stream.getRef (originalWidth - 1) ⋯ },
        assign.toAIGAssignment⟧) =
    (decide (idx < v) && if idx < originalWidth then (eval assign inner).getLsb idx else (eval assign inner).msb)

case signExtend.inr.htarget
w : Nat
assign : Assignment
originalWidth v : Nat
inner : BVExpr originalWidth
ih :
  ∀ (aig : AIG BVBit) (idx : Nat) (hidx : idx < originalWidth),
    ⟦{ aig := (go aig inner).val.aig, ref := (go aig inner).val.stream.getRef idx hidx }, assign.toAIGAssignment⟧ =
      (eval assign inner).getLsb idx
aig : AIG BVBit
idx : Nat
hidx : idx < v
res : RefStreamEntry BVBit v
hgo : blastSignExtend (go aig inner).1.aig { w := originalWidth, stream := (go aig inner).1.stream } = res
this : 0 ≤ originalWidth
hlt : 0 < originalWidth
⊢ 0 < { w := originalWidth, stream := (go aig inner).1.stream }.w

case signExtend.inr.htarget
w : Nat
assign : Assignment
originalWidth v : Nat
inner : BVExpr originalWidth
ih :
  ∀ (aig : AIG BVBit) (idx : Nat) (hidx : idx < originalWidth),
    ⟦{ aig := (go aig inner).val.aig, ref := (go aig inner).val.stream.getRef idx hidx }, assign.toAIGAssignment⟧ =
      (eval assign inner).getLsb idx
aig : AIG BVBit
idx : Nat
hidx : idx < v
res : RefStreamEntry BVBit v
hgo : blastSignExtend (go aig inner).1.aig { w := originalWidth, stream := (go aig inner).1.stream } = res
this : 0 ≤ originalWidth
hlt : 0 < originalWidth
⊢ 0 < { w := originalWidth, stream := (go aig inner).1.stream }.w
Tactic:
. simp only [hidx, decide_True, Bool.true_and]
  split
  . rw [ih]
  . rw [BitVec.msb_eq_getLsb_last]
    rw [ih]
    simp [hlt]
Proof state after:
no goals
Theorem: BVExpr.bitblast.go_denote_eq_eval_getLsb
Proof state before:
case signExtend.inr
w : Nat
assign : Assignment
originalWidth v : Nat
inner : BVExpr originalWidth
ih :
  ∀ (aig : AIG BVBit) (idx : Nat) (hidx : idx < originalWidth),
    ⟦{ aig := (go aig inner).val.aig, ref := (go aig inner).val.stream.getRef idx hidx }, assign.toAIGAssignment⟧ =
      (eval assign inner).getLsb idx
aig : AIG BVBit
idx : Nat
hidx : idx < v
res : RefStreamEntry BVBit v
hgo : blastSignExtend (go aig inner).1.aig { w := originalWidth, stream := (go aig inner).1.stream } = res
this : 0 ≤ originalWidth
hlt : 0 < originalWidth
⊢ (if h : idx < originalWidth then
      ⟦{ aig := (go aig inner).1.aig, ref := (go aig inner).1.stream.getRef idx ⋯ }, assign.toAIGAssignment⟧
    else
      ⟦{ aig := (go aig inner).1.aig, ref := (go aig inner).1.stream.getRef (originalWidth - 1) ⋯ },
        assign.toAIGAssignment⟧) =
    (decide (idx < v) && if idx < originalWidth then (eval assign inner).getLsb idx else (eval assign inner).msb)
Tactic:
simp only [hidx, decide_True, Bool.true_and]
Proof state after:
case signExtend.inr
w : Nat
assign : Assignment
originalWidth v : Nat
inner : BVExpr originalWidth
ih :
  ∀ (aig : AIG BVBit) (idx : Nat) (hidx : idx < originalWidth),
    ⟦{ aig := (go aig inner).val.aig, ref := (go aig inner).val.stream.getRef idx hidx }, assign.toAIGAssignment⟧ =
      (eval assign inner).getLsb idx
aig : AIG BVBit
idx : Nat
hidx : idx < v
res : RefStreamEntry BVBit v
hgo : blastSignExtend (go aig inner).1.aig { w := originalWidth, stream := (go aig inner).1.stream } = res
this : 0 ≤ originalWidth
hlt : 0 < originalWidth
⊢ (if h : idx < originalWidth then
      ⟦{ aig := (go aig inner).1.aig, ref := (go aig inner).1.stream.getRef idx ⋯ }, assign.toAIGAssignment⟧
    else
      ⟦{ aig := (go aig inner).1.aig, ref := (go aig inner).1.stream.getRef (originalWidth - 1) ⋯ },
        assign.toAIGAssignment⟧) =
    if idx < originalWidth then (eval assign inner).getLsb idx else (eval assign inner).msb
Theorem: BVExpr.bitblast.go_denote_eq_eval_getLsb
Proof state before:
case signExtend.inr
w : Nat
assign : Assignment
originalWidth v : Nat
inner : BVExpr originalWidth
ih :
  ∀ (aig : AIG BVBit) (idx : Nat) (hidx : idx < originalWidth),
    ⟦{ aig := (go aig inner).val.aig, ref := (go aig inner).val.stream.getRef idx hidx }, assign.toAIGAssignment⟧ =
      (eval assign inner).getLsb idx
aig : AIG BVBit
idx : Nat
hidx : idx < v
res : RefStreamEntry BVBit v
hgo : blastSignExtend (go aig inner).1.aig { w := originalWidth, stream := (go aig inner).1.stream } = res
this : 0 ≤ originalWidth
hlt : 0 < originalWidth
⊢ (if h : idx < originalWidth then
      ⟦{ aig := (go aig inner).1.aig, ref := (go aig inner).1.stream.getRef idx ⋯ }, assign.toAIGAssignment⟧
    else
      ⟦{ aig := (go aig inner).1.aig, ref := (go aig inner).1.stream.getRef (originalWidth - 1) ⋯ },
        assign.toAIGAssignment⟧) =
    if idx < originalWidth then (eval assign inner).getLsb idx else (eval assign inner).msb
Tactic:
split
Proof state after:
case signExtend.inr.isTrue
w : Nat
assign : Assignment
originalWidth v : Nat
inner : BVExpr originalWidth
ih :
  ∀ (aig : AIG BVBit) (idx : Nat) (hidx : idx < originalWidth),
    ⟦{ aig := (go aig inner).val.aig, ref := (go aig inner).val.stream.getRef idx hidx }, assign.toAIGAssignment⟧ =
      (eval assign inner).getLsb idx
aig : AIG BVBit
idx : Nat
hidx : idx < v
res : RefStreamEntry BVBit v
hgo : blastSignExtend (go aig inner).1.aig { w := originalWidth, stream := (go aig inner).1.stream } = res
this : 0 ≤ originalWidth
hlt : 0 < originalWidth
h✝ : idx < originalWidth
⊢ ⟦{ aig := (go aig inner).1.aig, ref := (go aig inner).1.stream.getRef idx ⋯ }, assign.toAIGAssignment⟧ =
    (eval assign inner).getLsb idx

case signExtend.inr.isFalse
w : Nat
assign : Assignment
originalWidth v : Nat
inner : BVExpr originalWidth
ih :
  ∀ (aig : AIG BVBit) (idx : Nat) (hidx : idx < originalWidth),
    ⟦{ aig := (go aig inner).val.aig, ref := (go aig inner).val.stream.getRef idx hidx }, assign.toAIGAssignment⟧ =
      (eval assign inner).getLsb idx
aig : AIG BVBit
idx : Nat
hidx : idx < v
res : RefStreamEntry BVBit v
hgo : blastSignExtend (go aig inner).1.aig { w := originalWidth, stream := (go aig inner).1.stream } = res
this : 0 ≤ originalWidth
hlt : 0 < originalWidth
h✝ : ¬idx < originalWidth
⊢ ⟦{ aig := (go aig inner).1.aig, ref := (go aig inner).1.stream.getRef (originalWidth - 1) ⋯ },
      assign.toAIGAssignment⟧ =
    (eval assign inner).msb
Theorem: BVExpr.bitblast.go_denote_eq_eval_getLsb
Proof state before:
case signExtend.inr.isTrue
w : Nat
assign : Assignment
originalWidth v : Nat
inner : BVExpr originalWidth
ih :
  ∀ (aig : AIG BVBit) (idx : Nat) (hidx : idx < originalWidth),
    ⟦{ aig := (go aig inner).val.aig, ref := (go aig inner).val.stream.getRef idx hidx }, assign.toAIGAssignment⟧ =
      (eval assign inner).getLsb idx
aig : AIG BVBit
idx : Nat
hidx : idx < v
res : RefStreamEntry BVBit v
hgo : blastSignExtend (go aig inner).1.aig { w := originalWidth, stream := (go aig inner).1.stream } = res
this : 0 ≤ originalWidth
hlt : 0 < originalWidth
h✝ : idx < originalWidth
⊢ ⟦{ aig := (go aig inner).1.aig, ref := (go aig inner).1.stream.getRef idx ⋯ }, assign.toAIGAssignment⟧ =
    (eval assign inner).getLsb idx

case signExtend.inr.isFalse
w : Nat
assign : Assignment
originalWidth v : Nat
inner : BVExpr originalWidth
ih :
  ∀ (aig : AIG BVBit) (idx : Nat) (hidx : idx < originalWidth),
    ⟦{ aig := (go aig inner).val.aig, ref := (go aig inner).val.stream.getRef idx hidx }, assign.toAIGAssignment⟧ =
      (eval assign inner).getLsb idx
aig : AIG BVBit
idx : Nat
hidx : idx < v
res : RefStreamEntry BVBit v
hgo : blastSignExtend (go aig inner).1.aig { w := originalWidth, stream := (go aig inner).1.stream } = res
this : 0 ≤ originalWidth
hlt : 0 < originalWidth
h✝ : ¬idx < originalWidth
⊢ ⟦{ aig := (go aig inner).1.aig, ref := (go aig inner).1.stream.getRef (originalWidth - 1) ⋯ },
      assign.toAIGAssignment⟧ =
    (eval assign inner).msb
Tactic:
. rw [ih]
Proof state after:
case signExtend.inr.isFalse
w : Nat
assign : Assignment
originalWidth v : Nat
inner : BVExpr originalWidth
ih :
  ∀ (aig : AIG BVBit) (idx : Nat) (hidx : idx < originalWidth),
    ⟦{ aig := (go aig inner).val.aig, ref := (go aig inner).val.stream.getRef idx hidx }, assign.toAIGAssignment⟧ =
      (eval assign inner).getLsb idx
aig : AIG BVBit
idx : Nat
hidx : idx < v
res : RefStreamEntry BVBit v
hgo : blastSignExtend (go aig inner).1.aig { w := originalWidth, stream := (go aig inner).1.stream } = res
this : 0 ≤ originalWidth
hlt : 0 < originalWidth
h✝ : ¬idx < originalWidth
⊢ ⟦{ aig := (go aig inner).1.aig, ref := (go aig inner).1.stream.getRef (originalWidth - 1) ⋯ },
      assign.toAIGAssignment⟧ =
    (eval assign inner).msb
Theorem: BVExpr.bitblast.go_denote_eq_eval_getLsb
Proof state before:
case signExtend.inr.isFalse
w : Nat
assign : Assignment
originalWidth v : Nat
inner : BVExpr originalWidth
ih :
  ∀ (aig : AIG BVBit) (idx : Nat) (hidx : idx < originalWidth),
    ⟦{ aig := (go aig inner).val.aig, ref := (go aig inner).val.stream.getRef idx hidx }, assign.toAIGAssignment⟧ =
      (eval assign inner).getLsb idx
aig : AIG BVBit
idx : Nat
hidx : idx < v
res : RefStreamEntry BVBit v
hgo : blastSignExtend (go aig inner).1.aig { w := originalWidth, stream := (go aig inner).1.stream } = res
this : 0 ≤ originalWidth
hlt : 0 < originalWidth
h✝ : ¬idx < originalWidth
⊢ ⟦{ aig := (go aig inner).1.aig, ref := (go aig inner).1.stream.getRef (originalWidth - 1) ⋯ },
      assign.toAIGAssignment⟧ =
    (eval assign inner).msb
Tactic:
. rw [BitVec.msb_eq_getLsb_last]
  rw [ih]
  simp [hlt]
Proof state after:
no goals
Theorem: BVExpr.bitblast.go_denote_eq_eval_getLsb
Proof state before:
case signExtend.inr.isTrue
w : Nat
assign : Assignment
originalWidth v : Nat
inner : BVExpr originalWidth
ih :
  ∀ (aig : AIG BVBit) (idx : Nat) (hidx : idx < originalWidth),
    ⟦{ aig := (go aig inner).val.aig, ref := (go aig inner).val.stream.getRef idx hidx }, assign.toAIGAssignment⟧ =
      (eval assign inner).getLsb idx
aig : AIG BVBit
idx : Nat
hidx : idx < v
res : RefStreamEntry BVBit v
hgo : blastSignExtend (go aig inner).1.aig { w := originalWidth, stream := (go aig inner).1.stream } = res
this : 0 ≤ originalWidth
hlt : 0 < originalWidth
h✝ : idx < originalWidth
⊢ ⟦{ aig := (go aig inner).1.aig, ref := (go aig inner).1.stream.getRef idx ⋯ }, assign.toAIGAssignment⟧ =
    (eval assign inner).getLsb idx
Tactic:
rw [ih]
Proof state after:
no goals
Theorem: BVExpr.bitblast.go_denote_eq_eval_getLsb
Proof state before:
case signExtend.inr.isFalse
w : Nat
assign : Assignment
originalWidth v : Nat
inner : BVExpr originalWidth
ih :
  ∀ (aig : AIG BVBit) (idx : Nat) (hidx : idx < originalWidth),
    ⟦{ aig := (go aig inner).val.aig, ref := (go aig inner).val.stream.getRef idx hidx }, assign.toAIGAssignment⟧ =
      (eval assign inner).getLsb idx
aig : AIG BVBit
idx : Nat
hidx : idx < v
res : RefStreamEntry BVBit v
hgo : blastSignExtend (go aig inner).1.aig { w := originalWidth, stream := (go aig inner).1.stream } = res
this : 0 ≤ originalWidth
hlt : 0 < originalWidth
h✝ : ¬idx < originalWidth
⊢ ⟦{ aig := (go aig inner).1.aig, ref := (go aig inner).1.stream.getRef (originalWidth - 1) ⋯ },
      assign.toAIGAssignment⟧ =
    (eval assign inner).msb
Tactic:
rw [BitVec.msb_eq_getLsb_last]
Proof state after:
case signExtend.inr.isFalse
w : Nat
assign : Assignment
originalWidth v : Nat
inner : BVExpr originalWidth
ih :
  ∀ (aig : AIG BVBit) (idx : Nat) (hidx : idx < originalWidth),
    ⟦{ aig := (go aig inner).val.aig, ref := (go aig inner).val.stream.getRef idx hidx }, assign.toAIGAssignment⟧ =
      (eval assign inner).getLsb idx
aig : AIG BVBit
idx : Nat
hidx : idx < v
res : RefStreamEntry BVBit v
hgo : blastSignExtend (go aig inner).1.aig { w := originalWidth, stream := (go aig inner).1.stream } = res
this : 0 ≤ originalWidth
hlt : 0 < originalWidth
h✝ : ¬idx < originalWidth
⊢ ⟦{ aig := (go aig inner).1.aig, ref := (go aig inner).1.stream.getRef (originalWidth - 1) ⋯ },
      assign.toAIGAssignment⟧ =
    (eval assign inner).getLsb (originalWidth - 1)

case signExtend.inr.htarget
w : Nat
assign : Assignment
originalWidth v : Nat
inner : BVExpr originalWidth
ih :
  ∀ (aig : AIG BVBit) (idx : Nat) (hidx : idx < originalWidth),
    ⟦{ aig := (go aig inner).val.aig, ref := (go aig inner).val.stream.getRef idx hidx }, assign.toAIGAssignment⟧ =
      (eval assign inner).getLsb idx
aig : AIG BVBit
idx : Nat
hidx : idx < v
res : RefStreamEntry BVBit v
hgo : blastSignExtend (go aig inner).1.aig { w := originalWidth, stream := (go aig inner).1.stream } = res
this : 0 ≤ originalWidth
hlt : 0 < originalWidth
⊢ 0 < { w := originalWidth, stream := (go aig inner).1.stream }.w