%!PS-Adobe-2.0 %%Creator: dvips 5.516 Copyright 1986, 1993 Radical Eye Software %%Title: final.dvi %%CreationDate: Fri Oct 21 14:19:23 1994 %%Pages: 6 %%PageOrder: Ascend %%BoundingBox: 0 0 596 842 %%EndComments %DVIPSCommandLine: dvips -o final.ps final.dvi %DVIPSSource: TeX output 1994.10.21:1418 %%BeginProcSet: tex.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 4 get round 4 exch put dup dup 5 get round 5 exch put 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 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 /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 showpage userdict /eop-hook known{eop-hook}if}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 product dup length 7 ge{0 7 getinterval dup(Display)eq exch 0 4 getinterval(NeXT)eq or}{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 /QV{gsave 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 TeXDict begin 39158280 55380996 1000 300 300 (/amnt/fauna/users/id2f/pistaff/enno/TEX/IPL/final.dvi) @start /Fa 1 98 df<00600000600000F00000F00000F000013800013800013800021C 00021C00040E00040E0007FE000807000807001003801003803803C0FC0FF014137F9217 >97 D E /Fb 6 54 df<07F0001E3C003C1E00380E00780F00780F00780F00F80F80F80F 80F80F80F80F80F80F80F80F80F80F80F80F80F80F80F80F80F80F80780F00780F00380E 003C1E001E3C0007F00011187E9716>48 D<00C003C0FFC0FFC003C003C003C003C003C0 03C003C003C003C003C003C003C003C003C003C003C003C003C07FFE7FFE0F187D9716> I<0FF0003FFC00787E00FC1F00FC1F80FC0F80FC0F80780F80001F80001F00001E00003C 0000780000700000E0000180000301800601800C01801003803FFF007FFF00FFFF00FFFF 0011187E9716>I<07F0001FFC00383E007C3E007C1F007C1F007C1F00383F00003E0000 3C0000780007F000003C00001E00001F00001F80781F80FC1F80FC1F80FC1F00F81F0070 3E003FFC000FF00011187E9716>I<000600000E00001E00003E00007E0000DE00019E00 011E00031E00061E000C1E00181E00301E00601E00C01E00FFFFE0FFFFE0001E00001E00 001E00001E00001E0001FFE001FFE013187F9716>I<3006003FFC003FFC003FF0003FE0 003F800030000030000030000037F000381C00301E00000F00000F00000F80700F80F80F 80F80F80F80F80F80F00601F00383E001FF80007E00011187E9716>I E /Fc 44 123 df<000400180030006000C0008001800300030006000E000C001C001800 180038003000300070007000600060006000E000E000E000C000C000C000C000C0006000 6000600020003000100008000E267B9B10>40 D<00400060002000300010001800180018 00180018001800180018001800180018003800380030003000700070006000E000C000C0 01C0018003800300060006000C00180010002000400080000D267F9B10>I<1838783808 101020204080050B7D830C>44 DI<3078F06005047C830C> I<000800180030007001F00E7000E000E000E000E001C001C001C001C003800380038003 8007000700070007000F00FFF00D187C9714>49 D<003E0000C3000101800201800481C0 0441C0088380048380070300000600000C0001F000001800000C00000C00000E00000E00 600E00E01C00E01C0080380040300020E0001F800012187D9714>51 D<0000200000600000600000E00001E00001E00002700002700004700008700008700010 7000107000207000207000407000807000FFF00100380100380200380400380400380C00 381C0038FF01FF181A7E991D>65 D<03FFF800700E00700600700700E00700E00700E007 00E00701C00E01C01C01C03801C07003FFE003807003803803801C07001C07001C07001C 07001C0E00380E00380E00700E00E01C03C0FFFF00181A7D991B>I<000F8200706200C0 1603801E07000C0E000C1C000C18000C380008300008700000700000E00000E00000E000 00E00000E00020E00020E00020E000406000406000803001001006000C180003E000171A 7A991B>I<03FFFF00700700700300700100E00100E00100E00100E00101C08001C08001 C08001C18003FF000381000381000381000702000700040700040700080E00080E00180E 00100E00301C00E0FFFFE0181A7D991A>69 D<03FF1FF800700380007003800070038000 E0070000E0070000E0070000E0070001C00E0001C00E0001C00E0001C00E0003FFFC0003 801C0003801C0003801C00070038000700380007003800070038000E0070000E0070000E 0070000E0070001C00E000FFC7FE001D1A7D991D>72 D<01FF8000380000380000380000 700000700000700000700000E00000E00000E00000E00001C00001C00001C00001C00003 80000380000380000380000700000700000700000700000E0000FFE000111A7E990F>I< 00FFC0000E00000E00000E00001C00001C00001C00001C00003800003800003800003800 00700000700000700000700000E00000E00000E00000E00061C000E1C000E18000838000 4700003C0000121A7C9914>I<03FF8000700000700000700000E00000E00000E00000E0 0001C00001C00001C00001C0000380000380000380000380000700000700100700100700 200E00200E00600E00400E00C01C0380FFFF80141A7D9918>76 D<03F8001FC00078003C 000078003C000078005C0000B800B80000B800B800009C013800009C013800011C027000 011C027000011C047000011C087000021C08E000021C10E000021C10E000021C20E00004 1C41C000041C41C000041C81C000041C81C000080F038000080F038000080E038000180C 038000380C070000FF083FF000221A7D9922>I<03FFF800701C00700600700700E00700 E00700E00700E00701C00E01C00E01C01C01C03803807003FF8003800003800007000007 00000700000700000E00000E00000E00000E00001C0000FFC000181A7D991A>80 D<03FFF000701C00700E00700700E00700E00700E00700E00701C00E01C01C01C03801C0 E003FF800380C00380600380700700700700700700700700700E00E00E00E00E00E10E00 E21C0062FFC03C181A7D991C>82 D<003F10006090018070010070030020060020060020 06002006000007000007C00003F80001FE00007F00000F80000380000180000180200180 200180600300600300600600700C00C8180087E000141A7D9916>I<3FFFFC381C0C201C 04401C0440380480380480380480380400700000700000700000700000E00000E00000E0 0000E00001C00001C00001C00001C000038000038000038000038000078000FFF800161A 79991B>I86 D<03CC0E2E181C381C301C701CE038E038E038E038C072C072C07260 F261341E180F107C8F14>97 D<7E000E000E000E001C001C001C001C00380038003BC03C 307830701870187018E038E038E038E038C070C060C0E060C063801E000D1A7C9912>I< 01F006080C181838301070006000E000E000E000E000E008E010602030C01F000D107C8F 12>I<001F80000380000380000380000700000700000700000700000E00000E0003CE00 0E2E00181C00381C00301C00701C00E03800E03800E03800E03800C07200C07200C07200 60F2006134001E1800111A7C9914>I<01E006181C08380870087010FFE0E000E000E000 E000E0086010602030C01F000D107C8F12>I<000700001980001B80003B000030000030 0000700000700000700000700007FF0000E00000E00000E00000E00000E00001C00001C0 0001C00001C00001C0000380000380000380000380000380000700000700000700006600 00E40000CC0000700000112181990C>I<00F300038B800607000E07000C07001C070038 0E00380E00380E00380E00301C00301C00301C00183C0018780007B80000380000380000 7000607000E0E000C1C0007F000011177E8F12>I<1F8000038000038000038000070000 0700000700000700000E00000E00000E7C000F86001E07001E07001C07001C0700380E00 380E00380E00381C00701C80701C80703880703900E01900600E00111A7E9914>I<0307 06000000000000384C4E8E9C9C1C3838707272E2E4643808197C980C>I<1F8003800380 038007000700070007000E000E000E0E0E131C271C431C801F003C003F8039C038E070E2 70E270E270E4E0646038101A7E9912>107 D<3F0707070E0E0E0E1C1C1C1C3838383870 707070E4E4E4E46830081A7D990A>I<307C1E00598663009E0783809E0703809C070380 9C070380380E0700380E0700380E0700380E0E00701C0E40701C0E40701C1C40701C1C80 E0380C80601807001A107C8F1F>I<307C005986009E07009E07009C07009C0700380E00 380E00380E00381C00701C80701C80703880703900E01900600E0011107C8F16>I<01F0 06180C0C180E300E700E600EE00EE00EE00CE01CE018E030606030C01F000F107C8F14> I<030F000590C009E0C009C06009C06009C0600380E00380E00380E00380E00701C00701 800703800703000E8E000E78000E00000E00001C00001C00001C00001C0000FF00001317 808F14>I<03C20E2E181C381C301C701CE038E038E038E038C070C070C07060F061E01E E000E000E001C001C001C001C01FF00F177C8F12>I<30F059189E389C189C009C003800 3800380038007000700070007000E00060000D107C8F10>I<03E004300830187018601C 001F801FC00FE000E00060E060E06080C041803E000C107D8F10>I<06000E000E000E00 0E001C001C00FFC01C0038003800380038007000700070007000E100E100E100E2006400 38000A177C960D>I<38064C074E0E8E0E9C0E9C0E1C1C381C381C381C70397039703930 79389A0F0C10107C8F15>I<380C304C0E384E1C388E1C189C1C189C1C181C3810383810 38381038381070702070702070704030704018B8800F0F0015107C8F19>119 D<38064C074E0E8E0E9C0E9C0E1C1C381C381C381C703870387038307838F00F70007000 6060E0E1C0C18047003C0010177C8F13>121 D<038207C40FFC10081010002000400180 030004000808100820187FF043E081C00F107E8F10>I E /Fd 3 111 df<0060007000600000000000000000038004C0046008C008C000C000C001800180 0180018003000300030003006600E600CC0078000C1A81930E>106 D<3E0006000C000C000C000C001800187018B819383230340038003E0063006310631063 10C320C1C00D147E9312>I<30F8590C4E0C9C0C980C180C180C30183019303130316032 601C100D7F8C15>110 D E /Fe 1 51 df<7FFFFCFFFFFEC00006C00006C00006C00006 C00006C00006C00006C00006C00006C00006C00006C00006C00006C00006C00006C00006 C00006C00006C00006FFFFFEFFFFFE17177C991F>50 D E /Ff 1 50 df<0C003C00CC000C000C000C000C000C000C000C000C000C000C000C000C00FF8009 107E8F0F>49 D E /Fg 21 127 df<0000000000200000000000600000000000C0000000 000180000000000300000000000600000000000C00000000001800000000003000000000 00600000000000C0000000000180000000000300000000000600000000000C0000000000 180000000000300000000000600000000000C00000000001800000000003000000000006 00000000000C0000000000180000000000300000000000600000000000C0000000000180 000000000300000000000600000000000C00000000001800000000003000000000006000 00000000C0000000000180000000000300000000000600000000000C0000000000180000 000000300000000000600000000000C000000000008000000000002B2C80AA2A>0 D<0000000000600000000001E0000000000780000000001E0000000000780000000001E0 000000000780000000001E0000000000780000000001E0000000000780000000001E0000 000000780000000001E0000000000780000000001E0000000000780000000001E0000000 000780000000001E0000000000780000000000E000000000008000000000002B1780952A >8 D<0100018003C003E003F007F807FC07FE0FFF0FFC1FE01F003C0070006000800010 10808F2A>I<0000000000600000000003E0000000001F8000000000FC0000000007E000 0000003F0000000001F8000000000FC0000000007E0000000003F0000000001F80000000 00FC0000000007E0000000003F0000000000F80000000000C000000000002B10808E2A> 16 D<00000000800000000180000000030000000006000000000C000000000C00000000 1800000000300000000060000000006000000000C0000000018000000001800000000300 00000006000000000C000000000C00000000180000000030000000006000000000600000 0000C000000001800000000300000000030000000006000000000C000000001800000000 180000000030000000006000000000C000000000C0000000018000000003000000000300 00000006000000000C000000001800000000180000000030000000006000000000C00000 00004000000000212C81AA1F>19 D<0030007000F800F801FC03FC07FE0FFE1FFF3FFF7F 008000100C7F8B2A>25 D<0000000000600000000000E000000000018000000000070000 0000000E0000000000180000000000700000000000E00000000003800000000007000000 00000C0000000000380000000000700000000000C0000000000380000000000700000000 000C0000000000380000000000700000000000C000000000038000000000070000000000 0C0000000000380000000000700000000001C0000000000380000000000600000000001C 0000000000380000000000600000000000C000000000008000000000002B21809F2A>I< 000800001800003C00007C0000FC0001FE0007FE000FFE001FFF007FFF00FFFF00000180 110C7F8A2A>41 D<0400060007000FC00FE00FF00FFC1FFE1FF81FE03F803F003C007800 6000400080000F1180901F>47 D<00400000600000E00000F00001F80001FC0003FC0007 FE0007FF000FFF801FFC001FC0003E0000700000800000110F808E2A>61 D63 D<800000000000C000000000006000000000003000000000001800000000000C0000 00000006000000000003000000000001800000000000C000000000006000000000003000 000000001800000000000C000000000006000000000003000000000001800000000000C0 00000000006000000000003000000000001800000000000C000000000006000000000003 000000000001800000000000C00000000000600000000000300000000000180000000000 0C000000000006000000000003000000000001800000000000C000000000006000000000 003000000000001800000000000C00000000000600000000000300000000000180000000 0000C00000000000600000000000202B2C80AA2A>I<800000000000E000000000007800 000000001E000000000007800000000001E000000000007800000000001E000000000007 800000000001E000000000007800000000001E000000000007800000000001E000000000 007800000000001E000000000007800000000001E000000000007800000000001E000000 000007800000000001E00000000000602B1780952A>72 D<800000000000F00000000000 7E00000000000FC00000000001F800000000003F000000000007E00000000000FC000000 00001F800000000003F000000000007E00000000000FC00000000001F800000000003F00 0000000007E00000000000E02B10808E2A>80 D<0080018003C007C00FC01FE03FE07FE0 FFF03FF007F800F8003C000E000600011010668F2A>82 D<4000000000C0000000006000 0000003000000000180000000018000000000C0000000006000000000300000000030000 0000018000000000C000000000C000000000600000000030000000001800000000180000 00000C00000000060000000003000000000300000000018000000000C000000000600000 00006000000000300000000018000000000C000000000C00000000060000000003000000 000180000000018000000000C00000000060000000006000000000300000000018000000 000C000000000C000000000600000000030000000001800000000080212C81AA1F>I<80 0000000000C000000000006000000000003800000000001C000000000006000000000003 800000000001C000000000007000000000003800000000000C0000000000070000000000 03800000000000C000000000007000000000003800000000000C00000000000700000000 0003800000000000C000000000007000000000003800000000000C000000000007000000 000003800000000000E000000000007000000000001800000000000E0000000000070000 00000001800000000000E00000000000602B21809F2A>90 D<0C000E001F001F003F803F C07FE07FF0FFF8FFFC00FE0001100C678B2A>106 D<0800000C00001E00001F00001F80 003FC0003FF0003FF8007FFC007FFF007FFF80C00000110C688A2A>113 D<004000C001C007E00FE01FE07FE0FFF03FF00FF003F801F80078003C000C000400020F 1170901F>119 D<0100000300000380000780000FC0001FC0001FE0003FF0007FF000FF F8001FFC0001FC00003E00000700000080110F678E2A>126 D E /Fh 25 122 df<0001FDC000070FC0000C0FC0001C0F80001C0380003803800038038000 38070000380700003807000070070007FFFE0000700E0000700E0000700E0000E01C0000 E01C0000E01C0000E01C0000E0380001C0380001C0380001C0380001C0710001C0710003 807100038072000380320003801C0003800000030000000700000006000000C6000000E4 000000CC000000700000001A25819C18>13 D45 D<3078F06005047C830D>I<01FFF800003C0E0000380700003803800038038000380380 00700780007007800070078000700F0000E00E0000E01C0000E0700000FFC00001C0C000 01C0600001C0700001C07000038070000380700003807000038070000700F0000700F040 0700F0400700F0800F007880FFE0790000001E001A1D7D9B1E>82 D<000F8400304C00403C0080180100180300180300180600100600100600000700000700 0003E00003FC0001FF00007F800007C00001C00001C00000C00000C02000C02000C06001 80600180600300600200F00400CC180083E000161E7D9C17>I<1FFFFFC01C0701C0300E 00C0200E0080600E0080400E0080401C0080801C0080801C0080001C0000003800000038 000000380000003800000070000000700000007000000070000000E0000000E0000000E0 000000E0000001C0000001C0000001C0000001C0000003C000007FFE00001A1C799B1E> I<03CC063C0C3C181C3838303870387038E070E070E070E070E0E2C0E2C0E261E462643C 380F127B9115>97 D<3F00070007000E000E000E000E001C001C001C001C0039C03E6038 3038307038703870387038E070E070E070E060E0E0C0C0C1C0618063003C000D1D7B9C13 >I<01F007080C08181C3838300070007000E000E000E000E000E000E008E010602030C0 1F000E127B9113>I<001F80000380000380000700000700000700000700000E00000E00 000E00000E0003DC00063C000C3C00181C00383800303800703800703800E07000E07000 E07000E07000E0E200C0E200C0E20061E4006264003C3800111D7B9C15>I<01E007100C 1018083810701070607F80E000E000E000E000E000E0086010602030C01F000D127B9113 >I<0003C0000670000C70001C60001C00001C0000380000380000380000380000380003 FF8000700000700000700000700000700000E00000E00000E00000E00000E00001C00001 C00001C00001C00001C000038000038000038000030000030000070000C60000E60000CC 00007800001425819C0D>I<00F3018F030F06070E0E0C0E1C0E1C0E381C381C381C381C 383830383038187818F00F700070007000E000E0C0C0E1C0C3007E00101A7D9113>I<01 800380010000000000000000000000000000001C002600470047008E008E000E001C001C 001C0038003800710071007100720072003C00091C7C9B0D>105 D<1F800380038007000700070007000E000E000E000E001C001C001C001C003800380038 0038007000700070007000E400E400E400E40068003800091D7C9C0B>108 D<3C1E0780266318C04683A0E04703C0E08E0380E08E0380E00E0380E00E0380E01C0701 C01C0701C01C0701C01C070380380E0388380E0388380E0708380E0710701C0320300C01 C01D127C9122>I<3C3C002646004687004707008E07008E07000E07000E07001C0E001C 0E001C0E001C1C00381C40381C40383840383880701900300E0012127C9117>I<01E007 180C0C180C380C300E700E700EE01CE01CE01CE018E038E030E06060C031801E000F127B 9115>I<07870004D98008E0C008E0C011C0E011C0E001C0E001C0E00381C00381C00381 C00381800703800703000707000706000E8C000E70000E00000E00001C00001C00001C00 001C00003C0000FF8000131A7F9115>I<3C3C26C2468747078E068E000E000E001C001C 001C001C0038003800380038007000300010127C9112>114 D<01F006080C080C1C1818 1C001F001FC00FF007F0007800386030E030C030806060C01F000E127D9111>I<00C001 C001C001C00380038003800380FFE00700070007000E000E000E000E001C001C001C001C 00384038403840388019000E000B1A7D990E>I<1E0300270700470700470700870E0087 0E000E0E000E0E001C1C001C1C001C1C001C1C003838803838801838801839001C590007 8E0011127C9116>I<1E06270E470E4706870287020E020E021C041C041C041C08180838 08181018200C4007800F127C9113>I<1E03270747074707870E870E0E0E0E0E1C1C1C1C 1C1C1C1C38383838183818381C7007F00070007000E0E0C0E1C0818047003C00101A7C91 14>121 D E /Fi 5 63 df<0000700001F00003C0000780000E00001C00003800007000 00700000F00000E00000E00000E00000E00000E00000E00000E00000E00000E00000E000 00E00000E00000E00000E00000E00000E00000E00000E00000E00000E00000E00000E000 00E00000E00000E00000E00000E00000E00000E00000E00001C00001C00001C000038000 0700000600000E0000380000700000C000007000003800000E0000060000070000038000 01C00001C00001C00000E00000E00000E00000E00000E00000E00000E00000E00000E000 00E00000E00000E00000E00000E00000E00000E00000E00000E00000E00000E00000E000 00E00000E00000E00000E00000E00000E00000E00000E00000E00000F000007000007000 003800001C00000E000007800003C00001F000007014637B811F>26 D<0018007800F001E003C007800F001F001E003E003C007C007C007800F800F800F800F8 00F800F800F800F800F800F800F800F800F800F800F800F800F800F800F800F800F800F8 00F8000D25707E25>56 D58 D<007C007C007C007C007C007C007C00 7C007C007C007C007C007C007C007C007C007C007C007C007C007C007C007C007C00F800 F800F800F001F001E003E003C0078007000E001C003800F000C000F00038001C000E0007 00078003C003E001E001F000F000F800F800F8007C007C007C007C007C007C007C007C00 7C007C007C007C007C007C007C007C007C007C007C007C007C007C007C007C0E4D798025 >60 D62 D E /Fj 2 51 df<18F818181818181818181818FF080D7D8C0E>49 D<3E00418080C0C0C000C000 C0018003000400084030407F80FF800A0D7E8C0E>I E /Fk 2 83 df<040004000400C460E4E03F800E003F80E4E0C4600400040004000B0D7E8D11>3 D<03FFF0000FFFF80030E07C0060C03C00C0C01C0081C0180001C0180001C0300001C020 000180C000018F0000039E0000030F0000030F8000070780000603C0000603E0800C01F1 000C00FE001800780019147F931D>82 D E /Fl 31 121 df<78FCFCFCFC7806067D850D >46 D<00600001E0000FE000FFE000F3E00003E00003E00003E00003E00003E00003E000 03E00003E00003E00003E00003E00003E00003E00003E00003E00003E00003E00003E000 03E00003E0007FFF807FFF80111B7D9A18>49 D<07F8001FFE00383F80780FC0FC07C0FC 07E0FC03E0FC03E07803E00007E00007C00007C0000F80001F00001E0000380000700000 E0000180600300600600600800E01FFFC03FFFC07FFFC0FFFFC0FFFFC0131B7E9A18>I< 03F8001FFE003C1F003C0F807C07C07E07C07C07C03807C0000F80000F80001E00003C00 03F800001E00000F800007C00007C00007E03007E07807E0FC07E0FC07E0FC07C0780F80 781F001FFE0007F800131B7E9A18>I<000180000380000780000F80001F80003F80006F 8000CF80008F80018F80030F80060F800C0F80180F80300F80600F80C00F80FFFFF8FFFF F8000F80000F80000F80000F80000F80000F8001FFF801FFF8151B7F9A18>I<78FCFCFC FC7800000000000078FCFCFCFC7806127D910D>58 D<00038000000380000007C0000007 C0000007C000000FE000000FE000001FF000001BF000001BF0000031F8000031F8000061 FC000060FC0000E0FE0000C07E0000C07E0001803F0001FFFF0003FFFF8003001F800300 1F8006000FC006000FC00E000FE00C0007E0FFC07FFEFFC07FFE1F1C7E9B24>65 D<001FE02000FFF8E003F80FE007C003E00F8001E01F0000E03E0000E03E0000607E0000 607C000060FC000000FC000000FC000000FC000000FC000000FC000000FC000000FC0000 007C0000607E0000603E0000603E0000C01F0000C00F80018007C0030003F80E0000FFFC 00001FE0001B1C7D9B22>67 D69 D76 D80 D<0FF8001C1E003E0F803E07803E07C0 1C07C00007C0007FC007E7C01F07C03C07C07C07C0F807C0F807C0F807C0780BC03E13F8 0FE1F815127F9117>97 D<03FC000E0E001C1F003C1F00781F00780E00F80000F80000F8 0000F80000F80000F800007800007801803C01801C03000E0E0003F80011127E9115>99 D<000FF0000FF00001F00001F00001F00001F00001F00001F00001F00001F00001F001F9 F00F07F01C03F03C01F07801F07801F0F801F0F801F0F801F0F801F0F801F0F801F07801 F07801F03C01F01C03F00F0FFE03F9FE171D7E9C1B>I<01FC000F07001C03803C01C078 01C07801E0F801E0F801E0FFFFE0F80000F80000F800007800007C00603C00601E00C00F 038001FC0013127F9116>I<007F0001E38003C7C00787C00F87C00F83800F80000F8000 0F80000F80000F8000FFF800FFF8000F80000F80000F80000F80000F80000F80000F8000 0F80000F80000F80000F80000F80000F80000F80007FF8007FF800121D809C0F>I<03F8 F00E0F381E0F381C07303C07803C07803C07803C07801C07001E0F000E0E001BF8001000 001800001800001FFF001FFFC00FFFE01FFFF07801F8F00078F00078F000787000707800 F01E03C007FF00151B7F9118>I<1E003F003F003F003F001E0000000000000000000000 0000FF00FF001F001F001F001F001F001F001F001F001F001F001F001F001F001F00FFE0 FFE00B1E7F9D0E>105 D<007800FC00FC00FC00FC007800000000000000000000000003 FC03FC007C007C007C007C007C007C007C007C007C007C007C007C007C007C007C007C00 7C007C707CF87CF878F8F070E01F800E26839D0F>II III<01FC000F07801C01C03C01E07800F07800F0F800F8 F800F8F800F8F800F8F800F8F800F87800F07800F03C01E01E03C00F078001FC0015127F 9118>II114 D<1FD830786018E018E018F000FF807FE07FF01FF807FC007CC01CC01C E01CE018F830CFC00E127E9113>I<0300030003000300070007000F000F003FFCFFFC1F 001F001F001F001F001F001F001F001F001F0C1F0C1F0C1F0C0F08079803F00E1A7F9913 >II119 DI E /Fm 8 56 df<006000006000006000006000006000006000006000006000006000006000 FFFFF0FFFFF0006000006000006000006000006000006000006000006000006000006000 14167E9119>43 D<0C001C00EC000C000C000C000C000C000C000C000C000C000C000C00 0C000C000C000C00FFC00A137D9211>49 D<1F0060C06060F070F0306030007000700060 00C001C00180020004000810101020207FE0FFE00C137E9211>I<0FC030707038703870 380038003000E00FC0007000380018001C601CF01CF018E03860701FC00E137F9211>I< 006000E000E00160026006600C600860106020606060C060FFFC00600060006000600060 03FC0E137F9211>I<60607FC07F8044004000400040004F0070C040E0006000700070E0 70E070E06040E021C01F000C137E9211>I<07C00C201070207060006000C000CF00D0C0 E060C020C030C030C03040306020206010C00F000C137E9211>I<40007FFC7FF8401080 108020004000800100010003000200060006000E000E000E000E000E0004000E147E9311 >I E /Fn 25 123 df<60F0F06004047C830C>58 D<60F0F0701010101020204080040C 7C830C>I<00000C0000000C0000001C0000001C0000003C0000007C0000005C0000009C 0000008E0000010E0000010E0000020E0000040E0000040E0000080E0000080E0000100E 0000200E00003FFE00004007000040070000800700010007000100070002000700020007 00060007001E000700FF807FF01C1D7F9C1F>65 D<01FFFFF8003C007800380018003800 1000380010003800100070001000700010007010100070100000E0200000E0200000E060 0000FFE00001C0400001C0400001C0400001C04000038080400380004003800080038000 80070001000700010007000300070006000E003E00FFFFFC001D1C7E9B1F>69 D<01FFFFF0003C00F0003800300038002000380020003800200070002000700020007010 200070100000E0200000E0200000E0600000FFE00001C0400001C0400001C0400001C040 0003808000038000000380000003800000070000000700000007000000070000000F0000 00FFF000001C1C7E9B1B>I<0001F808000E061800380138006000F001C0007003800070 070000300F0000200E0000201C0000203C0000203C000000780000007800000078000000 F0000000F0000000F0007FF0F0000780F0000700F0000700F00007007000070070000E00 30000E0038000E001C001E000E0064000701840000FE00001D1E7E9C21>I<01FFC3FF80 003C0078000038007000003800700000380070000038007000007000E000007000E00000 7000E000007000E00000E001C00000E001C00000E001C00000FFFFC00001C003800001C0 03800001C003800001C0038000038007000003800700000380070000038007000007000E 000007000E000007000E000007000E00000F001E0000FFE1FFC000211C7E9B23>I<03FF C0003C0000380000380000380000380000700000700000700000700000E00000E00000E0 0000E00001C00001C00001C00001C0000380000380000380000380000700000700000700 000700000F0000FFF000121C7E9B12>I<01E3000717000C0F00180F00380E00300E0070 0E00700E00E01C00E01C00E01C00E01C00E03880E03880E038806078803199001E0E0011 127E9116>97 D<0001E0000630000E78000CF0001C60001C00001C00001C00003C000038 0000380003FFC000380000380000700000700000700000700000700000E00000E00000E0 0000E00000E00001C00001C00001C00001C00001C000018000038000038000630000F300 00F60000E4000078000015257E9C14>102 D<007180018B800307800607800E07000C07 001C07001C0700380E00380E00380E00380E00381C00381C00381C00183C0008F8000738 00003800003800007000607000F06000F0E000E180007E0000111A7F9114>I<0FC00001 C00001C0000380000380000380000380000700000700000700000700000E3E000EC3000F 03800E03801E03801C03801C03801C0380380700380700380700380E00700E20700E2070 1C20701C40E00C80600700131D7E9C18>I<0007000F000F000600000000000000000000 00000070009C010C020C021C041C001C001C0038003800380038007000700070007000E0 00E000E000E001C061C0F180F300E6007C001024809B11>106 D<0FC00001C00001C000 0380000380000380000380000700000700000700000700000E07000E18800E21C00E23C0 1C47801C83001D00001E00003F800039C00038E00038E00070E10070E10070E10070E200 E06200603C00121D7E9C16>I<1F800380038007000700070007000E000E000E000E001C 001C001C001C0038003800380038007000700070007000E400E400E400E4006400380009 1D7E9C0C>I<381F004E61804681C04701C08F01C08E01C00E01C00E01C01C03801C0380 1C03801C0700380710380710380E10380E2070064030038014127E9119>110 D<383C4E424687470F8E1E8E0C0E000E001C001C001C001C003800380038003800700030 0010127E9113>114 D<01F0060C04040C0E180C1C001F000FE00FF003F80038201C7018 F018F010803060601F800F127E9113>I<00C001C001C001C00380038003800380FFF007 00070007000E000E000E000E001C001C001C001C00382038203840384018800F000C1A80 990F>I<1C00C02701C04701C04701C08703808703800E03800E03801C07001C07001C07 001C0700180E20180E20180E201C1E200C264007C38013127E9118>I<1C022707470747 03870187010E010E011C021C021C021C041804180818081C100C2007C010127E9114>I< 1C00C0802701C1C04701C1C04701C0C087038040870380400E0380400E0380401C070080 1C0700801C0700801C07010018060100180602001C0E02001C0F04000E13080003E1F000 1A127E911E>I<07878008C84010F0C020F1E020E3C040E18000E00000E00001C00001C0 0001C00001C000638080F38080F38100E5810084C60078780013127E9118>I<1C00C027 01C04701C04701C08703808703800E03800E03801C07001C07001C07001C0700180E0018 0E00180E001C1E000C3C0007DC00001C00001800603800F03000F06000E0C0004180003E 0000121A7E9114>I<038107C10FE6081C10080010002000400080010002000400080410 042C1877F843F081C010127E9113>I E /Fo 14 111 df<01800180018001804182F18F 399C0FF003C003C00FF0399CF18F4182018001800180018010127E9215>3 D17 D<00000004000000000200000000020000000001 0000000000800000000040FFFFFFFFF8FFFFFFFFF8000000004000000000800000000100 000000020000000002000000000400250E7E902A>33 D<007FF801FFF80780000E000018 0000300000300000600000600000C00000C00000C00000FFFFF8FFFFF8C00000C00000C0 00006000006000003000003000001800000E000007800001FFF8007FF8151A7D961C>50 D<0000600000600000C00000C0000180000180000180000300000300000600000600000C 00000C0000180000180000180000300000300000600000600000C00000C0000180000180 000300000300000300000600000600000C00000C00001800001800003000003000003000 00600000600000C0000040000013287A9D00>54 D<0001FFFF000FFFFF0038E00E0041E0 0C01C1E0000381C0000301C0000603C0000003C000000380000003800000078000000700 0000070000000FFFC0000FFF00000E0000001C0000001C0000003C000000380000003800 00007000000070000030E0000070C00000FD800000FF0000003C000000201D7F9B1E>70 D<003FFF0001FFFFC0071E0FE0081C03F0381C01F8703C00F8603C0078C03C0078003C00 780038007000380070007800E0007800E0007801C0007001800070020000F00C0000E030 0000E7C00001EF000001E0000001C0000001C00000038000000380000007800000070000 00070000000E0000000C0000001D1E809B1D>80 D<003FFF000001FFFFE000071E0FF000 081C01F800381C00F800703C007800603C007800C03C007800003C007000003800700000 3800E000007800C0000078018000007802000000700C00000071F0000000F3F0000000E1 F0000000E0F8000001E0F8000001C07C000001C07C000003C03C000003803E018003803E 070007801F060007001F880006000FF0000C0007C000211D809B23>82 D<0000000400FFFFF803FFFFE00400E0001C00E0003801C0003001C0007003C000E003C0 00C00380000003800000078000000780000007000000070000000F0000000E0000000E00 00001E0000001E0000001C0000001C00000038000000380000007000000060000000C000 0007FF00000FFC00001E1D7F9C17>84 D<78000CFC001E3E001F1E001F0F000F0F000707 00030700020780020780020380040380040380080380180380300380300380600380C003 8180038380038700038E00039C0003B80003F00003E00007C00007800006000004000018 1E7E9B19>86 D<400002C00006C00006C00006C00006C01806C01806C01806C01806C018 06C01806C7FFC6C7FFC6C01806C01806C01806C01806C01806C0180660000C60000C3000 181C00700F01E003FF8000FE00171A7E981C>93 D<003C00E001C0018003800380038003 80038003800380038003800380038003800380030007001C00F0001C0007000300038003 8003800380038003800380038003800380038003800380018001C000E0003C0E297D9E15 >102 DI110 D E /Fp 21 121 df<00180000780001F800FFF800FFF80001F80001F80001F800 01F80001F80001F80001F80001F80001F80001F80001F80001F80001F80001F80001F800 01F80001F80001F80001F80001F80001F80001F80001F80001F80001F8007FFFE07FFFE0 13207C9F1C>49 D<03FC000FFF003C1FC07007E07C07F0FE03F0FE03F8FE03F8FE01F87C 01F83803F80003F80003F00003F00007E00007C0000F80001F00003E0000380000700000 E01801C0180380180700180E00380FFFF01FFFF03FFFF07FFFF0FFFFF0FFFFF015207D9F 1C>I<0003FE0080001FFF818000FF01E38001F8003F8003E0001F8007C0000F800F8000 07801F800007803F000003803F000003807F000001807E000001807E00000180FE000000 00FE00000000FE00000000FE00000000FE00000000FE00000000FE00000000FE00000000 7E000000007E000001807F000001803F000001803F000003801F800003000F8000030007 C000060003F0000C0001F800380000FF00F000001FFFC0000003FE000021227DA128>67 D73 D82 D<07FC001FFF803F07C03F03E03F01E03F01F01E01F00001F00001F0003FF003FDF01FC1 F03F01F07E01F0FC01F0FC01F0FC01F0FC01F07E02F07E0CF81FF87F07E03F18167E951B >97 D<00FF8007FFE00F83F01F03F03E03F07E03F07C01E07C0000FC0000FC0000FC0000 FC0000FC0000FC00007C00007E00007E00003E00301F00600FC0E007FF8000FE0014167E 9519>99 D<0001FE000001FE0000003E0000003E0000003E0000003E0000003E0000003E 0000003E0000003E0000003E0000003E0000003E0001FC3E0007FFBE000F81FE001F007E 003E003E007E003E007C003E00FC003E00FC003E00FC003E00FC003E00FC003E00FC003E 00FC003E00FC003E007C003E007C003E003E007E001E00FE000F83BE0007FF3FC001FC3F C01A237EA21F>I<00FE0007FF800F87C01E01E03E01F07C00F07C00F8FC00F8FC00F8FF FFF8FFFFF8FC0000FC0000FC00007C00007C00007E00003E00181F00300FC07003FFC000 FF0015167E951A>I<003F8000FFC001E3E003C7E007C7E00F87E00F83C00F80000F8000 0F80000F80000F80000F8000FFFC00FFFC000F80000F80000F80000F80000F80000F8000 0F80000F80000F80000F80000F80000F80000F80000F80000F80000F80000F80000F8000 7FF8007FF80013237FA211>I<1C003E007F007F007F003E001C00000000000000000000 0000000000FF00FF001F001F001F001F001F001F001F001F001F001F001F001F001F001F 001F001F001F001F00FFE0FFE00B247EA310>105 D108 DII<00FE0007FFC00F83E01E00F03E00F87C00 7C7C007C7C007CFC007EFC007EFC007EFC007EFC007EFC007EFC007E7C007C7C007C3E00 F81F01F00F83E007FFC000FE0017167E951C>II114 D<0FF3003FFF00781F00600700E00300E00300F00300FC 00007FE0007FF8003FFE000FFF0001FF00000F80C00780C00380E00380E00380F00700FC 0E00EFFC00C7F00011167E9516>I<018000018000018000018000038000038000078000 0780000F80003F8000FFFF00FFFF000F80000F80000F80000F80000F80000F80000F8000 0F80000F80000F80000F80000F81800F81800F81800F81800F81800F830007C30003FE00 00F80011207F9F16>II120 D E /Fq 68 128 df<007E1F8001C170400703C060060380E00E0380400E0380000E0380000E0380000E03 80000E038000FFFFFFE00E0380E00E0380E00E0380E00E0380E00E0380E00E0380E00E03 80E00E0380E00E0380E00E0380E00E0380E00E0380E00E0380E00E0380E07F8FE3FC1E1A 809920>14 D<60F0F868080808101020C0050B7D990B>39 D<60F0F07010101020204080 040B7D830B>44 DI<60F0F06004047D830B>I<07801860303030 3060186018E01CE01CE01CE01CE01CE01CE01CE01CE01CE01CE01CE01C60186018703830 30186007800E187E9713>48 D<03000700FF000700070007000700070007000700070007 0007000700070007000700070007000700070007000700FFF00C187D9713>I<0F801060 20304038803CC01CE01C401C003C003800380070006000C0018001000200040408041004 30083FF87FF8FFF80E187E9713>I<0F8010E02070607870382038007800700070006000 C00F8000E000700038003C003CE03CE03CC03C4038407030E00F800E187E9713>I<0030 0030007000F000F001700370027004700C7008701070307020704070C070FFFF00700070 007000700070007007FF10187F9713>I<30183FF03FE03FC02000200020002000200027 C03860203000380018001C001C401CE01CE01C80184038403030E00F800E187E9713>I< 01E006100C1818383038300070006000E000E7C0E860F030F018E018E01CE01CE01C601C 601C701830183030186007C00E187E9713>I<40007FFE7FFC7FFC400880108010802000 4000400080018001800100030003000300030007000700070007000700070002000F197E 9813>I<078018603030201860186018601870103C303E600F8007C019F030F86038401C C00CC00CC00CC00C6008201018600FC00E187E9713>I<07801860303070306018E018E0 18E01CE01CE01C601C603C303C185C0F9C001C00180018003870307060604021801F000E 187E9713>I<60F0F060000000000000000060F0F06004107D8F0B>I<007F00000180C000 060030000800080010000400203E020020E1020041C08100438071008380708087007080 8700708087007080870070808700708087007080838070804380708041C0F10020E13100 203E1E0010000000080000000600038001803E00007FE000191A7E991E>64 D<000C0000000C0000000C0000001E0000001E0000003F00000027000000270000004380 0000438000004380000081C0000081C0000081C0000100E0000100E00001FFE000020070 000200700006007800040038000400380008001C0008001C001C001E00FF00FFC01A1A7F 991D>II<003F0201C0C603002E0E001E1C000E1C000638 0006780002700002700002F00000F00000F00000F00000F00000F0000070000270000278 00023800041C00041C00080E000803003001C0C0003F00171A7E991C>IIII<003F02 0001C0C60003002E000E001E001C000E001C000600380006007800020070000200700002 00F0000000F0000000F0000000F0000000F0000000F001FFC070000E0070000E0078000E 0038000E001C000E001C000E000E000E000300160001C06600003F82001A1A7E991E>I< FFE7FF0E00700E00700E00700E00700E00700E00700E00700E00700E00700E00700E0070 0FFFF00E00700E00700E00700E00700E00700E00700E00700E00700E00700E00700E0070 0E0070FFE7FF181A7E991D>II< 1FFC00E000E000E000E000E000E000E000E000E000E000E000E000E000E000E000E000E0 00E000E040E0E0E0E0E041C061801E000E1A7D9914>IIIII<007F000001C1C000070070000E0038001C 001C003C001E0038000E0078000F0070000700F0000780F0000780F0000780F0000780F0 000780F0000780F0000780F000078078000F0078000F0038000E003C001E001C001C000E 0038000700700001C1C000007F0000191A7E991E>II82 D<0FC21836200E6006C006C002C002C002E00070007E003FE01FF807FC003E000E00 070003800380038003C002C006E004D81887E0101A7E9915>I<7FFFFF00701C0700401C 0100401C0100C01C0180801C0080801C0080801C0080001C0000001C0000001C0000001C 0000001C0000001C0000001C0000001C0000001C0000001C0000001C0000001C0000001C 0000001C0000001C0000001C0000001C000003FFE000191A7F991C>IIII<7FC0FF000F003C0007003000078020000380600001C0400001E0800000E180000071 0000007A0000003C0000001C0000001E0000001E00000017000000278000004380000041 C0000081E0000100E0000100700002007800040038000C001C001E003E00FF80FFC01A1A 7F991D>II<3F8070C070E020700070007007F01C7030707070E070E071E071E0F1 71FB1E3C10107E8F13>97 DI<07F80C1C381C30087000E0 00E000E000E000E000E0007000300438080C1807E00E107F8F11>I<007E00000E00000E 00000E00000E00000E00000E00000E00000E00000E0003CE000C3E00380E00300E00700E 00E00E00E00E00E00E00E00E00E00E00E00E00600E00700E00381E001C2E0007CFC0121A 7F9915>I<07C01C3030187018600CE00CFFFCE000E000E000E0006000300438080C1807 E00E107F8F11>I<01F0031807380E100E000E000E000E000E000E00FFC00E000E000E00 0E000E000E000E000E000E000E000E000E000E000E007FE00D1A80990C>I<0FCE187330 307038703870387038303018602FC02000600070003FF03FFC1FFE600FC003C003C003C0 036006381C07E010187F8F13>II<18003C003C00180000 0000000000000000000000FC001C001C001C001C001C001C001C001C001C001C001C001C 001C001C00FF80091A80990A>I<018003C003C001800000000000000000000000000FC0 01C001C001C001C001C001C001C001C001C001C001C001C001C001C001C001C001C001C0 41C0E180E3007E000A2182990C>IIIII<07E01C 38300C700E6006E007E007E007E007E007E0076006700E381C1C3807E010107F8F13>I< FCF8001F0E001E07001C03801C03801C01C01C01C01C01C01C01C01C01C01C01C01C0380 1C03001E07001F0C001CF0001C00001C00001C00001C00001C00001C0000FF800012177F 8F15>I114 D<1F2060E04020C020C020F0007F003FC01FE000F080708030C030C0 20F0408F800C107F8F0F>I<0400040004000C000C001C003C00FFC01C001C001C001C00 1C001C001C001C001C201C201C201C201C200E4003800B177F960F>IIIIII<7FF86070407040E041C041C00380070007000E 081C081C08381070107030FFF00D107F8F11>II<6180F3C0F3C061 800A047C9913>127 D E /Fr 68 123 df<007E0001C1800301800703C00E03C00E0180 0E00000E00000E00000E00000E0000FFFFC00E01C00E01C00E01C00E01C00E01C00E01C0 0E01C00E01C00E01C00E01C00E01C00E01C00E01C00E01C00E01C00E01C07F87F8151D80 9C17>12 D<007FC001C1C00303C00703C00E01C00E01C00E01C00E01C00E01C00E01C00E 01C0FFFFC00E01C00E01C00E01C00E01C00E01C00E01C00E01C00E01C00E01C00E01C00E 01C00E01C00E01C00E01C00E01C00E01C07FCFF8151D809C17>I<003F07E00001C09C18 000380F018000701F03C000E01E03C000E00E018000E00E000000E00E000000E00E00000 0E00E000000E00E00000FFFFFFFC000E00E01C000E00E01C000E00E01C000E00E01C000E 00E01C000E00E01C000E00E01C000E00E01C000E00E01C000E00E01C000E00E01C000E00 E01C000E00E01C000E00E01C000E00E01C000E00E01C007FC7FCFF80211D809C23>I<60 F0F8680808081010204080050C7C9C0C>39 D<004000800100020006000C000C00180018 00300030007000600060006000E000E000E000E000E000E000E000E000E000E000E000E0 00600060006000700030003000180018000C000C00060002000100008000400A2A7D9E10 >I<800040002000100018000C000C000600060003000300038001800180018001C001C0 01C001C001C001C001C001C001C001C001C001C001800180018003800300030006000600 0C000C00180010002000400080000A2A7E9E10>I<60F0F0701010101020204080040C7C 830C>44 DI<60F0F06004047C830C>I<03C00C301818300C300C 700E60066006E007E007E007E007E007E007E007E007E007E007E007E007E00760066006 700E300C300C18180C3007E0101D7E9B15>48 D<030007003F00C7000700070007000700 070007000700070007000700070007000700070007000700070007000700070007000700 0F80FFF80D1C7C9B15>I<07C01830201C400C400EF00FF80FF807F8077007000F000E00 0E001C001C00380070006000C00180030006010C01180110023FFE7FFEFFFE101C7E9B15 >I<07E01830201C201C781E780E781E381E001C001C00180030006007E00030001C001C 000E000F000F700FF80FF80FF80FF00E401C201C183007E0101D7E9B15>I<000C00000C 00001C00003C00003C00005C0000DC00009C00011C00031C00021C00041C000C1C00081C 00101C00301C00201C00401C00C01C00FFFFC0001C00001C00001C00001C00001C00001C 00001C0001FFC0121C7F9B15>I<300C3FF83FF03FC020002000200020002000200023E0 24302818301C200E000E000F000F000F600FF00FF00FF00F800E401E401C2038187007C0 101D7E9B15>I<00F0030C06040C0E181E301E300C700070006000E3E0E430E818F00CF0 0EE006E007E007E007E007E007600760077006300E300C18180C3003E0101D7E9B15>I< 4000007FFF807FFF007FFF00400200800400800400800800001000001000002000006000 00400000C00000C00001C000018000018000038000038000038000038000078000078000 078000078000078000078000030000111D7E9B15>I<03E00C301008200C200660066006 60067006780C3E083FB01FE007F007F818FC307E601E600FC007C003C003C003C0036002 6004300C1C1007E0101D7E9B15>I<03C00C301818300C700C600EE006E006E007E007E0 07E007E0076007700F300F18170C2707C700060006000E300C780C78187010203030C00F 80101D7E9B15>I<60F0F0600000000000000000000060F0F06004127C910C>I<7FFFFFC0 FFFFFFE00000000000000000000000000000000000000000000000000000000000000000 FFFFFFE07FFFFFC01B0C7E8F20>61 D<000600000006000000060000000F0000000F0000 000F00000017800000178000001780000023C0000023C0000023C0000041E0000041E000 0041E0000080F0000080F0000180F8000100780001FFF80003007C0002003C0002003C00 06003E0004001E0004001E000C001F001E001F00FF80FFF01C1D7F9C1F>65 DI<001F808000E061800180198007000780 0E0003801C0003801C00018038000180780000807800008070000080F0000000F0000000 F0000000F0000000F0000000F0000000F0000000F0000000700000807800008078000080 380000801C0001001C0001000E000200070004000180080000E03000001FC000191E7E9C 1E>IIII<001F808000E0618001801980070007800E000380 1C0003801C00018038000180780000807800008070000080F0000000F0000000F0000000 F0000000F0000000F0000000F000FFF0F0000F8070000780780007807800078038000780 1C0007801C0007800E00078007000B800180118000E06080001F80001C1E7E9C21>II I75 DIII<003F800000E0E0000380380007001C000E000E001C0007003C00 078038000380780003C0780003C0700001C0F00001E0F00001E0F00001E0F00001E0F000 01E0F00001E0F00001E0F00001E0700001C0780003C0780003C0380003803C0007801C00 07000E000E0007001C000380380000E0E000003F80001B1E7E9C20>II82 D<07E0801C1980300580700380600180E00180E00080E00080E00080F00000F800007C00 007FC0003FF8001FFE0007FF0000FF80000F800007C00003C00001C08001C08001C08001 C0C00180C00180E00300D00200CC0C0083F800121E7E9C17>I<7FFFFFC0700F01C0600F 00C0400F0040400F0040C00F0020800F0020800F0020800F0020000F0000000F0000000F 0000000F0000000F0000000F0000000F0000000F0000000F0000000F0000000F0000000F 0000000F0000000F0000000F0000000F0000000F0000001F800003FFFC001B1C7F9B1E> I87 D91 D93 D<1FC000307000783800781C00301C00001C00001C0001FC000F1C00381C00701C00601C 00E01C40E01C40E01C40603C40304E801F870012127E9115>97 DI<07E00C301878307870306000E000E000E000E000E000E0 0060007004300418080C3007C00E127E9112>I<003F0000070000070000070000070000 070000070000070000070000070000070003E7000C1700180F00300700700700600700E0 0700E00700E00700E00700E00700E00700600700700700300700180F000C370007C7E013 1D7E9C17>I<03E00C301818300C700E6006E006FFFEE000E000E000E000600070023002 18040C1803E00F127F9112>I<00F8018C071E061E0E0C0E000E000E000E000E000E00FF E00E000E000E000E000E000E000E000E000E000E000E000E000E000E000E000E007FE00F 1D809C0D>I<00038003C4C00C38C01C3880181800381C00381C00381C00381C00181800 1C38000C300013C0001000003000001800001FF8001FFF001FFF803003806001C0C000C0 C000C0C000C06001803003001C0E0007F800121C7F9215>II<18003C003C0018000000000000000000000000000000FC001C 001C001C001C001C001C001C001C001C001C001C001C001C001C001C001C00FF80091D7F 9C0C>I<00C001E001E000C000000000000000000000000000000FE000E000E000E000E0 00E000E000E000E000E000E000E000E000E000E000E000E000E000E000E000E060E0F0C0 F1C061803E000B25839C0D>IIIII<03F0000E1C00180600300300700380600180E001C0E001C0E001C0E001C0 E001C0E001C06001807003803003001806000E1C0003F00012127F9115>II<03C1000C3300180B00300F00700700700700E00700E00700E00700E0 0700E00700E00700600700700700300F00180F000C370007C70000070000070000070000 0700000700000700000700003FE0131A7E9116>II<1F9030704030C010 C010E010F8007F803FE00FF000F880388018C018C018E010D0608FC00D127F9110>I<04 000400040004000C000C001C003C00FFE01C001C001C001C001C001C001C001C001C001C 101C101C101C101C100C100E2003C00C1A7F9910>III< FF3FCFE03C0F03801C0701801C0701001C0B01000E0B82000E0B82000E1182000711C400 0711C4000720C40003A0E80003A0E80003C0680001C0700001C070000180300000802000 1B127F911E>I<7F8FF00F03800F030007020003840001C80001D80000F0000070000078 0000F800009C00010E00020E000607000403801E07C0FF0FF81512809116>II<7FFC70386038407040F040E041C003C0038007000F040E041C043C 0C380870087038FFF80E127F9112>I E /Fs 27 122 df<0001FFFC00001FFFFC00007F 81FC0000FC01FC0001F801FC0003F801FC0007F001FC0007F001FC0007F001FC0007F001 FC0007F001FC0007F001FC0007F001FC0007F001FC0007F001FC00FFFFFFFC00FFFFFFFC 00FFFFFFFC0007F001FC0007F001FC0007F001FC0007F001FC0007F001FC0007F001FC00 07F001FC0007F001FC0007F001FC0007F001FC0007F001FC0007F001FC0007F001FC0007 F001FC0007F001FC0007F001FC0007F001FC0007F001FC0007F001FC0007F001FC0007F0 01FC007FFF1FFFC07FFF1FFFC07FFF1FFFC0222A7FA926>13 D45 D<00003FF001800003FFFE0380000FFFFF8780003F F007DF8000FF8001FF8001FE00007F8003FC00003F8007F000001F800FF000000F801FE0 000007801FE0000007803FC0000007803FC0000003807FC0000003807F80000003807F80 00000000FF8000000000FF8000000000FF8000000000FF8000000000FF8000000000FF80 00000000FF8000000000FF8000000000FF80000000007F80000000007F80000000007FC0 000003803FC0000003803FC0000003801FE0000003801FE0000007000FF00000070007F0 00000E0003FC00001E0001FE00003C0000FF8000F800003FF007E000000FFFFFC0000003 FFFF000000003FF8000029297CA832>67 D77 D80 D82 D<007F806003FFF0E007FFF9E00F807FE01F001FE03E0007E07C0003E07C0001E0FC 0001E0FC0001E0FC0000E0FE0000E0FE0000E0FF000000FFC000007FFE00007FFFE0003F FFFC001FFFFE000FFFFF8007FFFFC003FFFFE000FFFFE00007FFF000007FF000000FF800 0007F8000003F8600001F8E00001F8E00001F8E00001F8F00001F0F00001F0F80003F0FC 0003E0FF0007C0FFE01F80F3FFFF00E0FFFE00C01FF0001D297CA826>I<7FFFFFFFFFC0 7FFFFFFFFFC07FFFFFFFFFC07F803FC03FC07E003FC007C078003FC003C078003FC003C0 70003FC001C0F0003FC001E0F0003FC001E0E0003FC000E0E0003FC000E0E0003FC000E0 E0003FC000E0E0003FC000E000003FC0000000003FC0000000003FC0000000003FC00000 00003FC0000000003FC0000000003FC0000000003FC0000000003FC0000000003FC00000 00003FC0000000003FC0000000003FC0000000003FC0000000003FC0000000003FC00000 00003FC0000000003FC0000000003FC0000000003FC0000000003FC0000000003FC00000 007FFFFFE000007FFFFFE000007FFFFFE0002B287EA730>I86 D<01FF800007FFF0000F81F8001FC07E001FC07E001FC03F000F803F8007003F8000003F 8000003F8000003F80000FFF8000FFFF8007FC3F800FE03F803F803F803F003F807F003F 80FE003F80FE003F80FE003F80FE003F807E007F807F00DF803F839FFC0FFF0FFC01FC03 FC1E1B7E9A21>97 DI<00003FF80000003FF80000003FF800000003F800000003F80000 0003F800000003F800000003F800000003F800000003F800000003F800000003F8000000 03F800000003F800000003F800001FE3F80000FFFBF80003F03FF80007E00FF8000FC007 F8001F8003F8003F8003F8007F0003F8007F0003F8007F0003F800FF0003F800FF0003F8 00FF0003F800FF0003F800FF0003F800FF0003F800FF0003F8007F0003F8007F0003F800 7F0003F8003F8003F8001F8003F8000F8007F80007C00FF80003F03BFF8000FFF3FF8000 3FC3FF80212A7EA926>100 D<003FE00001FFF80003F07E0007C01F000F801F801F800F 803F800FC07F000FC07F0007C07F0007E0FF0007E0FF0007E0FFFFFFE0FFFFFFE0FF0000 00FF000000FF0000007F0000007F0000007F0000003F8000E01F8000E00FC001C007E003 8003F81F0000FFFE00001FF0001B1B7E9A20>I<0007F0003FFC00FE3E01F87F03F87F03 F07F07F07F07F03E07F00007F00007F00007F00007F00007F00007F000FFFFC0FFFFC0FF FFC007F00007F00007F00007F00007F00007F00007F00007F00007F00007F00007F00007 F00007F00007F00007F00007F00007F00007F00007F00007F00007F0007FFF807FFF807F FF80182A7EA915>I<00FF81F003FFE7F80FC1FE7C1F80FC7C1F007C383F007E107F007F 007F007F007F007F007F007F007F007F007F007F003F007E001F007C001F80FC000FC1F8 001FFFE00018FF800038000000380000003C0000003E0000003FFFF8001FFFFF001FFFFF 800FFFFFC007FFFFE01FFFFFF03E0007F07C0001F8F80000F8F80000F8F80000F8F80000 F87C0001F03C0001E01F0007C00FC01F8003FFFE00007FF0001E287E9A22>I<07000F80 1FC03FE03FE03FE01FC00F8007000000000000000000000000000000FFE0FFE0FFE00FE0 0FE00FE00FE00FE00FE00FE00FE00FE00FE00FE00FE00FE00FE00FE00FE00FE00FE00FE0 0FE00FE0FFFEFFFEFFFE0F2B7DAA14>105 D108 DII<003FE00001FFFC0003F07E000FC01F801F80 0FC03F800FE03F0007E07F0007F07F0007F07F0007F0FF0007F8FF0007F8FF0007F8FF00 07F8FF0007F8FF0007F8FF0007F8FF0007F87F0007F07F0007F03F800FE03F800FE01F80 0FC00FC01F8007F07F0001FFFC00003FE0001D1B7E9A22>I114 D<03FE300FFFF01E03F03800F0700070F00070F00070F80070FC0000FFE0 007FFE007FFF803FFFE01FFFF007FFF800FFF80003FC0000FC60007CE0003CF0003CF000 38F80038FC0070FF01E0F7FFC0C1FF00161B7E9A1B>I<00700000700000700000700000 F00000F00000F00001F00003F00003F00007F0001FFFF0FFFFF0FFFFF007F00007F00007 F00007F00007F00007F00007F00007F00007F00007F00007F00007F00007F00007F03807 F03807F03807F03807F03807F03803F03803F87001F86000FFC0001F8015267FA51B>I< FFE03FF800FFE03FF800FFE03FF8000FE003F8000FE003F8000FE003F8000FE003F8000F E003F8000FE003F8000FE003F8000FE003F8000FE003F8000FE003F8000FE003F8000FE0 03F8000FE003F8000FE003F8000FE003F8000FE003F8000FE003F8000FE003F8000FE007 F80007E007F80007E00FF80003F03BFF8001FFF3FF80003FC3FF80211B7D9A26>III121 D E end %%EndProlog %%BeginSetup %%Feature: *Resolution 300dpi TeXDict begin %%PaperSize: A4 %%EndSetup %%Page: 1 1 1 0 bop 271 194 a Fs(T)-6 b(ermination)21 b(is)h(not)i(Mo)r(dular)f (for)h(Con\015uen)n(t)221 263 y(V)-6 b(ariable-Preserving)22 b(T)-6 b(erm)22 b(Rewriting)e(Systems)755 408 y Fr(Enno)14 b(Ohlebusc)o(h)501 495 y Fq(Univ)o(ersit\177)-19 b(at)15 b(Bielefeld,)g(33501)f(Bielefeld,)h(German)o(y)m(,)594 541 y(e-mail:)f(enno@tec)o(hfak.uni-biel)q(efeld.de)183 642 y Fr(Keyw)o(ords:)g(T)m(erm)f(rewriting,)g(termination,)f(mo)q (dularit)o(y)m(,)e(program)i(sp)q(eci\014cation)183 779 y Fp(1)56 b(In)n(tro)r(duction)183 881 y Fr(A)14 b(term)g(rewriting)g (system)g(\(TRS)g(for)g(short\))h(is)f(a)g(pair)g(\()p Fo(F)t Fn(;)7 b Fo(R)p Fr(\))14 b(consisting)h(of)e(a)h(signa-)183 931 y(ture)d Fo(F)k Fr(and)10 b(a)h(set)g Fo(R)g Fr(of)f(rewrite)i (rules)f([1,)f(4].)f(Ev)o(ery)j(rewrite)f(rule)g Fn(l)i Fo(!)e Fn(r)i Fo(2)e(R)p Fr(,)f(where)i Fn(l)q(;)7 b(r)183 981 y Fr(are)13 b(terms)f(from)f Fo(T)f Fr(\()p Fo(F)t Fn(;)d Fo(V)t Fr(\),)12 b(m)o(ust)g(satisfy)g(the)i(follo)o(wing)c(t)o (w)o(o)i(constrain)o(ts:)h(\(i\))g Fn(l)h Fr(is)e(not)h(a)183 1031 y(v)n(ariable,)e(and)j(\(ii\))e(v)n(ariables)h(o)q(ccurring)h(in)f Fn(r)h Fr(also)f(o)q(ccur)i(in)d Fn(l)q Fr(.)i(Tw)o(o)e(TRSs)i(are)g (disjoin)o(t)183 1080 y(if)h(their)i(signatures)g(are)f(disjoin)o(t.)f (A)h(prop)q(ert)o(y)h Fo(P)j Fr(of)15 b(TRSs)i(is)f(called)g(mo)q (dular,)e(if)h(for)183 1130 y(all)d(disjoin)o(t)h(TRSs)g(\()p Fo(F)547 1136 y Fm(1)566 1130 y Fn(;)7 b Fo(R)620 1136 y Fm(1)638 1130 y Fr(\))14 b(and)g(\()p Fo(F)795 1136 y Fm(2)813 1130 y Fn(;)7 b Fo(R)867 1136 y Fm(2)886 1130 y Fr(\))13 b(their)i(disjoin)o(t)d(union)h(\()p Fo(F)1323 1136 y Fm(1)1351 1130 y Fo(])8 b(F)1417 1136 y Fm(2)1436 1130 y Fn(;)f Fo(R)1490 1136 y Fm(1)1517 1130 y Fo(])i(R)1589 1136 y Fm(2)1607 1130 y Fr(\))183 1180 y(has)k(the)i(prop)q(ert)o(y)f Fo(P)j Fr(if)c(and)g(only)g(if)g(b)q(oth)g(\()p Fo(F)933 1186 y Fm(1)952 1180 y Fn(;)7 b Fo(R)1006 1186 y Fm(1)1024 1180 y Fr(\))14 b(and)f(\()p Fo(F)1180 1186 y Fm(2)1199 1180 y Fn(;)7 b Fo(R)1253 1186 y Fm(2)1271 1180 y Fr(\))14 b(ha)o(v)o(e)f(the)i(prop)q(ert)o(y)183 1230 y Fo(P)s Fr(.)f(In)g(his)g(pioneering)g(pap)q(er)h([8],)e(T)m(o)o(y)o(ama)e(sho) o(w)o(ed)k(the)f(mo)q(dularit)o(y)e(of)i(con\015uence.)h(A)183 1280 y(comprehensiv)o(e)g(surv)o(ey)h(of)f(mo)q(dular)f(prop)q(erties)j (can)e(b)q(e)h(found)f(in)g([5)o(].)g(Sev)o(eral)g(coun-)183 1329 y(terexamples)e(to)g(the)i(mo)q(dularit)o(y)c(of)h(termination)g (are)i(presen)o(ted)i(in)d([7)o(].)g(The)h(simplest)183 1379 y(reads)g(as)g(follo)o(ws.)183 1473 y Fl(Example)h(1.1)21 b Fr(The)15 b(term)f(rewriting)h(systems)g(\()p Fo(F)1028 1479 y Fm(1)1047 1473 y Fn(;)7 b Fo(R)1101 1479 y Fm(1)1119 1473 y Fr(\))14 b(=)f(\()p Fo(f)p Fr(0)p Fn(;)7 b Fr(1)p Fn(;)g(F)f Fo(g)p Fn(;)h Fo(f)p Fn(F)e Fr(\(0)p Fn(;)i Fr(1)o Fn(;)g(x)p Fr(\))j Fo(!)183 1523 y Fn(F)c Fr(\()p Fn(x;)h(x;)g(x)p Fr(\))p Fo(g)p Fr(\),)17 b(and)j(\()p Fo(F)557 1529 y Fm(2)575 1523 y Fn(;)7 b Fo(R)629 1529 y Fm(2)648 1523 y Fr(\))21 b(=)h(\()p Fo(f)p Fn(g)q Fo(g)p Fn(;)7 b Fo(f)p Fn(g)q Fr(\()p Fn(x;)g(y)q Fr(\))22 b Fo(!)f Fn(x;)7 b(g)q Fr(\()p Fn(x;)g(y)q Fr(\))21 b Fo(!)h Fn(y)q Fo(g)p Fr(\))e(are)h(eviden)o(tly)183 1573 y(terminating)11 b(but)j(their)g(disjoin)o(t)e(union)h(is)g(not:)g(there)h(is)f(the)h (cyclic)g(rewrite)g(deriv)n(ation)183 1661 y Fn(t)d Fo(\021)h Fn(F)6 b Fr(\(0)p Fn(;)h Fr(1)p Fn(;)g(g)q Fr(\(0)p Fn(;)g Fr(1\)\))i Fo(!)563 1667 y Fk(R)592 1671 y Fj(1)621 1661 y Fn(F)d Fr(\()p Fn(g)q Fr(\(0)p Fn(;)h Fr(1\))p Fn(;)g(g)q Fr(\(0)p Fn(;)g Fr(1\))p Fn(;)g(g)q Fr(\(0)p Fn(;)g Fr(1\)\))i Fo(!)1117 1667 y Fk(R)1146 1671 y Fj(2)1175 1661 y Fn(F)d Fr(\(0)p Fn(;)h(g)q Fr(\(0)p Fn(;)g Fr(1\))p Fn(;)g(g)q Fr(\(0)p Fn(;)g Fr(1\)\))i Fo(!)1578 1667 y Fk(R)1607 1671 y Fj(2)1635 1661 y Fn(t)245 1755 y Fr(In)15 b(the)h(ab)q(o)o(v)o (e)f(example)e Fo(R)688 1761 y Fm(2)722 1755 y Fr(is)i(not)g (con\015uen)o(t,)h(but)f(coun)o(terexamples)g(giv)o(en)g(inde-)183 1805 y(p)q(enden)o(tly)i(b)o(y)f(Klop)f(and)h(Barendregt)i([7)o(])e(as) g(w)o(ell)g(as)g(Drosten)h([2)o(])f(sho)o(w)g(that)g(this)h(is)183 1854 y(not)c(essen)o(tial.)h(W)m(e)g(presen)o(t)h(a)f(v)n(arian)o(t)f (of)g(the)h(example)f(of)g([2].)183 1948 y Fl(Example)i(1.2)21 b Fr(Let)424 2038 y Fo(F)454 2044 y Fm(1)484 2038 y Fr(=)12 b Fo(f)p Fr(0)p Fn(;)7 b Fr(1)p Fn(;)g Fr(2)p Fn(;)g(F)e Fo(g)11 b Fr(and)j Fo(R)849 2044 y Fm(1)879 2038 y Fr(=)923 1928 y Fi(8)923 1966 y(>)923 1978 y(>)923 1991 y(<)923 2065 y(>)923 2078 y(>)923 2090 y(:)966 1963 y Fn(F)6 b Fr(\(0)p Fn(;)h Fr(1)p Fn(;)g(x)p Fr(\))k Fo(!)g Fn(F)6 b Fr(\()p Fn(x;)h(x;)g(x)p Fr(\))966 2013 y Fn(F)f Fr(\()p Fn(x;)h(y)q(;)g(z)r Fr(\))k Fo(!)g Fr(2)966 2063 y(0)159 b Fo(!)11 b Fr(2)966 2113 y(1)159 b Fo(!)11 b Fr(2)414 2234 y(as)j(w)o(ell)f(as)h Fo(F)630 2240 y Fm(2)660 2234 y Fr(=)e Fo(f)p Fn(g)q Fo(g)h Fr(and)h Fo(R)896 2240 y Fm(2)927 2234 y Fr(=)970 2175 y Fi(\032)1007 2209 y Fn(g)q Fr(\()p Fn(x;)7 b(y)q(;)g(y)q Fr(\))13 b Fo(!)e Fn(x)1007 2258 y(g)q Fr(\()p Fn(y)q(;)c(y)q(;)g(x)p Fr(\))13 b Fo(!)e Fn(x)183 2332 y Fr(Both)i(systems)h(are)g(con)o(v)o(ergen)o (t,)g(i.e,)e(con\015uen)o(t)j(and)e(terminating.)e Fo(R)1324 2338 y Fm(1)1352 2332 y Fo(])d(R)1423 2338 y Fm(2)1442 2332 y Fr(,)13 b(ho)o(w)o(ev)o(er,)183 2382 y(is)k(not)h(terminating.)e (Starting)h(from)f Fn(F)6 b Fr(\()p Fn(g)q Fr(\(0)p Fn(;)h Fr(1)p Fn(;)g Fr(1\))p Fn(;)g(g)q Fr(\(0)p Fn(;)g Fr(1)p Fn(;)g Fr(1\))p Fn(;)f(g)q Fr(\(0)p Fn(;)h Fr(1)p Fn(;)f Fr(1\)\),)15 b(w)o(e)j(obtain)f(a)183 2432 y(cyclic)d(reduction)g (sequence)i(as)e(in)g(the)g(previous)h(example.)893 2556 y(1)p eop %%Page: 2 2 2 1 bop 403 194 a Fr(In)16 b(Example)e(1.2)22 b Fo(R)742 200 y Fm(1)777 194 y Fr(is)16 b(not)g(irreducible)h(\(a)f(TRS)f Fo(R)h Fr(is)g(called)g(irreducible)h(if,)e(for)340 244 y(an)o(y)f(rule)g Fn(l)e Fo(!)f Fn(r)k Fr(in)e Fo(R)p Fr(,)h Fn(l)h Fr(and)e Fn(r)i Fr(are)f(normal)d(forms)i(w.r.t.)f Fo(R)e(n)e(f)p Fn(l)13 b Fo(!)e Fn(r)q Fo(g)p Fr(\).)i(Again)g(this)g (is)340 293 y(not)g(essen)o(tial)g(as)g(w)o(as)f(\014rst)i(sho)o(wn)f (b)o(y)f(T)m(o)o(y)o(ama)e([7)o(])i(b)o(y)h(a)f(certain)h(mo)q (di\014cation)e(of)h(Klop)340 343 y(and)g(Barendregt's)h(example.)d (Middeldorp)i(applied)f(this)h(tec)o(hnique)g(in)g([5)o(])f(to)h (Drosten's)340 393 y(example)h(and)h(obtained)f(the)i(follo)o(wing)c (coun)o(terexample.)340 474 y Fl(Example)16 b(1.3)k Fr(Let)15 b Fo(R)729 480 y Fm(2)761 474 y Fr(b)q(e)g(as)f(in)f(Example)g(1.2)f (and)i Fo(F)1267 480 y Fm(1)1297 474 y Fr(=)e Fo(f)p Fr(0)p Fn(;)7 b Fr(2)p Fn(;)g(F)q(;)g(G;)g(H)r Fo(g)p Fr(,)668 626 y Fo(R)703 632 y Fm(1)734 626 y Fr(=)778 516 y Fi(8)778 554 y(>)778 566 y(>)778 578 y(<)778 653 y(>)778 666 y(>)778 678 y(:)820 551 y Fn(F)f Fr(\()p Fn(G)p Fr(\()p Fn(x)p Fr(\))p Fn(;)h(H)s Fr(\()p Fn(x)p Fr(\))p Fn(;)g(y)q(;)g(x)p Fr(\))j Fo(!)h Fn(F)6 b Fr(\()p Fn(y)q(;)h(y)q(;)g(y)q(;)g(x)p Fr(\))820 601 y Fn(F)f Fr(\()p Fn(x;)h(y)q(;)g(z)r(;)g Fr(0\))151 b Fo(!)11 b Fr(2)820 651 y Fn(G)p Fr(\(0\))274 b Fo(!)11 b Fr(2)820 701 y Fn(H)s Fr(\(0\))269 b Fo(!)11 b Fr(2)340 776 y(Both)j Fo(R)478 782 y Fm(1)510 776 y Fr(and)f Fo(R)625 782 y Fm(2)656 776 y Fr(are)h(con)o(v)o(ergen)o(t)g(and)f(irreducible)g(but)h Fo(R)1327 782 y Fm(1)1353 776 y Fo(])7 b(R)1423 782 y Fm(2)1455 776 y Fr(is)13 b(not)g(terminating)340 826 y(b)q(ecause)k(there)g(is)d(a)h(cyclic)h(reduction)f(sequence)j (starting)d(from)e(the)j(term)e Fn(F)6 b Fr(\()p Fn(t;)h(t;)g(t;)g Fr(0\),)340 875 y(where)15 b Fn(t)d Fo(\021)g Fn(g)q Fr(\()p Fn(G)p Fr(\(0\))p Fn(;)7 b(H)s Fr(\(0\))p Fn(;)g(H)s Fr(\(0\)\).)403 957 y(Note)20 b(that)g(in)g(all)e(kno)o(wn)i(coun)o (terexamples)g(at)g(least)g(one)g(of)f(the)i(TRSs)f(is)f(not)340 1007 y(v)n(ariable-preserving)j(and)g(that)f(this)h(seems)g(to)g(b)q(e) g(essen)o(tial.)g(A)g(TRS)f Fo(R)h Fr(is)g(called)340 1056 y Fh(variable-pr)n(eserving)d Fr(or)h(non-erasing)g(if)f(all)g(v)n (ariables)g(that)h(o)q(ccur)h(at)f(the)h(left-hand)340 1106 y(side)15 b Fn(l)g Fr(of)e(some)g(rule)h Fn(l)f Fo(!)e Fn(r)h Fo(2)f(R)k Fr(also)e(o)q(ccur)i(in)e Fn(r)q Fr(.)403 1156 y(Of)i(course)h(su\016cien)o(t)f(conditions)g(can)g(b)q (e)h(giv)o(en)e(whic)o(h)h(ensure)i(the)e(mo)q(dularit)o(y)e(of)340 1206 y(termination.)j(The)h(in)o(terested)i(reader)g(is)e(referred)i (to)e([6,)g(3)o(])g(where)i(it)e(is)g(sho)o(wn)g(that)340 1256 y(most)e(of)f(the)i(kno)o(wn)f(results)i(are)f(co)o(v)o(ered)g(b)o (y)f(one)h(p)q(o)o(w)o(erful)f(theorem.)f(Another)i(deep)340 1305 y(theorem)f(of)f(T)m(o)o(y)o(ama,)d(Klop)j(and)h(Barendregt)h([9]) e(sa)o(ys)h(that)f Fh(termination)i(is)f(a)h(mo)n(du-)340 1355 y(lar)f(pr)n(op)n(erty)g(of)g(c)n(on\015uent)i(left-line)n(ar)d (TRSs)p Fr(.)g(Their)h(result,)g(in)f(conjunction)h(with)f(the)340 1405 y(ab)q(o)o(v)o(e)e(observ)n(ation,)g(suggests)h(to)f(examine)f (whether)j(the)e(follo)o(wing)e(conjecture)k(is)e(true.)340 1505 y Fl(Conjecture)p Fr(:)g Fh(T)m(ermination)i(is)h(mo)n(dular)f (for)h(c)n(on\015uent)h(variable-pr)n(eserving)e(TRSs.)340 1604 y Fr(Con)o(trary)i(to)f(exp)q(ectation,)h(the)g(answ)o(er)g(is)f (negativ)o(e.)g(W)m(e)g(giv)o(e)g(t)o(w)o(o)g(coun)o(terexamples)340 1654 y(whic)o(h)f(refute)h(this)f(conjecture)i(\(one)e(of)f(them)g(ev)o (en)i(uses)g(irreducible)f(TRSs\).)340 1781 y Fp(2)56 b(Coun)n(terexamples)340 1872 y Fr(The)15 b(next)f(example)f(sho)o(ws)h (that)g(the)g(ab)q(o)o(v)o(e)g(conjecture)i(do)q(es)e(not)g(hold.)340 1954 y Fl(Example)i(2.1)k Fr(Let)15 b Fo(F)724 1960 y Fm(1)755 1954 y Fr(=)d Fo(f)p Fn(F)847 1960 y Fm(1)865 1954 y Fn(;)7 b(F)911 1960 y Fm(2)929 1954 y Fn(;)g(G)981 1960 y Fm(1)999 1954 y Fn(;)g(G)1051 1960 y Fm(2)1068 1954 y Fn(;)g(H)1122 1960 y Fm(1)1140 1954 y Fn(;)g(H)1194 1960 y Fm(2)1212 1954 y Fn(;)g(I)s(;)g(E)1302 1960 y Fm(1)1319 1954 y Fn(;)g(:)g(:)g(:)e(;)i(E)1443 1960 y Fm(6)1461 1954 y Fo(g)14 b Fr(and)g(let)g Fo(R)1672 1960 y Fm(1)1705 1954 y Fr(con-)340 2003 y(sist)h(of)e(the)h(rules)433 2076 y Fn(F)460 2082 y Fm(1)551 2076 y Fn(F)578 2082 y Fm(2)429 2312 y Fn(H)464 2318 y Fm(1)430 2194 y Fn(G)463 2200 y Fm(1)548 2194 y Fn(G)581 2200 y Fm(2)548 2312 y Fn(H)583 2318 y Fm(2)504 2433 y Fn(I)456 2372 y Fg(@)474 2389 y(@)-42 b(R)533 2372 y(\000)515 2389 y(\000)g(\011)p 455 2271 2 60 v 456 2271 a(?)p 573 2271 V 76 w(?)486 2254 y(@)503 2271 y(@)g(R)503 2254 y(\000)486 2271 y(\000)g(\011)p 455 2153 V 456 2153 a(?)p 573 2153 V 76 w(?)486 2135 y(@)503 2153 y(@)g(R)503 2135 y(\000)486 2153 y(\000)g(\011)787 2127 y Fn(E)818 2133 y Fm(1)836 2127 y Fr(\()p Fn(H)887 2133 y Fm(1)905 2127 y Fn(;)7 b(H)959 2133 y Fm(2)977 2127 y Fn(;)g(x;)g(y)q(;)g(z)r Fr(\))k Fo(!)g Fn(E)1211 2133 y Fm(2)1229 2127 y Fr(\()p Fn(x;)c(x;)g(y)q(;)g(z)r(;)g(z)r Fr(\))787 2177 y Fn(E)818 2183 y Fm(1)836 2177 y Fr(\()p Fn(x)876 2183 y Fm(1)894 2177 y Fn(;)g(x)937 2183 y Fm(1)955 2177 y Fn(;)g(x;)g(y)q(;)g(z)r Fr(\))33 b Fo(!)11 b Fn(E)1211 2183 y Fm(5)1229 2177 y Fr(\()p Fn(x)1269 2183 y Fm(1)1287 2177 y Fn(;)c(x;)g(y)q(;)g(z)r Fr(\))787 2276 y Fn(E)818 2282 y Fm(2)836 2276 y Fr(\()p Fn(F)879 2282 y Fm(1)897 2276 y Fn(;)g(x;)g(y)q(;)g(z)r(;)g(F)1066 2282 y Fm(2)1083 2276 y Fr(\))28 b Fo(!)11 b Fn(E)1211 2282 y Fm(3)1229 2276 y Fr(\()p Fn(x;)c(y)q(;)g(x;)g(y)q(;)g(y)q(;)g(z)r(;)g(y)q(;)g(z)r (;)g(x;)g(y)q(;)g(z)r Fr(\))787 2326 y Fn(E)818 2332 y Fm(2)836 2326 y Fr(\()p Fn(x;)g(x;)g(y)q(;)g(z)r(;)g(z)r Fr(\))72 b Fo(!)11 b Fn(E)1211 2332 y Fm(6)1229 2326 y Fr(\()p Fn(x;)c(y)q(;)g(z)r Fr(\))787 2376 y Fn(E)818 2382 y Fm(2)836 2376 y Fr(\()p Fn(I)s(;)g(x;)g(y)q(;)g(z)r(;)g(I)s Fr(\))75 b Fo(!)11 b Fn(E)1211 2382 y Fm(6)1229 2376 y Fr(\()p Fn(x;)c(y)q(;)g(z)r Fr(\))1050 2556 y(2)p eop %%Page: 3 3 3 2 bop 188 187 a Fn(E)219 193 y Fm(3)238 187 y Fr(\()p Fn(x)278 193 y Fm(1)296 187 y Fn(;)7 b(x)339 193 y Fm(1)357 187 y Fn(;)g(x)400 193 y Fm(2)418 187 y Fn(;)g(x)461 193 y Fm(2)479 187 y Fn(;)g(x)522 193 y Fm(3)539 187 y Fn(;)g(x)582 193 y Fm(3)600 187 y Fn(;)g(x)643 193 y Fm(4)661 187 y Fn(;)g(x)704 193 y Fm(4)722 187 y Fn(;)g(x;)g(y)q(;)g (z)r Fr(\))46 b Fo(!)11 b Fn(E)991 193 y Fm(4)1010 187 y Fr(\()p Fn(x)1050 193 y Fm(1)1068 187 y Fn(;)c(x)1111 193 y Fm(1)1129 187 y Fn(;)g(x)1172 193 y Fm(2)1190 187 y Fn(;)g(x)1233 193 y Fm(2)1251 187 y Fn(;)g(x)1294 193 y Fm(3)1311 187 y Fn(;)g(x)1354 193 y Fm(3)1372 187 y Fn(;)g(x)1415 193 y Fm(4)1433 187 y Fn(;)g(x)1476 193 y Fm(4)1494 187 y Fn(;)g(x;)g(y)q(;)g(z)r Fr(\))188 237 y Fn(E)219 243 y Fm(3)238 237 y Fr(\()p Fn(x;)g(y)q(;)g(x;)g(y)q(;)g(y) q(;)g(z)r(;)g(y)q(;)g(z)r(;)g(x;)g(y)q(;)g(z)r Fr(\))207 b Fo(!)11 b Fn(E)991 243 y Fm(6)1010 237 y Fr(\()p Fn(x;)c(y)q(;)g(z)r Fr(\))188 287 y Fn(E)219 293 y Fm(4)238 287 y Fr(\()p Fn(G)287 293 y Fm(1)305 287 y Fn(;)g(x)348 293 y Fm(1)366 287 y Fn(;)g(G)418 293 y Fm(2)436 287 y Fn(;)g(x)479 293 y Fm(1)496 287 y Fn(;)g(G)548 293 y Fm(1)566 287 y Fn(;)g(x)609 293 y Fm(1)627 287 y Fn(;)g(G)679 293 y Fm(2)697 287 y Fn(;)g(x)740 293 y Fm(1)757 287 y Fn(;)g(x;)g(y)q(;)g (z)r Fr(\))k Fo(!)g Fn(E)991 293 y Fm(1)1010 287 y Fr(\()p Fn(x)1050 293 y Fm(1)1068 287 y Fn(;)c(x)1111 293 y Fm(1)1129 287 y Fn(;)g(x;)g(y)q(;)g(z)r Fr(\))188 336 y Fn(E)219 342 y Fm(4)238 336 y Fr(\()p Fn(I)s(;)g(x)318 342 y Fm(1)336 336 y Fn(;)g(I)s(;)g(x)419 342 y Fm(1)437 336 y Fn(;)g(I)s(;)g(x)520 342 y Fm(1)538 336 y Fn(;)g(I)s(;)g(x)621 342 y Fm(1)638 336 y Fn(;)g(x;)g(y)q(;)g(z)r Fr(\))130 b Fo(!)11 b Fn(E)991 342 y Fm(5)1010 336 y Fr(\()p Fn(x)1050 342 y Fm(1)1068 336 y Fn(;)c(x;)g(y)q(;)g(z)r Fr(\))188 386 y Fn(E)219 392 y Fm(4)238 386 y Fr(\()p Fn(x;)g(x;)g(x;)g(x;)g(x)o(;)g(x)o(;)g(x;) f(x;)g(x;)g(x;)h(x)o Fr(\))189 b Fo(!)11 b Fn(E)991 392 y Fm(6)1010 386 y Fr(\()p Fn(x;)c(x;)g(x)p Fr(\))188 436 y Fn(E)219 442 y Fm(5)238 436 y Fr(\()p Fn(I)s(;)g(x;)g(y)q(;)g(z)r Fr(\))493 b Fo(!)11 b Fn(E)991 442 y Fm(6)1010 436 y Fr(\()p Fn(x;)c(y)q(;)g(z)r Fr(\))183 517 y(Moreo)o(v)o(er,)14 b(consider)g(the)h(TRS)e(consisting)h(of)f Fo(F)976 523 y Fm(2)1006 517 y Fr(=)f Fo(f)p Fn(f)r(;)7 b(g)1132 523 y Fm(1)1150 517 y Fn(;)g(g)1189 523 y Fm(2)1207 517 y Fn(;)g(h)p Fo(g)13 b Fr(and)435 813 y Fo(R)470 819 y Fm(2)501 813 y Fr(=)545 578 y Fi(8)545 615 y(>)545 628 y(>)545 640 y(>)545 653 y(>)545 665 y(>)545 678 y(>)545 690 y(>)545 702 y(>)545 715 y(>)545 727 y(>)545 740 y(>)545 752 y(>)545 765 y(<)545 839 y(>)545 852 y(>)545 864 y(>)545 877 y(>)545 889 y(>)545 902 y(>)545 914 y(>)545 927 y(>)545 939 y(>)545 952 y(>)545 964 y(>)545 976 y(>)545 989 y(:)587 613 y Fn(f)t Fr(\()p Fn(x;)7 b(y)q Fr(\))69 b Fo(!)11 b Fn(g)849 619 y Fm(1)867 613 y Fr(\()p Fn(x;)c(x;)g(y)q Fr(\))587 663 y Fn(f)t Fr(\()p Fn(x;)g(y)q Fr(\))69 b Fo(!)11 b Fn(g)849 669 y Fm(1)867 663 y Fr(\()p Fn(y)q(;)c(x;)g(x)p Fr(\))587 712 y Fn(f)t Fr(\()p Fn(x;)g(y)q Fr(\))69 b Fo(!)11 b Fn(g)849 718 y Fm(2)867 712 y Fr(\()p Fn(x;)c(y)q(;)g(y)q Fr(\))587 762 y Fn(f)t Fr(\()p Fn(x;)g(y)q Fr(\))69 b Fo(!)11 b Fn(g)849 768 y Fm(2)867 762 y Fr(\()p Fn(y)q(;)c(y)q(;)g(x)p Fr(\))587 812 y Fn(g)607 818 y Fm(1)626 812 y Fr(\()p Fn(x;)g(x;)g(y)q Fr(\))k Fo(!)g Fn(h)p Fr(\()p Fn(x;)c(y)q Fr(\))587 862 y Fn(g)607 868 y Fm(1)626 862 y Fr(\()p Fn(y)q(;)g(x;)g(x)p Fr(\))k Fo(!)g Fn(h)p Fr(\()p Fn(x;)c(y)q Fr(\))587 912 y Fn(g)607 918 y Fm(2)626 912 y Fr(\()p Fn(x;)g(y)q(;)g(y)q Fr(\))14 b Fo(!)d Fn(h)p Fr(\()p Fn(x;)c(y)q Fr(\))587 962 y Fn(g)607 968 y Fm(2)626 962 y Fr(\()p Fn(y)q(;)g(y)q(;)g(x)p Fr(\))14 b Fo(!)d Fn(h)p Fr(\()p Fn(x;)c(y)q Fr(\))587 1011 y Fn(h)p Fr(\()p Fn(x;)g(x)p Fr(\))66 b Fo(!)11 b Fn(x)183 1106 y Fr(Both)16 b(TRSs)f(are)h(v)n (ariable-preserving)g(and)f Fo(R)949 1112 y Fm(2)984 1106 y Fr(is)g(clearly)h(terminating.)d(T)m(ermination)183 1155 y(of)i Fo(R)267 1161 y Fm(1)301 1155 y Fr(is)h(pro)o(v)o(ed)g(in)f (Prop)q(osition)h(2.3.)e(In)i(order)h(to)e(pro)o(v)o(e)h(that)g Fo(R)1296 1161 y Fm(1)1331 1155 y Fr(and)f Fo(R)1448 1161 y Fm(2)1483 1155 y Fr(are)h(also)183 1205 y(con\015uen)o(t,)j(it)f (is)h(su\016cien)o(t)g(to)g(sho)o(w)g(that)f(all)g(their)h(critical)g (pairs)f(are)i(con)o(v)o(ergen)o(t.)1605 1190 y Fm(1)183 1255 y Fr(This)13 b(task)h(is)f(left)h(to)f(the)i(reader)f(or)g (suitable)g(theorem)f(pro)o(v)o(ers.)h(Ho)o(w)o(ev)o(er,)f Fo(R)1464 1261 y Fm(1)1492 1255 y Fo(])8 b(R)1563 1261 y Fm(2)1596 1255 y Fr(is)183 1305 y(not)16 b(terminating.)f(With)g(the) j(abbreviations)e Fn(s)963 1311 y Fm(1)998 1305 y Fo(\021)g Fn(f)t Fr(\()p Fn(F)1113 1311 y Fm(1)1133 1305 y Fn(;)7 b(F)1179 1311 y Fm(1)1196 1305 y Fr(\),)17 b Fn(s)1260 1311 y Fm(2)1295 1305 y Fo(\021)f Fn(f)t Fr(\()p Fn(F)1410 1311 y Fm(1)1429 1305 y Fn(;)7 b(F)1475 1311 y Fm(2)1493 1305 y Fr(\),)16 b Fn(s)1556 1311 y Fm(3)1591 1305 y Fo(\021)183 1355 y Fn(f)t Fr(\()p Fn(F)250 1361 y Fm(2)269 1355 y Fn(;)7 b(F)315 1361 y Fm(2)333 1355 y Fr(\),)19 b Fn(t)395 1361 y Fm(1)436 1355 y Fo(\021)j Fn(g)510 1361 y Fm(1)529 1355 y Fr(\()p Fn(F)572 1361 y Fm(1)590 1355 y Fn(;)7 b(F)636 1361 y Fm(1)654 1355 y Fn(;)g(F)700 1361 y Fm(1)718 1355 y Fr(\),)20 b Fn(t)781 1361 y Fm(2)821 1355 y Fo(\021)i Fn(g)895 1361 y Fm(1)914 1355 y Fr(\()p Fn(F)957 1361 y Fm(2)975 1355 y Fn(;)7 b(F)1021 1361 y Fm(1)1039 1355 y Fn(;)g(F)1085 1361 y Fm(1)1103 1355 y Fr(\),)20 b Fn(t)1166 1361 y Fm(3)1206 1355 y Fo(\021)j Fn(g)1281 1361 y Fm(1)1299 1355 y Fr(\()p Fn(F)1342 1361 y Fm(1)1360 1355 y Fn(;)7 b(F)1406 1361 y Fm(1)1424 1355 y Fn(;)g(F)1470 1361 y Fm(2)1488 1355 y Fr(\),)20 b Fn(t)1551 1361 y Fm(4)1591 1355 y Fo(\021)183 1404 y Fn(g)203 1410 y Fm(2)221 1404 y Fr(\()p Fn(F)264 1410 y Fm(1)283 1404 y Fn(;)7 b(F)329 1410 y Fm(2)346 1404 y Fn(;)g(F)392 1410 y Fm(2)410 1404 y Fr(\),)13 b Fn(t)466 1410 y Fm(5)496 1404 y Fo(\021)f Fn(g)560 1410 y Fm(2)578 1404 y Fr(\()p Fn(F)621 1410 y Fm(2)640 1404 y Fn(;)7 b(F)686 1410 y Fm(2)704 1404 y Fn(;)g(F)750 1410 y Fm(1)767 1404 y Fr(\),)13 b Fn(t)823 1410 y Fm(6)853 1404 y Fo(\021)f Fn(g)917 1410 y Fm(2)936 1404 y Fr(\()p Fn(F)979 1410 y Fm(2)997 1404 y Fn(;)7 b(F)1043 1410 y Fm(2)1061 1404 y Fn(;)g(F)1107 1410 y Fm(2)1125 1404 y Fr(\),)12 b Fn(u)1189 1410 y Fm(1)1219 1404 y Fo(\021)g Fn(g)1283 1410 y Fm(1)1302 1404 y Fr(\()p Fn(G)1351 1410 y Fm(1)1369 1404 y Fn(;)7 b(F)1415 1410 y Fm(1)1433 1404 y Fn(;)g(F)1479 1410 y Fm(1)1497 1404 y Fr(\),)12 b Fn(u)1561 1410 y Fm(2)1591 1404 y Fo(\021)183 1454 y Fn(g)203 1460 y Fm(1)221 1454 y Fr(\()p Fn(F)264 1460 y Fm(1)283 1454 y Fn(;)7 b(F)329 1460 y Fm(1)346 1454 y Fn(;)g(G)398 1460 y Fm(2)416 1454 y Fr(\),)18 b Fn(u)486 1460 y Fm(3)522 1454 y Fo(\021)h Fn(g)593 1460 y Fm(2)612 1454 y Fr(\()p Fn(G)661 1460 y Fm(1)679 1454 y Fn(;)7 b(F)725 1460 y Fm(2)743 1454 y Fn(;)g(F)789 1460 y Fm(2)807 1454 y Fr(\),)17 b Fn(u)876 1460 y Fm(4)913 1454 y Fo(\021)i Fn(g)984 1460 y Fm(2)1002 1454 y Fr(\()p Fn(F)1045 1460 y Fm(2)1064 1454 y Fn(;)7 b(F)1110 1460 y Fm(2)1127 1454 y Fn(;)g(G)1179 1460 y Fm(2)1197 1454 y Fr(\),)18 b Fn(v)1263 1460 y Fm(1)1300 1454 y Fo(\021)h Fn(g)1371 1460 y Fm(1)1389 1454 y Fr(\()p Fn(G)1438 1460 y Fm(1)1456 1454 y Fn(;)7 b(G)1508 1460 y Fm(1)1526 1454 y Fn(;)g(G)1578 1460 y Fm(2)1596 1454 y Fr(\),)183 1504 y Fn(v)203 1510 y Fm(2)233 1504 y Fo(\021)12 b Fn(g)297 1510 y Fm(2)315 1504 y Fr(\()p Fn(G)364 1510 y Fm(1)383 1504 y Fn(;)7 b(G)435 1510 y Fm(2)452 1504 y Fn(;)g(G)504 1510 y Fm(2)522 1504 y Fr(\),)13 b Fn(v)583 1510 y Fm(3)614 1504 y Fo(\021)f Fn(h)p Fr(\()p Fn(G)731 1510 y Fm(1)749 1504 y Fn(;)7 b(G)801 1510 y Fm(2)819 1504 y Fr(\))14 b(w)o(e)g(obtain)f(the)h(cyclic)h(reduction)f(sequence) 478 1600 y Fn(E)509 1606 y Fm(1)527 1600 y Fr(\()p Fn(H)578 1606 y Fm(1)596 1600 y Fn(;)7 b(H)650 1606 y Fm(2)668 1600 y Fn(;)g(s)706 1606 y Fm(1)724 1600 y Fn(;)g(s)762 1606 y Fm(2)781 1600 y Fn(;)g(s)819 1606 y Fm(3)837 1600 y Fr(\))478 1649 y Fo(!)520 1655 y Fk(R)549 1659 y Fj(1)577 1649 y Fn(E)608 1655 y Fm(2)627 1649 y Fr(\()p Fn(s)662 1655 y Fm(1)681 1649 y Fn(;)g(s)719 1655 y Fm(1)737 1649 y Fn(;)g(s)775 1655 y Fm(2)794 1649 y Fn(;)g(s)832 1655 y Fm(3)851 1649 y Fn(;)g(s)889 1655 y Fm(3)907 1649 y Fr(\))478 1699 y Fo(!)520 1684 y Fk(\003)520 1711 y(R)549 1715 y Fj(2)577 1699 y Fn(E)608 1705 y Fm(2)627 1699 y Fr(\()p Fn(F)670 1705 y Fm(1)688 1699 y Fn(;)g(s)726 1705 y Fm(1)745 1699 y Fn(;)g(s)783 1705 y Fm(2)801 1699 y Fn(;)g(s)839 1705 y Fm(3)858 1699 y Fn(;)g(F)904 1705 y Fm(2)922 1699 y Fr(\))478 1750 y Fo(!)520 1756 y Fk(R)549 1760 y Fj(1)577 1750 y Fn(E)608 1756 y Fm(3)627 1750 y Fr(\()p Fn(s)662 1756 y Fm(1)681 1750 y Fn(;)g(s)719 1756 y Fm(2)737 1750 y Fn(;)g(s)775 1756 y Fm(1)794 1750 y Fn(;)g(s)832 1756 y Fm(2)851 1750 y Fn(;)g(s)889 1756 y Fm(2)907 1750 y Fn(;)g(s)945 1756 y Fm(3)964 1750 y Fn(;)g(s)1002 1756 y Fm(2)1020 1750 y Fn(;)g(s)1058 1756 y Fm(3)1077 1750 y Fn(;)g(s)1115 1756 y Fm(1)1133 1750 y Fn(;)g(s)1171 1756 y Fm(2)1190 1750 y Fn(;)g(s)1228 1756 y Fm(3)1246 1750 y Fr(\))478 1800 y Fo(!)520 1785 y Fk(\003)520 1811 y(R)549 1815 y Fj(2)577 1800 y Fn(E)608 1806 y Fm(3)627 1800 y Fr(\()p Fn(t)658 1806 y Fm(1)676 1800 y Fn(;)g(t)710 1806 y Fm(2)729 1800 y Fn(;)g(t)763 1806 y Fm(1)781 1800 y Fn(;)g(t)815 1806 y Fm(3)833 1800 y Fn(;)g(t)867 1806 y Fm(4)885 1800 y Fn(;)g(t)919 1806 y Fm(6)937 1800 y Fn(;)g(t)971 1806 y Fm(5)989 1800 y Fn(;)g(t)1023 1806 y Fm(6)1041 1800 y Fn(;)g(s)1079 1806 y Fm(1)1097 1800 y Fn(;)g(s)1135 1806 y Fm(2)1154 1800 y Fn(;)g(s)1192 1806 y Fm(3)1211 1800 y Fr(\))478 1850 y Fo(!)520 1835 y Fk(\003)520 1861 y(R)549 1865 y Fj(1)577 1850 y Fn(E)608 1856 y Fm(3)627 1850 y Fr(\()p Fn(u)667 1856 y Fm(1)685 1850 y Fn(;)g(u)728 1856 y Fm(1)746 1850 y Fn(;)g(u)789 1856 y Fm(2)807 1850 y Fn(;)g(u)850 1856 y Fm(2)868 1850 y Fn(;)g(u)911 1856 y Fm(3)929 1850 y Fn(;)g(u)972 1856 y Fm(3)989 1850 y Fn(;)g(u)1032 1856 y Fm(4)1050 1850 y Fn(;)g(u)1093 1856 y Fm(4)1111 1850 y Fn(;)g(s)1149 1856 y Fm(1)1168 1850 y Fn(;)g(s)1206 1856 y Fm(2)1224 1850 y Fn(;)g(s)1262 1856 y Fm(3)1281 1850 y Fr(\))478 1900 y Fo(!)520 1906 y Fk(R)549 1910 y Fj(1)577 1900 y Fn(E)608 1906 y Fm(4)627 1900 y Fr(\()p Fn(u)667 1906 y Fm(1)685 1900 y Fn(;)g(u)728 1906 y Fm(1)746 1900 y Fn(;)g(u)789 1906 y Fm(2)807 1900 y Fn(;)g(u)850 1906 y Fm(2)868 1900 y Fn(;)g(u)911 1906 y Fm(3)929 1900 y Fn(;)g(u)972 1906 y Fm(3)989 1900 y Fn(;)g(u)1032 1906 y Fm(4)1050 1900 y Fn(;)g(u)1093 1906 y Fm(4)1111 1900 y Fn(;)g(s)1149 1906 y Fm(1)1168 1900 y Fn(;)g(s)1206 1906 y Fm(2)1224 1900 y Fn(;)g(s)1262 1906 y Fm(3)1281 1900 y Fr(\))478 1950 y Fo(!)520 1935 y Fk(\003)520 1962 y(R)574 1950 y Fn(E)605 1956 y Fm(4)623 1950 y Fr(\()p Fn(G)672 1956 y Fm(1)690 1950 y Fn(;)g(u)733 1956 y Fm(1)751 1950 y Fn(;)g(G)803 1956 y Fm(2)821 1950 y Fn(;)g(u)864 1956 y Fm(2)882 1950 y Fn(;)g(G)934 1956 y Fm(1)951 1950 y Fn(;)g(u)994 1956 y Fm(3)1012 1950 y Fn(;)g(G)1064 1956 y Fm(2)1082 1950 y Fn(;)g(u)1125 1956 y Fm(4)1143 1950 y Fn(;)g(s)1181 1956 y Fm(1)1199 1950 y Fn(;)g(s)1237 1956 y Fm(2)1256 1950 y Fn(;)g(s)1294 1956 y Fm(3)1312 1950 y Fr(\))478 2000 y Fo(!)520 1985 y Fk(\003)520 2012 y(R)549 2016 y Fj(1)577 2000 y Fn(E)608 2006 y Fm(4)627 2000 y Fr(\()p Fn(G)676 2006 y Fm(1)694 2000 y Fn(;)g(v)733 2006 y Fm(1)751 2000 y Fn(;)g(G)803 2006 y Fm(2)821 2000 y Fn(;)g(v)860 2006 y Fm(1)878 2000 y Fn(;)g(G)930 2006 y Fm(1)948 2000 y Fn(;)g(v)987 2006 y Fm(2)1005 2000 y Fn(;)g(G)1057 2006 y Fm(2)1075 2000 y Fn(;)g(v)1114 2006 y Fm(2)1132 2000 y Fn(;)g(s)1170 2006 y Fm(1)1189 2000 y Fn(;)g(s)1227 2006 y Fm(2)1245 2000 y Fn(;)g(s)1283 2006 y Fm(3)1302 2000 y Fr(\))478 2051 y Fo(!)520 2035 y Fk(\003)520 2062 y(R)549 2066 y Fj(2)577 2051 y Fn(E)608 2057 y Fm(4)627 2051 y Fr(\()p Fn(G)676 2057 y Fm(1)694 2051 y Fn(;)g(v)733 2057 y Fm(3)751 2051 y Fn(;)g(G)803 2057 y Fm(2)821 2051 y Fn(;)g(v)860 2057 y Fm(3)878 2051 y Fn(;)g(G)930 2057 y Fm(1)948 2051 y Fn(;)g(v)987 2057 y Fm(3)1005 2051 y Fn(;)g(G)1057 2057 y Fm(2)1075 2051 y Fn(;)g(v)1114 2057 y Fm(3)1132 2051 y Fn(;)g(s)1170 2057 y Fm(1)1189 2051 y Fn(;)g(s)1227 2057 y Fm(2)1245 2051 y Fn(;)g(s)1283 2057 y Fm(3)1302 2051 y Fr(\))478 2101 y Fo(!)520 2107 y Fk(R)549 2111 y Fj(1)577 2101 y Fn(E)608 2107 y Fm(1)627 2101 y Fr(\()p Fn(v)663 2107 y Fm(3)682 2101 y Fn(;)g(v)721 2107 y Fm(3)739 2101 y Fn(;)g(s)777 2107 y Fm(1)795 2101 y Fn(;)g(s)833 2107 y Fm(2)852 2101 y Fn(;)g(s)890 2107 y Fm(3)908 2101 y Fr(\))478 2151 y Fo(!)520 2136 y Fk(\003)520 2162 y(R)574 2151 y Fn(E)605 2157 y Fm(1)623 2151 y Fr(\()p Fn(H)674 2157 y Fm(1)692 2151 y Fn(;)g(H)746 2157 y Fm(2)764 2151 y Fn(;)g(s)802 2157 y Fm(1)820 2151 y Fn(;)g(s)858 2157 y Fm(2)877 2151 y Fn(;)g(s)915 2157 y Fm(3)933 2151 y Fr(\))245 2247 y(The)18 b(reader)h(ma)o(y)c(ha)o(v)o(e)j(observ)o(ed)g (that)g(all)e(those)j(rules)f(of)f Fo(R)1289 2253 y Fm(1)1325 2247 y Fr(with)g(an)g Fn(E)1515 2253 y Fm(5)1534 2247 y Fr(,)g Fn(E)1594 2253 y Fm(6)1612 2247 y Fr(,)183 2297 y(or)d Fn(I)j Fr(op)q(erator)e(at)e(its)i(righ)o(t-hand)e(side)h(are)h (added)f(solely)g(to)f(ensure)j(con\015uence.)f(Th)o(us)183 2347 y(the)g(omission)f(of)g(those)i(rules)g(and)f(the)h(replacemen)o (t)f(of)f Fo(R)1156 2353 y Fm(2)1190 2347 y Fr(with)h(the)h(term)f (rewriting)p 183 2389 237 2 v 191 2416 a Ff(1)221 2432 y Fq(This)f(follo)o(ws)g(from)f(Newman's)f(Lemma)h(in)h(conjunction)h (with)f(the)f(Critical)h(P)o(air)g(Lemma.)893 2556 y Fr(3)p eop %%Page: 4 4 4 3 bop 340 194 a Fr(system)13 b Fo(f)p Fn(f)t Fr(\()p Fn(x;)7 b(y)q Fr(\))12 b Fo(!)f Fn(h)p Fr(\()p Fn(x;)c(y)q Fr(\))p Fn(;)g(f)t Fr(\()p Fn(x;)g(y)q Fr(\))12 b Fo(!)f Fn(h)p Fr(\()p Fn(y)q(;)c(x)p Fr(\))p Fn(;)g(h)p Fr(\()p Fn(x;)g(x)p Fr(\))k Fo(!)g Fn(x)p Fo(g)h Fr(yields)g(a)g(simpler)f (coun-)340 244 y(terexample)17 b(to)g(the)h(mo)q(dularit)o(y)d(of)h (termination)g(of)g(v)n(ariable-preserving)h(TRSs.)g(Let)340 293 y(us)e(turn)f(to)g(pro)o(ving)f(the)h(termination)e(of)i(the)g(TRS) g Fo(R)1236 299 y Fm(1)1268 293 y Fr(from)e(Example)h(2.1.)340 388 y Fl(Lemma)j(2.2)k Fr(F)m(or)14 b(all)f Fn(s)743 394 y Fm(1)762 388 y Fn(;)7 b(s)800 394 y Fm(2)818 388 y Fn(;)g(s)856 394 y Fm(3)875 388 y Fn(;)g(w)924 394 y Fm(1)941 388 y Fn(;)g(w)990 394 y Fm(2)1008 388 y Fn(;)g(w)1057 394 y Fm(3)1087 388 y Fo(2)k(T)f Fr(\()p Fo(F)1205 394 y Fm(1)1224 388 y Fn(;)d Fo(V)s Fr(\))14 b(w)o(e)g(ha)o(v)o(e)385 477 y Fn(E)416 483 y Fm(1)435 477 y Fr(\()p Fn(H)486 483 y Fm(1)504 477 y Fn(;)7 b(H)558 483 y Fm(2)576 477 y Fn(;)g(s)614 483 y Fm(1)632 477 y Fn(;)g(s)670 483 y Fm(2)689 477 y Fn(;)g(s)727 483 y Fm(3)745 477 y Fr(\))12 b Fo(!)815 483 y Fk(R)844 487 y Fj(1)873 477 y Fn(E)904 483 y Fm(2)922 477 y Fr(\()p Fn(s)957 483 y Fm(1)976 477 y Fn(;)7 b(s)1014 483 y Fm(1)1033 477 y Fn(;)g(s)1071 483 y Fm(2)1089 477 y Fn(;)g(s)1127 483 y Fm(3)1146 477 y Fn(;)g(s)1184 483 y Fm(3)1202 477 y Fr(\))12 b Fo(6!)1272 460 y Fm(+)1272 489 y Fk(R)1301 493 y Fj(1)1330 477 y Fn(E)1361 483 y Fm(1)1379 477 y Fr(\()p Fn(H)1430 483 y Fm(1)1448 477 y Fn(;)7 b(H)1502 483 y Fm(2)1520 477 y Fn(;)g(w)1569 483 y Fm(1)1587 477 y Fn(;)g(w)1636 483 y Fm(2)1653 477 y Fn(;)g(w)1702 483 y Fm(3)1720 477 y Fr(\))340 567 y Fl(Pro)q(of:)13 b Fr(W)m(e)f(pro)o(v)o(e)h(the)h(lemma) c(b)o(y)j(con)o(tradiction.)f(So)h(assume)g(that)g(there)h(exist)g (terms)340 617 y Fn(s)359 623 y Fm(1)378 617 y Fn(;)7 b(s)416 623 y Fm(2)435 617 y Fn(;)g(s)473 623 y Fm(3)492 617 y Fr(,)p Fn(w)534 623 y Fm(1)551 617 y Fn(;)g(w)600 623 y Fm(2)618 617 y Fn(;)g(w)667 623 y Fm(3)697 617 y Fo(2)k(T)f Fr(\()p Fo(F)815 623 y Fm(1)833 617 y Fn(;)d Fo(V)s Fr(\))15 b(suc)o(h)f(that)385 706 y Fn(E)416 712 y Fm(1)435 706 y Fr(\()p Fn(H)486 712 y Fm(1)504 706 y Fn(;)7 b(H)558 712 y Fm(2)576 706 y Fn(;)g(s)614 712 y Fm(1)632 706 y Fn(;)g(s)670 712 y Fm(2)689 706 y Fn(;)g(s)727 712 y Fm(3)745 706 y Fr(\))12 b Fo(!)815 712 y Fk(R)844 716 y Fj(1)873 706 y Fn(E)904 712 y Fm(2)922 706 y Fr(\()p Fn(s)957 712 y Fm(1)976 706 y Fn(;)7 b(s)1014 712 y Fm(1)1033 706 y Fn(;)g(s)1071 712 y Fm(2)1089 706 y Fn(;)g(s)1127 712 y Fm(3)1146 706 y Fn(;)g(s)1184 712 y Fm(3)1202 706 y Fr(\))12 b Fo(!)1272 689 y Fm(+)1272 719 y Fk(R)1301 723 y Fj(1)1330 706 y Fn(E)1361 712 y Fm(1)1379 706 y Fr(\()p Fn(H)1430 712 y Fm(1)1448 706 y Fn(;)7 b(H)1502 712 y Fm(2)1520 706 y Fn(;)g(w)1569 712 y Fm(1)1587 706 y Fn(;)g(w)1636 712 y Fm(2)1653 706 y Fn(;)g(w)1702 712 y Fm(3)1720 706 y Fr(\))340 796 y(Then)14 b(there)g(m)o(ust)e(b)q(e)i (terms)f Fn(t)841 802 y Fm(1)859 796 y Fn(;)7 b(t)893 802 y Fm(2)911 796 y Fn(;)g(t)945 802 y Fm(3)963 796 y Fn(;)g(u)1006 802 y Fm(1)1024 796 y Fn(;)g(:)g(:)g(:)e(;)i(u)1141 802 y Fm(7)1159 796 y Fn(;)g(v)1198 802 y Fm(1)1216 796 y Fn(;)g(v)1255 802 y Fm(2)1273 796 y Fn(;)g(v)1312 802 y Fm(3)1330 796 y Fn(;)g(v)1369 802 y Fm(4)1399 796 y Fo(2)k(T)f Fr(\()p Fo(F)1517 802 y Fm(1)1536 796 y Fn(;)d Fo(V)s Fr(\))13 b(suc)o(h)h(that)640 885 y Fn(E)671 891 y Fm(1)689 885 y Fr(\()p Fn(H)740 891 y Fm(1)758 885 y Fn(;)7 b(H)812 891 y Fm(2)830 885 y Fn(;)g(s)868 891 y Fm(1)886 885 y Fn(;)g(s)924 891 y Fm(2)943 885 y Fn(;)g(s)981 891 y Fm(3)1000 885 y Fr(\))640 934 y Fo(!)682 940 y Fk(R)711 944 y Fj(1)740 934 y Fn(E)771 940 y Fm(2)789 934 y Fr(\()p Fn(s)824 940 y Fm(1)843 934 y Fn(;)g(s)881 940 y Fm(1)900 934 y Fn(;)g(s)938 940 y Fm(2)956 934 y Fn(;)g(s)994 940 y Fm(3)1013 934 y Fn(;)g(s)1051 940 y Fm(3)1069 934 y Fr(\))640 984 y Fo(!)682 969 y Fk(\003)682 996 y(R)711 1000 y Fj(1)740 984 y Fn(E)771 990 y Fm(2)789 984 y Fr(\()p Fn(F)832 990 y Fm(1)850 984 y Fn(;)g(t)884 990 y Fm(1)902 984 y Fn(;)g(t)936 990 y Fm(2)954 984 y Fn(;)g(t)988 990 y Fm(3)1007 984 y Fn(;)g(F)1053 990 y Fm(2)1070 984 y Fr(\))640 1035 y Fo(!)682 1041 y Fk(R)711 1045 y Fj(1)740 1035 y Fn(E)771 1041 y Fm(3)789 1035 y Fr(\()p Fn(t)820 1041 y Fm(1)839 1035 y Fn(;)g(t)873 1041 y Fm(2)891 1035 y Fn(;)g(t)925 1041 y Fm(1)943 1035 y Fn(;)g(t)977 1041 y Fm(2)995 1035 y Fn(;)g(t)1029 1041 y Fm(2)1047 1035 y Fn(;)g(t)1081 1041 y Fm(3)1099 1035 y Fn(;)g(t)1133 1041 y Fm(2)1151 1035 y Fn(;)g(t)1185 1041 y Fm(3)1203 1035 y Fn(;)g(t)1237 1041 y Fm(1)1255 1035 y Fn(;)g(t)1289 1041 y Fm(2)1307 1035 y Fn(;)g(t)1341 1041 y Fm(3)1359 1035 y Fr(\))640 1084 y Fo(!)682 1069 y Fk(\003)682 1096 y(R)711 1100 y Fj(1)740 1084 y Fn(E)771 1090 y Fm(3)789 1084 y Fr(\()p Fn(u)829 1090 y Fm(1)847 1084 y Fn(;)g(u)890 1090 y Fm(1)908 1084 y Fn(;)g(u)951 1090 y Fm(2)969 1084 y Fn(;)g(u)1012 1090 y Fm(2)1030 1084 y Fn(;)g(u)1073 1090 y Fm(3)1091 1084 y Fn(;)g(u)1134 1090 y Fm(3)1152 1084 y Fn(;)g(u)1195 1090 y Fm(4)1212 1084 y Fn(;)g(u)1255 1090 y Fm(4)1273 1084 y Fn(;)g(u)1316 1090 y Fm(5)1334 1084 y Fn(;)g(u)1377 1090 y Fm(6)1395 1084 y Fn(;)g(u)1438 1090 y Fm(7)1456 1084 y Fr(\))640 1135 y Fo(!)682 1141 y Fk(R)711 1145 y Fj(1)740 1135 y Fn(E)771 1141 y Fm(4)789 1135 y Fr(\()p Fn(u)829 1141 y Fm(1)847 1135 y Fn(;)g(u)890 1141 y Fm(1)908 1135 y Fn(;)g(u)951 1141 y Fm(2)969 1135 y Fn(;)g(u)1012 1141 y Fm(2)1030 1135 y Fn(;)g(u)1073 1141 y Fm(3)1091 1135 y Fn(;)g(u)1134 1141 y Fm(3)1152 1135 y Fn(;)g(u)1195 1141 y Fm(4)1212 1135 y Fn(;)g(u)1255 1141 y Fm(4)1273 1135 y Fn(;)g(u)1316 1141 y Fm(5)1334 1135 y Fn(;)g(u)1377 1141 y Fm(6)1395 1135 y Fn(;)g(u)1438 1141 y Fm(7)1456 1135 y Fr(\))640 1185 y Fo(!)682 1170 y Fk(\003)682 1196 y(R)711 1200 y Fj(1)740 1185 y Fn(E)771 1191 y Fm(4)789 1185 y Fr(\()p Fn(G)838 1191 y Fm(1)856 1185 y Fn(;)g(v)895 1191 y Fm(1)913 1185 y Fn(;)g(G)965 1191 y Fm(2)983 1185 y Fn(;)g(v)1022 1191 y Fm(1)1040 1185 y Fn(;)g(G)1092 1191 y Fm(1)1110 1185 y Fn(;)g(v)1149 1191 y Fm(1)1167 1185 y Fn(;)g(G)1219 1191 y Fm(2)1237 1185 y Fn(;)g(v)1276 1191 y Fm(1)1294 1185 y Fn(;)g(v)1333 1191 y Fm(2)1351 1185 y Fn(;)g(v)1390 1191 y Fm(3)1409 1185 y Fn(;)g(v)1448 1191 y Fm(4)1466 1185 y Fr(\))640 1235 y Fo(!)682 1241 y Fk(R)711 1245 y Fj(1)740 1235 y Fn(E)771 1241 y Fm(1)789 1235 y Fr(\()p Fn(v)825 1241 y Fm(1)844 1235 y Fn(;)g(v)883 1241 y Fm(1)901 1235 y Fn(;)g(v)940 1241 y Fm(2)958 1235 y Fn(;)g(v)997 1241 y Fm(3)1015 1235 y Fn(;)g(v)1054 1241 y Fm(4)1073 1235 y Fr(\))640 1285 y Fo(!)682 1270 y Fk(\003)682 1296 y(R)711 1300 y Fj(1)740 1285 y Fn(E)771 1291 y Fm(1)789 1285 y Fr(\()p Fn(H)840 1291 y Fm(1)858 1285 y Fn(;)g(H)912 1291 y Fm(2)930 1285 y Fn(;)g(w)979 1291 y Fm(1)997 1285 y Fn(;)g(w)1046 1291 y Fm(2)1063 1285 y Fn(;)g(w)1112 1291 y Fm(3)1130 1285 y Fr(\))340 1373 y(and)14 b(the)h(follo)o(wing)c(dep)q(endencies)16 b(m)o(ust)d(hold:)549 1776 y Fg(H)591 1796 y(H)632 1817 y(H)674 1838 y(H)695 1848 y(H)-42 b(j)680 1796 y(@)714 1830 y(@)g(R)976 1776 y(\010)935 1796 y(\010)893 1817 y(\010)852 1838 y(\010)830 1848 y(\010)g(\031)845 1796 y(\000)812 1830 y(\000)g(\011)470 1486 y(\032)429 1517 y(\032)395 1543 y(\032)g(=)p 522 1534 2 75 v 523 1534 a(?)p 522 1684 V 523 1684 a(?)p 522 1834 V 523 1834 a(?)p 784 1530 V 785 1530 a(?)p 1047 1834 V 1048 1834 a(?)p 1047 1684 V 1048 1684 a(?)p 1047 1534 V 1048 1534 a(?)714 1626 y(\010)672 1646 y(\010)631 1667 y(\010)589 1688 y(\010)557 1704 y(\010)g(\031)724 1646 y(\023)693 1688 y(\023)683 1701 y(\023)-31 b(/)804 1626 y(H)846 1646 y(H)887 1667 y(H)929 1688 y(H)970 1709 y(H)976 1712 y(H)-42 b(j)804 1646 y(S)835 1688 y(S)845 1701 y(S)-31 b(w)733 1946 y(\000)699 1980 y(\000)-42 b(\011)812 1946 y(@)845 1980 y(@)g(R)530 1646 y(@)572 1688 y(@)598 1714 y(@)g(R)995 1646 y(\000)953 1688 y(\000)927 1714 y(\000)g(\011)1074 1486 y(Z)1115 1517 y(Z)1149 1543 y(Z)g(~)819 1750 y(\020)777 1764 y(\020)736 1778 y(\020)694 1791 y(\020)653 1805 y(\020)611 1819 y(\020)570 1833 y(\020)560 1836 y(\020)g(\))699 1750 y(P)741 1764 y(P)782 1778 y(P)824 1791 y(P)865 1805 y(P)907 1819 y(P)948 1833 y(P)976 1842 y(P)g(q)568 1822 y Fo(\003)999 1830 y(\003)515 1440 y Fn(s)534 1446 y Fm(1)365 1590 y Fn(F)392 1596 y Fm(1)515 1590 y Fn(t)530 1596 y Fm(1)515 1890 y Fn(G)548 1896 y Fm(1)399 1522 y Fo(\003)493 1530 y(\003)493 1680 y(\003)770 1440 y Fn(s)789 1446 y Fm(2)493 1830 y Fo(\003)770 1590 y Fn(t)785 1596 y Fm(2)1040 1440 y Fn(s)1059 1446 y Fm(3)1040 1590 y Fn(t)1055 1596 y Fm(3)1040 1890 y Fn(G)1073 1896 y Fm(2)1190 1590 y Fn(F)1217 1596 y Fm(2)890 2040 y Fn(H)925 2046 y Fm(2)647 2040 y Fn(H)682 2046 y Fm(1)1059 1530 y Fo(\003)1059 1680 y(\003)1059 1830 y(\003)680 1972 y(\003)186 b(\003)737 1811 y(\003)54 b(\003)699 1830 y(\003)129 b(\003)1168 1522 y(\003)755 1530 y(\003)643 1699 y(\003)54 b(\003)91 b(\003)54 b(\003)568 1687 y(\003)395 b(\003)515 1740 y Fn(u)539 1746 y Fm(1)647 1740 y Fn(u)671 1746 y Fm(2)872 1740 y Fn(u)896 1746 y Fm(3)1040 1740 y Fn(u)1064 1746 y Fm(4)778 1890 y Fn(v)798 1896 y Fm(1)p 1384 1534 V 1385 1534 a Fg(?)p 1384 1684 V 1385 1684 a(?)p 1384 1834 V 1385 1834 a(?)p 1384 1983 V 1385 1983 a(?)p 1684 1534 V 1685 1534 a(?)p 1684 1684 V 1685 1684 a(?)p 1684 1834 V 1685 1834 a(?)p 1684 1983 V 1685 1983 a(?)p 1534 1534 V 1535 1534 a(?)p 1534 1684 V 1535 1684 a(?)p 1534 1834 V 1535 1834 a(?)p 1534 1983 V 1535 1983 a(?)1378 1440 y Fn(s)1397 1446 y Fm(1)1528 1440 y Fn(s)1547 1446 y Fm(2)1678 1440 y Fn(s)1697 1446 y Fm(3)1378 1590 y Fn(t)1393 1596 y Fm(1)1528 1590 y Fn(t)1543 1596 y Fm(2)1678 1590 y Fn(t)1693 1596 y Fm(3)1378 1740 y Fn(u)1402 1746 y Fm(5)1528 1740 y Fn(u)1552 1746 y Fm(6)1678 1740 y Fn(u)1702 1746 y Fm(7)1378 1890 y Fn(v)1398 1896 y Fm(2)1528 1890 y Fn(v)1548 1896 y Fm(3)1678 1890 y Fn(v)1698 1896 y Fm(4)1378 2040 y Fn(w)1408 2046 y Fm(1)1528 2040 y Fn(w)1558 2046 y Fm(2)1678 2040 y Fn(w)1708 2046 y Fm(3)1351 1522 y Fo(\003)1351 1672 y(\003)1351 1822 y(\003)1351 1972 y(\003)1501 1522 y(\003)1501 1672 y(\003)1501 1822 y(\003)1501 1972 y(\003)1651 1522 y(\003)1651 1672 y(\003)1651 1822 y(\003)1651 1972 y(\003)340 2125 y Fr(Since)17 b(the)g(only)e (term)g(that)i(reduces)h(\(in)e(zero)g(or)h(more)e(steps\))i(to)f Fn(F)1480 2131 y Fm(1)1514 2125 y Fr(is)g Fn(F)1585 2131 y Fm(1)1620 2125 y Fr(itself,)f(w)o(e)340 2175 y(obtain)j Fn(s)493 2181 y Fm(1)532 2175 y Fo(\021)i Fn(F)611 2181 y Fm(1)629 2175 y Fr(.)e(It)h(follo)o(ws)e(analogously)g(that)i Fn(s)1194 2181 y Fm(3)1233 2175 y Fo(\021)g Fn(F)1311 2181 y Fm(2)1330 2175 y Fr(.)f(Since)h Fn(G)1506 2181 y Fm(1)1543 2175 y Fr(is)g(a)f(common)340 2224 y(reduct)g(of)e Fn(s)541 2230 y Fm(2)577 2224 y Fr(and)g Fn(s)679 2230 y Fm(1)715 2224 y Fo(\021)g Fn(F)790 2230 y Fm(1)808 2224 y Fr(,)g(and)h Fn(G)953 2230 y Fm(2)988 2224 y Fr(is)f(a)g(common) e(reduct)k(of)e Fn(s)1439 2230 y Fm(2)1475 2224 y Fr(and)g Fn(s)1577 2230 y Fm(3)1612 2224 y Fo(\021)h Fn(F)1688 2230 y Fm(2)1706 2224 y Fr(,)f(w)o(e)340 2274 y(deriv)o(e)g(that)g (either)h Fn(s)695 2280 y Fm(2)728 2274 y Fo(\021)e Fn(F)802 2280 y Fm(1)835 2274 y Fr(or)h Fn(s)907 2280 y Fm(2)940 2274 y Fo(\021)f Fn(F)1014 2280 y Fm(2)1032 2274 y Fr(.)g(W.l.o.g.)e (let)j Fn(s)1298 2280 y Fm(2)1331 2274 y Fo(\021)f Fn(F)1405 2280 y Fm(1)1423 2274 y Fr(.)g(As)h(a)f(consequence,)340 2324 y(w)o(e)g(obtain)e Fn(u)555 2330 y Fm(3)585 2324 y Fo(\021)f Fn(G)662 2330 y Fm(1)695 2324 y Fr(and)i Fn(u)800 2330 y Fm(4)830 2324 y Fo(\021)e Fn(G)907 2330 y Fm(2)925 2324 y Fr(.)i(No)o(w,)f(since)i Fn(v)1179 2330 y Fm(1)1212 2324 y Fr(is)f(a)g(common)d(reduct)k(of)f Fn(u)1656 2330 y Fm(3)1686 2324 y Fo(\021)e Fn(G)1763 2330 y Fm(1)340 2374 y Fr(and)i Fn(u)445 2380 y Fm(4)475 2374 y Fo(\021)e Fn(G)552 2380 y Fm(2)570 2374 y Fr(,)h(w)o(e)h(ha)o(v) o(e)f(either)i Fn(v)889 2380 y Fm(1)919 2374 y Fo(\021)d Fn(H)998 2380 y Fm(1)1029 2374 y Fr(or)i Fn(v)1100 2380 y Fm(1)1130 2374 y Fo(\021)e Fn(H)1209 2380 y Fm(2)1241 2374 y Fr(or)h Fn(v)1311 2380 y Fm(1)1342 2374 y Fo(\021)e Fn(I)s Fr(.)j(In)g(an)o(y)f(case)h Fn(v)1669 2380 y Fm(1)1702 2374 y Fr(do)q(es)340 2424 y(not)g(rewrite)h(to)f(b)q(oth)g Fn(H)739 2430 y Fm(1)771 2424 y Fr(and)g Fn(H)887 2430 y Fm(2)905 2424 y Fr(,)f(a)h(con)o(tradiction.)f Fe(2)1050 2556 y Fr(4)p eop %%Page: 5 5 5 4 bop 183 194 a Fl(Prop)q(ositi)o(on)13 b(2.3)20 b Fr(The)15 b(TRS)26 b Fo(R)753 200 y Fm(1)785 194 y Fr(is)14 b(terminating.)183 244 y Fl(Pro)q(of:)i Fr(W)m(e)h(will)f(pro)o(v)o(e)h (that)g(ev)o(ery)i(reduction)f(sequence)h(starting)e(from)f(some)g (term)183 293 y Fn(s)21 b Fo(2)g(T)10 b Fr(\()p Fo(F)351 299 y Fm(1)370 293 y Fn(;)d Fo(V)s Fr(\))20 b(m)o(ust)e(b)q(e)i (\014nite.)g(T)m(o)f(this)g(end)h(w)o(e)g(use)h(induction)e(on)g(the)h (structure)183 343 y(of)13 b Fn(s)p Fr(.)i(If)f Fn(s)h Fr(is)f(a)g(constan)o(t)h(or)g(a)f(v)n(ariable,)f(then)i(the)g (assertion)g(is)f(ob)o(viously)f(true.)i(So)f(let)183 393 y Fn(s)e Fo(\021)f Fn(F)6 b Fr(\()p Fn(t)321 399 y Fm(1)340 393 y Fn(;)h(:)g(:)g(:)t(;)g(t)447 399 y Fd(n)470 393 y Fr(\))k(with)f Fn(F)17 b Fo(2)12 b(F)702 399 y Fm(1)731 393 y Fr(and)f(terms)g Fn(t)937 399 y Fd(j)966 393 y Fo(2)g(T)f Fr(\()p Fo(F)1084 399 y Fm(1)1103 393 y Fn(;)d Fo(V)s Fr(\).)k(By)g(induction)g(h)o(yp)q(othesis)183 443 y(ev)o(ery)j(reduction)g(sequence)i(starting)e(from)e Fn(t)916 449 y Fd(j)933 443 y Fn(;)7 b(j)13 b Fo(2)f(f)p Fr(1)p Fn(;)7 b(:)g(:)g(:)t(;)g(n)p Fo(g)p Fr(,)12 b(is)i(\014nite.)f (Supp)q(ose)h(that)183 493 y(there)h(is)f(an)f(in\014nite)h(deriv)n (ation)f Fn(s)f Fo(\021)g Fn(s)818 499 y Fm(1)848 493 y Fo(!)890 499 y Fk(R)919 503 y Fj(1)948 493 y Fn(s)967 499 y Fm(2)998 493 y Fo(!)1040 499 y Fk(R)1069 503 y Fj(1)1098 493 y Fn(s)1117 499 y Fm(3)1147 493 y Fo(!)1189 499 y Fk(R)1218 503 y Fj(1)1247 493 y Fn(:)7 b(:)g(:)183 542 y Fr(It)17 b(is)h(easy)g(to)f(sho)o(w)h(that)f(there)i(m)o(ust)d (exist)i(terms)g Fn(u)1088 548 y Fm(1)1106 542 y Fn(;)7 b(u)1149 548 y Fm(2)1167 542 y Fn(;)g(u)1210 548 y Fm(3)1228 542 y Fn(;)g(v)1267 548 y Fm(1)1285 542 y Fn(;)g(v)1324 548 y Fm(2)1342 542 y Fn(;)g(v)1381 548 y Fm(3)1417 542 y Fr(and)17 b(indices)183 592 y Fn(j;)7 b(k)22 b Fo(2)g Fr(I)-7 b(N)20 b(suc)o(h)h(that)g Fn(s)588 598 y Fd(j)628 592 y Fo(\021)h Fn(E)713 598 y Fm(1)731 592 y Fr(\()p Fn(H)782 598 y Fm(1)801 592 y Fn(;)7 b(H)855 598 y Fm(2)872 592 y Fn(;)g(u)915 598 y Fm(1)933 592 y Fn(;)g(u)976 598 y Fm(2)994 592 y Fn(;)g(u)1037 598 y Fm(3)1055 592 y Fr(\))p Fn(;)g(s)1109 598 y Fd(j)r Fm(+1)1190 592 y Fo(\021)23 b Fn(E)1276 598 y Fm(2)1294 592 y Fr(\()p Fn(u)1334 598 y Fm(1)1353 592 y Fn(;)7 b(u)1396 598 y Fm(1)1413 592 y Fn(;)g(u)1456 598 y Fm(2)1474 592 y Fn(;)g(u)1517 598 y Fm(3)1535 592 y Fn(;)g(u)1578 598 y Fm(3)1596 592 y Fr(\),)183 642 y Fn(s)202 648 y Fd(k)234 642 y Fo(\021)12 b Fn(E)309 648 y Fm(1)327 642 y Fr(\()p Fn(H)378 648 y Fm(1)396 642 y Fn(;)7 b(H)450 648 y Fm(2)468 642 y Fn(;)g(v)507 648 y Fm(1)525 642 y Fn(;)g(v)564 648 y Fm(2)582 642 y Fn(;)g(v)621 648 y Fm(3)640 642 y Fr(\))12 b(and)g Fn(s)766 648 y Fd(j)796 642 y Fo(!)838 648 y Fk(R)867 652 y Fj(1)896 642 y Fn(s)915 648 y Fd(j)r Fm(+1)986 642 y Fo(!)1028 624 y Fm(+)1028 654 y Fk(R)1057 658 y Fj(1)1086 642 y Fn(s)1105 648 y Fd(k)1126 642 y Fr(.)g(This,)f(ho)o(w)o (ev)o(er,)i(con)o(tradicts)183 692 y(Lemma)e(2.2.)h Fe(2)245 780 y Fr(Applying)h(the)i(same)f(tec)o(hnique)h(as)g(in)f([7)o(])g (yields)g(a)h(coun)o(terexample)f(whic)o(h)g(sho)o(ws)183 830 y(that)g(the)g(conjecture)i(is)d(also)h(not)f(true)i(if)e(the)i (TRSs)f(are)g(also)f(irreducible.)183 918 y Fl(Example)i(2.4)21 b Fr(Let)d Fo(F)570 924 y Fm(1)608 918 y Fr(=)h Fo(f)p Fn(F)707 924 y Fm(1)725 918 y Fn(;)7 b(F)771 924 y Fm(2)789 918 y Fn(;)g(G)841 924 y Fm(1)858 918 y Fn(;)g(G)910 924 y Fm(2)928 918 y Fn(;)g(H)982 924 y Fm(1)1000 918 y Fn(;)g(H)1054 924 y Fm(2)1071 918 y Fn(;)g(I)s(;)g(A;)g(E)1211 924 y Fm(1)1228 918 y Fn(;)g(:)g(:)g(:)e(;)i(E)1352 924 y Fm(6)1370 918 y Fo(g)p Fr(,)17 b(and)h(let)h Fo(R)1605 924 y Fm(1)183 968 y Fr(consist)14 b(of)f(the)i(rules)190 1055 y Fn(F)217 1061 y Fm(1)235 1055 y Fr(\()p Fn(A;)7 b(x)p Fr(\))17 b Fo(!)11 b Fn(G)444 1061 y Fm(1)463 1055 y Fr(\()p Fn(x;)c(x)p Fr(\))412 b Fn(F)1001 1061 y Fm(1)1019 1055 y Fr(\()p Fn(x;)7 b(A)p Fr(\))17 b Fo(!)11 b Fn(G)1228 1061 y Fm(2)1247 1055 y Fr(\()p Fn(x;)c(x)p Fr(\))190 1105 y Fn(F)217 1111 y Fm(2)235 1105 y Fr(\()p Fn(A;)g(x)p Fr(\))17 b Fo(!)11 b Fn(G)444 1111 y Fm(1)463 1105 y Fr(\()p Fn(x;)c(x)p Fr(\))412 b Fn(F)1001 1111 y Fm(2)1019 1105 y Fr(\()p Fn(x;)7 b(A)p Fr(\))17 b Fo(!)11 b Fn(G)1228 1111 y Fm(2)1247 1105 y Fr(\()p Fn(x;)c(x)p Fr(\))190 1155 y Fn(G)223 1161 y Fm(1)241 1155 y Fr(\()p Fn(A;)g(x)p Fr(\))k Fo(!)g Fn(H)446 1161 y Fm(1)464 1155 y Fr(\()p Fn(x)p Fr(\))454 b Fn(G)1007 1161 y Fm(1)1025 1155 y Fr(\()p Fn(x;)7 b(A)p Fr(\))k Fo(!)g Fn(H)1230 1161 y Fm(2)1249 1155 y Fr(\()p Fn(x)p Fr(\))190 1205 y Fn(G)223 1211 y Fm(2)241 1205 y Fr(\()p Fn(A;)c(x)p Fr(\))k Fo(!)g Fn(H)446 1211 y Fm(1)464 1205 y Fr(\()p Fn(x)p Fr(\))454 b Fn(G)1007 1211 y Fm(2)1025 1205 y Fr(\()p Fn(x;)7 b(A)p Fr(\))k Fo(!)g Fn(H)1230 1211 y Fm(2)1249 1205 y Fr(\()p Fn(x)p Fr(\))190 1254 y Fn(H)225 1260 y Fm(1)243 1254 y Fr(\()p Fn(A)p Fr(\))52 b Fo(!)11 b Fn(I)545 b(H)1009 1260 y Fm(2)1027 1254 y Fr(\()p Fn(A)p Fr(\))52 b Fo(!)11 b Fn(I)188 1328 y(E)219 1334 y Fm(1)238 1328 y Fr(\()p Fn(H)289 1334 y Fm(1)307 1328 y Fr(\()p Fn(w)q Fr(\))p Fn(;)c(H)424 1334 y Fm(2)442 1328 y Fr(\()p Fn(w)q Fr(\))p Fn(;)g(x;)g(y)q(;)g(z)r(;)g(w)q Fr(\))227 b Fo(!)11 b Fn(E)1005 1334 y Fm(2)1023 1328 y Fr(\()p Fn(x;)c(x;)g(y)q(;)g(z)r(;)g (z)r(;)g(w)q Fr(\))188 1378 y Fn(E)219 1384 y Fm(1)238 1378 y Fr(\()p Fn(x)278 1384 y Fm(1)296 1378 y Fn(;)g(x)339 1384 y Fm(1)357 1378 y Fn(;)g(x;)g(y)q(;)g(z)r(;)g(A)p Fr(\))375 b Fo(!)11 b Fn(E)1005 1384 y Fm(5)1023 1378 y Fr(\()p Fn(x)1063 1384 y Fm(1)1082 1378 y Fn(;)c(x;)g(y)q(;)g(z)r Fr(\))188 1428 y Fn(E)219 1434 y Fm(2)238 1428 y Fr(\()p Fn(F)281 1434 y Fm(1)299 1428 y Fr(\()p Fn(w)q(;)g(w)q Fr(\))p Fn(;)g(x;)g(y)q(;)g(z)r(;)g(F)581 1434 y Fm(2)597 1428 y Fr(\()p Fn(w)q(;)g(w)q Fr(\))p Fn(;)g(w)q Fr(\))145 b Fo(!)11 b Fn(E)1005 1434 y Fm(3)1023 1428 y Fr(\()p Fn(x;)c(y)q(;)g(x;)g(y)q(;)g(y)q(;)g(z)r(;)g(y)q(;)g(z)r(;)g(x;)g(y)q (;)g(z)r(;)g(w)q Fr(\))188 1478 y Fn(E)219 1484 y Fm(2)238 1478 y Fr(\()p Fn(x;)g(x;)g(y)q(;)g(z)r(;)g(z)r(;)g(A)p Fr(\))414 b Fo(!)11 b Fn(E)1005 1484 y Fm(6)1023 1478 y Fr(\()p Fn(x;)c(y)q(;)g(z)r Fr(\))188 1527 y Fn(E)219 1533 y Fm(2)238 1527 y Fr(\()p Fn(I)s(;)g(x;)g(y)q(;)g(z)r(;)g(I)s(;)g (A)p Fr(\))417 b Fo(!)11 b Fn(E)1005 1533 y Fm(6)1023 1527 y Fr(\()p Fn(x;)c(y)q(;)g(z)r Fr(\))188 1577 y Fn(E)219 1583 y Fm(3)238 1577 y Fr(\()p Fn(x)278 1583 y Fm(1)296 1577 y Fn(;)g(x)339 1583 y Fm(1)357 1577 y Fn(;)g(x)400 1583 y Fm(2)418 1577 y Fn(;)g(x)461 1583 y Fm(2)479 1577 y Fn(;)g(x)522 1583 y Fm(3)539 1577 y Fn(;)g(x)582 1583 y Fm(3)600 1577 y Fn(;)g(x)643 1583 y Fm(4)661 1577 y Fn(;)g(x)704 1583 y Fm(4)722 1577 y Fn(;)g(x;)g(y)q(;)g(z)r(;)g(w)q Fr(\))j Fo(!)h Fn(E)1005 1583 y Fm(4)1023 1577 y Fr(\()p Fn(x)1063 1583 y Fm(1)1082 1577 y Fn(;)c(x)1125 1583 y Fm(1)1143 1577 y Fn(;)g(x)1186 1583 y Fm(2)1203 1577 y Fn(;)g(x)1246 1583 y Fm(2)1264 1577 y Fn(;)g(x)1307 1583 y Fm(3)1325 1577 y Fn(;)g(x)1368 1583 y Fm(3)1386 1577 y Fn(;)g(x)1429 1583 y Fm(4)1447 1577 y Fn(;)g(x)1490 1583 y Fm(4)1507 1577 y Fn(;)g(x;)g(y)q(;)g(z)r(;)g(w)q Fr(\))188 1627 y Fn(E)219 1633 y Fm(3)238 1627 y Fr(\()p Fn(x;)g(y)q(;)g(x;)g(y)q(;)g(y)q(;)g(z)r(;)g(y)q(;)g(z)r(;)g(x;)g(y)q (;)g(z)r(;)g(A)p Fr(\))171 b Fo(!)11 b Fn(E)1005 1633 y Fm(6)1023 1627 y Fr(\()p Fn(x;)c(y)q(;)g(z)r Fr(\))188 1677 y Fn(E)219 1683 y Fm(4)238 1677 y Fr(\()p Fn(G)287 1683 y Fm(1)305 1677 y Fr(\()p Fn(w)q(;)g(w)q Fr(\))p Fn(;)g(x)461 1683 y Fm(1)478 1677 y Fn(;)g(G)530 1683 y Fm(2)548 1677 y Fr(\()p Fn(w)q(;)g(w)q Fr(\))p Fn(;)g(x)704 1683 y Fm(1)721 1677 y Fn(;)246 1727 y(G)279 1733 y Fm(1)297 1727 y Fr(\()p Fn(w)q(;)g(w)q Fr(\))p Fn(;)g(x)453 1733 y Fm(1)471 1727 y Fn(;)g(G)523 1733 y Fm(2)540 1727 y Fr(\()p Fn(w)q(;)g(w)q Fr(\))p Fn(;)g(x)696 1733 y Fm(1)713 1727 y Fn(;)g(x;)g(y)q(;)g(z)r(;)g(w)q Fr(\))19 b Fo(!)11 b Fn(E)1005 1733 y Fm(1)1023 1727 y Fr(\()p Fn(x)1063 1733 y Fm(1)1082 1727 y Fn(;)c(x)1125 1733 y Fm(1)1143 1727 y Fn(;)g(x;)g(y)q(;)g(z)r(;)g(w)q Fr(\))188 1776 y Fn(E)219 1782 y Fm(4)238 1776 y Fr(\()p Fn(I)s(;)g(x)318 1782 y Fm(1)336 1776 y Fn(;)g(I)s(;)g(x)419 1782 y Fm(1)437 1776 y Fn(;)g(I)s(;)g(x)520 1782 y Fm(1)538 1776 y Fn(;)g(I)s(;)g(x)621 1782 y Fm(1)638 1776 y Fn(;)g(x;)g(y)q(;)g(z)r(;)g(A)p Fr(\))94 b Fo(!)11 b Fn(E)1005 1782 y Fm(5)1023 1776 y Fr(\()p Fn(x)1063 1782 y Fm(1)1082 1776 y Fn(;)c(x;)g(y)q(;)g(z)r Fr(\))188 1826 y Fn(E)219 1832 y Fm(4)238 1826 y Fr(\()p Fn(x;)g(x;)g(x;)g(x;)g(x)o(;)g(x)o(;)g(x;)f(x;)g(x;)g(x;)h(x)o(;)g(A)p Fr(\))153 b Fo(!)11 b Fn(E)1005 1832 y Fm(6)1023 1826 y Fr(\()p Fn(x;)c(x;)g(x)p Fr(\))188 1876 y Fn(E)219 1882 y Fm(5)238 1876 y Fr(\()p Fn(I)s(;)g(x;)g(y)q(;)g(z)r Fr(\))507 b Fo(!)11 b Fn(E)1005 1882 y Fm(6)1023 1876 y Fr(\()p Fn(x;)c(y)q(;)g(z)r Fr(\))183 1947 y(F)m(urthermore,)13 b(let)h Fo(F)525 1953 y Fm(2)555 1947 y Fr(=)e Fo(f)p Fn(f)r(;)7 b(g)681 1953 y Fm(1)699 1947 y Fn(;)g(g)738 1953 y Fm(2)756 1947 y Fn(;)g(h;)g(a)p Fo(g)12 b Fr(as)i(w)o(ell)f(as) 546 2235 y Fo(R)581 2241 y Fm(2)612 2235 y Fr(=)656 2000 y Fi(8)656 2037 y(>)656 2050 y(>)656 2062 y(>)656 2075 y(>)656 2087 y(>)656 2100 y(>)656 2112 y(>)656 2125 y(>)656 2137 y(>)656 2149 y(>)656 2162 y(>)656 2174 y(>)656 2187 y(<)656 2262 y(>)656 2274 y(>)656 2286 y(>)656 2299 y(>)656 2311 y(>)656 2324 y(>)656 2336 y(>)656 2349 y(>)656 2361 y(>)656 2374 y(>)656 2386 y(>)656 2398 y(>)656 2411 y(:)698 2035 y Fn(f)t Fr(\()p Fn(x;)7 b(y)q(;)g(w)q(;)g(w)q(;)g(a)p Fr(\))k Fo(!)g Fn(g)1043 2041 y Fm(1)1061 2035 y Fr(\()p Fn(x;)c(x;)g(y)q(;)g(w)q Fr(\))698 2085 y Fn(f)t Fr(\()p Fn(x;)g(y)q(;)g(w)q(;)g(a;)g(a)p Fr(\))k Fo(!)g Fn(g)1034 2091 y Fm(1)1052 2085 y Fr(\()p Fn(y)q(;)c(x;)g(x;)g(w)q Fr(\))698 2134 y Fn(f)t Fr(\()p Fn(x;)g(y)q(;)g(a;)g(a;)g(w)q Fr(\))k Fo(!)g Fn(g)1034 2140 y Fm(2)1052 2134 y Fr(\()p Fn(x;)c(y)q(;)g(y)q(;)g(w)q Fr(\))698 2184 y Fn(f)t Fr(\()p Fn(x;)g(y)q(;)g(a;)g(w)q(;)g(w)q Fr(\))k Fo(!)g Fn(g)1043 2190 y Fm(2)1061 2184 y Fr(\()p Fn(y)q(;)c(y)q(;)g(x;)g(w)q Fr(\))698 2234 y Fn(g)718 2240 y Fm(1)737 2234 y Fr(\()p Fn(x;)g(x;)g(y)q(;)g(a)p Fr(\))j Fo(!)h Fn(h)p Fr(\()p Fn(x;)c(y)q Fr(\))698 2284 y Fn(g)718 2290 y Fm(1)737 2284 y Fr(\()p Fn(y)q(;)g(x;)g(x;)g(a)p Fr(\))j Fo(!)h Fn(h)p Fr(\()p Fn(x;)c(y)q Fr(\))698 2334 y Fn(g)718 2340 y Fm(2)737 2334 y Fr(\()p Fn(x;)g(y)q(;)g(y)q(;)g(a)p Fr(\))k Fo(!)g Fn(h)p Fr(\()p Fn(x;)c(y)q Fr(\))698 2384 y Fn(g)718 2390 y Fm(2)737 2384 y Fr(\()p Fn(y)q(;)g(y)q(;)g(x;)g(a)p Fr(\))k Fo(!)g Fn(h)p Fr(\()p Fn(x;)c(y)q Fr(\))698 2433 y Fn(h)p Fr(\()p Fn(x;)g(x)p Fr(\))k Fo(!)g Fn(x)893 2556 y Fr(5)p eop %%Page: 6 6 6 5 bop 340 194 a Fr(It)17 b(is)f(easy)g(to)g(see)h(that)f Fo(R)774 200 y Fm(1)809 194 y Fr(and)g Fo(R)927 200 y Fm(2)962 194 y Fr(are)h(v)n(ariable-preserving)f(and)f(irreducible.)i (Con-)340 244 y(v)o(ergence)k(of)e(the)g(TRSs)g(can)h(b)q(e)f(pro)o(v)o (ed)h(as)f(in)f(Example)g(2.1.)g(Again)g(their)h(disjoin)o(t)340 293 y(union)i(is)f(not)h(terminating,)e(since)i(there)h(is)f(a)g (cyclic)g(reduction)g(sequence)i(starting)340 343 y(from)13 b(the)h(term)g Fn(E)641 349 y Fm(1)659 343 y Fr(\()p Fn(H)710 349 y Fm(1)728 343 y Fn(;)7 b(H)782 349 y Fm(2)800 343 y Fn(;)g(t)834 349 y Fm(1)852 343 y Fn(;)g(t)886 349 y Fm(2)904 343 y Fn(;)g(t)938 349 y Fm(3)956 343 y Fn(;)g(A)p Fr(\),)13 b(where)i Fn(t)1182 349 y Fm(1)1212 343 y Fo(\021)d Fn(f)t Fr(\()p Fn(F)1323 349 y Fm(1)1343 343 y Fr(\()p Fn(A;)7 b(A)p Fr(\))p Fn(;)g(F)1502 349 y Fm(1)1519 343 y Fr(\()p Fn(A;)g(A)p Fr(\))p Fn(;)g(a;)g(a;)g(a)p Fr(\),)340 393 y Fn(t)355 399 y Fm(2)386 393 y Fo(\021)k Fn(f)t Fr(\()p Fn(F)496 399 y Fm(1)516 393 y Fr(\()p Fn(A;)c(A)p Fr(\))p Fn(;)g(F)675 399 y Fm(2)692 393 y Fr(\()p Fn(A;)g(A)p Fr(\))p Fn(;)g(a;)g(a;)g(a)p Fr(\),)12 b(and)i Fn(t)1064 399 y Fm(3)1094 393 y Fo(\021)e Fn(f)t Fr(\()p Fn(F)1205 399 y Fm(2)1224 393 y Fr(\()p Fn(A;)7 b(A)p Fr(\))p Fn(;)g(F)1383 399 y Fm(2)1401 393 y Fr(\()p Fn(A;)g(A)p Fr(\))p Fn(;)g(a;)g(a;)g(a)p Fr(\).)340 484 y Fl(Ac)o(kno)o(wledgemen)o(ts:)13 b Fr(The)j(author)f(is)h(grateful)f (to)h(Rob)q(ert)g(Giegeric)o(h)f(for)h(v)n(aluable)340 534 y(commen)o(ts)11 b(on)i(previous)g(v)o(ersions)g(of)f(the)h(pap)q (er)g(and)g(to)f(Ank)o(e)h(Bo)q(dzin)g(for)f(t)o(yp)q(esetting)340 584 y(the)j(man)o(uscript.)340 718 y Fp(References)340 814 y Fq(1.)21 b(N.)12 b(Dersho)o(witz)k(and)g(J.P)m(.)e(Jouannaud.)24 b(Rewrite)16 b(Systems.)24 b(In)15 b(L.)d(v)n(an)j(Leeu)o(w)o(en,)g (editor,)391 860 y Fc(Handb)n(o)n(ok)9 b(of)i(The)n(or)n(etic)n(al)e (Computer)i(Scienc)n(e,)e(V)m(ol.)h(B)p Fq(,)h(c)o(hapter)i(6.)d (North-Holland,)j(1990.)340 905 y(2.)21 b(K.)12 b(Drosten.)k Fc(T)m(ermersetzungssyste)o(me)p Fq(.)c(Informatik-F)m(ac)o(h)o(b)q (eric)o(h)o(te)g Fb(210)p Fq(,)c(Springer)j(V)m(erlag,)391 951 y(1989.)340 997 y(3.)21 b(B.)12 b(Gramlic)o(h.)18 b(Generalized)13 b(Su\016cien)o(t)f(Conditions)h(for)e(Mo)q(dular)h(T)m (ermination)g(of)f(Rewrit-)391 1042 y(ing.)27 b Fc(Applic)n(able)13 b(A)o(lgebr)n(a)i(in)h(Engine)n(ering,)d(Communic)n(ation)h(and)i (Computing)f Fb(5)p Fq(,)g(pages)391 1088 y(131{158,)f(1994.)340 1133 y(4.)21 b(J.W.)29 b(Klop.)66 b(T)m(erm)29 b(Rewriting)i(Systems.) 67 b(In)29 b(S.)12 b(Abramsky)m(,)30 b(D.)12 b(Gabba)o(y)m(,)30 b(and)391 1179 y(T.)12 b(Maibaum,)19 b(editors,)g Fc(Handb)n(o)n(ok)c (of)i(L)n(o)n(gic)g(in)g(Computer)g(Scienc)n(e,)f(V)m(ol.)h(II)p Fq(,)f(pages)j(1{)391 1225 y(116.)13 b(Oxford)g(Univ)o(ersit)o(y)i (Press,)e(1992.)340 1270 y(5.)21 b(A.)12 b(Middeldorp.)23 b Fc(Mo)n(dular)13 b(Pr)n(op)n(erties)g(of)h(T)m(erm)h(R)n(ewriting)e (Systems)p Fq(.)18 b(PhD)d(thesis,)f(V)m(rije)391 1316 y(Univ)o(ersiteit)h(te)e(Amsterdam,)g(1990.)340 1362 y(6.)21 b(E.)12 b(Ohlebusc)o(h.)19 b(On)13 b(the)h(Mo)q(dularit)o(y)h (of)e(T)m(ermination)i(of)e(T)m(erm)f(Rewriting)j(Systems.)j(Re-)391 1407 y(p)q(ort)d(Nr.)f(11,)h(Univ)o(ersit\177)-19 b(at)17 b(Bielefeld,)f(1993.)23 b(Revised)17 b(v)o(ersion)f(to)f(app)q(ear)h (in)f(Theoretical)391 1453 y(Computer)e(Science.)340 1499 y(7.)21 b(Y.)12 b(T)m(o)o(y)o(ama.)k(Coun)o(terexamples)c(to)e(T)m (ermination)i(for)e(the)g(Direct)h(Sum)f(of)g(T)m(erm)f(Rewriting)391 1544 y(Systems.)18 b Fc(Information)11 b(Pr)n(o)n(c)n(essing)g(L)n (etters)i Fb(25)p Fq(,)f(pages)i(141{143,)g(1987.)340 1590 y(8.)21 b(Y.)12 b(T)m(o)o(y)o(ama.)17 b(On)12 b(the)g(Ch)o(urc)o (h-Rosser)h(Prop)q(ert)o(y)g(for)f(the)g(Direct)h(Sum)f(of)g(T)m(erm)f (Rewriting)391 1636 y(Systems.)18 b Fc(Journal)12 b(of)h(the)g(A)o(CM)h Fb(34)p Fc(\(1\))p Fq(,)d(pages)j(128{143,)g(1987.)340 1681 y(9.)21 b(Y.)12 b(T)m(o)o(y)o(ama,)k(J.W.)f(Klop,)h(and)h(H.P)e (Barendregt.)27 b(T)m(ermination)18 b(for)d(the)h(Direct)h(Sum)f(of)391 1727 y(Left-Linear)e(T)m(erm)f(Rewriting)i(Systems.)j(In)13 b Fc(Pr)n(o)n(c)n(e)n(e)n(dings)e(of)j(the)f(3r)n(d)g(Internationa)o(l) e(Con-)391 1773 y(fer)n(enc)n(e)g(on)h(R)n(ewriting)f(T)m(e)n(chniques) f(and)i(Applic)n(atio)o(ns)p Fq(,)c(pages)13 b(477{491.)f(Lecture)h (Notes)e(in)391 1818 y(Computer)i(Science)i Fb(355)p Fq(,)e(Springer)h(V)m(erlag,)g(1989.)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)985 2420 y Fq(T)1007 2432 y(E)1028 2420 y(X)g(macro)g(pac)o(k)n(age)h(with) f(LLNCS)g(st)o(yle)1050 2556 y Fr(6)p eop %%Trailer end userdict /end-hook known{end-hook}if %%EOF