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: List[A] 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 polylist ⊦ 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; List[A] freely generated by [], +; ⊦ a '.last = a; (s) ⊦ x + [] = x; (s) a: ⊦ (x + y) + z = x + y + z; from specification polylist

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 polylist ⊦ 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); List[A] 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 polylist ⊦ 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 polylist ⊦ 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; List[A] freely generated by [], +; ⊦ x + [] = x; (s) a: ⊦ (x + y) + z = x + y + z; from specification polylist ⊦ 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 polylist ⊦ (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 polylist ⊦ (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; List[A] freely generated by [], +; ⊦ x + [] = x; (s) ⊦ a '.last = a; (s) ⊦ [] + x = x; (s) a: ⊦ (x + y) + z = x + y + z; from specification polylist

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 polylist ⊦ (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 polylist Used terms: h, (h(r)).nxt