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{lemma}[theorem]{Lemma}

\theoremstyle{definition}

\newtheorem{definition}[theorem]{Definition}

\newtheorem{example}[theorem]{Example}

\newtheorem{remark}[theorem]{Remark}

\newcommand{\lhs}{\mathit{LHS}}

\newcommand{\rhs}{\mathit{RHS}}

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

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

\newcommand{\arith}{B_2}

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

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

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

\newcommand{\lind}{\mathit{LIND}}

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

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

\newcommand{\clind}[1]{#1\text{-}\lind}

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

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

\newcommand{\prefix}{\preccurlyeq}

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

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

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

\newcommand{\dfn}{:=}

\newcommand{\seqar}{\rightarrow}

\newcommand{\proves}{\vdash}

\renewcommand{\epsilon}{\varepsilon}

\newcommand{\pred}{\mathsf{p}}

\renewcommand{\succ}[1]{\mathsf{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{\bit}{\textsc{bit}}

\newcommand{\andfn}{\textsc{and}}

\newcommand{\orfn}{\textsc{or}}

\newcommand{\notfn}{\textsc{not}}

\newcommand{\equivfn}{\textsc{equiv}}

\newcommand{\shorten}{\textsc{shorten}}

\newcommand{\moins}{-}

\newcommand{\zerobit}{\textsc{0bit}}

\newcommand{\onebit}{\textsc{1bit}}

\newcommand{\pref}{\textsc{pref}}

\newcommand{\addtosequence}{\textsc{addtosequ}}

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

\newcommand{\mode}{\ \underline{\mathrm{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}}

	\newcommand{\LK}{\mathit{LK}}

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