Proof step 1 from proof sublist-append-04 (conclusion) (back to tree)

System applied rule normalize

And obtained the following new goals

• Proof step 2:

  sublist(n, n0, x) + sublist(n + n0, n1, x) ≠ sublist(n, n0 + n1, x), n + n0 + n1 ≤ # x ⊦

Rule argument

Additional information

Proof step 2 from proof sublist-append-04 (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 3:

  firstn(n0, restn(n, x)) + firstn(n1, restn(n + n0, x)) ≠ firstn(n0 + n1, restn(n, x)), n + n0 + n1 ≤ # x ⊦

Rule argument

Additional information

Used simplifier rules: sublist-def: ⊦ sublist(m, n, x) = firstn(n, restn(m, x));

Proof step 3 from proof sublist-append-04 (previous step) (back to tree)

User applied rule structural induction

And obtained the following new goals

• Proof step 4:

  firstn(n0, restn(n, a + x0)) + firstn(n1, restn(n + n0, a + x0)) ≠ firstn(n0 + n1, restn(n, a + x0)), n + n0 + n1 ≤ #(a + x0), ∀ n0, n, n1. ¬(firstn(n0, restn(n, x0)) + firstn(n1, restn(n + n0, x0)) ≠ firstn(n0 + n1, restn(n, x0)) ∧ n + n0 + n1 ≤ # x0) ⊦

Rule argument

Additional information

Used simplifier rules: restN-zero: ⊦ restn(0, x) = x; firstN-zero: ⊦ firstn(0, x) = []; list freely generated by [], +;; ⊦ # [] = 0; (s) ⊦ m ≤ 0 ↔ m = 0; (s) ⊦ m + n = 0 ↔ m = 0 ∧ n = 0; (ws) ⊦ [] + x = x; (s) a: ⊦ (x + y) + z = x + y + z; from specification list a: ⊦ (m + n0) + n1 = m + n0 + n1; from specification nat-basic c: ⊦ m + n = n + m; from specification nat-basic

Proof step 4 from proof sublist-append-04 (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 5:

  firstn(n0, restn(n, a ' + x0)) + firstn(n1, restn(n + n0, a ' + x0)) ≠ firstn(n0 + n1, restn(n, a ' + x0)), n + n0 + n1 ≤ 1 + # x0, ∀ n2, n3, n4. firstn(n2, restn(n3, x0)) + firstn(n4, restn(n3 + n2, x0)) = firstn(n2 + n4, restn(n3, x0)) ∨ ¬ n3 + n2 + n4 ≤ # x0 ⊦

Rule argument

Additional information

Used simplifier rules: a: ⊦ (x + y) + z = x + y + z; from specification list ⊦ # a ' = 0 +1; (s) ⊦ #(x + y) = # x + # y; (s) ⊦ a + x = a ' + x; (s)

Proof step 5 from proof sublist-append-04 (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 6:

  ⊦ 0 < n → restn(n, x) = restn(n -1, x.tail)

• Proof step 7:

  firstn(n0, restn(n, a ' + x0)) + firstn(n1, restn(n + n0, a ' + x0)) ≠ firstn(n0 + n1, restn(n, a ' + x0)), n + n0 + n1 ≤ 1 + # x0, ¬ 0 < n, ∀ n2, n3, n4. firstn(n2, restn(n3, x0)) + firstn(n4, restn(n3 + n2, x0)) = firstn(n2 + n4, restn(n3, x0)) ∨ ¬ n3 + n2 + n4 ≤ # x0 ⊦

• Proof step 19:

  firstn(n0, restn(n -1, (a ' + x0).tail)) + firstn(n1, restn(n + n0, a ' + x0)) ≠ firstn(n0 + n1, restn(n -1, (a ' + x0).tail)), 0 < n, n + n0 + n1 ≤ 1 + # x0, ∀ n2, n3, n4. firstn(n2, restn(n3, x0)) + firstn(n4, restn(n3 + n2, x0)) = firstn(n2 + n4, restn(n3, x0)) ∨ ¬ n3 + n2 + n4 ≤ # x0 ⊦

Rule argument

Additional information

Used terms: a ' + x0, n

Proof step 6 from proof sublist-append-04 (previous step) (back to tree)

Lemma rest-rec

Proof step 7 from proof sublist-append-04 (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 8:

  firstn(n0, a ' + x0) + firstn(n1, restn(n0, a ' + x0)) ≠ firstn(n0 + n1, a ' + x0), n0 + n1 ≤ 1 + # x0, ∀ n2, n3, n4. firstn(n2, restn(n3, x0)) + firstn(n4, restn(n3 + n2, x0)) = firstn(n2 + n4, restn(n3, x0)) ∨ ¬ n3 + n2 + n4 ≤ # x0 ⊦

Rule argument

Additional information

Used simplifier rules: restN-zero: ⊦ restn(0, x) = x; a: ⊦ (m + n0) + n1 = m + n0 + n1; from specification nat-basic c: ⊦ m + n = n + m; from specification nat-basic ⊦ 0 + m = m; (s) ⊦ 0 < m ↔ m ≠ 0; (s)

Proof step 8 from proof sublist-append-04 (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 9:

  n ≠ 0 ⊦ firstn((* n), x) = x.head ' + firstn(n -1, x.tail)

• Proof step 10:

  n0 + n1 ≠ 0, firstn(n0, a ' + x0) + firstn(n1, restn(n0, a ' + x0)) ≠ (a ' + x0).head ' + firstn((n0 + n1)-1, (a ' + x0).tail), n0 + n1 ≤ 1 + # x0, ∀ n2, n3, n4. firstn(n2, restn(n3, x0)) + firstn(n4, restn(n3 + n2, x0)) = firstn(n2 + n4, restn(n3, x0)) ∨ ¬ n3 + n2 + n4 ≤ # x0 ⊦

Rule argument

Additional information

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

Proof step 9 from proof sublist-append-04 (previous step) (back to tree)

Lemma first-num

Proof step 10 from proof sublist-append-04 (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 11:

  n0 + n1 ≠ 0, firstn(n0, a ' + x0) + firstn(n1, restn(n0, a ' + x0)) ≠ a ' + firstn(n0 + n1 - 1, x0), n0 + n1 ≤ 1 + # x0, ∀ n2, n3, n4. firstn(n2, restn(n3, x0)) + firstn(n4, restn(n3 + n2, x0)) = firstn(n2 + n4, restn(n3, x0)) ∨ ¬ n3 + n2 + n4 ≤ # x0 ⊦

Rule argument

Additional information

Used simplifier rules: a: ⊦ (x + y) + z = x + y + z; from specification list ⊦ (a ' + x).tail = x; (s) ⊦ n -1 = n - 1; (s) ⊦ (a ' + x).head = a; (s)

Proof step 11 from proof sublist-append-04 (previous step) (back to tree)

Heuristic elimination applied rule apply elim lemma

And obtained the following new goals

• Proof step 12:

  n0 + n1 = m + 1, n0 + n1 ≠ 0, firstn(n0, a ' + x0) + firstn(n1, restn(n0, a ' + x0)) ≠ a ' + firstn(m, x0), n0 + n1 ≤ 1 + # x0, ∀ n2, n3, n4. firstn(n2, restn(n3, x0)) + firstn(n4, restn(n3 + n2, x0)) = firstn(n2 + n4, restn(n3, x0)) ∨ ¬ n3 + n2 + n4 ≤ # x0 ⊦

Rule argument

Additional information

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

Proof step 12 from proof sublist-append-04 (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 13:

  n0 + n1 = m + 1, firstn(n0, a ' + x0) + firstn(n1, restn(n0, a ' + x0)) ≠ a ' + firstn(m, x0), m ≤ # x0, ∀ n2, n3, n4. firstn(n2, restn(n3, x0)) + firstn(n4, restn(n3 + n2, x0)) = firstn(n2 + n4, restn(n3, x0)) ∨ ¬ n3 + n2 + n4 ≤ # 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 13 from proof sublist-append-04 (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 14:

  n ≠ 0 ⊦ firstn((* n), x) = x.head ' + firstn(n -1, x.tail)

• Proof step 15:

  n0 + n1 = m + 1, ((a ' + x0).head ' + firstn(n0 -1, (a ' + x0).tail)) + firstn(n1, restn(n0, a ' + x0)) ≠ a ' + firstn(m, x0), n0 ≠ 0, m ≤ # x0, ∀ n2, n3, n4. firstn(n2, restn(n3, x0)) + firstn(n4, restn(n3 + n2, x0)) = firstn(n2 + n4, restn(n3, x0)) ∨ ¬ n3 + n2 + n4 ≤ # x0 ⊦

Rule argument

Additional information

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

Proof step 14 from proof sublist-append-04 (previous step) (back to tree)

Lemma first-num

Proof step 15 from proof sublist-append-04 (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 16:

  n0 + n1 = m + 1, firstn(n0 - 1, x0) + firstn(n1, restn(n0, a ' + x0)) ≠ firstn(m, x0), n0 ≠ 0, m ≤ # x0, ∀ n2, n3, n4. firstn(n2, restn(n3, x0)) + firstn(n4, restn(n3 + n2, x0)) = firstn(n2 + n4, restn(n3, x0)) ∨ ¬ n3 + n2 + n4 ≤ # x0 ⊦

Rule argument

Additional information

Used simplifier rules: a: ⊦ (x + y) + z = x + y + z; from specification list ⊦ x + y = x + z ↔ y = z; (s) ⊦ (a ' + x).tail = x; (s) ⊦ n -1 = n - 1; (s) ⊦ (a ' + x).head = a; (s)

Proof step 16 from proof sublist-append-04 (previous step) (back to tree)

Heuristic elimination applied rule apply elim lemma

And obtained the following new goals

• Proof step 17:

  n0 + n1 = m + 1, n0 = m0 + 1, firstn(m0, x0) + firstn(n1, restn(n0, a ' + x0)) ≠ firstn(m, x0), n0 ≠ 0, m ≤ # x0, ∀ n2, n3, n4. firstn(n2, restn(n3, x0)) + firstn(n4, restn(n3 + n2, x0)) = firstn(n2 + n4, restn(n3, x0)) ∨ ¬ n3 + n2 + n4 ≤ # x0 ⊦

Rule argument

Additional information

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

Proof step 17 from proof sublist-append-04 (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 18:

  firstn(m0, x0) + firstn(n1, restn(m0, x0)) ≠ firstn(m0 + n1, x0), m0 + n1 ≤ # x0, ∀ n2, n3, n4. firstn(n2, restn(n3, x0)) + firstn(n4, restn(n3 + n2, x0)) = firstn(n2 + n4, restn(n3, x0)) ∨ ¬ n3 + n2 + n4 ≤ # x0 ⊦

Rule argument

Additional information

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

Proof step 18 from proof sublist-append-04 (previous step) (back to tree)

User applied rule all left

And closed the goal!

Rule argument

Additional information

Used simplifier rules: restN-zero: ⊦ restn(0, x) = x; ⊦ n + 0 = n; (s) c: ⊦ m + n = n + m; from specification nat-basic a: ⊦ (m + n0) + n1 = m + n0 + n1; from specification nat-basic Used terms: m0, 0, n1

Proof step 19 from proof sublist-append-04 (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 20:

  firstn(n0, restn(n - 1, x0)) + firstn(n1, restn(n + n0, a ' + x0)) ≠ firstn(n0 + n1, restn(n - 1, x0)), n ≠ 0, n + n0 + n1 ≤ 1 + # x0, ∀ n2, n3, n4. firstn(n2, restn(n3, x0)) + firstn(n4, restn(n3 + n2, x0)) = firstn(n2 + n4, restn(n3, x0)) ∨ ¬ n3 + n2 + n4 ≤ # x0 ⊦

Rule argument

Additional information

Used simplifier rules: ⊦ 0 < m ↔ m ≠ 0; (s) a: ⊦ (x + y) + z = x + y + z; from specification list ⊦ (a ' + x).tail = x; (s) ⊦ n -1 = n - 1; (s)

Proof step 20 from proof sublist-append-04 (previous step) (back to tree)

Heuristic elimination applied rule apply elim lemma

And obtained the following new goals

• Proof step 21:

  n = m + 1, firstn(n0, restn(m, x0)) + firstn(n1, restn(n + n0, a ' + x0)) ≠ firstn(n0 + n1, restn(m, x0)), n ≠ 0, n + n0 + n1 ≤ 1 + # x0, ∀ n2, n3, n4. firstn(n2, restn(n3, x0)) + firstn(n4, restn(n3 + n2, x0)) = firstn(n2 + n4, restn(n3, x0)) ∨ ¬ n3 + n2 + n4 ≤ # x0 ⊦

Rule argument

Additional information

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

Proof step 21 from proof sublist-append-04 (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 22:

  firstn(n0, restn(m, x0)) + firstn(n1, restn(m + n0, x0)) ≠ firstn(n0 + n1, restn(m, x0)), m + n0 + n1 ≤ # x0, ∀ n2, n3, n4. firstn(n2, restn(n3, x0)) + firstn(n4, restn(n3 + n2, x0)) = firstn(n2 + n4, restn(n3, x0)) ∨ ¬ n3 + n2 + n4 ≤ # x0 ⊦

Rule argument

Additional information

Used simplifier rules: restN-rec: ⊦ restn(n + 1, x) = restn(n, x.tail); 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) a: ⊦ (x + y) + z = x + y + z; from specification list ⊦ (a ' + x).tail = x; (s)

Proof step 22 from proof sublist-append-04 (previous step) (back to tree)

User applied rule all left

And closed the goal!

Rule argument

Additional information

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