-- Mathlib/.lake/packages/lean4/src/lean/Std/Tactic/BVDecide/Bitblast/BVExpr/Circuit/Lemmas/Operations/Add.lean
theorem denote_mkFullAdderCarry (assign : α → Bool) (aig : AIG α) (input : FullAdderInput aig) :
    ⟦mkFullAdderCarry aig input, assign⟧
      =
      ((⟦aig, input.lhs, assign⟧ ^^ ⟦aig, input.rhs, assign⟧) && ⟦aig, input.cin, assign⟧ ||
       ⟦aig, input.lhs, assign⟧ && ⟦aig, input.rhs, assign⟧)

Proof state:
α : Type
inst✝¹ : Hashable α
inst✝ : DecidableEq α
assign : α → Bool
aig : AIG α
input : FullAdderInput aig
⊢ input.rhs.gate < (aig.mkXorCached { lhs := input.lhs, rhs := input.rhs }).aig.decls.size

Tactic:
apply LawfulOperator.lt_size_of_lt_aig_size (f := mkXorCached)

Result:
case h
α : Type
inst✝¹ : Hashable α
inst✝ : DecidableEq α
assign : α → Bool
aig : AIG α
input : FullAdderInput aig
⊢ input.rhs.gate < aig.decls.size

Proof state:
α : Type
inst✝¹ : Hashable α
inst✝ : DecidableEq α
assign : α → Bool
aig : AIG α
input : FullAdderInput aig
⊢ ⟦assign, mkFullAdderCarry aig input⟧ =
    ((⟦assign, { aig := aig, ref := input.lhs }⟧ ^^ ⟦assign, { aig := aig, ref := input.rhs }⟧) &&
        ⟦assign, { aig := aig, ref := input.cin }⟧ ||
      ⟦assign, { aig := aig, ref := input.lhs }⟧ && ⟦assign, { aig := aig, ref := input.rhs }⟧)

Tactic:
simp only [mkFullAdderCarry, Ref.cast_eq, Int.reduceNeg, denote_mkOrCached,
  LawfulOperator.denote_input_entry, denote_mkAndCached, denote_projected_entry',
  denote_mkXorCached, denote_projected_entry]

Result:
α : Type
inst✝¹ : Hashable α
inst✝ : DecidableEq α
assign : α → Bool
aig : AIG α
input : FullAdderInput aig
⊢ ((⟦assign, { aig := aig, ref := input.lhs }⟧ ^^ ⟦assign, { aig := aig, ref := input.rhs }⟧) &&
        ⟦assign,
          { aig := (aig.mkXorCached { lhs := input.lhs, rhs := input.rhs }).aig,
            ref := { gate := input.cin.gate, hgate := ⋯ } }⟧ ||
      ⟦assign,
          {
            aig :=
              ((aig.mkXorCached { lhs := input.lhs, rhs := input.rhs }).aig.mkAndCached
                  { lhs := (aig.mkXorCached { lhs := input.lhs, rhs := input.rhs }).ref,
                    rhs := { gate := input.cin.gate, hgate := ⋯ } }).aig,
            ref := { gate := input.lhs.gate, hgate := ⋯ } }⟧ &&
        ⟦assign,
          {
            aig :=
              ((aig.mkXorCached { lhs := input.lhs, rhs := input.rhs }).aig.mkAndCached
                  { lhs := (aig.mkXorCached { lhs := input.lhs, rhs := input.rhs }).ref,
                    rhs := { gate := input.cin.gate, hgate := ⋯ } }).aig,
            ref := { gate := input.rhs.gate, hgate := ⋯ } }⟧) =
    ((⟦assign, { aig := aig, ref := input.lhs }⟧ ^^ ⟦assign, { aig := aig, ref := input.rhs }⟧) &&
        ⟦assign, { aig := aig, ref := input.cin }⟧ ||
      ⟦assign, { aig := aig, ref := input.lhs }⟧ && ⟦assign, { aig := aig, ref := input.rhs }⟧)

Proof state:
α : Type
inst✝¹ : Hashable α
inst✝ : DecidableEq α
assign : α → Bool
aig : AIG α
input : FullAdderInput aig
⊢ input.lhs.gate < (aig.mkXorCached { lhs := input.lhs, rhs := input.rhs }).aig.decls.size

Tactic:
apply LawfulOperator.lt_size_of_lt_aig_size (f := mkXorCached)

Result:
case h
α : Type
inst✝¹ : Hashable α
inst✝ : DecidableEq α
assign : α → Bool
aig : AIG α
input : FullAdderInput aig
⊢ input.lhs.gate < aig.decls.size

Proof state:
case e_x.e_y
α : Type
inst✝¹ : Hashable α
inst✝ : DecidableEq α
assign : α → Bool
aig : AIG α
input : FullAdderInput aig
⊢ ⟦assign,
      { aig := (aig.mkXorCached { lhs := input.lhs, rhs := input.rhs }).aig,
        ref := { gate := input.cin.gate, hgate := ⋯ } }⟧ =
    ⟦assign, { aig := aig, ref := input.cin }⟧

