Proof step 1 from proof map-append-split (conclusion) (back to tree)

User applied rule structural induction

And obtained the following new goals

• Proof step 2:

  ∀ f, bx1, bx2. x0.map(f) = bx1 + bx2 ↔ (∃ y, z. x0 = y + z ∧ bx1 = y.map(f) ∧ bx2 = z.map(f)) ⊦ (a + x0).map(f) = bx1 + bx2 ↔ (∃ y, z. a + x0 = y + z ∧ bx1 = y.map(f) ∧ bx2 = z.map(f))

Rule argument

Additional information

Used simplifier rules: app-02: ⊦ x + y = [] ↔ x = [] ∧ y = []; map-base: ⊦ [].map(f) = []; Nil: ⊦ [] + x = x; a: ⊦ (x + y) + z = x + y + z; List[A] freely generated by [], +;

Proof step 2 from proof map-append-split (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 3:

  ∀ f, bx1, bx2. x0.map(f) = bx1 + bx2 ↔ (∃ y, z. x0 = y + z ∧ bx1 = y.map(f) ∧ bx2 = z.map(f)) ⊦ f(a) ' + x0.map(f) = bx1 + bx2 ↔ (∃ y, z. a ' + x0 = y + z ∧ bx1 = y.map(f) ∧ bx2 = z.map(f))

Rule argument

Additional information

