Proof step 8 from proof orderedls-all (previous step)

User applied rule case distinction

And obtained the following new goals

• Proof step 9:

  a < a0 ∧ ordered<(a0 ' + y), ordered<(a0 ' + y) ↔ (∀ m, n. m < n ∧ n < 1 + # y → (a0 ' + y)[m] < (a0 ' + y)[n]) ⊦ ∀ m, n. m < n ∧ ¬ 1 + # y < n → (a ' + a0 ' + y)[m] < (a ' + a0 ' + y)[n]

• Proof step 31:

  ∀ m, n. m < n ∧ ¬ 1 + # y < n → (a ' + a0 ' + y)[m] < (a ' + a0 ' + y)[n], ordered<(a0 ' + y) ↔ (∀ m, n. m < n ∧ n < 1 + # y → (a0 ' + y)[m] < (a0 ' + y)[n]) ⊦ a < a0 ∧ ordered<(a0 ' + y)

Rule argument

Additional information