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

System applied rule normalize

And obtained the following new goals

• Proof step 2:

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

Rule argument

Additional information

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

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 3:

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

Rule argument

Additional information

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

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 4:

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

• Proof step 5:

  h0 ⊥ h1, h1 ⊥ h, h ⊥ h0, ∃ r. ¬((r ∈ (h0 ∪ h1) ∪ h ↔ r ∈ h0 ∪ h1 ∪ h) ∧ (r ∈ (h0 ∪ h1) ∪ h → ((h0 ∪ h1) ∪ h)[r] = (h0 ∪ h1 ∪ h)[r])) ⊦

Rule argument

Additional information

Used terms: h0 ∪ h1 ∪ h, (h0 ∪ h1) ∪ h

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

Lemma ext

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

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 6:

  h ⊥ h0, h1 ⊥ h, h0 ⊥ h1 ⊦ (r ∈ (h0 ∪ h1) ∪ h ↔ r ∈ h0 ∪ h1 ∪ h) ∧ (r ∈ (h0 ∪ h1) ∪ h → ((h0 ∪ h1) ∪ h)[r] = (h0 ∪ h1 ∪ h)[r])

Rule argument

Additional information

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

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 7:

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

• Proof step 8:

  h0 ⊥ h1, h1 ⊥ h, h ⊥ h0, h0 ∪ h1 ⊥ h ⊦ (r ∈ h0 ∪ h1 ∨ r ∈ h ↔ r ∈ h0 ∪ h1 ∪ h) ∧ (r ∈ h0 ∪ h1 ∨ r ∈ h → ((h0 ∪ h1) ∪ h)[r] = (h0 ∪ h1 ∪ h)[r])

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; Used terms: h, h0 ∪ h1, r

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

Lemma in-uni

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

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 9:

  h ⊥ h0, h1 ⊥ h, h0 ⊥ h1 ⊦ (r ∈ h0 ∨ r ∈ h1 ∨ r ∈ h ↔ r ∈ h0 ∪ h1 ∪ h) ∧ (r ∈ h0 ∨ r ∈ h1 ∨ r ∈ h → ((h0 ∪ h1) ∪ h)[r] = (h0 ∪ h1 ∪ h)[r])

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; in-uni: ⊦ h0 ⊥ h1 → (r ∈ h0 ∪ h1 ↔ r ∈ h0 ∨ r ∈ h1);

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

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 10:

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

• Proof step 11:

  h0 ⊥ h1, h1 ⊥ h, h ⊥ h0, h0 ⊥ h1 ∪ h ⊦ (r ∈ h0 ∨ r ∈ h1 ∨ r ∈ h ↔ r ∈ h0 ∨ r ∈ h1 ∪ h) ∧ (r ∈ h0 ∨ r ∈ h1 ∨ r ∈ h → ((h0 ∪ h1) ∪ h)[r] = (h0 ∪ h1 ∪ h)[r])

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; Used terms: h1 ∪ h, h0, r

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

Lemma in-uni

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

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 12:

  ((h0 ∪ h1) ∪ h)[r] ≠ (h0 ∪ h1 ∪ h)[r], h ⊥ h0, h1 ⊥ h, h0 ⊥ h1, r ∈ h0 ∨ r ∈ h1 ∨ r ∈ h ⊦

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; in-uni: ⊦ h0 ⊥ h1 → (r ∈ h0 ∪ h1 ↔ r ∈ h0 ∨ r ∈ h1);

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

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 13:

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

• Proof step 14:

  (r ∈ h0 ∪ h1 ⊃ (h0 ∪ h1)[r];h[r]) ≠ (h0 ∪ h1 ∪ h)[r], r ∈ (h0 ∪ h1) ∪ h, h0 ⊥ h1, h1 ⊥ h, h ⊥ h0, h0 ∪ h1 ⊥ h, r ∈ h0 ∨ r ∈ h1 ∨ r ∈ h ⊦

Rule argument

Additional information

Used simplifier rules: in-uni: ⊦ h0 ⊥ h1 → (r ∈ h0 ∪ h1 ↔ r ∈ h0 ∨ r ∈ h1); disj-distr-uni-com: ⊦ h1 ⊥ h2 → (h1 ∪ h2 ⊥ h0 ↔ h0 ⊥ h1 ∧ h0 ⊥ h2); disj-com-rw: ⊦ h0 ⊥ h1 → h1 ⊥ h0; Used terms: r, h, h0 ∪ h1

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

Lemma at-uni

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

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 15:

  (r ∈ h0 ∨ r ∈ h1 ⊃ (r ∈ h0 ⊃ h0[r];h1[r]);h[r]) ≠ (h0 ∪ h1 ∪ h)[r], r ∈ (h0 ∪ h1) ∪ h, h ⊥ h0, h1 ⊥ h, h0 ⊥ h1, r ∈ h0 ∨ r ∈ h1 ∨ r ∈ h ⊦

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-distr-uni-com: ⊦ h1 ⊥ h2 → (h1 ∪ h2 ⊥ h0 ↔ h0 ⊥ h1 ∧ h0 ⊥ h2); disj-com-rw: ⊦ h0 ⊥ h1 → h1 ⊥ h0;

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

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 16:

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

• Proof step 17:

  (r ∈ h0 ∨ r ∈ h1 ⊃ (r ∈ h0 ⊃ h0[r];h1[r]);h[r]) ≠ (r ∈ h0 ⊃ h0[r];(h1 ∪ h)[r]), r ∈ (h0 ∪ h1) ∪ h, r ∈ h0 ∪ h1 ∪ h, h0 ⊥ h1, h1 ⊥ h, h ⊥ h0, h0 ⊥ h1 ∪ h, r ∈ h0 ∨ r ∈ h1 ∨ r ∈ h ⊦

Rule argument

Additional information

Used simplifier rules: in-uni: ⊦ h0 ⊥ h1 → (r ∈ h0 ∪ h1 ↔ r ∈ h0 ∨ r ∈ h1); disj-distr-uni: ⊦ h1 ⊥ h → (h0 ⊥ h1 ∪ h ↔ h0 ⊥ h1 ∧ h0 ⊥ h); disj-com-rw: ⊦ h0 ⊥ h1 → h1 ⊥ h0; Used terms: r, h1 ∪ h, h0

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

Lemma at-uni

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

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 18:

  (r ∈ h1 ⊃ h1[r];h[r]) ≠ (h1 ∪ h)[r], r ∈ (h0 ∪ h1) ∪ h, r ∈ h0 ∪ h1 ∪ h, h0 ⊥ h1, h1 ⊥ h, h ⊥ h0, ¬ r ∈ h0, r ∈ h ∨ r ∈ 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-r: ⊦ r ∈ h1 ∧ h0 ⊥ h1 → (r ∈ h0 ↔ false);

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

Heuristic cut applied rule cut formula

And closed the goal!

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]); 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); Used formulas: r ∈ h1