Proof step 1 from proof sharing-ass-aux1 (conclusion) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 2:

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

• Proof step 3:

  ⊦ (∃ h0, h1, h2. h0 ⊥ h2 ∧ h0 ⊥ h1 ∧ h1 ⊥ h2 ∧ h = h0 ∪ h1 ∪ h2 ∧ hP0(h0 ∪ h2) ∧ (hP1 ⊗ hP2)(h1 ∪ h2)) ↔ (∃ h0, h1, h2, h21, h20, h10, h210. h = (h1 ∪ h0 ∪ h10) ∪ h2 ∪ h20 ∪ h21 ∪ h210 ∧ h0 ⊥ h1 ∧ h0 ⊥ h2 ∧ h0 ⊥ h21 ∧ h0 ⊥ h20 ∧ h0 ⊥ h10 ∧ h0 ⊥ h210 ∧ h1 ⊥ h2 ∧ h1 ⊥ h21 ∧ h1 ⊥ h20 ∧ h1 ⊥ h10 ∧ h1 ⊥ h210 ∧ h2 ⊥ h21 ∧ h2 ⊥ h20 ∧ h2 ⊥ h10 ∧ h2 ⊥ h210 ∧ h21 ⊥ h20 ∧ h21 ⊥ h10 ∧ h21 ⊥ h210 ∧ h20 ⊥ h10 ∧ h20 ⊥ h210 ∧ h10 ⊥ h210 ∧ hP0(h0 ∪ h10 ∪ h20 ∪ h210) ∧ hP1(h1 ∪ h10 ∪ h21 ∪ h210) ∧ hP2(h2 ∪ h20 ∪ h21 ∪ h210))

Rule argument

Additional information

Used terms: hP0, hP1 ⊗ hP2, h

Proof step 2 from proof sharing-ass-aux1 (previous step) (back to tree)

Lemma sharing

Proof step 3 from proof sharing-ass-aux1 (previous step) (back to tree)

User applied rule case distinction

And obtained the following new goals

• Proof step 4:

  ∃ h0, h1, h2. h0 ⊥ h2 ∧ h0 ⊥ h1 ∧ h1 ⊥ h2 ∧ h = h0 ∪ h1 ∪ h2 ∧ hP0(h0 ∪ h2) ∧ (hP1 ⊗ hP2)(h1 ∪ h2) ⊦ ∃ h0, h1, h2, h21, h20, h10, h210. h = (h1 ∪ h0 ∪ h10) ∪ h2 ∪ h20 ∪ h21 ∪ h210 ∧ h0 ⊥ h1 ∧ h0 ⊥ h2 ∧ h0 ⊥ h21 ∧ h0 ⊥ h20 ∧ h0 ⊥ h10 ∧ h0 ⊥ h210 ∧ h1 ⊥ h2 ∧ h1 ⊥ h21 ∧ h1 ⊥ h20 ∧ h1 ⊥ h10 ∧ h1 ⊥ h210 ∧ h2 ⊥ h21 ∧ h2 ⊥ h20 ∧ h2 ⊥ h10 ∧ h2 ⊥ h210 ∧ h21 ⊥ h20 ∧ h21 ⊥ h10 ∧ h21 ⊥ h210 ∧ h20 ⊥ h10 ∧ h20 ⊥ h210 ∧ h10 ⊥ h210 ∧ hP0(h0 ∪ h10 ∪ h20 ∪ h210) ∧ hP1(h1 ∪ h10 ∪ h21 ∪ h210) ∧ hP2(h2 ∪ h20 ∪ h21 ∪ h210)

• Proof step 55:

  ∃ h0, h1, h2, h21, h20, h10, h210. h = (h1 ∪ h0 ∪ h10) ∪ h2 ∪ h20 ∪ h21 ∪ h210 ∧ h0 ⊥ h1 ∧ h0 ⊥ h2 ∧ h0 ⊥ h21 ∧ h0 ⊥ h20 ∧ h0 ⊥ h10 ∧ h0 ⊥ h210 ∧ h1 ⊥ h2 ∧ h1 ⊥ h21 ∧ h1 ⊥ h20 ∧ h1 ⊥ h10 ∧ h1 ⊥ h210 ∧ h2 ⊥ h21 ∧ h2 ⊥ h20 ∧ h2 ⊥ h10 ∧ h2 ⊥ h210 ∧ h21 ⊥ h20 ∧ h21 ⊥ h10 ∧ h21 ⊥ h210 ∧ h20 ⊥ h10 ∧ h20 ⊥ h210 ∧ h10 ⊥ h210 ∧ hP0(h0 ∪ h10 ∪ h20 ∪ h210) ∧ hP1(h1 ∪ h10 ∪ h21 ∪ h210) ∧ hP2(h2 ∪ h20 ∪ h21 ∪ h210) ⊦ ∃ h0, h1, h2. h0 ⊥ h2 ∧ h0 ⊥ h1 ∧ h1 ⊥ h2 ∧ h = h0 ∪ h1 ∪ h2 ∧ hP0(h0 ∪ h2) ∧ (hP1 ⊗ hP2)(h1 ∪ h2)

Rule argument

Additional information

