Proof step 15 from proof min-com (previous step)

Heuristic if-then-else split applied rule case distinction

And obtained the following new goals

• Proof step 16:

  a0 < min(x + a ' + x3), a < min(x3 + a0 ' + x), ∀ x1, x2. #(x1 + x2) < #((a + x3) + (a0 + x)) → true → x1 + x2 = [] ∨ min(x1 + x2) = min(x2 + x1) ⊦ a = a0

• Proof step 30:

  ¬ a0 < min(x + a ' + x3), a < min(x3 + a0 ' + x), ∀ x1, x2. #(x1 + x2) < #((a + x3) + (a0 + x)) → true → x1 + x2 = [] ∨ min(x1 + x2) = min(x2 + x1) ⊦ a = min(x + a ' + x3)

Rule argument

Additional information