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

System applied rule normalize

And obtained the following new goals

• Proof step 2:

  filter(rmdup(x), y -1l a) ≠ filter(rmdup(x), 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:

  filter(rmdup(x), y -1l a) ≠ filter(rmdup(x), 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:

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

Rule argument

Additional information

Used simplifier rules: filt-e: ⊦ filter([], y) = []; list freely generated by [], +;; ⊦ rmdup([]) = []; (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, filter(rmdup(a0 ' + x0), y -1l a) ≠ filter(rmdup(a0 ' + x0), y), ¬ a ∈ x0, ∀ y0, a1. filter(rmdup(x0), y0 -1l a1) = filter(rmdup(x0), y0) ∨ a1 ∈ x0 ⊦

Rule argument

Additional information

Used simplifier rules: a: ⊦ (x + y) + z = x + y + z; from specification list ⊦ a ∈ b ' + x ↔ ¬(a ≠ b ∧ ¬ 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:

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

• Proof step 7:

  a ≠ a0, filter((a0 ∈ x0 ⊃ rmdup(x0);a0 ' + rmdup(x0)), y -1l a) ≠ filter((a0 ∈ x0 ⊃ rmdup(x0);a0 ' + rmdup(x0)), y), ¬ a ∈ x0, ∀ y0, a1. filter(rmdup(x0), y0 -1l a1) = filter(rmdup(x0), 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, filter((a0 ∈ x0 ⊃ rmdup(x0);a0 ' + rmdup(x0)), y -1l a) ≠ filter((a0 ∈ x0 ⊃ rmdup(x0);a0 ' + rmdup(x0)), y), a0 ∈ x0, ¬ a ∈ x0, ∀ y0, a1. filter(rmdup(x0), y0 -1l a1) = filter(rmdup(x0), y0) ∨ a1 ∈ x0 ⊦

• Proof step 10:

  a ≠ a0, filter((a0 ∈ x0 ⊃ rmdup(x0);a0 ' + rmdup(x0)), y -1l a) ≠ filter((a0 ∈ x0 ⊃ rmdup(x0);a0 ' + rmdup(x0)), y), ¬ a0 ∈ x0, ¬ a ∈ x0, ∀ y0, a1. filter(rmdup(x0), y0 -1l a1) = filter(rmdup(x0), 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, filter(rmdup(x0), y -1l a) ≠ filter(rmdup(x0), y), a0 ∈ x0, ¬ a ∈ x0, ∀ y0, a1. filter(rmdup(x0), y0 -1l a1) = filter(rmdup(x0), 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, filter(a0 ' + rmdup(x0), y -1l a) ≠ filter(a0 ' + rmdup(x0), y), ¬ a0 ∈ x0, ¬ a ∈ x0, ∀ y0, a1. filter(rmdup(x0), y0 -1l a1) = filter(rmdup(x0), 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, filter(a0 ' + rmdup(x0), y -1l a) ≠ filter(a0 ' + rmdup(x0), y), a0 ∈ y -1l a, ¬ a0 ∈ x0, ¬ a ∈ x0, ∀ y0, a1. filter(rmdup(x0), y0 -1l a1) = filter(rmdup(x0), y0) ∨ a1 ∈ x0 ⊦

• Proof step 14:

  a ≠ a0, filter(a0 ' + rmdup(x0), y -1l a) ≠ filter(a0 ' + rmdup(x0), y), ¬ a0 ∈ y -1l a, ¬ a0 ∈ x0, ¬ a ∈ x0, ∀ y0, a1. filter(rmdup(x0), y0 -1l a1) = filter(rmdup(x0), 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, filter(rmdup(x0), y -1l a) ≠ filter(rmdup(x0), y), a0 ∈ y, ¬ a0 ∈ x0, ¬ a ∈ x0, ∀ y0, a1. filter(rmdup(x0), y0 -1l a1) = filter(rmdup(x0), y0) ∨ a1 ∈ x0 ⊦

Rule argument

Additional information

Used simplifier rules: filt-y: ⊦ a ∈ y → filter(a ' + x, y) = a ' + filter(x, y); a: ⊦ (x + y) + z = x + y + z; from specification list ⊦ 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, filter(rmdup(x0), y -1l a) ≠ filter(rmdup(x0), y), ¬ a0 ∈ x0, ¬ a ∈ x0, ¬ a0 ∈ y, ∀ y0, a1. filter(rmdup(x0), y0 -1l a1) = filter(rmdup(x0), y0) ∨ a1 ∈ x0 ⊦

Rule argument

Additional information

Used simplifier rules: filt-n: ⊦ ¬ a ∈ y → filter(a ' + x, y) = filter(x, y); a: ⊦ (x + y) + z = x + y + z; from specification list ⊦ 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