
\section{Recursive structure definitions and structural induction}

So far we've been looking at recursively defined functions of the
natural numbers\.  Recursive definitions are also a useful way to
describe other types of objects (structures) that are built up from
smaller pieces\.  Structural induction is an elegant variant of
induction for proving things about these recursively defined objects\.
Instead of using a number $n$, the induction is based explicitly on
the recursive structure of the definition.

\subsection{Some recursive definitions for data types}

\begin{definition}
  The set $F$ of fully parenthesized Boolean algebra expressions satisfies: 
  \begin{enumerate}
  \item The symbols $0$ and $1$ are in $F$. 
  \item If $e$ and $e'$ are in $F$ then the expression $[e \wedge e']$ is
    in $F$. 
  \item
    If $e$ and $e'$ are in $F$ then the expression $[e \vee e']$ is
    in $F$. 
  \item
    If $e$ is in $F$ then the expression $[\neg e]$ is in $F$. 
  \item
    $F$ contains nothing else. 
  \end{enumerate}
\end{definition}


\begin{definition}
  The set $T$ of binary trees satisfies: 
  \begin{enumerate}
  \item
    A single node (just a dot) is in $T$.
  \item 
    If $t$ is in $T$, then the structure formed from $t$, a single
    new node, and an arrow labeled ``left'' from the new node to
    $t$, is also in $T$. 
  \item
    If $t$ is in $T$, then the structure formed from $t$, a single
    new node, and an arrow labeled ``right'' from the new node to
    $t$, is also in $T$. 
  \item
    If $t$ and $t'$ are in $T$, then the structure formed from $t$, $t'$,
    and a single new node, with an arrow labeled ``left'' from the new
    node to $t$ and another arrow labeled ``right'' from the new node to
    $t'$, is also in $T$. 
  \end{enumerate}
