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

Heuristic if-then-else split applied rule case distinction

And obtained the following new goals

• Proof step 58:

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

• Proof step 75:

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

Rule argument

Additional information