Proof step 1 from proof bmin-intempty (conclusion) (back to tree)

System applied rule normalize

And obtained the following new goals

• Proof step 2:

  s ∩ s0 = ∅, s ≠ ∅, s.butmin ∩ s0 ≠ ∅ ⊦

Rule argument

Additional information

Proof step 2 from proof bmin-intempty (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 3:

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

Rule argument

Additional information

Used simplifier rules: Butmin: ⊦ s ≠ ∅ → s.butmin = s -- s.min; min-less: ⊦ a ≠ s.min ∧ a ∈ s → s.min < a; Max-in: ⊦ s ≠ ∅ → s.max ∈ s; Min-in: ⊦ s ≠ ∅ → s.min ∈ s; minmax-04: ⊦ s ≠ ∅ → ¬ s.max < s.min; Min-min: ⊦ a ∈ s → ¬ a < s.min; Max-max: ⊦ a ∈ s → ¬ s.max < a; ⊦ ¬ a < a; (s) leq-trans: ⊦ ¬ b < a ∧ ¬ c < b → ¬ c < a; (forward) from specification weakord[tord] size-zero-01: ⊦ s ≠ ∅ → # s ≠ 0; (forward) from specification set-basic ⊦ a ≠ b → (a < b ↔ ¬ b < a); (ss) size-zero: ⊦ # s ≠ 0 → s ≠ ∅; (forward) from specification set-basic ne-01: ⊦ a ∈ s → s ≠ ∅; (forward) from specification set-basic ⊦ a ∈ s -- a0 ↔ a ≠ a0 ∧ a ∈ s; (ws) int-c: ⊦ s ∩ s0 = s0 ∩ s; from specification set-union int-a: ⊦ (s ∩ s0) ∩ s1 = s ∩ s0 ∩ s1; from specification set-union ⊦ a ∈ s1 ∩ s2 ↔ a ∈ s1 ∧ a ∈ s2; (ws)

Proof step 3 from proof bmin-intempty (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 4:

  ⊦ s1 = s2 ↔ (∀ a. a ∈ s1 ↔ a ∈ s2)

• Proof step 5:

  # s ≠ 0, #((s -- s.min) ∩ s0) ≠ 0, # s0 ≠ 0, ((s -- s.min) ∩ s0).max ≠ s.min, ((s -- s.min) ∩ s0).min ≠ s.min, s ≠ ∅, s0 ≠ ∅, (s -- s.min) ∩ s0 ≠ ∅, s0.max ∈ s0, s0.min ∈ s0, ((s -- s.min) ∩ s0).min ∈ s0, s.max ∈ s, s.min ∈ s, ((s -- s.min) ∩ s0).max ∈ s, ((s -- s.min) ∩ s0).max ∈ s0, ((s -- s.min) ∩ s0).min ∈ s, ¬ ((s -- s.min) ∩ s0).min < s0.min, ¬ s0.max < ((s -- s.min) ∩ s0).min, ¬ s.max < ((s -- s.min) ∩ s0).max, ¬ ((s -- s.min) ∩ s0).max < s0.min, ¬ s0.max < ((s -- s.min) ∩ s0).max, ¬ s.max < ((s -- s.min) ∩ s0).min, ¬ s.max < s0.min, ∀ a. a ∈ s ∩ s0 ↔ a ∈ ∅ ⊦

Rule argument

Additional information

Used terms: s ∩ s0, ∅

Proof step 4 from proof bmin-intempty (previous step) (back to tree)

A spec-lemma

Proof step 5 from proof bmin-intempty (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 6:

  # s ≠ 0, #((s -- s.min) ∩ s0) ≠ 0, # s0 ≠ 0, ((s -- s.min) ∩ s0).max ≠ s.min, ((s -- s.min) ∩ s0).min ≠ s.min, s ≠ ∅, s0 ≠ ∅, (s -- s.min) ∩ s0 ≠ ∅, ((s -- s.min) ∩ s0).min ∈ s, ((s -- s.min) ∩ s0).max ∈ s0, ((s -- s.min) ∩ s0).max ∈ s, s.min ∈ s, s.max ∈ s, ((s -- s.min) ∩ s0).min ∈ s0, s0.min ∈ s0, s0.max ∈ s0, ¬ ((s -- s.min) ∩ s0).min < s0.min, ¬ s0.max < ((s -- s.min) ∩ s0).min, ¬ s.max < ((s -- s.min) ∩ s0).max, ¬ ((s -- s.min) ∩ s0).max < s0.min, ¬ s0.max < ((s -- s.min) ∩ s0).max, ¬ s.max < ((s -- s.min) ∩ s0).min, ¬ s.max < s0.min, ∀ a. ¬ a ∈ s ∩ s0 ⊦

Rule argument

Additional information

Used simplifier rules: ⊦ ¬ a ∈ ∅; (s)

Proof step 6 from proof bmin-intempty (previous step) (back to tree)

User applied rule all left

And closed the goal!

Rule argument

Additional information

Used simplifier rules: ⊦ a ∈ s1 ∩ s2 ↔ a ∈ s1 ∧ a ∈ s2; (ws) int-a: ⊦ (s ∩ s0) ∩ s1 = s ∩ s0 ∩ s1; from specification set-union int-c: ⊦ s ∩ s0 = s0 ∩ s; from specification set-union Used terms: ((s -- s.min) ∩ s0).min