Prove the partial correctness (Pre /\ Termination -> Post)
 of:

  r = 2
  i = n
  while i > 0
    r = 3 * r - 2
    i = i - 1

  Precondition: n >= 0
  Loop invariant: r = 3^(n-i) + 1
  Postcondition: r = 3^n + 1

Proof of invariant
------------------
  Base: r_0 = ...
  IS: Suppose true for k >= 0, show true for k+1:
      r_k+1 = 3r_k - 2 by code
            = 3(3^(n-i_k) + 1) - 2 by IH
            = 3^(n - i_k + 1) - 2
            = 3^(n - (i_k - 1)) - 2
            = 3^(n - i_k+1) - 2

Assuming it terminates after k iterations
-----------------------------------------

  i_k <= 0, r = r_k = 3^(n-i_k) + 1

  If k >= 1 iterations, then at k - 1 iterations i_(k-1) > 0
   so i_k = i_(k-1) - 1 >= 0. So i_k = 0.

  If k = 0 iterations, then i_k = i_0 = n >= 0 by precondition.
   So i_k = 0.

  In either case, r = 3^(n-0) + 1 = 3^n + 1.