internlm/Lean-Github huggingface dataset:
Theorem: BVExpr.bitblast.blastRotateLeft_eq_eval_getLsb
Proof state before:
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
w : Nat
aig : AIG α
target : aig.ShiftTarget w
assign : α → Bool
⊢ ∀ (idx : Nat) (hidx : idx < w),
    ⟦{ aig := (blastRotateLeft aig target).aig, ref := (blastRotateLeft aig target).stream.getRef idx hidx }, assign⟧ =
      if hidx2 : idx < target.distance % w then
        ⟦{ aig := aig, ref := target.stream.getRef (w - target.distance % w + idx) ⋯ }, assign⟧
      else ⟦{ aig := aig, ref := target.stream.getRef (idx - target.distance % w) ⋯ }, assign⟧
Tactic:
intros
Proof state after:
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
w : Nat
aig : AIG α
target : aig.ShiftTarget w
assign : α → Bool
idx✝ : Nat
hidx✝ : idx✝ < w
⊢ ⟦{ aig := (blastRotateLeft aig target).aig, ref := (blastRotateLeft aig target).stream.getRef idx✝ hidx✝ }, assign⟧ =
    if hidx2 : idx✝ < target.distance % w then
      ⟦{ aig := aig, ref := target.stream.getRef (w - target.distance % w + idx✝) ⋯ }, assign⟧
    else ⟦{ aig := aig, ref := target.stream.getRef (idx✝ - target.distance % w) ⋯ }, assign⟧
Theorem: BVExpr.bitblast.blastRotateLeft_eq_eval_getLsb
Proof state before:
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
w : Nat
aig : AIG α
target : aig.ShiftTarget w
assign : α → Bool
idx✝ : Nat
hidx✝ : idx✝ < w
⊢ ⟦{ aig := (blastRotateLeft aig target).aig, ref := (blastRotateLeft aig target).stream.getRef idx✝ hidx✝ }, assign⟧ =
    if hidx2 : idx✝ < target.distance % w then
      ⟦{ aig := aig, ref := target.stream.getRef (w - target.distance % w + idx✝) ⋯ }, assign⟧
    else ⟦{ aig := aig, ref := target.stream.getRef (idx✝ - target.distance % w) ⋯ }, assign⟧
Tactic:
unfold blastRotateLeft
Proof state after:
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
w : Nat
aig : AIG α
target : aig.ShiftTarget w
assign : α → Bool
idx✝ : Nat
hidx✝ : idx✝ < w
⊢ ⟦{
        aig :=
          (match target with
            | { stream := input, distance := distance } =>
              { aig := aig, stream := blastRotateLeft.go input distance 0 ⋯ RefStream.empty }).aig,
        ref :=
          (match target with
                | { stream := input, distance := distance } =>
                  { aig := aig, stream := blastRotateLeft.go input distance 0 ⋯ RefStream.empty }).stream.getRef
            idx✝ hidx✝ },
      assign⟧ =
    if hidx2 : idx✝ < target.distance % w then
      ⟦{ aig := aig, ref := target.stream.getRef (w - target.distance % w + idx✝) ⋯ }, assign⟧
    else ⟦{ aig := aig, ref := target.stream.getRef (idx✝ - target.distance % w) ⋯ }, assign⟧
Theorem: BVExpr.bitblast.blastRotateLeft_eq_eval_getLsb
Proof state before:
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
w : Nat
aig : AIG α
target : aig.ShiftTarget w
assign : α → Bool
idx✝ : Nat
hidx✝ : idx✝ < w
⊢ ⟦{
        aig :=
          (match target with
            | { stream := input, distance := distance } =>
              { aig := aig, stream := blastRotateLeft.go input distance 0 ⋯ RefStream.empty }).aig,
        ref :=
          (match target with
                | { stream := input, distance := distance } =>
                  { aig := aig, stream := blastRotateLeft.go input distance 0 ⋯ RefStream.empty }).stream.getRef
            idx✝ hidx✝ },
      assign⟧ =
    if hidx2 : idx✝ < target.distance % w then
      ⟦{ aig := aig, ref := target.stream.getRef (w - target.distance % w + idx✝) ⋯ }, assign⟧
    else ⟦{ aig := aig, ref := target.stream.getRef (idx✝ - target.distance % w) ⋯ }, assign⟧
