; TeX output 1997.09.17:1240so*sDtGGcmr17The7tGGcmss17ozpacqkage!", cmsy10XQ cmr12editedbrySebastianRahtzS.Rahrtz@elsevier.co.uk&37 1997/09/17:ōINff cmbx12ContentsI"V cmbx101XIn9troQduction1 XK`y cmr101.1oMoGdi cationUUHistoryÍ..........................V2I2XZTfon9ts+ %3I3XZTsym9bQolsT5I4XUtilit9yTmacrosforZsymbQolsfB6I5XAmstexTsym9bQolde nitionsv=7I6XObject-ZTNotations17I7XZTen9vironments:m17X7.1oMarginUUstack荍..............................V17X7.2oUtilityUUmacrosforZenvironments..................V19o7.2.1F*ormatUUandcontrolmacrosi..................V19X7.3oMacrosUUformarginsͲ...........................V20X7.4oMacrosUUfordrawingbGoxes"獍.......................V20X7.5oMacrosUUforsettingupZenvironments<................V20X7.6oSpacingUUcommands ...........................V21X7.7oEnvironment-breakingUUcommands2...................V22I8XUtilit9yTmacrosforObject-ZK22I9XNon-bQo9xTenvironments]23X9.1oBoxedUUenvironments..........................V23X9.2oOtherUUenvironments*..........................V25!č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|PKh2UUAug90_addedUU\subseq,\iseq-PKh9UUNov90_changedSh\MS'tohopGefullyinteractbGetterwithspac-_ingUU|PKh18UUDec90_changed#tonewAMS2.0fonts-PK(withhelp_fromUUAdrianLee)2sodh11UUF*eb91added\poly\widenandmoGdi ed\gendef-PK h10UUApr91addedUU\fuzzcompatible-PKh1UUApr91addedUU\gengendef-SteveAtkinsonh24UUF*eb92changedUUtoworkwithNFSS|SebastianRahtzh29UUDec92changedtoworkwithNFSS2|SebastianRahtzh23UUDec93checkedUUfor\LaTeXeh6UUJan94checkedagainfor\LaTeXewithhelpofDavidCarlisleh7UUApr94checkedUUagain,bundle lesaddedh13UUAug94removed]hard-wirednumbGer]offamilyformathlettersremovedK?de nitionof\casitpreventsK?cedillafromUUworkingh22UUF*eb95upGdated:'forAMSLaT*eX: 2.1andLucidacompat-ibilityh30UUAug96addedUUOb8ject-ZnotationsinSection2A-SAh17UUSep97re-addedצ !", cmsy10nzedbaselinestretch(L5ffٓRcmr7A͉TU>'ExX2 b> cmmi10"%S){DavidLeadbGetter{IPleaseUUpGostanyupdatesthatyoumaymaketothis leto: IF*ormalUUMethoGdsGroup{fmg@it.uq.edu.auۃLs1S# cmsy9h$ow cmss9pack9age#g i Ls2S ߤN cmtt9\NeedsTeXFormat{LaTeX2e}[1994/12/01]Ls3S\ProvidesPackage{oz}[\filedate\space\fileversion\spaceObjectZmacros]ۃIThe L5ffA͉TU>'ExX2"-}²parbGox codeismuchmorecomplicated,DsowegetbackasimplerIworldUUfromL5ffA͉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)ۃI15S\@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}%3}soI21S\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}I45S\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\DeclareSymbolFontAlphabet{\bbold}{AMSb}I52S\mathversion{oz}I53S}XAllow-changeofsizewithinschemas.UOThisisasoGdtogetright;myprinciple I(eventually!)AwasEDtogooutofmathtempGorarily*,?changesize,gointoaninnerImath,UUdothebusiness,thengetoutofmathandbacktooutermath.I54S\newbox\strutbox@ I55S\def\strut@{\copy\strutbox@}I56S\addto@hook\every@math@size{%I57f\setbox\strutbox@\hbox{\lower.5\normallineskiplimitI58XdD\vbox{\kern-\normallineskiplimit\copy\strutbox}}}I59I60S%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%I61S%NOTE:bBiggisusedtodefinethefontsizeforzbigetcI62S%howeveritdefinestheseasfixedsizes.I63S%The209definitionssetthefontsizedependentontheI64S%currentpointsize.I65S%I66S%Hencein209youcando\Large\cnjandthesymbolisbiggerI67S%Butin2eitremainsafixedsize!I68S%I69S%ThisisaproblemfortheObject-ZoperatorsasoriginallyI70S%definedinthe209oz.sty`96file.4)3soI71S%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% I72I73S\def\bBigg@#1#2{%I74S\mbox{\ifcase#1\or\large\or\Large\or\LARGE\or\small\or\footnotesize\fiI75S$#2$}\nulldelimiterspace\z@\m@th}I76S\addto@hook\every@math@size{\setbox\z@\vbox{\hbox{$($}\kern\z@}%I77]\big@size1.2\ht\z@}I78S\newdimen\big@sizeI79S\def\zBIG{\bBigg@{3}}I80S\def\zBig{\bBigg@{2}}I81S\def\zbig{\bBigg@{1}}I82S\def\zsmall{\bBigg@{4}}I83S\def\zSmall{\bBigg@{5}}XWORDCSTYLEStheseCneedhandlingabitdi erentlyinNFSSCfromtheorig- Iinal.I84S\def\String#1{\hbox{`\texttt{#1}'}}I85S\def\STRING#1{\hbox{``\texttt{#1}''}}I86S\def\infix#1{\z@rel{{\underline{#1}}}}I87S\def\word#1{\z@op{#1}}I88S\def\keyword#1{\z@op{\mbox{\textrm{#1}}}}I89S\def\boldword#1{\z@op{\mbox{\textbf{#1}}}}I90S\def\underword#1{\z@op{{\underline{#1}}}}I91S\def\underkeyword#1{\z@op{{\underline{\mbox{\textrm{#1}}}}}}I92S\def\underboldword#1{\z@op{{\underline{\mbox{\textbf{#1}}}}}}!čI3aLZffsymbs3olsIThe1NmathcoGdesforthelettersA,...,8Z,a,...,zarechangedtogeneratetextitalicIrather*thanmathitalicbydefault.SThismakesmulti-letteridenti ersloGokbetter.IThemathcoGdeforcharactercissetto"7000(vqariablefamily)+"400(textitalic)I+UUc.I93S\def\@setmcodes#1#2#3{{\count0=#1\count1=#3I94f\loop\global\mathcode\count0=\count1\ifnum\count0<#2I95f\advance\count0by1\advance\count1by1\repeat}}IUseq3\hexnumber@\symitalicsincaseotherfamiliesareloadedbGefore.`(fromD.IRoGegel,UUJuly13,1994)I96S\@setmcodes{`A}{`Z}{"7\hexnumber@\symitalics41}I97S\@setmcodes{`a}{`z}{"7\hexnumber@\symitalics61}XAlso,the+mathcoGdeforsemicolonissetto"8000,soitbGehaves+asanactiveIcharacter5inmathmoGde;itisde nedtoinsertathickspace.\semicolonisaIsemicolonUUasanordinarysymbGol.I98S\let\@mc=\mathchardefI99S\mathcode`\;="8000%Makes;activeinmathmodeE100S{\catcode`\;=\active\gdef;{\semicolon\;}}E101S\@mc\semicolon="603B54soI4aLUtilityffmacrosforZsymbs3ols"3獍dO\z@opzmakesUUalargemathopGerator O\z@relzmakesUUamathrelationO\z@binzmakesUUabinaryopGeratorqǍXEach$euseamathstruttodefeatT*eX'sverticaladjustment.aw\z@bigXXX$Xisabig IversionUUofsymbGolE102S\def\z@op#1{\mathop{\mathstrut{#1}}\nolimits} E103S\def\z@bin#1{\mathbin{\mathstrut{#1}}}E104S\def\z@rel#1{\mathrel{\mathstrut{#1}}}E105S%E106S\def\z@bigop#1{\z@op{\zbig{#1}}}E107S\def\z@bigbin#1{\z@bin{\zbig{#1}}}E108S\def\z@bigrel#1{\z@rel{\zbig{#1}}}E109S%E110S\def\z@Bigop#1{\z@op{\zBig{#1}}}E111S\def\z@Bigbin#1{\z@bin{\zBig{#1}}}E112S\def\z@Bigrel#1{\z@rel{\zBig{#1}}}E113S%E114S\def\z@smallop#1{\z@op{\zsmall{#1}}}E115S\def\z@smallbin#1{\z@bin{\zsmall{#1}}}E116S\def\z@smallrel#1{\z@rel{\zsmall{#1}}}XThisunderscoredoGesn'thavethelittlekern|yougetanitaliccorrectionIanywayUUinmathmoGde.E117S\def\_{\leavevmode\vbox{\hrulewidth0.4em}}ISaveUU\qas\xqforquanti ersq.E118S\let\xforall=\forall E119S\let\xexists=\existsE120S\let\xlambda=\lambdaE121S\let\xmu=\muISaveUUothersymbGolsE122S\let\xsucc\succE123S\let\xprec\precE124S\let\dotaccent=\dotE125S\let\sectionsymbol=\SE126S\let\integral=\intE127S\let\product\prodI\pUUand\fmakearrowswith1and2crossingsresp.E128S\def\p#1{\mathrel{\ooalign{\hfil$\mapstochar\mkern5mu$\hfil\cr$#1$}}}E129S\def\f#1{\mathrel{\ooalign{\hfilE130f$\mapstochar\mkern3mu\mapstochar\mkern5mu$\hfil\cr$#1$}}}E131S\@ifpackageloaded{lucbr}{%E132XdD\DeclareMathSymbol{\doublebarwedge}{\mathbin}{symbols}{"D4}E133XdD\DeclareMathSymbol{\lll}{\mathrel}{letters}{"DE}E134XdD\DeclareMathSymbol{\ggg}{\mathrel}{letters}{"DF}E135XdD\DeclareMathSymbol{\eth}{\mathrel}{operators}{"F0}E136S}{%6?VsoI5aLAmstexffsymbs3olde nitionsIDothesebGeforeZ{symbolssothatwecanusetheminourspecialsymbols.QAMSa Ifont:E137S\let\rightleftharpoons\undefined E138S\let\angle\undefinedE139S\DeclareMathSymbol\boxdot{\mathbin}{AMSa}{"00}E140S\DeclareMathSymbol\boxplus{\mathbin}{AMSa}{"01}E141S\DeclareMathSymbol\boxtimes{\mathbin}{AMSa}{"02}E142S\DeclareMathSymbol\square{\mathord}{AMSa}{"03}E143S\DeclareMathSymbol\blacksquare{\mathord}{AMSa}{"04}E144S\DeclareMathSymbol\centerdot{\mathbin}{AMSa}{"05}E145S\DeclareMathSymbol\lozenge{\mathord}{AMSa}{"06}E146S\DeclareMathSymbol\blacklozenge{\mathord}{AMSa}{"07}E147S\DeclareMathSymbol\circlearrowright{\mathrel}{AMSa}{"08}E148S\DeclareMathSymbol\circlearrowleft{\mathrel}{AMSa}{"09}E149S\DeclareMathSymbol\rightleftharpoons{\mathrel}{AMSa}{"0A}E150S\DeclareMathSymbol\leftrightharpoons{\mathrel}{AMSa}{"0B}E151S\DeclareMathSymbol\boxminus{\mathbin}{AMSa}{"0C}E152S\DeclareMathSymbol\Vdash{\mathrel}{AMSa}{"0D}E153S\DeclareMathSymbol\Vvdash{\mathrel}{AMSa}{"0E}E154S\DeclareMathSymbol\vDash{\mathrel}{AMSa}{"0F}E155S\DeclareMathSymbol\twoheadrightarrow{\mathrel}{AMSa}{"10}E156S\DeclareMathSymbol\twoheadleftarrow{\mathrel}{AMSa}{"11}E157S\DeclareMathSymbol\leftleftarrows{\mathrel}{AMSa}{"12}E158S\DeclareMathSymbol\rightrightarrows{\mathrel}{AMSa}{"13}E159S\DeclareMathSymbol\upuparrows{\mathrel}{AMSa}{"14}E160S\DeclareMathSymbol\downdownarrows{\mathrel}{AMSa}{"15}E161S\DeclareMathSymbol\upharpoonright{\mathrel}{AMSa}{"16}E162S\DeclareMathSymbol\downharpoonright{\mathrel}{AMSa}{"17}E163S\DeclareMathSymbol\upharpoonleft{\mathrel}{AMSa}{"18}E164S\DeclareMathSymbol\downharpoonleft{\mathrel}{AMSa}{"19}E165S\DeclareMathSymbol\rightarrowtail{\mathrel}{AMSa}{"1A}E166S\DeclareMathSymbol\leftarrowtail{\mathrel}{AMSa}{"1B}E167S\DeclareMathSymbol\leftrightarrows{\mathrel}{AMSa}{"1C}E168S\DeclareMathSymbol\rightleftarrows{\mathrel}{AMSa}{"1D}E169S\DeclareMathSymbol\Lsh{\mathrel}{AMSa}{"1E}E170S\DeclareMathSymbol\Rsh{\mathrel}{AMSa}{"1F}E171S\DeclareMathSymbol\rightsquigarrow{\mathrel}{AMSa}{"20}E172S\DeclareMathSymbol\leftrightsquigarrow{\mathrel}{AMSa}{"21}E173S\DeclareMathSymbol\looparrowleft{\mathrel}{AMSa}{"22}E174S\DeclareMathSymbol\looparrowright{\mathrel}{AMSa}{"23}E175S\DeclareMathSymbol\circeq{\mathrel}{AMSa}{"24}E176S\DeclareMathSymbol\succsim{\mathrel}{AMSa}{"25}E177S\DeclareMathSymbol\gtrsim{\mathrel}{AMSa}{"26}E178S\DeclareMathSymbol\gtrapprox{\mathrel}{AMSa}{"27}E179S\DeclareMathSymbol\multimap{\mathrel}{AMSa}{"28}E180S\DeclareMathSymbol\therefore{\mathrel}{AMSa}{"29}E181S\DeclareMathSymbol\because{\mathrel}{AMSa}{"2A}E182S\DeclareMathSymbol\doteqdot{\mathrel}{AMSa}{"2B}E183S\DeclareMathSymbol\triangleq{\mathrel}{AMSa}{"2C}E184S\DeclareMathSymbol\precsim{\mathrel}{AMSa}{"2D}E185S\DeclareMathSymbol\lesssim{\mathrel}{AMSa}{"2E}E186S\DeclareMathSymbol\lessapprox{\mathrel}{AMSa}{"2F}7HsoE187S\DeclareMathSymbol\eqslantless{\mathrel}{AMSa}{"30} E188S\DeclareMathSymbol\eqslantgtr{\mathrel}{AMSa}{"31}E189S\DeclareMathSymbol\curlyeqprec{\mathrel}{AMSa}{"32}E190S\DeclareMathSymbol\curlyeqsucc{\mathrel}{AMSa}{"33}E191S\DeclareMathSymbol\preccurlyeq{\mathrel}{AMSa}{"34}E192S\DeclareMathSymbol\leqq{\mathrel}{AMSa}{"35}E193S\DeclareMathSymbol\leqslant{\mathrel}{AMSa}{"36}E194S\DeclareMathSymbol\lessgtr{\mathrel}{AMSa}{"37}E195S\DeclareMathSymbol\backprime{\mathord}{AMSa}{"38}E196S\DeclareMathSymbol\risingdotseq{\mathrel}{AMSa}{"3A}E197S\DeclareMathSymbol\fallingdotseq{\mathrel}{AMSa}{"3B}E198S\DeclareMathSymbol\succcurlyeq{\mathrel}{AMSa}{"3C}E199S\DeclareMathSymbol\geqq{\mathrel}{AMSa}{"3D}E200S\DeclareMathSymbol\geqslant{\mathrel}{AMSa}{"3E}E201S\DeclareMathSymbol\gtrless{\mathrel}{AMSa}{"3F}E202S\DeclareMathSymbol\sqsubset{\mathrel}{AMSa}{"40}E203S\DeclareMathSymbol\sqsupset{\mathrel}{AMSa}{"41}E204S\DeclareMathSymbol\vartriangleright{\mathrel}{AMSa}{"42}E205S\DeclareMathSymbol\vartriangleleft{\mathrel}{AMSa}{"43}E206S\DeclareMathSymbol\trianglerighteq{\mathrel}{AMSa}{"44}E207S\DeclareMathSymbol\trianglelefteq{\mathrel}{AMSa}{"45}E208S\DeclareMathSymbol\bigstar{\mathord}{AMSa}{"46}E209S\DeclareMathSymbol\between{\mathrel}{AMSa}{"47}E210S\DeclareMathSymbol\blacktriangledown{\mathord}{AMSa}{"48}E211S\DeclareMathSymbol\blacktriangleright{\mathrel}{AMSa}{"49}E212S\DeclareMathSymbol\blacktriangleleft{\mathrel}{AMSa}{"4A}E213S\DeclareMathSymbol\vartriangle{\mathord}{AMSa}{"4D}E214S\DeclareMathSymbol\blacktriangle{\mathord}{AMSa}{"4E}E215S\DeclareMathSymbol\triangledown{\mathord}{AMSa}{"4F}E216S\DeclareMathSymbol\eqcirc{\mathrel}{AMSa}{"50}E217S\DeclareMathSymbol\lesseqgtr{\mathrel}{AMSa}{"51}E218S\DeclareMathSymbol\gtreqless{\mathrel}{AMSa}{"52}E219S\DeclareMathSymbol\lesseqqgtr{\mathrel}{AMSa}{"53}E220S\DeclareMathSymbol\gtreqqless{\mathrel}{AMSa}{"54}E221S\DeclareMathSymbol\Rrightarrow{\mathrel}{AMSa}{"56}E222S\DeclareMathSymbol\Lleftarrow{\mathrel}{AMSa}{"57}E223S\DeclareMathSymbol\veebar{\mathbin}{AMSa}{"59}E224S\DeclareMathSymbol\barwedge{\mathbin}{AMSa}{"5A}E225S\DeclareMathSymbol\doublebarwedge{\mathbin}{AMSa}{"5B}E226S\DeclareMathSymbol\angle{\mathord}{AMSa}{"5C}E227S\DeclareMathSymbol\measuredangle{\mathord}{AMSa}{"5D}E228S\DeclareMathSymbol\sphericalangle{\mathord}{AMSa}{"5E}E229S\DeclareMathSymbol\varpropto{\mathrel}{AMSa}{"5F}E230S\DeclareMathSymbol\smallsmile{\mathrel}{AMSa}{"60}E231S\DeclareMathSymbol\smallfrown{\mathrel}{AMSa}{"61}E232S\DeclareMathSymbol\Subset{\mathrel}{AMSa}{"62}E233S\DeclareMathSymbol\Supset{\mathrel}{AMSa}{"63}E234S\DeclareMathSymbol\Cup{\mathbin}{AMSa}{"64}E235S\DeclareMathSymbol\Cap{\mathbin}{AMSa}{"65}E236S\DeclareMathSymbol\curlywedge{\mathbin}{AMSa}{"66}E237S\DeclareMathSymbol\curlyvee{\mathbin}{AMSa}{"67}E238S\DeclareMathSymbol\leftthreetimes{\mathbin}{AMSa}{"68}E239S\DeclareMathSymbol\rightthreetimes{\mathbin}{AMSa}{"69}E240S\DeclareMathSymbol\subseteqq{\mathrel}{AMSa}{"6A}8 WEsoE241S\DeclareMathSymbol\supseteqq{\mathrel}{AMSa}{"6B} E242S\DeclareMathSymbol\bumpeq{\mathrel}{AMSa}{"6C}E243S\DeclareMathSymbol\Bumpeq{\mathrel}{AMSa}{"6D}E244S\DeclareMathSymbol\lll{\mathrel}{AMSa}{"6E}E245S\DeclareMathSymbol\ggg{\mathrel}{AMSa}{"6F}E246S\DeclareMathDelimiter\ulcorner{4}{AMSa}{"70}{AMSa}{"70}E247S\DeclareMathDelimiter\urcorner{5}{AMSa}{"71}{AMSa}{"71}E248S\DeclareMathDelimiter\llcorner{4}{AMSa}{"78}{AMSa}{"78}E249S\DeclareMathDelimiter\lrcorner{5}{AMSa}{"79}{AMSa}{"79}E250S\xdef\yen s,{\noexpand\mathhexbox\hexnumber@\symAMSa55}E251S\xdef\checkmark{\noexpand\mathhexbox\hexnumber@\symAMSa58}E252S\xdef\circledR{\noexpand\mathhexbox\hexnumber@\symAMSa72}E253S\xdef\maltese s,{\noexpand\mathhexbox\hexnumber@\symAMSa7A}E254S\DeclareMathSymbol\circledS{\mathord}{AMSa}{"73}E255S\DeclareMathSymbol\pitchfork{\mathrel}{AMSa}{"74}E256S\DeclareMathSymbol\dotplus{\mathbin}{AMSa}{"75}E257S\DeclareMathSymbol\backsim{\mathrel}{AMSa}{"76}E258S\DeclareMathSymbol\backsimeq{\mathrel}{AMSa}{"77}E259S\DeclareMathSymbol\complement{\mathord}{AMSa}{"7B}E260S\DeclareMathSymbol\intercal{\mathbin}{AMSa}{"7C}E261S\DeclareMathSymbol\circledcirc{\mathbin}{AMSa}{"7D}E262S\DeclareMathSymbol\circledast{\mathbin}{AMSa}{"7E}E263S\DeclareMathSymbol\circleddash{\mathbin}{AMSa}{"7F}XAMSbUUfont:E264S\DeclareMathSymbol\lvertneqq{\mathrel}{AMSb}{"00}E265S\DeclareMathSymbol\gvertneqq{\mathrel}{AMSb}{"01}E266S\DeclareMathSymbol\nleq{\mathrel}{AMSb}{"02}E267S\DeclareMathSymbol\ngeq{\mathrel}{AMSb}{"03}E268S\DeclareMathSymbol\nless{\mathrel}{AMSb}{"04}E269S\DeclareMathSymbol\ngtr{\mathrel}{AMSb}{"05}E270S\DeclareMathSymbol\nprec{\mathrel}{AMSb}{"06}E271S\DeclareMathSymbol\nsucc{\mathrel}{AMSb}{"07}E272S\DeclareMathSymbol\lneqq{\mathrel}{AMSb}{"08}E273S\DeclareMathSymbol\gneqq{\mathrel}{AMSb}{"09}E274S\DeclareMathSymbol\nleqslant{\mathrel}{AMSb}{"0A}E275S\DeclareMathSymbol\ngeqslant{\mathrel}{AMSb}{"0B}E276S\DeclareMathSymbol\lneq{\mathrel}{AMSb}{"0C}E277S\DeclareMathSymbol\gneq{\mathrel}{AMSb}{"0D}E278S\DeclareMathSymbol\npreceq{\mathrel}{AMSb}{"0E}E279S\DeclareMathSymbol\nsucceq{\mathrel}{AMSb}{"0F}E280S\DeclareMathSymbol\precnsim{\mathrel}{AMSb}{"10}E281S\DeclareMathSymbol\succnsim{\mathrel}{AMSb}{"11}E282S\DeclareMathSymbol\lnsim{\mathrel}{AMSb}{"12}E283S\DeclareMathSymbol\gnsim{\mathrel}{AMSb}{"13}E284S\DeclareMathSymbol\nleqq{\mathrel}{AMSb}{"14}E285S\DeclareMathSymbol\ngeqq{\mathrel}{AMSb}{"15}E286S\DeclareMathSymbol\precneqq{\mathrel}{AMSb}{"16}E287S\DeclareMathSymbol\succneqq{\mathrel}{AMSb}{"17}E288S\DeclareMathSymbol\precnapprox{\mathrel}{AMSb}{"18}E289S\DeclareMathSymbol\succnapprox{\mathrel}{AMSb}{"19}E290S\DeclareMathSymbol\lnapprox{\mathrel}{AMSb}{"1A}E291S\DeclareMathSymbol\gnapprox{\mathrel}{AMSb}{"1B}E292S\DeclareMathSymbol\nsim{\mathrel}{AMSb}{"1C}9 esoE293S\DeclareMathSymbol\ncong{\mathrel}{AMSb}{"1D} E294S%\DeclareMathSymbol\varsubsetneq{\mathrel}{AMSb}{"20}E295S%\DeclareMathSymbol\varsupsetneq{\mathrel}{AMSb}{"21}E296S\DeclareMathSymbol\nsubseteqq{\mathrel}{AMSb}{"22}E297S\DeclareMathSymbol\nsupseteqq{\mathrel}{AMSb}{"23}E298S\DeclareMathSymbol\subsetneqq{\mathrel}{AMSb}{"24}E299S\DeclareMathSymbol\supsetneqq{\mathrel}{AMSb}{"25}E300S%\DeclareMathSymbol\varsubsetneqq{\mathrel}{AMSb}{"26}E301S%\DeclareMathSymbol\varsupsetneqq{\mathrel}{AMSb}{"27}E302S\DeclareMathSymbol\subsetneq{\mathrel}{AMSb}{"28}E303S\DeclareMathSymbol\supsetneq{\mathrel}{AMSb}{"29}E304S\DeclareMathSymbol\nsubseteq{\mathrel}{AMSb}{"2A}E305S\DeclareMathSymbol\nsupseteq{\mathrel}{AMSb}{"2B}E306S\DeclareMathSymbol\nparallel{\mathrel}{AMSb}{"2C}E307S\DeclareMathSymbol\nmid{\mathrel}{AMSb}{"2D}E308S\DeclareMathSymbol\nshortmid{\mathrel}{AMSb}{"2E}E309S\DeclareMathSymbol\nshortparallel{\mathrel}{AMSb}{"2F}E310S\DeclareMathSymbol\nvdash{\mathrel}{AMSb}{"30}E311S\DeclareMathSymbol\nVdash{\mathrel}{AMSb}{"31}E312S\DeclareMathSymbol\nvDash{\mathrel}{AMSb}{"32}E313S\DeclareMathSymbol\nVDash{\mathrel}{AMSb}{"33}E314S\DeclareMathSymbol\ntrianglerighteq{\mathrel}{AMSb}{"34}E315S\DeclareMathSymbol\ntrianglelefteq{\mathrel}{AMSb}{"35}E316S\DeclareMathSymbol\ntriangleleft{\mathrel}{AMSb}{"36}E317S\DeclareMathSymbol\ntriangleright{\mathrel}{AMSb}{"37}E318S\DeclareMathSymbol\nleftarrow{\mathrel}{AMSb}{"38}E319S\DeclareMathSymbol\nrightarrow{\mathrel}{AMSb}{"39}E320S\DeclareMathSymbol\nLeftarrow{\mathrel}{AMSb}{"3A}E321S\DeclareMathSymbol\nRightarrow{\mathrel}{AMSb}{"3B}E322S\DeclareMathSymbol\nLeftrightarrow{\mathrel}{AMSb}{"3C}E323S\DeclareMathSymbol\nleftrightarrow{\mathrel}{AMSb}{"3D}E324S\DeclareMathSymbol\divideontimes{\mathbin}{AMSb}{"3E}E325S\DeclareMathSymbol\varnothing{\mathord}{AMSb}{"3F}E326S\DeclareMathSymbol\mho{\mathord}{AMSb}{"66}E327S\DeclareMathSymbol\eth{\mathord}{AMSb}{"67}E328S\DeclareMathSymbol\eqsim{\mathrel}{AMSb}{"68}E329S\DeclareMathSymbol\beth{\mathord}{AMSb}{"69}E330S\DeclareMathSymbol\gimel{\mathord}{AMSb}{"6A}E331S\DeclareMathSymbol\daleth{\mathord}{AMSb}{"6B}E332S\DeclareMathSymbol\lessdot{\mathrel}{AMSb}{"6C}E333S\DeclareMathSymbol\gtrdot{\mathrel}{AMSb}{"6D}E334S\DeclareMathSymbol\ltimes{\mathbin}{AMSb}{"6E}E335S\DeclareMathSymbol\rtimes{\mathbin}{AMSb}{"6F}E336S\DeclareMathSymbol\shortmid{\mathrel}{AMSb}{"70}E337S\DeclareMathSymbol\shortparallel{\mathrel}{AMSb}{"71}E338S\DeclareMathSymbol\smallsetminus{\mathbin}{AMSb}{"72}E339S\DeclareMathSymbol\thicksim{\mathrel}{AMSb}{"73}E340S\DeclareMathSymbol\thickapprox{\mathrel}{AMSb}{"74}E341S\DeclareMathSymbol\approxeq{\mathrel}{AMSb}{"75}E342S\DeclareMathSymbol\succapprox{\mathrel}{AMSb}{"76}E343S\DeclareMathSymbol\precapprox{\mathrel}{AMSb}{"77}E344S\DeclareMathSymbol\curvearrowleft{\mathrel}{AMSb}{"78}E345S\DeclareMathSymbol\curvearrowright{\mathrel}{AMSb}{"79}E346S\DeclareMathSymbol\digamma{\mathord}{AMSb}{"7A}10 ssoE347S\DeclareMathSymbol\varkappa{\mathord}{AMSb}{"7B} E348S\DeclareMathSymbol\hslash{\mathord}{AMSb}{"7D}E349S\DeclareMathSymbol\hbar{\mathord}{AMSb}{"7E}E350S\DeclareMathSymbol\backepsilon{\mathrel}{AMSb}{"7F}E351S}E352S\def\interleave{{\parallel\!\!\vert}}E353S\def\shortinterleave{\z@rel{\mathord\shortmid\mathord\shortparallel}}E354S\def\napprox{\not\approx}E355S\let\restriction\upharpoonrightE356S\let\Doteq\doteqdotE357S\let\doublecup\CupE358S\let\llless\lllE359S\let\gggtr\gggE360S\let\doublecap\CapUUINumbGers E361S\def\nat,{{\mathbbN}}E362S\def\integer,{{\mathbbZ}}E363S\def\natoneX{{\mathbbN}_1}E364S\def\real s,{{\mathbbR}}E365S\def\bool s,{{\mathbbB}}E366S\let\divides,\divE367S\def\div,{\z@bin{\mathrm{div}}}E368S\def\mod,{\z@bin{\mathrm{mod}}}E369S\def\succ s,{\word{succ}}E370S\def\expon{^}IaliasesE371S\let\num,\integerE372S\let\nplus\natoneILogicE373S\def\lnot s,{\neg\;}E374S\def\land s,{\z@rel{\wedge}}E375S\def\lor,{\z@rel{\vee}}E376S\let\imp,\RightarrowE377S\let\iffX\LeftrightarrowE378S\def\all,{\z@op{\xforall}}E379S\def\exi,{\z@op{\xexists}}E380S\def\exioneX{\exists_1}E381S\@ifpackageloaded{lucbr}{%E382S\DeclareMathSymbol{\nexi}{0}{arrows}{"20}E383S}{%E384S\DeclareMathSymbol{\nexi}{\mathord}{AMSb}{"40}E385S}E386S\def\dot,{\z@rel{\bullet}}E387S\def\true s,{\keyword{true}}E388S\def\false{\keyword{false}}E389S\let\cond s,\rightarrowIaliasesE390S\let\spot s,\dotE391S\mathcode`\@="8000%make@activeinmathmodeE392S{\catcode`\@=\active\gdef@{\dot}}E393S\let\implies,\impE394S\let\forallX\all11 soE395S\let\existsX\exi E396S\let\nexists,\nexiXSETSE397S\let\emptyset s,\varnothingE398S\def\varemptyset s,{\{\,\}}E399S\def\pset s,{\z@op{\mathbbP}}E400S\def\psetone,{\pset_1}E401S\def\fset s,{\z@op{\mathbbF}}E402S\def\fsetone,{\fset_1}E403S\def\sset s,{\z@op{\mathbbS}}E404S\let\mem,\inE405S\def\nem,{\not\mem}E406S\def\uni,{\z@bin\cup}E407S\def\int,{\z@bin\cap}E408S\let\prod s,\timesE409S\def\min,{\word{min}}E410S\def\max,{\word{max}}E411S\def\duni s,{\z@Bigop{\lower0.25ex\hbox{$\uni$}}}E412S\def\dint s,{\z@Bigop{\lower0.25ex\hbox{$\int$}}}E413S\def\upto s,{\z@bin{\ldotp\ldotp}}E414S\let\psubs\subsetE415S\let\subs s,\subseteqE416S\let\psups\supsetE417S\let\sups s,\supseteqE418S\def\diff s,{\z@bin{\backslash}}IaliasesE419S\let\cross\prodE420S\let\notin\nemE421S\let\nmem s,\nemE422S\let\union\uniE423S\let\inter\intE424S\let\power\psetE425S\let\finsetX\fsetE426S\let\dunionX\duniE427S\let\dinterX\dintE428S%IRELA*TIONSUU&FUNCTIONSE429S\def\lambdaX{\z@op{\xlambda}}E430S\def\muX{\z@op{\xmu}}E431S\def\dom,{\keyword{dom}}E432S\def\ran,{\keyword{ran}}E433S\def\idX{\keyword{id}}E434S\@ifpackageloaded{lucbr}{%E435S\DeclareMathSymbol{\dres}{\mathbin}{letters}{"2F}E436S\DeclareMathSymbol{\rres}{\mathbin}{letters}{"2E}E437S}{%E438S\DeclareMathSymbol{\dres}{\mathbin}{AMSa}{"43}E439S\DeclareMathSymbol{\rres}{\mathbin}{AMSa}{"42}E440S}E441S\def\dsub s,{\mathbin{\rlap{\raise.05ex\hbox{$-$}}{\dres}}}E442S\def\rsub s,{\mathbin{\rlap{\raise.05ex\hbox{$-$}}{\rres}}}E443S\let\fovr s,\oplus12 !soE444S\let\cmp,\circ E445S\def\fcmp s,{\mathbin{\raise0.6ex\hbox{\oalign{\hfil$\scriptscriptstyleE446kJ\mathrm{o}$\hfil\cr\hfil$\scriptscriptstyle\mathrm{9}$\hfil}}}}E447S\def\inv,{^\sim}E448S\def\limg s,{(\!|}E449S\def\rimg s,{|\!)}E450S\let\map,\mapstoE451S\let\rel,\leftrightarrowE452S\let\tfun s,\rightarrowE453S\let\tinj s,\rightarrowtailE454S\def\tsur s,{\mathrel{\ooalign{$\tfun$\hfil\cr$\mkern4mu\tfun$}}}E455S\def\pfun s,{\p\tfun}E456S\def\pinj s,{\p\tinj}E457S\def\psur s,{\p\tsur}E458S\def\ffun s,{\f\tfun}E459S\def\finj s,{\f\tinj}E460S\def\bij,{\mathrel{\ooalign{$\tinj$\hfil\cr$\mkern5mu\tfun$}}}E461S\def\tcl,{^+}E462S\def\rtcl s,{^*}E463S\def\iter s,{^}IaliasesE464S\let\comp s,\fcmpE465S\let\ndres\dsubE466S\let\nrres\rsubE467S\let\fun,\tfunE468S\let\inj,\tinjE469S\let\surj s,\tsurE470S\let\psurj\psurE471S\let\lllessX\lllE472S\let\gggtr\gggE473S\def\interleaveX{{\parallel\!\!\vert}}E474S\def\shortinterleave,{\z@rel{\mathord\shortmid\mathord\shortparallel}}E475S\let\restriction,\upharpoonrightE476S\def\napprox,{\not\approx}ISEQUENCESE477S\def\seq,{\keyword{seq}}E478S\def\iseq{\keyword{iseq}}E479S\def\seqoneX{\seq_1}E480S\def\emptyseq s,{\lseq\,\rseq}E481S\let\lseq s,\langleE482S\let\rseq s,\rangleE483S\def\head s,{\word{head}}E484S\def\tail s,{\word{tail}}E485S\def\front{\word{front}}E486S\def\last s,{\word{last}}E487S\def\rev,{\word{rev}}E488S\def\squashX{\word{squash}}E489S\def\next s,{\keyword{next}}E490S\def\inseq{\keyword{in}}E491S\@ifpackageloaded{lucbr}{%E492S\DeclareMathSymbol{\sres}{2}{arrows}{"75}E493S\DeclareMathSymbol{\ires}{2}{arrows}{"76}E494S\DeclareMathSymbol{\@@cat}{\mathbin}{operators}{"5F}13soE495S}{% E496S\DeclareMathSymbol{\@@cat}{\mathbin}{AMSa}{"61}E497S\DeclareMathSymbol{\sres}{\mathbin}{AMSa}{"16}E498S\DeclareMathSymbol{\ires}{\mathbin}{AMSa}{"18}E499S}E500S\def\cat,{\mathbin{\raise0.8ex\hbox{$\mathchar\@@cat$}}}E501S\def\ssub s,{\z@bin{\rlap{$-$}{\sres}}}E502S\def\isub s,{\z@bin{\rlap{$-$}{\ires}}}E503S\def\dcat s,{\z@op{\cat/}}E504S\def\dovr s,{\z@op{\fovr/}}E505S\def\dcmp s,{\z@op{\fcmp/}}E506S\let\prefixX\subseteqE507S\def\suffixX{\keyword{suffix}}E508S\def\seqi s,{\keyword{seq_\infty}}E509S\def\partitionsX{\keyword{partitions}}E510S\def\partition{\keyword{partitions}}E511S\def\disjoint s,{\keyword{disjoint}}E512S\def\subseqX{\keyword{subseq}}Ialiases E513S\let\filterX\sresISchemas:E514S\def\lsch s,{\z@bigop{[}} E515S\def\rsch s,{\z@bigop{]}}E516S\def\dparallel{\z@bigop{\parallel}\limits}E517S\def\zand s,{\z@bigbin\land}E518S\def\zor,{\z@bigbin\lor}E519S\def\zcmp s,{\z@bigbin\fcmp}E520S\def\zexi s,{\z@bigop\exists}E521S\def\zall s,{\z@bigop\forall}E522S\def\znot s,{\z@bigop\neg}E523S\def\zbar s,{\z@bigbin\cbar}E524S\def\zfor s,{/}E525S\def\zhide{\z@bigbin\backslash}E526S\def\zimp s,{\z@bigrel\imp}E527S\def\zeq,{\z@bigrel\iff}E528S\def\zovr s,{\z@bigrel\oplus}E529S\def\zpipe{\z@bigbin{\mathord>\!\!\mathord>}}E530S\def\pre,{\keyword{pre}}E531S\def\pred s,{\keyword{pred}}E532S\def\post s,{\keyword{post}}E533S\def\zproject s,{\z@bigbin\sres}E534S\def\rename{\@ifnextchar*{\z@rename}{\z@@rename}}E535S\def\z@rename*[#1/#2]{\left[#1\over#2\right]}E536S\def\z@@rename[#1/#2]{\left[#1\zfor#2\right]}IaliasesE537S\let\project,\zprojectE538S\let\importX\sresE539S\let\semi s,\zcmpE540S\let\hide s,\zhideXBAGSUUE541S\let\buni\uplusE542S\def\emptybag s,{\lbag\:\rbag}14VsoE543S\def\lbag s,{[\![} E544S\def\rbag s,{]\!]}E545S\def\bag,{\keyword{bag}}E546S\def\items{\word{items}}E547S\let\inbag\inseqE548S\def\bagcount s,{\word{count}}tXDe nitionsUU&declarationstE549S\def\ddef s,{\z@rel{\;::=\;}}E550S\def\bbar s,{\z@bigrel{|}}E551S\let\cbar s,\midE552S\def\lang s,{\langle\!\langle}E553S\def\rang s,{\rangle\!\rangle}E554S\def\sdef s,{\z@rel{\widehat=}}E555S\def\defs s,{\z@smallrel{==}}E556S\def\varsdef,{\z@rel\triangleq}Ialiases 躍E557S\let\sdefs\sdefE558S\mathcode`\|=\midE559S\let\ldata\langE560S\let\rdata\rang躍XMISCELLANEOUStE561S\def\lblot{\langle\!|}E562S\def\rblot{|\!\rangle}E563S\def\IMP,{\boldword{Import}}E564S\let\env,\RrightarrowE565S\def\zlet s,{\boldword{let}}E566S\def\zin,{\boldword{in}}E567S\def\zwhereX{\boldword{where}}XQZEDUUSUPPOR*TtE568S\def\HOLE{\z@op{\hbox{$\lll\star\star\star\ggg$}}}E569S\def\landd{}%tosupportqzededitorE570S\def\semid{}%tosupportqzededitorE571S\def\qzed{\ifz@inclass\else\zed\fi}E572S\def\endqzed{\ifz@inclass\else\endzed\fi}XCLASSEStE573S\def\qua{\mbox{::}}E574S\def\redef{\mbox{\textbf{~redef}}}E575S\def\Init{I\!\mbox{\footnotesize\emph{NIT}}}E576S\def\Exit{E\!\mbox{\footnotesize\emph{XIT}}}E577S\def\Internal{I\!\mbox{\footnotesize\emph{NTERNAL}}}E578S\def\Aux{A\!\mbox{\footnotesize\emph{UX}}}E579S\def\intern{\mbox{\textsf{i}}}XPROOFStE580S\def\thrm{\z@rel\vdash}E581S\def\qed{\zsmall\Box}E582S\let\Qed\BoxE583S\let\QED\squareE584S\def\BLACKQED{\zsmall\blacksquare}E585S\let\ETH\qed15ҠsoE586S\def\TH{\boldword{Theorem}} E587S\def\LE{\boldword{Lemma}}E588S\def\PR{\boldword{Proof}}E589S\def\refines{\z@rel\sqsupseteq}E590S\def\defines{\z@rel\sqsubseteq}E591S\def\weakrefine{\z@rel{\raise0.2ex\rlap{\hbox{$\sqsupset$}}\lower1ex\hbox{$\sim$}}}E592S\def\weakdefine{\z@rel{\raise0.2ex\rlap{\hbox{$\sqsubset$}}\lower1ex\hbox{$\sim$}}}#Ialiases ǍE593S\let\shows\thrmǍXOBJECTUUTHEOR*Y#E594S\def\childof{\z@rel\xsucc}E595S\def\parentof{\z@rel\xprec}E596S\let\weaksubclass\succsimE597S\let\weaksupclass\precsimE598S\def\hasa{\z@rel{\mathord\xsucc\!\!\!\mathord\xsucc}}E599S\def\instancein{\z@rel{\mathord\xprec\!\!\!\mathord\xprec}}E600S\def\subtype{\z@rel\sqsubset}E601S\def\subtypeeq{\z@rel\sqsubseteq}E602S\def\suptype{\z@rel\sqsupset}E603S\def\suptypeeq{\z@rel\sqsupseteq}Ialiases ǍE604S\let\inherits\childofE605S\let\subclass\childofE606S\let\isa\childofE607S\let\supclass\parentofE608S\let\instantiates\hasaE609S\let\islikea\weaksubclassE610S\def\poly{\mathord\downarrow}E611S\def\widen#1{\z@op{{\overline{#1}}}}ǍXTEMPORALUULOGIC#E612S\def\atnext{\rlap{$\zSmall\bigcirc$}\kern0.01em\rlap{$\zSmall\bigcirc$}\kern0.01em\zSmall\bigcirc}E613S\def\atlast{\rlap{$\zSmall\bigcirc$}\kern0.01em\rlap{$\zSmall\bigcirc$}\kern0.01em\rlap{$\kern0.01em\mathord-$}\zSmall\bigcirc}E614S\def\always{\lower0.37ex\hbox{$\zbig\Box$}}E615S\def\uptilnow{\rlap{$\kern0.02em\mathord-$}\lower0.37ex\hbox{$\zbig\Box$}}E616S\def\eventually{\lower0.37ex\hbox{$\zbig\Diamond$}}E617S\def\previously{\rlap{$\kern0.04em\mathord-$}\lower0.37ex\hbox{$\zbig\Diamond$}}Ialiases ǍE618S\let\henceforth\alwaysǍXORDERS#E619S\def\mono s,{\keyword{monotonic}}E620S\def\porderX{\keyword{partial\_order}}E621S\def\torderX{\keyword{total\_order}}E622S\newbox\z@combox\newdimen\z@wdcalcE623S\def\comment{\@ifnextchar*{\z@leftcomment}{\z@comment}}E624S\def\z@comment#1{$\z@stopfield\z@addfield\z@startfield$%E625S\global\setbox\z@combox\hbox{\quad[{\sf#1}]}\z@wdcalc=\wd\z@combox%E626S\advance\z@wdcalcby\wd\z@curline\advance\z@wdcalcby\z@curindent%E627S\advance\z@wdcalcby\zedleftsep\advance\z@wdcalcby\zedlinethickness%E628S\advance\z@wdcalcby2\zedindent\ifdim\z@wdcalc>\displaywidth\\%E629S\fi&\box\z@combox\ignorespaces}E630S\def\z@leftcomment*#1{\hbox{[{\sf#1}]}}16soI6aLObfject-ZffNotationsIKEYWORDSUUANDKEYSYMBOLSE631S\def\oid{{\bboldO}} E632S\def\self,{\word{self}}E633S\def\contained{\word{contained}}E634S\let\classuniX\uniE635S\def\visibility{\zproject}E636S\def\invisibility{{\project\hspace{-0.63em}\cross}}XCONT*AINMENTUUANDCONTROLADORNMENTSE637S\def\cid{{\bigcirc\mbox{\scriptsize{\hspace{-0.78em}}\mbox{\tiny{C}}}}}E638S\def\sid{{\bigcirc\mbox{\scriptsize{\hspace{-0.74em}}\mbox{\tiny{S}}}}}E639S\def\eid{{\bigcirc\mbox{\scriptsize{\hspace{-0.74em}}\mbox{\tiny{E}}}}}XBINAR*YUUCOMPOSITIONOPERATORSE640S\def\pll{~\parallel~}E641S\def\plo{~\parallel_{!}~}E642S\def\sqc{~\semi~}E643S\def\cnj{~\zand~}E644S\def\gch{~[\mbox{\hspace{-0.25mm}}]~}E645S\def\enh{~\dot~}XDISTRIBUTEDUUCOMPOSITIONOPERA*TORSE646S%Redefinedbecauseof\zbigproblemE647S%\def\dsqc{\mbox{{\Large$\zcmp~$}}}E648S\def\dsqc{\mbox{{\Large$\fcmp~$}}}E649S\def\dgch{\mbox{\hspace{-2.5mm}{\Large$\gch$}}}E650S%Redefinedbecauseof\zbigproblemE651S%\def\dcnj{\mbox{{\Large$\zand$}}}E652S\def\dcnj{\mbox{{\Large$\land$}}}E653S\def\dpll{\mbox{{\Large$\parallel$}}}E654S\def\dplo{\mbox{{\Large$\parallel_{!}$}}} WI7aLZffenvironmentsI7.1gMarginstackuTIDe ne=astackofdimensions(50elements)ThiscanprobablybGemadesmaller IwhenUUqzed ltersitsTU>'ExXoutputbGetter WE655S\newcount\z@stackminE656S\newcount\z@stackmaxE657S\newcount\z@stacktopE658S\newdimen\@gtempa\z@stackmin=\allocationnumberE659S\newdimen\@gtempa\newdimen\@gtempa\newdimen\@gtempa\newdimen\@gtempaE660S\newdimen\@gtempa\newdimen\@gtempa\newdimen\@gtempa\newdimen\@gtempaE661S\newdimen\@gtempa\newdimen\@gtempa\newdimen\@gtempa\newdimen\@gtempaE662S\newdimen\@gtempa\newdimen\@gtempa\newdimen\@gtempa\newdimen\@gtempaE663S\newdimen\@gtempa\newdimen\@gtempa\newdimen\@gtempa\newdimen\@gtempaE664S\newdimen\@gtempa\newdimen\@gtempa\newdimen\@gtempa\newdimen\@gtempaE665S\newdimen\@gtempa\newdimen\@gtempa\newdimen\@gtempa\newdimen\@gtempaE666S\newdimen\@gtempa\newdimen\@gtempa\newdimen\@gtempa\newdimen\@gtempaE667S\newdimen\@gtempa\newdimen\@gtempa\newdimen\@gtempa\newdimen\@gtempa17soE668S\newdimen\@gtempa\newdimen\@gtempa\newdimen\@gtempa\newdimen\@gtempa E669S\newdimen\@gtempa\newdimen\@gtempa\newdimen\@gtempa\newdimen\@gtempaE670S\newdimen\@gtempa\newdimen\@gtempa\newdimen\@gtempa\newdimen\@gtempaE671S\newdimen\@gtempaE672S\z@stackmax=\allocationnumberE673S\dimen\z@stackmin=0ptIDe neUUabGoxtocontainthecurrentline&avqariabletocontainit'sindentationE674S\newbox\z@curlineE675S\newdimen\z@curindentE676S\dimen\z@curindent=0ptISpaceUUbGetweenopGerandsofafunctionapplicationE677S\def\z@space{{}\;{}}IDe neUUabGoxtocontainthecurrent eldE678S\newbox\z@curfieldIDe neUUamini-tabbingenvironmentUUforuseinside`zed'E679S\def\z@startline{\setbox\z@curline\hbox{}% E680kJ\global\z@curindent\dimen\z@stacktopE681kJ\z@startfield\ignorespaces}E682S\def\z@stopline{\z@stopfieldE683f\z@addfieldE684f\hbox{\hskip\z@curindent\box\z@curline}}E685E686S\def\z@startfield{\global\setbox\z@curfield\hbox\bgroup}E687S\def\z@stopfield{\egroup}E688S\def\z@addfield{\global\setbox\z@curline\hbox{\unhboxE689kJ\z@curline\unhbox\z@curfield}}E690E691S\def\z@pushmargin{\hbox{\kern0pt}$%E692]\z@stopfieldE693]\z@addfieldE694]\ifnum\z@stacktop<\z@stackmaxE695f\global\advance\z@stacktop\@neE696]\elseE697f\@latexerr{Zmarginstackoverflow(toomany\string\M's)}E698f\@ehdE699]\fiE700]\global\dimen\z@stacktop\z@curindentE701]\global\advance\dimen\z@stacktop\wd\z@curlineE702]\z@startfield\ignorespacesE703]$\relax}E704S\def\z@popmargin{\ifnum\z@stacktop>\z@stackminE705f\global\advance\z@stacktop\m@ne\ignorespacesE706]\elseE707f\@latexerr{ZMarginstackunderflow(toomany\string\O's)}E708f\@ehdE709]\fi}E710S\def\M{\z@pushmargin}\def\O{\z@popmargin}\def\S{\z@space}E711S\z@stacktop\z@stackmin18soI7.2gUtilitymacrosforZenvironmentsuTIHereSareenvironmentsSforthevqarioussortsofdisplayswhichoGccurinZSrdocuments. IAlldisplaysareset ushleft,&indentedby\zedindent,&bydefault\leftmargini.ISchemas,UUetc,aremadejustwideenoughtogiveequalmarginsleftandright.XSome_environments(schema,etc.)mustonlybGesplitat\zbreak,andothersI(e.g.cargue)L&maybGesplitarbitrarily*.Allgeneratealignmentdisplays,0andpGenaltiesIareUUusedtocontrolpagebreaks.6I7.2.1l#F ormatTandcon9trolmacrosuTE712S\newdimen\zedindent\zedindent=\leftmargini E713S\newdimen\zedleftsepX\zedleftsep=1emE714S\newdimen\zedtabX\zedtab=2emE715S\newdimen\zedbarX\zedbar=8emE716S\newdimen\zedlinethickness s,\zedlinethickness=0.4ptE717S\newdimen\zedcornerheight,\zedcornerheight=0ptE718S\newcount\z@colsE719S\newif\ifz@firstlineX\z@firstlinefalseE720S\newif\ifz@inclass s,\z@inclassfalseE721S\newif\ifz@inenvX\z@inenvfalseE722S\newif\ifz@leftmargin,\z@leftmargintrueE723S\newif\ifz@incols,\z@incolsfalseE724S\newif\ifleftnames s,\leftnamesfalseE725S\def\leftschemas{\leftnamestrue}E726S\newif\ifz@inboxX\z@inboxfalseE727S\newskip\zedbaselineskipX\zedbaselineskip\baselineskipE728S\newbox\zstrutbox,\setbox\zstrutbox=\copy\strutboxE729S\def\zstrut{\relax\ifmmode\copy\zstrutbox\else\unhcopy\zstrutbox\fi}E730S\def\zedbaselinestretch{1}XPenaltiesE731S\newcount\interzedlinepenalty,\interzedlinepenalty=10000 s,%neverbreakE732S\newcount\preboxpenalty\preboxpenalty=0X%breakeasilyE733S\newcount\forcepagepenalty s,\forcepagepenalty=-10000X%alwaysbreakE734S\interdisplaylinepenalty=100X%breaksometimesXMacrosUUforchangingthesizeofschematextE735S\def\zedsize#1{\def\z@size{#1}}E736S\def\z@size{}E737S\newskip\z@adskip\newskip\z@bdskip\newskip\z@adsskip\newskip\z@bdsskipE738S\def\z@changesize{%E739S\z@adskip\abovedisplayskip\z@bdskip\belowdisplayskip%saveskipsE740S\z@adsskip\abovedisplayshortskip\z@bdsskip\belowdisplayshortskipE741S\z@size%changesizeE742S\abovedisplayskip\z@adskip\belowdisplayskip\z@bdskip%restoreskipsE743S\abovedisplayshortskip\z@adsskip\belowdisplayshortskip\z@bdsskip}E744S%E745S%E746S\def\z@zeroskips{\abovedisplayskip\z@\belowdisplayskip\z@E747f\abovedisplayshortskip\z@\belowdisplayshortskip\z@}E748S\def\@setfontsize#1#2#3{\@nomath#1%E749f\ifx\protect\@typeset@protectE750p2\let\@currsize#1%E751f\fi19ҠsoE752f\fontsize{#2}{#3}\selectfont E753f\zedbaselineskip#3ptE754f\zedbaselineskip\zedbaselinestretch\zedbaselineskipE755f\setbox\zstrutbox\hbox{\vruleheight.7\zedbaselineskipE756fdepth.3\zedbaselineskipwidth\z@}E757f}I7.3gMacrosformarginsuTI\z@narrow,UU\z@wide|makethemarginsnarrower,widerE758S\def\z@narrow{\advance\linewidthby-\zedindent}E759S\def\z@wide{\advance\linewidthby\zedindent}6I7.4gMacrosfordrawingb`oxesI\z@hrulefillUU|linewithcorrectthicknessE760S\def\z@hrulefill{\leaders\hruleheight\zedlinethickness\hfill}X\z@topline8drawsthetophorizontallineofbGoxedenvironments\z@dbltopline Idrawsa/adoubleruledtopline\z@botlinedrawsthebGottomhorizontallineofIbGoxedenvironments\zedline[comment]drawsalonghorizontallineendinginIcommentUU\wheredrawsashorthorizontallineE761S\def\z@topline#1{\omit\@ifnextchar[{\z@@topline{#1}}{\z@@topline{#1}[]}} E762S\def\z@@topline#1[#2]{\hboxto\linewidth{\zstrut\ifleftnames\elseE763f\vruleheight\zedlinethicknesswidth\zedlinethicknessE764f\hboxto\zedleftsep{\z@hrulefill}\fi#1\z@hrulefillE765f\smash{\vruleheight\zedlinethicknesswidth\zedlinethicknessE766fdepth\zedcornerheight}\hbox{\sf#2}}\cr}E767S\def\z@dbltopline#1{\omit\@ifnextchar[{\z@@dbltopline{#1}}{\z@@dbltopline{#1}[]}}E768S\def\z@@dbltopline#1[#2]{\z@@topline{#1}[#2]%E769S\noalign{\kern-\baselineskipE770f\kern-\zedlinethicknessE771f\kern-\doublerulesep\nobreak}%E772S\omit\z@@topline{\hphantom{#1}}[\hphantom{#2}]%E773S\noalign{\kern\doublerulesepE774f\kern\zedlinethickness\nobreak}}E775S\def\z@botline{\also\omit\hboxto\linewidth{\z@hrulefillE776S\smash{\vruleheight\zedcornerheightwidth\zedlinethicknessE777fdepth0pt}}\cr}E778S\def\z@@botline[#1]{\hboxto\linewidth{\vrule\z@hrulefill\hbox{\sf\smash{#1}}}\also}E779S\def\zedline{\also\omit\@ifnextchar[{\z@@botline}{\z@@botline[]}}E780S\def\where{\also\omit\hboxto\zedbar{\z@hrulefill}\cr\also}E781S\let\STX\whereX\z@leftisplacedattheleftofeachzline:Oinnon-bGoxenvironmentsitwilldo Inothing.inybGoxedenvironmentsitwilldoaverticallinewiththesameheightasItheUUmaximumheightoftheline.E782S\def\z@left{\ifz@inbox\vrulewidth\zedlinethickness\hskip\zedleftsep\fi}6I7.5gMacrosforsettingupZenvironmentsuTE783S\def\z@env{\global\z@firstlinetrue\z@changesize E784f$$20tsoE785f\z@inenvtrue E786f\baselineskip\zedbaselineskipE787f\parskip=0pt\lineskip=0pt\z@narrowE788f\advance\displayindentby\zedindentE789f\def\\{\crcr}%Musthave\defandnot\letfornestedalignments.E790f\everycr={\noalign{\ifz@firstline\global\z@firstlinefalseE791f\else\penalty\interzedlinepenalty\fi}}E792f\tabskip=0pt}E793S\def\endz@env{$$E794XdD\global\@ignoretrueE795S}XZܗlinesܺareformatedintwoܺ(overlapping)columns; lthe rst ushlefthaving Ithedsamewidthastheenvironment,and,thedsecond ushrightendingattherightIendUUoftheenvironment. E796S\def\z@format{\halignto\linewidth\bgroup%E797f\zstrut\z@left\z@startline\ignorespaces$\@lign##$\z@stopline\hfil%E798f\tabskip=0ptplus1fil%E799f&\hboxto0pt{\hss\@lign##}\tabskip=0pt\cr}E800S\def\z@boxenv{\z@narrow\let\also=\als@\let\Also=\Als@\let\ALSO=\ALS@E801f\z@inboxtrue\predisplaypenalty=\preboxpenalty\z@env\z@format}E802S\def\z@outnonbox{\z@outclasscheck\z@leavevmode\z@env}E803S\def\z@inoutbox{\z@leavevmode\z@makeouter\z@inclassfalse\z@boxenv}I7.6gSpacingcommandsuTInoUUverticalgluebGetweenabuttedlinesE804S\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{}}}E805S\def\z@nopar{\global\@endpetrue}X\z@leavevmodek̲{EnterhorizontalmoGde,takingaccountofpGossibleinteractionIwithUUlistsandsectionheads:U81.bAftera\item,use\indenttogetthelabGel(thisfailstoruninevenshortblabGels).U82.bAfterUUarun-inheading,use\indent.U83.bAfteranordinaryheading,~throwawaythe\everypartokens,~resetb\@nobreak,UUanduse\noindentwith\parskipzero.U84.bOtherwise,UUuse\noindentwith\parskipzeroIUseUUwhenenteringdisplayedenvironmentstogetcorrectspacingE806S\def\z@leavevmode{\ifvmode\if@inlabel\indent\else\if@noskipsec\indent\else E807f\if@nobreak\global\@nobreakfalse\everypar={}\fiE808f{\parskip=0pt\noindent}\fi\fi\fi}XextraUUverticalspaceinnon-bGoxenvironmentsE809S\def\also{\crcr\noalign{\vskip\jot}}E810S\def\Also{\crcr\noalign{\vskip2\jot}}E811S\def\ALSO{\Also\Also}21soXextraUUverticalspaceinbGoxedenvironmentsqaE812S\def\als@{\crcr\@but\omit\vruleheight\jotwidth\zedlinethickness\cr\@but} E813S\def\Als@{\crcr\@but\omit\vruleheight2\jotwidth\zedlinethickness\cr\@but}E814S\def\ALS@{\crcr\@but\omit\vruleheight4\jotwidth\zedlinethickness\cr\@but}ύI7.7gEnvironment-breakingcommandsuTE815S\def\znewpage{\also\noalign{\penalty\forcepagepenalty}\also}E816S\def\zbreak{\also\noalign{\penalty\interdisplaylinepenalty\vskip-\jot}\also}E817S\def\Zbreak{\also\noalign{\penalty\interdisplaylinepenalty}\also}E818S\def\ZBREAK{\Also\noalign{\penalty\interdisplaylinepenalty}\Also}E819S\def\t#1{\hskip#1\zedtab}E820S%\def\c#1#2{\hboxto#1\zedtab{$#2$\hfil}}E821S\def\flushr#1{\crcr\quad\cr}qaI8aLUtilityffmacrosforObfject-ZE822S\def\z@inclasscheck{\ifz@inclass\elseE823f\@latexerr{ThisZenvironmentisonlyallowedwithinaclass}E824S{Perhapsyouforgottoincludea\string\begin\string{class\string}E825Ssomewhere^^Joryouaretryingtoprintafilethatneedsupdating.^^J\@ehc}\fi}E826S\def\z@outclasscheck{\ifz@inclassE827f\@latexerr{ThisZenvironmentisnotallowedinsideaclass}E828S{Thisenvironmentdoesn'treallymakesensewithinaclass.^^J%E829SIfyoureallywantitthenI'lltrymybesttofitinin.^^J\@ehc}\elseE830S\ifz@inenv\@latexerr{NewZenvironmentdeclaredbeforepreviousE831Soneiscompleted}E832S{Isuspectthatyou'veforgottentofinishthelastenvironment.^^J%E833SYouaretryingtonestenvironmentsandthiscanonlybedoneinsideclasses^^J%E834Sbesides,theenvironmentyouhavestartedisn'tvalidwithinclassesanyway.^^JIsuggestthatyoutype\spaceX\spacetoquitandthencorrectyourdocument.}E835S\fi\fi}E836S%E837S\def\z@makeouter{%E838XdD\ifz@inenvE839ap\ifz@inclass\z@inenvfalseE840f\hskip-\zedleftsep\advance\linewidthby-\zedlinethicknessE841f\zedindent=\zedleftsep\zedleftsep=0.8\zedleftsepE842f\zedbar=0.8\zedbar\zedtab=0.8\zedtabE843f\oz@parbox{\linewidth}\bgroupE844f\z@zeroskipsE845ap\elseE846XdD\@latexerr{IncorrectplaceforZenvironment;nestingisE847]allowedonlyinsideclasses}E848ap{You'veeitherforgottentofinishthelastenvironment,^^J%E849apyou'veforgottentoincludeaE850ap\string\begin\string{class\string}somewhere^^J%E851aporyouaretryingtoprintafilethatneedsupdating.^^J%E852ap(Thenagain,youmightjustbetryingtodosomething^^J%E853fthattheauthorofthesemacrosdidn'tintendyoutodo)^^J\@ehc}E854ap\fiE855XdD\elseE856ap\bgroupE857XdD\fiE858S}22AsoE859S% E860S\def\z@makeinner{\egroupE861ap\global\z@curindent\z@E862S}E863S%E864S\def\classbreak{\also\egroup$$\vskip-\ht\zstrutboxE865f\vskip-\abovedisplayskip\vskip-\belowdisplayskip\z@wide\z@boxenv\also}I9aLNon-bs3oxffenvironmentsIZEDUUfornon-bGoxmultilineformulasE866S\def\zed{\z@outnonbox\z@inboxfalse\z@format}E867S\def\endzed{\crcr\egroup\endz@env}E868S\let\[=\zedE869S\def\]{\crcr\egroup$$\ignorespaces}XARGUEUUforalgebraicarguments XusedforalgebraicproGofsexpressedasextendedequations."likezedbutwithIextraspacingbGetweenlinesGeneratesanalignmentdisplay*,}whichmaybGesplitIacrossUUpages.E870S\def\argue{\z@outnonbox\interzedlinepenalty=\interdisplaylinepenalty E871f\openup1\jot\z@formatE872f\noalign{\vskip-\jot}}%equalvspaceaboveandbelowarguedisplayE873S\let\endargue=\endzedXINFRULEUUforinferencerules Xused}forinferencerules. ?Thehorizontallineisgeneratedby\derive:anIoptionalUUargumentcontainstheside-conditionsoftherule.E874S\def\infrule{\z@outnonbox\halign\bgroup E875f\zstrut\quad$\@lign##$\quad\hfil&\quad\@lign##\hfil\cr}E876S\let\endinfrule=\endzedE877S\def\derive{\crcr\also\@but\omit\z@hrulefill%E878f\@ifnextchar[{\z@sidecondition}{\cr\also\@but}}E879S\def\Derive{\crcr\also\@but\omit\z@hrulefill\cr\@butE880f\noalign{\kern-\dp\zstrutboxE881f\kern\doublerulesep\nobreak}%E882S\omit\derive}E883S\def\z@sidecondition[#1]{&$\smash{\lower0.2ex\hbox{$[\;#1\;]$}}$\cr\also\@but}XSYNT*AXUUforsyntaxrules X`syntax'UUenvironment:qusedforsyntaxrules|even(once!)qforVDM.E884S\def\syntax{\z@outnonbox\halign\bgroupE885f\zstrut$\@lign##$\hfil&\hfil$\@lign{}##{}$\hfilE886f&$\@lign##$\hfil&\qquad\@lign--##\hfil\cr}E887S\let\endsyntax=\endzed6I9.1gBoxedenvironmentsuTISCHEMAUUschemade nitionsE888S\def\schema#1{\z@inoutbox\z@topline{$\,#1\,$}}E889S\def\endschema{\z@botline\endzed\z@makeinner\z@nopar}23EsoXANONSCHEMAUUschemawithnonameE890S\@namedef{anonschema}{\leftnamesfalse\z@inoutbox\z@topline{}} E891S\expandafter\let\csnameendanonschema\endcsname=\endschemaXGENSCHEMAUUgenericschemade nitionsE892S\def\genschema#1#2{\z@inoutbox\z@topline{$\,#1\:[#2]\,$}}E893S\let\endgenschema=\endschemaXAXDEFUU`libGeral'axiomaticde nitionsE894S\def\axdef{\z@inoutbox}E895S\def\endaxdef{\endzed\z@makeinner}XUNIQDEFUU`unique'axiomaticde nitionsE896S\def\uniqdef{\leftnamesfalse\z@inoutbox\z@dbltopline{}}E897S\let\enduniqdef=\endschemaXGENDEFUU'generic'axiomaticde nitions XHACKUUTOMAKEITCOMP*ATIBLEUUWITHFUZZ.STYE898S\def\gendef{\@ifnextchar[{\z@gendef}{\z@@gendef}}E899S\def\z@gendef[#1]{\leftnamesfalse\z@inoutbox\z@dbltopline{$\,[#1]\,$}}E900S\def\z@@gendef#1{\leftnamesfalse\z@inoutbox\z@dbltopline{$\,[#1]\,$}}E901S\let\endgendef=\endschemaXGENGENDEFUUgenericcontentsUU'generic'axiomaticde nitionsXHackUUtoprovidesyntax-orienteddisplaybGoxesE902S\def\gengendef{\@ifnextchar[{\z@gengendef}{\z@@gengendef}}E903S\def\z@gengendef[#1]{\leftnamesfalse\z@inoutbox\z@dbltopline{$\,#1\,$}}E904S\def\z@@gengendef#1{\leftnamesfalse\z@inoutbox\z@dbltopline{$\,#1\,$}}E905S\let\endgengendef=\endschemaXCLASSE906S\def\class#1{\z@leavevmode\z@makeouter\z@inclasstrueE907f\z@boxenv\z@topline{$\,#1\,$}}E908S\let\endclass\endschemaXOPE909S\def\op{\z@inclasscheck\schema}E910S\let\endop\endschemaXST*ATEE911S\def\state{\z@inclasscheck\vbox\bgroup\vskip-\ht\zstrutbox\vbox\bgroup\hbox\bgroup\@nameuse{anonschema}}E912S\def\endstate{\endschema\egroup\egroup\egroup}XINITE913S\def\init{\z@inclasscheck\schema{\Init}}E914S\let\endinit\endschemaXCONSTE915S\let\const\axdefE916S\let\endconst\endaxdefXTYPEE917S\def\type{\z@inclasscheck}E918S\let\endtype\relax24soI9.2gOtherenvironmentsuTISIDEBYSIDE XThisX}shouldsuppGortanarbitarynumberX}ofcolumns\zedindent'sproportionIofUU\linewidthgivesapracticallimitE919S\def\sidebyside{\@ifnextchar[{\z@columns}{\z@columns[2]}} E920S\def\z@columns[#1]{\z@leavevmode\z@cols#1\z@makeouter\z@narrow%E921f$$\lineskip=0pt\z@incolstrueE922f\predisplaysize\maxdimenE923f\ifz@leftmargin\hskip-\zedindent\z@leftmarginfalse\fiE924f\setbox0=\hboxto\linewidth\bgroup\z@zeroskips%E925f\divide\zedbarby\z@cols\divide\zedleftsepby\z@colsE926f\divide\zedtabby\z@cols\divide\linewidthby\z@colsE927ap\oz@parbox[t]{\linewidth}\bgroup\z@wide}E928S%E929S\def\nextside{\egroup\hss\oz@parbox[t]{\linewidth}\bgroup\z@wide}E930S%E931S\newdimen\z@tempE932S\def\endsidebyside{\egroup\egroupE933f\z@temp\ht0\advance\z@tempby\dp0\advance\z@tempby-\dp\zstrutboxE934f\hbox{\raise\z@temp\box0}\endz@env\z@makeinner\z@nopar}XZP*ARE935S\def\zpar{\z@leavevmodeE936f\ifz@inenv\z@inclasstrue\fi%fudgetoletzparinallboxesE937f\z@makeouter\z@changesizeE938f\advance\linewidthby-\z@curindentE939f\advance\linewidthby-\wd\z@curlineE940f\hskip-\wd\z@curline\advance\linewidthby-\zedindent$$E941f\ifz@leftmargin\hskip-\zedindent\fi%adjustmentforfirstcolumnE942f\advance\displayindentby\zedindentE943f\advance\displaywidthby-\zedindentE944f\advance\displayindentby\z@curindentE945f\advance\displayindentby\wd\z@curlineE946f\advance\displaywidthby-\z@curindentE947f\advance\displaywidthby-\wd\z@curlineE948f\global\setbox\z@curline\hbox{}E949f\z@narrow\oz@parbox[b]{\linewidth}\bgroup\hfil\break}E950S\def\endzpar{\egroup$$\z@makeinner\z@nopar}XCLASSCOME951S\def\classcom{\zpar\sf}E952S\let\endclasscom=\endzparXPROOFE953S\def\proof{\zpar$\PR$\zpar}E954S\def\endproof{\endzpar\endzpar}XAdditionalUUauxiliarymacrosE955S\def\zseq#1{\lseq#1\rseq}E956S\def\zset#1{\{#1\}}E957S\def\zimg#1{\limg#1\rimg}E958S\def\zsch#1{\lsch#1\rsch}E959S\def\zimgset#1{\zimg\zset{#1}}25 soXOZUUFUZZ X\defsUU==\sdef\defsE960S\def\fuzzcompatible{% E961S\let\defs\sdefE962S\let\empty\emptysetE963S}E964S%E965Sh"5" cmmi9=pack9age#g i26$; $ow cmss9# cmsy9"5" cmmi9 ߤN cmtt9 cmmi10K`y cmr10ٓRcmr7&/