Theorem: BVExpr.bitblast.go_denote_eq_eval_getLsb (LeanSAT/Reflect/BVExpr/BitBlast/Lemmas/Expr.lean)

State before:
w : Nat
aig : AIG BVBit
expr : BVExpr w
assign : Assignment
⊢ ∀ (idx : Nat) (hidx : idx < w),
    ⟦{ aig := (go aig expr).val.aig, ref := (go aig expr).val.stream.getRef idx hidx }, assign.toAIGAssignment⟧ =
      (eval assign expr).getLsb idx
Tactic:
intro idx hidx
State after:
w : Nat
aig : AIG BVBit
expr : BVExpr w
assign : Assignment
idx : Nat
hidx : idx < w
⊢ ⟦{ aig := (go aig expr).val.aig, ref := (go aig expr).val.stream.getRef idx hidx }, assign.toAIGAssignment⟧ =
    (eval assign expr).getLsb idx

State before:
w : Nat
aig : AIG BVBit
expr : BVExpr w
assign : Assignment
idx : Nat
hidx : idx < w
⊢ ⟦{ aig := (go aig expr).val.aig, ref := (go aig expr).val.stream.getRef idx hidx }, assign.toAIGAssignment⟧ =
    (eval assign expr).getLsb idx
Tactic:
induction expr generalizing aig idx with
| const =>
  simp [go, blastConst_eq_eval_getLsb]
| var =>
  simp [go, hidx, blastVar_eq_eval_getLsb]
| zeroExtend v inner ih =>
  simp only [go, blastZeroExtend_eq_eval_getLsb, ih, dite_eq_ite, Bool.if_false_right,
    eval_zeroExtend, BitVec.getLsb_zeroExtend, hidx, decide_True, Bool.true_and,
    Bool.and_iff_right_iff_imp, decide_eq_true_eq]
  apply BitVec.lt_of_getLsb
| append lhs rhs lih rih =>
  rename_i lw rw
  simp only [go, blastAppend_eq_eval_getLsb, RefStream.getRef_cast, Ref_cast', eval_append,
    BitVec.getLsb_append]
  split
  . next hsplit =>
    simp only [hsplit, decide_True, cond_true]
    rw [rih]
  . next hsplit =>
    simp only [hsplit, decide_False, cond_false]
    rw [go_denote_mem_prefix, lih]
| signExtend v inner ih =>
  rename_i originalWidth
  generalize hgo : (go aig (signExtend v inner)).val = res
  unfold go at hgo
  dsimp at hgo
  have : 0 ≤ originalWidth := by omega
  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]
| extract hi lo inner ih =>
  simp only [go, blastExtract_eq_eval_getLsb, Bool.if_false_right, eval_extract,
    BitVec.getLsb_extract]
  have : idx ≤ hi - lo := by omega
  simp only [this, decide_True, Bool.true_and]
  split
  . next hsplit =>
    rw [ih]
  . apply Eq.symm
    apply BitVec.getLsb_ge
    omega
| bin lhs op rhs lih rih =>
  cases op with
  | and =>
    simp only [go, RefStream.denote_zip, denote_mkAndCached, rih, eval_bin, BVBinOp.eval_and,
      BitVec.getLsb_and]
    simp only [go_val_eq_bitblast, RefStream.getRef_cast]
    rw [AIG.LawfulStreamOperator.denote_input_stream (f := bitblast)]
    rw [← go_val_eq_bitblast]
    rw [lih]
  | or =>
    simp only [go, RefStream.denote_zip, denote_mkOrCached, rih, eval_bin, BVBinOp.eval_or,
      BitVec.getLsb_or]
    simp only [go_val_eq_bitblast, RefStream.getRef_cast]
    rw [AIG.LawfulStreamOperator.denote_input_stream (f := bitblast)]
    rw [← go_val_eq_bitblast]
    rw [lih]
  | xor =>
    simp only [go, RefStream.denote_zip, denote_mkXorCached, rih, eval_bin, BVBinOp.eval_xor,
      BitVec.getLsb_xor]
    simp only [go_val_eq_bitblast, RefStream.getRef_cast]
    rw [AIG.LawfulStreamOperator.denote_input_stream (f := bitblast)]
    rw [← go_val_eq_bitblast]
    rw [lih]
  | add =>
    simp only [go, eval_bin, BVBinOp.eval_add]
    apply blastAdd_eq_eval_getLsb
    . intros
      dsimp
      rw [go_denote_mem_prefix]
      rw [← lih (aig := aig)]
      . simp
      . assumption
      . simp [Ref.hgate]
    . intros
      rw [← rih]
| un op expr ih =>
  cases op with
  | not => simp [go, ih, hidx]
  | shiftLeftConst => simp [go, ih, hidx]
  | shiftRightConst =>
    simp only [go, blastShiftRight_eq_eval_getLsb, ih, dite_eq_ite, Bool.if_false_right, eval_un,
      BVUnOp.eval_shiftRightConst, BitVec.getLsb_ushiftRight, Bool.and_iff_right_iff_imp,
      decide_eq_true_eq]
    intro h
    apply BitVec.lt_of_getLsb
    assumption
  | rotateLeft => simp [go, ih, hidx]
  | rotateRight => simp [go, ih, hidx]
  | arithShiftRightConst n =>
    rename_i w
    have : ¬(w ≤ idx) := by omega
    simp [go, ih, this, BitVec.getLsb_sshiftRight, BitVec.msb_eq_getLsb_last ]
State after:
no goals

State before:
case const
w : Nat
assign : Assignment
w✝ : Nat
val✝ : BitVec w✝
aig : AIG BVBit
idx : Nat
hidx : idx < w✝
⊢ ⟦{ aig := (go aig (const val✝)).val.aig, ref := (go aig (const val✝)).val.stream.getRef idx hidx },
      assign.toAIGAssignment⟧ =
    (eval assign (const val✝)).getLsb idx
Tactic:
simp [go, blastConst_eq_eval_getLsb]
State after:
no goals

State before:
case var
w : Nat
assign : Assignment
w✝ idx✝ : Nat
aig : AIG BVBit
idx : Nat
hidx : idx < w✝
⊢ ⟦{ aig := (go aig (var idx✝)).val.aig, ref := (go aig (var idx✝)).val.stream.getRef idx hidx },
      assign.toAIGAssignment⟧ =
    (eval assign (var idx✝)).getLsb idx
Tactic:
simp [go, hidx, blastVar_eq_eval_getLsb]
State after:
no goals

State before:
case zeroExtend
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 (zeroExtend v inner)).val.aig, ref := (go aig (zeroExtend v inner)).val.stream.getRef idx hidx },
      assign.toAIGAssignment⟧ =
    (eval assign (zeroExtend v inner)).getLsb idx
Tactic:
simp only [go, blastZeroExtend_eq_eval_getLsb, ih, dite_eq_ite, Bool.if_false_right,
  eval_zeroExtend, BitVec.getLsb_zeroExtend, hidx, decide_True, Bool.true_and,
  Bool.and_iff_right_iff_imp, decide_eq_true_eq]
State after:
case zeroExtend
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
⊢ (eval assign inner).getLsb idx = true → idx < w✝

State before:
case zeroExtend
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
⊢ (eval assign inner).getLsb idx = true → idx < w✝
Tactic:
apply BitVec.lt_of_getLsb
State after:
no goals

State before:
case append
w : Nat
assign : Assignment
l✝ r✝ : Nat
lhs : BVExpr l✝
rhs : BVExpr r✝
lih :
  ∀ (aig : AIG BVBit) (idx : Nat) (hidx : idx < l✝),
    ⟦{ aig := (go aig lhs).val.aig, ref := (go aig lhs).val.stream.getRef idx hidx }, assign.toAIGAssignment⟧ =
      (eval assign lhs).getLsb idx
rih :
  ∀ (aig : AIG BVBit) (idx : Nat) (hidx : idx < r✝),
    ⟦{ aig := (go aig rhs).val.aig, ref := (go aig rhs).val.stream.getRef idx hidx }, assign.toAIGAssignment⟧ =
      (eval assign rhs).getLsb idx
aig : AIG BVBit
idx : Nat
hidx : idx < l✝ + r✝
⊢ ⟦{ aig := (go aig (lhs.append rhs)).val.aig, ref := (go aig (lhs.append rhs)).val.stream.getRef idx hidx },
      assign.toAIGAssignment⟧ =
    (eval assign (lhs.append rhs)).getLsb idx
Tactic:
rename_i lw rw
State after:
case append
w : Nat
assign : Assignment
lw rw : Nat
lhs : BVExpr lw
rhs : BVExpr rw
lih :
  ∀ (aig : AIG BVBit) (idx : Nat) (hidx : idx < lw),
    ⟦{ aig := (go aig lhs).val.aig, ref := (go aig lhs).val.stream.getRef idx hidx }, assign.toAIGAssignment⟧ =
      (eval assign lhs).getLsb idx
rih :
  ∀ (aig : AIG BVBit) (idx : Nat) (hidx : idx < rw),
    ⟦{ aig := (go aig rhs).val.aig, ref := (go aig rhs).val.stream.getRef idx hidx }, assign.toAIGAssignment⟧ =
      (eval assign rhs).getLsb idx
aig : AIG BVBit
idx : Nat
hidx : idx < lw + rw
⊢ ⟦{ aig := (go aig (lhs.append rhs)).val.aig, ref := (go aig (lhs.append rhs)).val.stream.getRef idx hidx },
      assign.toAIGAssignment⟧ =
    (eval assign (lhs.append rhs)).getLsb idx

State before:
case append
w : Nat
assign : Assignment
lw rw : Nat
lhs : BVExpr lw
rhs : BVExpr rw
lih :
  ∀ (aig : AIG BVBit) (idx : Nat) (hidx : idx < lw),
    ⟦{ aig := (go aig lhs).val.aig, ref := (go aig lhs).val.stream.getRef idx hidx }, assign.toAIGAssignment⟧ =
      (eval assign lhs).getLsb idx
rih :
  ∀ (aig : AIG BVBit) (idx : Nat) (hidx : idx < rw),
    ⟦{ aig := (go aig rhs).val.aig, ref := (go aig rhs).val.stream.getRef idx hidx }, assign.toAIGAssignment⟧ =
      (eval assign rhs).getLsb idx
aig : AIG BVBit
idx : Nat
hidx : idx < lw + rw
⊢ ⟦{ aig := (go aig (lhs.append rhs)).val.aig, ref := (go aig (lhs.append rhs)).val.stream.getRef idx hidx },
      assign.toAIGAssignment⟧ =
    (eval assign (lhs.append rhs)).getLsb idx
Tactic:
simp only [go, blastAppend_eq_eval_getLsb, RefStream.getRef_cast, Ref_cast', eval_append,
  BitVec.getLsb_append]
State after:
case append
w : Nat
assign : Assignment
lw rw : Nat
lhs : BVExpr lw
rhs : BVExpr rw
lih :
  ∀ (aig : AIG BVBit) (idx : Nat) (hidx : idx < lw),
    ⟦{ aig := (go aig lhs).val.aig, ref := (go aig lhs).val.stream.getRef idx hidx }, assign.toAIGAssignment⟧ =
      (eval assign lhs).getLsb idx
rih :
  ∀ (aig : AIG BVBit) (idx : Nat) (hidx : idx < rw),
    ⟦{ aig := (go aig rhs).val.aig, ref := (go aig rhs).val.stream.getRef idx hidx }, assign.toAIGAssignment⟧ =
      (eval assign rhs).getLsb idx
aig : AIG BVBit
idx : Nat
hidx : idx < lw + rw
⊢ (if h : idx < rw then
      ⟦{ aig := (go (go aig lhs).1.aig rhs).1.aig, ref := (go (go aig lhs).1.aig rhs).1.stream.getRef idx ⋯ },
        assign.toAIGAssignment⟧
    else
      ⟦{ aig := (go (go aig lhs).1.aig rhs).1.aig,
          ref := { gate := ((go aig lhs).1.stream.getRef (idx - rw) ⋯).gate, hgate := ⋯ } },
        assign.toAIGAssignment⟧) =
    bif decide (idx < rw) then (eval assign rhs).getLsb idx else (eval assign lhs).getLsb (idx - rw)

State before:
case append
w : Nat
assign : Assignment
lw rw : Nat
lhs : BVExpr lw
rhs : BVExpr rw
lih :
  ∀ (aig : AIG BVBit) (idx : Nat) (hidx : idx < lw),
    ⟦{ aig := (go aig lhs).val.aig, ref := (go aig lhs).val.stream.getRef idx hidx }, assign.toAIGAssignment⟧ =
      (eval assign lhs).getLsb idx
rih :
  ∀ (aig : AIG BVBit) (idx : Nat) (hidx : idx < rw),
    ⟦{ aig := (go aig rhs).val.aig, ref := (go aig rhs).val.stream.getRef idx hidx }, assign.toAIGAssignment⟧ =
      (eval assign rhs).getLsb idx
aig : AIG BVBit
idx : Nat
hidx : idx < lw + rw
⊢ (if h : idx < rw then
      ⟦{ aig := (go (go aig lhs).1.aig rhs).1.aig, ref := (go (go aig lhs).1.aig rhs).1.stream.getRef idx ⋯ },
        assign.toAIGAssignment⟧
    else
      ⟦{ aig := (go (go aig lhs).1.aig rhs).1.aig,
          ref := { gate := ((go aig lhs).1.stream.getRef (idx - rw) ⋯).gate, hgate := ⋯ } },
        assign.toAIGAssignment⟧) =
    bif decide (idx < rw) then (eval assign rhs).getLsb idx else (eval assign lhs).getLsb (idx - rw)
Tactic:
split
State after:
case append.isTrue
w : Nat
assign : Assignment
lw rw : Nat
lhs : BVExpr lw
rhs : BVExpr rw
lih :
  ∀ (aig : AIG BVBit) (idx : Nat) (hidx : idx < lw),
    ⟦{ aig := (go aig lhs).val.aig, ref := (go aig lhs).val.stream.getRef idx hidx }, assign.toAIGAssignment⟧ =
      (eval assign lhs).getLsb idx
rih :
  ∀ (aig : AIG BVBit) (idx : Nat) (hidx : idx < rw),
    ⟦{ aig := (go aig rhs).val.aig, ref := (go aig rhs).val.stream.getRef idx hidx }, assign.toAIGAssignment⟧ =
      (eval assign rhs).getLsb idx
aig : AIG BVBit
idx : Nat
hidx : idx < lw + rw
h✝ : idx < rw
⊢ ⟦{ aig := (go (go aig lhs).1.aig rhs).1.aig, ref := (go (go aig lhs).1.aig rhs).1.stream.getRef idx ⋯ },
      assign.toAIGAssignment⟧ =
    bif decide (idx < rw) then (eval assign rhs).getLsb idx else (eval assign lhs).getLsb (idx - rw)

case append.isFalse
w : Nat
assign : Assignment
lw rw : Nat
lhs : BVExpr lw
rhs : BVExpr rw
lih :
  ∀ (aig : AIG BVBit) (idx : Nat) (hidx : idx < lw),
    ⟦{ aig := (go aig lhs).val.aig, ref := (go aig lhs).val.stream.getRef idx hidx }, assign.toAIGAssignment⟧ =
      (eval assign lhs).getLsb idx
rih :
  ∀ (aig : AIG BVBit) (idx : Nat) (hidx : idx < rw),
    ⟦{ aig := (go aig rhs).val.aig, ref := (go aig rhs).val.stream.getRef idx hidx }, assign.toAIGAssignment⟧ =
      (eval assign rhs).getLsb idx
aig : AIG BVBit
idx : Nat
hidx : idx < lw + rw
h✝ : ¬idx < rw
⊢ ⟦{ aig := (go (go aig lhs).1.aig rhs).1.aig,
        ref := { gate := ((go aig lhs).1.stream.getRef (idx - rw) ⋯).gate, hgate := ⋯ } },
      assign.toAIGAssignment⟧ =
    bif decide (idx < rw) then (eval assign rhs).getLsb idx else (eval assign lhs).getLsb (idx - rw)

State before:
case append.isTrue
w : Nat
assign : Assignment
lw rw : Nat
lhs : BVExpr lw
rhs : BVExpr rw
lih :
  ∀ (aig : AIG BVBit) (idx : Nat) (hidx : idx < lw),
    ⟦{ aig := (go aig lhs).val.aig, ref := (go aig lhs).val.stream.getRef idx hidx }, assign.toAIGAssignment⟧ =
      (eval assign lhs).getLsb idx
rih :
  ∀ (aig : AIG BVBit) (idx : Nat) (hidx : idx < rw),
    ⟦{ aig := (go aig rhs).val.aig, ref := (go aig rhs).val.stream.getRef idx hidx }, assign.toAIGAssignment⟧ =
      (eval assign rhs).getLsb idx
aig : AIG BVBit
idx : Nat
hidx : idx < lw + rw
h✝ : idx < rw
⊢ ⟦{ aig := (go (go aig lhs).1.aig rhs).1.aig, ref := (go (go aig lhs).1.aig rhs).1.stream.getRef idx ⋯ },
      assign.toAIGAssignment⟧ =
    bif decide (idx < rw) then (eval assign rhs).getLsb idx else (eval assign lhs).getLsb (idx - rw)

case append.isFalse
w : Nat
assign : Assignment
lw rw : Nat
lhs : BVExpr lw
rhs : BVExpr rw
lih :
  ∀ (aig : AIG BVBit) (idx : Nat) (hidx : idx < lw),
    ⟦{ aig := (go aig lhs).val.aig, ref := (go aig lhs).val.stream.getRef idx hidx }, assign.toAIGAssignment⟧ =
      (eval assign lhs).getLsb idx
