--- /dev/null
+\newtheorem{Corol}{Corollary}
+\newtheorem{Prop}{Proposition}
+\newtheorem{Conjec}{Conjecture}
+\newtheorem{lemma}{Lemma}
+\newtheorem{Def}{Definition}
+\newtheorem{theorem}{Theorem}
+
+
+\newtheorem{definition}{Definition}
+\newtheorem{notation}{Notation}
+\newtheorem{proposition}{Proposition}
+\newtheorem{corollary}{Corollary}
+\newtheorem{remark}{Remark}
+\newtheorem{example}{Example}
+%\newtheorem{proof}{Proof}
+
+
+
+
+
+
+
+%{\theoremheaderfont{\normalfont\bfseries}
+%\theorembodyfont{\slshape}
+%\theoremsymbol{\ensuremath{\diamondsuit}}
+
+%\theoremseparator{:}
+
+
+\newcommand{\rel}[0]{\ensuremath{{\mathcal{R}}}}
+\newcommand{\Gall}[0]{\ensuremath{\mathcal{G}}}
+
+
+
+%%%%%%%%%% outils langages dédiés
+\newcommand{\harvey}[0]{\ensuremath{\textsf{haRVey}\xspace}}
+\newcommand{\barvey}[0]{\ensuremath{\textsf{barvey}\xspace}}
+\newcommand{\bamTorv}[0]{\ensuremath{\textsf{bam2rv}\xspace}}
+\newcommand{\rvqe}[0]{\ensuremath{\textsf{rvqe}\xspace}}
+\newcommand{\Why}[0]{\ensuremath{\textsf{Why}\xspace}}
+\newcommand{\Be}[0]{\textsf{B}\xspace}
+\newcommand{\Zed}[0]{\ensuremath{\textsf{Z}\xspace}}
+
+
+
+%%%%%%%%% Langages premier ordre
+\newcommand{\Lang}[0]{\ensuremath{{\cal L}}}
+\newcommand{\Sorts}[0]{\ensuremath{{\cal S}}}
+\newcommand{\Vars}[0]{\ensuremath{{\cal V}}}
+\newcommand{\Funcs}[0]{\ensuremath{{\cal F}}}
+\newcommand{\Preds}[0]{\ensuremath{{\cal P}}}
+\newcommand{\arite}[0]{\ensuremath{{\alpha}}}
+\newcommand{\sorte}[0]{\ensuremath{{\sigma}}}
+\newcommand{\tauTerm}[0]{\textit{$\tau$-terme}\xspace}
+\newcommand{\tauITerm}[1]{\textit{$\tau_{#1}$-term}\xspace}
+\newcommand{\atome}[0]{\textit{atome}\xspace}
+\newcommand{\fpoms}[0]{\textit{fpoms}\xspace}
+\newcommand{\VLibre}[1]{\Vars_{\textit{lib}}(#1)}
+\newcommand{\congruenceE}[0]{\ensuremath{{\cal E}}}
+\newcommand{\preInterpret}[1]{\ensuremath{[ #1 ]}}
+\newcommand{\preInterpretSSET}[1]{\preInterpret{#1}}
+\newcommand{\preInterpretBAES}[1]{I'(#1)}
+\newcommand{\preinterpret}[0]{\preInterpret{\,}}
+%\newcommand{\valuationX}[1]{\ensuremath{{\preInterpret{#1}}_{\rho}}}
+%\newcommand{\valuation}[0]{\valuationX{\,}}
+\newcommand{\valuationSSET}[1]{\valuation(#1)}
+\newcommand{\valuationBAES}[1]{\valuation'(#1)}
+\newcommand{\valuationX}[1]{\valuation(#1)}
+\newcommand{\valuation}[0]{\ensuremath{\rho}\xspace}
+\newcommand{\etat}[0]{\ensuremath{\rho}}
+\newcommand{\constt}[1]{\ensuremath{\textsf{#1}}}
+\newcommand{\termSet}[0]{t}
+
+%%%%%%%% SSET -> BAES
+\newcommand{\sset}[0]{\ensuremath{\mathit{SSET}}}
+\newcommand{\axCod}[0]{\ensuremath{\delta}}
+\newcommand{\mty}[0]{\ensuremath{\mathsf{mty}}}
+\newcommand{\ttrue}[0]{\ensuremath{\mathsf{tt}}}
+\newcommand{\tfalse}[0]{\ensuremath{\mathsf{ff}}}
+
+
+
+%%%%%%%%%%%% interprétation modeles
+\newcommand{\interpretI}[0]{\ensuremath{{\cal I}}\xspace}
+\newcommand{\classInterpret}[0]{\ensuremath{\mathbf{I}\xspace}}
+\newcommand{\ltrue}[0]{\ensuremath{\top}}
+\newcommand{\lfalse}[0]{\ensuremath{\bot}}
+\newcommand{\modele}[0]{\ensuremath{\Vdash}}
+\newcommand{\deduc}[0]{\vdash}
+
+\newcommand{\conseq}[0]{\ensuremath{\vDash}}
+\newcommand{\herbrandU}[0]{\ensuremath{\mathbbm{H}}\xspace}
+
+
+%%%%%%%%% réels entiers complexes
+\newcommand{\Nats}[0]{\ensuremath{\mathbb{N}}}
+\newcommand{\Z}[0]{\ensuremath{\mathbb{Z}}}
+\newcommand{\R}[0]{\ensuremath{\mathbb{R}}}
+\newcommand{\Bool}[0]{\ensuremath{\mathds{B}}}
+\newcommand{\StratSet}[0]{\ensuremath{\mathbb{S}}}
+
+%%%%%%%%% logique
+\newcommand{\impliq}[0]{\ensuremath{{\Rightarrow}}}
+\newcommand{\equival}[0]{\ensuremath{{\Leftrightarrow}}}
+
+
+%%%%%%%%%%%%%%% quantifs
+\newcommand{\sortedForall}[3]{\ensuremath{(\forall_{#1} #2\, . \, #3)}}
+\newcommand{\sortedExists}[3]{\ensuremath{(\exists_{#1} #2\, . \, #3)}}
+\newcommand{\sortedQ}[3]{\ensuremath{(Q_{#1} #2\, . \, #3)}}
+\newcommand{\Forall}[2]{\ensuremath{(\forall #1\, . \, #2)}}
+\newcommand{\qnnf}[0]{\ensuremath{_{\textit{nf}}}}
+\newcommand{\gq}{\ensuremath{\mathsf{gq}}}
+\newcommand{\gqe}{\ensuremath{\mathsf{gqe}}}
+\newcommand{\bdd}[1]{\textit{bdd}(#1)}
+
+
+%%%%%%%%%%%%% grammaire
+\newcommand{\regleSep}[0]{\mathtt{~\textbf{|}~}}
+\newcommand{\regleDeriv}[0]{\mathtt{::=}}
+
+%%%%%%%%%%%% Transformation de formules
+\newcommand{\transfo}[0]{\ensuremath{{\rightarrow}}}
+\newcommand{\negativeForm}[1]{\ensuremath{\textit{neg}({#1})}}
+\newcommand{\cnf}[1]{\ensuremath{\textit{cnf}({#1})}}
+\newcommand{\dnf}[1]{\ensuremath{\textit{dnf}({#1})}}
+\newcommand{\polar}[1]{\ensuremath{\textit{pol}(#1)}}
+
+%%%%%%%%%%%% Systèmes de transitions
+\newcommand{\statesVars}[0]{\ensuremath{X}}
+\newcommand{\statesSet}[0]{\ensuremath{{\Sigma}}}
+\newcommand{\initialAssertion}[0]{\ensuremath{I}}
+\newcommand{\transSymbol}[0]{\ensuremath{{\rightarrow}}}
+\newcommand{\transLabel}[0]{\ensuremath{{\textit{act}}}}
+\newcommand{\prodASync}[0]{\ensuremath{\otimes}}
+\newcommand{\prodSync}[0]{\ensuremath{\oplus}}
+
+\newcommand{\execTS}[1]{\ensuremath{[[ #1 ]]}}
+
+%%%%%%%%%%%%%%%% construction de formules
+\newcommand{\ite}[3]{\textit{ite}(#1,#2,#3)}
+\newcommand{\iteRV}[3]{\mathsf{ite}(#1,#2,#3)}
+\newcommand{\eqd}[0]{\ensuremath{=_{\textit{\small{def}}}}}
+\newcommand{\instruction}[1]{\xspace{\sf #1}\xspace}
+\newcommand{\ifB}[0]{\instruction{if~}}
+\newcommand{\thenB}[0]{\instruction{~then~}}
+\newcommand{\elseB}[0]{\instruction{~else~}}
+\newcommand{\skipB}[0]{\instruction{skip}}
+
+
+%%%%%%%%%%%%% symboles fonctionnels dans des théories
+\newcommand{\select}[2]{\ensuremath{\mathsf{rd}(#1,#2)}}
+\newcommand{\store}[3]{\ensuremath{\mathsf{wr}(#1,#2,#3)}}
+\newcommand{\InsO}[0]{\ensuremath{\mathsf{ins}}}
+\newcommand{\Ins}[2]{\ensuremath{\InsO(#1,#2)}}
+\newcommand{\enumO}[0]{\ensuremath{\mathsf{enum}}}
+\newcommand{\enum}[1]{\ensuremath{\enumO(#1)}}
+
+
+
+\newcommand{\PRE}[1]{\ensuremath{\langle #1 \rangle}}
+\newcommand{\PREB}[1]{\ensuremath{[ #1 ]}}
+\newcommand{\Pre}[2]{\ensuremath{\textit{Pre}_{#1}(#2)}}
+\newcommand{\pretilde}[0]{\ensuremath{\widetilde{\textit{pre}}}}
+\newcommand{\post}[0]{\ensuremath{\textit{post}}}
+\newcommand{\pretildeR}[0]{\ensuremath{\widetilde{\textrm{pre}}}}
+\newcommand{\postR}[0]{\ensuremath{\textrm{post}}}
+\newcommand{\Succ}[0]{\ensuremath{\textit{successeur}}}
+\newcommand{\Men}[0]{\ensuremath{\textit{meneur}}}
+\newcommand{\Gpre}[2]{\ensuremath{G_{#1}(#2)}}
+\newcommand{\Fpre}[2]{\ensuremath{F_{#1}(#2)}}
+\newcommand{\POST}[1]{\ensuremath{[ #1 ]^{o}}}
+\newcommand{\sem}[1]{\ensuremath{\textit{rel}_{#1}}}
+\newcommand{\quantToSubst}[0]{\ensuremath{\textit{q2s}}}
+
+
+\newcommand{\wpr}[0]{\ensuremath{\textit{wp}}\xspace}
+\newcommand{\wlp}[0]{\ensuremath{\textit{wlp}}\xspace}
+\newcommand{\weaklp}[2]{\ensuremath{\textit{wlp}_{#1}(#2)}\xspace}
+\newcommand{\weakp}[2]{\ensuremath{\textit{wp}_{#1}(#2)}\xspace}
+\newcommand{\prd}[2]{\ensuremath{\textit{prd}_{#1}({#2})}\xspace}
+
+%\newcommand{\true}[0]{\ensuremath{\textit{true}}}
+%%%%%%%%%%%%%%%%% inclusion de fichiers MCh
+\newcommand{\myInput}[1]{\begin{center}\begin{tabular}{l}\input{#1}\end{tabular}\end{center}}
+
+
+%%%%%%%%%%%%% algorithmes d'atteignabilité
+\newcommand{\Init}[0]{\ensuremath{\textit{Init}}\xspace}
+\newcommand{\Target}[0]{\ensuremath{\textit{Target}}\xspace}
+
+
+%%%%%%%%%%%%%%%% grammaire abstraite b
+\newcommand{\substs}[0]{\ensuremath{\textit{Substs}}}
+\newcommand{\choice}[0]{\ensuremath{[]}}
+\newcommand{\paral}[0]{\ensuremath{\mid\mid}}
+\newcommand{\card}[1]{\ensuremath{\textit{card}(#1)}}
+%\newcommand{\dom}[0]{\ensuremath{\textit{dom}}}
+
+
+%%%%%%%%%%%%%%%%%%%% A remplacer
+\newcommand{\fs}[1]{\ensuremath{\mathsf{#1}}}
+\newcommand{\sort}[1]{\mbox{\textsc{#1}}}
+\newcommand{\dropE}[0]{\ensuremath{\mathsf{dropExistential}}}
+\newcommand{\renameF}[0]{\ensuremath{\mathsf{renameFormula}}}
+\newcommand{\ppnf}[0]{\ensuremath{\mathsf{de}}}
+\newcommand{\apnx}[0]{\ensuremath{\mathsf{mini}}}
+\newcommand{\apnxq}[0]{\ensuremath{\mathsf{m}_q}}
+\newcommand{\sqs}[0]{\ensuremath{\mathsf{rf}}}
+\newcommand{\theoryT}[0]{\ensuremath{{\cal T}}}
+\newcommand{\theoryU}[0]{\ensuremath{{\cal T}}}
+\newcommand{\vars}[0]{\ensuremath{\mathcal{V}}}
+%\newcommand{\Vlib}{\mathcal V}
+
+%%%%%%%%%%%%%%%%% Abstraction
+\newcommand{\latice}[0]{\ensuremath{\textit{exp}^{A}}}
+\newcommand{\laticeB}[0]{\ensuremath{\latice(B_1,\ldots,B_l)}}
+\newcommand{\concretisation}[0]{\ensuremath{\gamma}}
+\newcommand{\abstraction}[0]{\ensuremath{\alpha}}
+
+
+%%%%%%%% SFUNC -> BAES
+%\newcommand{\dres}[0]{\mathbin{AMSa}{"43}}
+%\newcommand{\bdres}[0]{\mathrel{\ooalign{$\dres$\hfil\cr$\mkern5mu$\hbox{$-$}}}}
+\newcommand{\sfunc}[0]{\ensuremath{\textit{SFUNC}}}
+\newcommand{\override}[2]{\ensuremath{#1 \bdres #2 }}
+\newcommand{\Partition}[1]{\ensuremath{\mathbbm{P}}(#1)}
+\newcommand{\fc}[1]{\ensuremath{\widetilde{#1}}} %fresh constant
+\newcommand{\nul}[0]{\ensuremath{\mathsf{null}}} %fresh constant
+\newcommand{\overR}[3]{\ensuremath {\mathsf{over}(#1,#2,#3)}}
+\newcommand{\image}[2]{\ensuremath {\sf{image}(#1,#2)}}
+
+
+%\input{bmacro}
+
+%%%%%%%%%%%%%%%%%%%%%%%%%% sortes à supprimer
+\newcommand{\ind}[0]{\textit{index}}
+\newcommand{\val}[0]{\textit{val}}
+%\newcommand{\func}[0]{\ensuremath{\textit{F}\xspace}}
+\newcommand{\arr}[0]{\textit{array}}
+%\newcommand{\other}[0]{\ensuremath{\textit{other}\xspace}}
+\newcommand{\iSet}[0]{\ensuremath{\textit{S}_{i}}\xspace}
+\newcommand{\eSet}[0]{\ensuremath{\textit{S}_{e}}\xspace}
+\newcommand{\ARR}[0]{\textit{ARRAY}\xspace}
+\newcommand{\IND}[0]{\textit{INDEX}\xspace}
+\newcommand{\VAL}[0]{\textit{VALUE}\xspace}
+\newcommand{\constArr}{\ensuremath{\mathsf{const}}\xspace}
+%\newcommand{\block}{\ensuremath{\mathsf{block}}\xspace}
+\newcommand{\im}[0]{\ensuremath{\mathsf{im}}}
+
+
+%%%%%%%%%%%%%%%%%%%%%%%%%% multi-sorted languages
+\newcommand{\eJ}{\EuScript J}
+\newcommand{\eF}{\EuScript F}
+\newcommand{\eL}{\EuScript L}
+\newcommand{\eT}{\EuScript T}
+\newcommand{\eV}{\EuScript V}
+\newcommand{\eP}{\EuScript P}
+%\newcommand{\eC}{\EuScript C}
+%\newcommand{\eR}{\EuScript R}
+%\newcommand{\eI}{\EuScript I}
+\renewcommand{\le}{\leqslant}
+\renewcommand{\ge}{\geqslant}
+
+\newcommand{\any}[0]{\textrm{@}}
+
+\newcommand{\str}[0]{\textit{Strength}}
+
+
+%%%%%%%%%%%%%%%%%%%%%%%%
+\newcommand{\sortSet}{\mathcal{S}}
+\newcommand{\sortVars}{\mathcal{X}_s}
+\newcommand{\sortFunctionSet}{\mathcal{F}_s}
+\newcommand{\varSet}{\mathcal{X}}
+\newcommand{\functionSet}{\mathcal{F}}
+
+\def\unique{\sort{u}}
