Theorem: AIG.denote_mkIfCached (LeanSAT/AIG/If.lean)

State before:
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
assign : α → Bool
aig : AIG α
input : aig.TernaryInput
⊢ ⟦aig.mkIfCached input, assign⟧ =
    if ⟦{ aig := aig, ref := input.discr }, assign⟧ = true then ⟦{ aig := aig, ref := input.lhs }, assign⟧
    else ⟦{ aig := aig, ref := input.rhs }, assign⟧
Tactic:
rw [if_as_bool]
State after:
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
assign : α → Bool
aig : AIG α
input : aig.TernaryInput
⊢ ⟦aig.mkIfCached input, assign⟧ =
    (⟦{ aig := aig, ref := input.discr }, assign⟧ && ⟦{ aig := aig, ref := input.lhs }, assign⟧ ||
      !⟦{ aig := aig, ref := input.discr }, assign⟧ && ⟦{ aig := aig, ref := input.rhs }, assign⟧)

State before:
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
assign : α → Bool
aig : AIG α
input : aig.TernaryInput
⊢ ⟦aig.mkIfCached input, assign⟧ =
    (⟦{ aig := aig, ref := input.discr }, assign⟧ && ⟦{ aig := aig, ref := input.lhs }, assign⟧ ||
      !⟦{ aig := aig, ref := input.discr }, assign⟧ && ⟦{ aig := aig, ref := input.rhs }, assign⟧)
Tactic:
unfold mkIfCached
State after:
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
assign : α → Bool
aig : AIG α
input : aig.TernaryInput
⊢ ⟦let res := aig.mkAndCached { lhs := input.discr, rhs := input.lhs };
      let aig_1 := res.aig;
      let lhsRef := res.ref;
      let input_1 := input.cast ⋯;
      let res_1 := aig_1.mkNotCached input_1.discr;
      let aig_2 := res_1.aig;
      let notDiscr := res_1.ref;
      let input_2 := input_1.cast ⋯;
      let res_2 := aig_2.mkAndCached { lhs := notDiscr, rhs := input_2.rhs };
      let aig_3 := res_2.aig;
      let rhsRef := res_2.ref;
      let lhsRef := lhsRef.cast ⋯;
      aig_3.mkOrCached { lhs := lhsRef, rhs := rhsRef },
      assign⟧ =
    (⟦{ aig := aig, ref := input.discr }, assign⟧ && ⟦{ aig := aig, ref := input.lhs }, assign⟧ ||
      !⟦{ aig := aig, ref := input.discr }, assign⟧ && ⟦{ aig := aig, ref := input.rhs }, assign⟧)

State before:
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
assign : α → Bool
aig : AIG α
input : aig.TernaryInput
⊢ ⟦let res := aig.mkAndCached { lhs := input.discr, rhs := input.lhs };
      let aig_1 := res.aig;
      let lhsRef := res.ref;
      let input_1 := input.cast ⋯;
      let res_1 := aig_1.mkNotCached input_1.discr;
      let aig_2 := res_1.aig;
      let notDiscr := res_1.ref;
      let input_2 := input_1.cast ⋯;
      let res_2 := aig_2.mkAndCached { lhs := notDiscr, rhs := input_2.rhs };
      let aig_3 := res_2.aig;
      let rhsRef := res_2.ref;
      let lhsRef := lhsRef.cast ⋯;
      aig_3.mkOrCached { lhs := lhsRef, rhs := rhsRef },
      assign⟧ =
    (⟦{ aig := aig, ref := input.discr }, assign⟧ && ⟦{ aig := aig, ref := input.lhs }, assign⟧ ||
      !⟦{ aig := aig, ref := input.discr }, assign⟧ && ⟦{ aig := aig, ref := input.rhs }, assign⟧)
Tactic:
simp only [TernaryInput.cast, Ref_cast', id_eq, Int.reduceNeg, denote_mkOrCached,
  denote_projected_entry, denote_mkAndCached, denote_mkNotCached]
