Proof step 9 from proof reach-reachnext (previous step)

User applied rule case distinction

And obtained the following new goals

• Proof step 10:

  path(r ' + x, H), (r ' + x).last ∈ H, ∃ x0. path(r ' + x0, H) ∧ (r ' + x0).last = H[(r ' + x).last].nxt ⊦ H[(r ' + x).last].nxt ≠ null ∧ H[(r ' + x).last].nxt ∈ H

• Proof step 20:

  path(r ' + x, H), (r ' + x).last ∈ H, H[(r ' + x).last].nxt ∈ H ⊦ H[(r ' + x).last].nxt = null, ∃ x0. path(r ' + x0, H) ∧ (r ' + x0).last = H[(r ' + x).last].nxt

Rule argument

Additional information