rih :
  ∀ (aig : AIG BVBit) (idx : Nat) (hidx : idx < rw),
    ⟦{ aig := (go aig rhs).val.aig, ref := (go aig rhs).val.stream.getRef idx hidx }, assign.toAIGAssignment⟧ =
      (eval assign rhs).getLsb idx
aig : AIG BVBit
idx : Nat
hidx : idx < lw + rw
h✝ : ¬idx < rw
⊢ ⟦{ aig := (go (go aig lhs).1.aig rhs).1.aig,
        ref := { gate := ((go aig lhs).1.stream.getRef (idx - rw) ⋯).gate, hgate := ⋯ } },
      assign.toAIGAssignment⟧ =
    bif decide (idx < rw) then (eval assign rhs).getLsb idx else (eval assign lhs).getLsb (idx - rw)
Tactic:
. next hsplit =>
  simp only [hsplit, decide_True, cond_true]
  rw [rih]
State after:
case append.isFalse
w : Nat
assign : Assignment
lw rw : Nat
lhs : BVExpr lw
rhs : BVExpr rw
lih :
  ∀ (aig : AIG BVBit) (idx : Nat) (hidx : idx < lw),
    ⟦{ aig := (go aig lhs).val.aig, ref := (go aig lhs).val.stream.getRef idx hidx }, assign.toAIGAssignment⟧ =
      (eval assign lhs).getLsb idx
rih :
  ∀ (aig : AIG BVBit) (idx : Nat) (hidx : idx < rw),
    ⟦{ aig := (go aig rhs).val.aig, ref := (go aig rhs).val.stream.getRef idx hidx }, assign.toAIGAssignment⟧ =
      (eval assign rhs).getLsb idx
aig : AIG BVBit
idx : Nat
hidx : idx < lw + rw
h✝ : ¬idx < rw
⊢ ⟦{ aig := (go (go aig lhs).1.aig rhs).1.aig,
        ref := { gate := ((go aig lhs).1.stream.getRef (idx - rw) ⋯).gate, hgate := ⋯ } },
      assign.toAIGAssignment⟧ =
    bif decide (idx < rw) then (eval assign rhs).getLsb idx else (eval assign lhs).getLsb (idx - rw)

State before:
case append.isFalse
w : Nat
assign : Assignment
lw rw : Nat
lhs : BVExpr lw
rhs : BVExpr rw
lih :
  ∀ (aig : AIG BVBit) (idx : Nat) (hidx : idx < lw),
    ⟦{ aig := (go aig lhs).val.aig, ref := (go aig lhs).val.stream.getRef idx hidx }, assign.toAIGAssignment⟧ =
      (eval assign lhs).getLsb idx
rih :
  ∀ (aig : AIG BVBit) (idx : Nat) (hidx : idx < rw),
    ⟦{ aig := (go aig rhs).val.aig, ref := (go aig rhs).val.stream.getRef idx hidx }, assign.toAIGAssignment⟧ =
      (eval assign rhs).getLsb idx
aig : AIG BVBit
idx : Nat
hidx : idx < lw + rw
h✝ : ¬idx < rw
⊢ ⟦{ aig := (go (go aig lhs).1.aig rhs).1.aig,
        ref := { gate := ((go aig lhs).1.stream.getRef (idx - rw) ⋯).gate, hgate := ⋯ } },
      assign.toAIGAssignment⟧ =
    bif decide (idx < rw) then (eval assign rhs).getLsb idx else (eval assign lhs).getLsb (idx - rw)
Tactic:
. next hsplit =>
  simp only [hsplit, decide_False, cond_false]
  rw [go_denote_mem_prefix, lih]
State after:
no goals

State before:
case append.isTrue
w : Nat
assign : Assignment
lw rw : Nat
lhs : BVExpr lw
rhs : BVExpr rw
lih :
  ∀ (aig : AIG BVBit) (idx : Nat) (hidx : idx < lw),
    ⟦{ aig := (go aig lhs).val.aig, ref := (go aig lhs).val.stream.getRef idx hidx }, assign.toAIGAssignment⟧ =
      (eval assign lhs).getLsb idx
rih :
  ∀ (aig : AIG BVBit) (idx : Nat) (hidx : idx < rw),
    ⟦{ aig := (go aig rhs).val.aig, ref := (go aig rhs).val.stream.getRef idx hidx }, assign.toAIGAssignment⟧ =
      (eval assign rhs).getLsb idx
aig : AIG BVBit
idx : Nat
hidx : idx < lw + rw
h✝ : idx < rw
⊢ ⟦{ aig := (go (go aig lhs).1.aig rhs).1.aig, ref := (go (go aig lhs).1.aig rhs).1.stream.getRef idx ⋯ },
      assign.toAIGAssignment⟧ =
    bif decide (idx < rw) then (eval assign rhs).getLsb idx else (eval assign lhs).getLsb (idx - rw)
Tactic:
next hsplit =>
simp only [hsplit, decide_True, cond_true]
rw [rih]
State after:
no goals

State before:
w : Nat
assign : Assignment
lw rw : Nat
lhs : BVExpr lw
rhs : BVExpr rw
lih :
  ∀ (aig : AIG BVBit) (idx : Nat) (hidx : idx < lw),
    ⟦{ aig := (go aig lhs).val.aig, ref := (go aig lhs).val.stream.getRef idx hidx }, assign.toAIGAssignment⟧ =
      (eval assign lhs).getLsb idx
rih :
  ∀ (aig : AIG BVBit) (idx : Nat) (hidx : idx < rw),
    ⟦{ aig := (go aig rhs).val.aig, ref := (go aig rhs).val.stream.getRef idx hidx }, assign.toAIGAssignment⟧ =
      (eval assign rhs).getLsb idx
aig : AIG BVBit
idx : Nat
hidx : idx < lw + rw
hsplit : idx < rw
⊢ ⟦{ aig := (go (go aig lhs).1.aig rhs).1.aig, ref := (go (go aig lhs).1.aig rhs).1.stream.getRef idx ⋯ },
      assign.toAIGAssignment⟧ =
    bif decide (idx < rw) then (eval assign rhs).getLsb idx else (eval assign lhs).getLsb (idx - rw)
Tactic:
simp only [hsplit, decide_True, cond_true]
State after:
w : Nat
assign : Assignment
lw rw : Nat
lhs : BVExpr lw
rhs : BVExpr rw
lih :
  ∀ (aig : AIG BVBit) (idx : Nat) (hidx : idx < lw),
    ⟦{ aig := (go aig lhs).val.aig, ref := (go aig lhs).val.stream.getRef idx hidx }, assign.toAIGAssignment⟧ =
      (eval assign lhs).getLsb idx
rih :
  ∀ (aig : AIG BVBit) (idx : Nat) (hidx : idx < rw),
    ⟦{ aig := (go aig rhs).val.aig, ref := (go aig rhs).val.stream.getRef idx hidx }, assign.toAIGAssignment⟧ =
      (eval assign rhs).getLsb idx
aig : AIG BVBit
idx : Nat
hidx : idx < lw + rw
hsplit : idx < rw
⊢ ⟦{ aig := (go (go aig lhs).1.aig rhs).1.aig, ref := (go (go aig lhs).1.aig rhs).1.stream.getRef idx ⋯ },
      assign.toAIGAssignment⟧ =
    (eval assign rhs).getLsb idx

State before:
w : Nat
assign : Assignment
lw rw : Nat
lhs : BVExpr lw
rhs : BVExpr rw
lih :
  ∀ (aig : AIG BVBit) (idx : Nat) (hidx : idx < lw),
    ⟦{ aig := (go aig lhs).val.aig, ref := (go aig lhs).val.stream.getRef idx hidx }, assign.toAIGAssignment⟧ =
      (eval assign lhs).getLsb idx
rih :
  ∀ (aig : AIG BVBit) (idx : Nat) (hidx : idx < rw),
    ⟦{ aig := (go aig rhs).val.aig, ref := (go aig rhs).val.stream.getRef idx hidx }, assign.toAIGAssignment⟧ =
      (eval assign rhs).getLsb idx
aig : AIG BVBit
idx : Nat
hidx : idx < lw + rw
hsplit : idx < rw
⊢ ⟦{ aig := (go (go aig lhs).1.aig rhs).1.aig, ref := (go (go aig lhs).1.aig rhs).1.stream.getRef idx ⋯ },
      assign.toAIGAssignment⟧ =
    (eval assign rhs).getLsb idx
Tactic:
rw [rih]
State after:
no goals

State before:
case append.isFalse
w : Nat
assign : Assignment
lw rw : Nat
lhs : BVExpr lw
rhs : BVExpr rw
lih :
  ∀ (aig : AIG BVBit) (idx : Nat) (hidx : idx < lw),
    ⟦{ aig := (go aig lhs).val.aig, ref := (go aig lhs).val.stream.getRef idx hidx }, assign.toAIGAssignment⟧ =
      (eval assign lhs).getLsb idx
rih :
  ∀ (aig : AIG BVBit) (idx : Nat) (hidx : idx < rw),
    ⟦{ aig := (go aig rhs).val.aig, ref := (go aig rhs).val.stream.getRef idx hidx }, assign.toAIGAssignment⟧ =
      (eval assign rhs).getLsb idx
aig : AIG BVBit
idx : Nat
hidx : idx < lw + rw
h✝ : ¬idx < rw
⊢ ⟦{ aig := (go (go aig lhs).1.aig rhs).1.aig,
        ref := { gate := ((go aig lhs).1.stream.getRef (idx - rw) ⋯).gate, hgate := ⋯ } },
      assign.toAIGAssignment⟧ =
    bif decide (idx < rw) then (eval assign rhs).getLsb idx else (eval assign lhs).getLsb (idx - rw)
Tactic:
next hsplit =>
simp only [hsplit, decide_False, cond_false]
rw [go_denote_mem_prefix, lih]
State after:
no goals

State before:
w : Nat
assign : Assignment
lw rw : Nat
lhs : BVExpr lw
rhs : BVExpr rw
lih :
  ∀ (aig : AIG BVBit) (idx : Nat) (hidx : idx < lw),
    ⟦{ aig := (go aig lhs).val.aig, ref := (go aig lhs).val.stream.getRef idx hidx }, assign.toAIGAssignment⟧ =
      (eval assign lhs).getLsb idx
rih :
  ∀ (aig : AIG BVBit) (idx : Nat) (hidx : idx < rw),
    ⟦{ aig := (go aig rhs).val.aig, ref := (go aig rhs).val.stream.getRef idx hidx }, assign.toAIGAssignment⟧ =
      (eval assign rhs).getLsb idx
aig : AIG BVBit
idx : Nat
hidx : idx < lw + rw
hsplit : ¬idx < rw
⊢ ⟦{ aig := (go (go aig lhs).1.aig rhs).1.aig,
        ref := { gate := ((go aig lhs).1.stream.getRef (idx - rw) ⋯).gate, hgate := ⋯ } },
      assign.toAIGAssignment⟧ =
    bif decide (idx < rw) then (eval assign rhs).getLsb idx else (eval assign lhs).getLsb (idx - rw)
Tactic:
simp only [hsplit, decide_False, cond_false]
State after:
w : Nat
assign : Assignment
lw rw : Nat
lhs : BVExpr lw
rhs : BVExpr rw
lih :
  ∀ (aig : AIG BVBit) (idx : Nat) (hidx : idx < lw),
    ⟦{ aig := (go aig lhs).val.aig, ref := (go aig lhs).val.stream.getRef idx hidx }, assign.toAIGAssignment⟧ =
      (eval assign lhs).getLsb idx
rih :
  ∀ (aig : AIG BVBit) (idx : Nat) (hidx : idx < rw),
    ⟦{ aig := (go aig rhs).val.aig, ref := (go aig rhs).val.stream.getRef idx hidx }, assign.toAIGAssignment⟧ =
      (eval assign rhs).getLsb idx
aig : AIG BVBit
idx : Nat
hidx : idx < lw + rw
hsplit : ¬idx < rw
⊢ ⟦{ aig := (go (go aig lhs).1.aig rhs).1.aig,
        ref := { gate := ((go aig lhs).1.stream.getRef (idx - rw) ⋯).gate, hgate := ⋯ } },
      assign.toAIGAssignment⟧ =
    (eval assign lhs).getLsb (idx - rw)

State before:
w : Nat
assign : Assignment
lw rw : Nat
lhs : BVExpr lw
rhs : BVExpr rw
lih :
  ∀ (aig : AIG BVBit) (idx : Nat) (hidx : idx < lw),
    ⟦{ aig := (go aig lhs).val.aig, ref := (go aig lhs).val.stream.getRef idx hidx }, assign.toAIGAssignment⟧ =
      (eval assign lhs).getLsb idx
rih :
  ∀ (aig : AIG BVBit) (idx : Nat) (hidx : idx < rw),
    ⟦{ aig := (go aig rhs).val.aig, ref := (go aig rhs).val.stream.getRef idx hidx }, assign.toAIGAssignment⟧ =
      (eval assign rhs).getLsb idx
aig : AIG BVBit
idx : Nat
hidx : idx < lw + rw
hsplit : ¬idx < rw
⊢ ⟦{ aig := (go (go aig lhs).1.aig rhs).1.aig,
        ref := { gate := ((go aig lhs).1.stream.getRef (idx - rw) ⋯).gate, hgate := ⋯ } },
      assign.toAIGAssignment⟧ =
    (eval assign lhs).getLsb (idx - rw)
Tactic:
rw [go_denote_mem_prefix, lih]
State after:
no goals

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

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

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

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

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

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]
State after:
no goals

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
State after:
no goals

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

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

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]
State after:
no goals

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

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

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

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

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]
State after:
no goals

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

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
State after:
no goals

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

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]
State after:
no goals

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]
State after:
no goals

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

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

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 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
Tactic:
simp only [eval_signExtend]
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⟧) =
    (BitVec.signExtend v (eval assign 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

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⟧) =
    (BitVec.signExtend v (eval assign 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
Tactic:
rw [BitVec.getLsb_signExtend]
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⟧) =
    (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

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]
State after:
no goals

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

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

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

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]
State after:
no goals

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]
State after:
no goals

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

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).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
Tactic:
rw [ih]
State after:
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

State before:
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 [hlt]
State after:
no goals

State before:
case extract
w : Nat
assign : Assignment
w✝ hi lo : 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 < hi - lo + 1
⊢ ⟦{ aig := (go aig (extract hi lo inner)).val.aig, ref := (go aig (extract hi lo inner)).val.stream.getRef idx hidx },
      assign.toAIGAssignment⟧ =
    (eval assign (extract hi lo inner)).getLsb idx
Tactic:
simp only [go, blastExtract_eq_eval_getLsb, Bool.if_false_right, eval_extract,
  BitVec.getLsb_extract]
State after:
case extract
w : Nat
assign : Assignment
w✝ hi lo : 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 < hi - lo + 1
⊢ (if h : lo + idx < w✝ then
      ⟦{ aig := (go aig inner).1.aig, ref := (go aig inner).1.stream.getRef (lo + idx) ⋯ }, assign.toAIGAssignment⟧
    else false) =
    (decide (idx ≤ hi - lo) && (eval assign inner).getLsb (lo + idx))

State before:
case extract
w : Nat
assign : Assignment
w✝ hi lo : 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 < hi - lo + 1
⊢ (if h : lo + idx < w✝ then
      ⟦{ aig := (go aig inner).1.aig, ref := (go aig inner).1.stream.getRef (lo + idx) ⋯ }, assign.toAIGAssignment⟧
    else false) =
    (decide (idx ≤ hi - lo) && (eval assign inner).getLsb (lo + idx))
Tactic:
have : idx ≤ hi - lo := by omega
State after:
case extract
w : Nat
assign : Assignment
w✝ hi lo : 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 < hi - lo + 1
this : idx ≤ hi - lo
⊢ (if h : lo + idx < w✝ then
      ⟦{ aig := (go aig inner).1.aig, ref := (go aig inner).1.stream.getRef (lo + idx) ⋯ }, assign.toAIGAssignment⟧
    else false) =
    (decide (idx ≤ hi - lo) && (eval assign inner).getLsb (lo + idx))

State before:
case extract
w : Nat
assign : Assignment
w✝ hi lo : 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 < hi - lo + 1
this : idx ≤ hi - lo
⊢ (if h : lo + idx < w✝ then
      ⟦{ aig := (go aig inner).1.aig, ref := (go aig inner).1.stream.getRef (lo + idx) ⋯ }, assign.toAIGAssignment⟧
    else false) =
    (decide (idx ≤ hi - lo) && (eval assign inner).getLsb (lo + idx))
Tactic:
simp only [this, decide_True, Bool.true_and]
State after:
case extract
w : Nat
assign : Assignment
w✝ hi lo : 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 < hi - lo + 1
this : idx ≤ hi - lo
⊢ (if h : lo + idx < w✝ then
      ⟦{ aig := (go aig inner).1.aig, ref := (go aig inner).1.stream.getRef (lo + idx) ⋯ }, assign.toAIGAssignment⟧
    else false) =
    (eval assign inner).getLsb (lo + idx)