Tactic:
rw [LawfulOperator.denote_mem_prefix (f := mkXorCached) (h := input.cin.hgate)]

Result:
no goals

Proof state:
α : Type
inst✝¹ : Hashable α
inst✝ : DecidableEq α
assign : α → Bool
aig : AIG α
input : FullAdderInput aig
⊢ ((⟦assign, { aig := aig, ref := input.lhs }⟧ ^^ ⟦assign, { aig := aig, ref := input.rhs }⟧) &&
        ⟦assign,
          { aig := (aig.mkXorCached { lhs := input.lhs, rhs := input.rhs }).aig,
            ref := { gate := input.cin.gate, hgate := ⋯ } }⟧ ||
      ⟦assign,
          {
            aig :=
              ((aig.mkXorCached { lhs := input.lhs, rhs := input.rhs }).aig.mkAndCached
                  { lhs := (aig.mkXorCached { lhs := input.lhs, rhs := input.rhs }).ref,
                    rhs := { gate := input.cin.gate, hgate := ⋯ } }).aig,
            ref := { gate := input.lhs.gate, hgate := ⋯ } }⟧ &&
        ⟦assign,
          {
            aig :=
              ((aig.mkXorCached { lhs := input.lhs, rhs := input.rhs }).aig.mkAndCached
                  { lhs := (aig.mkXorCached { lhs := input.lhs, rhs := input.rhs }).ref,
                    rhs := { gate := input.cin.gate, hgate := ⋯ } }).aig,
            ref := { gate := input.rhs.gate, hgate := ⋯ } }⟧) =
    ((⟦assign, { aig := aig, ref := input.lhs }⟧ ^^ ⟦assign, { aig := aig, ref := input.rhs }⟧) &&
        ⟦assign, { aig := aig, ref := input.cin }⟧ ||
      ⟦assign, { aig := aig, ref := input.lhs }⟧ && ⟦assign, { aig := aig, ref := input.rhs }⟧)

Tactic:
congr 2

Result:
case e_x.e_y
α : Type
inst✝¹ : Hashable α
inst✝ : DecidableEq α
assign : α → Bool
aig : AIG α
input : FullAdderInput aig
⊢ ⟦assign,
      { aig := (aig.mkXorCached { lhs := input.lhs, rhs := input.rhs }).aig,
        ref := { gate := input.cin.gate, hgate := ⋯ } }⟧ =
    ⟦assign, { aig := aig, ref := input.cin }⟧

case e_y.e_x
α : Type
inst✝¹ : Hashable α
inst✝ : DecidableEq α
assign : α → Bool
aig : AIG α
input : FullAdderInput aig
⊢ ⟦assign,
      {
        aig :=
          ((aig.mkXorCached { lhs := input.lhs, rhs := input.rhs }).aig.mkAndCached
              { lhs := (aig.mkXorCached { lhs := input.lhs, rhs := input.rhs }).ref,
                rhs := { gate := input.cin.gate, hgate := ⋯ } }).aig,
        ref := { gate := input.lhs.gate, hgate := ⋯ } }⟧ =
    ⟦assign, { aig := aig, ref := input.lhs }⟧

case e_y.e_y
α : Type
inst✝¹ : Hashable α
inst✝ : DecidableEq α
assign : α → Bool
aig : AIG α
input : FullAdderInput aig
⊢ ⟦assign,
      {
        aig :=
          ((aig.mkXorCached { lhs := input.lhs, rhs := input.rhs }).aig.mkAndCached
              { lhs := (aig.mkXorCached { lhs := input.lhs, rhs := input.rhs }).ref,
                rhs := { gate := input.cin.gate, hgate := ⋯ } }).aig,
        ref := { gate := input.rhs.gate, hgate := ⋯ } }⟧ =
    ⟦assign, { aig := aig, ref := input.rhs }⟧

Proof state:
case h
α : Type
inst✝¹ : Hashable α
inst✝ : DecidableEq α
assign : α → Bool
aig : AIG α
input : FullAdderInput aig
⊢ input.rhs.gate < aig.decls.size

Tactic:
apply Ref.hgate

Result:
no goals

Proof state:
case e_y.e_x
α : Type
inst✝¹ : Hashable α
inst✝ : DecidableEq α
assign : α → Bool
aig : AIG α
input : FullAdderInput aig
⊢ ⟦assign,
      {
        aig :=
          ((aig.mkXorCached { lhs := input.lhs, rhs := input.rhs }).aig.mkAndCached
              { lhs := (aig.mkXorCached { lhs := input.lhs, rhs := input.rhs }).ref,
                rhs := { gate := input.cin.gate, hgate := ⋯ } }).aig,
        ref := { gate := input.lhs.gate, hgate := ⋯ } }⟧ =
    ⟦assign, { aig := aig, ref := input.lhs }⟧

Tactic:
rw [LawfulOperator.denote_mem_prefix
    (f := mkAndCached)
    (h := by
      apply LawfulOperator.lt_size_of_lt_aig_size (f := mkXorCached)
      apply Ref.hgate),
  LawfulOperator.denote_mem_prefix (f := mkXorCached) (h := input.lhs.hgate)]

Result:
no goals