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 141:

  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 21:

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

• Proof step 40:

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

• Proof step 72:

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

• Proof step 107:

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

• Proof step 114:

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

• Proof step 121:

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

• Proof step 131:

  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:

  ⊦ st1 = st2 ↔ (∀ a. (a ∈ st1 ↔ a ∈ st2) ∧ st1(a) = st2(a))

• Proof step 7:

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

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) ∧ ((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) ∧ ((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) ∧ ((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, ((h2 \ h1) ∪ (h2 \ h0))(r) ≠ h2(r), h0 ⊥ h1, h2 \ h1 ⊥ h2 \ h0, h2 ⊥ h3 ⊦

Rule argument

Additional information

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

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 ⊦ h0 ⊥ h1 → (h0 ∪ h1)(r) = (r ∈ h0 ⊃ h0(r);h1(r))

• Proof step 15:

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

Rule argument

Additional information

Used simplifier rules: in-uni: ⊦ h0 ⊥ h1 → (r ∈ h0 ∪ h1 ↔ r ∈ h0 ∨ 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, h2 \ h0, r

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

Lemma at-uni

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

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 16:

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

Rule argument

Additional information

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

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

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 17:

  ⊦ ¬ a ∈ st → st(a) = ∅(a)

• Proof step 18:

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

Rule argument

Additional information

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

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

A spec-lemma

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

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 19:

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

Rule argument

Additional information

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

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

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 20:

  ⊦ ¬ a ∈ st → st(a) = ∅(a)

Rule argument

Additional information

Used simplifier rules: disj-r: ⊦ r ∈ h1 ∧ h0 ⊥ h1 → (r ∈ h0 ↔ false); Used terms: h2, r

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

A spec-lemma

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

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 22:

  ⊦ st1 = st2 ↔ (∀ a. (a ∈ st1 ↔ a ∈ st2) ∧ st1(a) = st2(a))

• Proof step 23:

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

Rule argument

Additional information

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

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

A spec-lemma

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

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 24:

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

Rule argument

Additional information

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 ∈ h0 ∪ h1 ↔ r ∈ h0 ∨ r ∈ h1)

• Proof step 26:

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

• Proof step 31:

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

Rule argument

Additional information

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

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

Lemma in-uni

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

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 27:

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

• Proof step 28:

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

Rule argument

Additional information

Used terms: h3, h1, h0

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

Lemma disj-union-diff

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

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 29:

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

Rule argument

Additional information

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 ⊥ h1 → h1 ∪ h0 = h0 ∪ h1

Rule argument

Additional information

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

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

Lemma uni-com

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

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 32:

  h0 ∪ h1 = h2 ∪ h3, ((h3 \ h1) ∪ (h3 \ h0))(r) ≠ h3(r), h0 ⊥ h1, h2 ⊥ h3, h3 \ h1 ⊥ h3 \ 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 ↔ false);

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

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 33:

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

• Proof step 34:

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

Rule argument

Additional information

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

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

Lemma at-uni

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

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 35:

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

Rule argument

Additional information

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

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

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 36:

  ⊦ ¬ a ∈ st → st(a) = ∅(a)

• Proof step 37:

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

Rule argument

Additional information

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

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

A spec-lemma

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:

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

Rule argument

Additional information

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

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:

  ⊦ ¬ a ∈ st → st(a) = ∅(a)

Rule argument

Additional information

Used simplifier rules: disj-r: ⊦ r ∈ h1 ∧ h0 ⊥ h1 → (r ∈ h0 ↔ false); Used terms: h3, r

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

A spec-lemma

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

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 41:

  ⊦ st1 = st2 ↔ (∀ a. (a ∈ st1 ↔ a ∈ st2) ∧ st1(a) = st2(a))

• Proof step 42:

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

Rule argument

Additional information

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

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

A spec-lemma

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

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 43:

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

Rule argument

Additional information

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:

  ⊦ st1 = st2 ↔ (∀ a. (a ∈ st1 ↔ a ∈ st2) ∧ st1(a) = st2(a))

• Proof step 45:

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

Rule argument

Additional information

Used terms: h0 ∪ h1, h2 ∪ h3

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, ∀ a. (a ∈ h0 ∨ a ∈ h1 ↔ a ∈ h2 ∨ a ∈ h3) ∧ (h0 ∪ h1)(a) = (h2 ∪ h3)(a) ⊦ (r ∈ (h2 \ h1) ∪ (h3 \ h1) ↔ r ∈ h0) ∧ ((h2 \ h1) ∪ (h3 \ h1))(r) = h0(r)

Rule argument

Additional information

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

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

User applied rule all left

And obtained the following new goals

• Proof step 47:

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

Rule argument

Additional information

Used terms: r

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

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 48:

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

• Proof step 49:

  (h0 ∪ h1)(r) = (h2 ∪ h3)(r), r ∈ h0 ∨ r ∈ h1 ↔ r ∈ h2 ∨ r ∈ h3, h0 ⊥ h1, h2 ⊥ h3, h2 \ h1 ⊥ h3 \ h1 ⊦ (r ∈ h2 \ h1 ∨ r ∈ h3 \ h1 ↔ r ∈ h0) ∧ ((h2 \ h1) ∪ (h3 \ h1))(r) = h0(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 48 from proof union-split2 (previous step) (back to tree)

Lemma in-uni

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

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 50:

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

Rule argument

Additional information

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

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

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 51:

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

• Proof step 52:

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

• Proof step 59:

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

Rule argument

Additional information

Used terms: h0, h1, r

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

Lemma at-uni

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

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 53:

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

Rule argument

Additional information

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

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

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 54:

  ⊦ ¬ a ∈ st → st(a) = ∅(a)

• Proof step 55:

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

• Proof step 57:

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

Rule argument

Additional information

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

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

A spec-lemma

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

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 56:

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

Rule argument

Additional information

Used simplifier rules: disj-diffb: h0 ⊥ h1 ⊦ h0 \ h2 ⊥ h1 \ h3; 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-diffb: h0 ⊥ h1 ⊦ h0 \ h2 ⊥ h1 \ h3; diff-in: ⊦ r ∈ h0 \ h1 ↔ r ∈ h0 ∧ ¬ r ∈ h1; Used terms: r, h2 \ h1, h3 \ h1

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

Lemma in-uni

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

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 58:

  ⊦ ¬ a ∈ st → st(a) = ∅(a)

Rule argument

Additional information

Used terms: h0, r

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

A spec-lemma

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

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 60:

  (r ∈ h0 ⊃ h0(r);h1(r)) = (r ∈ h2 ⊃ h2(r);h3(r)), h0 ⊥ h1, h2 ⊥ h3, r ∈ h2 ∨ r ∈ h3, r ∈ h0 ∨ r ∈ h1 ⊦ (r ∈ h2 ∧ ¬ r ∈ h1 ∨ r ∈ h3 ∧ ¬ r ∈ h1 ↔ r ∈ h0) ∧ ((h2 \ h1) ∪ (h3 \ h1))(r) = 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 60 from proof union-split2 (previous step) (back to tree)

User applied rule case distinction

And obtained the following new goals

• Proof step 61:

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

Rule argument

Additional information

Used simplifier rules: disj-r: ⊦ r ∈ h1 ∧ h0 ⊥ h1 → (r ∈ h0 ↔ false); disj-l: ⊦ r ∈ h0 ∧ h0 ⊥ h1 → (r ∈ h1 ↔ false);

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

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 62:

  ⊦ ¬ a ∈ st → st(a) = ∅(a)

• Proof step 63:

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

• Proof step 67:

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

Rule argument

Additional information

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

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

A spec-lemma

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

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 64:

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

• Proof step 65:

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

Rule argument

Additional information

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

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

Lemma in-uni

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

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 66:

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

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-at: r ∈ h0, ¬ r ∈ h1 ⊦ (h0 \ h1)(r) = h0(r); disj-diffb: h0 ⊥ h1 ⊦ h0 \ h2 ⊥ h1 \ h3; diff-in: ⊦ r ∈ h0 \ h1 ↔ r ∈ h0 ∧ ¬ r ∈ h1;

Proof step 66 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: diff-at: r ∈ h0, ¬ r ∈ h1 ⊦ (h0 \ h1)(r) = h0(r); disj-r: ⊦ r ∈ h1 ∧ h0 ⊥ h1 → (r ∈ h0 ↔ false);

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

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 68:

  ⊦ ¬ a ∈ st → st(a) = ∅(a)

• Proof step 69:

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

Rule argument

Additional information

Used terms: h0, r

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

A spec-lemma

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

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 70:

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

Rule argument

Additional information

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

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 71:

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

Rule argument

Additional information

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

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

Lemma in-uni

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:

  ⊦ st1 = st2 ↔ (∀ a. (a ∈ st1 ↔ a ∈ st2) ∧ st1(a) = st2(a))

• Proof step 74:

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

Rule argument

Additional information

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

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

A spec-lemma

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 ∈ (h2 \ h0) ∪ (h3 \ h0) ↔ r ∈ h1) ∧ ((h2 \ h0) ∪ (h3 \ h0))(r) = h1(r)

Rule argument

Additional information

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:

  ⊦ st1 = st2 ↔ (∀ a. (a ∈ st1 ↔ a ∈ st2) ∧ st1(a) = st2(a))

• Proof step 77:

  h0 ⊥ h1, h2 ⊥ h3, ∀ a. (a ∈ h0 ∪ h1 ↔ a ∈ h2 ∪ h3) ∧ (h0 ∪ h1)(a) = (h2 ∪ h3)(a) ⊦ (r ∈ (h2 \ h0) ∪ (h3 \ h0) ↔ r ∈ h1) ∧ ((h2 \ h0) ∪ (h3 \ h0))(r) = h1(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, ∀ a. (a ∈ h0 ∨ a ∈ h1 ↔ a ∈ h2 ∨ a ∈ h3) ∧ (h0 ∪ h1)(a) = (h2 ∪ h3)(a) ⊦ (r ∈ (h2 \ h0) ∪ (h3 \ h0) ↔ r ∈ h1) ∧ ((h2 \ h0) ∪ (h3 \ h0))(r) = h1(r)

Rule argument

Additional information

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

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:

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

Rule argument

Additional information

Used terms: r

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

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 80:

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

• Proof step 81:

  (h0 ∪ h1)(r) = (h2 ∪ h3)(r), r ∈ h0 ∨ r ∈ h1 ↔ r ∈ h2 ∨ r ∈ h3, h0 ⊥ h1, h2 ⊥ h3, h2 \ h0 ⊥ h3 \ h0 ⊦ (r ∈ h2 \ h0 ∨ r ∈ h3 \ h0 ↔ r ∈ h1) ∧ ((h2 \ h0) ∪ (h3 \ h0))(r) = h1(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 80 from proof union-split2 (previous step) (back to tree)

Lemma in-uni

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

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 82:

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

Rule argument

Additional information

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

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

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 83:

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

• Proof step 84:

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

• Proof step 91:

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

Rule argument

Additional information

Used terms: h0, h1, r

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

Lemma at-uni

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

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 85:

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

Rule argument

Additional information

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

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

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 86:

  ⊦ ¬ a ∈ st → st(a) = ∅(a)

• Proof step 87:

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

• Proof step 89:

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

Rule argument

Additional information

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

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

A spec-lemma

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

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 88:

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

Rule argument

Additional information

Used simplifier rules: disj-diffb: h0 ⊥ h1 ⊦ h0 \ h2 ⊥ h1 \ h3; 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-diffb: h0 ⊥ h1 ⊦ h0 \ h2 ⊥ h1 \ h3; diff-in: ⊦ r ∈ h0 \ h1 ↔ r ∈ h0 ∧ ¬ r ∈ h1; Used terms: r, h2 \ h0, h3 \ h0

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

Lemma in-uni

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:

  ⊦ ¬ a ∈ st → st(a) = ∅(a)

Rule argument

Additional information

Used terms: h1, r

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

A spec-lemma

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 ∈ h0 ⊃ h0(r);h1(r)) = (r ∈ h2 ⊃ h2(r);h3(r)), h0 ⊥ h1, h2 ⊥ h3, r ∈ h2 ∨ r ∈ h3, r ∈ h0 ∨ r ∈ h1 ⊦ (r ∈ h2 ∧ ¬ r ∈ h0 ∨ r ∈ h3 ∧ ¬ r ∈ h0 ↔ r ∈ h1) ∧ ((h2 \ h0) ∪ (h3 \ 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 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 ∈ h0 ⊃ h0(r);h1(r)) = (r ∈ h2 ⊃ h2(r);h3(r)), ((h2 \ h0) ∪ (h3 \ h0))(r) ≠ h1(r), h0 ⊥ h1, h2 ⊥ h3, r ∈ h0 ∨ r ∈ h1, r ∈ h2 ∨ r ∈ h3 ⊦

Rule argument

Additional information

Used simplifier rules: disj-l: ⊦ r ∈ h0 ∧ h0 ⊥ h1 → (r ∈ h1 ↔ false); disj-r: ⊦ r ∈ h1 ∧ h0 ⊥ h1 → (r ∈ h0 ↔ false);

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

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 94:

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

• Proof step 95:

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

• Proof step 102:

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

Rule argument

Additional information

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

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

Lemma at-uni

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

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 96:

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

Rule argument

Additional information

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

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

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 97:

  ⊦ ¬ a ∈ st → st(a) = ∅(a)

• Proof step 98:

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

• Proof step 100:

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

Rule argument

Additional information

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

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

A spec-lemma

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

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 99:

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

Rule argument

Additional information

Used simplifier rules: disj-diffb: h0 ⊥ h1 ⊦ h0 \ h2 ⊥ h1 \ h3; 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-diffb: h0 ⊥ h1 ⊦ h0 \ h2 ⊥ h1 \ h3; diff-in: ⊦ r ∈ h0 \ h1 ↔ r ∈ h0 ∧ ¬ r ∈ h1; Used terms: r, h2 \ h0, h3 \ h0

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

Lemma in-uni

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

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 101:

  ⊦ ¬ a ∈ st → st(a) = ∅(a)

Rule argument

Additional information

Used simplifier rules: disj-l: ⊦ r ∈ h0 ∧ h0 ⊥ h1 → (r ∈ h1 ↔ false); disj-r: ⊦ r ∈ h1 ∧ h0 ⊥ h1 → (r ∈ h0 ↔ false); Used terms: h1, r

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

A spec-lemma

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

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 103:

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

Rule argument

Additional information

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

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

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 104:

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

• Proof step 105:

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

Rule argument

Additional information

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

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

Lemma in-uni

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

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 106:

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

Rule argument

Additional information

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

Proof step 106 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 ↔ false); diff-at: r ∈ h0, ¬ r ∈ h1 ⊦ (h0 \ h1)(r) = h0(r);

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

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 108:

  ⊦ h0 ⊥ h1 ↔ (∀ r. ¬ r ∈ h0 ∨ ¬ r ∈ h1)

• Proof step 109:

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

Rule argument

Additional information

Used terms: h2 \ h1, h2 \ h0

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

Lemma disj

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

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 110:

  h0 ∪ h1 = h2 ∪ h3, 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;

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

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 111:

  ⊦ st1 = st2 ↔ (∀ a. (a ∈ st1 ↔ a ∈ st2) ∧ st1(a) = st2(a))

• Proof step 112:

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

Rule argument

Additional information

Used terms: h0 ∪ h1, h2 ∪ h3

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

A spec-lemma

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

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 113:

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

Rule argument

Additional information

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

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

Heuristic quantifier closing applied rule all left

And closed the goal!

Rule argument

Additional information

Used terms: r

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 ↔ (∀ r. ¬ r ∈ h0 ∨ ¬ r ∈ h1)

• Proof step 116:

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

Rule argument

Additional information

Used terms: h3 \ h1, h3 \ h0

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

Lemma disj

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:

  h0 ∪ h1 = h2 ∪ h3, h0 ⊥ h1, h2 ⊥ h3, r ∈ h3, ¬ r ∈ h1, ¬ r ∈ h0 ⊦

Rule argument

Additional information

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

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:

  ⊦ st1 = st2 ↔ (∀ a. (a ∈ st1 ↔ a ∈ st2) ∧ st1(a) = st2(a))

• Proof step 119:

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

Rule argument

Additional information

Used terms: h0 ∪ h1, h2 ∪ h3

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

A spec-lemma

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

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 120:

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

Rule argument

Additional information

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

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

Heuristic quantifier closing applied rule all left

And closed the goal!

Rule argument

Additional information

Used simplifier rules: disj-r: ⊦ r ∈ h1 ∧ h0 ⊥ h1 → (r ∈ h0 ↔ false); Used terms: r

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

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 122:

  ⊦ h0 ⊥ h1 ↔ (∀ r. ¬ r ∈ h0 ∨ ¬ r ∈ h1)

• Proof step 123:

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

Rule argument

Additional information

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

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

Lemma disj

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

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 124:

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

Rule argument

Additional information

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

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

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 125:

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

• Proof step 126:

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

Rule argument

Additional information

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

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

Lemma in-uni

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

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 127:

  h0 ∪ h1 = h2 ∪ h3, h0 ⊥ h1, h2 ⊥ h3, r ∈ h2, ¬ r ∈ h0, ¬ r ∈ h1 ⊦

Rule argument

Additional information

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

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

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 128:

  ⊦ st1 = st2 ↔ (∀ a. (a ∈ st1 ↔ a ∈ st2) ∧ st1(a) = st2(a))

• Proof step 129:

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

Rule argument

Additional information

Used terms: h0 ∪ h1, h2 ∪ h3

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

A spec-lemma

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

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 130:

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

Rule argument

Additional information

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

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

Heuristic quantifier closing applied rule all left

And closed the goal!

Rule argument

Additional information

Used terms: r

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

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 132:

  ⊦ h0 ⊥ h1 ↔ (∀ r. ¬ r ∈ h0 ∨ ¬ r ∈ h1)

• Proof step 133:

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

Rule argument

Additional information

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

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

Lemma disj

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

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 134:

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

Rule argument

Additional information

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

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

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 135:

  ⊦ st1 = st2 ↔ (∀ a. (a ∈ st1 ↔ a ∈ st2) ∧ st1(a) = st2(a))

• Proof step 136:

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

Rule argument

Additional information

Used terms: h0 ∪ h1, h2 ∪ h3

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

A spec-lemma

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

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 137:

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

Rule argument

Additional information

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

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

User applied rule all left

And obtained the following new goals

• Proof step 138:

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

Rule argument

Additional information

Used terms: r

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

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 139:

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

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 ↔ false);

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

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 140:

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

Rule argument

Additional information

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

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

Lemma in-uni

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

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 142:

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

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 143:

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

• Proof step 144:

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

Lemma uni-ass

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

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 145:

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

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 146:

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

• Proof step 147:

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

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

Lemma uni-ass

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

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 148:

  h20 ∪ h30 ∪ h21 ∪ h31 ≠ h20 ∪ h21 ∪ h30 ∪ h31, h20 ⊥ h21, h20 ⊥ h30, 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-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 148 from proof union-split2 (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 149:

  ⊦ 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: h20, h30 ∪ h21 ∪ h31, h21 ∪ h30 ∪ h31

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

Lemma uni-inj