We have last’ defined like:

last' [x] = x

last' (x:xs) = last' xs(*)

Base case: A list of one element is equal to that element itself.

Inductive step: Assume that last’ (x:xs) returns the last element of the list.

Then, if last’ (x:xs) holds, last’ (y:x:xs) must also hold.

We must show that it holds for y:x:xs.

Set zs = x:xs and obtain:

last’ (y:zs) = **(*)** = last’ zs = last’ (x:xs) = inductive assumption = last element of the list

So the recursion chops elements from beginning until it reaches one element, which will be the last element from our list.

Advertisements