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) ∧ hd x = 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) ∧ hd x = r ∧ x.last = r0 ∧ # x = n0 + 1)) ⊦ reachable-n(h, n0 +1, r, r0) ↔ (∃ x. path(x, h) ∧ hd x = 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) ∧ hd x = r ∧ x.last = r0 ∧ # x = n0 + 1)) ⊦ (∃ r1. reachable-1(h, r, r1) ∧ reachable-n(h, n0, r1, r0)) ↔ (∃ x. path(x, h) ∧ hd x = 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) ∧ hd x = r ∧ x.last = r0 ∧ # x = n0 + 1)) ⊦ (∃ r1. reachable-1(h, r, r1) ∧ reachable-n(h, n0, r1, r0)) ↔ (∃ x. path(x, h) ∧ hd x = 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) ∧ hd x = r ∧ x.last = r0 ∧ # x = n0 + 1)) ⊦ (∃ r1. reachable-1(h, r, r1) ∧ reachable-n(h, n0, r1, r0)) ↔ (∃ x. path(x, h) ∧ hd x = 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) ∧ hd x = 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) ∧ hd x = 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) ∧ hd x = 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) ∧ hd x = r ∧ x.last = r0 ∧ # x = 2

• Proof step 12:

  ∃ x. path(x, h) ∧ hd x = 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) ∧ hd x = r ∧ x.last = h[hd x].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) ⊦ hd(a ' + x) = a; (s) ⊦ #(x + y) = # x + # y; (s) ⊦ # a ' = 0 +1; (s) a: ⊦ (x + y) + z = x + y + z; from specification list[reflist] 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) ⊦ hd x ≠ null ∧ h[hd x].nxt ≠ null ∧ hd x ∈ h ∧ h[hd x].nxt ∈ h ∧ h[hd x].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 + x0, 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 = hd x ∧ y = tl x ↔ 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 = # x0, r ≠ null, path(r ' + x0, h) ⊦ h[r].nxt = hd x0 ∧ 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 list[reflist] ⊦ # x = 1 → (y + x).last = hd x; (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 list[reflist] ⊦ # [] = 0; (s) x ≠ [] ⊦ a = hd x ∧ y = tl x ↔ x = a + y; (elim) Used terms: x0, a, y

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) ∧ hd x = 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) ∧ hd x = 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) ∧ hd x = 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) ∧ hd x = 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) ∧ hd x = r1 ∧ x.last = r2 ∧ # x = 2 + n), ∃ x. path(x, h) ∧ hd x = 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) ∧ hd x = r1 ∧ x.last = r2 ∧ # x = 2 + n) ⊦ ∃ x. path(x, h) ∧ hd x = 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) ∧ hd x = r1 ∧ x.last = r2 ∧ # x = 2 + n) ⊦ ∃ x. path(x, h) ∧ hd x = 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) ∧ hd x = r1 ∧ x.last = r2 ∧ # x = 2 + n) ⊦ ∃ x. path(x, h) ∧ hd x = 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) ∧ hd x = r3 ∧ x.last = r4 ∧ # x = 2) ⊦ ∃ x. path(x, h) ∧ hd x = 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) ∧ hd x = r3 ∧ x.last = r4 ∧ # x = 2) ⊦ path(r ' + r1 ' + r0 ', h) ∧ hd(r ' + r1 ' + r0 ') = 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) ∧ hd x = 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 list[reflist] ⊦ # a ' = 0 +1; (s) ⊦ #(x + y) = # x + # y; (s) ⊦ (x + a ').last = a; (s) ⊦ (b ' + a ' + x).last = (a ' + x).last; (s) ⊦ hd(a ' + x) = 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) ∧ hd x = 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) ∧ hd x = 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) ∧ hd x = r4 ∧ x.last = r5 ∧ # x = 3 + n0) ⊦ ∃ x. path(x, h) ∧ hd x = 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) ∧ hd x = r1 ∧ x.last = r0 ∧ # x = 3 + n0) ⊦ ∃ x. path(x, h) ∧ hd x = 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) ∧ hd x = r ∧ x.last = r0 ∧ # x = 4 + n0, ∃ x. path(x, h) ∧ hd x = 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) ∧ hd x = 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) ∧ hd x = 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) ∧ hd x = r1 ∧ x.last = r0 ∧ # x = 3 + n0, ∃ x. path(x, h) ∧ hd x = 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) ∧ hd x = r ∧ x.last = r0 ∧ # x = 4 + n0, ∃ x. path(x, h) ∧ hd x = 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, hd x, r6), reachable-1(h, r6, r4), reachable-1(h, r2, r3), reachable-1(h, hd x, r2), reachable-1(h, r, hd x), reachable-n(h, n0, r4, x.last), reachable-n(h, n0, r3, x.last) ⊦ ∃ x0. path(x0, h) ∧ hd x0 = 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 + x1, 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) ∧ hd x0 = 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 = hd x ∧ y = tl x ↔ 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 + # x1 = 3 + n0, path(r0 ' + x1, 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 ' + x1).last), reachable-n(h, n0, r3, (r0 ' + x1).last) ⊦ ∃ x0. path(x0, h) ∧ hd x0 = r ∧ x0.last = (r0 ' + x1).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 list[reflist] ⊦ 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 + # x1 = 3 + n0, x1 = [], path(r0 ' + x1, 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 ' + x1).last), reachable-n(h, n0, r4, (r0 ' + x1).last) ⊦ ∃ x0. path(x0, h) ∧ hd x0 = r ∧ x0.last = (r0 ' + x1).last ∧ # x0 = 4 + n0

