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

System applied rule normalize

And obtained the following new goals

• Proof step 2:

  x ≠ y, path(r ' + y, h), path(r ' + x, h) ⊦ ∃ r0, y0. x = y + r0 ' + y0, ∃ r0, x0. y = x + r0 ' + x0

Rule argument

Additional information

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

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 3:

  x ≠ y, path(r ' + x, h), path(r ' + y, h) ⊦ ∃ r0, x0. y = x + r0 ' + x0, ∃ r0, y0. x = y + r0 ' + y0

Rule argument

Additional information

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

User applied rule structural induction

And obtained the following new goals

• Proof step 4:

  [] ≠ y, path(r ' + y, h), path(r ' + [], h) ⊦ ∃ r0, y0. [] = y + r0 ' + y0, ∃ r0, x0. y = [] + r0 ' + x0

• Proof step 8:

  r0 + x0 ≠ y, path(r ' + y, h), path(r ' + (r0 + x0), h), ∀ y, r, h. x0 ≠ y ∧ path(r ' + x0, h) ∧ path(r ' + y, h) → (∃ r0, x1. y = x0 + r0 ' + x1) ∨ (∃ r0, y0. x0 = y + r0 ' + y0) ⊦ ∃ r, y0. r0 + x0 = y + r ' + y0, ∃ r, x1. y = (r0 + x0) + r ' + x1

Rule argument

Additional information

