%!PS-Adobe-2.0 %%Creator: dvips 5.516 Copyright 1986, 1993 Radical Eye Software %%Title: paper.dvi %%CreationDate: Thu Oct 19 10:20:37 1995 %%Pages: 16 %%PageOrder: Ascend %%BoundingBox: 0 0 596 842 %%EndComments %DVIPSCommandLine: dvips paper.dvi -o ../paper.ps %DVIPSSource: TeX output 1995.10.19:1020 %%BeginProcSet: tex.pro /TeXDict 250 dict def TeXDict begin /N{def}def /B{bind def}N /S{exch}N /X{S N}B /TR{translate}N /isls false N /vsize 11 72 mul N /hsize 8.5 72 mul N /landplus90{false}def /@rigin{isls{[0 landplus90{1 -1}{-1 1} ifelse 0 0 0]concat}if 72 Resolution div 72 VResolution div neg scale isls{landplus90{VResolution 72 div vsize mul 0 exch}{Resolution -72 div hsize mul 0}ifelse TR}if Resolution VResolution vsize -72 div 1 add mul TR matrix currentmatrix dup dup 4 get round 4 exch put dup dup 5 get round 5 exch put setmatrix}N /@landscape{/isls true N}B /@manualfeed{ statusdict /manualfeed true put}B /@copies{/#copies X}B /FMat[1 0 0 -1 0 0]N /FBB[0 0 0 0]N /nn 0 N /IE 0 N /ctr 0 N /df-tail{/nn 8 dict N nn begin /FontType 3 N /FontMatrix fntrx N /FontBBox FBB N string /base X array /BitMaps X /BuildChar{CharBuilder}N /Encoding IE N end dup{/foo setfont}2 array copy cvx N load 0 nn put /ctr 0 N[}B /df{/sf 1 N /fntrx FMat N df-tail}B /dfs{div /sf X /fntrx[sf 0 0 sf neg 0 0]N df-tail}B /E{ pop nn dup definefont setfont}B /ch-width{ch-data dup length 5 sub get} B /ch-height{ch-data dup length 4 sub get}B /ch-xoff{128 ch-data dup length 3 sub get sub}B /ch-yoff{ch-data dup length 2 sub get 127 sub}B /ch-dx{ch-data dup length 1 sub get}B /ch-image{ch-data dup type /stringtype ne{ctr get /ctr ctr 1 add N}if}B /id 0 N /rw 0 N /rc 0 N /gp 0 N /cp 0 N /G 0 N /sf 0 N /CharBuilder{save 3 1 roll S dup /base get 2 index get S /BitMaps get S get /ch-data X pop /ctr 0 N ch-dx 0 ch-xoff ch-yoff ch-height sub ch-xoff ch-width add ch-yoff setcachedevice ch-width ch-height true[1 0 0 -1 -.1 ch-xoff sub ch-yoff .1 add]{ ch-image}imagemask restore}B /D{/cc X dup type /stringtype ne{]}if nn /base get cc ctr put nn /BitMaps get S ctr S sf 1 ne{dup dup length 1 sub dup 2 index S get sf div put}if put /ctr ctr 1 add N}B /I{cc 1 add D }B /bop{userdict /bop-hook known{bop-hook}if /SI save N @rigin 0 0 moveto /V matrix currentmatrix dup 1 get dup mul exch 0 get dup mul add .99 lt{/QV}{/RV}ifelse load def pop pop}N /eop{SI restore showpage userdict /eop-hook known{eop-hook}if}N /@start{userdict /start-hook known{start-hook}if pop /VResolution X /Resolution X 1000 div /DVImag X /IE 256 array N 0 1 255{IE S 1 string dup 0 3 index put cvn put}for 65781.76 div /vsize X 65781.76 div /hsize X}N /p{show}N /RMat[1 0 0 -1 0 0]N /BDot 260 string N /rulex 0 N /ruley 0 N /v{/ruley X /rulex X V}B /V {}B /RV statusdict begin /product where{pop product dup length 7 ge{0 7 getinterval dup(Display)eq exch 0 4 getinterval(NeXT)eq or}{pop false} ifelse}{false}ifelse end{{gsave TR -.1 -.1 TR 1 1 scale rulex ruley false RMat{BDot}imagemask grestore}}{{gsave TR -.1 -.1 TR rulex ruley scale 1 1 false RMat{BDot}imagemask grestore}}ifelse B /QV{gsave transform round exch round exch itransform moveto rulex 0 rlineto 0 ruley neg rlineto rulex neg 0 rlineto fill grestore}B /a{moveto}B /delta 0 N /tail{dup /delta X 0 rmoveto}B /M{S p delta add tail}B /b{S p tail} B /c{-4 M}B /d{-3 M}B /e{-2 M}B /f{-1 M}B /g{0 M}B /h{1 M}B /i{2 M}B /j{ 3 M}B /k{4 M}B /w{0 rmoveto}B /l{p -4 w}B /m{p -3 w}B /n{p -2 w}B /o{p -1 w}B /q{p 1 w}B /r{p 2 w}B /s{p 3 w}B /t{p 4 w}B /x{0 S rmoveto}B /y{ 3 2 roll p a}B /bos{/SS save N}B /eos{SS restore}B end %%EndProcSet TeXDict begin 39158280 55380996 1000 300 300 (/amnt/fauna/users/c1t2d0s6/pihiwis/isthesin/hiwi/paper/paper.dvi) @start /Fa 1 98 df<00600000600000F00000F00000F000013800013800013800021C 00021C00040E00040E0007FE000807000807001003801003803803C0FC0FF014137F9217 >97 D E /Fb 2 81 df<018F800631E0084060108070218030610030400030C00030C000 30C00020C00060C00040E000806001007006003C18000FE00014117D9018>79 D<0FFF803181E0418070C180300180300100300300200300600300400301800206000678 000600000400000C000008000018000010000014127F9016>I E /Fc 2 116 df<383C004CC6008F07008E07008E07008E07001C0E001C0E001C0E001C1C 00381C40381C40383840383880701900300E0012107E8F17>110 D<03E006180818183818301C001FC00FE007F000700030E030E030806040C03F000D107E 8F12>115 D E /Fd 51 128 df<0003FE000E03001C0700180600380000380000700000 700000700000700007FFFC00E01C00E03800E03800E03800E03801C07001C07001C07001 C07001C0E403C0E40380E40380E4038068038030030000070000070000660000E60000CC 00007800001821819916>12 D<183C3C1C08080810204080060B78990C>39 D<000400180030006000C0008001800300030006000E000C001C00180018003800300030 0070007000600060006000E000E000E000C000C000C000C000C000600060006000200030 00100008000E267B9B10>I<004000600020003000100018001800180018001800180018 0018001800180018003800380030003000700070006000E000C000C001C0018003800300 060006000C00180010002000400080000D267F9B10>I45 D<000800180030007001F00E7000E000E000E000E001C001C001C001C003800380038003 8007000700070007000F00FFF00D187C9714>49 D<007C00018600020300040380048380 0883801083801083801083801107001207000C0E00001C00003000006000018000020000 0C00001001002001003C060067FE00C1FC0080F00011187D9714>I<003E0000C1000100 800200C00600C00600C00E018007030007860003CC0001F00001F800067C000C3E00180E 00300700600700600700C00600C00600600C006018003070000FC00012187D9714>56 D<007C000186000703000E03000C03801C0380380380380380380380380780380700380F 001817000C270007CE00000E00000C00001C00001800E03000E0600080C000C380003E00 0011187C9714>I<0000200000600000600000E00001E00001E000027000027000047000 087000087000107000107000207000207000407000807000FFF001003801003802003804 00380400380C00381C0038FF01FF181A7E991D>65 D<000F8200706200C01603801E0700 0C0E000C1C000C18000C380008300008700000700000E00000E00000E00000E00000E000 20E00020E00020E000406000406000803001001006000C180003E000171A7A991B>67 D<03FFF80000700E00007007000070030000E0018000E0018000E0018000E001C001C001 C001C001C001C001C001C001C00380038003800380038003800380030007000700070007 0007000E0007000C000E001C000E0038000E0070000E00E0001C038000FFFE00001A1A7D 991D>I<03FFFF00700700700300700100E00100E00100E00100E00101C08001C08001C0 8001C18003FF000381000381000381000702000700040700040700080E00080E00180E00 100E00301C00E0FFFFE0181A7D991A>I<03FF1FF800700380007003800070038000E007 0000E0070000E0070000E0070001C00E0001C00E0001C00E0001C00E0003FFFC0003801C 0003801C0003801C00070038000700380007003800070038000E0070000E0070000E0070 000E0070001C00E000FFC7FE001D1A7D991D>72 D<01FF80003800003800003800007000 00700000700000700000E00000E00000E00000E00001C00001C00001C00001C000038000 0380000380000380000700000700000700000700000E0000FFE000111A7E990F>I<00FF C0000E00000E00000E00001C00001C00001C00001C000038000038000038000038000070 0000700000700000700000E00000E00000E00000E00061C000E1C000E180008380004700 003C0000121A7C9914>I<03FF8000700000700000700000E00000E00000E00000E00001 C00001C00001C00001C0000380000380000380000380000700000700100700100700200E 00200E00600E00400E00C01C0380FFFF80141A7D9918>76 D<03F8001FC00078003C0000 78003C000078005C0000B800B80000B800B800009C013800009C013800011C027000011C 027000011C047000011C087000021C08E000021C10E000021C10E000021C20E000041C41 C000041C41C000041C81C000041C81C000080F038000080F038000080E038000180C0380 00380C070000FF083FF000221A7D9922>I<03F007F8007801C00078008000780080009C 0100009C0100009C0100008E0100010E0200010602000107020001070200020384000203 8400020384000201C4000401C8000401C8000400E8000400E8000800F000080070000800 70001800700038002000FF0020001D1A7D991D>I<001F8000706001C03003001806001C 0E000C1C000C18000E38000E30000E70000E70000EE0001CE0001CE0001CE00038E00038 E00030E00070E000E0E000C06001807003003806001C1C0007E000171A7A991D>I<03FF F800701C00700600700700E00700E00700E00700E00701C00E01C00E01C01C01C0380380 7003FF800380000380000700000700000700000700000E00000E00000E00000E00001C00 00FFC000181A7D991A>I<03FFF000701C00700E00700700E00700E00700E00700E00701 C00E01C01C01C03801C0E003FF800380C00380600380700700700700700700700700700E 00E00E00E00E00E10E00E21C0062FFC03C181A7D991C>82 D<003F100060900180700100 7003002006002006002006002006000007000007C00003F80001FE00007F00000F800003 80000180000180200180200180600300600300600600700C00C8180087E000141A7D9916 >I<3FFFFC381C0C201C04401C0440380480380480380480380400700000700000700000 700000E00000E00000E00000E00001C00001C00001C00001C00003800003800003800003 8000078000FFF800161A79991B>I<7FE0FF0E00380E00100E00101C00201C00201C0020 1C0020380040380040380040380040700080700080700080700080E00100E00100E00100 E00200E00200E004006008006010003860000F8000181A78991D>I87 D<03CC0E2E181C381C301C701CE038 E038E038E038C072C072C07260F261341E180F107C8F14>97 D<7E000E000E000E001C00 1C001C001C00380038003BC03C307830701870187018E038E038E038E038C070C060C0E0 60C063801E000D1A7C9912>I<01F006080C181838301070006000E000E000E000E000E0 08E010602030C01F000D107C8F12>I<001F800003800003800003800007000007000007 00000700000E00000E0003CE000E2E00181C00381C00301C00701C00E03800E03800E038 00E03800C07200C07200C0720060F2006134001E1800111A7C9914>I<01E006181C0838 0870087010FFE0E000E000E000E000E0086010602030C01F000D107C8F12>I<00070000 1980001B80003B0000300000300000700000700000700000700007FF0000E00000E00000 E00000E00000E00001C00001C00001C00001C00001C00003800003800003800003800003 8000070000070000070000660000E40000CC0000700000112181990C>I<00F300038B80 0607000E07000C07001C0700380E00380E00380E00380E00301C00301C00301C00183C00 18780007B800003800003800007000607000E0E000C1C0007F000011177E8F12>I<1F80 000380000380000380000700000700000700000700000E00000E00000E7C000F86001E07 001E07001C07001C0700380E00380E00380E00381C00701C80701C80703880703900E019 00600E00111A7E9914>I<030706000000000000384C4E8E9C9C1C3838707272E2E46438 08197C980C>I<1F8003800380038007000700070007000E000E000E0E0E131C271C431C 801F003C003F8039C038E070E270E270E270E4E0646038101A7E9912>107 D<3F0707070E0E0E0E1C1C1C1C3838383870707070E4E4E4E46830081A7D990A>I<307C 1E00598663009E0783809E0703809C0703809C070380380E0700380E0700380E0700380E 0E00701C0E40701C0E40701C1C40701C1C80E0380C80601807001A107C8F1F>I<307C00 5986009E07009E07009C07009C0700380E00380E00380E00381C00701C80701C80703880 703900E01900600E0011107C8F16>I<01F006180C0C180E300E700E600EE00EE00EE00C E01CE018E030606030C01F000F107C8F14>I<030F000590C009E0C009C06009C06009C0 600380E00380E00380E00380E00701C00701800703800703000E8E000E78000E00000E00 001C00001C00001C00001C0000FF00001317808F14>I<03C20E2E181C381C301C701CE0 38E038E038E038C070C070C07060F061E01EE000E000E001C001C001C001C01FF00F177C 8F12>I<30F059189E389C189C009C0038003800380038007000700070007000E0006000 0D107C8F10>I<03E004300830187018601C001F801FC00FE000E00060E060E06080C041 803E000C107D8F10>I<06000E000E000E000E001C001C00FFC01C003800380038003800 7000700070007000E100E100E100E200640038000A177C960D>I<38064C074E0E8E0E9C 0E9C0E1C1C381C381C381C7039703970393079389A0F0C10107C8F15>I<38184C1C4E1C 8E0C9C0C9C0C1C08380838083808701070107020304018C00F000E107C8F12>I<380C30 4C0E384E1C388E1C189C1C189C1C181C3810383810383810383810707020707020707040 30704018B8800F0F0015107C8F19>I<38064C074E0E8E0E9C0E9C0E1C1C381C381C381C 703870387038307838F00F700070006060E0E1C0C18047003C0010177C8F13>121 D<038207C40FFC10081010002000400180030004000808100820187FF043E081C00F107E 8F10>I<30C071E0F1C061800B04769914>127 D E /Fe 4 55 df<00C00000C00000C000 00C00000C00000C00000C00000C000FFFF80FFFF8000C00000C00000C00000C00000C000 00C00000C00000C00011127E8D15>43 D<18F818181818181818181818FF080D7D8C0E> 49 D<3E00418080C0C0C000C000C0018003000400084030407F80FF800A0D7E8C0E>I<0F 00118021806000C000DE00E180C0C0C0C0C0C060C021801E000A0D7E8C0E>54 D E /Ff 4 111 df<1FFC000603000601800601800C03000C06000FF8000C0C00180C00 180C00180C00180C00300C80FC0700110E7E8D15>82 D<0808000000007098B030306064 6870060F7D8E0B>105 D<00C0008000000000000000000F001180118003000300030003 0006000600060006008C00F0000A137F8E0C>I<73809C40986030C030C030C031886190 60E00D097D8812>110 D E /Fg 6 56 df<1F00618040C08060C0600060006000C00180 030006000C00102020207FC0FFC00B107F8F0F>50 D<1F00218060C060C000C000800180 0F00008000400060C060C060804060801F000B107F8F0F>I<0300030007000F000B0013 00330023004300C300FFE003000300030003001FE00B107F8F0F>I<20803F002C002000 200020002F0030802040006000600060C06080C061801F000B107F8F0F>I<0780184030 C060C06000C000CF00F080E040C060C060C060406060C030801F000B107F8F0F>I<4000 7FE07FC08080808001000200040004000C0008000800180018001800180018000B117E90 0F>I E /Fh 2 60 df<7FFFFCFFFFFEC00006C00006C00006C00006C00006C00006C000 06C00006C00006C00006C00006C00006C00006C00006C00006C00006C00006C00006C000 06FFFFFEFFFFFE17177C991F>50 D<0000000080000000004007C00000400FF000002018 38000010700C000008E0060007FF4003001FFF00018038080000E0E01000007FC0200000 1F004000000000400000000080280E81902A>59 D E /Fi 3 81 df<181818303030606060C0C0050B7E8B09>48 D<063E0008C700110380220180660180 400180C00180C00100C00300C00200E004007008003830001FC000110E7D8D17>79 D<1FFE0023070043038083018003018003010002030006060006180006E0000400000C00 00080000180000100000110F7E8D15>I E /Fj 1 84 df83 D E /Fk 2 79 df73 D78 D E /Fl 30 121 df<0F80180020006000C000FE00C00080008000C000C00061003E00090D7D8C0E >15 D<03FE0FFE18603030603060306030C060C060C0C0408023001E000F0D7E8C13>27 D<40E04003037D820A>58 D<40E06020202040408003097D820A>I<0000C00003C00007 00001C0000780001E0000780000E0000380000F00000F000003800000E000007800001E0 00007800001C000007000003C00000C012147D901A>I62 D<07FFE000E07001C01801C00C01C00C01C0 0E03800E03800E03800E03800E07001C07001C07001C0700380E00300E00700E00E00E01 C01C0700FFFC0017147F931B>68 D<07FFFC00E01C01C00C01C00C01C00C01C008038108 03810003830003FF000702000702000702080700100E00100E00100E00200E00601C01E0 FFFFC016147F9318>I<07FC7FC000E00E0001C01C0001C01C0001C01C0001C01C000380 3800038038000380380003FFF800070070000700700007007000070070000E00E0000E00 E0000E00E0000E00E0001C01C000FF8FF8001A147F931B>72 D<07FC00E001C001C001C0 01C0038003800380038007000700070007000E000E000E000E001C00FF800E147F930F> I<07F000FE00F000F0017001E0017002E0017002E0017004E0027009C0023809C0023811 C0023821C0043823800438438004388380041C8380081D0700081E0700081E0700081C07 0018180E00FE187FC01F147F9320>77 D<07FFC000E07001C01801C01C01C01C01C01C03 80380380700380C003FF000703C00701C00700E00700E00E01C00E01C00E01C00E01C21C 01C4FF807817147F9319>82 D86 D<07B00C7010703060606060606060C0C0C0C8C0C841C862D03C700D 0D7E8C12>97 D<07800C4010E031C0600060006000C000C0004020404021801E000B0D7E 8C0F>99 D<07800C401020304060407F8060004000C0004020604021801E000B0D7E8C10 >101 D<06070600000000384C4C8C98181830326262643808147F930C>105 D<0060007000600000000000000000038004C0046008C008C000C000C001800180018001 8003000300030003006600E600CC0078000C1A81930E>I<3E0006000C000C000C000C00 1800187018B819383230340038003E006300631063106310C320C1C00D147E9312>I<7C 0C181818183030303060606060C0D0D0D0D06006147E930A>I<30F87C00590C86004E0D 06009C0E0600980C0600180C0600180C060030180C0030180C8030181880301818806030 190060300E00190D7F8C1D>I<30F8590C4E0C9C0C980C180C180C301830193031303160 32601C100D7F8C15>I<03800C6018203030603060306030C060C06040C0608023001E00 0C0D7E8C10>I<0C78168C130426062606060606060C0C0C0C0C080C101A2019C0180018 00300030003000FC000F13818C11>I<072008E010E030C060C060C060C0C180C180C180 438067003B00030003000600060006003F800B137E8C0F>I<31E05A704C709C60980018 0018003000300030003000600060000C0D7F8C0F>I<0700188019C0318038001E000F00 03804180E180C10082007C000A0D7E8C10>I<02000600060006000C00FF800C000C0018 00180018001800300031003100320032001C0009127F910D>I<380C4C0C4C0C8C189818 18181818303030323032307218B40F1C0F0D7F8C14>I<0E3C13CE238E430C4300030003 0006000608C608E610CA2071C00F0D7F8C13>120 D E /Fm 52 123 df<0001FC000703000C03001C07001C0300180000380000380000380000380000700007 FFFC00701C00701C00701C00E03800E03800E03800E03800E07001C07001C07001C07001 C0E201C0E201C0E20380E4038064038038038000030000070000060000C60000E40000CC 00007000001825819C17>12 D<0001FDC000070FC0000C0FC0001C0F80001C0380003803 80003803800038070000380700003807000070070007FFFE0000700E0000700E0000700E 0000E01C0000E01C0000E01C0000E01C0000E0380001C0380001C0380001C0380001C071 0001C0710003807100038072000380320003801C00038000000300000007000000060000 00C6000000E4000000CC000000700000001A25819C18>I<000300060008001800300060 00C000C0018003000300060006000C000C001C0018001800380030003000700070006000 600060006000E000E000E000E000E0006000600060006000600020003000100008000800 102A7B9E11>40 D<001000100008000C0004000600060006000600060007000700070007 00070006000600060006000E000E000C000C001C001800180038003000300060006000C0 00C001800300030006000C00180010006000C000102A809E11>I<183878380808101020 404080050C7D830D>44 DI<3078F06005047C830D>I<0000 0200000600000600000C00000C0000180000300000300000600000600000C00000C00001 80000180000300000600000600000C00000C0000180000180000300000300000600000C0 0000C0000180000180000300000300000600000C00000C00001800001800003000003000 00600000600000C0000080000017297F9E15>I<00020006000C001C007C039C00380038 00380038007000700070007000E000E000E000E001C001C001C001C00380038003800380 0780FFF00F1C7C9B15>49 D<003C0000C3000101800201800201C00441C00441C00841C0 0841C00841C01083801083801107000E0600000C0000180000300000C000010000060000 0800001001001002002002004006007E0C00C7F80083F80080E000121D7C9B15>I<003E 0000C1800101800200C00400C00440C00841C00841C00841C0088380070380000700000E 0001F800003800000C00000C00000E00000E00000E00000E00700E00E01C00801C008038 0080300040600021C0001F0000121D7C9B15>I<0001800001C000038000038000038000 0300000700000700000600000E00000C00001C0000180000180000300000300000600000 400000C600018E00010E00020E00061C000C1C00181C003F1C0040F800803F0000380000 380000700000700000700000700000E00000600012247E9B15>I<00C06000FFC001FF80 01FE00010000010000020000020000020000020000047800058C00060600040600080600 000700000700000600000E00000E00700E00700C00E01C00801800803800403000406000 21C0001F0000131D7C9B15>I<000F0000308000C0800183800383800300000600000E00 000C00001C00001CF0003B18003C0C00380C00780C00700E00700E00700E00601C00E01C 00E01C00E01C00E03800E03800E0700060600060C0002180001E0000111D7B9B15>I<09 C04017E0801FE0803C6100302700601A00400600400400800C0080080000180000100000 300000600000600000600000C00000C00001C00001800003800003800003000007000007 00000700000E00000E00000C0000121D799B15>I<01FFFE00003C0780003801C0003801 C0003800E0003800E0007000F00070007000700070007000F000E000F000E000F000E000 F000E000F001C001E001C001E001C001E001C001C0038003C00380038003800780038007 0007000E0007001C0007003800070070000E01C000FFFF00001C1C7D9B1F>68 D<01FFFFE0003C00E0003800600038004000380040003800400070004000700040007020 400070200000E0400000E0400000E0C00000FFC00001C0800001C0800001C0800001C080 0003810100038001000380020003800200070004000700040007000C00070018000E0078 00FFFFF0001B1C7D9B1C>I<01FFFFC0003C01C0003800C0003800800038008000380080 0070008000700080007020800070200000E0400000E0400000E0C00000FFC00001C08000 01C0800001C0800001C08000038100000380000003800000038000000700000007000000 07000000070000000F000000FFF000001A1C7D9B1B>I<01FFC0003C0000380000380000 380000380000700000700000700000700000E00000E00000E00000E00001C00001C00001 C00001C0000380000380000380000380000700000700000700000700000F0000FFE00012 1C7E9B10>73 D<01FFE0003C000038000038000038000038000070000070000070000070 0000E00000E00000E00000E00001C00001C00001C00001C0000380080380080380080380 100700100700300700600700E00E03C0FFFFC0151C7D9B1A>76 D<01FE0007F8003E0007 80002E000F00002E001700002E001700002E002700004E002E00004E004E00004E004E00 004E008E00008E011C00008E011C00008E021C00008E021C000107043800010704380001 0708380001071038000207107000020720700002072070000207407000040740E0000407 80E000040700E0000C0700E0001C0601E000FF861FFC00251C7D9B25>I<01FC03FE001C 0070003C0060002E0040002E0040002E0040004700800047008000470080004380800083 810000838100008181000081C1000101C2000101C2000100E2000100E2000200E4000200 740002007400020074000400380004003800040038000C0018001C001000FF8010001F1C 7D9B1F>I<01FFFC00003C070000380380003801C0003801C0003801C0007003C0007003 C0007003C00070038000E0078000E0070000E00E0000E0380001FFE00001C0000001C000 0001C0000003800000038000000380000003800000070000000700000007000000070000 000F000000FFE000001A1C7D9B1C>80 D<01FFF800003C0E000038070000380380003803 800038038000700780007007800070078000700F0000E00E0000E01C0000E0700000FFC0 0001C0C00001C0600001C0700001C07000038070000380700003807000038070000700F0 000700F0400700F0400700F0800F007880FFE0790000001E001A1D7D9B1E>82 D<000F8400304C00403C0080180100180300180300180600100600100600000700000700 0003E00003FC0001FF00007F800007C00001C00001C00000C00000C02000C02000C06001 80600180600300600200F00400CC180083E000161E7D9C17>I<1FFFFFC01C0701C0300E 00C0200E0080600E0080400E0080401C0080801C0080801C0080001C0000003800000038 000000380000003800000070000000700000007000000070000000E0000000E0000000E0 000000E0000001C0000001C0000001C0000001C0000003C000007FFE00001A1C799B1E> I<03CC063C0C3C181C3838303870387038E070E070E070E070E0E2C0E2C0E261E462643C 380F127B9115>97 D<3F00070007000E000E000E000E001C001C001C001C0039C03E6038 3038307038703870387038E070E070E070E060E0E0C0C0C1C0618063003C000D1D7B9C13 >I<01F007080C08181C3838300070007000E000E000E000E000E000E008E010602030C0 1F000E127B9113>I<001F80000380000380000700000700000700000700000E00000E00 000E00000E0003DC00063C000C3C00181C00383800303800703800703800E07000E07000 E07000E07000E0E200C0E200C0E20061E4006264003C3800111D7B9C15>I<01E007100C 1018083810701070607F80E000E000E000E000E000E0086010602030C01F000D127B9113 >I<0003C0000670000C70001C60001C00001C0000380000380000380000380000380003 FF8000700000700000700000700000700000E00000E00000E00000E00000E00001C00001 C00001C00001C00001C000038000038000038000030000030000070000C60000E60000CC 00007800001425819C0D>I<00F3018F030F06070E0E0C0E1C0E1C0E381C381C381C381C 383830383038187818F00F700070007000E000E0C0C0E1C0C3007E00101A7D9113>I<0F C00001C00001C0000380000380000380000380000700000700000700000700000E78000E 8C000F0E000E0E001C0E001C0E001C0E001C0E00381C00381C00381C0038380070388070 3880707080707100E03200601C00111D7D9C15>I<018003800100000000000000000000 00000000001C002600470047008E008E000E001C001C001C003800380071007100710072 0072003C00091C7C9B0D>I<0006000E0006000000000000000000000000000000F00118 021802180438043800380038007000700070007000E000E000E000E001C001C001C001C0 03800380C300E700CE0078000F24819B0D>I<0FC00001C00001C0000380000380000380 000380000700000700000700000700000E0F000E11000E23800E43801C83001C80001D00 001E00003F800039C00038E00038E00070E20070E20070E20070E400E06400603800111D 7D9C13>I<1F800380038007000700070007000E000E000E000E001C001C001C001C0038 003800380038007000700070007000E400E400E400E40068003800091D7C9C0B>I<3C1E 0780266318C04683A0E04703C0E08E0380E08E0380E00E0380E00E0380E01C0701C01C07 01C01C0701C01C070380380E0388380E0388380E0708380E0710701C0320300C01C01D12 7C9122>I<3C3C002646004687004707008E07008E07000E07000E07001C0E001C0E001C 0E001C1C00381C40381C40383840383880701900300E0012127C9117>I<01E007180C0C 180C380C300E700E700EE01CE01CE01CE018E038E030E06060C031801E000F127B9115> I<07870004D98008E0C008E0C011C0E011C0E001C0E001C0E00381C00381C00381C00381 800703800703000707000706000E8C000E70000E00000E00001C00001C00001C00001C00 003C0000FF8000131A7F9115>I<03C4062C0C3C181C3838303870387038E070E070E070 E070E0E0C0E0C0E061E063C03DC001C001C0038003800380038007803FF00E1A7B9113> I<3C3C26C2468747078E068E000E000E001C001C001C001C003800380038003800700030 0010127C9112>I<01F006080C080C1C18181C001F001FC00FF007F0007800386030E030 C030806060C01F000E127D9111>I<00C001C001C001C00380038003800380FFE0070007 0007000E000E000E000E001C001C001C001C00384038403840388019000E000B1A7D990E >I<1E0300270700470700470700870E00870E000E0E000E0E001C1C001C1C001C1C001C 1C003838803838801838801839001C5900078E0011127C9116>I<1E06270E470E470687 0287020E020E021C041C041C041C0818083808181018200C4007800F127C9113>I<1E01 832703874703874703838707018707010E07010E07011C0E021C0E021C0E021C0E04180C 04181C04181C081C1C100C263007C3C018127C911C>I<070E0019910010E38020E38041 C30041C00001C00001C000038000038000038000038000070200670200E70400CB04008B 080070F00011127D9113>I<1E03270747074707870E870E0E0E0E0E1C1C1C1C1C1C1C1C 38383838183818381C7007F00070007000E0E0C0E1C0818047003C00101A7C9114>I<03 8207C20FEC08381008001000200040008001000200040008081008383067F043E081C00F 127D9111>I E /Fn 47 123 df<003FC00001F0300003C0380007C07C000F807C000F80 7C000F8038000F8000000F8000000F8000000F800000FFFFFC00FFFFFC000F807C000F80 7C000F807C000F807C000F807C000F807C000F807C000F807C000F807C000F807C000F80 7C000F807C000F807C000F807C007FE1FF807FE1FF80191D809C1B>12 D<003FC1FE0001F03F818003C03E01C007C07E03E00F807C03E00F807C03E00F807C01C0 0F807C00000F807C00000F807C00000F807C0000FFFFFFFFE0FFFFFFFFE00F807C03E00F 807C03E00F807C03E00F807C03E00F807C03E00F807C03E00F807C03E00F807C03E00F80 7C03E00F807C03E00F807C03E00F807C03E00F807C03E00F807C03E07FE1FF0FFC7FE1FF 0FFC261D809C28>14 D<0001C070000001C070000001C07000000380E000000380E00000 0380E000000380E000000701C000000701C000000701C000000701C000000E038000FFFF FFFF80FFFFFFFF807FFFFFFF80001C07000000380E000000380E000000380E000000380E 000000380E000000701C00007FFFFFFF80FFFFFFFF80FFFFFFFF8000E038000001C07000 0001C070000001C070000001C07000000380E000000380E000000380E000000380E00000 0701C000000701C000000701C0000021257D9C28>35 D45 D<78FCFCFCFC7806067D850D>I<00600001E0000FE000FFE000F3E00003E00003E0 0003E00003E00003E00003E00003E00003E00003E00003E00003E00003E00003E00003E0 0003E00003E00003E00003E00003E00003E0007FFF807FFF80111B7D9A18>49 D<07F8001FFE00383F80780FC0FC07C0FC07E0FC03E0FC03E07803E00007E00007C00007 C0000F80001F00001E0000380000700000E0000180600300600600600800E01FFFC03FFF C07FFFC0FFFFC0FFFFC0131B7E9A18>I<03F8001FFE003C1F003C0F807C07C07E07C07C 07C03807C0000F80000F80001E00003C0003F800001E00000F800007C00007C00007E030 07E07807E0FC07E0FC07E0FC07C0780F80781F001FFE0007F800131B7E9A18>I<000180 000380000780000F80001F80003F80006F8000CF80008F80018F80030F80060F800C0F80 180F80300F80600F80C00F80FFFFF8FFFFF8000F80000F80000F80000F80000F80000F80 01FFF801FFF8151B7F9A18>I<1801801FFF001FFE001FFC001FF8001FC0001800001800 0018000018000019F8001E0E00180F801007800007C00007E00007E00007E07807E0F807 E0F807E0F807C0F007C0600F80381F001FFE0007F000131B7E9A18>I<007E0003FF0007 81800F03C01E07C03C07C03C0380780000780000F80000F8F800FB0E00FA0780FC0380FC 03C0F803E0F803E0F803E0F803E07803E07803E07803C03C03C03C07801E0F0007FE0003 F800131B7E9A18>I<6000007FFFE07FFFE07FFFC07FFF807FFF80E00300C00600C00C00 C0180000300000300000600000E00000E00001E00001C00003C00003C00003C00003C000 07C00007C00007C00007C00007C00007C000038000131C7D9B18>I<03F8000FFE001E0F 803807803803C07803C07803C07E03C07F83807FC7003FFE001FFC000FFE0007FF801DFF 80387FC0781FE0F007E0F003E0F001E0F001E0F001E07801C07803803E07801FFE0003F8 00131B7E9A18>I<78FCFCFCFC7800000000000078FCFCFCFC7806127D910D>58 D<001FE02000FFF8E003F80FE007C003E00F8001E01F0000E03E0000E03E0000607E0000 607C000060FC000000FC000000FC000000FC000000FC000000FC000000FC000000FC0000 007C0000607E0000603E0000603E0000C01F0000C00F80018007C0030003F80E0000FFFC 00001FE0001B1C7D9B22>67 DII76 DII<003FE0 0001F07C0003C01E000F800F801F0007C01E0003C03E0003E07E0003F07C0001F07C0001 F0FC0001F8FC0001F8FC0001F8FC0001F8FC0001F8FC0001F8FC0001F8FC0001F87C0001 F07E0003F07E0003F03E0003E03F0007E01F0007C00F800F8003C01E0001F07C00003FE0 001D1C7D9B24>II82 D<07F8201FFEE03C07E07801E070 00E0F000E0F00060F00060F80000FE0000FFE0007FFE003FFF003FFF800FFFC007FFE000 7FE00003F00001F00000F0C000F0C000F0C000E0E000E0F001C0FC03C0EFFF0083FC0014 1C7D9B1B>I<7FFFFFE07FFFFFE0781F81E0701F80E0601F8060E01F8070C01F8030C01F 8030C01F8030C01F8030001F8000001F8000001F8000001F8000001F8000001F8000001F 8000001F8000001F8000001F8000001F8000001F8000001F8000001F8000001F8000001F 800007FFFE0007FFFE001C1C7E9B21>I86 D<0FF8001C1E003E0F803E07803E07C0 1C07C00007C0007FC007E7C01F07C03C07C07C07C0F807C0F807C0F807C0780BC03E13F8 0FE1F815127F9117>97 DI<03FC00 0E0E001C1F003C1F00781F00780E00F80000F80000F80000F80000F80000F80000780000 7801803C01801C03000E0E0003F80011127E9115>I<000FF0000FF00001F00001F00001 F00001F00001F00001F00001F00001F00001F001F9F00F07F01C03F03C01F07801F07801 F0F801F0F801F0F801F0F801F0F801F0F801F07801F07801F03C01F01C03F00F0FFE03F9 FE171D7E9C1B>I<01FC000F07001C03803C01C07801C07801E0F801E0F801E0FFFFE0F8 0000F80000F800007800007C00603C00601E00C00F038001FC0013127F9116>I<007F00 01E38003C7C00787C00F87C00F83800F80000F80000F80000F80000F8000FFF800FFF800 0F80000F80000F80000F80000F80000F80000F80000F80000F80000F80000F80000F8000 0F80000F80007FF8007FF800121D809C0F>I<03F8F00E0F381E0F381C07303C07803C07 803C07803C07801C07001E0F000E0E001BF8001000001800001800001FFF001FFFC00FFF E01FFFF07801F8F00078F00078F000787000707800F01E03C007FF00151B7F9118>II<1E003F003F003F003F001E00000000 000000000000000000FF00FF001F001F001F001F001F001F001F001F001F001F001F001F 001F001F00FFE0FFE00B1E7F9D0E>I108 DI< FF0FC0FF31E01F40F01F80F81F80F81F00F81F00F81F00F81F00F81F00F81F00F81F00F8 1F00F81F00F81F00F81F00F8FFE7FFFFE7FF18127F911B>I<01FC000F07801C01C03C01 E07800F07800F0F800F8F800F8F800F8F800F8F800F8F800F87800F07800F03C01E01E03 C00F078001FC0015127F9118>II114 D<1FD830786018E018E018F000FF807FE07FF0 1FF807FC007CC01CC01CE01CE018F830CFC00E127E9113>I<0300030003000300070007 000F000F003FFCFFFC1F001F001F001F001F001F001F001F001F001F0C1F0C1F0C1F0C0F 08079803F00E1A7F9913>I II121 D<3FFF803C1F00303F00303E00607C0060FC0060F80001F00003F00007E00007 C1800F81801F81801F03803E03007E07007C0F00FFFF0011127F9115>I E /Fo 1 64 df<01000100010001000100E10E3FF807C0038006C004400820183010100F 0E7F8C10>63 D E /Fp 14 111 df0 D<8002C006600C301818300C6006C00380038006C00C6018303018600CC00680020F107B 8E1A>2 D<040004000400C460E4E03F800E003F80E4E0C4600400040004000B0D7E8D11> I<0000C00003C0000700001C0000780001E0000780000E0000380000F00000F000003800 000E000007800001E000007800001C000007000003C00000C00000000000000000000000 000000007FFF80FFFFC0121B7D931A>20 D<00000400000004000000020000000100FFFF FFE0FFFFFFE0000001000000020000000400000004001B0A7E8B21>33 D<040E0E1C1C1C38383070706060C0C0070F7F8F0A>48 D<03FC0FFC1C00300060006000 6000C000C000FFFCFFFCC000C00060006000600030001C000FFC03FC0E147D9016>50 D<03FFC00FFFF030E1FC60C07CC0C01E81C01E01C00E01C00E01C00E01800C01800C0380 1C0300180300100700200600400601800C0E000FF8001FC00017147F931A>68 D<0043E0018FF80210F804203C08603C10C01C30801C71001C60001C600018E00018E000 38E00030E00020F00040F800807C01003E06001FF8000FE00016147F931A>79 D<03FFC00FFFF030E1F860C07CC0C03C81C01C01C01801C01801C0300180200180400383 80033E000370000700000600000600000E00000C00000C000018000016157F9318>I<03 FFF0000FFFF80030E07C0060C03C00C0C01C0081C0180001C0180001C0300001C0200001 80C000018F0000039E0000030F0000030F8000070780000603C0000603E0800C01F1000C 00FE001800780019147F931D>82 D<700180F801C07C01E03E00601E00200E00200F0060 0F00400700C0070180070380070700070600071C0007380007780007E00007C000078000 07000006000013157F9315>86 D106 D110 D E /Fq 33 111 df0 D<60F0F06004047C8B0C>I<400020C000606000C03001801803000C0600060C00031800 01B00000E00000E00001B000031800060C000C06001803003001806000C0C00060400020 13147A9320>I<01800180018001804182F18F399C0FF003C003C00FF0399CF18F418201 8001800180018010127E9215>I17 D<007FFF8001FFFF80078000000E00000018000000300000003000000060000000600000 00C0000000C0000000C0000000C0000000C0000000C0000000C000000060000000600000 003000000030000000180000000E0000000780000001FFFF80007FFF8000000000000000 0000000000000000000000000000000000000000007FFFFF807FFFFF8019227D9920>I< 7FFF00007FFFC0000000F0000000380000000C0000000600000006000000030000000300 000001800000018000000180000001800000018000000180000001800000030000000300 000006000000060000000C00000038000000F0007FFFC0007FFF00000000000000000000 0000000000000000000000000000000000000000FFFFFF00FFFFFF0019227D9920>I<00 0001800000078000001E00000078000001E00000078000001E00000078000001E0000007 8000001E00000078000000E0000000780000001E0000000780000001E000000078000000 1E0000000780000001E0000000780000001E000000078000000180000000000000000000 000000000000000000000000000000000000007FFFFF00FFFFFF8019227D9920>II<007FFF 8003FFFF80078000000C0000001800000030000000300000006000000060000000C00000 00C0000000C0000000C0000000C0000000C0000000C0000000C000000060000000600000 003000000030000000180000000E0000000780000001FFFF80007FFF80191A7D9620>26 D<020000000004000000000400000000080000000010000000002000000000FFFFFFFFF0 FFFFFFFFF020000000001000000000080000000004000000000400000000020000000024 0E7D902A>32 D<0000000400000000020000000002000000000100000000008000000000 40FFFFFFFFF8FFFFFFFFF800000000400000000080000000010000000002000000000200 0000000400250E7E902A>I<030003000300030003000300030003000300030003000300 030003000300030003000300030003000300030003000300030003000300030003008304 631813200B4007800300030001000E257D9C15>35 D<0000030000000003000000000180 000000018000000000C00000000060007FFFFFF000FFFFFFF8000000000E000000000700 00000001E0000000007800000001E0000000038000000006000000001C00FFFFFFF8007F FFFFF0000000006000000000C00000000180000000018000000003000000000300002518 7E952A>41 D<00180030000018003000003000180000300018000060000C0000C0000600 01FFFFFF0003FFFFFF8007000001C00C000000603800000038F00000001E780000003C1C 0000007006000000C0030000018001FFFFFF0000FFFFFE0000C00006000060000C000030 00180000300018000018003000001800300027187F952A>44 D<007FF801FFF80780000E 0000180000300000300000600000600000C00000C00000C00000FFFFF8FFFFF8C00000C0 0000C000006000006000003000003000001800000E000007800001FFF8007FF8151A7D96 1C>50 D<0000600000600000C00000C00001800001800001800003000003000006000006 00000C00000C0000180000180000180000300000300000600000600000C00000C0000180 000180000300000300000300000600000600000C00000C00001800001800003000003000 00300000600000600000C0000040000013287A9D00>54 D<400004C0000C600018600018 6000183000303000303000301800601800601FFFE00FFFC00C00C00C00C0060180060180 03030003030003030001860001860001860000CC0000CC0000CC00007800007800007800 003000003000161E809C17>56 DI< 0008001803D80C301838303C303C706E606660666066E0C7E0C7E0C7E0C7E187E187E187 E187E187E307E307E307E307E60766066606760E3C0C3C0C1C180C301BC0180018001023 7E9F15>59 D<003FFE0001FFFFC0071E1FE0081C03F0381C01F8703C00F8603C007CC03C 007C003C003C0038003C0038003C0078003C0078003C00780038007000380070007800F0 007000E0006000E000E001E001C001C0018001C0020003C0040003801800038060000703 80000FFE00001FF000001E1C809B20>68 D<003FFF8001FFFF000700C0000C01C0001C03 8000300380002007000000070000000F0000000F0000000E0000000E0000001E0000001E 0000001C0000001C0000003C0000003800000038000000780000007000000070000000E0 000000E0180001C07000018060007FFF8000FFFF0000191C819B17>73 D<003FFF0001FFFFC0071E0FE0081C03F0381C01F8703C00F8603C0078C03C0078003C00 780038007000380070007800E0007800E0007801C0007001800070020000F00C0000E030 0000E7C00001EF000001E0000001C0000001C00000038000000380000007800000070000 00070000000E0000000C0000001D1E809B1D>80 D<003FFF000001FFFFE000071E0FF000 081C01F800381C00F800703C007800603C007800C03C007800003C007000003800700000 3800E000007800C0000078018000007802000000700C00000071F0000000F3F0000000E1 F0000000E0F8000001E0F8000001C07C000001C07C000003C03C000003803E018003803E 070007801F060007001F880006000FF0000C0007C000211D809B23>82 D<0000000400FFFFF803FFFFE00400E0001C00E0003801C0003001C0007003C000E003C0 00C00380000003800000078000000780000007000000070000000F0000000E0000000E00 00001E0000001E0000001C0000001C00000038000000380000007000000060000000C000 0007FF00000FFC00001E1D7F9C17>84 D<78000CFC001E3E001F1E001F0F000F0F000707 00030700020780020780020380040380040380080380180380300380300380600380C003 8180038380038700038E00039C0003B80003F00003E00007C00007800006000004000018 1E7E9B19>86 D<400002C00006C00006C00006C00006C00006C00006C00006C00006C000 06C00006C00006C00006C00006C00006C00006C00006C00006C0000660000C60000C3000 181C00700F01E003FF8000FE00171A7E981C>91 D<00FE0003FF800F01E01C0070300018 60000C60000CC00006C00006C00006C00006C00006C00006C00006C00006C00006C00006 C00006C00006C00006C00006C00006C00006C00006C00006400002171A7E981C>I<0010 00003800003800006C00006C00006C0000C60000C6000183000183000301800301800600 C00600C00600C00C00600C006018003018003030001830001830001860000C60000CC000 06C00002171A7E981C>94 D<003C00E001C0018003800380038003800380038003800380 03800380038003800380030007001C00F0001C0007000300038003800380038003800380 0380038003800380038003800380018001C000E0003C0E297D9E15>102 DI106 D110 D E /Fr 16 115 df<0102040810302060 6040C0C0C0C0C0C0C0C0C0C040606020301008040201081E7E950D>40 D<80402010080C0406060203030303030303030303020606040C0810204080081E7E950D >I<006000006000006000006000006000006000006000006000006000006000FFFFF0FF FFF000600000600000600000600000600000600000600000600000600000600014167E91 19>43 D<0F0030C0606060604020C030C030C030C030C030C030C030C030C03040206060 606030C00F000C137E9211>48 D<0C001C00EC000C000C000C000C000C000C000C000C00 0C000C000C000C000C000C000C00FFC00A137D9211>I<1F0060C06060F070F030603000 700070006000C001C00180020004000810101020207FE0FFE00C137E9211>I<0FC03070 7038703870380038003000E00FC0007000380018001C601CF01CF018E03860701FC00E13 7F9211>I<006000E000E00160026006600C600860106020606060C060FFFC0060006000 600060006003FC0E137F9211>I<60607FC07F8044004000400040004F0070C040E00060 00700070E070E070E06040E021C01F000C137E9211>I<07C00C201070207060006000C0 00CF00D0C0E060C020C030C030C03040306020206010C00F000C137E9211>I<40007FFC 7FF8401080108020004000800100010003000200060006000E000E000E000E000E000400 0E147E9311>I<0FC0107020186018601870183C303F600F800FE031F06078C01CC00CC0 0CC00C601830300FC00E137F9211>I<1F8060C0C060E060E06000C00180030002000400 040004000400000000000000000004000E0004000B147E9310>63 D<0F80104020206030C010FFF0C000C000C0006000201018200FC00C0D7F8C0F>101 D<0F3C30E62040606060606060204030C02F00600060003FE03FF06018C00CC00CC00C60 1830300FC00F147F8C11>103 D114 D E /Fs 31 123 df<0007F80FF000007FFE7FFC0001F80F F80E0003E00FE01F0007C01FC03F000F801F803F000F801F803F000F800F801E000F800F 800C000F800F8000000F800F8000000F800F8000000F800F800000FFFFFFFFFF00FFFFFF FFFF000F800F801F000F800F801F000F800F801F000F800F801F000F800F801F000F800F 801F000F800F801F000F800F801F000F800F801F000F800F801F000F800F801F000F800F 801F000F800F801F000F800F801F000F800F801F000F800F801F000F800F801F000F800F 801F007FF07FF0FFE07FF07FF0FFE02B237FA22F>14 D<00180000780001F800FFF800FF F80001F80001F80001F80001F80001F80001F80001F80001F80001F80001F80001F80001 F80001F80001F80001F80001F80001F80001F80001F80001F80001F80001F80001F80001 F80001F8007FFFE07FFFE013207C9F1C>49 D<03FC000FFF003C1FC07007E07C07F0FE03 F0FE03F8FE03F8FE01F87C01F83803F80003F80003F00003F00007E00007C0000F80001F 00003E0000380000700000E01801C0180380180700180E00380FFFF01FFFF03FFFF07FFF F0FFFFF0FFFFF015207D9F1C>I<00FE0007FFC00F07E01E03F03F03F03F81F83F81F83F 81F81F03F81F03F00003F00003E00007C0001F8001FE0001FF000007C00001F00001F800 00FC0000FC3C00FE7E00FEFF00FEFF00FEFF00FEFF00FC7E01FC7801F81E07F00FFFC001 FE0017207E9F1C>I<0000E00001E00003E00003E00007E0000FE0001FE0001FE00037E0 0077E000E7E001C7E00187E00307E00707E00E07E00C07E01807E03807E07007E0E007E0 FFFFFEFFFFFE0007E00007E00007E00007E00007E00007E00007E000FFFE00FFFE17207E 9F1C>I<1000201E01E01FFFC01FFF801FFF001FFE001FF8001BC0001800001800001800 0018000019FC001FFF001E0FC01807E01803E00003F00003F00003F80003F83803F87C03 F8FE03F8FE03F8FC03F0FC03F07007E03007C01C1F800FFF0003F80015207D9F1C>I<00 03FE0080001FFF818000FF01E38001F8003F8003E0001F8007C0000F800F800007801F80 0007803F000003803F000003807F000001807E000001807E00000180FE00000000FE0000 0000FE00000000FE00000000FE00000000FE00000000FE00000000FE000000007E000000 007E000001807F000001803F000001803F000003801F800003000F8000030007C0000600 03F0000C0001F800380000FF00F000001FFFC0000003FE000021227DA128>67 D69 D73 D<0007FC0000003FFF800000FC07E00003F001F80007E000FC000FC0007E001F8000 3F001F80003F003F00001F803F00001F807F00001FC07E00000FC07E00000FC0FE00000F E0FE00000FE0FE00000FE0FE00000FE0FE00000FE0FE00000FE0FE00000FE0FE00000FE0 FE00000FE07E00000FC07F00001FC07F00001FC03F00001F803F80003F801F80003F000F C0007E0007E000FC0003F001F80000FC07E000003FFF80000007FC000023227DA12A>79 DI< FFFFFE0000FFFFFFC00007F007F00007F001F80007F000FC0007F0007E0007F0007F0007 F0007F0007F0007F0007F0007F0007F0007F0007F0007F0007F0007E0007F000FC0007F0 01F80007F007F00007FFFFC00007FFFF800007F00FE00007F007F00007F003F80007F001 FC0007F001FC0007F001FC0007F001FC0007F001FC0007F001FC0007F001FC0007F001FC 0007F001FC0607F000FE0607F000FF0CFFFF803FF8FFFF800FF027227EA12A>82 D<07FC001FFF803F07C03F03E03F01E03F01F01E01F00001F00001F0003FF003FDF01FC1 F03F01F07E01F0FC01F0FC01F0FC01F0FC01F07E02F07E0CF81FF87F07E03F18167E951B >97 D<00FF8007FFE00F83F01F03F03E03F07E03F07C01E07C0000FC0000FC0000FC0000 FC0000FC0000FC00007C00007E00007E00003E00301F00600FC0E007FF8000FE0014167E 9519>99 D<0001FE000001FE0000003E0000003E0000003E0000003E0000003E0000003E 0000003E0000003E0000003E0000003E0000003E0001FC3E0007FFBE000F81FE001F007E 003E003E007E003E007C003E00FC003E00FC003E00FC003E00FC003E00FC003E00FC003E 00FC003E00FC003E007C003E007C003E003E007E001E00FE000F83BE0007FF3FC001FC3F C01A237EA21F>I<00FE0007FF800F87C01E01E03E01F07C00F07C00F8FC00F8FC00F8FF FFF8FFFFF8FC0000FC0000FC00007C00007C00007E00003E00181F00300FC07003FFC000 FF0015167E951A>I<003F8000FFC001E3E003C7E007C7E00F87E00F83C00F80000F8000 0F80000F80000F80000F8000FFFC00FFFC000F80000F80000F80000F80000F80000F8000 0F80000F80000F80000F80000F80000F80000F80000F80000F80000F80000F80000F8000 7FF8007FF80013237FA211>I<03FC1E0FFF7F1F0F8F3E07CF3C03C07C03E07C03E07C03 E07C03E07C03E03C03C03E07C01F0F801FFF0013FC003000003000003800003FFF801FFF F00FFFF81FFFFC3800FC70003EF0001EF0001EF0001EF0001E78003C7C007C3F01F80FFF E001FF0018217E951C>I<1C003E007F007F007F003E001C000000000000000000000000 000000FF00FF001F001F001F001F001F001F001F001F001F001F001F001F001F001F001F 001F001F001F00FFE0FFE00B247EA310>105 D108 DII<00FE0007FFC00F83E01E00F03E00F87C007C7C007C7C007CFC007E FC007EFC007EFC007EFC007EFC007EFC007E7C007C7C007C3E00F81F01F00F83E007FFC0 00FE0017167E951C>I I114 D<0FF3003FFF00781F00600700E00300E00300F00300FC00007FE0007FF8003FFE 000FFF0001FF00000F80C00780C00380E00380E00380F00700FC0E00EFFC00C7F0001116 7E9516>I<0180000180000180000180000380000380000780000780000F80003F8000FF FF00FFFF000F80000F80000F80000F80000F80000F80000F80000F80000F80000F80000F 80000F81800F81800F81800F81800F81800F830007C30003FE0000F80011207F9F16>I< FF01FE00FF01FE001F003E001F003E001F003E001F003E001F003E001F003E001F003E00 1F003E001F003E001F003E001F003E001F003E001F003E001F003E001F003E001F007E00 1F00FE000F81BE0007FF3FC001FC3FC01A167E951F>II 121 D<7FFFF07FFFF07C03E07007C0600FC0E01F80C01F00C03E00C07E0000FC0000F800 01F00003F03007E03007C0300F80701F80703F00603E00E07C03E0FFFFE0FFFFE014167E 9519>I E /Ft 17 117 df<0078000001CC000003840000038600000786000007860000 07840000078C000007880000079007F807A007F803C0018003C0018003E0030005E00600 0DF0060018F80C0038781800787C3000F83E3000F81F6000F80FC000FC07C0187E0FF030 3FFCFFF00FE01FC01D1A7E9922>38 D<78FCFCFCFC7806067D850C>46 D<07F0001E3C003C1E00380E00780F00780F00780F00F80F80F80F80F80F80F80F80F80F 80F80F80F80F80F80F80F80F80F80F80F80F80780F00780F00380E003C1E001E3C0007F0 0011187E9716>48 D<00C003C0FFC0FFC003C003C003C003C003C003C003C003C003C003 C003C003C003C003C003C003C003C003C07FFE7FFE0F187D9716>I<0FF0003FFC00787E 00FC1F00FC1F80FC0F80FC0F80780F80001F80001F00001E00003C0000780000700000E0 000180000301800601800C01801003803FFF007FFF00FFFF00FFFF0011187E9716>I<07 F0001FFC00383E007C3E007C1F007C1F007C1F00383F00003E00003C0000780007F00000 3C00001E00001F00001F80781F80FC1F80FC1F80FC1F00F81F00703E003FFC000FF00011 187E9716>I<000600000E00001E00003E00007E0000DE00019E00011E00031E00061E00 0C1E00181E00301E00601E00C01E00FFFFE0FFFFE0001E00001E00001E00001E00001E00 01FFE001FFE013187F9716>I<3006003FFC003FFC003FF0003FE0003F80003000003000 0030000037F000381C00301E00000F00000F00000F80700F80F80F80F80F80F80F80F80F 00601F00383E001FF80007E00011187E9716>I<6000007FFFC07FFFC07FFF807FFF00E0 0600C00600C00C00C0180000300000600000600000E00001E00001C00003C00003C00003 C00007C00007C00007C00007C00007C00007C00003800012197E9816>55 D<07E0001FF8003C1C00781E00780F00F80F00F80F00F80F80F80F80F80F80F80F80781F 80381F801C2F8007CF80000F80000F00380F007C1F007C1E00783C003078001FF0000FC0 0011187E9716>57 D<00030000000780000007800000078000000FC000000FC000001BE0 00001BE000001BE0000031F0000031F0000060F8000060F80000E0FC0000C07C0000C07C 0001803E0001FFFE0003FFFF0003001F0003001F0006000F8006000F800E000FC0FFC07F FCFFC07FFC1E1A7F9921>65 D<0FF0001C3C003E1E003E0E003E0F001C0F00000F0000FF 000FCF003E0F007C0F00F80F00F80F00F80F00F817007C27E01FC3E013117F9015>97 DI<03FC000F0E001C1F003C1F00781F00780E00F80000F8 0000F80000F80000F800007800007800003C01801C03000F060003FC0011117F9014>I< FC78FC9C1D3E1D3E1E3E1E1C1E001E001E001E001E001E001E001E001E00FFC0FFC00F11 7F9012>114 D<1FB020704030C030C030F000FF807FE03FF807F8003CC00CC00CE00CE0 08F830CFE00E117F9011>I<06000600060006000E000E001E003FF0FFF01E001E001E00 1E001E001E001E001E001E181E181E181E181E180F3003E00D187F9711>I E /Fu 20 125 df45 D<70F8F8F8700505798414>I<01E0 07F00E38181C38FC71FC739E739EE70EE70EE70EE70EE70EE70EE70E739C739C71F838F0 18060E1E07F801F00F177E9614>64 D<1FC0007FF000707800201800001C00001C0007FC 001FFC003C1C00701C00E01C00E01C00E01C00707C003FFF800F8F8011107E8F14>97 DI<03F80FFC1C1C380870006000E000E000E000E00060007000380E1C1E0FFC03 F00F107E8F14>I<007E00007E00000E00000E00000E00000E00000E0007CE000FFE001C 3E00301E00700E00E00E00E00E00E00E00E00E00E00E00E00E00700E00301E00383E001F EFC007CFC012177F9614>I<07E00FF01C38301C700CE00EE00EFFFEFFFEE00060007000 380E1C1E0FFC03F00F107E8F14>I<007C00FE01CE03840380038003807FFEFFFE038003 8003800380038003800380038003800380038003807FFC7FFC0F177F9614>I 104 D<030007800780030000000000000000007F807F8003800380038003800380038003 8003800380038003800380FFFCFFFC0E187D9714>I107 DI 110 D<07C01FF03C78701C701CE00EE00EE00EE00EE00EE00E701C783C3C781FF007C00F 107E8F14>I114 D<0FD83FF86038C038C0 38F0007F803FF007F8001C6006E006F006F81CFFF8CFE00F107E8F14>I<030007000700 070007007FFCFFFC07000700070007000700070007000700070E070E070E070C03FC00F0 0F157F9414>II124 D E /Fv 5 104 df<8000C0C001C0600300300600180C000C180006300003600001C000 01C0000360000630000C1800180C00300600600300C001C08000C012127A911E>2 D<00103E000060FF8000C31FC0018607C0030C03E0061C03E00C3801E01C3801E0386001 E0384001E0780001E0700001E0700001C0F00001C0F00003C0F0000380F0000300F00007 00F8000E00F8000C007C0018007C0030003E0040003F8180001FFE000007F800001B1A7E 991E>79 D<00FFF80003FFFE000C787F0030781F8070780F80E0780780C0700780007007 0000F0070000F00E0000F00E0000E01C0000E0100001E0600001E7800001CFC00001C7C0 0003C3E0000383E0000381E0000781F0000701F0180700F8300E00FC400E007F8018003E 001D1A7E9921>82 D<007001C00380070007000700070007000700070007000700070007 00070007000E001C00F0001C000E00070007000700070007000700070007000700070007 0007000700038001C000700C257D9B13>102 DI E /Fw 78 128 df<00FC7C0183C607078E0607040E07000E07000E07000E07000E07000E 0700FFFFF00E07000E07000E07000E07000E07000E07000E07000E07000E07000E07000E 07000E07000E07000E07007F0FF0171A809916>11 D<00FC000182000703000607000E02 000E00000E00000E00000E00000E0000FFFF000E07000E07000E07000E07000E07000E07 000E07000E07000E07000E07000E07000E07000E07000E07007F0FE0131A809915>I<00 7E1F8001C170400703C060060380E00E0380400E0380000E0380000E0380000E0380000E 038000FFFFFFE00E0380E00E0380E00E0380E00E0380E00E0380E00E0380E00E0380E00E 0380E00E0380E00E0380E00E0380E00E0380E00E0380E00E0380E07F8FE3FC1E1A809920 >14 D<60C0F1E0F9F068D0081008100810102010202040C1800C0B7F9913>34 D<60F0F868080808101020C0050B7D990B>39 D<00800100020004000C00080018003000 300030006000600060006000E000E000E000E000E000E000E000E000E000E00060006000 60006000300030003000180008000C00040002000100008009267D9B0F>I<8000400020 001000180008000C00060006000600030003000300030003800380038003800380038003 8003800380038003000300030003000600060006000C0008001800100020004000800009 267E9B0F>I<000C0000000C0000000C0000000C0000000C0000000C0000000C0000000C 0000000C0000000C0000000C0000000C0000FFFFFF80FFFFFF80000C0000000C0000000C 0000000C0000000C0000000C0000000C0000000C0000000C0000000C0000000C0000000C 0000191A7E951E>43 D<60F0F07010101020204080040B7D830B>II<60F0F06004047D830B>I<0004000C00180018001800300030003000600060006000 C000C000C00180018001800300030003000600060006000C000C000C0018001800180030 0030003000600060006000C000C0000E257E9B13>I<078018603030303060186018E01C E01CE01CE01CE01CE01CE01CE01CE01CE01CE01CE01C6018601870383030186007800E18 7E9713>I<03000700FF0007000700070007000700070007000700070007000700070007 000700070007000700070007000700FFF00C187D9713>I<0F80106020304038803CC01C E01C401C003C003800380070006000C001800100020004040804100430083FF87FF8FFF8 0E187E9713>I<0F8010E02070607870382038007800700070006000C00F8000E0007000 38003C003CE03CE03CC03C4038407030E00F800E187E9713>I<00300030007000F000F0 01700370027004700C7008701070307020704070C070FFFF007000700070007000700070 07FF10187F9713>I<30183FF03FE03FC02000200020002000200027C038602030003800 18001C001C401CE01CE01C80184038403030E00F800E187E9713>I<01E006100C181838 3038300070006000E000E7C0E860F030F018E018E01CE01CE01C601C601C701830183030 186007C00E187E9713>I<40007FFE7FFC7FFC4008801080108020004000400080018001 800100030003000300030007000700070007000700070002000F197E9813>I<07801860 3030201860186018601870103C303E600F8007C019F030F86038401CC00CC00CC00CC00C 6008201018600FC00E187E9713>I<07801860303070306018E018E018E01CE01CE01C60 1C603C303C185C0F9C001C00180018003870307060604021801F000E187E9713>I<60F0 F060000000000000000060F0F06004107D8F0B>I<000C0000000C0000000C0000001E00 00001E0000003F000000270000002700000043800000438000004380000081C0000081C0 000081C0000100E0000100E00001FFE00002007000020070000600780004003800040038 0008001C0008001C001C001E00FF00FFC01A1A7F991D>65 DI<003F0201C0C603002E0E001E1C000E1C0006380006780002700002700002F00000F0 0000F00000F00000F00000F000007000027000027800023800041C00041C00080E000803 003001C0C0003F00171A7E991C>IIII<003F020001C0C60003002E000E001E001C00 0E001C00060038000600780002007000020070000200F0000000F0000000F0000000F000 0000F0000000F001FFC070000E0070000E0078000E0038000E001C000E001C000E000E00 0E000300160001C06600003F82001A1A7E991E>III<1FFC00E000E000E000E000E000E000 E000E000E000E000E000E000E000E000E000E000E000E000E040E0E0E0E0E041C061801E 000E1A7D9914>IIIII<007F000001C1C000070070000E0038001C001C003C001E0038000E0078000F00 70000700F0000780F0000780F0000780F0000780F0000780F0000780F0000780F0000780 78000F0078000F0038000E003C001E001C001C000E0038000700700001C1C000007F0000 191A7E991E>II82 D<0FC21836200E6006C006C002 C002C002E00070007E003FE01FF807FC003E000E00070003800380038003C002C006E004 D81887E0101A7E9915>I<7FFFFF00701C0700401C0100401C0100C01C0180801C008080 1C0080801C0080001C0000001C0000001C0000001C0000001C0000001C0000001C000000 1C0000001C0000001C0000001C0000001C0000001C0000001C0000001C0000001C000000 1C000003FFE000191A7F991C>IIII<7FC0FF000F003C000700300007 8020000380600001C0400001E0800000E1800000710000007A0000003C0000001C000000 1E0000001E00000017000000278000004380000041C0000081E0000100E0000100700002 007800040038000C001C001E003E00FF80FFC01A1A7F991D>II 91 D<1830204040804080810081008100B160F9F078F030600C0B7B9913>II<3F8070C070E020700070007007F01C7030707070E070E071E071E0F171FB1E3C10 107E8F13>97 DI<07F80C1C381C30087000E000E000E000 E000E000E0007000300438080C1807E00E107F8F11>I<007E00000E00000E00000E0000 0E00000E00000E00000E00000E00000E0003CE000C3E00380E00300E00700E00E00E00E0 0E00E00E00E00E00E00E00E00E00600E00700E00381E001C2E0007CFC0121A7F9915>I< 07C01C3030187018600CE00CFFFCE000E000E000E0006000300438080C1807E00E107F8F 11>I<01F0031807380E100E000E000E000E000E000E00FFC00E000E000E000E000E000E 000E000E000E000E000E000E000E000E007FE00D1A80990C>I<0FCE1873303070387038 70387038303018602FC02000600070003FF03FFC1FFE600FC003C003C003C0036006381C 07E010187F8F13>II<18003C003C001800000000000000 000000000000FC001C001C001C001C001C001C001C001C001C001C001C001C001C001C00 FF80091A80990A>I<018003C003C001800000000000000000000000000FC001C001C001 C001C001C001C001C001C001C001C001C001C001C001C001C001C001C001C041C0E180E3 007E000A2182990C>IIIII<07E01C38300C700E 6006E007E007E007E007E007E0076006700E381C1C3807E010107F8F13>II<03 C2000C2600381E00300E00700E00E00E00E00E00E00E00E00E00E00E00E00E00700E0070 0E00381E001C2E0007CE00000E00000E00000E00000E00000E00000E00007FC012177F8F 14>II<1F2060E04020C020C020F0007F003FC01FE000F080708030C030C020F040 8F800C107F8F0F>I<0400040004000C000C001C003C00FFC01C001C001C001C001C001C 001C001C001C201C201C201C201C200E4003800B177F960F>IIIIII<7FF86070407040E041C041C00380070007000E081C08 1C08381070107030FFF00D107F8F11>II<6180F3C0F3C061800A04 7C9913>127 D E /Fx 81 128 df<007E1F0001C1B1800303E3C00703C3C00E03C1800E 01C0000E01C0000E01C0000E01C0000E01C0000E01C000FFFFFC000E01C0000E01C0000E 01C0000E01C0000E01C0000E01C0000E01C0000E01C0000E01C0000E01C0000E01C0000E 01C0000E01C0000E01C0000E01C0000E01C0007F87FC001A1D809C18>11 D<007E0001C1800301800703C00E03C00E01800E00000E00000E00000E00000E0000FFFF C00E01C00E01C00E01C00E01C00E01C00E01C00E01C00E01C00E01C00E01C00E01C00E01 C00E01C00E01C00E01C00E01C07F87F8151D809C17>I<007FC001C1C00303C00703C00E 01C00E01C00E01C00E01C00E01C00E01C00E01C0FFFFC00E01C00E01C00E01C00E01C00E 01C00E01C00E01C00E01C00E01C00E01C00E01C00E01C00E01C00E01C00E01C00E01C07F CFF8151D809C17>I<003F07E00001C09C18000380F018000701F03C000E01E03C000E00 E018000E00E000000E00E000000E00E000000E00E000000E00E00000FFFFFFFC000E00E0 1C000E00E01C000E00E01C000E00E01C000E00E01C000E00E01C000E00E01C000E00E01C 000E00E01C000E00E01C000E00E01C000E00E01C000E00E01C000E00E01C000E00E01C00 0E00E01C007FC7FCFF80211D809C23>I<6060F0F0F8F868680808080808081010101020 20404080800D0C7F9C15>34 D<00E0000001900000030800000308000007080000070800 0007080000070800000710000007100000072000000740000003C03FE003800F00038006 000380040005C0040009C0080010E0100030E010006070200060702000E0384000E03C40 00E01C8000E00F0020E0070020700780403009C0401830E18007C03E001B1F7E9D20>38 D<60F0F8680808081010204080050C7C9C0C>I<004000800100020006000C000C001800 1800300030007000600060006000E000E000E000E000E000E000E000E000E000E000E000 E000600060006000700030003000180018000C000C00060002000100008000400A2A7D9E 10>I<800040002000100018000C000C000600060003000300038001800180018001C001 C001C001C001C001C001C001C001C001C001C001C0018001800180038003000300060006 000C000C00180010002000400080000A2A7E9E10>I<0006000000060000000600000006 000000060000000600000006000000060000000600000006000000060000000600000006 0000FFFFFFE0FFFFFFE00006000000060000000600000006000000060000000600000006 00000006000000060000000600000006000000060000000600001B1C7E9720>43 D<60F0F0701010101020204080040C7C830C>II<60F0F0600404 7C830C>I<00010003000600060006000C000C000C001800180018003000300030006000 6000C000C000C0018001800180030003000300060006000C000C000C0018001800180030 0030003000600060006000C000C00010297E9E15>I<03C00C301818300C300C700E6006 6006E007E007E007E007E007E007E007E007E007E007E007E007E00760066006700E300C 300C18180C3007E0101D7E9B15>I<030007003F00C70007000700070007000700070007 000700070007000700070007000700070007000700070007000700070007000F80FFF80D 1C7C9B15>I<07C01830201C400C400EF00FF80FF807F8077007000F000E000E001C001C 00380070006000C00180030006010C01180110023FFE7FFEFFFE101C7E9B15>I<07E018 30201C201C781E780E781E381E001C001C00180030006007E00030001C001C000E000F00 0F700FF80FF80FF80FF00E401C201C183007E0101D7E9B15>I<000C00000C00001C0000 3C00003C00005C0000DC00009C00011C00031C00021C00041C000C1C00081C00101C0030 1C00201C00401C00C01C00FFFFC0001C00001C00001C00001C00001C00001C00001C0001 FFC0121C7F9B15>I<300C3FF83FF03FC020002000200020002000200023E02430281830 1C200E000E000F000F000F600FF00FF00FF00F800E401E401C2038187007C0101D7E9B15 >I<00F0030C06040C0E181E301E300C700070006000E3E0E430E818F00CF00EE006E007 E007E007E007E007600760077006300E300C18180C3003E0101D7E9B15>I<4000007FFF 807FFF007FFF0040020080040080040080080000100000100000200000600000400000C0 0000C00001C0000180000180000380000380000380000380000780000780000780000780 00078000078000030000111D7E9B15>I<03E00C301008200C2006600660066006700678 0C3E083FB01FE007F007F818FC307E601E600FC007C003C003C003C00360026004300C1C 1007E0101D7E9B15>I<03C00C301818300C700C600EE006E006E007E007E007E007E007 6007700F300F18170C2707C700060006000E300C780C78187010203030C00F80101D7E9B 15>I<60F0F0600000000000000000000060F0F06004127C910C>I<60F0F0600000000000 000000000060F0F0701010101020204080041A7C910C>I<7FFFFFC0FFFFFFE000000000 00000000000000000000000000000000000000000000000000000000FFFFFFE07FFFFFC0 1B0C7E8F20>61 D<0FE03038401CE00EF00EF00EF00E000C001C0030006000C000800180 0100010001000100010001000000000000000000000003000780078003000F1D7E9C14> 63 D<000600000006000000060000000F0000000F0000000F0000001780000017800000 1780000023C0000023C0000023C0000041E0000041E0000041E0000080F0000080F00001 80F8000100780001FFF80003007C0002003C0002003C0006003E0004001E0004001E000C 001F001E001F00FF80FFF01C1D7F9C1F>65 DI<001F808000E0618001801980070007800E0003801C0003801C000180380001807800 00807800008070000080F0000000F0000000F0000000F0000000F0000000F0000000F000 0000F0000000700000807800008078000080380000801C0001001C0001000E0002000700 04000180080000E03000001FC000191E7E9C1E>IIII<001F 808000E0618001801980070007800E0003801C0003801C00018038000180780000807800 008070000080F0000000F0000000F0000000F0000000F0000000F0000000F000FFF0F000 0F80700007807800078078000780380007801C0007801C0007800E00078007000B800180 118000E06080001F80001C1E7E9C21>III<1FFF00F800780078007800780078007800 780078007800780078007800780078007800780078007800787078F878F878F878F0F040 E021C01F00101D7F9B15>IIIII<003F800000E0E0000380380007001C00 0E000E001C0007003C00078038000380780003C0780003C0700001C0F00001E0F00001E0 F00001E0F00001E0F00001E0F00001E0F00001E0F00001E0700001C0780003C0780003C0 380003803C0007801C0007000E000E0007001C000380380000E0E000003F80001B1E7E9C 20>II 82 D<07E0801C1980300580700380600180E00180E00080E00080E00080F00000F80000 7C00007FC0003FF8001FFE0007FF0000FF80000F800007C00003C00001C08001C08001C0 8001C0C00180C00180E00300D00200CC0C0083F800121E7E9C17>I<7FFFFFC0700F01C0 600F00C0400F0040400F0040C00F0020800F0020800F0020800F0020000F0000000F0000 000F0000000F0000000F0000000F0000000F0000000F0000000F0000000F0000000F0000 000F0000000F0000000F0000000F0000000F0000000F0000001F800003FFFC001B1C7F9B 1E>II87 D91 D<08081010202040404040808080808080B0B0F8F8787830300D0C7A9C15>II<1FC000307000783800781C00301C00001C00001C0001FC000F 1C00381C00701C00601C00E01C40E01C40E01C40603C40304E801F870012127E9115>97 DI<07E00C301878307870306000E0 00E000E000E000E000E00060007004300418080C3007C00E127E9112>I<003F00000700 00070000070000070000070000070000070000070000070000070003E7000C1700180F00 300700700700600700E00700E00700E00700E00700E00700E00700600700700700300700 180F000C370007C7E0131D7E9C17>I<03E00C301818300C700E6006E006FFFEE000E000 E000E00060007002300218040C1803E00F127F9112>I<00F8018C071E061E0E0C0E000E 000E000E000E000E00FFE00E000E000E000E000E000E000E000E000E000E000E000E000E 000E000E000E007FE00F1D809C0D>I<00038003C4C00C38C01C3880181800381C00381C 00381C00381C001818001C38000C300013C0001000003000001800001FF8001FFF001FFF 803003806001C0C000C0C000C0C000C06001803003001C0E0007F800121C7F9215>II<18003C003C00180000000000000000 00000000000000FC001C001C001C001C001C001C001C001C001C001C001C001C001C001C 001C001C00FF80091D7F9C0C>I<00C001E001E000C00000000000000000000000000000 0FE000E000E000E000E000E000E000E000E000E000E000E000E000E000E000E000E000E0 00E000E000E060E0F0C0F1C061803E000B25839C0D>IIIII<03F0000E1C00180600300300700380600180E001 C0E001C0E001C0E001C0E001C0E001C06001807003803003001806000E1C0003F0001212 7F9115>II<03C1000C3300180B00300F00700700700700 E00700E00700E00700E00700E00700E00700600700700700300F00180F000C370007C700 000700000700000700000700000700000700000700003FE0131A7E9116>II<1F9030704030C010C010E010F8007F803FE00FF000F880388018C018C018E010D060 8FC00D127F9110>I<04000400040004000C000C001C003C00FFE01C001C001C001C001C 001C001C001C001C001C101C101C101C101C100C100E2003C00C1A7F9910>IIII<7F8FF00F03800F030007020003840001C80001 D80000F00000700000780000F800009C00010E00020E000607000403801E07C0FF0FF815 12809116>II<7FFC70386038407040F040E041C003C003 8007000F040E041C043C0C380870087038FFF80E127F9112>II<1C 043F0843F080E00E047D9B15>126 D<6060F0F0F0F060600C047C9C15>I E /Fy 51 121 df<0003F800000E0E000038038000E001C001C001C0038000E0070000E0 0F0000F01E0000F01C0000F03C0000F03C0000F0788008F078FFF8F078FFF8F0F1FFF1E0 F1FFF1E0F10011E0F00003C0F00003C0F0000380F0000780F0000F0070000E0070001C00 38003800380070001C01C0000707800001FC00001C1E7E9C20>2 D<01FFFFFE01E0003E00E0000E00E0000400700004007000040078000400380004003C00 04001C0000001C0000001E0000000E0000000F0000000600000004000000080000001000 0000200020004000200080002001000040020000C00C0000C01000018020000F807FFFFF 00FFFFFF001F1C7E9B20>6 D<0780101FC0103FE0207FF020603040C010808010800009 00000900000A00000A00000A00000C00000C000008000008000008000018000018000018 00003000003000003000003000006000006000004000141B7F9115>13 D<007C00C2010203000600060006000700078003C001E001F003780E381C1C381C300C70 0C700CE008E008E018E010E010E0306020604030801F000F1D7E9C12>I<01F807000C00 18003800300070007FC0E000E000E000E000E00060006000300018600F800D127E9111> I<007800CC0186030606060E060C061C07180738063806300E700E700E7FFEE01CE01CE0 1CE018E038C038C070C060C060C0C0C180618062003C00101D7E9C13>18 D<07800001C00000E00000E00000F000007000007000007000003800003800003800003C 00001C00001C00001E00000E00001E00003F0000670000C7000187800303800703800E03 801C03C03801C07001C0E001E06000E0131D7E9C18>21 D<01FFF803FFF80FFFF01E1E00 180E00380600700600700600E00E00E00E00E00E00E00C00E01C00E01800E03000606000 30C0001F000015127E9118>27 D45 D<60F0F06004047C830C>58 D<60F0F0701010101020204080040C7C830C>I<00010003 000600060006000C000C000C0018001800180030003000300060006000C000C000C00180 01800180030003000300060006000C000C000C0018001800180030003000300060006000 6000C000C00010297E9E15>61 DI<002000002000002000002000002000002000007000C070187C71F0 0FFF8003FE0000F80000F80001DC00018C000306000202000603000C0180080080151480 9315>I<00000C0000000C0000001C0000001C0000003C0000007C0000005C0000009C00 00008E0000010E0000010E0000020E0000040E0000040E0000080E0000080E0000100E00 00200E00003FFE0000400700004007000080070001000700010007000200070002000700 060007001E000700FF807FF01C1D7F9C1F>65 D<01FFFF00003C01C0003800E0003800F0 003800700038007000700070007000F0007000F0007001E000E003C000E0078000E01F00 00FFFC0001C00F0001C0078001C003C001C003C0038003C0038003C0038003C0038003C0 070007800700070007000E0007001C000E007800FFFFC0001C1C7E9B1F>I<0001F80800 0E061800380138006000F001C0007003800070070000300F0000200E0000201C0000203C 0000203C000000780000007800000078000000F0000000F0000000F0000000F0000000F0 000100F0000100F0000100700002007000020030000400380008001C0010000E00600007 01800000FE00001D1E7E9C1E>I<0001F808000E061800380138006000F001C000700380 0070070000300F0000200E0000201C0000203C0000203C00000078000000780000007800 0000F0000000F0000000F0007FF0F0000780F0000700F0000700F0000700700007007000 0E0030000E0038000E001C001E000E0064000701840000FE00001D1E7E9C21>71 D<01FFE0003C0000380000380000380000380000700000700000700000700000E00000E0 0000E00000E00001C00001C00001C00001C0000380020380020380020380040700040700 0C0700180700380E00F0FFFFF0171C7E9B1C>76 D<01FC00FF80001C001C00002E001800 002E001000002E0010000027001000004700200000430020000043802000004380200000 81C040000081C040000081C040000080E040000100E08000010070800001007080000100 70800002003900000200390000020039000002001D000004001E000004000E000004000E 00000C000E00001C00040000FF80040000211C7E9B21>78 D<01FFFF00003C03C0003800 E0003800F00038007000380070007000F0007000F0007000F0007000E000E001E000E003 C000E0078000E01E0001FFF00001C0000001C0000001C000000380000003800000038000 0003800000070000000700000007000000070000000F000000FFE000001C1C7E9B1B>80 D<01FFFE00003C03C0003800E0003800F00038007000380070007000F0007000F0007000 F0007001E000E001C000E0078000E01E0000FFF00001C0300001C0180001C01C0001C01C 0003801C0003801C0003801C0003801C0007003C0007003C0807003C0807003C100F001E 10FFE00E20000007C01D1D7E9B20>82 D<1FFFFFF01C0380703007003020070020600700 2040070020400E0020800E0020800E0020000E0000001C0000001C0000001C0000001C00 00003800000038000000380000003800000070000000700000007000000070000000E000 0000E0000000E0000000E0000001E000007FFF00001C1C7F9B18>84 D<7FF03FE00F0007000E0006000E0004000E0004000E0004001C0008001C0008001C0008 001C00080038001000380010003800100038001000700020007000200070002000700020 00E0004000E0004000E0004000E0008000E0008000E00100006002000060040000300800 001830000007C000001B1D7D9B1C>II<01FFC0FF80 001E003C00001E003000000E002000000F00400000070080000007010000000782000000 038400000003C800000001D000000001F000000000E000000000E000000000F000000001 70000000027000000004380000000838000000103C000000201C000000401E000000800E 000001800E000003000F000006000700001E000F8000FF803FF000211C7F9B22>88 DI<01E3000717000C0F00180F00380E00300E00700E00700E00 E01C00E01C00E01C00E01C00E03880E03880E038806078803199001E0E0011127E9116> 97 D<3F00070007000E000E000E000E001C001C001C001C0039E03A303C183818701870 1C701C701CE038E038E038E030E070E060E0C061C023001E000E1D7E9C12>I<01F0030C 0E0C1C1E383C301870007000E000E000E000E000E000E0046008601030601F800F127E91 12>I<0007E00000E00000E00001C00001C00001C00001C0000380000380000380000380 01E7000717000C0F00180F00380E00300E00700E00700E00E01C00E01C00E01C00E01C00 E03880E03880E038806078803199001E0E00131D7E9C16>I<01F007080C081804380830 0870307FC0E000E000E000E000E000E0046008601030600F800E127E9113>I<0001E000 0630000E78000CF0001C60001C00001C00001C00003C0000380000380003FFC000380000 380000700000700000700000700000700000E00000E00000E00000E00000E00001C00001 C00001C00001C00001C000018000038000038000630000F30000F60000E4000078000015 257E9C14>I<007180018B800307800607800E07000C07001C07001C0700380E00380E00 380E00380E00381C00381C00381C00183C0008F800073800003800003800007000607000 F06000F0E000E180007E0000111A7F9114>I<0FC00001C00001C0000380000380000380 000380000700000700000700000700000E3E000EC3000F03800E03801E03801C03801C03 801C0380380700380700380700380E00700E20700E20701C20701C40E00C80600700131D 7E9C18>I<01C003C003C001800000000000000000000000001C00270047004700870087 000E000E001C001C001C003800388038807080710032001C000A1C7E9B0E>I<0007000F 000F00060000000000000000000000000070009C010C020C021C041C001C001C00380038 00380038007000700070007000E000E000E000E001C061C0F180F300E6007C001024809B 11>I<0FC00001C00001C000038000038000038000038000070000070000070000070000 0E07000E18800E21C00E23C01C47801C83001D00001E00003F800039C00038E00038E000 70E10070E10070E10070E200E06200603C00121D7E9C16>I<1F80038003800700070007 0007000E000E000E000E001C001C001C001C0038003800380038007000700070007000E4 00E400E400E40064003800091D7E9C0C>I<381F81F04E20C6184640E81C4680F01C8F00 F01C8E00E01C0E00E01C0E00E01C1C01C0381C01C0381C01C0381C01C070380380713803 8071380380E1380380E2700700643003003820127E9124>I<381F004E61804681C04701 C08F01C08E01C00E01C00E01C01C03801C03801C03801C0700380710380710380E10380E 2070064030038014127E9119>I<00F800030C000E06001C030018030030030070038070 0380E00700E00700E00700E00E00E00E00E01C0060180060300030E0000F800011127E91 14>I<07078009C86008D03008E03011C03011C03801C03801C038038070038070038070 0380600700E00700C00701800783000E86000E78000E00000E00001C00001C00001C0000 1C00003C0000FF8000151A819115>I<01C206260C1E181E381C301C701C701CE038E038 E038E038E070E070E07060F023E01CE000E000E001C001C001C001C003C01FF80F1A7E91 13>I<383C4E424687470F8E1E8E0C0E000E001C001C001C001C00380038003800380070 00300010127E9113>I<01F0060C04040C0E180C1C001F000FE00FF003F80038201C7018 F018F010803060601F800F127E9113>I<00C001C001C001C00380038003800380FFF007 00070007000E000E000E000E001C001C001C001C00382038203840384018800F000C1A80 990F>I<1C00C02701C04701C04701C08703808703800E03800E03801C07001C07001C07 001C0700180E20180E20180E201C1E200C264007C38013127E9118>I<1C022707470747 03870187010E010E011C021C021C021C041804180818081C100C2007C010127E9114>I< 1C00C0802701C1C04701C1C04701C0C087038040870380400E0380400E0380401C070080 1C0700801C0700801C07010018060100180602001C0E02001C0F04000E13080003E1F000 1A127E911E>I<07878008C84010F0C020F1E020E3C040E18000E00000E00001C00001C0 0001C00001C000638080F38080F38100E5810084C60078780013127E9118>I E /Fz 21 120 df<000003800000000007C00000000007C0000000000FE0000000000FE0 000000000FE0000000001FF0000000001FF0000000003FF8000000003FF8000000003FF8 0000000073FC0000000073FC00000000F3FE00000000E1FE00000000E1FE00000001C0FF 00000001C0FF00000003C0FF80000003807F80000007807FC0000007003FC0000007003F C000000E003FE000000E001FE000001E001FF000001C000FF000001FFFFFF000003FFFFF F800003FFFFFF80000780007FC0000700003FC0000700003FC0000E00001FE0000E00001 FE0001E00001FF0001C00000FF0001C00000FF00FFFE001FFFFEFFFE001FFFFEFFFE001F FFFE2F297EA834>65 D<00003FF001800003FFFE0380000FFFFF8780003FF007DF8000FF 8001FF8001FE00007F8003FC00003F8007F000001F800FF000000F801FE0000007801FE0 000007803FC0000007803FC0000003807FC0000003807F80000003807F8000000000FF80 00000000FF8000000000FF8000000000FF8000000000FF8000000000FF8000000000FF80 00000000FF8000000000FF80000000007F80000000007F80000000007FC0000003803FC0 000003803FC0000003801FE0000003801FE0000007000FF00000070007F000000E0003FC 00001E0001FE00003C0000FF8000F800003FF007E000000FFFFFC0000003FFFF00000000 3FF8000029297CA832>67 D77 DI<007F806003FFF0E007FFF9 E00F807FE01F001FE03E0007E07C0003E07C0001E0FC0001E0FC0001E0FC0000E0FE0000 E0FE0000E0FF000000FFC000007FFE00007FFFE0003FFFFC001FFFFE000FFFFF8007FFFF C003FFFFE000FFFFE00007FFF000007FF000000FF8000007F8000003F8600001F8E00001 F8E00001F8E00001F8F00001F0F00001F0F80003F0FC0003E0FF0007C0FFE01F80F3FFFF 00E0FFFE00C01FF0001D297CA826>83 D<01FF800007FFF0000F81F8001FC07E001FC07E 001FC03F000F803F8007003F8000003F8000003F8000003F80000FFF8000FFFF8007FC3F 800FE03F803F803F803F003F807F003F80FE003F80FE003F80FE003F80FE003F807E007F 807F00DF803F839FFC0FFF0FFC01FC03FC1E1B7E9A21>97 D<001FF80000FFFE0003F01F 0007E03F800FC03F801F803F803F801F007F800E007F0000007F000000FF000000FF0000 00FF000000FF000000FF000000FF000000FF0000007F0000007F0000007F8000003F8001 C01F8001C00FC0038007E0070003F01E0000FFFC00001FE0001A1B7E9A1F>99 D<003FE00001FFF80003F07E0007C01F000F801F801F800F803F800FC07F000FC07F0007 C07F0007E0FF0007E0FF0007E0FFFFFFE0FFFFFFE0FF000000FF000000FF0000007F0000 007F0000007F0000003F8000E01F8000E00FC001C007E0038003F81F0000FFFE00001FF0 001B1B7E9A20>101 D<0007F0003FFC00FE3E01F87F03F87F03F07F07F07F07F03E07F0 0007F00007F00007F00007F00007F00007F000FFFFC0FFFFC0FFFFC007F00007F00007F0 0007F00007F00007F00007F00007F00007F00007F00007F00007F00007F00007F00007F0 0007F00007F00007F00007F00007F00007F0007FFF807FFF807FFF80182A7EA915>I<00 FF81F003FFE7F80FC1FE7C1F80FC7C1F007C383F007E107F007F007F007F007F007F007F 007F007F007F007F007F003F007E001F007C001F80FC000FC1F8001FFFE00018FF800038 000000380000003C0000003E0000003FFFF8001FFFFF001FFFFF800FFFFFC007FFFFE01F FFFFF03E0007F07C0001F8F80000F8F80000F8F80000F8F80000F87C0001F03C0001E01F 0007C00FC01F8003FFFE00007FF0001E287E9A22>II<07000F801FC03FE03FE03FE01F C00F8007000000000000000000000000000000FFE0FFE0FFE00FE00FE00FE00FE00FE00F E00FE00FE00FE00FE00FE00FE00FE00FE00FE00FE00FE00FE00FE00FE00FE0FFFEFFFEFF FE0F2B7DAA14>I108 DII<003FE00001FFFC0003F07E000FC01F801F800FC03F 800FE03F0007E07F0007F07F0007F07F0007F0FF0007F8FF0007F8FF0007F8FF0007F8FF 0007F8FF0007F8FF0007F8FF0007F87F0007F07F0007F03F800FE03F800FE01F800FC00F C01F8007F07F0001FFFC00003FE0001D1B7E9A22>I114 D<03FE300FFFF01E03F03800F0700070F00070F00070F80070FC0000FFE0007FFE 007FFF803FFFE01FFFF007FFF800FFF80003FC0000FC60007CE0003CF0003CF00038F800 38FC0070FF01E0F7FFC0C1FF00161B7E9A1B>I<00700000700000700000700000F00000 F00000F00001F00003F00003F00007F0001FFFF0FFFFF0FFFFF007F00007F00007F00007 F00007F00007F00007F00007F00007F00007F00007F00007F00007F00007F03807F03807 F03807F03807F03807F03803F03803F87001F86000FFC0001F8015267FA51B>II119 D E end %%EndProlog %%BeginSetup %%Feature: *Resolution 300dpi TeXDict begin %%PaperSize: A4 %%EndSetup %%Page: 1 1 1 0 bop 293 194 a Fz(A)23 b(New)f(Calculus)f(for)j(Seman)n(tic)d(Matc)n (hing)1491 172 y Fy(?)288 339 y Fx(Bernd)15 b(B)q(\177)-22 b(uto)o(w,)14 b(Rob)q(ert)g(Giegeric)o(h,)f(Enno)h(Ohlebusc)o(h,)h (Stephan)f(Thesing)524 426 y Fw(T)m(ec)o(hnisc)o(he)g(F)m(akult\177)-19 b(at)15 b(der)e(Univ)o(ersit\177)-19 b(at)15 b(Bielefeld)541 472 y(P)o(ostfac)o(h)f(100131,)f(33501)h(Bielefeld,)h(German)o(y)374 517 y Fv(f)p Fu(berndb|rob)o(ert)o(|e)o(nno)o(|i)o(sth)o(esi)o(n)p Fv(g)p Fu(@t)o(ec)o(hfa)o(k.)o(uni)o(-bi)o(el)o(efe)o(ld)o(.de)301 696 y Ft(Abstract.)22 b Fw(In)9 b(this)h(pap)q(er,)g(w)o(e)e(presen)o (t)i(Rev)o(erse)g(Restructuring,)h(a)e(new)g(calcu-)301 741 y(lus)k(for)e(solving)j(the)e(seman)o(tic)h(matc)o(hing)g(problem.) g(F)m(or)f(narro)o(wing,)h(adv)n(anced)301 787 y(selection)e(rules)f (are)f(commonly)h(seen)g(as)f(an)g(appropriate)i(metho)q(d)f(to)e (reduce)i(the)301 833 y(searc)o(h)j(space.)g(Our)g(approac)o(h)h(to)e (design)j(a)d(sp)q(ecial)j(calculus)g(for)d(sp)q(ecial)j(goals)301 878 y(is)h(another)g(w)o(a)o(y)g(of)f(reducing)i(the)f(e\016ciency)h (defects)f(of)f(narro)o(wing.)i(Rev)o(erse)301 924 y(Restructuring)d (constructs)e(deriv)n(ations)i(in)f(the)f(rev)o(erse)g(direction)h(b)o (y)f(guessing)301 969 y(terms)g(from)f(whic)o(h)i(an)f(already)h(kno)o (wn)g(term)e(migh)o(t)i(b)q(e)f(deriv)o(ed.)h(T)m(o)e(this)i(end,)301 1015 y(the)f(rules)h(of)f(the)g(underlying)j(term)d(rewriting)h(system) g(are)f(also)h(applied)h(in)f(the)301 1061 y(rev)o(erse)e(direction,)h (i.e.)f(from)f(righ)o(t)i(to)e(left.)h(W)m(e)g(sho)o(w)g(the)g (soundness)h(and)f(com-)301 1106 y(pleteness)i(of)e(this)h(calculus)i (and)e(demonstrate)g(its)g(e\016ciency)h(for)e(an)h(imp)q(ortan)o(t)301 1152 y(class)i(of)f(problems.)183 1299 y Fs(1)56 b(In)n(tro)r(duction) 183 1404 y Fx(Narro)o(wing)10 b(is)h(commonl)o(y)d(seen)k(as)f(the)h (basis)f(for)f(the)i(amalgam)o(a)o(tion)c(of)i(logic)g(and)g(func-)183 1453 y(tional)h(programming.)e(Narro)o(wing)j(to)q(da)o(y)g(refers)i (to)f(a)f(whole)h(family)d(of)i(pro)q(cedures)j(for)183 1503 y(solving)9 b(equational)h(goals)g Fy(s)i Fx(=)682 1509 y Fr(?)712 1503 y Fy(t)f Fx(in)f(the)i(equational)e(theory)h (de\014ned)h(b)o(y)f(a)g(term)f(rewrit-)183 1553 y(ing)g(system)h (\(TRS\))g Fq(R)p Fx(.)g(The)h(dev)o(elopmen)o(t)e(of)h(di\013eren)o(t) h(narro)o(wing)f(strategies)h(is)f(driv)o(en)183 1603 y(b)o(y)16 b(the)h(need)h(to)e(impro)o(v)o(e)f(e\016ciency)i(b)o(y)f (cutting)h(do)o(wn)f(the)h(searc)o(h)h(space.)f(Most)g(ap-)183 1653 y(proac)o(hes)11 b(require)h(certain)g(restrictions)g(on)e(the)i (TRS)e(in)h(order)g(to)g(ensure)h(completeness.)183 1702 y(A)f(certain)h(endp)q(oin)o(t)g(in)f(this)g(line)g(of)g(dev)o(elopmen) o(t)f(is)h(curren)o(tly)i(mark)o(ed)d(b)o(y)h(the)h(needed)183 1752 y(narro)o(wing)e(strategy)j(of)d(An)o(to)o(y)i(et)g(al.)e ([AEH94],)g(where)j(a)e(relativ)o(ely)g(complex)f(selection)183 1802 y(rule)17 b(ensures)h(that)f(no)g(\\unnecessary")h(narro)o(wing)e (step)i(is)e(done.)h(The)g(price)h(paid)e(b)o(y)183 1852 y(this)e(strategy)g(is)g(a)g(sev)o(ere)h(restriction)g(on)f(the)g (underlying)g(TRSs.)245 1903 y(Another)k(line)f(of)f(attac)o(king)h (the)h(e\016ciency)g(defects)h(of)d(narro)o(wing)h(is)g(the)h(idea)f (to)183 1953 y(design)i(sp)q(ecial)g(calculi)f(for)h(sp)q(ecial)g (goals.)f(Of)g(course,)i(this)f(idea)g(mak)o(es)f(only)g(sense)183 2002 y(if)f(the)i(subgoals)f(arising)g(in)f(a)h(computation)f(ha)o(v)o (e)h(the)h(same)f(restricted)i(form.)c(Suc)o(h)183 2052 y(an)e(approac)o(h)h(w)o(as)g(\014rst)g(suggested)i(b)o(y)d(Dersho)o (witz)i(et)f(al.)f([DMS92)o(],)f(in)o(tro)q(ducing)i(the)183 2102 y(problem)j(of)i(seman)o(tic)f(matc)o(hing:)f(Giv)o(en)h(an)h (arbitrary)f(term)h Fy(s)g Fx(and)g(a)g(term)f Fy(N)25 b Fx(in)183 2152 y(ground)13 b(normal)f(form,)g(\014nd)i(a)g (substitution)g Fy(\033)h Fx(suc)o(h)f(that)g Fy(s\033)f Fx(=)1233 2158 y Fp(R)1276 2152 y Fy(N)5 b Fx(.)245 2203 y(A)o(t)15 b(\014rst)h(glance,)f(this)h(do)q(es)g(not)f(seem)g(to)g(b)q (e)h(a)f(problem)f(w)o(orth)i(individual)d(study)m(.)183 2252 y(It)18 b(is)g(a)g(common)d(tec)o(hnical)k(device)g(to)f (transform)f(general)i(narro)o(wing)e(goals)h Fy(s)h Fx(=)1572 2258 y Fr(?)1609 2252 y Fy(t)183 2302 y Fx(in)o(to)f(the)i (form)d Fy(eq)q Fx(\()p Fy(s;)7 b(t)p Fx(\))21 b(=)629 2308 y Fr(?)667 2302 y Fy(tr)q(ue)e Fx(b)o(y)g(means)f(of)h(the)g (extra)h(rule)f Fy(eq)q Fx(\()p Fy(X)q(;)7 b(X)s Fx(\))21 b Fq(!)f Fy(tr)q(ue)p Fx(.)p 183 2343 237 2 v 190 2370 a Fo(?)221 2386 y Fw(This)d(w)o(ork)f(is)h(supp)q(orted)h(b)o(y)f(the)f (DF)o(G-pro)r(ject:)h(\\Abstrakte)g(Inferenzmasc)o(hine")h(under)221 2432 y(Az.)12 b(Gi)i(178/1-2)p eop %%Page: 2 2 2 1 bop 340 194 a Fx(In)20 b(this)h(sense,)g(all)e(seman)o(tic)g (uni\014cation)h(problems)f(can)h(b)q(e)h(turned)g(in)o(to)e(seman)o (tic)340 244 y(matc)o(hing)11 b(problems,)g(and)i(w)o(e)g(cannot)f(exp) q(ect)j(a)d(seman)o(tic)g(matc)o(hing)e(calculus)j(to)g(o\013er)340 293 y(an)o(y)h(adv)n(an)o(tages.)403 345 y(Ho)o(w)o(ev)o(er,)g(the)i (situation)e(c)o(hanges)h(if)f(w)o(e)h(restrict)i(the)e(underlying)g (TRS)f Fq(R)h Fx(to)g(left-)340 394 y(linear)f(or)h(v)n (ariable-preserving)f(rules.)g(Note)h(that)g(the)g(rule)f Fy(eq)q Fx(\()p Fy(X)q(;)7 b(X)s Fx(\))14 b Fq(!)e Fy(tr)q(ue)i Fx(violates)340 444 y(either)i(restriction.)e(In)h(this)f(setting,)g (Dersho)o(witz)h(et)g(al.)e([DMS92)o(])g(ga)o(v)o(e)h(a)g(calculus)h (for)340 494 y(seman)o(tic)e(matc)o(hing)f(whic)o(h)i(is)g(sound)g(and) g(complete.)403 545 y(The)e(class)g(of)f(problems)f(whic)o(h)i(can)g(b) q(e)g(solv)o(ed)f(b)o(y)h(seman)o(tic)e(matc)o(hing)g(is)i(still)e (quite)340 595 y(in)o(teresting.)i(In)f(particular,)f(function)h(in)o (v)o(ersion)g(b)q(elongs)g(to)g(this)g(class,)h(i.e.)e(goals)g(of)h (the)340 645 y(form)d Fy(f)t Fx(\()p Fy(X)s Fx(\))14 b(=)573 651 y Fr(?)602 645 y Fy(N)5 b Fx(.)k(It)h(has)g(b)q(een)g (observ)o(ed)h(in)e([Gie90)o(])g(that)h(compiler)e(co)q(de)j(selection) f(can)340 695 y(b)q(e)15 b(seen)h(as)f(solving)e(an)h(equation)g Fy(\016)r Fx(\()p Fy(X)s Fx(\))g(=)1043 701 y Fr(?)1073 695 y Fy(il)q(pr)q(og)q Fx(,)h(where)g Fy(il)q(pr)q(og)i Fx(is)d(an)g(in)o(termediate)340 745 y(language)k(program,)e(and)i Fy(\016)j Fx(is)d(a)g(deriv)o(or)h(mapping)d(target)j(mac)o(hine)e (programs)g(in)o(to)340 794 y(in)o(termediate)i(language)g(programs.)e (\(W)m(e)j(shall)e(elab)q(orate)i(this)f(example)g(in)g(section)340 844 y(4.2.\))d(Curren)o(t)i(compiler)d(tec)o(hnology)i([ESL89)o(,)f (Gie90)o(,)h(FHP92,)f(Emm94)m(])g(solv)o(es)h(this)340 894 y(problem)c(with)g(an)h(e\016ciency)h(whic)o(h)f(narro)o(wing)f (pro)q(cedures)j(can)e(only)f(dream)g(of.)403 945 y(The)e(o)o(v)o (erall)f(goal)g(of)g(our)h(w)o(ork)g(is)g(to)g(impro)o(v)o(e)e(the)j (e\016ciency)g(of)e(seman)o(tic)g(matc)o(hing)340 995 y(while)16 b(at)f(the)i(same)e(time)f(impro)o(ving)f(the)k (\015exibilit)o(y)d(of)h(co)q(de)i(selection)g(mec)o(hanisms.)340 1045 y(The)c(presen)o(t)h(pap)q(er)f(is)f(a)g(\014rst)h(step)h(in)e (this)g(direction.)g(Our)h(basic)f(idea)g(is)h(as)f(follo)o(ws:)e(In) 340 1095 y(solving)i Fy(f)t Fx(\()p Fy(X)s Fx(\))i(=)618 1101 y Fr(?)647 1095 y Fy(N)5 b Fx(,)13 b(w)o(e)g(try)h(to)f(exploit)f (the)i(fact)f(that)g Fy(N)19 b Fx(is)13 b(in)f(ground)h(normal)f(form.) 340 1145 y(Rather)17 b(than)f(guessing)g(instan)o(tiations)f(of)h Fy(X)k Fx(that)c(successiv)o(ely)i(construct)f(a)f(rewrite)340 1194 y(deriv)n(ation)g Fy(f)t Fx(\()p Fy(X)s(\033)q Fx(\))h Fq(!)715 1200 y Fp(R)761 1194 y Fy(N)5 b Fx(,)16 b(w)o(e)g(construct)i (this)f(deriv)n(ation)e(in)h(the)h(rev)o(erse)h(direction)340 1244 y(b)o(y)g(guessing)g(terms)g(from)e(whic)o(h)i Fy(N)23 b Fx(can)18 b(b)q(e)g(deriv)o(ed.)g(In)g(this)g(pap)q(er,)g(w)o(e)h(in) o(tro)q(duce)340 1294 y(the)13 b(Rev)o(erse)f(Restructuring)h (calculus,)e(sho)o(w)h(its)g(soundness)h(and)e(completeness)h(for)g (the)340 1344 y(seman)o(tic)k(matc)o(hing)f(problem,)g(and)h(outline)g (some)g(optimizations.)e(F)m(urthermore,)i(w)o(e)340 1394 y(will)11 b(pro)o(vide)g(the)h(Rev)o(erse)h(Restructuring)g (computation)d(with)h(some)g(kno)o(wledge)g(ab)q(out)340 1443 y(the)16 b(forw)o(ard)f(computation)f(paths)h(resulting)h(in)f(a)g (further)h(considerable)g(reduction)g(of)340 1493 y(the)f(searc)o(h)g (space.)f(More)h(details)e(and)h(full)f(pro)q(ofs)h(can)g(b)q(e)g (found)g(in)f([BT94].)340 1635 y Fs(2)56 b(Preliminaries)340 1742 y Fn(2.1)48 b(Notations)340 1832 y Fx(In)14 b(this)g(section)h(w)o (e)f(brie\015y)g(recall)g(basic)g(notions)f(of)h(term)f(rewriting)h (\(see)h(for)f(example)340 1882 y([DJ90)o(,)g(Klo92)o(])f(for)h(more)f (details\).)403 1934 y(A)i Fm(signatur)n(e)g Fx(is)f(a)h(set)h Fy(\006)i Fx(of)c Fm(op)n(er)n(ators)p Fx(.)g(Ev)o(ery)i Fy(f)i Fq(2)13 b Fy(\006)18 b Fx(is)d(com)o(bined)e(with)i(an)g Fm(arity)340 1983 y Fy(n)p Fx(,)f Fy(n)d Fq(\025)h Fx(0.)i(Let)g Fy(X)s Fx(,)g Fy(X)f Fq(\\)c Fy(\006)15 b Fx(=)d Fq(;)p Fx(,)h(b)q(e)i(a)e(coun)o(table)i(in\014nite)e(set)i(of)f Fy(v)q(ar)q(iabl)q(es)p Fx(.)h(W)m(e)e(de\014ne)340 2033 y(the)k(set)f(of)f Fm(terms)j Fq(T)10 b Fx(\()p Fy(\006)r(;)d(X)s Fx(\))17 b(with)e(v)n(ariables)g(as)h(the)g(smallest)e(set)j(con)o (taining)d Fy(X)20 b Fx(suc)o(h)340 2083 y(that)13 b Fy(f)t Fx(\()p Fy(t)484 2089 y Fr(1)504 2083 y Fy(;)7 b(:)g(:)g(:)e(;)i(t)612 2089 y Fl(n)634 2083 y Fx(\))12 b Fq(2)f(T)f Fx(\()p Fy(\006)r(;)d(X)s Fx(\))14 b(if)e Fy(f)18 b Fx(has)13 b(arit)o(y)g Fy(n)g Fx(and)f Fy(t)1249 2089 y Fr(1)1268 2083 y Fy(;)7 b(:)g(:)g(:)e(;)i(t)1376 2089 y Fl(n)1409 2083 y Fq(2)12 b(T)e Fx(\()p Fy(\006)r(;)d(X)s Fx(\).)13 b(By)h Fq(V)s Fx(\()p Fy(t)p Fx(\),)340 2133 y(w)o(e)19 b(denote)h(the)f(set)g(of)f(v)n(ariables)g(o)q(ccurring)h (in)f(the)i(term)e Fy(t)p Fx(.)g(If)g Fq(V)s Fx(\()p Fy(t)p Fx(\))i(=)g Fq(;)p Fx(,)e Fy(t)g Fx(is)h(said)340 2183 y(to)d(b)q(e)g Fy(g)q(r)q(ound)p Fx(.)f(An)g Fy(occur)q(r)q(ence)h (p)f Fx(in)g(a)h(term)f Fy(t)g Fx(is)h(de\014ned)g(as)g(a)f(sequence)j (of)d(natural)340 2232 y(n)o(um)o(b)q(ers)c(iden)o(tifying)f(a)h (subterm)g(in)g Fy(t)p Fx(.)g(The)h(empt)o(y)e(sequence,)j(denoted)f(b) o(y)f Fy(\017)p Fx(,)g(iden)o(ti\014es)340 2282 y(for)h(ev)o(ery)i (term)d Fy(t)i Fx(the)g(whole)f(term)f(itself.)h(F)m(or)g(ev)o(ery)h (term)f Fy(f)t Fx(\()p Fy(t)1364 2288 y Fr(1)1383 2282 y Fy(;)7 b(:)g(:)g(:)e(;)i(t)1491 2288 y Fl(n)1513 2282 y Fx(\),)12 b(the)h(sequence)340 2332 y Fy(i:p)19 b Fx(where)h Fy(i)g Fq(\024)h Fy(n)e Fx(and)f Fy(p)h Fx(is)g(an)g(o)q(ccurrence)j (in)c Fy(t)1177 2338 y Fl(i)1191 2332 y Fx(,)g(iden)o(ti\014es)i(the)f (subterm)g(of)g Fy(t)1712 2338 y Fl(i)1744 2332 y Fx(at)340 2382 y(o)q(ccurrence)h Fy(p)p Fx(.)d Fy(t=p)g Fx(denotes)h(the)g Fy(subter)q(m)g Fx(of)e Fy(t)h Fx(at)g(o)q(ccurrence)j Fy(p)p Fx(;)d Fy(t)p Fx([)p Fy(p)f Fq( )h Fy(t)1605 2367 y Fp(0)1616 2382 y Fx(])g(denotes)340 2432 y(the)g(term)f(obtained)g (from)e Fy(t)i Fx(b)o(y)g(replacing)g Fy(t=p)g Fx(b)o(y)g Fy(t)1208 2417 y Fp(0)1219 2432 y Fx(.)g(W)m(e)g(de\014ne)h(the)g Fm(pr)n(e\014x)g(or)n(dering)1050 2556 y Fx(2)p eop %%Page: 3 3 3 2 bop 183 194 a Fq(\024)12 b(\032)20 b Fk(I)-6 b(N)315 175 y Fp(\003)346 194 y Fq(\002)13 b Fk(I)-6 b(N)426 175 y Fp(\003)464 194 y Fx(on)19 b(o)q(ccurrences)j(as)c(follo)o(ws:)f Fy(u)i Fq(\024)h Fy(v)i Fq(,)d(9)p Fy(w)h Fx(:)f Fy(u:w)h Fx(=)g Fy(v)q Fx(.)f(W)m(e)f(write)183 244 y Fy(v)h(>)f(u)g Fx(i\013)f Fy(u)h Fq(\024)g Fy(v)i Fx(and)d Fy(u)h Fq(6)p Fx(=)g Fy(v)q Fx(.)g(With)f Fy(r)q(oot)p Fx(\()p Fy(t)p Fx(\),)h(w)o(e)g(refer)h(to)e(the)i(outermost)e(sym)o(b)q(ol,)183 293 y(i.e.)d Fy(r)q(oot)p Fx(\()p Fy(t)p Fx(\))g(=)g Fy(f)20 b Fx(if)14 b Fy(t)g Fq(\021)g Fy(f)t Fx(\()p Fy(t)642 299 y Fr(1)662 293 y Fy(;)7 b(:)g(:)g(:)e(;)i(t)770 299 y Fl(n)792 293 y Fx(\))15 b(\(the)h(sym)o(b)q(ol)d Fq(\021)j Fx(denotes)g(syn)o(tactical)f(equalit)o(y\))183 343 y(and)g Fy(r)q(oot)p Fx(\()p Fy(t)p Fx(\))g(=)h Fy(t)f Fx(if)g Fy(t)g Fq(2)g Fy(X)s Fx(.)g(A)h Fm(substitution)j Fx(is)d(a)g(mapping)d Fy(\033)j Fx(:)e Fy(X)19 b Fq(!)14 b(T)c Fx(\()p Fy(\006)r(;)d(X)s Fx(\),)17 b(suc)o(h)183 393 y(that)g Fq(D)q Fx(\()p Fy(\033)q Fx(\))g(:=)f Fq(f)p Fy(x)g Fq(2)g Fy(X)h Fq(j)12 b Fy(\033)q Fx(\()p Fy(x)p Fx(\))k Fq(6)p Fx(=)h Fy(x)p Fq(g)f Fx(is)h(a)g(\014nite)g(set.)g Fq(D)q Fx(\()p Fy(\033)q Fx(\))h(denotes)g(the)f Fm(domain)k Fx(of)183 443 y Fy(\033)q Fx(.)16 b(Since)h Fq(D)q Fx(\()p Fy(\033)q Fx(\))g(is)f(\014nite,)h(w)o(e)f(can)h(represen)o(t)i Fy(\033)f Fx(as)e(a)g(\014nite)h(subset)h(of)e Fy(X)e Fq(\002)e(T)e Fx(\()p Fy(\006)r(;)d(X)s Fx(\):)183 493 y Fy(\033)21 b Fx(=)f Fq(f)p Fy(x)325 499 y Fr(1)363 493 y Fq( )g Fy(t)440 499 y Fr(1)459 493 y Fy(;)7 b(:)g(:)g(:)t(;)g(x) 575 499 y Fl(n)617 493 y Fq( )20 b Fy(t)694 499 y Fl(n)716 493 y Fq(g)p Fx(,)f(where)h Fy(x)917 499 y Fl(i)950 493 y Fq(6)p Fx(=)h Fy(x)1027 499 y Fl(j)1064 493 y Fq(,)f Fy(i)g Fq(6)p Fx(=)g Fy(j)r Fx(.)f(In)g(the)h(follo)o(wing)c(w)o(e)183 542 y(write)c Fy(x\033)h Fx(for)f Fy(\033)q Fx(\()p Fy(x)p Fx(\).)g Fq(I)s Fx(\()p Fy(\033)q Fx(\))g(:=)665 511 y Fj(S)700 555 y Fl(x)p Fp(2D)q Fr(\()p Fl(\033)q Fr(\))823 542 y Fq(V)s Fx(\()p Fy(x\033)q Fx(\))i(is)e(the)h(set)g(of)f Fm(variables)h(intr)n(o)n(duc)n(e)n(d)f Fx(b)o(y)g Fy(\033)q Fx(.)183 592 y(F)m(urthermore,)j(w)o(e)i(de\014ne)g(the)f Fm(r)n(estriction)f Fx(of)h(a)f(substitution)i Fy(\033)g Fx(to)f(a)g(set)h(of)e(v)n(ariables)183 642 y Fy(V)30 b Fq(\022)21 b Fy(X)i Fx(as)c Fy(\033)427 649 y Fp(j)p Fl(V)486 642 y Fx(:=)i Fq(f)p Fy(x)f Fq( )g Fy(t)g Fq(2)h Fy(\033)13 b Fq(j)f Fy(x)21 b Fq(2)f Fy(V)10 b Fq(g)p Fx(.)18 b(The)i(extension)g(of)f(substitutions)h(to)183 692 y(terms)9 b(is)g(straigh)o(tforw)o(ard,)f(w)o(e)i(de\014ne)g Fy(\033)j Fx(:)e Fq(T)f Fx(\()p Fy(\006)r(;)d(X)s Fx(\))13 b Fq(!)e(T)f Fx(\()p Fy(\006)r(;)d(X)s Fx(\))k(b)o(y)e Fy(\033)q Fx(\()p Fy(f)t Fx(\()p Fy(t)1398 698 y Fr(1)1418 692 y Fy(;)e(:)g(:)g(:)t(;)g(t)1525 698 y Fl(n)1547 692 y Fx(\)\))12 b(=)183 742 y Fy(f)t Fx(\()p Fy(\033)q Fx(\()p Fy(t)279 748 y Fr(1)299 742 y Fx(\))p Fy(;)7 b(:)g(:)g(:)t(;)g(\033)q Fx(\()p Fy(t)463 748 y Fl(n)486 742 y Fx(\)\))20 b(for)f(ev)o(ery)i (term)e Fy(f)t Fx(\()p Fy(t)883 748 y Fr(1)902 742 y Fy(;)7 b(:)g(:)g(:)e(;)i(t)1010 748 y Fl(n)1032 742 y Fx(\).)19 b(F)m(or)h(substitutions)g Fy(\033)15 b Fx(and)e Fy(\025)20 b Fx(w)o(e)183 791 y(de\014ne)15 b Fy(\033)d Fq(\024)g Fy(\025;)21 b Fx(i\013)13 b Fq(9)h Fx(substitution)g Fy(\022)f Fx(:)e Fy(\033)q(\022)j Fx(=)e Fy(\025)p Fx(.)245 853 y(A)i(term)g Fy(s)g(matches)h Fx(a)f(term)g Fy(t)g Fx(if)f Fy(s\033)h Fq(\021)e Fy(t)i Fx(for)g(a)g(substitution)g Fy(\033)q Fx(.)g(A)h(term)e Fy(s)i(unif)t(ies)183 903 y Fx(with)h(a)g(term)g Fy(t)h Fx(if)f Fy(s\033)i Fq(\021)e Fy(t\033)i Fx(for)f(a)f(substitution)h Fy(\033)q Fx(.)f(A)h (substitution)g Fy(\033)h Fx(is)e(called)h Fm(most)183 952 y(gener)n(al)f(uni\014er)h(\(mgu\))f Fx(of)f(t)o(w)o(o)g(terms)g Fy(s)i Fx(and)e Fy(t)h Fx(if,)e(for)h(an)o(y)h(other)g(uni\014er)g Fy(\033)1445 937 y Fp(0)1473 952 y Fx(of)f Fy(s)h Fx(and)183 1002 y Fy(t)p Fx(,)g(there)h(exists)g(a)g(substitution)f Fy(\015)j Fx(suc)o(h)f(that)e Fy(\033)976 987 y Fp(0)1004 1002 y Fx(=)g Fy(\033)q(\015)r Fx(.)h(If)f Fy(s)h Fx(and)f Fy(t)g Fx(are)h(uni\014able)f(the)183 1052 y Fy(mg)q(u)p Fx(\()p Fy(s;)7 b(t)p Fx(\))14 b(exists)h(and)f(is)f(unique)h(up)g(to)g Fm(variable)g(r)n(enaming)p Fx(.)245 1113 y(A)h(rewrite)h(rule)f(is)g (an)g(ordered)h(pair)f Fy(l)g Fq(!)d Fy(r)k Fx(from)e Fq(T)c Fx(\()p Fy(\006)r(;)d(X)s Fx(\))k Fq(\002)f(T)g Fx(\()p Fy(\006)r(;)d(X)s Fx(\))16 b(satisfying)183 1163 y(the)c(additional)e(conditions)i Fq(V)s Fx(\()p Fy(l)q Fx(\))h Fq(\023)f(V)s Fx(\()p Fy(r)q Fx(\))g(and)g Fy(l)h Fq(62)e Fy(X)s Fx(.)h(W)m(e)g(sp)q(eak)g(of)g(a)f Fm(c)n(ol)r(lapsing)h Fx(rule)g(if)183 1213 y Fy(r)g Fq(2)f Fy(X)s Fx(.)i(A)g(term)f (rewriting)g(system)g(\(TRS\))h(is)f(a)g(set)i(of)e(rules.)h(A)f(term)g Fy(t)h Fm(r)n(ewrites)d Fx(in)i(one)183 1263 y(step)i(to)f Fy(t)335 1248 y Fp(0)361 1263 y Fx(at)g(o)q(ccurrence)j Fy(p)d Fx(\(in)h(sym)o(b)q(ols:)d Fy(t)h Fq(!)954 1269 y Fl(l)p Fp(!)p Fl(r)o(;p;\033)1082 1263 y Fy(t)1097 1248 y Fp(0)1109 1263 y Fx(\))h(if)g(there)i(is)e(a)g(rule)h Fy(l)f Fq(!)e Fy(r)h Fq(2)f(R)183 1313 y Fx(and)i(a)g(\(smallest\))f (substitution)h Fy(\033)i Fx(with)d Fy(t=p)g Fq(\021)f Fy(l)q(\033)k Fx(and)e Fy(t)1109 1298 y Fp(0)1132 1313 y Fq(\021)f Fy(t)p Fx([)p Fy(p)f Fq( )g Fy(r)q(\033)q Fx(].)h(Sometimes)f(w)o(e)183 1363 y(just)16 b(write)g Fq(!)f Fx(or)g Fq(!)526 1369 y Fp(R)572 1363 y Fx(instead)h(of)f Fq(!)808 1369 y Fl(l)p Fp(!)p Fl(r)o(;p;\033)925 1363 y Fx(.)g(The)i(sym)o(b)q(ol)d Fq(!)1226 1347 y Fl(n)1226 1374 y Fp(R)1271 1363 y Fx(denotes)j(a)f(rewriting)183 1412 y(deriv)n(ation)i(in)g Fy(n)h Fx(steps;)h(in)e(analogy)m(,)f(w)o (e)i(de\014ne)h Fq(!)1054 1396 y Fl(p)1532 2022 y Fx(:)j Fy(t=p)1612 2007 y Fp(0)183 2071 y Fx(is)i(in)h(normal)e (form.)f(A)j(rewriting)g(deriv)n(ation)f(is)h(called)g Fm(innermost)j Fx(i\013)d(ev)o(ery)h(step)f(in)g(it)183 2121 y(is)e(innermost.)g(In)h(a)f(canonical)g(TRS)g Fq(R)h Fx(t)o(w)o(o)g(terms)f Fy(t;)7 b(t)1078 2106 y Fp(0)1102 2121 y Fx(are)13 b(de\014ned)h(to)f(b)q(e)g Fm(joinable)j Fx(\(in)183 2171 y(sym)o(b)q(ols:)10 b Fy(t)h Fx(=)409 2177 y Fp(R)452 2171 y Fy(t)467 2156 y Fp(0)478 2171 y Fx(\))i(i\013)e Fy(t)-5 b Fq(#\021)12 b Fy(t)644 2156 y Fp(0)650 2171 y Fq(#)p Fx(.)g(A)g Fm(go)n(al)k Fx(is)c(a)g(pair)g(\() p Fy(t;)7 b(t)1046 2156 y Fp(0)1057 2171 y Fx(\))12 b Fq(2)f(T)f Fx(\()p Fy(\006)r(;)d(X)s Fx(\))f Fq(\002)g(T)11 b Fx(\()p Fy(\006)r(;)c(X)s Fx(\))13 b(written)183 2221 y(as)j Fy(t)g Fx(=)299 2227 y Fr(?)333 2221 y Fy(t)348 2206 y Fp(0)360 2221 y Fx(.)g(An)h Fq(R)p Fm(-uni\014er)g Fx(of)f(this)g(goal)f(is)i(a)f(substitution)h Fy(\033)h Fx(suc)o(h)f(that:)f Fy(t\033)h Fx(=)1513 2227 y Fp(R)1560 2221 y Fy(t)1575 2206 y Fp(0)1587 2221 y Fy(\033)q Fx(.)183 2271 y(The)d(relation)f Fq(\024)452 2277 y Fp(R)497 2271 y Fx(on)h(substitutions)g(is)g(de\014ned)h(analogous)d(to)i Fq(\024)p Fx(.)245 2332 y(F)m(or)g(substitutions)g Fy(\033)o(;)7 b(\025;)g(\022)15 b Fx(w)o(e)g(de\014ne)g(the)g(follo)o(wing)c(prop)q (erties:)k Fy(\033)h Fx(is)e(called)g Fm(idem-)183 2382 y(p)n(otent)22 b Fx(i\013)c Fq(8)392 2389 y Fl(x)p Fp(2D)q Fr(\()p Fl(\033)q Fr(\))527 2382 y Fx(:)g Fy(x\033)q(\033)i Fq(\021)f Fy(x\033)q Fx(;)f Fy(\033)i Fx(=)f Fy(\025)p Fx([)p Fy(V)9 b Fx(])17 b(i\013)h Fy(\033)1051 2389 y Fp(j)p Fl(V)1108 2382 y Fx(=)h Fy(\025)1183 2389 y Fp(j)p Fl(V)1222 2382 y Fx(,)f(analogously)e(for)i(=)1581 2388 y Fp(R)1612 2382 y Fx(:)183 2432 y Fy(\033)j Fx(=)260 2438 y Fp(R)310 2432 y Fy(\025)p Fx([)p Fy(V)9 b Fx(])19 b(i\013)f Fq(8)487 2438 y Fl(x)p Fp(2)p Fl(V)577 2432 y Fx(:)h Fy(x\033)i Fx(=)709 2438 y Fp(R)760 2432 y Fy(x\025)p Fx(;)d Fy(\033)j Fq(\024)f Fy(\025)p Fx([)p Fy(V)9 b Fx(])18 b(i\013)h Fq(9)p Fy(\022)i Fx(:)f Fy(\033)q(\022)h Fx(=)f Fy(\025)p Fx([)p Fy(V)10 b Fx(],)17 b(analogously)893 2556 y(3)p eop %%Page: 4 4 4 3 bop 340 194 a Fx(for)20 b(=)442 200 y Fp(R)473 194 y Fx(:)f Fy(\033)k Fq(\024)583 200 y Fp(R)635 194 y Fy(\025)p Fx([)p Fy(V)10 b Fx(])19 b(i\013)h Fq(9)p Fy(\022)j Fx(:)e Fy(\033)q(\022)j Fx(=)990 200 y Fp(R)1042 194 y Fy(\025)p Fx([)p Fy(V)9 b Fx(].)19 b Fy(\033)i Fx(is)f(called)g Fm(gr)n(ound)h(substitution)i Fx(i\013)340 244 y Fq(8)363 251 y Fl(x)p Fp(2D)q Fr(\()p Fl(\033)q Fr(\))500 244 y Fx(:)d Fy(x\033)g Fx(is)f(a)g(ground)g(term;)f(it)h(is)g(called)g Fm(normalize)n(d)k Fx(i\013)c Fq(8)1463 251 y Fl(x)p Fp(2D)q Fr(\()p Fl(\033)q Fr(\))1600 244 y Fx(:)h Fy(x\033)g Fx(is)f(in)340 293 y(normal)12 b(form)g(and)i(it)g(is)f(called)h Fm(line)n(ar)k Fx(i\013)13 b Fq(8)1054 300 y Fl(x)p Fp(2D)q Fr(\()p Fl(\033)q Fr(\))1182 293 y Fx(:)e Fy(x\033)k Fx(is)f(a)f(linear)h(term.)340 344 y(The)h(follo)o(wing)c(prop)q (erties)k(of)f(substitutions)g(will)e(b)q(e)j(used)g(later:)340 416 y Fn(Lemma)h(2.1)g(:)356 491 y Fm(1.)21 b(Equivalenc)n(e)15 b(\()p Fq(\021)p Fm(\))h(is)e(pr)n(eserve)n(d)h(under)g(substitutions,) f(i.e.)g Fy(s)e Fq(\021)g Fy(t)g Fq(\))f Fy(s\033)i Fq(\021)f Fy(t\033)i Fq(8)p Fy(\033)q Fm(.)356 541 y(2.)21 b(If)15 b Fq(R)h Fm(is)f(a)g(c)n(anonic)n(al)h(TRS,)g(then)g(joinability)e(\()p Fx(=)1219 547 y Fp(R)1250 541 y Fm(\))i(is)f(pr)n(eserve)n(d)g(under)h (substitu-)411 591 y(tions,)f(i.e.)f Fy(s)e Fx(=)662 597 y Fp(R)705 591 y Fy(t)f Fq(\))g Fy(s\033)j Fx(=)873 597 y Fp(R)915 591 y Fy(t\033)g Fq(8)p Fy(\033)q Fm(.)h(F)m(urthermor)n (e,)f(note)h(that)g Fq(\021)e(\032)f Fx(=)1595 597 y Fp(R)1626 591 y Fm(,)j(that)g(is,)411 641 y Fy(s)d Fq(\021)g Fy(t)f Fq(\))g Fy(s)h Fx(=)628 647 y Fp(R)671 641 y Fy(t)p Fm(.)356 691 y(3.)21 b(If)15 b Fy(t)c Fq(!)523 697 y Fl(l)p Fp(!)p Fl(r)o(;p;\033)652 691 y Fy(t)667 676 y Fp(0)693 691 y Fm(is)k(an)g(innermost)g(step,)f(then)i Fy(\033)g Fm(is)e(a)h Fx(normalized)f Fm(substitution.)340 798 y(Pr)n(o)n(of.)20 b Fx(Routine.)13 b Fh(2)340 926 y Fn(2.2)48 b(Seman)o(tic)14 b(Matc)o(hing)340 1013 y Fx(The)21 b(task)g(of)f(seman)o(tic)g Fm(uni\014c)n(ation)h Fx(consists)h(of)e(\014nding)g(a)g(complete)g(set)h Fy(\002)g Fx(of)f Fq(R)p Fx(-)340 1063 y(uni\014ers)d(for)f(a)g(goal)f Fy(s)h Fx(=)748 1069 y Fr(?)782 1063 y Fy(t)p Fx(,)g(that)g(is)g(to)g (sa)o(y)m(,)f(for)h(ev)o(ery)h Fy(\033)h Fx(with)e Fy(s\033)h Fx(=)1505 1069 y Fp(R)1551 1063 y Fy(t\033)h Fx(there)f(is)g(a)340 1113 y Fy(\025)h Fq(2)f Fy(\002)e Fx(with)f Fy(s\025)k Fx(=)662 1119 y Fp(R)710 1113 y Fy(t\025)c Fx(and)g Fy(\025)k Fq(\024)918 1119 y Fp(R)966 1113 y Fy(\033)q Fx(.)f(F)m(or)g(seman)o (tic)g Fm(matching)h Fx(w)o(e)f(ha)o(v)o(e)h(to)f(\014nd)h(a)340 1163 y(complete)d(set)g Fy(\002)h Fx(of)e Fq(R)p Fx(-matc)o(hers)h(for) f(a)h(goal)e Fy(s)h Fx(=)1158 1169 y Fr(?)1189 1163 y Fy(N)5 b Fx(,)14 b(where)i Fy(N)k Fx(is)14 b(a)h(term)f(in)g(ground)340 1212 y(normal)d(form,)g(i.e.)h(for)g(ev)o(ery)i Fy(\033)g Fx(with)e Fy(s\033)h Fx(=)1045 1218 y Fp(R)1088 1212 y Fy(N)18 b Fx(there)c(is)e(a)h Fy(\025)f Fq(2)f Fy(\002)k Fx(with)e Fy(s\025)f Fx(=)1621 1218 y Fp(R)1664 1212 y Fy(N)17 b Fx(and)340 1262 y Fy(\025)c Fq(\024)409 1268 y Fp(R)451 1262 y Fy(\033)q Fx(.)h(In)g(general,)g(seman)o(tic)f(matc)o (hing)g(is)h(as)g(hard)g(as)g(seman)o(tic)f(uni\014cation,)g(since)340 1312 y(ev)o(ery)18 b(goal)e Fy(s)i Fx(=)613 1318 y Fr(?)648 1312 y Fy(t)f Fx(can)g(b)q(e)h(transformed)f(in)o(to)f(the)i(goal)e Fy(eq)q Fx(\()p Fy(s;)7 b(t)p Fx(\))18 b(=)1482 1318 y Fr(?)1517 1312 y Fy(tr)q(ue)f Fx(using)g(the)340 1362 y(additional)12 b(rule)j Fy(eq)q Fx(\()p Fy(X)q(;)7 b(X)s Fx(\))12 b Fq(!)f Fy(tr)q(ue)p Fx(.)403 1412 y(In)17 b([DMS92)o(])f(it)h(w)o(as)g(p)q(oin)o(ted)g(out)g(that)g(canonical)f (TRSs)h(whic)o(h)g(are)h(in)e(addition)340 1462 y Fm(variable-pr)n (eserving)c Fx(or)h Fm(left-line)n(ar)f Fx(prev)o(en)o(t)i(suc)o(h)g(a) f(transformation.)d(These)15 b(classes)f(of)340 1512 y(TRSs)i(are)h(still)e(quite)h(large,)f(so)h(it)g(is)f(reasonable)i(to) f(think)f(ab)q(out)h(a)g(sp)q(ecial)g(calculus)340 1562 y(whic)o(h)d(tak)o(es)g(adv)n(an)o(tage)f(of)g(the)h(p)q(eculiarities)g (of)f(the)h(seman)o(tic)f(matc)o(hing)e(problem.)h(In)340 1612 y([DMS92)o(])j(the)g(follo)o(wing)d(forw)o(ard)j(decomp)q(osition) e(rules)j(are)f(presen)o(ted:)340 1698 y Fn(Eliminate:)46 b Fx(\()p Fy(x)12 b Fx(=)687 1704 y Fr(?)716 1698 y Fy(s;)7 b(L)782 1704 y Fr(1)801 1698 y Fy(;)g(:)g(:)g(:)e(;)i(L)922 1704 y Fl(n)944 1698 y Fy(;)g(\025)p Fx(\))k Fh(;)g Fx(\()p Fy(L)1111 1704 y Fr(1)1130 1698 y Fy(\033)o(;)c(:)g(:)g(:)e(;)i(L)1274 1704 y Fl(n)1296 1698 y Fy(\033)r(;)g(\025\033)q Fx(\),)13 b(where)i Fy(\033)e Fx(=)f Fq(f)p Fy(x)f Fq( )g Fy(s)p Fq(g)340 1748 y Fn(Decomp)q(ose:)i Fx(\()p Fy(f)t Fx(\()p Fy(s)678 1754 y Fr(1)698 1748 y Fy(;)7 b(:)g(:)g(:)e(;)i(s)810 1754 y Fl(m)842 1748 y Fx(\))k(=)901 1754 y Fr(?)931 1748 y Fy(f)t Fx(\()p Fy(s)990 1733 y Fp(0)990 1758 y Fr(1)1010 1748 y Fy(;)c(:)g(:)g(:)e(;)i(s)1122 1733 y Fp(0)1122 1758 y Fl(m)1153 1748 y Fx(\))p Fy(;)g(L)1216 1754 y Fr(1)1235 1748 y Fy(;)g(:)g(:)g(:)t(;)g(L)1355 1754 y Fl(n)1378 1748 y Fy(;)g(\033)q Fx(\))603 1798 y Fh(;)k Fx(\()p Fy(s)691 1804 y Fr(1)722 1798 y Fx(=)754 1804 y Fr(?)784 1798 y Fy(s)803 1782 y Fp(0)803 1808 y Fr(1)822 1798 y Fy(;)c(:)g(:)g(:)t(;)g(s)933 1804 y Fl(m)976 1798 y Fx(=)1008 1804 y Fr(?)1038 1798 y Fy(s)1057 1782 y Fp(0)1057 1808 y Fl(m)1089 1798 y Fy(;)g(L)1136 1804 y Fr(1)1154 1798 y Fy(;)g(:)g(:)g(:)e(;)i(L)1275 1804 y Fl(n)1297 1798 y Fy(;)g(\033)q Fx(\))340 1847 y Fn(Mutate:)95 b Fx(\()p Fy(f)t Fx(\()p Fy(s)678 1853 y Fr(1)698 1847 y Fy(;)7 b(:)g(:)g(:)e(;)i(s)810 1853 y Fl(m)842 1847 y Fx(\))k(=)901 1853 y Fr(?)931 1847 y Fy(t;)c(L)993 1853 y Fr(1)1011 1847 y Fy(;)g(:)g(:)g(:)e(;)i(L)1132 1853 y Fl(n)1154 1847 y Fy(;)g(\033)q Fx(\))603 1897 y Fh(;)k Fx(\()p Fy(s)691 1903 y Fr(1)722 1897 y Fx(=)754 1903 y Fr(?)784 1897 y Fy(l)796 1903 y Fr(1)815 1897 y Fy(;)c(:)g(:)g(:)t(;)g(s)926 1903 y Fl(m)969 1897 y Fx(=)1001 1903 y Fr(?)1031 1897 y Fy(l)1043 1903 y Fl(m)1075 1897 y Fy(;)g(r)12 b Fx(=)1157 1903 y Fr(?)1186 1897 y Fy(t;)7 b(\033)q Fx(\),)603 1947 y(where)15 b Fy(f)t Fx(\()p Fy(l)775 1953 y Fr(1)795 1947 y Fy(;)7 b(:)g(:)g(:)e(;)i(l)900 1953 y Fl(m)931 1947 y Fx(\))12 b(=)g Fy(r)j Fx(is)e(a)h(renamed)f (rule)i(in)e Fq(R)403 2032 y Fx(This)d(forw)o(ard)f(decomp)q(osition)g (calculus)i(is)f(a)g(complete)f(pro)q(cedure)j(for)e(solving)f(goals) 340 2082 y Fy(s)j Fx(=)403 2088 y Fr(?)433 2082 y Fy(N)5 b Fx(,)11 b(where)h Fy(N)k Fx(is)11 b(in)g(ground)g(normal)e(form,)g (and)i(the)h(underlying)f(TRS)g(is)g(canonical)340 2132 y(and)j(v)n(ariable-preserving)g(or)g(left-linear)f([DMS92)o(].)403 2183 y(The)h(ab)q(o)o(v)o(e)g(rules)g(are)g(a)g(subset)h(of)e(the)i (transformation)d(rules)i(whic)o(h)g(w)o(ere)h(used)g(in)340 2232 y([DS87)o(,)e(MMR89)o(,)f(Mit90,)g(Mit94)o(])h(for)f(seman)o(tic)g (uni\014cation.)g(Ho)o(w)o(ev)o(er,)h(this)g(approac)o(h)340 2282 y(do)q(es)h(not)e(explicitly)g(exploit)g(the)h(fact)f(that)h(the)g (righ)o(t-hand)f(side)h(of)f(an)g(initial)f(goal)g(has)340 2332 y(to)g(b)q(e)h(in)f(ground)g(normal)e(form.)g(In)i(the)g(next)h (section)g(w)o(e)f(will)f(presen)o(t)i(a)f(calculus)g(whic)o(h)340 2382 y(tak)o(es)h(more)e(adv)n(an)o(tage)h(of)f(this)i(since)g(it)f (starts)h(with)f(the)h(result)g(on)f(the)g(righ)o(t-hand)g(side)340 2432 y(and)j(tries)h(to)e(\014nd)h(out)g(ho)o(w)g(the)g(w)o(a)o(y)f (leads)h(bac)o(k)g(to)g(the)g(term)g(on)f(the)i(left-hand)e(side.)1050 2556 y(4)p eop %%Page: 5 5 5 4 bop 183 194 a Fs(3)56 b(Rev)n(erse)17 b(Restructuring)183 318 y Fn(3.1)47 b(De\014nition)12 b(of)k(Rev)o(erse)e(Restructurin)o(g) 183 427 y Fx(The)f(follo)o(wing)e(inference)j(rules)g(de\014ne)g(the)g (calculus)g(of)e(Rev)o(erse)j(Restructuring)f(\(R)1566 422 y(R)1596 427 y(\).)183 507 y Fn(De\014niti)o(on)f(3.1)i(:)g Fx(\(Rev)o(erse)g(Restructuring)g(rules\))188 588 y Fn(Eliminate1:)38 b Fx(\([)p Fy(x)11 b Fx(=)562 594 y Fr(?)591 588 y Fy(s;)c(L)657 594 y Fr(1)676 588 y Fy(;)g(:)g(:)g(:)e(;)i(L)797 594 y Fl(n)819 588 y Fx(])p Fy(;)g(\025)p Fx(\))p Fq(\000)-7 b(!)906 600 y( )g Fy(-)972 588 y Fx(\([)p Fy(L)1028 594 y Fr(1)1047 588 y Fy(\033)o(;)7 b(:)g(:)g(:)e(;)i(L)1191 594 y Fl(n)1213 588 y Fy(\033)q Fx(])p Fy(;)g(\025\033)q Fx(\))467 637 y(if)13 b Fy(s)f Fq(\021)g Fy(x)h Fx(or)h Fy(x)d Fq(62)g(V)s Fx(\()p Fy(s)p Fx(\),)k(where)g Fy(\033)e Fx(=)f Fq(f)p Fy(x)f Fq( )g Fy(s)p Fq(g)188 687 y Fn(Eliminate2:)38 b Fx(\([)p Fy(s)11 b Fx(=?)p Fy(x;)c(L)648 693 y Fr(1)666 687 y Fy(;)g(:)g(:)g(:)e(;)i(L)787 693 y Fl(n)809 687 y Fx(])p Fy(;)g(\025)p Fx(\))p Fq(\000)-7 b(!)896 700 y( )g Fy(-)963 687 y Fx(\([)p Fy(L)1019 693 y Fr(1)1037 687 y Fy(\033)o(;)7 b(:)g(:)g(:)e(;)i(L)1181 693 y Fl(n)1203 687 y Fy(\033)q Fx(])p Fy(;)g(\025\033)q Fx(\))467 737 y(if)13 b Fy(x)e Fq(62)g(V)s Fx(\()p Fy(s)p Fx(\))p Fy(;)c(s)13 b Fq(62)e Fy(X)s Fx(,)j(where)h Fy(\033)e Fx(=)f Fq(f)p Fy(x)f Fq( )g Fy(s)p Fq(g)188 787 y Fn(Decomp)q(ose:)29 b Fx(\([)p Fy(f)t Fx(\()p Fy(s)554 793 y Fr(1)573 787 y Fy(;)7 b(:)g(:)g(:)e(;)i(s)685 793 y Fl(m)717 787 y Fx(\))k(=)776 793 y Fr(?)806 787 y Fy(f)t Fx(\()p Fy(s)865 772 y Fp(0)865 797 y Fr(1)885 787 y Fy(;)c(:)g(:)g(:)e(;)i(s)997 772 y Fp(0)997 797 y Fl(m)1028 787 y Fx(\))p Fy(;)g(L)1091 793 y Fr(1)1110 787 y Fy(;)g(:)g(:)g(:)t(;)g(L)1230 793 y Fl(n)1253 787 y Fx(])p Fy(;)g(\033)q Fx(\))p Fq(\000)-8 b(!)1340 799 y( )h Fy(-)467 837 y Fx(\([)p Fy(s)514 843 y Fr(1)544 837 y Fx(=)576 843 y Fr(?)606 837 y Fy(s)625 822 y Fp(0)625 847 y Fr(1)644 837 y Fy(;)7 b(:)g(:)g(:)t(;)g(s)755 843 y Fl(m)798 837 y Fx(=)830 843 y Fr(?)860 837 y Fy(s)879 822 y Fp(0)879 847 y Fl(m)911 837 y Fy(;)g(L)958 843 y Fr(1)976 837 y Fy(;)g(:)g(:)g(:)e(;)i(L)1097 843 y Fl(n)1119 837 y Fx(])p Fy(;)g(\033)q Fx(\))p Fy(;)13 b(m)f Fq(\025)g Fx(0)188 886 y Fn(Mutate1:)87 b Fx(\([)p Fy(s)11 b Fx(=)557 892 y Fr(?)587 886 y Fy(f)t Fx(\()p Fy(s)646 892 y Fr(1)666 886 y Fy(;)c(:)g(:)g(:)e(;)i(s)778 892 y Fl(m)809 886 y Fx(\))p Fy(;)g(L)872 892 y Fr(1)891 886 y Fy(;)g(:)g(:)g(:)t(;)g(L)1011 892 y Fl(n)1034 886 y Fx(])p Fy(;)g(\033)q Fx(\))p Fq(\000)-8 b(!)1121 899 y( )h Fy(-)467 936 y Fx(\([)p Fy(r)514 942 y Fr(1)543 936 y Fx(=)575 942 y Fr(?)605 936 y Fy(s)624 942 y Fr(1)643 936 y Fy(;)7 b(:)g(:)g(:)e(;)i(r)755 942 y Fl(m)797 936 y Fx(=)829 942 y Fr(?)858 936 y Fy(s)877 942 y Fl(m)909 936 y Fy(;)g(s)12 b Fx(=)991 942 y Fr(?)1020 936 y Fy(g)q Fx(\()p Fy(l)1069 942 y Fr(1)1089 936 y Fy(;)7 b(:)g(:)g(:)e(;)i(l)1194 942 y Fl(q)1212 936 y Fx(\))p Fy(;)g(L)1275 942 y Fr(1)1293 936 y Fy(;)g(:)g(:)g(:)e(;)i(L)1414 942 y Fl(n)1436 936 y Fx(])p Fy(;)g(\033)q Fx(\))p Fy(;)467 986 y Fx(where)15 b Fy(g)q Fx(\()p Fy(l)636 992 y Fr(1)655 986 y Fy(;)7 b(:)g(:)g(:)e(;)i(l)760 992 y Fl(q)778 986 y Fx(\))12 b Fq(!)f Fy(f)t Fx(\()p Fy(r)918 992 y Fr(1)937 986 y Fy(;)c(:)g(:)g(:)e(;)i(r)1049 992 y Fl(m)1080 986 y Fx(\))14 b(is)f(a)h(renamed)f(rule)i(from)d Fq(R)467 1036 y Fx(and)h(Eliminate1) f(do)q(es)i(not)g(apply)188 1086 y Fn(Mutate2:)87 b Fx(\([)p Fy(s)11 b Fx(=)557 1092 y Fr(?)587 1086 y Fy(s)606 1071 y Fp(0)618 1086 y Fy(;)c(L)665 1092 y Fr(1)683 1086 y Fy(;)g(:)g(:)g(:)e(;)i(L)804 1092 y Fl(n)826 1086 y Fx(])p Fy(;)g(\033)q Fx(\))p Fq(\000)-7 b(!)914 1098 y( )g Fy(-)467 1136 y Fx(\([)p Fy(s)11 b Fx(=)557 1142 y Fr(?)587 1136 y Fy(g)q Fx(\()p Fy(l)636 1142 y Fr(1)655 1136 y Fy(;)c(:)g(:)g(:)e(;)i (l)760 1142 y Fl(q)778 1136 y Fx(\))p Fy(\033)819 1120 y Fp(0)831 1136 y Fy(;)g(L)878 1142 y Fr(1)897 1136 y Fy(;)g(:)g(:)g(:)t(;)g(L)1017 1142 y Fl(n)1040 1136 y Fx(])p Fy(;)g(\033)q(\033)1121 1120 y Fp(0)1132 1136 y Fx(\),where)14 b Fy(\033)1304 1120 y Fp(0)1328 1136 y Fx(=)e Fq(f)p Fy(x)f Fq( )g Fy(s)1500 1120 y Fp(0)1512 1136 y Fq(g)p Fx(,)467 1185 y Fy(g)q Fx(\()p Fy(l)516 1191 y Fr(1)535 1185 y Fy(;)c(:)g(:)g(:)e(;)i(l)640 1191 y Fl(q)658 1185 y Fx(\))12 b Fq(!)f Fy(x)i Fx(is)h(a)g(renamed)f(rule)h (from)e Fq(R)i Fx(and)g(neither)467 1235 y(Eliminate1)d(nor)j (Eliminate2)d(do)q(es)k(apply)m(.)245 1338 y(Note)i(that)g(w)o(e)g (assume)g(that)g(the)g(v)n(ariables)f(in)h(the)g(rewrite)h(rules)g(are) f(alw)o(a)o(ys)f(re-)183 1388 y(named)f(suc)o(h)i(that)f(the)g(rules)h (con)o(tain)f(only)f(fresh)i(v)n(ariables.)e(Similar)e(to)j(the)h(forw) o(ard)183 1438 y(decomp)q(osition)11 b(calculus,)h(the)i(Martelli)d(&)i (Mon)o(tanari)f(rules)i({)e(Decomp)q(ose)g(and)h(Elim-)183 1487 y(inate1/2)355 1472 y Fr(2)395 1487 y Fx({)20 b(for)g(syn)o (tactic)h(matc)o(hing)e(and)i(uni\014cation)f([MM82)o(])g(are)h(part)g (of)f(our)183 1537 y(calculus.)e(The)i(Mutate)f(rules)h(mak)o(e)d(the)j (di\013erence:)g(Using)f(the)h(Mutate1)f(rule,)g(the)183 1587 y(righ)o(t-hand)14 b(side)i(of)e(a)h(rule)h(is)f(compared)f(to)h (the)h(righ)o(t-hand)e(side)i(of)e(the)i(goal.)e(Under)183 1637 y(the)i(presumption)f(that)h(the)h(goals)e(generated)i(b)o(y)f (this)g(comparison)e(are)i(solv)n(able,)f(an-)183 1687 y(other)f(goal)f(consisting)h(of)g(the)h(left-hand)e(side)i(of)e(the)i (original)d(goal)h(and)h(the)h(left-hand)183 1736 y(side)g(of)g(the)h (rule)g(under)g(consideration)g(is)f(added.)h(By)f(means)g(of)g(this)g (transformation)183 1786 y(a)k(rev)o(erse)i(computation,)d(starting)h (with)g(the)i(righ)o(t-hand)d(side,)i(is)f(established.)h(The)183 1836 y(Mutate2)c(rule)h(is)f(necessary)j(for)d(handling)f(collapsing)g (rules.)i(It)f(includes)h(an)f(implicit)183 1886 y(Eliminate2)e(step.)j (If)f(in)g(a)g(Decomp)q(ose)g(step)i(w)o(e)f(ha)o(v)o(e)f Fy(m)g Fx(=)g(0,)g(the)h(goal)f(is)g(remo)o(v)o(ed.)183 1936 y(In)d(this)g(case)h(w)o(e)g(sp)q(eak)g(of)e(a)h Fy(tr)q(iv)q(ial)j Fx(Decomp)q(ose)d(step.)g(The)h(reader)h(ma)o(y)c (also)h(observ)o(e)183 1985 y(that)h(w)o(e)h(deal)f(with)g(a)g Fm(list)f Fx(and)h(not)h(with)f(a)g(set)h(of)f(goals.)f(This)h(is)g(b)q (ecause)i(the)f(order)g(of)183 2035 y(ev)n(aluating)f(the)i(equations)g (is)f(strictly)h(sequen)o(tial)g(from)d(left)j(to)f(righ)o(t.)g(There)i (is)e(still)g(a)183 2085 y(high)h(degree)j(of)d(nondeterminism,)f(due)i (to)g(the)h(fact)f(that)g(in)g(general)g(more)f(than)h(one)183 2135 y(rule)d(can)f(b)q(e)i(used)f(for)g(a)f(Mutate1/2)h(step)g(and)g (that)f(a)h(Decomp)q(ose)f(and)h(a)f(Mutate)h(rule)183 2185 y(migh)o(t)h(b)q(e)j(applicable)e(at)i(the)g(same)e(time.)g(Ho)o (w)o(ev)o(er,)h(if)g(an)g(Eliminate1)e(or)i(an)g(Elimi-)183 2235 y(nate2)e(step)i(can)f(b)q(e)g(applied,)e(no)i(other)g (transformation)e(rule)h(is)h(applicable,)e(i.e.)h Fm(e)n(ager)183 2284 y(variable)h(elimination)g Fx(is)g(built)f(in)o(to)h(our)g (calculus.)g(In)g(order)h(to)e(complete)h(the)h(picture)183 2334 y(w)o(e)e(de\014ne)h(the)f(notions)g Fm(c)n(omputation)j Fx(and)d Fm(r)n(esult)t Fx(:)p 183 2389 237 2 v 191 2416 a Fg(2)221 2432 y Fw(In)f([DMS92)q(])f(a)h(kind)i(of)e(Eliminate2)i (rule)f(is)g(implicitly)i(assumed)e(in)g(the)f(left-linear)i(case.)893 2556 y Fx(5)p eop %%Page: 6 6 6 5 bop 340 194 a Fn(De\014nition)17 b(3.2)j(:)e Fx(\(computation,)d (result\))k(A)f Fm(c)n(omputation)j Fx(of)c(a)h(goal)e Fy(s)i Fx(=)1630 200 y Fr(?)1666 194 y Fy(s)1685 179 y Fp(0)1715 194 y Fx(is)g(a)340 244 y(sequence)f(of)d(R)588 239 y(R)633 244 y(steps)i(starting)f(with:)f(\([)p Fy(s)f Fx(=)1093 250 y Fr(?)1123 244 y Fy(s)1142 228 y Fp(0)1155 244 y Fx(])p Fy(;)7 b Fq(;)p Fx(\))p Fq(\000)-8 b(!)1238 256 y( )h Fy(-)1304 244 y Fx(\()p Fy(G)1353 250 y Fr(1)1372 244 y Fy(;)7 b(\033)1415 250 y Fr(1)1433 244 y Fx(\))p Fq(\000)-7 b(!)1465 256 y( )g Fy(-)1539 244 y Fq(\001)7 b(\001)g(\001)13 b Fx(A)i(compu-)340 293 y(tation)f(\([)p Fy(s)d Fx(=)553 299 y Fr(?)583 293 y Fy(s)602 278 y Fp(0)614 293 y Fx(])p Fy(;)c Fq(;)p Fx(\))p Fq(\000)-8 b(!)697 306 y( )h Fy(-)764 278 y Fp(\003)783 293 y Fx(\([)12 b(])p Fy(;)7 b(\033)q Fx(\))13 b(is)h(called)g Fy(successf)t(ul)j Fx(and)c Fy(\033)i Fx(is)f(its)g Fm(r)n(esult)t Fx(.)403 368 y(The)e(next)h(example)e(illustrates)i(ho)o(w)f(R)1042 363 y(R)1084 368 y(w)o(orks)h(in)f(detail.)f(W)m(e)h(de\014ne)h(the)g (addition)340 418 y(on)h(natural)f(n)o(um)o(b)q(ers)h(whic)o(h)g(are)g (constructed)i(b)o(y)e(0)f(and)h Fy(s)p Fx(.)p 361 658 5 178 v 365 484 1387 5 v 755 531 a Fy(R)787 537 y Fr(1)817 531 y Fx(:)37 b(0)9 b(+)h Fy(X)79 b Fq(!)11 b Fy(X)755 581 y(R)787 587 y Fr(2)817 581 y Fx(:)37 b Fy(s)p Fx(\()p Fy(X)s Fx(\))11 b(+)e Fy(Y)21 b Fq(!)11 b Fy(s)p Fx(\()p Fy(X)j Fx(+)9 b Fy(Y)h Fx(\))p 365 658 467 5 v 832 616 454 2 v 832 678 2 62 v 846 658 a(Example)j(3.3)g(:)g(Addition)p 1284 678 V 832 680 454 2 v 1285 658 467 5 v 1752 658 5 178 v 403 750 a(The)k(goal)e(to)h(solv)o(e)g(is)h Fy(s)p Fx(\(0\))11 b(+)g Fy(U)21 b Fx(=)990 756 y Fr(?)1024 750 y Fy(s)p Fx(\()p Fy(s)p Fx(\(0\)\).)c(Remem)o(b)q(er)e(that)h(the)h (computation)340 800 y(order)f(is)e(not)g(arbitrary:)g(the)h(leftmost)e (goal)g(has)i(to)f(b)q(e)h(solv)o(ed)g(\014rst)g(and)f(the)h(resulting) 340 850 y(substitution)f(has)g(to)g(b)q(e)h(applied)e(to)h(the)g(rest)h (of)f(the)g(goals.)677 913 y(\([)p Fy(s)p Fx(\(0\))9 b(+)h Fy(U)16 b Fx(=)904 919 y Fr(?)934 913 y Fy(s)p Fx(\()p Fy(s)p Fx(\(0\)\)])p Fy(;)7 b Fq(;)p Fx(\))450 952 y Fl(M)s(utate)p Fr(1)582 956 y Ff(R)603 962 y Fe(2)493 983 y Fq(\000)-6 b(!)509 995 y( )f Fy(-)677 983 y Fx(\([)p Fy(X)13 b Fx(+)c Fy(Y)21 b Fx(=)870 989 y Fr(?)899 983 y Fy(s)p Fx(\(0\))p Fy(;)7 b(s)p Fx(\(0\))j(+)g Fy(U)16 b Fx(=)1190 989 y Fr(?)1220 983 y Fy(s)p Fx(\()p Fy(X)s Fx(\))10 b(+)g Fy(Y)f Fx(])p Fy(;)e Fq(;)p Fx(\))450 1022 y Fl(M)s(utate)p Fr(2)582 1026 y Ff(R)603 1032 y Fe(1)493 1052 y Fq(\000)-6 b(!)509 1064 y( )f Fy(-)677 1052 y Fx(\([)p Fy(X)13 b Fx(+)c Fy(Y)21 b Fx(=)870 1058 y Fr(?)899 1052 y Fx(0)9 b(+)h Fy(s)p Fx(\(0\))p Fy(;)19 b(s)p Fx(\(0\))10 b(+)g Fy(U)16 b Fx(=)1274 1058 y Fr(?)1304 1052 y Fy(s)p Fx(\()p Fy(X)s Fx(\))10 b(+)g Fy(Y)f Fx(])p Fy(;)e Fq(f)p Fy(X)1566 1037 y Fp(0)1589 1052 y Fq( )k Fy(s)p Fx(\(0\))p Fq(g)p Fx(\))450 1091 y Fl(D)q(ecompose)493 1116 y Fq(\000)-6 b(!)509 1129 y( )f Fy(-)677 1116 y Fx(\([)p Fy(X)15 b Fx(=)786 1122 y Fr(?)815 1116 y Fx(0)p Fy(;)k(Y)i Fx(=)944 1122 y Fr(?)973 1116 y Fy(s)p Fx(\(0\))p Fy(;)f(s)p Fx(\(0\))10 b(+)f Fy(U)17 b Fx(=)1277 1122 y Fr(?)1306 1116 y Fy(s)p Fx(\()p Fy(X)s Fx(\))11 b(+)e Fy(Y)h Fx(])p Fy(;)d Fq(f)p Fy(X)1569 1101 y Fp(0)1591 1116 y Fq( )k Fy(s)p Fx(\(0\))p Fq(g)p Fx(\))429 1156 y Fr(2)p Fp(\002)p Fl(E)r(liminate)p Fr(1)495 1179 y Fq(\000)-6 b(!)512 1192 y( )f Fy(-)677 1179 y Fx(\([)p Fy(s)p Fx(\(0\))9 b(+)h Fy(U)16 b Fx(=)904 1185 y Fr(?)934 1179 y Fy(s)p Fx(\(0\))10 b(+)f Fy(s)p Fx(\(0\)])p Fy(;)e Fq(f)p Fy(X)1218 1164 y Fp(0)1241 1179 y Fq( )k Fy(s)p Fx(\(0\))p Fy(;)c(X)15 b Fq( )c Fx(0)p Fy(;)c(Y)20 b Fq( )11 b Fy(s)p Fx(\(0\))p Fq(g)p Fx(\))450 1218 y Fl(D)q(ecompose)493 1243 y Fq(\000)-6 b(!)509 1256 y( )f Fy(-)677 1243 y Fx(\([)p Fy(s)p Fx(\(0\))12 b(=)821 1249 y Fr(?)850 1243 y Fy(s)p Fx(\(0\))p Fy(;)20 b(U)c Fx(=)1030 1249 y Fr(?)1060 1243 y Fy(s)p Fx(\(0\)])p Fy(;)7 b Fq(f)p Fy(X)1221 1228 y Fp(0)1244 1243 y Fq( )k Fy(s)p Fx(\(0\))p Fy(;)c(X)15 b Fq( )c Fx(0)p Fy(;)c(Y)20 b Fq( )11 b Fy(s)p Fx(\(0\))p Fq(g)p Fx(\))429 1282 y Fr(2)p Fp(\002)p Fl(D)q(ecompose)494 1308 y Fq(\000)-7 b(!)510 1320 y( )g Fy(-)677 1308 y Fx(\([)p Fy(U)16 b Fx(=)781 1314 y Fr(?)811 1308 y Fy(s)p Fx(\(0\)])p Fy(;)7 b Fq(f)p Fy(X)972 1293 y Fp(0)995 1308 y Fq( )k Fy(s)p Fx(\(0\))p Fy(;)c(X)15 b Fq( )c Fx(0)p Fy(;)c(Y)20 b Fq( )11 b Fy(s)p Fx(\(0\))p Fq(g)p Fx(\))450 1347 y Fl(E)r(liminate)p Fr(1)495 1371 y Fq(\000)-7 b(!)511 1383 y( )g Fy(-)677 1371 y Fx(\([)12 b(])p Fy(;)7 b Fq(f)p Fy(X)806 1356 y Fp(0)829 1371 y Fq( )k Fy(s)p Fx(\(0\))p Fy(;)c(X)15 b Fq( )c Fx(0)p Fy(;)c(Y)20 b Fq( )11 b Fy(s)p Fx(\(0\))p Fy(;)c(U)16 b Fq( )11 b Fy(s)p Fx(\(0\))p Fq(g)p Fx(\))403 1443 y(A)o(t)16 b(\014rst)h(glance,)f(it)f (seems)i(that)f(in)g(comparison)f(to)h(other)g(narro)o(wing)g(deriv)n (ations)340 1493 y(the)21 b(length)f(of)g(a)g(R)673 1488 y(R)723 1493 y(computation)e(is)i(m)o(uc)o(h)f(longer;)g(e.g.)h(the)h (goal)d(ab)q(o)o(v)o(e)i(can)h(b)q(e)340 1543 y(computed)16 b(with)g(t)o(w)o(o)g(innermost)g(narro)o(wing)g(steps.)h(But)g(a)f (single)g(narro)o(wing)g(step)h(is)340 1593 y(more)12 b(complicated)g(than)g(a)h(R)829 1588 y(R)871 1593 y(step.)h(This)e(is) h(b)q(ecause)h(a)f(subterm)f(of)g(a)h(goal)e(has)i(to)g(b)q(e)340 1643 y(uni\014ed)i(with)g(a)f(left-hand)g(side)h(of)f(a)h(rule)g(b)q (efore)g(the)h(rewrite)f(step)h(can)f(b)q(e)g(b)q(e)h(carried)340 1692 y(out.)11 b(In)g(R)499 1687 y(R)529 1692 y(,)f(uni\014cation)h(is) g(p)q(erformed)f(explicitly)g(b)o(y)h(a)g(sequence)i(of)d(Eliminate1/2) e(and)340 1742 y(Decomp)q(ose)16 b(steps.)h(Therefore)h(w)o(e)e(will)e (only)i(coun)o(t)g(the)h(Mutate1/2)f(steps)h(when)g(the)340 1792 y(length)d(of)g(a)f(R)576 1787 y(R)620 1792 y(computation)f(is)i (compared)f(to)h(the)g(one)g(of)g(a)f(narro)o(wing)g(deriv)n(ation.)340 1936 y Fn(3.2)48 b(Soundness)340 2039 y Fx(In)14 b(this)g(section)h(w)o (e)f(sho)o(w)g(that)g(ev)o(ery)g(result)h(computed)e(b)o(y)h(R)1367 2034 y(R)1411 2039 y(is)g(an)f Fq(R)p Fx(-uni\014er.)340 2117 y Fn(Theorem)j(3.4:)e Fx(\(soundness)i(of)e(R)918 2112 y(R)948 2117 y(\))30 b Fm(L)n(et)15 b Fq(R)g Fm(b)n(e)g(a)h(c)n (anonic)n(al)g(TRS.)f(If)g(ther)n(e)g(exists)g(a)340 2167 y(suc)n(c)n(essful)g(c)n(omputation)h(of)e(the)h(go)n(al)g Fy(s)d Fx(=)1029 2173 y Fr(?)1059 2167 y Fy(s)1078 2152 y Fp(0)1105 2167 y Fm(with)i(r)n(esult)g Fy(\033)q Fm(,)h(then)g Fy(s\033)e Fx(=)1541 2173 y Fp(R)1584 2167 y Fy(s)1603 2152 y Fp(0)1615 2167 y Fy(\033)q Fm(.)340 2278 y(Pr)n(o)n(of.)20 b Fx(The)15 b(pro)q(of)e(is)h(b)o(y)g(induction)f(on)h Fy(m)p Fx(,)g(the)g(length)g(of)f(the)i(R)1412 2273 y(R)1456 2278 y(computation:)403 2332 y Fy(m)d Fx(=)h(1)e(:)j(Only)g(an)g (Eliminate1/2)d(or)k(a)e(trivial)g(Decomp)q(ose)h(step)h(is)f(p)q (ossible,)g(since)340 2382 y(only)g(suc)o(h)i(a)f(step)g(reduces)i(the) f(n)o(um)o(b)q(er)e(of)g(goals.)g(Suc)o(h)h(a)g(transformation)d (computes)340 2432 y(a)i(correct)i(solution.)1050 2556 y(6)p eop %%Page: 7 7 7 6 bop 245 194 a Fy(m)15 b Fx(=)g Fy(k)d Fx(+)f(1)p Fy(;)c(k)15 b Fq(\025)g Fx(1)g(:)g(W)m(e)h(split)f(the)i(computation)d (in)o(to)h(a)h(\014rst)g(and)g Fy(k)h Fx(subsequen)o(t)183 244 y(steps:)d(no)o(w)f(the)g(\014rst)h(step)g(cannot)g(b)q(e)g(an)f (Eliminate1/2)d(or)j(a)g(trivial)f(Decomp)q(ose)h(step)183 293 y(since)h(this)g(w)o(ould)f(con)o(tradict)i Fy(m)d(>)f Fx(1.)j(W)m(e)f(consider)i(the)f(remaining)e(p)q(ossibilities.)245 347 y(Decomp)q(ose:)j(W)m(e)g(ha)o(v)o(e)g(\([)p Fy(s)g Fx(=)740 353 y Fr(?)772 347 y Fy(s)791 332 y Fp(0)803 347 y Fx(])p Fy(;)7 b Fq(;)p Fx(\))p Fq(\000)-7 b(!)887 359 y( )g Fy(-)953 347 y Fx(\([)p Fy(s)1000 353 y Fr(1)1034 347 y Fx(=)1066 353 y Fr(?)1098 347 y Fy(s)1117 332 y Fp(0)1117 357 y Fr(1)1136 347 y Fy(;)7 b(:)g(:)g(:)e(;)i(s)1248 353 y Fl(n)1285 347 y Fx(=)1317 353 y Fr(?)1349 347 y Fy(s)1368 332 y Fp(0)1368 357 y Fl(n)1391 347 y Fx(])p Fy(;)g Fq(;)p Fx(\).)14 b(Eac)o(h)i(of)183 396 y(these)f(goals)e(can)g (b)q(e)i(solv)o(ed)e(in)g(at)h(most)f(k)g(steps.)i(Therefore)g(w)o(e)e (can)h(apply)f(the)i(induc-)183 446 y(tion)e(h)o(yp)q(othesis)i(from)d (left)h(to)h(righ)o(t)f(to)h(ev)o(ery)h(goal.)183 496 y(This)f(yields)g Fq(8)418 502 y Fr(1)p Fp(\024)p Fl(i)p Fp(\024)p Fl(n)534 496 y Fx(:)e Fy(s)577 502 y Fl(i)591 496 y Fy(\033)616 481 y Fr(1)642 496 y Fq(\001)7 b(\001)g(\001)e Fy(\033)722 481 y Fl(i)749 496 y Fx(=)781 502 y Fp(R)824 496 y Fy(s)843 481 y Fp(0)843 507 y Fl(i)857 496 y Fy(\033)882 481 y Fr(1)908 496 y Fq(\001)i(\001)g(\001)f Fy(\033)989 481 y Fl(i)1003 496 y Fx(.)14 b(Consequen)o(tly)m(,)g(it)g(follo)o(ws)f Fq(8)1497 502 y Fr(1)p Fp(\024)p Fl(i)p Fp(\024)p Fl(n)1612 496 y Fx(:)183 546 y Fy(s)202 552 y Fl(i)216 546 y Fy(\033)241 531 y Fr(1)267 546 y Fq(\001)7 b(\001)g(\001)e Fy(\033)347 531 y Fl(n)395 546 y Fx(=)427 552 y Fp(R)484 546 y Fy(s)503 531 y Fp(0)503 557 y Fl(i)517 546 y Fy(\033)542 531 y Fr(1)568 546 y Fq(\001)i(\001)g(\001)e Fy(\033)648 531 y Fl(n)671 546 y Fx(,)22 b(since)h(joinabilit)o(y)c(is)k(preserv)o(ed)h (under)f(substitutions)183 596 y(\(Lemma)11 b(2.1\).)i Fy(\033)f Fx(:=)g Fy(\033)559 581 y Fr(1)584 596 y Fq(\001)7 b(\001)g(\001)f Fy(\033)665 581 y Fl(n)701 596 y Fx(is)14 b(the)h(computed)e(result)i(and)e(clearly)h Fy(s\033)f Fx(=)1423 602 y Fp(R)1466 596 y Fy(s)1485 581 y Fp(0)1497 596 y Fy(\033)q Fx(.)245 649 y(Mutate1:)g(This)h(means)e Fy(s)663 634 y Fp(0)687 649 y Fq(\021)g Fy(f)t Fx(\()p Fy(s)790 634 y Fp(0)790 659 y Fr(1)810 649 y Fy(;)7 b(:)g(:)g(:)t(;)g (s)921 634 y Fp(0)921 659 y Fl(n)944 649 y Fx(\))14 b(and)f(there)i(is) e(a)g(rule)h Fy(l)f Fq(!)e Fy(f)t Fx(\()p Fy(r)1455 655 y Fr(1)1474 649 y Fy(;)c(:)g(:)g(:)e(;)i(r)1586 655 y Fl(n)1607 649 y Fx(\))183 699 y(in)14 b Fq(R)p Fx(,)h(suc)o(h)g(that)g (\([)p Fy(s)e Fx(=)571 705 y Fr(?)602 699 y Fy(s)621 684 y Fp(0)634 699 y Fx(])p Fy(;)7 b Fq(;)p Fx(\))p Fq(\000)-8 b(!)717 711 y( )h Fy(-)783 699 y Fx(\([)p Fy(r)830 705 y Fr(1)862 699 y Fx(=)894 705 y Fr(?)925 699 y Fy(s)944 684 y Fp(0)944 709 y Fr(1)963 699 y Fy(;)7 b(:)g(:)g(:)e(;)i(r)1075 705 y Fl(n)1110 699 y Fx(=)1142 705 y Fr(?)1173 699 y Fy(s)1192 684 y Fp(0)1192 709 y Fl(n)1215 699 y Fy(;)g(s)13 b Fx(=)1298 705 y Fr(?)1329 699 y Fy(l)q Fx(])p Fy(;)7 b Fq(;)p Fx(\).)13 b(Analogous)183 749 y(to)g(the)i(Decomp)q(ose)e (case)i(w)o(e)f(get)h(for)e(the)i(\014rst)f Fy(n)g Fx(goals:)183 811 y(\([)p Fy(r)230 817 y Fr(1)259 811 y Fx(=)291 817 y Fr(?)321 811 y Fy(s)340 796 y Fp(0)340 821 y Fr(1)359 811 y Fy(;)7 b(:)g(:)g(:)e(;)i(r)471 817 y Fl(n)504 811 y Fx(=)536 817 y Fr(?)565 811 y Fy(s)584 796 y Fp(0)584 821 y Fl(n)608 811 y Fx(])p Fy(;)g Fq(;)p Fx(\))690 785 y Fl(q)705 789 y Fe(1)721 785 y Fp(\024)p Fl(k)686 811 y Fq(\000)-7 b(!)702 823 y( )g Fy(-)780 811 y Fx(\([)13 b(])p Fy(;)7 b(\033)877 796 y Fr(1)894 811 y Fx(\))14 b(and)g(th)o(us)g Fy(f)t Fx(\()p Fy(r)1155 817 y Fr(1)1175 811 y Fy(;)7 b(:)g(:)g(:)e(;)i(r)1287 817 y Fl(n)1308 811 y Fx(\))p Fy(\033)1349 796 y Fr(1)1380 811 y Fx(=)1412 817 y Fp(R)1454 811 y Fy(s)1473 796 y Fp(0)1485 811 y Fy(\033)1510 796 y Fr(1)1529 811 y Fx(.)245 880 y(F)m(or)20 b(the)h(remaining)d(goal)h(w)o(e)h(get)h(\([)p Fy(s\033)913 865 y Fr(1)954 880 y Fx(=)986 886 y Fr(?)1026 880 y Fy(l)q(\033)1064 865 y Fr(1)1083 880 y Fx(])p Fy(;)7 b Fq(;)p Fx(\))1175 855 y Fl(q)1190 859 y Fe(2)1207 855 y Fp(\024)p Fl(k)1172 880 y Fq(\000)-7 b(!)1188 893 y( )g Fy(-)1277 880 y Fx(\([)12 b(])p Fy(;)7 b(\033)1373 865 y Fr(2)1391 880 y Fx(\).)20 b(Again)f(the)183 930 y(induction)c(h)o(yp)q(othesis)h(is)f(applicable) f(whic)o(h)h(yields)g Fy(s\033)1097 915 y Fr(1)1117 930 y Fy(\033)1142 915 y Fr(2)1174 930 y Fx(=)1206 936 y Fp(R)1251 930 y Fy(l)q(\033)1289 915 y Fr(1)1308 930 y Fy(\033)1333 915 y Fr(2)1352 930 y Fx(.)g(F)m(rom)e(Lemma)183 980 y(2.1)k(it)g(follo)o(ws)f(that)i Fy(f)t Fx(\()p Fy(r)592 986 y Fr(1)612 980 y Fy(;)7 b(:)g(:)g(:)t(;)g(r)723 986 y Fl(n)745 980 y Fx(\))p Fy(\033)786 965 y Fr(1)805 980 y Fy(\033)830 965 y Fr(2)867 980 y Fx(=)899 986 y Fp(R)948 980 y Fy(s)967 965 y Fp(0)979 980 y Fy(\033)1004 965 y Fr(1)1023 980 y Fy(\033)1048 965 y Fr(2)1067 980 y Fx(,)17 b Fy(l)q(\033)1134 965 y Fr(1)1153 980 y Fy(\033)1178 965 y Fr(2)1215 980 y Fx(=)1247 986 y Fp(R)1296 980 y Fy(f)t Fx(\()p Fy(r)1355 986 y Fr(1)1375 980 y Fy(;)7 b(:)g(:)g(:)t(;)g(r)1486 986 y Fl(n)1508 980 y Fx(\))p Fy(\033)1549 965 y Fr(1)1568 980 y Fy(\033)1593 965 y Fr(2)1612 980 y Fx(.)183 1030 y(The)k(latter)h(is)f(true,)h(b)q(ecause) h(for)e(ev)o(ery)h(rule)f Fy(l)i Fq(!)e Fy(r)i Fq(2)e(R)g Fx(it)g(trivially)f(holds)h(that)g Fy(l)i Fx(=)1550 1036 y Fp(R)1592 1030 y Fy(r)q Fx(.)183 1080 y(W)m(e)j(get)g Fy(s\033)372 1065 y Fr(1)392 1080 y Fy(\033)417 1065 y Fr(2)451 1080 y Fx(=)483 1086 y Fp(R)529 1080 y Fy(l)q(\033)567 1065 y Fr(1)586 1080 y Fy(\033)611 1065 y Fr(2)646 1080 y Fx(=)678 1086 y Fp(R)724 1080 y Fy(f)t Fx(\()p Fy(r)783 1086 y Fr(1)803 1080 y Fy(;)7 b(:)g(:)g(:)t(;)g(r)914 1086 y Fl(n)936 1080 y Fx(\))p Fy(\033)977 1065 y Fr(1)996 1080 y Fy(\033)1021 1065 y Fr(2)1056 1080 y Fx(=)1088 1086 y Fp(R)1134 1080 y Fy(s)1153 1065 y Fp(0)1165 1080 y Fy(\033)1190 1065 y Fr(1)1209 1080 y Fy(\033)1234 1065 y Fr(2)1253 1080 y Fx(.)16 b(Since)h Fy(\033)f Fx(:=)g Fy(\033)1517 1065 y Fr(1)1536 1080 y Fy(\033)1561 1065 y Fr(2)1596 1080 y Fx(is)183 1142 y(the)h(result)g(of)e(the)i (computation)e(\([)p Fy(s)g Fx(=)837 1148 y Fr(?)871 1142 y Fy(s)890 1127 y Fp(0)902 1142 y Fx(])p Fy(;)7 b Fq(;)p Fx(\))996 1119 y Fl(k)q Fr(+1)984 1142 y Fq(\000)-6 b(!)1001 1155 y( )f Fy(-)1083 1142 y Fx(\([)12 b(])p Fy(;)7 b(\033)1179 1127 y Fr(1)1197 1142 y Fy(\033)1222 1127 y Fr(2)1241 1142 y Fx(\))16 b(this)g(case)i(is)e(pro)o(v)o(ed.)183 1192 y(The)e(remaining)e(Mutate2)i(case)h(is)f(similar.)d Fh(2)245 1297 y Fx(Note)19 b(that)f(soundness)i(do)q(es)f(neither)g (dep)q(end)g(on)f(left-linearit)o(y)m(,)e(v)n(ariable-preser-)183 1347 y(vingness,)e(nor)f(the)i(form)d(of)h(the)i(goal.)183 1489 y Fn(3.3)47 b(Completeness)183 1589 y Fx(Although)16 b(the)h(completeness)g(pro)q(of)f(for)g(left-linear)f(TRSs)i(is)f(more) f(c)o(hallenging,)g(due)183 1639 y(to)f(space)i(limitatio)o(ns)c(w)o(e) j(presen)o(t)h(here)g(only)e(the)h(v)n(ariable-preserving)g(case)g(in)g (detail.)183 1688 y(The)g(structure)i(of)d(b)q(oth)g(pro)q(ofs)h(is)g (similar,)c(whic)o(h)k(mak)o(es)e(it)i(tolerable)f(to)h(restrict)h(the) 183 1738 y(pro)q(of)g(for)g(left-linear)g(TRSs)h(to)g(a)f(short)h(sk)o (etc)o(h)h(of)e(their)h(di\013erences.)i(F)m(or)d(a)h(detailed)183 1788 y(pro)q(of)c(see)i([BT94].)183 1883 y Fn(V)l(ariable-Preser)o(vin) o(g)e(TRSs)183 1978 y Fx(In)18 b(this)g(part,)g(w)o(e)g(tacitly)g (assume)g(that)g Fq(R)g Fx(is)g(a)g(canonical)g(and)g(v)n (ariable-preserving)183 2027 y(TRS.)e(In)i(Theorem)f(3.6,)f(w)o(e)h (will)f(sho)o(w)i(that)f(R)985 2022 y(R)1032 2027 y(is)h(complete)e (w.r.t.)h(to)g(normalized)183 2077 y(substitutions)e(and)f(goals)g(of)g (the)h(form)e Fy(s)g Fx(=)900 2083 y Fr(?)930 2077 y Fy(N)5 b Fx(,)14 b(where)i Fy(N)j Fx(is)c(a)f(ground)g(normal)f(form.) 183 2127 y(The)h(simple)e(pro)q(of)i(of)f(the)i(next)f(preparatory)h (lemma)10 b(is)k(omitted.)183 2204 y Fn(Lemma)h(3.5)h(:)29 b Fm(L)n(et)14 b Fy(s)i Fm(b)n(e)f(a)g(term)f(and)i Fy(t)e Fm(b)n(e)h(a)g(gr)n(ound)h(term.)199 2279 y(1.)k(Every)f(solution)h Fy(\033)g Fm(of)f(the)g(go)n(al)h Fy(s)f Fx(=)868 2285 y Fr(?)906 2279 y Fy(t)g Fm(satis\014es)g Fq(D)q Fx(\()p Fy(\033)q Fx(\))h Fq(\023)g(V)s Fx(\()p Fy(s)p Fx(\))h Fm(and)e(mor)n(e)n(over,)253 2329 y Fy(\033)277 2336 y Fp(jV)r Fr(\()p Fl(s)p Fr(\))369 2329 y Fm(is)14 b(a)h(gr)n(ound)h (substitution.)199 2382 y(2.)k(Every)c(right-hand)f(side)h(of)f(a)h(go) n(al)g(which)f(c)n(omes)h(into)f(existenc)n(e)h(during)g(the)g(c)n(om-) 253 2432 y(putation)g(of)e(the)h(go)n(al)g Fy(s)d Fx(=)683 2438 y Fr(?)713 2432 y Fy(t)j Fm(is)f(gr)n(ound)i(at)e(the)h(time)g(of) g(its)f(evaluation.)h Fh(2)893 2556 y Fx(7)p eop %%Page: 8 8 8 7 bop 340 194 a Fn(Theorem)15 b(3.6:)f Fx(\(Completeness)g(w.r.t.)f (v)n(ariable-preserving)h(TRSs\))340 244 y Fm(L)n(et)i Fy(s)h Fm(b)n(e)f(a)g(term,)g Fy(N)21 b Fm(a)16 b(term)f(in)h(gr)n (ound)h(normal)f(form,)f(and)i Fy(\033)g Fm(a)g(normalize)n(d)f (substi-)340 293 y(tution)f(with)g Fq(D)q Fx(\()p Fy(\033)q Fx(\))d(=)g Fq(V)s Fx(\()p Fy(s)p Fx(\))p Fm(.)k(If)f Fy(s\033)e Fx(=)939 299 y Fp(R)982 293 y Fy(N)5 b Fm(,)14 b(then)i(ther)n(e)e(is)h(a)g(suc)n(c)n(essful)g(c)n(omputation)g(of)340 343 y Fy(s)d Fx(=)403 349 y Fr(?)433 343 y Fy(N)20 b Fm(with)14 b(r)n(esult)i Fx(~)-23 b Fy(\033)16 b Fm(such)f(that)i Fx(~)-23 b Fy(\033)13 b Fx(=)f Fy(\033)q Fx([)p Fq(V)s Fx(\()p Fy(s)p Fx(\)])p Fm(.)340 479 y(Pr)n(o)n(of.)20 b Fx(F)m(or)14 b(tec)o(hnical)g(reasons,)g(w)o(e)h(pro)o(v)o(e)f(the)g (follo)o(wing)d(more)i(general)h(claim.)340 529 y Fn(Claim:)g Fm(L)n(et)h Fy(s)g Fm(b)n(e)g(a)h(term,)e Fy(t)h Fm(a)g(gr)n(ound)h (term,)e(and)i Fy(\033)g Fm(a)f(normalize)n(d)g(substitution)g(with)340 579 y Fq(D)q Fx(\()p Fy(\033)q Fx(\))e(=)e Fq(V)s Fx(\()p Fy(s)p Fx(\))p Fm(.)16 b(If)e Fy(s\033)f Fq(!)735 564 y Fl(n)735 590 y Fp(R)776 579 y Fy(t)i Fm(via)f(an)g(innermost)g (derivation,)g(then)h(ther)n(e)e(is)h(a)g(suc)n(c)n(essful)340 628 y(c)n(omputation)i(of)g Fy(s)d Fx(=)691 634 y Fr(?)721 628 y Fy(t)i Fm(with)g(r)n(esult)i Fx(~)-24 b Fy(\033)17 b Fm(such)f(that)h Fx(~)-23 b Fy(\033)14 b Fx(=)e Fy(\033)q Fx([)p Fq(V)s Fx(\()p Fy(s)p Fx(\)])p Fm(.)k(Mor)n(e)n(over,)f(if)g(no) h(rule)340 678 y(is)c(applie)n(d)h(at)f(a)g(r)n(o)n(ot)g(p)n(osition,)g (then)h(we)f(may)g(assume)h(that)f(the)h(suc)n(c)n(essful)f(c)n (omputation)340 728 y(starts)i(with)h(a)g(De)n(c)n(omp)n(ose)g(step.) 403 787 y Fx(The)10 b(theorem)f(is)g(a)g(sp)q(ecial)h(case)g(of)f(this) h(claim)d(b)q(ecause)k(if)e Fy(t)i Fq(\021)h Fy(N)i Fx(is)9 b(a)h(term)e(in)h(ground)340 837 y(normal)h(form,)g(then)j(the)f (existence)i(of)e(an)f(innermost)h(rewriting)g(deriv)n(ation)f Fy(s\033)i Fq(!)1685 821 y Fl(n)1685 848 y Fp(R)1726 837 y Fy(t)f Fx(is)340 886 y(equiv)n(alen)o(t)f(to)g Fy(s\033)j Fx(=)672 892 y Fp(R)714 886 y Fy(t)p Fx(.)d(Clearly)m(,)f Fy(\033)i Fx(m)o(ust)f(b)q(e)h(ground,)f(since)h Fq(R)g Fx(is)f(v)n(ariable-preserving.)403 945 y(The)h(pro)q(of)g(is)g(b)o(y)g (induction)f(on)h Fy(n)p Fx(,)g(the)g(length)g(of)g(the)g(rewrite)h (deriv)n(ation.)e(If)h Fy(n)f Fx(=)h(0,)340 995 y(then)17 b Fy(s\033)e Fq(\021)g Fy(t)g Fx(yields)g(the)h(syn)o(tactic)g(matc)o (hing)e(problem)g Fy(s)h Fx(=)1352 1001 y Fr(?)1384 995 y Fy(t)g Fx(whic)o(h)h(can)f(b)q(e)h(solv)o(ed)340 1045 y(b)o(y)21 b(R)432 1040 y(R)462 1045 y(.)f(So)g(let)h Fy(n)i Fq(\025)g Fx(1.)d(Clearly)m(,)f Fy(s)k Fq(6\021)g Fy(x)e Fx(b)q(ecause)h Fy(\033)g Fx(is)f(normalized.)d(So)j(w)o(e)f(ha) o(v)o(e)340 1095 y Fy(s)12 b Fq(\021)g Fy(f)t Fx(\()p Fy(s)474 1101 y Fr(1)494 1095 y Fy(;)7 b(:)g(:)g(:)e(;)i(s)606 1101 y Fl(m)637 1095 y Fx(\),)j Fy(m)i Fq(\025)g Fx(0)d(and)h Fy(t)h Fq(\021)h Fy(g)q Fx(\()p Fy(t)996 1101 y Fr(1)1015 1095 y Fy(;)7 b(:)g(:)g(:)e(;)i(t)1123 1101 y Fl(q)1141 1095 y Fx(\),)i Fy(q)j Fq(\025)g Fx(0.)d(In)h(the)g(innermost)f(deriv)n (ation)340 1144 y Fy(s\033)15 b Fq(\021)f Fy(T)468 1150 y Fr(0)500 1144 y Fq(\000)-6 b(!)505 1165 y Fl(p)522 1169 y Fe(1)538 1165 y Fl(;R)573 1169 y Ff(i)584 1175 y Fe(1)603 1165 y Fl(;\033)632 1169 y Fe(1)665 1144 y Fy(T)689 1150 y Fr(1)722 1144 y Fq(!)13 b(\001)7 b(\001)g(\001)12 b(!)h Fy(T)918 1150 y Fl(n)p Fp(\000)p Fr(1)996 1144 y Fq(\000)-6 b(!)1001 1165 y Fl(p)1018 1169 y Ff(n)1038 1165 y Fl(;R)1073 1169 y Ff(i)1084 1173 y(n)1107 1165 y Fl(;\033)1136 1169 y Ff(n)1174 1144 y Fy(T)1198 1150 y Fl(n)1234 1144 y Fq(\021)14 b Fy(t)h Fx(ev)o(ery)g Fy(T)1444 1150 y Fl(j)1477 1144 y Fx(is)g(ground.)g(Let)g Fq(P)340 1211 y Fx(b)q(e)i(the)g(set)g(of)f(redex)h(p)q(ositions)f(in)f (the)i(deriv)n(ation,)e(i.e.)g Fq(P)k Fx(:=)c Fq(f)p Fy(p)1432 1217 y Fl(i)1462 1211 y Fq(j)g Fx(1)g Fq(\024)h Fy(i)g Fq(\024)f Fy(n)p Fq(g)p Fx(.)h(W)m(e)340 1261 y(distinguish)e(b)q(et)o(w)o(een:)h(\(1\))e Fy(\017)f Fq(2)f(P)17 b Fx(and)d(\(2\))g Fy(\017)d Fq(62)g(P)s Fx(.)340 1319 y(\(1\))16 b Fy(\017)d Fq(2)h(P)s Fx(:)h(Let)h Fy(j)g Fx(:=)e(max)n Fq(f)p Fy(k)i Fq(j)f Fy(p)891 1325 y Fl(k)925 1319 y Fx(=)f Fy(\017;)7 b Fx(1)13 b Fq(\024)h Fy(k)h Fq(\024)f Fy(n)p Fq(g)p Fx(,)h(so)g(the)h(j-th)f(rewrite)h(step) h(is)e(the)340 1369 y(last)g(rewrite)h(step)f(at)g(a)f(ro)q(ot)h(p)q (osition.)e(W)m(e)i(ha)o(v)o(e)f Fy(T)1190 1375 y Fr(0)1222 1369 y Fq(!)1264 1353 y Fl()f Fx(0)h Fq(2)f Fk(I)-6 b(N)p Fq(g)p Fx(.)p 500 1361 1123 2 v 499 1411 2 50 v 506 1396 a Fn(strategy)p 923 1411 V 252 w(#)16 b(solutions)p 1189 1411 V 24 w(#)g(branc)o(hes)p 1442 1411 V 9 w(#)g(dead)p 1621 1411 V 499 1461 V 923 1461 V 990 1446 a(found)p 1189 1461 V 91 w(un\014nishe)o(d)p 1440 1461 V 59 w(ends)p 1621 1461 V 500 1462 1123 2 v 499 1512 2 50 v 506 1497 a Fx(R)533 1492 y(R)p 923 1512 V 1047 1497 a(1)p 1189 1512 V 237 w(0)p 1440 1512 V 195 w(3)p 1621 1512 V 500 1514 1123 2 v 499 1564 2 50 v 506 1549 a(forw)o(ard)d(decomp)q(osition) p 924 1564 V 128 w(1)p 1189 1564 V 237 w(0)p 1440 1564 V 195 w(6)p 1621 1564 V 500 1565 1123 2 v 499 1615 2 50 v 506 1600 a(innermost)g(narro)o(wing)p 923 1615 V 154 w(16)p 1189 1615 V 227 w(3)p 1440 1615 V 195 w(2)p 1621 1615 V 500 1617 1123 2 v 499 1667 2 50 v 506 1652 a(left-righ)o(t)g(basic)h(narr.)p 923 1667 V 165 w(25)p 1189 1667 V 227 w(3)p 1440 1667 V 195 w(4)p 1621 1667 V 500 1668 1123 2 v 500 1678 V 499 1728 2 50 v 506 1713 a(needed)h(narro)o(wing)p 923 1728 V 221 w(1)p 1189 1728 V 237 w(0)p 1440 1728 V 195 w(2)p 1621 1728 V 500 1730 1123 2 v 340 1788 a(With)f(R)475 1783 y(R)518 1788 y(the)h(follo)o (wing)c(successful)16 b(computation)c(is)i(obtained:)676 1856 y(\([)p Fy(g)q Fx(\()p Fy(X)q(;)7 b(f)t Fx(\()p Fy(X)s Fx(\)\))13 b(=)949 1862 y Fr(?)979 1856 y Fy(c)p Fx(\()p Fy(a)p Fx(\)])p Fy(;)7 b Fq(;)p Fx(\))450 1895 y Fl(M)s(utate)p Fr(1)582 1899 y Ff(R)603 1905 y Fe(6)493 1925 y Fq(\000)-6 b(!)509 1938 y( )f Fy(-)676 1925 y Fx(\([)p Fy(a)11 b Fx(=)769 1931 y Fr(?)799 1925 y Fy(a;)c(g)q Fx(\()p Fy(X)q(;)g(f)t Fx(\()p Fy(X)s Fx(\)\))13 b(=)1085 1931 y Fr(?)1114 1925 y Fy(g)q Fx(\()p Fy(b)p Fx(\()p Fy(X)1219 1931 y Fr(1)1239 1925 y Fx(\))p Fy(;)7 b(b)p Fx(\()p Fy(Y)1332 1931 y Fr(1)1350 1925 y Fx(\)\)])p Fy(;)g Fq(;)p Fx(\))429 1964 y Fr(2)p Fp(\002)p Fl(D)q(ecompose)494 1990 y Fq(\000)-7 b(!)510 2002 y( )g Fy(-)676 1990 y Fx(\([)p Fy(X)15 b Fx(=)785 1996 y Fr(?)814 1990 y Fy(b)p Fx(\()p Fy(X)882 1996 y Fr(1)901 1990 y Fx(\))p Fy(;)7 b(f)t Fx(\()p Fy(X)s Fx(\))13 b(=)1074 1996 y Fr(?)1104 1990 y Fy(b)p Fx(\()p Fy(Y)1162 1996 y Fr(1)1181 1990 y Fx(\)])p Fy(;)7 b Fq(;)p Fx(\))450 2029 y Fl(E)r(liminate)p Fr(1)495 2053 y Fq(\000)-7 b(!)511 2065 y( )g Fy(-)676 2053 y Fx(\([)p Fy(f)t Fx(\()p Fy(b)p Fx(\()p Fy(X)812 2059 y Fr(1)832 2053 y Fx(\)\))11 b(=)907 2059 y Fr(?)937 2053 y Fy(b)p Fx(\()p Fy(Y)995 2059 y Fr(1)1014 2053 y Fx(\)])p Fy(;)c Fq(f)p Fy(X)14 b Fq( )d Fy(b)p Fx(\()p Fy(X)1251 2059 y Fr(1)1270 2053 y Fx(\))p Fq(g)p Fx(\))450 2091 y Fl(M)s(utate)p Fr(1)582 2095 y Ff(R)603 2101 y Fe(2)493 2122 y Fq(\000)-6 b(!)509 2134 y( )f Fy(-)676 2122 y Fx(\([)p Fy(f)t Fx(\()p Fy(X)778 2128 y Fr(2)798 2122 y Fx(\))11 b(=)857 2128 y Fr(?)887 2122 y Fy(Y)911 2128 y Fr(1)930 2122 y Fy(;)c(f)t Fx(\()p Fy(b)p Fx(\()p Fy(X)1057 2128 y Fr(1)1076 2122 y Fx(\)\))12 b(=)1152 2128 y Fr(?)1181 2122 y Fy(f)t Fx(\()p Fy(b)p Fx(\()p Fy(X)1289 2128 y Fr(2)1309 2122 y Fx(\)\)])p Fy(;)7 b Fq(f)p Fy(X)14 b Fq( )d Fy(b)p Fx(\()p Fy(X)1562 2128 y Fr(1)1581 2122 y Fx(\))p Fq(g)p Fx(\))450 2161 y Fl(E)r(liminate)p Fr(2)495 2185 y Fq(\000)-7 b(!)511 2197 y( )g Fy(-)676 2185 y Fx(\([)p Fy(f)t Fx(\()p Fy(b)p Fx(\()p Fy(X)812 2191 y Fr(1)832 2185 y Fx(\)\))11 b(=)907 2191 y Fr(?)937 2185 y Fy(f)t Fx(\()p Fy(b)p Fx(\()p Fy(X)1045 2191 y Fr(2)1065 2185 y Fx(\)\)])p Fy(;)c Fq(f)p Fy(X)14 b Fq( )d Fy(b)p Fx(\()p Fy(X)1318 2191 y Fr(1)1337 2185 y Fx(\))p Fy(;)c(Y)1396 2191 y Fr(1)1426 2185 y Fq( )k Fy(f)t Fx(\()p Fy(X)1553 2191 y Fr(2)1573 2185 y Fx(\))p Fq(g)p Fx(\))429 2223 y Fr(2)p Fp(\002)p Fl(D)q(ecompose)494 2249 y Fq(\000)-7 b(!)510 2261 y( )g Fy(-)676 2249 y Fx(\([)p Fy(X)738 2255 y Fr(1)768 2249 y Fx(=?)p Fy(X)854 2255 y Fr(2)873 2249 y Fx(])p Fy(;)7 b Fq(f)p Fy(X)14 b Fq( )d Fy(b)p Fx(\()p Fy(X)1094 2255 y Fr(1)1113 2249 y Fx(\))p Fy(;)c(Y)1172 2255 y Fr(1)1202 2249 y Fq( )k Fy(f)t Fx(\()p Fy(X)1329 2255 y Fr(2)1349 2249 y Fx(\))p Fq(g)p Fx(\))450 2288 y Fl(E)r(liminate)p Fr(1)495 2312 y Fq(\000)-7 b(!)511 2324 y( )g Fy(-)676 2312 y Fx(\([)12 b(])p Fy(;)7 b Fq(f)p Fy(X)14 b Fq( )d Fy(b)p Fx(\()p Fy(X)937 2318 y Fr(2)956 2312 y Fx(\))p Fy(;)c(Y)1015 2318 y Fr(1)1045 2312 y Fq( )k Fy(f)t Fx(\()p Fy(X)1172 2318 y Fr(2)1192 2312 y Fx(\))p Fy(;)c(X)1261 2318 y Fr(1)1291 2312 y Fq( )k Fy(X)1378 2318 y Fr(2)1397 2312 y Fq(g)p Fx(\))p 340 2345 237 2 v 349 2372 a Fg(5)379 2388 y Fw(Needed)23 b(narro)o(wing)g(is)g(not)g(implemen)o(ted)h(in)f Fd(PaNaMa)s Fw(.)e(The)h(result)h(is)g(according)h(to)379 2433 y([AEH94].)1040 2556 y Fx(12)p eop %%Page: 13 13 13 12 bop 245 194 a Fx(The)19 b(coming)e(o\013)i(w)o(ell)f(of)g(R)715 189 y(R)764 194 y(results)i(from)d(the)j(fact)f(that)g(at)f(the)i(b)q (eginning)e(of)183 244 y(the)13 b(deriv)n(ation)f(only)g Fy(R)569 250 y Fr(6)600 244 y Fx(can)h(b)q(e)g(applied.)f(The)h(three)h (failing)d(computations)g(c)o(hose)j(the)183 293 y(rules)g Fy(R)314 299 y Fr(4)333 293 y Fy(;)7 b(R)384 299 y Fr(7)415 293 y Fx(or)14 b Fy(R)498 299 y Fr(8)531 293 y Fx(instead)g(of)g Fy(R)754 299 y Fr(2)786 293 y Fx(for)g(the)g(second)i(Mutate1)e(step.)h (These)g(dead)g(ends)183 343 y(can)f(b)q(e)g(foreseen)i(b)o(y)d(using)h (a)f(tec)o(hnique)i(whic)o(h)f(is)g(in)o(tro)q(duced)g(next.)183 468 y Fn(4.3)47 b(Op)q(erator)15 b(Deriv)m(abili)o(t)o(y)183 551 y Fx(In)c(order)h(to)f(further)i(reduce)g(rule)e(nondeterminism,)e (w)o(e)j(pro)o(vide)f(the)h(R)1347 546 y(R)1388 551 y(calculus)g(with) 183 601 y(some)h(kno)o(wledge)h(ab)q(out)f(the)i(forw)o(ard)f(deriv)n (ation)f(paths.)h(This)f(is)h(a)g(\014rst)h(approac)o(h)f(to)183 651 y(com)o(bine)g(kind)h(of)f(a)i(forw)o(ard)e(strategy)j(with)e(a)g (rev)o(erse)i(strategy)m(.)e(W)m(e)g(will)f(do)h(this)h(b)o(y)183 700 y(adopting)d(the)h(tec)o(hnique)h(of)e Fm(op)n(er)n(ator)i(r)n (ewriting)d Fx([DS87)n(])i(or)g Fm(op)n(er)n(ator)g(derivability)p Fx(.)183 771 y Fn(De\014niti)o(on)f(4.5)k(:)e Fx(\(Op)q(erator)h(TRS)e Fq(R)841 777 y Fp(O)q(P)897 771 y Fx(\))h(The)g(TRS)f Fq(R)1147 777 y Fp(O)q(P)1217 771 y Fx(is)g(deriv)o(ed)i(from)d(a)h (TRS)183 821 y Fq(R)h Fx(b)o(y)g(the)g(follo)o(wing)e(rules:)i(F)m(or)f (eac)o(h)i(de\014ned)g(function)f(in)f Fq(R)p Fx(,)h(w)o(e)g(add)g(a)f (rule)i Fy(f)i Fq(!)13 b Fy(f)183 871 y Fx(to)j Fq(R)271 877 y Fp(O)q(P)326 871 y Fx(.)g(F)m(or)f(eac)o(h)i(rule)f Fy(g)q Fx(\()p Fy(l)660 877 y Fr(1)680 871 y Fy(;)7 b(:)g(:)g(:)t(;)g (l)784 877 y Fl(q)802 871 y Fx(\))16 b Fq(!)e Fy(f)t Fx(\()p Fy(r)949 877 y Fr(1)969 871 y Fy(;)7 b(:)g(:)g(:)e(;)i(r)1081 877 y Fl(m)1111 871 y Fx(\))16 b Fq(2)g(R)29 b Fx(where)17 b Fy(f)k Fx(is)16 b(a)f(de\014ned)183 920 y(function,)e(w)o(e)h(add)g (a)f(rule)h Fy(g)f Fq(!)e Fy(f)19 b Fx(to)14 b Fq(R)827 926 y Fp(O)q(P)882 920 y Fx(.)183 991 y Fn(De\014niti)o(on)c(4.6)j(:)e Fx(\(Op)q(erator)i(deriv)n(abilit)o(y\))c(Giv)o(en)i(a)g(TRS)g Fq(R)1205 997 y Fp(O)q(P)1260 991 y Fx(,)g(w)o(e)g(call)g(an)g(op)q (erator)183 1041 y Fy(f)18 b Fx(deriv)n(able)c(from)e Fy(g)q Fx(,)i(if)f(there)i(is)f(a)f(rewriting)h(deriv)n(ation)f Fy(g)g Fq(!)1211 1026 y Fp(\003)1211 1052 y(R)1240 1056 y Fi(O)q(P)1300 1041 y Fy(f)t Fx(.)245 1111 y(W)m(e)g(no)o(w)h(com)o (bine)f(the)h(Mutate1)g(rule)g(with)g(a)g(deriv)n(abilit)o(y)e(c)o(hec) o(k,)i(excluding)g(suc)o(h)183 1161 y(Mutate1)g(steps)h(whic)o(h)f (will)e(nev)o(er)j(lead)f(to)f(a)h(solution.)183 1232 y Fn(De\014niti)o(on)f(4.7)i(:)183 1302 y(Mutate1)362 1287 y Fp(0)372 1302 y Fn(:)183 1352 y Fx(\([)p Fy(h)p Fx(\()p Fy(s)270 1358 y Fr(1)288 1352 y Fy(;)7 b(:)g(:)g(:)e(;)i(s)400 1358 y Fl(p)419 1352 y Fx(\))12 b(=)479 1358 y Fr(?)509 1352 y Fy(f)t Fx(\()p Fy(s)568 1337 y Fp(0)568 1363 y Fr(1)588 1352 y Fy(;)7 b(:)g(:)g(:)t(;)g(s)699 1337 y Fp(0)699 1362 y Fl(m)731 1352 y Fx(\))p Fy(;)g(L)794 1358 y Fr(1)812 1352 y Fy(;)g(:)g(:)g(:)e(;)i(L)933 1358 y Fl(n)955 1352 y Fx(])p Fy(;)g(\033)q Fx(\))p Fq(\000)-7 b(!)1041 1365 y( )g Fy(-)183 1402 y Fx(\([)p Fy(r)230 1408 y Fr(1)259 1402 y Fx(=)291 1408 y Fr(?)321 1402 y Fy(s)340 1387 y Fp(0)340 1412 y Fr(1)359 1402 y Fy(;)7 b(:)g(:)g(:)e(;)i(r)471 1408 y Fl(m)513 1402 y Fx(=)545 1408 y Fr(?)574 1402 y Fy(s)593 1387 y Fp(0)593 1412 y Fl(m)625 1402 y Fy(;)g(h)p Fx(\()p Fy(s)703 1408 y Fr(1)722 1402 y Fy(;)g(:)g(:)g(:)e(;)i(s)834 1408 y Fl(p)853 1402 y Fx(\))12 b(=)913 1408 y Fr(?)942 1402 y Fy(g)q Fx(\()p Fy(l)991 1408 y Fr(1)1011 1402 y Fy(;)7 b(:)g(:)g(:)t(;)g(l) 1115 1408 y Fl(q)1134 1402 y Fx(\))p Fy(;)g(L)1197 1408 y Fr(1)1215 1402 y Fy(;)g(:)g(:)g(:)e(;)i(L)1336 1408 y Fl(n)1358 1402 y Fx(])p Fy(;)g(\033)q Fx(\))p Fy(;)183 1452 y Fm(if)14 b Fy(g)q Fx(\()p Fy(l)272 1458 y Fr(1)291 1452 y Fy(;)7 b(:)g(:)g(:)e(;)i(l)396 1458 y Fl(q)414 1452 y Fx(\))12 b Fq(!)f Fy(f)t Fx(\()p Fy(r)554 1458 y Fr(1)573 1452 y Fy(;)c(:)g(:)g(:)e(;)i(r)685 1458 y Fl(m)716 1452 y Fx(\))15 b Fm(is)f(a)h(r)n(ename)n(d)h(rule)e(fr)n(om)g Fq(R)p Fm(,)h Fy(h)c Fq(!)1316 1437 y Fp(\003)1316 1463 y(R)1345 1467 y Fi(O)q(P)1406 1452 y Fy(g)q Fm(,)183 1502 y(and)k(Eliminate1)g(do)n(es)g(not)g(apply.)245 1572 y Fx(In)e(con)o(trast)h(to)e([DS87)o(],)g(w)o(e)h(do)g(not)g (consider)h(collapsing)e(rules)h(for)g(op)q(erator)h(deriv-)183 1622 y(abilit)o(y)m(,)9 b(whic)o(h)j(w)o(ould)f(add)h(to)g Fq(R)717 1628 y Fp(O)q(P)784 1622 y Fx(for)g(ev)o(ery)g(collapsing)f (rule)h(as)g(man)o(y)f(rules)h(as)g(there)183 1672 y(are)h(de\014ned)h (functions)f(in)f Fq(R)p Fx(.)h(Of)g(course,)h(w)o(e)f(also)f(need)i (not)f(add)g(rules)g Fy(f)k Fq(!)11 b Fy(c)h Fx(to)h Fq(R)1568 1678 y Fp(O)q(P)183 1722 y Fx(where)k Fy(c)e Fx(is)h(a)f(constructor,)i(since)g(these)g(rules)g(w)o(ould)e(nev)o(er) h(b)q(e)h(used)g(in)e(a)g(deriv)n(ation)183 1772 y Fy(h)h Fq(!)265 1756 y Fp(\003)265 1783 y(R)294 1787 y Fi(O)q(P)359 1772 y Fy(g)q Fx(,)h(where)g Fy(g)h Fx(is)f(a)f(de\014ned)i(function.)e (Therefore,)i(within)e(the)h(framew)o(ork)e(of)183 1821 y(R)210 1816 y(R)240 1821 y(,)e(op)q(erator)i(deriv)n(abilit)o(y)e(b)q (ecomes)h(a)g(more)g(e\013ectiv)o(e)i(and)e(imp)q(ortan)o(t)e (optimization)183 1871 y(than)i(in)f(the)h(con)o(text)h(of)e([DS87)o (].)183 1942 y Fn(Theorem)h(4.8:)g Fx(\(completeness)h(of)e(R)813 1937 y(R)857 1942 y(w.r.t.)g(op)q(erator)h(deriv)n(abilit)o(y\))183 1992 y Fm(L)n(et)19 b Fq(R)31 b Fm(b)n(e)19 b(a)h(c)n(anonic)n(al,)f (variable-pr)n(eserving)f(or)h(left-line)n(ar)e(TRS.)i(R)1369 1987 y(R)1419 1992 y(is)g(c)n(omplete)183 2041 y(w.r.t.)c(normalize)n (d)i(substitutions)g(for)g(go)n(als)g Fy(s)g Fx(=)994 2047 y Fr(?)1028 2041 y Fy(N)m Fm(,)g(wher)n(e)f(N)i(is)f(in)g(gr)n (ound)h(normal)183 2091 y(form,)c(if)g(Mutate1)h(is)g(r)n(eplac)n(e)n (d)f(by)i(Mutate1)904 2076 y Fp(0)916 2091 y Fm(.)183 2183 y(Pr)n(o)n(of.)k Fx(W)m(e)14 b(pro)o(v)o(e)h(the)h(claim)d(for)i (v)n(ariable-preserving)g(TRSs.)f(The)h(left-linear)g(case)h(is)183 2232 y(analogous.)245 2282 y(Recapitulate)10 b(the)h(pro)q(of)f(of)f (Theorem)h(3.6.)f(There)i(is)f(only)g(one)g(situation)g(\(case)h (1\(ii\)\))183 2332 y(where)k(explicitly)f(a)g(Mutate1)h(step)g(is)f (applied.)g(W)m(e)g(sho)o(w)g(that)h(the)g(prerequisites)h(of)e(a)183 2382 y(Mutate1)336 2367 y Fp(0)360 2382 y Fx(step)f(are)f(also)g (ful\014lled.)e(W)m(e)i(considered)h(the)g(follo)o(wing)c(innermost)j (rewriting)183 2432 y(deriv)n(ation:)882 2556 y(13)p eop %%Page: 14 14 14 13 bop 340 194 a Fy(s\033)16 b Fq(\021)f Fy(T)470 200 y Fr(0)503 194 y Fq(\000)-7 b(!)507 214 y Fl(p)524 218 y Fe(1)540 214 y Fl(;R)575 218 y Ff(i)586 224 y Fe(1)605 214 y Fl(;\033)634 218 y Fe(1)668 194 y Fy(T)692 200 y Fr(1)725 194 y Fq(!)14 b(\001)7 b(\001)g(\001)12 b(!)i Fy(T)923 200 y Fl(n)p Fp(\000)p Fr(1)1002 194 y Fq(\000)-6 b(!)1007 214 y Fl(p)1024 218 y Ff(n)1045 214 y Fl(;R)1080 218 y Ff(i)1091 222 y(n)1113 214 y Fl(;\033)1142 218 y Ff(n)1181 194 y Fy(T)1205 200 y Fl(n)1242 194 y Fq(\021)14 b Fy(t)p Fx(,)h(where)h Fy(s)f Fq(\021)f Fy(f)t Fx(\()p Fy(s)1590 200 y Fr(1)1610 194 y Fy(;)7 b(:)g(:)g(:)e(;)i(s)1722 200 y Fl(m)1754 194 y Fx(\),)340 256 y Fy(m)12 b Fq(\025)g Fx(0.)340 306 y(F)m(or)k(the)h(case)g(that)f(there)h(are)f(rewrite)h (steps)h(at)d(ro)q(ot)h(p)q(ositions,)g(w)o(e)g(de\014ned)h(the)g(j-th) 340 355 y(step)e(as)f(the)h(last)e(one)h(of)g(those,)g(with)f Fy(R)999 361 y Fl(i)1011 365 y Ff(j)1040 355 y Fx(:)e Fy(l)i Fq(!)e Fy(r)j Fx(as)g(the)h(rule)f(used.)340 405 y(W)m(e)h(obtained:)g Fy(s\033)g Fq(!)697 389 y Fl(