\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,175){\vector(1,-1){100}}% 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,435){\line(0,-1){320}}% 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,175.15){\line(1,-1){100}}% 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,435.15){\line(0,-1){320}}% 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,174.85){\line(1,-1){100}}% 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,434.85){\line(0,-1){320}}% 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}
 \\
 \\
 \\
 \\
 \\
 \\
 \\
 \\
 }
 %
 \\
 &
 &
 &
 &
 &
 &
 \\[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}
 \\
 \\
 \\
 \\
 \\
 \\
 \\
 \\
 \\
 \\
 \\
 \\
 \\
 \\
 \\
 }
 %
 &
 &
 %
 \lm{
 \lb{13}
 \cj{(x \cdot y) \cdot z}{x \cdot (y \cdot z)}
 \pr{z}
 \\
 \\
 \\
 \\
 \\
 \\
 \\
 \\
 \\
 \\
 \\
 }
 %
 &&
 \\
 &
 &
 &
 &
 &
 &
 \\[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}
   \\
   \\
   \\
   \\
   \\
   \\
   \\
   \\
   \\
 }
 %
 &
 &
 \\
 \rule{0cm}{0cm}
 \\
 \end{array}$
\end{document}