Theorem: BVExpr.bitblast.mkOverflowBit.go_eq_carry (LeanSAT/Reflect/BVExpr/BitBlast/Lemmas/Carry.lean)

State before:
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
w : Nat
aig : AIG α
curr : Nat
hcurr : curr ≤ w
cin origCin : aig.Ref
lhs rhs : aig.RefStream w
lhsExpr rhsExpr : BitVec w
assign : α → Bool
hleft : ∀ (idx : Nat) (hidx : idx < w), ⟦{ aig := aig, ref := lhs.getRef idx hidx }, assign⟧ = lhsExpr.getLsb idx
hright : ∀ (idx : Nat) (hidx : idx < w), ⟦{ aig := aig, ref := rhs.getRef idx hidx }, assign⟧ = rhsExpr.getLsb idx
hcin : ⟦{ aig := aig, ref := cin }, assign⟧ = BitVec.carry curr lhsExpr rhsExpr ⟦{ aig := aig, ref := origCin }, assign⟧
⊢ ⟦go aig curr hcurr cin lhs rhs, assign⟧ = BitVec.carry w lhsExpr rhsExpr ⟦{ aig := aig, ref := origCin }, assign⟧
Tactic:
unfold go
State after:
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
w : Nat
aig : AIG α
curr : Nat
hcurr : curr ≤ w
cin origCin : aig.Ref
lhs rhs : aig.RefStream w
lhsExpr rhsExpr : BitVec w
assign : α → Bool
hleft : ∀ (idx : Nat) (hidx : idx < w), ⟦{ aig := aig, ref := lhs.getRef idx hidx }, assign⟧ = lhsExpr.getLsb idx
hright : ∀ (idx : Nat) (hidx : idx < w), ⟦{ aig := aig, ref := rhs.getRef idx hidx }, assign⟧ = rhsExpr.getLsb idx
hcin : ⟦{ aig := aig, ref := cin }, assign⟧ = BitVec.carry curr lhsExpr rhsExpr ⟦{ aig := aig, ref := origCin }, assign⟧
⊢ ⟦if hidx : curr < w then
        let lin := lhs.getRef curr hidx;
        let rin := rhs.getRef curr hidx;
        let res := mkFullAdderCarry aig { lhs := lin, rhs := rin, cin := cin };
        let_fun this := ⋯;
        let aig_1 := res.aig;
        let carryRef := res.ref;
        let lhs_1 := lhs.cast this;
        let rhs_1 := rhs.cast this;
        go aig_1 (curr + 1) ⋯ carryRef lhs_1 rhs_1
      else { aig := aig, ref := cin },
      assign⟧ =
    BitVec.carry w lhsExpr rhsExpr ⟦{ aig := aig, ref := origCin }, assign⟧

State before:
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
w : Nat
aig : AIG α
curr : Nat
hcurr : curr ≤ w
cin origCin : aig.Ref
lhs rhs : aig.RefStream w
lhsExpr rhsExpr : BitVec w
assign : α → Bool
hleft : ∀ (idx : Nat) (hidx : idx < w), ⟦{ aig := aig, ref := lhs.getRef idx hidx }, assign⟧ = lhsExpr.getLsb idx
hright : ∀ (idx : Nat) (hidx : idx < w), ⟦{ aig := aig, ref := rhs.getRef idx hidx }, assign⟧ = rhsExpr.getLsb idx
hcin : ⟦{ aig := aig, ref := cin }, assign⟧ = BitVec.carry curr lhsExpr rhsExpr ⟦{ aig := aig, ref := origCin }, assign⟧
⊢ ⟦if hidx : curr < w then
        let lin := lhs.getRef curr hidx;
        let rin := rhs.getRef curr hidx;
        let res := mkFullAdderCarry aig { lhs := lin, rhs := rin, cin := cin };
        let_fun this := ⋯;
        let aig_1 := res.aig;
        let carryRef := res.ref;
        let lhs_1 := lhs.cast this;
        let rhs_1 := rhs.cast this;
        go aig_1 (curr + 1) ⋯ carryRef lhs_1 rhs_1
      else { aig := aig, ref := cin },
      assign⟧ =
    BitVec.carry w lhsExpr rhsExpr ⟦{ aig := aig, ref := origCin }, assign⟧
Tactic:
dsimp
State after:
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
w : Nat
aig : AIG α
curr : Nat
hcurr : curr ≤ w
cin origCin : aig.Ref
lhs rhs : aig.RefStream w
lhsExpr rhsExpr : BitVec w
assign : α → Bool
hleft : ∀ (idx : Nat) (hidx : idx < w), ⟦{ aig := aig, ref := lhs.getRef idx hidx }, assign⟧ = lhsExpr.getLsb idx
hright : ∀ (idx : Nat) (hidx : idx < w), ⟦{ aig := aig, ref := rhs.getRef idx hidx }, assign⟧ = rhsExpr.getLsb idx
hcin : ⟦{ aig := aig, ref := cin }, assign⟧ = BitVec.carry curr lhsExpr rhsExpr ⟦{ aig := aig, ref := origCin }, assign⟧
⊢ ⟦if hidx : curr < w then
        go (mkFullAdderCarry aig { lhs := lhs.getRef curr hidx, rhs := rhs.getRef curr hidx, cin := cin }).aig
          (curr + 1) ⋯
          (mkFullAdderCarry aig { lhs := lhs.getRef curr hidx, rhs := rhs.getRef curr hidx, cin := cin }).ref
          (lhs.cast ⋯) (rhs.cast ⋯)
      else { aig := aig, ref := cin },
      assign⟧ =
    BitVec.carry w lhsExpr rhsExpr ⟦{ aig := aig, ref := origCin }, assign⟧

State before:
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
w : Nat
aig : AIG α
curr : Nat
hcurr : curr ≤ w
cin origCin : aig.Ref
lhs rhs : aig.RefStream w
lhsExpr rhsExpr : BitVec w
assign : α → Bool
hleft : ∀ (idx : Nat) (hidx : idx < w), ⟦{ aig := aig, ref := lhs.getRef idx hidx }, assign⟧ = lhsExpr.getLsb idx
hright : ∀ (idx : Nat) (hidx : idx < w), ⟦{ aig := aig, ref := rhs.getRef idx hidx }, assign⟧ = rhsExpr.getLsb idx
hcin : ⟦{ aig := aig, ref := cin }, assign⟧ = BitVec.carry curr lhsExpr rhsExpr ⟦{ aig := aig, ref := origCin }, assign⟧
⊢ ⟦if hidx : curr < w then
        go (mkFullAdderCarry aig { lhs := lhs.getRef curr hidx, rhs := rhs.getRef curr hidx, cin := cin }).aig
          (curr + 1) ⋯
          (mkFullAdderCarry aig { lhs := lhs.getRef curr hidx, rhs := rhs.getRef curr hidx, cin := cin }).ref
          (lhs.cast ⋯) (rhs.cast ⋯)
      else { aig := aig, ref := cin },
      assign⟧ =
    BitVec.carry w lhsExpr rhsExpr ⟦{ aig := aig, ref := origCin }, assign⟧
Tactic:
split
State after:
case isTrue
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
w : Nat
aig : AIG α
curr : Nat
hcurr : curr ≤ w
cin origCin : aig.Ref
lhs rhs : aig.RefStream w
lhsExpr rhsExpr : BitVec w
assign : α → Bool
hleft : ∀ (idx : Nat) (hidx : idx < w), ⟦{ aig := aig, ref := lhs.getRef idx hidx }, assign⟧ = lhsExpr.getLsb idx
hright : ∀ (idx : Nat) (hidx : idx < w), ⟦{ aig := aig, ref := rhs.getRef idx hidx }, assign⟧ = rhsExpr.getLsb idx
hcin : ⟦{ aig := aig, ref := cin }, assign⟧ = BitVec.carry curr lhsExpr rhsExpr ⟦{ aig := aig, ref := origCin }, assign⟧
h✝ : curr < w
⊢ ⟦go (mkFullAdderCarry aig { lhs := lhs.getRef curr h✝, rhs := rhs.getRef curr h✝, cin := cin }).aig (curr + 1) ⋯
        (mkFullAdderCarry aig { lhs := lhs.getRef curr h✝, rhs := rhs.getRef curr h✝, cin := cin }).ref (lhs.cast ⋯)
        (rhs.cast ⋯),
      assign⟧ =
    BitVec.carry w lhsExpr rhsExpr ⟦{ aig := aig, ref := origCin }, assign⟧

case isFalse
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
w : Nat
aig : AIG α
curr : Nat
hcurr : curr ≤ w
cin origCin : aig.Ref
lhs rhs : aig.RefStream w
lhsExpr rhsExpr : BitVec w
assign : α → Bool
hleft : ∀ (idx : Nat) (hidx : idx < w), ⟦{ aig := aig, ref := lhs.getRef idx hidx }, assign⟧ = lhsExpr.getLsb idx
hright : ∀ (idx : Nat) (hidx : idx < w), ⟦{ aig := aig, ref := rhs.getRef idx hidx }, assign⟧ = rhsExpr.getLsb idx
hcin : ⟦{ aig := aig, ref := cin }, assign⟧ = BitVec.carry curr lhsExpr rhsExpr ⟦{ aig := aig, ref := origCin }, assign⟧
h✝ : ¬curr < w
⊢ ⟦{ aig := aig, ref := cin }, assign⟧ = BitVec.carry w lhsExpr rhsExpr ⟦{ aig := aig, ref := origCin }, assign⟧

State before:
case isTrue
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
w : Nat
aig : AIG α
curr : Nat
hcurr : curr ≤ w
cin origCin : aig.Ref
lhs rhs : aig.RefStream w
lhsExpr rhsExpr : BitVec w
assign : α → Bool
hleft : ∀ (idx : Nat) (hidx : idx < w), ⟦{ aig := aig, ref := lhs.getRef idx hidx }, assign⟧ = lhsExpr.getLsb idx
hright : ∀ (idx : Nat) (hidx : idx < w), ⟦{ aig := aig, ref := rhs.getRef idx hidx }, assign⟧ = rhsExpr.getLsb idx
hcin : ⟦{ aig := aig, ref := cin }, assign⟧ = BitVec.carry curr lhsExpr rhsExpr ⟦{ aig := aig, ref := origCin }, assign⟧
h✝ : curr < w
⊢ ⟦go (mkFullAdderCarry aig { lhs := lhs.getRef curr h✝, rhs := rhs.getRef curr h✝, cin := cin }).aig (curr + 1) ⋯
        (mkFullAdderCarry aig { lhs := lhs.getRef curr h✝, rhs := rhs.getRef curr h✝, cin := cin }).ref (lhs.cast ⋯)
        (rhs.cast ⋯),
      assign⟧ =
    BitVec.carry w lhsExpr rhsExpr ⟦{ aig := aig, ref := origCin }, assign⟧

case isFalse
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
w : Nat
aig : AIG α
curr : Nat
hcurr : curr ≤ w
cin origCin : aig.Ref
lhs rhs : aig.RefStream w
lhsExpr rhsExpr : BitVec w
assign : α → Bool
hleft : ∀ (idx : Nat) (hidx : idx < w), ⟦{ aig := aig, ref := lhs.getRef idx hidx }, assign⟧ = lhsExpr.getLsb idx
hright : ∀ (idx : Nat) (hidx : idx < w), ⟦{ aig := aig, ref := rhs.getRef idx hidx }, assign⟧ = rhsExpr.getLsb idx
hcin : ⟦{ aig := aig, ref := cin }, assign⟧ = BitVec.carry curr lhsExpr rhsExpr ⟦{ aig := aig, ref := origCin }, assign⟧
h✝ : ¬curr < w
⊢ ⟦{ aig := aig, ref := cin }, assign⟧ = BitVec.carry w lhsExpr rhsExpr ⟦{ aig := aig, ref := origCin }, assign⟧
Tactic:
. rw [go_eq_carry]
  . congr 1
    rw [AIG.LawfulOperator.denote_mem_prefix (f := mkFullAdderCarry)]
  . intros
    rw [AIG.LawfulOperator.denote_mem_prefix (f := mkFullAdderCarry)]
    . simp [hleft]
    . simp [Ref.hgate]
  . intros
    rw [AIG.LawfulOperator.denote_mem_prefix (f := mkFullAdderCarry)]
    . simp [hright]
    . simp [Ref.hgate]
  . simp [BitVec.carry_succ]
    rw [AIG.LawfulOperator.denote_mem_prefix (f := mkFullAdderCarry)]
    rw [hleft, hright, hcin]
    rw [Bool.atLeastTwo_eq_halfAdder]
