unfold mkUlt
α : 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 := (mkUlt aig input).aig, ref := (mkUlt aig input).ref }, assign⟧ = !BitVec.carry w lhs (~~~rhs) true
α : 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