Tactic:
dsimp
Proof state after:
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
w : Nat
aig : AIG α
target : aig.ShiftTarget w
assign : α → Bool
idx✝ : Nat
hidx✝ : idx✝ < w
⊢ ⟦{ aig := aig, ref := (blastRotateLeft.go target.stream target.distance 0 ⋯ RefStream.empty).getRef idx✝ hidx✝ },
      assign⟧ =
    if hidx2 : idx✝ < target.distance % w then
      ⟦{ aig := aig, ref := target.stream.getRef (w - target.distance % w + idx✝) ⋯ }, assign⟧
    else ⟦{ aig := aig, ref := target.stream.getRef (idx✝ - target.distance % w) ⋯ }, assign⟧
Theorem: BVExpr.bitblast.blastRotateLeft_eq_eval_getLsb
Proof state before:
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
w : Nat
aig : AIG α
target : aig.ShiftTarget w
assign : α → Bool
idx✝ : Nat
hidx✝ : idx✝ < w
⊢ ⟦{ aig := aig, ref := (blastRotateLeft.go target.stream target.distance 0 ⋯ RefStream.empty).getRef idx✝ hidx✝ },
      assign⟧ =
    if hidx2 : idx✝ < target.distance % w then
      ⟦{ aig := aig, ref := target.stream.getRef (w - target.distance % w + idx✝) ⋯ }, assign⟧
    else ⟦{ aig := aig, ref := target.stream.getRef (idx✝ - target.distance % w) ⋯ }, assign⟧
Tactic:
rw [blastRotateLeft.go_getRef]
Proof state after:
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
w : Nat
aig : AIG α
target : aig.ShiftTarget w
assign : α → Bool
idx✝ : Nat
hidx✝ : idx✝ < w
⊢ ⟦{ aig := aig,
        ref :=
          if hidx3 : idx✝ < target.distance % w then target.stream.getRef (w - target.distance % w + idx✝) ⋯
          else target.stream.getRef (idx✝ - target.distance % w) ⋯ },
      assign⟧ =
    if hidx2 : idx✝ < target.distance % w then
      ⟦{ aig := aig, ref := target.stream.getRef (w - target.distance % w + idx✝) ⋯ }, assign⟧
    else ⟦{ aig := aig, ref := target.stream.getRef (idx✝ - target.distance % w) ⋯ }, assign⟧

case a
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
w : Nat
aig : AIG α
target : aig.ShiftTarget w
assign : α → Bool
idx✝ : Nat
hidx✝ : idx✝ < w
⊢ 0 ≤ idx✝
Theorem: BVExpr.bitblast.blastRotateLeft_eq_eval_getLsb
Proof state before:
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
w : Nat
aig : AIG α
target : aig.ShiftTarget w
assign : α → Bool
idx✝ : Nat
hidx✝ : idx✝ < w
⊢ ⟦{ aig := aig,
        ref :=
          if hidx3 : idx✝ < target.distance % w then target.stream.getRef (w - target.distance % w + idx✝) ⋯
          else target.stream.getRef (idx✝ - target.distance % w) ⋯ },
      assign⟧ =
    if hidx2 : idx✝ < target.distance % w then
      ⟦{ aig := aig, ref := target.stream.getRef (w - target.distance % w + idx✝) ⋯ }, assign⟧
    else ⟦{ aig := aig, ref := target.stream.getRef (idx✝ - target.distance % w) ⋯ }, assign⟧

case a
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
w : Nat
aig : AIG α
target : aig.ShiftTarget w
assign : α → Bool
idx✝ : Nat
hidx✝ : idx✝ < w
⊢ 0 ≤ idx✝
Tactic:
. split
  . rfl
  . rfl
