Proof step 1 from proof max-q (conclusion) (back to tree)

System applied rule normalize

And obtained the following new goals

• Proof step 2:

  s.max ≠ a, a ∈ s, ∀ b. b ∈ s → ¬ a < b ⊦

Rule argument

Additional information

Proof step 2 from proof max-q (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 3:

  # s ≠ 0, s.max ≠ a, s ≠ ∅, a < s.max, s.min < s.max, a ∈ s, s.min ∈ s, s.max ∈ s, ¬ s.max < s.min, ¬ a < s.min, ∀ b. b ∈ s → ¬ a < b ⊦

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) nll: ⊦ ¬ b < a ∧ b < c → a < c; (forward) from specification oelem size-zero-01: ⊦ s ≠ ∅ → # s ≠ 0; (forward) from specification set-basic ⊦ a ≠ b → (a < b ↔ ¬ b < a); (ss) ne-01: ⊦ a ∈ s → s ≠ ∅; (forward) from specification set-basic

Proof step 3 from proof max-q (previous step) (back to tree)

Heuristic quantifier closing applied rule all left

And closed the goal!

Rule argument

Additional information

Used terms: s.max