%
%  LaTeX Style file for Linear Logic
%  by Naoyuki Tamura (tamura@kobe-u.ac.jp)
%   2/15/1995
%   5/23/1996 modified
%   12/30/2020 modified
%
%  Linear Logic Connectives
%
% \usepackage{graphicx}
% \usepackage{amssymb}
%  
% Girard Notation
%
\def\girardnotation{%
  \def\drv{\;\vdash\;}%
  \def\lnot##1{{\def\arg{##1}\ifx\arg\empty()\else\arg\fi}{}^{\bot}}%
  \def\tprod{\otimes}%
  % \def\tsum{\protect\raisebox{0.2ex}{$\wp$}}%
  \def\tsum{\rotatebox[origin=c]{180}{\&}}%
  \def\vartsum{\maltese}%
  \def\tunit{{\bf 1}}%
  \def\tzero{\bot}%
  \def\dprod{\mathop{\&}}%
  \def\dsum{\oplus}%
  \def\dunit{\top}%
  \def\dzero{{\bf 0}}%
  \def\limp{\mathop{\multimap}}%
  % \def\lall{{\textstyle\bigwedge}}%
  % \def\lexists{{\textstyle\bigvee}}%
  \def\lall{\forall}%
  \def\lexists{\exists}%
}
%
% Troelstra Notation
%
\def\troelstranotation{%
  \def\drv{\;\Rightarrow\;}%
  \def\lnot##1{\mathop{\sim}##1}%
  \def\tprod{\star}%
  \def\tsum{+}%
  \def\tunit{{\bf 1}}%
  \def\tzero{{\bf 0}}%
  \def\dprod{\sqcap}%
  \def\dsum{\sqcup}%
  \def\dunit{\top}%
  \def\dzero{\bot}%
  \def\limp{\mathop{\multimap}}%
  \def\lall{\forall}%
  \def\lexists{\exists}%
}
%
% Default is Troelstra's notation
%
\troelstranotation
%
% Rule names
%
\def\LX{{\rm LX}}
\def\RX{{\rm RX}}
\def\Cut{{\rm Cut}}
\def\Ax{{\rm Ax}}
\def\Axiom{{\rm Axiom}}
\def\LR#1{{\rm L}#1}
\def\RR#1{{\rm R}#1}
\def\WR#1{{\rm W}#1}
\def\CR#1{{\rm C}#1}
\def\DR#1{{\rm D}#1}
%
% System Names
%
\def\CLL#1{\mbox{${\bf CLL}_{\rm #1}$}}
\def\ILZ#1{\mbox{${\bf ILZ}_{\rm #1}$}}
\def\ILL#1{\mbox{${\bf ILL}_{\rm #1}$}}