Proof state after:
case a
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
w : Nat
aig : AIG α
target : aig.ShiftTarget w
assign : α → Bool
idx✝ : Nat
hidx✝ : idx✝ < w
⊢ 0 ≤ idx✝
Theorem: BVExpr.bitblast.blastRotateLeft_eq_eval_getLsb
Proof state before:
case a
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
w : Nat
aig : AIG α
target : aig.ShiftTarget w
assign : α → Bool
idx✝ : Nat
hidx✝ : idx✝ < w
⊢ 0 ≤ idx✝
Tactic:
. omega
Proof state after:
no goals
Theorem: BVExpr.bitblast.blastRotateLeft_eq_eval_getLsb
Proof state before:
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
w : Nat
aig : AIG α
target : aig.ShiftTarget w
assign : α → Bool
idx✝ : Nat
hidx✝ : idx✝ < w
⊢ ⟦{ aig := aig,
        ref :=
          if hidx3 : idx✝ < target.distance % w then target.stream.getRef (w - target.distance % w + idx✝) ⋯
          else target.stream.getRef (idx✝ - target.distance % w) ⋯ },
      assign⟧ =
    if hidx2 : idx✝ < target.distance % w then
      ⟦{ aig := aig, ref := target.stream.getRef (w - target.distance % w + idx✝) ⋯ }, assign⟧
    else ⟦{ aig := aig, ref := target.stream.getRef (idx✝ - target.distance % w) ⋯ }, assign⟧
Tactic:
split
Proof state after:
case isTrue
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
w : Nat
aig : AIG α
target : aig.ShiftTarget w
assign : α → Bool
idx✝ : Nat
hidx✝ : idx✝ < w
h✝ : idx✝ < target.distance % w
⊢ ⟦{ aig := aig, ref := target.stream.getRef (w - target.distance % w + idx✝) ⋯ }, assign⟧ =
    ⟦{ aig := aig, ref := target.stream.getRef (w - target.distance % w + idx✝) ⋯ }, assign⟧

case isFalse
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
w : Nat
aig : AIG α
target : aig.ShiftTarget w
assign : α → Bool
idx✝ : Nat
hidx✝ : idx✝ < w
h✝ : ¬idx✝ < target.distance % w
⊢ ⟦{ aig := aig, ref := target.stream.getRef (idx✝ - target.distance % w) ⋯ }, assign⟧ =
    ⟦{ aig := aig, ref := target.stream.getRef (idx✝ - target.distance % w) ⋯ }, assign⟧
Theorem: BVExpr.bitblast.blastRotateLeft_eq_eval_getLsb
Proof state before:
case isTrue
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
w : Nat
aig : AIG α
target : aig.ShiftTarget w
assign : α → Bool
idx✝ : Nat
hidx✝ : idx✝ < w
h✝ : idx✝ < target.distance % w
⊢ ⟦{ aig := aig, ref := target.stream.getRef (w - target.distance % w + idx✝) ⋯ }, assign⟧ =
    ⟦{ aig := aig, ref := target.stream.getRef (w - target.distance % w + idx✝) ⋯ }, assign⟧

case isFalse
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
w : Nat
aig : AIG α
target : aig.ShiftTarget w
assign : α → Bool
idx✝ : Nat
hidx✝ : idx✝ < w
h✝ : ¬idx✝ < target.distance % w
⊢ ⟦{ aig := aig, ref := target.stream.getRef (idx✝ - target.distance % w) ⋯ }, assign⟧ =
    ⟦{ aig := aig, ref := target.stream.getRef (idx✝ - target.distance % w) ⋯ }, assign⟧
Tactic:
. rfl
Proof state after:
case isFalse
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
w : Nat
aig : AIG α
target : aig.ShiftTarget w
assign : α → Bool
idx✝ : Nat
hidx✝ : idx✝ < w
h✝ : ¬idx✝ < target.distance % w
⊢ ⟦{ aig := aig, ref := target.stream.getRef (idx✝ - target.distance % w) ⋯ }, assign⟧ =
    ⟦{ aig := aig, ref := target.stream.getRef (idx✝ - target.distance % w) ⋯ }, assign⟧
