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

System applied rule normalize

And obtained the following new goals

• Proof step 2:

  (st(a := d)).butmin ≠ st.butmin(a := d), a ≠ (st(a := d)).min ⊦

Rule argument

Additional information

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

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 3:

  st(a := d) -- (st(a := d)).min ≠ (st -- st.min)(a := d), a ≠ (st(a := d)).min ⊦

Rule argument

Additional information

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

Proof step 3 from proof butmin-rewput (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 := d)).min, ∃ a0. ¬((a0 ∈ st(a := d) -- (st(a := d)).min ↔ a0 ∈ (st -- st.min)(a := d)) ∧ (st(a := d) -- (st(a := d)).min)(a0) = (st -- st.min)(a := d)(a0)) ⊦

Rule argument

Additional information

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

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

A spec-lemma

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

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 6:

  a ≠ (st(a := d)).min ⊦ (a0 ∈ st(a := d) -- (st(a := d)).min ↔ a0 ∈ (st -- st.min)(a := d)) ∧ (st(a := d) -- (st(a := d)).min)(a0) = (st -- st.min)(a := d)(a0)

Rule argument

Additional information

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

Heuristic weak cut applied rule cut formula

And obtained the following new goals

• Proof step 7:

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

Rule argument

Additional information

Used simplifier rules: ⊦ a ∈ st -- b ↔ a ≠ b ∧ a ∈ st; (ws) ⊦ a ∈ st(a := d); (s) ⊦ a ≠ b → (st -- b)(a) = st(a); (s) ⊦ st(a := d)(a) = d; (s) Used formulas: a0 = a

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

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 8:

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

Rule argument

Additional information

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

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

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 9:

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

• Proof step 10:

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

• Proof step 15:

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

Rule argument

Additional information

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

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

A spec-lemma

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

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 11:

  (st(a := d)).min ≠ st.min, (st(a := d)).min ≠ a, st.min < (st(a := d)).min, (st(a := d)).min ∈ st ⊦

Rule argument

Additional information

Used simplifier rules: Min-min: ⊦ a ∈ st → ¬ a < st.min; inf: ⊦ a ∈ st → a ∈ st.keys; Keys: ⊦ a ∈ st.keys ↔ a ∈ st; ⊦ a ≠ b → (a < b ↔ ¬ b < a); (ss) ⊦ a ∈ st -- b ↔ a ≠ b ∧ a ∈ st; (ws) ⊦ ¬ a ∈ st → st(a) = ∅(a); (s) ⊦ (st -- a)(a) = ∅(a); (s) ⊦ ¬ a ∈ st -- a; (s)

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

Heuristic weak cut applied rule cut formula

And obtained the following new goals

• Proof step 12:

  (st(a := d)).min ≠ st.min, (st(a := d)).min ≠ a, st ≠ ∅, st.min < (st(a := d)).min, (st(a := d)).min ∈ st ⊦

Rule argument

Additional information

Used simplifier rules: min: ⊦ (∅(a := d)).min = a; Used formulas: st = ∅

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

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 13:

  (st(a := d)).min ≠ a, (st(a := d)).min ≠ st.keys.min, st ≠ ∅, st.keys.min < (st(a := d)).min, (st(a := d)).min ∈ st, st.keys.min ∈ st ⊦

Rule argument

Additional information

Used simplifier rules: Min-in: ⊦ st ≠ ∅ → st.min ∈ st; Min-min: ⊦ a ∈ st → ¬ a < st.min; inf: ⊦ a ∈ st → a ∈ st.keys; Keys: ⊦ a ∈ st.keys ↔ a ∈ st; min-def: ⊦ st ≠ ∅ → st.min = st.keys.min; ⊦ ¬ a < a; (s)

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

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 14:

  ⊦ a ≠ (st(a := d)).min → (st(a := d)).min = st.min

Rule argument

Additional information

Used simplifier rules: min-def: ⊦ st ≠ ∅ → st.min = st.keys.min; Used terms: d, a, st

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

Lemma min-put

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

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 16:

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

Rule argument

Additional information

Used simplifier rules: ⊦ a ≠ b → st(b := d)(a) = st(a); (s) ⊦ a ≠ b → (a ∈ st(b := d) ↔ a ∈ st); (s) ⊦ a ∈ st -- b ↔ a ≠ b ∧ a ∈ st; (ws)

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

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 17:

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

• Proof step 18:

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

Rule argument

Additional information

Used simplifier rules: ⊦ a ∈ st -- b ↔ a ≠ b ∧ a ∈ st; (ws) Used terms: a0, st.min, st

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

A spec-lemma

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

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 19:

  st.min ≠ a, st.min ≠ (st(a := d)).min, a ≠ (st(a := d)).min, st.min ∈ st ⊦

Rule argument

Additional information

Used simplifier rules: Min-min: ⊦ a ∈ st → ¬ a < st.min; inf: ⊦ a ∈ st → a ∈ st.keys; Keys: ⊦ a ∈ st.keys ↔ a ∈ st; ⊦ ¬ a < a; (s) ⊦ ¬ a ∈ st → st(a) = ∅(a); (s) ⊦ ¬ a ∈ st → st -- a = st; (s) ⊦ a ∈ st -- b ↔ a ≠ b ∧ a ∈ st; (ws)

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

Heuristic weak cut applied rule cut formula

And obtained the following new goals

• Proof step 20:

  st.min ≠ a, st.min ≠ (st(a := d)).min, a ≠ (st(a := d)).min, st ≠ ∅, st.min ∈ st ⊦

Rule argument

Additional information

Used simplifier rules: min: ⊦ (∅(a := d)).min = a; Used formulas: st = ∅

Proof step 20 from proof butmin-rewput (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 21:

  st.keys.min ≠ (st(a := d)).min, st.keys.min ≠ a, a ≠ (st(a := d)).min, st ≠ ∅, st.keys.min ∈ st ⊦

Rule argument

Additional information

Used simplifier rules: Min-min: ⊦ a ∈ st → ¬ a < st.min; inf: ⊦ a ∈ st → a ∈ st.keys; Min-in: ⊦ st ≠ ∅ → st.min ∈ st; Keys: ⊦ a ∈ st.keys ↔ a ∈ st; min-def: ⊦ st ≠ ∅ → st.min = st.keys.min; ⊦ ¬ a < a; (s)

Proof step 21 from proof butmin-rewput (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 22:

  ⊦ a ≠ (st(a := d)).min → (st(a := d)).min = st.min

Rule argument

Additional information

Used simplifier rules: min-def: ⊦ st ≠ ∅ → st.min = st.keys.min; Used terms: d, a, st

Proof step 22 from proof butmin-rewput (previous step) (back to tree)

Lemma min-put