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

System applied rule normalize

And obtained the following new goals

• Proof step 2:

  ¬(a ' + b ' = x + a0 ' + c ' + y ↔ x = [] ∧ y = [] ∧ a = a0 ∧ b = c) ⊦

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 ' + b ' = x + a0 ' + c ' + y, a ∈ x ∨ a ∈ a0 ' ∨ a ∈ c ' ∨ a ∈ y, b ∈ x ∨ b ∈ a0 ' ∨ b ∈ c ' ∨ b ∈ y ⊦ x = [] ∧ y = [] ∧ a = a0 ∧ b = c

Rule argument

Additional information

Used simplifier rules: Nil: ⊦ [] + x = x; app: ⊦ x + [] = x; app-07: ⊦ a ' + x = b ' + x ↔ a = b; 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 ' + b ' = x + a0 ' + c ' + (a1 + y0), ∀ a, b, x, a0, c. a ' + b ' = x + a0 ' + c ' + y0 ∧ (a ∈ x ∨ a ∈ a0 ' ∨ a ∈ c ' ∨ a ∈ y0) ∧ (b ∈ x ∨ b ∈ a0 ' ∨ b ∈ c ' ∨ b ∈ y0) → x = [] ∧ y0 = [] ∧ a = a0 ∧ b = c, b ∈ x ∨ b ∈ a0 ' ∨ b ∈ c ' ∨ b ∈ a1 + y0, a ∈ x ∨ a ∈ a0 ' ∨ a ∈ c ' ∨ a ∈ a1 + y0 ⊦ x = [] ∧ a1 + y0 = [] ∧ a = a0 ∧ b = c

Rule argument

Additional information

Used simplifier rules: app: ⊦ x + [] = x; app-06: ⊦ x + a ' = y + b ' ↔ x = y ∧ a = b; c-05: ⊦ a ' = x + b ' ↔ a = b ∧ x = []; a: ⊦ (x + y) + z = x + y + z; list 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 ' + b ' = x + a0 ' + c ' + a1 ' + y0, a ∈ x, ∀ a, b, x, a0, c. a ' + b ' = x + a0 ' + c ' + y0 ∧ (a ∈ x ∨ a ∈ a0 ' ∨ a ∈ c ' ∨ a ∈ y0) ∧ (b ∈ x ∨ b ∈ a0 ' ∨ b ∈ c ' ∨ b ∈ y0) → x = [] ∧ y0 = [] ∧ a = a0 ∧ b = c, b ∈ x ∨ b ∈ a0 ' ∨ b ∈ c ' ∨ b ∈ a1 ' ∨ b ∈ 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 + c ' + z = a ' + z0 ↔ y = [] ∧ c = a ∧ z = z0); eq-04: ⊦ x + a ' + y = b ' ↔ x = [] ∧ a = b ∧ 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 ' + b ' = x + a0 ' + c ' + a1 ' + y0, a ∈ x, b ∈ x, ∀ a, b, x, a0, c. a ' + b ' = x + a0 ' + c ' + y0 ∧ (a ∈ x ∨ a ∈ a0 ' ∨ a ∈ c ' ∨ a ∈ y0) ∧ (b ∈ x ∨ b ∈ a0 ' ∨ b ∈ c ' ∨ b ∈ y0) → x = [] ∧ y0 = [] ∧ a = a0 ∧ b = c, b ∈ x ∨ b ∈ a0 ' ∨ b ∈ c ' ∨ b ∈ a1 ' ∨ b ∈ y0 ⊦

• Proof step 8:

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

Rule argument

Additional information

Used formulas: b ∈ 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 ' + b ' = x + a0 ' + c ' + a1 ' + y0, b ∈ x, a ∈ x, ∀ a2, b0, x0, a3, c0. a2 ' + b0 ' = x0 + a3 ' + c0 ' + y0 ∧ (a2 ∈ x0 ∨ a2 = a3 ∨ a2 = c0 ∨ a2 ∈ y0) → x0 = [] ∧ y0 = [] ∧ a2 = a3 ∧ b0 = c0 ⊦

Rule argument

Additional information

Used simplifier rules: in-17: ⊦ a ∈ b ' ↔ a = b; a: ⊦ (x + y) + z = x + y + z; in-16: ⊦ x + a ' = y + b ' + z ∧ a ≠ b → 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, b, x + a0 ', c, a1

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 ' + b ' = x + a0 ' + c ' + a1 ' + y0, a ∈ x, ¬ b ∈ x, ∀ a2, b0, x0, a3, c0. a2 ' + b0 ' = x0 + a3 ' + c0 ' + y0 ∧ (a2 ∈ x0 ∨ a2 = a3 ∨ a2 = c0 ∨ a2 ∈ y0) → x0 = [] ∧ y0 = [] ∧ a2 = a3 ∧ b0 = c0 ⊦

Rule argument

Additional information

Used simplifier rules: a: ⊦ (x + y) + z = x + y + z; in-17: ⊦ a ∈ b ' ↔ a = b; in-16: ⊦ x + a ' = y + b ' + z ∧ a ≠ b → 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, b, x + a0 ', c, a1