Theorem: BVExpr.bitblast.blastRotateLeft_eq_eval_getLsb
Proof state before:
case isFalse
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
w : Nat
aig : AIG α
target : aig.ShiftTarget w
assign : α → Bool
idx✝ : Nat
hidx✝ : idx✝ < w
h✝ : ¬idx✝ < target.distance % w
⊢ ⟦{ aig := aig, ref := target.stream.getRef (idx✝ - target.distance % w) ⋯ }, assign⟧ =
    ⟦{ aig := aig, ref := target.stream.getRef (idx✝ - target.distance % w) ⋯ }, assign⟧
Tactic:
. rfl
Proof state after:
no goals
Theorem: BVExpr.bitblast.blastRotateLeft_eq_eval_getLsb
Proof state before:
case isTrue
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
w : Nat
aig : AIG α
target : aig.ShiftTarget w
assign : α → Bool
idx✝ : Nat
hidx✝ : idx✝ < w
h✝ : idx✝ < target.distance % w
⊢ ⟦{ aig := aig, ref := target.stream.getRef (w - target.distance % w + idx✝) ⋯ }, assign⟧ =
    ⟦{ aig := aig, ref := target.stream.getRef (w - target.distance % w + idx✝) ⋯ }, assign⟧
Tactic:
rfl
Proof state after:
no goals
Theorem: BVExpr.bitblast.blastRotateLeft_eq_eval_getLsb
Proof state before:
case isFalse
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
w : Nat
aig : AIG α
target : aig.ShiftTarget w
assign : α → Bool
idx✝ : Nat
hidx✝ : idx✝ < w
h✝ : ¬idx✝ < target.distance % w
⊢ ⟦{ aig := aig, ref := target.stream.getRef (idx✝ - target.distance % w) ⋯ }, assign⟧ =
    ⟦{ aig := aig, ref := target.stream.getRef (idx✝ - target.distance % w) ⋯ }, assign⟧
Tactic:
rfl
Proof state after:
no goals
Theorem: BVExpr.bitblast.blastRotateLeft_eq_eval_getLsb
Proof state before:
case a
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
w : Nat
aig : AIG α
target : aig.ShiftTarget w
assign : α → Bool
idx✝ : Nat
hidx✝ : idx✝ < w
⊢ 0 ≤ idx✝
Tactic:
omega
Proof state after:
no goals
Theorem: BVPred.bitblast_denote_eq_eval
Proof state before:
aig : AIG BVBit
pred : BVPred
assign : BVExpr.Assignment
⊢ ⟦bitblast aig pred, assign.toAIGAssignment⟧ = eval assign pred
Tactic:
cases pred with
| bin lhs op rhs =>
  cases op with
  | eq =>
    simp only [bitblast, eval_bin, BVBinPred.eval_eq]
    rw [mkEq_denote_eq_eval_beq]
    . intros
      rw [AIG.LawfulStreamOperator.denote_mem_prefix (f := BVExpr.bitblast)]
      . simp
        rw [BVExpr.bitblast_denote_eq_eval_getLsb]
      . simp [Ref.hgate]
    . intros
      simp
  | ult =>
    simp only [bitblast, eval_bin, BVBinPred.eval_ult]
    rw [mkUlt_denote_eq_eval_ult]
    . intros
      rw [AIG.LawfulStreamOperator.denote_mem_prefix (f := BVExpr.bitblast)]
      . simp
        rw [BVExpr.bitblast_denote_eq_eval_getLsb]
      . simp [Ref.hgate]
    . intros
      simp
| getLsb expr idx =>
  simp [bitblast]
  apply BitVec.lt_of_getLsb
Proof state after:
no goals
Theorem: BVPred.bitblast_denote_eq_eval
Proof state before:
case bin
aig : AIG BVBit
assign : BVExpr.Assignment
w✝ : Nat
lhs : BVExpr w✝
op : BVBinPred
rhs : BVExpr w✝
⊢ ⟦bitblast aig (bin lhs op rhs), assign.toAIGAssignment⟧ = eval assign (bin lhs op rhs)
Tactic:
cases op with
| eq =>
  simp only [bitblast, eval_bin, BVBinPred.eval_eq]
  rw [mkEq_denote_eq_eval_beq]
  . intros
    rw [AIG.LawfulStreamOperator.denote_mem_prefix (f := BVExpr.bitblast)]
    . simp
      rw [BVExpr.bitblast_denote_eq_eval_getLsb]
    . simp [Ref.hgate]
  . intros
    simp
