Proof step 1 from proof rem-stays-reachable-aux2 (conclusion) (back to tree)

System applied rule normalize

And obtained the following new goals

• Proof step 2:

  h[r0].nxt ≠ null, reachable(r, r0, h), h[r0].nxt ∈ h ⊦ (∃ r1. reachable(r, r1, h) ∧ h[r0].nxt = h[r1].nxt ∧ ¬ reachable(r0, r1, h)) ↔ (∃ x. path(r ' + x + h[r0].nxt ', h) ∧ r0 ≠ r ∧ ¬ r0 ∈ x)

Rule argument

Additional information

Proof step 2 from proof rem-stays-reachable-aux2 (previous step) (back to tree)

User applied rule case distinction

And obtained the following new goals

• Proof step 3:

  h[r0].nxt ≠ null, reachable(r, r0, h), h[r0].nxt ∈ h, ∃ r1. reachable(r, r1, h) ∧ h[r0].nxt = h[r1].nxt ∧ ¬ reachable(r0, r1, h) ⊦ ∃ x. path(r ' + x + h[r0].nxt ', h) ∧ r0 ≠ r ∧ ¬ r0 ∈ x

• Proof step 20:

  h[r0].nxt ≠ null, reachable(r, r0, h), h[r0].nxt ∈ h, ∃ x. path(r ' + x + h[r0].nxt ', h) ∧ r0 ≠ r ∧ ¬ r0 ∈ x ⊦ ∃ r1. reachable(r, r1, h) ∧ h[r0].nxt = h[r1].nxt ∧ ¬ reachable(r0, r1, h)

Rule argument

Additional information