• Proof step 39:

  1 + # x1 = 3 + n0, x1 ≠ [], path(r0 ' + x1, 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 ' + x1).last), reachable-n(h, n0, r4, (r0 ' + x1).last) ⊦ ∃ x0. path(x0, h) ∧ hd x0 = r ∧ x0.last = (r0 ' + x1).last ∧ # x0 = 4 + n0

Rule argument

Additional information

Used formulas: x1 = []

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 + # x1 = 3 + n0, x1 ≠ [], path(r0 ' + x1, 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, x1.last), reachable-n(h, n0, r3, x1.last) ⊦ ∃ x0. path(x0, h) ∧ hd x0 = r ∧ x0.last = x1.last ∧ # x0 = 4 + n0

Rule argument

Additional information

Used simplifier rules: a: ⊦ (x + y) + z = x + y + z; from specification list[reflist] ⊦ 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 + # x1 = 3 + n0, x1 ≠ [], path(r0 ' + x1, 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, x1.last), reachable-n(h, n0, r4, x1.last) ⊦ path(r + r0 + x1, h) ∧ hd(r + r0 + x1) = r ∧ (r + r0 + x1).last = x1.last ∧ #(r + r0 + x1) = 4 + n0

Rule argument

Additional information

Used terms: r + r0 + x1

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 + # x1 = 3 + n0, x1 ≠ [], path(r0 ' + x1, 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, x1.last), reachable-n(h, n0, r3, x1.last) ⊦ r ∈ h ∧ r ≠ null ∧ h[r].nxt = r0 ∧ 2 + # x1 = 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 list[reflist] 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) ⊦ hd(a ' + x) = 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 + # x1 = 3 + n0, h[r].nxt = r0, r ≠ null, r0 ≠ null, x1 ≠ [], path(r0 ' + x1, 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, x1.last), reachable-n(h, n0, r4, x1.last), r ∈ h, r0 ∈ h ⊦ r ∈ h ∧ r ≠ null ∧ h[r].nxt = r0 ∧ 2 + # x1 = 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) ∧ hd x = r1 ∧ x.last = r2 ∧ # x = 2 + n) ⊦ ∃ r1. reachable-1(h, hd x, 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 + x0, x ≠ [], path(x, h), ∀ h0, r1, r2. (∃ r3. reachable-1(h0, r1, r3) ∧ reachable-n(h0, n, r3, r2)) ↔ (∃ x. path(x, h0) ∧ hd x = 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 = hd x ∧ y = tl x ↔ 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 + # x0 = 3 + n, path(r ' + x0, h), ∀ h0, r1, r2. (∃ r3. reachable-1(h0, r1, r3) ∧ reachable-n(h0, n, r3, r2)) ↔ (∃ x. path(x, h0) ∧ hd x = 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 ' + x0).last))

Rule argument

Additional information

