Proof step 1 from proof lastN-ex (conclusion) (back to tree)

Heuristic elimination applied rule apply elim lemma

And obtained the following new goals

• Proof step 2:

  # x = n0 + n, n ≤ # x ⊦ ∃ y. x = y + lastn(n, x) ∧ # y = n0

Rule argument

Additional information

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

Proof step 2 from proof lastN-ex (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 3:

  # x = n0 + n ⊦ ∃ y. x = y + lastn(n, x) ∧ # y = n0

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 ≤ m + n; (s)

Proof step 3 from proof lastN-ex (previous step) (back to tree)

User applied rule apply lemma

And obtained the following new goals

• Proof step 4:

  ⊦ n < # x ↔ x = firstn(n, x) + restn(n, x) ∧ n < # x

• Proof step 5:

  # x = n0 + n, # x - n < # x ↔ x = firstn(# x - n, x) + restn(# x - n, x) ∧ # x - n < # x ⊦ ∃ y. x = y + lastn(n, x) ∧ # y = n0

Rule argument

Additional information

Used terms: # x - n, x

Proof step 4 from proof lastN-ex (previous step) (back to tree)

Lemma firstrestex

Proof step 5 from proof lastN-ex (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 6:

  # x = n0 + n, n ≠ 0 → x = firstn(n0, x) + restn(n0, x) ⊦ ∃ y. x = y + lastn(n, x) ∧ # y = n0

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 = n; (s) ⊦ m < m + n ↔ n ≠ 0; (s) n0 ≤ n ⊦ n - n0 < m ↔ n < m + n0; (s) ⊦ ¬ m + n < m; (s) ⊦ m ≤ n ↔ ¬ n < m; (ss)

Proof step 6 from proof lastN-ex (previous step) (back to tree)

User applied rule cut formula

And obtained the following new goals

• Proof step 7:

  # x = n0 + n, n ≠ 0, n ≠ 0 → x = firstn(n0, x) + restn(n0, x) ⊦ ∃ y. x = y + lastn(n, x) ∧ # y = n0

Rule argument

Additional information

Used simplifier rules: lastN-zero: ⊦ lastn(0, x) = []; ⊦ 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 formulas: n = 0

Proof step 7 from proof lastN-ex (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 8:

  # x = n0 + n, x = firstn(n0, x) + restn(n0, x), n ≠ 0 ⊦ ∃ y. x = y + lastn(n, x) ∧ # y = n0

Rule argument

Additional information

Proof step 8 from proof lastN-ex (previous step) (back to tree)

User applied rule exists right

And obtained the following new goals

• Proof step 9:

  # x = n0 + n, x = firstn(n0, x) + restn(n0, x), n ≠ 0 ⊦ ∃ y. x = y + lastn(n, x) ∧ # y = n0, x = firstn(n0, x) + lastn(n, x) ∧ # firstn(n0, x) = n0

Rule argument

Additional information

Used terms: firstn(n0, x)

Proof step 9 from proof lastN-ex (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 10:

  n ≤ # x ⊦ lastn(n, x) = restn(# x - n, x)

Rule argument

Additional information

Used simplifier rules: first-length: ⊦ # firstn(n, x) = n; first-length: ⊦ # firstn(n, x) = n; ⊦ 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 ⊦ m ≤ n ↔ ¬ n < m; (ss) f: ⊦ m < n → n ≠ 0; (forward) from specification nat-basic lf-02: ⊦ m < n ∧ m = n0 → n0 < n; (forward) from specification nat-basic ⊦ m < n → n ≠ 0; (s) ⊦ ¬ m + n < m; (s) Used terms: x, n

Proof step 10 from proof lastN-ex (previous step) (back to tree)

Lemma lastn-restn-01