Proof step 5 from proof prefixn-split-dropn (previous step)

Heuristic if-then-else split applied rule case distinction

And obtained the following new goals

• Proof step 6:

  n0 + n1 ≤ # x ⊦ firstn(n0 + n1, x) = (n0 ≤ # x ⊃ firstn(n0, x);x) + (n1 ≤ # (n0 ≤ # x ⊃ restn(n0, x);[]) ⊃ firstn(n1, (n0 ≤ # x ⊃ restn(n0, x);[]));(n0 ≤ # x ⊃ restn(n0, x);[]))

• Proof step 14:

  ⊦ x = (n0 ≤ # x ⊃ firstn(n0, x);x) + (n1 ≤ # (n0 ≤ # x ⊃ restn(n0, x);[]) ⊃ firstn(n1, (n0 ≤ # x ⊃ restn(n0, x);[]));(n0 ≤ # x ⊃ restn(n0, x);[])), n0 + n1 ≤ # x

Rule argument

Additional information