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

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 2:

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

Rule argument

Additional information

Used simplifier rules: 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 2 from proof union-split2 (previous step) (back to tree)

User applied rule case distinction

And obtained the following new goals

• Proof step 3:

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

• Proof step 113:

  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 ⊥ h31 ∧ h30 ⊥ h21 ∧ h21 ⊥ h20 ∪ h30 ∧ h31 ⊥ h20 ∪ h30 ⊦

Rule argument

Additional information

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

User applied rule exists right

And obtained the following new goals

• Proof step 4:

  h0 ∪ h1 = h2 ∪ h3, h0 ⊥ h1, h2 ⊥ h3 ⊦ h2 = (h2 \ h1) ∪ (h2 \ h0) ∧ h3 = (h3 \ h1) ∪ (h3 \ h0) ∧ h0 = (h2 \ h1) ∪ (h3 \ h1) ∧ h1 = (h2 \ h0) ∪ (h3 \ h0) ∧ h2 \ h1 ⊥ h2 \ h0 ∧ h3 \ h1 ⊥ h3 \ h0 ∧ h2 \ h1 ⊥ h3 \ h0 ∧ h3 \ h1 ⊥ h2 \ h0 ∧ h2 \ h0 ⊥ (h2 \ h1) ∪ (h3 \ h1) ∧ h3 \ h0 ⊥ (h2 \ h1) ∪ (h3 \ h1)

Rule argument

Additional information

Used terms: h2 \ h1, h2 \ h0, h3 \ h1, h3 \ h0

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

User applied rule case distinction

And obtained the following new goals

• Proof step 5:

  h0 ∪ h1 = h2 ∪ h3, h2 ≠ (h2 \ h1) ∪ (h2 \ h0), h0 ⊥ h1, h2 ⊥ h3 ⊦

• Proof step 24:

  h0 ∪ h1 = h2 ∪ h3, h3 ≠ (h3 \ h1) ∪ (h3 \ h0), h0 ⊥ h1, h2 ⊥ h3 ⊦

• Proof step 43:

  h0 ∪ h1 = h2 ∪ h3, h0 ≠ (h2 \ h1) ∪ (h3 \ h1), h0 ⊥ h1, h2 ⊥ h3 ⊦

• Proof step 69:

  h0 ∪ h1 = h2 ∪ h3, h1 ≠ (h2 \ h0) ∪ (h3 \ h0), h0 ⊥ h1, h2 ⊥ h3 ⊦

• Proof step 97:

  h0 ∪ h1 = h2 ∪ h3, h0 ⊥ h1, h2 ⊥ h3, ¬ h2 \ h1 ⊥ h2 \ h0 ⊦

• Proof step 99:

  h0 ∪ h1 = h2 ∪ h3, h0 ⊥ h1, h2 ⊥ h3, ¬ h3 \ h1 ⊥ h3 \ h0 ⊦

• Proof step 101:

  h0 ∪ h1 = h2 ∪ h3, h0 ⊥ h1, h2 ⊥ h3, ¬ h2 \ h0 ⊥ (h2 \ h1) ∪ (h3 \ h1) ⊦

• Proof step 107:

  h0 ∪ h1 = h2 ∪ h3, h0 ⊥ h1, h2 ⊥ h3, ¬ h3 \ h0 ⊥ (h2 \ h1) ∪ (h3 \ h1) ⊦

Rule argument

Additional information

Used simplifier rules: disj-diffb: h0 ⊥ h1 ⊦ h0 \ h2 ⊥ h1 \ h3; disj-com-rw: ⊦ h0 ⊥ h1 → h1 ⊥ h0; disj-diffb: h0 ⊥ h1 ⊦ h0 \ h2 ⊥ h1 \ h3;

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

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 6:

  ⊦ h0 = h1 ↔ (∀ r. (r ∈ h0 ↔ r ∈ h1) ∧ (r ∈ h0 → h0(r) = h1(r)))

• Proof step 7:

  h0 ∪ h1 = h2 ∪ h3, h0 ⊥ h1, h2 ⊥ h3, ∃ r. ¬((r ∈ (h2 \ h1) ∪ (h2 \ h0) ↔ r ∈ h2) ∧ (r ∈ (h2 \ h1) ∪ (h2 \ h0) → ((h2 \ h1) ∪ (h2 \ h0))(r) = h2(r))) ⊦

Rule argument

Additional information

Used terms: h2, (h2 \ h1) ∪ (h2 \ h0)

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

A spec-lemma

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

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 8:

  h0 ∪ h1 = h2 ∪ h3, h0 ⊥ h1, h2 ⊥ h3 ⊦ (r ∈ (h2 \ h1) ∪ (h2 \ h0) ↔ r ∈ h2) ∧ (r ∈ (h2 \ h1) ∪ (h2 \ h0) → ((h2 \ h1) ∪ (h2 \ h0))(r) = h2(r))

Rule argument

Additional information

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

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 9:

  ⊦ h0 ⊥ h1 → (r ∈ h0 ∪ h1 ↔ r ∈ h0 ∨ r ∈ h1)

• Proof step 10:

  h0 ∪ h1 = h2 ∪ h3, h0 ⊥ h1, h2 ⊥ h3, ¬ h2 \ h1 ⊥ h2 \ h0 ⊦ (r ∈ (h2 \ h1) ∪ (h2 \ h0) ↔ r ∈ h2) ∧ (r ∈ (h2 \ h1) ∪ (h2 \ h0) → ((h2 \ h1) ∪ (h2 \ h0))(r) = h2(r))

• Proof step 12:

  h0 ∪ h1 = h2 ∪ h3, h0 ⊥ h1, h2 ⊥ h3, h2 \ h1 ⊥ h2 \ h0 ⊦ (r ∈ h2 \ h1 ∨ r ∈ h2 \ h0 ↔ r ∈ h2) ∧ (r ∈ h2 \ h1 ∨ r ∈ h2 \ h0 → ((h2 \ h1) ∪ (h2 \ h0))(r) = h2(r))

Rule argument

Additional information

Used terms: r, h2 \ h1, h2 \ h0

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

Lemma in-uni

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

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 11:

  h0 ⊥ h2 ⊦ h ⊆ h0 ∪ h2 → h \ h2 ⊥ h \ h0

Rule argument

Additional information

Used simplifier rules: subset-union: h0 ⊥ h1 ⊦ h0 ⊆ h0 ∪ h1; Used terms: h2, h1, h0

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

Lemma disj-union-diff

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

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 13:

  h0 ∪ h1 = h2 ∪ h3, h0 ⊥ h1, h2 \ h1 ⊥ h2 \ h0, h2 ⊥ h3 ⊦ (r ∈ h2 \ h1 ∨ r ∈ h2 \ h0 ↔ r ∈ h2) ∧ (r ∈ h2 \ h1 ∨ r ∈ h2 \ h0 → (r ∈ h2 \ h1 ⊃ h2(r);(h2 \ h0)(r)) = h2(r))

Rule argument

Additional information

Used simplifier rules: in-uni: ⊦ h0 ⊥ h1 → (r ∈ h0 ∪ h1 ↔ r ∈ h0 ∨ r ∈ h1); at-uni: r ∈ h0 ∪ h1 ⊦ h0 ⊥ h1 → (h0 ∪ h1)(r) = (r ∈ h0 ⊃ h0(r);h1(r)); diff-in: ⊦ r ∈ h0 \ h1 ↔ r ∈ h0 ∧ ¬ r ∈ h1; diff-at: r ∈ h0, ¬ r ∈ h1 ⊦ (h0 \ h1)(r) = h0(r);

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

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 14:

  ⊦ r ∈ h0 \ h1 ↔ r ∈ h0 ∧ ¬ r ∈ h1

