%!PS-Adobe-2.0 %%Creator: dvipsk 5.58f Copyright 1986, 1994 Radical Eye Software %%Title: caap.dvi %%Pages: 12 %%PageOrder: Ascend %%BoundingBox: 0 0 596 842 %%DocumentPaperSizes: a4 %%EndComments %DVIPSCommandLine: dvips -o caap.ps caap.dvi %DVIPSParameters: dpi=300, compressed, comments removed %DVIPSSource: TeX output 1997.01.24:1504 %%BeginProcSet: texc.pro /TeXDict 250 dict def TeXDict begin /N{def}def /B{bind def}N /S{exch}N /X{S N}B /TR{translate}N /isls false N /vsize 11 72 mul N /hsize 8.5 72 mul N /landplus90{false}def /@rigin{isls{[0 landplus90{1 -1}{-1 1} ifelse 0 0 0]concat}if 72 Resolution div 72 VResolution div neg scale isls{landplus90{VResolution 72 div vsize mul 0 exch}{Resolution -72 div hsize mul 0}ifelse TR}if Resolution VResolution vsize -72 div 1 add mul TR[matrix currentmatrix{dup dup round sub abs 0.00001 lt{round}if} forall round exch round exch]setmatrix}N /@landscape{/isls true N}B /@manualfeed{statusdict /manualfeed true put}B /@copies{/#copies X}B /FMat[1 0 0 -1 0 0]N /FBB[0 0 0 0]N /nn 0 N /IE 0 N /ctr 0 N /df-tail{ /nn 8 dict N nn begin /FontType 3 N /FontMatrix fntrx N /FontBBox FBB N string /base X array /BitMaps X /BuildChar{CharBuilder}N /Encoding IE N end dup{/foo setfont}2 array copy cvx N load 0 nn put /ctr 0 N[}B /df{ /sf 1 N /fntrx FMat N df-tail}B /dfs{div /sf X /fntrx[sf 0 0 sf neg 0 0] N df-tail}B /E{pop nn dup definefont setfont}B /ch-width{ch-data dup length 5 sub get}B /ch-height{ch-data dup length 4 sub get}B /ch-xoff{ 128 ch-data dup length 3 sub get sub}B /ch-yoff{ch-data dup length 2 sub get 127 sub}B /ch-dx{ch-data dup length 1 sub get}B /ch-image{ch-data dup type /stringtype ne{ctr get /ctr ctr 1 add N}if}B /id 0 N /rw 0 N /rc 0 N /gp 0 N /cp 0 N /G 0 N /sf 0 N /CharBuilder{save 3 1 roll S dup /base get 2 index get S /BitMaps get S get /ch-data X pop /ctr 0 N ch-dx 0 ch-xoff ch-yoff ch-height sub ch-xoff ch-width add ch-yoff setcachedevice ch-width ch-height true[1 0 0 -1 -.1 ch-xoff sub ch-yoff .1 sub]/id ch-image N /rw ch-width 7 add 8 idiv string N /rc 0 N /gp 0 N /cp 0 N{rc 0 ne{rc 1 sub /rc X rw}{G}ifelse}imagemask restore}B /G{{id gp get /gp gp 1 add N dup 18 mod S 18 idiv pl S get exec}loop}B /adv{cp add /cp X}B /chg{rw cp id gp 4 index getinterval putinterval dup gp add /gp X adv}B /nd{/cp 0 N rw exit}B /lsh{rw cp 2 copy get dup 0 eq{pop 1}{ dup 255 eq{pop 254}{dup dup add 255 and S 1 and or}ifelse}ifelse put 1 adv}B /rsh{rw cp 2 copy get dup 0 eq{pop 128}{dup 255 eq{pop 127}{dup 2 idiv S 128 and or}ifelse}ifelse put 1 adv}B /clr{rw cp 2 index string putinterval adv}B /set{rw cp fillstr 0 4 index getinterval putinterval adv}B /fillstr 18 string 0 1 17{2 copy 255 put pop}for N /pl[{adv 1 chg} {adv 1 chg nd}{1 add chg}{1 add chg nd}{adv lsh}{adv lsh nd}{adv rsh}{ adv rsh nd}{1 add adv}{/rc X nd}{1 add set}{1 add clr}{adv 2 chg}{adv 2 chg nd}{pop nd}]dup{bind pop}forall N /D{/cc X dup type /stringtype ne{] }if nn /base get cc ctr put nn /BitMaps get S ctr S sf 1 ne{dup dup length 1 sub dup 2 index S get sf div put}if put /ctr ctr 1 add N}B /I{ cc 1 add D}B /bop{userdict /bop-hook known{bop-hook}if /SI save N @rigin 0 0 moveto /V matrix currentmatrix dup 1 get dup mul exch 0 get dup mul add .99 lt{/QV}{/RV}ifelse load def pop pop}N /eop{SI restore userdict /eop-hook known{eop-hook}if showpage}N /@start{userdict /start-hook known{start-hook}if pop /VResolution X /Resolution X 1000 div /DVImag X /IE 256 array N 0 1 255{IE S 1 string dup 0 3 index put cvn put}for 65781.76 div /vsize X 65781.76 div /hsize X}N /p{show}N /RMat[1 0 0 -1 0 0]N /BDot 260 string N /rulex 0 N /ruley 0 N /v{/ruley X /rulex X V}B /V {}B /RV statusdict begin /product where{pop 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 newpath transform round exch round exch itransform moveto rulex 0 rlineto 0 ruley neg rlineto rulex neg 0 rlineto fill grestore}B /a{moveto}B /delta 0 N /tail {dup /delta X 0 rmoveto}B /M{S p delta add tail}B /b{S p tail}B /c{-4 M} B /d{-3 M}B /e{-2 M}B /f{-1 M}B /g{0 M}B /h{1 M}B /i{2 M}B /j{3 M}B /k{ 4 M}B /w{0 rmoveto}B /l{p -4 w}B /m{p -3 w}B /n{p -2 w}B /o{p -1 w}B /q{ p 1 w}B /r{p 2 w}B /s{p 3 w}B /t{p 4 w}B /x{0 S rmoveto}B /y{3 2 roll p a}B /bos{/SS save N}B /eos{SS restore}B end %%EndProcSet TeXDict begin 39158280 55380996 1000 300 300 (caap.dvi) @start /Fa 3 53 df<123EEA4180EA80C012C01200A2EA0180EA03001204EA08401230 EA7F8012FF0A0D7E8C0E>50 D<123E1241EA61801201EA0300121EEA0180EA00C0A212C0 A2EA4180EA3E000A0D7E8C0E>I<12035AA2120B12131223126312C3EAFFC0EA0300A3EA 0FC00A0D7E8C0E>I E /Fb 1 49 df<1218A31230A31260A312C0A2050B7E8B09>48 D E /Fc 1 106 df<1208A21200A41270129812B01230A21260126412681270060F7D8E 0B>105 D E /Fd 25 117 df12 D<127812FCA4127806067D85 0D>46 D48 D<1360EA01E0120F12FF12F312 03B3A2387FFF80A2111B7D9A18>III I<38380180383FFF005B5B5B13C00030C7FCA4EA31F8EA361E38380F80EA3007000013C0 14E0A3127812F8A214C012F038600F8038381F00EA1FFEEA07F0131B7E9A18>I<137EEA 03FF38078180380F03C0EA1E07123C387C03800078C7FCA212F813F8EAFB0E38FA0780EA FC0314C000F813E0A41278A214C0123CEB0780381E0F00EA07FEEA03F8131B7E9A18>I< 1260387FFFE0A214C01480A238E00300EAC0065B5BC65AA25B13E0A212015B1203A41207 A66C5A131C7D9B18>III68 D80 D<007FB512E0A238781F81007013800060146000E0 147000C01430A400001400B03807FFFEA21C1C7E9B21>84 D101 D104 D<121E123FA4121EC7FCA6127FA2121FAEEAFFC0A20A1E7F9D0E>I<39FF0FC0 7E903831E18F3A1F40F20780D980FC13C0A2EB00F8AB3AFFE7FF3FF8A225127F9128> 109 D<38FF0FC0EB31E0381F40F0EB80F8A21300AB38FFE7FFA218127F911B>II<38FF3F80EBE1E0381F80F0EB0078147C143C143EA614 3C147C1478EB80F0EBC1E0EB3F0090C7FCA6EAFFE0A2171A7F911B>I114 DI<1203A45AA25AA2EA3FFC12FFEA1F00A9130CA4EA0F08EA0798EA03F00E1A7F 9913>I E /Fe 4 28 df<13181360EA01C0EA0380EA0700B1120E5A123012C01230121C 7E7EB1EA0380EA01C0EA006013180D317B8118>8 D<12C01230121C7E7EB1EA0380EA01 C0EA006013181360EA01C0EA0380EA0700B1120E5A123012C00D317B8118>I<1470EB01 F0EB03C0EB0780EB0E005B5B5BA213F05BB3AC485AA3485A48C7FC1206120E12385A12C0 12707E120E120612076C7E6C7EA36C7EB3AC7F1370A27F7F7FEB0780EB03C0EB01F0EB00 7014637B811F>26 D<12E07E127C121E7E7E6C7E6C7EA26C7EB3AD1370A27FA27F7F7FEB 03C0EB00F0147014E0EB03C0EB0700130E5B5BA25BA25BB3AD485AA2485A48C7FC5A121E 127C12F05A14637B811F>I E /Ff 8 116 df<00F013F0ADB5FCA2EAF000AE141D7C9C1D >72 D<12F0B3A9B5FCA2101D7D9C16>76 D82 DI99 D110 DI115 D E /Fg 2 110 df<123C120C5AA45AEA3380EA3C60EA3020EA6030A4EAC060A2EA40C0 EA6080EA2300121E0C147D9310>98 D<3830F87838590D8C384E0E0C129CEA980C1218A2 38301818141914311432EA6030141C180D7D8C1C>109 D E /Fh 1 79 df<39FFE00FF839101003203908080140390C0400C0EA0E02A2EA0D01380C8080EB 4040EB2020A2EB1010EB0808EB0404EB020213011401EB0080EC404014201410A2140814 04140200121301123339FFC000C0C812401D1D809B20>78 D E /Fi 12 107 df0 D<1204A3EAC460EAF5E0EA3F80EA0E00EA3F80EA F5E0EAC460EA0400A30B0D7E8D11>3 D<14101418A280A28080B612E0A2C7EA03001406 5CA25CA214101B107E8E21>33 D<1204120EA2121CA31238A212301270A21260A212C0A2 070F7F8F0A>48 D<13201360EA0FE0EA10C0EA20E0EA60F0EA4190EAC198A2EAC318A312 C6A312CCA2EA4C10EA7830EA382013E0EA3F80EA3000A20D187F9511>59 D<137EEA01FFEA020FEA0406EA0C04EA1C00121E121FEA0FE0EA07C0EA0C00121012305A A2EAE004EAF018EAF820EA7FC0EA3F0010147F9312>69 DI<133FEBFFC0380307E0EA0401380800F05A003013705AA212E01460A26C13 C01480EA7C31387FE300EA1F06EA00081370383FC010007F1320380FF8403801FF803800 3F0014187D931B>81 D<3803FFF0000F7F3830E07C3860C03C00C0131C0081131812015C 1420EB80C0018FC7FCEA039E130F80EA0707380603C0ECE080390C01F100EB00FE481378 19147F931D>II<000F13 0C003F1318124700061330A2000E1370000C136014E05A1301383003C01302EA6005EB09 80EAE01113231343EAF18338FE03E0007813801614819315>85 D<12C0B3AB021D7D950A >106 D E /Fj 39 123 df45 D<127012F8A312700505798414> I<1306130EA2131CA21338A21370A213E0A2EA01C0A2EA0380A3EA0700A2120EA25AA25A A25AA25AA25A0F1D7E9914>II<1203A25A5A123F12F7124712 07AEEA7FF0A20C177C9614>I 51 D54 D<12E0EAFFFEA2EAE01C1338EA0030137013E013C0120113801203A2EA0700A4120EA612 040F187E9714>I57 D<127012F8A312701200A6127012F8A312700510798F14>I64 D<3801F180EA07FFEA0E1FEA1C071238EA7003A348C7FCA73870 0380A338380700121CEA0E0EEA07FCEA01F011177F9614>67 D75 D82 DI<38FE0FE0A238380380B0381C0700A2EA0E0EEA07FCEA01F01317809614>85 D97 D<12FCA2121CA513F8EA1DFEEA1F07EA1E03001C1380EB01C0 A6EB0380001E1300EA1F0EEA1DFCEA0CF81217809614>II<137EA2130E A5EA07CEEA0FFEEA1C3EEA301EEA700E12E0A61270EA301EEA383E381FEFC0EA07CF1217 7F9614>II<13FCEA01FEEA038EEA07041300A3EA7FFE12 FFEA0700ACEAFFF8A20F177F9614>II<12FCA2121CA51378EA1DFEEA1F86EA1E07121CAA38FF 8FE0A21317809614>I<1206120FA21206C7FCA4B4FCA21207ACEAFFF8A20D187C9714>I< 136013F0A213601300A4EA1FF0A2EA0070B2EA40E0EAE0C0EA7F80EA3F000C207E9714> I<12FCA2121CA5EBFF80A2EB1C005B5B5BEA1DC0EA1FE0A2EA1E70EA1C38133C131C7F38 FF1F80A21117809614>IIIIII114 DI<1206120EA4EA7FFC12FFEA0E00A8130EA3131CEA07F8EA01F00F157F9414>II<38FE3F80A2383C1E00EA1C1CA36C 5AA3EA0630EA0770A36C5AA311107F8F14>I<38FE3F80A238700700EA380EA3EA39CEA3 EA1B6C121AA3EA1E7CA2EA0E3811107F8F14>I122 D E /Fk 1 64 df<5AA5EAE10EEA3FF8EA07C0EA0380EA06C0EA0440EA0820EA1830EA10 100F0E7F8C10>63 D E /Fl 38 122 df<12181238127812381208A21210A212201240A2 1280050C7D830D>44 DI<1230127812F0126005047C830D>I<13 04130C131813381378EA07B8EA0070A413E0A4EA01C0A4EA0380A4EA0700A45AEAFFF00E 1C7B9B15>49 D<133EEB4180EB80C0EA0100000213E0EA0440A21208A3381081C0A23811 0380000E1300EA00065B5B136013800003C7FC12044813404813805AEB0100EA7F07EA43 FEEA81FCEA8078131D7D9B15>I<131FEB60C013803801006012021340000413E0A3EB81 C0EA030138000380EB070013FC131C1306A21307A41270EAE00E12805BEA40185BEA20E0 EA1F80131D7D9B15>III<903803F02090381E0C6090383002E09038E003C03801C001EA038048C7 FC000E1480121E121C123C15005AA35AA41404A35C12705C6C5B00185B6C485AD80706C7 FCEA01F81B1E7A9C1E>67 D73 D<3801FFC038003C001338A45BA45BA4485AA43803 8002A31404EA0700140C14181438000E13F0B5FC171C7E9B1A>76 D<3801FFFE39003C038090383801C0EC00E0A3EB7001A315C0EBE0031580EC0700141C38 01FFF001C0C7FCA3485AA448C8FCA45AEAFFE01B1C7E9B1C>80 D<3801FFFE39003C0780 90383801C015E01400A2EB7001A3EC03C001E01380EC0700141CEBFFE03801C03080141C A2EA0380A43807003C1520A348144039FFE01E80C7EA0F001B1D7E9B1E>82 DI<001FB512C0381C070138300E0000201480126012405B1280A2000014005B A45BA45BA4485AA41203EA7FFE1A1C799B1E>I97 D<123F1207A2120EA45A A4EA39E0EA3A18EA3C0C12381270130EA3EAE01CA31318133813301360EA60C0EA3180EA 1E000F1D7C9C13>I<13F8EA0304120EEA1C0EEA181CEA30001270A25AA51304EA600813 10EA3060EA0F800F127C9113>II<13F8 EA0704120CEA1802EA38041230EA7008EA7FF0EAE000A5EA60041308EA30101360EA0F80 0F127C9113>III II108 D<391C1E078039266318C0394683A0E0384703C0008E1380A2120EA239 1C0701C0A3EC0380D8380E1388A2EC0708151039701C032039300C01C01D127C9122>I< EA383EEA4CC3384D0380124E129E129C121CA238380700A3130E00701340A2131C1480EA E00C3860070012127C9117>I<13F8EA030CEA0E06487E1218123000701380A238E00700 A3130EA25BEA60185BEA30E0EA0F8011127C9115>I<380387803804C860EBD03013E0EA 09C014381201A238038070A31460380700E014C0EB0180EB8300EA0E86137890C7FCA25A A45AB4FC151A809115>IIII<12035AA3120EA4EAFFE0EA1C00A35AA45AA4EAE080A2EAE100A21266 12380B1A7C990E>I<381C0180EA2E03124EA2388E0700A2121CA2EA380EA438301C80A3 EA383C38184D00EA0F8611127C9116>II<381E018338270387124714 8338870701A2120EA2381C0E02A31404EA180C131C1408EA1C1E380C26303807C3C01812 7C911C>I<38038780380CC840380870E012103820E0C014001200A2485AA4EA03811263 EAE38212C5EA8584EA787813127E9113>I<381C0180EA2E03124EA2388E0700A2121CA2 EA380EA4EA301CA3EA383CEA1878EA0FB8EA003813301370EAE0605BEA81800043C7FC12 3C111A7C9114>I E /Fm 53 123 df<48B512E038003C00013813601540A35BA315005B A4485AA4485AA448C8FCA45AEAFFF01B1C7E9B1A>0 D<13F8EA030C380E0604EA1C0738 3803080030138800701390A200E013A0A214C01480A3EA6007EB0B8838307190380F80E0 16127E911B>11 DI<38078010EA1FC0383FE020EA7FF03860 3040EAC0183880088012001304EB0500A21306A31304A3130CA35BA45BA21320141B7F91 15>I<1310A3EB1FC0EB3040EB6F80EB800048C7FC120212065A120812185AA212201260 A312E05A7EA41270127C123FEA1FE0EA07F81200133C131C130C5BEA0310EA00E012257F 9C12>16 D<3801803000031370A3380700E0A4380E01C0A4381C0388A3EA1E07383E1990 383BE0E00038C7FCA25AA45AA25A151B7F9119>22 D<3801FFF85A120F381E1E00EA180E EA38061270A2EAE00EA3130C131C13185BEA60606C5A001FC7FC15127E9118>27 D<5B1302A45BA45BA2137E3801C980380710E0000C13600018137000381330EA7020A200 E01370A2134014E0A2386041C0EB838038308600EA1C9CEA07E00001C7FCA41202A41425 7E9C19>30 D<14401480A4EB0100A41302A2001C13060027130EEA4704140600871302A2 EA0E08A2001C1304A2EB1008A214101420EB2040000C138038072300EA01FCEA0040A45B A417257E9C1B>32 D<0008130648130EA248130614025A1308131800801304A2EB300C14 0800C01318EBF030B512F0387F9FE0EB1FC0383E0F00171280911A>I<13FCEA03FEEA0E 07EA180012105AA2EA10C0EA1720EA1FE0EA20005AA25AA21304EA4008EA6030EA3FE0EA 0F8010147F9213>I<126012F0A2126004047C830C>58 D<126012F0A212701210A41220 A212401280040C7C830C>I<12E01278121EEA0780EA01E0EA0078131EEB0780EB01E0EB 0078141EEC0780A2EC1E001478EB01E0EB0780011EC7FC1378EA01E0EA0780001EC8FC12 7812E019187D9520>62 D<140CA2141CA2143C145CA2149E148EEB010E1302A21304A213 081310A2497EEB3FFFEB40071380A2EA0100A212025AA2001C148039FF803FF01C1D7F9C 1F>65 D<48B5FC39003C01C090383800E015F01570A25B15F0A2EC01E09038E003C0EC07 80EC1F00EBFFFC3801C00FEC0780EC03C0A2EA0380A439070007801500140E5C000E1378 B512C01C1C7E9B1F>I<903801F80890380E0618903838013890386000F048481370485A 48C71230481420120E5A123C15005AA35AA45CA300701302A200305B00385B6C5B6C1360 38070180D800FEC7FC1D1E7E9C1E>I<48B5128039003C01E090383800701538153C151C 5B151EA35BA44848133CA3153848481378157015F015E039070001C0EC0380EC0700141C 000E1378B512C01F1C7E9B22>I<48B512F839003C0078013813181510A35BA214081500 495AA21430EBFFF03801C020A4390380404014001580A23907000100A25C1406000E133E B512FC1D1C7E9B1F>I<48B512F038003C00013813301520A35BA214081500495AA21430 EBFFF03801C020A448485A91C7FCA348C8FCA45AEAFFF01C1C7E9B1B>I<903801F80890 380E0618903838013890386000F048481370485A48C71230481420120E5A123C15005AA3 5AA2EC7FF0EC07801500A31270140E123012386C131E6C136438070184D800FEC7FC1D1E 7E9C21>I<3A01FFC3FF803A003C00780001381370A4495BA449485AA390B5FC3901C003 80A4484848C7FCA43807000EA448131E39FFE1FFC0211C7E9B23>I<48B5FC39003C03C0 90383800E015F01570A24913F0A315E0EBE001EC03C0EC0700141E3801FFF001C0C7FCA3 485AA448C8FCA45AEAFFE01C1C7E9B1B>80 DI<39FFC00FF0391C00038015001402A25C5C121E000E5B1430 14205CA25C49C7FC120FEA07025BA25BA25B5BEA03A013C05BA290C8FCA21C1D7D9B18> 86 D<3AFFC0FFC0FF3A3C001C003C001C1510143C1620025C1340A2029C1380A2903901 1C0100A20102130213045D01085BA2496C5A121ED80E205BA201405B018013C05D260F00 0FC7FCA2000E130EA2000C130CA2281D7D9B27>I<3A01FFC0FF803A001E003C00011C13 306D13205D010F5B6D48C7FC1482EB038414CCEB01D814F05C130080EB0170EB0278EB04 381308EB103CEB201CEB401EEB800E3801000F00027F1206001E497E39FF803FF0211C7F 9B22>I<39FFE007F8390F0001E0158015006C13026D5A00035BEBC018141000015B6D5A 00005B01F1C7FC13F21376137C1338A25BA45BA4485AEA1FFC1D1C7F9B18>I97 D<123F1207A2120EA45AA4EA39E0EA3A30EA3C1812381270131CA3EAE038A31330 1370136013C01261EA2300121E0E1D7E9C12>IIIIII< EA0FC01201A2485AA448C7FCA4EA0E3E13C3380F0380120E121E121CA338380700A3130E 00701320A2131C144038E00C8038600700131D7E9C18>II<13 07130FA213061300A61378139CEA010C1202131C12041200A21338A41370A413E0A4EA01 C01261EAF180EAF30012E6127C1024809B11>III<39381F81F0394E20C618394640E81CEB80F0EA8F00008E13 E0120EA2391C01C038A315703938038071A215E115E23970070064D83003133820127E91 24>II<380787803809C8603808D03013E0EA11 C014381201A238038070A31460380700E014C0EB0180EB8300EA0E86137890C7FCA25AA4 123CB4FC151A819115>112 DIII<13C01201A3EA0380A4EAFFF0EA0700A3120EA45AA4EA 3820A21340A2EA1880EA0F000C1A80990F>I<001C13C0EA27011247A238870380A2120E A2381C0700A438180E20A3EA1C1E380C26403807C38013127E9118>I I<001CEBC080392701C1C0124714C03987038040A2120EA2391C070080A3EC0100EA1806 A2381C0E02EB0F04380E13083803E1F01A127E911E>I<380787803808C8403810F0C038 20F1E0EBE3C03840E1803800E000A2485AA43863808012F3EB810012E5EA84C6EA787813 127E9118>I<001C13C0EA27011247A238870380A2120EA2381C0700A4EA180EA3EA1C1E EA0C3CEA07DCEA001C1318EA6038EAF0305B485AEA4180003EC7FC121A7E9114>II E /Fn 25 118 df0 D<126012F0A2126004047C8B0C>I<0040132000C01360006013C03830018038180300EA 0C066C5A6C5AEA01B0EA00E0A2EA01B0EA0318EA060C487E487E38300180386000C04813 600040132013147A9320>I<90387FFF8048B5FCD80780C7FC000EC8FC12185AA25AA25A A71260A27EA27E120E6C7E0001B512806C7E90C8FCA7007FB51280A219227D9920>18 D20 D<12C012F0123C120FEA03C0EA00F0133C130FEB03C0 EB00F0143C140FEC0380EC0F00143C14F0EB03C0010FC7FC133C13F0EA03C0000FC8FC12 3C127012C0C9FCA7007FB5FCB6128019227D9920>I<90387FFF800003B5FCD80780C7FC 000CC8FC5A5AA25AA25AA81260A27EA27E120E6C7E0001B512806C7E191A7D9620>26 D<153081A381A281811680ED00C0B712F8A2C912C0ED0380160015065DA25DA35D25167E 942A>33 D<1403A26E7E8114001560007FB512F0B67EC8120E81ED01E0ED0078ED01E0ED 0380ED06005DB612F86C5CC812605D4A5AA24AC7FCA225187E952A>41 D50 D<1304130CEA03CCEA0C38EA1818EA30 1C133CEA703EEA60361366A2EAE067A213C7A3EAE187A3EAE307A312E6A3EA6606126CEA 7C0EEA3C0C1238EA1818EA1C30EA33C0EA3000A210237E9F15>59 D69 D<0103B5FC131F903830E00E01C1130C00011400EA0381 EB01C01206EA0003A25CA2130791C7FCECFFC0491300010EC7FC131E131CA25BA25BA2EA 30E01270EAFD80B4C8FC123C201D7F9B1E>I81 DII<15 0348B512FE000714F8390C00E00048485A1230EA700312F000C05B12001307A291C7FCA2 5BA2130EA2131EA2131CA2133C1338A213781370A213F05B5B485A20207F9C17>II<011F131C90383F807C01EF133CEA0187390007 C0381530010313601580ECC10014C614C814F014C0A21307130B13331343EA0183EA0203 1204121800307F127039F001E180ECF70000F813FC38E000F81E1C7E9B1E>88 D<0040130200C01306B20060130CA26C1318001C1370380F01E03803FF803800FE00171A 7E981C>91 D<133C13E0EA01C013801203AD13005A121C12F0121C12077E1380AD120113 C0EA00E0133C0E297D9E15>102 D<12F0121C12077E1380AD120113C0EA00E0133C13E0 EA01C013801203AD13005A121C12F00E297D9E15>I<12C0B3B3A502297B9E0C>106 D<00C01306B3A5B512FE7E17197E981C>116 DI E /Fo 32 122 df45 D<13181378EA01F812FFA212 01B3A7387FFFE0A213207C9F1C>49 DI<13FE3807FFC038 0F07E0381E03F0123FEB81F8A3EA1F0314F0120014E0EB07C0EB1F803801FE007F380007 C0EB01F014F8EB00FCA2003C13FE127EB4FCA314FCEA7E01007813F8381E07F0380FFFC0 3801FE0017207E9F1C>I<14E013011303A21307130F131FA21337137713E7EA01C71387 EA03071207120E120C12181238127012E0B6FCA2380007E0A790B5FCA218207E9F1C>I< 00301320383E01E0383FFFC0148014005B13F8EA33C00030C7FCA4EA31FCEA37FF383E0F C0383807E0EA3003000013F0A214F8A21238127C12FEA200FC13F0A2387007E0003013C0 383C1F80380FFF00EA03F815207D9F1C>I67 D69 D72 DI79 DI 82 D<3801FE023807FF86381F01FE383C007E007C131E0078130EA200F81306A27E1400 B4FC13E06CB4FC14C06C13F06C13F86C13FC000313FEEA003F1303EB007F143FA200C013 1FA36C131EA26C133C12FCB413F838C7FFE00080138018227DA11F>I<007FB61280A239 7E03F80F00781407007014030060140100E015C0A200C01400A400001500B3A248B512F0 A222227EA127>I97 D99 DI<13FE3807FF80380F87C0381E01E0003E13F0EA7C0014 F812FCA2B5FCA200FCC7FCA3127CA2127E003E13186C1330380FC0703803FFC0C6130015 167E951A>II<3801FE0F3907FFBF80380F87C7381F03E7391E01E00000 3E7FA5001E5BEA1F03380F87C0EBFF80D809FEC7FC0018C8FCA2121C381FFFE06C13F86C 13FE001F7F383C003F48EB0F80481307A40078EB0F006C131E001F137C6CB45A000113C0 19217F951C>II<121C123E127FA3123E121CC7FCA7B4FCA2121FB2EAFFE0A20B247E A310>I108 D<3AFF07F007F090391FFC1FFC3A 1F303E303E01401340496C487EA201001300AE3BFFE0FFE0FFE0A22B167E9530>I<38FF 07E0EB1FF8381F307CEB403CEB803EA21300AE39FFE1FFC0A21A167E951F>I<13FE3807 FFC0380F83E0381E00F0003E13F848137CA300FC137EA7007C137CA26C13F8381F01F038 0F83E03807FFC03800FE0017167E951C>I114 DI<487EA41203A21207A2120F123FB5FCA2EA0F80ABEB8180 A5EB8300EA07C3EA03FEEA00F811207F9F16>I<38FF01FEA2381F003EAF147E14FE380F 81BE3907FF3FC0EA01FC1A167E951F>I<39FFE01FE0A2391F800700000F1306EBC00E00 07130C13E000035BA26C6C5AA26C6C5AA2EB7CC0A2137F6D5AA26DC7FCA2130EA2130CA2 5B1278EAFC3813305BEA69C0EA7F80001FC8FC1B207F951E>121 D E /Fp 3 83 df24 D<141880A280140780B612C081C81238151EED0780ED0E001538 5DB612C05DC70003C7FC1406A25CA25C21167E9326>41 D82 D E /Fq 3 90 df<0003B512C038007001140015405BA43901C02000A3 146048B45A13801440A248485A1401A21402120E14061404140C481338B512F81A1A7E99 1C>69 D<3901FF01FE39003C00F01540011C1380EC0100EB0E025CEB0F086D5A14A0EB03 C0A213011303497E1304497EEB1070EB2078EB4038138048487E120248131E121EB4EB7F C01F1A7F9920>88 D<39FF800FE0391E0007001406000E1304000F5B6C5B5C6D5A000313 C0EBC180000190C7FC13C213E4EA00E813F013705BA4485AA4485AEA1FF81B1A7E9916> I E /Fr 44 124 df<121812381278123812081210A21220A212401280050B7D830C>44 DI<1230127812F0126005047C830C>I<137CEA0186EA0303 1206000C1380121CA21238A338700700A4EAE00EA35BA213185BEA60606C5A001FC7FC11 187C9714>48 D<1308131813301370EA01F0EA0E70EA00E0A4EA01C0A4EA0380A4EA0700 A45AEAFFE00D187C9714>I<131EEB6180EA0180EA03031206000EC7FC5A12181238EA39 F0EA7218EA740CEA780E127012F012E0A35BA2EA60385BEA30C0EA1F8011187C9714>54 D<1420146014E0A2130114F0EB0270A213041308A21310A213201340A2EB8038EBFFF838 0100381202A25AA25A121838FE01FF181A7E991D>65 D<3803FFF83800700E1406140713 E0A43801C00E141C143814703803FFE0EB80781438141CEA0700A4000E1338A2147014E0 381C03C0B51200181A7D991B>II<0003B5FC380070071403140113E0A43801C080A313C13803FF001381A3EA 0702EB0004A21408120E1418141014304813E0B5FC181A7D991A>69 D<0003B5FC380070071403140113E0A43801C080A313C13803FF001381A3EA070290C7FC A3120EA4121EEAFFC0181A7D9919>I<3903FF1FF83900700380A39038E00700A43801C0 0EA43803FFFCEB801CA348485AA4000E5BA4485B38FF87FC1D1A7D991D>72 D I I76 DI<3903F007F839007800C01580A290389C0100A313 8E38010E0213061307A238020384A3EB01C4000413C8A2EB00E8A24813F01470A2121814 2012FE1D1A7D991D>I<3803FFF83800701C1406140713E0A43801C00EA2141C14383803 8060EBFF80EB8000A248C7FCA4120EA45AB47E181A7D991A>80 D<3803FFF03800701C14 0E140713E0A43801C00E141C143814E03803FF80EB80C014601470EA0700A4000E13E0A2 14E114E248136238FF803C181A7D991C>82 DI<383FFFFC38381C0C00201304124013381280A3380070 00A45BA4485AA4485AA41207EAFFF8161A79991B>I97 D<127E120EA35AA45AA2EA 3BC0EA3C301278EA7018A3EAE038A4EAC070136013E0EA60C0EA6380EA1E000D1A7C9912 >IIII<1307EB0980131B EB3B00133813301370A4EA07FFEA00E0A5485AA5485AA490C7FC5AA21206126612E412CC 1270112181990C>I<13F338038B8038060700120E120C121CEA380EA4EA301CA3EA183C 5BEA07B8EA0038A25B1260EAE0E0EAC1C0007FC7FC11177E8F12>II<1203120712061200A61238124C124E128E129CA2121C1238A21270 1272A212E212E41264123808197C980C>I107 D<121F1207A3120EA4121CA41238A41270A412E4A412E81230081A7D990A>I<38 307C1E38598663399E0783801403129CA239380E0700A3140ED8701C1340A2141C158038 E0380C39601807001A107C8F1F>IIII114 DI<1206120EA45AA2EAFFC0EA1C005AA45AA412E1A312E212E4 12380A177C960D>III<38380C10384C0E38EA4E1C008E131812 9CA2381C38101238A338707020A2144012303818B880380F0F0015107C8F19>I121 D123 D E /Fs 8 117 df<127812FCA4127806067D850C>46 D<1303497EA2497EA3EB1BE0A2 EB3BF01331A2EB60F8A2EBE0FCEBC07CA248487EEBFFFE487FEB001F4814800006130FA2 48EB07C039FF803FFCA21E1A7F9921>65 D97 D<12FCA2123CA713FE38 3F8780383E01C0003C13E0EB00F0A214F8A514F0A2EB01E0003E13C0383B07803830FE00 151A7E9919>II114 DI<1206A4120EA2121EEA3FF012 FFEA1E00A81318A5EA0F30EA03E00D187F9711>I E /Ft 65 128 df<90387E1F803901C17040390703C0600006EB80E0000E14401500A5B612E0380E0380 AE397F8FE3FC1E1A809920>14 D38 D<1380EA010012025A120C120812185AA35A A412E0AA1260A47EA37E1208120C12047E7EEA008009267D9B0F>40 D<7E12407E7E12181208120C7EA37EA41380AA1300A41206A35A1208121812105A5A5A09 267E9B0F>I<126012F0A212701210A31220A21240A2040B7D830B>44 DI<126012F0A2126004047D830B>I48 D<12035AB4FC1207B3A2EA7FF80D187D9713>III<1318A21338137813F813B8EA01381202A2120412081218121012201240 12C0B5FCEA0038A6EA03FF10187F9713>III<1240EA7F FF13FEA2EA4004EA80081310A2EA00201340A21380120113005AA25A1206A2120EA51204 10197E9813>III<126012F0 A212601200A8126012F0A2126004107D8F0B>I<130CA3131EA2132F1327A2EB4380A3EB 81C0A200017F1300A248B47E38020070A2487FA3487FA2003C131EB4EBFFC01A1A7F991D >65 DIII III<39FFE1FFC0390E001C00AB380FFFFC380E001CAC39FFE1FFC01A1A7F99 1D>III<39FFE01FC0390E000F00140C14085C5C5C495A0102C7FC5B 130C131C132E1347EB8380EA0F03380E01C06D7EA2147080A280141E141F39FFE07FC01A 1A7F991E>III<00FEEB7FC0000FEB0E001404 EA0B80EA09C0A2EA08E01370A21338131CA2130E1307EB0384A2EB01C4EB00E4A2147414 3CA2141C140C121C38FF80041A1A7F991D>I<137F3801C1C038070070000E7F487F003C 131E0038130E0078130F00707F00F01480A80078EB0F00A20038130E003C131E001C131C 6C5B6C5B3801C1C0D8007FC7FC191A7E991E>II82 DI<007FB5FC38701C0700401301A200C0148000801300A300001400B1 3803FFE0191A7F991C>I<39FFE07FC0390E000E001404B200065B12076C5B6C6C5A3800 E0C0013FC7FC1A1A7F991D>I<3AFF81FF07F03A3C007801C0001CEC0080A36C90389C01 00A33907010E02A33903830F04EB8207A2150C3901C40388A33900E801D0A390387000E0 A301305B01201340241A7F9927>87 D90 D97 D<12FC121CA913FCEA1D07381E0380381C01C0130014E0 A6EB01C01480381E0300EA1906EA10F8131A809915>II<133F1307A9EA03E7EA0C17EA180F 487E127012E0A6126012706C5AEA1C373807C7E0131A7F9915>IIII<12FC121CA9137CEA1D87381E0380A2121C AB38FF9FF0141A809915>I<1218123CA212181200A612FC121CAE12FF081A80990A>I<12 FC121CA9EB1FC0EB0F00130C5B13205B13E0121DEA1E70EA1C7813387F131E7F148038FF 9FE0131A809914>107 D<12FC121CB3A6EAFF80091A80990A>I<38FC7C1F391D8E638039 1E0781C0A2001C1301AB39FF9FE7F81D107F8F20>IIII114 DI<1208A41218A2 1238EAFFC0EA3800A81320A41218EA1C40EA07800B177F960F>I<38FC1F80EA1C03AB13 07120CEA0E0B3803F3F01410808F15>I<38FF0F80383C0700EA1C061304A26C5AA26C5A A3EA03A0A2EA01C0A36C5A11107F8F14>I<39FE7F1F8039381C0700003C1306381C0C04 130E380E16081317A238072310149013A33803C1A014E0380180C0A319107F8F1C>I<38 FF0F80383C0700EA1C061304A26C5AA26C5AA3EA03A0A2EA01C0A36C5AA248C7FCA212E1 12E212E4127811177F8F14>121 DII127 D E /Fu 6 55 df<1218127812981218AC12FF08107D8F0F>49 D<121FEA6180EA40C0EA806012C01200A213C0EA0180EA030012065AEA10201220EA7FC0 12FF0B107F8F0F>I<121FEA2180EA60C0A212001380EA0100121FEA00801340136012C0 A2EA8040EA6080EA1F000B107F8F0F>IIII E /Fv 18 118 df11 D<133C13C2EA0103120212041302EA080613FCA21304 EA1006A4EA200CA2EA30181310EA4860EA47C0EA4000A25AA4101A7F9313>I22 D<124012E012601220A31240A2128003097D820A>59 D<7FA638F08780381FFC00EA07F0 EA01C0EA0360EA0220EA0630487EEA0808487E1110818E11>63 D<5B5B5B1480130B131B 13131323A21343138314C0EA0101EA03FFEA02011204120C1208001813E038FE07F81514 7F9319>65 D<3807FFE03800E0703801C018141CA338038038A21470EB81C03807FF0090 C7FCA3120EA45AB47E16147F9315>80 D<133F3801C1C0380300E0000613704813304813 3812385AA3481370A314E014C0EA60013871C380383A2600EA1C3C3807F040EA003014C0 EB3180133FEB1F00130E151A7E931A>I<3807FFC03800E0703801C018141CA338038038 147014C0EBFF00380701C0A2EB00E0A2380E01C0A314C2001C13C438FF807817147F9319 >I<1206120712061200A41238124CA2128C12981218A212301232A21264A2123808147F 930C>105 D<1330133813301300A4EA01C0EA0260EA0430136012081200A213C0A4EA01 80A4EA630012E312C612780D1A81930E>I<121E12065AA45A1338135C139CEA3118EA36 001238EA3F80EA61C0EA60C8A3EAC0D013600E147F9312>I<123C120C1218A41230A412 60A412C012C8A312D0126006147F930A>I<3830F87C38590C86384E0D06EA9C0EEA980C 1218A248485A15801418A23960301900140E190D7F8C1D>II113 DI117 D E /Fw 10 55 df<120212041208121812101230122012601240A212C0AA1240A21260 1220123012101218120812041202071E7D950D>40 D<1280124012201230121012181208 120C1204A21206AA1204A2120C1208121812101230122012401280071E7E950D>I<1360 AAB512F0A238006000AA14167E9119>43 D<120FEA30C0EA6060A2EA4020EAC030A9EA40 20EA6060A2EA30C0EA0F000C137E9211>48 D<120C121C12EC120CAFEAFFC00A137D9211 >I<121FEA60C01360EAF07013301260EA0070A2136013C012011380EA02005AEA081012 10EA2020EA7FE012FF0C137E9211>II<136013E0A2EA 016012021206120C120812101220126012C0EAFFFCEA0060A5EA03FC0E137F9211>III E /Fx 77 125 df11 D<137E3801C180EA0301380703C0120EEB 018090C7FCA5B512C0EA0E01B0387F87F8151D809C17>II<90383F07E03901C09C18380380F0D807 01133C000E13E00100131892C7FCA5B612FC390E00E01CB03A7FC7FCFF80211D809C23> I<1380A2EA07E0EA1898EA3084EA6082EA4081EAC087138FA21386EAE0801270127EEA3F C0EA1FF0EA0FF8EA03FCEA00BE138E13871260EAF083A212E0EA808212401384EA2088EA 1890EA07E0EA0080A210217E9E15>36 D<126012F012F812681208A31210A21220124012 80050C7C9C0C>39 D<1380EA0100120212065AA25AA25AA35AA412E0AC1260A47EA37EA2 7EA27E12027EEA0080092A7C9E10>I<7E12407E12307EA27EA27EA37EA41380AC1300A4 1206A35AA25AA25A12205A5A092A7E9E10>I<1306ADB612E0A2D80006C7FCAD1B1C7E97 20>43 D<126012F0A212701210A41220A212401280040C7C830C>II<126012F0A2126004047C830C>I48 D<5A1207123F12C71207B3A5EAFFF80D1C7C9B15>III<130CA2131C133CA2135C13DC139CEA011C12 0312021204120C1208121012301220124012C0B512C038001C00A73801FFC0121C7F9B15 >II<13F0EA030CEA0404 EA0C0EEA181E1230130CEA7000A21260EAE3E0EAE430EAE818EAF00C130EEAE0061307A5 1260A2EA7006EA300E130CEA1818EA0C30EA03E0101D7E9B15>I<1240387FFF801400A2 EA4002485AA25B485AA25B1360134013C0A212015BA21203A41207A66CC7FC111D7E9B15 >III<126012F0A212601200AA126012F0A2126004127C910C>I<126012F0A212601200 AA126012F0A212701210A41220A212401280041A7C910C>I<007FB512C0B612E0C9FCA8 B612E06C14C01B0C7E8F20>61 D63 D<1306A3130FA3EB1780A2EB37C01323A2EB43E01341A2EB80F0A338010078A2EBFFF838 02003CA3487FA2000C131F80001E5BB4EBFFF01C1D7F9C1F>65 DI<90381F8080EBE0613801801938070007000E13035A14015A00781300A212 7000F01400A8007014801278A212386CEB0100A26C13026C5B380180083800E030EB1FC0 191E7E9C1E>IIII<90381F8080EBE0613801801938070007000E13035A14015A007813 00A2127000F01400A6ECFFF0EC0F80007013071278A212387EA27E6C130B380180113800 E06090381F80001C1E7E9C21>I<39FFF0FFF0390F000F00AC90B5FCEB000FAD39FFF0FF F01C1C7F9B1F>II<39FFF01FE0390F000780EC 060014045C5C5C5C5C49C7FC13021306130FEB17801327EB43C0EB81E013016D7E1478A2 80143E141E80158015C039FFF03FF01C1C7F9B20>75 DIIIII82 D<3807E080EA1C19EA30051303EA600112E01300 A36C13007E127CEA7FC0EA3FF8EA1FFEEA07FFC61380130FEB07C0130313011280A300C0 1380A238E00300EAD002EACC0CEA83F8121E7E9C17>I<007FB512C038700F0100601300 00401440A200C014201280A300001400B1497E3803FFFC1B1C7F9B1E>I<39FFF01FF039 0F000380EC0100B3A26C1302138000035BEA01C03800E018EB7060EB0F801C1D7F9B1F> I<39FFE00FF0391F0003C0EC01806C1400A238078002A213C000035BA2EBE00C00011308 A26C6C5AA213F8EB7820A26D5AA36D5AA2131F6DC7FCA21306A31C1D7F9B1F>I<3AFFE1 FFC0FF3A1F003E003C001E013C13186C6D1310A32607801F1320A33A03C0278040A33A01 E043C080A33A00F081E100A39038F900F3017913F2A2017E137E013E137CA2013C133C01 1C1338A20118131801081310281D7F9B2B>I<387FFFF0EA7C01007013E0386003C0A238 400780130F1400131E12005B137C13785BA2485A1203EBC010EA0780A2EA0F0048133000 1E13205A14604813E0EAF803B5FC141C7E9B19>90 D<12FEA212C0B3B312FEA207297C9E 0C>I<12FEA21206B3B312FEA20729809E0C>93 D97 D<12FC121CAA137CEA1D87381E0180381C00C014E014601470A6146014E014C0381E0180 38190700EA10FC141D7F9C17>IIII<13F8EA018CEA071E1206EA0E0C1300A6EAFFE0EA0E00B0EA7F E00F1D809C0D>II<12FC121CAA137C1387EA1D03001E1380121CAD38 FF9FF0141D7F9C17>I<1218123CA21218C7FCA712FC121CB0EAFF80091D7F9C0C>I<13C0 EA01E0A2EA00C01300A7EA07E01200B3A21260EAF0C012F1EA6180EA3E000B25839C0D> I<12FC121CAAEB0FE0EB0780EB06005B13105B5B13E0121DEA1E70EA1C781338133C131C 7F130F148038FF9FE0131D7F9C16>I<12FC121CB3A9EAFF80091D7F9C0C>I<39FC7E07E0 391C838838391D019018001EEBE01C001C13C0AD3AFF8FF8FF8021127F9124>IIII<3803E080EA0E19EA1805EA3807EA7003A212E0 A61270A2EA38071218EA0E1BEA03E3EA0003A7EB1FF0141A7F9116>II I<1204A4120CA2121C123CEAFFE0EA1C00A91310A5120CEA0E20EA03C00C1A7F9910>I< 38FC1F80EA1C03AD1307120CEA0E1B3803E3F014127F9117>I<38FF07E0383C0380381C 0100A2EA0E02A2EA0F06EA0704A2EA0388A213C8EA01D0A2EA00E0A3134013127F9116> I<39FF3FC7E0393C0703C0001CEB01801500130B000E1382A21311000713C4A213203803 A0E8A2EBC06800011370A2EB8030000013201B127F911E>I<38FF0FE0381E0700EA1C06 EA0E046C5AEA039013B0EA01E012007F12011338EA021C1204EA0C0E487E003C138038FE 1FF014127F9116>I<38FF07E0383C0380381C0100A2EA0E02A2EA0F06EA0704A2EA0388 A213C8EA01D0A2EA00E0A31340A25BA212F000F1C7FC12F312661238131A7F9116>II124 D E /Fy 25 122 df72 D82 D<9038FF80600003EBF0E0 000F13F8381F80FD383F001F003E1307481303A200FC1301A214007EA26C140013C0EA7F FCEBFFE06C13F86C13FE80000714806C14C0C6FC010F13E0EB007FEC1FF0140F140700E0 1303A46C14E0A26C13076C14C0B4EB0F80EBE03F39E3FFFE0000E15B38C01FF01C297CA8 25>I<007FB71280A39039807F807FD87C00140F00781507A20070150300F016C0A24815 01A5C791C7FCB3A490B612C0A32A287EA72F>II<3803FF80000F13F0381F01FC383F80FE147F801580EA1F00C7FCA4EB 3FFF3801FC3FEA0FE0EA1F80EA3F00127E5AA4145F007E13DF393F839FFC381FFE0F3803 FC031E1B7E9A21>97 DIIIII<9038 FF80F00003EBE3F8390FC1FE1C391F007C7C48137E003EEB3E10007EEB3F00A6003E133E 003F137E6C137C380FC1F8380BFFE00018138090C8FC1238A2123C383FFFF814FF6C14C0 6C14E06C14F0121F383C0007007CEB01F8481300A4007CEB01F0A2003FEB07E0390FC01F 806CB5120038007FF01E287E9A22>II<1207EA0F80EA1F C0EA3FE0A3EA1FC0EA0F80EA0700C7FCA7EAFFE0A3120FB3A3EAFFFEA30F2B7EAA12>I< EAFFE0A3120FB3B2EAFFFEA30F2A7EA912>108 D<26FFC07FEB1FC0903AC1FFC07FF090 3AC307E0C1F8D80FC49038F101FC9039C803F20001D801FE7F01D05BA201E05BB03CFFFE 3FFF8FFFE0A3331B7D9A38>I<38FFC07E9038C1FF809038C30FC0D80FC413E0EBC80701 D813F013D0A213E0B039FFFE3FFFA3201B7D9A25>II<38FFC1F0EBC7FCEB C63E380FCC7F13D813D0A2EBF03EEBE000B0B5FCA3181B7F9A1B>114 D<3803FE30380FFFF0EA3E03EA7800127000F01370A27E00FE1300EAFFE06CB4FC14C06C 13E06C13F0000713F8C6FCEB07FC130000E0137C143C7E14387E6C137038FF01E038E7FF C000C11300161B7E9A1B>I<13E0A41201A31203A21207120F381FFFE0B5FCA2380FE000 AD1470A73807F0E0000313C03801FF8038007F0014267FA51A>I<39FFE07FF0A3000F13 07B2140FA2000713173903F067FF3801FFC738007F87201B7D9A25>I<39FFFC03FFA339 0FF000F0000714E07F0003EB01C0A2EBFC0300011480EBFE070000140013FFEB7F0EA214 9EEB3F9C14FC6D5AA26D5AA36D5AA26D5AA2201B7F9A23>I<3BFFFC7FFC1FFCA33B0FE0 0FE001C02607F007EB0380A201F8EBF00700031600EC0FF801FC5C0001150EEC1FFC2600 FE1C5B15FE9039FF387E3C017F1438EC787F6D486C5A16F0ECE01F011F5CA26D486C5AA2 EC800701075CA22E1B7F9A31>I<39FFFC03FFA3390FF000F0000714E07F0003EB01C0A2 EBFC0300011480EBFE070000140013FFEB7F0EA2149EEB3F9C14FC6D5AA26D5AA36D5AA2 6D5AA25CA21307003890C7FCEA7C0FEAFE0E131E131C5BEA74F0EA3FE0EA0F8020277F9A 23>121 D E end %%EndProlog %%BeginSetup %%Feature: *Resolution 300dpi TeXDict begin %%PaperSize: a4 %%BeginPaperSize: a4 a4 %%EndPaperSize %%EndSetup %%Page: 1 1 1 0 bop 268 194 a Fy(Relativ)n(e)24 b(Undecidabilit)n(y)i(in)e(the)e(T) -6 b(ermination)401 263 y(Hierarc)n(h)n(y)24 b(of)d(Single)j(Rewrite)f (Rules)251 409 y Fx(Alfons)13 b(Geser)481 394 y Fw(1)s Fv(?)520 409 y Fx(,)g(Aart)i(Middeldorp)853 394 y Fw(2)q Fv(??)907 409 y Fx(,)e(Enno)h(Ohlebusc)o(h)1228 394 y Fw(3)1248 409 y Fx(,)g(Hans)g(Zan)o(tema)1538 394 y Fw(4)602 480 y Fu(1)638 496 y Ft(Univ)o(ersit)o(y)h(of)e(T)q(\177)-20 b(ubingen,)14 b(German)o(y)635 526 y Fu(2)672 542 y Ft(Univ)o(ersit)o (y)h(of)d(Tsukuba,)i(Japan)610 572 y Fu(3)647 588 y Ft(Univ)o(ersit)o (y)g(of)f(Bielefeld,)i(German)o(y)578 617 y Fu(4)615 633 y Ft(Utrec)o(h)o(t)e(Univ)o(ersit)o(y)m(,)h(The)f(Netherlands)301 816 y Fs(Abstract.)22 b Ft(F)m(or)14 b(a)g(hierarc)o(h)o(y)i(of)e(prop) q(erties)i(of)e(term)g(rewriting)i(systems,)f(re-)301 862 y(lated)e(to)f(termination,)i(w)o(e)e(pro)o(v)o(e)h Fr(r)n(elative)e(unde)n(cidabi)o(lity)h Ft(ev)o(en)h(in)g(the)f(case)h (of)301 908 y(single)e(rewrite)f(rules:)g(for)f(implication)q(s)j Fq(X)h Fp(\))e Fq(Y)18 b Ft(in)10 b(the)g(hierarc)o(h)o(y)h(the)e(prop) q(ert)o(y)301 953 y Fq(X)15 b Ft(is)f(undecidable)i(for)d(rewrite)g (rules)h(satisfying)h Fq(Y)9 b Ft(.)183 1102 y Fo(1)56 b(In)n(tro)r(duction)183 1210 y Fx(A)11 b(fundamen)o(tal)f(problem)g (in)h(the)h(theory)g(of)f(term)g(rewriting)g(is)g(the)h(detection)h(of) e(termi-)183 1260 y(nation:)i(for)h(a)h(\014xed)g(system)f(of)g (rewrite)i(rules,)f(determine)g(whether)h(there)g(are)f(in\014nite)183 1310 y(rewrite)20 b(sequences.)i(Besides)f(termination)d(a)h(n)o(um)o (b)q(er)g(of)g(related)h(prop)q(erties)h(are)f(of)183 1359 y(in)o(terest,)14 b(linearly)f(ordered)i(b)o(y)f(implication:)253 1454 y(p)q(olynomial)d(termination)f Fn(\))h Fm(!)q Fx(-termination)f Fn(\))h Fx(total)i(termination)336 1517 y Fn(\))e Fx(simple)i (termination)c Fn(\))j Fx(non-self-em)o(b)q(eddingness)f Fn(\))g Fx(termination)419 1579 y Fn(\))g Fx(non-lo)q(opingness)g Fn(\))g Fx(acyclicit)o(y)183 1674 y(W)m(e)j(call)g(this)g(the)i Fl(termination)f(hier)n(ar)n(chy)p Fx(.)e(Apart)i(from)e(p)q(olynomial) e(termination,)i(all)183 1724 y(prop)q(erties)18 b(in)f(the)g (termination)f(hierarc)o(h)o(y)h(are)g(kno)o(wn)g(to)g(b)q(e)g (undecidable)h(\([11)o(,)f(15)o(,)183 1773 y(13)o(,)d(18)o(,)g(8,)g(9)o (]\).)g(In)g([9)o(])g(w)o(e)h(sho)o(w)o(ed)f(the)h(stronger)g(result)g (of)f Fl(r)n(elative)g(unde)n(cidability)t Fx(:)g(for)183 1823 y(all)i(implications)e Fm(X)21 b Fn(\))c Fm(Y)26 b Fx(in)17 b(the)h(termination)e(hierarc)o(h)o(y)h(except)i(one|p)q (olynomial)183 1873 y(termination)9 b Fn(\))i Fm(!)q Fx(-termination|the)e(prop)q(ert)o(y)j Fm(X)j Fx(is)c(undecidable)g (for)g(term)g(rewriting)183 1923 y(systems)j(\(TRSs)g(for)f(short\))i (satisfying)e(prop)q(ert)o(y)h Fm(Y)c Fx(.)245 1974 y(In)19 b(this)g(pap)q(er)g(w)o(e)g(address)i(the)e(question)g(of)g(relativ)o (e)f(undecidabilit)o(y)g(for)h(TRSs)183 2024 y(consisting)14 b(of)g(a)h(single)f(rewrite)i(rule.)e(W)m(e)h(sho)o(w)f(that)h(for)g (all)e(implications)f Fm(X)17 b Fn(\))12 b Fm(Y)24 b Fx(in)183 2074 y(the)11 b(termination)d(hierarc)o(h)o(y)j(except)h(t)o (w)o(o|p)q(olynomia)o(l)7 b(termination)i Fn(\))h Fm(!)q Fx(-termination)p 183 2115 237 2 v 190 2142 a Fk(?)221 2158 y Ft(Corresp)q(onding)17 b(author.)f(Address)g(for)e(corresp)q (ondence:)j(Wilhelm-Sc)o(hi)q(c)o(k)n(ard)q(-Insti)q(tut)h(f)q(\177)-20 b(ur)221 2203 y(Informatik,)19 b(Univ)o(ersit\177)-19 b(at)20 b(T)q(\177)-20 b(ubingen,)20 b(Sand)f(13,)f(D-72076)h(T)q(\177) -20 b(ubingen,)20 b(German)o(y)m(.)e(Email:)221 2249 y Fj(geser@info)o(rm)o(ati)o(k.)o(uni)o(-tu)o(eb)o(ing)o(en)o(.de)o Ft(.)i(W)m(ork)j(carried)h(out)f(at)g(Univ)o(ersit\177)-19 b(at)25 b(P)o(assau,)221 2295 y(Lehrstuhl)14 b(f)q(\177)-20 b(ur)12 b(Programmiersysteme.)i(P)o(artially)g(supp)q(orted)g(b)o(y)f (gran)o(t)f Fj(Ku)19 b(996/3-1)9 b Ft(of)j(the)221 2340 y(Deutsc)o(he)i(F)m(orsc)o(h)o(ungsgemeinsc)o(ha)q(ft)h(within)g(the)e (Sc)o(h)o(w)o(erpunkt)h(Deduktion.)175 2370 y Fk(??)221 2386 y Ft(P)o(artially)k(supp)q(orted)g(b)o(y)e(the)g(Adv)n(anced)h (Information)g(T)m(ec)o(hnology)g(Program)g(\(AITP\))e(of)221 2432 y(the)e(Information)h(T)m(ec)o(hnology)h(Promotion)g(Agency)e (\(IP)m(A\).)893 2556 y Fx(1)p eop %%Page: 2 2 2 1 bop 340 194 a Fn(\))10 b Fx(total)f(termination|the)g(prop)q(ert)o (y)i Fm(X)i Fx(is)d(undecidable)h(for)f(one-rule)g(TRSs)g(satisfying) 340 244 y(prop)q(ert)o(y)15 b Fm(Y)9 b Fx(.)403 294 y(Dauc)o(het)21 b([1)o(])f(w)o(as)h(the)g(\014rst)g(to)g(pro)o(v)o(e)f(undecidabilit)o (y)g(of)g(termination)f(for)h(one-)340 344 y(rule)c(TRSs,)e(b)o(y)h (means)g(of)f(a)h(reduction)h(to)f(the)h(uniform)d(halting)h(problem)f (for)i(T)m(uring)340 394 y(mac)o(hines.)h(Middeldorp)h(and)g(Gramlic)o (h)d([13)o(])j(reduced)i(the)e(undecidabilit)o(y)f(of)h(simple)340 444 y(termination,)12 b(non-self-em)o(b)q(eddingness,)h(and)g(non-lo)q (opingness)h(for)f(one-rule)h(TRSs)f(to)340 493 y(the)g(uniform)c (halting)i(problem)f(for)i(linear)f(b)q(ounded)h(automata.)d(Lescanne) 14 b([12)o(])d(sho)o(w)o(ed)340 543 y(that)k(Dauc)o(het's)g(result)g (can)g(also)e(b)q(e)j(obtained)e(b)o(y)g(a)g(reduction)h(to)g(P)o (ost's)f(Corresp)q(on-)340 593 y(dence)h(Problem)d(\(PCP\).)i(The)g (results)g(presen)o(ted)i(in)d(this)g(pap)q(er)h(are)g(stronger)h(b)q (ecause)340 643 y(\(1\))f(w)o(e)h(obtain)e(the)h(same)f(undecidabilit)o (y)g(results)j(for)d(\(m)o(uc)o(h\))g(smaller)g(classes)i(of)e(one-)340 693 y(rule)h(TRSs,)g(and)f(\(2\))h(w)o(e)g(sho)o(w)f(the)i (undecidabilit)o(y)d(of)i(total)f(termination)f(for)h(one-rule)340 743 y(\(simply)i(terminating\))g(TRSs.)h(The)h(latter)f(solv)o(es)h (problem)e(87)h(in)g([4)o(])g(and)g(recti\014es)j(a)340 792 y(conjecture)d(in)d([18)o(].)403 843 y(The)j(relativ)o(e)g (undecidabilit)o(y)f(results)i(in)e([9])g(are)i(obtained)e(b)o(y)h (using)g(PCP)g(in)g(the)340 893 y(follo)o(wing)8 b(w)o(a)o(y:)g(for)h (the)i(lo)o(w)o(er)e(\014v)o(e)h(implications)d Fm(X)15 b Fn(\))c Fm(Y)19 b Fx(in)10 b(the)g(termination)e(hierarc)o(h)o(y)340 943 y(and)16 b(for)f(all)g(PCP)h(instances)h Fm(P)k Fx(a)16 b(TRS)f(is)h(constructed)i(that)e(alw)o(a)o(ys)f(satis\014es)h Fm(Y)25 b Fx(and)340 992 y(satis\014es)15 b Fm(X)j Fx(if)13 b(and)h(only)f(if)g Fm(P)19 b Fx(admits)12 b(no)i(solution.)f(In)h (this)f(pap)q(er)i(w)o(e)f(presen)o(t)i(a)d(more)340 1042 y(uniform)g(approac)o(h.)i(First)g(w)o(e)h(construct)g(a)f(TRS)g Fn(U)t Fx(\()p Fm(P)q(;)7 b Fn(Q)p Fx(\))14 b(parameterized)h(b)o(y)g (a)g(PCP)340 1092 y(instance)j Fm(P)23 b Fx(and)17 b(a)f(TRS)h Fn(Q)p Fx(.)f(The)i(TRS)e Fn(U)t Fx(\()p Fm(P)q(;)7 b Fn(Q)p Fx(\))17 b(has)g(the)h(follo)o(wing)c(prop)q(erties:)k(\(1\))340 1142 y(the)d(left-hand)f(sides)h(of)e(its)h(rewrite)h(rules)g(are)f (the)h(same,)e(\(2\))h(if)f Fm(P)20 b Fx(admits)12 b(no)i(solution)340 1192 y(then)f Fn(U)t Fx(\()p Fm(P)q(;)7 b Fn(Q)p Fx(\))12 b(is)h(totally)e(terminating,)f(and)i(\(3\))h(if)e Fm(P)18 b Fx(admits)11 b(a)h(solution)g(then)h Fn(U)t Fx(\()p Fm(P)q(;)7 b Fn(Q)p Fx(\))340 1242 y(sim)o(ulates)16 b Fn(Q)p Fx(.)g(Because)j(of)d(prop)q(ert)o(y)h(\(1\))g(ev)o(ery)g Fn(U)t Fx(\()p Fm(P)q(;)7 b Fn(Q)p Fx(\))17 b(can)g(b)q(e)g(compressed) h(in)o(to)e(a)340 1291 y(one-rule)11 b(TRS)e Fn(S)s Fx(\()p Fm(P)q(;)e Fn(Q)p Fx(\))j(without)g(a\013ecting)g(the)g(termination)f (b)q(eha)o(viour.)g(In)h(particular,)340 1341 y(if)h Fm(P)16 b Fx(admits)10 b(no)h(solution)f(then)i Fn(S)s Fx(\()p Fm(P)q(;)7 b Fn(Q)p Fx(\))k(is)g(totally)f(terminating.)f (Finally)m(,)g(for)i(the)h(lo)o(w)o(er)340 1391 y(\014v)o(e)f (implicatio)o(ns)d Fm(X)15 b Fn(\))c Fm(Y)19 b Fx(in)10 b(the)g(termination)f(hierarc)o(h)o(y)h(w)o(e)g(de\014ne)h(a)f (suitable)g(TRS)f Fn(Q)340 1441 y Fx(suc)o(h)k(that)g Fn(S)s Fx(\()p Fm(P)q(;)7 b Fn(Q)p Fx(\))12 b(satis\014es)h Fm(Y)22 b Fx(if)11 b(and)i(only)e(if)h Fm(P)17 b Fx(admits)11 b(no)h(solution.)f(The)i(adv)n(an)o(tage)340 1491 y(of)i(this)g (approac)o(h)g(is)g(that)g(the)g(complicated)f(part|the)h(construction) h(and)f(prop)q(erties)340 1540 y(of)k(the)g(TRS)g Fn(U)t Fx(\()p Fm(P)q(;)7 b Fn(Q)p Fx(\)|is)18 b(indep)q(enden)o(t)i(of)e(the) i(in)o(v)o(olv)o(ed)d(lev)o(el)i(in)g(the)g(termination)340 1590 y(hierarc)o(h)o(y)m(.)403 1641 y(The)d(remainder)f(of)g(this)g (pap)q(er)i(is)e(organized)h(as)f(follo)o(ws.)f(In)h(the)i(next)f (section)g(w)o(e)340 1691 y(brie\015y)g(recall)g(the)h(de\014nitions)e (of)h(the)g(prop)q(erties)h(in)f(the)g(termination)e(hierarc)o(h)o(y)i (and)340 1741 y(PCP)m(.)i(In)h(Section)g(3)f(w)o(e)h(de\014ne)g(the)g (TRS)f Fn(U)t Fx(\()p Fm(P)q(;)7 b Fn(Q)p Fx(\))18 b(and)g(sho)o(w)h (that)f(it)g(sim)o(ulates)f Fn(Q)340 1790 y Fx(whenev)o(er)e Fm(P)k Fx(admits)11 b(a)i(solution.)f(In)h(Section)h(4)f(w)o(e)g (de\014ne)h(the)g(one-rule)g(TRS)f Fn(S)s Fx(\()p Fm(P)q(;)7 b Fn(Q)p Fx(\))340 1840 y(and)14 b(sho)o(w)g(that)g(it)g(inherits)g (the)h(termination)d(b)q(eha)o(viour)i(from)e Fn(U)t Fx(\()p Fm(P)q(;)7 b Fn(Q)p Fx(\).)13 b(In)h(Section)h(5)340 1890 y(w)o(e)20 b(instan)o(tiate)f Fn(S)s Fx(\()p Fm(P)q(;)7 b Fn(Q)p Fx(\))20 b(b)o(y)f(suitable)g(TRSs)h Fn(Q)f Fx(in)g(order)h(to)g(conclude)g(the)g(desired)340 1940 y(relativ)o(e)c(undecidabilit)o(y)f(results.)i(F)m(or)f(reasons)h(of)f (space,)g(the)h(di\016cult)f(pro)q(of)f(of)h(total)340 1990 y(termination)c(of)h Fn(U)t Fx(\()p Fm(P)q(;)7 b Fn(Q)p Fx(\))12 b(in)h(the)h(case)g(that)g Fm(P)k Fx(admits)12 b(no)h(solution)f(has)i(b)q(een)g(omitted.)340 2039 y(It)g(can)g(b)q(e) h(found)e(in)h(the)g(full)f(v)o(ersion)h(of)f(this)h(pap)q(er)h([10)o (].)340 2178 y Fo(2)56 b(Preliminaries)340 2282 y Fx(F)m(or)18 b(preliminaries)e(on)h(rewriting)h(and)g(termination)e(w)o(e)i(refer)h (to)e([2)o(,)h(3)o(].)f(Let)i Fn(F)i Fx(b)q(e)e(a)340 2332 y(signature)14 b(con)o(taining)e(at)h(least)g(one)h(constan)o(t.)f (W)m(e)g(write)g Fn(T)e Fx(\()p Fn(F)t Fx(\))i(for)g(the)h(set)g(of)e (ground)340 2382 y(terms)k(o)o(v)o(er)g Fn(F)t Fx(;)g(for)g(a)f(set)i Fn(X)22 b Fx(of)16 b(v)n(ariable)f(sym)o(b)q(ols)f(w)o(e)j(write)f Fn(T)10 b Fx(\()p Fn(F)t Fm(;)d Fn(X)f Fx(\))15 b(for)h(the)h(set)g(of) 340 2432 y(op)q(en)i(terms.)e(A)h(\(strict)h(partial\))e(order)i Fm(>)f Fx(on)g Fn(T)10 b Fx(\()p Fn(F)t Fx(\))18 b(is)g(called)g Fl(monotonic)j Fx(if)c(for)h(all)1050 2556 y(2)p eop %%Page: 3 3 3 2 bop 183 194 a Fm(f)18 b Fn(2)c(F)19 b Fx(and)c Fm(t;)7 b(u)13 b Fn(2)g(T)d Fx(\()p Fn(F)t Fm(;)d Fn(X)f Fx(\))15 b(with)g Fm(t)f(>)g(u)h Fx(w)o(e)g(ha)o(v)o(e)g Fm(f)t Fx(\()p Fm(:)7 b(:)g(:)13 b(;)7 b(t;)g(:)g(:)g(:)t Fx(\))14 b Fm(>)g(f)t Fx(\()p Fm(:)7 b(:)g(:)14 b(;)7 b(u;)g(:)g(:)g(:)t Fx(\).)14 b(A)183 244 y(TRS)i Fn(R)g Fx(o)o(v)o(er)h Fn(F)j Fx(and)c(an)g(order)h Fm(>)g Fx(on)f Fn(T)10 b Fx(\()p Fn(F)t Fx(\))17 b(are)g(called)f Fl(c)n(omp)n(atible)j Fx(if)d Fm(t)g(>)g(u)g Fx(for)g(all)183 293 y(rewrite)i(steps)h Fm(t)e Fn(!)509 299 y Fi(R)556 293 y Fm(u)p Fx(.)f(F)m(or)h (compatibilit)o(y)d(with)j(a)g(monotonic)e(order)j(it)f(su\016ces)i(to) 183 343 y(c)o(hec)o(k)e(that)f Fm(l)q(\033)h(>)f(r)q(\033)h Fx(for)f(all)f(rules)i Fm(l)f Fn(!)f Fm(r)i Fx(in)f Fn(R)h Fx(and)f(all)f(ground)h(substitutions)h Fm(\033)q Fx(.)e(It)183 393 y(is)h(w)o(ell-kno)o(wn)f(that)h(a)g(TRS)g(is)g(terminating)e(if)i (and)g(only)f(if)h(it)f(is)h(compatible)f(with)h(a)183 443 y(monotonic)e(w)o(ell-founded)i(order.)g(An)h Fn(F)t Fx(-algebra)f(consists)h(of)f(a)g(set)h Fm(A)g Fx(and)f(for)g(ev)o(ery) 183 493 y Fm(f)g Fn(2)11 b(F)17 b Fx(a)12 b(function)g Fm(f)519 499 y Fv(A)551 493 y Fx(:)h Fm(A)607 478 y Fv(n)641 493 y Fn(!)e Fm(A)p Fx(,)h(where)i Fm(n)e Fx(is)h(the)g(arit)o(y)f(of)f Fm(f)t Fx(.)i(A)g Fl(monotone)j Fn(F)t Fx(-algebra)183 542 y(\()p Fm(A;)7 b(>)p Fx(\))13 b(is)g(an)g Fn(F)t Fx(-algebra)g Fm(A)g Fx(for)g(whic)o(h)g(the)h(underlying)f(set)h(is)f (pro)o(vided)g(with)g(an)g(order)183 592 y Fm(>)h Fx(suc)o(h)i(that)e (ev)o(ery)h(algebra)f(op)q(eration)h(is)f(monotonic)e(in)i(all)g(of)f (its)i(argumen)o(ts.)e(More)183 642 y(precisely)m(,)19 b(for)h(all)e Fm(f)26 b Fn(2)20 b(F)k Fx(and)19 b Fm(a;)7 b(b)21 b Fn(2)f Fm(A)g Fx(with)f Fm(a)i(>)h(b)d Fx(w)o(e)h(ha)o(v)o(e)f Fm(f)1334 648 y Fv(A)1362 642 y Fx(\()p Fm(:)7 b(:)g(:)12 b(;)7 b(a;)g(:)g(:)g(:)t Fx(\))21 b Fm(>)183 692 y(f)203 698 y Fv(A)230 692 y Fx(\()p Fm(:)7 b(:)g(:)12 b(;)7 b(b;)g(:)g(:)g(:)t Fx(\).)19 b(A)h(monotone)d Fn(F)t Fx(-algebra)i(\()p Fm(A;)7 b(>)p Fx(\))19 b(is)g(called)g Fl(wel)r(l-founde)n(d)k Fx(if)18 b Fm(>)i Fx(is)f(a)183 742 y(w)o(ell-founded)14 b(order.)i(Ev)o(ery)g(monotone)e Fn(F)t Fx(-algebra)h(\()p Fm(A;)7 b(>)p Fx(\))15 b(induces)i(an)e (order)h Fm(>)1537 748 y Fv(A)1580 742 y Fx(on)183 791 y(the)i(set)g(of)f(terms)g Fn(T)10 b Fx(\()p Fn(F)t Fm(;)d Fn(X)f Fx(\))17 b(as)h(follo)o(ws:)d Fm(t)j(>)938 797 y Fv(A)983 791 y Fm(u)f Fx(if)g(and)g(only)g(if)f([)p Fm(\013)p Fx(]\()p Fm(t)p Fx(\))h Fm(>)h Fx([)p Fm(\013)p Fx(]\()p Fm(u)p Fx(\))e(for)183 841 y(all)e(assignmen)o(ts)h Fm(\013)5 b Fx(:)14 b Fn(X)20 b(!)14 b Fm(A)p Fx(.)i(Here)h([)p Fm(\013)p Fx(])d(denotes)k(the)e(homomo)o(rphic)e(extension)i(of)f Fm(\013)p Fx(,)183 891 y(i.e.,)g([)p Fm(\013)p Fx(]\()p Fm(x)p Fx(\))h(=)h Fm(\013)p Fx(\()p Fm(x)p Fx(\))f(and)h([)p Fm(\013)p Fx(]\()p Fm(f)t Fx(\()p Fm(t)741 897 y Fw(1)759 891 y Fm(;)7 b(:)g(:)g(:)12 b(;)7 b(t)874 897 y Fv(n)896 891 y Fx(\)\))17 b(=)g Fm(f)1014 897 y Fv(A)1041 891 y Fx(\([)p Fm(\013)p Fx(]\()p Fm(t)1139 897 y Fw(1)1157 891 y Fx(\))p Fm(;)7 b(:)g(:)g(:)12 b(;)7 b Fx([)p Fm(\013)p Fx(]\()p Fm(t)1355 897 y Fv(n)1376 891 y Fx(\)\))17 b(for)g Fm(x)f Fn(2)g(X)6 b Fx(,)183 941 y Fm(f)16 b Fn(2)11 b(F)t Fx(,)i(and)h Fm(t)413 947 y Fw(1)432 941 y Fm(;)7 b(:)g(:)g(:)k(;)c(t)546 947 y Fv(n)580 941 y Fn(2)k(T)f Fx(\()p Fn(F)t Fm(;)d Fn(X)f Fx(\).)13 b(A)h(TRS)f Fn(R)h Fx(and)f(a)h(monotone)e(algebra)h(\()p Fm(A;)7 b(>)p Fx(\))14 b(are)183 991 y(called)i Fl(c)n(omp)n(atible)j Fx(if)c Fn(R)h Fx(and)g Fm(>)716 997 y Fv(A)760 991 y Fx(are)g(compatible.)e(It)j(is)f(w)o(ell-kno)o(wn)f(that)h(a)g(TRS)g (is)183 1041 y(terminating)9 b(if)h(and)h(only)f(if)g(it)h(is)g (compatible)e(with)i(a)g(w)o(ell-founded)f(monotone)f(algebra.)183 1090 y(The)16 b(set)g(of)f(rewrite)h(rules)g Fm(f)t Fx(\()p Fm(x)692 1096 y Fw(1)712 1090 y Fm(;)7 b(:)g(:)g(:)k(;)c(x)835 1096 y Fv(n)857 1090 y Fx(\))15 b Fn(!)e Fm(x)967 1096 y Fv(i)996 1090 y Fx(for)i(all)g Fm(f)j Fn(2)c(F)20 b Fx(and)15 b(all)f Fm(i)h Fx(=)f(1)p Fm(;)7 b(:)g(:)g(:)12 b(;)7 b(n)p Fx(,)183 1140 y(where)14 b Fm(n)d Fn(\025)h Fx(1)g(is)h(the)h(arit)o(y)e(of)g Fm(f)t Fx(,)h(is)g(denoted)h(b)o(y)e Fn(E)m Fl(mb)p Fx(\()p Fn(F)t Fx(\),)h(or)g(simply)d(b)o(y)j Fn(E)m Fl(mb)g Fx(when)g(the)183 1190 y(signature)h Fn(F)k Fx(can)c(b)q(e)g(inferred)h(from)d(the)i(con)o(text.)245 1241 y(The)i(prop)q(erties)g(in)f(the)h(hierarc)o(h)o(y)g(are)g (de\014ned)g(as)g(follo)o(ws.)d(A)i(TRS)g(is)g(called)g Fl(ter-)183 1291 y(minating)20 b Fx(if)15 b(it)h(do)q(es)h(not)f(allo)o (w)f(an)h(in\014nite)g(reduction.)g(A)h(TRS)f Fn(R)g Fx(o)o(v)o(er)g(a)g(signature)183 1341 y Fn(F)21 b Fx(is)c(called)g Fl(simply)g(terminating)k Fx(if)16 b Fn(R)c([)f(E)m Fl(mb)p Fx(\()p Fn(F)t Fx(\))17 b(is)g(terminating,)e(or,)i(equiv)n(alen)o(tly) m(,)183 1390 y Fn(R)9 b([)f(E)m Fl(mb)p Fx(\()p Fn(F)t Fx(\))14 b(has)g(no)f(cycle.)h(A)g(w)o(ell-kno)o(wn)e(su\016cien)o(t)i (condition)f(for)h(simple)e(termina-)183 1440 y(tion)h(of)g (terminating)f(TRSs)i(is)f Fl(length-pr)n(eservingness)p Fx(,)g(whic)o(h)h(means)f(that)h Fn(j)p Fm(l)q(\033)q Fn(j)d Fx(=)g Fn(j)p Fm(r)q(\033)q Fn(j)183 1490 y Fx(for)k(all)f (rules)h Fm(l)h Fn(!)d Fm(r)j Fx(and)f(all)f(ground)h(substitutions)h Fm(\033)q Fx(.)f(Here)i Fn(j)p Fm(t)p Fn(j)d Fx(denotes)i(the)g(n)o(um) o(b)q(er)183 1540 y(of)j(function)h(sym)o(b)q(ols)f(in)h Fm(t)p Fx(.)g(A)h(TRS)f(o)o(v)o(er)g(a)g(signature)h Fn(F)j Fx(is)c(called)g Fl(total)r(ly)h(termi-)183 1590 y(nating)f Fx(if)15 b(it)h(is)g(compatible)e(with)i(a)f(monotonic)f(w)o (ell-founded)i(total)f(order)i(on)f Fn(T)10 b Fx(\()p Fn(F)t Fx(\),)183 1639 y(or,)16 b(equiv)n(alen)o(tly)m(,)e(it)i(is)g (compatible)f(with)h Fm(>)921 1645 y Fv(A)965 1639 y Fx(for)g(some)f(w)o(ell-founded)h(monotone)f Fn(F)t Fx(-)183 1689 y(algebra)d(\()p Fm(A;)7 b(>)p Fx(\))13 b(in)f(whic)o(h)h(the)g (order)h Fm(>)f Fx(is)f(total.)g(A)h(TRS)f(o)o(v)o(er)h(a)f(signature)h Fn(F)k Fx(is)c(called)183 1739 y Fm(!)q Fl(-terminating)19 b Fx(if)c(it)g(is)h(compatible)e(with)h Fm(>)924 1745 y Fv(A)967 1739 y Fx(for)h(some)e(w)o(ell-founded)i(monotone)e Fn(F)t Fx(-)183 1789 y(algebra)i(\()p Fm(A;)7 b(>)p Fx(\))16 b(in)g(whic)o(h)g Fm(A)g Fx(=)g Fh(N)e Fx(and)i Fm(>)h Fx(is)f(the)h(usual)f(order)h(on)f Fh(N)p Fx(.)e(A)j(TRS)e(o)o(v)o(er)i (a)183 1839 y(signature)g Fn(F)j Fx(is)d(called)f Fl(p)n(olynomial)r (ly)h(terminating)j Fx(if)c(it)g(is)h(compatible)e(with)h Fm(>)1530 1845 y Fv(A)1574 1839 y Fx(for)183 1888 y(some)e(w)o (ell-founded)g(monotone)g Fn(F)t Fx(-algebra)h(\()p Fm(A;)7 b(>)p Fx(\))15 b(in)g(whic)o(h)g Fm(A)f Fx(=)g Fh(N)p Fx(,)e Fm(>)k Fx(is)f(the)h(usual)183 1938 y(order)g(on)f Fh(N)e Fx(and)i(for)g(whic)o(h)g(all)f(functions)i Fm(f)924 1944 y Fv(A)966 1938 y Fx(are)g(p)q(olynomials.)c(A)j(TRS)g Fn(R)h Fx(is)f(called)183 1988 y Fl(lo)n(oping)g Fx(if)c(it)g(admits)f (a)i(reduction)g Fm(t)g Fn(!)818 1970 y Fw(+)818 2000 y Fi(R)859 1988 y Fm(C)s Fx([)p Fm(t\033)q Fx(])f(for)g(some)g(term)g Fm(t)p Fx(,)g(some)g(con)o(text)h Fm(C)j Fx(and)183 2038 y(some)10 b(substitution)i Fm(\033)q Fx(.)f(A)h(TRS)f Fn(R)g Fx(is)h(called)f Fl(cyclic)i Fx(if)e(it)g(admits)f(a)h (reduction)h Fm(t)g Fn(!)1506 2020 y Fw(+)1506 2050 y Fi(R)1547 2038 y Fm(t)g Fx(for)183 2088 y(some)g(term)g Fm(t)p Fx(.)g(A)h(TRS)f Fn(R)h Fx(o)o(v)o(er)g(a)f(signature)h Fn(F)k Fx(is)c(called)f Fl(self-emb)n(e)n(dding)k Fx(if)c(it)h(admits)e (a)183 2138 y(reduction)k Fm(t)d Fn(!)437 2120 y Fw(+)437 2150 y Fi(R)479 2138 y Fm(u)g Fn(!)557 2122 y Fi(\003)557 2151 y(E)m Fg(mb)o Fw(\()p Fi(F)s Fw(\))681 2138 y Fm(t)j Fx(for)f(some)f(terms)h Fm(t)p Fx(,)g Fm(u)p Fx(.)f(Recen)o(t)i(in)o(v) o(estigations)e(of)h(these)183 2193 y(notions)f(include)h([5)o(,)g(7,)f (8,)g(14,)g(19)o(].)245 2244 y(F)m(or)h(the)g(pro)q(ofs)h(w)o(e)f(use)h (P)o(ost's)f(Corresp)q(ondence)j(Problem)c(\(PCP\),)i(whic)o(h)f(can)g (b)q(e)183 2294 y(describ)q(ed)h(as)f(follo)o(ws:)253 2382 y(giv)o(en)h(a)h(\014nite)f(alphab)q(et)h Fm(\000)21 b Fx(and)15 b(a)g(\014nite)h(set)g Fm(P)k Fn(\032)15 b Fm(\000)1146 2367 y Fw(+)1183 2382 y Fn(\002)c Fm(\000)1258 2367 y Fw(+)1285 2382 y Fx(,)k(is)g(there)i(some)253 2432 y(natural)j(n)o(um)o(b)q(er)g Fm(n)j(>)g Fx(0)d(and)h(\()p Fm(\013)838 2438 y Fv(i)851 2432 y Fm(;)7 b(\014)893 2438 y Fv(i)907 2432 y Fx(\))23 b Fn(2)f Fm(P)k Fx(for)20 b Fm(i)j Fx(=)g(1)p Fm(;)7 b(:)g(:)g(:)12 b(;)7 b(n)20 b Fx(suc)o(h)h(that)893 2556 y(3)p eop %%Page: 4 4 4 3 bop 411 194 a Fm(\013)438 200 y Fw(1)456 194 y Fm(\013)483 200 y Fw(2)508 194 y Fn(\001)7 b(\001)g(\001)f Fm(\013)591 200 y Fv(n)624 194 y Fx(=)12 b Fm(\014)691 200 y Fw(1)710 194 y Fm(\014)733 200 y Fw(2)759 194 y Fn(\001)7 b(\001)g(\001)f Fm(\014)838 200 y Fv(n)861 194 y Fx(?)340 269 y(This)k(problem)f(is)h (kno)o(wn)f(to)h(b)q(e)g(undecidable)h(ev)o(en)f(in)g(the)g(case)h(of)e (a)h(t)o(w)o(o-letter)g(alphab)q(et)340 319 y(\([16]\).)e(The)i(set)g Fm(P)15 b Fx(is)9 b(called)g(an)h Fl(instanc)n(e)j Fx(of)8 b(PCP)m(,)h(the)h(string)g Fm(\013)1359 325 y Fw(1)1377 319 y Fm(\013)1404 325 y Fw(2)1429 319 y Fn(\001)d(\001)g(\001)e Fm(\013)1511 325 y Fv(n)1545 319 y Fx(=)12 b Fm(\014)1612 325 y Fw(1)1631 319 y Fm(\014)1654 325 y Fw(2)1680 319 y Fn(\001)7 b(\001)g(\001)e Fm(\014)1758 325 y Fv(n)340 368 y Fx(a)14 b Fl(solution)j Fx(for)d Fm(P)6 b Fx(.)12 b(W)m(e)i(use)h(a)e(\014xed)i(t)o(w)o(o-letter)f(alphab)q(et)g Fm(\000)i Fx(=)c Fn(f)p Fx(0)p Fm(;)7 b Fx(1)p Fn(g)p Fx(.)403 418 y(W)m(e)14 b(enco)q(de)j(PCP)e(instances)h Fm(P)k Fx(and,)15 b(for)f(eac)o(h)i(la)o(y)o(er)e Fm(X)j Fn(\))c Fm(Y)24 b Fx(of)15 b(the)g(hierarc)o(h)o(y)m(,)g(a)340 468 y(c)o(haracteristic)g(TRS)d Fn(Q)h Fx(in)o(to)f(a)g(one-rule)i(TRS) e Fn(S)s Fx(\()p Fm(P)q(;)7 b Fn(Q)p Fx(\))12 b(suc)o(h)i(that)f Fn(S)s Fx(\()p Fm(P)q(;)7 b Fn(Q)p Fx(\))12 b(is)h(in)g Fm(Y)22 b Fx(for)340 518 y(all)15 b Fm(P)6 b Fx(,)16 b(and)g(in)g Fm(X)k Fx(if)15 b(and)h(only)g(if)f Fm(P)22 b Fx(has)16 b(no)h(solution.)e(Th)o(us)h(w)o(e)h(reduce)h(PCP)f(to)f (the)340 568 y(relativ)o(e)e(decision)g(problem)f(in)g(eac)o(h)i(la)o (y)o(er.)340 694 y Fo(3)56 b(The)19 b(Enco)r(ding)340 786 y Fx(W)m(e)13 b(are)h(no)o(w)f(going)f(to)h(enco)q(de)h(a)f(PCP)h (instance)g Fm(P)19 b Fx(and)13 b(a)g(TRS)g Fn(Q)g Fx(with)g(the)g (prop)q(ert)o(y)340 836 y(that)h(all)f(left-hand)g(sides)i(coincide)f (in)g(a)f(TRS)h Fn(U)t Fx(\()p Fm(P)q(;)7 b Fn(Q)p Fx(\))13 b(with)h(the)g(same)f(prop)q(ert)o(y)m(.)403 886 y(The)i(signature)g Fn(F)700 892 y Fi(U)741 886 y Fx(w)o(e)g(add)g(for)g(our)g(TRSs)g (consists)h(of)e(constan)o(ts)i(0,)e(1,)g($,)h(and)f Fm(")p Fx(,)340 936 y(binary)i(sym)o(b)q(ols)f Ff(cons)h Fx(and)p 809 912 77 2 v 16 w Ff(cons)q Fx(,)f(and)h(a)g(sym)o(b)q(ol)e Fm(A)j Fx(the)f(arit)o(y)g(of)f(whic)o(h)h(will)f(dep)q(end)340 985 y(on)f(the)h(size)f(of)f(the)i(PCP)f(instance)h Fm(P)6 b Fx(.)403 1035 y(The)18 b(binary)g(sym)o(b)q(ols)f Ff(cons)h Fx(and)p 969 1012 V 18 w Ff(cons)h Fx(as)f(w)o(ell)f(as)i(the)f (constan)o(t)h Fm(")g Fx(build)e(lists)h(of)340 1085 y(terms.)12 b(Usually)f(w)o(e)i(drop)f(the)h Ff(cons)g Fx(and)p 1007 1062 V 12 w Ff(cons)g Fx(sym)o(b)q(ols,)d(and)i(write)h (only)e(the)i(app)q(ended)340 1135 y(terms)j(and)f(barred)h(terms,)f (resp)q(ectiv)o(ely)m(.)h(F)m(ormally)m(,)c(w)o(e)j(de\014ne)i(the)f (notation)f Fm(\020)s Fx(\()p Fm(t)p Fx(\))h(for)340 1185 y(an)o(y)d(term)f Fm(t)g Fx(and)g(mixed)g(sequence)i Fm(\020)h Fn(2)c(f)p Fm(t;)p 1042 1154 15 2 v 7 w(t)g Fn(j)g Fm(t)h Fn(2)f(T)f Fx(\()p Fn(F)t Fm(;)d Fn(X)f Fx(\))o Fn(g)1331 1170 y Fi(\003)1363 1185 y Fx(of)12 b(barred)h(and)g(un)o(barred)340 1234 y(terms)h(as)g(follo)o(ws:)411 1324 y Fm(\020)s Fx(\()p Fm(t)p Fx(\))54 b(=)f Fm(t)274 b Fx(if)13 b Fm(\020)i Fx(=)d Fm(";)411 1387 y(\020)s Fx(\()p Fm(t)p Fx(\))54 b(=)f Ff(cons)p Fx(\()p Fm(t)725 1369 y Fi(0)737 1387 y Fm(;)7 b(\020)777 1369 y Fi(0)788 1387 y Fx(\()p Fm(t)p Fx(\)\))56 b(if)13 b Fm(\020)i Fx(=)d Fm(t)1037 1369 y Fi(0)1049 1387 y Fm(\020)1070 1369 y Fi(0)1081 1387 y Fm(;)411 1455 y(\020)s Fx(\()p Fm(t)p Fx(\))54 b(=)p 618 1431 77 2 v 53 w Ff(cons)p Fx(\()p Fm(t)725 1437 y Fi(0)737 1455 y Fm(;)7 b(\020)777 1437 y Fi(0)788 1455 y Fx(\()p Fm(t)p Fx(\)\))56 b(if)13 b Fm(\020)i Fx(=)p 1022 1421 27 2 v 12 w Fm(t)1037 1443 y Fi(0)1049 1455 y Fm(\020)1070 1437 y Fi(0)1081 1455 y Fm(:)340 1532 y Fx(Moreo)o(v)o(er,)g(with)f(an)o(y)g(sequence)i Fm(\013)c Fx(=)h Fm(t)980 1538 y Fw(1)998 1532 y Fm(t)1013 1538 y Fw(2)1039 1532 y Fm(:)7 b(:)g(:)e(t)1109 1538 y Fv(n)1146 1532 y Fx(of)14 b(un)o(barred)h(terms)f(w)o(e)h(asso)q (ciate)g(the)340 1582 y(sequence)p 512 1559 V 16 w Fm(\013)d Fx(=)p 594 1551 38 2 v 11 w Fm(t)609 1588 y Fv(n)639 1582 y Fm(:)7 b(:)g(:)p 694 1551 34 2 v 5 w(t)709 1588 y Fw(2)p 739 1551 V 739 1582 a Fm(t)754 1588 y Fw(1)787 1582 y Fx(of)13 b(barred)i(terms.)e(Hence)411 1659 y Fm(\013)p Fx(\()p Fm(t)p Fx(\))53 b(=)g Ff(cons)q Fx(\()p Fm(t)731 1665 y Fw(1)750 1659 y Fm(;)7 b Ff(cons)p Fx(\()p Fm(t)876 1665 y Fw(2)894 1659 y Fm(;)g(:)g(:)g(:)e Ff(cons)q Fx(\()p Fm(t)1076 1665 y Fv(n)1098 1659 y Fm(;)i(t)p Fx(\))g Fm(:)g(:)g(:)e Fx(\))p Fm(;)p 411 1699 27 2 v 411 1721 a(\013)p Fx(\()p Fm(t)p Fx(\))53 b(=)p 623 1698 77 2 v 53 w Ff(cons)q Fx(\()p Fm(t)731 1727 y Fv(n)754 1721 y Fm(;)p 773 1698 V 7 w Ff(cons)p Fx(\()p Fm(t)880 1727 y Fv(n)p Fi(\000)p Fw(1)945 1721 y Fm(;)7 b(:)g(:)g(:)p 1019 1698 V 5 w Ff(cons)p Fx(\()p Fm(t)1126 1727 y Fw(1)1145 1721 y Fm(;)g(t)p Fx(\))g Fm(:)g(:)g(:)e Fx(\))p Fm(:)340 1799 y Fx(In)23 b(order)g(to)f(a)o(v)o(oid)f(confusion,)h(w)o(e)h(will) e(use)i(the)g(latter)g(abbreviation)e(only)h(when)340 1849 y(the)f(app)q(ended)g(terms)e(are)h(in)g(the)g(set)h Fn(f)p Fx(0)p Fm(;)7 b Fx(1)p Fm(;)g Fx($)p Fn(g)k([)h(X)6 b Fx(.)19 b(F)m(or)h(instance,)g(0)p 1553 1817 21 2 v(0)o($\()p Fm(")p Fx(\))h(stands)340 1898 y(for)15 b Ff(cons)p Fx(\(0)p Fm(;)p 537 1875 77 2 v 7 w Ff(cons)p Fx(\(0\))p Fm(;)7 b Ff(cons)p Fx(\($)p Fm(;)g(")p Fx(\)\)\),)p 911 1876 24 2 v 15 w Fm(x)o(y)q Fx(1\()p Fm(")p Fx(\))16 b(for)p 1108 1875 77 2 v 15 w Ff(cons)p Fx(\()p Fm(x;)7 b Ff(cons)p Fx(\()p Fm(y)q(;)g Ff(cons)q Fx(\(1)p Fm(;)g(")p Fx(\)\)\),)p 1601 1867 42 2 v 14 w(010\()p Fm(z)r Fx(\))15 b(for)p 340 1925 77 2 v 340 1948 a Ff(cons)q Fx(\(1)p Fm(;)p 473 1925 V 7 w Ff(cons)p Fx(\(0)p Fm(;)7 b Ff(cons)p Fx(\(0)p Fm(;)g(z)r Fx(\)\)\),)12 b(and)g Fm(z)r Fx(\()p Fm(x)p Fx(\))h(for)g Ff(cons)p Fx(\()p Fm(z)r(;)7 b(x)p Fx(\).)12 b(Note)h(that)p 1446 1916 42 2 v 13 w(010\()p Fm(z)r Fx(\))f(di\013ers)i(from)p 340 1966 21 2 v 340 1998 a(0)p 373 1966 V 12 w(1)o(0\()p Fm(z)r Fx(\))e(=)p 523 1975 77 2 v 12 w Ff(cons)q Fx(\(0)p Fm(;)p 656 1975 V 7 w Ff(cons)o Fx(\(1)p Fm(;)7 b Ff(cons)p Fx(\(0)p Fm(;)g(z)r Fx(\)\)\).)403 2048 y(Before)13 b(w)o(e)g(giv)o(e)f(the)h (tec)o(hnical)g(de\014nition)f(of)g Fn(U)t Fx(\()p Fm(P)q(;)7 b Fn(Q)p Fx(\))12 b(let)h(us)g(explain)f(the)h(in)o(tuition)340 2098 y(b)q(ehind)k(its)g(arc)o(hitecture.)h(The)f(system)f Fn(U)t Fx(\()p Fm(P)q(;)7 b Fn(Q)p Fx(\))16 b(is)h(a)f(mo)q (di\014cation)f(of)h(the)h(follo)o(wing)340 2147 y(system)d(from)e([18) o(]:)411 2251 y Fn(S)s Fx(\()p Fm(P)6 b Fx(\))11 b(=)559 2192 y Fe(\032)611 2224 y Fm(F)6 b Fx(\()p Fm(x;)p 703 2202 22 2 v 7 w(a)o Fx(\()p Fm(y)q Fx(\))p Fm(;)h(x;)p 839 2202 V 7 w(a)p Fx(\()p Fm(y)q Fx(\)\))12 b Fn(!)g Fm(F)6 b Fx(\()p Fm(a)p Fx(\()p Fm(x)p Fx(\))p Fm(;)h(y)q(;)g(a)p Fx(\()p Fm(x)p Fx(\))p Fm(;)g(y)q Fx(\))40 b(for)13 b(all)g Fm(a)e Fn(2)g Fm(\000)6 b Fx(,)596 2277 y Fm(F)g Fx(\()p Fm(\013)p Fx(\()p Fm(x)p Fx(\))p Fm(;)h(y)q(;)g(\014)r Fx(\()p Fm(z)r Fx(\))p Fm(;)g(w)q Fx(\))k Fn(!)h Fm(F)6 b Fx(\()p Fm(x;)p 1088 2254 27 2 v 7 w(\013)n Fx(\()p Fm(y)q Fx(\))p Fm(;)h(z)r(;)p 1225 2243 26 2 v 7 w(\014)s Fx(\()p Fm(w)q Fx(\)\))26 b(for)13 b(all)g(\()p Fm(\013;)7 b(\014)r Fx(\))k Fn(2)h Fm(P)6 b Fx(.)340 2354 y(The)15 b(system)e Fn(S)s Fx(\()p Fm(P)6 b Fx(\))14 b(admits)e(a)i(reduction) 411 2432 y Fm(F)6 b Fx(\()p Fm(\015)r Fx(\()p Fm(x)p Fx(\))p Fm(;)h(y)q(;)g(\015)r Fx(\()p Fm(x)p Fx(\))p Fm(;)g(y)q Fx(\))13 b Fn(!)788 2415 y Fw(+)826 2432 y Fm(F)6 b Fx(\()p Fm(\015)r Fx(\()p Fm(x)p Fx(\))p Fm(;)h(y)q(;)g(\015)r Fx(\()p Fm(x)p Fx(\))p Fm(;)g(y)q Fx(\))580 b(\(1\))1050 2556 y(4)p eop %%Page: 5 5 5 4 bop 183 194 a Fx(if)11 b(and)i(only)f(if)g Fm(\015)j Fx(is)d(a)h(solution)f(of)g(the)h(PCP)g Fm(P)6 b Fx(.)11 b(If)i Fm(P)18 b Fx(has)12 b(no)h(solution)f(then)h Fn(S)s Fx(\()p Fm(P)6 b Fx(\))12 b(is)h(to-)183 244 y(tally)e(terminating.)f (The)j(use)g(of)e(barred)i(sym)o(b)q(ols)e(in)h(the)h(second)g(and)f (fourth)h(argumen)o(t)183 293 y(is)g(essen)o(tial)i(for)e(total)g (termination.)245 344 y(It)j(is)g(no)o(w)f(straigh)o(tforw)o(ard)g(to)h (c)o(hange)g(the)h(cyclic)f(b)q(eha)o(viour)f(\(1\))h(to)g(an)o(y)f (desired)183 394 y(b)q(eha)o(viour)k(that)h(can)g(b)q(e)g(expressed)i (b)o(y)e(some)f(rewrite)h(system)g Fn(Q)p Fx(.)f(T)m(o)g(this)h(end)g (an)183 444 y(argumen)o(t)15 b(is)i(added)h(to)e Fm(F)6 b Fx(.)16 b(This)h(last)g(argumen)o(t)f(is)g(left)h(unc)o(hanged,)g (except)h(for)f(the)183 493 y(step)e(completing)d(the)i(cycle)h(in)e (whic)o(h)h(it)g(is)f(rewritten)i(b)o(y)f(a)g(rule)g(in)f Fn(Q)p Fx(.)245 544 y(T)m(o)20 b(a)o(v)o(oid)g(unin)o(tended)i(rewrite) h(steps,)f(w)o(e)g(re\014ne)g(con)o(trol:)f(w)o(e)g(distinguish)g(t)o (w)o(o)183 594 y(states,)15 b(exhibited)g(b)o(y)g(function)g(sym)o(b)q (ols)e Fm(G)h Fx(and)h Fm(H)s Fx(,)f(whic)o(h)h(enable)g(only)f(steps)j (of)d(the)183 644 y(\014rst)g(and)f(second)h(shap)q(e,)g(resp)q(ectiv)o (ely)m(,)g(in)f Fn(S)s Fx(\()p Fm(P)6 b Fx(\).)13 b(A)g(c)o(hange)h (from)d(state)j Fm(G)f Fx(to)h(state)g Fm(H)183 693 y Fx(is)i(p)q(ossible)i(only)e(if)g(the)h(second)h(and)f(the)g(fourth)g (argumen)o(t)f(equals)h Fm(")p Fx(.)f(Vice)i(v)o(ersa,)f(a)183 743 y(c)o(hange)e(of)g(state)i(from)c Fm(H)19 b Fx(to)c Fm(G)g Fx(requires)i(that)e(the)h(\014rst)h(and)e(third)g(fourth)h (argumen)o(t)183 793 y(equals)e Fm(")p Fx(.)f(This)h(giv)o(es)g(the)g (rewrite)h(system)f(consisting)g(of)f(the)h(rule)253 883 y Fm(G)p Fx(\()p Fm(x;)7 b(";)g(z)r(;)g(";)g Ff(LHS)o Fx(\))12 b Fn(!)f Fm(H)s Fx(\()p Fm(x;)c(";)g(z)r(;)g(";)g Ff(LHS)o Fx(\))p Fm(;)642 b Fx(\(2\))183 974 y(the)14 b(rules)253 1064 y Fm(H)s Fx(\()p Fm(\013)p Fx(\()p Fm(x)p Fx(\))p Fm(;)7 b(y)q(;)g(\014)r Fx(\()p Fm(z)r Fx(\))p Fm(;)g(w)q(;)g Ff(LHS)p Fx(\))12 b Fn(!)f Fm(H)s Fx(\()p Fm(x;)p 848 1041 27 2 v 7 w(\013)o Fx(\()p Fm(y)q Fx(\))p Fm(;)c(z)r(;)p 986 1030 26 2 v 7 w(\014)s Fx(\()p Fm(w)q Fx(\))p Fm(;)g Ff(LHS)p Fx(\))387 b(\(3\))183 1154 y(for)13 b(eac)o(h)i(\()p Fm(\013;)7 b(\014)r Fx(\))k Fn(2)g Fm(P)6 b Fx(,)13 b(and)h(the)g(rules)254 1244 y Fm(H)s Fx(\()p Fm(";)p 346 1222 22 2 v 7 w(a)p Fx(\()p Fm(y)q Fx(\))p Fm(;)7 b(";)p 478 1222 V 7 w(a)p Fx(\()p Fm(w)q Fx(\))p Fm(;)g Ff(LHS)q Fx(\))k Fn(!)g Fm(G)p Fx(\()p Fm(a)p Fx(\()p Fm(")p Fx(\))p Fm(;)c(y)q(;)g(a)p Fx(\()p Fm(")p Fx(\))p Fm(;)g(w)q(;)g Ff(RHS)1139 1250 y Fv(j)1157 1244 y Fx(\))398 b(\(4\))253 1307 y Fm(G)p Fx(\()p Fm(x;)p 345 1284 V 7 w(a)o Fx(\()p Fm(y)q Fx(\))p Fm(;)7 b(z)r(;)p 478 1284 V 7 w(a)p Fx(\()p Fm(w)q Fx(\))p Fm(;)g Ff(LHS)q Fx(\))k Fn(!)g Fm(G)p Fx(\()p Fm(a)p Fx(\()p Fm(x)p Fx(\))p Fm(;)c(y)q(;)g(a)p Fx(\()p Fm(z)r Fx(\))p Fm(;)g(w)q(;)g Ff(LHS)p Fx(\))414 b(\(5\))183 1397 y(for)13 b(eac)o(h)i Fm(a)c Fn(2)g Fm(\000)19 b Fx(and)14 b(eac)o(h)h(rule)f(\()p Ff(LHS)e Fn(!)f Ff(RHS)950 1403 y Fv(j)967 1397 y Fx(\))h Fn(2)f(Q)p Fx(.)245 1448 y(In)k(view)f(of)g(the)i(one-rule)f (construction,)g(\014nally)m(,)e(there)j(is)f(the)g(need)h(to)e(ha)o(v) o(e)h(equal)183 1497 y(left-hand)d(sides.)i(F)m(or)e(this)i(reason)f Fn(Q)g Fx(has)h(to)f(ha)o(v)o(e)g(this)g(prop)q(ert)o(y)m(,)g(to)q(o.)f (The)i(t)o(w)o(o)e(states)183 1547 y Fm(G)17 b Fx(and)g Fm(H)j Fx(in)d(the)h(previous)f(de\014nition)g(are)h(enco)q(ded)h(b)o (y)e(argumen)o(t)f(pairs)h(\(0)p Fm(;)7 b Fx(1\))17 b(and)183 1597 y(\(1)p Fm(;)7 b Fx(0\),)15 b(resp)q(ectiv)o(ely)m(,)i(hence)h (one)f(function)g(sym)o(b)q(ol,)d Fm(A)p Fx(,)i(can)h(replace)h(b)q (oth)e Fm(G)h Fx(and)f Fm(H)s Fx(.)183 1647 y(Finally)m(,)9 b(the)k(end)f(of)g(a)f(sequence)j(ma)o(y)c(not)i(b)q(e)h Fm(")f Fx(b)q(ecause)i(sequences)h(of)c(v)n(arious)g(lengths)183 1697 y(ha)o(v)o(e)i(to)h(matc)o(h.)e(Instead)j(the)f(end)h(is)f(mark)o (ed)e(b)o(y)i(a)g(sp)q(ecial)g(sym)o(b)q(ol,)d($.)245 1747 y(In)i(this)g(w)o(a)o(y)m(,)f(one)i(gets)g(four)f(left-hand)f (sides)i(whic)o(h)f(can)h(b)q(e)g(regarded)g(as)f(instances)183 1797 y(of)i(one)h(pattern.)g(The)g(matc)o(h)f(to)h(the)g(pattern)h(can) f(b)q(e)g(dela)o(y)o(ed)g(b)o(y)f(the)i(same)e(tric)o(k)g(as)183 1847 y(in)g(Lescanne)i([12)o(]:)e(One)h(extends)i(the)e(argumen)o(t)f (v)o(ector)h(\(to)g(the)g(left\))g(b)o(y)f(a)h(v)o(ector)g(of)183 1897 y(terms)d(to)h(matc)o(h,)e(and)i(exc)o(hanges)h(v)n(ariables)e (with)h(the)g(terms)g(they)g(should)g(matc)o(h.)183 1992 y Fd(De\014niti)o(on)5 b(1.)20 b Fx(Let)14 b Fm(P)j Fx(=)12 b Fn(f)p Fx(\()p Fm(\013)681 1998 y Fw(1)699 1992 y Fm(;)7 b(\014)741 1998 y Fw(1)759 1992 y Fx(\))p Fm(;)g(:)g(:)g(:)e(;)i Fx(\()p Fm(\013)911 1998 y Fv(n)933 1992 y Fm(;)g(\014)975 1998 y Fv(n)998 1992 y Fx(\))p Fn(g)k(\022)h Fm(\000)1122 1977 y Fw(+)1156 1992 y Fn(\002)c Fm(\000)1228 1977 y Fw(+)1268 1992 y Fx(b)q(e)14 b(a)f(PCP)g(instance)1604 1977 y Fw(5)183 2042 y Fx(and)18 b(let)g Fm(\026)h Fx(=)g(max)n Fn(fj)p Fm(\013)p Fn(j)p Fm(;)7 b Fn(j)p Fm(\014)r Fn(j)17 b(j)h Fx(\()p Fm(\013;)7 b(\014)r Fx(\))19 b Fn(2)f Fm(P)6 b Fn(g)p Fx(.)17 b(Let)i Fm(Q)f Fx(=)h Fn(f)p Ff(LHS)h Fn(!)e Ff(RHS)1377 2048 y Fw(1)1396 2042 y Fm(;)7 b(:)g(:)g(:)e(;)i Ff(LHS)19 b Fn(!)183 2092 y Ff(RHS)262 2098 y Fv(m)293 2092 y Fn(g)12 b Fx(b)q(e)g(a)g(TRS)f(o)o(v)o(er)h(a)f(signature)h Fn(F)835 2098 y Fi(Q)876 2092 y Fx(disjoin)o(t)e(from)g Fn(F)1147 2098 y Fi(U)1173 2092 y Fx(.)h(W)m(e)h(assign)f(to)h Fm(P)17 b Fx(and)11 b Fn(Q)h Fx(a)183 2142 y(TRS)g Fn(U)t Fx(\()p Fm(P)q(;)7 b Fn(Q)p Fx(\))13 b(o)o(v)o(er)g(the)h(signature)g Fn(F)804 2148 y Fi(U)837 2142 y Fn([)8 b(F)903 2148 y Fi(Q)945 2142 y Fx(where)14 b Fm(A)g Fx(has)f(arit)o(y)f(2)p Fm(n)c Fx(+)g(15.)k(It)i(consists)183 2192 y(of)f(the)h(rules)h Fm(l)e Fn(!)e Fm(r)498 2198 y Fv(i)511 2192 y Fx(,)j(1)d Fn(\024)h Fm(i)g Fn(\024)f Fm(n)f Fx(+)f(2)p Fm(m)g Fx(+)h(3,)j(where)i Fm(l)g Fx(and)f Fm(r)1159 2198 y Fv(i)1186 2192 y Fx(are)h(de\014ned)g (as)f(follo)o(ws:)253 2282 y Fm(l)f Fx(=)f Fm(A)p Fx(\(0)p Fm(;)7 b Fx(1)p Fm(;)g Fx(0)p Fm(;)g Fx(1)p Fm(;)g Fx($)p Fm(;)f(\013)595 2288 y Fw(1)610 2282 y Fx(\()p Fm(")p Fx(\))p Fm(;)h(:)g(:)g(:)f(;)h(\013)782 2288 y Fv(n)803 2282 y Fx(\()p Fm(")p Fx(\))p Fm(;)g Fx(0)p Fm(;)g Fx(1)p Fm(;)g Fx($)p Fm(;)g(\014)1016 2288 y Fw(1)1033 2282 y Fx(\()p Fm(")p Fx(\))p Fm(;)g(:)g(:)g(:)f(;)h(\014)1201 2288 y Fv(n)1223 2282 y Fx(\()p Fm(")p Fx(\))p Fm(;)361 2344 y(u;)g(v)q(;)g(w)474 2350 y Fw(1)499 2344 y Fm(:)g(:)g(:)e(w)584 2350 y Fv(\026)606 2344 y Fx(\()p Fm(w)q Fx(\))p Fm(;)p 688 2321 43 2 v 7 w(x)712 2350 y Fw(1)730 2344 y Fx(\()p Fm(x)p Fx(\))p Fm(;)i(y)825 2350 y Fw(1)850 2344 y Fm(:)g(:)g(:)e(y)925 2350 y Fv(\026)948 2344 y Fx(\()p Fm(y)q Fx(\))p Fm(;)p 1020 2321 38 2 v 7 w(z)1039 2350 y Fw(1)1059 2344 y Fx(\()p Fm(z)r Fx(\))p Fm(;)i Ff(LHS)p Fx(\))p Fm(;)p 183 2389 237 2 v 191 2416 a Fu(5)221 2432 y Ft(Presen)o(ting)13 b(PCP)e(instances)i(as)e(ordered)h(lists)h(instead)f(of)f(sets)g(en)o (tails)i(no)f(loss)g(of)f(generalit)o(y)m(.)893 2556 y Fx(5)p eop %%Page: 6 6 6 5 bop 411 194 a Fm(r)430 200 y Fw(1)460 194 y Fx(=)12 b Fm(A)p Fx(\()p Fm(u;)7 b(v)q(;)g Fx(0)p Fm(;)g Fx(1)p Fm(;)g(x)738 200 y Fw(1)754 194 y Fm(;)g(\013)800 200 y Fw(1)818 194 y Fx(\()p Fm(")p Fx(\))p Fm(;)g(:)g(:)g(:)e(;)i(\013)989 200 y Fv(n)1011 194 y Fx(\()p Fm(")p Fx(\))p Fm(;)g Fx(0)p Fm(;)g Fx(1)p Fm(;)g(z)1180 200 y Fw(1)1197 194 y Fm(;)g(\014)1239 200 y Fw(1)1258 194 y Fx(\()p Fm(")p Fx(\))p Fm(;)g(:)g(:)g(:)e(;)i (\014)1425 200 y Fv(n)1448 194 y Fx(\()p Fm(")p Fx(\))p Fm(;)217 b Fx(\(2\))543 265 y(1)p Fm(;)7 b Fx(0)p Fm(;)g(w)653 271 y Fw(1)677 265 y Fm(:)g(:)g(:)e(w)762 271 y Fv(\026)784 265 y Fx(\()p Fm(w)q Fx(\))p Fm(;)p 866 229 21 2 v 7 w Fx($)o(\()p Fm(x)p Fx(\))p Fm(;)i(y)981 271 y Fw(1)1007 265 y Fm(:)g(:)g(:)e(y)1082 271 y Fv(\026)1104 265 y Fx(\()p Fm(y)q Fx(\))p Fm(;)p 1176 229 V 7 w Fx($)q(\()p Fm(z)r Fx(\))p Fm(;)i Ff(LHS)q Fx(\))p Fm(;)411 365 y(r)430 371 y Fv(i)p Fw(+1)497 365 y Fx(=)12 b Fm(A)p Fx(\()p Fm(v)q(;)7 b(u;)g Fx(0)p Fm(;)g Fx(1)p Fm(;)g Fx($)p Fm(;)g(\013)818 371 y Fw(1)833 365 y Fx(\()p Fm(")p Fx(\))p Fm(;)g(:)g(:)g(:)f(;)h(\013)1005 371 y Fv(i)p Fi(\000)p Fw(1)1060 365 y Fx(\()p Fm(")p Fx(\))p Fm(;)g(w)1160 371 y Fw(1)1185 365 y Fm(:)g(:)g(:)f(w)1271 372 y Fi(j)p Fv(\013)1303 376 y Fc(i)1315 372 y Fi(j)1327 365 y Fx(\()p Fm(")p Fx(\))p Fm(;)h(\013)1424 371 y Fv(i)p Fw(+1)1479 365 y Fx(\()p Fm(")p Fx(\))p Fm(;)g(:)g(:)g(:)f(;)h(\013)1651 371 y Fv(n)1672 365 y Fx(\()p Fm(")p Fx(\))p Fm(;)580 427 y Fx(0)p Fm(;)g Fx(1)p Fm(;)g Fx($)p Fm(;)g(\014)723 433 y Fw(1)740 427 y Fx(\()p Fm(")p Fx(\))p Fm(;)g(:)g(:)g(:)e(;)i (\014)907 433 y Fv(i)p Fi(\000)p Fw(1)963 427 y Fx(\()p Fm(")p Fx(\))p Fm(;)g(y)1053 433 y Fw(1)1079 427 y Fm(:)g(:)g(:)f(y) 1155 434 y Fi(j)p Fv(\014)1184 438 y Fc(i)1197 434 y Fi(j)1209 427 y Fx(\()p Fm(")p Fx(\))p Fm(;)h(\014)1302 433 y Fv(i)p Fw(+1)1358 427 y Fx(\()p Fm(")p Fx(\))p Fm(;)g(:)g(:)g(:)f(;)h(\014)1526 433 y Fv(n)1548 427 y Fx(\()p Fm(")p Fx(\))p Fm(;)117 b Fx(\(3\))580 496 y(1)p Fm(;)7 b Fx(0)p Fm(;)g(w)690 503 y Fi(j)p Fv(\013)722 507 y Fc(i)733 503 y Fi(j)p Fw(+1)794 496 y Fm(:)g(:)g(:)e(w)879 502 y Fv(\026)901 496 y Fx(\()p Fm(w)q Fx(\))p Fm(;)p 983 473 41 2 v 7 w(\013)1010 502 y Fv(i)p 1034 473 43 2 v 1034 496 a Fm(x)1058 502 y Fw(1)1077 496 y Fx(\()p Fm(x)p Fx(\))p Fm(;)i(y)1172 503 y Fi(j)p Fv(\014)1201 507 y Fc(i)1213 503 y Fi(j)p Fw(+1)1274 496 y Fm(:)g(:)g(:)f(y)1350 502 y Fv(\026)1372 496 y Fx(\()p Fm(y)q Fx(\))p Fm(;)p 1444 462 38 2 v 7 w(\014)1467 502 y Fv(i)p 1482 473 V 1482 496 a Fm(z)1501 502 y Fw(1)1520 496 y Fx(\()p Fm(z)r Fx(\))p Fm(;)h Ff(LHS)q Fx(\))340 571 y(for)14 b(all)f(1)e Fn(\024)h Fm(i)g Fn(\024)f Fm(n)p Fx(,)1728 646 y(\(4\))-1315 b Fm(r)485 652 y Fv(n)p Fw(+1+)p Fv(j)602 646 y Fx(=)11 b Fm(A)p Fx(\()p Fm(v)q(;)c(u;)g(x)799 652 y Fw(1)817 646 y Fm(;)g Fx(1)p Fm(;)g(w)906 652 y Fw(1)923 646 y Fm(;)g(\013)969 652 y Fw(1)987 646 y Fx(\()p Fm(")p Fx(\))p Fm(;)g(:)g(:)g(:)e(;)i(\013)1158 652 y Fv(n)1180 646 y Fx(\()p Fm(")p Fx(\))p Fm(;)g(z)1269 652 y Fw(1)1288 646 y Fm(;)g Fx(1)p Fm(;)g(y)1367 652 y Fw(1)1385 646 y Fm(;)g(\014)1427 652 y Fw(1)1445 646 y Fx(\()p Fm(")p Fx(\))p Fm(;)g(:)g(:)g(:)f(;)h(\014)1613 652 y Fv(n)1635 646 y Fx(\()p Fm(")p Fx(\))p Fm(;)685 708 y Fx(0)p Fm(;)g Fx(1)p Fm(;)g Fx(0$)p Fm(w)837 714 y Fw(2)860 708 y Fm(:)g(:)g(:)e(w) 945 714 y Fv(\026)967 708 y Fx(\()p Fm(w)q Fx(\))p Fm(;)i(x;)g Fx(0$)p Fm(y)1154 714 y Fw(2)1178 708 y Fm(:)g(:)g(:)f(y)1254 714 y Fv(\026)1276 708 y Fx(\()p Fm(y)q Fx(\))p Fm(;)h(z)r(;)g Ff(RHS)1468 714 y Fv(j)1485 708 y Fx(\))411 771 y Fm(r)430 777 y Fv(n)p Fw(+1+)p Fv(m)p Fw(+)p Fv(j)602 771 y Fx(=)k Fm(A)p Fx(\()p Fm(v)q(;)c(u;)g Fx(0)p Fm(;)g(x)839 777 y Fw(1)857 771 y Fm(;)g(w)906 777 y Fw(1)923 771 y Fm(;)g(\013)969 777 y Fw(1)987 771 y Fx(\()p Fm(")p Fx(\))p Fm(;)g(:)g(:)g(:)e(;)i (\013)1158 777 y Fv(n)1180 771 y Fx(\()p Fm(")p Fx(\))p Fm(;)g Fx(0)p Fm(;)g(z)1309 777 y Fw(1)1327 771 y Fm(;)g(y)1366 777 y Fw(1)1385 771 y Fm(;)g(\014)1427 777 y Fw(1)1445 771 y Fx(\()p Fm(")p Fx(\))p Fm(;)g(:)g(:)g(:)f(;)h(\014)1613 777 y Fv(n)1635 771 y Fx(\()p Fm(")p Fx(\))p Fm(;)685 833 y Fx(0)p Fm(;)g Fx(1)p Fm(;)g Fx(1$)p Fm(w)837 839 y Fw(2)860 833 y Fm(:)g(:)g(:)e(w)945 839 y Fv(\026)967 833 y Fx(\()p Fm(w)q Fx(\))p Fm(;)i(x;)g Fx(1$)p Fm(y)1154 839 y Fw(2)1178 833 y Fm(:)g(:)g(:)f(y)1254 839 y Fv(\026)1276 833 y Fx(\()p Fm(y)q Fx(\))p Fm(;)h(z)r(;)g Ff(RHS)1468 839 y Fv(j)1485 833 y Fx(\))340 908 y(for)14 b(all)f(1)e Fn(\024)h Fm(j)i Fn(\024)e Fm(m)p Fx(,)h(and)h(\014nally)1728 983 y(\(5\))-1370 b Fm(r)430 989 y Fv(n)p Fw(+2)p Fv(m)p Fw(+2)577 983 y Fx(=)12 b Fm(A)p Fx(\()p Fm(u;)7 b(v)q(;)g(x)775 989 y Fw(1)793 983 y Fm(;)g Fx(1)p Fm(;)g Fx($)p Fm(;)g(\013)919 989 y Fw(1)935 983 y Fx(\()p Fm(")p Fx(\))p Fm(;)g(:)g(:)g(:)f(;)h (\013)1107 989 y Fv(n)1128 983 y Fx(\()p Fm(")p Fx(\))p Fm(;)g(z)1217 989 y Fw(1)1236 983 y Fm(;)g Fx(1)p Fm(;)g Fx($)p Fm(;)g(\014)1358 989 y Fw(1)1375 983 y Fx(\()p Fm(")p Fx(\))p Fm(;)g(:)g(:)g(:)f(;)h(\014)1543 989 y Fv(n)1565 983 y Fx(\()p Fm(")p Fx(\))p Fm(;)660 1045 y Fx(0)p Fm(;)g Fx(1)p Fm(;)g Fx(0)p Fm(w)791 1051 y Fw(1)815 1045 y Fm(:)g(:)g(:)e(w)900 1051 y Fv(\026)922 1045 y Fx(\()p Fm(w)q Fx(\))p Fm(;)i(x;)g Fx(0)p Fm(y)1088 1051 y Fw(1)1112 1045 y Fm(:)g(:)g(:)f(y)1188 1051 y Fv(\026)1210 1045 y Fx(\()p Fm(y)q Fx(\))p Fm(;)h(z)r(;)g Ff(LHS)r Fx(\))411 1107 y Fm(r)430 1113 y Fv(n)p Fw(+2)p Fv(m)p Fw(+3)577 1107 y Fx(=)12 b Fm(A)p Fx(\()p Fm(u;)7 b(v)q(;)g Fx(0)p Fm(;)g(x)815 1113 y Fw(1)832 1107 y Fm(;)g Fx($)p Fm(;)g(\013)918 1113 y Fw(1)935 1107 y Fx(\()p Fm(")p Fx(\))p Fm(;)g(:)g(:)g(:)f(;)h(\013)1107 1113 y Fv(n)1128 1107 y Fx(\()p Fm(")p Fx(\))p Fm(;)g Fx(0)p Fm(;)g(z)1257 1113 y Fw(1)1275 1107 y Fm(;)g Fx($)p Fm(;)g(\014)1357 1113 y Fw(1)1375 1107 y Fx(\()p Fm(")p Fx(\))p Fm(;)g(:)g(:)g(:)f(;)h(\014)1543 1113 y Fv(n)1565 1107 y Fx(\()p Fm(")p Fx(\))p Fm(;)660 1170 y Fx(0)p Fm(;)g Fx(1)p Fm(;)g Fx(1)p Fm(w)791 1176 y Fw(1)815 1170 y Fm(:)g(:)g(:)e(w)900 1176 y Fv(\026)922 1170 y Fx(\()p Fm(w)q Fx(\))p Fm(;)i(x;)g Fx(1)p Fm(y)1088 1176 y Fw(1)1112 1170 y Fm(:)g(:)g(:)f(y)1188 1176 y Fv(\026)1210 1170 y Fx(\()p Fm(y)q Fx(\))p Fm(;)h(z)r(;)g Ff(LHS)r Fx(\))p Fm(:)340 1245 y Fx(In)20 b(the)h(follo)o(wing)c(w)o(e)j(denote) h(0)p Fm(;)7 b Fx(1)p Fm(;)g Fx(0)p Fm(;)g Fx(1)p Fm(;)g Fx($)p Fm(;)f(\013)1090 1251 y Fw(1)1105 1245 y Fx(\()p Fm(")p Fx(\))p Fm(;)h(:)g(:)g(:)f(;)h(\013)1277 1251 y Fv(n)1298 1245 y Fx(\()p Fm(")p Fx(\))p Fm(;)g Fx(0)p Fm(;)g Fx(1)p Fm(;)g Fx($)p Fm(;)g(\014)1511 1251 y Fw(1)1528 1245 y Fx(\()p Fm(")p Fx(\))p Fm(;)g(:)g(:)g(:)f(;)h(\014)1696 1251 y Fv(n)1718 1245 y Fx(\()p Fm(")p Fx(\),)340 1295 y(i.e.,)13 b(the)h(\014rst)h(2)p Fm(n)9 b Fx(+)g(8)14 b(argumen)o(ts)f(of)g Fm(l)q Fx(,)h(b)o(y)g Fm(V)9 b Fx(.)403 1373 y(W)m(e)17 b(are)h(no)o(w)f(going)f(to)h(sho)o(w)h(that)f (in)g(case)i Fm(P)k Fx(has)17 b(a)h(solution,)e(reductions)i(in)f Fn(Q)340 1423 y Fx(mirror)11 b(reductions)i(in)f Fn(U)t Fx(\()p Fm(P)q(;)7 b Fn(Q)p Fx(\).)k(That)h(is,)f(if)h Fm(P)17 b Fx(is)12 b(a)g(PCP)g(instance)h(that)f(has)g(a)g(solution)340 1473 y(then)j(w)o(e)f(get)g(the)h(follo)o(wing)c(particular)j(form)e (of)h(reduction)i(in)e Fn(U)t Fx(\()p Fm(P)q(;)7 b Fn(Q)p Fx(\).)340 1552 y Fd(Prop)q(osition)e(2.)20 b Fl(If)11 b(the)g(PCP)g(instanc)n(e)g Fm(P)16 b Fl(has)11 b(a)g(solution,)g Fm(\015)1342 1537 y Fi(0)1354 1552 y Fm(a)p Fl(,)g(then)g(for)f(every)h (r)n(ewrite)340 1602 y(rule)k Ff(LHS)d Fn(!)f Ff(RHS)k Fl(in)g Fn(Q)g Fl(we)g(have)411 1675 y Fm(A)p Fx(\()p Fm(V)r(;)7 b(W)o(;)g Ff(LHS)q Fx(\))54 b Fn(!)747 1657 y Fw(+)747 1689 y Fi(U)s Fw(\()p Fv(P)q(;)p Fi(Q)p Fw(\))911 1675 y Fm(A)p Fx(\()p Fm(V)r(;)7 b(W)o(;)g Ff(RHS)p Fx(\))340 1763 y Fl(wher)n(e)15 b Fm(W)20 b Fl(denotes)c(the)f(se)n(quenc)n(e)h Fx(0)p Fm(;)7 b Fx(1)p Fm(;)g(a)p Fx($)p Fm(w)1058 1769 y Fw(2)1081 1763 y Fm(:)g(:)g(:)e(w)1166 1769 y Fv(\026)1188 1763 y Fx(\()p Fm(w)q Fx(\))p Fm(;)p 1270 1727 57 2 v 7 w Fx($)p Fm(\015)1314 1751 y Fi(0)1326 1763 y Fx(\()p Fm(x)p Fx(\))p Fm(;)i(a)p Fx($)p Fm(y)1464 1769 y Fw(2)1489 1763 y Fm(:)g(:)g(:)e(y)1564 1769 y Fv(\026)1587 1763 y Fx(\()p Fm(y)q Fx(\))p Fm(;)p 1659 1727 V 7 w Fx($)p Fm(\015)1703 1751 y Fi(0)1716 1763 y Fx(\()p Fm(z)r Fx(\))p Fm(:)340 1841 y Fl(Pr)n(o)n(of.)20 b Fx(Let)e Fm(\015)h Fx(=)e Fm(\013)664 1847 y Fw(1)689 1841 y Fm(:)7 b(:)g(:)e(\013)771 1847 y Fv(n)810 1841 y Fx(=)17 b Fm(\014)882 1847 y Fw(1)908 1841 y Fm(:)7 b(:)g(:)e(\014)986 1847 y Fv(n)1026 1841 y Fx(=)16 b Fm(\015)1097 1826 y Fi(0)1110 1841 y Fm(a)g Fx(b)q(e)i(a)f(solution)f(of)g(the)h(PCP)h(instance)340 1891 y Fm(P)6 b Fx(.)19 b(Let)h Ff(LHS)i Fn(!)e Ff(RHS)g Fx(b)q(e)g(a)g(rule)g(in)f Fn(Q)g Fx(and)g(abbreviate)h(the)h(terms)e ($)p Fm(w)1586 1897 y Fw(2)1611 1891 y Fm(:)7 b(:)g(:)e(w)1696 1897 y Fv(\026)1718 1891 y Fx(\()p Fm(w)q Fx(\))340 1941 y(and)15 b($)p Fm(y)463 1947 y Fw(2)488 1941 y Fm(:)7 b(:)g(:)f(y)564 1947 y Fv(\026)586 1941 y Fx(\()p Fm(y)q Fx(\))16 b(b)o(y)e Fm(w)744 1926 y Fi(0)770 1941 y Fx(and)g Fm(y)872 1926 y Fi(0)885 1941 y Fx(,)f(resp)q(ectiv)o(ely)m(.)i(W)m(e)f (ha)o(v)o(e)h(the)g(follo)o(wing)d(reduction)j(in)340 1991 y Fn(U)t Fx(\()p Fm(P)q(;)7 b Fn(Q)p Fx(\):)539 2066 y Fm(A)p Fx(\()p Fm(V)r(;)g Fx(0)p Fm(;)g Fx(1)p Fm(;)g(aw)764 2049 y Fi(0)774 2066 y Fm(;)p 793 2030 V 7 w Fx($)p Fm(\015)837 2054 y Fi(0)848 2066 y Fx(\()p Fm(x)p Fx(\))p Fm(;)g(ay)966 2049 y Fi(0)978 2066 y Fm(;)p 997 2030 V 7 w Fx($)p Fm(\015)1041 2054 y Fi(0)1053 2066 y Fx(\()p Fm(z)r Fx(\))p Fm(;)g Ff(LHS)q Fx(\))411 2141 y Fn(!)453 2123 y Fi(\003)453 2152 y Fw(\(5\))539 2141 y Fm(A)p Fx(\()p Fm(V)r(;)g Fx(0)p Fm(;)g Fx(1)p Fm(;)g(\015)r(w)765 2123 y Fi(0)775 2141 y Fm(;)p 794 2104 21 2 v 7 w Fx($\()p Fm(x)p Fx(\))p Fm(;)g(\015)r(y)934 2123 y Fi(0)946 2141 y Fm(;)p 965 2104 V 7 w Fx($\()p Fm(z)r Fx(\))p Fm(;)g Ff(LHS)p Fx(\))411 2215 y Fn(!)453 2222 y Fw(\(2\))539 2215 y Fm(A)p Fx(\()p Fm(V)r(;)g Fx(1)p Fm(;)g Fx(0)p Fm(;)g(\015)r(w)765 2198 y Fi(0)775 2215 y Fm(;)p 794 2179 V 7 w Fx($\()p Fm(x)p Fx(\))p Fm(;)g(\015)r(y)934 2198 y Fi(0)946 2215 y Fm(;)p 965 2179 V 7 w Fx($\()p Fm(z)r Fx(\))p Fm(;)g Ff(LHS)p Fx(\))411 2286 y Fn(!)453 2293 y Fw(\(3\))539 2286 y Fm(A)p Fx(\()p Fm(V)r(;)g Fx(1)p Fm(;)g Fx(0)p Fm(;)g(\013)738 2292 y Fw(2)761 2286 y Fm(:)g(:)g(:)f(\013)844 2292 y Fv(n)866 2286 y Fm(w)897 2269 y Fi(0)908 2286 y Fm(;)p 927 2250 66 2 v 7 w Fx($)p Fm(\013)975 2292 y Fw(1)993 2286 y Fx(\()p Fm(x)p Fx(\))p Fm(;)h(\014)1091 2292 y Fw(2)1116 2286 y Fm(:)g(:)g(:)e(\014)1194 2292 y Fv(n)1218 2286 y Fm(y)1239 2269 y Fi(0)1251 2286 y Fm(;)p 1270 2250 63 2 v 7 w Fx($)p Fm(\014)1314 2292 y Fw(1)1332 2286 y Fx(\()p Fm(z)r Fx(\))p Fm(;)i Ff(LHS)q Fx(\))411 2357 y Fn(!)453 2340 y Fi(\003)453 2368 y Fw(\(3\))539 2357 y Fm(A)p Fx(\()p Fm(V)r(;)g Fx(1)p Fm(;)g Fx(0)p Fm(;)g(w)742 2340 y Fi(0)752 2357 y Fm(;)p 771 2321 45 2 v 7 w Fx($)p Fm(\015)r Fx(\()p Fm(x)p Fx(\))p Fm(;)g(y)911 2340 y Fi(0)923 2357 y Fm(;)p 942 2321 V 7 w Fx($)p Fm(\015)r Fx(\()p Fm(z)r Fx(\))p Fm(;)g Ff(LHS)p Fx(\))411 2432 y Fn(!)453 2439 y Fw(\(4\))539 2432 y Fm(A)p Fx(\()p Fm(V)r(;)g Fx(0)p Fm(;)g Fx(1)p Fm(;)g(aw)764 2415 y Fi(0)774 2432 y Fm(;)p 793 2396 57 2 v 7 w Fx($)p Fm(\015)837 2420 y Fi(0)848 2432 y Fx(\()p Fm(x)p Fx(\))p Fm(;)g(ay)966 2415 y Fi(0)978 2432 y Fm(;)p 997 2396 V 7 w Fx($)p Fm(\015)1041 2420 y Fi(0)1053 2432 y Fx(\()p Fm(z)r Fx(\))p Fm(;)g Ff(RHS)p Fx(\))p Fm(:)1050 2556 y Fx(6)p eop %%Page: 7 7 7 6 bop 183 194 a Fx(First,)16 b(using)f(rules)i(\(5\),)e Fm(\015)613 179 y Fi(0)642 194 y Fx(in)g(the)i(2)p Fm(n)10 b Fx(+)h(12-th)16 b(\(2)p Fm(n)10 b Fx(+)h(14-th\))16 b(argumen)o(t)f(is)g(shifted)i(to)183 244 y(the)f(2)p Fm(n)10 b Fx(+)h(11-th)k(\(2)p Fm(n)c Fx(+)g(13-th,)j(resp.\))j (argumen)o(t)e(c)o(haracter)i(b)o(y)e(c)o(haracter.)i(Note)f(that)p 183 257 57 2 v 183 293 a($)p Fm(\015)227 281 y Fi(0)239 293 y Fx(\()p Fm(x)p Fx(\))f(=)p 357 260 36 2 v 15 w Fm(\015)380 281 y Fi(0)p 408 257 21 2 v 408 293 a Fx($\()p Fm(x)p Fx(\).)g(Next)i(b)o(y)f(rule)g(\(2\),)f(there)j(is)e(a)f(c)o (hange)i(of)e(state)i(from)d(0)p Fm(;)7 b Fx(1)15 b(to)h(1)p Fm(;)7 b Fx(0.)183 343 y(Then,)k(since)h Fm(\015)i Fx(is)e(a)f (solution)f(of)h Fm(P)6 b Fx(,)k(it)h(can)h(b)q(e)g(shifted)g(bac)o(k)f (b)o(y)g(using)g(rules)h(\(3\).)f(Finally)m(,)183 393 y(with)i(rule)h(\(4\),)g(the)g(state)h(is)f(c)o(hanged)g(bac)o(k)g(to)g (0)p Fm(;)7 b Fx(1.)561 b Fn(u)-28 b(t)245 480 y Fx(Con)o(v)o(ersely)m (,)9 b(a)h(reduction)g(in)f Fn(U)t Fx(\()p Fm(P)q(;)e Fn(Q)p Fx(\))j(giv)o(es)f(rise)i(either)f(to)g(an)f(underlying)h (reduction)183 530 y(in)j Fn(Q)h Fx(or)g(to)g(a)g(reduction)h(in)e Fn(U)t Fx(\()p Fm(P)q(;)7 b Fn(Q)p Fx(\))14 b(without)g(the)g(2)p Fm(m)g Fx(rules)h(\(4\).)f(W)m(e)f(will)g(denote)i(the)183 580 y(latter)f(system)f(b)o(y)h Fn(U)t Fx(\()p Fm(P)q(;)7 b Fn(;)p Fx(\).)183 667 y Fd(Prop)q(ositi)o(on)e(3.)21 b Fl(If)h Fm(W)28 b Fl(and)22 b Fm(t)h Fl(c)n(ontain)f(no)h Fm(A)f Fl(symb)n(ols)g(then)h Fm(A)p Fx(\()p Fm(V)r(;)7 b(W)o(;)g(t)p Fx(\))24 b Fn(!)1513 674 y Fi(U)s Fw(\()p Fv(P)q(;)p Fi(Q)p Fw(\))183 716 y Fm(A)p Fx(\()p Fm(V)r(;)7 b(W)320 701 y Fi(0)332 716 y Fm(;)g(t)366 701 y Fi(0)377 716 y Fx(\))15 b Fl(implies)f Fm(t)d Fn(!)618 722 y Fv(Q)658 716 y Fm(t)673 701 y Fi(0)699 716 y Fl(or)k Fm(t)c Fx(=)h Fm(t)838 701 y Fi(0)864 716 y Fl(and)k Fm(A)p Fx(\()p Fm(V)r(;)7 b(W)o(;)g(t)p Fx(\))k Fn(!)1178 723 y Fi(U)s Fw(\()p Fv(P)q(;)p Fi(;)p Fw(\))1290 716 y Fm(A)p Fx(\()p Fm(V)r(;)c(W)1427 701 y Fi(0)1439 716 y Fm(;)g(t)p Fx(\))p Fl(.)183 796 y(Pr)n(o)n(of.)20 b Fx(Since)15 b(there)h(is)f(only)f(one) h Fm(A)g Fx(sym)o(b)q(ol)e(in)h Fm(A)p Fx(\()p Fm(V)r(;)7 b(W)o(;)g(t)p Fx(\),)15 b(the)g(reduction)h(m)o(ust)d(tak)o(e)183 846 y(place)d(at)g(the)h(ro)q(ot)g(p)q(osition.)e(If)h(a)g(rule)h (\(4\))f(has)g(b)q(een)i(applied,)d(then)i Fm(t)h Fn(!)1342 852 y Fv(Q)1381 846 y Fm(t)1396 831 y Fi(0)1408 846 y Fx(.)e(Otherwise,)183 896 y Fm(A)p Fx(\()p Fm(V)r(;)d(W)o(;)g(t)p Fx(\))k Fn(!)416 903 y Fi(U)s Fw(\()p Fv(P)q(;)p Fi(;)p Fw(\))528 896 y Fm(A)p Fx(\()p Fm(V)r(;)c(W)665 881 y Fi(0)677 896 y Fm(;)g(t)711 881 y Fi(0)722 896 y Fx(\).)12 b(Ob)o(viously)m(,)g(this)h(implies)e Fm(t)g Fx(=)h Fm(t)1270 881 y Fi(0)1295 896 y Fx(b)o(y)h(the)g(form)f(of)g(the)183 945 y(rules)i(in)g Fn(U)t Fx(\()p Fm(P)q(;)7 b Fn(;)p Fx(\).)1123 b Fn(u)-28 b(t)183 1033 y Fd(Prop)q(ositi)o(on)5 b(4.)21 b Fl(The)15 b(TRS)g Fn(U)t Fx(\()p Fm(P)q(;)7 b Fn(;)p Fx(\))14 b Fl(is)h(simply)f(terminating,)g(for)g(any)i Fm(P)6 b Fl(.)183 1120 y(Pr)n(o)n(of.)20 b Fx(Since)11 b Fn(U)t Fx(\()p Fm(P)q(;)c Fn(;)p Fx(\))k(is)g(length-preserving,)g (it)g(is)g(su\016cien)o(t)h(to)f(sho)o(w)g(termination.)e(W)m(e)183 1169 y(sho)o(w)14 b(termination)f(b)o(y)i(seman)o(tic)f(lab)q(elling)f ([20)o(].)h(Let)h(the)g(mo)q(del)e(b)q(e)j Fn(f)p Fx(0)p Fm(;)7 b Fx(1)p Fn(g)p Fx(,)12 b(and)j(let)g(1)183 1219 y(b)q(e)f(in)o(terpreted)h(b)o(y)e(1,)g(and)h(ev)o(ery)g(other)g(sym)o (b)q(ol)e(b)o(y)h(constan)o(t)h(0.)f(Lab)q(el)h(the)g(sym)o(b)q(ol)d Fm(A)183 1269 y Fx(b)o(y)h(2)p Fm(x)284 1275 y Fw(2)308 1269 y Fx(+)6 b Fm(x)370 1275 y Fw(2)p Fv(n)p Fw(+10)480 1269 y Fx(where)13 b Fm(x)622 1275 y Fv(i)648 1269 y Fx(denotes)g(the)g(v)n(alue)f(of)f Fm(A)p Fx('s)i Fm(i)p Fx(-th)f(argumen)o(t.)f(In)h(the)h(lab)q(elled)183 1319 y(system,)p 329 1283 162 2 v 10 w Fn(U)t Fx(\()p Fm(P)q(;)7 b Fn(Q)456 1325 y Fw(3)474 1319 y Fx(\),)j(obtained)h(in)f(this)h(w)o (a)o(y)f(the)h(sym)o(b)q(ol)e Fm(A)i Fx(carries)h(the)f(lab)q(el)f(2)s (+)s Fm(v)i Fx(at)f(the)183 1369 y(left-hand)g(side,)h(and)f(the)h(lab) q(els)g(2)p Fm(v)q Fx(,)f(2)p Fm(u)p Fx(,)g(2)p Fm(v)6 b Fx(+)f(1,)12 b(and)f(2)p Fm(v)6 b Fx(+)f(1at)12 b(the)g(righ)o (t-hand)f(sides)i Fm(r)1594 1375 y Fw(1)1612 1369 y Fx(,)183 1418 y Fm(r)202 1424 y Fv(i)p Fw(+1)257 1418 y Fx(,)f Fm(r)300 1424 y Fv(n)p Fw(+2)p Fv(m)p Fw(+2)436 1418 y Fx(,)f(and)h Fm(r)557 1424 y Fv(n)p Fw(+2)p Fv(m)p Fw(+3)693 1418 y Fx(,)f(resp)q(ectiv)o(ely)m(.)i(T)m(aking)e(in)o(to)g (accoun)o(t)h(that)h Fm(u;)7 b(v)12 b Fn(2)f(f)p Fx(0)p Fm(;)c Fx(1)p Fn(g)183 1468 y Fx(one)16 b(\014nds)h(that)f(the)h(lab)q (el)f(decreases)j(for)d(all)f(rules)i(except)g(in)f(case)h Fm(u)f Fx(=)f(1,)h Fm(v)h Fx(=)f(0)g(for)183 1518 y(Rule)g(\(2\),)f (and)i(case)g Fm(v)g Fx(=)f(1)g(for)g(t)o(yp)q(e)h(\(5\))g(rules,)f (where)i(it)e(sta)o(ys)g(equal.)g(T)m(ermination)183 1568 y(of)h(the)i(lab)q(elled)e(system)h(is)g(no)o(w)g(sho)o(wn)g(b)o (y)f(recursiv)o(e)j(path)e(order)h(with)e(precedence)183 1618 y Fm(A)214 1624 y Fw(3)248 1618 y Fm(>)e(A)326 1624 y Fw(2)361 1618 y Fm(>)g(A)439 1624 y Fw(1)473 1618 y Fm(>)h(A)552 1624 y Fw(0)587 1618 y Fx(and)g Fm(A)701 1624 y Fw(0)736 1618 y Fx(greater)h(than)f(an)o(y)g(other)h(function)f (sym)o(b)q(ol,)e(and)i Fm(A)1605 1624 y Fw(2)183 1667 y Fx(and)h Fm(A)298 1673 y Fw(0)334 1667 y Fx(ha)o(ving)f(status)i (lexicographic)e(\014rst)i(2)p Fm(n)11 b Fx(+)h(11)17 b(then)h(2)p Fm(n)11 b Fx(+)h(13)k(then)i(the)g(other)183 1717 y(argumen)o(ts,)c Fm(A)429 1723 y Fw(3)462 1717 y Fx(and)h Fm(A)575 1723 y Fw(1)609 1717 y Fx(ha)o(ving)f(status)i (\014rst)g(2)p Fm(n)10 b Fx(+)g(12)15 b(then)h(2)p Fm(n)9 b Fx(+)i(14)j(then)i(the)g(other)183 1767 y(argumen)o(ts,)c(and)i Ff(cons)g Fx(and)p 648 1744 77 2 v 14 w Ff(cons)h Fx(ha)o(ving)d (status)j(righ)o(t-to-left.)378 b Fn(u)-28 b(t)183 1854 y Fd(Theorem)6 b(5.)21 b Fl(If)15 b Fm(P)20 b Fl(has)15 b(no)h(solution)f(then)g Fn(U)t Fx(\()p Fm(P)q(;)7 b Fn(Q)p Fx(\))14 b Fl(is)h(total)r(ly)f(terminating.)133 b Fn(u)-28 b(t)245 1941 y Fx(The)14 b(complicated)f(pro)q(of)g(can)h(b) q(e)h(found)e(in)h(the)g(full)f(v)o(ersion)h([10)o(])f(of)h(this)g(pap) q(er.)183 2072 y Fo(4)56 b(One-Rule)17 b(Systems)183 2168 y Fx(T)m(ransforming)10 b Fn(U)t Fx(\()p Fm(P)q(;)d Fn(Q)p Fx(\))13 b(in)o(to)g(a)f(single-rule)h(TRS)g Fn(S)s Fx(\()p Fm(P)q(;)7 b Fn(Q)p Fx(\))13 b(is)g(easy:)g(w)o(e)h(de\014ne)g Fn(S)s Fx(\()p Fm(P)q(;)7 b Fn(Q)p Fx(\))183 2218 y(as)14 b(the)g(rule)253 2300 y Fm(l)54 b Fn(!)f Fm(B)r Fx(\()p Fm(r)482 2306 y Fw(1)501 2300 y Fm(;)7 b(:)g(:)g(:)e(;)i(r)613 2306 y Fv(n)p Fw(+2)p Fv(m)p Fw(+3)748 2300 y Fx(\))183 2382 y(where)15 b Fm(B)i Fx(is)e(a)f(new)h(function)f(sym)o(b)q(ol)f (of)h(arit)o(y)g Fm(n)9 b Fx(+)h(2)p Fm(m)g Fx(+)g(3.)k(The)h(sym)o(b)q (ol)d Fm(B)17 b Fx(is)e(called)183 2432 y(a)g Fl(dummy)k Fx(b)q(ecause)e(it)e(only)g(app)q(ears)h(in)f(the)h(righ)o(t-hand)f (sides)h(of)f(the)h(rules,)f(hence)i(it)893 2556 y(7)p eop %%Page: 8 8 8 7 bop 340 194 a Fx(acts)19 b(as)e(a)h(barrier)g(for)f(rewrite)i (steps.)f(So)g(the)g(transition)f(from)f Fn(S)s Fx(\()p Fm(P)q(;)7 b Fn(Q)p Fx(\))17 b(to)h Fn(U)t Fx(\()p Fm(P)q(;)7 b Fn(Q)p Fx(\))340 244 y(is)17 b(a)g(particular)g(form)e(of)i Fl(dummy)h(elimination)i Fx([6],)c(a)h(metho)q(d)f(to)h(supp)q(ort)h (pro)q(ofs)f(of)340 293 y(termination)c(b)o(y)g(decomp)q(osing)g(righ)o (t-hand)g(sides.)340 387 y Fd(Prop)q(osition)5 b(6.)20 b Fl(L)n(et)12 b Fn(R)h Fl(b)n(e)f(a)g(one-rule)g(TRS)h Fm(l)f Fn(!)f Fm(B)r Fx(\()p Fm(r)1247 393 y Fw(1)1266 387 y Fm(;)c(:)g(:)g(:)e(;)i(r)1378 393 y Fv(k)1398 387 y Fx(\))12 b Fl(wher)n(e)g Fm(B)i Fl(is)e(a)g(symb)n(ol)340 437 y(that)18 b(do)n(es)f(not)h(o)n(c)n(cur)f(in)g Fm(l)i Fl(nor)e(in)g(any)h(of)g(the)f Fm(r)1149 443 y Fv(i)1163 437 y Fl(,)g(and)h(let)e Fm(E)r Fx(\()p Fn(R)p Fx(\))i Fl(denote)g(the)f(system)340 487 y Fn(f)p Fm(l)c Fn(!)e Fm(r)458 493 y Fv(i)483 487 y Fn(j)g Fx(1)g Fn(\024)h Fm(i)g Fn(\024)g Fm(k)q Fn(g)p Fl(.)i(Supp)n(ose)i Fm(E)r Fx(\()p Fn(R)p Fx(\))f Fl(is)g(line)n(ar.)1157 472 y Fw(6)356 572 y Fl(1.)21 b(If)15 b Fn(R)g Fl(is)f(lo)n(oping)h(then)h Fm(E)r Fx(\()p Fn(R)p Fx(\))f Fl(is)f(lo)n(oping.)356 622 y(2.)21 b(If)15 b Fm(E)r Fx(\()p Fn(R)p Fx(\))g Fl(is)f (terminating)h(then)g Fn(R)g Fl(is)g(terminating.)356 673 y(3.)21 b(If)15 b Fn(R)g Fl(is)f(self-emb)n(e)n(dding)h(then)g Fm(E)r Fx(\()p Fn(R)p Fx(\))g Fl(is)g(self-emb)n(e)n(dding.)356 723 y(4.)21 b Fm(E)r Fx(\()p Fn(R)p Fx(\))15 b Fl(is)g(simply)f (terminating)h(if)f(and)i(only)f(if)f Fn(R)h Fl(is)g(simply)f (terminating.)356 773 y(5.)21 b Fm(E)r Fx(\()p Fn(R)p Fx(\))15 b Fl(is)g(total)r(ly)f(terminating)h(if)f(and)i(only)f(if)f Fn(R)h Fl(is)g(total)r(ly)f(terminating.)403 867 y Fx(The)f(con)o(v)o (erse)g(of)f(statemen)o(ts)h(1,)f(2,)g(and)g(3)g(do)q(es)h(not)g(hold)f (as)g(the)h(coun)o(terexamples)340 917 y Fn(R)375 923 y Fw(1)406 917 y Fx(=)f Fn(f)p Fm(f)t Fx(\()p Fm(g)q Fx(\()p Fm(x)p Fx(\)\))g Fn(!)f Fm(B)r Fx(\()p Fm(f)t Fx(\()p Fm(f)t Fx(\()p Fm(x)p Fx(\)\))p Fm(;)c(g)q Fx(\()p Fm(g)q Fx(\()p Fm(x)p Fx(\)\)\))p Fn(g)p Fx(,)12 b Fn(R)1099 923 y Fw(2)1129 917 y Fx(=)g Fn(f)p Fm(f)t Fx(\()p Fm(g)q Fx(\()p Fm(x)p Fx(\)\))h Fn(!)e Fm(B)r Fx(\()p Fm(f)t Fx(\()p Fm(f)t Fx(\()p Fm(h)p Fx(\()p Fm(x)p Fx(\)\)\))p Fm(;)c(g)q Fx(\()p Fm(g)q Fx(\()p Fm(x)p Fx(\)\)\))p Fn(g)340 966 y Fx(sho)o(w.)15 b(Here)i Fm(E)r Fx(\()p Fn(R)640 972 y Fw(1)659 966 y Fx(\))f(is)f(lo)q(oping,)f(but)h Fn(R)1006 972 y Fw(1)1040 966 y Fx(is)h(terminating;)d Fm(E)r Fx(\()p Fn(R)1407 972 y Fw(2)1426 966 y Fx(\))j(is)f(self-em)o (b)q(edding,)340 1016 y(but)f Fn(R)451 1022 y Fw(2)484 1016 y Fx(is)g(non-self-em)o(b)q(edding.)340 1101 y Fl(Pr)n(o)n(of.)20 b Fx(A)15 b(pro)q(of)f(of)h(statemen)o(t)f(1)g(for)h(the)g(case)h Fm(k)d Fx(=)g(2)i(can)g(b)q(e)g(found)f(in)g([19)o(].)g(It)h(easily)340 1151 y(extends)i(to)f(the)g(general)f(case.)h(Pro)q(ofs)g(of)f (statemen)o(ts)h(2,)e(4,)h(and)g(5)h(app)q(ear)g(in)f([17)o(].)f(It)340 1201 y(remains)f(to)h(pro)o(v)o(e)g(statemen)o(t)g(3.)403 1251 y(W)m(e)h(call)g(a)h(p)q(osition)f(an)h Fl(inner)g Fx(p)q(osition)f(of)h Fm(t)g Fx(if)f(it)h(is)f(a)h(function)g(sym)o(b)q (ol)e(p)q(osition)340 1301 y(of)k Fm(t)g Fx(not)g(at)f(the)i(top.)e (Call)g(a)h(p)q(osition)f Fm(p)h Fx(in)f(a)h(term)g Fm(t)f Fl(touche)n(d)j(by)f(the)f(r)n(ewrite)f(step)340 1351 y Fm(t)407 1327 y Fv(u)372 1351 y Fn(\000)-9 b(\000)h(!)386 1378 y Fv(l)p Fi(!)p Fv(r)477 1351 y Fm(t)492 1336 y Fi(0)521 1351 y Fx(if)16 b Fm(p)h Fx(is)g(of)f(the)i(form)d Fm(p)i Fx(=)g Fm(u:v)h Fx(where)g Fm(v)g Fx(is)f(an)g(inner)g(p)q (osition)g(in)f Fm(l)q Fx(.)h(No)o(w)g(a)340 1422 y(p)q(osition)e Fm(p)h Fx(ma)o(y)d(b)q(e)k(called)e Fl(touche)n(d)i(during)g(the)f(r)n (e)n(duction)g Fm(t)e Fn(!)1414 1404 y Fw(+)1414 1434 y Fv(R)1455 1422 y Fm(t)1470 1407 y Fi(0)1498 1422 y Fx(if)g(the)j(reduction)340 1472 y(is)e(of)f(the)h(form)e Fm(t)g Fn(!)672 1457 y Fi(\003)672 1483 y Fv(R)711 1472 y Fm(t)726 1457 y Fi(00)760 1472 y Fn(!)802 1478 y Fv(R)842 1472 y Fm(t)857 1457 y Fi(0)o(00)900 1472 y Fn(!)942 1457 y Fi(\003)942 1483 y Fv(R)982 1472 y Fm(t)997 1457 y Fi(0)1023 1472 y Fx(and)h(a)g(residual)h Fm(p)1316 1457 y Fi(00)1352 1472 y Fx(in)f Fm(t)1416 1457 y Fi(0)o(0)1452 1472 y Fx(of)g Fm(p)g Fx(b)o(y)g Fm(t)f Fn(!)1663 1457 y Fi(\003)1663 1483 y Fv(R)1703 1472 y Fm(t)1718 1457 y Fi(0)o(0)1753 1472 y Fx(is)340 1522 y(touc)o(hed)i(in)e(the)i(step)g Fm(t)719 1507 y Fi(0)o(0)752 1522 y Fn(!)794 1528 y Fv(R)832 1522 y Fm(t)847 1507 y Fi(0)o(00)878 1522 y Fx(.)403 1572 y(Assume)f(a)h(self-em)o(b)q(edding)f(reduction)h Fm(t)e Fn(!)1132 1554 y Fw(+)1132 1584 y Fi(R)1175 1572 y Fm(t)1190 1557 y Fi(0)1215 1572 y Fn(!)1257 1557 y Fi(\003)1257 1584 y(E)m Fg(mb)1330 1572 y Fm(t)p Fx(.)h(If)g(an)h (inner)g(p)q(osition,)f Fm(q)q Fx(,)340 1622 y(of)j Fm(t)f Fx(remains)g(un)o(touc)o(hed)i(during)e(this)h(reduction,)g(the)h (reduction)f(ma)o(y)e(b)q(e)j(split)e(in)o(to)340 1672 y(the)f(reduction)f(steps)i(ab)q(o)o(v)o(e)d(and)h(those)h(b)q(elo)o(w) e(the)i(\(unique\))f(residual)g(of)f Fm(q)q Fx(:)411 1760 y Fm(t)p Fx([)p Fm(z)r Fx(])471 1766 y Fv(q)500 1760 y Fn(!)542 1743 y Fi(\003)542 1770 y(R)584 1760 y Fm(t)599 1743 y Fi(0)610 1760 y Fx([)p Fm(z)r Fx(])655 1766 y Fv(q)671 1758 y Fb(0)696 1760 y Fn(!)738 1743 y Fi(\003)738 1770 y(E)m Fg(mb)809 1760 y Fm(t)p Fx([)p Fm(z)r Fx(])869 1766 y Fv(q)885 1758 y Fb(00)907 1760 y Fm(;)89 b(t)p Fn(j)1035 1766 y Fv(q)1065 1760 y Fn(!)1107 1743 y Fi(\003)1107 1770 y(R)1148 1760 y Fm(t)1163 1743 y Fi(0)1175 1760 y Fn(j)1187 1766 y Fv(q)1203 1758 y Fb(0)1228 1760 y Fn(!)1270 1743 y Fi(\003)1270 1770 y(E)m Fg(mb)1341 1760 y Fm(t)p Fn(j)1368 1766 y Fv(q)1384 1758 y Fb(00)340 1854 y Fx(If)14 b Fm(q)402 1838 y Fi(0)o(0)437 1854 y Fx(is)f(b)q(elo)o(w)h Fm(q)h Fx(then)f Fm(t)p Fx([)p Fm(z)r Fx(])784 1860 y Fv(q)813 1854 y Fn(!)855 1836 y Fw(+)855 1866 y Fi(R)897 1854 y Fm(t)912 1838 y Fi(0)924 1854 y Fx([)p Fm(z)r Fx(])969 1860 y Fv(q)985 1851 y Fb(0)1009 1854 y Fn(!)1051 1838 y Fi(\003)1051 1865 y(E)m Fg(mb)1122 1854 y Fm(t)p Fx([)p Fm(z)r Fx(])1182 1860 y Fv(q)1198 1851 y Fb(00)1232 1854 y Fn(!)1274 1838 y Fi(\003)1274 1865 y(E)m Fg(mb)1345 1854 y Fm(t)p Fx([)p Fm(z)r Fx(])1405 1860 y Fv(q)1436 1854 y Fx(is)g(a)f(self-em)o(b)q (edding)340 1903 y(reduction.)h(If)g Fm(q)598 1888 y Fi(0)o(0)630 1903 y Fx(=)e Fm(q)j Fx(then)f(one)g(of)f(the)h(t)o(w)o(o) g(reductions)g(m)o(ust)f(b)q(e)h(nonempt)o(y;)e(it)i(forms)340 1953 y(a)g(self-em)o(b)q(edding)f(reduction.)h(Otherwise)h Fm(t)p Fn(j)1077 1959 y Fv(q)1107 1953 y Fn(!)1149 1935 y Fw(+)1149 1965 y Fi(R)1190 1953 y Fm(t)1205 1938 y Fi(0)1217 1953 y Fn(j)1229 1959 y Fv(q)1245 1951 y Fb(0)1270 1953 y Fn(!)1312 1938 y Fi(\003)1312 1965 y(E)m Fg(mb)1383 1953 y Fm(t)p Fn(j)1410 1959 y Fv(q)1426 1951 y Fb(00)1460 1953 y Fn(!)1502 1938 y Fi(\003)1502 1965 y(E)m Fg(mb)1573 1953 y Fm(t)p Fn(j)1600 1959 y Fv(q)1632 1953 y Fx(is)f(a)f(self-)340 2003 y(em)o(b)q(edding)k(reduction.)h(By)f(induction,)g(all)f(un)o (touc)o(hed)j(inner)e(p)q(ositions)h(of)e Fm(t)i Fx(can)g(b)q(e)340 2053 y(eliminated.)403 2103 y(One)i(ma)o(y)f(so)h(assume)f(that)h(ev)o (ery)h(inner)f(p)q(osition)g(of)f Fm(t)h Fx(is)g(touc)o(hed)h(during)f (the)340 2153 y(self-em)o(b)q(edding)13 b(reduction.)h(Then)g Fm(t)f Fx(cannot)h(con)o(tain)f Fm(B)j Fx(sym)o(b)q(ols)c(except)j(one) f Fm(B)i Fx(sym-)340 2203 y(b)q(ol)j(at)g(the)g(top.)g(By)g(a)f(coun)o (ting)h(argumen)o(t)f(no)h Fm(B)i Fx(sym)o(b)q(ols)d(o)q(ccur)i(in)e Fm(t)h Fx(at)g(all.)e(All)340 2253 y Fm(B)h Fx(sym)o(b)q(ols)c(that)i (are)g(created)g(b)o(y)g Fn(R)f Fx(steps)i(m)o(ust)d(therefore)j(b)q(e) f(cancelled)g(b)o(y)f(an)h Fn(E)m Fl(mb)340 2302 y Fx(step)f(later.)f (One)h(ma)o(y)d(comm)o(ute)g(the)i Fn(E)m Fl(mb)g Fx(step,)h Fm(B)r Fx(\()p Fm(t)1215 2308 y Fw(1)1234 2302 y Fm(;)7 b(:)g(:)g(:)e(;)i(t)1342 2308 y Fv(k)1362 2302 y Fx(\))12 b Fn(!)f Fm(t)1458 2308 y Fv(i)1472 2302 y Fx(,)i(with)h(all)f(preced-) 340 2352 y(ing)j(steps)h(un)o(til)f(the)g Fn(R)h Fx(step)g(that)f (created)i(the)e(corresp)q(onding)i Fm(B)g Fx(sym)o(b)q(ol.)c(The)j (pair)p 340 2389 237 2 v 349 2416 a Fu(6)379 2432 y Ft(The)c(prop)q (osition)j(also)e(holds)g(without)g Fq(E)r Ft(\()p Fp(R)p Ft(\))f(righ)o(t-linear.)1050 2556 y Fx(8)p eop %%Page: 9 9 9 8 bop 183 194 a Fm(c)p Fx([)p Fm(l)q(\033)q Fx(])15 b Fn(!)320 200 y Fi(R)367 194 y Fm(c)p Fx([)p Fm(B)r Fx(\()p Fm(r)465 200 y Fw(1)483 194 y Fm(\033)o(;)7 b(:)g(:)g(:)e(;)i (r)618 200 y Fv(k)637 194 y Fm(\033)q Fx(\)])17 b Fn(!)749 200 y Fi(E)m Fg(mb)825 194 y Fm(c)p Fx([)p Fm(r)874 200 y Fv(i)887 194 y Fm(\033)q Fx(])f(of)g(steps)i(can)f(b)q(e)g(replaced)h (b)o(y)f(an)f Fm(E)r Fx(\()p Fn(R)p Fx(\))183 244 y(step)i Fm(c)p Fx([)p Fm(l)q(\033)q Fx(])f Fn(!)g Fm(c)p Fx([)p Fm(r)479 250 y Fv(i)492 244 y Fm(\033)q Fx(].)f(Eac)o(h)i(suc)o(h)g (replacemen)o(t)f(reduces)j(the)e(n)o(um)o(b)q(er)e(of)h Fm(B)j Fx(sym)o(b)q(ols)183 293 y(in)c(the)i(in)o(termediate)f(term,)f Fm(t)683 278 y Fi(0)695 293 y Fx(.)h(Rep)q(eating)g(this)g(pro)q (cedure)i(remo)o(v)o(es)e(all)f Fm(B)k Fx(sym)o(b)q(ols)183 343 y(from)11 b Fm(t)295 328 y Fi(0)320 343 y Fx(hence)k(the)f (reduction)g(con)o(tains)f(no)g(more)f Fn(R)i Fx(steps.)g(W)m(e)f(ha)o (v)o(e)g(th)o(us)h(obtained)f(a)183 393 y(self-em)o(b)q(edding)f (reduction)j(for)f Fm(E)r Fx(\()p Fn(R)p Fx(\).)1596 443 y Fn(u)-28 b(t)183 531 y Fd(Prop)q(ositi)o(on)5 b(7.)21 b Fl(If)f(ther)n(e)g(ar)n(e)g(no)h Fm(A)g Fl(symb)n(ols)f(in)h(the)f (se)n(quenc)n(e)h Fm(W)27 b Fl(of)20 b(terms)g(then)183 581 y Fm(A)p Fx(\()p Fm(V)r(;)7 b(W)f Fx(\))21 b Fn(!)399 563 y Fw(+)399 595 y Fi(U)s Fw(\()p Fv(P)q(;)p Fi(Q)p Fw(\))530 581 y Fm(A)p Fx(\()p Fm(V)r(;)7 b(W)667 566 y Fi(0)678 581 y Fx(\))20 b Fl(if)g(and)g(only)h(if)e Fm(A)p Fx(\()p Fm(V)r(;)7 b(W)f Fx(\))21 b Fn(!)1202 563 y Fw(+)1202 595 y Fi(S)r Fw(\()p Fv(P)q(;)p Fi(Q)p Fw(\))1332 581 y Fm(C)s Fx([)p Fm(A)p Fx(\()p Fm(V)r(;)7 b(W)1514 566 y Fi(0)1525 581 y Fx(\)])19 b Fl(for)183 630 y(some)c(c)n(ontext)g Fm(C)s Fl(.)1119 b Fn(u)-28 b(t)183 762 y Fo(5)56 b(The)18 b(T)-5 b(ermination)17 b(Hierarc)n(h)n(y)183 859 y Fx(In)d(this)f(section)i(w)o(e)f(apply)f (the)i(construction)g Fn(S)s Fx(\()p Fm(P)q(;)7 b Fn(Q)p Fx(\))13 b(to)h(the)g(follo)o(wing)e(TRSs)i Fn(Q)p Fx(.)183 947 y Fd(De\014niti)o(on)5 b(8.)20 b Fx(The)15 b(TRSs)f Fn(Q)689 953 y Fw(1)707 947 y Fm(;)7 b(:)g(:)g(:)e(;)i Fn(Q)834 953 y Fw(5)866 947 y Fx(are)14 b(de\014ned)h(as)f(follo)o(ws:) 253 1030 y Fn(Q)287 1036 y Fw(1)317 1030 y Fx(=)361 996 y Fe(\010)391 1030 y Fm(d)d Fn(!)g Fm(d)505 996 y Fe(\011)253 1122 y Fn(Q)287 1128 y Fw(2)317 1122 y Fx(=)361 1063 y Fe(\032)398 1096 y Fm(g)q Fx(\()p Fm(d;)c(b)p Fx(\()p Fm(x)534 1081 y Fi(0)545 1096 y Fx(\))p Fm(;)g(y)601 1081 y Fi(0)613 1096 y Fx(\))12 b Fn(!)f Fm(g)q Fx(\()p Fm(d;)c(x)796 1081 y Fi(0)807 1096 y Fm(;)g(b)p Fx(\()p Fm(y)881 1081 y Fi(0)893 1096 y Fx(\)\))398 1146 y Fm(g)q Fx(\()p Fm(d;)g(b)p Fx(\()p Fm(x)534 1131 y Fi(0)545 1146 y Fx(\))p Fm(;)g(y)601 1131 y Fi(0)613 1146 y Fx(\))12 b Fn(!)f Fm(g)q Fx(\()p Fm(x)755 1131 y Fi(0)767 1146 y Fm(;)c(y)807 1131 y Fi(0)819 1146 y Fm(;)g(b)p Fx(\()p Fm(b)p Fx(\()p Fm(d)p Fx(\)\)\))981 1063 y Fe(\033)253 1213 y Fn(Q)287 1219 y Fw(3)317 1213 y Fx(=)361 1179 y Fe(\010)391 1213 y Fm(g)q Fx(\()p Fm(d)p Fx(\))12 b Fn(!)f Fm(g)q Fx(\()p Fm(h)p Fx(\()p Fm(d)p Fx(\)\))668 1179 y Fe(\011)253 1305 y Fn(Q)287 1311 y Fw(4)317 1305 y Fx(=)361 1246 y Fe(\032)398 1279 y Fm(g)q Fx(\()p Fm(d;)c(e;)g(x)538 1264 y Fi(0)549 1279 y Fx(\))k Fn(!)h Fm(g)q Fx(\()p Fm(x)691 1264 y Fi(0)702 1279 y Fm(;)7 b(h)p Fx(\()p Fm(e)p Fx(\))p Fm(;)g(e)p Fx(\))398 1329 y Fm(g)q Fx(\()p Fm(d;)g(e;)g(x)538 1314 y Fi(0)549 1329 y Fx(\))k Fn(!)h Fm(g)q Fx(\()p Fm(h)p Fx(\()p Fm(d)p Fx(\))p Fm(;)7 b(x)788 1314 y Fi(0)799 1329 y Fm(;)g(d)p Fx(\))861 1246 y Fe(\033)253 1421 y Fn(Q)287 1427 y Fw(5)317 1421 y Fx(=)361 1362 y Fe(\032)398 1396 y Fm(g)q Fx(\()p Fm(d;)g(e)p Fx(\))12 b Fn(!)f Fm(g)q Fx(\()p Fm(e;)c(e)p Fx(\))398 1445 y Fm(g)q Fx(\()p Fm(d;)g(e)p Fx(\))12 b Fn(!)f Fm(g)q Fx(\()p Fm(d;)c(d)p Fx(\))697 1362 y Fe(\033)245 1532 y Fx(Observ)o(e)20 b(that)f(in)g(eac)o(h)g Fn(Q)690 1538 y Fv(i)723 1532 y Fx(the)h(left-hand)e(sides)i(coincide)f(and)g(that)g(eac)o(h)g Fn(Q)1563 1538 y Fv(i)1596 1532 y Fx(is)183 1581 y(linear)13 b(and)h(uses)h(no)f(v)n(ariables)f(from)f(Defninition)g(1.)h(Hence)j Fn(U)t Fx(\()p Fm(P)q(;)7 b Fn(Q)1309 1587 y Fv(i)1322 1581 y Fx(\))14 b(is)g(linear,)f(to)q(o.)245 1631 y(No)o(w)c(w)o(e)h (ha)o(v)o(e)g(all)e(the)i(ingredien)o(ts)g(to)g(complete)f(the)h (relativ)o(e)g(undecidabilit)o(y)e(results)183 1681 y(for)13 b(single)h(rule)g(systems.)183 1769 y Fd(Prop)q(ositi)o(on)5 b(9.)21 b Fl(The)13 b(TRS)h Fn(S)s Fx(\()p Fm(P)q(;)7 b Fn(Q)796 1775 y Fw(1)814 1769 y Fx(\))14 b Fl(is)f(acyclic.)g(It)g (is)h(non-lo)n(oping)g(if)f(and)h(only)g(if)f Fm(P)183 1819 y Fl(admits)h(no)i(solution.)183 1907 y(Pr)n(o)n(of.)k Fx(Acyclicit)o(y)h(is)g(ob)o(vious.)g(If)g Fm(P)27 b Fx(has)21 b(a)g(solution)g(then)h Fn(U)t Fx(\()p Fm(P)q(;)7 b Fn(Q)1353 1913 y Fw(1)1371 1907 y Fx(\))22 b(is)f(cyclic)h(b)o(y)183 1957 y(Prop.)13 b(2.)f(According)i(to)f(Prop.)g(7)g Fn(S)s Fx(\()p Fm(P)q(;)7 b Fn(Q)860 1963 y Fw(1)879 1957 y Fx(\))13 b(is)g(lo)q(oping.)f(Con)o(v)o(ersely)m(,)g(if)h Fm(P)18 b Fx(has)c(no)f(solu-)183 2007 y(tion)h(then)h Fn(S)s Fx(\()p Fm(P)q(;)7 b Fn(Q)489 2013 y Fw(1)508 2007 y Fx(\))15 b(is)f(totally)g(terminating)f(and)i(hence)h(non-lo)q (oping)d(b)o(y)i(Theorem)f(5)183 2056 y(and)f(Prop.)h(6.)1186 b Fn(u)-28 b(t)183 2144 y Fd(Prop)q(ositi)o(on)5 b(10.)21 b Fl(The)f(TRS)g Fn(S)s Fx(\()p Fm(P)q(;)7 b Fn(Q)833 2150 y Fw(2)852 2144 y Fx(\))20 b Fl(is)g(non-lo)n(oping.)h(It)f(is)g (terminating)g(if)g(and)183 2194 y(only)15 b(if)f Fm(P)20 b Fl(admits)15 b(no)h(solution.)183 2282 y(Pr)n(o)n(of.)k Fx(Assume)g Fn(S)s Fx(\()p Fm(P)q(;)7 b Fn(Q)598 2288 y Fw(2)616 2282 y Fx(\))21 b(admits)e(a)h(lo)q(op.)g(By)g(Prop.)h(6)f (one)h(obtains)f(a)g(lo)q(op,)g(sa)o(y)183 2332 y Fm(t)c Fn(!)256 2317 y Fw(+)298 2332 y Fm(C)s Fx([)p Fm(t\033)q Fx(],)f(in)h Fn(U)t Fx(\()p Fm(P)q(;)7 b Fn(Q)600 2338 y Fw(2)618 2332 y Fx(\).)16 b(De\014ne)i(the)f(linear)f(in)o (terpretation)h Fm( )h Fx(b)o(y)e Fm( )q Fx(\()p Fm(b)p Fx(\()p Fm(t)p Fx(\)\))h(=)f Fm( )q Fx(\()p Fm(t)p Fx(\))183 2382 y(and)10 b Fm( )q Fx(\()p Fm(f)t Fx(\()p Fm(t)359 2388 y Fw(1)379 2382 y Fm(;)d(:)g(:)g(:)e(;)i(t)487 2388 y Fv(k)507 2382 y Fx(\)\))12 b(=)f Fm( )q Fx(\()p Fm(t)653 2388 y Fw(1)673 2382 y Fx(\))r(+)r Fn(\001)c(\001)g(\001)q Fx(+)r Fm( )q Fx(\()p Fm(t)869 2388 y Fv(k)891 2382 y Fx(\))r(+)r(1.)j(for)g(ev)o(ery)h(other)g(function)f(sym)o(b)q(ol)f Fm(f)15 b Fx(of)183 2432 y(arit)o(y)d Fm(k)q Fx(.)h(Clearly)m(,)f Fm(s)g Fn(!)554 2439 y Fi(U)s Fw(\()p Fv(P)q(;)p Fi(Q)650 2443 y Fa(2)666 2439 y Fw(\))692 2432 y Fm(s)711 2417 y Fi(0)737 2432 y Fx(implies)f Fm( )q Fx(\()p Fm(s)p Fx(\))i Fn(\025)f Fm( )q Fx(\()p Fm(s)1076 2417 y Fi(0)1088 2432 y Fx(\))i(for)f(all)f(terms)h Fm(s)h Fx(and)f Fm(s)1485 2417 y Fi(0)1497 2432 y Fx(,)g(hence)893 2556 y(9)p eop %%Page: 10 10 10 9 bop 340 194 a Fm(C)15 b Fx(consists)f(of)e Fm(b)g Fx(sym)o(b)q(ols)f(only)m(.)f(De\014ne)k(another)e(linear)g(in)o (terpretation)h Fm(\036)f Fx(b)o(y)g Fm(\036)p Fx(\()p Fm(b)p Fx(\()p Fm(t)p Fx(\)\))g(=)340 244 y Fm(\036)p Fx(\()p Fm(t)p Fx(\))d(+)g(1)k(and)h Fm(\036)p Fx(\()p Fm(f)t Fx(\()p Fm(t)673 250 y Fw(1)692 244 y Fm(;)7 b(:)g(:)g(:)e(;)i (t)800 250 y Fv(k)820 244 y Fx(\)\))12 b(=)f(0)j(for)f(ev)o(ery)h (other)h(function)e(sym)o(b)q(ol)f(of)h(arit)o(y)g Fm(k)q Fx(.)g(F)m(or)340 293 y(all)i(terms)h Fm(s)h Fx(and)f Fm(s)656 278 y Fi(0)668 293 y Fx(,)f(if)h Fm(s)f Fn(!)812 300 y Fi(U)s Fw(\()p Fv(P)q(;)p Fi(Q)908 304 y Fa(2)924 300 y Fw(\))954 293 y Fm(s)973 278 y Fi(0)1001 293 y Fx(then)i Fm(\036)p Fx(\()p Fm(s)p Fx(\))f(=)g Fm(\036)p Fx(\()p Fm(s)1298 278 y Fi(0)1309 293 y Fx(\),)g(hence)i Fm(C)g Fx(is)e(empt)o(y)m(.)f(No)o(w)340 343 y(the)g(lo)q(op)e(m)o(ust) g(b)q(e)i(of)e(the)i(shap)q(e)f Fm(D)q Fx([)p Fm(A)p Fx(\()p Fm(V)r(;)7 b(W)o(;)g(u)p Fx(\)])k Fn(!)1199 328 y Fw(+)1238 343 y Fm(D)q Fx([)p Fm(A)p Fx(\()p Fm(V)f(\033)o(;)d(W)f (\033)o(;)h(u\033)q Fx(\)])12 b(where)j Fm(D)g Fx(is)340 393 y(a)i(con)o(text)g(not)g(con)o(taining)e(an)o(y)i Fm(A)f Fx(sym)o(b)q(ol.)f(Then)i Fm(A)p Fx(\()p Fm(V)r(;)7 b(W)o(;)g(u)p Fx(\))16 b Fn(!)1453 378 y Fw(+)1496 393 y Fm(A)p Fx(\()p Fm(V)10 b(\033)o(;)d(W)f(\033)o(;)h(u\033)q Fx(\).)340 443 y(Since)18 b Fm(A)p Fx(\()p Fm(V)r(;)7 b(W)o(;)g(u)p Fx(\))17 b Fn(!)700 425 y Fw(+)700 457 y Fi(U)s Fw(\()p Fv(P)q(;)p Fi(;)p Fw(\))818 443 y Fm(A)p Fx(\()p Fm(V)10 b(\033)o(;)d(W)f(\033)o(;)h(u\033)q Fx(\))16 b(w)o(ould)h(con)o(tradict)g(Prop.)h(4,)e(w)o(e)i(obtain)340 504 y Fm(u)12 b Fn(!)418 486 y Fw(+)418 516 y Fi(Q)445 520 y Fa(2)474 504 y Fm(u\033)j Fx(b)o(y)f(Prop.)f(3.)g(This)h(is)g (imp)q(ossible)e(since)j Fn(Q)1229 510 y Fw(2)1261 504 y Fx(is)f(non-lo)q(oping)e([19)o(].)403 554 y(No)o(w)i(let)g Fm(P)20 b Fx(ha)o(v)o(e)15 b(a)f(solution.)f(There)j(exists)f(an)f (in\014nite)h Fn(Q)1376 560 y Fw(2)1394 554 y Fx(-reduction)g Fm(t)1608 560 y Fw(1)1640 554 y Fn(!)d Fm(t)1709 560 y Fw(2)1740 554 y Fn(!)340 604 y Fm(t)355 610 y Fw(3)386 604 y Fn(!)f(\001)c(\001)g(\001)17 b Fx(in)11 b(whic)o(h)h(all)f(steps) j(tak)o(e)e(place)g(at)g(the)g(ro)q(ot)h(p)q(osition.)d(With)i(help)g (of)f(Props.)i(2)340 653 y(and)h(7)g(this)g(sequence)i(is)d (transformed)h(in)o(to)f(an)g(in\014nite)h Fn(S)s Fx(\()p Fm(P)q(;)7 b Fn(Q)1390 659 y Fw(2)1408 653 y Fx(\)-reduction)411 733 y Fm(A)p Fx(\()p Fm(V)r(;)g(W)o(;)g(t)575 739 y Fw(1)593 733 y Fx(\))12 b Fn(!)663 716 y Fw(+)702 733 y Fm(C)732 739 y Fw(1)750 733 y Fx([)p Fm(A)p Fx(\()p Fm(V)r(;)7 b(W)o(;)g(t)926 739 y Fw(2)944 733 y Fx(\)])k Fn(!)1025 716 y Fw(+)1064 733 y Fm(C)1094 739 y Fw(2)1112 733 y Fx([)p Fm(A)p Fx(\()p Fm(V)r(;)c(W)o(;)g(t)1288 739 y Fw(3)1306 733 y Fx(\)])k Fn(!)g(\001)c(\001)g(\001)340 813 y Fx(Con)o(v)o(ersely)m(,)13 b(if)g Fm(P)19 b Fx(has)13 b(no)g(solution)g(then)h Fn(S)s Fx(\()p Fm(P)q(;)7 b Fn(Q)1148 819 y Fw(2)1166 813 y Fx(\))14 b(is)f(totally)f(terminating)g (and)h(there-)340 863 y(fore)h(terminating)e(b)o(y)i(Theorem)g(5)f(and) h(Prop.)g(6.)610 b Fn(u)-28 b(t)340 950 y Fd(Prop)q(osition)5 b(11.)20 b Fl(The)15 b(TRS)g Fn(S)s Fx(\()p Fm(P)q(;)7 b Fn(Q)980 956 y Fw(3)998 950 y Fx(\))15 b Fl(is)f(terminating.)g(It)g (is)h(non-self-emb)n(e)n(dding)g(if)340 1000 y(and)h(only)f(if)f Fm(P)21 b Fl(admits)14 b(no)i(solution.)340 1087 y(Pr)n(o)n(of.)k Fx(W)m(e)9 b(pro)o(v)o(e)h(that)f Fn(U)t Fx(\()p Fm(P)q(;)e Fn(Q)857 1093 y Fw(3)875 1087 y Fx(\))i(is)h(terminating,)d(from)g (whic)o(h)i(termination)f(of)g Fn(S)s Fx(\()p Fm(P)q(;)f Fn(Q)1767 1093 y Fw(3)1786 1087 y Fx(\))340 1137 y(follo)o(ws)j(b)o(y)g (Prop.)h(6.)f(W)m(e)g(use)i(seman)o(tic)e(lab)q(elling)f(\([20)o(]\).)h (As)i(a)e(mo)q(del)g(w)o(e)h(c)o(ho)q(ose)g Fn(f)p Fx(0)p Fm(;)c Fx(1)p Fn(g)p Fx(,)340 1187 y(where)15 b Fm(g)g Fx(is)f(in)o(terpreted)i(as)d(the)i(iden)o(tit)o(y)m(,)d Fm(h)i Fx(as)g(b)q(eing)g(constan)o(t)g(0,)f(and)h(all)e(other)j(sym-) 340 1237 y(b)q(ols)f(as)g(b)q(eing)g(constan)o(t)h(1.)e(Lab)q(el)h(the) g(sym)o(b)q(ol)e Fm(A)i Fx(b)o(y)g(the)h(v)n(alue)e(of)g(its)h(last)g (argumen)o(t.)340 1287 y(According)g(to)f(the)h(main)d(result)j(of)e (seman)o(tic)h(lab)q(elling)e(then)j Fn(U)t Fx(\()p Fm(P)q(;)7 b Fn(Q)1481 1293 y Fw(3)1499 1287 y Fx(\))13 b(is)g(terminating)340 1336 y(if)e(and)g(only)g(if)p 579 1300 162 2 v 11 w Fn(U)t Fx(\()p Fm(P)q(;)c Fn(Q)706 1342 y Fw(3)724 1336 y Fx(\))12 b(is)f(terminating,)e(where)p 1144 1300 V 13 w Fn(U)t Fx(\()p Fm(P)q(;)e Fn(Q)1271 1342 y Fw(3)1289 1336 y Fx(\))12 b(is)f(obtained)g(from)f Fn(U)t Fx(\()p Fm(P)q(;)d Fn(Q)1747 1342 y Fw(3)1765 1336 y Fx(\))340 1386 y(b)o(y)15 b(replacing)h(the)f Fm(A)h Fx(sym)o(b)q(ols)e(in)g(the)i(righ)o(t-hand) f(sides)h(of)f(the)h(t)o(yp)q(e)f(\(4\))h(rules)g(b)o(y)f Fm(A)1763 1392 y Fw(0)340 1436 y Fx(and)c(all)f(other)i Fm(A)g Fx(sym)o(b)q(ols)d(b)o(y)i Fm(A)863 1442 y Fw(1)882 1436 y Fx(.)g(No)o(w)g(the)g(n)o(um)o(b)q(er)g(of)g Fm(A)1290 1442 y Fw(1)1319 1436 y Fx(sym)o(b)q(ols)f(strictly)i(decreases)340 1486 y(b)o(y)j(applying)e(a)h(t)o(yp)q(e)h(\(4\))f(rule)h(from)p 948 1450 V 13 w Fn(U)t Fx(\()p Fm(P)q(;)7 b Fn(Q)1075 1492 y Fw(3)1093 1486 y Fx(\),)14 b(while)g(it)g(remains)f(constan)o(t) i(b)o(y)f(apply-)340 1536 y(ing)f(an)o(y)g(other)h(rule.)g(Hence)h(an)e (in\014nite)p 1010 1500 V 13 w Fn(U)t Fx(\()p Fm(P)q(;)7 b Fn(Q)1137 1542 y Fw(3)1155 1536 y Fx(\)-reduction)14 b(giv)o(es)g(rise)g(to)f(an)g(in\014nite)p 340 1549 V 340 1586 a Fn(U)t Fx(\()p Fm(P)q(;)7 b Fn(Q)467 1592 y Fw(3)485 1586 y Fx(\))q(-reduction)13 b(without)f(application)f(of)h (t)o(yp)q(e)h(\(4\))f(rules.)h(By)f(omitting)e(the)j(lab)q(els)340 1635 y(this)h(giv)o(es)g(an)g(in\014nite)f Fn(U)t Fx(\()p Fm(P)q(;)7 b Fn(;)p Fx(\)-reduction,)14 b(con)o(tradicting)f(Prop.)h (4.)403 1685 y(If)9 b Fm(P)14 b Fx(has)c(a)f(solution)f(then)i(w)o(e)f (obtain)g Fm(A)p Fx(\()p Fm(V)r(;)e(W)o(;)g(g)q Fx(\()p Fm(d)p Fx(\)\))12 b Fn(!)1298 1667 y Fw(+)1298 1699 y Fi(S)r Fw(\()p Fv(P)q(;)p Fi(Q)1392 1703 y Fa(3)1408 1699 y Fw(\))1434 1685 y Fm(C)s Fx([)p Fm(A)p Fx(\()p Fm(V)r(;)7 b(W)o(;)g(g)q Fx(\()p Fm(h)p Fx(\()p Fm(d)p Fx(\)\)\)])340 1742 y(from)j(Props.)h(2)g(and)g(7.)f(Since)i Fm(A)p Fx(\()p Fm(V)r(;)7 b(W)o(;)g(g)q Fx(\()p Fm(d)p Fx(\)\))k(is)g(em)o(b)q(edded)g(in)g Fm(C)s Fx([)p Fm(A)p Fx(\()p Fm(V)r(;)c(W)o(;)g(g)q Fx(\()p Fm(h)p Fx(\()p Fm(d)p Fx(\)\)\)])j(this)340 1792 y(sho)o(ws)19 b(that)g Fn(S)s Fx(\()p Fm(P)q(;)7 b Fn(Q)684 1798 y Fw(3)702 1792 y Fx(\))19 b(is)f(self-em)o(b)q(edding.)f(Con)o(v)o(ersely)m(,)h (if)f Fm(P)24 b Fx(has)19 b(no)f(solution)g(then)340 1841 y Fn(S)s Fx(\()p Fm(P)q(;)7 b Fn(Q)465 1847 y Fw(3)484 1841 y Fx(\))13 b(is)h(totally)e(terminating)g(and)h(th)o(us)h (non-self-em)o(b)q(edding)f(b)o(y)g(Theorem)g(5)g(and)340 1891 y(Prop.)h(6.)1267 b Fn(u)-28 b(t)340 1979 y Fd(Prop)q(osition)5 b(12.)20 b Fl(The)c(TRS)g Fn(S)s Fx(\()p Fm(P)q(;)7 b Fn(Q)982 1985 y Fw(4)1000 1979 y Fx(\))16 b Fl(is)f(non-self-emb)n(e)n (dding.)h(It)g(is)f(simply)g(termi-)340 2028 y(nating)h(if)e(and)i (only)f(if)f Fm(P)20 b Fl(admits)15 b(no)h(solution.)340 2116 y(Pr)n(o)n(of.)k Fx(W)m(e)e(pro)o(v)o(e)f(that)h Fn(U)t Fx(\()p Fm(P)q(;)7 b Fn(Q)882 2122 y Fw(4)900 2116 y Fx(\))17 b(is)h(non-self-em)o(b)q(edding,)d(non-self-em)o(b)q (eddingness)340 2166 y(of)h Fn(S)s Fx(\()p Fm(P)q(;)7 b Fn(Q)515 2172 y Fw(4)533 2166 y Fx(\))16 b(follo)o(ws)f(then)h(b)o(y) g(Prop.)g(6.)f(Supp)q(ose)i(to)f(the)h(con)o(trary)f(that)g Fn(U)t Fx(\()p Fm(P)q(;)7 b Fn(Q)1703 2172 y Fw(4)1721 2166 y Fx(\))16 b(is)340 2215 y(self-em)o(b)q(edding.)d(Using)g(a)h (standard)g(minima)o(li)o(t)o(y)d(argumen)o(t)i(w)o(e)h(obtain)411 2295 y Fm(t)d Fx(=)h Fm(A)p Fx(\()p Fm(V)r(;)7 b(W)o(;)g(g)q Fx(\()p Fm(d;)g(e;)g(t)761 2278 y Fi(0)772 2295 y Fx(\)\))12 b Fn(!)858 2277 y Fw(+)858 2309 y Fi(U)s Fw(\()p Fv(P)q(;)p Fi(Q)954 2313 y Fa(4)969 2309 y Fw(\))996 2295 y Fm(u)f Fx(=)h Fm(A)p Fx(\()p Fm(V)r(;)7 b(W)1212 2278 y Fi(0)1224 2295 y Fm(;)g(v)q Fx(\))12 b Fn(!)1334 2278 y Fi(\003)1334 2305 y(E)m Fg(mb)1405 2295 y Fm(t)340 2382 y Fx(suc)o(h)18 b(that)e Fm(t)h Fx(con)o(tains)f(only)g(one)h Fm(A)f Fx(sym)o(b)q(ol.)f(Hence)j(rules)f(in)f Fn(E)m Fl(mb)p Fx(\()p Fn(f)p Fm(A)p Fn(g)p Fx(\))g(are)h(not)g(ap-)340 2432 y(plied.)j(So)g Fm(W)569 2417 y Fi(0)603 2432 y Fn(!)645 2417 y Fi(\003)645 2443 y(E)m Fg(mb)727 2432 y Fm(W)26 b Fx(and)20 b Fm(v)k Fn(!)965 2417 y Fi(\003)965 2443 y(E)m Fg(mb)1047 2432 y Fm(g)q Fx(\()p Fm(d;)7 b(e;)g(t)1178 2417 y Fi(0)1189 2432 y Fx(\))20 b(m)o(ust)g(hold.)f(By)h(Prop.)g(3)g (either)1040 2556 y(10)p eop %%Page: 11 11 11 10 bop 183 194 a Fm(g)q Fx(\()p Fm(d;)7 b(e;)g(t)314 179 y Fi(0)325 194 y Fx(\))15 b Fn(!)398 176 y Fw(+)398 206 y Fi(Q)425 210 y Fa(4)459 194 y Fm(v)j Fx(or)f Fm(A)p Fx(\()p Fm(V)r(;)7 b(W)o(;)g(g)q Fx(\()p Fm(d;)g(e;)g(t)831 179 y Fi(0)841 194 y Fx(\)\))16 b Fn(!)931 176 y Fw(+)931 208 y Fi(U)s Fw(\()p Fv(P)q(;)p Fi(;)p Fw(\))1047 194 y Fm(A)p Fx(\()p Fm(V)r(;)7 b(W)1184 179 y Fi(0)1196 194 y Fm(;)g(g)q Fx(\()p Fm(d;)g(e;)g(t)1346 179 y Fi(0)1357 194 y Fx(\)\).)16 b(The)h(former)183 248 y(con)o(tradicts)d(the)g (non-self-em)o(b)q(eddingness)g(of)f Fn(Q)986 254 y Fw(4)1018 248 y Fx(and)g(the)h(latter)g(simple)e(termination)183 298 y(of)h Fn(U)t Fx(\()p Fm(P)q(;)7 b Fn(;)p Fx(\))13 b(\(Prop.)h(4\).)245 348 y(If)j Fm(P)23 b Fx(has)17 b(a)h(solution)e (then)i(with)f(help)h(of)f(Props.)g(2)g(and)h(7)f(w)o(e)h(obtain)e(the) i(cyclic)183 398 y Fn(S)s Fx(\()p Fm(P)q(;)7 b Fn(Q)308 404 y Fw(4)326 398 y Fx(\))i Fn([)g(E)m Fl(mb)p Fx(\()p Fn(F)506 404 y Fi(U)541 398 y Fn([)g(F)608 404 y Fi(Q)637 398 y Fx(\)-reduction)253 486 y Fm(A)p Fx(\()p Fm(V)r(;)e(W)o(;)g(g)q Fx(\()p Fm(d;)g(e;)g(d)p Fx(\)\))k Fn(!)625 469 y Fw(+)663 486 y Fm(C)693 492 y Fw(1)712 486 y Fx([)p Fm(A)p Fx(\()p Fm(V)r(;)c(W)o(;)g(g)q Fx(\()p Fm(d;)g(h)p Fx(\()p Fm(e)p Fx(\))p Fm(;)g(e)p Fx(\)\)])12 b Fn(!)1162 469 y Fw(+)1201 486 y Fm(A)p Fx(\()p Fm(V)r(;)7 b(W)o(;)g(g)q Fx(\()p Fm(d;)g(e;)g(e)p Fx(\)\))583 553 y Fn(!)625 536 y Fw(+)663 553 y Fm(C)693 559 y Fw(2)712 553 y Fx([)p Fm(A)p Fx(\()p Fm(V)r(;)g(W)o(;)g(g)q Fx(\()p Fm(h)p Fx(\()p Fm(d)p Fx(\))p Fm(;)g(e;)g(d)p Fx(\)\)])i Fn(!)1162 536 y Fw(+)1201 553 y Fm(A)p Fx(\()p Fm(V)r(;)e(W)o(;)g(g)q Fx(\()p Fm(d;)g(e;)g(d)p Fx(\)\))p Fm(:)183 629 y Fx(So)20 b(in)g(this)h(case)g Fn(S)s Fx(\()p Fm(P)q(;)7 b Fn(Q)609 635 y Fw(4)627 629 y Fx(\))21 b(is)f(not)h(simply)d(terminating.)h(Con)o(v)o(ersely)m(,)g (if)h Fm(P)26 b Fx(has)21 b(no)183 679 y(solution)14 b(then)j Fn(S)s Fx(\()p Fm(P)q(;)7 b Fn(Q)563 685 y Fw(4)581 679 y Fx(\))15 b(is)h(totally)e(terminating)g(and)h(hence)i(simply)d (terminating)g(b)o(y)183 729 y(Theorem)f(5)h(and)f(Prop.)h(6.)976 b Fn(u)-28 b(t)183 809 y Fd(Prop)q(ositi)o(on)5 b(13.)21 b Fl(The)15 b(TRS)i Fn(S)s Fx(\()p Fm(P)q(;)7 b Fn(Q)825 815 y Fw(5)843 809 y Fx(\))16 b Fl(is)f(simply)h(terminating.)f(It)h (is)f(total)r(ly)h(termi-)183 859 y(nating)f(if)f(and)i(only)f(if)f Fm(P)21 b Fl(admits)14 b(no)i(solution.)183 939 y(Pr)n(o)n(of.)k Fx(If)g Fm(P)26 b Fx(has)21 b(no)f(solution)g(then)h(total)f (termination)f(of)g Fn(S)s Fx(\()p Fm(P)q(;)7 b Fn(Q)1341 945 y Fw(5)1360 939 y Fx(\))20 b(follo)o(ws)f(from)183 989 y(Theorem)f(5)g(in)g(conjunction)g(with)g(Prop.)g(6.)g(It)g (remains)g(to)g(sho)o(w)h(that)f Fn(S)s Fx(\()p Fm(P)q(;)7 b Fn(Q)1543 995 y Fw(5)1561 989 y Fx(\))19 b(is)183 1039 y(simply)13 b(terminating)h(but)h(not)g(totally)g(terminating)e(whenev) o(er)k Fm(P)k Fx(has)15 b(a)g(solution.)f(By)183 1089 y(Prop.)f(6,)g(it)h(is)g(su\016cien)o(t)g(to)g(sho)o(w)g(this)g(for)f Fn(U)t Fx(\()p Fm(P)q(;)7 b Fn(Q)p Fx(\).)245 1139 y(Let)21 b Fm(P)26 b Fx(ha)o(v)o(e)20 b(a)h(solution.)e(An)o(y)i(in\014nite)f Fn(U)t Fx(\()p Fm(P)q(;)7 b Fn(Q)1068 1145 y Fw(5)1086 1139 y Fx(\)-reduction)21 b(w)o(ould)f(b)o(y)h(Prop)q(o-)183 1189 y(sition)f(3)g(imply)e(an)j(in\014nite)f Fn(Q)713 1195 y Fw(5)732 1189 y Fx(-reduction,)h(con)o(tradicting)f(termination) f(of)h Fn(Q)1529 1195 y Fw(5)1548 1189 y Fx(.)g(So)183 1238 y Fn(U)t Fx(\()p Fm(P)q(;)7 b Fn(Q)310 1244 y Fw(5)328 1238 y Fx(\))12 b(is)h(terminating)d(and,)i(since)h(it)f(is)h(length)f (preserving,)h(ev)o(en)g(simply)e(terminat-)183 1288 y(ing.)h(Supp)q(ose)j Fn(U)t Fx(\()p Fm(P)q(;)7 b Fn(Q)553 1294 y Fw(5)571 1288 y Fx(\))14 b(is)g(totally)e(terminating.)g(With)h (help)h(of)f(Prop.)h(2)g(w)o(e)g(conclude)183 1338 y(the)20 b(existence)h(of)d(a)i(total)e(reduction)i(order)g Fm(>)g Fx(suc)o(h)g(that)f(b)q(oth)h Fm(A)p Fx(\()p Fm(V)r(;)7 b(W)o(;)g(g)q Fx(\()p Fm(d;)g(e)p Fx(\)\))20 b Fm(>)183 1388 y(A)p Fx(\()p Fm(V)r(;)7 b(W)o(;)g(g)q Fx(\()p Fm(e;)g(e)p Fx(\)\))17 b(and)f Fm(A)p Fx(\()p Fm(V)r(;)7 b(W)o(;)g(g)q Fx(\()p Fm(d;)g(e)p Fx(\)\))15 b Fm(>)h(A)p Fx(\()p Fm(V)r(;)7 b(W)o(;)g(g)q Fx(\()p Fm(d;)g(d)p Fx(\)\).)15 b(By)i(the)g(truncation)f (rule)183 1438 y(for)11 b(total)f(reduction)j(orders)f Fm(>)g Fx(in)f(Zan)o(tema)f([17)o(])h(one)h(ma)o(y)e(remo)o(v)o(e)g (the)i(con)o(text)g Fm(C)i Fx(from)183 1487 y(an)i(inequation)g Fm(C)s Fx([)p Fm(t)p Fx(])e Fm(>)j(C)s Fx([)p Fm(t)645 1472 y Fi(0)655 1487 y Fx(].)f(By)h(doing)e(this)i(for)f(the)h(con)o (texts)h Fm(A)p Fx(\()p Fm(V)r(;)7 b(W)o(;)g(g)q Fx(\()p 1457 1487 13 2 v 15 w Fm(;)g(e)p Fx(\)\))17 b(and)183 1537 y Fm(A)p Fx(\()p Fm(V)r(;)7 b(W)o(;)g(g)q Fx(\()p Fm(d;)p 411 1537 V 21 w Fx(\)\))13 b(w)o(e)h(get)g Fm(d)d(>)h(e)h Fx(and)g Fm(e)f(>)g(d)p Fx(,)h(whic)o(h)g(con)o(tradicts)h(the)g (irre\015exivit)o(y)f(of)g Fm(>)p Fx(.)183 1587 y(So)g Fn(U)t Fx(\()p Fm(P)q(;)7 b Fn(Q)367 1593 y Fw(5)385 1587 y Fx(\))14 b(cannot)g(b)q(e)h(totally)d(terminating.)630 b Fn(u)-28 b(t)245 1667 y Fx(Of)9 b(course)i(the)f(question)f(emerges)h (whether)g(the)g(next)g(implication)c(|)j Fm(!)q Fx(-termination)183 1717 y(=)-7 b Fn(\))12 b Fx(total)g(termination)f(|)h(is)h(undecidable) g(ev)o(en)g(for)g(single)f(rule)h(TRSs.)f(It)h(is)g(not)f(hard)183 1767 y(to)i(enco)q(de)h(the)g(implication)c(in)j(a)g(suitable)g(TRS)g Fn(Q)1031 1773 y Fw(6)1049 1767 y Fx(,)g(but)g(one)h(needs)g(the)g (stronger)g(re-)183 1817 y(sult)g(of)f Fm(!)q Fx(-termination)f(in)h (Theorem)h(5.)f(In)h(the)g(full)f(v)o(ersion)h([10)o(],)f(w)o(e)h (presen)o(t)h(a)f(pro)q(of)183 1867 y(in)h Fm(!)261 1851 y Fw(4)280 1867 y Fx(.)g(T)m(rying)g(hard)h(w)o(e)g(ha)o(v)o(e)f(also)g (established)i(a)e(termination)f(pro)q(of)i(in)f Fm(!)1465 1851 y Fw(2)1501 1867 y Fx(but)h(no)183 1916 y(pro)q(of)c(in)h Fm(!)q Fx(.)f(So)h(the)g(question)h(remains)d(op)q(en.)183 2042 y Fo(Conclusion)183 2133 y Fx(W)m(e)k(ha)o(v)o(e)g(sho)o(wn)h (that)g(the)g(lo)o(w)o(er)f(\014v)o(e)h(lev)o(els)f(of)g(the)i (termination)d(hierarc)o(h)o(y)h(are)i(rel-)183 2183 y(ativ)o(ely)c(undecidable)h(ev)o(en)h(for)e(single)h(rules.)g(These)i (results)f(sho)o(ws)f(ho)o(w)g(di\016cult)f(it)h(is)183 2232 y(in)g(general)h(to)g(detect)i(one)e(of)g(the)g(prop)q(erties)i (in)d(the)i(termination)d(hierarc)o(h)o(y)m(.)h(A)h(con-)183 2282 y(sequence)g(of)e(our)h(w)o(ork)f(is)h(the)g(imp)q(ossibilit)o(y)d (of)i(extending)h(metho)q(ds)f(for)g(establishing)183 2332 y(total)d(termination,)e(lik)o(e)j(recursiv)o(e)h(path)f(orders)h (and)f(Kn)o(uth-Bendix)g(orders,)h(to)e(a)h(lev)o(el)183 2382 y(where)j(total)f(termination)f(can)h(alw)o(a)o(ys)g(b)q(e)h (detected.)h(This)e(ev)o(en)h(holds)f(if)g(only)g(simply)183 2432 y(terminating)e(single)h(rewrite)i(rules)g(are)f(allo)o(w)o(ed)f (as)h(input)f(for)h(the)g(metho)q(d.)882 2556 y(11)p eop %%Page: 12 12 12 11 bop 340 194 a Fo(References)360 289 y Ft(1.)20 b(M.)12 b(Dauc)o(het.)18 b(Sim)o(ulation)d(of)d(Turing)i(mac)o(hines)g (b)o(y)e(a)h(regular)g(rewrite)g(rule.)18 b Fr(The)n(or)n(etic)n(al)410 335 y(Computer)13 b(Scienc)n(e)p Ft(,)d(103\(2\):409{420,)k(1992.)360 380 y(2.)20 b(N.)14 b(Dersho)o(witz.)24 b(T)m(ermination)17 b(of)d(rewriting.)24 b Fr(Journal)14 b(of)h(Symb)n(olic)e(Computation)p Ft(,)f(3\(1)410 426 y(&)h(2\):69{116,)g(1987.)360 472 y(3.)20 b(N.)12 b(Dersho)o(witz)h(and)g(J.-P)m(.)d(Jouannaud.)19 b(Rewrite)12 b(systems.)17 b(In)c Fr(Handb)n(o)n(ok)c(of)k(The)n(or)n (etic)n(al)410 517 y(Computer)g(Scienc)n(e)p Ft(,)d(v)o(olume)k(B,)f (pages)h(243{320.)g(Elsevier,)g(1990.)360 563 y(4.)20 b(N.)c(Dersho)o(witz,)h(J.-P)m(.)e(Jouannaud,)j(and)f(J.W.)e(Klop.)28 b(Problems)18 b(in)f(rewriting)h(I)q(I)q(I.)26 b(In)410 609 y Fr(Pr)n(o)n(c.)13 b(6th)g(R)m(T)m(A)p Ft(,)f(v)o(olume)j(914)e (of)g Fr(LNCS)p Ft(,)f(pages)i(457{471,)f(1995.)360 654 y(5.)20 b(M.)11 b(F)m(erreira.)17 b Fr(T)m(ermination)10 b(of)h(term)g(r)n(ewriting)g({)g(wel)r(l-founde)n(dne)o(ss,)d (totality,)h(and)i(tr)n(ans-)410 700 y(formations)p Ft(.)k(PhD)e (thesis,)h(Univ)o(ersit)o(y)h(of)e(Utrec)o(h)o(t,)f(1995.)360 746 y(6.)20 b(M.)13 b(F)m(erreira)h(and)g(H.)f(Zan)o(tema.)19 b(Dumm)o(y)14 b(elimination)q(:)i(Making)f(termination)g(easier.)k(In) 410 791 y Fr(Pr)n(o)n(c.)13 b(10th)f(F)o(CT)p Ft(,)i(v)o(olume)g(965,)f (pages)h(243{252,)g(1995.)360 837 y(7.)20 b(M.)e(F)m(erreira)h(and)g (H.)e(Zan)o(tema.)34 b(T)m(otal)18 b(termination)j(of)d(term)g (rewriting.)34 b Fr(Applic)n(able)410 883 y(A)o(lgebr)n(a)12 b(in)h(Engine)n(ering,)e(Communic)n(ation)g(and)h(Computing)p Ft(,)f(7\(2\):133{162,)j(1996.)360 928 y(8.)20 b(A.)9 b(Geser.)16 b(Omega-termination)c(is)f(undecidable)i(for)d(totally)h (terminating)h(term)e(rewriting)410 974 y(systems.)26 b(T)m(ec)o(hnical)17 b(Rep)q(ort)g(MIP-9608,)e(Univ)o(ersit)o(y)j(of)d (P)o(assau,)i(1996.)25 b(T)m(o)16 b(app)q(ear)g(in)410 1020 y Fr(Journal)c(of)h(Symb)n(olic)f(Computation)p Ft(.)360 1065 y(9.)20 b(A.)g(Geser,)h(A.)f(Middeldorp,)j(E.)d(Ohlebusc) o(h,)i(and)f(H.)f(Zan)o(tema.)41 b(Relativ)o(e)22 b(undecid-)410 1111 y(abilit)o(y)f(in)f(term)e(rewriting.)35 b(In)18 b Fr(Pr)n(o)n(c.)g(CSL)p Ft(,)g(Utrec)o(h)o(t,)g(1996.)34 b(Av)n(ailable)22 b(at)c Fj(http://)410 1157 y(www.score.)o(is.)o(ts)o (uku)o(ba)o(.ac)o(.jp)o(/)p Fp(\030)p Fj(a)o(mi)o(/pa)o(per)o(s/)o(csl) o(96)o(.dv)o(i)p Ft(.)340 1202 y(10.)j(A.)12 b(Geser,)h(A.)f (Middeldorp,)j(E.)e(Ohlebusc)o(h,)h(and)f(H.)f(Zan)o(tema.)18 b(Relativ)o(e)d(undecidabil)q(it)o(y)410 1248 y(in)e(the)g(termination) h(hierarc)o(h)o(y)g(of)e(single)i(rewrite)f(rules.)18 b(T)m(ec)o(hnical)13 b(rep)q(ort,)g(1997.)k(Av)n(ail-)410 1294 y(able)c(at)e Fj(http://www-)o(sr)o(.in)o(fo)o(rma)o(tik)o(.u)o (ni-)o(tu)o(ebi)o(nge)o(n.)o(de/)o Fp(\030)p Fj(ge)o(ser)o(/p)o(ape)o (rs)o(/ca)o(ap)o(97-)410 1339 y(full.dvi)p Ft(.)340 1385 y(11.)21 b(G.)14 b(Huet)g(and)g(D.)g(S.)g(Lankford.)21 b(On)13 b(the)i(uniform)g(halting)h(problem)f(for)f(term)g(rewriting) 410 1431 y(systems.)k(Rapp)q(ort)c(Lab)q(oria)g(283,)f(INRIA,)f(1978.) 340 1476 y(12.)21 b(P)m(.)15 b(Lescanne.)24 b(On)15 b(termination)j(of) d(one)g(rule)h(rewrite)g(systems.)24 b Fr(The)n(or)n(etic)n(al)13 b(Computer)410 1522 y(Scienc)n(e)p Ft(,)d(132:395{401,)k(1994.)340 1568 y(13.)21 b(A.)9 b(Middeldorp)j(and)e(B.)f(Gramlic)o(h.)17 b(Simple)12 b(termination)f(is)f(di\016cult.)17 b Fr(Applic)n(able)7 b(A)o(lgebr)n(a)410 1613 y(in)13 b(Engine)n(ering,)e(Communic)n(ation)g (and)i(Computing)p Ft(,)d(6\(2\):115{128,)k(1995.)340 1659 y(14.)21 b(A.)13 b(Middeldorp)j(and)e(H.)f(Zan)o(tema.)19 b(Simple)c(termination)g(of)f(rewrite)f(systems.)19 b Fr(The)n(or)n(et-)410 1705 y(ic)n(al)13 b(Computer)g(Scienc)n(e)p Ft(,)d(175,)j(1997.)k(T)m(o)c(app)q(ear.)340 1750 y(15.)21 b(Da)o(vid)15 b(Plaisted.)21 b(The)13 b(undecidabi)q(li)q(t)o(y)k(of)c (self-em)o(b)q(edding)j(for)d(term)h(rewriting)h(systems.)410 1796 y Fr(Information)c(Pr)n(o)n(c)n(essing)h(L)n(etters)p Ft(,)f(20:61{64,)i(1985.)340 1842 y(16.)21 b(E.)14 b(P)o(ost.)19 b(A)13 b(v)n(arian)o(t)i(of)f(a)g(recursiv)o(ely)i(unsolv)n(able)h (problem.)j Fr(Bul)r(letin)13 b(of)h(the)f(A)o(meric)n(an)410 1887 y(Mathematic)n(al)e(So)n(ciety)p Ft(,)g(52,)h(1946.)340 1933 y(17.)21 b(H.)14 b(Zan)o(tema.)21 b(T)m(ermination)15 b(of)f(term)g(rewriting:)h(in)o(terpretation)i(and)d(t)o(yp)q(e)h (elimination)q(.)410 1979 y Fr(Journal)d(of)h(Symb)n(olic)f (Computation)p Ft(,)e(17:23{50,)k(1994.)340 2024 y(18.)21 b(H.)12 b(Zan)o(tema.)18 b(T)m(otal)13 b(termination)i(of)e(term)f (rewriting)j(is)e(undecidable.)20 b Fr(Journal)12 b(of)h(Sym-)410 2070 y(b)n(olic)f(Computation)p Ft(,)e(20:43{60,)k(1995.)340 2116 y(19.)21 b(H.)11 b(Zan)o(tema)i(and)g(A.)e(Geser.)17 b(Non-lo)q(oping)d(rewriting.)k(T)m(ec)o(hnical)c(Rep)q(ort)e (UU-CS-1996-)410 2161 y(03,)19 b(Utrec)o(h)o(t)g(Univ)o(ersit)o(y)m(,)i (1996.)36 b(Av)n(ailable)21 b(at)e Fj(ftp://ftp.)o(cs.)o(ruu)o(.n)o (l/p)o(ub)o(/RU)o(U/)o(CS/)410 2207 y(techreps/C)o(S-1)o(99)o(6/1)o(99) o(6-0)o(3.p)o(s.)o(gz)p Ft(.)340 2253 y(20.)i(Hans)13 b(Zan)o(tema.)k(T)m(ermination)d(of)e(term)g(rewriting)h(b)o(y)g(seman) o(tic)g(lab)q(elling)q(.)19 b Fr(F)m(undamenta)410 2298 y(Informatic)n(ae)p Ft(,)10 b(24:89{105,)k(1995.)1040 2556 y Fx(12)p eop %%Trailer end userdict /end-hook known{end-hook}if %%EOF