State before:
case extract
w : Nat
assign : Assignment
w✝ hi lo : 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 < hi - lo + 1
this : idx ≤ hi - lo
⊢ (if h : lo + idx < w✝ then
      ⟦{ aig := (go aig inner).1.aig, ref := (go aig inner).1.stream.getRef (lo + idx) ⋯ }, assign.toAIGAssignment⟧
    else false) =
    (eval assign inner).getLsb (lo + idx)
Tactic:
split
State after:
case extract.isTrue
w : Nat
assign : Assignment
w✝ hi lo : 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 < hi - lo + 1
this : idx ≤ hi - lo
h✝ : lo + idx < w✝
⊢ ⟦{ aig := (go aig inner).1.aig, ref := (go aig inner).1.stream.getRef (lo + idx) ⋯ }, assign.toAIGAssignment⟧ =
    (eval assign inner).getLsb (lo + idx)

case extract.isFalse
w : Nat
assign : Assignment
w✝ hi lo : 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 < hi - lo + 1
this : idx ≤ hi - lo
h✝ : ¬lo + idx < w✝
⊢ false = (eval assign inner).getLsb (lo + idx)

State before:
case extract.isTrue
w : Nat
assign : Assignment
w✝ hi lo : 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 < hi - lo + 1
this : idx ≤ hi - lo
h✝ : lo + idx < w✝
⊢ ⟦{ aig := (go aig inner).1.aig, ref := (go aig inner).1.stream.getRef (lo + idx) ⋯ }, assign.toAIGAssignment⟧ =
    (eval assign inner).getLsb (lo + idx)

case extract.isFalse
w : Nat
assign : Assignment
w✝ hi lo : 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 < hi - lo + 1
this : idx ≤ hi - lo
h✝ : ¬lo + idx < w✝
⊢ false = (eval assign inner).getLsb (lo + idx)
Tactic:
. next hsplit =>
  rw [ih]
State after:
case extract.isFalse
w : Nat
assign : Assignment
w✝ hi lo : 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 < hi - lo + 1
this : idx ≤ hi - lo
h✝ : ¬lo + idx < w✝
⊢ false = (eval assign inner).getLsb (lo + idx)

State before:
case extract.isFalse
w : Nat
assign : Assignment
w✝ hi lo : 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 < hi - lo + 1
this : idx ≤ hi - lo
h✝ : ¬lo + idx < w✝
⊢ false = (eval assign inner).getLsb (lo + idx)
Tactic:
. apply Eq.symm
  apply BitVec.getLsb_ge
  omega
State after:
no goals

State before:
w : Nat
assign : Assignment
w✝ hi lo : 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 < hi - lo + 1
⊢ idx ≤ hi - lo
Tactic:
omega
State after:
no goals

State before:
case extract.isTrue
w : Nat
assign : Assignment
w✝ hi lo : 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 < hi - lo + 1
this : idx ≤ hi - lo
h✝ : lo + idx < w✝
⊢ ⟦{ aig := (go aig inner).1.aig, ref := (go aig inner).1.stream.getRef (lo + idx) ⋯ }, assign.toAIGAssignment⟧ =
    (eval assign inner).getLsb (lo + idx)
Tactic:
next hsplit =>
rw [ih]
State after:
no goals

State before:
w : Nat
assign : Assignment
w✝ hi lo : 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 < hi - lo + 1
this : idx ≤ hi - lo
hsplit : lo + idx < w✝
⊢ ⟦{ aig := (go aig inner).1.aig, ref := (go aig inner).1.stream.getRef (lo + idx) ⋯ }, assign.toAIGAssignment⟧ =
    (eval assign inner).getLsb (lo + idx)
Tactic:
rw [ih]
State after:
no goals

State before:
case extract.isFalse
w : Nat
assign : Assignment
w✝ hi lo : 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 < hi - lo + 1
this : idx ≤ hi - lo
h✝ : ¬lo + idx < w✝
⊢ false = (eval assign inner).getLsb (lo + idx)
Tactic:
apply Eq.symm
State after:
case extract.isFalse.h
w : Nat
assign : Assignment
w✝ hi lo : 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 < hi - lo + 1
this : idx ≤ hi - lo
h✝ : ¬lo + idx < w✝
⊢ (eval assign inner).getLsb (lo + idx) = false

State before:
case extract.isFalse.h
w : Nat
assign : Assignment
w✝ hi lo : 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 < hi - lo + 1
this : idx ≤ hi - lo
h✝ : ¬lo + idx < w✝
⊢ (eval assign inner).getLsb (lo + idx) = false
Tactic:
apply BitVec.getLsb_ge
State after:
case extract.isFalse.h.ge
w : Nat
assign : Assignment
w✝ hi lo : 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 < hi - lo + 1
this : idx ≤ hi - lo
h✝ : ¬lo + idx < w✝
⊢ w✝ ≤ lo + idx

State before:
case extract.isFalse.h.ge
w : Nat
assign : Assignment
w✝ hi lo : 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 < hi - lo + 1
this : idx ≤ hi - lo
h✝ : ¬lo + idx < w✝
⊢ w✝ ≤ lo + idx
Tactic:
omega
State after:
no goals

State before:
case bin
w : Nat
assign : Assignment
w✝ : Nat
lhs : BVExpr w✝
op : BVBinOp
rhs : BVExpr w✝
lih :
  ∀ (aig : AIG BVBit) (idx : Nat) (hidx : idx < w✝),
    ⟦{ aig := (go aig lhs).val.aig, ref := (go aig lhs).val.stream.getRef idx hidx }, assign.toAIGAssignment⟧ =
      (eval assign lhs).getLsb idx
rih :
  ∀ (aig : AIG BVBit) (idx : Nat) (hidx : idx < w✝),
    ⟦{ aig := (go aig rhs).val.aig, ref := (go aig rhs).val.stream.getRef idx hidx }, assign.toAIGAssignment⟧ =
      (eval assign rhs).getLsb idx
aig : AIG BVBit
idx : Nat
hidx : idx < w✝
⊢ ⟦{ aig := (go aig (lhs.bin op rhs)).val.aig, ref := (go aig (lhs.bin op rhs)).val.stream.getRef idx hidx },
      assign.toAIGAssignment⟧ =
    (eval assign (lhs.bin op rhs)).getLsb idx
Tactic:
cases op with
| and =>
  simp only [go, RefStream.denote_zip, denote_mkAndCached, rih, eval_bin, BVBinOp.eval_and,
    BitVec.getLsb_and]
  simp only [go_val_eq_bitblast, RefStream.getRef_cast]
  rw [AIG.LawfulStreamOperator.denote_input_stream (f := bitblast)]
  rw [← go_val_eq_bitblast]
  rw [lih]
| or =>
  simp only [go, RefStream.denote_zip, denote_mkOrCached, rih, eval_bin, BVBinOp.eval_or,
    BitVec.getLsb_or]
  simp only [go_val_eq_bitblast, RefStream.getRef_cast]
  rw [AIG.LawfulStreamOperator.denote_input_stream (f := bitblast)]
  rw [← go_val_eq_bitblast]
  rw [lih]
| xor =>
  simp only [go, RefStream.denote_zip, denote_mkXorCached, rih, eval_bin, BVBinOp.eval_xor,
    BitVec.getLsb_xor]
  simp only [go_val_eq_bitblast, RefStream.getRef_cast]
  rw [AIG.LawfulStreamOperator.denote_input_stream (f := bitblast)]
  rw [← go_val_eq_bitblast]
  rw [lih]
| add =>
  simp only [go, eval_bin, BVBinOp.eval_add]
  apply blastAdd_eq_eval_getLsb
  . intros
    dsimp
    rw [go_denote_mem_prefix]
    rw [← lih (aig := aig)]
    . simp
    . assumption
    . simp [Ref.hgate]
  . intros
    rw [← rih]
State after:
no goals

State before:
case bin.and
w : Nat
assign : Assignment
w✝ : Nat
lhs rhs : BVExpr w✝
lih :
  ∀ (aig : AIG BVBit) (idx : Nat) (hidx : idx < w✝),
    ⟦{ aig := (go aig lhs).val.aig, ref := (go aig lhs).val.stream.getRef idx hidx }, assign.toAIGAssignment⟧ =
      (eval assign lhs).getLsb idx
rih :
  ∀ (aig : AIG BVBit) (idx : Nat) (hidx : idx < w✝),
    ⟦{ aig := (go aig rhs).val.aig, ref := (go aig rhs).val.stream.getRef idx hidx }, assign.toAIGAssignment⟧ =
      (eval assign rhs).getLsb idx
aig : AIG BVBit
idx : Nat
hidx : idx < w✝
⊢ ⟦{ aig := (go aig (lhs.bin BVBinOp.and rhs)).val.aig,
        ref := (go aig (lhs.bin BVBinOp.and rhs)).val.stream.getRef idx hidx },
      assign.toAIGAssignment⟧ =
    (eval assign (lhs.bin BVBinOp.and rhs)).getLsb idx
Tactic:
simp only [go, RefStream.denote_zip, denote_mkAndCached, rih, eval_bin, BVBinOp.eval_and,
  BitVec.getLsb_and]
State after:
case bin.and
w : Nat
assign : Assignment
w✝ : Nat
lhs rhs : BVExpr w✝
lih :
  ∀ (aig : AIG BVBit) (idx : Nat) (hidx : idx < w✝),
    ⟦{ aig := (go aig lhs).val.aig, ref := (go aig lhs).val.stream.getRef idx hidx }, assign.toAIGAssignment⟧ =
      (eval assign lhs).getLsb idx
rih :
  ∀ (aig : AIG BVBit) (idx : Nat) (hidx : idx < w✝),
    ⟦{ aig := (go aig rhs).val.aig, ref := (go aig rhs).val.stream.getRef idx hidx }, assign.toAIGAssignment⟧ =
      (eval assign rhs).getLsb idx
aig : AIG BVBit
idx : Nat
hidx : idx < w✝
⊢ (⟦{ aig := (go (go aig lhs).1.aig rhs).1.aig, ref := ((go aig lhs).1.stream.cast ⋯).getRef idx hidx },
        assign.toAIGAssignment⟧ &&
      (eval assign rhs).getLsb idx) =
    ((eval assign lhs).getLsb idx && (eval assign rhs).getLsb idx)

State before:
case bin.and
w : Nat
assign : Assignment
w✝ : Nat
lhs rhs : BVExpr w✝
lih :
  ∀ (aig : AIG BVBit) (idx : Nat) (hidx : idx < w✝),
    ⟦{ aig := (go aig lhs).val.aig, ref := (go aig lhs).val.stream.getRef idx hidx }, assign.toAIGAssignment⟧ =
      (eval assign lhs).getLsb idx
rih :
  ∀ (aig : AIG BVBit) (idx : Nat) (hidx : idx < w✝),
    ⟦{ aig := (go aig rhs).val.aig, ref := (go aig rhs).val.stream.getRef idx hidx }, assign.toAIGAssignment⟧ =
      (eval assign rhs).getLsb idx
aig : AIG BVBit
idx : Nat
hidx : idx < w✝
⊢ (⟦{ aig := (go (go aig lhs).1.aig rhs).1.aig, ref := ((go aig lhs).1.stream.cast ⋯).getRef idx hidx },
        assign.toAIGAssignment⟧ &&
      (eval assign rhs).getLsb idx) =
    ((eval assign lhs).getLsb idx && (eval assign rhs).getLsb idx)
Tactic:
simp only [go_val_eq_bitblast, RefStream.getRef_cast]
State after:
case bin.and
w : Nat
assign : Assignment
w✝ : Nat
lhs rhs : BVExpr w✝
lih :
  ∀ (aig : AIG BVBit) (idx : Nat) (hidx : idx < w✝),
    ⟦{ aig := (go aig lhs).val.aig, ref := (go aig lhs).val.stream.getRef idx hidx }, assign.toAIGAssignment⟧ =
      (eval assign lhs).getLsb idx
rih :
  ∀ (aig : AIG BVBit) (idx : Nat) (hidx : idx < w✝),
    ⟦{ aig := (go aig rhs).val.aig, ref := (go aig rhs).val.stream.getRef idx hidx }, assign.toAIGAssignment⟧ =
      (eval assign rhs).getLsb idx
aig : AIG BVBit
idx : Nat
hidx : idx < w✝
⊢ (⟦{ aig := (bitblast (bitblast aig lhs).aig rhs).aig, ref := ((bitblast aig lhs).stream.getRef idx hidx).cast ⋯ },
        assign.toAIGAssignment⟧ &&
      (eval assign rhs).getLsb idx) =
    ((eval assign lhs).getLsb idx && (eval assign rhs).getLsb idx)

State before:
case bin.and
w : Nat
assign : Assignment
w✝ : Nat
lhs rhs : BVExpr w✝
lih :
  ∀ (aig : AIG BVBit) (idx : Nat) (hidx : idx < w✝),
    ⟦{ aig := (go aig lhs).val.aig, ref := (go aig lhs).val.stream.getRef idx hidx }, assign.toAIGAssignment⟧ =
      (eval assign lhs).getLsb idx
rih :
  ∀ (aig : AIG BVBit) (idx : Nat) (hidx : idx < w✝),
    ⟦{ aig := (go aig rhs).val.aig, ref := (go aig rhs).val.stream.getRef idx hidx }, assign.toAIGAssignment⟧ =
      (eval assign rhs).getLsb idx
aig : AIG BVBit
idx : Nat
hidx : idx < w✝
⊢ (⟦{ aig := (bitblast (bitblast aig lhs).aig rhs).aig, ref := ((bitblast aig lhs).stream.getRef idx hidx).cast ⋯ },
        assign.toAIGAssignment⟧ &&
      (eval assign rhs).getLsb idx) =
    ((eval assign lhs).getLsb idx && (eval assign rhs).getLsb idx)
Tactic:
rw [AIG.LawfulStreamOperator.denote_input_stream (f := bitblast)]
State after:
case bin.and
w : Nat
assign : Assignment
w✝ : Nat
lhs rhs : BVExpr w✝
lih :
  ∀ (aig : AIG BVBit) (idx : Nat) (hidx : idx < w✝),
    ⟦{ aig := (go aig lhs).val.aig, ref := (go aig lhs).val.stream.getRef idx hidx }, assign.toAIGAssignment⟧ =
      (eval assign lhs).getLsb idx
rih :
  ∀ (aig : AIG BVBit) (idx : Nat) (hidx : idx < w✝),
    ⟦{ aig := (go aig rhs).val.aig, ref := (go aig rhs).val.stream.getRef idx hidx }, assign.toAIGAssignment⟧ =
      (eval assign rhs).getLsb idx
aig : AIG BVBit
idx : Nat
hidx : idx < w✝
⊢ (⟦{ aig := (bitblast aig lhs).aig, ref := (bitblast aig lhs).stream.getRef idx hidx }, assign.toAIGAssignment⟧ &&
      (eval assign rhs).getLsb idx) =
    ((eval assign lhs).getLsb idx && (eval assign rhs).getLsb idx)

State before:
case bin.and
w : Nat
assign : Assignment
w✝ : Nat
lhs rhs : BVExpr w✝
lih :
  ∀ (aig : AIG BVBit) (idx : Nat) (hidx : idx < w✝),
    ⟦{ aig := (go aig lhs).val.aig, ref := (go aig lhs).val.stream.getRef idx hidx }, assign.toAIGAssignment⟧ =
      (eval assign lhs).getLsb idx
rih :
  ∀ (aig : AIG BVBit) (idx : Nat) (hidx : idx < w✝),
    ⟦{ aig := (go aig rhs).val.aig, ref := (go aig rhs).val.stream.getRef idx hidx }, assign.toAIGAssignment⟧ =
      (eval assign rhs).getLsb idx
aig : AIG BVBit
idx : Nat
hidx : idx < w✝
⊢ (⟦{ aig := (bitblast aig lhs).aig, ref := (bitblast aig lhs).stream.getRef idx hidx }, assign.toAIGAssignment⟧ &&
      (eval assign rhs).getLsb idx) =
    ((eval assign lhs).getLsb idx && (eval assign rhs).getLsb idx)
Tactic:
rw [← go_val_eq_bitblast]
State after:
case bin.and
w : Nat
assign : Assignment
w✝ : Nat
lhs rhs : BVExpr w✝
lih :
  ∀ (aig : AIG BVBit) (idx : Nat) (hidx : idx < w✝),
    ⟦{ aig := (go aig lhs).val.aig, ref := (go aig lhs).val.stream.getRef idx hidx }, assign.toAIGAssignment⟧ =
      (eval assign lhs).getLsb idx
rih :
  ∀ (aig : AIG BVBit) (idx : Nat) (hidx : idx < w✝),
    ⟦{ aig := (go aig rhs).val.aig, ref := (go aig rhs).val.stream.getRef idx hidx }, assign.toAIGAssignment⟧ =
      (eval assign rhs).getLsb idx
aig : AIG BVBit
idx : Nat
hidx : idx < w✝
⊢ (⟦{ aig := (go aig lhs).val.aig, ref := (go aig lhs).val.stream.getRef idx hidx }, assign.toAIGAssignment⟧ &&
      (eval assign rhs).getLsb idx) =
    ((eval assign lhs).getLsb idx && (eval assign rhs).getLsb idx)

State before:
case bin.and
w : Nat
assign : Assignment
w✝ : Nat
lhs rhs : BVExpr w✝
lih :
  ∀ (aig : AIG BVBit) (idx : Nat) (hidx : idx < w✝),
    ⟦{ aig := (go aig lhs).val.aig, ref := (go aig lhs).val.stream.getRef idx hidx }, assign.toAIGAssignment⟧ =
      (eval assign lhs).getLsb idx
