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

System applied rule normalize

And obtained the following new goals

• Proof step 2:

  x + a ' + b ' + y + c ' + z = x0 + a ' + c ' + z0, a ≠ b, b ≠ c, ¬ dups(x + a ' + c ' + z), ¬ a ∈ y ⊦

Rule argument

Additional information

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

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 3:

  x + a ' + b ' + y + c ' + z = x0 + a ' + c ' + z0, a ≠ b, a ≠ c, b ≠ c, ¬ dups(x + z), ¬ a ∈ y, ¬ a ∈ x, ¬ a ∈ z, ¬ c ∈ x, ¬ c ∈ z ⊦

Rule argument

Additional information

Used simplifier rules: f-01: ⊦ dups(x + a ' + y) ↔ a ∈ x ∨ a ∈ y ∨ dups(x + y); a: ⊦ (x + y) + z = x + y + z; from specification list ⊦ a ∈ b ' + x ↔ a = b ∨ a ∈ x; (s)

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

User applied rule structural induction

And obtained the following new goals

• Proof step 4:

  [] + a ' + b ' + y + c ' + z = x0 + a ' + c ' + z0, a ≠ b, a ≠ c, b ≠ c, ¬ dups([] + z), ¬ a ∈ y, ¬ a ∈ [], ¬ a ∈ z, ¬ c ∈ [], ¬ c ∈ z ⊦

• Proof step 12:

  (a0 + x1) + a ' + b ' + y + c ' + z = x0 + a ' + c ' + z0, a ≠ b, a ≠ c, b ≠ c, ¬ dups((a0 + x1) + z), ¬ a ∈ y, ¬ a ∈ a0 + x1, ¬ a ∈ z, ¬ c ∈ a0 + x1, ¬ c ∈ z, ∀ a, b, y, c, z, x0, z0. ¬(x1 + a ' + b ' + y + c ' + z = x0 + a ' + c ' + z0 ∧ a ≠ b ∧ a ≠ c ∧ b ≠ c ∧ ¬ dups(x1 + z) ∧ ¬ a ∈ y ∧ ¬ a ∈ x1 ∧ ¬ a ∈ z ∧ ¬ c ∈ x1 ∧ ¬ c ∈ z) ⊦

Rule argument

Additional information

Used simplifier rules: list freely generated by [], +;;

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

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 5:

  a ' + b ' + y + c ' + z = x0 + a ' + c ' + z0, a ≠ c, a ≠ b, b ≠ c, ¬ dups(z), ¬ c ∈ z, ¬ a ∈ z, ¬ a ∈ y ⊦

Rule argument

Additional information

Used simplifier rules: a: ⊦ (x + y) + z = x + y + z; from specification list ⊦ a ∈ b ' + x ↔ a = b ∨ a ∈ x; (s) ⊦ a ∈ x + y ↔ a ∈ x ∨ a ∈ y; (s) in-14: ⊦ a ' + x = y → a ∈ y; (forward) from specification list ⊦ ¬ a ∈ []; (s) ⊦ [] + x = x; (s)

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

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 6:

  y ≠ [] ⊦ a ' + x = y + z ↔ a = y.head ∧ x = y.tail + z

• Proof step 7:

  b ' + y + c ' + z = x0.tail + a ' + c ' + z0, a = x0.head, a ≠ c, a ≠ b, b ≠ c, x0 ≠ [], ¬ dups(z), ¬ c ∈ z, ¬ a ∈ z, ¬ a ∈ y ⊦

Rule argument

Additional information

Used simplifier rules: ⊦ [] + x = x; (s) ⊦ a ' + x = a ' + y ↔ x = y; (s) ⊦ a ' + x = b ' + y ↔ a = b ∧ x = y; (ws) a: ⊦ (x + y) + z = x + y + z; from specification list Used terms: a ' + c ' + z0, x0, b ' + y + c ' + z, a

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

A spec-lemma

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

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 8:

  b ' + y + c ' + z = x0.tail + x0.head ' + c ' + z0, x0.head ≠ b, x0.head ≠ c, b ≠ c, x0 ≠ [], b ∈ x0.tail, ¬ dups(z), ¬ x0.head ∈ y, ¬ x0.head ∈ z, ¬ c ∈ z ⊦

Rule argument

Additional information