State after:
case isFalse
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
w : Nat
aig : AIG α
curr : Nat
hcurr : curr ≤ w
cin origCin : aig.Ref
lhs rhs : aig.RefStream w
lhsExpr rhsExpr : BitVec w
assign : α → Bool
hleft : ∀ (idx : Nat) (hidx : idx < w), ⟦{ aig := aig, ref := lhs.getRef idx hidx }, assign⟧ = lhsExpr.getLsb idx
hright : ∀ (idx : Nat) (hidx : idx < w), ⟦{ aig := aig, ref := rhs.getRef idx hidx }, assign⟧ = rhsExpr.getLsb idx
hcin : ⟦{ aig := aig, ref := cin }, assign⟧ = BitVec.carry curr lhsExpr rhsExpr ⟦{ aig := aig, ref := origCin }, assign⟧
h✝ : ¬curr < w
⊢ ⟦{ aig := aig, ref := cin }, assign⟧ = BitVec.carry w lhsExpr rhsExpr ⟦{ aig := aig, ref := origCin }, assign⟧

State before:
case isFalse
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
w : Nat
aig : AIG α
curr : Nat
hcurr : curr ≤ w
cin origCin : aig.Ref
lhs rhs : aig.RefStream w
lhsExpr rhsExpr : BitVec w
assign : α → Bool
hleft : ∀ (idx : Nat) (hidx : idx < w), ⟦{ aig := aig, ref := lhs.getRef idx hidx }, assign⟧ = lhsExpr.getLsb idx
hright : ∀ (idx : Nat) (hidx : idx < w), ⟦{ aig := aig, ref := rhs.getRef idx hidx }, assign⟧ = rhsExpr.getLsb idx
hcin : ⟦{ aig := aig, ref := cin }, assign⟧ = BitVec.carry curr lhsExpr rhsExpr ⟦{ aig := aig, ref := origCin }, assign⟧
h✝ : ¬curr < w
⊢ ⟦{ aig := aig, ref := cin }, assign⟧ = BitVec.carry w lhsExpr rhsExpr ⟦{ aig := aig, ref := origCin }, assign⟧
Tactic:
. have : w = curr := by omega
  rw [hcin]
  simp [this]
State after:
no goals

State before:
case isTrue
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
w : Nat
aig : AIG α
curr : Nat
hcurr : curr ≤ w
cin origCin : aig.Ref
lhs rhs : aig.RefStream w
lhsExpr rhsExpr : BitVec w
assign : α → Bool
hleft : ∀ (idx : Nat) (hidx : idx < w), ⟦{ aig := aig, ref := lhs.getRef idx hidx }, assign⟧ = lhsExpr.getLsb idx
hright : ∀ (idx : Nat) (hidx : idx < w), ⟦{ aig := aig, ref := rhs.getRef idx hidx }, assign⟧ = rhsExpr.getLsb idx
hcin : ⟦{ aig := aig, ref := cin }, assign⟧ = BitVec.carry curr lhsExpr rhsExpr ⟦{ aig := aig, ref := origCin }, assign⟧
h✝ : curr < w
⊢ ⟦go (mkFullAdderCarry aig { lhs := lhs.getRef curr h✝, rhs := rhs.getRef curr h✝, cin := cin }).aig (curr + 1) ⋯
        (mkFullAdderCarry aig { lhs := lhs.getRef curr h✝, rhs := rhs.getRef curr h✝, cin := cin }).ref (lhs.cast ⋯)
        (rhs.cast ⋯),
      assign⟧ =
    BitVec.carry w lhsExpr rhsExpr ⟦{ aig := aig, ref := origCin }, assign⟧
Tactic:
rw [go_eq_carry]
State after:
case isTrue
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
w : Nat
aig : AIG α
curr : Nat
hcurr : curr ≤ w
cin origCin : aig.Ref
lhs rhs : aig.RefStream w
lhsExpr rhsExpr : BitVec w
assign : α → Bool
hleft : ∀ (idx : Nat) (hidx : idx < w), ⟦{ aig := aig, ref := lhs.getRef idx hidx }, assign⟧ = lhsExpr.getLsb idx
hright : ∀ (idx : Nat) (hidx : idx < w), ⟦{ aig := aig, ref := rhs.getRef idx hidx }, assign⟧ = rhsExpr.getLsb idx
hcin : ⟦{ aig := aig, ref := cin }, assign⟧ = BitVec.carry curr lhsExpr rhsExpr ⟦{ aig := aig, ref := origCin }, assign⟧
h✝ : curr < w
⊢ BitVec.carry w ?isTrue.lhsExpr ?isTrue.rhsExpr
      ⟦{ aig := (mkFullAdderCarry aig { lhs := lhs.getRef curr h✝, rhs := rhs.getRef curr h✝, cin := cin }).aig,
          ref := ?isTrue.origCin },
        assign⟧ =
    BitVec.carry w lhsExpr rhsExpr ⟦{ aig := aig, ref := origCin }, assign⟧

case isTrue.origCin
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
w : Nat
aig : AIG α
curr : Nat
hcurr : curr ≤ w
cin origCin : aig.Ref
lhs rhs : aig.RefStream w
lhsExpr rhsExpr : BitVec w
assign : α → Bool
hleft : ∀ (idx : Nat) (hidx : idx < w), ⟦{ aig := aig, ref := lhs.getRef idx hidx }, assign⟧ = lhsExpr.getLsb idx
hright : ∀ (idx : Nat) (hidx : idx < w), ⟦{ aig := aig, ref := rhs.getRef idx hidx }, assign⟧ = rhsExpr.getLsb idx
hcin : ⟦{ aig := aig, ref := cin }, assign⟧ = BitVec.carry curr lhsExpr rhsExpr ⟦{ aig := aig, ref := origCin }, assign⟧
h✝ : curr < w
⊢ (mkFullAdderCarry aig { lhs := lhs.getRef curr h✝, rhs := rhs.getRef curr h✝, cin := cin }).aig.Ref

case isTrue.lhsExpr
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
w : Nat
aig : AIG α
curr : Nat
hcurr : curr ≤ w
cin origCin : aig.Ref
lhs rhs : aig.RefStream w
lhsExpr rhsExpr : BitVec w
assign : α → Bool
hleft : ∀ (idx : Nat) (hidx : idx < w), ⟦{ aig := aig, ref := lhs.getRef idx hidx }, assign⟧ = lhsExpr.getLsb idx
hright : ∀ (idx : Nat) (hidx : idx < w), ⟦{ aig := aig, ref := rhs.getRef idx hidx }, assign⟧ = rhsExpr.getLsb idx
hcin : ⟦{ aig := aig, ref := cin }, assign⟧ = BitVec.carry curr lhsExpr rhsExpr ⟦{ aig := aig, ref := origCin }, assign⟧
h✝ : curr < w
⊢ BitVec w

case isTrue.rhsExpr
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
w : Nat
aig : AIG α
curr : Nat
hcurr : curr ≤ w
cin origCin : aig.Ref
lhs rhs : aig.RefStream w
lhsExpr rhsExpr : BitVec w
assign : α → Bool
hleft : ∀ (idx : Nat) (hidx : idx < w), ⟦{ aig := aig, ref := lhs.getRef idx hidx }, assign⟧ = lhsExpr.getLsb idx
hright : ∀ (idx : Nat) (hidx : idx < w), ⟦{ aig := aig, ref := rhs.getRef idx hidx }, assign⟧ = rhsExpr.getLsb idx
hcin : ⟦{ aig := aig, ref := cin }, assign⟧ = BitVec.carry curr lhsExpr rhsExpr ⟦{ aig := aig, ref := origCin }, assign⟧
h✝ : curr < w
⊢ BitVec w

case isTrue.hleft
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
w : Nat
aig : AIG α
curr : Nat
hcurr : curr ≤ w
cin origCin : aig.Ref
lhs rhs : aig.RefStream w
lhsExpr rhsExpr : BitVec w
assign : α → Bool
hleft : ∀ (idx : Nat) (hidx : idx < w), ⟦{ aig := aig, ref := lhs.getRef idx hidx }, assign⟧ = lhsExpr.getLsb idx
hright : ∀ (idx : Nat) (hidx : idx < w), ⟦{ aig := aig, ref := rhs.getRef idx hidx }, assign⟧ = rhsExpr.getLsb idx
hcin : ⟦{ aig := aig, ref := cin }, assign⟧ = BitVec.carry curr lhsExpr rhsExpr ⟦{ aig := aig, ref := origCin }, assign⟧
h✝ : curr < w
⊢ ∀ (idx : Nat) (hidx : idx < w),
    ⟦{ aig := (mkFullAdderCarry aig { lhs := lhs.getRef curr h✝, rhs := rhs.getRef curr h✝, cin := cin }).aig,
          ref := (lhs.cast ⋯).getRef idx hidx },
        assign⟧ =
      ?isTrue.lhsExpr.getLsb idx

case isTrue.hright
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
w : Nat
aig : AIG α
curr : Nat
hcurr : curr ≤ w
cin origCin : aig.Ref
lhs rhs : aig.RefStream w
lhsExpr rhsExpr : BitVec w
assign : α → Bool
hleft : ∀ (idx : Nat) (hidx : idx < w), ⟦{ aig := aig, ref := lhs.getRef idx hidx }, assign⟧ = lhsExpr.getLsb idx
hright : ∀ (idx : Nat) (hidx : idx < w), ⟦{ aig := aig, ref := rhs.getRef idx hidx }, assign⟧ = rhsExpr.getLsb idx
hcin : ⟦{ aig := aig, ref := cin }, assign⟧ = BitVec.carry curr lhsExpr rhsExpr ⟦{ aig := aig, ref := origCin }, assign⟧
h✝ : curr < w
⊢ ∀ (idx : Nat) (hidx : idx < w),
    ⟦{ aig := (mkFullAdderCarry aig { lhs := lhs.getRef curr h✝, rhs := rhs.getRef curr h✝, cin := cin }).aig,
          ref := (rhs.cast ⋯).getRef idx hidx },
        assign⟧ =
      ?isTrue.rhsExpr.getLsb idx

case isTrue.hcin
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
w : Nat
aig : AIG α
curr : Nat
hcurr : curr ≤ w
cin origCin : aig.Ref
lhs rhs : aig.RefStream w
lhsExpr rhsExpr : BitVec w
assign : α → Bool
hleft : ∀ (idx : Nat) (hidx : idx < w), ⟦{ aig := aig, ref := lhs.getRef idx hidx }, assign⟧ = lhsExpr.getLsb idx
hright : ∀ (idx : Nat) (hidx : idx < w), ⟦{ aig := aig, ref := rhs.getRef idx hidx }, assign⟧ = rhsExpr.getLsb idx
hcin : ⟦{ aig := aig, ref := cin }, assign⟧ = BitVec.carry curr lhsExpr rhsExpr ⟦{ aig := aig, ref := origCin }, assign⟧
h✝ : curr < w
⊢ ⟦{ aig := (mkFullAdderCarry aig { lhs := lhs.getRef curr h✝, rhs := rhs.getRef curr h✝, cin := cin }).aig,
        ref := (mkFullAdderCarry aig { lhs := lhs.getRef curr h✝, rhs := rhs.getRef curr h✝, cin := cin }).ref },
      assign⟧ =
    BitVec.carry (curr + 1) ?isTrue.lhsExpr ?isTrue.rhsExpr
      ⟦{ aig := (mkFullAdderCarry aig { lhs := lhs.getRef curr h✝, rhs := rhs.getRef curr h✝, cin := cin }).aig,
          ref := ?isTrue.origCin },
        assign⟧

State before:
case isTrue
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
w : Nat
aig : AIG α
curr : Nat
hcurr : curr ≤ w
cin origCin : aig.Ref
lhs rhs : aig.RefStream w
lhsExpr rhsExpr : BitVec w
assign : α → Bool
hleft : ∀ (idx : Nat) (hidx : idx < w), ⟦{ aig := aig, ref := lhs.getRef idx hidx }, assign⟧ = lhsExpr.getLsb idx
hright : ∀ (idx : Nat) (hidx : idx < w), ⟦{ aig := aig, ref := rhs.getRef idx hidx }, assign⟧ = rhsExpr.getLsb idx
hcin : ⟦{ aig := aig, ref := cin }, assign⟧ = BitVec.carry curr lhsExpr rhsExpr ⟦{ aig := aig, ref := origCin }, assign⟧
h✝ : curr < w
⊢ BitVec.carry w ?isTrue.lhsExpr ?isTrue.rhsExpr
      ⟦{ aig := (mkFullAdderCarry aig { lhs := lhs.getRef curr h✝, rhs := rhs.getRef curr h✝, cin := cin }).aig,
          ref := ?isTrue.origCin },
        assign⟧ =
    BitVec.carry w lhsExpr rhsExpr ⟦{ aig := aig, ref := origCin }, assign⟧

case isTrue.origCin
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
w : Nat
aig : AIG α
curr : Nat
hcurr : curr ≤ w
cin origCin : aig.Ref
lhs rhs : aig.RefStream w
lhsExpr rhsExpr : BitVec w
assign : α → Bool
hleft : ∀ (idx : Nat) (hidx : idx < w), ⟦{ aig := aig, ref := lhs.getRef idx hidx }, assign⟧ = lhsExpr.getLsb idx
hright : ∀ (idx : Nat) (hidx : idx < w), ⟦{ aig := aig, ref := rhs.getRef idx hidx }, assign⟧ = rhsExpr.getLsb idx
hcin : ⟦{ aig := aig, ref := cin }, assign⟧ = BitVec.carry curr lhsExpr rhsExpr ⟦{ aig := aig, ref := origCin }, assign⟧
h✝ : curr < w
⊢ (mkFullAdderCarry aig { lhs := lhs.getRef curr h✝, rhs := rhs.getRef curr h✝, cin := cin }).aig.Ref

