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

User applied rule case distinction

And obtained the following new goals

• Proof step 7:

  ce.nxt = H[H[(r ' + x).last].nxt].nxt, path(r ' + x, H), reachable(r, H[(r ' + x).last].nxt, H[(r ' + x).last, ce]), (r ' + x).last ∈ H, H[(r ' + x).last].nxt ∈ H ⊦ H[(r ' + x).last].nxt = null, H[(r ' + x).last].nxt = ce.nxt, dups(x), r ∈ x, ∃ 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 ≠ (r ' + x).last ∧ r = H[(r ' + x).last].nxt

• Proof step 50:

  ce.nxt = H[H[(r ' + x).last].nxt].nxt, path(r ' + x, H), (r ' + x).last ∈ H, H[(r ' + x).last].nxt ∈ 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 = null, H[(r ' + x).last].nxt = ce.nxt, dups(x), reachable(r, H[(r ' + x).last].nxt, H[(r ' + x).last, ce]), r ∈ x

Rule argument

Additional information