iris.sty 12.7 KB
Newer Older
1 2 3 4 5
\NeedsTeXFormat{LaTeX2e}[1999/12/01]
\ProvidesPackage{iris}

\RequirePackage{tikz}
\RequirePackage{scalerel}
6 7 8 9 10 11 12
\RequirePackage{array}
\RequirePackage{dashbox}
\RequirePackage{tensor}
\RequirePackage{xparse}
\RequirePackage{xstring}
\RequirePackage{mathtools}

13 14 15 16 17 18 19 20 21 22 23 24 25 26 27 28 29
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%% SETUP
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%


\usetikzlibrary{shapes}
%\usetikzlibrary{snakes}
\usetikzlibrary{arrows}
\usetikzlibrary{calc}
\usetikzlibrary{arrows.meta}
\tikzstyle{state}=[circle, draw, minimum size=1.2cm, align=center]
\tikzstyle{trans}=[arrows={->[scale=1.4]}]

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%% MATH SYMBOLS & NOTATION & IDENTIFIERS
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

30 31
\newcommand{\nat}{\mathbb{N}}

32
\DeclareMathOperator*{\Sep}{\scalerel*{\ast}{\sum}}
Ralf Jung's avatar
Ralf Jung committed
33 34
\newcommand*{\disj}[1][]{\mathrel{\#_{#1}}}
\newcommand\pord{\sqsubseteq}
35 36 37 38
\newcommand\dplus{\mathbin{+\kern-1.0ex+}}
\newcommand{\upclose}{\mathord{\uparrow}}
\newcommand{\ALT}{\ |\ }

39
\newcommand{\spac}{\,} % a space
40 41 42 43 44 45 46

\def\All #1.{\forall #1.\spac}%
\def\Exists #1.{\exists #1.\spac}%
\def\Ret #1.{#1.\spac}%

\newcommand{\any}{{\rule[-.2ex]{1ex}{.4pt}}}%

Ralf Jung's avatar
Ralf Jung committed
47
\newcommand{\judgment}[2][]{\paragraph{#1}\hspace{\stretch{1}}\fbox{$#2$}}
48 49 50

\newcommand{\pfn}{\rightharpoonup}
\newcommand\fpfn{\xrightharpoonup{\kern-0.25ex\textrm{fin}\kern-0.25ex}}
Ralf Jung's avatar
Ralf Jung committed
51
\newcommand{\la}{\leftarrow}
52 53 54
\newcommand{\ra}{\rightarrow}
\newcommand{\Ra}{\Rightarrow}
\newcommand{\Lra}{\Leftrightarrow}
55 56
\newcommand\monra{\xrightarrow{\kern-0.15ex\textrm{mon}\kern-0.05ex}}
\newcommand\nfn{\xrightarrow{\kern-0.15ex\textrm{ne}\kern-0.05ex}}
57
\newcommand{\eqdef}{\triangleq}
Ralf Jung's avatar
Ralf Jung committed
58 59
\newcommand{\bnfdef}{\vcentcolon\vcentcolon=}

Ralf Jung's avatar
Ralf Jung committed
60 61
\newcommand{\maybe}[1]{#1^?}

62 63
\newcommand*\setComp[2]{\left\{#1\spac\middle|\spac#2\right\}}
\newcommand*\set[1]{\left\{#1\right\}}
64
\newcommand*\record[1]{\left\{\spac#1\spac\right\}}
Ralf Jung's avatar
Ralf Jung committed
65
\newcommand*\recordComp[2]{\left\{\spac#1\spac\middle|\spac#2\spac\right\}}
66 67 68 69 70 71 72

\newenvironment{inbox}[1][]{
  \begin{array}[#1]{@{}l@{}}
}{
  \end{array}
}

Ralf Jung's avatar
Ralf Jung committed
73
\newcommand{\op}{\textrm{op}}
74 75 76 77 78 79
\newcommand{\dom}{\mathrm{dom}}
\newcommand{\cod}{\mathrm{cod}}
\newcommand{\chain}{\mathrm{chain}}

\newcommand{\pset}[1]{\wp(#1)} % Powerset
\newcommand{\psetdown}[1]{\wp^\downarrow(#1)}
Ralf Jung's avatar
Ralf Jung committed
80
\newcommand{\finpset}[1]{\wp^\mathrm{fin}(#1)}
Ralf Jung's avatar
Ralf Jung committed
81 82
\newcommand{\pmultiset}[1]{\wp^{+}(#1)}
\newcommand{\finpmultiset}[1]{\wp^{\mathrm{fin},+}(#1)}
83 84 85

\newcommand{\Func}{F} % functor

86 87
\newcommand{\subst}[3]{{#1}[{#3} / {#2}]}

Ralf Jung's avatar
Ralf Jung committed
88 89 90 91 92 93
\newcommand{\mapinsert}[3]{#3\left[#1\mathop{\la}#2\right]}
\newcommand{\mapsingleton}[2]{\mapinsert{#1}{#2}{}}
\newcommand{\mapinsertComp}[4]
  {\mapinsert{#1}{#2 \spac\middle|\spac #3}{#4}}
\newcommand{\mapComp}[3]
  {\mapinsertComp{#1}{#2}{#3}{}}
94 95 96

\newcommand{\nil}{\epsilon}

97 98 99 100 101 102 103 104 105
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%% MODEL-SPECIFIC SYMBOLS & NOTATION & IDENTIFIERS
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\newcommand{\textdom}[1]{\textit{#1}}

\newcommand{\wIso}{\xi}

\newcommand{\rs}{r}
\newcommand{\rsB}{s}
Ralf Jung's avatar
Ralf Jung committed
106
\newcommand{\rss}{R}
107 108 109 110 111 112

\newcommand{\pres}{\pi}
\newcommand{\wld}{w}
\newcommand{\ghostRes}{g}

%% Various pieces of syntax
Ralf Jung's avatar
Ralf Jung committed
113 114
\newcommand{\wsat}[3]{#1 \models_{#2} #3}
\newcommand{\wsatpre}{\textdom{pre-wsat}}
115 116 117 118 119 120 121 122

\newcommand{\wtt}[2]{#1 : #2} % well-typed term

\newcommand{\nequiv}[1]{\ensuremath{\mathrel{\stackrel{#1}{=}}}}
\newcommand{\notnequiv}[1]{\ensuremath{\mathrel{\stackrel{#1}{\neq}}}}
\newcommand{\nequivset}[2]{\ensuremath{\mathrel{\stackrel{#1}{=}_{#2}}}}
\newcommand{\nequivB}[1]{\ensuremath{\mathrel{\stackrel{#1}{\equiv}}}}
\newcommand{\latert}{\mathord{\blacktriangleright}}
Ralf Jung's avatar
Ralf Jung committed
123
\newcommand{\latertinj}{\textlog{next}}
124 125 126 127 128 129 130 131

\newcommand{\Sem}[1]{\llbracket #1 \rrbracket}

\newcommand{\sembox}[1]{\hfill \normalfont \mbox{\fbox{\(#1\)}}}
\newcommand{\typedsection}[2]{\subsubsection*{\rm\em #1 \sembox{#2}}}


%% Some commonly used identifiers
Ralf Jung's avatar
Ralf Jung committed
132
\newcommand{\SProp}{\textdom{SProp}}
133
\newcommand{\UPred}{\textdom{UPred}}
Ralf Jung's avatar
Ralf Jung committed
134 135
\newcommand{\mProp}{\textdom{Prop}} % meta-level prop
\newcommand{\iProp}{\textdom{iProp}}
Ralf Jung's avatar
Ralf Jung committed
136
\newcommand{\iPreProp}{\textdom{iPreProp}}
Ralf Jung's avatar
Ralf Jung committed
137
\newcommand{\Wld}{\textdom{Wld}}
Ralf Jung's avatar
Ralf Jung committed
138
\newcommand{\Res}{\textdom{Res}}
139 140 141 142
\newcommand{\State}{\textdom{State}}
\newcommand{\Val}{\textdom{Val}}
\newcommand{\Loc}{\textdom{Loc}}
\newcommand{\Expr}{\textdom{Expr}}
143 144
\newcommand{\Var}{\textdom{Var}}
\newcommand{\ThreadPool}{\textdom{ThreadPool}}
145

146 147 148
% List
\newcommand{\List}{\ensuremath{\textdom{List}}}

149 150 151 152 153
\newcommand{\ofe}{T}
\newcommand{\ofeB}{U}
\newcommand{\cofe}{\ofe}
\newcommand{\cofeB}{\ofeB}
\newcommand{\OFEs}{\mathcal{OFE}} % category of OFEs
Ralf Jung's avatar
Ralf Jung committed
154
\newcommand{\COFEs}{\mathcal{COFE}} % category of COFEs
155
\newcommand{\iFunc}{\Sigma}
Ralf Jung's avatar
Ralf Jung committed
156
\newcommand{\fix}{\textdom{fix}}
157 158 159 160 161 162 163

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% CMRA (RESOURCE ALGEBRA) SYMBOLS & NOTATION & IDENTIFIERS
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\newcommand{\textmon}[1]{\textsc{#1}}

\newcommand{\monoid}{M}
Ralf Jung's avatar
Ralf Jung committed
164
\newcommand{\mval}{\mathcal{V}}
165 166 167 168 169 170 171

\newcommand{\melt}{a}
\newcommand{\meltB}{b}
\newcommand{\meltC}{c}
\newcommand{\melts}{A}
\newcommand{\meltsB}{B}

Ralf Jung's avatar
Ralf Jung committed
172 173
\newcommand{\f}{\mathrm{f}} % for "frame"

174
\newcommand{\munit}{\varepsilon}
Ralf Jung's avatar
Ralf Jung committed
175
\newcommand{\mcore}[1]{{\mid}#1{\mid}} % using "|" here makes LaTeX diverge. WTF.
Ralf Jung's avatar
Ralf Jung committed
176
\newcommand{\mnocore}{\bot}
177
\newcommand{\mtimes}{\mathbin{\cdot}}
178
\newcommand{\mundef}{\lightning}
179 180

\newcommand{\mupd}{\rightsquigarrow}
181
\newcommand{\mincl}[1][]{\ensuremath{\mathrel{\stackrel{#1}{\preccurlyeq}}}}
182

Ralf Jung's avatar
Ralf Jung committed
183
\newcommand{\CMRAs}{\mathcal{CMRA}} % category of CMRAs
184 185 186 187 188 189 190 191 192 193 194 195 196 197 198

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%% LOGIC SYMBOLS & NOTATION & IDENTIFIERS
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\newcommand{\textlog}[1]{\textsf{#1}}

\newcommand{\Sig}{\mathcal{S}}
\newcommand{\SigType}{\mathcal{T}}
\newcommand{\SigFn}{\mathcal{F}}
\newcommand{\SigAx}{\mathcal{A}}
\newcommand{\sigtype}{T}
\newcommand{\sigfn}{F}
\newcommand{\sigax}{A}

\newcommand{\type}{\tau}
199
\newcommand{\typeB}{\sigma}
200 201 202 203 204 205 206 207 208 209 210 211 212 213 214

\newcommand{\var}{x}
\newcommand{\varB}{y}
\newcommand{\varC}{z}

\newcommand{\term}{t}
\newcommand{\termB}{u}

\newcommand{\vctx}{\Gamma}
\newcommand{\pfctx}{\Theta}

\newcommand{\prop}{P}
\newcommand{\propB}{Q}
\newcommand{\propC}{R}

215 216 217 218 219 220 221
% pure propositions
\newcommand{\pprop}{\phi}
\newcommand{\ppropB}{\psi}

\newcommand{\pred}{\varPhi}
\newcommand{\predB}{\Psi}
\newcommand{\predC}{\Zeta}
222 223 224 225 226 227

\newcommand{\gname}{\gamma}
\newcommand{\iname}{\iota}

\newcommand{\mask}{\mathcal{E}}
\newcommand{\namesp}{\mathcal{N}}
Ralf Jung's avatar
Ralf Jung committed
228
\newcommand{\namecl}[1]{{#1^{\kern0.2ex\uparrow}}}
229 230

%% various pieces of Syntax
231
\def\MU #1.{\mu\spac #1.\spac}%
232 233 234
\def\Lam #1.{\lambda #1.\spac}%

\newcommand{\proves}{\vdash}
Ralf Jung's avatar
Ralf Jung committed
235
\newcommand{\provesIff}{\mathrel{\dashv\vdash}}
236

237
\newcommand{\wand}{\mathrel{-\!\!*}}
238 239

% oh my... I have to wrap the "-" in a \mathrm, otherwise all hell breaks lose...
240
\newcommand{\fmapsto}[1][]{\xmapsto{#1}}
241 242 243
\newcommand{\gmapsto}{\hookrightarrow}%
\newcommand{\fgmapsto}[1][\mathrm{-}]{\xhookrightarrow{#1}}%

244
\NewDocumentCommand\wpre{m O{} m}%
245
  {\textlog{wp}_{#2}\spac#1\spac{\left\{#3\right\}}}
246

247 248 249
\newcommand{\later}{\mathop{\triangleright}}
\newcommand{\always}{\mathop{\Box}}
\newcommand{\pure}{\mathop{\blacksquare}}
250 251 252 253 254 255 256 257

%% Invariants and Ghost ownership
% PDS: Was 0pt inner, 2pt outer.
% \boxedassert [tikzoptions] contents [name]
\tikzstyle{boxedassert_border} = [sharp corners,line width=0.2pt]
\NewDocumentCommand \boxedassert {O{} m o}{%
	\tikz[baseline=(m.base)]{
		%	  \node[rectangle, draw,inner sep=0.8pt,anchor=base,#1] (m) {${#2}\mathstrut$};
258
		\node[rectangle,inner sep=0.8pt,outer sep=0.2pt,anchor=base] (m) {${\,#2\,}\mathstrut$};
259 260 261 262 263
		\draw[#1,boxedassert_border] ($(m.south west) + (0,0.65pt)$) rectangle ($(m.north east) + (0, 0.7pt)$);
	}\IfNoValueF{#3}{^{\,#3}}%
}
\newcommand*{\knowInv}[2]{\boxedassert{#2}[#1]}
\newcommand*{\ownGhost}[2]{\boxedassert[densely dashed]{#2}[#1]}
Ralf Jung's avatar
Ralf Jung committed
264 265
\newcommand*{\ownM}[1]{\textlog{Own}(#1)}
\newcommand*{\ownPhys}[1]{\textlog{Phy}(#1)}
266 267 268 269 270 271 272 273 274 275 276 277

%% View Shifts
\NewDocumentCommand \vsGen {O{} m O{}}%
  {\mathrel{%
    \ifthenelse{\equal{#3}{}}{%
      % Just one mask, or none
      {#2}_{#1}%
    }{%
      % Two masks
      \tensor*[^{#1}]{#2}{^{#3}}
    }%
  }}%
278 279
\NewDocumentCommand \vs {O{} O{}} {\vsGen[#1]{\Rrightarrow}[#2]}
\NewDocumentCommand \vsL {O{} O{}} {\vsGen[#1]{\Lleftarrow}[#2]}
280
\NewDocumentCommand \vsE {O{} O{}} %
281
  {\vsGen[#1]{\Lleftarrow\!\!\!\Rrightarrow}[#2]}
282
\NewDocumentCommand \pvs {O{} O{}} {\mathord{\vsGen[#1]{{\mid\kern-0.5ex\Rrightarrow\kern-0.25ex}}[#2]\kern0.2ex}}
283

284
\newcommand\vsWand{{\displaystyle\equiv\kern-1.6ex-\kern-1.5ex\smash{\scalerel*{\vphantom-\ast}{\sum}}\kern-0.2ex}}
Ralf Jung's avatar
Ralf Jung committed
285 286
\NewDocumentCommand \vsW {O{} O{}} {\vsGen[#1]{\vsWand}[#2]}

287
% for now, the update modality looks like a pvs without masks.
288
\NewDocumentCommand \upd {} {\mathop{\mid\kern-0.4ex\Rrightarrow\kern-0.25ex}}
289

290 291 292 293 294 295 296 297 298 299 300

%% Hoare Triples
\newcommand*{\hoaresizebox}[1]{%
  \hbox{$\mathsurround=0pt{#1}\mathstrut$}}
\newcommand*{\hoarescalebox}[2]{%
  \hbox{\scalerel*[1ex]{#1}{#2}}}
\newcommand{\triple}[5]{%
  \setbox0=\hoaresizebox{{#3}{#5}}%
  \setbox1=\hoarescalebox{#1}{\copy0}%
  \setbox2=\hoarescalebox{#2}{\copy0}%
  \copy1{#3}\copy2%
301
  \; #4 \;%
302 303 304 305 306 307 308 309 310 311
  \copy1{#5}\copy2}

\newcommand{\bracket}[4][]{%
  \setbox0=\hbox{$\mathsurround=0pt{#1}{#4}\mathstrut$}%
  \scalerel*[1ex]{#2}{\copy0}%
  {#4}%
  \scalerel*[1ex]{#3}{\copy0}}
% \curlybracket[other] x
\newcommand{\curlybracket}[2][]{\bracket[{#1}]\{\}{#2}}
\newcommand{\anglebracket}[2][]{\bracket[{#1}]\langle\rangle{#2}}
312 313 314 315 316

\NewDocumentCommand \hoare {m m m O{}}{
	\curlybracket{#1}\spac #2 \spac \curlybracket{#3}_{#4}%
}

317 318 319 320 321 322 323 324 325 326 327 328 329 330 331 332 333 334 335
% \hoareV[t] pre c post [mask]
\NewDocumentCommand \hoareV {O{c} m m m O{}}{
		{\begin{aligned}[#1]
		&\curlybracket{#2} \\
		&\quad{#3} \\
		&{\curlybracket{#4}}_{#5}
		\end{aligned}}%
}
% \hoareHV[t] pre c post [mask]
\NewDocumentCommand \hoareHV {O{c} m m m O{}}{
	{\begin{aligned}[#1]
	&\curlybracket{#2} \; {#3} \\
	&{\curlybracket{#4}}_{#5}
	\end{aligned}}%
}


%% Some commonly used identifiers
\newcommand{\timeless}[1]{\textlog{timeless}(#1)}
336
\newcommand{\persistent}[1]{\textlog{persistent}(#1)}
337
\newcommand{\physatomic}[1]{\textlog{atomic}($#1$)}
338 339 340 341 342 343 344 345 346
\newcommand{\infinite}{\textlog{infinite}}

\newcommand{\Prop}{\textlog{Prop}}
\newcommand{\Pred}{\textlog{Pred}}

\newcommand{\TRUE}{\textlog{True}}
\newcommand{\FALSE}{\textlog{False}}

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
Ralf Jung's avatar
Ralf Jung committed
347
% GENERIC LANGUAGE SYNTAX AND SEMANTICS
348 349 350 351 352 353
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\newcommand{\expr}{e}
\newcommand{\val}{v}
\newcommand{\valB}{w}
\newcommand{\state}{\sigma}
\newcommand{\step}{\ra}
354 355
\newcommand{\hstep}{\ra_{\mathsf{h}}}
\newcommand{\tpstep}{\ra_{\mathsf{tp}}}
356
\newcommand{\lctx}{K}
357
\newcommand{\Lctx}{\textdom{Ctx}}
358

359 360
\newcommand{\toval}{\mathrm{expr\any to\any val}}
\newcommand{\ofval}{\mathrm{val\any to\any expr}}
361 362
\newcommand{\atomic}{\mathrm{atomic}}
\newcommand{\red}{\mathrm{red}}
363 364 365 366 367 368
\newcommand{\Lang}{\Lambda}

\newcommand{\tpool}{T}

\newcommand{\cfg}[2]{{#1};{#2}}

369 370
\def\fill#1[#2]{#1 {[}\, #2\,{]} }

371 372 373 374
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% STANDARD DERIVED CONSTRUCTIONS
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

Ralf Jung's avatar
Ralf Jung committed
375 376 377
\newcommand{\unittt}{()}
\newcommand{\unit}{1}

378 379
% Agreement
\newcommand{\agm}{\ensuremath{\textmon{Ag}}}
Ralf Jung's avatar
Ralf Jung committed
380
\newcommand{\aginj}{\textlog{ag}}
381 382 383 384 385 386

% Fraction
\newcommand{\fracm}{\ensuremath{\textmon{Frac}}}

% Exclusive
\newcommand{\exm}{\ensuremath{\textmon{Ex}}}
Ralf Jung's avatar
Ralf Jung committed
387
\newcommand{\exinj}{\textlog{ex}}
388 389 390 391 392 393 394 395 396

% Auth
\newcommand{\authm}{\textmon{Auth}}
\newcommand{\authfull}{\mathord{\bullet}\,}
\newcommand{\authfrag}{\mathord{\circ}\,}

\newcommand{\AuthInv}{\textsf{AuthInv}}
\newcommand{\Auth}{\textsf{Auth}}

Ralf Jung's avatar
Ralf Jung committed
397
% Sum
398
\newcommand{\csumm}{\mathrel{+_{\!\mundef}}}
Ralf Jung's avatar
Ralf Jung committed
399 400 401
\newcommand{\cinl}{\textsf{inl}}
\newcommand{\cinr}{\textsf{inr}}

Ralf Jung's avatar
Ralf Jung committed
402 403 404 405 406 407
% One-Shot
\newcommand{\oneshotm}{\ensuremath{\textmon{OneShot}}}
\newcommand{\ospending}{\textlog{pending}}
\newcommand{\osshot}{\textlog{shot}}

% STSs
408 409
\newcommand{\STSCtx}{\textlog{StsCtx}}
\newcommand{\STSSt}{\textlog{StsSt}}
410 411 412
\newcommand{\STSclsd}{\textlog{closed}}
\newcommand{\STSauth}{\textlog{auth}}
\newcommand{\STSfrag}{\textlog{frag}}
413 414 415
\newcommand{\STSS}{\mathcal{S}} % states
\newcommand{\STST}{\mathcal{T}} % tokens
\newcommand{\STSL}{\mathcal{L}} % labels
416
\newcommand{\stsstep}{\ra}
417
\newcommand{\ststrans}{\ra^{*}}%	the relation relevant to the STS rules
418 419
\newcommand{\stsfstep}[1]{\xrightarrow{#1}}
\newcommand{\stsftrans}[1]{\stsfstep{#1}^{*}}
420 421 422 423 424

\tikzstyle{sts} = [->,every node/.style={rectangle, rounded corners, draw, minimum size=1.2cm, align=center}]
\tikzstyle{sts_arrows} = [arrows={->[scale=1.5]},every node/.style={font=\sffamily\small}]

%% Stored Propositions
425
\newcommand{\mapstoprop}{\mathrel{\kern-0.5ex\tikz[baseline=(m)]{\node at (0,0) (m){}; \draw[line cap=round] (0,0.16) -- (0,-0.004);}\kern-1.5ex\Ra}}
426 427

\endinput
428