<html><head><meta name="color-scheme" content="light dark"></head><body><pre style="word-wrap: break-word; white-space: pre-wrap;">\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 -&gt; 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 -&gt; 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}}
</pre></body></html>