rih :
  ∀ (aig : AIG BVBit) (idx : Nat) (hidx : idx < w✝),
    ⟦{ aig := (go aig rhs).val.aig, ref := (go aig rhs).val.stream.getRef idx hidx }, assign.toAIGAssignment⟧ =
      (eval assign rhs).getLsb idx
aig : AIG BVBit
idx : Nat
hidx : idx < w✝
⊢ (⟦{ aig := (go aig lhs).val.aig, ref := (go aig lhs).val.stream.getRef idx hidx }, assign.toAIGAssignment⟧ &&
      (eval assign rhs).getLsb idx) =
    ((eval assign lhs).getLsb idx && (eval assign rhs).getLsb idx)
Tactic:
rw [lih]
State after:
no goals

State before:
case bin.or
w : Nat
assign : Assignment
w✝ : Nat
lhs rhs : BVExpr w✝
lih :
  ∀ (aig : AIG BVBit) (idx : Nat) (hidx : idx < w✝),
    ⟦{ aig := (go aig lhs).val.aig, ref := (go aig lhs).val.stream.getRef idx hidx }, assign.toAIGAssignment⟧ =
      (eval assign lhs).getLsb idx
rih :
  ∀ (aig : AIG BVBit) (idx : Nat) (hidx : idx < w✝),
    ⟦{ aig := (go aig rhs).val.aig, ref := (go aig rhs).val.stream.getRef idx hidx }, assign.toAIGAssignment⟧ =
      (eval assign rhs).getLsb idx
aig : AIG BVBit
idx : Nat
hidx : idx < w✝
⊢ ⟦{ aig := (go aig (lhs.bin BVBinOp.or rhs)).val.aig,
        ref := (go aig (lhs.bin BVBinOp.or rhs)).val.stream.getRef idx hidx },
      assign.toAIGAssignment⟧ =
    (eval assign (lhs.bin BVBinOp.or rhs)).getLsb idx
Tactic:
simp only [go, RefStream.denote_zip, denote_mkOrCached, rih, eval_bin, BVBinOp.eval_or,
  BitVec.getLsb_or]
State after:
case bin.or
w : Nat
assign : Assignment
w✝ : Nat
lhs rhs : BVExpr w✝
lih :
  ∀ (aig : AIG BVBit) (idx : Nat) (hidx : idx < w✝),
    ⟦{ aig := (go aig lhs).val.aig, ref := (go aig lhs).val.stream.getRef idx hidx }, assign.toAIGAssignment⟧ =
      (eval assign lhs).getLsb idx
rih :
  ∀ (aig : AIG BVBit) (idx : Nat) (hidx : idx < w✝),
    ⟦{ aig := (go aig rhs).val.aig, ref := (go aig rhs).val.stream.getRef idx hidx }, assign.toAIGAssignment⟧ =
      (eval assign rhs).getLsb idx
aig : AIG BVBit
idx : Nat
hidx : idx < w✝
⊢ (⟦{ aig := (go (go aig lhs).1.aig rhs).1.aig, ref := ((go aig lhs).1.stream.cast ⋯).getRef idx hidx },
        assign.toAIGAssignment⟧ ||
      (eval assign rhs).getLsb idx) =
    ((eval assign lhs).getLsb idx || (eval assign rhs).getLsb idx)

State before:
case bin.or
w : Nat
assign : Assignment
w✝ : Nat
lhs rhs : BVExpr w✝
lih :
  ∀ (aig : AIG BVBit) (idx : Nat) (hidx : idx < w✝),
    ⟦{ aig := (go aig lhs).val.aig, ref := (go aig lhs).val.stream.getRef idx hidx }, assign.toAIGAssignment⟧ =
      (eval assign lhs).getLsb idx
rih :
  ∀ (aig : AIG BVBit) (idx : Nat) (hidx : idx < w✝),
    ⟦{ aig := (go aig rhs).val.aig, ref := (go aig rhs).val.stream.getRef idx hidx }, assign.toAIGAssignment⟧ =
      (eval assign rhs).getLsb idx
aig : AIG BVBit
idx : Nat
hidx : idx < w✝
⊢ (⟦{ aig := (go (go aig lhs).1.aig rhs).1.aig, ref := ((go aig lhs).1.stream.cast ⋯).getRef idx hidx },
        assign.toAIGAssignment⟧ ||
      (eval assign rhs).getLsb idx) =
    ((eval assign lhs).getLsb idx || (eval assign rhs).getLsb idx)
Tactic:
simp only [go_val_eq_bitblast, RefStream.getRef_cast]
State after:
case bin.or
w : Nat
assign : Assignment
w✝ : Nat
lhs rhs : BVExpr w✝
lih :
  ∀ (aig : AIG BVBit) (idx : Nat) (hidx : idx < w✝),
    ⟦{ aig := (go aig lhs).val.aig, ref := (go aig lhs).val.stream.getRef idx hidx }, assign.toAIGAssignment⟧ =
      (eval assign lhs).getLsb idx
rih :
  ∀ (aig : AIG BVBit) (idx : Nat) (hidx : idx < w✝),
    ⟦{ aig := (go aig rhs).val.aig, ref := (go aig rhs).val.stream.getRef idx hidx }, assign.toAIGAssignment⟧ =
      (eval assign rhs).getLsb idx
aig : AIG BVBit
idx : Nat
hidx : idx < w✝
⊢ (⟦{ aig := (bitblast (bitblast aig lhs).aig rhs).aig, ref := ((bitblast aig lhs).stream.getRef idx hidx).cast ⋯ },
        assign.toAIGAssignment⟧ ||
      (eval assign rhs).getLsb idx) =
    ((eval assign lhs).getLsb idx || (eval assign rhs).getLsb idx)

State before:
case bin.or
w : Nat
assign : Assignment
w✝ : Nat
lhs rhs : BVExpr w✝
lih :
  ∀ (aig : AIG BVBit) (idx : Nat) (hidx : idx < w✝),
    ⟦{ aig := (go aig lhs).val.aig, ref := (go aig lhs).val.stream.getRef idx hidx }, assign.toAIGAssignment⟧ =
      (eval assign lhs).getLsb idx
rih :
  ∀ (aig : AIG BVBit) (idx : Nat) (hidx : idx < w✝),
    ⟦{ aig := (go aig rhs).val.aig, ref := (go aig rhs).val.stream.getRef idx hidx }, assign.toAIGAssignment⟧ =
      (eval assign rhs).getLsb idx
aig : AIG BVBit
idx : Nat
hidx : idx < w✝
⊢ (⟦{ aig := (bitblast (bitblast aig lhs).aig rhs).aig, ref := ((bitblast aig lhs).stream.getRef idx hidx).cast ⋯ },
        assign.toAIGAssignment⟧ ||
      (eval assign rhs).getLsb idx) =
    ((eval assign lhs).getLsb idx || (eval assign rhs).getLsb idx)
Tactic:
rw [AIG.LawfulStreamOperator.denote_input_stream (f := bitblast)]
State after:
case bin.or
w : Nat
assign : Assignment
w✝ : Nat
lhs rhs : BVExpr w✝
lih :
  ∀ (aig : AIG BVBit) (idx : Nat) (hidx : idx < w✝),
    ⟦{ aig := (go aig lhs).val.aig, ref := (go aig lhs).val.stream.getRef idx hidx }, assign.toAIGAssignment⟧ =
      (eval assign lhs).getLsb idx
rih :
  ∀ (aig : AIG BVBit) (idx : Nat) (hidx : idx < w✝),
    ⟦{ aig := (go aig rhs).val.aig, ref := (go aig rhs).val.stream.getRef idx hidx }, assign.toAIGAssignment⟧ =
      (eval assign rhs).getLsb idx
aig : AIG BVBit
idx : Nat
hidx : idx < w✝
⊢ (⟦{ aig := (bitblast aig lhs).aig, ref := (bitblast aig lhs).stream.getRef idx hidx }, assign.toAIGAssignment⟧ ||
      (eval assign rhs).getLsb idx) =
    ((eval assign lhs).getLsb idx || (eval assign rhs).getLsb idx)

State before:
case bin.or
w : Nat
assign : Assignment
w✝ : Nat
lhs rhs : BVExpr w✝
lih :
  ∀ (aig : AIG BVBit) (idx : Nat) (hidx : idx < w✝),
    ⟦{ aig := (go aig lhs).val.aig, ref := (go aig lhs).val.stream.getRef idx hidx }, assign.toAIGAssignment⟧ =
      (eval assign lhs).getLsb idx
rih :
  ∀ (aig : AIG BVBit) (idx : Nat) (hidx : idx < w✝),
    ⟦{ aig := (go aig rhs).val.aig, ref := (go aig rhs).val.stream.getRef idx hidx }, assign.toAIGAssignment⟧ =
      (eval assign rhs).getLsb idx
aig : AIG BVBit
idx : Nat
hidx : idx < w✝
⊢ (⟦{ aig := (bitblast aig lhs).aig, ref := (bitblast aig lhs).stream.getRef idx hidx }, assign.toAIGAssignment⟧ ||
      (eval assign rhs).getLsb idx) =
    ((eval assign lhs).getLsb idx || (eval assign rhs).getLsb idx)
Tactic:
rw [← go_val_eq_bitblast]
State after:
case bin.or
w : Nat
assign : Assignment
w✝ : Nat
lhs rhs : BVExpr w✝
lih :
  ∀ (aig : AIG BVBit) (idx : Nat) (hidx : idx < w✝),
    ⟦{ aig := (go aig lhs).val.aig, ref := (go aig lhs).val.stream.getRef idx hidx }, assign.toAIGAssignment⟧ =
      (eval assign lhs).getLsb idx
rih :
  ∀ (aig : AIG BVBit) (idx : Nat) (hidx : idx < w✝),
    ⟦{ aig := (go aig rhs).val.aig, ref := (go aig rhs).val.stream.getRef idx hidx }, assign.toAIGAssignment⟧ =
      (eval assign rhs).getLsb idx
aig : AIG BVBit
idx : Nat
hidx : idx < w✝
⊢ (⟦{ aig := (go aig lhs).val.aig, ref := (go aig lhs).val.stream.getRef idx hidx }, assign.toAIGAssignment⟧ ||
      (eval assign rhs).getLsb idx) =
    ((eval assign lhs).getLsb idx || (eval assign rhs).getLsb idx)

State before:
case bin.or
w : Nat
assign : Assignment
w✝ : Nat
lhs rhs : BVExpr w✝
lih :
  ∀ (aig : AIG BVBit) (idx : Nat) (hidx : idx < w✝),
    ⟦{ aig := (go aig lhs).val.aig, ref := (go aig lhs).val.stream.getRef idx hidx }, assign.toAIGAssignment⟧ =
      (eval assign lhs).getLsb idx
rih :
  ∀ (aig : AIG BVBit) (idx : Nat) (hidx : idx < w✝),
    ⟦{ aig := (go aig rhs).val.aig, ref := (go aig rhs).val.stream.getRef idx hidx }, assign.toAIGAssignment⟧ =
      (eval assign rhs).getLsb idx
aig : AIG BVBit
idx : Nat
hidx : idx < w✝
⊢ (⟦{ aig := (go aig lhs).val.aig, ref := (go aig lhs).val.stream.getRef idx hidx }, assign.toAIGAssignment⟧ ||
      (eval assign rhs).getLsb idx) =
    ((eval assign lhs).getLsb idx || (eval assign rhs).getLsb idx)
Tactic:
rw [lih]
State after:
no goals

State before:
case bin.xor
w : Nat
assign : Assignment
w✝ : Nat
lhs rhs : BVExpr w✝
lih :
  ∀ (aig : AIG BVBit) (idx : Nat) (hidx : idx < w✝),
    ⟦{ aig := (go aig lhs).val.aig, ref := (go aig lhs).val.stream.getRef idx hidx }, assign.toAIGAssignment⟧ =
      (eval assign lhs).getLsb idx
rih :
  ∀ (aig : AIG BVBit) (idx : Nat) (hidx : idx < w✝),
    ⟦{ aig := (go aig rhs).val.aig, ref := (go aig rhs).val.stream.getRef idx hidx }, assign.toAIGAssignment⟧ =
      (eval assign rhs).getLsb idx
aig : AIG BVBit
idx : Nat
hidx : idx < w✝
⊢ ⟦{ aig := (go aig (lhs.bin BVBinOp.xor rhs)).val.aig,
        ref := (go aig (lhs.bin BVBinOp.xor rhs)).val.stream.getRef idx hidx },
      assign.toAIGAssignment⟧ =
    (eval assign (lhs.bin BVBinOp.xor rhs)).getLsb idx
Tactic:
simp only [go, RefStream.denote_zip, denote_mkXorCached, rih, eval_bin, BVBinOp.eval_xor,
  BitVec.getLsb_xor]
State after:
case bin.xor
w : Nat
assign : Assignment
w✝ : Nat
lhs rhs : BVExpr w✝
lih :
  ∀ (aig : AIG BVBit) (idx : Nat) (hidx : idx < w✝),
    ⟦{ aig := (go aig lhs).val.aig, ref := (go aig lhs).val.stream.getRef idx hidx }, assign.toAIGAssignment⟧ =
      (eval assign lhs).getLsb idx
rih :
  ∀ (aig : AIG BVBit) (idx : Nat) (hidx : idx < w✝),
    ⟦{ aig := (go aig rhs).val.aig, ref := (go aig rhs).val.stream.getRef idx hidx }, assign.toAIGAssignment⟧ =
      (eval assign rhs).getLsb idx
aig : AIG BVBit
idx : Nat
hidx : idx < w✝
⊢ xor
      ⟦{ aig := (go (go aig lhs).1.aig rhs).1.aig, ref := ((go aig lhs).1.stream.cast ⋯).getRef idx hidx },
        assign.toAIGAssignment⟧
      ((eval assign rhs).getLsb idx) =
    xor ((eval assign lhs).getLsb idx) ((eval assign rhs).getLsb idx)

State before:
case bin.xor
w : Nat
assign : Assignment
w✝ : Nat
lhs rhs : BVExpr w✝
lih :
  ∀ (aig : AIG BVBit) (idx : Nat) (hidx : idx < w✝),
    ⟦{ aig := (go aig lhs).val.aig, ref := (go aig lhs).val.stream.getRef idx hidx }, assign.toAIGAssignment⟧ =
      (eval assign lhs).getLsb idx
rih :
  ∀ (aig : AIG BVBit) (idx : Nat) (hidx : idx < w✝),
    ⟦{ aig := (go aig rhs).val.aig, ref := (go aig rhs).val.stream.getRef idx hidx }, assign.toAIGAssignment⟧ =
      (eval assign rhs).getLsb idx
aig : AIG BVBit
idx : Nat
hidx : idx < w✝
⊢ xor
      ⟦{ aig := (go (go aig lhs).1.aig rhs).1.aig, ref := ((go aig lhs).1.stream.cast ⋯).getRef idx hidx },
        assign.toAIGAssignment⟧
      ((eval assign rhs).getLsb idx) =
    xor ((eval assign lhs).getLsb idx) ((eval assign rhs).getLsb idx)
Tactic:
simp only [go_val_eq_bitblast, RefStream.getRef_cast]
State after:
case bin.xor
w : Nat
assign : Assignment
w✝ : Nat
lhs rhs : BVExpr w✝
lih :
  ∀ (aig : AIG BVBit) (idx : Nat) (hidx : idx < w✝),
    ⟦{ aig := (go aig lhs).val.aig, ref := (go aig lhs).val.stream.getRef idx hidx }, assign.toAIGAssignment⟧ =
      (eval assign lhs).getLsb idx
rih :
  ∀ (aig : AIG BVBit) (idx : Nat) (hidx : idx < w✝),
    ⟦{ aig := (go aig rhs).val.aig, ref := (go aig rhs).val.stream.getRef idx hidx }, assign.toAIGAssignment⟧ =
      (eval assign rhs).getLsb idx
aig : AIG BVBit
idx : Nat
hidx : idx < w✝
⊢ xor
      ⟦{ aig := (bitblast (bitblast aig lhs).aig rhs).aig, ref := ((bitblast aig lhs).stream.getRef idx hidx).cast ⋯ },
        assign.toAIGAssignment⟧
      ((eval assign rhs).getLsb idx) =
    xor ((eval assign lhs).getLsb idx) ((eval assign rhs).getLsb idx)

State before:
case bin.xor
w : Nat
assign : Assignment
w✝ : Nat
lhs rhs : BVExpr w✝
lih :
  ∀ (aig : AIG BVBit) (idx : Nat) (hidx : idx < w✝),
    ⟦{ aig := (go aig lhs).val.aig, ref := (go aig lhs).val.stream.getRef idx hidx }, assign.toAIGAssignment⟧ =
      (eval assign lhs).getLsb idx
rih :
  ∀ (aig : AIG BVBit) (idx : Nat) (hidx : idx < w✝),
    ⟦{ aig := (go aig rhs).val.aig, ref := (go aig rhs).val.stream.getRef idx hidx }, assign.toAIGAssignment⟧ =
      (eval assign rhs).getLsb idx
aig : AIG BVBit
idx : Nat
hidx : idx < w✝
⊢ xor
      ⟦{ aig := (bitblast (bitblast aig lhs).aig rhs).aig, ref := ((bitblast aig lhs).stream.getRef idx hidx).cast ⋯ },
        assign.toAIGAssignment⟧
      ((eval assign rhs).getLsb idx) =
    xor ((eval assign lhs).getLsb idx) ((eval assign rhs).getLsb idx)
