\documentclass{slides}

\setlength{\oddsidemargin}{-.5in}
\setlength{\topmargin}{-1in}
\setlength{\textheight}{7 in}
\setlength{\textwidth}{8.9 in}

\newcommand{\ms}[1]{\textit{#1}}

\begin{document}

\begin{slide}
\begin{tabbing}
XXX\=XXX\=XXX\=XXX\=XXXXXXXXXXXXXXXXXXXXX\=    \kill
Prove: $\forall n \geq k (P(n))$ \\
1. (Base) $P(k)$ \\
2. (Inductive step) 
$\forall n \geq k [(\forall i, k \leq i \leq n (P(n))) \Rightarrow P(n+1)]$ \\
\> 1. Fix $n \geq k$ \\
\> 2. Assume $\forall  i, k \leq i \leq n (P(i))$ \\
\> 3. $P(n+1)$ \\
\> 4. QED
    \> \> \> \> Implication, UG \\
3. QED                        
\> \> \> \> \> Strong induction 
\end{tabbing}
\end{slide}

\begin{slide}
\begin{tabbing}
XXX\=XXX\=XXX\=XXX\=XXXXXXXXXXXXXXXXXXXXX\=    \kill
Prove: $\forall n \geq k (P(n))$ \\
1. (Base) $P(k)$ \\
2. (Base) $P(k+1)$ \\
3. (Inductive step) 
$\forall n \geq k+1 [(\forall i, k \leq i \leq n (P(n))) \Rightarrow P(n+1)]$ \\
\> 1. Fix $n \geq k+1$ \\
\> 2. Assume $\forall  i, k \leq i \leq n (P(i))$ \\
\> 3. $P(n+1)$ \\
\> 4. QED \\
4. QED                        
\end{tabbing}
\end{slide}

\begin{slide}
\begin{tabbing}
XXX\=XXX\=XXX\=XXX\=XXXXXXXXXXXXXX\=    \kill
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
\> \> \> \> \> Struct.\ ind.\ on Boolean exps.
\end{tabbing}
\end{slide}

\begin{slide}
\begin{tabbing}
XXX\=XXX\=XXX\=XXX\=XXXXXXXXXXXXXXX\=    \kill
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(makeleft(t))$ \\
3. (Inductive step) 
$\forall t \in T (P(t) \Rightarrow P(makeright(t))$ \\
4. (Inductive step) 
$\forall t,t' \in T (P(t) \wedge P(t') \Rightarrow P(makeboth(t,t'))$ \\
5. QED
\> \> \> \> \> Struct.\ ind.\ on binary trees
\end{tabbing}
\end{slide}

\begin{slide}
\begin{tabbing}
XXX\=XXX\=XXX\=XXX\=XXXXXXXXXXXXXXX\=    \kill
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
\> \> \> \> \> Struct.\ ind.\ on strings.
\end{tabbing}
\end{slide}


\begin{slide}
\begin{tabbing}
XXX\=XXX\=XXX\=XXX\=XXXXXXXXXXXXXX\=    \kill
Prove: $\forall e \in F (P(e))$ \\
1. (Base) $P(0)$ 
\> \> \> \> \> $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 \\
\> \qquad same no.\ of left and right parens. \\
\> 3. $P((e \wedge e'))$, that is, the exp.\ $e \wedge e'$ has same no. \\ 
\> \qquad of left and right parens. 
   \> \> \> \> By ind.\ hyp.\ (3.2), and adding \\
\> \> \> \> \> \quad 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
\> \> \> \> \> Struct.\ ind.\ on Boolean exps
\end{tabbing}
\end{slide}

\begin{slide}
\small
\begin{tabbing}
XXX\=XXX\=XXX\=XXX\=XXXXXXXXXXXXXXXXXXXXXX\=    \kill
Prove: $\forall t \in T (P(t))$ \\
1. (Base) $P(n)$, where $n$ is single-node tree. 
\> \> \> \> \> $0$ edges, $1$ node \\
2. (Inductive step) 
$\forall t \in T (P(t) \Rightarrow P(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, 2.2, 2.3.1, 2.3.2 \\
\> 4. QED
   \> \> \> \> Implication, UG \\
3. (Inductive step) 
$\forall t \in T (P(t) \Rightarrow P(makeright(t))$ 
\> \> \> \> \> Similar to prev.\ case. \\
4. (Inductive step) 
$\forall t, t' \in T (P(t) \wedge P(t') \Rightarrow P(makeboth(t,t'))$ \\
\> 1. Fix $t$. \\
\> 2. Assume $P(t) \wedge P(t')$, that is, $|\ms{edges}(t)|+1 = |\ms{nodes}(t)|$\\
\> \qquad 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, 4.2, 4.3.1, and 4.3.2 \\
\> 4. QED
   \> \> \> \> Implication, UG \\
5. QED
\> \> \> \> \> Struct.\ ind.\ on binary trees
\end{tabbing}
\end{slide}

\begin{slide}
\small
\begin{tabbing}
XXX\=XXX\=XXX\=XXX\=XXXXXXXXXXXXXXXXXXXXX\=    \kill
Prove: $\forall s \in S (P(s))$ \\
1. (Base) $P(\lambda)$ 
\> \> \> \> \> 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$. 
      \> \> \> ??? \\
\> \> 2. If $s 0$ ends in $0$ then $\ms{num}(01,s0) \leq
\ms{num}(10,s0)$. \\
\> \> \> \> \> ??? \\
\> \> 3. QED
      \> \> \> Conjunction \\
\> 4. QED 
   \> \> \> \> 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$. 
      \> \> \> ??? \\
\> \> 2. If $s 1$ ends in $0$ then $\ms{num}(01,s1) \leq \ms{num}(10,s1)$.\\
\> \> \> \> \> ??? \\
\> \> 3. QED
      \> \> \> Conjunction \\
\> 4. QED 
   \> \> \> \> Implication, UG \\
4. QED
\> \> \> \> \> Struct.\ ind.\ on strings.
\end{tabbing}
\end{slide}

\begin{slide}
\small
\begin{tabbing}
XXX\=XXX\=XXX\=XXX\=XXXXXXXXXXXXXXXXXXXXXXX\=    \kill
\> 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)$ 
            \> ind.\ hyp.\ (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 (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$. \\
\> \> \> \> \> ind.\ hyp.\, 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, \\
\> \> \> \> \> \quad because $s1$ doesn't end in $0$. \\
\> \> 3. QED
      \> \> \> Conjunction \\
\end{tabbing}
\end{slide}

\begin{slide}
\small
\begin{tabbing}
XXX\=XXX\=XXX\=XXX\=XXX\=XXXXXXXXXXXXXXXXXXCXXX\=    \kill
\> 3. $P(s 0)$ \\
\> \> 1. $\ms{num}(01,s0) \leq \ms{num}(10,s0) + 1$. 
      \> \> \> \> ind.\ hyp.\, 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)$. \\
\> \> \> \> \> \> ind.\ hyp.\, part 2; no new $01$s \\
\> \> \> \> 2. If $s$ ends in $1$ then $\ms{num}(01,s0) \leq\ms{num}(10,s0)$. \\
\> \> \> \> \> 1. Assume $s$ ends in $1$. \\
\> \> \> \> \> 2. $\ms{num}(01,s) \leq \ms{num}(10,s) + 1$. 
               \> ind.\ hyp.\, part 1 \\
\> \> \> \> \> 3. $\ms{num}(01,s0) = \ms{num}(01,s)$ \\
\> \> \> \> \> 4. $\ms{num}(10,s0) = \ms{num}(10,s) + 1$ 
               \> Exactly one new $10$. \\
\> \> \> \> \> 5. $\ms{num}(01,s0) \leq \ms{num}(10,s0)$ 
               \> Algebra \\
\> \> \> \> \> 6. QED
               \> Implication \\
\> \> \> \> 3. If $s = \lambda$ then $\ms{num}(01,s0) \leq \ms{num}(10,s0)$. \\
\> \> \> \> \> \> $s0$ is just $1$, \\
\> \> \> \> \> \> \quad which has no $01$s or $10$s. \\
\> \> \> \> 4. QED 
            \> \> Cases \\
\> \> \> 2. QED
         \> \> Propositional reasoning (truth table) \\
\> \> 3. QED 
      \> \> \> Conjunction
\end{tabbing}
\end{slide}

\begin{slide}
\small
\begin{minipage}{8in}
\begin{tabbing}
XXX\=XXX\=XXX\=XXX\=XXXXXXXXXXXXXXXXXXXXXX\=    \kill
%Prove: $\forall t \in T (P(t))$ \\
1. (Base) $P(t_0)$, where $t_0$ is the single-node tree. 
\> \> \> \> \> By def., $\ms{numnodes}(t_0) = 1$ \\
\> \> \> \> \> \quad 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$ \\
	\hspace{4in} $= \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, $\ms{numedges}(t)+1 = \ms{numnodes}(t)$ \\
\> \qquad and $\ms{numedges}(t')+1 =\ms{numnodes}(t')$. \\
\> 3. $P(\ms{makeboth}(t,t'))$, that is,
	$\ms{numedges}(\ms{makeboth}(t,t'))+1 $ \\
	\hspace{4.5in} $= \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
\> \> \> \> \> Struct.\ ind.\ on binary trees
\end{tabbing}
\end{minipage}
\end{slide}


\end{document}
