%!PS-Adobe-2.0 %%Creator: dvipsk 5.58f Copyright 1986, 1994 Radical Eye Software %%Title: fcp.dvi %%Pages: 14 %%PageOrder: Ascend %%BoundingBox: 0 0 596 842 %%EndComments %DVIPSCommandLine: dvips fcp.dvi %DVIPSParameters: dpi=300, compressed, comments removed %DVIPSSource: TeX output 1999.03.08:1613 %%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 TeXDict begin 39158280 55380996 1000 300 300 (fcp.dvi) @start /Fa 45 123 df34 DI38 D<12301278127C123C121CA41238127812F012E01240060D789816>I<13E01201EA0380 EA0700120E5AA25AA25AA35AA91270A37EA27EA27E7EEA0380EA01E012000B217A9C16> I<12C07E12707E7E7EA27EA2EA0380A3EA01C0A9EA0380A3EA0700A2120EA25A5A5A5A5A 0A217B9C16>II<13E0A8B512E0A33800E000A813137F9516>I<1238127C 127EA2123E120E121E121C127812F01260070B798416>II<1270 12F8A312700505788416>I48 D<12035AA25A5AB4FCA212E71207AEEAFFF8A30D197B9816>II<127012F8A312701200A8127012F8A31270051278 9116>58 D60 DI<12C012F012FC123EEA0F806C7EEA01F06C7E133EEB1F80 1307131FEB3E0013F8485AEA07C0485A003EC7FC12FC12F012C011157E9616>I<387FFF E0B5FC7EEA1C00A41400A2131CA2EA1FFCA3EA1C1CA290C7FCA6EA7F80487E6C5A13197F 9816>70 D<387FFFE0B5FCA2EAE0E0A400001300AFEA07FC487E6C5A13197F9816>84 D91 D93 D95 D97 D<12FCA3121CA4137CEA1DFEEA1FFFEB0780381E03C0EA1C01EB00E0A6EB01C0EA1E0338 1F0780EBFF00EA1DFEEA0C7813197F9816>II<133FA31307A4EA03 C7EA0FF748B4FCEA3C1F487EEA700712E0A6EA700F12786C5A381FFFE0EA0FF7EA07C713 197F9816>II<131E137F3801FF8013C7380383 001380A2EA7FFFB5FCA2EA0380ACEA7FFC487E6C5A11197F9816>I<12FCA3121CA41378 EA1DFCEA1FFE130FEA1E07121CAA38FF8FE0139F138F13197F9816>104 D<1203EA0780A2EA0300C7FCA4EAFF80A31203ACEAFFFC13FE13FC0F1A7C9916>I<1330 1378A213301300A4EA0FF8121F120FEA0038B3EA6070EAF0F0EAFFE0EA7FC0EA3F800D23 7E9916>I<127E12FE127E120EA4EB7FE0A3EB0F00131E5B5B5B120F7F13BC131EEA0E0E 7F1480387F87F0EAFFCFEA7F871419809816>II<38F9C38038FFEFC0EBFFE0EA3C78A2EA3870AA38FE7CF8A31512 809116>II< EA03E0EA0FF8487EEA3C1E487EEA700738E00380A5EAF00700701300EA780FEA3C1EEA1F FC6C5AEA03E011127E9116>II<387F0F C038FF3FE0EA7F7F3807F040EBC0005BA290C7FCA8EA7FFC12FF127F13127F9116>114 DI<12035AA4EA7FFFB5FCA20007C7FCA75B EB0380A3EB8700EA03FE6C5A6C5A11177F9616>II<38FF1FE0A338380380A4EA39F3A20019130013B3A3EA1DB7 1317EA1F1FEA0F1EEA0E0E13127F9116>119 D<387F1FC0133F131F380F1E006C5AEA03 B813F012016C5A12017FEA03B8EA073C131CEA0E0E387F1FC038FF3FE0387F1FC013127F 9116>I<383FFFC05AA238700780EB0F00131EC65A5B485A485AEA078048C7FC381E01C0 123C1278B5FCA312127F9116>122 D E /Fb 3 110 df<121C1222126212FC12C0A212C2 12CC127007097D880B>101 D<12701230A31260A412C0A312E012C0A2040E7E8D06>108 DI E /Fc 2 81 df<141C143C14F8EB01E0EB03C0EB0780EB0F00130E131E5BA35BB3B3A25B A3485AA2485A5B48C7FC120E5A127812E0A21278121C7E7E6C7E7F6C7EA26C7EA31378B3 B3A27FA37F130E130FEB0780EB03C0EB01E0EB00F8143C141C167C7B8121>40 D80 D E /Fd 7 121 df99 D<12F0A41200A71270B204 1D7E9C0A>105 D<12E0AB133C137813F0EAE1E0EAE3C0EAE780EAEF00B4FC138012FBEA F9C0EAF1E012E013F013781338133C131E0F1D7D9C14>107 D110 D112 D<121CA6EAFFE0A2EA1C00AC1320EA1FF0120FEA07C00C187F970F>116 D<3870038038780700EA3C0EEA1C1C120E6C5AEA03F06C5A5B7F487EEA0738EA0618EA0E 1C487E487E3870038000F013C01212809113>120 D E /Fe 17 115 df<127812FCA4127806067D850D>46 D<1360EA01E0120F12FF12F31203B3A2387FFF80 A2111B7D9A18>49 DIII<3838018038 3FFF005B5B5B13C00030C7FCA4EA31F8EA361E38380F80EA3007000013C014E0A3127812 F8A214C012F038600F8038381F00EA1FFEEA07F0131B7E9A18>I<137EEA03FF38078180 380F03C0EA1E07123C387C03800078C7FCA212F813F8EAFB0E38FA0780EAFC0314C000F8 13E0A41278A214C0123CEB0780381E0F00EA07FEEA03F8131B7E9A18>I<1260387FFFE0 A214C01480A238E00300EAC0065B5BC65AA25B13E0A212015B1203A41207A66C5A131C7D 9B18>II76 D<007FB512E0A238781F81007013800060146000E0147000 C01430A400001400B03807FFFEA21C1C7E9B21>84 D97 D101 D104 D<39FF0FC07E903831E18F3A1F40F20780D980 FC13C0A2EB00F8AB3AFFE7FF3FF8A225127F9128>109 D111 D114 D E /Ff 18 118 df<123E1263EA0180121F127112C113A012C3EA3DC00B097E880E>97 D<121FEA2180EA400012C0A31240EA2080EA1F0009097E880D>99 DI<121E1261EA41 8012FFEAC000A21240EA2080EA1F0009097E880D>I<120FEA1980EA3000A312FE1230A7 12FC090E7F8D09>II<124012E012401200A312E01260A712F0040F7E8E08>105 D<1204120E12041200A3121E1206AA12C412780713818E09>I<12F01230A413F013C0EA 31001236123BEA3180EA30C013E0EAFCF80D0E7F8D0F>I<12E01260AC12F0040E7E8D08> I<38F7CF80383870C0EA3060A638FDFBF014097E8818>II<121EEA61801240EAC0C0A3EA40801261EA1E000A097E880E>II<12F7EA3980EA30 00A612FC09097F880B>114 D<127E1282A212F0123C1206128212C212BC07097E880B>I< 1210A21230A212FE1230A41231A3121E080D7F8C0B>II E /Fg 2 106 df<137C48B4FC380783C0380E00E000181330481318A248130C A2481306A50060130CA26C1318A26C1330000E13E0380783C03801FF00EA007C17178B8B 15>100 D105 D E /Fh 6 74 df<1720176017C0EE0180 EE030016065E5E5E5E5E4B5A4BC7FC15065D5D5D5D5D4A5A4AC8FC14065C5C5C5C5C495A 49C9FC13065B5B5B5B5B485A48CAFC12065A5A5A5A5A5A2B2C80AA2A>0 D<5A1380EA03C013E013F0EA07F813FC13FEEA0FFF13FCEA1FE01300123C127012601280 1010808F2A>9 D<13011306130E133C13F81207EA3FF012FFEA7FE0123F121FEA0FC012 071203EA01801200101066A92A>18 D<1302131E137EEA01FE120F12FFA2120F1201EA00 7E131E13020F0C7E852A>27 D<7E7E12607E7E7E7E7E6C7E6C7E13607F7F7F7F7F6D7E6D 7E146080808080806E7E6E7E156081818181816F7E6F7E16608282828282EE0180EE00C0 176017202B2C80AA2A>64 D<7E12601270123C121F13E0EA0FFC13FFEA07FE13FC13F8EA 03F013E013C0EA01801300101080A92A>73 D E /Fi 6 111 df<3907E01FC00000EB06 0038017004A21338A238021C08A2130EA2486C5AA2EB0390A2380801E0A21300A2001813 4012FE1A147F931A>78 D<38FF83F8381C00C0481380A438700100A4EAE002A4485AA25B EA6010EA3060EA1F8015147E9317>85 D97 D<1206120712061200A41238124CA2128C129812 18A212301232A21264A2123808147F930C>105 D<1330133813301300A4EA01C0EA0260 EA0430136012081200A213C0A4EA0180A4EA630012E312C612780D1A81930E>I110 D E /Fj 2 79 df<90387FFF800003B5FCD80780C7FC000CC8FC5A5AA25AA25AA81260A2 7EA27E120E6C7E0001B512806C7E90C8FCA3144014E0EB018049C7FC1306007FB51280A2 D80030C7FC5B5B485A48C8FC19297D9920>40 D<39FFE00FF83930100320390808014090 380400C0120CEA0E02EA0D01380C8080EB4040A2EB2020EB1010EB0808EB0404A2EB0202 EB0101EB0080EC40401420A2141014081404140200121301123339FFC000C0C812401D1D 809B20>78 D E /Fk 7 62 df<1360AAB512F0A238006000AA14167E9119>43 D<120FEA30C0EA6060A2EA4020EAC030A9EA4020EA6060A2EA30C0EA0F000C137E9211> 48 D<120C121C12EC120CAFEAFFC00A137D9211>I<121FEA60C01360EAF07013301260EA 0070A2136013C012011380EA02005AEA08101210EA2020EA7FE012FF0C137E9211>II<136013E0A2EA016012021206120C120812101220126012 C0EAFFFCEA0060A5EA03FC0E137F9211>I61 D E /Fl 28 123 df<130E131E137EEA07FE12FFA212F81200B3ABB512FEA317277BA622 >49 DII<121C127FA2EAFF80A3 EA7F00A2121CC7FCA9121C127FA2EAFF80A3EA7F00A2121C091B7B9A13>58 D<91387FE003903907FFFC07011FEBFF0F90397FF00F9F9039FF0001FFD801FC7F484814 7F4848143F4848141F485A160F485A1607127FA290C9FC5AA97E7F1607123FA26C7E160E 6C7E6C6C141C6C6C143C6C6C14786CB4EB01F090397FF007C0011FB512800107EBFE0090 38007FF028297CA831>67 DI82 D<9038FF80600003EBF0E0000F13F8381F80FD383F001F003E1307481303A200FC1301A2 14007EA26C140013C0EA7FFCEBFFE06C13F86C13FE80000714806C14C0C6FC010F13E0EB 007FEC1FF0140F140700E01303A46C14E0A26C13076C14C0B4EB0F80EBE03F39E3FFFE00 00E15B38C01FF01C297CA825>I<007FB71280A39039807F807FD87C00140F00781507A2 0070150300F016C0A2481501A5C791C7FCB3A490B612C0A32A287EA72F>I<3803FF8000 0F13F0381F01FC383F80FE147F801580EA1F00C7FCA4EB3FFF3801FC3FEA0FE0EA1F80EA 3F00127E5AA4145F007E13DF393F839FFC381FFE0F3803FC031E1B7E9A21>97 D99 D101 DI<9038FF80F00003EBE3F8390FC1 FE1C391F007C7C48137E003EEB3E10007EEB3F00A6003E133E003F137E6C137C380FC1F8 380BFFE00018138090C8FC1238A2123C383FFFF814FF6C14C06C14E06C14F0121F383C00 07007CEB01F8481300A4007CEB01F0A2003FEB07E0390FC01F806CB5120038007FF01E28 7E9A22>II<1207EA0F80EA1FC0EA3FE0A3EA1FC0EA0F80 EA0700C7FCA7EAFFE0A3120FB3A3EAFFFEA30F2B7EAA12>I<1307EB0F80EB1FC0EB3FE0 A3EB1FC0EB0F80EB070090C7FCA7EBFFE0A3130FB3AA127C12FE14C0EB1F801400EA7C3E EA3FFCEA0FF0133784AA15>III<26FFC07FEB 1FC0903AC1FFC07FF0903AC307E0C1F8D80FC49038F101FC9039C803F20001D801FE7F01 D05BA201E05BB03CFFFE3FFF8FFFE0A3331B7D9A38>I<38FFC07E9038C1FF809038C30F C0D80FC413E0EBC80701D813F013D0A213E0B039FFFE3FFFA3201B7D9A25>II<38FFE1FE9038EFFF809038FE0FE0390FF803F09038F001F801E013FC140015FEA215 7FA8157E15FEA215FC140101F013F89038F807F09038FC0FE09038EFFF809038E1FC0001 E0C7FCA9EAFFFEA320277E9A25>I<38FFC1F0EBC7FCEBC63E380FCC7F13D813D0A2EBF0 3EEBE000B0B5FCA3181B7F9A1B>114 D<3803FE30380FFFF0EA3E03EA7800127000F013 70A27E00FE1300EAFFE06CB4FC14C06C13E06C13F0000713F8C6FCEB07FC130000E0137C 143C7E14387E6C137038FF01E038E7FFC000C11300161B7E9A1B>I<13E0A41201A31203 A21207120F381FFFE0B5FCA2380FE000AD1470A73807F0E0000313C03801FF8038007F00 14267FA51A>I<39FFE07FF0A3000F1307B2140FA2000713173903F067FF3801FFC73800 7F87201B7D9A25>I<003FB5FCA2EB00FEEA3C01383803FC007813F8EB07F0EA700F14E0 EB1FC0EA003F1480EB7F005B5B3801FC07120313F8EA07F0000F130F13E0381FC00E003F 131E387F803EEB00FEB5FCA2181B7E9A1E>122 D E /Fm 13 117 df68 D77 D<13201370A313B8A3EA011CA2EA031E EA020EA2487EEA07FFEA040738080380A2001813C01301123838FC07F815157F9419>97 D103 D105 DI<38FF81F8 381C01E01480140013025B5B5B1330137013B8EA1D1C121EEA1C0E7F14801303EB01C014 E014F038FF83FC16157F941A>II<38FC03F8381E00E014401217EA138013C01211EA10E01370A21338131CA2130E 130714C0130313011300123800FE134015157F9419>110 DI114 DI<387FFFF03860703000401310A200 801308A300001300ADEA07FF15157F9419>I E /Fn 3 51 df0 D<1204A3EAC460EAF5E0EA3F80EA0E00EA3F80EAF5E0EAC460EA0400A30B0D7E8D11>3 D50 D E /Fo 25 122 df<126012F0A2126004047C830C>58 D<126012F0A212701210A41220A212401280040C7C830C>II<130113031306A3130CA313 18A31330A31360A213C0A3EA0180A3EA0300A31206A25AA35AA35AA35AA35AA210297E9E 15>I<140CA2141CA2143C145CA2149E148EEB010E1302A21304A213081310A2497EEB3F FFEB40071380A2EA0100A212025AA2001C148039FF803FF01C1D7F9C1F>65 D<48B5FC39003C01C090383800E015F01570A25B15F0A2EC01E09038E003C0EC0780EC1F 00EBFFFC3801C00FEC0780EC03C0A2EA0380A439070007801500140E5C000E1378B512C0 1C1C7E9B1F>I<903801F80890380E0618903838013890386000F048481370485A48C712 30481420120E5A123C15005AA35AA45CA300701302A200305B00385B6C5B6C1360380701 80D800FEC7FC1D1E7E9C1E>I<48B512F839003C0078013813181510A35BA21408150049 5AA21430EBFFF03801C020A4390380404014001580A23907000100A25C1406000E133EB5 12FC1D1C7E9B1F>69 D78 DI<397FF03FE0390F00 0700000E13061404A3485BA4485BA4485BA4485BA35CA249C7FCEA60025B6C5AEA1830EA 07C01B1D7D9B1C>85 D<39FFC00FF0391C00038015001402A25C5C121E000E5B14301420 5CA25C49C7FC120FEA07025BA25BA25B5BEA03A013C05BA290C8FCA21C1D7D9B18>I97 D<123F1207A2120EA45AA4EA39E0EA3A30EA3C1812381270131CA3EAE038 A313301370136013C01261EA2300121E0E1D7E9C12>III102 D105 D<1307130FA213061300A61378139CEA010C1202 131C12041200A21338A41370A413E0A4EA01C01261EAF180EAF30012E6127C1024809B11 >I<39381F81F0394E20C618394640E81CEB80F0EA8F00008E13E0120EA2391C01C038A3 15703938038071A215E115E23970070064D83003133820127E9124>109 DI<380787803809C8603808D03013E0EA11C014 381201A238038070A31460380700E014C0EB0180EB8300EA0E86137890C7FCA25AA4123C B4FC151A819115>112 D<001CEBC080392701C1C0124714C03987038040A2120EA2391C 070080A3EC0100EA1806A2381C0E02EB0F04380E13083803E1F01A127E911E>119 D<380787803808C8403810F0C03820F1E0EBE3C03840E1803800E000A2485AA438638080 12F3EB810012E5EA84C6EA787813127E9118>I<001C13C0EA27011247A238870380A212 0EA2381C0700A4EA180EA3EA1C1EEA0C3CEA07DCEA001C1318EA6038EAF0305B485AEA41 80003EC7FC121A7E9114>I E /Fp 22 111 df0 D15 D17 D<90387FFF800003B5FCD80780C7FC000CC8FC5A5AA25AA25AA81260A27EA27E120E6C7E 0001B512806C7E90C8FCA8007FB51280A219247D9920>I20 D<153081A381A281811680ED00C0B712F8A2C912C0ED0380160015065DA25DA35D25167E 942A>33 D49 DI<1460A214C0A2EB0180A3EB0300A21306A25BA25BA35BA25BA25BA2485AA248C7FC A31206A25AA25AA25AA35AA25A124013287A9D00>54 D<0040130400C0130C00601318A3 6C1330A36C1360A2381FFFE06C13C0EA0C00A238060180A238030300A3EA0186A3EA00CC A31378A31330A2161E809C17>56 DII<1304130CEA03CCEA0C38EA1818EA301C133CEA 703EEA60361366A2EAE067A213C7A3EAE187A3EAE307A312E6A3EA6606126CEA7C0EEA3C 0C1238EA1818EA1C30EA33C0EA3000A210237E9F15>I<0040130200C01306B20060130C A26C1318001C1370380F01E03803FF803800FE00171A7E981C>91 D<13101338A2136CA313C6A2EA0183A238030180A2380600C0A3481360A2481330A24813 18A348130CA24813061402171A7E981C>94 D<00C0130214060060130CA26C1318A36C13 30A26C1360A26C13C0A338030180A238018300A2EA00C6A2136CA31338A21310171A7E98 1C>I<133C13E0EA01C013801203AD13005A121C12F0121C12077E1380AD120113C0EA00 E0133C0E297D9E15>102 D<12F0121C12077E1380AD120113C0EA00E0133C13E0EA01C0 13801203AD13005A121C12F00E297D9E15>I<134013C0EA0180A3EA0300A21206A35AA2 5AA35AA25AA35AA21260A37EA27EA37EA27EA37EA2EA0180A3EA00C013400A2A7D9E10> I<12C0A21260A37EA27EA37EA27EA37EA2EA0180A3EA00C0A2EA0180A3EA0300A21206A3 5AA25AA35AA25AA35AA20A2A7E9E10>I<12C0B3B3A502297B9E0C>I<12C0A21260A37EA3 7EA37EA37EA27EA3EA0180A3EA00C0A31360A21330A31318A3130CA31306A31303130110 297E9E15>110 D E /Fq 53 123 df<14FE90380301801306EB0C03EB1C0191C7FC1318 1338A43803FFFE3800700EA35CA213E0A25CA3EA01C01472A438038034141891C7FC90C8 FCA25A12C612E65A12781925819C17>12 D<1218123CA31204A21208A212101220124012 80060C779C0D>39 D<13031306130813181330136013C0A2EA0180EA0300A21206A25AA2 121C1218A212381230A21270A21260A412E0A51260A51220123012107EA2102A7B9E11> I<1310A21308130C13041306A51307A51306A4130EA2130CA2131C1318A213381330A213 60A213C0A2EA0180EA0300A212065A5A121012605A102A809E11>I<1218123812781238 1208A21210A212201240A21280050C7D830D>44 DI<12301278 12F0126005047C830D>I<1304130C131813381378EA07B8EA0070A413E0A4EA01C0A4EA 0380A4EA0700A45AEAFFF00E1C7B9B15>49 D52 DI<133E13E138018180380300C01206120E120C12 1CA213011238A31303001813801307EA080B380C3300EA03C7EA0007130E130C131C1318 EAE0305BEA80C0EAC180003EC7FC121D7C9B15>57 D<1418A21438A21478A214B8EB0138 A2EB023C141C1304130C13081310A21320A2EB7FFCEBC01C1380EA0100141E0002130EA2 5A120C001C131EB4EBFFC01A1D7E9C1F>65 D<48B5FC39003C038090383801C0EC00E0A3 5B1401A2EC03C001E01380EC0F00141EEBFFFC3801C00E801580A2EA0380A43907000F00 140E141E5C000E13F0B512C01B1C7E9B1D>I<903803F02090381E0C6090383002E09038 E003C03801C001EA038048C7FC000E1480121E121C123C15005AA35AA41404A35C12705C 6C5B00185B6C485AD80706C7FCEA01F81B1E7A9C1E>I<48B512F038003C000138133015 20A35BA214081500495AA21430EBFFF03801C020A439038040801400A2EC0100EA07005C 14021406000E133CB512FC1C1C7E9B1C>69 D<3A01FFC3FF803A003C00780001381370A4 495BA449485AA390B5FC3901C00380A4484848C7FCA43807000EA448131E39FFE1FFC021 1C7E9B1F>72 DII<3A01FFC07F803A003C001E000138 131815205D5DD97002C7FC5C5C5CEBE04014C013E1EBE2E0EA01C4EBD07013E013C04848 7EA21418141CEA070080A348130F39FFE07FC0211C7E9B20>I<3801FFC038003C001338 A45BA45BA4485AA438038002A31404EA0700140C14181438000E13F0B5FC171C7E9B1A> IIII<3801FFFE39 003C038090383801C0EC00E0A3EB7001A315C0EBE0031580EC0700141C3801FFF001C0C7 FCA3485AA448C8FCA45AEAFFE01B1C7E9B1C>I83 D<001FB512C0381C070138 300E0000201480126012405B1280A2000014005BA45BA45BA4485AA41203EA7FFE1A1C79 9B1E>I<397FF03FE0390F000700000E13061404A3485BA4485BA4485BA4485BA35CA249 C7FCEA60025B6C5AEA1830EA07C01B1D789B1F>I<3AFF83FF07F03A3C007001C0003815 8002F01300A290380170025D13025D13045D13085D131001305B1320D81C405BA2D98071 C7FCA2381D0072A2001E1374A2001C1338A20018133014201210241D779B29>87 D<39FFC00FE0391E000380000EEB02005C000F130C6C13086D5A00035B5CEBC0C000015B 01C1C7FC13E2EA00E413EC13F81370A25BA4485AA4485AEA3FF81B1C789B1F>89 D97 D<123F1207A2120EA45AA4EA39E0EA3A18EA3C0C12381270130EA3EAE0 1CA31318133813301360EA60C0EA3180EA1E000F1D7C9C13>I<13F8EA0304120EEA1C0E EA181CEA30001270A25AA51304EA60081310EA3060EA0F800F127C9113>II<13F8EA0704120CEA1802EA38041230EA7008EA7FF0 EAE000A5EA60041308EA30101360EA0F800F127C9113>IIIII107 DI<391C1E078039266318C0394683A0E0384703 C0008E1380A2120EA2391C0701C0A3EC0380D8380E1388A2EC0708151039701C03203930 0C01C01D127C9122>II<13F8EA030CEA0E06487E121812 3000701380A238E00700A3130EA25BEA60185BEA30E0EA0F8011127C9115>I<38038780 3804C860EBD03013E0EA09C014381201A238038070A31460380700E014C0EB0180EB8300 EA0E86137890C7FCA25AA45AB4FC151A809115>I114 DI<12035AA3120EA4EAFFE0EA1C00A35AA45AA4EAE080A2EAE100A2126612380B1A7C99 0E>I<381C0180EA2E03124EA2388E0700A2121CA2EA380EA438301C80A3EA383C38184D 00EA0F8611127C9116>II<381E0183382703871247148338870701A2 120EA2381C0E02A31404EA180C131C1408EA1C1E380C26303807C3C018127C911C>I<38 038780380CC840380870E012103820E0C014001200A2485AA4EA03811263EAE38212C5EA 8584EA787813127E9113>I<381C0180EA2E03124EA2388E0700A2121CA2EA380EA4EA30 1CA3EA383CEA1878EA0FB8EA003813301370EAE0605BEA81800043C7FC123C111A7C9114 >II E /Fr 79 124 df0 D11 D<137E3801C180EA0301380703C0120EEB018090C7FCA5B512C0EA0E01B0387F87F8151D 809C17>II< 9038030180A39038060300A4EB0C06A5495AB612FCA23900301800A4495AA4B612FCA239 00C0600048485AA438030180A4D80603C7FCA31E257E9C23>35 D<126012F012F8126812 08A31210A2122012401280050C7C9C0C>39 D<1380EA0100120212065AA25AA25AA35AA4 12E0AC1260A47EA37EA27EA27E12027EEA0080092A7C9E10>I<7E12407E12307EA27EA2 7EA37EA41380AC1300A41206A35AA25AA25A12205A5A092A7E9E10>I<1203A4EAC30CEA E31CEA7338EA1FE0EA0780A2EA1FE0EA7338EAE31CEAC30CEA0300A40E127D9E15>I<13 06ADB612E0A2D80006C7FCAD1B1C7E9720>I<126012F0A212701210A41220A212401280 040C7C830C>II<126012F0A2126004047C830C>I<1301130313 06A3130CA31318A31330A31360A213C0A3EA0180A3EA0300A31206A25AA35AA35AA35AA3 5AA210297E9E15>II<5A1207123F12C71207B3A5EA FFF80D1C7C9B15>III<130CA2131C133CA2135C13DC139CEA011C120312021204120C120812101230 1220124012C0B512C038001C00A73801FFC0121C7F9B15>II<13F0EA030CEA0404EA0C0EEA181E1230130CEA7000 A21260EAE3E0EAE430EAE818EAF00C130EEAE0061307A51260A2EA7006EA300E130CEA18 18EA0C30EA03E0101D7E9B15>I<1240387FFF801400A2EA4002485AA25B485AA25B1360 134013C0A212015BA21203A41207A66CC7FC111D7E9B15>III<126012F0A212601200 AA126012F0A2126004127C910C>I<126012F0A212601200AA126012F0A212701210A412 20A212401280041A7C910C>I61 D<1306A3130FA3EB1780A2EB37C01323A2EB43E01341A2EB80F0A338010078A2EBFFF838 02003CA3487FA2000C131F80001E5BB4EBFFF01C1D7F9C1F>65 DI<90381F8080EBE0613801801938070007000E13035A14015A00781300A212 7000F01400A8007014801278A212386CEB0100A26C13026C5B380180083800E030EB1FC0 191E7E9C1E>IIII<90381F8080EBE0613801801938070007000E13035A14015A007813 00A2127000F01400A6ECFFF0EC0F80007013071278A212387EA27E6C130B380180113800 E06090381F80001C1E7E9C21>I<39FFF0FFF0390F000F00AC90B5FCEB000FAD39FFF0FF F01C1C7F9B1F>II<3807FF8038007C00133CB3 127012F8A21338EA7078EA4070EA30E0EA0F80111D7F9B15>I76 DIIII82 D<3807E080EA1C19EA30051303EA6001 12E01300A36C13007E127CEA7FC0EA3FF8EA1FFEEA07FFC61380130FEB07C01303130112 80A300C01380A238E00300EAD002EACC0CEA83F8121E7E9C17>I<007FB512C038700F01 0060130000401440A200C014201280A300001400B1497E3803FFFC1B1C7F9B1E>I<39FF F01FF0390F000380EC0100B3A26C1302138000035BEA01C03800E018EB7060EB0F801C1D 7F9B1F>I<39FFE00FF0391F0003C0EC01806C1400A238078002A213C000035BA2EBE00C 00011308A26C6C5AA213F8EB7820A26D5AA36D5AA2131F6DC7FCA21306A31C1D7F9B1F> I<3AFFE1FFC0FF3A1F003E003C001E013C13186C6D1310A32607801F1320A33A03C02780 40A33A01E043C080A33A00F081E100A39038F900F3017913F2A2017E137E013E137CA201 3C133C011C1338A20118131801081310281D7F9B2B>I<39FFF003FC390F8001E00007EB 00C06D13800003EB01006D5A000113026C6C5A13F8EB7808EB7C18EB3C10EB3E20131F6D 5A14C06D5AABEB7FF81E1C809B1F>89 D<12FEA212C0B3B312FEA207297C9E0C>91 D<12FEA21206B3B312FEA20729809E0C>93 D<1208121012201240A21280A312B012F812 781230050C7D9C0C>96 DI<12FC121CAA137CEA1D8738 1E0180381C00C014E014601470A6146014E014C0381E018038190700EA10FC141D7F9C17 >IIII<13 F8EA018CEA071E1206EA0E0C1300A6EAFFE0EA0E00B0EA7FE00F1D809C0D>II<12FC121CAA137C1387EA1D03001E1380121CAD38FF9FF0141D7F9C17>I<121812 3CA21218C7FCA712FC121CB0EAFF80091D7F9C0C>I<13C0EA01E0A2EA00C01300A7EA07 E01200B3A21260EAF0C012F1EA6180EA3E000B25839C0D>I<12FC121CAAEB0FE0EB0780 EB06005B13105B5B13E0121DEA1E70EA1C781338133C131C7F130F148038FF9FE0131D7F 9C16>I<12FC121CB3A9EAFF80091D7F9C0C>I<39FC7E07E0391C838838391D019018001E EBE01C001C13C0AD3AFF8FF8FF8021127F9124>IIII<3803E080EA0E19EA1805EA3807EA7003A212E0A61270A2EA38071218EA0E1B EA03E3EA0003A7EB1FF0141A7F9116>III<1204A4120CA2121C123CEA FFE0EA1C00A91310A5120CEA0E20EA03C00C1A7F9910>I<38FC1F80EA1C03AD1307120C EA0E1B3803E3F014127F9117>I<38FF07E0383C0380381C0100A2EA0E02A2EA0F06EA07 04A2EA0388A213C8EA01D0A2EA00E0A3134013127F9116>I<39FF3FC7E0393C0703C000 1CEB01801500130B000E1382A21311000713C4A213203803A0E8A2EBC06800011370A2EB 8030000013201B127F911E>I<38FF0FE0381E0700EA1C06EA0E046C5AEA039013B0EA01 E012007F12011338EA021C1204EA0C0E487E003C138038FE1FF014127F9116>I<38FF07 E0383C0380381C0100A2EA0E02A2EA0F06EA0704A2EA0388A213C8EA01D0A2EA00E0A313 40A25BA212F000F1C7FC12F312661238131A7F9116>III E /Fs 26 120 df<127012F812FCA212741204A41208A212 10A212201240060F7C840E>44 D<13801203120F12F31203B3A9EA07C0EAFFFE0F217CA0 18>49 D56 DI66 D68 D<39FFFC3FFF390FC003F039078001E0AE90B5FCEB8001AF390FC003F039FFFC3FFF 20227EA125>72 D77 D<3803F020380C0C60EA1802383001E0EA 70000060136012E0A21420A36C1300A21278127FEA3FF0EA1FFE6C7E0003138038003FC0 EB07E01301EB00F0A214707EA46C1360A26C13C07E38C8018038C60700EA81FC14247DA2 1B>83 D97 D<120E12FE121E120EAB131F EB61C0EB8060380F0030000E1338143C141C141EA7141C143C1438000F1370380C8060EB 41C038083F0017237FA21B>II<14E0130F1301 1300ABEA01F8EA0704EA0C02EA1C01EA38001278127012F0A7127012781238EA1801EA0C 0238070CF03801F0FE17237EA21B>II<133E13E33801C780EA0387130748C7FCA9EAFFF80007C7FCB27FEA7FF0112380 A20F>I<14703803F198380E1E18EA1C0E38380700A200781380A400381300A2EA1C0EEA 1E1CEA33F00020C7FCA212301238EA3FFE381FFFC06C13E0383000F0481330481318A400 601330A2003813E0380E03803803FE0015217F9518>I<120E12FE121E120EABEB1F80EB 60C0EB80E0380F0070A2120EAF38FFE7FF18237FA21B>I<121C123EA3121CC7FCA8120E 127E121E120EB1EAFFC00A227FA10E>I<120E12FE121E120EB3ADEAFFE00B237FA20E> 108 D<390E1FC07F3AFE60E183803A1E807201C03A0F003C00E0A2000E1338AF3AFFE3FF 8FFE27157F942A>I<380E1F8038FE60C0381E80E0380F0070A2120EAF38FFE7FF18157F 941B>II114 D<1202A41206A3120E121E 123EEAFFFCEA0E00AB1304A6EA07081203EA01F00E1F7F9E13>116 D<000E137038FE07F0EA1E00000E1370AD14F0A238060170380382783800FC7F18157F94 1B>I<39FF8FF87F393E01E03C001CEBC01814E0000E1410EB0260147000071420EB0430 1438D803841340EB8818141CD801C81380EBD00C140E3900F00F00497EA2EB6006EB4002 20157F9423>119 D E /Ft 25 122 df<127812FCA212FEA2127A1202A51204A31208A2 12101220A2124007147AB112>39 D<127812FCA212FEA2127A1202A51204A31208A21210 1220A2124007147A8512>44 D<127812FCA412781200B3127812FCA41278061F7A9E12> 58 D68 D70 D<13FE380303C0380C00E00010137080003C133C003E 131C141EA21208C7FCA3EB0FFEEBFC1EEA03E0EA0F80EA1F00123E123C127C481404A314 3EA21278007C135E6CEB8F08390F0307F03903FC03E01E1F7D9E21>97 D99 D<15F0141FA214011400AFEB0FC0EB70303801C00C3803800238070001120E 001E13005AA2127C1278A212F8A71278A2127C123CA27E000E13016C1302380380046C6C 487E3A00F030FF80EB1FC021327EB125>III< 15F090387F03083901C1C41C380380E8390700700848EB7800001E7FA2003E133EA6001E 133CA26C5B6C13706D5A3809C1C0D8087FC7FC0018C8FCA5121C7E380FFFF86C13FF6C14 80390E000FC00018EB01E048EB00F000701470481438A500701470A26C14E06CEB01C000 07EB07003801C01C38003FE01E2F7E9F21>II<120FEA1F80A4EA0F00C7FCABEA0780127FA2120F1207B3A6EA0FC0EAFFF8A20D30 7EAF12>I<131E133FA4131E1300AB131FEA01FFA2EA001F130FB3B0EA200E12F8131E13 1CEA7038EA6070EA1FC0103E83AF14>III<260780FEEB1FC03BFF83078060F0903A 8C03C180783B0F9001E2003CD807A013E4DA00F47F01C013F8A2495BB3A2486C486C133F 3CFFFC1FFF83FFF0A2341F7E9E38>I<380780FE39FF83078090388C03C0390F9001E0EA 07A06E7E13C0A25BB3A2486C487E3AFFFC1FFF80A2211F7E9E25>II<380781FC39FF86078090388801C0390F9000E0D807A0137001C01378497F 153E151E151FA2811680A716005DA2151E153E153C6D5B01A013705D90389803C0D9860F C7FCEB81F80180C8FCAB487EEAFFFCA2212D7E9E25>I<380783E038FF8418EB887CEA0F 90EA07A01438EBC000A35BB3487EEAFFFEA2161F7E9E19>114 D<3801FC10380E033038 1800F048137048133012E01410A37E6C1300127EEA3FF06CB4FC6C13C0000313E038003F F0EB01F813006C133CA2141C7EA27E14186C1338143000CC136038C301C03880FE00161F 7E9E1A>I<1340A513C0A31201A212031207120F381FFFE0B5FC3803C000B01410A80001 132013E000001340EB78C0EB1F00142C7FAB19>II121 D E end %%EndProlog %%BeginSetup %%Feature: *Resolution 300dpi TeXDict begin %%PaperSize: a4 %%EndSetup %%Page: 1 1 1 0 bop 390 369 a Ft(F)-6 b(ormal)22 b(correctness)g(pro)r(ofs)f(of)h (functional)307 461 y(programs:)29 b(Dijkstra's)21 b(algorithm,)g(a)g (case)h(study)516 587 y Fs(Holger)16 b(Benl)f(and)i(Helm)o(ut)c(Sc)o(h) o(wic)o(h)o(ten)o(b)q(erg)703 691 y(Draft)k(of)g(Marc)o(h)e(8,)i(1999) 307 839 y Fr(One)c(can)f(argue)g(that)g(writing)f(pro)q(ofs)h(migh)o(t) e(b)q(e)i(b)q(etter)i(than)e(writing)f(programs,)257 889 y(for)g(the)g(follo)o(wing)d(simple)i(reason:)17 b(There)12 b(is)e(no)h(algorithm)d(that)j(can)g(c)o(hec)o(k)h(whether) 257 938 y(a)e(program)f(meets)h(its)g(sp)q(eci\014cation,)h(but)f(it)g (is)g(easy)g(to)g(c)o(hec)o(k)h(whether)g(a)f(giv)o(en)g(pro)q(of)257 988 y(is)k(correct.)307 1044 y(Let)h(us)g(\014rst)g(review)g(some)e(w)o (ell-kno)o(wn)g(paradigms)g(for)h(connecting)h(pro)q(ofs)f(and)257 1094 y(programs)f(\(see)i(Bates/Constable)g([1)o(])f(for)f(more)g(bac)o (kground\).)308 1174 y(1.)20 b(W)m(rite)d(the)h(\(functional\))e (program)g(as)h(term)g(in)g(an)g(approriate)g(higher)h(t)o(yp)q(e)361 1223 y(language,)11 b(and)g(pro)o(v)o(e)g(its)g(correctness,)k(i.e.)10 b(that)h(it)g(satis\014es)i(its)e(sp)q(eci\014cation.)308 1302 y(2.)20 b(F)m(rom)8 b(a)h Fq(c)n(onstructive)k Fr(pro)q(of)c(of)g (a)g(form)o(ula)e Fp(8)p Fo(x)p Fp(9)1120 1287 y Fn(\003)1139 1302 y Fo(y)i(B)r Fr(\()p Fo(x;)e(y)q Fr(\))j(extract)h(a)e(program.) 308 1380 y(3.)20 b(F)m(or)13 b(a)g Fq(non-c)n(onstructive)j Fr(pro)q(of)d(of)f(a)h(form)o(ula)e Fp(8)p Fo(x)p Fp(9)p Fo(y)d(B)r Fr(\()p Fo(x;)f(y)q Fr(\))14 b(\(with)f Fp(9)g Fr(de\014ned)361 1430 y(b)o(y)h Fp(:8:)f Fr(and)h Fo(B)r Fr(\()p Fo(x;)7 b(y)q Fr(\))14 b(quan)o(ti\014er-free\):)399 1508 y(a.)20 b(Use)15 b(the)g(instanciated)f(pro)q(of)f(as)h(a)g (program.)397 1570 y(b.)20 b(T)m(ransform)f(the)i(non-constructiv)o(e)g (pro)q(of)f(in)o(to)g(a)g(constructiv)o(e)i(pro)q(of)452 1620 y(\(`)p Fo(A)p Fr(-translation'\))13 b(and)h(extract)h(a)e (program.)257 1700 y(Note)j(that)g(a)f(constructiv)o(e)i(pro)q(of)e(of) f Fp(8)p Fo(x)p Fp(9)950 1685 y Fn(\003)969 1700 y Fo(y)9 b(B)r Fr(\()p Fo(x;)e(y)q Fr(\))16 b(is)g(usually)e(based)i(on)f(an)g (idea)257 1750 y(for)e(an)g(algorithm,)e(and)i(hence)i(it)e(is)g(not)g (surprising)g(that)h(one)f(can)h(extract)g(a)f(corre-)257 1799 y(sp)q(onding)i(program)e(from)g(the)j(pro)q(of.)k(Therefore)c (paradigms)d(\(1\))i(and)f(\(2\))h(are)g(not)257 1849 y(to)q(o)f(di\013eren)o(t)g(from)e(eac)o(h)i(other.)k(Ho)o(w)o(ev)o (er,)c(there)g(are)g(adv)n(an)o(tages)f(of)g(\(2\))g(o)o(v)o(er)h (\(1\):)320 1929 y Fp(\017)20 b Fr(One)d(need)f(not)g(write)g(a)f (program)f(explicitely;)i(the)g(mac)o(hine)f(will)f(extract)j(it)361 1979 y(automatically)10 b(from)g(the)k(formal)c(pro)q(of)i(\(whic)o(h)h (can)g(b)q(e)g(mac)o(hine-c)o(hec)o(k)o(ed)f(to)361 2029 y(b)q(e)j(correct\).)320 2107 y Fp(\017)20 b Fr(More)15 b(imp)q(ortan)o(tly)m(,)10 b(when)15 b(dealing)e(with)h(pro)q(ofs)g (instead)g(of)g(mere)f(programs)361 2157 y(it)g(is)g(p)q(ossible)g(to)g (adapt)g(pro)q(ofs)g(to)g(sp)q(ecial)h(cases)g(\(Goad's)e Fq(pruning)18 b Fr([4)o(]\),)12 b(and)361 2207 y(then)j(extract)g(a)e (b)q(etter)j(program)c(\(cf.)18 b(e.g.)13 b([5]\).)257 2286 y(Concerning)e(program)d(extraction)j(from)d(classical)i(pro)q (ofs)g(\(3\),)h(it)f(is)g(kno)o(wn)f(that)h(\(3a\))257 2336 y(and)16 b(\(3b\))g(yield)g(the)h(same)e(algorithm)e(\(cf.)j ([2]\).)24 b(Moreo)o(v)o(er,)17 b(for)e(\(3b\))i(re\014nemen)o(ts)257 2386 y(are)c(p)q(ossible)f(\(and)g(necessary\),)j(in)c(order)i(to)f (obtain)f(reasonable)i(programs)e(\(cf.)h([3)o(]\).)938 2510 y(1)p eop %%Page: 2 2 2 1 bop 307 195 a Fr(In)14 b(the)g(presen)o(t)h(note)f(w)o(e)g(will)e (only)h(deal)g(with)h(\(1\),)f(and)g(to)h(a)f(lesser)i(exten)o(t)g (with)257 245 y(\(2\).)37 b(Rather)20 b(than)g(dev)o(eloping)g(m)o(uc)o (h)f(theory)h(w)o(e)g(shall)g(treat)g(a)g(case)h(study)g(of)257 295 y(some)13 b(practical)g(in)o(terest:)19 b(the)14 b(algorithm)d(of)16 b Fm(Dijkstra)p Fr(,)d(computing)f(the)i(minim)o (al)257 345 y(distances)h(from)d(a)i(\014xed)g(no)q(de)g(in)f(a)h(w)o (eigh)o(ted)f(graph.)18 b(The)c(aim)e(is)i(to)f(demonstrate)257 394 y(that)19 b(it)f(is)g(p)q(ossible)g(to)g(in)o(teractiv)o(ely)g (construct)i(a)e(formal)e(pro)q(of,)i(and)g(extract)i(a)257 444 y(reasonable)13 b(program)d(from)h(it.)17 b(The)12 b(theory)h(b)q(ehind)f(this)g(extraction)h(pro)q(cess)h(is)e(the)257 494 y(w)o(ell-kno)o(wn)h(\(mo)q(di\014ed\))g Fq(r)n(e)n(alizability)p Fr(.)307 552 y(The)g(plan)e(of)g(this)h(note)g(is)g(as)g(follo)o(ws.)k (W)m(e)11 b(\014rst)i(recall)f(the)g Fm(Dijkstra)g Fr(algorithm)257 601 y(and)i(pro)o(v)o(e)h(its)f(correctness.)22 b(Then)14 b(w)o(e)h(commen)o(t)d(on)i(some)f(issues)i(coming)e(up)h(in)g(a)257 651 y(formalization)8 b(of)j(this)g(pro)q(of,)g(whic)o(h)g(has)g(b)q (een)h(carried)g(out)f(in)f(the)i Fm(Minlog)f Fr(system)257 701 y(under)k(dev)o(elopmen)o(t)e(in)h(Munic)o(h.)257 846 y Fl(1)67 b(The)22 b(Dijkstra)h(algorithm:)31 b(correctness)22 b(pro)r(of)257 944 y Fm(Dijkstra)p Fr('s)10 b(algorithm)d(deals)j(with) f(a)h(w)o(eigh)o(ted)f(graph;)i(it)e(determines)h(the)h(minim)o(al)257 994 y(distances)i(from)e(a)g(\014xed)i(no)q(de.)18 b(The)12 b(p)q(oin)o(t)f(is)h(that)g(it)g(runs)g(in)g(time)e Fo(O)q Fr(\()p Fo(n)1437 979 y Fk(2)1456 994 y Fr(\),)i(whereas)257 1044 y(the)j(naiv)o(e)e(algorithm)e(needs)16 b Fo(O)q Fr(\()p Fo(n)814 1029 y Fk(3)832 1044 y Fr(\))e(steps.)307 1102 y(Let)20 b(\000)i(=)g(\()p Fo(V)r(;)7 b(E)r(;)g(w)q Fr(\))19 b(b)q(e)h(a)g(w)o(eigh)o(ted)g(graph,)g(where)h Fo(V)30 b Fr(is)19 b(the)i(\(\014nite\))f(set)h(of)257 1151 y Fq(no)n(des)p Fr(,)e Fo(E)h Fp(\022)d(f)7 b(f)p Fo(a;)g(b)p Fp(g)16 b(j)i Fo(a;)7 b(b)16 b Fp(2)i Fo(V)e Fp(g)h Fr(is)h(the)g(set)g(of)f Fq(e)n(dges)k Fr(and)d Fo(w)6 b Fr(:)14 b Fp(f)7 b(f)p Fo(a;)g(b)p Fp(g)16 b(j)h Fo(a;)7 b(b)17 b Fp(2)257 1201 y Fo(V)g Fp(g)11 b(!)g Fj(N)6 b Fp([)i(f1g)13 b Fr(is)g(the)h Fq(weight)j Fr(function.)g(W)m (e)c(write)h Fo(w)q Fr(\()p Fo(a;)7 b(b)p Fr(\))13 b(for)g Fo(w)q Fr(\()p Fp(f)p Fo(a;)7 b(b)p Fp(g)p Fr(\);)12 b(hence)257 1251 y Fo(w)q Fr(\()p Fo(a;)7 b(b)p Fr(\))k(=)h Fo(w)q Fr(\()p Fo(b;)7 b(a)p Fr(\))13 b(b)o(y)h(de\014nition.)k(W)m(e) 13 b(also)g(require)i(that)308 1340 y(1.)20 b Fo(w)q Fr(\()p Fo(a;)7 b(b)p Fr(\))k(=)h(0)h(i\013)h Fo(a)d Fr(=)h Fo(b)p Fr(.)308 1422 y(2.)20 b(F)m(or)g Fo(a)j Fp(6)p Fr(=)g Fo(b)p Fr(,)f Fo(w)q Fr(\()p Fo(a;)7 b(b)p Fr(\))22 b(=)h Fp(1)d Fr(i\013)g(there)i(is)e(no)h(edge)g(b)q(et)o(w)o (een)h Fo(a)e Fr(and)h Fo(b)p Fr(,)g(i.e.)361 1472 y Fp(f)p Fo(a;)7 b(b)p Fp(g)15 b Fo(=)-26 b Fp(2)12 b Fo(E)r Fr(.)257 1560 y(W)m(e)19 b(need)g(to)g(\014nd)g(a)f(map)g Fo(d)5 b Fr(:)14 b Fo(V)29 b Fp(!)19 b Fj(N)10 b Fp([)j(f1g)k Fr(suc)o(h)j(that)f Fo(d)p Fr(\()p Fo(b)p Fr(\))f(is)h(the)g(length)g (of)257 1610 y(the)d(shortest)h(path)f(from)d(the)j(distinguished)g(no) q(de)f Fo(b)1133 1616 y Fk(0)1167 1610 y Fr(to)g Fo(b)p Fr(.)23 b(F)m(or)15 b(simplicit)o(y)d(let)k(us)257 1660 y(assume)e(that)g(the)h(w)o(eigh)o(ted)f(graph)g(has)g(the)g(set)h Fo(V)21 b Fr(=)12 b Fp(f)p Fr(0)p Fo(;)7 b Fr(1)p Fo(;)g(:)g(:)g(:)k(;) c(N)13 b Fp(\000)d Fr(1)p Fp(g)j Fr(of)h(no)q(des,)257 1710 y(and)j(that)h(0)f(is)g(the)h(distinguished)f(no)q(de.)29 b(Here)18 b(is)g(a)f(w)o(ell-kno)o(wn)f(form)o(ulation)e(of)257 1760 y Fm(Dijkstra)p Fr('s)g(algorithm:)539 1846 y Fo(d)p Fr(\()p Fo(a)p Fr(\))d(:=)g Fo(w)q Fr(\()p Fo(a;)c Fr(0\);)539 1896 y Fo(U)16 b Fr(:=)11 b Fo(V)19 b Fp(n)9 b(f)p Fr(0)p Fp(g)41 b Fr(\(=)14 b(set)h(of)e(undone)h(no)q(des\);)539 1945 y(while)f Fo(U)j Fp(6)p Fr(=)c Fp(;)i Fr(do)580 1995 y Fp(h)p Fr(pic)o(k)g Fo(c)d Fp(2)h Fo(U)18 b Fr(suc)o(h)d(that)f Fo(d)p Fr(\()p Fo(c)p Fr(\))d(=)h(min)1179 2001 y Fi(a)p Fn(2)p Fi(U)1254 1995 y Fo(d)p Fr(\()p Fo(a)p Fr(\))p Fp(i)p Fr(;)580 2045 y(for)i Fo(a)d Fp(2)g Fo(U)19 b Fr(do)622 2095 y Fo(d)p Fr(\()p Fo(a)p Fr(\))11 b(:=)g(min)o Fp(f)p Fo(d)p Fr(\()p Fo(a)p Fr(\))p Fo(;)c(d)p Fr(\()p Fo(c)p Fr(\))h(+)h Fo(w)q Fr(\()p Fo(c;)e(a)p Fr(\)\))p Fp(g)p Fr(;)580 2145 y(end;)580 2194 y Fo(U)17 b Fr(:=)11 b Fo(U)j Fp(n)9 b(f)p Fo(c)p Fp(g)p Fr(;)539 2244 y(end;)257 2336 y(Clearly)j(the)h(complexit)o(y)d(is)j Fo(O)q Fr(\()p Fo(n)794 2321 y Fk(2)812 2336 y Fr(\).)18 b(In)12 b(the)h(table)f(1)g (b)q(elo)o(w)g(w)o(e)h(giv)o(e)e(an)i(example)e(for)257 2386 y(the)k(w)o(orking)e(of)g(the)i Fm(Dijkstra)e Fr(algorithm.)938 2510 y(2)p eop %%Page: 3 3 3 2 bop 332 210 1233 2 v 331 260 2 50 v 948 260 V 1564 260 V 331 298 V 493 283 a Fr(Up)q(date)14 b(distance)p 948 298 V 337 w(Pic)o(k)g(new)g(no)q(de)p 1564 298 V 331 348 V 948 348 V 1564 348 V 332 338 1233 2 v 331 387 2 50 v 948 387 V 1564 387 V 331 669 2 294 v 357 654 a Fo(d)379 660 y Fk(0)397 654 y Fr(:)524 457 y Fh(\000)482 498 y(\000)465 515 y(\000)524 615 y(@)482 573 y(@)465 556 y(@)p 565 416 200 2 v 723 457 a(\000)681 498 y(\000)640 540 y(\000)598 581 y(\000)565 615 y(\000)p 565 615 V 822 515 a(@)781 473 y(@)764 457 y(@)822 556 y(\000)781 598 y(\000)764 615 y(\000)495 588 y Fr(2)495 469 y(1)814 588 y(1)814 469 y(2)654 647 y(5)654 409 y(8)644 518 y(1)422 528 y(0)432 515 y Fg(i)555 399 y Fr(1)565 385 y Fg(i)555 657 y Fr(2)565 644 y Fg(i)p 948 669 2 294 v 974 654 a Fo(p)995 660 y Fk(0)1013 654 y Fr(:)1140 457 y Fh(\000)1098 498 y(\000)1081 515 y(\000)1140 615 y(@)1098 573 y(@)1081 556 y(@)p 1181 416 200 2 v 1339 457 a(\000)1297 498 y(\000)1256 540 y(\000)1214 581 y(\000)1181 615 y(\000)p 1181 615 V 1438 515 a(@)1397 473 y(@)1380 457 y(@)1438 556 y(\000)1397 598 y(\000)1380 615 y(\000)1111 588 y Fr(2)1111 469 y(1)1430 588 y(1)1430 469 y(2)1270 647 y(5)1270 409 y(8)1260 518 y(1)1171 425 y Fp(\017)1038 528 y Fr(0)1048 515 y Fg(i)1171 399 y Fr(1)1181 385 y Fg(i)1171 657 y Fr(2)1181 644 y Fg(i)p 1564 669 2 294 v 331 719 2 50 v 948 719 V 1564 719 V 332 709 1233 2 v 331 759 2 50 v 948 759 V 1564 759 V 331 1041 2 294 v 357 1026 a Fo(d)379 1032 y Fk(1)397 1026 y Fr(:)524 828 y Fh(\000)482 870 y(\000)465 886 y(\000)524 986 y(@)482 945 y(@)465 928 y(@)p 565 788 200 2 v 723 828 a(\000)681 870 y(\000)640 911 y(\000)598 953 y(\000)565 986 y(\000)p 565 987 V 822 886 a(@)781 845 y(@)764 828 y(@)822 928 y(\000)781 970 y(\000)764 986 y(\000)495 960 y Fr(2)495 840 y(1)814 960 y(1)814 840 y(2)654 1019 y(5)654 780 y(8)644 890 y(1)555 796 y Fp(\017)422 900 y Fr(0)432 886 y Fg(i)555 770 y Fr(1)565 757 y Fg(i)555 1029 y Fr(2)565 1016 y Fg(i)754 770 y Fr(9)764 757 y Fg(i)p 948 1041 2 294 v 974 1026 a Fo(p)995 1032 y Fk(1)1013 1026 y Fr(:)1140 828 y Fh(\000)1098 870 y(\000)1081 886 y(\000)1140 986 y(@)1098 945 y(@)1081 928 y(@)p 1181 788 200 2 v 1339 828 a(\000)1297 870 y(\000)1256 911 y(\000)1214 953 y(\000)1181 986 y(\000)p 1181 987 V 1438 886 a(@)1397 845 y(@)1380 828 y(@)1438 928 y(\000)1397 970 y(\000)1380 986 y(\000)1111 960 y Fr(2)1111 840 y(1)1430 960 y(1)1430 840 y(2)1270 1019 y(5)1270 780 y(8)1260 890 y(1)1171 796 y Fp(\017)1171 995 y(\017)1038 900 y Fr(0)1048 886 y Fg(i)1171 770 y Fr(1)1181 757 y Fg(i)1171 1029 y Fr(2)1181 1016 y Fg(i)1370 770 y Fr(9)1380 757 y Fg(i)p 1564 1041 2 294 v 331 1091 2 50 v 948 1091 V 1564 1091 V 332 1081 1233 2 v 331 1130 2 50 v 948 1130 V 1564 1130 V 331 1412 2 294 v 357 1398 a Fo(d)379 1404 y Fk(2)397 1398 y Fr(:)524 1200 y Fh(\000)482 1241 y(\000)465 1258 y(\000)524 1358 y(@)482 1316 y(@)465 1300 y(@)p 565 1159 200 2 v 723 1200 a(\000)681 1241 y(\000)640 1283 y(\000)598 1324 y(\000)565 1358 y(\000)p 565 1359 V 822 1258 a(@)781 1217 y(@)764 1200 y(@)822 1300 y(\000)781 1341 y(\000)764 1358 y(\000)495 1331 y Fr(2)495 1212 y(1)814 1331 y(1)814 1212 y(2)654 1391 y(5)654 1152 y(8)644 1261 y(1)555 1168 y Fp(\017)555 1367 y(\017)422 1271 y Fr(0)432 1258 y Fg(i)555 1142 y Fr(1)565 1129 y Fg(i)555 1401 y Fr(2)565 1388 y Fg(i)754 1142 y Fr(3)764 1129 y Fg(i)754 1401 y Fr(7)764 1388 y Fg(i)p 948 1412 2 294 v 974 1398 a Fo(p)995 1404 y Fk(2)1013 1398 y Fr(:)1140 1200 y Fh(\000)1098 1241 y(\000)1081 1258 y(\000)1140 1358 y(@)1098 1316 y(@)1081 1300 y(@)p 1181 1159 200 2 v 1339 1200 a(\000)1297 1241 y(\000)1256 1283 y(\000)1214 1324 y(\000)1181 1358 y(\000)p 1181 1359 V 1438 1258 a(@)1397 1217 y(@)1380 1200 y(@)1438 1300 y(\000)1397 1341 y(\000)1380 1358 y(\000)1111 1331 y Fr(2)1111 1212 y(1)1430 1331 y(1)1430 1212 y(2)1270 1391 y(5)1270 1152 y(8)1260 1261 y(1)1171 1168 y Fp(\017)1171 1367 y(\017)1370 1168 y(\017)1038 1271 y Fr(0)1048 1258 y Fg(i)1171 1142 y Fr(1)1181 1129 y Fg(i)1171 1401 y Fr(2)1181 1388 y Fg(i)1370 1142 y Fr(3)1380 1129 y Fg(i)1370 1401 y Fr(7)1380 1388 y Fg(i)p 1564 1412 2 294 v 331 1462 2 50 v 948 1462 V 1564 1462 V 332 1452 1233 2 v 331 1502 2 50 v 948 1502 V 1564 1502 V 331 1784 2 294 v 357 1769 a Fo(d)379 1775 y Fk(3)397 1769 y Fr(:)524 1572 y Fh(\000)482 1613 y(\000)465 1630 y(\000)524 1729 y(@)482 1688 y(@)465 1671 y(@)p 565 1531 200 2 v 723 1572 a(\000)681 1613 y(\000)640 1655 y(\000)598 1696 y(\000)565 1729 y(\000)p 565 1730 V 822 1630 a(@)781 1588 y(@)764 1572 y(@)822 1671 y(\000)781 1713 y(\000)764 1729 y(\000)495 1703 y Fr(2)495 1583 y(1)814 1703 y(1)814 1583 y(2)654 1762 y(5)654 1523 y(8)644 1633 y(1)555 1539 y Fp(\017)555 1738 y(\017)754 1539 y(\017)422 1643 y Fr(0)432 1630 y Fg(i)555 1513 y Fr(1)565 1500 y Fg(i)555 1772 y Fr(2)565 1759 y Fg(i)754 1513 y Fr(3)764 1500 y Fg(i)754 1772 y Fr(7)764 1759 y Fg(i)884 1643 y Fr(5)894 1630 y Fg(i)p 948 1784 2 294 v 974 1769 a Fo(p)995 1775 y Fk(3)1013 1769 y Fr(:)1140 1572 y Fh(\000)1098 1613 y(\000)1081 1630 y(\000)1140 1729 y(@)1098 1688 y(@)1081 1671 y(@)p 1181 1531 200 2 v 1339 1572 a(\000)1297 1613 y(\000)1256 1655 y(\000)1214 1696 y(\000)1181 1729 y(\000)p 1181 1730 V 1438 1630 a(@)1397 1588 y(@)1380 1572 y(@)1438 1671 y(\000)1397 1713 y(\000)1380 1729 y(\000)1111 1703 y Fr(2)1111 1583 y(1)1430 1703 y(1)1430 1583 y(2)1270 1762 y(5)1270 1523 y(8)1260 1633 y(1)1171 1539 y Fp(\017)1171 1738 y(\017)1370 1539 y(\017)1466 1639 y(\017)1038 1643 y Fr(0)1048 1630 y Fg(i)1171 1513 y Fr(1)1181 1500 y Fg(i)1171 1772 y Fr(2)1181 1759 y Fg(i)1370 1513 y Fr(3)1380 1500 y Fg(i)1370 1772 y Fr(7)1380 1759 y Fg(i)1499 1643 y Fr(5)1510 1630 y Fg(i)p 1564 1784 2 294 v 331 1834 2 50 v 948 1834 V 1564 1834 V 332 1824 1233 2 v 331 1874 2 50 v 948 1874 V 1564 1874 V 331 2156 2 294 v 357 2141 a Fo(d)379 2147 y Fk(4)397 2141 y Fr(:)524 1943 y Fh(\000)482 1985 y(\000)465 2001 y(\000)524 2101 y(@)482 2059 y(@)465 2043 y(@)p 565 1902 200 2 v 723 1943 a(\000)681 1985 y(\000)640 2026 y(\000)598 2068 y(\000)565 2101 y(\000)p 565 2102 V 822 2001 a(@)781 1960 y(@)764 1943 y(@)822 2043 y(\000)781 2084 y(\000)764 2101 y(\000)495 2074 y Fr(2)495 1955 y(1)814 2074 y(1)814 1955 y(2)654 2134 y(5)654 1895 y(8)644 2005 y(1)555 1911 y Fp(\017)555 2110 y(\017)754 1911 y(\017)854 2010 y(\017)422 2015 y Fr(0)432 2001 y Fg(i)555 1885 y Fr(1)565 1872 y Fg(i)555 2144 y Fr(2)565 2131 y Fg(i)754 1885 y Fr(3)764 1872 y Fg(i)754 2144 y Fr(6)764 2131 y Fg(i)884 2015 y Fr(5)894 2001 y Fg(i)p 948 2156 2 294 v 974 2141 a Fo(p)995 2147 y Fk(4)1013 2141 y Fr(:)1140 1943 y Fh(\000)1098 1985 y(\000)1081 2001 y(\000)1140 2101 y(@)1098 2059 y(@)1081 2043 y(@)p 1181 1902 200 2 v 1339 1943 a(\000)1297 1985 y(\000)1256 2026 y(\000)1214 2068 y(\000)1181 2101 y(\000)p 1181 2102 V 1438 2001 a(@)1397 1960 y(@)1380 1943 y(@)1438 2043 y(\000)1397 2084 y(\000)1380 2101 y(\000)1111 2074 y Fr(2)1111 1955 y(1)1430 2074 y(1)1430 1955 y(2)1270 2134 y(5)1270 1895 y(8)1260 2005 y(1)1171 1911 y Fp(\017)1171 2110 y(\017)178 b(\017)1370 1911 y(\017)1470 2010 y(\017)1038 2015 y Fr(0)1048 2001 y Fg(i)1171 1885 y Fr(1)1181 1872 y Fg(i)1171 2144 y Fr(2)1181 2131 y Fg(i)1370 1885 y Fr(3)1380 1872 y Fg(i)1370 2144 y Fr(6)1380 2131 y Fg(i)1499 2015 y Fr(5)1510 2001 y Fg(i)p 1564 2156 2 294 v 331 2205 2 50 v 948 2205 V 1564 2205 V 332 2207 1233 2 v 491 2323 a Fr(T)m(able)13 b(1:)18 b(An)c(example)e(for)i(the)g Fm(Dijkstra)g Fr(Algorithm)938 2510 y(3)p eop %%Page: 4 4 4 3 bop 1639 187 a Ff(dijkstraalg)257 242 y Fe(1.1.)21 b Fq(The)d Fm(Dijkstra)d Fq(algorithm.)j Fr(F)m(or)13 b(all)g Fo(n)e(<)h(N)19 b Fr(w)o(e)14 b(will)e(de\014ne)320 320 y Fp(\017)20 b Fr(a)14 b(set)h Fo(C)491 326 y Fi(n)524 320 y Fp(\022)d Fj(N)p Fr(,)g(the)i(set)h(of)e Fq(c)n(ompute)n(d)19 b Fr(no)q(des)c(at)e(stage)i Fo(n)p Fr(,)320 397 y Fp(\017)20 b Fr(a)g(function)g Fd(nxt)626 403 y Fi(n)653 397 y Fr(:)c Fj(N)k Fp(!)h Fj(N)p Fr(,)e(giving)f(for)i(ev)o(ery)h(no)q(de)f(the)h Fq(next)j Fr(no)q(de)d(in)f(a)361 447 y(shortest)c(path)d(from)g Fo(a)g Fr(to)h(0,)f(as)h(far)g(as)g(it)f(is)h(kno)o(wn)f(at)h(stage)g Fo(n)p Fr(,)320 525 y Fp(\017)20 b Fr(a)15 b(function)f Fo(d)582 531 y Fi(n)609 525 y Fr(:)g Fj(N)d Fp(!)h Fj(N)c Fp([)h(f1g)p Fr(,)14 b(giving)f(for)i(ev)o(ery)g(no)q(de)g(the)h Fq(distanc)n(e)i Fr(from)361 575 y(0)e(along)f(the)h(path)g(to)g(0)g (determined)g(b)o(y)g(the)h(next-function,)f(as)g(far)g(as)g(it)f(is) 361 624 y(kno)o(wn)f(at)f(stage)i Fo(n)p Fr(,)320 702 y Fp(\017)20 b Fo(p)382 708 y Fi(n)405 702 y Fr(,)13 b(the)h(no)q(de)h Fq(picke)n(d)j Fr(at)c(stage)g Fo(n)p Fr(.)257 779 y(The)i(reason)g(for)e(including)g(the)i(next-function)f (is)g(that)g(it)g(is)g(needed)h(for)f(writing)g(a)257 829 y(sp)q(eci\014cation)d(of)f(the)g(algorithm)e(in)h(1.2.)16 b(In)11 b(an)o(y)g(case,)h(it)f(seems)g(reasonable)g(that)h(the)257 879 y(algorithm)f(not)j(only)e(returns)j(minima)o(l)10 b(distances,)k(but)g(also)f(corresp)q(onding)h(paths.)307 934 y(Let)467 984 y Fo(C)497 990 y Fk(0)538 984 y Fr(:=)23 b Fp(f)p Fr(0)p Fp(g)p Fo(;)89 b Fd(nxt)824 990 y Fk(0)843 984 y Fr(\()p Fo(a)p Fr(\))23 b(:=)g(0)p Fo(;)89 b(d)1131 990 y Fk(0)1150 984 y Fr(\()p Fo(a)p Fr(\))23 b(:=)g Fo(w)q Fr(\()p Fo(a;)7 b Fr(0\))p Fo(:)257 1051 y Fr(Assume)14 b(that)g(at)g(stage)g Fo(n)g Fr(w)o(e)g(ha)o(v)o(e)g(pic)o(k)o(ed)g Fo(p)1003 1057 y Fi(n)1039 1051 y Fr(suc)o(h)h(that)446 1128 y Fo(p)467 1134 y Fi(n)501 1128 y Fo(<)d(N)i Fp(^)9 b Fo(p)650 1134 y Fi(n)688 1128 y Fo(=)-25 b Fp(2)11 b Fo(C)753 1134 y Fi(n)785 1128 y Fp(^)d(8)p Fo(a<)q(N)k Fr(\()p Fo(d)982 1134 y Fi(n)1004 1128 y Fr(\()p Fo(a)p Fr(\))g Fo(<)f(d)1135 1134 y Fi(n)1158 1128 y Fr(\()p Fo(p)1195 1134 y Fi(n)1217 1128 y Fr(\))h Fp(!)f Fo(a)g Fp(2)h Fo(C)1401 1134 y Fi(n)1423 1128 y Fr(\))p Fo(:)135 b Fr(\(1\))257 1206 y(Let)446 1283 y Fo(C)476 1289 y Fi(n)p Fk(+1)563 1283 y Fr(:=)23 b Fo(C)660 1289 y Fi(n)692 1283 y Fp([)9 b(f)p Fo(p)771 1289 y Fi(n)793 1283 y Fp(g)p Fo(;)446 1387 y Fd(nxt)502 1393 y Fi(n)p Fk(+1)566 1387 y Fr(\()p Fo(a)p Fr(\))23 b(:=)710 1316 y Fc(\()744 1359 y Fo(p)765 1365 y Fi(n)918 1359 y Fr(if)13 b Fo(d)978 1365 y Fi(n)1000 1359 y Fr(\()p Fo(p)1037 1365 y Fi(n)1060 1359 y Fr(\))c(+)g Fo(w)q Fr(\()p Fo(a;)e(p)1235 1365 y Fi(n)1257 1359 y Fr(\))12 b Fo(<)g(d)1351 1365 y Fi(n)1373 1359 y Fr(\()p Fo(a)p Fr(\),)744 1419 y Fd(nxt)799 1425 y Fi(n)822 1419 y Fr(\()p Fo(a)p Fr(\))42 b(otherwise,)446 1491 y Fo(d)468 1497 y Fi(n)p Fk(+1)532 1491 y Fr(\()p Fo(a)p Fr(\))23 b(:=)g(min)o Fp(f)p Fo(d)789 1497 y Fi(n)811 1491 y Fr(\()p Fo(p)848 1497 y Fi(n)870 1491 y Fr(\))10 b(+)f Fo(w)q Fr(\()p Fo(a;)e(p)1046 1497 y Fi(n)1068 1491 y Fr(\))p Fo(;)g(d)1125 1497 y Fi(n)1147 1491 y Fr(\()p Fo(a)p Fr(\))p Fp(g)p Fo(:)257 1568 y Fr(Note)17 b(that)f(the)h(algorithm)c(is)j(relativ)o(e)g(to)g(another)g(simple)f (searc)o(h)i(algorithm)c Fd(pick)257 1618 y Fr(that)k(for)g(a)f(giv)o (en)h(set)h Fo(C)h Fj(\()e Fo(V)26 b Fr(and)17 b(distance)g(function)g Fo(d)5 b Fr(:)13 b Fo(V)26 b Fp(!)16 b Fj(N)10 b Fp([)h(f1g)k Fr(yields)257 1668 y(some)h Fd(pick)q Fr(\()p Fo(C)q(;)7 b(d)p Fr(\))15 b Fp(2)h Fo(V)21 b Fp(n)11 b Fo(C)19 b Fr(whic)o(h)e(among)e(all)g Fo(a)h Fp(2)g Fo(V)21 b Fp(n)11 b Fo(C)19 b Fr(has)e(minim)o(al)c(distance)257 1718 y Fo(d)p Fr(\()p Fo(a)p Fr(\).)307 1773 y(In)18 b(table)g(2)f(b)q(elo)o (w)h(w)o(e)g(sho)o(w)f(ho)o(w)h(the)g(next-function)g(is)g (constructed,)i(for)e(the)257 1823 y(same)13 b(example)g(as)h(b)q (efore.)1639 1840 y Ff(sp)q(ec)257 1895 y Fe(1.2.)21 b Fq(Sp)n(e)n(ci\014c)n(ation)p Fr(.)36 b(Let)20 b(#)p Fo(C)i Fr(denote)f(the)f(n)o(um)o(b)q(er)f(of)g(elemen)o(ts)g(of)g Fo(C)j Fr(\(see)f(2.2)257 1945 y(b)q(elo)o(w)15 b(for)f(ho)o(w)g(coun)o (ting)g(ma)o(y)e(b)q(e)j(treated)h(formally\).)h(W)m(e)d(shall)f(pro)o (v)o(e,)h(for)g(ev)o(ery)257 1995 y Fo(n)e(<)g(N)292 2072 y Fr(#)p Fo(C)357 2078 y Fi(n)390 2072 y Fr(=)g Fo(n)d Fr(+)h(1)p Fo(;)1043 b Fr(\(2\))292 2134 y Fo(d)314 2140 y Fi(n)336 2134 y Fr(\(0\))12 b(=)g(0)p Fo(;)1108 b Fr(\(3\))292 2197 y Fo(a)p Fp(6)p Fr(=0)11 b Fp(!)g Fd(nxt)487 2203 y Fi(n)510 2197 y Fr(\()p Fo(a)p Fr(\))g Fp(6)p Fr(=)h Fo(a;)933 b Fr(\(4\))292 2259 y Fd(nxt)347 2265 y Fi(n)370 2259 y Fr(\()p Fo(a)p Fr(\))12 b Fp(2)f Fo(C)505 2265 y Fi(n)537 2259 y Fp(^)d Fo(d)595 2265 y Fi(n)618 2259 y Fr(\()p Fo(a)p Fr(\))j(=)h Fo(d)749 2265 y Fi(n)771 2259 y Fr(\()p Fd(nxt)843 2265 y Fi(n)866 2259 y Fr(\()p Fo(a)p Fr(\)\))d(+)h Fo(w)q Fr(\()p Fo(a;)d Fd(nxt)1130 2265 y Fi(n)1152 2259 y Fr(\()p Fo(a)p Fr(\)\))p Fo(;)352 b Fr(\(5\))292 2321 y Fo(b)11 b Fp(2)g Fo(C)390 2327 y Fi(n)424 2321 y Fp(!)g Fo(d)499 2327 y Fi(n)521 2321 y Fr(\()p Fo(a)p Fr(\))h Fp(\024)g Fo(d)653 2327 y Fi(n)675 2321 y Fr(\()p Fo(b)p Fr(\))e(+)f Fo(w)q Fr(\()p Fo(a;)e(b)p Fr(\))i Fp(^)g Fr(\()p Fo(a)i(<)h(N)k Fp(!)11 b Fo(d)1161 2327 y Fi(n)1184 2321 y Fr(\()p Fo(a)p Fr(\))g Fo(<)h(d)1315 2327 y Fi(n)1337 2321 y Fr(\()p Fo(b)p Fr(\))g Fp(!)f Fo(a)h Fp(2)f Fo(C)1555 2327 y Fi(n)1577 2321 y Fr(\))p Fo(:)1586 2371 y Fr(\(6\))938 2510 y(4)p eop %%Page: 5 5 5 4 bop 332 210 1233 2 v 331 260 2 50 v 948 260 V 1564 260 V 331 298 V 440 283 a Fr(Up)q(date)15 b(distance,)f(next)p 948 298 V 284 w(Pic)o(k)g(new)g(no)q(de)p 1564 298 V 331 348 V 948 348 V 1564 348 V 332 338 1233 2 v 331 387 2 50 v 948 387 V 1564 387 V 331 669 2 294 v 357 654 a Fo(d)379 660 y Fk(0)397 654 y Fr(:)524 457 y Fh(\000)482 498 y(\000)465 515 y(\000)-42 b(\011)524 615 y(@)482 573 y(@)465 556 y(@)g(I)p 565 416 200 2 v 723 457 a(\000)681 498 y(\000)640 540 y(\000)598 581 y(\000)565 615 y(\000)p 565 615 V 822 515 a(@)781 473 y(@)764 457 y(@)822 556 y(\000)781 598 y(\000)764 615 y(\000)495 588 y Fr(2)495 469 y(1)814 588 y(1)814 469 y(2)654 647 y(5)654 409 y(8)644 518 y(1)422 528 y(0)432 515 y Fg(i)555 399 y Fr(1)565 385 y Fg(i)555 657 y Fr(2)565 644 y Fg(i)p 948 669 2 294 v 974 654 a Fo(p)995 660 y Fk(0)1013 654 y Fr(:)1140 457 y Fh(\000)1098 498 y(\000)1081 515 y(\000)g(\011)1140 615 y(@)1098 573 y(@)1081 556 y(@)g(I)p 1181 416 200 2 v 1339 457 a(\000)1297 498 y(\000)1256 540 y(\000)1214 581 y(\000)1181 615 y(\000)p 1181 615 V 1438 515 a(@)1397 473 y(@)1380 457 y(@)1438 556 y(\000)1397 598 y(\000)1380 615 y(\000)1111 588 y Fr(2)1111 469 y(1)1430 588 y(1)1430 469 y(2)1270 647 y(5)1270 409 y(8)1260 518 y(1)1171 425 y Fp(\017)1038 528 y Fr(0)1048 515 y Fg(i)1171 399 y Fr(1)1181 385 y Fg(i)1171 657 y Fr(2)1181 644 y Fg(i)p 1564 669 2 294 v 331 719 2 50 v 948 719 V 1564 719 V 332 709 1233 2 v 331 759 2 50 v 948 759 V 1564 759 V 331 1041 2 294 v 357 1026 a Fo(d)379 1032 y Fk(1)397 1026 y Fr(:)524 828 y Fh(\000)482 870 y(\000)465 886 y(\000)g(\011)524 986 y(@)482 945 y(@)465 928 y(@)g(I)p 565 788 200 2 v 565 787 a(\033)723 828 y(\000)681 870 y(\000)640 911 y(\000)598 953 y(\000)565 986 y(\000)p 565 987 V 822 886 a(@)781 845 y(@)764 828 y(@)822 928 y(\000)781 970 y(\000)764 986 y(\000)495 960 y Fr(2)495 840 y(1)814 960 y(1)814 840 y(2)654 1019 y(5)654 780 y(8)644 890 y(1)555 796 y Fp(\017)565 986 y Fg(d)422 900 y Fr(0)432 886 y Fg(i)555 770 y Fr(1)565 757 y Fg(i)555 1029 y Fr(2)565 1016 y Fg(i)754 770 y Fr(9)764 757 y Fg(i)p 948 1041 2 294 v 974 1026 a Fo(p)995 1032 y Fk(1)1013 1026 y Fr(:)1140 828 y Fh(\000)1098 870 y(\000)1081 886 y(\000)g(\011)1140 986 y(@)1098 945 y(@)1081 928 y(@)g(I)p 1181 788 200 2 v 1181 787 a(\033)1339 828 y(\000)1297 870 y(\000)1256 911 y(\000)1214 953 y(\000)1181 986 y(\000)p 1181 987 V 1438 886 a(@)1397 845 y(@)1380 828 y(@)1438 928 y(\000)1397 970 y(\000)1380 986 y(\000)1111 960 y Fr(2)1111 840 y(1)1430 960 y(1)1430 840 y(2)1270 1019 y(5)1270 780 y(8)1260 890 y(1)1171 796 y Fp(\017)1171 995 y(\017)1038 900 y Fr(0)1048 886 y Fg(i)1171 770 y Fr(1)1181 757 y Fg(i)1171 1029 y Fr(2)1181 1016 y Fg(i)1370 770 y Fr(9)1380 757 y Fg(i)p 1564 1041 2 294 v 331 1091 2 50 v 948 1091 V 1564 1091 V 332 1081 1233 2 v 331 1130 2 50 v 948 1130 V 1564 1130 V 331 1412 2 294 v 357 1398 a Fo(d)379 1404 y Fk(2)397 1398 y Fr(:)524 1200 y Fh(\000)482 1241 y(\000)465 1258 y(\000)g(\011)524 1358 y(@)482 1316 y(@)465 1300 y(@)g(I)p 565 1159 200 2 v 723 1200 a(\000)681 1241 y(\000)640 1283 y(\000)598 1324 y(\000)565 1358 y(\000)g(\011)p 565 1359 V -42 w(\033)822 1258 y(@)781 1217 y(@)764 1200 y(@)822 1300 y(\000)781 1341 y(\000)764 1358 y(\000)495 1331 y Fr(2)495 1212 y(1)814 1331 y(1)814 1212 y(2)654 1391 y(5)654 1152 y(8)644 1261 y(1)555 1168 y Fp(\017)555 1367 y(\017)764 1358 y Fg(d)422 1271 y Fr(0)432 1258 y Fg(i)555 1142 y Fr(1)565 1129 y Fg(i)555 1401 y Fr(2)565 1388 y Fg(i)754 1142 y Fr(3)764 1129 y Fg(i)754 1401 y Fr(7)764 1388 y Fg(i)p 948 1412 2 294 v 974 1398 a Fo(p)995 1404 y Fk(2)1013 1398 y Fr(:)1140 1200 y Fh(\000)1098 1241 y(\000)1081 1258 y(\000)g(\011)1140 1358 y(@)1098 1316 y(@)1081 1300 y(@)g(I)p 1181 1159 200 2 v 1339 1200 a(\000)1297 1241 y(\000)1256 1283 y(\000)1214 1324 y(\000)1181 1358 y(\000)g(\011)p 1181 1359 V -42 w(\033)1438 1258 y(@)1397 1217 y(@)1380 1200 y(@)1438 1300 y(\000)1397 1341 y(\000)1380 1358 y(\000)1111 1331 y Fr(2)1111 1212 y(1)1430 1331 y(1)1430 1212 y(2)1270 1391 y(5)1270 1152 y(8)1260 1261 y(1)1171 1168 y Fp(\017)1171 1367 y(\017)1370 1168 y(\017)1038 1271 y Fr(0)1048 1258 y Fg(i)1171 1142 y Fr(1)1181 1129 y Fg(i)1171 1401 y Fr(2)1181 1388 y Fg(i)1370 1142 y Fr(3)1380 1129 y Fg(i)1370 1401 y Fr(7)1380 1388 y Fg(i)p 1564 1412 2 294 v 331 1462 2 50 v 948 1462 V 1564 1462 V 332 1452 1233 2 v 331 1502 2 50 v 948 1502 V 1564 1502 V 331 1784 2 294 v 357 1769 a Fo(d)379 1775 y Fk(3)397 1769 y Fr(:)524 1572 y Fh(\000)482 1613 y(\000)465 1630 y(\000)g(\011)524 1729 y(@)482 1688 y(@)465 1671 y(@)g(I)p 565 1531 200 2 v 723 1572 a(\000)681 1613 y(\000)640 1655 y(\000)598 1696 y(\000)565 1729 y(\000)g(\011)p 565 1730 V -42 w(\033)822 1630 y(@)781 1588 y(@)764 1572 y(@)g(I)822 1671 y(\000)781 1713 y(\000)764 1729 y(\000)495 1703 y Fr(2)495 1583 y(1)814 1703 y(1)814 1583 y(2)654 1762 y(5)654 1523 y(8)644 1633 y(1)555 1539 y Fp(\017)555 1738 y(\017)754 1539 y(\017)422 1643 y Fr(0)432 1630 y Fg(i)555 1513 y Fr(1)565 1500 y Fg(i)555 1772 y Fr(2)565 1759 y Fg(i)754 1513 y Fr(3)764 1500 y Fg(i)754 1772 y Fr(7)764 1759 y Fg(i)884 1643 y Fr(5)894 1630 y Fg(i)p 948 1784 2 294 v 974 1769 a Fo(p)995 1775 y Fk(3)1013 1769 y Fr(:)1140 1572 y Fh(\000)1098 1613 y(\000)1081 1630 y(\000)g(\011)1140 1729 y(@)1098 1688 y(@)1081 1671 y(@)g(I)p 1181 1531 200 2 v 1339 1572 a(\000)1297 1613 y(\000)1256 1655 y(\000)1214 1696 y(\000)1181 1729 y(\000)g(\011)p 1181 1730 V -42 w(\033)1438 1630 y(@)1397 1588 y(@)1380 1572 y(@)g(I)1438 1671 y(\000)1397 1713 y(\000)1380 1729 y(\000)1111 1703 y Fr(2)1111 1583 y(1)1430 1703 y(1)1430 1583 y(2)1270 1762 y(5)1270 1523 y(8)1260 1633 y(1)1171 1539 y Fp(\017)1171 1738 y(\017)1370 1539 y(\017)1466 1639 y(\017)1038 1643 y Fr(0)1048 1630 y Fg(i)1171 1513 y Fr(1)1181 1500 y Fg(i)1171 1772 y Fr(2)1181 1759 y Fg(i)1370 1513 y Fr(3)1380 1500 y Fg(i)1370 1772 y Fr(7)1380 1759 y Fg(i)1499 1643 y Fr(5)1510 1630 y Fg(i)p 1564 1784 2 294 v 331 1834 2 50 v 948 1834 V 1564 1834 V 332 1824 1233 2 v 331 1874 2 50 v 948 1874 V 1564 1874 V 331 2156 2 294 v 357 2141 a Fo(d)379 2147 y Fk(4)397 2141 y Fr(:)524 1943 y Fh(\000)482 1985 y(\000)465 2001 y(\000)g(\011)524 2101 y(@)482 2059 y(@)465 2043 y(@)g(I)p 565 1902 200 2 v 723 1943 a(\000)681 1985 y(\000)640 2026 y(\000)598 2068 y(\000)565 2101 y(\000)g(\011)p 565 2102 V 822 2001 a(@)781 1960 y(@)764 1943 y(@)g(I)764 2101 y(\000)806 2059 y(\000)822 2043 y(\000)g(\022)495 2074 y Fr(2)495 1955 y(1)814 2074 y(1)814 1955 y(2)654 2134 y(5)654 1895 y(8)644 2005 y(1)555 1911 y Fp(\017)555 2110 y(\017)754 1911 y(\017)854 2010 y(\017)422 2015 y Fr(0)432 2001 y Fg(i)555 1885 y Fr(1)565 1872 y Fg(i)555 2144 y Fr(2)565 2131 y Fg(i)754 1885 y Fr(3)764 1872 y Fg(i)754 2144 y Fr(6)764 2131 y Fg(i)884 2015 y Fr(5)894 2001 y Fg(i)p 948 2156 2 294 v 974 2141 a Fo(p)995 2147 y Fk(4)1013 2141 y Fr(:)1140 1943 y Fh(\000)1098 1985 y(\000)1081 2001 y(\000)g(\011)1140 2101 y(@)1098 2059 y(@)1081 2043 y(@)g(I)p 1181 1902 200 2 v 1339 1943 a(\000)1297 1985 y(\000)1256 2026 y(\000)1214 2068 y(\000)1181 2101 y(\000)g(\011)p 1181 2102 V 1438 2001 a(@)1397 1960 y(@)1380 1943 y(@)g(I)1380 2101 y(\000)1422 2059 y(\000)1438 2043 y(\000)g(\022)1111 2074 y Fr(2)1111 1955 y(1)1430 2074 y(1)1430 1955 y(2)1270 2134 y(5)1270 1895 y(8)1260 2005 y(1)1171 1911 y Fp(\017)1171 2110 y(\017)178 b(\017)1370 1911 y(\017)1470 2010 y(\017)1038 2015 y Fr(0)1048 2001 y Fg(i)1171 1885 y Fr(1)1181 1872 y Fg(i)1171 2144 y Fr(2)1181 2131 y Fg(i)1370 1885 y Fr(3)1380 1872 y Fg(i)1370 2144 y Fr(6)1380 2131 y Fg(i)1499 2015 y Fr(5)1510 2001 y Fg(i)p 1564 2156 2 294 v 331 2205 2 50 v 948 2205 V 1564 2205 V 332 2207 1233 2 v 274 2323 a Fr(T)m(able)13 b(2:)18 b(An)c(example)e(for)i(the)h Fm(Dijkstra)e Fr(Algorithm,)e (with)j(the)g(next-function)938 2510 y(5)p eop %%Page: 6 6 6 5 bop 257 195 a Fr(Let)13 b(us)f(\014rst)h(argue)g(that)f (\(2\){\(6\))g(for)f Fo(n)h Fr(:=)f Fo(N)g Fp(\000)6 b Fr(1)11 b(can)i(b)q(e)f(view)o(ed)h(as)f(a)f(sp)q(eci\014cation)257 245 y(of)j(the)g Fm(Dijkstra)g Fr(algorithm.)307 303 y(Ev)o(ery)f(no)q(de)h Fo(a)d(<)h(N)18 b Fr(is)12 b(in)g Fo(C)770 309 y Fi(N)s Fn(\000)p Fk(1)857 303 y Fr(b)o(y)h(\(2\).)k(By)d (\(4\))f(and)f(\(5\),)h Fo(d)1306 309 y Fi(N)s Fn(\000)p Fk(1)1379 303 y Fr(\()p Fd(nxt)1451 309 y Fi(N)s Fn(\000)p Fk(1)1525 303 y Fr(\()p Fo(a)p Fr(\)\))f Fo(<)257 353 y(d)279 359 y Fi(N)s Fn(\000)p Fk(1)353 353 y Fr(\()p Fo(a)p Fr(\))20 b(for)g Fo(a)j Fp(6)p Fr(=)f(0.)37 b(Hence)22 b(the)f(path)f Fo(a;)7 b Fd(nxt)1073 359 y Fi(N)s Fn(\000)p Fk(1)1147 353 y Fr(\()p Fo(a)p Fr(\))p Fo(;)g Fd(nxt)1275 359 y Fi(N)s Fn(\000)p Fk(1)1349 353 y Fr(\()p Fd(nxt)1421 359 y Fi(N)s Fn(\000)p Fk(1)1495 353 y Fr(\()p Fo(a)p Fr(\)\))p Fo(;)g(:)g(:)g(:)257 403 y Fr(m)o(ust)15 b(lead)g(to)g(0,)g (and)g(b)o(y)g(\(5\))h Fo(d)783 409 y Fi(N)s Fn(\000)p Fk(1)856 403 y Fr(\()p Fo(a)p Fr(\))g(giv)o(es)f(the)g(distance)i(of)d Fo(a)h Fr(along)f(this)i(path.)257 452 y(It)f(remains)f(to)h(sho)o(w)g (that)g(an)o(y)g(other)h(path)f Fo(f)k Fr(with)c(asso)q(ciated)h (distance)g(function)257 502 y Fo(d)e Fr(yields)g(a)f(distance)i (greater)g(than)f(or)f(equal)h(to)g(this)g(one,)f(i.e.)257 585 y Fe(1.3.)22 b(Theorem.)e Fq(\(Corr)n(e)n(ctness\).)325 677 y Fp(8)p Fo(d;)7 b(f)r(;)g(n)g Fr([)p Fo(f)t Fr(\(0\))k(=)h(0)f Fp(!)g(8)p Fo(m<)q(n)p Fr(+1)c(\()p Fo(f)t Fr(\()p Fo(m)p Fr(\))13 b Fo(<)f(N)5 b Fr(\))11 b Fp(!)495 739 y(8)p Fo(m<)q(n)p Fr(+1)c([)p Fo(d)p Fr(\()p Fo(f)t Fr(\()p Fo(m)p Fr(\)\))j(+)f Fo(w)q Fr(\()p Fo(f)t Fr(\()p Fo(m)p Fr(\))p Fo(;)e(f)t Fr(\()p Fo(m)12 b Fr(+)d(1\)\))j(=)g Fo(d)p Fr(\()p Fo(f)t Fr(\()p Fo(m)e Fr(+)f(1\)\)])j Fp(!)495 801 y Fo(d)517 807 y Fi(N)s Fn(\000)p Fk(1)590 801 y Fr(\()p Fo(f)t Fr(\()p Fo(n)p Fr(\)\))h Fp(\024)f Fo(d)p Fr(\()p Fo(f)t Fr(\()p Fo(n)p Fr(\)\)])p Fo(:)307 901 y Fr(Of)e(course,)h(w)o(e)f(could)g(a)o(v)o(oid)f(to)g(in)o(tro)q (duce)i(the)f(v)n(ariable)f Fo(d)g Fr(and)h(instead)g(of)f Fo(d)p Fr(\()p Fo(f)t Fr(\()p Fo(n)p Fr(\)\))257 951 y(use)333 919 y Fc(P)377 930 y Fi(n)377 963 y(i)p Fk(=1)440 951 y Fo(w)q Fr(\()p Fo(f)t Fr(\()p Fo(i)k Fp(\000)f Fr(1\))p Fo(;)7 b(f)t Fr(\()p Fo(i)p Fr(\)\).)31 b(Ho)o(w)o(ev)o(er,)19 b(the)f(formal)e(pro)q(of)h(gets)i(more)e(readable)257 1000 y(when)e(w)o(e)f(use)h Fo(d)p Fr(.)257 1092 y Fq(Pr)n(o)n(of.)20 b Fr(By)e(induction)e(on)h Fo(n)p Fr(.)28 b Fq(Base)20 b Fo(n)d Fr(=)g(0.)28 b(Immediate)14 b(from)h(\(3\).)28 b Fq(Step)20 b Fo(n)11 b Fr(+)h(1.)257 1142 y(First)j(note)f(that)g(b)o (y)g(\(2\))g(at)g(stage)g Fo(N)g Fp(\000)c Fr(1)j(all)g(no)q(des)i(are) f(computed.)j(Hence)305 1233 y Fo(d)327 1239 y Fi(N)s Fn(\000)p Fk(1)400 1233 y Fr(\()p Fo(f)t Fr(\()p Fo(n)10 b Fr(+)g(1\)\))i Fp(\024)f Fo(d)663 1239 y Fi(N)s Fn(\000)p Fk(1)737 1233 y Fr(\()p Fo(f)t Fr(\()p Fo(n)p Fr(\)\))f(+)g Fo(w)q Fr(\()p Fo(f)t Fr(\()p Fo(n)p Fr(\))p Fo(;)d(f)t Fr(\()p Fo(n)j Fr(+)g(1\)\))42 b(b)o(y)14 b(\(6\))598 1295 y Fp(\024)d Fo(d)p Fr(\()p Fo(f)t Fr(\()p Fo(n)p Fr(\)\))f(+)g Fo(w)q Fr(\()p Fo(f)t Fr(\()p Fo(n)p Fr(\))p Fo(;)d(f)t Fr(\()p Fo(n)k Fr(+)e(1\)\))116 b(b)o(y)13 b(ind.)g(h)o(yp)q(othesis)598 1357 y(=)e Fo(d)p Fr(\()p Fo(f)t Fr(\()p Fo(n)f Fr(+)g(1\)\))p Fo(:)p 1609 1449 2 29 v 1611 1422 25 2 v 1611 1449 V 1636 1449 2 29 v 257 1532 a Fe(1.4.)21 b Fr(It)14 b(remains)e(to)h(pro)o(v)o(e)g(the)h (in)o(v)n(arian)o(ts)d(\(2\){\(6\),)i(b)o(y)g(induction)g(on)f Fo(n)p Fr(.)18 b(The)c(base)257 1582 y(case)h Fo(n)d Fr(=)g(0)i(is)g(ob)o(vious.)j(F)m(or)d(the)g(step)h(case)g(assume)f (that)g(\(2\){\(6\))g(hold)f(for)h Fo(n)p Fr(,)f(and)257 1631 y(that)h Fo(p)368 1637 y Fi(n)405 1631 y Fr(is)f(c)o(hosen)i (according)f(to)g(\(1\),)f(i.e.)446 1723 y Fo(p)467 1729 y Fi(n)501 1723 y Fo(<)f(N)i Fp(^)9 b Fo(p)650 1729 y Fi(n)688 1723 y Fo(=)-25 b Fp(2)11 b Fo(C)753 1729 y Fi(n)785 1723 y Fp(^)d(8)p Fo(a<)q(N)k Fr(\()p Fo(d)982 1729 y Fi(n)1004 1723 y Fr(\()p Fo(a)p Fr(\))g Fo(<)f(d)1135 1729 y Fi(n)1158 1723 y Fr(\()p Fo(p)1195 1729 y Fi(n)1217 1723 y Fr(\))h Fp(!)f Fo(a)g Fp(2)h Fo(C)1401 1729 y Fi(n)1423 1723 y Fr(\))p Fo(:)1639 1756 y Fb(lem)257 1814 y Fe(Lemma.)21 b Fp(8)p Fo(a)p Fp(2)o Fo(C)547 1820 y Fi(n)577 1814 y Fr(\()p Fo(d)615 1820 y Fi(n)p Fk(+1)679 1814 y Fr(\()p Fo(a)p Fr(\))12 b(=)g Fo(d)811 1820 y Fi(n)833 1814 y Fr(\()p Fo(a)p Fr(\)\))p Fq(.)257 1905 y(Pr)n(o)n(of.)20 b Fr(Let)13 b Fo(a)f Fp(2)f Fo(C)563 1911 y Fi(n)597 1905 y Fr(b)q(e)i(giv)o(en.)k(The)c(claim)d(follo)o(ws) h(from)f(the)j(de\014nition)f(of)g Fo(d)1521 1911 y Fi(n)p Fk(+1)1585 1905 y Fr(\()p Fo(a)p Fr(\))257 1955 y(and)263 2046 y Fo(d)285 2052 y Fi(n)308 2046 y Fr(\()p Fo(a)p Fr(\))f Fp(\024)h Fo(d)439 2052 y Fi(n)461 2046 y Fr(\()p Fo(p)498 2052 y Fi(n)521 2046 y Fr(\))251 b(since)15 b(otherwise)g Fo(p)1096 2052 y Fi(n)1130 2046 y Fp(2)c Fo(C)1199 2052 y Fi(n)1235 2046 y Fr(b)o(y)j(ind.)f(h)o(yp)q(othesis)h (\(6\))373 2109 y Fp(\024)e Fo(d)439 2115 y Fi(n)461 2109 y Fr(\()p Fo(p)498 2115 y Fi(n)521 2109 y Fr(\))d(+)h Fo(w)q Fr(\()p Fo(a;)d(p)697 2115 y Fi(n)719 2109 y Fr(\))p Fo(:)p 1609 2200 V 1611 2174 25 2 v 1611 2200 V 1636 2200 2 29 v 307 2291 a Fr(No)o(w)19 b(\(2\))f(follo)o(ws)e(from)h Fo(p)742 2297 y Fi(n)783 2291 y Fo(<)i(N)e Fp(^)12 b Fo(p)945 2297 y Fi(n)990 2291 y Fo(=)-25 b Fp(2)18 b Fo(C)1062 2297 y Fi(n)1084 2291 y Fr(,)h(and)f(\(3\),)h(\(4\))f(follo)o (w)e(from)h(the)257 2341 y(de\014nition)d(and)g(the)g(induction)g(h)o (yp)q(othesis.)938 2510 y(6)p eop %%Page: 7 7 7 6 bop 257 195 a Fe(1.5.)21 b Fq(Pr)n(o)n(of)d(of)42 b Fp(8)p Fo(a)7 b Fr(\()p Fd(nxt)667 201 y Fi(n)p Fk(+1)732 195 y Fr(\()p Fo(a)p Fr(\))17 b Fp(2)g Fo(C)878 201 y Fi(n)p Fk(+1)943 195 y Fr(\).)28 b(By)18 b(de\014nition)f(w)o(e)h(ha)o (v)o(e)f Fd(nxt)1475 201 y Fi(n)p Fk(+1)1540 195 y Fr(\()p Fo(a)p Fr(\))h Fp(2)257 245 y(f)p Fd(nxt)334 251 y Fi(n)356 245 y Fr(\()p Fo(a)p Fr(\))p Fo(;)7 b(p)450 251 y Fi(n)472 245 y Fp(g)p Fr(,)18 b(and)f(b)o(y)g(induction)g(h)o(yp)q(othesis)h (\(5\))g Fd(nxt)1190 251 y Fi(n)1213 245 y Fr(\()p Fo(a)p Fr(\))f Fp(2)g Fo(C)1359 251 y Fi(n)1399 245 y Fp(\022)g Fo(C)1478 251 y Fi(n)p Fk(+1)1543 245 y Fr(,)g(and)257 295 y(also)d Fo(p)362 301 y Fi(n)396 295 y Fp(2)d Fo(C)465 301 y Fi(n)p Fk(+1)541 295 y Fr(=)g Fo(C)614 301 y Fi(n)646 295 y Fp([)e(f)p Fo(p)725 301 y Fi(n)747 295 y Fp(g)p Fr(.)257 366 y Fe(1.6.)21 b Fq(Pr)n(o)n(of)d(of)42 b Fp(8)p Fo(a)7 b Fr(\()p Fo(d)633 372 y Fi(n)p Fk(+1)697 366 y Fr(\()p Fo(a)p Fr(\))18 b(=)f Fo(d)840 372 y Fi(n)p Fk(+1)904 366 y Fr(\()p Fd(nxt)976 372 y Fi(n)p Fk(+1)1040 366 y Fr(\()p Fo(a)p Fr(\)\))12 b(+)g Fo(w)q Fr(\()p Fo(a;)7 b Fd(nxt)1309 372 y Fi(n)p Fk(+1)1374 366 y Fr(\()p Fo(a)p Fr(\)\)\).)28 b Fq(Case)20 b Fr(1:)257 416 y Fo(d)279 422 y Fi(n)302 416 y Fr(\()p Fo(p)339 422 y Fi(n)361 416 y Fr(\))10 b(+)h Fo(w)q Fr(\()p Fo(a;)c(p)539 422 y Fi(n)560 416 y Fr(\))14 b Fo(<)g(d)658 422 y Fi(n)680 416 y Fr(\()p Fo(a)p Fr(\).)22 b(Note)15 b(that)g Fo(d)982 422 y Fi(n)p Fk(+1)1047 416 y Fr(\()p Fo(p)1084 422 y Fi(n)1106 416 y Fr(\))f(=)g Fo(d)1204 422 y Fi(n)1226 416 y Fr(\()p Fo(p)1263 422 y Fi(n)1286 416 y Fr(\),)h(since)g Fo(d)1453 422 y Fi(n)p Fk(+1)1518 416 y Fr(\()p Fo(p)1555 422 y Fi(n)1577 416 y Fr(\))f(=)257 466 y(min)o Fp(f)p Fo(d)370 472 y Fi(n)392 466 y Fr(\()p Fo(p)429 472 y Fi(n)451 466 y Fr(\))c(+)f Fo(w)q Fr(\()p Fo(p)586 472 y Fi(n)608 466 y Fo(;)e(p)648 472 y Fi(n)670 466 y Fr(\))p Fo(;)g(d)727 472 y Fi(n)749 466 y Fr(\()p Fo(p)786 472 y Fi(n)809 466 y Fr(\))p Fp(g)p Fr(.)18 b(Then)c(w)o(e)g(ha)o(v)o(e)294 543 y Fo(d)316 549 y Fi(n)p Fk(+1)380 543 y Fr(\()p Fo(a)p Fr(\))305 605 y(=)e Fo(d)371 611 y Fi(n)p Fk(+1)435 605 y Fr(\()p Fo(p)472 611 y Fi(n)495 605 y Fr(\))d(+)h Fo(w)q Fr(\()p Fo(a;)d(p)671 611 y Fi(n)693 605 y Fr(\))303 b(b)o(y)14 b(de\014nition)g(and)f(the)i(note)f(ab)q(o)o(v)o(e)305 668 y(=)e Fo(d)371 674 y Fi(n)p Fk(+1)435 668 y Fr(\()p Fd(nxt)507 674 y Fi(n)p Fk(+1)572 668 y Fr(\()p Fo(a)p Fr(\)\))d(+)h Fo(w)q Fr(\()p Fo(a;)d Fd(nxt)836 674 y Fi(n)p Fk(+1)900 668 y Fr(\()p Fo(a)p Fr(\)\))42 b(b)o(y)14 b(de\014nition)g(of)f Fd(nxt)1357 674 y Fi(n)p Fk(+1)1422 668 y Fr(\()p Fo(a)p Fr(\))p Fo(:)257 745 y Fq(Case)21 b Fr(2:)k(Otherwise.)30 b(Then)18 b(b)o(y)f(de\014nition)g Fo(d)1029 751 y Fi(n)p Fk(+1)1093 745 y Fr(\()p Fo(a)p Fr(\))h(=)g Fo(d)1237 751 y Fi(n)1259 745 y Fr(\()p Fo(a)p Fr(\))g(and)f Fd(nxt)1471 751 y Fi(n)p Fk(+1)1535 745 y Fr(\()p Fo(a)p Fr(\))h(=)257 795 y Fd(nxt)313 801 y Fi(n)336 795 y Fr(\()p Fo(a)p Fr(\),)f(hence)h(the)g(claim)c(follo)o (ws)i(from)f(the)i(induction)g(h)o(yp)q(othesis)h(and)e(lemma)257 845 y(1.4,)d(using)g Fd(nxt)500 851 y Fi(n)523 845 y Fr(\()p Fo(a)p Fr(\))e Fp(2)h Fo(C)658 851 y Fi(n)680 845 y Fr(.)257 916 y Fe(1.7.)21 b Fq(Pr)n(o)n(of)15 b(of)g Fp(8)p Fo(a;)7 b(b)g Fr([)p Fo(b)k Fp(2)g Fo(C)712 922 y Fi(n)p Fk(+1)788 916 y Fp(!)h Fo(d)864 922 y Fi(n)p Fk(+1)928 916 y Fr(\()p Fo(a)p Fr(\))g Fp(\024)g Fo(d)1060 922 y Fi(n)p Fk(+1)1125 916 y Fr(\()p Fo(b)p Fr(\))d(+)h Fo(w)q Fr(\()p Fo(a;)d(b)p Fr(\)].)17 b(Let)e Fo(b)d Fp(2)f Fo(C)1563 922 y Fi(n)p Fk(+1)1628 916 y Fr(.)257 966 y Fq(Case)17 b Fo(b)12 b Fp(2)f Fo(C)460 972 y Fi(n)482 966 y Fr(.)18 b(Then)459 1043 y Fo(d)481 1049 y Fi(n)p Fk(+1)545 1043 y Fr(\()p Fo(a)p Fr(\))12 b Fp(\024)g Fo(d)677 1049 y Fi(n)699 1043 y Fr(\()p Fo(a)p Fr(\))252 b(b)o(y)13 b(de\014nition)611 1105 y Fp(\024)f Fo(d)677 1111 y Fi(n)699 1105 y Fr(\()p Fo(b)p Fr(\))d(+)h Fo(w)q Fr(\()p Fo(a;)d(b)p Fr(\))83 b(b)o(y)13 b(induction)h(h)o(yp)q(othesis) 611 1168 y(=)e Fo(d)677 1174 y Fi(n)p Fk(+1)741 1168 y Fr(\()p Fo(b)p Fr(\))d(+)h Fo(w)q Fr(\()p Fo(a;)d(b)p Fr(\))41 b(b)o(y)13 b(the)i(lemma)m Fo(:)257 1245 y Fq(Case)23 b Fr(2:)28 b Fo(b)21 b Fr(=)g Fo(p)541 1251 y Fi(n)563 1245 y Fr(.)35 b(Again)18 b(note)i(that)f Fo(d)951 1251 y Fi(n)p Fk(+1)1016 1245 y Fr(\()p Fo(p)1053 1251 y Fi(n)1075 1245 y Fr(\))i(=)g Fo(d)1187 1251 y Fi(n)1209 1245 y Fr(\()p Fo(p)1246 1251 y Fi(n)1269 1245 y Fr(\),)f(since)g Fo(d)1446 1251 y Fi(n)p Fk(+1)1511 1245 y Fr(\()p Fo(p)1548 1251 y Fi(n)1570 1245 y Fr(\))h(=)257 1295 y(min)o Fp(f)p Fo(d)370 1301 y Fi(n)392 1295 y Fr(\()p Fo(p)429 1301 y Fi(n)451 1295 y Fr(\))10 b(+)f Fo(w)q Fr(\()p Fo(p)586 1301 y Fi(n)608 1295 y Fo(;)e(p)648 1301 y Fi(n)670 1295 y Fr(\))p Fo(;)g(d)727 1301 y Fi(n)749 1295 y Fr(\()p Fo(p)786 1301 y Fi(n)809 1295 y Fr(\))p Fp(g)p Fr(.)18 b(Then)521 1372 y Fo(d)543 1378 y Fi(n)p Fk(+1)607 1372 y Fr(\()p Fo(a)p Fr(\))12 b Fp(\024)g Fo(d)739 1378 y Fi(n)761 1372 y Fr(\()p Fo(p)798 1378 y Fi(n)821 1372 y Fr(\))d(+)h Fo(w)q Fr(\()p Fo(a;)d(p)997 1378 y Fi(n)1018 1372 y Fr(\))84 b(b)o(y)14 b(de\014nition)673 1434 y(=)e Fo(d)739 1440 y Fi(n)p Fk(+1)803 1434 y Fr(\()p Fo(p)840 1440 y Fi(n)863 1434 y Fr(\))d(+)h Fo(w)q Fr(\()p Fo(a;)d(p)1039 1440 y Fi(n)1060 1434 y Fr(\))42 b(b)o(y)14 b(the)g(remark)673 1496 y(=)e Fo(d)739 1502 y Fi(n)p Fk(+1)803 1496 y Fr(\()p Fo(b)p Fr(\))d(+)h Fo(w)q Fr(\()p Fo(a;)d(b)p Fr(\))p Fo(:)257 1574 y Fe(1.8.)21 b Fq(Pr)n(o)n(of)16 b(of)g Fp(8)p Fo(a;)7 b(b)g Fr([)p Fo(b)12 b Fp(2)i Fo(C)718 1580 y Fi(n)p Fk(+1)796 1574 y Fp(!)f Fo(a)h(<)g(N)k Fp(!)13 b Fo(d)1061 1580 y Fi(n)p Fk(+1)1126 1574 y Fr(\()p Fo(a)p Fr(\))h Fo(<)g(d)1262 1580 y Fi(n)p Fk(+1)1326 1574 y Fr(\()p Fo(b)p Fr(\))g Fp(!)f Fo(a)h Fp(2)f Fo(C)1552 1580 y Fi(n)p Fk(+1)1616 1574 y Fr(].)257 1623 y(Assume)h Fo(b)e Fp(2)f Fo(C)510 1629 y Fi(n)p Fk(+1)575 1623 y Fr(,)i Fo(a)f(<)g(N)19 b Fr(and)13 b Fo(d)832 1629 y Fi(n)p Fk(+1)897 1623 y Fr(\()p Fo(a)p Fr(\))f Fo(<)g(d)1029 1629 y Fi(n)p Fk(+1)1093 1623 y Fr(\()p Fo(b)p Fr(\).)18 b Fq(Case)f Fo(d)1299 1629 y Fi(n)1322 1623 y Fr(\()p Fo(p)1359 1629 y Fi(n)1381 1623 y Fr(\))10 b(+)f Fo(w)q Fr(\()p Fo(a;)e(p)1557 1629 y Fi(n)1579 1623 y Fr(\))12 b Fo(<)257 1673 y(d)279 1679 y Fi(n)302 1673 y Fr(\()p Fo(a)p Fr(\),)h(i.e.)g Fo(d)470 1679 y Fi(n)p Fk(+1)534 1673 y Fr(\()p Fo(a)p Fr(\))f(=)g Fo(d)666 1679 y Fi(n)688 1673 y Fr(\()p Fo(p)725 1679 y Fi(n)748 1673 y Fr(\))d(+)h Fo(w)q Fr(\()p Fo(a;)d(p)924 1679 y Fi(n)945 1673 y Fr(\),)14 b(hence)549 1750 y Fo(d)571 1756 y Fi(n)594 1750 y Fr(\()p Fo(p)631 1756 y Fi(n)653 1750 y Fr(\))e Fp(\024)g Fo(d)747 1756 y Fi(n)769 1750 y Fr(\()p Fo(p)806 1756 y Fi(n)829 1750 y Fr(\))d(+)g Fo(w)q Fr(\()p Fo(a;)e(p)1004 1756 y Fi(n)1026 1750 y Fr(\))681 1813 y(=)12 b Fo(d)747 1819 y Fi(n)p Fk(+1)811 1813 y Fr(\()p Fo(a)p Fr(\))219 b(b)o(y)14 b(de\014nition)681 1875 y Fo(<)e(d)747 1881 y Fi(n)p Fk(+1)811 1875 y Fr(\()p Fo(b)p Fr(\))223 b(b)o(y)14 b(assumption)681 1937 y Fp(\024)e Fo(d)747 1943 y Fi(n)769 1937 y Fr(\()p Fo(b)p Fr(\))265 b(b)o(y)14 b(de\014nition)o Fo(:)257 2014 y Fq(Sub)n(c)n(ase)g Fo(b)d Fp(2)h Fo(C)506 2020 y Fi(n)528 2014 y Fr(.)k(Then)11 b(from)d(the)i(induction)g(h)o (yp)q(othesis)g(and)g(the)g(inequalit)o(y)e(ab)q(o)o(v)o(e)257 2064 y(w)o(e)j(ha)o(v)o(e)g Fo(p)429 2070 y Fi(n)463 2064 y Fp(2)g Fo(C)532 2070 y Fi(n)554 2064 y Fr(,)g(a)g(con)o (tradiction.)16 b Fq(Sub)n(c)n(ase)f Fo(b)c Fr(=)h Fo(p)1121 2070 y Fi(n)1144 2064 y Fr(.)17 b(Then)11 b(the)g(inequalit)o(y)e(ab)q (o)o(v)o(e)257 2114 y(immediately)i(yields)i(the)i(con)o(tradiction)f Fo(d)957 2120 y Fi(n)979 2114 y Fr(\()p Fo(p)1016 2120 y Fi(n)1038 2114 y Fr(\))e Fo(<)g(d)1132 2120 y Fi(n)1154 2114 y Fr(\()p Fo(p)1191 2120 y Fi(n)1214 2114 y Fr(\).)307 2169 y Fq(Case)17 b Fr(otherwise,)d(i.e.)f Fo(d)696 2175 y Fi(n)p Fk(+1)761 2169 y Fr(\()p Fo(a)p Fr(\))e(=)h Fo(d)892 2175 y Fi(n)914 2169 y Fr(\()p Fo(a)p Fr(\),)i(hence)649 2246 y Fo(d)671 2252 y Fi(n)693 2246 y Fr(\()p Fo(a)p Fr(\))e(=)g Fo(d)825 2252 y Fi(n)p Fk(+1)889 2246 y Fr(\()p Fo(a)p Fr(\))42 b(b)o(y)13 b(de\014nition)759 2309 y Fo(<)f(d)825 2315 y Fi(n)p Fk(+1)889 2309 y Fr(\()p Fo(b)p Fr(\))46 b(b)o(y)13 b(assumption)759 2371 y Fp(\024)f Fo(d)825 2377 y Fi(n)847 2371 y Fr(\()p Fo(b)p Fr(\))88 b(b)o(y)13 b(de\014nition)p Fo(:)938 2510 y Fr(7)p eop %%Page: 8 8 8 7 bop 257 195 a Fq(Sub)n(c)n(ase)23 b Fo(b)c Fp(2)g Fo(C)530 201 y Fi(n)552 195 y Fr(.)33 b(Then)19 b(from)e(the)i (induction)f(h)o(yp)q(othesis)h(w)o(e)g(obtain)f Fo(a)h Fp(2)g Fo(C)1605 201 y Fi(n)1628 195 y Fr(.)257 245 y Fq(Sub)n(c)n(ase)e Fo(b)11 b Fr(=)h Fo(p)504 251 y Fi(n)526 245 y Fr(.)18 b(Then)12 b(the)h(inequalit)o(y)e(ab)q(o)o(v)o(e)h (yields)g Fo(a)f Fp(2)h Fo(C)1257 251 y Fi(n)1291 245 y Fr(b)o(y)g(the)h(c)o(hoice)g(of)e Fo(p)1605 251 y Fi(n)1628 245 y Fr(.)257 386 y Fl(2)67 b(Some)22 b(commen)n(ts)g(on)h(the)f (formalization)257 483 y Fe(2.1.)f Fq(How)c(to)f(r)n(epr)n(esent)g(the) h(algorithm)f(in)h(the)g(formal)f(pr)n(o)n(of.)23 b Fr(There)17 b(are)g(sev)o(eral)257 533 y(w)o(a)o(ys)g(to)f(en)o(ter)i(the)f (de\014nition)f(of)g(the)h(program:)22 b(One)17 b(migh)o(t)e(use)i(a)f (constan)o(t)i(to-)257 583 y(gether)i(with)f(a)f(set)i(of)f(de\014ning) f(equations,)i(as)f(has)g(b)q(een)h(done)f(in)g(the)g(informal)257 633 y(pro)q(of)d(giv)o(en)g(ab)q(o)o(v)o(e.)26 b(This)16 b(w)o(ould)f(giv)o(e)h(rise)h(to)f(a)g(lot)g(of)g(equational)f (reasoning)i(in)257 682 y(the)f(formal)c(pro)q(of,)i(whic)o(h)g(can)h (easily)f(b)q(e)i(a)o(v)o(oided)e(if)f(w)o(e)i(en)o(ter)h(the)f (de\014nition)g(as)g(a)257 732 y(term)f(rewrite)h(system)e(and)h(iden)o (tify)f(terms)h(that)g(ha)o(v)o(e)f(the)i(same)e(normal)f(form.)307 788 y(Still,)17 b(there)i(are)f(t)o(w)o(o)f(w)o(a)o(ys)g(to)g(implemen) o(t)e(the)j(term)f(rewrite)h(system:)26 b(Either)257 838 y(one)18 b(uses)h(a)f(constan)o(t,)h(again,)e(and)g(implemen)o(ts)e (the)k(rewrite)g(rules)f(for)f(this)h(con-)257 888 y(stan)o(t)f (directly)m(,)g(or)g(one)f(en)o(ters)j(a)d(term)g(that)h(computes)f (the)h(algorithm)d(using)j(the)257 937 y(appropriate)j(recursors)i (already)e(implem)o(en)o(ted)e(in)i(the)g(system.)36 b(Both)20 b(metho)q(ds)257 987 y(ha)o(v)o(e)14 b(their)g(adv)n(an)o (tages)g(and)f(disadv)n(an)o(tages:)320 1067 y Fp(\017)20 b Fr(the)13 b(term)e(that)h(computes)g(the)h(algorithm)c(gets)k(rather) f(long)f(and)h(sho)o(ws)h(up)f(in)361 1117 y(the)h(form)o(ula)c (stating)i(its)h(correctness)j(more)c(than)h(once,)g(so)g(that)g(this)g (form)o(ula)361 1167 y(can)j(get)g(unreadable.)21 b(This)15 b(do)q(es)h(not)e(happ)q(en)i(if)e(w)o(e)h(use)g(constan)o(ts)h (instead)361 1217 y(\(similar)c(to)h(the)i(informal)c(pro)q(of)s(\).) 320 1295 y Fp(\017)20 b Fr(on)c(the)h(other)f(hand,)g(if)f(w)o(e)i(use) f(constan)o(ts,)h(w)o(e)g(are)f(only)f(able)h(to)g(deal)g(with)361 1345 y(the)g(case)h(distinctions)e(used)i(in)e(the)h(program)e(b)o(y)h (using)g(a)g(set)i(of)e(equations,)361 1395 y(again,)g(since)j(these)f (case)h(distinctions)e(do)g(not)g(sho)o(w)h(up)f(explicitly)g(and)g (are)361 1444 y(only)d(computed)h(when)g(the)h(constan)o(t)f(is)g (applied)f(to)h(concrete)i(data.)320 1523 y Fp(\017)k Fr(\014nally)m(,)10 b(if)g(w)o(e)h(use)g(a)g(term,)f(w)o(e)i(do)e(not)h (ha)o(v)o(e)g(to)g(w)o(orry)f(ab)q(out)h(termination)e(and)361 1573 y(con\015uence)16 b(of)e(our)g(term)g(rewrite)h(system,)f(since)h (these)h(are)f(already)f(c)o(hec)o(k)o(ed)361 1622 y(for)g(the)g (recursors)i(w)o(e)e(are)h(using.)257 1702 y(T)m(o)e(illustrate)h (these)h(p)q(oin)o(ts)e(and)h(the)g(use)g(of)f(program)f(extraction)i (in)f(our)h(example,)257 1752 y(w)o(e)g(sho)o(w)g(some)f(details)h(of)f (the)i(formalization:)307 1808 y(The)g Fm(Dijkstra)e Fr(algorithm)f(\(cf.)h(1.1\))g(is)h(giv)o(en)f(b)o(y)h(the)g(term)257 1888 y Fa(\(nat-rec)301 1938 y(\(\([a]a=0\))20 b(#)h(\([a]0\))g(#)h (\(w)f(0\)\))301 1987 y(\([n,cp*nxt*d])323 2037 y(\(\([a])g([if)g (a=\(pick)f(cp)h(d\)\))h(then)f(true)g(else)f(cp)i(a]\))f(#)345 2087 y(\([a])g([if)g(\(d)g(\(pick)g(cp)g(d\)\)+\(w)g(a)g(\(pick)g(cp)g (d\)\))h(<)f(\(d)h(a\))562 2137 y(then)f(\(pick)g(cp)h(d\))562 2187 y(else)f(\(nxt)g(a\)]\))g(#)345 2236 y(\([a])g([if)g(\(d)g(\(pick) g(cp)g(d\)\)+\(w)g(a)g(\(pick)g(cp)g(d\)\))h(<)f(\(d)h(a\))562 2286 y(then)f(\(d)h(\(pick)f(cp)g(d\)\)+\(w)g(a)g(\(pick)g(cp)g(d\)\)) 562 2336 y(else)g(\(d)h(a\)]\)\)\))257 2386 y(\(nn-1\))938 2510 y Fr(8)p eop %%Page: 9 9 9 8 bop 257 195 a Fr(F)m(or)14 b(readabilit)o(y)f(w)o(e)h(ha)o(v)o(e)f (replaced)629 284 y Fa(\(car)20 b(cp*nxt*d\))171 b Fr(b)o(y)41 b Fa(cp)p Fo(;)629 334 y Fa(\(car)20 b(\(cdr)h(cp*nxt*d\)\))40 b Fr(b)o(y)h Fa(nxt)p Fo(;)629 383 y Fa(\(cdr)20 b(\(cdr)h (cp*nxt*d\)\))40 b Fr(b)o(y)h Fa(d)p Fo(:)257 473 y Fr(This)16 b(term)f(de\014nes)i(triples)f(of)f(sets)i Fa(cp)f Fr(and)f(functions)h Fa(nxt)f Fr(and)h Fa(d)f Fr(for)g(ev)o(ery)i Fo(n)e Fr(b)o(y)257 523 y(recursion)g(o)o(v)o(er)f Fo(n)g Fr(using)g(the)g(recursor)i Fa(nat-rec)p Fr(.)g(The)f(result)f(is)g(the)g(triple)g(de\014ned)257 572 y(for)g Fa(nn-1)e Fr(\(corresp)q(onding)j(to)e Fo(N)h Fp(\000)8 b Fr(1)14 b(in)f(the)h(informal)c(pro)q(of)s(\).)18 b(W)m(e)c(ha)o(v)o(e)f(c)o(hosen)h(to)257 622 y(represen)o(t)j(the)f Fd(pick)p Fr(-function)f(\(computing)e Fo(p)1000 628 y Fi(n)1022 622 y Fr(\))i(b)o(y)g(a)f(constan)o(t)h(instead)g(of)f(a)g (term,)257 672 y(b)q(ecause)j(w)o(e)f(do)f(not)h(need)g(the)g(explicit) f(de\014nition)g(of)g(this)g(function)g(in)g(the)h(pro)q(of,)257 722 y(w)o(e)e(only)g(mak)o(e)e(use)j(of)e(the)h(prop)q(erties)i(giv)o (en)d(in)h(\(1\).)307 780 y(W)m(e)f(ha)o(v)o(e)g(already)g(men)o (tioned)f(that)i(the)g(in)o(v)n(arian)o(ts)e(\(2\){\(6\))h(w)o(ould)f (b)q(ecome)h(un-)257 830 y(readable,)19 b(if)e(w)o(e)i(use)g(this)f (term.)30 b(Program)16 b(extraction)j(can)f(solv)o(e)g(this)g(dilemma) 257 880 y(b)o(y)f(pro)o(viding)e(a)h(w)o(a)o(y)g(to)h(separate)h(the)f (sp)q(eci\014cation)g(for)g(the)g(algorithm)d(\(i.e.)i(the)257 929 y(in)o(v)n(arian)o(ts)d(\(2\){\(6\)\))h(from)e(the)i(algorithm)e (itself:)17 b(W)m(e)d(pro)o(v)o(e)g(the)g(goal)f(form)o(ula)257 1021 y Fa(all)22 b(n.)f(n)g(ex)h(cp,nxt,d.)584 1071 y(count)f(cp)g(=)h(n+1)f(&)584 1120 y(d)h(0)f(=)h(zero_natinf)e(&) 584 1170 y(\(all)h(a.)h(cp)f(\(nxt)g(a\))g(&)759 1220 y(d)g(a)h(=)f(d)h(\(nxt)f(a\))g(+)h(w)f(a)h(\(nxt)f(a\)\))g(&)584 1270 y(all)g(a,b.)g(cp)h(b)f(->)h(d)f(a)h(<=)f(d)h(b)f(+)h(w)g(a)f(b)h (&)955 1320 y(\(a)g(d)g(a)h(<)g(d)f(b)h(->)f(cp)h(a\))257 1411 y Fr(Note)c(that)f(w)o(e)g(ha)o(v)o(e)f(left)h(out)g(in)o(v)n (arian)o(t)e(\(4\))i(to)g(mak)o(e)e(the)j(formal)c(pro)q(of)i(shorter.) 257 1461 y(An)o(yw)o(a)o(y)m(,)f(w)o(e)h(can)h(easily)e(pro)o(v)o(e)h (\(4\))g(from)e(\(5\),)i(if)f(w)o(e)i(assume)e Fo(w)q Fr(\()p Fo(a;)7 b(b)p Fr(\))14 b(=)i(0)f(i\013)h Fo(a)f Fr(=)257 1511 y(0)d(=)h Fo(b)h Fr(\(instead)h(of)f Fo(a)e Fr(=)h Fo(b)p Fr(\),)h(so)g(adding)g(\(4\))h(to)f(the)h(form)o(ula)d (ab)q(o)o(v)o(e)i(w)o(ould)f(giv)o(e)h(just)257 1560 y(a)g(sligh)o(t)f(generalization.)307 1618 y(The)18 b(\014rst)g(step)g (in)f(the)h(pro)q(of)f(is)g(an)g(induction)f(o)o(v)o(er)i Fa(n)p Fr(.)28 b(In)17 b(the)h(base)f(case,)i(w)o(e)257 1668 y(assume)14 b Fa(0)h(F\))f(&)h(all)f(a.)g (a)g(d1)h(a)f(<)h(d1)f(c)h(->)f(cp1)h(a)257 2283 y Fr(\(cf.)d(\(1\)\))14 b(and)f(then)i(de\014ne)g Fa(cp)p Fr(,)e Fa(nxt)g Fr(and)h Fa(d)f Fr(for)h Fa(n+1)f Fr(b)o(y)h(en)o (tering)257 2374 y Fa(\(ex-intro)20 b(\(pt)h("[a])g([if)h(a=c)f(then)g (true)g(else)g(cp1)g(a]"\)\))938 2510 y Fr(9)p eop %%Page: 10 10 10 9 bop 257 195 a Fa(\(ex-intro)20 b(\(pt)h("[a])g([if)h(d1)f(c)h(+)f (w)h(a)f(c)h(<)g(d1)f(a)780 245 y(then)g(c)h(else)f(nxt1)g(a]"\)\))257 295 y(\(ex-intro)f(\(pt)h("[a])g([if)h(d1)f(c)h(+)f(w)h(a)f(c)h(<)g(d1) f(a)780 345 y(then)g(d1)h(c)f(+)h(w)g(a)f(c)h(else)f(d1)g(a]"\)\))307 432 y Fr(T)m(o)12 b(illustrate)h(the)h(b)q(ene\014ts)g(w)o(e)f(gain)f (from)g(en)o(tering)h(the)h(algorithm)c(using)i(terms)257 481 y(of)18 b(our)g(language)g(and)g(the)h(use)g(of)f(term)f(rewrite)j (systems,)f(w)o(e)f(sho)o(w)h(the)g(formal)257 531 y(pro)q(of)14 b(of)f(the)i(left)e(side)i(of)e(in)o(v)n(arian)o(t)f(\(5\):)18 b(W)m(e)c(ha)o(v)o(e)f(to)h(sho)o(w)257 618 y Fa([if)22 b([if)f(\(d1)g(c\)+\(w)g(a)g(c\)<\(d1)g(a\))g(then)g(c)h(else)f(nxt1)g (a]=c)345 668 y(then)g(true)345 718 y(else)g(cp1\([if)f(\(d1)h(c\)+\(w) g(a)g(c\)<\(d1)g(a\))g(then)g(c)h(else)f(nxt1)g(a]\)])257 805 y Fr(Lo)q(oking)9 b(at)h(the)g(term,)g(it)f(seems)h(ob)o(vious)f (to)h(do)g(this)f(b)o(y)h(the)g(follo)o(wing)e(case)i(analysis:)257 892 y Fa(\(cases)21 b(\(pt)g("\(d1)g(c\)+\(w)g(a)g(c\)<\(d1)g(a\)"\)\)) 257 979 y Fr(No)o(w)14 b(w)o(e)g(ha)o(v)o(e)g(to)f(sho)o(w)257 1066 y Fa(\(d1)22 b(c\)+\(w)e(a)i(c\)<\(d1)e(a\))i(->)257 1116 y([if)g([if)f(true)g(then)g(c)g(else)g(nxt1)g(a]=c)345 1166 y(then)g(true)345 1216 y(else)g(cp1\([if)f(true)h(then)g(c)g(else) g(nxt1)g(a]\)])257 1303 y Fr(and)257 1390 y Fa(\(\(d1)g(c\)+\(w)g(a)h (c\)<\(d1)e(a\))i(->)f(F\))g(->)257 1440 y([if)h([if)f(false)f(then)h (c)h(else)f(nxt1)g(a]=c)345 1490 y(then)g(true)345 1540 y(else)g(cp1\([if)f(false)h(then)g(c)g(else)g(nxt1)g(a]\)])257 1627 y Fr(In)e(the)h(\014rst)g(case,)h(w)o(e)e(simply)e(normalize)g (the)j(terms)f(in)f(the)i(form)o(ula)d(and)h(ha)o(v)o(e)257 1676 y(to)g(sho)o(w)h Fa(\(d1)i(c\)+\(w)g(a)g(c\)<\(d1)g(a\))g(->)h(T)c Fr(,)f(where)j Fa(T)e Fr(stands)h(for)f(the)h(truth,)g(so)257 1726 y(this)c(case)g(is)g(trivial.)j(In)c(the)h(second)h(case,)f(w)o(e) g(need)g(the)g(corresp)q(onding)h(induction)257 1776 y(h)o(yp)q(othesis,)e(whic)o(h)g(is)g(referenced)i(b)o(y)e(the)h (assumption)d(v)n(ariable)h Fa(ih12)g Fr(:)257 1863 y Fa(ih12:all)21 b(a.cp1\(nxt1)e(a\))j(&)f(\(d1)g(a\)=\(d1\(nxt1)f (a\)\)+\(w)g(a\(nxt1)h(a\)\))257 1950 y Fr(W)m(e)14 b(instan)o(tiate)f (this)h(using)257 2037 y Fa(\(inst-with)20 b('ih12)h('a)g('left\))257 2125 y Fr(and)14 b(get)257 2212 y Fa(ih12i:cp1\(nxt1)19 b(a\))257 2299 y Fr(The)c(normalized)d(form)o(ula)f(w)o(e)j(ha)o(v)o(e) g(to)g(sho)o(w)g(is)257 2386 y Fa([if)22 b(\(nxt1)e(a\)=c)h(then)g (true)g(else)g(cp1\(nxt1)f(a\)])928 2510 y Fr(10)p eop %%Page: 11 11 11 10 bop 257 195 a Fr(W)m(e)14 b(simplify)d(this)j(form)o(ula)d(using) 257 286 y Fa(\(simp)21 b('ih12i\))257 378 y Fr(and)14 b(hence)h(get)257 469 y Fa([if)22 b(\(nxt1)e(a\)=c)h(then)g(true)g (else)g(true])257 560 y Fr(whic)o(h)14 b(normalizes)f(to)g Fa(T)p Fr(.)1639 585 y Ff(coun)o(t)257 643 y Fe(2.2.)21 b Fq(Counting)p Fr(.)d(In)13 b(the)h(formal)c(pro)q(of)j(w)o(e)g(also)f (need)i(some)e(elemen)o(tary)g(prop)q(erties)257 693 y(of)d(a)g(coun)o(ting)g(op)q(erator)h(#)p Fo(C)i Fr(assigning)c(to)i (ev)o(ery)g(set)g Fo(C)i Fr(the)e(n)o(um)o(b)q(er)f(of)f(its)i(elemen)o (ts.)257 743 y(Let)15 b(#)p Fo(C)f Fr(:=)d(#)501 749 y Fi(N)532 743 y Fo(C)s Fr(,)i(where)i(#)745 749 y Fi(j)762 743 y Fo(C)i Fr(is)c(the)i(n)o(um)o(b)q(er)e(of)g(elemen)o(ts)h(of)f Fo(C)k Fr(less)d(than)g Fo(j)r Fr(,)g(so)487 873 y(#)522 879 y Fk(0)541 873 y Fo(C)25 b Fr(:=)e(0)p Fo(;)89 b Fr(#)820 879 y Fi(j)r Fk(+1)880 873 y Fo(C)25 b Fr(:=)e(#)1037 879 y Fi(j)1054 873 y Fo(C)12 b Fr(+)1138 802 y Fc(\()1171 845 y Fr(1)41 b(if)13 b Fo(j)h Fp(2)e Fo(C)1171 905 y Fr(0)41 b(otherwise)257 999 y Fe(Lemma.)562 1091 y Fr(#)597 1097 y Fi(j)614 1091 y Fp(;)11 b Fr(=)h(0)p Fo(;)863 b Fr(\(7\))562 1153 y(#)597 1159 y Fi(j)614 1153 y Fo(C)14 b Fp(\024)e Fo(j;)855 b Fr(\(8\))562 1215 y Fo(j)14 b Fp(\024)e Fr(#)672 1221 y Fi(j)689 1215 y Fo(C)i Fp(!)d Fo(b)g(<)h(j)i Fp(!)d Fo(b)g Fp(2)h Fo(C)q(;)531 b Fr(\(9\))562 1277 y Fo(j)14 b Fp(\024)e Fo(b)f Fp(!)g Fr(#)754 1283 y Fi(j)771 1277 y Fr(\()p Fo(C)h Fp([)d(f)p Fo(b)p Fp(g)p Fr(\))i(=)h(#)1032 1283 y Fi(j)1049 1277 y Fo(C)q(;)473 b Fr(\(10\))562 1340 y Fo(b)11 b(<)h(j)i Fp(!)d Fo(b)16 b(=)-26 b Fp(2)12 b Fo(C)i Fp(!)d Fr(#)920 1346 y Fi(j)937 1340 y Fr(\()p Fo(C)h Fp([)d(f)p Fo(b)p Fp(g)p Fr(\))i(=)h(1)d(+)g(#) 1269 1346 y Fi(j)1286 1340 y Fo(C)q(;)236 b Fr(\(11\))562 1402 y Fp(8)p Fo(b)h(F\))f(&)h(all)f(a.)g(a)g(d1)h(a)f(<)h(d1)f(c)h(->)f(cp1)h(a)257 2030 y Fr(w)o(e)16 b(then)h(pro)o(v)o(e)f(the)g(goal)f(form)o(ula.)21 b(In)16 b(this)f(w)o(a)o(y)h(w)o(e)g(ha)o(v)o(e)f(pro)o(v)o(ed)h(our)g (algorithm)257 2079 y(correct.)307 2137 y(W)m(e)e(can)g(then)h(go)e(on) h(and)g(let)g(the)g(mac)o(hine)f(extract)i(an)f(implemen)o(tati)o(on)d (of)j(the)257 2187 y(algorithm)g(from)g(the)j(formal)d(pro)q(of.)25 b(Of)16 b(course,)h(the)g(result)g(will)e(b)q(e)i(the)g(same)e(as)257 2236 y(what)c(w)o(e)g(had)g(in)f(mind)f(and)h(quite)h(explicitely)f (put)h(in)o(to)f(the)i(existence-in)o(tro)q(duction)257 2286 y(steps)j(of)e(our)h(formal)d(pro)q(of.)17 b(Ho)o(w)o(ev)o(er,)d (the)g(program)d(extracted)k(from)d(the)i(pro)q(of)f(is)257 2336 y(executable)i(co)q(de,)e(and)g(it)g(is)g(reliable)f(since)i(the)g (correctness)i(of)d(the)g(formal)e(pro)q(of)i(it)257 2386 y(is)h(extracted)i(from)c(can)i(b)q(e)g(mac)o(hine-c)o(hec)o(k)o (ed.)928 2510 y(13)p eop %%Page: 14 14 14 13 bop 257 195 a Fl(References)257 294 y Fr([1])20 b(Joseph)f(L.)e(Bates)i(and)f(Rob)q(ert)g(L.)f(Constable.)30 b(Pro)q(ofs)18 b(as)g(programs.)29 b Fq(A)o(CM)322 344 y(T)m(r)n(ansactions)c(on)g(Pr)n(o)n(gr)n(amming)g(L)n(anguages)h(and)f (Systems)p Fr(,)g(7\(1\):113{136,)322 394 y(Jan)o(uary)14 b(1985.)257 477 y([2])20 b(Ulric)o(h)11 b(Berger)h(and)f(Helm)o(ut)e (Sc)o(h)o(wic)o(h)o(ten)o(b)q(erg.)14 b(Program)c(extraction)h(from)e (clas-)322 527 y(sical)k(pro)q(ofs.)18 b(In)c(D.)f(Leiv)n(an)o(t,)f (editor,)i Fq(L)n(o)n(gic)g(and)i(Computational)f(Complexity,)322 577 y(International)g(Workshop)h(LCC)f('94,)g(Indianap)n(olis,)h(IN,)e (USA,)h(Octob)n(er)g(1994)p Fr(,)322 626 y(v)o(olume)c(960)h(of)g Fq(L)n(e)n(ctur)n(e)i(Notes)g(in)g(Computer)f(Scienc)n(e)p Fr(,)g(pages)h(77{97.)d(Springer)322 676 y(V)m(erlag,)i(Berlin,)g (Heidelb)q(erg,)i(New)f(Y)m(ork,)f(1995.)257 759 y([3])20 b(Ulric)o(h)11 b(Berger)i(and)f(Helm)o(ut)e(Sc)o(h)o(wic)o(h)o(ten)o(b) q(erg.)16 b(The)c(greatest)h(common)8 b(divisor:)322 809 y(a)15 b(case)h(study)g(for)f(program)f(extraction)i(from)d (classical)i(pro)q(ofs.)22 b(In)16 b(S.)f(Berardi)322 859 y(and)20 b(M.)g(Copp)q(o,)f(editors,)i Fq(T)m(yp)n(es)f(for)h(Pr)n (o)n(ofs)f(and)h(Pr)n(o)n(gr)n(ams.)f(International)322 909 y(Workshop)13 b(TYPES)g('95,)g(T)m(orino,)e(Italy,)h(June)h(1995.)h (Sele)n(cte)n(d)e(Pap)n(ers)p Fr(,)f(v)o(olume)322 959 y(1158)f(of)g Fq(L)n(e)n(ctur)n(e)i(Notes)g(in)g(Computer)g(Scienc)n(e) p Fr(,)f(pages)h(36{46.)d(Springer)i(V)m(erlag,)322 1008 y(Berlin,)j(Heidelb)q(erg,)g(New)g(Y)m(ork,)f(1996.)257 1091 y([4])20 b(Christopher)15 b(Alan)f(Goad.)k Fq(Computational)e (uses)f(of)h(the)f(manipulation)h(of)f(for-)322 1141 y(mal)g(pr)n(o)n(ofs)p Fr(.)k(PhD)c(thesis,)g(Stanford)f(Univ)o(ersit)o (y)m(,)f(August)i(1980.)k(Stanford)14 b(De-)322 1191 y(partmen)o(t)f(of)g(Computer)h(Science)h(Rep)q(ort)f(No.)f(ST)m (AN{CS{80{819.)257 1274 y([5])20 b(Helm)o(ut)g(Sc)o(h)o(wic)o(h)o(ten)o (b)q(erg.)41 b(Programmen)o(t)o(wic)o(klung)18 b(durc)o(h)k(Bew)o (eistransfor-)322 1324 y(mation:)15 b(Das)i(Maximalsegmen)o(tproblem)o (.)26 b Fq(Sitzungsb)n(er.)18 b(d.)h(Bayer.)f(A)o(kad.)g(d.)322 1374 y(Wiss.,)c(Math.-Nat.)h(Kl.)p Fr(,)d(pages)j(8*{12*,)d(1997.)928 2510 y(14)p eop %%Trailer end userdict /end-hook known{end-hook}if %%EOF