• Proof step 15:

  h0 ∪ h1 = h2 ∪ h3, h0 ⊥ h1, h2 ⊥ h3, h2 \ h1 ⊥ h2 \ h0 ⊦ (r ∈ h2 ∧ ¬ r ∈ h1 ∨ r ∈ h2 \ h0 ↔ r ∈ h2) ∧ (r ∈ h2 ∧ ¬ r ∈ h1 ∨ r ∈ h2 \ h0 → (r ∈ h2 ∧ ¬ r ∈ h1 ⊃ h2(r);(h2 \ h0)(r)) = h2(r))

Rule argument

Additional information

Used terms: r, h2, h1

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

Lemma diff-in

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

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 16:

  ⊦ r ∈ h0 \ h1 ↔ r ∈ h0 ∧ ¬ r ∈ h1

• Proof step 17:

  h0 ∪ h1 = h2 ∪ h3, h0 ⊥ h1, h2 \ h1 ⊥ h2 \ h0, h2 ⊥ h3 ⊦ (r ∈ h2 ∧ ¬ r ∈ h1 ∨ r ∈ h2 ∧ ¬ r ∈ h0 ↔ r ∈ h2) ∧ (r ∈ h2 ∧ ¬ r ∈ h1 ∨ r ∈ h2 ∧ ¬ r ∈ h0 → (r ∈ h2 ∧ ¬ r ∈ h1 ⊃ h2(r);(h2 \ h0)(r)) = h2(r))

Rule argument

Additional information

Used terms: r, h2, h0

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

Lemma diff-in

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

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 18:

  h0 ∪ h1 = h2 ∪ h3, (r ∈ h2 ∧ ¬ r ∈ h1 ⊃ h2(r);(h2 \ h0)(r)) ≠ h2(r), h0 ⊥ h1, h2 ⊥ h3, h2 \ h1 ⊥ h2 \ h0, r ∈ h2 ∧ ¬ r ∈ h1 ∨ r ∈ h2 ∧ ¬ r ∈ h0 ⊦

Rule argument

Additional information

Used simplifier rules: disj-r: ⊦ r ∈ h1 ∧ h0 ⊥ h1 → ¬ r ∈ h0;

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

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 19:

  ⊦ h0 = h1 ↔ (∀ r. (r ∈ h0 ↔ r ∈ h1) ∧ (r ∈ h0 → h0(r) = h1(r)))

• Proof step 20:

  (r ∈ h2 ∧ ¬ r ∈ h1 ⊃ h2(r);(h2 \ h0)(r)) ≠ h2(r), h0 ⊥ h1, h2 \ h1 ⊥ h2 \ h0, h2 ⊥ h3, r ∈ h2 ∧ ¬ r ∈ h1 ∨ r ∈ h2 ∧ ¬ r ∈ h0, ∀ r. (r ∈ h2 ∪ h3 ↔ r ∈ h0 ∪ h1) ∧ (r ∈ h2 ∪ h3 → (h2 ∪ h3)(r) = (h0 ∪ h1)(r)) ⊦

Rule argument

Additional information

Used terms: h0 ∪ h1, h2 ∪ h3

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

A spec-lemma

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

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 21:

  (r ∈ h2 ∧ ¬ r ∈ h1 ⊃ h2(r);(h2 \ h0)(r)) ≠ h2(r), h0 ⊥ h1, h2 ⊥ h3, h2 \ h1 ⊥ h2 \ h0, r ∈ h2 ∧ ¬ r ∈ h1 ∨ r ∈ h2 ∧ ¬ r ∈ h0, ∀ r0. (r0 ∈ h2 ∨ r0 ∈ h3 ↔ r0 ∈ h0 ∨ r0 ∈ h1) ∧ (r0 ∈ h2 ∨ r0 ∈ h3 → (r0 ∈ h2 ⊃ h2(r0);h3(r0)) = (h0 ∪ h1)(r0)) ⊦

Rule argument

Additional information

Used simplifier rules: in-uni: ⊦ h0 ⊥ h1 → (r ∈ h0 ∪ h1 ↔ r ∈ h0 ∨ r ∈ h1); at-uni: r ∈ h0 ∪ h1 ⊦ h0 ⊥ h1 → (h0 ∪ h1)(r) = (r ∈ h0 ⊃ h0(r);h1(r));

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

User applied rule all left

And obtained the following new goals

• Proof step 22:

  r ∈ h2 ∨ r ∈ h3 ↔ r ∈ h0 ∨ r ∈ h1, (r ∈ h2 ∧ ¬ r ∈ h1 ⊃ h2(r);(h2 \ h0)(r)) ≠ h2(r), h0 ⊥ h1, h2 \ h1 ⊥ h2 \ h0, h2 ⊥ h3, r ∈ h2 ∧ ¬ r ∈ h1 ∨ r ∈ h2 ∧ ¬ r ∈ h0, r ∈ h2 ∨ r ∈ h3 → (r ∈ h2 ⊃ h2(r);h3(r)) = (h0 ∪ h1)(r) ⊦

Rule argument

Additional information

Used terms: r

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

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 23:

  r ∈ h2 ∨ r ∈ h3 ↔ r ∈ h0 ∨ r ∈ h1, (r ∈ h2 ∧ ¬ r ∈ h1 ⊃ h2(r);(h2 \ h0)(r)) ≠ h2(r), h0 ⊥ h1, h2 \ h1 ⊥ h2 \ h0, h2 ⊥ h3, r ∈ h2 ∧ ¬ r ∈ h1 ∨ r ∈ h2 ∧ ¬ r ∈ h0, r ∈ h0 ∨ r ∈ h1 → (r ∈ h2 ⊃ h2(r);h3(r)) = (r ∈ h0 ⊃ h0(r);h1(r)) ⊦

Rule argument

Additional information

Used simplifier rules: in-uni: ⊦ h0 ⊥ h1 → (r ∈ h0 ∪ h1 ↔ r ∈ h0 ∨ r ∈ h1); at-uni: r ∈ h0 ∪ h1 ⊦ h0 ⊥ h1 → (h0 ∪ h1)(r) = (r ∈ h0 ⊃ h0(r);h1(r));

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

User applied rule case distinction

And closed the goal!

Rule argument

Additional information

Used simplifier rules: disj-l: ⊦ r ∈ h0 ∧ h0 ⊥ h1 → ¬ r ∈ h1; disj-r: ⊦ r ∈ h1 ∧ h0 ⊥ h1 → ¬ r ∈ h0; diff-at: r ∈ h0, ¬ r ∈ h1 ⊦ (h0 \ h1)(r) = h0(r);

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

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 25:

  ⊦ h0 = h1 ↔ (∀ r. (r ∈ h0 ↔ r ∈ h1) ∧ (r ∈ h0 → h0(r) = h1(r)))

• Proof step 26:

  h0 ∪ h1 = h2 ∪ h3, h0 ⊥ h1, h2 ⊥ h3, ∃ r. ¬((r ∈ h3 ↔ r ∈ (h3 \ h1) ∪ (h3 \ h0)) ∧ (r ∈ h3 → h3(r) = ((h3 \ h1) ∪ (h3 \ h0))(r))) ⊦

Rule argument

Additional information

Used terms: h3, (h3 \ h1) ∪ (h3 \ h0)

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

A spec-lemma

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

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 27:

  h0 ∪ h1 = h2 ∪ h3, h0 ⊥ h1, h2 ⊥ h3 ⊦ (r ∈ h3 ↔ r ∈ (h3 \ h1) ∪ (h3 \ h0)) ∧ (r ∈ h3 → h3(r) = ((h3 \ h1) ∪ (h3 \ h0))(r))

Rule argument

Additional information

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

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 28:

  ⊦ h0 ⊥ h1 → (r ∈ h0 ∪ h1 ↔ r ∈ h0 ∨ r ∈ h1)