Used simplifier rules: ⊦ a + x = a ' + x; (s) a: ⊦ (x + y) + z = x + y + z; from specification list[reflist] ⊦ 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 + # x0 = 3 + n, x0 = [], path(r ' + x0, h), ∀ h0, r1, r2. (∃ r3. reachable-1(h0, r1, r3) ∧ reachable-n(h0, n, r3, r2)) ↔ (∃ x. path(x, h0) ∧ hd x = 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 ' + x0).last))

• Proof step 50:

  1 + # x0 = 3 + n, x0 ≠ [], path(r ' + x0, h), ∀ h0, r1, r2. (∃ r3. reachable-1(h0, r1, r3) ∧ reachable-n(h0, n, r3, r2)) ↔ (∃ x. path(x, h0) ∧ hd x = 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 ' + x0).last))

Rule argument

Additional information

Used formulas: x0 = []

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 + # x0 = 3 + n, x0 ≠ [], path(r ' + x0, h), ∀ h0, r1, r2. (∃ r3. reachable-1(h0, r1, r3) ∧ reachable-n(h0, n, r3, r2)) ↔ (∃ x. path(x, h0) ∧ hd x = r1 ∧ x.last = r2 ∧ # x = 2 + n) ⊦ ∃ r1. reachable-1(h, r, r1) ∧ (∃ r2. reachable-1(h, r1, r2) ∧ reachable-n(h, n, r2, x0.last))

Rule argument

Additional information

Used simplifier rules: a: ⊦ (x + y) + z = x + y + z; from specification list[reflist] ⊦ 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 ∧ hd x ∈ h ∧ hd x ≠ null ∨ # x = 1 + 1 ∧ hd x ∈ h ∧ hd tl x ∈ h ∧ hd x ≠ null ∧ hd tl x ≠ null ∧ h[hd x].nxt = hd tl x ∨ # x ≥ 1 + 1 ∧ hd x ∈ h ∧ hd x ≠ null ∧ h[hd x].nxt = hd tl x ∧ path(tl x, h)

• Proof step 53:

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

Rule argument

Additional information

Used terms: h, r ' + x0

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 + # x0 = 3 + n, x0 ≠ [], ∀ h0, r1, r2. (∃ r3. reachable-1(h0, r1, r3) ∧ reachable-n(h0, n, r3, r2)) ↔ (∃ x. path(x, h0) ∧ hd x = r1 ∧ x.last = r2 ∧ # x = 2 + n), 1 = # x0 ∧ r ∈ h ∧ hd x0 ∈ h ∧ r ≠ null ∧ hd x0 ≠ null ∧ h[r].nxt = hd x0 ∨ 1 ≤ # x0 ∧ r ∈ h ∧ r ≠ null ∧ h[r].nxt = hd x0 ∧ path(x0, h) ⊦ ∃ r1. reachable-1(h, r, r1) ∧ (∃ r2. reachable-1(h, r1, r2) ∧ reachable-n(h, n, r2, x0.last))

Rule argument

Additional information

Used simplifier rules: a: ⊦ (x + y) + z = x + y + z; from specification list[reflist] ⊦ tl(a ' + x) = x; (s) ⊦ hd(a ' + x) = 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 + # x0 = 3 + n, x0 = r0 + x1, x0 ≠ [], ∀ h0, r1, r2. (∃ r3. reachable-1(h0, r1, r3) ∧ reachable-n(h0, n, r3, r2)) ↔ (∃ x. path(x, h0) ∧ hd x = r1 ∧ x.last = r2 ∧ # x = 2 + n), 1 = # x0 ∧ r ∈ h ∧ r0 ∈ h ∧ r ≠ null ∧ r0 ≠ null ∧ h[r].nxt = r0 ∨ 1 ≤ # x0 ∧ r ∈ h ∧ r ≠ null ∧ h[r].nxt = r0 ∧ path(x0, h) ⊦ ∃ r1. reachable-1(h, r, r1) ∧ (∃ r2. reachable-1(h, r1, r2) ∧ reachable-n(h, n, r2, x0.last))

Rule argument

Additional information

Used simplifier rules: x ≠ [] ⊦ a = hd x ∧ y = tl x ↔ x = a + y; (elim) Used terms: x0, a, y

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 + # x1 = 3 + n, ∀ h0, r1, r2. (∃ r3. reachable-1(h0, r1, r3) ∧ reachable-n(h0, n, r3, r2)) ↔ (∃ x. path(x, h0) ∧ hd x = r1 ∧ x.last = r2 ∧ # x = 2 + n), 1 = 1 + # x1 ∧ r ∈ h ∧ h[r].nxt ∈ h ∧ r ≠ null ∧ h[r].nxt ≠ null ∧ h[r].nxt = r0 ∨ 1 ≤ 1 + # x1 ∧ r ∈ h ∧ r ≠ null ∧ h[r].nxt = r0 ∧ path(h[r].nxt ' + x1, h) ⊦ ∃ r1. reachable-1(h, r, r1) ∧ (∃ r2. reachable-1(h, r1, r2) ∧ reachable-n(h, n, r2, (r0 ' + x1).last))

Rule argument

Additional information

Used simplifier rules: ⊦ a + x = a ' + x; (s) a: ⊦ (x + y) + z = x + y + z; from specification list[reflist] ⊦ # 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 + # x1 = 3 + n, x1 = [], ∀ h0, r1, r2. (∃ r3. reachable-1(h0, r1, r3) ∧ reachable-n(h0, n, r3, r2)) ↔ (∃ x. path(x, h0) ∧ hd x = r1 ∧ x.last = r2 ∧ # x = 2 + n), 1 = 1 + # x1 ∧ r ∈ h ∧ h[r].nxt ∈ h ∧ r ≠ null ∧ h[r].nxt ≠ null ∧ h[r].nxt = r0 ∨ 1 ≤ 1 + # x1 ∧ r ∈ h ∧ r ≠ null ∧ h[r].nxt = r0 ∧ path(h[r].nxt ' + x1, h) ⊦ ∃ r1. reachable-1(h, r, r1) ∧ (∃ r2. reachable-1(h, r1, r2) ∧ reachable-n(h, n, r2, (r0 ' + x1).last))

• Proof step 58:

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

Rule argument

Additional information

Used formulas: x1 = []

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:

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

Rule argument

Additional information

Used simplifier rules: a: ⊦ (x + y) + z = x + y + z; from specification list[reflist] ⊦ 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:

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

Rule argument

Additional information

Used terms: h, h[r].nxt, x1.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:

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

• Proof step 62:

  # x1 = n + 1, r ≠ null, x1 ≠ [], path(h[r].nxt ' + x1, h), r ∈ h, ∃ x. path(x, h) ∧ hd x = h[r].nxt ∧ x.last = x1.last ∧ # x = 2 + n, ∃ r3. reachable-1(h, h[r].nxt, r3) ∧ reachable-n(h, n, r3, x1.last) ⊦ ∃ r1. reachable-1(h, r, r1) ∧ (∃ r2. reachable-1(h, r1, r2) ∧ reachable-n(h, n, r2, x1.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: ⊦ hd(a ' + x) = 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 list[reflist] 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 + x1

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, # x1 = n + 1, x.last = x1.last, hd x = h[r].nxt, r ≠ null, x1 ≠ [], path(x, h), path((hd x)' + x1, h), reachable-1(h, hd x, r3), reachable-n(h, n, r3, x1.last), r ∈ h ⊦ ∃ r1. reachable-1(h, r, r1) ∧ (∃ r2. reachable-1(h, r1, r2) ∧ reachable-n(h, n, r2, x1.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:

  # x1 = n + 1, # x = 2 + n, x.last = x1.last, r0 = h[r].nxt, x = r0 + x0, r ≠ null, x ≠ [], x1 ≠ [], path(r0 ' + x1, h), path(x, h), reachable-1(h, r0, r3), reachable-n(h, n, r3, x1.last), r ∈ h ⊦ ∃ r1. reachable-1(h, r, r1) ∧ (∃ r2. reachable-1(h, r1, r2) ∧ reachable-n(h, n, r2, x1.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 = hd x ∧ y = tl x ↔ 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:

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

Rule argument

Additional information

Used simplifier rules: ⊦ a + x = a ' + x; (s) a: ⊦ (x + y) + z = x + y + z; from specification list[reflist] ⊦ 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:

  # x0 = n + 1, # x1 = n + 1, (h[r].nxt ' + x0).last = x1.last, r ≠ null, x1 ≠ [], path(h[r].nxt ' + x0, h), path(h[r].nxt ' + x1, h), reachable-1(h, h[r].nxt, r3), reachable-n(h, n, r3, x1.last), r ∈ h ⊦ reachable-1(h, r, h[r].nxt) ∧ (∃ r2. reachable-1(h, h[r].nxt, r2) ∧ reachable-n(h, n, r2, x1.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:

  # x1 = n + 1, # x0 = n + 1, (h[r].nxt ' + x0).last = x1.last, r ≠ null, x1 ≠ [], path(h[r].nxt ' + x1, h), path(h[r].nxt ' + x0, h), reachable-1(h, h[r].nxt, r3), reachable-n(h, n, r3, x1.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, x1.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:

  # x0 = n + 1, # x1 = n + 1, (h[r].nxt ' + x0).last = x1.last, r ≠ null, x1 ≠ [], path(h[r].nxt ' + x0, h), path(h[r].nxt ' + x1, h), reachable-1(h, h[r].nxt, r3), reachable-n(h, n, r3, x1.last), r ∈ h ⊦ h[r].nxt ≠ null ∧ (∃ r2. reachable-1(h, h[r].nxt, r2) ∧ reachable-n(h, n, r2, x1.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 list[reflist]

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:

  # x1 = n + 1, # x0 = n + 1, (h[r].nxt ' + x0).last = x1.last, r ≠ null, x1 ≠ [], path(h[r].nxt ' + x1, h), path(h[r].nxt ' + x0, h), reachable-1(h, h[r].nxt, r3), reachable-n(h, n, r3, x1.last), r ∈ h ⊦ ∃ r2. reachable-1(h, h[r].nxt, r2) ∧ reachable-n(h, n, r2, x1.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 list[reflist]

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