\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}