Proof step 1 from proof reach-reachnext (conclusion) (back to tree)

System applied rule normalize

And obtained the following new goals

• Proof step 2:

  ¬(reachable(r, h[r1].nxt, h) ↔ ¬(h[r1].nxt = null ∨ ¬ h[r1].nxt ∈ h)), reachable(r, r1, h) ⊦

Rule argument

Additional information

Proof step 2 from proof reach-reachnext (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 3:

  ¬(reachable(r, h[r1].nxt, h) ↔ h[r1].nxt ≠ null ∧ h[r1].nxt ∈ h), reachable(r, r1, h) ⊦

Rule argument

Additional information

Proof step 3 from proof reach-reachnext (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 4:

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

• Proof step 5:

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

Rule argument

Additional information

Used terms: h, r1, r

Proof step 4 from proof reach-reachnext (previous step) (back to tree)

Lemma reachable-def

Proof step 5 from proof reach-reachnext (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 6:

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

Rule argument

Additional information

Proof step 6 from proof reach-reachnext (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 7:

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

• Proof step 8:

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

Rule argument

Additional information

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

Proof step 7 from proof reach-reachnext (previous step) (back to tree)

Lemma reachable-def

Proof step 8 from proof reach-reachnext (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 9:

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

Rule argument

Additional information

Proof step 9 from proof reach-reachnext (previous step) (back to tree)

User applied rule case distinction

And obtained the following new goals

• Proof step 10:

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

• Proof step 20:

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

Rule argument

Additional information

Proof step 10 from proof reach-reachnext (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 11:

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

Rule argument

Additional information

Proof step 11 from proof reach-reachnext (previous step) (back to tree)

User applied rule structural induction

And obtained the following new goals

• Proof step 12:

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

• Proof step 16:

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

Rule argument

Additional information

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

Proof step 12 from proof reach-reachnext (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 13:

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

Rule argument

Additional information

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

Proof step 13 from proof reach-reachnext (previous step) (back to tree)

User applied rule structural induction

And obtained the following new goals

• Proof step 14:

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

Rule argument

Additional information

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

Proof step 14 from proof reach-reachnext (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 15:

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

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 list[reflist] ⊦ a + x = a ' + x; (s) ⊦ (b ' + a ' + x).last = (a ' + x).last; (s)

Proof step 15 from proof reach-reachnext (previous step) (back to tree)

User applied rule constructor cut

And closed the goal!

Rule argument

Additional information

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

Proof step 16 from proof reach-reachnext (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 17:

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

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 list[reflist] ⊦ a + x = a ' + x; (s) ⊦ (b ' + a ' + x).last = (a ' + x).last; (s)

Proof step 17 from proof reach-reachnext (previous step) (back to tree)

User applied rule constructor cut

And obtained the following new goals

• Proof step 18:

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

Rule argument

Additional information

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

Proof step 18 from proof reach-reachnext (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 19:

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

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 list[reflist] ⊦ (b ' + a ' + x).last = (a ' + x).last; (s) ⊦ a + x = a ' + x; (s)

Proof step 19 from proof reach-reachnext (previous step) (back to tree)

User applied rule all left

And closed the goal!

Rule argument

Additional information

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

Proof step 20 from proof reach-reachnext (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 21:

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

Rule argument

Additional information

Proof step 21 from proof reach-reachnext (previous step) (back to tree)

User applied rule exists right

And obtained the following new goals

• Proof step 22:

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

Rule argument

Additional information

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

Proof step 22 from proof reach-reachnext (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 23:

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

Rule argument

Additional information

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

Proof step 23 from proof reach-reachnext (previous step) (back to tree)

User applied rule structural induction

And obtained the following new goals

• Proof step 24:

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

Rule argument

Additional information

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

Proof step 24 from proof reach-reachnext (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 25:

  h[(h[r].nxt ' + x0).last].nxt ≠ null, r ≠ null, path(h[r].nxt ' + x0, h), r ∈ h, h[(h[r].nxt ' + x0).last].nxt ∈ h, ¬ path(h[r].nxt ' + x0 + h[(h[r].nxt ' + x0).last].nxt ', h), ∀ h0, r1. h0[(r1 ' + x0).last].nxt = null ∨ ¬ path(r1 ' + x0, h0) ∨ ¬ h0[(r1 ' + x0).last].nxt ∈ h0 ∨ path(r1 ' + x0 + h0[(r1 ' + x0).last].nxt ', h0) ⊦

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 list[reflist] ⊦ (b ' + a ' + x).last = (a ' + x).last; (s) ⊦ a + x = a ' + x; (s)

Proof step 25 from proof reach-reachnext (previous step) (back to tree)

Heuristic quantifier closing applied rule all left

And closed the goal!

Rule argument

Additional information

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