Proof step 1 from proof butmin-put-01 (conclusion) (back to tree)

System applied rule normalize

And obtained the following new goals

• Proof step 2:

  a = (st[a := d0]).min, (st[a := d]).butmin ≠ st, ¬ a ∈ st ⊦

Rule argument

Additional information

Proof step 2 from proof butmin-put-01 (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 3:

  a = (st[a := d0]).min, st[a := d] -- (st[a := d]).min ≠ st, ¬ a ∈ st ⊦

Rule argument

Additional information

Used simplifier rules: Butmin: ⊦ st.butmin = st -- st.min;

Proof step 3 from proof butmin-put-01 (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 4:

  ⊦ st1 = st2 ↔ (∀ a. (a ∈ st1 ↔ a ∈ st2) ∧ st1[a] = st2[a])

• Proof step 5:

  a = (st[a := d0]).min, ¬ a ∈ st, ∃ a0. ¬((a0 ∈ st[a := d] -- (st[a := d]).min ↔ a0 ∈ st) ∧ (st[a := d] -- (st[a := d]).min)[a0] = st[a0]) ⊦

Rule argument

Additional information

Used terms: st[a := d] -- (st[a := d]).min, st

Proof step 4 from proof butmin-put-01 (previous step) (back to tree)

A spec-lemma

Proof step 5 from proof butmin-put-01 (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 6:

  a = (st[a := d0]).min, ¬ a ∈ st ⊦ (a0 ∈ st[a := d] -- (st[a := d]).min ↔ a0 ∈ st) ∧ (st[a := d] -- (st[a := d]).min)[a0] = st[a0]

Rule argument

Additional information

Proof step 6 from proof butmin-put-01 (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 7:

  ⊦ a ≠ b → (st -- b)[a] = st[a]

• Proof step 8:

  a = (st[a := d0]).min, a0 = (st[a := d]).min, ¬ a ∈ st ⊦ (a0 ∈ st[a := d] -- (st[a := d]).min ↔ a0 ∈ st) ∧ (st[a := d] -- (st[a := d]).min)[a0] = st[a0]

• Proof step 10:

  a = (st[a := d0]).min, a0 ≠ (st[a := d]).min, ¬ a ∈ st ⊦ (a0 ∈ st[a := d] -- (st[a := d]).min ↔ a0 ∈ st) ∧ (st[a := d])[a0] = st[a0]

Rule argument

Additional information

Used terms: a0, (st[a := d]).min, st[a := d]

Proof step 7 from proof butmin-put-01 (previous step) (back to tree)

A spec-lemma

Proof step 8 from proof butmin-put-01 (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 9:

  a = (st[a := d0]).min, ¬ a ∈ st ⊦ ((st[a := d]).min ∈ st[a := d] -- (st[a := d]).min ↔ (st[a := d]).min ∈ st) ∧ ∅[(st[a := d]).min] = st[(st[a := d]).min]

Rule argument

Additional information

Used simplifier rules: ⊦ (st -- a)[a] = ∅[a]; (s)

Proof step 9 from proof butmin-put-01 (previous step) (back to tree)

User applied rule case distinction

And closed the goal!

Rule argument

Additional information

Used simplifier rules: min-put-01: ⊦ (st[a := d]).min = a → (st[a := d0]).min = a; min-put-01: ⊦ (st[a := d]).min = a → (st[a := d0]).min = a; ⊦ ¬ a ∈ st → st[a] = ∅[a]; (s) ⊦ st[a := d] -- a = st -- a; (s) ⊦ ¬ a ∈ st → st -- a = st; (s)

Proof step 10 from proof butmin-put-01 (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 11:

  a = (st[a := d0]).min, a0 ≠ (st[a := d]).min, ¬ a ∈ st ⊦ (a0 ∈ st[a := d] -- (st[a := d]).min ↔ a0 ∈ st) ∧ (st[a := d])[a0] = st[a0]

Rule argument

Additional information

Proof step 11 from proof butmin-put-01 (previous step) (back to tree)

Heuristic weak cut applied rule cut formula

And obtained the following new goals

• Proof step 12:

  a = (st[a := d0]).min, a0 = a, a0 ≠ (st[a := d]).min, ¬ a ∈ st ⊦ (a0 ∈ st[a := d] -- (st[a := d]).min ↔ a0 ∈ st) ∧ (st[a := d])[a0] = st[a0]

• Proof step 18:

  a = (st[a := d0]).min, a0 ≠ a, a0 ≠ (st[a := d]).min, ¬ a ∈ st ⊦ (a0 ∈ st[a := d] -- (st[a := d]).min ↔ a0 ∈ st) ∧ (st[a := d])[a0] = st[a0]

Rule argument

Additional information

Used formulas: a0 = a

Proof step 12 from proof butmin-put-01 (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 13:

  a = (st[a := d0]).min, a ≠ (st[a := d]).min, ¬ a ∈ st ⊦ ¬ a ∈ st[a := ∅[a]] -- (st[a := ∅[a]]).min ∧ d = ∅[a]

Rule argument

Additional information

Used simplifier rules: ⊦ ¬ a ∈ st → st[a] = ∅[a]; (s) ⊦ (st[a := d])[a] = d; (s)

Proof step 13 from proof butmin-put-01 (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 14:

  ⊦ st ≠ ∅ → st.min = st.keys.min

• Proof step 15:

  a = (st[a := d0]).keys.min, st[a := d0] ≠ ∅, a ≠ (st[a := d]).min, ¬ a ∈ st ⊦ ¬ a ∈ st[a := ∅[a]] -- (st[a := ∅[a]]).min ∧ d = ∅[a]

Rule argument

Additional information

Used simplifier rules: ⊦ st[a := d] ≠ ∅; (s) Used terms: st[a := d0]

Proof step 14 from proof butmin-put-01 (previous step) (back to tree)

Lemma min-def

Proof step 15 from proof butmin-put-01 (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 16:

  a = (st.keys ++ a).min, a ≠ (st[a := d]).min, ¬ a ∈ st ⊦ ¬ a ∈ st[a := ∅[a]] -- (st[a := ∅[a]]).min ∧ d = ∅[a]

Rule argument

Additional information

Used simplifier rules: insert-03: ⊦ (st[a := d]).keys = st.keys ++ a; ⊦ st[a := d] ≠ ∅; (s)

Proof step 16 from proof butmin-put-01 (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 17:

  ⊦ st ≠ ∅ → st.min = st.keys.min

Rule argument

Additional information

Used simplifier rules: insert-03: ⊦ (st[a := d]).keys = st.keys ++ a; ⊦ st[a := d] ≠ ∅; (s) Used terms: st[a := d]

Proof step 17 from proof butmin-put-01 (previous step) (back to tree)

Lemma min-def

Proof step 18 from proof butmin-put-01 (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 19:

  a = (st[a := d0]).min, ¬(a0 ∈ st[a := d] -- (st[a := d]).min ↔ a0 ∈ st), a0 ≠ a, a0 ≠ (st[a := d]).min, ¬ a ∈ st ⊦

Rule argument

Additional information

Used simplifier rules: ⊦ a ≠ b → (st[b := d])[a] = st[a]; (s)

Proof step 19 from proof butmin-put-01 (previous step) (back to tree)

User applied rule case distinction

And closed the goal!

Rule argument

Additional information

Used simplifier rules: min-put-01: ⊦ (st[a := d]).min = a → (st[a := d0]).min = a; min-put-01: ⊦ (st[a := d]).min = a → (st[a := d0]).min = a; ⊦ st[a := d] -- a = st -- a; (s) ⊦ ¬ a ∈ st → st -- a = st; (s)