case isTrue.lhsExpr
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
w : Nat
aig : AIG α
curr : Nat
hcurr : curr ≤ w
cin origCin : aig.Ref
lhs rhs : aig.RefStream w
lhsExpr rhsExpr : BitVec w
assign : α → Bool
hleft : ∀ (idx : Nat) (hidx : idx < w), ⟦{ aig := aig, ref := lhs.getRef idx hidx }, assign⟧ = lhsExpr.getLsb idx
hright : ∀ (idx : Nat) (hidx : idx < w), ⟦{ aig := aig, ref := rhs.getRef idx hidx }, assign⟧ = rhsExpr.getLsb idx
hcin : ⟦{ aig := aig, ref := cin }, assign⟧ = BitVec.carry curr lhsExpr rhsExpr ⟦{ aig := aig, ref := origCin }, assign⟧
h✝ : curr < w
⊢ BitVec w

case isTrue.rhsExpr
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
w : Nat
aig : AIG α
curr : Nat
hcurr : curr ≤ w
cin origCin : aig.Ref
lhs rhs : aig.RefStream w
lhsExpr rhsExpr : BitVec w
assign : α → Bool
hleft : ∀ (idx : Nat) (hidx : idx < w), ⟦{ aig := aig, ref := lhs.getRef idx hidx }, assign⟧ = lhsExpr.getLsb idx
hright : ∀ (idx : Nat) (hidx : idx < w), ⟦{ aig := aig, ref := rhs.getRef idx hidx }, assign⟧ = rhsExpr.getLsb idx
hcin : ⟦{ aig := aig, ref := cin }, assign⟧ = BitVec.carry curr lhsExpr rhsExpr ⟦{ aig := aig, ref := origCin }, assign⟧
h✝ : curr < w
⊢ BitVec w

case isTrue.hleft
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
w : Nat
aig : AIG α
curr : Nat
hcurr : curr ≤ w
cin origCin : aig.Ref
lhs rhs : aig.RefStream w
lhsExpr rhsExpr : BitVec w
assign : α → Bool
hleft : ∀ (idx : Nat) (hidx : idx < w), ⟦{ aig := aig, ref := lhs.getRef idx hidx }, assign⟧ = lhsExpr.getLsb idx
hright : ∀ (idx : Nat) (hidx : idx < w), ⟦{ aig := aig, ref := rhs.getRef idx hidx }, assign⟧ = rhsExpr.getLsb idx
hcin : ⟦{ aig := aig, ref := cin }, assign⟧ = BitVec.carry curr lhsExpr rhsExpr ⟦{ aig := aig, ref := origCin }, assign⟧
h✝ : curr < w
⊢ ∀ (idx : Nat) (hidx : idx < w),
    ⟦{ aig := (mkFullAdderCarry aig { lhs := lhs.getRef curr h✝, rhs := rhs.getRef curr h✝, cin := cin }).aig,
          ref := (lhs.cast ⋯).getRef idx hidx },
        assign⟧ =
      ?isTrue.lhsExpr.getLsb idx

case isTrue.hright
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
w : Nat
aig : AIG α
curr : Nat
hcurr : curr ≤ w
cin origCin : aig.Ref
lhs rhs : aig.RefStream w
lhsExpr rhsExpr : BitVec w
assign : α → Bool
hleft : ∀ (idx : Nat) (hidx : idx < w), ⟦{ aig := aig, ref := lhs.getRef idx hidx }, assign⟧ = lhsExpr.getLsb idx
hright : ∀ (idx : Nat) (hidx : idx < w), ⟦{ aig := aig, ref := rhs.getRef idx hidx }, assign⟧ = rhsExpr.getLsb idx
hcin : ⟦{ aig := aig, ref := cin }, assign⟧ = BitVec.carry curr lhsExpr rhsExpr ⟦{ aig := aig, ref := origCin }, assign⟧
h✝ : curr < w
⊢ ∀ (idx : Nat) (hidx : idx < w),
    ⟦{ aig := (mkFullAdderCarry aig { lhs := lhs.getRef curr h✝, rhs := rhs.getRef curr h✝, cin := cin }).aig,
          ref := (rhs.cast ⋯).getRef idx hidx },
        assign⟧ =
      ?isTrue.rhsExpr.getLsb idx

case isTrue.hcin
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
w : Nat
aig : AIG α
curr : Nat
hcurr : curr ≤ w
cin origCin : aig.Ref
lhs rhs : aig.RefStream w
lhsExpr rhsExpr : BitVec w
assign : α → Bool
hleft : ∀ (idx : Nat) (hidx : idx < w), ⟦{ aig := aig, ref := lhs.getRef idx hidx }, assign⟧ = lhsExpr.getLsb idx
hright : ∀ (idx : Nat) (hidx : idx < w), ⟦{ aig := aig, ref := rhs.getRef idx hidx }, assign⟧ = rhsExpr.getLsb idx
hcin : ⟦{ aig := aig, ref := cin }, assign⟧ = BitVec.carry curr lhsExpr rhsExpr ⟦{ aig := aig, ref := origCin }, assign⟧
h✝ : curr < w
⊢ ⟦{ aig := (mkFullAdderCarry aig { lhs := lhs.getRef curr h✝, rhs := rhs.getRef curr h✝, cin := cin }).aig,
        ref := (mkFullAdderCarry aig { lhs := lhs.getRef curr h✝, rhs := rhs.getRef curr h✝, cin := cin }).ref },
      assign⟧ =
    BitVec.carry (curr + 1) ?isTrue.lhsExpr ?isTrue.rhsExpr
      ⟦{ aig := (mkFullAdderCarry aig { lhs := lhs.getRef curr h✝, rhs := rhs.getRef curr h✝, cin := cin }).aig,
          ref := ?isTrue.origCin },
        assign⟧
Tactic:
. congr 1
  rw [AIG.LawfulOperator.denote_mem_prefix (f := mkFullAdderCarry)]
State after:
case isTrue.hleft
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
w : Nat
aig : AIG α
curr : Nat
hcurr : curr ≤ w
cin origCin : aig.Ref
lhs rhs : aig.RefStream w
lhsExpr rhsExpr : BitVec w
assign : α → Bool
hleft : ∀ (idx : Nat) (hidx : idx < w), ⟦{ aig := aig, ref := lhs.getRef idx hidx }, assign⟧ = lhsExpr.getLsb idx
hright : ∀ (idx : Nat) (hidx : idx < w), ⟦{ aig := aig, ref := rhs.getRef idx hidx }, assign⟧ = rhsExpr.getLsb idx
hcin : ⟦{ aig := aig, ref := cin }, assign⟧ = BitVec.carry curr lhsExpr rhsExpr ⟦{ aig := aig, ref := origCin }, assign⟧
h✝ : curr < w
⊢ ∀ (idx : Nat) (hidx : idx < w),
    ⟦{ aig := (mkFullAdderCarry aig { lhs := lhs.getRef curr h✝, rhs := rhs.getRef curr h✝, cin := cin }).aig,
          ref := (lhs.cast ⋯).getRef idx hidx },
        assign⟧ =
      lhsExpr.getLsb idx

case isTrue.hright
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
w : Nat
aig : AIG α
curr : Nat
hcurr : curr ≤ w
cin origCin : aig.Ref
lhs rhs : aig.RefStream w
lhsExpr rhsExpr : BitVec w
assign : α → Bool
hleft : ∀ (idx : Nat) (hidx : idx < w), ⟦{ aig := aig, ref := lhs.getRef idx hidx }, assign⟧ = lhsExpr.getLsb idx
hright : ∀ (idx : Nat) (hidx : idx < w), ⟦{ aig := aig, ref := rhs.getRef idx hidx }, assign⟧ = rhsExpr.getLsb idx
hcin : ⟦{ aig := aig, ref := cin }, assign⟧ = BitVec.carry curr lhsExpr rhsExpr ⟦{ aig := aig, ref := origCin }, assign⟧
h✝ : curr < w
⊢ ∀ (idx : Nat) (hidx : idx < w),
    ⟦{ aig := (mkFullAdderCarry aig { lhs := lhs.getRef curr h✝, rhs := rhs.getRef curr h✝, cin := cin }).aig,
          ref := (rhs.cast ⋯).getRef idx hidx },
        assign⟧ =
      rhsExpr.getLsb idx

case isTrue.hcin
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
w : Nat
aig : AIG α
curr : Nat
hcurr : curr ≤ w
cin origCin : aig.Ref
lhs rhs : aig.RefStream w
lhsExpr rhsExpr : BitVec w
assign : α → Bool
hleft : ∀ (idx : Nat) (hidx : idx < w), ⟦{ aig := aig, ref := lhs.getRef idx hidx }, assign⟧ = lhsExpr.getLsb idx
hright : ∀ (idx : Nat) (hidx : idx < w), ⟦{ aig := aig, ref := rhs.getRef idx hidx }, assign⟧ = rhsExpr.getLsb idx
hcin : ⟦{ aig := aig, ref := cin }, assign⟧ = BitVec.carry curr lhsExpr rhsExpr ⟦{ aig := aig, ref := origCin }, assign⟧
h✝ : curr < w
⊢ ⟦{ aig := (mkFullAdderCarry aig { lhs := lhs.getRef curr h✝, rhs := rhs.getRef curr h✝, cin := cin }).aig,
        ref := (mkFullAdderCarry aig { lhs := lhs.getRef curr h✝, rhs := rhs.getRef curr h✝, cin := cin }).ref },
      assign⟧ =
    BitVec.carry (curr + 1) lhsExpr rhsExpr
      ⟦{ aig := (mkFullAdderCarry aig { lhs := lhs.getRef curr h✝, rhs := rhs.getRef curr h✝, cin := cin }).aig,
          ref := { gate := origCin.gate, hgate := ⋯ } },
        assign⟧

State before:
case isTrue.hleft
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
w : Nat
aig : AIG α
curr : Nat
hcurr : curr ≤ w
cin origCin : aig.Ref
lhs rhs : aig.RefStream w
lhsExpr rhsExpr : BitVec w
assign : α → Bool
hleft : ∀ (idx : Nat) (hidx : idx < w), ⟦{ aig := aig, ref := lhs.getRef idx hidx }, assign⟧ = lhsExpr.getLsb idx
hright : ∀ (idx : Nat) (hidx : idx < w), ⟦{ aig := aig, ref := rhs.getRef idx hidx }, assign⟧ = rhsExpr.getLsb idx
hcin : ⟦{ aig := aig, ref := cin }, assign⟧ = BitVec.carry curr lhsExpr rhsExpr ⟦{ aig := aig, ref := origCin }, assign⟧
h✝ : curr < w
⊢ ∀ (idx : Nat) (hidx : idx < w),
    ⟦{ aig := (mkFullAdderCarry aig { lhs := lhs.getRef curr h✝, rhs := rhs.getRef curr h✝, cin := cin }).aig,
          ref := (lhs.cast ⋯).getRef idx hidx },
        assign⟧ =
      lhsExpr.getLsb idx

case isTrue.hright
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
w : Nat
aig : AIG α
curr : Nat
hcurr : curr ≤ w
cin origCin : aig.Ref
lhs rhs : aig.RefStream w
lhsExpr rhsExpr : BitVec w
assign : α → Bool
hleft : ∀ (idx : Nat) (hidx : idx < w), ⟦{ aig := aig, ref := lhs.getRef idx hidx }, assign⟧ = lhsExpr.getLsb idx
hright : ∀ (idx : Nat) (hidx : idx < w), ⟦{ aig := aig, ref := rhs.getRef idx hidx }, assign⟧ = rhsExpr.getLsb idx
hcin : ⟦{ aig := aig, ref := cin }, assign⟧ = BitVec.carry curr lhsExpr rhsExpr ⟦{ aig := aig, ref := origCin }, assign⟧
h✝ : curr < w
⊢ ∀ (idx : Nat) (hidx : idx < w),
    ⟦{ aig := (mkFullAdderCarry aig { lhs := lhs.getRef curr h✝, rhs := rhs.getRef curr h✝, cin := cin }).aig,
          ref := (rhs.cast ⋯).getRef idx hidx },
        assign⟧ =
      rhsExpr.getLsb idx

