%!PS-Adobe-2.0 %%Creator: dvips 5.526 Copyright 1986, 1994 Radical Eye Software %%Title: gcd3.dvi %%CreationDate: Wed May 29 13:00:06 1996 %%Pages: 12 %%PageOrder: Ascend %%BoundingBox: 0 0 596 842 %%EndComments %DVIPSCommandLine: /sw/tex/bin/Dvips gcd3.dvi %DVIPSParameters: dpi=300, comments removed %DVIPSSource: TeX output 1996.05.29:1256 %%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/turin95/gcd3.dvi) @start /Fa 7 116 df82 D<001FF80000FFFE0003F01F0007E03F800FC03F801F803F80 3F801F007F800E007F0000007F000000FF000000FF000000FF000000FF000000FF000000 FF000000FF0000007F0000007F0000007F8000003F8001C01F8001C00FC0038007E00700 03F01E0000FFFC00001FE0001A1B7E9A1F>99 D<003FE00001FFF80003F07E0007C01F00 0F801F801F800F803F800FC07F000FC07F0007C07F0007E0FF0007E0FF0007E0FFFFFFE0 FFFFFFE0FF000000FF000000FF0000007F0000007F0000007F0000003F8000E01F8000E0 0FC001C007E0038003F81F0000FFFE00001FF0001B1B7E9A20>101 D<0007F0003FFC00FE3E01F87F03F87F03F07F07F07F07F03E07F00007F00007F00007F0 0007F00007F00007F000FFFFC0FFFFC0FFFFC007F00007F00007F00007F00007F00007F0 0007F00007F00007F00007F00007F00007F00007F00007F00007F00007F00007F00007F0 0007F00007F00007F0007FFF807FFF807FFF80182A7EA915>I110 D114 D<03FE300FFFF01E03F03800F0700070F00070F00070F80070FC0000FF E0007FFE007FFF803FFFE01FFFF007FFF800FFF80003FC0000FC60007CE0003CF0003CF0 0038F80038FC0070FF01E0F7FFC0C1FF00161B7E9A1B>I E /Fb 27 120 df<387C7C7E3E0E0E0E1C1C38F8F0C0070E789B18>39 D<007000F001E003C007 800F001E001C00380038007000700070007000E000E000E000E000E000E000E000E00070 00700070007000380038001C001E000F00078003C001F000F000700C24799F18>I<6000 F00078003C001E000F000780038001C001C000E000E000E000E000700070007000700070 00700070007000E000E000E000E001C001C0038007800F001E003C007800F00060000C24 7C9F18>I<1C3E7E7F3F1F070E1E7CF860080C788518>44 D<7FFF00FFFF80FFFF807FFF 0011047D8F18>I<01F00007FC000FFE001F1F001C07003803807803C07001C07001C0E0 00E0E000E0E000E0E000E0E000E0E000E0E000E0E000E0E000E0F001E07001C07001C078 03C03803801C07001F1F000FFE0007FC0001F000131C7E9B18>48 D<01800380038007800F803F80FF80FB8043800380038003800380038003800380038003 8003800380038003800380038003807FFCFFFE7FFC0F1C7B9B18>I<03F0000FFE003FFF 007C0F807003C0E001C0F000E0F000E06000E00000E00000E00001C00001C00003C00007 80000F00001E00003C0000780000F00001E00007C0000F80001E00E03C00E07FFFE0FFFF E07FFFE0131C7E9B18>I<000300000780001F80003F00007E0001FC0003F00007E0001F C0003F00007E0000FC0000FC00007E00003F00001FC00007E00003F00001FC00007E0000 3F00001F8000078000030011187D9918>60 D<1FE0003FF8007FFC00781E00300E000007 0000070000FF0007FF001FFF007F0700780700E00700E00700E00700F00F00781F003FFF F01FFBF007E1F014147D9318>97 D<7E0000FE00007E00000E00000E00000E00000E0000 0E00000E3E000EFF800FFFC00FC1E00F80E00F00700E00700E00380E00380E00380E0038 0E00380E00380F00700F00700F80E00FC1E00FFFC00EFF80063E00151C809B18>I<01FE 0007FF001FFF803E0780380300700000700000E00000E00000E00000E00000E00000E000 007000007001C03801C03E03C01FFF8007FF0001FC0012147D9318>I<001F80003F8000 1F8000038000038000038000038000038003E3800FFB801FFF803C1F80380F8070078070 0380E00380E00380E00380E00380E00380E00380700780700780380F803C1F801FFFF00F FBF803E3F0151C7E9B18>I<01F00007FC001FFE003E0F00380780700380700380E001C0 E001C0FFFFC0FFFFC0FFFFC0E000007000007001C03801C03E03C01FFF8007FF0001FC00 12147D9318>I<001F80007FC000FFE000E1E001C0C001C00001C00001C0007FFFC0FFFF C0FFFFC001C00001C00001C00001C00001C00001C00001C00001C00001C00001C00001C0 0001C00001C00001C0007FFF007FFF007FFF00131C7F9B18>I<03800007C00007C00007 C0000380000000000000000000000000007FC000FFC0007FC00001C00001C00001C00001 C00001C00001C00001C00001C00001C00001C00001C00001C00001C00001C000FFFF00FF FF80FFFF00111D7C9C18>105 D107 D<7FE000FFE0007FE00000E00000E00000E00000E00000E00000E00000E00000E00000E0 0000E00000E00000E00000E00000E00000E00000E00000E00000E00000E00000E00000E0 0000E0007FFFC0FFFFE07FFFC0131C7E9B18>I<7CE0E000FFFBF8007FFFF8001F1F1C00 1E1E1C001E1E1C001C1C1C001C1C1C001C1C1C001C1C1C001C1C1C001C1C1C001C1C1C00 1C1C1C001C1C1C001C1C1C001C1C1C007F1F1F00FFBFBF807F1F1F001914819318>I<7E 3E00FEFF807FFFC00FC1C00F80E00F00E00E00E00E00E00E00E00E00E00E00E00E00E00E 00E00E00E00E00E00E00E00E00E07FC3FCFFE7FE7FC3FC1714809318>I<01F0000FFE00 1FFF003E0F803803807001C07001C0E000E0E000E0E000E0E000E0E000E0F001E07001C0 7803C03C07803E0F801FFF000FFE0001F00013147E9318>I<7E3E00FEFF807FFFC00FC1 E00F80E00F00700E00700E00380E00380E00380E00380E00380E00380F00700F00700F80 E00FC1E00FFFC00EFF800E3E000E00000E00000E00000E00000E00000E00000E00007FC0 00FFE0007FC000151E809318>I<7F87E0FF9FF07FBFF803F87803F03003E00003C00003 C0000380000380000380000380000380000380000380000380000380007FFE00FFFF007F FE0015147F9318>114 D<07F7003FFF007FFF00780F00E00700E00700E007007C00007F E0001FFC0003FE00001F00600780E00380E00380F00380F80F00FFFF00FFFC00E7F00011 147D9318>I<0180000380000380000380000380007FFFC0FFFFC0FFFFC0038000038000 0380000380000380000380000380000380000380000380400380E00380E00380E001C1C0 01FFC000FF80003E0013197F9818>I<7E07E0FE0FE07E07E00E00E00E00E00E00E00E00 E00E00E00E00E00E00E00E00E00E00E00E00E00E00E00E00E00E01E00F03E007FFFC03FF FE01FCFC1714809318>I119 D E /Fc 2 51 df<0C003C00CC000C000C000C000C000C000C000C000C 000C000C000C000C00FF8009107E8F0F>49 D<1F00618040C08060C0600060006000C001 80030006000C00102020207FC0FFC00B107F8F0F>I E /Fd 3 111 df<000400000E00000E0000160000260000260000460000870000830001030003FF0002 0300040300080300080180100180FC0FE013117E9017>65 D<040C000000000070589898 3030606464683006127E910B>105 D<71F09A189C189818181830303030303230626064 60380F0B7E8A13>110 D E /Fe 9 107 df0 D<60F0F06004047D890A>I<020002000200C218F2783AE00F800F803AE0F278C2180200 020002000D0E7E8E12>3 D<0000010000000080000000800000004000000020FFFFFFFC FFFFFFFC00000020000000400000008000000080000001001E0C7E8D23>33 D<060F0F0E1E1E1C3C383830707060E0C04008117F910A>48 D<0003000300060006000C 000C00180018003000300060006000C000C00180018003000300060006000C000C001800 18003000300060006000C0004000101E7B9600>54 D<400010C000306000606000606000 603000C03000C01801801FFF800FFF000C03000C0300060600060600030C00030C000198 0001980001980000F00000F0000060000060001417809615>56 D<002000006000006000 006000006000006000006000006000006000006000006000006000006000006000006000 006000006000006000006000006000FFFFF8FFFFF815167D951B>63 D106 D E /Ff 5 126 df<0000700001F00003C0000780000E00001C0000380000 700000700000F00000E00000E00000E00000E00000E00000E00000E00000E00000E00000 E00000E00000E00000E00000E00000E00000E00000E00000E00000E00000E00000E00000 E00000E00000E00000E00000E00000E00000E00000E00000E00001C00001C00001C00003 80000700000600000E0000380000700000C000007000003800000E000006000007000003 800001C00001C00001C00000E00000E00000E00000E00000E00000E00000E00000E00000 E00000E00000E00000E00000E00000E00000E00000E00000E00000E00000E00000E00000 E00000E00000E00000E00000E00000E00000E00000E00000E00000E00000F00000700000 7000003800001C00000E000007800003C00001F000007014637B811F>26 D<0001F8000FF8003FF800FFF801FFF803FE0007E0000F80001E00003800007000006000 00E00000C00000150E818413>122 DII<0000180000380000300000700000E00003C0000F80003F0003FE00FFFC00 FFF800FFE000FF8000FC0000150E818D13>I E /Fg 21 127 df<07C0000C3040101040 201880601880C00C80C00D00C00E00800E00800C00C01C00C02C0060C4803F0300120E7E 8D17>11 D<000F0000308000C0C00080400100600200C00400C0040080040180083F0008 3E00080100080180100180100180100180100180300300300300300600280C0044180043 E000400000400000800000800000800000800000131D7F9614>I<383C44C6470246028E 060C060C060C06180C180C180C180C301830180018001800300030003000200F147F8D12 >17 D<0402000C06000C06000C0600180C00180C00180C00180C00301800301880301880 3038807859006F8E00600000600000C00000C00000C0000080000011147E8D15>22 D<60F0F070101020204040040A7D830A>59 D<0000300000F00003C0000700001C000078 0001E0000780000E0000380000F00000F000003800000E000007800001E000007800001C 000007000003C00000F000003014167D921B>I<0000C00000C00001C00001C00003C000 05C00005E00008E00008E00010E00020E00020E00040E000C0E00080E001FFF001007002 0070040070040070080070180070FE03FE17177F961A>65 D<07FFF800E00E00E00700E0 0300E00301C00301C00701C00701C00E03803C03FFF003FFF003803C07001C07000E0700 0E07000E0E001C0E001C0E00380E00701C01E0FFFF0018177F961B>I<07F007F800F000 C000B8008000B80080009C0080011C0100011E0100010E0100010E010002070200020702 0002038200020382000401C4000401C4000400E4000400E4000800780008007800080038 000800380018001000FE0010001D177F961C>78 D<003000480088018801080310021006 1006200C400C400C800D001A001A001C0018001800780088000810046003800D1780960E >96 D<071018F0307060706060C060C060C06080C080C480C4C1C446C838700E0E7E8D13 >I<07C00C20107020706000C000C000C00080008000C010C02060C03F000C0E7E8D0F> 99 D<0300038003000000000000000000000000001C002400460046008C000C00180018 00180031003100320032001C0009177F960C>105 D<1F0006000600060006000C000C00 0C000C00181C1866188E190C32003C003F00318060C060C460C460C8C0C8C0700F177E96 12>107 D<383C1E0044C6630047028100460301008E0703000C0603000C0603000C0606 00180C0600180C0620180C0C20180C0C4030180440301807801B0E7F8D1F>109 D<383C0044C6004702004602008E06000C06000C06000C0C00180C00180C401818401818 80300880300F00120E7F8D15>I<071018D0307060706060C060C060C06080C080C080C0 C1C047803980018001800300030003001FC00C147E8D10>113 D<38F04518463846308C 000C000C000C001800180018001800300030000D0E7F8D10>I<1C020026060046060046 0600860C000C0C000C0C000C0C001818001818801818801838800C5900078E00110E7F8D 14>117 D<1C04260E4606460686040C040C040C0418081808181018100C6007800F0E7F 8D11>I<002000300030FFFCFFFC007000E000400E08799712>126 D E /Fh 47 124 df<0E1F3F3F1D0102020404081020C0080E779F0E>39 D<1C3C3C3C3C040408081020204080060E7D840E>44 D<7FF0FFE07FE00C037D8A10>I< 70F8F8F0E005057B840E>I<000200020006000E003C00DC031C001C0038003800380038 007000700070007000E000E000E000E001C001C001C001C003800380038003800780FFF8 0F1E7B9D17>49 D<0000600000E00000E00000E00001C00001C00001C000038000038000 0300000700000700000600000E00000C0000180000180000300000300000630000C70000 8700010700030700060E00040E00080E003F8E00607C00801FC0001C00001C0000380000 380000380000380000700000700000600013277E9D17>52 D<001F0000718000C0C00180 C00380E00700E00F00E00F01E01E01E01E01E01E01E01E01C01C03C01C03C01C03C01C07 C01C0F800C0F8006378003C700000F00000E00000E00001C00601C00F03800F07000E060 0080C0004380003E0000131F7B9D17>57 D<070F1F1F0E0000000000000000000070F8F8 F0E008147B930E>I<00000200000006000000060000000E0000001E0000001E0000003F 0000002F0000004F0000004F0000008F0000010F0000010F0000020F0000020F0000040F 00000C0F0000080F0000100F0000100F0000200F80003FFF800040078000C00780008007 8001000780010007800200078002000780060007801E000F80FF807FF81D207E9F22>65 D<01FFFFC0001E00F0001E0078001E0038001E003C003C003C003C003C003C003C003C00 3C0078007800780078007800F0007801E000F0078000FFFE0000F00F8000F003C001E001 C001E001E001E001E001E001E003C001E003C001E003C001E003C001C0078003C0078007 8007800F0007801E000F007800FFFFE0001E1F7D9E20>I<0000FE0200078186001C004C 0038003C0060003C00C0001C01C0001803800018070000180F0000181E0000101E000010 3C0000003C00000078000000780000007800000078000000F0000000F0000000F0000000 F0000000F00000807000008070000080700001003800010038000200180004000C001800 060020000381C00000FE00001F217A9F21>I<01FFFFFC001E0038001E0018001E000800 1E0008003C0008003C0008003C0008003C00080078001000780800007808000078080000 F0100000F0300000FFF00000F0300001E0200001E0200001E0200001E0200003C0000003 C0000003C0000003C00000078000000780000007800000078000000F800000FFF800001E 1F7D9E1E>70 D<01FFF3FFE0001F003E00001E003C00001E003C00001E003C00003C0078 00003C007800003C007800003C007800007800F000007800F000007800F000007800F000 00F001E00000FFFFE00000F001E00000F001E00001E003C00001E003C00001E003C00001 E003C00003C007800003C007800003C007800003C007800007800F000007800F00000780 0F000007800F00000F801F0000FFF1FFE000231F7D9E22>72 D<01FFF0001F00001E0000 1E00001E00003C00003C00003C00003C0000780000780000780000780000F00000F00000 F00000F00001E00001E00001E00001E00003C00003C00003C00003C00007800007800007 80000780000F8000FFF800141F7D9E12>I<01FFF800001F0000001E0000001E0000001E 0000003C0000003C0000003C0000003C00000078000000780000007800000078000000F0 000000F0000000F0000000F0000001E0000001E0000001E0000001E0008003C0010003C0 010003C0030003C00200078006000780060007800C0007801C000F007800FFFFF800191F 7D9E1D>76 D<01FE00007FC0001E0000FC00001E0000F800001700017800001700017800 00270002F00000270004F00000270004F00000270008F00000470009E00000470011E000 00470021E00000470021E00000870043C00000838043C00000838083C00000838083C000 0103810780000103820780000103820780000103840780000203840F00000203880F0000 0203900F00000203900F00000401E01E00000401E01E00000401C01E00000C01801E0000 1C01803E0000FF8103FFC0002A1F7D9E29>I<01FF007FE0001F000F00001F0004000017 800400001780040000278008000023C008000023C008000023C008000041E010000041E0 10000041F010000040F010000080F0200000807820000080782000008078200001003C40 0001003C400001003C400001001E400002001E800002001E800002000F800002000F8000 04000F0000040007000004000700000C000700001C00020000FF80020000231F7D9E22> I<0001FC0000070700001C01C0003000E000E0006001C000700380007007800038070000 380E0000381E0000381C0000383C0000383C000038780000787800007878000078780000 78F00000F0F00000F0F00000E0F00001E0F00001C0F00003C0700003807000070078000F 0038001E0038003C001C0070000E00E0000783800001FC00001D217A9F23>I<01FFFF80 001E00E0001E0070001E0038001E003C003C003C003C003C003C003C003C003C00780078 00780078007800F0007800E000F003C000F00F0000FFFC0000F0000001E0000001E00000 01E0000001E0000003C0000003C0000003C0000003C00000078000000780000007800000 078000000F800000FFF000001E1F7D9E1F>I<01FFFF00001E03C0001E00E0001E007000 1E0078003C0078003C0078003C0078003C0078007800F0007800F0007801E0007801C000 F0070000F01E0000FFF00000F0380001E01C0001E01E0001E00E0001E00F0003C01E0003 C01E0003C01E0003C01E0007803C0007803C0807803C0807803C100F801C10FFF00C2000 0007C01D207D9E21>82 D<0007E040001C18C0003005800060038000C0038001C0018001 8001000380010003800100038001000380000003C0000003C0000003F8000001FF800001 FFE000007FF000001FF0000001F800000078000000780000003800000038002000380020 0038002000300060007000600060006000E0007000C000E8038000C606000081F800001A 217D9F1A>I<0FFFFFF01E0780E0180780201007802020078020200F0020600F0020400F 0020400F0020801E0040001E0000001E0000001E0000003C0000003C0000003C0000003C 00000078000000780000007800000078000000F0000000F0000000F0000000F0000001E0 000001E0000001E0000001E0000003E00000FFFF00001C1F789E21>I<7FFC1FF807C003 C00780010007800100078001000F0002000F0002000F0002000F0002001E0004001E0004 001E0004001E0004003C0008003C0008003C0008003C0008007800100078001000780010 0078001000F0002000F0002000F0002000F0004000F00040007000800070010000300200 00380400000C18000007E000001D20779E22>I87 D<00F1800389C00707800E03801C03803C0380380700780700780700780700F00E 00F00E00F00E00F00E20F01C40F01C40703C40705C40308C800F070013147C9317>97 D<07803F8007000700070007000E000E000E000E001C001C001CF01D0C3A0E3C0E380F38 0F700F700F700F700FE01EE01EE01EE01CE03CE038607060E031C01F0010207B9F15>I< 007E0001C1000300800E07801E07801C07003C0200780000780000780000F00000F00000 F00000F00000F0000070010070020030040018380007C00011147C9315>I<0000780003 F80000700000700000700000700000E00000E00000E00000E00001C00001C000F1C00389 C00707800E03801C03803C0380380700780700780700780700F00E00F00E00F00E00F00E 20F01C40F01C40703C40705C40308C800F070015207C9F17>I<007C01C207010E011C01 3C013802780C7BF07C00F000F000F000F0007000700170023804183807C010147C9315> I<00007800019C00033C00033C000718000700000700000E00000E00000E00000E00000E 0001FFE0001C00001C00001C00001C000038000038000038000038000038000070000070 0000700000700000700000700000E00000E00000E00000E00000C00001C00001C0000180 003180007B0000F300006600003C00001629829F0E>I<003C6000E27001C1E00380E007 00E00F00E00E01C01E01C01E01C01E01C03C03803C03803C03803C03803C07003C07001C 0F001C17000C2E0003CE00000E00000E00001C00001C00301C00783800F0700060E0003F 8000141D7E9315>I<01E0000FE00001C00001C00001C00001C000038000038000038000 038000070000070000071E000763000E81800F01C00E01C00E01C01C03801C03801C0380 1C0380380700380700380700380E10700E20700C20701C20700C40E00CC060070014207D 9F17>I<00C001E001E001C000000000000000000000000000000E003300230043804300 470087000E000E000E001C001C001C003840388030807080310033001C000B1F7C9E0E> I<01E0000FE00001C00001C00001C00001C0000380000380000380000380000700000700 000703C00704200E08E00E11E00E21E00E40C01C80001D00001E00001FC00038E0003870 00387000383840707080707080707080703100E03100601E0013207D9F15>107 D<03C01FC0038003800380038007000700070007000E000E000E000E001C001C001C001C 0038003800380038007000700070007100E200E200E200E200640038000A207C9F0C>I< 1C0F80F0002630C318004740640C004780680E004700700E004700700E008E00E01C000E 00E01C000E00E01C000E00E01C001C01C038001C01C038001C01C038001C01C070803803 8071003803806100380380E10038038062007007006600300300380021147C9325>I<1C 0F802630C04740604780604700704700708E00E00E00E00E00E00E00E01C01C01C01C01C 01C01C03843803883803083807083803107003303001C016147C931A>I<007C0001C300 0301800E01C01E01C01C01E03C01E07801E07801E07801E0F003C0F003C0F003C0F00780 F00700700F00700E0030180018700007C00013147C9317>I<01C1E002621804741C0478 1C04701E04701E08E01E00E01E00E01E00E01E01C03C01C03C01C03C01C0380380780380 700380E003C1C0072380071E000700000700000E00000E00000E00000E00001C00001C00 00FFC000171D809317>I<1C1E002661004783804787804707804703008E00000E00000E 00000E00001C00001C00001C00001C000038000038000038000038000070000030000011 147C9313>114 D<00FC030206010C030C070C060C000F800FF007F803FC003E000E700E F00CF00CE008401020601F8010147D9313>I<018001C0038003800380038007000700FF F007000E000E000E000E001C001C001C001C003800380038003820704070407080708031 001E000C1C7C9B0F>I<0E00C03300E02301C04381C04301C04701C08703800E03800E03 800E03801C07001C07001C07001C07101C0E20180E20180E201C1E200C264007C3801414 7C9318>I<0E03803307802307C04383C04301C04700C08700800E00800E00800E00801C 01001C01001C01001C02001C02001C04001C04001C08000E300003C00012147C9315>I< 0383800CC4401068E01071E02071E02070C040E00000E00000E00000E00001C00001C000 01C00001C040638080F38080F38100E5810084C60078780013147D9315>120 D<0E00C03300E02301C04381C04301C04701C08703800E03800E03800E03801C07001C07 001C07001C07001C0E00180E00180E001C1E000C3C0007DC00001C00001C00003800F038 00F07000E06000C0C0004380003E0000131D7C9316>I123 D E /Fi 34 124 df<000FE000007FF80000F81C0001E07C0003E07C0007C07C0007C07C 0007C0380007C0000007C0000007C0000007C1FE00FFFFFE00FFFFFE0007C03E0007C03E 0007C03E0007C03E0007C03E0007C03E0007C03E0007C03E0007C03E0007C03E0007C03E 0007C03E0007C03E0007C03E0007C03E0007C03E003FF9FFC03FF9FFC01A20809F1D>12 D45 D<387CFEFEFE7C3807077C860F>I<0000E00000 0000E000000001F000000001F000000001F000000003F800000003F800000006FC000000 06FC0000000EFE0000000C7E0000000C7E000000183F000000183F000000303F80000030 1F800000701FC00000600FC00000600FC00000C007E00000FFFFE00001FFFFF000018003 F000018003F000030001F800030001F800060001FC00060000FC000E0000FE00FFE00FFF E0FFE00FFFE0231F7E9E28>65 D<0007FC02003FFF0E00FE03DE03F000FE07E0003E0FC0 001E1F80001E3F00000E3F00000E7F0000067E0000067E000006FE000000FE000000FE00 0000FE000000FE000000FE000000FE0000007E0000007E0000067F0000063F0000063F00 000C1F80000C0FC0001807E0003803F0007000FE01C0003FFF800007FC001F1F7D9E26> 67 DI70 D73 D78 D<7FFFFFFC7FFFFFFC7C07 E07C7007E01C6007E00C6007E00CE007E00EC007E006C007E006C007E006C007E0060007 E0000007E0000007E0000007E0000007E0000007E0000007E0000007E0000007E0000007 E0000007E0000007E0000007E0000007E0000007E0000007E0000007E00003FFFFC003FF FFC01F1E7E9D24>84 D<07FC001FFF003F0F803F07C03F03E03F03E00C03E00003E0007F E007FBE01F03E03C03E07C03E0F803E0F803E0F803E0FC05E07E0DE03FF8FE0FE07E1714 7F9319>97 D I<01FE0007FF801F0FC03E0FC03E0FC07C0FC07C0300FC0000FC0000FC0000FC0000FC00 00FC00007C00007E00003E00603F00C01F81C007FF0001FC0013147E9317>I<0007F800 07F80000F80000F80000F80000F80000F80000F80000F80000F80000F80000F801F8F80F FEF81F83F83E01F87E00F87C00F87C00F8FC00F8FC00F8FC00F8FC00F8FC00F8FC00F87C 00F87C00F87E00F83E01F81F07F80FFEFF03F8FF18207E9F1D>I<01FE0007FF800F83C0 1E01E03E00F07C00F07C00F8FC00F8FFFFF8FFFFF8FC0000FC0000FC00007C00007C0000 3E00181E00180F807007FFE000FF8015147F9318>I<001F8000FFC001F3E003E7E003C7 E007C7E007C3C007C00007C00007C00007C00007C000FFFC00FFFC0007C00007C00007C0 0007C00007C00007C00007C00007C00007C00007C00007C00007C00007C00007C00007C0 0007C0003FFC003FFC0013207F9F10>I<01FC3C07FFFE0F079E1E03DE3E03E03E03E03E 03E03E03E03E03E01E03C00F07800FFF0009FC001800001800001C00001FFF800FFFF007 FFF81FFFFC3C007C70003EF0001EF0001EF0001E78003C78003C3F01F80FFFE001FF0017 1E7F931A>I I<1C003E007F007F007F003E001C00000000000000000000000000FF00FF001F001F001F 001F001F001F001F001F001F001F001F001F001F001F001F001F00FFE0FFE00B217EA00E >I107 DI< FE0FE03F80FE1FF07FC01E70F9C3E01E407D01F01E807E01F01F807E01F01F007C01F01F 007C01F01F007C01F01F007C01F01F007C01F01F007C01F01F007C01F01F007C01F01F00 7C01F01F007C01F01F007C01F01F007C01F0FFE3FF8FFEFFE3FF8FFE27147D932C>II<01FF0007FFC0 1F83F03E00F83E00F87C007C7C007CFC007EFC007EFC007EFC007EFC007EFC007E7C007C 7C007C3E00F83E00F81F83F007FFC001FF0017147F931A>II114 D<0FE63FFE701E600EE006E006F800FFC07FF83FFC1FFE03FE001FC007 C007E007F006F81EFFFCC7F010147E9315>I<01800180018003800380038007800F803F 80FFFCFFFC0F800F800F800F800F800F800F800F800F800F800F860F860F860F860F8607 CC03F801F00F1D7F9C14>IIIII< FFE07F80FFE07F801F001C000F8018000F80180007C0300007C0300003E0600003E06000 01F0C00001F0C00001F9C00000F9800000FF8000007F0000007F0000003E0000003E0000 001C0000001C0000001800000018000078300000FC300000FC600000C0E00000E1C00000 7F8000001E000000191D7F931C>I123 D E /Fj 15 107 df0 D<70F8F8F87005057C8D0D>I< 01800180018001800180C183F18F399C0FF003C003C00FF0399CF18FC183018001800180 0180018010147D9417>3 D<000200000006000000060000000600000006000000060000 000600000006000000060000000600000006000000060000000600000006000000060000 FFFFFFF0FFFFFFF000060000000600000006000000060000000600000006000000060000 000600000006000000060000000600000006000000060000FFFFFFF0FFFFFFF01C207D9E 23>6 D17 D<00000004000000000200000000020000 00000100000000008000000000400000000020FFFFFFFFFCFFFFFFFFFC00000000200000 0000400000000080000000010000000002000000000200000000040026107D922D>33 D<003FF800FFF803C0000700000C0000180000300000300000600000600000C00000C000 00C00000FFFFF8FFFFF8C00000C00000C000006000006000003000003000001800000C00 0007000003C00000FFF8003FF8151C7C981E>50 D<00000C00000C000018000018000030 0000300000600000600000C00000C0000180000180000180000300000300000600000600 000C00000C0000180000180000300000300000600000600000C00000C000018000018000 0300000300000600000600000600000C00000C0000180000180000300000300000600000 600000C00000400000162C7AA000>54 D<400001C0000360000660000660000630000C30 000C30000C1800181800181800180FFFF00FFFF00C00300600600600600600600300C003 00C001818001818001818000C30000C30000C300006600006600006600003C00003C0000 3C000018000018001821809F19>56 DI<00040000000C0000000C0000000C0000000C0000000C000000 0C0000000C0000000C0000000C0000000C0000000C0000000C0000000C0000000C000000 0C0000000C0000000C0000000C0000000C0000000C0000000C0000000C0000000C000000 0C0000000C0000FFFFFFE0FFFFFFE01B1C7C9B23>63 D<001000003800003800006C0000 6C00006C0000C60000C6000183000183000183000301800301800600C00600C00600C00C 00600C006018003018003018003030001830001860000C60000C60000CC00006C0000217 1C7D9A1E>94 D<000F0038006000E001C001C001C001C001C001C001C001C001C001C001 C001C001C001C001C0038007001E00F8001E000700038001C001C001C001C001C001C001 C001C001C001C001C001C001C001C001C000E000600038000F102D7DA117>102 DI106 D E /Fk 28 119 df<0102040C1818303070606060E0E0E0E0E0E0E0E0 E0E060606070303018180C04020108227D980E>40 D<8040203018180C0C0E0606060707 07070707070707070606060E0C0C18183020408008227E980E>I<003000003000003000 003000003000003000003000003000003000003000003000FFFFFCFFFFFC003000003000 00300000300000300000300000300000300000300000300000300016187E931B>43 D<07C018303018701C600C600CE00EE00EE00EE00EE00EE00EE00EE00EE00E600C600C70 1C30181C7007C00F157F9412>48 D<03000700FF00070007000700070007000700070007 000700070007000700070007000700070007007FF00C157E9412>I<0F8030E040708030 C038E0384038003800700070006000C00180030006000C08080810183FF07FF0FFF00D15 7E9412>I<0FE030306018701C701C001C00180038006007E000300018000C000E000EE0 0EE00EC00C401830300FE00F157F9412>I<00300030007000F001F00170027004700870 1870107020704070C070FFFE0070007000700070007003FE0F157F9412>I<20303FE03F C0240020002000200020002F8030E020700030003800384038E038E0388030406020C01F 000D157E9412>I<01F00608080C181C301C70006000E000E3E0EC30F018F00CE00EE00E E00E600E600E300C3018183007C00F157F9412>I<40007FFE7FFC7FF8C0088010802000 40008000800100010003000200060006000E000E000E000E000E0004000F167E9512>I< 07E018302018600C600C700C78183E101F600FC00FF018F8607C601EC00EC006C006C004 600C38300FE00F157F9412>I<07C0183030186018E00CE00CE00EE00EE00E601E301E18 6E0F8E000E000C001C70187018603020C01F800F157F9412>I61 D80 D<1FC0386038301038003803F81E3830387038E039E039E07970FF1F1E100E 7F8D12>97 DI<007E00000E00000E00000E00000E00000E00000E00000E00000E 0007CE001C3E00300E00700E00600E00E00E00E00E00E00E00E00E00600E00700E00301E 00182E0007CFC012177F9614>100 D<0FC0186030307038E018FFF8E000E000E0006000 70083010183007C00D0E7F8D10>I<0F9E18E33060707070707070306018C02F80200060 003FE03FF83FFC600EC006C006C006600C38380FE010157F8D12>103 D<183C3C1800000000007C1C1C1C1C1C1C1C1C1C1C1C1CFF081780960A>105 D110 D<07C018303018600C600CE00EE00EE00EE00EE00E 701C3018183007C00F0E7F8D12>II114 D<1F4060C0C040C040E000FF007F801FC001E080608060C060E0 C09F000B0E7F8D0E>I<080008000800180018003800FF80380038003800380038003800 380038403840384038401C800F000A147F930E>I118 D E /Fl 45 127 df<07000001C00000E00000E00000F000007000007000007800003800003800003C0000 1C00001C00001E00000E00000E00000F00000700000F0000378000638000C38001C3C003 81C00701C00E01E01C00E03800E07000F0F00070E00070C0003815207D9F1B>21 D<01801801C01C0380380380380380380380380700700700700700700700700E00E00E00 E00E00E00E00E11E01C21E01C21E03C21E05C43F08C439F0783800003800007000007000 00700000700000E00000E00000E00000C00000181E7F931B>I<000F800038C000606000 C07001C0700380780380780700780700780700780E00F00E00F00E00F00E01E01C01C01C 01C01E03801E0700390C0038F000380000380000700000700000700000700000E00000E0 0000E00000C00000151E7F9318>26 D<0FFFF01FFFF03FFFF0604000C0400080C00000C0 000080000180000180000180000180000380000300000300000700000700000700000E00 0006000014147E9314>28 D<70F8F8F87005057C840D>58 D<70F8FCFC74040404080810 102040060E7C840D>I<000001C00000078000001E00000078000001E00000078000000E 00000038000000F0000003C000000F0000003C000000F0000000F00000003C0000000F00 000003C0000000F0000000380000000E0000000780000001E0000000780000001E000000 0780000001C01A1A7C9723>I<000100030003000600060006000C000C000C0018001800 1800300030003000600060006000C000C000C00180018001800300030003000600060006 000C000C000C00180018001800300030003000600060006000C000C000C000102D7DA117 >II<000002000000060000000E0000000E0000001E0000001F0000002F0000002F 0000004F0000008F0000008F0000010F0000010F0000020F0000040F0000040F0000080F 8000080780001007800020078000200780007FFF80004007800080078001800780010007 8002000780020007C0040003C00C0003C01E0007C0FF807FFC1E207E9F22>65 D<00FFFFE0000F0078000F003C000F001C000F001E001E001E001E001E001E001E001E00 1E003C003C003C003C003C0078003C00F0007803C0007FFF80007803C0007801E000F000 F000F000F000F000F000F0007001E000F001E000F001E000F001E000E003C001E003C003 C003C0038003C00F0007801E00FFFFF0001F1F7E9E22>I<0000FE0200078186001C004C 0038003C0060003C00C0001C01C0001803800018070000180F0000181E0000101E000010 3C0000003C00000078000000780000007800000078000000F0000000F0000000F0000000 F0000000F00000807000008070000080700001003800010038000200180004000C001800 060020000381C00000FE00001F217E9F21>I<00FFFFE000000F007800000F001C00000F 000E00000F000700001E000700001E000380001E000380001E000380003C000380003C00 0380003C000380003C000380007800078000780007800078000780007800078000F0000F 0000F0000F0000F0000E0000F0001E0001E0001C0001E0003C0001E000380001E0007000 03C000E00003C001C00003C003800003C007000007803C0000FFFFF00000211F7E9E26> I<00FFFFFF000F000E000F0006000F0002000F0002001E0002001E0002001E0002001E00 02003C0004003C0400003C0400003C04000078080000781800007FF8000078180000F010 0000F0100000F0100000F0100001E0000001E0000001E0000001E0000003C0000003C000 0003C0000003C0000007C00000FFFE0000201F7E9E1D>70 D<00FFFC00000F8000000F00 00000F0000000F0000001E0000001E0000001E0000001E0000003C0000003C0000003C00 00003C00000078000000780000007800000078000000F0000000F0000000F0000000F000 4001E0008001E0008001E0018001E0010003C0030003C0030003C0060003C00E0007803C 00FFFFFC001A1F7E9E1F>76 D<00FF00001FF0000F00003F00000B80003E00000B80005E 00000B80005E0000138000BC00001380013C00001380013C00001380023C000023800278 000023800478000023800878000021C00878000041C010F0000041C020F0000041C020F0 000041C040F0000081C041E0000081C081E0000081C101E0000081C101E0000100E203C0 000100E203C0000100E403C0000100E803C0000200E80780000200F00780000200F00780 000600E00780000F00C00F8000FFE0C1FFF8002C1F7E9E2C>I<00FF803FF0000F800780 000F800200000BC00200000BC002000013C004000011E004000011E004000011E0040000 20F008000020F008000020F808000020780800004078100000403C100000403C10000040 3C100000801E200000801E200000801E200000800F200001000F400001000F4000010007 C000010007C00002000780000200038000020003800006000380000F00010000FFE00100 00241F7E9E25>I<00FFFFC0000F0070000F0038000F001C000F001E001E001E001E001E 001E001E001E001E003C003C003C003C003C0078003C0070007800E000780380007FFE00 0078000000F0000000F0000000F0000000F0000001E0000001E0000001E0000001E00000 03C0000003C0000003C0000003C0000007C00000FFFC00001F1F7E9E1D>80 D<0001FC0000070700001C01C0003000E000E000E001C000700380007007800078070000 380F0000381E0000381E0000383C0000383C000078780000787800007878000078780000 78F00000F0F00000F0F00000E0F00001E0F00001C0F00003C070000380701C070070600F 0038811E0038813C001C8170000E81E0000783808001FD00800001018000010100000383 00000386000003FE000003FC000001F8000000F0001D297E9F24>I<00FFFF80000F01E0 000F0070000F0038000F003C001E003C001E003C001E003C001E003C003C0078003C0078 003C00F0003C01E00078038000780F00007FF80000781C0000F00E0000F00F0000F00700 00F0078001E00F0001E00F0001E00F0001E00F0003C01E0003C01E0203C01E0203C01E04 07C00E04FFFC0718000003E01F207E9E23>I<000700000C800018800030800030800060 8000610000C10000C10001C2000182000384000384000388000708000710000720000720 000E40000E80000F00000E00000E00000E00000E00001E00002E0000C601000603000604 0003180001E0001120809F13>96 D<00F1800389C00707800E03801C03803C0380380700 780700780700780700F00E00F00E00F00E00F00E10F01C20F01C20703C20705C40308C40 0F078014147E9318>I<07803F8007000700070007000E000E000E000E001C001C001CF0 1D0C3A0E3C0E380F380F700F700F700F700FE01EE01EE01EE01CE03CE038607060E031C0 1F0010207E9F14>I<007C01C207010E0F1E0F1C0E3C04780078007800F000F000F000F0 00F00070017002300418380FC010147E9314>I<0000780003F800007000007000007000 00700000E00000E00000E00000E00001C00001C000F1C00389C00707800E03801C03803C 0380380700780700780700780700F00E00F00E00F00E00F00E10F01C20F01C20703C2070 5C40308C400F078015207E9F18>I<007C01C207010E011C013C013802780C7BF07C00F0 00F000F000F0007000700170023004183807C010147E9315>I<00007C0000CE00019E00 039E00030C000700000700000700000700000E00000E00000E0000FFF0000E00000E0000 1C00001C00001C00001C00001C0000380000380000380000380000380000700000700000 700000700000700000E00000E00000E00000E00000C00001C000318000798000F3000062 00003C000017297E9F16>I<001E3000713800E0F001C0700380700780700700E00F00E0 0F00E00F00E01E01C01E01C01E01C01E01C01E03801E03800E07800E0B8006170001E700 000700000700000E00000E00300E00781C00F038006070003FC000151D809316>I<01E0 000FE00001C00001C00001C00001C000038000038000038000038000070000070000071F 000761800E80C00F00C00E00E00E00E01C01C01C01C01C01C01C01C03803803803803803 80380704700708700E08700E10700610E006206003C016207E9F1A>I<00E001E001E000 C000000000000000000000000000000E00130023804380438043808700070007000E000E 001C001C001C20384038403840388019000E000B1F7E9E10>I<0000C00001E00001E000 01C0000000000000000000000000000000000000000000001E0000630000438000838001 0380010380020700000700000700000700000E00000E00000E00000E00001C00001C0000 1C00001C0000380000380000380000380000700000700030700078E000F1C0006380003E 00001328819E13>I<01E0000FE00001C00001C00001C00001C000038000038000038000 0380000700000700000701E00706100E08700E10F00E20F00E40601C80001D00001E0000 1FC000387000383800383800381C20703840703840703840701880E01880600F0014207E 9F18>I<1E07C07C00231861860023A032030043C0340300438038038043803803808700 7007000700700700070070070007007007000E00E00E000E00E00E000E00E00E000E00E0 1C101C01C01C201C01C038201C01C038401C01C0184038038018801801800F0024147E93 28>109 D<1E07802318C023A06043C0704380704380708700E00700E00700E00700E00E 01C00E01C00E01C00E03821C03841C07041C07081C03083803101801E017147E931B>I< 00F0400388C00705800E03801C03803C0380380700780700780700780700F00E00F00E00 F00E00F00E00F01C00F01C00703C00705C0030B8000F3800003800003800007000007000 00700000700000E00000E0000FFE00121D7E9314>113 D<1E1E0023210023C38043C780 4387804383008700000700000700000700000E00000E00000E00000E00001C00001C0000 1C00001C000038000018000011147E9315>I<007C018203010603060706060E00078007 F803FC01FE001F00077007F006F006E004400820301FC010147E9315>I<00C000E001C0 01C001C001C003800380FFF8038007000700070007000E000E000E000E001C001C001C00 1C10382038203820384018800F000D1C7F9B10>I<0F00601180702180E021C0E041C0E0 4380E08381C00701C00701C00701C00E03800E03800E03800E03840E07080C07080C0708 0E0F1006131003E1E016147E931A>I<0F01801183C02183E021C1E041C0E04380608380 400700400700400700400E00800E00800E00800E01000E01000C02000E04000E04000618 0001E00013147E9316>I<0F006060118070F02180E0F821C0E07841C0E0384380E01883 81C0100701C0100701C0100701C0100E0380200E0380200E0380200E0380400E0380400E 0380800E078080060781000709860001F078001D147E9321>I<03C1C00C622010347010 38F02038F020386040700000700000700000700000E00000E00000E00000E02061C040F1 C040F1C080E2C080446300383C0014147E931A>I<0F00601180702180E021C0E041C0E0 4380E08381C00701C00701C00701C00E03800E03800E03800E03800E07000C07000C0700 0E0F00061E0003EE00000E00000E00001C0078180078380070700060600021C0001F0000 141D7E9316>I<01E02003F04007F8C00C1F800801000002000004000008000010000060 0000C0000100000200000400800801001003003F060061FC0040F80080700013147E9315 >I<000300000300000180FFFFE0FFFFE0000380000600000C001308779F17>126 D E /Fm 85 128 df5 D<001F83E000F06E3001C078780380F8780300F030070070000700700007007000070070 00070070000700700007007000FFFFFF8007007000070070000700700007007000070070 000700700007007000070070000700700007007000070070000700700007007000070070 00070070000700700007007000070070007FE3FF001D20809F1B>11 D<003F0000E0C001C0C00381E00701E00701E00700000700000700000700000700000700 00FFFFE00700E00700E00700E00700E00700E00700E00700E00700E00700E00700E00700 E00700E00700E00700E00700E00700E00700E00700E07FC3FE1720809F19>I<003FE000 E0E001C1E00381E00700E00700E00700E00700E00700E00700E00700E00700E0FFFFE007 00E00700E00700E00700E00700E00700E00700E00700E00700E00700E00700E00700E007 00E00700E00700E00700E00700E00700E07FE7FE1720809F19>I<001F81F80000F04F04 0001C07C06000380F80F000300F00F000700F00F00070070000007007000000700700000 070070000007007000000700700000FFFFFFFF0007007007000700700700070070070007 007007000700700700070070070007007007000700700700070070070007007007000700 700700070070070007007007000700700700070070070007007007000700700700070070 07007FE3FE3FF02420809F26>I<70F8F8F8F8F8F8F87070707070707070707020202020 20000000000070F8F8F87005217CA00D>33 D<7038F87CFC7EFC7E743A04020402040208 04080410081008201040200F0E7E9F17>I<70F8FCFC74040404080810102040060E7C9F 0D>39 D<0020004000800100020006000C000C0018001800300030003000700060006000 6000E000E000E000E000E000E000E000E000E000E000E000E00060006000600070003000 30003000180018000C000C000600020001000080004000200B2E7DA112>I<8000400020 00100008000C00060006000300030001800180018001C000C000C000C000E000E000E000 E000E000E000E000E000E000E000E000E000C000C000C001C00180018001800300030006 0006000C00080010002000400080000B2E7DA112>I<0006000000060000000600000006 000000060000000600000006000000060000000600000006000000060000000600000006 00000006000000060000FFFFFFF0FFFFFFF0000600000006000000060000000600000006 000000060000000600000006000000060000000600000006000000060000000600000006 0000000600001C207D9A23>43 D<70F8FCFC74040404080810102040060E7C840D>II<70F8F8F87005057C840D>I<000100030003000600060006000C00 0C000C00180018001800300030003000600060006000C000C000C0018001800180030003 0003000600060006000C000C000C00180018001800300030003000600060006000C000C0 00C000102D7DA117>I<03F0000E1C001C0E001806003807007003807003807003807003 80F003C0F003C0F003C0F003C0F003C0F003C0F003C0F003C0F003C0F003C0F003C0F003 C0F003C07003807003807003807807803807001806001C0E000E1C0003F000121F7E9D17 >I<018003800F80F3800380038003800380038003800380038003800380038003800380 0380038003800380038003800380038003800380038007C0FFFE0F1E7C9D17>I<03F000 0C1C00100E00200700400780800780F007C0F803C0F803C0F803C02007C00007C0000780 000780000F00000E00001C0000380000700000600000C0000180000300000600400C0040 1800401000803FFF807FFF80FFFF80121E7E9D17>I<03F0000C1C00100E00200F00780F 80780780780780380F80000F80000F00000F00000E00001C0000380003F000003C00000E 00000F000007800007800007C02007C0F807C0F807C0F807C0F00780400780400F00200E 001C3C0003F000121F7E9D17>I<000600000600000E00000E00001E00002E00002E0000 4E00008E00008E00010E00020E00020E00040E00080E00080E00100E00200E00200E0040 0E00C00E00FFFFF0000E00000E00000E00000E00000E00000E00000E0000FFE0141E7F9D 17>I<1803001FFE001FFC001FF8001FE000100000100000100000100000100000100000 11F000161C00180E001007001007800003800003800003C00003C00003C07003C0F003C0 F003C0E00380400380400700200600100E000C380003E000121F7E9D17>I<007C000182 000701000E03800C07801C0780380300380000780000700000700000F1F000F21C00F406 00F80700F80380F80380F003C0F003C0F003C0F003C0F003C07003C07003C07003803803 803807001807000C0E00061C0001F000121F7E9D17>I<4000007FFFC07FFF807FFF8040 010080020080020080040000080000080000100000200000200000400000400000C00000 C00001C00001800003800003800003800003800007800007800007800007800007800007 8000078000030000121F7D9D17>I<03F0000C0C00100600300300200180600180600180 6001807001807803003E03003F06001FC8000FF00003F80007FC000C7E00103F00300F80 6003804001C0C001C0C000C0C000C0C000C0C000806001802001001002000C0C0003F000 121F7E9D17>I<03F0000E18001C0C00380600380700700700700380F00380F00380F003 C0F003C0F003C0F003C0F003C07007C07007C03807C0180BC00E13C003E3C00003800003 80000380000700300700780600780E00700C002018001070000FC000121F7E9D17>I<70 F8F8F8700000000000000000000070F8F8F87005147C930D>I<70F8F8F8700000000000 000000000070F0F8F878080808101010202040051D7C930D>I<7FFFFFE0FFFFFFF00000 000000000000000000000000000000000000000000000000000000000000FFFFFFF07FFF FFE01C0C7D9023>61 D<07000F800F800F80070000000000000000000000020002000200 0200020002000600060004000C001C00380078007000F018F03CF03CF01CF00870183820 0FC00E207D9615>I<000100000003800000038000000380000007C0000007C0000007C0 000009E0000009E0000009E0000010F0000010F0000010F0000020780000207800002078 0000403C0000403C0000403C0000801E0000801E0000FFFE0001000F0001000F0001000F 00020007800200078002000780040003C00E0003C01F0007E0FFC03FFE1F207F9F22>65 DI<000FC040007030C001C009C0 038005C0070003C00E0001C01E0000C01C0000C03C0000C07C0000407C00004078000040 F8000000F8000000F8000000F8000000F8000000F8000000F8000000F8000000F8000000 780000007C0000407C0000403C0000401C0000401E0000800E0000800700010003800200 01C0040000703800000FC0001A217D9F21>IIII<000FE0200078186000E004E0038002E0070001E0 0F0000E01E0000601E0000603C0000603C0000207C00002078000020F8000000F8000000 F8000000F8000000F8000000F8000000F8000000F8007FFCF80003E0780001E07C0001E0 3C0001E03C0001E01E0001E01E0001E00F0001E0070001E0038002E000E0046000781820 000FE0001E217D9F24>III<0FFFC0007C 00003C00003C00003C00003C00003C00003C00003C00003C00003C00003C00003C00003C 00003C00003C00003C00003C00003C00003C00003C00003C00003C00203C00F83C00F83C 00F83C00F0380040780040700030E0000F800012207E9E17>IIIII<001F800000F0F00001C0380007801E000F000F000E0007001E00 07803C0003C03C0003C07C0003E0780001E0780001E0F80001F0F80001F0F80001F0F800 01F0F80001F0F80001F0F80001F0F80001F0F80001F0780001E07C0003E07C0003E03C00 03C03C0003C01E0007800E0007000F000F0007801E0001C0380000F0F000001F80001C21 7D9F23>II82 D<07E0800C198010078030038060018060 0180E00180E00080E00080E00080F00000F000007800007F00003FF0001FFC000FFE0003 FF00001F800007800003C00003C00001C08001C08001C08001C08001C0C00180C00380E0 0300F00600CE0C0081F80012217D9F19>I<7FFFFFE0780F01E0600F0060400F0020400F 0020C00F0030800F0010800F0010800F0010800F0010000F0000000F0000000F0000000F 0000000F0000000F0000000F0000000F0000000F0000000F0000000F0000000F0000000F 0000000F0000000F0000000F0000000F0000000F0000000F0000001F800007FFFE001C1F 7E9E21>IIII89 D91 D<080410082010201040204020804080408040 B85CFC7EFC7E7C3E381C0F0E7B9F17>II<1FE000 303000781800781C00300E00000E00000E00000E0000FE00078E001E0E00380E00780E00 F00E10F00E10F00E10F01E10781E103867200F83C014147E9317>97 D<0E0000FE00000E00000E00000E00000E00000E00000E00000E00000E00000E00000E00 000E3E000EC3800F01C00F00E00E00E00E00700E00700E00780E00780E00780E00780E00 780E00780E00700E00700E00E00F00E00D01C00CC300083E0015207F9F19>I<03F80E0C 1C1E381E380C70007000F000F000F000F000F000F00070007000380138011C020E0C03F0 10147E9314>I<000380003F800003800003800003800003800003800003800003800003 8000038000038003E380061B801C0780380380380380700380700380F00380F00380F003 80F00380F00380F003807003807003803803803807801C07800E1B8003E3F815207E9F19 >I<03F0000E1C001C0E00380700380700700700700380F00380F00380FFFF80F00000F0 0000F000007000007000003800801800800C010007060001F80011147F9314>I<007C00 C6018F038F07060700070007000700070007000700FFF007000700070007000700070007 00070007000700070007000700070007000700070007007FF01020809F0E>I<0000E003 E3300E3C301C1C30380E00780F00780F00780F00780F00780F00380E001C1C001E380033 E0002000002000003000003000003FFE001FFF800FFFC03001E0600070C00030C00030C0 0030C000306000603000C01C038003FC00141F7F9417>I<0E0000FE00000E00000E0000 0E00000E00000E00000E00000E00000E00000E00000E00000E3E000E43000E81800F01C0 0F01C00E01C00E01C00E01C00E01C00E01C00E01C00E01C00E01C00E01C00E01C00E01C0 0E01C00E01C00E01C0FFE7FC16207F9F19>I<1C001E003E001E001C0000000000000000 00000000000E007E000E000E000E000E000E000E000E000E000E000E000E000E000E000E 000E000E000E00FFC00A1F809E0C>I<00E001F001F001F000E000000000000000000000 0000007007F000F000700070007000700070007000700070007000700070007000700070 00700070007000700070007000706070F060F0C061803F000C28829E0E>I<0E0000FE00 000E00000E00000E00000E00000E00000E00000E00000E00000E00000E00000E0FF00E03 C00E03000E02000E04000E08000E10000E30000E70000EF8000F38000E1C000E1E000E0E 000E07000E07800E03800E03C00E03E0FFCFF815207F9F18>I<0E00FE000E000E000E00 0E000E000E000E000E000E000E000E000E000E000E000E000E000E000E000E000E000E00 0E000E000E000E000E000E000E000E00FFE00B20809F0C>I<0E1F01F000FE618618000E 81C81C000F00F00E000F00F00E000E00E00E000E00E00E000E00E00E000E00E00E000E00 E00E000E00E00E000E00E00E000E00E00E000E00E00E000E00E00E000E00E00E000E00E0 0E000E00E00E000E00E00E00FFE7FE7FE023147F9326>I<0E3E00FE43000E81800F01C0 0F01C00E01C00E01C00E01C00E01C00E01C00E01C00E01C00E01C00E01C00E01C00E01C0 0E01C00E01C00E01C0FFE7FC16147F9319>I<01F800070E001C03803801C03801C07000 E07000E0F000F0F000F0F000F0F000F0F000F0F000F07000E07000E03801C03801C01C03 80070E0001F80014147F9317>I<0E3E00FEC3800F01C00F00E00E00E00E00F00E00700E 00780E00780E00780E00780E00780E00780E00700E00F00E00E00F01E00F01C00EC3000E 3E000E00000E00000E00000E00000E00000E00000E00000E0000FFE000151D7F9319>I< 03E0800619801C05803C0780380380780380700380F00380F00380F00380F00380F00380 F003807003807803803803803807801C0B800E138003E380000380000380000380000380 000380000380000380000380003FF8151D7E9318>I<0E78FE8C0F1E0F1E0F0C0E000E00 0E000E000E000E000E000E000E000E000E000E000E000E00FFE00F147F9312>I<1F9030 704030C010C010C010E00078007F803FE00FF00070803880188018C018C018E030D0608F 800D147E9312>I<020002000200060006000E000E003E00FFF80E000E000E000E000E00 0E000E000E000E000E000E000E080E080E080E080E080610031001E00D1C7F9B12>I<0E 01C0FE1FC00E01C00E01C00E01C00E01C00E01C00E01C00E01C00E01C00E01C00E01C00E 01C00E01C00E01C00E01C00E03C00603C0030DC001F1FC16147F9319>III<7FC3FC0F01E00701C007018003810001C20000E40000EC00007800003800003C 00007C00004E000087000107000303800201C00601E01E01E0FF07FE1714809318>II<3FFF380E200E201C40384078407000 E001E001C00380078007010E011E011C0338027006700EFFFE10147F9314>III<1C043F1863F080E00E047C9D17>126 D<30307878F87C787830300E057C9E17>I E /Fn 23 122 df<70F8FCFC740404040408 0810102040060F7C840E>44 D<70F8F8F87005057C840E>46 D<008003800F80F3800380 038003800380038003800380038003800380038003800380038003800380038003800380 0380038003800380038003800380038007C0FFFE0F217CA018>49 D<03F0000C1C001007002007804003C04003C08003E0F003E0F801E0F801E0F801E02003 E00003E00003C00003C0000780000700000E00001C0000180000300000600000C0000180 000100000200200400200800201800603000403FFFC07FFFC0FFFFC013217EA018>I<00 7E0001C1000300800601C00E03C01C03C0180180380000380000780000700000700000F0 F800F30C00F40600F40300F80380F801C0F001C0F001E0F001E0F001E0F001E0F001E070 01E07001E07001E03801C03801C01803801C03000C0600070C0001F00013227EA018>54 D<01F000060C000C0600180700380380700380700380F001C0F001C0F001C0F001E0F001 E0F001E0F001E0F001E07001E07003E03803E01805E00C05E00619E003E1E00001C00001 C00001C0000380000380300300780700780600700C002018001030000FC00013227EA018 >57 D66 D72 D77 D<03F0200C0C601802603001E07000E0600060E00060E00060E00020E00020E00020F000 00F000007800007F00003FF0001FFE000FFF0003FF80003FC00007E00001E00000F00000 F0000070800070800070800070800070C00060C00060E000C0F000C0C80180C6070081FC 0014247DA21B>83 D85 D<0FE0001838003C0C003C0E001807000007000007000007 0000FF0007C7001E07003C0700780700700700F00708F00708F00708F00F087817083C23 900FC1E015157E9418>97 D<0E0000FE00001E00000E00000E00000E00000E00000E0000 0E00000E00000E00000E00000E00000E00000E1F000E61C00E80600F00300E00380E003C 0E001C0E001E0E001E0E001E0E001E0E001E0E001E0E001E0E001C0E003C0E00380F0070 0C80600C41C0083F0017237FA21B>I<01FE000703000C07801C07803803007800007000 00F00000F00000F00000F00000F00000F00000F000007000007800403800401C00800C01 0007060001F80012157E9416>I<01FC000707000C03801C01C03801C07801E07000E0F0 00E0FFFFE0F00000F00000F00000F00000F000007000007800203800201C00400E008007 030000FC0013157F9416>101 D<00007001F198071E180E0E181C07001C07003C07803C 07803C07803C07801C07001C07000E0E000F1C0019F0001000001000001800001800001F FE000FFFC00FFFE03800F0600030400018C00018C00018C000186000306000303800E00E 038003FE0015217F9518>103 D<0E0000FE00001E00000E00000E00000E00000E00000E 00000E00000E00000E00000E00000E00000E00000E1F800E60C00E80E00F00700F00700E 00700E00700E00700E00700E00700E00700E00700E00700E00700E00700E00700E00700E 00700E00700E0070FFE7FF18237FA21B>I<1C001E003E001E001C000000000000000000 00000000000000000E00FE001E000E000E000E000E000E000E000E000E000E000E000E00 0E000E000E000E000E000E00FFC00A227FA10E>I<0E1F80FE60C01E80E00F00700F0070 0E00700E00700E00700E00700E00700E00700E00700E00700E00700E00700E00700E0070 0E00700E00700E0070FFE7FF18157F941B>110 D<0E3CFE461E8F0F0F0F060F000E000E 000E000E000E000E000E000E000E000E000E000E000E000F00FFF010157F9413>114 D<02000200020002000600060006000E001E003E00FFF80E000E000E000E000E000E000E 000E000E000E000E000E040E040E040E040E040E040708030801F00E1F7F9E13>116 D119 D121 D E /Fo 22 122 df<78FCFCFCFC78000000000000 0000000000000000000000000078FCFCFCFC78061F7A9E12>58 D<7FFFFFFFFFE07FFFFF FFFFE07E000F8007E078000F8001E070000F8000E060000F80006040000F80002040000F 800020C0000F800030C0000F80003080000F80001080000F80001080000F80001080000F 80001080000F80001080000F80001000000F80000000000F80000000000F80000000000F 80000000000F80000000000F80000000000F80000000000F80000000000F80000000000F 80000000000F80000000000F80000000000F80000000000F80000000000F80000000000F 80000000000F80000000000F80000000000F80000000000F80000000000F80000000000F 80000000000F80000000000F80000000000F80000000000F80000000000F80000000000F 80000000000F80000000000F80000000001FC00000000FFFFF8000000FFFFF80002C317E B030>84 D<00FE00000303C0000C00E00010007000100038003C003C003E001C003E001E 003E001E0008001E0000001E0000001E0000001E00000FFE0000FC1E0003E01E000F801E 001F001E003E001E003C001E007C001E00F8001E04F8001E04F8001E04F8003E04F8003E 0478003E047C005E043E008F080F0307F003FC03E01E1F7D9E21>97 D<003F8000E0600380180700040F00041E001E1C003E3C003E7C003E7C0008780000F800 00F80000F80000F80000F80000F80000F80000F80000F800007800007C00007C00003C00 011E00011E00020F000207000403801800E060003F80181F7D9E1D>99 D<000001E000003FE000003FE0000003E0000001E0000001E0000001E0000001E0000001 E0000001E0000001E0000001E0000001E0000001E0000001E0000001E0000001E0000001 E0000001E0001F81E000F061E001C019E0078005E00F0003E00E0003E01E0001E03C0001 E03C0001E07C0001E0780001E0F80001E0F80001E0F80001E0F80001E0F80001E0F80001 E0F80001E0F80001E0F80001E0780001E0780001E03C0001E03C0001E01C0001E01E0003 E00E0005E0070009E0038011F000E061FF003F81FF20327DB125>I<003F800000E0E000 0380380007003C000E001E001E001E001C000F003C000F007C000F0078000F8078000780 F8000780F8000780FFFFFF80F8000000F8000000F8000000F8000000F8000000F8000000 780000007C0000003C0000003C0000801E0000800E0001000F0002000780020001C00C00 00F03000001FC000191F7E9E1D>I<0007E0001C1000383800707C00E07C01E07C01C038 03C00003C00003C00003C00003C00003C00003C00003C00003C00003C00003C00003C000 FFFFC0FFFFC003C00003C00003C00003C00003C00003C00003C00003C00003C00003C000 03C00003C00003C00003C00003C00003C00003C00003C00003C00003C00003C00003C000 03C00003C00003C00003C00007E0007FFF007FFF0016327FB114>I<000000F0007F0308 01C1C41C0380E81C070070080F0078001E003C001E003C003E003E003E003E003E003E00 3E003E003E003E003E003E001E003C001E003C000F007800070070000780E00009C1C000 087F000018000000180000001800000018000000180000001C0000000E0000000FFFF800 07FFFF0003FFFF800E000FC0180001E0300000F070000070E0000038E0000038E0000038 E0000038E00000387000007070000070380000E01C0001C00700070001C01C00003FE000 1E2F7E9F21>I<0780000000FF80000000FF800000000F80000000078000000007800000 000780000000078000000007800000000780000000078000000007800000000780000000 0780000000078000000007800000000780000000078000000007800000000780FE000007 83078000078C03C000079001E00007A001E00007A000F00007C000F00007C000F0000780 00F000078000F000078000F000078000F000078000F000078000F000078000F000078000 F000078000F000078000F000078000F000078000F000078000F000078000F000078000F0 00078000F000078000F000078000F000078000F000078000F0000FC001F800FFFC1FFF80 FFFC1FFF8021327EB125>I<07000F801F801F800F800700000000000000000000000000 000000000000000000000780FF80FF800F80078007800780078007800780078007800780 0780078007800780078007800780078007800780078007800780078007800FC0FFF8FFF8 0D307EAF12>I<0780FF80FF800F80078007800780078007800780078007800780078007 800780078007800780078007800780078007800780078007800780078007800780078007 80078007800780078007800780078007800780078007800780078007800FC0FFFCFFFC0E 327EB112>108 D<0780FE001FC000FF83078060F000FF8C03C18078000F9001E2003C00 07A001E4003C0007A000F4001E0007C000F8001E0007C000F8001E00078000F0001E0007 8000F0001E00078000F0001E00078000F0001E00078000F0001E00078000F0001E000780 00F0001E00078000F0001E00078000F0001E00078000F0001E00078000F0001E00078000 F0001E00078000F0001E00078000F0001E00078000F0001E00078000F0001E00078000F0 001E00078000F0001E00078000F0001E00078000F0001E000FC001F8003F00FFFC1FFF83 FFF0FFFC1FFF83FFF0341F7E9E38>I<0780FE0000FF83078000FF8C03C0000F9001E000 07A001E00007A000F00007C000F00007C000F000078000F000078000F000078000F00007 8000F000078000F000078000F000078000F000078000F000078000F000078000F0000780 00F000078000F000078000F000078000F000078000F000078000F000078000F000078000 F000078000F000078000F0000FC001F800FFFC1FFF80FFFC1FFF80211F7E9E25>I<001F C00000F0780001C01C00070007000F0007801E0003C01C0001C03C0001E03C0001E07800 00F0780000F0780000F0F80000F8F80000F8F80000F8F80000F8F80000F8F80000F8F800 00F8F80000F8780000F07C0001F03C0001E03C0001E01E0003C01E0003C00F0007800780 0F0001C01C0000F07800001FC0001D1F7E9E21>I<0781FC00FF860700FF8803C00F9001 E007A000F007C00078078000780780003C0780003C0780003E0780001E0780001F078000 1F0780001F0780001F0780001F0780001F0780001F0780001F0780001F0780003E078000 3E0780003C0780007C0780007807C000F007A000F007A001E00798038007860F000781F8 000780000007800000078000000780000007800000078000000780000007800000078000 0007800000078000000FC00000FFFC0000FFFC0000202D7E9E25>I<0783E0FF8C18FF90 7C0F907C07A07C07C03807C00007C00007C0000780000780000780000780000780000780 000780000780000780000780000780000780000780000780000780000780000780000780 000780000FC000FFFE00FFFE00161F7E9E19>114 D<01FC100E03301800F03000706000 30E00030E00010E00010E00010F00010F800007E00003FF0001FFF000FFFC003FFE0003F F00001F80000F880003C80003C80001CC0001CC0001CE0001CE00018F00038F00030CC00 60C301C080FE00161F7E9E1A>I<00400000400000400000400000400000C00000C00000 C00001C00001C00003C00007C0000FC0001FFFE0FFFFE003C00003C00003C00003C00003 C00003C00003C00003C00003C00003C00003C00003C00003C00003C00003C00003C00003 C01003C01003C01003C01003C01003C01003C01003C01001C02001E02000E0400078C000 1F00142C7FAB19>I<078000F000FF801FF000FF801FF0000F8001F000078000F0000780 00F000078000F000078000F000078000F000078000F000078000F000078000F000078000 F000078000F000078000F000078000F000078000F000078000F000078000F000078000F0 00078000F000078000F000078000F000078001F000078001F000078001F000038002F000 03C004F00001C008F800007030FF80001FC0FF80211F7E9E25>II120 DI E end %%EndProlog %%BeginSetup %%Feature: *Resolution 300dpi TeXDict begin %%PaperSize: A4 %%EndSetup %%Page: 1 1 1 0 bop 103 489 a Fo(The)21 b(greatest)i(common)d(divisor:)28 b(a)22 b(case)g(study)e(for)i(program)457 581 y(extraction)g(from)f (classical)g(pro)r(ofs)511 707 y Fn(U.)16 b(Berger)182 b(H.)15 b(Sc)o(h)o(wic)o(h)o(ten)o(b)q(erg)760 809 y(Ma)o(y)h(29,)h (1996)59 983 y Fm(Yiannis)d(Mosc)o(ho)o(v)m(akis)f(suggested)g(the)h (follo)o(wing)f(example)i(of)d(a)h(classical)i(existence)g(pro)q(of)d (with)i(a)-12 1040 y(quan)o(ti\014er{free)h(k)o(ernel)g(whic)o(h)g(do)q (es)g(not)f(ob)o(viously)i(con)o(tain)e(an)h(algorithm:)k(the)c(gcd)f (of)g(t)o(w)o(o)g(natural)-12 1096 y(n)o(um)o(b)q(ers)23 b Fl(a)203 1103 y Fk(1)245 1096 y Fm(and)g Fl(a)365 1103 y Fk(2)408 1096 y Fm(is)g(a)f(linear)i(com)o(bination)g(of)e(the)h(t)o (w)o(o.)41 b(Here)23 b(w)o(e)g(treat)e(that)h(example)i(as)-12 1153 y(a)e(case)h(study)g(for)f(program)f(extraction)i(from)f (classical)i(pro)q(ofs.)42 b(W)l(e)22 b(apply)i(H.)e(F)l(riedman's)h Fl(A)p Fm({)-12 1209 y(translation)16 b([3])g(follo)o(w)o(ed)h(b)o(y)f (a)g(mo)q(di\014ed)i(realizabilit)o(y)h(in)o(terpretation)d(to)g (extract)g(a)g(program)f(from)-12 1266 y(this)g(pro)q(of.)k(Ho)o(w)o (ev)o(er,)13 b(to)h(obtain)g(a)h(reasonable)f(program)g(it)g(is)h (essen)o(tial)g(to)f(use)h(a)f(re\014nemen)o(t)h(of)f(the)-12 1322 y Fl(A)p Fm({translation)g(in)o(tro)q(duced)i(in)f(Berger/Sc)o(h)o (wic)o(h)o(ten)o(b)q(erg)g([1)o(,)f(2].)19 b(This)c(re\014nemen)o(t)f (mak)o(es)g(it)h(p)q(ossible)-12 1379 y(that)j(not)g(all)i(atoms)d(in)i (the)g(pro)q(of)f(are)h Fl(A)p Fm({translated,)f(but)h(only)g(those)f (with)h(a)g(\\critical")g(relation)-12 1435 y(sym)o(b)q(ol.)h(In)c(our) f(example)h(only)g(the)f(divisibil)q(it)o(y)j(relation)e Fj(\001j\001)e Fm(will)i(b)q(e)g(critical.)59 1491 y(Let)g Fl(a;)8 b(b;)g(c;)g(i)o(;)f(j;)g(k)q(;)h(`;)f(m;)g(n;)g(q)r(;)h(r)13 b Fm(denote)k(natural)f(n)o(um)o(b)q(ers.)22 b(Our)17 b(language)f(is)g(determined)i(b)o(y)e(the)-12 1548 y(constan)o(ts)g(0) p Fl(;)8 b Fm(1)p Fl(;)g Fm(+)p Fl(;)g Fj(\003)p Fm(,)14 b(function)k(sym)o(b)q(ols)f(for)f(the)h(quotien)o(t)g(and)g(the)h (remainder)f(denoted)h(b)o(y)e Fl(q)r Fm(\()p Fl(a;)8 b(c)p Fm(\))-12 1604 y(and)j Fl(r)q Fm(\()p Fl(a;)d(c)p Fm(\),)h(a)h(4{ary)g(function)h(denoted)g(b)o(y)g(abs\()p Fl(k)878 1611 y Fk(1)897 1604 y Fl(a)921 1611 y Fk(1)942 1604 y Fj(\000)q Fl(k)1002 1611 y Fk(2)1021 1604 y Fl(a)1045 1611 y Fk(2)1065 1604 y Fm(\))f(whose)h(in)o(tended)h(meaning)f(is)g (clear)g(from)-12 1661 y(the)g(notation)g(and)h(an)f(auxiliary)i(5{ary) d(function)i Fl(f)k Fm(whic)o(h)c(will)h(b)q(e)f(de\014ned)h(later.)19 b(W)l(e)11 b(will)i(express)f(the)-12 1717 y(in)o(tended)k(meaning)f (of)g(these)f(function)i(sym)o(b)q(ols)f(b)o(y)f(stating)h(some)f(prop) q(erties)h(\(lemmata\))f Fl(v)1656 1724 y Fk(1)1676 1717 y Fl(;)8 b(:)g(:)g(:)d(;)j(v)1800 1724 y Fk(6)-12 1774 y Fm(of)15 b(them;)f(these)i(will)h(b)q(e)f(form)o(ulated)f(as)f(w)o(e) h(need)h(them.)-12 1855 y Fi(Theorem.)-12 1957 y Fj(8)p Fl(a)37 1964 y Fk(1)57 1957 y Fl(;)8 b(a)102 1964 y Fk(2)121 1957 y Fm(\(0)k Fl(<)h(a)246 1964 y Fk(2)278 1957 y Fj(!)g(9)p Fl(k)385 1964 y Fk(1)405 1957 y Fl(;)8 b(k)450 1964 y Fk(2)469 1957 y Fm(\(abs)o(\()p Fl(k)594 1964 y Fk(1)613 1957 y Fl(a)637 1964 y Fk(1)666 1957 y Fj(\000)i Fl(k)735 1964 y Fk(2)755 1957 y Fl(a)779 1964 y Fk(2)798 1957 y Fm(\))p Fj(j)p Fl(a)853 1964 y Fk(1)882 1957 y Fj(^)g Fm(abs\()p Fl(k)1030 1964 y Fk(1)1049 1957 y Fl(a)1073 1964 y Fk(1)1102 1957 y Fj(\000)g Fl(k)1171 1964 y Fk(2)1190 1957 y Fl(a)1214 1964 y Fk(2)1234 1957 y Fm(\))p Fj(j)p Fl(a)1289 1964 y Fk(2)1318 1957 y Fj(^)f Fm(0)k Fl(<)g Fm(abs\()p Fl(k)1549 1964 y Fk(1)1568 1957 y Fl(a)1592 1964 y Fk(1)1621 1957 y Fj(\000)d Fl(k)1690 1964 y Fk(2)1709 1957 y Fl(a)1733 1964 y Fk(2)1753 1957 y Fm(\)\)\))p Fl(:)-12 2059 y Fh(Pr)n(o)n(of.)20 b Fm(Let)15 b Fl(a)233 2066 y Fk(1)253 2059 y Fl(;)8 b(a)298 2066 y Fk(2)332 2059 y Fm(b)q(e)16 b(giv)o(en)f(and)h(assume)f(0)d Fl(<)h(a)865 2066 y Fk(2)885 2059 y Fm(.)20 b(The)15 b(ideal)h(\()p Fl(a)1161 2066 y Fk(1)1181 2059 y Fl(;)8 b(a)1226 2066 y Fk(2)1245 2059 y Fm(\))15 b(generated)g(from)f Fl(a)1616 2066 y Fk(1)1636 2059 y Fl(;)8 b(a)1681 2066 y Fk(2)1715 2059 y Fm(has)15 b(a)-12 2116 y(least)e(p)q(ositiv)o(e)h(elemen)o(t)g Fl(c)p Fm(,)f(since)h(0)e Fl(<)h(a)686 2123 y Fk(2)706 2116 y Fm(.)19 b(This)14 b(elemen)o(t)g(has)f(a)g(represen)o(tation)g Fl(c)f Fm(=)h(abs\()p Fl(k)1604 2123 y Fk(1)1623 2116 y Fl(a)1647 2123 y Fk(1)1673 2116 y Fj(\000)6 b Fl(k)1738 2123 y Fk(2)1757 2116 y Fl(a)1781 2123 y Fk(2)1801 2116 y Fm(\))-12 2172 y(with)17 b Fl(k)117 2179 y Fk(1)136 2172 y Fl(;)8 b(k)181 2179 y Fk(2)215 2172 y Fj(2)15 b Fi(N)p Fm(.)24 b(It)17 b(is)g(a)f(common)g(divisor)i(of)e Fl(a)885 2179 y Fk(1)921 2172 y Fm(and)h Fl(a)1035 2179 y Fk(2)1071 2172 y Fm(since)h(otherwise)f(the)f(remainder)i Fl(r)q Fm(\()p Fl(a)1748 2179 y Fg(i)1761 2172 y Fl(;)8 b(c)p Fm(\))-12 2229 y(w)o(ould)16 b(b)q(e)f(a)g(smaller)h(p)q(ositiv)o (e)g(elemen)o(t)g(of)f(the)g(ideal.)59 2285 y(The)20 b(n)o(um)o(b)q(er)g Fl(c)g Fj(2)h Fm(\()p Fl(a)460 2292 y Fk(1)480 2285 y Fl(;)8 b(a)525 2292 y Fk(2)544 2285 y Fm(\))19 b(dividing)j Fl(a)785 2292 y Fk(1)825 2285 y Fm(and)e Fl(a)942 2292 y Fk(2)982 2285 y Fm(is)g(the)g(greatest)f (common)h(divisor)h(since)g(an)o(y)-12 2342 y(common)15 b(divisor)h(of)f Fl(a)394 2349 y Fk(1)429 2342 y Fm(and)g Fl(a)541 2349 y Fk(2)576 2342 y Fm(m)o(ust)f(also)i(b)q(e)f(a)g (divisor)h(of)f Fl(c)p Fm(.)892 2577 y(1)p eop %%Page: 2 2 2 1 bop -12 307 a Fi(The)18 b(least)g(elemen)o(t)f(principle)i(and)f Fl(<)p Fi(-induction.)59 385 y Fm(In)12 b(order)g(to)g(formally)g (write)g(out)g(the)g(pro)q(of)g(ab)q(o)o(v)o(e)g(w)o(e)g(need)h(to)f (mak)o(e)f(explicit)k(the)d(instance)h(of)f(the)-12 442 y(induction)18 b(sc)o(heme)f(used)g(implicitly)i(in)e(the)g(least)f (elemen)o(t)h(principle.)27 b(The)16 b(least)h(elemen)o(t)g(principle) -12 498 y(w.r.t.)c(a)i(measure)g Fl(\026)h Fm(sa)o(ys)368 591 y Fj(9)391 579 y Fl(~)393 591 y(k)9 b(M)c Fm(\()491 579 y Fl(~)493 591 y(k)p Fm(\))13 b Fj(!)g(9)629 579 y Fl(~)631 591 y(k)c Fm(\()p Fl(M)c Fm(\()747 579 y Fl(~)749 591 y(k)p Fm(\))10 b Fj(^)g(8)866 579 y Fl(~)866 591 y(`)q Fm([)p Fl(\026)p Fm(\()944 579 y Fl(~)944 591 y(`)o Fm(\))j Fl(<)g(\026)p Fm(\()1084 579 y Fl(~)1086 591 y(k)q Fm(\))f Fj(!)h Fl(M)5 b Fm(\()1266 579 y Fl(~)1266 591 y(`)p Fm(\))12 b Fj(!)h(?)p Fm(]\))-12 684 y(\(in)g(our)f(example)h Fl(M)5 b Fm(\()p Fl(k)400 691 y Fk(1)419 684 y Fl(;)j(k)464 691 y Fk(2)483 684 y Fm(\))k Fj(\021)h Fm(0)f Fl(<)h Fm(abs\()p Fl(k)752 691 y Fk(1)771 684 y Fl(a)795 691 y Fk(1)819 684 y Fj(\000)t Fl(k)882 691 y Fk(2)902 684 y Fl(a)926 691 y Fk(2)946 684 y Fm(\))f(and)h Fl(\026)p Fm(\()p Fl(k)1131 691 y Fk(1)1150 684 y Fl(;)8 b(k)1195 691 y Fk(2)1214 684 y Fm(\))k Fj(\021)h Fm(abs\()p Fl(k)1400 691 y Fk(1)1419 684 y Fl(a)1443 691 y Fk(1)1467 684 y Fj(\000)t Fl(k)1530 691 y Fk(2)1550 684 y Fl(a)1574 691 y Fk(2)1594 684 y Fm(\)\).)18 b(In)13 b(order)-12 740 y(to)j(reduce)h(this)h(to)e(the)g(induction)j(sc)o(heme)e(w)o(e)f(use)h (the)g(fact)f(that)g(the)h(form)o(ula)f(ab)q(o)o(v)o(e)g(is)h (classically)-12 797 y(equiv)m(alen)o(t)g(to)238 889 y Fj(8)261 877 y Fl(~)263 889 y(k)9 b Fm(\()p Fl(M)c Fm(\()379 877 y Fl(~)381 889 y(k)p Fm(\))12 b Fj(!)i(8)519 877 y Fl(~)519 889 y(`)p Fm([)p Fl(\026)p Fm(\()596 877 y Fl(~)596 889 y(`)o Fm(\))f Fl(<)g(\026)p Fm(\()736 877 y Fl(~)738 889 y(k)q Fm(\))f Fj(!)h Fl(M)5 b Fm(\()918 877 y Fl(~)918 889 y(`)p Fm(\))12 b Fj(!)h(?)p Fm(])g Fj(!)g(?)p Fm(\))g Fj(!)g(8)1291 877 y Fl(~)1293 889 y(k)q Fm(\()p Fl(M)5 b Fm(\()1401 877 y Fl(~)1403 889 y(k)p Fm(\))13 b Fj(!)g(?)p Fm(\))-12 982 y(whic)o(h)e(nothing)g(but)f (the)g(principle)j(of)d Fl(<)p Fh({induction)g Fm(for)g(the)g (complemen)o(t)h(of)f Fl(M)5 b Fm(,)10 b Fl(N)5 b Fm(\()1473 970 y Fl(~)1475 982 y(k)q Fm(\))12 b(:=)g Fl(M)5 b Fm(\()1655 970 y Fl(~)1657 982 y(k)q Fm(\))13 b Fj(!)g(?)p Fm(.)-12 1039 y(W)l(e)i(can)h(write)f(this)g(as)696 1095 y(Prog\()p Fl(N)5 b Fm(\))11 b Fj(!)i(8)961 1083 y Fl(~)963 1095 y(k)c(N)c Fm(\()1054 1083 y Fl(~)1056 1095 y(k)p Fm(\))p Fl(;)-12 1174 y Fm(where)412 1230 y(Prog\()p Fl(N)g Fm(\))12 b(:=)g Fj(8)680 1218 y Fl(~)682 1230 y(k)r Fm(\()p Fj(8)751 1218 y Fl(~)751 1230 y(`)o Fm([)p Fl(\026)p Fm(\()827 1218 y Fl(~)827 1230 y(`)p Fm(\))g Fl(<)h(\026)p Fm(\()967 1218 y Fl(~)969 1230 y(k)r Fm(\))f Fj(!)h Fl(N)5 b Fm(\()1143 1218 y Fl(~)1143 1230 y(`)o Fm(\)])12 b Fj(!)h Fl(N)5 b Fm(\()1320 1218 y Fl(~)1322 1230 y(k)p Fm(\)\))p Fl(:)-12 1309 y Fm(In)18 b(the)f(formal)f(treatmen)o(t)g(of)g(our)h(example)h (it)f(will)i(b)q(e)e(more)g(con)o(v)o(enien)o(t)g(to)g(use)g(the)g (least)g(elemen)o(t)-12 1366 y(principle)h(in)e(the)f(form)g(of)f Fl(<)p Fm({induction.)59 1422 y(T)l(o)g(pro)o(v)o(e)h Fl(<)p Fm({induction)i(w)o(e)e(assume)g(that)g Fl(N)k Fm(is)d(progressiv)o(e,)775 1515 y Fl(w)808 1522 y Fk(1)827 1515 y Fm(:)8 b(Prog)o(\()p Fl(N)d Fm(\))p Fl(;)-12 1608 y Fm(and)15 b(pro)o(v)o(e)g Fj(8)222 1596 y Fl(~)224 1608 y(k)9 b(N)c Fm(\()315 1596 y Fl(~)317 1608 y(k)p Fm(\).)20 b(This)15 b(is)h(ac)o(hiev)o(ed)g(b)o(y)f(pro)o(ving)h Fj(8)p Fl(nB)r Fm(\()p Fl(n)p Fm(\),)f(where)594 1700 y Fl(B)r Fm(\()p Fl(n)p Fm(\))e(:=)f Fj(8)789 1688 y Fl(~)791 1700 y(k)r Fm(\()p Fl(\026)p Fm(\()878 1688 y Fl(~)880 1700 y(k)p Fm(\))h Fl(<)g(n)g Fj(!)g Fl(N)5 b Fm(\()1139 1688 y Fl(~)1141 1700 y(k)p Fm(\)\))p Fl(;)-12 1793 y Fm(and)15 b(using)h Fl(B)r Fm(\()p Fl(n)p Fm(\))g(with)f Fl(n)e Fm(:=)g Fl(\026)p Fm(\()557 1781 y Fl(~)559 1793 y(k)q Fm(\))d(+)g(1.)20 b(W)l(e)15 b(pro)o(v)o(e)g Fj(8)p Fl(nB)r Fm(\()p Fl(n)p Fm(\))h(b)o(y)f(\(zero{successor\))f(induction.) 59 1849 y Fh(Base.)19 b Fl(B)r Fm(\(0\))c(follo)o(ws)h(easily)g(from)e (the)i(lemma)707 1942 y Fl(v)729 1949 y Fk(1)749 1942 y Fm(:)8 b Fj(8)p Fl(m)p Fm(\()p Fl(m)k(<)h Fm(0)f Fj(!)h(?)p Fm(\))-12 2035 y(and)i(Efq:)8 b Fj(?)k(!)h Fl(N)5 b Fm(\()329 2023 y Fl(~)331 2035 y(k)q Fm(\).)19 b(Efq)c(is)h(not)f(needed)h(if)g (\(as)e(in)i(our)f(example\))h Fl(N)k Fm(is)15 b(a)g(negation.)59 2091 y Fh(Step.)k Fm(Let)d Fl(n)f Fm(b)q(e)h(giv)o(en)f(and)h(assume)e Fl(w)759 2098 y Fk(2)779 2091 y Fm(:)8 b Fl(B)r Fm(\()p Fl(n)p Fm(\).)19 b(T)l(o)c(sho)o(w)f Fl(B)r Fm(\()p Fl(n)d Fm(+)f(1\))15 b(let)1366 2079 y Fl(~)1368 2091 y(k)h Fm(b)q(e)g(giv)o(en)f(and)h(assume)-12 2148 y Fl(w)21 2155 y Fk(3)40 2148 y Fm(:)8 b Fl(\026)p Fm(\()104 2136 y Fl(~)106 2148 y(k)q Fm(\))k Fl(<)h(n)c Fm(+)g(1.)19 b(W)l(e)c(will)h(deriv)o(e)f Fl(N)5 b Fm(\()698 2136 y Fl(~)700 2148 y(k)p Fm(\))14 b(b)o(y)h(using)g(the)g(progressiv)o (eness)f(of)g(N,)h Fl(w)1474 2155 y Fk(1)1493 2148 y Fm(,)f(at)1573 2136 y Fl(~)1575 2148 y(k)q Fm(.)19 b(Hence)d(w)o(e)-12 2204 y(ha)o(v)o(e)f(to)f(pro)o(v)o(e)659 2261 y Fj(8)684 2249 y Fl(~)684 2261 y(`)p Fm(\()p Fl(\026)p Fm(\()766 2249 y Fl(~)766 2261 y(`)p Fm(\))e Fl(<)h(\026)p Fm(\()906 2249 y Fl(~)908 2261 y(k)q Fm(\))g Fj(!)g Fl(N)5 b Fm(\()1082 2249 y Fl(~)1082 2261 y(`)o Fm(\)\))p Fl(:)-12 2340 y Fm(So,)17 b(let)134 2328 y Fl(~)134 2340 y(`)h Fm(b)q(e)g(giv)o(en)f (and)h(assume)f(further)g Fl(w)793 2347 y Fk(4)813 2340 y Fm(:)8 b Fl(\026)p Fm(\()879 2328 y Fl(~)879 2340 y(`)o Fm(\))16 b Fl(<)g(\026)p Fm(\()1025 2328 y Fl(~)1027 2340 y(k)r Fm(\).)26 b(>F)l(rom)17 b Fl(w)1286 2347 y Fk(4)1322 2340 y Fm(and)h Fl(w)1446 2347 y Fk(3)1465 2340 y Fm(:)8 b Fl(\026)p Fm(\()1529 2328 y Fl(~)1531 2340 y(k)q Fm(\))15 b Fl(<)i(n)12 b Fm(+)g(1)17 b(w)o(e)-12 2396 y(infer)f Fl(\026)p Fm(\()138 2384 y Fl(~)138 2396 y(`)p Fm(\))d Fl(<)h(n)h Fm(\(using)h(an)g(arithmetical)g(lemma\).)21 b(Hence,)16 b(b)o(y)g(induction)h(h)o(yp)q(othesis)f Fl(w)1589 2403 y Fk(2)1609 2396 y Fm(:)8 b Fl(B)r Fm(\()p Fl(n)p Fm(\))15 b(at)1799 2384 y Fl(~)1800 2396 y(`)-12 2452 y Fm(w)o(e)g(get)g Fl(N)5 b Fm(\()191 2440 y Fl(~)191 2452 y(`)o Fm(\).)892 2577 y(2)p eop %%Page: 3 3 3 2 bop -12 307 a Fi(Detailed)19 b(pro)q(of)f(of)f(the)h(theorem.)59 386 y Fm(No)o(w)i(w)o(e)g(rep)q(eat)h(the)g(pro)q(of)f(of)h(the)g (theorem)f(in)i(some)e(more)h(detail)g(using)h Fl(<)p Fm({induction.)39 b(As)-12 443 y(alw)o(a)o(ys)15 b(in)i(classical)h (logic,)f(w)o(e)f(ma)o(y)f(view)i(the)f(pro)q(of)g(as)g(an)g(indirect)i (one,)e(deriving)h(a)f(con)o(tradiction)-12 499 y(from)d(the)i (assumption)f(that)g(the)g(claim)h(is)g(false.)20 b(So)14 b(let)h Fl(a)1022 506 y Fk(1)1042 499 y Fl(;)8 b(a)1087 506 y Fk(2)1120 499 y Fm(b)q(e)15 b(giv)o(en)g(and)f(assume)g Fl(v)1564 506 y Fk(0)1584 499 y Fm(:)8 b(0)j Fl(<)i(a)1711 506 y Fk(2)1745 499 y Fm(and)72 595 y Fl(u)p Fm(:)8 b Fj(8)p Fl(k)168 602 y Fk(1)187 595 y Fl(;)g(k)232 602 y Fk(2)250 595 y Fm(\(abs\()p Fl(k)376 602 y Fk(1)395 595 y Fl(a)419 602 y Fk(1)449 595 y Fj(\000)i Fl(k)518 602 y Fk(2)537 595 y Fl(a)561 602 y Fk(2)581 595 y Fm(\))p Fj(j)p Fl(a)636 602 y Fk(1)668 595 y Fj(!)j Fm(abs\()p Fl(k)834 602 y Fk(1)853 595 y Fl(a)877 602 y Fk(1)907 595 y Fj(\000)d Fl(k)976 602 y Fk(2)996 595 y Fl(a)1020 602 y Fk(2)1039 595 y Fm(\))p Fj(j)p Fl(a)1094 602 y Fk(2)1126 595 y Fj(!)j Fm(0)f Fl(<)h Fm(abs\()p Fl(k)1375 602 y Fk(1)1394 595 y Fl(a)1418 602 y Fk(1)1448 595 y Fj(\000)e Fl(k)1518 602 y Fk(2)1537 595 y Fl(a)1561 602 y Fk(2)1581 595 y Fm(\))h Fj(!)h(?)p Fm(\))p Fl(:)-12 691 y Fm(W)l(e)k(ha)o(v)o(e)h(to)e(pro)o(v)o(e)h Fj(?)h Fm(whic)o(h)g(will)h(b)q(e)f(ac)o(hiev)o(ed)h(b)o(y)e(pro)o(ving)h Fj(8)p Fl(k)1162 698 y Fk(1)1181 691 y Fl(;)8 b(k)1226 698 y Fk(2)1245 691 y Fm(\(0)16 b Fl(<)g Fm(abs\()p Fl(k)1461 698 y Fk(1)1480 691 y Fl(a)1504 698 y Fk(1)1536 691 y Fj(\000)c Fl(k)1607 698 y Fk(2)1626 691 y Fl(a)1650 698 y Fk(2)1670 691 y Fm(\))k Fj(!)h(?)p Fm(\))-12 748 y(b)o(y)e Fl(<)p Fm({induction)j(and)d(then)h(sp)q(ecializin)q(g)i(this)e(form)o (ula)f(to)g Fl(k)1082 755 y Fk(1)1101 748 y Fl(;)8 b(k)1146 755 y Fk(2)1178 748 y Fm(=)13 b(0)p Fl(;)8 b Fm(1)14 b(and)i(using)g(the)f(assumption)-12 804 y Fl(v)10 811 y Fk(0)30 804 y Fm(:)8 b(0)j Fl(<)i(a)157 811 y Fk(2)177 804 y Fm(\(=)g(abs\(0)p Fl(a)374 811 y Fk(1)403 804 y Fj(\000)d Fm(1)p Fl(a)495 811 y Fk(2)515 804 y Fm(\)\).)59 861 y(The)15 b(principle)j(of)d Fl(<)p Fm(-induction)i(is)f(used)g (with)139 957 y Fl(N)5 b Fm(\()p Fl(k)223 964 y Fk(1)242 957 y Fl(;)j(k)287 964 y Fk(2)305 957 y Fm(\))13 b(:=)f(0)h Fl(<)g Fm(abs)o(\()p Fl(k)587 964 y Fk(1)606 957 y Fl(a)630 964 y Fk(1)660 957 y Fj(\000)e Fl(k)730 964 y Fk(2)749 957 y Fl(a)773 964 y Fk(2)793 957 y Fm(\))h Fj(!)h(?)46 b Fm(and)g Fl(\026)p Fm(\()p Fl(k)1150 964 y Fk(1)1169 957 y Fl(;)8 b(k)1214 964 y Fk(2)1233 957 y Fm(\))k(:=)h(abs\()p Fl(k)1432 964 y Fk(1)1451 957 y Fl(a)1475 964 y Fk(1)1505 957 y Fj(\000)d Fl(k)1574 964 y Fk(2)1593 957 y Fl(a)1617 964 y Fk(2)1637 957 y Fm(\))p Fl(:)-12 1053 y Fm(W)l(e)15 b(ha)o(v)o(e)g(to)g(sho)o(w)f(that)h Fl(N)k Fm(is)d(progressiv)o(e.)k (T)l(o)15 b(this)g(end)h(let)g Fl(k)1122 1060 y Fk(1)1141 1053 y Fl(;)8 b(k)1186 1060 y Fk(2)1220 1053 y Fm(b)q(e)16 b(giv)o(en)g(and)f(assume)467 1149 y Fl(u)493 1156 y Fk(1)513 1149 y Fm(:)8 b Fj(8)p Fl(`)578 1156 y Fk(1)597 1149 y Fl(;)g(`)637 1156 y Fk(2)656 1149 y Fm(\()p Fl(\026)p Fm(\()p Fl(`)738 1156 y Fk(1)757 1149 y Fl(;)g(`)797 1156 y Fk(2)816 1149 y Fm(\))k Fl(<)h(\026)p Fm(\()p Fl(k)963 1156 y Fk(1)983 1149 y Fl(;)8 b(k)1028 1156 y Fk(2)1046 1149 y Fm(\))13 b Fj(!)g Fl(N)5 b Fm(\()p Fl(`)1214 1156 y Fk(1)1233 1149 y Fl(;)j(`)1273 1156 y Fk(2)1291 1149 y Fm(\)\))p Fl(:)-12 1245 y Fm(W)l(e)18 b(ha)o(v)o(e)g(to)g(pro)o(v)o(e)g Fl(N)5 b Fm(\()p Fl(k)446 1252 y Fk(1)464 1245 y Fl(;)j(k)509 1252 y Fk(2)528 1245 y Fm(\).)29 b(So,)19 b(assume)f Fl(u)854 1252 y Fk(2)873 1245 y Fm(:)8 b(0)17 b Fl(<)i(\026)p Fm(\()p Fl(k)1057 1252 y Fk(1)1076 1245 y Fl(;)8 b(k)1121 1252 y Fk(2)1140 1245 y Fm(\).)29 b(W)l(e)18 b(ha)o(v)o(e)g(to)g(sho)o(w)f Fj(?)p Fm(.)30 b(This)19 b(will)-12 1301 y(b)q(e)f(ac)o(hiev)o(ed)g(b)o (y)f(using)h(the)g(\(false\))e(assumption)i Fl(u)f Fm(at)g Fl(k)1011 1308 y Fk(1)1030 1301 y Fl(;)8 b(k)1075 1308 y Fk(2)1094 1301 y Fm(.)26 b(W)l(e)17 b(ha)o(v)o(e)g(to)f(pro)o(v)o(e)h Fl(\026)p Fm(\()p Fl(k)1571 1308 y Fk(1)1591 1301 y Fl(;)8 b(k)1636 1308 y Fk(2)1654 1301 y Fm(\))p Fj(j)p Fl(a)1709 1308 y Fk(1)1745 1301 y Fm(and)-12 1357 y Fl(\026)p Fm(\()p Fl(k)57 1364 y Fk(1)76 1357 y Fl(;)g(k)121 1364 y Fk(2)140 1357 y Fm(\))p Fj(j)p Fl(a)195 1364 y Fk(2)214 1357 y Fm(.)37 b(Informally)l(,)23 b(one)d(w)o(ould)i(argue)e(\\if,)i(sa)o(y)l (,)g Fl(\026)p Fm(\()p Fl(k)1105 1364 y Fk(1)1124 1357 y Fl(;)8 b(k)1169 1364 y Fk(2)1188 1357 y Fm(\))p Fj(6)k(j)o Fl(a)1254 1364 y Fk(1)1295 1357 y Fm(then)21 b(the)g(remainder)g Fl(r)1729 1364 y Fk(1)1771 1357 y Fm(:=)-12 1414 y Fl(r)q Fm(\()p Fl(a)52 1421 y Fk(1)71 1414 y Fl(;)8 b(\026)p Fm(\()p Fl(k)161 1421 y Fk(1)180 1414 y Fl(;)g(k)225 1421 y Fk(2)243 1414 y Fm(\)\))17 b(is)g(p)q(ositiv)o(e)h(and)f(less)h (than)f Fl(\026)p Fm(\()p Fl(k)866 1421 y Fk(1)885 1414 y Fl(;)8 b(k)930 1421 y Fk(2)949 1414 y Fm(\).)25 b(F)l(urthermore)16 b(w)o(e)h(can)g(\014nd)h Fl(`)1536 1421 y Fk(1)1555 1414 y Fl(;)8 b(`)1595 1421 y Fk(2)1631 1414 y Fm(suc)o(h)17 b(that)-12 1470 y Fl(r)9 1477 y Fk(1)50 1470 y Fm(=)23 b Fl(\026)p Fm(\()p Fl(`)172 1477 y Fk(1)191 1470 y Fl(;)8 b(`)231 1477 y Fk(2)250 1470 y Fm(\).)37 b(Altogether)20 b(this)i(con)o(tradicts)e(the)h(assumption)g Fl(u)1239 1477 y Fk(1)1259 1470 y Fm(".)36 b(More)21 b(formally)l(,)h(to)e(pro)o (v)o(e)-12 1527 y Fl(\026)p Fm(\()p Fl(k)57 1534 y Fk(1)76 1527 y Fl(;)8 b(k)121 1534 y Fk(2)140 1527 y Fm(\))p Fj(j)p Fl(a)195 1534 y Fk(1)229 1527 y Fm(w)o(e)15 b(use)h(the)f(lemma) 444 1623 y Fl(v)466 1630 y Fk(2)486 1623 y Fm(:)8 b Fj(8)p Fl(a;)g(q)r(;)g(c;)g(r)p Fm(\()p Fl(a)i Fm(=)j Fl(q)r(c)c Fm(+)i Fl(r)i Fj(!)g Fm(\(0)f Fl(<)h(r)h Fj(!)f(?)p Fm(\))f Fj(!)h Fl(c)p Fj(j)p Fl(a)p Fm(\))-12 1719 y(at)h Fl(a)67 1726 y Fk(1)87 1719 y Fm(,)h Fl(q)135 1726 y Fk(1)168 1719 y Fm(:=)d Fl(q)r Fm(\()p Fl(a)292 1726 y Fk(1)312 1719 y Fl(;)c(\026)p Fm(\()p Fl(k)402 1726 y Fk(1)420 1719 y Fl(;)g(k)465 1726 y Fk(2)484 1719 y Fm(\)\))14 b(\(the)h(quotien)o(t\),)g Fl(\026)p Fm(\()p Fl(k)909 1726 y Fk(1)928 1719 y Fl(;)8 b(k)973 1726 y Fk(2)992 1719 y Fm(\))15 b(and)g Fl(r)1134 1726 y Fk(1)1153 1719 y Fm(.)20 b(W)l(e)15 b(ha)o(v)o(e)g(to)g(pro)o(v)o(e)f(the)i(premises) 501 1815 y Fl(a)525 1822 y Fk(1)558 1815 y Fm(=)d Fl(q)626 1822 y Fk(1)646 1815 y Fl(\026)p Fm(\()p Fl(k)715 1822 y Fk(1)734 1815 y Fl(;)8 b(k)779 1822 y Fk(2)798 1815 y Fm(\))i(+)g Fl(r)892 1822 y Fk(1)957 1815 y Fm(and)45 b(0)13 b Fl(<)g(r)1180 1822 y Fk(1)1212 1815 y Fj(!)g(?)-12 1911 y Fm(of)i(the)g(instan)o(tiated)h(lemma)f Fl(v)538 1918 y Fk(2)558 1911 y Fm(.)20 b(Here)15 b(w)o(e)g(need)h(the)f (lemmata)516 1995 y Fl(v)538 2002 y Fk(3)558 1995 y Fm(:)8 b Fj(8)p Fl(a;)g(c)p Fm(\(0)i Fl(<)j(c)f Fj(!)h Fl(a)g Fm(=)g Fl(q)r Fm(\()p Fl(a;)8 b(c)p Fm(\))p Fl(c)g Fm(+)i Fl(r)q Fm(\()p Fl(a;)e(c)p Fm(\)\))p Fl(;)516 2052 y(v)538 2059 y Fk(4)558 2052 y Fm(:)g Fj(8)p Fl(a;)g(c)p Fm(\(0)i Fl(<)j(c)f Fj(!)h Fl(r)q Fm(\()p Fl(a;)8 b(c)p Fm(\))j Fl(<)i(c)p Fm(\))-12 2148 y(sp)q(ecifying)18 b(the)e(functions)g (quotien)o(t)h(and)f(remainder.)22 b(No)o(w)16 b(the)g(\014rst)f (premise)i(follo)o(ws)f(immediately)-12 2204 y(from)f(lemma)h Fl(v)265 2211 y Fk(3)301 2204 y Fm(and)g Fl(u)416 2211 y Fk(2)436 2204 y Fm(:)8 b(0)13 b Fl(<)h(\026)p Fm(\()p Fl(k)611 2211 y Fk(1)631 2204 y Fl(;)8 b(k)676 2211 y Fk(2)694 2204 y Fm(\).)22 b(T)l(o)16 b(pro)o(v)o(e)f(the)h(second)h (premise,)f(0)e Fl(<)g(r)1452 2211 y Fk(1)1486 2204 y Fj(!)g(?)p Fm(,)i(w)o(e)g(assume)-12 2261 y Fl(u)14 2268 y Fk(3)34 2261 y Fm(:)8 b(0)17 b Fl(<)h(r)169 2268 y Fk(1)207 2261 y Fm(and)h(sho)o(w)e Fj(?)p Fm(.)30 b(First)19 b(w)o(e)f(compute)g Fl(`)883 2268 y Fk(1)903 2261 y Fl(;)8 b(`)943 2268 y Fk(2)980 2261 y Fm(suc)o(h)19 b(that)f Fl(r)1209 2268 y Fk(1)1246 2261 y Fm(=)h Fl(\026)p Fm(\()p Fl(`)1364 2268 y Fk(1)1383 2261 y Fl(;)8 b(`)1423 2268 y Fk(2)1442 2261 y Fm(\).)30 b(This)19 b(is)g(done)g(b)o(y)-12 2317 y(some)c(auxiliary)h(function)g Fl(f)5 b Fm(,)15 b(de\014ned)i(b)o(y)325 2431 y Fl(f)5 b Fm(\()p Fl(a)394 2438 y Fk(1)414 2431 y Fl(;)j(a)459 2438 y Fk(2)478 2431 y Fl(;)g(k)523 2438 y Fk(1)541 2431 y Fl(;)g(k)586 2438 y Fk(2)605 2431 y Fl(;)g(q)r Fm(\))j(:=)738 2371 y Ff(\032)777 2402 y Fl(q)r(k)823 2409 y Fk(1)852 2402 y Fj(\000)g Fm(1)p Fl(;)44 b Fm(if)16 b Fl(k)1044 2409 y Fk(2)1063 2402 y Fl(a)1087 2409 y Fk(2)1120 2402 y Fl(<)d(k)1192 2409 y Fk(1)1211 2402 y Fl(a)1235 2409 y Fk(1)1270 2402 y Fm(and)i(0)e Fl(<)g(q)r Fm(;)777 2459 y Fl(q)r(k)823 2466 y Fk(1)852 2459 y Fm(+)e(1)p Fl(;)44 b Fm(otherwise.)892 2577 y(3)p eop %%Page: 4 4 4 3 bop -12 307 a Fl(f)20 b Fm(satis\014es)c(the)f(lemma)153 406 y Fl(v)175 413 y Fk(5)195 406 y Fm(:)8 b Fj(8)p Fl(a)265 413 y Fk(1)284 406 y Fl(;)g(a)329 413 y Fk(2)348 406 y Fl(;)g(k)393 413 y Fk(1)411 406 y Fl(;)g(k)456 413 y Fk(2)475 406 y Fl(;)g(q)r(;)g(r)q Fm(\()p Fl(a)603 413 y Fk(1)633 406 y Fm(=)13 b Fl(q)f Fj(\001)e Fl(\026)p Fm(\()p Fl(k)805 413 y Fk(1)824 406 y Fl(;)e(k)869 413 y Fk(2)888 406 y Fm(\))h(+)i Fl(r)i Fj(!)g Fl(r)h Fm(=)f Fl(\026)p Fm(\()p Fl(f)5 b Fm(\()p Fl(a)1250 413 y Fk(1)1269 406 y Fl(;)j(a)1314 413 y Fk(2)1333 406 y Fl(;)g(k)1378 413 y Fk(1)1397 406 y Fl(;)g(k)1442 413 y Fk(2)1461 406 y Fl(;)g(q)r Fm(\))p Fl(;)g(q)r(k)1589 413 y Fk(2)1606 406 y Fm(\)\))p Fl(:)-12 506 y Fm(Hence)15 b(w)o(e)g(let)g Fl(`)273 513 y Fk(1)305 506 y Fm(:=)e Fl(f)5 b Fm(\()p Fl(a)435 513 y Fk(1)454 506 y Fl(;)j(a)499 513 y Fk(2)518 506 y Fl(;)g(k)563 513 y Fk(1)582 506 y Fl(;)g(k)627 513 y Fk(2)645 506 y Fl(;)g(q)686 513 y Fk(1)706 506 y Fm(\))14 b(and)h Fl(`)845 513 y Fk(2)877 506 y Fm(:=)e Fl(q)958 513 y Fk(1)978 506 y Fl(k)1002 513 y Fk(2)1021 506 y Fm(.)20 b(No)o(w)14 b(w)o(e)g(ha)o(v)o(e)g Fl(\026)p Fm(\()p Fl(`)1391 513 y Fk(1)1411 506 y Fl(;)8 b(`)1451 513 y Fk(2)1470 506 y Fm(\))k(=)h Fl(r)1569 513 y Fk(1)1601 506 y Fl(<)g(\026)p Fm(\()p Fl(k)1718 513 y Fk(1)1737 506 y Fl(;)8 b(k)1782 513 y Fk(2)1801 506 y Fm(\))-12 562 y(b)o(y)17 b Fl(v)75 569 y Fk(5)95 562 y Fm(,)g Fl(u)151 569 y Fk(2)188 562 y Fm(and)g Fl(v)300 569 y Fk(4)319 562 y Fm(,)h(as)e(w)o(ell)i(as)f(0)e Fl(<)h(r)669 569 y Fk(1)704 562 y Fm(=)g Fl(\026)p Fm(\()p Fl(`)819 569 y Fk(1)839 562 y Fl(;)8 b(`)879 569 y Fk(2)898 562 y Fm(\))17 b(b)o(y)g Fl(u)1024 569 y Fk(3)1060 562 y Fm(and)h Fl(v)1173 569 y Fk(5)1192 562 y Fm(.)26 b(Therefore,)17 b(w)o(e)g(get)f Fj(?)i Fm(b)o(y)f Fl(u)1742 569 y Fk(1)1778 562 y Fm(at)-12 619 y Fl(`)7 626 y Fk(1)27 619 y Fl(;)8 b(`)67 626 y Fk(2)102 619 y Fm(\(using)18 b(some)e(equalit)o(y)i (lemmata\).)24 b(This)17 b(completes)h(the)f(pro)q(of)f(of)h Fl(\026)p Fm(\()p Fl(k)1398 626 y Fk(1)1417 619 y Fl(;)8 b(k)1462 626 y Fk(2)1481 619 y Fm(\))p Fj(j)p Fl(a)1536 626 y Fk(1)1555 619 y Fm(.)25 b Fl(\026)p Fm(\()p Fl(k)1662 626 y Fk(1)1681 619 y Fl(;)8 b(k)1726 626 y Fk(2)1745 619 y Fm(\))p Fj(j)p Fl(a)1800 626 y Fk(2)-12 675 y Fm(is)16 b(pro)o(v)o(ed)e(similarly)j(using)f(the)g(lemma)153 774 y Fl(v)175 781 y Fk(6)195 774 y Fm(:)8 b Fj(8)p Fl(a)265 781 y Fk(1)284 774 y Fl(;)g(a)329 781 y Fk(2)348 774 y Fl(;)g(k)393 781 y Fk(1)411 774 y Fl(;)g(k)456 781 y Fk(2)475 774 y Fl(;)g(q)r(;)g(r)q Fm(\()p Fl(a)603 781 y Fk(2)633 774 y Fm(=)13 b Fl(q)f Fj(\001)e Fl(\026)p Fm(\()p Fl(k)805 781 y Fk(1)824 774 y Fl(;)e(k)869 781 y Fk(2)888 774 y Fm(\))h(+)i Fl(r)i Fj(!)g Fl(r)h Fm(=)f Fl(\026)p Fm(\()p Fl(q)r(k)1227 781 y Fk(1)1246 774 y Fl(;)8 b(f)d Fm(\()p Fl(a)1336 781 y Fk(2)1355 774 y Fl(;)j(a)1400 781 y Fk(1)1419 774 y Fl(;)g(k)1464 781 y Fk(2)1482 774 y Fl(;)g(k)1527 781 y Fk(1)1546 774 y Fl(;)g(q)r Fm(\)\)\))p Fl(:)-12 922 y Fi(The)18 b(re\014ned)f Fl(A)p Fi({translation.)59 1002 y Fm(The)c(pro)q(of)f(of)g(the)h (principle)j(of)d Fl(<)p Fm({induction)h(and)f(the)g(pro)q(of)g(of)f (the)h(theorem)g(w)o(ere)f(giv)o(en)i(in)f(suc)o(h)-12 1059 y(a)j(detail)h(that)e(it)h(is)h(no)o(w)e(easy)h(to)f(formalize)i (them)f(completely)l(.)23 b(Only)18 b(some)d(argumen)o(ts)g(concerning) -12 1115 y Fl(<)h Fm(and)f(=)h(w)o(ere)f(left)h(implicit.)23 b(W)l(e)16 b(will)h(no)o(w)e(brie\015y)h(recall)h(the)f(term)f (extraction)g(pro)q(cess)h(describ)q(ed)-12 1171 y(in)g([1)o(,)f(2])g (in)h(general,)f(and)g(will)i(see)f(that)e(w)o(e)h(don't)g(need)h(to)e (w)o(orry)g(ab)q(out)h(these)h(omissions.)59 1228 y(Let)i Fj(8)o Fl(~)-22 b(x)194 1235 y Fk(1)214 1228 y Fl(C)247 1235 y Fk(1)266 1228 y Fl(;)8 b(:)g(:)g(:)d(;)j Fj(8)o Fl(~)-22 b(x)419 1235 y Fg(`)435 1228 y Fl(C)468 1235 y Fg(`)502 1228 y Fm(b)q(e)19 b(\005{form)o(ulas)f(\(i.e.)29 b Fl(C)950 1235 y Fg(i)982 1228 y Fm(quan)o(ti\014er)18 b(free\))g(and)h Fl(A)1423 1235 y Fk(1)1443 1228 y Fl(;)8 b(:)g(:)g(:)t(;)g(A)1578 1235 y Fg(m)1629 1228 y Fm(quan)o(ti\014er)-12 1284 y(free)17 b(form)o(ulas)g(\(in)h(our)f(example)h Fl(C)633 1291 y Fk(1)668 1284 y Fj(\021)f Fm(0)f Fl(<)g(a)834 1291 y Fk(2)871 1284 y Fm(\()o Fl(~)-22 b(x)915 1291 y Fk(1)952 1284 y Fm(is)18 b(empt)o(y\),)e Fl(A)1205 1291 y Fk(1)1241 1284 y Fj(\021)h Fm(abs\()p Fl(a)1401 1291 y Fk(1)1420 1284 y Fl(k)1444 1291 y Fk(1)1475 1284 y Fj(\000)12 b Fl(a)1546 1291 y Fk(2)1566 1284 y Fl(k)1590 1291 y Fk(2)1609 1284 y Fm(\))p Fj(j)p Fl(a)1664 1291 y Fk(1)1683 1284 y Fm(,)17 b Fl(A)1747 1291 y Fk(2)1783 1284 y Fj(\021)-12 1341 y Fm(abs\()p Fl(a)96 1348 y Fk(1)115 1341 y Fl(k)139 1348 y Fk(1)169 1341 y Fj(\000)10 b Fl(a)238 1348 y Fk(2)258 1341 y Fl(k)282 1348 y Fk(2)301 1341 y Fm(\))p Fj(j)p Fl(a)356 1348 y Fk(2)375 1341 y Fm(,)15 b Fl(A)437 1348 y Fk(3)470 1341 y Fj(\021)e Fm(0)f Fl(<)h Fm(abs\()p Fl(a)709 1348 y Fk(1)728 1341 y Fl(k)752 1348 y Fk(1)782 1341 y Fj(\000)d Fl(a)851 1348 y Fk(2)871 1341 y Fl(k)895 1348 y Fk(2)914 1341 y Fm(\)\).)19 b(Assume)d(w)o(e)f (ha)o(v)o(e)g(a)g(classical)h(pro)q(of)f(of)418 1440 y Fj(8)m Fl(~)-20 b(a)p Fm(\()p Fj(8)o Fl(~)e(x)536 1447 y Fk(1)556 1440 y Fl(C)589 1447 y Fk(1)621 1440 y Fj(!)13 b Fl(:)8 b(:)g(:)i Fj(!)j(8)o Fl(~)-22 b(x)853 1447 y Fg(`)870 1440 y Fl(C)903 1447 y Fg(`)932 1440 y Fj(!)13 b(9)1013 1428 y Fl(~)1015 1440 y(k)q Fm(\()p Fl(A)1092 1447 y Fk(1)1112 1440 y Fj(^)p Fl(;)8 b(:)g(:)g(:)d(;)j Fj(^)p Fl(A)1308 1447 y Fg(m)1341 1440 y Fm(\)\))p Fl(;)-12 1539 y Fm(i.e.,)15 b(a)g(deduction)317 1639 y Fl(d)p Fm([)p Fl(u)p Fm(:)8 b Fj(8)424 1627 y Fl(~)426 1639 y(k)p Fm(\()p Fl(A)502 1646 y Fk(1)534 1639 y Fj(!)13 b Fl(:)8 b(:)g(:)j Fj(!)i Fl(A)750 1646 y Fg(m)796 1639 y Fj(!)g(?)p Fm(\))p Fl(;)8 b(v)950 1646 y Fk(1)969 1639 y Fm(:)g Fj(8)o Fl(~)-22 b(x)1041 1646 y Fk(1)1060 1639 y Fl(C)1093 1646 y Fk(1)1112 1639 y Fl(;)8 b(:)g(:)g(:)d(;)j(v)1236 1646 y Fg(`)1252 1639 y Fm(:)g Fj(8)o Fl(~)-22 b(x)1324 1646 y Fg(`)1340 1639 y Fl(C)1373 1646 y Fg(`)1389 1639 y Fl(;)8 b Fm(]:)g Fj(?)p Fl(:)-12 1738 y Fm(T)l(o)16 b(k)o(eep)h(the)f(deriv)m(ation)i(short)e(w)o(e)g(allo)o(w)h(auxiliary) g(lemmata)f Fl(v)1160 1745 y Fg(`)p Fk(+1)1222 1738 y Fm(:)8 b Fj(8)o Fl(~)-22 b(x)1294 1745 y Fg(`)p Fk(+1)1355 1738 y Fl(C)1388 1745 y Fg(`)p Fk(+1)1449 1738 y Fl(;)8 b(:)g(:)g(:)d(;)j(v)1573 1745 y Fg(n)1596 1738 y Fm(:)g Fj(8)o Fl(~)-22 b(x)1668 1745 y Fg(n)1691 1738 y Fl(C)1724 1745 y Fg(n)1763 1738 y Fm(as-)-12 1794 y(serting)15 b(true)g(\005{form)o(ulas.)20 b(So,)14 b(in)i(fact,)f(w)o(e)g(ha)o(v)o (e)727 1894 y Fl(d)p Fm([)p Fl(u;)8 b(v)833 1901 y Fk(1)852 1894 y Fl(;)g(:)g(:)g(:)d(;)j(v)976 1901 y Fg(n)998 1894 y Fm(]:)g Fj(?)p Fl(:)-12 1993 y Fm(W)l(e)15 b(sk)o(etc)o(h)g(the)g (main)h(steps)f(leading)i(from)d(this)i(deriv)m(ation)g(to)f(an)g(in)o (tuitionistic)j(pro)q(of)c(of)659 2092 y Fl(A)f Fm(:=)g Fj(9)792 2074 y Fe(\003)809 2080 y Fl(~)812 2092 y(k)q Fm(\()p Fl(A)889 2099 y Fk(1)918 2092 y Fj(^)e Fl(:)d(:)g(:)g Fj(^)i Fl(A)1096 2099 y Fg(m)1130 2092 y Fm(\))-12 2192 y(\()p Fj(9)31 2175 y Fe(\003)66 2192 y Fm(is)15 b(the)h(constructiv)o (e)f(existen)o(tial)i(quan)o(ti\014er\))e(and)g(hence)i(to)d(terms)h (computing)h(a)e(witness)1702 2180 y Fl(~)1704 2192 y(k)q Fm(.)43 2283 y(1.)23 b(Let)c Fl(L)g Fm(:=)g Fj(f)p Fl(A)361 2290 y Fk(1)399 2283 y Fj(!)h Fl(:)8 b(:)g(:)17 b Fj(!)i Fl(A)634 2290 y Fg(m)687 2283 y Fj(!)g(?)p Fl(;)8 b(C)840 2290 y Fk(1)859 2283 y Fl(;)g(:)g(:)g(:)d(;)j(C)994 2290 y Fg(n)1016 2283 y Fj(g)p Fm(.)31 b(Determine)19 b(inductiv)o(ely)j (the)d Fl(L)p Fh({critic)n(al)102 2340 y Fm(relation)e(sym)o(b)q(ols)h (as)f(follo)o(ws:)24 b(If)17 b(\()747 2328 y Fl(~)740 2340 y(D)778 2347 y Fk(1)814 2340 y Fj(!)f Fl(P)904 2347 y Fk(1)924 2340 y Fm(\))g Fj(!)g Fl(:)8 b(:)g(:)14 b Fj(!)j Fm(\()1175 2328 y Fl(~)1168 2340 y(D)1206 2347 y Fg(m)1255 2340 y Fj(!)f Fl(P)1345 2347 y Fg(m)1379 2340 y Fm(\))f Fj(!)i Fl(R)p Fm(\()1524 2331 y Fl(~)1527 2340 y(t)p Fm(\))g(is)h(a)f(p)q(ositiv)o(e)102 2396 y(subform)o(ula)11 b(of)h(a)f(form)o(ula)g(in)i Fl(L)p Fm(,)f(and)g(for)f(some)g Fl(i)p Fm(,)h Fl(P)1016 2403 y Fg(i)1043 2396 y Fj(\021)h(?)f Fm(or)f Fl(P)1219 2403 y Fg(i)1246 2396 y Fj(\021)i Fl(Q)p Fm(\()n Fl(~)-21 b(s)p Fm(\))11 b(where)h Fl(Q)g Fm(is)g Fl(L)p Fm({critical,)102 2452 y(then)j Fl(R)g Fm(is)h Fl(L)p Fm({critical)g(to)q(o.)892 2577 y(4)p eop %%Page: 5 5 5 4 bop 43 307 a Fm(2.)23 b(F)l(or)9 b(eac)o(h)i(form)o(ula)f Fl(F)17 b Fm(let)11 b(its)f Fl(A)p Fh({tr)n(anslation)g Fl(F)918 291 y Fg(A)957 307 y Fm(b)q(e)i(the)e(form)o(ula)g(obtained)h (from)f Fl(F)17 b Fm(b)o(y)10 b(replacing)102 364 y Fj(?)17 b Fm(b)o(y)g Fl(A)g Fm(and)g(eac)o(h)g(subform)o(ula)g Fl(R)p Fm(\()n Fl(~)-21 b(s)p Fm(\),)16 b(where)h Fl(R)g Fm(is)h Fl(L)p Fm({critical,)g(b)o(y)f(\()p Fl(R)p Fm(\()n Fl(~)-21 b(s)o Fm(\))15 b Fj(!)h Fl(A)p Fm(\))g Fj(!)g Fl(A)p Fm(.)25 b(Find)102 420 y(deriv)m(ations)367 522 y Fl(d)391 529 y Fg(u)413 522 y Fm(:)8 b Fj(8)457 510 y Fl(~)459 522 y(k)q Fm(\()p Fl(A)536 529 y Fk(1)568 522 y Fj(!)13 b Fl(:)8 b(:)g(:)j Fj(!)i Fl(A)784 529 y Fg(m)830 522 y Fj(!)g(?)p Fm(\))941 503 y Fg(A)969 522 y Fl(;)53 b Fm(and)46 b Fl(d)1178 529 y Fg(v)1195 534 y Fd(i)1210 522 y Fm([)p Fl(v)1245 529 y Fg(i)1259 522 y Fm(:)8 b Fj(8)o Fl(~)-22 b(x)1331 529 y Fg(i)1344 522 y Fl(C)1377 529 y Fg(i)1391 522 y Fm(]:)8 b Fj(8)o Fl(~)-22 b(x)1476 529 y Fg(i)1489 522 y Fl(C)1525 503 y Fg(A)1522 533 y(i)102 624 y Fm(follo)o(wing)15 b(the)h(recip)q(e)g (giv)o(en)g(in)g([2].)43 718 y(3.)23 b(Replace)15 b(in)f Fl(d)p Fm([)p Fl(u;)8 b(v)427 725 y Fk(1)446 718 y Fl(;)g(:)g(:)g(:)t (;)g(v)569 725 y Fg(n)592 718 y Fm(]:)g Fj(?)13 b Fm(eac)o(h)h(form)o (ula)f(b)o(y)g(its)h Fl(A)p Fm({translation.)19 b(W)l(e)14 b(obtain)g(a)f(deriv)m(ation)730 820 y Fl(d)754 827 y Fg(A)782 820 y Fm([)p Fl(u)821 827 y Fg(A)849 820 y Fl(;)8 b(v)892 827 y Fk(1)p Fg(A)938 820 y Fl(;)g(:)g(:)g(:)d(;)j(v)1062 827 y Fg(nA)1111 820 y Fm(]:)g Fl(A;)102 922 y Fm(where)18 b Fl(u)262 929 y Fg(A)291 922 y Fm(:)8 b Fj(8)335 910 y Fl(~)337 922 y(k)p Fm(\()p Fl(A)413 906 y Fg(A)413 934 y Fk(1)459 922 y Fj(!)18 b Fl(:)8 b(:)g(:)16 b Fj(!)i Fl(A)690 906 y Fg(A)690 934 y(m)741 922 y Fj(!)h Fl(A)p Fm(\))f(and)g Fl(v)988 929 y Fg(iA)1029 922 y Fm(:)8 b Fj(8)o Fl(~)-22 b(x)1101 929 y Fg(i)1114 922 y Fl(C)1150 906 y Fg(A)1147 934 y(i)1197 922 y Fm(\(induction)19 b(axioms)f(are)g(replaced)102 979 y(b)o(y)f(new)h(induction)h(axioms)f (for)f(the)h Fl(A)p Fm({translated)f(form)o(ulas\).)26 b(F)l(urthermore)17 b(replace)i(in)g(the)102 1035 y(deriv)m(ation)c(ab) q(o)o(v)o(e)f(the)g(free)h(assumptions)f(b)o(y)h(the)f(deriv)m(ations)h (constructed)g(in)g(step)f(2.)20 b(W)l(e)14 b(get)102 1092 y(the)h(translated)g(deriv)m(ation)572 1194 y Fl(d)596 1175 y Fk(tr)625 1194 y Fm([)p Fl(v)660 1201 y Fk(1)680 1194 y Fl(;)8 b(:)g(:)g(:)t(;)g(v)803 1201 y Fg(n)826 1194 y Fm(])k(:=)h Fl(d)936 1201 y Fg(A)964 1194 y Fm([)p Fl(d)1001 1201 y Fg(u)1023 1194 y Fl(;)8 b(d)1068 1201 y Fg(v)1085 1206 y Fc(1)1103 1194 y Fl(;)g(:)g(:)g(:)d(;)j(d)1229 1201 y Fg(v)1246 1205 y Fd(n)1269 1194 y Fm(]:)g Fl(A:)43 1315 y Fm(4.)23 b(Apply)16 b(Kreisel's)g(mo)q(di\014ed)h(realizabilit)o (y)h(in)o(terpretation)d([4)o(])g(to)g(extract)f(a)h(\014nite)h(list)g (of)f(terms)844 1417 y Fl(~)-21 b(r)13 b Fm(:=)g(\()p Fl(d)983 1398 y Fk(tr)1012 1417 y Fm(\))1030 1398 y Fk(ets)102 1519 y Fm(suc)o(h)i(that)g Fl(A)337 1526 y Fk(1)356 1519 y Fm([)o Fl(~)-22 b(r)q(=)412 1507 y(~)414 1519 y(k)q Fm(])9 b Fj(^)i Fl(:)d(:)g(:)g Fj(^)i Fl(A)639 1526 y Fg(m)673 1519 y Fm([)o Fl(~)-22 b(r=)728 1507 y(~)730 1519 y(k)q Fm(])15 b(is)g(pro)o(v)m(able)h(from)f Fl(v)1140 1526 y Fk(1)1160 1519 y Fl(;)8 b(:)g(:)g(:)t(;)g(v)1283 1526 y Fk(6)1302 1519 y Fm(.)-12 1613 y Fh(Comments.)56 1707 y Fm({)23 b(T)l(erm)16 b(extraction)h(comm)o(utes)g(with)g(the)g (logical)h(rules,)g(e.g.)e(\()p Fl(d)1236 1714 y Fk(1)1255 1707 y Fl(d)1279 1714 y Fk(2)1299 1707 y Fm(\))1317 1690 y Fk(ets)1378 1707 y Fm(=)f Fl(d)1452 1690 y Fk(ets)1452 1718 y(1)1498 1707 y Fl(d)1522 1690 y Fk(ets)1522 1718 y(2)1567 1707 y Fm(,)i(and)g(substi-)102 1763 y(tution,)e(i.e.)390 1865 y(\()p Fl(d)432 1846 y Fk(tr)461 1865 y Fm(\))479 1846 y Fk(ets)536 1865 y Fj(\021)e Fm(\()p Fl(d)626 1872 y Fg(A)654 1865 y Fm([)p Fl(d)691 1872 y Fg(u)713 1865 y Fl(;)8 b(d)758 1872 y Fg(v)775 1877 y Fc(1)794 1865 y Fl(;)g(:)g(:)g(:)t(;)g(d)919 1872 y Fg(v)936 1876 y Fd(n)959 1865 y Fm(]\))990 1846 y Fk(ets)1047 1865 y Fj(\021)13 b Fl(d)1119 1846 y Fk(ets)1119 1876 y Fg(A)1164 1865 y Fm([)p Fl(d)1201 1846 y Fk(ets)1201 1876 y Fg(u)1246 1865 y Fl(;)8 b(d)1291 1846 y Fk(ets)1291 1876 y Fg(v)1308 1881 y Fc(1)1335 1865 y Fl(;)g(:)g(:)g(:)d(;)j(d)1461 1846 y Fk(ets)1461 1876 y Fg(v)1478 1880 y Fd(n)1505 1865 y Fm(])p Fl(:)102 1967 y Fm(By)16 b(the)f(latter)h(w)o(e)f(ma)o(y) g(\014rst)h(extract)f(terms)g(from)g(the)h(deriv)m(ations)h Fl(d)1364 1974 y Fg(A)1392 1967 y Fl(;)8 b(d)1437 1974 y Fg(v)1454 1979 y Fc(1)1473 1967 y Fl(;)g(:)g(:)g(:)d(;)j(d)1599 1974 y Fg(v)1616 1978 y Fd(n)1654 1967 y Fm(and)16 b(also)102 2024 y(from)k(the)h(pro)q(of)g(of)g Fl(<)p Fm({induction)i(separately)l (,)f(and)f(then)h(substitute)g(these)f(terms)f(in)o(to)i(the)102 2080 y(terms)14 b(extracted)h(from)g Fl(d)561 2087 y Fg(A)589 2080 y Fm([)p Fl(u)628 2087 y Fg(A)656 2080 y Fl(;)8 b(v)699 2087 y Fk(1)p Fg(A)744 2080 y Fl(;)g(:)g(:)g(:)d(;)j (v)868 2087 y Fg(nA)917 2080 y Fm(]:)g Fl(A)p Fm(.)56 2174 y({)23 b(Assume)16 b(that)g(w)o(e)g(ha)o(v)o(e)g(\014xed)h(some)f (system)g(of)g(lemmata)g Fj(8)o Fl(~)-22 b(x)1215 2181 y Fk(1)1234 2174 y Fl(C)1267 2181 y Fk(1)1287 2174 y Fl(;)8 b(:)g(:)g(:)d(;)j Fj(8)o Fl(~)-22 b(x)1440 2181 y Fg(n)1462 2174 y Fl(C)1495 2181 y Fg(n)1535 2174 y Fm(and)16 b(computed)102 2230 y(the)d Fl(L)p Fm(-critical)i(relation)f (sym)o(b)q(ols)f(according)h(to)e(step)i(1.)19 b(Then)13 b(it's)g(clear)h(that)f(w)o(e)g(ma)o(y)f(use)i(an)o(y)102 2287 y(other)g(true)h Fj(!)e(8)p Fm({form)o(ula)h Fl(D)i Fm(as)e(a)h(further)g(lemma,)f(pro)o(vided)i Fl(D)g Fm(do)q(es)f (neither)h(con)o(tain)f Fj(?)g Fm(nor)102 2343 y(an)o(y)f Fl(L)p Fm({critical)i(relation)f(sym)o(b)q(ol.)20 b(The)15 b(simple)i(reason)d(is,)h(that)f(in)i(this)f(case)g Fl(D)1539 2327 y Fg(A)1580 2343 y Fj(\021)e Fl(D)q Fm(.)19 b(In)d(the)102 2400 y(sequel)g(w)o(e)f(will)i(call)f(suc)o(h)g(form)o(ulas)e Fl(D)i Fh(harmless)p Fm(.)892 2577 y(5)p eop %%Page: 6 6 6 5 bop -12 307 a Fi(Computing)18 b(the)g Fl(L)p Fi({critical)h (relation)g(sym)o(b)q(ols.)59 389 y Fm(No)o(w)c(w)o(e)h(come)g(bac)o(k) h(to)e(our)h(example.)24 b(Let)17 b(us)f(rep)q(eat)h(the)f(main)h (lemmata)f(used)h(in)g(the)f(pro)q(ofs)-12 445 y(of)f(the)g(principle)j (of)d Fl(<)p Fm({induction)i(and)e(the)h(theorem.)190 547 y Fl(v)212 554 y Fk(0)232 547 y Fm(:)8 b(0)k Fl(<)h(a)360 554 y Fk(2)380 547 y Fl(;)190 616 y(v)212 623 y Fk(1)232 616 y Fm(:)8 b Fj(8)p Fl(m)p Fm(\()p Fl(m)k(<)h Fm(0)f Fj(!)h(?)p Fm(\))p Fl(;)190 685 y(v)212 692 y Fk(2)232 685 y Fm(:)8 b Fj(8)p Fl(a;)g(q)r(;)g(c;)g(r)p Fm(\()p Fl(a)i Fm(=)j Fl(q)r(c)d Fm(+)g Fl(r)k Fj(!)f Fm(\(0)f Fl(<)h(r)g Fj(!)g(?)p Fm(\))g Fj(!)g Fl(c)p Fj(j)p Fl(a)p Fm(\))p Fl(;)190 754 y(v)212 761 y Fk(3)232 754 y Fm(:)8 b Fj(8)p Fl(a;)g(c)p Fm(\(0)j Fl(<)i(c)f Fj(!)h Fl(a)g Fm(=)g Fl(q)r Fm(\()p Fl(a;)8 b(c)p Fm(\))p Fl(c)g Fm(+)i Fl(r)q Fm(\()p Fl(a;)e(c)p Fm(\)\))p Fl(;)190 823 y(v)212 830 y Fk(4)232 823 y Fm(:)g Fj(8)p Fl(a;)g(c)p Fm(\(0)j Fl(<)i(c)f Fj(!)h Fl(r)q Fm(\()p Fl(a;)8 b(c)p Fm(\))j Fl(<)i(c)p Fm(\))p Fl(;)190 892 y(v)212 899 y Fk(5)232 892 y Fm(:)8 b Fj(8)p Fl(a)302 899 y Fk(1)321 892 y Fl(;)g(a)366 899 y Fk(2)385 892 y Fl(;)g(k)430 899 y Fk(1)449 892 y Fl(;)g(k)494 899 y Fk(2)513 892 y Fl(;)g(q)r(;)g(r)q Fm(\()p Fl(a)641 899 y Fk(1)671 892 y Fm(=)13 b Fl(q)f Fj(\001)d Fl(\026)p Fm(\()p Fl(k)842 899 y Fk(1)862 892 y Fl(;)f(k)907 899 y Fk(2)925 892 y Fm(\))i(+)h Fl(r)i Fj(!)g Fl(r)h Fm(=)f Fl(\026)p Fm(\()p Fl(f)5 b Fm(\()p Fl(a)1288 899 y Fk(1)1307 892 y Fl(;)j(a)1352 899 y Fk(2)1371 892 y Fl(;)g(k)1416 899 y Fk(1)1435 892 y Fl(;)g(k)1480 899 y Fk(2)1498 892 y Fl(;)g(q)r Fm(\))p Fl(;)g(q)r(k)1626 899 y Fk(2)1644 892 y Fm(\)\))p Fl(;)190 961 y(v)212 968 y Fk(6)232 961 y Fm(:)g Fj(8)p Fl(a)302 968 y Fk(1)321 961 y Fl(;)g(a)366 968 y Fk(2)385 961 y Fl(;)g(k)430 968 y Fk(1)449 961 y Fl(;)g(k)494 968 y Fk(2)513 961 y Fl(;)g(q)r(;)g(r)q Fm(\()p Fl(a)641 968 y Fk(2)671 961 y Fm(=)13 b Fl(q)f Fj(\001)d Fl(\026)p Fm(\()p Fl(k)842 968 y Fk(1)862 961 y Fl(;)f(k)907 968 y Fk(2)925 961 y Fm(\))i(+)h Fl(r)i Fj(!)g Fl(r)h Fm(=)f Fl(\026)p Fm(\()p Fl(q)r(k)1265 968 y Fk(1)1284 961 y Fl(;)8 b(f)d Fm(\()p Fl(a)1374 968 y Fk(2)1393 961 y Fl(;)j(a)1438 968 y Fk(1)1457 961 y Fl(;)g(k)1502 968 y Fk(2)1520 961 y Fl(;)g(k)1565 968 y Fk(1)1584 961 y Fl(;)g(q)r Fm(\)\)\))p Fl(:)-12 1063 y Fm(The)17 b(only)g(critical)g(relation)g(sym)o(b)q(ol)g(w.r.t.) 22 b Fl(v)813 1070 y Fk(0)833 1063 y Fl(;)8 b(:)g(:)g(:)d(;)j(v)957 1070 y Fk(6)992 1063 y Fm(is)17 b Fj(\001j\001)p Fm(.)22 b(Since)c(the)f(parts)f(of)g(our)g(pro)q(ofs)g(whic)o(h)-12 1119 y(w)o(ere)d(left)h(implicit)h(concerned)g(neither)f Fj(\001j\001)e Fm(nor)h Fj(?)p Fm(,)h(they)f(ma)o(y)g(b)q(e)h(view)o (ed)g(as)f(applications)h(of)f(harmless)-12 1176 y(lemmata)i(\(in)h (the)f(sense)g(of)g(the)h(second)f(commen)o(t\))g(and)g(hence)h(w)o (on't)e(cause)i(problems.)-12 1282 y Fi(F)l(ormal)h(deriv)m(ations.)59 1363 y Fm(W)l(e)h(no)o(w)g(sp)q(ell)j(out)d(the)g(deriv)m(ation)i(term) e Fl(d)p Fm([)p Fl(u;)8 b(v)947 1370 y Fk(0)966 1363 y Fl(;)g(v)1009 1370 y Fk(1)1028 1363 y Fl(;)g(:)g(:)g(:)t(;)g(v)1151 1370 y Fk(6)1170 1363 y Fm(]:)g Fj(?)18 b Fm(formalizing)i(the)e(pro)q (of)g(of)h(the)-12 1420 y(theorem.)h(W)l(e)15 b(use)g(the)h(follo)o (wing)g(abbreviations.)429 1522 y Fl(\026)p Fm(\()472 1510 y Fl(~)474 1522 y(k)q Fm(\))41 b(:=)g(abs\()p Fl(k)755 1529 y Fk(1)774 1522 y Fl(a)798 1529 y Fk(1)828 1522 y Fj(\000)11 b Fl(k)898 1529 y Fk(2)917 1522 y Fl(a)941 1529 y Fk(2)961 1522 y Fm(\))p Fl(;)422 1591 y(q)442 1598 y Fg(i)456 1591 y Fm(\()472 1579 y Fl(~)474 1591 y(k)q Fm(\))41 b(:=)g Fl(q)r Fm(\()p Fl(a)711 1598 y Fg(i)725 1591 y Fl(;)8 b(\026)p Fm(\()789 1579 y Fl(~)791 1591 y(k)q Fm(\)\))p Fl(;)421 1660 y(r)442 1667 y Fg(i)456 1660 y Fm(\()472 1648 y Fl(~)474 1660 y(k)q Fm(\))41 b(:=)g Fl(r)q Fm(\()p Fl(a)711 1667 y Fg(i)725 1660 y Fl(;)8 b(\026)p Fm(\()789 1648 y Fl(~)791 1660 y(k)p Fm(\)\))p Fl(;)417 1717 y(~)417 1729 y(`)436 1736 y Fk(1)456 1729 y Fm(\()472 1717 y Fl(~)474 1729 y(k)q Fm(\))41 b(:=)g Fl(f)5 b Fm(\()p Fl(a)716 1736 y Fk(1)736 1729 y Fl(;)j(a)781 1736 y Fk(2)800 1729 y Fl(;)g(k)845 1736 y Fk(1)864 1729 y Fl(;)g(k)909 1736 y Fk(2)927 1729 y Fl(;)g(q)968 1736 y Fk(1)987 1729 y Fm(\()1003 1717 y Fl(~)1005 1729 y(k)q Fm(\)\))p Fl(;)g(q)1107 1736 y Fk(1)1126 1729 y Fm(\()1142 1717 y Fl(~)1144 1729 y(k)p Fm(\))p Fl(k)1210 1736 y Fk(2)1230 1729 y Fl(;)417 1785 y(~)417 1797 y(`)436 1804 y Fk(2)456 1797 y Fm(\()472 1785 y Fl(~)474 1797 y(k)q Fm(\))41 b(:=)g Fl(q)667 1804 y Fk(2)687 1797 y Fm(\()703 1785 y Fl(~)705 1797 y(k)q Fm(\))p Fl(k)772 1804 y Fk(1)791 1797 y Fl(;)8 b(f)d Fm(\()p Fl(a)881 1804 y Fk(2)900 1797 y Fl(;)j(a)945 1804 y Fk(1)964 1797 y Fl(;)g(k)1009 1804 y Fk(2)1028 1797 y Fl(;)g(k)1073 1804 y Fk(1)1091 1797 y Fl(;)g(q)1132 1804 y Fk(2)1151 1797 y Fm(\()1167 1785 y Fl(~)1169 1797 y(k)q Fm(\)\))p Fl(;)415 1866 y(N)d Fm(\()473 1854 y Fl(~)475 1866 y(k)p Fm(\))41 b(:=)g(0)13 b Fl(<)g(\026)p Fm(\()774 1854 y Fl(~)776 1866 y(k)q Fm(\))f Fj(!)h(?)p Fl(;)422 1935 y Fm(Prog)41 b(:=)g Fj(8)670 1923 y Fl(~)672 1935 y(k)r Fm(\()p Fj(8)741 1923 y Fl(~)741 1935 y(`)p Fm([)p Fl(\026)p Fm(\()818 1923 y Fl(~)818 1935 y(`)o Fm(\))13 b Fl(<)g(\026)p Fm(\()958 1923 y Fl(~)960 1935 y(k)q Fm(\))f Fj(!)h Fl(N)5 b Fm(\()1133 1923 y Fl(~)1133 1935 y(`)o Fm(\)])12 b Fj(!)h Fl(N)5 b Fm(\()1310 1923 y Fl(~)1312 1935 y(k)p Fm(\)\))p Fl(;)417 2004 y(B)r Fm(\()p Fl(n)p Fm(\))42 b(:=)f Fj(8)670 1992 y Fl(~)672 2004 y(k)r Fm(\()p Fl(\026)p Fm(\()759 1992 y Fl(~)761 2004 y(k)q Fm(\))12 b Fl(<)h(n)g Fj(!)g Fl(N)5 b Fm(\()1020 1992 y Fl(~)1022 2004 y(k)p Fm(\)\))p Fl(:)-12 2106 y Fm(Recall)17 b(that,)d(using)i(the)f (abbreviations)h(ab)q(o)o(v)o(e,)f Fl(u)g Fm(denotes)g(the)g (assumption)565 2208 y Fl(u)p Fm(:)8 b Fj(8)635 2196 y Fl(~)637 2208 y(k)q Fm(\()p Fl(\026)p Fm(\()723 2196 y Fl(~)725 2208 y(k)q Fm(\))p Fj(j)p Fl(a)805 2215 y Fk(1)836 2208 y Fj(!)13 b Fl(\026)p Fm(\()937 2196 y Fl(~)939 2208 y(k)q Fm(\))p Fj(j)p Fl(a)1019 2215 y Fk(2)1051 2208 y Fj(!)g Fl(N)5 b Fm(\()1167 2196 y Fl(~)1169 2208 y(k)p Fm(\)\))p Fl(:)-12 2311 y Fm(The)20 b(deriv)m(ations)g(b)q(elo)o (w)g(are)f(giv)o(en)h(in)h(a)e(natural)g(deduction)i(calculus)g(and)f (are)f(written)g(as)g(t)o(yp)q(ed)-12 2367 y Fl(\025)p Fm({terms)e(according)h(to)g(the)g(w)o(ell{kno)o(wn)g(Curry{Ho)o(w)o (ard)f(corresp)q(ondence.)29 b(By)19 b Fl(e)f Fm(w)o(e)g(will)h(denote) -12 2423 y(\(di\013eren)o(t\))d(sub)q(deriv)m(ations)j(of)d Fl(d)h Fm(whic)o(h)g(deriv)o(e)h(a)e(harmless)h(form)o(ula)g(from)f (harmless)h(assumptions.)892 2577 y(6)p eop %%Page: 7 7 7 6 bop -12 307 a Fm(There)21 b(is)h(no)f(need)g(to)g(mak)o(e)f(them)h (explicit)i(since)g(they)e(will)h(disapp)q(ear)g(in)g(the)f(term)g (extraction)-12 364 y(pro)q(cess.)f(The)c(deriv)m(ation)g(of)f(the)g (theorem)g(is)h(giv)o(en)f(b)o(y)522 467 y Fl(d)d Fj(\021)h Fl(d)630 443 y Fk(Prog)o Fe(!8)757 434 y Fg(~)759 443 y(k)6 b(N)t Fk(\()827 434 y Fg(~)829 443 y(k)q Fk(\))630 481 y Fg(<)p Fe(\000)p Fk(ind)863 467 y Fl(d)887 448 y Fk(Prog)887 478 y(prog)963 467 y Fm(01\()p Fl(e)1048 448 y Fk(0)p Fg(<\026)p Fk(\(0)p Fg(;)p Fk(1\))1188 467 y Fm([)p Fl(v)1223 474 y Fk(0)1242 467 y Fm(]\))p Fl(;)-12 557 y Fm(where)149 647 y Fl(d)173 654 y Fg(<)p Fe(\000)p Fk(ind)320 647 y Fj(\021)42 b Fl(\025w)458 625 y Fk(Prog)457 660 y(1)533 647 y Fl(\025)558 635 y(~)560 647 y(k)q(:)p Fm(Ind)664 657 y Fg(n;B)r Fk(\()p Fg(n)p Fk(\))775 647 y Fl(d)799 654 y Fk(base)867 647 y Fl(d)891 654 y Fk(step)956 647 y Fm(\()p Fl(\026)p Fm(\()1017 635 y Fl(~)1019 647 y(k)q Fm(\))10 b(+)g(1\))1156 635 y Fl(~)1158 647 y(k)q(e)1204 629 y Fg(\026)p Fk(\()1237 620 y Fg(~)1239 629 y(k)q Fk(\))p Fg(<\026)p Fk(\()1332 620 y Fg(~)1334 629 y(k)q Fk(\)+1)1414 647 y Fl(;)186 738 y(d)210 745 y Fk(base)320 738 y Fj(\021)42 b Fl(\025)422 726 y(~)424 738 y(k)q(;)8 b(w)504 714 y Fg(\026)p Fk(\()537 705 y Fg(~)539 714 y(k)p Fk(\))p Fg(<)p Fk(0)503 750 y(0)618 738 y Fl(;)22 b Fm(~)-37 b Fl(w)672 745 y Fk(0)690 719 y(0)p Fg(<\026)p Fk(\()768 711 y Fg(~)770 719 y(k)r Fk(\))806 738 y Fl(:v)841 745 y Fk(1)860 738 y Fl(\026)p Fm(\()903 726 y Fl(~)905 738 y(k)q Fm(\))p Fl(w)981 745 y Fk(0)1000 738 y Fl(;)190 824 y(d)214 831 y Fk(step)320 824 y Fj(\021)42 b Fl(\025n;)8 b(w)506 800 y Fg(B)r Fk(\()p Fg(n)p Fk(\))505 836 y(2)584 824 y Fl(;)602 812 y(~)605 824 y(k)q(;)g(w)685 800 y Fg(\026)p Fk(\()718 791 y Fg(~)720 800 y(k)p Fk(\))p Fg()h Fm(0)i(\(using)g(the)h(fact)e(that)h(this)h(do)q(esn't)f(c)o (hange)g(the)g(ideal\).)56 564 y({)23 b(There)17 b(is)g(an)g(in)o (teresting)g(phenomenon)h(whic)o(h)g(ma)o(y)e(o)q(ccur)h(if)g(w)o(e)g (extract)f(a)g(program)g(from)g(a)102 621 y(classical)e(pro)q(of)f (whic)o(h)h(uses)f(the)g(least)g(elemen)o(t)h(principle.)22 b(Consider)14 b(as)e(a)h(simple)i(example)f(the)102 677 y(w)o(ellfoundedness)j(of)e Fl(<)p Fm(,)611 761 y Fj(8)p Fl(g)660 743 y Fk(nat)n Fe(!)p Fk(nat)799 761 y Fj(9)p Fl(k)q Fm(\()p Fl(g)r Fm(\()p Fl(k)10 b Fm(+)g(1\))i Fl(<)h(g)r Fm(\()p Fl(k)q Fm(\))f Fj(!)h(?)p Fm(\))p Fl(:)102 846 y Fm(If)i(one)h(formalizes)g(the)f(classical)j(pro)q(of)d (\\c)o(ho)q(ose)g Fl(k)h Fm(suc)o(h)g(that)f Fl(g)r Fm(\()p Fl(k)q Fm(\))f(is)i(minimal")h(and)e(extracts)102 902 y(a)g(program)g(one)h(migh)o(t)f(exp)q(ect)i(that)e(it)h(computes)g(a)g Fl(k)h Fm(suc)o(h)f(that)f Fl(g)r Fm(\()p Fl(k)q Fm(\))g(is)h(minimal.) 23 b(But)16 b(this)102 958 y(is)e(imp)q(ossible!)22 b(In)15 b(fact)f(the)g(program)f(computes)h(the)h(least)f Fl(k)h Fm(suc)o(h)g(that)e Fl(g)r Fm(\()p Fl(k)8 b Fm(+)h(1\))j Fl(<)h(g)r Fm(\()p Fl(k)q Fm(\))e Fj(!)i(?)102 1015 y Fm(instead.)19 b(This)14 b(discrepancy)g(b)q(et)o(w)o(een)f(the)g (classical)i(pro)q(of)d(and)i(the)f(extracted)f(program)g(didn't)102 1071 y(sho)o(w)i(up)i(in)h(our)e(gcd)g(example)i(since)f(there)g(w)o (as)e(only)i(one)g Fl(c)d Fm(=)g Fl(\026)p Fm(\()p Fl(k)q Fm(\))g Fl(>)g Fm(0)i(suc)o(h)h(that)f Fl(c)g Fm(divides)102 1128 y Fl(a)126 1135 y Fk(1)164 1128 y Fm(and)k Fl(a)280 1135 y Fk(2)300 1128 y Fm(,)h(whereas)f(in)g(the)h(example)f(ab)q(o)o (v)o(e)g(there)g(ma)o(y)f(b)q(e)i(di\013eren)o(t)f Fl(c)g Fm(=)g Fl(g)r Fm(\()p Fl(k)q Fm(\))f(suc)o(h)h(that)102 1184 y Fl(g)r Fm(\()p Fl(k)10 b Fm(+)g(1\))i Fl(<)h(g)r Fm(\()p Fl(k)q Fm(\))f Fj(!)h(?)p Fm(.)-12 1282 y Fi(Implemen)o (tation.)59 1357 y Fm(The)18 b(gcd)h(example)h(has)e(b)q(een)i (implemen)o(ted)g(in)g(the)e(in)o(teractiv)o(e)h(pro)q(of)g(system)f (MINLOG.)h(W)l(e)-12 1414 y(sho)o(w)c(the)g(term)g(whic)o(h)h(w)o(as)e (extracted)h(automatically)g(from)g(a)g(deriv)m(ation)h(of)f(the)g (theorem.)-12 1493 y Fb(\(lambda)23 b(\(a1\))12 1549 y(\(lambda)g(\(a2\))36 1606 y(\(\(\(\(\(\(nat-rec-at)e('\(arrow)i(nat)h (\(arrow)f(nat)g(\(star)g(nat)h(nat\)\)\)\))155 1662 y(\(lambda)f(\(k1\))g(\(lambda)g(\(k2\))g(\(cons)h(n000)f(n000\)\)\)\)) 131 1719 y(\(lambda)g(\(n\))155 1775 y(\(lambda)g(\(w\))179 1831 y(\(lambda)g(\(k1\))203 1888 y(\(lambda)g(\(k2\))227 1944 y(\(\(\(\(if-at)f('\(star)h(nat)h(nat\)\))298 2001 y(\(\(<-strict-nat)e(0\))i(r2\)\))274 2057 y(\(\(w)g(l21\))f(l22\)\)) 274 2114 y(\(\(\(\(if-at)g('\(star)g(nat)g(nat\)\))322 2170 y(\(\(<-strict-nat)f(0\))i(r1\)\))322 2227 y(\(\(w)f(l11\))h (l12\)\))298 2283 y(\(cons)f(k1)h(k2\)\)\)\)\)\)\)\))107 2340 y(\(\(plus-nat)f(a2\))g(1\)\))83 2396 y(0\))60 2452 y(1\)\)\))881 2577 y Fm(11)p eop %%Page: 12 12 12 11 bop -12 307 a Fm(Here)23 b(w)o(e)g(ha)o(v)o(e)g(man)o(ually)h(in) o(tro)q(duced)g Fb(r1,)f(r2,)h(l11,)f(l12,)g(l21,)h(l22)e Fm(for)h(somewhat)f(length)o(y)-12 364 y(terms)12 b(corresp)q(onding)i (to)f(our)g(abbreviations)h Fl(r)836 371 y Fg(i)849 364 y Fm(,)875 352 y Fl(~)875 364 y(`)894 371 y Fg(i)908 364 y Fm(.)19 b(The)14 b(un)o(b)q(ound)g(v)m(ariable)g Fb(n000)f Fm(app)q(earing)h(in)g(the)-12 420 y(base)k(case)h(is)f(a)g (dumm)o(y)g(v)m(ariable)i(used)f(b)o(y)f(the)g(system)g(when)h(it)f(is) h(ask)o(ed)f(to)g(pro)q(duce)h(a)f(realizing)-12 477 y(term)f(for)f(the)h(instance)h Fj(?)e(!)g(9)p Fl(k)q(A)p Fm(\()p Fl(k)q Fm(\))h(of)g(ex{falso{quo)q(dlib)q(et.)27 b(In)18 b(our)e(case,)i(when)f(the)g(existen)o(tial)-12 533 y(quan)o(ti\014er)f(is)f(of)g(t)o(yp)q(e)g(nat)g(one)h(migh)o(t)f (as)f(w)o(ell)j(pic)o(k)e(the)h(constan)o(t)e(0)h(\(as)f(w)o(e)h(did)i (in)f(the)f(text\).)-12 639 y Fi(Ac)o(kno)o(wledgemen)o(ts.)i Fm(W)l(e)c(w)o(ould)g(lik)o(e)g(to)f(thank)h(Monik)m(a)g(Seisen)o(b)q (erger)h(and)f(F)l(elix)h(Joac)o(himski)f(for)-12 696 y(implemen)o(ting)k(the)d(re\014ned)i Fl(A)p Fm({translation)e(and)h (doing)h(the)e(gcd)h(example)h(in)f(the)g(MINLOG)g(system.)-12 839 y Fa(References)-12 940 y Fm([1])22 b(Ulric)o(h)c(Berger)g(and)f (Helm)o(ut)h(Sc)o(h)o(wic)o(h)o(ten)o(b)q(erg.)27 b(Program)16 b(dev)o(elopmen)o(t)i(b)o(y)f(pro)q(of)g(transforma-)59 997 y(tion.)38 b(In)22 b(H.)e(Sc)o(h)o(wic)o(h)o(ten)o(b)q(erg,)j (editor,)g Fh(Pr)n(o)n(of)f(and)f(Computation)p Fm(,)i(v)o(olume)f(139) e(of)h Fh(Series)g(F:)59 1053 y(Computer)g(and)g(Systems)f(Scienc)n(es) p Fm(,)f(pages)h(1{45.)e(NA)l(TO)j(Adv)m(anced)g(Study)g(Institute,)g (In)o(ter-)59 1110 y(national)g(Summer)g(Sc)o(ho)q(ol)h(held)g(in)g (Marktob)q(erdorf,)e(German)o(y)l(,)i(July)g(20)e({)h(August)f(1,)i (1993,)59 1166 y(Springer)16 b(V)l(erlag,)f(Berlin,)h(Heidelb)q(erg,)h (New)f(Y)l(ork,)e(1995.)-12 1260 y([2])22 b(Ulric)o(h)17 b(Berger)e(and)h(Helm)o(ut)g(Sc)o(h)o(wic)o(h)o(ten)o(b)q(erg.)22 b(Program)14 b(extraction)i(from)f(classical)i(pro)q(ofs.)k(In)59 1316 y(D.)c(Leiv)m(an)o(t,)j(editor,)f Fh(L)n(o)n(gic)f(and)h (Computational)h(Complexity,)g(International)e(Workshop)i(LCC)59 1373 y('94,)j(Indianap)n(olis,)f(IN,)f(USA,)g(Octob)n(er)h(1994)p Fm(,)h(v)o(olume)f(960)e(of)h Fh(L)n(e)n(ctur)n(e)g(Notes)h(in)f (Computer)59 1429 y(Scienc)n(e)p Fm(,)13 b(pages)i(77{97.)e(Springer)j (V)l(erlag,)f(Berlin,)i(Heidelb)q(erg,)g(New)e(Y)l(ork,)g(1995.)-12 1523 y([3])22 b(Harv)o(ey)14 b(F)l(riedman.)21 b(Classically)c(and)e (in)o(tuitionisticall)q(y)j(pro)o(v)m(ably)e(recursiv)o(e)g(functions.) 21 b(In)15 b(D.S.)59 1580 y(Scott)e(and)g(G.H.)g(M)q(\177)-24 b(uller,)14 b(editors,)g Fh(Higher)g(Set)h(The)n(ory)p Fm(,)e(v)o(olume)h(669)e(of)h Fh(L)n(e)n(ctur)n(e)h(Notes)g(in)g(Math-) 59 1636 y(ematics)p Fm(,)g(pages)h(21{28.)f(Springer)i(V)l(erlag,)f (Berlin,)h(Heidelb)q(erg,)h(New)f(Y)l(ork,)e(1978.)-12 1730 y([4])22 b(Georg)c(Kreisel.)32 b(In)o(terpretation)19 b(of)f(analysis)h(b)o(y)g(means)g(of)f(constructiv)o(e)h(functionals)h (of)f(\014nite)59 1786 y(t)o(yp)q(es.)41 b(In)23 b(A.)f(Heyting,)j (editor,)f Fh(Constructivity)e(in)h(Mathematics)p Fm(,)h(pages)e (101{128.)e(North{)59 1843 y(Holland,)c(Amsterdam,)e(1959.)881 2577 y(12)p eop %%Trailer end userdict /end-hook known{end-hook}if %%EOF