Proof step 1 from proof lls-lasso-inj-gen (conclusion) (back to tree)

System applied rule normalize

And obtained the following new goals

• Proof step 2:

  y ≠ z, h0 ⊆ h, h1 ⊆ h, (r => a × r0 * lls(r0, r1, x) * lls(r1, r, z))(h1), (r => a × r0 * lls(r0, r1, x) * lls(r1, r, y))(h0) ⊦

Rule argument

Additional information

Proof step 2 from proof lls-lasso-inj-gen (previous step) (back to tree)

User applied rule structural induction

And obtained the following new goals

• Proof step 3:

  [] ≠ z, h0 ⊆ h, h1 ⊆ h, (r => a × r0 * lls(r0, r1, x) * lls(r1, r, []))(h0), (r => a × r0 * lls(r0, r1, x) * lls(r1, r, z))(h1) ⊦

• Proof step 5:

  a0 + y0 ≠ z, h0 ⊆ h, h1 ⊆ h, (r => a × r0 * lls(r0, r1, x) * lls(r1, r, a0 + y0))(h0), (r => a × r0 * lls(r0, r1, x) * lls(r1, r, z))(h1), ∀ z, h0, h, h1, r, a, r0, r1, x. ¬(y0 ≠ z ∧ h0 ⊆ h ∧ h1 ⊆ h ∧ (r => a × r0 * lls(r0, r1, x) * lls(r1, r, z))(h1) ∧ (r => a × r0 * lls(r0, r1, x) * lls(r1, r, y0))(h0)) ⊦

Rule argument

Additional information

Used simplifier rules: List[A] freely generated by [], +;

