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

System applied rule normalize

And obtained the following new goals

• Proof step 2:

  1 < # s, ¬ s.min < (s -- s.min).min ⊦

Rule argument

Additional information

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

User applied rule simplifier

And obtained the following new goals

• Proof step 3:

  # s ≠ 0, # s ≠ 1, s ≠ ∅, s.min ∈ s, s.max ∈ s, ¬ s.max < s.min, ¬ s.min < (s -- s.min).min, ¬ s.max < (s -- s.min).min ⊦

Rule argument

Additional information

Used simplifier rules: Max-in: ⊦ s ≠ ∅ → s.max ∈ s; Min-in: ⊦ s ≠ ∅ → s.min ∈ s; Min-min: ⊦ a ∈ s → ¬ a < s.min; Max-max: ⊦ a ∈ s → ¬ s.max < a; leq-trans: ⊦ ¬ b < a ∧ ¬ c < b → ¬ c < a; (forward) from specification weakord[tord] ⊦ ¬ a < a; (s) size-zero-01: ⊦ s ≠ ∅ → # s ≠ 0; (forward) from specification set-basic size-zero: ⊦ # s ≠ 0 → s ≠ ∅; (forward) from specification set-basic ⊦ 1 < m ↔ ¬(m = 0 ∨ m = 1); (s)

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

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 4:

  ⊦ a ≠ s.min ∧ a ∈ s → s.min < a

• Proof step 5:

  # s ≠ 0, # s ≠ 1, s ≠ ∅, s.max ∈ s, s.min ∈ s, ¬ s.max < s.min, ¬ s.min < (s -- s.min).min, ¬ s.max < (s -- s.min).min ⊦ (s -- s.min).min ≠ s.min ∧ (s -- s.min).min ∈ s

Rule argument

Additional information

Used terms: (s -- s.min).min, s

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

Lemma min-less

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

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 6:

  # s ≠ 0, # s ≠ 1, s ≠ ∅, s.min ∈ s, s.max ∈ s, ¬ s.max < s.min, ¬ s.min < (s -- s.min).min, ¬ s.max < (s -- s.min).min ⊦ (s -- s.min).min ≠ s.min ∧ (s -- s.min).min ∈ s

Rule argument

Additional information

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

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 7:

  ⊦ s ≠ ∅ ∧ s ⊆ s0 → s.min ∈ s0

• Proof step 8:

  # s ≠ 0, # s ≠ 1, s ≠ ∅, s.max ∈ s, s.min ∈ s, ¬ s.max < s.min, ¬ s.min < (s -- s.min).min, ¬ s.max < (s -- s.min).min ⊦ (s -- s.min).min ≠ s.min ∧ (s -- s.min).min ∈ s, s -- s.min ≠ ∅ ∧ s -- s.min ⊆ s

• Proof step 14:

  # s ≠ 0, # s ≠ 1, s -- s.min ≠ ∅, s ≠ ∅, s.max ∈ s, s.min ∈ s, s -- s.min ⊆ s, ¬ s.max < s.min, ¬ s.min < (s -- s.min).min, ¬ s.max < (s -- s.min).min ⊦ (s -- s.min).min ≠ s.min ∧ true

Rule argument

Additional information

Used terms: s, s -- s.min

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

Lemma min-subset

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

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 9:

  s.max = s.min, s = ∅ ++ s.min, # s ≠ 0, # s ≠ 1, s ≠ ∅, s.min ∈ s, ¬ s.min < (s -- s.min).min ⊦ (s -- s.min).min ≠ s.min ∧ (s -- s.min).min ∈ s

Rule argument

Additional information

Used simplifier rules: ⊦ ¬ a < a; (s) leq-trans: ⊦ ¬ b < a ∧ ¬ c < b → ¬ c < a; (forward) from specification weakord[tord] in-06: ⊦ a ∈ s ∧ s = ∅ ++ b → a = b; (forward) from specification set-basic ⊦ s -- a ⊆ s; (s) ⊦ s -- a = ∅ ↔ s = ∅ ∨ s = ∅ ++ a; (ws)

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

User applied rule apply lemma

And obtained the following new goals

• Proof step 10:

  ⊦ ¬ a ∈ s → #(s ++ a) = # s + 1

• Proof step 11:

  s.max = s.min, s = ∅ ++ s.min, # s ≠ 0, # s ≠ 1, s ≠ ∅, s.min ∈ s, ¬ s.min < (s -- s.min).min, ¬ s.min ∈ ∅ → #(∅ ++ s.min) = # ∅ + 1 ⊦ (s -- s.min).min ≠ s.min ∧ (s -- s.min).min ∈ s

Rule argument

Additional information

Used terms: s.min, ∅

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

A spec-lemma

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

User applied rule case distinction

And obtained the following new goals

• Proof step 12:

  #(∅ ++ s.min) = # ∅ + 1, s.max = s.min, s = ∅ ++ s.min, # s ≠ 0, # s ≠ 1, s ≠ ∅, s.min ∈ s, ¬ s.min < (s -- s.min).min ⊦ (s -- s.min).min ≠ s.min ∧ (s -- s.min).min ∈ s

Rule argument

Additional information

Used simplifier rules: ⊦ a ∈ s → s ++ a = s; (s)

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

User applied rule subst equation

And obtained the following new goals

• Proof step 13:

  # s = # ∅ + 1, s.max = s.min, s = ∅ ++ s.min, # s ≠ 0, # s ≠ 1, s ≠ ∅, s.min ∈ s, ¬ s.min < (s -- s.min).min ⊦ (s -- s.min).min ≠ s.min ∧ (s -- s.min).min ∈ s

Rule argument

Additional information

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

Heuristic simplifier applied rule simplifier

And closed the goal!

Rule argument

Additional information

Used simplifier rules: ⊦ # ∅ = 0; (s)

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

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 15:

  (s -- s.min).min = s.min, # s ≠ 1, # s ≠ 0, s ≠ ∅ ++ s.min, s ≠ ∅, s.max ∈ s, s.min ∈ s, ¬ s.max < s.min ⊦

Rule argument

Additional information

Used simplifier rules: ⊦ ¬ a < a; (s) ⊦ s -- a ⊆ s; (s) ⊦ s -- a = ∅ ↔ s = ∅ ∨ s = ∅ ++ a; (ws)

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

User applied rule apply lemma

And obtained the following new goals

• Proof step 16:

  ⊦ s ≠ ∅ → s.min ∈ s

Rule argument

Additional information

Used simplifier rules: ⊦ s -- a = ∅ ↔ s = ∅ ∨ s = ∅ ++ a; (ws) ⊦ a ∈ s -- a0 ↔ a ≠ a0 ∧ a ∈ s; (ws) Used terms: s -- s.min

Proof step 16 from proof min-delmin (previous step) (back to tree)

Lemma Min-in