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

User applied rule apply lemma

And obtained the following new goals

• Proof step 2:

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

• Proof step 3:

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

Rule argument

Additional information

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

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

Lemma reachable-n-rec-rev

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

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 4:

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

Rule argument

Additional information

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

User applied rule case distinction

And obtained the following new goals

• Proof step 5:

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

• Proof step 24:

  ¬ reachable-n(h, n + 2, r, r0), reachable-n(h, (n + 1) + 1, r, r0) ↔ (∃ r1. reachable-n(h, n + 1, r, r1) ∧ reachable-1(h, r1, r0)), ∃ r1. reachable-n(h, n, r, r1) ∧ reachable-1(h, r1, h[r1].nxt) ∧ reachable-1(h, h[r1].nxt, r0) ⊦

Rule argument

Additional information

Proof step 5 from proof reachable-n-rec-rev2 (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 6:

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

Rule argument

Additional information

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

User applied rule case distinction

And obtained the following new goals

• Proof step 7:

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

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

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

User applied rule exists left

And obtained the following new goals

• Proof step 8:

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

Rule argument

Additional information

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

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 9:

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

• Proof step 10:

  reachable-1(h, r1, r0), reachable-n(h, n + 2, r, r0), reachable-n(h, (n + 1) + 1, r, r0), ∃ r2. reachable-n(h, n, r, r2) ∧ reachable-1(h, r2, r1) ⊦ ∃ r1. reachable-n(h, n, r, r1) ∧ reachable-1(h, r1, h[r1].nxt) ∧ reachable-1(h, h[r1].nxt, r0)

Rule argument

Additional information

Used terms: r1, r, n, h

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

Lemma reachable-n-rec-rev

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

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 11:

  reachable-1(h, r2, r1), reachable-1(h, r1, r0), reachable-n(h, n, r, r2), reachable-n(h, (n + 1) + 1, r, r0), reachable-n(h, n + 2, r, r0) ⊦ ∃ r1. reachable-n(h, n, r, r1) ∧ reachable-1(h, r1, h[r1].nxt) ∧ reachable-1(h, h[r1].nxt, r0)

Rule argument

Additional information

Proof step 11 from proof reachable-n-rec-rev2 (previous step) (back to tree)

User applied rule exists right

And obtained the following new goals

• Proof step 12:

  reachable-1(h, r1, r0), reachable-1(h, r2, r1), reachable-n(h, n + 2, r, r0), reachable-n(h, (n + 1) + 1, r, r0), reachable-n(h, n, r, r2) ⊦ reachable-n(h, n, r, r2) ∧ reachable-1(h, r2, h[r2].nxt) ∧ reachable-1(h, h[r2].nxt, r0)

Rule argument

Additional information

Used terms: r2

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

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 13:

  reachable-1(h, r2, r1), reachable-1(h, r1, r0), reachable-n(h, n, r, r2), reachable-n(h, (n + 1) + 1, r, r0), reachable-n(h, n + 2, r, r0) ⊦ reachable-1(h, r2, h[r2].nxt) ∧ reachable-1(h, h[r2].nxt, r0)

Rule argument

Additional information

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

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 14:

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

• Proof step 15:

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

Rule argument

Additional information

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

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

Lemma reachable-1-def

Proof step 15 from proof reachable-n-rec-rev2 (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 16:

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

Rule argument

Additional information

Proof step 16 from proof reachable-n-rec-rev2 (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 17:

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

• Proof step 18:

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

Rule argument

Additional information

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

Proof step 17 from proof reachable-n-rec-rev2 (previous step) (back to tree)

Lemma reachable-1-def

Proof step 18 from proof reachable-n-rec-rev2 (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 19:

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

Rule argument

Additional information

Proof step 19 from proof reachable-n-rec-rev2 (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 20:

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

• Proof step 21:

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

Rule argument

Additional information

Used terms: r0, r1, h

Proof step 20 from proof reachable-n-rec-rev2 (previous step) (back to tree)

Lemma reachable-1-def

Proof step 21 from proof reachable-n-rec-rev2 (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 22:

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

Rule argument

Additional information

Proof step 22 from proof reachable-n-rec-rev2 (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 23:

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

Rule argument

Additional information

Used terms: r1, r2, h

Proof step 23 from proof reachable-n-rec-rev2 (previous step) (back to tree)

Lemma reachable-1-def

Proof step 24 from proof reachable-n-rec-rev2 (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 25:

  reachable-1(h, r1, h[r1].nxt), reachable-1(h, h[r1].nxt, r0), reachable-n(h, n, r, r1), ¬ reachable-n(h, n + 2, r, r0), reachable-n(h, (n + 1) + 1, r, r0) ↔ (∃ r1. reachable-n(h, n + 1, r, r1) ∧ reachable-1(h, r1, r0)) ⊦

Rule argument

Additional information

Proof step 25 from proof reachable-n-rec-rev2 (previous step) (back to tree)

User applied rule case distinction

And obtained the following new goals

• Proof step 26:

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

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)); c: ⊦ m + n = n + m; from specification nat-basic a: ⊦ (m + n0) + n1 = m + n0 + n1; from specification nat-basic

Proof step 26 from proof reachable-n-rec-rev2 (previous step) (back to tree)

User applied rule exists right

And obtained the following new goals

• Proof step 27:

  reachable-1(h, r1, h[r1].nxt), reachable-1(h, h[r1].nxt, r0), reachable-n(h, n, r, r1), ¬ reachable-n(h, (n + 1) + 1, r, r0), ¬ reachable-n(h, n + 2, r, r0) ⊦ reachable-n(h, n + 1, r, h[r1].nxt) ∧ reachable-1(h, h[r1].nxt, r0)

Rule argument

Additional information

Used terms: h[r1].nxt

Proof step 27 from proof reachable-n-rec-rev2 (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 28:

  reachable-1(h, h[r1].nxt, r0), reachable-1(h, r1, h[r1].nxt), reachable-n(h, n, r, r1), ¬ reachable-n(h, (n + 1) + 1, r, r0), ¬ reachable-n(h, n + 2, r, r0), ¬ reachable-n(h, n + 1, r, h[r1].nxt) ⊦

Rule argument

Additional information

Proof step 28 from proof reachable-n-rec-rev2 (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 29:

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

• Proof step 30:

  reachable-1(h, r1, h[r1].nxt), reachable-1(h, h[r1].nxt, r0), reachable-n(h, n, r, r1), ¬ reachable-n(h, (n + 1) + 1, r, r0), ¬ reachable-n(h, n + 2, r, r0), ∀ r2. ¬(reachable-n(h, n, r, r2) ∧ reachable-1(h, r2, h[r1].nxt)) ⊦

Rule argument

Additional information

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

Proof step 29 from proof reachable-n-rec-rev2 (previous step) (back to tree)

Lemma reachable-n-rec-rev

Proof step 30 from proof reachable-n-rec-rev2 (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 31:

  reachable-1(h, h[r1].nxt, r0), reachable-1(h, r1, h[r1].nxt), reachable-n(h, n, r, r1), ¬ reachable-n(h, (n + 1) + 1, r, r0), ¬ reachable-n(h, n + 2, r, r0), ∀ r2. ¬ reachable-n(h, n, r, r2) ∨ ¬ reachable-1(h, r2, h[r1].nxt) ⊦

Rule argument

Additional information

Proof step 31 from proof reachable-n-rec-rev2 (previous step) (back to tree)

Heuristic quantifier closing applied rule all left

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 Used terms: r1