%!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