Proof step 11 from proof reach-reachnext (previous step)

User applied rule structural induction

And obtained the following new goals

• Proof step 12:

  (r ' + x0).last = H[(r ' + []).last].nxt, path(r ' + [], H), path(r ' + x0, H), (r ' + []).last ∈ H ⊦ (r ' + x0).last ≠ null ∧ (r ' + x0).last ∈ H

• Proof step 16:

  (r ' + x0).last = H[(r ' + (r0 + x1)).last].nxt, path(r ' + (r0 + x1), H), path(r ' + x0, H), (r ' + (r0 + x1)).last ∈ H, ∀ r, x0, H. (r ' + x0).last = H[(r ' + x1).last].nxt ∧ path(r ' + x0, H) ∧ path(r ' + x1, H) ∧ (r ' + x1).last ∈ H → (r ' + x0).last ≠ null ∧ (r ' + x0).last ∈ H ⊦ (r ' + x0).last ≠ null ∧ (r ' + x0).last ∈ H

Rule argument

Additional information

Used simplifier rules: reflist freely generated by [], +;;