%%
%% This is file `logicsym.sty',
%% generated with the docstrip utility.
%%
%% The original source files were:
%%
%% logicsym.dtx  (with options: `package')
%% 
%%  Logicsym package, version 1.61
%%  October 9, 2009
%% 
%%  Rett Bull (Everett.Bull@pomona.edu)
%%  Pomona College, Computer Science Department
%% 
\def\fileversion{1.61}
\def\filedate{09 October 2009}
\def\docdate{09 October 2009}
\def\filename{logicsym.sty}
\def\packagename{logicsym}
\NeedsTeXFormat{LaTeX2e}
\ProvidesPackage{logicsym}
  [2009/10/09 v1.61
   Logicsym package for Rett Bull, Pomona College]
\RequirePackage{ifthen,array}
\DeclareOption{tfletters}{\def\tf@constant{letters}}
\DeclareOption{tfwords}{\def\tf@constant{words}}
\DeclareOption{topbottom}{\def\tf@constant{topbottom}}
\DeclareOption{ampersand}{\def\And{\mathop{\&}}}
\DeclareOption{wedge}{\def\And{\wedge}}
\DeclareOption{singlearrows}{%
  \def\Implies{\mathop{\rightarrow}}
  \def\Followsfrom{\mathop{\leftarrow}}
  \def\Iff{\mathop{\leftrightarrow}}}
\DeclareOption{doublearrows}{%
  \def\Implies{\mathop{\Rightarrow}}
  \def\Followsfrom{\mathop{\Leftarrow}}
  \def\Iff{\mathop{\Leftrightarrow}}}
\DeclareOption{equivalence}{\AtBeginDocument{\let\Iff\equiv}}
\DeclareOption{oldnames}{%
  \AtBeginDocument{%
    \let\notR\NotR
    \let\Re\Real
    \let\models\Models
    \let\notmodels\Notmodels
    \let\revmodels\Revmodels
    \let\modelequiv\Modelsequiv
    \let\proves\Proves
    \let\notproves\Notproves
    \let\revproves\Revproves
    \let\provesequiv\Provesequiv
    \let\crossout\Crossout
    \let\crossbox\Crossbox}}
