Proof step 1 from proof removed-stays-reachable (conclusion) (back to tree)

System applied rule normalize

And obtained the following new goals

• Proof step 2:

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

Rule argument

Additional information

Proof step 2 from proof removed-stays-reachable (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 3:

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

Rule argument

Additional information

Used simplifier rules: reach-alloc: ⊦ reachable(r, r1, h) → r1 ∈ h;

Proof step 3 from proof removed-stays-reachable (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 4:

  reachable(r, r0, h), (h(r0)).nxt ≠ null, (h(r0)).nxt ∈ h, (h(r0)).nxt ≠ (h((h(r0)).nxt)).nxt, ce.nxt = (h((h(r0)).nxt)).nxt ⊦ reachable(r, (h(r0)).nxt, h(r0 := ce)) ↔ (h((h(r0)).nxt)).nxt = (h(r0)).nxt ∨ r ≠ r0 ∧ r = (h(r0)).nxt ∨ (∃ x. path(r ' + x + (h(r0)).nxt ', h) ∧ r0 ≠ r ∧ ¬ r0 ∈ x) ∨ (∃ x. path((h(r0)).nxt ' + x + (h(r0)).nxt ', h) ∧ ¬ r0 ∈ x)

• Proof step 5:

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

• Proof step 10:

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

Rule argument

Additional information

Used terms: ce, r0, h, r

Proof step 4 from proof removed-stays-reachable (previous step) (back to tree)

Lemma rem-stays-reachable-aux

Proof step 5 from proof removed-stays-reachable (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 6:

  ce.nxt = (h(ce.nxt)).nxt, ce.nxt = (h(r0)).nxt, ce.nxt ≠ null, reachable(r, r0, h), r0 ∈ h, ce.nxt ∈ h, ¬ reachable(r, ce.nxt, h(r0 := ce)) ⊦

Rule argument

Additional information

Proof step 6 from proof removed-stays-reachable (previous step) (back to tree)

User applied rule cut formula

And obtained the following new goals

• Proof step 7:

  ce.nxt = (h(r0)).nxt, ce.nxt = (h(ce.nxt)).nxt, ce.nxt ≠ null, reachable(r, r0, h), reachable(r, r0, h(r0 := ce)), ce.nxt ∈ h, r0 ∈ h, ¬ reachable(r, ce.nxt, h(r0 := ce)) ⊦

Rule argument

Additional information

Used simplifier rules: changenonnxt-reachable: ⊦ reachable(r, r0, h) ∧ ce.nxt = (h(r1)).nxt → (reachable(r, r0, h(r1 := ce)) ↔ true); Used formulas: reachable(r, r0, h(r0 := ce))

Proof step 7 from proof removed-stays-reachable (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 8:

  ce.nxt = (h(r0)).nxt, ce.nxt = (h(ce.nxt)).nxt, ce.nxt ≠ null, reachable(r, r0, h), reachable(r, r0, h(r0 := ce)), ce.nxt ∈ h, r0 ∈ h, ¬ reachable(r, ce.nxt, h(r0 := ce)) ⊦

Rule argument

Additional information

Used simplifier rules: reach-alloc: ⊦ reachable(r, r1, h) → r1 ∈ h; ⊦ a ∈ st(a := d); (s)

Proof step 8 from proof removed-stays-reachable (previous step) (back to tree)

User applied rule apply lemma

And obtained the following new goals

• Proof step 9:

  ⊦ reachable(r, r1, h) → (reachable(r, (h(r1)).nxt, h) ↔ ¬((h(r1)).nxt = null ∨ ¬ (h(r1)).nxt ∈ h))

Rule argument

Additional information

Used simplifier rules: changenonnxt-reachable: ⊦ reachable(r, r0, h) ∧ ce.nxt = (h(r1)).nxt → (reachable(r, r0, h(r1 := ce)) ↔ true); endnotinH-notreachable: ⊦ ¬ r0 ∈ h → (reachable(r, r0, h) ↔ false); ⊦ st(a := d)(a) = d; (s) ⊦ a ∈ st(b := d) ↔ a = b ∨ a ∈ st; (ws) Used terms: r, r0, h(r0 := ce)

Proof step 9 from proof removed-stays-reachable (previous step) (back to tree)

Lemma reach-reachnext

Proof step 10 from proof removed-stays-reachable (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 11:

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

Rule argument

Additional information

Proof step 11 from proof removed-stays-reachable (previous step) (back to tree)

User applied rule apply lemma

And obtained the following new goals

• Proof step 12:

  r0 ∈ h, (h(r0)).nxt ≠ null, (h(r0)).nxt ∈ h, (h(r0)).nxt ≠ (h((h(r0)).nxt)).nxt ⊦ reachable((h((h(r0)).nxt)).nxt, (h(r0)).nxt, h) ∧ ¬ reachable((h((h(r0)).nxt)).nxt, r0, h) ↔ (∃ x. path((h(r0)).nxt ' + x + (h(r0)).nxt ', h) ∧ ¬ r0 ∈ x)

• Proof step 13:

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

Rule argument

Additional information

Used terms: r0, h

Proof step 12 from proof removed-stays-reachable (previous step) (back to tree)

Lemma rem-stays-reachable-aux1

Proof step 13 from proof removed-stays-reachable (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 14:

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

Rule argument

Additional information

Proof step 14 from proof removed-stays-reachable (previous step) (back to tree)

User applied rule apply lemma

And obtained the following new goals

• Proof step 15:

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

• Proof step 16:

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

Rule argument

Additional information

Used terms: r, r0, h

Proof step 15 from proof removed-stays-reachable (previous step) (back to tree)

Lemma rem-stays-reachable-aux2

Proof step 16 from proof removed-stays-reachable (previous step) (back to tree)

User applied rule case distinction

And obtained the following new goals

• Proof step 17:

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

• Proof step 25:

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

Rule argument

Additional information

Proof step 17 from proof removed-stays-reachable (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 18:

  ce.nxt = (h((h(r0)).nxt)).nxt, (h(r0)).nxt ≠ null, (h(r0)).nxt ≠ ce.nxt, reachable(r, r0, h), (h(r0)).nxt ∈ h, r0 ∈ h, (∃ r1. reachable(r, r1, h) ∧ (h(r0)).nxt = (h(r1)).nxt ∧ ¬ reachable(r0, r1, h)) ↔ (∃ x. path(r ' + x + (h(r0)).nxt ', h) ∧ r0 ≠ r ∧ ¬ r0 ∈ x), (h(r0)).nxt = r0 ∨ r ≠ (h(r0)).nxt, path(r ' + x + (h(r0)).nxt ', h) ∧ r0 ≠ r ∧ ¬ r0 ∈ x ∨ path((h(r0)).nxt ' + x0 + (h(r0)).nxt ', h) ∧ ¬ r0 ∈ x0 ⊦ ∃ r1. reachable(r, r1, h) ∧ (h(r1)).nxt = (h(r0)).nxt ∧ ¬ reachable(r0, r1, h), ∃ x. path((h(r0)).nxt ' + x + (h(r0)).nxt ', h) ∧ ¬ r0 ∈ x, reachable(ce.nxt, (h(r0)).nxt, h) ∧ ¬ reachable(ce.nxt, r0, h)

Rule argument

Additional information

Proof step 18 from proof removed-stays-reachable (previous step) (back to tree)

User applied rule case distinction

And obtained the following new goals

• Proof step 19:

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

• Proof step 23:

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

Rule argument

Additional information

Proof step 19 from proof removed-stays-reachable (previous step) (back to tree)

User applied rule case distinction

And obtained the following new goals

• Proof step 20:

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

• Proof step 22:

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

Rule argument

Additional information

Proof step 20 from proof removed-stays-reachable (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 21:

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

Rule argument

Additional information

Proof step 21 from proof removed-stays-reachable (previous step) (back to tree)

Heuristic quantifier closing applied rule exists right

And closed the goal!

Rule argument

Additional information

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

Proof step 22 from proof removed-stays-reachable (previous step) (back to tree)

Heuristic quantifier closing applied rule exists right

And closed the goal!

Rule argument

Additional information

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

Proof step 23 from proof removed-stays-reachable (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 24:

  (h(r0)).nxt = (h(r1)).nxt, ce.nxt = (h((h(r1)).nxt)).nxt, (h(r1)).nxt ≠ null, (h(r1)).nxt ≠ ce.nxt, r ≠ (h(r1)).nxt, r0 ≠ r, path(r ' + x1 + (h(r1)).nxt ', h), reachable(r, r1, h), reachable(r, r0, h), (h(r1)).nxt ∈ h, r0 ∈ h, r1 ∈ h, ¬ reachable(r0, r1, h), ¬ r0 ∈ x1, path(r ' + x + (h(r1)).nxt ', h) ∧ ¬ r0 ∈ x ∨ path((h(r1)).nxt ' + x0 + (h(r1)).nxt ', h) ∧ ¬ r0 ∈ x0 ⊦ ∃ r1. reachable(r, r1, h) ∧ (h(r1)).nxt = (h(r0)).nxt ∧ ¬ reachable(r0, r1, h), ∃ x. path((h(r1)).nxt ' + x + (h(r1)).nxt ', h) ∧ ¬ r0 ∈ x, reachable(ce.nxt, (h(r1)).nxt, h) ∧ ¬ reachable(ce.nxt, r0, h)

Rule argument

Additional information

Used simplifier rules: reach-alloc: ⊦ reachable(r, r1, h) → r1 ∈ h;

Proof step 24 from proof removed-stays-reachable (previous step) (back to tree)

Heuristic quantifier closing applied rule exists right

And closed the goal!

Rule argument

Additional information

Used terms: r1

Proof step 25 from proof removed-stays-reachable (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 26:

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

Rule argument

Additional information

Used simplifier rules: reach-alloc: ⊦ reachable(r, r1, h) → r1 ∈ h;

Proof step 26 from proof removed-stays-reachable (previous step) (back to tree)

User applied rule exists right

And closed the goal!

Rule argument

Additional information

Used terms: r1