State after:
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
assign : α → Bool
aig : AIG α
input : aig.TernaryInput
⊢ (⟦{
          aig :=
            (((aig.mkAndCached { lhs := input.discr, rhs := input.lhs }).aig.mkNotCached
                      { gate := input.discr.gate, hgate := ⋯ }).aig.mkAndCached
                {
                  lhs :=
                    ((aig.mkAndCached { lhs := input.discr, rhs := input.lhs }).aig.mkNotCached
                        { gate := input.discr.gate, hgate := ⋯ }).ref,
                  rhs := { gate := input.rhs.gate, hgate := ⋯ } }).aig,
          ref := { gate := (aig.mkAndCached { lhs := input.discr, rhs := input.lhs }).ref.gate, hgate := ⋯ } },
        assign⟧ ||
      !⟦{ aig := (aig.mkAndCached { lhs := input.discr, rhs := input.lhs }).aig,
              ref := { gate := input.discr.gate, hgate := ⋯ } },
            assign⟧ &&
        ⟦{
            aig :=
              ((aig.mkAndCached { lhs := input.discr, rhs := input.lhs }).aig.mkNotCached
                  { gate := input.discr.gate, hgate := ⋯ }).aig,
            ref := { gate := input.rhs.gate, hgate := ⋯ } },
          assign⟧) =
    (⟦{ aig := aig, ref := input.discr }, assign⟧ && ⟦{ aig := aig, ref := input.lhs }, assign⟧ ||
      !⟦{ aig := aig, ref := input.discr }, assign⟧ && ⟦{ aig := aig, ref := input.rhs }, assign⟧)

State before:
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
assign : α → Bool
aig : AIG α
input : aig.TernaryInput
⊢ (⟦{
          aig :=
            (((aig.mkAndCached { lhs := input.discr, rhs := input.lhs }).aig.mkNotCached
                      { gate := input.discr.gate, hgate := ⋯ }).aig.mkAndCached
                {
                  lhs :=
                    ((aig.mkAndCached { lhs := input.discr, rhs := input.lhs }).aig.mkNotCached
                        { gate := input.discr.gate, hgate := ⋯ }).ref,
                  rhs := { gate := input.rhs.gate, hgate := ⋯ } }).aig,
          ref := { gate := (aig.mkAndCached { lhs := input.discr, rhs := input.lhs }).ref.gate, hgate := ⋯ } },
        assign⟧ ||
      !⟦{ aig := (aig.mkAndCached { lhs := input.discr, rhs := input.lhs }).aig,
              ref := { gate := input.discr.gate, hgate := ⋯ } },
            assign⟧ &&
        ⟦{
            aig :=
              ((aig.mkAndCached { lhs := input.discr, rhs := input.lhs }).aig.mkNotCached
                  { gate := input.discr.gate, hgate := ⋯ }).aig,
            ref := { gate := input.rhs.gate, hgate := ⋯ } },
          assign⟧) =
    (⟦{ aig := aig, ref := input.discr }, assign⟧ && ⟦{ aig := aig, ref := input.lhs }, assign⟧ ||
      !⟦{ aig := aig, ref := input.discr }, assign⟧ && ⟦{ aig := aig, ref := input.rhs }, assign⟧)
Tactic:
congr 2
State after:
case e_x
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
assign : α → Bool
aig : AIG α
input : aig.TernaryInput
⊢ ⟦{
        aig :=
          (((aig.mkAndCached { lhs := input.discr, rhs := input.lhs }).aig.mkNotCached
                    { gate := input.discr.gate, hgate := ⋯ }).aig.mkAndCached
              {
                lhs :=
                  ((aig.mkAndCached { lhs := input.discr, rhs := input.lhs }).aig.mkNotCached
                      { gate := input.discr.gate, hgate := ⋯ }).ref,
                rhs := { gate := input.rhs.gate, hgate := ⋯ } }).aig,
        ref := { gate := (aig.mkAndCached { lhs := input.discr, rhs := input.lhs }).ref.gate, hgate := ⋯ } },
      assign⟧ =
    (⟦{ aig := aig, ref := input.discr }, assign⟧ && ⟦{ aig := aig, ref := input.lhs }, assign⟧)

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

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

