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)