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

User applied rule case distinction

And obtained the following new goals

• Proof step 3:

  reachable(r, r1, H[r2, ce]), 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), r2 ∈ H

• Proof step 79:

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

Rule argument

Additional information