Used simplifier rules: list('a) freely generated by [], +;;

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

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 5:

  [] ≠ y, r ≠ null, path(r ' + y, h), r ∈ h ⊦ ∃ r0, x0. y = r0 ' + x0

Rule argument

Additional information

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

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

User applied rule constructor cut

And obtained the following new goals

• Proof step 6:

  y = r1 + y0, [] ≠ y, r ≠ null, path(r ' + y, h), r ∈ h ⊦ ∃ r0, x0. y = r0 ' + x0

Rule argument

Additional information

Used simplifier rules: list('a) freely generated by [], +;;

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

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 7:

  r ≠ null, path(h[r].nxt ' + y0, h), r ∈ h ⊦ ∃ r0, x0. h[r].nxt ' + y0 = r0 ' + x0

Rule argument

Additional information

Used simplifier rules: path-cons: ⊦ path(r ' + r0 ' + x, h) ↔ r ∈ h ∧ r ≠ null ∧ h[r].nxt = r0 ∧ path(r0 ' + x, h); ⊦ a + x = a ' + x; (s) a: ⊦ (x + y) + z = x + y + z; from specification polylist ⊦ a ' + x ≠ []; (s)

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

Heuristic quantifier closing applied rule exists right

And closed the goal!

Rule argument

Additional information

Used terms: h[r].nxt, y0

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

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 9:

  h[r].nxt ' + x0 ≠ y, r ≠ null, path(h[r].nxt ' + x0, h), path(r ' + y, h), r ∈ h, ∀ y, r, h. x0 ≠ y ∧ path(r ' + x0, h) ∧ path(r ' + y, h) → (∃ r0, x1. y = x0 + r0 ' + x1) ∨ (∃ r0, y0. x0 = y + r0 ' + y0) ⊦ ∃ r1, y0. h[r].nxt ' + x0 = y + r1 ' + y0, ∃ r1, x1. y = (h[r].nxt ' + x0) + r1 ' + x1

Rule argument

Additional information

Used simplifier rules: path-cons: ⊦ path(r ' + r0 ' + x, h) ↔ r ∈ h ∧ r ≠ null ∧ h[r].nxt = r0 ∧ path(r0 ' + x, h); ⊦ a + x = a ' + x; (s) a: ⊦ (x + y) + z = x + y + z; from specification polylist

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

User applied rule constructor cut

And obtained the following new goals

• Proof step 10:

  y = [], h[r].nxt ' + x0 ≠ y, r ≠ null, path(r ' + y, h), path(h[r].nxt ' + x0, h), r ∈ h, ∀ y, r, h. x0 ≠ y ∧ path(r ' + x0, h) ∧ path(r ' + y, h) → (∃ r0, x1. y = x0 + r0 ' + x1) ∨ (∃ r0, y0. x0 = y + r0 ' + y0) ⊦ ∃ r1, x1. y = (h[r].nxt ' + x0) + r1 ' + x1, ∃ r1, y0. h[r].nxt ' + x0 = y + r1 ' + y0

• Proof step 12:

  y = r2 + y1, h[r].nxt ' + x0 ≠ y, r ≠ null, path(r ' + y, h), path(h[r].nxt ' + x0, h), r ∈ h, ∀ y, r, h. x0 ≠ y ∧ path(r ' + x0, h) ∧ path(r ' + y, h) → (∃ r0, x1. y = x0 + r0 ' + x1) ∨ (∃ r0, y0. x0 = y + r0 ' + y0) ⊦ ∃ r1, x1. y = (h[r].nxt ' + x0) + r1 ' + x1, ∃ r1, y0. h[r].nxt ' + x0 = y + r1 ' + y0

Rule argument

Additional information

Used simplifier rules: list('a) freely generated by [], +;;

Proof step 10 from proof linearity-path (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 11:

  r ≠ null, path(h[r].nxt ' + x0, h), r ∈ h, ∀ y, r, h. x0 ≠ y ∧ path(r ' + x0, h) ∧ path(r ' + y, h) → (∃ r0, x1. y = x0 + r0 ' + x1) ∨ (∃ r0, y0. x0 = y + r0 ' + y0) ⊦ ∃ r1, y0. h[r].nxt ' + x0 = r1 ' + y0

Rule argument

Additional information

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

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

Heuristic quantifier closing applied rule exists right

And closed the goal!

Rule argument

Additional information

Used terms: h[r].nxt, x0

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

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 13:

  r ≠ null, x0 ≠ y1, path(h[r].nxt ' + y1, h), path(h[r].nxt ' + x0, h), r ∈ h, ∀ y, r, h. x0 ≠ y ∧ path(r ' + x0, h) ∧ path(r ' + y, h) → (∃ r0, x1. y = x0 + r0 ' + x1) ∨ (∃ r0, y0. x0 = y + r0 ' + y0) ⊦ ∃ r1, x1. y1 = x0 + r1 ' + x1, ∃ r1, y0. x0 = y1 + r1 ' + y0

Rule argument

Additional information

Used simplifier rules: path-cons: ⊦ path(r ' + r0 ' + x, h) ↔ r ∈ h ∧ r ≠ null ∧ h[r].nxt = r0 ∧ path(r0 ' + x, h); a: ⊦ (x + y) + z = x + y + z; from specification polylist ⊦ a ' + x = a0 ' + y ↔ a = a0 ∧ x = y; (ws) ⊦ a + x = a ' + x; (s)

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

User applied rule all left

And obtained the following new goals

• Proof step 14:

  r ≠ null, x0 ≠ y1, path(h[r].nxt ' + x0, h), path(h[r].nxt ' + y1, h), r ∈ h, x0 ≠ y1 ∧ path(h[r].nxt ' + x0, h) ∧ path(h[r].nxt ' + y1, h) → (∃ r0, x1. y1 = x0 + r0 ' + x1) ∨ (∃ r0, y0. x0 = y1 + r0 ' + y0) ⊦ ∃ r1, y0. x0 = y1 + r1 ' + y0, ∃ r1, x1. y1 = x0 + r1 ' + x1

Rule argument

Additional information

Used terms: y1, h[r].nxt, h

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

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 15:

  r ≠ null, x0 ≠ y1, path(h[r].nxt ' + y1, h), path(h[r].nxt ' + x0, h), r ∈ h, y1 = x0 + r0 ' + x1 ∨ x0 = y1 + r1 ' + y0 ⊦ ∃ r1, x1. y1 = x0 + r1 ' + x1, ∃ r1, y0. x0 = y1 + r1 ' + y0

Rule argument

Additional information

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

User applied rule exists right

And obtained the following new goals

• Proof step 16:

  r ≠ null, x0 ≠ y1, y1 ≠ x0 + r0 ' + x1, path(h[r].nxt ' + x0, h), path(h[r].nxt ' + y1, h), r ∈ h, y1 = x0 + r0 ' + x1 ∨ x0 = y1 + r1 ' + y0 ⊦ ∃ r1, y0. x0 = y1 + r1 ' + y0

Rule argument

Additional information

Used terms: r0, x1

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

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 17:

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

Rule argument

Additional information

Used simplifier rules: a: ⊦ (x + y) + z = x + y + z; from specification polylist ⊦ # x = # z → (x + y = z + y0 ↔ x = z ∧ y = y0); (ws) ⊦ a ' + x ≠ []; (s) ⊦ x = x + y ↔ y = []; (s)

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

Heuristic quantifier closing applied rule exists right

And closed the goal!

Rule argument

Additional information

Used terms: r1, y0