case isTrue.hcin
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
w : Nat
aig : AIG α
curr : Nat
hcurr : curr ≤ w
cin origCin : aig.Ref
lhs rhs : aig.RefStream w
lhsExpr rhsExpr : BitVec w
assign : α → Bool
hleft : ∀ (idx : Nat) (hidx : idx < w), ⟦{ aig := aig, ref := lhs.getRef idx hidx }, assign⟧ = lhsExpr.getLsb idx
hright : ∀ (idx : Nat) (hidx : idx < w), ⟦{ aig := aig, ref := rhs.getRef idx hidx }, assign⟧ = rhsExpr.getLsb idx
hcin : ⟦{ aig := aig, ref := cin }, assign⟧ = BitVec.carry curr lhsExpr rhsExpr ⟦{ aig := aig, ref := origCin }, assign⟧
h✝ : curr < w
⊢ ⟦{ aig := (mkFullAdderCarry aig { lhs := lhs.getRef curr h✝, rhs := rhs.getRef curr h✝, cin := cin }).aig,
        ref := (mkFullAdderCarry aig { lhs := lhs.getRef curr h✝, rhs := rhs.getRef curr h✝, cin := cin }).ref },
      assign⟧ =
    BitVec.carry (curr + 1) lhsExpr rhsExpr
      ⟦{ aig := (mkFullAdderCarry aig { lhs := lhs.getRef curr h✝, rhs := rhs.getRef curr h✝, cin := cin }).aig,
          ref := { gate := origCin.gate, hgate := ⋯ } },
        assign⟧
Tactic:
. intros
  rw [AIG.LawfulOperator.denote_mem_prefix (f := mkFullAdderCarry)]
  . simp [hleft]
  . simp [Ref.hgate]
State after:
case isTrue.hright
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
w : Nat
aig : AIG α
curr : Nat
hcurr : curr ≤ w
cin origCin : aig.Ref
lhs rhs : aig.RefStream w
lhsExpr rhsExpr : BitVec w
assign : α → Bool
hleft : ∀ (idx : Nat) (hidx : idx < w), ⟦{ aig := aig, ref := lhs.getRef idx hidx }, assign⟧ = lhsExpr.getLsb idx
hright : ∀ (idx : Nat) (hidx : idx < w), ⟦{ aig := aig, ref := rhs.getRef idx hidx }, assign⟧ = rhsExpr.getLsb idx
hcin : ⟦{ aig := aig, ref := cin }, assign⟧ = BitVec.carry curr lhsExpr rhsExpr ⟦{ aig := aig, ref := origCin }, assign⟧
h✝ : curr < w
⊢ ∀ (idx : Nat) (hidx : idx < w),
    ⟦{ aig := (mkFullAdderCarry aig { lhs := lhs.getRef curr h✝, rhs := rhs.getRef curr h✝, cin := cin }).aig,
          ref := (rhs.cast ⋯).getRef idx hidx },
        assign⟧ =
      rhsExpr.getLsb idx

case isTrue.hcin
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
w : Nat
aig : AIG α
curr : Nat
hcurr : curr ≤ w
cin origCin : aig.Ref
lhs rhs : aig.RefStream w
lhsExpr rhsExpr : BitVec w
assign : α → Bool
hleft : ∀ (idx : Nat) (hidx : idx < w), ⟦{ aig := aig, ref := lhs.getRef idx hidx }, assign⟧ = lhsExpr.getLsb idx
hright : ∀ (idx : Nat) (hidx : idx < w), ⟦{ aig := aig, ref := rhs.getRef idx hidx }, assign⟧ = rhsExpr.getLsb idx
hcin : ⟦{ aig := aig, ref := cin }, assign⟧ = BitVec.carry curr lhsExpr rhsExpr ⟦{ aig := aig, ref := origCin }, assign⟧
h✝ : curr < w
⊢ ⟦{ aig := (mkFullAdderCarry aig { lhs := lhs.getRef curr h✝, rhs := rhs.getRef curr h✝, cin := cin }).aig,
        ref := (mkFullAdderCarry aig { lhs := lhs.getRef curr h✝, rhs := rhs.getRef curr h✝, cin := cin }).ref },
      assign⟧ =
    BitVec.carry (curr + 1) lhsExpr rhsExpr
      ⟦{ aig := (mkFullAdderCarry aig { lhs := lhs.getRef curr h✝, rhs := rhs.getRef curr h✝, cin := cin }).aig,
          ref := { gate := origCin.gate, hgate := ⋯ } },
        assign⟧

State before:
case isTrue.hright
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
w : Nat
aig : AIG α
curr : Nat
hcurr : curr ≤ w
cin origCin : aig.Ref
lhs rhs : aig.RefStream w
lhsExpr rhsExpr : BitVec w
assign : α → Bool
hleft : ∀ (idx : Nat) (hidx : idx < w), ⟦{ aig := aig, ref := lhs.getRef idx hidx }, assign⟧ = lhsExpr.getLsb idx
hright : ∀ (idx : Nat) (hidx : idx < w), ⟦{ aig := aig, ref := rhs.getRef idx hidx }, assign⟧ = rhsExpr.getLsb idx
hcin : ⟦{ aig := aig, ref := cin }, assign⟧ = BitVec.carry curr lhsExpr rhsExpr ⟦{ aig := aig, ref := origCin }, assign⟧
h✝ : curr < w
⊢ ∀ (idx : Nat) (hidx : idx < w),
    ⟦{ aig := (mkFullAdderCarry aig { lhs := lhs.getRef curr h✝, rhs := rhs.getRef curr h✝, cin := cin }).aig,
          ref := (rhs.cast ⋯).getRef idx hidx },
        assign⟧ =
      rhsExpr.getLsb idx

case isTrue.hcin
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
w : Nat
aig : AIG α
curr : Nat
hcurr : curr ≤ w
cin origCin : aig.Ref
lhs rhs : aig.RefStream w
lhsExpr rhsExpr : BitVec w
assign : α → Bool
hleft : ∀ (idx : Nat) (hidx : idx < w), ⟦{ aig := aig, ref := lhs.getRef idx hidx }, assign⟧ = lhsExpr.getLsb idx
hright : ∀ (idx : Nat) (hidx : idx < w), ⟦{ aig := aig, ref := rhs.getRef idx hidx }, assign⟧ = rhsExpr.getLsb idx
hcin : ⟦{ aig := aig, ref := cin }, assign⟧ = BitVec.carry curr lhsExpr rhsExpr ⟦{ aig := aig, ref := origCin }, assign⟧
h✝ : curr < w
⊢ ⟦{ aig := (mkFullAdderCarry aig { lhs := lhs.getRef curr h✝, rhs := rhs.getRef curr h✝, cin := cin }).aig,
        ref := (mkFullAdderCarry aig { lhs := lhs.getRef curr h✝, rhs := rhs.getRef curr h✝, cin := cin }).ref },
      assign⟧ =
    BitVec.carry (curr + 1) lhsExpr rhsExpr
      ⟦{ aig := (mkFullAdderCarry aig { lhs := lhs.getRef curr h✝, rhs := rhs.getRef curr h✝, cin := cin }).aig,
          ref := { gate := origCin.gate, hgate := ⋯ } },
        assign⟧
Tactic:
. intros
  rw [AIG.LawfulOperator.denote_mem_prefix (f := mkFullAdderCarry)]
  . simp [hright]
  . simp [Ref.hgate]
State after:
case isTrue.hcin
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
w : Nat
aig : AIG α
curr : Nat
hcurr : curr ≤ w
cin origCin : aig.Ref
lhs rhs : aig.RefStream w
lhsExpr rhsExpr : BitVec w
assign : α → Bool
hleft : ∀ (idx : Nat) (hidx : idx < w), ⟦{ aig := aig, ref := lhs.getRef idx hidx }, assign⟧ = lhsExpr.getLsb idx
hright : ∀ (idx : Nat) (hidx : idx < w), ⟦{ aig := aig, ref := rhs.getRef idx hidx }, assign⟧ = rhsExpr.getLsb idx
hcin : ⟦{ aig := aig, ref := cin }, assign⟧ = BitVec.carry curr lhsExpr rhsExpr ⟦{ aig := aig, ref := origCin }, assign⟧
h✝ : curr < w
⊢ ⟦{ aig := (mkFullAdderCarry aig { lhs := lhs.getRef curr h✝, rhs := rhs.getRef curr h✝, cin := cin }).aig,
        ref := (mkFullAdderCarry aig { lhs := lhs.getRef curr h✝, rhs := rhs.getRef curr h✝, cin := cin }).ref },
      assign⟧ =
    BitVec.carry (curr + 1) lhsExpr rhsExpr
      ⟦{ aig := (mkFullAdderCarry aig { lhs := lhs.getRef curr h✝, rhs := rhs.getRef curr h✝, cin := cin }).aig,
          ref := { gate := origCin.gate, hgate := ⋯ } },
        assign⟧

State before:
case isTrue.hcin
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
w : Nat
aig : AIG α
curr : Nat
hcurr : curr ≤ w
cin origCin : aig.Ref
lhs rhs : aig.RefStream w
lhsExpr rhsExpr : BitVec w
assign : α → Bool
hleft : ∀ (idx : Nat) (hidx : idx < w), ⟦{ aig := aig, ref := lhs.getRef idx hidx }, assign⟧ = lhsExpr.getLsb idx
hright : ∀ (idx : Nat) (hidx : idx < w), ⟦{ aig := aig, ref := rhs.getRef idx hidx }, assign⟧ = rhsExpr.getLsb idx
hcin : ⟦{ aig := aig, ref := cin }, assign⟧ = BitVec.carry curr lhsExpr rhsExpr ⟦{ aig := aig, ref := origCin }, assign⟧
h✝ : curr < w
⊢ ⟦{ aig := (mkFullAdderCarry aig { lhs := lhs.getRef curr h✝, rhs := rhs.getRef curr h✝, cin := cin }).aig,
        ref := (mkFullAdderCarry aig { lhs := lhs.getRef curr h✝, rhs := rhs.getRef curr h✝, cin := cin }).ref },
      assign⟧ =
    BitVec.carry (curr + 1) lhsExpr rhsExpr
      ⟦{ aig := (mkFullAdderCarry aig { lhs := lhs.getRef curr h✝, rhs := rhs.getRef curr h✝, cin := cin }).aig,
          ref := { gate := origCin.gate, hgate := ⋯ } },
        assign⟧
Tactic:
. simp [BitVec.carry_succ]
  rw [AIG.LawfulOperator.denote_mem_prefix (f := mkFullAdderCarry)]
  rw [hleft, hright, hcin]
  rw [Bool.atLeastTwo_eq_halfAdder]
State after:
no goals

State before:
case isTrue
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
w : Nat
aig : AIG α
curr : Nat
hcurr : curr ≤ w
cin origCin : aig.Ref
lhs rhs : aig.RefStream w
lhsExpr rhsExpr : BitVec w
assign : α → Bool
hleft : ∀ (idx : Nat) (hidx : idx < w), ⟦{ aig := aig, ref := lhs.getRef idx hidx }, assign⟧ = lhsExpr.getLsb idx
hright : ∀ (idx : Nat) (hidx : idx < w), ⟦{ aig := aig, ref := rhs.getRef idx hidx }, assign⟧ = rhsExpr.getLsb idx
hcin : ⟦{ aig := aig, ref := cin }, assign⟧ = BitVec.carry curr lhsExpr rhsExpr ⟦{ aig := aig, ref := origCin }, assign⟧
h✝ : curr < w
⊢ BitVec.carry w ?isTrue.lhsExpr ?isTrue.rhsExpr
      ⟦{ aig := (mkFullAdderCarry aig { lhs := lhs.getRef curr h✝, rhs := rhs.getRef curr h✝, cin := cin }).aig,
          ref := ?isTrue.origCin },
        assign⟧ =
    BitVec.carry w lhsExpr rhsExpr ⟦{ aig := aig, ref := origCin }, assign⟧
Tactic:
congr 1
State after:
case isTrue.e_c
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
w : Nat
aig : AIG α
curr : Nat
hcurr : curr ≤ w
cin origCin : aig.Ref
lhs rhs : aig.RefStream w
lhsExpr rhsExpr : BitVec w
assign : α → Bool
hleft : ∀ (idx : Nat) (hidx : idx < w), ⟦{ aig := aig, ref := lhs.getRef idx hidx }, assign⟧ = lhsExpr.getLsb idx
hright : ∀ (idx : Nat) (hidx : idx < w), ⟦{ aig := aig, ref := rhs.getRef idx hidx }, assign⟧ = rhsExpr.getLsb idx
hcin : ⟦{ aig := aig, ref := cin }, assign⟧ = BitVec.carry curr lhsExpr rhsExpr ⟦{ aig := aig, ref := origCin }, assign⟧
h✝ : curr < w
⊢ ⟦{ aig := (mkFullAdderCarry aig { lhs := lhs.getRef curr h✝, rhs := rhs.getRef curr h✝, cin := cin }).aig,
        ref := ?isTrue.origCin },
      assign⟧ =
    ⟦{ aig := aig, ref := origCin }, assign⟧

