Proof step 1 from proof ll-trav2-next (conclusion) (back to tree)

System applied rule normalize

And obtained the following new goals

• Proof step 2:

  h[r2] = a × r, r2 ≠ null, ((ll-trav(r0, r1, r2, x) * hP))(h), ¬ ((ll-trav(r0, r2, r, x) * hP))(h) ⊦

Rule argument

Additional information

Proof step 2 from proof ll-trav2-next (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 3:

  h[r2] = a × r, r2 ≠ null, ((ll-trav(r0, r1, r2, x) * hP))(h) ⊦ ∃ x0, x1, a0. x = x0 + a0 ' + x1 ∧ ((lls(r0, r2, x0) * r2 => a0 × r * lls(r, null, x1) * hP))(h)

Rule argument

Additional information

Used simplifier rules: ll-trav2-nonnull-def: ⊦ r1 ≠ null → ( ((ll-trav(r0, r1, r2, x) * hP))(h) ↔ (∃ x0, x1, a. x = x0 + (a + x1) ∧ ((lls(r0, r1, x0) * r1 => a × r2 * lls(r2, null, x1) * hP))(h))); sep-com: ⊦ hP0 * hP1 = hP1 * hP0; from specification heap-sep sep-ass: ⊦ (hP0 * hP1) * hP2 = hP0 * hP1 * hP2; from specification heap-sep a: ⊦ (x + y) + z = x + y + z; from specification list ⊦ a + x = a ' + x; (s)

Proof step 3 from proof ll-trav2-next (previous step) (back to tree)

User applied rule cut formula

And obtained the following new goals

• Proof step 4:

  h[r2] = a × r, r1 = null, r2 ≠ null, ((ll-trav(r0, r1, r2, x) * hP))(h) ⊦ ∃ x0, x1, a0. x = x0 + a0 ' + x1 ∧ ((lls(r0, r2, x0) * r2 => a0 × r * lls(r, null, x1) * hP))(h)

• Proof step 8:

  h[r2] = a × r, r1 ≠ null, r2 ≠ null, ((ll-trav(r0, r1, r2, x) * hP))(h) ⊦ ∃ x0, x1, a0. x = x0 + a0 ' + x1 ∧ ((lls(r0, r2, x0) * r2 => a0 × r * lls(r, null, x1) * hP))(h)

Rule argument

Additional information

Used formulas: r1 = null

Proof step 4 from proof ll-trav2-next (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 5:

  h[r0] = a × r, r0 ≠ null, ((lls(r0, null, x) * hP))(h) ⊦ ∃ x0, x1, a0. x = x0 + a0 ' + x1 ∧ ((lls(r0, r0, x0) * r0 => a0 × r * lls(r, null, x1) * hP))(h)

Rule argument

Additional information

Used simplifier rules: ll-trav2-null-def: ⊦ ((ll-trav(r0, null, r2, x) * hP))(h) ↔ r2 = r0 ∧ ((lls(r0, null, x) * hP))(h); sep-com: ⊦ hP0 * hP1 = hP1 * hP0; from specification heap-sep sep-ass: ⊦ (hP0 * hP1) * hP2 = hP0 * hP1 * hP2; from specification heap-sep

Proof step 5 from proof ll-trav2-next (previous step) (back to tree)

User applied rule exists right

And obtained the following new goals

• Proof step 6:

  h[r0] = a × r, r0 ≠ null, ((lls(r0, null, x) * hP))(h) ⊦ x = [] + x.head ' + x.tail ∧ ((lls(r0, r0, []) * r0 => x.head × r * lls(r, null, x.tail) * hP))(h)

Rule argument

Additional information

Used terms: [], x.tail, x.head

Proof step 6 from proof ll-trav2-next (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 7:

  h[r0] = a × r, r0 ≠ null, ((lls(r0, null, x) * hP))(h) ⊦ x = x.head ' + x.tail ∧ ((r0 => x.head × r * lls(r, null, x.tail) * hP))(h)

Rule argument

Additional information

Used simplifier rules: lls-base: ⊦ lls(r0, r1, []) = (emp ∧ ⌜r0 = r1⌝ ); sep-com: ⊦ hP0 * hP1 = hP1 * hP0; from specification heap-sep sep-ass: ⊦ (hP0 * hP1) * hP2 = hP0 * hP1 * hP2; from specification heap-sep ⊦ emp * hP = hP; (s) and-com: ⊦ (hP0 ∧ hP1) = (hP1 ∧ hP0); from specification heap-sep and-ass: ⊦ ((hP0 ∧ hP1) ∧ hP2) = (hP0 ∧ hP1 ∧ hP2); from specification heap-sep ⊦ (true ∧ hP) = hP; (s) ⊦ ⌜true⌝ = true; (s) a: ⊦ (x + y) + z = x + y + z; from specification list ⊦ [] + x = x; (s)

Proof step 7 from proof ll-trav2-next (previous step) (back to tree)

Heuristic elimination applied rule apply elim lemma

And closed the goal!

Rule argument

Additional information

Used simplifier rules: lls-base: ⊦ lls(r0, r1, []) = (emp ∧ ⌜r0 = r1⌝ ); lls-rec: ⊦ lls(r, r1, a ' + x) = _∃(λ r0. r => a × r0 * lls(r0, r1, x)); ⊦ a ' + x ≠ []; (s) ⊦ ((_∃ rP * hP))(h) ↔ (∃ r. ((rP(r) * hP))(h)); (s) sep-ass: ⊦ (hP0 * hP1) * hP2 = hP0 * hP1 * hP2; from specification heap-sep sep-com: ⊦ hP0 * hP1 = hP1 * hP0; from specification heap-sep ⊦ ((r => o0 * hP))(h) → (h[r] = o1 ↔ o0 = o1); (s) ⊦ a × r = a0 × r0 ↔ a = a0 ∧ r = r0; (ws) ⊦ a + x = a ' + x; (s) ⊦ a ' + x = a ' + y ↔ x = y; (s) a: ⊦ (x + y) + z = x + y + z; from specification list ⊦ ⌜false⌝ = false; (s) ⊦ (false ∧ hP) = false; (s) and-ass: ⊦ ((hP0 ∧ hP1) ∧ hP2) = (hP0 ∧ hP1 ∧ hP2); from specification heap-sep and-com: ⊦ (hP0 ∧ hP1) = (hP1 ∧ hP0); from specification heap-sep ⊦ false * hP = false; (s) ⊦ ¬ false(h); (s) x ≠ [] ⊦ a = x.head ∧ y = x.tail ↔ x = a + y; (elim) Used terms: x, a0, y

Proof step 8 from proof ll-trav2-next (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 9:

  h[r2] = a × r, r1 ≠ null, r2 ≠ null, ((lls(r0, r1, x0) * r1 => a0 × r2 * lls(r2, null, x1) * hP))(h) ⊦ ∃ x2, x3, a. x0 + a0 ' + x1 = x2 + a ' + x3 ∧ ((lls(r0, r2, x2) * r2 => a × r * lls(r, null, x3) * hP))(h)

Rule argument

Additional information

Used simplifier rules: ll-trav2-nonnull-def: ⊦ r1 ≠ null → ( ((ll-trav(r0, r1, r2, x) * hP))(h) ↔ (∃ x0, x1, a. x = x0 + (a + x1) ∧ ((lls(r0, r1, x0) * r1 => a × r2 * lls(r2, null, x1) * hP))(h))); sep-com: ⊦ hP0 * hP1 = hP1 * hP0; from specification heap-sep sep-ass: ⊦ (hP0 * hP1) * hP2 = hP0 * hP1 * hP2; from specification heap-sep a: ⊦ (x + y) + z = x + y + z; from specification list ⊦ a + x = a ' + x; (s)

Proof step 9 from proof ll-trav2-next (previous step) (back to tree)

User applied rule exists right

And obtained the following new goals

• Proof step 10:

  h[r2] = a × r, r1 ≠ null, r2 ≠ null, ((lls(r0, r1, x0) * r1 => a0 × r2 * lls(r2, null, x1) * hP))(h) ⊦ x0 + a0 ' + x1 = (x0 + a0) + a ' + x1.tail ∧ ((lls(r0, r2, x0 + a0) * r2 => a × r * lls(r, null, x1.tail) * hP))(h)

Rule argument

Additional information

Used terms: x0 + a0, x1.tail, a

Proof step 10 from proof ll-trav2-next (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 11:

  h[r2] = a × r, r1 ≠ null, r2 ≠ null, ((lls(r0, r1, x0) * r1 => a0 × r2 * lls(r2, null, x1) * hP))(h) ⊦ x1 = a ' + x1.tail ∧ ((lls(r0, r2, x0 + a0 ') * r2 => a × r * lls(r, null, x1.tail) * hP))(h)

Rule argument

Additional information

Used simplifier rules: ⊦ x + a = x + a '; (s) a: ⊦ (x + y) + z = x + y + z; from specification list ⊦ a ' + x = a ' + y ↔ x = y; (s) ⊦ x + y = x + z ↔ y = z; (s)

Proof step 11 from proof ll-trav2-next (previous step) (back to tree)

Heuristic elimination applied rule apply elim lemma

And obtained the following new goals

• Proof step 12:

  h[r2] = a × r, x1 = a1 + y, r1 ≠ null, r2 ≠ null, x1 ≠ [], ((lls(r0, r1, x0) * r1 => a0 × r2 * lls(r2, null, x1) * hP))(h) ⊦ x1 = a ' + y ∧ ((lls(r0, r2, x0 + a0 ') * r2 => a × r * lls(r, null, y) * hP))(h)