Tactic:
rw [AIG.LawfulStreamOperator.denote_input_stream (f := bitblast)]
State after:
case bin.xor
w : Nat
assign : Assignment
w✝ : Nat
lhs rhs : BVExpr w✝
lih :
  ∀ (aig : AIG BVBit) (idx : Nat) (hidx : idx < w✝),
    ⟦{ aig := (go aig lhs).val.aig, ref := (go aig lhs).val.stream.getRef idx hidx }, assign.toAIGAssignment⟧ =
      (eval assign lhs).getLsb idx
rih :
  ∀ (aig : AIG BVBit) (idx : Nat) (hidx : idx < w✝),
    ⟦{ aig := (go aig rhs).val.aig, ref := (go aig rhs).val.stream.getRef idx hidx }, assign.toAIGAssignment⟧ =
      (eval assign rhs).getLsb idx
aig : AIG BVBit
idx : Nat
hidx : idx < w✝
⊢ xor ⟦{ aig := (bitblast aig lhs).aig, ref := (bitblast aig lhs).stream.getRef idx hidx }, assign.toAIGAssignment⟧
      ((eval assign rhs).getLsb idx) =
    xor ((eval assign lhs).getLsb idx) ((eval assign rhs).getLsb idx)

State before:
case bin.xor
w : Nat
assign : Assignment
w✝ : Nat
lhs rhs : BVExpr w✝
lih :
  ∀ (aig : AIG BVBit) (idx : Nat) (hidx : idx < w✝),
    ⟦{ aig := (go aig lhs).val.aig, ref := (go aig lhs).val.stream.getRef idx hidx }, assign.toAIGAssignment⟧ =
      (eval assign lhs).getLsb idx
rih :
  ∀ (aig : AIG BVBit) (idx : Nat) (hidx : idx < w✝),
    ⟦{ aig := (go aig rhs).val.aig, ref := (go aig rhs).val.stream.getRef idx hidx }, assign.toAIGAssignment⟧ =
      (eval assign rhs).getLsb idx
aig : AIG BVBit
idx : Nat
hidx : idx < w✝
⊢ xor ⟦{ aig := (bitblast aig lhs).aig, ref := (bitblast aig lhs).stream.getRef idx hidx }, assign.toAIGAssignment⟧
      ((eval assign rhs).getLsb idx) =
    xor ((eval assign lhs).getLsb idx) ((eval assign rhs).getLsb idx)
Tactic:
rw [← go_val_eq_bitblast]
State after:
case bin.xor
w : Nat
assign : Assignment
w✝ : Nat
lhs rhs : BVExpr w✝
lih :
  ∀ (aig : AIG BVBit) (idx : Nat) (hidx : idx < w✝),
    ⟦{ aig := (go aig lhs).val.aig, ref := (go aig lhs).val.stream.getRef idx hidx }, assign.toAIGAssignment⟧ =
      (eval assign lhs).getLsb idx
rih :
  ∀ (aig : AIG BVBit) (idx : Nat) (hidx : idx < w✝),
    ⟦{ aig := (go aig rhs).val.aig, ref := (go aig rhs).val.stream.getRef idx hidx }, assign.toAIGAssignment⟧ =
      (eval assign rhs).getLsb idx
aig : AIG BVBit
idx : Nat
hidx : idx < w✝
⊢ xor ⟦{ aig := (go aig lhs).val.aig, ref := (go aig lhs).val.stream.getRef idx hidx }, assign.toAIGAssignment⟧
      ((eval assign rhs).getLsb idx) =
    xor ((eval assign lhs).getLsb idx) ((eval assign rhs).getLsb idx)

State before:
case bin.xor
w : Nat
assign : Assignment
w✝ : Nat
lhs rhs : BVExpr w✝
lih :
  ∀ (aig : AIG BVBit) (idx : Nat) (hidx : idx < w✝),
    ⟦{ aig := (go aig lhs).val.aig, ref := (go aig lhs).val.stream.getRef idx hidx }, assign.toAIGAssignment⟧ =
      (eval assign lhs).getLsb idx
rih :
  ∀ (aig : AIG BVBit) (idx : Nat) (hidx : idx < w✝),
    ⟦{ aig := (go aig rhs).val.aig, ref := (go aig rhs).val.stream.getRef idx hidx }, assign.toAIGAssignment⟧ =
      (eval assign rhs).getLsb idx
aig : AIG BVBit
idx : Nat
hidx : idx < w✝
⊢ xor ⟦{ aig := (go aig lhs).val.aig, ref := (go aig lhs).val.stream.getRef idx hidx }, assign.toAIGAssignment⟧
      ((eval assign rhs).getLsb idx) =
    xor ((eval assign lhs).getLsb idx) ((eval assign rhs).getLsb idx)
Tactic:
rw [lih]
State after:
no goals

State before:
case bin.add
w : Nat
assign : Assignment
w✝ : Nat
lhs rhs : BVExpr w✝
lih :
  ∀ (aig : AIG BVBit) (idx : Nat) (hidx : idx < w✝),
    ⟦{ aig := (go aig lhs).val.aig, ref := (go aig lhs).val.stream.getRef idx hidx }, assign.toAIGAssignment⟧ =
      (eval assign lhs).getLsb idx
rih :
  ∀ (aig : AIG BVBit) (idx : Nat) (hidx : idx < w✝),
    ⟦{ aig := (go aig rhs).val.aig, ref := (go aig rhs).val.stream.getRef idx hidx }, assign.toAIGAssignment⟧ =
      (eval assign rhs).getLsb idx
aig : AIG BVBit
idx : Nat
hidx : idx < w✝
⊢ ⟦{ aig := (go aig (lhs.bin BVBinOp.add rhs)).val.aig,
        ref := (go aig (lhs.bin BVBinOp.add rhs)).val.stream.getRef idx hidx },
      assign.toAIGAssignment⟧ =
    (eval assign (lhs.bin BVBinOp.add rhs)).getLsb idx
Tactic:
simp only [go, eval_bin, BVBinOp.eval_add]
State after:
case bin.add
w : Nat
assign : Assignment
w✝ : Nat
lhs rhs : BVExpr w✝
lih :
  ∀ (aig : AIG BVBit) (idx : Nat) (hidx : idx < w✝),
    ⟦{ aig := (go aig lhs).val.aig, ref := (go aig lhs).val.stream.getRef idx hidx }, assign.toAIGAssignment⟧ =
      (eval assign lhs).getLsb idx
rih :
  ∀ (aig : AIG BVBit) (idx : Nat) (hidx : idx < w✝),
    ⟦{ aig := (go aig rhs).val.aig, ref := (go aig rhs).val.stream.getRef idx hidx }, assign.toAIGAssignment⟧ =
      (eval assign rhs).getLsb idx
aig : AIG BVBit
idx : Nat
hidx : idx < w✝
⊢ ⟦{
        aig :=
          (blastAdd (go (go aig lhs).1.aig rhs).1.aig
              { lhs := (go aig lhs).1.stream.cast ⋯, rhs := (go (go aig lhs).1.aig rhs).1.stream }).aig,
        ref :=
          (blastAdd (go (go aig lhs).1.aig rhs).1.aig
                  { lhs := (go aig lhs).1.stream.cast ⋯, rhs := (go (go aig lhs).1.aig rhs).1.stream }).stream.getRef
            idx hidx },
      assign.toAIGAssignment⟧ =
    (eval assign lhs + eval assign rhs).getLsb idx

State before:
case bin.add
w : Nat
assign : Assignment
w✝ : Nat
lhs rhs : BVExpr w✝
lih :
  ∀ (aig : AIG BVBit) (idx : Nat) (hidx : idx < w✝),
    ⟦{ aig := (go aig lhs).val.aig, ref := (go aig lhs).val.stream.getRef idx hidx }, assign.toAIGAssignment⟧ =
      (eval assign lhs).getLsb idx
rih :
  ∀ (aig : AIG BVBit) (idx : Nat) (hidx : idx < w✝),
    ⟦{ aig := (go aig rhs).val.aig, ref := (go aig rhs).val.stream.getRef idx hidx }, assign.toAIGAssignment⟧ =
      (eval assign rhs).getLsb idx
aig : AIG BVBit
idx : Nat
hidx : idx < w✝
⊢ ⟦{
        aig :=
          (blastAdd (go (go aig lhs).1.aig rhs).1.aig
              { lhs := (go aig lhs).1.stream.cast ⋯, rhs := (go (go aig lhs).1.aig rhs).1.stream }).aig,
        ref :=
          (blastAdd (go (go aig lhs).1.aig rhs).1.aig
                  { lhs := (go aig lhs).1.stream.cast ⋯, rhs := (go (go aig lhs).1.aig rhs).1.stream }).stream.getRef
            idx hidx },
      assign.toAIGAssignment⟧ =
    (eval assign lhs + eval assign rhs).getLsb idx
Tactic:
apply blastAdd_eq_eval_getLsb
State after:
case bin.add.hleft
w : Nat
assign : Assignment
w✝ : Nat
lhs rhs : BVExpr w✝
lih :
  ∀ (aig : AIG BVBit) (idx : Nat) (hidx : idx < w✝),
    ⟦{ aig := (go aig lhs).val.aig, ref := (go aig lhs).val.stream.getRef idx hidx }, assign.toAIGAssignment⟧ =
      (eval assign lhs).getLsb idx
rih :
  ∀ (aig : AIG BVBit) (idx : Nat) (hidx : idx < w✝),
    ⟦{ aig := (go aig rhs).val.aig, ref := (go aig rhs).val.stream.getRef idx hidx }, assign.toAIGAssignment⟧ =
      (eval assign rhs).getLsb idx
aig : AIG BVBit
idx : Nat
hidx : idx < w✝
⊢ ∀ (idx : Nat) (hidx : idx < w✝),
    ⟦{ aig := (go (go aig lhs).1.aig rhs).1.aig,
          ref :=
            { lhs := (go aig lhs).1.stream.cast ⋯, rhs := (go (go aig lhs).1.aig rhs).1.stream }.lhs.getRef idx hidx },
        assign.toAIGAssignment⟧ =
      (eval assign lhs).getLsb idx

case bin.add.hright
w : Nat
assign : Assignment
w✝ : Nat
lhs rhs : BVExpr w✝
lih :
  ∀ (aig : AIG BVBit) (idx : Nat) (hidx : idx < w✝),
    ⟦{ aig := (go aig lhs).val.aig, ref := (go aig lhs).val.stream.getRef idx hidx }, assign.toAIGAssignment⟧ =
      (eval assign lhs).getLsb idx
rih :
  ∀ (aig : AIG BVBit) (idx : Nat) (hidx : idx < w✝),
    ⟦{ aig := (go aig rhs).val.aig, ref := (go aig rhs).val.stream.getRef idx hidx }, assign.toAIGAssignment⟧ =
      (eval assign rhs).getLsb idx
aig : AIG BVBit
idx : Nat
hidx : idx < w✝
⊢ ∀ (idx : Nat) (hidx : idx < w✝),
    ⟦{ aig := (go (go aig lhs).1.aig rhs).1.aig,
          ref :=
            { lhs := (go aig lhs).1.stream.cast ⋯, rhs := (go (go aig lhs).1.aig rhs).1.stream }.rhs.getRef idx hidx },
        assign.toAIGAssignment⟧ =
      (eval assign rhs).getLsb idx

State before:
case bin.add.hleft
w : Nat
assign : Assignment
w✝ : Nat
lhs rhs : BVExpr w✝
lih :
  ∀ (aig : AIG BVBit) (idx : Nat) (hidx : idx < w✝),
    ⟦{ aig := (go aig lhs).val.aig, ref := (go aig lhs).val.stream.getRef idx hidx }, assign.toAIGAssignment⟧ =
      (eval assign lhs).getLsb idx
rih :
  ∀ (aig : AIG BVBit) (idx : Nat) (hidx : idx < w✝),
    ⟦{ aig := (go aig rhs).val.aig, ref := (go aig rhs).val.stream.getRef idx hidx }, assign.toAIGAssignment⟧ =
      (eval assign rhs).getLsb idx
aig : AIG BVBit
idx : Nat
hidx : idx < w✝
⊢ ∀ (idx : Nat) (hidx : idx < w✝),
    ⟦{ aig := (go (go aig lhs).1.aig rhs).1.aig,
          ref :=
            { lhs := (go aig lhs).1.stream.cast ⋯, rhs := (go (go aig lhs).1.aig rhs).1.stream }.lhs.getRef idx hidx },
        assign.toAIGAssignment⟧ =
      (eval assign lhs).getLsb idx

case bin.add.hright
w : Nat
assign : Assignment
w✝ : Nat
lhs rhs : BVExpr w✝
lih :
  ∀ (aig : AIG BVBit) (idx : Nat) (hidx : idx < w✝),
    ⟦{ aig := (go aig lhs).val.aig, ref := (go aig lhs).val.stream.getRef idx hidx }, assign.toAIGAssignment⟧ =
      (eval assign lhs).getLsb idx
rih :
  ∀ (aig : AIG BVBit) (idx : Nat) (hidx : idx < w✝),
    ⟦{ aig := (go aig rhs).val.aig, ref := (go aig rhs).val.stream.getRef idx hidx }, assign.toAIGAssignment⟧ =
      (eval assign rhs).getLsb idx
aig : AIG BVBit
idx : Nat
hidx : idx < w✝
⊢ ∀ (idx : Nat) (hidx : idx < w✝),
    ⟦{ aig := (go (go aig lhs).1.aig rhs).1.aig,
          ref :=
            { lhs := (go aig lhs).1.stream.cast ⋯, rhs := (go (go aig lhs).1.aig rhs).1.stream }.rhs.getRef idx hidx },
        assign.toAIGAssignment⟧ =
      (eval assign rhs).getLsb idx
Tactic:
. intros
  dsimp
  rw [go_denote_mem_prefix]
  rw [← lih (aig := aig)]
  . simp
  . assumption
  . simp [Ref.hgate]
State after:
case bin.add.hright
w : Nat
assign : Assignment
w✝ : Nat
lhs rhs : BVExpr w✝
lih :
  ∀ (aig : AIG BVBit) (idx : Nat) (hidx : idx < w✝),
    ⟦{ aig := (go aig lhs).val.aig, ref := (go aig lhs).val.stream.getRef idx hidx }, assign.toAIGAssignment⟧ =
      (eval assign lhs).getLsb idx
rih :
  ∀ (aig : AIG BVBit) (idx : Nat) (hidx : idx < w✝),
    ⟦{ aig := (go aig rhs).val.aig, ref := (go aig rhs).val.stream.getRef idx hidx }, assign.toAIGAssignment⟧ =
      (eval assign rhs).getLsb idx
aig : AIG BVBit
idx : Nat
hidx : idx < w✝
⊢ ∀ (idx : Nat) (hidx : idx < w✝),
    ⟦{ aig := (go (go aig lhs).1.aig rhs).1.aig,
          ref :=
            { lhs := (go aig lhs).1.stream.cast ⋯, rhs := (go (go aig lhs).1.aig rhs).1.stream }.rhs.getRef idx hidx },
        assign.toAIGAssignment⟧ =
      (eval assign rhs).getLsb idx

State before:
case bin.add.hright
w : Nat
assign : Assignment
w✝ : Nat
lhs rhs : BVExpr w✝
lih :
  ∀ (aig : AIG BVBit) (idx : Nat) (hidx : idx < w✝),
    ⟦{ aig := (go aig lhs).val.aig, ref := (go aig lhs).val.stream.getRef idx hidx }, assign.toAIGAssignment⟧ =
      (eval assign lhs).getLsb idx
rih :
  ∀ (aig : AIG BVBit) (idx : Nat) (hidx : idx < w✝),
    ⟦{ aig := (go aig rhs).val.aig, ref := (go aig rhs).val.stream.getRef idx hidx }, assign.toAIGAssignment⟧ =
      (eval assign rhs).getLsb idx
aig : AIG BVBit
idx : Nat
hidx : idx < w✝
⊢ ∀ (idx : Nat) (hidx : idx < w✝),
    ⟦{ aig := (go (go aig lhs).1.aig rhs).1.aig,
          ref :=
            { lhs := (go aig lhs).1.stream.cast ⋯, rhs := (go (go aig lhs).1.aig rhs).1.stream }.rhs.getRef idx hidx },
        assign.toAIGAssignment⟧ =
      (eval assign rhs).getLsb idx
Tactic:
. intros
  rw [← rih]
State after:
no goals

State before:
case bin.add.hleft
w : Nat
assign : Assignment
w✝ : Nat
lhs rhs : BVExpr w✝
lih :
  ∀ (aig : AIG BVBit) (idx : Nat) (hidx : idx < w✝),
    ⟦{ aig := (go aig lhs).val.aig, ref := (go aig lhs).val.stream.getRef idx hidx }, assign.toAIGAssignment⟧ =
      (eval assign lhs).getLsb idx
rih :
  ∀ (aig : AIG BVBit) (idx : Nat) (hidx : idx < w✝),
    ⟦{ aig := (go aig rhs).val.aig, ref := (go aig rhs).val.stream.getRef idx hidx }, assign.toAIGAssignment⟧ =
      (eval assign rhs).getLsb idx
aig : AIG BVBit
idx : Nat
hidx : idx < w✝
⊢ ∀ (idx : Nat) (hidx : idx < w✝),
    ⟦{ aig := (go (go aig lhs).1.aig rhs).1.aig,
          ref :=
            { lhs := (go aig lhs).1.stream.cast ⋯, rhs := (go (go aig lhs).1.aig rhs).1.stream }.lhs.getRef idx hidx },
        assign.toAIGAssignment⟧ =
      (eval assign lhs).getLsb idx