| ult =>
  simp only [bitblast, eval_bin, BVBinPred.eval_ult]
  rw [mkUlt_denote_eq_eval_ult]
  . intros
    rw [AIG.LawfulStreamOperator.denote_mem_prefix (f := BVExpr.bitblast)]
    . simp
      rw [BVExpr.bitblast_denote_eq_eval_getLsb]
    . simp [Ref.hgate]
  . intros
    simp
Proof state after:
no goals
Theorem: BVPred.bitblast_denote_eq_eval
Proof state before:
case bin.eq
aig : AIG BVBit
assign : BVExpr.Assignment
w✝ : Nat
lhs rhs : BVExpr w✝
⊢ ⟦bitblast aig (bin lhs BVBinPred.eq rhs), assign.toAIGAssignment⟧ = eval assign (bin lhs BVBinPred.eq rhs)
Tactic:
simp only [bitblast, eval_bin, BVBinPred.eval_eq]
Proof state after:
case bin.eq
aig : AIG BVBit
assign : BVExpr.Assignment
w✝ : Nat
lhs rhs : BVExpr w✝
⊢ ⟦mkEq (BVExpr.bitblast (BVExpr.bitblast aig lhs).aig rhs).aig
        { lhs := (BVExpr.bitblast aig lhs).stream.cast ⋯,
          rhs := (BVExpr.bitblast (BVExpr.bitblast aig lhs).aig rhs).stream },
      assign.toAIGAssignment⟧ =
    (BVExpr.eval assign lhs == BVExpr.eval assign rhs)
Theorem: BVPred.bitblast_denote_eq_eval
Proof state before:
case bin.eq
aig : AIG BVBit
assign : BVExpr.Assignment
w✝ : Nat
lhs rhs : BVExpr w✝
⊢ ⟦mkEq (BVExpr.bitblast (BVExpr.bitblast aig lhs).aig rhs).aig
        { lhs := (BVExpr.bitblast aig lhs).stream.cast ⋯,
          rhs := (BVExpr.bitblast (BVExpr.bitblast aig lhs).aig rhs).stream },
      assign.toAIGAssignment⟧ =
    (BVExpr.eval assign lhs == BVExpr.eval assign rhs)
Tactic:
rw [mkEq_denote_eq_eval_beq]
Proof state after:
case bin.eq.hleft
aig : AIG BVBit
assign : BVExpr.Assignment
w✝ : Nat
lhs rhs : BVExpr w✝
⊢ ∀ (idx : Nat) (hidx : idx < w✝),
    ⟦{ aig := (BVExpr.bitblast (BVExpr.bitblast aig lhs).aig rhs).aig,
          ref :=
            { lhs := (BVExpr.bitblast aig lhs).stream.cast ⋯,
                    rhs := (BVExpr.bitblast (BVExpr.bitblast aig lhs).aig rhs).stream }.lhs.getRef
              idx hidx },
        assign.toAIGAssignment⟧ =
      (BVExpr.eval assign lhs).getLsb idx

case bin.eq.hright
aig : AIG BVBit
assign : BVExpr.Assignment
w✝ : Nat
lhs rhs : BVExpr w✝
⊢ ∀ (idx : Nat) (hidx : idx < w✝),
    ⟦{ aig := (BVExpr.bitblast (BVExpr.bitblast aig lhs).aig rhs).aig,
          ref :=
            { lhs := (BVExpr.bitblast aig lhs).stream.cast ⋯,
                    rhs := (BVExpr.bitblast (BVExpr.bitblast aig lhs).aig rhs).stream }.rhs.getRef
              idx hidx },
        assign.toAIGAssignment⟧ =
      (BVExpr.eval assign rhs).getLsb idx
