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

(r ' + x0).last = H[(r ' + x).last].nxt, path(r ' + x0, H), path(r ' + x, H), (r ' + x).last ∈ H, (r ' + x0).last = null ∨ ¬ (r ' + x0).last ∈ H ⊦

User applied rule structural induction

Proof step 17:
(r ' + x0).last = H[(r ' + []).last].nxt, path(r ' + x0, H), path(r ' + [], H), (r ' + []).last ∈ H, (r ' + x0).last = null ∨ ¬ (r ' + x0).last ∈ H ⊦
Proof step 21:
∀ 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 = H[(r ' + (r0 + x1)).last].nxt, path(r ' + x0, H), path(r ' + (r0 + x1), H), (r ' + (r0 + x1)).last ∈ H, (r ' + x0).last = null ∨ ¬ (r ' + x0).last ∈ H ⊦

indvar: x

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