Proof step 1 from proof linearity (conclusion) (back to tree)

System applied rule normalize

And obtained the following new goals

• Proof step 2:

  reachable(r, r1, h), reachable(r, r0, h), ¬ reachable(r0, r1, h), ¬ reachable(r1, r0, h) ⊦

Rule argument

Additional information

Proof step 2 from proof linearity (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 3:

  reachable(r, r0, h), reachable(r, r1, h), ¬ reachable(r0, r1, h), ¬ reachable(r1, r0, h) ⊦

Rule argument

Additional information

Proof step 3 from proof linearity (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 4:

  ⊦ reachable(r, r0, h) ↔ (∃ x. path(r ' + x, h) ∧ (r ' + x).last = r0)

• Proof step 5:

  reachable(r, r1, h), ¬ reachable(r0, r1, h), ¬ reachable(r1, r0, h), ∃ x. path(r ' + x, h) ∧ (r ' + x).last = r0 ⊦

Rule argument

Additional information

Used terms: h, r0, r

Proof step 4 from proof linearity (previous step) (back to tree)

Lemma reachable-def

Proof step 5 from proof linearity (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 6:

  path(r ' + x, h), reachable(r, r1, h), ¬ reachable((r ' + x).last, r1, h), ¬ reachable(r1, (r ' + x).last, h) ⊦

Rule argument

Additional information

Proof step 6 from proof linearity (previous step) (back to tree)

User applied rule induction

And obtained the following new goals

• Proof step 7:

  path(r ' + x, h), reachable(r, r1, h), ¬ reachable(r1, (r ' + x).last, h), ¬ reachable((r ' + x).last, r1, h), ∀ x0, r, h, r1. # x0 < # x → path(r ' + x0, h) ∧ reachable(r, r1, h) ∧ ¬ reachable((r ' + x0).last, r1, h) ∧ ¬ reachable(r1, (r ' + x0).last, h) → false ⊦

Rule argument

Additional information

Used simplifier rules: <; (wellfounded) Used terms: # x

Proof step 7 from proof linearity (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 8:

  path(r ' + x, h), reachable(r, r1, h), ¬ reachable(r1, (r ' + x).last, h), ¬ reachable((r ' + x).last, r1, h), ∀ x0, r, h, r1. # x0 < # x → path(r ' + x0, h) ∧ reachable(r, r1, h) ∧ ¬ reachable((r ' + x0).last, r1, h) ∧ ¬ reachable(r1, (r ' + x0).last, h) → false ⊦

Rule argument

Additional information

Proof step 8 from proof linearity (previous step) (back to tree)

User applied rule cut formula

And obtained the following new goals

• Proof step 9:

  x ≠ [], path(r ' + x, h), reachable(r, r1, h), ¬ reachable(r1, (r ' + x).last, h), ¬ reachable((r ' + x).last, r1, h), ∀ x0, r, h, r1. # x0 < # x → path(r ' + x0, h) ∧ reachable(r, r1, h) ∧ ¬ reachable((r ' + x0).last, r1, h) ∧ ¬ reachable(r1, (r ' + x0).last, h) → false ⊦

Rule argument

Additional information

Used simplifier rules: path-one: ⊦ path(r ', h) ↔ r ∈ h ∧ r ≠ null; ⊦ x + [] = x; (s) a: ⊦ (x + y) + z = x + y + z; from specification list[reflist] ⊦ a '.last = a; (s) Used formulas: x = []

Proof step 9 from proof linearity (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 10:

  x ≠ [], path(r ' + x, h), reachable(r, r1, h), ¬ reachable(r1, x.last, h), ¬ reachable(x.last, r1, h), ∀ x0, r, h, r1. # x0 < # x → path(r ' + x0, h) ∧ reachable(r, r1, h) ∧ ¬ reachable((r ' + x0).last, r1, h) ∧ ¬ reachable(r1, (r ' + x0).last, h) → false ⊦

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 10 from proof linearity (previous step) (back to tree)

User applied rule apply elim lemma

And obtained the following new goals

• Proof step 11:

  x = x1 + r0 ', x ≠ [], path(r ' + x, h), reachable(r, r1, h), ¬ reachable(r1, r0, h), ¬ reachable(r0, r1, h), ∀ x0, r, h, r1. # x0 < # x → path(r ' + x0, h) ∧ reachable(r, r1, h) ∧ ¬ reachable((r ' + x0).last, r1, h) ∧ ¬ reachable(r1, (r ' + x0).last, h) → false ⊦

Rule argument

Additional information

Used simplifier rules: x ≠ [] ⊦ a = x.last ∧ y = x.butlast ↔ x = y + a '; (elim) Used terms: x, a, y

Proof step 11 from proof linearity (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 12:

  path(r ' + x1 + r0 ', h), reachable(r, r1, h), ¬ reachable(r1, r0, h), ¬ reachable(r0, r1, h), ∀ x0, r, h, r1. # x0 < #(x1 + r0 ') → path(r ' + x0, h) ∧ reachable(r, r1, h) ∧ ¬ reachable((r ' + x0).last, r1, h) ∧ ¬ reachable(r1, (r ' + x0).last, h) → false ⊦

Rule argument

Additional information

Used simplifier rules: a: ⊦ (x + y) + z = x + y + z; from specification list[reflist] ⊦ x + a ' ≠ []; (s)

Proof step 12 from proof linearity (previous step) (back to tree)

User applied rule apply lemma

And obtained the following new goals

• Proof step 13:

  ⊦ path(r ' + x + r0 ', h) ↔ path(r ' + x, h) ∧ h[(r ' + x).last].nxt = r0 ∧ r0 ∈ h ∧ r0 ≠ null

• Proof step 14:

  path(r ' + x1 + r0 ', h) ↔ path(r ' + x1, h) ∧ h[(r ' + x1).last].nxt = r0 ∧ r0 ∈ h ∧ r0 ≠ null, path(r ' + x1 + r0 ', h), reachable(r, r1, h), ¬ reachable(r1, r0, h), ¬ reachable(r0, r1, h), ∀ x0, r, h, r1. # x0 < #(x1 + r0 ') → path(r ' + x0, h) ∧ reachable(r, r1, h) ∧ ¬ reachable((r ' + x0).last, r1, h) ∧ ¬ reachable(r1, (r ' + x0).last, h) → false ⊦

Rule argument

Additional information

Used terms: r, x1, r0, h

Proof step 13 from proof linearity (previous step) (back to tree)

Lemma path-split-last

Proof step 14 from proof linearity (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 15:

  h[(r ' + x1).last].nxt ≠ null, path(r ' + x1, h), path(r ' + x1 + h[(r ' + x1).last].nxt ', h), reachable(r, r1, h), h[(r ' + x1).last].nxt ∈ h, ¬ reachable(h[(r ' + x1).last].nxt, r1, h), ¬ reachable(r1, h[(r ' + x1).last].nxt, h), ∀ x0, r1, h0, r2. # x0 < #(x1 + h[(r ' + x1).last].nxt ') → path(r1 ' + x0, h0) ∧ reachable(r1, r2, h0) ∧ ¬ reachable((r1 ' + x0).last, r2, h0) ∧ ¬ reachable(r2, (r1 ' + x0).last, h0) → false ⊦

Rule argument

Additional information

Used simplifier rules: a: ⊦ (x + y) + z = x + y + z; from specification list[reflist]

Proof step 15 from proof linearity (previous step) (back to tree)

User applied rule apply induction

And obtained the following new goals

• Proof step 16:

  h[(r ' + x1).last].nxt ≠ null, path(r ' + x1 + h[(r ' + x1).last].nxt ', h), path(r ' + x1, h), reachable(r, r1, h), h[(r ' + x1).last].nxt ∈ h, ¬ reachable(h[(r ' + x1).last].nxt, r1, h), ¬ reachable(r1, h[(r ' + x1).last].nxt, h), ∀ x0, r1, h0, r2. # x0 < #(x1 + h[(r ' + x1).last].nxt ') → path(r1 ' + x0, h0) ∧ reachable(r1, r2, h0) ∧ ¬ reachable((r1 ' + x0).last, r2, h0) ∧ ¬ reachable(r2, (r1 ' + x0).last, h0) → false ⊦ path(r ' + x1, h) ∧ reachable(r, r1, h) ∧ ¬ reachable((r ' + x1).last, r1, h) ∧ ¬ reachable(r1, (r ' + x1).last, h)

Rule argument

Additional information

Used simplifier rules: ⊦ #(x + y) = # x + # y; (s) ⊦ # a ' = 0 +1; (s) a: ⊦ (x + y) + z = x + y + z; from specification list[reflist] ⊦ m < n + 1 ↔ ¬ n < m; (s) ⊦ ¬ n < n; (s) a: ⊦ (m + n0) + n1 = m + n0 + n1; from specification nat-basic c: ⊦ m + n = n + m; from specification nat-basic Used terms: x1, r, h, r1

Proof step 16 from proof linearity (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 17:

  h[(r ' + x1).last].nxt ≠ null, path(r ' + x1 + h[(r ' + x1).last].nxt ', h), path(r ' + x1, h), reachable(r, r1, h), reachable((r ' + x1).last, r1, h), h[(r ' + x1).last].nxt ∈ h, ¬ reachable(r1, h[(r ' + x1).last].nxt, h), ¬ reachable(h[(r ' + x1).last].nxt, r1, h), ¬ reachable(r1, (r ' + x1).last, h), ∀ x0, r1, h0, r2. # x0 < #(x1 + h[(r ' + x1).last].nxt ') → path(r1 ' + x0, h0) ∧ reachable(r1, r2, h0) ∧ ¬ reachable((r1 ' + x0).last, r2, h0) ∧ ¬ reachable(r2, (r1 ' + x0).last, h0) → false ⊦

Rule argument

Additional information

Used simplifier rules: reach-reachnext: ⊦ reachable(r, r1, h) → (reachable(r, h[r1].nxt, h) ↔ ¬(h[r1].nxt = null ∨ ¬ h[r1].nxt ∈ h));

Proof step 17 from proof linearity (previous step) (back to tree)

User applied rule apply lemma

And obtained the following new goals

• Proof step 18:

  ⊦ reachable(r, r0, h) ∧ r ≠ r0 → (reachable(h[r].nxt, r0, h) ↔ true)

Rule argument

Additional information

Used terms: (r ' + x1).last, r1, h

Proof step 18 from proof linearity (previous step) (back to tree)

Lemma fromnext-reachable