Theorem: BVPred.bitblast_denote_eq_eval
Proof state before:
case bin.eq.hleft
aig : AIG BVBit
assign : BVExpr.Assignment
w✝ : Nat
lhs rhs : BVExpr w✝
⊢ ∀ (idx : Nat) (hidx : idx < w✝),
    ⟦{ aig := (BVExpr.bitblast (BVExpr.bitblast aig lhs).aig rhs).aig,
          ref :=
            { lhs := (BVExpr.bitblast aig lhs).stream.cast ⋯,
                    rhs := (BVExpr.bitblast (BVExpr.bitblast aig lhs).aig rhs).stream }.lhs.getRef
              idx hidx },
        assign.toAIGAssignment⟧ =
      (BVExpr.eval assign lhs).getLsb idx

case bin.eq.hright
aig : AIG BVBit
assign : BVExpr.Assignment
w✝ : Nat
lhs rhs : BVExpr w✝
⊢ ∀ (idx : Nat) (hidx : idx < w✝),
    ⟦{ aig := (BVExpr.bitblast (BVExpr.bitblast aig lhs).aig rhs).aig,
          ref :=
            { lhs := (BVExpr.bitblast aig lhs).stream.cast ⋯,
                    rhs := (BVExpr.bitblast (BVExpr.bitblast aig lhs).aig rhs).stream }.rhs.getRef
              idx hidx },
        assign.toAIGAssignment⟧ =
      (BVExpr.eval assign rhs).getLsb idx
Tactic:
. intros
  rw [AIG.LawfulStreamOperator.denote_mem_prefix (f := BVExpr.bitblast)]
  . simp
    rw [BVExpr.bitblast_denote_eq_eval_getLsb]
  . simp [Ref.hgate]
Proof state after:
case bin.eq.hright
aig : AIG BVBit
assign : BVExpr.Assignment
w✝ : Nat
lhs rhs : BVExpr w✝
⊢ ∀ (idx : Nat) (hidx : idx < w✝),
    ⟦{ aig := (BVExpr.bitblast (BVExpr.bitblast aig lhs).aig rhs).aig,
          ref :=
            { lhs := (BVExpr.bitblast aig lhs).stream.cast ⋯,
                    rhs := (BVExpr.bitblast (BVExpr.bitblast aig lhs).aig rhs).stream }.rhs.getRef
              idx hidx },
        assign.toAIGAssignment⟧ =
      (BVExpr.eval assign rhs).getLsb idx
Theorem: BVPred.bitblast_denote_eq_eval
Proof state before:
case bin.eq.hright
aig : AIG BVBit
assign : BVExpr.Assignment
w✝ : Nat
lhs rhs : BVExpr w✝
⊢ ∀ (idx : Nat) (hidx : idx < w✝),
    ⟦{ aig := (BVExpr.bitblast (BVExpr.bitblast aig lhs).aig rhs).aig,
          ref :=
            { lhs := (BVExpr.bitblast aig lhs).stream.cast ⋯,
                    rhs := (BVExpr.bitblast (BVExpr.bitblast aig lhs).aig rhs).stream }.rhs.getRef
              idx hidx },
        assign.toAIGAssignment⟧ =
      (BVExpr.eval assign rhs).getLsb idx
Tactic:
. intros
  simp
Proof state after:
no goals
Theorem: BVPred.bitblast_denote_eq_eval
Proof state before:
case bin.eq.hleft
aig : AIG BVBit
assign : BVExpr.Assignment
w✝ : Nat
lhs rhs : BVExpr w✝
⊢ ∀ (idx : Nat) (hidx : idx < w✝),
    ⟦{ aig := (BVExpr.bitblast (BVExpr.bitblast aig lhs).aig rhs).aig,
          ref :=
            { lhs := (BVExpr.bitblast aig lhs).stream.cast ⋯,
                    rhs := (BVExpr.bitblast (BVExpr.bitblast aig lhs).aig rhs).stream }.lhs.getRef
              idx hidx },
        assign.toAIGAssignment⟧ =
      (BVExpr.eval assign lhs).getLsb idx
Tactic:
intros
Proof state after:
case bin.eq.hleft
aig : AIG BVBit
assign : BVExpr.Assignment
w✝ : Nat
lhs rhs : BVExpr w✝
idx✝ : Nat
hidx✝ : idx✝ < w✝
⊢ ⟦{ aig := (BVExpr.bitblast (BVExpr.bitblast aig lhs).aig rhs).aig,
        ref :=
          { lhs := (BVExpr.bitblast aig lhs).stream.cast ⋯,
                  rhs := (BVExpr.bitblast (BVExpr.bitblast aig lhs).aig rhs).stream }.lhs.getRef
            idx✝ hidx✝ },
      assign.toAIGAssignment⟧ =
    (BVExpr.eval assign lhs).getLsb idx✝
