Proof step 29 from proof max-ins-max (previous step)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 30:

  a0 < a, ∀ a. max(ins≤(a, x0)) = a ∨ a < max(x0) ⊦ max(ins≤(a, x0)) = a, x0 = [], max(ins≤(a, x0)) < a0, a < (max(x0) < a0 ⊃ a0;max(x0))

Rule argument

Additional information