State before:
case e_x
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
assign : α → Bool
aig : AIG α
input : aig.TernaryInput
⊢ ⟦{
        aig :=
          (((aig.mkAndCached { lhs := input.discr, rhs := input.lhs }).aig.mkNotCached
                    { gate := input.discr.gate, hgate := ⋯ }).aig.mkAndCached
              {
                lhs :=
                  ((aig.mkAndCached { lhs := input.discr, rhs := input.lhs }).aig.mkNotCached
                      { gate := input.discr.gate, hgate := ⋯ }).ref,
                rhs := { gate := input.rhs.gate, hgate := ⋯ } }).aig,
        ref := { gate := (aig.mkAndCached { lhs := input.discr, rhs := input.lhs }).ref.gate, hgate := ⋯ } },
      assign⟧ =
    (⟦{ aig := aig, ref := input.discr }, assign⟧ && ⟦{ aig := aig, ref := input.lhs }, assign⟧)

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

case e_y.e_y
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
assign : α → Bool
aig : AIG α
input : aig.TernaryInput
⊢ ⟦{
        aig :=
          ((aig.mkAndCached { lhs := input.discr, rhs := input.lhs }).aig.mkNotCached
              { gate := input.discr.gate, hgate := ⋯ }).aig,
        ref := { gate := input.rhs.gate, hgate := ⋯ } },
      assign⟧ =
    ⟦{ aig := aig, ref := input.rhs }, assign⟧
Tactic:
. rw [LawfulOperator.denote_mem_prefix]
  rw [LawfulOperator.denote_mem_prefix]
  . simp
  . simp [Ref.hgate]
State after:
case e_y.e_x
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
assign : α → Bool
aig : AIG α
input : aig.TernaryInput
⊢ (!⟦{ aig := (aig.mkAndCached { lhs := input.discr, rhs := input.lhs }).aig,
          ref := { gate := input.discr.gate, hgate := ⋯ } },
        assign⟧) =
    !⟦{ aig := aig, ref := input.discr }, assign⟧

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

State before:
case e_y.e_x
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
assign : α → Bool
aig : AIG α
input : aig.TernaryInput
⊢ (!⟦{ aig := (aig.mkAndCached { lhs := input.discr, rhs := input.lhs }).aig,
          ref := { gate := input.discr.gate, hgate := ⋯ } },
        assign⟧) =
    !⟦{ aig := aig, ref := input.discr }, assign⟧

case e_y.e_y
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
assign : α → Bool
aig : AIG α
input : aig.TernaryInput
⊢ ⟦{
        aig :=
          ((aig.mkAndCached { lhs := input.discr, rhs := input.lhs }).aig.mkNotCached
              { gate := input.discr.gate, hgate := ⋯ }).aig,
        ref := { gate := input.rhs.gate, hgate := ⋯ } },
      assign⟧ =
    ⟦{ aig := aig, ref := input.rhs }, assign⟧
Tactic:
. rw [LawfulOperator.denote_mem_prefix]
State after:
case e_y.e_y
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
assign : α → Bool
aig : AIG α
input : aig.TernaryInput
⊢ ⟦{
        aig :=
          ((aig.mkAndCached { lhs := input.discr, rhs := input.lhs }).aig.mkNotCached
              { gate := input.discr.gate, hgate := ⋯ }).aig,
        ref := { gate := input.rhs.gate, hgate := ⋯ } },
      assign⟧ =
    ⟦{ aig := aig, ref := input.rhs }, assign⟧

State before:
case e_y.e_y
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
assign : α → Bool
aig : AIG α
input : aig.TernaryInput
⊢ ⟦{
        aig :=
          ((aig.mkAndCached { lhs := input.discr, rhs := input.lhs }).aig.mkNotCached
              { gate := input.discr.gate, hgate := ⋯ }).aig,
        ref := { gate := input.rhs.gate, hgate := ⋯ } },
      assign⟧ =
    ⟦{ aig := aig, ref := input.rhs }, assign⟧
Tactic:
. rw [LawfulOperator.denote_mem_prefix]
  rw [LawfulOperator.denote_mem_prefix]
State after:
no goals

