internlm/Lean-Github huggingface dataset:
Theorem: BVPred.mkUlt_denote_eq_eval_ult
Proof state before:
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
w : Nat
aig : AIG α
lhs rhs : BitVec w
input : aig.BinaryRefStream w
assign : α → Bool
hleft : ∀ (idx : Nat) (hidx : idx < w), ⟦{ aig := aig, ref := input.lhs.getRef idx hidx }, assign⟧ = lhs.getLsb idx
hright : ∀ (idx : Nat) (hidx : idx < w), ⟦{ aig := aig, ref := input.rhs.getRef idx hidx }, assign⟧ = rhs.getLsb idx
⊢ ⟦{
        aig :=
          (match input with
            | { lhs := lhsRefs, rhs := rhsRefs } =>
              let res := BVExpr.bitblast.blastNot aig rhsRefs;
              let aig_1 := res.aig;
              let rhsRefs_1 := res.stream;
              let res_1 := aig_1.mkConstCached true;
              let aig_2 := res_1.aig;
              let trueRef := res_1.ref;
              let lhsRefs := lhsRefs.cast ⋯;
              let rhsRefs := rhsRefs_1.cast ⋯;
              let res :=
                BVExpr.bitblast.mkOverflowBit aig_2
                  { w := w, stream := { lhs := lhsRefs, rhs := rhsRefs }, cin := trueRef };
              let aig := res.aig;
              let overflowRef := res.ref;
              aig.mkNotCached overflowRef).aig,
        ref :=
          (match input with
            | { lhs := lhsRefs, rhs := rhsRefs } =>
              let res := BVExpr.bitblast.blastNot aig rhsRefs;
              let aig_1 := res.aig;
              let rhsRefs_1 := res.stream;
              let res_1 := aig_1.mkConstCached true;
              let aig_2 := res_1.aig;
              let trueRef := res_1.ref;
              let lhsRefs := lhsRefs.cast ⋯;
              let rhsRefs := rhsRefs_1.cast ⋯;
              let res :=
                BVExpr.bitblast.mkOverflowBit aig_2
                  { w := w, stream := { lhs := lhsRefs, rhs := rhsRefs }, cin := trueRef };
              let aig := res.aig;
              let overflowRef := res.ref;
              aig.mkNotCached overflowRef).ref },
      assign⟧ =
    !BitVec.carry w lhs (~~~rhs) true
