Proof step 2 from proof shift-02 (previous step)

Heuristic pl case distinction applied rule case distinction

And obtained the following new goals

• Proof step 3:

  (∀ a. #oc(a, x) + #oc(a, x0) ≤ #oc(a, y)) ∧ (∀ a. #oc(a, y) ≤ #oc(a, x) + #oc(a, x0)) ⊦ (∀ a. #oc(a, x0) + #oc(a, x) ≤ #oc(a, y)) ∧ (∀ a. #oc(a, y) ≤ #oc(a, x0) + #oc(a, x))

• Proof step 7:

  (∀ a. #oc(a, x0) + #oc(a, x) ≤ #oc(a, y)) ∧ (∀ a. #oc(a, y) ≤ #oc(a, x0) + #oc(a, x)) ⊦ (∀ a. #oc(a, x) + #oc(a, x0) ≤ #oc(a, y)) ∧ (∀ a. #oc(a, y) ≤ #oc(a, x) + #oc(a, x0))

Rule argument

Additional information