%!PS-Adobe-2.0 %%Creator: dvips 5.526 Copyright 1986, 1994 Radical Eye Software %%Title: perm5.dvi %%CreationDate: Mon Feb 23 15:47:49 1998 %%Pages: 11 %%PageOrder: Ascend %%BoundingBox: 0 0 596 842 %%EndComments %DVIPSCommandLine: /sw/tex/bin/Dvips perm5 %DVIPSParameters: dpi=300, comments removed %DVIPSSource: TeX output 1998.02.23:1535 %%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 (/mnt3/home/math/schwicht/wwwpublic/papers/gentzen97/perm5.dvi) @start /Fa 44 123 df<0007E1F0001C173800703C3800E07C7801C0783001C0380001 C0380001C038000380700003807000038070003FFFFF0003807000038070000700E00007 00E0000700E0000700E0000700E0000700E0000E01C0000E01C0000E01C0000E01C0000E 01C0000E01C0001C0380001C03C000FF8FF8001D1D7F9C18>11 D<000400080030006000 C0008001800300060006000C000C001800180038003000300070007000600060006000E0 00E000E000E000E000E000E000E0006000600060006000200030003000180008000C0004 0002000E2A7C9E10>40 D<0100008000400060002000300010001800180018001C000C00 0C000C000C000C000C000C000C001C001C001C0018001800380038003000300070006000 E000C001C001800300030006000C0018003000600080000E2A809E10>I<387878380808 101020204080050C7D830C>44 D<7FF0FFE00C027F890E>I<7070F06004047C830C>I<00 18007003F00C7000700070007000E000E000E000E000E000E001C001C001C001C001C001 C003800380038003800380038007000780FFF80D1C7C9B15>49 D<007E000183800201C0 0400E00400E00F00E00F00E01F00E01F00E00E00E00001E00001C0000380000380000700 000E00001C0000380000600000C0000180000300800600800801001001003FFF007FFE00 FFFE00131C7E9B15>I<007C000187000203800403800F03C00F03C00F03C00E03800003 80000700000600000C0000380003F000001C00000E00000E00000F00000F00000F00700F 00F80F00F80F00F00E00E01E00801C004038003070000FC000121D7D9B15>I<00002000 0000300000007000000070000000F0000000F0000001F000000378000002780000067800 00047800000C780000087C0000183C0000103C0000203C0000203C0000403C0000403E00 00FFFE0000801E0001001E0001001E0002001E0002000F0004000F0004000F001E001F00 FF80FFF01C1D7F9C1F>65 D<0007F010001C0C300070026000C001E0038000E0070000E0 0E0000600E0000601C0000403C00004038000040780000007800000078000000F0000000 F0000000F0000000F0000000F0000000F0000080F0000100700001007000010038000200 380004001C0004000C001800060020000380C000007F00001C1E7C9C1E>67 D<0FFFFC0000F8078000F001C000F000E000F0007000F0007000F0007801E0003801E000 3801E0003801E0003801E0003C01E0003803C0003803C0007803C0007803C0007803C000 7003C000F0078000E0078000E0078001C0078003800780078007800E000F001C000F0070 00FFFFC0001E1C7E9B20>I<0FFFFFC000F803C000F001C000F0008000F0008000F00080 00F0008001E0008001E0408001E0400001E0400001E0C00001E1C00003FF800003C18000 03C0800003C0800003C0800003C080000780000007800000078000000780000007800000 078000000F0000000F800000FFF800001A1C7E9B1B>70 D<0FFF8000F80000F00000F000 00F00000F00000F00001E00001E00001E00001E00001E00001E00003C00003C00003C000 03C00003C00003C0000780000780000780000780000780000780000F00000F8000FFF800 111C7F9B0F>73 D<0FFFC000F80000F00000F00000F00000F00000F00001E00001E00001 E00001E00001E00001E00003C00003C00003C00003C00003C00003C00407800407800407 80040780080780080780180F00380F00F0FFFFF0161C7E9B1A>76 D<0FFFFC0000F80F0000F0038000F003C000F001C000F001C000F001C001E003C001E003 C001E003C001E0038001E0070001E00E0003C03C0003FFE00003C0000003C0000003C000 0003C000000780000007800000078000000780000007800000078000000F0000000F8000 00FFF000001A1C7E9B1C>80 D<1FFFFFF03C07C0F0300780302007802060078020400780 2040078020400F0020800F0020000F0000000F0000000F0000000F0000001E0000001E00 00001E0000001E0000001E0000001E0000003C0000003C0000003C0000003C0000003C00 00003C000000780000007C00001FFFE0001C1C7C9B1E>84 DI<01FC01FC01800180030003000300030003000300060006000600060006000600 0C000C000C000C000C000C00180018001800180018001800300030003000300030003000 600060006000600060007F00FE000E297E9E0C>91 D<01FC01FC000C000C001800180018 00180018001800300030003000300030003000600060006000600060006000C000C000C0 00C000C000C0018001800180018001800180030003000300030003007F00FE000E29829E 0C>93 D<07F0001C18001E0C001C0E00180E00000E00000E0001FE000F0E001C1C00301C 00701C00E01C40E01C40E03C40E05C80709D803F0E0012127D9115>97 D<3F00000F00000E00000E00000E00000E00000E00000E00001C00001C00001C00001C78 001D86001E03003C03803801803801803801C03801C03801C07003807003807003807003 00700700700E00F00C00CC300083C000121D7C9C17>I<01F8071C0C1E181C3818300070 0070007000E000E000E000600060047008301018200FC00F127D9112>I<0003F00000F0 0000E00000E00000E00000E00000E00000E00001C00001C00001C000F1C0030DC00C03C0 1C0380380380300380700380700380700380E00700E00700E00700600700600700700F00 301E00186F00078FC0141D7D9C17>I<01F8070C0C061C073803300370037FFF7000E000 E000E00060006002300430081C3007C010127E9112>I<000F800039C00061C000E3C001 C18001C00001C00001C0000380000380000380003FF80003800003800007000007000007 00000700000700000700000E00000E00000E00000E00000E00000E00001C00001E0000FF C000121D7F9C0D>I<000038003CCC00C69C018308038380070380070380070380070380 070700030600038C0004F0000400000C00000C00000FFE0007FF800FFFC01801C02000C0 6000E0C000C0C000C0600180200300180E0007F000161C809215>I<07E00001E00001C0 0001C00001C00001C00001C00001C000038000038000038000038F8003B0C003C0E00780 E00780E00700E00700E00700E00700E00E01C00E01C00E01C00E01C00E01C00E01C01C03 801E03C0FF9FF0141D7F9C17>I<00C001C001C001800000000000000000000000000000 1F80078003800700070007000700070007000E000E000E000E000E000E001C001E00FF80 0A1D7F9C0C>I<07E00001E00001C00001C00001C00001C00001C00001C0000380000380 000380000387F80381E003818007020007040007080007100007700007F8000F38000E3C 000E1C000E1E000E0E000E0F001C07001C0F80FF9FE0151D7F9C16>107 D<07E001E001C001C001C001C001C001C003800380038003800380038007000700070007 00070007000E000E000E000E000E000E001C001E00FF800B1D7F9C0C>I<1F8FC0FC0007 9061060003E0760700078078070007807807000700700700070070070007007007000700 7007000E00E00E000E00E00E000E00E00E000E00E00E000E00E00E000E00E00E001C01C0 1C001E01E01E00FF8FF8FF8021127F9124>I<1F8F8007B0C003C0E00780E00780E00700 E00700E00700E00700E00E01C00E01C00E01C00E01C00E01C00E01C01C03801E03C0FF9F F014127F9117>I<00FC000307000E01801C01C03800C03000C07000E07000E07000E0E0 01C0E001C0E001C0600180600380700700380E001C180007E00013127E9115>I<0FC780 03D86001E03003C03803803803801803801C03801C03801C070038070038070038070070 0700700700E00F01C00EC3000E3C000E00000E00000E00001C00001C00001C00001C0000 FF8000161A809117>I<00F0400308C00E05C01C03803803803803807003807003807003 80E00700E00700E00700600700700700700F00301E00186E00078E00000E00000E00000E 00001C00001C00001C00001C0000FF80121A7D9116>I<1F9C07EE03CF078E078C070007 00070007000E000E000E000E000E000E001C001E00FFC010127F9110>I<03F20C0E1806 1004300438043E001FE00FF007F8003C401C400C400C6018E010D0608FC00F127F9110> I<020002000200060006000C001C003C00FFE01C001C0038003800380038003800380070 0070407040704070407080708031001E000B1A7C9910>IIII<0FF0FE03C03801C03001C02001C06001C04001E08000E08000E100 00E10000E200007200007400007C00007800007000003000002000002000004000004000 708000F10000F10000E60000780000171A809116>121 D<0FFF800E0700080E00180E00 101C0010380010700000E00001C00001C0000382000702000E02001C0400380400380C00 703800FFF80011127F9112>I E /Fb 6 106 df<0006000C001800300070006000C001C0 018003800300070006000E000C001C001C00180038003800380030007000700070007000 70007000E000E000E000E000E000E000E000E000E000E000E000E000E000E000E000E000 E000E000700070007000700070007000300038003800380018001C001C000C000E000600 070003000380018001C000C00060007000300018000C00060F4A788119>16 DI<0000700001F00003C0000780000E00001C00003800007000 00700000F00000E00000E00000E00000E00000E00000E00000E00000E00000E00000E000 00E00000E00000E00000E00000E00000E00000E00000E00000E00000E00000E00000E000 00E00000E00000E00000E00000E00000E00000E00000E00001C00001C00001C000038000 0700000600000E0000380000700000C000007000003800000E0000060000070000038000 01C00001C00001C00000E00000E00000E00000E00000E00000E00000E00000E00000E000 00E00000E00000E00000E00000E00000E00000E00000E00000E00000E00000E00000E000 00E00000E00000E00000E00000E00000E00000E00000E00000E00000F000007000007000 003800001C00000E000007800003C00001F000007014637B811F>26 D88 D104 DI E /Fc 4 83 df<0000000000200000000000600000000000C000 0000000180000000000300000000000600000000000C0000000000180000000000300000 000000600000000000C0000000000180000000000300000000000600000000000C000000 0000180000000000300000000000600000000000C0000000000180000000000300000000 000600000000000C0000000000180000000000300000000000600000000000C000000000 0180000000000300000000000600000000000C0000000000180000000000300000000000 600000000000C0000000000180000000000300000000000600000000000C000000000018 0000000000300000000000600000000000C000000000008000000000002B2C80AA2A>0 D<0100018003C003E003F007F807FC07FE0FFF0FFC1FE01F003C00700060008000101080 8F2A>9 D<800000000000C000000000006000000000003000000000001800000000000C 000000000006000000000003000000000001800000000000C00000000000600000000000 3000000000001800000000000C0000000000060000000000030000000000018000000000 00C000000000006000000000003000000000001800000000000C00000000000600000000 0003000000000001800000000000C0000000000060000000000030000000000018000000 00000C000000000006000000000003000000000001800000000000C00000000000600000 0000003000000000001800000000000C0000000000060000000000030000000000018000 00000000C00000000000600000000000202B2C80AA2A>64 D<0080018003C007C00FC01F E03FE07FE0FFF03FF007F800F8003C000E000600011010668F2A>82 D E /Fd 22 122 df<60F0F06004047B830D>46 D<000FE0200070186001C00460030003 E0060001E00E0000E01C00006038000060380000207800002070000020F0000000F00000 00F0000000F0000000F0000000F0000000F0000000F00000007000002078000020380000 20380000201C0000400E000040060000800300010001C0060000701800000FE0001B1E7D 9C21>67 DI76 D80 D<001FC00000F0780001C01C00070007000E0003801E0003 C01C0001C0380000E0780000F0780000F070000070F0000078F0000078F0000078F00000 78F0000078F0000078F0000078F000007870000070780000F0780000F0380000E01C0701 C01C08C1C00E1043800710670003D07E0000F87808001FF008000038080000381800001C 3800001FF000000FF0000007E0000003C01D257D9C23>II<7FFFFFC0700F01C0600F00C0400F0040400F0040C00F0020800F0020800F002080 0F0020000F0000000F0000000F0000000F0000000F0000000F0000000F0000000F000000 0F0000000F0000000F0000000F0000000F0000000F0000000F0000000F0000000F000000 1F800003FFFC001B1C7D9B21>84 D<00200000700000700000700000B80000B80000B800 011C00011C00011C00020E00020E0004070004070007FF000803800803800803801801C0 3803C0FE0FF815157F9419>97 D100 DII104 DI107 DIII<01F800070E000C03001C03803801C07801E07000E0F000F0F000F0F000F0F000F0F0 00F0F000F0F000F07000E07801E03801C01C03801E0780070E0001F80014157E941A>I< FFF8001C0E001C07801C03801C03C01C03C01C03C01C03801C07801C0E001FF8001C1C00 1C0E001C07001C07001C07001C07801C07841C07C41C03CCFF80F816157F9419>114 D<7FFFF06070304070104070108070088070088070080070000070000070000070000070 0000700000700000700000700000700000700000700000700007FF0015157F9419>116 D121 D E /Fe 4 94 df<18F818181818181818181818FF080D7D8C0E>49 D<3E00418080C0C0C000C000C0018003000400084030407F80FF800A0D7E8C0E>I91 D93 D E /Ff 5 121 df<0018000038000038 00005800009800008C00010C00020C00060C0007FE00080600100600300600F81F80110E 7E8D16>65 D<1FFE000601800600C00600C00C01800C03000FFE000C0700180180180180 180180180300300E00FFF800120E7E8D16>I<73809C40986030C030C030C03188619060 E00D097D8812>110 D<0C0C0C18FE1818303030323438070D7E8C0C>116 D<1CF0231823100600060006004610CE2073C00D097F8810>120 D E /Fg 6 95 df0 D<040004000400C460E4E03F800E00 3F80E4E0C4600400040004000B0D7E8D11>3 D<00000400000004000000020000000100 FFFFFFE0FFFFFFE0000001000000020000000400000004001B0A7E8B21>33 D<040E0E1C1C1C38383070706060C0C0070F7F8F0A>48 D<400040C000C0600180600180 3003003003003FFF001FFE001806000C0C000C0C00061800061800033000033000033000 01E00001E00000C00000C0001214809314>56 D<0180018003C003C0066006600C300C30 181818181818300C300C60066006C003C00110117E9016>94 D E /Fh 37 122 df<0102040C1818303070606060E0E0E0E0E0E0E0E0E0E060606070303018 180C04020108227D980E>40 D<8040203018180C0C0E0606060707070707070707070706 06060E0C0C18183020408008227E980E>I<60F0F070101020204040040A7D830A>44 DI<60F0F06004047D830A>I<0F8030E040708030C038E0384038 003800700070006000C00180030006000C08080810183FF07FF0FFF00D157E9412>50 D<07E018302018600C600C700C78183E101F600FC00FF018F8607C601EC00EC006C006C0 04600C38300FE00F157F9412>56 D72 D<0FFC00E000E000E000E000E000E000E0 00E000E000E000E000E000E000E000E000E000E0E0E0E0E0C1C061801F000E177E9612> 74 D76 DI80 D<7FFFF86038184038084038088038048038048038040038000038000038000038 0000380000380000380000380000380000380000380000380000380000380000380007FF C016177F9619>84 D91 D93 D<1FC0386038301038003803F81E38303870 38E039E039E07970FF1F1E100E7F8D12>97 DI<07F01838303870106000E000E0 00E000E000600070083008183007C00D0E7F8D10>I<007E00000E00000E00000E00000E 00000E00000E00000E00000E0007CE001C3E00300E00700E00600E00E00E00E00E00E00E 00E00E00600E00700E00301E00182E0007CFC012177F9614>I<0FC0186030307038E018 FFF8E000E000E000600070083010183007C00D0E7F8D10>I<03E006700E701C201C001C 001C001C001C00FF801C001C001C001C001C001C001C001C001C001C001C001C00FF800C 1780960B>I<0F9E18E33060707070707070306018C02F80200060003FE03FF83FFC600E C006C006C006600C38380FE010157F8D12>II<183C3C1800000000007C1C1C1C 1C1C1C1C1C1C1C1C1CFF081780960A>I108 DII<07C018303018600C600CE00EE00EE00EE00EE00E701C3018183007C00F0E7F 8D12>II<07 C2001C2600381E00700E00600E00E00E00E00E00E00E00E00E00600E00700E00301E001C 2E0007CE00000E00000E00000E00000E00000E00007FC012147F8D13>II<1F4060C0C040C0 40E000FF007F801FC001E080608060C060E0C09F000B0E7F8D0E>I<0800080008001800 18003800FF80380038003800380038003800380038403840384038401C800F000A147F93 0E>IIII121 D E /Fi 1 50 df<0C003C00CC000C000C000C000C000C000C000C000C000C00 0C000C000C00FF8009107E8F0F>49 D E /Fj 50 123 df<183C3C3C0404080810204080 060C779C0D>39 D<183878380808101020404080050C7D830D>44 DI<3078F06005047C830D>I<00020006000C001C007C039C 0038003800380038007000700070007000E000E000E000E001C001C001C001C003800380 038003800780FFF00F1C7C9B15>49 D<0001800001C00003800003800003800003000007 00000700000600000E00000C00001C0000180000180000300000300000600000400000C6 00018E00010E00020E00061C000C1C00181C003F1C0040F800803F000038000038000070 0000700000700000700000E00000600012247E9B15>52 D<001E00006100008180018080 0300C00300C006018006018006018007030007860003CC0003F00001F000037800063C00 081E00180E00300E00600600600600600600C00C00C00C00C0180060100060200030C000 0F0000121D7C9B15>56 D<003C0000C6000183000303000603000E03000C03801C03801C 03001C0300380700380700380700380F00380E00181E00181E000C6C00079C00001C0000 1800003800003000006000E0C000E0C0008180008600007C0000111D7B9B15>I<060F0F 06000000000000000000003078F06008127C910D>I<0000180000001800000038000000 380000007800000078000000B8000001B800000138000002380000023C0000041C000004 1C0000081C0000181C0000101C0000201C0000201C00007FFC0000401C0000801C000180 1C0001001C0002001C0002001C0004000E000C000E001C001E00FF00FFC01A1D7E9C1F> 65 D<01FFFE00003C0780003803C0003801C0003801C0003801C0007001C0007003C000 7003C00070078000E0070000E00E0000E03C0000FFF80001C01C0001C00E0001C00F0001 C00F0003800F0003800F0003800F0003800F0007001E0007001C0007003C00070078000E 01E000FFFF80001A1C7D9B1D>I<0003F020001E0C60003002E000E003C001C001C00380 01C0070000C00E0000801E0000801C0000803C0000803C00000078000000780000007800 0000F0000000F0000000F0000000F0000000F0000400F0000400F0000400F00008007000 08007000100038002000180040000C0180000706000001F800001B1E7A9C1E>I<01FFFE 00003C0780003801C0003801C0003800E0003800E0007000F00070007000700070007000 F000E000F000E000F000E000F000E000F001C001E001C001E001C001E001C001C0038003 C003800380038007800380070007000E0007001C0007003800070070000E01C000FFFF00 001C1C7D9B1F>I<01FFFFE0003C00E00038006000380040003800400038004000700040 00700040007020400070200000E0400000E0400000E0C00000FFC00001C0800001C08000 01C0800001C0800003810100038001000380020003800200070004000700040007000C00 070018000E007800FFFFF0001B1C7D9B1C>I<01FFFFC0003C01C0003800C00038008000 380080003800800070008000700080007020800070200000E0400000E0400000E0C00000 FFC00001C0800001C0800001C0800001C080000381000003800000038000000380000007 0000000700000007000000070000000F000000FFF000001A1C7D9B1B>I<0003F020001E 0C60003002E000E003C001C001C0038001C0070000C00E0000801E0000801C0000803C00 00803C000000780000007800000078000000F0000000F0000000F001FFC0F0001E00F000 1C00F0001C00F0001C00F0001C00700038007000380038003800180078000C0090000707 100001F800001B1E7A9C20>I<01FFCFFE003C01E0003801C0003801C0003801C0003801 C00070038000700380007003800070038000E0070000E0070000E0070000FFFF0001C00E 0001C00E0001C00E0001C00E0003801C0003801C0003801C0003801C0007003800070038 0007003800070038000F007800FFE7FF001F1C7D9B1F>I<01FFC0FF003C003C00380030 0038004000380080003801000070020000700400007010000070200000E0400000E0C000 00E1C00000E5C00001C8E00001D0E00001E0E00001C07000038070000380700003803800 038038000700380007001C0007001C0007001C000F001E00FFE0FF80201C7D9B20>75 D<01FFE0003C0000380000380000380000380000700000700000700000700000E00000E0 0000E00000E00001C00001C00001C00001C0000380080380080380080380100700100700 300700600700E00E03C0FFFFC0151C7D9B1A>I<01FE0007F8003E000780002E000F0000 2E001700002E001700002E002700004E002E00004E004E00004E004E00004E008E00008E 011C00008E011C00008E021C00008E021C00010704380001070438000107083800010710 38000207107000020720700002072070000207407000040740E000040780E000040700E0 000C0700E0001C0601E000FF861FFC00251C7D9B25>I<01FC03FE001C0070003C006000 2E0040002E0040002E004000470080004700800047008000438080008381000083810000 8181000081C1000101C2000101C2000100E2000100E2000200E400020074000200740002 0074000400380004003800040038000C0018001C001000FF8010001F1C7D9B1F>I<01FF FC00003C070000380380003801C0003801C0003801C0007003C0007003C0007003C00070 038000E0078000E0070000E00E0000E0380001FFE00001C0000001C0000001C000000380 0000038000000380000003800000070000000700000007000000070000000F000000FFE0 00001A1C7D9B1C>80 D<000F8400304C00403C0080180100180300180300180600100600 1006000007000007000003E00003FC0001FF00007F800007C00001C00001C00000C00000 C02000C02000C0600180600180600300600200F00400CC180083E000161E7D9C17>83 D<1FFFFFC01C0701C0300E00C0200E0080600E0080400E0080401C0080801C0080801C00 80001C000000380000003800000038000000380000007000000070000000700000007000 0000E0000000E0000000E0000000E0000001C0000001C0000001C0000001C0000003C000 007FFE00001A1C799B1E>I<7FF0FF800F001C000E0018000E0010000E0010000E001000 1C0020001C0020001C0020001C0020003800400038004000380040003800400070008000 700080007000800070008000E0010000E0010000E0010000E0020000E0020000E0040000 E00400006008000030300000104000000F800000191D779B1F>I87 D<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<0FC00001C00001C000038000038000038000038000070000 0700000700000700000E0F000E11000E23800E43801C83001C80001D00001E00003F8000 39C00038E00038E00070E20070E20070E20070E400E06400603800111D7D9C13>107 D<1F800380038007000700070007000E000E000E000E001C001C001C001C003800380038 0038007000700070007000E400E400E400E40068003800091D7C9C0B>I<3C1E07802663 18C04683A0E04703C0E08E0380E08E0380E00E0380E00E0380E01C0701C01C0701C01C07 01C01C070380380E0388380E0388380E0708380E0710701C0320300C01C01D127C9122> I<3C3C002646004687004707008E07008E07000E07000E07001C0E001C0E001C0E001C1C 00381C40381C40383840383880701900300E0012127C9117>I<01E007180C0C180C380C 300E700E700EE01CE01CE01CE018E038E030E06060C031801E000F127B9115>I<078700 04D98008E0C008E0C011C0E011C0E001C0E001C0E00381C00381C00381C0038180070380 0703000707000706000E8C000E70000E00000E00001C00001C00001C00001C00003C0000 FF8000131A7F9115>I<03C4062C0C3C181C3838303870387038E070E070E070E070E0E0 C0E0C0E061E063C03DC001C001C0038003800380038007803FF00E1A7B9113>I<3C3C26 C2468747078E068E000E000E001C001C001C001C0038003800380038007000300010127C 9112>I<01F006080C080C1C18181C001F001FC00FF007F0007800386030E030C0308060 60C01F000E127D9111>I<00C001C001C001C00380038003800380FFE00700070007000E 000E000E000E001C001C001C001C00384038403840388019000E000B1A7D990E>I<1E03 00270700470700470700870E00870E000E0E000E0E001C1C001C1C001C1C001C1C003838 803838801838801839001C5900078E0011127C9116>I<1E06270E470E4706870287020E 020E021C041C041C041C0818083808181018200C4007800F127C9113>I<070E00199100 10E38020E38041C30041C00001C00001C000038000038000038000038000070200670200 E70400CB04008B080070F00011127D9113>120 D<1E03270747074707870E870E0E0E0E 0E1C1C1C1C1C1C1C1C38383838183818381C7007F00070007000E0E0C0E1C0818047003C 00101A7C9114>I<038207C20FEC08381008001000200040008001000200040008081008 383067F043E081C00F127D9111>I E /Fk 23 122 df<000E00001E00007E0007FE00FF FE00FFFE00F8FE0000FE0000FE0000FE0000FE0000FE0000FE0000FE0000FE0000FE0000 FE0000FE0000FE0000FE0000FE0000FE0000FE0000FE0000FE0000FE0000FE0000FE0000 FE0000FE0000FE0000FE0000FE0000FE0000FE0000FE007FFFFE7FFFFE7FFFFE17277BA6 22>49 D<00FF800007FFF0000FFFFC001E03FE003800FF807C003F80FE003FC0FF001FC0 FF001FE0FF000FE0FF000FE07E000FE03C001FE000001FE000001FC000001FC000003F80 00003F0000007E000000FC000000F8000001F0000003E00000078000000F0000001E0000 003C00E0007000E000E000E001C001C0038001C0060001C00FFFFFC01FFFFFC03FFFFFC0 7FFFFFC0FFFFFF80FFFFFF80FFFFFF801B277DA622>I<007F800003FFF00007FFFC000F 80FE001F007F003F807F003F803F803F803F803F803F801F803F801F003F8000007F0000 007F0000007E000000FC000001F8000007F00000FFC00000FFC0000001F80000007E0000 003F0000003F8000001FC000001FC000001FE000001FE03C001FE07E001FE0FF001FE0FF 001FE0FF001FC0FF003FC0FE003F807C007F003F00FE001FFFFC0007FFF00000FF80001B 277DA622>I68 D77 D80 D82 D<03FF80000FFFF0001F01FC003F80FE003F 807F003F803F003F803F801F003F8000003F8000003F8000003F8000003F80003FFF8001 FC3F800FE03F801F803F803F003F807E003F80FC003F80FC003F80FC003F80FC003F80FC 005F807E00DF803F839FFC1FFE0FFC03F803FC1E1B7E9A21>97 D<003FF00001FFFC0003 F03E000FC07F001F807F003F007F003F007F007F003E007E0000007E000000FE000000FE 000000FE000000FE000000FE000000FE000000FE0000007E0000007E0000007F0000003F 0003803F8003801F8007000FE00E0003F83C0001FFF800003FC000191B7E9A1E>99 D<003FC00001FFF00003E07C000F803E001F801F001F001F003F000F807E000F807E000F C07E000FC0FE0007C0FE0007C0FFFFFFC0FFFFFFC0FE000000FE000000FE0000007E0000 007E0000007F0000003F0001C01F0001C00F80038007C0070003F01E0000FFFC00003FE0 001A1B7E9A1F>101 D<0007F8003FFC007E3E01FC7F03F87F03F07F07F07F07F03E07F0 0007F00007F00007F00007F00007F00007F000FFFFC0FFFFC0FFFFC007F00007F00007F0 0007F00007F00007F00007F00007F00007F00007F00007F00007F00007F00007F00007F0 0007F00007F00007F00007F00007F00007F0007FFF807FFF807FFF80182A7EA915>I<07 000F801FC03FE03FE03FE01FC00F8007000000000000000000000000000000FFE0FFE0FF E00FE00FE00FE00FE00FE00FE00FE00FE00FE00FE00FE00FE00FE00FE00FE00FE00FE00F E00FE00FE00FE0FFFEFFFEFFFE0F2B7EAA12>105 D108 DII<003FE00001FF FC0003F07E000FC01F801F800FC03F0007E03F0007E07E0003F07E0003F07E0003F0FE00 03F8FE0003F8FE0003F8FE0003F8FE0003F8FE0003F8FE0003F8FE0003F87E0003F07E00 03F03F0007E03F0007E01F800FC00FC01F8007F07F0001FFFC00003FE0001D1B7E9A22> I<003F807001FFE0F003F071F00FC019F01F800FF03F800FF03F0007F07F0007F07F0007 F07E0007F0FE0007F0FE0007F0FE0007F0FE0007F0FE0007F0FE0007F0FE0007F0FE0007 F07F0007F07F0007F03F0007F03F8007F01F800FF00FC01FF007F077F001FFE7F0007F87 F0000007F0000007F0000007F0000007F0000007F0000007F0000007F0000007F0000007 F000007FFF00007FFF00007FFF20277E9A23>113 DI<03FE300FFFF03E03F07800F07000F0F00070F00070F80070FE0000FFE0007FFF007F FFC03FFFE01FFFF007FFF800FFF80007FC0000FCE0007CE0003CF0003CF00038F80038FC 0070FF01E0E7FFC0C1FF00161B7E9A1B>I<00700000700000700000700000F00000F000 00F00001F00003F00003F00007F0001FFFE0FFFFE0FFFFE007F00007F00007F00007F000 07F00007F00007F00007F00007F00007F00007F00007F00007F00007F07007F07007F070 07F07007F07007F07007F07003F0E001F8C000FFC0003F0014267FA51A>III121 D E /Fl 23 111 df0 D<60F0F06004047C8B0C>I<03 C00FF01FF83FFC7FFE7FFEFFFFFFFFFFFFFFFF7FFE7FFE3FFC1FF80FF003C010107E9115 >15 D21 D<07C000201FE000203FF80020783C0060E01F00E0C00783C08003FF808000FF0080 007C001B097E8E20>24 D<02000000000400000000040000000008000000001000000000 2000000000FFFFFFFFF0FFFFFFFFF0200000000010000000000800000000040000000004 000000000200000000240E7D902A>32 D<00000004000000000200000000020000000001 0000000000800000000040FFFFFFFFF8FFFFFFFFF8000000004000000000800000000100 000000020000000002000000000400250E7E902A>I<0000030000000003000000000180 000000018000000000C00000000060007FFFFFF000FFFFFFF8000000000E000000000700 00000001E0000000007800000001E0000000038000000006000000001C00FFFFFFF8007F FFFFF0000000006000000000C00000000180000000018000000003000000000300002518 7E952A>41 D<007FF801FFF80780000E0000180000300000300000600000600000C00000 C00000C00000FFFFF8FFFFF8C00000C00000C00000600000600000300000300000180000 0E000007800001FFF8007FF8151A7D961C>50 D<0000600000600000C00000C000018000 0180000180000300000300000600000600000C00000C0000180000180000180000300000 300000600000600000C00000C0000180000180000300000300000300000600000600000C 00000C0000180000180000300000300000300000600000600000C0000040000013287A9D 00>54 DI<400004C0000C6000186000 186000183000303000303000301800601800601FFFE00FFFC00C00C00C00C00601800601 8003030003030003030001860001860001860000CC0000CC0000CC000078000078000078 00003000003000161E809C17>II< 00040000000C0000000C0000000C0000000C0000000C0000000C0000000C0000000C0000 000C0000000C0000000C0000000C0000000C0000000C0000000C0000000C0000000C0000 000C0000000C0000000C0000000C0000000C0000000C0000000C0000000C0000FFFFFFE0 FFFFFFE01B1C7D9B21>63 D<400002C00006C00006C00006C00006C00006C00006C00006 C00006C00006C00006C00006C00006C00006C00006C00006C00006C00006C0000660000C 60000C3000181C00700F01E003FF8000FE00171A7E981C>91 D<00100000380000380000 6C00006C00006C0000C60000C6000183000183000301800301800600C00600C00600C00C 00600C006018003018003030001830001830001860000C60000CC00006C00002171A7E98 1C>94 DI<003C00E001C001800380038003800380038003 800380038003800380038003800380030007001C00F0001C000700030003800380038003 80038003800380038003800380038003800380018001C000E0003C0E297D9E15>102 DI<008001800300030003000600060006000C00 0C000C00180018001800300030003000600060006000C000C00060006000600030003000 30001800180018000C000C000C0006000600060003000300030001800080092A7C9E10> III110 D E /Fm 16 122 df<0C0C0C0C0C0C18181818181818 18303030323032307278B46F1C60006000C000C000C00080000F137E8C14>22 D<3FFE7FFEC440844004400CC008C008C018C018C030C030E020400F0D7E8C13>25 D<03FE0FFE18603030603060306030C060C060C0C0408023001E000F0D7E8C13>27 D<40E06020202040408003097D820A>59 D<000100000300000700000780000B80001B80 0013800023800023800043800083800083C00101C003FFC00201C00401C00401C00801C0 1801E0FE07F815147F9319>65 D<07FFE000E03801C01801C01C01C01C01C01C03803803 80700380E003FFC00700E00700700700300700380E00700E00700E00E00E00E01C0380FF FE0016147F9319>I<003F0800C0980300700600300C0030180030380020700000700000 700000E00000E00000E00000E000406000806000803001003002000C1C0007E00015147E 9318>I<07800C4010E031C0600060006000C000C0004020404021801E000B0D7E8C0F> 99 D<06070600000000384C4C8C98181830326262643808147F930C>105 D<30F8590C4E0C9C0C980C180C180C30183019303130316032601C100D7F8C15>110 D<02000600060006000C00FF800C000C001800180018001800300031003100320032001C 0009127F910D>116 D<380C4C0C4C0C8C18981818181818303030323032307218B40F1C 0F0D7F8C14>I<38104C304C108C10981018101810302030203040304018800F000C0D7F 8C11>I<3818204C18604C18208C30209830201830201830203060403060403060803060 8018B1000F1E00130D7F8C18>I<0E3C13CE238E430C43000300030006000608C608E610 CA2071C00F0D7F8C13>I<38184C184C188C3098301830183030603060306030E011C00E C000C00080E180E30046003C000D137F8C11>I E /Fn 9 94 df<010204081030206060 40C0C0C0C0C0C0C0C0C0C040606020301008040201081E7E950D>40 D<80402010080C0406060203030303030303030303020606040C0810204080081E7E950D >I<006000006000006000006000006000006000006000006000006000006000FFFFF0FF FFF000600000600000600000600000600000600000600000600000600000600014167E91 19>43 D<0F0030C0606060604020C030C030C030C030C030C030C030C030C03040206060 606030C00F000C137E9211>48 D<0C001C00EC000C000C000C000C000C000C000C000C00 0C000C000C000C000C000C000C00FFC00A137D9211>I<1F0060C06060F070F030603000 700070006000C001C00180020004000810101020207FE0FFE00C137E9211>I<0FC03070 7038703870380038003000E00FC0007000380018001C601CF01CF018E03860701FC00E13 7F9211>I91 D93 D E /Fo 11 79 df<78FCFCFCFC7806067D850D>46 D<00600001E0000FE000FFE000F3E00003E00003E00003E00003E00003E00003E00003E0 0003E00003E00003E00003E00003E00003E00003E00003E00003E00003E00003E00003E0 0003E0007FFF807FFF80111B7D9A18>49 D<07F8001FFE00383F80780FC0FC07C0FC07E0 FC03E0FC03E07803E00007E00007C00007C0000F80001F00001E0000380000700000E000 0180600300600600600800E01FFFC03FFFC07FFFC0FFFFC0FFFFC0131B7E9A18>I<03F8 001FFE003C1F003C0F807C07C07E07C07C07C03807C0000F80000F80001E00003C0003F8 00001E00000F800007C00007C00007E03007E07807E0FC07E0FC07E0FC07C0780F80781F 001FFE0007F800131B7E9A18>I<000180000380000780000F80001F80003F80006F8000 CF80008F80018F80030F80060F800C0F80180F80300F80600F80C00F80FFFFF8FFFFF800 0F80000F80000F80000F80000F80000F8001FFF801FFF8151B7F9A18>I<1801801FFF00 1FFE001FFC001FF8001FC00018000018000018000018000019F8001E0E00180F80100780 0007C00007E00007E00007E07807E0F807E0F807E0F807C0F007C0600F80381F001FFE00 07F000131B7E9A18>I<007E0003FF000781800F03C01E07C03C07C03C03807800007800 00F80000F8F800FB0E00FA0780FC0380FC03C0F803E0F803E0F803E0F803E07803E07803 E07803C03C03C03C07801E0F0007FE0003F800131B7E9A18>I<6000007FFFE07FFFE07F FFC07FFF807FFF80E00300C00600C00C00C0180000300000300000600000E00000E00001 E00001C00003C00003C00003C00003C00007C00007C00007C00007C00007C00007C00003 8000131C7D9B18>I<07FFF007FFF0001F80001F80001F80001F80001F80001F80001F80 001F80001F80001F80001F80001F80001F80001F80001F80001F80001F80001F80301F80 781F80FC1F80FC1F80FC1F00783E00387C000FF000141C7F9B19>74 D76 D78 D E /Fp 32 127 df<0001F000061800080C00100C00200E00400E00800E00801C01001C 010018010038020FF00210C0020FE0020030040030040030040038040038080070080070 0800700800E01800E01800C0140180140300230E0020F800200000200000400000400000 40000040000080000080000017257F9C17>12 D<007C00C2010203000600060006000700 078003C001E001F003780E381C1C381C300C700C700CE008E008E018E010E010E0306020 604030801F000F1D7E9C12>14 D<07800001C00000E00000E00000F00000700000700000 7000003800003800003800003C00001C00001C00001E00000E00001E00003F0000670000 C7000187800303800703800E03801C03C03801C07001C0E001E06000E0131D7E9C18>21 D<0180300380700380700380700700E00700E00700E00700E00E01C00E01C00E01C00E01 C01C03881C03881C03881E07883E19903BE0E03800003800007000007000007000007000 00E00000E00000C00000151B7F9119>I<7E00600E00E00E00E00E00E01C01C01C01C01C 03801C0300380700380E00380C0038180070300070600071C000730000FC0000F0000013 127E9115>I<0FFFF81FFFF83FFFF0608400408400808C00010C00010C00030C00030C00 020C00061C00061C000E1C000C1C001C0E001C0E00180C0015127E9118>25 D<01FFF803FFF80FFFF01E1E00180E00380600700600700600E00E00E00E00E00E00E00C 00E01C00E01800E0300060600030C0001F000015127E9118>27 D<60F0F06004047C830C >58 D<60F0F0701010101020204080040C7C830C>I<00010003000600060006000C000C 000C0018001800180030003000300060006000C000C000C0018001800180030003000300 060006000C000C000C00180018001800300030003000600060006000C000C00010297E9E 15>61 DI<00 000C0000000C0000001C0000001C0000003C0000007C0000005C0000009C0000008E0000 010E0000010E0000020E0000040E0000040E0000080E0000080E0000100E0000200E0000 3FFE0000400700004007000080070001000700010007000200070002000700060007001E 000700FF807FF01C1D7F9C1F>65 D<01FFFF00003C01C0003800E0003800F00038007000 38007000700070007000F0007000F0007001E000E003C000E0078000E01F0000FFFC0001 C00F0001C0078001C003C001C003C0038003C0038003C0038003C0038003C00700078007 00070007000E0007001C000E007800FFFFC0001C1C7E9B1F>I<0001F808000E06180038 0138006000F001C0007003800070070000300F0000200E0000201C0000203C0000203C00 0000780000007800000078000000F0000000F0000000F0000000F0000000F0000100F000 0100F0000100700002007000020030000400380008001C0010000E0060000701800000FE 00001D1E7E9C1E>I<01FFFF80003C01E000380070003800380038001C0038001C007000 1C0070001E0070001E0070001E00E0001E00E0001E00E0001E00E0001E01C0003C01C000 3C01C0003C01C000380380007803800070038000F0038000E0070001C007000380070007 0007001C000E007800FFFFC0001F1C7E9B22>I<01FFFFF0003C00F00038003000380020 00380020003800200070002000700020007010200070100000E0200000E0200000E06000 00FFE00001C0400001C0400001C0400001C0400003808000038000000380000003800000 070000000700000007000000070000000F000000FFF000001C1C7E9B1B>70 D<0001F808000E061800380138006000F001C0007003800070070000300F0000200E0000 201C0000203C0000203C000000780000007800000078000000F0000000F0000000F0007F F0F0000780F0000700F0000700F00007007000070070000E0030000E0038000E001C001E 000E0064000701840000FE00001D1E7E9C21>I<01FFC07F80003C001E00003800180000 3800200000380040000038008000007002000000700400000070080000007010000000E0 40000000E0C0000000E1E0000000E2E0000001C470000001D070000001E038000001C038 0000038038000003801C000003801C000003800E000007000E000007000E000007000700 0007000700000F00078000FFE03FF000211C7E9B23>75 D<01FFE0003C00003800003800 00380000380000700000700000700000700000E00000E00000E00000E00001C00001C000 01C00001C00003800203800203800203800407000407000C0700180700380E00F0FFFFF0 171C7E9B1C>I<01FE0000FF003E0000F0002E0001E0002E0002E0002E0002E0002E0004 E0004E0009C0004E0009C000470011C000470011C0008700238000870043800087004380 008700838001070107000107010700010382070001038207000203840E000203880E0002 03880E000203900E000403A01C000403A01C000401C01C000C01C01C001C01803C00FF81 03FF80281C7E9B28>I<01FC00FF80001C001C00002E001800002E001000002E00100000 2700100000470020000043002000004380200000438020000081C040000081C040000081 C040000080E040000100E080000100708000010070800001007080000200390000020039 0000020039000002001D000004001E000004000E000004000E00000C000E00001C000400 00FF80040000211C7E9B21>I<01C003C003C001800000000000000000000000001C0027 0047004700870087000E000E001C001C001C003800388038807080710032001C000A1C7E 9B0E>105 D<381F004E61804681C04701C08F01C08E01C00E01C00E01C01C03801C0380 1C03801C0700380710380710380E10380E2070064030038014127E9119>110 D<01F0060C04040C0E180C1C001F000FE00FF003F80038201C7018F018F010803060601F 800F127E9113>115 D<00C001C001C001C00380038003800380FFF00700070007000E00 0E000E000E001C001C001C001C00382038203840384018800F000C1A80990F>I<1C00C0 2701C04701C04701C08703808703800E03800E03801C07001C07001C07001C0700180E20 180E20180E201C1E200C264007C38013127E9118>I<1C02270747074703870187010E01 0E011C021C021C021C041804180818081C100C2007C010127E9114>I<1C00C0802701C1 C04701C1C04701C0C087038040870380400E0380400E0380401C0700801C0700801C0700 801C07010018060100180602001C0E02001C0F04000E13080003E1F0001A127E911E>I< 07878008C84010F0C020F1E020E3C040E18000E00000E00001C00001C00001C00001C000 638080F38080F38100E5810084C60078780013127E9118>I<1C00C02701C04701C04701 C08703808703800E03800E03801C07001C07001C07001C0700180E00180E00180E001C1E 000C3C0007DC00001C00001800603800F03000F06000E0C0004180003E0000121A7E9114 >I<038107C10FE6081C10080010002000400080010002000400080410042C1877F843F0 81C010127E9113>I<000200000300000300FFFF80FFFF80000700000C00000800110878 9D15>126 D E /Fq 82 128 df0 D<00030000000300000007800000078000000FC000000BC0000013E0000011E0000021F0 000020F0000040F8000040780000807C0000803C0001003E0001001E0002001F0002000F 0004000F8004000780080007C0080003C0100003E0100001E0200000F0200000F07FFFFF F8FFFFFFFCFFFFFFFC1E1D7E9C23>I<007E1F0001C1B1800303E3C00703C3C00E03C180 0E01C0000E01C0000E01C0000E01C0000E01C0000E01C000FFFFFC000E01C0000E01C000 0E01C0000E01C0000E01C0000E01C0000E01C0000E01C0000E01C0000E01C0000E01C000 0E01C0000E01C0000E01C0000E01C0000E01C0007F87FC001A1D809C18>11 D<007E0001C1800301800703C00E03C00E01800E00000E00000E00000E00000E0000FFFF C00E01C00E01C00E01C00E01C00E01C00E01C00E01C00E01C00E01C00E01C00E01C00E01 C00E01C00E01C00E01C00E01C07F87F8151D809C17>I<007FC001C1C00303C00703C00E 01C00E01C00E01C00E01C00E01C00E01C00E01C0FFFFC00E01C00E01C00E01C00E01C00E 01C00E01C00E01C00E01C00E01C00E01C00E01C00E01C00E01C00E01C00E01C00E01C07F CFF8151D809C17>I<003F07E00001C09C18000380F018000701F03C000E01E03C000E00 E018000E00E000000E00E000000E00E000000E00E000000E00E00000FFFFFFFC000E00E0 1C000E00E01C000E00E01C000E00E01C000E00E01C000E00E01C000E00E01C000E00E01C 000E00E01C000E00E01C000E00E01C000E00E01C000E00E01C000E00E01C000E00E01C00 0E00E01C007FC7FCFF80211D809C23>I<00030180000301800003018000060300000603 00000603000006030000060300000C0600000C0600000C0600000C060000180C007FFFFF F8FFFFFFFC00301800003018000030180000301800006030000060300000603000006030 00FFFFFFFC7FFFFFF800C060000180C0000180C0000180C0000180C00003018000030180 0003018000030180000603000006030000060300001E257E9C23>35 D<00E0000001900000030800000308000007080000070800000708000007080000071000 0007100000072000000740000003C03FE003800F00038006000380040005C0040009C008 0010E0100030E010006070200060702000E0384000E03C4000E01C8000E00F0020E00700 20700780403009C0401830E18007C03E001B1F7E9D20>38 D<60F0F86808080810102040 80050C7C9C0C>I<004000800100020006000C000C001800180030003000700060006000 6000E000E000E000E000E000E000E000E000E000E000E000E00060006000600070003000 3000180018000C000C00060002000100008000400A2A7D9E10>I<800040002000100018 000C000C000600060003000300038001800180018001C001C001C001C001C001C001C001 C001C001C001C001C0018001800180038003000300060006000C000C0018001000200040 0080000A2A7E9E10>I<0006000000060000000600000006000000060000000600000006 0000000600000006000000060000000600000006000000060000FFFFFFE0FFFFFFE00006 000000060000000600000006000000060000000600000006000000060000000600000006 00000006000000060000000600001B1C7E9720>43 D<60F0F0701010101020204080040C 7C830C>II<60F0F06004047C830C>I<03C00C301818300C300C 700E60066006E007E007E007E007E007E007E007E007E007E007E007E007E00760066006 700E300C300C18180C3007E0101D7E9B15>48 D<030007003F00C7000700070007000700 070007000700070007000700070007000700070007000700070007000700070007000700 0F80FFF80D1C7C9B15>I<07C01830201C400C400EF00FF80FF807F8077007000F000E00 0E001C001C00380070006000C00180030006010C01180110023FFE7FFEFFFE101C7E9B15 >I<07E01830201C201C781E780E781E381E001C001C00180030006007E00030001C001C 000E000F000F700FF80FF80FF80FF00E401C201C183007E0101D7E9B15>I<000C00000C 00001C00003C00003C00005C0000DC00009C00011C00031C00021C00041C000C1C00081C 00101C00301C00201C00401C00C01C00FFFFC0001C00001C00001C00001C00001C00001C 00001C0001FFC0121C7F9B15>I<300C3FF83FF03FC020002000200020002000200023E0 24302818301C200E000E000F000F000F600FF00FF00FF00F800E401E401C2038187007C0 101D7E9B15>I<00F0030C06040C0E181E301E300C700070006000E3E0E430E818F00CF0 0EE006E007E007E007E007E007600760077006300E300C18180C3003E0101D7E9B15>I< 4000007FFF807FFF007FFF00400200800400800400800800001000001000002000006000 00400000C00000C00001C000018000018000038000038000038000038000078000078000 078000078000078000078000030000111D7E9B15>I<03E00C301008200C200660066006 60067006780C3E083FB01FE007F007F818FC307E601E600FC007C003C003C003C0036002 6004300C1C1007E0101D7E9B15>I<03C00C301818300C700C600EE006E006E007E007E0 07E007E0076007700F300F18170C2707C700060006000E300C780C78187010203030C00F 80101D7E9B15>I<60F0F0600000000000000000000060F0F06004127C910C>I<60F0F060 0000000000000000000060F0F0701010101020204080041A7C910C>I<7FFFFFC0FFFFFF E00000000000000000000000000000000000000000000000000000000000000000FFFFFF E07FFFFFC01B0C7E8F20>61 D<000600000006000000060000000F0000000F0000000F00 000017800000178000001780000023C0000023C0000023C0000041E0000041E0000041E0 000080F0000080F0000180F8000100780001FFF80003007C0002003C0002003C0006003E 0004001E0004001E000C001F001E001F00FF80FFF01C1D7F9C1F>65 DI<001F808000E061800180198007000780 0E0003801C0003801C00018038000180780000807800008070000080F0000000F0000000 F0000000F0000000F0000000F0000000F0000000F0000000700000807800008078000080 380000801C0001001C0001000E000200070004000180080000E03000001FC000191E7E9C 1E>IIII<001F808000E0618001801980070007800E000380 1C0003801C00018038000180780000807800008070000080F0000000F0000000F0000000 F0000000F0000000F0000000F000FFF0F0000F8070000780780007807800078038000780 1C0007801C0007800E00078007000B800180118000E06080001F80001C1E7E9C21>II I<1FFF00F800780078007800780078007800780078007800780078007800780078007800 780078007800787078F878F878F878F0F040E021C01F00101D7F9B15>IIIII<003F800000E0E0000380380007001C000E000E001C0007003C000780380003807800 03C0780003C0700001C0F00001E0F00001E0F00001E0F00001E0F00001E0F00001E0F000 01E0F00001E0700001C0780003C0780003C0380003803C0007801C0007000E000E000700 1C000380380000E0E000003F80001B1E7E9C20>II82 D<07E0801C1980300580700380600180E0 0180E00080E00080E00080F00000F800007C00007FC0003FF8001FFE0007FF0000FF8000 0F800007C00003C00001C08001C08001C08001C0C00180C00180E00300D00200CC0C0083 F800121E7E9C17>I<7FFFFFC0700F01C0600F00C0400F0040400F0040C00F0020800F00 20800F0020800F0020000F0000000F0000000F0000000F0000000F0000000F0000000F00 00000F0000000F0000000F0000000F0000000F0000000F0000000F0000000F0000000F00 00000F0000001F800003FFFC001B1C7F9B1E>I86 DI89 D<7FFFF07C01F07001E06003C06003C0 400780400F80400F00401E00001E00003C00007C0000780000F00000F00001E00003E000 03C0100780100780100F00101F00301E00203C00203C00607800E0F803E0FFFFE0141C7E 9B19>II93 D<0810204040808080B0F87830050C7D9C0C>96 D<1FC000307000783800781C00301C00 001C00001C0001FC000F1C00381C00701C00601C00E01C40E01C40E01C40603C40304E80 1F870012127E9115>II<07E00C30 1878307870306000E000E000E000E000E000E00060007004300418080C3007C00E127E91 12>I<003F00000700000700000700000700000700000700000700000700000700000700 03E7000C1700180F00300700700700600700E00700E00700E00700E00700E00700E00700 600700700700300700180F000C370007C7E0131D7E9C17>I<03E00C301818300C700E60 06E006FFFEE000E000E000E00060007002300218040C1803E00F127F9112>I<00F8018C 071E061E0E0C0E000E000E000E000E000E00FFE00E000E000E000E000E000E000E000E00 0E000E000E000E000E000E000E000E007FE00F1D809C0D>I<00038003C4C00C38C01C38 80181800381C00381C00381C00381C001818001C38000C300013C0001000003000001800 001FF8001FFF001FFF803003806001C0C000C0C000C0C000C06001803003001C0E0007F8 00121C7F9215>II<18003C003C00 18000000000000000000000000000000FC001C001C001C001C001C001C001C001C001C00 1C001C001C001C001C001C001C00FF80091D7F9C0C>I<00C001E001E000C00000000000 0000000000000000000FE000E000E000E000E000E000E000E000E000E000E000E000E000 E000E000E000E000E000E000E000E060E0F0C0F1C061803E000B25839C0D>IIII< FC7C001C87001D03001E03801C03801C03801C03801C03801C03801C03801C03801C0380 1C03801C03801C03801C03801C0380FF9FF014127F9117>I<03F0000E1C001806003003 00700380600180E001C0E001C0E001C0E001C0E001C0E001C06001807003803003001806 000E1C0003F00012127F9115>II<03C1000C3300180B00 300F00700700700700E00700E00700E00700E00700E00700E00700600700700700300F00 180F000C370007C700000700000700000700000700000700000700000700003FE0131A7E 9116>II<1F9030704030C010C010E010F8007F803FE00FF000F8803880 18C018C018E010D0608FC00D127F9110>I<04000400040004000C000C001C003C00FFE0 1C001C001C001C001C001C001C001C001C001C101C101C101C101C100C100E2003C00C1A 7F9910>IIII<7F8FF00F03800F030007 020003840001C80001D80000F00000700000780000F800009C00010E00020E0006070004 03801E07C0FF0FF81512809116>II<7FFC703860384070 40F040E041C003C0038007000F040E041C043C0C380870087038FFF80E127F9112>II<6060F0F0F0F060600C047C9C15>127 D E /Fr 8 122 df<03FF07F0007001C0007001000070020000E0040000E0080000E0100000E040 0001C0800001C1000001C2000001C70000038F00000397000003C3800003838000070380 000701C0000701C0000701C0000E00E0000E00E0000E00E0000E00F0001C00F000FFC3FC 001C1A7D991D>75 D<001F80000380000380000380000700000700000700000700000E00 000E0003CE000E2E00181C00381C00301C00701C00E03800E03800E03800E03800C07200 C07200C0720060F2006134001E1800111A7C9914>100 D<01E006181C08380870087010 FFE0E000E000E000E000E0086010602030C01F000D107C8F12>I<01F006180C0C180E30 0E700E600EE00EE00EE00CE01CE018E030606030C01F000F107C8F14>111 D<30F059189E389C189C009C0038003800380038007000700070007000E00060000D107C 8F10>114 D<03E004300830187018601C001F801FC00FE000E00060E060E06080C04180 3E000C107D8F10>I<380C304C0E384E1C388E1C189C1C189C1C181C3810383810383810 38381070702070702070704030704018B8800F0F0015107C8F19>119 D<38064C074E0E8E0E9C0E9C0E1C1C381C381C381C703870387038307838F00F70007000 6060E0E1C0C18047003C0010177C8F13>121 D E /Fs 1 22 df<0F000003800001C000 01C00001E00000E00000E00000F000007000007000007800003800003800003800003C00 007C0000DC00019E00030E00060E000E0F001C0700380700700780E00380C003C0121A7E 9916>21 D E /Ft 38 123 df<00FC7C0183C607078E0607040E07000E07000E07000E07 000E07000E0700FFFFF00E07000E07000E07000E07000E07000E07000E07000E07000E07 000E07000E07000E07000E07000E07007F0FF0171A809916>11 D<00800100020004000C 00080018003000300030006000600060006000E000E000E000E000E000E000E000E000E0 00E0006000600060006000300030003000180008000C00040002000100008009267D9B0F >40 D<8000400020001000180008000C0006000600060003000300030003000380038003 80038003800380038003800380038003000300030003000600060006000C000800180010 0020004000800009267E9B0F>I<60F0F07010101020204080040B7D830B>44 DI<60F0F06004047D830B>I<60F0F060000000000000000060F0 F06004107D8F0B>58 D<60F0F060000000000000000060F0F0701010102020408004177D 8F0B>I68 D<003F020001C0C60003002E000E001E001C00 0E001C00060038000600780002007000020070000200F0000000F0000000F0000000F000 0000F0000000F001FFC070000E0070000E0078000E0038000E001C000E001C000E000E00 0E000300160001C06600003F82001A1A7E991E>71 D73 D80 D<7FFFFF00701C0700401C0100 401C0100C01C0180801C0080801C0080801C0080001C0000001C0000001C0000001C0000 001C0000001C0000001C0000001C0000001C0000001C0000001C0000001C0000001C0000 001C0000001C0000001C0000001C000003FFE000191A7F991C>84 D<3F8070C070E020700070007007F01C7030707070E070E071E071E0F171FB1E3C10107E 8F13>97 DI<07F80C1C381C30087000E000E000E000E000 E000E0007000300438080C1807E00E107F8F11>I<007E00000E00000E00000E00000E00 000E00000E00000E00000E00000E0003CE000C3E00380E00300E00700E00E00E00E00E00 E00E00E00E00E00E00E00E00600E00700E00381E001C2E0007CFC0121A7F9915>I<07C0 1C3030187018600CE00CFFFCE000E000E000E0006000300438080C1807E00E107F8F11> I<01F0031807380E100E000E000E000E000E000E00FFC00E000E000E000E000E000E000E 000E000E000E000E000E000E000E007FE00D1A80990C>I 104 D<18003C003C001800000000000000000000000000FC001C001C001C001C001C001C 001C001C001C001C001C001C001C001C00FF80091A80990A>I<018003C003C001800000 000000000000000000000FC001C001C001C001C001C001C001C001C001C001C001C001C0 01C001C001C001C001C001C041C0E180E3007E000A2182990C>IIIII<07E01C38300C700E6006E007E007E007E007E007E0076006700E38 1C1C3807E010107F8F13>II<03C2000C2600381E00300E00700E00E00E00E00E 00E00E00E00E00E00E00E00E00700E00700E00381E001C2E0007CE00000E00000E00000E 00000E00000E00000E00007FC012177F8F14>II<1F2060E04020C020C020F0007F 003FC01FE000F080708030C030C020F0408F800C107F8F0F>I<0400040004000C000C00 1C003C00FFC01C001C001C001C001C001C001C001C001C201C201C201C201C200E400380 0B177F960F>IIIIII<7FF8607040 7040E041C041C00380070007000E081C081C08381070107030FFF00D107F8F11>I E /Fu 7 117 df<00030000000780000007800000078000000FC000000FC000001BE000 001BE000001BE0000031F0000031F0000060F8000060F80000E0FC0000C07C0000C07C00 01803E0001FFFE0003FFFF0003001F0003001F0006000F8006000F800E000FC0FFC07FFC FFC07FFC1E1A7F9921>65 D<0FF0001C3C003E1E003E0E003E0F001C0F00000F0000FF00 0FCF003E0F007C0F00F80F00F80F00F80F00F817007C27E01FC3E013117F9015>97 DI<03FC000F0E001C1F003C1F00781F00780E00F80000F8 0000F80000F80000F800007800007800003C01801C03000F060003FC0011117F9014>I< FC78FC9C1D3E1D3E1E3E1E1C1E001E001E001E001E001E001E001E001E00FFC0FFC00F11 7F9012>114 D<1FB020704030C030C030F000FF807FE03FF807F8003CC00CC00CE00CE0 08F830CFE00E117F9011>I<06000600060006000E000E001E003FF0FFF01E001E001E00 1E001E001E001E001E001E181E181E181E181E180F3003E00D187F9711>I E /Fv 15 120 df72 D<03F0200C0C601802603001E07000E0600060E00060E00060E00020E0 0020E00020F00000F000007800007F00003FF0001FFE000FFF0003FF80003FC00007E000 01E00000F00000F0000070800070800070800070800070C00060C00060E000C0F000C0C8 0180C6070081FC0014247DA21B>83 D<0E0000FE00001E00000E00000E00000E00000E00 000E00000E00000E00000E00000E00000E00000E00000E1F000E61C00E80600F00300E00 380E003C0E001C0E001E0E001E0E001E0E001E0E001E0E001E0E001E0E001C0E003C0E00 380F00700C80600C41C0083F0017237FA21B>98 D<01FE000703000C07801C0780380300 780000700000F00000F00000F00000F00000F00000F00000F00000700000780040380040 1C00800C010007060001F80012157E9416>I<01FC000707000C03801C01C03801C07801 E07000E0F000E0FFFFE0F00000F00000F00000F00000F000007000007800203800201C00 400E008007030000FC0013157F9416>101 D<00007001F198071E180E0E181C07001C07 003C07803C07803C07803C07801C07001C07000E0E000F1C0019F0001000001000001800 001800001FFE000FFFC00FFFE03800F0600030400018C00018C00018C000186000306000 303800E00E038003FE0015217F9518>103 D<0E0000FE00001E00000E00000E00000E00 000E00000E00000E00000E00000E00000E00000E00000E00000E1F800E60C00E80E00F00 700F00700E00700E00700E00700E00700E00700E00700E00700E00700E00700E00700E00 700E00700E00700E00700E0070FFE7FF18237FA21B>I<1C001E003E001E001C00000000 000000000000000000000000000E00FE001E000E000E000E000E000E000E000E000E000E 000E000E000E000E000E000E000E000E00FFC00A227FA10E>I<0E00FE001E000E000E00 0E000E000E000E000E000E000E000E000E000E000E000E000E000E000E000E000E000E00 0E000E000E000E000E000E000E000E000E000E000E00FFE00B237FA20E>108 D<0E1FC07F00FE60E183801E807201C00F003C00E00F003C00E00E003800E00E003800E0 0E003800E00E003800E00E003800E00E003800E00E003800E00E003800E00E003800E00E 003800E00E003800E00E003800E00E003800E00E003800E00E003800E0FFE3FF8FFE2715 7F942A>I<0E1F80FE60C01E80E00F00700F00700E00700E00700E00700E00700E00700E 00700E00700E00700E00700E00700E00700E00700E00700E00700E0070FFE7FF18157F94 1B>I<0E3CFE461E8F0F0F0F060F000E000E000E000E000E000E000E000E000E000E000E 000E000E000F00FFF010157F9413>114 D<02000200020002000600060006000E001E00 3E00FFF80E000E000E000E000E000E000E000E000E000E000E000E040E040E040E040E04 0E040708030801F00E1F7F9E13>116 D<0E0070FE07F01E00F00E00700E00700E00700E 00700E00700E00700E00700E00700E00700E00700E00700E00700E00700E00F00E00F006 017003827800FC7F18157F941B>I119 D E /Fw 18 123 df<00001FE000800000FFFC01800007F00F0180000F80018380003E00 00C38000780000278000F00000178001E000000F8003C000000F80078000000780078000 0003800F00000003801F00000001801E00000001803E00000001803C00000001803C0000 0000807C00000000807C0000000080780000000000F80000000000F80000000000F80000 000000F80000000000F80000000000F80000000000F80000000000F80000000000F80000 000000F80000000000F800000FFFFC7800000FFFFC7C0000001FC07C0000000F803C0000 000F803C0000000F803E0000000F801E0000000F801F0000000F800F0000000F80078000 000F8007C000000F8003C000000F8001E000000F8000F000001780007C00001780003E00 006380000F8000C3800007F00781800000FFFE008000001FF000002E337CB134>71 D<7FFFFFFFFFE07FFFFFFFFFE07E000F8007E078000F8001E070000F8000E060000F8000 6040000F80002040000F800020C0000F800030C0000F80003080000F80001080000F8000 1080000F80001080000F80001080000F80001080000F80001000000F80000000000F8000 0000000F80000000000F80000000000F80000000000F80000000000F80000000000F8000 0000000F80000000000F80000000000F80000000000F80000000000F80000000000F8000 0000000F80000000000F80000000000F80000000000F80000000000F80000000000F8000 0000000F80000000000F80000000000F80000000000F80000000000F80000000000F8000 0000000F80000000000F80000000000F80000000000F80000000001FC00000000FFFFF80 00000FFFFF80002C317EB030>84 D<00FE00000303C0000C00E00010007000100038003C 003C003E001C003E001E003E001E0008001E0000001E0000001E0000001E00000FFE0000 FC1E0003E01E000F801E001F001E003E001E003C001E007C001E00F8001E04F8001E04F8 001E04F8003E04F8003E0478003E047C005E043E008F080F0307F003FC03E01E1F7D9E21 >97 D<003F8000E0600380180700040F00041E001E1C003E3C003E7C003E7C0008780000 F80000F80000F80000F80000F80000F80000F80000F80000F800007800007C00007C0000 3C00011E00011E00020F000207000403801800E060003F80181F7D9E1D>99 D<003F800000E0E0000380380007003C000E001E001E001E001C000F003C000F007C000F 0078000F8078000780F8000780F8000780FFFFFF80F8000000F8000000F8000000F80000 00F8000000F8000000780000007C0000003C0000003C0000801E0000800E0001000F0002 000780020001C00C0000F03000001FC000191F7E9E1D>101 D<0007E0001C1000383800 707C00E07C01E07C01C03803C00003C00003C00003C00003C00003C00003C00003C00003 C00003C00003C00003C000FFFFC0FFFFC003C00003C00003C00003C00003C00003C00003 C00003C00003C00003C00003C00003C00003C00003C00003C00003C00003C00003C00003 C00003C00003C00003C00003C00003C00003C00003C00007E0007FFF007FFF0016327FB1 14>I<07000F801F801F800F800700000000000000000000000000000000000000000000 000780FF80FF800F80078007800780078007800780078007800780078007800780078007 8007800780078007800780078007800780078007800FC0FFF8FFF80D307EAF12>105 D<0780FF80FF800F80078007800780078007800780078007800780078007800780078007 800780078007800780078007800780078007800780078007800780078007800780078007 80078007800780078007800780078007800780078007800FC0FFFCFFFC0E327EB112> 108 D<0780FE001FC000FF83078060F000FF8C03C18078000F9001E2003C0007A001E400 3C0007A000F4001E0007C000F8001E0007C000F8001E00078000F0001E00078000F0001E 00078000F0001E00078000F0001E00078000F0001E00078000F0001E00078000F0001E00 078000F0001E00078000F0001E00078000F0001E00078000F0001E00078000F0001E0007 8000F0001E00078000F0001E00078000F0001E00078000F0001E00078000F0001E000780 00F0001E00078000F0001E00078000F0001E000FC001F8003F00FFFC1FFF83FFF0FFFC1F FF83FFF0341F7E9E38>I<0780FE0000FF83078000FF8C03C0000F9001E00007A001E000 07A000F00007C000F00007C000F000078000F000078000F000078000F000078000F00007 8000F000078000F000078000F000078000F000078000F000078000F000078000F0000780 00F000078000F000078000F000078000F000078000F000078000F000078000F000078000 F000078000F0000FC001F800FFFC1FFF80FFFC1FFF80211F7E9E25>I<001FC00000F078 0001C01C00070007000F0007801E0003C01C0001C03C0001E03C0001E0780000F0780000 F0780000F0F80000F8F80000F8F80000F8F80000F8F80000F8F80000F8F80000F8F80000 F8780000F07C0001F03C0001E03C0001E01E0003C01E0003C00F00078007800F0001C01C 0000F07800001FC0001D1F7E9E21>I<0781FC00FF860700FF8803C00F9001E007A000F0 07C00078078000780780003C0780003C0780003E0780001E0780001F0780001F0780001F 0780001F0780001F0780001F0780001F0780001F0780001F0780003E0780003E0780003C 0780007C0780007807C000F007A000F007A001E00798038007860F000781F80007800000 078000000780000007800000078000000780000007800000078000000780000007800000 078000000FC00000FFFC0000FFFC0000202D7E9E25>I<0783E0FF8C18FF907C0F907C07 A07C07C03807C00007C00007C00007800007800007800007800007800007800007800007 80000780000780000780000780000780000780000780000780000780000780000780000F C000FFFE00FFFE00161F7E9E19>114 D<01FC100E03301800F0300070600030E00030E0 0010E00010E00010F00010F800007E00003FF0001FFF000FFFC003FFE0003FF00001F800 00F880003C80003C80001CC0001CC0001CE0001CE00018F00038F00030CC0060C301C080 FE00161F7E9E1A>I<00400000400000400000400000400000C00000C00000C00001C000 01C00003C00007C0000FC0001FFFE0FFFFE003C00003C00003C00003C00003C00003C000 03C00003C00003C00003C00003C00003C00003C00003C00003C00003C00003C01003C010 03C01003C01003C01003C01003C01003C01001C02001E02000E0400078C0001F00142C7F AB19>I<078000F000FF801FF000FF801FF0000F8001F000078000F000078000F0000780 00F000078000F000078000F000078000F000078000F000078000F000078000F000078000 F000078000F000078000F000078000F000078000F000078000F000078000F000078000F0 00078000F000078000F000078001F000078001F000078001F000038002F00003C004F000 01C008F800007030FF80001FC0FF80211F7E9E25>II<3FFFFF3E001E38001E30003C2000782000786000F04001E04001E04003C04007 80000780000F00001E00001E00003C0000780000780000F00101E00101E00103C0010780 010780030F00021E00021E00063C000678000E78007EFFFFFE181F7E9E1D>122 D E end %%EndProlog %%BeginSetup %%Feature: *Resolution 300dpi TeXDict begin %%PaperSize: A4 %%EndSetup %%Page: 1 1 1 0 bop 121 369 a Fw(T)-6 b(ermination)22 b(of)f(p)r(erm)n(utativ)n(e)g (con)n(v)n(ersions)g(in)h(in)n(tuitionistic)701 461 y(Gen)n(tzen)g (calculi)671 589 y Fv(Helm)o(ut)13 b(Sc)o(h)o(wic)o(h)o(ten)o(b)q(erg) 837 739 y Fu(Abstract)150 804 y Ft(It)h(is)i(sho)o(wn)f(that)g(p)q(erm) o(utativ)o(e)i(con)o(v)o(ersions)g(terminate)f(for)f(the)g(cut-free)g (in)o(tuitionisti)q(c)j(Gen)o(tzen)e(\(i.e.)92 850 y(sequen)o(t\))h (calculus;)j(this)d(pro)o(v)o(es)g(a)g(conjecture)g(b)o(y)f(Dyc)o (kho\013)i(and)f(Pin)o(to.)28 b(The)16 b(main)i(tec)o(hnical)g(to)q(ol) f(is)g(a)92 895 y(term)12 b(notation)i(for)f(deriv)n(ations)i(in)e(Gen) o(tzen)g(calculi.)19 b(These)13 b(terms)f(ma)o(y)h(b)q(e)g(seen)g(as)f Fs(\025)p Ft(-terms)h(with)g(explicit)92 941 y(substitution,)i(where)d (the)h(latter)g(corresp)q(onds)h(to)e(the)h(left)g(in)o(tro)q(duction)i (rules.)j Fr(Keywor)n(ds)s Ft(:)d(T)m(ermination)g(of)92 987 y(p)q(erm)o(utativ)o(e)g(con)o(v)o(ersions,)f(explicit)i (substitution,)f(sequen)o(t)f(term,)f(natural)h(deduction.)38 1070 y Fq(Pra)o(witz)e([7)o(])g(de\014nes)h(a)f(map)e Fp(F)17 b Fq(transforming)10 b(deriv)n(ations)i(in)f(the)i(in)o (tuitionistic)d(Gen)o(tzen)j(\(or)f(sequen)o(t\))h(calcu-)-12 1119 y(lus)e Fo(LJ)g Fq(in)o(to)f(natural)h(deductions)h(in)e Fo(NJ)p Fq(.)17 b(Moreo)o(v)o(er)12 b(he)g(\(essen)o(tially\))f(pro)o (v)o(ed)g(surjectivit)o(y)g(of)g Fp(F)16 b Fq(b)o(y)11 b(constructing)-12 1169 y(an)k(in)o(v)o(erse)h(map)d Fp(G)i Fq(from)e Fo(NJ)i Fq(bac)o(k)g(to)g Fo(LJ)o Fq(.)21 b(Ho)o(w)o(ard)15 b([3)o(])g(iden)o(ti\014ed)g(a)g(class)g(of)g (cut-free)h(sequen)o(t)g(deriv)n(ations)f({)-12 1219 y(to)e(b)q(e)g(called)f Fp(\031)q Fq(-normal)f(b)q(elo)o(w)h({)g (corresp)q(onding)i(to)e(normal)f(deriv)n(ation)g(terms)i(\(this)f(is)h (stated)g(without)g(pro)q(of)f(in)-12 1269 y([3)o(,)i(Theorem)f(2]\)) 283 1254 y Fn(1)301 1269 y Fq(.)18 b(A)c(n)o(um)o(b)q(er)e(of)h (authors)h(made)f(use)h(of)f(`p)q(erm)o(utativ)o(e)f(con)o(v)o (ersions')i(to)f(clarify)g(this)g(situation.)-12 1319 y(Zuc)o(k)o(er)g([9)o(])e(sho)o(w)o(ed)h(for)f(the)h(negativ)o(e)f (fragmen)o(t)f(of)h Fo(LJ)879 1300 y Fm(c)907 1319 y Fq(\(i.e.)g Fo(LJ)f Fq(with)i(cut\))g(that)f(t)o(w)o(o)g(deriv)n (ations)g(ha)o(v)o(e)g(the)h(same)-12 1369 y(v)n(alue)i(under)i Fp(F)k Fq(i\013)14 b(they)h(can)g(b)q(e)g(transformed)f(in)o(to)g(eac)o (h)h(other)g(b)o(y)f(means)g(of)g(p)q(erm)o(utativ)o(e)g(con)o(v)o (ersions)h(\(more)-12 1418 y(precisely:)k(p)q(erm)o(utativ)o(e)12 b(con)o(v)o(ersions)i(in)f(the)h(sense)h(of)d(Kleene)j([4)o(])e(and)g (in)f(addition)h(p)q(erm)o(utations)f(with)h(the)h(cut)-12 1468 y(rule\).)25 b(P)o(ottinger)16 b([6)o(])f(extended)j(Zuc)o(k)o (er's)e(results)h(to)f(form)o(ulas)e(with)h Fl(_)h Fq(and)f Fl(9)p Fq(.)24 b(Min)o(ts)16 b([5)o(])g(and)f(indep)q(enden)o(tly)-12 1518 y(Dyc)o(kho\013)h(and)f(Pin)o(to)h([1)o(])f(pro)o(v)o(e)h(a)g (similar)d(result)k(for)e(cut)i(free)f(calculi,)f(where)i(in)f(Dyc)o (kho\013)f(and)h(Pin)o(to)f([1)o(])h(the)-12 1568 y(orien)o(tation)f (of)h(p)q(erm)o(utativ)o(e)f(con)o(v)o(ersions)h(is)g(tak)o(en)g(in)o (to)f(accoun)o(t)i(and)e(con\015uence)j(is)e(pro)o(v)o(en.)24 b(Here)17 b(w)o(e)f(pro)o(v)o(e)-12 1618 y(termination)e(of)i(some)f(v) o(ersions)h(of)f(the)i(p)q(erm)o(utativ)o(e)e(con)o(v)o(ersion)h (rules;)h(a)f(w)o(eak)o(er)g(form)e(of)i(one)g(of)f(our)h(results)-12 1667 y(w)o(as)e(conjectured)i(in)d([1)o(].)38 1726 y(F)m(or)k (simplicit)o(y)d(w)o(e)j(restrict)h(atten)o(tion)f(to)g(the)g(negativ)o (e)g(fragmen)o(t)f(of)g(in)o(tuitionistic)g(logic)f(\(i.e.)h(of)h (minim)o(al)-12 1775 y(logic,)e(since)h(no)f(sym)o(b)q(ol)f Fl(?)h Fq(for)g(falsit)o(y)f(is)i(presen)o(t\);)h(ho)o(w)o(ev)o(er,)f (the)g(argumen)o(ts)f(b)q(elo)o(w)g(can)h(b)q(e)g(extended)h(to)f(the) -12 1825 y(full)d(language)g(with)g Fl(_)p Fp(;)7 b Fl(9)13 b Fq(\(thanks)i(to)e(Matthias)h(H\177)-21 b(olzl)13 b(who)h(has)g(c)o (hec)o(k)o(ed)h(this\).)38 1883 y(I)d(w)o(ould)e(lik)o(e)h(to)h(thank)f (Ro)o(y)g(Dyc)o(kho\013)g(for)g(making)f([1)o(])h(a)o(v)n(ailable)e(to) j(me)e(and)i(patien)o(tly)f(explaining)f(its)i(results.)-12 1933 y(Moreo)o(v)o(er,)19 b(Ro)o(y)e(Dyc)o(kho\013)h(and)g(Luis)f(Pin)o (to)h(pro)o(vided)g(useful)g(commen)o(ts)e(on)i(an)f(earlier)h(draft.) 30 b(The)19 b(presen)o(t)-12 1983 y(pap)q(er)c(w)o(ould)e(not)h(ha)o(v) o(e)f(b)q(een)i(p)q(ossible)g(without)e(this)h(in)o(teraction.)k (Thanks)c(are)h(also)e(due)h(to)g(J\177)-21 b(org)14 b(Hudelmaier,)-12 2033 y(Grigori)f(Min)o(ts,)g(Anne)i(T)m(ro)q(elstra)f (and)f(three)j(anon)o(ymous)c(referees)k(for)d(further)i(helpful)e (commen)o(ts.)-12 2178 y Fk(1)67 b(Deriv)l(ations)24 b(as)d(sequen)n(t)i(terms)-12 2277 y Fq(Cut-free)c(deriv)n(ations)f(in) f(the)i(negativ)o(e)f(fragmen)o(t)e(of)i Fo(LJ)f Fq(are)i(denoted)g(b)o (y)e Fj(se)n(quent)j(terms)s Fq(;)f(the)g(di\013erence)g(to)-12 2327 y Fp(\025)p Fq(-terms)f(and)f(hence)i(to)f(deriv)n(ation)f(terms)g (in)g(natural)h(deduction)g(is)f(that)h(a)g(form)e(of)h Fj(explicit)h(substitution)i Fq(is)-12 2377 y(allo)o(w)o(ed.)25 b(An)16 b(inductiv)o(e)h(de\014nition)f(of)g(sequen)o(t)i(terms)e(is)g (displa)o(y)o(ed)g(in)g(table)h(1.)25 b(T)o(yp)q(e)17 b(\(i.e.)f(form)o(ula\))e(indices)-12 2427 y(will)i(b)q(e)i(omitted)f (whenev)o(er)i(p)q(ossible.)29 b(W)m(e)17 b(use)i Fp(L;)7 b(M)r(;)g(N)r(;)g(K)20 b Fq(for)d(sequen)o(t)i(terms)e(and)h Fp(u;)7 b(v)q(;)g(w)17 b Fq(for)h(assumption)-12 2477 y(v)n(ariables.)38 2535 y(An)o(y)d(sequen)o(t)i(term)e Fp(L)h Fq(has)g(a)f Fj(typ)n(e)s Fq(,)h(whic)o(h)f(is)h(view)o(ed)f(as) h(usual)f(as)h(the)g(deriv)o(ed)g(form)o(ula.)21 b(The)16 b Fj(c)n(ontext)k Fq(of)15 b(a)-12 2585 y(sequen)o(t)g(term)f Fp(L)g Fq(is)f(the)i(set)g(\000)c(:=)h(F)-5 b(A\()p Fp(L)p Fq(\))15 b(of)e(free)h(\(t)o(yp)q(ed\))h(assumption)e(v)n(ariables)g (of)g Fp(L)p Fq(,)h(de\014ned)h(b)o(y)599 2676 y(F)-5 b(A)q(\()p Fp(u)p Fq(\))41 b(:=)h Fl(f)p Fp(u)p Fl(g)p Fp(;)499 2738 y Fq(F)-5 b(A)q(\()p Fl(h)p Fp(L;)7 b(M)e Fl(i)p Fq(\))41 b(:=)h(F)-5 b(A\()p Fp(L)p Fq(\))10 b Fl([)f Fq(F)-5 b(A)q(\()p Fp(M)5 b Fq(\))p Fp(;)468 2801 y Fq(F)-5 b(A)q(\()p Fp(L)566 2807 y Fm(u)588 2801 y Fl(f)p Fp(w)q(;)7 b(i)p Fl(g)o Fq(\))41 b(:=)h(\(F)-5 b(A)q(\()p Fp(L)p Fq(\))9 b Fl(n)g(f)p Fp(u)p Fl(g)p Fq(\))g Fl([)g(f)p Fp(w)q Fl(g)p Fp(;)p -12 2837 747 2 v 34 2864 a Fi(1)52 2876 y Fh(More)f(recen)o(tly)m(,)f(Herb)q(elin)g ([2])i(in)o(tro)q(duced)c(still)j(another)f(sequen)o(t)g(calculus)g (LJT)i(corresp)q(onding)c(one-to-one)h(with)j(normal)d(deriv)n(a-)-12 2915 y(tion)11 b(terms)f(\(cf.)h(also)f(T)m(ro)q(elstra)h([8)o(,)h (Prop)q(osition)d(2.2]\).)14 b(Herb)q(elin)c(pro)o(v)o(es)g (termination)e(of)j(cut-eliminat)o(ion)d(for)j(LJT.)911 3042 y Fq(1)p eop %%Page: 2 2 2 1 bop 547 195 a Fq(F)-5 b(A\()p Fp(\025uL)p Fq(\))42 b(:=)g(F)-5 b(A\()p Fp(L)p Fq(\))10 b Fl(n)f(f)p Fp(u)p Fl(g)p Fp(;)451 257 y Fq(F)-5 b(A)q(\()p Fp(M)561 263 y Fm(u)583 257 y Fl(f)p Fp(v)q(;)7 b(L)p Fl(g)p Fq(\))41 b(:=)h(\(F)-5 b(A)q(\()p Fp(M)5 b Fq(\))k Fl(n)g(f)p Fp(u)p Fl(g)p Fq(\))g Fl([)f(f)p Fp(v)q Fl(g)i([)f Fq(F)-5 b(A\()p Fp(L)p Fq(\))p Fp(;)547 320 y Fq(F)g(A\()p Fp(\025xL)p Fq(\))42 b(:=)g(F)-5 b(A\()p Fp(L)p Fq(\))p Fp(;)477 382 y Fq(F)g(A\()p Fp(L)574 388 y Fm(u)596 382 y Fl(f)p Fp(v)q(;)7 b(t)p Fl(g)p Fq(\))41 b(:=)h(\(F)-5 b(A)q(\()p Fp(L)p Fq(\))9 b Fl(n)g(f)p Fp(u)p Fl(g)p Fq(\))g Fl([)g(f)p Fp(v)q Fl(g)p Fp(:)-12 467 y Fq(The)15 b(v)n(ariable)d(condition)h(of)h (course)h(is)f Fp(x)i(=)-26 b Fl(2)11 b Fq(FV)q(\()p Fp(A)p Fq(\))j(for)g(all)e Fp(u)983 452 y Fm(A)1022 467 y Fl(2)f Fq(\000)g(:=)h(F)-5 b(A\()p Fp(L)p Fq(\).)38 524 y(So)14 b(a)g(con)o(text)g(\000)g(is)g(a)g(set)h Fl(f)p Fp(u)505 530 y Fn(1)523 524 y Fq(:)7 b Fp(A)573 530 y Fn(1)591 524 y Fp(;)g(:)g(:)g(:)e(;)i(u)708 530 y Fm(n)730 524 y Fq(:)g Fp(A)780 530 y Fm(n)802 524 y Fl(g)14 b Fq(with)g(distinct)g Fp(u)1106 530 y Fm(i)1120 524 y Fq(.)k(Sequen)o(t)d(terms)f(ma)o(y)e(b)q(e)j(view)o(ed)f(as)g (trees,)-12 574 y(where)k(eac)o(h)f(no)q(de)g(is)g(lab)q(elled)f(with)h (a)f(sequen)o(t)i(of)e(the)h(form)e(\000)i Fl(\))e Fp(A)p Fq(,)i(with)g(\000)f(:=)g(F)-5 b(A)q(\()p Fp(L)p Fq(\))17 b(the)g(con)o(text)h(and)e Fp(A)-12 623 y Fq(the)f(t)o(yp)q(e)g(of)f Fp(L)p Fq(.)19 b(The)c(notation)e(\000[)p Fp(u)p Fq(:)7 b Fp(A)p Fq(])13 b(in)g(rule)i Fl(!)o Fq(R)f Fp(u)g Fq(means)g(that)g (the)h(con)o(text)g(ma)o(y)d(or)i(ma)o(y)f(not)h(con)o(tain)g(the)-12 673 y(assumption)f Fp(u)p Fq(:)7 b Fp(A)p Fq(.)38 730 y(It)13 b(can)g(happ)q(en)g(that)f(a)h(sequen)o(t)h(is)e(deriv)n(able)g (in)h(more)e(than)i(one)g(w)o(a)o(y)m(.)j(F)m(or)c(instance,)i Fp(C)h Fq(can)e(b)q(e)g(deriv)o(ed)g(from)-12 780 y Fp(u)12 786 y Fn(1)31 780 y Fq(:)7 b Fp(A;)g(u)124 786 y Fn(2)141 780 y Fq(:)g Fp(A)k Fl(!)g Fp(B)r(;)c(u)331 786 y Fn(3)350 780 y Fq(:)g Fp(A)k Fl(!)g Fp(B)j Fl(!)d Fp(C)16 b Fq(b)o(y)e Fp(u)690 786 y Fm(u)711 780 y Fl(f)p Fp(w)q(;)7 b(v)q Fl(g)824 792 y Fm(w)851 780 y Fl(f)p Fp(u)896 786 y Fn(3)914 780 y Fp(;)g(u)957 786 y Fn(1)975 780 y Fl(g)995 794 y Fm(v)1015 780 y Fl(f)p Fp(u)1060 786 y Fn(2)1078 780 y Fp(;)g(u)1121 786 y Fn(1)1139 780 y Fl(g)p Fq(,)13 b(i.e.)g(b)o(y)422 964 y Fp(u)446 970 y Fn(1)464 964 y Fq(:)7 b Fp(A)k Fl(\))g Fp(A)703 909 y(u)727 915 y Fn(1)745 909 y Fq(:)c Fp(A)k Fl(\))g Fp(A)984 862 y(v)q Fq(:)c Fp(B)14 b Fl(\))d Fp(B)96 b(u)p Fq(:)7 b Fp(C)13 b Fl(\))e Fp(C)p 967 872 471 2 v 1019 909 a(w)q Fq(:)c Fp(B)13 b Fl(!)e Fp(C)q(;)c(v)q Fq(:)g Fp(B)13 b Fl(\))e Fp(C)p 686 927 717 2 v 752 964 a(u)776 970 y Fn(3)794 964 y Fq(:)c Fp(A)k Fl(!)g Fp(B)j Fl(!)e Fp(C)q(;)7 b(u)1081 970 y Fn(1)1098 964 y Fq(:)g Fp(A;)g(v)q Fq(:)g Fp(B)13 b Fl(\))e Fp(C)p 405 982 948 2 v 527 1018 a(u)551 1024 y Fn(2)570 1018 y Fq(:)c Fp(A)k Fl(!)g Fp(B)r(;)c(u)760 1024 y Fn(1)778 1018 y Fq(:)g Fp(A;)g(u)871 1024 y Fn(3)889 1018 y Fq(:)g Fp(A)k Fl(!)g Fp(B)j Fl(!)d Fp(C)j Fl(\))d Fp(C)-12 1097 y Fq(and)j(also)f(b)o(y)h Fp(u)234 1103 y Fm(u)255 1097 y Fl(f)p Fp(w)q(;)7 b(v)346 1103 y Fm(v)365 1097 y Fl(f)p Fp(u)410 1103 y Fn(2)428 1097 y Fp(;)g(u)471 1103 y Fn(1)489 1097 y Fl(gg)531 1109 y Fm(w)558 1097 y Fl(f)p Fp(u)603 1103 y Fn(3)621 1097 y Fp(;)g(u)664 1103 y Fn(1)681 1097 y Fl(g)p Fq(,)14 b(i.e.)422 1285 y Fp(u)446 1291 y Fn(1)464 1285 y Fq(:)7 b Fp(A)k Fl(\))g Fp(A)703 1177 y(u)727 1183 y Fn(1)745 1177 y Fq(:)c Fp(A)k Fl(\))g Fp(A)94 b(v)q Fq(:)7 b Fp(B)14 b Fl(\))d Fp(B)p 686 1193 486 2 v 730 1230 a(u)754 1236 y Fn(2)772 1230 y Fq(:)c Fp(A)k Fl(!)g Fp(B)r(;)c(u)962 1236 y Fn(1)981 1230 y Fq(:)g Fp(A)k Fl(\))g Fp(B)123 b(u)p Fq(:)7 b Fp(C)13 b Fl(\))e Fp(C)p 713 1248 725 2 v 778 1285 a(w)q Fq(:)c Fp(B)14 b Fl(!)d Fp(C)q(;)c(u)1000 1291 y Fn(2)1017 1285 y Fq(:)g Fp(A)k Fl(!)g Fp(B)r(;)c(u)1207 1291 y Fn(1)1225 1285 y Fq(:)g Fp(A)k Fl(\))h Fp(C)p 405 1303 984 2 v 546 1339 a(u)570 1345 y Fn(3)589 1339 y Fq(:)7 b Fp(A)k Fl(!)g Fp(B)j Fl(!)d Fp(C)q(;)c(u)875 1345 y Fn(1)892 1339 y Fq(:)g Fp(A;)g(u)985 1345 y Fn(2)1003 1339 y Fq(:)g Fp(A)k Fl(!)g Fp(B)j Fl(\))d Fp(C)-12 1462 y Fk(2)67 b(Multiary)25 b(normal)e(forms)-12 1560 y Fq(It)14 b(will)d(b)q(e)j(useful)f(to)h(allo)o(w)d(a)i(form)f(of)g(m)o(ultiary)f (application)h(for)h(sequen)o(t)h(terms.)k(E.g.)12 b Fp(M)1470 1566 y Fm(u)1492 1560 y Fl(f)p Fp(v)q(;)7 b(L)1581 1566 y Fn(1)1600 1560 y Fp(L)1628 1566 y Fn(2)1647 1560 y Fl(g)13 b Fq(should)g(b)q(e)-12 1609 y(essen)o(tially)d(the)h(same)f (deriv)n(ation)f(as)i Fp(M)631 1615 y Fm(u)653 1609 y Fl(f)p Fp(w)q(;)c(L)752 1615 y Fn(2)770 1609 y Fl(g)790 1622 y Fm(w)817 1609 y Fl(f)p Fp(v)q(;)g(L)906 1615 y Fn(1)925 1609 y Fl(g)j Fq(with)g(a)g(new)h(assumption)e(v)n(ariable)g Fp(w)q Fq(.)17 b(More)11 b(generally)-12 1659 y(w)o(e)h(w)o(an)o(t)g (to)g(allo)o(w)e(a)i(m)o(ultiary)e(application)g(of)i Fl(!)o Fq(L)g(and)g(denote)h(it)e(b)o(y)h(the)h(sequen)o(t)g(term)f Fp(M)1500 1665 y Fm(u)1522 1659 y Fl(f)p Fp(v)q(;)7 b(L)1611 1665 y Fn(1)1636 1659 y Fp(:)g(:)g(:)e(L)1719 1665 y Fm(n)1742 1659 y Fl(g)p Fq(;)12 b(this)-12 1709 y(corresp)q(onds)k(to)e (the)g(deriv)n(ation)519 1790 y Fl(j)25 b Fp(L)584 1796 y Fn(1)433 1850 y Fq(\000)459 1856 y Fn(1)489 1850 y Fl(\))11 b Fp(A)573 1856 y Fn(1)640 1850 y Fp(:)c(:)g(:)822 1790 y Fl(j)25 b Fp(L)887 1796 y Fm(n)782 1850 y Fq(\000)808 1856 y Fm(n)842 1850 y Fl(\))11 b Fp(A)926 1856 y Fm(n)1117 1788 y Fl(j)25 b Fp(M)1042 1850 y Fq([)p Fp(u)p Fq(:)7 b Fp(B)r Fq(]\001)j Fl(\))h Fp(C)p 417 1870 873 2 v 1302 1885 a Fl(!)o Fq(L)1369 1867 y Fg(\003)1402 1885 y Fp(u)495 1907 y(v)q Fq(:)c Fp(A)566 1913 y Fn(1)596 1907 y Fl(!)12 b Fp(:)7 b(:)g(:)e(A)736 1913 y Fm(n)770 1907 y Fl(!)11 b Fp(B)r(;)c Fq(\000)901 1913 y Fn(1)920 1907 y Fp(;)g(:)g(:)g(:)e(;)i Fq(\000)1039 1913 y Fm(n)1061 1907 y Fp(;)g Fq(\001)j Fl(\))h Fp(C)-12 1986 y Fq(W)m(e)j(also)f(w)o(an)o(t)g(to)h(allo)o(w)e (a)i(m)o(ultiary)d(application)i(of)g(the)i(rules)f Fl(!)p Fq(L)f(and)h Fl(^)p Fq(L)g(as)g(in)f Fp(M)1407 1992 y Fm(u)1429 1986 y Fl(f)p Fp(v)q(;)7 b(L)1518 1992 y Fn(1)1537 1986 y Fq(1)p Fp(L)1586 1992 y Fn(2)1604 1986 y Fl(g)p Fq(,)13 b(i.e.)g(in)528 2069 y Fl(j)25 b Fp(L)593 2075 y Fn(1)491 2129 y Fq(\000)517 2135 y Fn(1)547 2129 y Fl(\))11 b Fp(A)631 2135 y Fn(1)780 2069 y Fl(j)25 b Fp(L)845 2075 y Fn(2)743 2129 y Fq(\000)769 2135 y Fn(2)799 2129 y Fl(\))11 b Fp(A)883 2135 y Fn(2)1069 2066 y Fl(j)25 b Fp(M)995 2129 y Fq([)p Fp(u)p Fq(:)7 b Fp(B)r Fq(]\001)j Fl(\))h Fp(C)p 474 2149 769 2 v 1254 2163 a Fl(^!)p Fq(L)1350 2147 y Fg(\003)512 2189 y Fp(v)q Fq(:)c Fp(A)583 2195 y Fn(1)613 2189 y Fl(!)k Fp(D)g Fl(^)e Fq(\()p Fp(A)795 2195 y Fn(2)825 2189 y Fl(!)i Fp(B)r Fq(\))p Fp(;)c Fq(\000)972 2195 y Fn(1)991 2189 y Fp(;)g Fq(\000)1036 2195 y Fn(2)1054 2189 y Fp(;)g Fq(\001)j Fl(\))i Fp(C)-12 2269 y Fq(Also)i Fl(8)p Fq(L)g(can)g(b)q(e)g(included:)k(the)d(sequen)o(t)g(term)e Fp(M)820 2275 y Fm(u)842 2269 y Fl(f)p Fp(v)q(;)7 b(L)931 2275 y Fn(1)950 2269 y Fp(tL)993 2275 y Fn(2)1012 2269 y Fq(1)p Fp(s)p Fl(g)14 b Fq(corresp)q(onds)i(to)410 2353 y Fl(j)25 b Fp(L)475 2359 y Fn(1)372 2413 y Fq(\000)398 2419 y Fn(1)428 2413 y Fl(\))11 b Fp(A)512 2419 y Fn(1)707 2350 y Fl(j)25 b Fp(L)772 2356 y Fn(2)624 2413 y Fq(\000)650 2419 y Fn(2)680 2413 y Fl(\))11 b Fq(\()p Fp(A)780 2419 y Fn(2)799 2413 y Fq(\))815 2419 y Fm(x)836 2413 y Fq([)p Fp(t)p Fq(])1103 2350 y Fl(j)25 b Fp(M)968 2413 y Fq([)p Fp(u)p Fq(:)7 b Fp(B)1054 2419 y Fm(x;y)1101 2413 y Fq([)p Fp(t;)g(s)p Fq(])o(]\001)k Fl(\))g Fp(C)p 355 2434 982 2 v 1350 2448 a Fl(^)o(!8)p Fq(L)1468 2433 y Fg(\003)454 2474 y Fp(v)q Fq(:)c Fp(A)525 2480 y Fn(1)556 2474 y Fl(!)k(8)p Fp(x)p Fq(\()p Fp(A)703 2480 y Fn(2)733 2474 y Fl(!)g Fp(D)g Fl(^)e(8)p Fp(y)q(B)r Fq(\))p Fp(;)e Fq(\000)1006 2480 y Fn(1)1025 2474 y Fp(;)g Fq(\000)1070 2480 y Fn(2)1088 2474 y Fp(;)g Fq(\001)k Fl(\))g Fp(C)-12 2553 y Fq(It)j(should)g(b)q(e)h(clear)g(no)o(w)e(what)i(is)f(mean)o(t)f (b)o(y)g(a)h Fj(multiary)h(se)n(quent)g(term)s Fq(.)k(More)14 b(precisely)m(,)h(sim)o(ultaneously)d(with)-12 2602 y(the)h(inductiv)o (e)f(de\014nition)g(of)g(m)o(ultiary)d(sequen)o(t)14 b(terms)e(w)o(e)g(ha)o(v)o(e)g(to)g(de\014ne)h(the)g(notion)f(of)f(a)h Fj(p)n(ath)1582 2592 y Fp(~)1581 2602 y(L)g Fq(for)g(a)g(form)o(ula)-12 2652 y Fp(A)19 b Fq(leading)g(to)g(\(the)h(instance\))g Fp(B)i Fq(of)c Fp(A)p Fq(;)691 2642 y Fp(~)689 2652 y(L)h Fq(will)f(b)q(e)i(a)f(list)f(consisting)i(of)e(m)o(ultiary)f(sequen)o (t)k(terms,)e(0)p Fp(;)7 b Fq(1)18 b(\(for)-12 2702 y(pro)r(jections\)) d(and)f(ob)r(ject)g(terms.)k(The)d(clauses)f(are)50 2787 y Fl(\017)21 b Fq(F)m(or)13 b(ev)o(ery)i Fp(A)p Fq(,)f(the)g(empt)o(y)f (list)g(is)h(a)g(path)g(for)f Fp(A)h Fq(leading)f(to)h(the)g(instance)h Fp(A)f Fq(of)f Fp(A)p Fq(.)50 2868 y Fl(\017)21 b Fq(If)13 b Fp(L)161 2852 y Fm(A)202 2868 y Fq(is)g(a)h(m)o(ultiary)d(sequen)o(t) k(term)e(and)777 2857 y Fp(~)775 2868 y(L)h Fq(is)f(a)g(path)h(for)f Fp(B)j Fq(leading)d(to)g(the)h(instance)h Fp(C)h Fq(of)d Fp(B)r Fq(,)h(then)g Fp(L)1799 2852 y Fm(A)1828 2857 y Fp(~)1826 2868 y(L)92 2917 y Fq(is)g(a)f(path)h(for)g Fp(A)d Fl(!)g Fp(B)17 b Fq(leading)c(to)h(the)g(instance)h Fp(C)h Fq(of)d Fp(A)f Fl(!)f Fp(B)r Fq(.)911 3042 y(2)p eop %%Page: 3 3 3 2 bop -11 155 1864 2 v -12 205 2 50 v 1146 205 V 1852 205 V -12 255 V 473 240 a Fq(Deriv)n(ation)p 1146 255 V 788 w(T)m(erm)p 1852 255 V -12 305 V 1146 305 V 1852 305 V -11 306 1864 2 v -12 356 2 50 v 1146 356 V 1852 356 V -12 406 V 484 391 a Fp(u)p Fq(:)7 b Fp(A)j Fl(\))h Fp(A)p 1146 406 V 823 w(u)1499 376 y Fm(A)p 1852 406 V -12 456 V 1146 456 V 1852 456 V -11 458 1864 2 v -12 507 2 50 v 1146 507 V 1852 507 V -12 645 2 138 v 394 538 a Fl(j)g Fp(L)359 598 y Fq(\000)g Fl(\))g Fp(A)606 538 y Fl(j)g Fp(M)574 598 y Fq(\001)g Fl(\))g Fp(B)p 342 608 381 2 v 736 621 a Fl(^)p Fq(R)415 645 y(\000\001)g Fl(\))g Fp(A)e Fl(^)g Fp(B)p 1146 645 2 138 v 1389 567 a(L)1417 552 y Fm(A)1538 567 y Fp(M)1583 552 y Fm(B)p 1356 577 289 2 v 1372 620 a Fl(h)p Fp(L)1416 605 y Fm(A)1444 620 y Fp(;)e(M)1508 605 y Fm(B)1536 620 y Fl(i)1552 605 y Fm(A)p Fg(^)p Fm(B)p 1852 645 2 138 v -12 694 2 50 v 1146 694 V 1852 694 V -11 696 1864 2 v -12 746 2 50 v 1146 746 V 1852 746 V -12 912 2 167 v 156 777 a Fl(j)k Fp(L)72 839 y Fq([)p Fp(u)p Fq(:)c Fp(A)p Fq(]\000)j Fl(\))h Fp(C)p 14 860 335 2 v 362 869 a Fl(^)p Fq(L)415 875 y Fn(0)448 869 y Fp(u;)c(w)31 904 y(w)q Fq(:)g Fp(A)h Fl(^)h Fp(B)r(;)e Fq(\000)12 b Fl(\))f Fp(C)746 777 y Fl(j)g Fp(L)661 839 y Fq([)p Fp(v)q Fq(:)c Fp(B)r Fq(]\000)k Fl(\))g Fp(C)p 604 860 V 951 869 a Fl(^)p Fq(L)1005 875 y Fn(1)1037 869 y Fp(v)q(;)c(w)620 904 y(w)q Fq(:)g Fp(A)i Fl(^)g Fp(B)r(;)e Fq(\000)k Fl(\))g Fp(C)p 1146 912 2 167 v 1291 816 a(L)1319 801 y Fm(C)p 1172 826 295 2 v 1188 869 a Fp(L)1216 854 y Fm(C)1216 883 y(u)1236 875 y Ff(A)1262 869 y Fl(f)p Fp(w)1314 854 y Fm(A)p Fg(^)p Fm(B)1389 869 y Fp(;)c Fq(0)p Fl(g)1640 816 y Fp(L)1668 801 y Fm(C)p 1521 826 294 2 v 1538 869 a Fp(L)1566 854 y Fm(C)1566 883 y(v)1584 875 y Ff(B)1610 869 y Fl(f)p Fp(w)1662 854 y Fm(A)p Fg(^)p Fm(B)1738 869 y Fp(;)g Fq(1)p Fl(g)p 1852 912 2 167 v -12 962 2 50 v 1146 962 V 1852 962 V -11 964 1864 2 v -12 1014 2 50 v 1146 1014 V 1852 1014 V -12 1164 2 151 v 474 1045 a(j)k Fp(L)390 1107 y Fq(\000[)p Fp(u)p Fq(:)c Fp(A)p Fq(])j Fl(\))h Fp(B)p 373 1127 254 2 v 639 1141 a Fl(!)p Fq(R)i Fp(u)390 1164 y Fq(\000)f Fl(\))f Fp(A)g Fl(!)g Fp(B)p 1146 1164 2 151 v 1465 1080 a(L)1493 1065 y Fm(B)p 1351 1090 284 2 v 1368 1133 a Fq(\()p Fp(\025u)1432 1118 y Fm(A)1459 1133 y Fp(L)1487 1118 y Fm(B)1516 1133 y Fq(\))1532 1118 y Fm(A)p Fg(!)p Fm(B)p 1852 1164 2 151 v -12 1214 2 50 v 1146 1214 V 1852 1214 V -11 1216 1864 2 v -12 1265 2 50 v 1146 1265 V 1852 1265 V -12 1432 2 167 v 302 1299 a Fl(j)g Fp(L)267 1359 y Fq(\000)g Fl(\))g Fp(A)563 1297 y Fl(j)g Fp(M)481 1359 y Fq([)p Fp(u)p Fq(:)c Fp(B)r Fq(]\001)j Fl(\))h Fp(C)p 250 1379 479 2 v 741 1388 a Fl(!)p Fq(L)i Fp(u;)7 b(v)307 1424 y(v)q Fq(:)g Fp(A)12 b Fl(!)f Fp(B)r(;)c Fq(\000)p Fp(;)g Fq(\001)k Fl(\))g Fp(C)p 1146 1432 2 167 v 1389 1336 a(L)1417 1320 y Fm(A)1538 1336 y Fp(M)1583 1320 y Fm(C)p 1328 1345 344 2 v 1345 1389 a Fp(M)1390 1374 y Fm(C)1385 1403 y(u)1405 1394 y Ff(B)1432 1389 y Fl(f)p Fp(v)1474 1374 y Fm(A)p Fg(!)p Fm(B)1561 1389 y Fp(;)c(L)1608 1374 y Fm(A)1634 1389 y Fl(g)p 1852 1432 2 167 v -12 1482 2 50 v 1146 1482 V 1852 1482 V -11 1483 1864 2 v -12 1533 2 50 v 1146 1533 V 1852 1533 V -12 1671 2 138 v 341 1564 a(j)k Fp(L)306 1624 y Fq(\000)h Fl(\))f Fp(A)p 266 1634 202 2 v 480 1647 a Fl(8)p Fq(R)j Fp(x)283 1671 y Fq(\000)d Fl(\))g(8)p Fp(xA)641 1615 y Fq(if)i Fp(x)i(=)-25 b Fl(2)11 b Fq(FV)q(\(\000\))p 1146 1671 2 138 v 1285 1593 a Fp(L)1313 1578 y Fm(A)p 1196 1603 234 2 v 1212 1646 a Fq(\()p Fp(\025xL)1304 1631 y Fm(A)1332 1646 y Fq(\))1348 1631 y Fg(8)p Fm(xA)1498 1615 y Fq(\(with)j(v)n(ar.)f(cond.\))p 1852 1671 2 138 v -12 1721 2 50 v 1146 1721 V 1852 1721 V -11 1722 1864 2 v -12 1772 2 50 v 1146 1772 V 1852 1772 V -12 1939 2 168 v 449 1803 a Fl(j)e Fp(L)335 1866 y Fq([)p Fp(u)p Fq(:)c Fp(A)421 1872 y Fm(x)441 1866 y Fq([)p Fp(t)p Fq(])o(]\000)k Fl(\))g Fp(B)p 319 1886 313 2 v 644 1896 a Fl(8)p Fq(L)i Fp(u;)7 b(v)q(;)g(t)345 1931 y(v)q Fq(:)g Fl(8)p Fp(xA;)g Fq(\000)k Fl(\))g Fp(B)p 1146 1939 2 168 v 1465 1842 a(L)1493 1827 y Fm(B)p 1336 1852 315 2 v 1352 1896 a Fp(L)1380 1881 y Fm(B)1380 1911 y(u)1400 1903 y Ff(A)1422 1907 y(x)1440 1903 y Fe([)p Ff(t)p Fe(])1473 1896 y Fl(f)p Fp(v)1515 1881 y Fg(8)p Fm(xA)1580 1896 y Fp(;)c(t)p Fl(g)p 1852 1939 2 168 v -12 1989 2 50 v 1146 1989 V 1852 1989 V -11 1991 1864 2 v 686 2107 a Fq(T)m(able)13 b(1:)18 b(Gen)o(tzen)d(calculus)50 2223 y Fl(\017)21 b Fq(If)16 b Fp(t)g Fq(is)g(an)g(ob)r(ject)h(term)e(and) 585 2212 y Fp(~)583 2223 y(L)i Fq(is)f(a)g(path)g(for)g Fp(A)905 2229 y Fm(x)926 2223 y Fq([)p Fp(t)p Fq(])f(leading)g(to)h (the)h(instance)g Fp(B)h Fq(of)e Fp(A)1546 2229 y Fm(x)1567 2223 y Fq([)p Fp(t)p Fq(])o(,)g(then)h Fp(t)1747 2212 y(~)1745 2223 y(L)g Fq(is)f(a)92 2273 y(path)e(for)f Fl(8)p Fp(xA)h Fq(leading)f(to)h(the)g(instance)h Fp(B)h Fq(of)e Fl(8)p Fp(xA)p Fq(.)50 2351 y Fl(\017)21 b Fq(If)135 2341 y Fp(~)133 2351 y(L)14 b Fq(is)g(a)f(path)g(for)h Fp(A)442 2357 y Fm(i)469 2351 y Fq(leading)f(to)g(the)i(instance)f Fp(B)i Fq(of)d Fp(A)1020 2357 y Fm(i)1034 2351 y Fq(,)g(then)i Fp(i)1170 2341 y(~)1168 2351 y(L)f Fq(is)f(a)g(path)h(for)f Fp(A)1476 2357 y Fn(0)1504 2351 y Fl(^)8 b Fp(A)1571 2357 y Fn(1)1603 2351 y Fq(leading)13 b(to)h(the)92 2401 y(instance)h Fp(B)h Fq(of)d Fp(A)379 2407 y Fn(0)407 2401 y Fl(^)c Fp(A)475 2407 y Fn(1)494 2401 y Fq(.)-12 2482 y(F)m(or)18 b(example,)g Fp(L)275 2463 y Fm(A)300 2467 y Fe(1)275 2493 y Fn(1)318 2482 y Fp(tL)361 2460 y Fn(\()p Fm(A)399 2464 y Fe(2)416 2460 y Fn(\))429 2464 y Ff(x)447 2460 y Fn([)p Fm(t)p Fn(])361 2493 y(2)481 2482 y Fq(1)p Fp(s)g Fq(is)g(a)g(path)h(for)f Fp(A)h Fq(:=)f Fp(A)937 2488 y Fn(1)975 2482 y Fl(!)g(8)p Fp(x)p Fq(\()p Fp(A)1129 2488 y Fn(2)1167 2482 y Fl(!)h Fp(D)13 b Fl(^)f(8)p Fp(y)q(B)r Fq(\))20 b(leading)d(to)i(the)g(instance)-12 2532 y Fp(B)19 2538 y Fm(x;y)68 2532 y Fq([)p Fp(t;)7 b(s)p Fq(])13 b(of)g Fp(A)p Fq(.)18 b({)c(Then)g(in)g(the)g(inductiv)o (e)g(de\014nition)g(of)f(m)o(ultiary)f(sequen)o(t)j(terms)e(w)o(e)h(ha) o(v)o(e)g(a)g(single)f(L-clause)50 2619 y Fl(\017)21 b Fq(If)135 2608 y Fp(~)133 2619 y(L)14 b Fq(is)f(a)g(non)h(empt)o(y)e (path)i(for)f Fp(A)g Fq(leading)g(to)g(the)h(instance)h Fp(B)h Fq(of)d Fp(A)p Fq(,)g(and)g Fp(M)18 b Fq(is)c(a)f(m)o(ultiary)e (sequen)o(t)k(term)92 2669 y(of)e(t)o(yp)q(e)i Fp(C)s Fq(,)e(then)861 2718 y Fp(M)901 2727 y Fm(u)921 2718 y Ff(B)5 b Fl(f)p Fp(v)990 2701 y Fm(A)1017 2718 y Fp(;)1038 2708 y(~)1036 2718 y(L)p Fl(g)92 2787 y Fq(is)14 b(a)f(m)o(ultiary)f (sequen)o(t)j(term)e(of)g(t)o(yp)q(e)i Fp(C)s Fq(.)38 2868 y(W)m(e)f(no)o(w)f(w)o(an)o(t)h(to)g(explain)f(precisely)i(ho)o(w) e(a)h(m)o(ultiary)d(sequen)o(t)16 b(term)d(can)h(b)q(e)h(view)o(ed)f (as)g(an)g(abbreviation)f(of)-12 2917 y(an)h(ordinary)f(\(or)h (`binary'\))f(sequen)o(t)i(term.)911 3042 y(3)p eop %%Page: 4 4 4 3 bop -12 195 a Fo(2.1.)20 b Fd(Definition.)28 b Fq(F)m(or)11 b(m)o(ultiary)e(sequen)o(t)k(terms)e(w)o(e)h(de\014ne)h(an)e Fj(abbr)n(eviation)i(c)n(onversion)i Fp(\026)d Fq(\()p Fp(\026)f Fq(for)g(`m)o(ultiary'\))-12 245 y(b)o(y)435 295 y Fp(N)468 301 y Fm(w)495 295 y Fl(f)p Fp(u;)571 284 y(~)559 295 y(M)t Fl(g)624 307 y Fm(u)646 295 y Fl(f)p Fp(v)q(;)708 284 y(~)707 295 y(L)p Fl(g)g(7!)809 301 y Fm(\026)842 295 y Fp(N)875 301 y Fm(w)902 295 y Fl(f)p Fp(v)q(;)965 284 y(~)963 295 y(L)1004 284 y(~)992 295 y(M)t Fl(g)42 b Fq(if)13 b Fp(u)j(=)-26 b Fl(2)11 b Fq(F)-5 b(A)q(\()p Fp(N)r(;)1347 284 y(~)1335 295 y(M)5 b Fq(\).)-12 367 y(The)15 b Fj(term)f(closur)n(e)i Fl(\000)-6 b(!)382 373 y Fm(\026)417 367 y Fq(of)14 b(this)g(con)o(v)o(ersion)g(is)f (de\014ned)i(inductiv)o(ely)f(b)o(y)50 455 y Fl(\017)21 b Fq(If)13 b Fp(M)k Fl(7!)232 461 y Fm(\026)265 455 y Fp(M)310 440 y Fg(0)322 455 y Fq(,)c(then)h Fp(M)j Fl(\000)-7 b(!)565 461 y Fm(\026)598 455 y Fp(M)643 440 y Fg(0)669 455 y Fq(\()p Fj(he)n(ad)15 b(c)n(onversion)s Fq(\).)50 537 y Fl(\017)21 b Fq(If)13 b Fp(M)k Fl(\000)-7 b(!)257 543 y Fm(\026)290 537 y Fp(M)335 522 y Fg(0)347 537 y Fq(,)13 b(then)i(also)630 631 y Fp(M)670 637 y Fm(u)692 631 y Fl(f)p Fp(v)q(;)755 621 y(~)753 631 y(L)p Fl(g)42 b(\000)-7 b(!)911 637 y Fm(\026)974 631 y Fp(M)1019 614 y Fg(0)1014 641 y Fm(u)1036 631 y Fl(f)p Fp(v)q(;)1099 621 y(~)1097 631 y(L)p Fl(g)p Fp(;)543 700 y(L)571 706 y Fm(u)593 700 y Fl(f)p Fp(v)q(;)666 689 y(~)654 700 y(M)5 b(M)752 689 y(~)744 700 y(N)t Fl(g)42 b(\000)-7 b(!)911 706 y Fm(\026)974 700 y Fp(L)1002 706 y Fm(u)1024 700 y Fl(f)p Fp(v)q(;)1097 689 y(~)1085 700 y(M)5 b(M)1175 683 y Fg(0)1195 689 y Fp(~)1186 700 y(N)g Fl(g)p Fp(;)671 762 y Fl(h)p Fp(M)r(;)i(N)e Fl(i)42 b(\000)-7 b(!)911 768 y Fm(\026)974 762 y Fl(h)p Fp(M)1035 745 y Fg(0)1047 762 y Fp(;)7 b(N)e Fl(i)p Fp(;)671 824 y Fl(h)p Fp(N)r(;)i(M)e Fl(i)42 b(\000)-7 b(!)911 830 y Fm(\026)974 824 y Fl(h)p Fp(N)r(;)7 b(M)1089 807 y Fg(0)1101 824 y Fl(i)p Fp(;)712 887 y(\025z)r(M)47 b Fl(\000)-7 b(!)911 893 y Fm(\026)974 887 y Fp(\025z)r(M)1064 869 y Fg(0)1118 887 y Fq(with)13 b Fp(z)h Fl(2)d(f)p Fp(u;)c(x)p Fl(g)o Fp(:)92 1037 y Fq(These)15 b(reductions)g(are)f(called)g Fj(inner)h(r)n(e)n(ductions)s Fq(.)38 1125 y(F)m(or)g(example,)f(the)i(sequen)o(t)h(term)e Fp(u)640 1131 y Fm(u)662 1125 y Fl(f)p Fp(w)q(;)7 b(v)q Fl(g)774 1137 y Fm(w)801 1125 y Fl(f)p Fp(u)846 1131 y Fn(3)864 1125 y Fp(;)g(u)907 1131 y Fn(1)925 1125 y Fl(g)946 1139 y Fm(v)965 1125 y Fl(f)p Fp(u)1010 1131 y Fn(2)1029 1125 y Fp(;)g(u)1072 1131 y Fn(1)1089 1125 y Fl(g)16 b Fq(considered)h(ab)q(o)o(v)o(e)e(can)h(b)q(e)g(reduced)h (in)e(one)-12 1174 y Fl(\000)-6 b(!)56 1180 y Fm(\026)77 1174 y Fq(-step)15 b(to)f Fp(u)254 1180 y Fm(u)275 1174 y Fl(f)p Fp(u)320 1180 y Fn(3)338 1174 y Fp(;)7 b(u)381 1180 y Fn(1)399 1174 y Fp(v)q Fl(g)442 1187 y Fm(v)461 1174 y Fl(f)p Fp(u)506 1180 y Fn(2)524 1174 y Fp(;)g(u)567 1180 y Fn(1)585 1174 y Fl(g)p Fq(,)13 b(corresp)q(onding)i(to)422 1311 y Fp(u)446 1317 y Fn(1)464 1311 y Fq(:)7 b Fp(A)k Fl(\))g Fp(A)703 1257 y(u)727 1263 y Fn(1)745 1257 y Fq(:)c Fp(A)k Fl(\))g Fp(A)94 b(v)q Fq(:)7 b Fp(B)14 b Fl(\))d Fp(B)96 b(u)p Fq(:)7 b Fp(C)13 b Fl(\))e Fp(C)p 686 1274 752 2 v 769 1310 a(u)793 1316 y Fn(3)812 1310 y Fq(:)c Fp(A)k Fl(!)g Fp(B)j Fl(!)d Fp(C)q(;)c(u)1098 1316 y Fn(1)1115 1310 y Fq(:)g Fp(A;)g(v)q Fq(:)g Fp(B)13 b Fl(\))e Fp(C)p 405 1328 966 2 v 536 1365 a(u)560 1371 y Fn(2)579 1365 y Fq(:)c Fp(A)k Fl(!)g Fp(B)r(;)c(u)769 1371 y Fn(1)787 1365 y Fq(:)g Fp(A;)g(u)880 1371 y Fn(3)898 1365 y Fq(:)g Fp(A)k Fl(!)g Fp(B)j Fl(!)d Fp(C)j Fl(\))d Fp(C)-12 1446 y Fq(Similarly)18 b(the)k(second)g(sequen)o(t)h(term)e Fp(u)681 1452 y Fm(u)702 1446 y Fl(f)p Fp(w)q(;)7 b(v)793 1452 y Fm(v)812 1446 y Fl(f)p Fp(u)857 1452 y Fn(2)875 1446 y Fp(;)g(u)918 1452 y Fn(1)936 1446 y Fl(gg)978 1459 y Fm(w)1004 1446 y Fl(f)p Fp(u)1049 1452 y Fn(3)1068 1446 y Fp(;)g(u)1111 1452 y Fn(1)1128 1446 y Fl(g)21 b Fq(can)h(b)q(e)g(reduced)h(in)e(one)g Fl(\000)-6 b(!)1687 1452 y Fm(\026)1708 1446 y Fq(-step)22 b(to)-12 1496 y Fp(u)12 1502 y Fm(u)34 1496 y Fl(f)p Fp(u)79 1502 y Fn(3)97 1496 y Fp(;)7 b(u)140 1502 y Fn(1)158 1496 y Fp(v)178 1502 y Fm(v)197 1496 y Fl(f)p Fp(u)242 1502 y Fn(2)261 1496 y Fp(;)g(u)304 1502 y Fn(1)321 1496 y Fl(gg)p Fq(:)422 1630 y Fp(u)446 1636 y Fn(1)464 1630 y Fq(:)g Fp(A)k Fl(\))g Fp(A)703 1577 y(u)727 1583 y Fn(1)745 1577 y Fq(:)c Fp(A)k Fl(\))g Fp(A)94 b(v)q Fq(:)7 b Fp(B)14 b Fl(\))d Fp(B)p 686 1593 486 2 v 730 1630 a(u)754 1636 y Fn(2)772 1630 y Fq(:)c Fp(A)k Fl(!)g Fp(B)r(;)c(u)962 1636 y Fn(1)981 1630 y Fq(:)g Fp(A)k Fl(\))g Fp(B)123 b(u)p Fq(:)7 b Fp(C)13 b Fl(\))e Fp(C)p 405 1648 1033 2 v 571 1685 a(u)595 1691 y Fn(3)613 1685 y Fq(:)c Fp(A)k Fl(!)g Fp(B)j Fl(!)d Fp(C)q(;)c(u)899 1691 y Fn(1)917 1685 y Fq(:)g Fp(A;)g(u)1010 1691 y Fn(2)1027 1685 y Fq(:)g Fp(A)k Fl(!)g Fp(B)j Fl(\))d Fp(C)38 1772 y Fq(Clearly)i Fl(\000)-6 b(!)250 1778 y Fm(\026)285 1772 y Fq(is)14 b(terminating,)d(since)k(the)g(n)o(um)o(b)q(er)e(of)g(braces)i(go)q(es) f(do)o(wn.)k(Lo)q(cal)13 b(con\015uence)j(of)d Fl(\000)-6 b(!)1708 1778 y Fm(\026)1743 1772 y Fq(is)14 b(also)-12 1821 y(easy)h(to)e(see;)i(in)e(the)i(o)o(v)o(erlap)e(case)i(w)o(e)f(ha) o(v)o(e)681 1914 y Fp(N)714 1920 y Fm(w)741 1914 y Fl(f)p Fp(u;)816 1904 y(~)805 1914 y(M)t Fl(g)870 1927 y Fm(u)891 1914 y Fl(f)p Fp(v)q(;)954 1904 y(~)952 1914 y(L)p Fl(g)1001 1929 y Fm(v)1021 1914 y Fl(f)p Fp(u)1066 1920 y Fn(1)1084 1914 y Fp(;)1110 1904 y(~)1103 1914 y(K)s Fl(g)705 1973 y Fc(\000)664 2014 y(\000)657 2021 y(\000)-42 b(\011)1096 1973 y(@)1137 2014 y(@)1144 2021 y(@)g(R)283 2065 y Fp(N)316 2071 y Fm(w)344 2065 y Fl(f)p Fp(u;)419 2054 y(~)408 2065 y(M)s Fl(g)472 2077 y Fm(u)494 2065 y Fl(f)p Fp(u)539 2071 y Fn(1)557 2065 y Fp(;)583 2054 y(~)576 2065 y(K)615 2054 y(~)614 2065 y(L)p Fl(g)657 2122 y Fc(@)699 2164 y(@)705 2170 y(@)g(R)1182 2065 y Fp(N)1215 2071 y Fm(w)1242 2065 y Fl(f)p Fp(v)q(;)1305 2054 y(~)1303 2065 y(L)1344 2054 y(~)1331 2065 y(M)5 b Fl(g)1397 2077 y Fm(v)1417 2065 y Fl(f)p Fp(u)1462 2071 y Fn(1)1480 2065 y Fp(;)1506 2054 y(~)1499 2065 y(K)r Fl(g)1144 2122 y Fc(\000)1102 2164 y(\000)1096 2170 y(\000)-42 b(\011)784 2215 y Fp(N)817 2221 y Fm(w)845 2215 y Fl(f)p Fp(u)890 2221 y Fn(1)908 2215 y Fp(;)934 2205 y(~)927 2215 y(K)966 2205 y(~)964 2215 y(L)1005 2205 y(~)993 2215 y(M)t Fl(g)-12 2318 y Fq(Hence)20 b(ev)o(ery)f(m)o(ultiary)c(sequen)o(t)20 b(term)d(has)i(a)f(uniquely)f(determined)h Fp(\026)p Fj(-normal)h(form)h Fq(to)e(b)q(e)h(called)f Fj(multiary)-12 2368 y(normal)d(form)s Fq(.)i(Sequen)o(t)e(terms)f(in)f(m)o(ultiary)f (normal)g(form)g(are)i(c)o(haracterized)i(b)o(y)614 2456 y Fp(L)c Fq(::=)e Fp(u)i Fl(j)f(h)p Fp(L;)c(M)e Fl(i)11 b(j)g Fp(\025z)r(L)h Fl(j)f Fp(M)1085 2462 y Fm(u)1107 2456 y Fl(f)p Fp(v)q(;)1170 2445 y(~)1168 2456 y(L)p Fl(g)p Fp(;)-12 2549 y Fq(with)k Fp(z)i Fl(2)d(f)p Fp(u;)7 b(x)p Fl(g)p Fq(,)13 b(where)k(in)e(the)h(last)g(case)g Fp(M)k Fq(is)c(not)f(of)g(the)h(form)e Fp(N)1145 2555 y Fm(w)1172 2549 y Fl(f)p Fp(u;)1247 2538 y(~)1236 2549 y(M)t Fl(g)h Fq(with)g Fp(u)k(=)-26 b Fl(2)14 b Fq(F)-5 b(A)q(\()p Fp(N)r(;)1628 2538 y(~)1616 2549 y(M)5 b Fq(\))15 b(\(for)h(then)-12 2603 y Fp(N)21 2609 y Fm(w)48 2603 y Fl(f)p Fp(u;)124 2593 y(~)112 2603 y(M)t Fl(g)177 2616 y Fm(u)199 2603 y Fl(f)p Fp(v)q(;)261 2593 y(~)260 2603 y(L)p Fl(g)c Fq(could)h(b)q(e)g(further)h(abbreviated)f(b)o(y)f Fp(N)940 2609 y Fm(w)968 2603 y Fl(f)p Fp(v)q(;)1030 2593 y(~)1029 2603 y(L)1069 2593 y(~)1057 2603 y(M)t Fl(g)p Fq(\).)18 b(Recall)12 b(that)h(the)g(list)1521 2593 y Fp(~)1519 2603 y(L)g Fq(ma)o(y)e(con)o(tain)h(0)p Fp(;)7 b Fq(1)-12 2653 y(\(for)17 b(pro)r(jections\))h(as)f(w)o(ell)f (as)h(ob)r(ject)h(terms.)27 b(Also)17 b(in)f(case)i Fp(\025xL)f Fq(the)h(v)n(ariable)e(condition)g Fp(x)21 b(=)-26 b Fl(2)17 b Fq(FV)q(\()p Fp(A)p Fq(\))g(for)g(all)-12 2703 y Fp(u)12 2688 y Fm(A)51 2703 y Fl(2)11 b Fq(F)-5 b(A\()p Fp(L)p Fq(\))15 b(m)o(ust)e(hold.)38 2760 y(F)m(or)j(instance,)h Fp(u)315 2766 y Fm(u)336 2760 y Fl(f)p Fp(u)381 2766 y Fn(3)400 2760 y Fp(;)7 b(u)443 2766 y Fn(1)460 2760 y Fp(v)q Fl(g)503 2773 y Fm(v)522 2760 y Fl(f)p Fp(u)567 2766 y Fn(2)586 2760 y Fp(;)g(u)629 2766 y Fn(1)646 2760 y Fl(g)16 b Fq(is)g(the)h(m)o(ultiary)d(normal)g(form)h(of)g Fp(u)1289 2766 y Fm(u)1311 2760 y Fl(f)p Fp(w)q(;)7 b(v)q Fl(g)1423 2773 y Fm(w)1450 2760 y Fl(f)p Fp(u)1495 2766 y Fn(3)1513 2760 y Fp(;)g(u)1556 2766 y Fn(1)1574 2760 y Fl(g)1595 2775 y Fm(v)1614 2760 y Fl(f)p Fp(u)1659 2766 y Fn(2)1678 2760 y Fp(;)g(u)1721 2766 y Fn(1)1738 2760 y Fl(g)p Fq(,)16 b(and)-12 2810 y Fp(u)12 2816 y Fm(u)34 2810 y Fl(f)p Fp(u)79 2816 y Fn(3)97 2810 y Fp(;)7 b(u)140 2816 y Fn(1)158 2810 y Fp(v)178 2816 y Fm(v)197 2810 y Fl(f)p Fp(u)242 2816 y Fn(2)261 2810 y Fp(;)g(u)304 2816 y Fn(1)321 2810 y Fl(gg)14 b Fq(is)g(the)g(m)o(ultiary)d(normal)h (form)g(of)i Fp(u)969 2816 y Fm(u)990 2810 y Fl(f)p Fp(w)q(;)7 b(v)1081 2816 y Fm(v)1100 2810 y Fl(f)p Fp(u)1145 2816 y Fn(2)1163 2810 y Fp(;)g(u)1206 2816 y Fn(1)1224 2810 y Fl(gg)1266 2823 y Fm(w)1292 2810 y Fl(f)p Fp(u)1337 2816 y Fn(3)1356 2810 y Fp(;)g(u)1399 2816 y Fn(1)1416 2810 y Fl(g)p Fq(.)38 2868 y(The)17 b(m)o(ultiary)d(normal)g(form)g Fp(\026)p Fq(\()p Fp(L)p Fq(\))j(of)f(a)g(sequen)o(t)h(term)f Fp(L)g Fq(can)h(also)e(b)q(e)i(de\014ned)h(recursiv)o(ely)m(.)25 b(Moreo)o(v)o(er)17 b(w)o(e)-12 2917 y(de\014ne)e(a)f(kind)f(of)g(con)o (v)o(erse)j Fp(\027)g Fq(of)d Fp(\026)p Fq(,)g(turning)h(a)g(m)o (ultiary)d(sequen)o(t)k(term)e(in)o(to)h(a)f(binary)h(one.)911 3042 y(4)p eop %%Page: 5 5 5 4 bop -12 195 a Fo(2.2.)21 b Fd(Definition.)27 b Fq(1.)18 b(F)m(or)c(ev)o(ery)g(m)o(ultiary)e(sequen)o(t)j(term)e Fp(L)h Fq(w)o(e)g(de\014ne)h Fp(\026)p Fq(\()p Fp(L)p Fq(\))g(b)o(y)322 286 y Fp(\026)p Fq(\()p Fp(u)p Fq(\))41 b(:=)h Fp(u;)222 349 y(\026)p Fq(\()p Fl(h)p Fp(L;)7 b(M)e Fl(i)p Fq(\))41 b(:=)h Fl(h)p Fp(\026)p Fq(\()p Fp(L)p Fq(\))p Fp(;)7 b(\026)p Fq(\()p Fp(M)e Fq(\))p Fl(i)p Fp(;)272 411 y(\026)p Fq(\()p Fp(\025z)r(L)p Fq(\))42 b(:=)g Fp(\025z)r(\026)p Fq(\()p Fp(L)p Fq(\))g(with)14 b Fp(z)f Fl(2)f(f)p Fp(u;)7 b(x)p Fl(g)n Fp(;)174 501 y(\026)p Fq(\()p Fp(M)255 507 y Fm(u)277 501 y Fl(f)p Fp(v)q(;)340 490 y(~)338 501 y(L)p Fl(g)p Fq(\))41 b(:=)530 442 y Fb(\032)568 478 y Fp(N)601 484 y Fm(w)628 478 y Fl(f)p Fp(v)q(;)7 b(\026)p Fq(\()732 468 y Fp(~)730 478 y(L)p Fq(\))787 468 y Fp(~)774 478 y(M)e Fl(g)60 b Fq(if)13 b Fp(\026)p Fq(\()p Fp(M)5 b Fq(\))12 b(=)g Fp(N)1129 484 y Fm(w)1156 478 y Fl(f)p Fp(u;)1231 468 y(~)1220 478 y(M)t Fl(g)h Fq(with)h Fp(u)i(=)-26 b Fl(2)11 b Fq(F)-5 b(A)q(\()p Fp(N)r(;)1603 468 y(~)1591 478 y(M)5 b Fq(\),)568 533 y Fp(\026)p Fq(\()p Fp(M)g Fq(\))670 539 y Fm(u)692 533 y Fl(f)p Fp(v)q(;)i(\026)p Fq(\()796 522 y Fp(~)794 533 y(L)p Fq(\))p Fl(g)41 b Fq(otherwise.)38 628 y(2.)18 b(F)m(or)13 b(ev)o(ery)i(m)o(ultiary)c(sequen)o(t)k(term)f Fp(N)k Fq(w)o(e)d(de\014ne)g(a)e(binary)h(sequen)o(t)h(term)e Fp(\027)s Fq(\()p Fp(N)5 b Fq(\))13 b(b)o(y)404 720 y Fp(\027)s Fq(\()p Fp(u)p Fq(\))40 b(:=)i Fp(u;)296 782 y(\027)s Fq(\()p Fl(h)p Fp(M)r(;)7 b(N)e Fl(i)p Fq(\))41 b(:=)h Fl(h)p Fp(\027)s Fq(\()p Fp(M)5 b Fq(\))p Fp(;)i(\027)s Fq(\()p Fp(N)e Fq(\))p Fl(i)p Fp(;)344 844 y(\027)s Fq(\()p Fp(\025z)r(N)g Fq(\))41 b(:=)h Fp(\025z)r(\027)s Fq(\()p Fp(N)5 b Fq(\))41 b(with)13 b Fp(z)h Fl(2)d(f)p Fp(u;)c(x)p Fl(g)o Fp(;)213 934 y(\027)s Fq(\()p Fp(N)286 940 y Fm(w)312 934 y Fl(f)p Fp(v)q(;)g(L)413 924 y(~)401 934 y(M)e Fl(g)p Fq(\))41 b(:=)610 876 y Fb(\032)648 911 y Fp(\027)s Fq(\()p Fp(N)5 b Fq(\))742 917 y Fm(w)768 911 y Fl(f)p Fp(v)q(;)i(\027)s Fq(\()p Fp(L)p Fq(\))p Fl(g)432 b Fq(if)1416 901 y Fp(~)1404 911 y(M)18 b Fq(is)c(empt)o(y)m(,)648 966 y Fp(\027)s Fq(\()p Fp(N)721 972 y Fm(w)747 966 y Fl(f)p Fp(u;)822 955 y(~)811 966 y(M)t Fl(g)p Fq(\))892 972 y Fm(u)914 966 y Fl(f)p Fp(v)q(;)7 b(\027)s Fq(\()p Fp(L)p Fq(\))p Fl(g)40 b Fq(with)14 b Fp(u)g Fq(new)42 b(otherwise.)38 1061 y(Clearly)13 b Fp(\026)p Fq(\()p Fp(L)p Fq(\))i(is)e(the)i (uniquely)e(determined)h(m)o(ultiary)e(normal)f(form)i(of)g Fp(L)p Fq(.)-12 1178 y Fo(2.3.)21 b Fd(Lemma.)28 b Fa(F)m(or)13 b(ev)o(ery)i(binary)f(sequen)o(t)h(term)e Fp(L)h Fa(w)o(e)g(ha)o(v)o(e) g Fp(\027)s Fq(\()p Fp(\026)p Fq(\()p Fp(L)p Fq(\)\))d(=)h Fp(L)p Fa(.)-12 1265 y Fd(Pr)o(oof)p Fq(.)18 b(Induction)9 b(on)g Fp(L)p Fq(.)17 b(W)m(e)9 b(only)f(consider)j(the)e(case)i Fp(M)941 1271 y Fm(u)963 1265 y Fl(f)p Fp(v)q(;)c(L)p Fl(g)i Fq(with)g Fp(\026)p Fq(\()p Fp(M)c Fq(\))12 b(=)f Fp(N)1362 1271 y Fm(w)1390 1265 y Fl(f)p Fp(u;)1465 1255 y(~)1454 1265 y(M)s Fl(g)p Fq(.)17 b(If)9 b Fp(u)15 b(=)-25 b Fl(2)11 b Fq(F)-5 b(A)q(\()p Fp(N)r(;)1794 1255 y(~)1782 1265 y(M)5 b Fq(\),)-12 1315 y(then)156 1407 y Fp(\027)s Fq(\()p Fp(\026)p Fq(\()p Fp(M)277 1413 y Fm(u)298 1407 y Fl(f)p Fp(v)q(;)i(L)p Fl(g)p Fq(\)\))42 b(=)f Fp(\027)s Fq(\()p Fp(N)628 1413 y Fm(w)655 1407 y Fl(f)p Fp(v)q(;)7 b(\026)p Fq(\()p Fp(L)p Fq(\))814 1396 y Fp(~)801 1407 y(M)e Fl(g)p Fq(\))482 1474 y(=)41 b Fp(\027)s Fq(\()p Fp(N)628 1480 y Fm(w)655 1474 y Fl(f)p Fp(u;)730 1463 y(~)719 1474 y(M)t Fl(g)p Fq(\))800 1480 y Fm(u)821 1474 y Fl(f)p Fp(v)q(;)7 b(\027)s Fq(\()p Fp(\026)p Fq(\()p Fp(L)p Fq(\)\))p Fl(g)41 b Fq(wlog)13 b(with)h Fp(u)p Fq(,)f(since)i Fp(u)h(=)-26 b Fl(2)11 b Fq(F)-5 b(A)q(\()p Fp(N)r(;)1638 1463 y(~)1626 1474 y(M)5 b Fq(\))482 1536 y(=)41 b Fp(\027)s Fq(\()p Fp(\026)p Fq(\()p Fp(M)5 b Fq(\)\))713 1542 y Fm(u)735 1536 y Fl(f)p Fp(v)q(;)i(\027)s Fq(\()p Fp(\026)p Fq(\()p Fp(L)p Fq(\)\))p Fl(g)482 1598 y Fq(=)41 b Fp(M)595 1604 y Fm(u)617 1598 y Fl(f)p Fp(v)q(;)7 b(L)p Fl(g)42 b Fq(b)o(y)13 b(ind.)g(h)o(yp.)-12 1694 y(In)h(case)h Fp(u)c Fl(2)g Fq(F)-5 b(A)q(\()p Fp(N)r(;)339 1684 y(~)326 1694 y(M)5 b Fq(\))14 b(w)o(e)g(ha)o(v)o(e)230 1802 y Fp(\027)s Fq(\()p Fp(\026)p Fq(\()p Fp(M)351 1808 y Fm(u)373 1802 y Fl(f)p Fp(v)q(;)7 b(L)p Fl(g)o Fq(\)\))12 b(=)g Fp(\027)s Fq(\()p Fp(\026)p Fq(\()p Fp(M)5 b Fq(\))712 1808 y Fm(u)733 1802 y Fl(f)p Fp(v)q(;)i(\026)p Fq(\()p Fp(L)p Fq(\))p Fl(g)p Fq(\))12 b(=)g Fp(\027)s Fq(\()p Fp(\026)p Fq(\()p Fp(M)5 b Fq(\)\))1130 1808 y Fm(u)1151 1802 y Fl(f)p Fp(v)q(;)i(\027)s Fq(\()p Fp(\026)p Fq(\()p Fp(L)p Fq(\)\))p Fl(g)k Fq(=)h Fp(M)1469 1808 y Fm(u)1491 1802 y Fl(f)p Fp(v)q(;)7 b(L)p Fl(g)p Fp(:)157 b Fd(Qed)38 1960 y Fq(In)14 b(what)g(follo)o(ws)e(w)o(e)i(shall)f(simply)f(sp)q (eak)j(of)e(sequen)o(t)i(terms)f(when)g(w)o(e)g(mean)f(m)o(ultiary)e (sequen)o(t)k(terms.)38 2018 y(No)o(w)f(recall)g(the)g(usual)g (inductiv)o(e)g(de\014nition)f(of)h(deriv)n(ation)f(terms,)g(as)h (displa)o(y)o(ed)f(in)h(table)g(2.3.)j(The)d(\(actual\))-12 2068 y(substitution)20 b(of)f(a)g(deriv)n(ation)g(term)f Fp(N)661 2053 y Fm(A)708 2068 y Fq(for)h(an)g(assumption)f(v)n(ariable) h Fp(u)1251 2053 y Fm(A)1297 2068 y Fq(in)g(the)h(deriv)n(ation)f(term) g Fp(M)1779 2053 y Fm(B)1826 2068 y Fq(is)-12 2118 y(denoted)d(b)o(y)e Fp(M)244 2124 y Fm(u)266 2118 y Fq([)p Fp(N)5 b Fq(])o(.)21 b(Recall)14 b(also)g(that)h(normal)e(deriv)n(ation)h(terms)g(\(w.r.t.)g Fp(\014)r Fq(-con)o(v)o(ersion)i(\()p Fp(\025xM)5 b Fq(\))p Fp(N)18 b Fl(7!)12 b Fp(M)1756 2124 y Fm(x)1777 2118 y Fq([)p Fp(N)5 b Fq(])o(\))-12 2168 y(are)14 b(c)o(haracterized)i(b)o (y)680 2218 y Fp(M)g Fq(::=)11 b Fp(u)839 2207 y(~)827 2218 y(M)16 b Fl(j)c(h)p Fp(M)r(;)7 b(N)e Fl(i)11 b(j)g Fp(\025z)r(M)-12 2292 y Fq(with)j Fp(z)f Fl(2)f(f)p Fp(u;)7 b(x)p Fl(g)p Fq(,)k(where)k(in)f(case)h Fp(\025xM)j Fq(the)d(ob)o (vious)e(v)n(ariable)g(condition)g(m)o(ust)g(hold.)38 2350 y(The)20 b(w)o(ell)g(kno)o(wn)f(equiv)n(alence)i(of)e(the)i (cut-free)g(Gen)o(tzen)g(calculus)f(with)g(normal)e(deriv)n(ations)h (in)h(natural)-12 2400 y(deduction)15 b(can)f(b)q(e)g(written)h(quite)f (explicitly)e(with)i(the)g(presen)o(t)i(notation;)d(this)g(will)g(b)q (e)h(useful)g(b)q(elo)o(w.)-12 2516 y Fo(2.4.)25 b Fd(Definition.)j Fq(1.)21 b(F)m(or)14 b(ev)o(ery)i(sequen)o(t)g(term)f Fp(L)g Fq(w)o(e)g(de\014ne)i(a)d(deriv)n(ation)g(term)h Fp(F)6 b Fq(\()p Fp(L)p Fq(\))15 b(\()p Fp(F)20 b Fq(for)15 b(`functional'\))-12 2566 y(b)o(y)652 2657 y Fp(F)6 b Fq(\()p Fp(u)p Fq(\))41 b(:=)g Fp(u;)551 2720 y(F)6 b Fq(\()p Fl(h)p Fp(L;)h(M)e Fl(i)p Fq(\))42 b(:=)f Fl(h)p Fp(F)6 b Fq(\()p Fp(L)p Fq(\))p Fp(;)h(F)f Fq(\()p Fp(M)f Fq(\))p Fl(i)p Fp(;)602 2782 y(F)h Fq(\()p Fp(\025z)r(L)p Fq(\))42 b(:=)f Fp(\025z)r(F)6 b Fq(\()p Fp(L)p Fq(\))42 b(with)13 b Fp(z)h Fl(2)d(f)p Fp(u;)c(x)p Fl(g)o Fp(;)503 2849 y(F)f Fq(\()p Fp(M)592 2855 y Fm(u)614 2849 y Fl(f)p Fp(v)q(;)677 2839 y(~)675 2849 y(L)p Fl(g)p Fq(\))42 b(:=)f Fp(F)6 b Fq(\()p Fp(M)f Fq(\))977 2855 y Fm(u)998 2849 y Fq([)p Fp(v)q(F)h Fq(\()1082 2839 y Fp(~)1080 2849 y(L)p Fq(\)])p Fp(:)911 3042 y Fq(5)p eop %%Page: 6 6 6 5 bop 166 155 1511 2 v 165 205 2 50 v 1028 205 V 1675 205 V 165 255 V 503 240 a Fq(Deriv)n(ation)p 1028 255 V 611 w(T)m(erm)p 1675 255 V 165 305 V 1028 305 V 1675 305 V 166 306 1511 2 v 165 356 2 50 v 1028 356 V 1675 356 V 165 406 V 561 391 a Fp(u)p Fq(:)7 b Fp(A)p 1028 406 V 692 w(u)1351 376 y Fm(A)p 1675 406 V 165 456 V 1028 456 V 1675 456 V 166 458 1511 2 v 165 507 2 50 v 1028 507 V 1675 507 V 165 645 2 138 v 468 538 a Fl(j)k Fp(M)466 598 y(A)671 538 y Fl(j)g Fp(M)667 598 y(B)p 449 608 269 2 v 730 624 a Fl(^)758 609 y Fn(+)528 645 y Fp(A)e Fl(^)g Fp(B)p 1028 645 2 138 v 1237 567 a(M)1282 552 y Fm(A)1402 567 y Fp(N)1440 552 y Fm(B)p 1203 577 299 2 v 1220 620 a Fl(h)p Fp(M)1281 605 y Fm(A)1308 620 y Fp(;)e(N)1365 605 y Fm(B)1393 620 y Fl(i)1409 605 y Fm(A)p Fg(^)p Fm(B)p 1675 645 2 138 v 165 694 2 50 v 1028 694 V 1675 694 V 166 696 1511 2 v 165 746 2 50 v 1028 746 V 1675 746 V 165 894 2 149 v 396 777 a Fl(j)k Fp(M)353 836 y(A)f Fl(^)f Fp(B)p 337 846 145 2 v 493 858 a Fl(^)521 840 y Fg(\000)521 869 y Fn(0)393 894 y Fp(A)691 777 y Fl(j)i Fp(M)649 836 y(A)e Fl(^)g Fp(B)p 632 846 V 789 858 a Fl(^)817 840 y Fg(\000)817 869 y Fn(1)687 894 y Fp(B)p 1028 894 2 149 v 1178 811 a(M)1223 796 y Fm(A)p Fg(^)p Fm(B)p 1159 821 159 2 v 1176 864 a Fq(\()p Fp(M)c Fq(0\))1274 849 y Fm(A)1392 811 y Fp(M)1437 796 y Fm(A)p Fg(^)p Fm(B)p 1373 821 160 2 v 1389 864 a Fq(\()p Fp(M)g Fq(1\))1487 849 y Fm(B)p 1675 894 2 149 v 165 944 2 50 v 1028 944 V 1675 944 V 166 946 1511 2 v 165 995 2 50 v 1028 995 V 1675 995 V 165 1133 2 138 v 504 1027 a Fl(j)11 b Fp(M)501 1086 y(B)p 436 1096 163 2 v 611 1113 a Fl(!)653 1098 y Fn(+)694 1113 y Fp(u)718 1098 y Fm(A)453 1133 y Fp(A)h Fl(!)f Fp(B)p 1028 1133 2 138 v 1309 1055 a(M)1354 1040 y Fm(B)p 1210 1065 272 2 v 1226 1108 a Fq(\()p Fp(\025u)1290 1093 y Fm(A)1317 1108 y Fp(M)5 b Fq(\))1378 1093 y Fm(A)p Fg(!)p Fm(B)p 1675 1133 2 138 v 165 1183 2 50 v 1028 1183 V 1675 1183 V 166 1184 1511 2 v 165 1234 2 50 v 1028 1234 V 1675 1234 V 165 1371 2 138 v 463 1265 a Fl(j)11 b Fp(M)412 1325 y(A)h Fl(!)f Fp(B)676 1265 y Fl(j)g Fp(N)670 1325 y(A)p 395 1335 323 2 v 730 1350 a Fl(!)772 1335 y Fg(\000)540 1371 y Fp(B)p 1028 1371 2 138 v 1208 1294 a(M)1253 1278 y Fm(A)p Fg(!)p Fm(B)1432 1294 y Fp(N)1470 1278 y Fm(A)p 1191 1303 323 2 v 1281 1347 a Fq(\()p Fp(M)5 b(N)g Fq(\))1396 1332 y Fm(B)p 1675 1371 2 138 v 165 1421 2 50 v 1028 1421 V 1675 1421 V 166 1423 1511 2 v 165 1473 2 50 v 1028 1473 V 1675 1473 V 165 1610 2 138 v 249 1504 a Fl(j)11 b Fp(M)247 1563 y(A)p 207 1573 112 2 v 330 1589 a Fl(8)353 1574 y Fn(+)223 1610 y Fl(8)p Fp(xA)450 1554 y Fq(if)i Fp(x)j(=)-25 b Fl(2)11 b Fq(FV)q(\()p Fp(B)r Fq(\))j(for)g Fp(u)789 1539 y Fm(B)831 1554 y Fq(free)h(in)e Fp(M)p 1028 1610 2 138 v 1129 1532 a(M)1174 1517 y Fm(A)p 1054 1542 223 2 v 1070 1586 a Fq(\()p Fp(\025xM)5 b Fq(\))1195 1571 y Fg(8)p Fm(xA)1346 1554 y Fq(\(with)13 b(v)n(ar.)g(cond.\))p 1675 1610 2 138 v 165 1660 2 50 v 1028 1660 V 1675 1660 V 166 1662 1511 2 v 165 1712 2 50 v 1028 1712 V 1675 1712 V 165 1862 2 151 v 498 1743 a Fl(j)e Fp(M)473 1803 y Fl(8)p Fp(xA)108 b(t)p 456 1813 236 2 v 704 1828 a Fl(8)727 1813 y Fg(\000)529 1852 y Fp(A)560 1858 y Fm(x)581 1852 y Fq([)p Fp(t)p Fq(])p 1028 1862 2 151 v 1291 1772 a Fp(M)1336 1757 y Fg(8)p Fm(xA)p 1245 1782 203 2 v 1261 1827 a Fq(\()p Fp(M)5 b(t)p Fq(\))1353 1812 y Fm(A)1378 1816 y Ff(x)1397 1812 y Fn([)p Fm(t)p Fn(])p 1675 1862 2 151 v 165 1912 2 50 v 1028 1912 V 1675 1912 V 166 1914 1511 2 v 673 2030 a Fq(T)m(able)13 b(2:)18 b(Natural)c(deduction)38 2153 y(2.)k(F)m(or)13 b(ev)o(ery)i(normal)d(deriv)n(ation)h(term)g Fp(N)19 b Fq(w)o(e)14 b(de\014ne)h(a)e(sequen)o(t)i(term)f Fp(G)p Fq(\()p Fp(N)5 b Fq(\))13 b(\()p Fp(G)h Fq(for)f(Gen)o(tzen\))j (b)o(y)624 2243 y Fp(G)p Fq(\()p Fp(u)p Fq(\))41 b(:=)g Fp(u;)517 2306 y(G)p Fq(\()p Fl(h)p Fp(M)r(;)7 b(N)e Fl(i)p Fq(\))41 b(:=)g Fl(h)p Fp(G)p Fq(\()p Fp(M)5 b Fq(\))p Fp(;)i(G)p Fq(\()p Fp(N)e Fq(\))p Fl(i)p Fp(;)564 2368 y(G)p Fq(\()p Fp(\025z)r(N)g Fq(\))42 b(:=)f Fp(\025z)r(G)p Fq(\()p Fp(N)5 b Fq(\))42 b(with)14 b Fp(z)f Fl(2)f(f)p Fp(u;)7 b(x)p Fl(g)n Fp(;)588 2435 y(G)p Fq(\()p Fp(v)667 2424 y(~)658 2435 y(N)e Fq(\))42 b(:=)f Fp(u)863 2441 y Fm(u)885 2435 y Fl(f)p Fp(v)q(;)7 b(G)p Fq(\()1003 2424 y Fp(~)995 2435 y(N)t Fq(\))p Fl(g)42 b Fq(with)13 b Fp(u)h Fq(new.)-12 2530 y(Here)h(e.g.)e Fp(F)6 b Fq(\()213 2519 y Fp(~)211 2530 y(L)p Fq(\))14 b(abbreviates)h(the)f(list)g (obtained)f(b)o(y)h(applying)f Fp(F)19 b Fq(to)14 b(the)g(elemen)o(ts)g (of)f(the)i(list)1557 2519 y Fp(~)1555 2530 y(L)p Fq(.)-12 2645 y Fo(2.5.)21 b Fd(Lemma.)39 2735 y Fa(1.)f(F)m(or)f(ev)o(ery)h (sequen)o(t)h(term)d Fp(L)i Fa(w)o(e)f(ha)o(v)o(e)g(that)h Fp(F)6 b Fq(\()p Fp(L)p Fq(\))19 b Fa(is)g(a)g(normal)e(deriv)n(ation)i (term,)g(deriving)g(the)h(same)92 2785 y(form)o(ula)11 b(from)h(no)i(more)f(assumptions.)39 2868 y(2.)20 b(F)m(or)d(ev)o(ery)h (normal)e(deriv)n(ation)h(term)f Fp(N)23 b Fa(w)o(e)18 b(ha)o(v)o(e)f(that)h Fp(G)p Fq(\()p Fp(N)5 b Fq(\))17 b Fa(is)g(a)g(sequen)o(t)i(term)e(in)g(m)o(ultiary)e(normal)92 2917 y(form,)d(deriving)h(the)i(same)e(form)o(ula)e(from)h(the)i(same)f (assumptions.)911 3042 y Fq(6)p eop %%Page: 7 7 7 6 bop 39 195 a Fa(3.)20 b(F)m(or)13 b(normal)f(deriv)n(ation)h(terms) h Fp(N)19 b Fa(w)o(e)14 b(ha)o(v)o(e)f Fp(F)6 b Fq(\()p Fp(G)p Fq(\()p Fp(N)f Fq(\)\))12 b(=)f Fp(N)5 b Fa(.)-12 270 y Fd(Pr)o(oof)15 b Fq(1.)j(Induction)c(on)f Fp(L)p Fq(.)18 b(2.)g(Induction)c(on)g Fp(N)5 b Fq(.)18 b(3.)f(Induction)d(on) g Fp(N)5 b Fq(.)573 b Fd(Qed)38 344 y Fq(So)16 b(in)g(this)h(sense)h (natural)e(deduction)h(and)g(the)g(Gen)o(tzen)g(calculus)g(are)g(equiv) n(alen)o(t.)25 b(In)16 b(particular)h(w)o(e)f(ha)o(v)o(e)-12 394 y(assigned)c(to)e(an)o(y)h(sequen)o(t)h(term)f Fp(L)g Fq(in)g(a)f(natural)h(w)o(a)o(y)f(a)h(normal)e(deriv)n(ation)h(term)h Fp(F)6 b Fq(\()p Fp(L)p Fq(\),)11 b(essen)o(tially)g(b)o(y)g(executing) -12 443 y(the)k(explicit)e(substitutions)i(\(in)e(the)i(last)e(clause)i (of)e(the)i(de\014nition)e(of)g Fp(F)6 b Fq(\).)-12 554 y Fo(2.6.)23 b Fd(Remark.)29 b Fp(v)310 560 y Fm(n)332 554 y Fq(:)7 b Fp(A)382 560 y Fm(n)405 554 y Fp(;)g(w)454 560 y Fm(n)475 554 y Fq(:)g Fp(A)525 560 y Fm(n)560 554 y Fl(!)12 b Fp(A)645 560 y Fm(n)681 554 y Fl(!)g Fp(A)766 560 y Fm(n)p Fg(\000)p Fn(1)831 554 y Fp(;)7 b(:)g(:)g(:)e(;)i(w)954 560 y Fn(2)972 554 y Fq(:)g Fp(A)1022 560 y Fn(2)1053 554 y Fl(!)12 b Fp(A)1138 560 y Fn(2)1169 554 y Fl(!)g Fp(A)1254 560 y Fn(1)1273 554 y Fp(;)7 b(w)1322 560 y Fn(1)1340 554 y Fq(:)g Fp(A)1390 560 y Fn(1)1421 554 y Fl(!)12 b Fp(A)1506 560 y Fn(1)1537 554 y Fl(!)g Fp(A)h Fl(\))f Fp(A)j Fq(can)g(b)q(e)-12 603 y(deriv)o(ed)d(b)o(y)f Fp(L)214 609 y Fm(n)249 603 y Fq(:=)g Fp(u)328 609 y Fm(u)350 603 y Fl(f)p Fp(w)401 609 y Fn(1)419 603 y Fp(;)c(v)458 609 y Fn(1)476 603 y Fp(v)496 609 y Fn(1)515 603 y Fl(g)535 616 y Fm(v)552 620 y Fe(1)570 603 y Fl(f)p Fp(w)621 609 y Fn(2)639 603 y Fp(;)g(v)678 609 y Fn(2)697 603 y Fp(v)717 609 y Fn(2)735 603 y Fl(g)g(\001)g(\001)g(\001)811 609 y Fm(v)828 613 y Ff(n)857 603 y Fl(f)p Fp(w)908 609 y Fm(n)930 603 y Fp(;)g(v)969 609 y Fm(n)992 603 y Fp(v)1012 609 y Fm(n)1034 603 y Fl(g)p Fq(,)k(a)h(sequen)o(t)g(term)f(of)g(size)h (linear)f(in)g Fp(n)p Fq(.)17 b(Ho)o(w)o(ev)o(er,)-12 653 y(the)e(normal)c(deriv)n(ation)i(term)h Fp(F)6 b Fq(\()p Fp(L)572 659 y Fm(n)594 653 y Fq(\))12 b(=)g Fp(u)690 659 y Fm(u)711 653 y Fq([)p Fp(w)753 659 y Fn(1)771 653 y Fp(v)791 659 y Fn(1)810 653 y Fp(v)830 659 y Fn(1)849 653 y Fq(])860 666 y Fm(v)877 670 y Fe(1)895 653 y Fq([)p Fp(w)937 659 y Fn(2)955 653 y Fp(v)975 659 y Fn(2)994 653 y Fp(v)1014 659 y Fn(2)1032 653 y Fq(])7 b Fl(\001)g(\001)g(\001) 1099 659 y Fm(v)1116 663 y Ff(n)1145 653 y Fq([)p Fp(w)1187 659 y Fm(n)1209 653 y Fp(v)1229 659 y Fm(n)1252 653 y Fp(v)1272 659 y Fm(n)1294 653 y Fq(])14 b(has)g(2)1415 638 y Fm(n)1451 653 y Fq(o)q(ccurrences)j(of)c Fp(v)1741 659 y Fm(n)1764 653 y Fq(.)-12 793 y Fk(3)67 b(P)n(erm)n(utativ)n(e)24 b(con)n(v)n(ersions)-12 889 y Fq(In)14 b(the)g(t)o(w)o(o)f(example)g (deriv)n(ations)g(considered)i(ab)q(o)o(v)o(e)e(one)h(can)g(see)h(that) e(the)i(second)f(can)g(b)q(e)g(obtained)g(from)e(the)-12 939 y(\014rst)j(b)o(y)f(a)f(certain)i(p)q(erm)o(utation)d(of)i(rules.)k (The)d(righ)o(t)e(premise)g(of)h(the)g(lo)o(w)o(er)g(application)e(of)i Fl(!)o Fq(L)g(in)372 1058 y Fp(u)396 1064 y Fn(1)415 1058 y Fq(:)7 b Fp(A)k Fl(\))g Fp(A)653 1005 y(u)677 1011 y Fn(1)696 1005 y Fq(:)c Fp(A)k Fl(\))g Fp(A)93 b(v)q Fq(:)7 b Fp(B)14 b Fl(\))d Fp(B)96 b(u)p Fq(:)7 b Fp(C)13 b Fl(\))f Fp(C)p 637 1021 752 2 v 1400 1036 a Fl(!)p Fq(L)1468 1018 y Fg(\003)720 1057 y Fp(u)744 1063 y Fn(3)762 1057 y Fq(:)7 b Fp(A)k Fl(!)g Fp(B)j Fl(!)e Fp(C)q(;)7 b(u)1049 1063 y Fn(1)1066 1057 y Fq(:)g Fp(A;)g(v)q Fq(:)g Fp(B)13 b Fl(\))e Fp(C)p 356 1075 966 2 v 1334 1089 a Fl(!)o Fq(L)487 1112 y Fp(u)511 1118 y Fn(2)529 1112 y Fq(:)c Fp(A)k Fl(!)g Fp(B)r(;)c(u)719 1118 y Fn(1)738 1112 y Fq(:)g Fp(A;)g(u)831 1118 y Fn(3)848 1112 y Fq(:)g Fp(A)k Fl(!)g Fp(B)j Fl(!)d Fp(C)k Fl(\))c Fp(C)-12 1179 y Fq(is)18 b(an)f Fl(!)p Fq(L-application)f(itself.)30 b(If)17 b(one)h(mo)o(v)o(es)f(the)h(lo)o(w)o(er)g Fl(!)o Fq(L-application)e(up)o(w)o(ards)j(to)e(the)i(place)f(where)h(the)-12 1228 y(assumption)14 b(v)n(ariable)g(to)g(b)q(e)i(cancelled)f(app)q (ears)h({)f(i.e.)f(to)g(the)i(middle)d(premise)h({,)h(then)g(w)o(e)h (obtain)e(the)h(second)-12 1278 y(deriv)n(ation)332 1364 y Fp(u)356 1370 y Fn(1)375 1364 y Fq(:)7 b Fp(A)k Fl(\))g Fp(A)613 1311 y(u)637 1317 y Fn(1)656 1311 y Fq(:)c Fp(A)k Fl(\))g Fp(A)93 b(v)q Fq(:)7 b Fp(B)14 b Fl(\))d Fp(B)p 597 1327 486 2 v 1095 1340 a Fl(!)p Fq(L)640 1364 y Fp(u)664 1370 y Fn(2)683 1364 y Fq(:)c Fp(A)k Fl(!)g Fp(B)r(;)c(u)873 1370 y Fn(1)891 1364 y Fq(:)g Fp(A)k Fl(\))g Fp(B)203 b(u)p Fq(:)7 b Fp(C)13 b Fl(\))e Fp(C)p 316 1382 1112 2 v 1440 1397 a Fl(!)p Fq(L)1508 1379 y Fg(\003)521 1418 y Fp(u)545 1424 y Fn(3)564 1418 y Fq(:)c Fp(A)k Fl(!)g Fp(B)j Fl(!)d Fp(C)q(;)c(u)850 1424 y Fn(1)867 1418 y Fq(:)g Fp(A;)g(u)960 1424 y Fn(2)977 1418 y Fq(:)g Fp(A)12 b Fl(!)f Fp(B)j Fl(\))d Fp(C)-12 1475 y Fq(Here)k(the)g(righ)o(t)e (premise)h(of)f(an)o(y)g(of)h(the)g(t)o(w)o(o)g Fl(!)o Fq(L-rules)g(is)g(an)g(axiom.)38 1530 y(More)i(generally)g(b)o(y)f (so-called)h Fj(p)n(ermutative)g(c)n(onversions)k Fq(w)o(e)c(can)g(ac)o (hiev)o(e)g(that)g(in)f(all)g(`left')g(or)g(elimination)-12 1579 y(rules)g Fp(M)128 1585 y Fm(u)150 1579 y Fl(f)p Fp(w)q(;)7 b(i)p Fl(g)o Fq(,)13 b Fp(M)320 1585 y Fm(u)342 1579 y Fl(f)p Fp(v)q(;)7 b(L)p Fl(g)14 b Fq(and)g Fp(M)587 1585 y Fm(u)609 1579 y Fl(f)p Fp(v)q(;)7 b(t)p Fl(g)13 b Fq(the)i(main)d(premise)i Fp(M)k Fq(solely)c(consists)h(of)e(the)i (assumption)d(v)n(ariable)-12 1629 y Fp(u)h Fq(b)q(ound)h(in)f(this)g (rule.)18 b(W)m(e)13 b(will)f(see)i(that)g(these)h(so-called)e Fp(\031)q Fj(-normal)k Fq(sequen)o(t)e(terms)e(corresp)q(ond)i (bijectiv)o(ely)d(to)-12 1679 y(normal)g(deriv)n(ation)h(terms.)38 1734 y(T)m(o)g(form)o(ulate)f(p)q(erm)o(utativ)o(e)h(con)o(v)o(ersions) i(w)o(e)f(mak)o(e)e(use)j(of)e(the)i(m)o(ultiary)c(normal)h(form)g(in)o (tro)q(duced)j(ab)q(o)o(v)o(e.)-12 1844 y Fo(3.1.)21 b Fd(Definition.)27 b Fq(1.)18 b(The)c(relation)g Fl(7!)673 1850 y Fm(\031)709 1844 y Fq(of)f Fj(p)n(ermutative)h(c)n(onversion)k Fq(is)c(de\014ned)h(b)o(y)275 1919 y Fp(M)315 1925 y Fm(v)335 1919 y Fl(f)p Fp(u;)400 1909 y(~)399 1919 y(L)p Fl(g)41 b(7!)531 1925 y Fm(\031)594 1919 y Fp(M)r(;)49 b Fq(if)13 b Fp(v)18 b(=)-26 b Fl(2)11 b Fq(F)-5 b(A)q(\()p Fp(M)5 b Fq(\).)851 b(\(1\))108 1986 y Fp(N)141 1992 y Fm(w)169 1986 y Fl(f)p Fp(u)214 1992 y Fn(1)232 1986 y Fp(;)262 1976 y(~)251 1986 y(M)t Fl(g)316 1999 y Fm(v)335 1986 y Fl(f)p Fp(u;)400 1976 y(~)399 1986 y(L)p Fl(g)41 b(7!)531 1992 y Fm(\031)594 1986 y Fp(N)627 1992 y Fm(w)655 1986 y Fl(f)p Fp(u)700 1992 y Fn(1)718 1986 y Fp(;)7 b(\026)p Fq(\()790 1976 y Fp(~)778 1986 y(M)818 1992 y Fm(v)837 1986 y Fl(f)p Fp(u;)902 1976 y(~)901 1986 y(L)p Fl(g)o Fq(\))p Fl(g)p Fp(;)48 b Fq(if)13 b Fp(u)1108 1992 y Fn(1)1138 1986 y Fl(6)p Fq(=)f Fp(v)q Fq(,)i Fp(v)k(=)-26 b Fl(2)11 b Fq(F)-5 b(A)q(\()p Fp(N)5 b Fq(\))14 b(and)g Fp(v)f Fl(2)e Fq(F)-5 b(A)q(\()1674 1976 y Fp(~)1662 1986 y(M)5 b Fq(\).)66 b(\(2\))129 2056 y Fp(N)162 2062 y Fm(w)189 2056 y Fl(f)p Fp(v)q(;)262 2045 y(~)250 2056 y(M)5 b Fl(g)316 2068 y Fm(v)335 2056 y Fl(f)p Fp(u;)400 2045 y(~)399 2056 y(L)p Fl(g)41 b(7!)531 2062 y Fm(\031)594 2056 y Fp(N)627 2062 y Fm(w)655 2056 y Fl(f)p Fp(u;)719 2045 y(~)719 2056 y(L)o(\026)p Fq(\()799 2045 y Fp(~)787 2056 y(M)827 2062 y Fm(v)847 2056 y Fl(f)p Fp(u;)912 2045 y(~)911 2056 y(L)o Fl(g)p Fq(\))p Fl(g)p Fp(;)48 b Fq(if)13 b Fp(v)18 b(=)-26 b Fl(2)11 b Fq(F)-5 b(A)q(\()p Fp(N)5 b Fq(\))14 b(and)g Fp(v)f Fl(2)e Fq(F)-5 b(A)q(\()1539 2045 y Fp(~)1527 2056 y(M)t Fq(\).)202 b(\(3\))185 2125 y Fl(h)p Fp(M)r(;)7 b(N)e Fl(i)316 2131 y Fm(v)335 2125 y Fl(f)p Fp(u;)400 2114 y(~)399 2125 y(L)p Fl(g)41 b(7!)531 2131 y Fm(\031)594 2125 y Fl(h)p Fp(\026)p Fq(\()p Fp(M)691 2131 y Fm(v)712 2125 y Fl(f)p Fp(u;)776 2114 y(~)776 2125 y(L)o Fl(g)p Fq(\))p Fp(;)7 b(\026)p Fq(\()p Fp(N)933 2131 y Fm(v)953 2125 y Fl(f)p Fp(u;)1017 2114 y(~)1017 2125 y(L)o Fl(g)o Fq(\))p Fl(i)p Fp(:)693 b Fq(\(4\))193 2192 y(\()p Fp(\025z)r(M)5 b Fq(\))315 2198 y Fm(v)335 2192 y Fl(f)p Fp(u;)400 2181 y(~)399 2192 y(L)p Fl(g)41 b(7!)531 2198 y Fm(\031)594 2192 y Fp(\025z)r(:\026)p Fq(\()p Fp(M)732 2198 y Fm(v)752 2192 y Fl(f)p Fp(u;)817 2181 y(~)816 2192 y(L)p Fl(g)o Fq(\))h(for)14 b Fp(z)f Fl(2)e(f)p Fp(w)q(;)c(x)p Fl(g)13 b Fq(and)h Fp(w)e Fl(6)p Fq(=)g Fp(v)q Fq(.)415 b(\(5\))-12 2267 y(Observ)o(e)15 b(that)f(from)e Fp(M)k Fl(7!)433 2273 y Fm(\031)467 2267 y Fp(M)512 2252 y Fg(0)537 2267 y Fq(with)d Fp(M)18 b Fq(in)13 b(m)o(ultiary)e(normal)h(form)g(w)o(e)h(can)h(conclude)h(that) e Fp(M)1585 2252 y Fg(0)1610 2267 y Fq(is)h(in)f(m)o(ultiary)-12 2317 y(normal)f(form)g(to)q(o.)18 b({)13 b(The)i Fj(term)f(closur)n(e)j Fl(\000)-7 b(!)744 2323 y Fm(\031)780 2317 y Fq(of)13 b(these)i(con)o(v)o(ersions)g(is)f(de\014ned)h(as)f(in)f(de\014nition)h (2.1)38 2372 y(2.)19 b(F)m(or)14 b(an)o(y)g(sequen)o(t)h(terms)g Fp(M)r(;)7 b(M)617 2357 y Fg(0)642 2372 y Fq(let)15 b Fp(M)i Fl(\000)-7 b(!)827 2378 y Fm(\031)861 2372 y Fp(M)906 2357 y Fg(0)932 2372 y Fq(i\013)14 b(for)g(the)h(m)o(ultiary)d(normal)g (forms)h Fp(\026)p Fq(\()p Fp(M)5 b Fq(\))14 b(and)h Fp(\026)p Fq(\()p Fp(M)1827 2357 y Fg(0)1838 2372 y Fq(\))-12 2422 y(w)o(e)f(ha)o(v)o(e)g Fp(\026)p Fq(\()p Fp(M)5 b Fq(\))12 b Fl(\000)-7 b(!)326 2428 y Fm(\031)360 2422 y Fp(\026)p Fq(\()p Fp(M)446 2407 y Fg(0)457 2422 y Fq(\))14 b(as)g(de\014ned)h(in)f(1.)38 2477 y(W)m(e)h(no)o(w)g(pro)o(v)o(e)g (termination)e(of)i Fl(\000)-7 b(!)655 2483 y Fm(\031)677 2477 y Fq(;)16 b(clearly)f(it)g(su\016ces)h(to)f(consider)h(sequen)o(t) h(terms)e(in)g(m)o(ultiary)d(normal)-12 2526 y(form.)k(Our)f(main)d(to) q(ol)h(will)f(b)q(e)j(a)e(measure)h(function)g Fp(\016)r Fq(,)f(de\014ned)i(as)f(follo)o(ws.)-12 2637 y Fo(3.2.)21 b Fd(Definition.)606 2712 y Fp(\016)r Fq(\()p Fp(u)p Fq(\))41 b(:=)h(1)p Fp(;)506 2774 y(\016)r Fq(\()p Fl(h)p Fp(L;)7 b(M)e Fl(i)p Fq(\))41 b(:=)h Fp(\016)r Fq(\()p Fp(L)p Fq(\))9 b(+)h Fp(\016)r Fq(\()p Fp(M)5 b Fq(\))p Fp(;)556 2836 y(\016)r Fq(\()p Fp(\025z)r(L)p Fq(\))42 b(:=)g Fp(\016)r Fq(\()p Fp(L)p Fq(\))g(with)13 b Fp(z)h Fl(2)d(f)p Fp(u;)c(x)p Fl(g)n Fp(;)458 2911 y(\016)r Fq(\()p Fp(M)534 2917 y Fm(u)556 2911 y Fl(f)p Fp(v)q(;)618 2901 y(~)617 2911 y(L)p Fl(g)p Fq(\))41 b(:=)h Fp(\016)r Fq(\()p Fp(M)5 b Fq(\))k(+)g(#\()p Fp(M)c Fq(\))k Fl(\001)1098 2865 y Fb(\020)1123 2911 y Fq(1)g(+)1194 2872 y Fb(X)1261 2911 y Fp(\016)r Fq(\()1299 2901 y Fp(~)1297 2911 y(L)q Fq(\))1342 2865 y Fb(\021)1373 2911 y Fp(:)911 3042 y Fq(7)p eop %%Page: 8 8 8 7 bop -12 195 a Fq(Here)15 b(w)o(e)f(ha)o(v)o(e)g(made)f(use)i(of)e (#\()p Fp(M)5 b Fq(\))13 b(\(a)h(b)q(ound)g(for)g(the)g(n)o(um)o(b)q (er)f(of)h(no)q(des)g(in)g Fp(M)5 b Fq(\),)13 b(whic)o(h)h(is)f (de\014ned)i(b)o(y)636 286 y(#\()p Fp(u)p Fq(\))41 b(:=)h(1)p Fp(;)536 349 y Fq(#\()p Fl(h)p Fp(L;)7 b(M)e Fl(i)p Fq(\))41 b(:=)h(#\()p Fp(L)p Fq(\))9 b(+)h(#\()p Fp(M)5 b Fq(\))k(+)g(1)p Fp(;)586 411 y Fq(#\()p Fp(\025z)r(L)p Fq(\))42 b(:=)g(#\()p Fp(L)p Fq(\))9 b(+)h(1)41 b(with)13 b Fp(z)h Fl(2)d(f)p Fp(u;)c(x)p Fl(g)o Fp(;)488 486 y Fq(#\()p Fp(M)579 492 y Fm(u)601 486 y Fl(f)p Fp(v)q(;)664 475 y(~)662 486 y(L)p Fl(g)p Fq(\))41 b(:=)h(#\()p Fp(M)5 b Fq(\))k Fl(\001)995 440 y Fb(\020)1020 486 y Fq(1)g(+)1092 446 y Fb(X)1159 486 y Fq(#\()1212 475 y Fp(~)1210 486 y(L)p Fq(\))1254 440 y Fb(\021)1285 486 y Fp(:)38 595 y Fq(W)m(e)k(\014rst)i(sho)o(w)f (that)g(the)g(in)o(tro)q(duction)g(of)f(abbreviations)h(in)f(the)i (sense)g(of)f Fl(\000)-7 b(!)1343 601 y Fm(\026)1379 595 y Fq(also)13 b(lo)o(w)o(ers)h(the)g Fp(\016)r Fq(-measure.)-12 712 y Fo(3.3.)21 b Fd(Lemma.)28 b Fa(If)14 b Fp(M)i Fl(\000)-7 b(!)427 718 y Fm(\026)461 712 y Fp(M)506 697 y Fg(0)517 712 y Fa(,)13 b(then)i Fp(\016)r Fq(\()p Fp(M)5 b Fq(\))12 b Fp(>)f(\016)r Fq(\()p Fp(M)870 697 y Fg(0)882 712 y Fq(\))j Fa(and)g Fq(#\()p Fp(M)5 b Fq(\))11 b Fp(>)h Fq(#\()p Fp(M)1256 697 y Fg(0)1267 712 y Fq(\))p Fa(.)-12 795 y Fd(Pr)o(oof)p Fq(.)26 b(It)16 b(su\016ces)h(to)f(pro)o(v)o(e)g (the)h(claim)d(for)h(the)i(case)g Fp(M)j Fl(7!)1030 801 y Fm(\026)1067 795 y Fp(M)1112 780 y Fg(0)1123 795 y Fq(;)d(the)g(general)f(case)h(then)g(follo)o(ws)d(from)h(the)-12 851 y(de\014nition)d(of)g Fp(\016)r Fq(.)18 b(So)12 b(w)o(e)h(consider) g(a)g(con)o(v)o(ersion)f Fp(N)810 857 y Fm(w)838 851 y Fl(f)p Fp(u;)913 840 y(~)902 851 y(M)s Fl(g)966 863 y Fm(u)988 851 y Fl(f)p Fp(v)q(;)1050 840 y(~)1049 851 y(L)p Fl(g)f(7!)1151 857 y Fm(\026)1184 851 y Fp(N)1217 857 y Fm(w)1245 851 y Fl(f)p Fp(v)q(;)1307 840 y(~)1306 851 y(L)1346 840 y(~)1334 851 y(M)t Fl(g)i Fq(with)f Fp(u)k(=)-26 b Fl(2)11 b Fq(F)-5 b(A)q(\()p Fp(N)r(;)1715 840 y(~)1703 851 y(M)5 b Fq(\).)18 b(F)m(or)-12 901 y(the)d(left)e (hand)h(side)g(w)o(e)g(ha)o(v)o(e)40 992 y Fp(\016)r Fq(\()p Fp(N)109 998 y Fm(w)136 992 y Fl(f)p Fp(u;)211 981 y(~)200 992 y(M)t Fl(g)265 1004 y Fm(u)286 992 y Fl(f)p Fp(v)q(;)349 981 y(~)347 992 y(L)p Fl(g)p Fq(\))42 b(=)g Fp(\016)r Fq(\()p Fp(N)597 998 y Fm(w)624 992 y Fl(f)p Fp(u;)699 981 y(~)688 992 y(M)t Fl(g)p Fq(\))9 b(+)g(#\()p Fp(N)903 998 y Fm(w)930 992 y Fl(f)p Fp(u;)1006 981 y(~)994 992 y(M)t Fl(g)p Fq(\))1082 946 y Fb(\020)1107 992 y Fq(1)g(+)1178 953 y Fb(X)1245 992 y Fp(\016)r Fq(\()1283 981 y Fp(~)1281 992 y(L)q Fq(\))1326 946 y Fb(\021)454 1083 y Fq(=)42 b Fp(\016)r Fq(\()p Fp(N)5 b Fq(\))k(+)h(#\()p Fp(N)5 b Fq(\))781 1037 y Fb(\020)805 1083 y Fq(1)k(+)877 1044 y Fb(X)943 1083 y Fp(\016)r Fq(\()992 1073 y Fp(~)979 1083 y(M)c Fq(\))1040 1037 y Fb(\021)1075 1083 y Fq(+)k(#\()p Fp(N)c Fq(\))1228 1037 y Fb(\020)1252 1083 y Fq(1)k(+)1324 1044 y Fb(X)1391 1083 y Fq(#\()1454 1073 y Fp(~)1442 1083 y(M)t Fq(\))1502 1037 y Fb(\021)e(\020)1559 1083 y Fq(1)i(+)1631 1044 y Fb(X)1697 1083 y Fp(\016)r Fq(\()1735 1073 y Fp(~)1733 1083 y(L)q Fq(\))1778 1037 y Fb(\021)-12 1185 y Fq(and)14 b(for)f(the)i(righ)o(t)e(hand)h(side)383 1286 y Fp(\016)r Fq(\()p Fp(N)452 1292 y Fm(w)479 1286 y Fl(f)p Fp(v)q(;)542 1276 y(~)540 1286 y(L)581 1276 y(~)568 1286 y(M)5 b Fl(g)p Fq(\))12 b(=)f Fp(\016)r Fq(\()p Fp(N)5 b Fq(\))10 b(+)f(#\()p Fp(N)c Fq(\))958 1240 y Fb(\020)983 1286 y Fq(1)k(+)1054 1247 y Fb(X)1121 1286 y Fp(\016)r Fq(\()1159 1276 y Fp(~)1157 1286 y(L)q Fq(\))g(+)1252 1247 y Fb(X)1319 1286 y Fp(\016)r Fq(\()1368 1276 y Fp(~)1355 1286 y(M)c Fq(\))1416 1240 y Fb(\021)1448 1286 y Fp(:)-12 1388 y Fq(Clearly)13 b(the)i(lhs)f(is)f(greater)i(than) f(the)h(rhs.)j(Similarly)11 b(w)o(e)j(ha)o(v)o(e)g(for)f(#)h(on)f(the)i (lhs)349 1489 y(#\()p Fp(N)433 1495 y Fm(w)460 1489 y Fl(f)p Fp(u;)536 1479 y(~)524 1489 y(M)t Fl(g)589 1502 y Fm(u)611 1489 y Fl(f)p Fp(v)q(;)673 1479 y(~)672 1489 y(L)p Fl(g)o Fq(\))d(=)g(#\()p Fp(N)5 b Fq(\))904 1443 y Fb(\020)928 1489 y Fq(1)k(+)1000 1450 y Fb(X)1067 1489 y Fq(#\()1130 1479 y Fp(~)1118 1489 y(M)t Fq(\))1178 1443 y Fb(\021)e(\020)1235 1489 y Fq(1)i(+)1306 1450 y Fb(X)1373 1489 y Fq(#\()1426 1479 y Fp(~)1424 1489 y(L)p Fq(\))1468 1443 y Fb(\021)-12 1591 y Fq(and)14 b(on)g(the)g(rhs)431 1640 y(#\()p Fp(N)515 1646 y Fm(w)542 1640 y Fl(f)p Fp(v)q(;)605 1630 y(~)603 1640 y(L)644 1630 y(~)632 1640 y(M)t Fl(g)p Fq(\))e(=)g(#\()p Fp(N)5 b Fq(\))881 1594 y Fb(\020)905 1640 y Fq(1)k(+)977 1601 y Fb(X)1043 1640 y Fq(#\()1096 1630 y Fp(~)1094 1640 y(L)p Fq(\))h(+)1189 1601 y Fb(X)1256 1640 y Fq(#\()1319 1630 y Fp(~)1307 1640 y(M)5 b Fq(\))1368 1594 y Fb(\021)1400 1640 y Fp(:)-12 1725 y Fq(Again)13 b(the)i(lhs)f(clearly)f(is)h (greater)h(than)f(the)g(rhs.)974 b Fd(Qed)-12 1866 y Fo(3.4.)21 b Fd(Theorem.)28 b Fa(If)13 b Fp(M)k Fl(\000)-7 b(!)475 1872 y Fm(\031)509 1866 y Fp(M)554 1851 y Fg(0)565 1866 y Fa(,)13 b(then)i Fp(\016)r Fq(\()p Fp(M)5 b Fq(\))12 b Fp(>)f(\016)r Fq(\()p Fp(M)918 1851 y Fg(0)930 1866 y Fq(\))j Fa(and)g Fq(#\()p Fp(M)5 b Fq(\))11 b Fl(\025)h Fq(#\()p Fp(M)1304 1851 y Fg(0)1315 1866 y Fq(\))p Fa(.)-12 1949 y Fd(Pr)o(oof)p Fq(.)22 b(W)m(e)14 b(\014rst)i(treat)f(the)h(p)q (erm)o(utativ)o(e)e(con)o(v)o(ersions.)21 b(By)15 b(Lemma)d(3.3)i(it)g (su\016ces)j(to)d(do)h(this)g(for)f(the)i(terms)-12 1999 y(without)e Fp(\026)g Fq(on)f(the)i(righ)o(t)e(hand)h(side.)38 2057 y(\(1\).)k(Let)c Fp(v)k(=)-25 b Fl(2)11 b Fq(F)-5 b(A\()p Fp(M)5 b Fq(\).)18 b(Then)d(w)o(e)f(ha)o(v)o(e)432 2161 y Fp(\016)r Fq(\()p Fp(M)508 2167 y Fm(v)528 2161 y Fl(f)p Fp(u;)593 2151 y(~)592 2161 y(L)o Fl(g)p Fq(\))e(=)g Fp(\016)r Fq(\()p Fp(M)5 b Fq(\))k(+)g(#\()p Fp(M)c Fq(\))978 2115 y Fb(\020)1003 2161 y Fq(1)k(+)1074 2122 y Fb(X)1141 2161 y Fp(\016)r Fq(\()1179 2151 y Fp(~)1177 2161 y(L)q Fq(\))1222 2115 y Fb(\021)1258 2161 y Fp(>)j(\016)r Fq(\()p Fp(M)5 b Fq(\))p Fp(;)-12 2265 y Fq(since)15 b(#\()p Fp(M)5 b Fq(\))11 b Fp(>)h Fq(0,)h(and)484 2327 y(#\()p Fp(M)575 2333 y Fm(v)595 2327 y Fl(f)p Fp(u;)659 2317 y(~)659 2327 y(L)o Fl(g)p Fq(\))e(=)h(#\()p Fp(M)5 b Fq(\))897 2281 y Fb(\020)922 2327 y Fq(1)k(+)993 2288 y Fb(X)1060 2327 y Fq(#\()1113 2317 y Fp(~)1111 2327 y(L)p Fq(\))1155 2281 y Fb(\021)1191 2327 y Fl(\025)j Fq(#\()p Fp(M)5 b Fq(\))p Fp(:)38 2432 y Fq(\(2\).)18 b(Let)c Fp(u)219 2438 y Fn(1)249 2432 y Fl(6)p Fq(=)e Fp(v)q Fq(,)i Fp(v)k(=)-26 b Fl(2)11 b Fq(F)-5 b(A)q(\()p Fp(N)5 b Fq(\))14 b(and)g Fp(v)f Fl(2)e Fq(F)-5 b(A)q(\()785 2421 y Fp(~)773 2432 y(M)5 b Fq(\).)18 b(Then)c(w)o(e)g(ha)o(v)o(e)g (for)g(the)g(lhs)27 2536 y Fp(\016)r Fq(\()p Fp(N)96 2542 y Fm(w)123 2536 y Fl(f)p Fp(u)168 2542 y Fn(1)186 2536 y Fp(;)217 2525 y(~)205 2536 y(M)5 b Fl(g)270 2548 y Fm(v)290 2536 y Fl(f)p Fp(u;)355 2525 y(~)354 2536 y(L)o Fl(g)p Fq(\))42 b(=)g Fp(\016)r Fq(\()p Fp(N)603 2542 y Fm(w)630 2536 y Fl(f)p Fp(u)675 2542 y Fn(1)693 2536 y Fp(;)724 2525 y(~)712 2536 y(M)t Fl(g)p Fq(\))9 b(+)h(#\()p Fp(N)928 2542 y Fm(w)955 2536 y Fl(f)p Fp(u)1000 2542 y Fn(1)1018 2536 y Fp(;)1049 2525 y(~)1037 2536 y(M)t Fl(g)p Fq(\))1125 2489 y Fb(\020)1150 2536 y Fq(1)f(+)1221 2496 y Fb(X)1288 2536 y Fp(\016)r Fq(\()1326 2525 y Fp(~)1324 2536 y(L)q Fq(\))1369 2489 y Fb(\021)460 2627 y Fq(=)42 b Fp(\016)r Fq(\()p Fp(N)5 b Fq(\))k(+)h(#\()p Fp(N)5 b Fq(\))787 2581 y Fb(\020)811 2627 y Fq(1)k(+)882 2587 y Fb(X)949 2627 y Fp(\016)r Fq(\()998 2616 y Fp(~)985 2627 y(M)c Fq(\))1046 2581 y Fb(\021)1080 2627 y Fq(+)10 b(#\()p Fp(N)5 b Fq(\))1234 2581 y Fb(\020)1258 2627 y Fq(1)k(+)1330 2587 y Fb(X)1397 2627 y Fq(#\()1460 2616 y Fp(~)1448 2627 y(M)t Fq(\))1508 2581 y Fb(\021)e(\020)1565 2627 y Fq(1)i(+)1636 2587 y Fb(X)1703 2627 y Fp(\016)r Fq(\()1741 2616 y Fp(~)1739 2627 y(L)q Fq(\))1784 2581 y Fb(\021)-12 2708 y Fq(and)14 b(for)f(the)i(rhs)31 2820 y Fp(\016)r Fq(\()p Fp(N)100 2826 y Fm(w)128 2820 y Fl(f)p Fp(u)173 2826 y Fn(1)191 2820 y Fp(;)222 2809 y(~)210 2820 y(M)250 2826 y Fm(v)269 2820 y Fl(f)p Fp(u;)334 2809 y(~)333 2820 y(L)p Fl(g)o(g)p Fq(\))42 b(=)g Fp(\016)r Fq(\()p Fp(N)5 b Fq(\))k(+)h(#\()p Fp(N)5 b Fq(\))787 2774 y Fb(\020)811 2820 y Fq(1)k(+)882 2780 y Fb(X)949 2820 y Fp(\016)r Fq(\()998 2809 y Fp(~)985 2820 y(M)1025 2826 y Fm(v)1045 2820 y Fl(f)p Fp(u;)1110 2809 y(~)1109 2820 y(L)p Fl(g)o Fq(\))1173 2774 y Fb(\021)460 2911 y Fq(=)42 b Fp(\016)r Fq(\()p Fp(N)5 b Fq(\))k(+)h(#\()p Fp(N)5 b Fq(\))787 2865 y Fb(\020)811 2911 y Fq(1)k(+)882 2872 y Fb(X)949 2911 y Fp(\016)r Fq(\()998 2900 y Fp(~)985 2911 y(M)c Fq(\))10 b(+)1097 2865 y Fb(\020)1122 2872 y(X)1189 2911 y Fq(#\()1252 2900 y Fp(~)1240 2911 y(M)t Fq(\))1300 2865 y Fb(\021)d(\020)1357 2911 y Fq(1)i(+)1429 2872 y Fb(X)1495 2911 y Fp(\016)r Fq(\()1533 2900 y Fp(~)1531 2911 y(L)q Fq(\))1576 2865 y Fb(\021\021)1632 2911 y Fp(:)911 3042 y Fq(8)p eop %%Page: 9 9 9 8 bop -12 195 a Fq(Clearly)13 b(the)i(lhs)f(is)f(greater)i(than)f (the)h(rhs.)j(F)m(or)c(#)f(w)o(e)h(ha)o(v)o(e)g(on)g(the)g(lhs)281 291 y(#\()p Fp(N)365 297 y Fm(w)392 291 y Fl(f)p Fp(u)437 297 y Fn(1)455 291 y Fp(;)486 281 y(~)474 291 y(M)5 b Fl(g)539 304 y Fm(v)559 291 y Fl(f)p Fp(u;)624 281 y(~)623 291 y(L)o Fl(g)p Fq(\))42 b(=)f(#\()p Fp(N)886 297 y Fm(w)913 291 y Fl(f)p Fp(u)958 297 y Fn(1)977 291 y Fp(;)1007 281 y(~)996 291 y(M)t Fl(g)p Fq(\))1084 245 y Fb(\020)1108 291 y Fq(1)9 b(+)1180 252 y Fb(X)1247 291 y Fq(#\()1300 281 y Fp(~)1298 291 y(L)p Fq(\))1342 245 y Fb(\021)729 383 y Fq(=)41 b(#\()p Fp(N)5 b Fq(\))914 337 y Fb(h)934 383 y Fq(1)k(+)1005 343 y Fb(X)1072 383 y Fq(#\()1135 372 y Fp(~)1123 383 y(M)c Fq(\))1184 337 y Fb(i)h(\020)1235 383 y Fq(1)j(+)1307 343 y Fb(X)1373 383 y Fq(#\()1426 372 y Fp(~)1424 383 y(L)p Fq(\))1468 337 y Fb(\021)-12 462 y Fq(and)14 b(for)f(the)i(rhs)286 574 y(#\()p Fp(N)370 580 y Fm(w)397 574 y Fl(f)p Fp(u)442 580 y Fn(1)460 574 y Fp(;)491 564 y(~)479 574 y(M)519 580 y Fm(v)538 574 y Fl(f)p Fp(u;)603 564 y(~)602 574 y(L)o Fl(gg)p Fq(\))42 b(=)f(#\()p Fp(N)5 b Fq(\))914 528 y Fb(\020)939 574 y Fq(1)k(+)1010 535 y Fb(X)1077 574 y Fq(#\()1140 564 y Fp(~)1128 574 y(M)1168 580 y Fm(v)1188 574 y Fl(f)p Fp(u;)1253 564 y(~)1252 574 y(L)o Fl(g)p Fq(\))1316 528 y Fb(\021)729 666 y Fq(=)41 b(#\()p Fp(N)5 b Fq(\))914 620 y Fb(h)934 666 y Fq(1)k(+)1005 620 y Fb(\020)1030 626 y(X)1097 666 y Fq(#\()1160 655 y Fp(~)1148 666 y(M)t Fq(\))1208 620 y Fb(\021)e(\020)1265 666 y Fq(1)i(+)1337 626 y Fb(X)1403 666 y Fq(#\()1456 655 y Fp(~)1454 666 y(L)p Fq(\))1498 620 y Fb(\021i)1550 666 y Fp(:)-12 762 y Fq(Clearly)k(the)i(lhs)f(is)f(greater)i(than)f(or)g(equal)g(to)f(the) i(rhs.)38 819 y(\(3\).)j(Let)c Fp(v)k(=)-25 b Fl(2)11 b Fq(F)-5 b(A\()p Fp(N)5 b Fq(\))14 b(and)g Fp(v)f Fl(2)e Fq(F)-5 b(A)q(\()640 809 y Fp(~)628 819 y(M)5 b Fq(\).)18 b(Then)c(w)o(e)h(ha)o(v)o(e)e(for)h(the)g(lhs)32 918 y Fp(\016)r Fq(\()p Fp(N)101 924 y Fm(w)128 918 y Fl(f)p Fp(v)q(;)201 907 y(~)189 918 y(M)5 b Fl(g)254 930 y Fm(v)274 918 y Fl(f)p Fp(u;)339 907 y(~)338 918 y(L)o Fl(g)p Fq(\))42 b(=)f Fp(\016)r Fq(\()p Fp(N)586 924 y Fm(w)614 918 y Fl(f)p Fp(v)q(;)687 907 y(~)675 918 y(M)t Fl(g)p Fq(\))10 b(+)f(#\()p Fp(N)891 924 y Fm(w)918 918 y Fl(f)p Fp(v)q(;)991 907 y(~)979 918 y(M)c Fl(g)o Fq(\))1067 872 y Fb(\020)1092 918 y Fq(1)k(+)1164 878 y Fb(X)1231 918 y Fp(\016)r Fq(\()1269 907 y Fp(~)1267 918 y(L)p Fq(\))1311 872 y Fb(\021)444 1009 y Fq(=)41 b Fp(\016)r Fq(\()p Fp(N)5 b Fq(\))10 b(+)f(#\()p Fp(N)c Fq(\))770 963 y Fb(\020)795 1009 y Fq(1)k(+)866 969 y Fb(X)933 1009 y Fp(\016)r Fq(\()982 998 y Fp(~)969 1009 y(M)c Fq(\))1030 963 y Fb(\021)1064 1009 y Fq(+)10 b(#\()p Fp(N)5 b Fq(\))1218 963 y Fb(\020)1242 1009 y Fq(1)k(+)1314 969 y Fb(X)1381 1009 y Fq(#\()1444 998 y Fp(~)1432 1009 y(M)t Fq(\))1492 963 y Fb(\021)e(\020)1549 1009 y Fq(1)i(+)1620 969 y Fb(X)1687 1009 y Fp(\016)r Fq(\()1725 998 y Fp(~)1723 1009 y(L)q Fq(\))1768 963 y Fb(\021)1799 1009 y Fp(:)-12 1105 y Fq(F)m(or)14 b(the)g(rhs)h(w)o(e) f(obtain)163 1191 y Fp(\016)r Fq(\()p Fp(N)232 1197 y Fm(w)260 1191 y Fl(f)p Fp(u;)324 1181 y(~)324 1191 y(L)363 1181 y(~)351 1191 y(M)391 1197 y Fm(v)411 1191 y Fl(f)p Fp(u;)476 1181 y(~)475 1191 y(L)o Fl(gg)p Fq(\))163 1266 y(=)35 b Fp(\016)r Fq(\()p Fp(N)5 b Fq(\))10 b(+)f(#\()p Fp(N)c Fq(\))483 1220 y Fb(\020)508 1266 y Fq(1)k(+)579 1227 y Fb(X)646 1266 y Fp(\016)r Fq(\()684 1255 y Fp(~)682 1266 y(L)p Fq(\))h(+)777 1227 y Fb(X)844 1266 y Fp(\016)r Fq(\()893 1255 y Fp(~)880 1266 y(M)920 1272 y Fm(v)940 1266 y Fl(f)p Fp(u;)1005 1255 y(~)1004 1266 y(L)p Fl(g)o Fq(\))1068 1220 y Fb(\021)163 1357 y Fq(=)35 b Fp(\016)r Fq(\()p Fp(N)5 b Fq(\))10 b(+)f(#\()p Fp(N)c Fq(\))483 1311 y Fb(\020)508 1357 y Fq(1)k(+)579 1318 y Fb(X)646 1357 y Fp(\016)r Fq(\()694 1347 y Fp(~)682 1357 y(M)c Fq(\))743 1311 y Fb(\021)777 1357 y Fq(+)10 b(#\()p Fp(N)5 b Fq(\))931 1318 y Fb(X)997 1357 y Fp(\016)r Fq(\()1035 1347 y Fp(~)1033 1357 y(L)q Fq(\))k(+)g(#\()p Fp(N)c Fq(\))1240 1311 y Fb(\020)1265 1318 y(X)1332 1357 y Fq(#\()1395 1347 y Fp(~)1383 1357 y(M)t Fq(\))1443 1311 y Fb(\021)i(\020)1500 1357 y Fq(1)i(+)1571 1318 y Fb(X)1638 1357 y Fp(\016)r Fq(\()1676 1347 y Fp(~)1674 1357 y(L)q Fq(\))1719 1311 y Fb(\021)1751 1357 y Fp(:)-12 1454 y Fq(Clearly)k(again)g(the)i(lhs)e (is)h(greater)h(than)f(the)g(rhs.)19 b(F)m(or)14 b(#)f(w)o(e)h(ha)o(v)o (e)g(on)f(the)i(lhs)187 1550 y(#\()p Fp(N)271 1556 y Fm(u)291 1560 y Fe(1)309 1550 y Fl(f)p Fp(v)q(;)382 1539 y(~)370 1550 y(M)5 b Fl(g)436 1562 y Fm(v)455 1550 y Fl(f)p Fp(u;)520 1539 y(~)519 1550 y(L)p Fl(g)o Fq(\))42 b(=)g(#\()p Fp(N)783 1556 y Fm(u)803 1560 y Fe(1)821 1550 y Fl(f)p Fp(v)q(;)894 1539 y(~)882 1550 y(M)5 b Fl(g)o Fq(\))970 1504 y Fb(\020)995 1550 y Fq(1)k(+)1067 1510 y Fb(X)1133 1550 y Fq(#\()1186 1539 y Fp(~)1184 1550 y(L)p Fq(\))1228 1504 y Fb(\021)625 1641 y Fq(=)42 b(#\()p Fp(N)5 b Fq(\))811 1595 y Fb(\020)835 1641 y Fq(1)k(+)907 1602 y Fb(X)974 1641 y Fq(#\()1037 1631 y Fp(~)1025 1641 y(M)t Fq(\))1085 1595 y Fb(\021)e(\020)1142 1641 y Fq(1)i(+)1213 1602 y Fb(X)1280 1641 y Fq(#\()1333 1631 y Fp(~)1331 1641 y(L)p Fq(\))1375 1595 y Fb(\021)-12 1721 y Fq(and)14 b(for)f(the)i(rhs)162 1833 y(#\()p Fp(N)246 1839 y Fm(u)266 1843 y Fe(1)284 1833 y Fl(f)p Fp(u;)348 1822 y(~)348 1833 y(L)387 1822 y(~)375 1833 y(M)415 1839 y Fm(v)435 1833 y Fl(f)p Fp(u;)499 1822 y(~)499 1833 y(L)o Fl(gg)o Fq(\))42 b(=)g(#\()p Fp(N)5 b Fq(\))811 1787 y Fb(\020)835 1833 y Fq(1)k(+)907 1793 y Fb(X)974 1833 y Fq(#\()1027 1822 y Fp(~)1025 1833 y(L)p Fq(\))g(+)1120 1793 y Fb(X)1186 1833 y Fq(#\()1250 1822 y Fp(~)1237 1833 y(M)1277 1839 y Fm(v)1297 1833 y Fl(f)p Fp(u;)1362 1822 y(~)1361 1833 y(L)o Fl(g)p Fq(\))1425 1787 y Fb(\021)625 1924 y Fq(=)42 b(#\()p Fp(N)5 b Fq(\))811 1878 y Fb(\020)835 1924 y Fq(1)k(+)907 1885 y Fb(X)974 1924 y Fq(#\()1027 1914 y Fp(~)1025 1924 y(L)p Fq(\))g(+)1120 1878 y Fb(\020)1144 1885 y(X)1211 1924 y Fq(#\()1274 1914 y Fp(~)1262 1924 y(M)c Fq(\))1323 1878 y Fb(\021)i(\020)1379 1924 y Fq(1)i(+)1451 1885 y Fb(X)1518 1924 y Fq(#\()1571 1914 y Fp(~)1569 1924 y(L)p Fq(\))1613 1878 y Fb(\021\021)1669 1924 y Fp(:)-12 2020 y Fq(So)14 b(in)f(this)h(case)h(the)g(lhs)e(equals)h(the) h(rhs.)38 2077 y(Among)d(the)j(cases)g(\(4\))f(and)f(\(5\))h(w)o(e)g (only)g(treat)g(\(5\))g(with)g Fp(w)e Fl(6)p Fq(=)g Fp(v)q Fq(.)18 b(W)m(e)c(obtain)f(for)h(the)g(lhs)57 2176 y Fp(\016)r Fq(\(\()p Fp(\025w)q(M)5 b Fq(\))225 2182 y Fm(v)245 2176 y Fl(f)p Fp(u;)309 2166 y(~)309 2176 y(L)o Fl(g)p Fq(\))11 b(=)h Fp(\016)r Fq(\()p Fp(\025w)q(M)5 b Fq(\))10 b(+)f(#\()p Fp(\025w)q(M)c Fq(\))805 2130 y Fb(\020)830 2176 y Fq(1)k(+)901 2137 y Fb(X)968 2176 y Fp(\016)r Fq(\()1006 2166 y Fp(~)1004 2176 y(L)p Fq(\))1048 2130 y Fb(\021)1085 2176 y Fq(=)j Fp(\016)r Fq(\()p Fp(M)5 b Fq(\))k(+)g(\()q(#\()p Fp(M)c Fq(\))j(+)i(1\))1499 2130 y Fb(\020)1524 2176 y Fq(1)f(+)1595 2137 y Fb(X)1662 2176 y Fp(\016)r Fq(\()1700 2166 y Fp(~)1698 2176 y(L)p Fq(\))1742 2130 y Fb(\021)1774 2176 y Fp(:)-12 2272 y Fq(F)m(or)14 b(the)g(rhs)h(w)o(e)f(ha)o(v)o(e)332 2358 y Fp(\016)r Fq(\()p Fp(\025w)q(:M)475 2364 y Fm(v)494 2358 y Fl(f)p Fp(u;)559 2348 y(~)558 2358 y(L)p Fl(g)o Fq(\))e(=)g Fp(\016)r Fq(\()p Fp(M)754 2364 y Fm(v)774 2358 y Fl(f)p Fp(u;)839 2348 y(~)838 2358 y(L)o Fl(g)p Fq(\))g(=)f Fp(\016)r Fq(\()p Fp(M)5 b Fq(\))10 b(+)f(#\()p Fp(M)c Fq(\))1224 2312 y Fb(\020)1249 2358 y Fq(1)k(+)1320 2319 y Fb(X)1387 2358 y Fp(\016)r Fq(\()1425 2348 y Fp(~)1423 2358 y(L)p Fq(\))1467 2312 y Fb(\021)1499 2358 y Fp(:)-12 2455 y Fq(So)14 b(again)f(the)h(lhs)g(is)g(greater)g(than)g(the)h(rhs.) k(Concerning)14 b(#)f(w)o(e)h(ha)o(v)o(e)g(for)f(the)i(lhs)219 2551 y(#\(\()p Fp(\025w)q(M)5 b Fq(\))402 2557 y Fm(v)422 2551 y Fl(f)p Fp(u;)487 2540 y(~)486 2551 y(L)o Fl(g)p Fq(\))12 b(=)g(#\()p Fp(\025w)q(M)5 b Fq(\))780 2505 y Fb(\020)804 2551 y Fq(1)k(+)875 2511 y Fb(X)942 2551 y Fq(#\()995 2540 y Fp(~)993 2551 y(L)p Fq(\))1037 2505 y Fb(\021)1074 2551 y Fq(=)j(\(#\()p Fp(M)5 b Fq(\))k(+)g(1\))1340 2505 y Fb(\020)1365 2551 y Fq(1)g(+)1436 2511 y Fb(X)1503 2551 y Fq(#\()1556 2540 y Fp(~)1554 2551 y(L)p Fq(\))1598 2505 y Fb(\021)-12 2647 y Fq(and)14 b(for)f(the)i(rhs)316 2733 y(#\()p Fp(\025w)q(:M)474 2739 y Fm(v)493 2733 y Fl(f)p Fp(u;)558 2723 y(~)557 2733 y(L)o Fl(g)p Fq(\))d(=)f(#\()p Fp(M)767 2739 y Fm(v)787 2733 y Fl(f)p Fp(u;)852 2723 y(~)851 2733 y(L)o Fl(g)p Fq(\))f(+)f(1)i(=)h(#\()p Fp(M)5 b Fq(\))1161 2687 y Fb(\020)1186 2733 y Fq(1)k(+)1257 2694 y Fb(X)1324 2733 y Fq(#\()1377 2723 y Fp(~)1375 2733 y(L)p Fq(\))1419 2687 y Fb(\021)1453 2733 y Fq(+)h(1)p Fp(:)-12 2829 y Fq(Again)j(the)i(lhs)f(is)f(greater)i(than)f(or)g (equal)f(to)h(the)h(rhs.)38 2886 y(F)m(or)e(the)i(inner)f(reductions)h (the)g(claim)c(follo)o(ws)i(imm)o(ediately)e(from)h(the)j (de\014nitions)f(of)f Fp(\016)j Fq(and)d(#.)145 b Fd(Qed)911 3042 y Fq(9)p eop %%Page: 10 10 10 9 bop -12 195 a Fo(3.5.)22 b Fd(Lemma.)28 b Fa(A)14 b(sequen)o(t)h(term)f(in)g(m)o(ultiary)d(normal)h(form)h(is)h Fp(\031)q Fq(-normal)e Fa(i\013)h(subterms)i(of)e(the)i(form)d Fp(M)1722 201 y Fm(v)1742 195 y Fl(f)p Fp(u;)1807 185 y(~)1806 195 y(L)p Fl(g)-12 245 y Fa(only)h(o)q(ccur)i(with)f Fp(M)i Fq(=)c Fp(v)q Fa(.)-12 321 y Fd(Pr)o(oof)p Fq(.)18 b(The)13 b(direction)f(from)f(righ)o(t)g(to)h(left)g(is)g(clear.)18 b(F)m(or)11 b(the)i(con)o(v)o(erse)g(let)g(a)e(sequen)o(t)j(term)d(in)h (m)o(ultiary)d(normal)-12 370 y(form)j(b)q(e)h(giv)o(en)g(and)g(assume) g(that)g(it)g(con)o(tains)g(a)g(subterm)g(of)f(the)i(form)d Fp(M)1213 376 y Fm(v)1233 370 y Fl(f)p Fp(u;)1298 360 y(~)1297 370 y(L)o Fl(g)i Fq(with)g Fp(M)j Fl(6)p Fq(=)c Fp(v)q Fq(,)i(where)g(w)o(e)f(ma)o(y)-12 420 y(assume)j(that)h Fp(M)k Fq(has)c(the)g(required)g(form.)24 b(Then)17 b Fp(M)k Fq(is)c(not)f(an)g(assumption)f(v)n(ariable)h(b)q(ecause)i(of)e (rule)g(\(1\))h(of)-12 470 y(de\014nition)g(3.1,)f(not)h(a)f(pair)h(b)q (ecause)h(of)f(\(4\))g(and)f(not)h(an)g(abstraction)g(b)q(ecause)i(of)d (\(5\).)27 b(So)17 b Fp(M)k Fq(is)c(of)g(the)g(form)-12 525 y Fp(w)18 531 y Fm(w)45 525 y Fl(f)p Fp(u)90 531 y Fn(1)108 525 y Fp(;)139 514 y(~)127 525 y(M)t Fl(g)d Fq(and)f(hence)j Fp(M)442 531 y Fm(v)462 525 y Fl(f)p Fp(u;)526 514 y(~)526 525 y(L)o Fl(g)e Fq(of)f(the)h(form)748 609 y Fp(w)778 615 y Fm(w)804 609 y Fl(f)p Fp(u)849 615 y Fn(1)868 609 y Fp(;)898 598 y(~)887 609 y(M)t Fl(g)952 621 y Fm(v)971 609 y Fl(f)p Fp(u;)1036 598 y(~)1035 609 y(L)o Fl(g)p Fp(:)-12 695 y Fj(Case)19 b Fp(u)118 701 y Fn(1)151 695 y Fl(6)p Fq(=)c Fp(v)q Fq(.)24 b(Reducibilit)o(y)15 b(follo)o(ws)f(from)g(\(1\))i(if)f Fp(v)21 b(=)-26 b Fl(2)14 b Fq(F)-5 b(A)q(\()998 685 y Fp(~)986 695 y(M)5 b Fq(\),)16 b(and)f(from)f(\(2\))i(if)f Fp(v)i Fl(2)d Fq(F)-5 b(A)q(\()1527 685 y Fp(~)1515 695 y(M)t Fq(\).)24 b Fj(Case)19 b Fp(u)1741 701 y Fn(1)1774 695 y Fq(=)c Fp(v)q Fq(.)-12 750 y(Then)j(w)o(e)g(ha)o(v)o(e)f Fp(v)i Fl(2)e Fq(F)-5 b(A)q(\()430 739 y Fp(~)418 750 y(M)5 b Fq(\),)18 b(since)g(w)o(e)g(only)e(consider)i(terms)g(in)f(m)o (ultiary)e(normal)g(form.)27 b(No)o(w)17 b(reducibilit)o(y)-12 800 y(follo)o(ws)12 b(from)h(\(3\).)1482 b Fd(Qed)-12 931 y Fo(3.6.)21 b Fd(Lemma.)39 1011 y Fa(1.)f(F)m(or)13 b(normal)f(deriv)n(ation)h(terms)h Fp(N)19 b Fa(w)o(e)14 b(ha)o(v)o(e)f Fp(F)6 b Fq(\()p Fp(G)p Fq(\()p Fp(N)f Fq(\)\))12 b(=)f Fp(N)5 b Fa(.)39 1089 y(2.)20 b(F)m(or)13 b Fp(\031)q Fa(-normal)f(sequen)o(t)j(terms)f Fp(L)g Fa(w)o(e)g(ha)o(v)o(e)g Fp(G)p Fq(\()p Fp(F)6 b Fq(\()p Fp(L)p Fq(\)\))11 b(=)h Fp(L)p Fa(.)39 1167 y(3.)20 b(If)13 b Fp(L)f Fl(\000)-6 b(!)241 1173 y Fm(\031)274 1167 y Fp(L)302 1152 y Fg(0)314 1167 y Fa(,)13 b(then)i Fp(F)6 b Fq(\()p Fp(L)p Fq(\))12 b(=)f Fp(F)6 b Fq(\()p Fp(L)659 1152 y Fg(0)671 1167 y Fq(\))p Fa(.)-12 1246 y Fd(Pr)o(oof)15 b Fq(1.)j(This)13 b(is)h(Lemma)d(2.5\(3\).)17 b(2.)h(Induction)c(on)g Fp(L)p Fq(,)f(using)h(Lemma)d(3.5;)i(for)g(instance)i(w)o(e)f(ha)o(v)o (e)550 1330 y Fp(G)p Fq(\()p Fp(F)6 b Fq(\()p Fp(u)672 1336 y Fm(u)693 1330 y Fl(f)p Fp(v)q(;)756 1320 y(~)754 1330 y(L)p Fl(g)p Fq(\)\))12 b(=)g Fp(G)p Fq(\()p Fp(v)q(F)6 b Fq(\()1012 1320 y Fp(~)1010 1330 y(L)p Fq(\)\))12 b(=)f Fp(u)1149 1336 y Fm(u)1171 1330 y Fl(f)p Fp(v)q(;)1233 1320 y(~)1232 1330 y(L)p Fl(g)p Fp(:)-12 1410 y Fq(3.)26 b(Induction)17 b(on)f(the)h(de\014nition)f(of)g Fp(L)g Fl(\000)-6 b(!)721 1416 y Fm(\031)759 1410 y Fp(L)787 1394 y Fg(0)799 1410 y Fq(.)26 b(The)17 b(p)q(erm)o(utativ)o(e)e(con)o (v)o(ersions)j(are)f(de\014ned)g(in)f(suc)o(h)i(a)e(w)o(a)o(y)-12 1459 y(that)e(execution)h(of)e(the)i(explicit)e(substitutions)h(pro)q (duces)i(iden)o(tities.)642 b Fd(Qed)-12 1591 y Fo(3.7.)21 b Fd(Cor)o(ollar)m(y.)29 b Fa(\(Dyc)o(kho\013)14 b(and)g(Pin)o(to)f ([1]\).)39 1670 y(1.)20 b(\(Uniqueness)e(of)d(normal)f(form\).)24 b(An)o(y)16 b(sequen)o(t)i(term)d Fp(L)i Fa(has)f(the)h(uniquely)f (determined)g Fp(\031)q Fa(-normal)e(form)92 1720 y Fp(G)p Fq(\()p Fp(F)6 b Fq(\()p Fp(L)p Fq(\)\))p Fa(.)39 1804 y(2.)20 b(\(Characterization)15 b(of)f Fl(\030)505 1810 y Fm(\031)528 1804 y Fa(\).)21 b(Let)15 b Fl(\030)684 1810 y Fm(\031)707 1804 y Fq(:=)780 1781 y Fg(\003)751 1804 y Fl( )-7 b(!)827 1810 y Fm(\031)849 1804 y Fa(,)15 b(i.e.)f(the)h(equiv)n(alence)g(relation)f(generated)i(b)o(y)f Fl(\000)-7 b(!)1705 1810 y Fm(\031)1727 1804 y Fa(.)21 b(Then)92 1854 y(w)o(e)14 b(ha)o(v)o(e)g Fp(L)277 1860 y Fn(1)307 1854 y Fl(\030)339 1860 y Fm(\031)374 1854 y Fp(L)402 1860 y Fn(2)434 1854 y Fa(i\013)g Fp(F)6 b Fq(\()p Fp(L)561 1860 y Fn(1)579 1854 y Fq(\))12 b(=)g Fp(F)6 b Fq(\()p Fp(L)728 1860 y Fn(2)746 1854 y Fq(\))p Fa(.)-12 1933 y Fd(Pr)o(oof)14 b Fq(1.)j(By)c(Theorem)g(3.4)e(w)o(e)i (can)g(construct)i(a)d Fp(\031)q Fq(-normal)f(form)g Fp(L)1139 1918 y Fg(\003)1171 1933 y Fq(of)h Fp(L)p Fq(.)18 b(Then)c(w)o(e)f(ha)o(v)o(e)f Fp(F)6 b Fq(\()p Fp(L)p Fq(\))12 b(=)g Fp(F)6 b Fq(\()p Fp(L)1763 1918 y Fg(\003)1782 1933 y Fq(\))13 b(b)o(y)-12 1983 y(Lemma)e(3.6\(3\),)i(hence)i Fp(G)p Fq(\()p Fp(F)6 b Fq(\()p Fp(L)p Fq(\)\))12 b(=)f Fp(G)p Fq(\()p Fp(F)6 b Fq(\()p Fp(L)722 1968 y Fg(\003)741 1983 y Fq(\)\))12 b(=)g Fp(L)857 1968 y Fg(\003)890 1983 y Fq(b)o(y)i(Lemma)d(3.6\(2\).)38 2045 y(2.)20 b(F)m(rom)13 b Fp(L)229 2051 y Fn(1)260 2045 y Fl(\030)292 2051 y Fm(\031)328 2045 y Fp(L)356 2051 y Fn(2)389 2045 y Fq(w)o(e)i(obtain)f Fp(F)6 b Fq(\()p Fp(L)658 2051 y Fn(1)677 2045 y Fq(\))12 b(=)h Fp(F)6 b Fq(\()p Fp(L)827 2051 y Fn(2)846 2045 y Fq(\))15 b(b)o(y)f(Lemma)e(3.6\(3\).)19 b(The)c(con)o(v)o(erse)h (follo)o(ws)d(from)g Fp(L)1738 2051 y Fm(i)1790 2021 y Fg(\003)1765 2045 y Fl(\000)-7 b(!)1832 2051 y Fm(\031)-12 2095 y Fp(G)p Fq(\()p Fp(F)6 b Fq(\()p Fp(L)114 2101 y Fm(i)128 2095 y Fq(\)\),)13 b(whic)o(h)h(holds)g(b)o(y)f(part)h(1.) 1177 b Fd(Qed)38 2170 y Fq(Finally)12 b(w)o(e)j(pro)o(v)o(e)f(a)g (conjecture)i(b)o(y)e(Dyc)o(kho\013)f(and)h(Pin)o(to)g([1)o(])g (concerning)h(termination)d(of)i(a)f(certain)i(v)o(ersion)-12 2220 y(of)e(the)h(p)q(erm)o(utativ)o(e)e(con)o(v)o(ersion)h(rules)h (\(2\))f(and)g(\(3\))g(considered)i(there.)k(In)13 b(these)i(rules)f (they)f(require)h(\(instead)g(of)-12 2275 y(our)f(restriction)h Fp(v)k(=)-26 b Fl(2)11 b Fq(F)-5 b(A)q(\()p Fp(N)5 b Fq(\)\))13 b(that)g Fp(N)18 b Fq(has)13 b(the)h(form)d(\()p Fp(w)911 2281 y Fn(1)930 2275 y Fq(\))946 2281 y Fm(w)970 2285 y Fe(1)988 2275 y Fl(f)p Fp(w)q(;)1067 2264 y(~)1059 2275 y(N)t Fl(g)i Fq(with)f Fp(w)17 b(=)-25 b Fl(2)11 b Fq(F)-5 b(A)q(\()1384 2264 y Fp(~)1375 2275 y(N)5 b Fq(\),)12 b(where)j(no)o(w)d Fp(v)h Fl(2)f Fq(F)-5 b(A\()1809 2264 y Fp(~)1800 2275 y(N)5 b Fq(\))-12 2325 y(is)14 b(allo)o(w)o(ed.)j(So)c(w)o(e)h(no)o(w)g(ha)o(v)o(e)g(instead)g(of)f (\(2\))h(and)g(\(3\))g(the)g(rules)148 2409 y(\()p Fp(w)194 2415 y Fn(1)213 2409 y Fq(\))229 2415 y Fm(w)253 2419 y Fe(1)271 2409 y Fl(f)p Fp(w)q(;)350 2398 y(~)342 2409 y(N)t Fl(g)400 2421 y Fm(w)427 2409 y Fl(f)p Fp(u)472 2415 y Fn(1)490 2409 y Fp(;)521 2398 y(~)509 2409 y(M)t Fl(g)574 2423 y Fm(v)594 2409 y Fl(f)p Fp(u;)658 2398 y(~)658 2409 y(L)o Fl(g)41 b(7!)789 2415 y Fm(\031)853 2409 y Fq(\()p Fp(w)899 2415 y Fn(1)917 2409 y Fq(\))933 2415 y Fm(w)957 2419 y Fe(1)976 2409 y Fl(f)p Fp(w)q(;)1054 2398 y(~)1047 2409 y(N)1080 2415 y Fm(v)1099 2409 y Fl(f)p Fp(u;)1163 2398 y(~)1163 2409 y(L)o Fl(gg)1231 2421 y Fm(w)1258 2409 y Fl(f)p Fp(u)1303 2415 y Fn(1)1321 2409 y Fp(;)1352 2398 y(~)1340 2409 y(M)1380 2415 y Fm(v)1400 2409 y Fl(f)p Fp(u;)1465 2398 y(~)1464 2409 y(L)o Fl(gg)p Fp(;)894 2480 y Fq(if)13 b Fp(u)956 2486 y Fn(1)986 2480 y Fl(6)p Fq(=)f Fp(v)q Fq(,)i Fp(w)j(=)-26 b Fl(2)11 b Fq(F)-5 b(A)q(\()1237 2470 y Fp(~)1228 2480 y(N)5 b Fq(\))14 b(and)g Fp(v)f Fl(2)e Fq(F)-5 b(A)q(\()1528 2470 y Fp(~)1519 2480 y(N)5 b(;)1588 2470 y(~)1576 2480 y(M)t Fq(\).)153 b(\(6\))169 2547 y(\()p Fp(w)215 2553 y Fn(1)234 2547 y Fq(\))250 2553 y Fm(w)274 2557 y Fe(1)292 2547 y Fl(f)p Fp(w)q(;)371 2537 y(~)363 2547 y(N)t Fl(g)421 2560 y Fm(w)448 2547 y Fl(f)p Fp(v)q(;)521 2537 y(~)509 2547 y(M)t Fl(g)574 2562 y Fm(v)594 2547 y Fl(f)p Fp(u;)658 2537 y(~)658 2547 y(L)o Fl(g)41 b(7!)789 2553 y Fm(\031)853 2547 y Fq(\()p Fp(w)899 2553 y Fn(1)917 2547 y Fq(\))933 2553 y Fm(w)957 2557 y Fe(1)976 2547 y Fl(f)p Fp(w)q(;)1054 2537 y(~)1047 2547 y(N)1080 2553 y Fm(v)1099 2547 y Fl(f)p Fp(u;)1163 2537 y(~)1163 2547 y(L)o Fl(gg)1231 2560 y Fm(w)1258 2547 y Fl(f)p Fp(v)1299 2553 y Fn(1)1318 2547 y Fp(;)1349 2537 y(~)1337 2547 y(M)1377 2553 y Fm(v)1396 2547 y Fl(f)p Fp(u;)1461 2537 y(~)1460 2547 y(L)o Fl(gg)1529 2562 y Fm(v)1546 2566 y Fe(1)1564 2547 y Fl(f)p Fp(u;)1629 2537 y(~)1628 2547 y(L)o Fl(g)p Fp(;)894 2623 y Fq(if)13 b Fp(w)k(=)-25 b Fl(2)11 b Fq(F)-5 b(A\()1092 2612 y Fp(~)1083 2623 y(N)5 b Fq(\))14 b(and)g Fp(v)f Fl(2)e Fq(F)-5 b(A)q(\()1383 2612 y Fp(~)1374 2623 y(N)5 b(;)1443 2612 y(~)1431 2623 y(M)t Fq(\).)298 b(\(7\))-12 2702 y(T)m(o)13 b(see)i(termination)e(w)o(e)h(form)e(the)i(m)o(ultiary)e (normal)g(forms)g(on)i(b)q(oth)g(sides.)59 2781 y(\()p Fp(w)105 2787 y Fn(1)123 2781 y Fq(\))139 2787 y Fm(w)163 2791 y Fe(1)182 2781 y Fl(f)p Fp(u)227 2787 y Fn(1)245 2781 y Fp(;)7 b(\026)p Fq(\()317 2771 y Fp(~)305 2781 y(M)358 2771 y(~)349 2781 y(N)e Fq(\))p Fl(g)424 2793 y Fm(v)444 2781 y Fl(f)p Fp(u;)i(\026)p Fq(\()551 2771 y Fp(~)549 2781 y(L)o Fq(\))p Fl(g)42 b(\000)-7 b(!)722 2787 y Fm(\031)786 2781 y Fq(\()p Fp(w)832 2787 y Fn(1)850 2781 y Fq(\))866 2787 y Fm(w)890 2791 y Fe(1)908 2781 y Fl(f)p Fp(u)953 2787 y Fn(1)972 2781 y Fp(;)7 b(\026)p Fq(\()1043 2771 y Fp(~)1032 2781 y(M)1072 2787 y Fm(v)1091 2781 y Fl(f)p Fp(u;)1156 2771 y(~)1155 2781 y(L)o Fl(g)1212 2771 y Fp(~)1203 2781 y(N)1236 2787 y Fm(v)1256 2781 y Fl(f)p Fp(u;)1321 2771 y(~)1320 2781 y(L)o Fl(g)p Fq(\))p Fl(g)p Fp(;)827 2850 y Fq(if)13 b Fp(u)889 2856 y Fn(1)919 2850 y Fl(6)p Fq(=)f Fp(v)j Fq(and)f Fp(v)f Fl(2)e Fq(F)-5 b(A)q(\()1230 2840 y Fp(~)1221 2850 y(N)5 b(;)1290 2840 y(~)1278 2850 y(M)t Fq(\).)80 2917 y(\()p Fp(w)126 2923 y Fn(1)144 2917 y Fq(\))160 2923 y Fm(w)184 2927 y Fe(1)203 2917 y Fl(f)p Fp(v)q(;)i(\026)p Fq(\()317 2907 y Fp(~)305 2917 y(M)358 2907 y(~)349 2917 y(N)e Fq(\))p Fl(g)424 2930 y Fm(v)444 2917 y Fl(f)p Fp(u;)i(\026)p Fq(\()551 2907 y Fp(~)549 2917 y(L)o Fq(\))p Fl(g)42 b(\000)-7 b(!)722 2923 y Fm(\031)786 2917 y Fq(\()p Fp(w)832 2923 y Fn(1)850 2917 y Fq(\))866 2923 y Fm(w)890 2927 y Fe(1)908 2917 y Fl(f)p Fp(u;)7 b(\026)p Fq(\()1015 2907 y Fp(~)1013 2917 y(L)1053 2907 y(~)1041 2917 y(M)1081 2923 y Fm(v)1101 2917 y Fl(f)p Fp(u;)1165 2907 y(~)1165 2917 y(L)o Fl(g)1222 2907 y Fp(~)1213 2917 y(N)1246 2923 y Fm(v)1266 2917 y Fl(f)p Fp(u;)1331 2907 y(~)1330 2917 y(L)o Fl(g)p Fq(\))p Fl(g)p Fp(;)48 b Fq(if)13 b Fp(v)g Fl(2)e Fq(F)-5 b(A)q(\()1664 2907 y Fp(~)1655 2917 y(N)5 b(;)1723 2907 y(~)1712 2917 y(M)t Fq(\).)901 3042 y(10)p eop %%Page: 11 11 11 10 bop -12 195 a Fq(Eac)o(h)15 b(time)f(w)o(e)h(reac)o(h)h(the)g (righ)o(t)e(hand)h(side)g(from)e(the)j(left)f(hand)g(side)g(b)o(y)g (\(2\))g(or)g(\(3\).)21 b(Hence,)16 b(as)f(sho)o(wn)g(ab)q(o)o(v)o(e,) -12 245 y(the)g Fp(\016)r Fq(-v)n(alues)e(decrease.)38 303 y(More)k(precisely)m(,)g(Dyc)o(kho\013)f(and)g(Pin)o(to)g(consider) h(a)f(sligh)o(tly)f(di\013eren)o(t)i(form)d(of)i(\(6\))g(and)g(\(7\),)h (where)g(instead)-12 358 y(of)i(\()p Fp(w)87 364 y Fn(1)106 358 y Fq(\))122 364 y Fm(w)146 368 y Fe(1)164 358 y Fl(f)p Fp(w)q(;)243 347 y(~)235 358 y(N)268 364 y Fm(v)287 358 y Fl(f)p Fp(u;)352 347 y(~)351 358 y(L)o Fl(gg)g Fq(they)i(still)d(ha)o (v)o(e)i(\()p Fp(w)773 364 y Fn(1)791 358 y Fq(\))807 364 y Fm(w)831 368 y Fe(1)849 358 y Fl(f)p Fp(w)q(;)928 347 y(~)920 358 y(N)t Fl(g)978 370 y Fm(v)998 358 y Fl(f)p Fp(u;)1063 347 y(~)1062 358 y(L)o Fl(g)f Fq(\(whic)o(h)h(b)q(ecause)h (of)e Fp(v)k Fl(6)p Fq(=)e Fp(w)q(;)7 b(w)1658 364 y Fn(1)1695 358 y Fq(could)20 b(b)q(e)-12 408 y(reduced)c(to)e(the)h (former\).)k(T)m(o)13 b(see)j(that)e(also)g(this)g(original)f(form)f (of)i(their)g(con)o(v)o(ersion)h(terminates)f(w)o(e)h(in)o(tro)q(duce) -12 457 y(y)o(et)j(another)g(simpli\014cation)d(relation)i Fl(\000)-7 b(!)700 463 y Fm(\033)722 457 y Fq(,)18 b(to)f(b)q(e)h (called)g Fp(\033)q Fq(-reduction)g(and)f(de\014ned)i(as)f(the)g(term)f (closure)h(of)-12 507 y(\()p Fp(w)34 513 y Fn(1)53 507 y Fq(\))69 513 y Fm(w)93 517 y Fe(1)111 507 y Fl(f)p Fp(w)q(;)190 497 y(~)182 507 y(N)t Fl(g)240 520 y Fm(v)260 507 y Fl(f)p Fp(u;)324 497 y(~)324 507 y(L)o Fl(g)c(7!)428 513 y Fm(\033)464 507 y Fq(\()p Fp(w)510 513 y Fn(1)529 507 y Fq(\))545 513 y Fm(w)569 517 y Fe(1)587 507 y Fl(f)p Fp(w)q(;)666 497 y(~)658 507 y(N)691 513 y Fm(v)710 507 y Fl(f)p Fp(u;)775 497 y(~)774 507 y(L)o Fl(gg)h Fq(for)h Fp(v)g Fl(6)p Fq(=)e Fp(w)q Fq(.)23 b(It)16 b(is)f(easy)i(to)e(see)i (that)e Fl(\000)-6 b(!)1536 513 y Fm(\033)1573 507 y Fq(terminates)16 b(\(the)-12 557 y(n)o(um)o(b)q(er)h(of)g(o)q (ccurrences)k(of)c(pairs)g(of)g(braces)i(of)e(the)h(form)e Fp(:)7 b(:)g(:)n Fl(g)g Fp(:)g(:)g(:)e Fl(f)p Fp(:)i(:)g(:)16 b Fq(decreases\),)21 b(that)c(the)i Fp(\033)q Fq(-normal)c(form)-12 607 y(is)g(unique)h(\(easy\))g(and)f(that)h(the)g Fp(\016)r Fq(-v)n(alues)f(decrease)i(under)g Fl(\000)-7 b(!)1051 613 y Fm(\033)1088 607 y Fq(\(easy)16 b(calculation\).)22 b(Then)16 b(in)f(an)o(y)g(reduction)-12 657 y(step)20 b(the)g Fp(\016)r Fq(-v)n(alues)f(of)f(the)i Fp(\033)q Fq(-normal)d(forms)g(decrease,)22 b(and)d(hence)i(w)o(e)e(ha)o(v)o(e)g (termination.)32 b({)19 b(Dyc)o(kho\013)f(and)-12 706 y(Pin)o(to)12 b(suggest)i(that)e Fp(\031)q Fq(-normalit)o(y)e(of)614 696 y Fp(~)605 706 y(N)5 b(;)674 696 y(~)662 706 y(M)t(;)726 696 y(~)725 706 y(L)13 b Fq(w)o(ould)e(b)q(e)i(su\016cien)o(t;)g(ho)o (w)o(ev)o(er,)g(this)g(is)f(far)g(to)q(o)h(strong)g(and)f(is)g(not)-12 756 y(necessary)k(for)e(termination.)-12 902 y Fk(References)-12 1001 y Fq([1])20 b(Ro)o(y)11 b(Dyc)o(kho\013)i(and)f(Luis)h(Pin)o(to.)i (P)o(erm)o(utabilit)o(y)c(of)h(pro)q(ofs)g(in)h(in)o(tuitionistic)e (sequen)o(t)j(calculi.)h(This)e(v)o(olume.)-12 1084 y([2])20 b(Hugo)15 b(Herb)q(elin.)25 b(A)16 b Fp(\025)p Fq(-calculus)g (structure)i(isomorphic)c(to)h(Gen)o(tzen-st)o(yle)i(sequen)o(t)g (calculus)f(structure.)26 b(In)53 1134 y(L.)16 b(P)o(ac)o(holski)h(and) g(J.)g(Tiuryn,)g(editors,)h Fj(Computer)f(Scienc)n(e)i(L)n(o)n(gic.)e (8th)h(Workshop,)i(CSL'94.)e(Kazimierz,)53 1184 y(Poland,)h(Septemb)n (er)g(1994)p Fq(,)f(v)o(olume)e(933)h(of)g Fj(LNCS)p Fq(,)g(pages)h(61{75.)d(Springer)j(V)m(erlag,)g(Berlin,)g(Heidelb)q (erg,)53 1233 y(New)c(Y)m(ork,)f(1995.)-12 1316 y([3])20 b(W.A.)e(Ho)o(w)o(ard.)33 b(The)19 b(form)o(ulae{as{t)o(yp)q(es)f (notion)g(of)g(construction.)35 b(In)19 b(J.P)m(.)f(Seldin)h(and)g (J.R.)f(Hindley)m(,)53 1366 y(editors,)i Fj(T)m(o)g(H.B.)f(Curry:)28 b(Essays)20 b(on)g(Combinatory)g(L)n(o)n(gic,)h(L)n(amb)n(da)f (Calculus)f(and)i(F)m(ormalism)p Fq(,)e(pages)53 1416 y(479{490.)11 b(Academic)j(Press,)h(1980.)-12 1499 y([4])20 b(Stephen)e(C.)f(Kleene.)29 b(P)o(erm)o(utabilit)o(y)15 b(of)i(inferences)i(in)d(Gen)o(tzen's)j(calculi)d(LK)i(and)f(LJ.)28 b(Memoirs)16 b(of)h(the)53 1549 y(American)c(Mathematical)f(So)q(ciet)o (y)i(No.)f(10,)g(pp.)h(1{26,)e(Pro)o(vidence,)i(1952.)-12 1632 y([5])20 b(Gregory)c(Min)o(ts.)24 b(Normal)14 b(forms)h(for)h (sequen)o(t)h(deriv)n(ations.)24 b(In)16 b(P)m(.)f(Odifreddi,)h (editor,)g Fj(Kr)n(eiseliana.)g(A)o(b)n(out)53 1682 y(and)f(A)o(r)n (ound)g(Ge)n(or)n(g)g(Kr)n(eisel)p Fq(,)d(pages)i(469{492.)e(A.K.)h(P)o (eters,)j(W)m(ellesley)m(,)c(Massac)o(h)o(usetts,)j(1996.)-12 1765 y([6])20 b(G.)14 b(P)o(ottinger.)21 b(Normalization)12 b(as)j(a)g(homomo)o(rphic)e(image)g(of)h(cut{elimination.)k Fj(A)o(nnals)f(of)e(Mathematic)n(al)53 1815 y(L)n(o)n(gic)p Fq(,)e(12:323{357,)e(1977.)-12 1898 y([7])20 b(Dag)11 b(Pra)o(witz.)16 b Fj(Natur)n(al)c(De)n(duction)p Fq(,)h(v)o(olume)e(3) h(of)f Fj(A)n(cta)j(Universitatis)e(Sto)n(ckholmiensis.)h(Sto)n(ckholm) h(Studies)53 1947 y(in)h(Philosophy)p Fq(.)j(Almqvist)12 b(&)i(Wiksell,)f(Sto)q(c)o(kholm,)e(1965.)-12 2030 y([8])20 b(Anne)14 b(S.)g(T)m(ro)q(elstra.)k(Marginalia)12 b(on)h(sequen)o(t)i (calculi.)j(T)m(o)13 b(app)q(ear)h(in)g(Studia)f(Logica.)-12 2114 y([9])20 b(J.)15 b(I.)g(Zuc)o(k)o(er.)23 b(The)16 b(corresp)q(ondence)j(b)q(et)o(w)o(een)d(cut{elimination)d(and)i (normalization)e(I,)i(I)q(I.)22 b Fj(A)o(nnals)17 b(of)f(Ma-)53 2163 y(thematic)n(al)e(L)n(o)n(gic)p Fq(,)f(7:1{156,)f(1974.)901 3042 y(11)p eop %%Trailer end userdict /end-hook known{end-hook}if %%EOF