Tactic:
simp only [denote_projected_entry, denote_mkNotCached, denote_projected_entry']
Proof state after:
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
w : Nat
aig : AIG α
lhs rhs : BitVec w
input : aig.BinaryRefStream w
assign : α → Bool
hleft : ∀ (idx : Nat) (hidx : idx < w), ⟦{ aig := aig, ref := input.lhs.getRef idx hidx }, assign⟧ = lhs.getLsb idx
hright : ∀ (idx : Nat) (hidx : idx < w), ⟦{ aig := aig, ref := input.rhs.getRef idx hidx }, assign⟧ = rhs.getLsb idx
⊢ (!⟦BVExpr.bitblast.mkOverflowBit ((BVExpr.bitblast.blastNot aig input.rhs).aig.mkConstCached true).aig
          { w := w,
            stream := { lhs := input.lhs.cast ⋯, rhs := (BVExpr.bitblast.blastNot aig input.rhs).stream.cast ⋯ },
            cin := ((BVExpr.bitblast.blastNot aig input.rhs).aig.mkConstCached true).ref },
        assign⟧) =
    !BitVec.carry w lhs (~~~rhs) true
Theorem: BVPred.mkUlt_denote_eq_eval_ult
Proof state before:
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
w : Nat
aig : AIG α
lhs rhs : BitVec w
input : aig.BinaryRefStream w
assign : α → Bool
hleft : ∀ (idx : Nat) (hidx : idx < w), ⟦{ aig := aig, ref := input.lhs.getRef idx hidx }, assign⟧ = lhs.getLsb idx
hright : ∀ (idx : Nat) (hidx : idx < w), ⟦{ aig := aig, ref := input.rhs.getRef idx hidx }, assign⟧ = rhs.getLsb idx
⊢ (!⟦BVExpr.bitblast.mkOverflowBit ((BVExpr.bitblast.blastNot aig input.rhs).aig.mkConstCached true).aig
          { w := w,
            stream := { lhs := input.lhs.cast ⋯, rhs := (BVExpr.bitblast.blastNot aig input.rhs).stream.cast ⋯ },
            cin := ((BVExpr.bitblast.blastNot aig input.rhs).aig.mkConstCached true).ref },
        assign⟧) =
    !BitVec.carry w lhs (~~~rhs) true
Tactic:
congr 1
Proof state after:
case e_a
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
w : Nat
aig : AIG α
lhs rhs : BitVec w
input : aig.BinaryRefStream w
assign : α → Bool
hleft : ∀ (idx : Nat) (hidx : idx < w), ⟦{ aig := aig, ref := input.lhs.getRef idx hidx }, assign⟧ = lhs.getLsb idx
hright : ∀ (idx : Nat) (hidx : idx < w), ⟦{ aig := aig, ref := input.rhs.getRef idx hidx }, assign⟧ = rhs.getLsb idx
⊢ ⟦BVExpr.bitblast.mkOverflowBit ((BVExpr.bitblast.blastNot aig input.rhs).aig.mkConstCached true).aig
        { w := w, stream := { lhs := input.lhs.cast ⋯, rhs := (BVExpr.bitblast.blastNot aig input.rhs).stream.cast ⋯ },
          cin := ((BVExpr.bitblast.blastNot aig input.rhs).aig.mkConstCached true).ref },
      assign⟧ =
    BitVec.carry w lhs (~~~rhs) true
Theorem: BVPred.mkUlt_denote_eq_eval_ult
Proof state before:
case e_a.hright
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
w : Nat
aig : AIG α
lhs rhs : BitVec w
input : aig.BinaryRefStream w
assign : α → Bool
hleft : ∀ (idx : Nat) (hidx : idx < w), ⟦{ aig := aig, ref := input.lhs.getRef idx hidx }, assign⟧ = lhs.getLsb idx
hright : ∀ (idx : Nat) (hidx : idx < w), ⟦{ aig := aig, ref := input.rhs.getRef idx hidx }, assign⟧ = rhs.getLsb idx
⊢ ∀ (idx : Nat)
    (hidx :
      idx <
        { w := w, stream := { lhs := input.lhs.cast ⋯, rhs := (BVExpr.bitblast.blastNot aig input.rhs).stream.cast ⋯ },
            cin := ((BVExpr.bitblast.blastNot aig input.rhs).aig.mkConstCached true).ref }.w),
    ⟦{ aig := ((BVExpr.bitblast.blastNot aig input.rhs).aig.mkConstCached true).aig,
          ref :=
            { w := w,
                      stream :=
                        { lhs := input.lhs.cast ⋯, rhs := (BVExpr.bitblast.blastNot aig input.rhs).stream.cast ⋯ },
                      cin := ((BVExpr.bitblast.blastNot aig input.rhs).aig.mkConstCached true).ref }.stream.rhs.getRef
              idx hidx },
        assign⟧ =
      (~~~rhs).getLsb idx
Tactic:
. dsimp
  intro idx hidx
  rw [AIG.LawfulOperator.denote_mem_prefix (f := AIG.mkConstCached)]
  . simp only [RefStream.getRef_cast, Ref_cast', BitVec.getLsb_not, hidx, decide_True,
      Bool.true_and]
    rw [BVExpr.bitblast.blastNot_eq_eval_getLsb]
    congr 1
    apply hright
  . simp [Ref.hgate]
Proof state after:
no goals
Theorem: BVPred.mkUlt_denote_eq_eval_ult
Proof state before:
case e_a
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
w : Nat
aig : AIG α
lhs rhs : BitVec w
input : aig.BinaryRefStream w
assign : α → Bool
hleft : ∀ (idx : Nat) (hidx : idx < w), ⟦{ aig := aig, ref := input.lhs.getRef idx hidx }, assign⟧ = lhs.getLsb idx
hright : ∀ (idx : Nat) (hidx : idx < w), ⟦{ aig := aig, ref := input.rhs.getRef idx hidx }, assign⟧ = rhs.getLsb idx
⊢ BitVec.carry
      { w := w, stream := { lhs := input.lhs.cast ⋯, rhs := (BVExpr.bitblast.blastNot aig input.rhs).stream.cast ⋯ },
          cin := ((BVExpr.bitblast.blastNot aig input.rhs).aig.mkConstCached true).ref }.w
      lhs (~~~rhs)
      ⟦{ aig := ((BVExpr.bitblast.blastNot aig input.rhs).aig.mkConstCached true).aig,
          ref :=
            { w := w,
                stream := { lhs := input.lhs.cast ⋯, rhs := (BVExpr.bitblast.blastNot aig input.rhs).stream.cast ⋯ },
                cin := ((BVExpr.bitblast.blastNot aig input.rhs).aig.mkConstCached true).ref }.cin },
        assign⟧ =
    BitVec.carry w lhs (~~~rhs) true
Tactic:
simp
Proof state after:
no goals
Theorem: BVPred.mkUlt_denote_eq_eval_ult
Proof state before:
case e_a.hleft
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
w : Nat
aig : AIG α
lhs rhs : BitVec w
input : aig.BinaryRefStream w
assign : α → Bool
hleft : ∀ (idx : Nat) (hidx : idx < w), ⟦{ aig := aig, ref := input.lhs.getRef idx hidx }, assign⟧ = lhs.getLsb idx
hright : ∀ (idx : Nat) (hidx : idx < w), ⟦{ aig := aig, ref := input.rhs.getRef idx hidx }, assign⟧ = rhs.getLsb idx
⊢ ∀ (idx : Nat)
    (hidx :
      idx <
        { w := w, stream := { lhs := input.lhs.cast ⋯, rhs := (BVExpr.bitblast.blastNot aig input.rhs).stream.cast ⋯ },
            cin := ((BVExpr.bitblast.blastNot aig input.rhs).aig.mkConstCached true).ref }.w),
    ⟦{ aig := ((BVExpr.bitblast.blastNot aig input.rhs).aig.mkConstCached true).aig,
          ref :=
            { w := w,
                      stream :=
                        { lhs := input.lhs.cast ⋯, rhs := (BVExpr.bitblast.blastNot aig input.rhs).stream.cast ⋯ },
                      cin := ((BVExpr.bitblast.blastNot aig input.rhs).aig.mkConstCached true).ref }.stream.lhs.getRef
              idx hidx },
        assign⟧ =
      lhs.getLsb idx
Tactic:
dsimp
Proof state after:
case e_a.hleft
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
w : Nat
aig : AIG α
lhs rhs : BitVec w
input : aig.BinaryRefStream w
assign : α → Bool
hleft : ∀ (idx : Nat) (hidx : idx < w), ⟦{ aig := aig, ref := input.lhs.getRef idx hidx }, assign⟧ = lhs.getLsb idx
hright : ∀ (idx : Nat) (hidx : idx < w), ⟦{ aig := aig, ref := input.rhs.getRef idx hidx }, assign⟧ = rhs.getLsb idx
⊢ ∀ (idx : Nat) (hidx : idx < w),
    ⟦{ aig := ((BVExpr.bitblast.blastNot aig input.rhs).aig.mkConstCached true).aig,
          ref := (input.lhs.cast ⋯).getRef idx hidx },
        assign⟧ =
      lhs.getLsb idx
Theorem: BVPred.mkUlt_denote_eq_eval_ult
Proof state before:
case e_a.hleft
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
w : Nat
aig : AIG α
lhs rhs : BitVec w
input : aig.BinaryRefStream w
assign : α → Bool
hleft : ∀ (idx : Nat) (hidx : idx < w), ⟦{ aig := aig, ref := input.lhs.getRef idx hidx }, assign⟧ = lhs.getLsb idx
hright : ∀ (idx : Nat) (hidx : idx < w), ⟦{ aig := aig, ref := input.rhs.getRef idx hidx }, assign⟧ = rhs.getLsb idx
⊢ ∀ (idx : Nat) (hidx : idx < w),
    ⟦{ aig := ((BVExpr.bitblast.blastNot aig input.rhs).aig.mkConstCached true).aig,
          ref := (input.lhs.cast ⋯).getRef idx hidx },
        assign⟧ =
      lhs.getLsb idx
Tactic:
intro idx hidx
Proof state after:
case e_a.hleft
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
w : Nat
aig : AIG α
lhs rhs : BitVec w
input : aig.BinaryRefStream w
assign : α → Bool
hleft : ∀ (idx : Nat) (hidx : idx < w), ⟦{ aig := aig, ref := input.lhs.getRef idx hidx }, assign⟧ = lhs.getLsb idx
hright : ∀ (idx : Nat) (hidx : idx < w), ⟦{ aig := aig, ref := input.rhs.getRef idx hidx }, assign⟧ = rhs.getLsb idx
idx : Nat
hidx : idx < w
⊢ ⟦{ aig := ((BVExpr.bitblast.blastNot aig input.rhs).aig.mkConstCached true).aig,
        ref := (input.lhs.cast ⋯).getRef idx hidx },
      assign⟧ =
    lhs.getLsb idx
Theorem: BVPred.mkUlt_denote_eq_eval_ult
Proof state before:
case e_a.hleft
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
w : Nat
aig : AIG α
lhs rhs : BitVec w
input : aig.BinaryRefStream w
assign : α → Bool
hleft : ∀ (idx : Nat) (hidx : idx < w), ⟦{ aig := aig, ref := input.lhs.getRef idx hidx }, assign⟧ = lhs.getLsb idx
hright : ∀ (idx : Nat) (hidx : idx < w), ⟦{ aig := aig, ref := input.rhs.getRef idx hidx }, assign⟧ = rhs.getLsb idx
idx : Nat
hidx : idx < w
⊢ ⟦{ aig := ((BVExpr.bitblast.blastNot aig input.rhs).aig.mkConstCached true).aig,
        ref := (input.lhs.cast ⋯).getRef idx hidx },
      assign⟧ =
    lhs.getLsb idx
Tactic:
rw [AIG.LawfulOperator.denote_mem_prefix (f := AIG.mkConstCached)]
Proof state after:
case e_a.hleft
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
w : Nat
aig : AIG α
lhs rhs : BitVec w
input : aig.BinaryRefStream w
assign : α → Bool
hleft : ∀ (idx : Nat) (hidx : idx < w), ⟦{ aig := aig, ref := input.lhs.getRef idx hidx }, assign⟧ = lhs.getLsb idx
hright : ∀ (idx : Nat) (hidx : idx < w), ⟦{ aig := aig, ref := input.rhs.getRef idx hidx }, assign⟧ = rhs.getLsb idx
idx : Nat
hidx : idx < w
⊢ ⟦{ aig := (BVExpr.bitblast.blastNot aig input.rhs).aig,
        ref := { gate := ((input.lhs.cast ⋯).getRef idx hidx).gate, hgate := ?e_a.hleft✝ } },
      assign⟧ =
    lhs.getLsb idx

case e_a.hleft
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
w : Nat
aig : AIG α
lhs rhs : BitVec w
input : aig.BinaryRefStream w
assign : α → Bool
hleft : ∀ (idx : Nat) (hidx : idx < w), ⟦{ aig := aig, ref := input.lhs.getRef idx hidx }, assign⟧ = lhs.getLsb idx
hright : ∀ (idx : Nat) (hidx : idx < w), ⟦{ aig := aig, ref := input.rhs.getRef idx hidx }, assign⟧ = rhs.getLsb idx
idx : Nat
hidx : idx < w
⊢ ((input.lhs.cast ⋯).getRef idx hidx).gate < (BVExpr.bitblast.blastNot aig input.rhs).aig.decls.size
Theorem: BVPred.mkUlt_denote_eq_eval_ult
Proof state before:
case e_a.hleft
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
w : Nat
aig : AIG α
lhs rhs : BitVec w
input : aig.BinaryRefStream w
assign : α → Bool
hleft : ∀ (idx : Nat) (hidx : idx < w), ⟦{ aig := aig, ref := input.lhs.getRef idx hidx }, assign⟧ = lhs.getLsb idx
hright : ∀ (idx : Nat) (hidx : idx < w), ⟦{ aig := aig, ref := input.rhs.getRef idx hidx }, assign⟧ = rhs.getLsb idx
idx : Nat
hidx : idx < w
⊢ ⟦{ aig := (BVExpr.bitblast.blastNot aig input.rhs).aig,
        ref := { gate := ((input.lhs.cast ⋯).getRef idx hidx).gate, hgate := ?e_a.hleft✝ } },
      assign⟧ =
    lhs.getLsb idx

case e_a.hleft
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
w : Nat
aig : AIG α
lhs rhs : BitVec w
input : aig.BinaryRefStream w
assign : α → Bool
hleft : ∀ (idx : Nat) (hidx : idx < w), ⟦{ aig := aig, ref := input.lhs.getRef idx hidx }, assign⟧ = lhs.getLsb idx
hright : ∀ (idx : Nat) (hidx : idx < w), ⟦{ aig := aig, ref := input.rhs.getRef idx hidx }, assign⟧ = rhs.getLsb idx
idx : Nat
hidx : idx < w
⊢ ((input.lhs.cast ⋯).getRef idx hidx).gate < (BVExpr.bitblast.blastNot aig input.rhs).aig.decls.size
Tactic:
rw [AIG.LawfulStreamOperator.denote_mem_prefix (f := BVExpr.bitblast.blastNot)]
Proof state after:
case e_a.hleft
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
w : Nat
aig : AIG α
lhs rhs : BitVec w
input : aig.BinaryRefStream w
assign : α → Bool
hleft : ∀ (idx : Nat) (hidx : idx < w), ⟦{ aig := aig, ref := input.lhs.getRef idx hidx }, assign⟧ = lhs.getLsb idx
hright : ∀ (idx : Nat) (hidx : idx < w), ⟦{ aig := aig, ref := input.rhs.getRef idx hidx }, assign⟧ = rhs.getLsb idx
idx : Nat
hidx : idx < w
⊢ ⟦{ aig := aig, ref := { gate := ((input.lhs.cast ⋯).getRef idx hidx).gate, hgate := ?e_a.hleft✝ } }, assign⟧ =
    lhs.getLsb idx

case e_a.hleft
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
w : Nat
aig : AIG α
lhs rhs : BitVec w
input : aig.BinaryRefStream w
assign : α → Bool
hleft : ∀ (idx : Nat) (hidx : idx < w), ⟦{ aig := aig, ref := input.lhs.getRef idx hidx }, assign⟧ = lhs.getLsb idx
hright : ∀ (idx : Nat) (hidx : idx < w), ⟦{ aig := aig, ref := input.rhs.getRef idx hidx }, assign⟧ = rhs.getLsb idx
idx : Nat
hidx : idx < w
⊢ ((input.lhs.cast ⋯).getRef idx hidx).gate < aig.decls.size
Theorem: BVPred.mkUlt_denote_eq_eval_ult
Proof state before:
case e_a.hleft
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
w : Nat
aig : AIG α
lhs rhs : BitVec w
input : aig.BinaryRefStream w
assign : α → Bool
hleft : ∀ (idx : Nat) (hidx : idx < w), ⟦{ aig := aig, ref := input.lhs.getRef idx hidx }, assign⟧ = lhs.getLsb idx
hright : ∀ (idx : Nat) (hidx : idx < w), ⟦{ aig := aig, ref := input.rhs.getRef idx hidx }, assign⟧ = rhs.getLsb idx
idx : Nat
hidx : idx < w
⊢ ⟦{ aig := aig, ref := { gate := ((input.lhs.cast ⋯).getRef idx hidx).gate, hgate := ?e_a.hleft✝ } }, assign⟧ =
    lhs.getLsb idx

case e_a.hleft
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
w : Nat
aig : AIG α
lhs rhs : BitVec w
input : aig.BinaryRefStream w
assign : α → Bool
hleft : ∀ (idx : Nat) (hidx : idx < w), ⟦{ aig := aig, ref := input.lhs.getRef idx hidx }, assign⟧ = lhs.getLsb idx
hright : ∀ (idx : Nat) (hidx : idx < w), ⟦{ aig := aig, ref := input.rhs.getRef idx hidx }, assign⟧ = rhs.getLsb idx
idx : Nat
hidx : idx < w
⊢ ((input.lhs.cast ⋯).getRef idx hidx).gate < aig.decls.size
Tactic:
apply hleft
Proof state after:
case e_a.hleft.hidx
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
w : Nat
aig : AIG α
lhs rhs : BitVec w
input : aig.BinaryRefStream w
assign : α → Bool
hleft : ∀ (idx : Nat) (hidx : idx < w), ⟦{ aig := aig, ref := input.lhs.getRef idx hidx }, assign⟧ = lhs.getLsb idx
hright : ∀ (idx : Nat) (hidx : idx < w), ⟦{ aig := aig, ref := input.rhs.getRef idx hidx }, assign⟧ = rhs.getLsb idx
idx : Nat
hidx : idx < w
⊢ idx < w
Theorem: BVPred.mkUlt_denote_eq_eval_ult
Proof state before:
case e_a.hleft.hidx
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
w : Nat
aig : AIG α
lhs rhs : BitVec w
input : aig.BinaryRefStream w
assign : α → Bool
hleft : ∀ (idx : Nat) (hidx : idx < w), ⟦{ aig := aig, ref := input.lhs.getRef idx hidx }, assign⟧ = lhs.getLsb idx
hright : ∀ (idx : Nat) (hidx : idx < w), ⟦{ aig := aig, ref := input.rhs.getRef idx hidx }, assign⟧ = rhs.getLsb idx
idx : Nat
hidx : idx < w
⊢ idx < w
Tactic:
assumption
Proof state after:
no goals
Theorem: BVPred.mkUlt_denote_eq_eval_ult
Proof state before:
case e_a.hright
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
w : Nat
aig : AIG α
lhs rhs : BitVec w
input : aig.BinaryRefStream w
assign : α → Bool
hleft : ∀ (idx : Nat) (hidx : idx < w), ⟦{ aig := aig, ref := input.lhs.getRef idx hidx }, assign⟧ = lhs.getLsb idx
hright : ∀ (idx : Nat) (hidx : idx < w), ⟦{ aig := aig, ref := input.rhs.getRef idx hidx }, assign⟧ = rhs.getLsb idx
⊢ ∀ (idx : Nat)
    (hidx :
      idx <
        { w := w, stream := { lhs := input.lhs.cast ⋯, rhs := (BVExpr.bitblast.blastNot aig input.rhs).stream.cast ⋯ },
            cin := ((BVExpr.bitblast.blastNot aig input.rhs).aig.mkConstCached true).ref }.w),
    ⟦{ aig := ((BVExpr.bitblast.blastNot aig input.rhs).aig.mkConstCached true).aig,
          ref :=
            { w := w,
                      stream :=
                        { lhs := input.lhs.cast ⋯, rhs := (BVExpr.bitblast.blastNot aig input.rhs).stream.cast ⋯ },
                      cin := ((BVExpr.bitblast.blastNot aig input.rhs).aig.mkConstCached true).ref }.stream.rhs.getRef
              idx hidx },
        assign⟧ =
      (~~~rhs).getLsb idx
Tactic:
dsimp
Proof state after:
case e_a.hright
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
w : Nat
aig : AIG α
lhs rhs : BitVec w
input : aig.BinaryRefStream w
assign : α → Bool
hleft : ∀ (idx : Nat) (hidx : idx < w), ⟦{ aig := aig, ref := input.lhs.getRef idx hidx }, assign⟧ = lhs.getLsb idx
hright : ∀ (idx : Nat) (hidx : idx < w), ⟦{ aig := aig, ref := input.rhs.getRef idx hidx }, assign⟧ = rhs.getLsb idx
⊢ ∀ (idx : Nat) (hidx : idx < w),
    ⟦{ aig := ((BVExpr.bitblast.blastNot aig input.rhs).aig.mkConstCached true).aig,
          ref := ((BVExpr.bitblast.blastNot aig input.rhs).stream.cast ⋯).getRef idx hidx },
        assign⟧ =
      (~~~rhs).getLsb idx
Theorem: BVPred.mkUlt_denote_eq_eval_ult
Proof state before:
case e_a.hright
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
w : Nat
aig : AIG α
lhs rhs : BitVec w
input : aig.BinaryRefStream w
assign : α → Bool
hleft : ∀ (idx : Nat) (hidx : idx < w), ⟦{ aig := aig, ref := input.lhs.getRef idx hidx }, assign⟧ = lhs.getLsb idx
hright : ∀ (idx : Nat) (hidx : idx < w), ⟦{ aig := aig, ref := input.rhs.getRef idx hidx }, assign⟧ = rhs.getLsb idx
⊢ ∀ (idx : Nat) (hidx : idx < w),
    ⟦{ aig := ((BVExpr.bitblast.blastNot aig input.rhs).aig.mkConstCached true).aig,
          ref := ((BVExpr.bitblast.blastNot aig input.rhs).stream.cast ⋯).getRef idx hidx },
        assign⟧ =
      (~~~rhs).getLsb idx
Tactic:
intro idx hidx
Proof state after:
case e_a.hright
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
w : Nat
aig : AIG α
lhs rhs : BitVec w
input : aig.BinaryRefStream w
assign : α → Bool
hleft : ∀ (idx : Nat) (hidx : idx < w), ⟦{ aig := aig, ref := input.lhs.getRef idx hidx }, assign⟧ = lhs.getLsb idx
hright : ∀ (idx : Nat) (hidx : idx < w), ⟦{ aig := aig, ref := input.rhs.getRef idx hidx }, assign⟧ = rhs.getLsb idx
idx : Nat
hidx : idx < w
⊢ ⟦{ aig := ((BVExpr.bitblast.blastNot aig input.rhs).aig.mkConstCached true).aig,
        ref := ((BVExpr.bitblast.blastNot aig input.rhs).stream.cast ⋯).getRef idx hidx },
      assign⟧ =
    (~~~rhs).getLsb idx
Theorem: BVPred.mkUlt_denote_eq_eval_ult
Proof state before:
case e_a.hright
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
w : Nat
aig : AIG α
lhs rhs : BitVec w
input : aig.BinaryRefStream w
assign : α → Bool
hleft : ∀ (idx : Nat) (hidx : idx < w), ⟦{ aig := aig, ref := input.lhs.getRef idx hidx }, assign⟧ = lhs.getLsb idx
hright : ∀ (idx : Nat) (hidx : idx < w), ⟦{ aig := aig, ref := input.rhs.getRef idx hidx }, assign⟧ = rhs.getLsb idx
idx : Nat
hidx : idx < w
⊢ ⟦{ aig := ((BVExpr.bitblast.blastNot aig input.rhs).aig.mkConstCached true).aig,
        ref := ((BVExpr.bitblast.blastNot aig input.rhs).stream.cast ⋯).getRef idx hidx },
      assign⟧ =
    (~~~rhs).getLsb idx
Tactic:
rw [AIG.LawfulOperator.denote_mem_prefix (f := AIG.mkConstCached)]
Proof state after:
case e_a.hright
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
w : Nat
aig : AIG α
lhs rhs : BitVec w
input : aig.BinaryRefStream w
assign : α → Bool
hleft : ∀ (idx : Nat) (hidx : idx < w), ⟦{ aig := aig, ref := input.lhs.getRef idx hidx }, assign⟧ = lhs.getLsb idx
hright : ∀ (idx : Nat) (hidx : idx < w), ⟦{ aig := aig, ref := input.rhs.getRef idx hidx }, assign⟧ = rhs.getLsb idx
idx : Nat
hidx : idx < w
⊢ ⟦{ aig := (BVExpr.bitblast.blastNot aig input.rhs).aig,
        ref :=
          { gate := (((BVExpr.bitblast.blastNot aig input.rhs).stream.cast ⋯).getRef idx hidx).gate,
            hgate := ?e_a.hright✝ } },
      assign⟧ =
    (~~~rhs).getLsb idx

case e_a.hright
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
w : Nat
aig : AIG α
lhs rhs : BitVec w
input : aig.BinaryRefStream w
assign : α → Bool
hleft : ∀ (idx : Nat) (hidx : idx < w), ⟦{ aig := aig, ref := input.lhs.getRef idx hidx }, assign⟧ = lhs.getLsb idx
hright : ∀ (idx : Nat) (hidx : idx < w), ⟦{ aig := aig, ref := input.rhs.getRef idx hidx }, assign⟧ = rhs.getLsb idx
idx : Nat
hidx : idx < w
⊢ (((BVExpr.bitblast.blastNot aig input.rhs).stream.cast ⋯).getRef idx hidx).gate <
    (BVExpr.bitblast.blastNot aig input.rhs).aig.decls.size
Theorem: BVPred.mkUlt_denote_eq_eval_ult
Proof state before:
case e_a.hright
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
w : Nat
aig : AIG α
lhs rhs : BitVec w
input : aig.BinaryRefStream w
assign : α → Bool
hleft : ∀ (idx : Nat) (hidx : idx < w), ⟦{ aig := aig, ref := input.lhs.getRef idx hidx }, assign⟧ = lhs.getLsb idx
hright : ∀ (idx : Nat) (hidx : idx < w), ⟦{ aig := aig, ref := input.rhs.getRef idx hidx }, assign⟧ = rhs.getLsb idx
idx : Nat
hidx : idx < w
⊢ ⟦{ aig := (BVExpr.bitblast.blastNot aig input.rhs).aig,
        ref :=
          { gate := (((BVExpr.bitblast.blastNot aig input.rhs).stream.cast ⋯).getRef idx hidx).gate,
            hgate := ?e_a.hright✝ } },
      assign⟧ =
    (~~~rhs).getLsb idx

case e_a.hright
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
w : Nat
aig : AIG α
lhs rhs : BitVec w
input : aig.BinaryRefStream w
assign : α → Bool
hleft : ∀ (idx : Nat) (hidx : idx < w), ⟦{ aig := aig, ref := input.lhs.getRef idx hidx }, assign⟧ = lhs.getLsb idx
hright : ∀ (idx : Nat) (hidx : idx < w), ⟦{ aig := aig, ref := input.rhs.getRef idx hidx }, assign⟧ = rhs.getLsb idx
idx : Nat
hidx : idx < w
⊢ (((BVExpr.bitblast.blastNot aig input.rhs).stream.cast ⋯).getRef idx hidx).gate <
    (BVExpr.bitblast.blastNot aig input.rhs).aig.decls.size
Tactic:
. simp only [RefStream.getRef_cast, Ref_cast', BitVec.getLsb_not, hidx, decide_True,
    Bool.true_and]
  rw [BVExpr.bitblast.blastNot_eq_eval_getLsb]
  congr 1
  apply hright
Proof state after:
case e_a.hright
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
w : Nat
aig : AIG α
lhs rhs : BitVec w
input : aig.BinaryRefStream w
assign : α → Bool
hleft : ∀ (idx : Nat) (hidx : idx < w), ⟦{ aig := aig, ref := input.lhs.getRef idx hidx }, assign⟧ = lhs.getLsb idx
hright : ∀ (idx : Nat) (hidx : idx < w), ⟦{ aig := aig, ref := input.rhs.getRef idx hidx }, assign⟧ = rhs.getLsb idx
idx : Nat
hidx : idx < w
⊢ (((BVExpr.bitblast.blastNot aig input.rhs).stream.cast ⋯).getRef idx hidx).gate <
    (BVExpr.bitblast.blastNot aig input.rhs).aig.decls.size