Theorem: BVPred.bitblast_denote_eq_eval
Proof state before:
case bin.eq.hleft
aig : AIG BVBit
assign : BVExpr.Assignment
w✝ : Nat
lhs rhs : BVExpr w✝
idx✝ : Nat
hidx✝ : idx✝ < w✝
⊢ ⟦{ aig := (BVExpr.bitblast (BVExpr.bitblast aig lhs).aig rhs).aig,
        ref :=
          { lhs := (BVExpr.bitblast aig lhs).stream.cast ⋯,
                  rhs := (BVExpr.bitblast (BVExpr.bitblast aig lhs).aig rhs).stream }.lhs.getRef
            idx✝ hidx✝ },
      assign.toAIGAssignment⟧ =
    (BVExpr.eval assign lhs).getLsb idx✝
Tactic:
rw [AIG.LawfulStreamOperator.denote_mem_prefix (f := BVExpr.bitblast)]
Proof state after:
case bin.eq.hleft
aig : AIG BVBit
assign : BVExpr.Assignment
w✝ : Nat
lhs rhs : BVExpr w✝
idx✝ : Nat
hidx✝ : idx✝ < w✝
⊢ ⟦{ aig := (BVExpr.bitblast aig lhs).aig,
        ref :=
          {
            gate :=
              ({ lhs := (BVExpr.bitblast aig lhs).stream.cast ⋯,
                        rhs := (BVExpr.bitblast (BVExpr.bitblast aig lhs).aig rhs).stream }.lhs.getRef
                  idx✝ hidx✝).gate,
            hgate := ?bin.eq.hleft } },
      assign.toAIGAssignment⟧ =
    (BVExpr.eval assign lhs).getLsb idx✝

case bin.eq.hleft
aig : AIG BVBit
assign : BVExpr.Assignment
w✝ : Nat
lhs rhs : BVExpr w✝
idx✝ : Nat
hidx✝ : idx✝ < w✝
⊢ ({ lhs := (BVExpr.bitblast aig lhs).stream.cast ⋯,
              rhs := (BVExpr.bitblast (BVExpr.bitblast aig lhs).aig rhs).stream }.lhs.getRef
        idx✝ hidx✝).gate <
    (BVExpr.bitblast aig lhs).aig.decls.size
Theorem: BVPred.bitblast_denote_eq_eval
Proof state before:
case bin.eq.hleft
aig : AIG BVBit
assign : BVExpr.Assignment
w✝ : Nat
lhs rhs : BVExpr w✝
idx✝ : Nat
hidx✝ : idx✝ < w✝
⊢ ⟦{ aig := (BVExpr.bitblast aig lhs).aig,
        ref :=
          {
            gate :=
              ({ lhs := (BVExpr.bitblast aig lhs).stream.cast ⋯,
                        rhs := (BVExpr.bitblast (BVExpr.bitblast aig lhs).aig rhs).stream }.lhs.getRef
                  idx✝ hidx✝).gate,
            hgate := ?bin.eq.hleft } },
      assign.toAIGAssignment⟧ =
    (BVExpr.eval assign lhs).getLsb idx✝

case bin.eq.hleft
aig : AIG BVBit
assign : BVExpr.Assignment
w✝ : Nat
lhs rhs : BVExpr w✝
idx✝ : Nat
hidx✝ : idx✝ < w✝
⊢ ({ lhs := (BVExpr.bitblast aig lhs).stream.cast ⋯,
              rhs := (BVExpr.bitblast (BVExpr.bitblast aig lhs).aig rhs).stream }.lhs.getRef
        idx✝ hidx✝).gate <
    (BVExpr.bitblast aig lhs).aig.decls.size
Tactic:
. simp
  rw [BVExpr.bitblast_denote_eq_eval_getLsb]
