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

System applied rule normalize

And obtained the following new goals

• Proof step 2:

  n ≠ 0 ⊦ reachable-n(h, n, r, r0) ↔ (∃ x. path(x, h) ∧ x.head = r ∧ x.last = r0 ∧ # x = n + 1)

Rule argument

Additional information

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

User applied rule structural induction

And obtained the following new goals

• Proof step 3:

  n0 +1 ≠ 0, ∀ h, r, r0. n0 ≠ 0 → (reachable-n(h, n0, r, r0) ↔ (∃ x. path(x, h) ∧ x.head = r ∧ x.last = r0 ∧ # x = n0 + 1)) ⊦ reachable-n(h, n0 +1, r, r0) ↔ (∃ x. path(x, h) ∧ x.head = r ∧ x.last = r0 ∧ # x = n0 +1 + 1)

Rule argument

Additional information

Used simplifier rules: nat freely generated by 0, +1;;

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

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 4:

  n0 ≠ 0 → (∀ h, r, r0. reachable-n(h, n0, r, r0) ↔ (∃ x. path(x, h) ∧ x.head = r ∧ x.last = r0 ∧ # x = n0 + 1)) ⊦ (∃ r1. reachable-1(h, r, r1) ∧ reachable-n(h, n0, r1, r0)) ↔ (∃ x. path(x, h) ∧ x.head = r ∧ x.last = r0 ∧ # x = 2 + n0)

Rule argument

Additional information

Used simplifier rules: reachable-n-rec: ⊦ reachable-n(h, n + 1, r, r0) ↔ (∃ r1. reachable-1(h, r, r1) ∧ reachable-n(h, n, r1, r0)); a: ⊦ (m + n0) + n1 = m + n0 + n1; from specification nat-basic c: ⊦ m + n = n + m; from specification nat-basic ⊦ m +1 = m + 1; (s) ⊦ m + 1 ≠ 0; (s)

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

User applied rule constructor cut

And obtained the following new goals

• Proof step 5:

  n0 = 0, n0 ≠ 0 → (∀ h, r, r0. reachable-n(h, n0, r, r0) ↔ (∃ x. path(x, h) ∧ x.head = r ∧ x.last = r0 ∧ # x = n0 + 1)) ⊦ (∃ r1. reachable-1(h, r, r1) ∧ reachable-n(h, n0, r1, r0)) ↔ (∃ x. path(x, h) ∧ x.head = r ∧ x.last = r0 ∧ # x = 2 + n0)

• Proof step 16:

  n0 = n +1, n0 ≠ 0 → (∀ h, r, r0. reachable-n(h, n0, r, r0) ↔ (∃ x. path(x, h) ∧ x.head = r ∧ x.last = r0 ∧ # x = n0 + 1)) ⊦ (∃ r1. reachable-1(h, r, r1) ∧ reachable-n(h, n0, r1, r0)) ↔ (∃ x. path(x, h) ∧ x.head = r ∧ x.last = r0 ∧ # x = 2 + n0)

Rule argument

Additional information

Used simplifier rules: nat freely generated by 0, +1;;

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

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 6:

  ⊦ reachable-1(h, r, r0) ↔ (∃ x. path(x, h) ∧ x.head = r ∧ x.last = r0 ∧ # x = 2)

Rule argument

Additional information

Used simplifier rules: reachable-n-base: ⊦ reachable-n(h, 0, r, r0) ↔ r = r0;

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

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 7:

  ⊦ reachable-1(h, r, r0) ↔ r ≠ null ∧ r0 ≠ null ∧ r ∈ h ∧ r0 ∈ h ∧ h[r].nxt = r0

• Proof step 8:

  ⊦ r ≠ null ∧ r0 ≠ null ∧ r ∈ h ∧ r0 ∈ h ∧ h[r].nxt = r0 ↔ (∃ x. path(x, h) ∧ x.head = r ∧ x.last = r0 ∧ # x = 2)

Rule argument

Additional information

Used terms: r0, r, h

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

Lemma reachable-1-def

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

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 9:

  ⊦ r ≠ null ∧ h[r].nxt ≠ null ∧ r ∈ h ∧ h[r].nxt ∈ h ∧ h[r].nxt = r0 ↔ (∃ x. path(x, h) ∧ x.head = r ∧ x.last = r0 ∧ # x = 2)

Rule argument

Additional information

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

User applied rule case distinction

And obtained the following new goals

• Proof step 10:

  h[r].nxt = r0, h[r].nxt ≠ null, r ≠ null, r ∈ h, h[r].nxt ∈ h ⊦ ∃ x. path(x, h) ∧ x.head = r ∧ x.last = r0 ∧ # x = 2

• Proof step 12:

  ∃ x. path(x, h) ∧ x.head = r ∧ x.last = r0 ∧ # x = 2 ⊦ r ≠ null ∧ h[r].nxt ≠ null ∧ r ∈ h ∧ h[r].nxt ∈ h ∧ h[r].nxt = r0

Rule argument

Additional information

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

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 11:

  h[r].nxt ≠ null, r ≠ null, h[r].nxt ∈ h, r ∈ h ⊦ ∃ x. path(x, h) ∧ x.head = r ∧ x.last = h[x.head].nxt ∧ # x = 2

Rule argument

Additional information

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

User applied rule exists right

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; ⊦ (x + a ').last = a; (s) ⊦ (a ' + x).head = a; (s) ⊦ #(x + y) = # x + # y; (s) ⊦ # a ' = 0 +1; (s) a: ⊦ (x + y) + z = x + y + z; from specification polylist Used terms: r ' + h[r].nxt '

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

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 13:

  # x = 2, path(x, h) ⊦ x.head ≠ null ∧ h[x.head].nxt ≠ null ∧ x.head ∈ h ∧ h[x.head].nxt ∈ h ∧ h[x.head].nxt = x.last

Rule argument

Additional information

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

Heuristic elimination applied rule apply elim lemma

And obtained the following new goals

• Proof step 14:

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

Rule argument

Additional information

Used simplifier rules: ⊦ # [] = 0; (s) x ≠ [] ⊦ a = x.head ∧ y = x.tail ↔ x = a + y; (elim) Used terms: x, a, y

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

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 15:

  1 = # y, r ≠ null, path(r ' + y, h) ⊦ h[r].nxt = y.head ∧ h[r].nxt ∈ h ∧ h[r].nxt ≠ null

Rule argument

Additional information

Used simplifier rules: path-first-in-H: ⊦ path(r ' + x, h) → (r ∈ h ↔ true); null-not-start-of-path: ⊦ ¬ path(null ' + x, h); a: ⊦ (x + y) + z = x + y + z; from specification polylist ⊦ # x = 1 → (y + x).last = x.head; (s) ⊦ a + x = a ' + x; (s) ⊦ a ' + x ≠ []; (s) c: ⊦ m + n = n + m; from specification nat-basic a: ⊦ (m + n0) + n1 = m + n0 + n1; from specification nat-basic n0 < n ⊦ (* n) = m0 + (* n0) ↔ n - n0 = m0; (s) ⊦ # a ' = 0 +1; (s) ⊦ #(x + y) = # x + # y; (s)

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

Heuristic elimination applied rule apply elim lemma

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-first-in-H: ⊦ path(r ' + x, h) → (r ∈ h ↔ true); path-one: ⊦ path(r ', h) ↔ r ∈ h ∧ r ≠ null; ⊦ #(x + y) = # x + # y; (s) ⊦ # a ' = 0 +1; (s) ⊦ 1 = m + 1 ↔ m = 0; (s) ⊦ # x = 0 ↔ x = []; (s) a: ⊦ (m + n0) + n1 = m + n0 + n1; from specification nat-basic c: ⊦ m + n = n + m; from specification nat-basic ⊦ a ' + x ≠ []; (s) ⊦ a + x = a ' + x; (s) ⊦ x + [] = x; (s) a: ⊦ (x + y) + z = x + y + z; from specification polylist ⊦ # [] = 0; (s) x ≠ [] ⊦ a = x.head ∧ y = x.tail ↔ x = a + y; (elim) Used terms: y, a, y0

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

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 17:

  ∀ h0, r1, r2. (∃ r3. reachable-1(h0, r1, r3) ∧ reachable-n(h0, n, r3, r2)) ↔ (∃ x. path(x, h0) ∧ x.head = r1 ∧ x.last = r2 ∧ # x = 2 + n) ⊦ (∃ r1. reachable-1(h, r, r1) ∧ (∃ r2. reachable-1(h, r1, r2) ∧ reachable-n(h, n, r2, r0))) ↔ (∃ x. path(x, h) ∧ x.head = r ∧ x.last = r0 ∧ # x = 3 + n)

Rule argument

Additional information

Used simplifier rules: reachable-n-rec: ⊦ reachable-n(h, n + 1, r, r0) ↔ (∃ r1. reachable-1(h, r, r1) ∧ reachable-n(h, n, r1, r0)); a: ⊦ (m + n0) + n1 = m + n0 + n1; from specification nat-basic c: ⊦ m + n = n + m; from specification nat-basic ⊦ m +1 = m + 1; (s) ⊦ m + 1 ≠ 0; (s)

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

User applied rule case distinction

And obtained the following new goals

• Proof step 18:

  ∀ h0, r1, r2. (∃ r3. reachable-1(h0, r1, r3) ∧ reachable-n(h0, n, r3, r2)) ↔ (∃ x. path(x, h0) ∧ x.head = r1 ∧ x.last = r2 ∧ # x = 2 + n), ∃ r1. reachable-1(h, r, r1) ∧ (∃ r2. reachable-1(h, r1, r2) ∧ reachable-n(h, n, r2, r0)) ⊦ ∃ x. path(x, h) ∧ x.head = r ∧ x.last = r0 ∧ # x = 3 + n

• Proof step 45:

  ∀ h0, r1, r2. (∃ r3. reachable-1(h0, r1, r3) ∧ reachable-n(h0, n, r3, r2)) ↔ (∃ x. path(x, h0) ∧ x.head = r1 ∧ x.last = r2 ∧ # x = 2 + n), ∃ x. path(x, h) ∧ x.head = r ∧ x.last = r0 ∧ # x = 3 + n ⊦ ∃ r1. reachable-1(h, r, r1) ∧ (∃ r2. reachable-1(h, r1, r2) ∧ reachable-n(h, n, r2, r0))

Rule argument

Additional information

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

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 19:

  reachable-1(h, r, r1), reachable-1(h, r1, r2), reachable-n(h, n, r2, r0), ∀ h0, r1, r2. (∃ r3. reachable-1(h0, r1, r3) ∧ reachable-n(h0, n, r3, r2)) ↔ (∃ x. path(x, h0) ∧ x.head = r1 ∧ x.last = r2 ∧ # x = 2 + n) ⊦ ∃ x. path(x, h) ∧ x.head = r ∧ x.last = r0 ∧ # x = 3 + n

Rule argument

Additional information

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

User applied rule constructor cut

And obtained the following new goals

• Proof step 20:

  n = 0, reachable-1(h, r1, r2), reachable-1(h, r, r1), reachable-n(h, n, r2, r0), ∀ h0, r1, r2. (∃ r3. reachable-1(h0, r1, r3) ∧ reachable-n(h0, n, r3, r2)) ↔ (∃ x. path(x, h0) ∧ x.head = r1 ∧ x.last = r2 ∧ # x = 2 + n) ⊦ ∃ x. path(x, h) ∧ x.head = r ∧ x.last = r0 ∧ # x = 3 + n

• Proof step 28:

  n = n0 +1, reachable-1(h, r1, r2), reachable-1(h, r, r1), reachable-n(h, n, r2, r0), ∀ h0, r1, r2. (∃ r3. reachable-1(h0, r1, r3) ∧ reachable-n(h0, n, r3, r2)) ↔ (∃ x. path(x, h0) ∧ x.head = r1 ∧ x.last = r2 ∧ # x = 2 + n) ⊦ ∃ x. path(x, h) ∧ x.head = r ∧ x.last = r0 ∧ # x = 3 + n

Rule argument

Additional information

Used simplifier rules: nat freely generated by 0, +1;;

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

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 21:

  reachable-1(h, r1, r0), reachable-1(h, r, r1), ∀ h0, r3, r4. reachable-1(h0, r3, r4) ↔ (∃ x. path(x, h0) ∧ x.head = r3 ∧ x.last = r4 ∧ # x = 2) ⊦ ∃ x. path(x, h) ∧ x.head = r ∧ x.last = r0 ∧ # x = 3

Rule argument

Additional information

Used simplifier rules: reachable-n-base: ⊦ reachable-n(h, 0, r, r0) ↔ r = r0;

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

User applied rule exists right

And obtained the following new goals

• Proof step 22:

  reachable-1(h, r, r1), reachable-1(h, r1, r0), ∀ h0, r3, r4. reachable-1(h0, r3, r4) ↔ (∃ x. path(x, h0) ∧ x.head = r3 ∧ x.last = r4 ∧ # x = 2) ⊦ path(r ' + r1 ' + r0 ', h) ∧ (r ' + r1 ' + r0 ').head = r ∧ (r ' + r1 ' + r0 ').last = r0 ∧ #(r ' + r1 ' + r0 ') = 3

Rule argument

Additional information

Used terms: r ' + r1 ' + r0 '

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

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 23:

  reachable-1(h, r1, r0), reachable-1(h, r, r1), ∀ h0, r3, r4. reachable-1(h0, r3, r4) ↔ (∃ x. path(x, h0) ∧ x.head = r3 ∧ x.last = r4 ∧ # x = 2) ⊦ r ∈ h ∧ r ≠ null ∧ h[r].nxt = r1 ∧ h[r].nxt ∈ h ∧ h[h[r].nxt].nxt ∈ h ∧ h[r].nxt ≠ null ∧ h[h[r].nxt].nxt ≠ null ∧ h[h[r].nxt].nxt = r0

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-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 ⊦ # a ' = 0 +1; (s) ⊦ #(x + y) = # x + # y; (s) ⊦ (x + a ').last = a; (s) ⊦ (b ' + a ' + x).last = (a ' + x).last; (s) ⊦ (a ' + x).head = a; (s)

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

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 24:

  ⊦ reachable-1(h, r, r0) ↔ r ≠ null ∧ r0 ≠ null ∧ r ∈ h ∧ r0 ∈ h ∧ h[r].nxt = r0

• Proof step 25:

  h[r].nxt = r1, r ≠ null, r1 ≠ null, reachable-1(h, r1, r0), r ∈ h, r1 ∈ h, ∀ h0, r3, r4. reachable-1(h0, r3, r4) ↔ (∃ x. path(x, h0) ∧ x.head = r3 ∧ x.last = r4 ∧ # x = 2) ⊦ r ∈ h ∧ r ≠ null ∧ h[r].nxt = r1 ∧ h[r].nxt ∈ h ∧ h[h[r].nxt].nxt ∈ h ∧ h[r].nxt ≠ null ∧ h[h[r].nxt].nxt ≠ null ∧ h[h[r].nxt].nxt = r0

Rule argument

Additional information

Used terms: r1, r, h

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

Lemma reachable-1-def

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

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 26:

  h[r].nxt ≠ null, r ≠ null, reachable-1(h, h[r].nxt, r0), h[r].nxt ∈ h, r ∈ h, ∀ h0, r3, r4. reachable-1(h0, r3, r4) ↔ (∃ x. path(x, h0) ∧ x.head = r3 ∧ x.last = r4 ∧ # x = 2) ⊦ h[h[r].nxt].nxt ∈ h ∧ h[h[r].nxt].nxt ≠ null ∧ h[h[r].nxt].nxt = r0

Rule argument

Additional information

Proof step 26 from proof reach-n-path-n (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 27:

  ⊦ reachable-1(h, r, r0) ↔ r ≠ null ∧ r0 ≠ null ∧ r ∈ h ∧ r0 ∈ h ∧ h[r].nxt = r0

Rule argument

Additional information

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

Proof step 27 from proof reach-n-path-n (previous step) (back to tree)

Lemma reachable-1-def

Proof step 28 from proof reach-n-path-n (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 29:

  reachable-1(h, r, r1), reachable-1(h, r1, r2), reachable-1(h, r2, r3), reachable-n(h, n0, r3, r0), ∀ h0, r4, r5. (∃ r6. reachable-1(h0, r4, r6) ∧ (∃ r1. reachable-1(h0, r6, r1) ∧ reachable-n(h0, n0, r1, r5))) ↔ (∃ x. path(x, h0) ∧ x.head = r4 ∧ x.last = r5 ∧ # x = 3 + n0) ⊦ ∃ x. path(x, h) ∧ x.head = r ∧ x.last = r0 ∧ # x = 4 + n0

Rule argument

Additional information

Used simplifier rules: reachable-n-rec: ⊦ reachable-n(h, n + 1, r, r0) ↔ (∃ r1. reachable-1(h, r, r1) ∧ reachable-n(h, n, r1, r0)); a: ⊦ (m + n0) + n1 = m + n0 + n1; from specification nat-basic c: ⊦ m + n = n + m; from specification nat-basic ⊦ m +1 = m + 1; (s)

Proof step 29 from proof reach-n-path-n (previous step) (back to tree)

User applied rule all left

And obtained the following new goals

• Proof step 30:

  reachable-1(h, r2, r3), reachable-1(h, r1, r2), reachable-1(h, r, r1), reachable-n(h, n0, r3, r0), (∃ r6. reachable-1(h, r1, r6) ∧ (∃ r1. reachable-1(h, r6, r1) ∧ reachable-n(h, n0, r1, r0))) ↔ (∃ x. path(x, h) ∧ x.head = r1 ∧ x.last = r0 ∧ # x = 3 + n0) ⊦ ∃ x. path(x, h) ∧ x.head = r ∧ x.last = r0 ∧ # x = 4 + n0

Rule argument

Additional information

Used terms: h, r1, r0

Proof step 30 from proof reach-n-path-n (previous step) (back to tree)

User applied rule case distinction

And obtained the following new goals

• Proof step 31:

  reachable-1(h, r, r1), reachable-1(h, r1, r2), reachable-1(h, r2, r3), reachable-n(h, n0, r3, r0) ⊦ ∃ x. path(x, h) ∧ x.head = r ∧ x.last = r0 ∧ # x = 4 + n0, ∃ x. path(x, h) ∧ x.head = r1 ∧ x.last = r0 ∧ # x = 3 + n0, ∃ r6. reachable-1(h, r1, r6) ∧ (∃ r1. reachable-1(h, r6, r1) ∧ reachable-n(h, n0, r1, r0))

• Proof step 34:

  reachable-1(h, r, r1), reachable-1(h, r1, r2), reachable-1(h, r2, r3), reachable-n(h, n0, r3, r0), ∃ x. path(x, h) ∧ x.head = r1 ∧ x.last = r0 ∧ # x = 3 + n0, ∃ r6. reachable-1(h, r1, r6) ∧ (∃ r1. reachable-1(h, r6, r1) ∧ reachable-n(h, n0, r1, r0)) ⊦ ∃ x. path(x, h) ∧ x.head = r ∧ x.last = r0 ∧ # x = 4 + n0

Rule argument

Additional information

Proof step 31 from proof reach-n-path-n (previous step) (back to tree)

User applied rule exists right

And obtained the following new goals

• Proof step 32:

  reachable-1(h, r2, r3), reachable-1(h, r1, r2), reachable-1(h, r, r1), reachable-n(h, n0, r3, r0) ⊦ ∃ x. path(x, h) ∧ x.head = r1 ∧ x.last = r0 ∧ # x = 3 + n0, ∃ x. path(x, h) ∧ x.head = r ∧ x.last = r0 ∧ # x = 4 + n0, reachable-1(h, r1, r2) ∧ (∃ r1. reachable-1(h, r2, r1) ∧ reachable-n(h, n0, r1, r0))

Rule argument

Additional information

Used terms: r2

Proof step 32 from proof reach-n-path-n (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 33:

  reachable-1(h, r, r1), reachable-1(h, r1, r2), reachable-1(h, r2, r3), reachable-n(h, n0, r3, r0) ⊦ ∃ x. path(x, h) ∧ x.head = r ∧ x.last = r0 ∧ # x = 4 + n0, ∃ x. path(x, h) ∧ x.head = r1 ∧ x.last = r0 ∧ # x = 3 + n0, ∃ r1. reachable-1(h, r2, r1) ∧ reachable-n(h, n0, r1, r0)

Rule argument

Additional information

Proof step 33 from proof reach-n-path-n (previous step) (back to tree)

Heuristic quantifier closing applied rule exists right

And closed the goal!

Rule argument

Additional information

Used terms: r3

Proof step 34 from proof reach-n-path-n (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 35:

  # x = 3 + n0, path(x, h), reachable-1(h, x.head, r6), reachable-1(h, r6, r4), reachable-1(h, r2, r3), reachable-1(h, x.head, r2), reachable-1(h, r, x.head), reachable-n(h, n0, r4, x.last), reachable-n(h, n0, r3, x.last) ⊦ ∃ x0. path(x0, h) ∧ x0.head = r ∧ x0.last = x.last ∧ # x0 = 4 + n0

Rule argument

Additional information

Proof step 35 from proof reach-n-path-n (previous step) (back to tree)

Heuristic elimination applied rule apply elim lemma

And obtained the following new goals

• Proof step 36:

  # x = 3 + n0, x = r0 + y, x ≠ [], path(x, h), reachable-1(h, r, r0), reachable-1(h, r0, r2), reachable-1(h, r2, r3), reachable-1(h, r6, r4), reachable-1(h, r0, r6), reachable-n(h, n0, r3, x.last), reachable-n(h, n0, r4, x.last) ⊦ ∃ x0. path(x0, h) ∧ x0.head = r ∧ x0.last = x.last ∧ # x0 = 4 + n0

Rule argument

Additional information

Used simplifier rules: ⊦ # [] = 0; (s) ⊦ m + n = 0 ↔ m = 0 ∧ n = 0; (ws) a: ⊦ (m + n0) + n1 = m + n0 + n1; from specification nat-basic c: ⊦ m + n = n + m; from specification nat-basic x ≠ [] ⊦ a = x.head ∧ y = x.tail ↔ x = a + y; (elim) Used terms: x, a, y

Proof step 36 from proof reach-n-path-n (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 37:

  1 + # y = 3 + n0, path(r0 ' + y, h), reachable-1(h, r0, r6), reachable-1(h, r6, r4), reachable-1(h, r2, r3), reachable-1(h, r0, r2), reachable-1(h, r, r0), reachable-n(h, n0, r4, (r0 ' + y).last), reachable-n(h, n0, r3, (r0 ' + y).last) ⊦ ∃ x0. path(x0, h) ∧ x0.head = r ∧ x0.last = (r0 ' + y).last ∧ # x0 = 4 + n0

Rule argument

Additional information

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

Proof step 37 from proof reach-n-path-n (previous step) (back to tree)

Heuristic weak cut applied rule cut formula

And obtained the following new goals

• Proof step 38:

  1 + # y = 3 + n0, y = [], path(r0 ' + y, h), reachable-1(h, r, r0), reachable-1(h, r0, r2), reachable-1(h, r2, r3), reachable-1(h, r6, r4), reachable-1(h, r0, r6), reachable-n(h, n0, r3, (r0 ' + y).last), reachable-n(h, n0, r4, (r0 ' + y).last) ⊦ ∃ x0. path(x0, h) ∧ x0.head = r ∧ x0.last = (r0 ' + y).last ∧ # x0 = 4 + n0

• Proof step 39:

  1 + # y = 3 + n0, y ≠ [], path(r0 ' + y, h), reachable-1(h, r, r0), reachable-1(h, r0, r2), reachable-1(h, r2, r3), reachable-1(h, r6, r4), reachable-1(h, r0, r6), reachable-n(h, n0, r3, (r0 ' + y).last), reachable-n(h, n0, r4, (r0 ' + y).last) ⊦ ∃ x0. path(x0, h) ∧ x0.head = r ∧ x0.last = (r0 ' + y).last ∧ # x0 = 4 + n0

Rule argument

Additional information

Used formulas: y = []

Proof step 38 from proof reach-n-path-n (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And closed the goal!

Rule argument

Additional information

Used simplifier rules: c: ⊦ m + n = n + m; from specification nat-basic a: ⊦ (m + n0) + n1 = m + n0 + n1; from specification nat-basic n < n0 ⊦ (* n) ≠ m0 + (* n0); (s) ⊦ # [] = 0; (s)

Proof step 39 from proof reach-n-path-n (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 40:

  1 + # y = 3 + n0, y ≠ [], path(r0 ' + y, h), reachable-1(h, r0, r6), reachable-1(h, r6, r4), reachable-1(h, r2, r3), reachable-1(h, r0, r2), reachable-1(h, r, r0), reachable-n(h, n0, r4, y.last), reachable-n(h, n0, r3, y.last) ⊦ ∃ x0. path(x0, h) ∧ x0.head = r ∧ x0.last = y.last ∧ # x0 = 4 + n0

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 40 from proof reach-n-path-n (previous step) (back to tree)

User applied rule exists right

And obtained the following new goals

• Proof step 41:

  1 + # y = 3 + n0, y ≠ [], path(r0 ' + y, h), reachable-1(h, r, r0), reachable-1(h, r0, r2), reachable-1(h, r2, r3), reachable-1(h, r6, r4), reachable-1(h, r0, r6), reachable-n(h, n0, r3, y.last), reachable-n(h, n0, r4, y.last) ⊦ path(r + r0 + y, h) ∧ (r + r0 + y).head = r ∧ (r + r0 + y).last = y.last ∧ #(r + r0 + y) = 4 + n0

Rule argument

Additional information

Used terms: r + r0 + y

Proof step 41 from proof reach-n-path-n (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 42:

  1 + # y = 3 + n0, y ≠ [], path(r0 ' + y, h), reachable-1(h, r0, r6), reachable-1(h, r6, r4), reachable-1(h, r2, r3), reachable-1(h, r0, r2), reachable-1(h, r, r0), reachable-n(h, n0, r4, y.last), reachable-n(h, n0, r3, y.last) ⊦ r ∈ h ∧ r ≠ null ∧ h[r].nxt = r0 ∧ 2 + # y = 4 + n0

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 c: ⊦ m + n = n + m; from specification nat-basic a: ⊦ (m + n0) + n1 = m + n0 + n1; from specification nat-basic ⊦ # a ' = 0 +1; (s) ⊦ #(x + y) = # x + # y; (s) ⊦ a + x = a ' + x; (s) ⊦ x ≠ [] → (a ' + x).last = x.last; (s) ⊦ (b ' + a ' + x).last = (a ' + x).last; (s) ⊦ (a ' + x).head = a; (s)

Proof step 42 from proof reach-n-path-n (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 43:

  ⊦ reachable-1(h, r, r0) ↔ r ≠ null ∧ r0 ≠ null ∧ r ∈ h ∧ r0 ∈ h ∧ h[r].nxt = r0

• Proof step 44:

  1 + # y = 3 + n0, h[r].nxt = r0, r ≠ null, r0 ≠ null, y ≠ [], path(r0 ' + y, h), reachable-1(h, r0, r2), reachable-1(h, r2, r3), reachable-1(h, r6, r4), reachable-1(h, r0, r6), reachable-n(h, n0, r3, y.last), reachable-n(h, n0, r4, y.last), r ∈ h, r0 ∈ h ⊦ r ∈ h ∧ r ≠ null ∧ h[r].nxt = r0 ∧ 2 + # y = 4 + n0

Rule argument

Additional information

Used terms: r0, r, h

Proof step 43 from proof reach-n-path-n (previous step) (back to tree)

Lemma reachable-1-def

Proof step 44 from proof reach-n-path-n (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And closed the goal!

Rule argument

Additional information

Used simplifier rules: reachable-1-def: ⊦ reachable-1(h, r, r0) ↔ r ≠ null ∧ r0 ≠ null ∧ r ∈ h ∧ r0 ∈ h ∧ h[r].nxt = r0; c: ⊦ m + n = n + m; from specification nat-basic a: ⊦ (m + n0) + n1 = m + n0 + n1; from specification nat-basic n < n0 ⊦ m + (* n) = m0 + (* n0) ↔ m = m0 + (n0 - n); (s)

Proof step 45 from proof reach-n-path-n (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 46:

  # x = 3 + n, path(x, h), ∀ h0, r1, r2. (∃ r3. reachable-1(h0, r1, r3) ∧ reachable-n(h0, n, r3, r2)) ↔ (∃ x. path(x, h0) ∧ x.head = r1 ∧ x.last = r2 ∧ # x = 2 + n) ⊦ ∃ r1. reachable-1(h, x.head, r1) ∧ (∃ r2. reachable-1(h, r1, r2) ∧ reachable-n(h, n, r2, x.last))

Rule argument

Additional information

Proof step 46 from proof reach-n-path-n (previous step) (back to tree)

Heuristic elimination applied rule apply elim lemma

And obtained the following new goals

• Proof step 47:

  # x = 3 + n, x = r + y, x ≠ [], path(x, h), ∀ h0, r1, r2. (∃ r3. reachable-1(h0, r1, r3) ∧ reachable-n(h0, n, r3, r2)) ↔ (∃ x. path(x, h0) ∧ x.head = r1 ∧ x.last = r2 ∧ # x = 2 + n) ⊦ ∃ r1. reachable-1(h, r, r1) ∧ (∃ r2. reachable-1(h, r1, r2) ∧ reachable-n(h, n, r2, x.last))

Rule argument

Additional information

Used simplifier rules: ⊦ # [] = 0; (s) ⊦ m + n = 0 ↔ m = 0 ∧ n = 0; (ws) a: ⊦ (m + n0) + n1 = m + n0 + n1; from specification nat-basic c: ⊦ m + n = n + m; from specification nat-basic x ≠ [] ⊦ a = x.head ∧ y = x.tail ↔ x = a + y; (elim) Used terms: x, a, y

Proof step 47 from proof reach-n-path-n (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 48:

  1 + # y = 3 + n, path(r ' + y, h), ∀ h0, r1, r2. (∃ r3. reachable-1(h0, r1, r3) ∧ reachable-n(h0, n, r3, r2)) ↔ (∃ x. path(x, h0) ∧ x.head = r1 ∧ x.last = r2 ∧ # x = 2 + n) ⊦ ∃ r1. reachable-1(h, r, r1) ∧ (∃ r2. reachable-1(h, r1, r2) ∧ reachable-n(h, n, r2, (r ' + y).last))

Rule argument

Additional information

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

Proof step 48 from proof reach-n-path-n (previous step) (back to tree)

Heuristic weak cut applied rule cut formula

And obtained the following new goals

• Proof step 49:

  1 + # y = 3 + n, y = [], path(r ' + y, h), ∀ h0, r1, r2. (∃ r3. reachable-1(h0, r1, r3) ∧ reachable-n(h0, n, r3, r2)) ↔ (∃ x. path(x, h0) ∧ x.head = r1 ∧ x.last = r2 ∧ # x = 2 + n) ⊦ ∃ r1. reachable-1(h, r, r1) ∧ (∃ r2. reachable-1(h, r1, r2) ∧ reachable-n(h, n, r2, (r ' + y).last))

• Proof step 50:

  1 + # y = 3 + n, y ≠ [], path(r ' + y, h), ∀ h0, r1, r2. (∃ r3. reachable-1(h0, r1, r3) ∧ reachable-n(h0, n, r3, r2)) ↔ (∃ x. path(x, h0) ∧ x.head = r1 ∧ x.last = r2 ∧ # x = 2 + n) ⊦ ∃ r1. reachable-1(h, r, r1) ∧ (∃ r2. reachable-1(h, r1, r2) ∧ reachable-n(h, n, r2, (r ' + y).last))

Rule argument

Additional information

Used formulas: y = []

Proof step 49 from proof reach-n-path-n (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And closed the goal!

Rule argument

Additional information

Used simplifier rules: c: ⊦ m + n = n + m; from specification nat-basic a: ⊦ (m + n0) + n1 = m + n0 + n1; from specification nat-basic n < n0 ⊦ (* n) ≠ m0 + (* n0); (s) ⊦ # [] = 0; (s)

Proof step 50 from proof reach-n-path-n (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 51:

  1 + # y = 3 + n, y ≠ [], path(r ' + y, h), ∀ h0, r1, r2. (∃ r3. reachable-1(h0, r1, r3) ∧ reachable-n(h0, n, r3, r2)) ↔ (∃ x. path(x, h0) ∧ x.head = r1 ∧ x.last = r2 ∧ # x = 2 + n) ⊦ ∃ r1. reachable-1(h, r, r1) ∧ (∃ r2. reachable-1(h, r1, r2) ∧ reachable-n(h, n, r2, y.last))

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 51 from proof reach-n-path-n (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 52:

  ⊦ path(x, h) ↔ # x = 1 ∧ x.head ∈ h ∧ x.head ≠ null ∨ # x = 1 + 1 ∧ x.head ∈ h ∧ x.tail.head ∈ h ∧ x.head ≠ null ∧ x.tail.head ≠ null ∧ h[x.head].nxt = x.tail.head ∨ # x ≥ 1 + 1 ∧ x.head ∈ h ∧ x.head ≠ null ∧ h[x.head].nxt = x.tail.head ∧ path(x.tail, h)

• Proof step 53:

  1 + # y = 3 + n, y ≠ [], ∀ h0, r1, r2. (∃ r3. reachable-1(h0, r1, r3) ∧ reachable-n(h0, n, r3, r2)) ↔ (∃ x. path(x, h0) ∧ x.head = r1 ∧ x.last = r2 ∧ # x = 2 + n), #(r ' + y) = 1 ∧ (r ' + y).head ∈ h ∧ (r ' + y).head ≠ null ∨ #(r ' + y) = 1 + 1 ∧ (r ' + y).head ∈ h ∧ (r ' + y).tail.head ∈ h ∧ (r ' + y).head ≠ null ∧ (r ' + y).tail.head ≠ null ∧ h[(r ' + y).head].nxt = (r ' + y).tail.head ∨ #(r ' + y) ≥ 1 + 1 ∧ (r ' + y).head ∈ h ∧ (r ' + y).head ≠ null ∧ h[(r ' + y).head].nxt = (r ' + y).tail.head ∧ path((r ' + y).tail, h) ⊦ ∃ r1. reachable-1(h, r, r1) ∧ (∃ r2. reachable-1(h, r1, r2) ∧ reachable-n(h, n, r2, y.last))

Rule argument

Additional information

Used terms: h, r ' + y

Proof step 52 from proof reach-n-path-n (previous step) (back to tree)

Lemma k-path

Proof step 53 from proof reach-n-path-n (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 54:

  1 + # y = 3 + n, y ≠ [], ∀ h0, r1, r2. (∃ r3. reachable-1(h0, r1, r3) ∧ reachable-n(h0, n, r3, r2)) ↔ (∃ x. path(x, h0) ∧ x.head = r1 ∧ x.last = r2 ∧ # x = 2 + n), 1 = # y ∧ r ∈ h ∧ y.head ∈ h ∧ r ≠ null ∧ y.head ≠ null ∧ h[r].nxt = y.head ∨ 1 ≤ # y ∧ r ∈ h ∧ r ≠ null ∧ h[r].nxt = y.head ∧ path(y, h) ⊦ ∃ r1. reachable-1(h, r, r1) ∧ (∃ r2. reachable-1(h, r1, r2) ∧ reachable-n(h, n, r2, y.last))

Rule argument

Additional information

Used simplifier rules: a: ⊦ (x + y) + z = x + y + z; from specification polylist ⊦ (a ' + x).tail = x; (s) ⊦ (a ' + x).head = a; (s) c: ⊦ m + n = n + m; from specification nat-basic a: ⊦ (m + n0) + n1 = m + n0 + n1; from specification nat-basic n0 < n ⊦ (* n) ≤ m0 + (* n0) ↔ n - n0 ≤ m0; (s) ⊦ n ≥ m ↔ m ≤ n; (s) ⊦ # a ' = 0 +1; (s) ⊦ #(x + y) = # x + # y; (s) n0 < n ⊦ (* n) = m0 + (* n0) ↔ n - n0 = m0; (s) ⊦ # x = 0 ↔ x = []; (s) ⊦ 1 = m + 1 ↔ m = 0; (s)

Proof step 54 from proof reach-n-path-n (previous step) (back to tree)

Heuristic elimination applied rule apply elim lemma

And obtained the following new goals

• Proof step 55:

  1 + # y = 3 + n, y = r0 + y0, y ≠ [], ∀ h0, r1, r2. (∃ r3. reachable-1(h0, r1, r3) ∧ reachable-n(h0, n, r3, r2)) ↔ (∃ x. path(x, h0) ∧ x.head = r1 ∧ x.last = r2 ∧ # x = 2 + n), 1 = # y ∧ r ∈ h ∧ r0 ∈ h ∧ r ≠ null ∧ r0 ≠ null ∧ h[r].nxt = r0 ∨ 1 ≤ # y ∧ r ∈ h ∧ r ≠ null ∧ h[r].nxt = r0 ∧ path(y, h) ⊦ ∃ r1. reachable-1(h, r, r1) ∧ (∃ r2. reachable-1(h, r1, r2) ∧ reachable-n(h, n, r2, y.last))

Rule argument

Additional information

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

Proof step 55 from proof reach-n-path-n (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 56:

  1 + 1 + # y0 = 3 + n, ∀ h0, r1, r2. (∃ r3. reachable-1(h0, r1, r3) ∧ reachable-n(h0, n, r3, r2)) ↔ (∃ x. path(x, h0) ∧ x.head = r1 ∧ x.last = r2 ∧ # x = 2 + n), 1 = 1 + # y0 ∧ r ∈ h ∧ h[r].nxt ∈ h ∧ r ≠ null ∧ h[r].nxt ≠ null ∧ h[r].nxt = r0 ∨ 1 ≤ 1 + # y0 ∧ r ∈ h ∧ r ≠ null ∧ h[r].nxt = r0 ∧ path(h[r].nxt ' + y0, h) ⊦ ∃ r1. reachable-1(h, r, r1) ∧ (∃ r2. reachable-1(h, r1, r2) ∧ reachable-n(h, n, r2, (r0 ' + y0).last))

Rule argument

Additional information

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

Proof step 56 from proof reach-n-path-n (previous step) (back to tree)

Heuristic weak cut applied rule cut formula

And obtained the following new goals

• Proof step 57:

  1 + 1 + # y0 = 3 + n, y0 = [], ∀ h0, r1, r2. (∃ r3. reachable-1(h0, r1, r3) ∧ reachable-n(h0, n, r3, r2)) ↔ (∃ x. path(x, h0) ∧ x.head = r1 ∧ x.last = r2 ∧ # x = 2 + n), 1 = 1 + # y0 ∧ r ∈ h ∧ h[r].nxt ∈ h ∧ r ≠ null ∧ h[r].nxt ≠ null ∧ h[r].nxt = r0 ∨ 1 ≤ 1 + # y0 ∧ r ∈ h ∧ r ≠ null ∧ h[r].nxt = r0 ∧ path(h[r].nxt ' + y0, h) ⊦ ∃ r1. reachable-1(h, r, r1) ∧ (∃ r2. reachable-1(h, r1, r2) ∧ reachable-n(h, n, r2, (r0 ' + y0).last))

• Proof step 58:

  1 + 1 + # y0 = 3 + n, y0 ≠ [], ∀ h0, r1, r2. (∃ r3. reachable-1(h0, r1, r3) ∧ reachable-n(h0, n, r3, r2)) ↔ (∃ x. path(x, h0) ∧ x.head = r1 ∧ x.last = r2 ∧ # x = 2 + n), 1 = 1 + # y0 ∧ r ∈ h ∧ h[r].nxt ∈ h ∧ r ≠ null ∧ h[r].nxt ≠ null ∧ h[r].nxt = r0 ∨ 1 ≤ 1 + # y0 ∧ r ∈ h ∧ r ≠ null ∧ h[r].nxt = r0 ∧ path(h[r].nxt ' + y0, h) ⊦ ∃ r1. reachable-1(h, r, r1) ∧ (∃ r2. reachable-1(h, r1, r2) ∧ reachable-n(h, n, r2, (r0 ' + y0).last))

Rule argument

Additional information

Used formulas: y0 = []

Proof step 57 from proof reach-n-path-n (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And closed the goal!

Rule argument

Additional information

Used simplifier rules: c: ⊦ m + n = n + m; from specification nat-basic a: ⊦ (m + n0) + n1 = m + n0 + n1; from specification nat-basic n < n0 ⊦ (* n) ≠ m0 + (* n0); (s) ⊦ # [] = 0; (s)

Proof step 58 from proof reach-n-path-n (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 59:

  # y0 = n + 1, r ≠ null, y0 ≠ [], path(h[r].nxt ' + y0, h), r ∈ h, ∀ h0, r1, r2. (∃ r3. reachable-1(h0, r1, r3) ∧ reachable-n(h0, n, r3, r2)) ↔ (∃ x. path(x, h0) ∧ x.head = r1 ∧ x.last = r2 ∧ # x = 2 + n) ⊦ ∃ r1. reachable-1(h, r, r1) ∧ (∃ r2. reachable-1(h, r1, r2) ∧ reachable-n(h, n, r2, y0.last))

Rule argument

Additional information

Used simplifier rules: a: ⊦ (x + y) + z = x + y + z; from specification polylist ⊦ x ≠ [] → (a ' + x).last = x.last; (s) c: ⊦ m + n = n + m; from specification nat-basic a: ⊦ (m + n0) + n1 = m + n0 + n1; from specification nat-basic ⊦ m ≤ m + n; (s) ⊦ # x = 0 ↔ x = []; (s) ⊦ 1 = m + 1 ↔ m = 0; (s) n < n0 ⊦ m + (* n) = m0 + (* n0) ↔ m = m0 + (n0 - n); (s)

Proof step 59 from proof reach-n-path-n (previous step) (back to tree)

User applied rule all left

And obtained the following new goals

• Proof step 60:

  # y0 = n + 1, r ≠ null, y0 ≠ [], path(h[r].nxt ' + y0, h), r ∈ h, (∃ r3. reachable-1(h, h[r].nxt, r3) ∧ reachable-n(h, n, r3, y0.last)) ↔ (∃ x. path(x, h) ∧ x.head = h[r].nxt ∧ x.last = y0.last ∧ # x = 2 + n) ⊦ ∃ r1. reachable-1(h, r, r1) ∧ (∃ r2. reachable-1(h, r1, r2) ∧ reachable-n(h, n, r2, y0.last))

Rule argument

Additional information

Used terms: h, h[r].nxt, y0.last

Proof step 60 from proof reach-n-path-n (previous step) (back to tree)

User applied rule case distinction

And obtained the following new goals

• Proof step 61:

  # y0 = n + 1, r ≠ null, y0 ≠ [], path(h[r].nxt ' + y0, h), r ∈ h ⊦ ∃ r1. reachable-1(h, r, r1) ∧ (∃ r2. reachable-1(h, r1, r2) ∧ reachable-n(h, n, r2, y0.last)), ∃ x. path(x, h) ∧ x.head = h[r].nxt ∧ x.last = y0.last ∧ # x = 2 + n, ∃ r3. reachable-1(h, h[r].nxt, r3) ∧ reachable-n(h, n, r3, y0.last)

• Proof step 62:

  # y0 = n + 1, r ≠ null, y0 ≠ [], path(h[r].nxt ' + y0, h), r ∈ h, ∃ x. path(x, h) ∧ x.head = h[r].nxt ∧ x.last = y0.last ∧ # x = 2 + n, ∃ r3. reachable-1(h, h[r].nxt, r3) ∧ reachable-n(h, n, r3, y0.last) ⊦ ∃ r1. reachable-1(h, r, r1) ∧ (∃ r2. reachable-1(h, r1, r2) ∧ reachable-n(h, n, r2, y0.last))

Rule argument

Additional information

Proof step 61 from proof reach-n-path-n (previous step) (back to tree)

User applied rule exists right

And closed the goal!

Rule argument

Additional information

Used simplifier rules: ⊦ (a ' + x).head = a; (s) ⊦ x ≠ [] → (a ' + x).last = x.last; (s) ⊦ a + x = a ' + x; (s) ⊦ #(x + y) = # x + # y; (s) ⊦ # a ' = 0 +1; (s) a: ⊦ (x + y) + z = x + y + z; from specification polylist n < n0 ⊦ m + (* n) = m0 + (* n0) ↔ m = m0 + (n0 - n); (s) a: ⊦ (m + n0) + n1 = m + n0 + n1; from specification nat-basic c: ⊦ m + n = n + m; from specification nat-basic Used terms: h[r].nxt + y0

Proof step 62 from proof reach-n-path-n (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 63:

  # x = 2 + n, # y0 = n + 1, x.head = h[r].nxt, x.last = y0.last, r ≠ null, y0 ≠ [], path(x, h), path(x.head ' + y0, h), reachable-1(h, x.head, r3), reachable-n(h, n, r3, y0.last), r ∈ h ⊦ ∃ r1. reachable-1(h, r, r1) ∧ (∃ r2. reachable-1(h, r1, r2) ∧ reachable-n(h, n, r2, y0.last))

Rule argument

Additional information

Proof step 63 from proof reach-n-path-n (previous step) (back to tree)

Heuristic elimination applied rule apply elim lemma

And obtained the following new goals

• Proof step 64:

  # y0 = n + 1, # x = 2 + n, x.last = y0.last, r0 = h[r].nxt, x = r0 + y, r ≠ null, x ≠ [], y0 ≠ [], path(r0 ' + y0, h), path(x, h), reachable-1(h, r0, r3), reachable-n(h, n, r3, y0.last), r ∈ h ⊦ ∃ r1. reachable-1(h, r, r1) ∧ (∃ r2. reachable-1(h, r1, r2) ∧ reachable-n(h, n, r2, y0.last))

Rule argument

Additional information

Used simplifier rules: ⊦ # [] = 0; (s) ⊦ m + n = 0 ↔ m = 0 ∧ n = 0; (ws) a: ⊦ (m + n0) + n1 = m + n0 + n1; from specification nat-basic c: ⊦ m + n = n + m; from specification nat-basic x ≠ [] ⊦ a = x.head ∧ y = x.tail ↔ x = a + y; (elim) Used terms: x, a, y

Proof step 64 from proof reach-n-path-n (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 65:

  # y0 = n + 1, # y = n + 1, (h[r].nxt ' + y).last = y0.last, r ≠ null, y0 ≠ [], path(h[r].nxt ' + y0, h), path(h[r].nxt ' + y, h), reachable-1(h, h[r].nxt, r3), reachable-n(h, n, r3, y0.last), r ∈ h ⊦ ∃ r1. reachable-1(h, r, r1) ∧ (∃ r2. reachable-1(h, r1, r2) ∧ reachable-n(h, n, r2, y0.last))

Rule argument

Additional information

Used simplifier rules: ⊦ a + x = a ' + x; (s) a: ⊦ (x + y) + z = x + y + z; from specification polylist ⊦ a ' + x ≠ []; (s) c: ⊦ m + n = n + m; from specification nat-basic a: ⊦ (m + n0) + n1 = m + n0 + n1; from specification nat-basic n < n0 ⊦ m + (* n) = m0 + (* n0) ↔ m = m0 + (n0 - n); (s) ⊦ # a ' = 0 +1; (s) ⊦ #(x + y) = # x + # y; (s)

Proof step 65 from proof reach-n-path-n (previous step) (back to tree)

User applied rule exists right

And obtained the following new goals

• Proof step 66:

  # y = n + 1, # y0 = n + 1, (h[r].nxt ' + y).last = y0.last, r ≠ null, y0 ≠ [], path(h[r].nxt ' + y, h), path(h[r].nxt ' + y0, h), reachable-1(h, h[r].nxt, r3), reachable-n(h, n, r3, y0.last), r ∈ h ⊦ reachable-1(h, r, h[r].nxt) ∧ (∃ r2. reachable-1(h, h[r].nxt, r2) ∧ reachable-n(h, n, r2, y0.last))

Rule argument

Additional information

Used terms: h[r].nxt

Proof step 66 from proof reach-n-path-n (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 67:

  ⊦ reachable-1(h, r, r0) ↔ r ≠ null ∧ r0 ≠ null ∧ r ∈ h ∧ r0 ∈ h ∧ h[r].nxt = r0

• Proof step 68:

  # y0 = n + 1, # y = n + 1, (h[r].nxt ' + y).last = y0.last, r ≠ null, y0 ≠ [], path(h[r].nxt ' + y0, h), path(h[r].nxt ' + y, h), reachable-1(h, h[r].nxt, r3), reachable-n(h, n, r3, y0.last), r ∈ h ⊦ (r ≠ null ∧ h[r].nxt ≠ null ∧ r ∈ h ∧ h[r].nxt ∈ h ∧ h[r].nxt = h[r].nxt) ∧ (∃ r2. reachable-1(h, h[r].nxt, r2) ∧ reachable-n(h, n, r2, y0.last))

Rule argument

Additional information

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

Proof step 67 from proof reach-n-path-n (previous step) (back to tree)

Lemma reachable-1-def

Proof step 68 from proof reach-n-path-n (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 69:

  # y = n + 1, # y0 = n + 1, (h[r].nxt ' + y).last = y0.last, r ≠ null, y0 ≠ [], path(h[r].nxt ' + y, h), path(h[r].nxt ' + y0, h), reachable-1(h, h[r].nxt, r3), reachable-n(h, n, r3, y0.last), r ∈ h ⊦ h[r].nxt ≠ null ∧ (∃ r2. reachable-1(h, h[r].nxt, r2) ∧ reachable-n(h, n, r2, y0.last))

Rule argument

Additional information

Used simplifier rules: path-first-in-H: ⊦ path(r ' + x, h) → (r ∈ h ↔ true); a: ⊦ (x + y) + z = x + y + z; from specification polylist

Proof step 69 from proof reach-n-path-n (previous step) (back to tree)

User applied rule case distinction

And obtained the following new goals

• Proof step 70:

  # y0 = n + 1, # y = n + 1, (h[r].nxt ' + y).last = y0.last, r ≠ null, y0 ≠ [], path(h[r].nxt ' + y0, h), path(h[r].nxt ' + y, h), reachable-1(h, h[r].nxt, r3), reachable-n(h, n, r3, y0.last), r ∈ h ⊦ ∃ r2. reachable-1(h, h[r].nxt, r2) ∧ reachable-n(h, n, r2, y0.last)

Rule argument

Additional information

Used simplifier rules: null-not-start-of-path: ⊦ ¬ path(null ' + x, h); a: ⊦ (x + y) + z = x + y + z; from specification polylist

Proof step 70 from proof reach-n-path-n (previous step) (back to tree)

Heuristic quantifier closing applied rule exists right

And closed the goal!

Rule argument

Additional information

Used terms: r3