symbols/macroE.tex

   1 \newtheorem{Corol}{Corollary}
   2 \newtheorem{Prop}{Proposition}
   3 \newtheorem{Conjec}{Conjecture}
   4 \newtheorem{lemma}{Lemma}
   5 \newtheorem{Def}{Definition}
   6 \newtheorem{theorem}{Theorem}
   7
   8
   9 \newtheorem{definition}{Definition}
  10 \newtheorem{notation}{Notation}
  11 \newtheorem{proposition}{Proposition}
  12 \newtheorem{corollary}{Corollary}
  13 \newtheorem{remark}{Remark}
  14 \newtheorem{example}{Example}
  15 %\newtheorem{proof}{Proof}
  16
  17
  18
  19
  20
  21
  22
  23 %{\theoremheaderfont{\normalfont\bfseries}
  24 %\theorembodyfont{\slshape}
  25 %\theoremsymbol{\ensuremath{\diamondsuit}}
  26
  27 %\theoremseparator{:}
  28
  29
  30 \newcommand{\rel}[0]{\ensuremath{{\mathcal{R}}}}
  31 \newcommand{\Gall}[0]{\ensuremath{\mathcal{G}}}
  32
  33
  34
  35 %%%%%%%%%% outils langages dédiés
  36 \newcommand{\harvey}[0]{\ensuremath{\textsf{haRVey}\xspace}}
  37 \newcommand{\barvey}[0]{\ensuremath{\textsf{barvey}\xspace}}
  38 \newcommand{\bamTorv}[0]{\ensuremath{\textsf{bam2rv}\xspace}}
  39 \newcommand{\rvqe}[0]{\ensuremath{\textsf{rvqe}\xspace}}
  40 \newcommand{\Why}[0]{\ensuremath{\textsf{Why}\xspace}}
  41 \newcommand{\Be}[0]{\textsf{B}\xspace}
  42 \newcommand{\Zed}[0]{\ensuremath{\textsf{Z}\xspace}}
  43
  44
  45
  46 %%%%%%%%% Langages premier ordre
  47 \newcommand{\Lang}[0]{\ensuremath{{\cal L}}}
  48 \newcommand{\Sorts}[0]{\ensuremath{{\cal S}}}
  49 \newcommand{\Vars}[0]{\ensuremath{{\cal V}}}
  50 \newcommand{\Funcs}[0]{\ensuremath{{\cal F}}}
  51 \newcommand{\Preds}[0]{\ensuremath{{\cal P}}}
  52 \newcommand{\arite}[0]{\ensuremath{{\alpha}}}
  53 \newcommand{\sorte}[0]{\ensuremath{{\sigma}}}
  54 \newcommand{\tauTerm}[0]{\textit{$\tau$-terme}\xspace}
  55 \newcommand{\tauITerm}[1]{\textit{$\tau_{#1}$-term}\xspace}
  56 \newcommand{\atome}[0]{\textit{atome}\xspace}
  57 \newcommand{\fpoms}[0]{\textit{fpoms}\xspace}
  58 \newcommand{\VLibre}[1]{\Vars_{\textit{lib}}(#1)}
  59 \newcommand{\congruenceE}[0]{\ensuremath{{\cal E}}}
  60 \newcommand{\preInterpret}[1]{\ensuremath{[ #1 ]}}
  61 \newcommand{\preInterpretSSET}[1]{\preInterpret{#1}}
  62 \newcommand{\preInterpretBAES}[1]{I'(#1)}
  63 \newcommand{\preinterpret}[0]{\preInterpret{\,}}
  64 %\newcommand{\valuationX}[1]{\ensuremath{{\preInterpret{#1}}_{\rho}}}
  65 %\newcommand{\valuation}[0]{\valuationX{\,}}
  66 \newcommand{\valuationSSET}[1]{\valuation(#1)}
  67 \newcommand{\valuationBAES}[1]{\valuation'(#1)}
  68 \newcommand{\valuationX}[1]{\valuation(#1)}
  69 \newcommand{\valuation}[0]{\ensuremath{\rho}\xspace}
  70 \newcommand{\etat}[0]{\ensuremath{\rho}}
  71 \newcommand{\constt}[1]{\ensuremath{\textsf{#1}}}
  72 \newcommand{\termSet}[0]{t}
  73
  74 %%%%%%%% SSET -> BAES
  75 \newcommand{\sset}[0]{\ensuremath{\mathit{SSET}}}
  76 \newcommand{\axCod}[0]{\ensuremath{\delta}}
  77 \newcommand{\mty}[0]{\ensuremath{\mathsf{mty}}}
  78 \newcommand{\ttrue}[0]{\ensuremath{\mathsf{tt}}}
  79 \newcommand{\tfalse}[0]{\ensuremath{\mathsf{ff}}}
  80
  81
  82
  83 %%%%%%%%%%%% interprétation modeles
  84 \newcommand{\interpretI}[0]{\ensuremath{{\cal I}}\xspace}
  85 \newcommand{\classInterpret}[0]{\ensuremath{\mathbf{I}\xspace}}
  86 \newcommand{\ltrue}[0]{\ensuremath{\top}}
  87 \newcommand{\lfalse}[0]{\ensuremath{\bot}}
  88 \newcommand{\modele}[0]{\ensuremath{\Vdash}}
  89 \newcommand{\deduc}[0]{\vdash}
  90
  91 \newcommand{\conseq}[0]{\ensuremath{\vDash}}
  92 \newcommand{\herbrandU}[0]{\ensuremath{\mathbbm{H}}\xspace}
  93
  94
  95 %%%%%%%%% réels entiers complexes
  96 \newcommand{\Nats}[0]{\ensuremath{\mathbb{N}}}
  97 \newcommand{\Z}[0]{\ensuremath{\mathbb{Z}}}
  98 \newcommand{\R}[0]{\ensuremath{\mathbb{R}}}
  99 \newcommand{\Bool}[0]{\ensuremath{\mathds{B}}}
 100 \newcommand{\StratSet}[0]{\ensuremath{\mathbb{S}}}
 101
 102 %%%%%%%%% logique
 103 \newcommand{\impliq}[0]{\ensuremath{{\Rightarrow}}}
 104 \newcommand{\equival}[0]{\ensuremath{{\Leftrightarrow}}}
 105
 106
 107 %%%%%%%%%%%%%%% quantifs
 108 \newcommand{\sortedForall}[3]{\ensuremath{(\forall_{#1} #2\, . \, #3)}}
 109 \newcommand{\sortedExists}[3]{\ensuremath{(\exists_{#1} #2\, . \, #3)}}
 110 \newcommand{\sortedQ}[3]{\ensuremath{(Q_{#1} #2\, . \, #3)}}
 111 \newcommand{\Forall}[2]{\ensuremath{(\forall #1\, . \, #2)}}
 112 \newcommand{\qnnf}[0]{\ensuremath{_{\textit{nf}}}}
 113 \newcommand{\gq}{\ensuremath{\mathsf{gq}}}
 114 \newcommand{\gqe}{\ensuremath{\mathsf{gqe}}}
 115 \newcommand{\bdd}[1]{\textit{bdd}(#1)}
 116
 117
 118 %%%%%%%%%%%%% grammaire
 119 \newcommand{\regleSep}[0]{\mathtt{~\textbf{|}~}}
 120 \newcommand{\regleDeriv}[0]{\mathtt{::=}}
 121
 122 %%%%%%%%%%%% Transformation de formules
 123 \newcommand{\transfo}[0]{\ensuremath{{\rightarrow}}}
 124 \newcommand{\negativeForm}[1]{\ensuremath{\textit{neg}({#1})}}
 125 \newcommand{\cnf}[1]{\ensuremath{\textit{cnf}({#1})}}
 126 \newcommand{\dnf}[1]{\ensuremath{\textit{dnf}({#1})}}
 127 \newcommand{\polar}[1]{\ensuremath{\textit{pol}(#1)}}
 128
 129 %%%%%%%%%%%% Systèmes de transitions
 130 \newcommand{\statesVars}[0]{\ensuremath{X}}
 131 \newcommand{\statesSet}[0]{\ensuremath{{\Sigma}}}
 132 \newcommand{\initialAssertion}[0]{\ensuremath{I}}
 133 \newcommand{\transSymbol}[0]{\ensuremath{{\rightarrow}}}
 134 \newcommand{\transLabel}[0]{\ensuremath{{\textit{act}}}}
 135 \newcommand{\prodASync}[0]{\ensuremath{\otimes}}
 136 \newcommand{\prodSync}[0]{\ensuremath{\oplus}}
 137
 138 \newcommand{\execTS}[1]{\ensuremath{[[ #1 ]]}}
 139
 140 %%%%%%%%%%%%%%%% construction de formules
 141 \newcommand{\ite}[3]{\textit{ite}(#1,#2,#3)}
 142 \newcommand{\iteRV}[3]{\mathsf{ite}(#1,#2,#3)}
 143 \newcommand{\eqd}[0]{\ensuremath{=_{\textit{\small{def}}}}}
 144 \newcommand{\instruction}[1]{\xspace{\sf #1}\xspace}
 145 \newcommand{\ifB}[0]{\instruction{if~}}
 146 \newcommand{\thenB}[0]{\instruction{~then~}}
 147 \newcommand{\elseB}[0]{\instruction{~else~}}
 148 \newcommand{\skipB}[0]{\instruction{skip}}
 149
 150
 151 %%%%%%%%%%%%% symboles fonctionnels dans des théories
 152 \newcommand{\select}[2]{\ensuremath{\mathsf{rd}(#1,#2)}}
 153 \newcommand{\store}[3]{\ensuremath{\mathsf{wr}(#1,#2,#3)}}
 154 \newcommand{\InsO}[0]{\ensuremath{\mathsf{ins}}}
 155 \newcommand{\Ins}[2]{\ensuremath{\InsO(#1,#2)}}
 156 \newcommand{\enumO}[0]{\ensuremath{\mathsf{enum}}}
 157 \newcommand{\enum}[1]{\ensuremath{\enumO(#1)}}
 158
 159
 160
 161 \newcommand{\PRE}[1]{\ensuremath{\langle #1 \rangle}}
 162 \newcommand{\PREB}[1]{\ensuremath{[ #1 ]}}
 163 \newcommand{\Pre}[2]{\ensuremath{\textit{Pre}_{#1}(#2)}}
 164 \newcommand{\pretilde}[0]{\ensuremath{\widetilde{\textit{pre}}}}
 165 \newcommand{\post}[0]{\ensuremath{\textit{post}}}
 166 \newcommand{\pretildeR}[0]{\ensuremath{\widetilde{\textrm{pre}}}}
 167 \newcommand{\postR}[0]{\ensuremath{\textrm{post}}}
 168 \newcommand{\Succ}[0]{\ensuremath{\textit{successeur}}}
 169 \newcommand{\Men}[0]{\ensuremath{\textit{meneur}}}
 170 \newcommand{\Gpre}[2]{\ensuremath{G_{#1}(#2)}}
 171 \newcommand{\Fpre}[2]{\ensuremath{F_{#1}(#2)}}
 172 \newcommand{\POST}[1]{\ensuremath{[ #1 ]^{o}}}
 173 \newcommand{\sem}[1]{\ensuremath{\textit{rel}_{#1}}}
 174 \newcommand{\quantToSubst}[0]{\ensuremath{\textit{q2s}}}
 175
 176
 177 \newcommand{\wpr}[0]{\ensuremath{\textit{wp}}\xspace}
 178 \newcommand{\wlp}[0]{\ensuremath{\textit{wlp}}\xspace}
 179 \newcommand{\weaklp}[2]{\ensuremath{\textit{wlp}_{#1}(#2)}\xspace}
 180 \newcommand{\weakp}[2]{\ensuremath{\textit{wp}_{#1}(#2)}\xspace}
 181 \newcommand{\prd}[2]{\ensuremath{\textit{prd}_{#1}({#2})}\xspace}
 182
 183 %\newcommand{\true}[0]{\ensuremath{\textit{true}}}
 184 %%%%%%%%%%%%%%%%% inclusion de fichiers MCh
 185 \newcommand{\myInput}[1]{\begin{center}\begin{tabular}{l}\input{#1}\end{tabular}\end{center}}
 186
 187
 188 %%%%%%%%%%%%% algorithmes d'atteignabilité
 189 \newcommand{\Init}[0]{\ensuremath{\textit{Init}}\xspace}
 190 \newcommand{\Target}[0]{\ensuremath{\textit{Target}}\xspace}
 191
 192
 193 %%%%%%%%%%%%%%%% grammaire abstraite b
 194 \newcommand{\substs}[0]{\ensuremath{\textit{Substs}}}
 195 \newcommand{\choice}[0]{\ensuremath{[]}}
 196 \newcommand{\paral}[0]{\ensuremath{\mid\mid}}
 197 \newcommand{\card}[1]{\ensuremath{\textit{card}(#1)}}
 198 %\newcommand{\dom}[0]{\ensuremath{\textit{dom}}}
 199
 200
 201 %%%%%%%%%%%%%%%%%%%% A remplacer
 202 \newcommand{\fs}[1]{\ensuremath{\mathsf{#1}}}
 203 \newcommand{\sort}[1]{\mbox{\textsc{#1}}}
 204 \newcommand{\dropE}[0]{\ensuremath{\mathsf{dropExistential}}}
 205 \newcommand{\renameF}[0]{\ensuremath{\mathsf{renameFormula}}}
 206 \newcommand{\ppnf}[0]{\ensuremath{\mathsf{de}}}
 207 \newcommand{\apnx}[0]{\ensuremath{\mathsf{mini}}}
 208 \newcommand{\apnxq}[0]{\ensuremath{\mathsf{m}_q}}
 209 \newcommand{\sqs}[0]{\ensuremath{\mathsf{rf}}}
 210 \newcommand{\theoryT}[0]{\ensuremath{{\cal T}}}
 211 \newcommand{\theoryU}[0]{\ensuremath{{\cal T}}}
 212 \newcommand{\vars}[0]{\ensuremath{\mathcal{V}}}
 213 %\newcommand{\Vlib}{\mathcal V}
 214
 215 %%%%%%%%%%%%%%%%% Abstraction
 216 \newcommand{\latice}[0]{\ensuremath{\textit{exp}^{A}}}
 217 \newcommand{\laticeB}[0]{\ensuremath{\latice(B_1,\ldots,B_l)}}
 218 \newcommand{\concretisation}[0]{\ensuremath{\gamma}}
 219 \newcommand{\abstraction}[0]{\ensuremath{\alpha}}
 220
 221
 222 %%%%%%%% SFUNC -> BAES
 223 %\newcommand{\dres}[0]{\mathbin{AMSa}{"43}}
 224 %\newcommand{\bdres}[0]{\mathrel{\ooalign{$\dres$\hfil\cr$\mkern5mu$\hbox{$-$}}}}
 225 \newcommand{\sfunc}[0]{\ensuremath{\textit{SFUNC}}}
 226 \newcommand{\override}[2]{\ensuremath{#1 \bdres #2 }}
 227 \newcommand{\Partition}[1]{\ensuremath{\mathbbm{P}}(#1)}
 228 \newcommand{\fc}[1]{\ensuremath{\widetilde{#1}}} %fresh constant
 229 \newcommand{\nul}[0]{\ensuremath{\mathsf{null}}} %fresh constant
 230 \newcommand{\overR}[3]{\ensuremath {\mathsf{over}(#1,#2,#3)}}
 231 \newcommand{\image}[2]{\ensuremath {\sf{image}(#1,#2)}}
 232
 233
 234 %\input{bmacro}
 235
 236 %%%%%%%%%%%%%%%%%%%%%%%%%% sortes à supprimer
 237 \newcommand{\ind}[0]{\textit{index}}
 238 \newcommand{\val}[0]{\textit{val}}
 239 %\newcommand{\func}[0]{\ensuremath{\textit{F}\xspace}}
 240 \newcommand{\arr}[0]{\textit{array}}
 241 %\newcommand{\other}[0]{\ensuremath{\textit{other}\xspace}}
 242 \newcommand{\iSet}[0]{\ensuremath{\textit{S}_{i}}\xspace}
 243 \newcommand{\eSet}[0]{\ensuremath{\textit{S}_{e}}\xspace}
 244 \newcommand{\ARR}[0]{\textit{ARRAY}\xspace}
 245 \newcommand{\IND}[0]{\textit{INDEX}\xspace}
 246 \newcommand{\VAL}[0]{\textit{VALUE}\xspace}
 247 \newcommand{\constArr}{\ensuremath{\mathsf{const}}\xspace}
 248 %\newcommand{\block}{\ensuremath{\mathsf{block}}\xspace}
 249 \newcommand{\im}[0]{\ensuremath{\mathsf{im}}}
 250
 251
 252 %%%%%%%%%%%%%%%%%%%%%%%%%% multi-sorted languages
 253 \newcommand{\eJ}{\EuScript J}
 254 \newcommand{\eF}{\EuScript F}
 255 \newcommand{\eL}{\EuScript L}
 256 \newcommand{\eT}{\EuScript T}
 257 \newcommand{\eV}{\EuScript V}
 258 \newcommand{\eP}{\EuScript P}
 259 %\newcommand{\eC}{\EuScript C}
 260 %\newcommand{\eR}{\EuScript R}
 261 %\newcommand{\eI}{\EuScript I}
 262 \renewcommand{\le}{\leqslant}
 263 \renewcommand{\ge}{\geqslant}
 264
 265 \newcommand{\any}[0]{\textrm{@}}
 266
 267 \newcommand{\str}[0]{\textit{Strength}}
 268
 269
 270 %%%%%%%%%%%%%%%%%%%%%%%%
 271 \newcommand{\sortSet}{\mathcal{S}}
 272 \newcommand{\sortVars}{\mathcal{X}_s}
 273 \newcommand{\sortFunctionSet}{\mathcal{F}_s}
 274 \newcommand{\varSet}{\mathcal{X}}
 275 \newcommand{\functionSet}{\mathcal{F}}
 276
 277 \def\unique{\sort{u}}