% $Id: notation.sty,v 1.7 2008/01/25 13:30:18 logik Exp $
% \NeedsTexFormat{LaTeX2e}[1999/06/01]% does not yet work
\ProvidesPackage{notation}[2001/04/21 General Commands]
\RequirePackage{amsmath}
\RequirePackage{amssymb}
\RequirePackage{latexsym}
\RequirePackage{verbatim}
\RequirePackage{enumerate} %allows \begin{comment} text \end{comment}

% Font commands
\newcommand{\B}{\boldsymbol}
   % Bold math symbol, use as \B{a}
\newcommand{\C}[1]{\mathcal{#1}}
   % Euler Script - only caps, use as \C{A}
\newcommand{\D}[1]{\mathbb{#1}}
   % Doubles - only caps, use as \D{A}
\newcommand{\F}[1]{\mathfrak{#1}}
   % Fraktur, use as \F{a}

\newcommand{\betabf}{\beta\hspace{-1.35ex}\beta\hspace{-1.35ex}\beta}
   % bold beta
\newcommand{\lambf}{\lambda\hspace{-1.28ex}\lambda\hspace{-1.28ex}\lambda}
   % bold lambda
\newcommand{\etabf}{\eta\hspace{-1.28ex}\eta\hspace{-1.28ex}\eta}
   % bold eta

% Logic: formulas
\newcommand{\exc}{\exists} %constructive version, written without *
\newcommand{\lorc}{\lor}   %constructive version, written without *
\newcommand{\allnc}{\forall^{\mathsf{nc}}} %constructive, with no comp. content
\newcommand{\exnc}{\exists^{\mathsf{nc}}} %constructive, with no comp. content
\newcommand{\exca}{\exists^{\mathsf{ca}}} %classical, with arthmetic falsum
\newcommand{\excl}{\exists^{\mathsf{cl}}} %classical, with logical falsum
\newcommand{\lorcl}{\lor^{\mathsf{cl}}}
\newcommand{\falsum}{\bot}
\newcommand{\FV}{\mathsf{FV}}
\newcommand{\ltensor}{\otimes}
\newcommand{\truth}{\top}
\newcommand{\bigland}{\mathop{\hbox{$\bigwedge$\kern-.6em$\bigwedge$}}}
\newcommand{\biglor}{\mathop{\hbox{$\bigvee$\kern-.6em$\bigvee$}}}
\newcommand{\linto}{\multimap}
\newcommand{\passto}{\leadsto}
% \newcommand{\passto}{\rightsquigarrow}
\newcommand{\com}[1]{\bar{#1}}
\newcommand{\pass}[1]{\tilde{#1}}

% Logic: rules
\newcommand{\andI}{{\land}^{+}}
\newcommand{\andEzero}{{\land}^{-}_0}
\newcommand{\andEone}{{\land}^{-}_1}
\newcommand{\orcE}{\lorc^{-}}
\newcommand{\orcIzero}{\lorc^{+}_0}
\newcommand{\orcIone}{\lorc^{+}_1}
\newcommand{\orclE}{{\lorcl}^{-}}
\newcommand{\orclIzero}{{\lorcl}^{+}_0}
\newcommand{\orclIone}{{\lorcl}^{+}_1}
\newcommand{\allI}{{\forall}^{+}}
\newcommand{\allE}{{\forall}^{-}}
\newcommand{\allncI}{{\allnc}^{+}}
\newcommand{\allncE}{{\allnc}^{-}}
\newcommand{\excI}{{\exc}^{+}}
\newcommand{\excE}{{\exc}^{-}}
\newcommand{\exncI}{({\exnc})^{+}}
\newcommand{\exncE}{({\exnc})^{-}}
\newcommand{\exclI}{{\excl}^{+}}
\newcommand{\exclE}{{\excl}^{-}}
\newcommand{\impI}{{\to}^{+}}
\newcommand{\impE}{{\to}^{-}}
\newcommand{\ltensorI}{\ltensor^{+}}
\newcommand{\ltensorE}{\ltensor^{-}}
\newcommand{\falsumE}{\falsum^{-}}


% Logic: proof terms
\newcommand{\elim}[3]{(#1, #2.#3)}
\newcommand{\orcI}{{\lorc}\mathsf{I}}
\newcommand{\lamnc}{\lambda^{\mathsf{nc}}}

% Languages
\newcommand{\Fun}{\mathsf{Fun}}
\newcommand{\Rel}{\mathsf{Rel}}
\newcommand{\Ter}{\mathsf{Ter}}
\newcommand{\vars}{\mathsf{vars}}

% Lambda calculus
\newcommand{\cnv}{\mapsto}
\newcommand{\red}{\rightarrow}
\newcommand{\redl}{\leftarrow}
\newcommand{\redlstar}{\leftarrow^*}
\newcommand{\redlplus}{\leftarrow^+}
\newcommand{\redlr}{\leftrightarrow}
\newcommand{\redlrstar}{\overset{*}{\leftrightarrow}}
\newcommand{\redstar}{\rightarrow^*}
\newcommand{\redplus}{\rightarrow^+}
% \newcommand{\redstar}{\overset{*}{\rightarrow}}
% \newcommand{\redplus}{\overset{+}{\rightarrow}}
\newcommand{\sn}{\mathsf{sn}}
\newcommand{\SC}{\mathsf{SC}}
\newcommand{\SN}{\mathsf{SN}}
\newcommand{\Var}{\mathsf{Var}}

% Parallel reduction
\newcommand{\appmon}{\mathsf{appmon}}
\newcommand{\betapar}{\beta\mathsf{par}}
\newcommand{\etapar}{\eta\mathsf{par}}
\newcommand{\id}{\mathsf{id}}
\newcommand{\lambdamon}{\lambda\mathsf{mon}}
\newcommand{\redpar}{\rightarrow_{p}}

% Takahashi's Parallel reduction
\newcommand{\betatak}{\beta\mathsf{Tak}}
\newcommand{\redtak}{\rightarrow_{T}}

% Combinatory logic
\newcommand{\CL}{\textbf{CL}}
\newcommand{\cnvw}{\mapsto_{\mathsf{w}}}
\newcommand{\redstarw}{\rightarrow^*_{\mathsf{w}}}

% Sets
\newcommand{\es}{\varnothing}% the empty set
\newcommand{\set}[2]{\{\,#1\mid#2\,\}}

% Lists
\newcommand{\ls}[2]{[\,#1\mid #2\,]}

% Derivation symbols
\newcommand{\vdashm}{\vdash_{\mathrm{m}}}% derivability in minimal logic
\newcommand{\vdashi}{\vdash_{\mathrm{i}}}% derivability in intuitionistic logic
\newcommand{\vdashc}{\vdash_{\mathrm{c}}}% derivability in classical logic

% Systems
\newcommand{\MPC}{\textbf{Mp}}% minimal propositional logic
\newcommand{\IPC}{\textbf{Ip}}% intuitionistic propositional logic
\newcommand{\CPC}{\textbf{Cp}}% classical propositional logic
\newcommand{\MQC}{\textbf{M}}% minimal logic
\newcommand{\IQC}{\textbf{I}}% intuitionistic logic
\newcommand{\CQC}{\textbf{C}}% classical logic
\newcommand{\IQCE}{\textbf{Ie}}% int.logic with E-predicate
\newcommand{\lamto}{\lambf_{\to}}
\newcommand{\lametato}{\lambf\etabf_{\to}}
\newcommand{\HA}{\textbf{HA}}% Heyting arithmetic
\newcommand{\LHA}{\textbf{LHA}}% Linear Heyting arithmetic
\newcommand{\LT}{\textbf{LT}}% Linear Goedel T
\newcommand{\T}{\textbf{T}}% Goedel T

% Combinations for designating several systems at once
\newcommand{\mic}{\mathrm{[}\textbf{mic}\mathrm{]}}
\newcommand{\mi}{\mathrm{[}\textbf{mi}\mathrm{]}}
\newcommand{\ic}{\mathrm{[}\textbf{ic}\mathrm{]}}

% de Bruijn indices
\newcommand{\Abs}{\mathsf{Abs}}
\newcommand{\Term}{\mathsf{Term}}
\newcommand{\TERM}{textsc{Term}}
\newcommand{\abs}{\mathsf{abs}}
\newcommand{\app}{\mathsf{app}}

% Indexing
\renewcommand{\glossary}{\index}
\newcommand{\indexentry}[1]{\emph{#1}\index{#1}}
\newcommand{\mylabel}[1]{\label{#1}}
% \newcommand{\mylabel}[1]{\label{#1}\marginpar{\tiny #1}}

% Pattern unification and search
\newcommand{\unif}[3]{\mathsf{unif}(#1, #2 = #3)}
\newcommand{\unifalg}[1]{\Longrightarrow_{#1}}
\newcommand{\unifprefixalg}[1]{\longrightarrow_{#1}}

% Sequents
\newcommand{\seqarrow}{\Rightarrow}

% SFAs
\newcommand{\leaf}{\mathsf{Leaf}}
\newcommand{\tree}{\mathsf{tree}}
\newcommand{\branch}{\mathsf{Branch}}
\newcommand{\tlist}{\mathsf{tlist}}
\newcommand{\tcons}{\mathsf{Tcons}}
\newcommand{\constr}{\mathsf{constr}}
\newcommand{\rec}{\C{R}}
% \newcommand{\rec}{\mathsf{R}}
\newcommand{\Cases}{\C{C}}
% \newcommand{\Cases}{\mathsf{Cases}}
\newcommand{\ind}{\mathsf{Ind}}
% \newcommand{\closure}{\mathsf{Clos}}
% \newcommand{\mini}{\mathsf{Mini}}
\newcommand{\CasesAxiom}{\mathsf{Cases}}
\newcommand{\ST}{\delta}
\newcommand{\pair}[2]{\langle #1,#2\rangle}
\newcommand{\inj}{\mathsf{in}}
\newcommand{\bs}{\mathit{b}\!\mathit{s}}
% \newcommand{\bs}{\mathit{bs}}
\newcommand{\nil}{\mathsf{Nil}}
\newcommand{\cons}{\mathsf{Cons}}
\newcommand{\true}{\mathsf{t\kern-0.14em t}}
\newcommand{\false}{\mathsf{f\kern-0.14em f}}
\newcommand{\bottom}{\mathsf{b\kern-0.14em b}}
\newcommand{\suc}{\mathsf{S}}
\newcommand{\termUnit}{\mathsf{Dummy}}
% \newcommand{\termUnit}{\varepsilon}
\newcommand{\emp}{\mathsf{Empty}}
\newcommand{\termBoolElim}{\typeBool^-}%
\newcommand{\termTensorIntro}{\typeTensor^+}
\newcommand{\termTensorElim}{\typeTensor^-}
\newcommand{\termProdIntro}{\typeProd^+}
\newcommand{\termProdElimLeft}{\mathsf{Fst}}
\newcommand{\termProdElimRight}{\mathsf{Snd}}
\newcommand{\termSumIntroLeft}{\mathsf{Inl}}
\newcommand{\termSumIntroRight}{\mathsf{Inr}}
\newcommand{\termSumElim}{\typeSum^-}
\newcommand{\eqrel}[2]{{=}(#1,#2)}

% Types
\newcommand{\types}{\mathsf{T}}
\newcommand{\constrtypes}{\mathsf{KT}}
\newcommand{\bang}{\square}
\newcommand{\typeD}{\diamond}
% \newcommand{\typeN}{\mathsf{nat}}
\newcommand{\typeN}{\mathbf{N}}
\newcommand{\typeW}{\mathbf{W}}
\newcommand{\typeBin}{\mathbf{Bin}}
% \newcommand{\typeBool}{\mathsf{boole}}
\newcommand{\typeBool}{\mathbf{B}}
% \newcommand{\typeUnit}{\mathsf{unit}}
\newcommand{\typeUnit}{\mathbf{U}}
\newcommand{\typeTo}{\to}
\newcommand{\typeLinTo}{\multimap}
% \newcommand{\typeLinTo}{\to}
\newcommand{\typeTensor}{\otimes}
\newcommand{\typeProd}{\times}
\newcommand{\typeSum}{+}
% \newcommand{\typeL}[1]{\mathsf{list}(#1)}
\newcommand{\typeL}[1]{\mathbf{L}(#1)}

% Arithmetic
\newcommand{\0}{\mathsf{0}}
\newcommand{\one}{\mathsf{1}}
\newcommand{\n}{\mathbf{n}}
\newcommand{\s}{\mathsf{S}}
\newcommand{\p}{\mathsf{P}}
\newcommand{\caseconst}{\mathsf{case}}
\newcommand{\bincaseconst}{\B{d}}
\newcommand{\caseBooleConst}{\mathsf{if}}
\newcommand{\caseListConst}{\B{c}}
\newcommand{\dotminus}{\mathbin{{{-\mkern -9.5mu%
\mathchoice{\raise 2pt\hbox{$\cdot$}\mkern6mu}%
{\raise 2pt\hbox{$\cdot$}\mkern6mu}%
{\raise 1.5pt\hbox{$\scriptstyle\cdot$}\mkern4mu}%
{\raise 1pt\hbox{$\scriptscriptstyle\cdot$}\mkern4mu}}}}}

% Contexts
\newcommand{\termContextA}{\Gamma}
\newcommand{\HAcontextA}{\Pi}
\newcommand{\HAcontextB}{\Gamma}
\newcommand{\emptycontext}{\cdot}

% Typing judgements
\newcommand{\typed}[3]{{#1}\vdash{#2} \colon {#3}}
% \newcommand{\typed}[3]{{#1}\vdash{#2}^{#3}}
\newcommand{\splittyped}[4]{{#1}\mid{#2} \vdash {#3}\colon {#4}}
\newcommand{\trisplittyped}[5]{{#1}\mid{#2}\mid{#3} \vdash {#4}\colon {#5}}
\newcommand{\quadsplittyped}[6]{{#1}\mid{#2}\mid{#3}\mid{#4} \vdash 
{#5}\colon {#6}}
\newcommand{\HAtyped}[4]{{#1}\mid{#2} \vdash {#3}\colon {#4}}

% Axioms and rules
\newcommand{\variable}{\mathrm{Variable}}
\newcommand{\constant}{\mathrm{Constant}}
\newcommand{\axiom}{\mathrm{Axiom}}
\newcommand{\assumption}{\mathrm{Assumption}}
\newcommand{\typeTensorInd}{\typeTensor\mathrm{-Ind}}
\newcommand{\typeBoolInd}{\typeBool\mathrm{-Ind}}
\newcommand{\typeLrhoInd}{\typeL{\rho}\mathrm{-Ind}}
\newcommand{\typeLtauInd}{\typeL{\tau}\mathrm{-Ind}}
\newcommand{\typeLrhoStrongInd}{\typeL{\rho}\mathrm{-Ind}^+}
\newcommand{\typeLtauStrongInd}{\typeL{\tau}\mathrm{-Ind}^+}
\newcommand{\typeNInd}{\typeN\mathrm{-Ind}}
% \newcommand{\typeNStrongInd}{\typeN\mathrm{-PRInd}}
\newcommand{\typeNStrongInd}{\typeN\mathrm{-Ind}^+}
\newcommand{\contraction}{\mathrm{Contraction}}
\newcommand{\weakening}{\mathrm{Weakening}}
\newcommand{\passification}{\mathrm{Passification}}
\newcommand{\activation}{\mathrm{Activation}}
\newcommand{\completion}{\mathrm{Completion}}
\newcommand{\Neg}{\mathrm{Neg}}
\newcommand\VarBed{\hbox{\mathsf{VarCond}}}

% Derivation terms
\newcommand{\HAitA}[1]{\left\{{#1}\right\}}

% Functions and relations for examples
\newcommand{\ins}{\mathsf{ins}}
\newcommand{\sort}{\mathsf{sort}}
\newcommand{\Add}{\mathsf{Add}}
\newcommand{\Dup}{\mathsf{Dup}}
\newcommand{\Sort}{\mathsf{Sort}}
\newcommand{\Ins}{\mathsf{Ins}}

% Extraction
\newcommand{\extrTy}[1]{\tau(#1)}
\newcommand{\extrTer}[1]{\lbrack\!\lbrack#1\rbrack\!\rbrack}
\newcommand{\Uvar}[1]{x_{#1}}    %object var assigned to assumption var
\newcommand{\comUvar}[1]{\com{x}_{#1}}  %object var assigned to assumption var
\newcommand{\nulltype}{\varepsilon}

% Warshall algorithm
\newcommand{\emptyls}{\epsilon}
\newcommand{\con}[2]{#1 :: #2}
\newcommand{\consnil}[1]{#1{:}}
\newcommand{\elem}[2]{#1 \in #2}
\newcommand{\Rf}[1]{\mathsf{Rf}(#1)}
\newcommand{\concat}[2]{#1 \mid #2}

% Cleaning
\newcommand{\iso}{\varphi}            %\iso : rho -> clean(rho)  Isomorphism
\newcommand{\inviso}{\tilde{\varphi}} %and its inverse
\newcommand{\collapse}[1]{\mathrm{c}_{#1}}
\newcommand{\extend}[1]{\mathrm{e}_{#1}}

% Inductively generated predicates
\newcommand{\clauses}{\mathsf{KF}}
\newcommand{\formulas}{\mathsf{F}}
\newcommand{\preds}{\mathsf{P}}
\newcommand{\Acc}{\mathsf{Acc}}
\newcommand{\Barid}{\mathsf{Bar}}
\newcommand{\Good}{\mathsf{Good}}
\newcommand{\Even}{\mathsf{Even}}
\newcommand{\Ev}{\mathsf{Ev}}
\newcommand{\Od}{\mathsf{Od}}
\newcommand{\Tree}{\mathsf{Tree}}
\newcommand{\Tlist}{\mathsf{Tlist}}
\newcommand{\TrCl}{\mathsf{TrCl}}
\newcommand{\algAcc}{\mathsf{algAcc}}

% Program extraction from classical logic
\newcommand{\Truthax}{\ax_{\mathsf{true}}}
\newcommand{\ax}{\mathsf{Ax}}
\newcommand{\derint}{\vdash_{\mathsf{int}}}
\newcommand{\Zth}{Z}
\newcommand{\Efqdummy}{\mathsf{dummy}}
\newcommand{\mrAAA}{\;\mathbf{r}_{\C{A}}\;}
\newcommand{\Fib}{G}
\newcommand{\ran}{\mathsf{ran}}
\newcommand{\Prog}{\mathsf{Prog}}
\newcommand{\cvind}{\mathrm{cvind}}
\newcommand{\ifthenelse}[3]{[\textbf{if}\; #1\; \textbf{then}\; #2\; \textbf{else}\; #3]}
% \newcommand{\ifthenelse}[3]{\textbf{if}\ #1\ \textbf{then}\ #2\ \textbf{else}\ #3}


% Miscellaneous
\newcommand{\acronym}[1]{textsc{#1}}
\newcommand{\atom}{\mathsf{atom}}
\newcommand{\App}{\mathsf{App}}
\newcommand{\BNFdef}{\mathtt{\; ::= \;}}
\newcommand{\BNFor}{\mid}
\newcommand{\booleneg}{\mathsf{Neg}}
\newcommand{\card}[1]{\#(#1)}
% \newcommand{\card}[1]{|#1|}
\newcommand{\clean}[1]{{#1}^{\mathit{c}}}
% \newcommand{\clean}[1]{\mathsf{clean}(#1)}
\newcommand{\Comp}{\textsc{Comp}}
\newcommand{\comp}{\mathsf{comp}}
\newcommand{\conItA}[1]{\left\{{#1}\right\}}
\newcommand{\defiff}{\;\;:\Longleftrightarrow\;\;}
\newcommand{\dep}[1]{\mathsf{dp}(#1)}% depth of a formula or prooftree
% \newcommand{\dep}[1]{|#1|}% depth of a formula or prooftree
\newcommand{\dom}{\mathsf{dom}}
\newcommand{\domain}[1]{\mathsf{D_{#1}}}
% \newcommand{\edom}{\mathsf{edom}}
\newcommand{\eps}{\varepsilon}
\newcommand{\EqCompat}{\mathsf{Eq}\hbox{-}\mathsf{Compat}}
\newcommand{\Efq}{\mathsf{Efq}}
\newcommand{\EfqLog}{\textsf{Efq-Log}}
\newcommand{\Eig}{\mathsf{Eig}}
\newcommand{\Elim}{\mathsf{Elim}}
% \newcommand{\even}{\mathsf{Even}}
\newcommand{\Evenodd}{\mathsf{EvenOdd}}
\newcommand{\Eq}{\mathsf{Eq}}
\newcommand{\EqI}{\mathsf{Eq}^{+}}
\newcommand{\EqE}{\mathsf{Eq}^{-}}
\newcommand{\FA}{\mathsf{FA}}
\newcommand{\fini}{{\vbox{\hrule\hbox{%  
\vrule height1.3ex\hskip0.8ex\vrule}\hrule}}}
\newcommand{\fix}{\mathsf{fix}}
\newcommand{\hfilll}{\hspace*{0cm plus 1filll}}
\newcommand{\If}{\mathsf{If}}
\newcommand{\imp}{\Rightarrow}
\newcommand{\Intro}{\mathsf{Intro}}
\newcommand{\inquotes}[1]{``#1''}
% \newcommand{\inquotes}[1]{"`#1"'} %german quotes
\newcommand{\iterate}{\mathit{I}}
\newcommand{\len}[1]{\mathsf{len}(#1)}
\newcommand{\lev}[1]{\mathsf{lev}(#1)}
\newcommand{\leafsize}[1]{\mathsf{ls}(#1)} %leaf size of a formula or prooftree
\newcommand{\listappend}{\mathbin{{:}{+}{:}}}
\newcommand{\listrev}{\mathsf{Rev}}
\newcommand{\mr}{\,\mathbf{r}\,}
\newcommand{\mrind}{\mathbf{r}}
% \newcommand{\mr}{\,\underline{\mathbf{r}}\,}
% \newcommand{\mr}{\,\underline{\mathbf{mr}}\,}
\newcommand{\next}{\mathsf{nxt}}
\newcommand{\nf}[1]{\mathsf{nf}(#1)}
\newcommand{\odd}{\mathsf{Odd}}
\newcommand{\pick}{\mathsf{pick}}
\newcommand{\polylen}[1]{\vartheta(#1)}
\newcommand{\pred}{\mathsf{P}}
\newcommand{\PV}{\mathsf{PV}}
\renewcommand{\qedsymbol}{{\ \fini\par}}
% \renewcommand{\qedsymbol}{{\ \vbox{\hrule\hbox{%
%    \vrule height1.3ex\hskip0.8ex\vrule}\hrule}}\par}
\newcommand{\rew}{\mathsf{rew}}
\newcommand{\rf}[3]{\mathsf{rf}(#1;#2;#3)}
\newcommand{\select}{\mathsf{sel}}
\newcommand{\Set}{\mathbb{S}}
\newcommand{\size}[1]{|#1|} %size of a prooftree or formula
% \newcommand{\size}[1]{\mathsf{s}(#1)} %size of a prooftree or formula
\newcommand{\Stab}{\mathsf{Stab}}
\newcommand{\subst}[3]{#1[#2:= #3]}
\newcommand{\substnarrow}[3]{#1[#2{:=}#3]}
\newcommand{\Tikk}{\Diamond}
\newcommand{\Total}{\mathsf{Total}}
\newcommand{\tval}[1]{v(#1)}
\newcommand{\typ}{\C{T}_{\to}}
\newcommand{\weight}[1]{w(#1)}% weight of a type
\newcommand{\ws}{\mathit{w}\!\mathit{s}}

\newenvironment{enumeratei}{\begin{enumerate}[\upshape (i)]}
                           {\end{enumerate}}
   % produces (i), (ii), etc,  Cross-reference with \eqref
\newenvironment{enumeratea}{\begin{enumerate}[\upshape (a)]}
                           {\end{enumerate}}
   % produces (a), (b), etc,  Cross-reference with \eqref
\endinput

%%% Local Variables: 
%%% mode: latex-math
%%% End: