1\makeatletter 2 3\typeout{``page''} 4 5% cedric: removed for llncs 6 7%page layout 8%\oddsidemargin 0cm 9%\evensidemargin 0cm 10%\topmargin 10pt 11 12%\headheight 0pt 13%\headsep 0pt 14%\footheight 0pt 15%\footskip 24pt 16%\textheight 24cm 17%\textwidth 15.5cm 18%\footnotesep 1cm 19 20%\baselineskip = 24pt plus 4pt minus 3pt 21%\voffset=-0.5cm 22%\hoffset=0.5cm 23 24\makeatother 25 26\makeatletter 27 28% on active et desactive le mode frtypo par \frtypotrue et frtypofalse 29% quelquesoit le mode les caract\`eres : ; ? ! sont actifs. 30% En particulier ces caract\`eres ne peuvent plus \^etre mis dans des 31% \'etiquettes. 32 33\def\halfspace{\kern .166em} 34 35\def\space@pv{\ifmmode ;\else \halfspace;\fi} 36\def\space@dc{\ifmmode :\else \halfspace:\fi} 37\def\space@pi{\ifmmode ?\else \halfspace?\fi} 38\def\space@pe{\ifmmode !\else \halfspace!\fi} 39 40\let\nospace@pv=; 41\let\nospace@dc=: 42\let\nospace@pi=? 43\let\nospace@pe=! 44 45\catcode`;=\active \catcode`:=\active \catcode`?=\active \catcode`!=\active 46 47\def \frtypo 48 {\let;=\space@pv\let:=\space@dc\let!=\space@pe\let?=\space@pi} 49\def \entypo 50 {\let;=\nospace@pv\let:=\nospace@dc\let!=\nospace@pe\let?=\nospace@pi} 51 52\frtypo 53 54\def\@sanitize 55 {\@makeother\ \@makeother\\\@makeother\$\@makeother\&% 56\@makeother\#\@makeother\^\@makeother\^^K\@makeother\_\@makeother\^^A% 57\@makeother\%\@makeother\~\@makeother\;\@makeother\?\@makeother% 58\:\@makeother\!} 59 60\let \oldspecials \dospecials 61\def \dospecials {\oldspecials \do\:\do\!\do \?\do\;} 62 63%\scrollmode 64 65\makeatletter 66%=========================================================================== 67% Personals macros (They might have strange latex side effects 68%----------------- 69 70\def\noparindent{\everypar={\hskip -\parindent\everypar={}}} 71\def \para {\medskip\noparindent} 72\def \pari {\medskip\noparindent} 73\def \parii {\smallskip\noparindent} 74\let\paro=\noparindent 75 76 77%=========================================================================== 78% Definitions Theorems 79%--------------------- 80 81\newif \iffrench 82\if \csname french\endcsname \relax \frenchfalse \else \frenchtrue\fi 83 84\if \csname definition\endcsname\relax 85\newtheorem{definition}{D\iffrench \'e\else e\fi finition}\fi 86\def\bdf{\begin{definition}\begin{em}} 87\def\edf{\ifvmode\vskip-\lastskip\nopagebreak\else 88 \penalty 100\fi\end{em}\end{definition}} 89 90\if \csname theorem\endcsname\relax 91\newtheorem{theorem}{\iffrench Th�or�me\else Theorem\fi}\fi 92\def\bthm{\begin{theorem}} 93\def\ethm{\end{theorem}} 94 95\newtheorem{algorithm}{Algorithm\if\french e\else\fi} 96\def\balgo{\begin{algorithm}} 97\def\ealgo{\end{algorithm}} 98 99\if \csname proposition\endcsname\relax 100\newtheorem{proposition}{Proposition}\fi 101\def\bprop{\begin{proposition}} 102\def\eprop{\end{proposition}} 103 104\if \csname lemma\endcsname\relax 105\newtheorem{lemma}[proposition]{Lemm\iffrench e\else a\fi}\fi 106\def\blem{\begin{lemma}} 107\def\elem{\end{lemma}} 108 109\if \csname corollary\endcsname\relax 110\newtheorem{corollary}[proposition]{Corollary}\fi 111\def\bcor{\begin{corollary}} 112\def\ecor{\end{corollary}} 113 114\def\brmk{\trivlist \item[\hskip \labelsep {\bf {Note}}]} 115\def\ermk{\endtrivlist} 116 117\newtheorem{Note}{Note} 118\def\bnote{\begin{note}\begin{em}} 119\def\enote{\end{em}\end{note}} 120 121\if \csname example\endcsname\relax 122%\newtheorem{example}[remark]{Ex\iffrench a\else e\fi mple}\fi 123\newtheorem{example}{Ex\iffrench a\else e\fi mple}\fi 124\def\bxple{\trivlist \item[\hskip \labelsep {\bf {Example}}]} 125%{\begin{example}\begin{em}} 126\def\exple{\endtrivlist} 127%{\end{em}\end{example}} 128 129\def\@begintheorem#1#2{\it \trivlist \item[\hskip \labelsep{\bf #1\ #2}]} 130\def\@opargbegintheorem#1#2#3{\it \trivlist 131 \item[\hskip \labelsep{\bf #1\ #2\ (#3)}]} 132\def\@endtheorem{\endtrivlist} 133 134\newcount \indemo 135\def \makeno #1{\global \advance \indemo by 1\global 136 \expandafter \edef \csname demo/\the\cdemo/#1\endcsname{\the\indemo}} 137\def \refno #1{\if \relax\csname demo/\the\cdemo/#1\endcsname \relax 138 \write0 {Demo counter #1 undefined}??\else 139 \csname demo/\the\cdemo/#1\endcsname\fi} 140\def \labno #1{\makeno {#1}\refno {#1}} 141 142\newif \ifdemo \demotrue 143\newcount \cdemo 144\newenvironment{demo}{\bdemo}{\edemo} 145\def\bdemotrue{\trivlist \item[\hskip \labelsep 146 {\underline 147 {\iffrench Preuve\else Proof\fi}:}]\advance\cdemo by 1\indemo 0} 148\def\edemo{\penalty 100\hfill\rule{2mm}{2mm} \endtrivlist\@doendpe} 149\long \def \bdemofalse #1\edemo{\relax} 150\outer \def \bdemo 151 {\ifdemo \bdemotrue \else \expandafter \bdemofalse \fi\indent} 152 153\newif \ifhint \hintfalse 154\newtheorem{hint}{\rm \underline {Hint}} 155\def\bhintiftrue{\trivlist \item[\hskip \labelsep {\underline {Hint}:}]} 156\def\ehint{\penalty 100\hfill\noindent\rule{2mm}{2mm}\endtrivlist} 157\long \def \bhintiffalse #1\ehint{\relax} 158\outer \def \bhint 159 {\ifhint \bhintiftrue \else \expandafter \bhintiffalse \fi} 160 161\newif \ifexpert \expertfalse 162\newtheorem{expert}{Remark} 163\def\bexpertiftrue{\trivlist \item[\hskip \labelsep {\underline {Hint}:}]} 164\def\eexpert{\penalty 100\hfill\noindent\rule{2mm}{2mm}\endtrivlist} 165\long \def \bexpertiffalse #1\eexpert{\relax} 166\outer \def \bexpert 167 {\ifexpert \bexpertiftrue \else \expandafter \bexpertiffalse \fi} 168 169 170 171\def\notitle{\hskip\hsize minus\hsize\nobreak\hbox{}} 172 173\def\notation{\paragraph*{Notation}} 174\def\hypothesis{\paragraph*{Assumption}} 175 176 177\def \caseparagraph{\@startsection 178 {case}{6}{\z@}{1.5ex plus .3ex minus .2ex}{-1em}{\normalsize\bf}} 179\def \subcaseparagraph{\@startsection 180% {subcase}{7}{\parindent}{1.5ex plus .3ex minus .2ex}{-1em}{\normalsize\bf}} 181 {subcase}{7}{\z@}{1.5ex plus .3ex minus .2ex}{-1em}{\normalsize\bf}} 182 183 184\if \csname datefrench\endcsname\relax 185\def \langcase {Case} 186\def \langsubcase {Subcase} 187\else 188\def \langcase {Cas} 189\def \langsubcase {Sous-cas} 190\fi 191 192\def\case#1{\caseparagraph*{\langcase\space #1:}} 193\def\othercase#1{\caseparagraph*{#1:}} 194\def\mathcase#1{\caseparagraph*{\langcase\space $#1$:}} 195\def\subcase#1{\subcaseparagraph*{\langsubcase\space #1:}} 196 197% Send a warning when running latex 198\def\warning#1{\immediate\write0{Warning: #1}} 199 200\newenvironment{care}{\bwarning}{\ewarning} 201\def\bcare{\trivlist \item[\hskip \labelsep {\bf Warning!}]} 202\def\ecare{\endtrivlist} 203 204\def\subst#1#2{^{#1} \!/\! _{#2}} 205 206\def \comment #1{{\em #1}} 207%\def \comment #1{} 208\makeatother 209 210 211\makeatletter 212%%% To change size in math mode 213 214\let\Ts=\textstyle 215\let\Ds=\displaystyle 216\let\Ss=\scriptstyle 217 218%%% Abrevs 219 220\let \comp \circ 221\let \wild \_ 222 223 224%%% To put text between two formulas on the same line 225 226\def\text#1{\qquad\hbox{#1}\qquad} 227 228%%% Macros for mathematics 229 230%% Special symbols 231 232\def \nat {{\mathord{I\kern -.33em N}}} 233\def \natb {{\mathord{I\kern -.33em\overline{N}}}} 234 235\def\Vdash {\mathrel{\hbox{\vrule\kern .1ex$\vdash$}}} 236\def\VVdash {\mathrel{\hbox{\vrule\kern .2ex\vrule\kern .1ex $\vdash$}}} 237 238% An open box to end demonstrations with 239 240\def\Box{\hbox 241 {\vbox 242 {\hrule height .033em 243 \hbox to .5em 244 {\vrule width .033em 245 \hbox{\vbox to .5em{\vss}\hss} 246 \vrule width .033em} 247 \hrule height .033em 248 }}} 249 250 251%% Balanced symbols 252 253\def\absolute#1{\mathopen\mid#1\mathclose\mid} 254 255%% Operators 256 257\def \domain {\dv} 258%\def \domain {\dvmathop{\sl dom\,}} 259\def \image {\mathop{\sl im\,}} 260\def \modulo {\mathbin{\rm modulo}} 261\def \inverse{{}^{-1}} 262\def \cardinal {{\sl Card\,}} 263%\def \restrict #1{\mathbin{\mid}_{#1}} 264\def \restrict 265 {\mathbin{\hbox{$\mid$\kern-.24em\lower.09em\hbox{\rm\char'22}$\!$}}} 266\let \arity = \varrho 267 268 269%% Quantifiers 270 271\def \fall #1,{\forall #1,\;} 272\def \exist #1,{\exists #1,\;} 273\def \qt #1.{\forall\,#1.\,} 274\def \ex #1.{\exists\,#1.\,} 275 276%% Arrows 277 278\let\ar=\rightarrow 279\let\dar=\Rightarrow 280\def\imply{\Longrightarrow} 281 282 283\def \rewrite {\mathrel{-}\joinrel\leadsto} 284 285 286%% Equalities 287 288%\def \axiom {\mathrel {\mathop =^!}} 289\def \axiom {=} 290\def \eqdef {\mathrel {\mathop {=\joinrel=}\limits^{def}}} 291 292%% Sizes 293 294\def\({\left(} 295\def\){\right)} 296 297\def\Mid{\mathrel{\Big|}} 298 299%% Indices see also indices.def 300 301\def \ind #1#2{_{#1\in[1,#2]}} 302 303%% 304 305%% names 306 307\let \th \vdash 308\let \tth \Vdash 309\let \ttth \VVdash 310\let \thh \models 311 312\def\Cal#1{{\cal #1}} 313 314\let \eset = \emptyset 315 316 317 318%% Aligned constructions in math mode 319 320% For internal use only 321 322\def\noskip{\lineskiplimit=\the\lineskiplimit 323 \lineskip=\the\lineskip} 324\def\moreskip{\lineskiplimit=0.4em\lineskip=0.4em plus 0.2em} 325\def\moremoreskip{\lineskiplimit=1.2em\lineskip=1.2em plus 0.2em} 326 327\def\vatrix#1{\null\,\vcenter{\normalbaselines\moreskip\m@th 328 \let \and \cr 329 \ialign{$\displaystyle##$\hfil 330 &\quad$\displaystyle##$\hfil&\quad##\hfil\crcr 331 \mathstrut\crcr\noalign{\kern-\baselineskip} 332 #1\crcr\mathstrut\crcr\noalign{\kern-\baselineskip}}}\,} 333 334% A sequence of expressions is writen on separate lines to form one expression 335 336\def \band #1{\left\{\vatrix{#1}\right.} % brace and 337\def \wand #1{\wedge\band{#1}} % wedge and 338\def \vand #1{\vee\band{#1}} % vee and 339\def \vor #1{\vee\left[\vatrix{#1}\right.} % vee and or 340\def \Wand #1{\bigwedge\band{#1}} % big wedge and 341\def \Vand #1{\bigvee\band{#1}} % big vee and 342\def \Wor #1{\bigvee\left[\vatrix{#1}\right.} % big vee and 343 344 345 346% A general usage tabulation in math mode. 347% Indentation is alternatively left and right, so that good place for 348% tabs will produce many different 349 350% \dalign { & blabla :& blabla \cr 351% & bla :& blablabla \cr 352% } 353 354% \dalign { blabla :&& blabla \cr 355% bla : && blablabla \cr 356% } 357 358% \dalign { & blabla :& blabla \cr 359% & bla :& blablabla \cr 360% } 361 362% Internal and personal use 363\def\Dalign#1#2{\vcenter 364 \bgroup 365 \let\>=\qquad 366 \def\title##1{\crcr\noalign{\medskip}\multispan#1{\hfil\bf##1\hfil}} 367% \halign{$##$\hfil\qquad&&\hfil$##{}$&${}##$\hfil\qquad\cr#2\crcr} 368% \halign{$##$\hfil&&\qquad\hfil$##{}$&${}##$\hfil\cr#2\crcr} 369 \halign{&${}##$\hfil&\hfil$##{}$\cr#2\crcr} 370 \egroup} 371% End internal use 372 373\def\align#1{\vcenter 374 \bgroup 375 \let\>=\qquad 376 \halign{#1\crcr} 377 \egroup} 378 379%\def\aligndef#1#2{\expandafter\def\csname aligndef#1\endcsname{#2}} 380%\aligndef ]{\argalign} 381%\aligndef l{&\hfil$##{}$} 382%\aligndef r{&${}##$\hfil} 383%\aligndef c{&\hfil$##$\hfil} 384%\aligndef -{\qquad} 385%\aligndef L{&\hfil##$} 386%\aligndef R{&##\hfil} 387%\aligndef C{&\hfil##\hfil} 388%\def\argalign#1{\relax} 389%\def\prealign#1{\csname aligndef#1\endcsname\prealign} 390%\def\doalign#1]{\dohalign{\prealign#1]}} 391%\def\dohalign#1#2{\expandafter\halign{#1\cr#2\crcr}} 392 393 394 395%\def\dalign#1{\ifx#1[\doalign\else\Dalign3{#1}\fi} 396\def\dalign{\Dalign3} 397 398 399\def\Strut{\raise .4em\hbox{\strut}\raise -.4em\hbox{\strut}} 400 401\def \deftitle #1 402 {\def \title ##1 403 {\crcr\noalign{\medskip}\multispan#1{\hfil\bf##1\hfil}}} 404 405 406 407\bgroup 408 \catcode `\^^M \active 409 \gdef \obeycr {\catcode `\^^M\active \let ^^M\crcr} 410\egroup 411 412 413\ifx \csname linewidth\endcsname \hsize 414 \let \realwidth \hsize 415\else 416 \let \realwidth \linewidth 417\fi 418 419\def \oris {\crcr \mid&} 420\def \syntaxtable #1 421 {\def\is {::=&} 422 \def \\{\cr\noalign{\medskip}}\def\cont{\cr&}\vbox 423 \bgroup 424 \tabskip=100pt plus 1000pt minus 1000pt 425 \halign to \realwidth 426 {\hfil$##{}$\tabskip=0pt& 427 ${}##$\hfil \tabskip=100pt plus 1000pt minus 1000pt& 428 &##\hfil \cr#1\crcr} 429 \egroup} 430 431 432\def \assertions #1 433 {\deftitle2 \vbox 434 \bgroup 435 \halign {\hfil$##{}$&$##$\hfil&&\quad##\hfil\cr#1\crcr} 436 \egroup} 437 438 439%%% old version 440 441\def\malign#1{\vcenter\bgroup 442 \deftitle #1 443 \def \lign ##1\cr {\noalign {##1}} 444 \def \textlign##1{\noalign {\medskip \vbox {\noindent ##1}\medskip}} 445 \tabskip=100pt plus 1000pt minus 1000pt 446 \halign to \realwidth 447 {\hfil$##{}$\tabskip=0pt& 448 ${}##$\hfil \tabskip=100pt plus 1000pt minus 1000pt& 449 &##\hfil&$##$\hfil& \cr#1\crcr\egroup}} 450 451\newif \ifhsize \hsizefalse 452 453\newskip \nullskip \nullskip 0pt 454\newskip \fullskip \fullskip 100pt plus 1000pt minus 1000pt 455\def \maligntrue {\tabskip \fullskip 456 \halign to \realwidth \bgroup} 457\def \malignfalse {\halign \bgroup} 458\def \malign {\vcenter \bgroup \ifhsize \expandafter \maligntrue \else \expandafter \malignfalse \fi} 459\def \endmalign {\crcr \egroup \egroup} 460 461\def \makeword #1#2#3{\expandafter 462 \def \noexpand#3{#2 {#1\expandafter \let \expandafter \dummy\string #3}}} 463 464\let \vect \overrightarrow 465 466\def \uad {\hskip 0.5em} 467 468 469\newskip \mathandskip 470\newskip\mathmargin \mathmargin 0em 471 472\mathandskip 2em plus 0.5fil minus 0.5em 473\def \mathand {\hskip \mathandskip} 474\def \mathleftright {\hfill{}\hskip 0em plus -2fill\penalty 50{}\hfill} 475\def \mathandcr {\penalty 50\mathand} 476\def \mathcr {\penalty -10000\mathand} 477\def \mathcrleft {\hfill{}\hskip 0em plus -2fill\penalty -10000{}\hskip 478 \mathmargin} 479\def \mathbreak {\penalty 50} 480 481\def \incrmargin #1{\advance\mathmargin by #1em\advance\mathmargin by #1em} 482\def \mathslash#1{\let \do \mathcrleft 483 \ifx #1[\let\do\mathdoskip\fi\do#1} 484\def \mathdoskip#1#2]{\incrmargin {#2}\mathcrleft} 485 486% Type inference rules 487 488\let \mathmoreskip=\moremoreskip 489\def \nomoreskip {\let \mathmoreskip \relax} 490 491\def \bmaths {\let \and \mathandcr \hsize \realwidth 492 \centering \vbox \bgroup \mathmoreskip \noindent 493 $\displaystyle \let \\ \mathslash} 494\def \emaths {\unskip$\egroup} 495\def \mathflushleft {\def \emaths {\hfill$\egroup}\nomoreskip} 496\newenvironment {maths}{\bmaths}{\emaths} 497 498\def \maths #1{\bmaths #1\emaths} 499 500\def \whereis {\leftarrow} 501\def \where #1{[{\let \is \whereis #1}]} 502\def \dowhere #1\is#2\is{[\ifx#2\empty #1\else #2/#1\fi]} 503\def \where #1{\let \is \relax\dowhere #1\is\empty\is} 504 505\let \closeplus\relax 506\let \Empty \relax 507\let \is \relax 508\def \plus #1{\PLUS #1\is\is\END} 509\def \PLUS #1\is#2\is#3\END{\oplus\ifx #3\is (#1\plustoken#2)\else #1\fi} 510\let \plustoken \mapsto 511 512\let \diverge \uparrow 513 514\def \set #1{\{#1\}} 515\def \sem #1{\lbrack\!\lbrack#1\rbrack\!\rbrack} 516 517 518\def\mathrm #1{\mathrel {\rm #1}} 519\let \coerce \leq 520\makeatother 521 522\makeatletter 523 524 525%% see infer.doc for a documentation 526 527% Judgements 528 529\let\th=\vdash 530 531% naming 532 533\expandafter \ifx \csname name\endcsname\relax 534 \def\name#1{\hbox{\sc #1}}\else \relax \fi 535 536\def \labname #1{{\rm(\name{#1})}} 537\let \lab = \labname 538\def \clab #1{\hbox {$\smash {\lab{#1}}$}} 539\newskip \beforelabskip \beforelabskip = 0.5em 540\def \eqlab {\eqno \lab} 541 542%% inside rules 543 544\def \nmir #1[#2]{\crcr \hrulefill \cr} 545\def \rmir #1[#2]{\crcr \hrulefill & \clab {#2} \cr} 546\def \lmir #1[#2]{\relax} 547\def \Lmir #1[#2]{\crcr \Llabo {#2}\hrulefill \cr} 548\def \Rmir #1[#2]{\crcr \hrulefill \Rlabo {#2}\cr} 549\def \imir {\crcr \hrulefill\cr} 550 551% outside rules 552 553\def \rlabo #1{\hskip \beforelabskip \clab {#1}} 554\def \llabo #1{\clab {#1}\hskip \beforelabskip} 555\def \Rlabo #1{\rlap {\rlabo {#1}}} 556\def \Llabo #1{\llap {\llabo {#1}}} 557\let \labr \rlabo \let \labl \llabo \let \labR \Rlabo \let \labL \Llabo 558 559 560\def \rlab #1 {\rlap {\lab {#1}}} 561\def \llab #1 {\llap {\lab {#1}}} 562 563 564% A good separator for multiple hypothesis 565 566\let \and \qquad 567\let \andcr \cr 568 569 570% Single rules 571 572\def \lessskip {\lineskiplimit=.3em\lineskip= .2em plus .1em} 573 574\makeatletter 575\def \mathrulename {\scriptsize \labname} 576\def \ignoredash #1{\let\next\ignoredash 577 \ifx #1-\relax\else\let\next#1\fi\next} 578\def \mathrule {\@ifnextchar [{\mathrulelab}{\@mathrule}} 579\def \mathrulelab[#1]#2{\hbox 580 {\vbox {\hbox {\mathrulename {#1}}\nointerlineskip\smallskip 581 \hbox {$\@mathrule{#2}$}}}} 582\def \@mathrule #1{{\let \and \qquad \let \rlab \rl \let \llab \ll 583 \def \mir {MiR}\def\endrule {EnDrUlE} 584 \displaystyle \offinterlineskip \lessskip \bgroup \openrule 585 \beginrule #1\mir \mir \endrule}} 586\def \beginrule #1\mir#2{#1\ifx #2\mir \let \next \finishrule 587 \else \def \next {\middlerule\openrule \beginrule\ignoredash#2}\fi\next} 588\def\finishrule#1\endrule{\closerule\egroup} 589 590\def \openrule {\hbox \bgroup \vbox \bgroup 591 \halign \bgroup \hfil $##$\hfil &\hskip \beforelabskip$##$\hfil \cr} 592\def \closerule {\crcr\egroup\egroup\egroup} 593%\def \endrule {\closerule \egroup} 594 595\def \singleRule {\crcr\noalign {\vskip -0.1em}\closerule \over} 596\let \middlerule \singleRule 597 598 599% Double and Tripple rules see infer-more.def 600 601% Logic and rewriterules 602 603\def \logicrule #1{\let \mir \Longrightarrow #1} 604 605 606\def \longleadsto {\mathrel{-}\joinrel\leadsto} 607 608\def \rewriterule #1{\displaystyle \offinterlineskip \lessskip 609 \bgroup\let \mir \longleadsto \openrule#1\endrule} 610 611\def \suspend #1{\vbox to #1 {\leaders \hbox {$\cdot$}\vfill}} 612 613 614\if \relax \csname keywordstyle\endcsname \let \keywordstyle \tt \fi 615 616%\def \keyword #1{{\hbox {\keywordstyle #1}}} 617\def \keyword #1{{\keywordstyle #1}} 618\def \mathtoken #1{\ifmmode 619 \mathopen{}\keyword {#1}\mathclose{}\else \keyword{#1}\fi} 620\def \mathpostfix #1{\mathrel{\keyword {#1}}\mathclose{}} 621\def \mathprefix #1{\mathopen{}\mathrel{\keyword {#1}}} 622\def \mathinfix #1{\mathrel{\keyword {#1}}} 623 624\def\ignorefirst #1{} 625\def \lwt #1{\expandafter \lowercase \expandafter \bgroup 626 \expandafter \ignorefirst \string #1\egroup} 627 628 629\def \makeprefix #1#2{\expandafter\def \noexpand #1{\mathprefix {#2}}} 630\def \makepostfix #1#2{\expandafter\def \noexpand #1{\mathpostfix {#2}}} 631\def \maketoken #1#2{\expandafter\def \noexpand #1{\mathtoken {#2}}} 632\def \makeinfix #1#2{\expandafter\def \noexpand #1{\mathinfix {#2}}} 633 634\def \makein #1{\expandafter\def 635 \noexpand #1##1in{\keyword {\lwt #1}\,\,##1\,\,\keyword {in}\,\,}} 636 637\let \@ \; 638\def \Let #1=#2in{\keyword {let}\@ {#1 = #2} \@\keyword {in}\@} 639\def \fun (#1){\keyword {fun}\@ #1 \rightarrow} 640\def \type #1=#2in{\keyword {type}\@ #1 = #2 \@\keyword {in}\@} 641 642\makeatother 643 644\let \cont \kappa 645\let \t \tau 646\let \l \ell 647\let \s \sigma 648\let \tv \alpha 649\let \vect \bar 650 651\def \Gen {{\rm Gen}} 652 653\def \tplus #1{\TPLUS #1\is\is\END} 654\def \TPLUS #1\is#2\is#3\END{\oplus\ifx #3\is (#1:#2)\else #1\fi} 655 656%%%%%%%%%%%%%%% light programs 657 658\makeatletter 659\def \progstyle {\tt} 660\newskip \programindent \programindent 4em 661\def \program {\par \begingroup 662 \medskip \parindent \programindent \@tempswafalse 663 \frenchspacing \@vobeyspaces \let \par \programpar 664 \obeylines \progstyle 665 \catcode``=13 \@noligs \let \do \@makeother \dospecials 666 \catcode `\\ 0 \catcode `\{ 1 \catcode `\} 2 667 \prog@specials \prog@initspecials \obeyspaces} 668 669\def \programpar {\if@tempswa\hbox{}\fi\@tempswatrue\@@par} 670 671\bgroup 672\gdef \less@specials {\relax 673 \catcode `| \active 674 \catcode `< \active 675 \catcode `> \active 676 \catcode `- \active 677 \catcode `\' \active 678} 679\gdef \more@specials {\relax 680 \catcode `( \active 681 \catcode `) \active 682} 683\gdef \prog@specials {\less@specials\more@specials} 684\prog@specials 685\gdef \prog@initspecials {\def 686 -{\minus@program}\def 687 '{\acurate@program}\def 688 |{\bar@program}\def 689 <{\less@program}\def 690 >{\greater@program}\def 691 ({\less@program}\def 692 ){\greater@program}} 693 \gdef \bar@@program {\let\do \eattoken 694 \ifx \token >$\droite$\else ${}\mid{}$\let \do \relax\fi \do} 695 \gdef \minus@@program {\let\do \eattoken 696 \ifx \token >$\ar$\else -\let \do \relax\fi \do} 697\egroup 698 699\def \acurate@program {\futurelet \token \acurate@@program} 700\def \acurate@@program {\let \do \eattoken 701 \ifx \token a$\alpha$\else 702 \ifx \token b$\beta$\else 703 \char `\' \let \do \relax\fi\fi \do} 704\def \less@program {\hbox{$<$}} 705\def \greater@program {\hbox{$>$}} 706\def \bar@program {\futurelet \token \bar@@program} 707\def \minus@program {\futurelet \token \minus@@program} 708 709 710\def \endprogram {\ifdim\lastskip >\z@ \@tempskipa\lastskip 711 \vskip -\lastskip\fi\medskip \endgroup 712 \@endpetrue} 713 714\def\prog {\begingroup \hbox \bgroup 715 \catcode ``=13 \@noligs 716 \let \do \@makeother \dospecials \progstyle 717 \prog@specials \prog@initspecials 718 \catcode `\\ 0 \catcode `\{ 1 \catcode `\} 2 719 \@prog} 720\def\@prog#1{\obeyspaces \frenchspacing \catcode `\ 10 721 \def\@tempa ##1#1{##1\egroup\endgroup}\@tempa} 722\makeatother 723 724%%%%%%%%%%%%%%%%%%% "quotations" 725 726\makeatletter 727% on active le cararectere " et on s'en sert pour le mode \prog 728% s'il est d�fini ou \verb autrement 729 730\bgroup 731\@makeother \" 732\gdef \progquote {\prog"} 733\catcode `\" \active 734\gdef "{\progquote} 735\egroup 736 737\def \quoteon { 738\let \quote@sanitize \@sanitize 739\def \@sanitize {\quote@sanitize \@makeother\"} 740\let \quote@specials \dospecials 741\def \dospecials {\quote@specials \do\"} 742\def \quoteon {\catcode `\" \active}\quoteon} 743 744\def \quoteoff {\@makeother \"} 745\makeatother 746 747 748 749%%%%%%%%%%%%%%%% 750\def \lift #1{\;{}^{#1}} 751\def \inu #1{\lift {i \in 1..#1}} 752\def \jnu #1{\lift {j \in 1..#1}} 753 754%% typo 755 756\mathchardef \le "313C 757\mathchardef \ge "313E 758 759\mathcode `< "4268 760\mathcode `> "5269 761 762 763\catcode `\| \active 764\let \olspecials \dospecials \def \dospecials {\olspecials \do \|} 765 766%\def \droite {\mathrel {\,\hbox {\large$\triangleright$}\,}} 767\def \droite {\mathrel{\tt =}} 768 769\makeatletter 770\def |{\baractive} 771\def \baractive {\futurelet\token \next@baractive} 772\def \eattoken #1{} 773\def \next@baractive{\let\do\eattoken 774 \ifx \token>\droite\else \mid \let \do \relax \fi \do} 775 776 777\def \Def #1in{\mathprefix {let}#1\mathinfix{in}} 778\def \Let#1in{\mathprefix {let}#1\mathinfix{in}} 779\def \Reply#1to{\mathprefix {reply}#1\mathinfix{to}} 780\def \>{\droite} 781\def \And {\mathrel{\tt and}} 782\def \tuple #1{{\tt (}#1{\tt )}} 783\def \<#1> {\tuple {#1}} 784 785\let \bcup \cup 786\let \thd \th 787\def \fv {fv} 788\def \defines {::} 789\def \produces #1{\Ds\mathop{\Longrightarrow}^{#1}} 790\def \reduces {\longrightarrow} 791\let \red \reduces 792\let \redcham \mapsto 793 794\let \plus \tplus 795 796\makeatother 797 798 799\def \dd {{\cal D}} 800\def \pp {{\cal P}} 801 802\def \dv {dv} 803 804\def \redsoupe {\mathrel {\mathop {\red} \limits^s}} 805\let \redstruct \rightleftharpoons 806\let \redchaud \rightharpoonup 807\let \redfroid \leftharpoondown 808\let \cool \leftharpoondown 809\let \heat \rightharpoonup 810 811\def\redstep{\mathrel{\mathpalette\redstepaux{}}} 812\def\redstepaux#1{\vcenter{\hbox{\ooalign{\hfil 813 \raise2pt \hbox{$\rightharpoonup$}\hfil\cr\hfil 814 \lower2pt\hbox {$\leftharpoondown$}\hfil\crcr 815 $\longrightarrow$}}}} 816 817 818\let \redsoupe \red 819\let \redx \red 820 821 822\def \Comment #1{} 823\let \agree \approx 824\quoteon 825 826\maketoken \int {int} 827 828 829