State before:
case isTrue.e_c
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
w : Nat
aig : AIG α
curr : Nat
hcurr : curr ≤ w
cin origCin : aig.Ref
lhs rhs : aig.RefStream w
lhsExpr rhsExpr : BitVec w
assign : α → Bool
hleft : ∀ (idx : Nat) (hidx : idx < w), ⟦{ aig := aig, ref := lhs.getRef idx hidx }, assign⟧ = lhsExpr.getLsb idx
hright : ∀ (idx : Nat) (hidx : idx < w), ⟦{ aig := aig, ref := rhs.getRef idx hidx }, assign⟧ = rhsExpr.getLsb idx
hcin : ⟦{ aig := aig, ref := cin }, assign⟧ = BitVec.carry curr lhsExpr rhsExpr ⟦{ aig := aig, ref := origCin }, assign⟧
h✝ : curr < w
⊢ ⟦{ aig := (mkFullAdderCarry aig { lhs := lhs.getRef curr h✝, rhs := rhs.getRef curr h✝, cin := cin }).aig,
        ref := ?isTrue.origCin },
      assign⟧ =
    ⟦{ aig := aig, ref := origCin }, assign⟧
Tactic:
rw [AIG.LawfulOperator.denote_mem_prefix (f := mkFullAdderCarry)]
State after:
no goals

State before:
case isTrue.hleft
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
w : Nat
aig : AIG α
curr : Nat
hcurr : curr ≤ w
cin origCin : aig.Ref
lhs rhs : aig.RefStream w
lhsExpr rhsExpr : BitVec w
assign : α → Bool
hleft : ∀ (idx : Nat) (hidx : idx < w), ⟦{ aig := aig, ref := lhs.getRef idx hidx }, assign⟧ = lhsExpr.getLsb idx
hright : ∀ (idx : Nat) (hidx : idx < w), ⟦{ aig := aig, ref := rhs.getRef idx hidx }, assign⟧ = rhsExpr.getLsb idx
hcin : ⟦{ aig := aig, ref := cin }, assign⟧ = BitVec.carry curr lhsExpr rhsExpr ⟦{ aig := aig, ref := origCin }, assign⟧
h✝ : curr < w
⊢ ∀ (idx : Nat) (hidx : idx < w),
    ⟦{ aig := (mkFullAdderCarry aig { lhs := lhs.getRef curr h✝, rhs := rhs.getRef curr h✝, cin := cin }).aig,
          ref := (lhs.cast ⋯).getRef idx hidx },
        assign⟧ =
      lhsExpr.getLsb idx
Tactic:
intros
State after:
case isTrue.hleft
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
w : Nat
aig : AIG α
curr : Nat
hcurr : curr ≤ w
cin origCin : aig.Ref
lhs rhs : aig.RefStream w
lhsExpr rhsExpr : BitVec w
assign : α → Bool
hleft : ∀ (idx : Nat) (hidx : idx < w), ⟦{ aig := aig, ref := lhs.getRef idx hidx }, assign⟧ = lhsExpr.getLsb idx
hright : ∀ (idx : Nat) (hidx : idx < w), ⟦{ aig := aig, ref := rhs.getRef idx hidx }, assign⟧ = rhsExpr.getLsb idx
hcin : ⟦{ aig := aig, ref := cin }, assign⟧ = BitVec.carry curr lhsExpr rhsExpr ⟦{ aig := aig, ref := origCin }, assign⟧
h✝ : curr < w
idx✝ : Nat
hidx✝ : idx✝ < w
⊢ ⟦{ aig := (mkFullAdderCarry aig { lhs := lhs.getRef curr h✝, rhs := rhs.getRef curr h✝, cin := cin }).aig,
        ref := (lhs.cast ⋯).getRef idx✝ hidx✝ },
      assign⟧ =
    lhsExpr.getLsb idx✝

State before:
case isTrue.hleft
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
w : Nat
aig : AIG α
curr : Nat
hcurr : curr ≤ w
cin origCin : aig.Ref
lhs rhs : aig.RefStream w
lhsExpr rhsExpr : BitVec w
assign : α → Bool
hleft : ∀ (idx : Nat) (hidx : idx < w), ⟦{ aig := aig, ref := lhs.getRef idx hidx }, assign⟧ = lhsExpr.getLsb idx
hright : ∀ (idx : Nat) (hidx : idx < w), ⟦{ aig := aig, ref := rhs.getRef idx hidx }, assign⟧ = rhsExpr.getLsb idx
hcin : ⟦{ aig := aig, ref := cin }, assign⟧ = BitVec.carry curr lhsExpr rhsExpr ⟦{ aig := aig, ref := origCin }, assign⟧
h✝ : curr < w
idx✝ : Nat
hidx✝ : idx✝ < w
⊢ ⟦{ aig := (mkFullAdderCarry aig { lhs := lhs.getRef curr h✝, rhs := rhs.getRef curr h✝, cin := cin }).aig,
        ref := (lhs.cast ⋯).getRef idx✝ hidx✝ },
      assign⟧ =
    lhsExpr.getLsb idx✝
Tactic:
rw [AIG.LawfulOperator.denote_mem_prefix (f := mkFullAdderCarry)]
State after:
case isTrue.hleft
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
w : Nat
aig : AIG α
curr : Nat
hcurr : curr ≤ w
cin origCin : aig.Ref
lhs rhs : aig.RefStream w
lhsExpr rhsExpr : BitVec w
assign : α → Bool
hleft : ∀ (idx : Nat) (hidx : idx < w), ⟦{ aig := aig, ref := lhs.getRef idx hidx }, assign⟧ = lhsExpr.getLsb idx
hright : ∀ (idx : Nat) (hidx : idx < w), ⟦{ aig := aig, ref := rhs.getRef idx hidx }, assign⟧ = rhsExpr.getLsb idx
hcin : ⟦{ aig := aig, ref := cin }, assign⟧ = BitVec.carry curr lhsExpr rhsExpr ⟦{ aig := aig, ref := origCin }, assign⟧
h✝ : curr < w
idx✝ : Nat
hidx✝ : idx✝ < w
⊢ ⟦{ aig := aig, ref := { gate := ((lhs.cast ⋯).getRef idx✝ hidx✝).gate, hgate := ?isTrue.hleft } }, assign⟧ =
    lhsExpr.getLsb idx✝

case isTrue.hleft
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
w : Nat
aig : AIG α
curr : Nat
hcurr : curr ≤ w
cin origCin : aig.Ref
lhs rhs : aig.RefStream w
lhsExpr rhsExpr : BitVec w
assign : α → Bool
hleft : ∀ (idx : Nat) (hidx : idx < w), ⟦{ aig := aig, ref := lhs.getRef idx hidx }, assign⟧ = lhsExpr.getLsb idx
hright : ∀ (idx : Nat) (hidx : idx < w), ⟦{ aig := aig, ref := rhs.getRef idx hidx }, assign⟧ = rhsExpr.getLsb idx
hcin : ⟦{ aig := aig, ref := cin }, assign⟧ = BitVec.carry curr lhsExpr rhsExpr ⟦{ aig := aig, ref := origCin }, assign⟧
h✝ : curr < w
idx✝ : Nat
hidx✝ : idx✝ < w
⊢ ((lhs.cast ⋯).getRef idx✝ hidx✝).gate < aig.decls.size

State before:
case isTrue.hleft
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
w : Nat
aig : AIG α
curr : Nat
hcurr : curr ≤ w
cin origCin : aig.Ref
lhs rhs : aig.RefStream w
lhsExpr rhsExpr : BitVec w
assign : α → Bool
hleft : ∀ (idx : Nat) (hidx : idx < w), ⟦{ aig := aig, ref := lhs.getRef idx hidx }, assign⟧ = lhsExpr.getLsb idx
hright : ∀ (idx : Nat) (hidx : idx < w), ⟦{ aig := aig, ref := rhs.getRef idx hidx }, assign⟧ = rhsExpr.getLsb idx
hcin : ⟦{ aig := aig, ref := cin }, assign⟧ = BitVec.carry curr lhsExpr rhsExpr ⟦{ aig := aig, ref := origCin }, assign⟧
h✝ : curr < w
idx✝ : Nat
hidx✝ : idx✝ < w
⊢ ⟦{ aig := aig, ref := { gate := ((lhs.cast ⋯).getRef idx✝ hidx✝).gate, hgate := ?isTrue.hleft } }, assign⟧ =
    lhsExpr.getLsb idx✝

case isTrue.hleft
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
w : Nat
aig : AIG α
curr : Nat
hcurr : curr ≤ w
cin origCin : aig.Ref
lhs rhs : aig.RefStream w
lhsExpr rhsExpr : BitVec w
assign : α → Bool
hleft : ∀ (idx : Nat) (hidx : idx < w), ⟦{ aig := aig, ref := lhs.getRef idx hidx }, assign⟧ = lhsExpr.getLsb idx
hright : ∀ (idx : Nat) (hidx : idx < w), ⟦{ aig := aig, ref := rhs.getRef idx hidx }, assign⟧ = rhsExpr.getLsb idx
hcin : ⟦{ aig := aig, ref := cin }, assign⟧ = BitVec.carry curr lhsExpr rhsExpr ⟦{ aig := aig, ref := origCin }, assign⟧
h✝ : curr < w
idx✝ : Nat
hidx✝ : idx✝ < w
⊢ ((lhs.cast ⋯).getRef idx✝ hidx✝).gate < aig.decls.size
Tactic:
. simp [hleft]
State after:
case isTrue.hleft
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
w : Nat
aig : AIG α
curr : Nat
hcurr : curr ≤ w
cin origCin : aig.Ref
lhs rhs : aig.RefStream w
lhsExpr rhsExpr : BitVec w
assign : α → Bool
hleft : ∀ (idx : Nat) (hidx : idx < w), ⟦{ aig := aig, ref := lhs.getRef idx hidx }, assign⟧ = lhsExpr.getLsb idx
hright : ∀ (idx : Nat) (hidx : idx < w), ⟦{ aig := aig, ref := rhs.getRef idx hidx }, assign⟧ = rhsExpr.getLsb idx
hcin : ⟦{ aig := aig, ref := cin }, assign⟧ = BitVec.carry curr lhsExpr rhsExpr ⟦{ aig := aig, ref := origCin }, assign⟧
h✝ : curr < w
idx✝ : Nat
hidx✝ : idx✝ < w
⊢ ((lhs.cast ⋯).getRef idx✝ hidx✝).gate < aig.decls.size

State before:
case isTrue.hleft
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
w : Nat
aig : AIG α
curr : Nat
hcurr : curr ≤ w
cin origCin : aig.Ref
lhs rhs : aig.RefStream w
lhsExpr rhsExpr : BitVec w
assign : α → Bool
hleft : ∀ (idx : Nat) (hidx : idx < w), ⟦{ aig := aig, ref := lhs.getRef idx hidx }, assign⟧ = lhsExpr.getLsb idx
hright : ∀ (idx : Nat) (hidx : idx < w), ⟦{ aig := aig, ref := rhs.getRef idx hidx }, assign⟧ = rhsExpr.getLsb idx
hcin : ⟦{ aig := aig, ref := cin }, assign⟧ = BitVec.carry curr lhsExpr rhsExpr ⟦{ aig := aig, ref := origCin }, assign⟧
h✝ : curr < w
idx✝ : Nat
hidx✝ : idx✝ < w
⊢ ((lhs.cast ⋯).getRef idx✝ hidx✝).gate < aig.decls.size
Tactic:
. simp [Ref.hgate]
State after:
no goals

State before:
case isTrue.hleft
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
w : Nat
aig : AIG α
curr : Nat
hcurr : curr ≤ w
cin origCin : aig.Ref
lhs rhs : aig.RefStream w
lhsExpr rhsExpr : BitVec w
assign : α → Bool
hleft : ∀ (idx : Nat) (hidx : idx < w), ⟦{ aig := aig, ref := lhs.getRef idx hidx }, assign⟧ = lhsExpr.getLsb idx
hright : ∀ (idx : Nat) (hidx : idx < w), ⟦{ aig := aig, ref := rhs.getRef idx hidx }, assign⟧ = rhsExpr.getLsb idx
hcin : ⟦{ aig := aig, ref := cin }, assign⟧ = BitVec.carry curr lhsExpr rhsExpr ⟦{ aig := aig, ref := origCin }, assign⟧
h✝ : curr < w
idx✝ : Nat
hidx✝ : idx✝ < w
⊢ ⟦{ aig := aig, ref := { gate := ((lhs.cast ⋯).getRef idx✝ hidx✝).gate, hgate := ?isTrue.hleft } }, assign⟧ =
    lhsExpr.getLsb idx✝
Tactic:
simp [hleft]
State after:
no goals

State before:
case isTrue.hleft
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
w : Nat
aig : AIG α
curr : Nat
hcurr : curr ≤ w
cin origCin : aig.Ref
lhs rhs : aig.RefStream w
lhsExpr rhsExpr : BitVec w
assign : α → Bool
hleft : ∀ (idx : Nat) (hidx : idx < w), ⟦{ aig := aig, ref := lhs.getRef idx hidx }, assign⟧ = lhsExpr.getLsb idx
hright : ∀ (idx : Nat) (hidx : idx < w), ⟦{ aig := aig, ref := rhs.getRef idx hidx }, assign⟧ = rhsExpr.getLsb idx
hcin : ⟦{ aig := aig, ref := cin }, assign⟧ = BitVec.carry curr lhsExpr rhsExpr ⟦{ aig := aig, ref := origCin }, assign⟧
h✝ : curr < w
idx✝ : Nat
hidx✝ : idx✝ < w
⊢ ((lhs.cast ⋯).getRef idx✝ hidx✝).gate < aig.decls.size
Tactic:
simp [Ref.hgate]
State after:
no goals

