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

Heuristic if-then-else split applied rule case distinction

And obtained the following new goals

• Proof step 27:

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

• Proof step 29:

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

Rule argument

Additional information