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:

  y.distinct \ z ≠ (y \ z).distinct ⊦

Rule argument

Additional information

Used simplifier rules: diff-e: ⊦ [] \ y = []; union: ⊦ x ∪ y = (x + y).distinct; 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:

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

Rule argument

Additional information

Used simplifier rules: diff-e: ⊦ [] \ y = []; List('a) freely generated by [], +;; ⊦ [].distinct = []; (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:

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

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:

  ⊦ (a ' + x).distinct = (a ∈ x ⊃ x.distinct;a ' + x.distinct)

• Proof step 8:

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

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:

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

• Proof step 15:

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

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:

  y0.distinct \ z = (y0 \ z).distinct, y0.distinct \ z ≠ ((a ' + y0) \ z).distinct, 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:

  y0.distinct \ z = (y0 \ z).distinct, y0.distinct \ z ≠ (a + (y0 \ z)).distinct, 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:

  y0.distinct \ z = (y0 \ z).distinct, y0.distinct \ z ≠ (a ' + (y0 \ z)).distinct, 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 → (a ' + x).distinct = a + x.distinct

Rule argument

Additional information

Used simplifier rules: diff-in: ⊦ a ∈ x \ y ↔ a ∈ x ∧ ¬ a ∈ y; ⊦ a + x = a ' + x; (s) ⊦ a ∈ x → (a ' + x).distinct = x.distinct; (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 ' + y0.distinct) \ z ≠ ((a ' + y0) \ z).distinct, ¬ a ∈ y0, ∀ z. y0.distinct \ z = (y0 \ z).distinct ⊦

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 ' + y0.distinct) \ z ≠ ((a ' + y0) \ z).distinct, a ∈ z, ¬ a ∈ y0, ∀ z. y0.distinct \ z = (y0 \ z).distinct ⊦

• Proof step 20:

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

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:

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

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 ' + (y0.distinct \ z) ≠ (a ' + (y0 \ z)).distinct, ¬ a ∈ z, ¬ a ∈ y0, ∀ z. y0.distinct \ z = (y0 \ z).distinct ⊦

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 → (a ' + x).distinct = a + x.distinct

• Proof step 23:

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

Rule argument

Additional information

Used simplifier rules: diff-in: ⊦ a ∈ x \ y ↔ a ∈ x ∧ ¬ a ∈ y; ⊦ a ∈ x → (a ' + x).distinct = x.distinct; (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:

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

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:

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

Rule argument

Additional information

Used simplifier rules: union: ⊦ x ∪ y = (x + y).distinct; 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:

  ⊦ (a ' + x).distinct = (a ∈ x ⊃ x.distinct;a ' + x.distinct)

• Proof step 28:

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

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 ⊃ (x0 + y).distinct;a ' + (x0 + y).distinct) \ z ≠ (((a ' + x0) \ z) + (y \ z)).distinct, ∀ y0, z0. (x0 + y0).distinct \ z0 = ((x0 \ z0) + (y0 \ z0)).distinct ⊦

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 ⊃ (x0 + y).distinct;a ' + (x0 + y).distinct) \ z ≠ (((a ' + x0) \ z) + (y \ z)).distinct, a ∈ z, ∀ y0, z0. (x0 + y0).distinct \ z0 = ((x0 \ z0) + (y0 \ z0)).distinct ⊦

• Proof step 35:

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

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 ⊃ (x0 + y).distinct;a ' + (x0 + y).distinct) \ z ≠ ((x0 \ z) + (y \ z)).distinct, a ∈ z, ∀ y0, z0. (x0 + y0).distinct \ z0 = ((x0 \ z0) + (y0 \ z0)).distinct ⊦

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:

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

• Proof step 34:

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

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 ⊃ (x0 + y).distinct;a ' + (x0 + y).distinct) \ z ≠ ((a ' + (x0 \ z)) + (y \ z)).distinct, ¬ a ∈ z, ∀ y0, z0. (x0 + y0).distinct \ z0 = ((x0 \ z0) + (y0 \ z0)).distinct ⊦

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:

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

• Proof step 42:

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

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:

  (x0 + y).distinct \ z ≠ ((a ' + (x0 \ z)) + (y \ z)).distinct, ¬ a ∈ z, ∀ y0, z0. (x0 + y0).distinct \ z0 = ((x0 \ z0) + (y0 \ z0)).distinct, 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 → (a ' + x).distinct = a + x.distinct

• Proof step 40:

  (x0 + y).distinct \ z ≠ ((a ' + (x0 \ z)) + (y \ z)).distinct, a ∈ (x0 \ z) + (y \ z), ¬ a ∈ z, ∀ y0, z0. (x0 + y0).distinct \ z0 = ((x0 \ z0) + (y0 \ z0)).distinct, 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:

  (x0 + y).distinct \ z ≠ ((x0 \ z) + (y \ z)).distinct, ¬ a ∈ z, ∀ y0, z0. (x0 + y0).distinct \ z0 = ((x0 \ z0) + (y0 \ z0)).distinct, 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 → (a ' + x).distinct = x.distinct; (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 ' + ((x0 + y).distinct \ z) ≠ ((a ' + (x0 \ z)) + (y \ z)).distinct, ¬ a ∈ y, ¬ a ∈ x0, ¬ a ∈ z, ∀ y0, z0. (x0 + y0).distinct \ z0 = ((x0 \ z0) + (y0 \ z0)).distinct ⊦

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 → (a ' + x).distinct = a + x.distinct

• Proof step 45:

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

Rule argument

Additional information

Used simplifier rules: diff-in: ⊦ a ∈ x \ y ↔ a ∈ x ∧ ¬ a ∈ y; ⊦ a ∈ x → (a ' + x).distinct = x.distinct; (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:

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

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