Proof step 4 from proof sharing-ass-aux1 (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 5:

  h0 ⊥ h2, h0 ⊥ h1, h1 ⊥ h2, hP0(h0 ∪ h2), (hP1 ⊗ hP2)(h1 ∪ h2) ⊦ ∃ h3, h4, h5, h21, h20, h10, h210. h0 ∪ h1 ∪ h2 = (h4 ∪ h3 ∪ h10) ∪ h5 ∪ h20 ∪ h21 ∪ h210 ∧ h3 ⊥ h4 ∧ h3 ⊥ h5 ∧ h3 ⊥ h21 ∧ h3 ⊥ h20 ∧ h3 ⊥ h10 ∧ h3 ⊥ h210 ∧ h4 ⊥ h5 ∧ h4 ⊥ h21 ∧ h4 ⊥ h20 ∧ h4 ⊥ h10 ∧ h4 ⊥ h210 ∧ h5 ⊥ h21 ∧ h5 ⊥ h20 ∧ h5 ⊥ h10 ∧ h5 ⊥ h210 ∧ h21 ⊥ h20 ∧ h21 ⊥ h10 ∧ h21 ⊥ h210 ∧ h20 ⊥ h10 ∧ h20 ⊥ h210 ∧ h10 ⊥ h210 ∧ hP0(h3 ∪ h10 ∪ h20 ∪ h210) ∧ hP1(h4 ∪ h10 ∪ h21 ∪ h210) ∧ hP2(h5 ∪ h20 ∪ h21 ∪ h210)

Rule argument

Additional information

Proof step 5 from proof sharing-ass-aux1 (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 6:

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

• Proof step 7:

  h0 ⊥ h1, h0 ⊥ h2, h1 ⊥ h2, hP0(h0 ∪ h2), ∃ h0, h3, h4. h0 ⊥ h4 ∧ h0 ⊥ h3 ∧ h3 ⊥ h4 ∧ h1 ∪ h2 = h0 ∪ h3 ∪ h4 ∧ hP1(h0 ∪ h4) ∧ hP2(h3 ∪ h4) ⊦ ∃ h3, h4, h5, h21, h20, h10, h210. h0 ∪ h1 ∪ h2 = (h4 ∪ h3 ∪ h10) ∪ h5 ∪ h20 ∪ h21 ∪ h210 ∧ h3 ⊥ h4 ∧ h3 ⊥ h5 ∧ h3 ⊥ h21 ∧ h3 ⊥ h20 ∧ h3 ⊥ h10 ∧ h3 ⊥ h210 ∧ h4 ⊥ h5 ∧ h4 ⊥ h21 ∧ h4 ⊥ h20 ∧ h4 ⊥ h10 ∧ h4 ⊥ h210 ∧ h5 ⊥ h21 ∧ h5 ⊥ h20 ∧ h5 ⊥ h10 ∧ h5 ⊥ h210 ∧ h21 ⊥ h20 ∧ h21 ⊥ h10 ∧ h21 ⊥ h210 ∧ h20 ⊥ h10 ∧ h20 ⊥ h210 ∧ h10 ⊥ h210 ∧ hP0(h3 ∪ h10 ∪ h20 ∪ h210) ∧ hP1(h4 ∪ h10 ∪ h21 ∪ h210) ∧ hP2(h5 ∪ h20 ∪ h21 ∪ h210)

Rule argument

Additional information

Used terms: hP1, hP2, h1 ∪ h2

Proof step 6 from proof sharing-ass-aux1 (previous step) (back to tree)

Lemma sharing

Proof step 7 from proof sharing-ass-aux1 (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 8:

  h1 ∪ h2 = h ∪ h3 ∪ h4, h ⊥ h4, h ⊥ h3, h0 ⊥ h2, h0 ⊥ h1, h1 ⊥ h2, h3 ⊥ h4, hP0(h0 ∪ h2), hP1(h ∪ h4), hP2(h3 ∪ h4) ⊦ ∃ h3, h4, h5, h21, h20, h10, h210. h0 ∪ h1 ∪ h2 = (h4 ∪ h3 ∪ h10) ∪ h5 ∪ h20 ∪ h21 ∪ h210 ∧ h3 ⊥ h4 ∧ h3 ⊥ h5 ∧ h3 ⊥ h21 ∧ h3 ⊥ h20 ∧ h3 ⊥ h10 ∧ h3 ⊥ h210 ∧ h4 ⊥ h5 ∧ h4 ⊥ h21 ∧ h4 ⊥ h20 ∧ h4 ⊥ h10 ∧ h4 ⊥ h210 ∧ h5 ⊥ h21 ∧ h5 ⊥ h20 ∧ h5 ⊥ h10 ∧ h5 ⊥ h210 ∧ h21 ⊥ h20 ∧ h21 ⊥ h10 ∧ h21 ⊥ h210 ∧ h20 ⊥ h10 ∧ h20 ⊥ h210 ∧ h10 ⊥ h210 ∧ hP0(h3 ∪ h10 ∪ h20 ∪ h210) ∧ hP1(h4 ∪ h10 ∪ h21 ∪ h210) ∧ hP2(h5 ∪ h20 ∪ h21 ∪ h210)

Rule argument

Additional information

Proof step 8 from proof sharing-ass-aux1 (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 9:

  h0 ⊥ h1, h2 ⊥ h3, h2 ⊥ h4, h3 ⊥ h4 ⊦ h0 ∪ h1 = h2 ∪ h3 ∪ h4 ↔ (∃ h20, h21, h30, h31, h40, h41. h2 = h20 ∪ h21 ∧ h3 = h30 ∪ h31 ∧ h4 = h40 ∪ h41 ∧ h0 = h20 ∪ h30 ∪ h40 ∧ h1 = h21 ∪ h31 ∪ h41 ∧ h20 ⊥ h21 ∧ h30 ⊥ h31 ∧ h40 ⊥ h41 ∧ h20 ⊥ h1 ∧ h30 ⊥ h1 ∧ h40 ⊥ h1 ∧ h21 ⊥ h0 ∧ h31 ⊥ h0 ∧ h41 ⊥ h0)

• Proof step 10:

  h ⊥ h3, h ⊥ h4, h0 ⊥ h1, h0 ⊥ h2, h1 ⊥ h2, h3 ⊥ h4, hP0(h0 ∪ h2), hP1(h ∪ h4), hP2(h3 ∪ h4), ∃ h20, h21, h30, h31, h40, h41. h = h20 ∪ h21 ∧ h3 = h30 ∪ h31 ∧ h4 = h40 ∪ h41 ∧ h1 = h20 ∪ h30 ∪ h40 ∧ h2 = h21 ∪ h31 ∪ h41 ∧ h20 ⊥ h21 ∧ h30 ⊥ h31 ∧ h40 ⊥ h41 ∧ h20 ⊥ h2 ∧ h30 ⊥ h2 ∧ h40 ⊥ h2 ∧ h21 ⊥ h1 ∧ h31 ⊥ h1 ∧ h41 ⊥ h1 ⊦ ∃ h3, h4, h5, h21, h20, h10, h210. h0 ∪ h1 ∪ h2 = (h4 ∪ h3 ∪ h10) ∪ h5 ∪ h20 ∪ h21 ∪ h210 ∧ h3 ⊥ h4 ∧ h3 ⊥ h5 ∧ h3 ⊥ h21 ∧ h3 ⊥ h20 ∧ h3 ⊥ h10 ∧ h3 ⊥ h210 ∧ h4 ⊥ h5 ∧ h4 ⊥ h21 ∧ h4 ⊥ h20 ∧ h4 ⊥ h10 ∧ h4 ⊥ h210 ∧ h5 ⊥ h21 ∧ h5 ⊥ h20 ∧ h5 ⊥ h10 ∧ h5 ⊥ h210 ∧ h21 ⊥ h20 ∧ h21 ⊥ h10 ∧ h21 ⊥ h210 ∧ h20 ⊥ h10 ∧ h20 ⊥ h210 ∧ h10 ⊥ h210 ∧ hP0(h3 ∪ h10 ∪ h20 ∪ h210) ∧ hP1(h4 ∪ h10 ∪ h21 ∪ h210) ∧ hP2(h5 ∪ h20 ∪ h21 ∪ h210)

Rule argument

Additional information

Used terms: h, h4, h3, h2, h1

Proof step 9 from proof sharing-ass-aux1 (previous step) (back to tree)

A spec-lemma

Proof step 10 from proof sharing-ass-aux1 (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 11:

  h0 ⊥ h21, h0 ⊥ h31, h0 ⊥ h41, h0 ⊥ h20, h0 ⊥ h30, h0 ⊥ h40, h20 ⊥ h40, h20 ⊥ h41, h20 ⊥ h30, h20 ⊥ h31, h20 ⊥ h21, h21 ⊥ h41, h21 ⊥ h31, h21 ⊥ h20, h21 ⊥ h30, h21 ⊥ h40, h30 ⊥ h31, h30 ⊥ h21, h30 ⊥ h40, h30 ⊥ h41, h31 ⊥ h20, h31 ⊥ h30, h31 ⊥ h40, h31 ⊥ h41, h40 ⊥ h41, h40 ⊥ h21, h40 ⊥ h31, h41 ⊥ h20, h41 ⊥ h30, h41 ⊥ h40, hP0(h0 ∪ h21 ∪ h31 ∪ h41), hP1((h20 ∪ h21) ∪ h40 ∪ h41), hP2((h30 ∪ h31) ∪ h40 ∪ h41) ⊦ ∃ h3, h4, h5, h, h1, h10, h210. h0 ∪ (h20 ∪ h30 ∪ h40) ∪ h21 ∪ h31 ∪ h41 = (h4 ∪ h3 ∪ h10) ∪ h5 ∪ h1 ∪ h ∪ h210 ∧ h3 ⊥ h4 ∧ h3 ⊥ h5 ∧ h3 ⊥ h ∧ h3 ⊥ h1 ∧ h3 ⊥ h10 ∧ h3 ⊥ h210 ∧ h4 ⊥ h5 ∧ h4 ⊥ h ∧ h4 ⊥ h1 ∧ h4 ⊥ h10 ∧ h4 ⊥ h210 ∧ h5 ⊥ h ∧ h5 ⊥ h1 ∧ h5 ⊥ h10 ∧ h5 ⊥ h210 ∧ h ⊥ h1 ∧ h ⊥ h10 ∧ h ⊥ h210 ∧ h1 ⊥ h10 ∧ h1 ⊥ h210 ∧ h10 ⊥ h210 ∧ hP0(h3 ∪ h10 ∪ h1 ∪ h210) ∧ hP1(h4 ∪ h10 ∪ h ∪ h210) ∧ hP2(h5 ∪ h1 ∪ h ∪ h210)

Rule argument

Additional information

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

Proof step 11 from proof sharing-ass-aux1 (previous step) (back to tree)

User applied rule exists right

And obtained the following new goals

• Proof step 12:

  h0 ⊥ h40, h0 ⊥ h30, h0 ⊥ h20, h0 ⊥ h41, h0 ⊥ h31, h0 ⊥ h21, h20 ⊥ h21, h20 ⊥ h31, h20 ⊥ h30, h20 ⊥ h41, h20 ⊥ h40, h21 ⊥ h40, h21 ⊥ h30, h21 ⊥ h20, h21 ⊥ h31, h21 ⊥ h41, h30 ⊥ h41, h30 ⊥ h40, h30 ⊥ h21, h30 ⊥ h31, h31 ⊥ h41, h31 ⊥ h40, h31 ⊥ h30, h31 ⊥ h20, h40 ⊥ h31, h40 ⊥ h21, h40 ⊥ h41, h41 ⊥ h40, h41 ⊥ h30, h41 ⊥ h20, hP0(h0 ∪ h21 ∪ h31 ∪ h41), hP1((h20 ∪ h21) ∪ h40 ∪ h41), hP2((h30 ∪ h31) ∪ h40 ∪ h41) ⊦ h0 ∪ (h20 ∪ h30 ∪ h40) ∪ h21 ∪ h31 ∪ h41 = (h20 ∪ h0 ∪ h21) ∪ h30 ∪ h31 ∪ h40 ∪ h41 ∧ h0 ⊥ h20 ∧ h0 ⊥ h30 ∧ h0 ⊥ h40 ∧ h0 ⊥ h31 ∧ h0 ⊥ h21 ∧ h0 ⊥ h41 ∧ h20 ⊥ h30 ∧ h20 ⊥ h40 ∧ h20 ⊥ h31 ∧ h20 ⊥ h21 ∧ h20 ⊥ h41 ∧ h30 ⊥ h40 ∧ h30 ⊥ h31 ∧ h30 ⊥ h21 ∧ h30 ⊥ h41 ∧ h40 ⊥ h31 ∧ h40 ⊥ h21 ∧ h40 ⊥ h41 ∧ h31 ⊥ h21 ∧ h31 ⊥ h41 ∧ h21 ⊥ h41 ∧ hP0(h0 ∪ h21 ∪ h31 ∪ h41) ∧ hP1(h20 ∪ h21 ∪ h40 ∪ h41) ∧ hP2(h30 ∪ h31 ∪ h40 ∪ h41)

Rule argument

Additional information

Used terms: h0, h20, h30, h40, h31, h21, h41

Proof step 12 from proof sharing-ass-aux1 (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 13:

  h0 ⊥ h21, h0 ⊥ h31, h0 ⊥ h41, h0 ⊥ h20, h0 ⊥ h30, h0 ⊥ h40, h20 ⊥ h40, h20 ⊥ h41, h20 ⊥ h30, h20 ⊥ h31, h20 ⊥ h21, h21 ⊥ h41, h21 ⊥ h31, h21 ⊥ h20, h21 ⊥ h30, h21 ⊥ h40, h30 ⊥ h31, h30 ⊥ h21, h30 ⊥ h40, h30 ⊥ h41, h31 ⊥ h20, h31 ⊥ h30, h31 ⊥ h40, h31 ⊥ h41, h40 ⊥ h41, h40 ⊥ h21, h40 ⊥ h31, h41 ⊥ h20, h41 ⊥ h30, h41 ⊥ h40, hP0(h0 ∪ h21 ∪ h31 ∪ h41), hP1((h20 ∪ h21) ∪ h40 ∪ h41), hP2((h30 ∪ h31) ∪ h40 ∪ h41) ⊦ h0 ∪ (h20 ∪ h30 ∪ h40) ∪ h21 ∪ h31 ∪ h41 = (h20 ∪ h0 ∪ h21) ∪ h30 ∪ h31 ∪ h40 ∪ h41 ∧ hP1(h20 ∪ h21 ∪ h40 ∪ h41) ∧ hP2(h30 ∪ h31 ∪ h40 ∪ h41)

Rule argument

Additional information

Used simplifier rules: ⊦ h0 ⊥ h1 → h1 ⊥ h0; (ss)

Proof step 13 from proof sharing-ass-aux1 (previous step) (back to tree)

User applied rule case distinction

And obtained the following new goals

• Proof step 14:

  h0 ∪ (h20 ∪ h30 ∪ h40) ∪ h21 ∪ h31 ∪ h41 ≠ (h20 ∪ h0 ∪ h21) ∪ h30 ∪ h31 ∪ h40 ∪ h41, h0 ⊥ h40, h0 ⊥ h30, h0 ⊥ h20, h0 ⊥ h41, h0 ⊥ h31, h0 ⊥ h21, h20 ⊥ h21, h20 ⊥ h31, h20 ⊥ h30, h20 ⊥ h41, h20 ⊥ h40, h21 ⊥ h40, h21 ⊥ h30, h21 ⊥ h20, h21 ⊥ h31, h21 ⊥ h41, h30 ⊥ h41, h30 ⊥ h40, h30 ⊥ h21, h30 ⊥ h31, h31 ⊥ h41, h31 ⊥ h40, h31 ⊥ h30, h31 ⊥ h20, h40 ⊥ h31, h40 ⊥ h21, h40 ⊥ h41, h41 ⊥ h40, h41 ⊥ h30, h41 ⊥ h20, hP0(h0 ∪ h21 ∪ h31 ∪ h41), hP1((h20 ∪ h21) ∪ h40 ∪ h41), hP2((h30 ∪ h31) ∪ h40 ∪ h41) ⊦

• Proof step 51:

  h0 ⊥ h40, h0 ⊥ h30, h0 ⊥ h20, h0 ⊥ h41, h0 ⊥ h31, h0 ⊥ h21, h20 ⊥ h21, h20 ⊥ h31, h20 ⊥ h30, h20 ⊥ h41, h20 ⊥ h40, h21 ⊥ h40, h21 ⊥ h30, h21 ⊥ h20, h21 ⊥ h31, h21 ⊥ h41, h30 ⊥ h41, h30 ⊥ h40, h30 ⊥ h21, h30 ⊥ h31, h31 ⊥ h41, h31 ⊥ h40, h31 ⊥ h30, h31 ⊥ h20, h40 ⊥ h31, h40 ⊥ h21, h40 ⊥ h41, h41 ⊥ h40, h41 ⊥ h30, h41 ⊥ h20, hP0(h0 ∪ h21 ∪ h31 ∪ h41), hP1((h20 ∪ h21) ∪ h40 ∪ h41), hP2((h30 ∪ h31) ∪ h40 ∪ h41), ¬ hP1(h20 ∪ h21 ∪ h40 ∪ h41) ⊦

• Proof step 53:

  h0 ⊥ h40, h0 ⊥ h30, h0 ⊥ h20, h0 ⊥ h41, h0 ⊥ h31, h0 ⊥ h21, h20 ⊥ h21, h20 ⊥ h31, h20 ⊥ h30, h20 ⊥ h41, h20 ⊥ h40, h21 ⊥ h40, h21 ⊥ h30, h21 ⊥ h20, h21 ⊥ h31, h21 ⊥ h41, h30 ⊥ h41, h30 ⊥ h40, h30 ⊥ h21, h30 ⊥ h31, h31 ⊥ h41, h31 ⊥ h40, h31 ⊥ h30, h31 ⊥ h20, h40 ⊥ h31, h40 ⊥ h21, h40 ⊥ h41, h41 ⊥ h40, h41 ⊥ h30, h41 ⊥ h20, hP0(h0 ∪ h21 ∪ h31 ∪ h41), hP1((h20 ∪ h21) ∪ h40 ∪ h41), hP2((h30 ∪ h31) ∪ h40 ∪ h41), ¬ hP2(h30 ∪ h31 ∪ h40 ∪ h41) ⊦

Rule argument

Additional information

Proof step 14 from proof sharing-ass-aux1 (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 15:

  ⊦ h0 ⊥ h1 → h1 ∪ h0 = h0 ∪ h1

• Proof step 16:

  ((h20 ∪ h30 ∪ h40) ∪ h21 ∪ h31 ∪ h41) ∪ h0 ≠ (h20 ∪ h0 ∪ h21) ∪ h30 ∪ h31 ∪ h40 ∪ h41, h0 ⊥ h21, h0 ⊥ h31, h0 ⊥ h41, h0 ⊥ h20, h0 ⊥ h30, h0 ⊥ h40, h20 ⊥ h40, h20 ⊥ h41, h20 ⊥ h30, h20 ⊥ h31, h20 ⊥ h21, (h20 ∪ h30 ∪ h40) ∪ h21 ∪ h31 ∪ h41 ⊥ h0, h21 ⊥ h41, h21 ⊥ h31, h21 ⊥ h20, h21 ⊥ h30, h21 ⊥ h40, h30 ⊥ h31, h30 ⊥ h21, h30 ⊥ h40, h30 ⊥ h41, h31 ⊥ h20, h31 ⊥ h30, h31 ⊥ h40, h31 ⊥ h41, h40 ⊥ h41, h40 ⊥ h21, h40 ⊥ h31, h41 ⊥ h20, h41 ⊥ h30, h41 ⊥ h40, hP0(h0 ∪ h21 ∪ h31 ∪ h41), hP1((h20 ∪ h21) ∪ h40 ∪ h41), hP2((h30 ∪ h31) ∪ h40 ∪ h41) ⊦

Rule argument

Additional information

Used simplifier rules: ⊦ h0 ⊥ h1 → h1 ⊥ h0; (ss) h1 ⊥ h2 ⊦ h1 ∪ h2 ⊥ h0 ↔ h0 ⊥ h1 ∧ h0 ⊥ h2; (s) h1 ⊥ h ⊦ h0 ⊥ h1 ∪ h ↔ h0 ⊥ h1 ∧ h0 ⊥ h; (ws) Used terms: h0, (h20 ∪ h30 ∪ h40) ∪ h21 ∪ h31 ∪ h41

Proof step 15 from proof sharing-ass-aux1 (previous step) (back to tree)

A spec-lemma

Proof step 16 from proof sharing-ass-aux1 (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 17:

  ((h20 ∪ h30 ∪ h40) ∪ h21 ∪ h31 ∪ h41) ∪ h0 ≠ (h20 ∪ h0 ∪ h21) ∪ h30 ∪ h31 ∪ h40 ∪ h41, h0 ⊥ h40, h0 ⊥ h30, h0 ⊥ h20, h0 ⊥ h41, h0 ⊥ h31, h0 ⊥ h21, h20 ⊥ h21, h20 ⊥ h31, h20 ⊥ h30, h20 ⊥ h41, h20 ⊥ h40, h21 ⊥ h40, h21 ⊥ h30, h21 ⊥ h20, h21 ⊥ h31, h21 ⊥ h41, h30 ⊥ h41, h30 ⊥ h40, h30 ⊥ h21, h30 ⊥ h31, h31 ⊥ h41, h31 ⊥ h40, h31 ⊥ h30, h31 ⊥ h20, h40 ⊥ h31, h40 ⊥ h21, h40 ⊥ h41, h41 ⊥ h40, h41 ⊥ h30, h41 ⊥ h20, hP0(h0 ∪ h21 ∪ h31 ∪ h41), hP1((h20 ∪ h21) ∪ h40 ∪ h41), hP2((h30 ∪ h31) ∪ h40 ∪ h41) ⊦

Rule argument

Additional information

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

Proof step 17 from proof sharing-ass-aux1 (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 18:

  h0 ⊥ h1, h1 ⊥ h, h ⊥ h0 ⊦ (h0 ∪ h1) ∪ h = h0 ∪ h1 ∪ h

• Proof step 19:

  (h20 ∪ (h30 ∪ h40) ∪ h21 ∪ h31 ∪ h41) ∪ h0 ≠ (h20 ∪ h0 ∪ h21) ∪ h30 ∪ h31 ∪ h40 ∪ h41, h0 ⊥ h21, h0 ⊥ h31, h0 ⊥ h41, h0 ⊥ h20, h0 ⊥ h30, h0 ⊥ h40, h20 ⊥ h40, h20 ⊥ h41, h20 ⊥ h30, h20 ⊥ h31, h20 ⊥ h21, h20 ⊥ h30 ∪ h40, h21 ⊥ h41, h21 ⊥ h31, h21 ⊥ h20, h21 ⊥ h30, h21 ⊥ h40, h21 ∪ h31 ∪ h41 ⊥ h20, h30 ⊥ h31, h30 ⊥ h21, h30 ⊥ h40, h30 ⊥ h41, h30 ∪ h40 ⊥ h21 ∪ h31 ∪ h41, h31 ⊥ h20, h31 ⊥ h30, h31 ⊥ h40, h31 ⊥ h41, h40 ⊥ h41, h40 ⊥ h21, h40 ⊥ h31, h41 ⊥ h20, h41 ⊥ h30, h41 ⊥ h40, hP0(h0 ∪ h21 ∪ h31 ∪ h41), hP1((h20 ∪ h21) ∪ h40 ∪ h41), hP2((h30 ∪ h31) ∪ h40 ∪ h41) ⊦

Rule argument

Additional information

Used simplifier rules: h1 ⊥ h2 ⊦ h1 ∪ h2 ⊥ h0 ↔ h0 ⊥ h1 ∧ h0 ⊥ h2; (s) h1 ⊥ h ⊦ h0 ⊥ h1 ∪ h ↔ h0 ⊥ h1 ∧ h0 ⊥ h; (ws) ⊦ h0 ⊥ h1 → h1 ⊥ h0; (ss) Used terms: h20, h30 ∪ h40, h21 ∪ h31 ∪ h41

Proof step 18 from proof sharing-ass-aux1 (previous step) (back to tree)

A spec-lemma

Proof step 19 from proof sharing-ass-aux1 (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 20:

  (h20 ∪ (h30 ∪ h40) ∪ h21 ∪ h31 ∪ h41) ∪ h0 ≠ (h20 ∪ h0 ∪ h21) ∪ h30 ∪ h31 ∪ h40 ∪ h41, h0 ⊥ h40, h0 ⊥ h30, h0 ⊥ h20, h0 ⊥ h41, h0 ⊥ h31, h0 ⊥ h21, h20 ⊥ h21, h20 ⊥ h31, h20 ⊥ h30, h20 ⊥ h41, h20 ⊥ h40, h21 ⊥ h40, h21 ⊥ h30, h21 ⊥ h20, h21 ⊥ h31, h21 ⊥ h41, h30 ⊥ h41, h30 ⊥ h40, h30 ⊥ h21, h30 ⊥ h31, h31 ⊥ h41, h31 ⊥ h40, h31 ⊥ h30, h31 ⊥ h20, h40 ⊥ h31, h40 ⊥ h21, h40 ⊥ h41, h41 ⊥ h40, h41 ⊥ h30, h41 ⊥ h20, hP0(h0 ∪ h21 ∪ h31 ∪ h41), hP1((h20 ∪ h21) ∪ h40 ∪ h41), hP2((h30 ∪ h31) ∪ h40 ∪ h41) ⊦

Rule argument

Additional information

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

Proof step 20 from proof sharing-ass-aux1 (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 21:

  h0 ⊥ h1, h1 ⊥ h, h ⊥ h0 ⊦ (h0 ∪ h1) ∪ h = h0 ∪ h1 ∪ h

• Proof step 22:

  h20 ∪ ((h30 ∪ h40) ∪ h21 ∪ h31 ∪ h41) ∪ h0 ≠ (h20 ∪ h0 ∪ h21) ∪ h30 ∪ h31 ∪ h40 ∪ h41, h0 ⊥ h21, h0 ⊥ h31, h0 ⊥ h41, h0 ⊥ h30, h0 ⊥ h40, h0 ⊥ h20, h20 ⊥ h40, h20 ⊥ h41, h20 ⊥ h30, h20 ⊥ h31, h20 ⊥ h21, h20 ⊥ (h30 ∪ h40) ∪ h21 ∪ h31 ∪ h41, h21 ⊥ h41, h21 ⊥ h31, h21 ⊥ h20, h21 ⊥ h30, h21 ⊥ h40, h30 ⊥ h31, h30 ⊥ h21, h30 ⊥ h40, h30 ⊥ h41, (h30 ∪ h40) ∪ h21 ∪ h31 ∪ h41 ⊥ h0, h31 ⊥ h20, h31 ⊥ h30, h31 ⊥ h40, h31 ⊥ h41, h40 ⊥ h41, h40 ⊥ h21, h40 ⊥ h31, h41 ⊥ h20, h41 ⊥ h30, h41 ⊥ h40, hP0(h0 ∪ h21 ∪ h31 ∪ h41), hP1((h20 ∪ h21) ∪ h40 ∪ h41), hP2((h30 ∪ h31) ∪ h40 ∪ h41) ⊦

Rule argument

Additional information

Used simplifier rules: h1 ⊥ h2 ⊦ h1 ∪ h2 ⊥ h0 ↔ h0 ⊥ h1 ∧ h0 ⊥ h2; (s) h1 ⊥ h ⊦ h0 ⊥ h1 ∪ h ↔ h0 ⊥ h1 ∧ h0 ⊥ h; (ss) h1 ⊥ h ⊦ h0 ⊥ h1 ∪ h ↔ h0 ⊥ h1 ∧ h0 ⊥ h; (ws) ⊦ h0 ⊥ h1 → h1 ⊥ h0; (ss) Used terms: h20, (h30 ∪ h40) ∪ h21 ∪ h31 ∪ h41, h0

Proof step 21 from proof sharing-ass-aux1 (previous step) (back to tree)

A spec-lemma

Proof step 22 from proof sharing-ass-aux1 (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 23:

  h20 ∪ ((h30 ∪ h40) ∪ h21 ∪ h31 ∪ h41) ∪ h0 ≠ (h20 ∪ h0 ∪ h21) ∪ h30 ∪ h31 ∪ h40 ∪ h41, h0 ⊥ h20, h0 ⊥ h40, h0 ⊥ h30, h0 ⊥ h41, h0 ⊥ h31, h0 ⊥ h21, h20 ⊥ h21, h20 ⊥ h31, h20 ⊥ h30, h20 ⊥ h41, h20 ⊥ h40, h21 ⊥ h40, h21 ⊥ h30, h21 ⊥ h20, h21 ⊥ h31, h21 ⊥ h41, h30 ⊥ h41, h30 ⊥ h40, h30 ⊥ h21, h30 ⊥ h31, h31 ⊥ h41, h31 ⊥ h40, h31 ⊥ h30, h31 ⊥ h20, h40 ⊥ h31, h40 ⊥ h21, h40 ⊥ h41, h41 ⊥ h40, h41 ⊥ h30, h41 ⊥ h20, hP0(h0 ∪ h21 ∪ h31 ∪ h41), hP1((h20 ∪ h21) ∪ h40 ∪ h41), hP2((h30 ∪ h31) ∪ h40 ∪ h41) ⊦

Rule argument

Additional information

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

Proof step 23 from proof sharing-ass-aux1 (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 24:

  h0 ⊥ h1, h1 ⊥ h, h ⊥ h0 ⊦ (h0 ∪ h1) ∪ h = h0 ∪ h1 ∪ h

• Proof step 25:

  h20 ∪ ((h30 ∪ h40) ∪ h21 ∪ h31 ∪ h41) ∪ h0 ≠ h20 ∪ (h0 ∪ h21) ∪ h30 ∪ h31 ∪ h40 ∪ h41, h0 ⊥ h21, h0 ⊥ h31, h0 ⊥ h41, h0 ⊥ h30, h0 ⊥ h40, h0 ⊥ h20, h0 ∪ h21 ⊥ h30 ∪ h31 ∪ h40 ∪ h41, h20 ⊥ h40, h20 ⊥ h41, h20 ⊥ h30, h20 ⊥ h31, h20 ⊥ h21, h20 ⊥ h0 ∪ h21, h21 ⊥ h41, h21 ⊥ h31, h21 ⊥ h20, h21 ⊥ h30, h21 ⊥ h40, h30 ⊥ h31, h30 ⊥ h21, h30 ⊥ h40, h30 ⊥ h41, h30 ∪ h31 ∪ h40 ∪ h41 ⊥ h20, h31 ⊥ h20, h31 ⊥ h30, h31 ⊥ h40, h31 ⊥ h41, h40 ⊥ h41, h40 ⊥ h21, h40 ⊥ h31, h41 ⊥ h20, h41 ⊥ h30, h41 ⊥ h40, hP0(h0 ∪ h21 ∪ h31 ∪ h41), hP1((h20 ∪ h21) ∪ h40 ∪ h41), hP2((h30 ∪ h31) ∪ h40 ∪ h41) ⊦

Rule argument

Additional information

Used simplifier rules: h1 ⊥ h2 ⊦ h1 ∪ h2 ⊥ h0 ↔ h0 ⊥ h1 ∧ h0 ⊥ h2; (s) h1 ⊥ h ⊦ h0 ⊥ h1 ∪ h ↔ h0 ⊥ h1 ∧ h0 ⊥ h; (ws) ⊦ h0 ⊥ h1 → h1 ⊥ h0; (ss) Used terms: h20, h0 ∪ h21, h30 ∪ h31 ∪ h40 ∪ h41

Proof step 24 from proof sharing-ass-aux1 (previous step) (back to tree)

A spec-lemma

Proof step 25 from proof sharing-ass-aux1 (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 26:

  h20 ∪ ((h30 ∪ h40) ∪ h21 ∪ h31 ∪ h41) ∪ h0 ≠ h20 ∪ (h0 ∪ h21) ∪ h30 ∪ h31 ∪ h40 ∪ h41, h0 ⊥ h20, h0 ⊥ h40, h0 ⊥ h30, h0 ⊥ h41, h0 ⊥ h31, h0 ⊥ h21, h20 ⊥ h0, h20 ⊥ h21, h20 ⊥ h31, h20 ⊥ h30, h20 ⊥ h41, h20 ⊥ h40, h21 ⊥ h40, h21 ⊥ h30, h21 ⊥ h20, h21 ⊥ h31, h21 ⊥ h41, h30 ⊥ h41, h30 ⊥ h40, h30 ⊥ h21, h30 ⊥ h31, h31 ⊥ h41, h31 ⊥ h40, h31 ⊥ h30, h31 ⊥ h20, h40 ⊥ h31, h40 ⊥ h21, h40 ⊥ h41, h41 ⊥ h40, h41 ⊥ h30, h41 ⊥ h20, hP0(h0 ∪ h21 ∪ h31 ∪ h41), hP1((h20 ∪ h21) ∪ h40 ∪ h41), hP2((h30 ∪ h31) ∪ h40 ∪ h41) ⊦

Rule argument

Additional information

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

Proof step 26 from proof sharing-ass-aux1 (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 27:

  h ⊥ h0, h ⊥ h1 ⊦ h ∪ h0 = h ∪ h1 ↔ h0 = h1

• Proof step 28:

  h20 ∪ ((h30 ∪ h40) ∪ h21 ∪ h31 ∪ h41) ∪ h0 ≠ h20 ∪ (h0 ∪ h21) ∪ h30 ∪ h31 ∪ h40 ∪ h41, h0 ⊥ h21, h0 ⊥ h31, h0 ⊥ h41, h0 ⊥ h30, h0 ⊥ h40, h0 ⊥ h20, h20 ⊥ h40, h20 ⊥ h41, h20 ⊥ h30, h20 ⊥ h31, h20 ⊥ h21, h20 ⊥ h0, h21 ⊥ h41, h21 ⊥ h31, h21 ⊥ h20, h21 ⊥ h30, h21 ⊥ h40, h30 ⊥ h31, h30 ⊥ h21, h30 ⊥ h40, h30 ⊥ h41, h31 ⊥ h20, h31 ⊥ h30, h31 ⊥ h40, h31 ⊥ h41, h40 ⊥ h41, h40 ⊥ h21, h40 ⊥ h31, h41 ⊥ h20, h41 ⊥ h30, h41 ⊥ h40, hP0(h0 ∪ h21 ∪ h31 ∪ h41), hP1((h20 ∪ h21) ∪ h40 ∪ h41), hP2((h30 ∪ h31) ∪ h40 ∪ h41) ⊦ h20 ⊥ (h0 ∪ h21) ∪ h30 ∪ h31 ∪ h40 ∪ h41 ∧ h20 ⊥ ((h30 ∪ h40) ∪ h21 ∪ h31 ∪ h41) ∪ h0

• Proof step 30:

  (h0 ∪ h21) ∪ h30 ∪ h31 ∪ h40 ∪ h41 ≠ ((h30 ∪ h40) ∪ h21 ∪ h31 ∪ h41) ∪ h0, h0 ⊥ h21, h0 ⊥ h31, h0 ⊥ h41, h0 ⊥ h30, h0 ⊥ h40, h0 ⊥ h20, h20 ⊥ h40, h20 ⊥ h41, h20 ⊥ h30, h20 ⊥ h31, h20 ⊥ h21, h20 ⊥ h0, h20 ⊥ (h0 ∪ h21) ∪ h30 ∪ h31 ∪ h40 ∪ h41, h20 ⊥ ((h30 ∪ h40) ∪ h21 ∪ h31 ∪ h41) ∪ h0, h21 ⊥ h41, h21 ⊥ h31, h21 ⊥ h20, h21 ⊥ h30, h21 ⊥ h40, h30 ⊥ h31, h30 ⊥ h21, h30 ⊥ h40, h30 ⊥ h41, h31 ⊥ h20, h31 ⊥ h30, h31 ⊥ h40, h31 ⊥ h41, h40 ⊥ h41, h40 ⊥ h21, h40 ⊥ h31, h41 ⊥ h20, h41 ⊥ h30, h41 ⊥ h40, hP0(h0 ∪ h21 ∪ h31 ∪ h41), hP1((h20 ∪ h21) ∪ h40 ∪ h41), hP2((h30 ∪ h31) ∪ h40 ∪ h41) ⊦

Rule argument

Additional information

Used terms: h20, ((h30 ∪ h40) ∪ h21 ∪ h31 ∪ h41) ∪ h0, (h0 ∪ h21) ∪ h30 ∪ h31 ∪ h40 ∪ h41

Proof step 27 from proof sharing-ass-aux1 (previous step) (back to tree)

A spec-lemma

Proof step 28 from proof sharing-ass-aux1 (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 29:

  h20 ∪ ((h30 ∪ h40) ∪ h21 ∪ h31 ∪ h41) ∪ h0 ≠ h20 ∪ (h0 ∪ h21) ∪ h30 ∪ h31 ∪ h40 ∪ h41, h0 ⊥ h20, h0 ⊥ h40, h0 ⊥ h30, h0 ⊥ h41, h0 ⊥ h31, h0 ⊥ h21, h20 ⊥ h0, h20 ⊥ h21, h20 ⊥ h31, h20 ⊥ h30, h20 ⊥ h41, h20 ⊥ h40, h21 ⊥ h40, h21 ⊥ h30, h21 ⊥ h20, h21 ⊥ h31, h21 ⊥ h41, h30 ⊥ h41, h30 ⊥ h40, h30 ⊥ h21, h30 ⊥ h31, h31 ⊥ h41, h31 ⊥ h40, h31 ⊥ h30, h31 ⊥ h20, h40 ⊥ h31, h40 ⊥ h21, h40 ⊥ h41, h41 ⊥ h40, h41 ⊥ h30, h41 ⊥ h20, hP0(h0 ∪ h21 ∪ h31 ∪ h41), hP1((h20 ∪ h21) ∪ h40 ∪ h41), hP2((h30 ∪ h31) ∪ h40 ∪ h41) ⊦ h20 ⊥ (h0 ∪ h21) ∪ h30 ∪ h31 ∪ h40 ∪ h41 ∧ h20 ⊥ (h30 ∪ h40) ∪ h21 ∪ h31 ∪ h41

Rule argument

Additional information

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

Proof step 29 from proof sharing-ass-aux1 (previous step) (back to tree)

User applied rule case distinction

And closed the goal!

Rule argument

Additional information

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

Proof step 30 from proof sharing-ass-aux1 (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 31:

  (h0 ∪ h21) ∪ h30 ∪ h31 ∪ h40 ∪ h41 ≠ ((h30 ∪ h40) ∪ h21 ∪ h31 ∪ h41) ∪ h0, h0 ⊥ h20, h0 ⊥ h40, h0 ⊥ h30, h0 ⊥ h41, h0 ⊥ h31, h0 ⊥ h21, h20 ⊥ h0, h20 ⊥ h21, h20 ⊥ h31, h20 ⊥ h30, h20 ⊥ h41, h20 ⊥ h40, h21 ⊥ h40, h21 ⊥ h30, h21 ⊥ h20, h21 ⊥ h31, h21 ⊥ h41, h30 ⊥ h41, h30 ⊥ h40, h30 ⊥ h21, h30 ⊥ h31, h31 ⊥ h41, h31 ⊥ h40, h31 ⊥ h30, h31 ⊥ h20, h40 ⊥ h31, h40 ⊥ h21, h40 ⊥ h41, h41 ⊥ h40, h41 ⊥ h30, h41 ⊥ h20, hP0(h0 ∪ h21 ∪ h31 ∪ h41), hP1((h20 ∪ h21) ∪ h40 ∪ h41), hP2((h30 ∪ h31) ∪ h40 ∪ h41) ⊦

Rule argument

Additional information

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

Proof step 31 from proof sharing-ass-aux1 (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 32:

  ⊦ h0 ⊥ h1 → h1 ∪ h0 = h0 ∪ h1

• Proof step 33:

  (h0 ∪ h21) ∪ h30 ∪ h31 ∪ h40 ∪ h41 ≠ h0 ∪ (h30 ∪ h40) ∪ h21 ∪ h31 ∪ h41, h0 ⊥ h21, h0 ⊥ h31, h0 ⊥ h41, h0 ⊥ h30, h0 ⊥ h40, h0 ⊥ h20, h0 ⊥ (h30 ∪ h40) ∪ h21 ∪ h31 ∪ h41, h20 ⊥ h40, h20 ⊥ h41, h20 ⊥ h30, h20 ⊥ h31, h20 ⊥ h21, h20 ⊥ h0, h21 ⊥ h41, h21 ⊥ h31, h21 ⊥ h20, h21 ⊥ h30, h21 ⊥ h40, h30 ⊥ h31, h30 ⊥ h21, h30 ⊥ h40, h30 ⊥ h41, h31 ⊥ h20, h31 ⊥ h30, h31 ⊥ h40, h31 ⊥ h41, h40 ⊥ h41, h40 ⊥ h21, h40 ⊥ h31, h41 ⊥ h20, h41 ⊥ h30, h41 ⊥ h40, hP0(h0 ∪ h21 ∪ h31 ∪ h41), hP1((h20 ∪ h21) ∪ h40 ∪ h41), hP2((h30 ∪ h31) ∪ h40 ∪ h41) ⊦

Rule argument

Additional information

Used simplifier rules: h1 ⊥ h2 ⊦ h1 ∪ h2 ⊥ h0 ↔ h0 ⊥ h1 ∧ h0 ⊥ h2; (s) ⊦ h0 ⊥ h1 → h1 ⊥ h0; (ss) h1 ⊥ h ⊦ h0 ⊥ h1 ∪ h ↔ h0 ⊥ h1 ∧ h0 ⊥ h; (ss) h1 ⊥ h ⊦ h0 ⊥ h1 ∪ h ↔ h0 ⊥ h1 ∧ h0 ⊥ h; (ws) Used terms: (h30 ∪ h40) ∪ h21 ∪ h31 ∪ h41, h0

Proof step 32 from proof sharing-ass-aux1 (previous step) (back to tree)

A spec-lemma

Proof step 33 from proof sharing-ass-aux1 (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 34:

  (h0 ∪ h21) ∪ h30 ∪ h31 ∪ h40 ∪ h41 ≠ h0 ∪ (h30 ∪ h40) ∪ h21 ∪ h31 ∪ h41, h0 ⊥ h20, h0 ⊥ h40, h0 ⊥ h30, h0 ⊥ h41, h0 ⊥ h31, h0 ⊥ h21, h20 ⊥ h0, h20 ⊥ h21, h20 ⊥ h31, h20 ⊥ h30, h20 ⊥ h41, h20 ⊥ h40, h21 ⊥ h40, h21 ⊥ h30, h21 ⊥ h20, h21 ⊥ h31, h21 ⊥ h41, h30 ⊥ h41, h30 ⊥ h40, h30 ⊥ h21, h30 ⊥ h31, h31 ⊥ h41, h31 ⊥ h40, h31 ⊥ h30, h31 ⊥ h20, h40 ⊥ h31, h40 ⊥ h21, h40 ⊥ h41, h41 ⊥ h40, h41 ⊥ h30, h41 ⊥ h20, hP0(h0 ∪ h21 ∪ h31 ∪ h41), hP1((h20 ∪ h21) ∪ h40 ∪ h41), hP2((h30 ∪ h31) ∪ h40 ∪ h41) ⊦

Rule argument

Additional information

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

Proof step 34 from proof sharing-ass-aux1 (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 35:

  h0 ⊥ h1, h1 ⊥ h, h ⊥ h0 ⊦ (h0 ∪ h1) ∪ h = h0 ∪ h1 ∪ h

• Proof step 36:

  h0 ∪ h21 ∪ h30 ∪ h31 ∪ h40 ∪ h41 ≠ h0 ∪ (h30 ∪ h40) ∪ h21 ∪ h31 ∪ h41, h0 ⊥ h31, h0 ⊥ h41, h0 ⊥ h30, h0 ⊥ h40, h0 ⊥ h20, h0 ⊥ h21, h20 ⊥ h40, h20 ⊥ h41, h20 ⊥ h30, h20 ⊥ h31, h20 ⊥ h21, h20 ⊥ h0, h21 ⊥ h41, h21 ⊥ h31, h21 ⊥ h20, h21 ⊥ h30, h21 ⊥ h40, h21 ⊥ h30 ∪ h31 ∪ h40 ∪ h41, h30 ⊥ h31, h30 ⊥ h21, h30 ⊥ h40, h30 ⊥ h41, h30 ∪ h31 ∪ h40 ∪ h41 ⊥ h0, h31 ⊥ h20, h31 ⊥ h30, h31 ⊥ h40, h31 ⊥ h41, h40 ⊥ h41, h40 ⊥ h21, h40 ⊥ h31, h41 ⊥ h20, h41 ⊥ h30, h41 ⊥ h40, hP0(h0 ∪ h21 ∪ h31 ∪ h41), hP1((h20 ∪ h21) ∪ h40 ∪ h41), hP2((h30 ∪ h31) ∪ h40 ∪ h41) ⊦

Rule argument

Additional information

Used simplifier rules: h1 ⊥ h2 ⊦ h1 ∪ h2 ⊥ h0 ↔ h0 ⊥ h1 ∧ h0 ⊥ h2; (s) ⊦ h0 ⊥ h1 → h1 ⊥ h0; (ss) h1 ⊥ h ⊦ h0 ⊥ h1 ∪ h ↔ h0 ⊥ h1 ∧ h0 ⊥ h; (ws) Used terms: h0, h21, h30 ∪ h31 ∪ h40 ∪ h41

Proof step 35 from proof sharing-ass-aux1 (previous step) (back to tree)

A spec-lemma

Proof step 36 from proof sharing-ass-aux1 (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 37:

  h0 ∪ h21 ∪ h30 ∪ h31 ∪ h40 ∪ h41 ≠ h0 ∪ (h30 ∪ h40) ∪ h21 ∪ h31 ∪ h41, h0 ⊥ h21, h0 ⊥ h20, h0 ⊥ h40, h0 ⊥ h30, h0 ⊥ h41, h0 ⊥ h31, h20 ⊥ h0, h20 ⊥ h21, h20 ⊥ h31, h20 ⊥ h30, h20 ⊥ h41, h20 ⊥ h40, h21 ⊥ h40, h21 ⊥ h30, h21 ⊥ h20, h21 ⊥ h31, h21 ⊥ h41, h30 ⊥ h41, h30 ⊥ h40, h30 ⊥ h21, h30 ⊥ h31, h31 ⊥ h41, h31 ⊥ h40, h31 ⊥ h30, h31 ⊥ h20, h40 ⊥ h31, h40 ⊥ h21, h40 ⊥ h41, h41 ⊥ h40, h41 ⊥ h30, h41 ⊥ h20, hP0(h0 ∪ h21 ∪ h31 ∪ h41), hP1((h20 ∪ h21) ∪ h40 ∪ h41), hP2((h30 ∪ h31) ∪ h40 ∪ h41) ⊦

Rule argument

Additional information

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

Proof step 37 from proof sharing-ass-aux1 (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 38:

  h ⊥ h0, h ⊥ h1 ⊦ h ∪ h0 = h ∪ h1 ↔ h0 = h1

• Proof step 39:

  h21 ∪ h30 ∪ h31 ∪ h40 ∪ h41 ≠ (h30 ∪ h40) ∪ h21 ∪ h31 ∪ h41, h0 ⊥ h31, h0 ⊥ h41, h0 ⊥ h30, h0 ⊥ h40, h0 ⊥ h20, h0 ⊥ h21, h0 ⊥ h21 ∪ h30 ∪ h31 ∪ h40 ∪ h41, h0 ⊥ (h30 ∪ h40) ∪ h21 ∪ h31 ∪ h41, h20 ⊥ h40, h20 ⊥ h41, h20 ⊥ h30, h20 ⊥ h31, h20 ⊥ h21, h20 ⊥ h0, h21 ⊥ h41, h21 ⊥ h31, h21 ⊥ h20, h21 ⊥ h30, h21 ⊥ h40, h30 ⊥ h31, h30 ⊥ h21, h30 ⊥ h40, h30 ⊥ h41, h31 ⊥ h20, h31 ⊥ h30, h31 ⊥ h40, h31 ⊥ h41, h40 ⊥ h41, h40 ⊥ h21, h40 ⊥ h31, h41 ⊥ h20, h41 ⊥ h30, h41 ⊥ h40, hP0(h0 ∪ h21 ∪ h31 ∪ h41), hP1((h20 ∪ h21) ∪ h40 ∪ h41), hP2((h30 ∪ h31) ∪ h40 ∪ h41) ⊦

Rule argument

Additional information

Used simplifier rules: h1 ⊥ h2 ⊦ h1 ∪ h2 ⊥ h0 ↔ h0 ⊥ h1 ∧ h0 ⊥ h2; (s) ⊦ h0 ⊥ h1 → h1 ⊥ h0; (ss) h1 ⊥ h ⊦ h0 ⊥ h1 ∪ h ↔ h0 ⊥ h1 ∧ h0 ⊥ h; (ss) h1 ⊥ h ⊦ h0 ⊥ h1 ∪ h ↔ h0 ⊥ h1 ∧ h0 ⊥ h; (ws) Used terms: h0, h21 ∪ h30 ∪ h31 ∪ h40 ∪ h41, (h30 ∪ h40) ∪ h21 ∪ h31 ∪ h41

Proof step 38 from proof sharing-ass-aux1 (previous step) (back to tree)

A spec-lemma

Proof step 39 from proof sharing-ass-aux1 (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 40:

  h21 ∪ h30 ∪ h31 ∪ h40 ∪ h41 ≠ (h30 ∪ h40) ∪ h21 ∪ h31 ∪ h41, h0 ⊥ h21, h0 ⊥ h20, h0 ⊥ h40, h0 ⊥ h30, h0 ⊥ h41, h0 ⊥ h31, h20 ⊥ h0, h20 ⊥ h21, h20 ⊥ h31, h20 ⊥ h30, h20 ⊥ h41, h20 ⊥ h40, h21 ⊥ h40, h21 ⊥ h30, h21 ⊥ h20, h21 ⊥ h31, h21 ⊥ h41, h30 ⊥ h41, h30 ⊥ h40, h30 ⊥ h21, h30 ⊥ h31, h31 ⊥ h41, h31 ⊥ h40, h31 ⊥ h30, h31 ⊥ h20, h40 ⊥ h31, h40 ⊥ h21, h40 ⊥ h41, h41 ⊥ h40, h41 ⊥ h30, h41 ⊥ h20, hP0(h0 ∪ h21 ∪ h31 ∪ h41), hP1((h20 ∪ h21) ∪ h40 ∪ h41), hP2((h30 ∪ h31) ∪ h40 ∪ h41) ⊦

Rule argument

Additional information

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

Proof step 40 from proof sharing-ass-aux1 (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 41:

  ⊦ h0 ⊥ h1 → h1 ∪ h0 = h0 ∪ h1

• Proof step 42:

  h21 ∪ h30 ∪ h31 ∪ h40 ∪ h41 ≠ (h21 ∪ h31 ∪ h41) ∪ h30 ∪ h40, h0 ⊥ h31, h0 ⊥ h41, h0 ⊥ h30, h0 ⊥ h40, h0 ⊥ h20, h0 ⊥ h21, h20 ⊥ h40, h20 ⊥ h41, h20 ⊥ h30, h20 ⊥ h31, h20 ⊥ h21, h20 ⊥ h0, h21 ⊥ h41, h21 ⊥ h31, h21 ⊥ h20, h21 ⊥ h30, h21 ⊥ h40, h21 ∪ h31 ∪ h41 ⊥ h30 ∪ h40, h30 ⊥ h31, h30 ⊥ h21, h30 ⊥ h40, h30 ⊥ h41, h31 ⊥ h20, h31 ⊥ h30, h31 ⊥ h40, h31 ⊥ h41, h40 ⊥ h41, h40 ⊥ h21, h40 ⊥ h31, h41 ⊥ h20, h41 ⊥ h30, h41 ⊥ h40, hP0(h0 ∪ h21 ∪ h31 ∪ h41), hP1((h20 ∪ h21) ∪ h40 ∪ h41), hP2((h30 ∪ h31) ∪ h40 ∪ h41) ⊦

Rule argument

Additional information

Used simplifier rules: h1 ⊥ h ⊦ h0 ⊥ h1 ∪ h ↔ h0 ⊥ h1 ∧ h0 ⊥ h; (ws) h1 ⊥ h2 ⊦ h1 ∪ h2 ⊥ h0 ↔ h0 ⊥ h1 ∧ h0 ⊥ h2; (s) ⊦ h0 ⊥ h1 → h1 ⊥ h0; (ss) Used terms: h30 ∪ h40, h21 ∪ h31 ∪ h41

Proof step 41 from proof sharing-ass-aux1 (previous step) (back to tree)

A spec-lemma

Proof step 42 from proof sharing-ass-aux1 (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 43:

  h21 ∪ h30 ∪ h31 ∪ h40 ∪ h41 ≠ (h21 ∪ h31 ∪ h41) ∪ h30 ∪ h40, h0 ⊥ h21, h0 ⊥ h20, h0 ⊥ h40, h0 ⊥ h30, h0 ⊥ h41, h0 ⊥ h31, h20 ⊥ h0, h20 ⊥ h21, h20 ⊥ h31, h20 ⊥ h30, h20 ⊥ h41, h20 ⊥ h40, h21 ⊥ h40, h21 ⊥ h30, h21 ⊥ h20, h21 ⊥ h31, h21 ⊥ h41, h30 ⊥ h41, h30 ⊥ h40, h30 ⊥ h21, h30 ⊥ h31, h31 ⊥ h41, h31 ⊥ h40, h31 ⊥ h30, h31 ⊥ h20, h40 ⊥ h31, h40 ⊥ h21, h40 ⊥ h41, h41 ⊥ h40, h41 ⊥ h30, h41 ⊥ h20, hP0(h0 ∪ h21 ∪ h31 ∪ h41), hP1((h20 ∪ h21) ∪ h40 ∪ h41), hP2((h30 ∪ h31) ∪ h40 ∪ h41) ⊦

Rule argument

Additional information

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

Proof step 43 from proof sharing-ass-aux1 (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 44:

  h0 ⊥ h1, h1 ⊥ h, h ⊥ h0 ⊦ (h0 ∪ h1) ∪ h = h0 ∪ h1 ∪ h

• Proof step 45:

  h21 ∪ h30 ∪ h31 ∪ h40 ∪ h41 ≠ h21 ∪ (h31 ∪ h41) ∪ h30 ∪ h40, h0 ⊥ h31, h0 ⊥ h41, h0 ⊥ h30, h0 ⊥ h40, h0 ⊥ h20, h0 ⊥ h21, h20 ⊥ h40, h20 ⊥ h41, h20 ⊥ h30, h20 ⊥ h31, h20 ⊥ h21, h20 ⊥ h0, h21 ⊥ h41, h21 ⊥ h31, h21 ⊥ h20, h21 ⊥ h30, h21 ⊥ h40, h21 ⊥ h31 ∪ h41, h30 ⊥ h31, h30 ⊥ h21, h30 ⊥ h40, h30 ⊥ h41, h30 ∪ h40 ⊥ h21, h31 ⊥ h20, h31 ⊥ h30, h31 ⊥ h40, h31 ⊥ h41, h31 ∪ h41 ⊥ h30 ∪ h40, h40 ⊥ h41, h40 ⊥ h21, h40 ⊥ h31, h41 ⊥ h20, h41 ⊥ h30, h41 ⊥ h40, hP0(h0 ∪ h21 ∪ h31 ∪ h41), hP1((h20 ∪ h21) ∪ h40 ∪ h41), hP2((h30 ∪ h31) ∪ h40 ∪ h41) ⊦

Rule argument

Additional information

Used simplifier rules: h1 ⊥ h ⊦ h0 ⊥ h1 ∪ h ↔ h0 ⊥ h1 ∧ h0 ⊥ h; (ws) h1 ⊥ h2 ⊦ h1 ∪ h2 ⊥ h0 ↔ h0 ⊥ h1 ∧ h0 ⊥ h2; (s) ⊦ h0 ⊥ h1 → h1 ⊥ h0; (ss) Used terms: h21, h31 ∪ h41, h30 ∪ h40

Proof step 44 from proof sharing-ass-aux1 (previous step) (back to tree)

A spec-lemma

Proof step 45 from proof sharing-ass-aux1 (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 46:

  h30 ∪ h31 ∪ h40 ∪ h41 ≠ (h31 ∪ h41) ∪ h30 ∪ h40, h0 ⊥ h21, h0 ⊥ h20, h0 ⊥ h40, h0 ⊥ h30, h0 ⊥ h41, h0 ⊥ h31, h20 ⊥ h0, h20 ⊥ h21, h20 ⊥ h31, h20 ⊥ h30, h20 ⊥ h41, h20 ⊥ h40, h21 ⊥ h40, h21 ⊥ h30, h21 ⊥ h20, h21 ⊥ h31, h21 ⊥ h41, h30 ⊥ h41, h30 ⊥ h40, h30 ⊥ h21, h30 ⊥ h31, h31 ⊥ h41, h31 ⊥ h40, h31 ⊥ h30, h31 ⊥ h20, h40 ⊥ h31, h40 ⊥ h21, h40 ⊥ h41, h41 ⊥ h40, h41 ⊥ h30, h41 ⊥ h20, hP0(h0 ∪ h21 ∪ h31 ∪ h41), hP1((h20 ∪ h21) ∪ h40 ∪ h41), hP2((h30 ∪ h31) ∪ h40 ∪ h41) ⊦

Rule argument

Additional information

Used simplifier rules: h1 ⊥ h ⊦ h0 ⊥ h1 ∪ h ↔ h0 ⊥ h1 ∧ h0 ⊥ h; (ws) h1 ⊥ h2 ⊦ h1 ∪ h2 ⊥ h0 ↔ h0 ⊥ h1 ∧ h0 ⊥ h2; (s) h ⊥ h0, h ⊥ h1 ⊦ h ∪ h0 = h ∪ h1 ↔ h0 = h1; (s) ⊦ h0 ⊥ h1 → h1 ⊥ h0; (ss)

Proof step 46 from proof sharing-ass-aux1 (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 47:

  ⊦ h0 ⊥ h1 → h1 ∪ h0 = h0 ∪ h1

• Proof step 48:

  h30 ∪ h31 ∪ h40 ∪ h41 ≠ (h30 ∪ h40) ∪ h31 ∪ h41, h0 ⊥ h31, h0 ⊥ h41, h0 ⊥ h30, h0 ⊥ h40, h0 ⊥ h20, h0 ⊥ h21, h20 ⊥ h40, h20 ⊥ h41, h20 ⊥ h30, h20 ⊥ h31, h20 ⊥ h21, h20 ⊥ h0, h21 ⊥ h41, h21 ⊥ h31, h21 ⊥ h20, h21 ⊥ h30, h21 ⊥ h40, h30 ⊥ h31, h30 ⊥ h21, h30 ⊥ h40, h30 ⊥ h41, h30 ∪ h40 ⊥ h31 ∪ h41, h31 ⊥ h20, h31 ⊥ h30, h31 ⊥ h40, h31 ⊥ h41, h40 ⊥ h41, h40 ⊥ h21, h40 ⊥ h31, h41 ⊥ h20, h41 ⊥ h30, h41 ⊥ h40, hP0(h0 ∪ h21 ∪ h31 ∪ h41), hP1((h20 ∪ h21) ∪ h40 ∪ h41), hP2((h30 ∪ h31) ∪ h40 ∪ h41) ⊦

Rule argument

Additional information

Used simplifier rules: h1 ⊥ h2 ⊦ h1 ∪ h2 ⊥ h0 ↔ h0 ⊥ h1 ∧ h0 ⊥ h2; (s) ⊦ h0 ⊥ h1 → h1 ⊥ h0; (ss) Used terms: h31 ∪ h41, h30 ∪ h40

Proof step 47 from proof sharing-ass-aux1 (previous step) (back to tree)

A spec-lemma

Proof step 48 from proof sharing-ass-aux1 (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 49:

  h30 ∪ h31 ∪ h40 ∪ h41 ≠ (h30 ∪ h40) ∪ h31 ∪ h41, h0 ⊥ h21, h0 ⊥ h20, h0 ⊥ h40, h0 ⊥ h30, h0 ⊥ h41, h0 ⊥ h31, h20 ⊥ h0, h20 ⊥ h21, h20 ⊥ h31, h20 ⊥ h30, h20 ⊥ h41, h20 ⊥ h40, h21 ⊥ h40, h21 ⊥ h30, h21 ⊥ h20, h21 ⊥ h31, h21 ⊥ h41, h30 ⊥ h41, h30 ⊥ h40, h30 ⊥ h21, h30 ⊥ h31, h31 ⊥ h41, h31 ⊥ h40, h31 ⊥ h30, h31 ⊥ h20, h40 ⊥ h31, h40 ⊥ h21, h40 ⊥ h41, h41 ⊥ h40, h41 ⊥ h30, h41 ⊥ h20, hP0(h0 ∪ h21 ∪ h31 ∪ h41), hP1((h20 ∪ h21) ∪ h40 ∪ h41), hP2((h30 ∪ h31) ∪ h40 ∪ h41) ⊦

Rule argument

Additional information

Used simplifier rules: h1 ⊥ h2 ⊦ h1 ∪ h2 ⊥ h0 ↔ h0 ⊥ h1 ∧ h0 ⊥ h2; (s)

Proof step 49 from proof sharing-ass-aux1 (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 50:

  h0 ⊥ h1, h1 ⊥ h, h ⊥ h0 ⊦ (h0 ∪ h1) ∪ h = h0 ∪ h1 ∪ h

Rule argument

Additional information

Used simplifier rules: h1 ⊥ h ⊦ h0 ⊥ h1 ∪ h ↔ h0 ⊥ h1 ∧ h0 ⊥ h; (ws) h ⊥ h0, h ⊥ h1 ⊦ h ∪ h0 = h ∪ h1 ↔ h0 = h1; (s) ⊦ h0 ⊥ h1 → h1 ⊥ h0; (ss) h0 ⊥ h1, h1 ⊥ h, h ⊥ h0 ⊦ h ∪ h0 ∪ h1 = h0 ∪ h ∪ h1 ↔ true; (ss) h1 ⊥ h2 ⊦ h1 ∪ h2 ⊥ h0 ↔ h0 ⊥ h1 ∧ h0 ⊥ h2; (s) Used terms: h30, h40, h31 ∪ h41

Proof step 50 from proof sharing-ass-aux1 (previous step) (back to tree)

A spec-lemma

Proof step 51 from proof sharing-ass-aux1 (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 52:

  h0 ⊥ h1, h1 ⊥ h, h ⊥ h0 ⊦ (h0 ∪ h1) ∪ h = h0 ∪ h1 ∪ h

Rule argument

Additional information

Used simplifier rules: h1 ⊥ h ⊦ h0 ⊥ h1 ∪ h ↔ h0 ⊥ h1 ∧ h0 ⊥ h; (ws) h1 ⊥ h2 ⊦ h1 ∪ h2 ⊥ h0 ↔ h0 ⊥ h1 ∧ h0 ⊥ h2; (s) ⊦ h0 ⊥ h1 → h1 ⊥ h0; (ss) Used terms: h20, h21, h40 ∪ h41

Proof step 52 from proof sharing-ass-aux1 (previous step) (back to tree)

A spec-lemma

Proof step 53 from proof sharing-ass-aux1 (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 54:

  h0 ⊥ h1, h1 ⊥ h, h ⊥ h0 ⊦ (h0 ∪ h1) ∪ h = h0 ∪ h1 ∪ h

Rule argument

Additional information

Used simplifier rules: h1 ⊥ h ⊦ h0 ⊥ h1 ∪ h ↔ h0 ⊥ h1 ∧ h0 ⊥ h; (ws) h1 ⊥ h2 ⊦ h1 ∪ h2 ⊥ h0 ↔ h0 ⊥ h1 ∧ h0 ⊥ h2; (s) ⊦ h0 ⊥ h1 → h1 ⊥ h0; (ss) Used terms: h30, h31, h40 ∪ h41

Proof step 54 from proof sharing-ass-aux1 (previous step) (back to tree)

A spec-lemma

Proof step 55 from proof sharing-ass-aux1 (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 56:

  h0 ⊥ h1, h0 ⊥ h2, h0 ⊥ h21, h0 ⊥ h20, h0 ⊥ h10, h0 ⊥ h210, h1 ⊥ h2, h1 ⊥ h21, h1 ⊥ h20, h1 ⊥ h10, h1 ⊥ h210, h10 ⊥ h210, h2 ⊥ h21, h2 ⊥ h20, h2 ⊥ h10, h2 ⊥ h210, h20 ⊥ h10, h20 ⊥ h210, h21 ⊥ h20, h21 ⊥ h10, h21 ⊥ h210, hP0(h0 ∪ h10 ∪ h20 ∪ h210), hP1(h1 ∪ h10 ∪ h21 ∪ h210), hP2(h2 ∪ h20 ∪ h21 ∪ h210) ⊦ ∃ h3, h4, h5. h3 ⊥ h5 ∧ h3 ⊥ h4 ∧ h4 ⊥ h5 ∧ (h1 ∪ h0 ∪ h10) ∪ h2 ∪ h20 ∪ h21 ∪ h210 = h3 ∪ h4 ∪ h5 ∧ hP0(h3 ∪ h5) ∧ (hP1 ⊗ hP2)(h4 ∪ h5)

Rule argument

Additional information

Proof step 56 from proof sharing-ass-aux1 (previous step) (back to tree)

User applied rule exists right

And obtained the following new goals

• Proof step 57:

  h0 ⊥ h210, h0 ⊥ h10, h0 ⊥ h20, h0 ⊥ h21, h0 ⊥ h2, h0 ⊥ h1, h1 ⊥ h210, h1 ⊥ h10, h1 ⊥ h20, h1 ⊥ h21, h1 ⊥ h2, h10 ⊥ h210, h2 ⊥ h210, h2 ⊥ h10, h2 ⊥ h20, h2 ⊥ h21, h20 ⊥ h210, h20 ⊥ h10, h21 ⊥ h210, h21 ⊥ h10, h21 ⊥ h20, hP0(h0 ∪ h10 ∪ h20 ∪ h210), hP1(h1 ∪ h10 ∪ h21 ∪ h210), hP2(h2 ∪ h20 ∪ h21 ∪ h210) ⊦ h0 ⊥ h10 ∪ h20 ∪ h210 ∧ h0 ⊥ h1 ∪ h2 ∪ h21 ∧ h1 ∪ h2 ∪ h21 ⊥ h10 ∪ h20 ∪ h210 ∧ (h1 ∪ h0 ∪ h10) ∪ h2 ∪ h20 ∪ h21 ∪ h210 = h0 ∪ (h1 ∪ h2 ∪ h21) ∪ h10 ∪ h20 ∪ h210 ∧ hP0(h0 ∪ h10 ∪ h20 ∪ h210) ∧ (hP1 ⊗ hP2)((h1 ∪ h2 ∪ h21) ∪ h10 ∪ h20 ∪ h210)

Rule argument

Additional information

Used terms: h0, h1 ∪ h2 ∪ h21, h10 ∪ h20 ∪ h210

Proof step 57 from proof sharing-ass-aux1 (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 58:

  h0 ⊥ h1, h0 ⊥ h2, h0 ⊥ h21, h0 ⊥ h20, h0 ⊥ h10, h0 ⊥ h210, h1 ⊥ h2, h1 ⊥ h21, h1 ⊥ h20, h1 ⊥ h10, h1 ⊥ h210, h10 ⊥ h210, h2 ⊥ h21, h2 ⊥ h20, h2 ⊥ h10, h2 ⊥ h210, h20 ⊥ h10, h20 ⊥ h210, h21 ⊥ h20, h21 ⊥ h10, h21 ⊥ h210, hP0(h0 ∪ h10 ∪ h20 ∪ h210), hP1(h1 ∪ h10 ∪ h21 ∪ h210), hP2(h2 ∪ h20 ∪ h21 ∪ h210) ⊦ (h1 ∪ h0 ∪ h10) ∪ h2 ∪ h20 ∪ h21 ∪ h210 = h0 ∪ (h1 ∪ h2 ∪ h21) ∪ h10 ∪ h20 ∪ h210 ∧ (hP1 ⊗ hP2)((h1 ∪ h2 ∪ h21) ∪ h10 ∪ h20 ∪ h210)

Rule argument

Additional information

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

Proof step 58 from proof sharing-ass-aux1 (previous step) (back to tree)

User applied rule case distinction

And obtained the following new goals

• Proof step 59:

  (h1 ∪ h0 ∪ h10) ∪ h2 ∪ h20 ∪ h21 ∪ h210 ≠ h0 ∪ (h1 ∪ h2 ∪ h21) ∪ h10 ∪ h20 ∪ h210, h0 ⊥ h210, h0 ⊥ h10, h0 ⊥ h20, h0 ⊥ h21, h0 ⊥ h2, h0 ⊥ h1, h1 ⊥ h210, h1 ⊥ h10, h1 ⊥ h20, h1 ⊥ h21, h1 ⊥ h2, h10 ⊥ h210, h2 ⊥ h210, h2 ⊥ h10, h2 ⊥ h20, h2 ⊥ h21, h20 ⊥ h210, h20 ⊥ h10, h21 ⊥ h210, h21 ⊥ h10, h21 ⊥ h20, hP0(h0 ∪ h10 ∪ h20 ∪ h210), hP1(h1 ∪ h10 ∪ h21 ∪ h210), hP2(h2 ∪ h20 ∪ h21 ∪ h210) ⊦

• Proof step 96:

  h0 ⊥ h210, h0 ⊥ h10, h0 ⊥ h20, h0 ⊥ h21, h0 ⊥ h2, h0 ⊥ h1, h1 ⊥ h210, h1 ⊥ h10, h1 ⊥ h20, h1 ⊥ h21, h1 ⊥ h2, h10 ⊥ h210, h2 ⊥ h210, h2 ⊥ h10, h2 ⊥ h20, h2 ⊥ h21, h20 ⊥ h210, h20 ⊥ h10, h21 ⊥ h210, h21 ⊥ h10, h21 ⊥ h20, hP0(h0 ∪ h10 ∪ h20 ∪ h210), hP1(h1 ∪ h10 ∪ h21 ∪ h210), hP2(h2 ∪ h20 ∪ h21 ∪ h210), ¬ (hP1 ⊗ hP2)((h1 ∪ h2 ∪ h21) ∪ h10 ∪ h20 ∪ h210) ⊦

Rule argument

Additional information

Proof step 59 from proof sharing-ass-aux1 (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 60:

  ⊦ h0 ⊥ h1 → h1 ∪ h0 = h0 ∪ h1

• Proof step 61:

  (h1 ∪ h0 ∪ h10) ∪ h2 ∪ h20 ∪ h21 ∪ h210 ≠ ((h1 ∪ h2 ∪ h21) ∪ h10 ∪ h20 ∪ h210) ∪ h0, h0 ⊥ h1, h0 ⊥ h2, h0 ⊥ h21, h0 ⊥ h20, h0 ⊥ h10, h0 ⊥ h210, h1 ⊥ h2, h1 ⊥ h21, h1 ⊥ h20, h1 ⊥ h10, h1 ⊥ h210, (h1 ∪ h2 ∪ h21) ∪ h10 ∪ h20 ∪ h210 ⊥ h0, h10 ⊥ h210, h2 ⊥ h21, h2 ⊥ h20, h2 ⊥ h10, h2 ⊥ h210, h20 ⊥ h10, h20 ⊥ h210, h21 ⊥ h20, h21 ⊥ h10, h21 ⊥ h210, hP0(h0 ∪ h10 ∪ h20 ∪ h210), hP1(h1 ∪ h10 ∪ h21 ∪ h210), hP2(h2 ∪ h20 ∪ h21 ∪ h210) ⊦

Rule argument

Additional information

Used simplifier rules: h1 ⊥ h2 ⊦ h1 ∪ h2 ⊥ h0 ↔ h0 ⊥ h1 ∧ h0 ⊥ h2; (s) ⊦ h0 ⊥ h1 → h1 ⊥ h0; (ss) h1 ⊥ h ⊦ h0 ⊥ h1 ∪ h ↔ h0 ⊥ h1 ∧ h0 ⊥ h; (ws) Used terms: h0, (h1 ∪ h2 ∪ h21) ∪ h10 ∪ h20 ∪ h210

Proof step 60 from proof sharing-ass-aux1 (previous step) (back to tree)

A spec-lemma

Proof step 61 from proof sharing-ass-aux1 (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 62:

  (h1 ∪ h0 ∪ h10) ∪ h2 ∪ h20 ∪ h21 ∪ h210 ≠ ((h1 ∪ h2 ∪ h21) ∪ h10 ∪ h20 ∪ h210) ∪ h0, h0 ⊥ h210, h0 ⊥ h10, h0 ⊥ h20, h0 ⊥ h21, h0 ⊥ h2, h0 ⊥ h1, h1 ⊥ h210, h1 ⊥ h10, h1 ⊥ h20, h1 ⊥ h21, h1 ⊥ h2, h10 ⊥ h210, h2 ⊥ h210, h2 ⊥ h10, h2 ⊥ h20, h2 ⊥ h21, h20 ⊥ h210, h20 ⊥ h10, h21 ⊥ h210, h21 ⊥ h10, h21 ⊥ h20, hP0(h0 ∪ h10 ∪ h20 ∪ h210), hP1(h1 ∪ h10 ∪ h21 ∪ h210), hP2(h2 ∪ h20 ∪ h21 ∪ h210) ⊦

Rule argument

Additional information

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

Proof step 62 from proof sharing-ass-aux1 (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 63:

  h0 ⊥ h1, h1 ⊥ h, h ⊥ h0 ⊦ (h0 ∪ h1) ∪ h = h0 ∪ h1 ∪ h

• Proof step 64:

  h1 ∪ (h0 ∪ h10) ∪ h2 ∪ h20 ∪ h21 ∪ h210 ≠ ((h1 ∪ h2 ∪ h21) ∪ h10 ∪ h20 ∪ h210) ∪ h0, h0 ⊥ h1, h0 ⊥ h2, h0 ⊥ h21, h0 ⊥ h20, h0 ⊥ h10, h0 ⊥ h210, h0 ∪ h10 ⊥ h2 ∪ h20 ∪ h21 ∪ h210, h1 ⊥ h2, h1 ⊥ h21, h1 ⊥ h20, h1 ⊥ h10, h1 ⊥ h210, h1 ⊥ h0 ∪ h10, h10 ⊥ h210, h2 ⊥ h21, h2 ⊥ h20, h2 ⊥ h10, h2 ⊥ h210, h2 ∪ h20 ∪ h21 ∪ h210 ⊥ h1, h20 ⊥ h10, h20 ⊥ h210, h21 ⊥ h20, h21 ⊥ h10, h21 ⊥ h210, hP0(h0 ∪ h10 ∪ h20 ∪ h210), hP1(h1 ∪ h10 ∪ h21 ∪ h210), hP2(h2 ∪ h20 ∪ h21 ∪ h210) ⊦

Rule argument

Additional information

Used simplifier rules: h1 ⊥ h2 ⊦ h1 ∪ h2 ⊥ h0 ↔ h0 ⊥ h1 ∧ h0 ⊥ h2; (s) h1 ⊥ h ⊦ h0 ⊥ h1 ∪ h ↔ h0 ⊥ h1 ∧ h0 ⊥ h; (ss) h1 ⊥ h ⊦ h0 ⊥ h1 ∪ h ↔ h0 ⊥ h1 ∧ h0 ⊥ h; (ws) ⊦ h0 ⊥ h1 → h1 ⊥ h0; (ss) Used terms: h1, h0 ∪ h10, h2 ∪ h20 ∪ h21 ∪ h210

Proof step 63 from proof sharing-ass-aux1 (previous step) (back to tree)

A spec-lemma

Proof step 64 from proof sharing-ass-aux1 (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 65:

  h1 ∪ (h0 ∪ h10) ∪ h2 ∪ h20 ∪ h21 ∪ h210 ≠ ((h1 ∪ h2 ∪ h21) ∪ h10 ∪ h20 ∪ h210) ∪ h0, h0 ⊥ h210, h0 ⊥ h10, h0 ⊥ h20, h0 ⊥ h21, h0 ⊥ h2, h0 ⊥ h1, h1 ⊥ h0, h1 ⊥ h210, h1 ⊥ h10, h1 ⊥ h20, h1 ⊥ h21, h1 ⊥ h2, h10 ⊥ h210, h10 ⊥ h2, h10 ⊥ h20, h10 ⊥ h21, h2 ⊥ h210, h2 ⊥ h10, h2 ⊥ h20, h2 ⊥ h21, h20 ⊥ h210, h20 ⊥ h10, h21 ⊥ h210, h21 ⊥ h10, h21 ⊥ h20, hP0(h0 ∪ h10 ∪ h20 ∪ h210), hP1(h1 ∪ h10 ∪ h21 ∪ h210), hP2(h2 ∪ h20 ∪ h21 ∪ h210) ⊦

Rule argument

Additional information

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

Proof step 65 from proof sharing-ass-aux1 (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 66:

  h0 ⊥ h1, h1 ⊥ h, h ⊥ h0 ⊦ (h0 ∪ h1) ∪ h = h0 ∪ h1 ∪ h

• Proof step 67:

  h1 ∪ (h0 ∪ h10) ∪ h2 ∪ h20 ∪ h21 ∪ h210 ≠ (h1 ∪ (h2 ∪ h21) ∪ h10 ∪ h20 ∪ h210) ∪ h0, h0 ⊥ h1, h0 ⊥ h2, h0 ⊥ h21, h0 ⊥ h20, h0 ⊥ h10, h0 ⊥ h210, h1 ⊥ h2, h1 ⊥ h21, h1 ⊥ h20, h1 ⊥ h10, h1 ⊥ h210, h1 ⊥ h0, h1 ⊥ h2 ∪ h21, h10 ⊥ h21, h10 ⊥ h20, h10 ⊥ h2, h10 ⊥ h210, h10 ∪ h20 ∪ h210 ⊥ h1, h2 ⊥ h21, h2 ⊥ h20, h2 ⊥ h10, h2 ⊥ h210, h2 ∪ h21 ⊥ h10 ∪ h20 ∪ h210, h20 ⊥ h10, h20 ⊥ h210, h21 ⊥ h20, h21 ⊥ h10, h21 ⊥ h210, hP0(h0 ∪ h10 ∪ h20 ∪ h210), hP1(h1 ∪ h10 ∪ h21 ∪ h210), hP2(h2 ∪ h20 ∪ h21 ∪ h210) ⊦

Rule argument

Additional information

Used simplifier rules: ⊦ h0 ⊥ h1 → h1 ⊥ h0; (ss) h1 ⊥ h2 ⊦ h1 ∪ h2 ⊥ h0 ↔ h0 ⊥ h1 ∧ h0 ⊥ h2; (s) h1 ⊥ h ⊦ h0 ⊥ h1 ∪ h ↔ h0 ⊥ h1 ∧ h0 ⊥ h; (ws) Used terms: h1, h2 ∪ h21, h10 ∪ h20 ∪ h210

Proof step 66 from proof sharing-ass-aux1 (previous step) (back to tree)

A spec-lemma

Proof step 67 from proof sharing-ass-aux1 (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 68:

  h1 ∪ (h0 ∪ h10) ∪ h2 ∪ h20 ∪ h21 ∪ h210 ≠ (h1 ∪ (h2 ∪ h21) ∪ h10 ∪ h20 ∪ h210) ∪ h0, h0 ⊥ h210, h0 ⊥ h10, h0 ⊥ h20, h0 ⊥ h21, h0 ⊥ h2, h0 ⊥ h1, h1 ⊥ h0, h1 ⊥ h210, h1 ⊥ h10, h1 ⊥ h20, h1 ⊥ h21, h1 ⊥ h2, h10 ⊥ h210, h10 ⊥ h2, h10 ⊥ h20, h10 ⊥ h21, h2 ⊥ h210, h2 ⊥ h10, h2 ⊥ h20, h2 ⊥ h21, h20 ⊥ h210, h20 ⊥ h10, h21 ⊥ h210, h21 ⊥ h10, h21 ⊥ h20, hP0(h0 ∪ h10 ∪ h20 ∪ h210), hP1(h1 ∪ h10 ∪ h21 ∪ h210), hP2(h2 ∪ h20 ∪ h21 ∪ h210) ⊦

Rule argument

Additional information

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

Proof step 68 from proof sharing-ass-aux1 (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 69:

  h0 ⊥ h1, h1 ⊥ h, h ⊥ h0 ⊦ (h0 ∪ h1) ∪ h = h0 ∪ h1 ∪ h

• Proof step 70:

  h1 ∪ (h0 ∪ h10) ∪ h2 ∪ h20 ∪ h21 ∪ h210 ≠ h1 ∪ ((h2 ∪ h21) ∪ h10 ∪ h20 ∪ h210) ∪ h0, h0 ⊥ h2, h0 ⊥ h21, h0 ⊥ h20, h0 ⊥ h10, h0 ⊥ h210, h0 ⊥ h1, h1 ⊥ h2, h1 ⊥ h21, h1 ⊥ h20, h1 ⊥ h10, h1 ⊥ h210, h1 ⊥ h0, h1 ⊥ (h2 ∪ h21) ∪ h10 ∪ h20 ∪ h210, h10 ⊥ h21, h10 ⊥ h20, h10 ⊥ h2, h10 ⊥ h210, h2 ⊥ h21, h2 ⊥ h20, h2 ⊥ h10, h2 ⊥ h210, (h2 ∪ h21) ∪ h10 ∪ h20 ∪ h210 ⊥ h0, h20 ⊥ h10, h20 ⊥ h210, h21 ⊥ h20, h21 ⊥ h10, h21 ⊥ h210, hP0(h0 ∪ h10 ∪ h20 ∪ h210), hP1(h1 ∪ h10 ∪ h21 ∪ h210), hP2(h2 ∪ h20 ∪ h21 ∪ h210) ⊦

Rule argument

Additional information

Used simplifier rules: h1 ⊥ h2 ⊦ h1 ∪ h2 ⊥ h0 ↔ h0 ⊥ h1 ∧ h0 ⊥ h2; (s) ⊦ h0 ⊥ h1 → h1 ⊥ h0; (ss) h1 ⊥ h ⊦ h0 ⊥ h1 ∪ h ↔ h0 ⊥ h1 ∧ h0 ⊥ h; (ss) h1 ⊥ h ⊦ h0 ⊥ h1 ∪ h ↔ h0 ⊥ h1 ∧ h0 ⊥ h; (ws) Used terms: h1, (h2 ∪ h21) ∪ h10 ∪ h20 ∪ h210, h0

Proof step 69 from proof sharing-ass-aux1 (previous step) (back to tree)

A spec-lemma

Proof step 70 from proof sharing-ass-aux1 (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 71:

  h1 ∪ (h0 ∪ h10) ∪ h2 ∪ h20 ∪ h21 ∪ h210 ≠ h1 ∪ ((h2 ∪ h21) ∪ h10 ∪ h20 ∪ h210) ∪ h0, h0 ⊥ h1, h0 ⊥ h210, h0 ⊥ h10, h0 ⊥ h20, h0 ⊥ h21, h0 ⊥ h2, h1 ⊥ h0, h1 ⊥ h210, h1 ⊥ h10, h1 ⊥ h20, h1 ⊥ h21, h1 ⊥ h2, h10 ⊥ h210, h10 ⊥ h2, h10 ⊥ h20, h10 ⊥ h21, h2 ⊥ h210, h2 ⊥ h10, h2 ⊥ h20, h2 ⊥ h21, h20 ⊥ h210, h20 ⊥ h10, h21 ⊥ h210, h21 ⊥ h10, h21 ⊥ h20, hP0(h0 ∪ h10 ∪ h20 ∪ h210), hP1(h1 ∪ h10 ∪ h21 ∪ h210), hP2(h2 ∪ h20 ∪ h21 ∪ h210) ⊦

Rule argument

Additional information

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

Proof step 71 from proof sharing-ass-aux1 (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 72:

  h ⊥ h0, h ⊥ h1 ⊦ h ∪ h0 = h ∪ h1 ↔ h0 = h1

• Proof step 73:

  h1 ∪ (h0 ∪ h10) ∪ h2 ∪ h20 ∪ h21 ∪ h210 ≠ h1 ∪ ((h2 ∪ h21) ∪ h10 ∪ h20 ∪ h210) ∪ h0, h0 ⊥ h2, h0 ⊥ h21, h0 ⊥ h20, h0 ⊥ h10, h0 ⊥ h210, h0 ⊥ h1, h1 ⊥ h2, h1 ⊥ h21, h1 ⊥ h20, h1 ⊥ h10, h1 ⊥ h210, h1 ⊥ h0, h10 ⊥ h21, h10 ⊥ h20, h10 ⊥ h2, h10 ⊥ h210, h2 ⊥ h21, h2 ⊥ h20, h2 ⊥ h10, h2 ⊥ h210, h20 ⊥ h10, h20 ⊥ h210, h21 ⊥ h20, h21 ⊥ h10, h21 ⊥ h210, hP0(h0 ∪ h10 ∪ h20 ∪ h210), hP1(h1 ∪ h10 ∪ h21 ∪ h210), hP2(h2 ∪ h20 ∪ h21 ∪ h210) ⊦ h1 ⊥ (h0 ∪ h10) ∪ h2 ∪ h20 ∪ h21 ∪ h210 ∧ h1 ⊥ ((h2 ∪ h21) ∪ h10 ∪ h20 ∪ h210) ∪ h0

• Proof step 75:

  (h0 ∪ h10) ∪ h2 ∪ h20 ∪ h21 ∪ h210 ≠ ((h2 ∪ h21) ∪ h10 ∪ h20 ∪ h210) ∪ h0, h0 ⊥ h2, h0 ⊥ h21, h0 ⊥ h20, h0 ⊥ h10, h0 ⊥ h210, h0 ⊥ h1, h1 ⊥ h2, h1 ⊥ h21, h1 ⊥ h20, h1 ⊥ h10, h1 ⊥ h210, h1 ⊥ h0, h1 ⊥ (h0 ∪ h10) ∪ h2 ∪ h20 ∪ h21 ∪ h210, h1 ⊥ ((h2 ∪ h21) ∪ h10 ∪ h20 ∪ h210) ∪ h0, h10 ⊥ h21, h10 ⊥ h20, h10 ⊥ h2, h10 ⊥ h210, h2 ⊥ h21, h2 ⊥ h20, h2 ⊥ h10, h2 ⊥ h210, h20 ⊥ h10, h20 ⊥ h210, h21 ⊥ h20, h21 ⊥ h10, h21 ⊥ h210, hP0(h0 ∪ h10 ∪ h20 ∪ h210), hP1(h1 ∪ h10 ∪ h21 ∪ h210), hP2(h2 ∪ h20 ∪ h21 ∪ h210) ⊦

Rule argument

Additional information

Used terms: h1, (h0 ∪ h10) ∪ h2 ∪ h20 ∪ h21 ∪ h210, ((h2 ∪ h21) ∪ h10 ∪ h20 ∪ h210) ∪ h0

Proof step 72 from proof sharing-ass-aux1 (previous step) (back to tree)

A spec-lemma

Proof step 73 from proof sharing-ass-aux1 (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 74:

  h1 ∪ (h0 ∪ h10) ∪ h2 ∪ h20 ∪ h21 ∪ h210 ≠ h1 ∪ ((h2 ∪ h21) ∪ h10 ∪ h20 ∪ h210) ∪ h0, h0 ⊥ h1, h0 ⊥ h210, h0 ⊥ h10, h0 ⊥ h20, h0 ⊥ h21, h0 ⊥ h2, h1 ⊥ h0, h1 ⊥ h210, h1 ⊥ h10, h1 ⊥ h20, h1 ⊥ h21, h1 ⊥ h2, h10 ⊥ h210, h10 ⊥ h2, h10 ⊥ h20, h10 ⊥ h21, h2 ⊥ h210, h2 ⊥ h10, h2 ⊥ h20, h2 ⊥ h21, h20 ⊥ h210, h20 ⊥ h10, h21 ⊥ h210, h21 ⊥ h10, h21 ⊥ h20, hP0(h0 ∪ h10 ∪ h20 ∪ h210), hP1(h1 ∪ h10 ∪ h21 ∪ h210), hP2(h2 ∪ h20 ∪ h21 ∪ h210) ⊦ h1 ⊥ (h0 ∪ h10) ∪ h2 ∪ h20 ∪ h21 ∪ h210 ∧ h1 ⊥ (h2 ∪ h21) ∪ h10 ∪ h20 ∪ h210

Rule argument

Additional information

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

Proof step 74 from proof sharing-ass-aux1 (previous step) (back to tree)

User applied rule case distinction

And closed the goal!

Rule argument

Additional information

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

Proof step 75 from proof sharing-ass-aux1 (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 76:

  (h0 ∪ h10) ∪ h2 ∪ h20 ∪ h21 ∪ h210 ≠ ((h2 ∪ h21) ∪ h10 ∪ h20 ∪ h210) ∪ h0, h0 ⊥ h1, h0 ⊥ h210, h0 ⊥ h10, h0 ⊥ h20, h0 ⊥ h21, h0 ⊥ h2, h1 ⊥ h0, h1 ⊥ h210, h1 ⊥ h10, h1 ⊥ h20, h1 ⊥ h21, h1 ⊥ h2, h10 ⊥ h210, h10 ⊥ h2, h10 ⊥ h20, h10 ⊥ h21, h2 ⊥ h210, h2 ⊥ h10, h2 ⊥ h20, h2 ⊥ h21, h20 ⊥ h210, h20 ⊥ h10, h21 ⊥ h210, h21 ⊥ h10, h21 ⊥ h20, hP0(h0 ∪ h10 ∪ h20 ∪ h210), hP1(h1 ∪ h10 ∪ h21 ∪ h210), hP2(h2 ∪ h20 ∪ h21 ∪ h210) ⊦

Rule argument

Additional information

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

Proof step 76 from proof sharing-ass-aux1 (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 77:

  ⊦ h0 ⊥ h1 → h1 ∪ h0 = h0 ∪ h1

• Proof step 78:

  (h0 ∪ h10) ∪ h2 ∪ h20 ∪ h21 ∪ h210 ≠ h0 ∪ (h2 ∪ h21) ∪ h10 ∪ h20 ∪ h210, h0 ⊥ h2, h0 ⊥ h21, h0 ⊥ h20, h0 ⊥ h10, h0 ⊥ h210, h0 ⊥ h1, h0 ⊥ (h2 ∪ h21) ∪ h10 ∪ h20 ∪ h210, h1 ⊥ h2, h1 ⊥ h21, h1 ⊥ h20, h1 ⊥ h10, h1 ⊥ h210, h1 ⊥ h0, h10 ⊥ h21, h10 ⊥ h20, h10 ⊥ h2, h10 ⊥ h210, h2 ⊥ h21, h2 ⊥ h20, h2 ⊥ h10, h2 ⊥ h210, h20 ⊥ h10, h20 ⊥ h210, h21 ⊥ h20, h21 ⊥ h10, h21 ⊥ h210, hP0(h0 ∪ h10 ∪ h20 ∪ h210), hP1(h1 ∪ h10 ∪ h21 ∪ h210), hP2(h2 ∪ h20 ∪ h21 ∪ h210) ⊦

Rule argument

Additional information

Used simplifier rules: h1 ⊥ h2 ⊦ h1 ∪ h2 ⊥ h0 ↔ h0 ⊥ h1 ∧ h0 ⊥ h2; (s) ⊦ h0 ⊥ h1 → h1 ⊥ h0; (ss) h1 ⊥ h ⊦ h0 ⊥ h1 ∪ h ↔ h0 ⊥ h1 ∧ h0 ⊥ h; (ss) h1 ⊥ h ⊦ h0 ⊥ h1 ∪ h ↔ h0 ⊥ h1 ∧ h0 ⊥ h; (ws) Used terms: (h2 ∪ h21) ∪ h10 ∪ h20 ∪ h210, h0

Proof step 77 from proof sharing-ass-aux1 (previous step) (back to tree)

A spec-lemma

Proof step 78 from proof sharing-ass-aux1 (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 79:

  (h0 ∪ h10) ∪ h2 ∪ h20 ∪ h21 ∪ h210 ≠ h0 ∪ (h2 ∪ h21) ∪ h10 ∪ h20 ∪ h210, h0 ⊥ h1, h0 ⊥ h210, h0 ⊥ h10, h0 ⊥ h20, h0 ⊥ h21, h0 ⊥ h2, h1 ⊥ h0, h1 ⊥ h210, h1 ⊥ h10, h1 ⊥ h20, h1 ⊥ h21, h1 ⊥ h2, h10 ⊥ h210, h10 ⊥ h2, h10 ⊥ h20, h10 ⊥ h21, h2 ⊥ h210, h2 ⊥ h10, h2 ⊥ h20, h2 ⊥ h21, h20 ⊥ h210, h20 ⊥ h10, h21 ⊥ h210, h21 ⊥ h10, h21 ⊥ h20, hP0(h0 ∪ h10 ∪ h20 ∪ h210), hP1(h1 ∪ h10 ∪ h21 ∪ h210), hP2(h2 ∪ h20 ∪ h21 ∪ h210) ⊦

Rule argument

Additional information

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

Proof step 79 from proof sharing-ass-aux1 (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 80:

  h0 ⊥ h1, h1 ⊥ h, h ⊥ h0 ⊦ (h0 ∪ h1) ∪ h = h0 ∪ h1 ∪ h

• Proof step 81:

  h0 ∪ h10 ∪ h2 ∪ h20 ∪ h21 ∪ h210 ≠ h0 ∪ (h2 ∪ h21) ∪ h10 ∪ h20 ∪ h210, h0 ⊥ h2, h0 ⊥ h21, h0 ⊥ h20, h0 ⊥ h210, h0 ⊥ h1, h0 ⊥ h10, h1 ⊥ h2, h1 ⊥ h21, h1 ⊥ h20, h1 ⊥ h10, h1 ⊥ h210, h1 ⊥ h0, h10 ⊥ h21, h10 ⊥ h20, h10 ⊥ h2, h10 ⊥ h210, h10 ⊥ h2 ∪ h20 ∪ h21 ∪ h210, h2 ⊥ h21, h2 ⊥ h20, h2 ⊥ h10, h2 ⊥ h210, h2 ∪ h20 ∪ h21 ∪ h210 ⊥ h0, h20 ⊥ h10, h20 ⊥ h210, h21 ⊥ h20, h21 ⊥ h10, h21 ⊥ h210, hP0(h0 ∪ h10 ∪ h20 ∪ h210), hP1(h1 ∪ h10 ∪ h21 ∪ h210), hP2(h2 ∪ h20 ∪ h21 ∪ h210) ⊦

Rule argument

Additional information

Used simplifier rules: h1 ⊥ h2 ⊦ h1 ∪ h2 ⊥ h0 ↔ h0 ⊥ h1 ∧ h0 ⊥ h2; (s) ⊦ h0 ⊥ h1 → h1 ⊥ h0; (ss) h1 ⊥ h ⊦ h0 ⊥ h1 ∪ h ↔ h0 ⊥ h1 ∧ h0 ⊥ h; (ws) Used terms: h0, h10, h2 ∪ h20 ∪ h21 ∪ h210

Proof step 80 from proof sharing-ass-aux1 (previous step) (back to tree)

A spec-lemma

Proof step 81 from proof sharing-ass-aux1 (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 82:

  h0 ∪ h10 ∪ h2 ∪ h20 ∪ h21 ∪ h210 ≠ h0 ∪ (h2 ∪ h21) ∪ h10 ∪ h20 ∪ h210, h0 ⊥ h10, h0 ⊥ h1, h0 ⊥ h210, h0 ⊥ h20, h0 ⊥ h21, h0 ⊥ h2, h1 ⊥ h0, h1 ⊥ h210, h1 ⊥ h10, h1 ⊥ h20, h1 ⊥ h21, h1 ⊥ h2, h10 ⊥ h210, h10 ⊥ h2, h10 ⊥ h20, h10 ⊥ h21, h2 ⊥ h210, h2 ⊥ h10, h2 ⊥ h20, h2 ⊥ h21, h20 ⊥ h210, h20 ⊥ h10, h21 ⊥ h210, h21 ⊥ h10, h21 ⊥ h20, hP0(h0 ∪ h10 ∪ h20 ∪ h210), hP1(h1 ∪ h10 ∪ h21 ∪ h210), hP2(h2 ∪ h20 ∪ h21 ∪ h210) ⊦

Rule argument

Additional information

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

Proof step 82 from proof sharing-ass-aux1 (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 83:

  h ⊥ h0, h ⊥ h1 ⊦ h ∪ h0 = h ∪ h1 ↔ h0 = h1

• Proof step 84:

  h10 ∪ h2 ∪ h20 ∪ h21 ∪ h210 ≠ (h2 ∪ h21) ∪ h10 ∪ h20 ∪ h210, h0 ⊥ h2, h0 ⊥ h21, h0 ⊥ h20, h0 ⊥ h210, h0 ⊥ h1, h0 ⊥ h10, h0 ⊥ h10 ∪ h2 ∪ h20 ∪ h21 ∪ h210, h0 ⊥ (h2 ∪ h21) ∪ h10 ∪ h20 ∪ h210, h1 ⊥ h2, h1 ⊥ h21, h1 ⊥ h20, h1 ⊥ h10, h1 ⊥ h210, h1 ⊥ h0, h10 ⊥ h21, h10 ⊥ h20, h10 ⊥ h2, h10 ⊥ h210, h2 ⊥ h21, h2 ⊥ h20, h2 ⊥ h10, h2 ⊥ h210, h20 ⊥ h10, h20 ⊥ h210, h21 ⊥ h20, h21 ⊥ h10, h21 ⊥ h210, hP0(h0 ∪ h10 ∪ h20 ∪ h210), hP1(h1 ∪ h10 ∪ h21 ∪ h210), hP2(h2 ∪ h20 ∪ h21 ∪ h210) ⊦

Rule argument

Additional information

Used simplifier rules: h1 ⊥ h2 ⊦ h1 ∪ h2 ⊥ h0 ↔ h0 ⊥ h1 ∧ h0 ⊥ h2; (s) ⊦ h0 ⊥ h1 → h1 ⊥ h0; (ss) h1 ⊥ h ⊦ h0 ⊥ h1 ∪ h ↔ h0 ⊥ h1 ∧ h0 ⊥ h; (ss) h1 ⊥ h ⊦ h0 ⊥ h1 ∪ h ↔ h0 ⊥ h1 ∧ h0 ⊥ h; (ws) Used terms: h0, h10 ∪ h2 ∪ h20 ∪ h21 ∪ h210, (h2 ∪ h21) ∪ h10 ∪ h20 ∪ h210

Proof step 83 from proof sharing-ass-aux1 (previous step) (back to tree)

A spec-lemma

Proof step 84 from proof sharing-ass-aux1 (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 85:

  h10 ∪ h2 ∪ h20 ∪ h21 ∪ h210 ≠ (h2 ∪ h21) ∪ h10 ∪ h20 ∪ h210, h0 ⊥ h10, h0 ⊥ h1, h0 ⊥ h210, h0 ⊥ h20, h0 ⊥ h21, h0 ⊥ h2, h1 ⊥ h0, h1 ⊥ h210, h1 ⊥ h10, h1 ⊥ h20, h1 ⊥ h21, h1 ⊥ h2, h10 ⊥ h210, h10 ⊥ h2, h10 ⊥ h20, h10 ⊥ h21, h2 ⊥ h210, h2 ⊥ h10, h2 ⊥ h20, h2 ⊥ h21, h20 ⊥ h210, h20 ⊥ h10, h21 ⊥ h210, h21 ⊥ h10, h21 ⊥ h20, hP0(h0 ∪ h10 ∪ h20 ∪ h210), hP1(h1 ∪ h10 ∪ h21 ∪ h210), hP2(h2 ∪ h20 ∪ h21 ∪ h210) ⊦

Rule argument

Additional information

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

Proof step 85 from proof sharing-ass-aux1 (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 86:

  ⊦ h0 ⊥ h1 → h1 ∪ h0 = h0 ∪ h1

• Proof step 87:

  h10 ∪ h2 ∪ h20 ∪ h21 ∪ h210 ≠ (h10 ∪ h20 ∪ h210) ∪ h2 ∪ h21, h0 ⊥ h2, h0 ⊥ h21, h0 ⊥ h20, h0 ⊥ h210, h0 ⊥ h1, h0 ⊥ h10, h1 ⊥ h2, h1 ⊥ h21, h1 ⊥ h20, h1 ⊥ h10, h1 ⊥ h210, h1 ⊥ h0, h10 ⊥ h21, h10 ⊥ h20, h10 ⊥ h2, h10 ⊥ h210, h10 ∪ h20 ∪ h210 ⊥ h2 ∪ h21, h2 ⊥ h21, h2 ⊥ h20, h2 ⊥ h10, h2 ⊥ h210, h20 ⊥ h10, h20 ⊥ h210, h21 ⊥ h20, h21 ⊥ h10, h21 ⊥ h210, hP0(h0 ∪ h10 ∪ h20 ∪ h210), hP1(h1 ∪ h10 ∪ h21 ∪ h210), hP2(h2 ∪ h20 ∪ h21 ∪ h210) ⊦

Rule argument

Additional information

Used simplifier rules: h1 ⊥ h ⊦ h0 ⊥ h1 ∪ h ↔ h0 ⊥ h1 ∧ h0 ⊥ h; (ws) ⊦ h0 ⊥ h1 → h1 ⊥ h0; (ss) h1 ⊥ h2 ⊦ h1 ∪ h2 ⊥ h0 ↔ h0 ⊥ h1 ∧ h0 ⊥ h2; (s) Used terms: h2 ∪ h21, h10 ∪ h20 ∪ h210

Proof step 86 from proof sharing-ass-aux1 (previous step) (back to tree)

A spec-lemma

Proof step 87 from proof sharing-ass-aux1 (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 88:

  h10 ∪ h2 ∪ h20 ∪ h21 ∪ h210 ≠ (h10 ∪ h20 ∪ h210) ∪ h2 ∪ h21, h0 ⊥ h10, h0 ⊥ h1, h0 ⊥ h210, h0 ⊥ h20, h0 ⊥ h21, h0 ⊥ h2, h1 ⊥ h0, h1 ⊥ h210, h1 ⊥ h10, h1 ⊥ h20, h1 ⊥ h21, h1 ⊥ h2, h10 ⊥ h210, h10 ⊥ h2, h10 ⊥ h20, h10 ⊥ h21, h2 ⊥ h210, h2 ⊥ h10, h2 ⊥ h20, h2 ⊥ h21, h20 ⊥ h210, h20 ⊥ h10, h21 ⊥ h210, h21 ⊥ h10, h21 ⊥ h20, hP0(h0 ∪ h10 ∪ h20 ∪ h210), hP1(h1 ∪ h10 ∪ h21 ∪ h210), hP2(h2 ∪ h20 ∪ h21 ∪ h210) ⊦

Rule argument

Additional information

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

Proof step 88 from proof sharing-ass-aux1 (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 89:

  h0 ⊥ h1, h1 ⊥ h, h ⊥ h0 ⊦ (h0 ∪ h1) ∪ h = h0 ∪ h1 ∪ h

• Proof step 90:

  h10 ∪ h2 ∪ h20 ∪ h21 ∪ h210 ≠ h10 ∪ (h20 ∪ h210) ∪ h2 ∪ h21, h0 ⊥ h2, h0 ⊥ h21, h0 ⊥ h20, h0 ⊥ h210, h0 ⊥ h1, h0 ⊥ h10, h1 ⊥ h2, h1 ⊥ h21, h1 ⊥ h20, h1 ⊥ h10, h1 ⊥ h210, h1 ⊥ h0, h10 ⊥ h21, h10 ⊥ h20, h10 ⊥ h2, h10 ⊥ h210, h10 ⊥ h20 ∪ h210, h2 ⊥ h21, h2 ⊥ h20, h2 ⊥ h10, h2 ⊥ h210, h2 ∪ h21 ⊥ h10, h20 ⊥ h10, h20 ⊥ h210, h20 ∪ h210 ⊥ h2 ∪ h21, h21 ⊥ h20, h21 ⊥ h10, h21 ⊥ h210, hP0(h0 ∪ h10 ∪ h20 ∪ h210), hP1(h1 ∪ h10 ∪ h21 ∪ h210), hP2(h2 ∪ h20 ∪ h21 ∪ h210) ⊦

Rule argument

Additional information

Used simplifier rules: h1 ⊥ h ⊦ h0 ⊥ h1 ∪ h ↔ h0 ⊥ h1 ∧ h0 ⊥ h; (ws) h1 ⊥ h2 ⊦ h1 ∪ h2 ⊥ h0 ↔ h0 ⊥ h1 ∧ h0 ⊥ h2; (s) ⊦ h0 ⊥ h1 → h1 ⊥ h0; (ss) Used terms: h10, h20 ∪ h210, h2 ∪ h21

Proof step 89 from proof sharing-ass-aux1 (previous step) (back to tree)

A spec-lemma

Proof step 90 from proof sharing-ass-aux1 (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 91:

  h2 ∪ h20 ∪ h21 ∪ h210 ≠ (h20 ∪ h210) ∪ h2 ∪ h21, h0 ⊥ h10, h0 ⊥ h1, h0 ⊥ h210, h0 ⊥ h20, h0 ⊥ h21, h0 ⊥ h2, h1 ⊥ h0, h1 ⊥ h210, h1 ⊥ h10, h1 ⊥ h20, h1 ⊥ h21, h1 ⊥ h2, h10 ⊥ h210, h10 ⊥ h2, h10 ⊥ h20, h10 ⊥ h21, h2 ⊥ h210, h2 ⊥ h10, h2 ⊥ h20, h2 ⊥ h21, h20 ⊥ h210, h20 ⊥ h10, h20 ⊥ h2, h20 ⊥ h21, h21 ⊥ h210, h21 ⊥ h10, h21 ⊥ h20, h210 ⊥ h2, h210 ⊥ h21, hP0(h0 ∪ h10 ∪ h20 ∪ h210), hP1(h1 ∪ h10 ∪ h21 ∪ h210), hP2(h2 ∪ h20 ∪ h21 ∪ h210) ⊦

Rule argument

Additional information

Used simplifier rules: h1 ⊥ h ⊦ h0 ⊥ h1 ∪ h ↔ h0 ⊥ h1 ∧ h0 ⊥ h; (ws) h1 ⊥ h2 ⊦ h1 ∪ h2 ⊥ h0 ↔ h0 ⊥ h1 ∧ h0 ⊥ h2; (s) h ⊥ h0, h ⊥ h1 ⊦ h ∪ h0 = h ∪ h1 ↔ h0 = h1; (s) ⊦ h0 ⊥ h1 → h1 ⊥ h0; (ss)

Proof step 91 from proof sharing-ass-aux1 (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 92:

  ⊦ h0 ⊥ h1 → h1 ∪ h0 = h0 ∪ h1

• Proof step 93:

  h2 ∪ h20 ∪ h21 ∪ h210 ≠ (h2 ∪ h21) ∪ h20 ∪ h210, h0 ⊥ h2, h0 ⊥ h21, h0 ⊥ h20, h0 ⊥ h210, h0 ⊥ h1, h0 ⊥ h10, h1 ⊥ h2, h1 ⊥ h21, h1 ⊥ h20, h1 ⊥ h10, h1 ⊥ h210, h1 ⊥ h0, h10 ⊥ h21, h10 ⊥ h20, h10 ⊥ h2, h10 ⊥ h210, h2 ⊥ h21, h2 ⊥ h20, h2 ⊥ h10, h2 ⊥ h210, h2 ∪ h21 ⊥ h20 ∪ h210, h20 ⊥ h21, h20 ⊥ h2, h20 ⊥ h10, h20 ⊥ h210, h21 ⊥ h20, h21 ⊥ h10, h21 ⊥ h210, h210 ⊥ h21, h210 ⊥ h2, hP0(h0 ∪ h10 ∪ h20 ∪ h210), hP1(h1 ∪ h10 ∪ h21 ∪ h210), hP2(h2 ∪ h20 ∪ h21 ∪ h210) ⊦

Rule argument

Additional information

Used simplifier rules: h1 ⊥ h2 ⊦ h1 ∪ h2 ⊥ h0 ↔ h0 ⊥ h1 ∧ h0 ⊥ h2; (s) ⊦ h0 ⊥ h1 → h1 ⊥ h0; (ss) Used terms: h20 ∪ h210, h2 ∪ h21

Proof step 92 from proof sharing-ass-aux1 (previous step) (back to tree)

A spec-lemma

Proof step 93 from proof sharing-ass-aux1 (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 94:

  h2 ∪ h20 ∪ h21 ∪ h210 ≠ (h2 ∪ h21) ∪ h20 ∪ h210, h0 ⊥ h10, h0 ⊥ h1, h0 ⊥ h210, h0 ⊥ h20, h0 ⊥ h21, h0 ⊥ h2, h1 ⊥ h0, h1 ⊥ h210, h1 ⊥ h10, h1 ⊥ h20, h1 ⊥ h21, h1 ⊥ h2, h10 ⊥ h210, h10 ⊥ h2, h10 ⊥ h20, h10 ⊥ h21, h2 ⊥ h210, h2 ⊥ h10, h2 ⊥ h20, h2 ⊥ h21, h20 ⊥ h210, h20 ⊥ h10, h20 ⊥ h2, h20 ⊥ h21, h21 ⊥ h210, h21 ⊥ h10, h21 ⊥ h20, h210 ⊥ h2, h210 ⊥ h21, hP0(h0 ∪ h10 ∪ h20 ∪ h210), hP1(h1 ∪ h10 ∪ h21 ∪ h210), hP2(h2 ∪ h20 ∪ h21 ∪ h210) ⊦

Rule argument

Additional information

Used simplifier rules: h1 ⊥ h2 ⊦ h1 ∪ h2 ⊥ h0 ↔ h0 ⊥ h1 ∧ h0 ⊥ h2; (s)

Proof step 94 from proof sharing-ass-aux1 (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 95:

  h0 ⊥ h1, h1 ⊥ h, h ⊥ h0 ⊦ (h0 ∪ h1) ∪ h = h0 ∪ h1 ∪ h

Rule argument

Additional information

Used simplifier rules: h1 ⊥ h ⊦ h0 ⊥ h1 ∪ h ↔ h0 ⊥ h1 ∧ h0 ⊥ h; (ws) h ⊥ h0, h ⊥ h1 ⊦ h ∪ h0 = h ∪ h1 ↔ h0 = h1; (s) ⊦ h0 ⊥ h1 → h1 ⊥ h0; (ss) h0 ⊥ h1, h1 ⊥ h, h ⊥ h0 ⊦ h ∪ h0 ∪ h1 = h0 ∪ h ∪ h1 ↔ true; (ss) h1 ⊥ h2 ⊦ h1 ∪ h2 ⊥ h0 ↔ h0 ⊥ h1 ∧ h0 ⊥ h2; (s) Used terms: h2, h21, h20 ∪ h210

Proof step 95 from proof sharing-ass-aux1 (previous step) (back to tree)

A spec-lemma

Proof step 96 from proof sharing-ass-aux1 (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 97:

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

• Proof step 98:

  h0 ⊥ h1, h0 ⊥ h2, h0 ⊥ h21, h0 ⊥ h20, h0 ⊥ h10, h0 ⊥ h210, h1 ⊥ h2, h1 ⊥ h21, h1 ⊥ h20, h1 ⊥ h10, h1 ⊥ h210, h10 ⊥ h210, h2 ⊥ h21, h2 ⊥ h20, h2 ⊥ h10, h2 ⊥ h210, h20 ⊥ h10, h20 ⊥ h210, h21 ⊥ h20, h21 ⊥ h10, h21 ⊥ h210, hP0(h0 ∪ h10 ∪ h20 ∪ h210), hP1(h1 ∪ h10 ∪ h21 ∪ h210), hP2(h2 ∪ h20 ∪ h21 ∪ h210), ∀ h0, h3, h4. ¬(h0 ⊥ h4 ∧ h0 ⊥ h3 ∧ h3 ⊥ h4 ∧ (h1 ∪ h2 ∪ h21) ∪ h10 ∪ h20 ∪ h210 = h0 ∪ h3 ∪ h4 ∧ hP1(h0 ∪ h4) ∧ hP2(h3 ∪ h4)) ⊦

Rule argument

Additional information

Used terms: hP1, hP2, (h1 ∪ h2 ∪ h21) ∪ h10 ∪ h20 ∪ h210

Proof step 97 from proof sharing-ass-aux1 (previous step) (back to tree)

Lemma sharing

Proof step 98 from proof sharing-ass-aux1 (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 99:

  h0 ⊥ h210, h0 ⊥ h10, h0 ⊥ h20, h0 ⊥ h21, h0 ⊥ h2, h0 ⊥ h1, h1 ⊥ h210, h1 ⊥ h10, h1 ⊥ h20, h1 ⊥ h21, h1 ⊥ h2, h10 ⊥ h210, h2 ⊥ h210, h2 ⊥ h10, h2 ⊥ h20, h2 ⊥ h21, h20 ⊥ h210, h20 ⊥ h10, h21 ⊥ h210, h21 ⊥ h10, h21 ⊥ h20, hP0(h0 ∪ h10 ∪ h20 ∪ h210), hP1(h1 ∪ h10 ∪ h21 ∪ h210), hP2(h2 ∪ h20 ∪ h21 ∪ h210), ∀ h, h3, h4. ¬ h ⊥ h4 ∨ ¬ h ⊥ h3 ∨ ¬ h3 ⊥ h4 ∨ (h1 ∪ h2 ∪ h21) ∪ h10 ∪ h20 ∪ h210 ≠ h ∪ h3 ∪ h4 ∨ ¬ hP1(h ∪ h4) ∨ ¬ hP2(h3 ∪ h4) ⊦

Rule argument

Additional information

Proof step 99 from proof sharing-ass-aux1 (previous step) (back to tree)

User applied rule all left

And obtained the following new goals

• Proof step 100:

  h0 ⊥ h1, h0 ⊥ h2, h0 ⊥ h21, h0 ⊥ h20, h0 ⊥ h10, h0 ⊥ h210, h1 ⊥ h2, h1 ⊥ h21, h1 ⊥ h20, h1 ⊥ h10, h1 ⊥ h210, h10 ⊥ h210, h2 ⊥ h21, h2 ⊥ h20, h2 ⊥ h10, h2 ⊥ h210, h20 ⊥ h10, h20 ⊥ h210, h21 ⊥ h20, h21 ⊥ h10, h21 ⊥ h210, hP0(h0 ∪ h10 ∪ h20 ∪ h210), hP1(h1 ∪ h10 ∪ h21 ∪ h210), hP2(h2 ∪ h20 ∪ h21 ∪ h210), ¬ h1 ∪ h10 ⊥ h21 ∪ h210 ∨ ¬ h1 ∪ h10 ⊥ h2 ∪ h20 ∨ ¬ h2 ∪ h20 ⊥ h21 ∪ h210 ∨ (h1 ∪ h2 ∪ h21) ∪ h10 ∪ h20 ∪ h210 ≠ (h1 ∪ h10) ∪ (h2 ∪ h20) ∪ h21 ∪ h210 ∨ ¬ hP1((h1 ∪ h10) ∪ h21 ∪ h210) ∨ ¬ hP2((h2 ∪ h20) ∪ h21 ∪ h210) ⊦

Rule argument

Additional information

Used terms: h1 ∪ h10, h2 ∪ h20, h21 ∪ h210

Proof step 100 from proof sharing-ass-aux1 (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 101:

  h0 ⊥ h210, h0 ⊥ h10, h0 ⊥ h20, h0 ⊥ h21, h0 ⊥ h2, h0 ⊥ h1, h1 ⊥ h210, h1 ⊥ h10, h1 ⊥ h20, h1 ⊥ h21, h1 ⊥ h2, h10 ⊥ h210, h2 ⊥ h210, h2 ⊥ h10, h2 ⊥ h20, h2 ⊥ h21, h20 ⊥ h210, h20 ⊥ h10, h21 ⊥ h210, h21 ⊥ h10, h21 ⊥ h20, hP0(h0 ∪ h10 ∪ h20 ∪ h210), hP1(h1 ∪ h10 ∪ h21 ∪ h210), hP2(h2 ∪ h20 ∪ h21 ∪ h210), (h1 ∪ h2 ∪ h21) ∪ h10 ∪ h20 ∪ h210 ≠ (h1 ∪ h10) ∪ (h2 ∪ h20) ∪ h21 ∪ h210 ∨ ¬ hP1((h1 ∪ h10) ∪ h21 ∪ h210) ∨ ¬ hP2((h2 ∪ h20) ∪ h21 ∪ h210) ⊦

Rule argument

Additional information

Used simplifier rules: ⊦ h0 ⊥ h1 → h1 ⊥ h0; (ss) h1 ⊥ h2 ⊦ h1 ∪ h2 ⊥ h0 ↔ h0 ⊥ h1 ∧ h0 ⊥ h2; (s)

Proof step 101 from proof sharing-ass-aux1 (previous step) (back to tree)

User applied rule case distinction

And obtained the following new goals

• Proof step 102:

  (h1 ∪ h2 ∪ h21) ∪ h10 ∪ h20 ∪ h210 ≠ (h1 ∪ h10) ∪ (h2 ∪ h20) ∪ h21 ∪ h210, h0 ⊥ h1, h0 ⊥ h2, h0 ⊥ h21, h0 ⊥ h20, h0 ⊥ h10, h0 ⊥ h210, h1 ⊥ h2, h1 ⊥ h21, h1 ⊥ h20, h1 ⊥ h10, h1 ⊥ h210, h10 ⊥ h210, h2 ⊥ h21, h2 ⊥ h20, h2 ⊥ h10, h2 ⊥ h210, h20 ⊥ h10, h20 ⊥ h210, h21 ⊥ h20, h21 ⊥ h10, h21 ⊥ h210, hP0(h0 ∪ h10 ∪ h20 ∪ h210), hP1(h1 ∪ h10 ∪ h21 ∪ h210), hP2(h2 ∪ h20 ∪ h21 ∪ h210) ⊦

• Proof step 130:

  h0 ⊥ h1, h0 ⊥ h2, h0 ⊥ h21, h0 ⊥ h20, h0 ⊥ h10, h0 ⊥ h210, h1 ⊥ h2, h1 ⊥ h21, h1 ⊥ h20, h1 ⊥ h10, h1 ⊥ h210, h10 ⊥ h210, h2 ⊥ h21, h2 ⊥ h20, h2 ⊥ h10, h2 ⊥ h210, h20 ⊥ h10, h20 ⊥ h210, h21 ⊥ h20, h21 ⊥ h10, h21 ⊥ h210, hP0(h0 ∪ h10 ∪ h20 ∪ h210), hP1(h1 ∪ h10 ∪ h21 ∪ h210), hP2(h2 ∪ h20 ∪ h21 ∪ h210), ¬ hP1((h1 ∪ h10) ∪ h21 ∪ h210) ⊦

• Proof step 132:

  h0 ⊥ h1, h0 ⊥ h2, h0 ⊥ h21, h0 ⊥ h20, h0 ⊥ h10, h0 ⊥ h210, h1 ⊥ h2, h1 ⊥ h21, h1 ⊥ h20, h1 ⊥ h10, h1 ⊥ h210, h10 ⊥ h210, h2 ⊥ h21, h2 ⊥ h20, h2 ⊥ h10, h2 ⊥ h210, h20 ⊥ h10, h20 ⊥ h210, h21 ⊥ h20, h21 ⊥ h10, h21 ⊥ h210, hP0(h0 ∪ h10 ∪ h20 ∪ h210), hP1(h1 ∪ h10 ∪ h21 ∪ h210), hP2(h2 ∪ h20 ∪ h21 ∪ h210), ¬ hP2((h2 ∪ h20) ∪ h21 ∪ h210) ⊦

Rule argument

Additional information

Proof step 102 from proof sharing-ass-aux1 (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 103:

  h0 ⊥ h1, h1 ⊥ h, h ⊥ h0 ⊦ (h0 ∪ h1) ∪ h = h0 ∪ h1 ∪ h

• Proof step 104:

  (h1 ∪ h2 ∪ h21) ∪ h10 ∪ h20 ∪ h210 ≠ h1 ∪ h10 ∪ (h2 ∪ h20) ∪ h21 ∪ h210, h0 ⊥ h210, h0 ⊥ h10, h0 ⊥ h20, h0 ⊥ h21, h0 ⊥ h2, h0 ⊥ h1, h1 ⊥ h210, h1 ⊥ h20, h1 ⊥ h21, h1 ⊥ h2, h1 ⊥ h10, h10 ⊥ h210, h10 ⊥ (h2 ∪ h20) ∪ h21 ∪ h210, h2 ⊥ h210, h2 ⊥ h10, h2 ⊥ h20, h2 ⊥ h21, (h2 ∪ h20) ∪ h21 ∪ h210 ⊥ h1, h20 ⊥ h210, h20 ⊥ h10, h21 ⊥ h210, h21 ⊥ h10, h21 ⊥ h20, hP0(h0 ∪ h10 ∪ h20 ∪ h210), hP1(h1 ∪ h10 ∪ h21 ∪ h210), hP2(h2 ∪ h20 ∪ h21 ∪ h210) ⊦

Rule argument

Additional information

Used simplifier rules: h1 ⊥ h2 ⊦ h1 ∪ h2 ⊥ h0 ↔ h0 ⊥ h1 ∧ h0 ⊥ h2; (s) h1 ⊥ h ⊦ h0 ⊥ h1 ∪ h ↔ h0 ⊥ h1 ∧ h0 ⊥ h; (ws) h1 ⊥ h ⊦ h0 ⊥ h1 ∪ h ↔ h0 ⊥ h1 ∧ h0 ⊥ h; (ss) ⊦ h0 ⊥ h1 → h1 ⊥ h0; (ss) Used terms: h1, h10, (h2 ∪ h20) ∪ h21 ∪ h210

Proof step 103 from proof sharing-ass-aux1 (previous step) (back to tree)

A spec-lemma

Proof step 104 from proof sharing-ass-aux1 (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 105:

  (h1 ∪ h2 ∪ h21) ∪ h10 ∪ h20 ∪ h210 ≠ h1 ∪ h10 ∪ (h2 ∪ h20) ∪ h21 ∪ h210, h0 ⊥ h1, h0 ⊥ h2, h0 ⊥ h21, h0 ⊥ h20, h0 ⊥ h10, h0 ⊥ h210, h1 ⊥ h10, h1 ⊥ h2, h1 ⊥ h21, h1 ⊥ h20, h1 ⊥ h210, h10 ⊥ h210, h10 ⊥ h2, h10 ⊥ h20, h10 ⊥ h21, h2 ⊥ h21, h2 ⊥ h20, h2 ⊥ h10, h2 ⊥ h210, h20 ⊥ h10, h20 ⊥ h210, h21 ⊥ h20, h21 ⊥ h10, h21 ⊥ h210, hP0(h0 ∪ h10 ∪ h20 ∪ h210), hP1(h1 ∪ h10 ∪ h21 ∪ h210), hP2(h2 ∪ h20 ∪ h21 ∪ h210) ⊦

Rule argument

Additional information

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

Proof step 105 from proof sharing-ass-aux1 (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 106:

  h0 ⊥ h1, h1 ⊥ h, h ⊥ h0 ⊦ (h0 ∪ h1) ∪ h = h0 ∪ h1 ∪ h

• Proof step 107:

  h1 ∪ (h2 ∪ h21) ∪ h10 ∪ h20 ∪ h210 ≠ h1 ∪ h10 ∪ (h2 ∪ h20) ∪ h21 ∪ h210, h0 ⊥ h210, h0 ⊥ h10, h0 ⊥ h20, h0 ⊥ h21, h0 ⊥ h2, h0 ⊥ h1, h1 ⊥ h210, h1 ⊥ h20, h1 ⊥ h21, h1 ⊥ h2, h1 ⊥ h10, h1 ⊥ h2 ∪ h21, h10 ⊥ h21, h10 ⊥ h20, h10 ⊥ h2, h10 ⊥ h210, h10 ∪ h20 ∪ h210 ⊥ h1, h2 ⊥ h210, h2 ⊥ h10, h2 ⊥ h20, h2 ⊥ h21, h2 ∪ h21 ⊥ h10 ∪ h20 ∪ h210, h20 ⊥ h210, h20 ⊥ h10, h21 ⊥ h210, h21 ⊥ h10, h21 ⊥ h20, hP0(h0 ∪ h10 ∪ h20 ∪ h210), hP1(h1 ∪ h10 ∪ h21 ∪ h210), hP2(h2 ∪ h20 ∪ h21 ∪ h210) ⊦

Rule argument

Additional information

Used simplifier rules: ⊦ h0 ⊥ h1 → h1 ⊥ h0; (ss) h1 ⊥ h2 ⊦ h1 ∪ h2 ⊥ h0 ↔ h0 ⊥ h1 ∧ h0 ⊥ h2; (s) h1 ⊥ h ⊦ h0 ⊥ h1 ∪ h ↔ h0 ⊥ h1 ∧ h0 ⊥ h; (ws) Used terms: h1, h2 ∪ h21, h10 ∪ h20 ∪ h210

Proof step 106 from proof sharing-ass-aux1 (previous step) (back to tree)

A spec-lemma

Proof step 107 from proof sharing-ass-aux1 (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 108:

  h1 ∪ (h2 ∪ h21) ∪ h10 ∪ h20 ∪ h210 ≠ h1 ∪ h10 ∪ (h2 ∪ h20) ∪ h21 ∪ h210, h0 ⊥ h1, h0 ⊥ h2, h0 ⊥ h21, h0 ⊥ h20, h0 ⊥ h10, h0 ⊥ h210, h1 ⊥ h10, h1 ⊥ h2, h1 ⊥ h21, h1 ⊥ h20, h1 ⊥ h210, h10 ⊥ h210, h10 ⊥ h2, h10 ⊥ h20, h10 ⊥ h21, h2 ⊥ h21, h2 ⊥ h20, h2 ⊥ h10, h2 ⊥ h210, h20 ⊥ h10, h20 ⊥ h210, h21 ⊥ h20, h21 ⊥ h10, h21 ⊥ h210, hP0(h0 ∪ h10 ∪ h20 ∪ h210), hP1(h1 ∪ h10 ∪ h21 ∪ h210), hP2(h2 ∪ h20 ∪ h21 ∪ h210) ⊦

Rule argument

Additional information

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

Proof step 108 from proof sharing-ass-aux1 (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 109:

  h ⊥ h0, h ⊥ h1 ⊦ h ∪ h0 = h ∪ h1 ↔ h0 = h1

• Proof step 110:

  h1 ∪ (h2 ∪ h21) ∪ h10 ∪ h20 ∪ h210 ≠ h1 ∪ h10 ∪ (h2 ∪ h20) ∪ h21 ∪ h210, h0 ⊥ h210, h0 ⊥ h10, h0 ⊥ h20, h0 ⊥ h21, h0 ⊥ h2, h0 ⊥ h1, h1 ⊥ h210, h1 ⊥ h20, h1 ⊥ h21, h1 ⊥ h2, h1 ⊥ h10, h10 ⊥ h21, h10 ⊥ h20, h10 ⊥ h2, h10 ⊥ h210, h2 ⊥ h210, h2 ⊥ h10, h2 ⊥ h20, h2 ⊥ h21, h20 ⊥ h210, h20 ⊥ h10, h21 ⊥ h210, h21 ⊥ h10, h21 ⊥ h20, hP0(h0 ∪ h10 ∪ h20 ∪ h210), hP1(h1 ∪ h10 ∪ h21 ∪ h210), hP2(h2 ∪ h20 ∪ h21 ∪ h210) ⊦ h1 ⊥ h10 ∪ (h2 ∪ h20) ∪ h21 ∪ h210 ∧ h1 ⊥ (h2 ∪ h21) ∪ h10 ∪ h20 ∪ h210

• Proof step 112:

  h10 ∪ (h2 ∪ h20) ∪ h21 ∪ h210 ≠ (h2 ∪ h21) ∪ h10 ∪ h20 ∪ h210, h0 ⊥ h210, h0 ⊥ h10, h0 ⊥ h20, h0 ⊥ h21, h0 ⊥ h2, h0 ⊥ h1, h1 ⊥ h210, h1 ⊥ h20, h1 ⊥ h21, h1 ⊥ h2, h1 ⊥ h10, h1 ⊥ h10 ∪ (h2 ∪ h20) ∪ h21 ∪ h210, h1 ⊥ (h2 ∪ h21) ∪ h10 ∪ h20 ∪ h210, h10 ⊥ h21, h10 ⊥ h20, h10 ⊥ h2, h10 ⊥ h210, h2 ⊥ h210, h2 ⊥ h10, h2 ⊥ h20, h2 ⊥ h21, h20 ⊥ h210, h20 ⊥ h10, h21 ⊥ h210, h21 ⊥ h10, h21 ⊥ h20, hP0(h0 ∪ h10 ∪ h20 ∪ h210), hP1(h1 ∪ h10 ∪ h21 ∪ h210), hP2(h2 ∪ h20 ∪ h21 ∪ h210) ⊦

Rule argument

Additional information

Used terms: h1, (h2 ∪ h21) ∪ h10 ∪ h20 ∪ h210, h10 ∪ (h2 ∪ h20) ∪ h21 ∪ h210

Proof step 109 from proof sharing-ass-aux1 (previous step) (back to tree)

A spec-lemma

Proof step 110 from proof sharing-ass-aux1 (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 111:

  h1 ∪ (h2 ∪ h21) ∪ h10 ∪ h20 ∪ h210 ≠ h1 ∪ h10 ∪ (h2 ∪ h20) ∪ h21 ∪ h210, h0 ⊥ h1, h0 ⊥ h2, h0 ⊥ h21, h0 ⊥ h20, h0 ⊥ h10, h0 ⊥ h210, h1 ⊥ h10, h1 ⊥ h2, h1 ⊥ h21, h1 ⊥ h20, h1 ⊥ h210, h10 ⊥ h210, h10 ⊥ h2, h10 ⊥ h20, h10 ⊥ h21, h2 ⊥ h21, h2 ⊥ h20, h2 ⊥ h10, h2 ⊥ h210, h20 ⊥ h10, h20 ⊥ h210, h21 ⊥ h20, h21 ⊥ h10, h21 ⊥ h210, hP0(h0 ∪ h10 ∪ h20 ∪ h210), hP1(h1 ∪ h10 ∪ h21 ∪ h210), hP2(h2 ∪ h20 ∪ h21 ∪ h210) ⊦ h1 ⊥ (h2 ∪ h20) ∪ h21 ∪ h210 ∧ h1 ⊥ (h2 ∪ h21) ∪ h10 ∪ h20 ∪ h210

Rule argument

Additional information

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

Proof step 111 from proof sharing-ass-aux1 (previous step) (back to tree)

User applied rule case distinction

And closed the goal!

Rule argument

Additional information

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

Proof step 112 from proof sharing-ass-aux1 (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 113:

  h10 ∪ (h2 ∪ h20) ∪ h21 ∪ h210 ≠ (h2 ∪ h21) ∪ h10 ∪ h20 ∪ h210, h0 ⊥ h1, h0 ⊥ h2, h0 ⊥ h21, h0 ⊥ h20, h0 ⊥ h10, h0 ⊥ h210, h1 ⊥ h10, h1 ⊥ h2, h1 ⊥ h21, h1 ⊥ h20, h1 ⊥ h210, h10 ⊥ h210, h10 ⊥ h2, h10 ⊥ h20, h10 ⊥ h21, h2 ⊥ h21, h2 ⊥ h20, h2 ⊥ h10, h2 ⊥ h210, h20 ⊥ h10, h20 ⊥ h210, h21 ⊥ h20, h21 ⊥ h10, h21 ⊥ h210, hP0(h0 ∪ h10 ∪ h20 ∪ h210), hP1(h1 ∪ h10 ∪ h21 ∪ h210), hP2(h2 ∪ h20 ∪ h21 ∪ h210) ⊦

Rule argument

Additional information

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

Proof step 113 from proof sharing-ass-aux1 (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 114:

  ⊦ h0 ⊥ h1 → h1 ∪ h0 = h0 ∪ h1

• Proof step 115:

  h10 ∪ (h2 ∪ h20) ∪ h21 ∪ h210 ≠ (h10 ∪ h20 ∪ h210) ∪ h2 ∪ h21, h0 ⊥ h210, h0 ⊥ h10, h0 ⊥ h20, h0 ⊥ h21, h0 ⊥ h2, h0 ⊥ h1, h1 ⊥ h210, h1 ⊥ h20, h1 ⊥ h21, h1 ⊥ h2, h1 ⊥ h10, h10 ⊥ h21, h10 ⊥ h20, h10 ⊥ h2, h10 ⊥ h210, h10 ∪ h20 ∪ h210 ⊥ h2 ∪ h21, h2 ⊥ h210, h2 ⊥ h10, h2 ⊥ h20, h2 ⊥ h21, h20 ⊥ h210, h20 ⊥ h10, h21 ⊥ h210, h21 ⊥ h10, h21 ⊥ h20, hP0(h0 ∪ h10 ∪ h20 ∪ h210), hP1(h1 ∪ h10 ∪ h21 ∪ h210), hP2(h2 ∪ h20 ∪ h21 ∪ h210) ⊦

Rule argument

Additional information

Used simplifier rules: h1 ⊥ h ⊦ h0 ⊥ h1 ∪ h ↔ h0 ⊥ h1 ∧ h0 ⊥ h; (ws) ⊦ h0 ⊥ h1 → h1 ⊥ h0; (ss) h1 ⊥ h2 ⊦ h1 ∪ h2 ⊥ h0 ↔ h0 ⊥ h1 ∧ h0 ⊥ h2; (s) Used terms: h2 ∪ h21, h10 ∪ h20 ∪ h210

Proof step 114 from proof sharing-ass-aux1 (previous step) (back to tree)

A spec-lemma

Proof step 115 from proof sharing-ass-aux1 (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 116:

  h10 ∪ (h2 ∪ h20) ∪ h21 ∪ h210 ≠ (h10 ∪ h20 ∪ h210) ∪ h2 ∪ h21, h0 ⊥ h1, h0 ⊥ h2, h0 ⊥ h21, h0 ⊥ h20, h0 ⊥ h10, h0 ⊥ h210, h1 ⊥ h10, h1 ⊥ h2, h1 ⊥ h21, h1 ⊥ h20, h1 ⊥ h210, h10 ⊥ h210, h10 ⊥ h2, h10 ⊥ h20, h10 ⊥ h21, h2 ⊥ h21, h2 ⊥ h20, h2 ⊥ h10, h2 ⊥ h210, h20 ⊥ h10, h20 ⊥ h210, h21 ⊥ h20, h21 ⊥ h10, h21 ⊥ h210, hP0(h0 ∪ h10 ∪ h20 ∪ h210), hP1(h1 ∪ h10 ∪ h21 ∪ h210), hP2(h2 ∪ h20 ∪ h21 ∪ h210) ⊦

Rule argument

Additional information

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

Proof step 116 from proof sharing-ass-aux1 (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 117:

  h0 ⊥ h1, h1 ⊥ h, h ⊥ h0 ⊦ (h0 ∪ h1) ∪ h = h0 ∪ h1 ∪ h

• Proof step 118:

  h10 ∪ (h2 ∪ h20) ∪ h21 ∪ h210 ≠ h10 ∪ (h20 ∪ h210) ∪ h2 ∪ h21, h0 ⊥ h210, h0 ⊥ h10, h0 ⊥ h20, h0 ⊥ h21, h0 ⊥ h2, h0 ⊥ h1, h1 ⊥ h210, h1 ⊥ h20, h1 ⊥ h21, h1 ⊥ h2, h1 ⊥ h10, h10 ⊥ h21, h10 ⊥ h20, h10 ⊥ h2, h10 ⊥ h210, h10 ⊥ h20 ∪ h210, h2 ⊥ h210, h2 ⊥ h10, h2 ⊥ h20, h2 ⊥ h21, h2 ∪ h21 ⊥ h10, h20 ⊥ h210, h20 ⊥ h10, h20 ∪ h210 ⊥ h2 ∪ h21, h21 ⊥ h210, h21 ⊥ h10, h21 ⊥ h20, hP0(h0 ∪ h10 ∪ h20 ∪ h210), hP1(h1 ∪ h10 ∪ h21 ∪ h210), hP2(h2 ∪ h20 ∪ h21 ∪ h210) ⊦

Rule argument

Additional information

Used simplifier rules: h1 ⊥ h ⊦ h0 ⊥ h1 ∪ h ↔ h0 ⊥ h1 ∧ h0 ⊥ h; (ws) h1 ⊥ h2 ⊦ h1 ∪ h2 ⊥ h0 ↔ h0 ⊥ h1 ∧ h0 ⊥ h2; (s) ⊦ h0 ⊥ h1 → h1 ⊥ h0; (ss) Used terms: h10, h20 ∪ h210, h2 ∪ h21

Proof step 117 from proof sharing-ass-aux1 (previous step) (back to tree)

A spec-lemma

Proof step 118 from proof sharing-ass-aux1 (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 119:

  h10 ∪ (h2 ∪ h20) ∪ h21 ∪ h210 ≠ h10 ∪ (h20 ∪ h210) ∪ h2 ∪ h21, h0 ⊥ h1, h0 ⊥ h2, h0 ⊥ h21, h0 ⊥ h20, h0 ⊥ h10, h0 ⊥ h210, h1 ⊥ h10, h1 ⊥ h2, h1 ⊥ h21, h1 ⊥ h20, h1 ⊥ h210, h10 ⊥ h210, h10 ⊥ h2, h10 ⊥ h20, h10 ⊥ h21, h2 ⊥ h21, h2 ⊥ h20, h2 ⊥ h10, h2 ⊥ h210, h20 ⊥ h10, h20 ⊥ h210, h20 ⊥ h2, h20 ⊥ h21, h21 ⊥ h20, h21 ⊥ h10, h21 ⊥ h210, h210 ⊥ h2, h210 ⊥ h21, hP0(h0 ∪ h10 ∪ h20 ∪ h210), hP1(h1 ∪ h10 ∪ h21 ∪ h210), hP2(h2 ∪ h20 ∪ h21 ∪ h210) ⊦

Rule argument

Additional information

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

Proof step 119 from proof sharing-ass-aux1 (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 120:

  h ⊥ h0, h ⊥ h1 ⊦ h ∪ h0 = h ∪ h1 ↔ h0 = h1

• Proof step 121:

  h10 ∪ (h2 ∪ h20) ∪ h21 ∪ h210 ≠ h10 ∪ (h20 ∪ h210) ∪ h2 ∪ h21, h0 ⊥ h210, h0 ⊥ h10, h0 ⊥ h20, h0 ⊥ h21, h0 ⊥ h2, h0 ⊥ h1, h1 ⊥ h210, h1 ⊥ h20, h1 ⊥ h21, h1 ⊥ h2, h1 ⊥ h10, h10 ⊥ h21, h10 ⊥ h20, h10 ⊥ h2, h10 ⊥ h210, h2 ⊥ h210, h2 ⊥ h10, h2 ⊥ h20, h2 ⊥ h21, h20 ⊥ h21, h20 ⊥ h2, h20 ⊥ h210, h20 ⊥ h10, h21 ⊥ h210, h21 ⊥ h10, h21 ⊥ h20, h210 ⊥ h21, h210 ⊥ h2, hP0(h0 ∪ h10 ∪ h20 ∪ h210), hP1(h1 ∪ h10 ∪ h21 ∪ h210), hP2(h2 ∪ h20 ∪ h21 ∪ h210) ⊦ h10 ⊥ (h20 ∪ h210) ∪ h2 ∪ h21 ∧ h10 ⊥ (h2 ∪ h20) ∪ h21 ∪ h210

• Proof step 122:

  (h20 ∪ h210) ∪ h2 ∪ h21 ≠ (h2 ∪ h20) ∪ h21 ∪ h210, h0 ⊥ h210, h0 ⊥ h10, h0 ⊥ h20, h0 ⊥ h21, h0 ⊥ h2, h0 ⊥ h1, h1 ⊥ h210, h1 ⊥ h20, h1 ⊥ h21, h1 ⊥ h2, h1 ⊥ h10, h10 ⊥ h21, h10 ⊥ h20, h10 ⊥ h2, h10 ⊥ h210, h10 ⊥ (h20 ∪ h210) ∪ h2 ∪ h21, h10 ⊥ (h2 ∪ h20) ∪ h21 ∪ h210, h2 ⊥ h210, h2 ⊥ h10, h2 ⊥ h20, h2 ⊥ h21, h20 ⊥ h21, h20 ⊥ h2, h20 ⊥ h210, h20 ⊥ h10, h21 ⊥ h210, h21 ⊥ h10, h21 ⊥ h20, h210 ⊥ h21, h210 ⊥ h2, hP0(h0 ∪ h10 ∪ h20 ∪ h210), hP1(h1 ∪ h10 ∪ h21 ∪ h210), hP2(h2 ∪ h20 ∪ h21 ∪ h210) ⊦

Rule argument

Additional information

Used terms: h10, (h2 ∪ h20) ∪ h21 ∪ h210, (h20 ∪ h210) ∪ h2 ∪ h21

Proof step 120 from proof sharing-ass-aux1 (previous step) (back to tree)

A spec-lemma

Proof step 121 from proof sharing-ass-aux1 (previous step) (back to tree)

User applied rule case distinction

And closed the goal!

Rule argument

Additional information

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

Proof step 122 from proof sharing-ass-aux1 (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 123:

  (h20 ∪ h210) ∪ h2 ∪ h21 ≠ (h2 ∪ h20) ∪ h21 ∪ h210, h0 ⊥ h1, h0 ⊥ h2, h0 ⊥ h21, h0 ⊥ h20, h0 ⊥ h10, h0 ⊥ h210, h1 ⊥ h10, h1 ⊥ h2, h1 ⊥ h21, h1 ⊥ h20, h1 ⊥ h210, h10 ⊥ h210, h10 ⊥ h2, h10 ⊥ h20, h10 ⊥ h21, h2 ⊥ h21, h2 ⊥ h20, h2 ⊥ h10, h2 ⊥ h210, h20 ⊥ h10, h20 ⊥ h210, h20 ⊥ h2, h20 ⊥ h21, h21 ⊥ h20, h21 ⊥ h10, h21 ⊥ h210, h210 ⊥ h2, h210 ⊥ h21, hP0(h0 ∪ h10 ∪ h20 ∪ h210), hP1(h1 ∪ h10 ∪ h21 ∪ h210), hP2(h2 ∪ h20 ∪ h21 ∪ h210) ⊦

Rule argument

Additional information

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

Proof step 123 from proof sharing-ass-aux1 (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 124:

  ⊦ h0 ⊥ h1 → h1 ∪ h0 = h0 ∪ h1

• Proof step 125:

  (h20 ∪ h210) ∪ h2 ∪ h21 ≠ (h20 ∪ h2) ∪ h21 ∪ h210, h0 ⊥ h210, h0 ⊥ h10, h0 ⊥ h20, h0 ⊥ h21, h0 ⊥ h2, h0 ⊥ h1, h1 ⊥ h210, h1 ⊥ h20, h1 ⊥ h21, h1 ⊥ h2, h1 ⊥ h10, h10 ⊥ h21, h10 ⊥ h20, h10 ⊥ h2, h10 ⊥ h210, h2 ⊥ h210, h2 ⊥ h10, h2 ⊥ h20, h2 ⊥ h21, h20 ⊥ h21, h20 ⊥ h210, h20 ⊥ h10, h20 ⊥ h2, h21 ⊥ h210, h21 ⊥ h10, h21 ⊥ h20, h210 ⊥ h21, h210 ⊥ h2, hP0(h0 ∪ h10 ∪ h20 ∪ h210), hP1(h1 ∪ h10 ∪ h21 ∪ h210), hP2(h2 ∪ h20 ∪ h21 ∪ h210) ⊦

Rule argument

Additional information

Used terms: h2, h20

Proof step 124 from proof sharing-ass-aux1 (previous step) (back to tree)

A spec-lemma

Proof step 125 from proof sharing-ass-aux1 (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 126:

  h0 ⊥ h1, h1 ⊥ h, h ⊥ h0 ⊦ (h0 ∪ h1) ∪ h = h0 ∪ h1 ∪ h

• Proof step 127:

  (h20 ∪ h210) ∪ h2 ∪ h21 ≠ h20 ∪ h2 ∪ h21 ∪ h210, h0 ⊥ h1, h0 ⊥ h2, h0 ⊥ h21, h0 ⊥ h20, h0 ⊥ h10, h0 ⊥ h210, h1 ⊥ h10, h1 ⊥ h2, h1 ⊥ h21, h1 ⊥ h20, h1 ⊥ h210, h10 ⊥ h210, h10 ⊥ h2, h10 ⊥ h20, h10 ⊥ h21, h2 ⊥ h21, h2 ⊥ h20, h2 ⊥ h10, h2 ⊥ h210, h2 ⊥ h21 ∪ h210, h20 ⊥ h10, h20 ⊥ h210, h20 ⊥ h21, h20 ⊥ h2, h21 ⊥ h20, h21 ⊥ h10, h21 ⊥ h210, h21 ∪ h210 ⊥ h20, h210 ⊥ h2, h210 ⊥ h21, hP0(h0 ∪ h10 ∪ h20 ∪ h210), hP1(h1 ∪ h10 ∪ h21 ∪ h210), hP2(h2 ∪ h20 ∪ h21 ∪ h210) ⊦

Rule argument

Additional information

Used simplifier rules: h1 ⊥ h ⊦ h0 ⊥ h1 ∪ h ↔ h0 ⊥ h1 ∧ h0 ⊥ h; (ws) h1 ⊥ h2 ⊦ h1 ∪ h2 ⊥ h0 ↔ h0 ⊥ h1 ∧ h0 ⊥ h2; (s) ⊦ h0 ⊥ h1 → h1 ⊥ h0; (ss) Used terms: h20, h2, h21 ∪ h210

Proof step 126 from proof sharing-ass-aux1 (previous step) (back to tree)

A spec-lemma

Proof step 127 from proof sharing-ass-aux1 (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 128:

  (h20 ∪ h210) ∪ h2 ∪ h21 ≠ h20 ∪ h2 ∪ h21 ∪ h210, h0 ⊥ h210, h0 ⊥ h10, h0 ⊥ h20, h0 ⊥ h21, h0 ⊥ h2, h0 ⊥ h1, h1 ⊥ h210, h1 ⊥ h20, h1 ⊥ h21, h1 ⊥ h2, h1 ⊥ h10, h10 ⊥ h21, h10 ⊥ h20, h10 ⊥ h2, h10 ⊥ h210, h2 ⊥ h210, h2 ⊥ h10, h2 ⊥ h20, h2 ⊥ h21, h20 ⊥ h2, h20 ⊥ h21, h20 ⊥ h210, h20 ⊥ h10, h21 ⊥ h210, h21 ⊥ h10, h21 ⊥ h20, h210 ⊥ h21, h210 ⊥ h2, hP0(h0 ∪ h10 ∪ h20 ∪ h210), hP1(h1 ∪ h10 ∪ h21 ∪ h210), hP2(h2 ∪ h20 ∪ h21 ∪ h210) ⊦

Rule argument

Additional information

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

Proof step 128 from proof sharing-ass-aux1 (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 129:

  h0 ⊥ h1, h1 ⊥ h, h ⊥ h0 ⊦ (h0 ∪ h1) ∪ h = h0 ∪ h1 ∪ h

Rule argument

Additional information

Used simplifier rules: h1 ⊥ h ⊦ h0 ⊥ h1 ∪ h ↔ h0 ⊥ h1 ∧ h0 ⊥ h; (ws) h ⊥ h0, h ⊥ h1 ⊦ h ∪ h0 = h ∪ h1 ↔ h0 = h1; (s) ⊦ h0 ⊥ h1 → h1 ⊥ h0; (ss) h0 ⊥ h1, h1 ⊥ h, h ⊥ h0 ⊦ h ∪ h0 ∪ h1 = h0 ∪ h1 ∪ h ↔ true; (ss) h1 ⊥ h2 ⊦ h1 ∪ h2 ⊥ h0 ↔ h0 ⊥ h1 ∧ h0 ⊥ h2; (s) Used terms: h20, h210, h2 ∪ h21

Proof step 129 from proof sharing-ass-aux1 (previous step) (back to tree)

A spec-lemma

Proof step 130 from proof sharing-ass-aux1 (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 131:

  h0 ⊥ h1, h1 ⊥ h, h ⊥ h0 ⊦ (h0 ∪ h1) ∪ h = h0 ∪ h1 ∪ h

Rule argument

Additional information

Used simplifier rules: h1 ⊥ h ⊦ h0 ⊥ h1 ∪ h ↔ h0 ⊥ h1 ∧ h0 ⊥ h; (ws) ⊦ h0 ⊥ h1 → h1 ⊥ h0; (ss) h1 ⊥ h2 ⊦ h1 ∪ h2 ⊥ h0 ↔ h0 ⊥ h1 ∧ h0 ⊥ h2; (s) Used terms: h1, h10, h21 ∪ h210

Proof step 131 from proof sharing-ass-aux1 (previous step) (back to tree)

A spec-lemma

Proof step 132 from proof sharing-ass-aux1 (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 133:

  h0 ⊥ h1, h1 ⊥ h, h ⊥ h0 ⊦ (h0 ∪ h1) ∪ h = h0 ∪ h1 ∪ h

Rule argument

Additional information

Used simplifier rules: h1 ⊥ h ⊦ h0 ⊥ h1 ∪ h ↔ h0 ⊥ h1 ∧ h0 ⊥ h; (ws) ⊦ h0 ⊥ h1 → h1 ⊥ h0; (ss) h1 ⊥ h2 ⊦ h1 ∪ h2 ⊥ h0 ↔ h0 ⊥ h1 ∧ h0 ⊥ h2; (s) Used terms: h2, h20, h21 ∪ h210

Proof step 133 from proof sharing-ass-aux1 (previous step) (back to tree)

A spec-lemma