Proof step 1 from proof del1-01 (conclusion) (back to tree)

System applied rule normalize

And obtained the following new goals

• Proof step 2:

  x.distinct intersect (y -1l a) ≠ x.distinct intersect y, ¬ a ∈ x ⊦

Rule argument

Additional information

Proof step 2 from proof del1-01 (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 3:

  x.distinct intersect (y -1l a) ≠ x.distinct intersect y, ¬ a ∈ x ⊦

Rule argument

Additional information

Proof step 3 from proof del1-01 (previous step) (back to tree)

User applied rule structural induction

And obtained the following new goals

• Proof step 4:

  (a0 + x0).distinct intersect (y -1l a) ≠ (a0 + x0).distinct intersect y, ¬ a ∈ a0 + x0, ∀ y, a. ¬(x0.distinct intersect (y -1l a) ≠ x0.distinct intersect y ∧ ¬ a ∈ x0) ⊦

Rule argument

Additional information

Used simplifier rules: inters-e: ⊦ [] intersect y = []; List[A] freely generated by [], +; ⊦ [].distinct = []; (s)

Proof step 4 from proof del1-01 (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 5:

  a ≠ a0, (a0 ' + x0).distinct intersect (y -1l a) ≠ (a0 ' + x0).distinct intersect y, ¬ a ∈ x0, ∀ y0, a1. x0.distinct intersect (y0 -1l a1) = x0.distinct intersect y0 ∨ a1 ∈ x0 ⊦

Rule argument

Additional information

Used simplifier rules: a: ⊦ (x + y) + z = x + y + z; from specification polylist ⊦ a ∈ a0 ' + x ↔ ¬(a ≠ a0 ∧ ¬ a ∈ x); (ss) ⊦ a + x = a ' + x; (s)

Proof step 5 from proof del1-01 (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 6:

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

• Proof step 7:

  a ≠ a0, (a0 ∈ x0 ⊃ x0.distinct;a0 ' + x0.distinct) intersect (y -1l a) ≠ (a0 ∈ x0 ⊃ x0.distinct;a0 ' + x0.distinct) intersect y, ¬ a ∈ x0, ∀ y0, a1. x0.distinct intersect (y0 -1l a1) = x0.distinct intersect y0 ∨ a1 ∈ x0 ⊦

Rule argument

Additional information

Used terms: x0, a0

Proof step 6 from proof del1-01 (previous step) (back to tree)

A spec-lemma

Proof step 7 from proof del1-01 (previous step) (back to tree)

Heuristic cut applied rule cut formula

And obtained the following new goals

• Proof step 8:

  a ≠ a0, (a0 ∈ x0 ⊃ x0.distinct;a0 ' + x0.distinct) intersect (y -1l a) ≠ (a0 ∈ x0 ⊃ x0.distinct;a0 ' + x0.distinct) intersect y, a0 ∈ x0, ¬ a ∈ x0, ∀ y0, a1. x0.distinct intersect (y0 -1l a1) = x0.distinct intersect y0 ∨ a1 ∈ x0 ⊦

• Proof step 10:

  a ≠ a0, (a0 ∈ x0 ⊃ x0.distinct;a0 ' + x0.distinct) intersect (y -1l a) ≠ (a0 ∈ x0 ⊃ x0.distinct;a0 ' + x0.distinct) intersect y, ¬ a0 ∈ x0, ¬ a ∈ x0, ∀ y0, a1. x0.distinct intersect (y0 -1l a1) = x0.distinct intersect y0 ∨ a1 ∈ x0 ⊦

Rule argument

Additional information

Used formulas: a0 ∈ x0

Proof step 8 from proof del1-01 (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 9:

  a ≠ a0, x0.distinct intersect (y -1l a) ≠ x0.distinct intersect y, a0 ∈ x0, ¬ a ∈ x0, ∀ y0, a1. x0.distinct intersect (y0 -1l a1) = x0.distinct intersect y0 ∨ a1 ∈ x0 ⊦

Rule argument

Additional information

Proof step 9 from proof del1-01 (previous step) (back to tree)

Heuristic quantifier closing applied rule all left

And closed the goal!

Rule argument

Additional information

Used terms: y, a

Proof step 10 from proof del1-01 (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 11:

  a ≠ a0, (a0 ' + x0.distinct) intersect (y -1l a) ≠ (a0 ' + x0.distinct) intersect y, ¬ a0 ∈ x0, ¬ a ∈ x0, ∀ y0, a1. x0.distinct intersect (y0 -1l a1) = x0.distinct intersect y0 ∨ a1 ∈ x0 ⊦

Rule argument

Additional information

Proof step 11 from proof del1-01 (previous step) (back to tree)

Heuristic cut applied rule cut formula

And obtained the following new goals

• Proof step 12:

  a ≠ a0, (a0 ' + x0.distinct) intersect (y -1l a) ≠ (a0 ' + x0.distinct) intersect y, a0 ∈ y -1l a, ¬ a0 ∈ x0, ¬ a ∈ x0, ∀ y0, a1. x0.distinct intersect (y0 -1l a1) = x0.distinct intersect y0 ∨ a1 ∈ x0 ⊦

• Proof step 14:

  a ≠ a0, (a0 ' + x0.distinct) intersect (y -1l a) ≠ (a0 ' + x0.distinct) intersect y, ¬ a0 ∈ y -1l a, ¬ a0 ∈ x0, ¬ a ∈ x0, ∀ y0, a1. x0.distinct intersect (y0 -1l a1) = x0.distinct intersect y0 ∨ a1 ∈ x0 ⊦

Rule argument

Additional information

Used formulas: a0 ∈ y -1l a

Proof step 12 from proof del1-01 (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 13:

  a ≠ a0, x0.distinct intersect (y -1l a) ≠ x0.distinct intersect y, a0 ∈ y, ¬ a0 ∈ x0, ¬ a ∈ x0, ∀ y0, a1. x0.distinct intersect (y0 -1l a1) = x0.distinct intersect y0 ∨ a1 ∈ x0 ⊦

Rule argument

Additional information

Used simplifier rules: inters-y: ⊦ a ∈ y → (a ' + x) intersect y = a ' + (x intersect y); a: ⊦ (x + y) + z = x + y + z; from specification polylist ⊦ x + y = x + z ↔ y = z; (s) ⊦ a ≠ b → (a ∈ x -1l b ↔ a ∈ x); (s)

Proof step 13 from proof del1-01 (previous step) (back to tree)

Heuristic quantifier closing applied rule all left

And closed the goal!

Rule argument

Additional information

Used terms: y, a

Proof step 14 from proof del1-01 (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 15:

  a ≠ a0, x0.distinct intersect (y -1l a) ≠ x0.distinct intersect y, ¬ a0 ∈ x0, ¬ a ∈ x0, ¬ a0 ∈ y, ∀ y0, a1. x0.distinct intersect (y0 -1l a1) = x0.distinct intersect y0 ∨ a1 ∈ x0 ⊦

Rule argument

Additional information

Used simplifier rules: inters-n: ⊦ ¬ a ∈ y → (a ' + x) intersect y = x intersect y; a: ⊦ (x + y) + z = x + y + z; from specification polylist ⊦ a ≠ b → (a ∈ x -1l b ↔ a ∈ x); (s)

Proof step 15 from proof del1-01 (previous step) (back to tree)

Heuristic quantifier closing applied rule all left

And closed the goal!

Rule argument

Additional information

Used terms: y, a