Proof step 1 from proof inapp-06 (conclusion) (back to tree)

System applied rule normalize

And obtained the following new goals

• Proof step 2:

  ¬(x + a ' + y = x0 + b ' + z ↔ x = x0 ∧ a = b ∧ y = z), ¬ a ∈ z, ¬ b ∈ y ⊦

Rule argument

Additional information

Proof step 2 from proof inapp-06 (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 3:

  x + a ' + y = x0 + b ' + z, ¬ a ∈ z, ¬ b ∈ y ⊦ x = x0 ∧ a = b ∧ y = z

Rule argument

Additional information

Used simplifier rules: a: ⊦ (x + y) + z = x + y + z;

Proof step 3 from proof inapp-06 (previous step) (back to tree)

User applied rule structural induction

And obtained the following new goals

• Proof step 4:

  (a0 + x1) + a ' + y = x0 + b ' + z, ¬ a ∈ z, ¬ b ∈ y, ∀ a, y, x0, b, z. x1 + a ' + y = x0 + b ' + z ∧ ¬ a ∈ z ∧ ¬ b ∈ y → x1 = x0 ∧ a = b ∧ y = z ⊦ a0 + x1 = x0 ∧ a = b ∧ y = z

Rule argument

Additional information

Used simplifier rules: in-14: ⊦ a ' + x = y → a ∈ y; isin: ⊦ a ' + x = y + b ' + z ∧ y ≠ [] → b ∈ x; neq-02: ⊦ ¬ a ∈ z ∧ a ≠ c → c ' + z ≠ y1 + a ' + x; 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 4 from proof inapp-06 (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 5:

  (a0 ' + x1) + a ' + y = x0 + b ' + z, a0 ∈ x0, ¬ b ∈ y, ¬ a ∈ z, ∀ a, y, x0, b, z. x1 + a ' + y = x0 + b ' + z ∧ ¬ a ∈ z ∧ ¬ b ∈ y → x1 = x0 ∧ a = b ∧ y = z ⊦ a0 ' + x1 = x0 ∧ a = b ∧ y = z

Rule argument

Additional information

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

Proof step 5 from proof inapp-06 (previous step) (back to tree)

User applied rule structural induction

And obtained the following new goals

• Proof step 6:

  (a0 ' + x1) + a ' + y = (a1 + x) + b ' + z, a0 ∈ a1 + x, ¬ b ∈ y, ¬ a ∈ z, ∀ a, y, x0, b, z. x1 + a ' + y = x0 + b ' + z ∧ ¬ a ∈ z ∧ ¬ b ∈ y → x1 = x0 ∧ a = b ∧ y = z, ∀ a0, x1, a, y, b, z. (a0 ' + x1) + a ' + y = x + b ' + z ∧ a0 ∈ x ∧ ¬ b ∈ y ∧ ¬ a ∈ z ∧ (∀ a, y, x0, b, z. x1 + a ' + y = x0 + b ' + z ∧ ¬ a ∈ z ∧ ¬ b ∈ y → x1 = x0 ∧ a = b ∧ y = z) → a0 ' + x1 = x ∧ a = b ∧ y = z ⊦ a0 ' + x1 = a1 + x ∧ a = b ∧ y = z

Rule argument

Additional information

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

Proof step 6 from proof inapp-06 (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 7:

  x1 + a ' + y = x + b ' + z, ¬ a ∈ z, ¬ b ∈ y, ∀ a, y, x0, b, z. x1 + a ' + y = x0 + b ' + z ∧ ¬ a ∈ z ∧ ¬ b ∈ y → x1 = x0 ∧ a = b ∧ y = z, ∀ a0, x1, a, y, b, z. (a0 ' + x1) + a ' + y = x + b ' + z ∧ a0 ∈ x ∧ ¬ b ∈ y ∧ ¬ a ∈ z ∧ (∀ a, y, x0, b, z. x1 + a ' + y = x0 + b ' + z ∧ ¬ a ∈ z ∧ ¬ b ∈ y → x1 = x0 ∧ a = b ∧ y = z) → a0 ' + x1 = x ∧ a = b ∧ y = z ⊦ x1 = x ∧ a = b ∧ y = z

Rule argument

Additional information

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

Proof step 7 from proof inapp-06 (previous step) (back to tree)

User applied rule all left

And closed the goal!

Rule argument

Additional information

Used terms: a, y, x, b, z