Proof step 1 from proof maxunion (conclusion) (back to tree)

System applied rule normalize

And obtained the following new goals

• Proof step 2:

  s ≠ ∅, (s ∪ s0).max < s.max ⊦

Rule argument

Additional information

Proof step 2 from proof maxunion (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 3:

  # s ≠ 0, s ≠ ∅, (s ∪ s0).max < s.max, s.min ∈ s, s.max ∈ s, ¬ s.max < s.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; ⊦ ¬ a < a; (s) ne-01: ⊦ a ∈ s → s ≠ ∅; (forward) from specification set-basic size-zero-01: ⊦ s ≠ ∅ → # s ≠ 0; (forward) from specification set-basic

Proof step 3 from proof maxunion (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 4:

  ⊦ a ∈ s → ¬ s.max < a

Rule argument

Additional information

Used simplifier rules: ⊦ a ∈ s1 ∪ s2 ↔ a ∈ s1 ∨ a ∈ s2; (ws) una: ⊦ (s ∪ s0) ∪ s1 = s ∪ s0 ∪ s1; from specification set-union unc: ⊦ s ∪ s0 = s0 ∪ s; from specification set-union Used terms: s.max, s ∪ s0

Proof step 4 from proof maxunion (previous step) (back to tree)

Lemma Max-max