%%
%% This is file `logicproof.sty',
%% generated with the docstrip utility.
%%
%% The original source files were:
%%
%% logicproof.dtx  (with options: `package')
%% 
%% This is a generated file.
%% 
%% Copyright (C) 2014 by Alan Davidson
%% This file may be distributed and/or modified under the
%% conditions of the LaTeX Project Public License, either
%% version 1.3 of this license or (at your option) any later
%% version. The latest version of this license is in:
%% http://www.latex-project.org/lppl.txt
%% and version 1.3 or later is part of all distributions of
%% LaTeX version 2005/12/01 or later.
\NeedsTeXFormat{LaTeX2e}
\ProvidesPackage{logicproof}[2014/03/20 v1.0 Box proofs for propositional logic]
\RequirePackage{array}
\RequirePackage{ifthen}
\newlength{\subproofhorizspace}
\setlength{\subproofhorizspace}{0.5em}
\newlength{\intersubproofvertspace}
\setlength{\intersubproofvertspace}{0.333em}
\newcounter{lp@line}% Current line number on the proof
\newcounter{lp@nested}% Number of nested subproofs we're currently in
\newcounter{lp@total@nests}% Maximum number of nested subproofs allowed
\newcounter{lp@cline@1}% Used to draw horizontal lines in subproofs
\newcounter{lp@cline@2}% Also used to draw horizontal lines in subproofs
\newcounter{lp@temp}% Temporary storage counter
\newenvironment{logicproof}[1]{%
  \setcounter{lp@line}{0}%
  \setcounter{lp@nested}{0}%
  \setcounter{lp@total@nests}{#1}%
  \setlength{\tabcolsep}{0mm}%
  \let\lp@orig@arraycr\@arraycr%
  \renewcommand{\@arraycr}{\lp@cr}%
  \renewcommand{\@currentlabel}{\p@lp@line\thelp@line}%
  \ifthenelse{%
    0=#1%
  }{%
    \def\lp@tab@format{{r@{~~~}>{$}l<{$}@{~~~~}l}}%
  }{%
    \def\lp@tab@format%
        {{r@{~~~}*{#1}{l}@{~}>{$}l<{$}@{~~~~}l@{~}*{#1}{r}}}
  }%
  \center%
  \expandafter\tabular\lp@tab@format%
  \lp@start@proof@line%
}{%
  \lp@stop@proof@line%
  \endtabular%
  \endcenter%
  \setcounter{lp@total@nests}{0}%
  \ifthenelse{%
    0=\value{lp@nested}
  }{% All is well.
  }{% There are still open subproofs.
    \def\@currenvir{subproof}%
  }
}
\newenvironment{subproof}{%
  \ifthenelse{%
    \value{lp@total@nests}>\value{lp@nested}%
  }{% All is well; don't do anything.
  }{%
    \PackageError{logicproof}{Too many nested subproofs!}{%
      Increase the maximum number of nested subproofs allowed
      in the current logicproof environment.%
    }%
  }%
  \endgroup%
  \lp@stop@proof@line%
  \lp@orig@arraycr%
  \lp@add@space%
  \lp@go@up@a@line%
  \stepcounter{lp@nested}%
  \lp@cr@clines%
  &%
  \lp@continue@proof@line%
}{%
  \ifthenelse{%
    0<\value{lp@nested}%
  }{% All is well; don't do anything.
  }{%
    \PackageError{logicproof}{Cannot end a subproof before it begins}{%
      You must have a \protect\begin{subproof} before you can use %
      \protect\end{subproof}.%
    }%
  }%
  \lp@stop@proof@line%
  \lp@cr@clines%
  \addtocounter{lp@nested}{-1}%
  \lp@extend@space%
  \lp@start@proof@line%
  \begingroup%
  \def\@currenvir{subproof}%
}
\newcommand{\lp@cr}{%
  \lp@stop@proof@line%
  \lp@orig@arraycr%
  \lp@extend@space%
  \lp@start@proof@line%
}
\newcommand{\lp@go@up@a@line}{%
  \vspace{-\ht\@arstrutbox}%
  \vspace{-\dp\@arstrutbox}%
  \vspace{-\intersubproofvertspace}%
}
\newcommand{\lp@add@space}{%
  \lp@extend@space%
  \vspace{-\ht\@arstrutbox}%
  \vspace{-\dp\@arstrutbox}%
  %\vspace{-\intersubproofvertspace}%
}
\newcommand{\lp@extend@space}{%
  \vspace{-\ht\@arstrutbox}%
  \vspace{-\dp\@arstrutbox}%
  \vspace{\intersubproofvertspace}%
  &%
  \lp@continue@proof@line%
  &%
  \lp@stop@proof@line%
  \lp@orig@arraycr%
}
\newcommand{\lp@amper}{&}
\newcommand{\lp@start@proof@line}{%
  \stepcounter{lp@line}%
  \arabic{lp@line}.%
  &%
  \lp@continue@proof@line%
}
\newcommand{\lp@continue@proof@line}{%
  \setcounter{lp@temp}{0}%
  \whiledo{\value{lp@temp}<\value{lp@nested}}{%
    \vline%
    \hspace*{\subproofhorizspace}%
    \lp@amper%
    \stepcounter{lp@temp}%
  }%
  \whiledo{\value{lp@temp}<\value{lp@total@nests}}{%
    \hspace*{\subproofhorizspace}%
    \lp@amper%
    \stepcounter{lp@temp}%
  }%
}
\newcommand{\lp@stop@proof@line}{%
  \whiledo{\value{lp@temp}>\value{lp@nested}}{%
    \addtocounter{lp@temp}{-1}%
    \lp@amper%
    \hspace*{\subproofhorizspace}%
  }%
  \whiledo{\value{lp@temp}>0}{%
    \addtocounter{lp@temp}{-1}%
    \lp@amper%
    \hspace*{\subproofhorizspace}%
    \vline%
  }%
}
\newcommand{\lp@subtract@from@counter}[2]{%
  \addtocounter{#2}{-#1}%
}
\newcommand{\lp@set@clines}{%
  \setcounter{lp@cline@1}{\value{lp@nested}}%
  \stepcounter{lp@cline@1}%
  \setcounter{lp@cline@2}{\value{lp@total@nests}}%
  \addtocounter{lp@cline@2}{\value{lp@total@nests}}%
  \addtocounter{lp@cline@2}{4}%
  \expandafter\lp@subtract@from@counter\expandafter{%
      \value{lp@nested}}{lp@cline@2}%
}
\newcommand{\lp@cr@clines}{%
  \lp@set@clines%
  \lp@orig@arraycr%
  \cline{\value{lp@cline@1}-\value{lp@cline@2}}%
}
\endinput
%%
%% End of file `logicproof.sty'.
