Proof step 1 from proof neq-07 (conclusion) (back to tree)

System applied rule normalize

And obtained the following new goals

• Proof step 2:

  y1 + a0 ' + y0 + a ' = y2 + a ' + a1 ' + z0, a ≠ a1, a ≠ a0, a1 ≠ a0, ¬ a1 ∈ y0, ¬ a ∈ y1 ⊦

Rule argument

Additional information

Proof step 2 from proof neq-07 (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 3:

  y1 + a0 ' + y0 + a ' = y2 + a ' + a1 ' + z0, a ≠ a1, a ≠ a0, a1 ≠ a0, ¬ a1 ∈ y0, ¬ a ∈ y1 ⊦

Rule argument

Additional information

Proof step 3 from proof neq-07 (previous step) (back to tree)

User applied rule apply lemma

And obtained the following new goals

• Proof step 4:

  ⊦ x ≠ [] → (∃ y, a. x = y + a ')

• Proof step 5:

  y1 + a0 ' + y0 + a ' = y2 + a ' + a1 ' + z0, a ≠ a1, a ≠ a0, a1 ≠ a0, ¬ a1 ∈ y0, ¬ a ∈ y1, z0 ≠ [] → (∃ y, a. z0 = y + a ') ⊦

Rule argument

Additional information

Used terms: z0

Proof step 4 from proof neq-07 (previous step) (back to tree)

Lemma lastdiv

Proof step 5 from proof neq-07 (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 6:

  y1 + a0 ' + y0 = y2 + a2 ' + a1 ' + y, a1 ≠ a0, a2 ≠ a0, a2 ≠ a1, ¬ a2 ∈ y1, ¬ a1 ∈ y0 ⊦

Rule argument

Additional information

Used simplifier rules: app: ⊦ x + [] = x; app-06: ⊦ x + a ' = y + a0 ' ↔ x = y ∧ a = a0; e-02: ⊦ x + a ' ≠ []; a: ⊦ (x + y) + z = x + y + z;

Proof step 6 from proof neq-07 (previous step) (back to tree)

User applied rule structural induction

And obtained the following new goals

• Proof step 7:

  (a + y3) + a0 ' + y0 = y2 + a2 ' + a1 ' + y, a1 ≠ a0, a2 ≠ a0, a2 ≠ a1, ¬ a2 ∈ a + y3, ¬ a1 ∈ y0, ∀ a0, y0, y2, a2, a1, y. ¬(y3 + a0 ' + y0 = y2 + a2 ' + a1 ' + y ∧ a1 ≠ a0 ∧ a2 ≠ a0 ∧ a2 ≠ a1 ∧ ¬ a2 ∈ y3 ∧ ¬ a1 ∈ y0) ⊦

Rule argument

Additional information

Used simplifier rules: Nil: ⊦ [] + x = x; neq-02: ⊦ ¬ a ∈ z ∧ a ≠ a0 → a0 ' + z ≠ y1 + a ' + x; a: ⊦ (x + y) + z = x + y + z; list('a) freely generated by [], +;;

Proof step 7 from proof neq-07 (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 8:

  (a ' + y3) + a0 ' + y0 = y2 + a2 ' + a1 ' + y, a1 ≠ a0, a2 ≠ a0, a2 ≠ a1, a2 ≠ a, ¬ a1 ∈ y0, ¬ a2 ∈ y3, ∀ a3, y1, y4, a4, a5, y5. y3 + a3 ' + y1 ≠ y4 + a4 ' + a5 ' + y5 ∨ a5 = a3 ∨ a4 = a3 ∨ a4 = a5 ∨ a4 ∈ y3 ∨ a5 ∈ y1 ⊦

Rule argument

Additional information

Used simplifier rules: c: ⊦ a + x = a ' + x; in-06: ⊦ a ∈ a0 ' + x ↔ ¬(a ≠ a0 ∧ ¬ a ∈ x); a: ⊦ (x + y) + z = x + y + z;

Proof step 8 from proof neq-07 (previous step) (back to tree)

User applied rule constructor cut

And obtained the following new goals

• Proof step 9:

  (a ' + y3) + a0 ' + y0 = y2 + a2 ' + a1 ' + y, y2 = a6 + y6, a1 ≠ a0, a2 ≠ a0, a2 ≠ a1, a2 ≠ a, ¬ a1 ∈ y0, ¬ a2 ∈ y3, ∀ a3, y1, y4, a4, a5, y5. y3 + a3 ' + y1 ≠ y4 + a4 ' + a5 ' + y5 ∨ a5 = a3 ∨ a4 = a3 ∨ a4 = a5 ∨ a4 ∈ y3 ∨ a5 ∈ y1 ⊦

Rule argument

Additional information

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

Proof step 9 from proof neq-07 (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 10:

  y3 + a0 ' + y0 = y6 + a2 ' + a1 ' + y, a1 ≠ a0, a2 ≠ a, a2 ≠ a1, a2 ≠ a0, ¬ a2 ∈ y3, ¬ a1 ∈ y0, ∀ a3, y1, y4, a4, a5, y5. y3 + a3 ' + y1 ≠ y4 + a4 ' + a5 ' + y5 ∨ a5 = a3 ∨ a4 = a3 ∨ a4 = a5 ∨ a4 ∈ y3 ∨ a5 ∈ y1 ⊦

Rule argument

Additional information

Used simplifier rules: c: ⊦ a + x = a ' + x; c-06: ⊦ a ' + x = a0 ' + y ↔ a = a0 ∧ x = y; a: ⊦ (x + y) + z = x + y + z;

Proof step 10 from proof neq-07 (previous step) (back to tree)

User applied rule all left

And closed the goal!

Rule argument

Additional information

Used terms: a0, y0, y6, a2, a1, y