Theorem: BVExpr.bitblast.blastAdd.mkFullAdder_denote_mem_prefix (LeanSAT/Reflect/BVExpr/BitBlast/Lemmas/Add.lean)

State before:
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
assign : α → Bool
aig : AIG α
input : FullAdderInput aig
start : Nat
hstart : start < aig.decls.size
⊢ start < (mkFullAdder aig input).aig.decls.size
Tactic:
apply Nat.lt_of_lt_of_le
State after:
case a
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
assign : α → Bool
aig : AIG α
input : FullAdderInput aig
start : Nat
hstart : start < aig.decls.size
⊢ start < ?m

case a
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
assign : α → Bool
aig : AIG α
input : FullAdderInput aig
start : Nat
hstart : start < aig.decls.size
⊢ ?m ≤ (mkFullAdder aig input).aig.decls.size

case m
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
assign : α → Bool
aig : AIG α
input : FullAdderInput aig
start : Nat
hstart : start < aig.decls.size
⊢ Nat

State before:
case a
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
assign : α → Bool
aig : AIG α
input : FullAdderInput aig
start : Nat
hstart : start < aig.decls.size
⊢ start < ?m

case a
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
assign : α → Bool
aig : AIG α
input : FullAdderInput aig
start : Nat
hstart : start < aig.decls.size
⊢ ?m ≤ (mkFullAdder aig input).aig.decls.size

case m
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
assign : α → Bool
aig : AIG α
input : FullAdderInput aig
start : Nat
hstart : start < aig.decls.size
⊢ Nat
Tactic:
exact hstart
State after:
case a
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
assign : α → Bool
aig : AIG α
input : FullAdderInput aig
start : Nat
hstart : start < aig.decls.size
⊢ aig.decls.size ≤ (mkFullAdder aig input).aig.decls.size

State before:
case a
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
assign : α → Bool
aig : AIG α
input : FullAdderInput aig
start : Nat
hstart : start < aig.decls.size
⊢ aig.decls.size ≤ (mkFullAdder aig input).aig.decls.size
Tactic:
apply FullAdderOutput.hle
State after:
no goals

State before:
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
assign : α → Bool
aig : AIG α
input : FullAdderInput aig
start : Nat
hstart : start < aig.decls.size
⊢ ⟦{ aig := (mkFullAdder aig input).aig, ref := { gate := start, hgate := ⋯ } }, assign⟧ =
    ⟦{ aig := aig, ref := { gate := start, hgate := hstart } }, assign⟧
Tactic:
unfold mkFullAdder
State after:
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
assign : α → Bool
aig : AIG α
input : FullAdderInput aig
start : Nat
hstart : start < aig.decls.size
⊢ ⟦{
        aig :=
          (let res := mkFullAdderOut aig input;
            let aig_1 := res.aig;
            let outRef := res.ref;
            let_fun haig1 := ⋯;
            let input_1 := input.cast haig1;
            let res_1 := mkFullAdderCarry aig_1 input_1;
            let aig_2 := res_1.aig;
            let carryRef := res_1.ref;
            let_fun haig2 := ⋯;
            let outRef := outRef.cast haig2;
            let_fun hle := ⋯;
            { aig := aig_2, out := outRef, cout := carryRef, hle := hle }).aig,
        ref := { gate := start, hgate := ⋯ } },
      assign⟧ =
    ⟦{ aig := aig, ref := { gate := start, hgate := hstart } }, assign⟧

State before:
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
assign : α → Bool
aig : AIG α
input : FullAdderInput aig
start : Nat
hstart : start < aig.decls.size
⊢ ⟦{
        aig :=
          (let res := mkFullAdderOut aig input;
            let aig_1 := res.aig;
            let outRef := res.ref;
            let_fun haig1 := ⋯;
            let input_1 := input.cast haig1;
            let res_1 := mkFullAdderCarry aig_1 input_1;
            let aig_2 := res_1.aig;
            let carryRef := res_1.ref;
            let_fun haig2 := ⋯;
            let outRef := outRef.cast haig2;
            let_fun hle := ⋯;
            { aig := aig_2, out := outRef, cout := carryRef, hle := hle }).aig,
        ref := { gate := start, hgate := ⋯ } },
      assign⟧ =
    ⟦{ aig := aig, ref := { gate := start, hgate := hstart } }, assign⟧
Tactic:
dsimp
State after:
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
assign : α → Bool
aig : AIG α
input : FullAdderInput aig
start : Nat
hstart : start < aig.decls.size
⊢ ⟦{ aig := (mkFullAdderCarry (mkFullAdderOut aig input).aig (input.cast ⋯)).aig,
        ref := { gate := start, hgate := ⋯ } },
      assign⟧ =
    ⟦{ aig := aig, ref := { gate := start, hgate := hstart } }, assign⟧

State before:
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
assign : α → Bool
aig : AIG α
input : FullAdderInput aig
start : Nat
hstart : start < aig.decls.size
⊢ ⟦{ aig := (mkFullAdderCarry (mkFullAdderOut aig input).aig (input.cast ⋯)).aig,
        ref := { gate := start, hgate := ⋯ } },
      assign⟧ =
    ⟦{ aig := aig, ref := { gate := start, hgate := hstart } }, assign⟧
Tactic:
rw [AIG.LawfulOperator.denote_mem_prefix (f := mkFullAdderCarry)]
State after:
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
assign : α → Bool
aig : AIG α
input : FullAdderInput aig
start : Nat
hstart : start < aig.decls.size
⊢ ⟦{ aig := (mkFullAdderOut aig input).aig, ref := { gate := start, hgate := ?m.7385 } }, assign⟧ =
    ⟦{ aig := aig, ref := { gate := start, hgate := hstart } }, assign⟧

α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
assign : α → Bool
aig : AIG α
input : FullAdderInput aig
start : Nat
hstart : start < aig.decls.size
⊢ start < (mkFullAdderOut aig input).aig.decls.size

State before:
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
assign : α → Bool
aig : AIG α
input : FullAdderInput aig
start : Nat
hstart : start < aig.decls.size
⊢ ⟦{ aig := (mkFullAdderOut aig input).aig, ref := { gate := start, hgate := ?m.7385 } }, assign⟧ =
    ⟦{ aig := aig, ref := { gate := start, hgate := hstart } }, assign⟧

α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
assign : α → Bool
aig : AIG α
input : FullAdderInput aig
start : Nat
hstart : start < aig.decls.size
⊢ start < (mkFullAdderOut aig input).aig.decls.size
Tactic:
rw [AIG.LawfulOperator.denote_mem_prefix (f := mkFullAdderOut)]
State after:
no goals