Proof step 1 from proof firstN-in (conclusion) (back to tree)

System applied rule normalize

And obtained the following new goals

• Proof step 2:

  a ∈ firstn(n, x), n ≤ # x, ¬ a ∈ x ⊦

Rule argument

Additional information

Proof step 2 from proof firstN-in (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 3:

  a ∈ firstn(n, x), n ≤ # x, ¬ a ∈ x ⊦

Rule argument

Additional information

Proof step 3 from proof firstN-in (previous step) (back to tree)

User applied rule structural induction

And obtained the following new goals

• Proof step 4:

  a ∈ firstn(n, a0 + x0), n ≤ #(a0 + x0), ¬ a ∈ a0 + x0, ∀ a, n. ¬(a ∈ firstn(n, x0) ∧ n ≤ # x0 ∧ ¬ a ∈ x0) ⊦

Rule argument

Additional information

Used simplifier rules: firstN-zero: ⊦ firstn(0, x) = []; list freely generated by [], +;; ⊦ # [] = 0; (s) ⊦ m ≤ 0 ↔ m = 0; (s) ⊦ ¬ a ∈ []; (s)

Proof step 4 from proof firstN-in (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 5:

  a ≠ a0, a ∈ firstn(n, a0 ' + x0), n ≤ 1 + # x0, ¬ a ∈ x0, ∀ a1, n0. ¬ a1 ∈ firstn(n0, x0) ∨ ¬ n0 ≤ # x0 ∨ a1 ∈ x0 ⊦

Rule argument

Additional information

Used simplifier rules: a: ⊦ (x + y) + z = x + y + z; from specification list ⊦ a ∈ b ' + x ↔ ¬(a ≠ b ∧ ¬ a ∈ x); (ss) ⊦ a + x = a ' + x; (s) ⊦ # a ' = 0 +1; (s) ⊦ #(x + y) = # x + # y; (s)

Proof step 5 from proof firstN-in (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 6:

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

• Proof step 7:

  a ≠ a0, n ≠ 0, a ∈ a0 ' + firstn(n -1, x0), n ≤ 1 + # x0, ¬ a ∈ x0, ∀ a1, n0. ¬ a1 ∈ firstn(n0, x0) ∨ ¬ n0 ≤ # x0 ∨ a1 ∈ x0 ⊦

Rule argument

Additional information

Used simplifier rules: firstN-zero: ⊦ firstn(0, x) = []; ⊦ 0 ≤ m; (s) ⊦ ¬ a ∈ []; (s) Used terms: x0, a0, n

Proof step 6 from proof firstN-in (previous step) (back to tree)

Lemma firstN-rec-01

Proof step 7 from proof firstN-in (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 8:

  a ≠ a0, n ≠ 0, a ∈ firstn(n - 1, x0), n ≤ 1 + # x0, ¬ a ∈ x0, ∀ a1, n0. ¬ a1 ∈ firstn(n0, x0) ∨ ¬ n0 ≤ # x0 ∨ a1 ∈ x0 ⊦

Rule argument

Additional information

Used simplifier rules: a: ⊦ (x + y) + z = x + y + z; from specification list ⊦ a ≠ b → (a ∈ b ' + x ↔ a ∈ x); (s) ⊦ n -1 = n - 1; (s)

Proof step 8 from proof firstN-in (previous step) (back to tree)

Heuristic elimination applied rule apply elim lemma

And obtained the following new goals

• Proof step 9:

  n = m + 1, a ≠ a0, n ≠ 0, a ∈ firstn(m, x0), n ≤ 1 + # x0, ¬ a ∈ x0, ∀ a1, n0. ¬ a1 ∈ firstn(n0, x0) ∨ ¬ n0 ≤ # x0 ∨ a1 ∈ x0 ⊦

Rule argument

Additional information

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

Proof step 9 from proof firstN-in (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 10:

  a ≠ a0, a ∈ firstn(m, x0), m ≤ # x0, ¬ a ∈ x0, ∀ a1, n0. ¬ a1 ∈ firstn(n0, x0) ∨ ¬ n0 ≤ # x0 ∨ a1 ∈ x0 ⊦

Rule argument

Additional information

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

Proof step 10 from proof firstN-in (previous step) (back to tree)

Heuristic elimination applied rule apply elim lemma

And obtained the following new goals

• Proof step 11:

  ⊦ n ≤ # x → (y = firstn(n, x) ∧ z = restn(n, x) ↔ x = y + z ∧ # y = n)

Rule argument

Additional information

Used simplifier rules: ⊦ #(x + y) = # x + # y; (s) ⊦ m ≤ m + n; (s) a: ⊦ (m + n0) + n1 = m + n0 + n1; from specification nat-basic c: ⊦ m + n = n + m; from specification nat-basic ⊦ a ∈ x → a ∈ x + y; (s) a: ⊦ (x + y) + z = x + y + z; from specification list Used terms: x0, m, y, z

Proof step 11 from proof firstN-in (previous step) (back to tree)

Lemma elim-firstn-restn