Proof step 3 from proof prefixn-eq-prefixn-app (previous step)

Heuristic if-then-else split applied rule case distinction

And obtained the following new goals

• Proof step 4:

  (n0 ≤ # x0 ⊃ firstn(n0, x0);x0) = (n1 ≤ # x0 + # x1 ⊃ firstn(n1, x0 + x1);x0 + x1) ⊦ n1 < # x0 ∧ n0 = n1, # x0 ≤ n0 ∧ # x0 ≤ n1 ∧ x1 = [], # x0 ≤ n0 ∧ n1 = # x0 ∧ x1 ≠ []

• Proof step 11:

  n1 < # x0 ∧ n0 = n1 ∨ # x0 ≤ n0 ∧ # x0 ≤ n1 ∧ x1 = [] ∨ # x0 ≤ n0 ∧ n1 = # x0 ∧ x1 ≠ [] ⊦ (n0 ≤ # x0 ⊃ firstn(n0, x0);x0) = (n1 ≤ # x0 + # x1 ⊃ firstn(n1, x0 + x1);x0 + x1)

Rule argument

Additional information