Proof step 1 from proof ls-push (conclusion) (back to tree)

System applied rule normalize

And obtained the following new goals

• Proof step 2:

  ¬(x = a ' + x0 ↔ true), o ≠ o0, (o[ls(r, x)] * true)[rs, cf, af(r; o)], (o0[r => a × r0] * true)[rs, cf, af], (o[ls(r0, x0)] * true)[rs, cf, af] ⊦

Rule argument

Additional information

Proof step 2 from proof ls-push (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 3:

  o ≠ o0, x ≠ a ' + x0, (o[ls(r, x)] * true)[rs, cf, af(r; o)], (o0[r => a × r0] * o[ls(r0, x0)] * true)[rs, cf, af] ⊦

Rule argument

Additional information

Used simplifier rules: sep-com: ⊦ hP0 * hP1 = hP1 * hP0; from specification heap-sep[heap-aux-inst] sep-ass: ⊦ (hP0 * hP1) * hP2 = hP0 * hP1 * hP2; from specification heap-sep[heap-aux-inst] ⊦ (hR0 * hR)[rs, f, g] → (true * hR)[rs, f, g]; (s) ⊦ (a[hP] * true)[rs, f, g] ∧ a0 ≠ a → ((a0[hP0] * true)[rs, f, g] ↔ (a[hP] * a0[hP0] * true)[rs, f, g]); (s)

Proof step 3 from proof ls-push (previous step) (back to tree)

User applied rule constructor cut

And obtained the following new goals

• Proof step 4:

  x = a0 + x1, o ≠ o0, x ≠ a ' + x0, (o0[r => a × r0] * o[ls(r0, x0)] * true)[rs, cf, af], (o[ls(r, x)] * true)[rs, cf, af(r; o)] ⊦

Rule argument

Additional information

Used simplifier rules: ls-base: ⊦ ls(r, []) = (emp ∧ ⌜r = null⌝ ); list freely generated by [], +;; ⊦ a ' + x ≠ []; (s) a: ⊦ (x + y) + z = x + y + z; from specification list ⊦ a[hP0 ∧ hP1] = (a[hP0] ∧ a[hP1]); (s) ⊦ a[emp] = emp; (s) ⊦ (a[⌜bv⌝ ] ∧ emp) = (⌜bv⌝ ∧ emp); (s) and-ass: ⊦ ((hP0 ∧ hP1) ∧ hP2) = (hP0 ∧ hP1 ∧ hP2); from specification heap-sep and-com: ⊦ (hP0 ∧ hP1) = (hP1 ∧ hP0); from specification heap-sep ⊦ (⌜bv⌝ ∧ hP0) * hP1 = (⌜bv⌝ ∧ hP0 * hP1); (s) ⊦ emp * hP = hP; (s) ⊦ (true ∧ hP) = hP; (s) and-ass: ⊦ ((hP0 ∧ hP1) ∧ hP2) = (hP0 ∧ hP1 ∧ hP2); from specification heap-sep[heap-aux-inst] and-com: ⊦ (hP0 ∧ hP1) = (hP1 ∧ hP0); from specification heap-sep[heap-aux-inst] ⊦ ⌜bv⌝ [rs, f, g] ↔ bv; (s) ⊦ null => o = ⌜false⌝ ; (s) ⊦ ⌜false⌝ = false; (s) ⊦ a[false] = false; (s) ⊦ false * hP = false; (s) sep-com: ⊦ hP0 * hP1 = hP1 * hP0; from specification heap-sep[heap-aux-inst] sep-ass: ⊦ (hP0 * hP1) * hP2 = hP0 * hP1 * hP2; from specification heap-sep[heap-aux-inst] ⊦ ¬ false[rs, f, g]; (s)

Proof step 4 from proof ls-push (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 5:

  a0 ' + x1 ≠ a ' + x0, o ≠ o0, (o0[r => a × r0] * o[ls(r0, x0)] * true)[rs, cf, af], ((o[r => a0 × r1] * o[ls(r1, x1)]) * true)[rs, cf, af(r; o)] ⊦

Rule argument

Additional information

Used simplifier rules: ls-rec: ⊦ ls(r, a ' + x) = _∃(λ r0. r => a × r0 * ls(r0, x)); sep-com: ⊦ hP0 * hP1 = hP1 * hP0; from specification heap-sep[heap-aux-inst] sep-ass: ⊦ (hP0 * hP1) * hP2 = hP0 * hP1 * hP2; from specification heap-sep[heap-aux-inst] ⊦ (_∃ rR * hR)[rs, f, g] ↔ (∃ r. (rR(r) * hR)[rs, f, g]); (s) sep-com: ⊦ hP0 * hP1 = hP1 * hP0; from specification heap-sep sep-ass: ⊦ (hP0 * hP1) * hP2 = hP0 * hP1 * hP2; from specification heap-sep ⊦ a[hP0 * hP1] = a[hP0] * a[hP1]; (s) ⊦ a[_∃ rhP] = _∃(λ r. a[rhP(r)]); (s) a: ⊦ (x + y) + z = x + y + z; from specification list ⊦ a + x = a ' + x; (s)

Proof step 5 from proof ls-push (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 6:

  ⊦ (a0[r => o] * hR)[rs, f, g] ↔ (a1[r => o] * hR)[rs, f, g(r; a1)] ∧ g(r) = a0

• Proof step 7:

  af(r) = o0, a0 ' + x1 ≠ a ' + x0, o ≠ o0, ((o[r => a0 × r1] * o[ls(r1, x1)]) * true)[rs, cf, af(r; o)], (o[r => a × r0] * true * o[ls(r0, x0)])[rs, cf, af(r; o)] ⊦

Rule argument

Additional information

Used simplifier rules: sep-ass: ⊦ (hP0 * hP1) * hP2 = hP0 * hP1 * hP2; from specification heap-sep[heap-aux-inst] sep-com: ⊦ hP0 * hP1 = hP1 * hP0; from specification heap-sep[heap-aux-inst] Used terms: true * o[ls(r0, x0)], cf, o0, r, rs, o, af, a × r0

Proof step 6 from proof ls-push (previous step) (back to tree)

A spec-lemma

Proof step 7 from proof ls-push (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 8:

  a0 ' + x1 ≠ a ' + x0, o ≠ af(r), (o[r => a × r0] * true * o[ls(r0, x0)])[rs, cf, af(r; o)], ((o[r => a0 × r1] * o[ls(r1, x1)]) * true)[rs, cf, af(r; o)] ⊦

Rule argument

Additional information

Proof step 8 from proof ls-push (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 9:

  y ≠ [] ⊦ y + z = a ' + x ↔ a = y.head ∧ x = y.tail + z

Rule argument

Additional information

Used simplifier rules: ls-unique: ⊦ (o[ls(r, x)] * hR)[rs, cf, af] ∧ (o[ls(r, x0)] * hR)[rs, cf, af] → (x = x0 ↔ true); ⊦ a ' ≠ []; (s) ⊦ a '.head = a; (s) ⊦ a '.tail = []; (s) ⊦ [] + x = x; (s) a: ⊦ (x + y) + z = x + y + z; from specification list map2: ⊦ (a[r => o] * hR)[rs, f, g] ∧ (a[r => o0] * hR0)[rs, f, g] → o = o0; (forward) from specification embed-aux[cell-heap-aux] sep-ass: ⊦ (hP0 * hP1) * hP2 = hP0 * hP1 * hP2; from specification heap-sep[heap-aux-inst] sep-com: ⊦ hP0 * hP1 = hP1 * hP0; from specification heap-sep[heap-aux-inst] ⊦ a × r = a0 × r0 ↔ a = a0 ∧ r = r0; (ws) Used terms: a0 ', x1, a, x0

Proof step 9 from proof ls-push (previous step) (back to tree)

A spec-lemma