Used simplifier rules: a: ⊦ (x + y) + z = x + y + z; from specification list ⊦ ¬ a ∈ y → (y + c ' + z = a ' + z0 ↔ y = [] ∧ c = a ∧ z = z0); (ws) ⊦ a ≠ b → (a ∈ b ' + x ↔ a ∈ x); (s) ⊦ a ∈ x + y ↔ a ∈ x ∨ a ∈ y; (s) in-14: ⊦ a ' + x = y → a ∈ y; (forward) from specification list

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

Heuristic elimination applied rule apply elim lemma

And obtained the following new goals

• Proof step 9:

  b ' + y + c ' + z = y0 + a ' + c ' + z0, x0 = a + y0, a ≠ b, a ≠ c, b ≠ c, x0 ≠ [], b ∈ y0, ¬ dups(z), ¬ a ∈ y, ¬ a ∈ z, ¬ c ∈ z ⊦

Rule argument

Additional information

Used simplifier rules: x ≠ [] ⊦ a = x.head ∧ y = x.tail ↔ x = a + y; (elim) Used terms: x0, a, y0

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

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 10:

  b ' + y + c ' + z = y0 + a ' + c ' + z0, a ≠ c, a ≠ b, b ≠ c, b ∈ y0, ¬ dups(z), ¬ c ∈ z, ¬ a ∈ z, ¬ a ∈ y ⊦

Rule argument

Additional information

Used simplifier rules: a: ⊦ (x + y) + z = x + y + z; from specification list ⊦ a ∈ x → a ∈ x + y; (s) in-14: ⊦ a ' + x = y → a ∈ y; (forward) from specification list ⊦ a ' + x ≠ []; (s) ⊦ a + x = a ' + x; (s)

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

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 11:

  y ≠ [] ⊦ a ' + x = y + z ↔ a = y.head ∧ x = y.tail + z

Rule argument

Additional information

Used simplifier rules: ⊦ ¬ a ∈ y ∧ ¬ a ∈ z ∧ a ≠ c → y + c ' + z ≠ y1 + a ' + x; (s) a: ⊦ (x + y) + z = x + y + z; from specification list ⊦ [] + x = x; (s) ⊦ a ' + x = b ' + y ↔ a = b ∧ x = y; (ws) Used terms: a ' + c ' + z0, y0, y + c ' + z, b

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

A spec-lemma

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

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 13:

  (a0 ' + x1) + a ' + b ' + y + c ' + z = x0 + a ' + c ' + z0, a ≠ a0, a ≠ c, a ≠ b, b ≠ c, c ≠ a0, a0 ∈ x0, ¬ dups(x1 + z), ¬ c ∈ x1, ¬ a ∈ z, ¬ a ∈ x1, ¬ a ∈ y, ¬ a0 ∈ z, ¬ a0 ∈ x1, ¬ c ∈ z, ∀ a1, b0, y0, c0, z1, x, z2. x1 + a1 ' + b0 ' + y0 + c0 ' + z1 ≠ x + a1 ' + c0 ' + z2 ∨ a1 = b0 ∨ a1 = c0 ∨ b0 = c0 ∨ dups(x1 + z1) ∨ a1 ∈ y0 ∨ a1 ∈ x1 ∨ a1 ∈ z1 ∨ c0 ∈ x1 ∨ c0 ∈ z1 ⊦

Rule argument

Additional information

Used simplifier rules: rec: ⊦ dups(a ' + x) ↔ a ∈ x ∨ dups(x); a: ⊦ (x + y) + z = x + y + z; from specification list ⊦ ¬ a ∈ y → (y + c ' + z = a ' + z0 ↔ y = [] ∧ c = a ∧ z = z0); (ws) ⊦ a ≠ b → (a ∈ b ' + x ↔ a ∈ x); (s) ⊦ a ∈ x + y ↔ a ∈ x ∨ a ∈ y; (s) in-14: ⊦ a ' + x = y → a ∈ y; (forward) from specification list ⊦ a ∈ b ' + x ↔ ¬(a ≠ b ∧ ¬ a ∈ x); (ss) ⊦ a + x = a ' + x; (s)

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

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 14:

  y ≠ [] ⊦ a ' + x = y + z ↔ a = y.head ∧ x = y.tail + z

• Proof step 15:

  x1 + a ' + b ' + y + c ' + z = (x0 + a ' + c ').tail + z0, a0 = (x0 + a ' + c ').head, x0 + a ' + c ' ≠ [], a ≠ a0, a ≠ c, a ≠ b, b ≠ c, c ≠ a0, a0 ∈ x0, ¬ dups(x1 + z), ¬ c ∈ x1, ¬ a ∈ z, ¬ a ∈ x1, ¬ a ∈ y, ¬ a0 ∈ z, ¬ a0 ∈ x1, ¬ c ∈ z, ∀ a1, b0, y0, c0, z1, x, z2. x1 + a1 ' + b0 ' + y0 + c0 ' + z1 ≠ x + a1 ' + c0 ' + z2 ∨ a1 = b0 ∨ a1 = c0 ∨ b0 = c0 ∨ dups(x1 + z1) ∨ a1 ∈ y0 ∨ a1 ∈ x1 ∨ a1 ∈ z1 ∨ c0 ∈ x1 ∨ c0 ∈ z1 ⊦

Rule argument

Additional information

Used simplifier rules: ⊦ x + y = [] ↔ x = [] ∧ y = []; (as) ⊦ a ' + x ≠ []; (s) a: ⊦ (x + y) + z = x + y + z; from specification list Used terms: z0, x0 + a ' + c ', x1 + a ' + b ' + y + c ' + z, a0

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

A spec-lemma

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

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 16:

  x1 + a ' + b ' + y + c ' + z = (x0 + a ' + c ').tail + z0, a ≠ x0.head, a ≠ c, a ≠ b, b ≠ c, c ≠ x0.head, (x0 + a ').head ∈ x0, ¬ dups(x1 + z), ¬ c ∈ z, ¬ c ∈ x1, ¬ a ∈ z, ¬ a ∈ x1, ¬ a ∈ y, ¬ x0.head ∈ z, ¬ x0.head ∈ x1, ∀ a1, b0, y0, c0, z1, x, z2. x1 + a1 ' + b0 ' + y0 + c0 ' + z1 ≠ x + a1 ' + c0 ' + z2 ∨ a1 = b0 ∨ a1 = c0 ∨ b0 = c0 ∨ dups(x1 + z1) ∨ a1 ∈ y0 ∨ a1 ∈ x1 ∨ a1 ∈ z1 ∨ c0 ∈ x1 ∨ c0 ∈ z1 ⊦

Rule argument

Additional information

Used simplifier rules: a: ⊦ (x + y) + z = x + y + z; from specification list ⊦ a ∈ x → (x + y).head = x.head; (s) ⊦ (x + a ' + y).head = (x + a ').head; (s) ⊦ x + a ' ≠ []; (s)

Proof step 16 from proof eq-01 (previous step) (back to tree)

Heuristic elimination applied rule apply elim lemma

And obtained the following new goals

• Proof step 17:

  x1 + a ' + b ' + y + c ' + z = (x0 + a ' + c ').tail + z0, x0 = a0 + y1, a ≠ a0, a ≠ c, a ≠ b, b ≠ c, c ≠ a0, x0 ≠ [], (x0 + a ').head ∈ x0, ¬ dups(x1 + z), ¬ c ∈ z, ¬ c ∈ x1, ¬ a ∈ z, ¬ a ∈ x1, ¬ a ∈ y, ¬ a0 ∈ z, ¬ a0 ∈ x1, ∀ a1, b0, y0, c0, z1, x, z2. x1 + a1 ' + b0 ' + y0 + c0 ' + z1 ≠ x + a1 ' + c0 ' + z2 ∨ a1 = b0 ∨ a1 = c0 ∨ b0 = c0 ∨ dups(x1 + z1) ∨ a1 ∈ y0 ∨ a1 ∈ x1 ∨ a1 ∈ z1 ∨ c0 ∈ x1 ∨ c0 ∈ z1 ⊦

