%!PS-Adobe-2.0 %%Creator: dvips 5.47 Copyright 1986-91 Radical Eye Software %%Title: paper.dvi %%Pages: 6 1 %%BoundingBox: 0 0 596 843 %%EndComments %%BeginProcSet: tex.pro /TeXDict 200 dict def TeXDict begin /N /def load def /B{bind def}N /S /exch load def /X{S N}B /TR /translate load N /isls false N /vsize 10 N /@rigin{ isls{[0 1 -1 0 0 0]concat}if 72 Resolution div 72 VResolution div neg scale Resolution VResolution vsize neg mul TR matrix currentmatrix dup dup 4 get round 4 exch put dup dup 5 get round 5 exch put setmatrix}N /@letter{/vsize 10 N}B /@landscape{/isls true N /vsize -1 N}B /@a4{/vsize 10.6929133858 N}B /@a3{ /vsize 15.5531 N}B /@ledger{/vsize 16 N}B /@legal{/vsize 13 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 add]{ch-image} imagemask restore}B /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}N /eop{clear SI restore showpage userdict /eop-hook known{eop-hook}if}N /@start{userdict /start-hook known{start-hook}if /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}N /p /show load 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 statusdict begin /product where{pop product dup length 7 ge{0 7 getinterval(Display)eq}{pop false}ifelse}{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 /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{clear SS restore}B end %%EndProcSet TeXDict begin 1000 300 300 @start /Fa 1 98 df<00200000700000700000F80000B80000 B800011C00011C00021E00020E00020E0004070007FF000803800803801803C01001C03801E0FC 07F815137F9218>97 D E /Fb 7 55 df<07F0001E3C003C1E00380E00780F00780F00780F00F8 0F80F80F80F80F80F80F80F80F80F80F80F80F80F80F80F80F80F80F80F80F80780F00780F0038 0E003C1E001E3C0007F00011187E9716>48 D<00C003C0FFC0FFC003C003C003C003C003C003C0 03C003C003C003C003C003C003C003C003C003C003C003C07FFE7FFE0F187D9716>I<0FF0003F FC00787E00FC1F00FC1F80FC0F80FC0F80780F80001F80001F00001E00003C0000780000700000 E0000180000301800601800C01801003803FFF007FFF00FFFF00FFFF0011187E9716>I<07F000 1FFC00383E007C3E007C1F007C1F007C1F00383F00003E00003C0000780007F000003C00001E00 001F00001F80781F80FC1F80FC1F80FC1F00F81F00703E003FFC000FF00011187E9716>I<0006 00000E00001E00003E00007E0000DE00019E00011E00031E00061E000C1E00181E00301E00601E 00C01E00FFFFE0FFFFE0001E00001E00001E00001E00001E0001FFE001FFE013187F9716>I<30 06003FFC003FFC003FF0003FE0003F800030000030000030000037F000381C00301E00000F0000 0F00000F80700F80F80F80F80F80F80F80F80F00601F00383E001FF80007E00011187E9716>I< 00F80007FE000F06001E0F003C1F003C1F00780E00780000F80000F9F000FA1C00FC0E00FC0F00 F80F80F80F80F80F80F80F80780F80780F80780F003C0F001E1E000FFC0003F00011187E9716> I E /Fc 46 123 df<000400180030006000C0008001800300030006000E000C001C0018001800 38003000300070007000600060006000E000E000E000C000C000C000C000C00060006000600020 003000100008000E267B9B10>40 D<004000600020003000100018001800180018001800180018 0018001800180018003800380030003000700070006000E000C000C001C0018003800300060006 000C00180010002000400080000D267F9B10>I<1838783808101020204080050B7D830C>44 DI<3078F06005047C830C>I<000800180030007001F00E7000E000 E000E000E001C001C001C001C0038003800380038007000700070007000F00FFF00D187C9714> 49 D<003E0000C3000101800201800481C00441C0088380048380070300000600000C0001F000 001800000C00000C00000E00000E00600E00E01C00E01C0080380040300020E0001F800012187D 9714>51 D<000300000380000700000700000700000E00000E00000E00001C00001C0000180000 300000300000600000C00000C600018E00030E00021C00041C00081C00101C007FB800807F8000 3800003800007000007000007000007000006000111F7F9714>I<003E0000C1000100800200C0 0600C00600C00E018007030007860003CC0001F00001F800067C000C3E00180E00300700600700 600700C00600C00600600C006018003070000FC00012187D9714>56 D<00002000006000006000 00E00001E00001E000027000027000047000087000087000107000107000207000207000407000 807000FFF00100380100380200380400380400380C00381C0038FF01FF181A7E991D>65 D<03FFF800700E00700600700700E00700E00700E00700E00701C00E01C01C01C03801C07003FF E003807003803803801C07001C07001C07001C07001C0E00380E00380E00700E00E01C03C0FFFF 00181A7D991B>I<000F8200706200C01603801E07000C0E000C1C000C18000C38000830000870 0000700000E00000E00000E00000E00000E00020E00020E00020E0004060004060008030010010 06000C180003E000171A7A991B>I<03FFFF00700700700300700100E00100E00100E00100E001 01C08001C08001C08001C18003FF000381000381000381000702000700040700040700080E0008 0E00180E00100E00301C00E0FFFFE0181A7D991A>69 D<03FF1FF8007003800070038000700380 00E0070000E0070000E0070000E0070001C00E0001C00E0001C00E0001C00E0003FFFC0003801C 0003801C0003801C00070038000700380007003800070038000E0070000E0070000E0070000E00 70001C00E000FFC7FE001D1A7D991D>72 D<01FF80003800003800003800007000007000007000 00700000E00000E00000E00000E00001C00001C00001C00001C000038000038000038000038000 0700000700000700000700000E0000FFE000111A7E990F>I<00FFC0000E00000E00000E00001C 00001C00001C00001C0000380000380000380000380000700000700000700000700000E00000E0 0000E00000E00061C000E1C000E180008380004700003C0000121A7C9914>I<03FF8000700000 700000700000E00000E00000E00000E00001C00001C00001C00001C00003800003800003800003 80000700000700100700100700200E00200E00600E00400E00C01C0380FFFF80141A7D9918>76 D<03F8001FC00078003C000078003C000078005C0000B800B80000B800B800009C013800009C01 3800011C027000011C027000011C047000011C087000021C08E000021C10E000021C10E000021C 20E000041C41C000041C41C000041C81C000041C81C000080F038000080F038000080E03800018 0C038000380C070000FF083FF000221A7D9922>I<03FFF800701C00700600700700E00700E007 00E00700E00701C00E01C00E01C01C01C03803807003FF80038000038000070000070000070000 0700000E00000E00000E00000E00001C0000FFC000181A7D991A>80 D<03FFF000701C00700E00 700700E00700E00700E00700E00701C00E01C01C01C03801C0E003FF800380C003806003807007 00700700700700700700700E00E00E00E00E00E10E00E21C0062FFC03C181A7D991C>82 D<003F1000609001807001007003002006002006002006002006000007000007C00003F80001FE 00007F00000F80000380000180000180200180200180600300600300600600700C00C8180087E0 00141A7D9916>I<3FFFFC381C0C201C04401C0440380480380480380480380400700000700000 700000700000E00000E00000E00000E00001C00001C00001C00001C00003800003800003800003 8000078000FFF800161A79991B>I86 D<03CC0E2E181C381C301C701CE038E038E038E038C072C072C07260F261 341E180F107C8F14>97 D<7E000E000E000E001C001C001C001C00380038003BC03C3078307018 70187018E038E038E038E038C070C060C0E060C063801E000D1A7C9912>I<01F006080C181838 301070006000E000E000E000E000E008E010602030C01F000D107C8F12>I<001F800003800003 80000380000700000700000700000700000E00000E0003CE000E2E00181C00381C00301C00701C 00E03800E03800E03800E03800C07200C07200C0720060F2006134001E1800111A7C9914>I<01 E006181C08380870087010FFE0E000E000E000E000E0086010602030C01F000D107C8F12>I<00 0700001980001B80003B0000300000300000700000700000700000700007FF0000E00000E00000 E00000E00000E00001C00001C00001C00001C00001C00003800003800003800003800003800007 0000070000070000660000E40000CC0000700000112181990C>I<00F300038B800607000E0700 0C07001C0700380E00380E00380E00380E00301C00301C00301C00183C0018780007B800003800 003800007000607000E0E000C1C0007F000011177E8F12>I<1F80000380000380000380000700 000700000700000700000E00000E00000E7C000F86001E07001E07001C07001C0700380E00380E 00380E00381C00701C80701C80703880703900E01900600E00111A7E9914>I<03070600000000 0000384C4E8E9C9C1C3838707272E2E4643808197C980C>I<1F80038003800380070007000700 07000E000E000E0E0E131C271C431C801F003C003F8039C038E070E270E270E270E4E064603810 1A7E9912>107 D<3F0707070E0E0E0E1C1C1C1C3838383870707070E4E4E4E46830081A7D990A> I<307C1E00598663009E0783809E0703809C0703809C070380380E0700380E0700380E0700380E 0E00701C0E40701C0E40701C1C40701C1C80E0380C80601807001A107C8F1F>I<307C00598600 9E07009E07009C07009C0700380E00380E00380E00381C00701C80701C80703880703900E01900 600E0011107C8F16>I<01F006180C0C180E300E700E600EE00EE00EE00CE01CE018E030606030 C01F000F107C8F14>I<030F000590C009E0C009C06009C06009C0600380E00380E00380E00380 E00701C00701800703800703000E8E000E78000E00000E00001C00001C00001C00001C0000FF00 001317808F14>I<03C20E2E181C381C301C701CE038E038E038E038C070C070C07060F061E01E E000E000E001C001C001C001C01FF00F177C8F12>I<30F059189E389C189C009C003800380038 0038007000700070007000E00060000D107C8F10>I<03E004300830187018601C001F801FC00F E000E00060E060E06080C041803E000C107D8F10>I<06000E000E000E000E001C001C00FFC01C 0038003800380038007000700070007000E100E100E100E200640038000A177C960D>I<38064C 074E0E8E0E9C0E9C0E1C1C381C381C381C7039703970393079389A0F0C10107C8F15>I<380C30 4C0E384E1C388E1C189C1C189C1C181C3810383810383810383810707020707020707040307040 18B8800F0F0015107C8F19>119 D<38064C074E0E8E0E9C0E9C0E1C1C381C381C381C70387038 7038307838F00F700070006060E0E1C0C18047003C0010177C8F13>121 D<038207C40FFC10081010002000400180030004000808100820187FF043E081C00F107E8F10> I E /Fd 2 79 df73 D78 D E /Fe 1 51 df<7FFFFCFFFFFEC00006 C00006C00006C00006C00006C00006C00006C00006C00006C00006C00006C00006C00006C00006 C00006C00006C00006C00006C00006FFFFFEFFFFFE17177C991F>50 D E /Ff 2 84 df<0000700001F00003C0000780000E00001C0000380000700000700000F00000E000 00E00000E00000E00000E00000E00000E00000E00000E00000E00000E00000E00000E00000E000 00E00000E00000E00000E00000E00000E00000E00000E00000E00000E00000E00000E00000E000 00E00000E00000E00001C00001C00001C0000380000700000600000E0000380000700000C00000 7000003800000E000006000007000003800001C00001C00001C00000E00000E00000E00000E000 00E00000E00000E00000E00000E00000E00000E00000E00000E00000E00000E00000E00000E000 00E00000E00000E00000E00000E00000E00000E00000E00000E00000E00000E00000E00000E000 00F000007000007000003800001C00000E000007800003C00001F000007014637B811F>26 D83 D E /Fg 8 118 df<06070600000000384C4C 8C98181830326262643808147F930C>105 D<0060007000600000000000000000038004C00460 08C008C000C000C0018001800180018003000300030003006600E600CC0078000C1A81930E>I< 3E0006000C000C000C000C001800187018B819383230340038003E006300631063106310C320C1 C00D147E9312>I<7C0C181818183030303060606060C0D0D0D0D06006147E930A>I<30F87C0059 0C86004E0D06009C0E0600980C0600180C0600180C060030180C0030180C803018188030181880 6030190060300E00190D7F8C1D>I<30F8590C4E0C9C0C980C180C180C30183019303130316032 601C100D7F8C15>I<03800C6018203030603060306030C060C06040C0608023001E000C0D7E8C 10>I<380C4C0C4C0C8C18981818181818303030323032307218B40F1C0F0D7F8C14>117 D E /Fh 1 60 df<60F0F07010101020204080040B7D830B>59 D E /Fi 4 94 df<007F00000188C000060830000808080010080400200802002008020040080100400801 00800800808008008080080080FFFFFF8080080080800800808008008080080080400801004008 010020080200200802001008040008080800060830000188C000007F0000191A7E951E>8 D<0007FFFC001FFFFC0063C038018380200383800007078000060780000007000000070000000F 0000000E0000000E0000001FFF00001FFE00001C00000038000000380000007800000070000000 70000000E0000000E0000031C0000079800000FE0000007C0000001E1A7F991C>70 D<00FFF80003FFFE000C787F0030781F8070780F80E0780780C07007800070070000F0070000F0 0E0000F00E0000E01C0000E0100001E0600001E7800001CFC00001C7C00003C3E0000383E00003 81E0000781F0000701F0180700F8300E00FC400E007F8018003E001D1A7E9921>82 D<400008C00018C00018C00018C03018C03018C03018C03018C03018C7FF18C7FF18C03018C030 18C03018C03018C03018C000186000303000601E03C00FFF8001FC0015167E951A>93 D E /Fj 4 53 df<0C003C00CC000C000C000C000C000C000C000C000C000C000C000C000C00FF 8009107E8F0F>49 D<1F00618040C08060C0600060006000C00180030006000C00102020207FC0 FFC00B107F8F0F>I<1F00218060C060C000C0008001800F00008000400060C060C06080406080 1F000B107F8F0F>I<0300030007000F000B001300330023004300C300FFE00300030003000300 1FE00B107F8F0F>I E /Fk 25 122 df45 D<00020006000C001C007C039C0038003800380038007000700070007000E000E000E000E001C0 01C001C001C003800380038003800780FFF00F1C7C9B15>49 D<03CC063C0C3C181C3838303870 387038E070E070E070E070E0E2C0E2C0E261E462643C380F127B9115>97 D<3F00070007000E000E000E000E001C001C001C001C0039C03E60383038307038703870387038 E070E070E070E060E0E0C0C0C1C0618063003C000D1D7B9C13>I<01F007080C08181C38383000 70007000E000E000E000E000E000E008E010602030C01F000E127B9113>I<001F800003800003 80000700000700000700000700000E00000E00000E00000E0003DC00063C000C3C00181C003838 00303800703800703800E07000E07000E07000E07000E0E200C0E200C0E20061E4006264003C38 00111D7B9C15>I<01E007100C1018083810701070607F80E000E000E000E000E000E008601060 2030C01F000D127B9113>I<0003C0000670000C70001C60001C00001C00003800003800003800 00380000380003FF8000700000700000700000700000700000E00000E00000E00000E00000E000 01C00001C00001C00001C00001C000038000038000038000030000030000070000C60000E60000 CC00007800001425819C0D>I<00F3018F030F06070E0E0C0E1C0E1C0E381C381C381C381C3838 30383038187818F00F700070007000E000E0C0C0E1C0C3007E00101A7D9113>I<0FC00001C000 01C0000380000380000380000380000700000700000700000700000E78000E8C000F0E000E0E00 1C0E001C0E001C0E001C0E00381C00381C00381C00383800703880703880707080707100E03200 601C00111D7D9C15>I<01800380010000000000000000000000000000001C002600470047008E 008E000E001C001C001C0038003800710071007100720072003C00091C7C9B0D>I<0006000E00 06000000000000000000000000000000F001180218021804380438003800380070007000700070 00E000E000E000E001C001C001C001C003800380C300E700CE0078000F24819B0D>I<1F800380 038007000700070007000E000E000E000E001C001C001C001C0038003800380038007000700070 007000E400E400E400E40068003800091D7C9C0B>108 D<3C1E0780266318C04683A0E04703C0 E08E0380E08E0380E00E0380E00E0380E01C0701C01C0701C01C0701C01C070380380E0388380E 0388380E0708380E0710701C0320300C01C01D127C9122>I<3C3C002646004687004707008E07 008E07000E07000E07001C0E001C0E001C0E001C1C00381C40381C40383840383880701900300E 0012127C9117>I<01E007180C0C180C380C300E700E700EE01CE01CE01CE018E038E030E06060 C031801E000F127B9115>I<07870004D98008E0C008E0C011C0E011C0E001C0E001C0E00381C0 0381C00381C00381800703800703000707000706000E8C000E70000E00000E00001C00001C0000 1C00001C00003C0000FF8000131A7F9115>I<3C3C26C2468747078E068E000E000E001C001C00 1C001C0038003800380038007000300010127C9112>114 D<01F006080C080C1C18181C001F00 1FC00FF007F0007800386030E030C030806060C01F000E127D9111>I<00C001C001C001C00380 038003800380FFE00700070007000E000E000E000E001C001C001C001C00384038403840388019 000E000B1A7D990E>I<1E0300270700470700470700870E00870E000E0E000E0E001C1C001C1C 001C1C001C1C003838803838801838801839001C5900078E0011127C9116>I<1E06270E470E47 06870287020E020E021C041C041C041C0818083808181018200C4007800F127C9113>I<1E0183 2703874703874703838707018707010E07010E07011C0E021C0E021C0E021C0E04180C04181C04 181C081C1C100C263007C3C018127C911C>I<070E0019910010E38020E38041C30041C00001C0 0001C000038000038000038000038000070200670200E70400CB04008B080070F00011127D9113 >I<1E03270747074707870E870E0E0E0E0E1C1C1C1C1C1C1C1C38383838183818381C7007F000 70007000E0E0C0E1C0818047003C00101A7C9114>I E /Fl 2 51 df<18F81818181818181818 1818FF080D7D8C0E>49 D<3E00418080C0C0C000C000C0018003000400084030407F80FF800A0D 7E8C0E>I E /Fm 5 94 df<040004000400C460E4E03F800E003F80E4E0C4600400040004000B 0D7E8D11>3 D21 D<040E0E1C1C1C38383070706060C0C0070F7F8F0A> 48 D<03FFF0000FFFF80030E07C0060C03C00C0C01C0081C0180001C0180001C0300001C02000 0180C000018F0000039E0000030F0000030F8000070780000603C0000603E0800C01F1000C00FE 001800780019147F931D>82 D<4001C003C003C003C003C183C183C7E3C7E3C183C183C183C003 6006381C1FF807E010117E9016>93 D E /Fn 31 122 df<01FFF803FFF80FFFF01E1E00180E00 380600700600700600E00E00E00E00E00E00E00C00E01C00E01800E0300060600030C0001F0000 15127E9118>27 D<60F0F06004047C830C>58 D<60F0F0701010101020204080040C7C830C>I< 0000038000000F0000003C000000F0000003C000000F0000003C000000F0000003C000000F0000 003C000000F0000000F00000003C0000000F00000003C0000000F00000003C0000000F00000003 C0000000F00000003C0000000F000000038019187D9520>I62 D<00000C0000000C0000001C0000001C0000003C0000007C0000005C 0000009C0000008E0000010E0000010E0000020E0000040E0000040E0000080E0000080E000010 0E0000200E00003FFE000040070000400700008007000100070001000700020007000200070006 0007001E000700FF807FF01C1D7F9C1F>65 D<0001F808000E061800380138006000F001C00070 03800070070000300F0000200E0000201C0000203C0000203C0000007800000078000000780000 00F0000000F0000000F0000000F0000000F0000100F0000100F000010070000200700002003000 0400380008001C0010000E0060000701800000FE00001D1E7E9C1E>67 D<01FFFF80003C01E000 380070003800380038001C0038001C0070001C0070001E0070001E0070001E00E0001E00E0001E 00E0001E00E0001E01C0003C01C0003C01C0003C01C000380380007803800070038000F0038000 E0070001C0070003800700070007001C000E007800FFFFC0001F1C7E9B22>I<01FFFFF0003C00 F0003800300038002000380020003800200070002000700020007010200070100000E0200000E0 200000E0600000FFE00001C0400001C0400001C0400001C0400003808000038000000380000003 800000070000000700000007000000070000000F000000FFF000001C1C7E9B1B>70 D<01FE0000FF003E0000F0002E0001E0002E0002E0002E0002E0002E0004E0004E0009C0004E00 09C000470011C000470011C0008700238000870043800087004380008700838001070107000107 010700010382070001038207000203840E000203880E000203880E000203900E000403A01C0004 03A01C000401C01C000C01C01C001C01803C00FF8103FF80281C7E9B28>77 D<000FC100303300400F00800601800603000603000606000406000407000007000007800003F0 0001FF0000FFC0003FE00003E00000F00000700000300000302000302000306000606000606000 C0600080F00300CC060083F800181E7E9C19>83 D<01FFC0FF80001E003C00001E003000000E00 2000000F00400000070080000007010000000782000000038400000003C800000001D000000001 F000000000E000000000E000000000F00000000170000000027000000004380000000838000000 103C000000201C000000401E000000800E000001800E000003000F000006000700001E000F8000 FF803FF000211C7F9B22>88 DI<00800080208020802080208020802080208020E027E03FE0 FF80FC80E08020802080208020802080208020802080208020802080208020E027E03FE0FF80FC 80E0802080208020802080200020000B277E9D10>93 D<01E3000717000C0F00180F00380E0030 0E00700E00700E00E01C00E01C00E01C00E01C00E03880E03880E038806078803199001E0E0011 127E9116>97 D<0001E0000630000E78000CF0001C60001C00001C00001C00003C000038000038 0003FFC000380000380000700000700000700000700000700000E00000E00000E00000E00000E0 0001C00001C00001C00001C00001C000018000038000038000630000F30000F60000E400007800 0015257E9C14>102 D<007180018B800307800607800E07000C07001C07001C0700380E00380E 00380E00380E00381C00381C00381C00183C0008F800073800003800003800007000607000F060 00F0E000E180007E0000111A7F9114>I<01C003C003C001800000000000000000000000001C00 270047004700870087000E000E001C001C001C003800388038807080710032001C000A1C7E9B0E >105 D<0007000F000F00060000000000000000000000000070009C010C020C021C041C001C00 1C0038003800380038007000700070007000E000E000E000E001C061C0F180F300E6007C001024 809B11>I<0FC00001C00001C0000380000380000380000380000700000700000700000700000E 07000E18800E21C00E23C01C47801C83001D00001E00003F800039C00038E00038E00070E10070 E10070E10070E200E06200603C00121D7E9C16>I<1F800380038007000700070007000E000E00 0E000E001C001C001C001C0038003800380038007000700070007000E400E400E400E400640038 00091D7E9C0C>I<381F81F04E20C6184640E81C4680F01C8F00F01C8E00E01C0E00E01C0E00E0 1C1C01C0381C01C0381C01C0381C01C0703803807138038071380380E1380380E2700700643003 003820127E9124>I<381F004E61804681C04701C08F01C08E01C00E01C00E01C01C03801C0380 1C03801C0700380710380710380E10380E2070064030038014127E9119>I<00F800030C000E06 001C0300180300300300700380700380E00700E00700E00700E00E00E00E00E01C006018006030 0030E0000F800011127E9114>I<07078009C86008D03008E03011C03011C03801C03801C03803 80700380700380700380600700E00700C00701800783000E86000E78000E00000E00001C00001C 00001C00001C00003C0000FF8000151A819115>I<383C4E424687470F8E1E8E0C0E000E001C00 1C001C001C0038003800380038007000300010127E9113>114 D<01F0060C04040C0E180C1C00 1F000FE00FF003F80038201C7018F018F010803060601F800F127E9113>I<00C001C001C001C0 0380038003800380FFF00700070007000E000E000E000E001C001C001C001C0038203820384038 4018800F000C1A80990F>I<1C00C02701C04701C04701C08703808703800E03800E03801C0700 1C07001C07001C0700180E20180E20180E201C1E200C264007C38013127E9118>I<07878008C8 4010F0C020F1E020E3C040E18000E00000E00001C00001C00001C00001C000638080F38080F381 00E5810084C60078780013127E9118>120 D<1C00C02701C04701C04701C08703808703800E03 800E03801C07001C07001C07001C0700180E00180E00180E001C1E000C3C0007DC00001C000018 00603800F03000F06000E0C0004180003E0000121A7E9114>I E /Fo 22 107 df0 D<400020C000606000C03001801803000C0600060C 0003180001B00000E00000E00001B000031800060C000C06001803003001806000C0C000604000 2013147A9320>2 D17 D<007FFF8001FFFF80078000000E00000018000000 30000000300000006000000060000000C0000000C0000000C0000000C0000000C0000000C00000 00C000000060000000600000003000000030000000180000000E0000000780000001FFFF80007F FF80000000000000000000000000000000000000000000000000000000007FFFFF807FFFFF8019 227D9920>I<000001800000078000001E00000078000001E00000078000001E00000078000001 E00000078000001E00000078000000E0000000780000001E0000000780000001E0000000780000 001E0000000780000001E0000000780000001E0000000780000001800000000000000000000000 00000000000000000000000000000000007FFFFF00FFFFFF8019227D9920>20 DI<007FFF8003FFFF8007800000 0C0000001800000030000000300000006000000060000000C0000000C0000000C0000000C00000 00C0000000C0000000C0000000C000000060000000600000003000000030000000180000000E00 00000780000001FFFF80007FFF80191A7D9620>26 D<0000000400000000020000000002000000 00010000000000800000000040FFFFFFFFF8FFFFFFFFF800000000400000000080000000010000 0000020000000002000000000400250E7E902A>33 D<007FF801FFF80780000E00001800003000 00300000600000600000C00000C00000C00000FFFFF8FFFFF8C00000C00000C000006000006000 003000003000001800000E000007800001FFF8007FF8151A7D961C>50 D<0000600000600000C0 0000C0000180000180000180000300000300000600000600000C00000C00001800001800001800 00300000300000600000600000C00000C000018000018000030000030000030000060000060000 0C00000C0000180000180000300000300000300000600000600000C0000040000013287A9D00> 54 D<0008001803D80C301838303C303C706E606660666066E0C7E0C7E0C7E0C7E187E187E187 E187E187E307E307E307E307E60766066606760E3C0C3C0C1C180C301BC01800180010237E9F15 >59 D<0001FFFF000FFFFF0038E00E0041E00C01C1E0000381C0000301C0000603C0000003C000 0003800000038000000780000007000000070000000FFFC0000FFF00000E0000001C0000001C00 00003C00000038000000380000007000000070000030E0000070C00000FD800000FF0000003C00 0000201D7F9B1E>70 D<0001800000100003800000300003800000300003800000600007C00000 E00007C00001E00005C00003E00005C00007E00005C00007E00005E0000DC00009E00019C00008 E00033C00008E00073C00010F000E3C00010F001C3C00010700383C00020700303C00020780603 800020780C038000403818078000403C38078000403C70078000801CE0078000801FC007800100 1F80078001000F00078062000E000780FE00040007C0FC00000007F0FC00000003C07800000000 002C1F7F9C32>77 D<003FFF000001FFFFE000071E0FF000081C01F800381C00F800703C007800 603C007800C03C007800003C0070000038007000003800E000007800C000007801800000780200 0000700C00000071F0000000F3F0000000E1F0000000E0F8000001E0F8000001C07C000001C07C 000003C03C000003803E018003803E070007801F060007001F880006000FF0000C0007C000211D 809B23>82 D<0000000400FFFFF803FFFFE00400E0001C00E0003801C0003001C0007003C000E0 03C000C00380000003800000078000000780000007000000070000000F0000000E0000000E0000 001E0000001E0000001C0000001C00000038000000380000007000000060000000C0000007FF00 000FFC00001E1D7F9C17>84 D<78000CFC001E3E001F1E001F0F000F0F00070700030700020780 020780020380040380040380080380180380300380300380600380C0038180038380038700038E 00039C0003B80003F00003E00007C000078000060000040000181E7E9B19>86 D<400002C00006C00006C00006C00006C00006C00006C00006C00006C00006C00006C00006C000 06C00006C00006C00006C00006C00006C0000660000C60000C3000181C00700F01E003FF8000FE 00171A7E981C>91 D<00FE0003FF800F01E01C007030001860000C60000CC00006C00006C00006 C00006C00006C00006C00006C00006C00006C00006C00006C00006C00006C00006C00006C00006 C00006C00006400002171A7E981C>I<400002C00006C00006C00006C00006C01806C01806C018 06C01806C01806C01806C7FFC6C7FFC6C01806C01806C01806C01806C01806C0180660000C6000 0C3000181C00700F01E003FF8000FE00171A7E981C>I<003C00E001C001800380038003800380 038003800380038003800380038003800380030007001C00F0001C000700030003800380038003 80038003800380038003800380038003800380018001C000E0003C0E297D9E15>102 DI106 D E /Fp 39 124 df<003FC00001F03000 03C0380007C07C000F807C000F807C000F8038000F8000000F8000000F8000000F800000FFFFFC 00FFFFFC000F807C000F807C000F807C000F807C000F807C000F807C000F807C000F807C000F80 7C000F807C000F807C000F807C000F807C000F807C007FE1FF807FE1FF80191D809C1B>12 D<78FCFCFCFC7806067D850D>46 D<00600001E0000FE000FFE000F3E00003E00003E00003E000 03E00003E00003E00003E00003E00003E00003E00003E00003E00003E00003E00003E00003E000 03E00003E00003E00003E0007FFF807FFF80111B7D9A18>49 D<07F8001FFE00383F80780FC0FC 07C0FC07E0FC03E0FC03E07803E00007E00007C00007C0000F80001F00001E0000380000700000 E0000180600300600600600800E01FFFC03FFFC07FFFC0FFFFC0FFFFC0131B7E9A18>I<03F800 1FFE003C1F003C0F807C07C07E07C07C07C03807C0000F80000F80001E00003C0003F800001E00 000F800007C00007C00007E03007E07807E0FC07E0FC07E0FC07C0780F80781F001FFE0007F800 131B7E9A18>I<000180000380000780000F80001F80003F80006F8000CF80008F80018F80030F 80060F800C0F80180F80300F80600F80C00F80FFFFF8FFFFF8000F80000F80000F80000F80000F 80000F8001FFF801FFF8151B7F9A18>I<1801801FFF001FFE001FFC001FF8001FC00018000018 000018000018000019F8001E0E00180F801007800007C00007E00007E00007E07807E0F807E0F8 07E0F807C0F007C0600F80381F001FFE0007F000131B7E9A18>I<007E0003FF000781800F03C0 1E07C03C07C03C0380780000780000F80000F8F800FB0E00FA0780FC0380FC03C0F803E0F803E0 F803E0F803E07803E07803E07803C03C03C03C07801E0F0007FE0003F800131B7E9A18>I<78FC FCFCFC7800000000000078FCFCFCFC7806127D910D>58 D<00038000000380000007C0000007C0 000007C000000FE000000FE000001FF000001BF000001BF0000031F8000031F8000061FC000060 FC0000E0FE0000C07E0000C07E0001803F0001FFFF0003FFFF8003001F8003001F8006000FC006 000FC00E000FE00C0007E0FFC07FFEFFC07FFE1F1C7E9B24>65 DI68 DI76 D78 D80 D<7FFFFFE07FFFFFE0781F81E0701F80E0 601F8060E01F8070C01F8030C01F8030C01F8030C01F8030001F8000001F8000001F8000001F80 00001F8000001F8000001F8000001F8000001F8000001F8000001F8000001F8000001F8000001F 8000001F8000001F800007FFFE0007FFFE001C1C7E9B21>84 DI<0FF8001C1E003E0F803E07 803E07C01C07C00007C0007FC007E7C01F07C03C07C07C07C0F807C0F807C0F807C0780BC03E13 F80FE1F815127F9117>97 D<03FC000E0E001C1F003C1F00781F00780E00F80000F80000F80000 F80000F80000F800007800007801803C01801C03000E0E0003F80011127E9115>99 D<000FF0000FF00001F00001F00001F00001F00001F00001F00001F00001F00001F001F9F00F07 F01C03F03C01F07801F07801F0F801F0F801F0F801F0F801F0F801F0F801F07801F07801F03C01 F01C03F00F0FFE03F9FE171D7E9C1B>I<01FC000F07001C03803C01C07801C07801E0F801E0F8 01E0FFFFE0F80000F80000F800007800007C00603C00601E00C00F038001FC0013127F9116>I< 007F0001E38003C7C00787C00F87C00F83800F80000F80000F80000F80000F8000FFF800FFF800 0F80000F80000F80000F80000F80000F80000F80000F80000F80000F80000F80000F80000F8000 0F80007FF8007FF800121D809C0F>I<03F8F00E0F381E0F381C07303C07803C07803C07803C07 801C07001E0F000E0E001BF8001000001800001800001FFF001FFFC00FFFE01FFFF07801F8F000 78F00078F000787000707800F01E03C007FF00151B7F9118>II<1E003F003F003F003F001E00000000000000000000000000FF00FF001F001F001F001F00 1F001F001F001F001F001F001F001F001F001F00FFE0FFE00B1E7F9D0E>I<007800FC00FC00FC 00FC007800000000000000000000000003FC03FC007C007C007C007C007C007C007C007C007C00 7C007C007C007C007C007C007C007C007C707CF87CF878F8F070E01F800E26839D0F>III< FF0FC07E00FF31E18F001F40F207801F80FC07C01F80FC07C01F00F807C01F00F807C01F00F807 C01F00F807C01F00F807C01F00F807C01F00F807C01F00F807C01F00F807C01F00F807C01F00F8 07C0FFE7FF3FF8FFE7FF3FF825127F9128>II<01FC000F07801C01C03C01E07800F07800F0F800F8F800F8F800F8F800F8F800F8F800F878 00F07800F03C01E01E03C00F078001FC0015127F9118>II114 D<1FD830786018E018E018F000FF807FE07FF01FF807FC00 7CC01CC01CE01CE018F830CFC00E127E9113>I<0300030003000300070007000F000F003FFCFF FC1F001F001F001F001F001F001F001F001F001F0C1F0C1F0C1F0C0F08079803F00E1A7F9913> I119 DI123 D E /Fq 6 53 df<006000006000006000006000006000006000006000006000006000006000FF FFF0FFFFF000600000600000600000600000600000600000600000600000600000600014167E91 19>43 D<0F0030C0606060604020C030C030C030C030C030C030C030C030C03040206060606030 C00F000C137E9211>48 D<0C001C00EC000C000C000C000C000C000C000C000C000C000C000C00 0C000C000C000C00FFC00A137D9211>I<1F0060C06060F070F030603000700070006000C001C0 0180020004000810101020207FE0FFE00C137E9211>I<0FC030707038703870380038003000E0 0FC0007000380018001C601CF01CF018E03860701FC00E137F9211>I<006000E000E001600260 06600C600860106020606060C060FFFC0060006000600060006003FC0E137F9211>I E /Fr 24 118 df<00180000780001F800FFF800FFF80001F80001F80001F80001F80001F80001 F80001F80001F80001F80001F80001F80001F80001F80001F80001F80001F80001F80001F80001 F80001F80001F80001F80001F80001F80001F8007FFFE07FFFE013207C9F1C>49 D<03FC000FFF003C1FC07007E07C07F0FE03F0FE03F8FE03F8FE01F87C01F83803F80003F80003 F00003F00007E00007C0000F80001F00003E0000380000700000E01801C0180380180700180E00 380FFFF01FFFF03FFFF07FFFF0FFFFF0FFFFF015207D9F1C>I<00FE0007FFC00F07E01E03F03F 03F03F81F83F81F83F81F81F03F81F03F00003F00003E00007C0001F8001FE0001FF000007C000 01F00001F80000FC0000FC3C00FE7E00FEFF00FEFF00FEFF00FEFF00FC7E01FC7801F81E07F00F FFC001FE0017207E9F1C>I73 D80 D82 D<01FC0407FF8C1F03FC3C007C7C003C78 001C78001CF8000CF8000CFC000CFC0000FF0000FFE0007FFF007FFFC03FFFF01FFFF80FFFFC03 FFFE003FFE0003FF00007F00003F00003FC0001FC0001FC0001FE0001EE0001EF0003CFC003CFF 00F8C7FFE080FF8018227DA11F>I<7FFFFFFF807FFFFFFF807E03F80F807803F807807003F803 806003F80180E003F801C0E003F801C0C003F800C0C003F800C0C003F800C0C003F800C00003F8 00000003F800000003F800000003F800000003F800000003F800000003F800000003F800000003 F800000003F800000003F800000003F800000003F800000003F800000003F800000003F8000000 03F800000003F800000003F800000003F8000003FFFFF80003FFFFF80022227EA127>I<07FC00 1FFF803F07C03F03E03F01E03F01F01E01F00001F00001F0003FF003FDF01FC1F03F01F07E01F0 FC01F0FC01F0FC01F0FC01F07E02F07E0CF81FF87F07E03F18167E951B>97 D<00FF8007FFE00F83F01F03F03E03F07E03F07C01E07C0000FC0000FC0000FC0000FC0000FC00 00FC00007C00007E00007E00003E00301F00600FC0E007FF8000FE0014167E9519>99 D<0001FE000001FE0000003E0000003E0000003E0000003E0000003E0000003E0000003E000000 3E0000003E0000003E0000003E0001FC3E0007FFBE000F81FE001F007E003E003E007E003E007C 003E00FC003E00FC003E00FC003E00FC003E00FC003E00FC003E00FC003E00FC003E007C003E00 7C003E003E007E001E00FE000F83BE0007FF3FC001FC3FC01A237EA21F>I<00FE0007FF800F87 C01E01E03E01F07C00F07C00F8FC00F8FC00F8FFFFF8FFFFF8FC0000FC0000FC00007C00007C00 007E00003E00181F00300FC07003FFC000FF0015167E951A>I<003F8000FFC001E3E003C7E007 C7E00F87E00F83C00F80000F80000F80000F80000F80000F8000FFFC00FFFC000F80000F80000F 80000F80000F80000F80000F80000F80000F80000F80000F80000F80000F80000F80000F80000F 80000F80000F80007FF8007FF80013237FA211>I104 D<1C003E007F007F007F003E001C000000000000000000000000 000000FF00FF001F001F001F001F001F001F001F001F001F001F001F001F001F001F001F001F00 1F001F00FFE0FFE00B247EA310>I108 DII<00FE0007FFC00F83E01E00F03E00F87C007C7C007C7C00 7CFC007EFC007EFC007EFC007EFC007EFC007EFC007E7C007C7C007C3E00F81F01F00F83E007FF C000FE0017167E951C>II114 D<0FF3003FFF00781F00600700E0 0300E00300F00300FC00007FE0007FF8003FFE000FFF0001FF00000F80C00780C00380E00380E0 0380F00700FC0E00EFFC00C7F00011167E9516>I<018000018000018000018000038000038000 0780000780000F80003F8000FFFF00FFFF000F80000F80000F80000F80000F80000F80000F8000 0F80000F80000F80000F80000F81800F81800F81800F81800F81800F830007C30003FE0000F800 11207F9F16>II E /Fs 73 128 df<007E1F8001C170400703C060060380E00E0380400E0380000E0380000E0380000E0380000E 038000FFFFFFE00E0380E00E0380E00E0380E00E0380E00E0380E00E0380E00E0380E00E0380E0 0E0380E00E0380E00E0380E00E0380E00E0380E00E0380E07F8FE3FC1E1A809920>14 D<00800100020004000C00080018003000300030006000600060006000E000E000E000E000E000 E000E000E000E000E0006000600060006000300030003000180008000C00040002000100008009 267D9B0F>40 D<8000400020001000180008000C00060006000600030003000300030003800380 0380038003800380038003800380038003000300030003000600060006000C0008001800100020 004000800009267E9B0F>I<60F0F07010101020204080040B7D830B>44 DI<60F0F06004047D830B>I<078018603030303060186018E01CE01CE0 1CE01CE01CE01CE01CE01CE01CE01CE01CE01C6018601870383030186007800E187E9713>48 D<03000700FF000700070007000700070007000700070007000700070007000700070007000700 0700070007000700FFF00C187D9713>I<0F80106020304038803CC01CE01C401C003C00380038 0070006000C001800100020004040804100430083FF87FF8FFF80E187E9713>I<0F8010E02070 607870382038007800700070006000C00F8000E000700038003C003CE03CE03CC03C4038407030 E00F800E187E9713>I<00300030007000F000F001700370027004700C70087010703070207040 70C070FFFF00700070007000700070007007FF10187F9713>I<30183FF03FE03FC02000200020 002000200027C03860203000380018001C001C401CE01CE01C80184038403030E00F800E187E97 13>I<01E006100C1818383038300070006000E000E7C0E860F030F018E018E01CE01CE01C601C 601C701830183030186007C00E187E9713>I<40007FFE7FFC7FFC400880108010802000400040 0080018001800100030003000300030007000700070007000700070002000F197E9813>I<0780 18603030201860186018601870103C303E600F8007C019F030F86038401CC00CC00CC00CC00C60 08201018600FC00E187E9713>I<07801860303070306018E018E018E01CE01CE01C601C603C30 3C185C0F9C001C00180018003870307060604021801F000E187E9713>I<60F0F0600000000000 00000060F0F06004107D8F0B>I<007F00000180C000060030000800080010000400203E020020 E1020041C081004380710083807080870070808700708087007080870070808700708087007080 838070804380708041C0F10020E13100203E1E0010000000080000000600038001803E00007FE0 00191A7E991E>64 D<000C0000000C0000000C0000001E0000001E0000003F0000002700000027 00000043800000438000004380000081C0000081C0000081C0000100E0000100E00001FFE00002 0070000200700006007800040038000400380008001C0008001C001C001E00FF00FFC01A1A7F99 1D>II<003F0201C0C603002E0E001E1C000E1C00063800067800027000027000 02F00000F00000F00000F00000F00000F000007000027000027800023800041C00041C00080E00 0803003001C0C0003F00171A7E991C>IIII<00 3F020001C0C60003002E000E001E001C000E001C00060038000600780002007000020070000200 F0000000F0000000F0000000F0000000F0000000F001FFC070000E0070000E0078000E0038000E 001C000E001C000E000E000E000300160001C06600003F82001A1A7E991E>II< FFE00E000E000E000E000E000E000E000E000E000E000E000E000E000E000E000E000E000E000E 000E000E000E000E000E00FFE00B1A7F990E>I<1FFC00E000E000E000E000E000E000E000E000 E000E000E000E000E000E000E000E000E000E000E040E0E0E0E0E041C061801E000E1A7D9914> IIIII<007F000001C1C000070070000E0038001C001C003C001E0038000E0078000F0070000700 F0000780F0000780F0000780F0000780F0000780F0000780F0000780F000078078000F0078000F 0038000E003C001E001C001C000E0038000700700001C1C000007F0000191A7E991E>II82 D<0FC21836200E6006C006C002C002C002E00070007E003FE01FF807FC003E000E000700038003 80038003C002C006E004D81887E0101A7E9915>I<7FFFFF00701C0700401C0100401C0100C01C 0180801C0080801C0080801C0080001C0000001C0000001C0000001C0000001C0000001C000000 1C0000001C0000001C0000001C0000001C0000001C0000001C0000001C0000001C0000001C0000 001C000003FFE000191A7F991C>IIII<7FC0FF 000F003C0007003000078020000380600001C0400001E0800000E1800000710000007A0000003C 0000001C0000001E0000001E00000017000000278000004380000041C0000081E0000100E00001 00700002007800040038000C001C001E003E00FF80FFC01A1A7F991D>II<7FFFC0780380700380600700400700 400E00401C00401C0000380000380000700000E00000E00001C00001C000038000070040070040 0E00400E00401C00C0380080380180700380700780FFFF80121A7E9917>II93 D<3F8070C070E020700070007007F01C7030707070E070E071E071E0F171FB1E3C10107E8F 13>97 DI<07F80C1C381C30087000E000E000E000E000E000E000700030043808 0C1807E00E107F8F11>I<007E00000E00000E00000E00000E00000E00000E00000E00000E0000 0E0003CE000C3E00380E00300E00700E00E00E00E00E00E00E00E00E00E00E00E00E00600E0070 0E00381E001C2E0007CFC0121A7F9915>I<07C01C3030187018600CE00CFFFCE000E000E000E0 006000300438080C1807E00E107F8F11>I<01F0031807380E100E000E000E000E000E000E00FF C00E000E000E000E000E000E000E000E000E000E000E000E000E000E007FE00D1A80990C>I<0F CE187330307038703870387038303018602FC02000600070003FF03FFC1FFE600FC003C003C003 C0036006381C07E010187F8F13>II<18003C003C001800000000000000000000 000000FC001C001C001C001C001C001C001C001C001C001C001C001C001C001C00FF80091A8099 0A>I<018003C003C001800000000000000000000000000FC001C001C001C001C001C001C001C0 01C001C001C001C001C001C001C001C001C001C001C041C0E180E3007E000A2182990C>IIIII<07E01C3830 0C700E6006E007E007E007E007E007E0076006700E381C1C3807E010107F8F13>II<03C2000C260038 1E00300E00700E00E00E00E00E00E00E00E00E00E00E00E00E00700E00700E00381E001C2E0007 CE00000E00000E00000E00000E00000E00000E00007FC012177F8F14>II<1F2060E04020C020C0 20F0007F003FC01FE000F080708030C030C020F0408F800C107F8F0F>I<0400040004000C000C 001C003C00FFC01C001C001C001C001C001C001C001C001C201C201C201C201C200E4003800B17 7F960F>IIIIII<7FF86070407040E041C041C00380070007000E081C081C08381070107030FFF00D10 7F8F11>II<6180F3C0F3C061800A047C9913>127 D E /Ft 70 124 df<007E1F0001C1B1800303E3C00703C3C00E03C1800E01C0000E01C0000E01 C0000E01C0000E01C0000E01C000FFFFFC000E01C0000E01C0000E01C0000E01C0000E01C0000E 01C0000E01C0000E01C0000E01C0000E01C0000E01C0000E01C0000E01C0000E01C0000E01C000 0E01C0007F87FC001A1D809C18>11 D<007E0001C1800301800703C00E03C00E01800E00000E00 000E00000E00000E0000FFFFC00E01C00E01C00E01C00E01C00E01C00E01C00E01C00E01C00E01 C00E01C00E01C00E01C00E01C00E01C00E01C00E01C07F87F8151D809C17>I<007FC001C1C003 03C00703C00E01C00E01C00E01C00E01C00E01C00E01C00E01C0FFFFC00E01C00E01C00E01C00E 01C00E01C00E01C00E01C00E01C00E01C00E01C00E01C00E01C00E01C00E01C00E01C00E01C07F CFF8151D809C17>I<6060F0F0F8F86868080808080808101010102020404080800D0C7F9C15> 34 D<004000800100020006000C000C0018001800300030007000600060006000E000E000E000 E000E000E000E000E000E000E000E000E000600060006000700030003000180018000C000C0006 0002000100008000400A2A7D9E10>40 D<800040002000100018000C000C000600060003000300 038001800180018001C001C001C001C001C001C001C001C001C001C001C001C001800180018003 8003000300060006000C000C00180010002000400080000A2A7E9E10>I<000600000006000000 060000000600000006000000060000000600000006000000060000000600000006000000060000 00060000FFFFFFE0FFFFFFE0000600000006000000060000000600000006000000060000000600 000006000000060000000600000006000000060000000600001B1C7E9720>43 D<60F0F0701010101020204080040C7C830C>II<60F0F06004047C830C >I<03C00C301818300C300C700E60066006E007E007E007E007E007E007E007E007E007E007E0 07E007E00760066006700E300C300C18180C3007E0101D7E9B15>48 D<030007003F00C7000700 070007000700070007000700070007000700070007000700070007000700070007000700070007 0007000F80FFF80D1C7C9B15>I<07C01830201C400C400EF00FF80FF807F8077007000F000E00 0E001C001C00380070006000C00180030006010C01180110023FFE7FFEFFFE101C7E9B15>I<07 E01830201C201C781E780E781E381E001C001C00180030006007E00030001C001C000E000F000F 700FF80FF80FF80FF00E401C201C183007E0101D7E9B15>I<300C3FF83FF03FC0200020002000 20002000200023E024302818301C200E000E000F000F000F600FF00FF00FF00F800E401E401C20 38187007C0101D7E9B15>53 D<00F0030C06040C0E181E301E300C700070006000E3E0E430E818 F00CF00EE006E007E007E007E007E007600760077006300E300C18180C3003E0101D7E9B15>I< 4000007FFF807FFF007FFF00400200800400800400800800001000001000002000006000004000 00C00000C00001C000018000018000038000038000038000038000078000078000078000078000 078000078000030000111D7E9B15>I<03E00C301008200C20066006600660067006780C3E083F B01FE007F007F818FC307E601E600FC007C003C003C003C00360026004300C1C1007E0101D7E9B 15>I<03C00C301818300C700C600EE006E006E007E007E007E007E0076007700F300F18170C27 07C700060006000E300C780C78187010203030C00F80101D7E9B15>I<60F0F060000000000000 0000000060F0F06004127C910C>I<60F0F0600000000000000000000060F0F070101010102020 4080041A7C910C>I<7FFFFFC0FFFFFFE000000000000000000000000000000000000000000000 00000000000000000000FFFFFFE07FFFFFC01B0C7E8F20>61 D<00060000000600000006000000 0F0000000F0000000F00000017800000178000001780000023C0000023C0000023C0000041E000 0041E0000041E0000080F0000080F0000180F8000100780001FFF80003007C0002003C0002003C 0006003E0004001E0004001E000C001F001E001F00FF80FFF01C1D7F9C1F>65 DI<001F808000E0618001801980070007800E0003801C0003801C 00018038000180780000807800008070000080F0000000F0000000F0000000F0000000F0000000 F0000000F0000000F0000000700000807800008078000080380000801C0001001C0001000E0002 00070004000180080000E03000001FC000191E7E9C1E>III< FFFFF80F00780F00180F00080F00080F000C0F00040F00040F02040F02000F02000F02000F0600 0FFE000F06000F02000F02000F02000F02000F00000F00000F00000F00000F00000F00000F0000 0F8000FFF800161C7E9B1B>I<001F808000E0618001801980070007800E0003801C0003801C00 018038000180780000807800008070000080F0000000F0000000F0000000F0000000F0000000F0 000000F000FFF0F0000F80700007807800078078000780380007801C0007801C0007800E000780 07000B800180118000E06080001F80001C1E7E9C21>III<1FFF00F800780078007800780078007800780078007800780078007800 780078007800780078007800787078F878F878F878F0F040E021C01F00101D7F9B15>IIIII<003F800000E0E0000380380007001C000E000E001C0007003C000780380003807800 03C0780003C0700001C0F00001E0F00001E0F00001E0F00001E0F00001E0F00001E0F00001E0F0 0001E0700001C0780003C0780003C0380003803C0007801C0007000E000E0007001C0003803800 00E0E000003F80001B1E7E9C20>I82 D<07E0801C1980300580700380600180E001 80E00080E00080E00080F00000F800007C00007FC0003FF8001FFE0007FF0000FF80000F800007 C00003C00001C08001C08001C08001C0C00180C00180E00300D00200CC0C0083F800121E7E9C17 >I<7FFFFFC0700F01C0600F00C0400F0040400F0040C00F0020800F0020800F0020800F002000 0F0000000F0000000F0000000F0000000F0000000F0000000F0000000F0000000F0000000F0000 000F0000000F0000000F0000000F0000000F0000000F0000000F0000001F800003FFFC001B1C7F 9B1E>I87 D91 D93 D<1FC000307000783800781C00301C00001C00 001C0001FC000F1C00381C00701C00601C00E01C40E01C40E01C40603C40304E801F870012127E 9115>97 DI<07E00C301878307870306000E000E000E000 E000E000E00060007004300418080C3007C00E127E9112>I<003F000007000007000007000007 0000070000070000070000070000070000070003E7000C1700180F00300700700700600700E007 00E00700E00700E00700E00700E00700600700700700300700180F000C370007C7E0131D7E9C17 >I<03E00C301818300C700E6006E006FFFEE000E000E000E00060007002300218040C1803E00F 127F9112>I<00F8018C071E061E0E0C0E000E000E000E000E000E00FFE00E000E000E000E000E 000E000E000E000E000E000E000E000E000E000E000E007FE00F1D809C0D>I<00038003C4C00C 38C01C3880181800381C00381C00381C00381C001818001C38000C300013C00010000030000018 00001FF8001FFF001FFF803003806001C0C000C0C000C0C000C06001803003001C0E0007F80012 1C7F9215>II<18003C003C001800000000000000000000 0000000000FC001C001C001C001C001C001C001C001C001C001C001C001C001C001C001C001C00 FF80091D7F9C0C>I<00C001E001E000C000000000000000000000000000000FE000E000E000E0 00E000E000E000E000E000E000E000E000E000E000E000E000E000E000E000E000E060E0F0C0F1 C061803E000B25839C0D>IIIII<03F0000E1C00180600300300700380600180E001C0E0 01C0E001C0E001C0E001C0E001C06001807003803003001806000E1C0003F00012127F9115>I< FC7C001D86001E03001C01801C01C01C00C01C00E01C00E01C00E01C00E01C00E01C00E01C01C0 1C01C01C01801E03001D06001CF8001C00001C00001C00001C00001C00001C00001C0000FF8000 131A7F9117>I<03C1000C3300180B00300F00700700700700E00700E00700E00700E00700E007 00E00700600700700700300F00180F000C370007C7000007000007000007000007000007000007 00000700003FE0131A7E9116>II<1F9030704030C010C010E010F8007F803FE00FF000 F880388018C018C018E010D0608FC00D127F9110>I<04000400040004000C000C001C003C00FF E01C001C001C001C001C001C001C001C001C001C101C101C101C101C100C100E2003C00C1A7F99 10>IIII<7F8FF00F03800F030007020003840001C80001D80000F000007000007800 00F800009C00010E00020E000607000403801E07C0FF0FF81512809116>II<7F FC70386038407040F040E041C003C0038007000F040E041C043C0C380870087038FFF80E127F91 12>II E /Fu 29 122 df<0001FF007FC000001FFFC7FFF000007F01FFC0 380000FC00FF003C0001F003FC007E0003F003FC00FE0007E003F800FE0007E003F800FE0007E0 03F8007C0007E001F800380007E001F800000007E001F800000007E001F800000007E001F80000 0007E001F8000000FFFFFFFFFFFE00FFFFFFFFFFFE0007E001F8007E0007E001F8007E0007E001 F8007E0007E001F8007E0007E001F8007E0007E001F8007E0007E001F8007E0007E001F8007E00 07E001F8007E0007E001F8007E0007E001F8007E0007E001F8007E0007E001F8007E0007E001F8 007E0007E001F8007E0007E001F8007E0007E001F8007E0007E001F8007E0007E001F8007E0007 E001F8007E0007E001F8007E0007E001F8007E0007E001F8007E007FFE1FFF87FFE07FFE1FFF87 FFE0332A7FA937>14 D<00000700000000000700000000000F80000000000F80000000000F8000 0000001FC0000000001FC0000000003FE0000000003FE0000000003FE00000000067F000000000 67F000000000E7F800000000C3F800000000C3F80000000181FC0000000181FC0000000381FE00 00000300FE0000000300FE00000006007F00000006007F0000000C007F8000000C003F8000000C 003F80000018001FC0000018001FC000003FFFFFE000003FFFFFE0000070000FF00000600007F0 0000600007F00000C00007F80000C00003F80001C00003FC0001800001FC0001800001FC000300 0001FE0007800000FE00FFF8003FFFF8FFF8003FFFF82D297EA832>65 D<00007FE0020007FFF8 06001FE01E0E007F00039E00FC0001FE01F800007E07F000003E07E000003E0FC000001E1FC000 000E3F8000000E3F8000000E3F800000067F800000067F000000067F00000000FF00000000FF00 000000FF00000000FF00000000FF00000000FF00000000FF00000000FF00000000FF000000007F 000000007F000000007F800000063F800000063F800000063F800000061FC000000C0FC000000C 07E000001807F000003801F800003000FC0000E0007F0003C0001FE00F000007FFFC0000007FE0 0027297CA830>67 DI80 D82 D<00FF004003FFE0C00F80F9C0 1E001FC03C000FC03C0007C0780003C0780001C0F80001C0F80001C0F80000C0FC0000C0FC0000 C0FE0000007F0000007FF000007FFF00003FFFF0001FFFFC000FFFFE0007FFFF0001FFFF80003F FFC00001FFE000001FE000000FF0000007F0000003F0C00003F0C00001F0C00001F0C00001F0E0 0001F0E00001E0F00001E0F80003C0FC0003C0FF000780E3E01F00C1FFFC00801FF0001C297CA8 25>I<7FFFFFFFFF007FFFFFFFFF007F007F007F007C007F001F0070007F00070070007F000700 60007F000300E0007F000380E0007F000380C0007F000180C0007F000180C0007F000180C0007F 000180C0007F00018000007F00000000007F00000000007F00000000007F00000000007F000000 00007F00000000007F00000000007F00000000007F00000000007F00000000007F00000000007F 00000000007F00000000007F00000000007F00000000007F00000000007F00000000007F000000 00007F00000000007F00000000007F00000000007F00000000007F00000000007F00000000007F 00000000FFFFFF800000FFFFFF800029297EA82E>II<03FF80000FFFE0001F01F8003F80FC003F807E003F807E003F803F001F003F0000003F0000 003F0000003F0000003F00003FFF0001FE3F000FE03F001F803F003F003F007F003F00FE003F00 FE003F0CFE003F0CFE003F0CFE005F0C7F009F0C3F831FF81FFE0FF003F807C01E1B7E9A21>97 D<003FE001FFF807E07C0FC0FE1F80FE3F00FE3F00FE7E007C7E00007E0000FE0000FE0000FE00 00FE0000FE0000FE0000FE00007E00007E00007F00003F00033F80031F80060FC00C07F03801FF F0003FC0181B7E9A1D>99 D<00003FF000003FF0000003F0000003F0000003F0000003F0000003 F0000003F0000003F0000003F0000003F0000003F0000003F0000003F0000003F0003F83F001FF F3F007F03BF00FC00FF01F8007F03F0003F03F0003F07E0003F07E0003F07E0003F0FE0003F0FE 0003F0FE0003F0FE0003F0FE0003F0FE0003F0FE0003F0FE0003F07E0003F07E0003F03F0003F0 3F0007F01F8007F00FC01FF007E07BF001FFE3FF007F83FF202A7EA925>I<007F800001FFF000 07E0F8000F807C001F003E003F003F003F001F007E001F007E001F80FE001F80FE001F80FFFFFF 80FFFFFF80FE000000FE000000FE000000FE0000007E0000007E0000007F0000003F0001803F00 01801F8003000FC0060003F81C0001FFF800003FC000191B7E9A1E>I<0007F0003FF800FC7C01 F8FE03F0FE03E0FE07E0FE07E07C07E00007E00007E00007E00007E00007E00007E000FFFF80FF FF8007E00007E00007E00007E00007E00007E00007E00007E00007E00007E00007E00007E00007 E00007E00007E00007E00007E00007E00007E00007E00007E00007E00007E0007FFF007FFF0017 2A7FA914>I<00FF01E003FFC7F80F81FC781F00F8783E007C703E007C007E007E007E007E007E 007E007E007E007E007E007E007E003E007C003E007C001F00F8000F81F0000BFFC00018FF0000 1000000038000000380000003C0000001FFFF0001FFFFE000FFFFF8007FFFFC00FFFFFE03E000F E07C0003F0780003F0F80001F0F80001F0F80001F0F80001F07C0003E07C0003E03F000FC00FC0 3F0007FFFE00007FE0001D287E9A21>II<0F001F 803FC03FC03FC03FC01F800F0000000000000000000000000000000000FFC0FFC00FC00FC00FC0 0FC00FC00FC00FC00FC00FC00FC00FC00FC00FC00FC00FC00FC00FC00FC00FC00FC00FC00FC00F C0FFFCFFFC0E2B7EAA13>I<000F00001F80003FC0003FC0003FC0003FC0001F80000F00000000 00000000000000000000000000000000000000000001FFC001FFC0000FC0000FC0000FC0000FC0 000FC0000FC0000FC0000FC0000FC0000FC0000FC0000FC0000FC0000FC0000FC0000FC0000FC0 000FC0000FC0000FC0000FC0000FC0000FC0000FC0000FC0000FC0000FC0000FC0000FC07C0FC0 FE0FC0FE0F80FE1F80FE1F007C3E003FF8000FE000123784AA14>I108 DII<003FC00001FFF80007E07E000F801F001F801F803F000FC03F000FC07E0007E07E0007E0 7E0007E0FE0007F0FE0007F0FE0007F0FE0007F0FE0007F0FE0007F0FE0007F0FE0007F07E0007 E07E0007E03F000FC03F000FC01F801F800FC03F0007E07E0001FFF800003FC0001C1B7E9A21> II114 D<03FC601FFFE03C03E07801E07000E0F00060F0 0060F00060FC0000FF00007FFC007FFF003FFFC00FFFE003FFF0003FF00003F8C000F8C00078E0 0078E00078F00078F00070F800E0FE03E0E7FF8081FE00151B7E9A1A>I<006000006000006000 00600000E00000E00001E00001E00003E00007E0001FE000FFFFE0FFFFE007E00007E00007E000 07E00007E00007E00007E00007E00007E00007E00007E00007E00007E00007E00007E03007E030 07E03007E03007E03007E03007E03003F06001F8C000FF80003F0014267FA51A>II119 D121 D E end %%EndProlog %%BeginSetup %%Feature: *Resolution 300 TeXDict begin @a4 %%EndSetup %%Page: 1 1 bop 222 194 a Fu(A)22 b(Simple)e(Pro)r(of)h(of)i(Su\016cien)n(t)d(Conditions) f(for)j(the)284 263 y(T)-6 b(ermination)19 b(of)k(the)e(Disjoin)n(t)f(Union)g (of)i(T)-6 b(erm)632 333 y(Rewriting)20 b(Systems)755 477 y Ft(Enno)14 b(Ohlebusc)o(h)495 564 y Fs(Univ)o(ersit\177)-19 b(at)15 b(Bielefeld,)f(4800)g(Bielefeld)h(1,)e(German)o(y)m(,)594 610 y(e-mail:)h(enno@tec)o(hfak.uni-biel)q(efeld.de)183 739 y Fr(1)56 b(In)n(tro)r(duction)183 833 y Ft(The)19 b(question)g(whether)h(or) f(not)f(prop)q(erties)i(of)e(term)h(rewriting)f(systems)h(\(TRSs)g(for)183 882 y(short\))e(are)g(preserv)o(ed)h(under)g(disjoin)o(t)d(union)940 867 y Fq(1)975 882 y Ft(is)h(a)g(sub)r(ject)i(of)e(in)o(tensiv)o(e)h(curren)o (t)h(re-)183 932 y(searc)o(h.)e(T)m(o)o(y)o(ama)c(sho)o(w)o(ed)k(in)f([T)m(o) o(y87b)n(])g(that)h(con\015uence)h(is)f(preserv)o(ed)h(under)g(disjoin)o(t) 183 982 y(union,)12 b(whereas)k(termination)c(is)i(not)f(preserv)o(ed)j (\(cf.)e([T)m(o)o(y87a)n(]\):)183 1066 y Fp(Example)h(1.1)183 1116 y Ft(The)f(term)e(rewriting)i(systems)g(\()p Fo(F)744 1122 y Fq(1)762 1116 y Fn(;)7 b Fo(R)816 1122 y Fq(1)834 1116 y Ft(\))12 b(=)g(\()p Fo(f)p Ft(0)p Fn(;)7 b Ft(1)p Fn(;)g(F)f Fo(g)p Fn(;)h Fo(f)p Fn(F)e Ft(\(0)p Fn(;)h Ft(1)p Fn(;)h(x)o Ft(\))p Fo(!)m Fn(F)f Ft(\()p Fn(x;)h(x;)g(x)p Ft(\))p Fo(g)p Ft(\),)k(and)183 1166 y(\()p Fo(F)229 1172 y Fq(2)247 1166 y Fn(;)c Fo(R)301 1172 y Fq(2)320 1166 y Ft(\))20 b(=)h(\()p Fo(f)p Fn(g)q Fo(g)p Fn(;)7 b Fo(f)p Fn(g)q Ft(\()p Fn(x;)g(y)q Ft(\))p Fo(!)p Fn(x;)g(g)q Ft(\()p Fn(x;)g(y)q Ft(\))p Fo(!)o Fn(y)q Fo(g)p Ft(\))20 b(are)g(eviden)o(tly)f(terminating)f(but)h(their)183 1216 y(disjoin)o(t)12 b(union)i(is)g(not)f(terminating,)f(for)i(there)h(is)e (the)i(cyclic)f(rewrite)h(deriv)n(ation)204 1295 y Fn(t)c Fo(\021)h Fn(F)6 b Ft(\(0)p Fn(;)h Ft(1)p Fn(;)g(g)q Ft(\(0)p Fn(;)g Ft(1\)\))p Fo(!)572 1301 y Fm(R)601 1305 y Fl(1)619 1295 y Fn(F)f Ft(\()p Fn(g)q Ft(\(0)p Fn(;)h Ft(1\))p Fn(;)g(g)q Ft(\(0)p Fn(;)g Ft(1\))p Fn(;)g(g)q Ft(\(0)p Fn(;)g Ft(1\)\))p Fo(!)1103 1301 y Fm(R)1132 1305 y Fl(2)1150 1295 y Fn(F)f Ft(\(0)p Fn(;)h(g)q Ft(\(0)p Fn(;)g Ft(1\))p Fn(;)g(g)q Ft(\(0)p Fn(;)g Ft(1\)\))p Fo(!)1541 1301 y Fm(R)1570 1305 y Fl(2)1587 1295 y Fn(t)183 1379 y Ft(Naturally)14 b(the)j(question)e(arose)i(what)e(restrictions)i(ha)o (v)o(e)f(to)f(b)q(e)h(imp)q(osed)f(on)g(the)h(con-)183 1429 y(stituen)o(t)d(TRSs)h(so)f(that)g(their)g(disjoin)o(t)g(union)f(is)h(again)f (terminating.)f(The)i(\014rst)h(results)183 1479 y(w)o(ere)e(obtained)g(b)o (y)f(in)o(v)o(estigating)g(the)h(distribution)f(of)g(collapsing)g(rules)h (\(a)g(rewrite)g(rule)183 1528 y(is)h(collapsing)g(if)g(its)h(righ)o(t-hand)g (side)g(is)g(a)f(v)n(ariable\))g(and)h(duplicating)f(rules)i(\(a)f(rewrite) 183 1578 y(rules)e Fn(l)h Fo(!)e Fn(r)i Ft(is)f(duplicating)f(if)g Fn(r)i Ft(con)o(tains)f(more)f(o)q(ccurrences)16 b(of)11 b(some)g(v)n (ariable)g(than)h Fn(l)q Ft(\))183 1628 y(among)h(the)j(TRSs)f(\(note)h(that) f(in)g(the)h(ab)q(o)o(v)o(e)f(example)f Fo(R)1148 1634 y Fq(1)1182 1628 y Ft(consists)i(of)f(a)g(duplicating)183 1678 y(rule,)f(whereas)i Fo(R)471 1684 y Fq(2)504 1678 y Ft(con)o(tains)f(t)o(w)o(o)f(collapsing)g (rules\).)g(These)i(results)g(are)f(stated)h(in)e(the)183 1728 y(next)g(theorem.)183 1812 y Fp(Theorem)g(1.2)21 b Ft(Let)h Fo(R)584 1818 y Fq(1)603 1812 y Fn(;)7 b Fo(R)657 1818 y Fq(2)697 1812 y Ft(b)q(e)22 b(t)o(w)o(o)f(disjoin)o(t)f(terminating)g(TRSs.)h(Their)h (disjoin)o(t)183 1862 y(union)13 b(is)h(terminating)e(pro)o(vided)i(that)g (one)g(of)f(the)h(follo)o(wing)e(conditions)h(is)h(satis\014ed:)200 1939 y(1.)20 b(Neither)15 b Fo(R)437 1945 y Fq(1)470 1939 y Ft(nor)f Fo(R)579 1945 y Fq(2)611 1939 y Ft(con)o(tains)g(collapsing)f (rules.)200 1989 y(2.)20 b(Neither)15 b Fo(R)437 1995 y Fq(1)470 1989 y Ft(nor)f Fo(R)579 1995 y Fq(2)611 1989 y Ft(con)o(tains)g(duplicating) f(rules.)200 2038 y(3.)20 b(One)15 b(of)e(the)i(systems)f(con)o(tains)f (neither)i(collapsing)e(nor)h(duplicating)f(rules.)183 2122 y(Statemen)o(ts)g(1.)f(and)g(2.)h(w)o(ere)h(\014rst)f(pro)o(v)o(ed)g(b)o(y)g (Rusino)o(witc)o(h)f(in)h([Rus87)o(])1356 2107 y Fq(2)1374 2122 y Ft(.)f(The)i(pro)q(of)e(of)183 2172 y(statemen)o(t)k(3.)f(is)i(due)f (to)h(Middeldorp)f([Mid89)n(].)g(All)f Fk(thr)n(e)n(e)h Ft(pro)q(ofs)g (referred)j(to)d(ha)o(v)o(e)g(a)p 183 2206 237 2 v 191 2233 a Fj(1)221 2249 y Fs(If)10 b(\()p Fi(F)300 2253 y Fj(1)316 2249 y Fh(;)c Fi(R)366 2253 y Fj(1)383 2249 y Fs(\))k(and)h(\()p Fi(F)523 2253 y Fj(2)540 2249 y Fh(;)6 b Fi(R)590 2253 y Fj(2)607 2249 y Fs(\))k(are)g(t)o(w)o(o)g(TRSs)g(with)h(disjoin)o(t)h(signatures,)f (then)g(the)f(term)g(rewrit-)221 2295 y(ing)i(system)f(\()p Fi(F)451 2299 y Fj(1)472 2295 y Fi(])t(F)530 2299 y Fj(2)547 2295 y Fh(;)6 b Fi(R)597 2299 y Fj(1)619 2295 y Fi(])t(R)682 2299 y Fj(2)698 2295 y Fs(\))11 b(is)h(called)g(their)g(disjoin)o(t)h(union)f (\(here)g Fi(])e Fs(denotes)i(the)f(union)221 2340 y(of)i(disjoin)o(t)i (sets\).)191 2370 y Fj(2)221 2386 y Fs(Drosten)c(obtained)h(parts)f(of)f (these)h(results)g(indep)q(enden)o(tl)q(y)i({)e(in)g(2.)f(he)g(additional)q (ly)k(required)221 2432 y(righ)o(t-lineari)q(t)o(y)m(,)h(cf.)d([Dro89)q(].)p eop %%Page: 2 2 bop 340 194 a Ft(common)12 b(feature:)i(A)o(t)g(\014rst)h(a)f(sp)q(eci\014c)i (w)o(ell-founded)d(ordering)h Fn(>)g Ft(on)g(terms)g(is)g(de\014ned)340 244 y(and)i(then)h(it)e(is)h(sho)o(wn)g(that)f Fn(>)i Ft(con)o(tains)e(the)i (resp)q(ectiv)o(e)h(rewrite)f(relation.)d(Ho)o(w)o(ev)o(er,)340 293 y(the)i(three)g(pro)q(ofs)f(use)g(di\013eren)o(t)h(w)o(ell-founded)e (orderings.)h(In)g(the)g(sequel)h(w)o(e)f(will)e(giv)o(e)340 343 y Fk(one)f Ft(simple)e(in)o(tuitiv)o(e)g(pro)q(of)g(for)h(1.)f({)h(3.)f (using)h(the)h(minim)o(al)c(coun)o(terexample)i(approac)o(h)340 393 y(\(whic)o(h)15 b(is)g(nothing)f(but)h(induction)f(on)g(the)i(rank)e(of)g (deriv)n(ations\).)g(W)m(e)g(p)q(oin)o(t)h(out)f(that)340 443 y(the)k(pro)q(of)f(w)o(e)h(are)f(going)g(to)g(presen)o(t)i(is)e(only)f(sligh) o(tly)g(longer)h(than)h(the)f(title)h(of)e(this)340 493 y(pap)q(er.)d(F)m(or) f(a)h(comprehensiv)o(e)f(surv)o(ey)i(of)e(more)f(results)j(in)e(this)h (\014eld)f(of)g(term)g(rewriting)340 542 y(w)o(e)j(refer)f(to)g([Mid90)o(].)f (Additionally)m(,)e([Gra92)n(])j(discusses)i(more)c(recen)o(t)k(results.)340 684 y Fr(2)56 b(Preliminaries)340 791 y Fp(2.1)48 b(Basic)16 b(Notions)340 882 y Ft(In)11 b(this)g(section,)g(w)o(e)g(brie\015y)g(recall)g (the)g(basic)g(notions)f(of)g(term)g(rewriting)h(as)g(surv)o(ey)o(ed)h(in)340 931 y(e.g.)i(Dersho)o(witz)h(and)f(Jouannaud)g([DJ90)o(])g(and)g(Klop)g ([Klo92)n(].)g(W)m(e)g(use)h(the)g(notations)340 981 y(suggested)h(in)d ([DJ91)o(].)403 1033 y(A)e Fk(signatur)n(e)f Ft(is)h(a)f(coun)o(table)h(set)h Fo(F)j Ft(of)10 b Fk(function)i(symb)n(ols)f Ft(or)g Fk(op)n(er)n(ators)p Ft(,)f(where)i(ev)o(ery)340 1082 y Fn(f)17 b Fo(2)11 b(F)16 b Ft(is)c(asso)q(ciated)h(with)f(a)g(natural)f(n)o(um)o(b)q(er)h(denoting)g (its)g(arit)o(y)m(.)f Fo(F)1478 1088 y Fg(n)1512 1082 y Ft(denotes)j(the)e (set)340 1132 y(of)f(all)f(function)h(sym)o(b)q(ols)f(of)h(arit)o(y)g Fn(n)p Ft(,)f(hence)j Fo(F)j Ft(=)1147 1101 y Ff(S)1182 1145 y Fg(n)p Fm(\025)p Fq(0)1254 1132 y Fo(F)1284 1138 y Fg(n)1306 1132 y Ft(.)11 b(Elemen)o(ts)g(of)g Fo(F)1581 1138 y Fq(0)1611 1132 y Ft(are)h(called)340 1182 y Fk(c)n(onstants)p Ft(.)k(The)h(set)f Fo(T)11 b Ft(\()p Fo(F)t Fn(;)c Fo(V)s Ft(\))16 b(of)f Fk(terms)g Ft(built)g(from)f(a)i(signature)g Fo(F)k Ft(and)c(a)f(coun)o(table)340 1232 y(set)g(of)d Fk(variables)h Fo(V)k Ft(with)c Fo(F)f(\\)7 b(V)15 b Ft(=)d Fo(;)h Ft(is)g(the)h(smallest)e(set)i(suc)o(h)g(that)f Fo(V)j(\022)c(T)e Ft(\()p Fo(F)t Fn(;)d Fo(V)s Ft(\))13 b(and)340 1282 y(if)h Fn(f)k Fo(2)13 b(F)18 b Ft(has)d(arit)o(y)f Fn(n)h Ft(and)g Fn(t)818 1288 y Fq(1)836 1282 y Fn(;)7 b(:)g(:)g(:)e(;)i(t)944 1288 y Fg(n)979 1282 y Fo(2)13 b(T)d Ft(\()p Fo(F)t Fn(;)d Fo(V)s Ft(\))15 b(then)h Fn(f)t Ft(\()p Fn(t)1332 1288 y Fq(1)1351 1282 y Fn(;)7 b(:)g(:)g(:)e(;)i(t)1459 1288 y Fg(n)1481 1282 y Ft(\))13 b Fo(2)g(T)d Ft(\()p Fo(F)t Fn(;)d Fo(V)s Ft(\).)15 b(W)m(e)340 1331 y(write)f Fn(f)19 b Ft(instead)14 b(of)f Fn(f)t Ft(\()g(\))h(whenev)o(er)h Fn(f)j Ft(is)c(a)f(constan)o(t.)h(Iden)o(tit)o(y)g (of)f(terms)g(and)h(function)340 1381 y(sym)o(b)q(ols)i(is)g(denoted)i(b)o(y) e Fo(\021)p Ft(.)g(F)m(or)g Fn(t)h Fo(2)e(T)10 b Ft(\()p Fo(F)t Fn(;)d Fo(V)s Ft(\))17 b(w)o(e)g(de\014ne)h Fn(r)q(oot)p Ft(\()p Fn(t)p Ft(\))f(b)o(y:)f Fn(r)q(oot)p Ft(\()p Fn(t)p Ft(\))g Fo(\021)h Fn(t)f Ft(if)340 1431 y Fn(t)c Fo(2)f(V)s Ft(,)j(and)g Fn(r)q(oot)p Ft(\()p Fn(t)p Ft(\))e Fo(\021)g Fn(f)18 b Ft(if)13 b Fn(t)f Fo(\021)g Fn(f)t Ft(\()p Fn(t)921 1437 y Fq(1)940 1431 y Fn(;)7 b(:)g(:)g(:)e(;)i(t)1048 1437 y Fg(n)1070 1431 y Ft(\).)403 1482 y(A)k Fk(substitution)h Fn(\033)g Ft(is)f(a)h(mapping)d (from)h Fo(V)15 b Ft(to)c Fo(T)f Ft(\()p Fo(F)t Fn(;)d Fo(V)s Ft(\))12 b(suc)o(h)g(that)g Fo(f)p Fn(x)f Fo(2)g(V)16 b(j)c Fn(\033)q Ft(\()p Fn(x)p Ft(\))p Fo(6\021)p Fn(x)p Fo(g)340 1532 y Ft(is)h(\014nite.)f(Substitutions)h(are)g(extended)h(to)f(morphisms)d (from)h Fo(T)f Ft(\()p Fo(F)t Fn(;)d Fo(V)s Ft(\))13 b(to)f Fo(T)f Ft(\()p Fo(F)t Fn(;)c Fo(V)s Ft(\),)12 b(i.e.)340 1582 y Fn(\033)q Ft(\()p Fn(f)t Ft(\()p Fn(t)436 1588 y Fq(1)456 1582 y Fn(;)7 b(:)g(:)g(:)e(;)i(t)564 1588 y Fg(n)586 1582 y Ft(\)\))22 b Fo(\021)g Fn(f)t Ft(\()p Fn(\033)q Ft(\()p Fn(t)790 1588 y Fq(1)810 1582 y Ft(\))p Fn(;)7 b(:)g(:)g(:)e(;)i(\033)q Ft(\()p Fn(t)975 1588 y Fg(n)997 1582 y Ft(\)\))21 b(for)e(ev)o(ery)i Fn(n)p Ft(-ary)f(function)g(sym)o(b)q(ol)e Fn(f)24 b Ft(and)340 1632 y(terms)14 b Fn(t)471 1638 y Fq(1)490 1632 y Fn(;)7 b(:)g(:)g(:)t(;)g(t) 597 1638 y Fg(n)619 1632 y Ft(.)14 b(W)m(e)f(call)g Fn(\033)q Ft(\()p Fn(t)p Ft(\))i(an)e Fk(instanc)n(e)i Ft(of)e Fn(t)p Ft(.)g(W)m(e)h(also)f(write)h Fn(t\033)h Ft(instead)g(of)e Fn(\033)q Ft(\()p Fn(t)p Ft(\).)403 1683 y(In)c(order)h(to)f(describ)q(e)j (subterm)d(o)q(ccurrences)j(of)d(a)g(term,)g(w)o(e)g(in)o(tro)q(duce)h(the)g (notation-)340 1733 y(ally)15 b(con)o(v)o(enien)o(t)h(notion)g("con)o(text")g (instead)g(of)f(the)i(more)e(precise)i(notion)e("p)q(osition")340 1783 y(\(cf.)e([DJ90)o(]\).)f(Let)h Fe(2)g Ft(b)q(e)h(a)e(sp)q(ecial)h (constan)o(t)h(sym)o(b)q(ol.)c(A)j Fk(c)n(ontext)g Fn(C)s Ft([)p Fn(;)7 b(:)g(:)g(:)t(;)g Ft(])12 b(is)h(a)f(term)h(in)340 1832 y Fo(T)e Ft(\()p Fo(F)d([)d(f)p Fe(2)p Fo(g)p Fn(;)i Fo(V)s Ft(\).)k(If)g Fn(C)s Ft([)p Fn(;)c(:)g(:)g(:)t(;)g Ft(])j(is)i(a)f(con)o (text)h(with)g Fn(n)f Ft(o)q(ccurrences)k(of)c Fe(2)g Ft(and)h Fn(t)1566 1838 y Fq(1)1584 1832 y Fn(;)7 b(:)g(:)g(:)e(;)i(t)1692 1838 y Fg(n)1726 1832 y Ft(are)340 1882 y(terms,)16 b(then)g Fn(C)s Ft([)p Fn(t)626 1888 y Fq(1)644 1882 y Fn(;)7 b(:)g(:)g(:)e(;)i(t)752 1888 y Fg(n)774 1882 y Ft(])15 b(is)h(the)h(result)f(of)g(replacing)g(from)e (left)h(to)h(righ)o(t)g(the)g(o)q(ccur-)340 1932 y(rences)e(of)d Fe(2)h Ft(with)g Fn(t)659 1938 y Fq(1)677 1932 y Fn(;)7 b(:)g(:)g(:)e(;)i(t) 785 1938 y Fg(n)807 1932 y Ft(.)12 b(A)g(con)o(text)g(con)o(taining)f (precisely)i(one)f(o)q(ccurrence)i(of)e Fe(2)f Ft(is)340 1982 y(denoted)k(b)o(y)f Fn(C)s Ft([)e(].)h(A)h(term)g Fn(s)g Ft(is)g(a)g Fk(subterm)f Ft(of)h(a)g(term)f Fn(t)h Ft(if)f(there)j(exists)f(a)e(con)o (text)i Fn(C)s Ft([)d(])340 2032 y(suc)o(h)17 b(that)e Fn(t)f Fo(\021)h Fn(C)s Ft([)p Fn(s)p Ft(].)f(By)h(abuse)h(of)f(notation)g(w)o(e)g (write)h Fo(T)10 b Ft(\()p Fo(F)t Fn(;)d Fo(V)s Ft(\))16 b(for)f Fo(T)c Ft(\()p Fo(F)j([)c(f)p Fe(2)p Fo(g)p Fn(;)d Fo(V)s Ft(\),)340 2082 y(in)o(terpreting)15 b Fe(2)f Ft(as)h(a)f(sp)q(ecial)g(constan)o(t)h (whic)o(h)f(is)g(alw)o(a)o(ys)f(a)o(v)n(ailable)g(but)h(used)h(only)f(for)340 2131 y(the)h(aforemen)o(tioned)e(purp)q(ose.)403 2183 y(A)19 b Fk(term)g(r)n(ewriting)f(system)h Ft(\(TRS)g(for)g(short\))h(is)f(a)g(pair) g(\()p Fo(F)t Fn(;)7 b Fo(R)p Ft(\))19 b(consisting)g(of)g(a)340 2232 y(signature)12 b Fo(F)k Ft(and)11 b(a)h(set)g Fo(R)g(\032)g(T)e Ft(\()p Fo(F)t Fn(;)d Fo(V)s Ft(\))e Fo(\002)g(T)11 b Ft(\()p Fo(F)t Fn(;)c Fo(V)s Ft(\))12 b(of)f Fk(r)n(ewrite)g(rules)g Ft(or)h Fk(r)n(e)n(duction)g(rules)p Ft(.)340 2282 y(Ev)o(ery)k(rewrite)h (rule)e(\()p Fn(l)q(;)7 b(r)q Ft(\))15 b(m)o(ust)g(satisfy)g(the)h(follo)o (wing)c(t)o(w)o(o)j(constrain)o(ts:)h(\(i\))f(the)h(left-)340 2332 y(hand)d(side)f Fn(l)i Ft(is)e(not)g(a)g(v)n(ariable,)f(and)h(\(ii\))g (v)n(ariables)f(o)q(ccurring)i(in)f(the)h(righ)o(t-hand)f(side)g Fn(r)340 2382 y Ft(also)g(o)q(ccur)h(in)f Fn(l)q Ft(.)g(Rewrite)g(rules)h(\() p Fn(l)q(;)7 b(r)q Ft(\))12 b(will)f(b)q(e)i(denoted)g(b)o(y)f Fn(l)h Fo(!)e Fn(r)q Ft(.)g(The)i(rewrite)g(rules)g(of)340 2432 y(a)e(TRS)f(\()p Fo(F)t Fn(;)d Fo(R)p Ft(\))j(de\014ne)h(a)g Fk(r)n(ewrite)f(r)n(elation)f Fo(!)1070 2438 y Fm(R)1111 2432 y Ft(on)h Fo(T)g Ft(\()p Fo(F)t Fn(;)d Fo(V)s Ft(\))k(as)g(follo)o(ws:)d Fn(s)k Fo(!)1587 2438 y Fm(R)1629 2432 y Fn(t)e Ft(if)g(there)p eop %%Page: 3 3 bop 183 194 a Ft(exists)16 b(a)f(rewrite)h(rule)g Fn(l)f Fo(!)f Fn(r)i Ft(in)f Fo(R)p Ft(,)g(a)g(substitution)h Fn(\033)g Ft(and)g(a)f(con)o (text)h Fn(C)s Ft([)11 b(])k(suc)o(h)h(that)183 244 y Fn(s)f Fo(\021)g Fn(C)s Ft([)p Fn(l)q(\033)q Ft(])g(and)h Fn(t)f Fo(\021)g Fn(C)s Ft([)p Fn(r)q(\033)q Ft(].)f(The)j(transitiv)o(e-re\015exiv)o(e)f (closure)h(of)e Fo(!)1331 250 y Fm(R)1377 244 y Ft(is)h(denoted)h(b)o(y)183 293 y Fo(!)225 278 y Fm(\003)225 305 y(R)255 293 y Ft(.)9 b(W)m(e)h(often)g (simply)d(write)k Fo(R)f Ft(instead)g(of)f(\()p Fo(F)t Fn(;)e Fo(R)p Ft(\))j(if)f(there)i(is)f(no)f(am)o(biguit)o(y)e(ab)q(out)j(the)183 343 y(underlying)h(signature)i Fo(F)t Ft(.)e(A)i(rewrite)g(rule)f Fn(l)h Fo(!)e Fn(r)i Ft(is)f(called)g Fk(c)n(ol)r(lapsing)g Ft(if)f(its)h(righ)o(t-hand)183 393 y(side)i Fn(l)h Ft(is)f(a)g(v)n(ariable,) e(and)i(it)f(is)h(called)g Fk(duplic)n(ating)g Ft(if)f Fn(r)i Ft(con)o(tains)f(more)f(o)q(ccurrences)k(of)183 443 y(some)9 b(v)n(ariable)g(than)i Fn(l)q Ft(.)f(W)m(e)g(call)f Fn(s)j Fo(!)777 449 y Fm(R)819 443 y Fn(t)e Ft(a)g Fk(r)n(ewrite)g(step)g Ft(or)h Fk(r)n(e)n(duction)g(step)p Ft(.)f(A)h(reduction)183 493 y(step)h(is)g(called)g Fk(duplic)n(ating)g Ft(if)f(the)h(applied)f (rewrite)i(rule)f(is)g(duplicating.)e(A)i(TRS)g(\()p Fo(F)t Fn(;)7 b Fo(R)p Ft(\))183 542 y(is)13 b Fk(terminating)p Ft(,)g(if)f(there)j (is)f(no)f(in\014nite)g(rewrite)i(deriv)n(ation)d Fn(t)1192 548 y Fq(1)1222 542 y Fo(!)1264 548 y Fm(R)1306 542 y Fn(t)1321 548 y Fq(2)1351 542 y Fo(!)1393 548 y Fm(R)1435 542 y Fn(t)1450 548 y Fq(3)1480 542 y Fo(!)1522 548 y Fm(R)1564 542 y Fn(:)7 b(:)g(:)n Ft(.)245 593 y(A)j Fk(p)n(artial)h(or)n(dering)f Ft(\()p Fn(A;)d(>)p Ft(\))k(is)f(a)h(pair)f(consisting)g(of)g(a)g(set)h Fn(A)g Ft(and)f(a)h(binary)f(transitiv)o(e)183 643 y(and)i(irre\015exiv)o(e)i (relation)e Fn(>)h Ft(on)g Fn(A)p Ft(.)f(A)h(partial)f(ordering)h(is)g (called)g Fk(wel)r(l-founde)n(d)f Ft(if)g(there)183 693 y(are)i(no)g (in\014nite)f(sequences)k Fn(a)661 699 y Fq(1)691 693 y Fn(>)12 b(a)757 699 y Fq(2)787 693 y Fn(>)g(a)853 699 y Fq(3)883 693 y Fn(>)f(:)c(:)g(:)13 b Ft(of)g(elemen)o(ts)h(from)e Fn(A)p Ft(.)183 742 y(W)m(e)e(will)g(also)g(need)i(the)f(notion)f(m)o(ultiset)g (ordering.)g(A)h Fk(multiset)f Ft(is)h(a)g(collection)f(in)h(whic)o(h)183 792 y(elemen)o(ts)k(are)g(allo)o(w)o(ed)f(to)i(o)q(ccur)g(more)e(than)h (once.)h(If)f Fn(A)g Ft(is)g(a)g(set,)h(then)g(the)g(set)g(of)f(all)183 842 y(\014nite)f(m)o(ultisets)f(o)o(v)o(er)h Fn(A)g Ft(is)g(denoted)h(b)o(y)e Fo(M)p Ft(\()p Fn(A)p Ft(\).)h(The)h Fk(multiset)f(extension)g Ft(of)g(a)g(partial)183 892 y(ordering)g(\()p Fn(A;)7 b(>)p Ft(\))14 b(is)f(the)i(partial)e(ordering)h(\()p Fo(M)p Ft(\()p Fn(A)p Ft(\))p Fn(;)7 b(>)1066 877 y Fg(mul)1128 892 y Ft(\))14 b(de\014ned)h(as)f(follo)o(ws:)183 942 y Fn(M)223 948 y Fq(1)260 942 y Fn(>)292 927 y Fg(mul)373 942 y Fn(M)413 948 y Fq(2)449 942 y Ft(if)k Fn(M)532 948 y Fq(2)569 942 y Ft(=)h(\()p Fn(M)676 948 y Fq(1)707 942 y Fo(\000)12 b Fn(X)s Ft(\))h Fo(])e Fn(Y)28 b Ft(for)17 b(some)h(m)o(ultisets)f Fn(X)q(;)7 b(Y)27 b Fo(2)18 b(M)p Ft(\()p Fn(A)p Ft(\))g(that)183 991 y(satisfy)d(\(i\))g Fo(;)g(6)p Ft(=)g Fn(X)j Fo(\022)c Fn(M)594 997 y Fq(1)629 991 y Ft(and)h(\(ii\))g(for)h(all)e Fn(y)i Fo(2)f Fn(Y)25 b Ft(there)17 b(exists)f(an)f Fn(x)g Fo(2)f Fn(X)19 b Ft(suc)o(h)d(that)183 1041 y Fn(x)c(>)h(y)q Ft(.)h(Dersho)o(witz)h(and)g(Manna)f(pro)o(v)o(ed)h(in) f([DM79)n(])g(that)h(the)g(m)o(ultiset)e(extension)i(of)183 1091 y(a)e(w)o(ell-founded)g(ordering)h(is)g(a)g(w)o(ell-founded)f(ordering.) 183 1219 y Fp(2.2)47 b(Disjoin)o(t)12 b(Unions)183 1306 y Ft(Next)18 b(w)o(e)f(giv)o(e)g(a)g(brief)h(o)o(v)o(erview)f(of)g(the)h(basic)f(notions)g (of)g(disjoin)o(t)g(unions)g(of)g(TRSs)183 1356 y(\(see)j([T)m(o)o(y87b)n(,)f (Mid90)o(]\).)g(Let)h(\()p Fo(F)745 1362 y Fq(1)763 1356 y Fn(;)7 b Fo(R)817 1362 y Fq(1)835 1356 y Ft(\))20 b(and)f(\()p Fo(F)1003 1362 y Fq(2)1022 1356 y Fn(;)7 b Fo(R)1076 1362 y Fq(2)1094 1356 y Ft(\))19 b(b)q(e)h(t)o(w)o(o)f(disjoin)o(t)f(TRSs,)h(i.e.,) 183 1405 y Fo(F)213 1411 y Fq(1)239 1405 y Fo(\\)8 b(F)305 1411 y Fq(2)335 1405 y Ft(=)k Fo(;)p Ft(.)h(The)h(TRS)f(\()p Fo(F)653 1411 y Fq(1)680 1405 y Fo(])8 b(F)746 1411 y Fq(2)764 1405 y Fn(;)f Fo(R)818 1411 y Fq(1)845 1405 y Fo(])h(R)916 1411 y Fq(2)935 1405 y Ft(\))13 b(is)g(called)h(their)f Fk(disjoint)i(union)p Ft(;)e(w)o(e)h(will)183 1455 y(simply)d(write)k Fo(R)457 1461 y Fq(1)485 1455 y Fo(])9 b(R)557 1461 y Fq(2)589 1440 y(3)608 1455 y Ft(.)245 1506 y(In)14 b(the)h(sequel)g(let)f Fn(t)e Fo(2)g(T)e Ft(\()p Fo(F)699 1512 y Fq(1)727 1506 y Fo(])g(F)795 1512 y Fq(2)813 1506 y Fn(;)d Fo(V)s Ft(\).)14 b(Let)h Fn(t)d Fo(\021)g Fn(C)s Ft([)p Fn(t)1108 1512 y Fq(1)1126 1506 y Fn(;)7 b(:)g(:)g(:)e(;)i(t)1234 1512 y Fg(n)1256 1506 y Ft(])14 b(with)g Fn(C)s Ft([)p Fn(;)7 b(:)g(:)g(:)t(;)g Ft(])k Fo(6\021)h Fe(2)p Ft(.)183 1556 y(W)m(e)h(write)h Fn(t)d Fo(\021)h Fn(C)s Ft([)-7 b([)p Fn(t)495 1562 y Fq(1)513 1556 y Fn(;)7 b(:)g(:)g(:)t(;)g(t)620 1562 y Fg(n)642 1556 y Ft(])-7 b(])13 b(if)g Fn(C)s Ft([)p Fn(;)7 b(:)g(:)g(:)t(;)g Ft(])j Fo(2)i(T)e Ft(\()p Fo(F)988 1562 y Fg(j)1005 1556 y Fn(;)d Fo(V)s Ft(\))14 b(and)g Fn(r)q(oot)p Ft(\()p Fn(t)1269 1562 y Fq(1)1288 1556 y Ft(\))p Fn(;)7 b(:)g(:)g(:)e(r)q (oot)p Ft(\()p Fn(t)1484 1562 y Fg(n)1506 1556 y Ft(\))12 b Fo(2)f(F)1603 1562 y Fg(k)183 1605 y Ft(for)j(some)g Fn(j;)7 b(k)13 b Fo(2)g(f)p Ft(1)p Fn(;)7 b Ft(2)p Fo(g)13 b Ft(with)h Fn(j)i Fo(6)p Ft(=)d Fn(k)q Ft(.)h(In)h(this)g(case)g(w)o(e)g(de\014ne)h(the) g(m)o(ultiset)d Fn(S)r Ft(\()p Fn(t)p Ft(\))j(of)e(all)183 1655 y Fk(princip)n(al)f Ft(subterms)h(of)f Fn(t)h Ft(to)g(b)q(e)h Fn(S)r Ft(\()p Fn(t)p Ft(\))d(=)g([)p Fn(t)873 1661 y Fq(1)891 1655 y Fn(;)7 b(:)g(:)g(:)e(;)i(t)999 1661 y Fg(n)1021 1655 y Ft(])1033 1640 y Fq(4)1051 1655 y Ft(.)13 b(Moreo)o(v)o(er,)h(w)o(e)h (de\014ne)f(for)g(all)f Fn(t)246 1770 y(r)q(ank)q Ft(\()p Fn(t)p Ft(\))f(=)439 1711 y Ff(\032)476 1744 y Ft(1)554 b(,)14 b(if)f Fn(t)e Fo(2)g(T)g Ft(\()p Fo(F)1260 1750 y Fq(1)1278 1744 y Fn(;)c Fo(V)s Ft(\))j Fo([)f(T)h Ft(\()p Fo(F)1467 1750 y Fq(2)1486 1744 y Fn(;)d Fo(V)s Ft(\))476 1794 y(1)i(+)g Fn(max)p Fo(f)p Fn(r)q(ank)q Ft(\()p Fn(t)771 1800 y Fg(j)788 1794 y Ft(\))20 b Fo(j)f Ft(1)11 b Fo(\024)h Fn(j)i Fo(\024)e Fn(n)p Fo(g)p Ft(,)h(if)g Fn(t)e Fo(\021)h Fn(C)s Ft([)-7 b([)p Fn(t)1250 1800 y Fq(1)1267 1794 y Fn(;)7 b(:)g(:)g(:)e(;)i(t)1375 1800 y Fg(n)1397 1794 y Ft(])-7 b(])183 1884 y(The)17 b(topmost)e(homogeneous)h (part)h(of)f Fn(t)p Ft(,)g(denoted)h(b)o(y)g Fn(top)p Ft(\()p Fn(t)p Ft(\),)f(is)h(obtained)f(from)f Fn(t)i Ft(b)o(y)183 1934 y(replacing)c(all)g(principal)g(subterms)h(with)g Fe(2)p Ft(,)f(i.e.,)553 2046 y Fn(top)p Ft(\()p Fn(t)p Ft(\))f(=)712 1988 y Ff(\032)748 2021 y Fn(t)145 b Ft(if)11 b Fn(r)q(ank)q Ft(\()p Fn(t)p Ft(\))g(=)h(1)748 2071 y Fn(C)s Ft([)p Fn(;)7 b(:)g(:)g(:)t(;)g Ft(])k(if)g Fn(t)g Fo(\021)h Fn(C)s Ft([)-7 b([)p Fn(t)1079 2077 y Fq(1)1097 2071 y Fn(;)7 b(:)g(:)g(:)t(;)g(t)1204 2077 y Fg(n)1226 2071 y Ft(])-7 b(])183 2160 y(F)m(rom)7 b(no)o(w)i(on)h Fo(!)f Ft(denotes)h Fo(!)661 2166 y Fm(R)690 2170 y Fl(1)706 2166 y Fm(]R)757 2170 y Fl(2)775 2160 y Ft(.)f(A)g(reduction)i(step)f Fn(s)i Fo(!)f Fn(t)e Ft(is)h(called)f Fk(inner)g Ft(\(denoted)183 2210 y(b)o(y)16 b Fn(s)h Fo(!)321 2195 y Fg(i)351 2210 y Fn(t)p Ft(\),)f(if)g(the)h(reduction)h(tak)o(es)f(place)g(in)f(one)h(of)f(the)i (principal)d(subterms)i(of)g Fn(s)p Ft(.)183 2260 y(Otherwise,)i(w)o(e)g(sp)q (eak)g(of)f(an)g Fk(outer)g Ft(reduction)h(step)h(and)e(write)h Fn(s)g Fo(!)1365 2245 y Fg(o)1402 2260 y Fn(t)p Ft(.)f(A)h(rewrite)p 183 2298 237 2 v 191 2325 a Fj(3)221 2340 y Fs(Other)13 b(authors)h(use)f (the)h(notation)g Fi(R)790 2344 y Fj(1)816 2340 y Fi(\010)8 b(R)887 2344 y Fj(2)917 2340 y Fs(and)13 b(call)i(it)e(the)g(direct)h(sum)g (of)e Fi(R)1433 2344 y Fj(1)1463 2340 y Fs(and)i Fi(R)1571 2344 y Fj(2)1588 2340 y Fs(.)191 2370 y Fj(4)221 2386 y Fs(In)f(order)f(to)h (distinguish)j(m)o(ultisets)e(from)e(sets,)h(w)o(e)f(use)g(brac)o(k)o(ets)i (instead)g(of)e(braces)h(for)f(the)221 2432 y(former.)p eop %%Page: 4 4 bop 340 194 a Ft(step)18 b Fn(s)f Fo(!)f Fn(t)g Ft(is)h Fk(destructive)g(at)h (level)f(1)g Ft(if)e Fn(r)q(oot)p Ft(\()p Fn(s)p Ft(\))j Fo(2)e(F)1258 200 y Fg(j)1292 194 y Ft(and)g Fn(r)q(oot)p Ft(\()p Fn(t)p Ft(\))h Fo(2)f(F)1588 200 y Fg(k)1625 194 y Ft(for)g(some)340 244 y Fn(j;)7 b(k)18 b Fo(2)f(f)p Ft(1)p Fn(;)7 b Ft(2)p Fo(g)16 b Ft(with)h Fn(j)j Fo(6)p Ft(=)e Fn(k)q Ft(.)f(A)g(reduction)i(step)f Fn(s)g Fo(!)f Fn(t)g Ft(is)g Fk(destructive)h(at)g(level)f Fn(n)12 b Ft(+)g(1)340 293 y(\(for)17 b(some)f Fn(n)g Fo(\025)g Ft(1\))h(if)e Fn(s)i Fo(\021)f Fn(C)s Ft([)-7 b([)p Fn(s)866 299 y Fq(1)884 293 y Fn(;)7 b(:)g(:)g(:)e(;)i(s)996 299 y Fg(j)1014 293 y Fn(;)g(:)g(:)g(:)t(;)g(s)1125 299 y Fg(n)1148 293 y Ft(])-7 b(])15 b Fo(!)1222 278 y Fg(i)1252 293 y Fn(C)s Ft([)p Fn(s)1316 299 y Fq(1)1334 293 y Fn(;)7 b(:)g(:)g(:)e(;)i(t)1442 299 y Fg(j)1459 293 y Fn(;)g(:)g(:)g(:)t(;)g(s)1570 299 y Fg(n)1593 293 y Ft(])16 b Fo(\021)g Fn(t)h Ft(with)340 343 y Fn(s)359 349 y Fg(j)393 343 y Fo(!)d Fn(t)464 349 y Fg(j)498 343 y Ft(destructiv)o(e)k (at)d(lev)o(el)h Fn(n)p Ft(.)g(Ob)o(viously)m(,)e(if)h(a)h(rewrite)h(step)g (is)f(destructiv)o(e,)i(then)340 393 y(the)d(applied)e(rewrite)i(rule)f(is)g (collapsing.)340 525 y Fr(3)56 b(The)19 b(Simple)d(Pro)r(of)340 623 y Ft(W)m(e)e(omit)e(the)i(pro)q(ofs)g(of)f(the)i(next)f(lemmata)d(whic)o (h)j(are)g(routine.)340 712 y Fp(Lemma)i(3.1)k Ft(If)14 b Fn(s)e Fo(!)706 697 y Fm(\003)736 712 y Fn(t)p Ft(,)h(then)i Fn(r)q(ank)q Ft(\()p Fn(s)p Ft(\))d Fo(\025)g Fn(r)q(ank)q Ft(\()p Fn(t)p Ft(\).)340 801 y Fp(Lemma)k(3.2)k Ft(If)c Fn(s)h Fo(!)713 786 y Fg(o)747 801 y Fn(t)f Ft(is)g(a)g(non-destructiv)o(e)i(non-duplicating)d (rewrite)j(step,)f(then)340 851 y(the)e(m)o(ultiset)d(inclusion)i Fn(S)r Ft(\()p Fn(t)p Ft(\))e Fo(\022)g Fn(S)r Ft(\()p Fn(s)p Ft(\))j(holds.)340 940 y Fp(Lemma)h(3.3)k Ft(If)14 b Fn(s)f Fo(\021)f Fn(C)s Ft([)-7 b([)p Fn(s)778 946 y Fq(1)796 940 y Fn(;)7 b(:)g(:)g(:)e(;)i(s)908 946 y Fg(j)925 940 y Fn(;)g(:)g(:)g(:)e(;)i (s)1037 946 y Fg(n)1060 940 y Ft(])-7 b(])11 b Fo(!)1130 925 y Fg(i)1155 940 y Fn(C)s Ft([)p Fn(s)1219 946 y Fq(1)1237 940 y Fn(;)c(:)g(:)g(:)e(;)i(t)1345 946 y Fg(j)1362 940 y Fn(;)g(:)g(:)g(:)e(;)i (s)1474 946 y Fg(n)1496 940 y Ft(])12 b Fo(\021)g Fn(t)j Ft(is)f(destruc-)340 989 y(tiv)o(e)g(at)g(lev)o(el)f(t)o(w)o(o,)g(then)i Fn(S)r Ft(\()p Fn(t)p Ft(\))e(=)e(\()p Fn(S)r Ft(\()p Fn(s)p Ft(\))g Fo(\000)f Ft([)p Fn(s)1059 995 y Fg(j)1076 989 y Ft(]\))f Fo([)g Fn(S)r Ft(\()p Fn(t)1208 995 y Fg(j)1227 989 y Ft(\).)340 1078 y Fp(De\014nition)j(3.4)21 b Ft(F)m(or)16 b(an)o(y)f(rewrite)i(deriv)n(ation) e Fn(D)i Ft(:)d Fn(s)1238 1084 y Fq(1)1272 1078 y Fo(!)h Fn(s)1348 1084 y Fq(2)1382 1078 y Fo(!)f Fn(s)1457 1084 y Fq(3)1491 1078 y Fo(!)h Fn(:)7 b(:)g(:)14 b Ft(w)o(e)i(de\014ne)340 1128 y(the)f(rank)f(of)f Fn(D)i Ft(to)f(b)q(e)h Fn(r)q(ank)q Ft(\()p Fn(D)q Ft(\))d(=)f Fn(min)p Fo(f)p Fn(r)q(ank)q Ft(\()p Fn(s)1145 1134 y Fg(j)1164 1128 y Ft(\))h Fo(j)g Fn(j)i Fo(2)d Ft(\()p Fd(I)-6 b(N)10 b Fo(\000)g(f)p Ft(0)p Fo(g)p Ft(\))p Fo(g)p Ft(.)340 1217 y(Eviden)o(tly)m(,)i(in)g(the)i(situation)e(of)g(the)h(ab)q(o)o(v)o(e)g (de\014nition)f(w)o(e)h(ha)o(v)o(e)g Fn(r)q(ank)q Ft(\()p Fn(D)q Ft(\))f Fo(\024)g Fn(r)q(ank)q Ft(\()p Fn(s)1735 1223 y Fq(1)1754 1217 y Ft(\).)340 1267 y(Statemen)o(ts)18 b(1.)e(and)h(2.)f(of)h(the)h(next)f (lemma)d(app)q(eared)k(for)f(the)h(\014rst)g(time)e(in)g(Gram-)340 1317 y(lic)o(h)e([Gra92)o(],)f(although)h(they)h(ha)o(v)o(e)f(b)q(een)h (implicitly)d(in)i(man)o(y)e(earlier)j(w)o(orks)f(\(see)i(e.g.)340 1366 y([TKB89]\).)d(Statemen)o(t)h(3.)f(is)g(the)i(in)o(teresting)f(part;)g (it)g(is)f(the)i(essence)h(of)d(our)h(pro)q(of.)340 1455 y Fp(Lemma)i(3.5)k Ft(Let)15 b Fo(R)701 1461 y Fq(1)720 1455 y Fn(;)7 b Fo(R)774 1461 y Fq(2)806 1455 y Ft(b)q(e)14 b(t)o(w)o(o)g (terminating)e(disjoin)o(t)h(TRSs)g(suc)o(h)i(that)848 1539 y Fn(D)e Ft(:)e Fn(s)937 1545 y Fq(1)967 1539 y Fo(!)g Fn(s)1039 1545 y Fq(2)1070 1539 y Fo(!)g Fn(s)1142 1545 y Fq(3)1173 1539 y Fo(!)g Fn(:)c(:)g(:)340 1622 y Ft(is)13 b(an)g(in\014nite)g(rewrite)h (deriv)n(ation)e(of)h(minim)o(al)c(rank)k(w.r.t.)f Fo(R)1359 1628 y Fq(1)1386 1622 y Fo(])7 b(R)1456 1628 y Fq(2)1475 1622 y Ft(,)12 b(i.e.,)g(an)o(y)g(rewrite)340 1672 y(deriv)n(ation)h(w.r.t.)g Fo(R)681 1678 y Fq(1)709 1672 y Fo(])c(R)781 1678 y Fq(2)814 1672 y Ft(of)k(smaller)f(rank)i(is)g(\014nite.)g(Then)g(w)o(e)g(ha)o(v)o(e:) 358 1753 y(1.)20 b(There)15 b(are)f(in\014nitely)f(man)o(y)f(outer)j (reduction)g(steps)g(in)e(D.)358 1803 y(2.)20 b(There)d(are)f(in\014nitely)e (man)o(y)g(inner)i(reduction)g(steps)h(in)e(D)g(whic)o(h)h(are)g(destructiv)o (e)411 1853 y(at)e(lev)o(el)f(t)o(w)o(o.)358 1902 y(3.)20 b(There)15 b(are)f(in\014nitely)f(man)o(y)f(duplicating)h(outer)i(reduction)f(steps)i (in)d(D.)340 1983 y Fp(Pro)q(of:)c Ft(First)h(of)g(all)e(notice)i(that)g Fn(r)q(ank)q Ft(\()p Fn(s)1002 1989 y Fg(j)1020 1983 y Ft(\))h(=)h Fn(r)q(ank)q Ft(\()p Fn(D)q Ft(\))e(for)g(all)e(indices)j Fn(j)r Ft(.)e(In)h(particular,)340 2033 y(there)22 b(is)e(no)g(reduction)h(step)g (whic)o(h)f(is)g(destructiv)o(e)i(at)e(lev)o(el)g(1.)f(Moreo)o(v)o(er,)h (w.l.o.g.)340 2083 y Fn(r)q(oot)p Ft(\()p Fn(s)450 2089 y Fg(j)469 2083 y Ft(\))11 b Fo(2)g(F)565 2089 y Fq(1)598 2083 y Ft(for)i(an)o(y)h Fn(j)r Ft(.)340 2133 y(1.)c(Supp)q(ose)g(that)g(only)g(a)f(\014nite)h(n)o(um) o(b)q(er)g(of)f(reduction)i(steps)g(in)f(D)f(are)i(outer)f(ones.)g(Then,)340 2183 y(without)g(loss)g(of)g(generalit)o(y)m(,)f(w)o(e)h(ma)o(y)e(further)j (assume)f(that)g(there)i(is)e(no)g(outer)h(reduction)340 2232 y(step)19 b(in)f(D.)f(Th)o(us,)g(if)g Fn(s)727 2238 y Fq(1)764 2232 y Fo(\021)i Fn(C)s Ft([)-7 b([)p Fn(t)880 2238 y Fq(1)897 2232 y Fn(;)7 b(:)g(:)g(:)e(;)i(t)1005 2238 y Fg(n)1027 2232 y Ft(])-7 b(],)16 b(then)j(there)g(m)o(ust)e(b)q(e)h(an)g(in\014nite)f (rewrite)340 2282 y(deriv)n(ation)g(starting)g(from)f(some)g Fn(t)921 2288 y Fg(l)951 2282 y Fo(2)h Fn(S)r Ft(\()p Fn(s)1058 2288 y Fq(1)1078 2282 y Ft(\).)g(But)h(this)f(con)o(tradicts)h(the)g(minima)o (li)o(t)o(y)340 2332 y(assumption)13 b(on)h Fn(r)q(ank)q Ft(\()p Fn(D)q Ft(\))g(since)h Fn(r)q(ank)q Ft(\()p Fn(t)1012 2338 y Fg(l)1024 2332 y Ft(\))d Fn(<)g(r)q(ank)q Ft(\()p Fn(s)1221 2338 y Fq(1)1239 2332 y Ft(\).)340 2382 y(2.)17 b(As)i(ab)q(o)o(v)o(e)e(supp) q(ose)i(that)f(no)f(inner)h(reduction)h(step)f(in)g(D)f(is)h(destructiv)o(e)h (at)f(lev)o(el)340 2432 y(t)o(w)o(o.)f(In)h(this)g(case)h(w)o(e)f(ha)o(v)o(e) f(for)h(an)o(y)f(outer)h(reduction)h(step)g Fn(s)1393 2438 y Fg(j)1429 2432 y Fo(!)1471 2417 y Fg(o)1507 2432 y Fn(s)1526 2438 y Fg(j)r Fq(+1)1603 2432 y Ft(in)f(D)f(that)p eop %%Page: 5 5 bop 183 194 a Fn(top)p Ft(\()p Fn(s)274 200 y Fg(j)292 194 y Ft(\))11 b Fo(!)361 200 y Fm(R)390 204 y Fl(1)419 194 y Fn(top)p Ft(\()p Fn(s)510 200 y Fg(j)r Fq(+1)570 194 y Ft(\))g(using)f(the)g(same)g (rule)g(from)f Fo(R)1079 200 y Fq(1)1107 194 y Ft(and)i(for)e(ev)o(ery)i (inner)g(reduction)183 244 y(step)k Fn(s)290 250 y Fg(j)321 244 y Fo(!)363 228 y Fg(i)389 244 y Fn(s)408 250 y Fg(j)r Fq(+1)482 244 y Ft(w)o(e)g(ha)o(v)o(e)g Fn(top)p Ft(\()p Fn(s)732 250 y Fg(j)750 244 y Ft(\))d Fo(\021)h Fn(top)p Ft(\()p Fn(s)914 250 y Fg(j)r Fq(+1)975 244 y Ft(\).)h(Hence)i(w)o(e)f(conclude)g(b)o(y)f(1.)g (that)h Fo(R)1605 250 y Fq(1)183 293 y Ft(is)e(non-terminating,)f(a)h(con)o (tradiction.)183 343 y(3.)j(Let)h(\()p Fd(I)-6 b(N)p Fn(;)7 b(>)p Ft(\))17 b(denote)g(the)h(usual)e(w)o(ell-founded)g(ordering)h(on)f (natural)g(n)o(um)o(b)q(ers)h(and)183 393 y(\()p Fo(M)p Ft(\()p Fd(I)-6 b(N)p Ft(\))p Fn(;)7 b(>)367 378 y Fg(mul)429 393 y Ft(\))14 b(its)g(w)o(ell-founded)f(m)o(ultiset)f(extension.)j(W)m(e)e (de\014ne)597 475 y Fn(]s)f Ft(=)g([)p Fn(r)q(ank)q Ft(\()p Fn(t)p Ft(\))g Fo(j)g Fn(t)f Fo(2)g Fn(S)r Ft(\()p Fn(s)p Ft(\)])i Fo(2)e(M)p Ft(\()p Fd(I)-6 b(N)q Ft(\))p Fn(;)183 556 y Ft(i.e.,)12 b Fn(]s)i Ft(denotes)i(the)e(m)o(ultiset)f(of)g(the)h(ranks)h(of)e(the)h (principal)f(subterms)i(of)e Fn(s)p Ft(.)183 606 y(As)g(in)g(the)h(pro)q(of)f (of)g(1.,)f(w)o(e)h(ma)o(y)f(supp)q(ose)i(that)g(there)g(is)f(no)g (duplicating)g(outer)h(rewrite)183 656 y(step)h(in)e(D.)g(W)m(e)h (distinguish)f(b)q(et)o(w)o(een)i(three)g(cases:)209 735 y Fp({)20 b Ft(If)k Fn(s)324 741 y Fg(j)370 735 y Fo(!)412 720 y Fg(o)458 735 y Fn(s)477 741 y Fg(j)r Fq(+1)537 735 y Ft(,)g(then)h(b)o(y)e (Lemma)f(3.2)h Fn(S)r Ft(\()p Fn(s)1043 741 y Fg(j)r Fq(+1)1104 735 y Ft(\))28 b Fo(\022)h Fn(S)r Ft(\()p Fn(s)1271 741 y Fg(j)1290 735 y Ft(\))24 b(b)q(ecause)h(the)g(re-)253 785 y(duction)20 b(step)h(is)f(non-destructiv)o(e)h(and)e(non-duplicating.)f(Clearly)m(,)h (this)h(implies)253 835 y Fn(]s)288 841 y Fg(j)318 835 y Fo(\025)350 820 y Fg(mul)423 835 y Fn(]s)458 841 y Fg(j)r Fq(+1)519 835 y Ft(.)209 935 y Fp({)g Ft(If)15 b Fn(s)315 941 y Fg(j)346 935 y Fo(\021)f Fn(C)s Ft([)-7 b([)p Fn(t)457 941 y Fq(1)475 935 y Fn(;)7 b(:)g(:)g(:)t(;)g(t)582 941 y Fg(k)602 935 y Fn(;)g(:)g(:)g(:)e (;)i(t)710 941 y Fg(n)732 935 y Ft(])-7 b(])13 b Fo(!)804 920 y Fg(i)831 935 y Fn(C)s Ft([)-7 b([)p Fn(t)896 941 y Fq(1)913 935 y Fn(;)7 b(:)g(:)g(:)e(;)i(t)1021 920 y Fm(0)1021 946 y Fg(k)1041 935 y Fn(;)g(:)g(:)g(:)t(;)g(t)1148 941 y Fg(n)1170 935 y Ft(])-7 b(])13 b Fo(\021)h Fn(s)1265 941 y Fg(j)r Fq(+1)1325 935 y Ft(,)g(where)j Fn(t)1488 941 y Fg(k)1522 935 y Fo(!)c Fn(t)1592 920 y Fm(0)1592 946 y Fg(k)1612 935 y Ft(,)253 984 y(then)i(also)e Fn(]s)466 990 y Fg(j)496 984 y Fo(\025)528 969 y Fg(mul)601 984 y Fn(]s)636 990 y Fg(j)r Fq(+1)710 984 y Ft(since)i Fn(r)q(ank)q Ft(\()p Fn(t)933 990 y Fg(k)953 984 y Ft(\))d Fo(\025)g Fn(r)q(ank)q Ft(\()p Fn(t)1146 969 y Fm(0)1146 996 y Fg(k)1166 984 y Ft(\).)209 1084 y Fp({)20 b Ft(If)15 b Fn(s)315 1090 y Fg(j)347 1084 y Fo(!)389 1069 y Fg(i)417 1084 y Fn(s)436 1090 y Fg(j)r Fq(+1)511 1084 y Ft(is)g(destructiv)o(e)i(at)f (lev)o(el)f(t)o(w)o(o,)f(i.e.,)g Fn(s)1107 1090 y Fg(j)1139 1084 y Fo(\021)g Fn(C)s Ft([)-7 b([)p Fn(t)1250 1090 y Fq(1)1268 1084 y Fn(;)7 b(:)g(:)g(:)e(;)i(t)1376 1090 y Fg(k)1395 1084 y Fn(;)g(:)g(:)g(:)e(;)i(t)1503 1090 y Fg(n)1525 1084 y Ft(])-7 b(])15 b(and)253 1134 y Fn(s)272 1140 y Fg(j)r Fq(+1)345 1134 y Fo(\021)f Fn(C)s Ft([)p Fn(t)451 1140 y Fq(1)469 1134 y Fn(;)7 b(:)g(:)g(:)e(;)i(t)577 1119 y Fm(0)577 1146 y Fg(k)596 1134 y Fn(;)g(:)g(:)g(:)e(;)i(t)704 1140 y Fg(n)726 1134 y Ft(])15 b(suc)o(h)g(that)g Fn(t)953 1140 y Fg(k)987 1134 y Fo(!)e Fn(t)1057 1119 y Fm(0)1057 1146 y Fg(k)1092 1134 y Ft(is)i(destructiv)o(e)h(at)f(lev)o (el)g(1,)f(then)253 1184 y(b)o(y)19 b(Lemma)e(3.3)h(w)o(e)i(ha)o(v)o(e)f Fn(S)r Ft(\()p Fn(s)772 1190 y Fg(j)r Fq(+1)833 1184 y Ft(\))h(=)h(\()p Fn(S)r Ft(\()p Fn(s)1000 1190 y Fg(j)1019 1184 y Ft(\))13 b Fo(\000)g Ft([)p Fn(t)1120 1190 y Fg(k)1140 1184 y Ft(]\))g Fo([)f Fn(S)r Ft(\()p Fn(t)1279 1169 y Fm(0)1279 1195 y Fg(k)1300 1184 y Ft(\).)19 b(It)h(follo)o(ws)d(from)253 1233 y Fn(r)q(ank)q Ft(\()p Fn(t)374 1239 y Fg(k)394 1233 y Ft(\))d Fn(>)g(r)q(ank)q Ft(\()p Fn(t)591 1218 y Fm(0)591 1245 y Fg(k)611 1233 y Ft(\))h(in)g (conjunction)g(with)g Fn(r)q(ank)q Ft(\()p Fn(t)1135 1218 y Fm(0)1135 1245 y Fg(k)1155 1233 y Ft(\))f Fn(>)g(r)q(ank)q Ft(\()p Fn(u)p Ft(\))g(for)h(an)o(y)g(prin-)253 1283 y(cipal)e(subterm)h Fn(u)d Fo(2)h Fn(S)r Ft(\()p Fn(t)647 1268 y Fm(0)647 1295 y Fg(k)668 1283 y Ft(\))i(that)g Fn(]s)823 1289 y Fg(j)853 1283 y Fn(>)885 1268 y Fg(mul)958 1283 y Fn(]s)993 1289 y Fg(j)r Fq(+1)1053 1283 y Ft(.)183 1363 y(W)m(e)c(conclude)i(from)d(the)i(w)o (ell-foundedness)h(of)e(\()p Fo(M)p Ft(\()p Fd(I)-6 b(N)p Ft(\))p Fn(;)7 b(>)1124 1348 y Fg(mul)1186 1363 y Ft(\))k(that)g(only)f(\014nitely)g (man)o(y)183 1413 y(inner)j(reduction)g(steps)i(whic)o(h)d(are)i(destructiv)o (e)g(at)f(lev)o(el)f(t)o(w)o(o)h(can)g(o)q(ccur)h(in)e(the)i(consid-)183 1462 y(ered)h(deriv)n(ation)e Fn(D)q Ft(.)h(This)f(con)o(tradicts)i(statemen) o(t)f(2.)f Fe(2)183 1549 y Fp(Theorem)h(3.6)21 b Ft(Let)f Fo(R)582 1555 y Fq(1)601 1549 y Fn(;)7 b Fo(R)655 1555 y Fq(2)693 1549 y Ft(b)q(e)20 b(t)o(w)o(o)f(disjoin)o(t)f(terminating)g(TRSs)h(suc)o(h)i (that)e(their)183 1599 y(disjoin)o(t)d(union)g Fo(R)487 1605 y Fq(1)517 1599 y Fo(])11 b(R)591 1605 y Fq(2)627 1599 y Ft(is)17 b(non-terminating.)d(Then)k Fo(R)1140 1605 y Fg(j)1174 1599 y Ft(is)f(duplicating)f(and)h Fo(R)1558 1605 y Fg(k)1596 1599 y Ft(is)183 1649 y(collapsing)12 b(for)i(some)f Fn(j;)7 b(k)12 b Fo(2)f(f)p Ft(1)p Fn(;)c Ft(2)p Fo(g)12 b Ft(with)i Fn(j)g Fo(6)p Ft(=)e Fn(k)q Ft(.)183 1699 y Fp(Pro)q(of:)h Ft(This)g(is)h(an)g (immedia)o(te)e(consequence)k(of)d(Lemma)f(3.5.)g Fe(2)183 1785 y Ft(No)o(w)h(Theorem)h(1.2)e(is)i(a)g(corollary)f(of)g(Theorem)g(3.6.) 183 1885 y Fp(Ac)o(kno)o(wledgemen)o(t)o(s:)c Ft(The)k(author)f(is)g (grateful)f(to)h(Rob)q(ert)h(Giegeric)o(h)f(for)f(commen)o(ts)183 1935 y(on)i(a)h(previous)g(v)o(ersion)g(of)f(the)i(pap)q(er.)183 2066 y Fr(References)207 2158 y Fs([DJ90])21 b(N.)12 b(Dersho)o(witz)18 b(and)f(J.P)m(.)f(Jouannaud.)29 b(Rewrite)18 b(Systems.)28 b(In)17 b(L.)12 b(v)n(an)17 b(Leeu)o(w)o(en,)337 2203 y(editor,)c Fc(Handb)n(o)n(ok)e(of)h(The)n(or)n(etic)n(al)g(Computer)g(Scienc)n(e,)f(V)m (ol.)h(B)p Fs(,)h(c)o(hapter)g(6.)g(North-)337 2249 y(Holland,)h(1990.)207 2295 y([DJ91])21 b(N.)12 b(Dersho)o(witz)i(and)g(J.P)m(.)e(Jouannaud.)20 b(Notations)14 b(for)f(Rewriting.)19 b Fc(Bul)r(letin)12 b(of)i(the)337 2340 y(EA)m(TCS)f Fb(43)p Fs(,)g(pages)h(162{172,)g(F)m(ebruary)g(1991.)192 2386 y([DM79])21 b(N.)12 b(Dersho)o(witz)h(and)f(Z.)h(Manna.)k(Pro)o(ving)d (T)m(ermination)f(with)g(Multiset)g(Orderings.)337 2432 y Fc(Communic)n (ations)e(of)i(the)g(A)o(CM)h Fb(22)p Fc(\(8\))p Fs(,)d(pages)j(465{476,)g (1979.)p eop %%Page: 6 6 bop 350 194 a Fs([Dro89])21 b(K.)12 b(Drosten.)22 b Fc(T)m (ermersetzungssyste)o(me)p Fs(.)c(Informatik-F)m(ac)o(h)o(b)q(eric)o(h)o(te)f Fb(210)p Fs(,)d(Springer)494 239 y(V)m(erlag,)g(1989.)350 285 y([Gra92])20 b(B.)13 b(Gramlic)o(h.)25 b(Generalized)17 b(Su\016cien)o(t)g (Conditions)g(for)e(Mo)q(dular)i(T)m(ermination)f(of)494 331 y(Rewriting.)i(In)12 b Fc(Pr)n(o)n(c)n(e)n(e)n(dings)d(of)i(the)h(Thir)n(d)f (International)e(Confer)n(enc)n(e)h(on)h(A)o(lgebr)n(aic)494 376 y(and)16 b(L)n(o)n(gic)f(Pr)n(o)n(gr)n(amming)p Fs(.)g(Lecture)h(Notes)g (in)h(Computer)f(Science)i Fb(632)p Fs(,)d(Springer)494 422 y(V)m(erlag,)f(1992.)354 468 y([Klo92])21 b(J.W.)g(Klop.)40 b(T)m(erm)20 b(Rewriting)j(Systems.)40 b(In)21 b(S.)13 b(Abramsky)m(,)21 b(D.)12 b(Gabba)o(y)m(,)21 b(and)494 513 y(T.)12 b(Maibaum,)i(editors,)g Fc(Handb)n(o)n(ok)c(of)j(L)n(o)n(gic)f(in)h(Computer)g(Scienc)n(e,)d(V)m(ol.) j(II)p Fs(,)e(pages)494 559 y(1{112.)j(Oxford)f(Univ)o(ersit)o(y)i(Press,)e (1992.)347 605 y([Mid89])21 b(A.)12 b(Middeldorp)q(.)18 b(A)11 b(Su\016cien)o(t)h(Condition)i(for)c(the)h(T)m(ermination)i(of)e(the)g (Direct)h(Sum)494 650 y(of)j(T)m(erm)f(Rewriting)j(Systems.)23 b(In)15 b Fc(Pr)n(o)n(c)n(e)n(e)n(dings)e(of)h(the)h(4th)f(IEEE)i(Symp)n (osium)d(on)494 696 y(L)n(o)n(gic)g(in)g(Computer)g(Scienc)n(e)p Fs(,)d(pages)k(396{401,)f(1989.)347 742 y([Mid90])21 b(A.)12 b(Middeldorp)q(.)20 b Fc(Mo)n(dular)12 b(Pr)n(op)n(erties)g(of)h(T)m(erm)i(R) n(ewriting)d(Systems)p Fs(.)k(PhD)d(thesis,)494 787 y(F)m(ree)g(Univ)o(ersit) o(y)i(Amsterdam,)e(1990.)349 833 y([Rus87])21 b(M.)13 b(Rusino)o(witc)o(h.)20 b(On)14 b(T)m(ermination)h(of)e(the)h(Direct)g(Sum)g(of)g(T)m(erm)f (Rewriting)i(Sys-)494 879 y(tems.)i Fc(Information)12 b(Pr)n(o)n(c)n(essing)f (L)n(etters)h Fb(26)p Fs(,)h(pages)h(65{70,)f(1987.)340 924 y([TKB89])21 b(Y.)12 b(T)m(o)o(y)o(ama,)d(J.W.)g(Klop,)h(and)g(H.P)f (Barendregt.)16 b(T)m(ermination)11 b(for)f(the)f(Direct)i(Sum)494 970 y(of)16 b(Left-Linear)h(T)m(erm)e(Rewriting)i(Systems.)26 b(In)16 b Fc(Pr)n(o)n(c)n(e)n(e)n(dings)e(of)h(the)h(3r)n(d)g(Interna-)494 1016 y(tional)c(Confer)n(enc)n(e)g(on)h(R)n(ewriting)f(T)m(e)n(chniques)f (and)i(Applic)n(ation)o(s)p Fs(,)c(pages)14 b(477{491.)494 1061 y(Lecture)g(Notes)f(in)h(Computer)f(Science)h Fb(355)p Fs(,)f(Springer)i(V)m(erlag,)e(1989.)340 1107 y([T)m(o)o(y87a])21 b(Y.)12 b(T)m(o)o(y)o(ama.)27 b(Coun)o(terexamples)19 b(to)d(T)m(ermination)i (for)f(the)f(Direct)i(Sum)f(of)f(T)m(erm)494 1153 y(Rewriting)f(Systems.)i Fc(Information)11 b(Pr)n(o)n(c)n(essing)g(L)n(etters)h Fb(25)p Fs(,)h(pages)g(141{143,)h(1987.)340 1198 y([T)m(o)o(y87b])21 b(Y.)12 b(T)m(o)o(y)o(ama.)30 b(On)18 b(the)f(Ch)o(urc)o(h-Rosser)i(Prop)q (ert)o(y)f(for)g(the)f(Direct)i(Sum)e(of)h(T)m(erm)494 1244 y(Rewriting)d(Systems.)j Fc(Journal)12 b(of)h(the)g(A)o(CM)h Fb(34)p Fc(\(1\))p Fs(,)d(pages)j(128{143,)g(1987.)340 2420 y(This)g(article)g(w)o(as)f(pro)q(cessed)i(using)f(the)f(L)968 2415 y Fa(a)986 2420 y Fs(T)1008 2432 y(E)1029 2420 y(X)f(macro)h(pac)o(k)n (age)h(with)g(LLNCS)e(st)o(yle)p eop %%Trailer end userdict /end-hook known{end-hook}if %%EOF