\problemdata
{induction}
{velleman}
{S00 ps2}


\begin{problem}
% strong induction
% source: Velleman section 6.4, problem 9

Let the sequence $G_0, G_1, G_2,\ldots$ be defined recursively as
follows: $G_0 = 0$, $G_1 = 1$, and $G_n = 5 G_{n-1} - 6 G_{n-2}$, for
every $n \in \mathbb{N}, n \geq 2$.

Prove that for all $n \in \mathbb{N}$, $G_n = 3^n - 2^n$.

\solution{
  Let $P(n)$ be the predicate that $G_n = 3^n - 2^n$.  We prove
  $P(n)$, for all $n \in \mathbb{N}$, by strong induction on $n$.

  \begin{description}\itemsep 0\baselineskip
  \item[Base Case:] \mbox{} \\ In order to simplify the strong
    induction, we use two base cases, in particular $n = 0$ and $n =
    1$.  By the definition of the sequence it is the case that $G_0 =
    0$.  For $n = 0$, it is the case that $3^n - 2^n = 3^0 - 2^0 = 1 -
    1 = 0$; that is, it follows that $P(0)$ holds.  Similarly, by the
    definition of the sequence it is the case that $G_1 = 1$.  For $n
    = 1$, it is the case that $3^n - 2^n = 3^1 - 2^1 = 3 - 2 = 1$;
    that is, it follows that $P(1)$ holds.

  \item[Inductive Step:] \mbox{} \\ %
    We must show that for all $n \in \nats, n \geq 2$, it is the case
    that $(\forall\; k \in [ 0, n ], P(k)) \implies P(n+1)$.
    
    \begin{enumerate}\itemsep 0\baselineskip
    \item Fix $n \in \nats, n \geq 2$.
      
    \item Assume that the elements of the sequence $G_x$, for $0 \leq
      x \leq n$, can be expressed as $G_x = 3^x - 2^x$.
      
    \item The element of the sequence $G_{n+1}$ can be expressed as
      $G_{n+1} = 3^{n+1} - 2^{n+1}$.
      
      \begin{enumerate}\itemsep 0\baselineskip
      \item By the definition of the sequence we have $G_{n+1} = 5 G_n
        - 6 G_{n-1}$.  
        
      \item By our induction hypothesis, it is the case that $G_n =
        3^n - 2^n$ and $G_{n-1} = 3^{n-1} - 2^{n-1}$
        
      \item Thus, $G_{n+1} = 5 (3^n - 2^n) - 6 (3^{n-1} - 2^{n-1})$.
        Working through the algebra, we conclude that $G_{n+1} =
        3^{n+1} - 2^{n+1}$, as needed for the inductive step.
        
      \item QED 
        
      \end{enumerate}
      
    \item QED (implication and UG)
      
    \end{enumerate}
    
  \item QED (induction)
    
  \end{description}

}
\end{problem}