State before:
case isTrue.hright
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
w : Nat
aig : AIG α
curr : Nat
hcurr : curr ≤ w
cin origCin : aig.Ref
lhs rhs : aig.RefStream w
lhsExpr rhsExpr : BitVec w
assign : α → Bool
hleft : ∀ (idx : Nat) (hidx : idx < w), ⟦{ aig := aig, ref := lhs.getRef idx hidx }, assign⟧ = lhsExpr.getLsb idx
hright : ∀ (idx : Nat) (hidx : idx < w), ⟦{ aig := aig, ref := rhs.getRef idx hidx }, assign⟧ = rhsExpr.getLsb idx
hcin : ⟦{ aig := aig, ref := cin }, assign⟧ = BitVec.carry curr lhsExpr rhsExpr ⟦{ aig := aig, ref := origCin }, assign⟧
h✝ : curr < w
⊢ ∀ (idx : Nat) (hidx : idx < w),
    ⟦{ aig := (mkFullAdderCarry aig { lhs := lhs.getRef curr h✝, rhs := rhs.getRef curr h✝, cin := cin }).aig,
          ref := (rhs.cast ⋯).getRef idx hidx },
        assign⟧ =
      rhsExpr.getLsb idx
Tactic:
intros
State after:
case isTrue.hright
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
w : Nat
aig : AIG α
curr : Nat
hcurr : curr ≤ w
cin origCin : aig.Ref
lhs rhs : aig.RefStream w
lhsExpr rhsExpr : BitVec w
assign : α → Bool
hleft : ∀ (idx : Nat) (hidx : idx < w), ⟦{ aig := aig, ref := lhs.getRef idx hidx }, assign⟧ = lhsExpr.getLsb idx
hright : ∀ (idx : Nat) (hidx : idx < w), ⟦{ aig := aig, ref := rhs.getRef idx hidx }, assign⟧ = rhsExpr.getLsb idx
hcin : ⟦{ aig := aig, ref := cin }, assign⟧ = BitVec.carry curr lhsExpr rhsExpr ⟦{ aig := aig, ref := origCin }, assign⟧
h✝ : curr < w
idx✝ : Nat
hidx✝ : idx✝ < w
⊢ ⟦{ aig := (mkFullAdderCarry aig { lhs := lhs.getRef curr h✝, rhs := rhs.getRef curr h✝, cin := cin }).aig,
        ref := (rhs.cast ⋯).getRef idx✝ hidx✝ },
      assign⟧ =
    rhsExpr.getLsb idx✝

State before:
case isTrue.hright
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
w : Nat
aig : AIG α
curr : Nat
hcurr : curr ≤ w
cin origCin : aig.Ref
lhs rhs : aig.RefStream w
lhsExpr rhsExpr : BitVec w
assign : α → Bool
hleft : ∀ (idx : Nat) (hidx : idx < w), ⟦{ aig := aig, ref := lhs.getRef idx hidx }, assign⟧ = lhsExpr.getLsb idx
hright : ∀ (idx : Nat) (hidx : idx < w), ⟦{ aig := aig, ref := rhs.getRef idx hidx }, assign⟧ = rhsExpr.getLsb idx
hcin : ⟦{ aig := aig, ref := cin }, assign⟧ = BitVec.carry curr lhsExpr rhsExpr ⟦{ aig := aig, ref := origCin }, assign⟧
h✝ : curr < w
idx✝ : Nat
hidx✝ : idx✝ < w
⊢ ⟦{ aig := (mkFullAdderCarry aig { lhs := lhs.getRef curr h✝, rhs := rhs.getRef curr h✝, cin := cin }).aig,
        ref := (rhs.cast ⋯).getRef idx✝ hidx✝ },
      assign⟧ =
    rhsExpr.getLsb idx✝
Tactic:
rw [AIG.LawfulOperator.denote_mem_prefix (f := mkFullAdderCarry)]
State after:
case isTrue.hright
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
w : Nat
aig : AIG α
curr : Nat
hcurr : curr ≤ w
cin origCin : aig.Ref
lhs rhs : aig.RefStream w
lhsExpr rhsExpr : BitVec w
assign : α → Bool
hleft : ∀ (idx : Nat) (hidx : idx < w), ⟦{ aig := aig, ref := lhs.getRef idx hidx }, assign⟧ = lhsExpr.getLsb idx
hright : ∀ (idx : Nat) (hidx : idx < w), ⟦{ aig := aig, ref := rhs.getRef idx hidx }, assign⟧ = rhsExpr.getLsb idx
hcin : ⟦{ aig := aig, ref := cin }, assign⟧ = BitVec.carry curr lhsExpr rhsExpr ⟦{ aig := aig, ref := origCin }, assign⟧
h✝ : curr < w
idx✝ : Nat
hidx✝ : idx✝ < w
⊢ ⟦{ aig := aig, ref := { gate := ((rhs.cast ⋯).getRef idx✝ hidx✝).gate, hgate := ?isTrue.hright } }, assign⟧ =
    rhsExpr.getLsb idx✝

case isTrue.hright
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
w : Nat
aig : AIG α
curr : Nat
hcurr : curr ≤ w
cin origCin : aig.Ref
lhs rhs : aig.RefStream w
lhsExpr rhsExpr : BitVec w
assign : α → Bool
hleft : ∀ (idx : Nat) (hidx : idx < w), ⟦{ aig := aig, ref := lhs.getRef idx hidx }, assign⟧ = lhsExpr.getLsb idx
hright : ∀ (idx : Nat) (hidx : idx < w), ⟦{ aig := aig, ref := rhs.getRef idx hidx }, assign⟧ = rhsExpr.getLsb idx
hcin : ⟦{ aig := aig, ref := cin }, assign⟧ = BitVec.carry curr lhsExpr rhsExpr ⟦{ aig := aig, ref := origCin }, assign⟧
h✝ : curr < w
idx✝ : Nat
hidx✝ : idx✝ < w
⊢ ((rhs.cast ⋯).getRef idx✝ hidx✝).gate < aig.decls.size

State before:
case isTrue.hright
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
w : Nat
aig : AIG α
curr : Nat
hcurr : curr ≤ w
cin origCin : aig.Ref
lhs rhs : aig.RefStream w
lhsExpr rhsExpr : BitVec w
assign : α → Bool
hleft : ∀ (idx : Nat) (hidx : idx < w), ⟦{ aig := aig, ref := lhs.getRef idx hidx }, assign⟧ = lhsExpr.getLsb idx
hright : ∀ (idx : Nat) (hidx : idx < w), ⟦{ aig := aig, ref := rhs.getRef idx hidx }, assign⟧ = rhsExpr.getLsb idx
hcin : ⟦{ aig := aig, ref := cin }, assign⟧ = BitVec.carry curr lhsExpr rhsExpr ⟦{ aig := aig, ref := origCin }, assign⟧
h✝ : curr < w
idx✝ : Nat
hidx✝ : idx✝ < w
⊢ ⟦{ aig := aig, ref := { gate := ((rhs.cast ⋯).getRef idx✝ hidx✝).gate, hgate := ?isTrue.hright } }, assign⟧ =
    rhsExpr.getLsb idx✝

case isTrue.hright
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
w : Nat
aig : AIG α
curr : Nat
hcurr : curr ≤ w
cin origCin : aig.Ref
lhs rhs : aig.RefStream w
lhsExpr rhsExpr : BitVec w
assign : α → Bool
hleft : ∀ (idx : Nat) (hidx : idx < w), ⟦{ aig := aig, ref := lhs.getRef idx hidx }, assign⟧ = lhsExpr.getLsb idx
hright : ∀ (idx : Nat) (hidx : idx < w), ⟦{ aig := aig, ref := rhs.getRef idx hidx }, assign⟧ = rhsExpr.getLsb idx
hcin : ⟦{ aig := aig, ref := cin }, assign⟧ = BitVec.carry curr lhsExpr rhsExpr ⟦{ aig := aig, ref := origCin }, assign⟧
h✝ : curr < w
idx✝ : Nat
hidx✝ : idx✝ < w
⊢ ((rhs.cast ⋯).getRef idx✝ hidx✝).gate < aig.decls.size
Tactic:
. simp [hright]
State after:
case isTrue.hright
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
w : Nat
aig : AIG α
curr : Nat
hcurr : curr ≤ w
cin origCin : aig.Ref
lhs rhs : aig.RefStream w
lhsExpr rhsExpr : BitVec w
assign : α → Bool
hleft : ∀ (idx : Nat) (hidx : idx < w), ⟦{ aig := aig, ref := lhs.getRef idx hidx }, assign⟧ = lhsExpr.getLsb idx
hright : ∀ (idx : Nat) (hidx : idx < w), ⟦{ aig := aig, ref := rhs.getRef idx hidx }, assign⟧ = rhsExpr.getLsb idx
hcin : ⟦{ aig := aig, ref := cin }, assign⟧ = BitVec.carry curr lhsExpr rhsExpr ⟦{ aig := aig, ref := origCin }, assign⟧
h✝ : curr < w
idx✝ : Nat
hidx✝ : idx✝ < w
⊢ ((rhs.cast ⋯).getRef idx✝ hidx✝).gate < aig.decls.size

State before:
case isTrue.hright
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
w : Nat
aig : AIG α
curr : Nat
hcurr : curr ≤ w
cin origCin : aig.Ref
lhs rhs : aig.RefStream w
lhsExpr rhsExpr : BitVec w
assign : α → Bool
hleft : ∀ (idx : Nat) (hidx : idx < w), ⟦{ aig := aig, ref := lhs.getRef idx hidx }, assign⟧ = lhsExpr.getLsb idx
hright : ∀ (idx : Nat) (hidx : idx < w), ⟦{ aig := aig, ref := rhs.getRef idx hidx }, assign⟧ = rhsExpr.getLsb idx
hcin : ⟦{ aig := aig, ref := cin }, assign⟧ = BitVec.carry curr lhsExpr rhsExpr ⟦{ aig := aig, ref := origCin }, assign⟧
h✝ : curr < w
idx✝ : Nat
hidx✝ : idx✝ < w
⊢ ((rhs.cast ⋯).getRef idx✝ hidx✝).gate < aig.decls.size
Tactic:
. simp [Ref.hgate]
State after:
no goals

State before:
case isTrue.hright
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
w : Nat
aig : AIG α
curr : Nat
hcurr : curr ≤ w
cin origCin : aig.Ref
lhs rhs : aig.RefStream w
lhsExpr rhsExpr : BitVec w
assign : α → Bool
hleft : ∀ (idx : Nat) (hidx : idx < w), ⟦{ aig := aig, ref := lhs.getRef idx hidx }, assign⟧ = lhsExpr.getLsb idx
hright : ∀ (idx : Nat) (hidx : idx < w), ⟦{ aig := aig, ref := rhs.getRef idx hidx }, assign⟧ = rhsExpr.getLsb idx
hcin : ⟦{ aig := aig, ref := cin }, assign⟧ = BitVec.carry curr lhsExpr rhsExpr ⟦{ aig := aig, ref := origCin }, assign⟧
h✝ : curr < w
idx✝ : Nat
hidx✝ : idx✝ < w
⊢ ⟦{ aig := aig, ref := { gate := ((rhs.cast ⋯).getRef idx✝ hidx✝).gate, hgate := ?isTrue.hright } }, assign⟧ =
    rhsExpr.getLsb idx✝
Tactic:
simp [hright]
State after:
no goals

State before:
case isTrue.hright
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
w : Nat
aig : AIG α
curr : Nat
hcurr : curr ≤ w
cin origCin : aig.Ref
lhs rhs : aig.RefStream w
lhsExpr rhsExpr : BitVec w
assign : α → Bool
hleft : ∀ (idx : Nat) (hidx : idx < w), ⟦{ aig := aig, ref := lhs.getRef idx hidx }, assign⟧ = lhsExpr.getLsb idx
hright : ∀ (idx : Nat) (hidx : idx < w), ⟦{ aig := aig, ref := rhs.getRef idx hidx }, assign⟧ = rhsExpr.getLsb idx
hcin : ⟦{ aig := aig, ref := cin }, assign⟧ = BitVec.carry curr lhsExpr rhsExpr ⟦{ aig := aig, ref := origCin }, assign⟧
h✝ : curr < w
idx✝ : Nat
hidx✝ : idx✝ < w
⊢ ((rhs.cast ⋯).getRef idx✝ hidx✝).gate < aig.decls.size
Tactic:
simp [Ref.hgate]
State after:
no goals

