Proof step 1 from proof reachable-n-rec-rev (conclusion) (back to tree)

User applied rule apply lemma

And obtained the following new goals

• Proof step 2:

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

• Proof step 3:

  ⊦ reachable-n(h, n + 1, r, r0) ↔ (∃ r1. reachable-n(h, n, r, r1) ∧ reachable-1(h, r1, r0)), reachable-n(h, n + 1, r, r0) ∧ n < n + 1

• Proof step 8:

  ∃ r1. reachable-n(h, n, r, r1) ∧ reachable-n(h, n + 1 - n, r1, r0) ⊦ reachable-n(h, n + 1, r, r0) ↔ (∃ r1. reachable-n(h, n, r, r1) ∧ reachable-1(h, r1, r0))

Rule argument

Additional information

Used terms: r0, h, n + 1, n, r

Proof step 2 from proof reachable-n-rec-rev (previous step) (back to tree)

Lemma reach-n-split

Proof step 3 from proof reachable-n-rec-rev (previous step) (back to tree)

User applied rule case distinction

And obtained the following new goals

• Proof step 4:

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

• Proof step 5:

  ¬ reachable-n(h, n + 1, r, r0), ∃ r1. reachable-n(h, n, r, r1) ∧ reachable-1(h, r1, r0) ⊦ reachable-n(h, n + 1, r, r0) ∧ n < n + 1

Rule argument

Additional information

Proof step 4 from proof reachable-n-rec-rev (previous step) (back to tree)

User applied rule case distinction

And closed the goal!

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)); reachable-1-def: ⊦ reachable-1(h, r, r0) ↔ r ≠ null ∧ r0 ≠ null ∧ r ∈ h ∧ r0 ∈ h ∧ h[r].nxt = r0; ⊦ m < n + 1 ↔ m ≤ n; (s) ⊦ m ≤ n ↔ ¬ n < m; (ss) ⊦ ¬ n < n; (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 reachable-n-rec-rev (previous step) (back to tree)

User applied rule exists left

And obtained the following new goals

• Proof step 6:

  reachable-1(h, r1, r0), reachable-n(h, n, r, r1), ¬ reachable-n(h, n + 1, r, r0) ⊦ reachable-n(h, n + 1, r, r0) ∧ n < n + 1

Rule argument

Additional information

Proof step 6 from proof reachable-n-rec-rev (previous step) (back to tree)

User applied rule apply lemma

And obtained the following new goals

• Proof step 7:

  ⊦ reachable-n(h, n, r, r0) ∧ reachable-n(h, n0, r0, r1) → (reachable-n(h, n + n0, r, r1) ↔ true)

Rule argument

Additional information

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

Proof step 7 from proof reachable-n-rec-rev (previous step) (back to tree)

Lemma reachable-n-trans

Proof step 8 from proof reachable-n-rec-rev (previous step) (back to tree)

User applied rule case distinction

And obtained the following new goals

• Proof step 9:

  reachable-n(h, n + 1, r, r0), ∃ r1. reachable-n(h, n, r, r1) ∧ reachable-n(h, n + 1 - n, r1, r0) ⊦ ∃ r1. reachable-n(h, n, r, r1) ∧ reachable-1(h, r1, r0)

• Proof step 12:

  ¬ reachable-n(h, n + 1, r, r0), ∃ r1. reachable-n(h, n, r, r1) ∧ reachable-n(h, n + 1 - n, r1, r0), ∃ r1. reachable-n(h, n, r, r1) ∧ reachable-1(h, r1, r0) ⊦

Rule argument

Additional information

Proof step 9 from proof reachable-n-rec-rev (previous step) (back to tree)

User applied rule exists left

And obtained the following new goals

• Proof step 10:

  reachable-n(h, n + 1, r, r0), reachable-n(h, n, r, r1), reachable-n(h, n + 1 - n, r1, r0) ⊦ ∃ r1. reachable-n(h, n, r, r1) ∧ reachable-1(h, r1, r0)

Rule argument

Additional information

Proof step 10 from proof reachable-n-rec-rev (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 11:

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

Rule argument

Additional information

Used simplifier rules: reachable-n-1: ⊦ reachable-n(h, 1, r, r0) ↔ reachable-1(h, r, r0); reachable-n-rec: ⊦ reachable-n(h, n + 1, r, r0) ↔ (∃ r1. reachable-1(h, r, r1) ∧ reachable-n(h, n, r1, r0)); 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 ⊦ m + n - m = n; (s)

Proof step 11 from proof reachable-n-rec-rev (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: r1

Proof step 12 from proof reachable-n-rec-rev (previous step) (back to tree)

User applied rule exists left

And obtained the following new goals

• Proof step 13:

  reachable-n(h, n, r, r1), reachable-n(h, n + 1 - n, r1, r0), ¬ reachable-n(h, n + 1, r, r0), ∃ r1. reachable-n(h, n, r, r1) ∧ reachable-1(h, r1, r0) ⊦

Rule argument

Additional information

Proof step 13 from proof reachable-n-rec-rev (previous step) (back to tree)

User applied rule apply lemma

And obtained the following new goals

• Proof step 14:

  ⊦ reachable-n(h, n, r, r0) ∧ reachable-n(h, n0, r0, r1) → (reachable-n(h, n + n0, r, r1) ↔ true)

Rule argument

Additional information

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

Proof step 14 from proof reachable-n-rec-rev (previous step) (back to tree)

Lemma reachable-n-trans