Proof step 2 from proof rem-stays-reachable-aux1 (previous step)

User applied rule case distinction

And obtained the following new goals

• Proof step 3:

  reachable(H[H[r0].nxt].nxt, H[r0].nxt, H) ∧ ¬ reachable(H[H[r0].nxt].nxt, r0, H), r0 ∈ H, H[r0].nxt ∈ H ⊦ ∃ x. path(H[r0].nxt ' + x + H[r0].nxt ', H) ∧ ¬ r0 ∈ x, H[r0].nxt = H[H[r0].nxt].nxt, H[r0].nxt = null

• Proof step 25:

  ∃ x. path(H[r0].nxt ' + x + H[r0].nxt ', H) ∧ ¬ r0 ∈ x, r0 ∈ H, H[r0].nxt ∈ H ⊦ reachable(H[H[r0].nxt].nxt, H[r0].nxt, H) ∧ ¬ reachable(H[H[r0].nxt].nxt, r0, H), H[r0].nxt = H[H[r0].nxt].nxt, H[r0].nxt = null

Rule argument

Additional information