State before:
case e_x
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
assign : α → Bool
aig : AIG α
input : aig.TernaryInput
⊢ ⟦{
        aig :=
          (((aig.mkAndCached { lhs := input.discr, rhs := input.lhs }).aig.mkNotCached
                    { gate := input.discr.gate, hgate := ⋯ }).aig.mkAndCached
              {
                lhs :=
                  ((aig.mkAndCached { lhs := input.discr, rhs := input.lhs }).aig.mkNotCached
                      { gate := input.discr.gate, hgate := ⋯ }).ref,
                rhs := { gate := input.rhs.gate, hgate := ⋯ } }).aig,
        ref := { gate := (aig.mkAndCached { lhs := input.discr, rhs := input.lhs }).ref.gate, hgate := ⋯ } },
      assign⟧ =
    (⟦{ aig := aig, ref := input.discr }, assign⟧ && ⟦{ aig := aig, ref := input.lhs }, assign⟧)
Tactic:
rw [LawfulOperator.denote_mem_prefix]
State after:
case e_x
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
assign : α → Bool
aig : AIG α
input : aig.TernaryInput
⊢ ⟦{
        aig :=
          ((aig.mkAndCached { lhs := input.discr, rhs := input.lhs }).aig.mkNotCached
              { gate := input.discr.gate, hgate := ⋯ }).aig,
        ref := { gate := (aig.mkAndCached { lhs := input.discr, rhs := input.lhs }).ref.gate, hgate := ?e_x } },
      assign⟧ =
    (⟦{ aig := aig, ref := input.discr }, assign⟧ && ⟦{ aig := aig, ref := input.lhs }, assign⟧)

case e_x
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
assign : α → Bool
aig : AIG α
input : aig.TernaryInput
⊢ (aig.mkAndCached { lhs := input.discr, rhs := input.lhs }).ref.gate <
    ((aig.mkAndCached { lhs := input.discr, rhs := input.lhs }).aig.mkNotCached
            { gate := input.discr.gate, hgate := ⋯ }).aig.decls.size

State before:
case e_x
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
assign : α → Bool
aig : AIG α
input : aig.TernaryInput
⊢ ⟦{
        aig :=
          ((aig.mkAndCached { lhs := input.discr, rhs := input.lhs }).aig.mkNotCached
              { gate := input.discr.gate, hgate := ⋯ }).aig,
        ref := { gate := (aig.mkAndCached { lhs := input.discr, rhs := input.lhs }).ref.gate, hgate := ?e_x } },
      assign⟧ =
    (⟦{ aig := aig, ref := input.discr }, assign⟧ && ⟦{ aig := aig, ref := input.lhs }, assign⟧)

case e_x
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
assign : α → Bool
aig : AIG α
input : aig.TernaryInput
⊢ (aig.mkAndCached { lhs := input.discr, rhs := input.lhs }).ref.gate <
    ((aig.mkAndCached { lhs := input.discr, rhs := input.lhs }).aig.mkNotCached
            { gate := input.discr.gate, hgate := ⋯ }).aig.decls.size
Tactic:
rw [LawfulOperator.denote_mem_prefix]
State after:
case e_x
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
assign : α → Bool
aig : AIG α
input : aig.TernaryInput
⊢ ⟦{ aig := (aig.mkAndCached { lhs := input.discr, rhs := input.lhs }).aig,
        ref := { gate := (aig.mkAndCached { lhs := input.discr, rhs := input.lhs }).ref.gate, hgate := ?e_x } },
      assign⟧ =
    (⟦{ aig := aig, ref := input.discr }, assign⟧ && ⟦{ aig := aig, ref := input.lhs }, assign⟧)

case e_x
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
assign : α → Bool
aig : AIG α
input : aig.TernaryInput
⊢ (aig.mkAndCached { lhs := input.discr, rhs := input.lhs }).ref.gate <
    (aig.mkAndCached { lhs := input.discr, rhs := input.lhs }).aig.decls.size

State before:
case e_x
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
assign : α → Bool
aig : AIG α
input : aig.TernaryInput
⊢ ⟦{ aig := (aig.mkAndCached { lhs := input.discr, rhs := input.lhs }).aig,
        ref := { gate := (aig.mkAndCached { lhs := input.discr, rhs := input.lhs }).ref.gate, hgate := ?e_x } },
      assign⟧ =
    (⟦{ aig := aig, ref := input.discr }, assign⟧ && ⟦{ aig := aig, ref := input.lhs }, assign⟧)

case e_x
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
assign : α → Bool
aig : AIG α
input : aig.TernaryInput
⊢ (aig.mkAndCached { lhs := input.discr, rhs := input.lhs }).ref.gate <
    (aig.mkAndCached { lhs := input.discr, rhs := input.lhs }).aig.decls.size
