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

System applied rule normalize

And obtained the following new goals

• Proof step 2:

  st[a, d].min ≠ st.min, a ≠ st[a, d].min ⊦

Rule argument

Additional information

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

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 3:

  st[a, d].min ≠ st.min, a ≠ st[a, d].min ⊦

Rule argument

Additional information

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

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 4:

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

• Proof step 5:

  st[a, d].keys.min ≠ st.min, st[a, d] ≠ ∅, a ≠ st[a, d].keys.min ⊦

Rule argument

Additional information

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

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

Lemma min-def

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

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 6:

  (st.keys ++ a).min ≠ st.min, a ≠ (st.keys ++ a).min ⊦

Rule argument

Additional information

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

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

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 7:

  ⊦ a < s.min ∧ s ≠ ∅ → (s ++ a).min = a

• Proof step 8:

  (st.keys ++ a).min ≠ st.min, a ≠ (st.keys ++ a).min ⊦ a < st.keys.min ∧ st.keys ≠ ∅

Rule argument

Additional information

Used terms: a, st.keys

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

A spec-lemma

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

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 9:

  (st.keys ++ a).min ≠ st.min, a ≠ (st.keys ++ a).min ⊦ a < st.keys.min ∧ st.keys ≠ ∅

Rule argument

Additional information

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

User applied rule cut formula

And obtained the following new goals

• Proof step 10:

  st.keys ≠ ∅, (st.keys ++ a).min ≠ st.min, a ≠ (st.keys ++ a).min ⊦ a < st.keys.min ∧ st.keys ≠ ∅

Rule argument

Additional information

Used simplifier rules: ⊦ (∅ ++ a).min = a; (s) Used formulas: st.keys ≠ ∅

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

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 11:

  # st.keys ≠ 0, st.keys ≠ ∅, (st.keys ++ a).min ≠ st.min, a ≠ (st.keys ++ a).min, ¬ a < st.keys.min ⊦

Rule argument

Additional information

Used simplifier rules: size-zero: ⊦ # s ≠ 0 → s ≠ ∅; (forward) from specification set-basic size-zero-01: ⊦ s ≠ ∅ → # s ≠ 0; (forward) from specification set-basic

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

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 12:

  ⊦ a ∈ s ∧ ¬ b < a → (s ++ b).min = s.min

• Proof step 13:

  # st.keys ≠ 0, st.keys ≠ ∅, st.keys.min ≠ st.min, a ≠ st.keys.min, st.keys.min ∈ st.keys, ¬ a < st.keys.min ⊦

Rule argument

Additional information

Used simplifier rules: ⊦ s.min ∈ s ↔ s ≠ ∅; (ss) Used terms: st.keys.min, st.keys, a

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

A spec-lemma

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

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 14:

  # st.keys ≠ 0, st.keys.min ≠ st.min, a ≠ st.keys.min, st.keys.min < a, st.min < st.keys.min, st.min < a, st.keys.min ∈ st ⊦

Rule argument

Additional information

Used simplifier rules: notempty: ⊦ a ∈ st.keys → st.keys ≠ ∅; Min-min: ⊦ a ∈ st → ¬ a < st.min; inf: ⊦ a ∈ st → a ∈ st.keys; Keys: ⊦ a ∈ st.keys ↔ a ∈ st; transitivity: ⊦ a < b ∧ b < c → a < c; (forward) from specification oelem ⊦ a ≠ b → (a < b ↔ ¬ b < a); (ss)

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

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 15:

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

Rule argument

Additional information

Used simplifier rules: empty: ⊦ ∅.keys = ∅; ⊦ # ∅ = 0; (s) Used terms: st

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

Lemma min-def