Proof step 1 from proof sharing-ass-aux2 (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 ⊗ hP1)(h0 ∪ h2) ∧ 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-aux2 (previous step) (back to tree)

Lemma sharing

Proof step 3 from proof sharing-ass-aux2 (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 ⊗ hP1)(h0 ∪ h2) ∧ 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 49:

  ∃ 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 ⊗ hP1)(h0 ∪ h2) ∧ hP2(h1 ∪ h2)

Rule argument

Additional information

Proof step 4 from proof sharing-ass-aux2 (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 ⊗ hP1)(h0 ∪ h2), 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-aux2 (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, hP2(h1 ∪ h2), ∃ h1, h3, h4. h1 ⊥ h4 ∧ h1 ⊥ h3 ∧ h3 ⊥ h4 ∧ h0 ∪ h2 = h1 ∪ h3 ∪ h4 ∧ hP0(h1 ∪ h4) ∧ hP1(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: hP0, hP1, h0 ∪ h2

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

Lemma sharing

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

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 8:

  h0 ∪ h2 = h ∪ h3 ∪ h4, h ⊥ h4, h ⊥ h3, h0 ⊥ h2, h0 ⊥ h1, h1 ⊥ h2, h3 ⊥ h4, hP0(h ∪ h4), hP1(h3 ∪ h4), 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 8 from proof sharing-ass-aux2 (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(h ∪ h4), hP1(h3 ∪ h4), hP2(h1 ∪ h2), ∃ h20, h21, h30, h31, h40, h41. h = h20 ∪ h21 ∧ h3 = h30 ∪ h31 ∧ h4 = h40 ∪ h41 ∧ h0 = h20 ∪ h30 ∪ h40 ∧ h2 = h21 ∪ h31 ∪ h41 ∧ h20 ⊥ h21 ∧ h30 ⊥ h31 ∧ h40 ⊥ h41 ∧ h20 ⊥ h2 ∧ h30 ⊥ h2 ∧ h40 ⊥ h2 ∧ h21 ⊥ h0 ∧ h31 ⊥ h0 ∧ h41 ⊥ h0 ⊦ ∃ 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: h0, h2, h4, h3, h

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

A spec-lemma

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

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 11:

  h1 ⊥ h21, h1 ⊥ h31, h1 ⊥ h41, h1 ⊥ h20, h1 ⊥ h30, h1 ⊥ 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((h20 ∪ h21) ∪ h40 ∪ h41), hP1((h30 ∪ h31) ∪ h40 ∪ h41), hP2(h1 ∪ h21 ∪ h31 ∪ h41) ⊦ ∃ h3, h4, h5, h, h0, h10, h210. (h20 ∪ h30 ∪ h40) ∪ h1 ∪ h21 ∪ h31 ∪ h41 = (h4 ∪ h3 ∪ h10) ∪ h5 ∪ h0 ∪ h ∪ h210 ∧ h3 ⊥ h4 ∧ h3 ⊥ h5 ∧ h3 ⊥ h ∧ h3 ⊥ h0 ∧ h3 ⊥ h10 ∧ h3 ⊥ h210 ∧ h4 ⊥ h5 ∧ h4 ⊥ h ∧ h4 ⊥ h0 ∧ h4 ⊥ h10 ∧ h4 ⊥ h210 ∧ h5 ⊥ h ∧ h5 ⊥ h0 ∧ h5 ⊥ h10 ∧ h5 ⊥ h210 ∧ h ⊥ h0 ∧ h ⊥ h10 ∧ h ⊥ h210 ∧ h0 ⊥ h10 ∧ h0 ⊥ h210 ∧ h10 ⊥ h210 ∧ hP0(h3 ∪ h10 ∪ h0 ∪ h210) ∧ hP1(h4 ∪ h10 ∪ h ∪ h210) ∧ hP2(h5 ∪ h0 ∪ 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-aux2 (previous step) (back to tree)

User applied rule exists right

And obtained the following new goals

• Proof step 12:

  h1 ⊥ h40, h1 ⊥ h30, h1 ⊥ h20, h1 ⊥ h41, h1 ⊥ h31, h1 ⊥ 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((h20 ∪ h21) ∪ h40 ∪ h41), hP1((h30 ∪ h31) ∪ h40 ∪ h41), hP2(h1 ∪ h21 ∪ h31 ∪ h41) ⊦ (h20 ∪ h30 ∪ h40) ∪ h1 ∪ h21 ∪ h31 ∪ h41 = (h30 ∪ h20 ∪ h40) ∪ h1 ∪ h21 ∪ h31 ∪ h41 ∧ h20 ⊥ h30 ∧ h20 ⊥ h1 ∧ h20 ⊥ h31 ∧ h20 ⊥ h21 ∧ h20 ⊥ h40 ∧ h20 ⊥ h41 ∧ h30 ⊥ h1 ∧ h30 ⊥ h31 ∧ h30 ⊥ h21 ∧ h30 ⊥ h40 ∧ h30 ⊥ h41 ∧ h1 ⊥ h31 ∧ h1 ⊥ h21 ∧ h1 ⊥ h40 ∧ h1 ⊥ h41 ∧ h31 ⊥ h21 ∧ h31 ⊥ h40 ∧ h31 ⊥ h41 ∧ h21 ⊥ h40 ∧ h21 ⊥ h41 ∧ h40 ⊥ h41 ∧ hP0(h20 ∪ h40 ∪ h21 ∪ h41) ∧ hP1(h30 ∪ h40 ∪ h31 ∪ h41) ∧ hP2(h1 ∪ h21 ∪ h31 ∪ h41)

Rule argument

Additional information

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

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

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 13:

  h1 ⊥ h21, h1 ⊥ h31, h1 ⊥ h41, h1 ⊥ h20, h1 ⊥ h30, h1 ⊥ 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((h20 ∪ h21) ∪ h40 ∪ h41), hP1((h30 ∪ h31) ∪ h40 ∪ h41), hP2(h1 ∪ h21 ∪ h31 ∪ h41) ⊦ (h20 ∪ h30 ∪ h40) ∪ h1 ∪ h21 ∪ h31 ∪ h41 = (h30 ∪ h20 ∪ h40) ∪ h1 ∪ h21 ∪ h31 ∪ h41 ∧ hP0(h20 ∪ h40 ∪ h21 ∪ h41) ∧ hP1(h30 ∪ h40 ∪ h31 ∪ h41)

Rule argument

Additional information

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

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

User applied rule case distinction

And obtained the following new goals

• Proof step 14:

  (h20 ∪ h30 ∪ h40) ∪ h1 ∪ h21 ∪ h31 ∪ h41 ≠ (h30 ∪ h20 ∪ h40) ∪ h1 ∪ h21 ∪ h31 ∪ h41, h1 ⊥ h40, h1 ⊥ h30, h1 ⊥ h20, h1 ⊥ h41, h1 ⊥ h31, h1 ⊥ 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((h20 ∪ h21) ∪ h40 ∪ h41), hP1((h30 ∪ h31) ∪ h40 ∪ h41), hP2(h1 ∪ h21 ∪ h31 ∪ h41) ⊦

• Proof step 32:

  h1 ⊥ h40, h1 ⊥ h30, h1 ⊥ h20, h1 ⊥ h41, h1 ⊥ h31, h1 ⊥ 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((h20 ∪ h21) ∪ h40 ∪ h41), hP1((h30 ∪ h31) ∪ h40 ∪ h41), hP2(h1 ∪ h21 ∪ h31 ∪ h41), ¬ hP0(h20 ∪ h40 ∪ h21 ∪ h41) ⊦

• Proof step 41:

  h1 ⊥ h40, h1 ⊥ h30, h1 ⊥ h20, h1 ⊥ h41, h1 ⊥ h31, h1 ⊥ 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((h20 ∪ h21) ∪ h40 ∪ h41), hP1((h30 ∪ h31) ∪ h40 ∪ h41), hP2(h1 ∪ h21 ∪ h31 ∪ h41), ¬ hP1(h30 ∪ h40 ∪ h31 ∪ h41) ⊦

Rule argument

Additional information

Proof step 14 from proof sharing-ass-aux2 (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) ∪ h1 ∪ h21 ∪ h31 ∪ h41 ≠ ((h20 ∪ h40) ∪ h30) ∪ h1 ∪ h21 ∪ h31 ∪ h41, h1 ⊥ h21, h1 ⊥ h31, h1 ⊥ h41, h1 ⊥ h20, h1 ⊥ h30, h1 ⊥ h40, h20 ⊥ h40, h20 ⊥ h41, h20 ⊥ h30, h20 ⊥ h31, h20 ⊥ h21, h20 ∪ h40 ⊥ h30, 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((h20 ∪ h21) ∪ h40 ∪ h41), hP1((h30 ∪ h31) ∪ h40 ∪ h41), hP2(h1 ∪ h21 ∪ h31 ∪ 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: h30, h20 ∪ h40

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

A spec-lemma

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

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 17:

  (h20 ∪ h30 ∪ h40) ∪ h1 ∪ h21 ∪ h31 ∪ h41 ≠ ((h20 ∪ h40) ∪ h30) ∪ h1 ∪ h21 ∪ h31 ∪ h41, h1 ⊥ h40, h1 ⊥ h30, h1 ⊥ h20, h1 ⊥ h41, h1 ⊥ h31, h1 ⊥ 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, h30 ⊥ h20, h31 ⊥ h41, h31 ⊥ h40, h31 ⊥ h30, h31 ⊥ h20, h40 ⊥ h31, h40 ⊥ h21, h40 ⊥ h41, h41 ⊥ h40, h41 ⊥ h30, h41 ⊥ h20, hP0((h20 ∪ h21) ∪ h40 ∪ h41), hP1((h30 ∪ h31) ∪ h40 ∪ h41), hP2(h1 ∪ h21 ∪ h31 ∪ h41) ⊦

Rule argument

Additional information

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

Proof step 17 from proof sharing-ass-aux2 (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) ∪ h1 ∪ h21 ∪ h31 ∪ h41 ≠ (h20 ∪ h40 ∪ h30) ∪ h1 ∪ h21 ∪ h31 ∪ h41, h1 ⊥ h21, h1 ⊥ h31, h1 ⊥ h41, h1 ⊥ h20, h1 ⊥ h30, h1 ⊥ h40, h20 ⊥ h41, h20 ⊥ h30, h20 ⊥ h31, h20 ⊥ h21, h20 ⊥ h40, h21 ⊥ h41, h21 ⊥ h31, h21 ⊥ h20, h21 ⊥ h30, h21 ⊥ h40, h30 ⊥ h31, h30 ⊥ h21, h30 ⊥ h40, h30 ⊥ h41, h30 ⊥ h20, h31 ⊥ h20, h31 ⊥ h30, h31 ⊥ h40, h31 ⊥ h41, h40 ⊥ h41, h40 ⊥ h21, h40 ⊥ h31, h40 ⊥ h30, h41 ⊥ h20, h41 ⊥ h30, h41 ⊥ h40, hP0((h20 ∪ h21) ∪ h40 ∪ h41), hP1((h30 ∪ h31) ∪ h40 ∪ h41), hP2(h1 ∪ h21 ∪ h31 ∪ h41) ⊦

Rule argument

Additional information

Used simplifier rules: ⊦ h0 ⊥ h1 → h1 ⊥ h0; (ss) Used terms: h20, h40, h30

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

A spec-lemma

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

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 20:

  ⊦ h0 ⊥ h1 ∧ h1 ⊥ h ∧ h ⊥ h0 → (h0 ∪ h1) ∪ h = h0 ∪ h1 ∪ h

• Proof step 21:

  (h20 ∪ h30 ∪ h40) ∪ h1 ∪ h21 ∪ h31 ∪ h41 ≠ h20 ∪ (h40 ∪ h30) ∪ h1 ∪ h21 ∪ h31 ∪ h41, h1 ⊥ h40, h1 ⊥ h30, h1 ⊥ h20, h1 ⊥ h41, h1 ⊥ h31, h1 ⊥ h21, h1 ∪ h21 ∪ h31 ∪ h41 ⊥ h20, h20 ⊥ h40, h20 ⊥ h21, h20 ⊥ h31, h20 ⊥ h30, h20 ⊥ h41, h20 ⊥ h40 ∪ h30, h21 ⊥ h40, h21 ⊥ h30, h21 ⊥ h20, h21 ⊥ h31, h21 ⊥ h41, h30 ⊥ h20, h30 ⊥ h41, h30 ⊥ h40, h30 ⊥ h21, h30 ⊥ h31, h31 ⊥ h41, h31 ⊥ h40, h31 ⊥ h30, h31 ⊥ h20, h40 ⊥ h30, h40 ⊥ h31, h40 ⊥ h21, h40 ⊥ h41, h40 ∪ h30 ⊥ h1 ∪ h21 ∪ h31 ∪ h41, h41 ⊥ h40, h41 ⊥ h30, h41 ⊥ h20, hP0((h20 ∪ h21) ∪ h40 ∪ h41), hP1((h30 ∪ h31) ∪ h40 ∪ h41), hP2(h1 ∪ h21 ∪ h31 ∪ 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, h40 ∪ h30, h1 ∪ h21 ∪ h31 ∪ h41

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

A spec-lemma

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

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 22:

  (h20 ∪ h30 ∪ h40) ∪ h1 ∪ h21 ∪ h31 ∪ h41 ≠ h20 ∪ (h40 ∪ h30) ∪ h1 ∪ h21 ∪ h31 ∪ h41, h1 ⊥ h21, h1 ⊥ h31, h1 ⊥ h41, h1 ⊥ h20, h1 ⊥ h30, h1 ⊥ h40, h20 ⊥ h41, h20 ⊥ h30, h20 ⊥ h31, h20 ⊥ h21, h20 ⊥ h40, h20 ⊥ h1, h21 ⊥ h41, h21 ⊥ h31, h21 ⊥ h20, h21 ⊥ h30, h21 ⊥ h40, h30 ⊥ h1, h30 ⊥ h31, h30 ⊥ h21, h30 ⊥ h40, h30 ⊥ h41, h30 ⊥ h20, h31 ⊥ h20, h31 ⊥ h30, h31 ⊥ h40, h31 ⊥ h41, h40 ⊥ h1, h40 ⊥ h41, h40 ⊥ h21, h40 ⊥ h31, h40 ⊥ h30, h41 ⊥ h20, h41 ⊥ h30, h41 ⊥ h40, hP0((h20 ∪ h21) ∪ h40 ∪ h41), hP1((h30 ∪ h31) ∪ h40 ∪ h41), hP2(h1 ∪ 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 22 from proof sharing-ass-aux2 (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 23:

  ⊦ h0 ⊥ h1 ∧ h1 ⊥ h ∧ h ⊥ h0 → (h0 ∪ h1) ∪ h = h0 ∪ h1 ∪ h

• Proof step 24:

  h20 ∪ (h30 ∪ h40) ∪ h1 ∪ h21 ∪ h31 ∪ h41 ≠ h20 ∪ (h40 ∪ h30) ∪ h1 ∪ h21 ∪ h31 ∪ h41, h1 ⊥ h40, h1 ⊥ h30, h1 ⊥ h20, h1 ⊥ h41, h1 ⊥ h31, h1 ⊥ h21, h1 ∪ h21 ∪ h31 ∪ h41 ⊥ h20, h20 ⊥ h1, h20 ⊥ h40, h20 ⊥ h21, h20 ⊥ h31, h20 ⊥ h30, h20 ⊥ h41, h20 ⊥ h30 ∪ h40, h21 ⊥ h40, h21 ⊥ h30, h21 ⊥ h20, h21 ⊥ h31, h21 ⊥ h41, h30 ⊥ h20, h30 ⊥ h41, h30 ⊥ h40, h30 ⊥ h21, h30 ⊥ h31, h30 ⊥ h1, h30 ∪ h40 ⊥ h1 ∪ h21 ∪ h31 ∪ h41, h31 ⊥ h41, h31 ⊥ h40, h31 ⊥ h30, h31 ⊥ h20, h40 ⊥ h30, h40 ⊥ h31, h40 ⊥ h21, h40 ⊥ h41, h40 ⊥ h1, h41 ⊥ h40, h41 ⊥ h30, h41 ⊥ h20, hP0((h20 ∪ h21) ∪ h40 ∪ h41), hP1((h30 ∪ h31) ∪ h40 ∪ h41), hP2(h1 ∪ h21 ∪ h31 ∪ 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, h1 ∪ h21 ∪ h31 ∪ h41

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

A spec-lemma

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

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 25:

  h20 ∪ (h30 ∪ h40) ∪ h1 ∪ h21 ∪ h31 ∪ h41 ≠ h20 ∪ (h40 ∪ h30) ∪ h1 ∪ h21 ∪ h31 ∪ h41, h1 ⊥ h21, h1 ⊥ h31, h1 ⊥ h41, h1 ⊥ h20, h1 ⊥ h30, h1 ⊥ h40, h20 ⊥ h41, h20 ⊥ h30, h20 ⊥ h31, h20 ⊥ h21, h20 ⊥ h40, h20 ⊥ h1, h21 ⊥ h41, h21 ⊥ h31, h21 ⊥ h20, h21 ⊥ h30, h21 ⊥ h40, h30 ⊥ h1, h30 ⊥ h31, h30 ⊥ h21, h30 ⊥ h40, h30 ⊥ h41, h30 ⊥ h20, h31 ⊥ h20, h31 ⊥ h30, h31 ⊥ h40, h31 ⊥ h41, h40 ⊥ h1, h40 ⊥ h41, h40 ⊥ h21, h40 ⊥ h31, h40 ⊥ h30, h41 ⊥ h20, h41 ⊥ h30, h41 ⊥ h40, hP0((h20 ∪ h21) ∪ h40 ∪ h41), hP1((h30 ∪ h31) ∪ h40 ∪ h41), hP2(h1 ∪ 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 25 from proof sharing-ass-aux2 (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 26:

  ⊦ h ⊥ h0 ∧ h ⊥ h1 → (h ∪ h0 = h ∪ h1 ↔ h0 = h1)

• Proof step 27:

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

• Proof step 29:

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

Rule argument

Additional information

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

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

A spec-lemma

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

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 28:

  h1 ⊥ h ⊦ h0 ⊥ h1 ∪ h ↔ h0 ⊥ h1 ∧ h0 ⊥ h

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, h40 ∪ h30, h1 ∪ h21 ∪ h31 ∪ h41

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

A spec-lemma

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

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 30:

  (h40 ∪ h30) ∪ h1 ∪ h21 ∪ h31 ∪ h41 ≠ (h30 ∪ h40) ∪ h1 ∪ h21 ∪ h31 ∪ h41, h1 ⊥ h21, h1 ⊥ h31, h1 ⊥ h41, h1 ⊥ h20, h1 ⊥ h30, h1 ⊥ h40, h20 ⊥ h41, h20 ⊥ h30, h20 ⊥ h31, h20 ⊥ h21, h20 ⊥ h40, h20 ⊥ h1, h21 ⊥ h41, h21 ⊥ h31, h21 ⊥ h20, h21 ⊥ h30, h21 ⊥ h40, h30 ⊥ h1, h30 ⊥ h31, h30 ⊥ h21, h30 ⊥ h40, h30 ⊥ h41, h30 ⊥ h20, h31 ⊥ h20, h31 ⊥ h30, h31 ⊥ h40, h31 ⊥ h41, h40 ⊥ h1, h40 ⊥ h41, h40 ⊥ h21, h40 ⊥ h31, h40 ⊥ h30, h41 ⊥ h20, h41 ⊥ h30, h41 ⊥ h40, hP0((h20 ∪ h21) ∪ h40 ∪ h41), hP1((h30 ∪ h31) ∪ h40 ∪ h41), hP2(h1 ∪ h21 ∪ h31 ∪ 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 30 from proof sharing-ass-aux2 (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 31:

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

Rule argument

Additional information

Used terms: h30, h40

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

A spec-lemma

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

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 33:

  ⊦ h0 ⊥ h1 ∧ h1 ⊥ h ∧ h ⊥ h0 → (h0 ∪ h1) ∪ h = h0 ∪ h1 ∪ h

• Proof step 34:

  h1 ⊥ h21, h1 ⊥ h31, h1 ⊥ h41, h1 ⊥ h20, h1 ⊥ h30, h1 ⊥ h40, h20 ⊥ h40, h20 ⊥ h41, h20 ⊥ h30, h20 ⊥ h31, h20 ⊥ h21, h21 ⊥ h41, h21 ⊥ h31, h21 ⊥ h20, h21 ⊥ h30, h21 ⊥ h40, h21 ⊥ h40 ∪ h41, h30 ⊥ h31, h30 ⊥ h21, h30 ⊥ h40, h30 ⊥ h41, h31 ⊥ h20, h31 ⊥ h30, h31 ⊥ h40, h31 ⊥ h41, h40 ⊥ h41, h40 ⊥ h21, h40 ⊥ h31, h40 ∪ h41 ⊥ h20, h41 ⊥ h20, h41 ⊥ h30, h41 ⊥ h40, hP0(h20 ∪ h21 ∪ h40 ∪ h41), hP1((h30 ∪ h31) ∪ h40 ∪ h41), hP2(h1 ∪ h21 ∪ h31 ∪ h41), ¬ hP0(h20 ∪ h40 ∪ h21 ∪ 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: h20, h21, h40 ∪ h41

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

A spec-lemma

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

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 35:

  h1 ⊥ h40, h1 ⊥ h30, h1 ⊥ h20, h1 ⊥ h41, h1 ⊥ h31, h1 ⊥ 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(h20 ∪ h21 ∪ h40 ∪ h41), hP1((h30 ∪ h31) ∪ h40 ∪ h41), hP2(h1 ∪ h21 ∪ h31 ∪ h41), ¬ hP0(h20 ∪ h40 ∪ h21 ∪ 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 35 from proof sharing-ass-aux2 (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 36:

  ⊦ h0 ⊥ h1 ∧ h1 ⊥ h ∧ h ⊥ h0 → (h0 ∪ h1) ∪ h = h0 ∪ h1 ∪ h

• Proof step 37:

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

Rule argument

Additional information

Used simplifier rules: ⊦ h0 ⊥ h1 → h1 ⊥ h0; (ss) Used terms: h40, h21, h41

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

A spec-lemma

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

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 38:

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

• Proof step 39:

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

Rule argument

Additional information

Used terms: h40, h21

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

A spec-lemma

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

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 40:

  ⊦ h0 ⊥ h1 ∧ h1 ⊥ h ∧ h ⊥ h0 → (h0 ∪ h1) ∪ h = h0 ∪ h1 ∪ h

Rule argument

Additional information

Used simplifier rules: ⊦ h0 ⊥ h1 → h1 ⊥ h0; (ss) Used terms: h21, h40, h41

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

A spec-lemma

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

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 42:

  ⊦ h0 ⊥ h1 ∧ h1 ⊥ h ∧ h ⊥ h0 → (h0 ∪ h1) ∪ h = h0 ∪ h1 ∪ h

• Proof step 43:

  h1 ⊥ h21, h1 ⊥ h31, h1 ⊥ h41, h1 ⊥ h20, h1 ⊥ h30, h1 ⊥ 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((h20 ∪ h21) ∪ h40 ∪ h41), hP1((h30 ∪ h31) ∪ h40 ∪ h41), hP2(h1 ∪ h21 ∪ h31 ∪ h41), ¬ hP1(h30 ∪ (h40 ∪ h31) ∪ h41) ⊦

Rule argument

Additional information

Used simplifier rules: ⊦ h0 ⊥ h1 → h1 ⊥ h0; (ss) Used terms: h40, h31, h41

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

A spec-lemma

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

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 44:

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

• Proof step 45:

  h1 ⊥ h40, h1 ⊥ h30, h1 ⊥ h20, h1 ⊥ h41, h1 ⊥ h31, h1 ⊥ 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 ⊥ h30, h31 ⊥ h20, h31 ⊥ h40, h40 ⊥ h31, h40 ⊥ h21, h40 ⊥ h41, h41 ⊥ h40, h41 ⊥ h30, h41 ⊥ h20, hP0((h20 ∪ h21) ∪ h40 ∪ h41), hP1((h30 ∪ h31) ∪ h40 ∪ h41), hP2(h1 ∪ h21 ∪ h31 ∪ h41), ¬ hP1(h30 ∪ (h31 ∪ h40) ∪ h41) ⊦

Rule argument

Additional information

Used terms: h40, h31

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

A spec-lemma

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

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 46:

  ⊦ h0 ⊥ h1 ∧ h1 ⊥ h ∧ h ⊥ h0 → (h0 ∪ h1) ∪ h = h0 ∪ h1 ∪ h

• Proof step 47:

  h1 ⊥ h21, h1 ⊥ h31, h1 ⊥ h41, h1 ⊥ h20, h1 ⊥ h30, h1 ⊥ 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 ⊥ h41, h31 ⊥ h40, h40 ⊥ h21, h40 ⊥ h31, h40 ⊥ h41, h41 ⊥ h20, h41 ⊥ h30, h41 ⊥ h40, h41 ⊥ h31, hP0((h20 ∪ h21) ∪ h40 ∪ h41), hP1((h30 ∪ h31) ∪ h40 ∪ h41), hP2(h1 ∪ h21 ∪ h31 ∪ h41), ¬ hP1(h30 ∪ h31 ∪ h40 ∪ h41) ⊦

Rule argument

Additional information

Used simplifier rules: ⊦ h0 ⊥ h1 → h1 ⊥ h0; (ss) Used terms: h31, h40, h41

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

A spec-lemma

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

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 48:

  ⊦ 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 48 from proof sharing-ass-aux2 (previous step) (back to tree)

A spec-lemma

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

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 50:

  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 ⊗ hP1)(h3 ∪ h5) ∧ hP2(h4 ∪ h5)

Rule argument

Additional information

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

User applied rule exists right

And obtained the following new goals

• Proof step 51:

  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 ∪ h1 ∪ h10 ⊥ h20 ∪ h21 ∪ h210 ∧ h0 ∪ h1 ∪ h10 ⊥ h2 ∧ h2 ⊥ h20 ∪ h21 ∪ h210 ∧ (h1 ∪ h0 ∪ h10) ∪ h2 ∪ h20 ∪ h21 ∪ h210 = (h0 ∪ h1 ∪ h10) ∪ h2 ∪ h20 ∪ h21 ∪ h210 ∧ (hP0 ⊗ hP1)((h0 ∪ h1 ∪ h10) ∪ h20 ∪ h21 ∪ h210) ∧ hP2(h2 ∪ h20 ∪ h21 ∪ h210)

Rule argument

Additional information

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

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

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 52:

  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 ∪ h10) ∪ h2 ∪ h20 ∪ h21 ∪ h210 ∧ (hP0 ⊗ hP1)((h0 ∪ h1 ∪ h10) ∪ 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 52 from proof sharing-ass-aux2 (previous step) (back to tree)

User applied rule case distinction

And obtained the following new goals

• Proof step 53:

  (h1 ∪ h0 ∪ h10) ∪ h2 ∪ h20 ∪ h21 ∪ h210 ≠ (h0 ∪ h1 ∪ h10) ∪ h2 ∪ h20 ∪ h21 ∪ 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 59:

  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), ¬ (hP0 ⊗ hP1)((h0 ∪ h1 ∪ h10) ∪ h20 ∪ h21 ∪ h210) ⊦

Rule argument

Additional information

Proof step 53 from proof sharing-ass-aux2 (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

• Proof step 55:

  (h1 ∪ h0 ∪ h10) ∪ h2 ∪ h20 ∪ h21 ∪ h210 ≠ ((h0 ∪ h1) ∪ h10) ∪ h2 ∪ h20 ∪ h21 ∪ h210, h0 ⊥ h2, h0 ⊥ h21, h0 ⊥ h20, h0 ⊥ h10, h0 ⊥ h210, h0 ⊥ h1, h1 ⊥ h2, h1 ⊥ h21, h1 ⊥ h20, h1 ⊥ h210, h1 ⊥ h10, h10 ⊥ h210, h10 ⊥ h0, 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: ⊦ h0 ⊥ h1 → h1 ⊥ h0; (ss) Used terms: h0, h1, h10

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

A spec-lemma

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

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 56:

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

• Proof step 57:

  (h1 ∪ h0 ∪ h10) ∪ h2 ∪ h20 ∪ h21 ∪ h210 ≠ ((h1 ∪ h0) ∪ h10) ∪ h2 ∪ h20 ∪ h21 ∪ h210, h0 ⊥ h1, h0 ⊥ h210, h0 ⊥ h10, h0 ⊥ h20, h0 ⊥ h21, h0 ⊥ h2, h1 ⊥ h10, h1 ⊥ h210, h1 ⊥ h20, h1 ⊥ h21, h1 ⊥ h2, h1 ⊥ h0, h10 ⊥ h0, 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: ⊦ h0 ⊥ h1 → h1 ⊥ h0; (ss) Used terms: h0, h1

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

A spec-lemma

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

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 58:

  ⊦ h0 ⊥ h1 ∧ h1 ⊥ h ∧ h ⊥ h0 → (h0 ∪ h1) ∪ h = h0 ∪ h1 ∪ h

Rule argument

Additional information

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

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

A spec-lemma

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

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 60:

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

• Proof step 61:

  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), ∀ h2, h3, h4. ¬(h2 ⊥ h4 ∧ h2 ⊥ h3 ∧ h3 ⊥ h4 ∧ (h0 ∪ h1 ∪ h10) ∪ h20 ∪ h21 ∪ h210 = h2 ∪ h3 ∪ h4 ∧ hP0(h2 ∪ h4) ∧ hP1(h3 ∪ h4)) ⊦

Rule argument

Additional information

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

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

Lemma sharing

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

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 62:

  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 ∨ (h0 ∪ h1 ∪ h10) ∪ h20 ∪ h21 ∪ h210 ≠ h ∪ h3 ∪ h4 ∨ ¬ hP0(h ∪ h4) ∨ ¬ hP1(h3 ∪ h4) ⊦

Rule argument

Additional information

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

User applied rule all left

And obtained the following new goals

• Proof step 63:

  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 ∪ h20 ⊥ h10 ∪ h210 ∨ ¬ h0 ∪ h20 ⊥ h1 ∪ h21 ∨ ¬ h1 ∪ h21 ⊥ h10 ∪ h210 ∨ (h0 ∪ h1 ∪ h10) ∪ h20 ∪ h21 ∪ h210 ≠ (h0 ∪ h20) ∪ (h1 ∪ h21) ∪ h10 ∪ h210 ∨ ¬ hP0((h0 ∪ h20) ∪ h10 ∪ h210) ∨ ¬ hP1((h1 ∪ h21) ∪ h10 ∪ h210) ⊦

Rule argument

Additional information

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

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

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 64:

  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 ∪ h1 ∪ h10) ∪ h20 ∪ h21 ∪ h210 ≠ (h0 ∪ h20) ∪ (h1 ∪ h21) ∪ h10 ∪ h210 ∨ ¬ hP0((h0 ∪ h20) ∪ h10 ∪ h210) ∨ ¬ hP1((h1 ∪ h21) ∪ h10 ∪ h210) ⊦

Rule argument

Additional information

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

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

User applied rule case distinction

And obtained the following new goals

• Proof step 65:

  (h0 ∪ h1 ∪ h10) ∪ h20 ∪ h21 ∪ h210 ≠ (h0 ∪ h20) ∪ (h1 ∪ h21) ∪ h10 ∪ 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 99:

  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), ¬ hP0((h0 ∪ h20) ∪ h10 ∪ h210) ⊦

• Proof step 108:

  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 ∪ h21) ∪ h10 ∪ h210) ⊦

Rule argument

Additional information

Proof step 65 from proof sharing-ass-aux2 (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:

  (h0 ∪ h1 ∪ h10) ∪ h20 ∪ h21 ∪ h210 ≠ h0 ∪ h20 ∪ (h1 ∪ h21) ∪ h10 ∪ h210, h0 ⊥ h210, h0 ⊥ h10, h0 ⊥ h21, h0 ⊥ h2, h0 ⊥ h1, h0 ⊥ h20, h1 ⊥ h210, h1 ⊥ h10, h1 ⊥ h20, h1 ⊥ h21, h1 ⊥ h2, (h1 ∪ h21) ∪ h10 ∪ h210 ⊥ h0, h10 ⊥ h210, h2 ⊥ h210, h2 ⊥ h10, h2 ⊥ h20, h2 ⊥ h21, h20 ⊥ h210, h20 ⊥ h10, h20 ⊥ (h1 ∪ h21) ∪ h10 ∪ h210, 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: h0, h20, (h1 ∪ h21) ∪ h10 ∪ h210

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

A spec-lemma

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

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 68:

  (h0 ∪ h1 ∪ h10) ∪ h20 ∪ h21 ∪ h210 ≠ h0 ∪ h20 ∪ (h1 ∪ h21) ∪ h10 ∪ h210, h0 ⊥ h20, h0 ⊥ h1, h0 ⊥ h2, h0 ⊥ h21, 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, h20 ⊥ h1, h20 ⊥ 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)

Proof step 68 from proof sharing-ass-aux2 (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:

  h0 ∪ (h1 ∪ h10) ∪ h20 ∪ h21 ∪ h210 ≠ h0 ∪ h20 ∪ (h1 ∪ h21) ∪ h10 ∪ h210, h0 ⊥ h210, h0 ⊥ h10, h0 ⊥ h21, h0 ⊥ h2, h0 ⊥ h1, h0 ⊥ h20, h0 ⊥ h1 ∪ h10, h1 ⊥ h210, h1 ⊥ h10, h1 ⊥ h20, h1 ⊥ h21, h1 ⊥ h2, h1 ∪ h10 ⊥ h20 ∪ h21 ∪ h210, h10 ⊥ h210, h2 ⊥ h210, h2 ⊥ h10, h2 ⊥ h20, h2 ⊥ h21, h20 ⊥ h21, h20 ⊥ h1, h20 ⊥ h210, h20 ⊥ h10, h20 ∪ h21 ∪ h210 ⊥ h0, 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: h0, h1 ∪ h10, h20 ∪ h21 ∪ h210

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

A spec-lemma

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

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 71:

  h0 ∪ (h1 ∪ h10) ∪ h20 ∪ h21 ∪ h210 ≠ h0 ∪ h20 ∪ (h1 ∪ h21) ∪ h10 ∪ h210, h0 ⊥ h20, h0 ⊥ h1, h0 ⊥ h2, h0 ⊥ h21, h0 ⊥ h10, h0 ⊥ h210, h1 ⊥ h2, h1 ⊥ h21, h1 ⊥ h20, h1 ⊥ h10, h1 ⊥ h210, h10 ⊥ h210, h10 ⊥ h20, h10 ⊥ h21, h2 ⊥ h21, h2 ⊥ h20, h2 ⊥ h10, h2 ⊥ h210, h20 ⊥ h10, h20 ⊥ h210, h20 ⊥ h1, h20 ⊥ 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)

Proof step 71 from proof sharing-ass-aux2 (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:

  h0 ∪ (h1 ∪ h10) ∪ h20 ∪ h21 ∪ h210 ≠ h0 ∪ h20 ∪ (h1 ∪ h21) ∪ h10 ∪ h210, h0 ⊥ h210, h0 ⊥ h10, h0 ⊥ h21, h0 ⊥ h2, h0 ⊥ h1, h0 ⊥ h20, h1 ⊥ h210, h1 ⊥ h10, h1 ⊥ h20, h1 ⊥ h21, h1 ⊥ h2, h10 ⊥ h21, h10 ⊥ h20, h10 ⊥ h210, h2 ⊥ h210, h2 ⊥ h10, h2 ⊥ h20, h2 ⊥ h21, h20 ⊥ h21, h20 ⊥ 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) ⊦ h0 ⊥ h20 ∪ (h1 ∪ h21) ∪ h10 ∪ h210 ∧ h0 ⊥ (h1 ∪ h10) ∪ h20 ∪ h21 ∪ h210

• Proof step 76:

  h20 ∪ (h1 ∪ h21) ∪ h10 ∪ h210 ≠ (h1 ∪ h10) ∪ h20 ∪ h21 ∪ h210, h0 ⊥ h210, h0 ⊥ h10, h0 ⊥ h21, h0 ⊥ h2, h0 ⊥ h1, h0 ⊥ h20, h0 ⊥ h20 ∪ (h1 ∪ h21) ∪ h10 ∪ h210, h0 ⊥ (h1 ∪ h10) ∪ h20 ∪ h21 ∪ h210, h1 ⊥ h210, h1 ⊥ h10, h1 ⊥ h20, h1 ⊥ h21, h1 ⊥ h2, h10 ⊥ h21, h10 ⊥ h20, h10 ⊥ h210, h2 ⊥ h210, h2 ⊥ h10, h2 ⊥ h20, h2 ⊥ h21, h20 ⊥ h21, h20 ⊥ 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 terms: h0, (h1 ∪ h10) ∪ h20 ∪ h21 ∪ h210, h20 ∪ (h1 ∪ h21) ∪ h10 ∪ h210

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

A spec-lemma

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

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 74:

  h0 ∪ (h1 ∪ h10) ∪ h20 ∪ h21 ∪ h210 ≠ h0 ∪ h20 ∪ (h1 ∪ h21) ∪ h10 ∪ h210, h0 ⊥ h20, h0 ⊥ h1, h0 ⊥ h2, h0 ⊥ h21, h0 ⊥ h10, h0 ⊥ h210, h1 ⊥ h2, h1 ⊥ h21, h1 ⊥ h20, h1 ⊥ h10, h1 ⊥ h210, h10 ⊥ h210, h10 ⊥ h20, h10 ⊥ h21, h2 ⊥ h21, h2 ⊥ h20, h2 ⊥ h10, h2 ⊥ h210, h20 ⊥ h10, h20 ⊥ h210, h20 ⊥ h1, h20 ⊥ h21, h21 ⊥ h20, h21 ⊥ h10, h21 ⊥ h210, hP0(h0 ∪ h10 ∪ h20 ∪ h210), hP1(h1 ∪ h10 ∪ h21 ∪ h210), hP2(h2 ∪ h20 ∪ h21 ∪ h210) ⊦ h0 ⊥ (h1 ∪ h21) ∪ h10 ∪ h210 ∧ h0 ⊥ (h1 ∪ h10) ∪ 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 ⊥ h ⊦ h0 ⊥ h1 ∪ h ↔ h0 ⊥ h1 ∧ h0 ⊥ h; (ss) h1 ⊥ h2 ⊦ h1 ∪ h2 ⊥ h0 ↔ h0 ⊥ h1 ∧ h0 ⊥ h2; (s)

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

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 75:

  h1 ⊥ h ⊦ h0 ⊥ h1 ∪ h ↔ h0 ⊥ h1 ∧ h0 ⊥ h

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, h1 ∪ h21, h10 ∪ h210

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

A spec-lemma

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

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 77:

  h20 ∪ (h1 ∪ h21) ∪ h10 ∪ h210 ≠ (h1 ∪ h10) ∪ h20 ∪ h21 ∪ h210, h0 ⊥ h20, h0 ⊥ h1, h0 ⊥ h2, h0 ⊥ h21, h0 ⊥ h10, h0 ⊥ h210, h1 ⊥ h2, h1 ⊥ h21, h1 ⊥ h20, h1 ⊥ h10, h1 ⊥ h210, h10 ⊥ h210, h10 ⊥ h20, h10 ⊥ h21, h2 ⊥ h21, h2 ⊥ h20, h2 ⊥ h10, h2 ⊥ h210, h20 ⊥ h10, h20 ⊥ h210, h20 ⊥ h1, h20 ⊥ 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) ⊦ 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 77 from proof sharing-ass-aux2 (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 78:

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

• Proof step 79:

  h20 ∪ (h1 ∪ h21) ∪ h10 ∪ h210 ≠ (h20 ∪ h21 ∪ h210) ∪ h1 ∪ h10, h0 ⊥ h210, h0 ⊥ h10, h0 ⊥ h21, h0 ⊥ h2, h0 ⊥ h1, h0 ⊥ h20, h1 ⊥ h210, h1 ⊥ h10, h1 ⊥ h20, h1 ⊥ h21, h1 ⊥ h2, h10 ⊥ h21, h10 ⊥ h20, h10 ⊥ h210, h2 ⊥ h210, h2 ⊥ h10, h2 ⊥ h20, h2 ⊥ h21, h20 ⊥ h21, h20 ⊥ h1, h20 ⊥ h210, h20 ⊥ h10, h20 ∪ h21 ∪ h210 ⊥ h1 ∪ 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) ⊦ h0 ⊥ h1 → h1 ⊥ h0; (ss) Used terms: h1 ∪ h10, h20 ∪ h21 ∪ h210

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

A spec-lemma

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

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 80:

  h20 ∪ (h1 ∪ h21) ∪ h10 ∪ h210 ≠ (h20 ∪ h21 ∪ h210) ∪ h1 ∪ h10, h0 ⊥ h20, h0 ⊥ h1, h0 ⊥ h2, h0 ⊥ h21, h0 ⊥ h10, h0 ⊥ h210, h1 ⊥ h2, h1 ⊥ h21, h1 ⊥ h20, h1 ⊥ h10, h1 ⊥ h210, h10 ⊥ h210, h10 ⊥ h20, h10 ⊥ h21, h2 ⊥ h21, h2 ⊥ h20, h2 ⊥ h10, h2 ⊥ h210, h20 ⊥ h10, h20 ⊥ h210, h20 ⊥ h1, h20 ⊥ 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 ⊥ h2 ⊦ h1 ∪ h2 ⊥ h0 ↔ h0 ⊥ h1 ∧ h0 ⊥ h2; (s) h1 ⊥ h ⊦ h0 ⊥ h1 ∪ h ↔ h0 ⊥ h1 ∧ h0 ⊥ h; (ws)

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

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 81:

  ⊦ h0 ⊥ h1 ∧ h1 ⊥ h ∧ h ⊥ h0 → (h0 ∪ h1) ∪ h = h0 ∪ h1 ∪ h

• Proof step 82:

  h20 ∪ (h1 ∪ h21) ∪ h10 ∪ h210 ≠ h20 ∪ (h21 ∪ h210) ∪ h1 ∪ h10, h0 ⊥ h210, h0 ⊥ h10, h0 ⊥ h21, h0 ⊥ h2, h0 ⊥ h1, h0 ⊥ h20, h1 ⊥ h210, h1 ⊥ h10, h1 ⊥ h20, h1 ⊥ h21, h1 ⊥ h2, h1 ∪ h10 ⊥ h20, h10 ⊥ h21, h10 ⊥ h20, h10 ⊥ h210, h2 ⊥ h210, h2 ⊥ h10, h2 ⊥ h20, h2 ⊥ h21, h20 ⊥ h21, h20 ⊥ h1, h20 ⊥ h210, h20 ⊥ h10, h20 ⊥ h21 ∪ h210, h21 ⊥ h210, h21 ⊥ h10, h21 ⊥ h20, h21 ∪ h210 ⊥ h1 ∪ h10, 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, h21 ∪ h210, h1 ∪ h10

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

A spec-lemma

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

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 83:

  h20 ∪ (h1 ∪ h21) ∪ h10 ∪ h210 ≠ h20 ∪ (h21 ∪ h210) ∪ h1 ∪ h10, h0 ⊥ h20, h0 ⊥ h1, h0 ⊥ h2, h0 ⊥ h21, h0 ⊥ h10, h0 ⊥ h210, h1 ⊥ h2, h1 ⊥ h21, h1 ⊥ h20, h1 ⊥ h10, h1 ⊥ h210, h10 ⊥ h210, h10 ⊥ h20, h10 ⊥ h21, h2 ⊥ h21, h2 ⊥ h20, h2 ⊥ h10, h2 ⊥ h210, h20 ⊥ h10, h20 ⊥ h210, h20 ⊥ h1, h20 ⊥ h21, h21 ⊥ h20, h21 ⊥ h10, h21 ⊥ h210, h21 ⊥ h1, h210 ⊥ h1, h210 ⊥ h10, 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 83 from proof sharing-ass-aux2 (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 84:

  ⊦ h ⊥ h0 ∧ h ⊥ h1 → (h ∪ h0 = h ∪ h1 ↔ h0 = h1)

• Proof step 85:

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

• Proof step 87:

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

Rule argument

Additional information

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

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

A spec-lemma

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

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 86:

  h1 ⊥ h ⊦ h0 ⊥ h1 ∪ h ↔ h0 ⊥ h1 ∧ h0 ⊥ h

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) Used terms: h20, h21 ∪ h210, h1 ∪ h10

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

A spec-lemma

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

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 88:

  (h21 ∪ h210) ∪ h1 ∪ h10 ≠ (h1 ∪ h21) ∪ h10 ∪ h210, h0 ⊥ h20, h0 ⊥ h1, h0 ⊥ h2, h0 ⊥ h21, h0 ⊥ h10, h0 ⊥ h210, h1 ⊥ h2, h1 ⊥ h21, h1 ⊥ h20, h1 ⊥ h10, h1 ⊥ h210, h10 ⊥ h210, h10 ⊥ h20, h10 ⊥ h21, h2 ⊥ h21, h2 ⊥ h20, h2 ⊥ h10, h2 ⊥ h210, h20 ⊥ h10, h20 ⊥ h210, h20 ⊥ h1, h20 ⊥ h21, h21 ⊥ h20, h21 ⊥ h10, h21 ⊥ h210, h21 ⊥ h1, h210 ⊥ h1, h210 ⊥ h10, 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 88 from proof sharing-ass-aux2 (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 89:

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

• Proof step 90:

  (h1 ∪ h10) ∪ h21 ∪ h210 ≠ (h1 ∪ h21) ∪ h10 ∪ h210, h0 ⊥ h210, h0 ⊥ h10, h0 ⊥ h21, h0 ⊥ h2, h0 ⊥ h1, h0 ⊥ h20, h1 ⊥ h210, h1 ⊥ h10, h1 ⊥ h20, h1 ⊥ h21, h1 ⊥ h2, h1 ∪ h10 ⊥ h21 ∪ h210, h10 ⊥ h21, h10 ⊥ h20, h10 ⊥ h210, h2 ⊥ h210, h2 ⊥ h10, h2 ⊥ h20, h2 ⊥ h21, h20 ⊥ h21, h20 ⊥ h1, h20 ⊥ h210, h20 ⊥ h10, h21 ⊥ h1, h21 ⊥ h210, h21 ⊥ h10, h21 ⊥ h20, h210 ⊥ h10, h210 ⊥ h1, 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: h21 ∪ h210, h1 ∪ h10

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

A spec-lemma

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

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 91:

  (h1 ∪ h10) ∪ h21 ∪ h210 ≠ (h1 ∪ h21) ∪ h10 ∪ h210, h0 ⊥ h20, h0 ⊥ h1, h0 ⊥ h2, h0 ⊥ h21, h0 ⊥ h10, h0 ⊥ h210, h1 ⊥ h2, h1 ⊥ h21, h1 ⊥ h20, h1 ⊥ h10, h1 ⊥ h210, h10 ⊥ h210, h10 ⊥ h20, h10 ⊥ h21, h2 ⊥ h21, h2 ⊥ h20, h2 ⊥ h10, h2 ⊥ h210, h20 ⊥ h10, h20 ⊥ h210, h20 ⊥ h1, h20 ⊥ h21, h21 ⊥ h20, h21 ⊥ h10, h21 ⊥ h210, h21 ⊥ h1, h210 ⊥ h1, h210 ⊥ h10, 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 91 from proof sharing-ass-aux2 (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 92:

  ⊦ h0 ⊥ h1 ∧ h1 ⊥ h ∧ h ⊥ h0 → (h0 ∪ h1) ∪ h = h0 ∪ h1 ∪ h

• Proof step 93:

  h1 ∪ h10 ∪ h21 ∪ h210 ≠ (h1 ∪ h21) ∪ h10 ∪ h210, h0 ⊥ h210, h0 ⊥ h10, h0 ⊥ h21, h0 ⊥ h2, h0 ⊥ h1, h0 ⊥ h20, h1 ⊥ h210, h1 ⊥ h20, h1 ⊥ h21, h1 ⊥ h2, h1 ⊥ h10, h10 ⊥ h21, h10 ⊥ h20, h10 ⊥ h210, h10 ⊥ h21 ∪ h210, h2 ⊥ h210, h2 ⊥ h10, h2 ⊥ h20, h2 ⊥ h21, h20 ⊥ h21, h20 ⊥ h1, h20 ⊥ h210, h20 ⊥ h10, h21 ⊥ h1, h21 ⊥ h210, h21 ⊥ h10, h21 ⊥ h20, h21 ∪ h210 ⊥ h1, h210 ⊥ h10, h210 ⊥ h1, 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: h1, h10, h21 ∪ h210

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

A spec-lemma

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

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 94:

  h1 ∪ h10 ∪ h21 ∪ h210 ≠ (h1 ∪ h21) ∪ h10 ∪ h210, h0 ⊥ h20, h0 ⊥ h1, h0 ⊥ h2, h0 ⊥ h21, h0 ⊥ h10, h0 ⊥ h210, h1 ⊥ h10, h1 ⊥ h2, h1 ⊥ h21, h1 ⊥ h20, h1 ⊥ h210, h10 ⊥ h210, h10 ⊥ h20, h10 ⊥ h21, h2 ⊥ h21, h2 ⊥ h20, h2 ⊥ h10, h2 ⊥ h210, h20 ⊥ h10, h20 ⊥ h210, h20 ⊥ h1, h20 ⊥ h21, h21 ⊥ h20, h21 ⊥ h10, h21 ⊥ h210, h21 ⊥ h1, h210 ⊥ h1, h210 ⊥ h10, 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 94 from proof sharing-ass-aux2 (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

• Proof step 96:

  h1 ∪ h10 ∪ h21 ∪ h210 ≠ h1 ∪ h21 ∪ h10 ∪ h210, h0 ⊥ h210, h0 ⊥ h10, h0 ⊥ h21, h0 ⊥ h2, h0 ⊥ h1, h0 ⊥ h20, h1 ⊥ h210, h1 ⊥ h20, h1 ⊥ h2, h1 ⊥ h10, h1 ⊥ h21, h10 ⊥ h21, h10 ⊥ h20, h10 ⊥ h210, h10 ∪ h210 ⊥ h1, h2 ⊥ h210, h2 ⊥ h10, h2 ⊥ h20, h2 ⊥ h21, h20 ⊥ h21, h20 ⊥ h1, h20 ⊥ h210, h20 ⊥ h10, h21 ⊥ h1, h21 ⊥ h210, h21 ⊥ h10, h21 ⊥ h20, h21 ⊥ h10 ∪ h210, h210 ⊥ h10, h210 ⊥ h1, 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: h1, h21, h10 ∪ h210

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

A spec-lemma

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

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 97:

  h1 ∪ h10 ∪ h21 ∪ h210 ≠ h1 ∪ h21 ∪ h10 ∪ h210, h0 ⊥ h20, h0 ⊥ h1, h0 ⊥ h2, h0 ⊥ h21, h0 ⊥ h10, h0 ⊥ h210, h1 ⊥ h21, h1 ⊥ h10, h1 ⊥ h2, h1 ⊥ h20, h1 ⊥ h210, h10 ⊥ h210, h10 ⊥ h20, h10 ⊥ h21, h2 ⊥ h21, h2 ⊥ h20, h2 ⊥ h10, h2 ⊥ h210, h20 ⊥ h10, h20 ⊥ h210, h20 ⊥ h1, h20 ⊥ h21, h21 ⊥ h20, h21 ⊥ h10, h21 ⊥ h210, h21 ⊥ h1, h210 ⊥ h1, h210 ⊥ h10, 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)

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

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 98:

  ⊦ h ⊥ h0 ∧ h ⊥ h1 → (h ∪ h0 = h ∪ h1 ↔ h0 = h1)

Rule argument

Additional information

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

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

A spec-lemma

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

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 100:

  ⊦ h0 ⊥ h1 ∧ h1 ⊥ h ∧ h ⊥ h0 → (h0 ∪ h1) ∪ h = h0 ∪ h1 ∪ h

• Proof step 101:

  h0 ⊥ h210, h0 ⊥ h10, h0 ⊥ h21, h0 ⊥ h2, h0 ⊥ h1, h0 ⊥ h20, h1 ⊥ h210, h1 ⊥ h10, h1 ⊥ h20, h1 ⊥ h21, h1 ⊥ h2, h10 ⊥ h210, h10 ∪ h210 ⊥ h0, h2 ⊥ h210, h2 ⊥ h10, h2 ⊥ h20, h2 ⊥ h21, h20 ⊥ h210, h20 ⊥ h10, h20 ⊥ h10 ∪ h210, h21 ⊥ h210, h21 ⊥ h10, h21 ⊥ h20, hP0(h0 ∪ h10 ∪ h20 ∪ h210), hP1(h1 ∪ h10 ∪ h21 ∪ h210), hP2(h2 ∪ h20 ∪ h21 ∪ h210), ¬ hP0(h0 ∪ h20 ∪ h10 ∪ 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) Used terms: h0, h20, h10 ∪ h210

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

A spec-lemma

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

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 102:

  h0 ⊥ h20, h0 ⊥ h1, h0 ⊥ h2, h0 ⊥ h21, 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), ¬ hP0(h0 ∪ h20 ∪ h10 ∪ 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 102 from proof sharing-ass-aux2 (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:

  h0 ⊥ h210, h0 ⊥ h10, h0 ⊥ h21, h0 ⊥ h2, h0 ⊥ h1, h0 ⊥ h20, 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, h210 ⊥ h20, hP0(h0 ∪ h10 ∪ h20 ∪ h210), hP1(h1 ∪ h10 ∪ h21 ∪ h210), hP2(h2 ∪ h20 ∪ h21 ∪ h210), ¬ hP0(h0 ∪ (h20 ∪ h10) ∪ h210) ⊦

Rule argument

Additional information

Used simplifier rules: ⊦ h0 ⊥ h1 → h1 ⊥ h0; (ss) Used terms: h20, h10, h210

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

A spec-lemma

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

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 105:

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

• Proof step 106:

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

Rule argument

Additional information

Used simplifier rules: ⊦ h0 ⊥ h1 → h1 ⊥ h0; (ss) Used terms: h20, h10

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

A spec-lemma

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

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 107:

  ⊦ h0 ⊥ h1 ∧ h1 ⊥ h ∧ h ⊥ h0 → (h0 ∪ h1) ∪ h = h0 ∪ h1 ∪ h

Rule argument

Additional information

Used simplifier rules: ⊦ h0 ⊥ h1 → h1 ⊥ h0; (ss) Used terms: h10, h20, h210

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

A spec-lemma

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

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 109:

  ⊦ h0 ⊥ h1 ∧ h1 ⊥ h ∧ h ⊥ h0 → (h0 ∪ h1) ∪ h = h0 ∪ h1 ∪ h

• Proof step 110:

  h0 ⊥ h210, h0 ⊥ h10, h0 ⊥ h20, h0 ⊥ h21, h0 ⊥ h2, h0 ⊥ h1, h1 ⊥ h210, h1 ⊥ h10, h1 ⊥ h20, h1 ⊥ h2, h1 ⊥ h21, h10 ⊥ h210, h10 ∪ h210 ⊥ h1, h2 ⊥ h210, h2 ⊥ h10, h2 ⊥ h20, h2 ⊥ h21, h20 ⊥ h210, h20 ⊥ h10, h21 ⊥ h210, h21 ⊥ h10, h21 ⊥ h20, h21 ⊥ h10 ∪ h210, hP0(h0 ∪ h10 ∪ h20 ∪ h210), hP1(h1 ∪ h10 ∪ h21 ∪ h210), hP2(h2 ∪ h20 ∪ h21 ∪ h210), ¬ hP1(h1 ∪ h21 ∪ h10 ∪ 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) Used terms: h1, h21, h10 ∪ h210

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

A spec-lemma

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

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 111:

  h0 ⊥ h1, h0 ⊥ h2, h0 ⊥ h21, h0 ⊥ h20, h0 ⊥ h10, h0 ⊥ h210, h1 ⊥ h21, h1 ⊥ h2, 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 ∪ h21 ∪ h10 ∪ 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 111 from proof sharing-ass-aux2 (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 112:

  ⊦ h0 ⊥ h1 ∧ h1 ⊥ h ∧ h ⊥ h0 → (h0 ∪ h1) ∪ h = h0 ∪ h1 ∪ h

• Proof step 113:

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

Rule argument

Additional information

Used simplifier rules: ⊦ h0 ⊥ h1 → h1 ⊥ h0; (ss) Used terms: h21, h10, h210

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

A spec-lemma

Proof step 113 from proof sharing-ass-aux2 (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:

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

Rule argument

Additional information

Used simplifier rules: ⊦ h0 ⊥ h1 → h1 ⊥ h0; (ss) Used terms: h21, h10

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

A spec-lemma

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

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 116:

  ⊦ h0 ⊥ h1 ∧ h1 ⊥ h ∧ h ⊥ h0 → (h0 ∪ h1) ∪ h = h0 ∪ h1 ∪ h

Rule argument

Additional information

Used simplifier rules: ⊦ h0 ⊥ h1 → h1 ⊥ h0; (ss) Used terms: h10, h21, h210

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

A spec-lemma