Theorem: BVPred.bitblast_denote_eq_eval (LeanSAT/Reflect/BVExpr/BitBlast/Lemmas/Pred.lean)

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

State before:
case bin.ult
aig : AIG BVBit
assign : BVExpr.Assignment
w✝ : Nat
lhs rhs : BVExpr w✝
⊢ ⟦bitblast aig (bin lhs BVBinPred.ult rhs), assign.toAIGAssignment⟧ = eval assign (bin lhs BVBinPred.ult rhs)
Tactic:
simp only [bitblast, eval_bin, BVBinPred.eval_ult]
State after:
case bin.ult
aig : AIG BVBit
assign : BVExpr.Assignment
w✝ : Nat
lhs rhs : BVExpr w✝
⊢ ⟦mkUlt (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).ult (BVExpr.eval assign rhs)

State before:
case bin.ult
aig : AIG BVBit
assign : BVExpr.Assignment
w✝ : Nat
lhs rhs : BVExpr w✝
⊢ ⟦mkUlt (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).ult (BVExpr.eval assign rhs)
Tactic:
rw [mkUlt_denote_eq_eval_ult]
State after:
case bin.ult.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.ult.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

State before:
case bin.ult.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.ult.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]
State after:
case bin.ult.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

State before:
case bin.ult.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
State after:
no goals

State before:
case bin.ult.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
State after:
case bin.ult.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✝

State before:
case bin.ult.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)]
State after:
case bin.ult.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.ult.hleft } },
      assign.toAIGAssignment⟧ =
    (BVExpr.eval assign lhs).getLsb idx✝

case bin.ult.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

State before:
case bin.ult.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.ult.hleft } },
      assign.toAIGAssignment⟧ =
    (BVExpr.eval assign lhs).getLsb idx✝

case bin.ult.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]
State after:
case bin.ult.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

State before:
case bin.ult.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]
State after:
no goals

State before:
case bin.ult.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.ult.hleft } },
      assign.toAIGAssignment⟧ =
    (BVExpr.eval assign lhs).getLsb idx✝
Tactic:
simp
State after:
case bin.ult.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✝

State before:
case bin.ult.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]
State after:
no goals

State before:
case bin.ult.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]
State after:
no goals

State before:
case bin.ult.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
State after:
case bin.ult.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✝

State before:
case bin.ult.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:
simp
State after:
no goals

State before:
case getLsb
aig : AIG BVBit
assign : BVExpr.Assignment
w✝ : Nat
expr : BVExpr w✝
idx : Nat
⊢ ⟦bitblast aig (getLsb expr idx), assign.toAIGAssignment⟧ = eval assign (getLsb expr idx)
Tactic:
simp [bitblast]
State after:
case getLsb
aig : AIG BVBit
assign : BVExpr.Assignment
w✝ : Nat
expr : BVExpr w✝
idx : Nat
⊢ (BVExpr.eval assign expr).getLsb idx = true → idx < w✝

State before:
case getLsb
aig : AIG BVBit
assign : BVExpr.Assignment
w✝ : Nat
expr : BVExpr w✝
idx : Nat
⊢ (BVExpr.eval assign expr).getLsb idx = true → idx < w✝
Tactic:
apply BitVec.lt_of_getLsb
State after:
no goals