; TeX output 1996.03.06:1219so*sDtGGcmr17The7tGGcmss17ozpacqkage!", cmsy10XQ cmr12editedbrySebastianRahtzS.Rahrtz@elsevier.co.uk&37 1995/10/03:ōINff cmbx12ContentsI"V cmbx101XIn9troQduction1 XK`y cmr101.1oMoGdi cationUUHistoryÍ..........................V2I2XZTfon9ts+ %4I3XZTsym9bQolsT5I4XUtilit9yTmacrosforZsymbQolsfB6I5XAmstexTsym9bQolde nitionsv=7I6XZTen9vironments:m17X6.1oMarginUUstack荍..............................V17X6.2oUtilityUUmacrosforZenvironments..................V18o6.2.1F*ormatUUandcontrolmacrosi..................V18X6.3oMacrosUUformarginsͲ...........................V19X6.4oMacrosUUfordrawingbGoxes"獍.......................V19X6.5oMacrosUUforsettingupZenvironments<................V20X6.6oSpacingUUcommands ...........................V20X6.7oEnvironment-breakingUUcommands2...................V21I7XUtilit9yTmacrosforObject-ZK21I8XNon-bQo9xTenvironments]22X8.1oBoxedUUenvironments..........................V23X8.2oOtherUUenvironments*..........................V24!čI1aLIntros3ductionIThisUU leprovidesmacrostotypGeOb8jectZschemas.IX-ffr @ -:q% cmsy6L|{Ycmr8ThisX lehasvÎersionnumb\sdefto\varsdef,yD\sdef&\defsto^Spivey'sUUlatest|PKh27UUMay90^added\c{n}{text}|atablike\t{n}withtext^atUUleft|PKh29UUMay90^added``corners'tobGoxesand\zedcornerheight^|UUPKh11UUJul90^addedj\rename*[y/x]and\zseq?\zset...,^changedUU\zeq\zimp|PKh2UUAug90^addedUUsubseq|PKh9UUNov90^changedSh\MS'tohopGefullyinteractbGetterwithspac-^ingUU|PKh24UUF*eb92^changedUUtoworkwithNFSS|SebastianRahtzh29UUDec92^changedtoworkwithNFSS2|SebastianRahtzh23UUDec93^checkedUUfor\LaTeXeh6UUJan94^checkedagainfor\LaTeXewithhelpofDavid^Carlisleh7UUApr94^checkedUUagain,bundle lesaddedh13UUAug94^removed]hard-wirednumbGer]offamilyformath^letters^removedK?de nitionof\casitpreventsK?cedilla^fromUUworkingh22UUF*eb95^upGdated:'forAMSLaT*eX: 2.1andLucidacompat-^ibility#qǍIPleasecpGostanyupdatesthatyoumaymaketothis leto:3PaulKing{ACSnet: Iking@batserver.cs.uq.oz.auLsٓRcmr71S# cmsy9h$ow cmss9pack9age#g i3ǠsoLs2S ߤN cmtt9\NeedsTeXFormat{LaTeX2e}[1994/12/01] Ls3S\ProvidesPackage{oz}[\filedate\space\fileversion\spaceObjectZmacros]SIThe L5ffA͉TU>'ExX2 b> cmmi10"-}²parbGox codeismuchmorecomplicated,Dsowegetbackasimpler IworldUUfromL5ffA͉TU>'ExX209. ܍Ls4S\def\oz@parbox{\@ifnextchar[{\oz@iparbox}{\oz@iparbox[c]}}Ls5S\long\def\oz@iparbox[#1]#2#3{\leavevmode\@pboxswfalseLs6ap\if#1b\vboxLs7kJ\else\if#1t\vtopLs8\else\vboxLs9%\ifmmode\vcenter\else\@pboxswtrue$\vcenter\fiI10 \fiI11f\fiI12S{\hsize#2\@parboxrestore#3}I13%\if@pboxsw\m@th$\fiI14S} ǘI2aLZfffontsITheAMSextrasymbGolfontsareloadedifwearenotusingLucidaNewMath.INote:msamtYandmsbmsometimescalledeuxmandeuymrespGectivelyNOTE:Ithe-newAMSFONTS!2.0callthesefontsmsamandmsbmrepGectively(thefontsIbGelowUUneedtoberenamedifyouwanttousethenewfonts)SI15S\@ifpackageloaded{lucbr}{}{%I16S\DeclareMathVersion{oz}I17S\SetMathAlphabet{\mathrm}{oz}{\encodingdefault}{\rmdefault}{m}{n}%I18S\SetMathAlphabet{\mathbf}{oz}{\encodingdefault}{\rmdefault}{bx}{n}%I19S\SetMathAlphabet{\mathsf}{oz}{\encodingdefault}{\sfdefault}{m}{n}%I20S\DeclareSymbolFont{italics}{\encodingdefault}{\rmdefault}{m}{it}%I21S\DeclareSymbolFontAlphabet{\mathrm}{operators}I22S\DeclareSymbolFontAlphabet{\mathit}{letters}I23S\DeclareSymbolFontAlphabet{\mathcal}{symbols}I24S\DeclareSymbolFontAlphabet{\ozit}{italics}I25S\DeclareSymbolFont{lasy}{U}{lasy}{m}{n}I26S\DeclareSymbolFont{AMSa}{U}{msa}{m}{n}I27S\DeclareSymbolFont{AMSb}{U}{msb}{m}{n}I28S\let\mho\undefinedI29S\let\Join\undefinedI30S\let\Box\undefinedI31S\let\Diamond\undefinedI32S\let\leadsto\undefinedI33S\let\sqsubset\undefinedI34S\let\sqsupset\undefinedI35S\let\lhd\undefinedI36S\let\unlhd\undefinedI37S\let\rhd\undefinedI38S\let\unrhd\undefinedI39S\DeclareMathSymbol{\mho}{\mathord}{lasy}{"30}I40S\DeclareMathSymbol{\Join}{\mathrel}{lasy}{"31}I41S\DeclareMathSymbol{\Box}{\mathord}{lasy}{"32}I42S\DeclareMathSymbol{\Diamond}{\mathord}{lasy}{"33}I43S\DeclareMathSymbol{\leadsto}{\mathrel}{lasy}{"3B}I44S\DeclareMathSymbol{\sqsubset}{\mathrel}{lasy}{"3C}4soI45S\DeclareMathSymbol{\sqsupset}{\mathrel}{lasy}{"3D} I46S\DeclareMathSymbol{\lhd}{\mathrel}{lasy}{"01}I47S\DeclareMathSymbol{\unlhd}{\mathrel}{lasy}{"02}I48S\DeclareMathSymbol{\rhd}{\mathrel}{lasy}{"03}I49S\DeclareMathSymbol{\unrhd}{\mathrel}{lasy}{"04}I50S\DeclareSymbolFontAlphabet{\mathbb}{AMSb}I51S\mathversion{oz}I52S}XAllow-changeofsizewithinschemas.UOThisisasoGdtogetright;myprinciple I(eventually!)AwasEDtogooutofmathtempGorarily*,?changesize,gointoaninnerImath,UUdothebusiness,thengetoutofmathandbacktooutermath.I53S\newbox\strutbox@ I54S\def\strut@{\copy\strutbox@}I55S\addto@hook\every@math@size{%I56f\setbox\strutbox@\hbox{\lower.5\normallineskiplimitI57XdD\vbox{\kern-\normallineskiplimit\copy\strutbox}}}I58S\def\bBigg@#1#2{%I59S\mbox{\ifcase#1\or\large\or\Large\or\LARGE\or\small\or\footnotesize\fiI60S$#2$}\nulldelimiterspace\z@\m@th}I61S\addto@hook\every@math@size{\setbox\z@\vbox{\hbox{$($}\kern\z@}%I62]\big@size1.2\ht\z@}I63S\newdimen\big@sizeI64S\def\zBIG{\bBigg@{3}}I65S\def\zBig{\bBigg@{2}}I66S\def\zbig{\bBigg@{1}}I67S\def\zsmall{\bBigg@{4}}I68S\def\zSmall{\bBigg@{5}}XWORDCSTYLEStheseCneedhandlingabitdi erentlyinNFSSCfromtheorig- Iinal.I69S\def\String#1{\hbox{`\texttt{#1}'}}I70S\def\STRING#1{\hbox{``\texttt{#1}''}}I71S\def\infix#1{\z@rel{{\underline{#1}}}}I72S\def\word#1{\z@op{#1}}I73S\def\keyword#1{\z@op{\mbox{\textrm{#1}}}}I74S\def\boldword#1{\z@op{\mbox{\textbf{#1}}}}I75S\def\underword#1{\z@op{{\underline{#1}}}}I76S\def\underkeyword#1{\z@op{{\underline{\mbox{\textrm{#1}}}}}}I77S\def\underboldword#1{\z@op{{\underline{\mbox{\textbf{#1}}}}}} I3aLZffsymbs3olsIThe1NmathcoGdesforthelettersA,...,8Z,a,...,zarechangedtogeneratetextitalicIrather*thanmathitalicbydefault.SThismakesmulti-letteridenti ersloGokbetter.IThemathcoGdeforcharactercissetto"7000(vqariablefamily)+"400(textitalic)I+UUc.I78S\def\@setmcodes#1#2#3{{\count0=#1\count1=#3I79f\loop\global\mathcode\count0=\count1\ifnum\count0<#2I80f\advance\count0by1\advance\count1by1\repeat}}IUseq3\hexnumber@\symitalicsincaseotherfamiliesareloadedbGefore.`(fromD.IRoGegel,UUJuly13,1994)5+XsoI81S\@setmcodes{`A}{`Z}{"7\hexnumber@\symitalics41} I82S\@setmcodes{`a}{`z}{"7\hexnumber@\symitalics61}nXAlso,the+mathcoGdeforsemicolonissetto"8000,soitbGehaves+asanactive Icharacter5inmathmoGde;itisde nedtoinsertathickspace.\semicolonisaIsemicolonUUasanordinarysymbGol.܍I83S\let\@mc=\mathchardefI84S\mathcode`\;="8000%Makes;activeinmathmodeI85S{\catcode`\;=\active\gdef;{\semicolon\;}}I86S\@mc\semicolon="603B NI4aLUtilityffmacrosforZsymbs3ols"3獍dO\z@opzmakesUUalargemathopGeratorO\z@relzmakesUUamathrelationO\z@binzmakesUUabinaryopGeratorqǍXEach$euseamathstruttodefeatT*eX'sverticaladjustment.aw\z@bigXXX$XisabigIversionUUofsymbGol܍I87S\def\z@op#1{\mathop{\mathstrut{#1}}\nolimits}I88S\def\z@bin#1{\mathbin{\mathstrut{#1}}}I89S\def\z@rel#1{\mathrel{\mathstrut{#1}}}I90S%I91S\def\z@bigop#1{\z@op{\zbig{#1}}}I92S\def\z@bigbin#1{\z@bin{\zbig{#1}}}I93S\def\z@bigrel#1{\z@rel{\zbig{#1}}}I94S%I95S\def\z@Bigop#1{\z@op{\zBig{#1}}}I96S\def\z@Bigbin#1{\z@bin{\zBig{#1}}}I97S\def\z@Bigrel#1{\z@rel{\zBig{#1}}}I98S%I99S\def\z@smallop#1{\z@op{\zsmall{#1}}}E100S\def\z@smallbin#1{\z@bin{\zsmall{#1}}}E101S\def\z@smallrel#1{\z@rel{\zsmall{#1}}}܍XThisunderscoredoGesn'thavethelittlekern|yougetanitaliccorrectionIanywayUUinmathmoGde. nE102S\def\_{\leavevmode\vbox{\hrulewidth0.4em}}nISaveUU\qas\xqforquanti ersq.E103S\let\xforall=\forallE104S\let\xexists=\existsE105S\let\xlambda=\lambdaE106S\let\xmu=\munISaveUUothersymbGolsE107S\let\xsucc\succE108S\let\xprec\precE109S\let\dotaccent=\dotE110S\let\sectionsymbol=\SE111S\let\integral=\intE112S\let\product\prodnI\pUUand\fmakearrowswith1and2crossingsresp.E113S\def\p#1{\mathrel{\ooalign{\hfil$\mapstochar\mkern5mu$\hfil\cr$#1$}}}66soE114S\def\f#1{\mathrel{\ooalign{\hfil E115f$\mapstochar\mkern3mu\mapstochar\mkern5mu$\hfil\cr$#1$}}}E116S\@ifpackageloaded{lucbr}{%E117XdD\DeclareMathSymbol{\doublebarwedge}{\mathbin}{symbols}{"D4}E118XdD\DeclareMathSymbol{\lll}{\mathrel}{letters}{"DE}E119XdD\DeclareMathSymbol{\ggg}{\mathrel}{letters}{"DF}E120XdD\DeclareMathSymbol{\eth}{\mathrel}{operators}{"F0}E121S}{%!čI5aLAmstexffsymbs3olde nitionsIDothesebGeforeZ{symbolssothatwecanusetheminourspecialsymbols.QAMSa Ifont:E122S\let\rightleftharpoons\undefinedE123S\let\angle\undefinedE124S\DeclareMathSymbol\boxdot{\mathbin}{AMSa}{"00}E125S\DeclareMathSymbol\boxplus{\mathbin}{AMSa}{"01}E126S\DeclareMathSymbol\boxtimes{\mathbin}{AMSa}{"02}E127S\DeclareMathSymbol\square{\mathord}{AMSa}{"03}E128S\DeclareMathSymbol\blacksquare{\mathord}{AMSa}{"04}E129S\DeclareMathSymbol\centerdot{\mathbin}{AMSa}{"05}E130S\DeclareMathSymbol\lozenge{\mathord}{AMSa}{"06}E131S\DeclareMathSymbol\blacklozenge{\mathord}{AMSa}{"07}E132S\DeclareMathSymbol\circlearrowright{\mathrel}{AMSa}{"08}E133S\DeclareMathSymbol\circlearrowleft{\mathrel}{AMSa}{"09}E134S\DeclareMathSymbol\rightleftharpoons{\mathrel}{AMSa}{"0A}E135S\DeclareMathSymbol\leftrightharpoons{\mathrel}{AMSa}{"0B}E136S\DeclareMathSymbol\boxminus{\mathbin}{AMSa}{"0C}E137S\DeclareMathSymbol\Vdash{\mathrel}{AMSa}{"0D}E138S\DeclareMathSymbol\Vvdash{\mathrel}{AMSa}{"0E}E139S\DeclareMathSymbol\vDash{\mathrel}{AMSa}{"0F}E140S\DeclareMathSymbol\twoheadrightarrow{\mathrel}{AMSa}{"10}E141S\DeclareMathSymbol\twoheadleftarrow{\mathrel}{AMSa}{"11}E142S\DeclareMathSymbol\leftleftarrows{\mathrel}{AMSa}{"12}E143S\DeclareMathSymbol\rightrightarrows{\mathrel}{AMSa}{"13}E144S\DeclareMathSymbol\upuparrows{\mathrel}{AMSa}{"14}E145S\DeclareMathSymbol\downdownarrows{\mathrel}{AMSa}{"15}E146S\DeclareMathSymbol\upharpoonright{\mathrel}{AMSa}{"16}E147S\DeclareMathSymbol\downharpoonright{\mathrel}{AMSa}{"17}E148S\DeclareMathSymbol\upharpoonleft{\mathrel}{AMSa}{"18}E149S\DeclareMathSymbol\downharpoonleft{\mathrel}{AMSa}{"19}E150S\DeclareMathSymbol\rightarrowtail{\mathrel}{AMSa}{"1A}E151S\DeclareMathSymbol\leftarrowtail{\mathrel}{AMSa}{"1B}E152S\DeclareMathSymbol\leftrightarrows{\mathrel}{AMSa}{"1C}E153S\DeclareMathSymbol\rightleftarrows{\mathrel}{AMSa}{"1D}E154S\DeclareMathSymbol\Lsh{\mathrel}{AMSa}{"1E}E155S\DeclareMathSymbol\Rsh{\mathrel}{AMSa}{"1F}E156S\DeclareMathSymbol\rightsquigarrow{\mathrel}{AMSa}{"20}E157S\DeclareMathSymbol\leftrightsquigarrow{\mathrel}{AMSa}{"21}E158S\DeclareMathSymbol\looparrowleft{\mathrel}{AMSa}{"22}E159S\DeclareMathSymbol\looparrowright{\mathrel}{AMSa}{"23}E160S\DeclareMathSymbol\circeq{\mathrel}{AMSa}{"24}E161S\DeclareMathSymbol\succsim{\mathrel}{AMSa}{"25}7@soE162S\DeclareMathSymbol\gtrsim{\mathrel}{AMSa}{"26} E163S\DeclareMathSymbol\gtrapprox{\mathrel}{AMSa}{"27}E164S\DeclareMathSymbol\multimap{\mathrel}{AMSa}{"28}E165S\DeclareMathSymbol\therefore{\mathrel}{AMSa}{"29}E166S\DeclareMathSymbol\because{\mathrel}{AMSa}{"2A}E167S\DeclareMathSymbol\doteqdot{\mathrel}{AMSa}{"2B}E168S\DeclareMathSymbol\triangleq{\mathrel}{AMSa}{"2C}E169S\DeclareMathSymbol\precsim{\mathrel}{AMSa}{"2D}E170S\DeclareMathSymbol\lesssim{\mathrel}{AMSa}{"2E}E171S\DeclareMathSymbol\lessapprox{\mathrel}{AMSa}{"2F}E172S\DeclareMathSymbol\eqslantless{\mathrel}{AMSa}{"30}E173S\DeclareMathSymbol\eqslantgtr{\mathrel}{AMSa}{"31}E174S\DeclareMathSymbol\curlyeqprec{\mathrel}{AMSa}{"32}E175S\DeclareMathSymbol\curlyeqsucc{\mathrel}{AMSa}{"33}E176S\DeclareMathSymbol\preccurlyeq{\mathrel}{AMSa}{"34}E177S\DeclareMathSymbol\leqq{\mathrel}{AMSa}{"35}E178S\DeclareMathSymbol\leqslant{\mathrel}{AMSa}{"36}E179S\DeclareMathSymbol\lessgtr{\mathrel}{AMSa}{"37}E180S\DeclareMathSymbol\backprime{\mathord}{AMSa}{"38}E181S\DeclareMathSymbol\risingdotseq{\mathrel}{AMSa}{"3A}E182S\DeclareMathSymbol\fallingdotseq{\mathrel}{AMSa}{"3B}E183S\DeclareMathSymbol\succcurlyeq{\mathrel}{AMSa}{"3C}E184S\DeclareMathSymbol\geqq{\mathrel}{AMSa}{"3D}E185S\DeclareMathSymbol\geqslant{\mathrel}{AMSa}{"3E}E186S\DeclareMathSymbol\gtrless{\mathrel}{AMSa}{"3F}E187S\DeclareMathSymbol\sqsubset{\mathrel}{AMSa}{"40}E188S\DeclareMathSymbol\sqsupset{\mathrel}{AMSa}{"41}E189S\DeclareMathSymbol\vartriangleright{\mathrel}{AMSa}{"42}E190S\DeclareMathSymbol\vartriangleleft{\mathrel}{AMSa}{"43}E191S\DeclareMathSymbol\trianglerighteq{\mathrel}{AMSa}{"44}E192S\DeclareMathSymbol\trianglelefteq{\mathrel}{AMSa}{"45}E193S\DeclareMathSymbol\bigstar{\mathord}{AMSa}{"46}E194S\DeclareMathSymbol\between{\mathrel}{AMSa}{"47}E195S\DeclareMathSymbol\blacktriangledown{\mathord}{AMSa}{"48}E196S\DeclareMathSymbol\blacktriangleright{\mathrel}{AMSa}{"49}E197S\DeclareMathSymbol\blacktriangleleft{\mathrel}{AMSa}{"4A}E198S\DeclareMathSymbol\vartriangle{\mathord}{AMSa}{"4D}E199S\DeclareMathSymbol\blacktriangle{\mathord}{AMSa}{"4E}E200S\DeclareMathSymbol\triangledown{\mathord}{AMSa}{"4F}E201S\DeclareMathSymbol\eqcirc{\mathrel}{AMSa}{"50}E202S\DeclareMathSymbol\lesseqgtr{\mathrel}{AMSa}{"51}E203S\DeclareMathSymbol\gtreqless{\mathrel}{AMSa}{"52}E204S\DeclareMathSymbol\lesseqqgtr{\mathrel}{AMSa}{"53}E205S\DeclareMathSymbol\gtreqqless{\mathrel}{AMSa}{"54}E206S\DeclareMathSymbol\Rrightarrow{\mathrel}{AMSa}{"56}E207S\DeclareMathSymbol\Lleftarrow{\mathrel}{AMSa}{"57}E208S\DeclareMathSymbol\veebar{\mathbin}{AMSa}{"59}E209S\DeclareMathSymbol\barwedge{\mathbin}{AMSa}{"5A}E210S\DeclareMathSymbol\doublebarwedge{\mathbin}{AMSa}{"5B}E211S\DeclareMathSymbol\angle{\mathord}{AMSa}{"5C}E212S\DeclareMathSymbol\measuredangle{\mathord}{AMSa}{"5D}E213S\DeclareMathSymbol\sphericalangle{\mathord}{AMSa}{"5E}E214S\DeclareMathSymbol\varpropto{\mathrel}{AMSa}{"5F}E215S\DeclareMathSymbol\smallsmile{\mathrel}{AMSa}{"60}8 NsoE216S\DeclareMathSymbol\smallfrown{\mathrel}{AMSa}{"61} E217S\DeclareMathSymbol\Subset{\mathrel}{AMSa}{"62}E218S\DeclareMathSymbol\Supset{\mathrel}{AMSa}{"63}E219S\DeclareMathSymbol\Cup{\mathbin}{AMSa}{"64}E220S\DeclareMathSymbol\Cap{\mathbin}{AMSa}{"65}E221S\DeclareMathSymbol\curlywedge{\mathbin}{AMSa}{"66}E222S\DeclareMathSymbol\curlyvee{\mathbin}{AMSa}{"67}E223S\DeclareMathSymbol\leftthreetimes{\mathbin}{AMSa}{"68}E224S\DeclareMathSymbol\rightthreetimes{\mathbin}{AMSa}{"69}E225S\DeclareMathSymbol\subseteqq{\mathrel}{AMSa}{"6A}E226S\DeclareMathSymbol\supseteqq{\mathrel}{AMSa}{"6B}E227S\DeclareMathSymbol\bumpeq{\mathrel}{AMSa}{"6C}E228S\DeclareMathSymbol\Bumpeq{\mathrel}{AMSa}{"6D}E229S\DeclareMathSymbol\lll{\mathrel}{AMSa}{"6E}E230S\DeclareMathSymbol\ggg{\mathrel}{AMSa}{"6F}E231S\DeclareMathDelimiter\ulcorner{4}{AMSa}{"70}{AMSa}{"70}E232S\DeclareMathDelimiter\urcorner{5}{AMSa}{"71}{AMSa}{"71}E233S\DeclareMathDelimiter\llcorner{4}{AMSa}{"78}{AMSa}{"78}E234S\DeclareMathDelimiter\lrcorner{5}{AMSa}{"79}{AMSa}{"79}E235S\xdef\yen s,{\noexpand\mathhexbox\hexnumber@\symAMSa55}E236S\xdef\checkmark{\noexpand\mathhexbox\hexnumber@\symAMSa58}E237S\xdef\circledR{\noexpand\mathhexbox\hexnumber@\symAMSa72}E238S\xdef\maltese s,{\noexpand\mathhexbox\hexnumber@\symAMSa7A}E239S\DeclareMathSymbol\circledS{\mathord}{AMSa}{"73}E240S\DeclareMathSymbol\pitchfork{\mathrel}{AMSa}{"74}E241S\DeclareMathSymbol\dotplus{\mathbin}{AMSa}{"75}E242S\DeclareMathSymbol\backsim{\mathrel}{AMSa}{"76}E243S\DeclareMathSymbol\backsimeq{\mathrel}{AMSa}{"77}E244S\DeclareMathSymbol\complement{\mathord}{AMSa}{"7B}E245S\DeclareMathSymbol\intercal{\mathbin}{AMSa}{"7C}E246S\DeclareMathSymbol\circledcirc{\mathbin}{AMSa}{"7D}E247S\DeclareMathSymbol\circledast{\mathbin}{AMSa}{"7E}E248S\DeclareMathSymbol\circleddash{\mathbin}{AMSa}{"7F}XAMSbUUfont:E249S\DeclareMathSymbol\lvertneqq{\mathrel}{AMSb}{"00}E250S\DeclareMathSymbol\gvertneqq{\mathrel}{AMSb}{"01}E251S\DeclareMathSymbol\nleq{\mathrel}{AMSb}{"02}E252S\DeclareMathSymbol\ngeq{\mathrel}{AMSb}{"03}E253S\DeclareMathSymbol\nless{\mathrel}{AMSb}{"04}E254S\DeclareMathSymbol\ngtr{\mathrel}{AMSb}{"05}E255S\DeclareMathSymbol\nprec{\mathrel}{AMSb}{"06}E256S\DeclareMathSymbol\nsucc{\mathrel}{AMSb}{"07}E257S\DeclareMathSymbol\lneqq{\mathrel}{AMSb}{"08}E258S\DeclareMathSymbol\gneqq{\mathrel}{AMSb}{"09}E259S\DeclareMathSymbol\nleqslant{\mathrel}{AMSb}{"0A}E260S\DeclareMathSymbol\ngeqslant{\mathrel}{AMSb}{"0B}E261S\DeclareMathSymbol\lneq{\mathrel}{AMSb}{"0C}E262S\DeclareMathSymbol\gneq{\mathrel}{AMSb}{"0D}E263S\DeclareMathSymbol\npreceq{\mathrel}{AMSb}{"0E}E264S\DeclareMathSymbol\nsucceq{\mathrel}{AMSb}{"0F}E265S\DeclareMathSymbol\precnsim{\mathrel}{AMSb}{"10}E266S\DeclareMathSymbol\succnsim{\mathrel}{AMSb}{"11}E267S\DeclareMathSymbol\lnsim{\mathrel}{AMSb}{"12}9 ]:soE268S\DeclareMathSymbol\gnsim{\mathrel}{AMSb}{"13} E269S\DeclareMathSymbol\nleqq{\mathrel}{AMSb}{"14}E270S\DeclareMathSymbol\ngeqq{\mathrel}{AMSb}{"15}E271S\DeclareMathSymbol\precneqq{\mathrel}{AMSb}{"16}E272S\DeclareMathSymbol\succneqq{\mathrel}{AMSb}{"17}E273S\DeclareMathSymbol\precnapprox{\mathrel}{AMSb}{"18}E274S\DeclareMathSymbol\succnapprox{\mathrel}{AMSb}{"19}E275S\DeclareMathSymbol\lnapprox{\mathrel}{AMSb}{"1A}E276S\DeclareMathSymbol\gnapprox{\mathrel}{AMSb}{"1B}E277S\DeclareMathSymbol\nsim{\mathrel}{AMSb}{"1C}E278S\DeclareMathSymbol\ncong{\mathrel}{AMSb}{"1D}E279S%\DeclareMathSymbol\varsubsetneq{\mathrel}{AMSb}{"20}E280S%\DeclareMathSymbol\varsupsetneq{\mathrel}{AMSb}{"21}E281S\DeclareMathSymbol\nsubseteqq{\mathrel}{AMSb}{"22}E282S\DeclareMathSymbol\nsupseteqq{\mathrel}{AMSb}{"23}E283S\DeclareMathSymbol\subsetneqq{\mathrel}{AMSb}{"24}E284S\DeclareMathSymbol\supsetneqq{\mathrel}{AMSb}{"25}E285S%\DeclareMathSymbol\varsubsetneqq{\mathrel}{AMSb}{"26}E286S%\DeclareMathSymbol\varsupsetneqq{\mathrel}{AMSb}{"27}E287S\DeclareMathSymbol\subsetneq{\mathrel}{AMSb}{"28}E288S\DeclareMathSymbol\supsetneq{\mathrel}{AMSb}{"29}E289S\DeclareMathSymbol\nsubseteq{\mathrel}{AMSb}{"2A}E290S\DeclareMathSymbol\nsupseteq{\mathrel}{AMSb}{"2B}E291S\DeclareMathSymbol\nparallel{\mathrel}{AMSb}{"2C}E292S\DeclareMathSymbol\nmid{\mathrel}{AMSb}{"2D}E293S\DeclareMathSymbol\nshortmid{\mathrel}{AMSb}{"2E}E294S\DeclareMathSymbol\nshortparallel{\mathrel}{AMSb}{"2F}E295S\DeclareMathSymbol\nvdash{\mathrel}{AMSb}{"30}E296S\DeclareMathSymbol\nVdash{\mathrel}{AMSb}{"31}E297S\DeclareMathSymbol\nvDash{\mathrel}{AMSb}{"32}E298S\DeclareMathSymbol\nVDash{\mathrel}{AMSb}{"33}E299S\DeclareMathSymbol\ntrianglerighteq{\mathrel}{AMSb}{"34}E300S\DeclareMathSymbol\ntrianglelefteq{\mathrel}{AMSb}{"35}E301S\DeclareMathSymbol\ntriangleleft{\mathrel}{AMSb}{"36}E302S\DeclareMathSymbol\ntriangleright{\mathrel}{AMSb}{"37}E303S\DeclareMathSymbol\nleftarrow{\mathrel}{AMSb}{"38}E304S\DeclareMathSymbol\nrightarrow{\mathrel}{AMSb}{"39}E305S\DeclareMathSymbol\nLeftarrow{\mathrel}{AMSb}{"3A}E306S\DeclareMathSymbol\nRightarrow{\mathrel}{AMSb}{"3B}E307S\DeclareMathSymbol\nLeftrightarrow{\mathrel}{AMSb}{"3C}E308S\DeclareMathSymbol\nleftrightarrow{\mathrel}{AMSb}{"3D}E309S\DeclareMathSymbol\divideontimes{\mathbin}{AMSb}{"3E}E310S\DeclareMathSymbol\varnothing{\mathord}{AMSb}{"3F}E311S\DeclareMathSymbol\mho{\mathord}{AMSb}{"66}E312S\DeclareMathSymbol\eth{\mathord}{AMSb}{"67}E313S\DeclareMathSymbol\eqsim{\mathrel}{AMSb}{"68}E314S\DeclareMathSymbol\beth{\mathord}{AMSb}{"69}E315S\DeclareMathSymbol\gimel{\mathord}{AMSb}{"6A}E316S\DeclareMathSymbol\daleth{\mathord}{AMSb}{"6B}E317S\DeclareMathSymbol\lessdot{\mathrel}{AMSb}{"6C}E318S\DeclareMathSymbol\gtrdot{\mathrel}{AMSb}{"6D}E319S\DeclareMathSymbol\ltimes{\mathbin}{AMSb}{"6E}E320S\DeclareMathSymbol\rtimes{\mathbin}{AMSb}{"6F}E321S\DeclareMathSymbol\shortmid{\mathrel}{AMSb}{"70}10 kJsoE322S\DeclareMathSymbol\shortparallel{\mathrel}{AMSb}{"71} E323S\DeclareMathSymbol\smallsetminus{\mathbin}{AMSb}{"72}E324S\DeclareMathSymbol\thicksim{\mathrel}{AMSb}{"73}E325S\DeclareMathSymbol\thickapprox{\mathrel}{AMSb}{"74}E326S\DeclareMathSymbol\approxeq{\mathrel}{AMSb}{"75}E327S\DeclareMathSymbol\succapprox{\mathrel}{AMSb}{"76}E328S\DeclareMathSymbol\precapprox{\mathrel}{AMSb}{"77}E329S\DeclareMathSymbol\curvearrowleft{\mathrel}{AMSb}{"78}E330S\DeclareMathSymbol\curvearrowright{\mathrel}{AMSb}{"79}E331S\DeclareMathSymbol\digamma{\mathord}{AMSb}{"7A}E332S\DeclareMathSymbol\varkappa{\mathord}{AMSb}{"7B}E333S\DeclareMathSymbol\hslash{\mathord}{AMSb}{"7D}E334S\DeclareMathSymbol\hbar{\mathord}{AMSb}{"7E}E335S\DeclareMathSymbol\backepsilon{\mathrel}{AMSb}{"7F}E336S}E337S\def\interleave{{\parallel\!\!\vert}}E338S\def\shortinterleave{\z@rel{\mathord\shortmid\mathord\shortparallel}}E339S\def\napprox{\not\approx}E340S\let\restriction\upharpoonrightE341S\let\Doteq\doteqdotE342S\let\doublecup\CupE343S\let\llless\lllE344S\let\gggtr\gggE345S\let\doublecap\CapINumbGersE346S\def\nat,{{\mathbbN}}E347S\def\integer,{{\mathbbZ}}E348S\def\natoneX{{\mathbbN}_1}E349S\def\real s,{{\mathbbR}}E350S\def\bool s,{{\mathbbB}}E351S\let\divides,\divE352S\def\div,{\z@bin{\mathrm{div}}}E353S\def\mod,{\z@bin{\mathrm{mod}}}E354S\def\succ s,{\word{succ}}E355S\def\expon{^}IaliasesE356S\let\num,\integerE357S\let\nplus\natoneILogicE358S\def\lnot s,{\neg\;}E359S\def\land s,{\z@rel{\wedge}}E360S\def\lor,{\z@rel{\vee}}E361S\let\imp,\RightarrowE362S\let\iffX\LeftrightarrowE363S\def\all,{\z@op{\xforall}}E364S\def\exi,{\z@op{\xexists}}E365S\def\exioneX{\exists_1}E366S\@ifpackageloaded{lucbr}{%E367S\DeclareMathSymbol{\nexi}{0}{arrows}{"20}E368S}{%E369S\DeclareMathSymbol{\nexi}{\mathord}{AMSb}{"40}E370S}11 ysoE371S\def\dot,{\z@rel{\bullet}} E372S\def\true s,{\keyword{true}}E373S\def\false{\keyword{false}}E374S\let\cond s,\rightarrowIaliasesE375S\let\spot s,\dotE376S\mathcode`\@="8000%make@activeinmathmodeE377S{\catcode`\@=\active\gdef@{\dot}}E378S\let\implies,\impE379S\let\forallX\allE380S\let\existsX\exiE381S\let\nexists,\nexiXSETSE382S\let\emptyset s,\varnothingE383S\def\varemptyset s,{\{\,\}}E384S\def\pset s,{\z@op{\mathbbP}}E385S\def\psetone,{\pset_1}E386S\def\fset s,{\z@op{\mathbbF}}E387S\def\fsetone,{\fset_1}E388S\def\sset s,{\z@op{\mathbbS}}E389S\let\mem,\inE390S\def\nem,{\not\mem}E391S\def\uni,{\z@bin\cup}E392S\def\int,{\z@bin\cap}E393S\let\prod s,\timesE394S\def\min,{\word{min}}E395S\def\max,{\word{max}}E396S\def\duni s,{\z@Bigop{\lower0.25ex\hbox{$\uni$}}}E397S\def\dint s,{\z@Bigop{\lower0.25ex\hbox{$\int$}}}E398S\def\upto s,{\z@bin{\ldotp\ldotp}}E399S\let\psubs\subsetE400S\let\subs s,\subseteqE401S\let\psups\supsetE402S\let\sups s,\supseteqE403S\def\diff s,{\z@bin{\backslash}}IaliasesE404S\let\cross\prodE405S\let\notin\nemE406S\let\nmem s,\nemE407S\let\union\uniE408S\let\inter\intE409S\let\power\psetE410S\let\finsetX\fsetE411S\let\dunionX\duniE412S\let\dinterX\dintE413S%IRELA*TIONSUU&FUNCTIONSE414S\def\lambdaX{\z@op{\xlambda}}E415S\def\muX{\z@op{\xmu}}E416S\def\dom,{\keyword{dom}}E417S\def\ran,{\keyword{ran}}12 3soE418S\def\idX{\keyword{id}} E419S\@ifpackageloaded{lucbr}{%E420S\DeclareMathSymbol{\dres}{\mathbin}{letters}{"2F}E421S\DeclareMathSymbol{\rres}{\mathbin}{letters}{"2E}E422S}{%E423S\DeclareMathSymbol{\dres}{\mathbin}{AMSa}{"43}E424S\DeclareMathSymbol{\rres}{\mathbin}{AMSa}{"42}E425S}E426S\def\dsub s,{\mathbin{\rlap{\raise.05ex\hbox{$-$}}{\dres}}}E427S\def\rsub s,{\mathbin{\rlap{\raise.05ex\hbox{$-$}}{\rres}}}E428S\let\fovr s,\oplusE429S\let\cmp,\circE430S\def\fcmp s,{\mathbin{\raise0.6ex\hbox{\oalign{\hfil$\scriptscriptstyleE431kJ\mathrm{o}$\hfil\cr\hfil$\scriptscriptstyle\mathrm{9}$\hfil}}}}E432S\def\inv,{^{-1}}E433S\def\limg s,{(\!|}E434S\def\rimg s,{|\!)}E435S\let\map,\mapstoE436S\let\rel,\leftrightarrowE437S\let\tfun s,\rightarrowE438S\let\tinj s,\rightarrowtailE439S\def\tsur s,{\mathrel{\ooalign{$\tfun$\hfil\cr$\mkern4mu\tfun$}}}E440S\def\pfun s,{\p\tfun}E441S\def\pinj s,{\p\tinj}E442S\def\psur s,{\p\tsur}E443S\def\ffun s,{\f\tfun}E444S\def\finj s,{\f\tinj}E445S\def\bij,{\mathrel{\ooalign{$\tinj$\hfil\cr$\mkern5mu\tfun$}}}E446S\def\tcl,{^+}E447S\def\rtcl s,{^*}E448S\def\iter s,{^}IaliasesE449S\let\comp s,\fcmpE450S\let\ndres\dsubE451S\let\nrres\rsubE452S\let\fun,\tfunE453S\let\inj,\tinjE454S\let\surj s,\tsurE455S\let\psurj\psurE456S\let\lllessX\lllE457S\let\gggtr\gggE458S\def\interleaveX{{\parallel\!\!\vert}}E459S\def\shortinterleave,{\z@rel{\mathord\shortmid\mathord\shortparallel}}E460S\let\restriction,\upharpoonrightE461S\def\napprox,{\not\approx}ISEQUENCESE462S\def\seq,{\keyword{seq}}E463S\def\seqoneX{\seq_1}E464S\def\emptyseq s,{\lseq\,\rseq}E465S\let\lseq s,\langleE466S\let\rseq s,\rangleE467S\def\head s,{\word{head}}E468S\def\tail s,{\word{tail}}13jsoE469S\def\front{\word{front}} E470S\def\last s,{\word{last}}E471S\def\rev,{\word{rev}}E472S\def\squashX{\word{squash}}E473S\def\next s,{\keyword{next}}E474S\def\inseq{\keyword{in}}E475S\@ifpackageloaded{lucbr}{%E476S\DeclareMathSymbol{\sres}{2}{arrows}{"75}E477S\DeclareMathSymbol{\ires}{2}{arrows}{"76}E478S\DeclareMathSymbol{\@@cat}{\mathbin}{operators}{"5F}E479S}{%E480S\DeclareMathSymbol{\@@cat}{\mathbin}{AMSa}{"61}E481S\DeclareMathSymbol{\sres}{\mathbin}{AMSa}{"16}E482S\DeclareMathSymbol{\ires}{\mathbin}{AMSa}{"18}E483S}E484S\def\cat,{\mathbin{\raise0.8ex\hbox{$\mathchar\@@cat$}}}E485S\def\ssub s,{\z@bin{\rlap{$-$}{\sres}}}E486S\def\isub s,{\z@bin{\rlap{$-$}{\ires}}}E487S\def\dcat s,{\z@op{\cat/}}E488S\def\dovr s,{\z@op{\fovr/}}E489S\def\dcmp s,{\z@op{\fcmp/}}E490S\let\prefixX\subseteqE491S\def\suffixX{\keyword{suffix}}E492S\def\seqi s,{\keyword{seq_\infty}}E493S\def\partitionsX{\keyword{partitions}}E494S\def\disjoint s,{\keyword{disjoint}}E495S\def\subseqX{\keyword{subseq}}IaliasesE496S\let\filterX\sresISchemas:E497S\def\lsch s,{\z@bigop{[}} E498S\def\rsch s,{\z@bigop{]}}E499S\def\dparallel{\z@bigop{\parallel}\limits}E500S\def\zand s,{\z@bigbin\land}E501S\def\zor,{\z@bigbin\lor}E502S\def\zcmp s,{\z@bigbin\fcmp}E503S\def\zexi s,{\z@bigop\exists}E504S\def\zall s,{\z@bigop\forall}E505S\def\znot s,{\z@bigop\neg}E506S\def\zbar s,{\z@bigbin\cbar}E507S\def\zfor s,{/}E508S\def\zhide{\z@bigbin\backslash}E509S\def\zimp s,{\z@bigrel\imp}E510S\def\zeq,{\z@bigrel\iff}E511S\def\zovr s,{\z@bigrel\oplus}E512S\def\zpipe{\z@bigbin{\mathord>\!\!\mathord>}}E513S\def\pre,{\keyword{pre}}E514S\def\pred s,{\keyword{pred}}E515S\def\post s,{\keyword{post}}E516S\def\zproject s,{\z@bigbin\sres}E517S\def\rename{\@ifnextchar*{\z@rename}{\z@@rename}}E518S\def\z@rename*[#1/#2]{\left[#1\over#2\right]}E519S\def\z@@rename[#1/#2]{\left[#1\zfor#2\right]}14soIaliases ]E520S\let\project,\zproject E521S\let\importX\sresE522S\let\semi s,\zcmpE523S\let\hide s,\zhide]XBAGS/E524S\let\buni\uplusE525S\def\emptybag s,{\lbag\:\rbag}E526S\def\lbag s,{[\![}E527S\def\rbag s,{]\!]}E528S\def\bag,{\keyword{bag}}E529S\def\items{\word{items}}E530S\let\inbag\inseqE531S\def\bagcount s,{\word{count}}/XDe nitionsUU&declarationsE532S\def\ddef s,{\z@rel{\;::=\;}}E533S\def\bbar s,{\z@bigrel{|}}E534S\let\cbar s,\midE535S\def\lang s,{\langle\!\langle}E536S\def\rang s,{\rangle\!\rangle}E537S\def\sdef s,{\z@rel{\widehat=}}E538S\def\defs s,{\z@smallrel{==}}E539S\def\varsdef,{\z@rel\triangleq}/Ialiases ]E540S\let\sdefs\sdefE541S\mathcode`\|=\midE542S\let\ldata\langE543S\let\rdata\rang]XMISCELLANEOUSE544S\def\lblot{\langle\!|}E545S\def\rblot{|\!\rangle}E546S\def\IMP,{\boldword{Import}}E547S\let\env,\RrightarrowE548S\def\zlet s,{\boldword{let}}E549S\def\zin,{\boldword{in}}E550S\def\zwhereX{\boldword{where}}/XQZEDUUSUPPOR*TE551S\def\HOLE{\z@op{\hbox{$\lll\star\star\star\ggg$}}}E552S\def\landd{}%tosupportqzededitorE553S\def\semid{}%tosupportqzededitorE554S\def\qzed{\ifz@inclass\else\zed\fi}E555S\def\endqzed{\ifz@inclass\else\endzed\fi}/XCLASSESE556S\def\qua{\mbox{::}}E557S\def\redef{\mbox{\textbf{~redef}}}E558S\def\Init{I\!\mbox{\footnotesize\emph{NIT}}}E559S\def\Exit{E\!\mbox{\footnotesize\emph{XIT}}}E560S\def\Internal{I\!\mbox{\footnotesize\emph{NTERNAL}}}E561S\def\Aux{A\!\mbox{\footnotesize\emph{UX}}}E562S\def\intern{\mbox{\textsf{i}}}15soXPROOFSE563S\def\thrm{\z@rel\vdash} E564S\def\qed{\zsmall\Box}E565S\let\Qed\BoxE566S\let\QED\squareE567S\def\BLACKQED{\zsmall\blacksquare}E568S\let\ETH\qedE569S\def\TH{\boldword{Theorem}}E570S\def\LE{\boldword{Lemma}}E571S\def\PR{\boldword{Proof}}E572S\def\refines{\z@rel\sqsupseteq}E573S\def\defines{\z@rel\sqsubseteq}E574S\def\weakrefine{\z@rel{\raise0.2ex\rlap{\hbox{$\sqsupset$}}\lower1ex\hbox{$\sim$}}}E575S\def\weakdefine{\z@rel{\raise0.2ex\rlap{\hbox{$\sqsubset$}}\lower1ex\hbox{$\sim$}}}IaliasesE576S\let\shows\thrmXOBJECTUUTHEOR*YE577S\def\childof{\z@rel\xsucc}E578S\def\parentof{\z@rel\xprec}E579S\let\weaksubclass\succsimE580S\let\weaksupclass\precsimE581S\def\hasa{\z@rel{\mathord\xsucc\!\!\!\mathord\xsucc}}E582S\def\instancein{\z@rel{\mathord\xprec\!\!\!\mathord\xprec}}E583S\def\subtype{\z@rel\sqsubset}E584S\def\subtypeeq{\z@rel\sqsubseteq}E585S\def\suptype{\z@rel\sqsupset}E586S\def\suptypeeq{\z@rel\sqsupseteq}IaliasesE587S\let\inherits\childofE588S\let\subclass\childofE589S\let\isa\childofE590S\let\supclass\parentofE591S\let\instantiates\hasaE592S\let\islikea\weaksubclassXTEMPORALUULOGICE593S\def\atnext{\rlap{$\zSmall\bigcirc$}\kern0.01em\rlap{$\zSmall\bigcirc$}\kern0.01em\zSmall\bigcirc}E594S\def\atlast{\rlap{$\zSmall\bigcirc$}\kern0.01em\rlap{$\zSmall\bigcirc$}\kern0.01em\rlap{$\kern0.01em\mathord-$}\zSmall\bigcirc}E595S\def\always{\lower0.37ex\hbox{$\zbig\Box$}}E596S\def\uptilnow{\rlap{$\kern0.02em\mathord-$}\lower0.37ex\hbox{$\zbig\Box$}}E597S\def\eventually{\lower0.37ex\hbox{$\zbig\Diamond$}}E598S\def\previously{\rlap{$\kern0.04em\mathord-$}\lower0.37ex\hbox{$\zbig\Diamond$}}IaliasesE599S\let\henceforth\alwaysXORDERSE600S\def\mono s,{\keyword{monotonic}}E601S\def\porderX{\keyword{partial\_order}}E602S\def\torderX{\keyword{total\_order}}E603S\newbox\z@combox\newdimen\z@wdcalcE604S\def\comment{\@ifnextchar*{\z@leftcomment}{\z@comment}}16`soE605S\def\z@comment#1{$\z@stopfield\z@addfield\z@startfield$% E606S\global\setbox\z@combox\hbox{\quad[{\sf#1}]}\z@wdcalc=\wd\z@combox%E607S\advance\z@wdcalcby\wd\z@curline\advance\z@wdcalcby\z@curindent%E608S\advance\z@wdcalcby\zedleftsep\advance\z@wdcalcby\zedlinethickness%E609S\advance\z@wdcalcby2\zedindent\ifdim\z@wdcalc>\displaywidth\\%E610S\fi&\box\z@combox\ignorespaces}E611S\def\z@leftcomment*#1{\hbox{[{\sf#1}]}}!čI6aLZffenvironmentsI6.1gMarginstackuTIDe ne=astackofdimensions(50elements)ThiscanprobablybGemadesmaller IwhenUUqzed ltersitsTU>'ExXoutputbGetterE612S\newcount\z@stackminE613S\newcount\z@stackmaxE614S\newcount\z@stacktopE615S\newdimen\@gtempa\z@stackmin=\allocationnumberE616S\newdimen\@gtempa\newdimen\@gtempa\newdimen\@gtempa\newdimen\@gtempaE617S\newdimen\@gtempa\newdimen\@gtempa\newdimen\@gtempa\newdimen\@gtempaE618S\newdimen\@gtempa\newdimen\@gtempa\newdimen\@gtempa\newdimen\@gtempaE619S\newdimen\@gtempa\newdimen\@gtempa\newdimen\@gtempa\newdimen\@gtempaE620S\newdimen\@gtempa\newdimen\@gtempa\newdimen\@gtempa\newdimen\@gtempaE621S\newdimen\@gtempa\newdimen\@gtempa\newdimen\@gtempa\newdimen\@gtempaE622S\newdimen\@gtempa\newdimen\@gtempa\newdimen\@gtempa\newdimen\@gtempaE623S\newdimen\@gtempa\newdimen\@gtempa\newdimen\@gtempa\newdimen\@gtempaE624S\newdimen\@gtempa\newdimen\@gtempa\newdimen\@gtempa\newdimen\@gtempaE625S\newdimen\@gtempa\newdimen\@gtempa\newdimen\@gtempa\newdimen\@gtempaE626S\newdimen\@gtempa\newdimen\@gtempa\newdimen\@gtempa\newdimen\@gtempaE627S\newdimen\@gtempa\newdimen\@gtempa\newdimen\@gtempa\newdimen\@gtempaE628S\newdimen\@gtempaE629S\z@stackmax=\allocationnumberE630S\dimen\z@stackmin=0ptIDe neUUabGoxtocontainthecurrentline&avqariabletocontainit'sindentationE631S\newbox\z@curlineE632S\newdimen\z@curindentE633S\dimen\z@curindent=0ptISpaceUUbGetweenopGerandsofafunctionapplicationE634S\def\z@space{{}\;{}}IDe neUUabGoxtocontainthecurrent eldE635S\newbox\z@curfieldIDe neUUamini-tabbingenvironmentUUforuseinside`zed'E636S\def\z@startline{\setbox\z@curline\hbox{}% E637kJ\global\z@curindent\dimen\z@stacktopE638kJ\z@startfield\ignorespaces}E639S\def\z@stopline{\z@stopfieldE640f\z@addfieldE641f\hbox{\hskip\z@curindent\box\z@curline}}E642E643S\def\z@startfield{\global\setbox\z@curfield\hbox\bgroup}17soE644S\def\z@stopfield{\egroup} E645S\def\z@addfield{\global\setbox\z@curline\hbox{\unhboxE646kJ\z@curline\unhbox\z@curfield}}E647E648S\def\z@pushmargin{\hbox{\kern0pt}$%E649]\z@stopfieldE650]\z@addfieldE651]\ifnum\z@stacktop<\z@stackmaxE652f\global\advance\z@stacktop\@neE653]\elseE654f\@latexerr{Zmarginstackoverflow(toomany\string\M's)}E655f\@ehdE656]\fiE657]\global\dimen\z@stacktop\z@curindentE658]\global\advance\dimen\z@stacktop\wd\z@curlineE659]\z@startfield\ignorespacesE660]$\relax}E661S\def\z@popmargin{\ifnum\z@stacktop>\z@stackminE662f\global\advance\z@stacktop\m@ne\ignorespacesE663]\elseE664f\@latexerr{ZMarginstackunderflow(toomany\string\O's)}E665f\@ehdE666]\fi}E667S\def\M{\z@pushmargin}\def\O{\z@popmargin}\def\S{\z@space}E668S\z@stacktop\z@stackmin6I6.2gUtilitymacrosforZenvironmentsuTIHereSareenvironmentsSforthevqarioussortsofdisplayswhichoGccurinZSrdocuments. IAlldisplaysareset ushleft,&indentedby\zedindent,&bydefault\leftmargini.ISchemas,UUetc,aremadejustwideenoughtogiveequalmarginsleftandright.XSome_environments(schema,etc.)mustonlybGesplitat\zbreak,andothersI(e.g.cargue)L&maybGesplitarbitrarily*.Allgeneratealignmentdisplays,0andpGenaltiesIareUUusedtocontrolpagebreaks.6I6.2.1l#F ormatTandcon9trolmacrosuTE669S\newdimen\zedindent\zedindent=\leftmargini E670S\newdimen\zedleftsepX\zedleftsep=1emE671S\newdimen\zedtabX\zedtab=2emE672S\newdimen\zedbarX\zedbar=8emE673S\newdimen\zedlinethickness s,\zedlinethickness=0.4ptE674S\newdimen\zedcornerheight,\zedcornerheight=0ptE675S\newcount\z@colsE676S\newif\ifz@firstlineX\z@firstlinefalseE677S\newif\ifz@inclass s,\z@inclassfalseE678S\newif\ifz@inenvX\z@inenvfalseE679S\newif\ifz@leftmargin,\z@leftmargintrueE680S\newif\ifz@incols,\z@incolsfalseE681S\newif\ifleftnames s,\leftnamesfalseE682S\def\leftschemas{\leftnamestrue}E683S\newif\ifz@inboxX\z@inboxfalseE684S\newskip\zedbaselineskipX\zedbaselineskip\baselineskip18¤soE685S\newbox\zstrutbox,\setbox\zstrutbox=\copy\strutbox E686S\def\zstrut{\relax\ifmmode\copy\zstrutbox\else\unhcopy\zstrutbox\fi}E687S\def\zedbaselinestretch{1}XPenaltiesE688S\newcount\interzedlinepenalty,\interzedlinepenalty=10000 s,%neverbreakE689S\newcount\preboxpenalty\preboxpenalty=0X%breakeasilyE690S\newcount\forcepagepenalty s,\forcepagepenalty=-10000X%alwaysbreakE691S\interdisplaylinepenalty=100X%breaksometimesXMacrosUUforchangingthesizeofschematextE692S\def\zedsize#1{\def\z@size{#1}}E693S\def\z@size{}E694S\newskip\z@adskip\newskip\z@bdskip\newskip\z@adsskip\newskip\z@bdsskipE695S\def\z@changesize{%E696S\z@adskip\abovedisplayskip\z@bdskip\belowdisplayskip%saveskipsE697S\z@adsskip\abovedisplayshortskip\z@bdsskip\belowdisplayshortskipE698S\z@size%changesizeE699S\abovedisplayskip\z@adskip\belowdisplayskip\z@bdskip%restoreskipsE700S\abovedisplayshortskip\z@adsskip\belowdisplayshortskip\z@bdsskip}E701S%E702S%E703S\def\z@zeroskips{\abovedisplayskip\z@\belowdisplayskip\z@E704f\abovedisplayshortskip\z@\belowdisplayshortskip\z@}拍I6.3gMacrosformarginsuTI\z@narrow,UU\z@wide|makethemarginsnarrower,widerE705S\def\z@narrow{\advance\linewidthby-\zedindent}E706S\def\z@wide{\advance\linewidthby\zedindent}拍I6.4gMacrosfordrawingb`oxesuTI\z@hrulefillUU|linewithcorrectthicknessE707S\def\z@hrulefill{\leaders\hruleheight\zedlinethickness\hfill}X\z@topline8drawsthetophorizontallineofbGoxedenvironments\z@dbltopline Idrawsa/adoubleruledtopline\z@botlinedrawsthebGottomhorizontallineofIbGoxedenvironments\zedline[comment]drawsalonghorizontallineendinginIcommentUU\wheredrawsashorthorizontallineE708S\def\z@topline#1{\omit\@ifnextchar[{\z@@topline{#1}}{\z@@topline{#1}[]}} E709S\def\z@@topline#1[#2]{\hboxto\linewidth{\zstrut\ifleftnames\elseE710f\vruleheight\zedlinethicknesswidth\zedlinethicknessE711f\hboxto\zedleftsep{\z@hrulefill}\fi#1\z@hrulefillE712f\smash{\vruleheight\zedlinethicknesswidth\zedlinethicknessE713fdepth\zedcornerheight}\hbox{\sf#2}}\cr}E714S\def\z@dbltopline#1{\omit\@ifnextchar[{\z@@dbltopline{#1}}{\z@@dbltopline{#1}[]}}E715S\def\z@@dbltopline#1[#2]{\z@@topline{#1}[#2]%E716S\noalign{\kern-\baselineskipE717f\kern-\zedlinethicknessE718f\kern-\doublerulesep\nobreak}%E719S\omit\z@@topline{\hphantom{#1}}[\hphantom{#2}]%E720S\noalign{\kern\doublerulesep19͵soE721f\kern\zedlinethickness\nobreak}} E722S\def\z@botline{\also\omit\hboxto\linewidth{\z@hrulefillE723S\smash{\vruleheight\zedcornerheightwidth\zedlinethicknessE724fdepth0pt}}\cr}E725S\def\z@@botline[#1]{\hboxto\linewidth{\vrule\z@hrulefill\hbox{\sf\smash{#1}}}\also}E726S\def\zedline{\also\omit\@ifnextchar[{\z@@botline}{\z@@botline[]}}E727S\def\where{\also\omit\hboxto\zedbar{\z@hrulefill}\cr\also}E728S\let\STX\whereX\z@leftisplacedattheleftofeachzline:Oinnon-bGoxenvironmentsitwilldo Inothing.inybGoxedenvironmentsitwilldoaverticallinewiththesameheightasItheUUmaximumheightoftheline.E729S\def\z@left{\ifz@inbox\vrulewidth\zedlinethickness\hskip\zedleftsep\fi}6I6.5gMacrosforsettingupZenvironmentsuTE730S\def\z@env{\global\z@firstlinetrue\z@changesize E731f$$E732f\z@inenvtrueE733f\baselineskip\zedbaselineskipE734f\parskip=0pt\lineskip=0pt\z@narrowE735f\advance\displayindentby\zedindentE736f\def\\{\crcr}%Musthave\defandnot\letfornestedalignments.E737f\everycr={\noalign{\ifz@firstline\global\z@firstlinefalseE738f\else\penalty\interzedlinepenalty\fi}}E739f\tabskip=0pt}E740S\def\endz@env{$$E741XdD\global\@ignoretrueE742S}XZܗlinesܺareformatedintwoܺ(overlapping)columns; lthe rst ushlefthaving Ithedsamewidthastheenvironment,and,thedsecond ushrightendingattherightIendUUoftheenvironment.E743S\def\z@format{\halignto\linewidth\bgroup% E744f\zstrut\z@left\z@startline\ignorespaces$\@lign##$\z@stopline\hfil%E745f\tabskip=0ptplus1fil%E746f&\hboxto0pt{\hss\@lign##}\tabskip=0pt\cr}E747S\def\z@boxenv{\z@narrow\let\also=\als@\let\Also=\Als@\let\ALSO=\ALS@E748f\z@inboxtrue\predisplaypenalty=\preboxpenalty\z@env\z@format}E749S\def\z@outnonbox{\z@outclasscheck\z@leavevmode\z@env}E750S\def\z@inoutbox{\z@leavevmode\z@makeouter\z@inclassfalse\z@boxenv}6I6.6gSpacingcommandsuTInoUUverticalgluebGetweenabuttedlinesE751S\def\@but{\noalign{\nointerlineskip}}XnoUU\parextraverticalspacingafterZenvironments X\def\z@nopar{\ifz@inclass\else\vskip-\parskip\fi}8\def\z@nopar{\global\parskip0pt\global\everypar{\parskip30mm\everypar{}}}E752S\def\z@nopar{\global\@endpetrue}X\z@leavevmodek̲{EnterhorizontalmoGde,takingaccountofpGossibleinteractionIwithUUlistsandsectionheads:20soU81.bAftera\item,use\indenttogetthelabGel(thisfailstoruninevenshort blabGels).U82.bAfterUUarun-inheading,use\indent.U83.bAfteranordinaryheading,~throwawaythe\everypartokens,~resetb\@nobreak,UUanduse\noindentwith\parskipzero.U84.bOtherwise,UUuse\noindentwith\parskipzeroIUseUUwhenenteringdisplayedenvironmentstogetcorrectspacingE753S\def\z@leavevmode{\ifvmode\if@inlabel\indent\else\if@noskipsec\indent\else E754f\if@nobreak\global\@nobreakfalse\everypar={}\fiE755f{\parskip=0pt\noindent}\fi\fi\fi}XextraUUverticalspaceinnon-bGoxenvironmentsE756S\def\also{\crcr\noalign{\vskip\jot}}E757S\def\Also{\crcr\noalign{\vskip2\jot}}E758S\def\ALSO{\Also\Also}XextraUUverticalspaceinbGoxedenvironmentsE759S\def\als@{\crcr\@but\omit\vruleheight\jotwidth\zedlinethickness\cr\@but}E760S\def\Als@{\crcr\@but\omit\vruleheight2\jotwidth\zedlinethickness\cr\@but}E761S\def\ALS@{\crcr\@but\omit\vruleheight4\jotwidth\zedlinethickness\cr\@but}6I6.7gEnvironment-breakingcommandsuTE762S\def\znewpage{\also\noalign{\penalty\forcepagepenalty}\also}E763S\def\zbreak{\also\noalign{\penalty\interdisplaylinepenalty\vskip-\jot}\also}E764S\def\Zbreak{\also\noalign{\penalty\interdisplaylinepenalty}\also}E765S\def\ZBREAK{\Also\noalign{\penalty\interdisplaylinepenalty}\Also}E766S\def\t#1{\hskip#1\zedtab}E767S%\def\c#1#2{\hboxto#1\zedtab{$#2$\hfil}}E768S\def\flushr#1{\crcr\quad\cr}!čI7aLUtilityffmacrosforObfject-ZE769S\def\z@inclasscheck{\ifz@inclass\elseE770f\@latexerr{ThisZenvironmentisonlyallowedwithinaclass}E771S{Perhapsyouforgottoincludea\string\begin\string{class\string}E772Ssomewhere^^Joryouaretryingtoprintafilethatneedsupdating.^^J\@ehc}\fi}E773S\def\z@outclasscheck{\ifz@inclassE774f\@latexerr{ThisZenvironmentisnotallowedinsideaclass}E775S{Thisenvironmentdoesn'treallymakesensewithinaclass.^^J%E776SIfyoureallywantitthenI'lltrymybesttofitinin.^^J\@ehc}\elseE777S\ifz@inenv\@latexerr{NewZenvironmentdeclaredbeforepreviousE778Soneiscompleted}E779S{Isuspectthatyou'veforgottentofinishthelastenvironment.^^J%E780SYouaretryingtonestenvironmentsandthiscanonlybedoneinsideclasses^^J%E781Sbesides,theenvironmentyouhavestartedisn'tvalidwithinclassesanyway.^^JIsuggestthatyoutype\spaceX\spacetoquitandthencorrectyourdocument.}E782S\fi\fi}E783S%E784S\def\z@makeouter{%21soE785XdD\ifz@inenv E786ap\ifz@inclass\z@inenvfalseE787f\hskip-\zedleftsep\advance\linewidthby-\zedlinethicknessE788f\zedindent=\zedleftsep\zedleftsep=0.8\zedleftsepE789f\zedbar=0.8\zedbar\zedtab=0.8\zedtabE790f\oz@parbox{\linewidth}\bgroupE791f\z@zeroskipsE792ap\elseE793XdD\@latexerr{IncorrectplaceforZenvironment;nestingisE794]allowedonlyinsideclasses}E795ap{You'veeitherforgottentofinishthelastenvironment,^^J%E796apyou'veforgottentoincludeaE797ap\string\begin\string{class\string}somewhere^^J%E798aporyouaretryingtoprintafilethatneedsupdating.^^J%E799ap(Thenagain,youmightjustbetryingtodosomething^^J%E800fthattheauthorofthesemacrosdidn'tintendyoutodo)^^J\@ehc}E801ap\fiE802XdD\elseE803ap\bgroupE804XdD\fiE805S}E806S%E807S\def\z@makeinner{\egroupE808ap\global\z@curindent\z@E809S}E810S%E811S\def\classbreak{\also\egroup$$\vskip-\ht\zstrutboxE812f\vskip-\abovedisplayskip\vskip-\belowdisplayskip\z@wide\z@boxenv\also}!čI8aLNon-bs3oxffenvironmentsIZEDUUfornon-bGoxmultilineformulasE813S\def\zed{\z@outnonbox\z@inboxfalse\z@format}E814S\def\endzed{\crcr\egroup\endz@env}E815S\let\[=\zedE816S\def\]{\crcr\egroup$$\ignorespaces}XARGUEUUforalgebraicarguments XusedforalgebraicproGofsexpressedasextendedequations."likezedbutwithIextraspacingbGetweenlinesGeneratesanalignmentdisplay*,}whichmaybGesplitIacrossUUpages.E817S\def\argue{\z@outnonbox\interzedlinepenalty=\interdisplaylinepenalty E818f\openup1\jot\z@formatE819f\noalign{\vskip-\jot}}%equalvspaceaboveandbelowarguedisplayE820S\let\endargue=\endzedXINFRULEUUforinferencerules Xused}forinferencerules. ?Thehorizontallineisgeneratedby\derive:anIoptionalUUargumentcontainstheside-conditionsoftherule.E821S\def\infrule{\z@outnonbox\halign\bgroup E822f\zstrut\quad$\@lign##$\quad\hfil&\quad\@lign##\hfil\cr}E823S\let\endinfrule=\endzed22soE824S\def\derive{\crcr\also\@but\omit\z@hrulefill% E825f\@ifnextchar[{\z@sidecondition}{\cr\also\@but}}E826S\def\Derive{\crcr\also\@but\omit\z@hrulefill\cr\@butE827f\noalign{\kern-\dp\zstrutboxE828f\kern\doublerulesep\nobreak}%E829S\omit\derive}E830S\def\z@sidecondition[#1]{&$\smash{\lower0.2ex\hbox{$[\;#1\;]$}}$\cr\also\@but}QuXSYNT*AXUUforsyntaxrules X`syntax'UUenvironment:qusedforsyntaxrules|even(once!)qforVDM. (E831S\def\syntax{\z@outnonbox\halign\bgroupE832f\zstrut$\@lign##$\hfil&\hfil$\@lign{}##{}$\hfilE833f&$\@lign##$\hfil&\qquad\@lign--##\hfil\cr}E834S\let\endsyntax=\endzedD؍I8.1gBoxedenvironmentsuTISCHEMAUUschemade nitionsQuE835S\def\schema#1{\z@inoutbox\z@topline{$\,#1\,$}}E836S\def\endschema{\z@botline\endzed\z@makeinner\z@nopar}XSCHEMA*UUschemawithnonameQuE837S\@namedef{schema*}{\leftnamesfalse\z@inoutbox\z@topline{}}E838S\expandafter\let\csnameendschema*\endcsname=\endschemaXGENSCHEMAUUgenericschemade nitionsQuE839S\def\genschema#1#2{\z@inoutbox\z@topline{$\,#1\:[#2]\,$}}E840S\let\endgenschema=\endschemaXAXDEFUU`libGeral'axiomaticde nitionsQuE841S\def\axdef{\z@inoutbox}E842S\def\endaxdef{\endzed\z@makeinner}XUNIQDEFUU`unique'axiomaticde nitionsQuE843S\def\uniqdef{\leftnamesfalse\z@inoutbox\z@dbltopline{}}E844S\let\enduniqdef=\endschemaXGENDEFUU'generic'axiomaticde nitionsQuE845S\def\gendef#1{\leftnamesfalse\z@inoutbox\z@dbltopline{$\,[#1]\,$}}E846S\let\endgendef=\endschemaXCLASSQuE847S\def\class#1{\z@leavevmode\z@makeouter\z@inclasstrueE848f\z@boxenv\z@topline{$\,#1\,$}}E849S\let\endclass\endschemaXOPQuE850S\def\op{\z@inclasscheck\schema}E851S\let\endop\endschemaXST*ATEQuE852S\def\state{\z@inclasscheck\vbox\bgroup\vskip-\ht\zstrutbox\vbox\bgroup\hbox\bgroup\@nameuse{schema*}}E853S\def\endstate{\endschema\egroup\egroup\egroup}XINITQuE854S\def\init{\z@inclasscheck\schema{\Init}}E855S\let\endinit\endschema23$soI8.2gOtherenvironmentsuTISIDEBYSIDE XThisX}shouldsuppGortanarbitarynumberX}ofcolumns\zedindent'sproportionIofUU\linewidthgivesapracticallimitE856S\def\sidebyside{\@ifnextchar[{\z@columns}{\z@columns[2]}} E857S\def\z@columns[#1]{\z@leavevmode\z@cols#1\z@makeouter\z@narrow%E858f$$\lineskip=0pt\z@incolstrueE859f\predisplaysize\maxdimenE860f\ifz@leftmargin\hskip-\zedindent\z@leftmarginfalse\fiE861f\setbox0=\hboxto\linewidth\bgroup\z@zeroskips%E862f\divide\zedbarby\z@cols\divide\zedleftsepby\z@colsE863f\divide\zedtabby\z@cols\divide\linewidthby\z@colsE864ap\oz@parbox[t]{\linewidth}\bgroup\z@wide}E865S%E866S\def\nextside{\egroup\hss\oz@parbox[t]{\linewidth}\bgroup\z@wide}E867S%E868S\newdimen\z@tempE869S\def\endsidebyside{\egroup\egroupE870f\z@temp\ht0\advance\z@tempby\dp0\advance\z@tempby-\dp\zstrutboxE871f\hbox{\raise\z@temp\box0}\endz@env\z@makeinner\z@nopar}XZP*ARE872S\def\zpar{\z@leavevmodeE873f\ifz@inenv\z@inclasstrue\fi%fudgetoletzparinallboxesE874f\z@makeouter\z@changesizeE875f\advance\linewidthby-\z@curindentE876f\advance\linewidthby-\wd\z@curlineE877f\hskip-\wd\z@curline\advance\linewidthby-\zedindent$$E878f\ifz@leftmargin\hskip-\zedindent\fi%adjustmentforfirstcolumnE879f\advance\displayindentby\zedindentE880f\advance\displaywidthby-\zedindentE881f\advance\displayindentby\z@curindentE882f\advance\displayindentby\wd\z@curlineE883f\advance\displaywidthby-\z@curindentE884f\advance\displaywidthby-\wd\z@curlineE885f\global\setbox\z@curline\hbox{}E886f\z@narrow\oz@parbox[b]{\linewidth}\bgroup\hfil\break}E887S\def\endzpar{\egroup$$\z@makeinner\z@nopar}XCLASSCOME888S\def\classcom{\zpar\sf}E889S\let\endclasscom=\endzparXPROOFE890S\def\proof{\zpar$\PR$\zpar}E891S\def\endproof{\endzpar\endzpar}XAdditionalUUauxiliarymacrosE892S\def\zseq#1{\lseq#1\rseq}E893S\def\zset#1{\{#1\}}E894S\def\zimg#1{\limg#1\rimg}E895S\def\zsch#1{\lsch#1\rsch}E896S\def\zimgset#1{\zimg\zset{#1}}24*soE897S% E898Sh"5" cmmi9=pack9age#g i25; $ow cmss9# cmsy9"5" cmmi9 ߤN cmtt9 cmmi10K`y cmr10ٓRcmr7