Proof step 4 from proof reachable-modbehind (previous step)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 5:

  path(r ' + x, H), reachable((r ' + x).last, r1, H), (r ' + x).last ∈ H, r1 ∈ H ⊦ reachable(r1, (r ' + x).last, H), reachable(r, (r ' + x).last, H[r1, ce])

Rule argument

Additional information