Proof step 1 from proof union-split3 (conclusion) (back to tree)

System applied rule normalize

And obtained the following new goals

• Proof step 2:

  h0 ⊥ h1, h2 ⊥ h4, h2 ⊥ h3, 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)

Rule argument

Additional information

Proof step 2 from proof union-split3 (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 3:

  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 ⊥ h31 ∪ h41 ∧ h30 ⊥ h21 ∪ h31 ∪ h41 ∧ h40 ⊥ h21 ∪ h31 ∪ h41 ∧ h21 ⊥ h20 ∪ h30 ∪ h40 ∧ h31 ⊥ h20 ∪ h30 ∪ h40 ∧ h41 ⊥ h20 ∪ h30 ∪ h40)

Rule argument

Additional information

Used simplifier rules: disj-distr-uni: h1 ⊥ h ⊦ h0 ⊥ h1 ∪ h ↔ h0 ⊥ h1 ∧ h0 ⊥ h; disj-distr-uni-com: h1 ⊥ h2 ⊦ h1 ∪ h2 ⊥ h0 ↔ h0 ⊥ h1 ∧ h0 ⊥ h2; disj-distr-uni: h1 ⊥ h ⊦ h0 ⊥ h1 ∪ h ↔ h0 ⊥ h1 ∧ h0 ⊥ h;