Used simplifier rules: map-rec: ⊦ (a ' + x).map(f) = f(a) + x.map(f); a: ⊦ (x + y) + z = x + y + z; c: ⊦ a + x = a ' + x;

Proof step 3 from proof map-append-split (previous step) (back to tree)

User applied rule case distinction

And obtained the following new goals

• Proof step 4:

  f(a) ' + x0.map(f) = bx1 + bx2, ∀ f, bx1, bx2. x0.map(f) = bx1 + bx2 ↔ (∃ y, z. x0 = y + z ∧ bx1 = y.map(f) ∧ bx2 = z.map(f)) ⊦ ∃ y, z. a ' + x0 = y + z ∧ bx1 = y.map(f) ∧ bx2 = z.map(f)

• Proof step 10:

  f(a) ' + x0.map(f) ≠ bx1 + bx2, ∀ f, bx1, bx2. x0.map(f) = bx1 + bx2 ↔ (∃ y, z. x0 = y + z ∧ bx1 = y.map(f) ∧ bx2 = z.map(f)), ∃ y, z. a ' + x0 = y + z ∧ bx1 = y.map(f) ∧ bx2 = z.map(f) ⊦

Rule argument

Additional information

Proof step 4 from proof map-append-split (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 5:

  f(a) ' + x0.map(f) = bx1 + bx2, ∀ f, bx1, bx2. x0.map(f) = bx1 + bx2 ↔ (∃ y, z. x0 = y + z ∧ bx1 = y.map(f) ∧ bx2 = z.map(f)), f(a) ∈ bx1 ∨ f(a) ∈ bx2 ⊦ ∃ y, z. a ' + x0 = y + z ∧ bx1 = y.map(f) ∧ bx2 = z.map(f)

Rule argument

Additional information

Used simplifier rules: in-14: ⊦ a ' + x = y → a ∈ y; in-append: ⊦ a ∈ x + y ↔ a ∈ x ∨ a ∈ y; a: ⊦ (x + y) + z = x + y + z;

Proof step 5 from proof map-append-split (previous step) (back to tree)

User applied rule constructor cut

And obtained the following new goals

• Proof step 6:

  f(a) ' + x0.map(f) = bx1 + bx2, bx1 = b + bx, ∀ f, bx1, bx2. x0.map(f) = bx1 + bx2 ↔ (∃ y, z. x0 = y + z ∧ bx1 = y.map(f) ∧ bx2 = z.map(f)), f(a) ∈ bx1 ∨ f(a) ∈ bx2 ⊦ ∃ y, z. a ' + x0 = y + z ∧ bx1 = y.map(f) ∧ bx2 = z.map(f)

Rule argument

Additional information

Used simplifier rules: in-empty: ⊦ ¬ a ∈ []; map-empty: ⊦ x.map(f) = [] ↔ x = []; Nil: ⊦ [] + x = x; map-rec: ⊦ (a ' + x).map(f) = f(a) + x.map(f); c: ⊦ a + x = a ' + x; a: ⊦ (x + y) + z = x + y + z; List[A] freely generated by [], +;

Proof step 6 from proof map-append-split (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 7:

  x0.map(f) = bx + bx2, ∀ f, bx1, bx2. x0.map(f) = bx1 + bx2 ↔ (∃ y, z. x0 = y + z ∧ bx1 = y.map(f) ∧ bx2 = z.map(f)) ⊦ ∃ y, z. a ' + x0 = y + z ∧ f(a) ' + bx = y.map(f) ∧ bx2 = z.map(f)

Rule argument

Additional information

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

Proof step 7 from proof map-append-split (previous step) (back to tree)

User applied rule all left

And obtained the following new goals

• Proof step 8:

  x0.map(f) = bx + bx2, x0.map(f) = bx + bx2 ↔ (∃ y, z. x0 = y + z ∧ bx = y.map(f) ∧ bx2 = z.map(f)) ⊦ ∃ y, z. a ' + x0 = y + z ∧ f(a) ' + bx = y.map(f) ∧ bx2 = z.map(f)

Rule argument

Additional information

Used terms: f, bx, bx2

Proof step 8 from proof map-append-split (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 9:

  (y + z).map(f) = y.map(f) + z.map(f) ⊦ ∃ y0, z0. a ' + y + z = y0 + z0 ∧ f(a) ' + y.map(f) = y0.map(f) ∧ z.map(f) = z0.map(f)

Rule argument

Additional information

Proof step 9 from proof map-append-split (previous step) (back to tree)

Heuristic quantifier closing applied rule exists right

And closed the goal!

Rule argument

Additional information

Used simplifier rules: map-rec: ⊦ (a ' + x).map(f) = f(a) + x.map(f); c: ⊦ a + x = a ' + x; len-01: ⊦ # x = # z → (x + y = z + y0 ↔ x = z ∧ y = y0); a: ⊦ (x + y) + z = x + y + z; Used terms: a ' + y, z

Proof step 10 from proof map-append-split (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 11:

  a ' + x0 = y + z, f(a) ' + x0.map(f) ≠ y.map(f) + z.map(f), ∀ f, bx1, bx2. x0.map(f) = bx1 + bx2 ↔ (∃ y, z. x0 = y + z ∧ bx1 = y.map(f) ∧ bx2 = z.map(f)), a ∈ y ∨ a ∈ z ⊦

Rule argument

Additional information

Used simplifier rules: in-14: ⊦ a ' + x = y → a ∈ y; in-append: ⊦ a ∈ x + y ↔ a ∈ x ∨ a ∈ y; a: ⊦ (x + y) + z = x + y + z;

Proof step 11 from proof map-append-split (previous step) (back to tree)

User applied rule constructor cut

And obtained the following new goals

• Proof step 12:

  a ' + x0 = y + z, y = a0 + y0, f(a) ' + x0.map(f) ≠ y.map(f) + z.map(f), ∀ f, bx1, bx2. x0.map(f) = bx1 + bx2 ↔ (∃ y, z. x0 = y + z ∧ bx1 = y.map(f) ∧ bx2 = z.map(f)), a ∈ y ∨ a ∈ z ⊦

Rule argument

Additional information

Used simplifier rules: map-base: ⊦ [].map(f) = []; Nil: ⊦ [] + x = x; in-empty: ⊦ ¬ a ∈ []; in-14: ⊦ a ' + x = y → a ∈ y; map-rec: ⊦ (a ' + x).map(f) = f(a) + x.map(f); c: ⊦ a + x = a ' + x; len-01: ⊦ # x = # z → (x + y = z + y0 ↔ x = z ∧ y = y0); a: ⊦ (x + y) + z = x + y + z; List[A] freely generated by [], +;

Proof step 12 from proof map-append-split (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 13:

  (y0 + z).map(f) ≠ y0.map(f) + z.map(f), ∀ f, bx1, bx2. (y0 + z).map(f) = bx1 + bx2 ↔ (∃ y, z0. y0 + z = y + z0 ∧ bx1 = y.map(f) ∧ bx2 = z0.map(f)) ⊦

Rule argument

Additional information

Used simplifier rules: c-06: ⊦ a ' + x = a0 ' + y ↔ a = a0 ∧ x = y; map-rec: ⊦ (a ' + x).map(f) = f(a) + x.map(f); c: ⊦ a + x = a ' + x; in-rec: ⊦ a ∈ a0 ' + x ↔ a = a0 ∨ a ∈ x; len-01: ⊦ # x = # z → (x + y = z + y0 ↔ x = z ∧ y = y0); a: ⊦ (x + y) + z = x + y + z;

Proof step 13 from proof map-append-split (previous step) (back to tree)

User applied rule all left

And obtained the following new goals

• Proof step 14:

  (y0 + z).map(f) ≠ y0.map(f) + z.map(f), (y0 + z).map(f) = y0.map(f) + z.map(f) ↔ (∃ y, z0. y0 + z = y + z0 ∧ y0.map(f) = y.map(f) ∧ z.map(f) = z0.map(f)) ⊦

Rule argument

Additional information

Used terms: f, y0.map(f), z.map(f)

Proof step 14 from proof map-append-split (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 15:

  (y0 + z).map(f) ≠ y0.map(f) + z.map(f) ⊦ ∃ y, z0. y0 + z = y + z0 ∧ y0.map(f) = y.map(f) ∧ z.map(f) = z0.map(f)

Rule argument

Additional information

Proof step 15 from proof map-append-split (previous step) (back to tree)

Heuristic quantifier closing applied rule exists right

And closed the goal!

Rule argument

Additional information

Used terms: y0, z