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 ≠ a0, a ≠ a1, a1 ≠ a0, ¬ a ∈ y1, ¬ a1 ∈ y0 ⊦

Rule argument

Additional information

Used simplifier rules: in-16: ⊦ x + a ' = y + b ' + z ∧ a ≠ b → a ∈ z; in-15: ⊦ x + a ' = y → a ∈ y; in-16: ⊦ x + a ' = y + b ' + z ∧ a ≠ b → a ∈ z; in-append: ⊦ a ∈ x + y ↔ a ∈ x ∨ a ∈ y; in-17: ⊦ a ∈ b ' ↔ a = b; a: ⊦ (x + y) + z = x + y + z;

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 ≠ a0, a ≠ a1, a1 ≠ a0, ¬ a ∈ y1, ¬ a1 ∈ y0, 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 ≠ a1, a2 ≠ a0, ¬ a1 ∈ y0, ¬ a2 ∈ y1 ⊦

Rule argument

Additional information

Used simplifier rules: app: ⊦ x + [] = x; in-15: ⊦ x + a ' = y → a ∈ y; app-06: ⊦ x + a ' = y + b ' ↔ x = y ∧ a = b; e-02: ⊦ x + a ' ≠ []; 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 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 ≠ a1, a2 ≠ a0, ¬ a1 ∈ y0, ¬ a2 ∈ a + y3, ∀ a0, y0, y2, a2, a1, y. ¬(y3 + a0 ' + y0 = y2 + a2 ' + a1 ' + y ∧ a1 ≠ a0 ∧ a2 ≠ a1 ∧ a2 ≠ a0 ∧ ¬ a1 ∈ y0 ∧ ¬ a2 ∈ y3) ⊦

Rule argument

Additional information

Used simplifier rules: Nil: ⊦ [] + x = x; neq-02: ⊦ ¬ a ∈ z ∧ a ≠ c → c ' + z ≠ y1 + a ' + x; a: ⊦ (x + y) + z = x + y + z; list 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 ≠ a, a2 ≠ a0, a2 ≠ a1, a ∈ y2, ¬ a2 ∈ y3, ¬ a1 ∈ y0, ∀ a3, y1, y4, a4, a5, y5. y3 + a3 ' + y1 ≠ y4 + a4 ' + a5 ' + y5 ∨ a5 = a3 ∨ a4 = a5 ∨ a4 = a3 ∨ a5 ∈ y1 ∨ a4 ∈ y3 ⊦

Rule argument

Additional information

Used simplifier rules: c: ⊦ a + x = a ' + x; in-06: ⊦ a ∈ b ' + x ↔ ¬(a ≠ b ∧ ¬ a ∈ x); in-14: ⊦ a ' + x = y → a ∈ y; in-01: ⊦ a ≠ b → (a ∈ b ' + x ↔ a ∈ x); in-append: ⊦ a ∈ x + y ↔ a ∈ x ∨ a ∈ y; in-17: ⊦ a ∈ b ' ↔ a = b; inapp-02: ⊦ ¬ a ∈ y → (y + c ' + z = a ' + z0 ↔ y = [] ∧ c = a ∧ z = z0); 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 ≠ a, a2 ≠ a0, a2 ≠ a1, a ∈ y2, ¬ a2 ∈ y3, ¬ a1 ∈ y0, ∀ a3, y1, y4, a4, a5, y5. y3 + a3 ' + y1 ≠ y4 + a4 ' + a5 ' + y5 ∨ a5 = a3 ∨ a4 = a5 ∨ a4 = a3 ∨ a5 ∈ y1 ∨ a4 ∈ y3 ⊦

Rule argument

Additional information

Used simplifier rules: Nil: ⊦ [] + x = x; c-06: ⊦ a ' + x = b ' + y ↔ a = b ∧ x = y; a: ⊦ (x + y) + z = x + y + z; list 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 ≠ a1, a2 ≠ a0, a2 ≠ a, ¬ a1 ∈ y0, ¬ a2 ∈ y3, ∀ a3, y1, y4, a4, a5, y5. y3 + a3 ' + y1 ≠ y4 + a4 ' + a5 ' + y5 ∨ a5 = a3 ∨ a4 = a5 ∨ a4 = a3 ∨ a5 ∈ y1 ∨ a4 ∈ y3 ⊦

Rule argument

Additional information

Used simplifier rules: c-06: ⊦ a ' + x = b ' + y ↔ a = b ∧ x = y; c: ⊦ a + x = a ' + x; in-rec: ⊦ a ∈ b ' + x ↔ a = b ∨ a ∈ x; 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