\documentclass[10pt]{article}
\usepackage[pdftex]{color}
\usepackage[paperwidth=485mm,paperheight=550mm]{geometry}
\usepackage{amssymb}
\setlength{\topmargin}{-36mm}
\setlength{\textwidth}{485mm}
\setlength{\textheight}{550mm}
\setlength{\evensidemargin}{0cm}
\setlength{\oddsidemargin}{-23mm}
\setlength{\parindent}{0cm}
\setlength{\parskip}{1ex}
\setlength{\unitlength}{1mm}
\sloppy


\begin{document}

\definecolor{fLb}      {rgb}{0.70,0.50,0.50}   % label
\definecolor{fCj}      {rgb}{0.00,0.00,0.00}   % conjecture
\definecolor{fPr}      {rgb}{0.50,0.70,0.50}   % proof
\definecolor{fRf}      {rgb}{0.50,0.50,0.70}   % reference
\definecolor{fEq}      {rgb}{0.50,0.50,0.50}   % proof equality
\definecolor{fLn}      {rgb}{0.99,0.00,0.00}   % "uses"-line
\definecolor{fLg}      {rgb}{0.70,0.70,0.50}   % legend


\newcommand{\lm}[1]{%                                  % lemma
\begin{array}{r@{\;}ll}%
#1%
\end{array}%
}

