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

System applied rule normalize

And obtained the following new goals

• Proof step 2:

  lastn(n, lastn(n, x)) ≠ lastn(n, x) ⊦

Rule argument

Additional information

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

User applied rule structural induction

And obtained the following new goals

• Proof step 3:

  lastn(n0 +1, lastn(n0 +1, x)) ≠ lastn(n0 +1, x), ∀ x. lastn(n0, lastn(n0, x)) = lastn(n0, x) ⊦

Rule argument

Additional information

Used simplifier rules: lastN-zero: ⊦ lastn(0, x) = []; nat freely generated by 0, +1;;

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

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 4:

  lastn(n0 + 1, lastn(n0 + 1, x)) ≠ lastn(n0 + 1, x), ∀ x. lastn(n0, lastn(n0, x)) = lastn(n0, x) ⊦

Rule argument

Additional information

Used simplifier rules: ⊦ m +1 = m + 1; (s)

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

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 5:

  ⊦ lastn(n + 1, x) = lastn(n, x.butlast) + x.last

• Proof step 6:

  lastn(n0 + 1, lastn(n0, x.butlast) + x.last) ≠ lastn(n0, x.butlast) + x.last, ∀ x. lastn(n0, lastn(n0, x)) = lastn(n0, x) ⊦

Rule argument

Additional information

Used terms: x, n0

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

Lemma lastN-rec

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

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 7:

  lastn(n0, lastn(n0, x.butlast)) ≠ lastn(n0, x.butlast), ∀ x. lastn(n0, lastn(n0, x)) = lastn(n0, x) ⊦

Rule argument

Additional information

Used simplifier rules: lastN-rec-01: ⊦ lastn(n + 1, x + a ') = lastn(n, x) + a '; a: ⊦ (x + y) + z = x + y + z; from specification list ⊦ x + y = z + y ↔ x = z; (s) ⊦ x + a = x + a '; (s) c: ⊦ m + n = n + m; from specification nat-basic a: ⊦ (m + n0) + n1 = m + n0 + n1; from specification nat-basic

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

Heuristic quantifier closing applied rule all left

And closed the goal!

Rule argument

Additional information

Used terms: x.butlast