Proof step 1 from proof reachable-split-last (conclusion) (back to tree)

System applied rule normalize

And obtained the following new goals

• Proof step 2:

  r ≠ r0 ⊦ reachable(r, r0, h) ↔ (∃ r1. reachable(r, r1, h) ∧ (h(r1)).nxt = r0 ∧ r0 ∈ h ∧ r0 ≠ null)

Rule argument

Additional information

Proof step 2 from proof reachable-split-last (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 3:

  r ≠ r0 ⊦ reachable(r, r0, h) ↔ (∃ r1. reachable(r, r1, h) ∧ (h(r1)).nxt = r0 ∧ (h(r1)).nxt ∈ h ∧ (h(r1)).nxt ≠ null)

Rule argument

Additional information

Proof step 3 from proof reachable-split-last (previous step) (back to tree)

User applied rule case distinction

And obtained the following new goals

• Proof step 4:

  r ≠ r0, reachable(r, r0, h) ⊦ ∃ r1. reachable(r, r1, h) ∧ (h(r1)).nxt = r0 ∧ (h(r1)).nxt ∈ h ∧ (h(r1)).nxt ≠ null

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 4 from proof reachable-split-last (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 5:

  r ≠ r0, reachable(r, r0, h) ⊦ ∃ r1. reachable(r, r1, h) ∧ (h(r1)).nxt = r0 ∧ (h(r1)).nxt ∈ h ∧ (h(r1)).nxt ≠ null

Rule argument

Additional information

Proof step 5 from proof reachable-split-last (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 6:

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

• Proof step 7:

  r ≠ r0, ∃ x. path(r ' + x, h) ∧ (r ' + x).last = r0 ⊦ ∃ r1. reachable(r, r1, h) ∧ (h(r1)).nxt = r0 ∧ (h(r1)).nxt ∈ h ∧ (h(r1)).nxt ≠ null

Rule argument

Additional information

Used terms: h, r0, r

Proof step 6 from proof reachable-split-last (previous step) (back to tree)

Lemma reachable-def

Proof step 7 from proof reachable-split-last (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 8:

  r ≠ (r ' + x).last, path(r ' + x, h) ⊦ ∃ r1. reachable(r, r1, h) ∧ (h(r1)).nxt = (r ' + x).last ∧ (h(r1)).nxt ∈ h ∧ (h(r1)).nxt ≠ null

Rule argument

Additional information

Proof step 8 from proof reachable-split-last (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 9:

  ⊦ y ≠ [] → (x + y).last = y.last

• Proof step 10:

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

Rule argument

Additional information

Used simplifier rules: ⊦ x + [] = x; (s) a: ⊦ (x + y) + z = x + y + z; from specification polylist ⊦ a '.last = a; (s) Used terms: x, r '

Proof step 9 from proof reachable-split-last (previous step) (back to tree)

A spec-lemma

Proof step 10 from proof reachable-split-last (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 11:

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

Rule argument

Additional information

Proof step 11 from proof reachable-split-last (previous step) (back to tree)

User applied rule apply elim lemma

And obtained the following new goals

• Proof step 12:

  x = y + r0 ', r ≠ r0, x ≠ [], path(r ' + x, h) ⊦ ∃ r1. reachable(r, r1, h) ∧ (h(r1)).nxt = r0 ∧ (h(r1)).nxt ∈ h ∧ (h(r1)).nxt ≠ null

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 12 from proof reachable-split-last (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 13:

  r ≠ r0, path(r ' + y + r0 ', h) ⊦ ∃ r1. reachable(r, r1, h) ∧ (h(r1)).nxt = r0 ∧ (h(r1)).nxt ∈ h ∧ (h(r1)).nxt ≠ null

Rule argument

Additional information

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

Proof step 13 from proof reachable-split-last (previous step) (back to tree)

User applied rule exists right

And obtained the following new goals

• Proof step 14:

  r ≠ r0, path(r ' + y + r0 ', h) ⊦ reachable(r, (r ' + y).last, h) ∧ (h((r ' + y).last)).nxt = r0 ∧ (h((r ' + y).last)).nxt ∈ h ∧ (h((r ' + y).last)).nxt ≠ null

Rule argument

Additional information

Used terms: (r ' + y).last

Proof step 14 from proof reachable-split-last (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 15:

  r ≠ r0, path(r ' + y + r0 ', h) ⊦ reachable(r, (r ' + y).last, h) ∧ (h((r ' + y).last)).nxt ∈ h ∧ (h((r ' + y).last)).nxt ≠ null

Rule argument

Additional information

Used simplifier rules: path-last-nxt: ⊦ path(r ' + x + r0 ', h) → ((h((r ' + x).last)).nxt = r0 ↔ true); a: ⊦ (x + y) + z = x + y + z; from specification polylist

Proof step 15 from proof reachable-split-last (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 16:

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

• Proof step 17:

  (h((r ' + y).last)).nxt = r0, r ≠ r0, r0 ≠ null, path(r ' + y, h), r0 ∈ h ⊦ reachable(r, (r ' + y).last, h) ∧ (h((r ' + y).last)).nxt ∈ h ∧ (h((r ' + y).last)).nxt ≠ null

Rule argument

Additional information

Used terms: h, r0, y, r

Proof step 16 from proof reachable-split-last (previous step) (back to tree)

Lemma path-split-last

Proof step 17 from proof reachable-split-last (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 18:

  (h((r ' + y).last)).nxt ≠ null, r ≠ (h((r ' + y).last)).nxt, path(r ' + y, h), (h((r ' + y).last)).nxt ∈ h, ¬ reachable(r, (r ' + y).last, h) ⊦

Rule argument

Additional information

Proof step 18 from proof reachable-split-last (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 19:

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

• Proof step 20:

  (h((r ' + y).last)).nxt ≠ null, r ≠ (h((r ' + y).last)).nxt, path(r ' + y, h), (h((r ' + y).last)).nxt ∈ h, ∀ x. ¬(path(r ' + x, h) ∧ (r ' + x).last = (r ' + y).last) ⊦

Rule argument

Additional information

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

Proof step 19 from proof reachable-split-last (previous step) (back to tree)

Lemma reachable-def

Proof step 20 from proof reachable-split-last (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 21:

  (h((r ' + y).last)).nxt ≠ null, r ≠ (h((r ' + y).last)).nxt, path(r ' + y, h), (h((r ' + y).last)).nxt ∈ h, ∀ x. ¬ path(r ' + x, h) ∨ (r ' + x).last ≠ (r ' + y).last ⊦

Rule argument

Additional information

Proof step 21 from proof reachable-split-last (previous step) (back to tree)

Heuristic quantifier closing applied rule all left

And closed the goal!

Rule argument

Additional information

Used terms: y