Proof step 3 from proof lls-lasso-inj-gen (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 4:

  [] ≠ z, h0 ⊆ h, h1 ⊆ h, (r => a × r0 * lls(r0, r, x))(h0), (r => a × r0 * lls(r0, r, x) * lls(r, r, z))(h1) ⊦

Rule argument

Additional information

Used simplifier rules: lls-base: ⊦ lls(r0, r1, []) = (emp ∧ ⌜r0 = r1⌝ ); and-com: ⊦ (hP0 ∧ hP1) = (hP1 ∧ hP0); from specification heap-sep and-ass: ⊦ ((hP0 ∧ hP1) ∧ hP2) = (hP0 ∧ hP1 ∧ hP2); from specification heap-sep ⊦ ⌜bv⌝ (h) ↔ bv; (s) ⊦ (hP0 ∧ hP1)(h) ↔ hP0(h) ∧ hP1(h); (s) sep-com: ⊦ hP0 * hP1 = hP1 * hP0; from specification heap-sep sep-ass: ⊦ (hP0 * hP1) * hP2 = hP0 * hP1 * hP2; from specification heap-sep ⊦ (⌜bv⌝ ∧ hP0) * hP1 = (⌜bv⌝ ∧ hP0 * hP1); (s) ⊦ emp * hP = hP; (s)

Proof step 4 from proof lls-lasso-inj-gen (previous step) (back to tree)

User applied rule constructor cut

And closed the goal!

Rule argument

Additional information

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

Proof step 5 from proof lls-lasso-inj-gen (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 6:

  a0 ' + y0 ≠ z, h0 ⊆ h, h1 ⊆ h, (r => a × r0 * lls(r0, r1, x) * lls(r1, r, z))(h1), ((r1 => a0 × r2 * lls(r2, r, y0)) * r => a × r0 * lls(r0, r1, x))(h0), ∀ z0, h2, h3, h4, r3, a1, r4, r5, x0. y0 = z0 ∨ ¬ h2 ⊆ h3 ∨ ¬ h4 ⊆ h3 ∨ ¬ (r3 => a1 × r4 * lls(r4, r5, x0) * lls(r5, r3, z0))(h4) ∨ ¬ (r3 => a1 × r4 * lls(r4, r5, x0) * lls(r5, r3, y0))(h2) ⊦

Rule argument

Additional information

Used simplifier rules: lls-rec: ⊦ lls(r, r1, a ' + x) = _∃(λ r0. r => a × r0 * lls(r0, r1, x)); 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 ⊦ a + x = a ' + x; (s)

Proof step 6 from proof lls-lasso-inj-gen (previous step) (back to tree)

User applied rule constructor cut

And obtained the following new goals

• Proof step 7:

  z = a2 + z1, a0 ' + y0 ≠ z, h0 ⊆ h, h1 ⊆ h, (r => a × r0 * lls(r0, r1, x) * lls(r1, r, z))(h1), ((r1 => a0 × r2 * lls(r2, r, y0)) * r => a × r0 * lls(r0, r1, x))(h0), ∀ z0, h2, h3, h4, r3, a1, r4, r5, x0. y0 = z0 ∨ ¬ h2 ⊆ h3 ∨ ¬ h4 ⊆ h3 ∨ ¬ (r3 => a1 × r4 * lls(r4, r5, x0) * lls(r5, r3, z0))(h4) ∨ ¬ (r3 => a1 × r4 * lls(r4, r5, x0) * lls(r5, r3, y0))(h2) ⊦

Rule argument

Additional information

Used simplifier rules: lls-base: ⊦ lls(r0, r1, []) = (emp ∧ ⌜r0 = r1⌝ ); List[A] freely generated by [], +; ⊦ x + y = [] ↔ x = [] ∧ y = []; (s) ⊦ a ' ≠ []; (s) a: ⊦ (x + y) + z = x + y + z; from specification list ⊦ emp * hP = hP; (s) ⊦ (⌜bv⌝ ∧ hP0) * hP1 = (⌜bv⌝ ∧ hP0 * hP1); (s) ⊦ (hP0 ∧ hP1)(h) ↔ hP0(h) ∧ hP1(h); (s) ⊦ ⌜bv⌝ (h) ↔ bv; (s) and-ass: ⊦ ((hP0 ∧ hP1) ∧ hP2) = (hP0 ∧ hP1 ∧ hP2); from specification heap-sep and-com: ⊦ (hP0 ∧ hP1) = (hP1 ∧ hP0); from specification heap-sep ⊦ r => o0 * r => o1 = 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)

Proof step 7 from proof lls-lasso-inj-gen (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 8:

  a0 ' + y0 ≠ a2 ' + z1, h0 ⊆ h, h1 ⊆ h, ((r1 => a0 × r2 * lls(r2, r, y0)) * r => a × r0 * lls(r0, r1, x))(h0), ((r1 => a2 × r3 * lls(r3, r, z1)) * r => a × r0 * lls(r0, r1, x))(h1), ∀ z0, h2, h3, h4, r3, a1, r4, r5, x0. y0 = z0 ∨ ¬ h2 ⊆ h3 ∨ ¬ h4 ⊆ h3 ∨ ¬ (r3 => a1 × r4 * lls(r4, r5, x0) * lls(r5, r3, z0))(h4) ∨ ¬ (r3 => a1 × r4 * lls(r4, r5, x0) * lls(r5, r3, y0))(h2) ⊦

Rule argument

Additional information

Used simplifier rules: lls-rec: ⊦ lls(r, r1, a ' + x) = _∃(λ r0. r => a × r0 * lls(r0, r1, x)); 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 ⊦ a + x = a ' + x; (s)

Proof step 8 from proof lls-lasso-inj-gen (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 9:

  ⊦ a ' + x = a0 ' + y ↔ a = a0 ∧ x = y

• Proof step 10:

  h0 ⊆ h, h1 ⊆ h, ((r1 => a2 × r3 * lls(r3, r, z1)) * r => a × r0 * lls(r0, r1, x))(h1), ((r1 => a0 × r2 * lls(r2, r, y0)) * r => a × r0 * lls(r0, r1, x))(h0), a2 ≠ a0 ∨ z1 ≠ y0, ∀ z0, h2, h3, h4, r3, a1, r4, r5, x0. y0 = z0 ∨ ¬ h2 ⊆ h3 ∨ ¬ h4 ⊆ h3 ∨ ¬ (r3 => a1 × r4 * lls(r4, r5, x0) * lls(r5, r3, z0))(h4) ∨ ¬ (r3 => a1 × r4 * lls(r4, r5, x0) * lls(r5, r3, y0))(h2) ⊦

Rule argument

Additional information

Used terms: a0, y0, a2, z1

Proof step 9 from proof lls-lasso-inj-gen (previous step) (back to tree)

A spec-lemma

Proof step 10 from proof lls-lasso-inj-gen (previous step) (back to tree)

User applied rule case distinction

And obtained the following new goals

• Proof step 11:

  a2 ≠ a0, h0 ⊆ h, h1 ⊆ h, ((r1 => a0 × r2 * lls(r2, r, y0)) * r => a × r0 * lls(r0, r1, x))(h0), ((r1 => a2 × r3 * lls(r3, r, z1)) * r => a × r0 * lls(r0, r1, x))(h1), ∀ z0, h2, h3, h4, r3, a1, r4, r5, x0. y0 = z0 ∨ ¬ h2 ⊆ h3 ∨ ¬ h4 ⊆ h3 ∨ ¬ (r3 => a1 × r4 * lls(r4, r5, x0) * lls(r5, r3, z0))(h4) ∨ ¬ (r3 => a1 × r4 * lls(r4, r5, x0) * lls(r5, r3, y0))(h2) ⊦

• Proof step 16:

  z1 ≠ y0, h0 ⊆ h, h1 ⊆ h, ((r1 => a0 × r2 * lls(r2, r, y0)) * r => a × r0 * lls(r0, r1, x))(h0), ((r1 => a2 × r3 * lls(r3, r, z1)) * r => a × r0 * lls(r0, r1, x))(h1), ∀ z0, h2, h3, h4, r3, a1, r4, r5, x0. y0 = z0 ∨ ¬ h2 ⊆ h3 ∨ ¬ h4 ⊆ h3 ∨ ¬ (r3 => a1 × r4 * lls(r4, r5, x0) * lls(r5, r3, z0))(h4) ∨ ¬ (r3 => a1 × r4 * lls(r4, r5, x0) * lls(r5, r3, y0))(h2) ⊦

Rule argument

Additional information

Proof step 11 from proof lls-lasso-inj-gen (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 12:

  ⊦ (hP0 * hP1)(h) ↔ (∃ h0, h1. h0 ⊥ h1 ∧ h = h0 ∪ h1 ∧ hP0(h0) ∧ hP1(h1))

• Proof step 13:

  a2 ≠ a0, h0 ⊆ h, h1 ⊆ h, ((r1 => a2 × r3 * lls(r3, r, z1)) * r => a × r0 * lls(r0, r1, x))(h1), ∃ h1, h2. h1 ⊥ h2 ∧ h0 = h1 ∪ h2 ∧ (lls(r2, r, y0) * r => a × r0 * lls(r0, r1, x))(h1) ∧ (r1 => a0 × r2)(h2), ∀ z0, h2, h3, h4, r3, a1, r4, r5, x0. y0 = z0 ∨ ¬ h2 ⊆ h3 ∨ ¬ h4 ⊆ h3 ∨ ¬ (r3 => a1 × r4 * lls(r4, r5, x0) * lls(r5, r3, z0))(h4) ∨ ¬ (r3 => a1 × r4 * lls(r4, r5, x0) * lls(r5, r3, y0))(h2) ⊦

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: h0, lls(r2, r, y0) * r => a × r0 * lls(r0, r1, x), r1 => a0 × r2

Proof step 12 from proof lls-lasso-inj-gen (previous step) (back to tree)

A spec-lemma

Proof step 13 from proof lls-lasso-inj-gen (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 14:

  a2 ≠ a0, h1 ⊆ h, h2 ⊥ h3, h2 ⊆ h, h3 ⊆ h, (lls(r2, r, y0) * r => a × r0 * lls(r0, r1, x))(h2), (r1 => a0 × r2)(h3), ((r1 => a2 × r3 * lls(r3, r, z1)) * r => a × r0 * lls(r0, r1, x))(h1), ∀ z0, h2, h3, h4, r3, a1, r4, r5, x0. y0 = z0 ∨ ¬ h2 ⊆ h3 ∨ ¬ h4 ⊆ h3 ∨ ¬ (r3 => a1 × r4 * lls(r4, r5, x0) * lls(r5, r3, z0))(h4) ∨ ¬ (r3 => a1 × r4 * lls(r4, r5, x0) * lls(r5, r3, y0))(h2) ⊦

Rule argument

Additional information

Used simplifier rules: ⊦ h0 ⊥ h1 → (h0 ∪ h1 ⊆ h ↔ h0 ⊆ h ∧ h1 ⊆ h); (ws)

Proof step 14 from proof lls-lasso-inj-gen (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 15:

  ⊦ (hP0 * hP1)(h) ↔ (∃ h0, h1. h0 ⊥ h1 ∧ h = h0 ∪ h1 ∧ hP0(h0) ∧ hP1(h1))

Rule argument

Additional information

Used simplifier rules: ⊦ h0 ⊥ h1 → (h0 ∪ h1 ⊆ h ↔ h0 ⊆ h ∧ h1 ⊆ h); (ws) ⊦ (r => o)(h1) ∧ h1 ⊆ h ∧ h2 ⊆ h → ((r => o1)(h2) ↔ o1 = o ∧ h1 = h2); (s) ⊦ a × r = a0 × r0 ↔ a = a0 ∧ r = r0; (ws) sep-ass: ⊦ (hP0 * hP1) * hP2 = hP0 * hP1 * hP2; from specification heap-sep sep-com: ⊦ hP0 * hP1 = hP1 * hP0; from specification heap-sep Used terms: h1, lls(r3, r, z1) * r => a × r0 * lls(r0, r1, x), r1 => a2 × r3

Proof step 15 from proof lls-lasso-inj-gen (previous step) (back to tree)

A spec-lemma

Proof step 16 from proof lls-lasso-inj-gen (previous step) (back to tree)

User applied rule all left

And obtained the following new goals

• Proof step 17:

  z1 ≠ y0, h0 ⊆ h, h1 ⊆ h, ((r1 => a2 × r3 * lls(r3, r, z1)) * r => a × r0 * lls(r0, r1, x))(h1), ((r1 => a0 × r2 * lls(r2, r, y0)) * r => a × r0 * lls(r0, r1, x))(h0), y0 = z1 ∨ ¬ h0 ⊆ h ∨ ¬ h1 ⊆ h ∨ ¬ (r => a × r0 * lls(r0, r3, x + a2) * lls(r3, r, z1))(h1) ∨ ¬ (r => a × r0 * lls(r0, r3, x + a2) * lls(r3, r, y0))(h0) ⊦

Rule argument

Additional information

Used terms: z1, h0, h, h1, r, a, r0, r3, x + a2

Proof step 17 from proof lls-lasso-inj-gen (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 18:

  z1 ≠ y0, h0 ⊆ h, h1 ⊆ h, ((r1 => a0 × r2 * lls(r2, r, y0)) * r => a × r0 * lls(r0, r1, x))(h0), ((r1 => a2 × r3 * lls(r3, r, z1)) * r => a × r0 * lls(r0, r1, x))(h1), ¬ (r => a × r0 * lls(r0, r3, x + a2 ') * lls(r3, r, z1))(h1) ∨ ¬ (r => a × r0 * lls(r0, r3, x + a2 ') * lls(r3, r, y0))(h0) ⊦

Rule argument

Additional information

Used simplifier rules: ⊦ x + a = x + a '; (s)

Proof step 18 from proof lls-lasso-inj-gen (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 19:

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

• Proof step 20:

  z1 ≠ y0, h0 ⊆ h, h1 ⊆ h, ((r1 => a2 × r3 * lls(r3, r, z1)) * r => a × r0 * lls(r0, r1, x))(h1), ((r1 => a0 × r2 * lls(r2, r, y0)) * r => a × r0 * lls(r0, r1, x))(h0), ¬ (r => a × r0 * _∃(λ r1. lls(r0, r1, x) * r1 => a2 × r3) * lls(r3, r, z1))(h1) ∨ ¬ (r => a × r0 * _∃(λ r1. lls(r0, r1, x) * r1 => a2 × r3) * lls(r3, r, y0))(h0) ⊦

Rule argument

Additional information

Used terms: r0, r3, x, a2

Proof step 19 from proof lls-lasso-inj-gen (previous step) (back to tree)

Lemma lls-unfold-tail

Proof step 20 from proof lls-lasso-inj-gen (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 21:

  z1 ≠ y0, h0 ⊆ h, h1 ⊆ h, ((r1 => a0 × r2 * lls(r2, r, y0)) * r => a × r0 * lls(r0, r1, x))(h0), ((r1 => a2 × r3 * lls(r3, r, z1)) * r => a × r0 * lls(r0, r1, x))(h1), ¬(∃ r1. ((lls(r0, r1, x) * r1 => a2 × r3) * r => a × r0 * lls(r3, r, z1))(h1)) ∨ ¬(∃ r1. ((lls(r0, r1, x) * r1 => a2 × r3) * r => a × r0 * lls(r3, r, y0))(h0)) ⊦

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 21 from proof lls-lasso-inj-gen (previous step) (back to tree)

User applied rule case distinction

And obtained the following new goals

• Proof step 22:

  z1 ≠ y0, h0 ⊆ h, h1 ⊆ h, ((r1 => a2 × r3 * lls(r3, r, z1)) * r => a × r0 * lls(r0, r1, x))(h1), ((r1 => a0 × r2 * lls(r2, r, y0)) * r => a × r0 * lls(r0, r1, x))(h0) ⊦ ∃ r1. ((lls(r0, r1, x) * r1 => a2 × r3) * r => a × r0 * lls(r3, r, z1))(h1)

• Proof step 23:

  z1 ≠ y0, h0 ⊆ h, h1 ⊆ h, ((r1 => a2 × r3 * lls(r3, r, z1)) * r => a × r0 * lls(r0, r1, x))(h1), ((r1 => a0 × r2 * lls(r2, r, y0)) * r => a × r0 * lls(r0, r1, x))(h0) ⊦ ∃ r1. ((lls(r0, r1, x) * r1 => a2 × r3) * r => a × r0 * lls(r3, r, y0))(h0)

Rule argument

Additional information

Proof step 22 from proof lls-lasso-inj-gen (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

Proof step 23 from proof lls-lasso-inj-gen (previous step) (back to tree)

User applied rule exists right

And obtained the following new goals

• Proof step 24:

  z1 ≠ y0, h0 ⊆ h, h1 ⊆ h, ((r1 => a0 × r2 * lls(r2, r, y0)) * r => a × r0 * lls(r0, r1, x))(h0), ((r1 => a2 × r3 * lls(r3, r, z1)) * r => a × r0 * lls(r0, r1, x))(h1), ¬ ((lls(r0, r1, x) * r1 => a2 × r3) * r => a × r0 * lls(r3, r, y0))(h0) ⊦

Rule argument

Additional information

Used terms: r1

Proof step 24 from proof lls-lasso-inj-gen (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 25:

  ⊦ (hP0 * hP1)(h) ↔ (∃ h0, h1. h0 ⊥ h1 ∧ h = h0 ∪ h1 ∧ hP0(h0) ∧ hP1(h1))

• Proof step 26:

  z1 ≠ y0, h0 ⊆ h, h1 ⊆ h, ((r1 => a2 × r3 * lls(r3, r, z1)) * r => a × r0 * lls(r0, r1, x))(h1), ¬ ((lls(r0, r1, x) * r1 => a2 × r3) * r => a × r0 * lls(r3, r, y0))(h0), ∃ h1, h2. h1 ⊥ h2 ∧ h0 = h1 ∪ h2 ∧ (lls(r2, r, y0) * r => a × r0 * lls(r0, r1, x))(h1) ∧ (r1 => a0 × r2)(h2) ⊦

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: h0, lls(r2, r, y0) * r => a × r0 * lls(r0, r1, x), r1 => a0 × r2

Proof step 25 from proof lls-lasso-inj-gen (previous step) (back to tree)

A spec-lemma

Proof step 26 from proof lls-lasso-inj-gen (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 27:

  z1 ≠ y0, h1 ⊆ h, h2 ⊥ h3, h2 ⊆ h, h3 ⊆ h, (lls(r2, r, y0) * r => a × r0 * lls(r0, r1, x))(h2), (r1 => a0 × r2)(h3), ((r1 => a2 × r3 * lls(r3, r, z1)) * r => a × r0 * lls(r0, r1, x))(h1), ¬ ((lls(r0, r1, x) * r1 => a2 × r3) * r => a × r0 * lls(r3, r, y0))(h2 ∪ h3) ⊦

Rule argument

Additional information

Used simplifier rules: ⊦ h0 ⊥ h1 → (h0 ∪ h1 ⊆ h ↔ h0 ⊆ h ∧ h1 ⊆ h); (ws)

Proof step 27 from proof lls-lasso-inj-gen (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 28:

  ⊦ (hP0 * hP1)(h) ↔ (∃ h0, h1. h0 ⊥ h1 ∧ h = h0 ∪ h1 ∧ hP0(h0) ∧ hP1(h1))

Rule argument

Additional information

Used simplifier rules: ⊦ h0 ⊥ h1 → (h0 ∪ h1 ⊆ h ↔ h0 ⊆ h ∧ h1 ⊆ h); (ws) ⊦ (r => o)(h1) ∧ h1 ⊆ h ∧ h2 ⊆ h → ((r => o1)(h2) ↔ o1 = o ∧ h1 = h2); (s) ⊦ a × r = a0 × r0 ↔ a = a0 ∧ r = r0; (ws) ⊦ hP0(h0) ∧ hP1(h1) ∧ h0 ⊥ h1 → (hP0 * hP1)(h0 ∪ h1); (ss) sep-ass: ⊦ (hP0 * hP1) * hP2 = hP0 * hP1 * hP2; from specification heap-sep sep-com: ⊦ hP0 * hP1 = hP1 * hP0; from specification heap-sep Used terms: h1, lls(r3, r, z1) * r => a × r0 * lls(r0, r1, x), r1 => a2 × r3

Proof step 28 from proof lls-lasso-inj-gen (previous step) (back to tree)

A spec-lemma