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

System applied rule normalize

And obtained the following new goals

• Proof step 2:

  (x ∪ y) \ z ≠ (x \ z) ∪ (y \ z) ⊦

Rule argument

Additional information

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

User applied rule structural induction

And obtained the following new goals

• Proof step 3:

  ([] ∪ y) \ z ≠ ([] \ z) ∪ (y \ z) ⊦

• Proof step 25:

  ((a + x0) ∪ y) \ z ≠ ((a + x0) \ z) ∪ (y \ z), ∀ y, z. (x0 ∪ y) \ z = (x0 \ z) ∪ (y \ z) ⊦

Rule argument

Additional information

Used simplifier rules: list('a) freely generated by [], +;;

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

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 4:

  rmdup(y) \ z ≠ rmdup(y \ z) ⊦

Rule argument

Additional information

Used simplifier rules: diff-e: ⊦ [] \ y = []; union: ⊦ x ∪ y = rmdup(x + y); assoc: ⊦ (x ∪ y) ∪ z = x ∪ y ∪ z; a: ⊦ (x + y) + z = x + y + z; from specification polylist ⊦ [] + x = x; (s)

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

User applied rule structural induction

And obtained the following new goals

• Proof step 5:

  rmdup(a + y0) \ z ≠ rmdup((a + y0) \ z), ∀ z. rmdup(y0) \ z = rmdup(y0 \ z) ⊦

Rule argument

Additional information

Used simplifier rules: diff-e: ⊦ [] \ y = []; list('a) freely generated by [], +;; ⊦ rmdup([]) = []; (s)

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

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 6:

  rmdup(a ' + y0) \ z ≠ rmdup((a ' + y0) \ z), ∀ z. rmdup(y0) \ z = rmdup(y0 \ z) ⊦

Rule argument

Additional information

Used simplifier rules: ⊦ a + x = a ' + x; (s)

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

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 7:

  ⊦ rmdup(a ' + x) = (a ∈ x ⊃ rmdup(x);a ' + rmdup(x))

• Proof step 8:

  (a ∈ y0 ⊃ rmdup(y0);a ' + rmdup(y0)) \ z ≠ rmdup((a ' + y0) \ z), ∀ z. rmdup(y0) \ z = rmdup(y0 \ z) ⊦

Rule argument

Additional information

Used terms: y0, a

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

A spec-lemma

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

User applied rule case distinction

And obtained the following new goals

