internlm/Lean-Github huggingface dataset:
Theorem: BVExpr.bitblast.go_denote_eq_eval_getLsb
Proof 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]
Proof 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)
Theorem: BVExpr.bitblast.go_denote_eq_eval_getLsb
Proof 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]
Proof state after:
no goals
Theorem: BVExpr.bitblast.go_denote_eq_eval_getLsb
Proof 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]
Proof 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)
Theorem: BVExpr.bitblast.go_denote_eq_eval_getLsb
Proof 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]
Proof 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)
Theorem: BVExpr.bitblast.go_denote_eq_eval_getLsb
Proof 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)]
Proof 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)
Theorem: BVExpr.bitblast.go_denote_eq_eval_getLsb
Proof 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]
Proof 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)
Theorem: BVExpr.bitblast.go_denote_eq_eval_getLsb
Proof 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]
Proof state after:
no goals
Theorem: BVExpr.bitblast.go_denote_eq_eval_getLsb
Proof 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]
Proof 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)
Theorem: BVExpr.bitblast.go_denote_eq_eval_getLsb
Proof 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]
Proof 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)
Theorem: BVExpr.bitblast.go_denote_eq_eval_getLsb
Proof 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)]
Proof 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)
Theorem: BVExpr.bitblast.go_denote_eq_eval_getLsb
Proof 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]
Proof 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)
Theorem: BVExpr.bitblast.go_denote_eq_eval_getLsb
Proof 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]
Proof state after:
no goals
Theorem: BVExpr.bitblast.go_denote_eq_eval_getLsb
Proof 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]
Proof 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
Theorem: BVExpr.bitblast.go_denote_eq_eval_getLsb
Proof 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
Proof 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