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

\newcommand{\nb}[1]{{\color{violet} NB: #1}}

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

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

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

%\newtheorem{theorem}{Theorem}

\newtheorem{proposition}[theorem]{Proposition}

\newtheorem{conjecture}[theorem]{Conjecture}

\newtheorem{claim}[theorem]{Claim}

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

%

%

%\theoremstyle{definition}

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

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

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

\newcommand{\arith}{B}

\newcommand{\basic}{\mathit{BASIC}}

\newcommand{\RC}{RC}                                           % name for ramified classical logic

\newcommand{\RCi}{$\Sigma_i^{{N_0}}$-RC}

\newcommand{\safeRC}{$\Sigma^{{N_0}}$-RC}

\newcommand{\ind}{\mathit{IND}}

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

\newcommand{\cind}[1]{#1\text{-}\ind}

\newcommand{\cpind}[1]{#1\text{-}\pind}

\renewcommand{\min}{\mathit{MIN}}

\newcommand{\cmin}[1]{#1\text{-}\min}

\newcommand{\prefix}{\preccurlyeq}

\newcommand{\charfn}[2]{\chi^{#1}_{#2}}

\newcommand{\wit}[2]{\mathit{wit}^{#1}_{#2}}

\newcommand{\Wit}[2]{\mathit{Wit}^{#1}_{#2}}

\newcommand{\dfn}{:=}

\newcommand{\seqar}{\rightarrow}

\newcommand{\proves}{\vdash}

\renewcommand{\epsilon}{\varepsilon}

\newcommand{\pred}{p}

\renewcommand{\succ}[1]{s_{#1}}

\newcommand{\hlf}[1]{\lfloor \frac{#1}{2}\rfloor}

\newcommand{\cond}{C}

\newcommand{\smsh}{\#}

\newcommand{\pair}[3]{\langle ; #1,#2 , #3 \rangle}

\newcommand{\eq}{\textsc{eq}}

\newcommand{\leqfn}{\textsc{leq}}

\newcommand{\safe}{{N_0}}

\newcommand{\normal}{{N_1}}

\newcommand{\pv}{\mathit{PV}}

\newcommand{\pvbci}[1]{\pv^{#1}_{\mathrm{BC}}}

\newcommand{\mubci}[1]{\mu\mathrm{BC}^{#1}}

\newcommand{\mubc}{\mu\mathrm{BC}}

\newcommand{\bc}{\mathrm{BC}}

\newcommand{\sigp}[1]{\Sigma^p_{#1}}

\newcommand{\pip}[1]{\Pi^p_{#1}}

\newcommand{\fphi}[1]{\Box^p_{#1}}

\newcommand{\fph}{\Box^p}

	\newcommand{\ph}{\mathbf{PH}}

	\newcommand{\pspace}{\mathbf{PSPACE}}

	\newcommand{\fpspace}{\mathbf{FPSPACE}}

	\newcommand{\ptime}{\mathbf{P}}

	\newcommand{\fptime}{\mathbf{FP}}

	\newcommand{\nc}{\mathbf{NC}}

	\newcommand{\ac}{\mathbf{AC}}

	\newcommand{\exptime}{\mathbf{EXP}}

	\newcommand{\np}{\mathbf{NP}}

	\newcommand{\conp}{\mathbf{coNP}}

	\newcommand{\poly}{\mathrm{poly}}

\newcommand{\cnot}{\neg}

\newcommand{\cimp}{\supset}

\newcommand{\cor}{\vee}

\newcommand{\cand}{\wedge}

\newcommand{\ciff}{\equiv}

\newcommand{\size}[1]{|#1|}                        %% length of a word

%\newcommand{\mode}{\; \underline{\mbox{mod}}\;}   %% mod 2^{|x|}  %% replaced \mode by \modu because of command clash..

\newcommand{\modu}{\; \underline{\mbox{mod}}\;}   %% mod 2^{|x|}

%%%%% RULES %%%%%%

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

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

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

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

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

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

	\newcommand{\rais}{\mathit{raise}}

% theories

	\newcommand{\theory}{\mathcal T}

	\newcommand{\system}{\mathcal S}

	%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}