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

State before:
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
assign : α → Bool
aig : AIG α
input : FullAdderInput aig
⊢ ⟦mkFullAdderCarry aig input, assign⟧ =
    (xor ⟦{ 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 }, assign⟧)
Tactic:
simp only [mkFullAdderCarry, Ref_cast', Int.reduceNeg, denote_mkOrCached,
  LawfulOperator.denote_input_entry, denote_mkAndCached, denote_projected_entry',
  denote_mkXorCached, denote_projected_entry]
State after:
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
assign : α → Bool
aig : AIG α
input : FullAdderInput aig
⊢ (xor ⟦{ 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⟧) =
    (xor ⟦{ 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 }, assign⟧)

State before:
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
assign : α → Bool
aig : AIG α
input : FullAdderInput aig
⊢ (xor ⟦{ 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⟧) =
    (xor ⟦{ 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 }, assign⟧)
Tactic:
conv =>
  lhs
  lhs
  rw [LawfulOperator.denote_mem_prefix (f := mkXorCached) (h := input.cin.hgate)]
State after:
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
assign : α → Bool
aig : AIG α
input : FullAdderInput aig
⊢ (xor ⟦{ aig := aig, ref := input.lhs }, assign⟧ ⟦{ aig := aig, ref := input.rhs }, assign⟧ &&
        ⟦{ aig := 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⟧) =
    (xor ⟦{ 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 }, assign⟧)

State before:
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
assign : α → Bool
aig : AIG α
input : FullAdderInput aig
⊢ (xor ⟦{ aig := aig, ref := input.lhs }, assign⟧ ⟦{ aig := aig, ref := input.rhs }, assign⟧ &&
        ⟦{ aig := 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⟧) =
    (xor ⟦{ 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 }, assign⟧)
Tactic:
conv =>
  lhs
  rhs
  lhs
  rw [
    LawfulOperator.denote_mem_prefix
      (f := mkAndCached)
      (h := by
        apply LawfulOperator.lt_size_of_lt_aig_size (f := mkXorCached)
        apply Ref.hgate
      )
  ]
State after:
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
assign : α → Bool
aig : AIG α
input : FullAdderInput aig
⊢ (xor ⟦{ aig := aig, ref := input.lhs }, assign⟧ ⟦{ aig := aig, ref := input.rhs }, assign⟧ &&
        ⟦{ aig := aig, ref := { gate := input.cin.gate, hgate := ⋯ } }, assign⟧ ||
      ⟦{ aig := (aig.mkXorCached { lhs := input.lhs, rhs := input.rhs }).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⟧) =
    (xor ⟦{ 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 }, assign⟧)

State before:
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
assign : α → Bool
aig : AIG α
input : FullAdderInput aig
⊢ (xor ⟦{ aig := aig, ref := input.lhs }, assign⟧ ⟦{ aig := aig, ref := input.rhs }, assign⟧ &&
        ⟦{ aig := aig, ref := { gate := input.cin.gate, hgate := ⋯ } }, assign⟧ ||
      ⟦{ aig := (aig.mkXorCached { lhs := input.lhs, rhs := input.rhs }).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⟧) =
    (xor ⟦{ 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 }, assign⟧)
Tactic:
conv =>
  lhs
  rhs
  lhs
  rw [LawfulOperator.denote_mem_prefix (f := mkXorCached) (h := input.lhs.hgate)]
State after:
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
assign : α → Bool
aig : AIG α
input : FullAdderInput aig
⊢ (xor ⟦{ aig := aig, ref := input.lhs }, assign⟧ ⟦{ aig := aig, ref := input.rhs }, assign⟧ &&
        ⟦{ aig := aig, ref := { gate := input.cin.gate, hgate := ⋯ } }, assign⟧ ||
      ⟦{ aig := 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⟧) =
    (xor ⟦{ 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 }, assign⟧)

State before:
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
assign : α → Bool
aig : AIG α
input : FullAdderInput aig
⊢ (xor ⟦{ aig := aig, ref := input.lhs }, assign⟧ ⟦{ aig := aig, ref := input.rhs }, assign⟧ &&
        ⟦{ aig := aig, ref := { gate := input.cin.gate, hgate := ⋯ } }, assign⟧ ||
      ⟦{ aig := 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⟧) =
    (xor ⟦{ 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 }, assign⟧)
Tactic:
conv =>
  lhs
  rhs
  rhs
  rw [
    LawfulOperator.denote_mem_prefix
      (f := mkAndCached)
      (h := by
        apply LawfulOperator.lt_size_of_lt_aig_size (f := mkXorCached)
        apply Ref.hgate
      )
  ]
State after:
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
assign : α → Bool
aig : AIG α
input : FullAdderInput aig
⊢ (xor ⟦{ aig := aig, ref := input.lhs }, assign⟧ ⟦{ aig := aig, ref := input.rhs }, assign⟧ &&
        ⟦{ aig := aig, ref := { gate := input.cin.gate, hgate := ⋯ } }, assign⟧ ||
      ⟦{ aig := aig, ref := { gate := input.lhs.gate, hgate := ⋯ } }, assign⟧ &&
        ⟦{ aig := (aig.mkXorCached { lhs := input.lhs, rhs := input.rhs }).aig,
            ref := { gate := input.rhs.gate, hgate := ⋯ } },
          assign⟧) =
    (xor ⟦{ 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 }, assign⟧)

State before:
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
assign : α → Bool
aig : AIG α
input : FullAdderInput aig
⊢ (xor ⟦{ aig := aig, ref := input.lhs }, assign⟧ ⟦{ aig := aig, ref := input.rhs }, assign⟧ &&
        ⟦{ aig := aig, ref := { gate := input.cin.gate, hgate := ⋯ } }, assign⟧ ||
      ⟦{ aig := aig, ref := { gate := input.lhs.gate, hgate := ⋯ } }, assign⟧ &&
        ⟦{ aig := (aig.mkXorCached { lhs := input.lhs, rhs := input.rhs }).aig,
            ref := { gate := input.rhs.gate, hgate := ⋯ } },
          assign⟧) =
    (xor ⟦{ 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 }, assign⟧)
Tactic:
conv =>
  lhs
  rhs
  rhs
  rw [LawfulOperator.denote_mem_prefix (f := mkXorCached) (h := input.rhs.hgate)]
State after:
no goals

State before:
α : Type
inst✝² : BEq α
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)
State after:
case h
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
assign : α → Bool
aig : AIG α
input : FullAdderInput aig
⊢ input.lhs.gate < aig.decls.size

State before:
case h
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
assign : α → Bool
aig : AIG α
input : FullAdderInput aig
⊢ input.lhs.gate < aig.decls.size
Tactic:
apply Ref.hgate
State after:
no goals

State before:
α : Type
inst✝² : BEq α
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)
State after:
case h
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
assign : α → Bool
aig : AIG α
input : FullAdderInput aig
⊢ input.rhs.gate < aig.decls.size

State before:
case h
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
assign : α → Bool
aig : AIG α
input : FullAdderInput aig
⊢ input.rhs.gate < aig.decls.size
Tactic:
apply Ref.hgate
State after:
no goals