• Proof step 29:

  h0 ∪ h1 = h2 ∪ h3, h0 ⊥ h1, h2 ⊥ h3, ¬ h3 \ h1 ⊥ h3 \ h0 ⊦ (r ∈ h3 ↔ r ∈ (h3 \ h1) ∪ (h3 \ h0)) ∧ (r ∈ h3 → h3(r) = ((h3 \ h1) ∪ (h3 \ h0))(r))

• Proof step 31:

  h0 ∪ h1 = h2 ∪ h3, h0 ⊥ h1, h2 ⊥ h3, h3 \ h1 ⊥ h3 \ h0 ⊦ (r ∈ h3 ↔ r ∈ h3 \ h1 ∨ r ∈ h3 \ h0) ∧ (r ∈ h3 → h3(r) = ((h3 \ h1) ∪ (h3 \ h0))(r))

Rule argument

Additional information

Used terms: r, h3 \ h1, h3 \ h0

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

Lemma in-uni

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

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 30:

  h0 ⊥ h2 ⊦ h ⊆ h0 ∪ h2 → h \ h2 ⊥ h \ h0

Rule argument

Additional information

Used simplifier rules: disj-com-rw: ⊦ h0 ⊥ h1 → h1 ⊥ h0; subset-union2: h1 ⊥ h0 ⊦ h1 ⊆ h0 ∪ h1; Used terms: h3, h1, h0

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

Lemma disj-union-diff

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

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 32:

  ⊦ h0 = h1 ↔ (∀ r. (r ∈ h0 ↔ r ∈ h1) ∧ (r ∈ h0 → h0(r) = h1(r)))

• Proof step 33:

  h0 ⊥ h1, h2 ⊥ h3, h3 \ h1 ⊥ h3 \ h0, ∀ r. (r ∈ h2 ∪ h3 ↔ r ∈ h0 ∪ h1) ∧ (r ∈ h2 ∪ h3 → (h2 ∪ h3)(r) = (h0 ∪ h1)(r)) ⊦ (r ∈ h3 ↔ r ∈ h3 \ h1 ∨ r ∈ h3 \ h0) ∧ (r ∈ h3 → h3(r) = ((h3 \ h1) ∪ (h3 \ h0))(r))

Rule argument

Additional information

Used terms: h0 ∪ h1, h2 ∪ h3

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

A spec-lemma

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

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 34:

  h0 ⊥ h1, h2 ⊥ h3, h3 \ h1 ⊥ h3 \ h0, ∀ r0. (r0 ∈ h2 ∨ r0 ∈ h3 ↔ r0 ∈ h0 ∨ r0 ∈ h1) ∧ (r0 ∈ h2 ∨ r0 ∈ h3 → (r0 ∈ h2 ⊃ h2(r0);h3(r0)) = (h0 ∪ h1)(r0)) ⊦ (r ∈ h3 ↔ r ∈ h3 \ h1 ∨ r ∈ h3 \ h0) ∧ (r ∈ h3 → h3(r) = ((h3 \ h1) ∪ (h3 \ h0))(r))

Rule argument

Additional information

Used simplifier rules: in-uni: ⊦ h0 ⊥ h1 → (r ∈ h0 ∪ h1 ↔ r ∈ h0 ∨ r ∈ h1); at-uni: r ∈ h0 ∪ h1 ⊦ h0 ⊥ h1 → (h0 ∪ h1)(r) = (r ∈ h0 ⊃ h0(r);h1(r));

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

User applied rule all left

And obtained the following new goals

• Proof step 35:

  r ∈ h2 ∨ r ∈ h3 ↔ r ∈ h0 ∨ r ∈ h1, h0 ⊥ h1, h2 ⊥ h3, h3 \ h1 ⊥ h3 \ h0, r ∈ h2 ∨ r ∈ h3 → (r ∈ h2 ⊃ h2(r);h3(r)) = (h0 ∪ h1)(r) ⊦ (r ∈ h3 ↔ r ∈ h3 \ h1 ∨ r ∈ h3 \ h0) ∧ (r ∈ h3 → h3(r) = ((h3 \ h1) ∪ (h3 \ h0))(r))

Rule argument

Additional information

Used terms: r

