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

System applied rule normalize

And obtained the following new goals

• Proof step 2:

  m < n, reachable-n(h, n, r, r0) ⊦ ∃ r1. reachable-n(h, m, r, r1) ∧ reachable-n(h, n - m, r1, r0)

Rule argument

Additional information

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

Heuristic elimination applied rule apply elim lemma

And obtained the following new goals

• Proof step 3:

  n = n0 + m, m < n, reachable-n(h, n, r, r0), m ≤ n ⊦ ∃ r1. reachable-n(h, m, r, r1) ∧ reachable-n(h, n0, r1, r0)

Rule argument

Additional information

Used simplifier rules: ⊦ m < n → m ≤ n; (s) n ≤ m ⊦ n0 = m - n ↔ m = n0 + n; (elim) Used terms: n, m, n0

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

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 4:

  n0 ≠ 0, reachable-n(h, n0 + m, r, r0) ⊦ ∃ r1. reachable-n(h, m, r, r1) ∧ reachable-n(h, n0, r1, r0)

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 ⊦ m < m + n ↔ n ≠ 0; (s) ⊦ m < n → m ≤ n; (s)

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

User applied rule structural induction

And obtained the following new goals

• Proof step 5:

  n0 ≠ 0, reachable-n(h, n0 + m0 +1, r, r0), ∀ n0, h, r, r0. n0 ≠ 0 ∧ reachable-n(h, n0 + m0, r, r0) → (∃ r1. reachable-n(h, m0, r, r1) ∧ reachable-n(h, n0, r1, r0)) ⊦ ∃ r1. reachable-n(h, m0 +1, r, r1) ∧ reachable-n(h, n0, r1, r0)

Rule argument

Additional information

Used simplifier rules: reachable-n-base: ⊦ reachable-n(h, 0, r, r0) ↔ r = r0; nat freely generated by 0, +1;; ⊦ 0 + m = m; (s) a: ⊦ (m + n0) + n1 = m + n0 + n1; from specification nat-basic c: ⊦ m + n = n + m; from specification nat-basic

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

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 6:

  h[r].nxt ≠ null, n0 ≠ 0, r ≠ null, reachable-n(h, n0 + m0, h[r].nxt, r0), h[r].nxt ∈ h, r ∈ h, ∀ n0, h, r, r0. n0 ≠ 0 ∧ reachable-n(h, n0 + m0, r, r0) → (∃ r1. reachable-n(h, m0, r, r1) ∧ reachable-n(h, n0, r1, r0)) ⊦ ∃ r2. (∃ r1. reachable-1(h, r, r1) ∧ reachable-n(h, m0, r1, r2)) ∧ reachable-n(h, n0, r2, r0)

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; reachable-n-rec: ⊦ reachable-n(h, n + 1, r, r0) ↔ (∃ r1. reachable-1(h, r, r1) ∧ reachable-n(h, n, r1, r0)); c: ⊦ m + n = n + m; from specification nat-basic a: ⊦ (m + n0) + n1 = m + n0 + n1; from specification nat-basic ⊦ m +1 = m + 1; (s)

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

User applied rule all left

And obtained the following new goals

• Proof step 7:

  h[r].nxt ≠ null, n0 ≠ 0, r ≠ null, reachable-n(h, n0 + m0, h[r].nxt, r0), r ∈ h, h[r].nxt ∈ h, n0 ≠ 0 ∧ reachable-n(h, n0 + m0, h[r].nxt, r0) → (∃ r1. reachable-n(h, m0, h[r].nxt, r1) ∧ reachable-n(h, n0, r1, r0)) ⊦ ∃ r2. (∃ r1. reachable-1(h, r, r1) ∧ reachable-n(h, m0, r1, r2)) ∧ reachable-n(h, n0, r2, r0)

Rule argument

Additional information

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

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

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 8:

  h[r].nxt ≠ null, n0 ≠ 0, r ≠ null, reachable-n(h, n0 + m0, h[r].nxt, r0), reachable-n(h, m0, h[r].nxt, r1), reachable-n(h, n0, r1, r0), h[r].nxt ∈ h, r ∈ h ⊦ ∃ r2. (∃ r1. reachable-1(h, r, r1) ∧ reachable-n(h, m0, r1, r2)) ∧ reachable-n(h, n0, r2, r0)

Rule argument

Additional information

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

User applied rule exists right

And obtained the following new goals

• Proof step 9:

  h[r].nxt ≠ null, n0 ≠ 0, r ≠ null, reachable-n(h, n0, r1, r0), reachable-n(h, m0, h[r].nxt, r1), reachable-n(h, n0 + m0, h[r].nxt, r0), r ∈ h, h[r].nxt ∈ h ⊦ (∃ r0. reachable-1(h, r, r0) ∧ reachable-n(h, m0, r0, r1)) ∧ reachable-n(h, n0, r1, r0)

Rule argument

Additional information

Used terms: r1

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

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 10:

  h[r].nxt ≠ null, n0 ≠ 0, r ≠ null, reachable-n(h, n0 + m0, h[r].nxt, r0), reachable-n(h, m0, h[r].nxt, r1), reachable-n(h, n0, r1, r0), h[r].nxt ∈ h, r ∈ h ⊦ ∃ r0. reachable-1(h, r, r0) ∧ reachable-n(h, m0, r0, r1)

Rule argument

Additional information

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

Heuristic quantifier closing applied rule exists right

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