Reading material

Pages 59-62.

Additional material

The LISP function 
  (DEFUN product (n) (IF (zerop n) 0 (+ (product (1- n)) m)))
can be expressed in Standard ML as 
  fun product(n) = if n = 0 then 0 else product(n-1) + m
or 
  fun product(0) = 0
    | product(n) = product(n-1) + m

Question

Consider the following function in Standard ML. 

  fun t(0) = 1
    | t(n) = t(n - 1) + t(n - 1)
What does this function compute? How can we use the induction tool to prove the above function correct.