Proof step 3 from proof rem-stays-reachable-aux2 (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 4:

  h[r0].nxt = h[r1].nxt, h[r1].nxt ≠ null, reachable(r, r1, h), reachable(r, r0, h), h[r1].nxt ∈ h, ¬ reachable(r0, r1, h) ⊦ ∃ x. path(r ' + x + h[r1].nxt ', h) ∧ ¬ r0 ∈ x

Rule argument

Additional information

Proof step 4 from proof rem-stays-reachable-aux2 (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 5:

  ⊦ reachable(r, r0, h) ↔ (∃ x. path(r ' + x, h) ∧ (r ' + x).last = r0)

• Proof step 6:

  h[r0].nxt = h[r1].nxt, h[r1].nxt ≠ null, reachable(r, r0, h), h[r1].nxt ∈ h, ¬ reachable(r0, r1, h), ∃ x. path(r ' + x, h) ∧ (r ' + x).last = r1 ⊦ ∃ x. path(r ' + x + h[r1].nxt ', h) ∧ ¬ r0 ∈ x

Rule argument

Additional information

Used terms: h, r1, r

Proof step 5 from proof rem-stays-reachable-aux2 (previous step) (back to tree)

Lemma reachable-def

Proof step 6 from proof rem-stays-reachable-aux2 (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 7:

  h[r0].nxt = h[(r ' + x).last].nxt, h[r0].nxt ≠ null, path(r ' + x, h), reachable(r, r0, h), h[r0].nxt ∈ h, ¬ reachable(r0, (r ' + x).last, h) ⊦ ∃ x0. path(r ' + x0 + h[r0].nxt ', h) ∧ ¬ r0 ∈ x0

Rule argument

Additional information

Proof step 7 from proof rem-stays-reachable-aux2 (previous step) (back to tree)

User applied rule exists right

And obtained the following new goals

• Proof step 8:

  h[r0].nxt = h[(r ' + x).last].nxt, h[r0].nxt ≠ null, path(r ' + x, h), reachable(r, r0, h), h[r0].nxt ∈ h, ¬ reachable(r0, (r ' + x).last, h) ⊦ path(r ' + x + h[r0].nxt ', h) ∧ ¬ r0 ∈ x

Rule argument

Additional information

Used terms: x

Proof step 8 from proof rem-stays-reachable-aux2 (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 9:

  ⊦ path(r ' + x + r0 ', h) ↔ path(r ' + x, h) ∧ h[(r ' + x).last].nxt = r0 ∧ r0 ∈ h ∧ r0 ≠ null

• Proof step 10:

  h[r0].nxt = h[(r ' + x).last].nxt, h[r0].nxt ≠ null, path(r ' + x, h), reachable(r, r0, h), h[r0].nxt ∈ h, ¬ reachable(r0, (r ' + x).last, h) ⊦ (path(r ' + x, h) ∧ h[(r ' + x).last].nxt = h[r0].nxt ∧ h[r0].nxt ∈ h ∧ h[r0].nxt ≠ null) ∧ ¬ r0 ∈ x

Rule argument

Additional information

Used terms: h, h[r0].nxt, x, r

Proof step 9 from proof rem-stays-reachable-aux2 (previous step) (back to tree)

Lemma path-split-last

Proof step 10 from proof rem-stays-reachable-aux2 (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 11:

  h[r0].nxt = h[x.last].nxt, h[r0].nxt ≠ null, path(r ' + x, h), reachable(r, r0, h), h[r0].nxt ∈ h, r0 ∈ x, ¬ reachable(r0, x.last, h) ⊦

Rule argument

Additional information

Used simplifier rules: a: ⊦ (x + y) + z = x + y + z; from specification polylist ⊦ a ∈ x → (b ' + x).last = x.last; (s)

Proof step 11 from proof rem-stays-reachable-aux2 (previous step) (back to tree)

User applied rule cut formula

And obtained the following new goals

• Proof step 12:

  h[r0].nxt = h[x.last].nxt, h[r0].nxt ≠ null, path(r ' + x, h), reachable(r, r0, h), r0 ∈ x, h[r0].nxt ∈ h, ¬ reachable(r0, x.last, h) ⊦

Rule argument

Additional information

Used formulas: h[r0].nxt ∈ h

Proof step 12 from proof rem-stays-reachable-aux2 (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 13:

  h[r0].nxt = h[x.last].nxt, h[r0].nxt ≠ null, path(r ' + x, h), reachable(r, r0, h), h[r0].nxt ∈ h, r0 ∈ x, ¬ reachable(r0, x.last, h) ⊦

Rule argument

Additional information

Proof step 13 from proof rem-stays-reachable-aux2 (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 14:

  ⊦ a ∈ x ↔ (∃ y, z. x = y + (a + z))

• Proof step 15:

  h[r0].nxt = h[x.last].nxt, h[r0].nxt ≠ null, path(r ' + x, h), reachable(r, r0, h), h[r0].nxt ∈ h, ¬ reachable(r0, x.last, h), ∃ y, z. x = y + (r0 + z) ⊦

Rule argument

Additional information

Used terms: x, r0

Proof step 14 from proof rem-stays-reachable-aux2 (previous step) (back to tree)

A spec-lemma

Proof step 15 from proof rem-stays-reachable-aux2 (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 16:

  h[r0].nxt = h[(r0 ' + x0).last].nxt, h[r0].nxt ≠ null, path(r ' + y + r0 ' + x0, h), reachable(r, r0, h), h[r0].nxt ∈ h, ¬ reachable(r0, (r0 ' + x0).last, h) ⊦

Rule argument

Additional information

Used simplifier rules: a: ⊦ (x + y) + z = x + y + z; from specification polylist ⊦ (x + a ' + y).last = (a ' + y).last; (s) ⊦ a + x = a ' + x; (s)

Proof step 16 from proof rem-stays-reachable-aux2 (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 17:

  ⊦ reachable(r, r0, h) ↔ (∃ x. path(r ' + x, h) ∧ (r ' + x).last = r0)

• Proof step 18:

  h[r0].nxt = h[(r0 ' + x0).last].nxt, h[r0].nxt ≠ null, path(r ' + y + r0 ' + x0, h), reachable(r, r0, h), h[r0].nxt ∈ h, ∀ x. ¬(path(r0 ' + x, h) ∧ (r0 ' + x).last = (r0 ' + x0).last) ⊦

Rule argument

Additional information

Used terms: h, (r0 ' + x0).last, r0

Proof step 17 from proof rem-stays-reachable-aux2 (previous step) (back to tree)

Lemma reachable-def

Proof step 18 from proof rem-stays-reachable-aux2 (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 19:

  h[r0].nxt = h[(r0 ' + x0).last].nxt, h[r0].nxt ≠ null, path(r ' + y + r0 ' + x0, h), reachable(r, r0, h), h[r0].nxt ∈ h, ∀ x. ¬ path(r0 ' + x, h) ∨ (r0 ' + x).last ≠ (r0 ' + x0).last ⊦

Rule argument

Additional information

Proof step 19 from proof rem-stays-reachable-aux2 (previous step) (back to tree)

Heuristic quantifier closing applied rule all left

And closed the goal!

Rule argument

Additional information

Used simplifier rules: path-postfix: ⊦ path(x + r ' + y, h) → (path(r ' + y, h) ↔ true); a: ⊦ (x + y) + z = x + y + z; from specification polylist Used terms: x0

Proof step 20 from proof rem-stays-reachable-aux2 (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 21:

  h[r0].nxt ≠ null, r0 ≠ r, path(r ' + x + h[r0].nxt ', h), reachable(r, r0, h), h[r0].nxt ∈ h, ¬ r0 ∈ x ⊦ ∃ r1. reachable(r, r1, h) ∧ h[r0].nxt = h[r1].nxt ∧ ¬ reachable(r0, r1, h)

Rule argument

Additional information

Proof step 21 from proof rem-stays-reachable-aux2 (previous step) (back to tree)

User applied rule exists right

And obtained the following new goals

• Proof step 22:

  h[r0].nxt ≠ null, r0 ≠ r, path(r ' + x + h[r0].nxt ', h), reachable(r, r0, h), h[r0].nxt ∈ h, ¬ r0 ∈ x ⊦ reachable(r, (r ' + x).last, h) ∧ h[r0].nxt = h[(r ' + x).last].nxt ∧ ¬ reachable(r0, (r ' + x).last, h)

Rule argument

Additional information

Used terms: (r ' + x).last

Proof step 22 from proof rem-stays-reachable-aux2 (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 23:

  h[r0].nxt ≠ null, r0 ≠ r, path(r ' + x + h[r0].nxt ', h), reachable(r, r0, h), h[r0].nxt ∈ h, ¬ r0 ∈ x ⊦ reachable(r, (r ' + x).last, h) ∧ ¬ reachable(r0, (r ' + x).last, h)

Rule argument

Additional information

Used simplifier rules: path-last-nxt: ⊦ path(r ' + x + r0 ', h) → (h[(r ' + x).last].nxt = r0 ↔ true); a: ⊦ (x + y) + z = x + y + z; from specification polylist

Proof step 23 from proof rem-stays-reachable-aux2 (previous step) (back to tree)

User applied rule cut formula

And obtained the following new goals

• Proof step 24:

  h[r0].nxt ≠ null, r0 ≠ r, path(r ' + x + h[r0].nxt ', h), reachable(r, r0, h), reachable(r, (r ' + x).last, h), h[r0].nxt ∈ h, ¬ r0 ∈ x ⊦ reachable(r, (r ' + x).last, h) ∧ ¬ reachable(r0, (r ' + x).last, h)

• Proof step 212:

  h[r0].nxt ≠ null, r0 ≠ r, path(r ' + x + h[r0].nxt ', h), reachable(r, r0, h), h[r0].nxt ∈ h, ¬ reachable(r, (r ' + x).last, h), ¬ r0 ∈ x ⊦ reachable(r, (r ' + x).last, h) ∧ ¬ reachable(r0, (r ' + x).last, h)

Rule argument

Additional information

Used formulas: reachable(r, (r ' + x).last, h)

Proof step 24 from proof rem-stays-reachable-aux2 (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 25:

  h[r0].nxt ≠ null, r0 ≠ r, path(r ' + x + h[r0].nxt ', h), reachable(r, (r ' + x).last, h), reachable(r, r0, h), reachable(r0, (r ' + x).last, h), h[r0].nxt ∈ h, ¬ r0 ∈ x ⊦

Rule argument

Additional information

Proof step 25 from proof rem-stays-reachable-aux2 (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 26:

  ⊦ reachable(r, r0, h) ↔ (∃ x. path(r ' + x, h) ∧ (r ' + x).last = r0 ∧ ¬ dups(r ' + x))

• Proof step 27:

  h[r0].nxt ≠ null, r0 ≠ r, path(r ' + x + h[r0].nxt ', h), reachable(r, r0, h), reachable(r, (r ' + x).last, h), h[r0].nxt ∈ h, ¬ r0 ∈ x, ∃ x0. path(r0 ' + x0, h) ∧ (r0 ' + x0).last = (r ' + x).last ∧ ¬ dups(r0 ' + x0) ⊦

Rule argument

Additional information

Used terms: h, (r ' + x).last, r0

Proof step 26 from proof rem-stays-reachable-aux2 (previous step) (back to tree)

Lemma reachable-nodups-def

Proof step 27 from proof rem-stays-reachable-aux2 (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 28:

  (r0 ' + x0).last = (r ' + x).last, h[r0].nxt ≠ null, r0 ≠ r, path(r0 ' + x0, h), path(r ' + x + h[r0].nxt ', h), reachable(r, (r ' + x).last, h), reachable(r, r0, h), h[r0].nxt ∈ h, ¬ dups(x0), ¬ r0 ∈ x, ¬ r0 ∈ x0 ⊦

Rule argument

Additional information

Used simplifier rules: a: ⊦ (x + y) + z = x + y + z; from specification polylist ⊦ dups(a ' + x) ↔ a ∈ x ∨ dups(x); (s)

Proof step 28 from proof rem-stays-reachable-aux2 (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 29:

  ⊦ reachable(r, r0, h) ↔ (∃ x. path(r ' + x, h) ∧ (r ' + x).last = r0 ∧ ¬ dups(r ' + x))

• Proof step 30:

  (r0 ' + x0).last = (r ' + x).last, h[r0].nxt ≠ null, r0 ≠ r, path(r ' + x + h[r0].nxt ', h), path(r0 ' + x0, h), reachable(r, r0, h), h[r0].nxt ∈ h, ¬ dups(x0), ¬ r0 ∈ x, ¬ r0 ∈ x0, ∃ x0. path(r ' + x0, h) ∧ (r ' + x0).last = (r ' + x).last ∧ ¬ dups(r ' + x0) ⊦

Rule argument

Additional information

Used terms: h, (r ' + x).last, r

Proof step 29 from proof rem-stays-reachable-aux2 (previous step) (back to tree)

Lemma reachable-nodups-def

Proof step 30 from proof rem-stays-reachable-aux2 (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 31:

  (r ' + x1).last = (r ' + x).last, (r0 ' + x0).last = (r ' + x).last, h[r0].nxt ≠ null, r0 ≠ r, path(r ' + x1, h), path(r0 ' + x0, h), path(r ' + x + h[r0].nxt ', h), reachable(r, r0, h), h[r0].nxt ∈ h, ¬ dups(x0), ¬ dups(x1), ¬ r0 ∈ x, ¬ r0 ∈ x0, ¬ r ∈ x1 ⊦

Rule argument

Additional information

Used simplifier rules: a: ⊦ (x + y) + z = x + y + z; from specification polylist ⊦ dups(a ' + x) ↔ a ∈ x ∨ dups(x); (s)

Proof step 31 from proof rem-stays-reachable-aux2 (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 32:

  ⊦ reachable(r, r0, h) ↔ (∃ x. path(r ' + x, h) ∧ (r ' + x).last = r0 ∧ ¬ dups(r ' + x))

• Proof step 33:

  (r0 ' + x0).last = (r ' + x).last, (r ' + x1).last = (r ' + x).last, h[r0].nxt ≠ null, r0 ≠ r, path(r ' + x + h[r0].nxt ', h), path(r0 ' + x0, h), path(r ' + x1, h), h[r0].nxt ∈ h, ¬ dups(x0), ¬ dups(x1), ¬ r0 ∈ x, ¬ r0 ∈ x0, ¬ r ∈ x1, ∃ x. path(r ' + x, h) ∧ (r ' + x).last = r0 ∧ ¬ dups(r ' + x) ⊦

Rule argument

Additional information

Used terms: h, r0, r

Proof step 32 from proof rem-stays-reachable-aux2 (previous step) (back to tree)

Lemma reachable-nodups-def

Proof step 33 from proof rem-stays-reachable-aux2 (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 34:

  (r ' + x1).last = (r ' + x).last, ((r ' + x2).last ' + x0).last = (r ' + x).last, (r ' + x2).last ≠ r, h[(r ' + x2).last].nxt ≠ null, path(r ' + x2, h), path(r ' + x1, h), path((r ' + x2).last ' + x0, h), path(r ' + x + h[(r ' + x2).last].nxt ', h), h[(r ' + x2).last].nxt ∈ h, ¬ dups(x0), ¬ dups(x1), ¬ dups(x2), ¬ (r ' + x2).last ∈ x, ¬ (r ' + x2).last ∈ x0, ¬ r ∈ x1, ¬ r ∈ x2 ⊦

Rule argument

Additional information

Used simplifier rules: a: ⊦ (x + y) + z = x + y + z; from specification polylist ⊦ dups(a ' + x) ↔ a ∈ x ∨ dups(x); (s)

Proof step 34 from proof rem-stays-reachable-aux2 (previous step) (back to tree)

User applied rule apply lemma

And obtained the following new goals

• Proof step 35:

  path(r ' + x, h), path(r ' + y, h) ⊦ x = y ∨ (∃ r0, y0. x = y + r0 ' + y0) ∨ (∃ r0, x0. y = x + r0 ' + x0)

• Proof step 36:

  ((r ' + x2).last ' + x0).last = (r ' + x).last, (r ' + x1).last = (r ' + x).last, (r ' + x2).last ≠ r, h[(r ' + x2).last].nxt ≠ null, path(r ' + x + h[(r ' + x2).last].nxt ', h), path((r ' + x2).last ' + x0, h), path(r ' + x1, h), path(r ' + x2, h), h[(r ' + x2).last].nxt ∈ h, ¬ dups(x0), ¬ dups(x1), ¬ dups(x2), ¬ (r ' + x2).last ∈ x, ¬ (r ' + x2).last ∈ x0, ¬ r ∈ x1, ¬ r ∈ x2, x2 = x + h[(r ' + x2).last].nxt ' ∨ (∃ r0, y0. x2 = (x + h[(r ' + x2).last].nxt ') + r0 ' + y0) ∨ (∃ r0, x0. x + h[(r ' + x2).last].nxt ' = x2 + r0 ' + x0) ⊦

Rule argument

Additional information

Used terms: r, x2, h, x + h[(r ' + x2).last].nxt '

Proof step 35 from proof rem-stays-reachable-aux2 (previous step) (back to tree)

Lemma linearity-path

Proof step 36 from proof rem-stays-reachable-aux2 (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 37:

  (r ' + x1).last = (r ' + x).last, ((r ' + x2).last ' + x0).last = (r ' + x).last, (r ' + x2).last ≠ r, h[(r ' + x2).last].nxt ≠ null, path(r ' + x2, h), path(r ' + x1, h), path((r ' + x2).last ' + x0, h), path(r ' + x + h[(r ' + x2).last].nxt ', h), h[(r ' + x2).last].nxt ∈ h, ¬ dups(x0), ¬ dups(x1), ¬ dups(x2), ¬ (r ' + x2).last ∈ x, ¬ (r ' + x2).last ∈ x0, ¬ r ∈ x1, ¬ r ∈ x2, x2 = x + h[(r ' + x2).last].nxt ' ∨ x2 = (x + h[(r ' + x2).last].nxt ') + r0 ' + y0 ∨ x + h[(r ' + x2).last].nxt ' = x2 + r1 ' + x3 ⊦

Rule argument

Additional information

Proof step 37 from proof rem-stays-reachable-aux2 (previous step) (back to tree)

User applied rule case distinction

And obtained the following new goals

• Proof step 38:

  ((r ' + x2).last ' + x0).last = (r ' + x).last, (r ' + x1).last = (r ' + x).last, x2 = x + h[(r ' + x2).last].nxt ', (r ' + x2).last ≠ r, h[(r ' + x2).last].nxt ≠ null, path(r ' + x + h[(r ' + x2).last].nxt ', h), path((r ' + x2).last ' + x0, h), path(r ' + x1, h), path(r ' + x2, h), h[(r ' + x2).last].nxt ∈ h, ¬ dups(x0), ¬ dups(x1), ¬ dups(x2), ¬ (r ' + x2).last ∈ x, ¬ (r ' + x2).last ∈ x0, ¬ r ∈ x1, ¬ r ∈ x2 ⊦

• Proof step 64:

  ((r ' + x2).last ' + x0).last = (r ' + x).last, (r ' + x1).last = (r ' + x).last, x2 = (x + h[(r ' + x2).last].nxt ') + r0 ' + y0, (r ' + x2).last ≠ r, h[(r ' + x2).last].nxt ≠ null, path(r ' + x + h[(r ' + x2).last].nxt ', h), path((r ' + x2).last ' + x0, h), path(r ' + x1, h), path(r ' + x2, h), h[(r ' + x2).last].nxt ∈ h, ¬ dups(x0), ¬ dups(x1), ¬ dups(x2), ¬ (r ' + x2).last ∈ x, ¬ (r ' + x2).last ∈ x0, ¬ r ∈ x1, ¬ r ∈ x2 ⊦

• Proof step 200:

  x + h[(r ' + x2).last].nxt ' = x2 + r1 ' + x3, ((r ' + x2).last ' + x0).last = (r ' + x).last, (r ' + x1).last = (r ' + x).last, (r ' + x2).last ≠ r, h[(r ' + x2).last].nxt ≠ null, path(r ' + x + h[(r ' + x2).last].nxt ', h), path((r ' + x2).last ' + x0, h), path(r ' + x1, h), path(r ' + x2, h), h[(r ' + x2).last].nxt ∈ h, ¬ dups(x0), ¬ dups(x1), ¬ dups(x2), ¬ (r ' + x2).last ∈ x, ¬ (r ' + x2).last ∈ x0, ¬ r ∈ x1, ¬ r ∈ x2 ⊦

Rule argument

Additional information

Proof step 38 from proof rem-stays-reachable-aux2 (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 39:

  (r ' + x1).last = (r ' + x).last, (x2.last ' + x0).last = (r ' + x).last, x2 = x + h[x2.last].nxt ', x2.last ≠ r, h[x2.last].nxt ≠ null, path(r ' + x1, h), path(x2.last ' + x0, h), path(r ' + x2, h), h[x2.last].nxt ∈ h, h[x2.last].nxt ∈ x2, ¬ dups(x0), ¬ dups(x1), ¬ dups(x2), ¬ x2.last ∈ x, ¬ x2.last ∈ x0, ¬ r ∈ x1, ¬ r ∈ x2 ⊦

Rule argument

Additional information

Used simplifier rules: a: ⊦ (x + y) + z = x + y + z; from specification polylist ⊦ a ∈ x → (b ' + x).last = x.last; (s) in-15: ⊦ x + a ' = y → a ∈ y; (forward) from specification polylist

Proof step 39 from proof rem-stays-reachable-aux2 (previous step) (back to tree)

User applied rule apply elim lemma

And obtained the following new goals

• Proof step 40:

  (r0 ' + x0).last = (r ' + x).last, (r ' + x1).last = (r ' + x).last, x2 = x + h[r0].nxt ', x2 = y + r0 ', h[r0].nxt ≠ null, r0 ≠ r, x2 ≠ [], path(r ' + x2, h), path(r0 ' + x0, h), path(r ' + x1, h), h[r0].nxt ∈ x2, h[r0].nxt ∈ h, ¬ dups(x0), ¬ dups(x1), ¬ dups(x2), ¬ r0 ∈ x, ¬ r0 ∈ x0, ¬ r ∈ x1, ¬ r ∈ x2 ⊦

Rule argument

Additional information

Used simplifier rules: ⊦ x + y = [] ↔ x = [] ∧ y = []; (as) ⊦ a ' ≠ []; (s) a: ⊦ (x + y) + z = x + y + z; from specification polylist x ≠ [] ⊦ a = x.last ∧ y = x.butlast ↔ x = y + a '; (elim) Used terms: x2, a, y

Proof step 40 from proof rem-stays-reachable-aux2 (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 41:

  (r0 ' + x0).last = (r ' + x).last, (r ' + x1).last = (r ' + x).last, r0 = h[r0].nxt, r0 ≠ r, r0 ≠ null, path(r ' + x + r0 ', h), path(r0 ' + x0, h), path(r ' + x1, h), r0 ∈ h, ¬ dups(x), ¬ dups(x1), ¬ dups(x0), ¬ r ∈ x, ¬ r ∈ x1, ¬ r0 ∈ x0, ¬ r0 ∈ x ⊦

Rule argument

Additional information

Used simplifier rules: a: ⊦ (x + y) + z = x + y + z; from specification polylist ⊦ a ∈ a0 ' ↔ a = a0; (s) ⊦ a ∈ x + y ↔ a ∈ x ∨ a ∈ y; (s) ⊦ dups(x + a ') ↔ a ∈ x ∨ dups(x); (ws) ⊦ x + a ' ≠ []; (s) ⊦ x + a ' = y + a0 ' ↔ x = y ∧ a = a0; (ws)

Proof step 41 from proof rem-stays-reachable-aux2 (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 42:

  ⊦ y ≠ [] → (x + y).last = y.last

• Proof step 43:

  (r ' + x1).last = (r ' + x).last, (r0 ' + x0).last = (r ' + x).last, r0 = h[r0].nxt, x1 = [], r0 ≠ r, r0 ≠ null, path(r ' + x1, h), path(r0 ' + x0, h), path(r ' + x + r0 ', h), r0 ∈ h, ¬ dups(x), ¬ dups(x1), ¬ dups(x0), ¬ r ∈ x, ¬ r ∈ x1, ¬ r0 ∈ x0, ¬ r0 ∈ x ⊦

• Proof step 52:

  x1.last = (r ' + x).last, (r0 ' + x0).last = (r ' + x).last, r0 = h[r0].nxt, r0 ≠ r, r0 ≠ null, x1 ≠ [], path(r ' + x1, h), path(r0 ' + x0, h), path(r ' + x + r0 ', h), r0 ∈ h, ¬ dups(x), ¬ dups(x1), ¬ dups(x0), ¬ r ∈ x, ¬ r ∈ x1, ¬ r0 ∈ x0, ¬ r0 ∈ x ⊦

Rule argument

Additional information

Used terms: x1, r '

Proof step 42 from proof rem-stays-reachable-aux2 (previous step) (back to tree)

A spec-lemma

Proof step 43 from proof rem-stays-reachable-aux2 (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 44:

  (r0 ' + x0).last = ((r0 ' + x0).last ' + x).last, r0 = h[r0].nxt, (r0 ' + x0).last ≠ null, r0 ≠ null, r0 ≠ (r0 ' + x0).last, path(r0 ' + x0, h), path((r0 ' + x0).last ' + x + r0 ', h), (r0 ' + x0).last ∈ h, r0 ∈ h, ¬ dups(x0), ¬ dups(x), ¬ r0 ∈ x, ¬ r0 ∈ x0, ¬ (r0 ' + x0).last ∈ x ⊦

Rule argument

Additional information

Used simplifier rules: path-one: ⊦ path(r ', h) ↔ r ∈ h ∧ r ≠ null; ⊦ ¬ a ∈ []; (s) ⊦ ¬ dups([]); (s) a: ⊦ (x + y) + z = x + y + z; from specification polylist ⊦ x + [] = x; (s) ⊦ a '.last = a; (s)

Proof step 44 from proof rem-stays-reachable-aux2 (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 45:

  ⊦ y ≠ [] → (x + y).last = y.last

• Proof step 46:

  x0.last = (x0.last ' + x).last, r0 = h[r0].nxt, x0.last ≠ null, r0 ≠ null, r0 ≠ x0.last, x0 ≠ [], path(x0.last ' + x + r0 ', h), path(r0 ' + x0, h), r0 ∈ h, x0.last ∈ h, ¬ dups(x0), ¬ dups(x), ¬ r0 ∈ x, ¬ r0 ∈ x0, ¬ x0.last ∈ x ⊦

Rule argument

Additional information

Used simplifier rules: ⊦ x + [] = x; (s) a: ⊦ (x + y) + z = x + y + z; from specification polylist ⊦ a '.last = a; (s) Used terms: r0 ', x0

Proof step 45 from proof rem-stays-reachable-aux2 (previous step) (back to tree)

A spec-lemma

Proof step 46 from proof rem-stays-reachable-aux2 (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 47:

  ⊦ y ≠ [] → (x + y).last = y.last

• Proof step 48:

  x0.last = (x0.last ' + x).last, r0 = h[r0].nxt, x = [], x0.last ≠ null, r0 ≠ null, r0 ≠ x0.last, x0 ≠ [], path(r0 ' + x0, h), path(x0.last ' + x + r0 ', h), x0.last ∈ h, r0 ∈ h, ¬ dups(x0), ¬ dups(x), ¬ r0 ∈ x, ¬ r0 ∈ x0, ¬ x0.last ∈ x ⊦

Rule argument

Additional information

Used simplifier rules: ⊦ x.last = a ∧ x ≠ [] → a ∈ x; (s) Used terms: x0.last ', x

Proof step 47 from proof rem-stays-reachable-aux2 (previous step) (back to tree)

A spec-lemma

Proof step 48 from proof rem-stays-reachable-aux2 (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 49:

  h[x0.last].nxt = h[h[x0.last].nxt].nxt, x0.last ≠ null, h[x0.last].nxt ≠ x0.last, h[x0.last].nxt ≠ null, x0 ≠ [], path(h[x0.last].nxt ' + x0, h), x0.last ∈ h, h[x0.last].nxt ∈ h, ¬ dups(x0), ¬ h[x0.last].nxt ∈ x0 ⊦

Rule argument

Additional information

Used simplifier rules: path-two: ⊦ path(r ' + r0 ', h) ↔ r ∈ h ∧ r0 ∈ h ∧ r ≠ null ∧ r0 ≠ null ∧ h[r].nxt = r0; ⊦ ¬ a ∈ []; (s) ⊦ ¬ dups([]); (s) a: ⊦ (x + y) + z = x + y + z; from specification polylist ⊦ [] + x = x; (s) ⊦ a '.last = a; (s) ⊦ x + [] = x; (s)

Proof step 49 from proof rem-stays-reachable-aux2 (previous step) (back to tree)

User applied rule apply elim lemma

And obtained the following new goals

• Proof step 50:

  h[r].nxt = h[h[r].nxt].nxt, x0 = y + r ', h[r].nxt ≠ r, h[r].nxt ≠ null, r ≠ null, x0 ≠ [], path(h[r].nxt ' + x0, h), h[r].nxt ∈ h, r ∈ h, ¬ dups(x0), ¬ h[r].nxt ∈ x0 ⊦

Rule argument

Additional information

Used simplifier rules: x ≠ [] ⊦ a = x.last ∧ y = x.butlast ↔ x = y + a '; (elim) Used terms: x0, a, y

Proof step 50 from proof rem-stays-reachable-aux2 (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 51:

  h[r].nxt = h[h[r].nxt].nxt, h[r].nxt ≠ r, h[r].nxt ≠ null, r ≠ null, path(h[r].nxt ' + y + r ', h), r ∈ h, h[r].nxt ∈ h, ¬ dups(y), ¬ r ∈ y, ¬ h[r].nxt ∈ y ⊦

Rule argument

Additional information

Used simplifier rules: a: ⊦ (x + y) + z = x + y + z; from specification polylist ⊦ a ∈ a0 ' ↔ a = a0; (s) ⊦ a ∈ x + y ↔ a ∈ x ∨ a ∈ y; (s) ⊦ dups(x + a ') ↔ a ∈ x ∨ dups(x); (ws) ⊦ x + a ' ≠ []; (s)

Proof step 51 from proof rem-stays-reachable-aux2 (previous step) (back to tree)

User applied rule constructor cut

And closed the goal!

Rule argument

Additional information

Used simplifier rules: path-two: ⊦ path(r ' + r0 ', h) ↔ r ∈ h ∧ r0 ∈ h ∧ r ≠ null ∧ r0 ≠ null ∧ h[r].nxt = r0; path-cons: ⊦ path(r ' + r0 ' + x, h) ↔ r ∈ h ∧ r ≠ null ∧ h[r].nxt = r0 ∧ path(r0 ' + x, h); list('a) freely generated by [], +;; ⊦ a + x = a ' + x; (s) ⊦ a ∈ a0 ' + x ↔ ¬(a ≠ a0 ∧ ¬ a ∈ x); (ss) a: ⊦ (x + y) + z = x + y + z; from specification polylist ⊦ [] + x = x; (s) ⊦ ¬ dups([]); (s) ⊦ ¬ a ∈ []; (s)

Proof step 52 from proof rem-stays-reachable-aux2 (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 53:

  (r0 ' + x0).last = x1.last, x1.last = (r ' + x).last, r0 = h[r0].nxt, r0 ≠ r, r0 ≠ null, x1 ≠ [], path(r ' + x + r0 ', h), path(r0 ' + x0, h), path(r ' + x1, h), r0 ∈ h, ¬ dups(x), ¬ dups(x1), ¬ dups(x0), ¬ r ∈ x, ¬ r ∈ x1, ¬ r0 ∈ x0, ¬ r0 ∈ x ⊦

Rule argument

Additional information

Proof step 53 from proof rem-stays-reachable-aux2 (previous step) (back to tree)

User applied rule apply elim lemma

And obtained the following new goals

• Proof step 54:

  (r0 ' + x0).last = r1, r0 = h[r0].nxt, r1 = (r ' + x).last, x1 = y + r1 ', r0 ≠ r, r0 ≠ null, x1 ≠ [], path(r ' + x1, h), path(r0 ' + x0, h), path(r ' + x + r0 ', h), r0 ∈ h, ¬ dups(x), ¬ dups(x1), ¬ dups(x0), ¬ r ∈ x, ¬ r ∈ x1, ¬ r0 ∈ x0, ¬ r0 ∈ x ⊦

Rule argument

Additional information

Used simplifier rules: x ≠ [] ⊦ a = x.last ∧ y = x.butlast ↔ x = y + a '; (elim) Used terms: x1, a, y

Proof step 54 from proof rem-stays-reachable-aux2 (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 55:

  (r0 ' + x0).last = (r ' + x).last, r0 = h[r0].nxt, r ≠ (r ' + x).last, r0 ≠ r, r0 ≠ null, path(r ' + x + r0 ', h), path(r0 ' + x0, h), path(r ' + y + (r ' + x).last ', h), r0 ∈ h, ¬ dups(x), ¬ dups(y), ¬ dups(x0), ¬ r0 ∈ x0, ¬ r0 ∈ x, ¬ (r ' + x).last ∈ y, ¬ r ∈ x, ¬ r ∈ y ⊦

Rule argument

Additional information

Used simplifier rules: a: ⊦ (x + y) + z = x + y + z; from specification polylist ⊦ a ∈ a0 ' ↔ a = a0; (s) ⊦ a ∈ x + y ↔ a ∈ x ∨ a ∈ y; (s) ⊦ dups(x + a ') ↔ a ∈ x ∨ dups(x); (ws) ⊦ x + a ' ≠ []; (s)

Proof step 55 from proof rem-stays-reachable-aux2 (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 56:

  ⊦ y ≠ [] → (x + y).last = y.last

• Proof step 57:

  (r0 ' + x0).last = x.last, r0 = h[r0].nxt, r ≠ x.last, r0 ≠ r, r0 ≠ null, x ≠ [], path(r ' + y + x.last ', h), path(r0 ' + x0, h), path(r ' + x + r0 ', h), r0 ∈ h, ¬ dups(x), ¬ dups(y), ¬ dups(x0), ¬ r0 ∈ x0, ¬ r0 ∈ x, ¬ x.last ∈ y, ¬ r ∈ x, ¬ r ∈ y ⊦

Rule argument

Additional information

Used simplifier rules: ⊦ x + [] = x; (s) a: ⊦ (x + y) + z = x + y + z; from specification polylist ⊦ a '.last = a; (s) Used terms: r ', x

Proof step 56 from proof rem-stays-reachable-aux2 (previous step) (back to tree)

A spec-lemma

Proof step 57 from proof rem-stays-reachable-aux2 (previous step) (back to tree)

User applied rule apply elim lemma

And obtained the following new goals

• Proof step 58:

  (r0 ' + x0).last = r1, r0 = h[r0].nxt, x = y0 + r1 ', r ≠ r1, r0 ≠ r, r0 ≠ null, x ≠ [], path(r ' + x + r0 ', h), path(r0 ' + x0, h), path(r ' + y + r1 ', h), r0 ∈ h, ¬ dups(x), ¬ dups(y), ¬ dups(x0), ¬ r0 ∈ x0, ¬ r0 ∈ x, ¬ r1 ∈ y, ¬ r ∈ x, ¬ r ∈ y ⊦

Rule argument

Additional information

Used simplifier rules: x ≠ [] ⊦ a = x.last ∧ y = x.butlast ↔ x = y + a '; (elim) Used terms: x, a, y0

Proof step 58 from proof rem-stays-reachable-aux2 (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 59:

  r0 = h[r0].nxt, r ≠ (r0 ' + x0).last, r0 ≠ r, r0 ≠ null, r0 ≠ (r0 ' + x0).last, path(r ' + y + (r0 ' + x0).last ', h), path(r0 ' + x0, h), path(r ' + (y0 + (r0 ' + x0).last ') + r0 ', h), r0 ∈ h, ¬ dups(y0), ¬ dups(y), ¬ dups(x0), ¬ r ∈ y, ¬ (r0 ' + x0).last ∈ y0, ¬ r0 ∈ x0, ¬ r0 ∈ y0, ¬ (r0 ' + x0).last ∈ y, ¬ r ∈ y0 ⊦

Rule argument

Additional information

Used simplifier rules: a: ⊦ (x + y) + z = x + y + z; from specification polylist ⊦ a ∈ a0 ' ↔ a = a0; (s) ⊦ a ∈ x + y ↔ a ∈ x ∨ a ∈ y; (s) ⊦ dups(x + a ') ↔ a ∈ x ∨ dups(x); (ws) ⊦ x + a ' ≠ []; (s)

Proof step 59 from proof rem-stays-reachable-aux2 (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 60:

  ⊦ y ≠ [] → (x + y).last = y.last

• Proof step 61:

  r0 = h[r0].nxt, r ≠ x0.last, r0 ≠ r, r0 ≠ null, r0 ≠ x0.last, x0 ≠ [], path(r ' + (y0 + x0.last ') + r0 ', h), path(r0 ' + x0, h), path(r ' + y + x0.last ', h), r0 ∈ h, ¬ dups(y0), ¬ dups(y), ¬ dups(x0), ¬ r ∈ y, ¬ x0.last ∈ y0, ¬ r0 ∈ x0, ¬ r0 ∈ y0, ¬ x0.last ∈ y, ¬ r ∈ y0 ⊦

Rule argument

Additional information

Used simplifier rules: ⊦ x + [] = x; (s) a: ⊦ (x + y) + z = x + y + z; from specification polylist ⊦ a '.last = a; (s) Used terms: r0 ', x0

Proof step 60 from proof rem-stays-reachable-aux2 (previous step) (back to tree)

A spec-lemma

Proof step 61 from proof rem-stays-reachable-aux2 (previous step) (back to tree)

User applied rule apply elim lemma

And obtained the following new goals

• Proof step 62:

  r0 = h[r0].nxt, x0 = y1 + r1 ', r ≠ r1, r0 ≠ r, r0 ≠ null, r0 ≠ r1, x0 ≠ [], path(r ' + y + r1 ', h), path(r0 ' + x0, h), path(r ' + (y0 + r1 ') + r0 ', h), r0 ∈ h, ¬ dups(y0), ¬ dups(y), ¬ dups(x0), ¬ r ∈ y, ¬ r1 ∈ y0, ¬ r0 ∈ x0, ¬ r0 ∈ y0, ¬ r1 ∈ y, ¬ r ∈ y0 ⊦

Rule argument

Additional information

Used simplifier rules: x ≠ [] ⊦ a = x.last ∧ y = x.butlast ↔ x = y + a '; (elim) Used terms: x0, a, y1

Proof step 62 from proof rem-stays-reachable-aux2 (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 63:

  r0 = h[r0].nxt, r ≠ r1, r0 ≠ r, r0 ≠ null, r0 ≠ r1, path(r ' + (y0 + r1 ') + r0 ', h), path(r0 ' + y1 + r1 ', h), path(r ' + y + r1 ', h), r0 ∈ h, ¬ dups(y0), ¬ dups(y), ¬ dups(y1), ¬ r0 ∈ y0, ¬ r1 ∈ y, ¬ r ∈ y0, ¬ r1 ∈ y1, ¬ r ∈ y, ¬ r1 ∈ y0, ¬ r0 ∈ y1 ⊦

Rule argument

Additional information

Used simplifier rules: a: ⊦ (x + y) + z = x + y + z; from specification polylist ⊦ a ∈ a0 ' ↔ a = a0; (s) ⊦ a ∈ x + y ↔ a ∈ x ∨ a ∈ y; (s) ⊦ dups(x + a ') ↔ a ∈ x ∨ dups(x); (ws) ⊦ x + a ' ≠ []; (s)

Proof step 63 from proof rem-stays-reachable-aux2 (previous step) (back to tree)

User applied rule constructor cut

And closed the goal!

Rule argument

Additional information

Used simplifier rules: path-two: ⊦ path(r ' + r0 ', h) ↔ r ∈ h ∧ r0 ∈ h ∧ r ≠ null ∧ r0 ≠ null ∧ h[r].nxt = r0; path-cons: ⊦ path(r ' + r0 ' + x, h) ↔ r ∈ h ∧ r ≠ null ∧ h[r].nxt = r0 ∧ path(r0 ' + x, h); list('a) freely generated by [], +;; ⊦ a + x = a ' + x; (s) ⊦ a ∈ a0 ' + x ↔ ¬(a ≠ a0 ∧ ¬ a ∈ x); (ss) a: ⊦ (x + y) + z = x + y + z; from specification polylist ⊦ [] + x = x; (s)

Proof step 64 from proof rem-stays-reachable-aux2 (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 65:

  ⊦ y ≠ [] → (x + y).last = y.last

• Proof step 66:

  (r ' + x1).last = (r ' + x).last, (x2.last ' + x0).last = (r ' + x).last, x2 = (x + h[x2.last].nxt ') + r0 ' + y0, x2.last ≠ r, h[x2.last].nxt ≠ null, x2 ≠ [], path(r ' + x2, h), path(r ' + x1, h), path(x2.last ' + x0, h), path(r ' + x + h[x2.last].nxt ', h), h[x2.last].nxt ∈ h, ¬ dups(x0), ¬ dups(x1), ¬ dups(x2), ¬ x2.last ∈ x, ¬ x2.last ∈ x0, ¬ r ∈ x1, ¬ r ∈ x2 ⊦

Rule argument

Additional information

Used simplifier rules: ⊦ x + [] = x; (s) ⊦ a '.last = a; (s) ⊦ x + y = [] ↔ x = [] ∧ y = []; (as) ⊦ a ' + x ≠ []; (s) a: ⊦ (x + y) + z = x + y + z; from specification polylist Used terms: x2, r '

Proof step 65 from proof rem-stays-reachable-aux2 (previous step) (back to tree)

A spec-lemma

Proof step 66 from proof rem-stays-reachable-aux2 (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 67:

  (x2.last ' + x0).last = (r ' + x).last, (r ' + x1).last = (r ' + x).last, x2 = (x + h[x2.last].nxt ') + r0 ' + y0, x2.last ≠ r, h[x2.last].nxt ≠ null, x2 ≠ [], path(r ' + x + h[x2.last].nxt ', h), path(x2.last ' + x0, h), path(r ' + x1, h), path(r ' + x2, h), h[x2.last].nxt ∈ h, ¬ dups(x0), ¬ dups(x1), ¬ dups(x2), ¬ x2.last ∈ x, ¬ x2.last ∈ x0, ¬ r ∈ x1, ¬ r ∈ x2 ⊦

Rule argument

Additional information

Proof step 67 from proof rem-stays-reachable-aux2 (previous step) (back to tree)

User applied rule apply lemma

And obtained the following new goals

• Proof step 68:

  path(r ' + x, h), path(r ' + y, h) ⊦ x = y ∨ (∃ r0, y0. x = y + r0 ' + y0) ∨ (∃ r0, x0. y = x + r0 ' + x0)

• Proof step 69:

  (r ' + x1).last = (r ' + x).last, (x2.last ' + x0).last = (r ' + x).last, x2 = (x + h[x2.last].nxt ') + r0 ' + y0, x2.last ≠ r, h[x2.last].nxt ≠ null, x2 ≠ [], path(r ' + x2, h), path(r ' + x1, h), path(x2.last ' + x0, h), path(r ' + x + h[x2.last].nxt ', h), h[x2.last].nxt ∈ h, ¬ dups(x0), ¬ dups(x1), ¬ dups(x2), ¬ x2.last ∈ x, ¬ x2.last ∈ x0, ¬ r ∈ x1, ¬ r ∈ x2, x1 = x2 ∨ (∃ r0, y0. x1 = x2 + r0 ' + y0) ∨ (∃ r0, x0. x2 = x1 + r0 ' + x0) ⊦

Rule argument

Additional information

Used terms: r, x1, h, x2

Proof step 68 from proof rem-stays-reachable-aux2 (previous step) (back to tree)

Lemma linearity-path

Proof step 69 from proof rem-stays-reachable-aux2 (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 70:

  (x2.last ' + x0).last = (r ' + x).last, (r ' + x1).last = (r ' + x).last, x2 = (x + h[x2.last].nxt ') + r0 ' + y0, x2.last ≠ r, h[x2.last].nxt ≠ null, x2 ≠ [], path(r ' + x + h[x2.last].nxt ', h), path(x2.last ' + x0, h), path(r ' + x1, h), path(r ' + x2, h), h[x2.last].nxt ∈ h, ¬ dups(x0), ¬ dups(x1), ¬ dups(x2), ¬ x2.last ∈ x, ¬ x2.last ∈ x0, ¬ r ∈ x1, ¬ r ∈ x2, x1 = x2 ∨ x1 = x2 + r1 ' + y ∨ x2 = x1 + r2 ' + x3 ⊦

Rule argument

Additional information

Proof step 70 from proof rem-stays-reachable-aux2 (previous step) (back to tree)

User applied rule case distinction

And obtained the following new goals

• Proof step 71:

  (r ' + x1).last = (r ' + x).last, (x2.last ' + x0).last = (r ' + x).last, x1 = x2, x2 = (x + h[x2.last].nxt ') + r0 ' + y0, x2.last ≠ r, h[x2.last].nxt ≠ null, x2 ≠ [], path(r ' + x2, h), path(r ' + x1, h), path(x2.last ' + x0, h), path(r ' + x + h[x2.last].nxt ', h), h[x2.last].nxt ∈ h, ¬ dups(x0), ¬ dups(x1), ¬ dups(x2), ¬ x2.last ∈ x, ¬ x2.last ∈ x0, ¬ r ∈ x1, ¬ r ∈ x2 ⊦

• Proof step 76:

  (r ' + x1).last = (r ' + x).last, (x2.last ' + x0).last = (r ' + x).last, x1 = x2 + r1 ' + y, x2 = (x + h[x2.last].nxt ') + r0 ' + y0, x2.last ≠ r, h[x2.last].nxt ≠ null, x2 ≠ [], path(r ' + x2, h), path(r ' + x1, h), path(x2.last ' + x0, h), path(r ' + x + h[x2.last].nxt ', h), h[x2.last].nxt ∈ h, ¬ dups(x0), ¬ dups(x1), ¬ dups(x2), ¬ x2.last ∈ x, ¬ x2.last ∈ x0, ¬ r ∈ x1, ¬ r ∈ x2 ⊦

• Proof step 80:

  (r ' + x1).last = (r ' + x).last, (x2.last ' + x0).last = (r ' + x).last, x2 = (x + h[x2.last].nxt ') + r0 ' + y0, x2 = x1 + r2 ' + x3, x2.last ≠ r, h[x2.last].nxt ≠ null, x2 ≠ [], path(r ' + x2, h), path(r ' + x1, h), path(x2.last ' + x0, h), path(r ' + x + h[x2.last].nxt ', h), h[x2.last].nxt ∈ h, ¬ dups(x0), ¬ dups(x1), ¬ dups(x2), ¬ x2.last ∈ x, ¬ x2.last ∈ x0, ¬ r ∈ x1, ¬ r ∈ x2 ⊦

Rule argument

Additional information

Proof step 71 from proof rem-stays-reachable-aux2 (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 72:

  (x2.last ' + x0).last = x2.last, x2.last = (r ' + x).last, x2 = (x + h[x2.last].nxt ') + r0 ' + y0, x2.last ≠ r, h[x2.last].nxt ≠ null, x2 ≠ [], path(r ' + x + h[x2.last].nxt ', h), path(x2.last ' + x0, h), path(r ' + x2, h), h[x2.last].nxt ∈ h, ¬ dups(x0), ¬ dups(x2), ¬ x2.last ∈ x, ¬ x2.last ∈ x0, ¬ r ∈ x2 ⊦

Rule argument

Additional information

Used simplifier rules: a: ⊦ (x + y) + z = x + y + z; from specification polylist ⊦ x ≠ [] → (a ' + x).last = x.last; (s)

Proof step 72 from proof rem-stays-reachable-aux2 (previous step) (back to tree)

User applied rule apply elim lemma

And obtained the following new goals

• Proof step 73:

  (r1 ' + x0).last = r1, r1 = (r ' + x).last, x2 = (x + h[r1].nxt ') + r0 ' + y0, x2 = y + r1 ', h[r1].nxt ≠ null, r1 ≠ r, x2 ≠ [], path(r ' + x2, h), path(r1 ' + x0, h), path(r ' + x + h[r1].nxt ', h), h[r1].nxt ∈ h, ¬ dups(x0), ¬ dups(x2), ¬ r1 ∈ x, ¬ r1 ∈ x0, ¬ r ∈ x2 ⊦

Rule argument

Additional information

Used simplifier rules: x ≠ [] ⊦ a = x.last ∧ y = x.butlast ↔ x = y + a '; (elim) Used terms: x2, a, y

Proof step 73 from proof rem-stays-reachable-aux2 (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 74:

  y + (r ' + x).last ' = (x + h[(r ' + x).last].nxt ') + r0 ' + y0, ((r ' + x).last ' + x0).last = (r ' + x).last, (r ' + x).last ≠ r, h[(r ' + x).last].nxt ≠ null, path(r ' + x + h[(r ' + x).last].nxt ', h), path((r ' + x).last ' + x0, h), path(r ' + y + (r ' + x).last ', h), h[(r ' + x).last].nxt ∈ h, ¬ dups(x0), ¬ dups(y), ¬ (r ' + x).last ∈ y, ¬ (r ' + x).last ∈ x, ¬ (r ' + x).last ∈ x0, ¬ r ∈ y ⊦

Rule argument

Additional information

Used simplifier rules: a: ⊦ (x + y) + z = x + y + z; from specification polylist ⊦ a ∈ a0 ' ↔ a = a0; (s) ⊦ a ∈ x + y ↔ a ∈ x ∨ a ∈ y; (s) ⊦ dups(x + a ') ↔ a ∈ x ∨ dups(x); (ws) ⊦ x + a ' ≠ []; (s)

Proof step 74 from proof rem-stays-reachable-aux2 (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 75:

  ⊦ y ≠ [] → (x + y).last = y.last

Rule argument

Additional information

Used simplifier rules: ⊦ x.last ∈ x ↔ x ≠ []; (s) ⊦ [] + x = x; (s) ⊦ x + [] = x; (s) a: ⊦ (x + y) + z = x + y + z; from specification polylist ⊦ a '.last = a; (s) Used terms: x, r '

Proof step 75 from proof rem-stays-reachable-aux2 (previous step) (back to tree)

A spec-lemma

Proof step 76 from proof rem-stays-reachable-aux2 (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 77:

  (x2.last ' + x0).last = (r ' + x).last, (r1 ' + y).last = (r ' + x).last, x2 = (x + h[x2.last].nxt ') + r0 ' + y0, x2.last ≠ r, h[x2.last].nxt ≠ null, r ≠ r1, x2 ≠ [], path(r ' + x + h[x2.last].nxt ', h), path(x2.last ' + x0, h), path(r ' + x2 + r1 ' + y, h), path(r ' + x2, h), h[x2.last].nxt ∈ h, ¬ dups(x0), ¬ dups(x2 + y), ¬ dups(x2), ¬ r ∈ x2, ¬ r1 ∈ x2, ¬ r1 ∈ y, ¬ x2.last ∈ x, ¬ x2.last ∈ x0, ¬ r ∈ y ⊦

Rule argument

Additional information

Used simplifier rules: a: ⊦ (x + y) + z = x + y + z; from specification polylist ⊦ a ∈ a0 ' + x ↔ a = a0 ∨ a ∈ x; (s) ⊦ a ∈ x + y ↔ a ∈ x ∨ a ∈ y; (s) ⊦ dups(x + a ' + y) ↔ a ∈ x ∨ a ∈ y ∨ dups(x + y); (ws) ⊦ (x + a ' + y).last = (a ' + y).last; (s) ⊦ y ≠ [] → (x + y + z).last = (y + z).last; (s)

Proof step 77 from proof rem-stays-reachable-aux2 (previous step) (back to tree)

User applied rule apply elim lemma

And obtained the following new goals

• Proof step 78:

  (r1 ' + y).last = (r ' + x).last, (r2 ' + x0).last = (r ' + x).last, x2 = (x + h[r2].nxt ') + r0 ' + y0, x2 = y1 + r2 ', h[r2].nxt ≠ null, r ≠ r1, r2 ≠ r, x2 ≠ [], path(r ' + x2, h), path(r ' + x2 + r1 ' + y, h), path(r2 ' + x0, h), path(r ' + x + h[r2].nxt ', h), h[r2].nxt ∈ h, ¬ dups(x0), ¬ dups(x2 + y), ¬ dups(x2), ¬ r ∈ x2, ¬ r1 ∈ x2, ¬ r1 ∈ y, ¬ r2 ∈ x, ¬ r2 ∈ x0, ¬ r ∈ y ⊦

Rule argument

Additional information

Used simplifier rules: x ≠ [] ⊦ a = x.last ∧ y = x.butlast ↔ x = y + a '; (elim) Used terms: x2, a, y1

Proof step 78 from proof rem-stays-reachable-aux2 (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 79:

  y1 + r2 ' = (x + h[r2].nxt ') + r0 ' + y0, (r2 ' + x0).last = (r ' + x).last, (r1 ' + y).last = (r ' + x).last, h[r2].nxt ≠ null, r ≠ r1, r1 ≠ r2, r2 ≠ r, path(r ' + x + h[r2].nxt ', h), path(r2 ' + x0, h), path(r ' + (y1 + r2 ') + r1 ' + y, h), path(r ' + y1 + r2 ', h), h[r2].nxt ∈ h, ¬ dups(x0), ¬ dups(y1 + y), ¬ dups(y1), ¬ r1 ∈ y, ¬ r2 ∈ x, ¬ r2 ∈ x0, ¬ r ∈ y, ¬ r2 ∈ y1, ¬ r2 ∈ y, ¬ r ∈ y1, ¬ r1 ∈ y1 ⊦

Rule argument

Additional information

Used simplifier rules: a: ⊦ (x + y) + z = x + y + z; from specification polylist ⊦ a ∈ a0 ' ↔ a = a0; (s) ⊦ a ∈ x + y ↔ a ∈ x ∨ a ∈ y; (s) ⊦ ¬ b ∈ x → (dups(x + b ') ↔ dups(x)); (s) ⊦ dups(x + a ' + y) ↔ a ∈ x ∨ a ∈ y ∨ dups(x + y); (ws) ⊦ x + a ' ≠ []; (s)

Proof step 79 from proof rem-stays-reachable-aux2 (previous step) (back to tree)

User applied rule cut formula

And closed the goal!

Rule argument

Additional information

Used simplifier rules: path-cons: ⊦ path(r ' + r0 ' + x, h) ↔ r ∈ h ∧ r ≠ null ∧ h[r].nxt = r0 ∧ path(r0 ' + x, h); path-postfix: ⊦ path(x + r ' + y, h) → (path(r ' + y, h) ↔ true); a: ⊦ (x + y) + z = x + y + z; from specification polylist ⊦ ¬ a0 ∈ y ∧ a0 ≠ a → y + a ' ≠ y0 + a0 ' + z; (s) Used formulas: path(r2 ' + r1 ' + y, h)

Proof step 80 from proof rem-stays-reachable-aux2 (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 81:

  x1 + r2 ' + x3 = x + h[(r2 ' + x3).last].nxt ' + r0 ' + y0, (r ' + x1).last = (r ' + x).last, ((r2 ' + x3).last ' + x0).last = (r ' + x).last, (r2 ' + x3).last ≠ r, h[(r2 ' + x3).last].nxt ≠ null, r ≠ r2, path(r ' + x1, h), path(r ' + x1 + r2 ' + x3, h), path(r ' + x + h[(r2 ' + x3).last].nxt ', h), path((r2 ' + x3).last ' + x0, h), h[(r2 ' + x3).last].nxt ∈ h, ¬ dups(x0), ¬ dups(x1), ¬ dups(x1 + x3), ¬ r2 ∈ x1, ¬ r2 ∈ x3, ¬ (r2 ' + x3).last ∈ x, ¬ (r2 ' + x3).last ∈ x0, ¬ r ∈ x1, ¬ r ∈ x3 ⊦

Rule argument

Additional information

Used simplifier rules: a: ⊦ (x + y) + z = x + y + z; from specification polylist ⊦ a ∈ a0 ' + x ↔ a = a0 ∨ a ∈ x; (s) ⊦ a ∈ x + y ↔ a ∈ x ∨ a ∈ y; (s) ⊦ (x + a ' + y).last = (a ' + y).last; (s) ⊦ dups(x + a ' + y) ↔ a ∈ x ∨ a ∈ y ∨ dups(x + y); (ws) ⊦ x + a ' + y ≠ []; (s)

Proof step 81 from proof rem-stays-reachable-aux2 (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 82:

  ⊦ y ≠ [] → (x + y).last = y.last

• Proof step 83:

  x1 + r2 ' + x3 = x + h[(r2 ' + x3).last].nxt ' + r0 ' + y0, ((r2 ' + x3).last ' + x0).last = (r ' + x).last, (r ' + x1).last = (r ' + x).last, x3 = [], (r2 ' + x3).last ≠ r, h[(r2 ' + x3).last].nxt ≠ null, r ≠ r2, path((r2 ' + x3).last ' + x0, h), path(r ' + x + h[(r2 ' + x3).last].nxt ', h), path(r ' + x1 + r2 ' + x3, h), path(r ' + x1, h), h[(r2 ' + x3).last].nxt ∈ h, ¬ dups(x0), ¬ dups(x1), ¬ dups(x1 + x3), ¬ r2 ∈ x1, ¬ r2 ∈ x3, ¬ (r2 ' + x3).last ∈ x, ¬ (r2 ' + x3).last ∈ x0, ¬ r ∈ x1, ¬ r ∈ x3 ⊦

• Proof step 103:

  x1 + r2 ' + x3 = x + h[x3.last].nxt ' + r0 ' + y0, (x3.last ' + x0).last = (r ' + x).last, (r ' + x1).last = (r ' + x).last, x3.last ≠ r, h[x3.last].nxt ≠ null, r ≠ r2, x3 ≠ [], path(x3.last ' + x0, h), path(r ' + x + h[x3.last].nxt ', h), path(r ' + x1 + r2 ' + x3, h), path(r ' + x1, h), h[x3.last].nxt ∈ h, ¬ dups(x0), ¬ dups(x1), ¬ dups(x1 + x3), ¬ r2 ∈ x1, ¬ r2 ∈ x3, ¬ x3.last ∈ x, ¬ x3.last ∈ x0, ¬ r ∈ x1, ¬ r ∈ x3 ⊦

Rule argument

Additional information

Used terms: x3, r2 '

Proof step 82 from proof rem-stays-reachable-aux2 (previous step) (back to tree)

A spec-lemma

Proof step 83 from proof rem-stays-reachable-aux2 (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 84:

  x1 + r2 ' = x + h[r2].nxt ' + r0 ' + y0, (r ' + x1).last = (r ' + x).last, (r2 ' + x0).last = (r ' + x).last, h[r2].nxt ≠ null, r2 ≠ r, path(r ' + x1, h), path(r ' + x1 + r2 ', h), path(r ' + x + h[r2].nxt ', h), path(r2 ' + x0, h), h[r2].nxt ∈ h, ¬ dups(x0), ¬ dups(x1), ¬ r ∈ x1, ¬ r2 ∈ x1, ¬ r2 ∈ x, ¬ r2 ∈ x0 ⊦

Rule argument

Additional information

Used simplifier rules: ⊦ ¬ a ∈ []; (s) ⊦ a '.last = a; (s) a: ⊦ (x + y) + z = x + y + z; from specification polylist ⊦ x + [] = x; (s)

Proof step 84 from proof rem-stays-reachable-aux2 (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 85:

  ⊦ y ≠ [] → (x + y).last = y.last

• Proof step 86:

  x1 + r2 ' = x + h[r2].nxt ' + r0 ' + y0, (r2 ' + x0).last = (r ' + x).last, (r ' + x1).last = (r ' + x).last, x = [], h[r2].nxt ≠ null, r2 ≠ r, path(r2 ' + x0, h), path(r ' + x + h[r2].nxt ', h), path(r ' + x1 + r2 ', h), path(r ' + x1, h), h[r2].nxt ∈ h, ¬ dups(x0), ¬ dups(x1), ¬ r ∈ x1, ¬ r2 ∈ x1, ¬ r2 ∈ x, ¬ r2 ∈ x0 ⊦

• Proof step 94:

  x1 + r2 ' = x + h[r2].nxt ' + r0 ' + y0, (r2 ' + x0).last = x.last, (r ' + x1).last = x.last, h[r2].nxt ≠ null, r2 ≠ r, x ≠ [], path(r2 ' + x0, h), path(r ' + x + h[r2].nxt ', h), path(r ' + x1 + r2 ', h), path(r ' + x1, h), h[r2].nxt ∈ h, ¬ dups(x0), ¬ dups(x1), ¬ r ∈ x1, ¬ r2 ∈ x1, ¬ r2 ∈ x, ¬ r2 ∈ x0 ⊦

Rule argument

Additional information

Used terms: x, r '

Proof step 85 from proof rem-stays-reachable-aux2 (previous step) (back to tree)

A spec-lemma

Proof step 86 from proof rem-stays-reachable-aux2 (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 87:

  x1 + r2 ' = h[r2].nxt ' + r0 ' + y0, ((r2 ' + x0).last ' + x1).last = (r2 ' + x0).last, h[(r2 ' + x0).last].nxt = h[r2].nxt, (r2 ' + x0).last ≠ null, h[r2].nxt ≠ null, r2 ≠ (r2 ' + x0).last, path((r2 ' + x0).last ' + x1 + r2 ', h), path((r2 ' + x0).last ' + x1, h), path(r2 ' + x0, h), (r2 ' + x0).last ∈ h, h[r2].nxt ∈ h, ¬ dups(x1), ¬ dups(x0), ¬ r2 ∈ x0, ¬ r2 ∈ x1, ¬ (r2 ' + x0).last ∈ x1 ⊦

Rule argument

Additional information

Used simplifier rules: path-two: ⊦ path(r ' + r0 ', h) ↔ r ∈ h ∧ r0 ∈ h ∧ r ≠ null ∧ r0 ≠ null ∧ h[r].nxt = r0; ⊦ ¬ a ∈ []; (s) a: ⊦ (x + y) + z = x + y + z; from specification polylist ⊦ [] + x = x; (s) ⊦ a '.last = a; (s) ⊦ x + [] = x; (s)

Proof step 87 from proof rem-stays-reachable-aux2 (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 88:

  ⊦ y ≠ [] → (x + y).last = y.last

• Proof step 89:

  x1 + r2 ' = h[r2].nxt ' + r0 ' + y0, (x0.last ' + x1).last = x0.last, h[x0.last].nxt = h[r2].nxt, x0.last ≠ null, h[r2].nxt ≠ null, r2 ≠ x0.last, x0 ≠ [], path(r2 ' + x0, h), path(x0.last ' + x1, h), path(x0.last ' + x1 + r2 ', h), h[r2].nxt ∈ h, x0.last ∈ h, ¬ dups(x1), ¬ dups(x0), ¬ r2 ∈ x0, ¬ r2 ∈ x1, ¬ x0.last ∈ x1 ⊦

Rule argument

Additional information

Used simplifier rules: ⊦ x + [] = x; (s) a: ⊦ (x + y) + z = x + y + z; from specification polylist ⊦ a '.last = a; (s) Used terms: x0, r2 '

Proof step 88 from proof rem-stays-reachable-aux2 (previous step) (back to tree)

A spec-lemma

Proof step 89 from proof rem-stays-reachable-aux2 (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 90:

  x1 + r2 ' = h[r2].nxt ' + r0 ' + y0, (x0.last ' + x1).last = x0.last, h[x0.last].nxt = h[r2].nxt, x0.last ≠ null, h[r2].nxt ≠ null, r2 ≠ x0.last, x0 ≠ [], path(x0.last ' + x1 + r2 ', h), path(x0.last ' + x1, h), path(r2 ' + x0, h), x0.last ∈ h, h[r2].nxt ∈ h, ¬ dups(x1), ¬ dups(x0), ¬ r2 ∈ x0, ¬ r2 ∈ x1, ¬ x0.last ∈ x1 ⊦

Rule argument

Additional information

Proof step 90 from proof rem-stays-reachable-aux2 (previous step) (back to tree)

User applied rule apply elim lemma

And obtained the following new goals

• Proof step 91:

  x1 + r2 ' = h[r2].nxt ' + r0 ' + y0, (r ' + x1).last = r, h[r].nxt = h[r2].nxt, x0 = y + r ', h[r2].nxt ≠ null, r ≠ null, r2 ≠ r, x0 ≠ [], path(r2 ' + x0, h), path(r ' + x1, h), path(r ' + x1 + r2 ', h), h[r2].nxt ∈ h, r ∈ h, ¬ dups(x1), ¬ dups(x0), ¬ r2 ∈ x0, ¬ r2 ∈ x1, ¬ r ∈ x1 ⊦

Rule argument

Additional information

Used simplifier rules: x ≠ [] ⊦ a = x.last ∧ y = x.butlast ↔ x = y + a '; (elim) Used terms: x0, a, y

Proof step 91 from proof rem-stays-reachable-aux2 (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 92:

  x1 + r2 ' = h[r2].nxt ' + r0 ' + y0, (r ' + x1).last = r, h[r].nxt = h[r2].nxt, h[r2].nxt ≠ null, r ≠ null, r2 ≠ r, path(r ' + x1 + r2 ', h), path(r ' + x1, h), path(r2 ' + y + r ', h), r ∈ h, h[r2].nxt ∈ h, ¬ dups(x1), ¬ dups(y), ¬ r2 ∈ x1, ¬ r ∈ x1, ¬ r ∈ y, ¬ r2 ∈ y ⊦

Rule argument

Additional information

Used simplifier rules: a: ⊦ (x + y) + z = x + y + z; from specification polylist ⊦ a ∈ a0 ' ↔ a = a0; (s) ⊦ a ∈ x + y ↔ a ∈ x ∨ a ∈ y; (s) ⊦ dups(x + a ') ↔ a ∈ x ∨ dups(x); (ws) ⊦ x + a ' ≠ []; (s)

Proof step 92 from proof rem-stays-reachable-aux2 (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 93:

  ⊦ y ≠ [] → (x + y).last = y.last

Rule argument

Additional information

Used simplifier rules: ⊦ x.last ∈ x ↔ x ≠ []; (s) ⊦ x + [] = x; (s) ⊦ a '.last = a; (s) ⊦ [] + x = x; (s) ⊦ a ' = a0 ' + x ↔ a = a0 ∧ x = []; (ws) ⊦ a ' + x ≠ []; (s) a: ⊦ (x + y) + z = x + y + z; from specification polylist Used terms: x1, r '

Proof step 93 from proof rem-stays-reachable-aux2 (previous step) (back to tree)

A spec-lemma

Proof step 94 from proof rem-stays-reachable-aux2 (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 95:

  x1 + r2 ' = x + h[r2].nxt ' + r0 ' + y0, (r ' + x1).last = x.last, (r2 ' + x0).last = x.last, h[r2].nxt ≠ null, r2 ≠ r, x ≠ [], path(r ' + x1, h), path(r ' + x1 + r2 ', h), path(r ' + x + h[r2].nxt ', h), path(r2 ' + x0, h), h[r2].nxt ∈ h, ¬ dups(x0), ¬ dups(x1), ¬ r ∈ x1, ¬ r2 ∈ x1, ¬ r2 ∈ x, ¬ r2 ∈ x0 ⊦

Rule argument

Additional information

Proof step 95 from proof rem-stays-reachable-aux2 (previous step) (back to tree)

User applied rule apply elim lemma

And obtained the following new goals

• Proof step 96:

  x1 + r2 ' = x + h[r2].nxt ' + r0 ' + y0, (r2 ' + x0).last = r1, (r ' + x1).last = r1, x = y + r1 ', h[r2].nxt ≠ null, r2 ≠ r, x ≠ [], path(r2 ' + x0, h), path(r ' + x + h[r2].nxt ', h), path(r ' + x1 + r2 ', h), path(r ' + x1, h), h[r2].nxt ∈ h, ¬ dups(x0), ¬ dups(x1), ¬ r ∈ x1, ¬ r2 ∈ x1, ¬ r2 ∈ x, ¬ r2 ∈ x0 ⊦

Rule argument

Additional information

Used simplifier rules: x ≠ [] ⊦ a = x.last ∧ y = x.butlast ↔ x = y + a '; (elim) Used terms: x, a, y

Proof step 96 from proof rem-stays-reachable-aux2 (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 97:

  x1 + r2 ' = (y + (r ' + x1).last ') + h[r2].nxt ' + r0 ' + y0, (r2 ' + x0).last = (r ' + x1).last, h[r2].nxt ≠ null, r2 ≠ r, r2 ≠ (r ' + x1).last, path(r ' + x1, h), path(r ' + x1 + r2 ', h), path(r ' + (y + (r ' + x1).last ') + h[r2].nxt ', h), path(r2 ' + x0, h), h[r2].nxt ∈ h, ¬ dups(x0), ¬ dups(x1), ¬ r2 ∈ x0, ¬ r ∈ x1, ¬ r2 ∈ x1, ¬ r2 ∈ y ⊦

Rule argument

Additional information

Used simplifier rules: a: ⊦ (x + y) + z = x + y + z; from specification polylist ⊦ a ∈ a0 ' ↔ a = a0; (s) ⊦ a ∈ x + y ↔ a ∈ x ∨ a ∈ y; (s) ⊦ x + a ' ≠ []; (s)

Proof step 97 from proof rem-stays-reachable-aux2 (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 98:

  ⊦ y ≠ [] → (x + y).last = y.last

• Proof step 99:

  x1 + r2 ' = (y + x1.last ') + h[r2].nxt ' + r0 ' + y0, (r2 ' + x0).last = x1.last, h[r2].nxt ≠ null, r2 ≠ r, r2 ≠ x1.last, x1 ≠ [], path(r2 ' + x0, h), path(r ' + (y + x1.last ') + h[r2].nxt ', h), path(r ' + x1 + r2 ', h), path(r ' + x1, h), h[r2].nxt ∈ h, ¬ dups(x0), ¬ dups(x1), ¬ r2 ∈ x0, ¬ r ∈ x1, ¬ r2 ∈ x1, ¬ r2 ∈ y ⊦

Rule argument

Additional information

Used simplifier rules: ⊦ [] + x = x; (s) ⊦ x + [] = x; (s) ⊦ a '.last = a; (s) ⊦ x + a ' + y = a0 ' ↔ x = [] ∧ a = a0 ∧ y = []; (ws) a: ⊦ (x + y) + z = x + y + z; from specification polylist Used terms: r ', x1

Proof step 98 from proof rem-stays-reachable-aux2 (previous step) (back to tree)

A spec-lemma

Proof step 99 from proof rem-stays-reachable-aux2 (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 100:

  h[r2].nxt ' + r0 ' + y0 = x + r2 ', (r2 ' + x0).last = x1.last, x1 = y + x1.last ' + x, h[r2].nxt ≠ null, r2 ≠ x1.last, r2 ≠ r, x1 ≠ [], path(r2 ' + x0, h), path(r ' + (y + x1.last ') + h[r2].nxt ', h), path(r ' + x1 + r2 ', h), path(r ' + x1, h), h[r2].nxt ∈ h, ¬ dups(x1), ¬ dups(x0), ¬ r2 ∈ y, ¬ r2 ∈ x1, ¬ r ∈ x1, ¬ r2 ∈ x0, h[r2].nxt ∈ x ∨ h[r2].nxt = r2, r2 = h[r2].nxt ∨ r2 = r0 ∨ r2 ∈ y0 ⊦

Rule argument

Additional information

Used simplifier rules: a: ⊦ (x + y) + z = x + y + z; from specification polylist ⊦ x + y = z + y ↔ x = z; (s) ⊦ a ∈ a0 ' ↔ a = a0; (s) ⊦ a ∈ x + y ↔ a ∈ x ∨ a ∈ y; (s) ⊦ a ≠ a0 → (a ∈ a0 ' + x ↔ a ∈ x); (s) ⊦ x + a ' = y + a0 ' ↔ x = y ∧ a = a0; (ws) in-15: ⊦ x + a ' = y → a ∈ y; (forward) from specification polylist inex: ⊦ x + a ' = y + a0 ' + z ∧ a ≠ a0 → (∃ z0. z = z0 + a '); (forward) from specification polylist in-16: ⊦ x + a ' = y + a0 ' + z ∧ a ≠ a0 → a ∈ z; (forward) from specification polylist in-14: ⊦ a ' + x = y → a ∈ y; (forward) from specification polylist ⊦ a ∈ a0 ' + x ↔ a = a0 ∨ a ∈ x; (s)

Proof step 100 from proof rem-stays-reachable-aux2 (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 101:

  ⊦ y ≠ [] → (x + y).last = y.last

• Proof step 102:

  h[r2].nxt ' + r0 ' + y0 = x + r2 ', x0.last = x1.last, x1 = y + x1.last ' + x, h[r2].nxt ≠ null, r2 ≠ x1.last, r2 ≠ r, x0 ≠ [], x1 ≠ [], path(r ' + x1, h), path(r ' + x1 + r2 ', h), path(r ' + (y + x1.last ') + h[r2].nxt ', h), path(r2 ' + x0, h), h[r2].nxt ∈ h, ¬ dups(x1), ¬ dups(x0), ¬ r2 ∈ y, ¬ r2 ∈ x1, ¬ r ∈ x1, ¬ r2 ∈ x0, r2 = h[r2].nxt ∨ r2 = r0 ∨ r2 ∈ y0, h[r2].nxt ∈ x ∨ h[r2].nxt = r2 ⊦

Rule argument

Additional information

Used simplifier rules: ⊦ x + [] = x; (s) a: ⊦ (x + y) + z = x + y + z; from specification polylist ⊦ a '.last = a; (s) Used terms: r2 ', x0

Proof step 101 from proof rem-stays-reachable-aux2 (previous step) (back to tree)

A spec-lemma

Proof step 102 from proof rem-stays-reachable-aux2 (previous step) (back to tree)

User applied rule apply elim lemma

And closed the goal!

Rule argument

Additional information

Used simplifier rules: ⊦ x + a ' ≠ []; (s) ⊦ dups(x + a ') ↔ a ∈ x ∨ dups(x); (ws) ⊦ ¬ a ∈ x → (x + a ' = y + a ' + z ↔ y = x ∧ z = []); (ws) ⊦ a ∈ x + y ↔ a ∈ x ∨ a ∈ y; (s) ⊦ a ∈ a0 ' ↔ a = a0; (s) ⊦ [] + x = x; (s) ⊦ a ' = a0 ' + x ↔ a = a0 ∧ x = []; (ws) ⊦ a ' + x ≠ []; (s) a: ⊦ (x + y) + z = x + y + z; from specification polylist x ≠ [] ⊦ a = x.last ∧ y = x.butlast ↔ x = y + a '; (elim) Used terms: x1, a, y1

Proof step 103 from proof rem-stays-reachable-aux2 (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 104:

  x1 + r2 ' + x3 = x + h[x3.last].nxt ' + r0 ' + y0, (r ' + x1).last = (r ' + x).last, (x3.last ' + x0).last = (r ' + x).last, x3.last ≠ r, h[x3.last].nxt ≠ null, r ≠ r2, x3 ≠ [], path(r ' + x1, h), path(r ' + x1 + r2 ' + x3, h), path(r ' + x + h[x3.last].nxt ', h), path(x3.last ' + x0, h), h[x3.last].nxt ∈ h, ¬ dups(x0), ¬ dups(x1), ¬ dups(x1 + x3), ¬ r2 ∈ x1, ¬ r2 ∈ x3, ¬ x3.last ∈ x, ¬ x3.last ∈ x0, ¬ r ∈ x1, ¬ r ∈ x3 ⊦

Rule argument

Additional information

Proof step 104 from proof rem-stays-reachable-aux2 (previous step) (back to tree)

User applied rule apply elim lemma

And obtained the following new goals

• Proof step 105:

  x1 + r2 ' + x3 = x + h[r1].nxt ' + r0 ' + y0, (r1 ' + x0).last = (r ' + x).last, (r ' + x1).last = (r ' + x).last, x3 = y + r1 ', h[r1].nxt ≠ null, r ≠ r2, r1 ≠ r, x3 ≠ [], path(r1 ' + x0, h), path(r ' + x + h[r1].nxt ', h), path(r ' + x1 + r2 ' + x3, h), path(r ' + x1, h), h[r1].nxt ∈ h, ¬ dups(x0), ¬ dups(x1), ¬ dups(x1 + x3), ¬ r2 ∈ x1, ¬ r2 ∈ x3, ¬ r1 ∈ x, ¬ r1 ∈ x0, ¬ r ∈ x1, ¬ r ∈ x3 ⊦

Rule argument

Additional information

Used simplifier rules: x ≠ [] ⊦ a = x.last ∧ y = x.butlast ↔ x = y + a '; (elim) Used terms: x3, a, y

Proof step 105 from proof rem-stays-reachable-aux2 (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 106:

  x1 + r2 ' + y + r1 ' = x + h[r1].nxt ' + r0 ' + y0, (r ' + x1).last = (r ' + x).last, (r1 ' + x0).last = (r ' + x).last, h[r1].nxt ≠ null, r ≠ r2, r1 ≠ r, r2 ≠ r1, path(r ' + x1, h), path(r ' + x1 + r2 ' + y + r1 ', h), path(r ' + x + h[r1].nxt ', h), path(r1 ' + x0, h), h[r1].nxt ∈ h, ¬ dups(x0), ¬ dups(x1), ¬ dups(x1 + y), ¬ r1 ∈ x1, ¬ r1 ∈ y, ¬ r2 ∈ x1, ¬ r2 ∈ y, ¬ r1 ∈ x, ¬ r1 ∈ x0, ¬ r ∈ x1, ¬ r ∈ y ⊦

Rule argument

Additional information

Used simplifier rules: a: ⊦ (x + y) + z = x + y + z; from specification polylist ⊦ a ∈ a0 ' ↔ a = a0; (s) ⊦ a ∈ x + y ↔ a ∈ x ∨ a ∈ y; (s) ⊦ dups(x + a ') ↔ a ∈ x ∨ dups(x); (ws) ⊦ x + a ' ≠ []; (s)

Proof step 106 from proof rem-stays-reachable-aux2 (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 107:

  y ≠ [] ⊦ x + a ' = y ↔ x = y.butlast ∧ a = y.last

• Proof step 108:

  x1 + r2 ' + y = (x + h[r1].nxt ' + r0 ' + y0).butlast, (r1 ' + x0).last = (r ' + x).last, (r ' + x1).last = (r ' + x).last, r1 = (x + h[r1].nxt ' + r0 ' + y0).last, x + h[r1].nxt ' + r0 ' + y0 ≠ [], h[r1].nxt ≠ null, r ≠ r2, r1 ≠ r, r2 ≠ r1, path(r1 ' + x0, h), path(r ' + x + h[r1].nxt ', h), path(r ' + x1 + r2 ' + y + r1 ', h), path(r ' + x1, h), h[r1].nxt ∈ h, ¬ dups(x0), ¬ dups(x1), ¬ dups(x1 + y), ¬ r1 ∈ x1, ¬ r1 ∈ y, ¬ r2 ∈ x1, ¬ r2 ∈ y, ¬ r1 ∈ x, ¬ r1 ∈ x0, ¬ r ∈ x1, ¬ r ∈ y ⊦

Rule argument

Additional information

Used simplifier rules: ⊦ x + y = [] ↔ x = [] ∧ y = []; (as) ⊦ a ' + x ≠ []; (s) a: ⊦ (x + y) + z = x + y + z; from specification polylist Used terms: x + h[r1].nxt ' + r0 ' + y0, r1, x1 + r2 ' + y

Proof step 107 from proof rem-stays-reachable-aux2 (previous step) (back to tree)

A spec-lemma

Proof step 108 from proof rem-stays-reachable-aux2 (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 109:

  x1 + r2 ' + y = x + h[(r0 ' + y0).last].nxt ' + (r0 ' + y0).butlast, ((r0 ' + y0).last ' + x0).last = (r ' + x).last, (r ' + x1).last = (r ' + x).last, (r0 ' + y0).last ≠ r, h[(r0 ' + y0).last].nxt ≠ null, r ≠ r2, r2 ≠ (r0 ' + y0).last, path((r0 ' + y0).last ' + x0, h), path(r ' + x + h[(r0 ' + y0).last].nxt ', h), path(r ' + x1 + r2 ' + y + (r0 ' + y0).last ', h), path(r ' + x1, h), h[(r0 ' + y0).last].nxt ∈ h, ¬ dups(x1 + y), ¬ dups(x1), ¬ dups(x0), ¬ r ∈ y, ¬ r ∈ x1, ¬ (r0 ' + y0).last ∈ x0, ¬ (r0 ' + y0).last ∈ x, ¬ r2 ∈ y, ¬ r2 ∈ x1, ¬ (r0 ' + y0).last ∈ y, ¬ (r0 ' + y0).last ∈ x1 ⊦

Rule argument

Additional information

Used simplifier rules: a: ⊦ (x + y) + z = x + y + z; from specification polylist ⊦ x + a ' + y ≠ []; (s) ⊦ (a ' + b ' + x).butlast = a ' + (b ' + x).butlast; (s) ⊦ (x + a ' + y).butlast = x + (a ' + y).butlast; (s) ⊦ (b ' + a ' + x).last = (a ' + x).last; (s) ⊦ (x + a ' + y).last = (a ' + y).last; (s)

Proof step 109 from proof rem-stays-reachable-aux2 (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 110:

  ⊦ y ≠ [] → (x + y).butlast = x + y.butlast

• Proof step 111:

  x1 + r2 ' + y = x + h[(r0 ' + y0).last].nxt ' + (r0 ' + y0).butlast, (r ' + x1).last = (r ' + x).last, ((r0 ' + y0).last ' + x0).last = (r ' + x).last, y0 = [], (r0 ' + y0).last ≠ r, h[(r0 ' + y0).last].nxt ≠ null, r ≠ r2, r2 ≠ (r0 ' + y0).last, path(r ' + x1, h), path(r ' + x1 + r2 ' + y + (r0 ' + y0).last ', h), path(r ' + x + h[(r0 ' + y0).last].nxt ', h), path((r0 ' + y0).last ' + x0, h), h[(r0 ' + y0).last].nxt ∈ h, ¬ dups(x1 + y), ¬ dups(x1), ¬ dups(x0), ¬ r ∈ y, ¬ r ∈ x1, ¬ (r0 ' + y0).last ∈ x0, ¬ (r0 ' + y0).last ∈ x, ¬ r2 ∈ y, ¬ r2 ∈ x1, ¬ (r0 ' + y0).last ∈ y, ¬ (r0 ' + y0).last ∈ x1 ⊦

• Proof step 156:

  x1 + r2 ' + y = x + h[(r0 ' + y0).last].nxt ' + r0 ' + y0.butlast, (r ' + x1).last = (r ' + x).last, ((r0 ' + y0).last ' + x0).last = (r ' + x).last, (r0 ' + y0).last ≠ r, h[(r0 ' + y0).last].nxt ≠ null, r ≠ r2, r2 ≠ (r0 ' + y0).last, y0 ≠ [], path(r ' + x1, h), path(r ' + x1 + r2 ' + y + (r0 ' + y0).last ', h), path(r ' + x + h[(r0 ' + y0).last].nxt ', h), path((r0 ' + y0).last ' + x0, h), h[(r0 ' + y0).last].nxt ∈ h, ¬ dups(x1 + y), ¬ dups(x1), ¬ dups(x0), ¬ r ∈ y, ¬ r ∈ x1, ¬ (r0 ' + y0).last ∈ x0, ¬ (r0 ' + y0).last ∈ x, ¬ r2 ∈ y, ¬ r2 ∈ x1, ¬ (r0 ' + y0).last ∈ y, ¬ (r0 ' + y0).last ∈ x1 ⊦

Rule argument

Additional information

Used terms: y0, r0 '

Proof step 110 from proof rem-stays-reachable-aux2 (previous step) (back to tree)

A spec-lemma

Proof step 111 from proof rem-stays-reachable-aux2 (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 112:

  x1 + r2 ' + y = x + h[r0].nxt ', (r0 ' + x0).last = (r ' + x).last, (r ' + x1).last = (r ' + x).last, h[r0].nxt ≠ null, r ≠ r2, r0 ≠ r, r2 ≠ r0, path(r ' + x1, h), path(r0 ' + x0, h), path(r ' + x1 + r2 ' + y, h), path(r ' + x1 + r2 ' + y + r0 ', h), h[r0].nxt ∈ h, ¬ dups(x1 + y), ¬ dups(x1), ¬ dups(x0), ¬ r ∈ y, ¬ r ∈ x1, ¬ r0 ∈ x0, ¬ r0 ∈ x, ¬ r2 ∈ y, ¬ r2 ∈ x1, ¬ r0 ∈ y, ¬ r0 ∈ x1 ⊦

Rule argument

Additional information

Used simplifier rules: ⊦ a '.last = a; (s) a: ⊦ (x + y) + z = x + y + z; from specification polylist ⊦ x + [] = x; (s) ⊦ a '.butlast = []; (s)

Proof step 112 from proof rem-stays-reachable-aux2 (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 113:

  y ≠ [] ⊦ y = x + a ' ↔ x = y.butlast ∧ a = y.last

• Proof step 114:

  (r ' + x1).last = (r ' + x).last, (r0 ' + x0).last = (r ' + x).last, h[r0].nxt = (x1 + r2 ' + y).last, x = (x1 + r2 ' + y).butlast, x1 + r2 ' + y ≠ [], h[r0].nxt ≠ null, r ≠ r2, r0 ≠ r, r2 ≠ r0, path(r ' + x1 + r2 ' + y + r0 ', h), path(r ' + x1 + r2 ' + y, h), path(r0 ' + x0, h), path(r ' + x1, h), h[r0].nxt ∈ h, ¬ dups(x1 + y), ¬ dups(x1), ¬ dups(x0), ¬ r ∈ y, ¬ r ∈ x1, ¬ r0 ∈ x0, ¬ r0 ∈ x, ¬ r2 ∈ y, ¬ r2 ∈ x1, ¬ r0 ∈ y, ¬ r0 ∈ x1 ⊦

Rule argument

Additional information

Used simplifier rules: ⊦ x + y = [] ↔ x = [] ∧ y = []; (as) ⊦ a ' + x ≠ []; (s) a: ⊦ (x + y) + z = x + y + z; from specification polylist Used terms: h[r0].nxt, x, x1 + r2 ' + y

Proof step 113 from proof rem-stays-reachable-aux2 (previous step) (back to tree)

A spec-lemma

Proof step 114 from proof rem-stays-reachable-aux2 (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 115:

  (r0 ' + x0).last = (r ' + x1).last, (r ' + x1).last = (r ' + x1 + (r2 ' + y).butlast).last, h[r0].nxt = (r2 ' + y).last, h[r0].nxt ≠ null, r ≠ r2, r0 ≠ r, r2 ≠ r0, path(r ' + x1, h), path(r0 ' + x0, h), path(r ' + x1 + r2 ' + y, h), path(r ' + x1 + r2 ' + y + r0 ', h), h[r0].nxt ∈ h, ¬ dups(x1 + y), ¬ dups(x1), ¬ dups(x0), ¬ r2 ∈ y, ¬ r2 ∈ x1, ¬ r0 ∈ y, ¬ r0 ∈ x1, ¬ r ∈ y, ¬ r ∈ x1, ¬ r0 ∈ x0, ¬ r0 ∈ (r2 ' + y).butlast ⊦

Rule argument

Additional information

Used simplifier rules: a: ⊦ (x + y) + z = x + y + z; from specification polylist ⊦ a ∈ x + y ↔ a ∈ x ∨ a ∈ y; (s) ⊦ (x + a ' + y).butlast = x + (a ' + y).butlast; (s) ⊦ x + a ' + y ≠ []; (s) ⊦ (x + a ' + y).last = (a ' + y).last; (s)

Proof step 115 from proof rem-stays-reachable-aux2 (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 116:

  ⊦ y ≠ [] → (x + y).butlast = x + y.butlast

• Proof step 117:

  (r ' + x1).last = (r ' + x1 + (r2 ' + y).butlast).last, (r0 ' + x0).last = (r ' + x1).last, h[r0].nxt = (r2 ' + y).last, y = [], h[r0].nxt ≠ null, r ≠ r2, r0 ≠ r, r2 ≠ r0, path(r ' + x1 + r2 ' + y + r0 ', h), path(r ' + x1 + r2 ' + y, h), path(r0 ' + x0, h), path(r ' + x1, h), h[r0].nxt ∈ h, ¬ dups(x1 + y), ¬ dups(x1), ¬ dups(x0), ¬ r2 ∈ y, ¬ r2 ∈ x1, ¬ r0 ∈ y, ¬ r0 ∈ x1, ¬ r ∈ y, ¬ r ∈ x1, ¬ r0 ∈ x0, ¬ r0 ∈ (r2 ' + y).butlast ⊦

• Proof step 143:

  (r ' + x1).last = (r ' + x1 + r2 ' + y.butlast).last, (r0 ' + x0).last = (r ' + x1).last, h[r0].nxt = (r2 ' + y).last, h[r0].nxt ≠ null, r ≠ r2, r0 ≠ r, r2 ≠ r0, y ≠ [], path(r ' + x1 + r2 ' + y + r0 ', h), path(r ' + x1 + r2 ' + y, h), path(r0 ' + x0, h), path(r ' + x1, h), h[r0].nxt ∈ h, ¬ dups(x1 + y), ¬ dups(x1), ¬ dups(x0), ¬ r2 ∈ y, ¬ r2 ∈ x1, ¬ r0 ∈ y, ¬ r0 ∈ x1, ¬ r ∈ y, ¬ r ∈ x1, ¬ r0 ∈ x0, ¬ r0 ∈ r2 ' + y.butlast ⊦

Rule argument

Additional information

Used terms: y, r2 '

Proof step 116 from proof rem-stays-reachable-aux2 (previous step) (back to tree)

A spec-lemma

Proof step 117 from proof rem-stays-reachable-aux2 (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 118:

  (r0 ' + x0).last = (r ' + x1).last, h[r0].nxt ≠ r0, h[r0].nxt ≠ null, r ≠ h[r0].nxt, r0 ≠ r, path(r ' + x1 + h[r0].nxt ' + r0 ', h), path(r ' + x1 + h[r0].nxt ', h), path(r0 ' + x0, h), path(r ' + x1, h), h[r0].nxt ∈ h, ¬ dups(x0), ¬ dups(x1), ¬ r0 ∈ x0, ¬ r ∈ x1, ¬ r0 ∈ x1, ¬ h[r0].nxt ∈ x1 ⊦

Rule argument

Additional information

Used simplifier rules: ⊦ ¬ a ∈ []; (s) ⊦ a '.butlast = []; (s) a: ⊦ (x + y) + z = x + y + z; from specification polylist ⊦ x + [] = x; (s) ⊦ [] + x = x; (s) ⊦ a '.last = a; (s)

Proof step 118 from proof rem-stays-reachable-aux2 (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 119:

  ⊦ path(r ' + x + r0 ', h) ↔ path(r ' + x, h) ∧ h[(r ' + x).last].nxt = r0 ∧ r0 ∈ h ∧ r0 ≠ null

• Proof step 120:

  (r0 ' + x0).last = (r ' + x1).last, h[(r ' + x1 + h[r0].nxt ').last].nxt = r0, h[r0].nxt ≠ r0, h[r0].nxt ≠ null, r ≠ h[r0].nxt, r0 ≠ r, r0 ≠ null, path(r ' + x1, h), path(r0 ' + x0, h), path(r ' + x1 + h[r0].nxt ', h), h[r0].nxt ∈ h, r0 ∈ h, ¬ dups(x0), ¬ dups(x1), ¬ r0 ∈ x0, ¬ r ∈ x1, ¬ r0 ∈ x1, ¬ h[r0].nxt ∈ x1 ⊦

Rule argument

Additional information

Used simplifier rules: a: ⊦ (x + y) + z = x + y + z; from specification polylist Used terms: h, r0, x1 + h[r0].nxt ', r

Proof step 119 from proof rem-stays-reachable-aux2 (previous step) (back to tree)

Lemma path-split-last

Proof step 120 from proof rem-stays-reachable-aux2 (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 121:

  (r0 ' + x0).last = (r ' + x1).last, h[h[r0].nxt].nxt = r0, h[r0].nxt ≠ r0, h[r0].nxt ≠ null, r ≠ h[r0].nxt, r0 ≠ r, r0 ≠ null, path(r ' + x1 + h[r0].nxt ', h), path(r0 ' + x0, h), path(r ' + x1, h), r0 ∈ h, h[r0].nxt ∈ h, ¬ dups(x0), ¬ dups(x1), ¬ r0 ∈ x0, ¬ r ∈ x1, ¬ r0 ∈ x1, ¬ h[r0].nxt ∈ x1 ⊦

Rule argument

Additional information

Used simplifier rules: a: ⊦ (x + y) + z = x + y + z; from specification polylist ⊦ (a ' + x + b ').last = b; (s)

Proof step 121 from proof rem-stays-reachable-aux2 (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 122:

  ⊦ y ≠ [] → (x + y).last = y.last

• Proof step 123:

  (r0 ' + x0).last = (r ' + x1).last, h[h[r0].nxt].nxt = r0, x0 = [], h[r0].nxt ≠ r0, h[r0].nxt ≠ null, r ≠ h[r0].nxt, r0 ≠ r, r0 ≠ null, path(r ' + x1, h), path(r0 ' + x0, h), path(r ' + x1 + h[r0].nxt ', h), h[r0].nxt ∈ h, r0 ∈ h, ¬ dups(x0), ¬ dups(x1), ¬ r0 ∈ x0, ¬ r ∈ x1, ¬ r0 ∈ x1, ¬ h[r0].nxt ∈ x1 ⊦

• Proof step 126:

  x0.last = (r ' + x1).last, h[h[r0].nxt].nxt = r0, h[r0].nxt ≠ r0, h[r0].nxt ≠ null, r ≠ h[r0].nxt, r0 ≠ r, r0 ≠ null, x0 ≠ [], path(r ' + x1, h), path(r0 ' + x0, h), path(r ' + x1 + h[r0].nxt ', h), h[r0].nxt ∈ h, r0 ∈ h, ¬ dups(x0), ¬ dups(x1), ¬ r0 ∈ x0, ¬ r ∈ x1, ¬ r0 ∈ x1, ¬ h[r0].nxt ∈ x1 ⊦

Rule argument

Additional information

Used terms: x0, r0 '

Proof step 122 from proof rem-stays-reachable-aux2 (previous step) (back to tree)

A spec-lemma

Proof step 123 from proof rem-stays-reachable-aux2 (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 124:

  h[h[(r ' + x1).last].nxt].nxt = (r ' + x1).last, (r ' + x1).last ≠ null, (r ' + x1).last ≠ r, h[(r ' + x1).last].nxt ≠ null, h[(r ' + x1).last].nxt ≠ (r ' + x1).last, r ≠ h[(r ' + x1).last].nxt, path(r ' + x1, h), path(r ' + x1 + h[(r ' + x1).last].nxt ', h), h[(r ' + x1).last].nxt ∈ h, (r ' + x1).last ∈ h, ¬ dups(x1), ¬ h[(r ' + x1).last].nxt ∈ x1, ¬ (r ' + x1).last ∈ x1, ¬ r ∈ x1 ⊦

Rule argument

Additional information

Used simplifier rules: path-one: ⊦ path(r ', h) ↔ r ∈ h ∧ r ≠ null; ⊦ ¬ a ∈ []; (s) ⊦ ¬ dups([]); (s) a: ⊦ (x + y) + z = x + y + z; from specification polylist ⊦ x + [] = x; (s) ⊦ a '.last = a; (s)

Proof step 124 from proof rem-stays-reachable-aux2 (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 125:

  ⊦ y ≠ [] → (x + y).last = y.last

Rule argument

Additional information

Used simplifier rules: ⊦ x.last ∈ x ↔ x ≠ []; (s) ⊦ x + [] = x; (s) a: ⊦ (x + y) + z = x + y + z; from specification polylist ⊦ a '.last = a; (s) Used terms: x1, r '

Proof step 125 from proof rem-stays-reachable-aux2 (previous step) (back to tree)

A spec-lemma

Proof step 126 from proof rem-stays-reachable-aux2 (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 127:

  x0.last = (r ' + x1).last, h[h[r0].nxt].nxt = r0, h[r0].nxt ≠ r0, h[r0].nxt ≠ null, r ≠ h[r0].nxt, r0 ≠ r, r0 ≠ null, x0 ≠ [], path(r ' + x1 + h[r0].nxt ', h), path(r0 ' + x0, h), path(r ' + x1, h), r0 ∈ h, h[r0].nxt ∈ h, ¬ dups(x0), ¬ dups(x1), ¬ r0 ∈ x0, ¬ r ∈ x1, ¬ r0 ∈ x1, ¬ h[r0].nxt ∈ x1 ⊦

Rule argument

Additional information

Proof step 127 from proof rem-stays-reachable-aux2 (previous step) (back to tree)

User applied rule apply elim lemma

And obtained the following new goals

• Proof step 128:

  h[h[r0].nxt].nxt = r0, r1 = (r ' + x1).last, x0 = y + r1 ', h[r0].nxt ≠ r0, h[r0].nxt ≠ null, r ≠ h[r0].nxt, r0 ≠ r, r0 ≠ null, x0 ≠ [], path(r ' + x1, h), path(r0 ' + x0, h), path(r ' + x1 + h[r0].nxt ', h), h[r0].nxt ∈ h, r0 ∈ h, ¬ dups(x0), ¬ dups(x1), ¬ r0 ∈ x0, ¬ r ∈ x1, ¬ r0 ∈ x1, ¬ h[r0].nxt ∈ x1 ⊦

Rule argument

Additional information

Used simplifier rules: x ≠ [] ⊦ a = x.last ∧ y = x.butlast ↔ x = y + a '; (elim) Used terms: x0, a, y

Proof step 128 from proof rem-stays-reachable-aux2 (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 129:

  h[h[r0].nxt].nxt = r0, h[r0].nxt ≠ r0, h[r0].nxt ≠ null, r ≠ h[r0].nxt, r0 ≠ r, r0 ≠ null, r0 ≠ (r ' + x1).last, path(r ' + x1 + h[r0].nxt ', h), path(r0 ' + y + (r ' + x1).last ', h), path(r ' + x1, h), r0 ∈ h, h[r0].nxt ∈ h, ¬ dups(y), ¬ dups(x1), ¬ r ∈ x1, ¬ r0 ∈ x1, ¬ h[r0].nxt ∈ x1, ¬ (r ' + x1).last ∈ y, ¬ r0 ∈ y ⊦

Rule argument

Additional information

Used simplifier rules: a: ⊦ (x + y) + z = x + y + z; from specification polylist ⊦ a ∈ a0 ' ↔ a = a0; (s) ⊦ a ∈ x + y ↔ a ∈ x ∨ a ∈ y; (s) ⊦ dups(x + a ') ↔ a ∈ x ∨ dups(x); (ws) ⊦ x + a ' ≠ []; (s)

Proof step 129 from proof rem-stays-reachable-aux2 (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 130:

  ⊦ y ≠ [] → (x + y).last = y.last

• Proof step 131:

  h[h[r0].nxt].nxt = r0, x1 = [], h[r0].nxt ≠ r0, h[r0].nxt ≠ null, r ≠ h[r0].nxt, r0 ≠ r, r0 ≠ null, r0 ≠ (r ' + x1).last, path(r ' + x1, h), path(r0 ' + y + (r ' + x1).last ', h), path(r ' + x1 + h[r0].nxt ', h), h[r0].nxt ∈ h, r0 ∈ h, ¬ dups(y), ¬ dups(x1), ¬ r ∈ x1, ¬ r0 ∈ x1, ¬ h[r0].nxt ∈ x1, ¬ (r ' + x1).last ∈ y, ¬ r0 ∈ y ⊦

• Proof step 135:

  h[h[r0].nxt].nxt = r0, h[r0].nxt ≠ r0, h[r0].nxt ≠ null, r ≠ h[r0].nxt, r0 ≠ r, r0 ≠ null, r0 ≠ x1.last, x1 ≠ [], path(r ' + x1, h), path(r0 ' + y + x1.last ', h), path(r ' + x1 + h[r0].nxt ', h), h[r0].nxt ∈ h, r0 ∈ h, ¬ dups(y), ¬ dups(x1), ¬ r ∈ x1, ¬ r0 ∈ x1, ¬ h[r0].nxt ∈ x1, ¬ x1.last ∈ y, ¬ r0 ∈ y ⊦

Rule argument

Additional information

Used terms: x1, r '

Proof step 130 from proof rem-stays-reachable-aux2 (previous step) (back to tree)

A spec-lemma

Proof step 131 from proof rem-stays-reachable-aux2 (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 132:

  h[h[r0].nxt].nxt = r0, h[r].nxt = h[r0].nxt, h[r0].nxt ≠ r0, h[r0].nxt ≠ null, r ≠ h[r0].nxt, r ≠ null, r0 ≠ null, r0 ≠ r, path(r0 ' + y + r ', h), r0 ∈ h, h[r0].nxt ∈ h, r ∈ h, ¬ dups(y), ¬ r0 ∈ y, ¬ r ∈ y ⊦

Rule argument

Additional information

Used simplifier rules: path-two: ⊦ path(r ' + r0 ', h) ↔ r ∈ h ∧ r0 ∈ h ∧ r ≠ null ∧ r0 ≠ null ∧ h[r].nxt = r0; path-one: ⊦ path(r ', h) ↔ r ∈ h ∧ r ≠ null; ⊦ a '.last = a; (s) a: ⊦ (x + y) + z = x + y + z; from specification polylist ⊦ x + [] = x; (s) ⊦ ¬ a ∈ []; (s) ⊦ ¬ dups([]); (s) ⊦ [] + x = x; (s)

Proof step 132 from proof rem-stays-reachable-aux2 (previous step) (back to tree)

User applied rule constructor cut

And obtained the following new goals

• Proof step 133:

  h[r].nxt = h[r0].nxt, h[h[r0].nxt].nxt = r0, y = r1 + y0, h[r0].nxt ≠ r0, h[r0].nxt ≠ null, r ≠ h[r0].nxt, r ≠ null, r0 ≠ null, r0 ≠ r, path(r0 ' + y + r ', h), r ∈ h, h[r0].nxt ∈ h, r0 ∈ h, ¬ dups(y), ¬ r0 ∈ y, ¬ r ∈ y ⊦

Rule argument

Additional information

Used simplifier rules: path-two: ⊦ path(r ' + r0 ', h) ↔ r ∈ h ∧ r0 ∈ h ∧ r ≠ null ∧ r0 ≠ null ∧ h[r].nxt = r0; list('a) freely generated by [], +;; ⊦ [] + x = x; (s) a: ⊦ (x + y) + z = x + y + z; from specification polylist

Proof step 133 from proof rem-stays-reachable-aux2 (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 134:

  h[r].nxt = h[r0].nxt, h[h[r0].nxt].nxt = r0, h[r0].nxt ≠ null, h[r0].nxt ≠ r0, r ≠ null, r ≠ h[r0].nxt, r0 ≠ r, r0 ≠ null, path(h[r0].nxt ' + y0 + r ', h), r ∈ h, h[r0].nxt ∈ h, r0 ∈ h, ¬ dups(y0), ¬ r ∈ y0, ¬ r0 ∈ y0, ¬ h[r0].nxt ∈ y0 ⊦

Rule argument

Additional information

Used simplifier rules: path-cons: ⊦ path(r ' + r0 ' + x, h) ↔ r ∈ h ∧ r ≠ null ∧ h[r].nxt = r0 ∧ path(r0 ' + x, h); a: ⊦ (x + y) + z = x + y + z; from specification polylist ⊦ a ∈ a0 ' + x ↔ ¬(a ≠ a0 ∧ ¬ a ∈ x); (ss) ⊦ a + x = a ' + x; (s) ⊦ dups(a ' + x) ↔ a ∈ x ∨ dups(x); (s)

Proof step 134 from proof rem-stays-reachable-aux2 (previous step) (back to tree)

User applied rule constructor cut

And closed the goal!

Rule argument

Additional information

Used simplifier rules: path-two: ⊦ path(r ' + r0 ', h) ↔ r ∈ h ∧ r0 ∈ h ∧ r ≠ null ∧ r0 ≠ null ∧ h[r].nxt = r0; path-cons: ⊦ path(r ' + r0 ' + x, h) ↔ r ∈ h ∧ r ≠ null ∧ h[r].nxt = r0 ∧ path(r0 ' + x, h); list('a) freely generated by [], +;; ⊦ a + x = a ' + x; (s) ⊦ a ∈ a0 ' + x ↔ ¬(a ≠ a0 ∧ ¬ a ∈ x); (ss) a: ⊦ (x + y) + z = x + y + z; from specification polylist ⊦ [] + x = x; (s)

Proof step 135 from proof rem-stays-reachable-aux2 (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 136:

  h[h[r0].nxt].nxt = r0, h[r0].nxt ≠ r0, h[r0].nxt ≠ null, r ≠ h[r0].nxt, r0 ≠ r, r0 ≠ null, r0 ≠ x1.last, x1 ≠ [], path(r ' + x1 + h[r0].nxt ', h), path(r0 ' + y + x1.last ', h), path(r ' + x1, h), r0 ∈ h, h[r0].nxt ∈ h, ¬ dups(y), ¬ dups(x1), ¬ r ∈ x1, ¬ r0 ∈ x1, ¬ h[r0].nxt ∈ x1, ¬ x1.last ∈ y, ¬ r0 ∈ y ⊦

Rule argument

Additional information

Proof step 136 from proof rem-stays-reachable-aux2 (previous step) (back to tree)

User applied rule apply elim lemma

And obtained the following new goals

• Proof step 137:

  h[h[r0].nxt].nxt = r0, x1 = y0 + r1 ', h[r0].nxt ≠ r0, h[r0].nxt ≠ null, r ≠ h[r0].nxt, r0 ≠ r, r0 ≠ null, r0 ≠ r1, x1 ≠ [], path(r ' + x1, h), path(r0 ' + y + r1 ', h), path(r ' + x1 + h[r0].nxt ', h), h[r0].nxt ∈ h, r0 ∈ h, ¬ dups(y), ¬ dups(x1), ¬ r ∈ x1, ¬ r0 ∈ x1, ¬ h[r0].nxt ∈ x1, ¬ r1 ∈ y, ¬ r0 ∈ y ⊦

Rule argument

Additional information

Used simplifier rules: x ≠ [] ⊦ a = x.last ∧ y = x.butlast ↔ x = y + a '; (elim) Used terms: x1, a, y0

Proof step 137 from proof rem-stays-reachable-aux2 (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 138:

  h[h[r0].nxt].nxt = r0, h[r0].nxt ≠ r0, h[r0].nxt ≠ null, h[r0].nxt ≠ r1, r ≠ h[r0].nxt, r ≠ r1, r0 ≠ r, r0 ≠ null, r0 ≠ r1, path(r ' + (y0 + r1 ') + h[r0].nxt ', h), path(r0 ' + y + r1 ', h), path(r ' + y0 + r1 ', h), r0 ∈ h, h[r0].nxt ∈ h, ¬ dups(y), ¬ dups(y0), ¬ r1 ∈ y, ¬ r0 ∈ y, ¬ r1 ∈ y0, ¬ r ∈ y0, ¬ r0 ∈ y0, ¬ h[r0].nxt ∈ y0 ⊦

Rule argument

Additional information

Used simplifier rules: a: ⊦ (x + y) + z = x + y + z; from specification polylist ⊦ a ∈ a0 ' ↔ a = a0; (s) ⊦ a ∈ x + y ↔ a ∈ x ∨ a ∈ y; (s) ⊦ dups(x + a ') ↔ a ∈ x ∨ dups(x); (ws) ⊦ x + a ' ≠ []; (s)

Proof step 138 from proof rem-stays-reachable-aux2 (previous step) (back to tree)

User applied rule cut formula

And obtained the following new goals

• Proof step 139:

  h[h[r0].nxt].nxt = r0, h[r0].nxt ≠ r0, h[r0].nxt ≠ null, h[r0].nxt ≠ r1, r ≠ h[r0].nxt, r ≠ r1, r0 ≠ r, r0 ≠ null, r0 ≠ r1, path(r ' + y0 + r1 ', h), path(r0 ' + y + r1 ', h), path(r ' + (y0 + r1 ') + h[r0].nxt ', h), path(r1 ' + h[r0].nxt ', h), h[r0].nxt ∈ h, r0 ∈ h, ¬ dups(y), ¬ dups(y0), ¬ r1 ∈ y, ¬ r0 ∈ y, ¬ r1 ∈ y0, ¬ r ∈ y0, ¬ r0 ∈ y0, ¬ h[r0].nxt ∈ y0 ⊦

Rule argument

Additional information

Used simplifier rules: path-postfix: ⊦ path(x + r ' + y, h) → (path(r ' + y, h) ↔ true); a: ⊦ (x + y) + z = x + y + z; from specification polylist Used formulas: path(r1 ' + h[r0].nxt ', h)

Proof step 139 from proof rem-stays-reachable-aux2 (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 140:

  h[h[r0].nxt].nxt = r0, h[r1].nxt = h[r0].nxt, h[r0].nxt ≠ r0, h[r0].nxt ≠ null, h[r0].nxt ≠ r1, r ≠ h[r0].nxt, r ≠ r1, r0 ≠ r, r0 ≠ null, r0 ≠ r1, r1 ≠ null, path(r ' + (y0 + r1 ') + h[r0].nxt ', h), path(r0 ' + y + r1 ', h), path(r ' + y0 + r1 ', h), r0 ∈ h, h[r0].nxt ∈ h, r1 ∈ h, ¬ dups(y), ¬ dups(y0), ¬ r1 ∈ y, ¬ r0 ∈ y, ¬ r1 ∈ y0, ¬ r ∈ y0, ¬ r0 ∈ y0, ¬ h[r0].nxt ∈ y0 ⊦

Rule argument

Additional information

Used simplifier rules: path-two: ⊦ path(r ' + r0 ', h) ↔ r ∈ h ∧ r0 ∈ h ∧ r ≠ null ∧ r0 ≠ null ∧ h[r].nxt = r0; a: ⊦ (x + y) + z = x + y + z; from specification polylist

Proof step 140 from proof rem-stays-reachable-aux2 (previous step) (back to tree)

User applied rule constructor cut

And obtained the following new goals

• Proof step 141:

  h[r1].nxt = h[r0].nxt, h[h[r0].nxt].nxt = r0, y = r2 + y1, h[r0].nxt ≠ r0, h[r0].nxt ≠ null, h[r0].nxt ≠ r1, r ≠ h[r0].nxt, r ≠ r1, r0 ≠ r, r0 ≠ null, r0 ≠ r1, r1 ≠ null, path(r ' + y0 + r1 ', h), path(r0 ' + y + r1 ', h), path(r ' + (y0 + r1 ') + h[r0].nxt ', h), r1 ∈ h, h[r0].nxt ∈ h, r0 ∈ h, ¬ dups(y), ¬ dups(y0), ¬ r1 ∈ y, ¬ r0 ∈ y, ¬ r1 ∈ y0, ¬ r ∈ y0, ¬ r0 ∈ y0, ¬ h[r0].nxt ∈ y0 ⊦

Rule argument

Additional information

Used simplifier rules: path-two: ⊦ path(r ' + r0 ', h) ↔ r ∈ h ∧ r0 ∈ h ∧ r ≠ null ∧ r0 ≠ null ∧ h[r].nxt = r0; list('a) freely generated by [], +;; ⊦ [] + x = x; (s) a: ⊦ (x + y) + z = x + y + z; from specification polylist

Proof step 141 from proof rem-stays-reachable-aux2 (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 142:

  h[r1].nxt = h[r0].nxt, h[h[r0].nxt].nxt = r0, h[r0].nxt ≠ r1, h[r0].nxt ≠ null, h[r0].nxt ≠ r0, r ≠ r1, r ≠ h[r0].nxt, r0 ≠ r1, r0 ≠ null, r0 ≠ r, r1 ≠ null, path(h[r0].nxt ' + y1 + r1 ', h), path(r ' + (y0 + r1 ') + h[r0].nxt ', h), path(r ' + y0 + r1 ', h), r1 ∈ h, h[r0].nxt ∈ h, r0 ∈ h, ¬ dups(y0), ¬ dups(y1), ¬ r0 ∈ y1, ¬ r1 ∈ y1, ¬ h[r0].nxt ∈ y1, ¬ h[r0].nxt ∈ y0, ¬ r0 ∈ y0, ¬ r ∈ y0, ¬ r1 ∈ y0 ⊦

Rule argument

Additional information

Used simplifier rules: path-cons: ⊦ path(r ' + r0 ' + x, h) ↔ r ∈ h ∧ r ≠ null ∧ h[r].nxt = r0 ∧ path(r0 ' + x, h); a: ⊦ (x + y) + z = x + y + z; from specification polylist ⊦ a ∈ a0 ' + x ↔ ¬(a ≠ a0 ∧ ¬ a ∈ x); (ss) ⊦ a + x = a ' + x; (s) ⊦ dups(a ' + x) ↔ a ∈ x ∨ dups(x); (s)

Proof step 142 from proof rem-stays-reachable-aux2 (previous step) (back to tree)

User applied rule constructor cut

And closed the goal!

Rule argument

Additional information

Used simplifier rules: path-two: ⊦ path(r ' + r0 ', h) ↔ r ∈ h ∧ r0 ∈ h ∧ r ≠ null ∧ r0 ≠ null ∧ h[r].nxt = r0; path-cons: ⊦ path(r ' + r0 ' + x, h) ↔ r ∈ h ∧ r ≠ null ∧ h[r].nxt = r0 ∧ path(r0 ' + x, h); list('a) freely generated by [], +;; ⊦ a + x = a ' + x; (s) ⊦ a ∈ a0 ' + x ↔ ¬(a ≠ a0 ∧ ¬ a ∈ x); (ss) a: ⊦ (x + y) + z = x + y + z; from specification polylist ⊦ [] + x = x; (s)

Proof step 143 from proof rem-stays-reachable-aux2 (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 144:

  (r0 ' + x0).last = (r2 ' + y.butlast).last, (r ' + x1).last = (r2 ' + y.butlast).last, h[r0].nxt = y.last, y.last ≠ null, r ≠ r2, r0 ≠ r, r2 ≠ r0, y ≠ [], path(r ' + x1, h), path(r0 ' + x0, h), path(r ' + x1 + r2 ' + y, h), path(r ' + x1 + r2 ' + y + r0 ', h), y.last ∈ h, ¬ dups(x1 + y), ¬ dups(x1), ¬ dups(x0), ¬ r2 ∈ y, ¬ r2 ∈ x1, ¬ r0 ∈ y, ¬ r0 ∈ x1, ¬ r ∈ y, ¬ r ∈ x1, ¬ r0 ∈ x0, ¬ r0 ∈ y.butlast ⊦

Rule argument

Additional information

Used simplifier rules: a: ⊦ (x + y) + z = x + y + z; from specification polylist ⊦ a ≠ a0 → (a ∈ a0 ' + x ↔ a ∈ x); (s) ⊦ (a ' + x + b ' + y).last = (b ' + y).last; (s) ⊦ x ≠ [] → (a ' + x).last = x.last; (s)

Proof step 144 from proof rem-stays-reachable-aux2 (previous step) (back to tree)

User applied rule apply elim lemma

And obtained the following new goals

• Proof step 145:

  (r ' + x1).last = (r2 ' + y0).last, (r0 ' + x0).last = (r2 ' + y0).last, h[r0].nxt = r1, y = y0 + r1 ', r ≠ r2, r0 ≠ r, r1 ≠ null, r2 ≠ r0, y ≠ [], path(r ' + x1 + r2 ' + y + r0 ', h), path(r ' + x1 + r2 ' + y, h), path(r0 ' + x0, h), path(r ' + x1, h), r1 ∈ h, ¬ dups(x1 + y), ¬ dups(x1), ¬ dups(x0), ¬ r2 ∈ y, ¬ r2 ∈ x1, ¬ r0 ∈ y, ¬ r0 ∈ x1, ¬ r ∈ y, ¬ r ∈ x1, ¬ r0 ∈ x0, ¬ r0 ∈ y0 ⊦

Rule argument

Additional information

Used simplifier rules: x ≠ [] ⊦ a = x.last ∧ y = x.butlast ↔ x = y + a '; (elim) Used terms: y, a, y0

Proof step 145 from proof rem-stays-reachable-aux2 (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 146:

  (r0 ' + x0).last = (r2 ' + y0).last, (r ' + x1).last = (r2 ' + y0).last, h[r0].nxt ≠ null, r ≠ r2, r ≠ h[r0].nxt, r0 ≠ r, r0 ≠ h[r0].nxt, r2 ≠ r0, r2 ≠ h[r0].nxt, path(r ' + x1, h), path(r0 ' + x0, h), path(r ' + x1 + r2 ' + y0 + h[r0].nxt ', h), path(r ' + x1 + r2 ' + (y0 + h[r0].nxt ') + r0 ', h), h[r0].nxt ∈ h, ¬ dups(x1 + y0), ¬ dups(x1), ¬ dups(x0), ¬ r ∈ x1, ¬ r0 ∈ x0, ¬ r0 ∈ y0, ¬ h[r0].nxt ∈ x1, ¬ h[r0].nxt ∈ y0, ¬ r2 ∈ y0, ¬ r2 ∈ x1, ¬ r0 ∈ x1, ¬ r ∈ y0 ⊦

Rule argument

Additional information

Used simplifier rules: a: ⊦ (x + y) + z = x + y + z; from specification polylist ⊦ a ∈ a0 ' ↔ a = a0; (s) ⊦ a ∈ x + y ↔ a ∈ x ∨ a ∈ y; (s) ⊦ dups(x + a ') ↔ a ∈ x ∨ dups(x); (ws) ⊦ x + a ' ≠ []; (s)

Proof step 146 from proof rem-stays-reachable-aux2 (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 147:

  ⊦ y ≠ [] → (x + y).last = y.last

• Proof step 148:

  (r ' + x1).last = (r2 ' + y0).last, (r0 ' + x0).last = (r2 ' + y0).last, y0 = [], h[r0].nxt ≠ null, r ≠ r2, r ≠ h[r0].nxt, r0 ≠ r, r0 ≠ h[r0].nxt, r2 ≠ r0, r2 ≠ h[r0].nxt, path(r ' + x1 + r2 ' + (y0 + h[r0].nxt ') + r0 ', h), path(r ' + x1 + r2 ' + y0 + h[r0].nxt ', h), path(r0 ' + x0, h), path(r ' + x1, h), h[r0].nxt ∈ h, ¬ dups(x1 + y0), ¬ dups(x1), ¬ dups(x0), ¬ r ∈ x1, ¬ r0 ∈ x0, ¬ r0 ∈ y0, ¬ h[r0].nxt ∈ x1, ¬ h[r0].nxt ∈ y0, ¬ r2 ∈ y0, ¬ r2 ∈ x1, ¬ r0 ∈ x1, ¬ r ∈ y0 ⊦

• Proof step 151:

  (r ' + x1).last = y0.last, (r0 ' + x0).last = y0.last, h[r0].nxt ≠ null, r ≠ r2, r ≠ h[r0].nxt, r0 ≠ r, r0 ≠ h[r0].nxt, r2 ≠ r0, r2 ≠ h[r0].nxt, y0 ≠ [], path(r ' + x1 + r2 ' + (y0 + h[r0].nxt ') + r0 ', h), path(r ' + x1 + r2 ' + y0 + h[r0].nxt ', h), path(r0 ' + x0, h), path(r ' + x1, h), h[r0].nxt ∈ h, ¬ dups(x1 + y0), ¬ dups(x1), ¬ dups(x0), ¬ r ∈ x1, ¬ r0 ∈ x0, ¬ r0 ∈ y0, ¬ h[r0].nxt ∈ x1, ¬ h[r0].nxt ∈ y0, ¬ r2 ∈ y0, ¬ r2 ∈ x1, ¬ r0 ∈ x1, ¬ r ∈ y0 ⊦

Rule argument

Additional information

Used terms: y0, r2 '

Proof step 147 from proof rem-stays-reachable-aux2 (previous step) (back to tree)

A spec-lemma

Proof step 148 from proof rem-stays-reachable-aux2 (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 149:

  (r0 ' + x0).last = (r ' + x1).last, (r ' + x1).last ≠ h[r0].nxt, (r ' + x1).last ≠ r0, h[r0].nxt ≠ null, r ≠ h[r0].nxt, r ≠ (r ' + x1).last, r0 ≠ h[r0].nxt, r0 ≠ r, path(r ' + x1 + (r ' + x1).last ' + h[r0].nxt ' + r0 ', h), path(r ' + x1 + (r ' + x1).last ' + h[r0].nxt ', h), path(r0 ' + x0, h), path(r ' + x1, h), h[r0].nxt ∈ h, ¬ dups(x0), ¬ dups(x1), ¬ r0 ∈ x1, ¬ (r ' + x1).last ∈ x1, ¬ h[r0].nxt ∈ x1, ¬ r0 ∈ x0, ¬ r ∈ x1 ⊦

Rule argument

Additional information

Used simplifier rules: ⊦ ¬ a ∈ []; (s) a: ⊦ (x + y) + z = x + y + z; from specification polylist ⊦ x + [] = x; (s) ⊦ [] + x = x; (s) ⊦ a '.last = a; (s)

Proof step 149 from proof rem-stays-reachable-aux2 (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 150:

  ⊦ y ≠ [] → (x + y).last = y.last

Rule argument

Additional information

Used simplifier rules: ⊦ x.last ∈ x ↔ x ≠ []; (s) ⊦ x + [] = x; (s) a: ⊦ (x + y) + z = x + y + z; from specification polylist ⊦ a '.last = a; (s) Used terms: x1, r '

Proof step 150 from proof rem-stays-reachable-aux2 (previous step) (back to tree)

A spec-lemma

Proof step 151 from proof rem-stays-reachable-aux2 (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 152:

  (r0 ' + x0).last = y0.last, (r ' + x1).last = y0.last, h[r0].nxt ≠ null, r ≠ r2, r ≠ h[r0].nxt, r0 ≠ r, r0 ≠ h[r0].nxt, r2 ≠ r0, r2 ≠ h[r0].nxt, y0 ≠ [], path(r ' + x1, h), path(r0 ' + x0, h), path(r ' + x1 + r2 ' + y0 + h[r0].nxt ', h), path(r ' + x1 + r2 ' + (y0 + h[r0].nxt ') + r0 ', h), h[r0].nxt ∈ h, ¬ dups(x1 + y0), ¬ dups(x1), ¬ dups(x0), ¬ r ∈ x1, ¬ r0 ∈ x0, ¬ r0 ∈ y0, ¬ h[r0].nxt ∈ x1, ¬ h[r0].nxt ∈ y0, ¬ r2 ∈ y0, ¬ r2 ∈ x1, ¬ r0 ∈ x1, ¬ r ∈ y0 ⊦

Rule argument

Additional information

Proof step 152 from proof rem-stays-reachable-aux2 (previous step) (back to tree)

User applied rule apply elim lemma

And obtained the following new goals

• Proof step 153:

  (r ' + x1).last = r1, (r0 ' + x0).last = r1, y0 = y + r1 ', h[r0].nxt ≠ null, r ≠ r2, r ≠ h[r0].nxt, r0 ≠ r, r0 ≠ h[r0].nxt, r2 ≠ r0, r2 ≠ h[r0].nxt, y0 ≠ [], path(r ' + x1 + r2 ' + (y0 + h[r0].nxt ') + r0 ', h), path(r ' + x1 + r2 ' + y0 + h[r0].nxt ', h), path(r0 ' + x0, h), path(r ' + x1, h), h[r0].nxt ∈ h, ¬ dups(x1 + y0), ¬ dups(x1), ¬ dups(x0), ¬ r ∈ x1, ¬ r0 ∈ x0, ¬ r0 ∈ y0, ¬ h[r0].nxt ∈ x1, ¬ h[r0].nxt ∈ y0, ¬ r2 ∈ y0, ¬ r2 ∈ x1, ¬ r0 ∈ x1, ¬ r ∈ y0 ⊦

Rule argument

Additional information

Used simplifier rules: x ≠ [] ⊦ a = x.last ∧ y = x.butlast ↔ x = y + a '; (elim) Used terms: y0, a, y

Proof step 153 from proof rem-stays-reachable-aux2 (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 154:

  (r ' + x1).last = (r0 ' + x0).last, h[r0].nxt ≠ null, h[r0].nxt ≠ (r0 ' + x0).last, r ≠ r2, r ≠ h[r0].nxt, r ≠ (r0 ' + x0).last, r0 ≠ r, r0 ≠ h[r0].nxt, r0 ≠ (r0 ' + x0).last, r2 ≠ r0, r2 ≠ h[r0].nxt, r2 ≠ (r0 ' + x0).last, path(r ' + x1, h), path(r0 ' + x0, h), path(r ' + x1 + r2 ' + (y + (r0 ' + x0).last ') + h[r0].nxt ', h), path(r ' + x1 + r2 ' + ((y + (r0 ' + x0).last ') + h[r0].nxt ') + r0 ', h), h[r0].nxt ∈ h, ¬ dups(x1 + y), ¬ dups(x1), ¬ dups(x0), ¬ (r0 ' + x0).last ∈ x1, ¬ (r0 ' + x0).last ∈ y, ¬ r ∈ x1, ¬ r0 ∈ x0, ¬ r0 ∈ y, ¬ h[r0].nxt ∈ x1, ¬ h[r0].nxt ∈ y, ¬ r2 ∈ y, ¬ r2 ∈ x1, ¬ r0 ∈ x1, ¬ r ∈ y ⊦

Rule argument

Additional information

Used simplifier rules: a: ⊦ (x + y) + z = x + y + z; from specification polylist ⊦ a ∈ a0 ' ↔ a = a0; (s) ⊦ a ∈ x + y ↔ a ∈ x ∨ a ∈ y; (s) ⊦ dups(x + a ') ↔ a ∈ x ∨ dups(x); (ws) ⊦ x + a ' ≠ []; (s)

Proof step 154 from proof rem-stays-reachable-aux2 (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 155:

  ⊦ y ≠ [] → (x + y).last = y.last

Rule argument

Additional information

Used simplifier rules: ⊦ x.last = a ∧ x ≠ [] → a ∈ x; (s) ⊦ x + [] = x; (s) a: ⊦ (x + y) + z = x + y + z; from specification polylist ⊦ a '.last = a; (s) Used terms: x1, r '

Proof step 155 from proof rem-stays-reachable-aux2 (previous step) (back to tree)

A spec-lemma

Proof step 156 from proof rem-stays-reachable-aux2 (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 157:

  x1 + r2 ' + y = x + h[y0.last].nxt ' + r0 ' + y0.butlast, (y0.last ' + x0).last = (r ' + x).last, (r ' + x1).last = (r ' + x).last, y0.last ≠ r, h[y0.last].nxt ≠ null, r ≠ r2, r2 ≠ y0.last, y0 ≠ [], path(r ' + x1, h), path(y0.last ' + x0, h), path(r ' + x + h[y0.last].nxt ', h), path(r ' + x1 + r2 ' + y + y0.last ', h), h[y0.last].nxt ∈ h, ¬ dups(x1 + y), ¬ dups(x1), ¬ dups(x0), ¬ r ∈ y, ¬ r ∈ x1, ¬ y0.last ∈ x0, ¬ y0.last ∈ x, ¬ r2 ∈ y, ¬ r2 ∈ x1, ¬ y0.last ∈ y, ¬ y0.last ∈ x1 ⊦

Rule argument

Additional information

Used simplifier rules: a: ⊦ (x + y) + z = x + y + z; from specification polylist ⊦ x ≠ [] → (a ' + x).last = x.last; (s)

Proof step 157 from proof rem-stays-reachable-aux2 (previous step) (back to tree)

User applied rule apply elim lemma

And obtained the following new goals

• Proof step 158:

  x1 + r2 ' + y = x + h[r1].nxt ' + r0 ' + y1, (r ' + x1).last = (r ' + x).last, (r1 ' + x0).last = (r ' + x).last, y0 = y1 + r1 ', h[r1].nxt ≠ null, r ≠ r2, r1 ≠ r, r2 ≠ r1, y0 ≠ [], path(r ' + x1 + r2 ' + y + r1 ', h), path(r ' + x + h[r1].nxt ', h), path(r1 ' + x0, h), path(r ' + x1, h), h[r1].nxt ∈ h, ¬ dups(x1 + y), ¬ dups(x1), ¬ dups(x0), ¬ r ∈ y, ¬ r ∈ x1, ¬ r1 ∈ x0, ¬ r1 ∈ x, ¬ r2 ∈ y, ¬ r2 ∈ x1, ¬ r1 ∈ y, ¬ r1 ∈ x1 ⊦

Rule argument

Additional information

Used simplifier rules: x ≠ [] ⊦ a = x.last ∧ y = x.butlast ↔ x = y + a '; (elim) Used terms: y0, a, y1

Proof step 158 from proof rem-stays-reachable-aux2 (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 159:

  x1 + r2 ' + y = x + h[r1].nxt ' + r0 ' + y1, (r1 ' + x0).last = (r ' + x).last, (r ' + x1).last = (r ' + x).last, h[r1].nxt ≠ null, r ≠ r2, r1 ≠ r, r2 ≠ r1, path(r ' + x1, h), path(r1 ' + x0, h), path(r ' + x + h[r1].nxt ', h), path(r ' + x1 + r2 ' + y + r1 ', h), h[r1].nxt ∈ h, ¬ dups(x1 + y), ¬ dups(x1), ¬ dups(x0), ¬ r ∈ y, ¬ r ∈ x1, ¬ r1 ∈ x0, ¬ r1 ∈ x, ¬ r2 ∈ y, ¬ r2 ∈ x1, ¬ r1 ∈ y, ¬ r1 ∈ x1 ⊦

Rule argument

Additional information

Used simplifier rules: a: ⊦ (x + y) + z = x + y + z; from specification polylist ⊦ x + a ' ≠ []; (s)

Proof step 159 from proof rem-stays-reachable-aux2 (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 160:

  ⊦ path(r ' + x + r0 ', h) ↔ path(r ' + x, h) ∧ h[(r ' + x).last].nxt = r0 ∧ r0 ∈ h ∧ r0 ≠ null

• Proof step 161:

  x1 + r2 ' + y = x + h[r1].nxt ' + r0 ' + y1, (r ' + x1).last = (r ' + x).last, (r1 ' + x0).last = (r ' + x).last, h[(r ' + x).last].nxt = h[r1].nxt, h[r1].nxt ≠ null, r ≠ r2, r1 ≠ r, r2 ≠ r1, path(r ' + x1 + r2 ' + y + r1 ', h), path(r ' + x, h), path(r1 ' + x0, h), path(r ' + x1, h), h[r1].nxt ∈ h, ¬ dups(x1 + y), ¬ dups(x1), ¬ dups(x0), ¬ r ∈ y, ¬ r ∈ x1, ¬ r1 ∈ x0, ¬ r1 ∈ x, ¬ r2 ∈ y, ¬ r2 ∈ x1, ¬ r1 ∈ y, ¬ r1 ∈ x1 ⊦

Rule argument

Additional information

Used terms: h, h[r1].nxt, x, r

Proof step 160 from proof rem-stays-reachable-aux2 (previous step) (back to tree)

Lemma path-split-last

Proof step 161 from proof rem-stays-reachable-aux2 (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 162:

  x1 + r2 ' + y = x + h[r1].nxt ' + r0 ' + y1, (r1 ' + x0).last = (r ' + x).last, (r ' + x1).last = (r ' + x).last, h[(r ' + x).last].nxt = h[r1].nxt, h[r1].nxt ≠ null, r ≠ r2, r1 ≠ r, r2 ≠ r1, path(r ' + x1, h), path(r1 ' + x0, h), path(r ' + x, h), path(r ' + x1 + r2 ' + y + r1 ', h), h[r1].nxt ∈ h, ¬ dups(x1 + y), ¬ dups(x1), ¬ dups(x0), ¬ r ∈ y, ¬ r ∈ x1, ¬ r1 ∈ x0, ¬ r1 ∈ x, ¬ r2 ∈ y, ¬ r2 ∈ x1, ¬ r1 ∈ y, ¬ r1 ∈ x1 ⊦

Rule argument

Additional information

Proof step 162 from proof rem-stays-reachable-aux2 (previous step) (back to tree)

User applied rule cut formula

And obtained the following new goals

• Proof step 163:

  x1 + r2 ' + y = x + h[r1].nxt ' + r0 ' + y1, (r ' + x1).last = (r ' + x).last, (r1 ' + x0).last = (r ' + x).last, h[(r ' + x).last].nxt = h[r1].nxt, h[r1].nxt ≠ null, r ≠ r2, r1 ≠ r, r2 ≠ r1, path(r ' + x1 + r2 ' + y + r1 ', h), path(r ' + x, h), path(r1 ' + x0, h), path(r ' + x1, h), path(r ' + x1 + r2 ', h), h[r1].nxt ∈ h, ¬ dups(x1 + y), ¬ dups(x1), ¬ dups(x0), ¬ r ∈ y, ¬ r ∈ x1, ¬ r1 ∈ x0, ¬ r1 ∈ x, ¬ r2 ∈ y, ¬ r2 ∈ x1, ¬ r1 ∈ y, ¬ r1 ∈ x1 ⊦

Rule argument

Additional information

Used simplifier rules: path-prefix: ⊦ path(r ' + x + y, h) → (path(r ' + x, h) ↔ true); a: ⊦ (x + y) + z = x + y + z; from specification polylist Used formulas: path(r ' + x1 + r2 ', h)

Proof step 163 from proof rem-stays-reachable-aux2 (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 164:

  ⊦ path(r ' + x + r0 ', h) ↔ path(r ' + x, h) ∧ h[(r ' + x).last].nxt = r0 ∧ r0 ∈ h ∧ r0 ≠ null

• Proof step 165:

  x1 + r2 ' + y = x + h[r1].nxt ' + r0 ' + y1, (r1 ' + x0).last = (r ' + x).last, (r ' + x1).last = (r ' + x).last, h[(r ' + x1).last].nxt = r2, h[(r ' + x).last].nxt = h[r1].nxt, h[r1].nxt ≠ null, r ≠ r2, r1 ≠ r, r2 ≠ r1, r2 ≠ null, path(r ' + x1, h), path(r1 ' + x0, h), path(r ' + x, h), path(r ' + x1 + r2 ' + y + r1 ', h), h[r1].nxt ∈ h, r2 ∈ h, ¬ dups(x1 + y), ¬ dups(x1), ¬ dups(x0), ¬ r ∈ y, ¬ r ∈ x1, ¬ r1 ∈ x0, ¬ r1 ∈ x, ¬ r2 ∈ y, ¬ r2 ∈ x1, ¬ r1 ∈ y, ¬ r1 ∈ x1 ⊦

Rule argument

Additional information

Used terms: h, r2, x1, r

Proof step 164 from proof rem-stays-reachable-aux2 (previous step) (back to tree)

Lemma path-split-last

Proof step 165 from proof rem-stays-reachable-aux2 (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 166:

  (r1 ' + x0).last = (r ' + x).last, h[(r ' + x).last].nxt = h[r1].nxt, h[r1].nxt ≠ null, h[r1].nxt ≠ r1, h[r1].nxt ≠ r0, r ≠ h[r1].nxt, r ≠ r0, r1 ≠ r, r1 ≠ r0, path(r ' + x + h[r1].nxt ' + (r0 ' + y1) + r1 ', h), path(r1 ' + x0, h), path(r ' + x, h), h[r1].nxt ∈ h, ¬ dups(x + y1), ¬ dups(x), ¬ dups(x0), ¬ r0 ∈ x, ¬ r0 ∈ y1, ¬ r ∈ y1, ¬ r ∈ x, ¬ r1 ∈ x0, ¬ r1 ∈ x, ¬ h[r1].nxt ∈ y1, ¬ h[r1].nxt ∈ x, ¬ r1 ∈ y1 ⊦

Rule argument

Additional information

Used simplifier rules: a: ⊦ (x + y) + z = x + y + z; from specification polylist ⊦ a ∈ a0 ' + x ↔ ¬(a ≠ a0 ∧ ¬ a ∈ x); (ss) ⊦ dups(x + a ' + y) ↔ a ∈ x ∨ a ∈ y ∨ dups(x + y); (ws) ⊦ ¬ a ∈ x ∧ ¬ a ∈ y → (x + a ' + y = z + a ' + y0 ↔ y = y0 ∧ x = z); (ws)

Proof step 166 from proof rem-stays-reachable-aux2 (previous step) (back to tree)

User applied rule cut formula

And obtained the following new goals

• Proof step 167:

  (r1 ' + x0).last = (r ' + x).last, h[(r ' + x).last].nxt = h[r1].nxt, h[r1].nxt ≠ null, h[r1].nxt ≠ r1, h[r1].nxt ≠ r0, r ≠ h[r1].nxt, r ≠ r0, r1 ≠ r, r1 ≠ r0, path(r ' + x, h), path(r1 ' + x0, h), path(r ' + x + h[r1].nxt ' + (r0 ' + y1) + r1 ', h), path(r ' + x + h[r1].nxt ', h), h[r1].nxt ∈ h, ¬ dups(x + y1), ¬ dups(x), ¬ dups(x0), ¬ r0 ∈ x, ¬ r0 ∈ y1, ¬ r ∈ y1, ¬ r ∈ x, ¬ r1 ∈ x0, ¬ r1 ∈ x, ¬ h[r1].nxt ∈ y1, ¬ h[r1].nxt ∈ x, ¬ r1 ∈ y1 ⊦

Rule argument

Additional information

Used simplifier rules: path-prefix: ⊦ path(r ' + x + y, h) → (path(r ' + x, h) ↔ true); a: ⊦ (x + y) + z = x + y + z; from specification polylist Used formulas: path(r ' + x + h[r1].nxt ', h)

Proof step 167 from proof rem-stays-reachable-aux2 (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 168:

  ⊦ path(r ' + x + r0 ', h) ↔ path(r ' + x, h) ∧ h[(r ' + x).last].nxt = r0 ∧ r0 ∈ h ∧ r0 ≠ null

• Proof step 169:

  (r1 ' + x0).last = (r ' + x).last, h[(r ' + x).last].nxt = h[r1].nxt, h[r1].nxt ≠ r1, h[r1].nxt ≠ r0, h[r1].nxt ≠ null, r ≠ h[r1].nxt, r ≠ r0, r1 ≠ r, r1 ≠ r0, path(r ' + x + h[r1].nxt ' + (r0 ' + y1) + r1 ', h), path(r1 ' + x0, h), path(r ' + x, h), h[r1].nxt ∈ h, ¬ dups(x + y1), ¬ dups(x), ¬ dups(x0), ¬ r0 ∈ x, ¬ r0 ∈ y1, ¬ r ∈ y1, ¬ r ∈ x, ¬ r1 ∈ x0, ¬ r1 ∈ x, ¬ h[r1].nxt ∈ y1, ¬ h[r1].nxt ∈ x, ¬ r1 ∈ y1 ⊦

Rule argument

Additional information

Used terms: h, h[r1].nxt, x, r

Proof step 168 from proof rem-stays-reachable-aux2 (previous step) (back to tree)

Lemma path-split-last

Proof step 169 from proof rem-stays-reachable-aux2 (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 170:

  (r1 ' + x0).last = (r ' + x).last, h[(r ' + x).last].nxt = h[r1].nxt, h[r1].nxt ≠ r1, h[r1].nxt ≠ r0, h[r1].nxt ≠ null, r ≠ h[r1].nxt, r ≠ r0, r1 ≠ r, r1 ≠ r0, path(r ' + x, h), path(r1 ' + x0, h), path(r ' + x + h[r1].nxt ' + (r0 ' + y1) + r1 ', h), h[r1].nxt ∈ h, ¬ dups(x + y1), ¬ dups(x), ¬ dups(x0), ¬ r0 ∈ x, ¬ r0 ∈ y1, ¬ r ∈ y1, ¬ r ∈ x, ¬ r1 ∈ x0, ¬ r1 ∈ x, ¬ h[r1].nxt ∈ y1, ¬ h[r1].nxt ∈ x, ¬ r1 ∈ y1 ⊦

Rule argument

Additional information

Proof step 170 from proof rem-stays-reachable-aux2 (previous step) (back to tree)

User applied rule cut formula

And obtained the following new goals

• Proof step 171:

  (r1 ' + x0).last = (r ' + x).last, h[(r ' + x).last].nxt = h[r1].nxt, h[r1].nxt ≠ r1, h[r1].nxt ≠ r0, h[r1].nxt ≠ null, r ≠ h[r1].nxt, r ≠ r0, r1 ≠ r, r1 ≠ r0, path(r ' + x + h[r1].nxt ' + (r0 ' + y1) + r1 ', h), path(r1 ' + x0, h), path(r ' + x, h), path(h[r1].nxt ' + (r0 ' + y1) + r1 ', h), h[r1].nxt ∈ h, ¬ dups(x + y1), ¬ dups(x), ¬ dups(x0), ¬ r0 ∈ x, ¬ r0 ∈ y1, ¬ r ∈ y1, ¬ r ∈ x, ¬ r1 ∈ x0, ¬ r1 ∈ x, ¬ h[r1].nxt ∈ y1, ¬ h[r1].nxt ∈ x, ¬ r1 ∈ y1 ⊦

Rule argument

Additional information

Used simplifier rules: path-postfix: ⊦ path(x + r ' + y, h) → (path(r ' + y, h) ↔ true); a: ⊦ (x + y) + z = x + y + z; from specification polylist Used formulas: path(h[r1].nxt ' + (r0 ' + y1) + r1 ', h)

Proof step 171 from proof rem-stays-reachable-aux2 (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 172:

  (r1 ' + x0).last = (r ' + x).last, h[(r ' + x).last].nxt = h[r1].nxt, h[r1].nxt ≠ null, h[r1].nxt ≠ h[h[r1].nxt].nxt, h[r1].nxt ≠ r1, r ≠ h[h[r1].nxt].nxt, r ≠ h[r1].nxt, r1 ≠ h[h[r1].nxt].nxt, r1 ≠ r, path(h[h[r1].nxt].nxt ' + y1 + r1 ', h), path(r ' + x + h[r1].nxt ' + (h[h[r1].nxt].nxt ' + y1) + r1 ', h), path(r1 ' + x0, h), path(r ' + x, h), h[r1].nxt ∈ h, ¬ dups(x0), ¬ dups(x), ¬ dups(x + y1), ¬ r1 ∈ y1, ¬ h[r1].nxt ∈ x, ¬ h[r1].nxt ∈ y1, ¬ r1 ∈ x, ¬ r1 ∈ x0, ¬ r ∈ x, ¬ r ∈ y1, ¬ h[h[r1].nxt].nxt ∈ y1, ¬ h[h[r1].nxt].nxt ∈ x ⊦

Rule argument

Additional information

Used simplifier rules: path-cons: ⊦ path(r ' + r0 ' + x, h) ↔ r ∈ h ∧ r ≠ null ∧ h[r].nxt = r0 ∧ path(r0 ' + x, h); a: ⊦ (x + y) + z = x + y + z; from specification polylist

Proof step 172 from proof rem-stays-reachable-aux2 (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 173:

  ⊦ y ≠ [] → (x + y).last = y.last

• Proof step 174:

  (r1 ' + x0).last = (r ' + x).last, h[(r ' + x).last].nxt = h[r1].nxt, x = [], h[r1].nxt ≠ null, h[r1].nxt ≠ h[h[r1].nxt].nxt, h[r1].nxt ≠ r1, r ≠ h[h[r1].nxt].nxt, r ≠ h[r1].nxt, r1 ≠ h[h[r1].nxt].nxt, r1 ≠ r, path(r ' + x, h), path(r1 ' + x0, h), path(r ' + x + h[r1].nxt ' + (h[h[r1].nxt].nxt ' + y1) + r1 ', h), path(h[h[r1].nxt].nxt ' + y1 + r1 ', h), h[r1].nxt ∈ h, ¬ dups(x0), ¬ dups(x), ¬ dups(x + y1), ¬ r1 ∈ y1, ¬ h[r1].nxt ∈ x, ¬ h[r1].nxt ∈ y1, ¬ r1 ∈ x, ¬ r1 ∈ x0, ¬ r ∈ x, ¬ r ∈ y1, ¬ h[h[r1].nxt].nxt ∈ y1, ¬ h[h[r1].nxt].nxt ∈ x ⊦

• Proof step 186:

  (r1 ' + x0).last = x.last, h[x.last].nxt = h[r1].nxt, h[r1].nxt ≠ null, h[r1].nxt ≠ h[h[r1].nxt].nxt, h[r1].nxt ≠ r1, r ≠ h[h[r1].nxt].nxt, r ≠ h[r1].nxt, r1 ≠ h[h[r1].nxt].nxt, r1 ≠ r, x ≠ [], path(r ' + x, h), path(r1 ' + x0, h), path(r ' + x + h[r1].nxt ' + (h[h[r1].nxt].nxt ' + y1) + r1 ', h), path(h[h[r1].nxt].nxt ' + y1 + r1 ', h), h[r1].nxt ∈ h, ¬ dups(x0), ¬ dups(x), ¬ dups(x + y1), ¬ r1 ∈ y1, ¬ h[r1].nxt ∈ x, ¬ h[r1].nxt ∈ y1, ¬ r1 ∈ x, ¬ r1 ∈ x0, ¬ r ∈ x, ¬ r ∈ y1, ¬ h[h[r1].nxt].nxt ∈ y1, ¬ h[h[r1].nxt].nxt ∈ x ⊦

Rule argument

Additional information

Used terms: x, r '

Proof step 173 from proof rem-stays-reachable-aux2 (previous step) (back to tree)

A spec-lemma

Proof step 174 from proof rem-stays-reachable-aux2 (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 175:

  h[(r1 ' + x0).last].nxt = h[r1].nxt, (r1 ' + x0).last ≠ null, (r1 ' + x0).last ≠ h[r1].nxt, (r1 ' + x0).last ≠ h[h[r1].nxt].nxt, h[r1].nxt ≠ r1, h[r1].nxt ≠ h[h[r1].nxt].nxt, h[r1].nxt ≠ null, r1 ≠ (r1 ' + x0).last, r1 ≠ h[h[r1].nxt].nxt, path(h[h[r1].nxt].nxt ' + y1 + r1 ', h), path(r1 ' + x0, h), (r1 ' + x0).last ∈ h, h[r1].nxt ∈ h, ¬ dups(y1), ¬ dups(x0), ¬ h[h[r1].nxt].nxt ∈ y1, ¬ (r1 ' + x0).last ∈ y1, ¬ r1 ∈ x0, ¬ h[r1].nxt ∈ y1, ¬ r1 ∈ y1 ⊦

Rule argument

Additional information

Used simplifier rules: path-cons: ⊦ path(r ' + r0 ' + x, h) ↔ r ∈ h ∧ r ≠ null ∧ h[r].nxt = r0 ∧ path(r0 ' + x, h); path-one: ⊦ path(r ', h) ↔ r ∈ h ∧ r ≠ null; ⊦ ¬ a ∈ []; (s) a: ⊦ (x + y) + z = x + y + z; from specification polylist ⊦ [] + x = x; (s) ⊦ ¬ dups([]); (s) ⊦ x + [] = x; (s) ⊦ a '.last = a; (s)

Proof step 175 from proof rem-stays-reachable-aux2 (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 176:

  ⊦ y ≠ [] → (x + y).last = y.last

• Proof step 177:

  h[x0.last].nxt = h[r1].nxt, x0.last ≠ null, x0.last ≠ h[r1].nxt, x0.last ≠ h[h[r1].nxt].nxt, h[r1].nxt ≠ r1, h[r1].nxt ≠ h[h[r1].nxt].nxt, h[r1].nxt ≠ null, r1 ≠ x0.last, r1 ≠ h[h[r1].nxt].nxt, x0 ≠ [], path(r1 ' + x0, h), path(h[h[r1].nxt].nxt ' + y1 + r1 ', h), h[r1].nxt ∈ h, x0.last ∈ h, ¬ dups(y1), ¬ dups(x0), ¬ h[h[r1].nxt].nxt ∈ y1, ¬ x0.last ∈ y1, ¬ r1 ∈ x0, ¬ h[r1].nxt ∈ y1, ¬ r1 ∈ y1 ⊦

Rule argument

Additional information

Used simplifier rules: ⊦ x + [] = x; (s) a: ⊦ (x + y) + z = x + y + z; from specification polylist ⊦ a '.last = a; (s) Used terms: x0, r1 '

Proof step 176 from proof rem-stays-reachable-aux2 (previous step) (back to tree)

A spec-lemma

Proof step 177 from proof rem-stays-reachable-aux2 (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 178:

  h[x0.last].nxt = h[r1].nxt, x0.last ≠ null, x0.last ≠ h[r1].nxt, x0.last ≠ h[h[r1].nxt].nxt, h[r1].nxt ≠ r1, h[r1].nxt ≠ h[h[r1].nxt].nxt, h[r1].nxt ≠ null, r1 ≠ x0.last, r1 ≠ h[h[r1].nxt].nxt, x0 ≠ [], path(h[h[r1].nxt].nxt ' + y1 + r1 ', h), path(r1 ' + x0, h), x0.last ∈ h, h[r1].nxt ∈ h, ¬ dups(y1), ¬ dups(x0), ¬ h[h[r1].nxt].nxt ∈ y1, ¬ x0.last ∈ y1, ¬ r1 ∈ x0, ¬ h[r1].nxt ∈ y1, ¬ r1 ∈ y1 ⊦

Rule argument

Additional information

Proof step 178 from proof rem-stays-reachable-aux2 (previous step) (back to tree)

User applied rule apply elim lemma

And obtained the following new goals

• Proof step 179:

  h[r].nxt = h[r1].nxt, x0 = y + r ', h[r1].nxt ≠ r1, h[r1].nxt ≠ h[h[r1].nxt].nxt, h[r1].nxt ≠ null, r ≠ null, r ≠ h[r1].nxt, r ≠ h[h[r1].nxt].nxt, r1 ≠ r, r1 ≠ h[h[r1].nxt].nxt, x0 ≠ [], path(r1 ' + x0, h), path(h[h[r1].nxt].nxt ' + y1 + r1 ', h), h[r1].nxt ∈ h, r ∈ h, ¬ dups(y1), ¬ dups(x0), ¬ h[h[r1].nxt].nxt ∈ y1, ¬ r ∈ y1, ¬ r1 ∈ x0, ¬ h[r1].nxt ∈ y1, ¬ r1 ∈ y1 ⊦

Rule argument

Additional information

Used simplifier rules: x ≠ [] ⊦ a = x.last ∧ y = x.butlast ↔ x = y + a '; (elim) Used terms: x0, a, y

Proof step 179 from proof rem-stays-reachable-aux2 (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 180:

  h[r].nxt = h[r1].nxt, h[r1].nxt ≠ r1, h[r1].nxt ≠ h[h[r1].nxt].nxt, h[r1].nxt ≠ null, r ≠ null, r ≠ h[r1].nxt, r ≠ h[h[r1].nxt].nxt, r1 ≠ r, r1 ≠ h[h[r1].nxt].nxt, path(h[h[r1].nxt].nxt ' + y1 + r1 ', h), path(r1 ' + y + r ', h), r ∈ h, h[r1].nxt ∈ h, ¬ dups(y1), ¬ dups(y), ¬ h[r1].nxt ∈ y1, ¬ r1 ∈ y1, ¬ r ∈ y, ¬ h[h[r1].nxt].nxt ∈ y1, ¬ r ∈ y1, ¬ r1 ∈ y ⊦

Rule argument

Additional information

Used simplifier rules: a: ⊦ (x + y) + z = x + y + z; from specification polylist ⊦ a ∈ a0 ' ↔ a = a0; (s) ⊦ a ∈ x + y ↔ a ∈ x ∨ a ∈ y; (s) ⊦ dups(x + a ') ↔ a ∈ x ∨ dups(x); (ws) ⊦ x + a ' ≠ []; (s)

Proof step 180 from proof rem-stays-reachable-aux2 (previous step) (back to tree)

User applied rule constructor cut

And obtained the following new goals

• Proof step 181:

  h[r].nxt = h[r1].nxt, y = r0 + y0, h[r1].nxt ≠ r1, h[r1].nxt ≠ h[h[r1].nxt].nxt, h[r1].nxt ≠ null, r ≠ null, r ≠ h[r1].nxt, r ≠ h[h[r1].nxt].nxt, r1 ≠ r, r1 ≠ h[h[r1].nxt].nxt, path(r1 ' + y + r ', h), path(h[h[r1].nxt].nxt ' + y1 + r1 ', h), h[r1].nxt ∈ h, r ∈ h, ¬ dups(y1), ¬ dups(y), ¬ h[r1].nxt ∈ y1, ¬ r1 ∈ y1, ¬ r ∈ y, ¬ h[h[r1].nxt].nxt ∈ y1, ¬ r ∈ y1, ¬ r1 ∈ y ⊦

Rule argument

Additional information

Used simplifier rules: path-two: ⊦ path(r ' + r0 ', h) ↔ r ∈ h ∧ r0 ∈ h ∧ r ≠ null ∧ r0 ≠ null ∧ h[r].nxt = r0; list('a) freely generated by [], +;; ⊦ [] + x = x; (s) a: ⊦ (x + y) + z = x + y + z; from specification polylist

Proof step 181 from proof rem-stays-reachable-aux2 (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 182:

  h[r].nxt = h[r1].nxt, h[r1].nxt ≠ null, h[r1].nxt ≠ h[h[r1].nxt].nxt, h[r1].nxt ≠ r1, r ≠ h[h[r1].nxt].nxt, r ≠ h[r1].nxt, r ≠ null, r1 ≠ null, r1 ≠ h[h[r1].nxt].nxt, r1 ≠ r, path(h[r1].nxt ' + y0 + r ', h), path(h[h[r1].nxt].nxt ' + y1 + r1 ', h), r1 ∈ h, h[r1].nxt ∈ h, r ∈ h, ¬ dups(y0), ¬ dups(y1), ¬ r1 ∈ y0, ¬ r ∈ y1, ¬ h[h[r1].nxt].nxt ∈ y1, ¬ r ∈ y0, ¬ r1 ∈ y1, ¬ h[r1].nxt ∈ y1, ¬ h[r1].nxt ∈ y0 ⊦

Rule argument

Additional information

Used simplifier rules: path-cons: ⊦ path(r ' + r0 ' + x, h) ↔ r ∈ h ∧ r ≠ null ∧ h[r].nxt = r0 ∧ path(r0 ' + x, h); a: ⊦ (x + y) + z = x + y + z; from specification polylist ⊦ a ∈ a0 ' + x ↔ ¬(a ≠ a0 ∧ ¬ a ∈ x); (ss) ⊦ a + x = a ' + x; (s) ⊦ dups(a ' + x) ↔ a ∈ x ∨ dups(x); (s)

Proof step 182 from proof rem-stays-reachable-aux2 (previous step) (back to tree)

User applied rule constructor cut

And obtained the following new goals

• Proof step 183:

  h[r].nxt = h[r1].nxt, y0 = r0 + y, h[r1].nxt ≠ null, h[r1].nxt ≠ h[h[r1].nxt].nxt, h[r1].nxt ≠ r1, r ≠ h[h[r1].nxt].nxt, r ≠ h[r1].nxt, r ≠ null, r1 ≠ null, r1 ≠ h[h[r1].nxt].nxt, r1 ≠ r, path(h[h[r1].nxt].nxt ' + y1 + r1 ', h), path(h[r1].nxt ' + y0 + r ', h), r ∈ h, h[r1].nxt ∈ h, r1 ∈ h, ¬ dups(y0), ¬ dups(y1), ¬ r1 ∈ y0, ¬ r ∈ y1, ¬ h[h[r1].nxt].nxt ∈ y1, ¬ r ∈ y0, ¬ r1 ∈ y1, ¬ h[r1].nxt ∈ y1, ¬ h[r1].nxt ∈ y0 ⊦

Rule argument

Additional information

Used simplifier rules: path-two: ⊦ path(r ' + r0 ', h) ↔ r ∈ h ∧ r0 ∈ h ∧ r ≠ null ∧ r0 ≠ null ∧ h[r].nxt = r0; list('a) freely generated by [], +;; ⊦ [] + x = x; (s) a: ⊦ (x + y) + z = x + y + z; from specification polylist

Proof step 183 from proof rem-stays-reachable-aux2 (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 184:

  h[r].nxt = h[r1].nxt, h[r1].nxt ≠ r1, h[r1].nxt ≠ h[h[r1].nxt].nxt, h[r1].nxt ≠ null, r ≠ null, r ≠ h[r1].nxt, r ≠ h[h[r1].nxt].nxt, r1 ≠ r, r1 ≠ h[h[r1].nxt].nxt, r1 ≠ null, path(h[h[r1].nxt].nxt ' + y + r ', h), path(h[h[r1].nxt].nxt ' + y1 + r1 ', h), r ∈ h, h[r1].nxt ∈ h, r1 ∈ h, ¬ dups(y1), ¬ dups(y), ¬ h[r1].nxt ∈ y, ¬ h[r1].nxt ∈ y1, ¬ r1 ∈ y1, ¬ r ∈ y, ¬ h[h[r1].nxt].nxt ∈ y1, ¬ r ∈ y1, ¬ r1 ∈ y, ¬ h[h[r1].nxt].nxt ∈ y ⊦

Rule argument

Additional information

Used simplifier rules: path-cons: ⊦ path(r ' + r0 ' + x, h) ↔ r ∈ h ∧ r ≠ null ∧ h[r].nxt = r0 ∧ path(r0 ' + x, h); a: ⊦ (x + y) + z = x + y + z; from specification polylist ⊦ a ∈ a0 ' + x ↔ ¬(a ≠ a0 ∧ ¬ a ∈ x); (ss) ⊦ a + x = a ' + x; (s) ⊦ dups(a ' + x) ↔ a ∈ x ∨ dups(x); (s)

Proof step 184 from proof rem-stays-reachable-aux2 (previous step) (back to tree)

User applied rule apply lemma

And obtained the following new goals

• Proof step 185:

  path(r ' + x, h), path(r ' + y, h) ⊦ x = y ∨ (∃ r0, y0. x = y + r0 ' + y0) ∨ (∃ r0, x0. y = x + r0 ' + x0)

Rule argument

Additional information

Used simplifier rules: ⊦ ¬ a0 ∈ y ∧ a0 ≠ a → y + a ' ≠ y0 + a0 ' + z; (s) ⊦ x + a ' = y + a0 ' ↔ x = y ∧ a = a0; (ws) a: ⊦ (x + y) + z = x + y + z; from specification polylist Used terms: h[h[r1].nxt].nxt, y1 + r1 ', h, y + r '

Proof step 185 from proof rem-stays-reachable-aux2 (previous step) (back to tree)

Lemma linearity-path

Proof step 186 from proof rem-stays-reachable-aux2 (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 187:

  (r1 ' + x0).last = x.last, h[x.last].nxt = h[r1].nxt, h[r1].nxt ≠ null, h[r1].nxt ≠ h[h[r1].nxt].nxt, h[r1].nxt ≠ r1, r ≠ h[h[r1].nxt].nxt, r ≠ h[r1].nxt, r1 ≠ h[h[r1].nxt].nxt, r1 ≠ r, x ≠ [], path(h[h[r1].nxt].nxt ' + y1 + r1 ', h), path(r ' + x + h[r1].nxt ' + (h[h[r1].nxt].nxt ' + y1) + r1 ', h), path(r1 ' + x0, h), path(r ' + x, h), h[r1].nxt ∈ h, ¬ dups(x0), ¬ dups(x), ¬ dups(x + y1), ¬ r1 ∈ y1, ¬ h[r1].nxt ∈ x, ¬ h[r1].nxt ∈ y1, ¬ r1 ∈ x, ¬ r1 ∈ x0, ¬ r ∈ x, ¬ r ∈ y1, ¬ h[h[r1].nxt].nxt ∈ y1, ¬ h[h[r1].nxt].nxt ∈ x ⊦

Rule argument

Additional information

Proof step 187 from proof rem-stays-reachable-aux2 (previous step) (back to tree)

User applied rule apply elim lemma

And obtained the following new goals

• Proof step 188:

  (r1 ' + x0).last = r0, h[r0].nxt = h[r1].nxt, x = y + r0 ', h[r1].nxt ≠ null, h[r1].nxt ≠ h[h[r1].nxt].nxt, h[r1].nxt ≠ r1, r ≠ h[h[r1].nxt].nxt, r ≠ h[r1].nxt, r1 ≠ h[h[r1].nxt].nxt, r1 ≠ r, x ≠ [], path(r ' + x, h), path(r1 ' + x0, h), path(r ' + x + h[r1].nxt ' + (h[h[r1].nxt].nxt ' + y1) + r1 ', h), path(h[h[r1].nxt].nxt ' + y1 + r1 ', h), h[r1].nxt ∈ h, ¬ dups(x0), ¬ dups(x), ¬ dups(x + y1), ¬ r1 ∈ y1, ¬ h[r1].nxt ∈ x, ¬ h[r1].nxt ∈ y1, ¬ r1 ∈ x, ¬ r1 ∈ x0, ¬ r ∈ x, ¬ r ∈ y1, ¬ h[h[r1].nxt].nxt ∈ y1, ¬ h[h[r1].nxt].nxt ∈ x ⊦

Rule argument

Additional information

Used simplifier rules: x ≠ [] ⊦ a = x.last ∧ y = x.butlast ↔ x = y + a '; (elim) Used terms: x, a, y

Proof step 188 from proof rem-stays-reachable-aux2 (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 189:

  h[(r1 ' + x0).last].nxt = h[r1].nxt, h[r1].nxt ≠ null, h[r1].nxt ≠ h[h[r1].nxt].nxt, h[r1].nxt ≠ r1, h[r1].nxt ≠ (r1 ' + x0).last, h[h[r1].nxt].nxt ≠ (r1 ' + x0).last, r ≠ h[h[r1].nxt].nxt, r ≠ h[r1].nxt, r ≠ (r1 ' + x0).last, r1 ≠ h[h[r1].nxt].nxt, r1 ≠ r, r1 ≠ (r1 ' + x0).last, path(h[h[r1].nxt].nxt ' + y1 + r1 ', h), path(r ' + (y + (r1 ' + x0).last ') + h[r1].nxt ' + (h[h[r1].nxt].nxt ' + y1) + r1 ', h), path(r1 ' + x0, h), path(r ' + y + (r1 ' + x0).last ', h), h[r1].nxt ∈ h, ¬ dups(y + y1), ¬ dups(x0), ¬ dups(y), ¬ (r1 ' + x0).last ∈ y, ¬ (r1 ' + x0).last ∈ y1, ¬ r1 ∈ y1, ¬ h[r1].nxt ∈ y, ¬ h[r1].nxt ∈ y1, ¬ r1 ∈ y, ¬ r1 ∈ x0, ¬ r ∈ y, ¬ r ∈ y1, ¬ h[h[r1].nxt].nxt ∈ y1, ¬ h[h[r1].nxt].nxt ∈ y ⊦

Rule argument

Additional information

Used simplifier rules: a: ⊦ (x + y) + z = x + y + z; from specification polylist ⊦ ¬ b ∈ x → (dups(x + b ') ↔ dups(x)); (s) ⊦ a ∈ a0 ' ↔ a = a0; (s) ⊦ a ∈ x + y ↔ a ∈ x ∨ a ∈ y; (s) ⊦ dups(x + a ' + y) ↔ a ∈ x ∨ a ∈ y ∨ dups(x + y); (ws) ⊦ x + a ' ≠ []; (s)

Proof step 189 from proof rem-stays-reachable-aux2 (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 190:

  ⊦ y ≠ [] → (x + y).last = y.last

• Proof step 191:

  h[x0.last].nxt = h[r1].nxt, h[r1].nxt ≠ null, h[r1].nxt ≠ h[h[r1].nxt].nxt, h[r1].nxt ≠ r1, h[r1].nxt ≠ x0.last, h[h[r1].nxt].nxt ≠ x0.last, r ≠ h[h[r1].nxt].nxt, r ≠ h[r1].nxt, r ≠ x0.last, r1 ≠ h[h[r1].nxt].nxt, r1 ≠ r, r1 ≠ x0.last, x0 ≠ [], path(r ' + y + x0.last ', h), path(r1 ' + x0, h), path(r ' + (y + x0.last ') + h[r1].nxt ' + (h[h[r1].nxt].nxt ' + y1) + r1 ', h), path(h[h[r1].nxt].nxt ' + y1 + r1 ', h), h[r1].nxt ∈ h, ¬ dups(y + y1), ¬ dups(x0), ¬ dups(y), ¬ x0.last ∈ y, ¬ x0.last ∈ y1, ¬ r1 ∈ y1, ¬ h[r1].nxt ∈ y, ¬ h[r1].nxt ∈ y1, ¬ r1 ∈ y, ¬ r1 ∈ x0, ¬ r ∈ y, ¬ r ∈ y1, ¬ h[h[r1].nxt].nxt ∈ y1, ¬ h[h[r1].nxt].nxt ∈ y ⊦

Rule argument

Additional information

Used simplifier rules: ⊦ x + [] = x; (s) a: ⊦ (x + y) + z = x + y + z; from specification polylist ⊦ a '.last = a; (s) Used terms: x0, r1 '

Proof step 190 from proof rem-stays-reachable-aux2 (previous step) (back to tree)

A spec-lemma

Proof step 191 from proof rem-stays-reachable-aux2 (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 192:

  h[x0.last].nxt = h[r1].nxt, h[r1].nxt ≠ null, h[r1].nxt ≠ h[h[r1].nxt].nxt, h[r1].nxt ≠ r1, h[r1].nxt ≠ x0.last, h[h[r1].nxt].nxt ≠ x0.last, r ≠ h[h[r1].nxt].nxt, r ≠ h[r1].nxt, r ≠ x0.last, r1 ≠ h[h[r1].nxt].nxt, r1 ≠ r, r1 ≠ x0.last, x0 ≠ [], path(h[h[r1].nxt].nxt ' + y1 + r1 ', h), path(r ' + (y + x0.last ') + h[r1].nxt ' + (h[h[r1].nxt].nxt ' + y1) + r1 ', h), path(r1 ' + x0, h), path(r ' + y + x0.last ', h), h[r1].nxt ∈ h, ¬ dups(y + y1), ¬ dups(x0), ¬ dups(y), ¬ x0.last ∈ y, ¬ x0.last ∈ y1, ¬ r1 ∈ y1, ¬ h[r1].nxt ∈ y, ¬ h[r1].nxt ∈ y1, ¬ r1 ∈ y, ¬ r1 ∈ x0, ¬ r ∈ y, ¬ r ∈ y1, ¬ h[h[r1].nxt].nxt ∈ y1, ¬ h[h[r1].nxt].nxt ∈ y ⊦

Rule argument

Additional information

Proof step 192 from proof rem-stays-reachable-aux2 (previous step) (back to tree)

User applied rule apply elim lemma

And obtained the following new goals

• Proof step 193:

  h[r0].nxt = h[r1].nxt, x0 = y0 + r0 ', h[r1].nxt ≠ null, h[r1].nxt ≠ h[h[r1].nxt].nxt, h[r1].nxt ≠ r1, h[r1].nxt ≠ r0, h[h[r1].nxt].nxt ≠ r0, r ≠ h[h[r1].nxt].nxt, r ≠ h[r1].nxt, r ≠ r0, r1 ≠ h[h[r1].nxt].nxt, r1 ≠ r, r1 ≠ r0, x0 ≠ [], path(r ' + y + r0 ', h), path(r1 ' + x0, h), path(r ' + (y + r0 ') + h[r1].nxt ' + (h[h[r1].nxt].nxt ' + y1) + r1 ', h), path(h[h[r1].nxt].nxt ' + y1 + r1 ', h), h[r1].nxt ∈ h, ¬ dups(y + y1), ¬ dups(x0), ¬ dups(y), ¬ r0 ∈ y, ¬ r0 ∈ y1, ¬ r1 ∈ y1, ¬ h[r1].nxt ∈ y, ¬ h[r1].nxt ∈ y1, ¬ r1 ∈ y, ¬ r1 ∈ x0, ¬ r ∈ y, ¬ r ∈ y1, ¬ h[h[r1].nxt].nxt ∈ y1, ¬ h[h[r1].nxt].nxt ∈ y ⊦

Rule argument

Additional information

Used simplifier rules: x ≠ [] ⊦ a = x.last ∧ y = x.butlast ↔ x = y + a '; (elim) Used terms: x0, a, y0

Proof step 193 from proof rem-stays-reachable-aux2 (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 194:

  h[r0].nxt = h[r1].nxt, h[r1].nxt ≠ null, h[r1].nxt ≠ h[h[r1].nxt].nxt, h[r1].nxt ≠ r1, h[r1].nxt ≠ r0, h[h[r1].nxt].nxt ≠ r0, r ≠ h[h[r1].nxt].nxt, r ≠ h[r1].nxt, r ≠ r0, r1 ≠ h[h[r1].nxt].nxt, r1 ≠ r, r1 ≠ r0, path(h[h[r1].nxt].nxt ' + y1 + r1 ', h), path(r ' + (y + r0 ') + h[r1].nxt ' + (h[h[r1].nxt].nxt ' + y1) + r1 ', h), path(r1 ' + y0 + r0 ', h), path(r ' + y + r0 ', h), h[r1].nxt ∈ h, ¬ dups(y + y1), ¬ dups(y0), ¬ dups(y), ¬ r ∈ y, ¬ r ∈ y1, ¬ h[h[r1].nxt].nxt ∈ y1, ¬ h[h[r1].nxt].nxt ∈ y, ¬ r0 ∈ y0, ¬ r0 ∈ y, ¬ r0 ∈ y1, ¬ r1 ∈ y1, ¬ h[r1].nxt ∈ y, ¬ h[r1].nxt ∈ y1, ¬ r1 ∈ y, ¬ r1 ∈ y0 ⊦

Rule argument

Additional information

Used simplifier rules: a: ⊦ (x + y) + z = x + y + z; from specification polylist ⊦ a ∈ a0 ' ↔ a = a0; (s) ⊦ a ∈ x + y ↔ a ∈ x ∨ a ∈ y; (s) ⊦ dups(x + a ') ↔ a ∈ x ∨ dups(x); (ws) ⊦ x + a ' ≠ []; (s)

Proof step 194 from proof rem-stays-reachable-aux2 (previous step) (back to tree)

User applied rule constructor cut

And obtained the following new goals

• Proof step 195:

  h[r0].nxt = h[r1].nxt, y0 = r2 + y2, h[r1].nxt ≠ null, h[r1].nxt ≠ h[h[r1].nxt].nxt, h[r1].nxt ≠ r1, h[r1].nxt ≠ r0, h[h[r1].nxt].nxt ≠ r0, r ≠ h[h[r1].nxt].nxt, r ≠ h[r1].nxt, r ≠ r0, r1 ≠ h[h[r1].nxt].nxt, r1 ≠ r, r1 ≠ r0, path(r ' + y + r0 ', h), path(r1 ' + y0 + r0 ', h), path(r ' + (y + r0 ') + h[r1].nxt ' + (h[h[r1].nxt].nxt ' + y1) + r1 ', h), path(h[h[r1].nxt].nxt ' + y1 + r1 ', h), h[r1].nxt ∈ h, ¬ dups(y + y1), ¬ dups(y0), ¬ dups(y), ¬ r ∈ y, ¬ r ∈ y1, ¬ h[h[r1].nxt].nxt ∈ y1, ¬ h[h[r1].nxt].nxt ∈ y, ¬ r0 ∈ y0, ¬ r0 ∈ y, ¬ r0 ∈ y1, ¬ r1 ∈ y1, ¬ h[r1].nxt ∈ y, ¬ h[r1].nxt ∈ y1, ¬ r1 ∈ y, ¬ r1 ∈ y0 ⊦

Rule argument

Additional information

Used simplifier rules: path-two: ⊦ path(r ' + r0 ', h) ↔ r ∈ h ∧ r0 ∈ h ∧ r ≠ null ∧ r0 ≠ null ∧ h[r].nxt = r0; list('a) freely generated by [], +;; ⊦ [] + x = x; (s) a: ⊦ (x + y) + z = x + y + z; from specification polylist

Proof step 195 from proof rem-stays-reachable-aux2 (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 196:

  h[r0].nxt = h[r1].nxt, h[h[r1].nxt].nxt ≠ r0, h[r1].nxt ≠ r0, h[r1].nxt ≠ r1, h[r1].nxt ≠ h[h[r1].nxt].nxt, h[r1].nxt ≠ null, r ≠ r0, r ≠ h[r1].nxt, r ≠ h[h[r1].nxt].nxt, r1 ≠ null, r1 ≠ r0, r1 ≠ r, r1 ≠ h[h[r1].nxt].nxt, path(h[r1].nxt ' + y2 + r0 ', h), path(r ' + (y + r0 ') + h[r1].nxt ' + (h[h[r1].nxt].nxt ' + y1) + r1 ', h), path(h[h[r1].nxt].nxt ' + y1 + r1 ', h), path(r ' + y + r0 ', h), r1 ∈ h, h[r1].nxt ∈ h, ¬ dups(y), ¬ dups(y2), ¬ dups(y + y1), ¬ r1 ∈ y2, ¬ r1 ∈ y, ¬ h[r1].nxt ∈ y1, ¬ h[r1].nxt ∈ y, ¬ r1 ∈ y1, ¬ r0 ∈ y1, ¬ r0 ∈ y, ¬ r0 ∈ y2, ¬ h[h[r1].nxt].nxt ∈ y, ¬ h[h[r1].nxt].nxt ∈ y1, ¬ r ∈ y1, ¬ r ∈ y, ¬ h[r1].nxt ∈ y2 ⊦

Rule argument

Additional information

Used simplifier rules: path-cons: ⊦ path(r ' + r0 ' + x, h) ↔ r ∈ h ∧ r ≠ null ∧ h[r].nxt = r0 ∧ path(r0 ' + x, h); a: ⊦ (x + y) + z = x + y + z; from specification polylist ⊦ a ∈ a0 ' + x ↔ ¬(a ≠ a0 ∧ ¬ a ∈ x); (ss) ⊦ a + x = a ' + x; (s) ⊦ dups(a ' + x) ↔ a ∈ x ∨ dups(x); (s)

Proof step 196 from proof rem-stays-reachable-aux2 (previous step) (back to tree)

User applied rule constructor cut

And obtained the following new goals

• Proof step 197:

  h[r0].nxt = h[r1].nxt, y2 = r2 + y0, h[h[r1].nxt].nxt ≠ r0, h[r1].nxt ≠ r0, h[r1].nxt ≠ r1, h[r1].nxt ≠ h[h[r1].nxt].nxt, h[r1].nxt ≠ null, r ≠ r0, r ≠ h[r1].nxt, r ≠ h[h[r1].nxt].nxt, r1 ≠ null, r1 ≠ r0, r1 ≠ r, r1 ≠ h[h[r1].nxt].nxt, path(r ' + y + r0 ', h), path(h[h[r1].nxt].nxt ' + y1 + r1 ', h), path(r ' + (y + r0 ') + h[r1].nxt ' + (h[h[r1].nxt].nxt ' + y1) + r1 ', h), path(h[r1].nxt ' + y2 + r0 ', h), h[r1].nxt ∈ h, r1 ∈ h, ¬ dups(y), ¬ dups(y2), ¬ dups(y + y1), ¬ r1 ∈ y2, ¬ r1 ∈ y, ¬ h[r1].nxt ∈ y1, ¬ h[r1].nxt ∈ y, ¬ r1 ∈ y1, ¬ r0 ∈ y1, ¬ r0 ∈ y, ¬ r0 ∈ y2, ¬ h[h[r1].nxt].nxt ∈ y, ¬ h[h[r1].nxt].nxt ∈ y1, ¬ r ∈ y1, ¬ r ∈ y, ¬ h[r1].nxt ∈ y2 ⊦

Rule argument

Additional information

Used simplifier rules: path-two: ⊦ path(r ' + r0 ', h) ↔ r ∈ h ∧ r0 ∈ h ∧ r ≠ null ∧ r0 ≠ null ∧ h[r].nxt = r0; list('a) freely generated by [], +;; ⊦ [] + x = x; (s) a: ⊦ (x + y) + z = x + y + z; from specification polylist

Proof step 197 from proof rem-stays-reachable-aux2 (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 198:

  h[r0].nxt = h[r1].nxt, h[r1].nxt ≠ null, h[r1].nxt ≠ h[h[r1].nxt].nxt, h[r1].nxt ≠ r1, h[r1].nxt ≠ r0, h[h[r1].nxt].nxt ≠ r0, r ≠ h[h[r1].nxt].nxt, r ≠ h[r1].nxt, r ≠ r0, r1 ≠ h[h[r1].nxt].nxt, r1 ≠ r, r1 ≠ r0, r1 ≠ null, path(h[h[r1].nxt].nxt ' + y0 + r0 ', h), path(r ' + y + r0 ', h), path(h[h[r1].nxt].nxt ' + y1 + r1 ', h), path(r ' + (y + r0 ') + h[r1].nxt ' + (h[h[r1].nxt].nxt ' + y1) + r1 ', h), h[r1].nxt ∈ h, r1 ∈ h, ¬ dups(y + y1), ¬ dups(y0), ¬ dups(y), ¬ h[r1].nxt ∈ y0, ¬ r ∈ y, ¬ r ∈ y1, ¬ h[h[r1].nxt].nxt ∈ y1, ¬ h[h[r1].nxt].nxt ∈ y, ¬ r0 ∈ y0, ¬ r0 ∈ y, ¬ r0 ∈ y1, ¬ r1 ∈ y1, ¬ h[r1].nxt ∈ y, ¬ h[r1].nxt ∈ y1, ¬ r1 ∈ y, ¬ r1 ∈ y0, ¬ h[h[r1].nxt].nxt ∈ y0 ⊦

Rule argument

Additional information

Used simplifier rules: path-cons: ⊦ path(r ' + r0 ' + x, h) ↔ r ∈ h ∧ r ≠ null ∧ h[r].nxt = r0 ∧ path(r0 ' + x, h); a: ⊦ (x + y) + z = x + y + z; from specification polylist ⊦ a ∈ a0 ' + x ↔ ¬(a ≠ a0 ∧ ¬ a ∈ x); (ss) ⊦ a + x = a ' + x; (s) ⊦ dups(a ' + x) ↔ a ∈ x ∨ dups(x); (s)

Proof step 198 from proof rem-stays-reachable-aux2 (previous step) (back to tree)

User applied rule apply lemma

And obtained the following new goals

• Proof step 199:

  path(r ' + x, h), path(r ' + y, h) ⊦ x = y ∨ (∃ r0, y0. x = y + r0 ' + y0) ∨ (∃ r0, x0. y = x + r0 ' + x0)

Rule argument

Additional information

Used simplifier rules: ⊦ ¬ a0 ∈ y ∧ a0 ≠ a → y + a ' ≠ y0 + a0 ' + z; (s) ⊦ x + a ' = y + a0 ' ↔ x = y ∧ a = a0; (ws) a: ⊦ (x + y) + z = x + y + z; from specification polylist Used terms: h[h[r1].nxt].nxt, y1 + r1 ', h, y0 + r0 '

Proof step 199 from proof rem-stays-reachable-aux2 (previous step) (back to tree)

Lemma linearity-path

Proof step 200 from proof rem-stays-reachable-aux2 (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 201:

  x + h[(r ' + x2).last].nxt ' = x2 + r1 ' + x3, (r ' + x1).last = (r ' + x).last, ((r ' + x2).last ' + x0).last = (r ' + x).last, (r ' + x2).last ≠ r, h[(r ' + x2).last].nxt ≠ null, path(r ' + x2, h), path(r ' + x1, h), path((r ' + x2).last ' + x0, h), path(r ' + x2 + r1 ' + x3, h), h[(r ' + x2).last].nxt ∈ h, ¬ dups(x0), ¬ dups(x1), ¬ dups(x2), ¬ (r ' + x2).last ∈ x, ¬ (r ' + x2).last ∈ x0, ¬ r ∈ x1, ¬ r ∈ x2 ⊦

Rule argument

Additional information

Proof step 201 from proof rem-stays-reachable-aux2 (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 202:

  ⊦ y ≠ [] → (x + y).last = y.last

• Proof step 203:

  x + h[x2.last].nxt ' = x2 + r1 ' + x3, (x2.last ' + x0).last = (r ' + x).last, (r ' + x1).last = (r ' + x).last, x2.last ≠ r, h[x2.last].nxt ≠ null, x2 ≠ [], path(r ' + x2 + r1 ' + x3, h), path(x2.last ' + x0, h), path(r ' + x1, h), path(r ' + x2, h), h[x2.last].nxt ∈ h, ¬ dups(x0), ¬ dups(x1), ¬ dups(x2), ¬ x2.last ∈ x, ¬ x2.last ∈ x0, ¬ r ∈ x1, ¬ r ∈ x2 ⊦

Rule argument

Additional information

Used simplifier rules: ⊦ [] + x = x; (s) ⊦ x + [] = x; (s) a: ⊦ (x + y) + z = x + y + z; from specification polylist ⊦ a '.last = a; (s) Used terms: x2, r '

Proof step 202 from proof rem-stays-reachable-aux2 (previous step) (back to tree)

A spec-lemma

Proof step 203 from proof rem-stays-reachable-aux2 (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 204:

  x + h[x2.last].nxt ' = x2 + r1 ' + x3, (r ' + x1).last = (r ' + x).last, (x2.last ' + x0).last = (r ' + x).last, x2.last ≠ r, h[x2.last].nxt ≠ null, x2 ≠ [], path(r ' + x2, h), path(r ' + x1, h), path(x2.last ' + x0, h), path(r ' + x2 + r1 ' + x3, h), h[x2.last].nxt ∈ h, ¬ dups(x0), ¬ dups(x1), ¬ dups(x2), ¬ x2.last ∈ x, ¬ x2.last ∈ x0, ¬ r ∈ x1, ¬ r ∈ x2 ⊦

Rule argument

Additional information

Proof step 204 from proof rem-stays-reachable-aux2 (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 205:

  ⊦ y ≠ [] → (x + y).last = y.last

• Proof step 206:

  x + h[x2.last].nxt ' = x2 + r1 ' + x3, (x2.last ' + x0).last = (r ' + x).last, (r ' + x1).last = (r ' + x).last, x1 = [], x2.last ≠ r, h[x2.last].nxt ≠ null, x2 ≠ [], path(r ' + x2 + r1 ' + x3, h), path(x2.last ' + x0, h), path(r ' + x1, h), path(r ' + x2, h), h[x2.last].nxt ∈ h, ¬ dups(x0), ¬ dups(x1), ¬ dups(x2), ¬ x2.last ∈ x, ¬ x2.last ∈ x0, ¬ r ∈ x1, ¬ r ∈ x2 ⊦

• Proof step 208:

  x + h[x2.last].nxt ' = x2 + r1 ' + x3, (x2.last ' + x0).last = (r ' + x).last, x1.last = (r ' + x).last, x2.last ≠ r, h[x2.last].nxt ≠ null, x1 ≠ [], x2 ≠ [], path(r ' + x2 + r1 ' + x3, h), path(x2.last ' + x0, h), path(r ' + x1, h), path(r ' + x2, h), h[x2.last].nxt ∈ h, ¬ dups(x0), ¬ dups(x1), ¬ dups(x2), ¬ x2.last ∈ x, ¬ x2.last ∈ x0, ¬ r ∈ x1, ¬ r ∈ x2 ⊦

Rule argument

Additional information

Used terms: x1, r '

Proof step 205 from proof rem-stays-reachable-aux2 (previous step) (back to tree)

A spec-lemma

Proof step 206 from proof rem-stays-reachable-aux2 (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 207:

  x + h[x2.last].nxt ' = x2 + r1 ' + x3, (x2.last ' + x0).last = ((x2.last ' + x0).last ' + x).last, (x2.last ' + x0).last ≠ null, x2.last ≠ (x2.last ' + x0).last, h[x2.last].nxt ≠ null, x2 ≠ [], path((x2.last ' + x0).last ' + x2, h), path((x2.last ' + x0).last ' + x2 + r1 ' + x3, h), path(x2.last ' + x0, h), (x2.last ' + x0).last ∈ h, h[x2.last].nxt ∈ h, ¬ dups(x2), ¬ dups(x0), ¬ (x2.last ' + x0).last ∈ x2, ¬ x2.last ∈ x0, ¬ x2.last ∈ x ⊦

Rule argument

Additional information

Used simplifier rules: path-one: ⊦ path(r ', h) ↔ r ∈ h ∧ r ≠ null; ⊦ ¬ a ∈ []; (s) ⊦ ¬ dups([]); (s) a: ⊦ (x + y) + z = x + y + z; from specification polylist ⊦ x + [] = x; (s) ⊦ a '.last = a; (s)

Proof step 207 from proof rem-stays-reachable-aux2 (previous step) (back to tree)

User applied rule apply elim lemma

And closed the goal!

Rule argument

Additional information

Used simplifier rules: ⊦ x + a ' ≠ []; (s) ⊦ dups(x + a ') ↔ a ∈ x ∨ dups(x); (ws) ⊦ a ∈ a0 ' ↔ a = a0; (s) ⊦ a ∈ x + y ↔ a ∈ x ∨ a ∈ y; (s) ⊦ a ∈ a0 ' + x ↔ a = a0 ∨ a ∈ x; (s) ⊦ ¬ a0 ∈ y ∧ a0 ≠ a → y + a ' ≠ y0 + a0 ' + z; (s) in-15: ⊦ x + a ' = y → a ∈ y; (forward) from specification polylist ⊦ ¬ a ∈ x → (x + a ' = y + a ' + z ↔ y = x ∧ z = []); (ws) ⊦ a ' + x ≠ []; (s) a: ⊦ (x + y) + z = x + y + z; from specification polylist x ≠ [] ⊦ a = x.last ∧ y = x.butlast ↔ x = y + a '; (elim) Used terms: x2, a, y

Proof step 208 from proof rem-stays-reachable-aux2 (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 209:

  x + h[x2.last].nxt ' = x2 + r1 ' + x3, x1.last = (r ' + x).last, (x2.last ' + x0).last = x1.last, x2.last ≠ r, h[x2.last].nxt ≠ null, x1 ≠ [], x2 ≠ [], path(r ' + x2, h), path(r ' + x1, h), path(x2.last ' + x0, h), path(r ' + x2 + r1 ' + x3, h), h[x2.last].nxt ∈ h, ¬ dups(x0), ¬ dups(x1), ¬ dups(x2), ¬ x2.last ∈ x, ¬ x2.last ∈ x0, ¬ r ∈ x1, ¬ r ∈ x2 ⊦

Rule argument

Additional information

Proof step 209 from proof rem-stays-reachable-aux2 (previous step) (back to tree)

User applied rule apply elim lemma

And obtained the following new goals

• Proof step 210:

  x + h[x2.last].nxt ' = x2 + r1 ' + x3, (x2.last ' + x0).last = r0, r0 = (r ' + x).last, x1 = y + r0 ', x2.last ≠ r, h[x2.last].nxt ≠ null, x1 ≠ [], x2 ≠ [], path(r ' + x2 + r1 ' + x3, h), path(x2.last ' + x0, h), path(r ' + x1, h), path(r ' + x2, h), h[x2.last].nxt ∈ h, ¬ dups(x0), ¬ dups(x1), ¬ dups(x2), ¬ x2.last ∈ x, ¬ x2.last ∈ x0, ¬ r ∈ x1, ¬ r ∈ x2 ⊦

Rule argument

Additional information

Used simplifier rules: x ≠ [] ⊦ a = x.last ∧ y = x.butlast ↔ x = y + a '; (elim) Used terms: x1, a, y

Proof step 210 from proof rem-stays-reachable-aux2 (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 211:

  x + h[x2.last].nxt ' = x2 + r1 ' + x3, (x2.last ' + x0).last = (r ' + x).last, x2.last ≠ r, h[x2.last].nxt ≠ null, r ≠ (r ' + x).last, x2 ≠ [], path(r ' + x2 + r1 ' + x3, h), path(x2.last ' + x0, h), path(r ' + y + (r ' + x).last ', h), path(r ' + x2, h), h[x2.last].nxt ∈ h, ¬ dups(x2), ¬ dups(y), ¬ dups(x0), ¬ r ∈ y, ¬ x2.last ∈ x0, ¬ x2.last ∈ x, ¬ (r ' + x).last ∈ y, ¬ r ∈ x2, h[x2.last].nxt ∈ x2 ∨ h[x2.last].nxt = r1 ∨ h[x2.last].nxt ∈ x3 ⊦

Rule argument

Additional information

Used simplifier rules: a: ⊦ (x + y) + z = x + y + z; from specification polylist ⊦ a ∈ a0 ' + x ↔ a = a0 ∨ a ∈ x; (s) ⊦ a ∈ x + y ↔ a ∈ x ∨ a ∈ y; (s) in-15: ⊦ x + a ' = y → a ∈ y; (forward) from specification polylist ⊦ a ∈ a0 ' ↔ a = a0; (s) ⊦ dups(x + a ') ↔ a ∈ x ∨ dups(x); (ws) ⊦ x + a ' ≠ []; (s)

Proof step 211 from proof rem-stays-reachable-aux2 (previous step) (back to tree)

User applied rule apply elim lemma

And closed the goal!

Rule argument

Additional information

Used simplifier rules: ⊦ x + a ' ≠ []; (s) ⊦ dups(x + a ') ↔ a ∈ x ∨ dups(x); (ws) ⊦ a ∈ a0 ' ↔ a = a0; (s) ⊦ a ∈ x + y ↔ a ∈ x ∨ a ∈ y; (s) ⊦ a ∈ a0 ' + x ↔ a = a0 ∨ a ∈ x; (s) ⊦ ¬ a0 ∈ y ∧ a0 ≠ a → y + a ' ≠ y0 + a0 ' + z; (s) in-15: ⊦ x + a ' = y → a ∈ y; (forward) from specification polylist ⊦ ¬ a ∈ x → (x + a ' = y + a ' + z ↔ y = x ∧ z = []); (ws) ⊦ a ' + x ≠ []; (s) a: ⊦ (x + y) + z = x + y + z; from specification polylist x ≠ [] ⊦ a = x.last ∧ y = x.butlast ↔ x = y + a '; (elim) Used terms: x2, a, y0

Proof step 212 from proof rem-stays-reachable-aux2 (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 213:

  h[r0].nxt ≠ null, r0 ≠ r, path(r ' + x + h[r0].nxt ', h), reachable(r, r0, h), h[r0].nxt ∈ h, ¬ reachable(r, (r ' + x).last, h), ¬ r0 ∈ x ⊦

Rule argument

Additional information

Proof step 213 from proof rem-stays-reachable-aux2 (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 214:

  ⊦ reachable(r, r0, h) ↔ (∃ x. path(r ' + x, h) ∧ (r ' + x).last = r0)

• Proof step 215:

  h[r0].nxt ≠ null, r0 ≠ r, path(r ' + x + h[r0].nxt ', h), reachable(r, r0, h), h[r0].nxt ∈ h, ¬ r0 ∈ x, ∀ x0. ¬(path(r ' + x0, h) ∧ (r ' + x0).last = (r ' + x).last) ⊦

Rule argument

Additional information

Used terms: h, (r ' + x).last, r

Proof step 214 from proof rem-stays-reachable-aux2 (previous step) (back to tree)

Lemma reachable-def

Proof step 215 from proof rem-stays-reachable-aux2 (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 216:

  h[r0].nxt ≠ null, r0 ≠ r, path(r ' + x + h[r0].nxt ', h), reachable(r, r0, h), h[r0].nxt ∈ h, ¬ r0 ∈ x, ∀ x0. ¬ path(r ' + x0, h) ∨ (r ' + x0).last ≠ (r ' + x).last ⊦

Rule argument

Additional information

Proof step 216 from proof rem-stays-reachable-aux2 (previous step) (back to tree)

Heuristic quantifier closing applied rule all left

And closed the goal!

Rule argument

Additional information

Used simplifier rules: path-butlast: ⊦ path(r ' + x + r0 ', h) → (path(r ' + x, h) ↔ true); a: ⊦ (x + y) + z = x + y + z; from specification polylist Used terms: x