Proof step 1 from proof first-02 (conclusion) (back to tree)

System applied rule normalize

And obtained the following new goals

• Proof step 2:

  (x + a ' + y).head ≠ (x + a ').head ⊦

Rule argument

Additional information

Proof step 2 from proof first-02 (previous step) (back to tree)

Heuristic elimination applied rule apply elim lemma

And obtained the following new goals

• Proof step 3:

  x + a ' + y = a0 + y0, x + a ' + y ≠ [], a0 ≠ (x + a ').head ⊦

Rule argument

Additional information

Used simplifier rules: e-03: ⊦ x + a ' + y ≠ []; a: ⊦ (x + y) + z = x + y + z; x ≠ [] ⊦ a = x.head ∧ y = x.tail ↔ x = a + y; (elim) Used terms: x + a ' + y, a0, y0

Proof step 3 from proof first-02 (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 4:

  x + a ' + y = a0 ' + y0, a0 ≠ (x + a ').head, a0 ∈ x ∨ a0 = a ∨ a0 ∈ y ⊦

Rule argument

Additional information

Used simplifier rules: c: ⊦ a + x = a ' + x; e-03: ⊦ x + a ' + y ≠ []; in-14: ⊦ a ' + x = y → a ∈ y; in-append: ⊦ a ∈ x + y ↔ a ∈ x ∨ a ∈ y; in-17: ⊦ a ∈ b ' ↔ a = b; a: ⊦ (x + y) + z = x + y + z;

Proof step 4 from proof first-02 (previous step) (back to tree)

Heuristic elimination applied rule apply elim lemma

And obtained the following new goals

• Proof step 5:

  x + a ' + y = a0 ' + y0, x + a ' = a1 + y1, x + a ' ≠ [], a0 ≠ a1, a0 ∈ x ∨ a0 = a ∨ a0 ∈ y ⊦

Rule argument

Additional information

Used simplifier rules: e-02: ⊦ x + a ' ≠ []; a: ⊦ (x + y) + z = x + y + z; x ≠ [] ⊦ a = x.head ∧ y = x.tail ↔ x = a + y; (elim) Used terms: x + a ', a1, y1

Proof step 5 from proof first-02 (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 6:

  x + a ' = a1 ' + y1, x + a ' + y = a0 ' + y0, a0 ≠ a1, a0 ∈ x ∨ a0 = a ∨ a0 ∈ y, a = a1 ∨ a ∈ y1, a1 ∈ x ∨ a1 = a ⊦

Rule argument

Additional information

Used simplifier rules: c: ⊦ a + x = a ' + x; e-02: ⊦ x + a ' ≠ []; in-15: ⊦ x + a ' = y → a ∈ y; in-14: ⊦ a ' + x = y → a ∈ y; in-append: ⊦ a ∈ x + y ↔ a ∈ x ∨ a ∈ y; in-17: ⊦ a ∈ b ' ↔ a = b; a: ⊦ (x + y) + z = x + y + z;

Proof step 6 from proof first-02 (previous step) (back to tree)

Heuristic structural induction applied rule structural induction

And closed the goal!

Rule argument

Additional information

Used simplifier rules: c-03: ⊦ a ' = b ' + x ↔ a = b ∧ x = []; Nil: ⊦ [] + x = x; c-06: ⊦ a ' + x = b ' + y ↔ a = b ∧ x = y; a: ⊦ (x + y) + z = x + y + z; c: ⊦ a + x = a ' + x; c-06: ⊦ a ' + x = b ' + y ↔ a = b ∧ x = y; a: ⊦ (x + y) + z = x + y + z; list freely generated by [], +;;