\end{definition}
Since the descriptions above are wordy, it's nice to introduce some
notation, like makeleft$(t)$ to denote the thing built up from $t$
according to the first recursive rule\.  Likewise, makeright$(t)$,
makeboth$(t,t')$.

\forlecture{ (diagram)\\ }

Here is a definition that we already used informally:
\begin{definition}
  The set $S$ of (finite length) strings over alphabet $A$ satisfies: 
  \begin{enumerate}
  \item  $\lambda$, the empty string, is in $S$. 
  \item  If $s$ is in the set $S$ and $a \in A$, then $sa$ is in $S$. 
  \item $S$ contains nothing else. 
  \end{enumerate}
\end{definition}
This is a recursive description (definition) of the set of strings\. 
Notice that it includes every (finite length) string\. 
Moreover, every string has a unique derivation using these rules (this
isn't strictly necessary, but is often convenient in proofs).  

Finally, here is a definition of lists for 6.001:
\begin{definition}
  The set $L$ of lists over atom set $A$ satisfies:
  \begin{enumerate}
  \item $()$, the empty list, is in $L$
  \item If $\ell \in L$ and $a \in A$, then $(a\ . \ \ell)$ is in $L$
  \item $L$ contains nothing else
  \end{enumerate}
\end{definition}
Note the close similarity to the definition of strings.

\subsection{Structural induction on recursive data type definitions}

Structural induction is used to prove a property $P$ of all the elements
of some recursively-defined data type\. 

\subsubsection{The Method}

The proof consists of two steps: 
\begin{itemize}
\item Prove for the ``base cases'' of the definition. 
\item Prove for the result of any combination rule, assuming that it
  is true for all the parts.  
\end{itemize}

Structural induction looks like a new inference rule, but it isn't: it
is standard (strong) induction on the \emph{number of formation steps}
it takes to build the object at hand out of the basic objects of the
recursive definition.


For Boolean expressions:
                                %[[[Victor: slide]]]
\begin{structproof}
  Prove: $\forall e \in F (P(e))$ \\
  1. (Base) $P(0)$ \\
  2. (Base) $P(1)$ \\
  3. (Inductive step) 
  $\forall e, e' \in F (P(e) \wedge P(e') \Rightarrow P([e \wedge e']))$\\
  4. (Inductive step) 
  $\forall e, e' \in F (P(e) \wedge P(e') \Rightarrow P([e \vee e']))$ \\
  5. (Inductive step) 
  $\forall e \in F (P(e) \Rightarrow P([\neg e]))$\\
  6. QED
  \> \> \> \> \> Structural induction on Boolean expressions
\end{structproof}
(Note that we are being careful to distinguish parentheses that are
art of the boolean expression (represented by brackets) from
parenthesis used in our proof formulas (represented by standard
parentheses).

For binary trees:
                                %[[[Victor: slide]]]
\begin{structproof}
  Prove: $\forall t \in T (P(t))$ \\
  1. (Base) $P(n)$, where $n$ is the single-node tree. \\
  2. (Inductive step) 
  $\forall t \in T (P(t) \Rightarrow P(\ms{makeleft}(t)))$ \\
  3. (Inductive step) 
  $\forall t \in T (P(t) \Rightarrow P(\ms{makeright}(t)))$ \\
  4. (Inductive step) 
  $\forall t,t' \in T (P(t) \wedge P(t') \Rightarrow P(\ms{makeboth}(t,t')))$ \\
  5. QED
  \> \> \> \> \> Structural induction on binary trees
\end{structproof}

For strings over alphabet $A = \{ 0,1 \}$:
                                %[[[Victor: slide]]]
\begin{structproof}
  Prove: $\forall s \in S (P(s))$ \\
  1. (Base) $P(\lambda)$ \\
  2. (Inductive step) $\forall s \in S (P(s) \Rightarrow P(s 0))$ \\
  3. (Inductive step) $\forall s \in S (P(s) \Rightarrow P(s 1))$ \\
  4. QED
  \> \> \> \> \> Structural induction on strings.
\end{structproof}
You can see how this would extend to different alphabets.

\subsubsection{Examples}

Here's example for each of the data types: 

\begin{theorem}
  Every Boolean expression has the same number of left and right parentheses. 
\end{theorem}
\begin{proof}
  Define $P(e)$: Expression $e$ has the same number of left and right
  parentheses.
                                %[[[Victor: slide]]]
  \begin{structproof}
    Prove: $\forall e \in F (P(e))$ \\
    1. (Base) $P(0)$ 
    \> \> \> \> \> The expression $0$ has no parens. \\
    2. (Base) $P(1)$ 
    \> \> \> \> \> No parens \\
    3. (Inductive step) 
    $\forall e, e' \in F (P(e) \wedge P(e') \Rightarrow P([e \wedge e'])$\\
    \> 1. Fix $e, e' \in F$. \\
    \> 2. Assume $P(e) \wedge P(e')$, that is, each of $e$ and $e'$ has the
    same number \\
    \> \quad of left and right parens. \\
    \> 3. $P([e \wedge e'])$, that is, the expression $e \wedge e'$ has the
    same number of \\
    \> \quad left and right parens. \\
    \> \> \> \> \> By inductive hypothesis (3.2), and the fact \\ 
    \> \> \> \> \> that we're adding one left and one right \\
    \> \> \> \> \> paren. \\
    \> 4. QED 
    \> \> \> \> Implication, UG \\
    4. (Inductive step) 
    $\forall e, e' \in F (P(e) \wedge P(e') \Rightarrow P([e \vee e'])$
    \\
    \> \> \> \> \> Similar to the previous case. \\
    5. (Inductive step) 
    $\forall e \in F (P(e) \Rightarrow P([\neg e])$
    \> \> \> \> \> Similar to the previous case. \\
    6. QED
    \> \> \> \> \> Structural induction on Boolean expressions
  \end{structproof}
\end{proof}

\begin{theorem}
  The number of edges in any binary tree is exactly one fewer than the
  number of nodes. 
\end{theorem}
\begin{proof}
  Define $P(t)$: Binary tree $t$ has exactly $1$ fewer edges than nodes\.
  We are using the notation $\ms{nodes}(t)$, $\ms{edges}(t)$\. 
  The key is that the inductive steps all preserve the ``deficit'' of
  1\. 
  For instance, combining two trees involves adding two edges and one
  node; since each subtree had a ``deficit'' of 1, this maintains the
  deficit of 1:
                                %[[[Victor: slide]]]
  \begin{structproof}
    Prove: $\forall t \in T (P(t))$ \\
    1. (Base) $P(n)$, where $n$ is the single-node tree. 
    \> \> \> \> \> $0$ edges and $1$ node \\
    2. (Inductive step) 
    $\forall t \in T (P(t) \Rightarrow P(\ms{makeleft}(t))$ \\
    \> 1. Fix $t$. \\
    \> 2. Assume $P(t)$, that is, $|\ms{edges}(t)|+1 = |\ms{nodes}(t)|$. \\
    \> 3. $P(\ms{makeleft}(t))$, that is,
    $|\ms{edges}(\ms{makeleft}(t))|+1 = |\ms{nodes}(\ms{makeleft}(t))|$. \\
    \> \> 1. $|\ms{edges}(\ms{makeleft}(t))| = |\ms{edges}(t)| + 1$ \\
    \> \> 2. $|\ms{nodes}(\ms{makeleft}(t))| = |\ms{nodes}(t)| + 1$. \\
    \> \> 3. QED
    \> \> \> Algebra, using 2.2, 2.3.1, 2.3.2 \\
    \> 4. QED
    \> \> \> \> Implication, UG \\
    3. (Inductive step) 
    $\forall t \in T (P(t) \Rightarrow P(\ms{makeright}(t))$ 
    \> \> \> \> \> Similar to the previous case. \\
    4. (Inductive step) 
    $\forall t, t' \in T (P(t) \wedge P(t') \Rightarrow P(\ms{makeboth}(t,t'))$ \\
    \> 1. Fix $t$. \\
    \> 2. Assume $P(t) \wedge P(t')$, that is, $|\ms{edges}(t)|+1 =
    |\ms{nodes}(t)|$ and $|\ms{edges}(t')|+1 =|\ms{nodes}(t')|$. \\
    \> 3. $P(\ms{makeboth}(t,t'))$, that is,
    $|\ms{edges}(\ms{makeboth}(t,t'))|+1 = |\ms{nodes}(\ms{makeboth}(t))|$. \\
    \> \> 1. $|\ms{edges}(\ms{makeboth}(t,t'))| = |\ms{edges}(t)| +
    |\ms{edges}(t')| + 2$ \\
    \> \> 2. $|\ms{nodes}(\ms{makeboth}(t,t'))| = |\ms{nodes}(t)| +
    |\ms{nodes}(t')| + 1$. \\
    \> \> 3. QED
    \> \> \> Algebra, using 4.2, 4.3.1, and 4.3.2 \\
    \> 4. QED
    \> \> \> \> Implication, UG \\
    5. QED
    \> \> \> \> \> Structural induction on binary trees
  \end{structproof}
\end{proof}


\subsubsection{A string Theorem}

Here is a more complex proof, illustrating a combination of structural
induction and strengthening the hypothesis.

\forstudents{
\begin{theorem}
  In a string of $0$s and $1$s, the number of occurrences of the pattern
  $01$ is less than or equal to the number of occurrences of $10$, plus
  one.
\end{theorem}

Let's try to prove this by structural induction\.  First we must
define $P(s)$\.  Let's write $\ms{num}(pat,s)$ as the number of
occurrences of the pattern string pat in s\.  Now our inductive
hypothesis is
\[
P(s): \ms{num}(01,s) \leq \ms{num}(10,s) + 1. 
\]
If you try to prove this by structural induction, you will get
stuck\.
Why\? 
Consider what happens when you add $1$ at the end\.  
This could increase the number of $01$s without increasing the number of
$10$s\. 

So, to prove by structural induction on strings, let's strengthen the
hypothesis by adding another clause\.  If a string ends in $0$ then
the number of $01$s is less than or equal to the number of $10$s\.
That solves the problem by weakening what we have to show when the
string ends in $1$\.  But maybe it causes another problem somewhere
else\.  Let's give it a try: \\ 
\\
Redefine $P(s)$: \\
$\ms{num}(01,s) \leq \ms{num}(10,s) + 1$, \\
and \\
If $s$ ends in $0$ then $\ms{num}(01,s) \leq \ms{num}(10,s)$. \\
\\
This means that, for each inductive step, we have two things to show:
                                %[[[Victor: slide]]]
\structuredproof{
  Prove: $\forall s \in S (P(s))$ \\
  1. (Base) $P(\lambda)$ 
  \> \> \> \> \> \reason{No patterns of either kind.} \\
  2. (Inductive step) $\forall s \in S (P(s) \Rightarrow P(s 0))$ \\
  \> 1. Fix $s$. \\
  \> 2. Assume $P(s)$. \\
  \> 3. $P(s 0)$ \\
  \> \> 1. $\ms{num}(01,s0) \leq \ms{num}(10,s0) + 1$. 
  \> \> \> \reason{???} \\
  \> \> 2. If $s 0$ ends in $0$ then $\ms{num}(01,s0) \leq
  \ms{num}(10,s0)$. \noreason \\
  \> \> \> \> \> \reason{???} \\
  \> \> 3. QED
  \> \> \> \reason{Conjunction} \\
  \> 4. QED 
  \> \> \> \> \reason{Implication, UG} \\
  3. (Inductive step) $\forall s \in S (P(s) \Rightarrow P(s 1))$ \\
  \> 1. Fix $s$. \\
  \> 2. Assume $P(s)$. \\
  \> 3. $P(s 1)$ \\
  \> \> 1. $\ms{num}(01,s1) \leq \ms{num}(10,s1) + 1$. 
  \> \> \> \reason{???} \\
  \> \> 2. If $s 1$ ends in $0$ then $\ms{num}(01,s1) \leq
  \ms{num}(10,s1)$.\noreason \\
  \> \> \> \> \> \reason{???} \\
  \> \> 3. QED
  \> \> \> \reason{Conjunction} \\
  \> 4. QED 
  \> \> \> \> \reason{Implication, UG} \\
  4. QED
  \> \> \> \> \> \reason{Structural induction on strings.}\\
}

First let's consider $s1$\. 
This is the case that looks dangerous, because it might increase the
number of $01$s\. 
We have to prove two statements\. 
The second is easy, because the new string doesn't end in $0$\. 
We say it's ``vacuously true''\. 

The first statement now takes some work\. 
We might be adding to the number of $01$s\.  
However, if we do, the previous string must have ended with $0$\. 
Then the inductive hypothesis says that the previous string had to
satisfy the stronger inequality in the second statement\. 
Adding one to the LHS of the stronger inequality yields the weaker
inequality we want\.

The following proof fragment considers cases based on whether $s$ ends
in $0$ or not\. 
If not, it might end in $1$, or might be empty (don't forget this
possibility). 

\begin{structproof}
  \> 3. $P(s 1)$ \\
  \> \> 1. $\ms{num}(01,s1) \leq \ms{num}(10,s1) + 1$. \\
  \> \> \> 1. If $s$ ends in $0$ then $\ms{num}(01,s1) \leq\ms{num}(10,s1) + 1$. \\
  \> \> \> \> 1. Assume $s$ ends in $0$. \\
  \> \> \> \> 2. $\ms{num}(01,s) \leq \ms{num}(10,s)$ 
  \> Inductive hypothesis (3.2), part 2. \\
  \> \> \> \> 3. $\ms{num}(01,s1) = \ms{num}(01,s) + 1$ 
  \> Adding one more $01$. \\
  \> \> \> \> 4. $\ms{num}(10,s1) = \ms{num}(10,s)$ \\
  \> \> \> \> 5. $\ms{num}(01,s1) \leq\ms{num}(10,s1) + 1$. 
  \> Algebra (combining 3.3.1.1.2, ...3, and ...4) \\
  \> \> \> \> QED 
  \> Implication \\
  \> \> \> 2. If $s$ ends in $1$ then $\ms{num}(01,s1)\leq\ms{num}(10,s1) + 1$. \\
  \> \> \> \> \> Inductive hypothesis, part 1; no new $01$s. \\
  \> \> \> 3. If $s = \lambda$ then $\ms{num}(01,s1) \leq\ms{num}(10,s1)+ 1$. \\
  \> \> \> \> \> $s1$ is just $1$, which has no $01$s. \\
  \> \> \> 4. QED 
  \> \> Cases \\
  \> \> 2. If $s 1$ ends in $0$ then $\ms{num}(01,s1) \leq \ms{num}(10,s1)$. \\
  \> \> \> \> \> Vacuously true, because $s1$ doesn't end in $0$. \\
  \> \> 3. QED
  \> \> \> Conjunction \\
\end{structproof}
Of course, you could also expand the step for $s$ ending in $1$ into a
careful series of inequalities. \\
\\
Now consider $s0$\.
We hope that what we did to make the $s1$ case work doesn't mess up
the $s0$ case\. 
But we have to check\. 

The first statement is easy\. 
It follows from the first statement of the inductive
hypothesis for $s$, because we are not increasing the number of $01$s\. 
But now the second statement takes more work\.
The difficulty is that the new string ends in $0$, which means that we
have to show the stronger inequality in the second statement\.
But to do this, we might only have the weaker inequality for the previous
string\.
The argument again depends on what the previous string $s$ ended with\.
So again, we consider cases, based on whether $s$ ends in $0$ or $1$,
or is empty\.
If $s$ ends in $0$ we rely on the second statement of the inductive
hypothesis for $s$ (with the stronger inequality), whereas if $s$ ends
in $1$ we rely on the first statement (with the weaker inequality)\.
In this case, we have to ``turn the weaker inequality into the
stronger inequality''.

\structuredproof[38ex]{
  \> 3. $P(s 0)$ \\
  \> \> 1. $\ms{num}(01,s0) \leq \ms{num}(10,s0) + 1$.
  \reason{Induct. hypothesis, part 1; no new $01$s.} \\
  \> \> 2. If $s 0$ ends in $0$ then $\ms{num}(01,s0) \leq\ms{num}(10,s0)$. \\
  \> \> \> 1. $\ms{num}(01,s0) \leq \ms{num}(10,s0)$. \\
  \> \> \> \> 1. If $s$ ends in $0$ then $\ms{num}(01,s0)
  \leq\ms{num}(10,s0)$. \noreason \\
  \reason{Induct. hypothesis, part 2; no new $01$s} \\
  \> \> \> \> 2. If $s$ ends in $1$ then $\ms{num}(01,s0)
  \leq\ms{num}(10,s0)$. \noreason \\ 
  \> \> \> \> \> 1. Assume $s$ ends in $1$. \\
  \> \> \> \> \> 2. $\ms{num}(01,s) \leq \ms{num}(10,s) + 1$. 
  \reason{Inductive hypothesis, part 1} \\
  \> \> \> \> \> 3. $\ms{num}(01,s0) = \ms{num}(01,s)$ \\
  \> \> \> \> \> 4. $\ms{num}(10,s0) = \ms{num}(10,s) + 1$ 
  \reason{Exactly one new occurrence of $10$.} \\
  \> \> \> \> \> 5. $\ms{num}(01,s0) \leq \ms{num}(10,s0)$ 
  \reason{Algebra} \\
  \> \> \> \> \> 6. QED
  \reason{Implication} \\
  \> \> \> \> 3. If $s = \lambda$ then $\ms{num}(01,s0) \leq
  \ms{num}(10,s0)$. \noreason \\ 
  \> \> \> \> \> \> 
\reason{$s0$ is just $1$, which has no $01$s or $10$s.} \\
  \> \> \> \> 4. QED 
  \> \> \reason{Cases} \\
  \> \> \> 2. QED
  \> \> \reason{Propositional reasoning (truth table)} \\
  \> \> 3. QED 
  \> \> \> \reason{Conjunction}\\
}

If you actually write out all these cases in the proof, you will
notice that some facts are stated repeatedly, e.g., that when you add
a $0$ to the end of a string you are not increasing the number of $01$s. \\
To avoid having to state these facts several times, you can move them
earlier in the proof\.
}

\subsection{Recursively-defined functions on recursively-defined data
  types}

Recursive definitions provide a natural way to define functions whose
domains are recursively-defined data types\.
\\
\begin{example}(Boolean Expressions)
  Define $\ms{eval}$, a function from Boolean expressions to $\{ 0, 1
  \}$, by: 
\begin{quote}
  $\ms{eval}(0) = 0$ \\
  $\ms{eval}(1) = 1$ \\
  $\ms{eval}([e \wedge e']) = 1$ if $\ms{eval}(e) = \ms{eval}(e') = 1$, $0$ otherwise. \\
  $\ms{eval}([e \vee e']) = 0$ if $\ms{eval}(e) = \ms{eval}(e') = 0$, $1$ otherwise. \\
  $\ms{eval}([\neg e]) = 0$ if $\ms{eval}(e) = 1$, $1$ otherwise. 
\end{quote}
\end{example}

\begin{example} (Strings)
For strings over alphabet $A$, define the function $\ms{length}(s)$ as
follows:
\begin{quote}
$\ms{length(\lambda)}=0$ (the empty string)\\
$\ms{length}(sa) = \ms{length}(s)+1$ for string $s$ and $a\in A$.\\
\end{quote}
\end{example}

\begin{example} (Binary Trees)
  Define the function $\ms{numnodes}(t)$ (a formal definition of what
  we previously used intuitively to be the number of nodes in the tree
  $t$), by: 
\begin{quote}
  $\ms{numnodes}(\mbox{single node}) = 1$ \\
  $\ms{numnodes}(\ms{makeleft}(t)) = \ms{numnodes}(t) + 1$ \\
  $\ms{numnodes}(\ms{makeright}(t)) = \ms{numnodes}(t) + 1$ \\
  $\ms{numnodes}(\ms{makeboth}(t,t')) = \ms{numnodes}(t)
  +\ms{numnodes}(t') + 1$ 
\end{quote}

Similarly,  define $\ms{numedges}(t)$: 
\begin{quote}
  $\ms{numedges}(\mbox{single node}) = 0$ \\
  $\ms{numedges}(\ms{makeleft}(t)) = \ms{numedges}(t) + 1$ \\
  $\ms{numedges}(\ms{makeright}(t)) = \ms{numedges}(t) + 1$ \\
  $\ms{numedges}(\ms{makeboth}(t)) = \ms{numedges}(t) +
  \ms{numedges}(t') + 2$ 
\end{quote}
\end{example}

We can use structural induction to prove properties of functions
defined in this way\.
For example, we can reprove the relationship between numbers of nodes
and edges in terms of the formal functions $\ms{numnodes}$ and
$\ms{numedges}$\.
(The argument is pretty much the same as before, just using the formal
function definitions instead of relying on our understanding of the
sizes of sets.) \\

\forstudents{
Define $P(t)$: 
$\ms{numnodes}(t) = \ms{numedges}(t) + 1$. 
                                %[[[Victor: slide]]]
\begin{structproof}
  Prove: $\forall t \in T (P(t))$ \\
  1. (Base) $P(t_0)$, where $t_0$ is the single-node tree. 
  \> \> \> \> \> By definition, $\ms{numnodes}(t_0) = 1$ \\
  \> \> \> \> \> and $\ms{numedges}(t_0) = 0$ \\
  2. (Inductive step) 
  $\forall t \in T (P(t) \Rightarrow P(\ms{makeleft}(t))$ \\
  \> 1. Fix $t$. \\
  \> 2. Assume $P(t)$, that is, $\ms{numedges}(t)+1 = \ms{numnodes}(t)$. \\
  \> 3. $P(\ms{makeleft}(t))$, that is,
  $\ms{numedges}(\ms{makeleft}(t))+1 = \ms{numnodes}(\ms{makeleft}(t))$. \\
  \> \> 1. $\ms{numedges}(\ms{makeleft}(t)) = \ms{numedges}(t) + 1$ \\
  \> \> \> \> \> Definition of $\ms{numedges}$ \\
  \> \> 2. $\ms{numnodes}(\ms{makeleft}(t)) = \ms{numnodes}(t) + 1$ \\
  \> \> \> \> \> Definition of $\ms{numnodes}$ \\
  \> \> 3. QED
  \> \> \> Algebra \\
  \> 4. QED \\
  3. (Inductive step) 
  $\forall t \in T (P(t) \Rightarrow P(\ms{makeright}(t))$ 
  \> \> \> \> \> Similar to the previous case. \\
  4. (Inductive step) 
  $\forall t, t' \in T (P(t) \wedge P(t') \Rightarrow P(\ms{makeboth}(t,t'))$ \\
  \> 1. Fix $t$. \\
  \> 2. Assume $P(t) \wedge P(t')$, that is, \\
  \> \quad $\ms{numedges}(t)+1 = \ms{numnodes}(t)$ and $\ms{numedges}(t')+1 =\ms{numnodes}(t')$. \\
  \> 3. $P(\ms{makeboth}(t,t'))$, that is,
  $\ms{numedges}(\ms{makeboth}(t,t'))+1 = \ms{numnodes}(\ms{makeboth}(t))$. \\
  \> \> 1. $\ms{numedges}(\ms{makeboth}(t,t')) = \ms{numedges}(t) +
  \ms{numedges}(t') + 2$ \\
  \> \> \> \> \> Definition of $\ms{numedges}$ \\
  \> \> 2. $\ms{numnodes}(\ms{makeboth}(t,t')) = \ms{numnodes}(t) +
  \ms{numnodes}(t') + 1$ \\
  \> \> \> \> \> Definition of $\ms{numnodes}$ \\
  \> \> 3. QED
  \> \> \> Algebra \\
  \> 4. QED \\
  5. QED
  \> \> \> \> \> Structural induction on binary trees
\end{structproof}
}

\forstudents{ We've connected structural induction to recursive
  definitions.  In a sense, this connection also holds for the natural
  numbers.  One can think of the natural numbers as a recursively
  defined set ($0\in\naturals$, and if $n\in\naturals$ then $n+1 \in
  \naturals$), and of normal induction as a structural induction on
  this recursive definition. }
