internlm/Lean-Github huggingface dataset:
Theorem: BVExpr.bitblast.mkOverflowBit.go_decl_eq
Proof state before:
case isTrue
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
curr a✝ : Nat
hcurr : curr ≤ a✝
aig : AIG α
cin : aig.Ref
lhs rhs : aig.RefStream a✝
res : AIG.Entrypoint α
h✝ : curr < a✝
hgo :
  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 ⋯) =
    res
idx✝ : Nat
h1✝ : idx✝ < aig.decls.size
h2✝ :
  idx✝ <
    (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 ⋯)).aig.decls.size
⊢ (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 ⋯)).aig.decls[idx✝] =
    aig.decls[idx✝]
Tactic:
rw [go_decl_eq]
Proof state after:
case isTrue
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
curr a✝ : Nat
hcurr : curr ≤ a✝
aig : AIG α
cin : aig.Ref
lhs rhs : aig.RefStream a✝
res : AIG.Entrypoint α
h✝ : curr < a✝
hgo :
  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 ⋯) =
    res
idx✝ : Nat
h1✝ : idx✝ < aig.decls.size
h2✝ :
  idx✝ <
    (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 ⋯)).aig.decls.size
⊢ (mkFullAdderCarry aig { lhs := lhs.getRef curr h✝, rhs := rhs.getRef curr h✝, cin := cin }).aig.decls[idx✝] =
    aig.decls[idx✝]

case isTrue.h1
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
curr a✝ : Nat
hcurr : curr ≤ a✝
aig : AIG α
cin : aig.Ref
lhs rhs : aig.RefStream a✝
res : AIG.Entrypoint α
h✝ : curr < a✝
hgo :
  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 ⋯) =
    res
idx✝ : Nat
h1✝ : idx✝ < aig.decls.size
h2✝ :
  idx✝ <
    (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 ⋯)).aig.decls.size
⊢ idx✝ < (mkFullAdderCarry aig { lhs := lhs.getRef curr h✝, rhs := rhs.getRef curr h✝, cin := cin }).aig.decls.size
Theorem: BVExpr.bitblast.mkOverflowBit.go_decl_eq
Proof state before:
case isTrue
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
curr a✝ : Nat
hcurr : curr ≤ a✝
aig : AIG α
cin : aig.Ref
lhs rhs : aig.RefStream a✝
res : AIG.Entrypoint α
h✝ : curr < a✝
hgo :
  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 ⋯) =
    res
idx✝ : Nat
h1✝ : idx✝ < aig.decls.size
h2✝ :
  idx✝ <
    (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 ⋯)).aig.decls.size
⊢ (mkFullAdderCarry aig { lhs := lhs.getRef curr h✝, rhs := rhs.getRef curr h✝, cin := cin }).aig.decls[idx✝] =
    aig.decls[idx✝]

case isTrue.h1
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
curr a✝ : Nat
hcurr : curr ≤ a✝
aig : AIG α
cin : aig.Ref
lhs rhs : aig.RefStream a✝
res : AIG.Entrypoint α
h✝ : curr < a✝
hgo :
  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 ⋯) =
    res
idx✝ : Nat
h1✝ : idx✝ < aig.decls.size
h2✝ :
  idx✝ <
    (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 ⋯)).aig.decls.size
⊢ idx✝ < (mkFullAdderCarry aig { lhs := lhs.getRef curr h✝, rhs := rhs.getRef curr h✝, cin := cin }).aig.decls.size
Tactic:
rw [AIG.LawfulOperator.decl_eq (f := mkFullAdderCarry)]
Proof state after:
case isTrue.h2
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
curr a✝ : Nat
hcurr : curr ≤ a✝
aig : AIG α
cin : aig.Ref
lhs rhs : aig.RefStream a✝
res : AIG.Entrypoint α
h✝ : curr < a✝
hgo :
  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 ⋯) =
    res
idx✝ : Nat
h1✝ : idx✝ < aig.decls.size
h2✝ :
  idx✝ <
    (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 ⋯)).aig.decls.size