Proof step 3 from proof union-split3 (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 4:

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

• Proof step 5:

  h0 ⊥ h1, h2 ⊥ h4, h2 ⊥ h3, h2 ⊥ h3 ∪ h4, h3 ⊥ h4 ⊦ (∃ h20, h21, h30, h31. h0 = h20 ∪ h21 ∧ h1 = h30 ∪ h31 ∧ h2 = h20 ∪ h30 ∧ h3 ∪ h4 = h21 ∪ h31 ∧ h20 ⊥ h21 ∧ h30 ⊥ h31 ∧ h20 ⊥ h3 ∪ h4 ∧ h30 ⊥ h3 ∪ h4 ∧ h21 ⊥ h2 ∧ h31 ⊥ h2) ↔ (∃ 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 ⊥ h31 ∪ h41 ∧ h30 ⊥ h21 ∪ h31 ∪ h41 ∧ h40 ⊥ h21 ∪ h31 ∪ h41 ∧ h21 ⊥ h20 ∪ h30 ∪ h40 ∧ h31 ⊥ h20 ∪ h30 ∪ h40 ∧ h41 ⊥ h20 ∪ h30 ∪ h40)

Rule argument

Additional information

Used simplifier rules: disj-distr-uni: h1 ⊥ h ⊦ h0 ⊥ h1 ∪ h ↔ h0 ⊥ h1 ∧ h0 ⊥ h; Used terms: h0, h1, h2, h3 ∪ h4

Proof step 4 from proof union-split3 (previous step) (back to tree)

Lemma union-split2

Proof step 5 from proof union-split3 (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 6:

  h0 ⊥ h1, h2 ⊥ h3, h2 ⊥ h4, h3 ⊥ h4 ⊦ (∃ h20, h21, h30, h31. h0 = h20 ∪ h21 ∧ h1 = h30 ∪ h31 ∧ h2 = h20 ∪ h30 ∧ h3 ∪ h4 = h21 ∪ h31 ∧ h20 ⊥ h21 ∧ h30 ⊥ h31 ∧ h20 ⊥ h3 ∪ h4 ∧ h30 ⊥ h3 ∪ h4 ∧ h21 ⊥ h20 ∪ h30 ∧ h31 ⊥ h20 ∪ h30) ↔ (∃ 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 ⊥ h31 ∪ h41 ∧ h30 ⊥ h21 ∪ h31 ∪ h41 ∧ h40 ⊥ h21 ∪ h31 ∪ h41 ∧ h21 ⊥ h20 ∪ h30 ∪ h40 ∧ h31 ⊥ h20 ∪ h30 ∪ h40 ∧ h41 ⊥ h20 ∪ h30 ∪ h40)

Rule argument

Additional information

Used simplifier rules: disj-distr-uni: h1 ⊥ h ⊦ h0 ⊥ h1 ∪ h ↔ h0 ⊥ h1 ∧ h0 ⊥ h;

Proof step 6 from proof union-split3 (previous step) (back to tree)

User applied rule case distinction

And obtained the following new goals

• Proof step 7:

  h0 ⊥ h1, h2 ⊥ h4, h2 ⊥ h3, h3 ⊥ h4, ∃ h20, h21, h30, h31. h0 = h20 ∪ h21 ∧ h1 = h30 ∪ h31 ∧ h2 = h20 ∪ h30 ∧ h3 ∪ h4 = h21 ∪ h31 ∧ h20 ⊥ h21 ∧ h30 ⊥ h31 ∧ h20 ⊥ h3 ∪ h4 ∧ h30 ⊥ h3 ∪ h4 ∧ h21 ⊥ h20 ∪ h30 ∧ h31 ⊥ h20 ∪ h30 ⊦ ∃ 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 ⊥ h31 ∪ h41 ∧ h30 ⊥ h21 ∪ h31 ∪ h41 ∧ h40 ⊥ h21 ∪ h31 ∪ h41 ∧ h21 ⊥ h20 ∪ h30 ∪ h40 ∧ h31 ⊥ h20 ∪ h30 ∪ h40 ∧ h41 ⊥ h20 ∪ h30 ∪ h40

• Proof step 24:

  h0 ⊥ h1, h2 ⊥ h4, h2 ⊥ h3, 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 ⊥ h31 ∪ h41 ∧ h30 ⊥ h21 ∪ h31 ∪ h41 ∧ h40 ⊥ h21 ∪ h31 ∪ h41 ∧ h21 ⊥ h20 ∪ h30 ∪ h40 ∧ h31 ⊥ h20 ∪ h30 ∪ h40 ∧ h41 ⊥ h20 ∪ h30 ∪ h40 ⊦ ∃ h20, h21, h30, h31. h0 = h20 ∪ h21 ∧ h1 = h30 ∪ h31 ∧ h2 = h20 ∪ h30 ∧ h3 ∪ h4 = h21 ∪ h31 ∧ h20 ⊥ h21 ∧ h30 ⊥ h31 ∧ h20 ⊥ h3 ∪ h4 ∧ h30 ⊥ h3 ∪ h4 ∧ h21 ⊥ h20 ∪ h30 ∧ h31 ⊥ h20 ∪ h30

Rule argument

Additional information

Proof step 7 from proof union-split3 (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 8:

  h3 ∪ h4 = h21 ∪ h31, h20 ⊥ h21, h20 ⊥ h3, h20 ⊥ h4, h20 ⊥ h30, h20 ⊥ h31, h21 ⊥ h20, h21 ⊥ h30, h21 ⊥ h31, h3 ⊥ h4, h3 ⊥ h20, h3 ⊥ h30, h30 ⊥ h31, h30 ⊥ h3, h30 ⊥ h4, h31 ⊥ h20, h31 ⊥ h30, h4 ⊥ h20, h4 ⊥ h30 ⊦ ∃ h, h5, h0, h6, h40, h41. h20 ∪ h30 = h ∪ h5 ∧ h3 = h0 ∪ h6 ∧ h4 = h40 ∪ h41 ∧ h20 ∪ h21 = h ∪ h0 ∪ h40 ∧ h30 ∪ h31 = h5 ∪ h6 ∪ h41 ∧ h ⊥ h5 ∧ h0 ⊥ h6 ∧ h40 ⊥ h41 ∧ h ⊥ h6 ∪ h41 ∧ h0 ⊥ h5 ∪ h6 ∪ h41 ∧ h40 ⊥ h5 ∪ h6 ∪ h41 ∧ h5 ⊥ h ∪ h0 ∪ h40 ∧ h6 ⊥ h ∪ h0 ∪ h40 ∧ h41 ⊥ h ∪ h0 ∪ h40

Rule argument

Additional information

Used simplifier rules: disj-distr-uni: h1 ⊥ h ⊦ h0 ⊥ h1 ∪ h ↔ h0 ⊥ h1 ∧ h0 ⊥ h; disj-com-rw: ⊦ h0 ⊥ h1 → h1 ⊥ h0; disj-distr-uni-com: h1 ⊥ h2 ⊦ h1 ∪ h2 ⊥ h0 ↔ h0 ⊥ h1 ∧ h0 ⊥ h2;

Proof step 8 from proof union-split3 (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 9:

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

• Proof step 10:

  h20 ⊥ h31, h20 ⊥ h30, h20 ⊥ h4, h20 ⊥ h3, h20 ⊥ h21, h21 ⊥ h30, h21 ⊥ h20, h21 ⊥ h31, h3 ⊥ h30, h3 ⊥ h20, h3 ⊥ h4, h30 ⊥ h4, h30 ⊥ h3, h30 ⊥ h31, h31 ⊥ h30, h31 ⊥ h20, h4 ⊥ h30, h4 ⊥ h20, ∃ h20, h, h30, h5. h21 = h20 ∪ h ∧ h31 = h30 ∪ h5 ∧ h3 = h20 ∪ h30 ∧ h4 = h ∪ h5 ∧ h20 ⊥ h ∧ h30 ⊥ h5 ∧ h20 ⊥ h4 ∧ h30 ⊥ h4 ∧ h ⊥ h3 ∧ h5 ⊥ h3 ⊦ ∃ h, h5, h0, h6, h40, h41. h20 ∪ h30 = h ∪ h5 ∧ h3 = h0 ∪ h6 ∧ h4 = h40 ∪ h41 ∧ h20 ∪ h21 = h ∪ h0 ∪ h40 ∧ h30 ∪ h31 = h5 ∪ h6 ∪ h41 ∧ h ⊥ h5 ∧ h0 ⊥ h6 ∧ h40 ⊥ h41 ∧ h ⊥ h6 ∪ h41 ∧ h0 ⊥ h5 ∪ h6 ∪ h41 ∧ h40 ⊥ h5 ∪ h6 ∪ h41 ∧ h5 ⊥ h ∪ h0 ∪ h40 ∧ h6 ⊥ h ∪ h0 ∪ h40 ∧ h41 ⊥ h ∪ h0 ∪ h40

Rule argument

Additional information

Used terms: h3, h4, h21, h31

Proof step 9 from proof union-split3 (previous step) (back to tree)

Lemma union-split2

Proof step 10 from proof union-split3 (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 11:

  h ⊥ h0, h ⊥ h5, h ⊥ h1, h0 ⊥ h, h0 ⊥ h1, h0 ⊥ h5, h1 ⊥ h5, h1 ⊥ h0, h20 ⊥ h30, h20 ⊥ h0, h20 ⊥ h5, h20 ⊥ h1, h20 ⊥ h, h30 ⊥ h0, h30 ⊥ h5, h30 ⊥ h1, h30 ⊥ h, h5 ⊥ h, h5 ⊥ h1 ⊦ ∃ h2, h6, h7, h8, h40, h41. h20 ∪ h30 = h2 ∪ h6 ∧ h ∪ h1 = h7 ∪ h8 ∧ h0 ∪ h5 = h40 ∪ h41 ∧ h20 ∪ h ∪ h0 = h2 ∪ h7 ∪ h40 ∧ h30 ∪ h1 ∪ h5 = h6 ∪ h8 ∪ h41 ∧ h2 ⊥ h6 ∧ h7 ⊥ h8 ∧ h40 ⊥ h41 ∧ h2 ⊥ h8 ∪ h41 ∧ h7 ⊥ h6 ∪ h8 ∪ h41 ∧ h40 ⊥ h6 ∪ h8 ∪ h41 ∧ h6 ⊥ h2 ∪ h7 ∪ h40 ∧ h8 ⊥ h2 ∪ h7 ∪ h40 ∧ h41 ⊥ h2 ∪ h7 ∪ h40

Rule argument

Additional information

Used simplifier rules: disj-distr-uni-com: h1 ⊥ h2 ⊦ h1 ∪ h2 ⊥ h0 ↔ h0 ⊥ h1 ∧ h0 ⊥ h2; disj-com-rw: ⊦ h0 ⊥ h1 → h1 ⊥ h0; disj-distr-uni: h1 ⊥ h ⊦ h0 ⊥ h1 ∪ h ↔ h0 ⊥ h1 ∧ h0 ⊥ h;

Proof step 11 from proof union-split3 (previous step) (back to tree)

User applied rule exists right

And obtained the following new goals

• Proof step 12:

  h ⊥ h1, h ⊥ h5, h ⊥ h0, h0 ⊥ h5, h0 ⊥ h1, h0 ⊥ h, h1 ⊥ h0, h1 ⊥ h5, h20 ⊥ h, h20 ⊥ h1, h20 ⊥ h5, h20 ⊥ h0, h20 ⊥ h30, h30 ⊥ h, h30 ⊥ h1, h30 ⊥ h5, h30 ⊥ h0, h5 ⊥ h1, h5 ⊥ h ⊦ h20 ∪ h30 = h20 ∪ h30 ∧ h ∪ h1 = h ∪ h1 ∧ h0 ∪ h5 = h0 ∪ h5 ∧ h20 ∪ h ∪ h0 = h20 ∪ h ∪ h0 ∧ h30 ∪ h1 ∪ h5 = h30 ∪ h1 ∪ h5 ∧ h20 ⊥ h30 ∧ h ⊥ h1 ∧ h0 ⊥ h5 ∧ h20 ⊥ h1 ∪ h5 ∧ h ⊥ h30 ∪ h1 ∪ h5 ∧ h0 ⊥ h30 ∪ h1 ∪ h5 ∧ h30 ⊥ h20 ∪ h ∪ h0 ∧ h1 ⊥ h20 ∪ h ∪ h0 ∧ h5 ⊥ h20 ∪ h ∪ h0

Rule argument

Additional information

Used terms: h20, h30, h, h1, h0, h5

Proof step 12 from proof union-split3 (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 13:

  h ⊥ h0, h ⊥ h5, h ⊥ h1, h0 ⊥ h, h0 ⊥ h1, h0 ⊥ h5, h1 ⊥ h5, h1 ⊥ h0, h20 ⊥ h30, h20 ⊥ h0, h20 ⊥ h5, h20 ⊥ h1, h20 ⊥ h, h30 ⊥ h0, h30 ⊥ h5, h30 ⊥ h1, h30 ⊥ h, h5 ⊥ h, h5 ⊥ h1 ⊦ h ⊥ h30 ∪ h1 ∪ h5 ∧ h0 ⊥ h30 ∪ h1 ∪ h5 ∧ h30 ⊥ h20 ∪ h ∪ h0 ∧ h1 ⊥ h20 ∪ h ∪ h0 ∧ h5 ⊥ h20 ∪ h ∪ h0

Rule argument

Additional information

Used simplifier rules: disj-com-rw: ⊦ h0 ⊥ h1 → h1 ⊥ h0; disj-distr-uni: h1 ⊥ h ⊦ h0 ⊥ h1 ∪ h ↔ h0 ⊥ h1 ∧ h0 ⊥ h;

Proof step 13 from proof union-split3 (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 14:

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

• Proof step 15:

  h ⊥ h1, h ⊥ h5, h ⊥ h0, h0 ⊥ h5, h0 ⊥ h1, h0 ⊥ h, h1 ⊥ h0, h1 ⊥ h5, h20 ⊥ h, h20 ⊥ h1, h20 ⊥ h5, h20 ⊥ h0, h20 ⊥ h30, h30 ⊥ h, h30 ⊥ h1, h30 ⊥ h5, h30 ⊥ h0, h30 ⊥ h1 ∪ h5, h5 ⊥ h1, h5 ⊥ h ⊦ (h ⊥ h30 ∧ h ⊥ h1 ∪ h5) ∧ h0 ⊥ h30 ∪ h1 ∪ h5 ∧ h30 ⊥ h20 ∪ h ∪ h0 ∧ h1 ⊥ h20 ∪ h ∪ h0 ∧ h5 ⊥ h20 ∪ h ∪ h0

Rule argument

Additional information

Used simplifier rules: disj-com-rw: ⊦ h0 ⊥ h1 → h1 ⊥ h0; disj-distr-uni: h1 ⊥ h ⊦ h0 ⊥ h1 ∪ h ↔ h0 ⊥ h1 ∧ h0 ⊥ h; Used terms: h, h30, h1 ∪ h5

Proof step 14 from proof union-split3 (previous step) (back to tree)

Lemma disj-distr-uni

Proof step 15 from proof union-split3 (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 16:

  h ⊥ h0, h ⊥ h5, h ⊥ h1, h0 ⊥ h, h0 ⊥ h1, h0 ⊥ h5, h1 ⊥ h5, h1 ⊥ h0, h20 ⊥ h30, h20 ⊥ h0, h20 ⊥ h5, h20 ⊥ h1, h20 ⊥ h, h30 ⊥ h0, h30 ⊥ h5, h30 ⊥ h1, h30 ⊥ h, h5 ⊥ h, h5 ⊥ h1 ⊦ h0 ⊥ h30 ∪ h1 ∪ h5 ∧ h30 ⊥ h20 ∪ h ∪ h0 ∧ h1 ⊥ h20 ∪ h ∪ h0 ∧ h5 ⊥ h20 ∪ h ∪ h0

Rule argument

Additional information

Used simplifier rules: disj-distr-uni: h1 ⊥ h ⊦ h0 ⊥ h1 ∪ h ↔ h0 ⊥ h1 ∧ h0 ⊥ h; disj-com-rw: ⊦ h0 ⊥ h1 → h1 ⊥ h0;

Proof step 16 from proof union-split3 (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 17:

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

• Proof step 18:

  h ⊥ h1, h ⊥ h5, h ⊥ h0, h0 ⊥ h5, h0 ⊥ h1, h0 ⊥ h, h1 ⊥ h0, h1 ⊥ h5, h20 ⊥ h, h20 ⊥ h1, h20 ⊥ h5, h20 ⊥ h0, h20 ⊥ h30, h30 ⊥ h, h30 ⊥ h1, h30 ⊥ h5, h30 ⊥ h0, h30 ⊥ h1 ∪ h5, h5 ⊥ h1, h5 ⊥ h ⊦ (h0 ⊥ h30 ∧ h0 ⊥ h1 ∪ h5) ∧ h30 ⊥ h20 ∪ h ∪ h0 ∧ h1 ⊥ h20 ∪ h ∪ h0 ∧ h5 ⊥ h20 ∪ h ∪ h0

Rule argument

Additional information

Used simplifier rules: disj-com-rw: ⊦ h0 ⊥ h1 → h1 ⊥ h0; disj-distr-uni: h1 ⊥ h ⊦ h0 ⊥ h1 ∪ h ↔ h0 ⊥ h1 ∧ h0 ⊥ h; Used terms: h0, h30, h1 ∪ h5

Proof step 17 from proof union-split3 (previous step) (back to tree)

Lemma disj-distr-uni

Proof step 18 from proof union-split3 (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 19:

  h ⊥ h0, h ⊥ h5, h ⊥ h1, h0 ⊥ h, h0 ⊥ h1, h0 ⊥ h5, h1 ⊥ h5, h1 ⊥ h0, h20 ⊥ h30, h20 ⊥ h0, h20 ⊥ h5, h20 ⊥ h1, h20 ⊥ h, h30 ⊥ h0, h30 ⊥ h5, h30 ⊥ h1, h30 ⊥ h, h5 ⊥ h, h5 ⊥ h1 ⊦ h30 ⊥ h20 ∪ h ∪ h0 ∧ h1 ⊥ h20 ∪ h ∪ h0 ∧ h5 ⊥ h20 ∪ h ∪ h0

Rule argument

Additional information

Used simplifier rules: disj-com-rw: ⊦ h0 ⊥ h1 → h1 ⊥ h0; disj-distr-uni: h1 ⊥ h ⊦ h0 ⊥ h1 ∪ h ↔ h0 ⊥ h1 ∧ h0 ⊥ h;

Proof step 19 from proof union-split3 (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 20:

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

• Proof step 21:

  h ⊥ h1, h ⊥ h5, h ⊥ h0, h0 ⊥ h5, h0 ⊥ h1, h0 ⊥ h, h1 ⊥ h0, h1 ⊥ h5, h20 ⊥ h, h20 ⊥ h1, h20 ⊥ h5, h20 ⊥ h0, h20 ⊥ h30, h20 ⊥ h ∪ h0, h30 ⊥ h, h30 ⊥ h1, h30 ⊥ h5, h30 ⊥ h0, h5 ⊥ h1, h5 ⊥ h ⊦ (h30 ⊥ h20 ∧ h30 ⊥ h ∪ h0) ∧ h1 ⊥ h20 ∪ h ∪ h0 ∧ h5 ⊥ h20 ∪ h ∪ h0

Rule argument

Additional information

Used simplifier rules: disj-com-rw: ⊦ h0 ⊥ h1 → h1 ⊥ h0; disj-distr-uni: h1 ⊥ h ⊦ h0 ⊥ h1 ∪ h ↔ h0 ⊥ h1 ∧ h0 ⊥ h; Used terms: h30, h20, h ∪ h0

Proof step 20 from proof union-split3 (previous step) (back to tree)

Lemma disj-distr-uni

Proof step 21 from proof union-split3 (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 22:

  h ⊥ h0, h ⊥ h5, h ⊥ h1, h0 ⊥ h, h0 ⊥ h1, h0 ⊥ h5, h1 ⊥ h5, h1 ⊥ h0, h20 ⊥ h30, h20 ⊥ h0, h20 ⊥ h5, h20 ⊥ h1, h20 ⊥ h, h30 ⊥ h0, h30 ⊥ h5, h30 ⊥ h1, h30 ⊥ h, h5 ⊥ h, h5 ⊥ h1 ⊦ h1 ⊥ h20 ∪ h ∪ h0 ∧ h5 ⊥ h20 ∪ h ∪ h0

Rule argument

Additional information

Used simplifier rules: disj-com-rw: ⊦ h0 ⊥ h1 → h1 ⊥ h0; disj-distr-uni: h1 ⊥ h ⊦ h0 ⊥ h1 ∪ h ↔ h0 ⊥ h1 ∧ h0 ⊥ h;

Proof step 22 from proof union-split3 (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 23:

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

Rule argument

Additional information

Used simplifier rules: disj-com-rw: ⊦ h0 ⊥ h1 → h1 ⊥ h0; disj-distr-uni: h1 ⊥ h ⊦ h0 ⊥ h1 ∪ h ↔ h0 ⊥ h1 ∧ h0 ⊥ h; disj-distr-uni: h1 ⊥ h ⊦ h0 ⊥ h1 ∪ h ↔ h0 ⊥ h1 ∧ h0 ⊥ h; disj-distr-uni: h1 ⊥ h ⊦ h0 ⊥ h1 ∪ h ↔ h0 ⊥ h1 ∧ h0 ⊥ h; disj-com-rw: ⊦ h0 ⊥ h1 → h1 ⊥ h0; Used terms: h1, h20, h ∪ h0

Proof step 23 from proof union-split3 (previous step) (back to tree)

Lemma disj-distr-uni

Proof step 24 from proof union-split3 (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 25:

  h20 ⊥ h30, h20 ⊥ h40, h20 ⊥ h21, h20 ⊥ h31, h20 ⊥ h41, h21 ⊥ h30, h21 ⊥ h31, h21 ⊥ h40, h21 ⊥ h41, h21 ⊥ h20, h30 ⊥ h40, h30 ⊥ h41, h30 ⊥ h31, h30 ⊥ h21, h31 ⊥ h40, h31 ⊥ h41, h31 ⊥ h20, h31 ⊥ h30, h40 ⊥ h31, h40 ⊥ h41, h40 ⊥ h21, h41 ⊥ h20, h41 ⊥ h30, h41 ⊥ h40 ⊦ ∃ h, h5, h2, h6. h20 ∪ h30 ∪ h40 = h ∪ h5 ∧ h21 ∪ h31 ∪ h41 = h2 ∪ h6 ∧ h20 ∪ h21 = h ∪ h2 ∧ (h30 ∪ h31) ∪ h40 ∪ h41 = h5 ∪ h6 ∧ h ⊥ h5 ∧ h2 ⊥ h6 ∧ h ⊥ (h30 ∪ h31) ∪ h40 ∪ h41 ∧ h2 ⊥ (h30 ∪ h31) ∪ h40 ∪ h41 ∧ h5 ⊥ h ∪ h2 ∧ h6 ⊥ h ∪ h2

Rule argument

Additional information

Used simplifier rules: disj-distr-uni: h1 ⊥ h ⊦ h0 ⊥ h1 ∪ h ↔ h0 ⊥ h1 ∧ h0 ⊥ h; disj-com-rw: ⊦ h0 ⊥ h1 → h1 ⊥ h0; disj-distr-uni-com: h1 ⊥ h2 ⊦ h1 ∪ h2 ⊥ h0 ↔ h0 ⊥ h1 ∧ h0 ⊥ h2; disj-distr-uni: h1 ⊥ h ⊦ h0 ⊥ h1 ∪ h ↔ h0 ⊥ h1 ∧ h0 ⊥ h;

Proof step 25 from proof union-split3 (previous step) (back to tree)

User applied rule exists right

And obtained the following new goals

• Proof step 26:

  h20 ⊥ h41, h20 ⊥ h31, h20 ⊥ h21, h20 ⊥ h40, h20 ⊥ h30, h21 ⊥ h20, h21 ⊥ h41, h21 ⊥ h40, h21 ⊥ h31, h21 ⊥ h30, h30 ⊥ h21, h30 ⊥ h31, h30 ⊥ h41, h30 ⊥ h40, h31 ⊥ h30, h31 ⊥ h20, h31 ⊥ h41, h31 ⊥ h40, h40 ⊥ h21, h40 ⊥ h41, h40 ⊥ h31, h41 ⊥ h40, h41 ⊥ h30, h41 ⊥ h20 ⊦ h20 ∪ h30 ∪ h40 = h20 ∪ h30 ∪ h40 ∧ h21 ∪ h31 ∪ h41 = h21 ∪ h31 ∪ h41 ∧ h20 ∪ h21 = h20 ∪ h21 ∧ (h30 ∪ h31) ∪ h40 ∪ h41 = (h30 ∪ h40) ∪ h31 ∪ h41 ∧ h20 ⊥ h30 ∪ h40 ∧ h21 ⊥ h31 ∪ h41 ∧ h20 ⊥ (h30 ∪ h31) ∪ h40 ∪ h41 ∧ h21 ⊥ (h30 ∪ h31) ∪ h40 ∪ h41 ∧ h30 ∪ h40 ⊥ h20 ∪ h21 ∧ h31 ∪ h41 ⊥ h20 ∪ h21

Rule argument

Additional information

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

Proof step 26 from proof union-split3 (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 27:

  h20 ⊥ h30, h20 ⊥ h40, h20 ⊥ h21, h20 ⊥ h31, h20 ⊥ h41, h21 ⊥ h30, h21 ⊥ h31, h21 ⊥ h40, h21 ⊥ h41, h21 ⊥ h20, h30 ⊥ h40, h30 ⊥ h41, h30 ⊥ h31, h30 ⊥ h21, h31 ⊥ h40, h31 ⊥ h41, h31 ⊥ h20, h31 ⊥ h30, h40 ⊥ h31, h40 ⊥ h41, h40 ⊥ h21, h41 ⊥ h20, h41 ⊥ h30, h41 ⊥ h40 ⊦ (h30 ∪ h31) ∪ h40 ∪ h41 = (h30 ∪ h40) ∪ h31 ∪ h41 ∧ h20 ⊥ (h30 ∪ h31) ∪ h40 ∪ h41 ∧ h21 ⊥ (h30 ∪ h31) ∪ h40 ∪ h41

Rule argument

Additional information

Used simplifier rules: disj-distr-uni: h1 ⊥ h ⊦ h0 ⊥ h1 ∪ h ↔ h0 ⊥ h1 ∧ h0 ⊥ h; disj-distr-uni-com: h1 ⊥ h2 ⊦ h1 ∪ h2 ⊥ h0 ↔ h0 ⊥ h1 ∧ h0 ⊥ h2; disj-com-rw: ⊦ h0 ⊥ h1 → h1 ⊥ h0;

Proof step 27 from proof union-split3 (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 28:

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

• Proof step 29:

  h20 ⊥ h41, h20 ⊥ h31, h20 ⊥ h21, h20 ⊥ h40, h20 ⊥ h30, h21 ⊥ h20, h21 ⊥ h41, h21 ⊥ h40, h21 ⊥ h31, h21 ⊥ h30, h30 ⊥ h21, h30 ⊥ h41, h30 ⊥ h40, h30 ⊥ h31, h31 ⊥ h30, h31 ⊥ h20, h31 ⊥ h41, h31 ⊥ h40, h31 ⊥ h40 ∪ h41, h40 ⊥ h21, h40 ⊥ h41, h40 ⊥ h31, h40 ∪ h41 ⊥ h30, h41 ⊥ h40, h41 ⊥ h30, h41 ⊥ h20 ⊦ h30 ∪ h31 ∪ h40 ∪ h41 = (h30 ∪ h40) ∪ h31 ∪ h41 ∧ h20 ⊥ h30 ∪ h31 ∪ h40 ∪ h41 ∧ h21 ⊥ h30 ∪ h31 ∪ h40 ∪ h41

Rule argument

Additional information

Used simplifier rules: disj-distr-uni: h1 ⊥ h ⊦ h0 ⊥ h1 ∪ h ↔ h0 ⊥ h1 ∧ h0 ⊥ h; disj-distr-uni-com: h1 ⊥ h2 ⊦ h1 ∪ h2 ⊥ h0 ↔ h0 ⊥ h1 ∧ h0 ⊥ h2; disj-com-rw: ⊦ h0 ⊥ h1 → h1 ⊥ h0; Used terms: h30, h31, h40 ∪ h41

Proof step 28 from proof union-split3 (previous step) (back to tree)

Lemma uni-ass

Proof step 29 from proof union-split3 (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 30:

  h30 ∪ h31 ∪ h40 ∪ h41 ≠ (h30 ∪ h40) ∪ h31 ∪ h41, h20 ⊥ h30, h20 ⊥ h40, h20 ⊥ h21, h20 ⊥ h31, h20 ⊥ h41, h21 ⊥ h30, h21 ⊥ h31, h21 ⊥ h40, h21 ⊥ h41, h21 ⊥ h20, h30 ⊥ h31, h30 ⊥ h40, h30 ⊥ h41, h30 ⊥ h21, h31 ⊥ h40, h31 ⊥ h41, h31 ⊥ h20, h31 ⊥ h30, h40 ⊥ h31, h40 ⊥ h41, h40 ⊥ h21, h41 ⊥ h20, h41 ⊥ h30, h41 ⊥ h40 ⊦

Rule argument

Additional information

Used simplifier rules: disj-distr-uni-com: h1 ⊥ h2 ⊦ h1 ∪ h2 ⊥ h0 ↔ h0 ⊥ h1 ∧ h0 ⊥ h2; disj-com-rw: ⊦ h0 ⊥ h1 → h1 ⊥ h0; disj-distr-uni: h1 ⊥ h ⊦ h0 ⊥ h1 ∪ h ↔ h0 ⊥ h1 ∧ h0 ⊥ h;

Proof step 30 from proof union-split3 (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 31:

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

• Proof step 32:

  h30 ∪ h31 ∪ h40 ∪ h41 ≠ h30 ∪ h40 ∪ h31 ∪ h41, h20 ⊥ h41, h20 ⊥ h31, h20 ⊥ h21, h20 ⊥ h40, h20 ⊥ h30, h21 ⊥ h20, h21 ⊥ h41, h21 ⊥ h40, h21 ⊥ h31, h21 ⊥ h30, h30 ⊥ h21, h30 ⊥ h41, h30 ⊥ h31, h30 ⊥ h40, h31 ⊥ h30, h31 ⊥ h20, h31 ⊥ h41, h31 ⊥ h40, h31 ∪ h41 ⊥ h30, h40 ⊥ h21, h40 ⊥ h41, h40 ⊥ h31, h40 ⊥ h31 ∪ h41, h41 ⊥ h40, h41 ⊥ h30, h41 ⊥ h20 ⊦

Rule argument

Additional information

Used simplifier rules: disj-distr-uni: h1 ⊥ h ⊦ h0 ⊥ h1 ∪ h ↔ h0 ⊥ h1 ∧ h0 ⊥ h; disj-distr-uni-com: h1 ⊥ h2 ⊦ h1 ∪ h2 ⊥ h0 ↔ h0 ⊥ h1 ∧ h0 ⊥ h2; disj-com-rw: ⊦ h0 ⊥ h1 → h1 ⊥ h0; Used terms: h30, h40, h31 ∪ h41

Proof step 31 from proof union-split3 (previous step) (back to tree)

Lemma uni-ass

Proof step 32 from proof union-split3 (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 33:

  h30 ∪ h31 ∪ h40 ∪ h41 ≠ h30 ∪ h40 ∪ h31 ∪ h41, h20 ⊥ h30, h20 ⊥ h40, h20 ⊥ h21, h20 ⊥ h31, h20 ⊥ h41, h21 ⊥ h30, h21 ⊥ h31, h21 ⊥ h40, h21 ⊥ h41, h21 ⊥ h20, h30 ⊥ h40, h30 ⊥ h31, h30 ⊥ h41, h30 ⊥ h21, h31 ⊥ h40, h31 ⊥ h41, h31 ⊥ h20, h31 ⊥ h30, h40 ⊥ h31, h40 ⊥ h41, h40 ⊥ h21, h41 ⊥ h20, h41 ⊥ h30, h41 ⊥ h40 ⊦

Rule argument

Additional information

Used simplifier rules: disj-distr-uni: h1 ⊥ h ⊦ h0 ⊥ h1 ∪ h ↔ h0 ⊥ h1 ∧ h0 ⊥ h; disj-distr-uni-com: h1 ⊥ h2 ⊦ h1 ∪ h2 ⊥ h0 ↔ h0 ⊥ h1 ∧ h0 ⊥ h2;

Proof step 33 from proof union-split3 (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 34:

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

Rule argument

Additional information

Used simplifier rules: disj-distr-uni: h1 ⊥ h ⊦ h0 ⊥ h1 ∪ h ↔ h0 ⊥ h1 ∧ h0 ⊥ h; disj-com-rw: ⊦ h0 ⊥ h1 → h1 ⊥ h0; disj-com-rw: ⊦ h0 ⊥ h1 → h1 ⊥ h0; uni-ac3-true: h0 ⊥ h1, h1 ⊥ h, h ⊥ h0 ⊦ h ∪ h0 ∪ h1 = h0 ∪ h ∪ h1 ↔ true; Used terms: h30, h31 ∪ h40 ∪ h41, h40 ∪ h31 ∪ h41

Proof step 34 from proof union-split3 (previous step) (back to tree)

Lemma uni-inj