Proof state after:
case bin.eq.hleft
aig : AIG BVBit
assign : BVExpr.Assignment
w✝ : Nat
lhs rhs : BVExpr w✝
idx✝ : Nat
hidx✝ : idx✝ < w✝
⊢ ({ lhs := (BVExpr.bitblast aig lhs).stream.cast ⋯,
              rhs := (BVExpr.bitblast (BVExpr.bitblast aig lhs).aig rhs).stream }.lhs.getRef
        idx✝ hidx✝).gate <
    (BVExpr.bitblast aig lhs).aig.decls.size
Theorem: BVPred.bitblast_denote_eq_eval
Proof state before:
case bin.eq.hleft
aig : AIG BVBit
assign : BVExpr.Assignment
w✝ : Nat
lhs rhs : BVExpr w✝
idx✝ : Nat
hidx✝ : idx✝ < w✝
⊢ ({ lhs := (BVExpr.bitblast aig lhs).stream.cast ⋯,
              rhs := (BVExpr.bitblast (BVExpr.bitblast aig lhs).aig rhs).stream }.lhs.getRef
        idx✝ hidx✝).gate <
    (BVExpr.bitblast aig lhs).aig.decls.size
Tactic:
. simp [Ref.hgate]
Proof state after:
no goals
Theorem: BVPred.bitblast_denote_eq_eval
Proof state before:
case bin.eq.hleft
aig : AIG BVBit
assign : BVExpr.Assignment
w✝ : Nat
lhs rhs : BVExpr w✝
idx✝ : Nat
hidx✝ : idx✝ < w✝
⊢ ⟦{ aig := (BVExpr.bitblast aig lhs).aig,
        ref :=
          {
            gate :=
              ({ lhs := (BVExpr.bitblast aig lhs).stream.cast ⋯,
                        rhs := (BVExpr.bitblast (BVExpr.bitblast aig lhs).aig rhs).stream }.lhs.getRef
                  idx✝ hidx✝).gate,
            hgate := ?bin.eq.hleft } },
      assign.toAIGAssignment⟧ =
    (BVExpr.eval assign lhs).getLsb idx✝
Tactic:
simp
Proof state after:
case bin.eq.hleft
aig : AIG BVBit
assign : BVExpr.Assignment
w✝ : Nat
lhs rhs : BVExpr w✝
idx✝ : Nat
hidx✝ : idx✝ < w✝
⊢ ⟦{ aig := (BVExpr.bitblast aig lhs).aig,
        ref := { gate := ((BVExpr.bitblast aig lhs).stream.getRef idx✝ hidx✝).gate, hgate := ⋯ } },
      assign.toAIGAssignment⟧ =
    (BVExpr.eval assign lhs).getLsb idx✝
Theorem: BVPred.bitblast_denote_eq_eval
Proof state before:
case bin.eq.hleft
aig : AIG BVBit
assign : BVExpr.Assignment
w✝ : Nat
lhs rhs : BVExpr w✝
idx✝ : Nat
hidx✝ : idx✝ < w✝
⊢ ⟦{ aig := (BVExpr.bitblast aig lhs).aig,
        ref := { gate := ((BVExpr.bitblast aig lhs).stream.getRef idx✝ hidx✝).gate, hgate := ⋯ } },
      assign.toAIGAssignment⟧ =
    (BVExpr.eval assign lhs).getLsb idx✝
Tactic:
rw [BVExpr.bitblast_denote_eq_eval_getLsb]
Proof state after:
no goals
Theorem: BVPred.bitblast_denote_eq_eval
Proof state before:
case bin.eq.hleft
aig : AIG BVBit
assign : BVExpr.Assignment
w✝ : Nat
lhs rhs : BVExpr w✝
idx✝ : Nat
hidx✝ : idx✝ < w✝
⊢ ({ lhs := (BVExpr.bitblast aig lhs).stream.cast ⋯,
              rhs := (BVExpr.bitblast (BVExpr.bitblast aig lhs).aig rhs).stream }.lhs.getRef
        idx✝ hidx✝).gate <
    (BVExpr.bitblast aig lhs).aig.decls.size
Tactic:
simp [Ref.hgate]
Proof state after:
no goals