Proof step 1 from proof two (conclusion) (back to tree)

System applied rule normalize

And obtained the following new goals

• Proof step 2:

  ¬(a ' + a1 ' = x + a0 ' + a2 ' + y ↔ x = [] ∧ y = [] ∧ a = a0 ∧ a1 = a2) ⊦

Rule argument

Additional information

Proof step 2 from proof two (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 3:

  a ' + a1 ' = x + a0 ' + a2 ' + y, a ∈ x ∨ a ∈ a0 ' ∨ a ∈ a2 ' ∨ a ∈ y, a1 ∈ x ∨ a1 ∈ a0 ' ∨ a1 ∈ a2 ' ∨ a1 ∈ y ⊦ x = [] ∧ y = [] ∧ a = a0 ∧ a1 = a2

Rule argument

Additional information

Used simplifier rules: Nil: ⊦ [] + x = x; app: ⊦ x + [] = x; app-07: ⊦ a ' + x = a0 ' + x ↔ a = a0; in-14: ⊦ a ' + x = y → a ∈ y; in-15: ⊦ x + a ' = y → a ∈ y; in-append: ⊦ a ∈ x + y ↔ a ∈ x ∨ a ∈ y; a: ⊦ (x + y) + z = x + y + z;

Proof step 3 from proof two (previous step) (back to tree)

Heuristic structural induction applied rule structural induction

And obtained the following new goals

• Proof step 4:

  a ' + a1 ' = x + a0 ' + a2 ' + (a3 + y0), ∀ a, a1, x, a0, a2. a ' + a1 ' = x + a0 ' + a2 ' + y0 ∧ (a ∈ x ∨ a ∈ a0 ' ∨ a ∈ a2 ' ∨ a ∈ y0) ∧ (a1 ∈ x ∨ a1 ∈ a0 ' ∨ a1 ∈ a2 ' ∨ a1 ∈ y0) → x = [] ∧ y0 = [] ∧ a = a0 ∧ a1 = a2, a1 ∈ x ∨ a1 ∈ a0 ' ∨ a1 ∈ a2 ' ∨ a1 ∈ a3 + y0, a ∈ x ∨ a ∈ a0 ' ∨ a ∈ a2 ' ∨ a ∈ a3 + y0 ⊦ x = [] ∧ a3 + y0 = [] ∧ a = a0 ∧ a1 = a2

Rule argument

Additional information

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

Proof step 4 from proof two (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 5:

  a ' + a1 ' = x + a0 ' + a2 ' + a3 ' + y0, a ∈ x, ∀ a, a1, x, a0, a2. a ' + a1 ' = x + a0 ' + a2 ' + y0 ∧ (a ∈ x ∨ a ∈ a0 ' ∨ a ∈ a2 ' ∨ a ∈ y0) ∧ (a1 ∈ x ∨ a1 ∈ a0 ' ∨ a1 ∈ a2 ' ∨ a1 ∈ y0) → x = [] ∧ y0 = [] ∧ a = a0 ∧ a1 = a2, a1 ∈ x ∨ a1 ∈ a0 ' ∨ a1 ∈ a2 ' ∨ a1 ∈ a3 ' ∨ a1 ∈ y0 ⊦

Rule argument

Additional information

Used simplifier rules: c: ⊦ a + x = a ' + x; e-01: ⊦ a ' + x ≠ []; in-14: ⊦ a ' + x = y → a ∈ y; in-15: ⊦ x + a ' = y → a ∈ y; inapp-02: ⊦ ¬ a ∈ y → (y + a0 ' + z = a ' + z0 ↔ y = [] ∧ a0 = a ∧ z = z0); eq-04: ⊦ x + a ' + y = a0 ' ↔ x = [] ∧ a = a0 ∧ y = []; e: ⊦ a ' ≠ []; in-append: ⊦ a ∈ x + y ↔ a ∈ x ∨ a ∈ y; a: ⊦ (x + y) + z = x + y + z;

Proof step 5 from proof two (previous step) (back to tree)

Heuristic cut applied rule cut formula

And obtained the following new goals

• Proof step 6:

  a ' + a1 ' = x + a0 ' + a2 ' + a3 ' + y0, a ∈ x, a1 ∈ x, ∀ a, a1, x, a0, a2. a ' + a1 ' = x + a0 ' + a2 ' + y0 ∧ (a ∈ x ∨ a ∈ a0 ' ∨ a ∈ a2 ' ∨ a ∈ y0) ∧ (a1 ∈ x ∨ a1 ∈ a0 ' ∨ a1 ∈ a2 ' ∨ a1 ∈ y0) → x = [] ∧ y0 = [] ∧ a = a0 ∧ a1 = a2, a1 ∈ x ∨ a1 ∈ a0 ' ∨ a1 ∈ a2 ' ∨ a1 ∈ a3 ' ∨ a1 ∈ y0 ⊦

• Proof step 8:

  a ' + a1 ' = x + a0 ' + a2 ' + a3 ' + y0, a ∈ x, ¬ a1 ∈ x, ∀ a, a1, x, a0, a2. a ' + a1 ' = x + a0 ' + a2 ' + y0 ∧ (a ∈ x ∨ a ∈ a0 ' ∨ a ∈ a2 ' ∨ a ∈ y0) ∧ (a1 ∈ x ∨ a1 ∈ a0 ' ∨ a1 ∈ a2 ' ∨ a1 ∈ y0) → x = [] ∧ y0 = [] ∧ a = a0 ∧ a1 = a2, a1 ∈ x ∨ a1 ∈ a0 ' ∨ a1 ∈ a2 ' ∨ a1 ∈ a3 ' ∨ a1 ∈ y0 ⊦

Rule argument

Additional information

Used formulas: a1 ∈ x

Proof step 6 from proof two (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 7:

  a ' + a1 ' = x + a0 ' + a2 ' + a3 ' + y0, a1 ∈ x, a ∈ x, ∀ a4, a5, x0, a6, a7. a4 ' + a5 ' = x0 + a6 ' + a7 ' + y0 ∧ (a4 ∈ x0 ∨ a4 = a6 ∨ a4 = a7 ∨ a4 ∈ y0) → x0 = [] ∧ y0 = [] ∧ a4 = a6 ∧ a5 = a7 ⊦

Rule argument

Additional information

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

Proof step 7 from proof two (previous step) (back to tree)

Heuristic quantifier closing applied rule all left

And closed the goal!

Rule argument

Additional information

Used simplifier rules: in-append: ⊦ a ∈ x + y ↔ a ∈ x ∨ a ∈ y; e-02: ⊦ x + a ' ≠ []; a: ⊦ (x + y) + z = x + y + z; Used terms: a, a1, x + a0 ', a2, a3

Proof step 8 from proof two (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 9:

  a ' + a1 ' = x + a0 ' + a2 ' + a3 ' + y0, a ∈ x, ¬ a1 ∈ x, ∀ a4, a5, x0, a6, a7. a4 ' + a5 ' = x0 + a6 ' + a7 ' + y0 ∧ (a4 ∈ x0 ∨ a4 = a6 ∨ a4 = a7 ∨ a4 ∈ y0) → x0 = [] ∧ y0 = [] ∧ a4 = a6 ∧ a5 = a7 ⊦

Rule argument

Additional information

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

Proof step 9 from proof two (previous step) (back to tree)

Heuristic quantifier closing applied rule all left

And closed the goal!

Rule argument

Additional information

Used simplifier rules: in-append: ⊦ a ∈ x + y ↔ a ∈ x ∨ a ∈ y; e-02: ⊦ x + a ' ≠ []; a: ⊦ (x + y) + z = x + y + z; Used terms: a, a1, x + a0 ', a2, a3