A trivial Oz code for returning the number of elements of a list can be given by:

declare

fun {Length L}

case L

of nil then 0

[] H|T then 1+{Length T}

end

end

For example, the call {Browse {Length [1 f 2 3 s 5]}} will display 6. Explain why this function is not tail recursive. Write an equivalent tail recursive function. Write also an invariant for this tail recursive function. Using the invariant, prove the correctness for this program.