• Proof step 9:

  rmdup(y0) \ z ≠ rmdup((a ' + y0) \ z), a ∈ y0, ∀ z. rmdup(y0) \ z = rmdup(y0 \ z) ⊦

• Proof step 15:

  (a ' + rmdup(y0)) \ z ≠ rmdup((a ' + y0) \ z), ¬ a ∈ y0, ∀ z. rmdup(y0) \ z = rmdup(y0 \ z) ⊦

Rule argument

Additional information

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

User applied rule all left

And obtained the following new goals

• Proof step 10:

  rmdup(y0) \ z = rmdup(y0 \ z), rmdup(y0) \ z ≠ rmdup((a ' + y0) \ z), a ∈ y0 ⊦

Rule argument

Additional information

Used terms: z

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

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 11:

  ⊦ ¬ a ∈ y → (a ' + x) \ y = a + (x \ y)

• Proof step 12:

  rmdup(y0) \ z = rmdup(y0 \ z), rmdup(y0) \ z ≠ rmdup(a + (y0 \ z)), a ∈ y0, ¬ a ∈ z ⊦

Rule argument

Additional information

Used simplifier rules: diff-y: ⊦ a ∈ y → (a ' + x) \ y = x \ y; a: ⊦ (x + y) + z = x + y + z; from specification polylist Used terms: z, y0, a

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

Lemma diff-n

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

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 13:

  rmdup(y0) \ z = rmdup(y0 \ z), rmdup(y0) \ z ≠ rmdup(a ' + (y0 \ z)), a ∈ y0, ¬ a ∈ z ⊦

Rule argument

Additional information

Used simplifier rules: ⊦ a + x = a ' + x; (s)

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

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 14:

  ⊦ ¬ a ∈ x → rmdup(a ' + x) = a + rmdup(x)

Rule argument

Additional information

Used simplifier rules: diff-in: ⊦ a ∈ x \ y ↔ a ∈ x ∧ ¬ a ∈ y; ⊦ a + x = a ' + x; (s) ⊦ a ∈ x → rmdup(a ' + x) = rmdup(x); (s) a: ⊦ (x + y) + z = x + y + z; from specification polylist Used terms: y0 \ z, a

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

A spec-lemma

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

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 16:

  (a ' + rmdup(y0)) \ z ≠ rmdup((a ' + y0) \ z), ¬ a ∈ y0, ∀ z. rmdup(y0) \ z = rmdup(y0 \ z) ⊦

Rule argument

Additional information

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

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 17:

  ⊦ ¬ a ∈ y → (a ' + x) \ y = a + (x \ y)

• Proof step 18:

  (a ' + rmdup(y0)) \ z ≠ rmdup((a ' + y0) \ z), a ∈ z, ¬ a ∈ y0, ∀ z. rmdup(y0) \ z = rmdup(y0 \ z) ⊦

• Proof step 20:

  (a ' + rmdup(y0)) \ z ≠ rmdup(a + (y0 \ z)), ¬ a ∈ z, ¬ a ∈ y0, ∀ z. rmdup(y0) \ z = rmdup(y0 \ z) ⊦

Rule argument

Additional information

Used terms: z, y0, a

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

Lemma diff-n

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

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 19:

  rmdup(y0) \ z ≠ rmdup(y0 \ z), a ∈ z, ¬ a ∈ y0, ∀ z. rmdup(y0) \ z = rmdup(y0 \ z) ⊦

Rule argument

Additional information

Used simplifier rules: diff-y: ⊦ a ∈ y → (a ' + x) \ y = x \ y; a: ⊦ (x + y) + z = x + y + z; from specification polylist

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

Heuristic quantifier closing applied rule all left

And closed the goal!

Rule argument

Additional information

Used terms: z

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

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 21:

  a ' + (rmdup(y0) \ z) ≠ rmdup(a ' + (y0 \ z)), ¬ a ∈ z, ¬ a ∈ y0, ∀ z. rmdup(y0) \ z = rmdup(y0 \ z) ⊦

Rule argument

Additional information

Used simplifier rules: diff-n: ⊦ ¬ a ∈ y → (a ' + x) \ y = a + (x \ y); ⊦ a + x = a ' + x; (s) a: ⊦ (x + y) + z = x + y + z; from specification polylist

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

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 22:

  ⊦ ¬ a ∈ x → rmdup(a ' + x) = a + rmdup(x)

• Proof step 23:

  a ' + (rmdup(y0) \ z) ≠ a + rmdup(y0 \ z), ¬ a ∈ y0 \ z, ¬ a ∈ z, ¬ a ∈ y0, ∀ z. rmdup(y0) \ z = rmdup(y0 \ z) ⊦

Rule argument

Additional information

Used simplifier rules: diff-in: ⊦ a ∈ x \ y ↔ a ∈ x ∧ ¬ a ∈ y; ⊦ a ∈ x → rmdup(a ' + x) = rmdup(x); (s) a: ⊦ (x + y) + z = x + y + z; from specification polylist Used terms: y0 \ z, a

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

A spec-lemma

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

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 24:

  rmdup(y0) \ z ≠ rmdup(y0 \ z), ¬ a ∈ z, ¬ a ∈ y0, ∀ z. rmdup(y0) \ z = rmdup(y0 \ z) ⊦

Rule argument

Additional information

Used simplifier rules: diff-in: ⊦ a ∈ x \ y ↔ a ∈ x ∧ ¬ a ∈ y; a: ⊦ (x + y) + z = x + y + z; from specification polylist ⊦ x + y = x + z ↔ y = z; (s) ⊦ a + x = a ' + x; (s)

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

Heuristic quantifier closing applied rule all left

And closed the goal!

Rule argument

Additional information

Used terms: z

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

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 26:

  rmdup((a ' + x0) + y) \ z ≠ rmdup(((a ' + x0) \ z) + (y \ z)), ∀ y0, z0. rmdup(x0 + y0) \ z0 = rmdup((x0 \ z0) + (y0 \ z0)) ⊦

Rule argument

Additional information

Used simplifier rules: union: ⊦ x ∪ y = rmdup(x + y); assoc: ⊦ (x ∪ y) ∪ z = x ∪ y ∪ z; ⊦ a + x = a ' + x; (s)

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

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 27:

  ⊦ rmdup(a ' + x) = (a ∈ x ⊃ rmdup(x);a ' + rmdup(x))

• Proof step 28:

  (a ∈ x0 + y ⊃ rmdup(x0 + y);a ' + rmdup(x0 + y)) \ z ≠ rmdup(((a ' + x0) \ z) + (y \ z)), ∀ y0, z0. rmdup(x0 + y0) \ z0 = rmdup((x0 \ z0) + (y0 \ z0)) ⊦

Rule argument

Additional information

Used simplifier rules: a: ⊦ (x + y) + z = x + y + z; from specification polylist Used terms: x0 + y, a

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

A spec-lemma

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

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 29:

  (a ∈ x0 ∨ a ∈ y ⊃ rmdup(x0 + y);a ' + rmdup(x0 + y)) \ z ≠ rmdup(((a ' + x0) \ z) + (y \ z)), ∀ y0, z0. rmdup(x0 + y0) \ z0 = rmdup((x0 \ z0) + (y0 \ z0)) ⊦

Rule argument

Additional information

Used simplifier rules: a: ⊦ (x + y) + z = x + y + z; from specification polylist ⊦ a ∈ x + y ↔ a ∈ x ∨ a ∈ y; (s)

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

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 30:

  ⊦ ¬ a ∈ y → (a ' + x) \ y = a + (x \ y)

• Proof step 31:

  (a ∈ x0 ∨ a ∈ y ⊃ rmdup(x0 + y);a ' + rmdup(x0 + y)) \ z ≠ rmdup(((a ' + x0) \ z) + (y \ z)), a ∈ z, ∀ y0, z0. rmdup(x0 + y0) \ z0 = rmdup((x0 \ z0) + (y0 \ z0)) ⊦

• Proof step 35:

  (a ∈ x0 ∨ a ∈ y ⊃ rmdup(x0 + y);a ' + rmdup(x0 + y)) \ z ≠ rmdup((a + (x0 \ z)) + (y \ z)), ¬ a ∈ z, ∀ y0, z0. rmdup(x0 + y0) \ z0 = rmdup((x0 \ z0) + (y0 \ z0)) ⊦

Rule argument

Additional information

Used terms: z, x0, a

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

Lemma diff-n

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

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 32:

  (a ∈ x0 ∨ a ∈ y ⊃ rmdup(x0 + y);a ' + rmdup(x0 + y)) \ z ≠ rmdup((x0 \ z) + (y \ z)), a ∈ z, ∀ y0, z0. rmdup(x0 + y0) \ z0 = rmdup((x0 \ z0) + (y0 \ z0)) ⊦

Rule argument

Additional information

Used simplifier rules: diff-y: ⊦ a ∈ y → (a ' + x) \ y = x \ y; a: ⊦ (x + y) + z = x + y + z; from specification polylist

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

User applied rule case distinction

And obtained the following new goals

• Proof step 33:

  rmdup(x0 + y) \ z ≠ rmdup((x0 \ z) + (y \ z)), a ∈ z, ∀ y0, z0. rmdup(x0 + y0) \ z0 = rmdup((x0 \ z0) + (y0 \ z0)), a ∈ x0 ∨ a ∈ y ⊦

• Proof step 34:

  (a ' + rmdup(x0 + y)) \ z ≠ rmdup((x0 \ z) + (y \ z)), a ∈ z, ¬ a ∈ y, ¬ a ∈ x0, ∀ y0, z0. rmdup(x0 + y0) \ z0 = rmdup((x0 \ z0) + (y0 \ z0)) ⊦

Rule argument

Additional information

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

Heuristic quantifier closing applied rule all left

And closed the goal!

Rule argument

Additional information

Used terms: y, z

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

Heuristic quantifier closing applied rule all left

And closed the goal!

Rule argument

Additional information

Used simplifier rules: diff-y: ⊦ a ∈ y → (a ' + x) \ y = x \ y; a: ⊦ (x + y) + z = x + y + z; from specification polylist Used terms: y, z

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

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 36:

  (a ∈ x0 ∨ a ∈ y ⊃ rmdup(x0 + y);a ' + rmdup(x0 + y)) \ z ≠ rmdup((a ' + (x0 \ z)) + (y \ z)), ¬ a ∈ z, ∀ y0, z0. rmdup(x0 + y0) \ z0 = rmdup((x0 \ z0) + (y0 \ z0)) ⊦

Rule argument

Additional information

Used simplifier rules: ⊦ a + x = a ' + x; (s)

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

User applied rule case distinction

And obtained the following new goals

• Proof step 37:

  rmdup(x0 + y) \ z ≠ rmdup((a ' + (x0 \ z)) + (y \ z)), ¬ a ∈ z, ∀ y0, z0. rmdup(x0 + y0) \ z0 = rmdup((x0 \ z0) + (y0 \ z0)), a ∈ x0 ∨ a ∈ y ⊦

• Proof step 42:

  (a ' + rmdup(x0 + y)) \ z ≠ rmdup((a ' + (x0 \ z)) + (y \ z)), ¬ a ∈ y, ¬ a ∈ x0, ¬ a ∈ z, ∀ y0, z0. rmdup(x0 + y0) \ z0 = rmdup((x0 \ z0) + (y0 \ z0)) ⊦

Rule argument

Additional information

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

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 38:

  rmdup(x0 + y) \ z ≠ rmdup((a ' + (x0 \ z)) + (y \ z)), ¬ a ∈ z, ∀ y0, z0. rmdup(x0 + y0) \ z0 = rmdup((x0 \ z0) + (y0 \ z0)), a ∈ x0 ∨ a ∈ y ⊦

Rule argument

Additional information

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

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 39:

  ⊦ ¬ a ∈ x → rmdup(a ' + x) = a + rmdup(x)

• Proof step 40:

  rmdup(x0 + y) \ z ≠ rmdup((a ' + (x0 \ z)) + (y \ z)), a ∈ (x0 \ z) + (y \ z), ¬ a ∈ z, ∀ y0, z0. rmdup(x0 + y0) \ z0 = rmdup((x0 \ z0) + (y0 \ z0)), a ∈ x0 ∨ a ∈ y ⊦

Rule argument

Additional information

Used simplifier rules: diff-in: ⊦ a ∈ x \ y ↔ a ∈ x ∧ ¬ a ∈ y; ⊦ a + x = a ' + x; (s) ⊦ a ∈ x + y ↔ a ∈ x ∨ a ∈ y; (s) a: ⊦ (x + y) + z = x + y + z; from specification polylist Used terms: (x0 \ z) + (y \ z), a

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

A spec-lemma

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

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 41:

  rmdup(x0 + y) \ z ≠ rmdup((x0 \ z) + (y \ z)), ¬ a ∈ z, ∀ y0, z0. rmdup(x0 + y0) \ z0 = rmdup((x0 \ z0) + (y0 \ z0)), a ∈ x0 ∨ a ∈ y, a ∈ x0 \ z ∨ a ∈ y \ z ⊦

Rule argument

Additional information

Used simplifier rules: a: ⊦ (x + y) + z = x + y + z; from specification polylist ⊦ a ∈ x + y ↔ a ∈ x ∨ a ∈ y; (s) ⊦ a ∈ x → rmdup(a ' + x) = rmdup(x); (s)

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

Heuristic quantifier closing applied rule all left

And closed the goal!

Rule argument

Additional information

Used terms: y, z

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

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 43:

  a ' + (rmdup(x0 + y) \ z) ≠ rmdup((a ' + (x0 \ z)) + (y \ z)), ¬ a ∈ y, ¬ a ∈ x0, ¬ a ∈ z, ∀ y0, z0. rmdup(x0 + y0) \ z0 = rmdup((x0 \ z0) + (y0 \ z0)) ⊦

Rule argument

Additional information

Used simplifier rules: diff-n: ⊦ ¬ a ∈ y → (a ' + x) \ y = a + (x \ y); a: ⊦ (x + y) + z = x + y + z; from specification polylist ⊦ a + x = a ' + x; (s)

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

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 44:

  ⊦ ¬ a ∈ x → rmdup(a ' + x) = a + rmdup(x)

• Proof step 45:

  a ' + (rmdup(x0 + y) \ z) ≠ a + rmdup((x0 \ z) + (y \ z)), ¬ a ∈ (x0 \ z) + (y \ z), ¬ a ∈ y, ¬ a ∈ x0, ¬ a ∈ z, ∀ y0, z0. rmdup(x0 + y0) \ z0 = rmdup((x0 \ z0) + (y0 \ z0)) ⊦

Rule argument

Additional information

Used simplifier rules: diff-in: ⊦ a ∈ x \ y ↔ a ∈ x ∧ ¬ a ∈ y; ⊦ a ∈ x → rmdup(a ' + x) = rmdup(x); (s) ⊦ a ∈ x + y ↔ a ∈ x ∨ a ∈ y; (s) a: ⊦ (x + y) + z = x + y + z; from specification polylist Used terms: (x0 \ z) + (y \ z), a

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

A spec-lemma

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

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 46:

  rmdup(x0 + y) \ z ≠ rmdup((x0 \ z) + (y \ z)), ¬ a ∈ y, ¬ a ∈ x0, ¬ a ∈ z, ∀ y0, z0. rmdup(x0 + y0) \ z0 = rmdup((x0 \ z0) + (y0 \ z0)) ⊦

Rule argument

Additional information

Used simplifier rules: diff-in: ⊦ a ∈ x \ y ↔ a ∈ x ∧ ¬ a ∈ y; a: ⊦ (x + y) + z = x + y + z; from specification polylist ⊦ a ∈ x + y ↔ a ∈ x ∨ a ∈ y; (s) ⊦ x + y = x + z ↔ y = z; (s) ⊦ a + x = a ' + x; (s)

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

Heuristic quantifier closing applied rule all left

And closed the goal!

Rule argument

Additional information

Used terms: y, z