State before:
case isTrue.hcin
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
w : Nat
aig : AIG α
curr : Nat
hcurr : curr ≤ w
cin origCin : aig.Ref
lhs rhs : aig.RefStream w
lhsExpr rhsExpr : BitVec w
assign : α → Bool
hleft : ∀ (idx : Nat) (hidx : idx < w), ⟦{ aig := aig, ref := lhs.getRef idx hidx }, assign⟧ = lhsExpr.getLsb idx
hright : ∀ (idx : Nat) (hidx : idx < w), ⟦{ aig := aig, ref := rhs.getRef idx hidx }, assign⟧ = rhsExpr.getLsb idx
hcin : ⟦{ aig := aig, ref := cin }, assign⟧ = BitVec.carry curr lhsExpr rhsExpr ⟦{ aig := aig, ref := origCin }, assign⟧
h✝ : curr < w
⊢ ⟦{ aig := (mkFullAdderCarry aig { lhs := lhs.getRef curr h✝, rhs := rhs.getRef curr h✝, cin := cin }).aig,
        ref := (mkFullAdderCarry aig { lhs := lhs.getRef curr h✝, rhs := rhs.getRef curr h✝, cin := cin }).ref },
      assign⟧ =
    BitVec.carry (curr + 1) lhsExpr rhsExpr
      ⟦{ aig := (mkFullAdderCarry aig { lhs := lhs.getRef curr h✝, rhs := rhs.getRef curr h✝, cin := cin }).aig,
          ref := { gate := origCin.gate, hgate := ⋯ } },
        assign⟧
Tactic:
simp [BitVec.carry_succ]
State after:
case isTrue.hcin
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
w : Nat
aig : AIG α
curr : Nat
hcurr : curr ≤ w
cin origCin : aig.Ref
lhs rhs : aig.RefStream w
lhsExpr rhsExpr : BitVec w
assign : α → Bool
hleft : ∀ (idx : Nat) (hidx : idx < w), ⟦{ aig := aig, ref := lhs.getRef idx hidx }, assign⟧ = lhsExpr.getLsb idx
hright : ∀ (idx : Nat) (hidx : idx < w), ⟦{ aig := aig, ref := rhs.getRef idx hidx }, assign⟧ = rhsExpr.getLsb idx
hcin : ⟦{ aig := aig, ref := cin }, assign⟧ = BitVec.carry curr lhsExpr rhsExpr ⟦{ aig := aig, ref := origCin }, assign⟧
h✝ : curr < w
⊢ (xor ⟦{ aig := aig, ref := lhs.getRef curr h✝ }, assign⟧ ⟦{ aig := aig, ref := rhs.getRef curr h✝ }, assign⟧ &&
        ⟦{ aig := aig, ref := cin }, assign⟧ ||
      ⟦{ aig := aig, ref := lhs.getRef curr h✝ }, assign⟧ && ⟦{ aig := aig, ref := rhs.getRef curr h✝ }, assign⟧) =
    (lhsExpr.getLsb curr).atLeastTwo (rhsExpr.getLsb curr)
      (BitVec.carry curr lhsExpr rhsExpr
        ⟦{ aig := (mkFullAdderCarry aig { lhs := lhs.getRef curr h✝, rhs := rhs.getRef curr h✝, cin := cin }).aig,
            ref := { gate := origCin.gate, hgate := ⋯ } },
          assign⟧)

State before:
case isTrue.hcin
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
w : Nat
aig : AIG α
curr : Nat
hcurr : curr ≤ w
cin origCin : aig.Ref
lhs rhs : aig.RefStream w
lhsExpr rhsExpr : BitVec w
assign : α → Bool
hleft : ∀ (idx : Nat) (hidx : idx < w), ⟦{ aig := aig, ref := lhs.getRef idx hidx }, assign⟧ = lhsExpr.getLsb idx
hright : ∀ (idx : Nat) (hidx : idx < w), ⟦{ aig := aig, ref := rhs.getRef idx hidx }, assign⟧ = rhsExpr.getLsb idx
hcin : ⟦{ aig := aig, ref := cin }, assign⟧ = BitVec.carry curr lhsExpr rhsExpr ⟦{ aig := aig, ref := origCin }, assign⟧
h✝ : curr < w
⊢ (xor ⟦{ aig := aig, ref := lhs.getRef curr h✝ }, assign⟧ ⟦{ aig := aig, ref := rhs.getRef curr h✝ }, assign⟧ &&
        ⟦{ aig := aig, ref := cin }, assign⟧ ||
      ⟦{ aig := aig, ref := lhs.getRef curr h✝ }, assign⟧ && ⟦{ aig := aig, ref := rhs.getRef curr h✝ }, assign⟧) =
    (lhsExpr.getLsb curr).atLeastTwo (rhsExpr.getLsb curr)
      (BitVec.carry curr lhsExpr rhsExpr
        ⟦{ aig := (mkFullAdderCarry aig { lhs := lhs.getRef curr h✝, rhs := rhs.getRef curr h✝, cin := cin }).aig,
            ref := { gate := origCin.gate, hgate := ⋯ } },
          assign⟧)
Tactic:
rw [AIG.LawfulOperator.denote_mem_prefix (f := mkFullAdderCarry)]
State after:
case isTrue.hcin
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
w : Nat
aig : AIG α
curr : Nat
hcurr : curr ≤ w
cin origCin : aig.Ref
lhs rhs : aig.RefStream w
lhsExpr rhsExpr : BitVec w
assign : α → Bool
hleft : ∀ (idx : Nat) (hidx : idx < w), ⟦{ aig := aig, ref := lhs.getRef idx hidx }, assign⟧ = lhsExpr.getLsb idx
hright : ∀ (idx : Nat) (hidx : idx < w), ⟦{ aig := aig, ref := rhs.getRef idx hidx }, assign⟧ = rhsExpr.getLsb idx
hcin : ⟦{ aig := aig, ref := cin }, assign⟧ = BitVec.carry curr lhsExpr rhsExpr ⟦{ aig := aig, ref := origCin }, assign⟧
h✝ : curr < w
⊢ (xor ⟦{ aig := aig, ref := lhs.getRef curr h✝ }, assign⟧ ⟦{ aig := aig, ref := rhs.getRef curr h✝ }, assign⟧ &&
        ⟦{ aig := aig, ref := cin }, assign⟧ ||
      ⟦{ aig := aig, ref := lhs.getRef curr h✝ }, assign⟧ && ⟦{ aig := aig, ref := rhs.getRef curr h✝ }, assign⟧) =
    (lhsExpr.getLsb curr).atLeastTwo (rhsExpr.getLsb curr)
      (BitVec.carry curr lhsExpr rhsExpr
        ⟦{ aig := aig, ref := { gate := origCin.gate, hgate := ?isTrue.hcin } }, assign⟧)

case isTrue.hcin
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
w : Nat
aig : AIG α
curr : Nat
hcurr : curr ≤ w
cin origCin : aig.Ref
lhs rhs : aig.RefStream w
lhsExpr rhsExpr : BitVec w
assign : α → Bool
hleft : ∀ (idx : Nat) (hidx : idx < w), ⟦{ aig := aig, ref := lhs.getRef idx hidx }, assign⟧ = lhsExpr.getLsb idx
hright : ∀ (idx : Nat) (hidx : idx < w), ⟦{ aig := aig, ref := rhs.getRef idx hidx }, assign⟧ = rhsExpr.getLsb idx
hcin : ⟦{ aig := aig, ref := cin }, assign⟧ = BitVec.carry curr lhsExpr rhsExpr ⟦{ aig := aig, ref := origCin }, assign⟧
h✝ : curr < w
⊢ origCin.gate < aig.decls.size

State before:
case isTrue.hcin
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
w : Nat
aig : AIG α
curr : Nat
hcurr : curr ≤ w
cin origCin : aig.Ref
lhs rhs : aig.RefStream w
lhsExpr rhsExpr : BitVec w
assign : α → Bool
hleft : ∀ (idx : Nat) (hidx : idx < w), ⟦{ aig := aig, ref := lhs.getRef idx hidx }, assign⟧ = lhsExpr.getLsb idx
hright : ∀ (idx : Nat) (hidx : idx < w), ⟦{ aig := aig, ref := rhs.getRef idx hidx }, assign⟧ = rhsExpr.getLsb idx
hcin : ⟦{ aig := aig, ref := cin }, assign⟧ = BitVec.carry curr lhsExpr rhsExpr ⟦{ aig := aig, ref := origCin }, assign⟧
h✝ : curr < w
⊢ (xor ⟦{ aig := aig, ref := lhs.getRef curr h✝ }, assign⟧ ⟦{ aig := aig, ref := rhs.getRef curr h✝ }, assign⟧ &&
        ⟦{ aig := aig, ref := cin }, assign⟧ ||
      ⟦{ aig := aig, ref := lhs.getRef curr h✝ }, assign⟧ && ⟦{ aig := aig, ref := rhs.getRef curr h✝ }, assign⟧) =
    (lhsExpr.getLsb curr).atLeastTwo (rhsExpr.getLsb curr)
      (BitVec.carry curr lhsExpr rhsExpr
        ⟦{ aig := aig, ref := { gate := origCin.gate, hgate := ?isTrue.hcin } }, assign⟧)

case isTrue.hcin
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
w : Nat
aig : AIG α
curr : Nat
hcurr : curr ≤ w
cin origCin : aig.Ref
lhs rhs : aig.RefStream w
lhsExpr rhsExpr : BitVec w
assign : α → Bool
hleft : ∀ (idx : Nat) (hidx : idx < w), ⟦{ aig := aig, ref := lhs.getRef idx hidx }, assign⟧ = lhsExpr.getLsb idx
hright : ∀ (idx : Nat) (hidx : idx < w), ⟦{ aig := aig, ref := rhs.getRef idx hidx }, assign⟧ = rhsExpr.getLsb idx
hcin : ⟦{ aig := aig, ref := cin }, assign⟧ = BitVec.carry curr lhsExpr rhsExpr ⟦{ aig := aig, ref := origCin }, assign⟧
h✝ : curr < w
⊢ origCin.gate < aig.decls.size
Tactic:
rw [hleft, hright, hcin]
State after:
case isTrue.hcin
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
w : Nat
aig : AIG α
curr : Nat
hcurr : curr ≤ w
cin origCin : aig.Ref
lhs rhs : aig.RefStream w
lhsExpr rhsExpr : BitVec w
assign : α → Bool
hleft : ∀ (idx : Nat) (hidx : idx < w), ⟦{ aig := aig, ref := lhs.getRef idx hidx }, assign⟧ = lhsExpr.getLsb idx
hright : ∀ (idx : Nat) (hidx : idx < w), ⟦{ aig := aig, ref := rhs.getRef idx hidx }, assign⟧ = rhsExpr.getLsb idx
hcin : ⟦{ aig := aig, ref := cin }, assign⟧ = BitVec.carry curr lhsExpr rhsExpr ⟦{ aig := aig, ref := origCin }, assign⟧
h✝ : curr < w
⊢ (xor (lhsExpr.getLsb curr) (rhsExpr.getLsb curr) &&
        BitVec.carry curr lhsExpr rhsExpr ⟦{ aig := aig, ref := origCin }, assign⟧ ||
      lhsExpr.getLsb curr && rhsExpr.getLsb curr) =
    (lhsExpr.getLsb curr).atLeastTwo (rhsExpr.getLsb curr)
      (BitVec.carry curr lhsExpr rhsExpr
        ⟦{ aig := aig, ref := { gate := origCin.gate, hgate := ?isTrue.hcin } }, assign⟧)

case isTrue.hcin
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
w : Nat
aig : AIG α
curr : Nat
hcurr : curr ≤ w
cin origCin : aig.Ref
lhs rhs : aig.RefStream w
lhsExpr rhsExpr : BitVec w
assign : α → Bool
hleft : ∀ (idx : Nat) (hidx : idx < w), ⟦{ aig := aig, ref := lhs.getRef idx hidx }, assign⟧ = lhsExpr.getLsb idx
hright : ∀ (idx : Nat) (hidx : idx < w), ⟦{ aig := aig, ref := rhs.getRef idx hidx }, assign⟧ = rhsExpr.getLsb idx
hcin : ⟦{ aig := aig, ref := cin }, assign⟧ = BitVec.carry curr lhsExpr rhsExpr ⟦{ aig := aig, ref := origCin }, assign⟧
h✝ : curr < w
⊢ origCin.gate < aig.decls.size

case isTrue.hcin
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
w : Nat
aig : AIG α
curr : Nat
hcurr : curr ≤ w
cin origCin : aig.Ref
lhs rhs : aig.RefStream w
lhsExpr rhsExpr : BitVec w
assign : α → Bool
hleft : ∀ (idx : Nat) (hidx : idx < w), ⟦{ aig := aig, ref := lhs.getRef idx hidx }, assign⟧ = lhsExpr.getLsb idx
hright : ∀ (idx : Nat) (hidx : idx < w), ⟦{ aig := aig, ref := rhs.getRef idx hidx }, assign⟧ = rhsExpr.getLsb idx
hcin : ⟦{ aig := aig, ref := cin }, assign⟧ = BitVec.carry curr lhsExpr rhsExpr ⟦{ aig := aig, ref := origCin }, assign⟧
h✝ : curr < w
⊢ origCin.gate < aig.decls.size

