Proof step 3 from proof ll-trav1-end (previous step)

User applied rule case distinction

And obtained the following new goals

• Proof step 4:

  H[r1] = a × null, ∃ x0, x1. x = x0 + x1 ∧ ((lls(r0, r1, x0) * lls(r1, null, x1) * P))(H) ⊦ r1 = null, x ≠ [] ∧ (∃ y. x = y + a ' ∧ ((lls(r0, r1, y) * r1 => a × null * P))(H))

• Proof step 8:

  H[r1] = a × null, ∃ y. x = y + a ' ∧ ((lls(r0, r1, y) * r1 => a × null * P))(H) ⊦ r1 = null, x = [], ∃ x0, x1. x = x0 + x1 ∧ ((lls(r0, r1, x0) * lls(r1, null, x1) * P))(H)

Rule argument

Additional information