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

System applied rule normalize

And obtained the following new goals

• Proof step 2:

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

Rule argument

Additional information

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

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 3:

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

Rule argument

Additional information

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

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

User applied rule structural induction

And obtained the following new goals

• Proof step 4:

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

Rule argument

Additional information

Used simplifier rules: Nil: ⊦ [] + x = x; inapp-04: ⊦ ¬ a ∈ x → (a ' + x = y + a ' + z ↔ y = [] ∧ z = x); a: ⊦ (x + y) + z = x + y + z; in-empty: ⊦ ¬ a ∈ []; list('a) freely generated by [], +;;

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

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 5:

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

Rule argument

Additional information

Used simplifier rules: in-06: ⊦ a ∈ a0 ' + x ↔ ¬(a ≠ a0 ∧ ¬ a ∈ x); 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 + a0 ' + z = a ' + z0 ↔ y = [] ∧ a0 = a ∧ z = z0); a: ⊦ (x + y) + z = x + y + z;

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

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 6:

  y ≠ [] ⊦ a ' + x = y + z ↔ a = y.head ∧ x = y.tail + z

• Proof step 7:

  x0 + a ' + y = (z + a ').tail + y0, a0 = (z + a ').head, z + a ' ≠ [], a ≠ a0, a0 ∈ z, ¬ a ∈ x0, ¬ a ∈ y, ∀ a, y, z, y0. x0 + a ' + y = z + a ' + y0 ∧ ¬ a ∈ y ∧ ¬ a ∈ x0 → y = y0 ∧ x0 = z ⊦ y = y0 ∧ a0 ' + x0 = z

Rule argument

Additional information

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

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

Lemma firsteq

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

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 8:

  x0 + a ' + y = (z + a ').tail + y0, a ≠ z.head, (z + a ').head ∈ z, ¬ a ∈ x0, ¬ a ∈ y, ∀ a, y, z, y0. x0 + a ' + y = z + a ' + y0 ∧ ¬ a ∈ y ∧ ¬ a ∈ x0 → y = y0 ∧ x0 = z ⊦ y = y0 ∧ z.head ' + x0 = z

Rule argument

Additional information

Used simplifier rules: e-02: ⊦ x + a ' ≠ []; first-app: ⊦ a ∈ x → (x + y).head = x.head; a: ⊦ (x + y) + z = x + y + z;

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

Heuristic elimination applied rule apply elim lemma

And obtained the following new goals

• Proof step 9:

  x0 + a ' + y = (z + a ').tail + y0, z = a0 + y1, a ≠ a0, z ≠ [], (z + a ').head ∈ z, ¬ a ∈ x0, ¬ a ∈ y, ∀ a, y, z, y0. x0 + a ' + y = z + a ' + y0 ∧ ¬ a ∈ y ∧ ¬ a ∈ x0 → y = y0 ∧ x0 = z ⊦ y = y0 ∧ a0 ' + x0 = z

Rule argument

Additional information

Used simplifier rules: rest: ⊦ a '.tail = []; Nil: ⊦ [] + x = x; a: ⊦ (x + y) + z = x + y + z; first: ⊦ a '.head = a; in-empty: ⊦ ¬ a ∈ []; x ≠ [] ⊦ a = x.head ∧ y = x.tail ↔ x = a + y; (elim) Used terms: z, a0, y1

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

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 10:

  x0 + a ' + y = (y1 + a ') + y0, a ≠ a0, ¬ a ∈ x0, ¬ a ∈ y, ∀ a, y, z, y0. x0 + a ' + y = z + a ' + y0 ∧ ¬ a ∈ y ∧ ¬ a ∈ x0 → y = y0 ∧ x0 = z ⊦ y = y0 ∧ x0 = y1

Rule argument

Additional information

Used simplifier rules: c-07: ⊦ (a ' + x).tail = x; e-01: ⊦ a ' + x ≠ []; c-08: ⊦ (a ' + x).head = a; in-append: ⊦ a ∈ x + y ↔ a ∈ x ∨ a ∈ y; in-17: ⊦ a ∈ a0 ' ↔ a = a0; c: ⊦ a + x = a ' + x; app-01: ⊦ x + y = x + z ↔ y = z; a: ⊦ (x + y) + z = x + y + z;

Proof step 10 from proof inapp (previous step) (back to tree)

User applied rule all left

And closed the goal!

Rule argument

Additional information

Used simplifier rules: a: ⊦ (x + y) + z = x + y + z; Used terms: a, y, y1, y0