\problemdata                                                             
        {Full Binary Trees} % latex-friendly label for the prob.
        {Structural Induction} % The topic(s) of the problem content.  
        {?} % Source (if known)                                          
        {S01 Tutorial 1, 2} % Usage (list ones you are aware of). 
        {Tina Wang, S02} % Last revision info (author, date).   
                                                                         
                                                                         
\begin{problem}           
\mbox{}

\begin{problemparts}

\problempart

Give the structural inductive definition of the set $F$ of full
binary trees.

\solution{
  \begin{tabbing}
    XXX\=XXX\=XXX\=XXX\kill
    $\forall t \in F (P(t))$ \\
    1. (Base) $P(n)$, where $n$ is the single-node tree. \\
    2. (Inductive step) 
    $\forall t,t' \in F, (P(t) \wedge P(t') \implies P(\emph{makeboth}(t,t')))$ \\
    3. QED
  \end{tabbing}
 } 

\problempart

Define the function $\emph{numleaves}(t)$, for $t \in F$, giving the
number of ``leaves'' of the full binary tree $t$; that is,
$\emph{numleaves}(t)$, for $t \in F$, gives the number of nodes in $t$
that do not have children.  Your definition should be recursive, based
on the recursive definition of the set $F$.


\solution{
We define the function $\emph{numleaves}(t)$, for $t \in F$, as
   follows:

   $\emph{numleaves}(\text{single node}) = 1$

   $\emph{numleaves}(\emph{makeboth}(t,t')) 
   = \emph{numleaves}(t) + \emph{numleaves}(t')$ }

\problempart

Define the function $\emph{numinternal}(t)$, for $t \in F$, giving the
number of ``internal'' nodes of the full binary tree $t$; that is,
$\emph{numinternal}(t)$, for $t \in F$, gives the number of nodes in $t$
that have children.  Your definition should be recursive, based on the
recursive definition of the set $F$.


\solution{

   We define the function $\emph{numinternal}(t)$, for $t \in F$, as
   follows:

   $\emph{numinternal}(\text{single node}) = 0$

   $\emph{numinternal}(\emph{makeboth}(t,t')) = 
   \emph{numinternal}(t) + \emph{numinternal}(t') + 1$
}

\problempart

Prove by structural induction that for any full binary tree $t$ in
$F$, $\emph{numleaves}(t) = 1 + \emph{numinternal}(t)$.

\solution{

This part is shown by structural induction on the recursion step.

   Let $P(t): \emph{numleaves}(t) = 1 + \emph{numinternal}(t)$.

   Use the structural inductive definition of part (a) to show the
   property is true. 
}

\end{problemparts}
\end{problem}

                                 