internlm/Lean-Github huggingface dataset:
Theorem: BVExpr.bitblast.go_denote_eq_eval_getLsb
Proof state before:
case signExtend
w : Nat
assign : Assignment
w✝ v : Nat
inner : BVExpr w✝
ih :
  ∀ (aig : AIG BVBit) (idx : Nat) (hidx : idx < w✝),
    ⟦{ 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
⊢ ⟦{ aig := (go aig (signExtend v inner)).val.aig, ref := (go aig (signExtend v inner)).val.stream.getRef idx hidx },
      assign.toAIGAssignment⟧ =
    (eval assign (signExtend v inner)).getLsb idx
Tactic:
rename_i originalWidth
Proof state after:
case signExtend
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
⊢ ⟦{ aig := (go aig (signExtend v inner)).val.aig, ref := (go aig (signExtend v inner)).val.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
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
⊢ ⟦{ aig := (go aig (signExtend v inner)).val.aig, ref := (go aig (signExtend v inner)).val.stream.getRef idx hidx },
      assign.toAIGAssignment⟧ =
    (eval assign (signExtend v inner)).getLsb idx
Tactic:
generalize hgo : (go aig (signExtend v inner)).val = res
Proof state after:
case signExtend
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 : (go aig (signExtend v inner)).val = res
⊢ ⟦{ aig := res.aig, ref := res.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
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 : (go aig (signExtend v inner)).val = res
⊢ ⟦{ aig := res.aig, ref := res.stream.getRef idx hidx }, assign.toAIGAssignment⟧ =
    (eval assign (signExtend v inner)).getLsb idx
Tactic:
unfold go at hgo
Proof state after:
case signExtend
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 :
  (match go aig inner with
      | ⟨{ aig := eaig, stream := estream }, heaig⟩ =>
        let res := blastSignExtend eaig { w := originalWidth, stream := estream };
        ⟨res, ⋯⟩).val =
    res
⊢ ⟦{ aig := res.aig, ref := res.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
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 :
  (match go aig inner with
      | ⟨{ aig := eaig, stream := estream }, heaig⟩ =>
        let res := blastSignExtend eaig { w := originalWidth, stream := estream };
        ⟨res, ⋯⟩).val =
    res
⊢ ⟦{ aig := res.aig, ref := res.stream.getRef idx hidx }, assign.toAIGAssignment⟧ =
    (eval assign (signExtend v inner)).getLsb idx
Tactic:
dsimp at hgo
Proof state after:
case signExtend
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
⊢ ⟦{ aig := res.aig, ref := res.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
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
⊢ ⟦{ aig := res.aig, ref := res.stream.getRef idx hidx }, assign.toAIGAssignment⟧ =
    (eval assign (signExtend v inner)).getLsb idx
Tactic:
have : 0 ≤ originalWidth := by omega
Proof state after:
case signExtend
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
⊢ ⟦{ aig := res.aig, ref := res.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
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
⊢ ⟦{ aig := res.aig, ref := res.stream.getRef idx hidx }, assign.toAIGAssignment⟧ =
    (eval assign (signExtend v inner)).getLsb idx
Tactic:
cases Nat.eq_or_lt_of_le this with
| inl heq =>
  rw [blastSignExtend_empty_eq_zeroExtend] at hgo
  . rw [← hgo]
    simp only [eval_signExtend]
    rw [BitVec.signExtend_eq_not_zeroExtend_not_of_msb_false]
    . 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]
      apply BitVec.lt_of_getLsb
    . subst heq
      rw [BitVec.msb_zero_length]
  . simp [heq]
| inr hlt =>
  rw [← hgo]
  rw [blastSignExtend_eq_eval_getLsb]
  simp only [eval_signExtend]
  rw [BitVec.getLsb_signExtend]
  . 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:
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
⊢ 0 ≤ originalWidth
Tactic:
omega
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 : blastSignExtend (go aig inner).1.aig { w := originalWidth, stream := (go aig inner).1.stream } = res
this : 0 ≤ originalWidth
heq : 0 = originalWidth
⊢ ⟦{ aig := res.aig, ref := res.stream.getRef idx hidx }, assign.toAIGAssignment⟧ =
    (eval assign (signExtend v inner)).getLsb idx
Tactic:
rw [blastSignExtend_empty_eq_zeroExtend] at hgo
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
⊢ ⟦{ aig := res.aig, ref := res.stream.getRef idx hidx }, assign.toAIGAssignment⟧ =
    (eval assign (signExtend v inner)).getLsb idx

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
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 := res.aig, ref := res.stream.getRef idx hidx }, assign.toAIGAssignment⟧ =
    (eval assign (signExtend v inner)).getLsb idx

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:
. rw [← hgo]
  simp only [eval_signExtend]
  rw [BitVec.signExtend_eq_not_zeroExtend_not_of_msb_false]
  . 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]
    apply BitVec.lt_of_getLsb
  . subst heq
    rw [BitVec.msb_zero_length]
Proof state after:
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
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.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 := 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.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⟧ =
    (eval assign (signExtend v inner)).getLsb idx
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⟧ =
    (eval assign (signExtend v inner)).getLsb idx
Tactic:
simp only [eval_signExtend]
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
⊢ ⟦{ 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.signExtend v (eval assign inner)).getLsb idx
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.signExtend v (eval assign inner)).getLsb idx
Tactic:
rw [BitVec.signExtend_eq_not_zeroExtend_not_of_msb_false]
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
⊢ ⟦{ 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

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
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

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:
. 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]
  apply BitVec.lt_of_getLsb
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).msb = false
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
  rw [BitVec.msb_zero_length]
Proof state after:
no goals