Proof step 1 from proof dll-trav-next (conclusion) (back to tree)

System applied rule normalize

And obtained the following new goals

• Proof step 2:

  h(hd0) = mknode(cur, a, r1), hd0 ≠ nxt, (dll-trav(prv, hd, lst, cur, hd0, lst0, nxt, x) * hP)(h), ¬ (dll-trav(prv, hd, cur, hd0, r1, lst0, nxt, x) * hP)(h) ⊦

Rule argument

Additional information

Proof step 2 from proof dll-trav-next (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 3:

  h(hd0) = mknode(cur, a, r1), hd0 ≠ nxt, (dll-trav(prv, hd, lst, cur, hd0, lst0, nxt, x) * hP)(h), ¬ (dll-trav(prv, hd, cur, hd0, r1, lst0, nxt, x) * hP)(h) ⊦

Rule argument

Additional information

Proof step 3 from proof dll-trav-next (previous step) (back to tree)

User applied rule cut formula

And obtained the following new goals

• Proof step 4:

  cur = null, h(hd0) = mknode(cur, a, r1), hd0 ≠ nxt, (dll-trav(prv, hd, lst, cur, hd0, lst0, nxt, x) * hP)(h), ¬ (dll-trav(prv, hd, cur, hd0, r1, lst0, nxt, x) * hP)(h) ⊦

• Proof step 10:

  h(hd0) = mknode(cur, a, r1), cur ≠ null, hd0 ≠ nxt, (dll-trav(prv, hd, lst, cur, hd0, lst0, nxt, x) * hP)(h), ¬ (dll-trav(prv, hd, cur, hd0, r1, lst0, nxt, x) * hP)(h) ⊦

Rule argument

Additional information

Used formulas: cur = null

Proof step 4 from proof dll-trav-next (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 5:

  h(hd0) = mknode(null, a, r1), hd0 ≠ nxt, (dlls(hd0, lst0, prv, nxt, x) * hP)(h), ¬ (dll-trav(prv, hd0, null, hd0, r1, lst0, nxt, x) * hP)(h) ⊦

Rule argument

Additional information

Used simplifier rules: dll-trav-null: ⊦ (dll-trav(prv, hd, lst, null, hd0, lst0, nxt, x) * hP)(h) ↔ hd = hd0 ∧ lst = lst0 ∧ (dlls(hd, lst, prv, nxt, 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 dll-trav-next (previous step) (back to tree)

User applied rule constructor cut

And obtained the following new goals

• Proof step 6:

  h(hd0) = mknode(null, a, r1), x = a0 + x0, hd0 ≠ nxt, (dlls(hd0, lst0, prv, nxt, x) * hP)(h), ¬ (dll-trav(prv, hd0, null, hd0, r1, lst0, nxt, x) * hP)(h) ⊦

Rule argument

Additional information

Used simplifier rules: dlls-last-base: ⊦ dlls(hd, lst, prv, nxt, []) = (emp ∧ ⌜hd = nxt⌝ ∧ ⌜lst = prv⌝ ); List[A] freely generated by [], +; ⊦ ⌜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)

Proof step 6 from proof dll-trav-next (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 7:

  hd0 ≠ nxt, ((hd0 => mknode(null, a0, r1) * dlls(r1, lst0, hd0, nxt, x0)) * hP)(h), ¬ (dll-trav(null, hd0, null, hd0, r1, lst0, nxt, a0 ' + x0) * hP)(h) ⊦

Rule argument

Additional information

Used simplifier rules: dlls-last-rec: ⊦ dlls(hd, lst, prv, nxt, a ' + x) = _∃(λ nxt0. hd => mknode(prv, a, nxt0) * dlls(nxt0, lst, hd, nxt, x)); ⊦ a + x = a ' + x; (s) ⊦ mknode(left, val, left0) = mknode(left1, val0, left2) ↔ left = left1 ∧ val = val0 ∧ left0 = left2; (ws) ⊦ (r => o0 * hP)(h) → h(r) = o0; (s) sep-com: ⊦ hP0 * hP1 = hP1 * hP0; from specification heap-sep sep-ass: ⊦ (hP0 * hP1) * hP2 = hP0 * hP1 * hP2; from specification heap-sep ⊦ (_∃ bP * hP)(h) ↔ (∃ b. (bP(b) * hP)(h)); (s) a: ⊦ (x + y) + z = x + y + z; from specification list

Proof step 7 from proof dll-trav-next (previous step) (back to tree)

User applied rule cut formula

And obtained the following new goals

• Proof step 8:

  hd0 ≠ null, hd0 ≠ nxt, ((hd0 => mknode(null, a0, r1) * dlls(r1, lst0, hd0, nxt, x0)) * hP)(h), ¬ (dll-trav(null, hd0, null, hd0, r1, lst0, nxt, a0 ' + x0) * hP)(h) ⊦

Rule argument

Additional information

Used simplifier rules: ⊦ null => o = ⌜false⌝ ; (s) ⊦ ⌜false⌝ = false; (s) ⊦ 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) Used formulas: hd0 = null

Proof step 8 from proof dll-trav-next (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 9:

  hd0 ≠ null, hd0 ≠ nxt, ((hd0 => mknode(null, a0, r1) * dlls(r1, lst0, hd0, nxt, x0)) * hP)(h) ⊦ ∃ x1, x2, a. a0 ' + x0 = x1 + a ' + x2 ∧ (dlls(hd0, null, null, hd0, x1) * hd0 => mknode(null, a, r1) * dlls(r1, lst0, hd0, nxt, x2) * hP)(h)

Rule argument

Additional information

Used simplifier rules: ll-trav-nonnull: ⊦ cur ≠ null → ( (dll-trav(prv, hd, lst, cur, hd0, lst0, nxt, x) * hP)(h) ↔ (∃ x0, x1, a. x = x0 + (a + x1) ∧ ( dlls(hd, lst, prv, cur, x0) * cur => mknode(lst, a, hd0) * dlls(hd0, lst0, cur, nxt, 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 dll-trav-next (previous step) (back to tree)

User applied rule exists right

And closed the goal!

Rule argument

Additional information

Used simplifier rules: dlls-last-base: ⊦ dlls(hd, lst, prv, nxt, []) = (emp ∧ ⌜hd = nxt⌝ ∧ ⌜lst = prv⌝ ); ⊦ [] + x = x; (s) ⊦ # x = # z → (x + y = z + y0 ↔ x = z ∧ y = y0); (ws) a: ⊦ (x + y) + z = x + y + z; from specification list ⊦ ⌜true⌝ = true; (s) ⊦ (true ∧ hP) = hP; (s) and-ass: ⊦ ((hP0 ∧ hP1) ∧ hP2) = (hP0 ∧ hP1 ∧ hP2); from specification heap-sep and-com: ⊦ (hP0 ∧ hP1) = (hP1 ∧ hP0); from specification heap-sep ⊦ emp * hP = hP; (s) sep-ass: ⊦ (hP0 * hP1) * hP2 = hP0 * hP1 * hP2; from specification heap-sep sep-com: ⊦ hP0 * hP1 = hP1 * hP0; from specification heap-sep Used terms: [], x0, a0

Proof step 10 from proof dll-trav-next (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 11:

  h(hd0) = mknode(cur, a, r1), cur ≠ null, hd0 ≠ nxt, (dlls(hd, lst, prv, cur, x0) * cur => mknode(lst, a0, hd0) * dlls(hd0, lst0, cur, nxt, x1) * hP)(h), ¬ (dll-trav(prv, hd, cur, hd0, r1, lst0, nxt, x0 + a0 ' + x1) * hP)(h) ⊦

Rule argument

Additional information

Used simplifier rules: ll-trav-nonnull: ⊦ cur ≠ null → ( (dll-trav(prv, hd, lst, cur, hd0, lst0, nxt, x) * hP)(h) ↔ (∃ x0, x1, a. x = x0 + (a + x1) ∧ ( dlls(hd, lst, prv, cur, x0) * cur => mknode(lst, a, hd0) * dlls(hd0, lst0, cur, nxt, 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 11 from proof dll-trav-next (previous step) (back to tree)

User applied rule cut formula

And obtained the following new goals

• Proof step 12:

  h(hd0) = mknode(cur, a, r1), cur ≠ null, hd0 ≠ null, hd0 ≠ nxt, (dlls(hd, lst, prv, cur, x0) * cur => mknode(lst, a0, hd0) * dlls(hd0, lst0, cur, nxt, x1) * hP)(h), ¬ (dll-trav(prv, hd, cur, hd0, r1, lst0, nxt, x0 + a0 ' + x1) * hP)(h) ⊦

Rule argument

Additional information

Used simplifier rules: dlls-last-head-null: ⊦ dlls(null, lst, prv, nxt, x) = (emp ∧ ⌜nxt = null⌝ ∧ ⌜lst = prv⌝ ∧ ⌜x = []⌝ ); ⊦ ⌜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) Used formulas: hd0 = null

Proof step 12 from proof dll-trav-next (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 13:

  h(hd0) = mknode(cur, a, r1), cur ≠ null, hd0 ≠ null, hd0 ≠ nxt, (dlls(hd, lst, prv, cur, x0) * cur => mknode(lst, a0, hd0) * dlls(hd0, lst0, cur, nxt, x1) * hP)(h) ⊦ ∃ x2, x3, a1. x0 + a0 ' + x1 = x2 + a1 ' + x3 ∧ (dlls(hd, cur, prv, hd0, x2) * hd0 => mknode(cur, a1, r1) * dlls(r1, lst0, hd0, nxt, x3) * hP)(h)

Rule argument

Additional information

Used simplifier rules: ll-trav-nonnull: ⊦ cur ≠ null → ( (dll-trav(prv, hd, lst, cur, hd0, lst0, nxt, x) * hP)(h) ↔ (∃ x0, x1, a. x = x0 + (a + x1) ∧ ( dlls(hd, lst, prv, cur, x0) * cur => mknode(lst, a, hd0) * dlls(hd0, lst0, cur, nxt, 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 13 from proof dll-trav-next (previous step) (back to tree)

User applied rule exists right

And obtained the following new goals

• Proof step 14:

  h(hd0) = mknode(cur, a, r1), cur ≠ null, hd0 ≠ null, hd0 ≠ nxt, (dlls(hd, lst, prv, cur, x0) * cur => mknode(lst, a0, hd0) * dlls(hd0, lst0, cur, nxt, x1) * hP)(h) ⊦ x0 + a0 ' + x1 = (x0 + a0) + x1.head ' + x1.tail ∧ (dlls(hd, cur, prv, hd0, x0 + a0) * hd0 => mknode(cur, x1.head, r1) * dlls(r1, lst0, hd0, nxt, x1.tail) * hP)(h)

Rule argument

Additional information

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

Proof step 14 from proof dll-trav-next (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 15:

  h(hd0) = mknode(cur, a, r1), cur ≠ null, hd0 ≠ null, hd0 ≠ nxt, (dlls(hd, lst, prv, cur, x0) * cur => mknode(lst, a0, hd0) * dlls(hd0, lst0, cur, nxt, x1) * hP)(h) ⊦ x1 = x1.head ' + x1.tail ∧ (dlls(hd, cur, prv, hd0, x0 + a0 ') * hd0 => mknode(cur, x1.head, r1) * dlls(r1, lst0, hd0, nxt, 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 ⊦ # x = # z → (x + y = z + y0 ↔ x = z ∧ y = y0); (ws)

Proof step 15 from proof dll-trav-next (previous step) (back to tree)

Heuristic elimination applied rule apply elim lemma

And obtained the following new goals

• Proof step 16:

  h(hd0) = mknode(cur, a, r1), x1 = a1 + y, cur ≠ null, hd0 ≠ null, hd0 ≠ nxt, x1 ≠ [], (dlls(hd, lst, prv, cur, x0) * cur => mknode(lst, a0, hd0) * dlls(hd0, lst0, cur, nxt, x1) * hP)(h) ⊦ x1 = a1 ' + y ∧ (dlls(hd, cur, prv, hd0, x0 + a0 ') * hd0 => mknode(cur, a1, r1) * dlls(r1, lst0, hd0, nxt, y) * hP)(h)

Rule argument

Additional information

Used simplifier rules: dlls-last-base: ⊦ dlls(hd, lst, prv, nxt, []) = (emp ∧ ⌜hd = nxt⌝ ∧ ⌜lst = prv⌝ ); ⊦ ⌜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 16 from proof dll-trav-next (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 17:

  cur ≠ null, hd0 ≠ nxt, hd0 ≠ null, ((hd0 => mknode(cur, a1, r1) * dlls(r1, lst0, hd0, nxt, y)) * dlls(hd, lst, prv, cur, x0) * cur => mknode(lst, a0, hd0) * hP)(h), ¬ (dlls(hd, cur, prv, hd0, x0 + a0 ') * hd0 => mknode(cur, a1, r1) * dlls(r1, lst0, hd0, nxt, y) * hP)(h) ⊦

Rule argument

Additional information

Used simplifier rules: dlls-last-rec: ⊦ dlls(hd, lst, prv, nxt, a ' + x) = _∃(λ nxt0. hd => mknode(prv, a, nxt0) * dlls(nxt0, lst, hd, nxt, x)); a: ⊦ (x + y) + z = x + y + z; from specification list ⊦ # x = # z → (x + y = z + y0 ↔ x = z ∧ y = y0); (ws) ⊦ a + x = a ' + x; (s) ⊦ mknode(left, val, left0) = mknode(left1, val0, left2) ↔ left = left1 ∧ val = val0 ∧ left0 = left2; (ws) ⊦ (r => o0 * hP)(h) → h(r) = o0; (s) sep-com: ⊦ hP0 * hP1 = hP1 * hP0; from specification heap-sep sep-ass: ⊦ (hP0 * hP1) * hP2 = hP0 * hP1 * hP2; from specification heap-sep ⊦ (_∃ bP * hP)(h) ↔ (∃ b. (bP(b) * hP)(h)); (s) ⊦ a ' ≠ []; (s) ⊦ x + y = [] ↔ x = [] ∧ y = []; (s)

Proof step 17 from proof dll-trav-next (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 18:

  ⊦ dlls(hd, lst, prv, nxt, x + a ') = _∃(λ lst0. dlls(hd, lst0, prv, lst, x) * lst => mknode(lst0, a, nxt))

• Proof step 19:

  cur ≠ null, hd0 ≠ nxt, hd0 ≠ null, ((hd0 => mknode(cur, a1, r1) * dlls(r1, lst0, hd0, nxt, y)) * dlls(hd, lst, prv, cur, x0) * cur => mknode(lst, a0, hd0) * hP)(h), ¬ (_∃(λ lst0. dlls(hd, lst0, prv, cur, x0) * cur => mknode(lst0, a0, hd0)) * hd0 => mknode(cur, a1, r1) * dlls(r1, lst0, hd0, nxt, y) * hP)(h) ⊦

Rule argument

Additional information

Used terms: hd, cur, prv, a0, hd0, x0

Proof step 18 from proof dll-trav-next (previous step) (back to tree)

Lemma dlls-unfold-tail

Proof step 19 from proof dll-trav-next (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 20:

  cur ≠ null, hd0 ≠ nxt, hd0 ≠ null, ((hd0 => mknode(cur, a1, r1) * dlls(r1, lst0, hd0, nxt, y)) * dlls(hd, lst, prv, cur, x0) * cur => mknode(lst, a0, hd0) * hP)(h) ⊦ ∃ nxt0. ((dlls(hd, nxt0, prv, cur, x0) * cur => mknode(nxt0, a0, hd0)) * hd0 => mknode(cur, a1, r1) * dlls(r1, lst0, hd0, nxt, 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 ⊦ (_∃ bP * hP)(h) ↔ (∃ b. (bP(b) * hP)(h)); (s)

Proof step 20 from proof dll-trav-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: lst