Proof step 9 from proof max-sort-sublist (previous step)

Heuristic if-then-else split applied rule case distinction

And obtained the following new goals

• Proof step 10:

  max(x1 + x0) < a, ∀ x0. x1 + x0 = [] ∨ max(x1 + x0) = max(x1) ∨ max(x1 + x0) = max(x0) ⊦ a = max(x0), (max(x1 + x0) < a ⊃ a;max(x1 + x0)) = max(a ' + x1), x1 + x0 = []

• Proof step 22:

  ¬ max(x1 + x0) < a, ∀ x0. x1 + x0 = [] ∨ max(x1 + x0) = max(x1) ∨ max(x1 + x0) = max(x0) ⊦ max(x1 + x0) = max(x0), (max(x1 + x0) < a ⊃ a;max(x1 + x0)) = max(a ' + x1), x1 + x0 = []

Rule argument

Additional information