Proof step 35 from proof union-split2 (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 36:

  r ∈ h2 ∨ r ∈ h3 ↔ r ∈ h0 ∨ r ∈ h1, h0 ⊥ h1, h2 ⊥ h3, h3 \ h1 ⊥ h3 \ h0, r ∈ h0 ∨ r ∈ h1 → (r ∈ h2 ⊃ h2(r);h3(r)) = (r ∈ h0 ⊃ h0(r);h1(r)) ⊦ (r ∈ h3 ↔ r ∈ h3 \ h1 ∨ r ∈ h3 \ h0) ∧ (r ∈ h3 → h3(r) = ((h3 \ h1) ∪ (h3 \ h0))(r))

Rule argument

Additional information

Used simplifier rules: in-uni: ⊦ h0 ⊥ h1 → (r ∈ h0 ∪ h1 ↔ r ∈ h0 ∨ r ∈ h1); at-uni: r ∈ h0 ∪ h1 ⊦ h0 ⊥ h1 → (h0 ∪ h1)(r) = (r ∈ h0 ⊃ h0(r);h1(r));

Proof step 36 from proof union-split2 (previous step) (back to tree)

User applied rule cut formula

And obtained the following new goals

• Proof step 37:

  r ∈ h2 ∨ r ∈ h3 ↔ r ∈ h0 ∨ r ∈ h1, ¬(r ∈ h3 ↔ r ∈ h3 \ h1 ∨ r ∈ h3 \ h0), h0 ⊥ h1, h2 ⊥ h3, h3 \ h1 ⊥ h3 \ h0, r ∈ h0 ∨ r ∈ h1 → (r ∈ h2 ⊃ h2(r);h3(r)) = (r ∈ h0 ⊃ h0(r);h1(r)) ⊦ (r ∈ h3 ↔ r ∈ h3 \ h1 ∨ r ∈ h3 \ h0) ∧ (r ∈ h3 → h3(r) = ((h3 \ h1) ∪ (h3 \ h0))(r))

Rule argument

Additional information

Used simplifier rules: in-uni: ⊦ h0 ⊥ h1 → (r ∈ h0 ∪ h1 ↔ r ∈ h0 ∨ r ∈ h1); at-uni: r ∈ h0 ∪ h1 ⊦ h0 ⊥ h1 → (h0 ∪ h1)(r) = (r ∈ h0 ⊃ h0(r);h1(r)); disj-r: ⊦ r ∈ h1 ∧ h0 ⊥ h1 → ¬ r ∈ h0; diff-at: r ∈ h0, ¬ r ∈ h1 ⊦ (h0 \ h1)(r) = h0(r); diff-in: ⊦ r ∈ h0 \ h1 ↔ r ∈ h0 ∧ ¬ r ∈ h1; Used formulas: r ∈ h3 ↔ r ∈ h3 \ h1 ∨ r ∈ h3 \ h0

Proof step 37 from proof union-split2 (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 38:

  r ∈ h2 ∨ r ∈ h3 ↔ r ∈ h0 ∨ r ∈ h1, ¬(r ∈ h3 ↔ r ∈ h3 \ h1 ∨ r ∈ h3 \ h0), h0 ⊥ h1, h2 ⊥ h3, h3 \ h1 ⊥ h3 \ h0, r ∈ h0 ∨ r ∈ h1 → (r ∈ h2 ⊃ h2(r);h3(r)) = (r ∈ h0 ⊃ h0(r);h1(r)) ⊦

Rule argument

Additional information

Proof step 38 from proof union-split2 (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 39:

  ⊦ r ∈ h0 \ h1 ↔ r ∈ h0 ∧ ¬ r ∈ h1

• Proof step 40:

  r ∈ h2 ∨ r ∈ h3 ↔ r ∈ h0 ∨ r ∈ h1, ¬(r ∈ h3 ↔ r ∈ h3 \ h1 ∨ r ∈ h3 ∧ ¬ r ∈ h0), h0 ⊥ h1, h2 ⊥ h3, h3 \ h1 ⊥ h3 \ h0, r ∈ h0 ∨ r ∈ h1 → (r ∈ h2 ⊃ h2(r);h3(r)) = (r ∈ h0 ⊃ h0(r);h1(r)) ⊦

Rule argument

Additional information

Used terms: r, h3, h0

Proof step 39 from proof union-split2 (previous step) (back to tree)

Lemma diff-in

Proof step 40 from proof union-split2 (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 41:

  r ∈ h2 ∨ r ∈ h3 ↔ r ∈ h0 ∨ r ∈ h1, ¬(r ∈ h3 ↔ r ∈ h3 \ h1 ∨ r ∈ h3 ∧ ¬ r ∈ h0), h0 ⊥ h1, h2 ⊥ h3, h3 \ h1 ⊥ h3 \ h0, r ∈ h0 ∨ r ∈ h1 → h3(r) = h0(r) ⊦

Rule argument

Additional information

Used simplifier rules: disj-l: ⊦ r ∈ h0 ∧ h0 ⊥ h1 → ¬ r ∈ h1; diff-in: ⊦ r ∈ h0 \ h1 ↔ r ∈ h0 ∧ ¬ r ∈ h1;

Proof step 41 from proof union-split2 (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 42:

  ⊦ r ∈ h0 \ h1 ↔ r ∈ h0 ∧ ¬ r ∈ h1

Rule argument

Additional information

Used simplifier rules: disj-r: ⊦ r ∈ h1 ∧ h0 ⊥ h1 → ¬ r ∈ h0; Used terms: r, h3, h1

Proof step 42 from proof union-split2 (previous step) (back to tree)

Lemma diff-in

Proof step 43 from proof union-split2 (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 44:

  ⊦ h0 = h1 ↔ (∀ r. (r ∈ h0 ↔ r ∈ h1) ∧ (r ∈ h0 → h0(r) = h1(r)))

• Proof step 45:

  h0 ∪ h1 = h2 ∪ h3, h0 ⊥ h1, h2 ⊥ h3, ∃ r. ¬((r ∈ h0 ↔ r ∈ (h2 \ h1) ∪ (h3 \ h1)) ∧ (r ∈ h0 → h0(r) = ((h2 \ h1) ∪ (h3 \ h1))(r))) ⊦

Rule argument

Additional information

Used terms: h0, (h2 \ h1) ∪ (h3 \ h1)

Proof step 44 from proof union-split2 (previous step) (back to tree)

A spec-lemma

Proof step 45 from proof union-split2 (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 46:

  h0 ∪ h1 = h2 ∪ h3, h0 ⊥ h1, h2 ⊥ h3 ⊦ (r ∈ h0 ↔ r ∈ (h2 \ h1) ∪ (h3 \ h1)) ∧ (r ∈ h0 → h0(r) = ((h2 \ h1) ∪ (h3 \ h1))(r))

Rule argument

Additional information

Proof step 46 from proof union-split2 (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 47:

  ⊦ h0 ⊥ h1 → (r ∈ h0 ∪ h1 ↔ r ∈ h0 ∨ r ∈ h1)

• Proof step 48:

  h0 ∪ h1 = h2 ∪ h3, h0 ⊥ h1, h2 ⊥ h3, h2 \ h1 ⊥ h3 \ h1 ⊦ (r ∈ h0 ↔ r ∈ h2 \ h1 ∨ r ∈ h3 \ h1) ∧ (r ∈ h0 → h0(r) = ((h2 \ h1) ∪ (h3 \ h1))(r))

Rule argument

Additional information

Used simplifier rules: disj-diffb: h0 ⊥ h1 ⊦ h0 \ h2 ⊥ h1 \ h3; Used terms: r, h2 \ h1, h3 \ h1

Proof step 47 from proof union-split2 (previous step) (back to tree)

Lemma in-uni

Proof step 48 from proof union-split2 (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 49:

  h0 ∪ h1 = h2 ∪ h3, h0 ⊥ h1, h2 ⊥ h3 ⊦ (r ∈ h0 ↔ r ∈ h2 \ h1 ∨ r ∈ h3 \ h1) ∧ (r ∈ h0 → h0(r) = ((h2 \ h1) ∪ (h3 \ h1))(r))

Rule argument

Additional information

Used simplifier rules: disj-diffb: h0 ⊥ h1 ⊦ h0 \ h2 ⊥ h1 \ h3;

Proof step 49 from proof union-split2 (previous step) (back to tree)

User applied rule cut formula

And obtained the following new goals

• Proof step 50:

  h0 ∪ h1 = h2 ∪ h3, r ∈ h0 ↔ r ∈ h2 \ h1 ∨ r ∈ h3 \ h1, h0 ⊥ h1, h2 ⊥ h3 ⊦ (r ∈ h0 ↔ r ∈ h2 \ h1 ∨ r ∈ h3 \ h1) ∧ (r ∈ h0 → h0(r) = ((h2 \ h1) ∪ (h3 \ h1))(r))

• Proof step 58:

  h0 ∪ h1 = h2 ∪ h3, ¬(r ∈ h0 ↔ r ∈ h2 \ h1 ∨ r ∈ h3 \ h1), h0 ⊥ h1, h2 ⊥ h3 ⊦ (r ∈ h0 ↔ r ∈ h2 \ h1 ∨ r ∈ h3 \ h1) ∧ (r ∈ h0 → h0(r) = ((h2 \ h1) ∪ (h3 \ h1))(r))

Rule argument

Additional information

Used formulas: r ∈ h0 ↔ r ∈ h2 \ h1 ∨ r ∈ h3 \ h1

Proof step 50 from proof union-split2 (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 51:

  h0 ∪ h1 = h2 ∪ h3, h0(r) ≠ ((h2 \ h1) ∪ (h3 \ h1))(r), h0 ⊥ h1, h2 ⊥ h3, r ∈ h0, r ∈ h2 \ h1 ∨ r ∈ h3 \ h1 ⊦

Rule argument

Additional information

Proof step 51 from proof union-split2 (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 52:

  ⊦ h0 = h1 ↔ (∀ r. (r ∈ h0 ↔ r ∈ h1) ∧ (r ∈ h0 → h0(r) = h1(r)))

• Proof step 53:

  h0(r) ≠ ((h2 \ h1) ∪ (h3 \ h1))(r), h0 ⊥ h1, h2 ⊥ h3, r ∈ h0, r ∈ h2 \ h1 ∨ r ∈ h3 \ h1, ∀ r. (r ∈ h2 ∪ h3 ↔ r ∈ h0 ∪ h1) ∧ (r ∈ h2 ∪ h3 → (h2 ∪ h3)(r) = (h0 ∪ h1)(r)) ⊦

Rule argument

Additional information

Used terms: h0 ∪ h1, h2 ∪ h3

Proof step 52 from proof union-split2 (previous step) (back to tree)

A spec-lemma

Proof step 53 from proof union-split2 (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 54:

  h0(r) ≠ ((h2 \ h1) ∪ (h3 \ h1))(r), h0 ⊥ h1, h2 ⊥ h3, r ∈ h0, r ∈ h2 \ h1 ∨ r ∈ h3 \ h1, ∀ r0. (r0 ∈ h2 ∨ r0 ∈ h3 ↔ r0 ∈ h0 ∨ r0 ∈ h1) ∧ (r0 ∈ h2 ∨ r0 ∈ h3 → (r0 ∈ h2 ⊃ h2(r0);h3(r0)) = (h0 ∪ h1)(r0)) ⊦

Rule argument

Additional information

Used simplifier rules: in-uni: ⊦ h0 ⊥ h1 → (r ∈ h0 ∪ h1 ↔ r ∈ h0 ∨ r ∈ h1); at-uni: r ∈ h0 ∪ h1 ⊦ h0 ⊥ h1 → (h0 ∪ h1)(r) = (r ∈ h0 ⊃ h0(r);h1(r));

Proof step 54 from proof union-split2 (previous step) (back to tree)

User applied rule all left

And obtained the following new goals

• Proof step 55:

  r ∈ h2 ∨ r ∈ h3 ↔ r ∈ h0 ∨ r ∈ h1, h0(r) ≠ ((h2 \ h1) ∪ (h3 \ h1))(r), h0 ⊥ h1, h2 ⊥ h3, r ∈ h0, r ∈ h2 \ h1 ∨ r ∈ h3 \ h1, r ∈ h2 ∨ r ∈ h3 → (r ∈ h2 ⊃ h2(r);h3(r)) = (h0 ∪ h1)(r) ⊦

Rule argument

Additional information

Used terms: r

Proof step 55 from proof union-split2 (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 56:

  (r ∈ h2 ⊃ h2(r);h3(r)) = h0(r), h0(r) ≠ ((h2 \ h1) ∪ (h3 \ h1))(r), h0 ⊥ h1, h2 ⊥ h3, r ∈ h0, r ∈ h2 \ h1 ∨ r ∈ h3 \ h1, r ∈ h2 ∨ r ∈ h3 ⊦

Rule argument

Additional information

Used simplifier rules: in-uni: ⊦ h0 ⊥ h1 → (r ∈ h0 ∪ h1 ↔ r ∈ h0 ∨ r ∈ h1); at-uni: r ∈ h0 ∪ h1 ⊦ h0 ⊥ h1 → (h0 ∪ h1)(r) = (r ∈ h0 ⊃ h0(r);h1(r));

Proof step 56 from proof union-split2 (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 57:

  r ∈ h0 ∪ h1 ⊦ h0 ⊥ h1 → (h0 ∪ h1)(r) = (r ∈ h0 ⊃ h0(r);h1(r))

Rule argument

Additional information

Used simplifier rules: in-uni: ⊦ h0 ⊥ h1 → (r ∈ h0 ∪ h1 ↔ r ∈ h0 ∨ r ∈ h1); disj-diffb: h0 ⊥ h1 ⊦ h0 \ h2 ⊥ h1 \ h3; in-uni: ⊦ h0 ⊥ h1 → (r ∈ h0 ∪ h1 ↔ r ∈ h0 ∨ r ∈ h1); disj-diffb: h0 ⊥ h1 ⊦ h0 \ h2 ⊥ h1 \ h3; disj-l: ⊦ r ∈ h0 ∧ h0 ⊥ h1 → ¬ r ∈ h1; diff-in: ⊦ r ∈ h0 \ h1 ↔ r ∈ h0 ∧ ¬ r ∈ h1; diff-at: r ∈ h0, ¬ r ∈ h1 ⊦ (h0 \ h1)(r) = h0(r); Used terms: h2 \ h1, h3 \ h1, r

Proof step 57 from proof union-split2 (previous step) (back to tree)

Lemma at-uni

Proof step 58 from proof union-split2 (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 59:

  h0 ∪ h1 = h2 ∪ h3, ¬(r ∈ h0 ↔ r ∈ h2 \ h1 ∨ r ∈ h3 \ h1), h0 ⊥ h1, h2 ⊥ h3 ⊦

Rule argument

Additional information

Proof step 59 from proof union-split2 (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 60:

  ⊦ h0 = h1 ↔ (∀ r. (r ∈ h0 ↔ r ∈ h1) ∧ (r ∈ h0 → h0(r) = h1(r)))

• Proof step 61:

  ¬(r ∈ h0 ↔ r ∈ h2 \ h1 ∨ r ∈ h3 \ h1), h0 ⊥ h1, h2 ⊥ h3, ∀ r. (r ∈ h2 ∪ h3 ↔ r ∈ h0 ∪ h1) ∧ (r ∈ h2 ∪ h3 → (h2 ∪ h3)(r) = (h0 ∪ h1)(r)) ⊦

Rule argument

Additional information

Used terms: h0 ∪ h1, h2 ∪ h3

Proof step 60 from proof union-split2 (previous step) (back to tree)

A spec-lemma

Proof step 61 from proof union-split2 (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 62:

  ¬(r ∈ h0 ↔ r ∈ h2 \ h1 ∨ r ∈ h3 \ h1), h0 ⊥ h1, h2 ⊥ h3, ∀ r0. (r0 ∈ h2 ∨ r0 ∈ h3 ↔ r0 ∈ h0 ∨ r0 ∈ h1) ∧ (r0 ∈ h2 ∨ r0 ∈ h3 → (r0 ∈ h2 ⊃ h2(r0);h3(r0)) = (h0 ∪ h1)(r0)) ⊦

Rule argument

Additional information

Used simplifier rules: in-uni: ⊦ h0 ⊥ h1 → (r ∈ h0 ∪ h1 ↔ r ∈ h0 ∨ r ∈ h1); at-uni: r ∈ h0 ∪ h1 ⊦ h0 ⊥ h1 → (h0 ∪ h1)(r) = (r ∈ h0 ⊃ h0(r);h1(r));

Proof step 62 from proof union-split2 (previous step) (back to tree)

User applied rule all left

And obtained the following new goals

• Proof step 63:

  r ∈ h2 ∨ r ∈ h3 ↔ r ∈ h0 ∨ r ∈ h1, ¬(r ∈ h0 ↔ r ∈ h2 \ h1 ∨ r ∈ h3 \ h1), h0 ⊥ h1, h2 ⊥ h3, r ∈ h2 ∨ r ∈ h3 → (r ∈ h2 ⊃ h2(r);h3(r)) = (h0 ∪ h1)(r) ⊦

Rule argument

Additional information

Used terms: r

Proof step 63 from proof union-split2 (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 64:

  r ∈ h2 ∨ r ∈ h3 ↔ r ∈ h0 ∨ r ∈ h1, ¬(r ∈ h0 ↔ r ∈ h2 \ h1 ∨ r ∈ h3 \ h1), h0 ⊥ h1, h2 ⊥ h3, r ∈ h0 ∨ r ∈ h1 → (r ∈ h2 ⊃ h2(r);h3(r)) = (r ∈ h0 ⊃ h0(r);h1(r)) ⊦

Rule argument

Additional information

Used simplifier rules: in-uni: ⊦ h0 ⊥ h1 → (r ∈ h0 ∪ h1 ↔ r ∈ h0 ∨ r ∈ h1); at-uni: r ∈ h0 ∪ h1 ⊦ h0 ⊥ h1 → (h0 ∪ h1)(r) = (r ∈ h0 ⊃ h0(r);h1(r));

Proof step 64 from proof union-split2 (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 65:

  ⊦ r ∈ h0 \ h1 ↔ r ∈ h0 ∧ ¬ r ∈ h1

• Proof step 66:

  r ∈ h2 ∨ r ∈ h3 ↔ r ∈ h0 ∨ r ∈ h1, ¬(r ∈ h0 ↔ r ∈ h2 ∧ ¬ r ∈ h1 ∨ r ∈ h3 \ h1), h0 ⊥ h1, h2 ⊥ h3, r ∈ h0 ∨ r ∈ h1 → (r ∈ h2 ⊃ h2(r);h3(r)) = (r ∈ h0 ⊃ h0(r);h1(r)) ⊦

Rule argument

Additional information

Used terms: r, h2, h1

Proof step 65 from proof union-split2 (previous step) (back to tree)

Lemma diff-in

Proof step 66 from proof union-split2 (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 67:

  ⊦ r ∈ h0 \ h1 ↔ r ∈ h0 ∧ ¬ r ∈ h1

• Proof step 68:

  r ∈ h2 ∨ r ∈ h3 ↔ r ∈ h0 ∨ r ∈ h1, ¬(r ∈ h0 ↔ r ∈ h2 ∧ ¬ r ∈ h1 ∨ r ∈ h3 ∧ ¬ r ∈ h1), h0 ⊥ h1, h2 ⊥ h3, r ∈ h0 ∨ r ∈ h1 → (r ∈ h2 ⊃ h2(r);h3(r)) = (r ∈ h0 ⊃ h0(r);h1(r)) ⊦

Rule argument

Additional information

Used terms: r, h3, h1

Proof step 67 from proof union-split2 (previous step) (back to tree)

Lemma diff-in

Proof step 68 from proof union-split2 (previous step) (back to tree)

User applied rule case distinction

And closed the goal!

Rule argument

Additional information

Used simplifier rules: disj-r: ⊦ r ∈ h1 ∧ h0 ⊥ h1 → ¬ r ∈ h0; disj-l: ⊦ r ∈ h0 ∧ h0 ⊥ h1 → ¬ r ∈ h1;

Proof step 69 from proof union-split2 (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 70:

  ⊦ h0 = h1 ↔ (∀ r. (r ∈ h0 ↔ r ∈ h1) ∧ (r ∈ h0 → h0(r) = h1(r)))

• Proof step 71:

  h0 ∪ h1 = h2 ∪ h3, h0 ⊥ h1, h2 ⊥ h3, ∃ r. ¬((r ∈ h1 ↔ r ∈ (h2 \ h0) ∪ (h3 \ h0)) ∧ (r ∈ h1 → h1(r) = ((h2 \ h0) ∪ (h3 \ h0))(r))) ⊦

Rule argument

Additional information

Used terms: h1, (h2 \ h0) ∪ (h3 \ h0)

Proof step 70 from proof union-split2 (previous step) (back to tree)

A spec-lemma

Proof step 71 from proof union-split2 (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 72:

  h0 ∪ h1 = h2 ∪ h3, h0 ⊥ h1, h2 ⊥ h3 ⊦ (r ∈ h1 ↔ r ∈ (h2 \ h0) ∪ (h3 \ h0)) ∧ (r ∈ h1 → h1(r) = ((h2 \ h0) ∪ (h3 \ h0))(r))

Rule argument

Additional information

Proof step 72 from proof union-split2 (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 73:

  ⊦ h0 ⊥ h1 → (r ∈ h0 ∪ h1 ↔ r ∈ h0 ∨ r ∈ h1)

• Proof step 74:

  h0 ∪ h1 = h2 ∪ h3, h0 ⊥ h1, h2 ⊥ h3, h2 \ h0 ⊥ h3 \ h0 ⊦ (r ∈ h1 ↔ r ∈ h2 \ h0 ∨ r ∈ h3 \ h0) ∧ (r ∈ h1 → h1(r) = ((h2 \ h0) ∪ (h3 \ h0))(r))

Rule argument

Additional information

Used simplifier rules: disj-diffb: h0 ⊥ h1 ⊦ h0 \ h2 ⊥ h1 \ h3; Used terms: r, h2 \ h0, h3 \ h0

Proof step 73 from proof union-split2 (previous step) (back to tree)

Lemma in-uni

Proof step 74 from proof union-split2 (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 75:

  h0 ∪ h1 = h2 ∪ h3, h0 ⊥ h1, h2 ⊥ h3 ⊦ (r ∈ h1 ↔ r ∈ h2 \ h0 ∨ r ∈ h3 \ h0) ∧ (r ∈ h1 → h1(r) = ((h2 \ h0) ∪ (h3 \ h0))(r))

Rule argument

Additional information

Used simplifier rules: disj-diffb: h0 ⊥ h1 ⊦ h0 \ h2 ⊥ h1 \ h3;

Proof step 75 from proof union-split2 (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 76:

  ⊦ h0 = h1 ↔ (∀ r. (r ∈ h0 ↔ r ∈ h1) ∧ (r ∈ h0 → h0(r) = h1(r)))

• Proof step 77:

  h0 ⊥ h1, h2 ⊥ h3, ∀ r. (r ∈ h2 ∪ h3 ↔ r ∈ h0 ∪ h1) ∧ (r ∈ h2 ∪ h3 → (h2 ∪ h3)(r) = (h0 ∪ h1)(r)) ⊦ (r ∈ h1 ↔ r ∈ h2 \ h0 ∨ r ∈ h3 \ h0) ∧ (r ∈ h1 → h1(r) = ((h2 \ h0) ∪ (h3 \ h0))(r))

Rule argument

Additional information

Used terms: h0 ∪ h1, h2 ∪ h3

Proof step 76 from proof union-split2 (previous step) (back to tree)

A spec-lemma

Proof step 77 from proof union-split2 (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 78:

  h0 ⊥ h1, h2 ⊥ h3, ∀ r0. (r0 ∈ h2 ∨ r0 ∈ h3 ↔ r0 ∈ h0 ∨ r0 ∈ h1) ∧ (r0 ∈ h2 ∨ r0 ∈ h3 → (r0 ∈ h2 ⊃ h2(r0);h3(r0)) = (h0 ∪ h1)(r0)) ⊦ (r ∈ h1 ↔ r ∈ h2 \ h0 ∨ r ∈ h3 \ h0) ∧ (r ∈ h1 → h1(r) = ((h2 \ h0) ∪ (h3 \ h0))(r))

Rule argument

Additional information

Used simplifier rules: in-uni: ⊦ h0 ⊥ h1 → (r ∈ h0 ∪ h1 ↔ r ∈ h0 ∨ r ∈ h1); at-uni: r ∈ h0 ∪ h1 ⊦ h0 ⊥ h1 → (h0 ∪ h1)(r) = (r ∈ h0 ⊃ h0(r);h1(r));

Proof step 78 from proof union-split2 (previous step) (back to tree)

User applied rule all left

And obtained the following new goals

• Proof step 79:

  r ∈ h2 ∨ r ∈ h3 ↔ r ∈ h0 ∨ r ∈ h1, h0 ⊥ h1, h2 ⊥ h3, r ∈ h2 ∨ r ∈ h3 → (r ∈ h2 ⊃ h2(r);h3(r)) = (h0 ∪ h1)(r) ⊦ (r ∈ h1 ↔ r ∈ h2 \ h0 ∨ r ∈ h3 \ h0) ∧ (r ∈ h1 → h1(r) = ((h2 \ h0) ∪ (h3 \ h0))(r))

Rule argument

Additional information

Used terms: r

Proof step 79 from proof union-split2 (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 80:

  r ∈ h2 ∨ r ∈ h3 ↔ r ∈ h0 ∨ r ∈ h1, h0 ⊥ h1, h2 ⊥ h3, r ∈ h0 ∨ r ∈ h1 → (r ∈ h2 ⊃ h2(r);h3(r)) = (r ∈ h0 ⊃ h0(r);h1(r)) ⊦ (r ∈ h1 ↔ r ∈ h2 \ h0 ∨ r ∈ h3 \ h0) ∧ (r ∈ h1 → h1(r) = ((h2 \ h0) ∪ (h3 \ h0))(r))

Rule argument

Additional information

Used simplifier rules: in-uni: ⊦ h0 ⊥ h1 → (r ∈ h0 ∪ h1 ↔ r ∈ h0 ∨ r ∈ h1); at-uni: r ∈ h0 ∪ h1 ⊦ h0 ⊥ h1 → (h0 ∪ h1)(r) = (r ∈ h0 ⊃ h0(r);h1(r));

Proof step 80 from proof union-split2 (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 81:

  r ∈ h0 ∪ h1 ⊦ h0 ⊥ h1 → (h0 ∪ h1)(r) = (r ∈ h0 ⊃ h0(r);h1(r))

• Proof step 82:

  r ∈ h2 ∨ r ∈ h3 ↔ r ∈ h0 ∨ r ∈ h1, h0 ⊥ h1, h2 ⊥ h3, r ∈ h0 ∨ r ∈ h1 → (r ∈ h2 ⊃ h2(r);h3(r)) = (r ∈ h0 ⊃ h0(r);h1(r)) ⊦ (r ∈ h1 ↔ r ∈ h2 \ h0 ∨ r ∈ h3 \ h0) ∧ (r ∈ h1 → h1(r) = ((h2 \ h0) ∪ (h3 \ h0))(r)), r ∈ (h2 \ h0) ∪ (h3 \ h0) ∧ h2 \ h0 ⊥ h3 \ h0

• Proof step 88:

  r ∈ h2 ∨ r ∈ h3 ↔ r ∈ h0 ∨ r ∈ h1, h0 ⊥ h1, h2 ⊥ h3, h2 \ h0 ⊥ h3 \ h0, r ∈ (h2 \ h0) ∪ (h3 \ h0), r ∈ h0 ∨ r ∈ h1 → (r ∈ h2 ⊃ h2(r);h3(r)) = (r ∈ h0 ⊃ h0(r);h1(r)) ⊦ (r ∈ h1 ↔ r ∈ h2 \ h0 ∨ r ∈ h3 \ h0) ∧ (r ∈ h1 → h1(r) = (r ∈ h2 \ h0 ⊃ (h2 \ h0)(r);(h3 \ h0)(r)))

Rule argument

Additional information

Used terms: h2 \ h0, h3 \ h0, r

Proof step 81 from proof union-split2 (previous step) (back to tree)

Lemma at-uni

Proof step 82 from proof union-split2 (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 83:

  (r ∈ h2 ⊃ h2(r);h3(r)) = h1(r), h0 ⊥ h1, h2 ⊥ h3, r ∈ h1, ¬ r ∈ h2 \ h0, ¬ r ∈ h3 \ h0, r ∈ h2 ∨ r ∈ h3 ⊦

Rule argument

Additional information

Used simplifier rules: in-uni: ⊦ h0 ⊥ h1 → (r ∈ h0 ∪ h1 ↔ r ∈ h0 ∨ r ∈ h1); disj-diffb: h0 ⊥ h1 ⊦ h0 \ h2 ⊥ h1 \ h3; disj-r: ⊦ r ∈ h1 ∧ h0 ⊥ h1 → ¬ r ∈ h0;

Proof step 83 from proof union-split2 (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 84:

  ⊦ r ∈ h0 \ h1 ↔ r ∈ h0 ∧ ¬ r ∈ h1

• Proof step 85:

  (r ∈ h2 ⊃ h2(r);h3(r)) = h1(r), h0 ⊥ h1, h2 ⊥ h3, r ∈ h1, ¬ r ∈ h3 \ h0, ¬ r ∈ h2 ∨ r ∈ h0, r ∈ h2 ∨ r ∈ h3 ⊦

Rule argument

Additional information

Used terms: r, h2, h0

Proof step 84 from proof union-split2 (previous step) (back to tree)

Lemma diff-in

Proof step 85 from proof union-split2 (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 86:

  h3(r) = h1(r), h0 ⊥ h1, h2 ⊥ h3, r ∈ h1, r ∈ h3, ¬ r ∈ h3 \ h0, ¬ r ∈ h2 ⊦

Rule argument

Additional information

Used simplifier rules: disj-r: ⊦ r ∈ h1 ∧ h0 ⊥ h1 → ¬ r ∈ h0;

Proof step 86 from proof union-split2 (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 87:

  ⊦ r ∈ h0 \ h1 ↔ r ∈ h0 ∧ ¬ r ∈ h1

Rule argument

Additional information

Used simplifier rules: disj-r: ⊦ r ∈ h1 ∧ h0 ⊥ h1 → ¬ r ∈ h0; Used terms: r, h3, h0

Proof step 87 from proof union-split2 (previous step) (back to tree)

Lemma diff-in

Proof step 88 from proof union-split2 (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 89:

  r ∈ h2 ∨ r ∈ h3 ↔ r ∈ h0 ∨ r ∈ h1, h0 ⊥ h1, h2 ⊥ h3, r ∈ (h2 \ h0) ∪ (h3 \ h0), r ∈ h0 ∨ r ∈ h1 → (r ∈ h2 ⊃ h2(r);h3(r)) = (r ∈ h0 ⊃ h0(r);h1(r)) ⊦ (r ∈ h1 ↔ r ∈ h2 \ h0 ∨ r ∈ h3 \ h0) ∧ (r ∈ h1 → h1(r) = (r ∈ h2 \ h0 ⊃ h2(r);h3(r)))

Rule argument

Additional information

Used simplifier rules: disj-diffb: h0 ⊥ h1 ⊦ h0 \ h2 ⊥ h1 \ h3; disj-r: ⊦ r ∈ h1 ∧ h0 ⊥ h1 → ¬ r ∈ h0; diff-in: ⊦ r ∈ h0 \ h1 ↔ r ∈ h0 ∧ ¬ r ∈ h1; disj-l: ⊦ r ∈ h0 ∧ h0 ⊥ h1 → ¬ r ∈ h1; diff-at: r ∈ h0, ¬ r ∈ h1 ⊦ (h0 \ h1)(r) = h0(r);

Proof step 89 from proof union-split2 (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 90:

  ⊦ h0 ⊥ h1 → (r ∈ h0 ∪ h1 ↔ r ∈ h0 ∨ r ∈ h1)

• Proof step 91:

  r ∈ h2 ∨ r ∈ h3 ↔ r ∈ h0 ∨ r ∈ h1, h0 ⊥ h1, h2 ⊥ h3, h2 \ h0 ⊥ h3 \ h0, r ∈ h0 ∨ r ∈ h1 → (r ∈ h2 ⊃ h2(r);h3(r)) = (r ∈ h0 ⊃ h0(r);h1(r)), r ∈ h2 \ h0 ∨ r ∈ h3 \ h0 ⊦ (r ∈ h1 ↔ r ∈ h2 \ h0 ∨ r ∈ h3 \ h0) ∧ (r ∈ h1 → h1(r) = (r ∈ h2 \ h0 ⊃ h2(r);h3(r)))

Rule argument

Additional information

Used simplifier rules: disj-diffb: h0 ⊥ h1 ⊦ h0 \ h2 ⊥ h1 \ h3; Used terms: r, h2 \ h0, h3 \ h0

Proof step 90 from proof union-split2 (previous step) (back to tree)

Lemma in-uni

Proof step 91 from proof union-split2 (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 92:

  r ∈ h2 ∨ r ∈ h3 ↔ r ∈ h0 ∨ r ∈ h1, h0 ⊥ h1, h2 ⊥ h3, r ∈ h2 \ h0 ∨ r ∈ h3 \ h0, r ∈ h0 ∨ r ∈ h1 → (r ∈ h2 ⊃ h2(r);h3(r)) = (r ∈ h0 ⊃ h0(r);h1(r)) ⊦ r ∈ h1 ∧ h1(r) = (r ∈ h2 \ h0 ⊃ h2(r);h3(r))

Rule argument

Additional information

Used simplifier rules: disj-diffb: h0 ⊥ h1 ⊦ h0 \ h2 ⊥ h1 \ h3;

Proof step 92 from proof union-split2 (previous step) (back to tree)

User applied rule case distinction

And obtained the following new goals

• Proof step 93:

  r ∈ h2 ∨ r ∈ h3 ↔ r ∈ h0 ∨ r ∈ h1, h0 ⊥ h1, h2 ⊥ h3, r ∈ h2 \ h0, r ∈ h0 ∨ r ∈ h1 → (r ∈ h2 ⊃ h2(r);h3(r)) = (r ∈ h0 ⊃ h0(r);h1(r)) ⊦ r ∈ h1 ∧ h1(r) = (r ∈ h2 \ h0 ⊃ h2(r);h3(r))

Rule argument

Additional information

Used simplifier rules: diff-in: ⊦ r ∈ h0 \ h1 ↔ r ∈ h0 ∧ ¬ r ∈ h1; disj-r: ⊦ r ∈ h1 ∧ h0 ⊥ h1 → ¬ r ∈ h0;

Proof step 93 from proof union-split2 (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 94:

  h2(r) = h1(r), h1(r) ≠ (r ∈ h2 \ h0 ⊃ h1(r);h3(r)), h0 ⊥ h1, h2 ⊥ h3, r ∈ h2, r ∈ h1, ¬ r ∈ h0 ⊦

Rule argument

Additional information

Used simplifier rules: diff-in: ⊦ r ∈ h0 \ h1 ↔ r ∈ h0 ∧ ¬ r ∈ h1; disj-r: ⊦ r ∈ h1 ∧ h0 ⊥ h1 → ¬ r ∈ h0;

Proof step 94 from proof union-split2 (previous step) (back to tree)

User applied rule case distinction

And obtained the following new goals

• Proof step 95:

  h2(r) = h1(r), h1(r) ≠ h3(r), h0 ⊥ h1, h2 ⊥ h3, r ∈ h1, r ∈ h2, ¬ r ∈ h2 \ h0, ¬ r ∈ h0 ⊦

Rule argument

Additional information

Proof step 95 from proof union-split2 (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 96:

  ⊦ r ∈ h0 \ h1 ↔ r ∈ h0 ∧ ¬ r ∈ h1

Rule argument

Additional information

Used simplifier rules: disj-r: ⊦ r ∈ h1 ∧ h0 ⊥ h1 → ¬ r ∈ h0; Used terms: r, h2, h0

Proof step 96 from proof union-split2 (previous step) (back to tree)

Lemma diff-in

Proof step 97 from proof union-split2 (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 98:

  h0 ⊥ h2 ⊦ h ⊆ h0 ∪ h2 → h \ h2 ⊥ h \ h0

Rule argument

Additional information

Used simplifier rules: subset-union: h0 ⊥ h1 ⊦ h0 ⊆ h0 ∪ h1; Used terms: h2, h1, h0

Proof step 98 from proof union-split2 (previous step) (back to tree)

Lemma disj-union-diff

Proof step 99 from proof union-split2 (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 100:

  h0 ⊥ h2 ⊦ h ⊆ h0 ∪ h2 → h \ h2 ⊥ h \ h0

Rule argument

Additional information

Used simplifier rules: disj-com-rw: ⊦ h0 ⊥ h1 → h1 ⊥ h0; subset-union2: h1 ⊥ h0 ⊦ h1 ⊆ h0 ∪ h1; Used terms: h3, h1, h0

Proof step 100 from proof union-split2 (previous step) (back to tree)

Lemma disj-union-diff

Proof step 101 from proof union-split2 (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 102:

  h0 ∪ h1 = h2 ∪ h3, h0 ⊥ h1, h2 ⊥ h3, ¬ h2 \ h0 ⊥ h2 \ h1 ⊦

Rule argument

Additional information

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

Proof step 102 from proof union-split2 (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 103:

  h0 ⊥ h2 ⊦ h ⊆ h0 ∪ h2 → h \ h2 ⊥ h \ h0

• Proof step 104:

  h0 ∪ h1 = h2 ∪ h3, h0 ⊥ h1, h2 ⊥ h3, ¬ h2 \ h0 ⊥ h2 \ h1 ⊦ h1 ⊥ h0 ∧ h2 ⊆ h1 ∪ h0

Rule argument

Additional information

Used terms: h2, h0, h1

Proof step 103 from proof union-split2 (previous step) (back to tree)

Lemma disj-union-diff

Proof step 104 from proof union-split2 (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 105:

  h0 ∪ h1 = h2 ∪ h3, h0 ⊥ h1, h2 ⊥ h3, ¬ h2 \ h0 ⊥ h2 \ h1, ¬ h2 ⊆ h1 ∪ h0 ⊦

Rule argument

Additional information

Used simplifier rules: disj-com-rw: ⊦ h0 ⊥ h1 → h1 ⊥ h0;

Proof step 105 from proof union-split2 (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 106:

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

Rule argument

Additional information

Used simplifier rules: subset-union: h0 ⊥ h1 ⊦ h0 ⊆ h0 ∪ h1; Used terms: h1, h0

Proof step 106 from proof union-split2 (previous step) (back to tree)

Lemma uni-com

Proof step 107 from proof union-split2 (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 108:

  h0 ∪ h1 = h2 ∪ h3, h0 ⊥ h1, h2 ⊥ h3, ¬ h3 \ h0 ⊥ h3 \ 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-diffb: h0 ⊥ h1 ⊦ h0 \ h2 ⊥ h1 \ h3;

Proof step 108 from proof union-split2 (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 109:

  h0 ⊥ h2 ⊦ h ⊆ h0 ∪ h2 → h \ h2 ⊥ h \ h0

• Proof step 110:

  h0 ∪ h1 = h2 ∪ h3, h0 ⊥ h1, h2 ⊥ h3, ¬ h3 \ h0 ⊥ h3 \ h1 ⊦ h1 ⊥ h0 ∧ h3 ⊆ h1 ∪ h0

Rule argument

Additional information

Used terms: h3, h0, h1

Proof step 109 from proof union-split2 (previous step) (back to tree)

Lemma disj-union-diff

Proof step 110 from proof union-split2 (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 111:

  h0 ∪ h1 = h2 ∪ h3, h0 ⊥ h1, h2 ⊥ h3, ¬ h3 \ h0 ⊥ h3 \ h1, ¬ h3 ⊆ h1 ∪ h0 ⊦

Rule argument

Additional information

Used simplifier rules: disj-com-rw: ⊦ h0 ⊥ h1 → h1 ⊥ h0;

Proof step 111 from proof union-split2 (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 112:

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

Rule argument

Additional information

Used simplifier rules: disj-com-rw: ⊦ h0 ⊥ h1 → h1 ⊥ h0; subset-union2: h1 ⊥ h0 ⊦ h1 ⊆ h0 ∪ h1; Used terms: h1, h0

Proof step 112 from proof union-split2 (previous step) (back to tree)

Lemma uni-com

Proof step 113 from proof union-split2 (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 114:

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

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 114 from proof union-split2 (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 115:

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

• Proof step 116:

  h20 ∪ h30 ∪ h21 ∪ h31 ≠ (h20 ∪ h21) ∪ h30 ∪ h31, h20 ⊥ h31, h20 ⊥ h21, h20 ⊥ h30, h21 ⊥ h31, h21 ⊥ h30, h21 ⊥ h20, h21 ∪ h31 ⊥ h20, h30 ⊥ h21, h30 ⊥ h31, h30 ⊥ h21 ∪ h31, h31 ⊥ h30, h31 ⊥ 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: h20, h30, h21 ∪ h31

Proof step 115 from proof union-split2 (previous step) (back to tree)

Lemma uni-ass

Proof step 116 from proof union-split2 (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 117:

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

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 117 from proof union-split2 (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 118:

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

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; disj-distr-uni: h1 ⊥ h ⊦ h0 ⊥ h1 ∪ h ↔ h0 ⊥ h1 ∧ h0 ⊥ h; uni-inj: h ⊥ h0, h ⊥ h1 ⊦ h ∪ h0 = h ∪ h1 ↔ h0 = h1; 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: h20, h21, h30 ∪ h31

Proof step 118 from proof union-split2 (previous step) (back to tree)

Lemma uni-ass