Proof step 1 from proof firstn-append-01 (conclusion) (back to tree)

System applied rule normalize

And obtained the following new goals

• Proof step 2:

  x = firstn(# x - 1 + # z, x) + a ' + z, ¬(x = firstn(# x - # z, x) + z ↔ true) ⊦

Rule argument

Additional information

Proof step 2 from proof firstn-append-01 (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 3:

  x = firstn(# x - 1 + # z, x) + a ' + z, x ≠ firstn(# x - # z, x) + z ⊦

Rule argument

Additional information

Proof step 3 from proof firstn-append-01 (previous step) (back to tree)

User applied rule structural induction

And obtained the following new goals

• Proof step 4:

  a0 + x0 = firstn(#(a0 + x0) - 1 + # z, a0 + x0) + a ' + z, a0 + x0 ≠ firstn(#(a0 + x0) - # z, a0 + x0) + z, ∀ z, a. ¬(x0 = firstn(# x0 - 1 + # z, x0) + a ' + z ∧ x0 ≠ firstn(# x0 - # z, x0) + z) ⊦

Rule argument

Additional information

Used simplifier rules: firstN-empty: ⊦ firstn(n, x) = [] ↔ n = 0; list('a) freely generated by [], +;; ⊦ # [] = 0; (s) ⊦ x + y = [] ↔ x = [] ∧ y = []; (s) ⊦ a ' ≠ []; (s) a: ⊦ (x + y) + z = x + y + z; from specification list

Proof step 4 from proof firstn-append-01 (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 5:

  a0 ' + x0 = firstn(# x0 - # z, a0 ' + x0) + a ' + z, a0 ' + x0 ≠ firstn(# x0 + 1 - # z, a0 ' + x0) + z, ∀ z0, a1. x0 ≠ firstn(# x0 - 1 + # z0, x0) + a1 ' + z0 ∨ x0 = firstn(# x0 - # z0, x0) + z0, a0 ∈ firstn(# x0 - # z, a0 ' + x0) ∨ a0 = a ∨ a0 ∈ z ⊦

Rule argument

Additional information

Used simplifier rules: a: ⊦ (x + y) + z = x + y + z; from specification list ⊦ a ∈ a0 ' + x ↔ a = a0 ∨ a ∈ x; (s) ⊦ a ∈ x + y ↔ a ∈ x ∨ a ∈ y; (s) in-14: ⊦ a ' + x = y → a ∈ y; (forward) from specification list ⊦ a + x = a ' + x; (s) ⊦ m +1 = m + 1; (s) ⊦ #(a ' + x) = (# x)+1; (s) c: ⊦ m + n = n + m; from specification nat-basic a: ⊦ (m + n0) + n1 = m + n0 + n1; from specification nat-basic ⊦ m + n - n + n1 = m - n1; (s)

Proof step 5 from proof firstn-append-01 (previous step) (back to tree)

Heuristic elimination applied rule apply elim lemma

And obtained the following new goals

• Proof step 6:

  # x0 = n0 + # z, a0 ' + x0 = firstn(n0, a0 ' + x0) + a ' + z, a0 ' + x0 ≠ firstn(# x0 + 1 - # z, a0 ' + x0) + z, # z ≤ # x0, ∀ z0, a1. x0 ≠ firstn(# x0 - 1 + # z0, x0) + a1 ' + z0 ∨ x0 = firstn(# x0 - # z0, x0) + z0, a0 ∈ firstn(n0, a0 ' + x0) ∨ a0 = a ∨ a0 ∈ z ⊦

Rule argument

Additional information

Used simplifier rules: ⊦ m ≤ n ↔ ¬ n < m; (ss) a: ⊦ (x + y) + z = x + y + z; from specification list ⊦ a ' + x = y + a0 ' + z → ¬ # x < # z; (s) n ≤ m ⊦ n0 = m - n ↔ m = n0 + n; (elim) Used terms: # x0, # z, n0

Proof step 6 from proof firstn-append-01 (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 7:

  # x0 = n0 + # z, a0 ' + x0 = firstn(n0, a0 ' + x0) + a ' + z, x0 ≠ firstn(# x0 - # z, x0) + z, # z ≤ # x0, ∀ z0, a1. x0 ≠ firstn(# x0 - 1 + # z0, x0) + a1 ' + z0 ∨ x0 = firstn(# x0 - # z0, x0) + z0, a0 ∈ firstn(n0, a0 ' + x0) ∨ a0 = a ∨ a0 ∈ z ⊦

Rule argument

Additional information

Used simplifier rules: firstN-rec: ⊦ firstn(n + 1, x) = x.head + firstn(n, x.tail); a: ⊦ (x + y) + z = x + y + z; from specification list ⊦ a ∈ a0 ' + x ↔ a = a0 ∨ a ∈ x; (s) ⊦ a ∈ x + y ↔ a ∈ x ∨ a ∈ y; (s) in-14: ⊦ a ' + x = y → a ∈ y; (forward) from specification list ⊦ # x = # z → (x + y = z + y0 ↔ x = z ∧ y = y0); (ws) c: ⊦ m + n = n + m; from specification nat-basic a: ⊦ (m + n0) + n1 = m + n0 + n1; from specification nat-basic ⊦ a + x = a ' + x; (s) ⊦ (a ' + x).tail = x; (s) ⊦ (a ' + x).head = a; (s) ⊦ n ≤ m → m + n0 - n = (m - n) + n0; (s)

Proof step 7 from proof firstn-append-01 (previous step) (back to tree)

Heuristic elimination applied rule apply elim lemma

And obtained the following new goals

• Proof step 8:

  # x0 = n0 + # z, # x0 = n1 + # z, a0 ' + x0 = firstn(n0, a0 ' + x0) + a ' + z, x0 ≠ firstn(n1, x0) + z, # z ≤ # x0, ∀ z0, a1. x0 ≠ firstn(# x0 - 1 + # z0, x0) + a1 ' + z0 ∨ x0 = firstn(# x0 - # z0, x0) + z0, a0 ∈ firstn(n0, a0 ' + x0) ∨ a0 = a ∨ a0 ∈ z ⊦

Rule argument

Additional information

Used simplifier rules: n ≤ m ⊦ n0 = m - n ↔ m = n0 + n; (elim) Used terms: # x0, # z, n1

Proof step 8 from proof firstn-append-01 (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 9:

  # x0 = n1 + # z, a0 ' + x0 = firstn(n1, a0 ' + x0) + a ' + z, x0 ≠ firstn(n1, x0) + z, # z ≤ # x0, ∀ z0, a1. x0 ≠ firstn(# x0 - 1 + # z0, x0) + a1 ' + z0 ∨ x0 = firstn(# x0 - # z0, x0) + z0, a0 ∈ firstn(n1, a0 ' + x0) ∨ a0 = a ∨ a0 ∈ z ⊦

Rule argument

Additional information

Used simplifier rules: a: ⊦ (x + y) + z = x + y + z; from specification list ⊦ a ∈ a0 ' + x ↔ a = a0 ∨ a ∈ x; (s) ⊦ a ∈ x + y ↔ a ∈ x ∨ a ∈ y; (s) in-14: ⊦ a ' + x = y → a ∈ y; (forward) from specification list c: ⊦ m + n = n + m; from specification nat-basic a: ⊦ (m + n0) + n1 = m + n0 + n1; from specification nat-basic eqs: ⊦ m = n + n0 ∧ m = n + n1 → n0 = n1; (forward) from specification nat-basic

Proof step 9 from proof firstn-append-01 (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 10:

  ⊦ n ≠ 0 → firstn(n, a ' + x) = a ' + firstn(n -1, x)

• Proof step 11:

  # x0 = n1 + # z, a0 ' + x0 = (a0 ' + firstn(n1 -1, x0)) + a ' + z, n1 ≠ 0, x0 ≠ firstn(n1, x0) + z, # z ≤ # x0, ∀ z0, a1. x0 ≠ firstn(# x0 - 1 + # z0, x0) + a1 ' + z0 ∨ x0 = firstn(# x0 - # z0, x0) + z0, a0 ∈ a0 ' + firstn(n1 -1, x0) ∨ a0 = a ∨ a0 ∈ z ⊦

Rule argument

Additional information

Used simplifier rules: firstN-zero: ⊦ firstn(0, x) = []; ⊦ a ' + x = a0 ' + y ↔ a = a0 ∧ x = y; (ws) ⊦ n + 0 = n; (s) a: ⊦ (m + n0) + n1 = m + n0 + n1; from specification nat-basic c: ⊦ m + n = n + m; from specification nat-basic ⊦ [] + x = x; (s) a: ⊦ (x + y) + z = x + y + z; from specification list Used terms: x0, a0, n1

Proof step 10 from proof firstn-append-01 (previous step) (back to tree)

Lemma firstN-rec-01

Proof step 11 from proof firstn-append-01 (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 12:

  # x0 = n1 + # z, x0 = firstn(n1 - 1, x0) + a ' + z, n1 ≠ 0, x0 ≠ firstn(n1, x0) + z, # z ≤ # x0, ∀ z0, a1. x0 ≠ firstn(# x0 - 1 + # z0, x0) + a1 ' + z0 ∨ x0 = firstn(# x0 - # z0, x0) + z0 ⊦

Rule argument

Additional information

Used simplifier rules: a: ⊦ (x + y) + z = x + y + z; from specification list ⊦ a ∈ a0 ' + x ↔ a = a0 ∨ a ∈ x; (s) ⊦ n -1 = n - 1; (s) ⊦ # x = # z → (x + y = z + y0 ↔ x = z ∧ y = y0); (ws)

Proof step 12 from proof firstn-append-01 (previous step) (back to tree)

User applied rule all left

And obtained the following new goals

• Proof step 13:

  # x0 = n1 + # z, x0 = firstn(n1 - 1, x0) + a ' + z, n1 ≠ 0, x0 ≠ firstn(n1, x0) + z, # z ≤ # x0, ∀ z0, a1. x0 ≠ firstn(# x0 - 1 + # z0, x0) + a1 ' + z0 ∨ x0 = firstn(# x0 - # z0, x0) + z0, x0 ≠ firstn(# x0 - 1 + # z, x0) + a ' + z ∨ x0 = firstn(# x0 - # z, x0) + z ⊦

Rule argument

Additional information

Used terms: z, a

Proof step 13 from proof firstn-append-01 (previous step) (back to tree)

User applied rule case distinction

And obtained the following new goals

• Proof step 14:

  # x0 = n1 + # z, x0 = firstn(n1 - 1, x0) + a ' + z, n1 ≠ 0, x0 ≠ firstn(# x0 - 1 + # z, x0) + a ' + z, x0 ≠ firstn(n1, x0) + z, # z ≤ # x0, ∀ z0, a1. x0 ≠ firstn(# x0 - 1 + # z0, x0) + a1 ' + z0 ∨ x0 = firstn(# x0 - # z0, x0) + z0 ⊦

• Proof step 19:

  # x0 = n1 + # z, x0 = firstn(n1 - 1, x0) + a ' + z, x0 = firstn(# x0 - # z, x0) + z, n1 ≠ 0, x0 ≠ firstn(n1, x0) + z, # z ≤ # x0, ∀ z0, a1. x0 ≠ firstn(# x0 - 1 + # z0, x0) + a1 ' + z0 ∨ x0 = firstn(# x0 - # z0, x0) + z0 ⊦

Rule argument

Additional information

Proof step 14 from proof firstn-append-01 (previous step) (back to tree)

Heuristic elimination applied rule apply elim lemma

And obtained the following new goals

• Proof step 15:

  # x0 = n1 + # z, n1 = m + 1, x0 = firstn(m, x0) + a ' + z, n1 ≠ 0, x0 ≠ firstn(# x0 - 1 + # z, x0) + a ' + z, x0 ≠ firstn(n1, x0) + z, # z ≤ # x0, ∀ z0, a1. x0 ≠ firstn(# x0 - 1 + # z0, x0) + a1 ' + z0 ∨ x0 = firstn(# x0 - # z0, x0) + z0 ⊦

Rule argument

Additional information

Used simplifier rules: n ≠ 0 ⊦ m = n - 1 ↔ n = m + 1; (elim) Used terms: n1, m

Proof step 15 from proof firstn-append-01 (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 16:

  # x0 = (m + 1) + # z, x0 = firstn(m, x0) + a ' + z, x0 ≠ firstn(# x0 - 1 + # z, x0) + a ' + z, x0 ≠ (x0.head ' + firstn(m, x0.tail)) + z, # z ≤ # x0, ∀ z0, a1. x0 ≠ firstn(# x0 - 1 + # z0, x0) + a1 ' + z0 ∨ x0 = firstn(# x0 - # z0, x0) + z0 ⊦

Rule argument

Additional information

Used simplifier rules: firstN-rec: ⊦ firstn(n + 1, x) = x.head + firstn(n, x.tail); a: ⊦ (x + y) + z = x + y + z; from specification list c: ⊦ m + n = n + m; from specification nat-basic a: ⊦ (m + n0) + n1 = m + n0 + n1; from specification nat-basic ⊦ a + x = a ' + x; (s) ⊦ m + 1 ≠ 0; (s)

Proof step 16 from proof firstn-append-01 (previous step) (back to tree)

Heuristic elimination applied rule apply elim lemma

And obtained the following new goals

• Proof step 17:

  # x0 = (m + 1) + # z, x0 = firstn(m, x0) + a ' + z, x0 = a0 + y, x0 ≠ [], x0 ≠ firstn(# x0 - 1 + # z, x0) + a ' + z, x0 ≠ (a0 ' + firstn(m, y)) + z, # z ≤ # x0, ∀ z0, a1. x0 ≠ firstn(# x0 - 1 + # z0, x0) + a1 ' + z0 ∨ x0 = firstn(# x0 - # z0, x0) + z0 ⊦

Rule argument

Additional information

Used simplifier rules: firstN-empty: ⊦ firstn(n, x) = [] ↔ n = 0; ⊦ x + y = [] ↔ x = [] ∧ y = []; (s) ⊦ a ' ≠ []; (s) a: ⊦ (x + y) + z = x + y + z; from specification list x ≠ [] ⊦ a = x.head ∧ y = x.tail ↔ x = a + y; (elim) Used terms: x0, a0, y

Proof step 17 from proof firstn-append-01 (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 18:

  # y = m + # z, a0 ' + y = firstn(m, a0 ' + y) + a ' + z, a0 ' + y ≠ firstn(# y - # z, a0 ' + y) + a ' + z, y ≠ firstn(m, y) + z, # z ≤ # y + 1, ∀ z0, a1. a0 ' + y ≠ firstn(# y - # z0, a0 ' + y) + a1 ' + z0 ∨ a0 ' + y = firstn(# y + 1 - # z0, a0 ' + y) + z0, a0 ∈ firstn(m, a0 ' + y) ∨ a0 = a ∨ a0 ∈ z ⊦

Rule argument

Additional information

Used simplifier rules: a: ⊦ (x + y) + z = x + y + z; from specification list ⊦ a ∈ a0 ' + x ↔ a = a0 ∨ a ∈ x; (s) ⊦ a ∈ x + y ↔ a ∈ x ∨ a ∈ y; (s) in-14: ⊦ a ' + x = y → a ∈ y; (forward) from specification list ⊦ a + x = a ' + x; (s) ⊦ m +1 = m + 1; (s) ⊦ #(a ' + x) = (# x)+1; (s) c: ⊦ m + n = n + m; from specification nat-basic a: ⊦ (m + n0) + n1 = m + n0 + n1; from specification nat-basic ⊦ m + n - n + n1 = m - n1; (s) ⊦ # x = # z → (x + y = z + y0 ↔ x = z ∧ y = y0); (ws) ⊦ a ' ≠ []; (s) ⊦ x + y = [] ↔ x = [] ∧ y = []; (s) ⊦ m + n = m + n0 ↔ n = n0; (s)

Proof step 18 from proof firstn-append-01 (previous step) (back to tree)

Heuristic elimination applied rule apply elim lemma

And closed the goal!

Rule argument

Additional information

Used simplifier rules: eqs: ⊦ m = n + n0 ∧ m = n + n1 → n0 = n1; (forward) from specification nat-basic a: ⊦ (m + n0) + n1 = m + n0 + n1; from specification nat-basic c: ⊦ m + n = n + m; from specification nat-basic a: ⊦ (x + y) + z = x + y + z; from specification list ⊦ m ≤ n ↔ ¬ n < m; (ss) ⊦ a ' + x = y + a0 ' + z → ¬ # x < # z; (s) n ≤ m ⊦ n0 = m - n ↔ m = n0 + n; (elim) Used terms: # y, # z, n0

Proof step 19 from proof firstn-append-01 (previous step) (back to tree)

User applied rule subst equation

And closed the goal!

Rule argument

Additional information

Used simplifier rules: ⊦ m + n - m = n; (s) a: ⊦ (m + n0) + n1 = m + n0 + n1; from specification nat-basic c: ⊦ m + n = n + m; from specification nat-basic