Proof step 5 from proof rem-stays-reachable-aux (previous step)

User applied rule case distinction

And obtained the following new goals

• Proof step 6:

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

• Proof step 49:

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

Rule argument

Additional information