%!PS-Adobe-2.0 %%Creator: dvipsk 5.58f Copyright 1986, 1994 Radical Eye Software %%Title: finaljar2.dvi %%Pages: 10 0 %%PageOrder: Ascend %%BoundingBox: 0 0 596 842 %%EndComments %%BeginProcSet: pstops-clip 1 0 [/showpage/erasepage/copypage]{dup where{pop dup load type/operatortype eq{1 array cvx dup 0 3 index cvx put bind def}{pop}ifelse}{pop}ifelse}forall [/letter/legal/executivepage/a4/a4small/b5/com10envelope /monarchenvelope/c5envelope/dlenvelope/lettersmall/note /folio/quarto/a5]{dup where{dup wcheck{exch{}put} {pop{}def}ifelse}{pop}ifelse}forall /lcvx{dup load dup type dup/operatortype eq{pop exch pop} {/arraytype eq{dup xcheck{exch pop aload pop} {pop cvx}ifelse}{pop cvx}ifelse}ifelse}bind def /pstopsmatrix matrix currentmatrix def /pstopsxform matrix def /defaultmatrix{pstopsmatrix exch pstopsxform exch concatmatrix}bind def /initmatrix{matrix defaultmatrix setmatrix}bind def /pathtoproc{[{currentpoint}stopped{$error/newerror false put{newpath}}{/newpath cvx 3 1 roll/moveto cvx 4 array astore cvx}ifelse]{[/newpath cvx{/moveto cvx}{/lineto cvx} {/curveto cvx}{/closepath cvx}pathforall]cvx exch pop} stopped{$error/errorname get/invalidaccess eq{cleartomark $error/newerror false put cvx exec}{stop}ifelse}if}def /initclip[/matrix lcvx/currentmatrix lcvx/pstopsmatrix cvx/setmatrix lcvx /pathtoproc lcvx/initclip lcvx/newpath lcvx 0 0 /moveto lcvx 595.000000 0/rlineto lcvx 0 842.000000/rlineto lcvx -595.000000 0/rlineto lcvx /closepath lcvx/clip lcvx /newpath lcvx/exec lcvx/setmatrix lcvx]cvx def /initgraphics{initmatrix newpath initclip 1 setlinewidth 0 setlinecap 0 setlinejoin []0 setdash 0 setgray 10 setmiterlimit}bind def %%EndProcSet %DVIPSCommandLine: dvips finaljar2 %DVIPSParameters: dpi=300, compressed, comments removed %DVIPSSource: TeX output 2001.01.29:1437 %%BeginProcSet: texc.pro /TeXDict 250 dict def TeXDict begin /N{def}def /B{bind def}N /S{exch}N /X{S N}B /TR{translate}N /isls false N /vsize 11 72 mul N /hsize 8.5 72 mul N /landplus90{false}def /@rigin{isls{[0 landplus90{1 -1}{-1 1} ifelse 0 0 0]concat}if 72 Resolution div 72 VResolution div neg scale isls{landplus90{VResolution 72 div vsize mul 0 exch}{Resolution -72 div hsize mul 0}ifelse TR}if Resolution VResolution vsize -72 div 1 add mul TR[matrix currentmatrix{dup dup round sub abs 0.00001 lt{round}if} forall round exch round exch]setmatrix}N /@landscape{/isls true N}B /@manualfeed{statusdict /manualfeed true put}B /@copies{/#copies X}B /FMat[1 0 0 -1 0 0]N /FBB[0 0 0 0]N /nn 0 N /IE 0 N /ctr 0 N /df-tail{ /nn 8 dict N nn begin /FontType 3 N /FontMatrix fntrx N /FontBBox FBB N string /base X array /BitMaps X /BuildChar{CharBuilder}N /Encoding IE N end dup{/foo setfont}2 array copy cvx N load 0 nn put /ctr 0 N[}B /df{ /sf 1 N /fntrx FMat N df-tail}B /dfs{div /sf X /fntrx[sf 0 0 sf neg 0 0] N df-tail}B /E{pop nn dup definefont setfont}B /ch-width{ch-data dup length 5 sub get}B /ch-height{ch-data dup length 4 sub get}B /ch-xoff{ 128 ch-data dup length 3 sub get sub}B /ch-yoff{ch-data dup length 2 sub get 127 sub}B /ch-dx{ch-data dup length 1 sub get}B /ch-image{ch-data dup type /stringtype ne{ctr get /ctr ctr 1 add N}if}B /id 0 N /rw 0 N /rc 0 N /gp 0 N /cp 0 N /G 0 N /sf 0 N /CharBuilder{save 3 1 roll S dup /base get 2 index get S /BitMaps get S get /ch-data X pop /ctr 0 N ch-dx 0 ch-xoff ch-yoff ch-height sub ch-xoff ch-width add ch-yoff setcachedevice ch-width ch-height true[1 0 0 -1 -.1 ch-xoff sub ch-yoff .1 sub]/id ch-image N /rw ch-width 7 add 8 idiv string N /rc 0 N /gp 0 N /cp 0 N{rc 0 ne{rc 1 sub /rc X rw}{G}ifelse}imagemask restore}B /G{{id gp get /gp gp 1 add N dup 18 mod S 18 idiv pl S get exec}loop}B /adv{cp add /cp X}B /chg{rw cp id gp 4 index getinterval putinterval dup gp add /gp X adv}B /nd{/cp 0 N rw exit}B /lsh{rw cp 2 copy get dup 0 eq{pop 1}{ dup 255 eq{pop 254}{dup dup add 255 and S 1 and or}ifelse}ifelse put 1 adv}B /rsh{rw cp 2 copy get dup 0 eq{pop 128}{dup 255 eq{pop 127}{dup 2 idiv S 128 and or}ifelse}ifelse put 1 adv}B /clr{rw cp 2 index string putinterval adv}B /set{rw cp fillstr 0 4 index getinterval putinterval adv}B /fillstr 18 string 0 1 17{2 copy 255 put pop}for N /pl[{adv 1 chg} {adv 1 chg nd}{1 add chg}{1 add chg nd}{adv lsh}{adv lsh nd}{adv rsh}{ adv rsh nd}{1 add adv}{/rc X nd}{1 add set}{1 add clr}{adv 2 chg}{adv 2 chg nd}{pop nd}]dup{bind pop}forall N /D{/cc X dup type /stringtype ne{] }if nn /base get cc ctr put nn /BitMaps get S ctr S sf 1 ne{dup dup length 1 sub dup 2 index S get sf div put}if put /ctr ctr 1 add N}B /I{ cc 1 add D}B /bop{userdict /bop-hook known{bop-hook}if /SI save N @rigin 0 0 moveto /V matrix currentmatrix dup 1 get dup mul exch 0 get dup mul add .99 lt{/QV}{/RV}ifelse load def pop pop}N /eop{SI restore userdict /eop-hook known{eop-hook}if showpage}N /@start{userdict /start-hook known{start-hook}if pop /VResolution X /Resolution X 1000 div /DVImag X /IE 256 array N 0 1 255{IE S 1 string dup 0 3 index put cvn put}for 65781.76 div /vsize X 65781.76 div /hsize X}N /p{show}N /RMat[1 0 0 -1 0 0]N /BDot 260 string N /rulex 0 N /ruley 0 N /v{/ruley X /rulex X V}B /V {}B /RV statusdict begin /product where{pop product dup length 7 ge{0 7 getinterval dup(Display)eq exch 0 4 getinterval(NeXT)eq or}{pop false} ifelse}{false}ifelse end{{gsave TR -.1 .1 TR 1 1 scale rulex ruley false RMat{BDot}imagemask grestore}}{{gsave TR -.1 .1 TR rulex ruley scale 1 1 false RMat{BDot}imagemask grestore}}ifelse B /QV{gsave newpath transform round exch round exch itransform moveto rulex 0 rlineto 0 ruley neg rlineto rulex neg 0 rlineto fill grestore}B /a{moveto}B /delta 0 N /tail {dup /delta X 0 rmoveto}B /M{S p delta add tail}B /b{S p tail}B /c{-4 M} B /d{-3 M}B /e{-2 M}B /f{-1 M}B /g{0 M}B /h{1 M}B /i{2 M}B /j{3 M}B /k{ 4 M}B /w{0 rmoveto}B /l{p -4 w}B /m{p -3 w}B /n{p -2 w}B /o{p -1 w}B /q{ p 1 w}B /r{p 2 w}B /s{p 3 w}B /t{p 4 w}B /x{0 S rmoveto}B /y{3 2 roll p a}B /bos{/SS save N}B /eos{SS restore}B end %%EndProcSet %%BeginProcSet: special.pro TeXDict begin /SDict 200 dict N SDict begin /@SpecialDefaults{/hs 612 N /vs 792 N /ho 0 N /vo 0 N /hsc 1 N /vsc 1 N /ang 0 N /CLIP 0 N /rwiSeen false N /rhiSeen false N /letter{}N /note{}N /a4{}N /legal{}N}B /@scaleunit 100 N /@hscale{@scaleunit div /hsc X}B /@vscale{@scaleunit div /vsc X}B /@hsize{/hs X /CLIP 1 N}B /@vsize{/vs X /CLIP 1 N}B /@clip{ /CLIP 2 N}B /@hoffset{/ho X}B /@voffset{/vo X}B /@angle{/ang X}B /@rwi{ 10 div /rwi X /rwiSeen true N}B /@rhi{10 div /rhi X /rhiSeen true N}B /@llx{/llx X}B /@lly{/lly X}B /@urx{/urx X}B /@ury{/ury X}B /magscale true def end /@MacSetUp{userdict /md known{userdict /md get type /dicttype eq{userdict begin md length 10 add md maxlength ge{/md md dup length 20 add dict copy def}if end md begin /letter{}N /note{}N /legal{} N /od{txpose 1 0 mtx defaultmatrix dtransform S atan/pa X newpath clippath mark{transform{itransform moveto}}{transform{itransform lineto} }{6 -2 roll transform 6 -2 roll transform 6 -2 roll transform{ itransform 6 2 roll itransform 6 2 roll itransform 6 2 roll curveto}}{{ closepath}}pathforall newpath counttomark array astore /gc xdf pop ct 39 0 put 10 fz 0 fs 2 F/|______Courier fnt invertflag{PaintBlack}if}N /txpose{pxs pys scale ppr aload pop por{noflips{pop S neg S TR pop 1 -1 scale}if xflip yflip and{pop S neg S TR 180 rotate 1 -1 scale ppr 3 get ppr 1 get neg sub neg ppr 2 get ppr 0 get neg sub neg TR}if xflip yflip not and{pop S neg S TR pop 180 rotate ppr 3 get ppr 1 get neg sub neg 0 TR}if yflip xflip not and{ppr 1 get neg ppr 0 get neg TR}if}{noflips{TR pop pop 270 rotate 1 -1 scale}if xflip yflip and{TR pop pop 90 rotate 1 -1 scale ppr 3 get ppr 1 get neg sub neg ppr 2 get ppr 0 get neg sub neg TR}if xflip yflip not and{TR pop pop 90 rotate ppr 3 get ppr 1 get neg sub neg 0 TR}if yflip xflip not and{TR pop pop 270 rotate ppr 2 get ppr 0 get neg sub neg 0 S TR}if}ifelse scaleby96{ppr aload pop 4 -1 roll add 2 div 3 1 roll add 2 div 2 copy TR .96 dup scale neg S neg S TR}if}N /cp {pop pop showpage pm restore}N end}if}if}N /normalscale{Resolution 72 div VResolution 72 div neg scale magscale{DVImag dup scale}if 0 setgray} N /psfts{S 65781.76 div N}N /startTexFig{/psf$SavedState save N userdict maxlength dict begin /magscale true def normalscale currentpoint TR /psf$ury psfts /psf$urx psfts /psf$lly psfts /psf$llx psfts /psf$y psfts /psf$x psfts currentpoint /psf$cy X /psf$cx X /psf$sx psf$x psf$urx psf$llx sub div N /psf$sy psf$y psf$ury psf$lly sub div N psf$sx psf$sy scale psf$cx psf$sx div psf$llx sub psf$cy psf$sy div psf$ury sub TR /showpage{}N /erasepage{}N /copypage{}N /p 3 def @MacSetUp}N /doclip{ psf$llx psf$lly psf$urx psf$ury currentpoint 6 2 roll newpath 4 copy 4 2 roll moveto 6 -1 roll S lineto S lineto S lineto closepath clip newpath moveto}N /endTexFig{end psf$SavedState restore}N /@beginspecial{SDict begin /SpecialSave save N gsave normalscale currentpoint TR @SpecialDefaults count /ocount X /dcount countdictstack N}N /@setspecial {CLIP 1 eq{newpath 0 0 moveto hs 0 rlineto 0 vs rlineto hs neg 0 rlineto closepath clip}if ho vo TR hsc vsc scale ang rotate rwiSeen{rwi urx llx sub div rhiSeen{rhi ury lly sub div}{dup}ifelse scale llx neg lly neg TR }{rhiSeen{rhi ury lly sub div dup scale llx neg lly neg TR}if}ifelse CLIP 2 eq{newpath llx lly moveto urx lly lineto urx ury lineto llx ury lineto closepath clip}if /showpage{}N /erasepage{}N /copypage{}N newpath }N /@endspecial{count ocount sub{pop}repeat countdictstack dcount sub{ end}repeat grestore SpecialSave restore end}N /@defspecial{SDict begin} N /@fedspecial{end}B /li{lineto}B /rl{rlineto}B /rc{rcurveto}B /np{ /SaveX currentpoint /SaveY X N 1 setlinecap newpath}N /st{stroke SaveX SaveY moveto}N /fil{fill SaveX SaveY moveto}N /ellipse{/endangle X /startangle X /yrad X /xrad X /savematrix matrix currentmatrix N TR xrad yrad scale 0 0 1 startangle endangle arc savematrix setmatrix}N end %%EndProcSet TeXDict begin 39158280 55380996 1000 300 300 (finaljar2.dvi) @start /Fa 1 111 df110 D E /Fb 25 117 df<137013F0EA01E0EA03C0EA0780EA0F00121E121C5AA25AA45AA81270A47EA27E121E 7EEA0780EA03C0EA01F0120013700C24799F18>40 D<126012F012787E7E7EEA07801203 EA01C0A2EA00E0A41370A813E0A4EA01C0A2EA03801207EA0F00121E5A5A5A12600C247C 9F18>I<121C123E127E127F123F121F1207120E121E127C12F81260080C788518>44 D<387FFFC0B512E0A26C13C013047E8F18>I<387FFFC0B512E0A26C13C0C8FCA4387FFF C0B512E0A26C13C0130C7E9318>61 D82 D91 D93 D97 D99 DIII< 3801E1F03807FFF85A381E1E30381C0E00487EA5EA1C0EEA1E1EEA1FFC5BEA39E00038C7 FC7EEA1FFEEBFFC04813E0387801F038700070481338A4007813F0EA7E03381FFFC06C13 803801FC00151F7F9318>I<127E12FE127E120EA5133EEBFF80000F13C013C1EB80E013 00120EAB387FC7FC38FFE7FE387FC7FC171C809B18>II<1338137CA313381300A4EA0FFCA3EA00 1CB3A4EA6038EAF078EAFFF0EA7FE0EA3F800E277E9C18>I<127E12FE127E120EA5EB3F F0A3EB0780EB0F00131E5B5B5BEA0FF87F139C130EEA0E0F7FEB038014C0387FC7F812FF 127F151C7F9B18>II110 DII<38FF0FC0EB3FE0EB7FF0EA07F0EBE060EBC0005BA290 C7FCA9EAFFFC7F5B14147E9318>114 DI<487E1203A4387FFFC0B5FCA238038000A9144014E0A33801C1C013FF6C1380EB3E 0013197F9818>I E /Fc 6 87 df<1470EB01F0EB03C0EB0780EB0E005B5B5BA213F05B B3AC485AA3485A48C7FC1206120E12385A12C012707E120E120612076C7E6C7EA36C7EB3 AC7F1370A27F7F7FEB0780EB03C0EB01F0EB007014637B811F>26 D<141C143C14F8EB01E0EB03C0EB0780EB0F00130E131E5BA35BB3B3A25BA3485AA2485A 5B48C7FC120E5A127812E0A21278121C7E7E6C7E7F6C7EA26C7EA31378B3B3A27FA37F13 0E130FEB0780EB03C0EB01E0EB00F8143C141C167C7B8121>40 D<1318137813F0EA01E0 EA03C0EA0780EA0F005A121E123E123C127CA2127812F8B3A50D25707E25>56 D<12F8B3A51278127CA2123C123E121E121F7EEA0780EA03C0EA01E0EA00F0137813180D 25708025>58 D<137CB3A613F8A313F0120113E0120313C0EA07801300120E5A5A12F012 C012F012387E7E7E1380EA03C013E0120113F0120013F8A3137CB3A60E4D798025>60 D<1303801307A2497EA3EB1CE0A3EB3870A3497EA3497EA348487EA348487EA339070003 80A2000EEB01C0A348EB00E0A3481470A3481438A348141CA248140C1E2A7E7F23>86 D E /Fd 4 108 df26 D67 D<1204120C1200A5123012581298A2 1230A212601264A21268123006127E910B>105 D<123C120CA25AA31370EA3190EA3230 EA34001238127FEA61801390A2EAC1A0EAC0C00C117E9010>107 D E /Fe 2 50 df<121FEA3180EA60C0EA4040EAC060A8EA4040EA60C0EA3180EA1F000B 107F8F0F>48 D<1218127812981218AC12FF08107D8F0F>I E /Ff 12 118 df82 D97 D<12E0A8EAE7C0EAFFE0EAF870EAE038A2131CA51338A2EAF0F0EAFFE0EAE7800E177E96 12>I101 DI<12E0B3A503177E9608>108 D110 DI114 D<121FEA7FC012E01300A27E127FEA3F80EA0FC0EA01E0128012C0EAE1C0127FEA1F000B 0F7F8E0E>I<1238A4EAFFC0A2EA3800AA1340EA1FC013000A137F920D>II E /Fg 21 122 df<131FA2497E133BA2EB7BC013731371EB F1E013E113E000017FA213C000031378A2138000077FA21300380FFFFEA2487F381E000F A24814801407A24814C01403A248EB01E01B207F9F1E>65 D<12F0B3AE04207C9F0D>73 D82 DI97 D<12F0ACEAF1F0EAF7FCB47EEAFC1F38F80F80EAF007A2EB03C0A6EB0780A238F80F00EA FC3FEAFFFEEAF7FCEAF1F012207D9F17>I100 DI<137EEA01FE1203EA078013005AA7EAFF F0A3EA0F00B10F20809F0E>I<12F0ACEAF1F8EAF3FCEAF7FEEAFC1FEAF80FA212F0AE10 207D9F17>104 D<12F0A41200A812F0B3A204207D9F0B>I<12F0B3AE04207D9F0B>108 D<39F0FC07E039F3FE1FF039F7FF3FF839FE0FF07C39F807C03CA200F01380AE1E147D93 25>III 114 DI<121EA6EAFFF0A3EA1E00AD1310 EA0FF8A2EA07E00D1A7F9910>II< 387801E0387C03C0383E0780EA1E0F000F1300EA079EEA03FC5B12016C5A12017F487EEA 079EEA0F0F120E381E0780383C03C0387801E000F813F01414809315>120 D<38F003C0A238780780A2127C383C0F00A2121E131EA2EA0F1CA2EA073C133813B81203 13B0EA01F05B1200A2485AA212035B1207B4C7FC5A5A121D7F9315>I E /Fh 10 95 df0 D2 D<1202A3EAC218EAF278EA3AE0EA0F80A2EA3AE0EAF278EAC218EA0200A3 0D0E7E8E12>I<1406A380A2EC0180EC00C01560B612FCA2C8126015C0EC0180EC0300A2 1406A31E127E9023>33 D<0040131000C0133000601360A36C13C0A238180180EA1FFF6C 1300EA0C03A2EA0606A26C5AA2EA0198A3EA00F0A21360A21417809615>56 D58 D62 D<13201360B3B512F8A215167D951B>I92 D<134013E0A2EA01B0A2EA0318A2EA060CA2487EA2487EA23830 0180A2386000C0A2481360142013137E9218>94 D E /Fi 23 121 df<130FEB3080EBC0C0380100401460000213C05A1480130138083F00133E1301148012 10A438300300A21306EA280CEA4418EA43E00040C7FCA25AA4131D7F9614>12 D<13F0EA0318EA0608EA0C0CA21218A3EA3018A213301320EA68C0EA6780EA6000A25AA3 5A0E147E8D12>26 D<3803FF805A381C3000EA181812301260A3485AA2EA4060EA6040EA 2180001EC7FC110E7F8D14>II<001013204813305AA2388020201360A21460EB4040EBC0C03881C18038 E76700EA7E7EEA3C3C140E7F8D16>33 D<126012F0A2126004047D830A>58 D<126012F0A212701210A21220A21240A2040A7D830A>I<130813181330A31360A313C0 A3EA0180A3EA0300A21206A35AA35AA35AA35AA35AA20D217E9812>61 D<14C0A21301A21303130514E01308131813101320A213401380A23801FFF0EB00701202 5AA25A121838FE03FE17177F961A>65 D<3807FFF83800E00E14071403A2EA01C01407A2 140E3803803CEBFFF0A2EB803C3807001C140EA3000E131CA214381470381C01E0B51200 18177F961B>II<3807FF F83800E00E1407A3EA01C0A3140E3803801C1470EBFFC0EB800048C7FCA4120EA45AB47E 18177F9616>80 D<121F1206A45AA4EA18F0EA1B18EA1C081218EA38181230A3EA603013 3113611362EAC026133810177E9614>104 D<120313801300C7FCA6121C12241246A25A 120C5AA31231A21232A2121C09177F960C>I<1318133813101300A6EA01C0EA0220EA04 30A2EA08601200A313C0A4EA0180A4EA630012E312C612780D1D80960E>I<121F1206A4 5AA4EA181C1366138EEA190CEA3200123C123FEA3180EA60C013C4A3EAC0C813700F177E 9612>I<123E120CA41218A41230A41260A412C012C8A312D0127007177E960B>I<38383C 1E3844C6633847028138460301388E0703EA0C06A338180C061520140C154039301804C0 EC07001B0E7F8D1F>II112 D<1203A21206A4EAFFC0EA0C00A3 5AA45A1380A2EA31001232121C0A147F930D>116 DI120 D E /Fj 41 123 df12 D<130113021304130813101320136013C0EA0180A2EA03005A1206120E120C121C121812 38A212301270A21260A212E0A25AAD12401260A212207EA27E102E79A113>40 D<13107F7F130613021303A37F1480A71303A31400A35BA21306A2130E130CA2131C1318 133813301370136013E05B485A90C7FC5A12065A5A5A5A1280112E80A113>I45 D<127012F8A212F012E005057B840E>I<14021406A2140E14 1EA2143F142F144F14CF148FEB010FA21302A213041308A20110138014071320EB3FFFEB 40071380A2EA0100A2120212061204001E14C039FF807FF81D207E9F22>65 D<48B512C039001E00F015781538153C5BA4491378A215F0EC01E09038F007809038FFFE 009038F00F80EC03C03801E00115E0A3EA03C0A315C038078003EC0780EC0F00141E380F 007CB512E01E1F7D9E20>II<90B5128090381E00E015701538151C5B 150EA35BA449131EA44848133CA3157848481370A215E0EC01C0380780031580EC0E005C 380F0070B512C01F1F7D9E22>I<48B512FE39001E001C150C1504A25BA4903878040815 00A2140C495AEBFFF8EBF018A23801E010A3EC001048481320A21540A248481380140115 001407380F001FB512FE1F1F7D9E1F>I<48B512FC39001E003815181508A25BA4491310 EC0800A3495A1430EBFFF0EBF0303801E020A44848C7FCA4485AA4120FEAFFF81E1F7D9E 1E>I<9039FFF1FFE090391F003E00011E133CA3495BA4495BA449485A90B5FCEBF001A2 4848485AA44848485AA4484848C7FCA4000F5B39FFF1FFE0231F7D9E22>72 D<01FFEB3FE0011FEB0F001504EB1780A201275BEB23C0A3903841E010A214F013400180 5B1478A348486C5AA3141E00025CA2140FA24891C7FC80A2120C001C1302EAFF80231F7D 9E22>78 D<48B5128039001E00E015701538153C5BA4491378A215F015E09038F003C0EC 0F00EBFFFC01F0C7FC485AA4485AA4485AA4120FEAFFF01E1F7D9E1F>80 D<90B5FC90381E03C0EC00E0157015785BA44913F0A2EC01E015C09038F00700141EEBFF F0EBF01C48487E140F8015803903C00F00A43807801E1508A21510000F130ED8FFF01320 C7EA03C01D207D9E21>82 D<903807E04090381C18C09038300580EB600313C000011301 018013001203A391C7FC7FA213F86CB47E14E06C6C7E131FEB01F8EB0078A21438A21220 A2143000601370146014E000705B38E80380D8C606C7FCEA81F81A217D9F1A>I<000FB5 12FC391E03C03800181418001014081220EB078012601240A239800F001000001400A313 1EA45BA45BA45BA41201387FFF801E1F799E21>I97 DI<137EEA01C1380300 80EA0E07121E001C1300EA3C0248C7FCA35AA5EA70011302EA3004EA1838EA07C011147C 9315>I<1478EB03F8EB0070A414E0A4EB01C0A213F1EA038938070780EA0E03121C123C 383807001278A3EAF00EA31420EB1C40A2EA703C135C38308C80380F070015207C9F17> I<137CEA01C2EA0701120E121C123CEA3802EA780CEA7BF0EA7C0012F0A4127013011302 EA3804EA1838EA07C010147C9315>I<1478EB019CEB033CA2EB07181400A2130EA5EBFF E0EB1C00A45BA55BA55BA5485AA35B1231007BC7FC12F31266123C1629829F0E>III<13C0EA01E0A2 13C0C7FCA7120E12131223EA4380EA4700A21287120EA35AA3EA38401380A21270EA3100 1232121C0B1F7C9E0E>I107 DI<391C0F80F0392630C318394740640C903880 680EEB0070A2008E495A120EA34848485AA3ED70803A3803807100A215E1156239700700 64D83003133821147C9325>I<381C0F80382630C0384740601380EB0070A2008E13E012 0EA3381C01C0A3EB038400381388A2EB0708EB031000701330383001C016147C931A>I< 137CEA01C338030180000E13C0121E001C13E0123C1278A338F003C0A3EB07801400EA70 0F130EEA3018EA1870EA07C013147C9317>I<3801C1E0380262183804741C1378EB701E A2EA08E01200A33801C03CA3143838038078147014E0EBC1C038072380EB1E0090C7FCA2 120EA45AA2B47E171D809317>I II<13FCEA0302EA0601EA0C03130713061300EA0F8013F0EA07F8EA03FCEA003E13 0E1270EAF00CA2EAE008EA4010EA2060EA1F8010147D9313>I I<000E13C0001313E0382301C0EA4381EA4701A238870380120EA3381C0700A31410EB0E 201218A2381C1E40EA0C263807C38014147C9318>I<380E0380EA1307002313C0EA4383 EA4701130000871380120EA3381C0100A31302A25BA25BEA0E30EA03C012147C9315>I< 38038380380CC440381068E013711220EB70C03840E0001200A3485AA314403863808012 F3EB810012E5EA84C6EA787813147D9315>120 D<000E13C0001313E0382301C0EA4381 EA4701A238870380120EA3381C0700A4130E1218A2EA1C1EEA0C3CEA07DCEA001CA25B12 F05BEAE060485AEA4380003EC7FC131D7C9316>I<3801C0403803E080EA07F1380C1F00 EA0802C65A5B5B5B5B5B48C7FC1202485AEA08021210EA3E0CEA63FCEA41F8EA80E01214 7D9313>I E /Fk 1 79 df<39FFC007FCA239386001E039183000C0EA1C18121EEA1B0C 7FEA1983EA18C3EB6180EB60C0EB30601318EB0C3014181306EB030CEB01861483EB00C3 14611430A21418140C1406A2003C130338FF80011400C812401E207D9E22>78 D E /Fl 28 107 df0 D<127012F8A3127005057C8D0D>I<0040 130400C0130C006013186C13306C13606C13C03806018038030300EA0186EA00CC137813 30A2137813CCEA0186EA030338060180380C00C048136048133048131848130C00401304 16187A9623>II17 D<15C01403EC0F00141C1470495AEB0780011EC7FC1378EA01E0EA038000 0EC8FC123C12F0A2123C120EEA0380EA01E0EA0078131EEB0780EB01E0EB0070141C140F EC03C014001500A8007FB51280B612C01A267C9C23>20 D<12C012F0123C120EEA0380EA 01E0EA0078131EEB0780EB01E0EB0070141C140FEC03C0A2EC0F00141C1470495AEB0780 011EC7FC1378EA01E0EA0380000EC8FC123C127012C0C9FCA8007FB51280B612C01A267C 9C23>I24 D<1506A381A216801501ED00C0166016701618 B8FCA2C912181670166016C0ED018015031600A21506A328187E962D>33 D<01C0130CA348487FA20003140790C77E0006EC018048EC00C0001C15E000301530B712 FEA20030C81230001C15E0000C15C06CEC01806CEC03006D5B00011406A26C6C5BA32718 7D962D>36 D50 D<140CA21418A21430A214 60A214C0A2EB0180A3EB0300A21306A25BA25BA25BA25BA25BA2485AA248C7FCA21206A3 5AA25AA25AA25AA25A1240162C7AA000>54 D<12C0A712E0A212C0A703107E9200>I<00 40130100C0130300601306A36C130CA36C1318A3380FFFF0A2380C00306C1360A36C13C0 A238018180A33800C300A31366A3133CA31318A21821809F19>III62 D<13021306B3A9B612F8A21D1E7D9D23>I<15 10153015F0A31401A21402A21404140C1408141814101420A24A7E14C0EC80781301EB03 001302130690380DFFF8130F90381800785B49137CEA40E0D8C0C0133CEAE380B4C7123E 48EC3F80ED1F00007891C7FC21237FA024>65 D<013F14C03A01FF800180D8070F1303D8 0C0713070018150012300070495A00C0140EC65A151E151C130E153C011E1338A2011C13 7848B55A5A38003800A201785B1370140113F013E05D1201EBC00316400003ECC1C00180 EBE300010013FE0006EB01F822217F9E26>72 D<90383FFFE048B512F839071E01FE0008 EB007F0018141F007080A212C0D8001C130EA2013C131E151C151801385B5D0178138002 07C7FCEB70FCEB71F8EBF0FCEBE07C801201497EA200036D13100180EB806016E0000790 3807C1800100EBE3000006EB03FE48EB01F024207F9E27>82 D<1308131CA21336A31363 A2EBC180A2380180C0A238030060A300067FA2487FA2487FA2487FA3487FA248EB018014 00191C7E9A1E>94 D<124012C0AEB512FEA200C0C7FCAE124017207E9F1C>96 D<130F1338136013E0EA01C0AFEA0380EA0700121E12F8121E1207EA0380EA01C0AFEA00 E013601338130F102D7DA117>102 D<12F8121E1207EA0380EA01C0AFEA00E013601338 130F1338136013E0EA01C0AFEA0380EA0700121E12F8102D7DA117>I<1320136013C0A3 EA0180A2EA0300A31206A25AA25AA35AA25AA35AA21260A37EA27EA37EA27EA27EA3EA01 80A2EA00C0A3136013200B2E7CA112>I<12C0A21260A37EA27EA37EA27EA27EA3EA0180 A2EA00C0A31360A213C0A3EA0180A2EA0300A31206A25AA25AA35AA25AA35AA20B2E7EA1 12>I<12C0B3B3A9022D7BA10D>I E /Fm 25 121 df<127012F8A312700505798414>46 D<1306130EA2131CA21338A21370A213E0A2EA01C0A2EA0380A3EA0700A2120EA25AA25A A25AA25AA25A0F1D7E9914>II<1203A25A5A123F12F7124712 07AEEA7FF0A20C177C9614>III<137813F8EA01B8A2EA0338A2120612 0E120C121C12381230127012E0B51280A238003800A548B4FCA211177F9614>III<12E0EAFFFEA2EAE01C1338EA0030137013E013C0120113801203A2EA0700A4120EA6 12040F187E9714>III<127012F8A312701200A6127012 F8A312700510798F14>I<127012F8A312701200A6126012F012F8A21278121812301270 12E012800515798F14>I97 D101 D<13FCEA01FEEA038EEA07041300A3EA7FFE12FFEA0700ACEAFFF8A20F177F9614>I<12 06120FA21206C7FCA4B4FCA21207ACEAFFF8A20D187C9714>105 D<136013F0A213601300A4EA1FF0A2EA0070B2EA40E0EAE0C0EA7F80EA3F000C207E9714 >I108 D110 D112 D114 D<1206120EA4EA7FFC12FFEA0E00A8130EA3131CEA07F8EA01F00F157F9414>116 D120 D E /Fn 1 14 df13 D E /Fo 27 116 df<120112021204120C1218A21230A212701260A312E0AA1260A3127012 30A21218A2120C12041202120108227D980E>40 D<12801240122012301218A2120CA212 0E1206A31207AA1206A3120E120CA21218A2123012201240128008227E980E>I<1330AB B512FCA238003000AB16187E931B>43 D48 D<1206120E12FE120EB1EAFF E00B157D9412>III<1330A2137013F0120113701202120412081218121012 20124012C0EAFFFEEA0070A5EA03FE0F157F9412>III<1240EA7FFE13FC13F8EAC008 EA80101320EA00401380A2EA01005AA212021206A2120EA512040F167E9512>I61 D68 D<3AFF07FC3F803A3C00 E00E00001C1404A2EB0170000E5CA2EB023800075CA2EB041CD803845BA2EB880ED801C8 5BA2EBD007D800F05BA3EBE003016090C7FCA221177F9624>87 D<12FCA212C0B3AB12FC A206217D980A>91 D<12FCA2120CB3AB12FCA2062180980A>93 D97 D99 D<133E130EA8EA07CEEA1C3EEA300E1270126012E0A412601270EA301EEA182E3807 CF8011177F9614>I<12F81238A813F8EA3B1CEA3C0E1238AA38FE3F8011177F9614>104 D<12301278A212301200A512F81238AC12FE07177F960A>I<12F81238A8133E13381330 134013801239EA3FC0EA39E0123813F01378133CA2EAFE7F10177F9613>107 D<12F81238B3A312FE07177F960A>I110 DI114 DI E /Fp 45 127 df<137CEA0180EA0700120E5A123C12381278A2EA7F F0EAF000A31270A312301238EA0C18EA07E00E147E9312>15 D<1207EA01C07F12007F13 70A213781338A2133C131CA2131E130EA2130F7F131FEB3780136313C3380183C0EA0381 EA0701000E13E0EA1C005A48137012F048137848133815207D9F1B>21 D<1308A3EB0FE0EB3810EBF7E03801E000485A485AA248C7FCA57E6CB4FC3801C0803802 7F00000CC7FC5A121012305AA312E0A212701278123EEA1FC0EA0FF0EA03FCEA007F131F 1303A21201EA00C6133C1429809F14>24 D<380FFFFC4813FE4813FC3860820012C01281 EA010613041203A21202EA060C130E120CA2121CA2EA180FEA3807EA300617147E931A> III<380FFFF05A5A3860400012C0EA80C012005B1201A4120390C7 FCA25AA3120E120614147E9314>I<1440A21480A4EB0100A41302A2EB1FC0EBE2703803 84183806040C000C130E001C13063838080712301270A238E0100EA2140C141C38602038 0070133000301360381821C0380E4700EA03F8EA0040A25BA448C7FCA318297E9F1B>30 D<1410A35CA45CA45C000FEB818039118083C0002114E0EBC10100411300D84381136000 831440EA0702A3000E14805BEC0100A21402495A00065B000713303801C8C0D8007FC7FC 1310A35BA45BA21B297E9F1E>32 D<137F3801FF80380701E0380C00404813001210A4EA 0FF813B0EA104048C7FC5AA25AA2EA40011302EA300CEA1FF8EA07E01316809415>34 D<127012F8A3127005057C840D>58 D<127012F012F8A212781208A31210A31220A21240 050E7C840D>I<15C01403EC0F00141C1470495AEB0780011EC7FC1378EA01E0EA038000 0EC8FC123C12F0A2123C120EEA0380EA01E0EA0078131EEB0780EB01E0EB0070141C140F EC03C014001A1C7C9823>I<144014C0EB0180A3EB0300A31306A25BA35BA35BA25BA35B A3485AA348C7FCA21206A35AA35AA25AA35AA35AA2122D7EA117>I<12C012F0123C120E EA0380EA01E0EA0078131EEB0780EB01E0EB0070141C140FEC03C0A2EC0F00141C147049 5AEB0780011EC7FC1378EA01E0EA0380000EC8FC123C12F012C01A1C7C9823>I<140214 06140EA2141E141F142F146F144F148FA2EB010F1303130201041380A2EB080713181310 1320A2EB7FFFEB8007A2D8010013C0140312025AA2120C003C1307B4EB3FFC1E207E9F22 >65 D<48B512E039001E0078153C151C151E5BA449133CA2157815F09038F003C090B512 009038F007C0EC00E0484813F01578A3485AA31570484813F0EC01E0EC03C0EC0780390F 001E00B512F01F1F7E9E22>I<027F1380903803C0C190390E0023000138131749130F5B 48481306485A48C7FC5A000E1404121E4891C7FCA25AA45AA400701420A35D6C5CA26C49 C7FC6C13066C13183801C06038007F8021217F9F21>I<48B512E039001E0038150E81A2 49EB0380A2ED01C0A25BA4491303A44848EB0780A216005D4848130E151E151C5D48485B 5D4A5A0207C7FC380F001CB512F0221F7E9E26>I<3801FFF8D8001FC7FC131EA35BA45B A45BA4485AA3154048481380A21401150048485AA21406140E380F007CB512FC1A1F7E9E 1F>76 DI< 14FF90380781C090381C00E0491370491338D801C0131C120349131E48C7120E5A121EA2 5AA248141EA448143CA2153815781570007014F0EC01E0007814C0EC03800038EB07006C 130E5C000F1370380381C0C6B4C7FC1F217F9F23>79 D<48B512E039001E0078151C150E 150F5BA449131EA2153C15784913E0EC03C09038FFFE0001F0C7FC485AA4485AA4485AA4 120FEAFFF8201F7E9E1D>I<48B5128039001E00F01538151CA249131EA449133CA21578 15F09038F001C0EC0700EBFFF8EBF00E48487E1580140315C03903C00780A43907800F00 1502A21504000F130739FFF80308C7EA01F01F207E9E23>82 D<137CEA01C338070080EA 0E07121E001C1300EA3C0248C7FCA35AA5EA70011302EA3004EA1838EA0FC011147E9314 >99 D<1478EB03F8EB0070A414E0A4EB01C0A213F1EA038938070780EA0E03121C123C38 3807001278A3EAF00EA31410EB1C20A2EA703CEB5C40EA308C380F078015207E9F18>I< 137CEA0182EA0701120E121C123CEA3802EA780CEA7BF0EA7C0012F0A4127013011302EA 3004EA1838EA0FC010147E9315>I<147C14CEEB019E1303140CEB0700A4130EA3EBFFF0 EB0E00A25BA55BA55BA55BA45B1201EA3180127948C7FC1262123C17297E9F16>III<13E01201 A2EA00C01300A7120E1213EA23801243A3EA87001207A2120EA25AA21320EA3840A31380 EA1900120E0B1F7E9E10>I<14C0EB01E0A214C090C7FCA7131E1323EB43801383EA0103 A2380207001200A3130EA45BA45BA45BA21230EA78E0EAF1C0EA6380003EC7FC1328819E 13>III<391E07C07C39231861869038A032033843C034D980381380A23A87 007007001207A3000EEBE00EA3ED1C10261C01C01320153816401518263803801380D818 01EB0F0024147E9328>I<381E0780382318C0EBA0603843C0701380A2388700E01207A3 380E01C0A3EB0382001C1384EB07041408130300381310381801E017147E931B>I<3803 C1E038046218EB741CEA0878EB701EA2EA10E01200A33801C03CA3143838038078147014 E0EBC1C038072380EB1E0090C7FCA2120EA45AA2EAFFC0171D819317>112 D114 D<13FCEA030338060080EA0C0113031400000EC7FCEA0F8013F86C7EEA01FEEA 001F13071270EAF006A2EAE004EA4008EA2030EA1FC011147E9315>II<000F136038118070002113E013C01241EA4380388381C0EA0701A3380E0380 A31484EB0708120CA2380E0F10EA06133803E1E016147E931A>I<3803C1C0380C622038 103470EB38F012201460384070001200A35BA314203861C04012F1148012E238446300EA 383C14147E931A>120 D<001E13600023137014E0EA438013001247388701C0120EA338 1C0380A4EB07001218121C5BEA0C3EEA03CEEA000EA25BEAF0181338485AEAC060EA41C0 003FC7FC141D7E9316>I<3801C0203803F0403807F8C0380C1F8038080100EA00025B5B 5B13605B48C7FC120248138038080100485AEA3F06EA63FEEA40FCEA807013147E9315> I126 D E /Fq 29 122 df12 D<1218123C127CA2123C1204A21208A21210A2122012401280060E7D840D>44 DI<1230127812F81278127005057C840D>I<0007B512F83900F8 00780178133815185B1508A53901E00800A314181438EBFFF83803C0301410A491C7FC48 5AA648C8FC7FEAFFFC1D1F7E9E1E>70 D<3807FFE0D800FCC7FC1378A25BA6485AA6485A A41580EC0100EA0780A25C14021406140E380F001E147CB512FC191F7E9E1C>76 D<003FB512F0383C078000301430126039400F0010A212C01280A3D8001E1300A65BA65B A65B7F383FFFE01C1F7A9E21>84 D97 D<1207123F120F7EA2120EA65A137CEA1D83381E0180001C13C0EB00E05A14F0A5387001 E0A214C013031480EB0700EAE80EEACC38EA83E014207B9F19>I<13FEEA0383380E0780 121C0038130090C7FC12785AA45AA37E5BEA70026C5AEA1C18EA07E011147D9314>I<14 38EB01F8EB00781438A21470A614E013FCEA0382EA0601121CEA3C00383801C0127812F0 A438E00380A412F0EA700738380F00381C37803807C7E015207D9F19>I<13F8EA070EEA 0E07121C383803801278127012F0A2B5FC00F0C7FC5AA46C5AEA7002EA3004EA1C18EA07 E011147D9314>II<140EEB3E11EBE1A33801C1C2380381 E0EA07801301120FA3380703C01480EB8700EA04FC48C7FCA21218121CEA0FFF14C014E0 381800F04813305A5AA3006013606C13C0381C0700EA07FC181F809417>I<13E0120712 011200A2485AA6485AEB8F80EB90E013A0EBC0601380000713E01300A5380E01C0A6381C 0380001E13C038FF8FF014207E9F19>II<13E0120712011200A2EA 01C0A6EA0380A6EA0700A6120EA65A121EEAFF800B207F9F0C>108 D<390387C07C391F9861863907A072073903C03403EB80380007EB7807EB0070A5000EEB E00EA64848485A001EEBE01E3AFFCFFCFFC022147E9326>I<38038F80381F90E0EA07A0 3803C0601380000713E01300A5380E01C0A6381C0380001E13C038FF8FF014147E9319> I<13FCEA0387380E0180381C00C04813E0A24813F012F0A438E001E0A214C0130300F013 8038700700EA380E6C5AEA07E014147D9317>IIIII<1380EA0100A3 5A5A5A121EEAFFF8EA0E00A45AA65A1310A41320A2EA1840EA0F800D1C7C9B12>I<381C 0380EAFC1FEA3C07EA1C03A238380700A6EA700EA4131EA25BEA305E381F9F8011147B93 19>I<38FF83F8381E00E0001C13C01480121E380E01005B13025B12075BA25BEA039013 A013E05B5B120190C7FC15147C9318>I<39FF9FE1FC393C078070391C03006014801540 1580EA0E0790380D81001309EB19C21311380F21C4EA0720EB40C814E8EB80F0A26C485A 1460000213401E147C9321>I<390FF83F803901E00E00EBC00C140813E000005B143014 205C13705CA20171C7FC1339133A133E133C133813181310A25BA25BEA70C0EAF08000F1 C8FC12E61278191D809318>121 D E /Fr 39 128 df<127012F812FCA212741204A312 08A21210A212201240060E7B9F0F>39 D<127012F8A3127005057B840F>46 D49 DI<80497EA3497EA3EB04F0A2497E1478A2497EA2EB303EEB201EA2497EA390B57E EB8007000180EB0003A200026D7EA3486D7E120E001F497E3AFFC00FFF8021207E9F25> 65 D68 DI<903807F0089038 3C0C189038E003383901C000B8D80780137848C71238120E001E14185A1508127C127815 0012F8A6EC1FFF0078EB00F81578127C123CA27E120E120F6C7ED801C013B83900E00118 90383C0E08903807F00020217C9F27>71 D76 DI80 D<3803F020380C0C60381803E0EA30005A146012E01420A36C13007E127CEA7F80EA3FFC 6CB4FC00071380000113C038000FE013031301EB00F014707EA46C136014E06C13C038F8 018038C60300EA81FC14217C9F1C>83 D<007FB512F839780780780060141800401408A2 00C0140C00801404A400001400B3497E0003B5FC1E1F7D9E24>I<3BFFF03FFC07FC3B1F 0007E001F06C903903C00060174081D807801580A2EC04F0D803C0EC0100A2EC0878D801 E01402A2EC103CD800F05CA2EC201E01785CA2EC400F013C5CA29138800790011E14A0A2 90391F0003E0A26D5C010E1301A201065CA22E207E9E32>87 D<12FFA212C0B3B3A512FF A2082D7BA10F>91 D<12FFA21203B3B3A512FFA2082D7EA10F>93 D<1318A2133CA3134EA213CF1387A238010380A2000313C0EA0201A23807FFE0EA0400A2 481370A2001813380038137838FE01FF18177F961C>97 DIIIIII<38FF87FC381C00E0AAEA 1FFFEA1C00AA38FF87FC16177E961C>II<38FF 80FE381C0078146014401480EB0100130613085B13381378139CEA1D0E121EEA1C07EB03 80EB01C0A2EB00E014701478147C38FF80FF18177E961D>107 DI<00FCEB07F0001C1480A20016130BA200 131313A338118023A23810C043A3EB6083A2EB3103A3131AA2130C123800FEEB1FF01C17 7E9622>I<38FC01FC381E007014201217EA1380A2EA11C0EA10E0A213701338A2131C13 0E1307A2EB03A0EB01E0A213001460123800FE132016177E961C>I<13FE38038380380E 00E0481370003C1378003813380078133C0070131C00F0131EA70070131C0078133C0038 1338003C1378001C13706C13E0380383803800FE0017177E961D>II114 DI<387FFFFC3870381C00401304A200C0130600801302A300001300AE3803FF80 17177F961B>I<38FF81FC381C00701420B0000C1340120E6C138038018300EA007C1617 7E961C>I<38FF80FE381F0070000E13606C1340EB80803803C100EA01C3EA00E213F413 7813387F133E134E13C7EB8780380103C0EA0201380600E0000413F0000C1370003C1378 00FE13FF18177F961C>120 DII127 D E /Fs 39 122 df12 D<1238127C12FE12FFA2127F123B1203A21206A2120E120C12181230122008107C9F0F> 39 D<1238127C12FEA3127C123807077C860F>46 D<137013F0120712FF12F91201B3A4 387FFFC0A2121D7D9C1A>49 DIII<001C13E0EA1FFF14C01480140013FC 13C00018C7FCA4EA19FE381FFF80381E07C0381803E0381001F0120014F8A2127812FCA3 14F0EA7803007013E0383C0FC0380FFF00EA03FC151D7E9C1A>I<133F3801FFC03807C0 E0EA0F81381F03F0121E123E127CEB01E090C7FCEAFC1013FF00FD13C0EB03E038FE01F0 A200FC13F8A4127CA3003C13F0123E381E03E0380F07C03807FF803801FE00151D7E9C1A >I<1260387FFFF8A214F014E014C038E0018038C00300A21306C65A5B13381330137013 F0A2485AA21203A41207A56C5A6C5A151E7D9D1A>I<14E0A2497EA3497EA2EB06FCA2EB 0EFEEB0C7EA2497EA201307F141F01707FEB600FA2496C7E90B5FC4880EB8003000380EB 0001A200066D7EA2000E803AFFE00FFFE0A2231F7E9E28>65 D<903807FC0290383FFF0E 9038FE03DE3903F000FE4848133E4848131E485A48C7120EA2481406127EA200FE1400A7 127E1506127F7E150C6C7E6C6C13186C6C13386C6C13703900FE01C090383FFF80903807 FC001F1F7D9E26>67 DI70 D73 D76 D82 D<007FB512FCA2397C07E07C0070141C0060140CA200E0140E00C01406A400001400B100 03B512C0A21F1E7E9D24>84 D<3CFFFC0FFFC0FFE0A23C0FC000FC000E007F00076E130C A26D151C0003D901BF1318A2D801F85D9138031F80A22600FC076D5AEC060F01FE15E090 3A7E0C07E0C0A2013FECE18091381803F1A2D91FB801FBC7FCECB00102F013FF6D486C5A A201075C4A137CA2010314784A133801011430331F7F9E36>87 D97 D99 DIII<3803FC3C380FFFFE381E079E383C03DE007C13E0A5003C13C0 381E0780381FFF00EA13FC0030C7FCA21238383FFF806C13F06C13F84813FC3878007C00 70133E00F0131EA30078133CA2383F01F8380FFFE000011300171E7F931A>II<121C123E12 7FA3123E121CC7FCA6B4FCA2121FB0EAFFE0A20B217EA00E>I107 DI<3AFE 0FE03F8090391FF07FC03A1E70F9C3E09039407D01F0EB807E121FEB007CAC3AFFE3FF8F FEA227147D932C>I<38FE0FC0EB3FE0381E61F0EBC0F81380EA1F00AD38FFE7FFA21814 7D931D>I<48B4FC000713C0381F83F0383E00F8A248137CA200FC137EA6007C137CA26C 13F8A2381F83F03807FFC00001130017147F931A>I<38FF1FC0EB7FF0381FE1F8EB80FC EB007EA2143E143FA6143E147E147CEB80FCEBC1F8EB7FE0EB1F8090C7FCA7EAFFE0A218 1D7E931D>I114 DI<1203A45AA25A A2123FEAFFFCA2EA1F00AA1306A5EA0F8CEA07F8EA03F00F1D7F9C14>I<38FF07F8A2EA 1F00AD1301A2EA0F063807FCFF6C5A18147D931D>I<3AFFC7FE1FE0A23A1F00F0030014 F8D80F801306A29038C1BC0E0007140CEBC3BE3903E31E18A29038F60F380001143001FE 13B03900FC07E0A2EBF80301785BA2903830018023147F9326>119 D<39FFE07F80A2391F001C00380F8018A26C6C5AA26C6C5AA2EBF0E000015B13F900005B 13FF6DC7FCA2133EA2131CA21318A2EA783012FC5BEAC0E0EAE1C0EA7F80001EC8FC191D 7F931C>121 D E /Ft 6 112 df77 D<3801F840380706C0EA0C01EA3800123000701340126000E01300A3EB1FF0EB01C01260 127012301238120CEA07023801FC4014137E9218>103 D105 D108 D<38FC07F0381E01C0381F00801217EA1380EA11C0A2EA10E0137013781338131C130EA2 1307130313011238EAFE0014137F9217>110 DI E /Fu 73 128 df<13FEEA038138060180EA0E03381C010090C7FCA5B51280EA1C03AE38 FF8FF0141A809915>12 D<90387E1F803901C17040390703C0600006EB80E0000E144015 00A5B612E0380E0380AE397F8FE3FC1E1A809920>14 D25 D<126012F012F812681208A31210A212201240050B7D990B>39 D<1380EA010012025A12 0C120812185AA35AA412E0AA1260A47EA37E1208120C12047E7EEA008009267D9B0F>I< 7E12407E7E12181208120C7EA37EA41380AA1300A41206A35A1208121812105A5A5A0926 7E9B0F>I<126012F0A212701210A31220A21240A2040B7D830B>44 DI<126012F0A2126004047D830B>I48 D<12035AB4FC1207B3A2EA7FF80D187D9713>III<1318A21338137813F813B8EA01381202A2120412081218121012201240 12C0B5FCEA0038A6EA03FF10187F9713>III<1240EA7F FF13FEA2EA4004EA80081310A2EA00201340A21380120113005AA25A1206A2120EA51204 10197E9813>III<126012F0 A212601200A8126012F0A2126004107D8F0B>I<130CA3131EA2132F1327A2EB4380A3EB 81C0A200017F1300A248B47E38020070A2487FA3487FA2003C131EB4EBFFC01A1A7F991D >65 DIII III<39FFE1FFC0390E001C00AB380FFFFC380E001CAC39FFE1FFC01A1A7F99 1D>III<39FFE01FC0390E000F00140C14085C5C5C495A0102C7FC5B 130C131C132E1347EB8380EA0F03380E01C06D7EA2147080A280141E141F39FFE07FC01A 1A7F991E>III<00FEEB7FC0000FEB0E001404 EA0B80EA09C0A2EA08E01370A21338131CA2130E1307EB0384A2EB01C4EB00E4A2147414 3CA2141C140C121C38FF80041A1A7F991D>I<137F3801C1C038070070000E7F487F003C 131E0038130E0078130F00707F00F01480A80078EB0F00A20038130E003C131E001C131C 6C5B6C5B3801C1C0D8007FC7FC191A7E991E>II82 DI<007FB5FC38701C0700401301A200C0148000801300A300001400B1 3803FFE0191A7F991C>I<39FFE07FC0390E000E001404B200065B12076C5B6C6C5A3800 E0C0013FC7FC1A1A7F991D>I<39FF801FC0391C00070014066C1304A36C5BA26C6C5AA3 6C6C5AA26C6C5AA3EB7080A213790139C7FCA2131EA3130CA21A1A7F991D>I<3AFF81FF 07F03A3C007801C0001CEC0080A36C90389C0100A33907010E02A33903830F04EB8207A2 150C3901C40388A33900E801D0A390387000E0A301305B01201340241A7F9927>I<39FF 801FE0391E00070014066C13046C130CEB800800035BEA01C06D5A00001360EB7040EB78 801338011DC7FC131F130EAAEBFFC01B1A7F991D>89 DI<1220A21240A21280A312E012F0A21260040B7D990B>96 DI<12FC121CA913FCEA1D07381E0380381C01C0130014E0A6EB01C014 80381E0300EA1906EA10F8131A809915>II<133F1307A9EA03E7EA0C17EA180F487E127012 E0A6126012706C5AEA1C373807C7E0131A7F9915>IIII<12FC121CA9137CEA1D87381E0380A2121CAB38FF9FF0 141A809915>I<1218123CA212181200A612FC121CAE12FF081A80990A>II<12FC121CA9EB 1FC0EB0F00130C5B13205B13E0121DEA1E70EA1C7813387F131E7F148038FF9FE0131A80 9914>I<12FC121CB3A6EAFF80091A80990A>I<38FC7C1F391D8E6380391E0781C0A2001C 1301AB39FF9FE7F81D107F8F20>IIIIIII<1208A41218A21238 EAFFC0EA3800A81320A41218EA1C40EA07800B177F960F>I<38FC1F80EA1C03AB130712 0CEA0E0B3803F3F01410808F15>I<38FF0F80383C0700EA1C061304A26C5AA26C5AA3EA 03A0A2EA01C0A36C5A11107F8F14>I<39FE7F1F8039381C0700003C1306381C0C04130E 380E16081317A238072310149013A33803C1A014E0380180C0A319107F8F1C>I<38FE3F 80383C1E00EA1C086C5AEA0F306C5A6C5A12017F1203EA0270487E1208EA181CEA381E38 FC3FC012107F8F14>I<38FF0F80383C0700EA1C061304A26C5AA26C5AA3EA03A0A2EA01 C0A36C5AA248C7FCA212E112E212E4127811177F8F14>III127 D E /Fv 15 117 df<127812FCA412780606 7D850C>46 D48 D50 DI<1306130E131E133E137E13 DEEA019E131E12031206120C12181230126012C0B512E0A238001E00A53801FFE0A21318 7F9716>II<1260387FFFC0A214801400 EAE00612C05B5BC65A5B13E0A212015B1203A31207A66C5A12197E9816>55 D57 D<1303497EA2497EA3EB 1BE0A2EB3BF01331A2EB60F8A2EBE0FCEBC07CA248487EEBFFFE487FEB001F4814800006 130FA248EB07C039FF803FFCA21E1A7F9921>65 D97 D<12FCA2123CA713FE383F8780383E01C0003C13E0EB00F0A214F8A514F0A2EB01E0003E 13C0383B07803830FE00151A7E9919>II114 DI<1206 A4120EA2121EEA3FF012FFEA1E00A81318A5EA0F30EA03E00D187F9711>I E /Fw 58 128 df<903803F0F090380E19989038183B38EC33309038380700A3EB700EA3 0007B512E03900700E0013E05CA4EA01C05CA4EA03805CA3130048136014E0386630C038 E67180D8CC63C7FCEA783E1D21819918>11 D<1218123CA2121C1208A312101220124012 80060B78990C>39 D<130413181330136013C013801201EA0300A21206120E120C121C12 18A212381230A21270A21260A312E0A35AA51260A31220123012107E0E267B9B10>I<13 4013601320133013101318AB1338A21330A21370A2136013E013C0A21201138012031300 1206A25A5A12105A5A5A0D267F9B10>I<121812381278123812081210A21220A2124012 80050B7D830C>44 DI<1230127812F0126005047C830C>I< 1308131813301370EA01F0EA0E70EA00E0A4EA01C0A4EA0380A4EA0700A45AEAFFE00D18 7C9714>49 D<133E13C3380101801202380481C0134138088380120438070300EA00065B EA01F0EA00187FA2130EA21260EAE01CA2EA8038EA4030EA20E0EA1F8012187D9714>51 D<13031480EB0700A3130EA35BA213185BA25B5B13C6EA018EEA030EEA021C1204120812 10EA7FB838807F8038003800A25BA41360111F7F9714>I<131EEB6180EA0180EA030312 06000EC7FC5A12181238EA39F0EA7218EA740CEA780E127012F012E0A35BA2EA60385BEA 30C0EA1F8011187C9714>54 D<137CEA0186EA0703120E000C1380121C1238A313071400 5BEA1817EA0C27EA07CEEA000E130C131C1318EAE0305BEA80C0EAC380003EC7FC11187C 9714>57 D<1206120F121E120C1200A81230127812F0126008107C8F0C>I<1420146014 E0A2130114F0EB0270A213041308A21310A213201340A2EB8038EBFFF8380100381202A2 5AA25A121838FE01FF181A7E991D>65 D<3803FFF83800700E1406140713E0A43801C00E 141C143814703803FFE0EB80781438141CEA0700A4000E1338A2147014E0381C03C0B512 00181A7D991B>II< 3803FFF83800700E80809038E00180A315C0EA01C0A43903800380A3150048485AA2140E 140C000E131C5C5C5C381C0380D8FFFEC7FC1A1A7D991D>I<0003B5FC38007007140314 0113E0A43801C080A313C13803FF001381A3EA0702EB0004A21408120E14181410143048 13E0B5FC181A7D991A>I<0003B5FC380070071403140113E0A43801C080A313C13803FF 001381A3EA070290C7FCA3120EA4121EEAFFC0181A7D9919>I<3903FF1FF83900700380 A39038E00700A43801C00EA43803FFFCEB801CA348485AA4000E5BA4485B38FF87FC1D1A 7D991D>72 DII<3903FF03F039007001C015001402495A5C5C144048485A01C1C7FC13C313 C738038B80139313C3EB81C0EA0701A26D7EA2120E1470A348137838FF81FE1C1A7D991D >III<3903F007F839007800C01580A290389C0100A313 8E38010E0213061307A238020384A3EB01C4000413C8A2EB00E8A24813F01470A2121814 2012FE1D1A7D991D>II<3803FFF83800701C1406140713E0A43801C00EA2141C143838 038060EBFF80EB8000A248C7FCA4120EA45AB47E181A7D991A>I83 D<383FFFFC38381C0C0020130412 4013381280A338007000A45BA4485AA4485AA41207EAFFF8161A79991B>I<387FE0FF38 0E00181410A2481320A4481340A4481380A438E00100A31302A25BEA60085BEA3860EA0F 80181A78991D>I<3AFF87FC1FC03A3C00E007000038140413015D1302001C5C13045D13 085D13105DD920E1C7FC134014E2138014E4EA1D0014E8121E1470121C14601218144022 1A789926>87 D97 D<127E120EA35AA45AA2EA3BC0EA3C301278EA7018A3EAE038A4 EAC070136013E0EA60C0EA6380EA1E000D1A7C9912>IIII<1307EB0980131BEB3B00133813301370A4EA07FFEA00 E0A5485AA5485AA490C7FC5AA21206126612E412CC1270112181990C>I<13F338038B80 38060700120E120C121CEA380EA4EA301CA3EA183C5BEA07B8EA0038A25B1260EAE0E0EA C1C0007FC7FC11177E8F12>II<120312071206 1200A61238124C124E128E129CA2121C1238A212701272A212E212E41264123808197C98 0C>I107 D<121F1207A3120EA4121C A41238A41270A412E4A412E81230081A7D990A>I<38307C1E38598663399E0783801403 129CA239380E0700A3140ED8701C1340A2141C158038E0380C39601807001A107C8F1F> IIIIIII<1206120EA45AA2EAFFC0EA1C005AA45AA412E1A312E212E412380A177C 960D>III<38380C10384C0E38EA4E1C008E1318129CA2381C38 101238A338707020A2144012303818B880380F0F0015107C8F19>III123 D127 D E /Fx 87 128 df0 D4 DI<3803FFFC38001F806DC7FCA4EB 7FE03803CF3C38070F0E001EEB0780003CEB03C0007C14E00078130100F814F0A5007814 E0007C1303003C14C0001EEB07800007EB0E003803CF3C38007FE0010FC7FCA4497E3803 FFFC1C1F7E9E21>8 D<3801FFFE38000FC06D5AA300F8147C003C14F0A2001EEB81E0A9 000FEB83C0A200071480EB8787000314003801C78E380077B8EB1FE0EB0780A4497E3801 FFFE1E1F7E9E23>I<90381F83E09038F06E303901C07878380380F8903800F03048EB70 00A7B612803907007000B2383FE3FF1D20809F1B>11 D<133FEBE0C0EA01C0380381E0EA 0701A290C7FCA6B512E0EA0700B2383FC3FC1620809F19>II<90381F81F89038F04F043901C07C06 390380F80FEB00F05A0270C7FCA6B7FC3907007007B23A3FE3FE3FE02320809F26>I<12 7012F8A71270AA1220A51200A5127012F8A3127005217CA00D>33 DI<127012F812FCA212741204A31208A21210A212201240060E7C9F0D>39 D<13401380EA01005A12061204120C5AA212381230A212701260A412E0AC1260A4127012 30A212381218A27E120412067E7EEA008013400A2E7BA112>I<7E12407E12307E120812 0C7EA212077EA213801201A413C0AC1380A412031300A25A1206A25A120812185A12205A 5A0A2E7EA112>I<1303AFB612FCA2D80003C7FCAF1E207E9A23>43 D<127012F012F8A212781208A31210A31220A21240050E7C840D>II<127012F8A3127005057C840D>I<144014C0EB0180A3EB0300A31306A25BA35BA35B A25BA35BA3485AA348C7FCA21206A35AA35AA25AA35AA35AA2122D7EA117>II<13801203120F12F31203B3A6EA07C0EAFFFE0F1E7C9D 17>III<1306A2130EA2131E132EA2134E138EA2EA010E1202A212041208 A212101220A2124012C0B512F038000E00A7EBFFE0141E7F9D17>II<137CEA0182EA0701380E0380 EA0C0712183838030090C7FC12781270A2EAF1F0EAF21CEAF406EAF807EB0380A200F013 C0A51270A214801238EB07001218EA0C0E6C5AEA01F0121F7E9D17>I<1240387FFFE014 C0A23840008038800100A21302485AA25B5BA25BA21360A213E05B1201A41203A76C5A13 1F7E9D17>III<127012F8A312701200AA127012F8A3 127005147C930D>I<127012F8A312701200AA127012F012F8A212781208A31210A31220 A21240051D7C930D>I61 D<5B497EA3497EA3EB09E0A3EB10F0A3EB2078A3497EA2EBC03EEB801EA248B5FCEB000F A20002EB0780A348EB03C0A2120C001E14E039FF801FFE1F207F9F22>65 DI<90380FE0109038381C30 9038E002703803C00139078000F048C71270121E15305A1510127C127800F81400A91278 007C1410123CA26C1420A27E6C6C13406C6C13803900E00300EB380CEB0FF01C217E9F21 >IIII<90380FE01090 38381C309038E002703803C00139078000F048C71270121E15305A1510127C127800F814 00A7EC3FFEEC01F000781300127C123CA27EA27E6C7E3903C001703900E002309038380C 1090380FF0001F217E9F24>I<39FFF07FF8390F000780AD90B5FCEB0007AF39FFF07FF8 1D1F7E9E22>II<3807FFC038003E00131EB3A3 122012F8A3EAF01CEA403CEA6038EA1070EA0FC012207F9E17>I<39FFF007FC390F0003 E0EC0180150014025C5C5C5C5C5C49C7FC5B497E130FEB13C0EB21E01341EB80F0EB0078 A28080A280EC0780A2EC03C015E015F039FFF01FFE1F1F7E9E23>IIIIII82 D<3803F040380C0CC0EA1803EA3001EA6000A2 12E01440A36C13007E127CEA7F80EA3FF86CB4FC00071380C613C0EB1FE013031301EB00 F014707EA46C136014E06C13C038F8018038C60300EA81FC14217E9F19>I<007FB512E0 38780F010060EB006000401420A200C0143000801410A400001400B3497E3803FFFC1C1F 7E9E21>I<39FFF00FF8390F0003E0EC0080B3A46CEB01001380120314026C6C5A6C6C5A EB3830EB0FC01D207E9E22>I<39FFF003FE391F8000F86CC7126015206C6C1340A36C6C 1380A2EBE00100011400A23800F002A213F8EB7804A26D5AA36D5AA2131F6D5AA2EB07C0 A36D5AA36DC7FC1F207F9E22>I<3BFFF07FF81FF03B1F000FC007C06C90390780018017 0015C001805C00071502EC09E013C000035DEC19F01410D801E05CA2EC2078D800F05CA2 EC403C01785CA2EC801E017C1460013C144090383D000F133F6D5CA2011E1307010E91C7 FCA2010C7F010413022C207F9E2F>I<12FFA212C0B3B3A512FFA2082D7CA10D>91 DI<12FFA21203B3B3A512FFA2082D80A10D>I<120C121E1233EA6180EAC0C0EA80400A 067A9E17>I<120812101220A21240A21280A312B812FCA2127C1238060E7D9F0D>96 DI<121C12FC121CAA137CEA1D87381E0180EB00 C0001C13E01470A21478A6147014F014E0001E13C0381A018038198700EA107C15207E9F 19>IIII<137CEA01C6EA030F1207EA0E061300A7EAFFF0EA0E00B2EA7FE0 1020809F0E>I<14E03803E330EA0E3CEA1C1C38380E00EA780FA5EA380E6C5AEA1E38EA 33E00020C7FCA21230A2EA3FFE381FFF8014C0383001E038600070481330A4006013606C 13C0381C03803803FC00141F7F9417>I<121C12FC121CAA137C1386EA1D03001E1380A2 121CAE38FF8FF014207E9F19>I<1238127CA31238C7FCA6121C12FC121CB1EAFF80091F 7F9E0C>I<13E0EA01F0A3EA00E01300A61370EA07F012001370B3A31260EAF06013C0EA 6180EA3F000C28829E0E>I<121C12FC121CAAEB1FE0EB0780EB060013045B5B5B136013 E0EA1DF0EA1E70EA1C38133C131C7F130F7F148014C038FF9FF014207E9F18>I<121C12 FC121CB3ABEAFF8009207F9F0C>I<391C3E03E039FCC30C30391D039038391E01E01CA2 001C13C0AE3AFF8FF8FF8021147E9326>IIII<3801F04038070CC0EA0E02EA1C03EA38011278127012F0A612 7012781238EA1C03EA0C05EA0709EA01F1EA0001A8EB0FF8151D7F9318>III<1202A31206A2120EA2123EEAFFF8EA0E00AB1304A5EA07081203EA01F00E1C 7F9B12>I<381C0380EAFC1FEA1C03AE1307120CEA061B3803E3F014147E9319>I<38FF83 F8383E00E0001C13C06C1380A338070100A21383EA0382A2EA01C4A213E4EA00E8A21370 A3132015147F9318>I<39FF9FE1FC393C078070391C030060EC8020000E1440A214C0D8 0704138014E0A239038861001471A23801D032143A143E3800E01CA2EB6018EB40081E14 7F9321>I<38FF87F8381E03C0380E0180EB0300EA0702EA0384EA01C813D8EA00F01370 137813F8139CEA010E1202EA060738040380000C13C0003C13E038FE07FC16147F9318> I<38FF83F8383E00E0001C13C06C1380A338070100A21383EA0382A2EA01C4A213E4EA00 E8A21370A31320A25BA3EAF080A200F1C7FC1262123C151D7F9318>III127 D E /Fy 24 121 df<127812FCA212FEA2127A1202A41204A31208A212101220 124007127BA910>39 D<127812FCA412781200AE127812FCA41278061A7B9910>58 D68 D<007FB612F0A2397C00F8010070EC00700060153000401510 A200C01518A2481508A5C71400B3A6497E90B512F8A225297EA82A>84 D<3DFFFC03FFF003FF80A2270FE0003FC7EA7C006C4816386F14107F00035F6F7EA26C6C 5EED17C0A26C6C5EED23E0A2017C4BC7FCED41F0A26D1502ED80F8A26D5D913801007CA2 D90F815C0283137E0282133E02C21418D907C6EB3F1002C4131F02E41430010315A002E8 130F14F8010115C04A1307A201005D4A1303A2026091C8FC02407F392A7FA83C>87 D 97 D<137F3801C0E038070010000E1378001E13F85A1470007C13200078130012F8A812 78127C003C1308A26C1310000E13206C13603801C18038007E00151A7E991A>99 D<140F14FFA2141F80AC133F3801C0CF3803802F380F001F121E001C7F123C127C1278A2 12F8A71278A27EA26C5B000E132F6CEB4F803901C18FF038007E0F1C2A7EA921>I<13FC 38038780380701C0000E13E0EA1C00003C13F0A2481378A212F8A2B512F800F8C7FCA512 78A26C1308A26C1310000E13206C13403801C18038007E00151A7E991A>I<131FEB70C0 EBE1E0EA01C31203EB81C0380780801400A9EAFFFEA2EA0780B3A37FEA7FFCA2132A7FA9 12>I<140F3901FC308038070743380E03C3001EEBC100486C7EA2007C7FA5003C5BA26C 485A000E5BD81707C7FCEA11FC0030C8FCA47E381FFF806C13F06C7F3818007C48131E00 70130E00607F12E0A40070130EA26C5B6C5B380781E0C6B4C7FC19287E9A1D>I<120FB4 FCA2121F7EACEB07F0EB1838EB201C497E140F1380A21300B139FFF0FFF0A21C2A7EA921 >I<121E123FA4121EC7FCA9120FB4FCA2121F7EB3A2EAFFF0A20C297EA811>I<120FB4FC A2121F7EACECFFC0A2EC7E0014305C14405C0103C7FC1304130C131E133E135F138FEB07 80801303806D7E1300801478147C147E39FFF1FFE0A21B2A7EA91F>107 D<120FB4FCA2121F7EB3B2EAFFF0A20C2A7EA911>I<3A0F07F007F03AFF183818389039 201C201C3A1F400E400E000F010F130F01801380A201001300B13BFFF0FFF0FFF0A22C1A 7E9931>I<380F07F038FF1838EB201C381F400E000F130F1380A21300B139FFF0FFF0A2 1C1A7E9921>I<137E3803C3C0380700E0000E1370481338003C133CA248131EA200F813 1FA80078131EA26C133CA2001C13386C13706C13E03803C3C038007E00181A7E991D>I< 380F07E038FF1838EB601E380F800FEC0780010013C0140315E0A2EC01F0A715E01403A2 15C0EC07801380EC0F00EB401CEB3078EB0FC090C8FCAAEAFFF0A21C267E9921>I<380F 0F8038FF11C0EB23E0EA1F43EA0F83EB81C0EB800090C7FCB07FEAFFFCA2131A7E9917> 114 D<3807F080EA1C0DEA3003EA600112E01300A27E6C1300127EEA7FE0EA3FFC6C7EEA 07FF38003F801307388003C0A2130112C0A200E01380130300F01300EACC0EEA83F8121A 7E9917>I<7FA41201A31203A21207120F381FFF80B5FC38078000AD1440A73803C08012 013800E100133E12257FA417>I<3AFFF3FF83FEA23A1F803C00F8D80F001460EB801C00 07011E1340A2D9C02E13C00003012F1380A23A01E04701001581A23900F0838215C2A290 387901C415E4137B90383E00E815F8A2011C1370A20118133001081320271A7F992A> 119 D<39FFF03FF0A2390FC01F003807801C3803C0183801E0106D5A00005BEB78C06D5A 013DC7FC7F7F80A2EB13C0EB21E0EB61F01340EB80783801007C48133C487F001F133F39 FF807FF8A21D1A7F991F>I E end %%EndProlog %%BeginSetup %%Feature: *Resolution 300dpi TeXDict begin %%PaperSize: a4 /pstopsxform pstopsmatrix matrix currentmatrix matrix invertmatrix matrix concatmatrix matrix invertmatrix store %%EndSetup %%Page: pstops 1 /pstopssaved save def pstopsmatrix setmatrix 708.661417 0.000000 translate 90 rotate 0.880000 dup scale /pstopsmatrix matrix currentmatrix def initclip pstopsxform concat /showpage{}def/copypage{}def/erasepage{}def 1 0 bop 243 145 a Fy(The)31 b(W)-5 b(arshall)31 b(algorithm)e(and)i (Dic)n(kson's)g(lemma:)g(Tw)n(o)243 224 y(examples)18 b(of)i(realistic)d(program)i(extraction)243 367 y Fx(Ulric)o(h)d (Berger)243 413 y Fw(Dep)n(artment)c(of)h(Computer)g(Scienc)n(e,)e (University)f(of)j(Wales)g(Swanse)n(a)243 488 y Fx(Helm)o(ut)i(Sc)o(h)o (wic)o(h)o(ten)o(b)q(erg)h(and)g(Monik)m(a)f(Seisen)o(b)q(erger)243 534 y Fw(Mathematisches)10 b(Institut)i(der)h(Ludwig-Maximilians)o(-Un) o(ive)o(rsit\177)-21 b(at)11 b(M\177)-20 b(unchen)243 650 y Fv(Abstract.)41 b Fu(By)20 b(means)f(of)g(t)o(w)o(o)f(w)o (ell-kno)o(wn)j(examples)f(it)f(is)h(demonstrated)g(that)f(the)243 696 y(metho)q(d)12 b(of)f(extracting)h(programs)g(from)f(pro)q(ofs)h (is)g(manageable)h(in)f(practice)g(and)g(ma)o(y)g(yield)243 741 y(e\016cien)o(t)18 b(programs.)f(The)g(W)m(arshall)j(algorithm)f (computing)g(the)e(transitiv)o(e)i(closure)g(of)d(a)243 787 y(relation)e(is)e(extracted)h(from)e(a)h(constructiv)o(e)i(pro)q (of)e(that)g(rep)q(etitions)i(in)f(a)f(path)g(can)g(alw)o(a)o(ys)243 832 y(b)q(e)i(a)o(v)o(oided.)h(Secondly)m(,)h(w)o(e)d(extract)h(a)g (program)h(from)e(a)h(classical)i(\(i.e.)e(non)h(constructiv)o(e\))243 878 y(pro)q(of)d(of)g(a)h(sp)q(ecial)h(case)e(of)g(Dic)o(kson's)i (Lemma,)e(b)o(y)h(transforming)h(the)e(classical)j(pro)q(of)d(in)o(to) 243 923 y(a)i(constructiv)o(e)h(one.)f(These)g(tec)o(hniques)i(\(as)e (w)o(ell)g(as)g(the)g(examples\))i(are)e(implemen)o(ted)i(in)243 968 y(the)d(in)o(teractiv)o(e)i(theorem)e(pro)o(v)o(er)h Ft(Minlog)f Fu(dev)o(elop)q(ed)i(at)e(the)g(Univ)o(ersit)o(y)i(of)d (Munic)o(h.)757 1162 y Fs(1.)37 b(In)o(tro)q(duction)243 1268 y Fx(The)18 b(ob)s(jectiv)o(e)g(of)f(this)h(pap)q(er)h(is)f(to)f (sho)o(w)g(that)g(the)h(metho)q(d)g(of)g(extracting)243 1322 y(programs)f(from)h(pro)q(ofs)f(is)i(not)f(only)h(a)f(p)q(o)o(w)o (erful)h(metamathematical)f(to)q(ol,)243 1376 y(but)c(is)h(also)g(of)f (considerable)i(practical)f(in)o(terest:)f(used)h(in)g(a)g(re\014ned)g (w)o(a)o(y)e(it)i(is)243 1430 y(applicable)f(to)d(rather)g(in)o(v)o (olv)o(ed)i(pro)q(ofs)e(and)h(yields)h(concise)g(and)f(e\016cien)o(t)h (pro-)243 1483 y(grams)i(whic)o(h)h(moreo)o(v)o(er)f(are)g(pro)o(v)m (ably)i(correct.)e(W)l(e)g(presen)o(t)h(t)o(w)o(o)f(examples)243 1537 y(highligh)o(ting)h(di\013eren)o(t)e(asp)q(ects)g(of)f(the)h (metho)q(d.)g(The)g(\014rst)f(is)i(a)e(constructiv)o(e)243 1591 y(pro)q(of)i(dominated)h(b)o(y)g(equational)g(reasoning.)g(It)f (is)h(dramatically)h(simpli\014ed)243 1645 y(b)o(y)c(an)g(extensiv)o(e) i(use)e(of)g(term)g(rewriting)h(tec)o(hniques.)h(The)e(second)h(is)g(a) f(short)243 1699 y(and)h(elegan)o(t)h(non-constructiv)o(e)g(pro)q(of.)e (W)l(e)i(translate)e(it)i(in)o(to)f(a)g(constructiv)o(e)243 1753 y(pro)q(of)h(and)g(extract)f(an)i(e\016cien)o(t)f(higher)h(t)o(yp) q(e)g(program.)301 1829 y(In)j(the)g(follo)o(wing)g(w)o(e)g(discuss)h (the)e(examples)i(in)f(some)g(detail.)g(The)g(\014rst)243 1883 y(starts)14 b(from)g(a)h(constructiv)o(e)g(pro)q(of)g(of)g(the)g (follo)o(wing)243 1970 y Fr(Pr)o(oposition)e([W)-5 b(arshall].)24 b Fq(F)l(or)12 b(ev)o(ery)h(t)o(w)o(o)e(p)q(oin)o(ts)i Fp(j;)8 b(k)13 b Fq(in)g(the)g(\014nite)g(\014eld)243 2024 y(of)f(a)g(giv)o(en)h(relation)g Fp(R)g Fq(w)o(e)f(can)h(either)g (\014nd)g(a)g(rep)q(etition-free)h Fp(R)p Fq(-path)e(leading)243 2078 y(from)i Fp(j)k Fq(to)c Fp(k)i Fq(or)f(else)h(\014nd)g(that)f (there)g(is)h(no)f(suc)o(h)g Fp(R)p Fq(-path.)301 2154 y Fx(Giv)o(en)f(this)h(pro)q(of,)e(w)o(e)h(can)g(extract)g(a)f(v)o(ery) h(short)g(and)g(readable)h(program)243 2208 y(that)k(corresp)q(onds)i (to)e(the)i(W)l(arshall)g(algorithm.)f(This)g(is)h(remark)m(able,)g(b)q (e-)243 2262 y(cause)f(the)f(naiv)o(e)h(test)f(for)g(reac)o(habilit)o (y)i(via)f(the)g(relation)g Fp(R)f Fx(in)i(a)e(set)g(of)g Fp(n)243 2316 y Fx(elemen)o(ts)f(has)f(complexit)o(y)h Fp(O)q Fx(\()p Fp(n)828 2300 y Fo(4)847 2316 y Fx(\),)f(whereas)g(the)g (W)l(arshall)h(algorithm)f(do)q(es)243 2370 y(the)12 b(same)g(with)h(complexit)o(y)g Fp(O)q Fx(\()p Fp(n)839 2354 y Fo(3)859 2370 y Fx(\).)e(The)i(reason)f(for)g(the)g(fact)g(that) g(our)g(pro)q(of)243 2424 y(yields)19 b(the)f(b)q(etter)g(algorithm)g (is)h(of)f(course)g(the)g(phrase)g(`rep)q(etition-free')h(in)243 2569 y @beginspecial @setspecial 4 4 translate 989 1138 1 [60 0 0 -60 210 930] currentfile /ASCII85Decode filter << /K -1 /Columns 989 >> /CCITTFaxDecode filter image Q>'H49/K0rjdMhW-(A!cb;A.`/DC9EH"NLrmTGB3G`p9Q"2Q+cbR4Nj7'd7dn1Os5 $DPm^#D5dp.Sq0)HOI.%W!@rm_0-3j?%po`_0-3j?%VDq_0-W'Fr+S1(LXi_Ye(:I ]*kjT$a@6KL"blG_X2L_CTtEVL"blG_X2L_CTtEVY/9RL]*l%#ln6muG.V%6g?j&" CUMm`Fr+r%g?j'q?%q#"G.V%_f3rj7?*;dp[G("lm<6*IY1IHshmM2*G.V%_f7)=e [G("lm<6*Iqd$AVIb/AMCUMmbg?j'qp:FV5rN=b$f7)=e^MCT"[GSCL[G(*'m<@rA m<6,8\:3%Yf7)>#f7)>#f7)>#f7)>#f7)>#f7)>#f7)>#f7)>#rN?+r?2Iq)p:L(d GOO8ShmM@LhnNsAIb0&IY5S7k]D(dJn)(P1^OFd`rVKmtp:L(fg@*q6CVP>sqd'*n n)(lq^OH.Yp[*1nhnOWlIf90sqtKR:^OH.Yp[@"SCVP>s qtKQ8s8U1@C);u92$r0TIf90CC\p\,F'GICC\nD=uZ_hb.nbI4`5$oX=e/f5K6t?,'TlG5Z:Ng\&&-DqCYDlD=uZV\(>QLhd*s^hlchCoX=e/dbFH(f5ILprP"TT?+uW^XhMDq /\\iG[ea3VG5>El[ea3VG5>El[ea3VG5>El[efC`[ea3V/\\iF/\[P.XhMDq/\[P. 95gZ9f5ILpdbF#'oX=U#J(s4)oX=U#I4`1!hb.mjhb.ma\'j$qD=k:5>CA*;QJW!c oX=U#I4`1FI4`1!hb.ma\'j$qD=EkK95gZ9_HVF?^(T2bD=eV$$#T=CqHJ=n\'j$i /\[P.95fJ!hb.m@[eNL6V74;LDl'q[>C7R%qHJ=i[eNL6V74;LDl'q[$ZC^,qHJ=Y >C7a+_@(:8[eN.*n:KEQQJVs"^(T2Z"h2?QHm#lm6#H*aDh8@8Jm3UF[eLuRp`R$? 6#H*WD=C2:KGNGN/\XRt27@;0aCL$khf"Uu#*%Ks"Le+7OAWdIj>'(dl*n`EL,P%* &6jO::U(jdL-R$a;@XEKW5W@E:h]\'fZTZ&2IlgdAO,jOIenNlo_n[O qs""Pe+_>cn#,WPn)$pu^7W-3^O8=p5CGbE5CGbE5CGbE5CGcgrUg'\rUg'\qL89h 5CG_f^7S3Y:Z"sGn#+Y/e*6boo_nFYI6W-DT22BRVpjo-l1Fh#5CG_f:T*ZZe*6N$ I6O9!Vpjo&qL(Q":T)\+o_Nu"T21.:I6O9!K_g*\T21.:I6O9!K_g*\'C#/a:T)'X 5+`/RpeRg)I6O80o_;48peQS>HmcdY-e%$<'B)+gl0qK%paFT*b&n L=7gF:P*s-i1C/I-c%t[j:;B)"QU(.PuEc.AeiBCZN4SP=c/;D"]f?=L:]C?)O[;? Ai"3B!'gY~> @endspecial 353 2532 a Fu(c)342 2533 y Fn(\015)14 b Fu(2001)f Fw(Kluwer)h(A)n(c)n(ademic)e (Publishers.)24 b(Printe)n(d)13 b(in)g(the)f(Netherlands.)912 2924 y Fm(finaljar2)o(.te)o(x;)k(29/01/2001)o(;)g(14:37;)i(p.1)p eop pstopssaved restore /pstopssaved save def pstopsmatrix setmatrix 708.661417 368.503937 translate 90 rotate 0.880000 dup scale /pstopsmatrix matrix currentmatrix def initclip pstopsxform concat 2 1 bop 243 50 a Fx(2)243 145 y(the)15 b(statemen)o(t.)e(But)i(at)f (the)h(`mathematical')g(lev)o(el)h(this)f(is)g(a)g(rather)f(ob)o(vious) 243 199 y(requiremen)o(t,)d(and)g(since)h(the)f(program)f(can)h(b)q(e)h (obtained)g(automatically)f(once)243 253 y(the)16 b(formal)f(pro)q(of)g (is)i(kno)o(wn)e(w)o(e)h(ha)o(v)o(e)f(here)i(an)e(instance)i(of)e(the)h (\(Bates)f(and)243 307 y(Constable,)g(1985\))f(goal)g(of)h(`v)o(ery)g (high)h(lev)o(el)g(programming'.)301 384 y(The)i(second)g(example,)g(a) f(sp)q(ecial)i(case)f(of)f(Dic)o(kson's)g(Lemma)h(\(Dic)o(kson,)243 438 y(1913\),)13 b(has)i(b)q(een)i(prop)q(osed)e(in)h(\(V)l(eldman)g (and)g(Bezem,)f(1993\).)243 526 y Fr(Pr)o(oposition)e([Dickson].)35 b Fq(Let)13 b Fp(f)5 b Fx(\(0\))p Fp(;)j(f)d Fx(\(1\))p Fp(;)j(:)f(:)g(:)i Fq(and)k Fp(g)r Fx(\(0\))p Fp(;)8 b(g)r Fx(\(1)o(\))p Fp(;)f(:)g(:)h(:)h Fq(b)q(e)k(t)o(w)o(o)243 580 y(in\014nite)18 b(sequences)f(of)e(natural)h(n)o(um)o(b)q(ers.)g (Then)g(there)g(are)g(indices)i Fp(i;)8 b(j)15 b Fl(2)f Fk(N)p Fq(,)243 634 y Fp(i)e(<)h(j)s Fq(,)h(suc)o(h)i(that)e Fp(f)5 b Fx(\()p Fp(i)p Fx(\))12 b Fl(\024)h Fp(f)5 b Fx(\()p Fp(j)s Fx(\))14 b Fq(and)h Fp(g)r Fx(\()p Fp(i)p Fx(\))c Fl(\024)i Fp(g)r Fx(\()p Fp(j)s Fx(\))p Fq(.)243 711 y Fj(Pr)n(o)n(of)c Fx(.)43 b(Let)22 b Fp(i)518 718 y Fo(0)561 711 y Fl(2)h Fk(N)e Fx(b)q(e)h(suc)o(h)g(that)f Fp(f)5 b Fx(\()p Fp(i)1012 718 y Fo(0)1031 711 y Fx(\))23 b(=)h(min)q Fl(f)8 b Fp(f)d Fx(\()p Fp(i)p Fx(\))21 b Fl(j)i Fp(i)g Fl(2)h Fk(N)8 b Fl(g)20 b Fx(and,)243 765 y(inductiv)o(ely)l(,)e Fp(i)502 772 y Fi(n)p Fo(+1)583 765 y Fp(>)c(i)648 772 y Fi(n)686 765 y Fx(suc)o(h)i(that)f Fp(f)5 b Fx(\()p Fp(i)949 772 y Fi(n)p Fo(+1)1017 765 y Fx(\))13 b(=)g(min)q Fl(f)8 b Fp(f)d Fx(\()p Fp(i)p Fx(\))12 b Fl(j)h Fp(i)g(>)g(i)1413 772 y Fi(n)1444 765 y Fl(g)p Fx(.)i(Clearly)243 819 y(w)o(e)g(ha)o(v)o(e)h Fp(i)432 826 y Fo(0)464 819 y Fp(<)e(i)529 826 y Fo(1)562 819 y Fp(<)g(:)8 b(:)g(:)14 b Fx(and)i Fp(f)5 b Fx(\()p Fp(i)830 826 y Fo(0)849 819 y Fx(\))13 b Fl(\024)h Fp(f)5 b Fx(\()p Fp(i)990 826 y Fo(1)1009 819 y Fx(\))13 b Fl(\024)h Fp(:)8 b(:)g(:)n Fx(.)16 b(By)g(the)f(w)o(ellfoundedness)243 873 y(of)10 b Fk(N)p Fx(,)f(the)i(sequence)h Fp(g)r Fx(\()p Fp(i)662 880 y Fo(0)681 873 y Fx(\))p Fp(;)c(g)r Fx(\()p Fp(i)778 880 y Fo(1)795 873 y Fx(\))p Fp(;)g(:)g(:)g(:)g Fx(cannot)i(alw)o(a)o(ys)g(decrease)h(strictly)l(.)h(Hence)243 927 y(there)18 b(is)g(a)f Fp(k)h Fl(2)f Fk(N)f Fx(suc)o(h)i(that)f Fp(g)r Fx(\()p Fp(i)853 934 y Fi(k)873 927 y Fx(\))g Fl(\024)g Fp(g)r Fx(\()p Fp(i)1018 934 y Fi(k)q Fo(+1)1083 927 y Fx(\).)g(No)o(w)g(the)h(n)o(um)o(b)q(ers)f Fp(i)g Fx(:=)g Fp(i)1617 934 y Fi(k)243 981 y Fx(and)e Fp(j)g Fx(:=)e Fp(i)442 988 y Fi(k)q Fo(+1)523 981 y Fx(are)i(as)g(required.) 301 1058 y(This)25 b(pro)q(of)f(can)g(b)q(e)h(view)o(ed)h(as)e(a)g (simpli\014cation)i(of)e(Nash{Williams')243 1112 y (minimal{bad{sequence)14 b(argumen)o(t)e(for)f(Higman's)h(lemma)g (\(Nash-Williams,)243 1166 y(1963\).)k(Clearly)j(it)f(is)h(not)f (constructiv)o(e)g(since)h(it)g(requires)g(determining)g(the)243 1220 y(minim)o(um)f(of)e(an)g(in\014nite)j(set.)d(Ho)o(w)o(ev)o(er,)f (b)o(y)i(applying)h(a)e(re\014ned)i(v)o(ersion)f(of)243 1274 y(the)f Fp(A)p Fx(-translation,)h(w)o(e)f(get)g(a)g(constructiv)o (e)h(pro)q(of)f(that)g(con)o(tains)h(a)f(\(higher)243 1328 y(t)o(yp)q(e\))d(primitiv)o(e)j(recursiv)o(e)e(program)f (computing)i(from)e(arbitrary)g(sequences)243 1382 y Fp(f)5 b Fx(\(0\))p Fp(;)j(f)d Fx(\(1\))p Fp(;)j(:)f(:)g(:)i Fx(and)k Fp(g)r Fx(\(0\))p Fp(;)8 b(g)r Fx(\(1)o(\))p Fp(;)f(:)g(:)h(:)h Fx(indices)15 b Fp(i)d(<)h(j)i Fl(2)e Fk(N)e Fx(suc)o(h)i(that)f Fp(f)5 b Fx(\()p Fp(i)p Fx(\))12 b Fl(\024)h Fp(f)5 b Fx(\()p Fp(j)s Fx(\))243 1436 y(and)15 b Fp(g)r Fx(\()p Fp(i)p Fx(\))c Fl(\024)i Fp(g)r Fx(\()p Fp(j)s Fx(\).)301 1513 y(The)g(pap)q(er)g(is)h(organized)f(as)g(follo)o (ws.)f(Section)i(2)f(con)o(tains)g(a)f(brief)i(descrip-)243 1567 y(tion)i(of)g(the)g(formal)f(system)h(w)o(e)g(are)f(w)o(orking)h (with.)g(In)h(section)f(3)g(w)o(e)g(sk)o(etc)o(h)243 1621 y(program)g(extraction)i(via)g(Kreisel's)h(mo)q(di\014ed)g (realizabilit)o(y)h(and)e(apply)g(this)243 1675 y(in)d(section)g(4)f (to)f(the)i(W)l(arshall)g(example.)g(In)f(section)h(5)f(w)o(e)g(dev)o (elop)i(a)e(re\014ned)243 1729 y(v)o(ersion)h(of)g(the)g Fp(A)p Fx(-translation)h(whic)o(h)g(will)h(enable)f(us)g(in)g(section)f (6)g(to)g(trans-)243 1783 y(form)f(the)i(classical)h(pro)q(of)e(of)g (our)g(Dic)o(kson)h(prop)q(osition)g(in)o(to)f(a)g(constructiv)o(e)243 1836 y(pro)q(of)g(and)g(to)g(obtain)g(a)g(program)f(from)g(the)i (translated)f(pro)q(of.)301 1890 y(Both)j(examples)h(are)f(implemen)o (ted)j(in)e(the)f(in)o(teractiv)o(e)h(theorem)f(pro)o(v)o(er)243 1944 y Fr(Minlog)24 b Fx(dev)o(elop)q(ed)j(at)d(the)g(univ)o(ersit)o(y) i(of)e(Munic)o(h.)h(F)l(or)f(a)g(brief)i(in)o(tro-)243 1998 y(duction)c(to)g(the)f(system)h(see)g(\(Benl)g(et)g(al.,)f (1998\).)f(The)i Fr(Minlog)g Fx(system)243 2052 y(as)i(w)o(ell)i(as)e (the)g(examples)i(and)f(the)f Fr(Minlog)h Fx(man)o(ual)g(are)f(a)o(v)m (ailable)i(at)243 2106 y(h)o(ttp://www.mathematik.uni-m)o(uenc)o (hen.de/)p Fl(\030)p Fx(logik/)298 2264 y Fs(2.)36 b(In)o(tuitionistic) 20 b(arithmetic)f(for)e(functionals)i(of)f(\014nite)g(t)o(yp)q(e)243 2370 y Fx(The)11 b(system)g(w)o(e)g(consider)i(is)f(essen)o(tially)h (Heyting's)e(in)o(tuitionistic)j(arithmetic)243 2424 y(in)22 b(\014nite)h(t)o(yp)q(es)e Fl(HA)626 2406 y Fi(!)673 2424 y Fx(as)g(describ)q(ed)i(e.g.)e(in)h(\(T)l(ro)q(elstra,)f(1973\).) e(Classical)912 2924 y Fm(finaljar2)o(.te)o(x;)d(29/01/2001)o(;)g (14:37;)i(p.2)p eop pstopssaved restore %%Page: pstops 2 /pstopssaved save def pstopsmatrix setmatrix 708.661417 0.000000 translate 90 rotate 0.880000 dup scale /pstopsmatrix matrix currentmatrix def initclip pstopsxform concat /showpage{}def/copypage{}def/erasepage{}def 3 2 bop 772 50 a Fo(W)m(arshall)10 b(and)g(Dic)o(kson)505 b Fx(3)243 145 y(arithmetic)15 b(is)f(obtained)h(b)o(y)g(restriction)f (to)g(form)o(ulas)g(without)g(the)g(construc-)243 199 y(tiv)o(e)h(existen)o(tial)g(quan)o(ti\014er)h Fl(9)777 183 y Fh(\003)811 199 y Fx(but)f(using)g(the)g(classical)h (de\014nition)h Fl(9)c Fx(=)g Fl(:8:)243 253 y Fx(instead.)k(Equations) g(are)g(treated)g(on)g(the)g(meta)g(lev)o(el)h(b)o(y)f(iden)o(tifying)i (terms)243 307 y(with)c(the)h(same)e(normal)i(form.)243 412 y(2.1.)30 b Fr(G)386 408 y(\177)384 412 y(odel)m('s)17 b(system)g Fx(T)243 507 y(W)l(e)k(use)g(G\177)-23 b(odel's)21 b(system)f(T)h(of)f(primitiv)o(e)j(recursiv)o(e)e(functionals)h(of)f (\014nite)243 561 y(t)o(yp)q(e)d(form)o(ulated)g(as)h(a)f(simply)h(t)o (yp)q(ed)g(lam)o(b)q(da)g(calculus)h(with)f(higher)g(t)o(yp)q(e)243 615 y(arithmetic)d(constan)o(ts.)243 691 y Fj(T)m(yp)n(es.)44 b Fg(b)q(o)q(ole)13 b Fl(j)f Fg(nat)h Fl(j)g Fp(\032)c Fl(\002)i Fp(\033)j Fl(j)e Fp(\032)g Fl(!)h Fp(\033)r Fx(.)243 767 y Fj(Constants.)44 b Fg(true)575 750 y Ff(b)q(o)q(ole)670 767 y Fl(j)12 b Fg(false)779 748 y Ff(b)q(o)q(ole)873 767 y Fl(j)h Fx(0)922 750 y Ff(nat)984 767 y Fl(j)f Fg(S)1034 750 y Ff(nat)p Fh(!)p Ff(nat)1180 767 y Fl(j)g Fg(R)1234 774 y Ff(b)q(o)q(ole)p Fi(;\032)1357 767 y Fl(j)g Fg(R)1411 774 y Ff(nat)p Fi(;\032)1489 767 y Fx(.)243 843 y Fg(R)272 850 y Ff(nat)p Fi(;\032)368 843 y Fx(is)18 b(the)g(recursor)g(of)f(t)o (yp)q(e)h Fp(\032)f Fl(!)g Fx(\()p Fg(nat)h Fl(!)g Fp(\032)e Fl(!)i Fp(\032)p Fx(\))e Fl(!)i Fg(nat)g Fl(!)f Fp(\032)h Fx(\(where)243 897 y Fl(!)j Fx(asso)q(ciates)g(to)g(the)g(righ)o(t\).)f Fg(R)845 904 y Ff(b)q(o)q(ole)p Fi(;\032)976 897 y Fx(is)i(of)e(t)o(yp) q(e)h Fp(\032)h Fl(!)h Fp(\032)f Fl(!)h Fg(b)q(o)q(ole)g Fl(!)g Fp(\032)243 951 y Fx(and)d(represen)o(ts)h(b)q(o)q(olean)g (induction,)h(i.e.)e(de\014nition)i(b)o(y)e(cases.)g(Instead)h(of)243 1005 y Fg(R)272 1012 y Ff(b)q(o)q(ole)p Fi(;\032)382 1005 y Fp(r)q(s)8 b(t)15 b Fx(w)o(e)g(will)i(often)e(write)g Fg(if)j Fp(t)d Fg(then)i Fp(r)f Fg(else)g Fp(s)p Fx(.)301 1081 y(Dep)q(ending)21 b(on)e(applications)j(w)o(e)d(ma)o(y)f(add)i (further)f(ground)h(t)o(yp)q(es)f(and)243 1135 y(constan)o(ts.)243 1211 y Fj(T)m(erms.)44 b Fp(x)453 1194 y Fi(\032)486 1211 y Fl(j)12 b Fp(c)531 1194 y Fi(\032)566 1211 y Fx(\()p Fp(c)604 1194 y Fi(\032)639 1211 y Fx(a)j(constan)o(t\))c Fl(j)h(h)p Fp(r)o(;)c(s)p Fl(i)j(j)h Fp(\031)1060 1218 y Fo(0)1080 1211 y Fx(\()p Fp(r)q Fx(\))g Fl(j)g Fp(\031)1201 1218 y Fo(1)1221 1211 y Fx(\()p Fp(r)q Fx(\))f Fl(j)i Fp(\025x)1369 1194 y Fi(\032)1388 1211 y Fp(r)h Fl(j)e Fp(r)q(s)243 1287 y Fx(with)g(the)g(usual)h(t)o(yping)f(rules.)g(W)l(e) h(will)g(use)f(the)h(con)o(v)o(en)o(tion)f(that)f(application)243 1341 y(asso)q(ciates)g(to)g(the)g(left,)g(i.e.)g Fp(r)q(s)d(t)k Fx(means)f(\()p Fp(r)q(s)p Fx(\))p Fp(t)p Fx(,)g(and)g(the)g(\\dot)g (notation")g(whic)o(h)243 1395 y(mak)o(es)21 b(the)i(scop)q(e)f(of)g(a) g(binder)h(as)f(large)g(as)g(p)q(ossible,)i(i.e.)e Fp(\025x)8 b(:)g(r)q(s)21 b Fx(means)243 1449 y Fp(\025x)p Fx(\()p Fp(r)q(s)p Fx(\).)243 1525 y Fj(Conversions.)28 b Fx(\(W)l(riting)16 b Fp(t)10 b Fx(+)h(1)k(for)f Fg(S)p Fp(t)p Fx(.\))765 1613 y Fp(\031)791 1620 y Fo(0)810 1613 y Fl(h)p Fp(r)o(;)8 b(s)p Fl(i)23 b(7!)j Fp(r)765 1680 y(\031)791 1687 y Fo(1)810 1680 y Fl(h)p Fp(r)o(;)8 b(s)p Fl(i)23 b(7!)j Fp(s)768 1746 y Fx(\()p Fp(\025x)8 b(r)q Fx(\))p Fp(s)23 b Fl(7!)j Fp(r)q Fx([)p Fp(s=x)p Fx(])641 1813 y Fg(R)670 1820 y Ff(b)q(o)q(ole)p Fi(;\032)780 1813 y Fp(r)q(s)8 b Fg(true)25 b Fl(7!)h Fp(r)633 1879 y Fg(R)662 1886 y Ff(b)q(o)q(ole)p Fi(;\032)772 1879 y Fp(r)q(s)8 b Fg(false)24 b Fl(7!)i Fp(s)733 1946 y Fg(R)762 1953 y Ff(nat)q Fi(;\032)841 1946 y Fp(r)q(s)p Fx(0)e Fl(7!)i Fp(r)626 2012 y Fg(R)655 2019 y Ff(nat)p Fi(;\032)733 2012 y Fp(r)q(s)p Fx(\()p Fp(t)11 b Fx(+)f(1\))24 b Fl(7!)i Fp(st)p Fx(\()p Fg(R)1086 2019 y Ff(nat)p Fi(;\032)1164 2012 y Fp(r)q(st)p Fx(\))p Fp(:)243 2100 y Fx(W)l(e)15 b(let)g(=)421 2107 y Fi(\014)r Ff(R)482 2100 y Fx(denote)g(the)g(congruence)g(generated)g(b)o(y)g (these)g(con)o(v)o(ersions)f(and)243 2154 y(iden)o(tify)i(terms)e Fp(r)q Fx(,)g Fp(s)h Fx(with)g Fp(r)e Fx(=)791 2161 y Fi(\014)r Ff(R)851 2154 y Fp(s)p Fx(.)h(By)h(the)g(normalization)g (theorem)g(due)g(to)243 2208 y(\(T)l(ait,)c(1967\))g(and)h(\(T)l(ro)q (elstra,)f(1973\))g(ev)o(ery)h(term)f(in)i(G\177)-23 b(odel's)12 b(T)g(has)g(a)g(unique)243 2262 y(normal)j(form)f(w.r.t.)f (the)j(rewrite)f(relation)g(generated)g(b)o(y)g Fl(7!)p Fx(.)h(Hence)g(w)o(e)e(can)243 2316 y(decide)f(whether)e Fp(r)j Fx(=)618 2323 y Fi(\014)r Ff(R)677 2316 y Fp(s)e Fx(holds)g(b)o(y)g(normalizing)g(b)q(oth)g Fp(r)g Fx(and)g Fp(s)p Fx(.)f(T)l(reating)g(the)243 2370 y(calculus)k(mo)q(dulo)e(=)608 2377 y Fi(\014)r Ff(R)668 2370 y Fx(mak)o(es)f(pro)q(ofs)h(m)o(uc)o(h)g (shorter)f(and)h(more)g(p)q(erspicuous)243 2424 y(b)q(ecause)j(w)o(e)f (don't)g(ha)o(v)o(e)f(to)h(handle)h(equations)g(at)e(the)i(logical)g (lev)o(el.)912 2924 y Fm(finaljar2)o(.te)o(x;)g(29/01/2001)o(;)g (14:37;)i(p.3)p eop pstopssaved restore /pstopssaved save def pstopsmatrix setmatrix 708.661417 368.503937 translate 90 rotate 0.880000 dup scale /pstopsmatrix matrix currentmatrix def initclip pstopsxform concat 4 3 bop 243 50 a Fx(4)243 145 y(2.2.)30 b Fr(Arithmetic)243 244 y Fj(Pr)n(e)n(dic)n(ate)14 b(symb)n(ols)f(and)i(atomic)g(formulas.) 40 b Fx(Eac)o(h)13 b(predicate)h(sym)o(b)q(ol)g Fp(P)20 b Fx(has)243 298 y(a)c(\014xed)g(arit)o(y)g(that)f(is)i(a)f(tuple)h(of) f(t)o(yp)q(es)g(\()p Fp(\032)1020 305 y Fo(1)1039 298 y Fp(;)8 b(:)g(:)g(:)d(;)j(\032)1165 305 y Fi(k)1185 298 y Fx(\).)15 b(A)o(tomic)h(form)o(ulas)g(are)243 352 y(of)f(the)g(form)g Fp(P)6 b Fx(\()p Fp(r)556 330 y Fi(\032)574 335 y Fe(1)555 364 y Fo(1)593 352 y Fp(;)i(:)g(:)g(:)d(;)j(r)717 330 y Fi(\032)735 336 y Fd(k)716 366 y Fi(k)755 352 y Fx(\).)15 b(If)g Fp(P)22 b Fx(is)16 b(of)f(arit)o(y)g(\(\))g(then)g (the)h(atomic)f(form)o(ula)243 406 y Fp(P)6 b Fx(\(\))15 b(will)i(b)q(e)f(written)f(simply)h Fp(P)6 b Fx(.)301 460 y(The)13 b(c)o(hoice)g(of)f(the)h(predicate)h(sym)o(b)q(ols)f(dep)q (ends)h(on)e(the)h(particular)g(prob-)243 514 y(lem)h(in)h (consideration.)f(In)h(most)e(cases)h(there)g(will)h(b)q(e)g(the)e (predicate)i(sym)o(b)q(ols)243 568 y Fl(?)f Fx(\(falsit)o(y\))g(of)f (arit)o(y)h(\(\))f(and)h Fg(atom)f Fx(of)h(arit)o(y)g(\()p Fg(b)q(o)q(ole)p Fx(\).)f(The)h(in)o(tended)i(in)o(terpre-)243 622 y(tation)i(of)h Fg(atom)f Fx(is)h(the)g(set)g Fl(f)p Fg(true)p Fl(g)p Fx(.)g(Hence)g(`)p Fg(atom)o Fx(\()p Fp(t)p Fx(\)')f(means)h(`)p Fp(t)g Fx(=)g Fg(true)q Fx('.)f(If)243 676 y(confusion)e(is)f(unlik)o(ely)l(,)j(w)o(e)d(will)i(write)e Fp(t)g Fx(instead)h(of)f Fg(atom)o Fx(\()p Fp(t)p Fx(\).)243 756 y Fj(F)m(ormulas.)45 b Fp(P)515 763 y Fi(t)530 756 y Fx(\()p Fp(r)570 734 y Fi(\032)588 739 y Fe(1)569 768 y Fo(1)607 756 y Fp(;)8 b(:)g(:)g(:)t(;)g(r)730 734 y Fi(\032)748 740 y Fd(k)729 770 y Fi(k)769 756 y Fx(\))k Fl(j)g Fp(A)e Fl(^)h Fp(B)k Fl(j)d Fp(A)h Fl(!)g Fp(B)j Fl(j)c(8)p Fp(x)1214 740 y Fi(\032)1234 756 y Fp(A)h Fl(j)f(9)1331 740 y Fh(\003)1351 756 y Fp(x)1377 740 y Fi(\032)1397 756 y Fp(A)p Fx(.)243 810 y(A)20 b(form)o(ula)g(not)g (con)o(taining)h Fl(9)806 794 y Fh(\003)846 810 y Fx(is)f(called)i Fj(ne)n(gative)d Fx(or)h Fj(classic)n(al)p Fx(.)e Fj(Ne)n(gation)243 864 y Fx(and)d(the)g Fj(classic)n(al)g(existential)g(quanti\014er)g Fx(are)g(de\014ned)i(b)o(y)790 961 y Fl(:)p Fp(A)26 b Fx(:=)e Fp(A)13 b Fl(!)g(?)762 1027 y(9)p Fp(x)8 b(A)25 b Fx(:=)f Fl(:8)p Fp(x)8 b Fl(:)p Fp(A:)243 1151 y Fj(Axioms)16 b(for)g(b)n(o)n(ole)n(an)f(and)i(natur)n(al)f(induction.)408 1248 y Fg(Ind)467 1257 y Fh(8)p Fi(p)t(A)p Fo(\()p Fi(p)p Fo(\))584 1248 y Fx(:)50 b Fp(A)p Fx(\()p Fg(true)p Fx(\))12 b Fl(!)h Fp(A)p Fx(\()p Fg(false)p Fx(\))g Fl(!)g(8)p Fp(pA)p Fx(\()p Fp(p)p Fx(\))400 1314 y Fg(Ind)460 1324 y Fh(8)p Fi(n)5 b(A)p Fo(\()p Fi(n)p Fo(\))584 1314 y Fx(:)50 b Fp(A)p Fx(\(0\))11 b Fl(!)i(8)p Fp(n)p Fx(\()p Fp(A)p Fx(\()p Fp(n)p Fx(\))g Fl(!)g Fp(A)p Fx(\()p Fp(n)d Fx(+)h(1\)\))g Fl(!)j(8)p Fp(n)8 b(A)p Fx(\()p Fp(n)p Fx(\))p Fp(:)243 1464 y Fx(Axioms)15 b(for)g(the)g(constructiv)o(e)g Fl(9)835 1448 y Fh(\003)855 1464 y Fx(.)525 1561 y Fl(9)550 1542 y Fh(\003)p Fo(+)550 1577 y Fi(x;A)p Fo(\()p Fi(x)p Fo(\))656 1561 y Fx(:)65 b Fl(8)p Fp(x)8 b(:)g(A)p Fx(\()p Fp(x)p Fx(\))j Fl(!)i(9)1004 1542 y Fh(\003)1024 1561 y Fp(x)8 b(A)p Fx(\()p Fp(x)p Fx(\))487 1641 y Fl(9)512 1622 y Fh(\003\000)512 1657 y Fi(x;A)p Fo(\()p Fi(x)p Fo(\))p Fi(;B)656 1641 y Fx(:)50 b Fl(9)744 1622 y Fh(\003)764 1641 y Fp(x)790 1622 y Fi(\032)810 1641 y Fp(A)p Fx(\()p Fp(x)p Fx(\))12 b Fl(!)h(8)p Fp(x)1027 1622 y Fi(\032)1047 1641 y Fx(\()p Fp(A)p Fx(\()p Fp(x)p Fx(\))f Fl(!)h Fp(B)r Fx(\))g Fl(!)g Fp(B)243 1744 y Fx(with)i(the)h(usual)g(pro)o(viso)e (that)h Fp(x)g Fx(is)h(not)f(free)g(in)h Fp(B)r Fx(.)243 1851 y Fj(Pr)n(e)n(dic)n(ate-axioms.)26 b Fx(Usually)14 b(one)g(will)h(p)q(ostulate)e(axioms)h(for)e(describing)j(the)243 1905 y(in)o(tended)h(in)o(terpretation)g(of)f(the)g(predicate)h(sym)o (b)q(ols.)f(F)l(or)g(example)494 2002 y Fg(Ax)545 2009 y Fh(>)574 2002 y Fx(:)50 b Fg(atom)o Fx(\()p Fg(true)p Fx(\))136 b(\(truth)15 b(axiom\))494 2068 y Fg(Ax)545 2075 y Fh(?)574 2068 y Fx(:)50 b Fl(?)13 b($)g Fg(atom)o Fx(\()p Fg(false)p Fx(\))136 b(\(falsit)o(y)15 b(axiom\))243 2165 y(In)k(most)e(cases)i(the)f(in)o(tended)i(in)o(terpretation)f(of)f (a)g(predicate)h(sym)o(b)q(ol)g Fp(P)25 b Fx(is)243 2219 y(a)15 b(decidable)j(relation)e(with)g(a)g(decision)h(pro)q(cedure)g (represen)o(ted)f(b)o(y)f(a)h(closed)243 2273 y(term)f Fp(t)p Fx(:)8 b Fp(\032)413 2280 y Fo(1)445 2273 y Fl(!)13 b Fp(:)8 b(:)g(:)j Fl(!)j Fp(\032)652 2280 y Fi(k)686 2273 y Fl(!)f Fg(b)q(o)q(ole)q Fx(,)i(where)h(\()p Fp(\032)1049 2280 y Fo(1)1068 2273 y Fp(;)8 b(:)g(:)g(:)d(;)j(\032)1194 2280 y Fi(k)1214 2273 y Fx(\))15 b(is)h(the)f(arit)o(y)g(of)g Fp(P)6 b Fx(.)16 b(In)243 2327 y(that)e(case)h(w)o(e)g(include)j(the)d (axiom)414 2424 y Fg(Ax)465 2431 y Fi(P)495 2424 y Fx(:)49 b Fl(8)o Fp(~)-22 b(x)8 b(:)g(P)e Fx(\()o Fp(~)-22 b(x)o Fx(\))13 b Fl($)g Fg(atom)o Fx(\()p Fp(t)o(~)-22 b(x)p Fx(\))52 b(\(c)o(haracteristic)16 b(axiom\))912 2924 y Fm(finaljar2)o(.te)o(x;)g(29/01/2001)o(;)g(14:37;)i(p.4)p eop pstopssaved restore %%Page: pstops 3 /pstopssaved save def pstopsmatrix setmatrix 708.661417 0.000000 translate 90 rotate 0.880000 dup scale /pstopsmatrix matrix currentmatrix def initclip pstopsxform concat /showpage{}def/copypage{}def/erasepage{}def 5 4 bop 772 50 a Fo(W)m(arshall)10 b(and)g(Dic)o(kson)505 b Fx(5)243 145 y(and)15 b(w)o(e)g(call)h Fp(P)22 b Fj(de)n(cidable)p Fx(.)301 199 y(F)l(or)16 b(reasons)g(to)f(b)q(e)i(explained)i(later)d (w)o(e)g(require)h(that)f(the)g(predicate)i(ax-)243 253 y(ioms)12 b(are)f(negativ)o(e)h(form)o(ulas,)f(i.e.)h(do)g(not)g(con)o (tain)g Fl(9)1178 237 y Fh(\003)1198 253 y Fx(.)f(Otherwise)i(there)f (is)h(no)243 307 y(restriction,)i(except,)h(of)e(course,)h(that)g(they) g(should)i(b)q(e)e(true)h(in)g(the)f(in)o(tended)243 361 y(mo)q(del.)243 440 y Fj(Derivations)20 b Fx(are)c(form)o(ulated)g (in)h(a)f(natural)g(deduction)i(calculus)g(written)e(as)243 494 y(Curry-Ho)o(w)o(ard)e(t)o(yp)q(ed)h(lam)o(b)q(da-terms.)659 590 y Fp(u)685 571 y Fi(B)761 590 y Fx(\(assumptions\))d Fl(j)g Fx(axioms)h Fl(j)659 657 y Fx(\()p Fp(\025u)730 638 y Fi(A)766 657 y Fp(d)790 638 y Fi(B)820 657 y Fx(\))838 638 y Fi(A)p Fh(!)p Fi(B)942 657 y Fl(j)f Fx(\()p Fp(d)1009 638 y Fi(A)p Fh(!)p Fi(B)1101 657 y Fp(e)1122 638 y Fi(A)1150 657 y Fx(\))1168 638 y Fi(B)1211 657 y Fl(j)659 723 y(h)p Fp(d)701 704 y Fi(A)729 723 y Fp(;)c(e)771 704 y Fi(B)801 723 y Fl(i)819 704 y Fi(A)p Fh(^)p Fi(B)911 723 y Fl(j)13 b Fp(\031)963 730 y Fi(i)977 723 y Fx(\()p Fp(d)1019 704 y Fi(A)1045 709 y Fe(0)1062 704 y Fh(^)p Fi(A)1112 709 y Fe(1)1131 723 y Fx(\))1149 704 y Fi(A)1175 709 y Fd(i)1203 723 y Fl(j)659 795 y Fx(\()p Fp(\025x)730 776 y Fi(\032)750 795 y Fp(d)774 776 y Fi(A)802 795 y Fx(\))820 776 y Fh(8)p Fi(x)861 764 y Fd(\032)883 776 y Fi(A)924 795 y Fl(j)f Fx(\()p Fp(d)991 776 y Fh(8)p Fi(x)1032 764 y Fd(\032)1054 776 y Fi(A)1082 795 y Fp(t)1098 776 y Fi(\032)1119 795 y Fx(\))1137 776 y Fi(A)p Fo([)p Fi(t)1186 764 y Fd(\032)1204 776 y Fi(=x)1242 764 y Fd(\032)1259 776 y Fo(])243 891 y Fx(where)i(in)g(the)g Fl(8)p Fx(-in)o(tro)q (duction)h Fp(\025xd)877 874 y Fi(A)918 891 y Fp(x)e Fx(m)o(ust)g(not)h(b)q(e)g(free)f(in)i(an)o(y)e Fp(B)j Fx(with)e Fp(u)1607 874 y Fi(B)243 944 y Fx(a)h(free)g(assumption)g(v)m (ariable)i(in)f Fp(d)p Fx(.)301 998 y(A)h(deriv)m(ation)i(without)e (free)g(assumptions)g(is)h(called)h(a)e Fj(pr)n(o)n(of)p Fx(.)g(More)f(gen-)243 1052 y(erally)l(,)f(a)f(deriv)m(ation)h Fp(d)f Fx(of)g(a)f(form)o(ula)h Fp(A)g Fx(using)h(only)g(assumptions)f (from)g(a)g(set)243 1106 y(of)h(form)o(ulas)f(\000)i(is)g(called)g(a)f Fj(pr)n(o)n(of)i(of)f Fp(A)g Fj(fr)n(om)h Fx(\000,)e(written)g(\000)e Fl(`)g Fp(d)8 b Fx(:)g Fp(A)p Fx(.)301 1186 y(It)17 b(is)h(easy)g(to)e (see)i(that)f(stabilit)o(y)l(,)h Fl(::)p Fp(A)f Fl(!)g Fp(A)p Fx(,)g(is)h(pro)o(v)m(able)g(for)f(all)h(nega-)243 1240 y(tiv)o(e)f(form)o(ulas)f Fp(A)p Fx(,)h(b)o(y)f(using)i(b)q(o)q (olean)g(induction)g(and)f(the)g(axioms)g Fg(Ax)1518 1247 y Fh(>)1564 1240 y Fx(and)243 1294 y Fg(Ax)294 1301 y Fh(?)324 1294 y Fx(.)f(Hence,)g(restricting)h(ourselv)o(es)g(to)f (negativ)o(e)g(form)o(ulas)g(\(whic)o(h)h(is)g(not)f(a)243 1348 y(restriction)f(from)g(a)g(classical)i(p)q(oin)o(t)e(of)g(view\))g (w)o(e)g(ha)o(v)o(e)g(full)i(classical)f(logic.)462 1511 y Fs(3.)36 b(F)l(rom)16 b(in)o(tuitionistic)21 b(pro)q(ofs)c(to)h (programs)243 1619 y Fx(W)l(e)d(no)o(w)g(describ)q(e)i(ho)o(w)d(from)h (a)g(pro)q(of)f(of)h(a)g(constructiv)o(e)h Fl(89)1346 1603 y Fh(\003)1366 1619 y Fx(-statemen)o(t)799 1715 y Fl(8)p Fp(x)p Fl(9)875 1696 y Fh(\003)895 1715 y Fp(y)10 b(B)r Fx(\()p Fp(x;)e(y)r Fx(\))p Fp(;)243 1811 y Fx(where)15 b Fp(B)r Fx(\()p Fp(x;)8 b(y)r Fx(\))15 b(is)g(negativ)o(e,)g(a)g (program)f Fp(t)i Fx(can)f(b)q(e)h(extracted)f(suc)o(h)g(that)830 1907 y Fl(8)p Fp(x)8 b(B)r Fx(\()p Fp(x;)g(tx)p Fx(\))243 2002 y(is)21 b(pro)o(v)m(able.)g(W)l(e)f(will)i(do)f(this)g(via)f (Kreisel's)i Fj(mo)n(di\014e)n(d)f(r)n(e)n(alizability)f(inter-)243 2056 y(pr)n(etation)d Fx(\(Kreisel,)h(1959\))d(whic)o(h)j(is)f(treated) g(extensiv)o(ely)h(in)g(the)f(literature)243 2110 y(\(T)l(ro)q(elstra,) i(1973\),)f(\(T)l(ro)q(elstra)h(and)h(v)m(an)g(Dalen,)g(1988\),)e (\(see)i(also)g(Berger,)243 2164 y(1993,)13 b(Berger)j(and)f(Sc)o(h)o (wic)o(h)o(ten)o(b)q(erg,)g(1995\).)243 2273 y(3.1.)30 b Fr(Pr)o(ogram)18 b(extra)o(ction)243 2370 y Fx(The)e(extraction)f(op) q(eration)h(maps)g(ev)o(ery)f(deriv)m(ation)i Fp(d)f Fx(of)f(a)h(form)o(ula)f Fp(A)h Fx(to)f(a)243 2424 y(term)f([)-8 b([)p Fp(d)p Fx(])g(])13 b(`realizing)i Fp(A)p Fx('.)f(The)h(term)e([) -8 b([)p Fp(d)p Fx(])g(])14 b(is)g(the)h(program)e(extracted)h(from)f (the)912 2924 y Fm(finaljar2)o(.te)o(x;)j(29/01/2001)o(;)g(14:37;)i (p.5)p eop pstopssaved restore /pstopssaved save def pstopsmatrix setmatrix 708.661417 368.503937 translate 90 rotate 0.880000 dup scale /pstopsmatrix matrix currentmatrix def initclip pstopsxform concat 6 5 bop 243 50 a Fx(6)243 145 y(deriv)m(ation)19 b Fp(d)p Fx(.)f(In)g(particular,)h(if)f Fp(A)g Fx(is)h(the)f(form)o(ula)g Fl(8)p Fp(x)p Fl(9)1271 129 y Fh(\003)1291 145 y Fp(y)9 b(B)r Fx(\()p Fp(x;)f(y)r Fx(\),)17 b Fp(B)r Fx(\()p Fp(x;)8 b(y)r Fx(\))243 199 y(negativ)o(e,)13 b(then)h(`[)-8 b([)p Fp(d)p Fx(])g(])13 b(realizes)i Fp(A)p Fx(')e(will)j(mean)e Fl(8)p Fp(x)8 b(B)r Fx(\()p Fp(x;)g Fx([)-8 b([)p Fp(d)p Fx(])g(])p Fp(x)p Fx(\))12 b(i.e.)i([)-8 b([)p Fp(d)p Fx(])g(])12 b(correctly)243 253 y(meets)j(the)g(sp)q(eci\014cation)i Fp(A)p Fx(.)301 342 y(W)l(e)g(assign)g(to)g(ev)o(ery)f(form)o(ula)h Fp(A)g Fx(an)g(ob)s(ject)g Fp(\034)5 b Fx(\()p Fp(A)p Fx(\))16 b(that)g(is)i(either)g(a)e(t)o(yp)q(e)243 396 y(or)e(the)i(sym)o(b)q(ol)f Fl(\003)p Fx(.)g(Then)h Fp(\034)5 b Fx(\()p Fp(A)p Fx(\))14 b(will)j(b)q(e)f(the)f(t)o(yp)q(e)h(of)e(the) i(program)e(extracted)243 450 y(from)g(a)h(pro)q(of)g(of)g Fp(A)g Fx(\(pro)o(vided)h Fp(\034)5 b Fx(\()p Fp(A)p Fx(\))12 b Fl(6)p Fx(=)h Fl(\003)p Fx(\).)514 555 y Fp(\034)5 b Fx(\()p Fp(P)h Fx(\()n Fp(~)-21 b(s)p Fx(\)\))24 b(:=)h Fl(\003)481 648 y Fp(\034)5 b Fx(\()p Fl(9)549 629 y Fh(\003)568 648 y Fp(x)594 629 y Fi(\032)614 648 y Fp(A)p Fx(\))25 b(:=)764 588 y Fc(\032)808 620 y Fp(\032)174 b Fx(if)16 b Fp(\034)5 b Fx(\()p Fp(A)p Fx(\))12 b(=)h Fl(\003)p Fp(;)808 674 y(\032)c Fl(\002)i Fp(\034)5 b Fx(\()p Fp(A)p Fx(\))24 b(otherwise.)500 772 y Fp(\034)5 b Fx(\()p Fl(8)p Fp(x)594 754 y Fi(\032)614 772 y Fp(A)p Fx(\))25 b(:=)764 713 y Fc(\032)808 745 y Fl(\003)190 b Fx(if)16 b Fp(\034)5 b Fx(\()p Fp(A)p Fx(\))12 b(=)h Fl(\003)p Fp(;)808 799 y(\032)f Fl(!)h Fp(\034)5 b Fx(\()p Fp(A)p Fx(\))24 b(otherwise.)448 897 y Fp(\034)5 b Fx(\()p Fp(A)525 904 y Fo(0)554 897 y Fl(^)11 b Fp(A)629 904 y Fo(1)648 897 y Fx(\))25 b(:=)764 837 y Fc(\032)808 869 y Fp(\034)5 b Fx(\()p Fp(A)885 876 y Fi(i)898 869 y Fx(\))200 b(if)16 b Fp(\034)5 b Fx(\()p Fp(A)1235 876 y Fo(1)p Fh(\000)p Fi(i)1294 869 y Fx(\))12 b(=)h Fl(\003)p Fp(;)808 923 y(\034)5 b Fx(\()p Fp(A)885 930 y Fo(0)904 923 y Fx(\))10 b Fl(\002)g Fp(\034)5 b Fx(\()p Fp(A)1054 930 y Fo(1)1074 923 y Fx(\))24 b(otherwise.)464 1048 y Fp(\034)5 b Fx(\()p Fp(A)13 b Fl(!)g Fp(B)r Fx(\))25 b(:=)764 962 y Fc(8)764 1000 y(<)764 1074 y(:)813 994 y Fp(\034)5 b Fx(\()p Fp(B)r Fx(\))191 b(if)15 b Fp(\034)5 b Fx(\()p Fp(A)p Fx(\))12 b(=)h Fl(\003)p Fp(;)813 1048 y Fl(\003)265 b Fx(if)15 b Fp(\034)5 b Fx(\()p Fp(B)r Fx(\))13 b(=)g Fl(\003)p Fp(;)813 1102 y(\034)5 b Fx(\()p Fp(A)p Fx(\))12 b Fl(!)h Fp(\034)5 b Fx(\()p Fp(B)r Fx(\))26 b(otherwise.)243 1207 y(A)15 b(form)o(ula)f(is)h(called)i Fj(c)n(omputational)r(ly)f(me)n(aningful)e Fx(if)h Fp(\034)5 b Fx(\()p Fp(A)p Fx(\))13 b Fl(6)p Fx(=)g Fl(\003)p Fx(.)h(Otherwise) 243 1261 y(it)h(is)g(called)i(a)d Fj(Harr)n(op-formula)p Fx(.)i(Note)f(that)f(negativ)o(e)h(form)o(ulas)f(are)h(Harrop-)243 1315 y(form)o(ulas.)301 1404 y(Next)d(for)f(ev)o(ery)h(deriv)m(ation)i Fp(d)d Fx(of)h(a)g(computationally)g(meaningful)i(form)o(ula)243 1458 y Fp(A)i Fx(w)o(e)f(de\014ne)i(the)g Fj(extr)n(acte)n(d)f(pr)n(o)n (gr)n(am)h Fx([)-8 b([)p Fp(d)p Fx(])g(]:)8 b Fp(\034)d Fx(\()p Fp(A)p Fx(\).)13 b(F)l(or)i(assumption)h(v)m(ariables)243 1522 y Fp(u)269 1505 y Fi(A)310 1522 y Fx(w)o(e)d(set)g([)-8 b([)p Fp(u)488 1505 y Fi(A)516 1522 y Fx(])g(])12 b(:=)h Fp(x)633 1498 y Fi(\034)t Fo(\()p Fi(A)p Fo(\))633 1527 y Fi(u)708 1522 y Fx(,)g(where)g Fp(x)889 1498 y Fi(\034)t Fo(\()p Fi(A)p Fo(\))889 1527 y Fi(u)977 1522 y Fx(is)h(some)f(ob)s (ject)f(v)m(ariable)i(asso)q(ciated)243 1576 y(with)h(the)h(assumption) f(v)m(ariable)i Fp(u)862 1559 y Fi(A)905 1576 y Fx(in)f(a)f(one)g(to)g (one)g(w)o(a)o(y)l(,)f(and)i(inductiv)o(ely)582 1714 y([)-8 b([)p Fp(\025u)653 1695 y Fi(A)681 1714 y Fp(d)p Fx(])g(])24 b(:=)820 1642 y Fc(\()866 1680 y Fx([)-8 b([)p Fp(d)p Fx(])g(])152 b(if)16 b Fp(\034)5 b Fx(\()p Fp(A)p Fx(\))12 b(=)h Fl(\003)p Fp(;)866 1745 y(\025x)919 1722 y Fi(\034)t Fo(\()p Fi(A)p Fo(\))919 1751 y Fi(u)994 1745 y Fx([)-8 b([)p Fp(d)p Fx(])g(])24 b(otherwise.)550 1862 y([)-8 b([)p Fp(d)592 1843 y Fi(A)p Fh(!)p Fi(B)684 1862 y Fp(e)p Fx(])g(])24 b(:=)820 1802 y Fc(\032)864 1834 y Fx([)-8 b([)p Fp(d)p Fx(])g(])80 b(if)16 b Fp(\034)5 b Fx(\()p Fp(A)p Fx(\))12 b(=)h Fl(\003)p Fp(;)864 1888 y Fx([)-8 b([)p Fp(d)p Fx(])g(][)g([)p Fp(e)p Fx(])g(])23 b(otherwise.)493 2010 y([)-8 b([)p Fl(h)p Fp(d)553 1990 y Fi(A)579 1995 y Fe(0)553 2023 y Fo(0)597 2010 y Fp(;)8 b(d)642 1990 y Fi(A)668 1995 y Fe(1)642 2023 y Fo(1)687 2010 y Fl(i)p Fx(])-8 b(])24 b(:=)820 1951 y Fc(\032)864 1983 y Fx([)-8 b([)p Fp(d)906 1990 y Fi(i)919 1983 y Fx(])g(])165 b(if)15 b Fp(\034)5 b Fx(\()p Fp(A)1220 1990 y Fo(1)p Fh(\000)p Fi(i)1279 1983 y Fx(\))13 b(=)g Fl(\003)864 2037 y(h)p Fx([)-8 b([)p Fp(d)924 2044 y Fo(0)943 2037 y Fx(])g(])p Fp(;)8 b Fx([)-8 b([)p Fp(d)1024 2044 y Fo(1)1041 2037 y Fx(])g(])p Fl(i)25 b Fx(otherwise.)475 2159 y([)-8 b([)p Fp(\031)519 2166 y Fi(i)533 2159 y Fx(\()p Fp(d)575 2140 y Fi(A)601 2145 y Fe(0)618 2140 y Fh(^)p Fi(A)668 2145 y Fe(1)687 2159 y Fx(\)])g(])24 b(:=)820 2099 y Fc(\032)864 2131 y Fx([)-8 b([)p Fp(d)p Fx(])g(])64 b(if)15 b Fp(\034)5 b Fx(\()p Fp(A)1106 2138 y Fo(1)p Fh(\000)p Fi(i)1165 2131 y Fx(\))13 b(=)g Fl(\003)864 2185 y Fp(\031)890 2192 y Fi(i)904 2185 y Fx([)-8 b([)p Fp(d)p Fx(])g(])24 b(otherwise.)591 2291 y([)-8 b([)p Fp(\025x)662 2273 y Fi(\032)681 2291 y Fp(d)p Fx(])g(])24 b(:=)h Fp(\025x)873 2273 y Fi(\032)893 2291 y Fx([)-8 b([)p Fp(d)p Fx(])g(])p Fp(;)647 2424 y Fx([)g([)p Fp(dt)p Fx(])g(])24 b(:=)h([)-8 b([)p Fp(d)p Fx(])g(])p Fp(t:)912 2924 y Fm(finaljar2)o(.te)o(x;)16 b(29/01/2001)o(;)g(14:37;)i(p.6)p eop pstopssaved restore %%Page: pstops 4 /pstopssaved save def pstopsmatrix setmatrix 708.661417 0.000000 translate 90 rotate 0.880000 dup scale /pstopsmatrix matrix currentmatrix def initclip pstopsxform concat /showpage{}def/copypage{}def/erasepage{}def 7 6 bop 772 50 a Fo(W)m(arshall)10 b(and)g(Dic)o(kson)505 b Fx(7)243 145 y(The)13 b(axioms)g(are)g(realized)h(b)o(y)f(suitable)h (closed)g(terms.)e(F)l(or)h(induction)i(axioms)414 229 y Fg(Ind)473 239 y Fh(8)p Fi(n)5 b(A)p Fo(\()p Fi(n)p Fo(\))598 229 y Fx(:)j Fp(A)p Fx(\(0\))j Fl(!)i Fx(\()p Fl(8)p Fp(n)8 b(:)g(A)p Fx(\()p Fp(n)p Fx(\))j Fl(!)i Fp(A)p Fx(\()p Fp(n)d Fx(+)h(1\)\))h Fl(!)h(8)p Fp(n)8 b(A)p Fx(\()p Fp(n)p Fx(\))243 314 y(the)15 b(realizing)i(program)d([) -8 b([)p Fg(Ind)762 323 y Fh(8)p Fi(n)5 b(A)p Fo(\()p Fi(n)p Fo(\))887 314 y Fx(])-8 b(])14 b(is)i(the)f(recursor)567 398 y Fg(R)596 405 y Ff(nat)p Fi(;\032)674 398 y Fx(:)8 b Fp(\032)j Fl(!)j Fx(\()p Fg(nat)f Fl(!)g Fp(\032)f Fl(!)h Fp(\032)p Fx(\))f Fl(!)h Fg(nat)g Fl(!)g Fp(\032;)243 482 y Fx(where)i Fp(\032)e Fx(=)g Fp(\034)5 b Fx(\()p Fp(A)p Fx(\()p Fp(n)p Fx(\)\).)14 b(Similarly)k(b)q(o)q(olean)e (induction)i(is)e(realized)h(b)o(y)e Fg(R)1515 489 y Ff(b)q(o)q(ole)p Fi(;\032)1625 482 y Fx(.)243 536 y(F)l(or)f(the)i Fl(9)428 519 y Fh(\003)448 536 y Fx(-axioms)f(w)o(e)g(set)356 644 y([)-8 b([)p Fl(9)399 624 y Fh(\003)p Fo(+)399 657 y Fi(x)419 648 y Fd(\032)437 657 y Fi(;A)475 644 y Fx(])g(])25 b(:=)590 572 y Fc(\()636 614 y Fp(\025x)689 598 y Fi(\032)709 614 y Fp(x)230 b Fx(if)16 b Fp(\034)5 b Fx(\()p Fp(A)p Fx(\))12 b(=)h Fl(\003)p Fp(;)636 672 y(\025x)689 655 y Fi(\032)709 672 y Fp(\025y)760 655 y Fi(\034)t Fo(\()p Fi(A)p Fo(\))835 672 y Fl(h)p Fp(x;)8 b(y)r Fl(i)23 b Fx(otherwise.)271 822 y([)-8 b([)p Fl(9)314 803 y Fh(\003\000)314 838 y Fi(x)334 829 y Fd(\032)351 838 y Fi(;A)p Fo(\()p Fi(x)p Fo(\))p Fi(;B)475 822 y Fx(])g(])25 b(:=)590 750 y Fc(\()636 795 y Fp(\025x)689 778 y Fi(\032)709 795 y Fp(\025f)763 778 y Fi(\032)p Fh(!)p Fi(\034)t Fo(\()p Fi(B)r Fo(\))893 795 y Fp(f)5 b(x)414 b Fx(if)16 b Fp(\034)5 b Fx(\()p Fp(A)p Fx(\))12 b(=)h Fl(\003)p Fp(;)636 852 y(\025z)686 836 y Fi(\032)p Fh(\002)p Fi(\034)t Fo(\()p Fi(A)p Fo(\))807 852 y Fp(\025f)861 836 y Fi(\032)p Fh(!)p Fi(\034)t Fo(\()p Fi(A)p Fo(\))p Fh(!)p Fi(\034)t Fo(\()p Fi(B)r Fo(\))1100 852 y Fp(f)5 b(\031)1153 859 y Fo(0)1173 852 y Fx(\()p Fp(z)r Fx(\))p Fp(\031)1258 859 y Fo(1)1277 852 y Fx(\()p Fp(z)r Fx(\))24 b(otherwise.)243 946 y(It)15 b(is)g(con)o(v)o(enien)o(t)g(to)f(extend)i(the)f(de\014nition)h(of)e([) -8 b([)p Fp(d)p Fx(])g(])14 b(to)g(deriv)m(ations)i Fp(d)1478 930 y Fi(A)1521 946 y Fx(where)243 1000 y Fp(A)22 b Fx(is)g(a)g (Harrop-form)o(ula,)e(b)o(y)i(setting)g(in)h(this)f(case)g([)-8 b([)p Fp(d)p Fx(])g(])23 b(:=)h Fp(\017)p Fx(,)e(where)g Fp(\017)g Fx(is)243 1054 y(some)13 b(new)g(sym)o(b)q(ol.)g(This)g (applies)i(in)f(particular)g(if)f Fp(A)g Fx(is)h(negativ)o(e.)e(Hence)i (the)243 1108 y(extracted)h(program)f(of)g(a)h(predicate)h(axiom)g(is)f Fp(\017)p Fx(.)243 1183 y Fj(Example.)42 b Fx(It)21 b(is)g(easy)g(to)g (see)g(that)f(for)h(ev)o(ery)g(quan)o(ti\014er)g(free)g(form)o(ula)g Fp(C)243 1237 y Fx(con)o(taining)e(only)g(decidable)i(predicate)f(sym)o (b)q(ols,)e(there)h(is)g(a)f(term)h Fp(t)1502 1244 y Fi(C)1550 1237 y Fx(suc)o(h)243 1291 y(that)d Fp(C)i Fl($)e Fp(t)471 1298 y Fi(C)518 1291 y Fx(is)i(pro)o(v)m(able.)f (Therefore)g(for)f(suc)o(h)i Fp(C)h Fx(w)o(e)e(can)g(easily)h(deriv)o (e)g(a)243 1345 y(sc)o(heme)d(of)g(pro)q(of)g(b)o(y)g(cases)574 1429 y(Cases)686 1436 y Fi(C)716 1429 y Fx(:)8 b(\()p Fp(C)14 b Fl(!)f Fp(A)p Fx(\))f Fl(!)h Fx(\()p Fl(:)p Fp(C)j Fl(!)d Fp(A)p Fx(\))f Fl(!)h Fp(A:)243 1513 y Fx(The)i(pro)q(of)g(term)g(is)365 1597 y Fp(\025u)418 1578 y Fi(C)r Fh(!)p Fi(A)418 1608 y Fo(1)509 1597 y Fp(\025u)562 1578 y Fh(:)p Fi(C)r Fh(!)p Fi(A)562 1608 y Fo(2)676 1597 y Fp(:)50 b Fg(Ind)798 1606 y Fh(8)p Fi(p)t(:)6 b Fo(\()p Fi(p)p Fh(!)p Fi(C)r Fo(\))p Fh(!)p Fo(\()p Fi(C)r Fh(!)p Fi(p)p Fo(\))p Fh(!)p Fi(A)739 1673 y Fx(\()p Fp(\025u)810 1654 y Ff(true)o Fh(!)p Fi(C)810 1684 y Fo(3)932 1673 y Fp(\025u)985 1654 y Fi(C)r Fh(!)p Ff(true)985 1684 y Fo(4)1108 1673 y Fp(:)i(u)1155 1680 y Fo(1)1174 1673 y Fx(\()p Fp(u)1218 1680 y Fo(3)1238 1673 y Fg(Ax)1289 1680 y Fh(>)1319 1673 y Fx(\)\))739 1739 y(\()p Fp(\025u)810 1720 y Ff(false)n Fh(!)p Fi(C)810 1750 y Fo(5)939 1739 y Fp(\025u)992 1720 y Fi(C)r Fh(!)p Ff(false)992 1750 y Fo(6)1122 1739 y Fp(:)g(u)1169 1746 y Fo(2)1188 1739 y Fp(\025u)1241 1720 y Fi(C)1241 1750 y Fo(7)1270 1739 y Fp(:)g Fg(Ax)1341 1746 y Fh(?)1371 1739 y Fx(\()p Fp(u)1415 1746 y Fo(6)1434 1739 y Fp(u)1460 1746 y Fo(7)1480 1739 y Fx(\)\))739 1805 y Fp(t)755 1812 y Fi(C)739 1872 y Fp(d)763 1851 y Fi(t)776 1857 y Fd(C)801 1851 y Fh(!)p Fi(C)763 1884 y Fo(1)739 1945 y Fp(d)763 1923 y Fi(C)r Fh(!)p Fi(t)838 1929 y Fd(C)763 1957 y Fo(2)243 2029 y Fx(with)15 b(extracted)g(program)399 2113 y Fp(\025x)452 2091 y Fi(\032)452 2125 y Fo(1)471 2113 y Fp(\025x)524 2091 y Fi(\032)524 2125 y Fo(2)544 2113 y Fp(:)8 b Fg(R)594 2120 y Ff(b)q(o)q(ole)o Fi(;\032)703 2113 y Fp(x)729 2120 y Fo(1)749 2113 y Fp(x)775 2120 y Fo(2)794 2113 y Fp(t)810 2120 y Fi(C)853 2113 y Fx(=)13 b Fp(\025x)954 2120 y Fo(1)973 2113 y Fp(\025x)1026 2120 y Fo(2)1053 2113 y Fp(:)8 b Fg(if)17 b Fp(t)1132 2120 y Fi(C)1177 2113 y Fg(then)g Fp(x)1302 2120 y Fo(1)1337 2113 y Fg(else)f Fp(x)1447 2120 y Fo(2)243 2197 y Fx(of)f(t)o(yp)q(e)g Fp(\032)d Fl(!)h Fp(\032)f Fl(!)h Fp(\032)p Fx(,)i(where)g Fp(\032)d Fx(:=)h Fp(\034)5 b Fx(\()p Fp(A)p Fx(\).)912 2924 y Fm(finaljar2)o(.te)o(x;)16 b(29/01/2001)o(;)g(14:37;)i(p.7)p eop pstopssaved restore /pstopssaved save def pstopsmatrix setmatrix 708.661417 368.503937 translate 90 rotate 0.880000 dup scale /pstopsmatrix matrix currentmatrix def initclip pstopsxform concat 8 7 bop 243 50 a Fx(8)243 145 y(3.2.)30 b Fr(Modified)18 b(realizability)243 248 y Fx(Correctness)12 b(of)g(the)h(extracted)f (programs)f(is)i(guaran)o(teed)f(b)o(y)h(the)g(w)o(ell-kno)o(wn)243 302 y(soundness)25 b(theorem)e(\(see)h(b)q(elo)o(w\))h(stating)e(that)h (the)g(extracted)g(program)243 356 y Fj(\(mo)n(di\014e)n(d\))15 b(r)n(e)n(alizes)e Fx(the)j(form)o(ula)e(deriv)o(ed.)301 441 y(W)l(e)j(de\014ne)h(form)o(ulas)f Fp(r)8 b Fs(mr)f Fp(A)p Fx(,)17 b(where)g Fp(A)g Fx(is)h(a)f(form)o(ula)f(and)i Fp(r)f Fx(is)h(either)g(a)243 495 y(term)c(of)h(t)o(yp)q(e)h Fp(\034)5 b Fx(\()p Fp(A)p Fx(\))14 b(if)i(the)f(latter)g(is)h(a)f(t)o (yp)q(e,)f(or)h(the)g(sym)o(b)q(ol)h Fp(\017)g Fx(if)f Fp(\034)5 b Fx(\()p Fp(A)p Fx(\))12 b(=)h Fl(\003)p Fx(.)379 595 y Fp(\017)8 b Fs(mr)f Fp(P)507 602 y Fi(t)522 595 y Fx(\()n Fp(~)-21 b(s)p Fx(\))24 b(:=)h Fp(P)705 602 y Fi(t)720 595 y Fx(\()n Fp(~)-21 b(s)p Fx(\))p Fp(;)364 731 y(r)8 b Fs(mr)f Fl(9)p Fp(x)517 714 y Fh(\003)544 731 y Fp(A)25 b Fx(:=)676 671 y Fc(\032)720 703 y Fp(\017)8 b Fs(mr)f Fp(A)p Fx([)p Fp(r)q(=x)p Fx(])189 b(if)15 b Fp(\034)5 b Fx(\()p Fp(A)p Fx(\))12 b(=)h Fl(\003)p Fp(;)720 757 y(\031)746 764 y Fo(1)765 757 y Fx(\()p Fp(r)q Fx(\))8 b Fs(mr)e Fp(A)p Fx([)p Fp(\031)976 764 y Fo(0)995 757 y Fx(\()p Fp(r)q Fx(\))p Fp(=x)p Fx(])24 b(otherwise.)391 893 y Fp(r)8 b Fs(mr)f Fl(8)p Fp(xA)25 b Fx(:=)676 833 y Fc(\032)720 865 y Fl(8)p Fp(x:\017)8 b Fs(mr)e Fp(A)67 b Fx(if)16 b Fp(\034)5 b Fx(\()p Fp(A)p Fx(\))12 b(=)h Fl(\003)p Fp(;)720 919 y Fl(8)p Fp(x:r)q(x)8 b Fs(mr)e Fp(A;)24 b Fx(otherwise.)283 1055 y Fp(r)8 b Fs(mr)f Fx(\()p Fp(A)437 1062 y Fo(0)467 1055 y Fl(^)j Fp(A)541 1062 y Fo(1)561 1055 y Fx(\))24 b(:=)676 995 y Fc(\032)720 1027 y Fp(r)8 b Fs(mr)f Fp(A)856 1034 y Fo(1)p Fh(\000)p Fi(i)925 1027 y Fl(^)26 b Fp(\017)8 b Fs(mr)e Fp(A)1113 1034 y Fi(i)1269 1027 y Fx(if)15 b Fp(\034)5 b Fx(\()p Fp(A)1387 1034 y Fi(i)1401 1027 y Fx(\))13 b(=)g Fl(\003)p Fp(;)720 1081 y(\031)746 1088 y Fo(0)765 1081 y Fx(\()p Fp(r)q Fx(\))8 b Fs(mr)e Fp(A)937 1088 y Fo(0)967 1081 y Fl(^)k Fp(\031)1033 1088 y Fo(1)1053 1081 y Fx(\()p Fp(r)q Fx(\))e Fs(mr)d Fp(A)1224 1088 y Fo(1)1269 1081 y Fx(otherwise.)300 1243 y Fp(r)j Fs(mr)f Fx(\()p Fp(A)12 b Fl(!)h Fp(B)r Fx(\))25 b(:=)676 1157 y Fc(8)676 1195 y(<)676 1269 y(:)726 1189 y Fp(\017)8 b Fs(mr)e Fp(A)13 b Fl(!)g Fp(r)8 b Fs(mr)f Fp(B)125 b Fx(if)16 b Fp(\034)5 b Fx(\()p Fp(A)p Fx(\))12 b(=)h Fl(\003)p Fp(;)726 1243 y Fl(8)p Fp(x:x)8 b Fs(mr)e Fp(A)12 b Fl(!)h Fp(\017)8 b Fs(mr)f Fp(B)57 b Fx(if)16 b Fp(\034)5 b Fx(\()p Fp(A)p Fx(\))12 b Fl(6)p Fx(=)h Fl(\003)f Fx(=)h Fp(\034)5 b Fx(\()p Fp(B)r Fx(\))p Fp(;)726 1297 y Fl(8)p Fp(x:x)j Fs(mr)e Fp(A)12 b Fl(!)h Fp(r)q(x)8 b Fs(mr)e Fp(B)28 b Fx(otherwise.)243 1427 y Fr(Soundness)19 b(Theorem.)36 b Fx(If)18 b Fp(d)g Fx(is)g(a)g(deriv)m(ation)h(of)e(a)h(form)o(ula)f Fp(B)r Fx(,)i(then)f(w)o(e)243 1481 y(can)h(deriv)o(e)h([)-8 b([)p Fp(d)p Fx(])g(])8 b Fs(mr)d Fp(B)22 b Fx(from)d(the)g (assumptions)g Fl(f)8 b Fp(x)1176 1488 y Fi(u)1206 1481 y Fs(mr)e Fp(C)22 b Fl(j)d Fp(u)1391 1464 y Fi(C)1440 1481 y Fl(2)h Fx(F)-5 b(A)o(\()p Fp(d)p Fx(\))8 b Fl(g)243 1535 y Fx(where)17 b Fp(x)402 1542 y Fi(u)441 1535 y Fx(:=)f Fp(\017)h Fx(if)h Fp(u)610 1518 y Fi(C)657 1535 y Fx(is)g(an)f(assumption)g(v)m(ariable)i(with)e(a)g(Harrop-form)o(ula) 243 1589 y Fp(C)s Fx(.)243 1673 y Fj(Pr)n(o)n(of)9 b Fx(.)28 b(Induction)15 b(on)f(the)g(structure)g(of)f Fp(d)p Fx(.)g(The)i(pro)q(of)e(can)h(b)q(e)h(found)f(in)h(an)o(y)243 1727 y(of)i(the)h(cited)g(literature)h(on)e(realizabilit)o(y;)j(see)e (for)f(instance)h(\(T)l(ro)q(elstra)f(and)243 1781 y(v)m(an)e(Dalen,)h (1988\).)301 1866 y(Clearly)d(if)g Fp(B)i Fx(is)e(negativ)o(e)g(then)g Fp(\017)8 b Fs(mr)f Fp(B)15 b Fx(=)e Fp(B)r Fx(.)g(\(Note)f(this)h (need)g(not)f(b)q(e)h(the)243 1920 y(case)18 b(for)f(arbitrary)h Fp(B)j Fx(with)d Fp(\034)5 b Fx(\()p Fp(B)r Fx(\))18 b(=)g Fl(\003)p Fx(.\))f(Hence)i(for)f(form)o(ulas)f(of)h(the)g(form) 243 1974 y Fl(8)p Fp(x)294 1957 y Fi(\032)314 1974 y Fl(9)339 1957 y Fh(\003)359 1974 y Fp(y)383 1957 y Fi(\033)406 1974 y Fp(B)r Fx(\()p Fp(x;)8 b(y)r Fx(\))15 b(with)g(negativ)o(e)g Fp(B)r Fx(\()p Fp(x;)8 b(y)r Fx(\))15 b(w)o(e)g(ha)o(v)o(e)f Fp(\034)5 b Fx(\()p Fl(8)p Fp(x)p Fl(9)p Fp(y)1318 1957 y Fh(\003)1338 1974 y Fp(A)p Fx(\()p Fp(x;)j(y)r Fx(\)\))j(=)i Fp(\032)f Fl(!)243 2028 y Fp(\033)17 b Fx(and)621 2090 y Fp(t)8 b Fs(mr)e Fl(8)p Fp(x)p Fl(9)793 2071 y Fh(\003)814 2090 y Fp(y)r(A)p Fx(\()p Fp(x;)i(y)r Fx(\))j(=)i Fl(8)p Fp(xA)p Fx(\()p Fp(x;)8 b(tx)p Fx(\))p Fp(:)301 2178 y Fx(Therefore)20 b(w)o(e)h(obtain)f(as)g(a)h(corollary)f(to)g(the)h (soundness)g(theorem)f(the)243 2232 y(follo)o(wing.)243 2316 y Fr(Extra)o(ction)11 b(Theorem.)21 b Fx(F)l(rom)9 b(a)h(pro)q(of)g Fp(d)g Fx(of)g Fl(8)p Fp(x)1155 2300 y Fi(\032)1176 2316 y Fl(9)p Fp(y)1225 2300 y Fi(\033)1248 2316 y Fp(B)r Fx(\()p Fp(x;)e(y)r Fx(\),)i Fp(B)j Fx(negativ)o(e,)243 2370 y(from)e(negativ)o(e)h(assumptions)g(\000)h(one)f(can)g(extract)f (a)h(closed)h(term)e([)-8 b([)p Fp(d)p Fx(])g(])1462 2354 y Fi(\032)p Fh(!)p Fi(\033)1550 2370 y Fx(suc)o(h)243 2424 y(that)14 b(the)i(form)o(ula)e Fl(8)p Fp(xB)r Fx(\()p Fp(x;)8 b Fx([)-8 b([)p Fp(d)p Fx(])g(])p Fp(x)p Fx(\))14 b(is)i(pro)o(v)m(able)g(from)e(\000.)912 2924 y Fm(finaljar2)o(.te)o (x;)i(29/01/2001)o(;)g(14:37;)i(p.8)p eop pstopssaved restore %%Page: pstops 5 /pstopssaved save def pstopsmatrix setmatrix 708.661417 0.000000 translate 90 rotate 0.880000 dup scale /pstopsmatrix matrix currentmatrix def initclip pstopsxform concat /showpage{}def/copypage{}def/erasepage{}def 9 8 bop 772 50 a Fo(W)m(arshall)10 b(and)g(Dic)o(kson)505 b Fx(9)301 145 y(Usually)18 b(\000)g(consists)g(of)f(lemmas,)g(i.e.)g (true)g(form)o(ulas)g(that)g(w)o(e)g(could)h(but)243 199 y(do)c(not)g(pro)o(v)o(e)f(in)i(order)f(to)f(k)o(eep)i(the)f(deriv) m(ation)h Fp(d)f Fx(short.)f(The)h(theorem)g(sa)o(ys)243 253 y(that)g(this)i(abbreviation)g(do)q(es)f(not)g(a\013ect)g(program)f (extraction.)628 409 y Fs(4.)37 b(The)18 b(W)l(arshall)g(algorithm)243 514 y Fx(The)f(W)l(arshall)g(algorithm)g(computes)g(the)g(transitiv)o (e)h(closure)f(of)g(a)f(relation;)243 568 y(its)11 b(complexit)o(y)i (is)f Fp(O)q Fx(\()p Fp(n)653 551 y Fo(3)673 568 y Fx(\),)e(whereas)i (the)f(naiv)o(e)h(algorithm)g(needs)g Fp(O)q Fx(\()p Fp(n)1477 551 y Fo(4)1497 568 y Fx(\))f(steps.)243 622 y(Using)h(the)f(extraction)g(metho)q(d)g(describ)q(ed)j(in)e(the)f (preceeding)i(section)f(w)o(e)f(will)243 675 y(obtain)i(this)g(`clev)o (er')g(algorithm)g(from)f(a)g(pro)q(of)h(that)f(uses)h(only)g(the)g (basic)h(idea)243 729 y(of)h(W)l(arshall's)g(algorithm,)g(i.e.)g(to)f (a)o(v)o(oid)h(rep)q(etitions)i(in)f(paths.)301 805 y(Besides)k Fg(nat)f Fx(w)o(e)f(will)i(use)f(an)f(additional)i(ground)e(t)o(yp)q(e) h Fg(nats)g Fx(for)f(lists)h(of)243 859 y(natural)13 b(n)o(um)o(b)q(ers)h(represen)o(ting)g(paths)f(with)h(natural)f(n)o(um) o(b)q(ers)h(as)f(elemen)o(ts.)243 913 y(It)i(will)h(b)q(e)g(useful)g (to)e(ha)o(v)o(e)h(an)g(error)f(ob)s(ject)h Fl(?)1076 897 y Ff(nats)1139 913 y Fx(,)g(since)h(a)f(natural)g(function)243 967 y(for)f(concatenation)i(of)f(t)o(w)o(o)e(paths)i(will)i(b)q(e)f (only)g(partially)g(de\014ned.)301 1021 y(Lists)h(^)-26 b Fp(x;)10 b Fx(^)-25 b Fp(y)q(;)10 b Fx(^)-25 b Fp(z)14 b Fx(are)f(generated)h(from)e(the)i(empt)o(y)f(list)h Fp(")f Fx(and)h(the)f(error)g(ob)s(ject)243 1075 y Fl(?)278 1059 y Ff(nats)354 1075 y Fx(b)o(y)g(means)f(of)601 1065 y Fh(\\)624 1075 y Fx(,)g(whic)o(h)i(constructs)e(a)g(list)i Fp(k)1126 1065 y Fh(\\)1152 1075 y Fx(^)-25 b Fp(x)12 b Fx(from)g(a)g(n)o(um)o(b)q(er)h Fp(k)h Fx(and)f(a)243 1129 y(list)19 b(^)-26 b Fp(x)p Fx(.)15 b Fp(x;)8 b(y)r(;)g(z)16 b Fx(\(without)f(hat)t(^)t(\))g(denote)h(lists)g Fl(6)p Fx(=)e Fl(?)1144 1112 y Ff(nats)1208 1129 y Fx(,)h Fp(i;)8 b(j;)g(k)q(;)g(l;)g(m)o(;)g(n)k Fx(natural)243 1183 y(n)o(um)o(b)q (ers.)301 1259 y(Our)g(language)h(consists)f(of)g(the)g(follo)o(wing)h (relation)g(and)f(function)h(sym)o(b)q(ols)243 1313 y(with)23 b(their)f(in)o(tended)i(meaning.)f(W)l(e)f(deal)i(with)e(a)g(binary)h (relation)g Fp(R)g Fx(on)243 1367 y Fl(f)p Fx(0)p Fp(;)8 b Fx(1)p Fp(;)g(:)g(:)f(:)t(;)h(n)p Fl(\000)p Fx(1)p Fl(g)p Fx(,)14 b(whose)h(transitiv)o(e)h(closure)f(is)h(to)f(b)q(e)h (determined.)611 1454 y Fp(k)e Fg(in)i Fx(^)-26 b Fp(x)p Fx(:)24 b Fp(k)16 b Fx(o)q(ccurs)g(in)g(the)f(path)j(^)-26 b Fp(x)p Fx(,)631 1507 y Fg(rf)o Fx(\()s(^)g Fp(x)p Fx(\):)27 b(^)-26 b Fp(x)15 b Fx(is)h(a)f(rep)q(etition)h(free)g(path,)533 1561 y Fp(P)562 1568 y Fi(i)576 1561 y Fx(\()s(^)-26 b Fp(x;)8 b(j;)g(k)q Fx(\):)25 b(^)-26 b Fp(x)15 b Fx(is)h(an)f Fp(R)p Fx(-path)g(from)g Fp(j)i Fx(to)e Fp(k)759 1615 y Fx(whose)g(inner)i(elemen)o(ts)e(are)g Fp(<)e(i)p Fx(,)642 1669 y(^)-26 b Fp(x)10 b Fl(\001)j Fx(^)-26 b Fp(y)r Fx(:)24 b(concatenation,)243 1755 y(where)18 b(the)h(concatenation)f (function)k(^)-25 b Fp(x)12 b Fl(\001)j Fx(^)-26 b Fp(y)20 b Fx(is)f(de\014ned)g(as)f(follo)o(ws.)g(If)k(^)-26 b Fp(x)18 b Fx(and)246 1809 y(^)-26 b Fp(y)19 b Fx(are)d(lists)i(with)f (the)g(same)g(end)g(and)g(initial)i(p)q(oin)o(t)f(resp)q(ectiv)o(ely)l (,)g(then)i(^)-25 b Fp(x)11 b Fl(\001)j Fx(^)-26 b Fp(y)243 1863 y Fx(is)15 b(the)g(list)g(obtained)h(b)o(y)f(concatenating)g(the)f (t)o(w)o(o,)g(where)h(the)f(same)h(end)g(and)243 1917 y(initial)20 b(p)q(oin)o(t)f(is)g(used)g(only)g(once.)g(If)f(end)h(and) g(initial)i(p)q(oin)o(ts)e(are)f(di\013eren)o(t,)243 1971 y(the)d(result)h(is)f(the)h(error)e(ob)s(ject)h Fl(?)856 1954 y Ff(nats)920 1971 y Fx(.)301 2025 y(In)j(the)g(formal)f (pro)q(ofs)h(w)o(e)f(will)i(mak)o(e)e(extensiv)o(e)i(use)f(of)f (equational)i(rea-)243 2079 y(soning,)g(in)i(the)e(sense)h(that)f(a)g (built-in)i(term)e(rewriting)h(system)f(is)h(used)g(to)243 2133 y(automatically)15 b(decide)i(or)e(simplify)i(atomic)e(form)o (ulas)g(in)h(this)f(language.)301 2208 y(No)o(w,)c(w)o(e)h(can)h(form)o (ulate)f(the)g(goal)g(that)g(for)g(our)g(relation)h Fp(R)f Fx(\(notationally)243 2262 y(suppressed\))17 b(and)f(giv)o(en)h Fp(i;)8 b(j;)g(k)15 b Fx(there)i(exists)f(a)g(path)h(whic)o(h)g(either) g(is)g(empt)o(y)243 2316 y(\(then)22 b(there)h(is)g(no)g Fp(R)p Fx(-path)g(from)f Fp(j)j Fx(to)d Fp(k)h Fx(with)g(inner)h (elemen)o(ts)g Fp(<)h(i)p Fx(\))d(or)243 2370 y(connects)14 b Fp(j)i Fx(and)e Fp(k)h Fx(with)f(inner)h(no)q(des)g Fp(<)e(i)g Fx(and)i(is)f(rep)q(etition)h(free.)f(Note)f(that)243 2424 y(in)j(b)q(oth)f(cases)g(the)h(path)f(is)g(total.)912 2924 y Fm(finaljar2)o(.te)o(x;)h(29/01/2001)o(;)g(14:37;)i(p.9)p eop pstopssaved restore /pstopssaved save def pstopsmatrix setmatrix 708.661417 368.503937 translate 90 rotate 0.880000 dup scale /pstopsmatrix matrix currentmatrix def initclip pstopsxform concat 10 9 bop 243 50 a Fx(10)243 145 y Fr(Pr)o(oposition.)286 229 y Fl(8)p Fp(i;)8 b(j;)g(k)q Fl(9)438 210 y Fh(\003)456 229 y Fp(x)p Fl(f)p Fx([)p Fp(x)k Fx(=)h Fp(")g Fl(!)g(8)p Fp(y)r Fl(:)p Fp(P)804 236 y Fi(i)819 229 y Fx(\()p Fp(y)r(;)8 b(j;)g(k)q Fx(\)])f Fl(^)j Fx([)p Fp(x)i Fl(6)p Fx(=)h Fp(")g Fl(!)g Fp(P)1245 236 y Fi(i)1260 229 y Fx(\()p Fp(x;)8 b(j;)g(k)q Fx(\))f Fl(^)k Fg(rf)o Fx(\()p Fp(x)p Fx(\)])p Fl(g)p Fp(:)243 332 y Fx(W)l(e)k(use)h(the)f(follo)o(wing)h (assumptions:)351 416 y Fp(P)380 423 y Fi(i)395 416 y Fx(\()p Fp(x;)8 b(j;)g(k)q Fx(\))i Fl(!)j Fp(P)640 423 y Fi(i)p Fo(+1)699 416 y Fx(\()p Fp(x;)8 b(j;)g(k)q Fx(\))732 b(\(1\))351 482 y Fp(P)380 489 y Fo(0)400 482 y Fx(\()p Fp(x;)8 b(j;)g(k)q Fx(\))g Fl(^)i Fp(j)15 b Fl(6)p Fx(=)e Fp(k)h Fl(!)f Fp(R)p Fx(\()p Fp(j;)8 b(k)q Fx(\))669 b(\(2\))351 549 y Fp(P)380 556 y Fi(i)395 549 y Fx(\()p Fp(x;)8 b(j;)g(i)p Fx(\))f Fl(^)j Fp(P)610 556 y Fi(i)625 549 y Fx(\()p Fp(y)r(;)e(i;)g(k)q Fx(\))i Fl(!)j Fp(P)865 556 y Fi(i)p Fo(+1)924 549 y Fx(\()p Fp(x)d Fl(\001)f Fp(y)r(;)f(j;)g(k)q Fx(\))451 b(\(3\))351 615 y Fp(P)380 622 y Fi(i)395 615 y Fx(\()p Fp(x;)8 b(j;)g(i)p Fx(\))f Fl(^)j Fg(rf)p Fx(\()p Fp(x)p Fx(\))f Fl(^)i Fp(P)752 622 y Fi(i)766 615 y Fx(\()p Fp(y)r(;)d(i;)g(k)q Fx(\))f Fl(^)k Fg(rf)o Fx(\()p Fp(y)r Fx(\))e Fl(^)i(8)p Fp(z)r Fl(:)p Fp(P)1203 622 y Fi(i)1218 615 y Fx(\()p Fp(z)r(;)d(j;)g(k)q Fx(\))i Fl(!)j Fg(rf)p Fx(\()p Fp(x)d Fl(\001)f Fp(y)r Fx(\)\(4\))351 682 y Fp(P)380 689 y Fi(i)p Fo(+1)440 682 y Fx(\()p Fp(x;)f(j;)g(k)q Fx(\))f Fl(^)k(:)p Fp(P)695 689 y Fi(i)709 682 y Fx(\()p Fp(x;)d(j;)g(k)q Fx(\))j Fl(!)i(9)p Fp(y)r(P)1004 689 y Fi(i)1018 682 y Fx(\()p Fp(y)r(;)8 b(j;)g(i)p Fx(\))f Fl(^)k(9)p Fp(z)r(P)1280 689 y Fi(i)1294 682 y Fx(\()p Fp(z)r(;)d(i;)g(k)q Fx(\))143 b(\(5\))243 765 y(The)14 b(last)g(assumption)h(\(where)f(w)o(e)g(used)g (the)h(classical)g Fl(9)p Fx(\))g(con)o(tains)f(the)g(main)243 819 y(idea)f(of)f(the)g(pro)q(of:)f(if)i(there)g(is)f(a)g(path)g(from)g Fp(j)i Fx(to)e Fp(k)h Fx(whose)g(inner)g(elemen)o(ts)g(are)243 873 y(smaller)h(than)g Fp(i)p Fx(+1,)f(but)g(not)h(smaller)g(than)f Fp(i)p Fx(,)g(then)h(there)g(exist)g(paths)f(from)g Fp(j)243 927 y Fx(to)f Fp(i)g Fx(and)h(from)f Fp(i)g Fx(to)g Fp(k)i Fx(with)f(inner)g(elemen)o(ts)h(smaller)f(than)f Fp(i)p Fx(.)g(Assumption)h(\(4\))243 981 y(can)18 b(b)q(e)i(seen)f(as)f(follo) o(ws:)g(under)h(the)g(giv)o(en)g(h)o(yp)q(othesises)h Fp(x)12 b Fl(\001)g Fp(y)20 b Fx(could)g(only)243 1035 y(con)o(tain)15 b(a)f(rep)q(etition)i(if)f Fp(x)f Fx(and)h Fp(y)i Fx(ha)o(v)o(e)d(a)g(common)h(inner)g(elemen)o(t.)g(But)g(this) 243 1089 y(w)o(ould)g(con)o(tradict)g Fl(8)p Fp(z)r Fl(:)p Fp(P)698 1096 y Fi(i)713 1089 y Fx(\()p Fp(z)r(;)8 b(j;)g(k)q Fx(\).)243 1163 y Fj(Pr)n(o)n(of)h Fx(.)36 b(Induction)20 b(on)e Fp(i)p Fx(.)g Fj(Basis)t Fx(.)f(Giv)o(en)i Fp(j;)8 b(k)q Fx(.)17 b Fj(Case)k Fp(j)f Fx(=)e Fp(k)q Fx(.)g(Let)g Fp(x)g Fx(:=)g Fp(j)1581 1153 y Fh(\\)1604 1163 y Fp(")p Fx(.)243 1217 y(Then)e(w)o(e)g(ha)o(v)o(e)g Fp(P)565 1224 y Fo(0)585 1217 y Fx(\()p Fp(j)625 1207 y Fh(\\)648 1217 y Fp(";)8 b(j;)g(k)q Fx(\))14 b(since)j Fp(j)g Fx(=)e Fp(k)i Fx(and)f Fg(rf)p Fx(\()p Fp(j)1185 1207 y Fh(\\)1207 1217 y Fp(")p Fx(\))g(b)o(y)h(de\014nition.)g Fj(Case)243 1271 y Fp(j)h Fl(6)p Fx(=)f Fp(k)q Fx(.)g Fj(Sub)n(c)n(ase)j Fp(R)p Fx(\()p Fp(j;)8 b(k)q Fx(\).)15 b(Let)j Fp(x)e Fx(:=)h Fp(j)935 1261 y Fh(\\)957 1271 y Fp(k)982 1261 y Fh(\\)1006 1271 y Fp(")p Fx(.)g(Then)h(w)o(e)f(ha)o(v)o(e)g Fp(P)1383 1278 y Fo(0)1403 1271 y Fx(\()p Fp(j)1443 1261 y Fh(\\)1466 1271 y Fp(k)1491 1261 y Fh(\\)1514 1271 y Fp(";)8 b(j;)g(k)q Fx(\))243 1325 y(since)18 b Fp(R)p Fx(\()p Fp(j;)8 b(k)q Fx(\))15 b(and)j Fg(rf)o Fx(\()p Fp(j)667 1315 y Fh(\\)690 1325 y Fp(k)715 1315 y Fh(\\)738 1325 y Fp(")p Fx(\))f(since)h Fp(j)g Fl(6)p Fx(=)f Fp(k)q Fx(.)f Fj(Sub)n(c)n(ase)k Fl(:)p Fp(R)p Fx(\()p Fp(j;)8 b(k)q Fx(\).)15 b(Let)i Fp(x)f Fx(:=)g Fp(")p Fx(.)243 1379 y(W)l(e)f(obtain)g Fl(8)p Fp(y)r Fl(:)p Fp(P)570 1386 y Fi(i)585 1379 y Fx(\()p Fp(y)r(;)8 b(j;)g(k)q Fx(\))13 b(b)o(y)i(using)h(\(2\).)301 1433 y Fj(Step)i Fp(i)9 b Fx(+)i(1.)j(Giv)o(en)i Fp(j;)8 b(k)q Fx(.)14 b(By)h(IH)h(w)o(e)f(ha)o(v)o(e)g Fp(x)1084 1440 y Fi(i)1098 1433 y Fx(.)f(W)l(e)i(m)o(ust)e(\014nd)i Fp(x)1433 1440 y Fi(i)p Fo(+1)1492 1433 y Fx(.)301 1487 y Fj(Case)22 b Fp(x)445 1494 y Fi(i)479 1487 y Fx(=)e Fp(")p Fx(.)f(Then)h(w)o(e)f (ha)o(v)o(e)g Fl(8)p Fp(y)r Fl(:)p Fp(P)998 1494 y Fi(i)1013 1487 y Fx(\()p Fp(y)r(;)8 b(j;)g(k)q Fx(\).)17 b(By)i(IH,)h(applied)h (to)e Fp(j;)8 b(i;)243 1541 y Fx(\()p Fp(i;)g(k)14 b Fx(resp)q(ectiv)o(ely\))j(w)o(e)e(ha)o(v)o(e)g Fp(x)800 1548 y Fi(i;j;i)875 1541 y Fx(and)g Fp(x)989 1548 y Fi(i;i;k)1054 1541 y Fx(,)f(i.e.)i(paths)f(from)f Fp(j)j Fx(to)e Fp(i)g Fx(\()p Fp(i)f Fx(to)g Fp(k)243 1595 y Fx(resp)q(ectiv)o(ely\))i(with)g (inner)g(elemen)o(ts)g(smaller)g(than)f Fp(i)p Fx(.)301 1649 y Fj(Sub)n(c)n(ase)27 b Fp(x)505 1656 y Fi(i;j;i)593 1649 y Fx(=)i Fp(")p Fx(.)24 b(Then)h(w)o(e)g(ha)o(v)o(e)f Fl(8)p Fp(y)10 b Fl(:)p Fp(P)1150 1656 y Fi(i)1164 1649 y Fx(\()p Fp(y)r(;)e(j;)g(i)p Fx(\).)22 b(Let)i Fp(x)1452 1656 y Fi(i)p Fo(+1)1540 1649 y Fx(=)29 b Fp(")p Fx(.)243 1703 y(Giv)o(en)16 b Fp(y)r Fx(.)g(Assumption:)g Fp(P)722 1710 y Fi(i)p Fo(+1)781 1703 y Fx(\()p Fp(y)r(;)8 b(j;)g(k)q Fx(\).)13 b(By)k(\(5\))e(\(since)h Fl(:)p Fp(P)1288 1710 y Fi(i)1303 1703 y Fx(\()p Fp(y)r(;)8 b(j;)g(k)q Fx(\)\))13 b(w)o(e)j(ha)o(v)o(e)243 1757 y Fl(9)p Fp(y)r(P)321 1764 y Fi(i)335 1757 y Fx(\()p Fp(y)r(;)8 b(j;)g(i)p Fx(\);)k(con)o (tradiction.)301 1811 y Fj(Sub)n(c)n(ase)17 b Fp(x)495 1818 y Fi(i;j;i)568 1811 y Fl(6)p Fx(=)c Fp(")p Fx(.)301 1864 y Fj(Subsub)n(c)n(ase)22 b Fp(x)564 1871 y Fi(i;i;k)649 1864 y Fx(=)e Fp(")p Fx(.)g(Then)g(w)o(e)f(ha)o(v)o(e)h Fl(8)p Fp(y)r Fl(:)p Fp(P)1170 1871 y Fi(i)1184 1864 y Fx(\()p Fp(y)r(;)8 b(i;)g(k)q Fx(\).)17 b(Let)j Fp(x)1469 1871 y Fi(i)p Fo(+1)1548 1864 y Fx(=)h Fp(")p Fx(.)243 1918 y(Giv)o(en)16 b Fp(y)r Fx(.)g(Assumption:)g Fp(P)722 1925 y Fi(i)p Fo(+1)781 1918 y Fx(\()p Fp(y)r(;)8 b(j;)g(k)q Fx(\).)13 b(By)k(\(5\))e(\(since)h Fl(:)p Fp(P)1288 1925 y Fi(i)1303 1918 y Fx(\()p Fp(y)r(;)8 b(j;)g(k)q Fx(\)\))13 b(w)o(e)j(ha)o(v)o(e)243 1972 y Fl(9)p Fp(z)r(P)320 1979 y Fi(i)334 1972 y Fx(\()p Fp(z)r(;)8 b(i;)g(k)q Fx(\);)13 b(con)o(tradiction.)301 2026 y Fj(Subsub)n(c)n(ase)k Fp(x)559 2033 y Fi(i;i;k)637 2026 y Fl(6)p Fx(=)c Fp(")p Fx(.)i(Let)h Fp(x)842 2033 y Fi(i)p Fo(+1)914 2026 y Fx(:=)d Fp(x)1001 2033 y Fi(i;j;i)1071 2026 y Fl(\001)d Fp(x)1120 2033 y Fi(i;i;k)1185 2026 y Fx(.)15 b(Then,)g(b)o(y)g(\(3\))g (w)o(e)g(ha)o(v)o(e)243 2080 y Fp(P)272 2087 y Fi(i)p Fo(+1)331 2080 y Fx(\()p Fp(x)375 2087 y Fi(i)p Fo(+1)434 2080 y Fp(;)8 b(j;)g(k)q Fx(\))19 b(and)j(b)o(y)f(\(4\))g Fg(rf)o Fx(\()p Fp(x)874 2087 y Fi(i)p Fo(+1)933 2080 y Fx(\),)g(since)h Fl(8)p Fp(y)r Fl(:)p Fp(P)1210 2087 y Fi(i)1225 2080 y Fx(\()p Fp(y)r(;)8 b(j;)g(k)q Fx(\))19 b(follo)o(ws)i(from)243 2134 y Fp(x)269 2141 y Fi(i)295 2134 y Fx(=)13 b Fp(")p Fx(.)301 2188 y Fj(Case)g Fp(x)436 2195 y Fi(i)463 2188 y Fl(6)p Fx(=)g Fp(")p Fx(.)e(Let)g Fp(x)659 2195 y Fi(i)p Fo(+1)731 2188 y Fx(:=)h Fp(x)817 2195 y Fi(i)831 2188 y Fx(.)f(Then)g(w)o(e)g(ha)o(v)o(e)f Fg(rf)o Fx(\()p Fp(x)1205 2195 y Fi(i)p Fo(+1)1264 2188 y Fx(\))h(and)g Fp(P)1406 2195 y Fi(i)1420 2188 y Fx(\()p Fp(x)1464 2195 y Fi(i)p Fo(+1)1523 2188 y Fp(;)d(j;)g(k)q Fx(\),)243 2242 y(hence)16 b Fp(P)398 2249 y Fi(i)p Fo(+1)457 2242 y Fx(\()p Fp(x)501 2249 y Fi(i)p Fo(+1)560 2242 y Fp(;)8 b(j;)g(k)q Fx(\))13 b(b)o(y)i(\(1\).)f(This)i(concludes)h(the) e(pro)q(of.)301 2316 y(F)l(rom)9 b(a)h(formal)g(pro)q(of)g(of)f(this)i (prop)q(osition)g(w)o(e)f(ha)o(v)o(e)g(extracted)g(in)h Fr(Minlog)243 2370 y Fx(the)j(follo)o(wing)g(program;)f(this)h(is)h (the)f(original)h(output,)e(with)h(only)h(the)f(names)243 2424 y(of)h(the)g(v)m(ariables)h(adjusted)g(and)f(inden)o(tation)h (added.)892 2924 y Fm(finaljar2.)o(tex)o(;)g(29/01/2001;)g(14:37;)h (p.10)p eop pstopssaved restore %%Page: pstops 6 /pstopssaved save def pstopsmatrix setmatrix 708.661417 0.000000 translate 90 rotate 0.880000 dup scale /pstopsmatrix matrix currentmatrix def initclip pstopsxform concat /showpage{}def/copypage{}def/erasepage{}def 11 10 bop 772 50 a Fo(W)m(arshall)10 b(and)g(Dic)o(kson)482 b Fx(11)243 145 y Fb([R]nat-rec)243 199 y(\([j,k][if)22 b(j=k)i(then)f(con)h(j)f(eps)h(else)386 253 y([if)f(R)h(j)g(k)g(then)f (con)g(j\(con)h(k)f(eps\))h(else)f(eps]]\))243 307 y(\([i,g,j,k][if)f (\(g)h(j)h(k\)=eps)f(then)577 361 y([if)g(\(g)h(j)g(i\)=eps)f(then)672 415 y(eps)h(else)672 469 y([if)g(\(g)f(i)h(k\)=eps)f(then)768 523 y(eps)g(else)768 577 y(dot\(g)g(j)h(i\)\(g)f(i)h(k\)]])f(else)601 631 y(g)g(j)h(k]\))243 727 y Fx(T)l(o)13 b(mak)o(e)g(this)h(program)e (more)h(readable,)g(w)o(e)h(giv)o(e)f(the)h(\(primitiv)o(e\))g (recursion)243 781 y(equations)21 b(for)e(the)i(function)g Fp(f)26 b Fx(de\014ned)21 b(b)o(y)g(it,)f(returning)h(for)f(giv)o(en)h Fp(i;)8 b(j;)g(k)243 835 y Fx(either)20 b(a)g(path)f(from)g Fp(j)j Fx(to)d Fp(k)i Fx(with)f(inner)h(elemen)o(ts)g(smaller)f(than)g Fp(i)f Fx(or)g(the)243 889 y(empt)o(y)14 b(path)g Fp(")p Fx(.)h(W)l(e)f(again)h(suppress)g(the)f(parameter)g(for)g(the)g(giv)o (en)h(relation:)445 987 y Fp(f)5 b Fx(\(0)p Fp(;)j(j;)g(k)q Fx(\))22 b(:=)j Fg(if)116 b Fp(j)15 b Fx(=)e Fp(k)712 1054 y Fg(then)47 b Fp(j)863 1044 y Fh(\\)886 1054 y Fp(")712 1120 y Fg(else)69 b(if)116 b Fp(Rj)s(k)848 1186 y Fg(then)47 b Fp(j)999 1177 y Fh(\\)1022 1186 y Fp(k)1047 1177 y Fh(\\)1071 1186 y Fp(")848 1253 y Fg(else)69 b Fp(")373 1386 y(f)5 b Fx(\()p Fp(i)10 b Fx(+)g(1)p Fp(;)e(j;)g(k)q Fx(\))23 b(:=)i Fg(if)116 b Fp(f)5 b Fx(\()p Fp(i;)j(j;)g(k)q Fx(\))i(=)j Fp(")712 1452 y Fg(then)47 b(if)116 b Fp(f)5 b Fx(\()p Fp(i;)j(j;)g(i)p Fx(\))i(=)j Fp(")843 1519 y Fg(then)47 b Fp(")843 1585 y Fg(else)69 b(if)117 b Fp(f)5 b Fx(\()p Fp(i;)j(i;)g(k)q Fx(\))i(=)i Fp(")980 1651 y Fg(then)47 b Fp(")980 1718 y Fg(else)68 b Fp(f)5 b Fx(\()p Fp(i;)j(j;)g(i)p Fx(\))g Fl(\001)h Fp(f)c Fx(\()p Fp(i;)j(i;)g(k)q Fx(\))712 1784 y Fg(else)69 b Fp(f)5 b Fx(\()p Fp(i;)j(j;)g(k)q Fx(\))243 1883 y Fj(R)n(emarks)t Fx(.)44 b(1.)22 b(In)h(order)f(to)g(get)g(a)h(truly)f Fp(O)q Fx(\()p Fp(n)1115 1866 y Fo(3)1135 1883 y Fx(\))g(algorithm)h Fp(f)k Fx(has)c(to)f(b)q(e)243 1937 y(understo)q(o)q(d)f(as)f(a)h (function)g(computing)g(for)f(ev)o(ery)h Fp(i)f Fx(an)h Fp(n)14 b Fl(\002)g Fp(n)21 b Fx(matrix)f(of)243 1991 y(paths)15 b(\(and)g(not)g(as)f(a)h(function)h(of)f(three)g(argumen)o (ts\).)301 2073 y(2.)c(The)g(W)l(arshall)h(algorithm)g(w)o(as)e(also)i (considered)h(b)o(y)e(\(Bro)o(y)g(and)g(P)o(epp)q(er,)243 2126 y(1981\))19 b(and)i(\(Pfenning,)f(1990\))g(in)h(the)f(con)o(text)g (of)h(program)e(optimization.)243 2180 y(Pfenning)g(informally)g(reads) g(o\013)e(the)h(algorithm)h(from)e(a)h(similar)h(pro)q(of)f(and)243 2234 y(claims)e(that)e(this)i(could)g(b)q(e)g(done)g(automatically)l(.) 301 2316 y(3.)h(The)i(Dijkstra)e(algorithm)h(has)g(b)q(een)h(treated)f (similarly)h(in)g(\(Benl)g(and)243 2370 y(Sc)o(h)o(wic)o(h)o(ten)o(b)q (erg,)13 b(1999\).)f(Ho)o(w)o(ev)o(er,)g(the)h(pro)q(of)g(is)h (somewhat)e(more)h(complex;)243 2424 y(in)20 b(particular)h(one)f(has)f (to)g(b)q(e)i(careful)f(to)f(select)h(the)g(righ)o(t)g(language.)f(The) 892 2924 y Fm(finaljar2.)o(tex)o(;)d(29/01/2001;)g(14:37;)h(p.11)p eop pstopssaved restore /pstopssaved save def pstopsmatrix setmatrix 708.661417 368.503937 translate 90 rotate 0.880000 dup scale /pstopsmatrix matrix currentmatrix def initclip pstopsxform concat 12 11 bop 243 50 a Fx(12)243 145 y(program)14 b(extracted)h(from)g(the) h(pro)q(of)f(is)h(as)f(readable)i(as)e(the)g(one)h(ab)q(o)o(v)o(e)f (and)243 199 y(not)g(m)o(uc)o(h)g(longer.)477 357 y Fs(5.)37 b(F)l(rom)16 b(classical)j(to)f(in)o(tuitionistic)j(pro)q(ofs)243 462 y Fx(In)i(our)f(second)h(example)g(w)o(e)f(will)i(study)f(a)f (non-constructiv)o(e)h(pro)q(of)f(of)g(a)243 516 y(sp)q(ecial)h(case)e (of)g(Dic)o(kson's)g(Lemma.)g(T)l(o)g(extract)f(a)h(program)f(w)o(e)h (need)h(to)243 570 y(transform)17 b(this)j(pro)q(of)f(in)o(to)g(a)f (constructiv)o(e)i(one.)f(In)g(the)g(follo)o(wing)h(w)o(e)f(de-)243 624 y(scrib)q(e)e(in)f(general)g(ho)o(w)f(and)h(under)g(whic)o(h)h (conditions)g(a)e(classical)i(existence)243 678 y(pro)q(of,)j(i.e.)h(a) f(pro)q(of)h(of)f Fl(9)p Fp(y)r(B)r Fx(,)h(can)g(b)q(e)h(transformed)e (in)o(to)g(an)h(in)o(tuitionistic)243 732 y(existence)e(pro)q(of,)e (i.e.)h(a)g(pro)q(of)g(of)f Fl(9)891 716 y Fh(\003)911 732 y Fp(y)10 b(B)r Fx(.)18 b(This)h(metho)q(d)f(is)h(mostly)e (referred)243 786 y(to)h(as)g(H.)h(F)l(riedman's)g Fp(A)p Fx(-translation)g(\(F)l(riedman,)f(1978\).)f(It)i(w)o(as)f(indep)q(en-) 243 840 y(den)o(tly)h(in)o(v)o(estigated)g(in)g(\(Dragalin,)f(1979\),)e (and)j(v)m(arian)o(ts)f(w)o(ere)g(considered)243 894 y(in)i(\(Leiv)m(an)o(t,)f(1985\))f(and)h(\(T)l(ro)q(elstra)f(and)h(v)m (an)h(Dalen,)f(1988\).)e(In)j(\(Murth)o(y)l(,)243 948 y(1990\))12 b(this)i(translation)f(has)g(b)q(een)i(applied)g(to)e(a)g (classical)i(pro)q(of)e(of)g(Higman's)243 1002 y(Lemma.)20 b(The)h(results)f(there)h(ho)o(w)o(ev)o(er)e(sho)o(w)o(ed)h(that)g(a)g (literal)i(application)243 1056 y(leads)g(to)f(an)g(explosion)i(in)f (size)h(of)e(the)g(translated)g(pro)q(of)h(and)f(in)i(turn)e(of)243 1110 y(the)i(extracted)g(program.)e(F)l(or)i(this)g(reason)g(w)o(e)g (use)g(a)g(re\014nemen)o(t)h(of)e(the)243 1164 y Fp(A)p Fx(-translation,)c(dev)o(elop)q(ed)i(in)f(\(Berger)f(and)g(Sc)o(h)o (wic)o(h)o(ten)o(b)q(erg,)g(1995\).)f(First)243 1218 y(w)o(e)e(allo)o(w)g(assumptions)g(\(without)g(computational)g(con)o (ten)o(t\))f(and)h(second)h(w)o(e)243 1272 y(apply)e(the)f(translation) h(only)g(when)g(necessary)l(,)f(i.e.)g(to)g(atomic)g(form)o(ulas)g (with)243 1326 y(so-called)22 b(critical)g(relation)f(sym)o(b)q(ols)g (\(see)f(b)q(elo)o(w\).)h(Using)g(this)g(re\014nemen)o(t)243 1380 y(the)14 b(extracted)f(programs)f(will)k(in)e(general)h(ha)o(v)o (e)e(a)g(simpler)i(con)o(trol)f(structure)243 1434 y(and)h(th)o(us)g (will)i(b)q(e)f(more)f(e\016cien)o(t)h(and)f(more)g(readable.)301 1510 y(The)h(basic)h(idea)f(of)g(the)g(translation)g(is)g(as)g(follo)o (ws:)f(b)o(y)h(means)g(of)g(G\177)-23 b(odel's)243 1564 y(w)o(ell-kno)o(wn)13 b(negativ)o(e)g(translation)g(a)f(classical)j (pro)q(of)d(of)g Fl(9)p Fp(y)e(B)16 b Fx(\(sa)o(y)11 b Fp(B)16 b Fx(atomic)243 1618 y(for)d(simplicit)o(y\))j(is)f (transformed)e(in)o(to)h(a)g(pro)q(of)g(in)h Fj(minimal)g(lo)n(gic)e Fx(of)h(the)g(same)243 1672 y(form)o(ula)h(\(recall)h(that)f Fl(9)p Fp(y)10 b(B)16 b Fx(=)d(\()p Fl(8)p Fp(y)r(:B)j Fl(!)d(?)p Fx(\))g Fl(!)h(?)p Fx(\).)h(Since)i(in)g(minimal)g(logic)243 1726 y(the)i(prop)q(ositional)i(constan)o(t)d Fl(?)i Fx(do)q(es)f(not)g(pla)o(y)h(a)e(sp)q(ecial)k(role,)d(it)g(ma)o(y)g(b)q (e)243 1780 y(replaced)d(b)o(y)f(an)g(arbitrary)g(prop)q(osition,)h (for)e(example)i(b)o(y)824 1870 y Fp(A)c Fx(:=)h Fl(9)956 1851 y Fh(\003)976 1870 y Fp(y)c(B)r(:)243 1960 y Fx(Applying)18 b(this)f(to)f(our)h(minimal)h(pro)q(of)e(of)g Fl(9)p Fp(y)10 b(B)20 b Fx(yields)e(a)e(pro)q(of)g(in)i(minimal)243 2014 y(logic)e(of)g(\()p Fl(8)p Fp(y)r(:B)g Fl(!)e Fp(A)p Fx(\))g Fl(!)g Fp(A)p Fx(.)h(Since)j(the)e(premise,)g Fl(8)p Fp(y)r(:B)g Fl(!)e Fp(A)p Fx(,)i(is)g(a)g(theorem)243 2068 y(of)f(in)o(tuitionistic)i(logic,)f(w)o(e)f(obtain)g(an)g(in)o (tuitionistic)j(pro)q(of)d(of)g Fp(A)p Fx(.)301 2145 y(T)l(o)g(describ)q(e)i(the)e(re\014nemen)o(t)h(w)o(e)f(\014rst)f(set) 340 2244 y Fl(9)p Fp(y)387 2251 y Fo(1)408 2244 y Fp(;)8 b(:)g(:)g(:)t(;)g(y)531 2251 y Fi(k)578 2203 y(n)567 2212 y Fc(V)-27 b(V)560 2282 y Fi(i)p Fo(=1)624 2244 y Fp(B)658 2251 y Fi(i)686 2244 y Fx(:=)12 b(\()p Fl(8)p Fp(y)811 2251 y Fo(1)831 2244 y Fp(;)c(:)g(:)g(:)d(;)j(y)955 2251 y Fi(k)983 2244 y Fp(:)g(B)1038 2251 y Fo(1)1070 2244 y Fl(!)13 b Fp(:)8 b(:)g(:)j Fl(!)i Fp(B)1286 2251 y Fi(n)1323 2244 y Fl(!)g(?)p Fx(\))g Fl(!)g(?)243 2370 y Fx(or)d(more)g(brie\015y)h Fl(9)p Fp(~)-23 b(y)595 2338 y Fc(V)-28 b(V)637 2382 y Fi(i)659 2370 y Fp(B)693 2377 y Fi(i)720 2370 y Fx(:=)13 b(\()p Fl(8)p Fp(~)-23 b(y)9 b(:)882 2359 y(~)876 2370 y(B)15 b Fl(!)e(?)p Fx(\))f Fl(!)h(?)p Fp(:)e Fx(Supp)q(ose)g(w)o(e)g(ha)o(v)o(e)f(a)g(pro)q(of)243 2424 y Fp(d)p Fx(:)e Fl(9)p Fp(~)-23 b(y)343 2392 y Fc(V)c(V)385 2436 y Fi(i)407 2424 y Fp(B)441 2431 y Fi(i)456 2424 y Fx(,)18 b(where)h Fp(B)656 2431 y Fi(i)690 2424 y Fx(is)g(quan)o (ti\014er)g(free,)g(using)g(a)g(set)g(of)f(\005-assumptions)892 2924 y Fm(finaljar2.)o(tex)o(;)e(29/01/2001;)g(14:37;)h(p.12)p eop pstopssaved restore %%Page: pstops 7 /pstopssaved save def pstopsmatrix setmatrix 708.661417 0.000000 translate 90 rotate 0.880000 dup scale /pstopsmatrix matrix currentmatrix def initclip pstopsxform concat /showpage{}def/copypage{}def/erasepage{}def 13 12 bop 772 50 a Fo(W)m(arshall)10 b(and)g(Dic)o(kson)482 b Fx(13)243 145 y(\000)19 b(=)g Fl(f8)o Fp(~)-22 b(x)418 152 y Fo(1)445 145 y Fp(C)478 152 y Fo(1)497 145 y Fp(;)8 b(:)g(:)g(:)d(;)j Fl(8)o Fp(~)-22 b(x)650 152 y Fi(n)681 145 y Fp(C)714 152 y Fi(n)744 145 y Fl(g)p Fx(,)18 b(where)i(the)e Fp(C)1048 152 y Fi(i)1081 145 y Fx(are)g(quan)o(ti\014er)i(free.)e(W)l (e)h(ma)o(y)243 199 y(assume)11 b(that)g(the)h Fp(B)600 206 y Fi(i)626 199 y Fx(and)g Fp(C)744 206 y Fi(j)773 199 y Fx(are)g(purely)g(implicational)i(form)o(ulas)e(\(otherwise)243 253 y(using)21 b(the)g(logical)i(equiv)m(alences)g([)p Fp(A)14 b Fl(^)g Fp(B)25 b Fl(!)e Fp(C)s Fx(])e Fl($)i Fx([)p Fp(A)f Fl(!)g Fp(B)j Fl(!)e Fp(C)s Fx(])d(and)243 307 y([)p Fp(A)12 b Fl(!)h Fp(C)f Fl(^)d Fp(D)q Fx(])j Fl($)h Fx([)p Fp(A)g Fl(!)g Fp(C)s Fx(])8 b Fl(^)i Fx([)p Fp(A)i Fl(!)h Fp(D)q Fx(])h(w)o(e)g(can)h(push)h Fl(^)e Fx(to)g(the)h(outside\).)g(T)l(o)243 361 y(sp)q(ecify)h(the)g(atomic)f (form)o(ulas)f(a\013ected)h(b)o(y)g(the)h(translation)f(w)o(e)g(set)672 445 y Fp(L)d Fx(:=)h Fl(f)8 b Fp(C)840 452 y Fo(1)858 445 y Fp(;)g(:)g(:)g(:)d(;)j(C)993 452 y Fi(n)1015 445 y Fp(;)1043 434 y(~)1036 445 y(B)15 b Fl(!)e(?)8 b(g)243 530 y Fx(and)21 b(de\014ne)i(the)e(set)g(of)g Fp(L)p Fx(-)p Fj(critic)n(al)k Fx(relation)d(sym)o(b)q(ols)g(as)f(the)g (smallest)h(set)243 584 y(satisfying)15 b(the)h(follo)o(wing)g (conditions:)255 664 y(\(i\))31 b Fl(?)15 b Fx(is)h Fp(L)p Fx(-critical.)249 756 y(\(ii\))25 b(If)17 b(\()406 745 y Fp(~)399 756 y(C)432 763 y Fo(1)468 756 y Fl(!)g Fp(P)559 763 y Fo(1)578 756 y Fx(\()n Fp(~)-21 b(s)617 763 y Fo(1)637 756 y Fx(\)\))16 b Fl(!)h Fp(:)8 b(:)g(:)14 b Fl(!)j Fx(\()907 745 y Fp(~)900 756 y(C)933 763 y Fi(m)982 756 y Fl(!)g Fp(P)1073 763 y Fi(m)1106 756 y Fx(\()n Fp(~)-21 b(s)1145 763 y Fi(m)1179 756 y Fx(\)\))15 b Fl(!)i Fp(R)p Fx(\()1342 748 y Fp(~)1345 756 y(t)p Fx(\))g(is)h(a)g(p)q(ositiv)o(e) 334 810 y(subform)o(ula)h(of)g(a)h(form)o(ula)f(in)h Fp(L)p Fx(,)f(and)h(if)g(for)f(some)g Fp(i)g(P)1358 817 y Fi(i)1392 810 y Fx(is)h Fp(L)p Fx(-critical,)334 864 y(then)15 b Fp(R)g Fx(is)h Fp(L)p Fx(-critical.)243 944 y(W)l(e)f(let)h Fp(A)c Fx(:=)h Fl(9)519 928 y Fh(\003)539 944 y Fp(~)-23 b(y)570 912 y Fc(V)c(V)612 956 y Fi(i)634 944 y Fp(B)668 951 y Fi(i)698 944 y Fx(and)15 b(de\014ne)h(an)g Fp(A)p Fx(-translation)f(relativ)o(e)h(to)e Fp(L)p Fx(:)490 1029 y Fl(?)525 1010 y Fi(A)567 1029 y Fx(:=)f Fp(A)45 b Fx(and)15 b(for)g Fp(R)e Fl(6)p Fx(=)f Fl(?)490 1119 y Fp(R)p Fx(\()540 1110 y Fp(~)543 1119 y(t)p Fx(\))577 1100 y Fi(A)618 1119 y Fx(:=)679 1059 y Fc(\032)718 1095 y Fx(\()p Fp(R)p Fx(\()786 1087 y Fp(~)789 1095 y(t)o Fx(\))g Fl(!)i Fp(A)p Fx(\))e Fl(!)h Fp(A)46 b Fx(if)15 b Fp(R)g Fx(is)h Fp(L)p Fx(-critical,)718 1149 y Fp(R)p Fx(\()768 1141 y Fp(~)771 1149 y(t)o Fx(\))291 b(otherwise,)490 1218 y(\()p Fp(B)15 b Fl(!)f Fp(C)s Fx(\))670 1200 y Fi(A)710 1218 y Fx(:=)f Fp(B)807 1200 y Fi(A)849 1218 y Fl(!)g Fp(C)943 1200 y Fi(A)971 1218 y Fp(:)243 1303 y Fx(No)o(w,)j(a)g(constructiv)o(e)i(pro)q(of)e(of)h Fl(9)857 1286 y Fh(\003)876 1303 y Fp(~)-22 b(y)908 1271 y Fc(V)-27 b(V)950 1314 y Fi(i)972 1303 y Fp(B)1006 1310 y Fi(i)1037 1303 y Fx(can)18 b(b)q(e)f(generated)g(with)h(help)g(of)243 1357 y(the)d(follo)o(wing)h(lemmas.)243 1431 y Fr(Lemma)h(1.)30 b Fp(C)15 b Fl(!)f Fp(C)625 1415 y Fi(A)668 1431 y Fq(is)i(deriv)m (able)h(for)d(an)o(y)h Fp(C)h Fl(2)d(f)8 b Fp(C)1218 1438 y Fo(1)1236 1431 y Fp(;)g(:)g(:)g(:)d(;)j(C)1371 1438 y Fi(n)1393 1431 y Fl(g)p Fq(.)243 1511 y Fr(Lemma)17 b(2.)30 b Fq(There)16 b(is)f(a)g(deriv)m(ation)i(of)d Fl(8)p Fp(~)-23 b(y)s(:)1032 1500 y(~)1025 1511 y(B)1061 1495 y Fi(A)1102 1511 y Fl(!)13 b Fp(A)p Fq(.)243 1586 y Fx(F)l(ollo)o(wing)18 b(the)g(ideas)h(sk)o(etc)o(hed)f(in)h(the)f(ra) o(w)e(translation)i(the)g Fp(A)p Fx(-translation)243 1639 y(transforms)c(the)h(pro)q(of)g Fp(d)p Fx(:)8 b Fl(9)p Fp(~)-23 b(y)767 1607 y Fc(V)c(V)809 1651 y Fi(i)831 1639 y Fp(B)865 1646 y Fi(i)895 1639 y Fx(in)o(to)15 b(a)g(deriv)m(ation)710 1729 y Fp(d)734 1711 y Fi(A)763 1729 y Fx(:)8 b(\()p Fl(8)p Fp(~)-23 b(y)8 b(:)885 1718 y(~)878 1729 y(B)914 1711 y Fi(A)955 1729 y Fl(!)13 b Fp(A)p Fx(\))g Fl(!)g Fp(A)243 1814 y Fx(from)j(the)h(assumptions)g Fl(8)o Fp(~)-22 b(x)743 1821 y Fo(1)763 1814 y Fp(C)799 1797 y Fi(A)796 1825 y Fo(1)827 1814 y Fp(;)8 b(:)g(:)g(:)d(;)j Fl(8)o Fp(~)-22 b(x)980 1821 y Fi(n)1003 1814 y Fp(C)1039 1797 y Fi(A)1036 1825 y(n)1067 1814 y Fp(:)17 b Fx(By)g(lemma)g(1)f (these)h(assump-)243 1868 y(tions)g(are)g(pro)o(v)m(able)i(\(from)d (the)h(\005-assumptions)h(they)g(come)f(from\),)f(and)i(b)o(y)243 1927 y(lemma)d(2)g(the)g(premise)h Fl(8)p Fp(~)-23 b(y)s(:)742 1916 y(~)735 1927 y(B)771 1911 y Fi(A)812 1927 y Fl(!)13 b Fp(A)i Fx(is)h(pro)o(v)m(able.)301 1981 y(T)l(o)h(summarize,)g(w)o(e) g(end)h(up)g(with)g(a)f(pro)q(of)f(of)h Fp(A)g Fx(=)f Fl(9)1284 1965 y Fh(\003)1304 1981 y Fp(~)-23 b(y)1335 1949 y Fc(V)c(V)1377 1993 y Fi(i)1399 1981 y Fp(B)1433 1988 y Fi(i)1465 1981 y Fx(from)16 b(the)243 2035 y(assumptions)g Fl(8)o Fp(~)-22 b(x)553 2042 y Fo(1)573 2035 y Fp(C)606 2042 y Fo(1)625 2035 y Fp(;)8 b(:)g(:)g(:)d(;)j Fl(8)o Fp(~)-22 b(x)778 2042 y Fi(n)800 2035 y Fp(C)833 2042 y Fi(n)856 2035 y Fx(,)16 b(whic)o(h)g(\(compared)g(with)g(the)g (original)g Fp(A)p Fx(-)243 2089 y(translation\))k(uses)g(signi\014can) o(tly)i(few)o(er)e(case)g(distinctions)i(\(cf.)e(Berger)g(and)243 2143 y(Sc)o(h)o(wic)o(h)o(ten)o(b)q(erg,)15 b(1995\).)892 2924 y Fm(finaljar2.)o(tex)o(;)h(29/01/2001;)g(14:37;)h(p.13)p eop pstopssaved restore /pstopssaved save def pstopsmatrix setmatrix 708.661417 368.503937 translate 90 rotate 0.880000 dup scale /pstopsmatrix matrix currentmatrix def initclip pstopsxform concat 14 13 bop 243 50 a Fx(14)353 145 y Fs(6.)36 b(The)18 b(computational)i(con)o(ten)o(t)e(of)f(Dic)o(kson's)f(Lemma)243 257 y Fx(In)i(this)h(section)g(w)o(e)e(study)i(a)e(non-constructiv)o(e) i(pro)q(of)f(of)f(a)h(sp)q(ecial)i(case)e(of)243 311 y(Dic)o(kson's)h(Lemma.)h(The)g(pro)q(of)g(will)h(b)q(e)g(giv)o(en)f (informally)l(,)h(but)f(in)h(suc)o(h)f(a)243 365 y(detail)c(that)f(it)h (will)h(b)q(e)f(immediately)i(clear)e(ho)o(w)f(to)g(formalize)h(it.)f (W)l(e)h(sk)o(etc)o(h)243 419 y(ho)o(w)g(this)g(pro)q(of)g(is)h (transformed)e(in)o(to)i(a)f(constructiv)o(e)g(one)h(b)o(y)f(applying)h (the)243 473 y(metho)q(d)e(ab)q(o)o(v)o(e,)g(and)g(discuss)h(the)g (extracted)e(program.)243 585 y(6.1.)30 b Fr(The)17 b(classical)g(pr)o (oof)h(and)f(its)g(transla)m(tion)243 684 y Fx(Recall)g(Dic)o(kson's)e (Lemma)g(for)f(pairs)i(of)f(sequences:)243 793 y Fr(Pr)o(oposition.)29 b Fl(8)p Fp(f)r(;)8 b(g)h Fl(9)f Fp(i;)g(j:)13 b(i)f(<)h(j)28 b Fl(^)d Fp(f)5 b Fx(\()p Fp(j)s Fx(\))12 b Fl(6)p Fp(<)h(f)5 b Fx(\()p Fp(i)p Fx(\))24 b Fl(^)i Fp(g)r Fx(\()p Fp(j)s Fx(\))10 b Fl(6)p Fp(<)j(g)r Fx(\()p Fp(i)p Fx(\))p Fp(:)301 875 y Fx(Analogously)h(to)f(the)h(informal)g(pro)q(of)g(giv)o(en)g(in)g (the)g(in)o(tro)q(duction,)g(w)o(e)g(will)243 929 y(use)19 b(a)g(\(classical\))g(minim)o(um)h(principle)i(sa)o(ying)d(that)f(if)h (there)g(is)h(an)e Fp(x)h Fx(with)243 983 y(prop)q(ert)o(y)i Fp(P)6 b Fx(\()p Fp(x)p Fx(\),)22 b(then)g(there)g(also)g(exists)g(a)g (minimal)i(one,)d(w.r.t.)f(a)i(giv)o(en)243 1037 y(measure)15 b(function)h Fp(m)p Fx(:)407 1135 y Fl(9)8 b Fp(x)14 b(P)6 b Fx(\()p Fp(x)p Fx(\))13 b Fl(!)g(9)8 b Fp(x)15 b Fx(\()p Fp(P)6 b Fx(\()p Fp(x)p Fx(\))25 b Fl(^)g(8)p Fp(y)r(:)8 b(m)p Fx(\()p Fp(y)r Fx(\))j Fp(<)i(m)p Fx(\()p Fp(x)p Fx(\))f Fl(!)h(:)p Fp(P)6 b Fx(\()p Fp(y)r Fx(\)\))p Fp(:)243 1260 y Fj(Pr)n(o)n(of)16 b(of)g(the)h(pr)n(op)n(osition)s Fx(.)30 b(Let)15 b Fp(f)21 b Fx(and)15 b Fp(g)i Fx(b)q(e)e(giv)o(en.)h (Consider)f(the)h(set)627 1358 y Fp(M)i Fx(:=)13 b Fl(f)p Fp(x)8 b Fl(j)g(8)p Fp(y)13 b Fl(\025)g Fp(x:)8 b(f)d Fx(\()p Fp(y)r Fx(\))11 b Fl(6)p Fp(<)i(f)5 b Fx(\()p Fp(x)p Fx(\))p Fl(g)p Fp(:)266 1551 y Fx(1.)17 b Fp(M)f Fx(is)c(not)e(empt)o(y)h(b)q(ecause)h Fp(f)17 b Fx(has)11 b(a)f(global)i(minim)o(um)g(\(Use)f(the)g(minim)o(um)319 1605 y(principle)18 b(with)e Fp(P)6 b Fx(\()p Fp(x)p Fx(\))12 b(:)p Fl(\021)h(>)i Fx(and)h Fp(m)c Fx(:)p Fl(\021)h Fp(f)5 b Fx(\).)266 1702 y(2.)17 b(There)f(is)g(an)g Fp(i)d Fl(2)h Fp(M)21 b Fx(minimal)c(w.r.t.)d Fp(g)r Fx(,)h(i.e.)g Fl(8)p Fp(y)10 b Fx(\()p Fp(g)r Fx(\()p Fp(y)r Fx(\))i Fp(<)i(g)r Fx(\()p Fp(i)p Fx(\))e Fl(!)i Fp(y)h Fl(62)f Fp(M)5 b Fx(\))319 1756 y(\(Apply)16 b(the)f(minim)o(um) i(principle)h(at)c Fp(P)6 b Fx(\()p Fp(x)p Fx(\))13 b(:)p Fl(\021)f Fp(x)h Fl(2)g Fp(M)20 b Fx(and)15 b Fp(m)e Fx(:)p Fl(\021)g Fp(g)r Fx(\).)266 1852 y(3.)k(By)11 b(a)g(third)h(application)h(of)e(the)g(minim)o(um)i(principle)h(with)d Fp(P)6 b Fx(\()p Fp(x)p Fx(\))13 b(:)p Fl(\021)f Fp(x)h(>)g(i)319 1906 y Fx(and)i Fp(m)e Fx(:)p Fl(\021)g Fp(f)20 b Fx(w)o(e)15 b(obtain)g(an)g(elemen)o(t)h Fp(j)f(>)e(i)p Fx(,)i(s.t.)f Fl(8)p Fp(y)g(>)f(i:)8 b(f)d Fx(\()p Fp(y)r Fx(\))11 b Fl(6)p Fp(<)i(f)5 b Fx(\()p Fp(j)s Fx(\))p Fp(:)243 2001 y Fx(No)o(w,)13 b Fp(i)h Fx(and)g Fp(j)i Fx(are)e(as)g(desired:)h Fp(f)5 b Fx(\()p Fp(j)s Fx(\))11 b Fl(6)p Fp(<)i(f)5 b Fx(\()p Fp(i)p Fx(\))14 b(b)q(ecause)h Fp(i)d Fl(2)h Fp(M)5 b Fx(,)14 b(and,)g(using)g(the)243 2055 y(minimalit)o(y)k(of)e Fp(i)p Fx(,)g(for)g(pro)o(ving)h Fp(g)r Fx(\()p Fp(j)s Fx(\))c Fl(6)p Fp(<)i(g)r Fx(\()p Fp(i)p Fx(\))g(it)i(su\016ces)g(to)f (sho)o(w)g Fp(j)i Fl(2)d Fp(M)5 b Fx(,)16 b(i.e.)243 2109 y Fl(8)p Fp(y)f Fl(\025)e Fp(j)c(f)c Fx(\()p Fp(y)r Fx(\))12 b Fl(6)p Fp(<)h(f)5 b Fx(\()p Fp(j)s Fx(\))p Fp(:)14 b Fx(But)h(this)h(holds)g(b)o(y)f(minimalit)o(y)i(of)e Fp(j)i Fx(and)e(since)i Fp(i)12 b(<)h(j)s Fx(.)301 2218 y(T)l(o)j(transform)g(this)h(pro)q(of)f(in)o(to)h(a)f(constructiv)o(e)h (one)g(w)o(e)g(ha)o(v)o(e)f(to)g(lo)q(ok)h(at)243 2272 y(the)g(set)g(of)g(form)o(ulas)g Fp(L)g Fx(steering)g(the)h (translation.)f(Here,)g(it)g(consists)h(of)e(the)243 2326 y(k)o(ernel)g(of)f(the)g(wrong)f(assumption)458 2424 y Fp(u)p Fx(:)22 b Fl(8)p Fp(i;)8 b(j:)14 b(i)e(<)h(j)i Fl(!)e Fp(f)5 b Fx(\()p Fp(j)s Fx(\))12 b Fl(6)p Fp(<)h(f)5 b Fx(\()p Fp(i)p Fx(\))12 b Fl(!)h Fp(g)r Fx(\()p Fp(j)s Fx(\))d Fl(6)p Fp(<)j(g)r Fx(\()p Fp(i)p Fx(\))e Fl(!)i(?)p Fp(:)892 2924 y Fm(finaljar2.)o(tex)o(;)j(29/01/2001;)g(14:37;)h(p.14)p eop pstopssaved restore %%Page: pstops 8 /pstopssaved save def pstopsmatrix setmatrix 708.661417 0.000000 translate 90 rotate 0.880000 dup scale /pstopsmatrix matrix currentmatrix def initclip pstopsxform concat /showpage{}def/copypage{}def/erasepage{}def 15 14 bop 772 50 a Fo(W)m(arshall)10 b(and)g(Dic)o(kson)482 b Fx(15)243 145 y(and)15 b(the)g(k)o(ernels)h(of)f(the)g (\005-assumptions,)h(tacitly)f(used)h(in)g(the)f(pro)q(of)g(ab)q(o)o(v) o(e)642 240 y Fp(C)675 247 y Fo(1)694 240 y Fx(:)50 b Fp(x)12 b Fl(\024)h Fp(y)i Fl(!)e Fp(x)f(<)h(y)642 306 y(C)675 313 y Fo(2)694 306 y Fx(:)50 b Fp(x)12 b(<)h(y)i Fl(!)e Fp(y)h Fl(\024)f Fp(z)i Fl(!)e Fp(x)g(<)g(z)r(:)243 400 y Fx(F)l(urthermore)i(in)i(the)g(pro)q(of)e(of)h(the)g(minim)o(um)h (principle)i(\(omitted\))d(one)g(use)243 454 y(the)f(assumptions)609 548 y Fp(C)642 555 y Fo(3)661 548 y Fx(:)50 b Fp(x)12 b(<)h(y)i Fl(!)e Fp(y)h(<)f(z)g Fx(+)d(1)i Fl(!)i Fp(x)e(<)h(z)609 615 y(C)642 622 y Fo(4)661 615 y Fx(:)50 b Fl(:)p Fp(x)13 b(<)g Fx(0)243 709 y(whic)o(h)19 b(also)g(ha)o(v)o(e)f(to)g(b)q(e)h (tak)o(en)f(in)o(to)g(accoun)o(t.)g(Clearly)h(the)g(only)g Fp(L)p Fx(-critical)243 763 y(relation)c(sym)o(b)q(ol)g(is)g Fl(?)p Fx(.)f(Therefore)h Fp(C)910 770 y Fo(4)929 763 y Fx(:)f Fl(:)p Fp(n)f(<)g Fx(0)h(and)h(the)f(wrong)g(assumption)243 817 y Fp(u)e Fx(are)h(the)f(only)i(assumptions)e(a\013ected)h(b)o(y)f (the)h(translation.)f(W)l(e)h(do)g(not)f(sho)o(w)243 871 y(the)k(constructiv)o(e)h(pro)q(of,)e(since)j(despite)f(its)f (computational)h(con)o(ten)o(t)f(it)g(is)h(of)243 925 y(no)e(in)o(terest)g(here.)243 1032 y(6.2.)30 b Fr(The)17 b(extra)o(cted)h(pr)o(ogram)243 1129 y Fx(The)j(program)g(extracted)g (from)g(the)g(constructiv)o(e)h(pro)q(of)f(dep)q(ends)i(on)e(the)243 1183 y(pro)q(of)16 b(of)h(the)f(minim)o(um)i(principle)i(whic)o(h)e(in) f(turn)g(can)g(b)q(e)g(pro)o(v)o(ed)g(b)o(y)f(zero-)243 1237 y(successor)h(induction.)i(Since)g(w)o(e)f(ha)o(v)o(e)f(used)h (the)f(minim)o(um)i(principle)h(three)243 1291 y(times,)15 b(w)o(e)f(obtain)h(a)g(program)e(con)o(taining)j(three)f(nested)g (subroutines)h(called)243 1345 y(\010)p Fp(;)8 b Fx(\011)19 b(and)g(\004.)h(F)l(or)f(b)q(etter)g(readabilit)o(y)i(w)o(e)e (informally)i(comm)o(unicate)f(them)243 1399 y(via)e(recursion)g (equations.)f(The)h(program)f(tak)o(es)f(t)o(w)o(o)g(functions)j Fp(f)j Fx(and)c Fp(g)h Fx(as)243 1453 y(inputs)i(\(notationally)g (suppressed\))f(and)h(returns)f(a)g(pair)h Fp(i)g(<)g(j)i Fx(suc)o(h)d(that)243 1507 y Fp(f)5 b Fx(\()p Fp(i)p Fx(\))12 b Fl(\024)h Fp(f)5 b Fx(\()p Fp(j)s Fx(\))14 b(and)h Fp(g)r Fx(\()p Fp(i)p Fx(\))c Fl(\024)i Fp(g)r Fx(\()p Fp(j)s Fx(\).)301 1610 y(extracted-solution)j(=)f(\010\()p Fp(f)5 b Fx(\(0\))k(+)i(1\)\(0\),)i(where)243 1688 y(\010:)8 b Fg(nat)k Fl(!)h Fx(\()p Fg(nat)g Fl(!)g Fg(nat)e Fl(\002)g Fg(nat)p Fx(\))681 1782 y(\010\(0\)\()p Fp(i)p Fx(\))22 b(=)k Fg(dummy)620 1849 y Fx(\010\()p Fp(k)q Fx(+1\)\()p Fp(i)p Fx(\))d(=)j(\011\()p Fp(g)r Fx(\()p Fp(i)p Fx(\)+)n(1)p Fp(;)8 b(i;)g Fx(\010\()p Fp(k)q Fx(\)\))243 1943 y(Here)17 b Fg(dummy)o Fx(:)8 b Fg(nat)j Fl(\002)h Fg(nat)17 b Fx(is)g(some)g(arbitrary)f(term)g(extracted)g(from)g(an)h(Efq-)243 1997 y(Axiom.)243 2075 y(\011:)8 b Fg(nat)13 b Fl(!)g Fg(nat)g Fl(!)g Fx(\()p Fg(nat)g Fl(!)g Fg(nat)e Fl(\002)g Fg(nat)p Fx(\))i Fl(!)g Fg(nat)e Fl(\002)f Fg(nat)618 2169 y Fx(\011\(0)p Fp(;)e(i;)g(h)p Fx(\))22 b(=)j Fg(dummy)568 2236 y Fx(\011\()p Fp(l)q Fx(+1)p Fp(;)8 b(i;)g(h)p Fx(\))22 b(=)j(\004)908 2243 y Fi(l;i;h)974 2236 y Fx(\()p Fp(f)5 b Fx(\()p Fp(i)p Fx(+)o(1\)+1\)\()p Fp(i)p Fx(+)o(1\))243 2330 y(\004:)j Fg(nat)13 b Fl(!)g Fg(nat)g Fl(!)g Fx(\()p Fg(nat)g Fl(!)g Fg(nat)e Fl(\002)g Fg(nat)p Fx(\))i Fl(!)g Fg(nat)g Fl(!)g Fg(nat)h Fl(!)f Fg(nat)d Fl(\002)h Fg(nat)580 2424 y Fx(\004)610 2431 y Fi(l;i;h)675 2424 y Fx(\(0\)\()p Fp(j)s Fx(\))23 b(=)i Fg(dummy)892 2924 y Fm(finaljar2.)o(tex)o(;)16 b(29/01/2001;)g(14:37;)h(p.15)p eop pstopssaved restore /pstopssaved save def pstopsmatrix setmatrix 708.661417 368.503937 translate 90 rotate 0.880000 dup scale /pstopsmatrix matrix currentmatrix def initclip pstopsxform concat 16 15 bop 243 50 a Fx(16)504 145 y(\004)534 152 y Fi(l;i;h)600 145 y Fx(\()p Fp(m)p Fx(+1\)\()p Fp(j)s Fx(\))23 b(=)i Fg(if)116 b Fp(g)r Fx(\()p Fp(j)s Fx(\))11 b Fp(<)i(g)r Fx(\()p Fp(i)p Fx(\))875 212 y Fg(then)47 b Fx(\011\()p Fp(l)q(;)8 b(j;)g Fx(\004)1163 219 y Fi(l;i;h)1226 212 y Fx(\()p Fp(m)p Fx(\)\))875 278 y Fg(else)69 b(if)116 b Fp(f)5 b Fx(\()p Fp(j)s Fx(\))12 b Fp(<)h(f)5 b Fx(\()p Fp(i)p Fx(\))1011 345 y Fg(then)47 b Fp(h)p Fx(\()p Fp(j)s Fx(\))1011 411 y Fg(else)69 b Fx(\()p Fp(i;)8 b(j)s Fx(\))243 536 y Fj(R)n(emarks)t Fx(.)45 b(1.)22 b(The)h(program)e(ab)q(o)o(v)o(e) i(can)g(b)q(e)g(optimized)i(b)o(y)d(suppressing)243 590 y(the)h(recursion)g(parameters)f Fp(k)q Fx(,)g Fp(l)h Fx(and)g Fp(m)g Fx(whic)o(h)g(serv)o(e)g(only)g(as)f(coun)o(ters.)243 644 y(F)l(urthermore)15 b({as)h(w)o(e)f(will)j(argue)e(b)q(elo)o(w{)g (the)g(zero)g(cases)g(ma)o(y)f(b)q(e)i(omitted.)243 698 y(W)l(e)e(get)g(the)301 779 y(optimized-solution)i(=)f Fp(\036)p Fx(\(0\),)e(where)633 877 y Fp(\036)p Fx(\()p Fp(i)p Fx(\))24 b(=)i Fp( )r Fx(\()p Fp(i;)8 b(\036)p Fx(\))583 943 y Fp( )r Fx(\()p Fp(i;)g(h)p Fx(\))22 b(=)k Fp(\030)817 950 y Fi(i;h)861 943 y Fx(\()p Fp(i)9 b Fx(+)i(1\))591 1010 y Fp(\030)611 1017 y Fi(i;h)655 1010 y Fx(\()p Fp(j)s Fx(\))23 b(=)j Fg(if)116 b Fp(g)r Fx(\()p Fp(j)s Fx(\))11 b Fp(<)i(g)r Fx(\()p Fp(i)p Fx(\))797 1076 y Fg(then)47 b Fp( )r Fx(\()p Fp(j;)8 b(\030)1036 1083 y Fi(i;h)1078 1076 y Fx(\))797 1142 y Fg(else)68 b(if)117 b Fp(f)5 b Fx(\()p Fp(j)s Fx(\))11 b Fp(<)i(f)5 b Fx(\()p Fp(i)p Fx(\))933 1209 y Fg(then)47 b Fp(h)p Fx(\()p Fp(j)s Fx(\))933 1275 y Fg(else)69 b Fx(\()p Fp(i;)8 b(j)s Fx(\))301 1373 y(This)k(optimized)g(solution)g(can)f(also)g(b)q(e)h(extracted)f (directly)h(from)f(the)g(pro)q(of)243 1427 y(as)20 b(follo)o(ws:)g (Observ)o(e)h(that)f(the)g(minim)o(um)i(principle)h(immediately)f (follo)o(ws)243 1481 y(from)14 b(the)i(principle)i(of)c(w)o(ellfounded) j(induction)g(w.r.t.)d(a)h(measure)g Fp(m)p Fx(:)448 1579 y Fl(8)p Fp(x)p Fx(\()p Fl(8)p Fp(y)r Fx(\()p Fp(m)p Fx(\()p Fp(y)r Fx(\))d Fp(<)h(m)p Fx(\()p Fp(x)p Fx(\))f Fl(!)h Fp(P)6 b Fx(\()p Fp(y)r Fx(\)\))12 b Fl(!)h Fp(P)6 b Fx(\()p Fp(x)p Fx(\)\))12 b Fl(!)h(8)p Fp(xP)6 b Fx(\()p Fp(x)p Fx(\))243 1677 y(In)12 b(the)g(pro)q(of)f(ab)q(o)o(v)o(e)g(this) h(principle)j(w)o(as)c(reduced)h(to)f(ordinary)h(zero-successor)243 1731 y(induction,)j(and)e(hence)i(realized)g(b)o(y)e(a)g(primitiv)o(e)i (recursiv)o(e)f(functional.)g(Ho)o(w-)243 1785 y(ev)o(er)h(it)h(is)g (also)g(p)q(ossible)h(to)e(realize)i(w)o(ellfounded)h(induction)f (directly)g(b)o(y)e(the)243 1838 y(recursiv)o(e)h(functional)620 1936 y Fl(R)659 1943 y Fi(\034)693 1936 y Fx(:)c(\()p Fg(nat)h Fl(!)h Fg(nat)f Fl(!)g Fp(\034)5 b Fx(\))12 b Fl(!)h Fg(nat)h Fl(!)f Fp(\034)k Fx(:)620 2003 y Fl(R)p Fp(hx)c Fx(=)g Fp(hx)p Fx(\()p Fl(R)p Fp(h)p Fx(\))243 2100 y(Although)f Fl(R)479 2107 y Fi(\034)511 2100 y Fx(formally)g(is)f(not)g(primitiv)o(e)i(recursiv)o(e)f(and)f(ev)o(en)h (is)g(not)f(total)g(\(!\))243 2154 y(it)f(can)h(b)q(e)g(easily)h(seen)f (to)f(realize)h(w)o(ellfounded)i(induction.)f(Moreo)o(v)o(er)d(it)h (can)h(b)q(e)243 2208 y(sho)o(wn)k(that)g(in)i(an)o(y)e(extracted)h (program)e(this)i(realizer)h(ma)o(y)e(b)q(e)i(substituted)243 2262 y(for)j(the)h(primitiv)o(e)h(recursiv)o(e)g(realizer)g(of)e(w)o (ellfounded)j(induction)g(without)243 2316 y(c)o(hanging)13 b(the)h(input-output)g(b)q(eha)o(vior)g(of)f(the)g(program)f(\(but)h(p) q(ossibly)i(mak-)243 2370 y(ing)f(it)h(more)e(e\016cien)o(t\).)h(In)h (our)e(example)i(this)g(replacemen)o(t)f(results)h(precisely)243 2424 y(in)h(the)f(optimized)i(solution)f(sho)o(wn)f(ab)q(o)o(v)o(e.)892 2924 y Fm(finaljar2.)o(tex)o(;)h(29/01/2001;)g(14:37;)h(p.16)p eop pstopssaved restore %%Page: pstops 9 /pstopssaved save def pstopsmatrix setmatrix 708.661417 0.000000 translate 90 rotate 0.880000 dup scale /pstopsmatrix matrix currentmatrix def initclip pstopsxform concat /showpage{}def/copypage{}def/erasepage{}def 17 16 bop 772 50 a Fo(W)m(arshall)10 b(and)g(Dic)o(kson)482 b Fx(17)301 145 y(2.)12 b(Because)i(of)f(its)h(second-order)f (sub-program)g Fp(\030)i Fx(the)f(extracted)f(program)243 199 y Fp(\036)19 b Fx(is)g(probably)g(not)g(easy)g(to)f(understand.)h (Ho)o(w)o(ev)o(er)f(one)h(can)g(transform)e(it)243 253 y(in)o(to)e(the)g(follo)o(wing)h(more)f(transparen)o(t)f(\014rst-order) h(iterativ)o(e)g(program.)301 332 y(mo)q(di\014ed-solution)i(=)c Fg(mo)q(d)p Fx(\()p Fp(";)8 b Fx(0)p Fp(;)g Fx(1\),)k(where)345 428 y Fg(mo)q(d)p Fx(\()p Fp(s;)c(i;)g(j)s Fx(\))22 b(=)j Fg(if)117 b Fp(g)r Fx(\()p Fp(j)s Fx(\))10 b Fp(<)j(g)r Fx(\()p Fp(i)p Fx(\))648 494 y Fg(then)47 b(mo)q(d)p Fx(\()p Fp(s)10 b Fl(\003)g Fp(i;)e(j;)g(j)i Fx(+)g(1\))648 560 y Fg(else)69 b(if)117 b Fp(f)5 b Fx(\()p Fp(j)s Fx(\))11 b Fp(<)i(f)5 b Fx(\()p Fp(i)p Fx(\))784 627 y Fg(then)48 b(if)116 b Fp(s)13 b Fx(=)g Fp(")916 693 y Fg(then)47 b(mo)q(d)o Fx(\()p Fp(";)8 b(j;)g(j)j Fx(+)f(1\))916 760 y Fg(else)69 b(mo)q(d)o Fx(\()p Fg(lead)p Fx(\()p Fp(s)p Fx(\))p Fp(;)8 b Fg(last)p Fx(\()p Fp(s)p Fx(\))p Fp(;)g(j)s Fx(\))784 826 y Fg(else)69 b Fx(\()p Fp(i;)8 b(j)s Fx(\))243 922 y(Here)22 b Fp(s)g Fx(runs)h(o)o(v)o(er)e(\014nite) i(sequences)g(of)f(natural)g(n)o(um)o(b)q(ers,)g Fp(s)15 b Fl(\003)g Fp(i)21 b Fx(denotes)243 976 y Fp(s)e Fx(with)g Fp(i)f Fx(attac)o(hed)h(at)f(the)h(end,)g(and)g Fg(last)p Fx(\()p Fp(s)p Fx(\))g(and)g Fg(lead)p Fx(\()p Fp(s)p Fx(\))g(denote)g(the)g(last)243 1029 y(elemen)o(t)13 b(of)g Fp(s)g Fx(and)g Fp(s)g Fx(without)g(the)g(last)g(elemen)o(t)h (resp)q(ectiv)o(ely)l(.)g(W)l(e)f(emphasize)243 1083 y(that)19 b(neither)j(for)e(a)g(correctness)g(pro)q(of)g(nor)g(for)g (e\016ciency)i(reasons)e(is)h(this)243 1137 y(transformation)14 b(necessary)l(.)301 1241 y(3.)h(Note)h(that,)f(of)h(course,)g(already)h (the)f Fj(classic)n(al)e Fx(pro)q(of)i(tells)i(us)e(that)f(the)243 1295 y(systematic)e(searc)o(h)g(for)g(a)g(pair)h(\()p Fp(i;)8 b(j)s Fx(\))j(suc)o(h)i(that)g Fp(f)5 b Fx(\()p Fp(j)s Fx(\))12 b Fl(6)p Fp(<)h(f)5 b Fx(\()p Fp(i)p Fx(\))12 b(and)i Fp(g)r Fx(\()p Fp(j)s Fx(\))c Fl(6)p Fp(<)j(g)r Fx(\()p Fp(i)p Fx(\))243 1349 y(will)j(b)q(e)g(successful.)g (Ho)o(w)o(ev)o(er,)d(suc)o(h)j(a)e(brute)h(force)g(searc)o(h)g(program) f(do)q(esn't)243 1403 y(use)g(an)o(y)g(information)g(giv)o(en)g(b)o(y)g (the)g(pro)q(of)f(whereas)h(the)g(extracted)g(program)243 1457 y(do)q(es)j(and)g(hence)i(has)e(a)f(c)o(hance)i(to)e(b)q(e)i (`more)e(e\016cien)o(t'.)h(Exp)q(erimen)o(ts)h(with)243 1511 y(random)d(sequences)i(ha)o(v)o(e)e(con\014rmed)i(this,)f(ev)o(en) g(though)f(a)h(precise)h(analysis)243 1565 y(of)d(the)g(e\016ciency)i (of)d(the)i(extracted)f(program)f(remains)h(to)g(b)q(e)h(done.)f(It)g (is)h(not)243 1619 y(ev)o(en)h(clear)h(what)f(notion)h(of)e (e\016ciency)j(should)f(b)q(e)g(used)g(for)f(programs)f(with)243 1673 y(in\014nite)i(sequences)f(as)f(inputs.)301 1777 y(4.)i(In)i(order)f(to)g(obtain)g(a)g(go)q(o)q(d)g(program)g(from)f (our)h(pro)q(of)g(of)g(Dic)o(kson's)243 1831 y(Lemma)d(w)o(e)h(had)f (to)g(b)q(e)h(v)o(ery)g(careful)g(in)g(form)o(ulating)g(the)f (assertion:)g(for)g(ex-)243 1885 y(ample)d(instead)g(of)g Fl(\024)g Fx(w)o(e)f(had)h(to)f(use)h Fl(6)p Fp(>)p Fx(.)g(W)l(e)f(hop) q(e)i(to)e(impro)o(v)o(e)g(our)h(extraction)243 1939 y(pro)q(cedure)h(suc)o(h)g(that)f(it)h(will)h(b)q(e)f(robust)g(w.r.t.)d (suc)o(h)j(c)o(hanges)g(and)g(allo)o(ws)f(the)243 1993 y(user)j(to)g(form)o(ulate)f(the)i(problem)g(in)g(a)e(most)h(natural)g (w)o(a)o(y)l(.)777 2154 y Fs(7.)36 b(Conclusion)243 2262 y Fx(In)19 b(recen)o(t)g(y)o(ears)f(quite)h(a)f(n)o(um)o(b)q(er)h(of)g (formal)f(systems)g(for)g(extracting)h(pro-)243 2316 y(grams)11 b(from)g(constructiv)o(e)h(and)f(non-constructiv)o(e)i(pro)q (ofs)e(ha)o(v)o(e)g(b)q(een)i(studied)243 2370 y(and)e(implemen)o(ted.) i(Ho)o(w)o(ev)o(er)d(not)h(so)g(man)o(y)g(in)o(teresting)h(examples)g (ha)o(v)o(e)e(b)q(een)243 2424 y(presen)o(ted)i(y)o(et,)e(whic)o(h)j(w) o(ould)f(sho)o(w)f(that)f(this)i(metho)q(d)g(migh)o(t)f(b)q(e)i(of)e (practical)892 2924 y Fm(finaljar2.)o(tex)o(;)16 b(29/01/2001;)g (14:37;)h(p.17)p eop pstopssaved restore /pstopssaved save def pstopsmatrix setmatrix 708.661417 368.503937 translate 90 rotate 0.880000 dup scale /pstopsmatrix matrix currentmatrix def initclip pstopsxform concat 18 17 bop 243 50 a Fx(18)243 145 y(in)o(terest)16 b(in)i(the)e(future.) g(With)h(this)g(pap)q(er)g(w)o(e)f(tried)h(to)f(do)h(one)f(step)h(in)g (this)243 199 y(direction)12 b(b)o(y)f(sho)o(wing)g(that)f(fairly)h (complicated)i(pro)q(ofs)d(can)h(b)q(e)h(treated)e(with-)243 253 y(out)17 b(problems)i(and)f(yield)i(go)q(o)q(d)d(results.)h(A)g (more)g(in)o(v)o(olv)o(ed)h(example,)f(done)243 307 y(recen)o(tly)c(in) h(the)f Fr(Minlog)g Fx(system,)f(is)h(the)g(extraction)g(of)g(the)g (normalization-)243 361 y(b)o(y-ev)m(aluation)h(algorithm)e(from)g(a)h (T)l(ait-st)o(yle)g(normalization)g(pro)q(of)f(\(Berger,)243 415 y(1993\).)21 b(Other)i(in)o(teresting)g(examples)h(of)e(program)f (extraction)i(ha)o(v)o(e)f(b)q(een)243 469 y(studied)16 b(b)o(y)e(the)h(group)f(around)h(Co)q(quand)g(\(see)g(e.g.)f(Co)q (quand)h(and)f(P)o(ersson,)243 523 y(1999\))21 b(in)i(a)f(t)o(yp)q(e)h (theoretic)f(con)o(text)g(and)h(b)o(y)f(Kohlen)o(bac)o(h)i(\(Kohlen)o (bac)o(h,)243 577 y(1996\))14 b(using)h(a)g(Dialectica-in)o (terpretation.)723 733 y Fs(Ac)o(kno)o(wledgemen)o(ts)243 838 y Fx(W)l(e)c(thank)h(H.)f(Benl)h(and)g(F.)f(Joac)o(himski)h(for)f (their)h(con)o(tributions)g(to)f(the)g(w)o(ork)243 892 y(rep)q(orted)20 b(in)i(this)f(pap)q(er)g(and)g(t)o(w)o(o)e(anon)o (ymous)h(referees)g(for)g(their)h(helpful)243 946 y(commen)o(ts.)817 1146 y Fs(References)243 1242 y Fu(Bates,)15 b(J.)f(L.)h(and)g(R.)g(L.) g(Constable:)h(1985,)f(`Pro)q(ofs)g(as)g(Programs'.)23 b Fw(A)o(CM)16 b(T)m(r)n(ansactions)301 1288 y(on)d(Pr)n(o)n(gr)n (amming)g(L)n(anguages)d(and)j(Systems)e Fv(7)p Fu(\(1\),)i(113{136.) 243 1333 y(Benl,)d(H.,)f(U.)f(Berger,)i(H.)f(Sc)o(h)o(wic)o(h)o(ten)o (b)q(erg,)i(M.)e(Seisen)o(b)q(erger,)j(and)e(W.)f(Zub)q(er:)i(1998,)f (`Pro)q(of)301 1379 y(theory)k(at)f(w)o(ork:)g(Program)h(dev)o(elopmen) o(t)i(in)e(the)f(Minlog)j(system'.)i(In:)13 b(W.)g(Bib)q(el)j(and)301 1424 y(P)m(.)j(Sc)o(hmitt)h(\(eds.\):)f Fw(A)o(utomate)n(d)d(De)n (duction)h({)i(A)g(Basis)f(for)h(Applic)n(ations)o Fu(,)d(V)m(ol.)j(I)q (I:)301 1470 y(Systems)g(and)f(Implemen)o(tation)j(T)m(ec)o(hniques)e (of)f Fw(Applie)n(d)e(L)n(o)n(gic)h(Series)p Fu(.)30 b(Dordrec)o(h)o(t:)301 1515 y(Klu)o(w)o(er)13 b(Academic)h(Publishers,) i(pp.)d(41{71.)243 1561 y(Benl,)20 b(H.)g(and)g(H.)f(Sc)o(h)o(wic)o(h)o (ten)o(b)q(erg:)j(1999,)e(`F)m(ormal)g(correctness)h(pro)q(ofs)f(of)g (functional)301 1606 y(programs:)13 b(Dijkstra's)g(algorithm,)h(a)e (case)h(study'.)j(In:)c(U.)g(Berger)h(and)g(H.)e(Sc)o(h)o(wic)o(h)o (ten-)301 1652 y(b)q(erg)k(\(eds.\):)f Fw(Computational)f(L)n(o)n(gic)p Fu(,)g(V)m(ol.)h(165)h(of)g Fw(Series)f(F:)h(Computer)f(and)g(Systems) 301 1697 y(Scienc)n(es)p Fu(.)c(pp.)j(113{126,)h(Springer)g(V)m(erlag,) g(Berlin,)g(Heidelb)q(erg,)h(New)d(Y)m(ork.)243 1742 y(Berger,)k(U.:)g(1993,)h(`Program)g(extraction)h(from)e(normalization) k(pro)q(ofs'.)28 b(In:)16 b(M.)g(Bezem)301 1788 y(and)11 b(J.)f(Gro)q(ote)h(\(eds.\):)f Fw(T)m(yp)n(e)n(d)h(L)n(amb)n(da)f (Calculi)h(and)f(Applic)n(ation)o(s)p Fu(,)d(V)m(ol.)k(664)g(of)f Fw(L)n(e)n(ctur)n(e)301 1833 y(Notes)f(in)g(Computer)h(Scienc)n(e)p Fu(.)c(pp.)k(91{106,)g(Springer)h(V)m(erlag,)f(Berlin,)h(Heidelb)q (erg,)g(New)301 1879 y(Y)m(ork.)243 1924 y(Berger,)e(U.)f(and)i(H.)e (Sc)o(h)o(wic)o(h)o(ten)o(b)q(erg:)j(1995,)f(`Program)f(Extraction)h (from)f(Classical)j(Pro)q(ofs'.)301 1970 y(In:)h(D.)g(Leiv)n(an)o(t)h (\(ed.\):)e Fw(L)n(o)n(gic)h(and)f(Computational)f(Complexity,)h (Internationa)o(l)f(Work-)301 2015 y(shop)i(LCC)j('94,)d(Indianap)n (oli)o(s,)f(IN,)h(USA,)g(Octob)n(er)h(1994)p Fu(,)e(V)m(ol.)i(960)g(of) g Fw(L)n(e)n(ctur)n(e)f(Notes)301 2061 y(in)f(Computer)g(Scienc)n(e)p Fu(.)d(pp.)j(77{97,)g(Springer)i(V)m(erlag,)e(Berlin,)h(Heidelb)q(erg,) h(New)d(Y)m(ork.)243 2106 y(Bro)o(y)m(,)h(M.)g(and)i(P)m(.)e(P)o(epp)q (er:)h(1981,)g(`Program)f(Dev)o(elopmen)o(t)j(as)e(a)f(F)m(ormal)i (Activit)o(y'.)j Fw(IEEE)301 2152 y(T)m(r)n(ans.)c(on)g(Softwar)n(e)f (Eng.)g Fv(7)p Fu(\(1\),)h(14{22.)243 2197 y(Co)q(quand,)22 b(T.)f(and)h(H.)f(P)o(ersson:)h(1999,)g(`Gr\177)-19 b(obner)23 b(Bases)f(in)g(T)o(yp)q(e)g(Theory'.)43 b(In:)21 b(T.)301 2242 y(Altenkirc)o(h,)e(W.)f(Narasc)o(hewski,)h(and)g(B.)e(Reus)i (\(eds.\):)e Fw(T)m(yp)n(es)g(for)h(Pr)n(o)n(ofs)f(and)g(Pr)n(o-)301 2288 y(gr)n(ams)p Fu(,)11 b(V)m(ol.)h(1657)h(of)f Fw(L)n(e)n(ctur)n(e)f (Notes)g(in)h(Computer)h(Scienc)n(e)p Fu(.)c(Springer)14 b(V)m(erlag,)e(Berlin,)301 2333 y(Heidelb)q(erg,)j(New)d(Y)m(ork.)243 2379 y(Dic)o(kson,)k(L.:)e(1913,)i(`Finiteness)h(of)d(the)i(o)q(dd)f(p) q(erfect)h(and)f(primitiv)o(e)j(abundan)o(t)e(n)o(um)o(b)q(ers)301 2424 y(with)d Fa(n)g Fu(distinct)i(prime)f(factors'.)j Fw(A)o(m.)c(J.)h(Math)e Fv(35)p Fu(,)h(413{422.)892 2924 y Fm(finaljar2.)o(tex)o(;)j(29/01/2001;)g(14:37;)h(p.18)p eop pstopssaved restore %%Page: pstops 10 /pstopssaved save def pstopsmatrix setmatrix 708.661417 0.000000 translate 90 rotate 0.880000 dup scale /pstopsmatrix matrix currentmatrix def initclip pstopsxform concat /showpage{}def/copypage{}def/erasepage{}def 19 18 bop 772 50 a Fo(W)m(arshall)10 b(and)g(Dic)o(kson)482 b Fx(19)243 145 y Fu(Dragalin,)20 b(A.:)d(1979,)h(`New)f(Kinds)i(of)e (Realizabil)q(i)q(t)o(y'.)34 b(In:)17 b Fw(A)o(bstr)n(acts)f(of)i(the)f (6th)g(Inter-)301 191 y(national)11 b(Congr)n(ess)h(of)h(L)n(o)n(gic,)g (Metho)n(dolo)n(gy)e(and)h(Philosophy)f(of)i(Scienc)n(es)p Fu(.)d(Hanno)o(v)o(er,)301 236 y(German)o(y)m(,)j(pp.)g(20{24.)243 282 y(F)m(riedman,)g(H.:)f(1978,)h(`Classically)j(and)d(in)o(tuitioni)q (stica)q(ll)q(y)j(pro)o(v)n(ably)e(recursiv)o(e)g(functions'.)301 327 y(In:)f(D.)g(Scott)g(and)h(G.)f(M)q(\177)-20 b(uller)15 b(\(eds.\):)e Fw(Higher)f(Set)h(The)n(ory)p Fu(,)f(V)m(ol.)h(669)h(of)f Fw(L)n(e)n(ctur)n(e)f(Notes)301 373 y(in)h(Mathematics)p Fu(.)d(pp.)j(21{28,)h(Springer)h(V)m(erlag,)e(Berlin,)h(Heidelb)q(erg,) h(New)d(Y)m(ork.)243 418 y(Kohlen)o(bac)o(h,)k(U.:)d(1996,)i (`Analysing)i(Pro)q(ofs)d(in)i(Analysis'.)23 b(In:)14 b(W.)g(Ho)q(dges,)h(M.)f(Hyland,)301 463 y(C.)20 b(Steinhorn,)i(and)g (J.)e(T)m(russ)h(\(eds.\):)f Fw(L)n(o)n(gic:)f(fr)n(om)i(F)m (oundations)d(to)i(Applic)n(ation)o(s.)301 509 y(Eur)n(op)n(e)n(an)9 b(L)n(o)n(gic)h(Col)r(lo)n(quium)g(\(Ke)n(ele,)g(1993\))p Fu(.)e(pp.)j(225{260,)g(Oxford)g(Univ)o(ersit)o(y)h(Press.)243 554 y(Kreisel,)17 b(G.:)e(1959,)i(`In)o(terpretation)g(of)f(analysis)j (b)o(y)d(means)h(of)f(constructiv)o(e)i(functionals)301 600 y(of)e(\014nite)i(t)o(yp)q(es'.)29 b(In:)16 b(A.)h(Heyting)g (\(ed.\):)g Fw(Constructivity)d(in)i(Mathematics)p Fu(.)26 b(North{)301 645 y(Holland,)15 b(Amsterdam,)d(pp.)i(101{128.)243 691 y(Leiv)n(an)o(t,)g(D.:)g(1985,)g(`Syn)o(tactic)h(T)m(ranslations)h (and)e(Pro)o(v)n(ably)i(Recursiv)o(e)f(F)m(unctions'.)21 b Fw(The)301 736 y(Journal)12 b(of)h(Symb)n(olic)f(L)n(o)n(gic)f Fv(50)p Fu(\(3\),)i(682{688.)243 782 y(Murth)o(y)m(,)i(C.:)f(1990,)h (`Extracting)i(Constructiv)o(e)f(Con)o(ten)o(t)g(from)e(Classical)k (Pro)q(ofs'.)23 b(T)m(ec)o(h-)301 827 y(nical)17 b(Rep)q(ort)f (90{1151,)h(Dep.of)f(Comp.Science,)g(Cornell)h(Univ.,)f(Ithaca,)g(New)f (Y)m(ork.)301 873 y(PhD)e(thesis.)243 918 y(Nash-Williams)q(,)24 b(C.)c(S.)i(J.)f(A.:)f(1963,)i(`On)g(w)o(ell{quasi{orderi)q(ng)j (\014nite)e(trees'.)42 b Fw(Pr)n(o)n(c.)301 963 y(Cambridge)12 b(Phil.)h(So)n(c.)f Fv(59)p Fu(,)g(833{835.)243 1009 y(Pfenning,)20 b(F.:)e(1990,)h(`Program)g(Dev)o(elopmen)o(t)h(Through)g (Pro)q(of)f(T)m(ransformation'.)35 b(In:)301 1054 y(W.)14 b(Sieg)h(\(ed.\):)e Fw(L)n(o)n(gic)g(and)h(Computation)p Fu(,)d(V)m(ol.)i(106)i(of)e Fw(Contemp)n(or)n(ary)g(Mathematics)p Fu(.)301 1100 y(Pro)o(vidence,)h(Rho)q(de)h(Island,)f(pp.)f(251{262,)h (AMS.)243 1145 y(T)m(ait,)c(W.)h(W.:)g(1967,)g(`In)o(tensional)i(In)o (terpretations)g(of)d(F)m(unctionals)k(of)c(Finite)j(T)o(yp)q(e)e(I'.)i Fw(The)301 1191 y(Journal)f(of)h(Symb)n(olic)f(L)n(o)n(gic)f Fv(32)p Fu(\(2\),)i(198{212.)243 1236 y(T)m(ro)q(elstra,)h(A.)g(S.:)f (1973,)i Fw(Metamathematic)n(al)c(Investigation)g(of)j(Intuitionist)o (ic)e(A)o(rithmetic)301 1282 y(and)f(A)o(nalysis)p Fu(,)d(V)m(ol.)j (344)g(of)g Fw(L)n(e)n(ctur)n(e)g(Notes)f(in)h(Mathematics)p Fu(.)h(Springer)h(V)m(erlag,)e(Berlin,)301 1327 y(Heidelb)q(erg,)k(New) d(Y)m(ork.)243 1373 y(T)m(ro)q(elstra,)g(A.)g(S.)g(and)h(D.)f(v)n(an)h (Dalen:)g(1988,)f Fw(Constructivism)f(in)h(Mathematics.)f(A)o(n)h(Intr) n(o-)301 1418 y(duction)p Fu(,)f(V)m(ol.)j(121,)f(123)i(of)e Fw(Studies)f(in)i(L)n(o)n(gic)g(and)f(the)g(F)m(oundations)e(of)j (Mathematics)p Fu(.)301 1463 y(North{Holland,)h(Amsterdam.)243 1509 y(V)m(eldman,)d(W.)g(and)h(M.)e(Bezem:)h(1993,)g(`Ramsey's)g (theorem)g(and)h(the)f(pigeonhole)i(principle)301 1554 y(in)g(in)o(tuitioni)q(stic)j(mathematics'.)h Fw(Journal)13 b(of)g(the)g(L)n(ondon)f(Mathematic)n(al)g(So)n(ciety)f Fv(47)p Fu(,)301 1600 y(193{211.)243 1700 y Fw(A)n(ddr)n(ess)g(for)j (O\013prints:)243 1746 y Fu(U.)e(Berger)243 1791 y(Departmen)o(t)i(of)e (Computer)i(Science)243 1837 y(Univ)o(ersit)o(y)h(of)d(W)m(ales)i(Sw)o (ansea)243 1882 y(Singleton)h(P)o(ark)243 1928 y(Sw)o(ansea)f(SA2)f (8PP)m(,)f(UK)243 2019 y(H.)g(Sc)o(h)o(wic)o(h)o(ten)o(b)q(erg,)j (Monik)n(a)f(Seisen)o(b)q(erger)243 2064 y(Mathematisc)o(hes)h (Institut)243 2110 y(der)e(Ludwig-Maximil)q(ia)q(ns-Uni)q(v)o(ersi)q (t\177)-19 b(at)16 b(M)q(\177)-20 b(unc)o(hen)243 2155 y(Theresienstra\031e)15 b(39)243 2200 y(80333)f(M)q(\177)-20 b(unc)o(hen,)14 b(German)o(y)892 2924 y Fm(finaljar2.)o(tex)o(;)i (29/01/2001;)g(14:37;)h(p.19)p eop pstopssaved restore /pstopssaved save def pstopsmatrix setmatrix 708.661417 368.503937 translate 90 rotate 0.880000 dup scale /pstopsmatrix matrix currentmatrix def initclip pstopsxform concat 20 19 bop 892 2924 a Fm(finaljar2.)o(tex)o(;)16 b(29/01/2001;)g(14:37;) h(p.20)p eop pstopssaved restore %%Trailer end userdict /end-hook known{end-hook}if %%EOF