case isTrue.hcin
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
w : Nat
aig : AIG α
curr : Nat
hcurr : curr ≤ w
cin origCin : aig.Ref
lhs rhs : aig.RefStream w
lhsExpr rhsExpr : BitVec w
assign : α → Bool
hleft : ∀ (idx : Nat) (hidx : idx < w), ⟦{ aig := aig, ref := lhs.getRef idx hidx }, assign⟧ = lhsExpr.getLsb idx
hright : ∀ (idx : Nat) (hidx : idx < w), ⟦{ aig := aig, ref := rhs.getRef idx hidx }, assign⟧ = rhsExpr.getLsb idx
hcin : ⟦{ aig := aig, ref := cin }, assign⟧ = BitVec.carry curr lhsExpr rhsExpr ⟦{ aig := aig, ref := origCin }, assign⟧
h✝ : curr < w
⊢ origCin.gate < aig.decls.size

case isTrue.hcin
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
w : Nat
aig : AIG α
curr : Nat
hcurr : curr ≤ w
cin origCin : aig.Ref
lhs rhs : aig.RefStream w
lhsExpr rhsExpr : BitVec w
assign : α → Bool
hleft : ∀ (idx : Nat) (hidx : idx < w), ⟦{ aig := aig, ref := lhs.getRef idx hidx }, assign⟧ = lhsExpr.getLsb idx
hright : ∀ (idx : Nat) (hidx : idx < w), ⟦{ aig := aig, ref := rhs.getRef idx hidx }, assign⟧ = rhsExpr.getLsb idx
hcin : ⟦{ aig := aig, ref := cin }, assign⟧ = BitVec.carry curr lhsExpr rhsExpr ⟦{ aig := aig, ref := origCin }, assign⟧
h✝ : curr < w
⊢ origCin.gate < aig.decls.size

State before:
case isTrue.hcin
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
w : Nat
aig : AIG α
curr : Nat
hcurr : curr ≤ w
cin origCin : aig.Ref
lhs rhs : aig.RefStream w
lhsExpr rhsExpr : BitVec w
assign : α → Bool
hleft : ∀ (idx : Nat) (hidx : idx < w), ⟦{ aig := aig, ref := lhs.getRef idx hidx }, assign⟧ = lhsExpr.getLsb idx
hright : ∀ (idx : Nat) (hidx : idx < w), ⟦{ aig := aig, ref := rhs.getRef idx hidx }, assign⟧ = rhsExpr.getLsb idx
hcin : ⟦{ aig := aig, ref := cin }, assign⟧ = BitVec.carry curr lhsExpr rhsExpr ⟦{ aig := aig, ref := origCin }, assign⟧
h✝ : curr < w
⊢ (xor (lhsExpr.getLsb curr) (rhsExpr.getLsb curr) &&
        BitVec.carry curr lhsExpr rhsExpr ⟦{ aig := aig, ref := origCin }, assign⟧ ||
      lhsExpr.getLsb curr && rhsExpr.getLsb curr) =
    (lhsExpr.getLsb curr).atLeastTwo (rhsExpr.getLsb curr)
      (BitVec.carry curr lhsExpr rhsExpr
        ⟦{ aig := aig, ref := { gate := origCin.gate, hgate := ?isTrue.hcin } }, assign⟧)

case isTrue.hcin
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
w : Nat
aig : AIG α
curr : Nat
hcurr : curr ≤ w
cin origCin : aig.Ref
lhs rhs : aig.RefStream w
lhsExpr rhsExpr : BitVec w
assign : α → Bool
hleft : ∀ (idx : Nat) (hidx : idx < w), ⟦{ aig := aig, ref := lhs.getRef idx hidx }, assign⟧ = lhsExpr.getLsb idx
hright : ∀ (idx : Nat) (hidx : idx < w), ⟦{ aig := aig, ref := rhs.getRef idx hidx }, assign⟧ = rhsExpr.getLsb idx
hcin : ⟦{ aig := aig, ref := cin }, assign⟧ = BitVec.carry curr lhsExpr rhsExpr ⟦{ aig := aig, ref := origCin }, assign⟧
h✝ : curr < w
⊢ origCin.gate < aig.decls.size

case isTrue.hcin
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
w : Nat
aig : AIG α
curr : Nat
hcurr : curr ≤ w
cin origCin : aig.Ref
lhs rhs : aig.RefStream w
lhsExpr rhsExpr : BitVec w
assign : α → Bool
hleft : ∀ (idx : Nat) (hidx : idx < w), ⟦{ aig := aig, ref := lhs.getRef idx hidx }, assign⟧ = lhsExpr.getLsb idx
hright : ∀ (idx : Nat) (hidx : idx < w), ⟦{ aig := aig, ref := rhs.getRef idx hidx }, assign⟧ = rhsExpr.getLsb idx
hcin : ⟦{ aig := aig, ref := cin }, assign⟧ = BitVec.carry curr lhsExpr rhsExpr ⟦{ aig := aig, ref := origCin }, assign⟧
h✝ : curr < w
⊢ origCin.gate < aig.decls.size

case isTrue.hcin
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
w : Nat
aig : AIG α
curr : Nat
hcurr : curr ≤ w
cin origCin : aig.Ref
lhs rhs : aig.RefStream w
lhsExpr rhsExpr : BitVec w
assign : α → Bool
hleft : ∀ (idx : Nat) (hidx : idx < w), ⟦{ aig := aig, ref := lhs.getRef idx hidx }, assign⟧ = lhsExpr.getLsb idx
hright : ∀ (idx : Nat) (hidx : idx < w), ⟦{ aig := aig, ref := rhs.getRef idx hidx }, assign⟧ = rhsExpr.getLsb idx
hcin : ⟦{ aig := aig, ref := cin }, assign⟧ = BitVec.carry curr lhsExpr rhsExpr ⟦{ aig := aig, ref := origCin }, assign⟧
h✝ : curr < w
⊢ origCin.gate < aig.decls.size

case isTrue.hcin
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
w : Nat
aig : AIG α
curr : Nat
hcurr : curr ≤ w
cin origCin : aig.Ref
lhs rhs : aig.RefStream w
lhsExpr rhsExpr : BitVec w
assign : α → Bool
hleft : ∀ (idx : Nat) (hidx : idx < w), ⟦{ aig := aig, ref := lhs.getRef idx hidx }, assign⟧ = lhsExpr.getLsb idx
hright : ∀ (idx : Nat) (hidx : idx < w), ⟦{ aig := aig, ref := rhs.getRef idx hidx }, assign⟧ = rhsExpr.getLsb idx
hcin : ⟦{ aig := aig, ref := cin }, assign⟧ = BitVec.carry curr lhsExpr rhsExpr ⟦{ aig := aig, ref := origCin }, assign⟧
h✝ : curr < w
⊢ origCin.gate < aig.decls.size
Tactic:
rw [Bool.atLeastTwo_eq_halfAdder]
State after:
no goals

State before:
case isFalse
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
w : Nat
aig : AIG α
curr : Nat
hcurr : curr ≤ w
cin origCin : aig.Ref
lhs rhs : aig.RefStream w
lhsExpr rhsExpr : BitVec w
assign : α → Bool
hleft : ∀ (idx : Nat) (hidx : idx < w), ⟦{ aig := aig, ref := lhs.getRef idx hidx }, assign⟧ = lhsExpr.getLsb idx
hright : ∀ (idx : Nat) (hidx : idx < w), ⟦{ aig := aig, ref := rhs.getRef idx hidx }, assign⟧ = rhsExpr.getLsb idx
hcin : ⟦{ aig := aig, ref := cin }, assign⟧ = BitVec.carry curr lhsExpr rhsExpr ⟦{ aig := aig, ref := origCin }, assign⟧
h✝ : ¬curr < w
⊢ ⟦{ aig := aig, ref := cin }, assign⟧ = BitVec.carry w lhsExpr rhsExpr ⟦{ aig := aig, ref := origCin }, assign⟧
Tactic:
have : w = curr := by omega
State after:
case isFalse
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
w : Nat
aig : AIG α
curr : Nat
hcurr : curr ≤ w
cin origCin : aig.Ref
lhs rhs : aig.RefStream w
lhsExpr rhsExpr : BitVec w
assign : α → Bool
hleft : ∀ (idx : Nat) (hidx : idx < w), ⟦{ aig := aig, ref := lhs.getRef idx hidx }, assign⟧ = lhsExpr.getLsb idx
hright : ∀ (idx : Nat) (hidx : idx < w), ⟦{ aig := aig, ref := rhs.getRef idx hidx }, assign⟧ = rhsExpr.getLsb idx
hcin : ⟦{ aig := aig, ref := cin }, assign⟧ = BitVec.carry curr lhsExpr rhsExpr ⟦{ aig := aig, ref := origCin }, assign⟧
h✝ : ¬curr < w
this : w = curr
⊢ ⟦{ aig := aig, ref := cin }, assign⟧ = BitVec.carry w lhsExpr rhsExpr ⟦{ aig := aig, ref := origCin }, assign⟧

State before:
case isFalse
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
w : Nat
aig : AIG α
curr : Nat
hcurr : curr ≤ w
cin origCin : aig.Ref
lhs rhs : aig.RefStream w
lhsExpr rhsExpr : BitVec w
assign : α → Bool
hleft : ∀ (idx : Nat) (hidx : idx < w), ⟦{ aig := aig, ref := lhs.getRef idx hidx }, assign⟧ = lhsExpr.getLsb idx
hright : ∀ (idx : Nat) (hidx : idx < w), ⟦{ aig := aig, ref := rhs.getRef idx hidx }, assign⟧ = rhsExpr.getLsb idx
hcin : ⟦{ aig := aig, ref := cin }, assign⟧ = BitVec.carry curr lhsExpr rhsExpr ⟦{ aig := aig, ref := origCin }, assign⟧
h✝ : ¬curr < w
this : w = curr
⊢ ⟦{ aig := aig, ref := cin }, assign⟧ = BitVec.carry w lhsExpr rhsExpr ⟦{ aig := aig, ref := origCin }, assign⟧
Tactic:
rw [hcin]
State after:
case isFalse
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
w : Nat
aig : AIG α
curr : Nat
hcurr : curr ≤ w
cin origCin : aig.Ref
lhs rhs : aig.RefStream w
lhsExpr rhsExpr : BitVec w
assign : α → Bool
hleft : ∀ (idx : Nat) (hidx : idx < w), ⟦{ aig := aig, ref := lhs.getRef idx hidx }, assign⟧ = lhsExpr.getLsb idx
hright : ∀ (idx : Nat) (hidx : idx < w), ⟦{ aig := aig, ref := rhs.getRef idx hidx }, assign⟧ = rhsExpr.getLsb idx
hcin : ⟦{ aig := aig, ref := cin }, assign⟧ = BitVec.carry curr lhsExpr rhsExpr ⟦{ aig := aig, ref := origCin }, assign⟧
h✝ : ¬curr < w
this : w = curr
⊢ BitVec.carry curr lhsExpr rhsExpr ⟦{ aig := aig, ref := origCin }, assign⟧ =
    BitVec.carry w lhsExpr rhsExpr ⟦{ aig := aig, ref := origCin }, assign⟧

State before:
case isFalse
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
w : Nat
aig : AIG α
curr : Nat
hcurr : curr ≤ w
cin origCin : aig.Ref
lhs rhs : aig.RefStream w
lhsExpr rhsExpr : BitVec w
assign : α → Bool
hleft : ∀ (idx : Nat) (hidx : idx < w), ⟦{ aig := aig, ref := lhs.getRef idx hidx }, assign⟧ = lhsExpr.getLsb idx
hright : ∀ (idx : Nat) (hidx : idx < w), ⟦{ aig := aig, ref := rhs.getRef idx hidx }, assign⟧ = rhsExpr.getLsb idx
hcin : ⟦{ aig := aig, ref := cin }, assign⟧ = BitVec.carry curr lhsExpr rhsExpr ⟦{ aig := aig, ref := origCin }, assign⟧
h✝ : ¬curr < w
this : w = curr
⊢ BitVec.carry curr lhsExpr rhsExpr ⟦{ aig := aig, ref := origCin }, assign⟧ =
    BitVec.carry w lhsExpr rhsExpr ⟦{ aig := aig, ref := origCin }, assign⟧
Tactic:
simp [this]
State after:
no goals

State before:
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
w : Nat
aig : AIG α
curr : Nat
hcurr : curr ≤ w
cin origCin : aig.Ref
lhs rhs : aig.RefStream w
lhsExpr rhsExpr : BitVec w
assign : α → Bool
hleft : ∀ (idx : Nat) (hidx : idx < w), ⟦{ aig := aig, ref := lhs.getRef idx hidx }, assign⟧ = lhsExpr.getLsb idx
hright : ∀ (idx : Nat) (hidx : idx < w), ⟦{ aig := aig, ref := rhs.getRef idx hidx }, assign⟧ = rhsExpr.getLsb idx
hcin : ⟦{ aig := aig, ref := cin }, assign⟧ = BitVec.carry curr lhsExpr rhsExpr ⟦{ aig := aig, ref := origCin }, assign⟧
h✝ : ¬curr < w
⊢ w = curr
Tactic:
omega
State after:
no goals