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

User applied rule case distinction

And obtained the following new goals

• Proof step 9:

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

• Proof step 15:

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

Rule argument

Additional information