\newcommand{\lb}[1]{%                                  % lemma label
\multicolumn{3}{l}{\mbox{\textcolor{fLb}{\bf Lemma #1:}}}\\[1ex]%
}

\newcommand{\df}[1]{%                                  % definition label
\multicolumn{3}{l}{\mbox{\textcolor{fLb}{\bf Definition #1:}}}\\[1ex]%
}

\newcommand{\cj}[2]{%                                  % conjecture
& \multicolumn{2}{l}{\color{fCj}\mbox{\Huge $\mathbf{#1}$}}\\[1ex]
\multicolumn{1}{l}{\color{fCj}\mbox{\Huge $\mathbf{=}$}}
& \multicolumn{2}{l}{\color{fCj}\mbox{\Huge $\mathbf{#2}$}}\\[1ex]
}

\newcommand{\pr}[1]{%                                  % proof
\multicolumn{3}{l}{%
        \mbox{\textcolor{fPr}{Proof by induction on $#1$:}}}\\%
}

\newcommand{\bc}{%                                     % base case
\multicolumn{3}{l}{\mbox{\textcolor{fPr}{Base case:}}}\\%
}

\newcommand{\ic}{%                                     % inductive case
\multicolumn{3}{l}{\mbox{\textcolor{fPr}{Inductive case:}}}\\%
}

\newcommand{\rs}[1]{%                                  % reason
\mbox{\textcolor{fRf}{ by #1}}%
}

\color{fLn}
\begin{picture}(0,0)%
\thicklines%
\put(035,390){\vector(0,-1){50}}% 5 - 7
\put(055,260){\vector(2,-1){90}}% 7 - 11
\put(200,115){\vector(2,-1){90}}% 11 - 12
\put(150,390){\vector(-2,-1){100}}% 6 - 7
\put(310,390){\vector(0,-1){50}}% 8 - 9
\put(310,255){\vector(0,-1){50}}% 9 - 13
\put(280,390){\vector(-1,-2){87}}% 8 - 11
\put(420,390){\line(0,-1){275}}% 10 - 12
\put(420,115){\vector(-2,-1){90}}% 10 - 12
%
\put(035.15,390.15){\line(0,-1){50}}% 5 - 7
\put(055.15,260.15){\line(2,-1){90}}% 7 - 11
\put(200.15,115.15){\line(2,-1){90}}% 11 - 12
\put(150.15,390.15){\line(-2,-1){100}}% 6 - 7
\put(310.15,390.15){\line(0,-1){50}}% 8 - 9
\put(310.15,255.15){\line(0,-1){50}}% 9 - 13
\put(280.15,390.15){\line(-1,-2){87}}% 8 - 11
\put(420.15,390.15){\line(0,-1){275}}% 10 - 12
\put(420.15,115.15){\line(-2,-1){90}}% 10 - 12
%
\put(034.85,389.85){\line(0,-1){50}}% 5 - 7
\put(054.85,259.85){\line(2,-1){90}}% 7 - 11
\put(199.85,114.85){\line(2,-1){90}}% 11 - 12
\put(149.85,389.85){\line(-2,-1){100}}% 6 - 7
\put(309.85,389.85){\line(0,-1){50}}% 8 - 9
\put(309.85,254.85){\line(0,-1){50}}% 9 - 13
\put(279.85,389.85){\line(-1,-2){87}}% 8 - 11
\put(419.85,389.85){\line(0,-1){275}}% 10 - 12
\put(419.85,114.85){\line(-2,-1){90}}% 10 - 12
\end{picture}
\color{fEq}
$\begin{array}[b]{ccccccc}
\rule{65mm}{0mm}
& \rule{65mm}{0mm}
& \rule{65mm}{0mm}
& \rule{65mm}{0mm}
& \rule{65mm}{0mm}
& \rule{65mm}{0mm}
& \rule{65mm}{0mm} \\
%
\lm{
\df{1}
\cj{x+0}{x}
}
%
&
&
%
\lm{
\df{2}
\cj{x+Sy}{S(x+y)}
}
%
&
&
%
\lm{
\df{3}
\cj{x \cdot 0}{0}
}
%
&
&
%
\lm{
\df{4}
\cj{x \cdot Sy}{x \cdot y+x}
}
%
\\
&
&
&
&
&
&
\\[50mm]
%
\lm{
\lb{5}
\cj{0+x}{x}
\pr{x}
\bc
& 0+0                &                       \\
= & 0          & \rs{Def.\ 1}  \\
\ic
& 0+Sx       &                       \\
= & S(0+x)     & \rs{Def.\ 2}  \\
= & Sx         & \rs{I.H.}     \\
}
%
&
&
%
\lm{
\lb{6}
\cj{Sx+y}{S(x+y)}
\pr{y}
\bc
& Sx+0       &                       \\
= & Sx         & \rs{Def.\ 1}  \\
= & S(x+0)     & \rs{Def.\ 1}  \\
\ic
& Sx+Sy      &                       \\
= & S(Sx+y)    & \rs{Def.\ 2}  \\
= & SS(x+y)    & \rs{I.H.}     \\
= & S(x+Sy)    & \rs{Def.\ 2}  \\
}
%
&
&
%
\lm{
\lb{8}
\cj{(x+y)+z}{x+(y+z)}
\pr{z}
\bc
& (x+y)+0    &                       \\
= & x+y                & \rs{Def.\ 1}  \\
= & x+(y+0)    & \rs{Def.\ 1}  \\
\ic
& (x+y)+Sz   &                       \\
= & S((x+y)+z) & \rs{Def.\ 2}  \\
= & S(x+(y+z)) & \rs{I.H.}     \\
= & x+S(y+z)   & \rs{Def.\ 2}  \\
= & x+(y+Sz)   & \rs{Def.\ 2}  \\
}
%
&
&
%
\lm{
\lb{10}
\cj{0 \cdot x}{0}
\pr{x}
\bc
& 0 \cdot 0          &                       \\
= & 0          & \rs{Def.\ 3}  \\
\ic
& 0 \cdot Sx &                       \\
= & 0 \cdot x+0        & \rs{Def.\ 4}  \\
= & 0+0                & \rs{I.H.}     \\
= & 0          & \rs{Def.\ 1}  \\
}
%
\\
&
&
&
&
&
&
\\[50mm]
%
\lm{
\lb{7}
\cj{x+y}{y+x}
\pr{y}
\bc
& x+0                &                       \\
= & x          & \rs{Def.\ 1}  \\
= & 0+x                & \rs{Lem.\ 5}  \\
\ic
& x+Sy       &                       \\
= & S(x+y)     & \rs{Def.\ 2}  \\
= & S(y+x)     & \rs{I.H.}     \\
= & Sy+x       & \rs{Lem.\ 6}  \\
}
%
&
&
&
&
%
\lm{
\lb{9}
\cj{x \cdot (y+z)}{x \cdot y+x \cdot z}
\pr{z}
\bc
& x \cdot (y+0)      &                       \\
= & x \cdot y          & \rs{Def.\ 1}  \\
= & x \cdot y+0        & \rs{Def.\ 1}  \\
= & x \cdot y+x \cdot 0        & \rs{Def.\ 3}  \\
\ic
& x \cdot (y+Sz)     &                       \\
= & x \cdot S(y+z)     & \rs{Def.\ 2}  \\
= & x \cdot (y+z)+x    & \rs{Def.\ 4}  \\
= & (x \cdot y+x \cdot z)+x    & \rs{I.H.}     \\
= & x \cdot y+(x \cdot z+x)    & \rs{Lem.\ 8}  \\
= & x \cdot y+x \cdot Sz       & \rs{Def.\ 4}  \\
}
%
&
&
\\
&
&
&
&
&
&
\\[50mm]
&
&
%
\lm{
\lb{11}
\cj{Sx \cdot y}{x \cdot y+y}
\pr{y}
\bc
& Sx \cdot 0 &                       \\
= & 0          & \rs{Def.\ 3}  \\
= & 0+0                & \rs{Def.\ 1}  \\
= & x \cdot 0+0        & \rs{Def.\ 4}  \\
\ic
& Sx \cdot Sy        &                       \\
= & Sx \cdot y+Sx      & \rs{Def.\ 4}  \\
= & (x \cdot y+y)+Sx   & \rs{I.H.}     \\
= & S((x \cdot y+y)+x)& \rs{Def.\ 2}   \\
= & S(x \cdot y+(y+x))& \rs{Lem.\ 8}   \\
= & S(x \cdot y+(x+y))& \rs{Lem.\ 7}   \\
= & S((x \cdot y+x)+y)& \rs{Lem.\ 8}   \\
= & (x \cdot y+x)+Sy   & \rs{Def.\ 2}  \\
= & x \cdot Sy+Sy      & \rs{Def.\ 4}  \\
}
%
&
&
%
\lm{
\lb{13}
\cj{(x \cdot y) \cdot z}{x \cdot (y \cdot z)}
\pr{z}
\bc
& (x \cdot y) \cdot 0        &                       \\
= & 0          & \rs{Def.\ 3}  \\
= & x \cdot 0          & \rs{Def.\ 3}  \\
= & x \cdot (y \cdot 0)        & \rs{Def.\ 3}  \\
\ic
& (x \cdot y) \cdot Sz       &                       \\
= & (x \cdot y) \cdot z+x \cdot y      & \rs{Def.\ 4}  \\
= & x \cdot (y \cdot z)+x \cdot y      & \rs{I.H.}     \\
= & x \cdot (y \cdot z+y)      & \rs{Lem.\ 9}  \\
= & x \cdot (y \cdot Sz)       & \rs{Def.\ 4}  \\
}
%
&&
\\
&
&
&
&
&
&
\\[50mm]
\color{fLg}
\begin{tabular}{ll|}
\hline
\multicolumn{2}{l|}{\bf Legend:}       \\
$S(x)$ & Successor of $x$      \\
Def. & Definition      \\
Lem. & Lemma   \\
I.H. & Induction Hypothesis    \\
\multicolumn{2}{l|}{\bf Binding Priorities:}   \\
%\multicolumn{2}{l}{$S$ , $ \cdot $ , $+$}     \\
\multicolumn{2}{l|}{$Sx \cdot y+z$ denotes $((S(x)) \cdot y)+z$}       \\
\multicolumn{2}{l|}{\bf Used Induction Scheme:}        \\
If & $P(0)$    \\
and & $P(x)$ always implies $P(Sx)$,   \\
then & always $P(x)$.  \\
&\\
\multicolumn{2}{l|}{Red arrow: use of lemma}   \\
\multicolumn{2}{l|}{Definition-uses omitted}   \\
\end{tabular}
&
&
&
&
%
\lm{
\lb{12}
\cj{x \cdot y}{y \cdot x}
\pr{y}
\bc
& x \cdot 0          &                       \\
= & 0          & \rs{Def.\ 3}  \\
= & 0 \cdot x          & \rs{Lem.\ 10} \\
\ic
& x \cdot Sy &                       \\
= & x \cdot y+x        & \rs{Def.\ 4}  \\
= & y \cdot x+x        & \rs{I.H.}     \\
= & Sy \cdot x & \rs{Lem.\ 11} \\
}
%
&
&
\\
\rule{0cm}{0cm}
\\
\end{array}$


\end{document}