Proof step 3 from proof reachable-addnew-rev (previous step)

User applied rule case distinction

And obtained the following new goals

• Proof step 4:

  reachable(r, r1, H[r2, ce]), r ∈ H ⊦ reachable(r, r1, H), r2 ∈ H, ∃ r0. reachable(r, r0, H) ∧ H[r0].nxt = r2 ∧ H[r0].nxt ≠ null ∧ (r1 = H[r0].nxt ∨ reachable(ce.nxt, r1, H))

• Proof step 80:

  r ∈ H, ∃ r0. reachable(r, r0, H) ∧ H[r0].nxt = r2 ∧ H[r0].nxt ≠ null ∧ (r1 = H[r0].nxt ∨ reachable(ce.nxt, r1, H)) ⊦ reachable(r, r1, H), reachable(r, r1, H[r2, ce]), r2 ∈ H

Rule argument

Additional information