Tactic:
intros
State after:
case bin.add.hleft
w : Nat
assign : Assignment
w✝ : Nat
lhs rhs : BVExpr w✝
lih :
  ∀ (aig : AIG BVBit) (idx : Nat) (hidx : idx < w✝),
    ⟦{ aig := (go aig lhs).val.aig, ref := (go aig lhs).val.stream.getRef idx hidx }, assign.toAIGAssignment⟧ =
      (eval assign lhs).getLsb idx
rih :
  ∀ (aig : AIG BVBit) (idx : Nat) (hidx : idx < w✝),
    ⟦{ aig := (go aig rhs).val.aig, ref := (go aig rhs).val.stream.getRef idx hidx }, assign.toAIGAssignment⟧ =
      (eval assign rhs).getLsb idx
aig : AIG BVBit
idx : Nat
hidx : idx < w✝
idx✝ : Nat
hidx✝ : idx✝ < w✝
⊢ ⟦{ aig := (go (go aig lhs).1.aig rhs).1.aig,
        ref :=
          { lhs := (go aig lhs).1.stream.cast ⋯, rhs := (go (go aig lhs).1.aig rhs).1.stream }.lhs.getRef idx✝ hidx✝ },
      assign.toAIGAssignment⟧ =
    (eval assign lhs).getLsb idx✝

State before:
case bin.add.hleft
w : Nat
assign : Assignment
w✝ : Nat
lhs rhs : BVExpr w✝
lih :
  ∀ (aig : AIG BVBit) (idx : Nat) (hidx : idx < w✝),
    ⟦{ aig := (go aig lhs).val.aig, ref := (go aig lhs).val.stream.getRef idx hidx }, assign.toAIGAssignment⟧ =
      (eval assign lhs).getLsb idx
rih :
  ∀ (aig : AIG BVBit) (idx : Nat) (hidx : idx < w✝),
    ⟦{ aig := (go aig rhs).val.aig, ref := (go aig rhs).val.stream.getRef idx hidx }, assign.toAIGAssignment⟧ =
      (eval assign rhs).getLsb idx
aig : AIG BVBit
idx : Nat
hidx : idx < w✝
idx✝ : Nat
hidx✝ : idx✝ < w✝
⊢ ⟦{ aig := (go (go aig lhs).1.aig rhs).1.aig,
        ref :=
          { lhs := (go aig lhs).1.stream.cast ⋯, rhs := (go (go aig lhs).1.aig rhs).1.stream }.lhs.getRef idx✝ hidx✝ },
      assign.toAIGAssignment⟧ =
    (eval assign lhs).getLsb idx✝
Tactic:
dsimp
State after:
case bin.add.hleft
w : Nat
assign : Assignment
w✝ : Nat
lhs rhs : BVExpr w✝
lih :
  ∀ (aig : AIG BVBit) (idx : Nat) (hidx : idx < w✝),
    ⟦{ aig := (go aig lhs).val.aig, ref := (go aig lhs).val.stream.getRef idx hidx }, assign.toAIGAssignment⟧ =
      (eval assign lhs).getLsb idx
rih :
  ∀ (aig : AIG BVBit) (idx : Nat) (hidx : idx < w✝),
    ⟦{ aig := (go aig rhs).val.aig, ref := (go aig rhs).val.stream.getRef idx hidx }, assign.toAIGAssignment⟧ =
      (eval assign rhs).getLsb idx
aig : AIG BVBit
idx : Nat
hidx : idx < w✝
idx✝ : Nat
hidx✝ : idx✝ < w✝
⊢ ⟦{ aig := (go (go aig lhs).1.aig rhs).1.aig, ref := ((go aig lhs).1.stream.cast ⋯).getRef idx✝ hidx✝ },
      assign.toAIGAssignment⟧ =
    (eval assign lhs).getLsb idx✝

State before:
case bin.add.hleft
w : Nat
assign : Assignment
w✝ : Nat
lhs rhs : BVExpr w✝
lih :
  ∀ (aig : AIG BVBit) (idx : Nat) (hidx : idx < w✝),
    ⟦{ aig := (go aig lhs).val.aig, ref := (go aig lhs).val.stream.getRef idx hidx }, assign.toAIGAssignment⟧ =
      (eval assign lhs).getLsb idx
rih :
  ∀ (aig : AIG BVBit) (idx : Nat) (hidx : idx < w✝),
    ⟦{ aig := (go aig rhs).val.aig, ref := (go aig rhs).val.stream.getRef idx hidx }, assign.toAIGAssignment⟧ =
      (eval assign rhs).getLsb idx
aig : AIG BVBit
idx : Nat
hidx : idx < w✝
idx✝ : Nat
hidx✝ : idx✝ < w✝
⊢ ⟦{ aig := (go (go aig lhs).1.aig rhs).1.aig, ref := ((go aig lhs).1.stream.cast ⋯).getRef idx✝ hidx✝ },
      assign.toAIGAssignment⟧ =
    (eval assign lhs).getLsb idx✝
Tactic:
rw [go_denote_mem_prefix]
State after:
case bin.add.hleft
w : Nat
assign : Assignment
w✝ : Nat
lhs rhs : BVExpr w✝
lih :
  ∀ (aig : AIG BVBit) (idx : Nat) (hidx : idx < w✝),
    ⟦{ aig := (go aig lhs).val.aig, ref := (go aig lhs).val.stream.getRef idx hidx }, assign.toAIGAssignment⟧ =
      (eval assign lhs).getLsb idx
rih :
  ∀ (aig : AIG BVBit) (idx : Nat) (hidx : idx < w✝),
    ⟦{ aig := (go aig rhs).val.aig, ref := (go aig rhs).val.stream.getRef idx hidx }, assign.toAIGAssignment⟧ =
      (eval assign rhs).getLsb idx
aig : AIG BVBit
idx : Nat
hidx : idx < w✝
idx✝ : Nat
hidx✝ : idx✝ < w✝
⊢ ⟦{ aig := (go aig lhs).1.aig,
        ref := { gate := (((go aig lhs).1.stream.cast ⋯).getRef idx✝ hidx✝).gate, hgate := ?bin.add.hleft.hstart } },
      assign.toAIGAssignment⟧ =
    (eval assign lhs).getLsb idx✝

case bin.add.hleft.hstart
w : Nat
assign : Assignment
w✝ : Nat
lhs rhs : BVExpr w✝
lih :
  ∀ (aig : AIG BVBit) (idx : Nat) (hidx : idx < w✝),
    ⟦{ aig := (go aig lhs).val.aig, ref := (go aig lhs).val.stream.getRef idx hidx }, assign.toAIGAssignment⟧ =
      (eval assign lhs).getLsb idx
rih :
  ∀ (aig : AIG BVBit) (idx : Nat) (hidx : idx < w✝),
    ⟦{ aig := (go aig rhs).val.aig, ref := (go aig rhs).val.stream.getRef idx hidx }, assign.toAIGAssignment⟧ =
      (eval assign rhs).getLsb idx
aig : AIG BVBit
idx : Nat
hidx : idx < w✝
idx✝ : Nat
hidx✝ : idx✝ < w✝
⊢ (((go aig lhs).1.stream.cast ⋯).getRef idx✝ hidx✝).gate < (go aig lhs).1.aig.decls.size

State before:
case bin.add.hleft
w : Nat
assign : Assignment
w✝ : Nat
lhs rhs : BVExpr w✝
lih :
  ∀ (aig : AIG BVBit) (idx : Nat) (hidx : idx < w✝),
    ⟦{ aig := (go aig lhs).val.aig, ref := (go aig lhs).val.stream.getRef idx hidx }, assign.toAIGAssignment⟧ =
      (eval assign lhs).getLsb idx
rih :
  ∀ (aig : AIG BVBit) (idx : Nat) (hidx : idx < w✝),
    ⟦{ aig := (go aig rhs).val.aig, ref := (go aig rhs).val.stream.getRef idx hidx }, assign.toAIGAssignment⟧ =
      (eval assign rhs).getLsb idx
aig : AIG BVBit
idx : Nat
hidx : idx < w✝
idx✝ : Nat
hidx✝ : idx✝ < w✝
⊢ ⟦{ aig := (go aig lhs).1.aig,
        ref := { gate := (((go aig lhs).1.stream.cast ⋯).getRef idx✝ hidx✝).gate, hgate := ?bin.add.hleft.hstart } },
      assign.toAIGAssignment⟧ =
    (eval assign lhs).getLsb idx✝

case bin.add.hleft.hstart
w : Nat
assign : Assignment
w✝ : Nat
lhs rhs : BVExpr w✝
lih :
  ∀ (aig : AIG BVBit) (idx : Nat) (hidx : idx < w✝),
    ⟦{ aig := (go aig lhs).val.aig, ref := (go aig lhs).val.stream.getRef idx hidx }, assign.toAIGAssignment⟧ =
      (eval assign lhs).getLsb idx
rih :
  ∀ (aig : AIG BVBit) (idx : Nat) (hidx : idx < w✝),
    ⟦{ aig := (go aig rhs).val.aig, ref := (go aig rhs).val.stream.getRef idx hidx }, assign.toAIGAssignment⟧ =
      (eval assign rhs).getLsb idx
aig : AIG BVBit
idx : Nat
hidx : idx < w✝
idx✝ : Nat
hidx✝ : idx✝ < w✝
⊢ (((go aig lhs).1.stream.cast ⋯).getRef idx✝ hidx✝).gate < (go aig lhs).1.aig.decls.size
Tactic:
rw [← lih (aig := aig)]
State after:
case bin.add.hleft
w : Nat
assign : Assignment
w✝ : Nat
lhs rhs : BVExpr w✝
lih :
  ∀ (aig : AIG BVBit) (idx : Nat) (hidx : idx < w✝),
    ⟦{ aig := (go aig lhs).val.aig, ref := (go aig lhs).val.stream.getRef idx hidx }, assign.toAIGAssignment⟧ =
      (eval assign lhs).getLsb idx
rih :
  ∀ (aig : AIG BVBit) (idx : Nat) (hidx : idx < w✝),
    ⟦{ aig := (go aig rhs).val.aig, ref := (go aig rhs).val.stream.getRef idx hidx }, assign.toAIGAssignment⟧ =
      (eval assign rhs).getLsb idx
aig : AIG BVBit
idx : Nat
hidx : idx < w✝
idx✝ : Nat
hidx✝ : idx✝ < w✝
⊢ ⟦{ aig := (go aig lhs).1.aig,
        ref := { gate := (((go aig lhs).1.stream.cast ⋯).getRef idx✝ hidx✝).gate, hgate := ?bin.add.hleft.hstart } },
      assign.toAIGAssignment⟧ =
    ⟦{ aig := (go aig lhs).val.aig, ref := (go aig lhs).val.stream.getRef idx✝ ?bin.add.hleft.hidx },
      assign.toAIGAssignment⟧

case bin.add.hleft.hidx
w : Nat
assign : Assignment
w✝ : Nat
lhs rhs : BVExpr w✝
lih :
  ∀ (aig : AIG BVBit) (idx : Nat) (hidx : idx < w✝),
    ⟦{ aig := (go aig lhs).val.aig, ref := (go aig lhs).val.stream.getRef idx hidx }, assign.toAIGAssignment⟧ =
      (eval assign lhs).getLsb idx
rih :
  ∀ (aig : AIG BVBit) (idx : Nat) (hidx : idx < w✝),
    ⟦{ aig := (go aig rhs).val.aig, ref := (go aig rhs).val.stream.getRef idx hidx }, assign.toAIGAssignment⟧ =
      (eval assign rhs).getLsb idx
aig : AIG BVBit
idx : Nat
hidx : idx < w✝
idx✝ : Nat
hidx✝ : idx✝ < w✝
⊢ idx✝ < w✝

case bin.add.hleft.hstart
w : Nat
assign : Assignment
w✝ : Nat
lhs rhs : BVExpr w✝
lih :
  ∀ (aig : AIG BVBit) (idx : Nat) (hidx : idx < w✝),
    ⟦{ aig := (go aig lhs).val.aig, ref := (go aig lhs).val.stream.getRef idx hidx }, assign.toAIGAssignment⟧ =
      (eval assign lhs).getLsb idx
rih :
  ∀ (aig : AIG BVBit) (idx : Nat) (hidx : idx < w✝),
    ⟦{ aig := (go aig rhs).val.aig, ref := (go aig rhs).val.stream.getRef idx hidx }, assign.toAIGAssignment⟧ =
      (eval assign rhs).getLsb idx
aig : AIG BVBit
idx : Nat
hidx : idx < w✝
idx✝ : Nat
hidx✝ : idx✝ < w✝
⊢ (((go aig lhs).1.stream.cast ⋯).getRef idx✝ hidx✝).gate < (go aig lhs).1.aig.decls.size

case bin.add.hleft.hstart
w : Nat
assign : Assignment
w✝ : Nat
lhs rhs : BVExpr w✝
lih :
  ∀ (aig : AIG BVBit) (idx : Nat) (hidx : idx < w✝),
    ⟦{ aig := (go aig lhs).val.aig, ref := (go aig lhs).val.stream.getRef idx hidx }, assign.toAIGAssignment⟧ =
      (eval assign lhs).getLsb idx
rih :
  ∀ (aig : AIG BVBit) (idx : Nat) (hidx : idx < w✝),
    ⟦{ aig := (go aig rhs).val.aig, ref := (go aig rhs).val.stream.getRef idx hidx }, assign.toAIGAssignment⟧ =
      (eval assign rhs).getLsb idx
aig : AIG BVBit
idx : Nat
hidx : idx < w✝
idx✝ : Nat
hidx✝ : idx✝ < w✝
⊢ (((go aig lhs).1.stream.cast ⋯).getRef idx✝ hidx✝).gate < (go aig lhs).1.aig.decls.size

State before:
case bin.add.hleft
w : Nat
assign : Assignment
w✝ : Nat
lhs rhs : BVExpr w✝
lih :
  ∀ (aig : AIG BVBit) (idx : Nat) (hidx : idx < w✝),
    ⟦{ aig := (go aig lhs).val.aig, ref := (go aig lhs).val.stream.getRef idx hidx }, assign.toAIGAssignment⟧ =
      (eval assign lhs).getLsb idx
rih :
  ∀ (aig : AIG BVBit) (idx : Nat) (hidx : idx < w✝),
    ⟦{ aig := (go aig rhs).val.aig, ref := (go aig rhs).val.stream.getRef idx hidx }, assign.toAIGAssignment⟧ =
      (eval assign rhs).getLsb idx
aig : AIG BVBit
idx : Nat
hidx : idx < w✝
idx✝ : Nat
hidx✝ : idx✝ < w✝
⊢ ⟦{ aig := (go aig lhs).1.aig,
        ref := { gate := (((go aig lhs).1.stream.cast ⋯).getRef idx✝ hidx✝).gate, hgate := ?bin.add.hleft.hstart } },
      assign.toAIGAssignment⟧ =
    ⟦{ aig := (go aig lhs).val.aig, ref := (go aig lhs).val.stream.getRef idx✝ ?bin.add.hleft.hidx },
      assign.toAIGAssignment⟧

case bin.add.hleft.hidx
w : Nat
assign : Assignment
w✝ : Nat
lhs rhs : BVExpr w✝
lih :
  ∀ (aig : AIG BVBit) (idx : Nat) (hidx : idx < w✝),
    ⟦{ aig := (go aig lhs).val.aig, ref := (go aig lhs).val.stream.getRef idx hidx }, assign.toAIGAssignment⟧ =
      (eval assign lhs).getLsb idx
rih :
  ∀ (aig : AIG BVBit) (idx : Nat) (hidx : idx < w✝),
    ⟦{ aig := (go aig rhs).val.aig, ref := (go aig rhs).val.stream.getRef idx hidx }, assign.toAIGAssignment⟧ =
      (eval assign rhs).getLsb idx
aig : AIG BVBit
idx : Nat
hidx : idx < w✝
idx✝ : Nat
hidx✝ : idx✝ < w✝
⊢ idx✝ < w✝

case bin.add.hleft.hstart
w : Nat
assign : Assignment
w✝ : Nat
lhs rhs : BVExpr w✝
lih :
  ∀ (aig : AIG BVBit) (idx : Nat) (hidx : idx < w✝),
    ⟦{ aig := (go aig lhs).val.aig, ref := (go aig lhs).val.stream.getRef idx hidx }, assign.toAIGAssignment⟧ =
      (eval assign lhs).getLsb idx
rih :
  ∀ (aig : AIG BVBit) (idx : Nat) (hidx : idx < w✝),
    ⟦{ aig := (go aig rhs).val.aig, ref := (go aig rhs).val.stream.getRef idx hidx }, assign.toAIGAssignment⟧ =
      (eval assign rhs).getLsb idx
aig : AIG BVBit
idx : Nat
hidx : idx < w✝
idx✝ : Nat
hidx✝ : idx✝ < w✝
⊢ (((go aig lhs).1.stream.cast ⋯).getRef idx✝ hidx✝).gate < (go aig lhs).1.aig.decls.size

case bin.add.hleft.hstart
w : Nat
assign : Assignment
w✝ : Nat
lhs rhs : BVExpr w✝
lih :
  ∀ (aig : AIG BVBit) (idx : Nat) (hidx : idx < w✝),
    ⟦{ aig := (go aig lhs).val.aig, ref := (go aig lhs).val.stream.getRef idx hidx }, assign.toAIGAssignment⟧ =
      (eval assign lhs).getLsb idx