\DeclareOption{crossboxgraphicx}{\def\cb@style{cbgraphicx}}
\DeclareOption{crossboxlatex}{\def\cb@style{cblatex}}
\DeclareOption{crossboxdvips}{\def\cb@style{cbdvips}}
\ExecuteOptions{topbottom,doublearrows,wedge,crossboxgraphicx}
\ProcessOptions
\newcommand{\Truthconstantfont}{\mathit}
\newcommand{\truth@constant}[3]{%
\ensuremath{%
\ifthenelse{\equal{\tf@constant}{letters}}{\Truthconstantfont{#1}}{%
\ifthenelse{\equal{\tf@constant}{words}}{\Truthconstantfont{#2}}{#3}}}}
\newcommand{\True}{\truth@constant{T}{true}{\top}}
\newcommand{\False}{\truth@constant{F}{false}{\bot}}
\newcommand{\Not}{\neg}
\newcommand{\Or}{\vee}
\newcommand{\@quantifier}[2]{#1#2\,}
\newcommand{\Forall}{\@quantifier\forall}
\newcommand{\Exists}{\@quantifier\exists}
\newcommand{\Equals}{\approx}
\newcommand{\ModelA}{\mathfrak{A}}
\newcommand{\ModelB}{\mathfrak{B}}
\newcommand{\ModelN}{\mathfrak{N}}
\newcommand{\ModelR}{\mathfrak{R}}
\newcommand{\ModelZ}{\mathfrak{Z}}
\newcommand{\Nat}{\mathbb{N}}
\newcommand{\Int}{\mathbb{Z}}
\renewcommand{\Re}{\mathbb{R}}
\newcommand{\Cx}{\mathbb{C}}
\newcommand{\NotR}{\mathbin{\Crossout{R}}}
\renewcommand{\mp}{\emph{modus ponens}}
\newcommand{\Mp}{\emph{Modus ponens}}
\newcommand{\TurnstileScale}{1.0}
\newlength{\turnstile@height}
\newlength{\turnstile@width}
\newlength{\turnstile@thickness}
\newlength{\turnstile@sep}
\newlength{\turnstile@templength}
\newlength{\turnstile@lift}
\newsavebox{\turnstile@box}
\newcommand{\turnstile@singlevertical}{%
  \rule[-0.5\turnstile@height]{\turnstile@thickness}{\turnstile@height}}
\newcommand{\turnstile@doublevertical}{%
  \turnstile@singlevertical%
  \hspace{\turnstile@sep}%
  \turnstile@singlevertical}
\newcommand{\turnstile@singlehorizontal}{%
  \rule[-0.5\turnstile@thickness]{\turnstile@width}{\turnstile@thickness}}
\newcommand{\turnstile@doublehorizontal}{%
  \setlength{\turnstile@templength}{\turnstile@sep}%
  \addtolength{\turnstile@templength}{-0.5\turnstile@thickness}%
  \rule[\turnstile@templength]{\turnstile@width}{\turnstile@thickness}%
  \hspace{-\turnstile@width}%
  \rule[-\turnstile@templength]{\turnstile@width}{\turnstile@thickness}}
\newcommand{\turnstile@setup}{%
  \setlength{\turnstile@height}{1.8ex}
  \setlength{\turnstile@height}{\TurnstileScale\turnstile@height}
  \setlength{\turnstile@width}{0.72em}
  \setlength{\turnstile@width}{\TurnstileScale\turnstile@width}
  \setlength{\turnstile@thickness}{0.05\turnstile@height} %{0.1ex}
  \setlength{\turnstile@sep}{3\turnstile@thickness} %{0.3ex}
  \settoheight{\turnstile@lift}{${+}$}
  \setlength{\turnstile@lift}{0.5\turnstile@width}}
\newcommand{\turnstile@make}[1]{%
  \turnstile@setup%
  \sbox{\turnstile@box}{\raisebox{\turnstile@lift}{#1}}%
  \mathrel{\usebox{\turnstile@box}}}
\newcommand{\turnstile@negate}[1]{%
  \turnstile@setup%
  \sbox{\turnstile@box}{%
    \hbox to\turnstile@width{\hss${\big/}$\hss}%
    \hspace{-\turnstile@width}\raisebox{\turnstile@lift}{#1}}%
  \mathrel{\usebox{\turnstile@box}}}
\newcommand\turnstile@sequence[2]{%
  \turnstile@setup%
  \sbox{\turnstile@box}{%
    \raisebox{\turnstile@lift}{#1\hspace{0.3\turnstile@width}#2}}%
  \mathrel{\usebox{\turnstile@box}}}
\newcommand{\turnstile@single}{%
  \turnstile@singlevertical%
  \hspace{-\turnstile@thickness}%
  \turnstile@singlehorizontal}
\newcommand{\turnstile@single@reverse}{%
  \turnstile@singlehorizontal%
  \hspace{-\turnstile@thickness}%
  \turnstile@singlevertical}
\newcommand{\turnstile@double}{%
  \turnstile@singlevertical%
  \hspace{-\turnstile@thickness}%
  \turnstile@doublehorizontal}
\newcommand{\turnstile@double@reverse}{%
  \turnstile@doublehorizontal%
  \hspace{-\turnstile@thickness}%
  \turnstile@singlevertical}
\newcommand{\turnstile@forces}{%
  \turnstile@doublevertical%
  \hspace{-\turnstile@thickness}%
  \addtolength{\turnstile@width}{-\turnstile@sep}%
  \addtolength{\turnstile@width}{-\turnstile@thickness}%
  \turnstile@singlehorizontal}
\newcommand{\Models}{\turnstile@make{\turnstile@double}}
\newcommand{\Revmodels}{\turnstile@make{\turnstile@double@reverse}}
\newcommand{\Modelsequiv}{%
  \turnstile@sequence{\turnstile@double}{\turnstile@double@reverse}}
\newcommand{\Notmodels}{\turnstile@negate{\turnstile@double}}
\newcommand{\Proves}{\turnstile@make{\turnstile@single}}
\newcommand{\Revproves}{\turnstile@make{\turnstile@single@reverse}}
\newcommand{\Provesequiv}{%
  \turnstile@sequence{\turnstile@single}{\turnstile@single@reverse}}
\newcommand{\Notproves}{\turnstile@negate{\turnstile@single}}
\newcommand{\Forces}{\turnstile@make{\turnstile@forces}}
\newcommand{\Notforces}{\turnstile@negate{\turnstile@forces}}
\newlength{\crossoutwidth}
\newcommand{\Crossout}[1]{%
  \settowidth{\crossoutwidth}{$#1$}%
  \hbox to\crossoutwidth{\hss${\big/}$\hss}%
  \hspace{-\crossoutwidth}#1}
\newcommand{\CrossboxMargin}{0.3}
\newcommand{\CrossboxLineThickness}{0.1}
\newbox\thecrossbox@
\newlength\crossbox@MarginWidth
\newlength\crossbox@Height
\newlength\crossbox@Depth
\newlength\crossbox@Width
\newcommand{\Crossbox}[1]{%
\setbox\thecrossbox@=\hbox{\ensuremath{#1}}
\setlength{\crossbox@MarginWidth}{\CrossboxMargin em}
\setlength{\crossbox@Height}{\ht\thecrossbox@}
\setlength{\crossbox@Depth}{\dp\thecrossbox@}
\setlength{\crossbox@Width}{\wd\thecrossbox@}
\hspace*{1\crossbox@MarginWidth}
\box\thecrossbox@
\addtolength{\crossbox@Width}{1\crossbox@MarginWidth}
\hspace{-\crossbox@Width}
\addtolength{\crossbox@Width}{1\crossbox@MarginWidth}
\crossbox@Diagonal}
\ifthenelse{\equal{\cb@style}{cblatex}}{
\newbox\thecrossbox@
\newlength{\cb@TempA}
\newlength{\cb@TempB}
\newcommand{\greater@test}[2]{
  \setlength{\cb@TempA}{#2\crossbox@Width}
  \setlength{\cb@TempB}{#1\crossbox@Height}
  \ifthenelse{\lengthtest{\cb@TempB<\cb@TempA}}}
\newcommand{\setslope}[2]{
  \def\line@cmd{\line(#1,#2)}
  \setlength{\cb@TempA}{#2\crossbox@Width}
  \divide\cb@TempA#1\relax
  \setlength{\cb@TempB}{0.5\crossbox@Height}
  \addtolength{\cb@TempB}{-0.5\cb@TempA}
  \addtolength{\cb@TempB}{-\crossbox@Depth}}
\newcommand{\crossbox@Diagonal}{%
\addtolength{\crossbox@Height}{\crossbox@Depth}
\setlength{\unitlength}{\crossbox@Width}
\greater@test{6}{1}{\setslope{1}{0}}{
\greater@test{5}{1}{\setslope{6}{1}}{
\greater@test{4}{1}{\setslope{5}{1}}{
\greater@test{3}{1}{\setslope{4}{1}}{
\greater@test{5}{2}{\setslope{3}{1}}{
\greater@test{2}{1}{\setslope{5}{2}}{
\greater@test{5}{3}{\setslope{2}{1}}{
\greater@test{3}{2}{\setslope{5}{3}}{
\greater@test{4}{3}{\setslope{3}{2}}{
\greater@test{5}{4}{\setslope{4}{3}}{
\greater@test{6}{5}{\setslope{5}{4}}{
\greater@test{1}{1}{\setslope{6}{5}}{
                    \setslope{1}{1}}}}}}}}}}}}}
\raisebox{\cb@TempB}
         {\begin{picture}(1,0)\put(0,0){\line@cmd{1}}\end{picture}}}
}{}
\ifthenelse{\equal{\cb@style}{cbdvips}}{
\newcount\crossbox@Ht
\newcount\crossbox@Wd
\newcount\crossbox@Dp
\newcount\crossbox@Tk
\newdimen\dpifactor
\newlength{\crossbox@Thickness}
\newcommand{\DPIfactor}[1]{\dpifactor=1in\relax\divide\dpifactor#1\relax}
\DPIfactor{1200}
\newcommand{\crossbox@Diagonal}{
\crossbox@Ht=\crossbox@Height \divide\crossbox@Ht\dpifactor
\crossbox@Wd=\crossbox@Width  \divide\crossbox@Wd\dpifactor
\crossbox@Dp=\crossbox@Depth  \divide\crossbox@Dp\dpifactor
\setlength{\crossbox@Thickness}{\CrossboxLineThickness ex}
\crossbox@Tk\crossbox@Thickness \divide\crossbox@Tk\dpifactor
\setlength{\unitlength}{\crossbox@Width}
\begin{picture}(1,0)
\put(0,0){\special{ps:
 matrix currentmatrix currentpoint translate newpath
 \the\crossbox@Tk\space setlinewidth
 0 \the\crossbox@Dp\space moveto
 \the\crossbox@Wd\space
 \the\crossbox@Ht\space \the\crossbox@Dp\space add neg
 lineto stroke
 setmatrix
}}
\end{picture}}
}{}
\ifthenelse{\equal{\cb@style}{cbgraphicx}}{
\RequirePackage{graphicx}
\RequirePackage{fp}
\newcount\crossbox@Count
\newcommand{\crossbox@Diagonal}{
\addtolength{\crossbox@Height}{\crossbox@Depth}
\crossbox@Count\crossbox@Height
\FPset\crossbox@Ht{\the\crossbox@Count}
\crossbox@Count=\crossbox@Width
\FPset\crossbox@Wd{\the\crossbox@Count}
\FPupn{\crossbox@Diag}
      {2 1 \crossbox@Ht{} \crossbox@Wd{} div copy mul add root}
\FPupn{\crossbox@Angle}
      {\crossbox@Ht{} \crossbox@Wd{} div arctan 180 mul pi div}
\FPround{\crossbox@Angle}{\crossbox@Angle}{1}
\raisebox{-\crossbox@Depth}
         {\rotatebox{\crossbox@Angle}
                    {\rule{\crossbox@Diag\crossbox@Width}
                          {\CrossboxLineThickness ex}}}}
}{}
\newlength\@InferFullSep
\newcommand\InferStretch{1}
\newcommand\InferAlign{b}
\newcommand\Infer{\@ifnextchar[{\@Infer}{\@Infer[\InferAlign]}}
\def\@Infer[#1]#2#3#4{%
  \setlength{\@InferFullSep}{\InferStretch\normalbaselineskip}%
  \renewcommand\arraystretch{1}\ensuremath{
  \ifthenelse{\equal{#4}{}}{\@@Infer[#1]{#2}{#3}}{\@@@Infer[#1]{#2}{#3}{#4}}\relax}}
\def\@@Infer[#1]#2#3{\begin{array}[#1]{cccc}#2\\ \hline#3\end{array}}
\def\@@@Infer[#1]#2#3#4{\begin{array}[#1]{@{}c@{}c@{}c@{}c@{}}
  \@@Infer[b]{#2}{#3}&\raisebox{0.5\@InferFullSep}{$\,#4$}\end{array}}
\newcommand\VStack[1]{\ensuremath{
  \begin{array}[b]{@{}c@{}}\vphantom{\raisebox{0.5ex}{(}}#1\end{array}}\relax}
\newcounter{bprf@State}
\newcounter{bprf@TempCount}
\newcounter{bprf@LineNumber}
\newcounter{bprf@NestCount}
\newcounter{bprf@NestLimit}
\newcounter{bprf@PendingStarts}
\newcounter{bprf@PendingStops}
\renewcommand{\thebprf@LineNumber}{\arabic{bprf@LineNumber}}
\newlength{\bprf@HLineSep}
\newlength{\bprf@VLineSep}
\newenvironment{BoxProof}[2][t]
{\setcounter{bprf@State}{-1}%
 \setcounter{bprf@LineNumber}{0}%
 \setcounter{bprf@NestCount}{0}%
 \setcounter{bprf@NestLimit}{#2}%
 \setcounter{bprf@PendingStarts}{0}%
 \setcounter{bprf@PendingStops}{0}%
 \setlength{\bprf@HLineSep}{1ex}%
 \setlength{\bprf@VLineSep}{1ex}%
 \let\item\bprf@Item%
 \let\line\bprf@Line%
 \let\linenn\bprf@LineNN%
 \ifthenelse{\boolean{bprf@QBox}}
   {\begin{tabular}[#1]
     {@{}r<{\bprf@HSpace{\arraycolsep}}
      @{}>{\bprf@LeftBlock{\vline}$}l<{$\bprf@HSpace{\arraycolsep}}
      @{}>{$\bprf@HSpace{\arraycolsep}}l<{$\bprf@HSpace{\arraycolsep}}%
      @{}>{\bprf@RightBlock{\vline}}l@{}}}
   {\begin{tabular}[#1]
     {@{}r<{\bprf@HSpace{\arraycolsep}}
      @{}>{\bprf@LeftBlock{\vline}$}l<{$\bprf@HSpace{\arraycolsep}}
      @{}>{\bprf@RightBlock{\vline}}l@{}}}
}{\setcounter{bprf@State}{1}\bprf@MakeHLines\end{tabular}}
\newboolean{bprf@QBox}
\setboolean{bprf@QBox}{false}
\newenvironment{QBoxProof}[2][t]
{\setboolean{bprf@QBox}{true}\begin{BoxProof}[#1]{#2}}
{\end{BoxProof}}
\newcommand{\bprf@ItemPreamble}{%
 \ifthenelse{-1=\value{bprf@State}}%
    {\ifthenelse{0=\value{bprf@PendingStarts}}%
      {}{\bprf@MakeFirstHLines}%
     \setcounter{bprf@State}{0}}%
    {\bprf@MakeHLines}}
\newcommand{\bprf@Item}{\@ifstar\bprf@LineNN\bprf@Line}
\newcommand{\bprf@LineNN}{\bprf@ItemPreamble&\ignorespaces}
\newcommand{\bprf@Line}{%
  \bprf@ItemPreamble%
  \refstepcounter{bprf@LineNumber}\xdef\@currentlabel{\thebprf@LineNumber}%
  \thebprf@LineNumber.&\ignorespaces}
\newcommand{\bprf@MakeFirstHLines}{%
  \backup@length\value{bprf@PendingStarts}\bprf@HLineSep%
  \backup@length0.5\backup@length%
  \advance\backup@length\value{bprf@PendingStarts}\arrayrulewidth%
  \advance\backup@length\ht\@arstrutbox%
  \advance\backup@length\dp\@arstrutbox%
  \vspace*{-\backup@length}
  \bprf@MakeHLines}
\newcommand{\StartBox}{%
 \addtocounter{bprf@PendingStarts}{1}\ignorespaces}
\newcommand{\StopBox}{%
 \addtocounter{bprf@PendingStops}{1}\ignorespaces}
\newcommand{\bprf@Narrow}{%
  \ifthenelse{\value{bprf@NestCount}<\value{bprf@NestLimit}}
    {\addtocounter{bprf@NestCount}{1}}
    {\@latex@warning{Boxes are nested too deeply}}\ignorespaces}
\newcommand{\bprf@Widen}{%
  \ifthenelse{0<\value{bprf@NestCount}}
    {\addtocounter{bprf@NestCount}{-1}}
    {\@latex@warning{Attempt to close non-existant box}}\ignorespaces}
\newcommand{\bprf@MakeHLines}{%
  \whiledo{0<\value{bprf@PendingStops}}%
    {\addtocounter{bprf@PendingStops}{-1}%
     \bprf@Gap\bprf@Widen\bprf@HLine%
     \ifthenelse{1=\value{bprf@State}\and0=\value{bprf@PendingStops}}%
       {}{\bprf@Gap}}%
  \ifthenelse{-1=\value{bprf@State}\and0<\value{bprf@PendingStarts}}%
    {\addtocounter{bprf@PendingStarts}{-1}%
     \bprf@HLine\bprf@Narrow\bprf@Gap}{}%
  \whiledo{0<\value{bprf@PendingStarts}}%
    {\addtocounter{bprf@PendingStarts}{-1}%
     \bprf@Gap\bprf@HLine\bprf@Narrow\bprf@Gap}%
  \ifthenelse{1=\value{bprf@State}}{}{\crcr}\ignorespaces}
\newcommand{\bprf@HRule}{\leaders\hrule\@height\arrayrulewidth\hfill}
\newcommand{\bprf@Gap}[1][0.5]{%
  \crcr\omit&\omit%
  \rule{0pt}{#1\bprf@HLineSep}% for vertical spacing when nesting is 0
  \bprf@LeftBlock{\rule{\arrayrulewidth}{#1\bprf@HLineSep}}%
  \ifthenelse{\boolean{bprf@QBox}}{&\omit}{}&\omit%
  \bprf@RightBlock{\rule{\arrayrulewidth}{#1\bprf@HLineSep}}}
\newcommand{\bprf@HSpace}[1]{\rule{#1}{\z@}}
\newcommand{\bprf@HLine}{%
  \crcr\omit&\omit%
  \setcounter{bprf@TempCount}{1}%
  \whiledo{\value{bprf@TempCount}<\value{bprf@NestLimit}}%
     {\rule{\arrayrulewidth}{\arrayrulewidth}%
      \ifthenelse{\value{bprf@NestCount}<\value{bprf@TempCount}}%
         {\rule{\bprf@VLineSep}{\arrayrulewidth}}{\bprf@HSpace{\bprf@VLineSep}}%
      \stepcounter{bprf@TempCount}}%
  \rule{\arrayrulewidth}{\arrayrulewidth}%
  \rule{\arraycolsep}{\arrayrulewidth}%
  \ifthenelse{\boolean{bprf@QBox}}{\bprf@HRule&\omit}{}\bprf@HRule&\omit%
  \setcounter{bprf@TempCount}{\value{bprf@NestLimit}}%
  \addtocounter{bprf@TempCount}{-1}%
  \whiledo{0<\value{bprf@TempCount}}%
     {\rule{\arrayrulewidth}{\arrayrulewidth}%
      \ifthenelse{\value{bprf@NestCount}<\value{bprf@TempCount}}%
         {\rule{\bprf@VLineSep}{\arrayrulewidth}}{\bprf@HSpace{\bprf@VLineSep}}%
      \addtocounter{bprf@TempCount}{-1}}%
  \rule{\arrayrulewidth}{\arrayrulewidth}}
\newcommand{\bprf@LeftBlock}[1]{%
  \setcounter{bprf@TempCount}{1}%
  \whiledo{\value{bprf@TempCount}<\value{bprf@NestLimit}}
     {\ifthenelse{\value{bprf@NestCount}<\value{bprf@TempCount}}
         {\bprf@HSpace{\arrayrulewidth}}{#1}%
      \bprf@HSpace{\bprf@VLineSep}%
      \stepcounter{bprf@TempCount}}%
  \ifthenelse{0<\value{bprf@NestLimit}\and
              \value{bprf@NestCount}=\value{bprf@NestLimit}}
     {#1}{\bprf@HSpace{\arrayrulewidth}}%
  \bprf@HSpace{\arraycolsep}}
\newcommand{\bprf@RightBlock}[1]{%
  \setcounter{bprf@TempCount}{\value{bprf@NestLimit}}%
  \addtocounter{bprf@TempCount}{-1}%
  \whiledo{0<\value{bprf@TempCount}}
     {\ifthenelse{\value{bprf@TempCount}<\value{bprf@NestCount}}
         {#1}{\bprf@HSpace{\arrayrulewidth}}%
      \bprf@HSpace{\bprf@VLineSep}%
      \addtocounter{bprf@TempCount}{-1}}%
  \ifthenelse{0=\value{bprf@NestCount}}
     {\bprf@HSpace{\arrayrulewidth}}{#1}%
  \bprf@HSpace{\arraycolsep}}
\endinput
%%
%% End of file `logicsym.sty'.
