Laboratoire de l'Informatique et du Parallélisme » Linear Arithmetic

%\newtheorem{theorem}{Theorem}    %% Patrick: added for 'article' class version

%\newtheorem{maintheorem}[theorem]{Main Theorem}

%\newtheorem{observation}[theorem]{Observation}

%\newtheorem{corollary}[theorem]{Corollary}

%\newtheorem{lemma}[theorem]{Lemma}

\theoremstyle{plain}

\newtheorem{proposition}[theorem]{Proposition}

%\newtheorem{conjecture}[theorem]{Conjecture}

%

%\theoremstyle{definition}

%\newtheorem{definition}[theorem]{Definition}

%\newtheorem{example}[theorem]{Example}

%\newtheorem{notation}[theorem]{Notation}

%\newtheorem{convention}[theorem]{Convention}

%\newtheorem{remark}[theorem]{Remark}

%\newtheorem{discussion}[theorem]{Discussion}

\newcommand{\todo}[1]{{\color{red}{\textbf{Todo:} #1}}}

\newcommand{\anupam}[1]{{\color{orange}{\textbf{Anupam:} #1}}}

\newcommand{\patrick}[1]{{\color{blue}{\textbf{Patrick:} #1}}}

\newcommand{\IH}{\mathit{IH}}

\newcommand{\defined}{:=}

	\newcommand{\LL}{\it{LL}}

	\vllineartrue

	\newcommand{\FV}{\mathit{FV}}

	%specification

	\newcommand{\eqspec}{\mathcal E}

	\newcommand{\closure}[1]{\overline{#1}}

	\newcommand{\conv}{\mathit{Conv}}

	% theories

	\newcommand{\theory}{\mathcal T}

	\newcommand{\system}{\mathcal S}

	%terms

	\newcommand{\pred}{p}

	\newcommand{\cond}{C}

	\renewcommand{\succ}{\mathsf{s}}

	\renewcommand{\epsilon}{\varepsilon}

	% linear connectives

	\newcommand{\limp}{\multimap}

	\renewcommand{\land}{\otimes}

	\newcommand{\laand}{\&}

	\newcommand{\laor}{\oplus}

	\renewcommand{\lor}{\vlpa}

	\renewcommand{\lnot}[1]{{#1^{\perp}}}

	\newcommand{\lnotnot}[1]{#1^{\perp \perp}}

	% classical connectives

	\newcommand{\cimp}{\rightarrow}

	\newcommand{\cand}{\wedge}

	\newcommand{\cor}{\vee}

	\newcommand{\cnot}{\neg}

	\newcommand{\Ax}{\mathit{(Ax)}}

	\newcommand{\Rl}{\mathit{(Rl)}}

	\newcommand{\MELL}{\mathit{MELL}}

	\newcommand{\MEAL}{\mathit{MELLW}}

	\newcommand{\MELLW}{\mathit{MELL(W)}}

	\newcommand{\Aonetwo}{\mathcal{A}^1_2}

	\newcommand{\logic}{\mathit{L}_{\mathcal A} }

	% predicates

	\newcommand{\nat}{N}

	\newcommand{\word}{W}

	\newcommand{\Nat}{\mathbb{N}}

	\newcommand{\Word}{\mathbb{W}}

	%axioms

	\newcommand{\wk}{\mathit{wk}}

	\newcommand{\impl}{\cimp\text{-}\mathit{l}}

	\newcommand{\impcomm}{\mathit{com}}

	\newcommand{\conint}{\cand\text{-}\mathit{i}}

	\newcommand{\conel}{\cand\text{-}\mathit{e}}

	\newcommand{\negclass}{\cnot}

	%equality

	\newcommand{\refl}{\mathit{ref}}

	\newcommand{\symm}{\mathit{sym}}

	\newcommand{\trans}{\mathit{trans}}

	\newcommand{\subst}{\mathit{sub}}

	%rules

	\newcommand{\inv}[1]{#1\text{-inv}}

	\renewcommand{\mp}{\mathit{mp}}

	\newcommand{\gen}{\mathit{gen}}

	\newcommand{\inst}{\mathit{ins}}

	\newcommand{\id}{\it{id}}

	\newcommand{\cut}{\it{cut}}

	\newcommand{\multicut}{\it{mcut}}

	\newcommand{\indr}{\mathit{PIND}}

	\newcommand{\nec}{\mathit{nec}}

	\newcommand{\tax}{\mathit{T}}

	\newcommand{\four}{\mathit{4}}

	\newcommand{\kax}{\mathit{K}}

	\newcommand{\cntr}{\mathit{cntr}}

	\newcommand{\lefrul}[1]{#1\text{-}\mathit{l}}

	\newcommand{\rigrul}[1]{#1\text{-}\mathit{r}}

	%consequence relations

	\newcommand{\admits}{\vDash}

	\newcommand{\seqar}{\vdash}

	\newcommand{\proves}{\vdash_e}

	%induction

	\newcommand{\ind}{\mathit{PIND}}

	\newcommand{\pind}{\mathit{PIND}}

	\newcommand{\cax}[2]{#1\text{-}#2}

	\newcommand{\sigone}{\Sigma^{\word^+}_1 }

	\newcommand{\sigzer}{\Sigma^{\word^+}_0}

	\newcommand{\bharith}{\mathcal A^1_2}

	\newcommand{\arith}{I\sigone}

          % sizes

          \newcommand{\height}[1]{\mathit{h}(#1)}