rih :
  ∀ (aig : AIG BVBit) (idx : Nat) (hidx : idx < w✝),
    ⟦{ aig := (go aig rhs).val.aig, ref := (go aig rhs).val.stream.getRef idx hidx }, assign.toAIGAssignment⟧ =
      (eval assign rhs).getLsb idx
aig : AIG BVBit
idx : Nat
hidx : idx < w✝
idx✝ : Nat
hidx✝ : idx✝ < w✝
⊢ (((go aig lhs).1.stream.cast ⋯).getRef idx✝ hidx✝).gate < (go aig lhs).1.aig.decls.size
Tactic:
. simp
State after:
case bin.add.hleft.hidx
w : Nat
assign : Assignment
w✝ : Nat
lhs rhs : BVExpr w✝
lih :
  ∀ (aig : AIG BVBit) (idx : Nat) (hidx : idx < w✝),
    ⟦{ aig := (go aig lhs).val.aig, ref := (go aig lhs).val.stream.getRef idx hidx }, assign.toAIGAssignment⟧ =
      (eval assign lhs).getLsb idx
rih :
  ∀ (aig : AIG BVBit) (idx : Nat) (hidx : idx < w✝),
    ⟦{ aig := (go aig rhs).val.aig, ref := (go aig rhs).val.stream.getRef idx hidx }, assign.toAIGAssignment⟧ =
      (eval assign rhs).getLsb idx
aig : AIG BVBit
idx : Nat
hidx : idx < w✝
idx✝ : Nat
hidx✝ : idx✝ < w✝
⊢ idx✝ < w✝

case bin.add.hleft.hstart
w : Nat
assign : Assignment
w✝ : Nat
lhs rhs : BVExpr w✝
lih :
  ∀ (aig : AIG BVBit) (idx : Nat) (hidx : idx < w✝),
    ⟦{ aig := (go aig lhs).val.aig, ref := (go aig lhs).val.stream.getRef idx hidx }, assign.toAIGAssignment⟧ =
      (eval assign lhs).getLsb idx
rih :
  ∀ (aig : AIG BVBit) (idx : Nat) (hidx : idx < w✝),
    ⟦{ aig := (go aig rhs).val.aig, ref := (go aig rhs).val.stream.getRef idx hidx }, assign.toAIGAssignment⟧ =
      (eval assign rhs).getLsb idx
aig : AIG BVBit
idx : Nat
hidx : idx < w✝
idx✝ : Nat
hidx✝ : idx✝ < w✝
⊢ (((go aig lhs).1.stream.cast ⋯).getRef idx✝ hidx✝).gate < (go aig lhs).1.aig.decls.size

case bin.add.hleft.hstart
w : Nat
assign : Assignment
w✝ : Nat
lhs rhs : BVExpr w✝
lih :
  ∀ (aig : AIG BVBit) (idx : Nat) (hidx : idx < w✝),
    ⟦{ aig := (go aig lhs).val.aig, ref := (go aig lhs).val.stream.getRef idx hidx }, assign.toAIGAssignment⟧ =
      (eval assign lhs).getLsb idx
rih :
  ∀ (aig : AIG BVBit) (idx : Nat) (hidx : idx < w✝),
    ⟦{ aig := (go aig rhs).val.aig, ref := (go aig rhs).val.stream.getRef idx hidx }, assign.toAIGAssignment⟧ =
      (eval assign rhs).getLsb idx
aig : AIG BVBit
idx : Nat
hidx : idx < w✝
idx✝ : Nat
hidx✝ : idx✝ < w✝
⊢ (((go aig lhs).1.stream.cast ⋯).getRef idx✝ hidx✝).gate < (go aig lhs).1.aig.decls.size

State before:
case bin.add.hleft.hidx
w : Nat
assign : Assignment
w✝ : Nat
lhs rhs : BVExpr w✝
lih :
  ∀ (aig : AIG BVBit) (idx : Nat) (hidx : idx < w✝),
    ⟦{ aig := (go aig lhs).val.aig, ref := (go aig lhs).val.stream.getRef idx hidx }, assign.toAIGAssignment⟧ =
      (eval assign lhs).getLsb idx
rih :
  ∀ (aig : AIG BVBit) (idx : Nat) (hidx : idx < w✝),
    ⟦{ aig := (go aig rhs).val.aig, ref := (go aig rhs).val.stream.getRef idx hidx }, assign.toAIGAssignment⟧ =
      (eval assign rhs).getLsb idx
aig : AIG BVBit
idx : Nat
hidx : idx < w✝
idx✝ : Nat
hidx✝ : idx✝ < w✝
⊢ idx✝ < w✝

case bin.add.hleft.hstart
w : Nat
assign : Assignment
w✝ : Nat
lhs rhs : BVExpr w✝
lih :
  ∀ (aig : AIG BVBit) (idx : Nat) (hidx : idx < w✝),
    ⟦{ aig := (go aig lhs).val.aig, ref := (go aig lhs).val.stream.getRef idx hidx }, assign.toAIGAssignment⟧ =
      (eval assign lhs).getLsb idx
rih :
  ∀ (aig : AIG BVBit) (idx : Nat) (hidx : idx < w✝),
    ⟦{ aig := (go aig rhs).val.aig, ref := (go aig rhs).val.stream.getRef idx hidx }, assign.toAIGAssignment⟧ =
      (eval assign rhs).getLsb idx
aig : AIG BVBit
idx : Nat
hidx : idx < w✝
idx✝ : Nat
hidx✝ : idx✝ < w✝
⊢ (((go aig lhs).1.stream.cast ⋯).getRef idx✝ hidx✝).gate < (go aig lhs).1.aig.decls.size

case bin.add.hleft.hstart
w : Nat
assign : Assignment
w✝ : Nat
lhs rhs : BVExpr w✝
lih :
  ∀ (aig : AIG BVBit) (idx : Nat) (hidx : idx < w✝),
    ⟦{ aig := (go aig lhs).val.aig, ref := (go aig lhs).val.stream.getRef idx hidx }, assign.toAIGAssignment⟧ =
      (eval assign lhs).getLsb idx
rih :
  ∀ (aig : AIG BVBit) (idx : Nat) (hidx : idx < w✝),
    ⟦{ aig := (go aig rhs).val.aig, ref := (go aig rhs).val.stream.getRef idx hidx }, assign.toAIGAssignment⟧ =
      (eval assign rhs).getLsb idx
aig : AIG BVBit
idx : Nat
hidx : idx < w✝
idx✝ : Nat
hidx✝ : idx✝ < w✝
⊢ (((go aig lhs).1.stream.cast ⋯).getRef idx✝ hidx✝).gate < (go aig lhs).1.aig.decls.size
Tactic:
. assumption
State after:
case bin.add.hleft.hstart
w : Nat
assign : Assignment
w✝ : Nat
lhs rhs : BVExpr w✝
lih :
  ∀ (aig : AIG BVBit) (idx : Nat) (hidx : idx < w✝),
    ⟦{ aig := (go aig lhs).val.aig, ref := (go aig lhs).val.stream.getRef idx hidx }, assign.toAIGAssignment⟧ =
      (eval assign lhs).getLsb idx
rih :
  ∀ (aig : AIG BVBit) (idx : Nat) (hidx : idx < w✝),
    ⟦{ aig := (go aig rhs).val.aig, ref := (go aig rhs).val.stream.getRef idx hidx }, assign.toAIGAssignment⟧ =
      (eval assign rhs).getLsb idx
aig : AIG BVBit
idx : Nat
hidx : idx < w✝
idx✝ : Nat
hidx✝ : idx✝ < w✝
⊢ (((go aig lhs).1.stream.cast ⋯).getRef idx✝ hidx✝).gate < (go aig lhs).1.aig.decls.size

case bin.add.hleft.hstart
w : Nat
assign : Assignment
w✝ : Nat
lhs rhs : BVExpr w✝
lih :
  ∀ (aig : AIG BVBit) (idx : Nat) (hidx : idx < w✝),
    ⟦{ aig := (go aig lhs).val.aig, ref := (go aig lhs).val.stream.getRef idx hidx }, assign.toAIGAssignment⟧ =
      (eval assign lhs).getLsb idx
rih :
  ∀ (aig : AIG BVBit) (idx : Nat) (hidx : idx < w✝),
    ⟦{ aig := (go aig rhs).val.aig, ref := (go aig rhs).val.stream.getRef idx hidx }, assign.toAIGAssignment⟧ =
      (eval assign rhs).getLsb idx
aig : AIG BVBit
idx : Nat
hidx : idx < w✝
idx✝ : Nat
hidx✝ : idx✝ < w✝
⊢ (((go aig lhs).1.stream.cast ⋯).getRef idx✝ hidx✝).gate < (go aig lhs).1.aig.decls.size

State before:
case bin.add.hleft.hstart
w : Nat
assign : Assignment
w✝ : Nat
lhs rhs : BVExpr w✝
lih :
  ∀ (aig : AIG BVBit) (idx : Nat) (hidx : idx < w✝),
    ⟦{ aig := (go aig lhs).val.aig, ref := (go aig lhs).val.stream.getRef idx hidx }, assign.toAIGAssignment⟧ =
      (eval assign lhs).getLsb idx
rih :
  ∀ (aig : AIG BVBit) (idx : Nat) (hidx : idx < w✝),
    ⟦{ aig := (go aig rhs).val.aig, ref := (go aig rhs).val.stream.getRef idx hidx }, assign.toAIGAssignment⟧ =
      (eval assign rhs).getLsb idx
aig : AIG BVBit
idx : Nat
hidx : idx < w✝
idx✝ : Nat
hidx✝ : idx✝ < w✝
⊢ (((go aig lhs).1.stream.cast ⋯).getRef idx✝ hidx✝).gate < (go aig lhs).1.aig.decls.size

case bin.add.hleft.hstart
w : Nat
assign : Assignment
w✝ : Nat
lhs rhs : BVExpr w✝
lih :
  ∀ (aig : AIG BVBit) (idx : Nat) (hidx : idx < w✝),
    ⟦{ aig := (go aig lhs).val.aig, ref := (go aig lhs).val.stream.getRef idx hidx }, assign.toAIGAssignment⟧ =
      (eval assign lhs).getLsb idx
rih :
  ∀ (aig : AIG BVBit) (idx : Nat) (hidx : idx < w✝),
    ⟦{ aig := (go aig rhs).val.aig, ref := (go aig rhs).val.stream.getRef idx hidx }, assign.toAIGAssignment⟧ =
      (eval assign rhs).getLsb idx
aig : AIG BVBit
idx : Nat
hidx : idx < w✝
idx✝ : Nat
hidx✝ : idx✝ < w✝
⊢ (((go aig lhs).1.stream.cast ⋯).getRef idx✝ hidx✝).gate < (go aig lhs).1.aig.decls.size
Tactic:
. simp [Ref.hgate]
State after:
no goals

State before:
case bin.add.hleft
w : Nat
assign : Assignment
w✝ : Nat
lhs rhs : BVExpr w✝
lih :
  ∀ (aig : AIG BVBit) (idx : Nat) (hidx : idx < w✝),
    ⟦{ aig := (go aig lhs).val.aig, ref := (go aig lhs).val.stream.getRef idx hidx }, assign.toAIGAssignment⟧ =
      (eval assign lhs).getLsb idx
rih :
  ∀ (aig : AIG BVBit) (idx : Nat) (hidx : idx < w✝),
    ⟦{ aig := (go aig rhs).val.aig, ref := (go aig rhs).val.stream.getRef idx hidx }, assign.toAIGAssignment⟧ =
      (eval assign rhs).getLsb idx
aig : AIG BVBit
idx : Nat
hidx : idx < w✝
idx✝ : Nat
hidx✝ : idx✝ < w✝
⊢ ⟦{ aig := (go aig lhs).1.aig,
        ref := { gate := (((go aig lhs).1.stream.cast ⋯).getRef idx✝ hidx✝).gate, hgate := ?bin.add.hleft.hstart } },
      assign.toAIGAssignment⟧ =
    ⟦{ aig := (go aig lhs).val.aig, ref := (go aig lhs).val.stream.getRef idx✝ ?bin.add.hleft.hidx },
      assign.toAIGAssignment⟧
Tactic:
simp
State after:
no goals

State before:
case bin.add.hleft.hidx
w : Nat
assign : Assignment
w✝ : Nat
lhs rhs : BVExpr w✝
lih :
  ∀ (aig : AIG BVBit) (idx : Nat) (hidx : idx < w✝),
    ⟦{ aig := (go aig lhs).val.aig, ref := (go aig lhs).val.stream.getRef idx hidx }, assign.toAIGAssignment⟧ =
      (eval assign lhs).getLsb idx
rih :
  ∀ (aig : AIG BVBit) (idx : Nat) (hidx : idx < w✝),
    ⟦{ aig := (go aig rhs).val.aig, ref := (go aig rhs).val.stream.getRef idx hidx }, assign.toAIGAssignment⟧ =
      (eval assign rhs).getLsb idx
aig : AIG BVBit
idx : Nat
hidx : idx < w✝
idx✝ : Nat
hidx✝ : idx✝ < w✝
⊢ idx✝ < w✝
Tactic:
assumption
State after:
no goals

State before:
case bin.add.hleft.hstart
w : Nat
assign : Assignment
w✝ : Nat
lhs rhs : BVExpr w✝
lih :
  ∀ (aig : AIG BVBit) (idx : Nat) (hidx : idx < w✝),
    ⟦{ aig := (go aig lhs).val.aig, ref := (go aig lhs).val.stream.getRef idx hidx }, assign.toAIGAssignment⟧ =
      (eval assign lhs).getLsb idx
rih :
  ∀ (aig : AIG BVBit) (idx : Nat) (hidx : idx < w✝),
    ⟦{ aig := (go aig rhs).val.aig, ref := (go aig rhs).val.stream.getRef idx hidx }, assign.toAIGAssignment⟧ =
      (eval assign rhs).getLsb idx
aig : AIG BVBit
idx : Nat
hidx : idx < w✝
idx✝ : Nat
hidx✝ : idx✝ < w✝
⊢ (((go aig lhs).1.stream.cast ⋯).getRef idx✝ hidx✝).gate < (go aig lhs).1.aig.decls.size
Tactic:
simp [Ref.hgate]
State after:
no goals

State before:
case bin.add.hright
w : Nat
assign : Assignment
w✝ : Nat
lhs rhs : BVExpr w✝
lih :
  ∀ (aig : AIG BVBit) (idx : Nat) (hidx : idx < w✝),
    ⟦{ aig := (go aig lhs).val.aig, ref := (go aig lhs).val.stream.getRef idx hidx }, assign.toAIGAssignment⟧ =
      (eval assign lhs).getLsb idx
rih :
  ∀ (aig : AIG BVBit) (idx : Nat) (hidx : idx < w✝),
    ⟦{ aig := (go aig rhs).val.aig, ref := (go aig rhs).val.stream.getRef idx hidx }, assign.toAIGAssignment⟧ =
      (eval assign rhs).getLsb idx
aig : AIG BVBit
idx : Nat
hidx : idx < w✝
⊢ ∀ (idx : Nat) (hidx : idx < w✝),
    ⟦{ aig := (go (go aig lhs).1.aig rhs).1.aig,
          ref :=
            { lhs := (go aig lhs).1.stream.cast ⋯, rhs := (go (go aig lhs).1.aig rhs).1.stream }.rhs.getRef idx hidx },
        assign.toAIGAssignment⟧ =
      (eval assign rhs).getLsb idx
Tactic:
intros
State after:
case bin.add.hright
w : Nat
assign : Assignment
w✝ : Nat
lhs rhs : BVExpr w✝
lih :
  ∀ (aig : AIG BVBit) (idx : Nat) (hidx : idx < w✝),
    ⟦{ aig := (go aig lhs).val.aig, ref := (go aig lhs).val.stream.getRef idx hidx }, assign.toAIGAssignment⟧ =
      (eval assign lhs).getLsb idx
rih :
  ∀ (aig : AIG BVBit) (idx : Nat) (hidx : idx < w✝),
    ⟦{ aig := (go aig rhs).val.aig, ref := (go aig rhs).val.stream.getRef idx hidx }, assign.toAIGAssignment⟧ =
      (eval assign rhs).getLsb idx
aig : AIG BVBit
idx : Nat
hidx : idx < w✝
idx✝ : Nat
hidx✝ : idx✝ < w✝
⊢ ⟦{ aig := (go (go aig lhs).1.aig rhs).1.aig,
        ref :=
          { lhs := (go aig lhs).1.stream.cast ⋯, rhs := (go (go aig lhs).1.aig rhs).1.stream }.rhs.getRef idx✝ hidx✝ },
      assign.toAIGAssignment⟧ =
    (eval assign rhs).getLsb idx✝

State before:
case bin.add.hright
w : Nat
assign : Assignment
w✝ : Nat
lhs rhs : BVExpr w✝
lih :
  ∀ (aig : AIG BVBit) (idx : Nat) (hidx : idx < w✝),
    ⟦{ aig := (go aig lhs).val.aig, ref := (go aig lhs).val.stream.getRef idx hidx }, assign.toAIGAssignment⟧ =
      (eval assign lhs).getLsb idx
rih :
  ∀ (aig : AIG BVBit) (idx : Nat) (hidx : idx < w✝),
    ⟦{ aig := (go aig rhs).val.aig, ref := (go aig rhs).val.stream.getRef idx hidx }, assign.toAIGAssignment⟧ =
      (eval assign rhs).getLsb idx
aig : AIG BVBit
idx : Nat
hidx : idx < w✝
idx✝ : Nat
hidx✝ : idx✝ < w✝
⊢ ⟦{ aig := (go (go aig lhs).1.aig rhs).1.aig,
        ref :=
          { lhs := (go aig lhs).1.stream.cast ⋯, rhs := (go (go aig lhs).1.aig rhs).1.stream }.rhs.getRef idx✝ hidx✝ },
      assign.toAIGAssignment⟧ =
    (eval assign rhs).getLsb idx✝
Tactic:
rw [← rih]
State after:
no goals

State before:
case un
w : Nat
assign : Assignment
w✝ : Nat
op : BVUnOp
expr : BVExpr w✝
ih :
  ∀ (aig : AIG BVBit) (idx : Nat) (hidx : idx < w✝),
    ⟦{ aig := (go aig expr).val.aig, ref := (go aig expr).val.stream.getRef idx hidx }, assign.toAIGAssignment⟧ =
      (eval assign expr).getLsb idx
aig : AIG BVBit
idx : Nat
hidx : idx < w✝
⊢ ⟦{ aig := (go aig (un op expr)).val.aig, ref := (go aig (un op expr)).val.stream.getRef idx hidx },
      assign.toAIGAssignment⟧ =
    (eval assign (un op expr)).getLsb idx
Tactic:
cases op with
| not => simp [go, ih, hidx]
| shiftLeftConst => simp [go, ih, hidx]
| shiftRightConst =>
  simp only [go, blastShiftRight_eq_eval_getLsb, ih, dite_eq_ite, Bool.if_false_right, eval_un,
    BVUnOp.eval_shiftRightConst, BitVec.getLsb_ushiftRight, Bool.and_iff_right_iff_imp,
    decide_eq_true_eq]
  intro h
  apply BitVec.lt_of_getLsb
  assumption
| rotateLeft => simp [go, ih, hidx]
| rotateRight => simp [go, ih, hidx]
| arithShiftRightConst n =>
  rename_i w
  have : ¬(w ≤ idx) := by omega
  simp [go, ih, this, BitVec.getLsb_sshiftRight, BitVec.msb_eq_getLsb_last ]
State after:
no goals

State before:
case un.not
w : Nat
assign : Assignment
w✝ : Nat
expr : BVExpr w✝
ih :
  ∀ (aig : AIG BVBit) (idx : Nat) (hidx : idx < w✝),
    ⟦{ aig := (go aig expr).val.aig, ref := (go aig expr).val.stream.getRef idx hidx }, assign.toAIGAssignment⟧ =
      (eval assign expr).getLsb idx
aig : AIG BVBit
idx : Nat
hidx : idx < w✝
⊢ ⟦{ aig := (go aig (un BVUnOp.not expr)).val.aig, ref := (go aig (un BVUnOp.not expr)).val.stream.getRef idx hidx },
      assign.toAIGAssignment⟧ =
    (eval assign (un BVUnOp.not expr)).getLsb idx
Tactic:
simp [go, ih, hidx]
State after:
no goals

State before:
case un.shiftLeftConst
w : Nat
assign : Assignment
w✝ : Nat
expr : BVExpr w✝
ih :
  ∀ (aig : AIG BVBit) (idx : Nat) (hidx : idx < w✝),
    ⟦{ aig := (go aig expr).val.aig, ref := (go aig expr).val.stream.getRef idx hidx }, assign.toAIGAssignment⟧ =
      (eval assign expr).getLsb idx
aig : AIG BVBit
idx : Nat
hidx : idx < w✝
n✝ : Nat
⊢ ⟦{ aig := (go aig (un (BVUnOp.shiftLeftConst n✝) expr)).val.aig,
        ref := (go aig (un (BVUnOp.shiftLeftConst n✝) expr)).val.stream.getRef idx hidx },
      assign.toAIGAssignment⟧ =
    (eval assign (un (BVUnOp.shiftLeftConst n✝) expr)).getLsb idx
Tactic:
simp [go, ih, hidx]
State after:
no goals

State before:
case un.shiftRightConst
w : Nat
assign : Assignment
w✝ : Nat
expr : BVExpr w✝
ih :
  ∀ (aig : AIG BVBit) (idx : Nat) (hidx : idx < w✝),
    ⟦{ aig := (go aig expr).val.aig, ref := (go aig expr).val.stream.getRef idx hidx }, assign.toAIGAssignment⟧ =
      (eval assign expr).getLsb idx
aig : AIG BVBit
idx : Nat
hidx : idx < w✝
n✝ : Nat
⊢ ⟦{ aig := (go aig (un (BVUnOp.shiftRightConst n✝) expr)).val.aig,
        ref := (go aig (un (BVUnOp.shiftRightConst n✝) expr)).val.stream.getRef idx hidx },
      assign.toAIGAssignment⟧ =
    (eval assign (un (BVUnOp.shiftRightConst n✝) expr)).getLsb idx
Tactic:
simp only [go, blastShiftRight_eq_eval_getLsb, ih, dite_eq_ite, Bool.if_false_right, eval_un,
  BVUnOp.eval_shiftRightConst, BitVec.getLsb_ushiftRight, Bool.and_iff_right_iff_imp,
  decide_eq_true_eq]
State after:
case un.shiftRightConst
w : Nat
assign : Assignment
w✝ : Nat
expr : BVExpr w✝
ih :
  ∀ (aig : AIG BVBit) (idx : Nat) (hidx : idx < w✝),
    ⟦{ aig := (go aig expr).val.aig, ref := (go aig expr).val.stream.getRef idx hidx }, assign.toAIGAssignment⟧ =
      (eval assign expr).getLsb idx
aig : AIG BVBit
idx : Nat
hidx : idx < w✝
n✝ : Nat
⊢ (eval assign expr).getLsb (n✝ + idx) = true → n✝ + idx < w✝

State before:
case un.shiftRightConst
w : Nat
assign : Assignment
w✝ : Nat
expr : BVExpr w✝
ih :
  ∀ (aig : AIG BVBit) (idx : Nat) (hidx : idx < w✝),
    ⟦{ aig := (go aig expr).val.aig, ref := (go aig expr).val.stream.getRef idx hidx }, assign.toAIGAssignment⟧ =
      (eval assign expr).getLsb idx
aig : AIG BVBit
idx : Nat
hidx : idx < w✝
n✝ : Nat
⊢ (eval assign expr).getLsb (n✝ + idx) = true → n✝ + idx < w✝
Tactic:
intro h
State after:
case un.shiftRightConst
w : Nat
assign : Assignment
w✝ : Nat
expr : BVExpr w✝
ih :
  ∀ (aig : AIG BVBit) (idx : Nat) (hidx : idx < w✝),
    ⟦{ aig := (go aig expr).val.aig, ref := (go aig expr).val.stream.getRef idx hidx }, assign.toAIGAssignment⟧ =
      (eval assign expr).getLsb idx
aig : AIG BVBit
idx : Nat
hidx : idx < w✝
n✝ : Nat
h : (eval assign expr).getLsb (n✝ + idx) = true
⊢ n✝ + idx < w✝

State before:
case un.shiftRightConst
w : Nat
assign : Assignment
w✝ : Nat
expr : BVExpr w✝
ih :
  ∀ (aig : AIG BVBit) (idx : Nat) (hidx : idx < w✝),
    ⟦{ aig := (go aig expr).val.aig, ref := (go aig expr).val.stream.getRef idx hidx }, assign.toAIGAssignment⟧ =
      (eval assign expr).getLsb idx
aig : AIG BVBit
idx : Nat
hidx : idx < w✝
n✝ : Nat
h : (eval assign expr).getLsb (n✝ + idx) = true
⊢ n✝ + idx < w✝
Tactic:
apply BitVec.lt_of_getLsb
State after:
case un.shiftRightConst.a
w : Nat
assign : Assignment
w✝ : Nat
expr : BVExpr w✝
ih :
  ∀ (aig : AIG BVBit) (idx : Nat) (hidx : idx < w✝),
    ⟦{ aig := (go aig expr).val.aig, ref := (go aig expr).val.stream.getRef idx hidx }, assign.toAIGAssignment⟧ =
      (eval assign expr).getLsb idx
aig : AIG BVBit
idx : Nat
hidx : idx < w✝
n✝ : Nat
h : (eval assign expr).getLsb (n✝ + idx) = true
⊢ ?un.shiftRightConst.x.getLsb (n✝ + idx) = true

case un.shiftRightConst.x
w : Nat
assign : Assignment
w✝ : Nat
expr : BVExpr w✝
ih :
  ∀ (aig : AIG BVBit) (idx : Nat) (hidx : idx < w✝),
    ⟦{ aig := (go aig expr).val.aig, ref := (go aig expr).val.stream.getRef idx hidx }, assign.toAIGAssignment⟧ =
      (eval assign expr).getLsb idx
aig : AIG BVBit
idx : Nat
hidx : idx < w✝
n✝ : Nat
h : (eval assign expr).getLsb (n✝ + idx) = true
⊢ BitVec w✝

State before:
case un.shiftRightConst.a
w : Nat
assign : Assignment
w✝ : Nat
expr : BVExpr w✝
ih :
  ∀ (aig : AIG BVBit) (idx : Nat) (hidx : idx < w✝),
    ⟦{ aig := (go aig expr).val.aig, ref := (go aig expr).val.stream.getRef idx hidx }, assign.toAIGAssignment⟧ =
      (eval assign expr).getLsb idx
aig : AIG BVBit
idx : Nat
hidx : idx < w✝
n✝ : Nat
h : (eval assign expr).getLsb (n✝ + idx) = true
⊢ ?un.shiftRightConst.x.getLsb (n✝ + idx) = true

case un.shiftRightConst.x
w : Nat
assign : Assignment
w✝ : Nat
expr : BVExpr w✝
ih :
  ∀ (aig : AIG BVBit) (idx : Nat) (hidx : idx < w✝),
    ⟦{ aig := (go aig expr).val.aig, ref := (go aig expr).val.stream.getRef idx hidx }, assign.toAIGAssignment⟧ =
      (eval assign expr).getLsb idx
aig : AIG BVBit
idx : Nat
hidx : idx < w✝
n✝ : Nat
h : (eval assign expr).getLsb (n✝ + idx) = true
⊢ BitVec w✝
Tactic:
assumption
State after:
no goals

State before:
case un.rotateLeft
w : Nat
assign : Assignment
w✝ : Nat
expr : BVExpr w✝
ih :
  ∀ (aig : AIG BVBit) (idx : Nat) (hidx : idx < w✝),
    ⟦{ aig := (go aig expr).val.aig, ref := (go aig expr).val.stream.getRef idx hidx }, assign.toAIGAssignment⟧ =
      (eval assign expr).getLsb idx
aig : AIG BVBit
idx : Nat
hidx : idx < w✝
n✝ : Nat
⊢ ⟦{ aig := (go aig (un (BVUnOp.rotateLeft n✝) expr)).val.aig,
        ref := (go aig (un (BVUnOp.rotateLeft n✝) expr)).val.stream.getRef idx hidx },
      assign.toAIGAssignment⟧ =
    (eval assign (un (BVUnOp.rotateLeft n✝) expr)).getLsb idx
Tactic:
simp [go, ih, hidx]
State after:
no goals

State before:
case un.rotateRight
w : Nat
assign : Assignment
w✝ : Nat
expr : BVExpr w✝
ih :
  ∀ (aig : AIG BVBit) (idx : Nat) (hidx : idx < w✝),
    ⟦{ aig := (go aig expr).val.aig, ref := (go aig expr).val.stream.getRef idx hidx }, assign.toAIGAssignment⟧ =
      (eval assign expr).getLsb idx
aig : AIG BVBit
idx : Nat
hidx : idx < w✝
n✝ : Nat
⊢ ⟦{ aig := (go aig (un (BVUnOp.rotateRight n✝) expr)).val.aig,
        ref := (go aig (un (BVUnOp.rotateRight n✝) expr)).val.stream.getRef idx hidx },
      assign.toAIGAssignment⟧ =
    (eval assign (un (BVUnOp.rotateRight n✝) expr)).getLsb idx
Tactic:
simp [go, ih, hidx]
State after:
no goals

State before:
case un.arithShiftRightConst
w : Nat
assign : Assignment
w✝ : Nat
expr : BVExpr w✝
ih :
  ∀ (aig : AIG BVBit) (idx : Nat) (hidx : idx < w✝),
    ⟦{ aig := (go aig expr).val.aig, ref := (go aig expr).val.stream.getRef idx hidx }, assign.toAIGAssignment⟧ =
      (eval assign expr).getLsb idx
aig : AIG BVBit
idx : Nat
hidx : idx < w✝
n : Nat
⊢ ⟦{ aig := (go aig (un (BVUnOp.arithShiftRightConst n) expr)).val.aig,
        ref := (go aig (un (BVUnOp.arithShiftRightConst n) expr)).val.stream.getRef idx hidx },
      assign.toAIGAssignment⟧ =
    (eval assign (un (BVUnOp.arithShiftRightConst n) expr)).getLsb idx
Tactic:
rename_i w
State after:
case un.arithShiftRightConst
w✝ : Nat
assign : Assignment
w : Nat
expr : BVExpr w
ih :
  ∀ (aig : AIG BVBit) (idx : Nat) (hidx : idx < w),
    ⟦{ aig := (go aig expr).val.aig, ref := (go aig expr).val.stream.getRef idx hidx }, assign.toAIGAssignment⟧ =
      (eval assign expr).getLsb idx
aig : AIG BVBit
idx : Nat
hidx : idx < w
n : Nat
⊢ ⟦{ aig := (go aig (un (BVUnOp.arithShiftRightConst n) expr)).val.aig,
        ref := (go aig (un (BVUnOp.arithShiftRightConst n) expr)).val.stream.getRef idx hidx },
      assign.toAIGAssignment⟧ =
    (eval assign (un (BVUnOp.arithShiftRightConst n) expr)).getLsb idx

State before:
case un.arithShiftRightConst
w✝ : Nat
assign : Assignment
w : Nat
expr : BVExpr w
ih :
  ∀ (aig : AIG BVBit) (idx : Nat) (hidx : idx < w),
    ⟦{ aig := (go aig expr).val.aig, ref := (go aig expr).val.stream.getRef idx hidx }, assign.toAIGAssignment⟧ =
      (eval assign expr).getLsb idx
aig : AIG BVBit
idx : Nat
hidx : idx < w
n : Nat
⊢ ⟦{ aig := (go aig (un (BVUnOp.arithShiftRightConst n) expr)).val.aig,
        ref := (go aig (un (BVUnOp.arithShiftRightConst n) expr)).val.stream.getRef idx hidx },
      assign.toAIGAssignment⟧ =
    (eval assign (un (BVUnOp.arithShiftRightConst n) expr)).getLsb idx
Tactic:
have : ¬(w ≤ idx) := by omega
State after:
case un.arithShiftRightConst
w✝ : Nat
assign : Assignment
w : Nat
expr : BVExpr w
ih :
  ∀ (aig : AIG BVBit) (idx : Nat) (hidx : idx < w),
    ⟦{ aig := (go aig expr).val.aig, ref := (go aig expr).val.stream.getRef idx hidx }, assign.toAIGAssignment⟧ =
      (eval assign expr).getLsb idx
aig : AIG BVBit
idx : Nat
hidx : idx < w
n : Nat
this : ¬w ≤ idx
⊢ ⟦{ aig := (go aig (un (BVUnOp.arithShiftRightConst n) expr)).val.aig,
        ref := (go aig (un (BVUnOp.arithShiftRightConst n) expr)).val.stream.getRef idx hidx },
      assign.toAIGAssignment⟧ =
    (eval assign (un (BVUnOp.arithShiftRightConst n) expr)).getLsb idx

State before:
case un.arithShiftRightConst
w✝ : Nat
assign : Assignment
w : Nat
expr : BVExpr w
ih :
  ∀ (aig : AIG BVBit) (idx : Nat) (hidx : idx < w),
    ⟦{ aig := (go aig expr).val.aig, ref := (go aig expr).val.stream.getRef idx hidx }, assign.toAIGAssignment⟧ =
      (eval assign expr).getLsb idx
aig : AIG BVBit
idx : Nat
hidx : idx < w
n : Nat
this : ¬w ≤ idx
⊢ ⟦{ aig := (go aig (un (BVUnOp.arithShiftRightConst n) expr)).val.aig,
        ref := (go aig (un (BVUnOp.arithShiftRightConst n) expr)).val.stream.getRef idx hidx },
      assign.toAIGAssignment⟧ =
    (eval assign (un (BVUnOp.arithShiftRightConst n) expr)).getLsb idx
Tactic:
simp [go, ih, this, BitVec.getLsb_sshiftRight, BitVec.msb_eq_getLsb_last ]
State after:
no goals

State before:
w✝ : Nat
assign : Assignment
w : Nat
expr : BVExpr w
ih :
  ∀ (aig : AIG BVBit) (idx : Nat) (hidx : idx < w),
    ⟦{ aig := (go aig expr).val.aig, ref := (go aig expr).val.stream.getRef idx hidx }, assign.toAIGAssignment⟧ =
      (eval assign expr).getLsb idx
aig : AIG BVBit
idx : Nat
hidx : idx < w
n : Nat
⊢ ¬w ≤ idx
Tactic:
omega
State after:
no goals