Rule argument

Additional information

Used simplifier rules: lls-base: ⊦ lls(r0, r1, []) = (emp ∧ ⌜r0 = r1⌝ ); ⊦ ⌜false⌝ = false; (s) ⊦ (false ∧ hP) = false; (s) and-ass: ⊦ ((hP0 ∧ hP1) ∧ hP2) = (hP0 ∧ hP1 ∧ hP2); from specification heap-sep and-com: ⊦ (hP0 ∧ hP1) = (hP1 ∧ hP0); from specification heap-sep ⊦ false * hP = false; (s) sep-ass: ⊦ (hP0 * hP1) * hP2 = hP0 * hP1 * hP2; from specification heap-sep sep-com: ⊦ hP0 * hP1 = hP1 * hP0; from specification heap-sep ⊦ ¬ false(h); (s) x ≠ [] ⊦ a = x.head ∧ y = x.tail ↔ x = a + y; (elim) Used terms: x1, a1, y

Proof step 12 from proof ll-trav2-next (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 13:

  r1 ≠ null, r2 ≠ null, (((r2 => a × r * lls(r, null, y)) * lls(r0, r1, x0) * r1 => a0 × r2 * hP))(h), ¬ ((lls(r0, r2, x0 + a0 ') * r2 => a × r * lls(r, null, y) * hP))(h) ⊦

Rule argument

Additional information

Used simplifier rules: lls-rec: ⊦ lls(r, r1, a ' + x) = _∃(λ r0. r => a × r0 * lls(r0, r1, x)); a: ⊦ (x + y) + z = x + y + z; from specification list ⊦ a ' + x = b ' + x ↔ a = b; (s) ⊦ a + x = a ' + x; (s) ⊦ a × r = a0 × r0 ↔ a = a0 ∧ r = r0; (ws) ⊦ ((r => o0 * hP))(h) → (h[r] = o1 ↔ o0 = o1); (s) sep-com: ⊦ hP0 * hP1 = hP1 * hP0; from specification heap-sep sep-ass: ⊦ (hP0 * hP1) * hP2 = hP0 * hP1 * hP2; from specification heap-sep ⊦ ((_∃ rP * hP))(h) ↔ (∃ r. ((rP(r) * hP))(h)); (s) ⊦ a ' + x ≠ []; (s)

Proof step 13 from proof ll-trav2-next (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 14:

  ⊦ lls(r0, r2, x + a ') = _∃(λ r1. lls(r0, r1, x) * r1 => a × r2)

• Proof step 15:

  r1 ≠ null, r2 ≠ null, (((r2 => a × r * lls(r, null, y)) * lls(r0, r1, x0) * r1 => a0 × r2 * hP))(h), ¬ ((_∃(λ r1. lls(r0, r1, x0) * r1 => a0 × r2) * r2 => a × r * lls(r, null, y) * hP))(h) ⊦

Rule argument

Additional information

Used terms: a0, x0, r2, r0

Proof step 14 from proof ll-trav2-next (previous step) (back to tree)

Lemma lls-unfold-tail

Proof step 15 from proof ll-trav2-next (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 16:

  r1 ≠ null, r2 ≠ null, (((r2 => a × r * lls(r, null, y)) * lls(r0, r1, x0) * r1 => a0 × r2 * hP))(h) ⊦ ∃ r1. (((lls(r0, r1, x0) * r1 => a0 × r2) * r2 => a × r * lls(r, null, y) * hP))(h)

Rule argument

Additional information

Used simplifier rules: sep-com: ⊦ hP0 * hP1 = hP1 * hP0; from specification heap-sep sep-ass: ⊦ (hP0 * hP1) * hP2 = hP0 * hP1 * hP2; from specification heap-sep ⊦ ((_∃ rP * hP))(h) ↔ (∃ r. ((rP(r) * hP))(h)); (s)

Proof step 16 from proof ll-trav2-next (previous step) (back to tree)

User applied rule exists right

And closed the goal!

Rule argument

Additional information

Used simplifier rules: sep-ass: ⊦ (hP0 * hP1) * hP2 = hP0 * hP1 * hP2; from specification heap-sep sep-com: ⊦ hP0 * hP1 = hP1 * hP0; from specification heap-sep Used terms: r1