%!PS-Adobe-2.0 %%Creator: dvipsk 5.58f Copyright 1986, 1994 Radical Eye Software %%Title: rpe5.dvi %%Pages: 23 %%PageOrder: Ascend %%BoundingBox: 0 0 596 842 %%EndComments %DVIPSCommandLine: dvips rpe5.dvi %DVIPSParameters: dpi=300, compressed, comments removed %DVIPSSource: TeX output 2001.03.24:1804 %%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 (rpe5.dvi) @start /Fa 1 79 df<3AFFE001FF8013F03A3818003800D80C0C1318A2EA0E06EA0F03 380D8180A2380CC0C0EB6060EB303013181418EB0C0CEB06061303140390380181989038 00C0D814601578EC3038EC1818140CA214061403EC0198EC00D8A2000E1478D87FE01338 1518C8120821237EA123>78 D E /Fb 37 121 df<13E01201EA0380EA0700120E5AA25A A25AA35AA91270A37EA27EA27E7EEA0380EA01E012000B217A9C16>40 D<12C07E12707E7E7EA27EA2EA0380A3EA01C0A9EA0380A3EA0700A2120EA25A5A5A5A5A 0A217B9C16>II<13E0A8B512E0A33800E000A813137F9516>I45 D48 D<12035AA25A5AB4FCA212E71207AEEAFFF8A30D197B9816>III<137C13FC13DC1201EA039CA2EA071C120F120E121E123C1238127812 F0B512E0A338001C00A53801FFC0A313197F9816>II<13F8EA03FC487EEA0F07EA1C0F1238EA78060070C7FCA2EAE3F8EAEFFCB4 7EEAF80F487EEB038012E0A21270A2130700381300EA3C1EEA1FFC6C5AEA03E011197E98 16>I60 DI<1203EA0F80EA3FE0EAFDF8EAF078EA40100D067C9816>94 D97 D<12FCA3121CA4137CEA1DFEEA1FFFEB0780381E03C0 EA1C01EB00E0A6EB01C0EA1E03381F0780EBFF00EA1DFEEA0C7813197F9816>II<133FA31307A4EA03C7EA0FF748B4FCEA3C1F487EEA700712E0A6EA700F12 786C5A381FFFE0EA0FF7EA07C713197F9816>I I<131E137F3801FF8013C7380383001380A2EA7FFFB5FCA2EA0380ACEA7FFC487E6C5A11 197F9816>I<12FCA3121CA41378EA1DFCEA1FFE130FEA1E07121CAA38FF8FE0139F138F 13197F9816>104 D<1203EA0780A2EA0300C7FCA4EAFF80A31203ACEAFFFC13FE13FC0F 1A7C9916>I<127E12FE127E120EA4EB7FE0A3EB0F00131E5B5B5B120F7F13BC131EEA0E 0E7F1480387F87F0EAFFCFEA7F871419809816>107 DI<38F9C38038FFEFC0EBFFE0EA3C78A2EA3870AA38FE7CF8 A31512809116>III I<3803E380EA0FF3EA1FFBEA3E0FEA78071270EAE003A6EA70071278EA3C1FEA1FFBEA0F F3EA03E3EA0003A6EB1FF0EB3FF8EB1FF0151B7F9116>I<387F0FC038FF3FE0EA7F7F38 07F040EBC0005BA290C7FCA8EA7FFC12FF127F13127F9116>II<12035AA4EA7FFFB5FCA20007C7FCA75BEB0380A3EB8700EA03FE6C 5A6C5A11177F9616>II< 387F1FC038FF9FE0387F1FC0381C0700A2EA0E0EA36C5AA4EA03B8A3EA01F0A26C5A1312 7F9116>I<38FF1FE0A338380380A4EA39F3A20019130013B3A3EA1DB71317EA1F1FEA0F 1EEA0E0E13127F9116>I<387F1FC0133F131F380F1E006C5AEA03B813F012016C5A1201 7FEA03B8EA073C131CEA0E0E387F1FC038FF3FE0387F1FC013127F9116>I E /Fc 33 121 df12 D<1238127C12FEA3127C12380707 7C8610>46 D<13181378EA01F812FFA21201B3A7387FFFE0A213207C9F1C>49 DI<13FE3807FFC0380F07E0381E03F0123FEB81F8A3EA1F 0314F0120014E0EB07C0EB1F803801FE007F380007C0EB01F014F8EB00FCA2003C13FE12 7EB4FCA314FCEA7E01007813F8381E07F0380FFFC03801FE0017207E9F1C>I54 D69 DI72 DI77 DI<007FB61280A2397E03F80F 00781407007014030060140100E015C0A200C01400A400001500B3A248B512F0A222227E A127>84 D87 D97 DIII<13FE3807FF80380F87C0381E01E0003E13F0EA7C0014F812FCA2B5FCA200FC C7FCA3127CA2127E003E13186C1330380FC0703803FFC0C6130015167E951A>II<3801FE0F3907FFBF80380F87C7381F03E7391E01E000003E7FA5001E5BEA1F03 380F87C0EBFF80D809FEC7FC0018C8FCA2121C381FFFE06C13F86C13FE001F7F383C003F 48EB0F80481307A40078EB0F006C131E001F137C6CB45A000113C019217F951C>I<121C 123E127FA3123E121CC7FCA7B4FCA2121FB2EAFFE0A20B247EA310>105 D108 D<3AFF07F007F090391FFC1FFC3A1F30 3E303E01401340496C487EA201001300AE3BFFE0FFE0FFE0A22B167E9530>I<38FF07E0 EB1FF8381F307CEB403CEB803EA21300AE39FFE1FFC0A21A167E951F>I<13FE3807FFC0 380F83E0381E00F0003E13F848137CA300FC137EA7007C137CA26C13F8381F01F0380F83 E03807FFC03800FE0017167E951C>I<38FF0FE0EB3FF8381FE07CEB803E497E1580A2EC 0FC0A8EC1F80A29038803F00EBC03EEBE0FCEB3FF8EB0FC090C8FCA8EAFFE0A21A207E95 1F>I 114 DI<487E A41203A21207A2120F123FB5FCA2EA0F80ABEB8180A5EB8300EA07C3EA03FEEA00F81120 7F9F16>I<38FF01FEA2381F003EAF147E14FE380F81BE3907FF3FC0EA01FC1A167E951F> I<3AFFE3FF07F8A23A1F007800C09038807C01000F1580A23A07C07E030014DE5D3903E1 DF06148FD801F1138CEBF307A2D800FF13D8EBFE0315F890387C01F0A2013C5BEB3800A2 25167F9528>119 D<39FFE07FC0A2390F801C006C6C5A6C6C5AEBF0606C6C5A3800F980 137F6DC7FC7F80497E1337EB63E0EBC1F03801C0F848487E3807007E000E133E39FF80FF E0A21B167F951E>I E /Fd 8 87 df<132013401380EA01005A1206A25AA25AA2123812 30A21270A3126012E0AD12601270A31230A212381218A27EA27EA27E7EEA008013401320 0B317A8113>0 D<7E12407E7E12187EA27EA27EA213801201A213C0A3120013E0AD13C0 1201A31380A212031300A21206A25AA25A12105A5A5A0B317F8113>I<141C143C14F8EB 01E0EB03C0EB0780EB0F00130E131E5BA35BB3B3A25BA3485AA2485A5B48C7FC120E5A12 7812E0A21278121C7E7E6C7E7F6C7EA26C7EA31378B3B3A27FA37F130E130FEB0780EB03 C0EB01E0EB00F8143C141C167C7B8121>40 D<1318137813F0EA01E0EA03C0EA0780EA0F 005A121E123E123C127CA2127812F8B3A50D25707E25>56 D<12F8B3A51278127CA2123C 123E121E121F7EEA0780EA03C0EA01E0EA00F0137813180D25708025>58 D<137CB3A613F8A313F0120113E0120313C0EA07801300120E5A5A12F012C012F012387E 7E7E1380EA03C013E0120113F0120013F8A3137CB3A60E4D798025>60 D<12F8AE050E708025>62 D<1303801307A2497EA3EB1CE0A3EB3870A3497EA3497EA348 487EA348487EA33907000380A2000EEB01C0A348EB00E0A3481470A3481438A348141CA2 48140C1E2A7E7F23>86 D E /Fe 33 122 df<127812FCA4127806067D850D>46 D<1360EA01E0120F12FF12F31203B3A2387FFF80A2111B7D9A18>49 DI< EA07F8EA1FFEEA3C1FEB0F80387C07C0127E127C123838000F80A2EB1E005BEA03F8EA00 1EEB0F80EB07C0A214E01230127812FCA214C038780F80EB1F00EA1FFEEA07F8131B7E9A 18>II<38380180383FFF005B5B5B13C0 0030C7FCA4EA31F8EA361E38380F80EA3007000013C014E0A3127812F8A214C012F03860 0F8038381F00EA1FFEEA07F0131B7E9A18>I<137EEA03FF38078180380F03C0EA1E0712 3C387C03800078C7FCA212F813F8EAFB0E38FA0780EAFC0314C000F813E0A41278A214C0 123CEB0780381E0F00EA07FEEA03F8131B7E9A18>I65 D<90381FE0209038FFF8E03803F80F3807 C003380F800148C7FC123E1560127E127C00FC1400A8007C1460127E123E15C07E390F80 01803907C003003803F80E3800FFFCEB1FE01B1C7D9B22>67 D69 D76 D82 D<007FB512E0A238781F81007013800060146000E0147000C01430A400001400B03807FF FEA21C1C7E9B21>84 D97 D99 DII<137F3801E3803803C7 C0EA0787120FEB8380EB8000A5EAFFF8A2EA0F80AEEA7FF0A2121D809C0F>I<3803F0F0 380E1F38EA3C0F3838073000781380A400381300EA3C0FEA1E1CEA33F00030C7FCA3EA3F FF14C06C13E014F0387801F838F00078A300701370007813F0381E03C03807FF00151B7F 9118>I I<121E123FA4121EC7FCA6127FA2121FAEEAFFC0A20A1E7F9D0E>I107 DI<39FF0FC07E903831E18F 3A1F40F20780D980FC13C0A2EB00F8AB3AFFE7FF3FF8A225127F9128>I<38FF0FC0EB31 E0381F40F0EB80F8A21300AB38FFE7FFA218127F911B>II<38FF3F80EBE1E0381F80F0EB0078147C143C143EA6143C147C1478EB80F0EB C1E0EB3F0090C7FCA6EAFFE0A2171A7F911B>I114 DI<1203A45A A25AA2EA3FFC12FFEA1F00A9130CA4EA0F08EA0798EA03F00E1A7F9913>I<39FF8FF8FE A2391F03E030A3390F87F06013869038C6F8E03907CC78C0A23903FC7D80EBF83D143F39 01F01F00A20000131EEBE00EA21F127F9122>119 D<38FFC7FCA2381F81C0380F838038 07C700EA03EEEA01FC5B1200137C13FEEA01DF38039F80EA070F380607C0380C03E038FF 07FCA216127F9119>I<38FFC1FCA2381F00601380000F13C0A23807C180A23803E300A2 13F7EA01F613FE6C5AA21378A21330A25B1270EAF8E05BEAF9800073C7FC123E161A7F91 19>I E /Ff 2 71 df26 D70 D E /Fg 1 79 df<39FFE00FF83930100320390808014090380400C0120C EA0E02EA0D01380C8080EB4040A2EB2020EB1010EB0808EB0404A2EB0202EB0101EB0080 EC40401420A2141014081404140200121301123339FFC000C0C812401D1D809B20>78 D E /Fh 1 50 df<1218127812981218AC12FF08107D8F0F>49 D E /Fi 13 118 df80 D<121FEA7FC01261EA40E012001207123F127812E0A212F1127F123E0B0D7F 8C0F>97 D<120FEA3F80EA71C0EA70E0EAE060EAFFE0A2EAE000A21270EA7860EA3FE0EA 0F800B0D7F8C0E>101 DII<12E0A31200A512E0AD03157E9408>105 D<12E0B3A203147E9308>108 D110 D<120FEA3FC0EA70E0A2EAE070A5EA70E01279EA3FC0EA0F000C0D7F8C0F>I<12E712EF 12F812F0A212E0A8080D7E8C0B>114 D<123EEA7F8012E1EAE000A212FE127FEA1F8012 03128312C3EAFF00123E090D7F8C0C>I<1270A412FFA21270A81271127F123C08117F90 0B>II E /Fj 29 122 df<133C13C2EA01031202 12041302EA080613FCA21304EA1006A4EA200CA2EA30181310EA4860EA47C0EA4000A25A A4101A7F9313>12 D17 D<1218A31230A412601261A212C212C41278080D7F8C0C>19 DI<121C120612077EA2EA0180A213C01200A213E01201EA0370EA0630120CEA18181230 EA601CEAC00CEA800E0F147E9314>I23 D26 D28 D<124012E0124003037D820A>58 D<124012E012601220A31240A2128003097D820A>I<14C01303EB0700131C1378EA01E0 EA0780000EC7FC123812F0A21238120E6C7EEA01E0EA0078131C1307EB03C0130012147D 901A>I<5B5B5B1480130B131B13131323A21343138314C0EA0101EA03FFEA0201120412 0C1208001813E038FE07F815147F9319>65 D<3807FFE03800E0383801C018141CA33803 8038147014E0EBFFC0380700E0147014301438000E1370A214E0A2381C038038FFFE0016 147F9319>II<3807FFE03800E0703801C018140C A2140EEA0380A43807001CA31438000E1330147014E0EB01C0381C0700EAFFFC17147F93 1B>I<3807FFFC3800E01C3801C00CA31408EA03811400138313FFEA0702A390C7FC120E A45AEAFFC016147F9315>70 DI<3907FC 3F803900E01C00EBF010EB70205C6D5A0139C7FC133E131C131EA2133F136713C7380183 80EA030300067FEA0401001C7F38FE07F819147F931B>88 D<1318136C137C136C13C0A3 EA07F8EA00C0EA0180A5EA0300A512021206A2126612E45A12700E1A7F9310>102 D<1206120712061200A41238124CA2128C12981218A212301232A21264A2123808147F93 0C>105 D<1330133813301300A4EA01C0EA0260EA0430136012081200A213C0A4EA0180 A4EA630012E312C612780D1A81930E>I<121E12065AA45A1338135C139CEA3118EA3600 1238EA3F80EA61C0EA60C8A3EAC0D013600E147F9312>I<123C120C1218A41230A41260 A412C012C8A312D0126006147F930A>I<3830F87C38590C86384E0D06EA9C0EEA980C12 18A248485A15801418A23960301900140E190D7F8C1D>II112 D<1204120CA35AEAFF80EA1800A25AA45A1261A212621264123809127F910D>116 D120 DI E /Fk 20 122 df<131C133EA2132E1367A2EB E78013C713C300017F1383138100037F1301486C7EA21206000E1378380FFFF8A2381C00 3CA2121800387FA248131F80126000E0EB0780191D7F9C1C>65 D70 D<12F0B3AB041D7C9C0C>73 D80 D97 D<1307ABEA07C7EA1FF7EA3FFF EA3C1FEA7807127012E0A61270EA780FEA3C1FEA3FFFEA1FF7EA07C7101D7F9C15>100 DI<13FC12011203EA0700120EA7EAFFE0A2EA0E00B00E1D 809C0D>I<3807C3C0EA0FFF5A38383800487EA56C5AEA3FF05BEA77C00070C7FCA2EA3F FC13FF481380EA700738E001C0A3EAF003387C0F80383FFF006C5AEA07F8121B7F9115> I<12E0B3AB031D7D9C0A>108 D<38E3F03F39EFF8FF80D8FFFD13C039F81F81E038F00F 00EAE00EAD1B127D9122>II< EA03F0EA0FFC487EEA3C0F38780780EA700338E001C0A5EAF00300701380EA7807383C0F 00EA1FFE6C5AEA03F012127F9115>I113 DII<121CA6EAFFE0A2EA1C00AC1320EA1FF0120FEA07C00C187F970F>II<3870038038780700EA3C0EEA1C1C120E6C5AEA03 F06C5A5B7F487EEA0738EA0618EA0E1C487E487E3870038000F013C01212809113>120 DI E /Fl 9 83 df0 D<1204A3EAC460EAF5E0EA3F80EA0E00EA3F80EAF5E0EAC460EA0400A30B0D7E8D 11>3 D<14101418A280A28080B612E0A2C7EA030014065CA25CA214101B107E8E21>33 D<1204120EA2121CA31238A212301270A21260A212C0A2070F7F8F0A>48 D<1303A21306A2130C1318A21330A2136013C0A2EA0180A2EA0300A212065AA25AA25A5A A25A1240101A7C9300>54 D<0040134000C013C038600180A238300300A2EA3FFF6C5AEA 18066C5AA26C5AA26C5AA3EA01E0A26C5AA21214809314>56 D<134013C0B1B512E0A213 147D931A>63 D<146014E0A213011303A213061304130C1318A21330136014F013FF5A38 038070EA830000CE137800FC137E14380030130017167F941B>65 D<3803FFF0000F7F3830E07C3860C03C00C0131C0081131812015C1420EB80C0018FC7FC EA039E130F80EA0707380603C0ECE080390C01F100EB00FE48137819147F931D>82 D E /Fm 27 119 df<120212041208121812101230122012601240A212C0AA1240A21260 1220123012101218120812041202071E7D950D>40 D<1280124012201230121012181208 120C1204A21206AA1204A2120C1208121812101230122012401280071E7E950D>I<1360 AAB512F0A238006000AA14167E9119>43 D<120FEA30C0EA6060A2EA4020EAC030A9EA40 20EA6060A2EA30C0EA0F000C137E9211>48 D<120C121C12EC120CAFEAFFC00A137D9211 >I<121FEA60C01360EAF07013301260EA0070A2136013C012011380EA02005AEA081012 10EA2020EA7FE012FF0C137E9211>II<136013E0A2EA 016012021206120C120812101220126012C0EAFFFCEA0060A5EA03FC0E137F9211>II<124012E012401200A7124012E01240030D7D8C09>58 D61 D<12FCA212C0B3A712FCA2061D7E9509> 91 D<12FCA2120CB3A712FCA2061D809509>93 D<127FEAE1C0EAE040EA40601200EA07 E0EA3860126012C01364A2EA61E4EA3E380E0D7E8C11>97 D<12F01230A6EA33E0EA3430 EA3808EA300C1306A5130CEA3808EA3430EA23E00F147F9312>II<13781318A6EA0F98EA1878EA 2038EA601812C0A51260EA2038EA1858EA0F9E0F147F9312>II103 D<1220127012201200A512F01230AB12FC06157F9409>105 D110 DII114 DI<1210A312301270EAFF80EA3000A71380A3EA110012 0E09127F910D>I118 D E /Fn 39 122 df<13FCEA0782EA0E07121C130290C7FCA4B5FCEA1C 07AC387F1FC01217809614>12 D<9038FC7F80380703C3380E0783001C1303A6B6FC381C 0703AC397F1FCFE01B1780961D>15 D<126012F0A212701210A21220A21240A2040A7D83 0A>44 DI<126012F0A2126004047D830A>I48 D<1206120E12FE120EB1EAFFE00B157D9412>II<126012F0A212601200A6126012F0A21260040E7D8D0A>58 D73 D76 D<00FEEB03F8001E14C000171305A338138009A23811C0 11A33810E021A2EB7041A3EB3881A2EB1D01A2130EA2123839FE040FF81D177F9620>I< 00FC13FE001E1338001F13101217EA1380EA11C0A2EA10E013701338A2131C130E130F13 07EB0390EB01D0A2EB00F014701430123800FE131017177F961A>I<13FCEA0303380E01 C0381C00E048137000301330007013380060131800E0131CA700701338A2003013300038 13706C13E0380E01C038030300EA00FC16177E961B>I<387FFFF83860381800401308A2 00801304A300001300AF3803FF8016177F9619>84 D97 D<12F81238A8EA39F0EA3E0CEA380613077F1480A414005B1306EA361CEA21F011177F96 14>II<133E130EA8EA07CEEA1C3EEA300E1270126012E0A412601270EA301EEA182E38 07CF8011177F9614>IIII<12F812 38A813F8EA3B1CEA3C0E1238AA38FE3F8011177F9614>I<12301278A212301200A512F8 1238AC12FE07177F960A>I<12F81238A8133E13381330134013801239EA3FC0EA39E012 3813F01378133CA2EAFE7F10177F9613>107 D<12F81238B3A312FE07177F960A>I<38F8 F83E383B1CC7393C0F0380EA380EAA39FE3F8FE01B0E7F8D1E>IIIIIII<1208A31218A21238EAFFC0EA3800A713 40A4EA1C80EA0F000A147F930E>I II<38FEFE7C383838381410133C001C1320134C381E4E60380ECE4013870007138013 03A200031300EA0201160E7F8D19>III E /Fo 1 4 df<120CA2EACCC012EDEA7F80EA0C00EA7F80EAEDC012CCEA0C00A2 0A0B7D8B10>3 D E /Fp 38 128 df45 D66 D<90380FE02090387018603801C00439 030003E000061301000E13004814605A15201278127000F01400A80070142012781238A2 6C14407E000614806CEB01003801C00638007018EB0FE01B1E7D9C21>II70 D<90381FC04090387030C03801C00C 38030003000E1301120C001C13005A15401278127000F01400A6EC7FF8EC07C000701303 12781238A27E120C120E000313053801C008390070304090381FC0001D1E7D9C23>I<39 FFF0FFF0390F000F00AC90B5FCEB000FAD39FFF0FFF01C1C7D9B22>I<3803FFC038003E 00131EB3127012F8A2131CEA703CEA4038EA3070EA0FC0121D7E9B18>74 D<39FFF00FF0390F0003C0150014025C5C5C1460148049C7FC13021307497E1317EB23C0 EB43E01381EB00F08014788080141F80EC078015C015E039FFF01FF81D1C7D9B23>I77 D80 D<3803F040380C0CC0EA1002EA3001EA600012E01440A36C13007E127EEA7FE0EA 3FFC6CB4FC00071380EA007FEB07C0EB03E0130113007EA36C13C0A238E0018038D00300 EACE06EA81F8131E7D9C19>83 D<39FFE003FC001FC712F06C146015406D13C000071480 A23903C00100A23801E002A213F000005BA2EB7808A2137CEB3C10A26D5AA2131F6D5AA2 6D5AA36DC7FCA21E1D7E9B22>86 D<3BFFE0FFE03FC03B1F001F000F00001E011E13066C 6D1304A3D807806D5AA201C013C0000301135BA29038E033E0000101215BA29039F061F0 60000001401340A29039F88078C001785CA290263D003DC7FCA36D7FA3010C130CA32A1D 7E9B2E>I<13201370A313B8A3EA011CA2EA031EEA020EA2487EEA07FFEA040738080380 A2001813C01301123838FC07F815157F9419>97 DIIII< B51280EA1C031300A21440A213081400A21318EA1FF8EA1C181308A390C7FCA5EAFFC012 157F9416>II<38FF8FF8381C01C0 A9EA1FFFEA1C01A938FF8FF815157F9419>II<38 FF81F8381C01E01480140013025B5B5B1330137013B8EA1D1C121EEA1C0E7F14801303EB 01C014E014F038FF83FC16157F941A>107 DI<00FEEB0FE0001E140000171317A338138027A23811C047A33810E0 87A2EB7107A3133AA2131CA2123839FE083FE01B157F941F>I<38FC03F8381E00E01440 1217EA138013C01211EA10E01370A21338131CA2130E130714C0130313011300123800FE 134015157F9419>II113 DII<387FFFF03860703000401310A200801308A300001300ADEA07FF15157F9419>I<38 FF83F8381C00E01440AE000C13C0000E138038060100EA0386EA00FC15157F9419>I<38 FF01F8383C0070001C13601440A26C1380A238070100A3EA0382A2EA01C4A3EA00E8A213 70A3132015157F9419>I<39FF07F87E393C01E03C0038EBC018391C02E010A3390E0470 20A33907083840A33903901C80A33901E00F00A33800C006A31F157F9423>I<38FF80FE 381E0038000E1320000F13606C13403803808013C03801C10013E212001374137C1338A8 48B4FC1715809419>121 DI127 D E /Fq 61 123 df<14FE90380301801306EB0C03EB1C0191C7FC13181338 A43803FFFE3800700EA35CA213E0A25CA3EA01C01472A438038034141891C7FC90C8FCA2 5A12C612E65A12781925819C17>12 D<1218123CA31204A21208A2121012201240128006 0C779C0D>39 D<13031306130813181330136013C0A2EA0180EA0300A21206A25AA2121C 1218A212381230A21270A21260A412E0A51260A51220123012107EA2102A7B9E11>I<13 10A21308130C13041306A51307A51306A4130EA2130CA2131C1318A213381330A21360A2 13C0A2EA0180EA0300A212065A5A121012605A102A809E11>I<12181238127812381208 A21210A212201240A21280050C7D830D>44 DI<1230127812F0 126005047C830D>I<1304130C131813381378EA07B8EA0070A413E0A4EA01C0A4EA0380 A4EA0700A45AEAFFF00E1C7B9B15>49 D<133EEB4180EB80C0EA0100000213E0EA0440A2 1208A3381081C0A238110380000E1300EA00065B5B136013800003C7FC12044813404813 805AEB0100EA7F07EA43FEEA81FCEA8078131D7D9B15>I<131FEB60C013803801006012 021340000413E0A3EB81C0EA030138000380EB070013FC131C1306A21307A41270EAE00E 12805BEA40185BEA20E0EA1F80131D7D9B15>II<3809C040380FE080EA1FE1381C6100EA30 26EA201AEA6004EA400CEA80081318485AA25BA25BA212015B120390C7FC5AA3120EA35A A21218121D799B15>55 D<133E13E138018180380300C01206120E120C121CA213011238 A31303001813801307EA080B380C3300EA03C7EA0007130E130C131C1318EAE0305BEA80 C0EAC180003EC7FC121D7C9B15>57 D<1206120FA212061200AA1230127812F012600812 7C910D>I<1203EA0780A2EA0300C7FCAA12181238127812381208A25AA25A5AA25A091A 7D910D>I<1418A21438A21478A214B8EB0138A2EB023C141C1304130C13081310A21320 A2EB7FFCEBC01C1380EA0100141E0002130EA25A120C001C131EB4EBFFC01A1D7E9C1F> 65 D<48B5FC39003C038090383801C0EC00E0A35B1401A2EC03C001E01380EC0F00141E EBFFFC3801C00E801580A2EA0380A43907000F00140E141E5C000E13F0B512C01B1C7E9B 1D>I<903803F02090381E0C6090383002E09038E003C03801C001EA038048C7FC000E14 80121E121C123C15005AA35AA41404A35C12705C6C5B00185B6C485AD80706C7FCEA01F8 1B1E7A9C1E>I<48B5FC39003C03C090383800E0A21570A24913781538A215785BA44848 13F0A315E03803800115C0140315803907000700140E5C5C000E13E0B512801D1C7E9B1F >I<48B512F038003C00013813301520A35BA214081500495AA21430EBFFF03801C020A4 39038040801400A2EC0100EA07005C14021406000E133CB512FC1C1C7E9B1C>I<48B512 F038003C00013813301520A35BA214081500495AA21430EBFFF03801C020A448485A91C7 FCA348C8FCA45AEAFFF01C1C7E9B1B>I<903803F02090381E0C6090383002E09038E003 C03801C001EA038048C7FC000E1480121E121C123C15005AA35AA2903801FF809038001E 00141CA400705BA27E001813786C139038070710D801F8C7FC1B1E7A9C20>I<3A01FFC3 FF803A003C00780001381370A4495BA449485AA390B5FC3901C00380A4484848C7FCA438 07000EA448131E39FFE1FFC0211C7E9B1F>III<3A01 FFC07F803A003C001E000138131815205D5DD97002C7FC5C5C5CEBE04014C013E1EBE2E0 EA01C4EBD07013E013C048487EA21418141CEA070080A348130F39FFE07FC0211C7E9B20 >I<3801FFC038003C001338A45BA45BA4485AA438038002A31404EA0700140C14181438 000E13F0B5FC171C7E9B1A>III< EB07F0EB1C1CEB700E497E3901C00380EA0380EA0700000E14C0121E121C123CA25AA348 EB0780A3EC0F00A2140E141E5C007013385C00785B383801C06C485AD80E0EC7FCEA03F8 1A1E7A9C20>I<3801FFFE39003C038090383801C0EC00E0A3EB7001A315C0EBE0031580 EC0700141C3801FFF001C0C7FCA3485AA448C8FCA45AEAFFE01B1C7E9B1C>I<3801FFFE 39003C078090383801C015E01400A2EB7001A3EC03C001E01380EC0700141CEBFFE03801 C03080141CA2EA0380A43807003C1520A348144039FFE01E80C7EA0F001B1D7E9B1E>82 DI<001FB512C0381C070138300E0000201480126012405B1280A2000014005B A45BA45BA4485AA41203EA7FFE1A1C799B1E>I<397FF03FE0390F000700000E13061404 A3485BA4485BA4485BA4485BA35CA249C7FCEA60025B6C5AEA1830EA07C01B1D789B1F> I<3AFF83FF07F03A3C007001C00038158002F01300A290380170025D13025D13045D1308 5D131001305B1320D81C405BA2D98071C7FCA2381D0072A2001E1374A2001C1338A20018 133014201210241D779B29>87 D97 D<123F1207A2120EA45AA4EA39E0EA3A 18EA3C0C12381270130EA3EAE01CA31318133813301360EA60C0EA3180EA1E000F1D7C9C 13>I<13F8EA0304120EEA1C0EEA181CEA30001270A25AA51304EA60081310EA3060EA0F 800F127C9113>II<13F8EA0704120CEA 1802EA38041230EA7008EA7FF0EAE000A5EA60041308EA30101360EA0F800F127C9113> IIII I107 DI< 391C1E078039266318C0394683A0E0384703C0008E1380A2120EA2391C0701C0A3EC0380 D8380E1388A2EC0708151039701C032039300C01C01D127C9122>II<13F8EA030CEA0E06487E1218123000701380A238E00700A3130EA25BEA6018 5BEA30E0EA0F8011127C9115>I<380387803804C860EBD03013E0EA09C014381201A238 038070A31460380700E014C0EB0180EB8300EA0E86137890C7FCA25AA45AB4FC151A8091 15>IIII< 12035AA3120EA4EAFFE0EA1C00A35AA45AA4EAE080A2EAE100A2126612380B1A7C990E> I<381C0180EA2E03124EA2388E0700A2121CA2EA380EA438301C80A3EA383C38184D00EA 0F8611127C9116>II<381E0183382703871247148338870701A2120E A2381C0E02A31404EA180C131C1408EA1C1E380C26303807C3C018127C911C>I<380387 80380CC840380870E012103820E0C014001200A2485AA4EA03811263EAE38212C5EA8584 EA787813127E9113>I<381C0180EA2E03124EA2388E0700A2121CA2EA380EA4EA301CA3 EA383CEA1878EA0FB8EA003813301370EAE0605BEA81800043C7FC123C111A7C9114>I< EA01C1EA07E1EA0FF6EA081CEA1008EA0010132013401380EA010012025AEA08041210EA 2C0CEA73F8EA41F0EA80E010127E9111>I E /Fr 52 127 df<13F8EA030C380E0604EA 1C07383803080030138800701390A200E013A0A214C01480A3EA6007EB0B883830719038 0F80E016127E911B>11 D<1206120EA35AA45AA35A1340A2EAE080A2EA6300123C0A127E 910F>19 D<380601C0380E07E01309EB10C0381C20005BEA1D80001EC7FCEA3FF0EA3838 7FA200701320A31440EAE00C3860078013127E9118>II<3801803000031370A3380700E0A4 380E01C0A4381C0388A3EA1E07383E1990383BE0E00038C7FCA25AA45AA25A151B7F9119 >I<007E1360000E13E0A3381C01C0A2EB03801400485A130E130C5B485A5BEA71C00073 C7FC12FC12F013127E9115>I<131EEB7180EBC0C0EA01801203EB00E05AA2380E01C0A3 1480EA1C0314001306EA1E0CEA3A18EA39E00038C7FCA25AA45AA25A131B7F9115>26 D<3801FFF85A120F381E1E00EA180EEA38061270A2EAE00EA3130C131C13185BEA60606C 5A001FC7FC15127E9118>I<380FFFE05A5A3860C0001240485A12001201A348C7FCA35A A3120E120613127E9112>I<13FCEA03FEEA0E07EA180012105AA2EA10C0EA1720EA1FE0 EA20005AA25AA21304EA4008EA6030EA3FE0EA0F8010147F9213>34 D<126012F0A2126004047C830C>58 D<126012F0A212701210A41220A212401280040C7C 830C>II<140CA2141CA2143C145CA2149E148EEB010E1302A21304A213081310A2497EEB 3FFFEB40071380A2EA0100A212025AA2001C148039FF803FF01C1D7F9C1F>65 D<48B5FC39003C01C090383800E015F01570A25B15F0A2EC01E09038E003C0EC0780EC1F 00EBFFFC3801C00FEC0780EC03C0A2EA0380A439070007801500140E5C000E1378B512C0 1C1C7E9B1F>I<903801F80890380E0618903838013890386000F048481370485A48C712 30481420120E5A123C15005AA35AA45CA300701302A200305B00385B6C5B6C1360380701 80D800FEC7FC1D1E7E9C1E>I<48B5128039003C01E090383800701538153C151C5B151E A35BA44848133CA3153848481378157015F015E039070001C0EC0380EC0700141C000E13 78B512C01F1C7E9B22>I<48B512F038003C00013813301520A35BA214081500495AA214 30EBFFF03801C020A448485A91C7FCA348C8FCA45AEAFFF01C1C7E9B1B>70 D<903801F80890380E0618903838013890386000F048481370485A48C71230481420120E 5A123C15005AA35AA2EC7FF0EC07801500A31270140E123012386C131E6C136438070184 D800FEC7FC1D1E7E9C21>I<3A01FFC3FF803A003C00780001381370A4495BA449485AA3 90B5FC3901C00380A4484848C7FCA43807000EA448131E39FFE1FFC0211C7E9B23>I<38 01FFE038003C001338A45BA45BA4485AA438038002A31404EA0700140C14181438000E13 F0B5FC171C7E9B1C>76 DIII<48B5FC39003C03C090383800E015F01570A24913F0A315E0EB E001EC03C0EC0700141E3801FFF001C0C7FCA3485AA448C8FCA45AEAFFE01C1C7E9B1B> II<3801FFFE3900 3C03C090383800E015F01570A24913F0A3EC01E001E013C0EC0780EC1E00EBFFF03801C0 38140C140EA2EA0380A43807001E1508A2151048130FD8FFE01320C7EA03C01D1D7E9B20 >II<001FB512F0391C03807039300700300020142012601240130E12 80A2000014005BA45BA45BA45BA41201EA7FFF1C1C7F9B18>I<3A01FFC0FF803A001E00 3C00011C13306D13205D010F5B6D48C7FC1482EB038414CCEB01D814F05C130080EB0170 EB0278EB04381308EB103CEB201CEB401EEB800E3801000F00027F1206001E497E39FF80 3FF0211C7F9B22>88 D<90B512E09038F001C03901C003809038800700EB000E141E0002 131C5C5CC75A495A495A49C7FC5B131E131C5BEB7002495AEA01C0EA038048485A5A000E 1318485B48137048485AB5FC1B1C7E9B1C>90 D97 D99 D102 D104 DI<1307130FA213061300A61378139CEA010C1202131C12041200A21338A41370A413E0 A4EA01C01261EAF180EAF30012E6127C1024809B11>III<39381F81F0394E20C618394640E81CEB80F0EA8F00 008E13E0120EA2391C01C038A315703938038071A215E115E23970070064D83003133820 127E9124>II<380787803809C8603808D03013 E0EA11C014381201A238038070A31460380700E014C0EB0180EB8300EA0E86137890C7FC A25AA4123CB4FC151A819115>112 D114 D I<13C01201A3EA0380A4EAFFF0EA0700A3120EA45AA4EA3820A21340A2EA1880EA0F000C 1A80990F>I<001C13C0EA27011247A238870380A2120EA2381C0700A438180E20A3EA1C 1E380C26403807C38013127E9118>II<001CEBC080392701C1C01247 14C03987038040A2120EA2391C070080A3EC0100EA1806A2381C0E02EB0F04380E130838 03E1F01A127E911E>I<380787803808C8403810F0C03820F1E0EBE3C03840E1803800E0 00A2485AA43863808012F3EB810012E5EA84C6EA787813127E9118>I<001C13C0EA2701 1247A238870380A2120EA2381C0700A4EA180EA3EA1C1EEA0C3CEA07DCEA001C1318EA60 38EAF0305B485AEA4180003EC7FC121A7E9114>II<13021303A2B51280A238000700130C13081108789D15>126 D E /Fs 28 107 df0 D<126012F0A2126004047C8B0C>I<1203 A4EAC30CEAE31CEA7338EA1FE0EA0780A2EA1FE0EA7338EAE31CEAC30CEA0300A40E127D 9215>3 D15 D<90387FFF800003B5FCD80780C7FC000CC8FC5A5AA25AA25A A81260A27EA27E120E6C7E0001B512806C7E90C8FCA8007FB51280A219247D9920>18 D20 D<12C012F0123C120FEA03C0EA00F01338130E6D7EEB01E0 EB0078141EEC0780A2EC1E001478EB01E0EB0780010EC7FC133813F0EA03C0000FC8FC12 3C127012C0C9FCA8007FB5FCB6128019247D9920>I<153081A381A281811680ED00C0B7 12F8A2C912C0ED0380160015065DA25DA35D25167E942A>33 D<01C0136048487FA348C7 7EA20006804880001C14070030EC0180B712F0A20030C7EA0180001CEC0700000C14066C 5C6C5CA26C6C5BA36C6C5B24167D942A>36 D<13065BA25B13381330017FB512F848B6FC D80380C8FC000EC9FC123C12F01238120E7EEA01806CB612F87F0130C8FC7FA27FA27F25 187E952A>40 D<14036E7EA26E7E811560B612F015FCC8120EED0380ED01E0ED007816E0 ED0380ED0700150CB612F85DC812605DA24A5AA24AC7FC25187E952A>I50 D<1460A214C0A2EB0180A3EB0300A21306A25BA25BA35B A25BA25BA2485AA248C7FCA31206A25AA25AA25AA35AA25A124013287A9D00>54 D<12C0A612E0A212C0A6030E7E9000>I<0040130400C0130C00601318A36C1330A36C13 60A2381FFFE06C13C0EA0C00A238060180A238030300A3EA0186A3EA00CCA31378A31330 A2161E809C17>III<1304130CB3A7B612E0A21B1C7D9B21>63 D<152015E01401A21403A21405A21409A214111431142114611441148113011401130313 06130490380FFFF05BEB3000A25BEA60C0D8718013F8127F48C7127E007E147C003C1400 1F20809D21>65 D67 DI<14 7E49B4FCEB031FEB060F130C1318EB380CEB78080170C7FCA25BA21201A25BA212035BA2 1207A290C8FCA2000E14801403391FE00700EBFC063831FF8C38603FF838C007E0191E7F 9C1D>76 D82 D<13101338A2136CA313C6A2EA0183A238030180A2380600C0A3481360A2481330A24813 18A348130CA24813061402171A7E981C>94 D<124012C0ACB512E014F000C0C7FCAD1240 141D7E9C19>96 D<133C13E0EA01C013801203AD13005A121C12F0121C12077E1380AD12 0113C0EA00E0133C0E297D9E15>102 D<12F0121C12077E1380AD120113C0EA00E0133C 13E0EA01C013801203AD13005A121C12F00E297D9E15>I<12C0B3B3A502297B9E0C>106 D E /Ft 81 128 df11 D<137E3801C180EA0301380703C0120E EB018090C7FCA5B512C0EA0E01B0387F87F8151D809C17>II<90383F07E03901C09C18380380F0D8 0701133C000E13E00100131892C7FCA5B612FC390E00E01CB03A7FC7FCFF80211D809C23 >I<126012F0A71260AD1200A5126012F0A21260041E7C9D0C>33 D I<126012F012F812681208A31210A2122012401280050C7C9C0C>39 D<1380EA0100120212065AA25AA25AA35AA412E0AC1260A47EA37EA27EA27E12027EEA00 80092A7C9E10>I<7E12407E12307EA27EA27EA37EA41380AC1300A41206A35AA25AA25A 12205A5A092A7E9E10>I<1306ADB612E0A2D80006C7FCAD1B1C7E9720>43 D<126012F0A212701210A41220A212401280040C7C830C>II<12 6012F0A2126004047C830C>I48 D<5A1207123F12C71207B3A5EAFFF80D1C7C9B15>III<130CA2131C133CA2135C13DC139CEA011C12 0312021204120C1208121012301220124012C0B512C038001C00A73801FFC0121C7F9B15 >II<13F0EA030CEA0404 EA0C0EEA181E1230130CEA7000A21260EAE3E0EAE430EAE818EAF00C130EEAE0061307A5 1260A2EA7006EA300E130CEA1818EA0C30EA03E0101D7E9B15>I<1240387FFF801400A2 EA4002485AA25B485AA25B1360134013C0A212015BA21203A41207A66CC7FC111D7E9B15 >III<126012F0A212601200AA126012F0A2126004127C910C>I<126012F0A212601200 AA126012F0A212701210A41220A212401280041A7C910C>I61 D<1306A3130FA3EB1780A2EB37C01323A2EB43E01341A2EB80F0A33801 0078A2EBFFF83802003CA3487FA2000C131F80001E5BB4EBFFF01C1D7F9C1F>65 DI<90381F8080EBE0613801801938070007000E1303 5A14015A00781300A2127000F01400A8007014801278A212386CEB0100A26C13026C5B38 0180083800E030EB1FC0191E7E9C1E>IIII<90381F8080EBE061380180193807000700 0E13035A14015A00781300A2127000F01400A6ECFFF0EC0F80007013071278A212387EA2 7E6C130B380180113800E06090381F80001C1E7E9C21>I<39FFF0FFF0390F000F00AC90 B5FCEB000FAD39FFF0FFF01C1C7F9B1F>II<38 07FF8038007C00133CB3127012F8A21338EA7078EA4070EA30E0EA0F80111D7F9B15>I< 39FFF01FE0390F000780EC060014045C5C5C5C5C49C7FC13021306130FEB17801327EB43 C0EB81E013016D7E1478A280143E141E80158015C039FFF03FF01C1C7F9B20>IIIIII82 D<3807E080EA1C19EA30 051303EA600112E01300A36C13007E127CEA7FC0EA3FF8EA1FFEEA07FFC61380130FEB07 C0130313011280A300C01380A238E00300EAD002EACC0CEA83F8121E7E9C17>I<007FB5 12C038700F010060130000401440A200C014201280A300001400B1497E3803FFFC1B1C7F 9B1E>I<39FFF01FF0390F000380EC0100B3A26C1302138000035BEA01C03800E018EB70 60EB0F801C1D7F9B1F>I<39FFE00FF0391F0003C0EC01806C1400A238078002A213C000 035BA2EBE00C00011308A26C6C5AA213F8EB7820A26D5AA36D5AA2131F6DC7FCA21306A3 1C1D7F9B1F>I<3AFFE1FFC0FF3A1F003E003C001E013C13186C6D1310A32607801F1320 A33A03C0278040A33A01E043C080A33A00F081E100A39038F900F3017913F2A2017E137E 013E137CA2013C133C011C1338A20118131801081310281D7F9B2B>I<39FFF003FC390F 8001E00007EB00C06D13800003EB01006D5A000113026C6C5A13F8EB7808EB7C18EB3C10 EB3E20131F6D5A14C06D5AABEB7FF81E1C809B1F>89 D<12FEA212C0B3B312FEA207297C 9E0C>91 DI<12FEA21206B3B312FEA20729809E0C>I97 D<12FC121CAA137CEA1D87381E0180381C00C014E014601470A6146014E014C0381E0180 38190700EA10FC141D7F9C17>IIII<13F8EA018CEA071E1206EA0E0C1300A6EAFFE0EA0E00B0EA7F E00F1D809C0D>II<12FC121CAA137C1387EA1D03001E1380121CAD38 FF9FF0141D7F9C17>I<1218123CA21218C7FCA712FC121CB0EAFF80091D7F9C0C>I<13C0 EA01E0A2EA00C01300A7EA07E01200B3A21260EAF0C012F1EA6180EA3E000B25839C0D> I<12FC121CAAEB0FE0EB0780EB06005B13105B5B13E0121DEA1E70EA1C781338133C131C 7F130F148038FF9FE0131D7F9C16>I<12FC121CB3A9EAFF80091D7F9C0C>I<39FC7E07E0 391C838838391D019018001EEBE01C001C13C0AD3AFF8FF8FF8021127F9124>IIII<3803E080EA0E19EA1805EA3807EA7003A212E0 A61270A2EA38071218EA0E1BEA03E3EA0003A7EB1FF0141A7F9116>II I<1204A4120CA2121C123CEAFFE0EA1C00A91310A5120CEA0E20EA03C00C1A7F9910>I< 38FC1F80EA1C03AD1307120CEA0E1B3803E3F014127F9117>I<38FF07E0383C0380381C 0100A2EA0E02A2EA0F06EA0704A2EA0388A213C8EA01D0A2EA00E0A3134013127F9116> I<39FF3FC7E0393C0703C0001CEB01801500130B000E1382A21311000713C4A213203803 A0E8A2EBC06800011370A2EB8030000013201B127F911E>I<38FF0FE0381E0700EA1C06 EA0E046C5AEA039013B0EA01E012007F12011338EA021C1204EA0C0E487E003C138038FE 1FF014127F9116>I<38FF07E0383C0380381C0100A2EA0E02A2EA0F06EA0704A2EA0388 A213C8EA01D0A2EA00E0A31340A25BA212F000F1C7FC12F312661238131A7F9116>III126 DI E /Fu 34 121 df<49B4FC011F13C090387F81E0EBFC013901F807F01203EA07F0A4EC01C091C8 FCA3EC3FF8B6FCA33807F003B3A33A7FFF3FFF80A3212A7FA925>12 D<130E131E137EEA07FE12FFA212F81200B3ABB512FEA317277BA622>49 DII<140FA25C5C5C5C5BA2EB03 BFEB073F130E131C133C1338137013E0EA01C0EA038012071300120E5A5A5A12F0B612F8 A3C7EA7F00A890381FFFF8A31D277EA622>I<00181303381F801FEBFFFE5C5C5C14C091 C7FC001CC8FCA7EB7FC0381DFFF8381F80FC381E003F1208C7EA1F8015C0A215E0A21218 127C12FEA315C05A0078EB3F80A26CEB7F00381F01FE6CB45A000313F0C613801B277DA6 22>II65 D<91387FE003903907FFFC07 011FEBFF0F90397FF00F9F9039FF0001FFD801FC7F4848147F4848143F4848141F485A16 0F485A1607127FA290C9FC5AA97E7F1607123FA26C7E160E6C7E6C6C141C6C6C143C6C6C 14786CB4EB01F090397FF007C0011FB512800107EBFE009038007FF028297CA831>67 DIII<91387FE003903907FFFC07011FEBFF0F90397FF00F9F9039FF0001FF D801FC7F484880484880484880485A82485A82127FA290CAFC5AA892B512F87E7F030013 00123FA26C7EA26C7E6C7E6C7E6C7E6CB45B90387FF007011FB5129F0107EBFE0F903900 7FF0032D297CA835>I73 D80 D82 D<3803FF80000F13F0381F01FC383F80FE147F801580EA1F00C7FCA4EB3FFF 3801FC3FEA0FE0EA1F80EA3F00127E5AA4145F007E13DF393F839FFC381FFE0F3803FC03 1E1B7E9A21>97 D99 DIII<9038FF80F00003EBE3F839 0FC1FE1C391F007C7C48137E003EEB3E10007EEB3F00A6003E133E003F137E6C137C380F C1F8380BFFE00018138090C8FC1238A2123C383FFFF814FF6C14C06C14E06C14F0121F38 3C0007007CEB01F8481300A4007CEB01F0A2003FEB07E0390FC01F806CB5120038007FF0 1E287E9A22>II<1207EA0F80EA1FC0EA3FE0A3EA1FC0EA 0F80EA0700C7FCA7EAFFE0A3120FB3A3EAFFFEA30F2B7EAA12>I108 D<26FFC07FEB1FC0903AC1FFC07FF0903AC307E0C1F8D80FC4 9038F101FC9039C803F20001D801FE7F01D05BA201E05BB03CFFFE3FFF8FFFE0A3331B7D 9A38>I<38FFC07E9038C1FF809038C30FC0D80FC413E0EBC80701D813F013D0A213E0B0 39FFFE3FFFA3201B7D9A25>II<38FFE1FE9038EFFF809038FE0FE0390FF8 03F09038F001F801E013FC140015FEA2157FA8157E15FEA215FC140101F013F89038F807 F09038FC0FE09038EFFF809038E1FC0001E0C7FCA9EAFFFEA320277E9A25>I<38FFC1F0 EBC7FCEBC63E380FCC7F13D813D0A2EBF03EEBE000B0B5FCA3181B7F9A1B>114 D<3803FE30380FFFF0EA3E03EA7800127000F01370A27E00FE1300EAFFE06CB4FC14C06C 13E06C13F0000713F8C6FCEB07FC130000E0137C143C7E14387E6C137038FF01E038E7FF C000C11300161B7E9A1B>I<13E0A41201A31203A21207120F381FFFE0B5FCA2380FE000 AD1470A73807F0E0000313C03801FF8038007F0014267FA51A>I<39FFE07FF0A3000F13 07B2140FA2000713173903F067FF3801FFC738007F87201B7D9A25>I<39FFFC1FFEA339 07F003803803F8079038FC0F003801FE1E00005BEB7F3814F86D5A6D5A130F806D7E130F 497EEB3CFEEB38FFEB787F9038F03F803901E01FC0D803C013E0EB800F39FFF03FFFA320 1B7F9A23>120 D E /Fv 3 95 df<1202A3EAC218EAF278EA3AE0EA0F80A2EA3AE0EAF2 78EAC218EA0200A30D0E7E8E12>3 D<1406A380A2EC0180EC00C01560B612FCA2C81260 15C0EC0180EC0300A21406A31E127E9023>33 D<134013E0A2EA01B0A2EA0318A2EA060C A2487EA2487EA238300180A2386000C0A2481360142013137E9218>94 D E /Fw 29 123 df<127012F812FCA212741204A41208A21210A212201240060F7C840E >44 D48 D<13801203120F12F312 03B3A9EA07C0EAFFFE0F217CA018>II<1303A25BA25B1317A21327 136713471387120113071202120612041208A212101220A2124012C0B512F838000700A7 EB0F80EB7FF015217FA018>52 D66 D<39FFFC3FFF390FC003F03907 8001E0AE90B5FCEB8001AF390FC003F039FFFC3FFF20227EA125>72 D77 D<3803F020380C0C60EA1802383001E0EA70000060136012 E0A21420A36C1300A21278127FEA3FF0EA1FFE6C7E0003138038003FC0EB07E01301EB00 F0A214707EA46C1360A26C13C07E38C8018038C60700EA81FC14247DA21B>83 D<39FFFC07FF390FC000F86C4813701520B3A5000314407FA2000114806C7E9038600100 EB3006EB1C08EB03F020237EA125>85 D<3BFFF03FFC03FE3B1F8007E000F86C486C4813 7017206E7ED807801540A24A7E2603C0021480A39039E004780100011600A2EC083CD800 F01402A2EC101E01785CA2EC200F013C5CA20260138890391E400790A216D090391F8003 F0010F5CA2EC00016D5CA20106130001025C2F237FA132>87 D97 D<120E12FE121E120EAB131FEB61C0EB8060380F0030000E1338 143C141C141EA7141C143C1438000F1370380C8060EB41C038083F0017237FA21B>II<14E0130F13011300ABEA01F8EA0704EA0C02EA1C 01EA38001278127012F0A7127012781238EA1801EA0C0238070CF03801F0FE17237EA21B >II<133E13E33801C780EA03 87130748C7FCA9EAFFF80007C7FCB27FEA7FF0112380A20F>I<14703803F198380E1E18 EA1C0E38380700A200781380A400381300A2EA1C0EEA1E1CEA33F00020C7FCA212301238 EA3FFE381FFFC06C13E0383000F0481330481318A400601330A2003813E0380E03803803 FE0015217F9518>I<120E12FE121E120EABEB1F80EB60C0EB80E0380F0070A2120EAF38 FFE7FF18237FA21B>I<121C123EA3121CC7FCA8120E127E121E120EB1EAFFC00A227FA1 0E>I<120E12FE121E120EB3ADEAFFE00B237FA20E>108 D<390E1FC07F3AFE60E183803A 1E807201C03A0F003C00E0A2000E1338AF3AFFE3FF8FFE27157F942A>I<380E1F8038FE 60C0381E80E0380F0070A2120EAF38FFE7FF18157F941B>II114 D<1202A41206A3120E121E123EEAFFFCEA0E00AB1304A6EA0708 1203EA01F00E1F7F9E13>116 D<000E137038FE07F0EA1E00000E1370AD14F0A2380601 70380382783800FC7F18157F941B>I<39FF8FF87F393E01E03C001CEBC01814E0000E14 10EB0260147000071420EB04301438D803841340EB8818141CD801C81380EBD00C140E39 00F00F00497EA2EB6006EB400220157F9423>119 D<383FFFC038380380EA3007002013 00EA600EEA401C133C1338C65A5B12015B38038040EA07005A000E13C04813805AEA7801 EA7007B5FC12157F9416>122 D E /Fx 20 121 df12 D<91383FE001903901FFF803903807F01E90391F800307 013EC712870178144F49142F4848141F4848140F485A000F150790C8FC481503121E123E 003C1501127CA30078150012F8AB1278127C1601A2123C123E121E001F15027E6D140600 0715046C6C14086C7E6C6C141001781420013E14C090391F800380903907F00F00903801 FFFC9038003FE028337CB130>67 D69 D80 D82 D<13FE380303C0380C00E00010137080003C133C003E131C141EA21208C7FCA3EB0FFEEB FC1EEA03E0EA0F80EA1F00123E123C127C481404A3143EA21278007C135E6CEB8F08390F 0307F03903FC03E01E1F7D9E21>97 D99 D<15F0141FA214011400AFEB0FC0EB70 303801C00C3803800238070001120E001E13005AA2127C1278A212F8A71278A2127C123C A27E000E13016C1302380380046C6C487E3A00F030FF80EB1FC021327EB125>III<15F090387F03083901C1C41C380380E83907007008 48EB7800001E7FA2003E133EA6001E133CA26C5B6C13706D5A3809C1C0D8087FC7FC0018 C8FCA5121C7E380FFFF86C13FF6C1480390E000FC00018EB01E048EB00F0007014704814 38A500701470A26C14E06CEB01C00007EB07003801C01C38003FE01E2F7E9F21>I<120F EA1F80A4EA0F00C7FCABEA0780127FA2120F1207B3A6EA0FC0EAFFF8A20D307EAF12> 105 D108 D<260780FEEB1FC03BFF83078060F0903A8C03C180783B0F9001E2003CD807A013E4DA00 F47F01C013F8A2495BB3A2486C486C133F3CFFFC1FFF83FFF0A2341F7E9E38>I<380780 FE39FF83078090388C03C0390F9001E0EA07A06E7E13C0A25BB3A2486C487E3AFFFC1FFF 80A2211F7E9E25>II<380783E038FF8418EB887CEA0F 90EA07A01438EBC000A35BB3487EEAFFFEA2161F7E9E19>114 D<3801FC10380E033038 1800F048137048133012E01410A37E6C1300127EEA3FF06CB4FC6C13C0000313E038003F F0EB01F813006C133CA2141C7EA27E14186C1338143000CC136038C301C03880FE00161F 7E9E1A>I<1340A513C0A31201A212031207120F381FFFE0B5FC3803C000B01410A80001 132013E000001340EB78C0EB1F00142C7FAB19>I<39FFF003FFA2390FE001F8D803C013 E001E01380000191C7FC6C6C5AEB7802EB7C04EB3C086D5AEB0F3014A0EB07C01303806D 7E1302EB0478EB087CEB183EEB101E497E01407F9038C007C0EB800348486C7E000780D8 1F807F3AFFC007FFC0A2221F7F9E23>120 D E end %%EndProlog %%BeginSetup %%Feature: *Resolution 300dpi TeXDict begin %%PaperSize: a4 %%EndSetup %%Page: 1 1 1 0 bop 257 436 a Fx(Re\014ned)19 b(Program)g(Extraction)g(from)g (Classical)f(Pro)r(ofs)316 556 y Fw(Ulric)o(h)d(Berger,)g(Wilfried)f (Buc)o(hholz)h(and)i(Helm)o(ut)d(Sc)o(h)o(wic)o(h)o(ten)o(b)q(erg)1633 538 y Fv(\003)810 654 y Fw(Marc)o(h)h(24,)i(2001)257 895 y Fu(1)67 b(In)n(tro)r(duction)257 986 y Ft(It)12 b(is)f(w)o(ell)g(kno)o(wn)f(that)i(it)f(is)g(undecidable)h(in)f (general)g(whether)i(a)e(giv)o(en)g(program)e(meets)257 1036 y(its)16 b(sp)q(eci\014cation.)23 b(In)15 b(con)o(trast,)h(it)f (can)h(b)q(e)f(c)o(hec)o(k)o(ed)i(easily)e(b)o(y)g(a)g(mac)o(hine)f (whether)j(a)257 1086 y(formal)f(pro)q(of)h(is)h(correct,)j(and)c(from) g(a)g(constructiv)o(e)j(pro)q(of)d(one)h(can)h(automatically)257 1135 y(extract)f(a)e(corresp)q(onding)i(program,)d(whic)o(h)h(b)o(y)h (its)f(v)o(ery)h(construction)h(is)e(correct)i(as)257 1185 y(w)o(ell.)f(This)c({)f(at)g(least)h(in)f(principle)h({)f(op)q (ens)h(a)g(w)o(a)o(y)e(to)i(pro)q(duce)h(correct)g(soft)o(w)o(are,)e (e.g.)257 1235 y(for)18 b(safet)o(y-critical)f(applications.)28 b(Moreo)o(v)o(er,)19 b(programs)d(obtained)i(from)d(pro)q(ofs)j(are)257 1285 y(\\commen)o(ted")11 b(in)i(a)g(rather)h(extreme)f(sense.)19 b(Therefore)c(it)d(is)h(easy)h(to)e(main)o(tain)f(them,)257 1335 y(and)j(also)f(to)h(adapt)g(them)f(to)h(particular)f(situations.) 320 1384 y(W)m(e)i(will)f(concen)o(trate)j(on)e(the)h(question)g(of)e (classical)i(v)o(ersus)g(constructiv)o(e)h(pro)q(ofs.)257 1434 y(It)c(is)f(kno)o(wn)g(that)g(an)o(y)g(classical)f(pro)q(of)h(of)g (a)g(sp)q(eci\014cation)h(of)e(the)i(form)e Fs(8)p Fr(x)p Fs(9)p Fr(y)q(B)k Ft(with)d Fr(B)257 1484 y Ft(quan)o(ti\014er-free)g (can)f(b)q(e)h(transformed)e(in)o(to)g(a)h(constructiv)o(e)h(pro)q(of)f (of)f(the)h(same)f(form)o(ula.)257 1534 y(Ho)o(w)o(ev)o(er,)18 b(when)f(it)g(comes)f(to)g(extraction)i(of)e(a)g(program)f(from)g(a)i (pro)q(of)f(obtained)h(in)257 1584 y(this)g(w)o(a)o(y)m(,)e(one)i (easily)f(ends)h(up)g(with)f(a)g(mess.)25 b(Therefore,)18 b(some)e(re\014nemen)o(ts)h(of)f(the)257 1633 y(standard)f (transformation)d(are)i(necessary)m(.)320 1683 y(In)c(this)g(pap)q(er)h (w)o(e)f(dev)o(elop)g(a)g(re\014ned)i(metho)q(d)d(of)g(extracting)i (reasonable)g(and)e(some-)257 1733 y(times)j(unexp)q(ected)j(programs)c (from)g(classical)i(pro)q(ofs.)k(W)m(e)12 b(also)g(generalize)i (previously)257 1783 y(kno)o(wn)g(results)g(since)h Fr(B)h Ft(in)e Fs(8)p Fr(x)p Fs(9)p Fr(y)q(B)i Ft(no)e(longer)f(needs)i(to)f (b)q(e)g(quan)o(ti\014er-free,)g(but)g(only)257 1833 y(has)i(to)g(b)q(elong)g(to)f(the)i(strictly)f(larger)g(class)g(of)f Fq(go)n(al)i(formulas)h Ft(de\014ned)f(in)f(section)g(3.)257 1883 y(F)m(urthermore)d(w)o(e)g(allo)o(w)e(unpro)o(v)o(en)i(lemmas)d Fr(D)k Ft(in)f(the)g(pro)q(of)f(of)g Fs(8)p Fr(x)p Fs(9)p Fr(y)q(B)r Ft(,)i(where)g Fr(D)g Ft(is)f(a)257 1932 y Fq(de\014nite)18 b Ft(form)o(ula)11 b(\(also)j(de\014ned)h(in)e (section)i(3\).)320 1982 y(Other)f(in)o(teresting)f(examples)f(of)g (program)g(extraction)h(from)e(classical)i(pro)q(ofs)g(ha)o(v)o(e)257 2032 y(b)q(een)e(studied)f(b)o(y)g Fp(Mur)m(thy)i Ft([16)o(],)e Fp(Coquand)p Ft('s)h(group)e(\(see)i(e.g.)e([6)o(]\))h(in)f(a)g(t)o(yp) q(e)h(theoretic)257 2082 y(con)o(text)15 b(and)f(b)o(y)g Fp(K)o(ohlenba)o(ch)i Ft([13)o(])d(using)h(a)g(Dialectica-in)o (terpretation.)320 2132 y(There)21 b(is)g(also)f(a)g(di\013eren)o(t)i (line)e(of)g(researc)o(h)i(aimed)d(at)i(giving)e(an)h(algorithmic)257 2181 y(in)o(terpretation)f(to)e(\(sp)q(eci\014c)j(instances)f(of)s(\))f (the)g(classical)g(double)g(negation)f(rule.)30 b(It)257 2231 y(essen)o(tially)20 b(started)h(with)e Fp(Griffin)p Ft('s)h(observ)n(ation)f([12)o(])g(that)h Fp(Felleisen)p Ft('s)g(con)o(trol)257 2281 y(op)q(erator)13 b Fs(C)i Ft([9)o(,)d(10])g(can)g(b)q(e)h(giv)o(en)f(the)h(t)o(yp)q(e)g(of)f(the) h(stabilit)o(y)e(sc)o(heme)i Fs(::)p Fr(A)e Fs(!)g Fr(A)p Ft(.)18 b(This)257 2331 y(initiated)d(quite)g(a)g(bit)g(of)g(w)o(ork)g (aimed)e(at)i(extending)h(the)g(Curry-Ho)o(w)o(ard)f(corresp)q(on-)p 257 2366 573 2 v 303 2392 a Fo(\003)321 2404 y Fn(The)d(hospitalit)o(y) c(of)k(the)f(Mittag-Le\017er)f(Institute)f(in)i(the)g(spring)g(of)g (2001)f(is)i(gratefully)d(ac)o(kno)o(w-)257 2443 y(ledged.)963 2628 y Ft(1)p eop %%Page: 2 2 2 1 bop 257 262 a Ft(dence)14 b(to)f(classical)f(logic,)f(e.g.)h(b)o(y) h Fp(Barbanera)i Ft(and)d Fp(Berardi)h Ft([1)o(],)f Fp(Const)m(able)i Ft(and)257 311 y Fp(Mur)m(thy)i Ft([5],)c Fp(Krivine)i Ft([14)o(])g(and)g Fp(P)l(arigot)f Ft([17)o(].)320 361 y(W)m(e)20 b(no)o(w)g(describ)q(e)j(in)d(more)g(detail)g(what)h(the)h (pap)q(er)f(is)g(ab)q(out.)38 b(In)21 b(section)h(2)257 411 y(w)o(e)d(\014x)g(our)g(v)o(ersion)g(of)f(in)o(tuitionistic)f (arithmetic)h(for)h(functionals,)g(and)f(recall)h(ho)o(w)257 461 y(classical)f(arithmetic)e(can)i(b)q(e)g(seen)h(as)e(a)g (subsystem.)30 b(Then)18 b(our)f(argumen)o(t)f(go)q(es)i(as)257 511 y(follo)o(ws.)e(It)d(is)f(w)o(ell)g(kno)o(wn)g(that)g(from)f(a)h (deriv)n(ation)f(of)h(a)g(classical)g(existen)o(tial)g(form)o(ula)257 560 y Fs(9)p Fr(y)q(A)k Ft(:=)e Fs(8)p Fr(y)q Ft(\()p Fr(A)i Fs(!)e(?)p Ft(\))g Fs(!)g(?)h Ft(one)h(generally)f(cannot)h (read)g(o\013)g(an)f(instance.)24 b(A)16 b(simple)257 610 y(example)g(has)h(b)q(een)h(giv)o(en)f(b)o(y)g Fp(Kreisel)p Ft(:)25 b(Let)17 b Fr(R)g Ft(b)q(e)h(a)f(primitiv)o(e)d(recursiv)o(e)19 b(relation)257 660 y(suc)o(h)c(that)f Fs(9)p Fr(z)r(R)p Ft(\()p Fr(x;)7 b(z)r Ft(\))13 b(is)h(undecidable.)19 b(Clearly)13 b(w)o(e)h(ha)o(v)o(e)g({)f(ev)o(en)i(logically)c({)715 743 y Fs(`)h(8)p Fr(x)p Fs(9)p Fr(y)q Fs(8)p Fr(z)r(:R)p Ft(\()p Fr(x;)7 b(z)r Ft(\))12 b Fs(!)f Fr(R)p Ft(\()p Fr(x;)c(y)q Ft(\))p Fr(:)257 826 y Ft(But)15 b(there)g(is)f(no)f (computable)g Fr(f)19 b Ft(satisfying)727 909 y Fs(8)p Fr(x)p Fs(8)p Fr(z)r(:R)p Ft(\()p Fr(x;)7 b(z)r Ft(\))j Fs(!)h Fr(R)p Ft(\()p Fr(x;)c(f)t Ft(\()p Fr(x)p Ft(\)\))p Fr(;)257 992 y Ft(for)12 b(then)g Fs(9)p Fr(z)r(R)p Ft(\()p Fr(x;)7 b(z)r Ft(\))k(w)o(ould)g(b)q(e)i(decidable:)k(it)11 b(w)o(ould)g(b)q(e)i(true)f(if)f(and)h(only)f(if)f Fr(R)p Ft(\()p Fr(x;)d(f)t Ft(\()p Fr(x)p Ft(\)\))257 1042 y(holds.)364 1027 y Fm(1)320 1092 y Ft(Ho)o(w)o(ev)o(er,)16 b(it)g(is)g(w)o(ell)f (kno)o(wn)h(that)g(in)g(case)h Fs(9)p Fr(y)q(G)f Ft(with)g Fr(G)g Ft(quan)o(ti\014er-free)h(one)f Fq(c)n(an)257 1142 y Ft(read)e(o\013)g(an)f(instance.)19 b(Here)c(is)e(a)g(simple)f (idea)i(of)f(ho)o(w)g(to)g(pro)o(v)o(e)h(this:)k(replace)c Fs(?)f Ft(an)o(y-)257 1192 y(where)e(in)e(the)h(pro)q(of)f(b)o(y)h Fs(9)665 1177 y Fl(\003)684 1192 y Fr(y)q(G)g Ft(\(w)o(e)g(use)g Fs(9)911 1177 y Fl(\003)939 1192 y Ft(for)g(the)g(constructiv)o(e)h (existen)o(tial)e(quan)o(ti\014er\).)257 1242 y(Then)15 b(the)f(end)h(form)o(ula)c Fs(8)p Fr(y)q Ft(\()p Fr(G)h Fs(!)f(?)p Ft(\))g Fs(!)h(?)h Ft(is)g(turned)i(in)o(to)f Fs(8)p Fr(y)q Ft(\()p Fr(G)e Fs(!)f(9)1427 1226 y Fl(\003)1446 1242 y Fr(y)q(G)p Ft(\))h Fs(!)f(9)1604 1226 y Fl(\003)1623 1242 y Fr(y)q(G)p Ft(,)257 1291 y(and)j(since)h(the)f(premise)g(is)g (trivially)e(pro)o(v)n(able,)g(w)o(e)i(ha)o(v)o(e)g(the)h(claim.)320 1341 y(Unfortunately)m(,)21 b(this)g(simple)e(argumen)o(t)h(is)h(not)f (quite)h(correct.)41 b(First,)22 b Fr(G)e Ft(ma)o(y)257 1391 y(con)o(tain)12 b Fs(?)p Ft(,)g(and)g(hence)i(is)f(c)o(hanged)g (under)g(the)g(substitution)g Fs(?)e(7!)g(9)1388 1376 y Fl(\003)1407 1391 y Fr(y)q(G)p Ft(.)18 b(Second,)13 b(w)o(e)257 1441 y(ma)o(y)h(ha)o(v)o(e)i(used)g(axioms)e(or)h(lemmata)e (in)o(v)o(olving)g Fs(?)i Ft(\(e.g.)g Fs(?)f(!)g Fr(P)6 b Ft(\),)15 b(whic)o(h)h(need)h(not)257 1491 y(b)q(e)e(deriv)n(able)f (after)g(the)h(substitution.)k(But)c(in)f(spite)h(of)e(this,)h(the)h (simple)d(idea)i(can)h(b)q(e)257 1540 y(turned)g(in)o(to)e(something)g (useful.)320 1590 y(T)m(o)e(tak)o(e)i(care)g(of)f(lemmata)d(w)o(e)k (normally)d(w)o(an)o(t)i(to)g(use)i(in)e(a)g(deriv)n(ation)g(of)g Fs(9)p Fr(y)q(G)p Ft(,)g(let)257 1640 y(us)k(\014rst)f(sligh)o(tly)f (generalize)h(the)h(situation)e(w)o(e)h(are)g(lo)q(oking)e(at.)21 b(Let)15 b(a)g(deriv)n(ation)f(\(in)257 1695 y(minima)o(l)d(logic\))i (of)g Fs(9)p Fr(y)q(G)h Ft(from)775 1684 y Fr(~)769 1695 y(D)h Ft(and)f(axioms)496 1778 y Fk(Ind)550 1784 y Fj(n;A)612 1778 y Ft(:)55 b Fr(A)p Ft([)p Fr(n)11 b Ft(:=)h(0])e Fs(!)h(8)p Fr(n)p Ft(\()p Fr(A)h Fs(!)f Fr(A)p Ft([)p Fr(n)g Ft(:=)h Fr(n)d Ft(+)g(1]\))i Fs(!)g(8)p Fr(nA)499 1840 y Fk(Ind)554 1846 y Fj(p;A)612 1840 y Ft(:)55 b Fr(A)p Ft([)p Fr(p)11 b Ft(:=)h Fk(true)q Ft(])f Fs(!)g Fr(A)p Ft([)p Fr(p)g Ft(:=)g Fk(false)p Ft(])g Fs(!)g(8)p Fr(pA)515 1902 y Fk(ax)554 1908 y Fi(true)612 1902 y Ft(:)55 b Fk(atom)o Ft(\()p Fk(true)q Ft(\))474 1965 y Fk(ax)514 1971 y Fi(false)o Fj(;A)612 1965 y Ft(:)g Fk(atom)o Ft(\()p Fk(false)p Ft(\))11 b Fs(!)h Fr(A)257 2048 y Ft(b)q(e)17 b(giv)o(en.)26 b(Here)17 b Fk(atom)e Ft(is)i(a)f(unary)g(predicate)i(sym)o(b)q(ol)c(taking)i(one)h(argumen)o (t)e(of)h(the)257 2098 y(t)o(yp)q(e)e Fk(o)e Ft(of)g(b)q(o)q(oleans.)18 b(The)13 b(in)o(tended)g(in)o(terpretation)g(of)f Fk(atom)f Ft(is)i(the)g(set)h Fs(f)p Fk(true)q Fs(g)p Ft(;)e(hence)257 2152 y(\\)p Fk(atom)o Ft(\()p Fr(t)p Ft(\)")k(means)f(\\)p Fr(t)f Ft(=)i Fk(true)q Ft(".)23 b(Assume)16 b(the)h(lemmata)1212 2142 y Fr(~)1205 2152 y(D)h Ft(and)d(the)i(goal)e(form)o(ula)e Fr(G)257 2202 y Ft(are)i(suc)o(h)f(that)730 2285 y Fs(`)755 2291 y Fi(int)810 2275 y Fr(~)804 2285 y(D)f Fs(!)e Fr(D)938 2291 y Fj(i)952 2285 y Ft([)p Fs(?)f Ft(:=)i Fs(9)1086 2268 y Fl(\003)1105 2285 y Fr(y)q(G)p Ft(])p Fr(;)460 b Ft(\(1\))730 2347 y Fs(`)755 2353 y Fi(int)804 2347 y Fr(G)p Ft([)p Fs(?)10 b Ft(:=)h Fs(9)970 2330 y Fl(\003)989 2347 y Fr(y)q(G)p Ft(])h Fs(!)f(9)1143 2330 y Fl(\003)1162 2347 y Fr(y)q(G)p Ft(;)415 b(\(2\))p 257 2386 573 2 v 304 2413 a Fh(1)321 2424 y Fn(Notice)16 b(our)f(sligh)o(tly)g(un)o (usual)f(form)o(ula)h(notation:)23 b(the)15 b(scop)q(e)g(of)i(a)f(quan) o(ti\014er)e(follo)o(w)o(ed)h(b)o(y)h(a)257 2464 y(dot)d(extends)f(as)h (far)g(as)h(the)f(surrounding)d(paren)o(theses)h(allo)o(w.)21 b(Otherwise)13 b(w)o(e)h(follo)o(w)f(the)g(standard)257 2503 y(con)o(v)o(en)o(tion)c(that)h(quan)o(ti\014ers)f(bind)h(stronger) g(than)g Fv(^)p Fn(,)h(whic)o(h)g(binds)f(stronger)g(than)g Fv(!)p Fn(.)963 2628 y Ft(2)p eop %%Page: 3 3 3 2 bop 257 262 a Ft(here)16 b Fs(`)373 268 y Fi(int)424 262 y Ft(means)d(deriv)n(abilit)o(y)f(in)i(in)o(tuitionistic)e (arithmetic,)h(i.e.)g(with)h(the)g(additional)257 311 y(axioms)j Fk(efq)454 321 y Fj(A)486 311 y Ft(:)e Fs(?)j(!)h Fr(A)p Ft(.)32 b(The)18 b(substitution)h Fs(?)f(7!)h(9)1160 296 y Fl(\003)1179 311 y Fr(y)q(G)g Ft(turns)g(the)g(axioms)e(ab)q(o)o (v)o(e)257 361 y(\(except)j Fk(efq)460 371 y Fj(A)487 361 y Ft(\))e(in)o(to)f(instances)i(of)e(the)i(same)d(sc)o(heme)i(with) g(di\013eren)o(t)h(form)o(ulas,)d(and)257 416 y(hence)f(from)c(our)i (giv)o(en)f(deriv)n(ation)g(\(in)h(minim)o(al)c(logic\))j(of)1232 405 y Fr(~)1226 416 y(D)h Fs(!)e(8)p Fr(y)q Ft(\()p Fr(G)h Fs(!)f(?)p Ft(\))g Fs(!)g(?)h Ft(w)o(e)257 466 y(obtain)446 557 y Fs(`)471 563 y Fi(int)526 546 y Fr(~)519 557 y(D)r Ft([)p Fs(?)e Ft(:=)i Fs(9)689 539 y Fl(\003)708 557 y Fr(y)q(G)p Ft(])f Fs(!)g(8)p Fr(y)q Ft(\()p Fr(G)p Ft([)p Fs(?)g Ft(:=)h Fs(9)1066 539 y Fl(\003)1085 557 y Fr(y)q(G)p Ft(])f Fs(!)g(9)1238 539 y Fl(\003)1258 557 y Fr(y)q(G)p Ft(\))h Fs(!)f(9)1416 539 y Fl(\003)1435 557 y Fr(y)q(G:)257 652 y Ft(No)o(w)j(\(1\))g(allo)o(ws)e(to)h(drop)h (the)g(substitution)g(in)1046 642 y Fr(~)1039 652 y(D)r Ft(,)f(and)g(b)o(y)h(\(2\))g(the)g(second)g(premise)g(is)257 702 y(deriv)n(able.)k(Hence)d(w)o(e)g(obtain)e(as)h(desired)833 793 y Fs(`)858 799 y Fi(int)913 783 y Fr(~)906 793 y(D)f Fs(!)e(9)1029 776 y Fl(\003)1048 793 y Fr(y)q(G:)257 884 y Ft(A)k(main)e(con)o(tribution)i(of)f(the)i(presen)o(t)g(pap)q(er) g(is)e(the)i(iden)o(ti\014cation)e(of)g(classes)j(of)d(for-)257 934 y(m)o(ulas)c({)h(to)g(b)q(e)h(called)g Fq(de\014nite)j Ft(and)c Fq(go)n(al)16 b Ft(form)o(ulas)9 b({)i(suc)o(h)h(that)g(sligh) o(t)f(generalizations)257 984 y(of)17 b(\(1\))d(and)f(\(2\))h(hold.)k (This)c(will)e(b)q(e)i(done)h(in)e(section)i(3.)320 1033 y(W)m(e)f(will)g(also)h(giv)o(e)f(\(in)h(section)h(5\))f(an)g(explicit) g(and)g(useful)g(represen)o(tation)i(of)e(the)257 1083 y(program)8 b(term)h(extracted)i(\(b)o(y)e(the)i(w)o(ell-kno)o(wn)d(mo) q(di\014ed)g(realizabilit)o(y)g(in)o(terpretation,)257 1138 y(cf.)16 b([18)o(]\))g(from)f(the)i(deriv)n(ation)e Fr(M)21 b Ft(of)903 1127 y Fr(~)896 1138 y(D)c Fs(!)e(9)1027 1123 y Fl(\003)1046 1138 y Fr(y)q(G)i Ft(just)g(constructed.)27 b(The)17 b(program)257 1188 y(term)d(has)g(the)h(form)d Fr(pt)637 1194 y Fm(1)662 1188 y Fr(:)7 b(:)g(:)f(t)733 1194 y Fj(n)755 1188 y Fr(s)p Ft(,)14 b(where)h Fr(p)f Ft(is)g(extracted)i(from)c Fr(M)19 b Ft(and)14 b Fr(t)1434 1194 y Fm(1)1452 1188 y Fr(;)7 b(:)g(:)g(:)e(;)i(t)1560 1194 y Fj(n)1582 1188 y Fr(;)g(s)14 b Ft(are)257 1238 y(determined)g(b)o(y)g(the)g(form)o(ulas)779 1227 y Fr(~)772 1238 y(D)h Ft(and)f Fr(G)g Ft(only)m(.)320 1287 y(Since)19 b(the)h(constructiv)o(e)h(existen)o(tial)e(quan)o(ti\014er)g Fs(9)1168 1272 y Fl(\003)1206 1287 y Ft(only)f(en)o(ters)j(our)e(deriv) n(ation)257 1337 y(in)c(the)i(con)o(text)f Fs(9)553 1322 y Fl(\003)572 1337 y Fr(y)q(G)p Ft(,)g(it)f(is)g(easiest)i(to)e (replace)i(this)e(form)o(ula)e(ev)o(erywhere)18 b(b)o(y)d(a)g(new)257 1387 y(prop)q(ositional)9 b(sym)o(b)q(ol)g Fr(X)14 b Ft(and)c(stipulate)h(that)f(a)g(term)g Fr(r)h Ft(realizes)g Fr(X)j Ft(i\013)c Fr(G)p Ft([)p Fr(y)j Ft(:=)e Fr(r)q Ft(].)17 b(This)257 1437 y(allo)o(ws)e(for)g(a)g(short)h(and)f (self-con)o(tained)h(exp)q(osition)f({)g(in)g(section)h(4)f({)h(of)f (all)f(w)o(e)h(need)257 1487 y(ab)q(out)g(mo)q(di\014ed)f(realizabilit) o(y)m(,)f(including)h(the)h(soundness)i(theorem.)k(In)15 b(section)g(5)g(w)o(e)257 1536 y(then)g(pro)o(v)o(e)f(our)g(main)e (theorem)h(ab)q(out)h(program)e(extraction)i(from)f(classical)g(pro)q (ofs.)320 1586 y(The)j(\014nal)f(section)h(6)f(then)i(con)o(tains)e (some)g(examples)g(of)g(our)h(general)g(mac)o(hinery)m(.)257 1636 y(F)m(rom)11 b(a)h(classical)h(pro)q(of)f(of)g(the)h(existence)h (of)e(the)i Fp(Fibona)o(cci)d Ft(n)o(um)o(b)q(ers)h(w)o(e)h(extract)h (in)257 1686 y(6.1)g(a)g(short)h(and)f(surprisingly)g(e\016cien)o(t)h (program,)d(where)j Fr(\025)p Ft(-expressions)h(rather)f(than)257 1736 y(pairs)h(are)h(passed.)25 b(In)16 b(6.2)f(w)o(e)h(treat)h(as)f(a) g(further)h(example)d(a)i(classical)g(pro)q(of)f(of)h(the)257 1786 y(w)o(ellfoundedness)d(of)f Fr(<)h Ft(on)f Fg(N)p Ft(.)j(Finally)c(in)h(6.3)f(w)o(e)h(tak)o(e)h(up)f(a)g(suggestion)h(of) h Fp(Veldman)257 1835 y Ft(and)19 b Fp(Bezem)g Ft([19)o(])g(and)f (presen)o(t)j(a)e(short)g(classical)g(pro)q(of)f(of)h(\(the)g(general)h (form)d(of)s(\))257 1885 y Fp(Dickson)p Ft('s)e(Lemma,)c(as)j(an)f(in)o (teresting)i(candidate)f(for)f(further)i(study)m(.)257 2022 y Fu(2)67 b(Arithmetic)25 b(for)d(F)-6 b(unctionals)257 2113 y Ft(The)20 b(system)f(w)o(e)g(consider)h(is)f(essen)o(tially)g (\(the)h(negativ)o(e)f(fragmen)o(t)f(of)s(\))h Fp(Heyting)p Ft('s)257 2163 y(in)o(tuitionistic)d(arithmetic)g(in)g(\014nite)h(t)o (yp)q(es)h(as)f(describ)q(ed)h(e.g.)e(in)h([8)o(].)27 b(It)16 b(is)h(based)h(on)257 2213 y Fp(G)294 2210 y(\177)292 2213 y(odel)p Ft('s)i(system)f Fr(T)25 b Ft(and)18 b(just)h(adds)g(the) h(corresp)q(onding)g(logical)d(and)h(arithmetical)257 2263 y(apparatus)e(to)g(it.)24 b(Equations)16 b(are)g(treated)h(on)f (the)g(meta)f(lev)o(el)h(b)o(y)f(iden)o(tifying)g(terms)257 2313 y(with)f(the)g(same)f(normal)f(form.)320 2362 y Fq(T)m(yp)n(es)18 b Ft(are)e(built)f(from)e(ground)i(t)o(yp)q(es)i Fr(\023)e Ft(for)g(the)h(natural)f(n)o(um)o(b)q(ers)g(and)g Fk(o)g Ft(for)g(the)257 2412 y(b)q(o)q(olean)d(ob)r(jects)h(\(and)f(p)q (ossibly)f(other)i(ground)f(t)o(yp)q(es\))h(b)o(y)e Fr(\032)h Fs(!)f Fr(\033)q Ft(.)18 b(The)12 b Fq(c)n(onstants)k Ft(are)665 2503 y Fk(true)734 2486 y Fi(o)752 2503 y Fr(;)i Fk(false)859 2485 y Fi(o)876 2503 y Fr(;)g Ft(0)927 2486 y Fj(\023)941 2503 y Fr(;)g Ft(S)994 2486 y Fj(\023)p Fl(!)p Fj(\023)1054 2503 y Fr(;)g Fs(R)1119 2509 y Fi(o)p Fj(;\032)1164 2503 y Fr(;)g Fs(R)1229 2509 y Fj(\023;\032)1270 2503 y Fr(:)963 2628 y Ft(3)p eop %%Page: 4 4 4 3 bop 257 262 a Fs(R)292 268 y Fj(\023;\032)352 262 y Ft(is)17 b(the)h Fq(primitive)g(r)n(e)n(cursion)f(op)n(er)n(ator)22 b Ft(of)17 b(t)o(yp)q(e)h Fr(\032)g Fs(!)g Ft(\()p Fr(\023)f Fs(!)h Fr(\032)g Fs(!)f Fr(\032)p Ft(\))i Fs(!)e Fr(\023)h Fs(!)f Fr(\032)257 311 y Ft(and)i Fs(R)378 317 y Fi(o)p Fj(;\032)441 311 y Ft(is)f(the)i(recursion)f(op)q(erator)g(for)f(the)i (t)o(yp)q(e)f Fk(o)f Ft(of)g(b)q(o)q(oleans,)h(i.e.)f(is)g(of)g(t)o(yp) q(e)257 361 y Fr(\032)12 b Fs(!)f Fr(\032)h Fs(!)f Fk(o)h Fs(!)f Fr(\032)j Ft(and)g(represen)o(ts)i(de\014nition)e(b)o(y)f (cases.)20 b Fq(T)m(erms)c Ft(are)684 451 y Fr(x)708 434 y Fj(\032)727 451 y Fr(;)i(c)775 434 y Fj(\032)808 451 y Ft(\()p Fr(c)842 436 y Fj(\032)875 451 y Ft(a)13 b(constan)o(t\))q Fr(;)18 b(\025x)1157 434 y Fj(\032)1176 451 y Fr(r)o(;)g(r)q(s)257 540 y Ft(with)g(the)g(usual)f(t)o(yping)g (rules.)30 b(The)19 b Fq(c)n(onversions)i Ft(are)d(those)h(for)e(the)h (simply)e(t)o(yp)q(ed)257 590 y(lam)o(b)q(da)10 b(calculus,)i(plus)g (some)f(new)h(ones)g(for)g(the)g(recursion)h(op)q(erators.)19 b(W)m(e)11 b(write)h Fr(t)5 b Ft(+)g(1)257 640 y(for)14 b(S)344 625 y Fj(\023)p Fl(!)p Fj(\023)404 640 y Fr(t)p Ft(.)708 729 y Fs(R)743 735 y Fi(o)p Fj(;\032)788 729 y Fr(r)q(s)7 b Fk(true)54 b Fs(7!)998 735 y Fl(R)1081 729 y Fr(r)700 792 y Fs(R)735 798 y Fi(o)p Fj(;\032)780 792 y Fr(r)q(s)7 b Fk(false)53 b Fs(7!)998 798 y Fl(R)1081 792 y Fr(s)766 854 y Fs(R)801 860 y Fj(\023;\032)843 854 y Fr(r)q(s)p Ft(0)g Fs(7!)998 860 y Fl(R)1081 854 y Fr(r)668 916 y Fs(R)703 922 y Fj(\023;\032)745 916 y Fr(r)q(s)p Ft(\()p Fr(t)9 b Ft(+)h(1\))53 b Fs(7!)998 922 y Fl(R)1081 916 y Fr(st)p Ft(\()p Fs(R)1166 922 y Fj(\023;\032)1208 916 y Fr(r)q(st)p Ft(\))257 1006 y(It)10 b(is)g(w)o(ell)e(kno)o(wn)i(that)f(for)h(this)f(system)h(of)f(terms)g (ev)o(ery)i(term)e(strongly)g(normalizes,)g(and)257 1055 y(that)14 b(the)g(normal)e(form)g(is)h(uniquely)h(determined;)f(hence)i (the)f(relation)f Fr(r)g Ft(=)1497 1061 y Fj(\014)q Fl(R)1560 1055 y Fr(s)h Ft(is)f(de-)257 1105 y(cidable)g(\(b)o(y)g(normalizing)e Fr(r)i Ft(and)g Fr(s)p Ft(\).)19 b(By)13 b(iden)o(tifying)f(=)1176 1111 y Fj(\014)q Fl(R)1227 1105 y Ft(-equal)g(terms)h(\(i.e.)f (treating)257 1155 y(equations)i(on)g(the)g(meta)f(lev)o(el\))h(w)o(e)g (can)g(greatly)g(simplify)d(man)o(y)h(formal)f(deriv)n(ations.)320 1205 y(Let)k Fk(atom)e Ft(b)q(e)i(a)f(unary)g(predicate)i(sym)o(b)q(ol) c(taking)i(one)h(argumen)o(t)e(of)h(t)o(yp)q(e)h Fk(o)p Ft(.)k(The)257 1255 y(in)o(tended)d(in)o(terpretation)g(of)f Fk(atom)f Ft(is)i(the)g(set)g Fs(f)p Fk(true)q Fs(g)p Ft(;)g(hence)h(\\)p Fk(atom)n Ft(\()p Fr(t)p Ft(\)")f(means)e(\\)p Fr(t)g Ft(=)257 1304 y Fk(true)q Ft(".)26 b(W)m(e)16 b(also)f(allo)o(w)g(the)i(prop)q(ositional)e(sym)o(b)q(ols)g Fs(?)h Ft(and)g Fr(X)k Ft(\(i.e.)15 b(0-ary)h(predicate)257 1354 y(sym)o(b)q(ols\).)h(So)d Fq(formulas)i Ft(are)388 1444 y Fs(?)p Fr(;)h(X)q(;)f Fk(atom)o Ft(\()p Fr(t)633 1427 y Fi(o)651 1444 y Ft(\))p Fr(;)i(A)11 b Fs(!)h Fr(B)r(;)18 b Fs(8)p Fr(x)903 1427 y Fj(\032)922 1444 y Fr(A)p Ft(;)48 b(abbreviation:)41 b Fs(:)p Fr(A)11 b Ft(:=)g Fr(A)h Fs(!)f(?)p Fr(:)257 1533 y Ft(As)h Fq(axioms)i Ft(w)o(e)e(tak)o(e)f (the)g(induction)g(sc)o(hemes)g Fk(Ind)1061 1539 y Fj(n;A)1129 1533 y Ft(and)g Fk(Ind)1261 1539 y Fj(p;A)1326 1533 y Ft(for)g(the)h(ground)f(t)o(yp)q(es)257 1583 y Fr(\023)j Ft(and)g Fk(o)p Ft(,)f(and)h(in)f(addition)g(the)i(\\truth)f(axiom")d Fk(ax)1090 1589 y Fi(true)1158 1583 y Ft(and)j(t)o(w)o(o)f(sc)o(hemes)i Fk(ax)1515 1589 y Fi(false)o Fj(;A)1623 1583 y Ft(and)257 1633 y Fk(efq)310 1643 y Fj(A)354 1633 y Ft(for)i(\\ex-falso-quo)q (dlib)q(et",)f(one)i(for)f(eac)o(h)h(of)e(the)i(t)o(w)o(o)f(p)q (ossibilities)g Fk(atom)n Ft(\()p Fk(false)p Ft(\))257 1683 y(and)d Fs(?)f Ft(to)g(express)i(falsit)o(y)e(\(see)i(in)o(tro)q (duction\).)i(Note)d(that)g(ev)o(ery)g(instance)h Fs(?)10 b(!)h Fr(A)j Ft(of)257 1733 y(ex-falso-quo)q(dlib)q(et)h(is)g(deriv)n (able)h(from)e Fs(?)f(!)h Fr(X)20 b Ft(and)15 b Fs(?)f(!)g Fk(atom)o Ft(\()p Fk(false)p Ft(\);)i(this)g(will)e(b)q(e)257 1782 y(useful)h(in)f(section)i(4)e(\(when)i(w)o(e)f(de\014ne)g(the)h (extracted)g(program)d([)-7 b([)p Fr(M)5 b Ft(])-7 b(])13 b(of)h(a)g(deriv)n(ation)257 1832 y Fr(M)5 b Ft(\).)320 1882 y Fq(Derivations)14 b Ft(are)e(within)f(minim)o(al)d(logic.)16 b(They)c(are)g(written)g(in)f(natural)g(deduction)257 1932 y(st)o(yle,)g(i.e.)e(as)h(t)o(yp)q(ed)h Fr(\025)p Ft(-terms)f(via)f(the)i(w)o(ell-kno)o(wn)e Fp(Curr)m(y)q Ft(-)p Fp(Ho)o(w)l(ard)i Ft(corresp)q(ondence:)647 2021 y Fr(u)671 2004 y Fj(B)741 2021 y Ft(\(assumptions\))o Fr(;)48 b Ft(axioms)n Fr(;)647 2090 y Ft(\()p Fr(\025u)711 2073 y Fj(A)738 2090 y Fr(M)783 2073 y Fj(B)812 2090 y Ft(\))828 2073 y Fj(A)p Fl(!)p Fj(B)914 2090 y Fr(;)g Ft(\()p Fr(M)1035 2073 y Fj(A)p Fl(!)p Fj(B)1122 2090 y Fr(N)1160 2073 y Fj(A)1187 2090 y Ft(\))1203 2073 y Fj(B)1232 2090 y Fr(;)647 2160 y Ft(\()p Fr(\025x)711 2143 y Fj(\032)730 2160 y Fr(M)775 2143 y Fj(A)802 2160 y Ft(\))818 2143 y Fl(8)p Fj(x)857 2131 y Ff(\032)873 2143 y Fj(A)900 2160 y Fr(;)g Ft(\()p Fr(M)1021 2143 y Fl(8)p Fj(x)1060 2131 y Ff(\032)1076 2143 y Fj(A)1103 2160 y Fr(t)1118 2143 y Fj(\032)1137 2160 y Ft(\))1153 2143 y Fj(A)p Fm([)p Fj(x)1206 2131 y Ff(\032)1224 2143 y Fm(:=)p Fj(t)1271 2131 y Ff(\032)1288 2143 y Fm(])257 2254 y Ft(where)19 b(in)f(the)g Fs(8)p Ft(-in)o(tro)q(duction)f Fr(\025xM)880 2239 y Fj(A)907 2254 y Ft(,)h Fr(x)g Ft(m)o(ust)f(not)g (b)q(e)i(free)f(in)f(an)o(y)h Fr(B)i Ft(with)d Fr(u)1615 2239 y Fj(B)1662 2254 y Fs(2)257 2304 y Fk(F)m(A)o Ft(\()p Fr(M)5 b Ft(\);)14 b(here)h Fk(F)m(A)o Ft(\()p Fr(M)5 b Ft(\))14 b(is)f(the)i(set)g(of)e(free)h(assumption)f(v)n(ariables)g (of)g Fr(M)5 b Ft(.)320 2354 y(Let)16 b Fr(Z)427 2339 y Fj(X)474 2354 y Ft(denote)h(this)f(system)f(of)h(in)o(tuitionistic)e (arithmetic;)h Fr(Z)k Ft(is)d(obtained)f(from)257 2403 y Fr(Z)288 2388 y Fj(X)340 2403 y Ft(b)o(y)k(omitting)e Fr(X)s Ft(.)36 b Fr(Z)690 2409 y Fm(0)729 2403 y Ft(\()p Fr(Z)776 2388 y Fj(X)773 2414 y Fm(0)808 2403 y Ft(,)21 b(resp.\))36 b(is)20 b Fr(Z)j Ft(\()p Fr(Z)1124 2388 y Fj(X)1156 2403 y Ft(,)d(resp.\))37 b(without)19 b(the)i(axioms)257 2453 y Fk(efq)310 2463 y Fj(A)337 2453 y Ft(.)28 b(F)m(or)17 b(ev)o(ery)h Fr(Z)596 2459 y Fm(0)615 2453 y Ft(-deriv)n(ation)e Fr(M)22 b Ft(let)17 b Fr(M)997 2438 y Fj(X)1045 2453 y Ft(denote)i(the)e Fr(Z)1288 2438 y Fj(X)1285 2464 y Fm(0)1320 2453 y Ft(-deriv)n(ation)f(resulting)257 2503 y(from)e Fr(M)20 b Ft(b)o(y)15 b(substituting)g Fr(X)k Ft(for)c Fs(?)p Ft(.)21 b(W)m(rite)15 b Fr(C)1042 2488 y Fj(X)1087 2503 y Ft(:=)e Fr(C)s Ft([)p Fs(?)g Ft(:=)g Fr(X)s Ft(].)22 b({)15 b Fs(L)p Ft([)p Fr(X)s Ft(])g(\()p Fs(L)p Ft(,)g(resp.\))963 2628 y(4)p eop %%Page: 5 5 5 4 bop 257 262 a Ft(denotes)18 b(the)f(language)f(of)g Fr(Z)741 246 y Fj(X)790 262 y Ft(\()p Fr(Z)s Ft(,)h(resp.\).)27 b(W)m(e)16 b(use)i Fr(P)k Ft(for)16 b(atomic)f Fs(L)p Ft(-form)o(ulas)f(and)257 311 y Fr(A;)7 b(B)r(;)g(C)q(;)g(D)q(;)g(G)12 b Ft(for)i Fs(L)p Ft([)p Fr(X)s Ft(]-form)o(ula)o(s.)i Fs(`)e Ft(denotes)h(deriv)n(abilit)o(y)d(in)i(minim)o(al)c(logic.)320 361 y(Note)j(that)g(in)g(our)g(setting)g(deriv)n(abilit)o(y)e(in)i Fr(Z)1060 346 y Fj(X)1105 361 y Ft(is)g(essen)o(tially)g(the)g(same)f (as)i(in)e Fr(Z)1646 346 y Fj(X)1643 371 y Fm(0)1678 361 y Ft(:)257 432 y Fe(Lemma)k(2.1.)21 b Fq(L)n(et)14 b Fr(F)j Ft(:=)12 b Fk(atom)n Ft(\()p Fk(false)p Ft(\))j Fq(and)h Fr(A)1017 417 y Fj(F)1056 432 y Ft(:=)c Fr(A)p Ft([)p Fs(?)e Ft(:=)h Fr(F)6 b Ft(])p Fq(.)18 b(Then)741 509 y Fr(Z)772 492 y Fj(X)816 509 y Fs(`)11 b Fr(A)33 b Fs(\()-7 b(\))31 b Fr(Z)1055 492 y Fj(X)1052 519 y Fm(0)1099 509 y Fs(`)11 b Fr(A)1166 492 y Fj(F)1194 509 y Fr(:)257 585 y Fq(Pr)n(o)n(of.)20 b Fs(\))14 b Ft(holds)f(since)i Fk(efq)706 567 y Fj(F)706 596 y(A)747 585 y Ft(is)f Fk(ax)828 594 y Fi(false)o Fj(;A)920 585 y Ff(F)8 b Ft(.)320 635 y Fs(\()p Ft(.)17 b(W)m(e)12 b(ha)o(v)o(e)h Fr(Z)587 620 y Fj(X)631 635 y Fs(`)f(?)e($)h Fr(F)19 b Ft(b)o(y)13 b Fk(efq)919 645 y Fj(F)960 635 y Ft(and)g Fk(ax)1079 641 y Fi(false)o Fj(;)p Fl(?)1174 635 y Ft(.)18 b(This)12 b(implies)g(the)h(claim.)p 1672 610 18 2 v 1672 634 2 24 v 1688 634 V 1672 636 18 2 v 320 715 a(Since)h(our)f(form)o(ulas)f (do)h(not)h(con)o(tain)f(the)h(constructiv)o(e)h(existen)o(tial)e(quan) o(ti\014er)h Fs(9)1659 700 y Fl(\003)1678 715 y Ft(,)257 765 y(w)o(e)d(can)g(deriv)o(e)g(stabilit)o(y)f(for)g(all)g Fs(L)p Ft(-form)o(ulas.)k(Hence)e(classical)f(arithmetic)e(\(in)i(all)e (\014nite)257 815 y(t)o(yp)q(es\))15 b(is)f(a)g(subsystem)g(of)f(our)h (presen)o(t)h(system)f Fr(Z)s Ft(:)257 886 y Fe(Lemma)i(2.2.)21 b Fq(\(Stability\).)d Fr(Z)d Fs(`)d(::)p Fr(A)f Fs(!)g Fr(A)k Fq(for)f(every)h Fs(L)p Fq(-formula)f Fr(A)p Fq(.)257 957 y(Pr)n(o)n(of.)20 b Ft(Induction)14 b(on)g Fr(A)p Ft(.)320 1007 y Fq(Case)g Fk(atom)o Ft(\()p Fr(t)p Ft(\).)k(W)m(e)11 b(ha)o(v)o(e)g Fr(Z)k Fs(`)d(8)p Fr(p:)p Fs(::)p Fk(atom)m Ft(\()p Fr(p)p Ft(\))g Fs(!)f Fk(atom)o Ft(\()p Fr(p)p Ft(\))h(b)o(y)f(b)q(o)q(olean)g(induction,)257 1057 y(again)i(using)h Fr(Z)h Fs(`)c(?)g($)g Fr(F)20 b Ft(and)13 b(the)i(truth)f(axiom)e Fk(ax)1123 1063 y Fi(true)1181 1057 y Ft(:)h Fk(atom)o Ft(\()p Fk(true)q Ft(\).)320 1107 y Fq(Case)k Fs(?)p Ft(.)g(Ob)o(viously)c Fr(Z)i Fs(`)d(::?)e(!)h(?)p Ft(.)320 1157 y Fq(Case)17 b Fr(A)11 b Fs(!)g Fr(B)r Ft(.)19 b(By)14 b(induction)f(h)o(yp)q(othesis)i(for)f Fr(B)r Ft(:)319 1495 y Fr(u)5 b Ft(:)13 b Fs(::)p Fr(B)g Fs(!)e Fr(B)653 1385 y(v)6 b Ft(:)13 b Fs(::)p Ft(\()p Fr(A)f Fs(!)f Fr(B)r Ft(\))1014 1277 y Fr(u)1038 1283 y Fm(1)1061 1277 y Ft(:)j Fs(:)p Fr(B)1241 1224 y(u)1265 1230 y Fm(2)1288 1224 y Ft(:)g Fr(A)d Fs(!)g Fr(B)96 b(w)6 b Ft(:)13 b Fr(A)p 1225 1240 421 2 v 1418 1277 a(B)p 998 1293 471 2 v 1217 1330 a(F)p 1122 1340 223 2 v 1357 1352 a Fs(!)1399 1337 y Fm(+)1426 1352 y Fr(u)1450 1358 y Fm(2)1138 1385 y Fs(:)p Ft(\()p Fr(A)f Fs(!)f Fr(B)r Ft(\))p 636 1406 709 2 v 974 1442 a Fr(F)p 929 1452 123 2 v 1064 1465 a Fs(!)1106 1450 y Fm(+)1133 1465 y Fr(u)1157 1471 y Fm(1)946 1495 y Fs(::)p Fr(B)p 302 1505 750 2 v 660 1542 a(B)320 1604 y Fq(Case)17 b Fs(8)p Fr(xA)p Ft(.)g(Clearly)d(it)f (su\016ces)i(to)f(sho)o(w)g Fr(Z)h Fs(`)d Ft(\()p Fs(::)p Fr(A)f Fs(!)g Fr(A)p Ft(\))h Fs(!)f(::8)p Fr(xA)g Fs(!)g Fr(A)p Ft(:)424 1933 y Fr(u)5 b Ft(:)13 b Fs(::)p Fr(A)e Fs(!)g Fr(A)753 1833 y(v)6 b Ft(:)14 b Fs(::8)p Fr(xA)1031 1727 y(u)1055 1733 y Fm(1)1078 1727 y Ft(:)g Fs(:)p Fr(A)1256 1674 y(u)1280 1680 y Fm(2)1303 1674 y Ft(:)f Fs(8)p Fr(xA)93 b(x)p 1239 1690 301 2 v 1374 1727 a(A)p 1015 1743 407 2 v 1202 1780 a(F)p 1149 1790 139 2 v 1300 1802 a Fs(!)1342 1787 y Fm(+)1369 1802 y Fr(u)1393 1808 y Fm(2)1165 1833 y Fs(:8)p Fr(xA)p 737 1843 551 2 v 996 1880 a(F)p 952 1890 120 2 v 1084 1902 a Fs(!)1126 1887 y Fm(+)1153 1902 y Fr(u)1177 1908 y Fm(1)969 1933 y Fs(::)p Fr(A)p 407 1942 665 2 v 724 1979 a(A)257 2039 y Ft(This)14 b(concludes)h(the)g (pro)q(of.)p 1672 2014 18 2 v 1672 2037 2 24 v 1688 2037 V 1672 2039 18 2 v 257 2119 a Fe(Lemma)h(2.3.)21 b Fq(\(Cases\).)d Fr(Z)722 2104 y Fj(X)766 2119 y Fs(`)12 b Ft(\()p Fs(:)p Fr(C)i Fs(!)d Fr(A)p Ft(\))g Fs(!)g Ft(\()p Fr(C)k Fs(!)c Fr(A)p Ft(\))h Fs(!)f Fr(A)k Fq(for)f(every)g(quanti\014er-)257 2169 y(fr)n(e)n(e)g Fs(L)p Fq(-formula)g Fr(C)s Fq(.)257 2240 y(Pr)n(o)n(of.)20 b Ft(W)m(e)13 b(ma)o(y)e(assume)h(that)h Fs(?)f Ft(do)q(es)h(not)g(o)q(ccur)h(in)e Fr(C)s Ft(,)g(since)i Fr(Z)g Fs(`)e(?)f($)g Fk(atom)o Ft(\()p Fk(false)p Ft(\).)257 2290 y(Note)19 b(that)g(for)f(ev)o(ery)h(suc)o(h)g(quan)o (ti\014er-free)g(form)o(ula)d Fr(C)21 b Ft(w)o(e)e(can)g(easily)f (construct)i(a)257 2340 y(b)q(o)q(olean)14 b(term)f Fr(t)526 2346 y Fj(C)568 2340 y Ft(suc)o(h)i(that)e Fr(Z)779 2346 y Fm(0)810 2340 y Fs(`)f Fk(atom)o Ft(\()p Fr(t)967 2346 y Fj(C)995 2340 y Ft(\))f Fs($)g Fr(C)s Ft(.)18 b(Hence)d(it)f (su\016ces)h(to)f(deriv)o(e)443 2416 y Fs(8)p Fr(p:)p Ft(\(\()p Fk(atom)n Ft(\()p Fr(p)p Ft(\))e Fs(!)f Fk(atom)n Ft(\()p Fk(false)p Ft(\)\))h Fs(!)f Fr(A)p Ft(\))h Fs(!)f Ft(\()p Fk(atom)o Ft(\()p Fr(p)p Ft(\))h Fs(!)f Fr(A)p Ft(\))h Fs(!)f Fr(A:)257 2493 y Ft(This)j(is)g(done)g(b)o(y)g (induction)f(on)h Fr(p)p Ft(,)f(using)h(the)g(truth)h(axiom)c Fk(ax)1290 2499 y Fi(true)1348 2493 y Ft(:)j Fk(atom)n Ft(\()p Fk(true)q Ft(\).)p 1672 2468 V 1672 2491 2 24 v 1688 2491 V 1672 2493 18 2 v 963 2628 a(5)p eop %%Page: 6 6 6 5 bop 257 262 a Fu(3)67 b(De\014nite)23 b(and)g(Goal)f(F)-6 b(orm)n(ulas)257 352 y Ft(A)14 b(form)o(ula)d(is)i Fq(r)n(elevant)k Ft(if)c(it)g(\\ends")h(with)f Fs(?)p Ft(.)k(More)d(precisely)m(,)f (relev)n(an)o(t)h(form)o(ulas)d(are)257 402 y(de\014ned)k(inductiv)o (ely)f(b)o(y)f(the)i(clauses)320 485 y Fs(\017)20 b(?)13 b Ft(is)h(relev)n(an)o(t,)320 568 y Fs(\017)20 b Ft(if)13 b Fr(C)k Ft(is)c(relev)n(an)o(t)h(and)g Fr(B)i Ft(is)e(arbitrary)m(,)f (then)i Fr(B)f Fs(!)d Fr(C)16 b Ft(is)e(relev)n(an)o(t,)f(and)320 651 y Fs(\017)20 b Ft(if)13 b Fr(C)k Ft(is)c(relev)n(an)o(t,)h(then)g Fs(8)p Fr(xC)j Ft(is)c(relev)n(an)o(t.)257 734 y(A)h(form)o(ula)e(whic) o(h)h(is)h(not)g(relev)n(an)o(t)g(is)g(called)f Fq(irr)n(elevant)t Ft(.)320 784 y(W)m(e)i(de\014ne)h Fq(go)n(al)g(formulas)i Fr(G)d Ft(and)g Fq(de\014nite)i(formulas)h Fr(D)f Ft(inductiv)o(ely)m (.)k(These)c(no-)257 834 y(tions)12 b(are)g(related)h(to)f(similar)d (ones)k(common)c(under)j(the)h(same)e(name)g(in)g(the)h(con)o(text)h (of)257 884 y(extensions)j(of)d(logic)g(programming)o(.)j(Recall)d (that)i Fr(P)k Ft(ranges)c(o)o(v)o(er)f(atomic)e Fs(L)p Ft(-form)o(ulas)257 934 y(\(including)h Fs(?)p Ft(\).)400 1025 y Fr(G)35 b Ft(:=)f Fr(P)17 b Fs(j)11 b Fr(D)i Fs(!)e Fr(G)41 b Ft(pro)o(vided)14 b Fr(D)h Ft(irrelev)n(an)o(t)f Fs(\))f Fr(D)j Ft(quan)o(ti\014er-free)590 1087 y Fs(j)11 b(8)p Fr(xG)94 b Ft(pro)o(vided)14 b Fr(G)f Ft(irrelev)n(an)o(t,)397 1174 y Fr(D)37 b Ft(:=)d Fr(P)17 b Fs(j)11 b Fr(G)g Fs(!)g Fr(D)43 b Ft(pro)o(vided)14 b Fr(D)h Ft(irrelev)n(an)o(t)f Fs(\))f Fr(G)h Ft(irrelev)n(an)o(t)590 1237 y Fs(j)d(8)p Fr(xD)q(:)257 1328 y Fe(Lemma)16 b(3.1.)21 b Fq(F)m(or)14 b(de\014nite)i(formulas)e Fr(D)i Fq(and)g(go)n(al)f(formulas)f Fr(G)h Fq(we)f(have)544 1419 y Fr(Z)575 1402 y Fj(X)618 1419 y Fs(`)e Ft(\()p Fs(:)p Fr(D)h Fs(!)e Fr(X)s Ft(\))h Fs(!)f Fr(D)952 1402 y Fj(X)1105 1419 y Fq(for)j Fr(D)i Fq(r)n(elevant,)260 b Ft(\(3\))544 1488 y Fr(Z)575 1471 y Fj(X)618 1488 y Fs(`)12 b Fr(D)h Fs(!)e Fr(D)790 1471 y Fj(X)822 1488 y Fr(;)802 b Ft(\(4\))544 1556 y Fr(Z)575 1539 y Fj(X)618 1556 y Fs(`)12 b Fr(G)688 1539 y Fj(X)731 1556 y Fs(!)f Fr(G)288 b Fq(for)14 b Fr(G)h Fq(irr)n(elevant,)231 b Ft(\(5\))544 1625 y Fr(Z)575 1608 y Fj(X)618 1625 y Fs(`)12 b Fr(G)688 1608 y Fj(X)731 1625 y Fs(!)f Ft(\()p Fr(G)g Fs(!)g Fr(X)s Ft(\))h Fs(!)f Fr(X)q(:)574 b Ft(\(6\))257 1716 y Fq(Pr)n(o)n(of.)20 b Ft(Sim)o(ultaneous)12 b(induction)i(on)g (form)o(ulas.)320 1766 y(\(3\).)j(Let)d Fr(D)h Ft(b)q(e)f(relev)n(an)o (t.)k Fq(Case)e Fs(?)p Ft(.)h(Clearly)c(\(\()p Fs(?)e(!)g(?)p Ft(\))g Fs(!)g Fr(X)s Ft(\))h Fs(!)f Fr(X)17 b Ft(is)c(deriv)n(able.) 320 1816 y Fq(Case)k Fr(G)11 b Fs(!)g Fr(D)q Ft(.)429 2174 y Fs(j)293 2240 y Ft(\()p Fs(:)p Fr(D)q Fs(!)p Fr(X)s Ft(\))p Fs(!)p Fr(D)544 2225 y Fj(X)773 2011 y Fs(j)615 2077 y Fr(G)648 2062 y Fj(X)679 2077 y Fs(!)o Ft(\()p Fr(G)p Fs(!)p Fr(X)s Ft(\))p Fs(!)p Fr(X)42 b(G)1015 2062 y Fj(X)p 611 2097 440 2 v 696 2137 a Ft(\()p Fr(G)11 b Fs(!)g Fr(X)s Ft(\))h Fs(!)f Fr(X)1084 2033 y Fs(:)p Ft(\()p Fr(G)p Fs(!)o Fr(D)q Ft(\))p Fs(!)q Fr(X)1372 1937 y Fs(:)p Fr(D)1473 1890 y(G)p Fs(!)o Fr(D)40 b(G)p 1469 1900 189 2 v 1546 1937 a(D)p 1367 1946 218 2 v 1460 1984 a Fs(?)p 1376 1994 201 2 v 1380 2033 a(:)p Ft(\()p Fr(G)11 b Fs(!)g Fr(D)q Ft(\))p 1080 2053 497 2 v 1310 2090 a Fr(X)p 1257 2100 144 2 v 1261 2137 a(G)g Fs(!)g Fr(X)p 692 2157 709 2 v 1027 2194 a(X)p 959 2204 174 2 v 963 2240 a Fs(:)p Fr(D)i Fs(!)e Fr(X)p 289 2261 844 2 v 677 2304 a(D)712 2289 y Fj(X)p 413 2314 596 2 v 417 2357 a Ft(\()p Fs(:)p Ft(\()p Fr(G)g Fs(!)g Fr(D)q Ft(\))h Fs(!)f Fr(X)s Ft(\))i Fs(!)e Fr(G)842 2342 y Fj(X)885 2357 y Fs(!)g Fr(D)973 2342 y Fj(X)257 2444 y Ft(Here)k(w)o(e)g(ha)o(v) o(e)e(used)i(the)g(induction)e(h)o(yp)q(otheses)j(\(3\))d(for)h Fr(D)h Ft(and)f(\(6\))g(for)f Fr(G)p Ft(.)963 2628 y(6)p eop %%Page: 7 7 7 6 bop 320 262 a Fq(Case)17 b Fs(8)p Fr(xD)q Ft(.)649 504 y Fs(j)490 570 y Ft(\()p Fs(:)p Fr(D)c Fs(!)e Fr(X)s Ft(\))h Fs(!)f Fr(D)787 555 y Fj(X)913 477 y Fs(:8)p Fr(xD)h Fs(!)f Fr(X)1218 383 y Fs(:)p Fr(D)1374 336 y Fs(8)p Fr(xD)p 1358 346 116 2 v 1398 383 a(D)p 1201 393 249 2 v 1310 430 a Fs(?)p 1254 440 144 2 v 1271 477 a(:8)p Fr(xD)p 896 487 502 2 v 1128 523 a(X)p 1047 533 199 2 v 1064 570 a Fs(:)p Fr(D)i Fs(!)e Fr(X)p 473 590 773 2 v 826 634 a(D)861 619 y Fj(X)p 786 644 148 2 v 803 687 a Fs(8)p Fr(xD)885 672 y Fj(X)p 632 697 457 2 v 648 740 a Ft(\()p Fs(:8)p Fr(xD)i Fs(!)e Fr(X)s Ft(\))h Fs(!)f(8)p Fr(xD)1039 725 y Fj(X)257 827 y Ft(Here)k(w)o(e)g(ha)o(v)o(e)e(used)i (the)g(induction)e(h)o(yp)q(othesis)i(\(3\))f(for)f Fr(D)q Ft(.)320 877 y(\(4\).)18 b Fq(Case)f Fr(D)e Ft(relev)n(an)o(t.)711 1036 y Fs(j)552 1102 y Ft(\()p Fs(:)p Fr(D)e Fs(!)e Fr(X)s Ft(\))i Fs(!)e Fr(D)850 1087 y Fj(X)975 1009 y Fs(?)g(!)g Fr(X)1203 961 y Fs(:)p Fr(D)94 b(D)p 1186 971 226 2 v 1282 1009 a Fs(?)p 958 1018 374 2 v 1126 1055 a Fr(X)p 1045 1065 199 2 v 1062 1102 a Fs(:)p Fr(D)13 b Fs(!)e Fr(X)p 536 1122 709 2 v 856 1165 a(D)891 1150 y Fj(X)p 790 1175 201 2 v 806 1219 a Fr(D)i Fs(!)e Fr(D)941 1203 y Fj(X)257 1295 y Ft(Here)k(w)o(e)g(ha)o(v)o(e)e(used)i(\(3\))f(and)g Fs(?)d(!)g Fr(X)s Ft(.)320 1345 y Fq(Case)21 b Fr(D)e Ft(irrelev)n(an)o(t.)30 b Fq(Sub)n(c)n(ase)22 b Fr(P)6 b Ft(.)29 b(Then)18 b Fr(P)1071 1330 y Fj(X)1120 1345 y Ft(=)h Fr(P)k Ft(and)18 b(the)g(claim)e(is)i(ob)o(vious.)257 1395 y Fq(Sub)n(c)n(ase)g Fr(G)11 b Fs(!)g Fr(D)q Ft(.)19 b(Then)14 b Fr(D)i Ft(is)d(irrelev)n(an)o(t,)h(hence)h(also)e Fr(G)h Ft(is)f(irrelev)n(an)o(t.)649 1573 y Fs(j)571 1639 y Fr(D)g Fs(!)e Fr(D)706 1624 y Fj(X)831 1592 y Fr(G)g Fs(!)g Fr(D)1132 1480 y Fs(j)1057 1546 y Fr(G)1090 1531 y Fj(X)1133 1546 y Fs(!)g Fr(G)93 b(G)1345 1531 y Fj(X)p 1041 1556 353 2 v 1200 1592 a Fr(G)p 815 1602 435 2 v 1014 1639 a(D)p 554 1649 513 2 v 777 1692 a(D)812 1677 y Fj(X)p 581 1702 459 2 v 598 1745 a Ft(\()p Fr(G)11 b Fs(!)g Fr(D)q Ft(\))h Fs(!)f Fr(G)860 1730 y Fj(X)903 1745 y Fs(!)g Fr(D)991 1730 y Fj(X)257 1833 y Ft(Here)k(w)o(e)g(ha)o(v) o(e)e(used)i(the)g(induction)e(h)o(yp)q(otheses)j(\(5\))d(for)h Fr(G)f Ft(and)h(\(4\))g(for)g Fr(D)q Ft(.)320 1882 y Fq(Sub)n(c)n(ase)21 b Fs(8)p Fr(xD)q Ft(.)30 b(By)18 b(the)g(induction)g(h)o(yp)q(othesis)g(\(4\))g(for)f Fr(D)i Ft(w)o(e)f(ha)o(v)o(e)g Fr(D)h Fs(!)f Fr(D)1646 1867 y Fj(X)1678 1882 y Ft(,)257 1932 y(whic)o(h)c(clearly)g(implies)e Fs(8)p Fr(xD)h Fs(!)e(8)p Fr(xD)879 1917 y Fj(X)911 1932 y Ft(.)320 1982 y(\(5\).)18 b(Let)c Fr(G)g Ft(b)q(e)g(irrelev)n(an)o (t.)k Fq(Case)f Fr(P)6 b Ft(.)17 b(Then)e Fr(P)1089 1967 y Fj(X)1131 1982 y Ft(=)d Fr(P)19 b Ft(and)14 b(the)g(claim)e(is)i(ob)o (vious.)320 2032 y Fq(Case)j Fr(D)c Fs(!)e Fr(G)p Ft(.)629 2215 y Fs(j)554 2281 y Fr(G)587 2266 y Fj(X)629 2281 y Fs(!)g Fr(G)808 2228 y(D)843 2213 y Fj(X)887 2228 y Fs(!)g Fr(G)973 2213 y Fj(X)1175 2109 y Fs(j)1097 2175 y Fr(D)i Fs(!)e Fr(D)1232 2160 y Fj(X)1358 2175 y Fr(D)p 1081 2185 330 2 v 1212 2228 a(D)1247 2213 y Fj(X)p 792 2238 504 2 v 1011 2281 a Fr(G)1044 2266 y Fj(X)p 537 2291 556 2 v 798 2328 a Fr(G)p 585 2338 459 2 v 602 2381 a Ft(\()p Fr(D)653 2366 y Fj(X)697 2381 y Fs(!)g Fr(G)783 2366 y Fj(X)814 2381 y Ft(\))h Fs(!)f Fr(D)i Fs(!)e Fr(G)257 2468 y Ft(Here)k(w)o(e)g(ha)o(v)o(e)e(used)i(the)g(induction)e(h)o(yp)q (otheses)j(\(5\))d(for)h Fr(G)f Ft(and)h(\(4\))g(for)g Fr(D)q Ft(.)963 2628 y(7)p eop %%Page: 8 8 8 7 bop 320 262 a Fq(Case)17 b Fs(8)p Fr(xG)p Ft(.)866 297 y Fs(j)791 363 y Fr(G)824 348 y Fj(X)866 363 y Fs(!)11 b Fr(G)1045 310 y Fs(8)p Fr(xG)1125 295 y Fj(X)p 1029 320 145 2 v 1069 363 a Fr(G)1102 348 y Fj(X)p 774 373 376 2 v 945 409 a Fr(G)p 905 419 113 2 v 922 457 a Fs(8)p Fr(xG)p 818 467 289 2 v 834 510 a Fs(8)p Fr(xG)914 495 y Fj(X)957 510 y Fs(!)g(8)p Fr(xG)257 570 y Ft(Here)k(w)o(e)g(ha)o(v)o (e)e(used)i(the)g(induction)e(h)o(yp)q(othesis)i(\(5\))f(for)f Fr(G)p Ft(.)320 620 y(\(6\).)36 b(W)m(e)19 b(ma)o(y)f(assume)i(that)g Fr(G)f Ft(is)h(relev)n(an)o(t,)h(for)f(otherwise)g(the)h(claim)d (clearly)257 670 y(follo)o(ws)13 b(from)f(\(5\).)18 b Fq(Case)f Fs(?)p Ft(.)g(Ob)o(vious,)c(since)i Fs(?)1049 655 y Fj(X)1091 670 y Ft(=)d Fr(X)s Ft(.)320 719 y Fq(Case)20 b Fr(D)f Fs(!)e Fr(G)p Ft(.)28 b(Our)17 b(goal)g(is)g(\()p Fr(D)888 704 y Fj(X)937 719 y Fs(!)g Fr(G)1029 704 y Fj(X)1060 719 y Ft(\))h Fs(!)e Ft(\(\()p Fr(D)k Fs(!)c Fr(G)p Ft(\))h Fs(!)g Fr(X)s Ft(\))h Fs(!)f Fr(X)s Ft(.)29 b(Let)257 769 y Fs(D)289 775 y Fm(1)308 769 y Ft([)p Fr(D)355 754 y Fj(X)398 769 y Fs(!)11 b Fr(G)484 754 y Fj(X)515 769 y Fr(;)c Ft(\()p Fr(D)13 b Fs(!)e Fr(G)p Ft(\))g Fs(!)g Fr(X)s Ft(])j(b)q(e)560 878 y Fs(j)366 944 y Fr(G)399 929 y Fj(X)442 944 y Fs(!)d Ft(\()p Fr(G)g Fs(!)g Fr(X)s Ft(\))i Fs(!)e Fr(X)803 891 y(D)838 876 y Fj(X)881 891 y Fs(!)g Fr(G)967 876 y Fj(X)1037 891 y Fr(D)1072 876 y Fj(X)p 799 901 310 2 v 921 944 a Fr(G)954 929 y Fj(X)p 362 964 628 2 v 541 1004 a Ft(\()p Fr(G)h Fs(!)f Fr(X)s Ft(\))h Fs(!)f Fr(X)1142 900 y Ft(\()p Fr(D)i Fs(!)f Fr(G)p Ft(\))f Fs(!)g Fr(X)1498 854 y(G)p 1444 864 142 2 v 1448 900 a(D)i Fs(!)e Fr(G)p 1138 921 447 2 v 1343 957 a(X)p 1290 967 144 2 v 1294 1004 a(G)g Fs(!)g Fr(X)p 537 1024 896 2 v 966 1061 a(X)p 896 1071 178 2 v 900 1114 a(D)935 1099 y Fj(X)979 1114 y Fs(!)g Fr(X)257 1191 y Ft(\(using)j(the)h(induction)e(h)o(yp)q(othesis)i (\(6\))f(for)f Fr(G)p Ft(\))h(and)f Fs(D)1148 1197 y Fm(2)1167 1191 y Ft([\()p Fr(D)g Fs(!)e Fr(G)p Ft(\))g Fs(!)g Fr(X)s Ft(])j(b)q(e)697 1416 y(\()p Fr(D)f Fs(!)e Fr(G)p Ft(\))h Fs(!)f Fr(X)1058 1275 y Fs(:)p Fr(D)94 b(D)p 1041 1285 226 2 v 1138 1322 a Fs(?)p 1121 1332 66 2 v 1137 1369 a Fr(G)p 1071 1379 166 2 v 1087 1416 a(D)13 b Fs(!)e Fr(G)p 681 1436 556 2 v 940 1473 a(X)p 859 1483 199 2 v 876 1519 a Fs(:)p Fr(D)i Fs(!)e Fr(X)257 1594 y Ft(Note)i(that)g(the)g(passage)g(from)e Fs(?)h Ft(to)g Fr(G)g Ft(can)h(b)q(e)g(done)g(b)o(y)f(means)g(of)g(in)o(tro)q (duction)g(rules,)257 1644 y(since)j Fr(G)f Ft(is)f(relev)n(an)o(t.)320 1693 y Fq(Sub)n(c)n(ase)k Fr(D)f Ft(relev)n(an)o(t.)325 1827 y Fs(D)357 1833 y Fm(1)376 1827 y Ft([)p Fr(D)423 1812 y Fj(X)454 1827 y Fs(!)p Fr(G)529 1812 y Fj(X)560 1827 y Fr(;)7 b Ft(\()p Fr(D)q Fs(!)p Fr(G)p Ft(\))p Fs(!)o Fr(X)s Ft(])562 1889 y Fs(j)483 1956 y Fr(D)518 1940 y Fj(X)562 1956 y Fs(!)k Fr(X)1063 1826 y Fs(j)904 1892 y Ft(\()p Fs(:)p Fr(D)i Fs(!)e Fr(X)s Ft(\))i Fs(!)e Fr(D)1202 1877 y Fj(X)1327 1770 y Fs(D)1359 1776 y Fm(2)1378 1770 y Ft([\()p Fr(D)q Fs(!)o Fr(G)p Ft(\))p Fs(!)p Fr(X)s Ft(])1469 1832 y Fs(j)1392 1892 y(:)p Fr(D)h Fs(!)f Fr(X)p 888 1912 686 2 v 1197 1956 a(D)1232 1940 y Fj(X)p 467 1965 814 2 v 855 2002 a Fr(X)p 510 2012 728 2 v 527 2055 a Ft(\()p Fr(D)578 2040 y Fj(X)621 2055 y Fs(!)g Fr(G)707 2040 y Fj(X)739 2055 y Ft(\))g Fs(!)g Ft(\(\()p Fr(D)j Fs(!)d Fr(G)p Ft(\))g Fs(!)g Fr(X)s Ft(\))h Fs(!)f Fr(X)257 2142 y Ft(Here)k(w)o(e)g(ha)o(v)o(e)e(used)i(the)g(induction)e(h)o(yp)q (othesis)i(\(3\))f(for)f Fr(D)q Ft(.)320 2192 y Fq(Sub)n(c)n(ase)18 b Fr(D)d Ft(irrelev)n(an)o(t.)k(Then)14 b Fr(D)i Ft(is)e(quan)o (ti\014er-free.)19 b(W)m(e)14 b(use)h(case)g(distinction)f(on)257 2242 y Fr(D)i Ft(from)d(lemma)e(2.3,)i(in)h(the)h(form)e(\()p Fr(D)h Fs(!)d Fr(X)s Ft(\))i Fs(!)f Ft(\()p Fs(:)p Fr(D)i Fs(!)e Fr(X)s Ft(\))h Fs(!)f Fr(X)s Ft(.)20 b(So)14 b(it)g(su\016ces)i (to)257 2292 y(deriv)o(e)f(from)e Fr(D)514 2277 y Fj(X)559 2292 y Fs(!)f Fr(G)646 2277 y Fj(X)692 2292 y Ft(and)i(\()p Fr(D)g Fs(!)e Fr(G)p Ft(\))h Fs(!)f Fr(X)18 b Ft(b)q(oth)d(premises;)f (recall)h(that)f(our)h(goal)257 2342 y(w)o(as)h(\()p Fr(D)390 2327 y Fj(X)436 2342 y Fs(!)d Fr(G)524 2327 y Fj(X)555 2342 y Ft(\))h Fs(!)f Ft(\(\()p Fr(D)j Fs(!)d Fr(G)p Ft(\))h Fs(!)f Fr(X)s Ft(\))i Fs(!)e Fr(X)s Ft(.)22 b(The)16 b(negativ)o(e)f(case)h(is)g(pro)o(vided)f(b)o(y)963 2628 y(8)p eop %%Page: 9 9 9 8 bop 257 262 a Fs(D)289 268 y Fm(2)308 262 y Ft([\()p Fr(D)13 b Fs(!)e Fr(G)p Ft(\))g Fs(!)g Fr(X)s Ft(],)j(and)f(the)i(p)q (ositiv)o(e)e(case)i(b)o(y)501 346 y Fs(D)533 352 y Fm(1)552 346 y Ft([)p Fr(D)599 331 y Fj(X)642 346 y Fs(!)c Fr(G)728 331 y Fj(X)759 346 y Fr(;)c Ft(\()p Fr(D)13 b Fs(!)e Fr(G)p Ft(\))g Fs(!)g Fr(X)s Ft(])773 409 y Fs(j)694 475 y Fr(D)729 460 y Fj(X)773 475 y Fs(!)g Fr(X)1228 355 y Fs(j)1150 422 y Fr(D)i Fs(!)e Fr(D)1285 406 y Fj(X)1410 422 y Fr(D)p 1133 431 330 2 v 1264 475 a(D)1299 460 y Fj(X)p 678 485 671 2 v 994 521 a Fr(X)p 927 531 171 2 v 944 568 a(D)i Fs(!)e Fr(X)257 639 y Ft(Here)k(w)o(e)g(ha)o(v)o(e)e (used)i(the)g(induction)e(h)o(yp)q(othesis)i(\(4\))f(for)f Fr(D)q Ft(.)p 1672 614 18 2 v 1672 637 2 24 v 1688 637 V 1672 639 18 2 v 257 725 a Fe(Lemma)j(3.2.)21 b Fq(F)m(or)14 b(go)n(al)h(formulas)862 715 y Fr(~)855 725 y(G)c Ft(=)h Fr(G)976 731 y Fm(1)995 725 y Fr(;)7 b(:)g(:)g(:)k(;)c(G)1127 731 y Fj(n)1164 725 y Fq(we)14 b(have)714 811 y Fr(Z)745 793 y Fj(X)789 811 y Fs(`)d Ft(\()847 800 y Fr(~)841 811 y(G)h Fs(!)f Fr(X)s Ft(\))h Fs(!)1063 800 y Fr(~)1057 811 y(G)1090 793 y Fj(X)1133 811 y Fs(!)f Fr(X)q(:)257 896 y Fq(Pr)n(o)n(of.)20 b Ft(By)15 b(lemma)10 b(3.1\(6\))j(w)o(e)h(ha) o(v)o(e)712 981 y Fr(Z)743 964 y Fj(X)786 981 y Fs(`)e Fr(G)856 964 y Fj(X)856 991 y(i)899 981 y Fs(!)f Ft(\()p Fr(G)1001 987 y Fj(i)1026 981 y Fs(!)g Fr(X)s Ft(\))h Fs(!)f Fr(X)257 1071 y Ft(for)h(all)e Fr(i)i Ft(=)f(1)p Fr(;)c(:)g(:)g(:)e(;)i(n)p Ft(.)17 b(No)o(w)11 b(the)h(assertion)g (follo)o(ws)e(b)o(y)h(minima)o(l)d(logic:)16 b(Assume)1561 1061 y Fr(~)1555 1071 y(G)11 b Fs(!)g Fr(X)257 1121 y Ft(and)344 1110 y Fr(~)338 1121 y(G)371 1106 y Fj(X)402 1121 y Ft(;)j(w)o(e)g(m)o(ust)f(sho)o(w)g Fr(X)s Ft(.)320 1171 y(Because)h(of)e Fr(G)556 1156 y Fj(X)556 1181 y Fm(1)598 1171 y Fs(!)g Ft(\()p Fr(G)701 1177 y Fm(1)730 1171 y Fs(!)g Fr(X)s Ft(\))g Fs(!)f Fr(X)16 b Ft(it)c(su\016ces)i(to)e (pro)o(v)o(e)g Fr(G)1324 1177 y Fm(1)1354 1171 y Fs(!)f Fr(X)s Ft(.)18 b(Assume)13 b Fr(G)1660 1177 y Fm(1)1678 1171 y Ft(.)320 1221 y(Because)h(of)e Fr(G)556 1206 y Fj(X)556 1231 y Fm(2)598 1221 y Fs(!)g Ft(\()p Fr(G)701 1227 y Fm(2)730 1221 y Fs(!)g Fr(X)s Ft(\))g Fs(!)f Fr(X)16 b Ft(it)c(su\016ces)i(to)e(pro)o(v)o(e)g Fr(G)1324 1227 y Fm(2)1354 1221 y Fs(!)f Fr(X)s Ft(.)18 b(Assume)13 b Fr(G)1660 1227 y Fm(2)1678 1221 y Ft(.)320 1270 y(Rep)q(eating)k (this)h(pattern,)h(w)o(e)f(\014nally)f(ha)o(v)o(e)h(assumptions)f Fr(G)1338 1276 y Fm(1)1356 1270 y Fr(;)7 b(:)g(:)g(:)e(;)i(G)1482 1276 y Fj(n)1521 1270 y Ft(a)o(v)n(ailable,)257 1320 y(and)14 b(obtain)f Fr(X)18 b Ft(from)623 1310 y Fr(~)617 1320 y(G)11 b Fs(!)g Fr(X)s Ft(.)p 1672 1295 V 1672 1319 2 24 v 1688 1319 V 1672 1321 18 2 v 257 1402 a Fe(Theorem)k(3.3.)21 b Fq(Assume)d(that)g(for)f(de\014nite)h(formulas)1201 1392 y Fr(~)1194 1402 y(D)h Fq(and)g(go)n(al)e(formulas)1599 1392 y Fr(~)1593 1402 y(G)g Fq(we)257 1452 y(have)718 1502 y Fr(Z)746 1508 y Fm(0)777 1502 y Fs(`)820 1491 y Fr(~)814 1502 y(D)c Fs(!)e(8)p Fr(~)-21 b(y)r Ft(\()981 1491 y Fr(~)975 1502 y(G)11 b Fs(!)g(?)p Ft(\))g Fs(!)g(?)p Fr(:)257 1573 y Fq(Then)16 b(we)e(also)h(have)706 1623 y Fr(Z)737 1605 y Fj(X)780 1623 y Fs(`)824 1612 y Fr(~)817 1623 y(D)e Fs(!)e(8)p Fr(~)-21 b(y)r Ft(\()984 1612 y Fr(~)978 1623 y(G)12 b Fs(!)f Fr(X)s Ft(\))h Fs(!)f Fr(X)q(:)257 1694 y Fq(In)16 b(p)n(articular,)d(substitution)i(of)g(the)g(formula) 725 1779 y Fs(9)748 1762 y Fl(\003)766 1779 y Fr(~)-20 b(y)r(:)807 1768 y(~)801 1779 y(G)10 b Ft(:=)i Fs(9)923 1762 y Fl(\003)941 1779 y Fr(~)-20 b(y)r(:G)1009 1785 y Fm(1)1036 1779 y Fs(^)9 b Fr(:)e(:)g(:)g Fs(^)i Fr(G)1200 1785 y Fj(n)257 1864 y Fq(for)15 b Fr(X)j Fq(yields)824 1914 y Fr(Z)d Fs(`)910 1903 y Fr(~)903 1914 y(D)e Fs(!)f(9)1027 1897 y Fl(\003)1045 1914 y Fr(~)-20 b(y)q(:)1085 1903 y(~)1079 1914 y(G:)257 1992 y Fq(Pr)n(o)n(of.)20 b Ft(Substitution)14 b(of)f Fr(X)18 b Ft(for)13 b Fs(?)h Ft(in)f(the)i(giv)o(en)e(deriv)n (ation)g(yields)674 2077 y Fr(Z)705 2060 y Fj(X)702 2088 y Fm(0)749 2077 y Fs(`)792 2067 y Fr(~)786 2077 y(D)821 2060 y Fj(X)864 2077 y Fs(!)e(8)p Fr(~)-21 b(y)r Ft(\()984 2067 y Fr(~)978 2077 y(G)1011 2060 y Fj(X)1054 2077 y Fs(!)11 b Fr(X)s Ft(\))i Fs(!)e Fr(X)q(:)257 2167 y Ft(No)o(w)j(b)o(y)g (lemma)c(3.1\(4\))j(w)o(e)h(can)g(drop)g Fr(X)k Ft(in)1004 2157 y Fr(~)997 2167 y(D)1032 2152 y Fj(X)1064 2167 y Ft(,)c(and)g(b)o(y)f(lemma)e(3.2)i(also)g(in)1567 2157 y Fr(~)1560 2167 y(G)1593 2152 y Fj(X)1625 2167 y Ft(.)320 2222 y(The)i(second)h(assertion)f(follo)o(ws)f(from)f(the)i(\014rst)h (one)f(since)h Fs(8)p Fr(~)-21 b(y)r(:)1354 2212 y(~)1348 2222 y(G)12 b Fs(!)h(9)1471 2207 y Fl(\003)1489 2222 y Fr(~)-20 b(y)r(:)1530 2212 y(~)1524 2222 y(G)14 b Ft(clearly)257 2272 y(is)g(deriv)n(able.)p 1672 2247 V 1672 2270 2 24 v 1688 2270 V 1672 2272 18 2 v 320 2354 a(The)g(theorem)g(can)g(b)q(e)h (view)o(ed)f(in)g(the)g(standard)h(w)o(a)o(y)e(to)h(yield)g(a)g(metho)q (d)f(for)h(pro-)257 2403 y(gram)j(extraction)i(from)e(classical)i(pro)q (ofs.)32 b(Ho)o(w)o(ev)o(er,)20 b(in)e(section)h(5)f(w)o(e)h(giv)o(e)f (a)h(\014ner)257 2453 y(analysis)d(of)h(the)g(extracted)h(programs,)e (and)h(an)f(explanation)g(of)g(the)i(role)f(of)f(de\014nite)257 2503 y(and)e(goal)f(form)o(ulas.)963 2628 y(9)p eop %%Page: 10 10 10 9 bop 257 262 a Fe(Example)41 b Ft(Let)15 b(us)g(c)o(hec)o(k)g(the)g (mec)o(hanism)e(of)h(w)o(orking)f(with)h(de\014nite)h(and)g(goal)e (for-)257 311 y(m)o(ulas)k(for)h(Kreisel's)h(\\non-example")e(giv)o(en) h(in)g(the)h(in)o(tro)q(duction.)32 b(There)19 b(w)o(e)g(ga)o(v)o(e)257 361 y(a)f(trivial)e(pro)q(of)h(in)h(classical)f(logic)g(of)g(a)g Fs(89)p Ft(-form)o(ula)e(that)j(cannot)g(b)q(e)g(realized)g(b)o(y)g(a) 257 411 y(computable)12 b(function,)g(and)h(w)o(e)g(b)q(etter)h(mak)o (e)d(sure)j(that)f(our)g(general)g(result)h(also)e(do)q(es)257 461 y(not)i(pro)o(vide)g(suc)o(h)h(a)f(function.)k(The)c(example)f (amoun)o(ts)f(to)i(a)g(pro)q(of)f(in)h(minim)o(al)c(logic)257 511 y(of)373 602 y Fs(8)p Fr(z)r Ft(\()p Fs(::)p Fr(R)p Ft(\()p Fr(x;)d(z)r Ft(\))k Fs(!)g Fr(R)p Ft(\()p Fr(x;)c(z)r Ft(\)\))k Fs(!)g(8)p Fr(y)933 568 y Fd(\000)953 602 y Ft(\()p Fr(R)p Ft(\()p Fr(x;)c(y)q Ft(\))12 b Fs(!)f(8)p Fr(z)r(R)p Ft(\()p Fr(x;)c(z)r Ft(\)\))k Fs(!)g(?)1447 568 y Fd(\001)1477 602 y Fs(!)g(?)p Fr(:)257 693 y Ft(Here)18 b Fr(R)p Ft(\()p Fr(x;)7 b(y)q Ft(\))16 b Fs(!)f(8)p Fr(z)r(R)p Ft(\()p Fr(x;)7 b(z)r Ft(\))16 b(is)h(a)f(goal)f(form)o (ula,)f(but)j(the)g(premise)f Fs(8)p Fr(z)r(:)p Fs(::)p Fr(R)p Ft(\()p Fr(x;)7 b(z)r Ft(\))14 b Fs(!)257 743 y Fr(R)p Ft(\()p Fr(x;)7 b(z)r Ft(\))i(is)h Fq(not)j Ft(de\014nite.)18 b(Replacing)8 b Fr(R)i Ft(b)o(y)f Fs(:)p Fr(S)j Ft(\(to)d(get)h(rid)f(of)g(the)h(stabilit)o(y)f(assumption\))257 793 y(do)q(es)i(not)e(help,)h(for)f(then)h Fs(:)p Fr(S)r Ft(\()p Fr(x;)d(y)q Ft(\))13 b Fs(!)e(8)p Fr(z)r Fs(:)p Fr(S)r Ft(\()p Fr(x;)c(z)r Ft(\))j(is)f Fq(not)14 b Ft(a)9 b(goal)f(form)o(ula.)14 b(A)c(third)f(p)q(os-)257 843 y(sibilit)o(y)f(w)o(ould)h(b)q(e)i(to)e(use)h(the)h(fact)e(that)h Fr(R)g Ft(is)f(primitiv)o(e)e(recursiv)o(e)12 b(and)d(write)h Fk(atom)o Ft(\()p Fr(r)q(xy)q Ft(\))257 892 y(instead)15 b(of)f Fr(R)p Ft(\()p Fr(x;)7 b(y)q Ft(\).)21 b(Ho)o(w)o(ev)o(er,)15 b(then)g Fs(8)p Fr(y)929 859 y Fd(\000)949 892 y Ft(\()p Fk(atom)o Ft(\()p Fr(r)q(xy)q Ft(\))e Fs(!)g(8)p Fr(z)c Fk(atom)n Ft(\()p Fr(r)q(xz)r Ft(\)\))k Fs(!)g(?)1572 859 y Fd(\001)1603 892 y Fs(!)f(?)257 942 y Ft(could)i(only)f(b)q(e)i (pro)o(v)o(ed)f(in)f Fr(Z)s Ft(,)h Fq(not)k Ft(in)13 b Fr(Z)908 948 y Fm(0)941 942 y Ft(as)h(required)h(in)e(theorem)h(3.3.) 257 1059 y Fc(Ho)n(w)20 b(to)e(obtain)h(de\014nite)e(and)j(goal)e(form) n(ulas)257 1135 y Ft(T)m(o)d(apply)g(these)i(results)g(w)o(e)f(ha)o(v)o (e)f(to)h(kno)o(w)f(that)g(our)h(assumptions)f(are)h(de\014nite)g(for-) 257 1185 y(m)o(ulas)d(and)i(our)g(goal)f(is)g(giv)o(en)h(b)o(y)f(goal)g (form)o(ulas.)19 b(F)m(or)14 b(quan)o(ti\014er-free)i(form)o(ulas)c (this)257 1235 y(clearly)k(can)h(alw)o(a)o(ys)e(b)q(e)h(ac)o(hiev)o(ed) h(b)o(y)f(inserting)g(double)g(negations)g(in)f(fron)o(t)h(of)g(ev)o (ery)257 1285 y(atom)11 b(\(cf.)i(the)g(de\014nitions)f(of)g (de\014nite)i(and)e(goal)g(form)o(ulas\).)j(This)e(corresp)q(onds)h(to) f(the)257 1334 y(original)i(\(unre\014ned\))k(so-called)d Fr(A)p Ft(-translation)g(of)g(F)m(riedman)f([11)o(])h(\(or)h(Leiv)n(an) o(t)f([15)o(]\).)257 1384 y(Ho)o(w)o(ev)o(er,)h(in)f(order)g(to)g (obtain)g(reasonable)g(programs)f(whic)o(h)h(do)g(not)g(unneccessarily) 257 1434 y(use)f(higher)f(t)o(yp)q(es)h(or)f(case)h(analysis)f(w)o(e)g (w)o(an)o(t)g(to)g(insert)g(double)g(negations)g(only)f(at)h(as)257 1484 y(few)g(places)h(as)f(p)q(ossible.)320 1534 y(W)m(e)f(describ)q(e) j(a)d(more)g(economical)g(general)h(w)o(a)o(y)f(to)h(obtain)f (de\014nite)i(and)e(goal)g(for-)257 1583 y(m)o(ulas,)k(follo)o(wing)e ([2)o(,)i(3].)29 b(It)18 b(consists)g(in)g(singling)e(out)h(some)g (predicate)i(sym)o(b)q(ols)d(as)257 1633 y(b)q(eing)f(\\critical",)e (and)i(then)g(double)f(negating)g(only)g(the)h(atoms)e(formed)h(with)g (critical)257 1683 y(predicate)h(sym)o(b)q(ols;)d(call)h(these)j Fq(critic)n(al)h Ft(atoms.)320 1733 y(Assume)c(w)o(e)i(ha)o(v)o(e)e(a)h (pro)q(of)f(in)h(minim)o(al)c(arithmetic)j Fr(Z)k Ft(of)582 1824 y Fs(8)o Fr(~)-20 b(x)629 1830 y Fm(1)648 1824 y Fr(C)678 1830 y Fm(1)708 1824 y Fs(!)11 b(\001)c(\001)g(\001)j(!)h(8)o Fr(~)-20 b(x)921 1830 y Fj(n)943 1824 y Fr(C)973 1830 y Fj(n)1007 1824 y Fs(!)11 b(8)p Fr(~)-21 b(y)r Ft(\()1128 1814 y Fr(~)1121 1824 y(B)14 b Fs(!)d(?)p Ft(\))g Fs(!)g(?)257 1920 y Ft(with)361 1910 y Fr(~)354 1920 y(C)s(;)412 1910 y(~)406 1920 y(B)18 b Ft(quan)o(ti\014er-free)f(\(among)e(the)i (premises)f Fs(8)o Fr(~)-20 b(x)1169 1926 y Fj(i)1183 1920 y Fr(C)1213 1926 y Fj(i)1243 1920 y Ft(w)o(e)16 b(ma)o(y)f(ha)o(v)o(e)h(efq-axioms)257 1970 y(for)f(quan)o (ti\014er-free)g(form)o(ulas,)e(hence)j(in)e(fact)h(the)g(situation)f (describ)q(ed)j(applies)d(to)h(in-)257 2020 y(tuitionistic)e(logic\).) 18 b(Let)727 2116 y Fr(L)12 b Ft(:=)f Fs(f)c Fr(C)880 2122 y Fm(1)898 2116 y Fr(;)g(:)g(:)g(:)e(;)i(C)1021 2122 y Fj(n)1043 2116 y Fr(;)1068 2106 y(~)1062 2116 y(B)14 b Fs(!)d(?)c(g)320 2208 y Ft(The)20 b(set)h(of)f Fr(L)p Ft(-)p Fq(critic)n(al)j Ft(predicate)e(sym)o(b)q(ols)e(is)h (de\014ned)h(to)f(b)q(e)h(the)g(smallest)e(set)257 2257 y(satisfying)297 2340 y(\(i\))h Fs(?)13 b Ft(is)h(critical.)285 2428 y(\(ii\))20 b(If)15 b(\()426 2418 y Fr(~)420 2428 y(C)450 2434 y Fm(1)481 2428 y Fs(!)e Fr(R)568 2434 y Fm(1)586 2428 y Ft(\()n Fr(~)-19 b(s)621 2434 y Fm(1)640 2428 y Ft(\)\))14 b Fs(!)e(\001)7 b(\001)g(\001)12 b(!)h Ft(\()879 2418 y Fr(~)873 2428 y(C)903 2434 y Fj(m)947 2428 y Fs(!)g Fr(R)1034 2434 y Fj(m)1065 2428 y Ft(\()n Fr(~)-19 b(s)1100 2434 y Fj(m)1132 2428 y Ft(\)\))14 b Fs(!)e Fr(R)p Ft(\()n Fr(~)-19 b(s)q Ft(\))15 b(is)f(a)h(p)q(ositiv)o (e)f(subfor-)361 2478 y(m)o(ula)e(of)h Fr(L)p Ft(,)h(and)f(if)g(some)g Fr(R)819 2484 y Fj(i)847 2478 y Ft(is)g Fr(L)p Ft(-critical,)g(then)i Fr(R)f Ft(is)f Fr(L)p Ft(-critical.)953 2628 y(10)p eop %%Page: 11 11 11 10 bop 257 262 a Ft(No)o(w)11 b(if)f(w)o(e)h(double)f(negate)i(ev)o (ery)f Fr(L)p Ft(-critical)g(atom)e(di\013eren)o(t)j(from)d Fs(?)h Ft(w)o(e)h(clearly)f(obtain)257 311 y(de\014nite)17 b(assumptions)651 301 y Fr(~)645 311 y(C)678 296 y Fl(0)705 311 y Ft(and)e(goal)g(form)o(ulas)1054 301 y Fr(~)1047 311 y(B)1080 296 y Fl(0)1093 311 y Ft(.)23 b(F)m(urthermore)16 b(the)g(pro)q(of)g(term)f(of)257 361 y(the)i(giv)o(en)e(deriv)n(ation)f (can)i(easily)f(b)q(e)i(transformed)e(in)o(to)f(a)i(correct)h(deriv)n (ation)e(of)g(the)257 411 y(translated)j(form)o(ula)c(from)i(the)i (translated)f(assumptions)f(\(b)o(y)h(inserting)g(the)h(ob)o(vious)257 461 y(pro)q(ofs)c(of)g(the)g(translated)g(axioms\).)320 511 y(Ho)o(w)o(ev)o(er,)k(in)e(particular)h(cases)i(w)o(e)e(migh)o(t)e (b)q(e)j(able)f(to)g(obtain)g(de\014nite)h(and)f(goal)257 560 y(form)o(ulas)d(with)i(still)f(few)o(er)i(double)f(negations:)22 b(it)16 b(ma)o(y)e(not)i(b)q(e)h(necessary)h(to)e(double)257 610 y(negate)f Fq(every)i Ft(critical)d(atom.)320 660 y(Of)f(course)h(this)g(metho)q(d)e(will)g(b)q(e)h(really)g(useful)g (only)g(if)f(b)q(esides)j Fk(atom)d Ft(and)h Fs(?)f Ft(there)257 710 y(are)j(other)f(predicate)h(sym)o(b)q(ols)d(a)o(v)n(ailable.)k(Our) f(results)g(could)e(b)q(e)i(easily)e(adapted)h(to)g(a)257 760 y(language)f(with)h(free)h(predicate)g(sym)o(b)q(ols.)257 896 y Fu(4)67 b(Program)23 b(Extraction)257 986 y Ft(W)m(e)16 b(assign)g(to)f(ev)o(ery)i(form)o(ula)d Fr(A)i Ft(an)f(ob)r(ject)i Fr(\034)5 b Ft(\()p Fr(A)p Ft(\))16 b(\(a)g(t)o(yp)q(e)h(or)e(the)i (sym)o(b)q(ol)d Fs(\003)p Ft(\).)24 b Fr(\034)5 b Ft(\()p Fr(A)p Ft(\))257 1036 y(is)17 b(in)o(tended)g(to)f(b)q(e)h(the)g(t)o (yp)q(e)g(of)f(the)h(program)e(to)i(b)q(e)g(extracted)h(from)d(a)h(pro) q(of)g(of)g Fr(A)p Ft(,)257 1086 y(assuming)11 b(that)h(a)g(pro)q(of)g (of)g Fr(X)j Ft(carries)f(computational)9 b(con)o(ten)o(t)k(of)f(some)f (giv)o(en)h(t)o(yp)q(e)h Fr(\027)s Ft(.)677 1170 y Fr(\034)5 b Ft(\()p Fr(X)s Ft(\))12 b(:=)f Fr(\027)682 1232 y(\034)5 b Ft(\()p Fr(P)h Ft(\))11 b(:=)g Fs(\003)41 b Ft(\(in)14 b(particular)g Fr(\034)5 b Ft(\()p Fs(?)p Ft(\))11 b(=)g Fs(\003)p Ft(\))617 1336 y Fr(\034)5 b Ft(\()p Fs(8)p Fr(x)703 1319 y Fj(\032)722 1336 y Fr(A)p Ft(\))12 b(:=)836 1265 y Fd(\()870 1308 y Fs(\003)192 b Ft(if)13 b Fr(\034)5 b Ft(\()p Fr(A)p Ft(\))12 b(=)g Fs(\003)870 1367 y Fr(\032)g Fs(!)f Fr(\034)5 b Ft(\()p Fr(A)p Ft(\))41 b(otherwise)585 1505 y Fr(\034)5 b Ft(\()p Fr(A)12 b Fs(!)f Fr(B)r Ft(\))h(:=)836 1407 y Fd(8)836 1444 y(>)836 1457 y(<)836 1531 y(>)836 1544 y(:)873 1446 y Fr(\034)5 b Ft(\()p Fr(B)r Ft(\))193 b(if)13 b Fr(\034)5 b Ft(\()p Fr(A)p Ft(\))12 b(=)g Fs(\003)873 1506 y(\003)260 b Ft(if)13 b Fr(\034)5 b Ft(\()p Fr(B)r Ft(\))12 b(=)g Fs(\003)873 1566 y Fr(\034)5 b Ft(\()p Fr(A)p Ft(\))12 b Fs(!)f Fr(\034)5 b Ft(\()p Fr(B)r Ft(\))42 b(otherwise)257 1653 y(W)m(e)18 b(no)o(w)g(de\014ne,)i(for)e(a)g(giv)o (en)f(deriv)n(ation)h Fr(M)23 b Ft(of)17 b(a)h(form)o(ula)e Fr(A)i Ft(with)g Fr(\034)5 b Ft(\()p Fr(A)p Ft(\))19 b Fs(6)p Ft(=)g Fs(\003)p Ft(,)f(its)257 1702 y Fq(extr)n(acte)n(d)d (pr)n(o)n(gr)n(am)h Ft([)-7 b([)p Fr(M)5 b Ft(])-7 b(])12 b(of)i(t)o(yp)q(e)g Fr(\034)5 b Ft(\()p Fr(A)p Ft(\).)716 1786 y([)-7 b([)p Fr(u)757 1769 y Fj(A)783 1786 y Ft(])g(])10 b(:=)i Fr(u)890 1769 y Fj(\034)s Fm(\()p Fj(A)p Fm(\))647 1890 y Ft([)-7 b([)p Fr(\025u)712 1873 y Fj(A)738 1890 y Fr(M)5 b Ft(])-7 b(])10 b(:=)866 1819 y Fd(\()899 1862 y Ft([)-7 b([)p Fr(M)5 b Ft(])-7 b(])159 b(if)13 b Fr(\034)5 b Ft(\()p Fr(A)p Ft(\))12 b(=)g Fs(\003)899 1922 y Fr(\025u)947 1906 y Fj(\034)s Fm(\()p Fj(A)p Fm(\))1019 1922 y Ft([)-7 b([)p Fr(M)5 b Ft(])-7 b(])39 b(otherwise)597 2031 y([)-7 b([)p Fr(M)659 2014 y Fj(A)p Fl(!)p Fj(B)745 2031 y Fr(N)5 b Ft(])-7 b(])10 b(:=)866 1960 y Fd(\()899 2003 y Ft([)-7 b([)p Fr(M)5 b Ft(])-7 b(])110 b(if)13 b Fr(\034)5 b Ft(\()p Fr(A)p Ft(\))12 b(=)g Fs(\003)899 2063 y Ft([)-7 b([)p Fr(M)5 b Ft(])-7 b(][)g([)p Fr(N)5 b Ft(])-7 b(])38 b(otherwise)654 2135 y([)-7 b([)p Fr(\025x)719 2117 y Fj(\032)738 2135 y Fr(M)5 b Ft(])-7 b(])10 b(:=)i Fr(\025x)914 2117 y Fj(\032)933 2135 y Ft([)-7 b([)p Fr(M)5 b Ft(])-7 b(])707 2197 y([)g([)p Fr(M)5 b(t)p Ft(])-7 b(])9 b(:=)j([)-7 b([)p Fr(M)5 b Ft(])-7 b(])p Fr(t)257 2280 y Ft(W)m(e)14 b(also)f(need)i(extracted)g(programs)e(for)h(the)g(axioms.)380 2364 y([)-7 b([)p Fk(Ind)451 2370 y Fj(p;A)505 2364 y Ft(])g(])10 b(:=)i Fs(R)623 2370 y Fi(o)p Fj(;\032)672 2364 y Ft(:)i Fr(\032)e Fs(!)f Fr(\032)h Fs(!)f Fk(o)g Fs(!)g Fr(\032)230 b Ft(with)14 b Fr(\032)e Ft(:=)f Fr(\034)5 b Ft(\()p Fr(A)p Ft(\))12 b Fs(6)p Ft(=)g Fs(\003)p Fr(;)377 2426 y Ft([)-7 b([)p Fk(Ind)447 2432 y Fj(n;A)505 2426 y Ft(])g(])10 b(:=)i Fs(R)623 2432 y Fj(\023;\032)669 2426 y Ft(:)h Fr(\032)f Fs(!)f Ft(\()p Fr(\023)h Fs(!)f Fr(\032)h Fs(!)f Fr(\032)p Ft(\))h Fs(!)f Fr(\023)g Fs(!)g Fr(\032)42 b Ft(with)14 b Fr(\032)e Ft(:=)f Fr(\034)5 b Ft(\()p Fr(A)p Ft(\))12 b Fs(6)p Ft(=)g Fs(\003)p Fr(;)405 2488 y Ft([)-7 b([)p Fk(efq)473 2498 y Fj(X)505 2488 y Ft(])g(])10 b(:=)i Fk(dummy)716 2470 y Fj(\027)953 2628 y Ft(11)p eop %%Page: 12 12 12 11 bop 257 262 a Ft(where)21 b Fk(dummy)511 243 y Fj(\027)551 262 y Ft(is)e(an)g(arbitrary)g(closed)h(term)e(of)h(t)o(yp) q(e)h Fr(\027)s Ft(.)33 b(F)m(or)18 b(deriv)n(ations)h Fr(M)24 b Ft(of)257 311 y Fr(A)18 b Ft(with)f Fr(\034)5 b Ft(\()p Fr(A)p Ft(\))18 b(=)g Fs(\003)g Ft(w)o(e)g(de\014ne)g([)-7 b([)p Fr(M)5 b Ft(])-7 b(])16 b(:=)i Fr(")g Ft(\()p Fr(")g Ft(some)e(new)i(sym)o(b)q(ol\).)28 b(This)18 b(applies)f(in)257 361 y(particular)d(if)f Fr(A)h Ft(is)g(an)f Fs(L)p Ft(-form)o(ula.)320 411 y(Finally)c(w)o(e)i(de\014ne)h Fq(mo)n(di\014e)n(d)h(r)n(e)n (alizability)f Ft(for)f(form)o(ulas)e(in)h Fs(L)p Ft([)p Fr(X)s Ft(].)17 b(F)m(or)10 b(the)i(prop)q(osi-)257 461 y(tional)g(sym)o(b)q(ol)e Fr(X)16 b Ft(w)o(e)d(need)g(a)f (comprehension)h(term)e Fs(A)h Ft(:=)f Fr(\025y)1275 446 y Fj(\027)1297 461 y Fr(A)1328 467 y Fm(0)1359 461 y Ft(with)h(an)h Fs(L)p Ft(-form)o(ula)257 511 y Fr(A)288 517 y Fm(0)307 511 y Ft(;)k(write)g Fs(A)p Ft(\()p Fr(r)q Ft(\))f(for)g Fr(A)643 517 y Fm(0)662 511 y Ft([)p Fr(y)695 496 y Fj(\027)732 511 y Ft(:=)f Fr(r)q Ft(].)25 b(More)17 b(precisely)m(,)g(w)o(e)f(de\014ne)h(form)o(ulas)e Fr(r)h Fe(mr)1603 517 y Fl(A)1647 511 y Fr(A)p Ft(,)257 560 y(where)g Fr(r)g Ft(is)f(either)g(a)g(term)f(of)g(t)o(yp)q(e)i Fr(\034)5 b Ft(\()p Fr(A)p Ft(\))15 b(if)f(the)h(latter)g(is)g(a)g(t)o (yp)q(e,)g(or)g(the)g(sym)o(b)q(ol)e Fr(")i Ft(if)257 610 y Fr(\034)5 b Ft(\()p Fr(A)p Ft(\))12 b(=)g Fs(\003)p Ft(.)448 695 y Fr(r)g Fe(mr)538 701 y Fl(A)579 695 y Fr(X)26 b Ft(=)e Fs(A)p Ft(\()p Fr(r)q Ft(\))453 757 y Fr(r)12 b Fe(mr)544 763 y Fl(A)584 757 y Fr(P)28 b Ft(=)c Fr(P)407 862 y(r)13 b Fe(mr)498 868 y Fl(A)538 862 y Fs(8)p Fr(xA)23 b Ft(=)695 791 y Fd(\()728 833 y Fs(8)p Fr(x:")11 b Fe(mr)877 839 y Fl(A)917 833 y Fr(A)66 b Ft(if)13 b Fr(\034)5 b Ft(\()p Fr(A)p Ft(\))12 b(=)g Fs(\003)728 893 y(8)p Fr(x:r)q(x)f Fe(mr)901 899 y Fl(A)941 893 y Fr(A)42 b Ft(otherwise)324 1030 y Fr(r)12 b Fe(mr)415 1036 y Fl(A)455 1030 y Ft(\()p Fr(A)g Fs(!)f Fr(B)r Ft(\))23 b(=)695 933 y Fd(8)695 970 y(>)695 982 y(<)695 1057 y(>)695 1070 y(:)732 972 y Fr(")12 b Fe(mr)822 978 y Fl(A)862 972 y Fr(A)24 b Fs(!)e Fr(r)12 b Fe(mr)1072 978 y Fl(A)1112 972 y Fr(B)131 b Ft(if)13 b Fr(\034)5 b Ft(\()p Fr(A)p Ft(\))12 b(=)f Fs(\003)732 1032 y(8)p Fr(x:x)f Fe(mr)885 1038 y Fl(A)925 1032 y Fr(A)23 b Fs(!)g Fr(")12 b Fe(mr)1134 1038 y Fl(A)1174 1032 y Fr(B)69 b Ft(if)13 b Fr(\034)5 b Ft(\()p Fr(A)p Ft(\))12 b Fs(6)p Ft(=)f Fs(\003)h Ft(=)f Fr(\034)5 b Ft(\()p Fr(B)r Ft(\))732 1091 y Fs(8)p Fr(x:x)10 b Fe(mr)885 1097 y Fl(A)925 1091 y Fr(A)23 b Fs(!)g Fr(r)q(x)11 b Fe(mr)1158 1097 y Fl(A)1199 1091 y Fr(B)44 b Ft(otherwise)257 1180 y(Note)19 b(that)f(for)g Fs(L)p Ft(-form)o(ulas)d Fr(A)k Ft(w)o(e)f(ha)o(v)o(e)g Fr(\034)5 b Ft(\()p Fr(A)p Ft(\))19 b(=)g Fs(\003)f Ft(and)g Fr(")h Fe(mr)1331 1186 y Fl(A)1378 1180 y Fr(A)g Ft(=)g Fr(A)p Ft(.)31 b(F)m(or)18 b(the)257 1230 y(form)o(ulation)11 b(of)j(the)g(soundness)i(theorem)d (it)h(will)e(b)q(e)j(useful)f(to)g(let)g Fr(u)1387 1215 y Fj(\034)s Fm(\()p Fj(A)p Fm(\))1470 1230 y Ft(:=)d Fr(")k Ft(if)e Fr(u)1621 1215 y Fj(A)1662 1230 y Ft(is)257 1279 y(an)h(assumption)f(v)n(ariable)f(with)i Fr(\034)5 b Ft(\()p Fr(A)p Ft(\))12 b(=)g Fs(\003)p Ft(.)257 1357 y Fe(Theorem)j(4.1.)21 b Fq(\(Soundness\).)k(Assume)16 b(that)h Fr(M)k Fq(is)16 b(a)g Fr(Z)1231 1342 y Fj(X)1263 1357 y Fq(-derivation)g(of)g Fr(B)r Fq(.)24 b(Then)257 1407 y(ther)n(e)16 b(is)g(a)h Fr(Z)s Fq(-derivation)f(of)g Ft([)-7 b([)p Fr(M)5 b Ft(])-7 b(])13 b Fe(mr)891 1413 y Fl(A)934 1407 y Fr(B)19 b Fq(fr)n(om)c(the)i(assumptions)g Fs(f)7 b Fr(u)1443 1392 y Fj(\034)s Fm(\()p Fj(C)r Fm(\))1529 1407 y Fe(mr)1588 1413 y Fl(A)1631 1407 y Fr(C)17 b Fs(j)257 1457 y Fr(u)281 1442 y Fj(C)321 1457 y Fs(2)11 b Fk(F)m(A)o Ft(\()p Fr(M)5 b Ft(\))i Fs(g)p Fq(.)257 1535 y(Pr)n(o)n(of.)20 b Ft(Induction)13 b(on)f Fr(M)5 b Ft(.)18 b Fq(Case)d Fk(Ind)862 1541 y Fj(n;A)919 1535 y Ft(.)j(T)m(ak)o(e)12 b Fs(R)1083 1541 y Fj(\023;\032)1124 1535 y Ft(.)18 b Fq(Case)d Fk(Ind)1311 1541 y Fj(p;A)1365 1535 y Ft(.)i(T)m(ak)o(e)12 b Fs(R)1528 1541 y Fi(o)p Fj(;\032)1573 1535 y Ft(.)18 b Fq(Case)257 1585 y Fk(efq)310 1595 y Fj(A)342 1585 y Ft(:)13 b Fs(?)e(!)g Fr(A)p Ft(.)18 b(Then)573 1670 y([)-7 b([)p Fk(efq)641 1680 y Fj(A)668 1670 y Ft(])g(])11 b Fe(mr)756 1676 y Fl(A)796 1670 y Ft(\()p Fs(?)g(!)g Fr(A)p Ft(\))h(=)f Fs(?)g(!)g Ft([)-7 b([)p Fk(efq)1177 1680 y Fj(A)1204 1670 y Ft(])g(])11 b Fe(mr)1291 1676 y Fl(A)1331 1670 y Fr(A;)257 1755 y Ft(whic)o(h)g(is)f(an)g(instance)h (of)e(the)i(same)f(axiom)d(sc)o(heme.)17 b(The)11 b(inductiv)o(e)f (steps)i(are)f(straigh)o(t-)257 1804 y(forw)o(ard.)p 1672 1780 18 2 v 1672 1803 2 24 v 1688 1803 V 1672 1805 18 2 v 257 1941 a Fu(5)67 b(Computational)24 b(Con)n(ten)n(t)e(of)g (Classical)g(Pro)r(ofs)257 2032 y Ft(F)m(or)13 b(a)f(smo)q(oth)g(form)o (ulation)d(of)j(the)i(follo)o(wing)c(theorem)i(when)h(writing)f(an)h (application)257 2081 y Fr(ts)k Ft(where)g Fr(s)g Ft(is)f(of)f(t)o(yp)q (e)i Fs(\003)p Ft(,)f(w)o(e)g(mean)f(simply)g Fr(t)p Ft(.)24 b(Similarly)13 b(abstractions)k(of)e(the)i(form)257 2131 y Fr(\025w)312 2116 y Fl(\003)332 2131 y Fr(t)c Ft(stand)i(for)e Fr(t)p Ft(.)257 2209 y Fe(Theorem)i(5.1.)21 b Fq(L)n(et)640 2199 y Fr(~)634 2209 y(D)26 b Ft(=)f Fr(D)785 2215 y Fm(1)804 2209 y Fr(;)7 b(:)g(:)g(:)e(;)i(D)931 2215 y Fj(n)975 2209 y Fq(and)1069 2199 y Fr(~)1063 2209 y(G)24 b Ft(=)h Fr(G)1210 2215 y Fm(1)1229 2209 y Fr(;)7 b(:)g(:)g(:)t(;)g(G)1354 2215 y Fj(m)1407 2209 y Fq(b)n(e)22 b(arbitr)n(ary)f Fs(L)p Fq(-)257 2259 y(formulas.)e(Assume)c(that)g(we) f(have)i(terms)e Fr(t)974 2265 y Fm(1)992 2259 y Fr(;)7 b(:)g(:)g(:)e(;)i(t)1100 2265 y Fj(n)1122 2259 y Fr(;)g(s)1160 2265 y Fm(1)1179 2259 y Fr(;)g(:)g(:)g(:)t(;)g(s)1290 2265 y Fj(m)1322 2259 y Fr(;)g(r)15 b Fq(such)g(that)322 2344 y Fr(Z)g Fs(`)408 2333 y Fr(~)401 2344 y(D)e Fs(!)e Fr(t)516 2350 y Fj(j)546 2344 y Fe(mr)605 2350 y Fl(A)645 2344 y Fr(D)680 2327 y Fj(X)679 2354 y(j)1311 2344 y Fq(for)j Ft(1)e Fs(\024)f Fr(j)j Fs(\024)e Fr(n)p Fq(,)70 b Ft(\(7\))322 2416 y Fr(Z)15 b Fs(`)408 2406 y Fr(~)401 2416 y(D)e Fs(!)e Fr(w)531 2422 y Fj(i)557 2416 y Fe(mr)616 2422 y Fl(A)656 2416 y Fr(G)689 2399 y Fj(X)689 2427 y(i)732 2416 y Fs(!)g Ft(\()p Fr(G)834 2422 y Fj(i)859 2416 y Fs(!)g(A)p Ft(\()p Fr(v)981 2422 y Fj(i)995 2416 y Ft(\)\))h Fs(!)f(A)p Ft(\()p Fr(s)1160 2422 y Fj(i)1175 2416 y Fr(w)1205 2422 y Fj(i)1218 2416 y Fr(v)1238 2422 y Fj(i)1252 2416 y Ft(\))43 b Fq(for)14 b Ft(1)e Fs(\024)f Fr(i)h Fs(\024)g Fr(m)p Fq(,)64 b Ft(\(8\))322 2488 y Fr(Z)15 b Fs(`)408 2478 y Fr(~)401 2488 y(D)e Fs(!)e(8)p Fr(~)-21 b(y)r(:)564 2478 y(~)558 2488 y(G)11 b Fs(!)g(A)p Ft(\()p Fr(r)q(~)-21 b(y)r Ft(\))p Fr(:)862 b Ft(\(9\))953 2628 y(12)p eop %%Page: 13 13 13 12 bop 257 262 a Fq(L)n(et)15 b Fr(M)20 b Fq(b)n(e)15 b(a)g Fr(Z)504 268 y Fm(0)523 262 y Fq(-derivation)f(of)790 251 y Fr(~)783 262 y(D)f Fs(!)e(8)p Fr(~)-21 b(y)r Ft(\()950 251 y Fr(~)944 262 y(G)11 b Fs(!)g(?)p Ft(\))g Fs(!)g(?)p Fq(,)j(and)322 365 y Fr(s)e Ft(:=)f Fr(\025~)-21 b(y)r(\025)5 b(~)-26 b(w)q(:s)540 371 y Fm(1)559 365 y Fr(w)589 371 y Fm(1)607 365 y Ft(\()p Fr(:)7 b(:)g(:)f Ft(\()p Fr(s)714 371 y Fj(m)746 365 y Fr(w)776 371 y Fj(m)807 365 y Ft(\()p Fr(r)q(~)-21 b(y)r Ft(\)\))7 b Fr(:)g(:)g(:)e Ft(\))p Fr(:)257 469 y Fq(Then)322 573 y Fr(Z)15 b Fs(`)408 562 y Fr(~)401 573 y(D)e Fs(!)e(A)p Ft(\([)-7 b([)p Fr(M)612 556 y Fj(X)643 573 y Ft(])g(])p Fr(t)675 579 y Fm(1)700 573 y Fr(:)7 b(:)g(:)e(t)770 579 y Fj(n)793 573 y Fr(s)p Ft(\))p Fr(:)257 668 y Fq(Pr)n(o)n(of.)20 b Ft(F)m(rom)12 b(the)i Fr(Z)595 674 y Fm(0)614 668 y Ft(-deriv)n(ation)f Fr(M)18 b Ft(w)o(e)c(obtain)f(b)o(y)g(the)i(substitution)e Fs(?)e(7!)g Fr(X)17 b Ft(a)d Fr(Z)1644 653 y Fj(X)1641 679 y Fm(0)1676 668 y Ft(-)257 723 y(deriv)n(ation)f Fr(M)497 708 y Fj(X)533 723 y Ft(:)565 712 y Fr(~)559 723 y(D)594 708 y Fj(X)637 723 y Fs(!)e(8)p Fr(~)-21 b(y)r Ft(\()757 712 y Fr(~)751 723 y(G)784 708 y Fj(X)827 723 y Fs(!)11 b Fr(X)s Ft(\))h Fs(!)g Fr(X)s Ft(.)18 b(The)c(soundness)i(theorem)d(4.1)g(yields)303 819 y([)-7 b([)p Fr(M)365 802 y Fj(X)395 819 y Ft(])g(])11 b Fe(mr)482 825 y Fl(A)522 786 y Fd(\000)548 809 y Fr(~)541 819 y(D)576 802 y Fj(X)620 819 y Fs(!)g(8)p Fr(~)-21 b(y)r Ft(\()740 809 y Fr(~)734 819 y(G)767 802 y Fj(X)810 819 y Fs(!)11 b Fr(X)s Ft(\))h Fs(!)f Fr(X)1018 786 y Fd(\001)314 891 y Ft(=)h Fs(8)o Fr(~)-20 b(u)p Fs(8)p Fr(v)q(:)o(~)g(u)11 b Fe(mr)556 897 y Fl(A)602 880 y Fr(~)596 891 y(D)631 874 y Fj(X)675 891 y Fs(!)g Ft(\()p Fr(v)i Fe(mr)836 897 y Fl(A)877 891 y Fs(8)p Fr(~)-21 b(y)q(:)939 880 y(~)933 891 y(G)966 874 y Fj(X)1009 891 y Fs(!)11 b Fr(X)s Ft(\))h Fs(!)f(A)p Ft(\([)-7 b([)p Fr(M)1291 874 y Fj(X)1322 891 y Ft(])g(])o Fr(~)-20 b(u)o(v)q Ft(\))314 963 y(=)12 b Fs(8)o Fr(~)-20 b(u)p Fs(8)p Fr(v)q(:)o(~)g(u)11 b Fe(mr)556 969 y Fl(A)602 952 y Fr(~)596 963 y(D)631 945 y Fj(X)675 963 y Fs(!)g(8)p Fr(~)-21 b(y)q Fs(8)5 b Fr(~)-26 b(w)826 929 y Fd(\000)851 963 y Fr(~)f(w)13 b Fe(mr)947 969 y Fl(A)994 952 y Fr(~)987 963 y(G)1020 945 y Fj(X)1063 963 y Fs(!)e(A)p Ft(\()p Fr(v)q(~)-21 b(y)8 b(~)-26 b(w)q Ft(\))1256 929 y Fd(\001)1287 963 y Fs(!)11 b(A)p Ft(\([)-7 b([)p Fr(M)1451 945 y Fj(X)1481 963 y Ft(])g(])o Fr(~)-20 b(u)o(v)q Ft(\))p Fr(:)46 b Ft(\(10\))257 1063 y(Instan)o(tiate)16 b(\(10\))f(with)651 1056 y Fr(~)654 1063 y(t)g Ft(for)f Fr(~)-20 b(u)15 b Ft(and)g Fr(s)h Ft(for)f Fr(v)q Ft(.)22 b(Clearly)1168 1056 y Fr(~)1171 1063 y(t)14 b Fe(mr)1259 1069 y Fl(A)1308 1053 y Fr(~)1302 1063 y(D)1337 1048 y Fj(X)1384 1063 y Ft(is)h(deriv)n(able)g(from)264 1108 y Fr(~)257 1118 y(D)h Ft(b)o(y)e(\(7\),)f(so)h(it)g(remains)f(to)g(sho) o(w)851 1108 y Fr(~)844 1118 y(D)g Fs(!)k Fr(~)-27 b(w)13 b Fe(mr)1046 1124 y Fl(A)1093 1108 y Fr(~)1086 1118 y(G)1119 1103 y Fj(X)1162 1118 y Fs(!)e(A)p Ft(\()p Fr(s~)-21 b(y)8 b(~)-26 b(w)q Ft(\).)320 1168 y(Let)20 b Fr(a)422 1174 y Fj(m)p Fm(+1)518 1168 y Ft(:=)i Fr(r)q(~)-21 b(y)21 b Ft(and)g Fr(a)755 1174 y Fj(i)790 1168 y Ft(:=)h Fr(s)875 1174 y Fj(i)889 1168 y Fr(w)919 1174 y Fj(i)933 1168 y Fr(a)955 1174 y Fj(i)p Fm(+1)1011 1168 y Ft(,)f(hence)h Fr(s)g Ft(=)g Fr(\025~)-21 b(y)r(\025)5 b(~)-26 b(w)8 b(a)1391 1174 y Fm(1)1410 1168 y Ft(.)37 b(W)m(e)20 b(sho)o(w)g(b)o(y) 257 1218 y(induction)14 b(on)g Fr(j)g Ft(:=)d Fr(m)f Fs(\000)f Fr(i)301 1298 y(~)294 1309 y(D)k Fs(!)e Fr(G)427 1315 y Fm(1)457 1309 y Fs(!)g(\001)c(\001)g(\001)j(!)h Fr(G)656 1315 y Fj(i)681 1309 y Fs(!)g Fr(w)764 1315 y Fj(i)p Fm(+1)831 1309 y Fe(mr)891 1315 y Fl(A)931 1309 y Fr(G)964 1292 y Fj(X)964 1319 y(i)p Fm(+1)1031 1309 y Fs(!)g(\001)c(\001)g(\001)j(!)h Fr(w)1227 1315 y Fj(m)1270 1309 y Fe(mr)1329 1315 y Fl(A)1369 1309 y Fr(G)1402 1292 y Fj(X)1402 1319 y(m)1445 1309 y Fs(!)g(A)p Ft(\()p Fr(a)1569 1315 y Fj(i)p Fm(+1)1625 1309 y Ft(\))p Fr(:)1616 1359 y Ft(\(11\))257 1451 y Fq(Basis)p Ft(.)19 b(F)m(or)14 b Fr(j)g Ft(=)e(0)i(w)o(e)g(ha)o(v)o(e)g Fr(i)e Ft(=)g Fr(m)i Ft(and)g(\(11\))g(holds)g(b)o(y)g(\(9\).)19 b Fq(Step)p Ft(.)g(F)m(rom)12 b(the)j(IH)f(\(11\))257 1500 y(and)g(the)h(assumption)d(\(8\))i(w)o(e)g(obtain)274 1586 y Fr(~)268 1597 y(D)f Fs(!)e Fr(G)401 1603 y Fm(1)430 1597 y Fs(!)g(\001)c(\001)g(\001)j(!)h Fr(G)629 1603 y Fj(i)p Fl(\000)p Fm(1)697 1597 y Fs(!)g Fr(w)780 1603 y Fj(i)805 1597 y Fe(mr)864 1603 y Fl(A)905 1597 y Fr(G)938 1579 y Fj(X)938 1607 y(i)980 1597 y Fs(!)h(\001)7 b(\001)g(\001)i(!)j Fr(w)1177 1603 y Fj(m)1219 1597 y Fe(mr)1279 1603 y Fl(A)1319 1597 y Fr(G)1352 1579 y Fj(X)1352 1607 y(m)1395 1597 y Fs(!)f(A)p Ft(\()p Fr(s)1516 1603 y Fj(i)1530 1597 y Fr(w)1560 1603 y Fj(i)1574 1597 y Fr(a)1596 1603 y Fj(i)p Fm(+1)1652 1597 y Ft(\))p Fr(:)257 1688 y Ft(F)m(or)j Fr(j)g Ft(=)e Fr(m)i Ft(w)o(e)g(ha)o(v)o(e)g Fr(i)e Ft(=)f(0)j(and)g (hence)h(w)o(e)f(obtain)f(from)f(\(11\))520 1774 y Fr(~)513 1784 y(D)h Fs(!)e Fr(w)643 1790 y Fm(1)673 1784 y Fe(mr)733 1790 y Fl(A)773 1784 y Fr(G)806 1767 y Fj(X)806 1794 y Fm(1)849 1784 y Fs(!)g(\001)c(\001)g(\001)j(!)h Fr(w)1045 1790 y Fj(m)1088 1784 y Fe(mr)1147 1790 y Fl(A)1187 1784 y Fr(G)1220 1767 y Fj(X)1220 1794 y(m)1263 1784 y Fs(!)g(A)p Ft(\()p Fr(a)1387 1790 y Fm(1)1406 1784 y Ft(\))p Fr(;)257 1875 y Ft(whic)o(h)j(w)o(as)g(to)g(b)q(e)g(sho)o(wn.)p 1672 1850 18 2 v 1672 1874 2 24 v 1688 1874 V 1672 1876 18 2 v 320 1958 a(In)i(order)h(to)f(apply)f(theorem)h(5.1,)f(w)o(e)i (need)g Fs(A)e Ft(=)h Fr(\025y)q(A)1234 1964 y Fm(0)1270 1958 y Ft(and)g(terms)g Fr(t)1486 1964 y Fj(j)1504 1958 y Fr(;)7 b(s)1542 1964 y Fj(i)1555 1958 y Fr(;)g(r)17 b Ft(suc)o(h)257 2008 y(that)e(\(7\){\(9\))f(hold.)20 b(The)15 b(c)o(hoice)g(of)f Fs(A)h Ft(and)f Fr(r)h Ft(of)f(course)i (dep)q(ends)g(on)f(the)g(application)257 2058 y(at)g(hand)g(and)f (should)h(b)q(e)g(done)g(suc)o(h)h(that)e(\(9\))h(holds.)20 b(The)c(rest)f(follo)o(ws)f(from)f(lemma)257 2108 y(3.1)g(b)o(y)h(the)g (soundness)i(theorem)d(4.1:)257 2191 y Fe(Theorem)i(5.2.)21 b Fq(F)m(or)12 b(every)g(de\014nite)g(formula)g Fr(D)i Fq(and)e(go)n(al)h(formula)e Fr(G)h Fq(we)g(have)g(terms)257 2241 y Fr(t;)7 b(s)15 b Fq(such)h(that)e(for)h(an)g(arbitr)n(ary)f Fs(A)d Ft(=)h Fr(\025y)q(A)968 2247 y Fm(0)1003 2241 y Fq(with)i(an)h Fs(L)p Fq(-formula)f Fr(A)1381 2247 y Fm(0)1400 2241 y Fq(:)589 2332 y Fr(Z)h Fs(`)d Fr(D)h Fs(!)e Fr(t)g Fe(mr)855 2338 y Fl(A)895 2332 y Fr(D)930 2315 y Fj(X)962 2332 y Fr(;)642 b Ft(\(12\))589 2401 y Fr(Z)15 b Fs(`)d Fr(w)g Fe(mr)770 2407 y Fl(A)811 2401 y Fr(G)844 2383 y Fj(X)886 2401 y Fs(!)f Ft(\()p Fr(G)h Fs(!)f(A)p Ft(\()p Fr(v)q Ft(\)\))i Fs(!)e(A)p Ft(\()p Fr(sw)q(v)q Ft(\))259 b(\(13\))953 2628 y(13)p eop %%Page: 14 14 14 13 bop 257 262 a Fq(Pr)n(o)n(of.)20 b Ft(\(12\).)d(Let)c Fr(N)596 268 y Fj(D)638 262 y Ft(b)q(e)f(the)h Fr(Z)793 246 y Fj(X)824 262 y Ft(-deriv)n(ation)e(of)g Fr(D)i Fs(!)e Fr(D)1211 246 y Fj(X)1255 262 y Ft(from)f(lemma)f(3.1\(4\))o(.) 17 b(The)257 311 y(soundness)f(theorem)d(yields)420 393 y Fr(Z)i Fs(`)d Ft([)-7 b([)p Fr(N)550 399 y Fj(D)580 393 y Ft(])g(])10 b Fe(mr)667 399 y Fl(A)707 393 y Ft(\()p Fr(D)j Fs(!)e Fr(D)858 376 y Fj(X)890 393 y Ft(\))p Fr(;)49 b Ft(i.e.)40 b Fr(Z)15 b Fs(`)d Fr(D)h Fs(!)e Ft([)-7 b([)p Fr(N)1291 399 y Fj(D)1321 393 y Ft(])g(])10 b Fe(mr)1408 399 y Fl(A)1448 393 y Fr(D)1483 376 y Fj(X)1515 393 y Fr(:)320 475 y Ft(\(13\))o(.)24 b(Let)16 b Fr(H)540 481 y Fj(G)583 475 y Ft(b)q(e)h(the)f Fr(Z)746 460 y Fj(X)778 475 y Ft(-deriv)n(ation)e(of)h Fr(G)1070 460 y Fj(X)1116 475 y Fs(!)f Ft(\()p Fr(G)h Fs(!)f Fr(X)s Ft(\))h Fs(!)f Fr(X)20 b Ft(from)14 b(lemma)257 525 y(3.1\(6\))o(.)k(By)d(the)f (soundness)h(theorem)546 607 y Fr(Z)f Fs(`)e Ft([)-7 b([)p Fr(H)677 613 y Fj(G)704 607 y Ft(])g(])11 b Fe(mr)791 613 y Fl(A)831 607 y Ft(\()p Fr(G)880 590 y Fj(X)923 607 y Fs(!)g Ft(\()p Fr(G)g Fs(!)g Fr(X)s Ft(\))i Fs(!)e Fr(X)s Ft(\))p Fr(;)49 b Ft(i.e.)546 675 y Fr(Z)14 b Fs(`)e Fr(w)h Fe(mr)727 681 y Fl(A)767 675 y Fr(G)800 658 y Fj(X)843 675 y Fs(!)e Ft(\()p Fr(G)g Fs(!)g(A)p Ft(\()p Fr(v)q Ft(\)\))i Fs(!)e(A)p Ft(\([)-7 b([)p Fr(H)1278 681 y Fj(G)1305 675 y Ft(])g(])p Fr(w)q(v)q Ft(\))p Fr(:)p 1672 732 18 2 v 1672 755 2 24 v 1688 755 V 1672 757 18 2 v 257 838 a Fe(Corollary)15 b(5.3.)21 b Fq(L)n(et)640 828 y Fr(~)634 838 y(D)13 b Ft(=)e Fr(D)758 844 y Fm(1)777 838 y Fr(;)c(:)g(:)g(:)e(;)i(D)904 844 y Fj(n)939 838 y Fq(b)n(e)12 b(de\014nite)g(formulas)g(and)g Fr(G)g Fq(a)g(go)n(al)g(formula.)257 888 y(L)n(et)j Fr(M)20 b Fq(b)n(e)15 b(a)g Fr(Z)504 894 y Fm(0)523 888 y Fq(-derivation)f(of) 790 878 y Fr(~)783 888 y(D)f Fs(!)e(8)p Fr(y)q Ft(\()p Fr(G)h Fs(!)f(?)p Ft(\))g Fs(!)g(?)p Fq(.)19 b(Then)675 975 y Fr(Z)c Fs(`)761 964 y Fr(~)754 975 y(D)f Fs(!)d Fr(G)p Ft([)p Fr(y)h Ft(:=)f([)-7 b([)p Fr(M)1049 958 y Fj(X)1080 975 y Ft(])g(])p Fr(t)1112 981 y Fm(1)1137 975 y Fr(:)7 b(:)g(:)e(t)1207 981 y Fj(n)1230 975 y Fr(s)p Ft(])p Fr(;)257 1062 y Fq(wher)n(e)15 b Fr(t)390 1068 y Fm(1)408 1062 y Fr(;)7 b(:)g(:)g(:)e(;)i(t)516 1068 y Fj(n)538 1062 y Fr(;)g(s)15 b Fq(ar)n(e)f(determine)n(d)h(by)g(the)g (formulas)1176 1051 y Fr(~)1169 1062 y(D)r(;)7 b(G)14 b Fq(only.)257 1197 y Fu(6)67 b(Examples)257 1288 y Ft(W)m(e)15 b(no)o(w)f(w)o(an)o(t)h(to)g(giv)o(e)f(some)g(simple)f(examples)h(of)g (ho)o(w)h(to)g(apply)f(theorems)h(5.1)f(and)257 1338 y(5.2.)29 b(Here)19 b(w)o(e)f(will)e(alw)o(a)o(ys)h(ha)o(v)o(e)g(a)g (single)h(goal)e(form)o(ula)f Fr(G)j Ft(and)f Fs(A)h Ft(will)e(alw)o(a)o(ys)h(b)q(e)257 1388 y(c)o(hosen)e(as)f Fr(\025y)q(G)p Ft(.)19 b(Hence)c(\(9\))f(trivially)e(holds)i(with)f Fr(r)g Ft(:=)e Fr(\025y)q(y)q Ft(.)257 1502 y Fc(6.1)56 b(Fib)r(onacci)18 b(Num)n(b)r(ers)257 1579 y Ft(Let)d Fr(\013)359 1585 y Fj(n)395 1579 y Ft(b)q(e)f(the)h Fr(n)p Ft(-th)f(Fib)q(onacci)f(n)o(um)o(b)q(er,)g(i.e.)497 1661 y Fr(\013)524 1667 y Fm(0)554 1661 y Ft(:=)e(0)p Fr(;)48 b(\013)717 1667 y Fm(1)746 1661 y Ft(:=)12 b(1)p Fr(;)47 b(\013)909 1667 y Fj(n)943 1661 y Ft(:=)11 b Fr(\013)1025 1667 y Fj(n)p Fl(\000)p Fm(2)1099 1661 y Ft(+)f Fr(\013)1168 1667 y Fj(n)p Fl(\000)p Fm(1)1274 1661 y Ft(for)j Fr(n)f Fs(\025)g Ft(2)o Fr(:)257 1743 y Ft(W)m(e)i(w)o(an)o(t)f(to)h(giv)o(e)f (a)g(\(classical\))h(existence)h(pro)q(of)f(for)f(the)i(Fib)q(onacci)e (n)o(um)o(b)q(ers.)18 b(So)13 b(w)o(e)257 1792 y(need)i(to)f(pro)o(v)o (e)579 1874 y Fs(8)p Fr(n)p Fs(9)p Fr(k)7 b(G)p Ft(\()p Fr(n;)g(k)q Ft(\))p Fr(;)48 b Ft(i.e.)40 b Fs(8)p Fr(k)q Ft(\()p Fr(G)p Ft(\()p Fr(n;)7 b(k)q Ft(\))k Fs(!)g(?)p Ft(\))g Fs(!)g(?)257 1956 y Ft(from)h(assumptions)h(expressing)h(that)g Fr(G)f Ft(is)g(the)h(graph)f(of)g(the)h(Fib)q(onacci)g(function,)e (i.e.)352 2038 y Fr(G)p Ft(\(0)p Fr(;)7 b Ft(0\))p Fr(;)47 b(G)p Ft(\(1)p Fr(;)7 b Ft(1\))p Fr(;)47 b Fs(8)p Fr(n)p Fs(8)p Fr(k)q Fs(8)p Fr(l)q(:G)p Ft(\()p Fr(n;)7 b(k)q Ft(\))j Fs(!)h Fr(G)p Ft(\()p Fr(n)e Ft(+)h(1)p Fr(;)d(l)q Ft(\))k Fs(!)g Fr(G)p Ft(\()p Fr(n)e Ft(+)g(2)p Fr(;)e(k)j Ft(+)f Fr(l)q Ft(\))p Fr(:)257 2120 y Ft(Clearly)14 b(the)h(assumption) f(form)o(ulas)e(are)j(de\014nite)g(and)g Fr(G)p Ft(\()p Fr(n;)7 b(k)q Ft(\))13 b(is)i(a)f(goal)f(form)o(ula.)18 b(So)257 2170 y(theorems)c(5.1)f(and)h(5.2)f(can)h(b)q(e)g(applied)g (without)f(inserting)h(double)g(negations.)320 2220 y(T)m(o)f (construct)i(a)f(deriv)n(ation,)e(assume)508 2301 y Fr(v)528 2307 y Fm(0)552 2301 y Ft(:)h Fr(G)p Ft(\(0)p Fr(;)7 b Ft(0\))p Fr(;)508 2364 y(v)528 2370 y Fm(1)552 2364 y Ft(:)13 b Fr(G)p Ft(\(1)p Fr(;)7 b Ft(1\))p Fr(;)508 2426 y(v)528 2432 y Fm(2)552 2426 y Ft(:)13 b Fs(8)p Fr(n)p Fs(8)p Fr(k)q Fs(8)p Fr(l)q(:G)p Ft(\()p Fr(n;)7 b(k)q Ft(\))j Fs(!)h Fr(G)p Ft(\()p Fr(n)e Ft(+)h(1)p Fr(;)d(l)q Ft(\))k Fs(!)g Fr(G)p Ft(\()p Fr(n)e Ft(+)g(2)p Fr(;)e(k)j Ft(+)f Fr(l)q Ft(\))523 2488 y Fr(u)c Ft(:)13 b Fs(8)p Fr(k)q(:G)p Ft(\()p Fr(n;)7 b(k)q Ft(\))j Fs(!)h(?)p Fr(:)953 2628 y Ft(14)p eop %%Page: 15 15 15 14 bop 257 262 a Ft(Our)16 b(goal)e(is)h Fs(?)p Ft(.)20 b(T)m(o)14 b(this)i(end)f(w)o(e)g(\014rst)h(pro)o(v)o(e)f(a)g (strengthened)i(claim)c(in)i(order)g(to)g(get)257 311 y(the)g(induction)e(through:)460 403 y Fs(8)p Fr(nB)44 b Ft(with)14 b Fr(B)g Ft(:=)d Fs(8)p Fr(k)q Fs(8)p Fr(l)q Ft(\()p Fr(G)p Ft(\()p Fr(n;)c(k)q Ft(\))k Fs(!)g Fr(G)p Ft(\()p Fr(n)e Ft(+)h(1)p Fr(;)d(l)q Ft(\))k Fs(!)g(?)p Ft(\))g Fs(!)g(?)p Ft(.)257 494 y(This)j(is)f(pro)o(v)o(ed)h(b)o(y)f (induction)g(on)g Fr(n)p Ft(.)18 b(The)c(base)g(case)h(follo)o(ws)d (from)f Fr(v)1399 500 y Fm(0)1431 494 y Ft(and)j Fr(v)1532 500 y Fm(1)1550 494 y Ft(.)k(In)c(the)257 544 y(step)f(case)g(w)o(e)g (can)f(assume)f(that)h(w)o(e)h(ha)o(v)o(e)e Fr(k)q(;)c(l)13 b Ft(satisfying)e Fr(G)p Ft(\()p Fr(n;)c(k)q Ft(\))k(and)h Fr(G)p Ft(\()p Fr(n)5 b Ft(+)g(1)p Fr(;)i(l)q Ft(\).)18 b(W)m(e)257 594 y(need)e Fr(k)378 579 y Fl(0)389 594 y Fr(;)7 b(l)421 579 y Fl(0)447 594 y Ft(suc)o(h)15 b(that)g Fr(G)p Ft(\()p Fr(n)9 b Ft(+)h(1)p Fr(;)d(k)820 579 y Fl(0)830 594 y Ft(\))15 b(and)f Fr(G)p Ft(\()p Fr(n)9 b Ft(+)h(2)p Fr(;)d(l)1120 579 y Fl(0)1131 594 y Ft(\).)20 b(Using)14 b Fr(v)1316 600 y Fm(2)1349 594 y Ft(simply)f(tak)o(e)h Fr(k)1596 579 y Fl(0)1620 594 y Ft(:=)e Fr(l)257 643 y Ft(and)k Fr(l)353 628 y Fl(0)380 643 y Ft(:=)e Fr(k)e Ft(+)f Fr(l)q Ft(.)24 b({)15 b(T)m(o)g(obtain)g(our)h(goal)f Fs(?)g Ft(from)f Fs(8)p Fr(nB)r Ft(,)i(it)g(clearly)g(su\016ces)h(to)e (pro)o(v)o(e)257 693 y(its)i(premise)f Fs(8)p Fr(k)q Fs(8)p Fr(l)q(:G)p Ft(\()p Fr(n;)7 b(k)q Ft(\))15 b Fs(!)h Fr(G)p Ft(\()p Fr(n)10 b Ft(+)i(1)p Fr(;)7 b(l)q Ft(\))15 b Fs(!)h(?)p Ft(.)25 b(So)16 b(let)h Fr(k)q(;)7 b(l)17 b Ft(b)q(e)g(giv)o(en)f(and)h(assume)257 743 y Fr(u)281 749 y Fm(1)304 743 y Ft(:)d Fr(G)p Ft(\()p Fr(n;)7 b(k)q Ft(\))13 b(and)g Fr(u)579 749 y Fm(2)602 743 y Ft(:)h Fr(G)p Ft(\()p Fr(n)9 b Ft(+)g(1)p Fr(;)e(l)q Ft(\).)18 b(Then)c Fr(u)g Ft(applied)f(to)h Fr(k)h Ft(and)e Fr(u)1334 749 y Fm(1)1367 743 y Ft(giv)o(es)g(our)h(goal)f Fs(?)p Ft(.)320 793 y(The)h(deriv)n(ation)f(term)g(is)336 884 y Fr(M)k Ft(=)p Fr(\025v)470 863 y Fj(G)p Fm(\(0)p Fj(;)p Fm(0\))469 895 y(0)567 884 y Fr(\025v)612 863 y Fj(G)p Fm(\(1)p Fj(;)p Fm(1\))611 895 y(1)710 884 y Fr(\025v)755 863 y Fl(8)p Fj(n)p Fl(8)p Fj(k)q Fl(8)o Fj(l:G)p Fm(\()p Fj(n;k)p Fm(\))p Fl(!)p Fj(G)p Fm(\()p Fj(n)p Fm(+1)p Fj(;l)p Fm(\))p Fl(!)p Fj(G)p Fm(\()p Fj(n)p Fm(+2)p Fj(;k)p Fm(+)p Fj(l)p Fm(\))754 895 y(2)1354 884 y Fr(\025u)1402 867 y Fl(8)p Fj(k)q(:G)p Fm(\()p Fj(n;k)q Fm(\))p Fl(!?)425 959 y Fk(Ind)479 965 y Fj(n;B)538 959 y Fr(M)578 965 y Fm(base)643 959 y Fr(M)683 965 y Fm(step)745 959 y Fr(n)p Ft(\()p Fr(\025k)q(\025l)q(\025u)918 938 y Fj(G)p Fm(\()p Fj(n;k)q Fm(\))918 970 y(1)1021 959 y Fr(\025u)1069 938 y Fj(G)p Fm(\()p Fj(n)p Fm(+1)p Fj(;l)p Fm(\))1069 970 y(2)1206 959 y Fr(:uk)q(u)1289 965 y Fm(1)1307 959 y Ft(\))257 1050 y(where)438 1142 y Fr(M)478 1148 y Fm(base)555 1142 y Ft(=)p Fr(\025w)642 1120 y Fl(8)p Fj(k)q Fl(8)p Fj(l:G)p Fm(\(0)p Fj(;k)p Fm(\))p Fl(!)p Fj(G)p Fm(\(1)p Fj(;l)p Fm(\))p Fl(!?)641 1153 y Fm(0)998 1142 y Fr(:w)1040 1148 y Fm(0)1058 1142 y Ft(01)p Fr(v)1120 1148 y Fm(0)1139 1142 y Fr(v)1159 1148 y Fm(1)442 1217 y Fr(M)482 1223 y Fm(step)555 1217 y Ft(=)p Fr(\025n\025w)691 1200 y Fj(B)720 1217 y Fr(\025w)775 1195 y Fl(8)p Fj(k)q Fl(8)p Fj(l:G)p Fm(\()p Fj(n)p Fm(+1)p Fj(;k)p Fm(\))p Fl(!)p Fj(G)p Fm(\()p Fj(n)p Fm(+2)p Fj(;)o(l)p Fm(\))p Fl(!?)774 1228 y Fm(1)1223 1217 y Fr(:)587 1292 y(w)q Ft(\()p Fr(\025k)q(\025l)q (\025u)766 1270 y Fj(G)p Fm(\()p Fj(n;k)q Fm(\))766 1303 y(3)869 1292 y Fr(\025u)917 1270 y Fj(G)p Fm(\()p Fj(n)p Fm(+1)p Fj(;l)p Fm(\))917 1303 y(4)1054 1292 y Fr(:w)1096 1298 y Fm(1)1114 1292 y Fr(l)q Ft(\()p Fr(k)11 b Ft(+)e Fr(l)q Ft(\))p Fr(u)1270 1298 y Fm(4)1289 1292 y Ft(\()p Fr(v)1325 1298 y Fm(2)1344 1292 y Fr(k)q(l)q(u)1404 1298 y Fm(3)1422 1292 y Fr(u)1446 1298 y Fm(4)1465 1292 y Ft(\)\))p Fr(:)257 1387 y Ft(No)o(w)20 b(let)g Fs(A)i Ft(:=)f Fr(\025k)q(G)p Ft(\()p Fr(n;)7 b(k)q Ft(\),)20 b(and)g Fr(M)887 1372 y Fj(X)938 1387 y Ft(b)q(e)h(obtained)e(from)g Fr(M)24 b Ft(b)o(y)c(replacing)g(ev)o(ery)257 1437 y(o)q(ccurrence)d (of)c Fs(?)g Ft(b)o(y)h Fr(X)s Ft(.)19 b(Therefore)479 1528 y([)-7 b([)p Fr(M)541 1511 y Fj(X)572 1528 y Ft(])g(])10 b(=)i Fr(\025u)691 1511 y Fj(\023)p Fl(!)p Fj(\023)751 1528 y Fr(:)p Fs(R)798 1535 y Fj(\023;)p Fm(\()p Fj(\023)p Fl(!)p Fj(\023)p Fl(!)p Fj(\023)p Fm(\))p Fl(!)p Fj(\023)996 1528 y Ft([)-7 b([)p Fr(M)1058 1511 y Fj(X)1053 1538 y Fm(base)1118 1528 y Ft(])g(][)g([)p Fr(M)1197 1511 y Fj(X)1192 1538 y Fm(step)1251 1528 y Ft(])g(])p Fr(n)p Ft(\()p Fr(\025k)q(\025l)q(:uk)q Ft(\))257 1620 y(where)481 1711 y([)g([)p Fr(M)543 1694 y Fj(X)538 1721 y Fm(base)602 1711 y Ft(])g(])11 b(=)h Fr(\025w)729 1694 y Fj(\023)p Fl(!)p Fj(\023)p Fl(!)p Fj(\023)728 1721 y Fm(0)834 1711 y Fr(:w)876 1717 y Fm(0)894 1711 y Ft(01)485 1781 y([)-7 b([)p Fr(M)547 1764 y Fj(X)542 1792 y Fm(step)602 1781 y Ft(])g(])11 b(=)h Fr(\025n\025w)778 1764 y Fm(\()p Fj(\023)p Fl(!)p Fj(\023)p Fl(!)p Fj(\023)p Fm(\))p Fl(!)p Fj(\023)954 1781 y Fr(\025w)1009 1764 y Fj(\023)p Fl(!)p Fj(\023)p Fl(!)p Fj(\023)1008 1792 y Fm(1)1115 1781 y Fr(:w)q Ft(\()p Fr(\025k)q(\025l)q(:w)1300 1787 y Fm(1)1317 1781 y Fr(l)q Ft(\()p Fr(k)f Ft(+)e Fr(l)q Ft(\)\))257 1873 y(Since)16 b(there)g(are)g(no)e(relev)n(an)o(t)i(form)o(ulas)c(in) o(v)o(olv)o(ed,)i(the)i(extracted)g(term)f(according)g(to)257 1922 y(theorem)f(5.1)f(is)499 2014 y([)-7 b([)p Fr(M)561 1997 y Fj(X)591 2014 y Ft(])g(]\()p Fr(\025xx)p Ft(\))11 b(=)h Fs(R)802 2021 y Fj(\023;)p Fm(\()p Fj(\023)p Fl(!)p Fj(\023)p Fl(!)p Fj(\023)p Fm(\))p Fl(!)p Fj(\023)1001 2014 y Ft([)-7 b([)p Fr(M)1063 1997 y Fj(X)1058 2024 y Fm(base)1122 2014 y Ft(])g(][)g([)p Fr(M)1201 1997 y Fj(X)1196 2024 y Fm(step)1256 2014 y Ft(])g(])p Fr(n)p Ft(\()p Fr(\025k)q(\025l)q(:k)q Ft(\))257 2105 y(This)15 b(algorithm)e(migh)o(t)g(b)q(e)i(easier)h(to)f(understand)h(if)f(w)o(e) g(write)g(it)g(as)g(a)g Fp(Scheme)h Ft(pro-)257 2155 y(gram:)257 2238 y Fb(\(define)21 b(\(fibo)f(n\))i(\(fibo1)e(n)i (\(lambda)e(\(k)i(l\))f(k\)\)\))257 2338 y(\(define)g(\(fibo1)f(n1)i (f\))301 2387 y(\(if)f(\(=)h(n1)f(0\))388 2437 y(\(f)h(0)f(1\))388 2487 y(\(fibo1)g(\(-)g(n1)g(1\))h(\(lambda)e(\(k)i(l\))f(\(f)g(l)h(\(+) f(k)h(l\)\)\)\)\)\))953 2628 y Ft(15)p eop %%Page: 16 16 16 15 bop 257 262 a Ft(This)18 b(is)h(a)e(linear)h(algorithm)e(in)i (tail)f(recursiv)o(e)i(form.)30 b(It)18 b(is)g(somewhat)f(unexp)q (ected)257 311 y(since)i(it)f(passes)i Fr(\025)p Ft(-expressions)f (\(rather)h(than)e(pairs,)g(as)h(one)f(w)o(ould)f(ordinarily)g(do\),) 257 361 y(and)c(hence)i(uses)f(functional)e(programming)d(in)k(a)g (prop)q(er)h(w)o(a)o(y)m(.)i(This)d(clearly)g(is)g(related)257 411 y(to)f(the)f(use)i(of)d(classical)h(logic,)f(whic)o(h)i(b)o(y)f (its)g(use)h(of)f(double)g(negations)g(has)g(a)g(functional)257 461 y(\015a)o(v)o(our.)320 511 y(T)m(o)i(remo)o(v)o(e)g(some)g(of)g (the)i(tedium)e(of)g(doing)g(all)g(that)h(b)o(y)g(hand,)g(w)o(e)g (certainly)g(w)o(an)o(t)257 560 y(mac)o(hine)g(help.)21 b(W)m(e)15 b(ha)o(v)o(e)g(done)g(suc)o(h)h(an)e(implemen)o(tation)e (within)i(our)h(system)g Fp(Min-)257 610 y(log)p Ft(;)f(here)h(is)f (the)h(original)d(prin)o(tout)h(of)h(the)g(extracted)i(term,)d(with)g (only)g(some)g(inden-)257 660 y(tation)h(added.)257 730 y Fb(\(lambda)21 b(\(n^1\))301 780 y(\(\(\(\(\(nat-rec-at)432 830 y(\(quote)f(\(arrow)h(\(arrow)f(nat)i(\(arrow)e(nat)h(nat\)\))g (nat\)\)\))388 879 y(\(lambda)f(\(hh^2\))h(\(\(hh^2)g(\(num)g(0\)\))g (\(num)g(1\)\)\)\))366 929 y(\(lambda)g(\(n^2\))410 979 y(\(lambda)f(\(ff^3\))454 1029 y(\(lambda)g(\(hh^4\))497 1079 y(\(ff^3)h(\(lambda)f(\(n^5\))671 1129 y(\(lambda)h(\(n^6\))715 1178 y(\(\(hh^4)g(n^6\))g(\(\(plus-nat)e(n^5\))i(n^6\)\)\)\)\)\)\)\)\)) 345 1228 y(n^1\))g(\(lambda)f(\(n^2\))h(\(lambda)f(\(n^3\))h (n^2\)\)\)\))257 1298 y Ft(It)12 b(is)f(rather)h(ob)o(vious)f(that)g (this)h(can)f(b)q(e)h(translated)g(in)o(to)f(the)h Fp(Scheme)f Ft(program)f(ab)q(o)o(v)o(e.)257 1368 y Fe(Remark.)21 b Ft(Of)11 b(course,)h(in)e(this)h(example)f(there)i(is)f(no)g(need)g (to)g(do)g(the)g(pro)q(of)g(classically;)257 1418 y(in)h(fact,)g(it)g (is)g(more)f(natural)h(to)g(w)o(ork)g(with)g(the)h(constructiv)o(e)g (existen)o(tial)f(quan)o(ti\014er)g Fs(9)1670 1403 y Fl(\003)257 1468 y Ft(instead.)17 b(Here)12 b(is)e(the)h(term)e (extracted)j(from)c(this)i(pro)q(of)g(\(original)e(output)j(of)h Fp(Minlog)p Ft(\).)257 1538 y Fb(\(lambda)21 b(\(n^1\))301 1588 y(\(car)g(\(\(\(\(nat-rec-at)e(\(quote)h(\(star)h(nat)g(nat\)\)\)) 475 1637 y(\(cons)g(\(num)g(0\))g(\(num)g(1\)\)\))454 1687 y(\(lambda)f(\(n^2\))497 1737 y(\(lambda)g(\(nat*nat^3\))541 1787 y(\(cons)g(\(cdr)h(nat*nat^3\))671 1837 y(\(\(plus-nat)f(\(car)h (nat*nat^3\)\))693 1887 y(\(cdr)g(nat*nat^3\)\)\)\)\)\))e(n^1\)\)\))257 1957 y Ft(A)14 b(more)f(readable)h(Sc)o(heme)g(program)e(is)257 2027 y Fb(\(define)21 b(\(constr-fibo)e(n\))i(\(car)g (\(constr-fibo-aux)e(n\)\)\))257 2126 y(\(define)i(\(constr-fibo-aux)d (n\))301 2176 y(\(if)j(\(=)h(0)f(n\))388 2226 y(\(cons)g(0)g(1\))388 2276 y(\(let)g(\(\(prev)g(\(constr-fibo-aux)d(\(-)k(n)f(1\)\)\)\))432 2325 y(\(cons)f(\(cdr)h(prev\))562 2375 y(\(+)h(\(car)f(prev\))g(\(cdr) g(prev\)\)\)\)\)\))257 2445 y Ft(So)h(the)h(resulting)f(algorithm)e(is) i(linear)f(again,)i(but)f(passes)h(pairs)f(rather)h(than)f Fr(\025)p Ft(-)257 2495 y(expressions.)953 2628 y(16)p eop %%Page: 17 17 17 16 bop 257 262 a Fc(6.2)56 b(W)-5 b(ellfoundedness)18 b(of)h Fa(N)257 338 y Ft(There)e(is)e(an)g(in)o(teresting)h(phenomenon) f(whic)o(h)g(ma)o(y)e(o)q(ccur)k(if)d(w)o(e)i(extract)g(a)f(program)257 388 y(from)e(a)h(classical)g(pro)q(of)g(whic)o(h)g(uses)i(the)f(minim)n (um)10 b(principle.)19 b(Consider)c(as)f(a)g(simple)257 438 y(example)f(the)h(w)o(ellfoundedness)h(of)e Fr(<)h Ft(on)g Fg(N)p Ft(,)d(i.e.)693 525 y Fs(8)p Fr(f)740 508 y Fj(\023)p Fl(!)p Fj(\023)801 525 y Fs(9)p Fr(k)q(:f)t Ft(\()p Fr(k)f Ft(+)g(1\))h Fr(<)h(f)t Ft(\()p Fr(k)q Ft(\))h Fs(!)e(?)p Fr(:)257 612 y Ft(If)16 b(one)f(formalizes)f(the)j (classical)e(pro)q(of)g(\\c)o(ho)q(ose)h Fr(k)h Ft(suc)o(h)f(that)g Fr(f)t Ft(\()p Fr(k)q Ft(\))g(is)g(minim)o(al)o(")d(and)257 662 y(extracts)20 b(a)d(program)f(one)i(migh)o(t)e(exp)q(ect)j(that)f (it)f(computes)h(a)f Fr(k)i Ft(suc)o(h)f(that)g Fr(f)t Ft(\()p Fr(k)q Ft(\))h(is)257 712 y(minima)o(l.)c(But)e(this)g(is)g (imp)q(ossible!)j(In)d(fact)g(the)h(program)d(computes)i(the)h(least)f Fr(k)h Ft(suc)o(h)257 762 y(that)e Fr(f)t Ft(\()p Fr(k)7 b Ft(+)f(1\))12 b Fr(<)g(f)t Ft(\()p Fr(k)q Ft(\))h Fs(!)e(?)g Ft(instead.)18 b(This)12 b(discrepancy)h(b)q(et)o(w)o(een)g(the)g (classical)f(pro)q(of)257 811 y(and)18 b(the)h(extracted)g(program)e (can)h(of)f(course)j(only)d(sho)o(w)h(up)g(if)f(the)i(solution)e(is)h (not)257 861 y(uniquely)c(determined.)320 911 y(W)m(e)i(b)q(egin)g (with)g(a)g(rather)h(detailed)f(exp)q(osition)g(of)g(the)h(classical)f (pro)q(of,)g(since)h(w)o(e)257 961 y(need)d(a)e(complete)f (formalization.)j(Our)f(goal)e(is)h Fs(9)p Fr(k)c(f)t Ft(\()p Fr(k)q Ft(\))13 b Fs(\024)f Fr(f)t Ft(\()p Fr(k)c Ft(+)e(1\),)12 b(and)g(the)h(classical)257 1011 y(pro)q(of)i(consists)i (in)e(using)g(the)h(minim)o(um)11 b(principle)k(to)g(c)o(ho)q(ose)i(a)e (minim)o(al)d(elemen)o(t)j(in)257 1061 y Fk(ran)q Ft(\()p Fr(f)t Ft(\))e(:=)e Fs(f)c Fr(y)13 b Fs(j)e(9)p Fr(x)c(f)t Ft(\()p Fr(x)p Ft(\))12 b(=)g Fr(y)d Fs(g)p Ft(,)k(the)h(range)g(of)f Fr(f)t Ft(.)18 b(This)c(su\016ces,)g(for)f(if)g(w)o(e)h(ha)o(v)o(e)f (suc)o(h)i(a)257 1110 y(minima)o(l)d(elemen)o(t,)i(sa)o(y)g Fr(y)678 1116 y Fm(0)697 1110 y Ft(,)h(then)g(it)f(m)o(ust)g(b)q(e)h (of)f(the)i(form)d Fr(f)t Ft(\()p Fr(x)1306 1116 y Fm(0)1325 1110 y Ft(\),)i(and)f(b)o(y)h(the)g(c)o(hoice)257 1160 y(of)f Fr(y)325 1166 y Fm(0)357 1160 y Ft(w)o(e)h(ha)o(v)o(e)e Fr(f)t Ft(\()p Fr(x)578 1166 y Fm(0)598 1160 y Ft(\))e Fs(\024)h Fr(f)t Ft(\()p Fr(x)p Ft(\))j(for)e(ev)o(ery)i Fr(x)p Ft(,)e(so)h(in)f(particular)h Fr(f)t Ft(\()p Fr(x)1341 1166 y Fm(0)1360 1160 y Ft(\))e Fs(\024)g Fr(f)t Ft(\()p Fr(x)1496 1166 y Fm(0)1524 1160 y Ft(+)e(1\).)320 1210 y(Next)j(w)o(e)g(need)h(to)e(pro)o(v)o(e)h(the)g(minim)n(um)c (principle)j(from)f(ordinary)h(zero-success)q(or-)257 1260 y(induction.)18 b(The)c(minim)n(um)c(principle)637 1347 y Fs(9)p Fr(k)e(R)p Ft(\()p Fr(k)q Ft(\))k Fs(!)f(9)p Fr(k)q(:R)p Ft(\()p Fr(k)q Ft(\))e Fs(^)f(8)p Fr(l)q(<)q(k)q(:R)p Ft(\()p Fr(l)q Ft(\))j Fs(!)g(?)306 b Ft(\(14\))257 1434 y(is)14 b(to)g(b)q(e)g(applied)g(with)f Fr(R)p Ft(\()p Fr(k)q Ft(\))f(:=)f Fr(k)i Fs(2)e Fk(ran)p Ft(\()p Fr(f)t Ft(\).)19 b(No)o(w)c(\(14\))e(is)h(logically)d(equiv)n(alen)o(t)j(to) 505 1521 y Fs(8)p Fr(k)551 1488 y Fd(\000)570 1521 y Fr(R)p Ft(\()p Fr(k)q Ft(\))e Fs(!)f(8)p Fr(l)q(