Tactic:
. simp
State after:
case e_x
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
assign : α → Bool
aig : AIG α
input : aig.TernaryInput
⊢ (aig.mkAndCached { lhs := input.discr, rhs := input.lhs }).ref.gate <
    (aig.mkAndCached { lhs := input.discr, rhs := input.lhs }).aig.decls.size

State before:
case e_x
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
assign : α → Bool
aig : AIG α
input : aig.TernaryInput
⊢ (aig.mkAndCached { lhs := input.discr, rhs := input.lhs }).ref.gate <
    (aig.mkAndCached { lhs := input.discr, rhs := input.lhs }).aig.decls.size
Tactic:
. simp [Ref.hgate]
State after:
no goals

State before:
case e_x
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
assign : α → Bool
aig : AIG α
input : aig.TernaryInput
⊢ ⟦{ aig := (aig.mkAndCached { lhs := input.discr, rhs := input.lhs }).aig,
        ref := { gate := (aig.mkAndCached { lhs := input.discr, rhs := input.lhs }).ref.gate, hgate := ?e_x } },
      assign⟧ =
    (⟦{ aig := aig, ref := input.discr }, assign⟧ && ⟦{ aig := aig, ref := input.lhs }, assign⟧)
Tactic:
simp
State after:
no goals

State before:
case e_x
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
assign : α → Bool
aig : AIG α
input : aig.TernaryInput
⊢ (aig.mkAndCached { lhs := input.discr, rhs := input.lhs }).ref.gate <
    (aig.mkAndCached { lhs := input.discr, rhs := input.lhs }).aig.decls.size
Tactic:
simp [Ref.hgate]
State after:
no goals

State before:
case e_y.e_x
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
assign : α → Bool
aig : AIG α
input : aig.TernaryInput
⊢ (!⟦{ aig := (aig.mkAndCached { lhs := input.discr, rhs := input.lhs }).aig,
          ref := { gate := input.discr.gate, hgate := ⋯ } },
        assign⟧) =
    !⟦{ aig := aig, ref := input.discr }, assign⟧
Tactic:
rw [LawfulOperator.denote_mem_prefix]
State after:
no goals

State before:
case e_y.e_y
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
assign : α → Bool
aig : AIG α
input : aig.TernaryInput
⊢ ⟦{
        aig :=
          ((aig.mkAndCached { lhs := input.discr, rhs := input.lhs }).aig.mkNotCached
              { gate := input.discr.gate, hgate := ⋯ }).aig,
        ref := { gate := input.rhs.gate, hgate := ⋯ } },
      assign⟧ =
    ⟦{ aig := aig, ref := input.rhs }, assign⟧
Tactic:
rw [LawfulOperator.denote_mem_prefix]
State after:
case e_y.e_y
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
assign : α → Bool
aig : AIG α
input : aig.TernaryInput
⊢ ⟦{ aig := (aig.mkAndCached { lhs := input.discr, rhs := input.lhs }).aig,
        ref := { gate := input.rhs.gate, hgate := ?e_y.e_y } },
      assign⟧ =
    ⟦{ aig := aig, ref := input.rhs }, assign⟧

case e_y.e_y
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
assign : α → Bool
aig : AIG α
input : aig.TernaryInput
⊢ input.rhs.gate < (aig.mkAndCached { lhs := input.discr, rhs := input.lhs }).aig.decls.size

State before:
case e_y.e_y
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
assign : α → Bool
aig : AIG α
input : aig.TernaryInput
⊢ ⟦{ aig := (aig.mkAndCached { lhs := input.discr, rhs := input.lhs }).aig,
        ref := { gate := input.rhs.gate, hgate := ?e_y.e_y } },
      assign⟧ =
    ⟦{ aig := aig, ref := input.rhs }, assign⟧

case e_y.e_y
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
assign : α → Bool
aig : AIG α
input : aig.TernaryInput
⊢ input.rhs.gate < (aig.mkAndCached { lhs := input.discr, rhs := input.lhs }).aig.decls.size
Tactic:
rw [LawfulOperator.denote_mem_prefix]
State after:
no goals