Rule argument

Additional information

Used simplifier rules: ⊦ [] + x = x; (s) ⊦ (a ' + x).tail = x; (s) ⊦ ¬ a ∈ y → (y + c ' + z = a ' + z0 ↔ y = [] ∧ c = a ∧ z = z0); (ws) a: ⊦ (x + y) + z = x + y + z; from specification list x ≠ [] ⊦ a = x.head ∧ y = x.tail ↔ x = a + y; (elim) Used terms: x0, a0, y1

Proof step 17 from proof eq-01 (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 18:

  x1 + a ' + b ' + y + c ' + z = (y1 + a ' + c ') + z0, a ≠ a0, a ≠ c, a ≠ b, b ≠ c, c ≠ a0, ¬ dups(x1 + z), ¬ c ∈ z, ¬ c ∈ x1, ¬ a ∈ z, ¬ a ∈ x1, ¬ a ∈ y, ¬ a0 ∈ z, ¬ a0 ∈ x1, ∀ a1, b0, y0, c0, z1, x, z2. x1 + a1 ' + b0 ' + y0 + c0 ' + z1 ≠ x + a1 ' + c0 ' + z2 ∨ a1 = b0 ∨ a1 = c0 ∨ b0 = c0 ∨ dups(x1 + z1) ∨ a1 ∈ y0 ∨ a1 ∈ x1 ∨ a1 ∈ z1 ∨ c0 ∈ x1 ∨ c0 ∈ z1 ⊦

Rule argument

Additional information

Used simplifier rules: a: ⊦ (x + y) + z = x + y + z; from specification list ⊦ a ∈ b ' + x ↔ a = b ∨ a ∈ x; (s) ⊦ a + x = a ' + x; (s) ⊦ (a ' + x).head = a; (s) ⊦ a ' + x ≠ []; (s) ⊦ (a ' + x).tail = x; (s)

Proof step 18 from proof eq-01 (previous step) (back to tree)

User applied rule all left

And closed the goal!

Rule argument

Additional information

Used simplifier rules: a: ⊦ (x + y) + z = x + y + z; from specification list Used terms: a, b, y, c, z, y1, z0