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

System applied rule normalize

And obtained the following new goals

• Proof step 2:

  (h0 ∪ h1) -- r ≠ (h0 -- r) ∪ (h1 -- r), h0 ⊥ h1 ⊦

Rule argument

Additional information

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

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 3:

  (h0 ∪ h1) -- r ≠ (h0 -- r) ∪ (h1 -- r), h0 ⊥ h1 ⊦

Rule argument

Additional information

Proof step 3 from proof del-uni (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, ∃ r0. ¬((r0 ∈ (h0 ∪ h1) -- r ↔ r0 ∈ (h0 -- r) ∪ (h1 -- r)) ∧ (r0 ∈ (h0 ∪ h1) -- r → ((h0 ∪ h1) -- r)[r0] = ((h0 -- r) ∪ (h1 -- r))[r0])) ⊦

Rule argument

Additional information

Used terms: (h0 -- r) ∪ (h1 -- r), (h0 ∪ h1) -- r

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

Lemma ext

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

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 6:

  h0 ⊥ h1 ⊦ (r0 ≠ r ∧ (r0 ∈ h0 ∨ r0 ∈ h1) ↔ r0 ∈ (h0 -- r) ∪ (h1 -- r)) ∧ (r0 ≠ r ∧ (r0 ∈ h0 ∨ r0 ∈ h1) → (r0 ∈ h0 ⊃ h0[r0];h1[r0]) = ((h0 -- r) ∪ (h1 -- r))[r0])

Rule argument

Additional information

Used simplifier rules: in-del: ⊦ r ∈ h -- r0 ↔ r ≠ r0 ∧ r ∈ h; at-del: r ∈ h ⊦ r ≠ r0 → (h -- r0)[r] = h[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]);

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

User applied rule cut formula

And obtained the following new goals

• Proof step 7:

  r0 ≠ r ∧ (r0 ∈ h0 ∨ r0 ∈ h1) ↔ r0 ∈ (h0 -- r) ∪ (h1 -- r), h0 ⊥ h1 ⊦ (r0 ≠ r ∧ (r0 ∈ h0 ∨ r0 ∈ h1) ↔ r0 ∈ (h0 -- r) ∪ (h1 -- r)) ∧ (r0 ≠ r ∧ (r0 ∈ h0 ∨ r0 ∈ h1) → (r0 ∈ h0 ⊃ h0[r0];h1[r0]) = ((h0 -- r) ∪ (h1 -- r))[r0])

• Proof step 15:

  ¬(r0 ≠ r ∧ (r0 ∈ h0 ∨ r0 ∈ h1) ↔ r0 ∈ (h0 -- r) ∪ (h1 -- r)), h0 ⊥ h1 ⊦ (r0 ≠ r ∧ (r0 ∈ h0 ∨ r0 ∈ h1) ↔ r0 ∈ (h0 -- r) ∪ (h1 -- r)) ∧ (r0 ≠ r ∧ (r0 ∈ h0 ∨ r0 ∈ h1) → (r0 ∈ h0 ⊃ h0[r0];h1[r0]) = ((h0 -- r) ∪ (h1 -- r))[r0])

Rule argument

Additional information

Used formulas: r0 ≠ r ∧ (r0 ∈ h0 ∨ r0 ∈ h1) ↔ r0 ∈ (h0 -- r) ∪ (h1 -- r)

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

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 8:

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

Rule argument

Additional information

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

User applied rule case distinction

And obtained the following new goals

• Proof step 9:

  (r0 ∈ h0 ⊃ h0[r0];h1[r0]) ≠ ((h0 -- r) ∪ (h1 -- r))[r0], r0 ≠ r, r0 ∈ (h0 -- r) ∪ (h1 -- r), r0 ∈ h0, h0 ⊥ h1 ⊦

• Proof step 12:

  (r0 ∈ h0 ⊃ h0[r0];h1[r0]) ≠ ((h0 -- r) ∪ (h1 -- r))[r0], r0 ≠ r, r0 ∈ (h0 -- r) ∪ (h1 -- r), r0 ∈ h1, h0 ⊥ h1 ⊦

Rule argument

Additional information

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

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 10:

  h0[r0] ≠ ((h0 -- r) ∪ (h1 -- r))[r0], r0 ≠ r, r0 ∈ h0, r0 ∈ (h0 -- r) ∪ (h1 -- r), h0 ⊥ h1 ⊦

Rule argument

Additional information

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

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 11:

  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); in-del: ⊦ r ∈ h -- r0 ↔ r ≠ r0 ∧ r ∈ h; disj-rem: ⊦ h0 ⊥ h1 → h0 -- r ⊥ h1 -- r; in-del: ⊦ r ∈ h -- r0 ↔ r ≠ r0 ∧ r ∈ h; at-del: r ∈ h ⊦ r ≠ r0 → (h -- r0)[r] = h[r]; Used terms: r0, h1 -- r, h0 -- r

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

Lemma at-uni

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

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 13:

  h1[r0] ≠ ((h0 -- r) ∪ (h1 -- r))[r0], r0 ≠ r, r0 ∈ h1, r0 ∈ (h0 -- r) ∪ (h1 -- r), h0 ⊥ h1 ⊦

Rule argument

Additional information

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

Proof step 13 from proof del-uni (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])

Rule argument

Additional information

Used simplifier rules: in-uni: ⊦ h0 ⊥ h1 → (r ∈ h0 ∪ h1 ↔ r ∈ h0 ∨ r ∈ h1); disj-r: ⊦ r ∈ h1 ∧ h0 ⊥ h1 → (r ∈ h0 ↔ false); in-del: ⊦ r ∈ h -- r0 ↔ r ≠ r0 ∧ r ∈ h; disj-rem: ⊦ h0 ⊥ h1 → h0 -- r ⊥ h1 -- r; in-del: ⊦ r ∈ h -- r0 ↔ r ≠ r0 ∧ r ∈ h; disj-r: ⊦ r ∈ h1 ∧ h0 ⊥ h1 → (r ∈ h0 ↔ false); at-del: r ∈ h ⊦ r ≠ r0 → (h -- r0)[r] = h[r]; Used terms: r0, h1 -- r, h0 -- r

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

Lemma at-uni

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

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 16:

  ¬(r0 ≠ r ∧ (r0 ∈ h0 ∨ r0 ∈ h1) ↔ r0 ∈ (h0 -- r) ∪ (h1 -- r)), h0 ⊥ h1 ⊦

Rule argument

Additional information

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

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 17:

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

• Proof step 18:

  ¬(r0 ≠ r ∧ (r0 ∈ h0 ∨ r0 ∈ h1) ↔ r0 ∈ h0 -- r ∨ r0 ∈ h1 -- r), h0 ⊥ h1, h0 -- r ⊥ h1 -- r ⊦

Rule argument

Additional information

Used simplifier rules: disj-rem: ⊦ h0 ⊥ h1 → h0 -- r ⊥ h1 -- r; Used terms: h1 -- r, h0 -- r, r0

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

Lemma in-uni

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

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 19:

  h0 -- r ⊥ h1 -- r, h0 ⊥ h1, r0 ≠ r ∧ r0 ∈ h0 ∨ r0 ≠ r ∧ r0 ∈ h1 ⊦ r0 ≠ r ∧ (r0 ∈ h0 ∨ r0 ∈ h1)

Rule argument

Additional information

Used simplifier rules: in-del: ⊦ r ∈ h -- r0 ↔ r ≠ r0 ∧ r ∈ h;

Proof step 19 from proof del-uni (previous step) (back to tree)

User applied rule case distinction

And closed the goal!

Rule argument

Additional information