Proof step 1 from proof rest-mklist-04 (conclusion) (back to tree)

System applied rule normalize

And obtained the following new goals

• Proof step 2:

  restn(m, mklist(a, m)) ≠ [] ⊦

Rule argument

Additional information

Proof step 2 from proof rest-mklist-04 (previous step) (back to tree)

Heuristic structural induction applied rule structural induction

And obtained the following new goals

• Proof step 3:

  restn(m0 +1, mklist(a, m0 +1)) ≠ [], ∀ a. restn(m0, mklist(a, m0)) = [] ⊦

Rule argument

Additional information

Used simplifier rules: restN-zero: ⊦ restn(0, x) = x; nat freely generated by 0, +1;; ⊦ mklist(a, 0) = []; (s)

Proof step 3 from proof rest-mklist-04 (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 4:

  restn(m0, mklist(a, m0 + 1).tail) ≠ [], ∀ a. restn(m0, mklist(a, m0)) = [] ⊦

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 = m + 1; (s)

Proof step 4 from proof rest-mklist-04 (previous step) (back to tree)

Heuristic elimination applied rule apply elim lemma

And obtained the following new goals

• Proof step 5:

  mklist(a, m0 + 1) = a0 + y, mklist(a, m0 + 1) ≠ [], restn(m0, y) ≠ [], ∀ a. restn(m0, mklist(a, m0)) = [] ⊦

Rule argument

Additional information

Used simplifier rules: ⊦ mklist(a, m) = [] ↔ m = 0; (s) ⊦ m + n = 0 ↔ m = 0 ∧ n = 0; (ws) a: ⊦ (m + n0) + n1 = m + n0 + n1; from specification nat-basic c: ⊦ m + n = n + m; from specification nat-basic x ≠ [] ⊦ a = x.head ∧ y = x.tail ↔ x = a + y; (elim) Used terms: mklist(a, m0 + 1), a0, y

Proof step 5 from proof rest-mklist-04 (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 6:

  mklist(a, m0 + 1) = a0 ' + y, restn(m0, y) ≠ [], ∀ a. restn(m0, mklist(a, m0)) = [] ⊦

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) 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 ⊦ m + 1 ≠ 0; (s) ⊦ mklist(a, m) = [] ↔ m = 0; (s) ⊦ a + x = a ' + x; (s)

Proof step 6 from proof rest-mklist-04 (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 7:

  ⊦ m ≠ 0 → mklist(a, m) = a + mklist(a, m - 1)

• Proof step 8:

  a + mklist(a, m0 + 1 - 1) = a0 ' + y, m0 + 1 ≠ 0, restn(m0, y) ≠ [], ∀ a. restn(m0, mklist(a, m0)) = [] ⊦

Rule argument

Additional information

Used simplifier rules: ⊦ m + n = 0 ↔ m = 0 ∧ n = 0; (ws) a: ⊦ (m + n0) + n1 = m + n0 + n1; from specification nat-basic c: ⊦ m + n = n + m; from specification nat-basic Used terms: a, m0 + 1

Proof step 7 from proof rest-mklist-04 (previous step) (back to tree)

A spec-lemma

Proof step 8 from proof rest-mklist-04 (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 9:

  restn(m0, mklist(a0, m0)) ≠ [], ∀ a. restn(m0, mklist(a, m0)) = [] ⊦

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 + 1 ≠ 0; (s) a: ⊦ (x + y) + z = x + y + z; from specification list ⊦ a ' + x = a0 ' + y ↔ a = a0 ∧ x = y; (ws) ⊦ a + x = a ' + x; (s) ⊦ n + 0 = n; (s) ⊦ n ≤ m → m + n0 - n = (m - n) + n0; (s)

Proof step 9 from proof rest-mklist-04 (previous step) (back to tree)

Heuristic quantifier closing applied rule all left

And closed the goal!

Rule argument

Additional information

Used terms: a0