⊢ idx✝ < (mkFullAdderCarry aig { lhs := lhs.getRef curr h✝, rhs := rhs.getRef curr h✝, cin := cin }).aig.decls.size
Theorem: BVExpr.bitblast.mkOverflowBit.go_decl_eq
Proof state before:
case isTrue.h2
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
curr a✝ : Nat
hcurr : curr ≤ a✝
aig : AIG α
cin : aig.Ref
lhs rhs : aig.RefStream a✝
res : AIG.Entrypoint α
h✝ : curr < a✝
hgo :
  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 ⋯) =
    res
idx✝ : Nat
h1✝ : idx✝ < aig.decls.size
h2✝ :
  idx✝ <
    (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 ⋯)).aig.decls.size
⊢ idx✝ < (mkFullAdderCarry aig { lhs := lhs.getRef curr h✝, rhs := rhs.getRef curr h✝, cin := cin }).aig.decls.size
Tactic:
apply AIG.LawfulOperator.lt_size_of_lt_aig_size (f := mkFullAdderCarry)
Proof state after:
case isTrue.h2.h
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
curr a✝ : Nat
hcurr : curr ≤ a✝
aig : AIG α
cin : aig.Ref
lhs rhs : aig.RefStream a✝
res : AIG.Entrypoint α
h✝ : curr < a✝
hgo :
  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 ⋯) =
    res
idx✝ : Nat
h1✝ : idx✝ < aig.decls.size
h2✝ :
  idx✝ <
    (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 ⋯)).aig.decls.size
⊢ idx✝ < aig.decls.size
Theorem: BVExpr.bitblast.mkOverflowBit.go_decl_eq
Proof state before:
case isTrue.h2.h
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
curr a✝ : Nat
hcurr : curr ≤ a✝
aig : AIG α
cin : aig.Ref
lhs rhs : aig.RefStream a✝
res : AIG.Entrypoint α
h✝ : curr < a✝
hgo :
  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 ⋯) =
    res
idx✝ : Nat
h1✝ : idx✝ < aig.decls.size
h2✝ :
  idx✝ <
    (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 ⋯)).aig.decls.size
⊢ idx✝ < aig.decls.size
Tactic:
assumption
Proof state after:
no goals
Theorem: BVExpr.bitblast.mkOverflowBit.go_decl_eq
Proof state before:
case isFalse
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
curr a✝ : Nat
hcurr : curr ≤ a✝
aig : AIG α
cin : aig.Ref
lhs rhs : aig.RefStream a✝
res : AIG.Entrypoint α
h✝ : ¬curr < a✝
hgo : { aig := aig, ref := cin } = res
⊢ ∀ (idx : Nat) (h1 : idx < aig.decls.size) (h2 : idx < res.aig.decls.size), res.aig.decls[idx] = aig.decls[idx]
Tactic:
simp [← hgo]
Proof state after:
no goals
Theorem: AIG.if_as_bool
Proof state before:
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
d l r : Bool
⊢ (if d = true then l else r) = (d && l || !d && r)
Tactic:
revert d l r
Proof state after:
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
⊢ ∀ (d l r : Bool), (if d = true then l else r) = (d && l || !d && r)
Theorem: AIG.if_as_bool
Proof state before:
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
⊢ ∀ (d l r : Bool), (if d = true then l else r) = (d && l || !d && r)
Tactic:
decide
Proof state after:
no goals
Theorem: AIG.denote_mkIfCached
Proof 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]
Proof 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⟧)
Theorem: AIG.denote_mkIfCached
Proof 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
Proof 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⟧)
Theorem: AIG.denote_mkIfCached
Proof 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]
Proof 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⟧)
Theorem: AIG.denote_mkIfCached
Proof 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
Proof 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⟧
Theorem: AIG.denote_mkIfCached
Proof 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]
Proof 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⟧
Theorem: AIG.denote_mkIfCached
Proof 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]
Proof 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⟧
Theorem: AIG.denote_mkIfCached
Proof 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]
Proof state after:
no goals
Theorem: AIG.denote_mkIfCached
Proof 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]
Proof 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