%!PS-Adobe-2.0 %%Creator: dvipsk 5.66a Copyright 1986-97 Radical Eye Software (www.radicaleye.com) %%Title: final.dvi %%Pages: 9 %%PageOrder: Ascend %%BoundingBox: 0 0 596 842 %%DocumentPaperSizes: a4 %%EndComments %DVIPSCommandLine: dvips -o final.ps final.dvi %DVIPSParameters: dpi=600, compressed %DVIPSSource: TeX output 1999.10.04:1017 %%BeginProcSet: texc.pro %! /TeXDict 250 dict def TeXDict begin /N{def}def /B{bind def}N /S{exch}N /X{S N}B /TR{translate}N /isls false N /vsize 11 72 mul N /hsize 8.5 72 mul N /landplus90{false}def /@rigin{isls{[0 landplus90{1 -1}{-1 1} ifelse 0 0 0]concat}if 72 Resolution div 72 VResolution div neg scale isls{landplus90{VResolution 72 div vsize mul 0 exch}{Resolution -72 div hsize mul 0}ifelse TR}if Resolution VResolution vsize -72 div 1 add mul TR[matrix currentmatrix{dup dup round sub abs 0.00001 lt{round}if} forall round exch round exch]setmatrix}N /@landscape{/isls true N}B /@manualfeed{statusdict /manualfeed true put}B /@copies{/#copies X}B /FMat[1 0 0 -1 0 0]N /FBB[0 0 0 0]N /nn 0 N /IE 0 N /ctr 0 N /df-tail{ /nn 8 dict N nn begin /FontType 3 N /FontMatrix fntrx N /FontBBox FBB N string /base X array /BitMaps X /BuildChar{CharBuilder}N /Encoding IE N end dup{/foo setfont}2 array copy cvx N load 0 nn put /ctr 0 N[}B /df{ /sf 1 N /fntrx FMat N df-tail}B /dfs{div /sf X /fntrx[sf 0 0 sf neg 0 0] N df-tail}B /E{pop nn dup definefont setfont}B /ch-width{ch-data dup length 5 sub get}B /ch-height{ch-data dup length 4 sub get}B /ch-xoff{ 128 ch-data dup length 3 sub get sub}B /ch-yoff{ch-data dup length 2 sub get 127 sub}B /ch-dx{ch-data dup length 1 sub get}B /ch-image{ch-data dup type /stringtype ne{ctr get /ctr ctr 1 add N}if}B /id 0 N /rw 0 N /rc 0 N /gp 0 N /cp 0 N /G 0 N /sf 0 N /CharBuilder{save 3 1 roll S dup /base get 2 index get S /BitMaps get S get /ch-data X pop /ctr 0 N ch-dx 0 ch-xoff ch-yoff ch-height sub ch-xoff ch-width add ch-yoff setcachedevice ch-width ch-height true[1 0 0 -1 -.1 ch-xoff sub ch-yoff .1 sub]/id ch-image N /rw ch-width 7 add 8 idiv string N /rc 0 N /gp 0 N /cp 0 N{rc 0 ne{rc 1 sub /rc X rw}{G}ifelse}imagemask restore}B /G{{id gp get /gp gp 1 add N dup 18 mod S 18 idiv pl S get exec}loop}B /adv{cp add /cp X}B /chg{rw cp id gp 4 index getinterval putinterval dup gp add /gp X adv}B /nd{/cp 0 N rw exit}B /lsh{rw cp 2 copy get dup 0 eq{pop 1}{ dup 255 eq{pop 254}{dup dup add 255 and S 1 and or}ifelse}ifelse put 1 adv}B /rsh{rw cp 2 copy get dup 0 eq{pop 128}{dup 255 eq{pop 127}{dup 2 idiv S 128 and or}ifelse}ifelse put 1 adv}B /clr{rw cp 2 index string putinterval adv}B /set{rw cp fillstr 0 4 index getinterval putinterval adv}B /fillstr 18 string 0 1 17{2 copy 255 put pop}for N /pl[{adv 1 chg} {adv 1 chg nd}{1 add chg}{1 add chg nd}{adv lsh}{adv lsh nd}{adv rsh}{ adv rsh nd}{1 add adv}{/rc X nd}{1 add set}{1 add clr}{adv 2 chg}{adv 2 chg nd}{pop nd}]dup{bind pop}forall N /D{/cc X dup type /stringtype ne{] }if nn /base get cc ctr put nn /BitMaps get S ctr S sf 1 ne{dup dup length 1 sub dup 2 index S get sf div put}if put /ctr ctr 1 add N}B /I{ cc 1 add D}B /bop{userdict /bop-hook known{bop-hook}if /SI save N @rigin 0 0 moveto /V matrix currentmatrix dup 1 get dup mul exch 0 get dup mul add .99 lt{/QV}{/RV}ifelse load def pop pop}N /eop{SI restore userdict /eop-hook known{eop-hook}if showpage}N /@start{userdict /start-hook known{start-hook}if pop /VResolution X /Resolution X 1000 div /DVImag X /IE 256 array N 0 1 255{IE S 1 string dup 0 3 index put cvn put}for 65781.76 div /vsize X 65781.76 div /hsize X}N /p{show}N /RMat[1 0 0 -1 0 0]N /BDot 260 string N /rulex 0 N /ruley 0 N /v{/ruley X /rulex X V}B /V {}B /RV statusdict begin /product where{pop false[(Display)(NeXT) (LaserWriter 16/600)]{dup length product length le{dup length product exch 0 exch getinterval eq{pop true exit}if}{pop}ifelse}forall}{false} ifelse end{{gsave TR -.1 .1 TR 1 1 scale rulex ruley false RMat{BDot} imagemask grestore}}{{gsave TR -.1 .1 TR rulex ruley scale 1 1 false RMat{BDot}imagemask grestore}}ifelse B /QV{gsave newpath transform round exch round exch itransform moveto rulex 0 rlineto 0 ruley neg rlineto rulex neg 0 rlineto fill grestore}B /a{moveto}B /delta 0 N /tail{dup /delta X 0 rmoveto}B /M{S p delta add tail}B /b{S p tail}B /c{-4 M}B /d{ -3 M}B /e{-2 M}B /f{-1 M}B /g{0 M}B /h{1 M}B /i{2 M}B /j{3 M}B /k{4 M}B /w{0 rmoveto}B /l{p -4 w}B /m{p -3 w}B /n{p -2 w}B /o{p -1 w}B /q{p 1 w} B /r{p 2 w}B /s{p 3 w}B /t{p 4 w}B /x{0 S rmoveto}B /y{3 2 roll p a}B /bos{/SS save N}B /eos{SS restore}B end %%EndProcSet %%BeginProcSet: special.pro %! TeXDict begin /SDict 200 dict N SDict begin /@SpecialDefaults{/hs 612 N /vs 792 N /ho 0 N /vo 0 N /hsc 1 N /vsc 1 N /ang 0 N /CLIP 0 N /rwiSeen false N /rhiSeen false N /letter{}N /note{}N /a4{}N /legal{}N}B /@scaleunit 100 N /@hscale{@scaleunit div /hsc X}B /@vscale{@scaleunit div /vsc X}B /@hsize{/hs X /CLIP 1 N}B /@vsize{/vs X /CLIP 1 N}B /@clip{ /CLIP 2 N}B /@hoffset{/ho X}B /@voffset{/vo X}B /@angle{/ang X}B /@rwi{ 10 div /rwi X /rwiSeen true N}B /@rhi{10 div /rhi X /rhiSeen true N}B /@llx{/llx X}B /@lly{/lly X}B /@urx{/urx X}B /@ury{/ury X}B /magscale true def end /@MacSetUp{userdict /md known{userdict /md get type /dicttype eq{userdict begin md length 10 add md maxlength ge{/md md dup length 20 add dict copy def}if end md begin /letter{}N /note{}N /legal{} N /od{txpose 1 0 mtx defaultmatrix dtransform S atan/pa X newpath clippath mark{transform{itransform moveto}}{transform{itransform lineto} }{6 -2 roll transform 6 -2 roll transform 6 -2 roll transform{ itransform 6 2 roll itransform 6 2 roll itransform 6 2 roll curveto}}{{ closepath}}pathforall newpath counttomark array astore /gc xdf pop ct 39 0 put 10 fz 0 fs 2 F/|______Courier fnt invertflag{PaintBlack}if}N /txpose{pxs pys scale ppr aload pop por{noflips{pop S neg S TR pop 1 -1 scale}if xflip yflip and{pop S neg S TR 180 rotate 1 -1 scale ppr 3 get ppr 1 get neg sub neg ppr 2 get ppr 0 get neg sub neg TR}if xflip yflip not and{pop S neg S TR pop 180 rotate ppr 3 get ppr 1 get neg sub neg 0 TR}if yflip xflip not and{ppr 1 get neg ppr 0 get neg TR}if}{noflips{TR pop pop 270 rotate 1 -1 scale}if xflip yflip and{TR pop pop 90 rotate 1 -1 scale ppr 3 get ppr 1 get neg sub neg ppr 2 get ppr 0 get neg sub neg TR}if xflip yflip not and{TR pop pop 90 rotate ppr 3 get ppr 1 get neg sub neg 0 TR}if yflip xflip not and{TR pop pop 270 rotate ppr 2 get ppr 0 get neg sub neg 0 S TR}if}ifelse scaleby96{ppr aload pop 4 -1 roll add 2 div 3 1 roll add 2 div 2 copy TR .96 dup scale neg S neg S TR}if}N /cp {pop pop showpage pm restore}N end}if}if}N /normalscale{Resolution 72 div VResolution 72 div neg scale magscale{DVImag dup scale}if 0 setgray} N /psfts{S 65781.76 div N}N /startTexFig{/psf$SavedState save N userdict maxlength dict begin /magscale true def normalscale currentpoint TR /psf$ury psfts /psf$urx psfts /psf$lly psfts /psf$llx psfts /psf$y psfts /psf$x psfts currentpoint /psf$cy X /psf$cx X /psf$sx psf$x psf$urx psf$llx sub div N /psf$sy psf$y psf$ury psf$lly sub div N psf$sx psf$sy scale psf$cx psf$sx div psf$llx sub psf$cy psf$sy div psf$ury sub TR /showpage{}N /erasepage{}N /copypage{}N /p 3 def @MacSetUp}N /doclip{ psf$llx psf$lly psf$urx psf$ury currentpoint 6 2 roll newpath 4 copy 4 2 roll moveto 6 -1 roll S lineto S lineto S lineto closepath clip newpath moveto}N /endTexFig{end psf$SavedState restore}N /@beginspecial{SDict begin /SpecialSave save N gsave normalscale currentpoint TR @SpecialDefaults count /ocount X /dcount countdictstack N}N /@setspecial {CLIP 1 eq{newpath 0 0 moveto hs 0 rlineto 0 vs rlineto hs neg 0 rlineto closepath clip}if ho vo TR hsc vsc scale ang rotate rwiSeen{rwi urx llx sub div rhiSeen{rhi ury lly sub div}{dup}ifelse scale llx neg lly neg TR }{rhiSeen{rhi ury lly sub div dup scale llx neg lly neg TR}if}ifelse CLIP 2 eq{newpath llx lly moveto urx lly lineto urx ury lineto llx ury lineto closepath clip}if /showpage{}N /erasepage{}N /copypage{}N newpath }N /@endspecial{count ocount sub{pop}repeat countdictstack dcount sub{ end}repeat grestore SpecialSave restore end}N /@defspecial{SDict begin} N /@fedspecial{end}B /li{lineto}B /rl{rlineto}B /rc{rcurveto}B /np{ /SaveX currentpoint /SaveY X N 1 setlinecap newpath}N /st{stroke SaveX SaveY moveto}N /fil{fill SaveX SaveY moveto}N /ellipse{/endangle X /startangle X /yrad X /xrad X /savematrix matrix currentmatrix N TR xrad yrad scale 0 0 1 startangle endangle arc savematrix setmatrix}N end %%EndProcSet TeXDict begin 39158280 55380996 1000 600 600 (final.dvi) @start %DVIPSBitmapFont: Fa msbm10 10 1 /Fa 1 79 df78 D E %EndDVIPSBitmapFont %DVIPSBitmapFont: Fb cmr5 5 2 /Fb 2 51 df<1360EA01E0120F12FF12F11201B3A3387FFF80A2111C7B9B1C>49 DI E %EndDVIPSBitmapFont %DVIPSBitmapFont: Fc cmmi5 5 3 /Fc 3 111 df<137013F8A213F013E01300A6EA0F80EA1FC0EA31E01261A2EAC3C01203 EA0780A3EA0F001308EA1E18A213301370EA0FE0EA07800D1D7D9C16>105 D 107 D<380F03F0383F87FC3833DC1EEA63F8EAC3F013E0EA03C0A248485AA3EC7820D80F 00136014F015C014F1001EEB7F80000CEB3E001B127D9125>110 D E %EndDVIPSBitmapFont %DVIPSBitmapFont: Fd cmr8 8 28 /Fd 28 122 df<003C13F0387E01F838FF03FCA2EB83FEA2EA7F81383D80F600011306A3 0003130EEB000CA248131C00061318000E13384813704813E0387001C00060138017157E AD23>34 D<123C127E12FFA4127E123C08087A8714>46 D57 D<4A7E4A7EA34A7EA24A7EA3EC1BF81419A2EC30FCA2EC70FEEC607EA24A7EA349 486C7EA2010380EC000FA201066D7EA3496D7EA2011FB57EA29038180001496D7EA34914 7EA201E0147F4980A20001ED1F801203000716C0D80FF0EC3FE0D8FFFC0103B5FCA2302F 7EAE35>65 D75 D80 D<007FB712F8A29039000FC003007C150000701638A2 00601618A200E0161CA248160CA5C71500B3A94A7E011FB512E0A22E2D7EAC33>84 D91 D<0003130C48131C000E133848 13704813E0003013C0EA700100601380A2EAE00300C01300A300DE137800FF13FCEB83FE A2EA7F81A2383F00FC001E1378171577AD23>II<13FF000713C0380F01F0381C00F8003F137C80A2143F001E7FC7FCA4EB07FF13 7F3801FE1FEA07F0EA1FC0EA3F80EA7F00127E00FE14065AA3143F7E007E137F007FEBEF 8C391F83C7FC390FFF03F83901FC01E01F207D9E23>97 DI<15F8141FA214011400ACEB0FE0EB7FF83801F81E3803E0073807C003 380F8001EA1F00481300123E127EA25AA9127C127EA2003E13017EEB8003000F13073903 E00EFC3A01F03CFFC038007FF090391FC0F800222F7EAD27>100 DII<013F13F890 38FFC3FE3903E1FF1E3807807C000F140C391F003E00A2003E7FA76C133EA26C6C5A0007 1378380FE1F0380CFFC0D81C3FC7FC90C8FCA3121E121F380FFFF814FF6C14C04814F039 1E0007F848130048147C12F848143CA46C147C007C14F86CEB01F06CEB03E03907E01F80 3901FFFE0038003FF01F2D7E9D23>II< EA0780EA0FC0EA1FE0A4EA0FC0EA0780C7FCA8EA07C012FFA2120F1207B3A5EA0FE0EAFF FCA20E2E7EAD14>I108 D<2607C07FEB07F03BFFC3FFC03FFC903AC783F0783F3C0FCE01F8E01F803B07DC00F9C0 0F01F8D9FF8013C04990387F000749137EA249137CB2486C01FEEB0FE03CFFFE0FFFE0FF FEA2371E7E9D3C>I<3807C0FE39FFC3FF809038C703E0390FDE01F0EA07F8496C7EA25B A25BB2486C487E3AFFFE1FFFC0A2221E7E9D27>II< 3807C0FE39FFC7FF809038CF03E0390FDC01F03907F800FC49137E49133E49133FED1F80 A3ED0FC0A8151F1680A2ED3F00A26D137E6D137C5D9038FC01F09038CE07E09038C7FF80 D9C1FCC7FC01C0C8FCA9487EEAFFFEA2222B7E9D27>I<380781F838FF87FEEB8E3FEA0F 9CEA07B813B0EBF01EEBE000A45BB0487EB5FCA2181E7E9D1C>114 D<3801FE183807FFB8381E01F8EA3C00481378481338A21418A27E7EB41300EA7FF06CB4 FC6C13C06C13F0000113F838001FFC130138C0007E143EA26C131EA27EA26C133CA26C13 7838FF01F038E3FFC000C0130017207E9E1C>I<1360A413E0A312011203A21207121FB5 12F0A23803E000AF1418A714383801F03014703800F860EB3FE0EB0F80152A7FA81B>I< 3AFFFC07FF80A23A0FF003FC000003EB01F0000114C06D485A000091C7FCEB7C06EB3E0E 6D5A14B8EB0FB0EB07E013036D7E497E1307EB067C497EEB1C1F01387FEB700F496C7E6E 7ED803C07F00076D7E391FE003FC3AFFF007FFC0A2221D7F9C25>120 D<3AFFFC01FFC0A23A0FE0007E000007147C1538000314306D137000011460A26C6C5BA2 EBFC01017C5BEB7E03013E90C7FCA2EB1F06A2148EEB0F8CA2EB07D8A2EB03F0A36D5AA2 6D5AA2495AA2130391C8FC1278EAFC06A25B131CEA7838EA7070EA3FE0EA0F80222B7F9C 25>I E %EndDVIPSBitmapFont %DVIPSBitmapFont: Fe cmr6 6 1 /Fe 1 50 df<13E01201120712FF12F91201B3A7487EB512C0A212217AA01E>49 D E %EndDVIPSBitmapFont %DVIPSBitmapFont: Ff msam10 10 2 /Ff 2 33 df<007FB812F8B912FCA300F0CA123CB3B3ACB912FCA36C17F836387BB741> 3 D<1938A285A28501E0DA01C0130F486C4A6C7F486C4A6CEB0380486C4A6CEB01C0486C 4A6C14E0261FBF80D97F7EEB00F0263F1FC0D9FE3F1478297E07E001F81FB512FE486C6C 48486C14FF486C6C48487E296000FC0FC00114FEC7267E1F80C812786E48C912F0DA1FFE ED01E06E4816C06E48ED03806E48ED0700DA00C05D92C9120E61A261A2481C7CA253>32 D E %EndDVIPSBitmapFont %DVIPSBitmapFont: Fg cmbx10 10 34 /Fg 34 122 df<913803FFC0027F13F00103B512FC010FEB00FED93FF8133FD97FE0EBFF 8049485A5A1480484A13C04A6C1380A36F1300167E93C7FCA592383FFFC0B8FCA4000390 C7FCB3ABB5D8FC3F13FFA4303A7EB935>12 D46 D<141E143E14FE1307133FB5FCA313CFEA000FB3B3A6 007FB61280A4213779B630>49 DIII<001C15C0D81F80130701F8137F90B61280A216005D5D15F05D15804AC7FC 14F090C9FCA8EB07FE90383FFFE090B512F89038FC07FC9038E003FFD98001138090C713 C0120EC813E0157F16F0A216F8A21206EA3F80EA7FE012FF7FA44914F0A26C4813FF90C7 13E0007C15C06C5B6C491380D9C0071300390FF01FFE6CB512F8000114E06C6C1380D90F F8C7FC25387BB630>II<123C123EEA 3FE090B71280A41700485D5E5E5EA25E007CC7EA0FC000784A5A4BC7FC00F8147E48147C 15FC4A5A4A5AC7485A5D140F4A5A143F92C8FC5C147E14FE1301A2495AA31307A2130F5C A2131FA5133FA96D5A6D5A6D5A293A7BB830>I<49B47E010F13F0013F13FC9038FE01FF 3A01F8007F804848EB3FC04848EB1FE0150F485AED07F0121FA27FA27F7F01FEEB0FE0EB FF809138E01FC06CEBF03F02FC13809138FF7F006C14FC6C5C7E6C14FE6D7F6D14C04914 E048B612F0EA07F848486C13F8261FE01F13FC383FC007EB8001007F6D13FE90C7123F48 140F48140715031501A21500A216FC7E6C14016D14F86C6CEB03F06D13076C6CEB0FE0D8 0FFEEB7FC00003B61200C614FC013F13F00103138027387CB630>III65 D67 DI76 D<003FB91280A4D9F800EBF003D87FC09238 007FC049161F007EC7150FA2007C1707A200781703A400F818E0481701A4C892C7FCB3AE 010FB7FCA43B387DB742>84 D97 D<903801FFC0010F13FC017F13FFD9FF80 13802603FE0013C048485AEA0FF8121F13F0123F6E13804848EB7F00151C92C7FC12FFA9 127FA27F123FED01E06C7E15036C6CEB07C06C6C14806C6C131FC69038C07E006DB45A01 0F13F00101138023257DA42A>99 DI<903803FF80011F13F0017F13FC3901FF83FE3A03FE007F804848 133F484814C0001FEC1FE05B003FEC0FF0A2485A16F8150712FFA290B6FCA301E0C8FCA4 127FA36C7E1678121F6C6C14F86D14F000071403D801FFEB0FE06C9038C07FC06DB51200 010F13FC010113E025257DA42C>I<161FD907FEEBFFC090387FFFE348B6EAEFE02607FE 07138F260FF801131F48486C138F003F15CF4990387FC7C0EEC000007F81A6003F5DA26D 13FF001F5D6C6C4890C7FC3907FE07FE48B512F86D13E0261E07FEC8FC90CAFCA2123E12 3F7F6C7E90B512F8EDFF8016E06C15F86C816C815A001F81393FC0000F48C8138048157F 5A163FA36C157F6C16006D5C6C6C495AD81FF0EB07FCD807FEEB3FF00001B612C06C6C91 C7FC010713F02B377DA530>103 D<13FFB5FCA412077EAFED7FC0913803FFF8020F13FE 91381F03FFDA3C01138014784A7E4A14C05CA25CA291C7FCB3A3B5D8FC3F13FFA4303A7D B935>II<13FFB5FCA412077EAF92380FFFE0A4923803FC0016F0ED0F E0ED1F804BC7FC157E5DEC03F8EC07E04A5A141FEC7FE04A7E8181A2ECCFFEEC0FFF496C 7F806E7F6E7F82157F6F7E6F7E82150F82B5D8F83F13F8A42D3A7EB932>107 D<13FFB5FCA412077EB3B3ACB512FCA4163A7DB91B>I<01FED97FE0EB0FFC00FF902601 FFFC90383FFF80020701FF90B512E0DA1F81903983F03FF0DA3C00903887801F000749DA CF007F00034914DE6D48D97FFC6D7E4A5CA24A5CA291C75BB3A3B5D8FC1FB50083B512F0 A44C257DA451>I<01FEEB7FC000FF903803FFF8020F13FE91381F03FFDA3C0113800007 13780003497E6D4814C05CA25CA291C7FCB3A3B5D8FC3F13FFA430257DA435>I<903801 FFC0010F13F8017F13FFD9FF807F3A03FE003FE048486D7E48486D7E48486D7EA2003F81 491303007F81A300FF1680A9007F1600A3003F5D6D1307001F5DA26C6C495A6C6C495A6C 6C495A6C6C6CB45A6C6CB5C7FC011F13FC010113C029257DA430>I<9038FE03F000FFEB 0FFEEC3FFF91387C7F809138F8FFC000075B6C6C5A5CA29138807F80ED3F00150C92C7FC 91C8FCB3A2B512FEA422257EA427>114 D<90383FF0383903FFFEF8000F13FF381FC00F 383F0003007E1301007C130012FC15787E7E6D130013FCEBFFE06C13FCECFF806C14C06C 14F06C14F81203C614FC131F9038007FFE140700F0130114007E157E7E157C6C14FC6C14 F8EB80019038F007F090B512C000F8140038E01FF81F257DA426>I<130FA55BA45BA25B 5BA25A1207001FEBFFE0B6FCA3000390C7FCB21578A815F86CEB80F014816CEBC3E09038 3FFFC06D1380903803FE001D357EB425>I119 D121 D E %EndDVIPSBitmapFont %DVIPSBitmapFont: Fh lasy10 10 2 /Fh 2 60 df<003FB712FEB9FCA300F0C9120FB3B3A4B9FCA4303079B43E>50 D59 D E %EndDVIPSBitmapFont %DVIPSBitmapFont: Fi cmex10 10 1 /Fi 1 27 df<161E167EED01FE1507ED0FF8ED3FE0ED7FC0EDFF80913801FE004A5A4A5A 5D140F4A5A5D143F5D147F92C7FCA25C5CB3B3B3A313015CA3495AA213075C495AA2495A 495A137F49C8FC485A485AEA07F0EA1FE0485AB4C9FC12FCA2B4FCEA3FC06C7EEA07F0EA 03FC6C7E6C7E6D7E133F6D7E6D7EA26D7E801303A26D7EA3801300B3B3B3A38080A28114 3F81141F816E7E1407816E7E6E7E913800FF80ED7FC0ED3FE0ED0FF8ED07FE1501ED007E 161E27C675823E>26 D E %EndDVIPSBitmapFont %DVIPSBitmapFont: Fj cmr7 7 14 /Fj 14 58 df<90383FFFFCA2010090C7FC147EA5903803FF80013F13F89038FC7E7ED8 03E0EB0F80D80FC0EB07E0D81F00EB01F04815F8007EEC00FCA248157EA6007E15FCA26C EC01F86C15F0D80FC0EB07E0D803E0EB0F80D800FCEB7E0090383FFFF801031380D9007E C7FCA514FF013F13FCA227287DA72F>8 D<1306130C13181330136013E0EA01C0EA0380 A2EA07005A120E121EA2121C123CA35AA512F85AAB7E1278A57EA3121C121EA2120E120F 7EEA0380A2EA01C0EA00E0136013301318130C13060F3B7AAB1A>40 D<12C012607E7E7E120E7EEA0380A2EA01C013E0120013F0A213701378A3133CA5133E13 1EAB133E133CA51378A3137013F0A213E0120113C0EA0380A2EA0700120E120C5A5A5A5A 0F3B7DAB1A>I<140EB3A2B812E0A3C7000EC8FCB3A22B2B7DA333>43 D48 D<13381378EA01F8121F12FE12E01200B3AB487EB512F8A215267BA521 >I<13FF000313E0380E03F0381800F848137C48137E00787F12FC6CEB1F80A4127CC7FC 15005C143E147E147C5C495A495A5C495A010EC7FC5B5B903870018013E0EA0180390300 030012065A001FB5FC5A485BB5FCA219267DA521>I<13FF000313E0380F01F8381C007C 0030137E003C133E007E133FA4123CC7123E147E147C5C495AEB07E03801FF8091C7FC38 0001E06D7E147C80143F801580A21238127C12FEA21500485B0078133E00705B6C5B381F 01F03807FFC0C690C7FC19277DA521>I<1438A2147814F81301A2130313071306130C13 1C131813301370136013C012011380EA03005A120E120C121C5A12305A12E0B612E0A2C7 EAF800A7497E90383FFFE0A21B277EA621>I<0018130C001F137CEBFFF85C5C1480D819 FCC7FC0018C8FCA7137F3819FFE0381F81F0381E0078001C7F0018133EC7FC80A21580A2 1230127C12FCA3150012F00060133E127000305B001C5B380F03E03803FFC0C648C7FC19 277DA521>I I<1230123C003FB512E0A215C0481480A239700007000060130E140C48131C5C5CC75A5C 1301495AA249C7FC5B130E131EA3133E133CA2137CA413FCA813781B287DA621>I<137F 3803FFE0380781F8380E007C48131E5A801278A3127C007E131EEA3F80EBE03C6C6C5A38 0FFCF03807FFC06C5BC613E0487F38079FFC380F07FEEA1E0348C67E48133FEC1F804813 0FA21407A315001278140E6C5B6C5B380F80F03803FFE0C66CC7FC19277DA521>I<137F 3801FFC03807C1E0380F0070001E1378003E7F003C133E007C131EA200FC131FA41580A4 007C133FA2123C003E137F121E380F01DF3807FF9F3801FE1FD8001013001300A2143E12 3C007E133CA25C5C007C5B383003C0381C0780D80FFFC7FCEA03F819277DA521>I E %EndDVIPSBitmapFont %DVIPSBitmapFont: Fk cmmi7 7 13 /Fk 13 120 df<137001F81338157CA248485BA44848485AA44848485AA44848485AEDC1 80A3001F90380F8300A2141F9038C03786393FE0E7CC9038FFC3FC393E7F00F090C9FC5A A45AA45A5A21267D9928>22 DI99 D<130E131F5BA2133E131C90C7FCA7EA 03E0487EEA0C78EA187C1230A212605B12C0A2EA01F0A3485AA2485AA2EBC180EA0F81A2 381F0300A213066C5A131CEA07F06C5A11287DA617>105 D<1407EC0F80141FA2150014 0E91C7FCA7EB03E0EB07F8EB0C3C1318EB303E136013C0A248485AA2C7FCA25CA4495AA4 495AA4495AA4495AA21238D87C1FC7FC12FC133E485AEA70F8EA7FE0EA1F80193380A61B >I<133EEA07FEA2EA007CA213FCA25BA21201A25BA21203EC07809038E01FC0EC386000 07EB61E014C3EBC187EBC307D80FC613C09038CC038001B8C7FC13E0487E13FEEB3F80EB 0FC0486C7E1303003E1460A2127EECC0C0127CECC18012FC903801E30038F800FE007013 7C1B297CA723>I<137CEA0FFCA2EA00F8A21201A213F0A21203A213E0A21207A213C0A2 120FA21380A2121FA21300A25AA2123EA2127EA2EA7C18A3EAF830A21320EA786013C0EA 3F80EA0F000E297EA715>I<3B07801FC007E03B0FE07FF01FF83B18F0E0F8783C3B30F1 807CE03E903AFB007D801ED860FEEB3F005B49133E00C14A133E5B1201A24848495BA35F 4848485A1830EE01F0A23C0F8003E003E060A218C0933801E180271F0007C013E3933800 FF00000E6D48137C341B7D993B>I<3907801FC0390FE07FF03918F0E0F83930F1807CEB FB00D860FE133C5B5B00C1147C5B1201A248485BA34A5AEA07C01660EC03E0A23A0F8007 C0C0A2EDC180913803C300D81F0013C7EC01FE000EEB00F8231B7D9929>II< 131C133EA25BA45BA4485AB512E0A23801F000485AA4485AA4485AA448C7FC1460A214C0 123EEB0180EB0300EA1E06EA1F1CEA0FF8EA03E013267EA419>116 DI119 D E %EndDVIPSBitmapFont %DVIPSBitmapFont: Fl cmsy7 7 3 /Fl 3 83 df0 D<1338A50060130C00F8133E00FC137E00FE13 FE383FBBF83807FFC000011300EA007C48B4FC000713C0383FBBF838FE38FE00FC137E00 F8133E0060130C00001300A517197B9A22>3 D<0103B512F8013FECFF8090B712E02703 F078007F260F80F8EB0FF8D81E001403481501007C1500127812F812E0C7485C01011401 5F16035F4A495A01034AC7FC161E1678ED03F09138C0FFC0902607C3FEC8FCA2EC80FF01 0F7F6F7E151F02007F496D7E131E013E6D7E1503013C6E1370017C010114F09338FC01E0 0178903900FE038001F89138FF0F0049EC7FFE4848EC3FF849EC1FC034297EA739>82 D E %EndDVIPSBitmapFont %DVIPSBitmapFont: Fm cmmi10 10 35 /Fm 35 122 df22 D<027FB512C00103B612E0130F5B017F15C09026FF81FEC7FC39 01FC007E48487F485A497F484880485AA248C7FCA2127EA2153F00FE92C7FC5AA25D157E 5A5DA24A5AA24A5A007C495A5D003C495A003E013FC8FC6C137C380F81F83803FFE0C66C C9FC2B257DA32F>27 D<121C127FEAFF80A5EA7F00121C0909798817>58 D<121C127FEAFF80A213C0A3127F121C1200A412011380A2120313005A1206120E5A5A5A 12600A19798817>I I<126012FCB4FCEA7FC0EA1FF0EA07FCEA01FF38007FC0EB1FF0EB07FCEB01FF9038007F C0EC1FF0EC07FCEC01FF9138007FC0ED1FF0ED07FCED01FF9238007FC0EE1FF0EE07FCEE 01FF9338007F80EF1FC0A2EF7F80933801FF00EE07FCEE1FF0EE7FC04B48C7FCED07FCED 1FF0ED7FC04A48C8FCEC07FCEC1FF0EC7FC04948C9FCEB07FCEB1FF0EB7FC04848CAFCEA 07FCEA3FF0EA7FC048CBFC12FC1270323279AD41>62 D<9339FF8001C0030F13E0037F90 38F80380913A01FF807E07913A07F8000F0FDA1FE0EB079FDA3F80903803BF0002FFC76C B4FCD901FC80495A4948157E495A495A4948153E017F163C49C9FC5B1201484816385B12 07485A1830121F4993C7FCA2485AA3127F5BA312FF90CCFCA41703A25F1706A26C160E17 0C171C5F6C7E5F001F5E6D4A5A6C6C4A5A16076C6C020EC8FC6C6C143C6C6C5C6CB4495A 90393FE00FC0010FB5C9FC010313FC9038007FC03A3D7CBA3B>67 D<0103B7FC4916E018F8903B0007F80007FE4BEB00FFF03F80020FED1FC0180F4B15E0F0 07F0021F1503A24B15F81801143F19FC5DA2147FA292C8FCA25C18035CA2130119F84A15 07A2130319F04A150FA2010717E0181F4A16C0A2010FEE3F80A24AED7F00187E011F16FE 4D5A4A5D4D5A013F4B5A4D5A4A4A5A057FC7FC017F15FEEE03FC91C7EA0FF049EC7FC0B8 C8FC16FC16C03E397DB845>I<0103B812E05BA290260007F8C7123F4B140FF003C0140F 18015DA2141FA25D1980143FA25D1760027F14E095C7FC92C75AA24A1301A24A495A1607 0101141F91B6FC94C8FCA2903903FC001F824A130EA21307A24A130CA2010F141CA24A90 C9FCA2131FA25CA2133FA25CA2137FA291CBFC497EB612C0A33B397DB835>70 DI<902603FFF893383FFF80496081D900079438FF 80000206DC01BFC7FCA2020E4C5A1A7E020C1606190CDA1C7E16FE4F5A02181630A20238 166162023016C1F00181DA703F158395380303F002601506A202E0ED0C076202C0151818 3001016D6C140F06605B028015C0A20103923801801FDD03005B140092380FC00649173F 4D91C8FC01065DA2010E4B5B4D137E130C6F6C5A011C17FEDCE1805B011802E3C7FCA201 3802E6130104EC5C1330ED03F8017016034C5C01F05CD807FC4C7EB500E0D9C007B512F0 1680150151397CB851>77 D<92391FE00380DBFFFC130002036D5A91390FE01F8F91393F 0007DF027EEB01FE02F81300495A4948147E177C4948143C495AA2011F153891C8FCA349 1530A28094C7FC80806D7E14FEECFFE06D13FE6DEBFFC06D14F06D806D80021F7F02037F EC003F03037F1500167F163F161FA3120C160FA2001C151F94C7FCA3003C153EA25E003E 5D127E007F4A5A6D495A6DEB0FC0D8F9F0495AD8F0FE01FEC8FC39E03FFFF8010F13E0D8 C00190C9FC313D7CBA33>83 D<1460A5120CAC146E147EEB03FE131F13FF120F123FB512 F814E0EBFE6013F01380EAFC0012EC120CB3A4146E147EEB03FE131F13FF120F123FB512 F814E0EBFE6013F01380EAFC0012EC120CA61400A5174E7CBB20>93 D<147E903803FF8090390FC1C38090391F00EFC0017E137F49133F485A4848EB1F801207 5B000F143F48481400A2485A5D007F147E90C7FCA215FE485C5AA214015D48150CA21403 EDF01C16181407007C1538007E010F1330003E131F027B13706C01E113E03A0F83C0F9C0 3A03FF007F80D800FCEB1F0026267DA42C>97 D<133FEA1FFFA3C67E137EA313FE5BA312 015BA312035BA31207EBE0FCEBE3FF9038E707C0390FFE03E09038F801F001F013F8EBE0 00485A15FC5BA2123F90C7FCA214015A127EA2140312FE4814F8A2140715F05AEC0FE0A2 15C0EC1F80143F00781400007C137E5C383C01F86C485A380F07C06CB4C7FCEA01FC1E3B 7CB924>I<163FED1FFFA3ED007F167EA216FEA216FCA21501A216F8A21503A216F0A215 07A2027E13E0903803FF8790380FC1CF90381F00EF017EEB7FC049133F485A4848131F00 0715805B000F143F485A1600485A5D127F90C7127EA215FE5A485CA21401A248ECF80CA2 1403161CEDF0181407007C1538007E010F1330003E131F027B13706C01E113E03A0F83C0 F9C03A03FF007F80D800FCEB1F00283B7DB92B>100 DI<16F8ED03FEED0F8792 381F0F80ED3E3F167F157CA215FC1700161C4A48C7FCA414035DA414075DA20107B512F0 A39026000FE0C7FC5DA4141F5DA4143F92C8FCA45C147EA514FE5CA413015CA4495AA45C 1307A25C121E123F387F8F80A200FF90C9FC131E12FEEA7C3CEA7878EA1FF0EA07C0294C 7CBA29>II<14E0EB03F8A21307A314F0EB01 C090C7FCAB13F8EA03FEEA070F000E1380121C121812381230EA701F1260133F00E01300 12C05BEA007EA213FE5B1201A25B12035BA20007131813E01438000F133013C01470EB80 6014E014C01381EB838038078700EA03FEEA00F815397EB71D>105 D<150FED3F80A2157FA31600151C92C7FCABEC0F80EC3FE0ECF0F0903801C0F849487E14 005B130E130C131CEB1801133801305BA2EB0003A25DA21407A25DA2140FA25DA2141FA2 5DA2143FA292C7FCA25CA2147EA214FEA25CA21301001E5B123F387F83F0A238FF87E049 5A00FE5BD87C1FC8FCEA707EEA3FF8EA0FC0214981B722>IIIIII<90 390F8003F090391FE00FFC903939F03C1F903A70F8700F80903AE0FDE007C09038C0FF80 030013E00001491303018015F05CEA038113015CA2D800031407A25CA20107140FA24A14 E0A2010F141F17C05CEE3F80131FEE7F004A137E16FE013F5C6E485A4B5A6E485A90397F 700F80DA383FC7FC90387E1FFCEC07E001FEC9FCA25BA21201A25BA21203A25B1207B512 C0A32C3583A42A>I<02FC13C0903803FF0190380F838390383F01C790397E00EF804913 7F485A4848133F000715005B485A001F5C157E485AA2007F14FE90C75AA3481301485CA3 1403485CA314075D140F127C141F007E495A003E137F381F01EF380F839F3903FF1F80EA 00FC1300143F92C7FCA35C147EA314FE5C130190387FFFF0A322357DA425>I<3903E001 F83907F807FE390E3C1E07391C3E381F3A183F703F800038EBE07F0030EBC0FF00705B00 601500EC007E153CD8E07F90C7FCEAC07EA2120013FE5BA312015BA312035BA312075BA3 120F5BA3121F5B0007C9FC21267EA425>I<14FF010313C090380F80F090383E00380178 131C153C4913FC0001130113E0A33903F000F06D13007F3801FFE014FC14FF6C14806D13 C0011F13E013039038003FF014071403001E1301127FA24814E0A348EB03C012F800E0EB 07800070EB0F006C133E001E13F83807FFE0000190C7FC1E267CA427>II<13F8D803FE1438D8070F147C000E6D13 FC121C1218003814011230D8701F5C12601503EAE03F00C001005B5BD8007E1307A201FE 5C5B150F1201495CA2151F120349EC80C0A2153F1681EE0180A2ED7F0303FF130012014A 5B3A00F8079F0E90397C0E0F1C90393FFC07F8903907F001F02A267EA430>I<01F8EB03 C0D803FEEB07E0D8070F130F000E018013F0121C12180038140700301403D8701F130112 601500D8E03F14E000C090C7FC5BEA007E16C013FE5B1501000115805B15031600120349 5B1506150E150C151C151815385D00015C6D485A6C6C485AD97E0FC7FCEB1FFEEB07F024 267EA428>I<903907E001F090391FF807FC9039783E0E0F9039E01F1C1FD801C0903838 3F803A03800FF07F0100EBE0FF5A000E4A1300000C157E021F133C001C4AC7FC1218A2C7 123FA292C8FCA25CA2147EA214FEA24A130CA20101141C001E1518003F5BD87F81143801 835C00FF1560010714E03AFE0E7C01C0D87C1C495A2778383E0FC7FC391FF00FFC3907C0 03F029267EA42F>120 D<13F8D803FE1470D8070F14F8000EEB8001121C121800381403 003015F0EA701F1260013F130700E0010013E012C05BD8007E130F16C013FE5B151F0001 15805BA2153F000315005BA25D157EA315FE5D1401000113033800F80790387C1FF8EB3F F9EB0FE1EB00035DA2000E1307D83F805B007F495AA24A5A92C7FCEB003E007C5B00705B 6C485A381E07C06CB4C8FCEA01FC25367EA429>I E %EndDVIPSBitmapFont %DVIPSBitmapFont: Fn cmsy10 10 25 /Fn 25 107 df<0060150600F8150F6C151F007E153F6C157E6C6C14FC6C6CEB01F86C6C EB03F06C6CEB07E06C6CEB0FC06C6CEB1F80017EEB3F006D137E6D6C5A90380FC1F89038 07E3F0903803F7E06DB45A6D5B6EC7FCA24A7E497F903803F7E0903807E3F090380FC1F8 90381F80FC90383F007E017E7F49EB1F804848EB0FC04848EB07E04848EB03F04848EB01 F84848EB00FC48C8127E007E153F48151F48150F00601506282874A841>2 D15 D<020FB6128091B712C01303010F1680D91FF8C9FCEB7F8001FECAFCEA01F8485A485A48 5A5B48CBFCA2123EA25AA2127812F8A25AA87EA21278127CA27EA27EA26C7E7F6C7E6C7E 6C7EEA00FEEB7F80EB1FF86DB71280010316C01300020F158091CAFCAE001FB812804817 C0A26C1780324479B441>18 D20 D<126012F812FEEA7F80EA3FE0EA0FF8EA03FEC6 6C7EEB3FE0EB0FF8EB03FE903800FF80EC3FE0EC0FF8EC03FE913800FF80ED3FE0ED0FF8 ED03FE923800FF80EE3FE0EE0FF8EE03FE933800FF80EF3FC0171FEF7F80933801FF00EE 07FCEE1FF0EE7FC04B48C7FCED07FCED1FF0ED7FC04A48C8FCEC07FCEC1FF0EC7FC04948 C9FCEB07FCEB1FF0EB7FC04848CAFCEA07FCEA1FF0EA7FC048CBFC12FC1270CCFCAE007F B81280B912C0A26C1780324479B441>I<126012F0A37EA21278127CA27EA27E7F6C7E6C 7E6C7EEA01FC6CB4FCEB3FC0EB1FF8903807FF80010113F89039007FFFF8020F90B51280 020015C0A2020F1580027F01F8C7FC902601FFF8C8FC01071380D91FF8C9FCEB3FC001FF CAFCEA01FCEA03F0485A485A485A90CBFC123EA25AA2127812F8A25AA31260CCFCAE007F B81280B912C0A26C1780324479B441>23 DI<126012F0A37EA21278127CA27EA27E7F6C7E6C7E6C7EEA01FC6CB4FCEB3F C0EB1FF8903807FF80010113F89039007FFFF8020F90B51280020015C0A2020F1580027F 01F8C7FC902601FFF8C8FC01071380D91FF8C9FCEB3FC001FFCAFCEA01FCEA03F0485A48 5A485A90CBFC123EA25AA2127812F8A25AA31260323279AC41>31 D<181EA4181F84A285180785727EA2727E727E85197E85F11F80F10FC0F107F0007FBA12 FCBCFCA26C19FCCCEA07F0F10FC0F11F80F13F00197E61614E5A4E5AA24E5A61180F96C7 FCA260181EA4482C7BAA53>33 D<173CA2173E171E171F8384717E170384717E717E187C 007FB812FEBAFC856C84CBEA03F0727EF000FEF13F80F11FE0F107F8F101FFA2F107F8F1 1FE0F13F80F1FE00F001F84E5A007FB912C0BA5A96C7FC6C5FCB127C604D5A4D5A601707 4D5A95C8FC5F171E173E173CA248307BAC53>41 D<91381FFFFE91B6FC1303010F14FED9 1FF0C7FCEB7F8001FEC8FCEA01F8485A485A485A5B48C9FCA2123EA25AA2127812F8A25A A2B712FE16FFA216FE00F0C9FCA27EA21278127CA27EA27EA26C7E7F6C7E6C7E6C7EEA00 FEEB7F80EB1FF06DB512FE010314FF1300021F13FE283279AD37>50 D54 D<126012F0AD12FCA412F0AD126006207BA4 00>I<156015F0A21401EB07F190383FFFE0EB7C1FEBF00748486C5AD803C07F4848487E D80F007FA248497E001E14BC153C003E143E141FA248EB1E1F143EA2143CA2147C00FC15 80147814F8A214F0A21301A214E01303A214C0A21307A21480A2130FA214005B007C1500 131EA2D87E3E5BA2D83E3C133E137CA21378001F5C13F8000F14784913F800075C000349 5AEBE0033901F007802603FC1FC7FCEBFFFEEBC7F0D807C0C8FCA25BA26CC9FC21477CBF 2A>59 D<0203B512F0027F14FF49B712E0010F16F890273FC3F00713FED978039038007F FF2601E007020F1380D803C0030313C0D80780030013E0000F177FD81F00EE3FF048EF1F F8003E4A140F5A0078EF07FC00C0010F1503C7FCA24B1401A3141F5DA3023F16F8A292C8 FCF003F0A25C027EED07E0A219C04A150F1980F01F00495A183E6049481578604D5A4948 4A5A4D5A050EC7FC4948143C5FEE01E04948EB07C0043FC8FC91380001FC49EB3FF049B5 128048B500FCC9FC4814E04801FCCAFC3E397FB840>68 D<0307B612FE033FEDFF804AB8 12C0140791260F807EC7FC91263C00FEEC3F004A161E4A491418010194C7FC495A010713 01A2D90FC05B148014000118130390C75BA34B5AA3150F5EA34B5AA293B512FC4B5C604B 14C0037ECAFCA25DA25D1401A24A5AA25D14075D140F5D141F92CBFC5C0006133E003E13 7E007E137CB413FC6D5AEBC1F0EBF1E06CB45A6C90CCFC6C5AEA07F0423C7EB83C>70 D77 D<0203B512FE027FECFFF049B712FC010F16FF 90273FC3F00080D9780302077F2601E0071401D803C06F6C7ED80780163F000F171FEA1F 00484A140F123E5A0078010F5E12C0C7FC4B4A5AA296C7FC021F5D183E4B5C187860023F 4A5A4D5A92C7000FC8FC173EEE03F84AEBFFE0DA7E0313804B48C9FC4B7EECFC036F7F6F 7F0101147F4A80163F707E495A707EA249481307830403151049486E14F0F101E04A6D6C EB03C0011F933880078070EC0F0049C8EBC01E716C5A013E92383FF0F0017EEEFFE0017C 6F1380496F48C7FC01E0ED07F0443B7FB846>82 D<1A801907F10F00023FB712FE49B85A 010F17F0013F17C0494CC7FC2801E00003F0C9FC48481307485A120F48C7485A5A5AA200 FE4A5A5A12F01280C8485AA44BCAFCA415FEA44A5AA44A5AA44A5AA4140F5DA35D141FA2 5D143FA292CBFC5CA2147E14FE5CA2495A5C495A5C0102CCFC41427DBB2D>84 D86 D<0060161800F0163CB3B26C167CA2007C16F8A26CED01F0003F15036C6CEC 07E06C6CEC0FC0D807F0EC3F80D803FE903801FF003A00FFC00FFC6DB55A011F14E00103 91C7FC9038007FF82E347CB137>91 DI102 D<12FCEAFFC0EA07F0EA01FCEA007E7F80131F80130FB3A7801307806D7E6D7E EB007EEC1FF0EC07F8EC1FF0EC7E00495A495A495A5C130F5CB3A7131F5C133F91C7FC13 7E485AEA07F0EAFFC000FCC8FC1D537ABD2A>I<126012F0B3B3B3B3A91260045377BD17> 106 D E %EndDVIPSBitmapFont %DVIPSBitmapFont: Fo cmbx12 14.4 30 /Fo 30 120 df<157815FC14031407141F14FF130F0007B5FCB6FCA2147F13F0EAF800C7 FCB3B3B3A6007FB712FEA52F4E76CD43>49 DI<9138 0FFFC091B512FC0107ECFF80011F15E090263FF8077F9026FF800113FC4848C76C7ED803 F86E7E491680D807FC8048B416C080486D15E0A4805CA36C17C06C5B6C90C75AD801FC16 80C9FC4C13005FA24C5A4B5B4B5B4B13C04B5BDBFFFEC7FC91B512F816E016FCEEFF80DA 000713E0030113F89238007FFE707E7013807013C018E07013F0A218F8A27013FCA218FE A2EA03E0EA0FF8487E487E487EB57EA318FCA25E18F891C7FC6C17F0495C6C4816E001F0 4A13C06C484A1380D80FF84A13006CB44A5A6CD9F0075BC690B612F06D5D011F15800103 02FCC7FCD9001F1380374F7ACD43>I<177C17FEA2160116031607160FA2161F163F167F A216FF5D5DA25D5DED1FBFED3F3F153E157C15FCEC01F815F0EC03E01407EC0FC01580EC 1F005C147E147C5C1301495A495A5C495A131F49C7FC133E5B13FC485A5B485A1207485A 485A90C8FC123E127E5ABA12C0A5C96C48C7FCAF020FB712C0A53A4F7CCE43>I<171F4D 7E4D7EA24D7EA34C7FA24C7FA34C7FA34C7FA24C7FA34C8083047F80167E8304FE804C7E 03018116F8830303814C7E03078116E083030F814C7E031F81168083033F8293C77E4B82 157E8403FE824B800201835D840203834B800207835D844AB87EA24A83A3DA3F80C88092 C97E4A84A2027E8202FE844A82010185A24A820103854A82010785A24A82010F855C011F 717FEBFFFCB600F8020FB712E0A55B547BD366>65 D<932601FFFCEC01C0047FD9FFC013 030307B600F81307033F03FE131F92B8EA803F0203DAE003EBC07F020F01FCC7383FF0FF 023F01E0EC0FF94A01800203B5FC494848C9FC4901F88249498249498249498249498249 90CA7E494883A2484983485B1B7F485B481A3FA24849181FA3485B1B0FA25AA298C7FC5C A2B5FCAE7EA280A2F307C07EA36C7FA21B0F6C6D1980A26C1A1F6C7F1C006C6D606C6D18 7EA26D6C606D6D4C5A6D6D16036D6D4C5A6D6D4C5A6D01FC4C5A6D6DEE7F806D6C6C6C4B C7FC6E01E0EC07FE020F01FEEC1FF80203903AFFE001FFF0020091B612C0033F93C8FC03 0715FCDB007F14E0040101FCC9FC525479D261>67 D70 D73 D82 D<003FBC1280A59126C0 003F9038C0007F49C71607D87FF8060113C001E08449197F49193F90C8171FA2007E1A0F A3007C1A07A500FC1BE0481A03A6C994C7FCB3B3AC91B912F0A553517BD05E>84 DI97 D<913801FFF8021FEBFF8091B612F0010315FC010F9038C00FFE903A1FFE00 01FFD97FFC491380D9FFF05B4817C048495B5C5A485BA2486F138091C7FC486F1300705A 4892C8FC5BA312FFAD127F7FA27EA2EF03E06C7F17076C6D15C07E6E140F6CEE1F806C6D EC3F006C6D147ED97FFE5C6D6CEB03F8010F9038E01FF0010390B55A01001580023F49C7 FC020113E033387CB63C>99 D<4DB47E0407B5FCA5EE001F1707B3A4913801FFE0021F13 FC91B6FC010315C7010F9038E03FE74990380007F7D97FFC0101B5FC49487F4849143F48 4980485B83485B5A91C8FC5AA3485AA412FFAC127FA36C7EA37EA26C7F5F6C6D5C7E6C6D 5C6C6D49B5FC6D6C4914E0D93FFED90FEFEBFF80903A0FFFC07FCF6D90B5128F0101ECFE 0FD9003F13F8020301C049C7FC41547CD24B>I<913803FFC0023F13FC49B6FC010715C0 4901817F903A3FFC007FF849486D7E49486D7E4849130F48496D7E48178048497F18C048 8191C7FC4817E0A248815B18F0A212FFA490B8FCA318E049CAFCA6127FA27F7EA218E06C EE01F06E14037E6C6DEC07E0A26C6DEC0FC06C6D141F6C6DEC3F806D6CECFF00D91FFEEB 03FE903A0FFFC03FF8010390B55A010015C0021F49C7FC020113F034387CB63D>IIII<137F 497E000313E0487FA2487FA76C5BA26C5BC613806DC7FC90C8FCADEB3FF0B5FCA512017E B3B3A6B612E0A51B547BD325>I107 DIII<913801FFE0021F13FE91B612C0010315F0010F90 38807FFC903A1FFC000FFED97FF86D6C7E49486D7F48496D7F48496D7F4A147F48834890 C86C7EA24883A248486F7EA3007F1880A400FF18C0AC007F1880A3003F18006D5DA26C5F A26C5F6E147F6C5F6C6D4A5A6C6D495B6C6D495B6D6C495BD93FFE011F90C7FC903A0FFF 807FFC6D90B55A010015C0023F91C8FC020113E03A387CB643>I<903A3FF001FFE0B501 0F13FE033FEBFFC092B612F002F301017F913AF7F8007FFE0003D9FFE0EB1FFFC602806D 7F92C76C7F4A824A6E7F4A6E7FA2717FA285187F85A4721380AC1A0060A36118FFA2615F 616E4A5BA26E4A5B6E4A5B6F495B6F4990C7FC03F0EBFFFC9126FBFE075B02F8B612E06F 1480031F01FCC8FC030313C092CBFCB1B612F8A5414D7BB54B>I<90397FE003FEB59038 0FFF80033F13E04B13F09238FE1FF89139E1F83FFC0003D9E3E013FEC6ECC07FECE78014 EF150014EE02FEEB3FFC5CEE1FF8EE0FF04A90C7FCA55CB3AAB612FCA52F367CB537> 114 D<903903FFF00F013FEBFE1F90B7FC120348EB003FD80FF81307D81FE0130148487F 4980127F90C87EA24881A27FA27F01F091C7FC13FCEBFFC06C13FF15F86C14FF16C06C15 F06C816C816C81C681013F1580010F15C01300020714E0EC003F030713F015010078EC00 7F00F8153F161F7E160FA27E17E07E6D141F17C07F6DEC3F8001F8EC7F0001FEEB01FE90 39FFC00FFC6DB55AD8FC1F14E0D8F807148048C601F8C7FC2C387CB635>I<143EA6147E A414FEA21301A313031307A2130F131F133F13FF5A000F90B6FCB8FCA426003FFEC8FCB3 A9EE07C0AB011FEC0F8080A26DEC1F0015806DEBC03E6DEBF0FC6DEBFFF86D6C5B021F5B 020313802A4D7ECB34>II119 D E %EndDVIPSBitmapFont %DVIPSBitmapFont: Fp cmr10 10 82 /Fp 82 128 df<011FB512FEA39026001FFEC8FCEC07F8A8EC3FFE0103B512E0D91FF713 FC90397F07F87F01FCEC1F80D803F8EC0FE0D807F06E7ED80FE06E7E001F82D83FC06E7E A2007F8201808000FF1780A7007F170001C05C003F5EA2D81FE04A5A000F5ED807F04A5A D803F84A5AD800FCEC1F80017F027FC7FC90391FF7FFFC0103B512E09026003FFEC8FCEC 07F8A8EC1FFE011FB512FEA331397BB83C>8 D11 DIII22 D<001C131C007F137F39FF80FF80A26D13C0A3007F137F001C131C00001300A400011301 01801380A20003130301001300485B00061306000E130E485B485B485B006013601A197D B92A>34 D<121C127FEAFF80A213C0A3127F121C1200A412011380A2120313005A120612 0E5A5A5A12600A1979B917>39 D<146014E0EB01C0EB0380EB0700130E131E5B5BA25B48 5AA2485AA212075B120F90C7FCA25A121EA2123EA35AA65AB2127CA67EA3121EA2121F7E A27F12077F1203A26C7EA26C7E1378A27F7F130E7FEB0380EB01C0EB00E01460135278BD 20>I<12C07E12707E7E7E120F6C7E6C7EA26C7E6C7EA21378A2137C133C133E131EA213 1F7FA21480A3EB07C0A6EB03E0B2EB07C0A6EB0F80A31400A25B131EA2133E133C137C13 78A25BA2485A485AA2485A48C7FC120E5A5A5A5A5A13527CBD20>I<15301578B3A6007F B812F8B912FCA26C17F8C80078C8FCB3A6153036367BAF41>43 D<121C127FEAFF80A213 C0A3127F121C1200A412011380A2120313005A1206120E5A5A5A12600A19798817>II<121C127FEAFF80A5EA7F00121C0909798817>I48 D III<1538A2157815F8 A2140114031407A2140F141F141B14331473146314C313011483EB030313071306130C13 1C131813301370136013C01201EA038013005A120E120C5A123812305A12E0B712F8A3C7 3803F800AB4A7E0103B512F8A325397EB82A>I<0006140CD80780133C9038F003F890B5 FC5D5D158092C7FC14FC38067FE090C9FCABEB07F8EB3FFE9038780F803907E007E09038 8003F0496C7E12066E7EC87EA28181A21680A4123E127F487EA490C71300485C12E00060 5C12700030495A00385C6C1303001E495A6C6C485A3907E03F800001B5C7FC38007FFCEB 1FE0213A7CB72A>II<12301238123E003FB612E0A3 16C05A168016000070C712060060140E5D151800E01438485C5D5DC712014A5A92C7FC5C 140E140C141C5CA25CA214F0495AA21303A25C1307A2130FA3495AA3133FA5137FA96DC8 FC131E233B7BB82A>III<121C12 7FEAFF80A5EA7F00121CC7FCB2121C127FEAFF80A5EA7F00121C092479A317>I<121C12 7FEAFF80A5EA7F00121CC7FCB2121C127F5A1380A4127F121D1201A412031300A25A1206 A2120E5A121812385A1260093479A317>I<007FB812F8B912FCA26C17F8CCFCAE007FB8 12F8B912FCA26C17F836167B9F41>61 D<1538A3157CA315FEA34A7EA34A6C7EA202077F EC063FA2020E7FEC0C1FA2021C7FEC180FA202387FEC3007A202707FEC6003A202C07F15 01A2D901807F81A249C77F167FA20106810107B6FCA24981010CC7121FA2496E7EA3496E 7EA3496E7EA213E0707E1201486C81D80FFC02071380B56C90B512FEA3373C7DBB3E>65 DI<913A01FF800180020FEBE003027F13F8903A01FF807E07903A03 FC000F0FD90FF0EB039F4948EB01DFD93F80EB00FF49C8127F01FE153F12014848151F48 48150FA248481507A2485A1703123F5B007F1601A35B00FF93C7FCAD127F6DED0180A312 3F7F001F160318006C7E5F6C7E17066C6C150E6C6C5D00001618017F15386D6C5CD91FE0 5C6D6CEB03C0D903FCEB0F80902701FF803FC7FC9039007FFFFC020F13F002011380313D 7BBA3C>III< B812F8A30001903880001F6C90C71201EE00FC177C173C171CA2170CA4170E1706A2ED01 80A21700A41503A21507151F91B5FCA3EC001F15071503A21501A692C8FCAD4813C0B612 C0A32F397DB836>III I<013FB512E0A39039001FFC00EC07F8B3B3A3123FEA7F80EAFFC0A44A5A1380D87F005B 0070131F6C5C6C495A6C49C7FC380781FC3801FFF038007F80233B7DB82B>III< B5933807FFF86E5DA20001F0FC002600DFC0ED1BF8A2D9CFE01533A3D9C7F01563A3D9C3 F815C3A2D9C1FCEC0183A3D9C0FEEC0303A2027F1406A36E6C130CA36E6C1318A26E6C13 30A36E6C1360A26E6C13C0A3913901FC0180A3913900FE0300A2ED7F06A3ED3F8CA2ED1F D8A3ED0FF0A3486C6D5A487ED80FFC6D48497EB500C00203B512F8A2ED018045397DB84C >I III82 D I<003FB812E0A3D9C003EB001F273E0001FE130348EE01F00078160000701770A3006017 30A400E01738481718A4C71600B3B0913807FF80011FB612E0A335397DB83C>IIII89 D<003FB7FCA39039FC0001 FE01C0130349495A003EC7FC003C4A5A5E0038141F00784A5A12704B5A5E006014FF4A90 C7FCA24A5A5DC712074A5AA24A5A5D143F4A5AA24A5A92C8FC5B495AA2495A5C130F4948 EB0180A2495A5C137F495A16034890C7FC5B1203485AEE0700485A495C001F5D48485C5E 4848495A49130FB8FCA329397BB833>II<3901800180000313033907000700000E130E485B001813180038133800301330 0070137000601360A200E013E0485BA400CE13CE39FF80FF806D13C0A3007F137FA2393F 803F80390E000E001A1974B92A>I I97 DIIII<147E903803FF8090380FC1E0EB1F8790 383F0FF0137EA213FCA23901F803C091C7FCADB512FCA3D801F8C7FCB3AB487E387FFFF8 A31C3B7FBA19>IIII< EB01C0EB07F0EB0FF8A5EB07F0EB01C090C7FCAAEB01F813FFA313071301B3B3A2123C12 7E00FF13F01303A214E038FE07C0127C383C0F00EA0FFEEA03F8154984B719>III<2703F00FF0EB1FE000FFD93FFCEB7FF8913AF03F01E0 7E903BF1C01F83803F3D0FF3800FC7001F802603F70013CE01FE14DC49D907F8EB0FC0A2 495CA3495CB3A3486C496CEB1FE0B500C1B50083B5FCA340257EA445>I<3903F00FF000 FFEB3FFCECF03F9039F1C01F803A0FF3800FC03803F70013FE496D7EA25BA35BB3A3486C 497EB500C1B51280A329257EA42E>II<3903F01FE000FFEB7FF89038 F1E07E9039F3801F803A07F7000FC0D803FEEB07E049EB03F04914F849130116FC150016 FEA3167FAA16FEA3ED01FCA26DEB03F816F06D13076DEB0FE001F614C09039F7803F0090 38F1E07E9038F0FFF8EC1FC091C8FCAB487EB512C0A328357EA42E>II<3807E01F00 FFEB7FC09038E1E3E09038E387F0380FE707EA03E613EE9038EC03E09038FC0080491300 A45BB3A2487EB512F0A31C257EA421>II<1318A51338A31378A313F8120112031207001FB5FCB6FC A2D801F8C7FCB215C0A93800FC011580EB7C03017E13006D5AEB0FFEEB01F81A347FB220 >IIIIII<003FB512FCA2EB8003D83E0013F8003CEB07F00038EB0FE012300070EB1FC0 EC3F800060137F150014FE495AA2C6485A495AA2495A495A495AA290387F000613FEA248 5A485A0007140E5B4848130C4848131CA24848133C48C7127C48EB03FC90B5FCA21F247E A325>II<001C131C007F137F39FF80FF80A5397F007F00001C13 1C190978B72A>127 D E %EndDVIPSBitmapFont %DVIPSBitmapFont: Fq cmti10 10 49 /Fq 49 122 df13 D<150C151C153815F0EC01E0EC03C0EC0780 EC0F00141E5C147C5C5C495A1303495A5C130F49C7FCA2133EA25BA25BA2485AA212035B 12075BA2120F5BA2121FA290C8FCA25AA2123EA2127EA2127CA412FC5AAD1278A57EA312 1C121EA2120E7EA26C7E6C7EA212001E5274BD22>40 D<140C140E80EC0380A2EC01C015 E0A2140015F0A21578A4157C153CAB157CA715FCA215F8A21401A215F0A21403A215E0A2 1407A215C0140F1580A2141F1500A2143EA25CA25CA2495AA2495A5C1307495A91C7FC5B 133E133C5B5B485A12035B48C8FC120E5A12785A12C01E527FBD22>I44 D<387FFFF8A2B5FCA214F0150579941E>I<120EEA3F80127F12FF A31300127E123C0909778819>I<15181538157815F0140114031407EC0FE0141F147FEB 03FF90383FEFC0148FEB1C1F13001580A2143FA21500A25CA2147EA214FEA25CA21301A2 5CA21303A25CA21307A25CA2130FA25CA2131FA25CA2133FA291C7FC497EB61280A31D38 77B72A>49 DII<157F913803FFC0020F13E0EC3F8191 387E00F002F81370903903F003F0903807E007EB0FC0EB1F80020013E04914C0017E90C7 FC13FE5B485AA21203485AA2380FE07E9038E3FF809038E783E0391FCE01F09038DC00F8 13F84848137C5B49137EA2485AA290C7FC15FE5A5AA214015D5AA214035DA348495A5D14 0F5D4A5A6C49C7FC127C147C6C485A6C485A6CB45A6C1380D801FCC8FC243A76B72A>54 D<133C137E13FF5AA313FE13FCEA00701300B2120EEA3F80127F12FFA31300127E123C10 2477A319>58 D65 D<0107B612FCEFFF8018C0903B000FF0001FF04BEB07F81703021F15FC17014B14FEA202 3F1400A24B1301A2147F18FC92C7120318F84A140718F04AEC0FE0EF1FC00101ED3F80EF 7F004AEB01FEEE07F849B612E05F9139F80007F0EE01FC01076E7E177F4AEC3F80A2010F 16C0171F5CA2131F173F5CA2133FEF7F805C1800017F5D4C5A91C7485A5F49140FEE1FE0 494A5A00014AB45AB748C7FC16F816C037397BB83A>II<0107B8FCA3903A000FF000034BEB00 7F183E141F181E5DA2143FA25D181C147FA29238000380A24A130718004A91C7FC5E1301 5E4A133E167E49B512FEA25EECF8000107147C163C4A1338A2010F147818E04A13701701 011F16C016004A14031880013F150718004A5CA2017F151E173E91C8123C177C4915FC4C 5A4914070001ED7FF0B8FCA25F38397BB838>69 D<0107B712FEA3903A000FF000074B13 00187C021F153CA25DA2143FA25D1838147FA292C8FCEE03804A130718004A91C7FCA201 015CA24A131E163E010314FE91B5FC5EA2903807F800167C4A1378A2130FA24A1370A201 1F14F0A24A90C8FCA2133FA25CA2137FA291CAFCA25BA25B487EB6FCA337397BB836>I< 0103B512F8A390390007F8005DA2140FA25DA2141FA25DA2143FA25DA2147FA292C7FCA2 5CA25CA21301A25CA21303A25CA21307A25CA2130FA25CA2131FA25CA2133FA25CA2137F A291C8FC497EB6FCA25C25397CB820>73 D<0103B500F890387FFFE0A21AC090260007F8 C7380FFC004B15E061020F4BC7FC183E4B5C18F0021F4A5A4D5A4BEB0F804DC8FC023F14 3C5F4B5B4C5A027FEB07C04CC9FCED001E5E4A5BED01FCECFE0315070101497E151FECFC 7C4B7E903903FDE07FDAFFC07F1580ED003F49488014F84A131F83130F160F4A80160701 1F81A24A130383133F16014A80A2017F6E7EA291C8FC494A7F007F01FE011F13FCB55CA2 43397CB840>75 D<0107B512FCA25E9026000FF8C7FC5D5D141FA25DA2143FA25DA2147F A292C8FCA25CA25CA21301A25CA21303A25CA21307A25CA2130F170C4A141CA2011F153C 17384A1478A2013F157017F04A14E01601017F140317C091C71207160F49EC1F80163F49 14FF000102071300B8FCA25E2E397BB834>I<902607FFF8923807FFF0614F13E0D9000F EFF0004F5AA2021F167FF1EFC0141DDA1CFCEC01CF023C16DF9538039F800238ED071FA2 0278ED0E3F97C7FC0270151CA202F04B5AF0707E14E0037E14E0010117FE4D485A02C0EC 0380A20103ED0701610280140EA20107ED1C0305385B14006F137049160705E05B010EEC 01C0A2011E913803800F61011CEC0700A2013C020E131F4C5C1338ED1FB80178163F04F0 91C8FC01705CA201F04A5B187E00015DD807F816FEB500C09039007FFFFC151E150E4C39 7AB84A>I<902603FFF891B512E0A281D90007923807F8006F6E5A61020F5E81DA0E7F5D A2021E6D1307033F92C7FC141C82DA3C1F5C70130EEC380FA202786D131E0307141C1470 82DAF003143C70133814E0150101016E1378030014705C8201036E13F0604A1480163F01 0715C1041F5B91C7FC17E149EC0FE360010E15F31607011E15FF95C8FC011C80A2013C80 5F1338160013785F01F8157CEA03FC267FFFE0143CB51538A243397CB83E>I<0107B612 F817FF1880903B000FF0003FE04BEB0FF0EF03F8141FEF01FC5DA2023F15FEA25DA2147F EF03FC92C7FCA24A15F817074A15F0EF0FE01301EF1FC04AEC3F80EFFE0001034A5AEE0F F091B612C04CC7FCD907F8C9FCA25CA2130FA25CA2131FA25CA2133FA25CA2137FA291CA FCA25BA25B1201B512FCA337397BB838>80 D<0103B612F017FEEFFF80903B0007F8003F C04BEB0FF01707020FEC03F8EF01FC5DA2021F15FEA25DA2143FEF03FC5DA2027FEC07F8 18F092C7120F18E04AEC1FC0EF3F004A14FEEE01F80101EC0FE091B6128004FCC7FC9138 FC003F0103EC0F80834A6D7E8301071403A25C83010F14075F5CA2011F140FA25CA2133F 161F4AECE007A2017F160F180E91C7FC49020F131C007F01FE153CB5913807F078040313 F0CAEAFFE0EF3F80383B7CB83D>82 D<92383FC00E913901FFF01C020713FC91391FC07E 3C91393F001F7C027CEB0FF84A130749481303495A4948EB01F0A2495AA2011F15E091C7 FCA34915C0A36E90C7FCA2806D7E14FCECFF806D13F015FE6D6D7E6D14E0010080023F7F 14079138007FFC150F15031501A21500A2167C120EA3001E15FC5EA3003E4A5AA24B5AA2 007F4A5A4B5A6D49C7FC6D133ED8F9F013FC39F8FC03F839F07FFFE0D8E01F138026C003 FCC8FC2F3D7ABA2F>I<0007B812E0A25AD9F800EB001F01C049EB07C0485AD900011403 121E001C5C003C17801403123800785C00701607140700F01700485CA2140FC792C7FC5D A2141FA25DA2143FA25DA2147FA292C9FCA25CA25CA21301A25CA21303A25CA21307A25C A2130FA25CEB3FF0007FB512F8B6FCA2333971B83B>I87 D<14F8EB07FE90381F871C90383E03FE137CEBF80112 0148486C5A485A120FEBC001001F5CA2EA3F801403007F5C1300A21407485C5AA2140F5D 48ECC1C0A2141F15831680143F1587007C017F1300ECFF076C485B9038038F8E391F0F07 9E3907FE03FC3901F000F0222677A42A>97 D<133FEA1FFFA3C67E137EA313FE5BA31201 5BA312035BA31207EBE0F8EBE7FE9038EF0F80390FFC07C013F89038F003E013E0D81FC0 13F0A21380A2123F1300A214075A127EA2140F12FE4814E0A2141F15C05AEC3F80A21500 5C147E5C387801F8007C5B383C03E0383E07C0381E1F80D80FFEC7FCEA01F01C3B77B926 >I<147F903803FFC090380FC1E090381F0070017E13784913383901F801F83803F00312 0713E0120FD81FC013F091C7FC485AA2127F90C8FCA35A5AA45AA3153015381578007C14 F0007EEB01E0003EEB03C0EC0F806CEB3E00380F81F83803FFE0C690C7FC1D2677A426> II<147F903803FFC090380FC1E090383F00F0017E13785B485A485A485A120F4913 F8001F14F0383F8001EC07E0EC1F80397F81FF00EBFFF891C7FC90C8FC5A5AA55AA21530 007C14381578007E14F0003EEB01E0EC03C06CEB0F806CEB3E00380781F83803FFE0C690 C7FC1D2677A426>IIIII107 D III<147F903803FFC090380FC1F090381F00F8 017E137C5B4848137E4848133E0007143F5B120F485AA2485A157F127F90C7FCA215FF5A 4814FEA2140115FC5AEC03F8A2EC07F015E0140F007C14C0007EEB1F80003EEB3F00147E 6C13F8380F83F03803FFC0C648C7FC202677A42A>I<9039078007C090391FE03FF09039 3CF0787C903938F8E03E9038787FC00170497EECFF00D9F0FE148013E05CEA01E113C15C A2D80003143FA25CA20107147FA24A1400A2010F5C5E5C4B5A131F5EEC80035E013F495A 6E485A5E6E48C7FC017F133EEC70FC90387E3FF0EC0F8001FEC9FCA25BA21201A25BA212 03A25B1207B512C0A3293580A42A>I<3903C003F0390FF01FFC391E783C0F381C7C703A 3C3EE03F8038383FC0EB7F800078150000701300151CD8F07E90C7FCEAE0FE5BA2120012 015BA312035BA312075BA3120F5BA3121F5BA3123F90C9FC120E212679A423>114 D<14FE903807FF8090380F83C090383E00E04913F00178137001F813F00001130313F0A2 15E00003EB01C06DC7FC7FEBFFC06C13F814FE6C7F6D13807F010F13C01300143F141F14 0F123E127E00FE1480A348EB1F0012E06C133E00705B6C5B381E03E06CB45AD801FEC7FC 1C267AA422>II<13F8D8 03FEEB01C0D8078FEB03E0390E0F8007121E121C0038140F131F007815C01270013F131F 00F0130000E015805BD8007E133FA201FE14005B5D120149137EA215FE120349EBFC0EA2 0201131E161C15F813E0163CD9F003133814070001ECF07091381EF8F03A00F83C78E090 393FF03FC090390FC00F00272679A42D>I<01F0130ED803FC133FD8071EEB7F80EA0E1F 121C123C0038143F49131F0070140FA25BD8F07E140000E08013FEC6485B150E12015B15 1E0003141C5BA2153C000714385B5DA35DA24A5A140300035C6D48C7FC0001130E3800F8 3CEB7FF8EB0FC0212679A426>I<01F01507D803FC903903801F80D8071E903907C03FC0 D80E1F130F121C123C0038021F131F49EC800F00701607A249133FD8F07E168000E0ED00 0313FEC64849130718000001147E5B03FE5B0003160E495BA2171E00070101141C01E05B 173C1738A217781770020314F05F0003010713016D486C485A000190391E7C07802800FC 3C3E0FC7FC90393FF81FFE90390FE003F0322679A437>I<903907E007C090391FF81FF8 9039787C383C9038F03E703A01E01EE0FE3803C01F018013C0D8070014FC481480000E15 70023F1300001E91C7FC121CA2C75AA2147EA214FEA25CA21301A24A1370A2010314F016 E0001C5B007E1401010714C000FEEC0380010F1307010EEB0F0039781CF81E9038387C3C 393FF03FF03907C00FC027267CA427>I<13F0D803FCEB01C0D8071EEB03E0D80E1F1307 121C123C0038140F4914C01270A249131FD8F07E148012E013FEC648133F160012015B5D 0003147E5BA215FE00075C5BA214015DA314035D14070003130FEBF01F3901F87FE03800 7FF7EB1FC7EB000F5DA2141F003F5C48133F92C7FC147E147C007E13FC387001F8EB03E0 6C485A383C1F80D80FFEC8FCEA03F0233679A428>I E %EndDVIPSBitmapFont %DVIPSBitmapFont: Fr cmtt12 12 20 /Fr 20 112 df<007FB612FEA2B8FCA36C15FEA228077BA133>45 D<121FEA3F80EA7FC0EAFFE0A5EA7FC0EA3F80EA1F000B0B6C8A33>I64 D<007FB512F8B7FC16C082826C813A03F8000FFCED03FE15016F7E82A2EE3F 80A7EE7F00A25E4B5AA2ED07FCED1FF890B65A5E1680828216F89039F8000FFCED01FE6F 7EEE7F80163F17C0161FA2EE0FE0A7161F17C0A2163FEE7F8016FF4B1300150F007FB65A B75A5E16E05E6C4AC7FC2B3D7DBC33>66 D<003FB512F04814FCB7FC826C816C813A03F8 007FF0ED1FF8ED07FC15036F7E8281EE7F80A2163F17C0161FA217E0160FA4EE07F0AD16 0F17E0A4161F17C0163FA21780167FEEFF00A24B5A15034B5AED1FF8ED7FF0003FB6FC48 15C0B75A93C7FC6C14FC6C14F02C3D7EBC33>68 D<003FB712E04816F0B8FCA27E7ED801 FCC71207A8EE03E093C7FCA6151F4B7EA490B6FCA69038FC003FA46FC7FC92C8FCA817F8 EE01FCA9003FB7FC5AB8FCA27E6C16F82E3D7EBC33>I<003FB712E04816F0B8FCA27E7E D801FCC71207A8EE03E093C7FCA7151F4B7EA490B6FCA69038FC003FA46FC7FC92C8FCB1 383FFFF8487FB57EA26C5B6C5B2C3D7DBC33>I<003FB712F84816FCB8FCA43AFE000FE0 01A8007CED00F8C71500B3B3A40107B512C049804980A26D5C6D5C2E3D7EBC33>84 D<273FFFE001B5FC486D481480B56C4814C0A26C496C14806C496C1400D801FCC7EA0FE0 B3B3A36D141F00005EA26D143F6D5DA26D6C49C7FC6E5B6D6C485AECF00390390FFC0FFC 6DB55A6D5C6D5C6D6C1380DA1FFEC8FCEC07F8323E80BC33>I97 D99 DIII104 D<14E0EB03F8A2497EA36D5AA2EB00E091C8FCAA383FFFF8487FA47EEA0001B3AD007FB6 12C0B712E016F0A216E06C15C0243E78BD33>I107 D<383FFFFC487FB5FCA27E7EC7FCB3B3AD003FB612F84815FCB712FEA26C15FC 6C15F8273D7ABC33>I<4AB4FC263FFC0713C0267FFE1F13F000FF017F7F91B5FC6CB67E 6CEC07FEC6EBF801ECF0004A7F4A7F5CA291C7FCA35BB3A43B3FFFF80FFFFC486D4813FE B56C4813FFA26C496C13FE6C496C13FC302C7FAB33>110 DI E %EndDVIPSBitmapFont %DVIPSBitmapFont: Fs cmr12 12 35 /Fs 35 122 df<121EEA7F8012FF13C0A213E0A3127FEA1E601200A413E013C0A3120113 80120313005A1206120E5A5A5A12600B1D78891B>44 D<121EEA7F80A2EAFFC0A4EA7F80 A2EA1E000A0A78891B>46 D<14FF010713E090381F81F890383E007C01FC133F4848EB1F 8049130F4848EB07C04848EB03E0A2000F15F0491301001F15F8A2003F15FCA390C8FC48 15FEA54815FFB3A46C15FEA56D1301003F15FCA3001F15F8A26C6CEB03F0A36C6CEB07E0 000315C06D130F6C6CEB1F806C6CEB3F00013E137C90381F81F8903807FFE0010090C7FC 28447CC131>48 D<143014F013011303131F13FFB5FC13E713071200B3B3B0497E497E00 7FB6FCA3204278C131>I<49B4FC010F13E0013F13FC9038FE01FE3A01F0007F80D803C0 EB3FC048C7EA1FE0120EED0FF0EA0FE0486C14F8A215077F5BA26C48130FEA03C0C813F0 A3ED1FE0A2ED3FC01680ED7F0015FE4A5AEC03F0EC1FC0D90FFFC7FC15F090380001FCEC 007FED3F80ED1FC0ED0FE016F0ED07F816FC150316FEA2150116FFA3121EEA7F80487EA4 16FE491303A2007EC713FC00701407003015F80038140F6C15F06CEC1FE06C6CEB3FC0D8 03E0EB7F803A01FE01FE0039007FFFF8010F13E0010190C7FC28447CC131>51 D<000615C0D807C0130701FCEB7F8090B612005D5D5D15E0158026063FFCC7FC90C9FCAE 14FF010713C090381F01F090383800FC01F0137ED807C07F49EB1F8016C090C7120F0006 15E0C8EA07F0A316F81503A216FCA5123E127F487EA416F890C712075A006015F0A20070 140F003015E00038EC1FC07E001EEC3F806CEC7F006C6C13FE6C6C485A3901F807F03900 7FFFE0011F90C7FCEB07F826447BC131>53 D<121EEA7F80A2EAFFC0A4EA7F80A2EA1E00 C7FCB3A5121EEA7F80A2EAFFC0A4EA7F80A2EA1E000A2B78AA1B>58 D66 D69 DII79 DI<003FB912F8A3903BF0001FF8001F01806D481303003EC7150048187C007818 3CA20070181CA30060180CA5481806A5C81600B3B3A54B7EED7FFE49B77EA33F447DC346 >84 DI97 DII<167FED3FFFA315018182B3EC7F80903803FFF090380FC07C 90383F000E017E1307496D5AD803F87F48487F5B000F81485AA2485AA2127FA290C8FC5A AB7E7FA2123FA26C7EA2000F5D7F6C6C5B00035C6C6C9038077F806C6C010E13C0013F01 1C13FE90380FC0F8903803FFE09026007F0013002F467DC436>III III108 DI<3901FC01FE00FF903807FFC091381E07F091383801F8000701707F0003EB E0002601FDC07F5C01FF147F91C7FCA25BA35BB3A8486CECFF80B5D8F83F13FEA32F2C7D AB36>II<3903F803F000FFEB1FFCEC3C3E EC707F0007EBE0FF3803F9C000015B13FBEC007E153C01FF13005BA45BB3A748B4FCB512 FEA3202C7DAB26>114 D<90383FE0183901FFFC383907E01F78390F0003F8001E130148 1300007C1478127800F81438A21518A27EA27E6C6C13006C7E13FC383FFFE06C13FC6C13 FF6C14C06C14E0C614F0011F13F81300EC0FFC140300C0EB01FE1400157E7E153EA27EA3 6C143C6C147C15786C14F86CEB01F039F38003E039F1F00F8039E07FFE0038C00FF01F2E 7DAC26>I<1306A5130EA4131EA3133E137EA213FE12011207001FB512F0B6FCA2C648C7 FCB3A4150CAA017E131C017F1318A26D133890381F8030ECC070903807E0E0903801FFC0 9038007F001E3E7EBC26>III120 DI E %EndDVIPSBitmapFont %DVIPSBitmapFont: Ft cmr17 17.28 27 /Ft 27 122 df<170FA34D7EA24D7EA34D7EA34D7EA34C7F17DFA29338039FFC178FA293 38070FFE1707040F7FEE0E03A2041E80EE1C01A2043C80EE3800A24C80187FA24C80183F A24B4880181F0303814C130FA203078193C71207A24B81030E80A24B8284A24B8284A24B 82197F03F0824B153FA20201834B151FA202038392B8FCA24A83A292C91207020E8385A2 4A8485023C84023882A20278840270177FA202F0844A173FA24948841A1FA24948841A0F A249CB7F1A074985865B496C85497E48486C4D7F000F01F8051F13F0B60407B612F0A45C 657DE463>65 D67 D70 DI82 DI<003FBC12F8A49126C000039038C0000301FCC76C49EB007F 01F0190F01C019074848F103FC90C81701007E1A00007C1B7CA300781B3CA400701B1CA6 00F01B1E481B0EA7C91800B3B3B3A54C7FA2041F13F84AB87EA457627CE160>II97 DI<181EEF3FFEEE07FFA4EE000F1703A21701B3AAEDFF80 020F13F8023F13FE9139FF803F81903A03FC0007C14948EB01E1D91FE0EB00F94948147D 4948143D49C8121F4848150F491507120348481503491501120F121F5BA2123F5B127FA4 5B12FFAD127F7FA3123FA27F121FA26C6C1503A26C6C150712036D150F6C6C151F000016 3D137F6D6CECF9FF6D6CEB01F1D90FF0D903C113C06D6CD90F81EBFF80D901FFEB7F0190 39007FFFFC021F13E00201010091C7FC41657CE349>100 DII< F03F80DA03FC903801FFE091273FFFC00713F091B539F01FC1F8903B03FC03FC3E03903A 07F000FE784948EB7FE04948EB3FC04948011FEB01F049C76C6CC7FC01FE6E7EA248486E 7EA2000382A2491401000782AA00035E6D1403A200015EA26C6C4A5AA2017F4A5A6D6C49 5A6D6C495A496C49C8FCD937F013FE903973FC03FC0160B512F0D9E03F13C0DA03FCC9FC 4848CBFCA57FA27FA27F6C7E13FF91B512FE6DECFFF06D15FE6D6F7E6D16E084013F16FC 01FEC700017FD803F8EC001FD807E0ED03FF4848030013804848167F003FEF3FC090CA12 1F127EF00FE012FE481707A66C170F007E18C0A2007F171F6C6CEE3F806C6CEE7F00000F 177ED807F04B5A6C6C4B5A6C6C4B5AD8007FED1FC0D93FE0ECFF80D90FFED90FFEC7FC01 01B612F0D9003F1480020101F0C8FC3D5E7DBF42>II<133C13FF487F487FA66C5B6C90C7FC133C90C8FCB3 A2EB03C0EA07FF127FA41201EA007FA2133FB3B3AC497E497EB612E0A41B5F7DDE23>I< EB03C0EA07FFB5FCA41201EA007FA2133FB3AB0403B512F8A40400148094387FFC0018E0 6095C7FC177E5F17F04C5A4C5A4C5A4CC8FC163E5E5E4B5A4B5A4B5A4B5A151F4B7E4B7E 15FF02C17F9138C3CFF8ECC7879138CF07FC9138FE03FEECFC0102F87F4A6C7F4A137F4A 80707E161F83707E160783707E160183707F177F84717E171F84717E84A284496CEDFF80 496C4A13E0B600F090B6FCA440647CE346>107 DIIIII<9039078003F8D807FFEB0FFFB5013F13C092387C0F E0913881F01F9238E03FF00001EB838039007F8700148FEB3F8E029CEB1FE0EE0FC00298 EB030002B890C7FCA214B014F0A25CA55CB3B0497EEBFFF8B612FCA42C3F7CBE33>114 D<9139FFE00180010FEBFC03017FEBFF073A01FF001FCFD803F8EB03EFD807E0EB01FF48 487F4848147F48C8123F003E151F007E150F127CA200FC1507A316037EA27E7F6C7E6D91 C7FC13F8EA3FFE381FFFF06CEBFF806C14F86C14FF6C15C06C6C14F0011F80010714FED9 007F7F02031480DA003F13C01503030013E0167F00E0ED1FF0160F17F86C15071603A36C 1501A37EA26C16F016037E17E06D14076DEC0FC06D1580D8FDF0141FD8F8F8EC7F00013E 14FC3AF01FC00FF80107B512E0D8E001148027C0003FF8C7FC2D417DBF34>I<1438A714 78A414F8A31301A31303A21307130F131FA2137F13FF1203000F90B6FCB8FCA3260007F8 C8FCB3AE17E0AE6D6CEB01C0A316036D6C148016076D6C14006E6C5A91383FC01E91381F F07C6EB45A020313E09138007F802B597FD733>I119 D121 D E %EndDVIPSBitmapFont end %%EndProlog %%BeginSetup %%Feature: *Resolution 600dpi TeXDict begin %%PaperSize: a4 %%BeginPaperSize: a4 a4 %%EndPaperSize %%EndSetup %%Page: 1 1 1 0 bop 615 880 a Ft(A)44 b(Uniform)g(F)-11 b(ramew)l(ork)42 b(for)g(T)-11 b(erm)43 b(and)h(Graph)696 1063 y(Rewriting)h(Applied)h (to)d(Com)l(bined)i(Systems)1523 1303 y Fs(Enno)33 b(Ohlebusc)m(h)905 1463 y(F)-8 b(acult)m(y)32 b(of)g(T)-8 b(ec)m(hnology)g(,)33 b(Univ)m(ersit)m(y)g(of)f(Bielefeld)908 1579 y(P)-8 b(.O.)33 b(Bo)m(x)g(10)f(01)g(31,)g(33501)g(Bielefeld,)f(German)m(y)980 1695 y(email:)41 b Fr(enno@TechFak.Uni-Bielefeld)q(.DE)440 2003 y Fq(Keywor)l(ds:)c Fp(Theory)22 b(of)i(computation,)g(term)g (rewriting,)g(graph)e(rewriting,)i(mo)r(dularit)n(y)440 2278 y Fo(1)135 b(In)l(tro)t(duction)440 2460 y Fp(T)-7 b(erm)35 b(rewriting)f(has)h(applications)f(in)h(v)-5 b(arious)34 b(\014elds)i(of)f(computer)f(science)h(suc)n(h)g(as)440 2559 y(sym)n(b)r(olic)g(computation,)i(functional)e(programming,)g (abstract)g(data)g(t)n(yp)r(e)g(sp)r(eci\014ca-)440 2659 y(tions,)h(program)c(v)n(eri\014cation,)i(program)e(syn)n(thesis,)j (and)f(automated)f(theorem)h(pro)n(v-)440 2759 y(ing.)48 b(F)-7 b(or)30 b(reasons)g(of)h(e\016ciency)-7 b(,)32 b(term)f(rewriting)g(is)g(usually)g(implemen)n(ted)h(b)n(y)e(graph)440 2858 y(rewriting.)46 b(In)31 b(term)g(rewriting,)g(expressions)f(are)g (represen)n(ted)f(as)i(terms,)g(whereas)f(in)440 2958 y(graph)c(rewriting)f(these)i(are)f(represen)n(ted)f(as)h(directed)h (acyclic)f(graphs.)35 b(In)27 b(con)n(trast)e(to)440 3058 y(the)e(former,)g(the)g(latter)g(represen)n(tation)e(allo)n(ws)h (a)g(sharing)g(of)g(common)h(sub)r(expressions)440 3157 y(and)29 b(expressions)e(are)g(ev)-5 b(aluated)29 b(b)n(y)f(rule-based) g(graph)f(transformations.)39 b(Details)29 b(on)440 3257 y(this)23 b(sub)5 b(ject)22 b(can)g(b)r(e)h(found)g(in)g(the)g(recen)n (t)e(o)n(v)n(erview)g(article)h(of)g(Plump)h([Plu98)n(],)h(for)e(ex-) 440 3356 y(ample.)36 b(It)24 b(has)f(b)r(een)i(sho)n(wn)e(b)n(y)h (Kurihara)e(and)i(Oh)n(uc)n(hi)f([K)n(O95)n(])h(that)g(directed)g (acyclic)440 3456 y(graphs)33 b(can)i(b)r(e)g(represen)n(ted)e(b)n(y)h (w)n(ell-mark)n(ed)f(terms;)38 b(th)n(us)d(graph)e(transformations)440 3556 y(can)c(b)r(e)g(mo)r(deled)g(b)n(y)g(rewriting)f(w)n(ell-mark)n (ed)f(terms.)41 b(Although)29 b(term)g(rewriting)f(and)440 3655 y(graph)k(rewriting)h(share)f(man)n(y)h(common)g(features,)i (neither)e(is)h(a)f(sp)r(ecial)g(case)g(of)g(the)440 3755 y(other.)74 b(This)40 b(pap)r(er)g(will)g(bridge)g(this)g(gap)f(b) n(y)h(presen)n(ting)f(a)h(uniform)g(framew)n(ork,)440 3855 y(called)25 b Fq(marke)l(d)k(r)l(ewriting)p Fp(.)37 b(The)26 b(adv)-5 b(an)n(tage)24 b(of)i(this)g(new)g(approac)n(h)e(is)h (that)h(b)r(oth)g(term)440 3954 y(rewriting)i(and)i(graph)e(rewriting)g (can)h(b)r(e)h(view)n(ed)f(as)g(instances)g(of)g(mark)n(ed)f (rewriting.)440 4054 y(With)40 b(suc)n(h)f(a)g(metho)r(d)h(it)g(is)f(p) r(ossible)g(to)h(pro)n(v)n(e)d(statemen)n(ts)j(in)f(the)h(framew)n(ork) d(of)440 4153 y(mark)n(ed)22 b(rewriting)g(and)h(to)h(obtain)e(results) h(for)g(term)g(and)g(graph)f(rewriting)g(as)h(corollar-)440 4253 y(ies)31 b(thereof.)48 b(This)31 b(will)h(b)r(e)f(demonstrated)g (b)n(y)g(pro)n(ving)f(di\013eren)n(t)h(mo)r(dularit)n(y)g(results)440 4353 y(from)c Fq(b)l(oth)h Fp(areas)e(in)i Fq(one)g Fp(framew)n(ork.) 440 4627 y Fo(2)135 b(The)44 b(Uniform)i(F)-11 b(ramew)l(ork)440 4809 y Fp(The)31 b(reader)f(is)i(assumed)e(to)i(b)r(e)g(familiar)e (with)i(the)g(basic)f(notions)g(of)g(term)g(rewriting)440 4909 y(as)j(surv)n(ey)n(ed)f(in)i([BN98)o(],)h(for)e(instance.)58 b(Let)35 b Fn(F)42 b Fp(b)r(e)35 b(a)f(signature)g(and)g Fn(V)42 b Fp(b)r(e)35 b(a)f(set)g(of)440 5008 y(v)-5 b(ariables.)56 b(Let)35 b Fm(M)43 b Fp(b)r(e)35 b(a)f(coun)n(tably)g (in\014nite)h(set)f(of)h(ob)5 b(jects)34 b(called)g Fq(marks)h Fp(\(w)n(e)f(will)440 5108 y(use)d(natural)f(n)n(um)n(b)r(ers)h(as)f (marks\).)46 b(Let)32 b Fn(F)1868 5072 y Fl(\003)1935 5108 y Fp(=)c Fn(f)p Fm(f)2120 5078 y Fk(\026)2195 5108 y Fn(j)j Fm(f)37 b Fn(2)29 b(F)8 b Fm(;)14 b(\026)29 b Fn(2)g Fm(M)9 b Fn(g)30 b Fp(b)r(e)i(the)f(set)g(of)440 5208 y Fq(marke)l(d)i(function)f(symb)l(ols)p Fp(.)46 b(F)-7 b(or)30 b(all)g Fm(f)1723 5177 y Fk(\026)1795 5208 y Fn(2)e(F)1945 5171 y Fl(\003)1984 5208 y Fp(,)j(the)f(arit)n(y)g (of)g Fm(f)2532 5177 y Fk(\026)2607 5208 y Fp(coincides)f(with)i(that) 440 5307 y(of)25 b Fm(f)9 b Fp(.)36 b(Moreo)n(v)n(er,)23 b(w)n(e)i(de\014ne)h Fm(sy)s(mbol)r Fp(\()p Fm(f)1726 5277 y Fk(\026)1769 5307 y Fp(\))d(=)g Fm(f)34 b Fp(and)25 b Fm(mar)r(k)s Fp(\()p Fm(f)2430 5277 y Fk(\026)2475 5307 y Fp(\))e(=)g Fm(\026)p Fp(.)36 b(Analogously)-7 b(,)24 b(let)440 5407 y Fn(V)498 5371 y Fl(\003)559 5407 y Fp(=)f Fn(f)p Fm(x)736 5377 y Fk(\026)808 5407 y Fn(j)k Fm(x)d Fn(2)f(V)7 b Fm(;)14 b(\026)23 b Fn(2)g Fm(M)9 b Fn(g)27 b Fp(b)r(e)h(the)g(set)g(of)f Fq(marke)l(d)k(variables)p Fp(,)e Fm(sy)s(mbol)r Fp(\()p Fm(x)2885 5377 y Fk(\026)2929 5407 y Fp(\))24 b(=)e Fm(x)p Fp(,)29 b(and)1851 5662 y(1)p eop %%Page: 2 2 2 1 bop 440 531 a Fm(mar)r(k)s Fp(\()p Fm(x)721 501 y Fk(\026)767 531 y Fp(\))23 b(=)g Fm(\026)p Fp(.)36 b(The)26 b(set)f(of)h Fq(marke)l(d)j(terms)c Fp(o)n(v)n(er)f Fn(F)2168 495 y Fl(\003)2232 531 y Fp(and)h Fn(V)2449 495 y Fl(\003)2513 531 y Fp(is)h(de\014ned)g(in)g(the)g(usual)440 631 y(w)n(a)n(y)h(and)i (is)f(denoted)h(b)n(y)f Fn(T)21 b Fp(\()p Fn(F)1454 595 y Fl(\003)1492 631 y Fm(;)14 b Fn(V)1586 595 y Fl(\003)1625 631 y Fp(\).)40 b(The)28 b(set)h(of)f(all)h(marks)e(app)r(earing)h(in)g (a)h(mark)n(ed)440 731 y(term)35 b Fm(t)676 700 y Fl(\003)748 731 y Fn(2)g(T)22 b Fp(\()p Fn(F)1005 694 y Fl(\003)1043 731 y Fm(;)14 b Fn(V)1137 694 y Fl(\003)1176 731 y Fp(\))35 b(is)f(denoted)h(b)n(y)f Fm(mar)r(k)s(s)p Fp(\()p Fm(t)2079 700 y Fl(\003)2117 731 y Fp(\).)58 b(Tw)n(o)34 b(subterms)g Fm(t)2817 700 y Fl(\003)2817 751 y Fj(1)2890 731 y Fp(and)h Fm(t)3089 700 y Fl(\003)3089 751 y Fj(2)3161 731 y Fp(of)g(a)440 830 y(mark)n(ed)25 b(term)h Fm(t)961 800 y Fl(\003)1025 830 y Fp(are)f Fq(shar)l(e)l(d)j Fp(in)e Fm(t)1540 800 y Fl(\003)1604 830 y Fp(if)h Fm(t)1709 800 y Fl(\003)1709 851 y Fj(1)1770 830 y Fp(=)c Fm(t)1888 800 y Fl(\003)1888 851 y Fj(2)1926 830 y Fp(;)k(e.g.)e(0)2168 800 y Fj(1)2231 830 y Fp(and)h(0)2433 800 y Fj(1)2496 830 y Fp(are)f(shared)h(in)g(0) 3033 800 y Fj(1)3085 830 y Fp(+)3150 800 y Fj(0)3202 830 y Fp(0)3244 800 y Fj(1)3281 830 y Fp(.)440 930 y(If)35 b Fm(t)560 900 y Fl(\003)632 930 y Fp(is)f(a)g(mark)n(ed)f(term,)j (then)f Fm(e)p Fp(\()p Fm(t)1627 900 y Fl(\003)1665 930 y Fp(\))g(denotes)f(the)g(unmark)n(ed)g(term)g(obtained)g(from)440 1029 y Fm(t)470 999 y Fl(\003)540 1029 y Fp(b)n(y)e(erasing)e(all)h (marks.)49 b(Tw)n(o)31 b(mark)n(ed)g(terms)g Fm(s)2123 999 y Fl(\003)2193 1029 y Fp(and)h Fm(t)2389 999 y Fl(\003)2459 1029 y Fp(are)f Fq(bisimilar)2915 999 y Fj(1)2986 1029 y Fp(\(denoted)440 1129 y(b)n(y)i Fm(s)600 1099 y Fl(\003)672 1129 y Fn(\030)g Fm(t)800 1099 y Fl(\003)838 1129 y Fp(\))h(if)g(and)g (only)f(if)i Fm(e)p Fp(\()p Fm(s)1535 1099 y Fl(\003)1573 1129 y Fp(\))e(=)g Fm(e)p Fp(\()p Fm(t)1837 1099 y Fl(\003)1875 1129 y Fp(\).)56 b(Giv)n(en)34 b(t)n(w)n(o)e(mark)n(ed)h(terms)h Fm(s)2974 1099 y Fl(\003)3045 1129 y Fp(and)g Fm(t)3243 1099 y Fl(\003)3281 1129 y Fp(,)440 1229 y Fm(s)479 1199 y Fl(\003)553 1229 y Fq(c)l(ol)t(lapses)k Fp(to)d Fm(t)1042 1199 y Fl(\003)1116 1229 y Fp(\(denoted)h(b)n(y)f Fm(s)1632 1199 y Fl(\003)1707 1229 y Fn(\027)h Fm(t)1838 1199 y Fl(\003)1876 1229 y Fp(\))g(if)g(and)f(only)h(if)g(there)f(exists)h(a)f (function)440 1328 y(\010)24 b(:)h Fm(mar)r(k)s(s)p Fp(\()p Fm(s)884 1298 y Fl(\003)923 1328 y Fp(\))g Fn(!)f Fm(mar)r(k)s(s)p Fp(\()p Fm(t)1390 1298 y Fl(\003)1429 1328 y Fp(\))29 b(suc)n(h)f(that)h(\010\()p Fm(s)1990 1298 y Fl(\003)2028 1328 y Fp(\))c(=)f Fm(t)2204 1298 y Fl(\003)2242 1328 y Fp(,)29 b(where)f(the)h(extension)f(of)g(\010)g(to)440 1428 y Fn(T)21 b Fp(\()p Fn(F)606 1398 y Fl(\003)645 1428 y Fm(;)14 b Fn(V)740 1398 y Fl(\003)777 1428 y Fp(\))28 b(is)g(de\014ned)g(b)n(y)804 1656 y(\010\()p Fm(s)935 1621 y Fl(\003)974 1656 y Fp(\))23 b(=)1117 1538 y Fi(\032)1220 1605 y Fm(x)1267 1575 y Fj(\010\()p Fk(\026)p Fj(\))2138 1605 y Fp(if)28 b Fm(s)2253 1575 y Fl(\003)2314 1605 y Fp(=)23 b Fm(x)2449 1575 y Fk(\026)2494 1605 y Fm(;)14 b(x)23 b Fn(2)h(V)7 b Fm(;)1220 1708 y(f)1270 1678 y Fj(\010\()p Fk(\026)p Fj(\))1414 1708 y Fp(\(\010\()p Fm(t)1568 1678 y Fl(\003)1568 1729 y Fj(1)1606 1708 y Fp(\))p Fm(;)14 b(:)g(:)g(:)g(;)g Fp(\010\()p Fm(t)1945 1678 y Fl(\003)1945 1729 y Fk(n)1991 1708 y Fp(\)\))83 b(if)28 b Fm(s)2253 1678 y Fl(\003)2314 1708 y Fp(=)23 b Fm(f)2452 1678 y Fk(\026)2496 1708 y Fp(\()p Fm(t)2558 1678 y Fl(\003)2558 1729 y Fj(1)2597 1708 y Fm(;)14 b(:)g(:)g(:)f(;)h (t)2811 1678 y Fl(\003)2811 1729 y Fk(n)2856 1708 y Fp(\))440 1883 y(Note)32 b(that)g Fn(\027)g Fp(is)g(a)f(quasi-ordering.)47 b(A)32 b(collapsing)f(step)h Fm(s)2376 1853 y Fl(\003)2444 1883 y Fn(\027)e Fm(t)2569 1853 y Fl(\003)2639 1883 y Fp(is)i Fq(pr)l(op)l(er)h Fp(\(denoted)440 1983 y(b)n(y)26 b Fm(s)593 1953 y Fl(\003)654 1983 y Fn(\037)d Fm(t)772 1953 y Fl(\003)810 1983 y Fp(\))k(if)g Fm(t)974 1953 y Fl(\003)1035 1983 y Fn(6\027)c Fm(s)1162 1953 y Fl(\003)1200 1983 y Fp(.)36 b(The)27 b(mark)n(ed)e(terms)h Fm(s)1992 1953 y Fl(\003)2057 1983 y Fp(and)g Fm(t)2247 1953 y Fl(\003)2312 1983 y Fp(are)g Fq(isomorphic)j Fp(\(denoted)e(b)n(y)440 2082 y Fm(s)479 2052 y Fl(\003)544 2060 y Fn(\030)544 2086 y Fp(=)635 2082 y Fm(t)665 2052 y Fl(\003)703 2082 y Fp(\))j(if)h(and)e(only)h(if)g Fm(s)1309 2052 y Fl(\003)1374 2082 y Fn(\027)c Fm(t)1495 2052 y Fl(\003)1563 2082 y Fp(and)j Fm(t)1756 2052 y Fl(\003)1821 2082 y Fn(\027)e Fm(s)1952 2052 y Fl(\003)1990 2082 y Fp(.)43 b(Note)30 b(that)g Fm(s)2480 2052 y Fl(\003)2545 2060 y Fn(\030)2545 2086 y Fp(=)2636 2082 y Fm(t)2666 2052 y Fl(\003)2734 2082 y Fp(implies)g Fm(s)3057 2052 y Fl(\003)3122 2082 y Fn(\030)c Fm(t)3243 2052 y Fl(\003)3281 2082 y Fp(.)440 2182 y(The)j(marks)f(of)i(a)e(mark)n(ed)g(term)i Fm(s)1565 2152 y Fl(\003)1632 2182 y Fp(are)e(called)h Fq(fr)l(esh)h Fp(w.r.t.)g(another)e(mark)n(ed)g(term)h Fm(t)3266 2152 y Fl(\003)440 2282 y Fp(if)36 b Fm(mar)r(k)s(s)p Fp(\()p Fm(s)836 2251 y Fl(\003)875 2282 y Fp(\))24 b Fn(\\)g Fm(mar)r(k)s(s)p Fp(\()p Fm(t)1313 2251 y Fl(\003)1352 2282 y Fp(\))37 b(=)f Fn(;)p Fp(.)61 b(A)36 b Fq(marke)l(d)i (substitution)d Fm(\033)2547 2251 y Fl(\003)2623 2282 y Fp(:)h Fn(V)2740 2245 y Fl(\003)2815 2282 y Fn(!)h(T)21 b Fp(\()p Fn(F)3101 2251 y Fl(\003)3139 2282 y Fm(;)14 b Fn(V)3234 2251 y Fl(\003)3272 2282 y Fp(\))440 2381 y(is)36 b(a)g(substitution)h(whic)n(h)f(satis\014es)f Fm(x)1688 2351 y Fk(\026)1733 2381 y Fm(\033)1783 2351 y Fl(\003)1859 2381 y Fn(\030)i Fm(y)2005 2351 y Fk(\027)2046 2381 y Fm(\033)2096 2351 y Fl(\003)2171 2381 y Fp(for)e(all)h Fm(x)2477 2351 y Fk(\026)2522 2381 y Fm(;)14 b(y)2603 2351 y Fk(\027)2681 2381 y Fn(2)38 b(D)r Fm(om)p Fp(\()p Fm(\033)3035 2351 y Fl(\003)3074 2381 y Fp(\))f(with)440 2481 y Fm(sy)s(mbol)r Fp(\()p Fm(x)778 2451 y Fk(\026)822 2481 y Fp(\))26 b(=)f Fm(sy)s(mbol)r Fp(\()p Fm(y)1305 2451 y Fk(\027)1345 2481 y Fp(\).)41 b(This)29 b(de\014nition)h(of)f (mark)n(ed)e(substitution)j(ensures)e(that)440 2580 y(the)39 b(unmark)n(ed)e(substitution)i Fm(\033)i Fp(obtained)d(from)g Fm(\033)2162 2550 y Fl(\003)2239 2580 y Fp(b)n(y)g(erasing)f(all)h (marks)f(is)h(w)n(ell-)440 2680 y(de\014ned)28 b(\(i.e.,)g Fm(\033)j Fp(really)c(is)g(a)g(substitution\).)565 2780 y(Let)c Fh(2)h Fp(b)r(e)g(a)f(sp)r(ecial)g(constan)n(t)g(sym)n(b)r(ol.) 35 b(A)24 b Fq(c)l(ontext)f Fm(C)30 b Fp(is)23 b(a)g(term)h(in)g Fn(T)d Fp(\()p Fn(F)e([)10 b(f)p Fh(2)p Fn(g)p Fm(;)k Fn(V)7 b Fp(\).)440 2879 y(If)35 b Fm(C)41 b Fp(is)34 b(a)g(con)n(text)g(with)h Fm(n)g Fn(\025)f Fp(0)g(o)r(ccurrences)f(of)h Fh(2)h Fp(and)f Fm(t)2403 2891 y Fj(1)2440 2879 y Fm(;)14 b(:)g(:)g(:)g(;)g(t)2655 2891 y Fk(n)2734 2879 y Fp(are)34 b(terms,)i(then)440 2979 y Fm(C)6 b Fp([)p Fm(t)558 2991 y Fj(1)596 2979 y Fm(;)14 b(:)g(:)g(:)f(;)h(t)810 2991 y Fk(n)855 2979 y Fp(])28 b(is)g(the)h(result)e(of)h(replacing)f(the)i (o)r(ccurrences)d(of)i Fh(2)g Fp(with)h Fm(t)2811 2991 y Fj(1)2848 2979 y Fm(;)14 b(:)g(:)g(:)g(;)g(t)3063 2991 y Fk(n)3136 2979 y Fp(from)440 3079 y(left)28 b(to)g(righ)n(t.)36 b(The)28 b(notion)f Fq(marke)l(d)j(c)l(ontext)d Fp(is)h(de\014ned)g(in) f(the)h(ob)n(vious)f(w)n(a)n(y)-7 b(.)440 3252 y Fg(De\014nition)31 b(2.1)40 b Fp(Let)g Fn(R)g Fp(b)r(e)h(a)e(TRS)h(o)n(v)n(er)e(the)i (signature)f Fn(F)8 b Fp(.)73 b(A)40 b(rule)f Fm(l)2923 3222 y Fl(\003)3004 3252 y Fn(!)44 b Fm(r)3170 3222 y Fl(\003)3248 3252 y Fp(is)440 3352 y(a)38 b Fq(marke)l(d)j(version)f Fp(of)f(a)f(rule)g Fm(l)44 b Fn(!)d Fm(r)h Fp(in)d Fn(R)g Fp(if)g Fm(e)p Fp(\()p Fm(l)2156 3322 y Fl(\003)2194 3352 y Fp(\))j(=)f Fm(l)f Fp(and)f Fm(e)p Fp(\()p Fm(r)2722 3322 y Fl(\003)2761 3352 y Fp(\))j(=)f Fm(r)r Fp(.)71 b(In)39 b(the)440 3452 y(follo)n(wing,)k Fm(l)857 3421 y Fl(\003)940 3452 y Fn(!)i Fm(r)1107 3421 y Fl(\003)1187 3452 y Fp(is)40 b(also)g(called)g Fq(marke)l(d)j(rule)p Fp(.)77 b(The)41 b Fq(marke)l(d)h(r)l(ewrite)h(r)l(elation)440 3551 y Fh(;)523 3563 y Fl(R)598 3551 y Fn(\022)26 b(T)21 b Fp(\()p Fn(F)855 3521 y Fl(\003)893 3551 y Fm(;)14 b Fn(V)988 3521 y Fl(\003)1026 3551 y Fp(\))20 b Fn(\002)f(T)j Fp(\()p Fn(F)1329 3521 y Fl(\003)1367 3551 y Fm(;)14 b Fn(V)1462 3521 y Fl(\003)1500 3551 y Fp(\))30 b(w.r.t.)f Fn(R)h Fp(is)f(de\014ned)h(as)f(follo)n(ws:)39 b Fm(s)2709 3521 y Fl(\003)2774 3551 y Fh(;)2857 3563 y Fl(R)2944 3551 y Fm(t)2974 3521 y Fl(\003)3042 3551 y Fp(if)30 b(there)440 3651 y(exists)37 b(a)h(mark)n(ed)e(v)n(ersion)g Fm(l)1383 3621 y Fl(\003)1460 3651 y Fn(!)k Fm(r)1622 3621 y Fl(\003)1699 3651 y Fp(of)d(a)h(rewrite)f(rule)g Fm(l)k Fn(!)f Fm(r)g Fp(from)e Fn(R)p Fp(,)i(a)e(mark)n(ed)440 3750 y(substitution)33 b Fm(\033)957 3720 y Fl(\003)1027 3750 y Fp(and)f(a)g(mark)n(ed)f(con)n(text)g Fm(C)1931 3720 y Fl(\003)2002 3750 y Fp(con)n(taining)g(at)h(least)f(one)h(hole)g Fh(2)g Fp(suc)n(h)440 3850 y(that)24 b Fm(s)655 3820 y Fl(\003)716 3850 y Fp(=)f Fm(C)869 3820 y Fl(\003)907 3850 y Fp([)p Fm(l)957 3820 y Fl(\003)995 3850 y Fm(\033)1045 3820 y Fl(\003)1083 3850 y Fm(;)14 b(:)g(:)g(:)g(;)g(l)1295 3820 y Fl(\003)1333 3850 y Fm(\033)1383 3820 y Fl(\003)1421 3850 y Fp(],)25 b Fm(t)1522 3820 y Fl(\003)1583 3850 y Fp(=)e Fm(C)1736 3820 y Fl(\003)1774 3850 y Fp([)p Fm(r)1836 3820 y Fl(\003)1875 3850 y Fm(\033)1925 3820 y Fl(\003)1964 3850 y Fm(;)14 b(:)g(:)g(:)f(;)h(r)2187 3820 y Fl(\003)2226 3850 y Fm(\033)2276 3820 y Fl(\003)2315 3850 y Fp(],)24 b(and)g Fm(l)2570 3820 y Fl(\003)2607 3850 y Fm(\033)2657 3820 y Fl(\003)2720 3850 y Fp(is)f(not)h(a)f (subterm)440 3950 y(of)33 b Fm(C)605 3920 y Fl(\003)644 3950 y Fp(.)54 b Fm(l)748 3920 y Fl(\003)785 3950 y Fm(\033)835 3920 y Fl(\003)907 3950 y Fp(is)33 b(called)g(the)h Fq(c)l(ontr)l(acte) l(d)h(marke)l(d)h(r)l(e)l(dex)d Fp(in)g Fm(s)2440 3920 y Fl(\003)2478 3950 y Fp(.)54 b(Note)34 b(that)f(all)g(shared)440 4049 y(subterms)27 b Fm(l)823 4019 y Fl(\003)861 4049 y Fm(\033)911 4019 y Fl(\003)977 4049 y Fp(are)g(replaced)f(sim)n (ultaneously)h(with)h Fm(r)2235 4019 y Fl(\003)2274 4049 y Fm(\033)2324 4019 y Fl(\003)2363 4049 y Fp(.)565 4223 y(In)c(con)n(trast)f(to)h(an)g(unmark)n(ed)g(rewrite)f(rule,)i(a)f (mark)n(ed)f(rewrite)g(rule)h Fm(l)2869 4193 y Fl(\003)2930 4223 y Fn(!)f Fm(r)3075 4193 y Fl(\003)3138 4223 y Fp(need)440 4323 y Fq(not)28 b Fp(satisfy)g Fn(V)7 b Fm(ar)r Fp(\()p Fm(r)1057 4293 y Fl(\003)1097 4323 y Fp(\))24 b Fn(\022)g(V)7 b Fm(ar)r Fp(\()p Fm(l)1442 4293 y Fl(\003)1481 4323 y Fp(\).)39 b(F)-7 b(or)28 b(example,)g(if)h Fn(R)c Fp(=)f Fn(f)p Fm(doubl)r(e)p Fp(\()p Fm(x)p Fp(\))g Fn(!)g Fm(x)c Fp(+)e Fm(x)p Fn(g)p Fp(,)29 b(then)440 4422 y Fm(doubl)r(e)673 4392 y Fj(0)709 4422 y Fp(\(0)783 4392 y Fj(1)820 4422 y Fp(\))g Fh(;)964 4434 y Fl(R)1054 4422 y Fp(0)1096 4392 y Fj(3)1154 4422 y Fp(+)1219 4392 y Fj(2)1277 4422 y Fp(0)1319 4392 y Fj(4)1387 4422 y Fp(b)n(y)h(the)i(mark)n(ed)e(rule)h Fm(doubl)r(e)2354 4392 y Fj(0)2390 4422 y Fp(\()p Fm(x)2469 4392 y Fj(5)2507 4422 y Fp(\))e Fn(!)g Fm(x)2727 4392 y Fj(6)2785 4422 y Fp(+)2850 4392 y Fj(2)2908 4422 y Fm(x)2955 4392 y Fj(7)3024 4422 y Fp(and)i(the)440 4522 y(substitution)i Fm(\033)957 4492 y Fl(\003)1026 4522 y Fp(=)d Fn(f)p Fm(x)1210 4492 y Fj(5)1277 4522 y Fn(7!)h Fp(0)1433 4492 y Fj(1)1470 4522 y Fm(;)14 b(x)1554 4492 y Fj(6)1622 4522 y Fn(7!)30 b Fp(0)1777 4492 y Fj(3)1814 4522 y Fm(;)14 b(x)1898 4492 y Fj(7)1966 4522 y Fn(7!)31 b Fp(0)2122 4492 y Fj(4)2158 4522 y Fn(g)p Fp(.)50 b(The)32 b(next)h(lemma)e(states)h(that)440 4622 y(mark)n(ed)26 b(rewriting)h(is)h(sound)f(with)h(resp)r(ect)f(to)h(unmark)n(ed)e(term) i(rewriting.)440 4795 y Fg(Lemma)i(2.2)40 b Fm(s)981 4765 y Fl(\003)1042 4795 y Fh(;)1125 4807 y Fl(R)1209 4795 y Fm(t)1239 4765 y Fl(\003)1307 4795 y Fq(implies)32 b Fm(e)p Fp(\()p Fm(s)1702 4765 y Fl(\003)1740 4795 y Fp(\))23 b Fn(!)1878 4760 y Fj(+)1878 4820 y Fl(R)1962 4795 y Fm(e)p Fp(\()p Fm(t)2063 4765 y Fl(\003)2101 4795 y Fp(\))p Fq(.)440 4987 y(Pr)l(o)l(of)62 b Fp(Supp)r(ose)30 b Fm(s)1061 4957 y Fl(\003)1125 4987 y Fp(=)c Fm(C)1281 4957 y Fl(\003)1320 4987 y Fp([)p Fm(l)1370 4957 y Fl(\003)1407 4987 y Fm(\033)1457 4957 y Fl(\003)1496 4987 y Fm(;)14 b(:)g(:)g(:)f(;)h(l)1707 4957 y Fl(\003)1745 4987 y Fm(\033)1795 4957 y Fl(\003)1833 4987 y Fp(])27 b Fh(;)1966 4999 y Fl(R)2053 4987 y Fm(C)2118 4957 y Fl(\003)2157 4987 y Fp([)p Fm(r)2219 4957 y Fl(\003)2258 4987 y Fm(\033)2308 4957 y Fl(\003)2346 4987 y Fm(;)14 b(:)g(:)g(:)g(;)g(r)2570 4957 y Fl(\003)2609 4987 y Fm(\033)2659 4957 y Fl(\003)2697 4987 y Fp(])27 b(=)f Fm(t)2868 4957 y Fl(\003)2906 4987 y Fp(,)k(where)f Fm(C)3266 4957 y Fl(\003)440 5087 y Fp(con)n(tains)f Fm(n)c Fn(\025)g Fp(1)k(holes.)39 b(De\014ne)29 b(the)g(unmark)n(ed)e(substitution)i Fm(\033)j Fp(b)n(y)c Fm(x\033)h Fp(=)24 b Fm(e)p Fp(\()p Fm(x\033)3071 5057 y Fl(\003)3110 5087 y Fp(\))29 b(and)440 5187 y(let)f Fm(C)h Fp(=)23 b Fm(e)p Fp(\()p Fm(C)872 5157 y Fl(\003)910 5187 y Fp(\).)37 b(Then)28 b Fm(e)p Fp(\()p Fm(s)1329 5157 y Fl(\003)1367 5187 y Fp(\))23 b(=)g Fm(C)6 b Fp([)p Fm(l)r(\033)n(;)14 b(:)g(:)g(:)g(;)g(l)r(\033)s Fp(])23 b Fn(!)2061 5151 y Fj(+)2061 5211 y Fl(R)2145 5187 y Fm(C)6 b Fp([)p Fm(r)r(\033)n(;)14 b(:)g(:)g(:)i(;)e(r)r(\033)s Fp(])24 b(=)f Fm(e)p Fp(\()p Fm(t)2829 5157 y Fl(\003)2867 5187 y Fp(\))k(in)h Fm(n)f Fp(steps.)440 5286 y Ff(\003)p 440 5336 1146 4 v 532 5390 a Fe(1)567 5413 y Fd(The)d(origin)f(of)g (the)i(notion)g(\\bisimilarit)n(y")c(is)i(explained)i(in)e([AKP99].) 1851 5662 y Fp(2)p eop %%Page: 3 3 3 2 bop 565 531 a Fp(The)33 b(set)h Fn(T)922 543 y Fk(w)976 531 y Fp(\()p Fn(F)1076 501 y Fl(\003)1115 531 y Fm(;)14 b Fn(V)1210 501 y Fl(\003)1247 531 y Fp(\))35 b(of)e Fq(wel)t(l-marke)l(d)38 b(terms)33 b Fp(o)n(v)n(er)f Fn(F)2368 495 y Fl(\003)2440 531 y Fp(and)i Fn(V)2665 495 y Fl(\003)2738 531 y Fp(is)f(the)i(subset)e(of)440 631 y Fn(T)21 b Fp(\()p Fn(F)606 601 y Fl(\003)645 631 y Fm(;)14 b Fn(V)740 601 y Fl(\003)777 631 y Fp(\))29 b(suc)n(h)g(that)f Fm(t)1237 601 y Fl(\003)1300 631 y Fn(2)d(T)1425 643 y Fk(w)1479 631 y Fp(\()p Fn(F)1579 601 y Fl(\003)1618 631 y Fm(;)14 b Fn(V)1713 601 y Fl(\003)1750 631 y Fp(\))29 b(if)g(and)g(only)f(if,)h(for)f(ev)n(ery)f(pair)h Fm(t)2884 601 y Fl(\003)2884 652 y Fj(1)2922 631 y Fm(;)14 b(t)2989 601 y Fl(\003)2989 652 y Fj(2)3056 631 y Fp(of)29 b(sub-)440 731 y(terms)24 b(of)h Fm(t)790 700 y Fl(\003)828 731 y Fp(,)h Fm(mar)r(k)s Fp(\()p Fm(r)r(oot)p Fp(\()p Fm(t)1322 700 y Fl(\003)1322 751 y Fj(1)1362 731 y Fp(\)\))e(=)e Fm(mar)r(k)s Fp(\()p Fm(r)r(oot)p Fp(\()p Fm(t)1982 700 y Fl(\003)1982 751 y Fj(2)2023 731 y Fp(\)\))j(implies)g Fm(t)2421 700 y Fl(\003)2421 751 y Fj(1)2482 731 y Fp(=)e Fm(t)2600 700 y Fl(\003)2600 751 y Fj(2)2638 731 y Fp(.)36 b(F)-7 b(or)24 b(example,)h(the)440 830 y(term)f(0)677 800 y Fj(1)726 830 y Fp(+)791 800 y Fj(0)840 830 y Fp(0)882 800 y Fj(1)943 830 y Fp(is)g(w)n(ell-mark)n(ed)f(but)i(0)1675 800 y Fj(1)1724 830 y Fp(+)1789 800 y Fj(1)1837 830 y Fp(0)1879 800 y Fj(1)1941 830 y Fp(is)f(not.)36 b(W)-7 b(ell-mark)n(ed)23 b(terms)h(corresp)r(ond)440 930 y(exactly)30 b(to)g(lab)r(eled)h(directed)g(acyclic)e(graphs)h(with)h(a)f(unique)h (ro)r(ot)f(no)r(de;)i(the)f(reader)440 1029 y(is)c(referred)g(to)g([K)n (O95)n(])h(for)f(details.)440 1204 y Fg(De\014nition)k(2.3)40 b Fp(The)35 b Fq(gr)l(aph)i(r)l(ewrite)g(r)l(elation)63 b Fn(\))2166 1216 y Fl(R)2289 1204 y Fn(\022)35 b(T)2434 1216 y Fk(w)2488 1204 y Fp(\()p Fn(F)2588 1174 y Fl(\003)2626 1204 y Fm(;)14 b Fn(V)2721 1174 y Fl(\003)2759 1204 y Fp(\))23 b Fn(\002)g(T)2947 1216 y Fk(w)3001 1204 y Fp(\()p Fn(F)3101 1174 y Fl(\003)3139 1204 y Fm(;)14 b Fn(V)3234 1174 y Fl(\003)3272 1204 y Fp(\))440 1303 y(w.r.t.)30 b Fn(R)f Fp(is)h(de\014ned)g(as)e(follo)n(ws:)40 b Fm(s)1588 1273 y Fl(\003)1654 1303 y Fn(\))1737 1315 y Fl(R)1826 1303 y Fm(t)1856 1273 y Fl(\003)1923 1303 y Fp(if)30 b Fm(s)2040 1273 y Fl(\003)2105 1303 y Fh(;)2188 1315 y Fl(R)2275 1303 y Fm(t)2305 1273 y Fl(\003)2373 1303 y Fp(b)n(y)f(a)g(mark)n(ed)f(rule)h Fm(l)3053 1273 y Fl(\003)3117 1303 y Fn(!)d Fm(r)3265 1273 y Fl(\003)440 1403 y Fp(suc)n(h)41 b(that)g(\(i\))h(for)f(all)g Fm(x)1280 1373 y Fk(\026)1325 1403 y Fm(;)14 b(y)1406 1373 y Fk(\027)1493 1403 y Fn(2)46 b(V)7 b Fm(ar)r Fp(\()p Fm(l)1794 1373 y Fl(\003)1832 1403 y Fp(\))28 b Fn([)g(V)7 b Fm(ar)r Fp(\()p Fm(r)2187 1373 y Fl(\003)2226 1403 y Fp(\),)45 b Fm(sy)s(mbol)r Fp(\()p Fm(x)2664 1373 y Fk(\026)2708 1403 y Fp(\))i(=)e Fm(sy)s(mbol)r Fp(\()p Fm(y)3232 1373 y Fk(\027)3272 1403 y Fp(\))440 1503 y(implies)34 b Fm(mar)r(k)s Fp(\()p Fm(x)1009 1473 y Fk(\026)1055 1503 y Fp(\))g(=)f Fm(mar)r(k)s Fp(\()p Fm(y)1497 1473 y Fk(\027)1539 1503 y Fp(\),)j(and)e(\(ii\))h(the)f(marks)f(on)h(function)h(sym)n(b)r(ols)e (in)h Fm(r)3265 1473 y Fl(\003)440 1602 y Fp(are)27 b(m)n(utually)g (distinct)h(and)g(fresh)f(w.r.t.)h Fm(s)1853 1572 y Fl(\003)1891 1602 y Fp(.)565 1777 y(The)35 b(\014rst)g(condition)g(can)g(b)r(e)g (rephrased)f(as:)52 b(ev)n(ery)34 b(o)r(ccurrence)g(of)h(a)g(v)-5 b(ariable)34 b Fm(x)440 1876 y Fp(in)f Fm(l)h Fn(!)e Fm(r)j Fp(m)n(ust)e(ha)n(v)n(e)f(the)i(same)e(mark)g(in)h Fm(l)1907 1846 y Fl(\003)1977 1876 y Fn(!)f Fm(r)2131 1846 y Fl(\003)2170 1876 y Fp(.)53 b(This)33 b(means)f(that)h(v)-5 b(ariables)32 b(in)440 1976 y(rewrite)e(rules)g(are)f(maximally)h (shared.)45 b(F)-7 b(or)30 b(the)h(sak)n(e)e(of)h(simplicit)n(y)-7 b(,)32 b(one)e(could)g(omit)440 2076 y(the)d(marks)f(on)h(v)-5 b(ariables)26 b(in)h(mark)n(ed)f(rewrite)g(rules)h(b)r(ecause)f(these)h (marks)f(are)g(unique)440 2175 y(an)n(yw)n(a)n(y)-7 b(.)35 b(The)27 b(last)f(condition)h(means)g(that)g(in)g(graph)f(rewriting)g (one)g(uses)h(a)g(\\minimal)440 2275 y(structure)e(sharing)f(sc)n (heme".)35 b(Di\013eren)n(t)26 b(structure)e(sharing)g(sc)n(hemes)h (are)f(discussed)h(in)440 2374 y([K)n(O95)n(].)440 2549 y Fg(De\014nition)31 b(2.4)137 b Fp(The)48 b Fq(nonc)l(opying)i(r)l (ewrite)f(r)l(elation)76 b Fn(\))2523 2519 y Fk(nc)2523 2572 y Fl(R)2683 2549 y Fn(\022)57 b(T)2850 2561 y Fk(w)2904 2549 y Fp(\()p Fn(F)3004 2519 y Fl(\003)3043 2549 y Fm(;)14 b Fn(V)3138 2519 y Fl(\003)3175 2549 y Fp(\))33 b Fn(\002)440 2648 y(T)485 2660 y Fk(w)539 2648 y Fp(\()p Fn(F)639 2618 y Fl(\003)677 2648 y Fm(;)14 b Fn(V)772 2618 y Fl(\003)810 2648 y Fp(\))37 b(w.r.t.)g Fn(R)h Fp(is)f(de\014ned)g(b)n(y:)56 b Fm(s)1812 2618 y Fl(\003)1877 2648 y Fn(\))1960 2618 y Fk(nc)1960 2671 y Fl(R)2063 2648 y Fm(t)2093 2618 y Fl(\003)2168 2648 y Fp(if)38 b Fm(s)2293 2618 y Fl(\003)2369 2648 y Fh(;)2452 2660 y Fl(R)2552 2648 y Fm(t)2582 2618 y Fl(\003)2658 2648 y Fp(b)n(y)e(a)h(mark)n(ed)f(rule)440 2748 y Fm(l)467 2718 y Fl(\003)528 2748 y Fn(!)23 b Fm(r)673 2718 y Fl(\003)739 2748 y Fp(suc)n(h)28 b(that)f(ev)n(ery)g(mark)n(ed)f (v)-5 b(ariable)27 b(in)h Fm(r)2069 2718 y Fl(\003)2135 2748 y Fp(app)r(ears)f(also)f(in)i Fm(l)2733 2718 y Fl(\003)2771 2748 y Fp(.)565 2922 y(Both)18 b(the)g(graph)g(rewrite)f(relation)h(as) f(de\014ned)i(in)g([Plu93)o(,)f(KKSV94)o(,)g(AK96)o(,)h(AKP99)n(,)440 3022 y(Plu98)o(])27 b(and)h(the)f(noncop)n(ying)f(rewrite)h(relation)f (as)h(de\014ned)h(in)g([K)n(O95)m(])g(can)f(b)r(e)h(view)n(ed)440 3122 y(as)c(a)f(sp)r(ecial)h(case)g(of)g(mark)n(ed)f(rewriting.)35 b(In)24 b(con)n(trast)f(to)h(graph)g(rewriting,)g(the)g(de\014ni-)440 3221 y(tion)k(of)f(noncop)n(ying)g(rewriting)g(do)r(es)g(not)h(sp)r (ecify)g(ho)n(w)f(the)h(righ)n(t-hand)e(side)i Fm(r)j Fp(should)440 3321 y(b)r(e)e(mark)n(ed.)39 b(It)30 b(is)e(only)h (necessary)e(that)i(a)f(reduct)h(of)f(a)h(w)n(ell-mark)n(ed)e(term)i (is)f(again)g(a)440 3421 y(w)n(ell-mark)n(ed)h(term.)47 b(This)30 b(is)h(the)g(case)f(if)i(one)e(uses)h(for)f(instance)h(the)g (minimal)g(struc-)440 3520 y(ture)i(sharing)f(sc)n(heme)g(as)h(in)g (graph)f(rewriting.)53 b(As)33 b(a)f(matter)h(of)g(fact,)i(the)f (inclusion)468 3620 y Fn(\))551 3632 y Fl(R)668 3620 y Fn(\022)55 b(\))871 3590 y Fk(nc)871 3643 y Fl(R)1005 3620 y Fp(holds)30 b(true,)i(b)r(ecause)e(the)h(\014rst)g(condition)f (of)h(De\014nition)g(2.3)f(implies)440 3719 y Fn(V)7 b Fm(ar)r Fp(\()p Fm(r)652 3689 y Fl(\003)692 3719 y Fp(\))29 b Fn(\022)f(V)7 b Fm(ar)r Fp(\()p Fm(l)1046 3689 y Fl(\003)1084 3719 y Fp(\).)48 b(If)32 b(one)e(uses)h(the)h (minimal)f(structure)g(sharing)e(sc)n(heme)i(and)g(the)440 3819 y(system)26 b Fn(R)g Fp(is)g(left-linear,)f(then)i(the)f(con)n(v)n (erse)e(implication)h(also)g(holds)h(b)r(ecause)f(in)h(left-)440 3919 y(linear)g(systems)g(v)-5 b(ariables)26 b(are)g(automatically)g (maximally)g(shared)g([BEG)2854 3889 y Fj(+)2908 3919 y Fp(87)o(,)h(Ohl97)o(].)440 4018 y(Ho)n(w)n(ev)n(er,)40 b(the)g(con)n(v)n(erse)d(implication)i(in)g(general)f(do)r(es)g(not)i (hold)e(as)h(the)g(follo)n(wing)440 4118 y(example)34 b(sho)n(ws.)54 b(Let)35 b Fn(R)f Fp(=)f Fn(f)p Fm(eq)s Fp(\()p Fm(x;)14 b(x)p Fp(\))34 b Fn(!)g Fm(tr)r(ue)p Fn(g)p Fp(.)55 b(Since)35 b(the)f(same)f(v)-5 b(ariable)33 b(on)h(the)440 4218 y(left-hand)27 b(side)g(of)g(a)g(mark)n(ed)f(rule)g (ma)n(y)h(ha)n(v)n(e)e(di\013eren)n(t)j(marks)d(in)j(noncop)n(ying)d (rewrit-)440 4317 y(ing,)42 b(w)n(e)c(ha)n(v)n(e)g Fm(s)991 4287 y Fl(\003)1071 4317 y Fp(=)j Fm(eq)1256 4287 y Fj(0)1293 4317 y Fp(\()p Fm(eq)1404 4287 y Fj(1)1441 4317 y Fp(\(0)1515 4287 y Fj(2)1552 4317 y Fm(;)14 b Fp(0)1631 4287 y Fj(3)1668 4317 y Fp(\))p Fm(;)g(eq)1816 4287 y Fj(1)1853 4317 y Fp(\(0)1927 4287 y Fj(2)1964 4317 y Fm(;)g Fp(0)2043 4287 y Fj(3)2080 4317 y Fp(\)\))28 b Fn(\))2255 4287 y Fk(nc)2255 4340 y Fl(R)2358 4317 y Fm(eq)2437 4287 y Fj(0)2473 4317 y Fp(\()p Fm(tr)r(ue)2661 4287 y Fj(6)2699 4317 y Fm(;)14 b(tr)r(ue)2892 4287 y Fj(6)2929 4317 y Fp(\))42 b(=)g Fm(t)3140 4287 y Fl(\003)3217 4317 y Fp(b)n(y)440 4417 y(using)35 b(the)h(rule)f Fm(eq)1069 4387 y Fj(1)1106 4417 y Fp(\()p Fm(x)1185 4387 y Fj(4)1222 4417 y Fm(;)14 b(x)1306 4387 y Fj(5)1344 4417 y Fp(\))36 b Fn(!)g Fm(tr)r(ue)1687 4387 y Fj(6)1724 4417 y Fp(.)60 b(In)36 b(con)n(trast)e(to)h(this,)i Fm(s)2590 4387 y Fl(\003)2664 4417 y Fn(6\))2747 4429 y Fl(R)2844 4417 y Fm(t)2874 4387 y Fl(\003)2948 4417 y Fp(b)r(ecause)e(a)440 4516 y(mark)n(ed)c(v)n(ersion)g(of)h(the)h (rule)f Fm(eq)s Fp(\()p Fm(x;)14 b(x)p Fp(\))32 b Fn(!)f Fm(tr)r(ue)i Fp(in)f(whic)n(h)g(the)h(t)n(w)n(o)f(o)r(ccurrences)f(of)h Fm(x)440 4616 y Fp(ha)n(v)n(e)26 b(the)i(same)f(mark)g(cannot)g(matc)n (h)h(the)g(\(shared\))f(subterm)g Fm(eq)2594 4586 y Fj(1)2631 4616 y Fp(\(0)2705 4586 y Fj(2)2742 4616 y Fm(;)14 b Fp(0)2821 4586 y Fj(3)2858 4616 y Fp(\).)565 4716 y(In)23 b(con)n(trast)e(to)i(graph)f(rewriting)g(and)h(noncop)n(ying)f (rewriting,)h(subterms)f(are)g(nev)n(er)440 4815 y(shared)j(in)h(term)g (rewriting.)35 b(F)-7 b(ormally)g(,)26 b(the)g(set)g Fn(T)2060 4827 y Fk(t)2089 4815 y Fp(\()p Fn(F)2189 4785 y Fl(\003)2228 4815 y Fm(;)14 b Fn(V)2323 4785 y Fl(\003)2361 4815 y Fp(\))26 b(of)g Fq(terms)f Fp(o)n(v)n(er)g Fn(F)2984 4779 y Fl(\003)3049 4815 y Fp(and)g Fn(V)3266 4779 y Fl(\003)440 4915 y Fp(is)30 b(the)h(subset)g(of)f Fn(T)21 b Fp(\()p Fn(F)1193 4885 y Fl(\003)1232 4915 y Fm(;)14 b Fn(V)1327 4885 y Fl(\003)1365 4915 y Fp(\))30 b(suc)n(h)g(that)h Fm(t)1830 4885 y Fl(\003)1896 4915 y Fn(2)d(T)2024 4927 y Fk(t)2054 4915 y Fp(\()p Fn(F)2154 4885 y Fl(\003)2192 4915 y Fm(;)14 b Fn(V)2287 4885 y Fl(\003)2325 4915 y Fp(\))31 b(if)g(and)f(only)g(if)h(ev)n(ery)e(mark)440 5015 y(in)k Fm(t)572 4984 y Fl(\003)643 5015 y Fp(app)r(ears)f(only)g (once.)53 b(Moreo)n(v)n(er,)31 b(the)i Fq(\(marke)l(d\))j(term)e(r)l (ewrite)h(r)l(elation)f Fn(!)3165 5027 y Fl(R)3240 5015 y Fn(\022)440 5114 y(T)485 5126 y Fk(t)514 5114 y Fp(\()p Fn(F)614 5084 y Fl(\003)653 5114 y Fm(;)14 b Fn(V)748 5084 y Fl(\003)786 5114 y Fp(\))8 b Fn(\002)g(T)944 5126 y Fk(t)973 5114 y Fp(\()p Fn(F)1073 5084 y Fl(\003)1111 5114 y Fm(;)14 b Fn(V)1206 5084 y Fl(\003)1244 5114 y Fp(\))23 b(is)f(just)h(the)g(restriction)f(of)g(the)h(mark)n(ed)e (rewrite)h(relation)f Fh(;)3243 5126 y Fl(R)440 5214 y Fp(to)27 b Fn(T)586 5226 y Fk(t)616 5214 y Fp(\()p Fn(F)716 5184 y Fl(\003)754 5214 y Fm(;)14 b Fn(V)849 5184 y Fl(\003)887 5214 y Fp(\).)565 5313 y(Our)33 b(de\014nition)i(of) g(\(mark)n(ed\))f(term)g(rewriting)g(seems)g(to)g(complicate)g(things)g (un-)440 5413 y(necessarily)e(and)h(the)h(reader)d(ma)n(y)i(w)n(onder)f (what)i(it)f(migh)n(t)h(b)r(e)f(go)r(o)r(d)g(for.)53 b(It)34 b(is)f(easy)1851 5662 y(3)p eop %%Page: 4 4 4 3 bop 440 531 a Fp(to)37 b(see)g(that)h(term)f(rewriting)f(do)r(es)h (not)g(subsume)h(graph)e(rewriting)g(and)h(vice)g(v)n(ersa)440 631 y(\()p Fm(s)511 601 y Fl(\003)583 631 y Fp(=)d Fm(doubl)r(e)915 601 y Fj(0)951 631 y Fp(\(0)1025 601 y Fj(1)1062 631 y Fp(\))g Fn(!)1211 643 y Fl(R)1306 631 y Fp(0)1348 601 y Fj(3)1407 631 y Fp(+)1472 601 y Fj(2)1532 631 y Fp(0)1574 601 y Fj(4)1644 631 y Fp(=)g Fm(t)1773 601 y Fl(\003)1845 631 y Fp(but)h Fm(s)2043 601 y Fl(\003)2115 631 y Fn(6\))2198 643 y Fl(R)2293 631 y Fm(t)2323 601 y Fl(\003)2361 631 y Fp(\).)57 b(Th)n(us)33 b(the)i(adv)-5 b(an)n(tage)32 b(of)440 731 y(our)f(approac)n(h)e(is)j(that)f(term,)i(graph,)e(and)h (noncop)n(ying)e(rewriting)g(can)h(b)r(e)h(view)n(ed)f(as)440 830 y(instances)c(of)g(the)h(same)e(more)h(general)e(mo)r(del)j(of)f (mark)n(ed)f(rewriting)g(and)h(w)n(e)g(can)g(no)n(w)440 930 y(argue)f(in)i(the)g(general)e(mo)r(del.)565 1029 y(In)g(the)g(follo)n(wing,)g(it)g(can)g(b)r(e)g(seen)g(that)g(\(mark)n (ed\))g(term)g(rewriting)f(indeed)h(mo)r(dels)440 1129 y(unmark)n(ed)21 b(term)h(rewriting.)34 b(W)-7 b(e)23 b(asso)r(ciate)d(the)j(unmark)n(ed)e(term)h Fm(t)h Fp(=)g Fm(e)p Fp(\()p Fm(t)2837 1099 y Fl(\003)2875 1129 y Fp(\))f(with)h(ev)n (ery)440 1229 y(term)32 b Fm(t)673 1199 y Fl(\003)741 1229 y Fn(2)e(T)21 b Fp(\()p Fn(F)992 1199 y Fl(\003)1031 1229 y Fm(;)14 b Fn(V)1126 1199 y Fl(\003)1164 1229 y Fp(\).)49 b(Con)n(v)n(ersely)-7 b(,)31 b(with)h(ev)n(ery)f(unmark)n(ed) g(term)g Fm(t)h Fp(w)n(e)f(asso)r(ciate)g(a)440 1328 y(term)g Fm(t)672 1298 y Fl(\003)739 1328 y Fn(2)f(T)21 b Fp(\()p Fn(F)990 1298 y Fl(\003)1028 1328 y Fm(;)14 b Fn(V)1123 1298 y Fl(\003)1161 1328 y Fp(\))32 b(b)n(y)f(marking)f (the)h(function)h(sym)n(b)r(ols)e(and)h(v)-5 b(ariables)30 b(in)i Fm(t)f Fp(with)440 1428 y(marks)26 b(whic)n(h)i(are)f(pairwise)f (distinct.)38 b(Clearly)-7 b(,)26 b Fm(t)2054 1398 y Fl(\003)2120 1428 y Fp(is)i(unique)f(up)h(to)g(isomorphism.)440 1611 y Fg(Lemma)i(2.5)40 b Fq(The)31 b(fol)t(lowing)h(statements)d (hold:)538 1777 y(1.)43 b Fm(s)687 1747 y Fl(\003)748 1777 y Fn(!)831 1789 y Fl(R)915 1777 y Fm(t)945 1747 y Fl(\003)1013 1777 y Fq(implies)31 b Fm(e)p Fp(\()p Fm(s)1407 1747 y Fl(\003)1445 1777 y Fp(\))23 b Fn(!)1583 1789 y Fl(R)1668 1777 y Fm(e)p Fp(\()p Fm(t)1769 1747 y Fl(\003)1807 1777 y Fp(\))p Fq(.)538 1943 y(2.)43 b(L)l(et)29 b Fm(s)i Fq(and)f Fm(t)h Fq(b)l(e)f(unmarke)l(d)g(terms)g(such)h(that)f Fm(s)24 b Fn(!)2305 1955 y Fl(R)2390 1943 y Fm(t)31 b Fq(and)f(let)h Fm(s)2769 1913 y Fl(\003)2807 1943 y Fm(;)14 b(t)2874 1913 y Fl(\003)2942 1943 y Fq(b)l(e)30 b(marke)l(d)648 2042 y(terms)f(with)h Fm(e)p Fp(\()p Fm(s)1170 2012 y Fl(\003)1208 2042 y Fp(\))24 b(=)e Fm(s)30 b Fq(and)g Fm(e)p Fp(\()p Fm(t)1682 2012 y Fl(\003)1720 2042 y Fp(\))24 b(=)e Fm(t)p Fq(.)39 b(Then)31 b(ther)l(e)e(is)i(a)f(marke)l(d)g(term)g Fm(u)3078 2012 y Fl(\003)3145 2042 y Fq(such)648 2142 y(that)f Fm(s)856 2112 y Fl(\003)917 2142 y Fn(!)1000 2154 y Fl(R)1085 2142 y Fm(u)1133 2112 y Fl(\003)1193 2120 y Fn(\030)1193 2146 y Fp(=)1281 2142 y Fm(t)1311 2112 y Fl(\003)1349 2142 y Fq(.)440 2341 y(Pr)l(o)l(of)84 b Fp(\(1\))41 b(Since)g(ev)n(ery)e(mark)h(app)r(ears)g(only)g(once)h (in)g Fm(s)2421 2311 y Fl(\003)2459 2341 y Fp(,)j(there)d(is)f(at)h (most)g(one)440 2441 y(o)r(ccurrence)26 b(of)i(a)f(subterm)h Fm(l)1368 2411 y Fl(\003)1405 2441 y Fm(\033)1455 2411 y Fl(\003)1521 2441 y Fp(in)g Fm(s)1657 2411 y Fl(\003)1695 2441 y Fp(.)37 b(Th)n(us)28 b(the)g(claim)f(follo)n(ws)g(from)g(Lemma)g (2.2.)440 2540 y(\(2\))38 b(Supp)r(ose)g Fm(s)i Fp(=)f Fm(C)6 b Fp([)p Fm(l)r(\033)s Fp(])41 b Fn(!)1415 2552 y Fl(R)1516 2540 y Fm(C)6 b Fp([)p Fm(r)r(\033)s Fp(])41 b(=)f Fm(t)p Fp(.)68 b(Mark)36 b(ev)n(ery)h(v)-5 b(ariable)37 b(in)h Fn(V)7 b Fm(ar)r Fp(\()p Fm(l)r Fp(\))38 b(with)440 2640 y(pairwise)23 b(distinct)h(marks)e(whic)n(h)i(are)f(fresh)g (w.r.t.)h Fm(s)2122 2610 y Fl(\003)2160 2640 y Fp(.)35 b(Then)24 b(let)g Fm(l)2574 2610 y Fl(\003)2612 2640 y Fp(,)g Fm(\033)2709 2610 y Fl(\003)2748 2640 y Fp(,)g(and)g Fm(C)3018 2610 y Fl(\003)3080 2640 y Fp(b)r(e)g(the)440 2740 y(mark)n(ed)i(v)n(ersions)f(of)i Fm(l)r Fp(,)g Fm(\033)s Fp(,)h(and)f Fm(C)34 b Fp(suc)n(h)26 b(that)i Fm(s)1980 2710 y Fl(\003)2041 2740 y Fp(=)23 b Fm(C)2194 2710 y Fl(\003)2232 2740 y Fp([)p Fm(l)2282 2710 y Fl(\003)2320 2740 y Fm(\033)2370 2710 y Fl(\003)2408 2740 y Fp(].)37 b(F)-7 b(urthermore,)26 b(w)n(e)h(mark)440 2839 y Fm(r)j Fp(with)f(pairwise)d(distinct)i(marks)f(whic)n(h)g(are)g(fresh)g (w.r.t.)h Fm(s)2406 2809 y Fl(\003)2472 2839 y Fp(and)f Fn(V)7 b Fm(ar)r Fp(\()p Fm(l)2833 2809 y Fl(\003)2871 2839 y Fp(\).)38 b(F)-7 b(or)27 b(ev)n(ery)440 2939 y Fm(x)487 2899 y Fk(\026)527 2907 y Fc(i)487 2962 y Fk(i)585 2939 y Fp(in)g Fn(V)7 b Fm(ar)r Fp(\()p Fm(r)893 2909 y Fl(\003)932 2939 y Fp(\))24 b(=)e Fn(f)p Fm(x)1164 2899 y Fk(\026)1204 2907 y Fb(1)1164 2961 y Fj(1)1241 2939 y Fm(;)14 b(:)g(:)g(:)g(;)g(x)1473 2909 y Fk(\026)1513 2917 y Fc(n)1473 2960 y Fk(n)1558 2939 y Fn(g)26 b Fp(let)h Fm(v)1788 2909 y Fl(\003)1785 2961 y Fk(i)1853 2939 y Fp(b)r(e)g(a)f(term)h(asso)r(ciated)e(with)i Fm(sy)s(mbol)r Fp(\()p Fm(x)3151 2899 y Fk(\026)3191 2907 y Fc(i)3151 2962 y Fk(i)3222 2939 y Fp(\))p Fm(\033)440 3039 y Fp(suc)n(h)38 b(that)g(all)f(marks)g(in)h Fm(v)1361 3008 y Fl(\003)1358 3060 y Fk(i)1438 3039 y Fp(are)f(fresh)g(w.r.t.)h Fm(s)2069 3008 y Fl(\003)2145 3039 y Fp(and)g Fm(v)2360 3008 y Fl(\003)2357 3060 y Fk(j)2398 3039 y Fp(,)j(where)c(1)j Fn(\024)g Fm(j)45 b Fn(\024)40 b Fm(n)e Fp(and)440 3138 y Fm(j)43 b Fn(6)p Fp(=)37 b Fm(i)p Fp(.)63 b(Finally)-7 b(,)38 b(w)n(e)e(extend)h Fm(\033)1503 3108 y Fl(\003)1578 3138 y Fp(from)f Fn(V)7 b Fm(ar)r Fp(\()p Fm(l)1983 3108 y Fl(\003)2021 3138 y Fp(\))36 b(to)h Fn(V)7 b Fm(ar)r Fp(\()p Fm(l)2400 3108 y Fl(\003)2438 3138 y Fp(\))24 b Fn([)h(V)7 b Fm(ar)r Fp(\()p Fm(r)2786 3108 y Fl(\003)2826 3138 y Fp(\))36 b(b)n(y)g(de\014ning)440 3238 y Fm(x)487 3198 y Fk(\026)527 3206 y Fc(i)487 3261 y Fk(i)558 3238 y Fm(\033)608 3208 y Fl(\003)672 3238 y Fp(=)26 b Fm(v)806 3208 y Fl(\003)803 3259 y Fk(i)873 3238 y Fp(for)j(all)g(1)c Fn(\024)g Fm(i)g Fn(\024)g Fm(n)p Fp(.)42 b(W)-7 b(e)29 b(infer)g Fm(s)1911 3208 y Fl(\003)1975 3238 y Fp(=)c Fm(C)2130 3208 y Fl(\003)2169 3238 y Fp([)p Fm(l)2219 3208 y Fl(\003)2256 3238 y Fm(\033)2306 3208 y Fl(\003)2345 3238 y Fp(])h Fn(!)2477 3250 y Fl(R)2563 3238 y Fm(C)2628 3208 y Fl(\003)2667 3238 y Fp([)p Fm(r)2729 3208 y Fl(\003)2768 3238 y Fm(\033)2818 3208 y Fl(\003)2856 3238 y Fp(].)42 b(Moreo)n(v)n(er,)440 3337 y(b)n(y)22 b(construction)e Fm(C)1084 3307 y Fl(\003)1123 3337 y Fp([)p Fm(r)1185 3307 y Fl(\003)1224 3337 y Fm(\033)1274 3307 y Fl(\003)1312 3337 y Fp(])k Fn(2)f(T)1482 3349 y Fk(t)1511 3337 y Fp(\()p Fn(F)1611 3307 y Fl(\003)1650 3337 y Fm(;)14 b Fn(V)1745 3307 y Fl(\003)1783 3337 y Fp(\))22 b(and)f Fm(C)2057 3307 y Fl(\003)2096 3337 y Fp([)p Fm(r)2158 3307 y Fl(\003)2197 3337 y Fm(\033)2247 3307 y Fl(\003)2285 3337 y Fp(])j Fn(\030)e Fm(t)2449 3307 y Fl(\003)2487 3337 y Fp(.)35 b(Hence)22 b Fm(C)2851 3307 y Fl(\003)2890 3337 y Fp([)p Fm(r)2952 3307 y Fl(\003)2991 3337 y Fm(\033)3041 3307 y Fl(\003)3079 3337 y Fp(])3125 3315 y Fn(\030)3125 3342 y Fp(=)3213 3337 y Fm(t)3243 3307 y Fl(\003)3281 3337 y Fp(.)440 3437 y Ff(\003)440 3712 y Fo(3)135 b(An)44 b(Application)440 3894 y Fp(It)23 b(is)f(w)n(ell-kno)n(wn)e(that)j (termination)f(is)g(not)g(mo)r(dular)f(for)h(disjoin)n(t)g(TRSs.)35 b(In)23 b(T)-7 b(o)n(y)n(ama's)440 3993 y(coun)n(terexample)41 b([T)-7 b(o)n(y87)n(],)46 b(the)c(com)n(bination)g(of)g(the)g (terminating)g(systems)g Fn(R)3155 4005 y Fj(1)3240 3993 y Fp(=)440 4093 y Fn(f)p Fm(F)12 b Fp(\(0)p Fm(;)i Fp(1)p Fm(;)g(x)p Fp(\))35 b Fn(!)g Fm(F)12 b Fp(\()p Fm(x;)i(x;)g(x)p Fp(\))p Fn(g)36 b Fp(and)f Fn(R)1630 4105 y Fj(2)1702 4093 y Fp(=)g Fn(f)p Fm(g)s Fp(\()p Fm(x;)14 b(y)s Fp(\))35 b Fn(!)g Fm(x;)14 b(g)s Fp(\()p Fm(x;)g(y)s Fp(\))36 b Fn(!)f Fm(y)s Fn(g)g Fp(yields)f(a)h(non-)440 4192 y(terminating)27 b(system)h(b)r(ecause)f(there)g(is)h(the)g(cyclic)f (deriv)-5 b(ation)440 4845 y @beginspecial 0 @llx 0 @lly 800 @urx 157 @ury 3437 @rwi @setspecial %%BeginDocument: exTerm.eps %!PS-Adobe-2.0 EPSF-2.0 %%Title: exTerm.eps %%Creator: fig2dev Version 3.2 Patchlevel 0-beta3 %%CreationDate: Thu Jul 9 13:22:05 1998 %%For: enno@thymian (Enno Ohlebusch) %%Orientation: Portrait %%BoundingBox: 0 0 800 157 %%Pages: 0 %%BeginSetup %%EndSetup %%Magnification: 1.0000 %%EndComments /$F2psDict 200 dict def $F2psDict begin $F2psDict /mtrx matrix put /col-1 {0 setgray} bind def /col0 {0.000 0.000 0.000 srgb} bind def /col1 {0.000 0.000 1.000 srgb} bind def /col2 {0.000 1.000 0.000 srgb} bind def /col3 {0.000 1.000 1.000 srgb} bind def /col4 {1.000 0.000 0.000 srgb} bind def /col5 {1.000 0.000 1.000 srgb} bind def /col6 {1.000 1.000 0.000 srgb} bind def /col7 {1.000 1.000 1.000 srgb} bind def /col8 {0.000 0.000 0.560 srgb} bind def /col9 {0.000 0.000 0.690 srgb} bind def /col10 {0.000 0.000 0.820 srgb} bind def /col11 {0.530 0.810 1.000 srgb} bind def /col12 {0.000 0.560 0.000 srgb} bind def /col13 {0.000 0.690 0.000 srgb} bind def /col14 {0.000 0.820 0.000 srgb} bind def /col15 {0.000 0.560 0.560 srgb} bind def /col16 {0.000 0.690 0.690 srgb} bind def /col17 {0.000 0.820 0.820 srgb} bind def /col18 {0.560 0.000 0.000 srgb} bind def /col19 {0.690 0.000 0.000 srgb} bind def /col20 {0.820 0.000 0.000 srgb} bind def /col21 {0.560 0.000 0.560 srgb} bind def /col22 {0.690 0.000 0.690 srgb} bind def /col23 {0.820 0.000 0.820 srgb} bind def /col24 {0.500 0.190 0.000 srgb} bind def /col25 {0.630 0.250 0.000 srgb} bind def /col26 {0.750 0.380 0.000 srgb} bind def /col27 {1.000 0.500 0.500 srgb} bind def /col28 {1.000 0.630 0.630 srgb} bind def /col29 {1.000 0.750 0.750 srgb} bind def /col30 {1.000 0.880 0.880 srgb} bind def /col31 {1.000 0.840 0.000 srgb} bind def end save -41.0 185.0 translate 1 -1 scale /cp {closepath} bind def /ef {eofill} bind def /gr {grestore} bind def /gs {gsave} bind def /sa {save} bind def /rs {restore} bind def /l {lineto} bind def /m {moveto} bind def /rm {rmoveto} bind def /n {newpath} bind def /s {stroke} bind def /sh {show} bind def /slc {setlinecap} bind def /slj {setlinejoin} bind def /slw {setlinewidth} bind def /srgb {setrgbcolor} bind def /rot {rotate} bind def /sc {scale} bind def /sd {setdash} bind def /ff {findfont} bind def /sf {setfont} bind def /scf {scalefont} bind def /sw {stringwidth} bind def /tr {translate} bind def /tnt {dup dup currentrgbcolor 4 -2 roll dup 1 exch sub 3 -1 roll mul add 4 -2 roll dup 1 exch sub 3 -1 roll mul add 4 -2 roll dup 1 exch sub 3 -1 roll mul add srgb} bind def /shd {dup dup currentrgbcolor 4 -2 roll mul 4 -2 roll mul 4 -2 roll mul srgb} bind def /DrawEllipse { /endangle exch def /startangle exch def /yrad exch def /xrad exch def /y exch def /x exch def /savematrix mtrx currentmatrix def x y tr xrad yrad sc 0 0 1 startangle endangle arc closepath savematrix setmatrix } def /$F2psBegin {$F2psDict begin /$F2psEnteredState save def} def /$F2psEnd {$F2psEnteredState restore end} def %%EndProlog $F2psBegin 10 setmiterlimit n -1000 4082 m -1000 -1000 l 15003 -1000 l 15003 4082 l cp clip 0.06000 0.06000 sc 7.500 slw % Ellipse n 7125 750 270 270 0 360 DrawEllipse gs col0 s gr % Ellipse n 7125 1725 270 270 0 360 DrawEllipse gs col0 s gr % Ellipse n 8175 2775 270 270 0 360 DrawEllipse gs col0 s gr % Ellipse n 8775 2775 270 270 0 360 DrawEllipse gs col0 s gr % Ellipse n 8475 1725 270 270 0 360 DrawEllipse gs col0 s gr % Ellipse n 5775 1725 270 270 0 360 DrawEllipse gs col0 s gr % Ellipse n 975 2775 270 270 0 360 DrawEllipse gs col0 s gr % Ellipse n 1575 2775 270 270 0 360 DrawEllipse gs col0 s gr % Ellipse n 1275 1725 270 270 0 360 DrawEllipse gs col0 s gr % Ellipse n 3675 2775 270 270 0 360 DrawEllipse gs col0 s gr % Ellipse n 4275 2775 270 270 0 360 DrawEllipse gs col0 s gr % Ellipse n 3975 1725 270 270 0 360 DrawEllipse gs col0 s gr % Ellipse n 2625 1725 270 270 0 360 DrawEllipse gs col0 s gr % Ellipse n 2325 2775 270 270 0 360 DrawEllipse gs col0 s gr % Ellipse n 2925 2775 270 270 0 360 DrawEllipse gs col0 s gr % Ellipse n 10425 2805 270 270 0 360 DrawEllipse gs col0 s gr % Ellipse n 11025 2805 270 270 0 360 DrawEllipse gs col0 s gr % Ellipse n 10725 1755 270 270 0 360 DrawEllipse gs col0 s gr % Ellipse n 13125 2805 270 270 0 360 DrawEllipse gs col0 s gr % Ellipse n 13725 2805 270 270 0 360 DrawEllipse gs col0 s gr % Ellipse n 13425 1755 270 270 0 360 DrawEllipse gs col0 s gr % Ellipse n 12075 1755 270 270 0 360 DrawEllipse gs col0 s gr % Ellipse n 11775 2805 270 270 0 360 DrawEllipse gs col0 s gr % Ellipse n 12375 2805 270 270 0 360 DrawEllipse gs col0 s gr % Ellipse n 2655 765 270 270 0 360 DrawEllipse gs col0 s gr % Ellipse n 12105 765 270 270 0 360 DrawEllipse gs col0 s gr % Polyline gs clippath 9753 945 m 9873 975 l 9753 1005 l 9915 1005 l 9915 945 l cp clip n 9225 975 m 9900 975 l gs col0 s gr gr % arrowhead n 9753 945 m 9873 975 l 9753 1005 l col0 s % Polyline gs clippath 6148 1473 m 6025 1489 l 6125 1418 l 5975 1478 l 5997 1533 l cp clip n 7125 1050 m 6000 1500 l gs col0 s gr gr % arrowhead n 6148 1473 m 6025 1489 l 6125 1418 l col0 s % Polyline gs clippath 7155 1278 m 7125 1398 l 7095 1278 l 7095 1440 l 7155 1440 l cp clip n 7125 1125 m 7125 1425 l gs col0 s gr gr % arrowhead n 7155 1278 m 7125 1398 l 7095 1278 l col0 s % Polyline gs clippath 8125 1418 m 8224 1489 l 8102 1473 l 8253 1533 l 8275 1478 l cp clip n 7125 1050 m 8250 1500 l gs col0 s gr gr % arrowhead n 8125 1418 m 8224 1489 l 8102 1473 l col0 s % Polyline gs clippath 8735 2324 m 8777 2440 l 8685 2357 l 8775 2492 l 8825 2459 l cp 8299 2357 m 8206 2440 l 8249 2324 l 8159 2459 l 8209 2492 l cp clip n 8192 2463 m 8492 2013 l 8792 2463 l gs col0 s gr gr % arrowhead n 8299 2357 m 8206 2440 l 8249 2324 l col0 s % arrowhead n 8735 2324 m 8777 2440 l 8685 2357 l col0 s % Polyline gs clippath 5178 945 m 5298 975 l 5178 1005 l 5340 1005 l 5340 945 l cp clip n 4650 975 m 5325 975 l gs col0 s gr gr % arrowhead n 5178 945 m 5298 975 l 5178 1005 l col0 s % Polyline gs clippath 1648 1473 m 1525 1489 l 1625 1418 l 1475 1478 l 1497 1533 l cp clip n 2625 1050 m 1500 1500 l gs col0 s gr gr % arrowhead n 1648 1473 m 1525 1489 l 1625 1418 l col0 s % Polyline gs clippath 3625 1418 m 3724 1489 l 3602 1473 l 3753 1533 l 3775 1478 l cp clip n 2625 1050 m 3750 1500 l gs col0 s gr gr % arrowhead n 3625 1418 m 3724 1489 l 3602 1473 l col0 s % Polyline gs clippath 1518 2336 m 1560 2452 l 1468 2369 l 1558 2504 l 1608 2471 l cp 1082 2369 m 989 2452 l 1032 2336 l 942 2471 l 992 2504 l cp clip n 975 2475 m 1275 2025 l 1575 2475 l gs col0 s gr gr % arrowhead n 1082 2369 m 989 2452 l 1032 2336 l col0 s % arrowhead n 1518 2336 m 1560 2452 l 1468 2369 l col0 s % Polyline gs clippath 4235 2324 m 4277 2440 l 4185 2357 l 4275 2492 l 4325 2459 l cp 3799 2357 m 3706 2440 l 3749 2324 l 3659 2459 l 3709 2492 l cp clip n 3692 2463 m 3992 2013 l 4292 2463 l gs col0 s gr gr % arrowhead n 3799 2357 m 3706 2440 l 3749 2324 l col0 s % arrowhead n 4235 2324 m 4277 2440 l 4185 2357 l col0 s % Polyline gs clippath 2655 1278 m 2625 1398 l 2595 1278 l 2595 1440 l 2655 1440 l cp clip n 2625 1125 m 2625 1425 l gs col0 s gr gr % arrowhead n 2655 1278 m 2625 1398 l 2595 1278 l col0 s % Polyline gs clippath 2861 2308 m 2903 2424 l 2811 2341 l 2901 2476 l 2951 2443 l cp 2425 2341 m 2332 2424 l 2375 2308 l 2285 2443 l 2335 2476 l cp clip n 2318 2447 m 2618 1997 l 2918 2447 l gs col0 s gr gr % arrowhead n 2425 2341 m 2332 2424 l 2375 2308 l col0 s % arrowhead n 2861 2308 m 2903 2424 l 2811 2341 l col0 s % Polyline gs clippath 11098 1503 m 10975 1519 l 11075 1448 l 10925 1508 l 10947 1563 l cp clip n 12075 1080 m 10950 1530 l gs col0 s gr gr % arrowhead n 11098 1503 m 10975 1519 l 11075 1448 l col0 s % Polyline gs clippath 13075 1448 m 13174 1519 l 13052 1503 l 13203 1563 l 13225 1508 l cp clip n 12075 1080 m 13200 1530 l gs col0 s gr gr % arrowhead n 13075 1448 m 13174 1519 l 13052 1503 l col0 s % Polyline gs clippath 10968 2366 m 11010 2482 l 10918 2399 l 11008 2534 l 11058 2501 l cp 10532 2399 m 10439 2482 l 10482 2366 l 10392 2501 l 10442 2534 l cp clip n 10425 2505 m 10725 2055 l 11025 2505 l gs col0 s gr gr % arrowhead n 10532 2399 m 10439 2482 l 10482 2366 l col0 s % arrowhead n 10968 2366 m 11010 2482 l 10918 2399 l col0 s % Polyline gs clippath 13685 2354 m 13727 2470 l 13635 2387 l 13725 2522 l 13775 2489 l cp 13249 2387 m 13156 2470 l 13199 2354 l 13109 2489 l 13159 2522 l cp clip n 13142 2493 m 13442 2043 l 13742 2493 l gs col0 s gr gr % arrowhead n 13249 2387 m 13156 2470 l 13199 2354 l col0 s % arrowhead n 13685 2354 m 13727 2470 l 13635 2387 l col0 s % Polyline gs clippath 12105 1308 m 12075 1428 l 12045 1308 l 12045 1470 l 12105 1470 l cp clip n 12075 1155 m 12075 1455 l gs col0 s gr gr % arrowhead n 12105 1308 m 12075 1428 l 12045 1308 l col0 s % Polyline gs clippath 12311 2338 m 12353 2454 l 12261 2371 l 12351 2506 l 12401 2473 l cp 11875 2371 m 11782 2454 l 11825 2338 l 11735 2473 l 11785 2506 l cp clip n 11768 2477 m 12068 2027 l 12368 2477 l gs col0 s gr gr % arrowhead n 11875 2371 m 11782 2454 l 11825 2338 l col0 s % arrowhead n 12311 2338 m 12353 2454 l 12261 2371 l col0 s /Times-Roman ff 330.00 scf sf 8100 2925 m gs 1 -1 sc (0) col0 sh gr /Times-Roman ff 330.00 scf sf 8700 2925 m gs 1 -1 sc (1) col0 sh gr /Times-Italic ff 330.00 scf sf 8400 1800 m gs 1 -1 sc (g) col0 sh gr /Times-Roman ff 330.00 scf sf 7050 1875 m gs 1 -1 sc (1) col0 sh gr /Times-Roman ff 330.00 scf sf 5700 1875 m gs 1 -1 sc (0) col0 sh gr /Times-Roman ff 270.00 scf sf 5250 900 m gs 1 -1 sc (+) col0 sh gr /Times-Roman ff 330.00 scf sf 900 2925 m gs 1 -1 sc (0) col0 sh gr /Times-Roman ff 330.00 scf sf 1500 2925 m gs 1 -1 sc (1) col0 sh gr /Times-Italic ff 330.00 scf sf 1200 1800 m gs 1 -1 sc (g) col0 sh gr /Times-Roman ff 330.00 scf sf 3600 2925 m gs 1 -1 sc (0) col0 sh gr /Times-Roman ff 330.00 scf sf 4200 2925 m gs 1 -1 sc (1) col0 sh gr /Times-Italic ff 330.00 scf sf 3900 1800 m gs 1 -1 sc (g) col0 sh gr /Times-Italic ff 330.00 scf sf 2550 1800 m gs 1 -1 sc (g) col0 sh gr /Times-Roman ff 330.00 scf sf 2250 2925 m gs 1 -1 sc (0) col0 sh gr /Times-Roman ff 330.00 scf sf 2850 2925 m gs 1 -1 sc (1) col0 sh gr /Times-Roman ff 330.00 scf sf 10350 2955 m gs 1 -1 sc (0) col0 sh gr /Times-Roman ff 330.00 scf sf 10950 2955 m gs 1 -1 sc (1) col0 sh gr /Times-Italic ff 330.00 scf sf 10650 1830 m gs 1 -1 sc (g) col0 sh gr /Times-Roman ff 330.00 scf sf 13050 2955 m gs 1 -1 sc (0) col0 sh gr /Times-Roman ff 330.00 scf sf 13650 2955 m gs 1 -1 sc (1) col0 sh gr /Times-Italic ff 330.00 scf sf 13350 1830 m gs 1 -1 sc (g) col0 sh gr /Times-Italic ff 330.00 scf sf 12000 1830 m gs 1 -1 sc (g) col0 sh gr /Times-Roman ff 330.00 scf sf 11700 2955 m gs 1 -1 sc (0) col0 sh gr /Times-Roman ff 330.00 scf sf 12300 2955 m gs 1 -1 sc (1) col0 sh gr /Times-Italic ff 330.00 scf sf 2595 870 m gs 1 -1 sc (F) col0 sh gr /Times-Italic ff 330.00 scf sf 7050 855 m gs 1 -1 sc (F) col0 sh gr /Times-Italic ff 330.00 scf sf 12030 900 m gs 1 -1 sc (F) col0 sh gr $F2psEnd rs %%EndDocument @endspecial 166 x(In)36 b(the)f(last)g(decade,)i(man)n(y)e(su\016cien) n(t)h(criteria)e(for)h(the)h(mo)r(dularit)n(y)e(of)i(termination)440 5111 y(ha)n(v)n(e)j(b)r(een)j(giv)n(en;)k(see)40 b([Mid90,)g(Ohl94)o(,) h(Gra96)n(])g(for)f(an)h(o)n(v)n(erview.)74 b(F)-7 b(or)40 b(instance,)440 5211 y(termination)e(is)g(mo)r(dular)g(for)g(the)g (classes)f(of)h(non-collapsing)f(and)h(non-duplicating)440 5310 y(TRSs.)53 b(These)33 b(results)f(are)g(due)i(to)f(Rusino)n(witc)n (h)f([Rus87)o(].)54 b(A)33 b(v)n(ery)f(simple)h(pro)r(of)f(of)440 5410 y(these)j(facts)g(can)g(b)r(e)h(found)f(in)h([Ohl93)o(,)f(BN98)o (].)60 b(Recall)35 b(that)g(a)g(rewrite)g(rule)g Fm(l)i Fn(!)f Fm(r)1851 5662 y Fp(4)p eop %%Page: 5 5 5 4 bop 440 531 a Fp(is)32 b(non-duplicating)f(if)i(no)e(v)-5 b(ariable)31 b(app)r(ears)g(more)g(often)i(in)f Fm(r)j Fp(than)d(in)g Fm(l)i Fp(and)d(that)i(a)440 631 y(non-duplicating)27 b(TRS)h(solely)f(consists)f(of)i(non-duplicating)f(rules.)565 731 y(In)d(the)h(con)n(text)g(of)f(noncop)n(ying)g(and)g(graph)g (rewriting,)g(the)h(coun)n(terexample)e(men-)440 830 y(tioned)28 b(ab)r(o)n(v)n(e)e(v)-5 b(anishes:)440 1540 y @beginspecial 0 @llx 0 @lly 719 @urx 160 @ury 3437 @rwi @setspecial %%BeginDocument: exGraph.eps %!PS-Adobe-2.0 EPSF-2.0 %%Title: exGraph.eps %%Creator: fig2dev Version 3.2 Patchlevel 1 %%CreationDate: Wed Mar 10 11:37:23 1999 %%For: enno@thymian (Enno Ohlebusch) %%Orientation: Portrait %%BoundingBox: 0 0 719 160 %%Pages: 0 %%BeginSetup %%EndSetup %%Magnification: 1.0000 %%EndComments /$F2psDict 200 dict def $F2psDict begin $F2psDict /mtrx matrix put /col-1 {0 setgray} bind def /col0 {0.000 0.000 0.000 srgb} bind def /col1 {0.000 0.000 1.000 srgb} bind def /col2 {0.000 1.000 0.000 srgb} bind def /col3 {0.000 1.000 1.000 srgb} bind def /col4 {1.000 0.000 0.000 srgb} bind def /col5 {1.000 0.000 1.000 srgb} bind def /col6 {1.000 1.000 0.000 srgb} bind def /col7 {1.000 1.000 1.000 srgb} bind def /col8 {0.000 0.000 0.560 srgb} bind def /col9 {0.000 0.000 0.690 srgb} bind def /col10 {0.000 0.000 0.820 srgb} bind def /col11 {0.530 0.810 1.000 srgb} bind def /col12 {0.000 0.560 0.000 srgb} bind def /col13 {0.000 0.690 0.000 srgb} bind def /col14 {0.000 0.820 0.000 srgb} bind def /col15 {0.000 0.560 0.560 srgb} bind def /col16 {0.000 0.690 0.690 srgb} bind def /col17 {0.000 0.820 0.820 srgb} bind def /col18 {0.560 0.000 0.000 srgb} bind def /col19 {0.690 0.000 0.000 srgb} bind def /col20 {0.820 0.000 0.000 srgb} bind def /col21 {0.560 0.000 0.560 srgb} bind def /col22 {0.690 0.000 0.690 srgb} bind def /col23 {0.820 0.000 0.820 srgb} bind def /col24 {0.500 0.190 0.000 srgb} bind def /col25 {0.630 0.250 0.000 srgb} bind def /col26 {0.750 0.380 0.000 srgb} bind def /col27 {1.000 0.500 0.500 srgb} bind def /col28 {1.000 0.630 0.630 srgb} bind def /col29 {1.000 0.750 0.750 srgb} bind def /col30 {1.000 0.880 0.880 srgb} bind def /col31 {1.000 0.840 0.000 srgb} bind def end save -41.0 188.0 translate 1 -1 scale /cp {closepath} bind def /ef {eofill} bind def /gr {grestore} bind def /gs {gsave} bind def /sa {save} bind def /rs {restore} bind def /l {lineto} bind def /m {moveto} bind def /rm {rmoveto} bind def /n {newpath} bind def /s {stroke} bind def /sh {show} bind def /slc {setlinecap} bind def /slj {setlinejoin} bind def /slw {setlinewidth} bind def /srgb {setrgbcolor} bind def /rot {rotate} bind def /sc {scale} bind def /sd {setdash} bind def /ff {findfont} bind def /sf {setfont} bind def /scf {scalefont} bind def /sw {stringwidth} bind def /tr {translate} bind def /tnt {dup dup currentrgbcolor 4 -2 roll dup 1 exch sub 3 -1 roll mul add 4 -2 roll dup 1 exch sub 3 -1 roll mul add 4 -2 roll dup 1 exch sub 3 -1 roll mul add srgb} bind def /shd {dup dup currentrgbcolor 4 -2 roll mul 4 -2 roll mul 4 -2 roll mul srgb} bind def /DrawEllipse { /endangle exch def /startangle exch def /yrad exch def /xrad exch def /y exch def /x exch def /savematrix mtrx currentmatrix def x y tr xrad yrad sc 0 0 1 startangle endangle arc closepath savematrix setmatrix } def /$F2psBegin {$F2psDict begin /$F2psEnteredState save def} def /$F2psEnd {$F2psEnteredState restore end} def %%EndProlog $F2psBegin 10 setmiterlimit n -1000 4127 m -1000 -1000 l 13653 -1000 l 13653 4127 l cp clip 0.06000 0.06000 sc 7.500 slw % Ellipse n 975 2775 270 270 0 360 DrawEllipse gs col0 s gr % Ellipse n 1575 2775 270 270 0 360 DrawEllipse gs col0 s gr % Ellipse n 1275 1725 270 270 0 360 DrawEllipse gs col0 s gr % Ellipse n 3675 2775 270 270 0 360 DrawEllipse gs col0 s gr % Ellipse n 4275 2775 270 270 0 360 DrawEllipse gs col0 s gr % Ellipse n 3975 1725 270 270 0 360 DrawEllipse gs col0 s gr % Ellipse n 2625 1725 270 270 0 360 DrawEllipse gs col0 s gr % Ellipse n 2325 2775 270 270 0 360 DrawEllipse gs col0 s gr % Ellipse n 2925 2775 270 270 0 360 DrawEllipse gs col0 s gr % Ellipse n 10500 2850 270 270 0 360 DrawEllipse gs col0 s gr % Ellipse n 11100 2850 270 270 0 360 DrawEllipse gs col0 s gr % Ellipse n 10800 825 270 270 0 360 DrawEllipse gs col0 s gr % Ellipse n 10800 1800 270 270 0 360 DrawEllipse gs col0 s gr % Ellipse n 12375 825 270 270 0 360 DrawEllipse gs col0 s gr % Ellipse n 12375 1800 270 270 0 360 DrawEllipse gs col0 s gr % Ellipse n 7125 750 270 270 0 360 DrawEllipse gs col0 s gr % Ellipse n 7125 1725 270 270 0 360 DrawEllipse gs col0 s gr % Ellipse n 8175 2775 270 270 0 360 DrawEllipse gs col0 s gr % Ellipse n 8775 2775 270 270 0 360 DrawEllipse gs col0 s gr % Ellipse n 8475 1725 270 270 0 360 DrawEllipse gs col0 s gr % Ellipse n 5775 1725 270 270 0 360 DrawEllipse gs col0 s gr % Ellipse n 2625 750 270 270 0 360 DrawEllipse gs col0 s gr % Polyline gs clippath 1623 1483 m 1500 1500 l 1600 1428 l 1475 1478 l 1497 1533 l cp clip n 2625 1050 m 1500 1500 l gs col0 s gr gr % arrowhead n 1623 1483 m 1500 1500 l 1600 1428 l col0 s % Polyline gs clippath 3650 1428 m 3750 1500 l 3627 1483 l 3753 1533 l 3775 1478 l cp clip n 2625 1050 m 3750 1500 l gs col0 s gr gr % arrowhead n 3650 1428 m 3750 1500 l 3627 1483 l col0 s % Polyline gs clippath 1533 2359 m 1575 2475 l 1483 2392 l 1558 2504 l 1608 2471 l cp 1067 2392 m 975 2475 l 1017 2359 l 942 2471 l 992 2504 l cp clip n 975 2475 m 1275 2025 l 1575 2475 l gs col0 s gr gr % arrowhead n 1067 2392 m 975 2475 l 1017 2359 l col0 s % arrowhead n 1533 2359 m 1575 2475 l 1483 2392 l col0 s % Polyline gs clippath 4250 2347 m 4292 2463 l 4200 2380 l 4275 2492 l 4325 2459 l cp 3784 2380 m 3692 2463 l 3734 2347 l 3659 2459 l 3709 2492 l cp clip n 3692 2463 m 3992 2013 l 4292 2463 l gs col0 s gr gr % arrowhead n 3784 2380 m 3692 2463 l 3734 2347 l col0 s % arrowhead n 4250 2347 m 4292 2463 l 4200 2380 l col0 s % Polyline gs clippath 2655 1305 m 2625 1425 l 2595 1305 l 2595 1440 l 2655 1440 l cp clip n 2625 1125 m 2625 1425 l gs col0 s gr gr % arrowhead n 2655 1305 m 2625 1425 l 2595 1305 l col0 s % Polyline gs clippath 2876 2331 m 2918 2447 l 2826 2364 l 2901 2476 l 2951 2443 l cp 2410 2364 m 2318 2447 l 2360 2331 l 2285 2443 l 2335 2476 l cp clip n 2318 2447 m 2618 1997 l 2918 2447 l gs col0 s gr gr % arrowhead n 2410 2364 m 2318 2447 l 2360 2331 l col0 s % arrowhead n 2876 2331 m 2918 2447 l 2826 2364 l col0 s % Polyline gs clippath 11051 2406 m 11093 2522 l 11001 2439 l 11076 2551 l 11126 2518 l cp 10585 2439 m 10493 2522 l 10535 2406 l 10460 2518 l 10510 2551 l cp clip n 10493 2522 m 10793 2072 l 11093 2522 l gs col0 s gr gr % arrowhead n 10585 2439 m 10493 2522 l 10535 2406 l col0 s % arrowhead n 11051 2406 m 11093 2522 l 11001 2439 l col0 s % Polyline gs clippath 10830 1380 m 10800 1500 l 10770 1380 l 10770 1515 l 10830 1515 l cp clip n 10800 1125 m 10800 1500 l gs col0 s gr gr % arrowhead n 10830 1380 m 10800 1500 l 10770 1380 l col0 s % Polyline gs clippath 10905 1380 m 10875 1500 l 10845 1380 l 10845 1515 l 10905 1515 l cp clip n 10875 1125 m 10875 1500 l gs col0 s gr gr % arrowhead n 10905 1380 m 10875 1500 l 10845 1380 l col0 s % Polyline gs clippath 10755 1380 m 10725 1500 l 10695 1380 l 10695 1515 l 10755 1515 l cp clip n 10725 1125 m 10725 1500 l gs col0 s gr gr % arrowhead n 10755 1380 m 10725 1500 l 10695 1380 l col0 s % Polyline gs clippath 12405 1380 m 12375 1500 l 12345 1380 l 12345 1515 l 12405 1515 l cp clip n 12375 1125 m 12375 1500 l gs col0 s gr gr % arrowhead n 12405 1380 m 12375 1500 l 12345 1380 l col0 s % Polyline gs clippath 12480 1380 m 12450 1500 l 12420 1380 l 12420 1515 l 12480 1515 l cp clip n 12450 1125 m 12450 1500 l gs col0 s gr gr % arrowhead n 12480 1380 m 12450 1500 l 12420 1380 l col0 s % Polyline gs clippath 12330 1380 m 12300 1500 l 12270 1380 l 12270 1515 l 12330 1515 l cp clip n 12300 1125 m 12300 1500 l gs col0 s gr gr % arrowhead n 12330 1380 m 12300 1500 l 12270 1380 l col0 s % Polyline gs clippath 9780 945 m 9900 975 l 9780 1005 l 9915 1005 l 9915 945 l cp clip n 9225 975 m 9900 975 l gs col0 s gr gr % arrowhead n 9780 945 m 9900 975 l 9780 1005 l col0 s % Polyline gs clippath 11880 945 m 12000 975 l 11880 1005 l 12015 1005 l 12015 945 l cp clip n 11325 975 m 12000 975 l gs col0 s gr gr % arrowhead n 11880 945 m 12000 975 l 11880 1005 l col0 s % Polyline gs clippath 6123 1483 m 6000 1500 l 6100 1428 l 5975 1478 l 5997 1533 l cp clip n 7125 1050 m 6000 1500 l gs col0 s gr gr % arrowhead n 6123 1483 m 6000 1500 l 6100 1428 l col0 s % Polyline gs clippath 7155 1305 m 7125 1425 l 7095 1305 l 7095 1440 l 7155 1440 l cp clip n 7125 1125 m 7125 1425 l gs col0 s gr gr % arrowhead n 7155 1305 m 7125 1425 l 7095 1305 l col0 s % Polyline gs clippath 8150 1428 m 8250 1500 l 8127 1483 l 8253 1533 l 8275 1478 l cp clip n 7125 1050 m 8250 1500 l gs col0 s gr gr % arrowhead n 8150 1428 m 8250 1500 l 8127 1483 l col0 s % Polyline gs clippath 8750 2347 m 8792 2463 l 8700 2380 l 8775 2492 l 8825 2459 l cp 8284 2380 m 8192 2463 l 8234 2347 l 8159 2459 l 8209 2492 l cp clip n 8192 2463 m 8492 2013 l 8792 2463 l gs col0 s gr gr % arrowhead n 8284 2380 m 8192 2463 l 8234 2347 l col0 s % arrowhead n 8750 2347 m 8792 2463 l 8700 2380 l col0 s % Polyline gs clippath 5205 945 m 5325 975 l 5205 1005 l 5340 1005 l 5340 945 l cp clip n 4650 975 m 5325 975 l gs col0 s gr gr % arrowhead n 5205 945 m 5325 975 l 5205 1005 l col0 s /Times-Roman ff 330.00 scf sf 900 2925 m gs 1 -1 sc (0) col0 sh gr /Times-Roman ff 330.00 scf sf 1500 2925 m gs 1 -1 sc (1) col0 sh gr /Times-Italic ff 330.00 scf sf 1200 1800 m gs 1 -1 sc (g) col0 sh gr /Times-Roman ff 330.00 scf sf 3600 2925 m gs 1 -1 sc (0) col0 sh gr /Times-Roman ff 330.00 scf sf 4200 2925 m gs 1 -1 sc (1) col0 sh gr /Times-Italic ff 330.00 scf sf 3900 1800 m gs 1 -1 sc (g) col0 sh gr /Times-Italic ff 330.00 scf sf 2550 1800 m gs 1 -1 sc (g) col0 sh gr /Times-Roman ff 330.00 scf sf 2250 2925 m gs 1 -1 sc (0) col0 sh gr /Times-Roman ff 330.00 scf sf 2850 2925 m gs 1 -1 sc (1) col0 sh gr /Times-Roman ff 330.00 scf sf 10425 3000 m gs 1 -1 sc (0) col0 sh gr /Times-Roman ff 330.00 scf sf 11025 3000 m gs 1 -1 sc (1) col0 sh gr /Times-Italic ff 330.00 scf sf 10725 1875 m gs 1 -1 sc (g) col0 sh gr /Times-Roman ff 330.00 scf sf 12150 1950 m gs 1 -1 sc (0/1) col0 sh gr /Times-Roman ff 330.00 scf sf 8100 2925 m gs 1 -1 sc (0) col0 sh gr /Times-Roman ff 330.00 scf sf 8700 2925 m gs 1 -1 sc (1) col0 sh gr /Times-Italic ff 330.00 scf sf 8400 1800 m gs 1 -1 sc (g) col0 sh gr /Times-Roman ff 330.00 scf sf 7050 1875 m gs 1 -1 sc (1) col0 sh gr /Times-Roman ff 330.00 scf sf 5700 1875 m gs 1 -1 sc (0) col0 sh gr /Times-Roman ff 270.00 scf sf 5250 900 m gs 1 -1 sc (+) col0 sh gr /Times-Italic ff 330.00 scf sf 2550 855 m gs 1 -1 sc (F) col0 sh gr /Times-Italic ff 330.00 scf sf 7035 855 m gs 1 -1 sc (F) col0 sh gr /Times-Italic ff 330.00 scf sf 10710 945 m gs 1 -1 sc (F) col0 sh gr /Times-Italic ff 330.00 scf sf 12315 945 m gs 1 -1 sc (F) col0 sh gr $F2psEnd rs %%EndDocument @endspecial 164 x(Mo)r(dularit)n(y)20 b(of)h(termination)f(for)h (graph)e(rewriting)h(w)n(as)g(\014rst)h(pro)n(v)n(ed)e(b)n(y)i(Plump)f ([Plu91)o(])440 1804 y(in)41 b(the)g(con)n(text)f(of)h(jungle)g(ev)-5 b(aluation.)75 b(Kurihara)38 b(and)j(Oh)n(uc)n(hi)f([K)n(O95)n(])h (obtained)440 1903 y(the)g(same)e(result)h(for)g(noncop)n(ying)e (rewriting.)74 b(\(Here)40 b(w)n(e)g(only)g(deal)g(with)g(disjoin)n(t) 440 2003 y(systems;)23 b(for)e(results)g(on)g(more)g(general)f(kinds)h (of)h(com)n(binations,)f(the)h(reader)e(is)i(referred)440 2103 y(to)37 b([Plu91)o(,)g(K)n(O95)n(,)g(KR98)o(,)g(Plu98)o(]\).)66 b(A)38 b(simpler)f(pro)r(of)f(for)h(b)r(oth)h(results)e(has)h(b)r(een) 440 2202 y(presen)n(ted)30 b(in)g([Ohl98)o(].)46 b(The)30 b(simple)h(pro)r(of)f(uses)g(essen)n(tially)f(the)i(same)f(ideas)f(as)h (that)440 2302 y(of)38 b([Ohl93)o(])g(and)g(it)g(sho)n(ws)f(that)h (there)g(is)g(a)g(v)n(ery)f(close)g(relationship)g(b)r(et)n(w)n(een)h (non-)440 2402 y(duplicating)h(term)g(rewriting)f(and)h(graph)f (rewriting.)71 b(W)-7 b(e)39 b(will)h(tak)n(e)e(this)h(one)g(step)440 2501 y(further.)51 b(In)33 b(the)g(uniform)f(framew)n(ork)e(of)j(term,) h(graph,)e(and)g(noncop)n(ying)f(rewriting,)440 2601 y(it)j(is)g(p)r(ossible)g(to)g(giv)n(e)f Fq(one)h Fp(pro)r(of)g(for)f (the)i Fq(thr)l(e)l(e)f Fp(mo)r(dularit)n(y)f(results)h(from)f (di\013eren)n(t)440 2700 y(\014elds.)565 2800 y(Throughout)26 b(the)i(rest)f(of)g(the)h(pap)r(er,)f(let)h Fn(R)2014 2812 y Fj(1)2079 2800 y Fp(and)f Fn(R)2310 2812 y Fj(2)2375 2800 y Fp(b)r(e)h(TRSs)g(o)n(v)n(er)d(the)j(disjoin)n(t)440 2900 y(signatures)f Fn(F)894 2912 y Fj(1)959 2900 y Fp(and)h Fn(F)1181 2912 y Fj(2)1247 2900 y Fp(and)g(let)g Fn(R)d Fp(=)f Fn(R)1783 2912 y Fj(1)1839 2900 y Fn([)c(R)1984 2912 y Fj(2)2049 2900 y Fp(b)r(e)29 b(their)f(com)n(bined)g(system)g(o) n(v)n(er)f(the)440 2999 y(signature)f Fn(F)31 b Fp(=)23 b Fn(F)1047 3011 y Fj(1)1103 2999 y Fn([)18 b(F)1244 3011 y Fj(2)1282 2999 y Fp(.)565 3099 y(W)-7 b(e)39 b(start)g(with)g(a) g(brief)g(o)n(v)n(erview)e(of)i(the)g(basic)g(notions)f(of)h(disjoin)n (t)h(unions)e(of)440 3199 y(mark)n(ed)31 b(rewrite)g(relations.)50 b(Let)32 b Fm(t)1593 3168 y Fl(\003)1662 3199 y Fn(2)f(T)21 b Fp(\()p Fn(F)1914 3168 y Fl(\003)1953 3199 y Fm(;)14 b Fn(V)2048 3168 y Fl(\003)2085 3199 y Fp(\))33 b(and)f(supp)r(ose)g Fm(t)2663 3168 y Fl(\003)2732 3199 y Fp(=)e Fm(C)2892 3168 y Fl(\003)2930 3199 y Fp([)p Fm(t)2983 3168 y Fl(\003)2983 3219 y Fj(1)3022 3199 y Fm(;)14 b(:)g(:)g(:)f(;)h(t)3236 3168 y Fl(\003)3236 3219 y Fk(n)3281 3199 y Fp(])440 3298 y(with)32 b Fm(C)698 3268 y Fl(\003)765 3298 y Fn(6)p Fp(=)c Fh(2)p Fp(.)47 b(If)32 b Fm(C)1142 3268 y Fl(\003)1209 3298 y Fn(2)d(T)21 b Fp(\()p Fn(F)1459 3268 y Fl(\003)1451 3322 y Fk(k)1519 3298 y Fn([)g(f)p Fh(2)p Fn(g)p Fm(;)14 b Fn(V)1836 3268 y Fl(\003)1872 3298 y Fp(\))32 b(and)f Fm(r)r(oot)p Fp(\()p Fm(t)2312 3268 y Fl(\003)2312 3319 y Fj(1)2351 3298 y Fp(\))p Fm(;)h(:)14 b(:)g(:)g(;)g(r)r(oot)p Fp(\()p Fm(t)2797 3268 y Fl(\003)2797 3319 y Fk(n)2843 3298 y Fp(\))29 b Fn(2)g(F)3056 3268 y Fl(\003)3048 3322 y Fj(3)p Fl(\000)p Fk(k)3205 3298 y Fp(for)440 3398 y(some)i Fm(k)h Fn(2)e(f)p Fp(1)p Fm(;)14 b Fp(2)p Fn(g)p Fp(,)31 b(then)h(w)n(e)f(write)g Fm(t)1636 3368 y Fl(\003)1704 3398 y Fp(=)e Fm(C)1863 3368 y Fl(\003)1902 3398 y Fp([)-14 b([)p Fm(t)1964 3368 y Fl(\003)1964 3418 y Fj(1)2002 3398 y Fm(;)14 b(:)g(:)g(:)g(;)g(t)2217 3368 y Fl(\003)2217 3418 y Fk(n)2262 3398 y Fp(])-14 b(].)49 b(In)32 b(this)f(case)g(w)n(e) g(de\014ne)h(the)440 3497 y Fq(set)26 b Fm(S)5 b Fp(\()p Fm(t)684 3467 y Fl(\003)722 3497 y Fp(\))26 b(of)g(all)g Fq(princip)l(al)i Fp(subterms)d(of)h Fm(t)1805 3467 y Fl(\003)1869 3497 y Fp(b)n(y)g Fm(S)5 b Fp(\()p Fm(t)2101 3467 y Fl(\003)2139 3497 y Fp(\))23 b(=)g Fn(f)p Fm(t)2354 3467 y Fl(\003)2354 3518 y Fj(1)2392 3497 y Fm(;)14 b(:)g(:)g(:)f(;)h (t)2606 3467 y Fl(\003)2606 3518 y Fk(n)2651 3497 y Fn(g)26 b Fp(and)g(the)g Fq(topmost)440 3597 y(homo)l(gene)l(ous)31 b(p)l(art)c Fm(top)p Fp(\()p Fm(t)1283 3567 y Fl(\003)1322 3597 y Fp(\))h(of)f Fm(t)1506 3567 y Fl(\003)1572 3597 y Fp(b)n(y)h Fm(top)p Fp(\()p Fm(t)1862 3567 y Fl(\003)1900 3597 y Fp(\))23 b(=)g Fm(C)2108 3567 y Fl(\003)2146 3597 y Fp(.)37 b(F)-7 b(urthermore,)27 b(w)n(e)g(de\014ne)652 3777 y Fm(r)r(ank)s Fp(\()p Fm(t)893 3743 y Fl(\003)932 3777 y Fp(\))d(=)e(1)c(+)g(max)p Fn(f)p Fm(r)r(ank)s Fp(\()p Fm(t)1656 3743 y Fl(\003)1656 3798 y Fk(j)1694 3777 y Fp(\))42 b Fn(j)f Fp(1)23 b Fn(\024)g Fm(j)28 b Fn(\024)22 b Fm(n)p Fn(g)27 b Fp(for)g Fm(t)2410 3743 y Fl(\003)2471 3777 y Fp(=)c Fm(C)2624 3743 y Fl(\003)2663 3777 y Fp([)-14 b([)p Fm(t)2725 3743 y Fl(\003)2725 3798 y Fj(1)2763 3777 y Fm(;)14 b(:)g(:)g(:)g(;)g(t)2978 3743 y Fl(\003)2978 3798 y Fk(n)3023 3777 y Fp(])-14 b(])p Fm(;)440 3957 y Fp(where)25 b(max)14 b Fn(;)22 b Fp(=)h(0.)36 b(Observ)n(e)24 b(that)i Fm(r)r(ank)s Fp(\()p Fm(t)1836 3927 y Fl(\003)1874 3957 y Fp(\))e(=)e Fm(r)r(ank)s Fp(\()p Fm(e)p Fp(\()p Fm(t)2329 3927 y Fl(\003)2368 3957 y Fp(\)\),)27 b(that)f(is)g(to)f(sa)n(y)-7 b(,)25 b(the)h(rank)440 4057 y(of)36 b(a)f(term)h(is)f(indep)r(enden)n(t)i(of)e(its)h(marking.) 121 b(A)36 b(mark)n(ed)f(rewrite)g(step)h Fm(s)2981 4027 y Fl(\003)3055 4057 y Fh(;)3138 4069 y Fl(R)3236 4057 y Fm(t)3266 4027 y Fl(\003)440 4156 y Fp(is)h Fq(destructive)i(at)g (level)g(1)f Fp(if)g Fm(r)r(oot)p Fp(\()p Fm(s)1651 4126 y Fl(\003)1690 4156 y Fp(\))i Fn(2)f(F)1924 4126 y Fl(\003)1916 4180 y Fk(k)1999 4156 y Fp(and)e Fm(r)r(oot)p Fp(\()p Fm(t)2381 4126 y Fl(\003)2421 4156 y Fp(\))i Fn(2)h(F)2655 4126 y Fl(\003)2647 4180 y Fj(3)p Fl(\000)p Fk(k)2810 4156 y Fp(for)c(some)h Fm(k)42 b Fn(2)440 4256 y(f)p Fp(1)p Fm(;)14 b Fp(2)p Fn(g)p Fp(.)68 b(A)39 b(mark)n(ed)f(reduction)g (step)h Fm(s)1750 4226 y Fl(\003)1829 4256 y Fh(;)1912 4268 y Fl(R)2015 4256 y Fm(t)2045 4226 y Fl(\003)2122 4256 y Fp(is)g Fq(destructive)h(at)g(level)h(2)e Fp(if)g Fm(s)3160 4226 y Fl(\003)3240 4256 y Fp(=)440 4356 y Fm(C)505 4325 y Fl(\003)543 4356 y Fp([)-14 b([)p Fm(s)614 4325 y Fl(\003)614 4376 y Fj(1)653 4356 y Fm(;)14 b(:)g(:)g(:)f(;)h(s) 876 4325 y Fl(\003)876 4377 y Fk(j)914 4356 y Fm(;)g(:)g(:)g(:)g(;)g(s) 1138 4325 y Fl(\003)1138 4376 y Fk(n)1183 4356 y Fp(])-14 b(])25 b Fh(;)1323 4368 y Fl(R)1409 4356 y Fm(C)1474 4325 y Fl(\003)1512 4356 y Fp([)p Fm(t)1565 4325 y Fl(\003)1565 4376 y Fj(1)1603 4356 y Fm(;)14 b(:)g(:)g(:)g(;)g(t)1818 4325 y Fl(\003)1818 4377 y Fk(j)1856 4356 y Fm(;)g(:)g(:)g(:)g(;)g(t) 2071 4325 y Fl(\003)2071 4376 y Fk(n)2116 4356 y Fp(])24 b(=)h Fm(t)2283 4325 y Fl(\003)2349 4356 y Fp(with)30 b Fm(s)2579 4325 y Fl(\003)2579 4377 y Fk(j)2641 4356 y Fh(;)2724 4368 y Fl(R)2810 4356 y Fm(t)2840 4325 y Fl(\003)2840 4377 y Fk(j)2907 4356 y Fp(destructiv)n(e)440 4455 y(at)d(lev)n(el)g(1)f(for)h(at)g(least)g(one)g Fm(j)h Fn(2)23 b(f)p Fp(1)p Fm(;)14 b(:)g(:)g(:)f(;)h(n)p Fn(g)p Fp(.)36 b(In)27 b(this)g(pap)r(er)g(a)g(mark)n(ed)f(rewrite)g(step)h (is)440 4555 y(called)g Fq(destructive)h Fp(if)g(it)g(is)g(either)f (destructiv)n(e)g(at)h(lev)n(el)f(1)g(or)g(at)g(lev)n(el)g(2.)565 4654 y(Let)k(\()p Fa(N)5 b Fm(;)14 b(>)p Fp(\))37 b(denote)32 b(the)g(usual)f(w)n(ell-founded)h(ordering)e(on)h(the)h(natural)f(n)n (um)n(b)r(ers)440 4754 y(and)24 b(\()p Fn(M)p Fp(\()p Fa(N)5 b Fp(\))p Fm(;)14 b(>)951 4724 y Fk(mult)1105 4754 y Fp(\))25 b(its)g(w)n(ell-founded)f(m)n(ultiset)h(extension;)g (see)g([DM79)o(,)g(BN98)o(])g(for)f(a)440 4854 y(de\014nition)k(of)g (this)f(notion.)37 b(W)-7 b(e)28 b(de\014ne)1186 5034 y Fm(]s)1257 4999 y Fl(\003)1318 5034 y Fp(=)23 b([)p Fm(r)r(ank)s Fp(\()p Fm(t)1670 4999 y Fl(\003)1709 5034 y Fp(\))28 b Fn(j)g Fm(t)1850 4999 y Fl(\003)1911 5034 y Fn(2)23 b Fm(S)5 b Fp(\()p Fm(s)2116 4999 y Fl(\003)2154 5034 y Fp(\)])24 b Fn(2)f(M)p Fp(\()p Fa(N)t Fp(\))p Fm(;)440 5214 y Fp(i.e.,)40 b Fm(]s)680 5184 y Fl(\003)756 5214 y Fp(denotes)e(the)g(m)n(ultiset)g(of)f(the)h(ranks)f(of)g(the)h (terms)f(in)h(the)g(set)g Fm(S)5 b Fp(\()p Fm(s)3068 5184 y Fl(\003)3106 5214 y Fp(\).)67 b(In)440 5313 y(con)n(trast)27 b(to)g Fm(r)r(ank)s Fp(\()p Fm(s)1113 5283 y Fl(\003)1152 5313 y Fp(\),)i Fm(]s)1307 5283 y Fl(\003)1373 5313 y Fp(hea)n(vily)e(dep)r(ends)h(on)g(the)g(marking)f(of)h Fm(s)2697 5283 y Fl(\003)2735 5313 y Fp(.)38 b(If)28 b(for)g(example)440 5413 y Fn(F)508 5425 y Fj(1)568 5413 y Fp(=)23 b Fn(f)p Fm(G)p Fn(g)k Fp(and)g Fn(F)1061 5425 y Fj(2)1121 5413 y Fp(=)c Fn(f)p Fm(a)p Fn(g)p Fp(,)k(then)h Fm(]G)1673 5383 y Fj(0)1711 5413 y Fp(\()p Fm(a)1787 5383 y Fj(1)1824 5413 y Fm(;)14 b(a)1905 5383 y Fj(2)1942 5413 y Fp(\))23 b(=)g([1)p Fm(;)14 b Fp(1])27 b(but)h Fm(]G)2528 5383 y Fj(0)2566 5413 y Fp(\()p Fm(a)2642 5383 y Fj(1)2679 5413 y Fm(;)14 b(a)2760 5383 y Fj(1)2797 5413 y Fp(\))24 b(=)e([1].)1851 5662 y(5)p eop %%Page: 6 6 6 5 bop 440 531 a Fg(Lemma)30 b(3.1)40 b Fq(If)30 b Fm(s)1068 501 y Fl(\003)1129 531 y Fh(;)1212 501 y Fl(\003)1212 554 y(R)1297 531 y Fm(t)1327 501 y Fl(\003)1365 531 y Fq(,)g(then)g Fm(r)r(ank)s Fp(\()p Fm(s)1855 501 y Fl(\003)1893 531 y Fp(\))24 b Fn(\025)e Fm(r)r(ank)s Fp(\()p Fm(t)2277 501 y Fl(\003)2316 531 y Fp(\))p Fq(.)440 727 y(Pr)l(o)l(of)58 b Fp(The)27 b(lemma)g(follo)n(ws)f(from)h(Lemma)g(2.2)f(in)i (conjunction)f(with)h(the)f(w)n(ell)g(kno)n(wn)440 826 y(fact)h(that)g(an)f(unmark)n(ed)g(rewrite)f(step)i(cannot)f(increase)g (the)h(rank.)578 b Ff(\003)440 1021 y Fg(Lemma)30 b(3.2)40 b Fq(If)30 b Fm(s)1068 991 y Fl(\003)1129 1021 y Fh(;)1212 1033 y Fl(R)1297 1021 y Fm(t)1327 991 y Fl(\003)1394 1021 y Fq(is)h(destructive,)f(then)g Fm(]s)2184 991 y Fl(\003)2245 1021 y Fm(>)2310 991 y Fk(mult)2481 1021 y Fm(]t)2543 991 y Fl(\003)2582 1021 y Fq(.)440 1217 y(Pr)l(o)l(of)49 b Fp(If)23 b Fm(s)798 1186 y Fl(\003)859 1217 y Fh(;)942 1229 y Fl(R)1026 1217 y Fm(t)1056 1186 y Fl(\003)1117 1217 y Fp(is)f(destructiv)n(e)g(at)h(lev)n(el)f(1,)h (then)g(the)g(lemma)g(immediately)f(follo)n(ws.)440 1316 y(Supp)r(ose)31 b Fm(s)808 1286 y Fl(\003)876 1316 y Fh(;)959 1328 y Fl(R)1049 1316 y Fm(t)1079 1286 y Fl(\003)1149 1316 y Fp(is)g(destructiv)n(e)g(at)g(lev)n(el)g(2.)47 b(W)-7 b(e)32 b(ha)n(v)n(e)e Fm(s)2456 1286 y Fl(\003)2523 1316 y Fp(=)f Fm(C)2682 1286 y Fl(\003)2721 1316 y Fp([)-14 b([)p Fm(s)2792 1286 y Fl(\003)2792 1337 y Fj(1)2830 1316 y Fm(;)14 b(:)g(:)g(:)g(;)g(s)3054 1286 y Fl(\003)3054 1337 y Fk(n)3099 1316 y Fp(])-14 b(])29 b Fh(;)3243 1328 y Fl(R)440 1416 y Fm(C)505 1386 y Fl(\003)543 1416 y Fp([)p Fm(t)596 1386 y Fl(\003)596 1436 y Fj(1)635 1416 y Fm(;)14 b(:)g(:)g(:)f(;)h(t)849 1386 y Fl(\003)849 1436 y Fk(n)894 1416 y Fp(])26 b(=)f Fm(t)1063 1386 y Fl(\003)1101 1416 y Fp(,)30 b(where)e(either)h Fm(s)1671 1386 y Fl(\003)1671 1437 y Fk(j)1735 1416 y Fp(=)c Fm(t)1855 1386 y Fl(\003)1855 1437 y Fk(j)1922 1416 y Fp(or)k Fm(s)2065 1386 y Fl(\003)2065 1437 y Fk(j)2128 1416 y Fh(;)2211 1428 y Fl(R)2298 1416 y Fm(t)2328 1386 y Fl(\003)2328 1437 y Fk(j)2395 1416 y Fp(for)g(1)c Fn(\024)g Fm(j)31 b Fn(\024)25 b Fm(n)p Fp(.)41 b(Note)29 b(that)440 1515 y(the)i(outer)g(con)n(text)g Fm(C)1171 1485 y Fl(\003)1240 1515 y Fp(is)g(not)g(a\013ected)h(b)n(y)e(the)i(mark)n(ed)e(reduction)h (step.)47 b(Moreo)n(v)n(er,)440 1615 y(there)40 b(is)h(at)f(least)g (one)g(index)h Fm(k)i Fp(suc)n(h)e(that)f Fm(s)2003 1585 y Fl(\003)2003 1639 y Fk(k)2089 1615 y Fh(;)2172 1627 y Fl(R)2278 1615 y Fm(t)2308 1585 y Fl(\003)2308 1639 y Fk(k)2389 1615 y Fp(is)g(destructiv)n(e)g(at)h(lev)n(el)f(1.)440 1715 y(Apparen)n(tly)-7 b(,)35 b([)p Fm(r)r(ank)s Fp(\()p Fm(s)1173 1685 y Fl(\003)1173 1738 y Fk(k)1214 1715 y Fp(\)])f Fm(>)1368 1685 y Fk(mult)1549 1715 y Fm(]t)1611 1685 y Fl(\003)1611 1738 y Fk(k)1653 1715 y Fp(.)55 b(It)34 b(is)g(not)f(di\016cult)i(to)e(see)h(that)g Fm(]s)2886 1685 y Fl(\003)2957 1715 y Fm(>)3022 1685 y Fk(mult)3204 1715 y Fm(]t)3266 1685 y Fl(\003)440 1814 y Fp(follo)n(ws)27 b(as)g(a)g(consequence)f(b)r(ecause)i Fm(s)1699 1784 y Fl(\003)1699 1836 y Fk(i)1760 1814 y Fp(=)22 b Fm(s)1886 1784 y Fl(\003)1886 1836 y Fk(j)1952 1814 y Fp(implies)28 b Fm(t)2264 1784 y Fl(\003)2264 1836 y Fk(i)2325 1814 y Fp(=)23 b Fm(t)2443 1784 y Fl(\003)2443 1836 y Fk(j)2481 1814 y Fp(.)736 b Ff(\003)440 2009 y Fg(De\014nition)31 b(3.3)40 b Fp(F)-7 b(or)29 b(ev)n(ery)f(mark)n(ed)g(rewrite)g(deriv)-5 b(ation)29 b Fm(D)f Fp(:)d Fm(s)2577 1979 y Fl(\003)2577 2030 y Fj(1)2641 2009 y Fh(;)2724 2021 y Fl(R)2811 2009 y Fm(s)2850 1979 y Fl(\003)2850 2030 y Fj(2)2914 2009 y Fh(;)2997 2021 y Fl(R)3084 2009 y Fm(:)14 b(:)g(:)29 b Fp(w)n(e)440 2109 y(de\014ne)f(the)g Fq(r)l(ank)g Fp(of)f Fm(D)j Fp(b)n(y)d Fm(r)r(ank)s Fp(\()p Fm(D)r Fp(\))d(=)f Fm(r)r(ank)s Fp(\()p Fm(s)1993 2079 y Fl(\003)1993 2130 y Fj(1)2031 2109 y Fp(\).)440 2287 y Fg(Theorem)30 b(3.4)41 b Fq(L)l(et)29 b(b)l(oth)h Ff( )1411 2299 y Fl(R)1468 2307 y Fb(1)1535 2287 y Fq(and)g Ff( )1779 2299 y Fl(R)1836 2307 y Fb(2)1902 2287 y Fq(b)l(e)g(either)h(marke)l(d,)g(term,)f(gr)l (aph,)i(or)e(non-)440 2386 y(c)l(opying)f(r)l(ewrite)g(r)l(elations.)39 b(If)28 b Ff( )1556 2398 y Fl(R)1613 2406 y Fb(1)1678 2386 y Fq(and)g Ff( )1920 2398 y Fl(R)1977 2406 y Fb(2)2042 2386 y Fq(ar)l(e)g(terminating)g(and)h(for)g(every)g(non-)440 2486 y(destructive)42 b(r)l(ewrite)g(step)g Fm(s)1386 2456 y Fl(\003)1469 2486 y Ff( )1552 2498 y Fl(R)1658 2486 y Fm(t)1688 2456 y Fl(\003)1726 2486 y Fq(,)j(we)d(have)h Fm(]s)2205 2456 y Fl(\003)2288 2486 y Fn(\025)2353 2456 y Fk(mult)2546 2486 y Fm(]t)2608 2456 y Fl(\003)2688 2486 y Fq(and)g Fm(top)p Fp(\()p Fm(s)3045 2456 y Fl(\003)3083 2486 y Fp(\))i Ff( )3243 2456 y Fl(\003)3243 2509 y(R)440 2586 y Fm(top)p Fp(\()p Fm(t)614 2555 y Fl(\003)652 2586 y Fp(\))p Fq(,)31 b(then)e Ff( )1007 2598 y Fl(R)1098 2586 y Fq(is)h(also)h(terminating.)440 2781 y(Pr)l(o)l(of)59 b Fp(F)-7 b(or)27 b(an)g(indirect)g(pro)r(of,)h(supp)r(ose)f(that)h (there)f(is)h(an)f(in\014nite)h Ff( )2767 2793 y Fl(R)2828 2781 y Fp(-deriv)-5 b(ation)1354 2958 y Fm(D)25 b Fp(:)e Fm(s)1533 2970 y Fj(1)1593 2958 y Ff( )1676 2970 y Fl(R)1761 2958 y Fm(s)1800 2970 y Fj(2)1860 2958 y Ff( )1943 2970 y Fl(R)2027 2958 y Fm(s)2066 2970 y Fj(3)2126 2958 y Ff( )2209 2970 y Fl(R)2294 2958 y Fm(:)14 b(:)g(:)440 3136 y Fp(Without)32 b(loss)f(of)h(generalit)n(y)-7 b(,)31 b(w)n(e)g(ma)n(y)g(assume)g(that)h Fm(r)r(ank)s Fp(\()p Fm(D)r Fp(\))h(is)e(minimal,)i(i.e.,)g(an)n(y)440 3235 y Ff( )523 3247 y Fl(R)584 3235 y Fp(-deriv)-5 b(ation)27 b(of)g(smaller)g(rank)g(is)g(\014nite.)565 3335 y(First)22 b(of)h(all)g(notice)g(that)g Fm(D)j Fp(can)c(b)r(e)i(view)n(ed)e(as)h (a)f Fh(;)2241 3347 y Fl(R)2302 3335 y Fp(-deriv)-5 b(ation)23 b(since)f Ff( )2997 3347 y Fl(R)3072 3335 y Fn(\022)p Fh(;)3220 3347 y Fl(R)3281 3335 y Fp(.)440 3435 y(F)-7 b(urthermore,)24 b(w)n(e)f(ha)n(v)n(e)g Fm(r)r(ank)s Fp(\()p Fm(s)1498 3447 y Fk(j)1533 3435 y Fp(\))h(=)e Fm(r)r(ank)s Fp(\()p Fm(D)r Fp(\))j(for)e(all)h(indices)g Fm(j)5 b Fp(.)35 b(In)24 b(particular,)g(there)440 3534 y(is)k(no)h(step)f(whic)n(h)h(is)f(destructiv)n(e)g(at)g(lev)n(el)g(1.) 39 b(Finally)-7 b(,)29 b(without)g(loss)e(of)i(generalit)n(y)e(w)n(e) 440 3634 y(ma)n(y)g(assume)g(that)h Fm(r)r(oot)p Fp(\()p Fm(s)1307 3646 y Fj(1)1345 3634 y Fp(\))c Fn(2)f(F)1547 3604 y Fl(\003)1539 3655 y Fj(1)1613 3634 y Fp(and)k(hence)h Fm(r)r(oot)p Fp(\()p Fm(s)2225 3646 y Fk(j)2261 3634 y Fp(\))c Fn(2)f(F)2463 3604 y Fl(\003)2455 3655 y Fj(1)2529 3634 y Fp(for)k(all)g Fm(j)h Fn(\025)23 b Fp(1.)565 3734 y(There)28 b(is)h(only)f(a)g(\014nite)i(n)n(um)n(b)r(er)e(of)h(steps)g (in)g Fm(D)i Fp(whic)n(h)e(are)e(destructiv)n(e)i(at)f(lev)n(el)h(2)440 3833 y(b)r(ecause)e Fm(>)812 3803 y Fk(mult)988 3833 y Fp(is)h(w)n(ell-founded)f(and)565 3995 y Fn(\017)41 b Fm(s)687 4007 y Fk(j)745 3995 y Ff( )828 4007 y Fl(R)912 3995 y Fm(s)951 4007 y Fk(j)s Fj(+1)1097 3995 y Fp(destructiv)n(e)27 b(at)h(lev)n(el)f(2)g(implies)h Fm(]s)2235 4007 y Fk(j)2293 3995 y Fm(>)2358 3965 y Fk(mult)2530 3995 y Fm(]s)2601 4007 y Fk(j)s Fj(+1)2748 3995 y Fp(b)n(y)f(Lemma)g(3.2,)565 4159 y Fn(\017)41 b Fm(s)687 4171 y Fk(j)745 4159 y Ff( )828 4171 y Fl(R)912 4159 y Fm(s)951 4171 y Fk(j)s Fj(+1)1097 4159 y Fp(non-destructiv)n(e)27 b(at)g(lev)n(el)g(2)h(yields)f Fm(]s)2348 4171 y Fk(j)2406 4159 y Fn(\025)2471 4129 y Fk(mult)2643 4159 y Fm(]s)2714 4171 y Fk(j)s Fj(+1)2833 4159 y Fp(.)440 4321 y(Th)n(us,)e(without)h(loss)e(of)h(generalit)n(y) -7 b(,)24 b(w)n(e)h(ma)n(y)f(further)h(assume)g(that)g(there)g(is)g(no) g(step)g(in)440 4421 y Fm(D)j Fp(whic)n(h)d(is)h(destructiv)n(e)f(at)g (lev)n(el)g(2.)36 b(Hence)26 b Fm(D)h Fp(do)r(es)f(not)f(con)n(tain)g (destructiv)n(e)g(rewrite)440 4520 y(steps)j(at)f(all.)37 b(According)27 b(to)g(the)i(premise,)e(w)n(e)g(then)h(ha)n(v)n(e)f Fm(top)p Fp(\()p Fm(s)2552 4532 y Fk(j)2587 4520 y Fp(\))d Ff( )2726 4490 y Fl(\003)2726 4543 y(R)2783 4551 y Fb(1)2843 4520 y Fm(top)p Fp(\()p Fm(s)3026 4532 y Fk(j)s Fj(+1)3145 4520 y Fp(\))k(for)440 4620 y(ev)n(ery)k(step)i Fm(s)886 4632 y Fk(j)954 4620 y Ff( )1037 4632 y Fl(R)1131 4620 y Fm(s)1170 4632 y Fk(j)s Fj(+1)1323 4620 y Fp(in)f Fm(D)r Fp(.)55 b(Since)34 b Ff( )1880 4632 y Fl(R)1937 4640 y Fb(1)2007 4620 y Fp(is)f(terminating,)i(there)f(can)f(b)r(e)h(only)f (a)440 4720 y(\014nite)23 b(n)n(um)n(b)r(er)f(of)g(steps)g(with)g Fm(top)p Fp(\()p Fm(s)1602 4732 y Fk(j)1637 4720 y Fp(\))i Ff( )1776 4684 y Fj(+)1776 4744 y Fl(R)1833 4752 y Fb(1)1892 4720 y Fm(top)p Fp(\()p Fm(s)2075 4732 y Fk(j)s Fj(+1)2195 4720 y Fp(\))e(in)h Fm(D)r Fp(.)35 b(So)22 b(w)n(e)f(ma)n(y)h(assume)f (that)440 4819 y Fm(D)35 b Fp(con)n(tains)d(none)h(of)g(these)h(steps,) g(or)e(in)i(other)e(w)n(ords,)i Fm(top)p Fp(\()p Fm(s)2520 4831 y Fk(j)2555 4819 y Fp(\))e(=)g Fm(top)p Fp(\()p Fm(s)2899 4831 y Fk(j)s Fj(+1)3019 4819 y Fp(\))h(for)g(all)440 4919 y Fm(j)28 b Fn(\025)23 b Fp(1.)35 b(Th)n(us,)23 b(if)h Fm(s)1030 4931 y Fj(1)1090 4919 y Fp(=)f Fm(C)6 b Fp([)-14 b([)p Fm(t)1305 4931 y Fj(1)1342 4919 y Fm(;)14 b(:)g(:)g(:)g(;)g(t)1557 4931 y Fk(n)1602 4919 y Fp(])-14 b(],)24 b(then)g(there)e(m)n(ust)h(b)r(e)h(an)e(in\014nite)i Ff( )2853 4931 y Fl(R)2914 4919 y Fp(-deriv)-5 b(ation)440 5019 y(starting)24 b(from)g(some)g Fm(t)1175 5031 y Fk(k)1239 5019 y Fn(2)f Fm(S)5 b Fp(\()p Fm(s)1444 5031 y Fj(1)1482 5019 y Fp(\).)36 b(Ho)n(w)n(ev)n(er,)23 b(this)i(con)n(tradicts)f(the)h (fact)f(that)h Fm(r)r(ank)s Fp(\()p Fm(D)r Fp(\))440 5118 y(is)i(minimal)h(b)r(ecause)g Fm(r)r(ank)s Fp(\()p Fm(t)1395 5130 y Fk(k)1436 5118 y Fp(\))23 b Fm(<)g(r)r(ank)s Fp(\()p Fm(s)1829 5130 y Fj(1)1867 5118 y Fp(\).)1318 b Ff(\003)565 5313 y Fp(The)24 b(next)h(lemma)f(sho)n(ws)g(that)h(the)f (last)h(condition)f(in)h(Theorem)e(3.4)h(is)h(satis\014ed)f(b)n(y)440 5413 y(ev)n(ery)i(relation)h(under)g(consideration.)36 b(The)27 b(simple)h(pro)r(of)f(is)h(omitted.)1851 5662 y(6)p eop %%Page: 7 7 7 6 bop 440 531 a Fg(Lemma)30 b(3.5)40 b Fq(L)l(et)e Ff( )1177 543 y Fl(R)1276 531 y Fq(b)l(e)h(either)g Fh(;)1715 543 y Fl(R)1776 531 y Fq(,)71 b Fn(\))1955 543 y Fl(R)2046 531 y Fq(,)f Fn(\))2224 501 y Fk(nc)2224 554 y Fl(R)2329 531 y Fq(,)41 b(or)e Fn(!)2594 543 y Fl(R)2655 531 y Fq(.)64 b(If)39 b Fm(s)2879 501 y Fl(\003)2956 531 y Ff( )3039 543 y Fl(R)3138 531 y Fm(t)3168 501 y Fl(\003)3245 531 y Fq(is)440 631 y(non-destructive,)30 b(then)g Fm(top)p Fp(\()p Fm(s)1418 601 y Fl(\003)1456 631 y Fp(\))23 b Ff( )1594 643 y Fl(R)1679 631 y Fm(top)p Fp(\()p Fm(t)1853 601 y Fl(\003)1891 631 y Fp(\))30 b Fq(or)g Fm(top)p Fp(\()p Fm(s)2243 601 y Fl(\003)2281 631 y Fp(\))24 b(=)e Fm(top)p Fp(\()p Fm(t)2598 601 y Fl(\003)2637 631 y Fp(\))p Fq(.)565 784 y Fp(Since)j(the)g(other)g(condition)g(is)g(also)f (ful\014lled)i(b)n(y)f(the)g(noncop)n(ying)f(rewrite)g(relation,)440 884 y(it)j(is)f(an)g(immediate)g(consequence)g(of)g(Theorem)f(3.4)h (that)g(termination)g(is)g(mo)r(dular)g(for)440 983 y(noncop)n(ying)g (and)i(graph)e(rewriting.)440 1136 y Fg(Lemma)k(3.6)40 b Fq(If)30 b Fm(s)1068 1106 y Fl(\003)1136 1136 y Fn(\))1219 1106 y Fk(nc)1219 1159 y Fl(R)1324 1136 y Fm(t)1354 1106 y Fl(\003)1421 1136 y Fq(is)h(non-destructive,)f(then)f Fm(]s)2376 1106 y Fl(\003)2438 1136 y Fn(\025)2503 1106 y Fk(mult)2674 1136 y Fm(]t)2736 1106 y Fl(\003)2774 1136 y Fq(.)440 1312 y(Pr)l(o)l(of)89 b Fp(Supp)r(ose)44 b Fm(r)r(oot)p Fp(\()p Fm(s)1283 1282 y Fl(\003)1323 1312 y Fp(\))50 b Fn(2)g(F)1578 1276 y Fl(\003)1578 1332 y Fj(1)1660 1312 y Fp(and)43 b Fm(s)1876 1282 y Fl(\003)1964 1312 y Fp(=)49 b Fm(C)2143 1282 y Fl(\003)2182 1312 y Fp([)-14 b([)p Fm(s)2253 1282 y Fl(\003)2253 1332 y Fj(1)2291 1312 y Fm(;)14 b(:)g(:)g(:)g(;)g(s)2515 1282 y Fl(\003)2515 1332 y Fk(n)2560 1312 y Fp(])-14 b(])28 b Fn(\))2703 1282 y Fk(nc)2703 1335 y Fl(R)2805 1312 y Fm(t)2835 1282 y Fl(\003)2873 1312 y Fp(.)86 b(W)-7 b(e)44 b(ha)n(v)n(e)440 1411 y Fm(t)470 1381 y Fl(\003)561 1411 y Fp(=)698 1390 y(\026)679 1411 y Fm(C)744 1381 y Fl(\003)783 1411 y Fp([)-14 b([)p Fm(t)845 1381 y Fl(\003)845 1432 y Fj(1)883 1411 y Fm(;)14 b(:)g(:)g(:)g(;)g(t)1098 1381 y Fl(\003)1098 1432 y Fk(m)1161 1411 y Fp(])-14 b(],)50 b(where)c(either)f Fm(C)1843 1381 y Fl(\003)1909 1411 y Fn(\))1992 1381 y Fk(nc)1992 1434 y Fl(R)2114 1390 y Fp(\026)2095 1411 y Fm(C)2160 1381 y Fl(\003)2244 1411 y Fp(or)g Fm(C)2429 1381 y Fl(\003)2521 1411 y Fp(=)2657 1390 y(\026)2639 1411 y Fm(C)2704 1381 y Fl(\003)2788 1411 y Fp(and)g(for)h(ev)n(ery)440 1511 y Fm(k)26 b Fn(2)d(f)p Fp(1)p Fm(;)14 b(:)g(:)g(:)f(;)h(m)p Fn(g)p Fp(,)21 b(there)e(is)h(a)f Fm(j)1389 1523 y Fk(k)1453 1511 y Fn(2)k(f)p Fp(1)p Fm(;)14 b(:)g(:)g(:)f(;)h(n)p Fn(g)19 b Fp(suc)n(h)g(that)h(either)g Fm(s)2528 1481 y Fl(\003)2528 1533 y Fk(j)2555 1542 y Fc(k)2618 1511 y Fp(=)j Fm(t)2736 1481 y Fl(\003)2736 1535 y Fk(k)2797 1511 y Fp(or)18 b Fm(s)2929 1481 y Fl(\003)2929 1533 y Fk(j)2956 1542 y Fc(k)3025 1511 y Fn(\))3108 1481 y Fk(nc)3108 1534 y Fl(R)3210 1511 y Fm(t)3240 1481 y Fl(\003)3240 1535 y Fk(k)3281 1511 y Fp(.)440 1623 y(Hence)28 b Fm(]s)758 1593 y Fl(\003)819 1623 y Fn(\025)884 1593 y Fk(mult)1056 1623 y Fm(]t)1118 1593 y Fl(\003)1184 1623 y Fp(follo)n(ws)e(from)i Fm(r)r(ank)s Fp(\()p Fm(s)1903 1593 y Fl(\003)1903 1644 y Fk(j)1930 1653 y Fc(k)1971 1623 y Fp(\))23 b Fn(\025)g Fm(r)r(ank)s Fp(\()p Fm(t)2355 1593 y Fl(\003)2355 1646 y Fk(k)2396 1623 y Fp(\).)789 b Ff(\003)565 1798 y Fp(Since)62 b Fn(\))899 1810 y Fl(R)1023 1798 y Fn(\022)h(\))1234 1768 y Fk(nc)1234 1821 y Fl(R)1337 1798 y Fp(,)36 b(the)g(ab)r(o)n(v)n (e)d(lemma)i(remains)f(v)-5 b(alid)35 b(if)h(w)n(e)e(replace)62 b Fn(\))3202 1768 y Fk(nc)3202 1821 y Fl(R)440 1898 y Fp(with)56 b Fn(\))740 1910 y Fl(R)829 1898 y Fp(.)37 b(The)27 b(same)g(is)h(true)f(for)g(the)h(next)g(corollary)-7 b(.)440 2051 y Fg(Corollary)32 b(3.7)40 b Fq(T)-6 b(ermination)38 b(is)f(mo)l(dular)g(for)h(nonc)l(opying)g(r)l(ewriting,)h(i.e.,)71 b Fn(\))3200 2021 y Fk(nc)3200 2074 y Fl(R)440 2151 y Fq(is)30 b(terminating)g(if)h(and)f(only)g(if)h(b)l(oth)60 b Fn(\))1772 2120 y Fk(nc)1772 2173 y Fl(R)1829 2181 y Fb(1)1925 2151 y Fq(and)g Fn(\))2199 2120 y Fk(nc)2199 2173 y Fl(R)2256 2181 y Fb(2)2352 2151 y Fq(ar)l(e)30 b(terminating.)565 2304 y Fp(Ho)n(w)n(ev)n(er,)40 b(if)f(a)g(\(mark)n (ed\))f(term)h(rewriting)f(step)h Fm(s)2279 2273 y Fl(\003)2359 2304 y Fn(!)2442 2316 y Fl(R)2546 2304 y Fm(t)2576 2273 y Fl(\003)2653 2304 y Fp(is)g(not)g(destructiv)n(e)440 2403 y(at)d(lev)n(el)f(2,)j(then)e Fm(]s)1118 2373 y Fl(\003)1194 2403 y Fn(\025)1259 2415 y Fk(mult)1444 2403 y Fm(]t)1506 2373 y Fl(\003)1580 2403 y Fp(follo)n(ws)f(only)h(if) g(the)g(applied)g(rewrite)f(rule)h(is)g(non-)440 2503 y(duplicating.)69 b(It)39 b(is)g(not)f(surprising)f(that)i(T)-7 b(o)n(y)n(ama's)36 b(example)i(constitutes)h(a)f(coun-)440 2602 y(terexample)27 b(for)g(duplicating)h(systems.)36 b(In)28 b(the)g(rewrite)e(step)498 2755 y Fm(s)537 2721 y Fl(\003)598 2755 y Fp(=)c Fm(F)750 2721 y Fj(0)787 2755 y Fp(\(0)861 2721 y Fj(1)898 2755 y Fm(;)14 b Fp(1)977 2721 y Fj(2)1014 2755 y Fm(;)g(g)1094 2721 y Fj(3)1131 2755 y Fp(\(0)1205 2721 y Fj(4)1242 2755 y Fm(;)g Fp(1)1321 2721 y Fj(5)1358 2755 y Fp(\)\))23 b Fn(!)1528 2767 y Fl(R)1612 2755 y Fm(F)1677 2721 y Fj(6)1715 2755 y Fp(\()p Fm(g)1790 2721 y Fj(7)1827 2755 y Fp(\(0)1901 2721 y Fj(8)1938 2755 y Fm(;)14 b Fp(1)2017 2721 y Fj(9)2053 2755 y Fp(\))p Fm(;)g(g)2165 2721 y Fj(10)2236 2755 y Fp(\(0)2310 2721 y Fj(11)2380 2755 y Fm(;)g Fp(1)2459 2721 y Fj(12)2528 2755 y Fp(\))p Fm(;)g(g)2640 2721 y Fj(13)2710 2755 y Fp(\(0)2784 2721 y Fj(14)2855 2755 y Fm(;)g Fp(1)2934 2721 y Fj(15)3003 2755 y Fp(\)\))24 b(=)f Fm(t)3209 2721 y Fl(\003)440 2908 y Fp(w)n(e)k(ha)n(v)n(e)g Fm(]s)825 2878 y Fl(\003)886 2908 y Fp(=)c([2])k(and)g Fm(]t)1312 2878 y Fl(\003)1374 2908 y Fp(=)c([2)p Fm(;)14 b Fp(2)p Fm(;)g Fp(2].)440 3061 y Fg(Lemma)30 b(3.8)40 b Fq(If)i Fm(s)1080 3031 y Fl(\003)1163 3061 y Fn(!)1246 3073 y Fl(R)1351 3061 y Fm(t)1381 3031 y Fl(\003)1461 3061 y Fq(is)g(non-destructive)f(and)h(the)g(applie)l(d)i(r)l(ewrite)d (rule)h(is)440 3161 y(non-duplic)l(ating,)31 b(then)f Fm(]s)1307 3131 y Fl(\003)1368 3161 y Fn(\025)1433 3131 y Fk(mult)1604 3161 y Fm(]t)1666 3131 y Fl(\003)1705 3161 y Fq(.)440 3337 y(Pr)l(o)l(of)80 b Fp(Supp)r(ose)38 b Fm(r)r(oot)p Fp(\()p Fm(s)1268 3306 y Fl(\003)1308 3337 y Fp(\))k Fn(2)g(F)1547 3300 y Fl(\003)1547 3357 y Fj(1)1624 3337 y Fp(and)c Fm(s)1835 3306 y Fl(\003)1915 3337 y Fp(=)j Fm(C)2086 3306 y Fl(\003)2124 3337 y Fp([)-14 b([)p Fm(s)2195 3306 y Fl(\003)2195 3357 y Fj(1)2233 3337 y Fm(;)14 b(:)g(:)g(:)g(;)g(s)2457 3306 y Fl(\003)2457 3357 y Fk(n)2502 3337 y Fp(])-14 b(])42 b Fn(!)2659 3349 y Fl(R)2762 3337 y Fm(t)2792 3306 y Fl(\003)2830 3337 y Fp(.)70 b(Either)38 b(the)440 3436 y(reduction)27 b(step)g(tak)n(es)f (place)g(in)h(the)h(outer)e(con)n(text)g(\(so)h Fm(C)2355 3406 y Fl(\003)2416 3436 y Fn(!)2499 3448 y Fl(R)2602 3415 y Fp(\026)2584 3436 y Fm(C)2649 3406 y Fl(\003)2687 3436 y Fp(\))g(or)f(in)i(one)e(of)h(the)440 3536 y(principal)h (subterms.)41 b(In)29 b(the)g(former)f(case,)h(w)n(e)f(ha)n(v)n(e)g Fm(t)2243 3506 y Fl(\003)2306 3536 y Fp(=)2415 3515 y(\026)2396 3536 y Fm(C)2461 3506 y Fl(\003)2500 3536 y Fp([)-14 b([)p Fm(t)2562 3506 y Fl(\003)2562 3556 y Fj(1)2600 3536 y Fm(;)14 b(:)g(:)g(:)g(;)g(t)2815 3506 y Fl(\003)2815 3556 y Fk(m)2878 3536 y Fp(])-14 b(].)41 b(Fix)29 b(some)440 3635 y Fm(k)h Fn(2)e(f)p Fp(1)p Fm(;)14 b(:)g(:)g(:)e(;)i(m)p Fn(g)p Fp(.)44 b(There)30 b(is)g(at)g(least)g(one)g(index)g Fm(j)2090 3647 y Fk(k)2158 3635 y Fn(2)e(f)p Fp(1)p Fm(;)14 b(:)g(:)g(:)f(;)h(n)p Fn(g)29 b Fp(suc)n(h)h(that)g Fm(e)p Fp(\()p Fm(s)3112 3605 y Fl(\003)3112 3657 y Fk(j)3139 3666 y Fc(k)3180 3635 y Fp(\))e(=)440 3735 y Fm(e)p Fp(\()p Fm(t)541 3705 y Fl(\003)541 3759 y Fk(k)582 3735 y Fp(\).)69 b(Moreo)n(v)n(er,)38 b(the)g(n)n(um)n(b)r(er)g(of)g(terms)g(in)g Fm(S)5 b Fp(\()p Fm(t)2145 3705 y Fl(\003)2183 3735 y Fp(\))41 b(=)f Fn(f)p Fm(t)2433 3705 y Fl(\003)2433 3756 y Fj(1)2471 3735 y Fm(;)14 b(:)g(:)g(:)g(;)g(t)2686 3705 y Fl(\003)2686 3756 y Fk(m)2748 3735 y Fn(g)38 b Fp(with)h Fm(e)p Fp(\()p Fm(t)3129 3705 y Fl(\003)3129 3757 y Fk(i)3167 3735 y Fp(\))i(=)440 3835 y Fm(e)p Fp(\()p Fm(t)541 3805 y Fl(\003)541 3858 y Fk(k)582 3835 y Fp(\))33 b(is)f(smaller)g(or)f (equal)i(to)f(the)h(n)n(um)n(b)r(er)f(of)h(terms)f(in)h Fm(S)5 b Fp(\()p Fm(s)2484 3805 y Fl(\003)2522 3835 y Fp(\))32 b(=)e Fn(f)p Fm(s)2762 3805 y Fl(\003)2762 3855 y Fj(1)2800 3835 y Fm(;)14 b(:)g(:)g(:)g(;)g(s)3024 3805 y Fl(\003)3024 3855 y Fk(n)3069 3835 y Fn(g)32 b Fp(with)440 3934 y Fm(e)p Fp(\()p Fm(s)550 3904 y Fl(\003)550 3956 y Fk(j)588 3934 y Fp(\))24 b(=)f Fm(e)p Fp(\()p Fm(t)833 3904 y Fl(\003)833 3958 y Fk(k)874 3934 y Fp(\))29 b(b)r(ecause)e(the)i (rule)e(applied)h(in)h(the)f(reduction)g(step)g(is)g(non-duplicating.) 440 4034 y(Therefore,)576 4182 y Fm(]s)647 4152 y Fl(\003)708 4182 y Fp(=)83 b([)p Fm(r)r(ank)s Fp(\()p Fm(s)1129 4152 y Fl(\003)1129 4203 y Fj(1)1168 4182 y Fp(\))p Fm(;)14 b(:)g(:)g(:)f(;)h(r)r(ank)s Fp(\()p Fm(s)1634 4152 y Fl(\003)1634 4203 y Fk(n)1680 4182 y Fp(\)])23 b(=)g([)p Fm(r)r(ank)s Fp(\()p Fm(e)p Fp(\()p Fm(s)2190 4152 y Fl(\003)2190 4203 y Fj(1)2229 4182 y Fp(\)\))p Fm(;)14 b(:)g(:)g(:)g(;)g(r)r(ank)s Fp(\()p Fm(e)p Fp(\()p Fm(s)2799 4152 y Fl(\003)2799 4203 y Fk(n)2845 4182 y Fp(\)\)])23 b Fn(\025)3020 4152 y Fk(mult)856 4282 y Fp([)p Fm(r)r(ank)s Fp(\()p Fm(e)p Fp(\()p Fm(t)1191 4252 y Fl(\003)1191 4303 y Fj(1)1230 4282 y Fp(\)\))p Fm(;)14 b(:)g(:)g(:)g(;)g(r)r(ank)s Fp(\()p Fm(e)p Fp(\()p Fm(t)1791 4252 y Fl(\003)1791 4302 y Fk(m)1854 4282 y Fp(\)\)])24 b(=)f([)p Fm(r)r(ank)s Fp(\()p Fm(t)2317 4252 y Fl(\003)2317 4303 y Fj(1)2355 4282 y Fp(\))p Fm(;)14 b(:)g(:)g(:)g(;)g(r)r(ank)s Fp(\()p Fm(t)2813 4252 y Fl(\003)2813 4302 y Fk(m)2877 4282 y Fp(\)])23 b(=)g Fm(]t)3105 4252 y Fl(\003)3143 4282 y Fm(:)440 4431 y Fp(If)i(the)g(con)n(tracted)f(redex)g(is)h(a)f(subterm) h(of)g(one)f(of)h(the)h(principal)e(subterms)g(of)h Fm(s)3056 4401 y Fl(\003)3094 4431 y Fp(,)h(then)440 4531 y Fm(s)479 4501 y Fl(\003)479 4552 y Fk(j)543 4531 y Fn(!)626 4543 y Fl(R)714 4531 y Fm(t)744 4501 y Fl(\003)744 4552 y Fk(j)811 4531 y Fp(for)j(some)g(1)d Fn(\024)f Fm(j)31 b Fn(\024)26 b Fm(n)k Fp(and)f(hence)g Fm(t)1969 4501 y Fl(\003)2034 4531 y Fp(=)c Fm(C)2189 4501 y Fl(\003)2228 4531 y Fp([)-14 b([)p Fm(s)2299 4501 y Fl(\003)2299 4551 y Fj(1)2337 4531 y Fm(;)14 b(:)g(:)g(:)g(;)g(s)2561 4501 y Fl(\003)2561 4552 y Fk(j)s Fl(\000)p Fj(1)2680 4531 y Fm(;)g(t)2747 4501 y Fl(\003)2747 4552 y Fk(j)2785 4531 y Fm(;)g(s)2861 4501 y Fl(\003)2861 4552 y Fk(j)s Fj(+1)2980 4531 y Fm(;)g(:)g(:)g(:)g(;)g(s)3204 4501 y Fl(\003)3204 4551 y Fk(n)3249 4531 y Fp(])-14 b(].)440 4630 y(In)28 b(this)g(case)507 4762 y Fm(]s)578 4732 y Fl(\003)640 4762 y Fp(=)82 b([)p Fm(r)r(ank)s Fp(\()p Fm(s)1060 4732 y Fl(\003)1060 4782 y Fj(1)1099 4762 y Fp(\))p Fm(;)14 b(:)g(:)g(:)g(;)g(r)r(ank)s Fp(\()p Fm(s)1566 4732 y Fl(\003)1566 4783 y Fk(j)s Fl(\000)p Fj(1)1686 4762 y Fp(\))p Fm(;)g(r)r(ank)s Fp(\()p Fm(s)2005 4732 y Fl(\003)2005 4783 y Fk(j)2044 4762 y Fp(\))p Fm(;)g(r)r(ank)s Fp(\()p Fm(s)2363 4732 y Fl(\003)2363 4783 y Fk(j)s Fj(+1)2483 4762 y Fp(\))p Fm(;)g(:)g(:)g(:)g(;)g(r)r(ank)s Fp(\()p Fm(s)2950 4732 y Fl(\003)2950 4782 y Fk(n)2996 4762 y Fp(\)])491 4865 y Fn(\025)556 4835 y Fk(mult)787 4865 y Fp([)p Fm(r)r(ank)s Fp(\()p Fm(s)1060 4835 y Fl(\003)1060 4886 y Fj(1)1099 4865 y Fp(\))p Fm(;)g(:)g(:)g(:)g(;)g(r)r(ank)s Fp(\()p Fm(s)1566 4835 y Fl(\003)1566 4887 y Fk(j)s Fl(\000)p Fj(1)1686 4865 y Fp(\))p Fm(;)g(r)r(ank)s Fp(\()p Fm(t)1996 4835 y Fl(\003)1996 4887 y Fk(j)2035 4865 y Fp(\))p Fm(;)g(r)r(ank)s Fp(\()p Fm(s)2354 4835 y Fl(\003)2354 4887 y Fk(j)s Fj(+1)2474 4865 y Fp(\))p Fm(;)g(:)g(:)g(:)g(;)g(r)r(ank)s Fp(\()p Fm(s)2941 4835 y Fl(\003)2941 4886 y Fk(n)2987 4865 y Fp(\)])23 b(=)g Fm(]t)3215 4835 y Fl(\003)440 5022 y Fp(b)r(ecause)k Fm(r)r(ank)s Fp(\()p Fm(s)997 4992 y Fl(\003)997 5044 y Fk(j)1036 5022 y Fp(\))c Fn(\025)g Fm(r)r(ank)s Fp(\()p Fm(t)1420 4992 y Fl(\003)1420 5044 y Fk(j)1459 5022 y Fp(\).)1726 b Ff(\003)440 5198 y Fg(Corollary)32 b(3.9)40 b Fq(T)-6 b(ermination)50 b(is)g(a)f(mo)l(dular)h(pr)l(op)l (erty)g(of)h(non-duplic)l(ating)f(term)440 5297 y(r)l(ewriting)36 b(systems,)h(i.e.,)h Fn(!)1395 5309 y Fl(R)1492 5297 y Fq(is)d(terminating)h(if)g(and)g(only)f(if)i(b)l(oth)e Fn(!)2832 5309 y Fl(R)2889 5317 y Fb(1)2961 5297 y Fq(and)h Fn(!)3211 5309 y Fl(R)3268 5317 y Fb(2)440 5397 y Fq(ar)l(e)30 b(terminating.)1851 5662 y Fp(7)p eop %%Page: 8 8 8 7 bop 440 531 a Fo(4)135 b(Concluding)45 b(Remarks)440 713 y Fp(W)-7 b(e)25 b(ha)n(v)n(e)f(seen)g(that)h(in)h(plain)e(graph)g (rewriting)g Fm(eq)2087 683 y Fj(0)2124 713 y Fp(\()p Fm(eq)2235 683 y Fj(1)2272 713 y Fp(\(0)2346 683 y Fj(2)2383 713 y Fm(;)14 b Fp(0)2462 683 y Fj(3)2499 713 y Fp(\))p Fm(;)g(eq)2647 683 y Fj(1)2684 713 y Fp(\(0)2758 683 y Fj(2)2795 713 y Fm(;)g Fp(0)2874 683 y Fj(3)2910 713 y Fp(\)\))26 b(do)r(es)e(not)440 813 y(reduce)k(to)g Fm(eq)885 783 y Fj(0)922 813 y Fp(\()p Fm(tr)r(ue)1110 783 y Fj(6)1148 813 y Fm(;)14 b(tr)r(ue)1341 783 y Fj(6)1378 813 y Fp(\))29 b(b)r(ecause)f(0)1789 783 y Fj(2)1854 813 y Fp(and)g(0)2058 783 y Fj(3)2124 813 y Fp(are)f(not)i(shared)e (and)h(th)n(us)h(the)g(rule)440 912 y Fm(eq)519 882 y Fj(1)556 912 y Fp(\()p Fm(x)635 882 y Fj(4)673 912 y Fm(;)14 b(x)757 882 y Fj(4)795 912 y Fp(\))23 b Fn(!)g Fm(tr)r(ue)1112 882 y Fj(6)1174 912 y Fp(cannot)i(b)r(e)g(applied.)36 b(In)25 b(order)e(to)i(cop)r(e)g(with)g(this)h(phenomenon,)440 1012 y(one)37 b(can)g(use)g(in)n(termediate)g(prop)r(er)g(collapsing)f (steps)h Fn(\037)p Fp(;)42 b(see)37 b([Plu93)n(,)h(Plu98)o(].)66 b(F)-7 b(or)440 1112 y(example,)27 b(after)h(the)f(collapsing)g(step) 850 1280 y Fm(eq)929 1246 y Fj(0)965 1280 y Fp(\()p Fm(eq)1076 1246 y Fj(1)1114 1280 y Fp(\(0)1188 1246 y Fj(2)1225 1280 y Fm(;)14 b Fp(0)1304 1246 y Fj(3)1340 1280 y Fp(\))p Fm(;)g(eq)1488 1246 y Fj(1)1526 1280 y Fp(\(0)1600 1246 y Fj(2)1637 1280 y Fm(;)g Fp(0)1716 1246 y Fj(3)1752 1280 y Fp(\)\))24 b Fn(\037)e Fm(eq)2006 1246 y Fj(0)2043 1280 y Fp(\()p Fm(eq)2154 1246 y Fj(1)2192 1280 y Fp(\(0)2266 1246 y Fj(3)2303 1280 y Fm(;)14 b Fp(0)2382 1246 y Fj(3)2418 1280 y Fp(\))p Fm(;)g(eq)2566 1246 y Fj(1)2603 1280 y Fp(\(0)2677 1246 y Fj(3)2715 1280 y Fm(;)g Fp(0)2794 1246 y Fj(3)2830 1280 y Fp(\)\))440 1448 y(the)28 b(rule)f Fm(eq)828 1418 y Fj(1)865 1448 y Fp(\()p Fm(x)944 1418 y Fj(4)982 1448 y Fm(;)14 b(x)1066 1418 y Fj(4)1104 1448 y Fp(\))23 b Fn(!)g Fm(tr)r(ue)1421 1418 y Fj(6)1486 1448 y Fp(is)28 b(applicable,)f(so)g(that)975 1616 y Fm(eq)1054 1582 y Fj(0)1091 1616 y Fp(\()p Fm(eq)1202 1582 y Fj(1)1240 1616 y Fp(\(0)1314 1582 y Fj(3)1351 1616 y Fm(;)14 b Fp(0)1430 1582 y Fj(3)1466 1616 y Fp(\))p Fm(;)g(eq)1614 1582 y Fj(1)1651 1616 y Fp(\(0)1725 1582 y Fj(3)1762 1616 y Fm(;)g Fp(0)1841 1582 y Fj(3)1878 1616 y Fp(\)\))28 b Fn(\))2053 1628 y Fl(R)2142 1616 y Fm(eq)2221 1582 y Fj(0)2258 1616 y Fp(\()p Fm(tr)r(ue)2446 1582 y Fj(6)2484 1616 y Fm(;)14 b(tr)r(ue)2677 1582 y Fj(6)2714 1616 y Fp(\))p Fm(:)440 1784 y Fp(T)-7 b(ermination)27 b(of)h(graph)f(rewriting)g(is)h(also)f(mo)r(dular)g(in)h(the)h (presence)e(of)h(in)n(termediate)440 1884 y(collapsing)33 b(steps.)55 b(T)-7 b(o)34 b(b)r(e)g(precise,)h(termination)f(of)f(the)i (relation)e Fn(\))2744 1854 y Fk(coll)2744 1907 y Fl(R)2853 1884 y Fp(=)61 b Fn(\))3062 1896 y Fl(R)3151 1884 y Fn([)34 b(\037)440 1984 y Fp(is)29 b(also)e(mo)r(dular)i(for)f(disjoin)n(t)h (TRSs.)40 b(This)29 b(follo)n(ws)f(from)g(Theorem)g(3.4)g(and)h(the)g (fact)440 2083 y(that)f Fm(s)659 2053 y Fl(\003)720 2083 y Fn(\037)23 b Fm(t)838 2053 y Fl(\003)903 2083 y Fp(implies)28 b Fm(]s)1256 2053 y Fl(\003)1318 2083 y Fn(\025)1383 2095 y Fk(mult)1554 2083 y Fm(]t)1616 2053 y Fl(\003)1682 2083 y Fp(and)g Fm(top)p Fp(\()p Fm(s)2027 2053 y Fl(\003)2065 2083 y Fp(\))23 b Fn(\027)g Fm(top)p Fp(\()p Fm(t)2382 2053 y Fl(\003)2420 2083 y Fp(\).)440 2282 y Fg(Ac)m(kno)m(wledgemen)m (ts:)42 b Fp(T)-7 b(obias)30 b(Nipk)n(o)n(w)h(suggested)f(to)g(study)i (this)f(uniform)g(frame-)440 2382 y(w)n(ork)38 b(and)g(I)h(w)n(ould)g (lik)n(e)f(to)h(thank)g(him.)71 b(F)-7 b(urthermore,)41 b(I)e(thank)g(the)g(anon)n(ymous)440 2482 y(review)n(ers)26 b(for)h(their)g(commen)n(ts)h(whic)n(h)f(help)r(ed)h(to)g(impro)n(v)n (e)e(the)i(pap)r(er.)440 2754 y Fo(References)440 2936 y Fp([AK96])149 b(Z.)40 b(M.)g(Ariola)e(and)i(J.)f(W.)h(Klop.)72 b(Equational)38 b(term)i(graph)e(rewriting.)846 3035 y Fq(F)-6 b(undamentae)30 b(Informatic)l(ae)p Fp(,)f(26:207{240,)24 b(1996.)440 3195 y([AKP99])92 b(Z.)25 b(M.)g(Ariola,)g(J.)g(W.)g(Klop,) g(and)g(D.)h(Plump.)32 b(Bisimilarit)n(y)24 b(in)i(term)e(graph)846 3295 y(rewriting.)36 b Fq(Information)31 b(and)f(Computation)p Fp(,)f(1999.)35 b(T)-7 b(o)27 b(app)r(ear.)440 3455 y([BEG)644 3425 y Fj(+)699 3455 y Fp(87])40 b(H.P)-7 b(.)28 b(Barendregt,)f (M.C.J.D.)h(v)-5 b(an)28 b(Eek)n(elen,)g(J.R.W.)g(Glauert,)g(J.R.)g (Ken-)846 3555 y(na)n(w)n(a)n(y)-7 b(,)29 b(M.J.)g(Plasmeijer,)g(and)h (M.R.)g(Sleep.)43 b(T)-7 b(erm)29 b(graph)f(rewriting.)42 b(In)846 3655 y Fq(Pr)l(o)l(c.)c(Par)l(al)t(lel)h(A)n(r)l(chite)l(ctur) l(es)d(and)h(L)l(anguages)h(Eur)l(op)l(e)p Fp(,)g(v)n(olume)c(259)g(of) 846 3754 y Fq(L)l(e)l(ctur)l(e)29 b(Notes)h(in)f(Computer)i(Scienc)l(e) p Fp(,)d(pages)e(141{158,)e(1987.)440 3914 y([BN98])155 b(F.)23 b(Baader)d(and)i(T.)g(Nipk)n(o)n(w.)27 b Fq(T)-6 b(erm)25 b(R)l(ewriting)f(and)h(A)n(l)t(l)g(That)p Fp(.)k(Cam)n(bridge) 846 4014 y(Univ)n(ersit)n(y)e(Press,)f(1998.)440 4174 y([DM79])137 b(N.)38 b(Dersho)n(witz)e(and)h(Z.)g(Manna.)65 b(Pro)n(ving)35 b(termination)h(with)i(m)n(ultiset)846 4274 y(orderings.)d Fq(Communic)l(ations)c(of)f(the)g(A)n(CM)p Fp(,)e(22\(8\):465{476,)c(1979.)440 4434 y([Gra96])136 b(B.)30 b(Gramlic)n(h.)42 b Fq(T)-6 b(ermination)33 b(and)f (Con\015uenc)l(e)g(Pr)l(op)l(erties)g(of)h(Structur)l(e)l(d)846 4534 y(R)l(ewrite)d(Systems)p Fp(.)36 b(PhD)28 b(thesis,)g(Univ)n (ersit\177)-42 b(at)27 b(Kaiserslautern,)e(1996.)440 4694 y([KKSV94])40 b(J.R.)g(Kenna)n(w)n(a)n(y)-7 b(,)42 b(J.W.)e(Klop,)j(M.R.)d(Sleep,)k(and)c(F.-J.)g(de)g(V)-7 b(ries.)75 b(On)846 4794 y(the)27 b(adequacy)d(of)i(term)g(graph)f (rewriting)g(for)h(sim)n(ulating)f(term)h(rewriting.)846 4893 y Fq(T)-6 b(r)l(ans.)30 b(on)g(Pr)l(o)l(gr)l(amming)h(L)l (anguages)f(and)g(Systems)p Fp(,)d(16:493{523,)d(1994.)440 5054 y([K)n(O95])148 b(M.)25 b(Kurihara)e(and)h(A.)h(Oh)n(uc)n(hi.)31 b(Mo)r(dularit)n(y)24 b(in)h(noncop)n(ying)e(term)h(rewrit-)846 5153 y(ing.)37 b Fq(The)l(or)l(etic)l(al)31 b(Computer)g(Scienc)l(e)p Fp(,)d(152:139{169,)23 b(1995.)440 5313 y([KR98])150 b(M.R.K.)41 b(Krishna)f(Rao.)77 b(Mo)r(dular)40 b(asp)r(ects)h(of)g (term)g(graph)f(rewriting.)846 5413 y Fq(The)l(or)l(etic)l(al)32 b(Computer)e(Scienc)l(e)p Fp(,)e(208:59{86,)c(1998.)1851 5662 y(8)p eop %%Page: 9 9 9 8 bop 440 531 a Fp([Mid90])131 b(A.)20 b(Middeldorp.)k Fq(Mo)l(dular)g(Pr)l(op)l(erties)f(of)h(T)-6 b(erm)22 b(R)l(ewriting)h(Systems)p Fp(.)g(PhD)846 631 y(thesis,)28 b(V)-7 b(rije)28 b(Univ)n(ersiteit)f(te)h(Amsterdam,)f(1990.)440 797 y([Ohl93])142 b(E.)29 b(Ohlebusc)n(h.)40 b(A)30 b(simple)f(pro)r (of)f(of)h(su\016cien)n(t)g(conditions)g(for)f(the)i(termi-)846 897 y(nation)21 b(of)g(the)g(disjoin)n(t)g(union)g(of)g(term)g (rewriting)f(systems.)25 b Fq(Bul)t(letin)g(of)f(the)846 996 y(Eur)l(op)l(e)l(an)g(Asso)l(ciation)g(for)g(The)l(or)l(etic)l(al)h (Computer)f(Scienc)l(e)p Fp(,)f(49:178{183,)846 1096 y(1993.)440 1262 y([Ohl94])142 b(E.)35 b(Ohlebusc)n(h.)60 b Fq(Mo)l(dular)38 b(Pr)l(op)l(erties)g(of)g(Comp)l(osable)h(T)-6 b(erm)37 b(R)l(ewriting)846 1362 y(Systems)p Fp(.)g(PhD)27 b(thesis,)h(Univ)n(ersit\177)-42 b(at)27 b(Bielefeld,)h(1994.)440 1528 y([Ohl97])142 b(E.)30 b(Ohlebusc)n(h.)42 b(Conditional)29 b(term)h(graph)f(rewriting.)42 b(In)30 b Fq(Pr)l(o)l(c)l(e)l(e)l(dings) i(of)846 1627 y(the)k(6th)h(International)f(Confer)l(enc)l(e)h(on)f(A)n (lgebr)l(aic)i(and)e(L)l(o)l(gic)h(Pr)l(o)l(gr)l(am-)846 1727 y(ming)p Fp(,)45 b(v)n(olume)c(1298)e(of)i Fq(L)l(e)l(ctur)l(e)g (Notes)h(in)h(Computer)f(Scienc)l(e)p Fp(,)j(pages)846 1826 y(144{158,)25 b(1997.)440 1993 y([Ohl98])142 b(E.)38 b(Ohlebusc)n(h.)68 b(Mo)r(dularit)n(y)37 b(of)h(termination)g(for)f (disjoin)n(t)h(term)g(graph)846 2092 y(rewrite)28 b(systems:)40 b(A)29 b(simple)g(pro)r(of.)41 b Fq(Bul)t(letin)31 b(of)h(the)f(Eur)l (op)l(e)l(an)h(Asso)l(cia-)846 2192 y(tion)e(for)h(The)l(or)l(etic)l (al)g(Computer)f(Scienc)l(e)p Fp(,)e(66:171{177,)c(1998.)440 2358 y([Plu91])150 b(D.)25 b(Plump.)30 b(Implemen)n(ting)24 b(term)g(rewriting)e(b)n(y)i(graph)e(reduction:)35 b(T)-7 b(ermi-)846 2457 y(nation)25 b(of)g(com)n(bined)f(systems.)32 b(In)25 b Fq(Pr)l(o)l(c)l(e)l(e)l(dings)k(of)f(the)f(2nd)h (International)846 2557 y(Workshop)g(on)e(Conditional)j(and)d(T)-6 b(yp)l(e)l(d)27 b(R)l(ewriting)g(Systems)p Fp(,)d(v)n(olume)f(516)846 2657 y(of)28 b Fq(L)l(e)l(ctur)l(e)h(Notes)g(in)h(Computer)g(Scienc)l (e)p Fp(,)e(pages)f(307{317,)d(1991.)440 2823 y([Plu93])150 b(D.)29 b(Plump.)39 b(Collapsed)27 b(tree)h(rewriting:)37 b(Completeness,)28 b(con\015uence,)h(and)846 2922 y(mo)r(dularit)n(y)-7 b(.)66 b(In)38 b Fq(Pr)l(o)l(c)l(e)l(e)l(dings)i(of)g(the)f(3r)l(d)g (International)g(Workshop)i(on)846 3022 y(Conditional)c(T)-6 b(erm)34 b(R)l(ewriting)g(Systems)p Fp(,)f(v)n(olume)f(656)f(of)h Fq(L)l(e)l(ctur)l(e)h(Notes)846 3122 y(in)d(Computer)g(Scienc)l(e)p Fp(,)e(pages)f(97{112,)e(1993.)440 3288 y([Plu98])150 b(D.)41 b(Plump.)74 b(T)-7 b(erm)40 b(graph)f(rewriting.)73 b(T)-7 b(ec)n(hnical)39 b(Rep)r(ort)h(CSI-R9822,)846 3387 y(Computing)30 b(Science)g(Institute)h(Nijmegen,)g(1998.)42 b(T)-7 b(o)30 b(app)r(ear)f(in:)42 b(Hand-)846 3487 y(b)r(o)r(ok)19 b(of)h(Graph)f(Grammars)f(and)h(Computing)h(b)n(y)f(Graph)g(T)-7 b(ransformation,)846 3587 y(v)n(olume)27 b(2,)g(W)-7 b(orld)28 b(Scien)n(ti\014c.)440 3753 y([Rus87])136 b(M.)25 b(Rusino)n(witc)n(h.)31 b(On)24 b(termination)g(of)h(the)g(direct)f (sum)h(of)f(term)g(rewriting)846 3852 y(systems.)37 b Fq(Information)30 b(Pr)l(o)l(c)l(essing)h(L)l(etters)p Fp(,)c(26:65{70,)d(1987.)440 4018 y([T)-7 b(o)n(y87])139 b(Y.)32 b(T)-7 b(o)n(y)n(ama.)48 b(Coun)n(terexamples)30 b(to)i(termination)f(for)h(the)g(direct)f(sum)h(of)846 4118 y(term)24 b(rewriting)f(systems.)30 b Fq(Information)d(Pr)l(o)l(c) l(essing)g(L)l(etters)p Fp(,)d(25:141{143,)846 4218 y(1987.)1851 5662 y(9)p eop %%Trailer end userdict /end-hook known{end-hook}if %%EOF