%!PS-Adobe-2.0 %%Creator: dvipsk 5.58f Copyright 1986, 1994 Radical Eye Software %%Title: mod99ios.dvi %%Pages: 20 %%PageOrder: Ascend %%BoundingBox: 0 0 596 842 %%EndComments %DVIPSCommandLine: dvips mod99ios.dvi %DVIPSParameters: dpi=300, compressed, comments removed %DVIPSSource: TeX output 2000.01.10:1234 %%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 (mod99ios.dvi) @start /Fa 49 122 df<121C123E127EA2123A12021204A21208A21210122012401280 070E769F0E>39 D<130113021304130813101320136013C0EA0180A2EA03005A1206120E 120C121C12181238A212301270A21260A212E0A25AAD12401260A212207EA27E102E79A1 13>I<13107F7F130613021303A37F1480A71303A31400A35BA21306A2130E130CA2131C 1318133813301370136013E05B485A90C7FC5A12065A5A5A5A1280112E80A113>I<121C 123CA41204A21208A212101220A212401280060E7D840E>44 DI<127012F8A212F012E005057B840E>I<1302A21306130E133C13DCEA031C1200 1338A41370A413E0A4EA01C0A4EA0380A41207EAFFF80F1E7B9D17>49 D51 D53 D<131FEB7180EBC0C0EA0180000313E0EA07005A130112 1EA314C0EA1C03A31307EB0F80120CEA06373803C700EA000F130EA25B1260EAF0385BEA E060EA80C0EA4380003EC7FC131F7B9D17>57 D<1207120F121FA2120E1200AA127012F8 A212F012E008147B930E>I<14021406A2140E141EA2143F142F144F14CF148FEB010FA2 1302A213041308A20110138014071320EB3FFFEB40071380A2EA0100A212021206120400 1E14C039FF807FF81D207E9F22>65 D67 D<48B512FE39001E001C150C 1504A25BA490387804081500A2140C495AEBFFF8EBF018A23801E010A3EC001048481320 A21540A248481380140115001407380F001FB512FE1F1F7D9E1F>69 D<48B512FC39001E003815181508A25BA4491310EC0800A3495A1430EBFFF0EBF0303801 E020A44848C7FCA4485AA4120FEAFFF81E1F7D9E1E>I<9039FFF1FFE090391F003E0001 1E133CA3495BA4495BA449485A90B5FCEBF001A24848485AA44848485AA4484848C7FCA4 000F5B39FFF1FFE0231F7D9E22>72 D<3801FFF038001F00131EA35BA45BA45BA4485AA4 485AA4485AA4120FEAFFF0141F7D9E12>I<90380FFF809038007C001478A35CA4495AA4 495AA4495AA449C7FCA212301278EAF81EA2485AEA8038EA40706C5AEA1F8019207D9E18 >I<9039FFF01FE090391F000F80011EEB0E0015085D495B5D4AC7FC1402495A5C5C1430 EBF0F0EBF1F8EBF27813F448487E13F013E080EA03C0A280A2EA07806E7EA3000F8039FF F03FF8231F7D9E23>I<3801FFF8D8001FC7FC131EA35BA45BA45BA4485AA315803903C0 0100A25C140238078006A25C141C380F0078B512F8191F7D9E1D>II<01FFEB3FE0011FEB0F001504EB1780A201 275BEB23C0A3903841E010A214F0134001805B1478A348486C5AA3141E00025CA2140FA2 4891C7FC80A2120C001C1302EAFF80231F7D9E22>I<48B5128039001E00E01570153815 3C5BA4491378A215F015E09038F003C0EC0F00EBFFFC01F0C7FC485AA4485AA4485AA412 0FEAFFF01E1F7D9E1F>80 D<903807E04090381C18C09038300580EB600313C000011301 018013001203A391C7FC7FA213F86CB47E14E06C6C7E131FEB01F8EB0078A21438A21220 A2143000601370146014E000705B38E80380D8C606C7FCEA81F81A217D9F1A>83 D<000FB512FC391E03C03800181418001014081220EB078012601240A239800F00100000 1400A3131EA45BA45BA45BA41201387FFF801E1F799E21>I<3BFFE1FFC07F803B1F003E 001C00001E013C13181610143E021E5B121F6C013E5BA2025E5B149E4BC7FC9038011E02 A201025BA201045BA201085BA201105B13205D01405BA2D9801FC8FC80EB000E7E000613 0CA2000413082920779E2D>87 D<39FFF003FC001FC712E06C14C06D1380EC0100000713 026D5AA200035B6D5A5C00011360EBF0405CD800F1C7FC13FA13FE137C1378A2137013F0 A35B1201A4485AEA3FFC1E1F779E22>89 D 97 DI<137EEA01C138030080EA 0E07121E001C1300EA3C0248C7FCA35AA5EA70011302EA3004EA1838EA07C011147C9315 >I<1478EB03F8EB0070A414E0A4EB01C0A213F1EA038938070780EA0E03121C123C3838 07001278A3EAF00EA31420EB1C40A2EA703C135C38308C80380F070015207C9F17>I<13 7CEA01C2EA0701120E121C123CEA3802EA780CEA7BF0EA7C0012F0A4127013011302EA38 04EA1838EA07C010147C9315>I<1478EB019CEB033CA2EB07181400A2130EA5EBFFE0EB 1C00A45BA55BA55BA5485AA35B1231007BC7FC12F31266123C1629829F0E>III<13C0EA01E0A213C0 C7FCA7120E12131223EA4380EA4700A21287120EA35AA3EA38401380A21270EA31001232 121C0B1F7C9E0E>I107 DI<391C0F80F0392630C318394740640C903880680E EB0070A2008E495A120EA34848485AA3ED70803A3803807100A215E115623970070064D8 3003133821147C9325>I<381C0F80382630C0384740601380EB0070A2008E13E0120EA3 381C01C0A3EB038400381388A2EB0708EB031000701330383001C016147C931A>I<137C EA01C338030180000E13C0121E001C13E0123C1278A338F003C0A3EB07801400EA700F13 0EEA3018EA1870EA07C013147C9317>I<3801C1E0380262183804741C1378EB701EA2EA 08E01200A33801C03CA3143838038078147014E0EBC1C038072380EB1E0090C7FCA2120E A45AA2B47E171D809317>III<13FCEA0302EA0601EA0C03130713061300EA0F8013F0EA07F8EA03FCEA003E130E12 70EAF00CA2EAE008EA4010EA2060EA1F8010147D9313>II<00 0E13C0001313E0382301C0EA4381EA4701A238870380120EA3381C0700A31410EB0E2012 18A2381C1E40EA0C263807C38014147C9318>I<380E0380EA1307002313C0EA4383EA47 01130000871380120EA3381C0100A31302A25BA25BEA0E30EA03C012147C9315>I<000E 13C0001313E0382301C0EA4381EA4701A238870380120EA3381C0700A4130E1218A2EA1C 1EEA0C3CEA07DCEA001CA25B12F05BEAE060485AEA4380003EC7FC131D7C9316>121 D E /Fb 71 128 df<133FEBE0C0EA01C0380381E0EA0701A290C7FCA6B512E0EA0700B2 383FC3FC1620809F19>12 D34 D<13401380EA01005A12061204120C5AA212381230A2 12701260A412E0AC1260A412701230A212381218A27E120412067E7EEA008013400A2E7B A112>40 D<7E12407E12307E1208120C7EA212077EA213801201A413C0AC1380A4120313 00A25A1206A25A120812185A12205A5A0A2E7EA112>I<127012F012F8A212781208A312 10A31220A21240050E7C840D>44 DI<127012F8A3127005057C 840D>I48 D<13801203120F12F31203B3A6EA 07C0EAFFFE0F1E7C9D17>III<1306A2130EA2131E132EA2134E138EA2EA 010E1202A212041208A212101220A2124012C0B512F038000E00A7EBFFE0141E7F9D17> II<137CEA 0182EA0701380E0380EA0C0712183838030090C7FC12781270A2EAF1F0EAF21CEAF406EA F807EB0380A200F013C0A51270A214801238EB07001218EA0C0E6C5AEA01F0121F7E9D17 >I<1240387FFFE014C0A23840008038800100A21302485AA25B5BA25BA21360A213E05B 1201A41203A76C5A131F7E9D17>III<127012F8A312 701200AA127012F8A3127005147C930D>I<5B497EA3497EA3EB09E0A3EB10F0A3EB2078 A3497EA2EBC03EEB801EA248B5FCEB000FA20002EB0780A348EB03C0A2120C001E14E039 FF801FFE1F207F9F22>65 D I<90380FE0109038381C309038E002703803C00139078000F048C71270121E15305A1510 127C127800F81400A91278007C1410123CA26C1420A27E6C6C13406C6C13803900E00300 EB380CEB0FF01C217E9F21>IIII<90380FE0109038381C309038E002703803C00139078000F048C71270121E15 305A1510127C127800F81400A7EC3FFEEC01F000781300127C123CA27EA27E6C7E3903C0 01703900E002309038380C1090380FF0001F217E9F24>I<39FFF07FF8390F000780AD90 B5FCEB0007AF39FFF07FF81D1F7E9E22>II<38 07FFC038003E00131EB3A3122012F8A3EAF01CEA403CEA6038EA1070EA0FC012207F9E17 >I<39FFF007FC390F0003E0EC0180150014025C5C5C5C5C5C49C7FC5B497E130FEB13C0 EB21E01341EB80F0EB0078A28080A280EC0780A2EC03C015E015F039FFF01FFE1F1F7E9E 23>II< B46CEB07FE000715C0A2D805C0130BA2D804E01313A301701323A26D1343A36D1383A290 380E0103A3EB0702A3EB0384A2EB01C8A3EB00F0A21460121FD8FFE0EB7FFE271F7F9E2A >IIII82 D<3803F040380C0CC0EA1803EA3001EA6000A212E01440A36C13007E127CEA7F80EA3FF8 6CB4FC00071380C613C0EB1FE013031301EB00F014707EA46C136014E06C13C038F80180 38C60300EA81FC14217E9F19>I<007FB512E038780F010060EB006000401420A200C014 3000801410A400001400B3497E3803FFFC1C1F7E9E21>I<39FFF00FF8390F0003E0EC00 80B3A46CEB01001380120314026C6C5A6C6C5AEB3830EB0FC01D207E9E22>I<39FFF003 FE391F8000F86CC7126015206C6C1340A36C6C1380A2EBE00100011400A23800F002A213 F8EB7804A26D5AA36D5AA2131F6D5AA2EB07C0A36D5AA36DC7FC1F207F9E22>I<3BFFF0 7FF81FF03B1F000FC007C06C903907800180170015C001805C00071502EC09E013C00003 5DEC19F01410D801E05CA2EC2078D800F05CA2EC403C01785CA2EC801E017C1460013C14 4090383D000F133F6D5CA2011E1307010E91C7FCA2010C7F010413022C207F9E2F>I<39 FFF001FF391F800078000F146012076D1340000314807F3901F001001200EBF802EB7C06 EB3C04EB3E08131EEB1F10EB0FB0EB07A014E06D5AACEB3FFC201F7F9E22>89 D<12FFA212C0B3B3A512FFA2082D7CA10D>91 DI<12FFA21203B3B3A512FFA2082D80 A10D>I97 D<121C12FC121CAA137CEA1D87381E 0180EB00C0001C13E01470A21478A6147014F014E0001E13C0381A018038198700EA107C 15207E9F19>III< EA03F0EA0E1C487E487EA21270EB038012F0A2B5FC00F0C7FCA31270A26C1380A2381C01 00EA0706EA01F811147F9314>I<137CEA01C6EA030F1207EA0E061300A7EAFFF0EA0E00 B2EA7FE01020809F0E>I<14E03803E330EA0E3CEA1C1C38380E00EA780FA5EA380E6C5A EA1E38EA33E00020C7FCA21230A2EA3FFE381FFF8014C0383001E038600070481330A400 6013606C13C0381C03803803FC00141F7F9417>I<121C12FC121CAA137C1386EA1D0300 1E1380A2121CAE38FF8FF014207E9F19>I<1238127CA31238C7FCA6121C12FC121CB1EA FF80091F7F9E0C>I<121C12FC121CAAEB1FE0EB0780EB060013045B5B5B136013E0EA1D F0EA1E70EA1C38133C131C7F130F7F148014C038FF9FF014207E9F18>107 D<121C12FC121CB3ABEAFF8009207F9F0C>I<391C3E03E039FCC30C30391D039038391E 01E01CA2001C13C0AE3AFF8FF8FF8021147E9326>IIII<3801F04038070CC0EA0E02EA1C03EA380112781270 12F0A6127012781238EA1C03EA0C05EA0709EA01F1EA0001A8EB0FF8151D7F9318>III<1202A31206A2120EA2123EEAFFF8EA0E00AB1304A5EA07081203EA 01F00E1C7F9B12>I<381C0380EAFC1FEA1C03AE1307120CEA061B3803E3F014147E9319> I<38FF83F8383E00E0001C13C06C1380A338070100A21383EA0382A2EA01C4A213E4EA00 E8A21370A3132015147F9318>I<39FF9FE1FC393C078070391C030060EC8020000E1440 A214C0D80704138014E0A239038861001471A23801D032143A143E3800E01CA2EB6018EB 40081E147F9321>I<38FF87F8381E03C0380E0180EB0300EA0702EA0384EA01C813D8EA 00F01370137813F8139CEA010E1202EA060738040380000C13C0003C13E038FE07FC1614 7F9318>I<38FF83F8383E00E0001C13C06C1380A338070100A21383EA0382A2EA01C4A2 13E4EA00E8A21370A31320A25BA3EAF080A200F1C7FC1262123C151D7F9318>III127 D E /Fc 7 116 df82 D99 D101 DI<38FE0FC0 EB3FE0381E61F0EBC0F81380EA1F00AD38FFE7FFA218147D931D>110 D114 DI E /Fd 27 120 df<1218123C123E121E120EA5121CA2123812F812F01260070F779D1A>39 D<1338137813F0EA01E0EA03C0EA0780EA0F00120E5AA25AA25AA35AAA1270A37EA27EA2 7E120FEA0780EA03C0EA01E0EA00F8137813380D2878A21A>I<126012F012787E7E7EEA 07801203EA01C0A2EA00E0A21370A31338AA1370A313E0A2EA01C0A2EA03801207EA0F00 121E5A5A5A12600D287CA21A>I<1218123E127E127F123F121F1207120EA2121C12FC12 F81260080D77851A>44 D<387FFFC0B512E0A26C13C013047D901A>I48 D<13C01201A212031207 120F127F12FD12711201B2EA7FFFA3101E7B9D1A>II<14C0EB03E01307EB0F C0EB3F80EB7E005BEA03F8EA07E0485AEA3F80007EC7FC5AA2127E6C7EEA0FC06C7EEA03 F8C67E137EEB3F80EB0FC0EB07E01303EB00C0131A7D9B1A>60 D97 D<127E12FE127E120EA6133EEBFF80000F13E0EBC1 F0EB8070EB0038120E141CA7000F13381478EB80F0EBC1E0EBFFC0000E138038063E0016 1E7F9D1A>IIIII<13C0487EA26C5A90C7FCA6EA7F E0A31200AF387FFF80B512C06C1380121F7C9E1A>105 D<12FEA3120EA6EB0FFC131F13 0FEB03C0EB0780EB0F00131E5B5B13FC120F13DE138F380E07801303EB01C014E0EB00F0 38FFE3FEA3171E7F9D1A>107 DI<387CE0E038FFFBF8EA7FFF381F1F1CEA1E1EA2EA1C1CAC387F1F1F39FFBF BF80397F1F1F00191580941A>IIII<387F81F838FF8FFC387F9FFE3803FE1EEBF80CEBE000A25B5BAAEA7FFFB5FC7E17 157F941A>114 D<3807FB80EA1FFF127FEA7807EAE003A30078C7FCEA7FC0EA1FFCEA07 FE38003F801307386001C012E0A2EAF00338FC0780B51200EAEFFEEAE3F812157C941A> I<487E1203A6387FFFE0B5FCA238038000AA1470A43801C1E013FF6C1380EB3F00141C7F 9B1A>I<387E07E0EAFE0FEA7E07EA0E00AD1301EA0F033807FFFC6C13FE3800FCFC1715 7F941A>I<38FF83FEA338380038A26C1370A31338137CA2380C6C60380EEEE0A413C600 0613C0EA07C71383A217157F941A>119 D E /Fe 1 79 df<39FFE00FF8393010032039 0808014090380400C0120CEA0E02EA0D01380C8080EB4040A2EB2020EB1010EB0808EB04 04A2EB0202EB0101EB0080EC40401420A2141014081404140200121301123339FFC000C0 C812401D1D809B20>78 D E /Ff 12 126 df<1306130C131813301370136013C0120113 80120313005A1206120E120C121CA212181238A312301270A65AB21270A612301238A312 18121CA2120C120E120612077E1380120113C012001360137013301318130C13060F4A78 8119>16 D<12C012607E7E121C120C7E12077E1380120113C0120013E013601370A21330 1338A31318131CA6130EB2131CA613181338A313301370A2136013E013C0120113801203 13005A12065A121C12185A5A5A0F4A7F8119>I<1470EB01F0EB03C0EB0780EB0E005B5B 5BA213F05BB3AC485AA3485A48C7FC1206120E12385A12C012707E120E120612076C7E6C 7EA36C7EB3AC7F1370A27F7F7FEB0780EB03C0EB01F0EB007014637B811F>26 D<141C143C14F8EB01E0EB03C0EB0780EB0F00130E131E5BA35BB3B3A25BA3485AA2485A 5B48C7FC120E5A127812E0A21278121C7E7E6C7E7F6C7EA26C7EA31378B3B3A27FA37F13 0E130FEB0780EB03C0EB01E0EB00F8143C141C167C7B8121>40 D<1318137813F0EA01E0 EA03C0EA0780EA0F005A121E123E123C127CA2127812F8B3A50D25707E25>56 D<12F8B3A51278127CA2123C123E121E121F7EEA0780EA03C0EA01E0EA00F0137813180D 25708025>58 D<137CB3A613F8A313F0120113E0120313C0EA07801300120E5A5A12F012 C012F012387E7E7E1380EA03C013E0120113F0120013F8A3137CB3A60E4D798025>60 D<12F8AE050E708025>62 D122 D<12FCB47E13E013F813FEEA01FF38001F80EB07C0EB01E0 EB00F0147014381418150D818413>I<12C07E126012707E121E6C7EEA07E0EA03FE3801 FFF87E133F130F1301150E818D13>I<141814381430147014E0EB03C0EB0F80EB3F00EA 03FEB45A5B13E0138000FCC7FC150E818D13>I E /Fg 5 109 df26 D<1304130EA213161326A2134613871383EA010348B4FCEA020312041208EB0180121038 FC0FE013117E9017>65 D<1204120C1200A5123012581298A21230A212601264A2126812 3006127E910B>105 D<123C120CA25AA31370EA3190EA3230EA34001238127FEA618013 90A2EAC1A0EAC0C00C117E9010>107 D<12781218A21230A41260A412C0A212C8A212D0 126005117E900A>I E /Fh 4 53 df<121FEA3180EA60C0EA4040EAC060A8EA4040EA60 C0EA3180EA1F000B107F8F0F>48 D<1218127812981218AC12FF08107D8F0F>I<121FEA 6180EA40C0EA806012C01200A213C0EA0180EA030012065AEA10201220EA7FC012FF0B10 7F8F0F>I52 D E /Fi 29 119 df<120112021204120C1218A21230A212701260A312E0 AA1260A312701230A21218A2120C12041202120108227D980E>40 D<12801240122012301218A2120CA2120E1206A31207AA1206A3120E120CA21218A21230 12201240128008227E980E>I<1330ABB512FCA238003000AB16187E931B>43 D48 D<1206120E12FE120EB1EAFFE00B157D9412>III<1330 A2137013F012011370120212041208121812101220124012C0EAFFFEEA0070A5EA03FE0F 157F9412>III<1240EA7FFE13FC13F8EAC008EA80101320EA00401380A2EA01005AA2 12021206A2120EA512040F167E9512>I<126012F0A212601200A6126012F0A21260040E 7D8D0A>58 D61 D<12FCA212C0B3AB12FCA206 217D980A>91 D<12FCA2120CB3AB12FCA2062180980A>93 D97 D<12F81238A8EA39F0EA3E0CEA380613077F1480A414005B1306EA361CEA21F011177F96 14>II<133E130EA8EA07CEEA1C3EEA300E1270126012E0A412601270EA301EEA182E38 07CF8011177F9614>II103 D<12301278A212301200A512F81238AC12FE07177F960A>105 D110 DII114 DI<1208A31218A21238EAFF C0EA3800A71340A4EA1C80EA0F000A147F930E>I118 D E /Fj 37 127 df<130FEB3080EBC0C0380100401460000213C05A1480130138083F00133E1301 14801210A438300300A21306EA280CEA4418EA43E00040C7FCA25AA4131D7F9614>12 D17 D<12081218A31230A31260A2126112C112C212441278080E7E8D0C>19 D22 D<13F0EA0318EA0608EA0C0CA21218A3EA3018A213301320EA68C0EA6780EA60 00A25AA35A0E147E8D12>26 D<3803FF805A381C3000EA181812301260A3485AA2EA4060 EA6040EA2180001EC7FC110E7F8D14>II<001013204813305AA2388020201360A21460EB4040EBC0C038 81C18038E76700EA7E7EEA3C3C140E7F8D16>33 D<126012F0A2126004047D830A>58 D<126012F0A212701210A21220A21240A2040A7D830A>I<143014F0EB03C0EB0700131C 1378EA01E0EA0780000EC7FC123812F0A21238120E6C7EEA01E0EA0078131C1307EB03C0 EB00F0143014167D921B>I<14C0A21301A21303130514E01308131813101320A2134013 80A23801FFF0EB007012025AA25A121838FE03FE17177F961A>65 D<3807FFF83800E00E14071403A2EA01C01407A2140E3803803CEBFFF0A2EB803C380700 1C140EA3000E131CA214381470381C01E0B5120018177F961B>II<3807FFF83800E00E140315801401D801C013C0 A21400A238038001A43907000380A215005C000E130E140C5C1470381C01C0B5C7FC1A17 7F961D>I71 D<13301348138812011308EA0310120212061320EA0C40A21380EA0D00121A121C1218A2 123812581288EA0810EA0C60EA07800D1780960E>96 DI99 D<130E131313371336133013 60A4EA03FCEA00C0A5EA0180A5EA0300A41202126612E65A1278101D7E9611>102 D<13E2EA031EEA060E120C130C1218A3EA1018A3EA1838EA08F0EA07301200A2EA606012 E0EAC1C0EA7F000F14808D11>I<120313801300C7FCA6121C12241246A25A120C5AA312 31A21232A2121C09177F960C>105 D<1318133813101300A6EA01C0EA0220EA0430A2EA 08601200A313C0A4EA0180A4EA630012E312C612780D1D80960E>I<121F1206A45AA4EA 181C1366138EEA190CEA3200123C123FEA3180EA60C013C4A3EAC0C813700F177E9612> I<123E120CA41218A41230A41260A412C012C8A312D0127007177E960B>I<38383C1E38 44C6633847028138460301388E0703EA0C06A338180C061520140C154039301804C0EC07 001B0E7F8D1F>II112 DII<1203A21206A4EAFFC0EA0C00A35A A45A1380A2EA31001232121C0A147F930D>116 DII<381C0204382606061246A238860C04 120CA338181808A214101208380C2C203803C7C0170E7F8D19>II122 D<13201330A2EAFFFCA2EA007013E013400E08799712>126 D E /Fk 4 115 df<3807FFFC3800F80F9038F0038015C01401A33801E003A31580EC07 00140E3803C03CEBFFE001C0C7FCA4485AA648C8FC7FEAFFF01A1C7E9B1C>80 D<1438EB7CCC3801871C3803030800071380120EA4EB0700EA0606EA070CEA09F00008C7 FC1218A2EA1FFE380FFF8014C0EA3001EA600014E04813C0A23860018038200300EA180E EA07F0161C809215>103 D<13FCEA0307380E0180001C13C0EA38001230007013E0A338 E001C0A300601380130338700700EA380EEA1C18EA07E013127E9115>111 D114 D E /Fl 21 118 df<14041406140E141EA2143E143F144FA2148FA29038010F80140713 02A2130481EB0803A21310A2132090383FFFE0EB400113C01380EA01008100021300A25A A2000C80003E13013AFF800FFF8021237EA225>65 D<0007B512FE39007C003E0178131C 150C1504A35BA314041500140C3801E008A21438EBFFF8EBE03814183803C010A491C7FC A2485AA6120FA2EAFFFC1F227DA120>70 D<3A07FFC1FFF03A007C001F000178131EA549 5BA648485BA390B512F89038E00078A248485BA64848485AA64848485A01807F39FFF83F FE24227DA125>72 D<3807FFC038007C001378A55BA6485AA6485AA6485AA648C7FC7FEA FFF812227DA112>I<0007B5128039007C01E090387800F01578A2157CA25BA4157815F8 484813F0EC01E0EC03C0EC0F00EBFFFC01E0C7FC485AA6485AA648C8FC7FEAFFF81E227D A121>80 D<001FB512FE393C03E03E0038EBC00C00301404122012601240EB078012C012 80A200001400A249C7FCA6131EA65BA6137C13FC381FFFF01F227AA123>84 D86 D97 DI<141E 14FE141CA61438A6EB7C70EA0383380700F0120C001C13705A007813E0127012F0A438E0 01C0A4EA7003A238380F80381C33C03807C3F817237CA21B>100 D<13FE38038380380701C0380C00E0121C5A12781270B5FC00F0C7FCA45AA26C13400070 1380123038380300EA0E0CEA03F013157D9416>III<1378EA03F8EA0070A613E0A6EA01C0A6EA0380A6EA07 00A6120E120FEAFFE00D237FA20E>108 D<3A01C1F807E03A0FC60C18303A01D80E6038 9039E007801CA201C013000003491338EB800EA54848481370A6000E4913E0000F013C13 F03AFFE3FF8FFE27157F942A>I<3801C3F0380FCC183801D00CEBE00EA213C00003131C 1380A538070038A6000E1370000F137838FFE7FF18157F941B>I<137E38038380380600 C04813E0001C13705A00781378127012F0A44813F0A214E0EAF001007013C0EB03803838 0700EA1C1CEA07F015157D9418>I<3801C3C0380FCCE0EA01D113E1EBE0C0EBC0001203 5BA548C7FCA6120E120FEAFFF013157F9413>114 DI<1380A3120113005AA25A5A5AEAFFFCEA0E00A55AA6EA3810A51320A2EA 1C40EA07800E1F7C9E13>I<001C13E0EAFC07EA1C00A4383801C0A638700380A4130713 0BEB170038382780380FC7F014157B941B>I E /Fm 6 112 df77 D 103 D105 D108 D<00FEEB3F80001FEB0E00EB80041217 EA13C0EA11E013F012101378137C133C131E130F14841307EB03C4EB01E4A2EB00F4147C A2143C141C140C123800FE1304191A7E991F>110 DI E /Fn 49 128 df12 D<120C121E123FA2121D1202A31204A212081210122012401280080F75A20F>39 D<120E121EA41202A21204A21208A21210122012401280070F7D840F>44 DI<127012F8A212F012E005057A840F>I<13011303A21306 131E132EEA03CEEA001CA41338A41370A413E0A4EA01C0A4EA0380A41207EAFFFC10217A A019>49 DII<1207EA0F80A21300120EC7FCAB127012F8A25A5A09157A 940F>58 D<1403A25CA25CA25C142FA2EC4F80A21487A2EB01071302A21304A213081318 13101320A290387FFFC0EB40031380EA0100A21202A25AA2120C003CEB07E0B4EB3FFC1E 237DA224>65 D<90B512E090380F0038151C151E011E130E150FA349130E151EA2153C49 13781570EC01E0EC078090B5FC9038F001E0EC00F01578485A1538153CA248481378A315 F0485AEC01E0EC03C0EC0700380F001EB512F020227DA122>I<027F1380903903808100 90380E00630138132749131F49130E485A485A48C7FC481404120E121E5A5D4891C7FCA3 5AA55A1520A25DA26C5C12704AC7FC6C130200185B001C5B00061330380381C0D800FEC8 FC212479A223>I<90B512F090380F003C150E81011EEB0380A2ED01C0A25B16E0A35BA4 49EB03C0A44848EB0780A216005D4848130E5D153C153848485B5DEC03804AC7FC000F13 1CB512F023227DA125>I<90B6128090380F00071501A2131EA21600A25BA2140192C7FC EB7802A21406140EEBFFFCEBF00CA33801E008A21504EC0008485AA25DA248485B15605D 1401380F0007B65A21227DA121>I<90B6FC90380F000F1503A2131EA21502A25BA21401 1500EB7802A21406140EEBFFFCEBF00CA33801E008A391C7FC485AA4485AA4120FEAFFF8 20227DA120>I<027F138090390380810090380E00630138132749131F49130E485A485A 48C7FC481404120E121E5A5D4891C7FCA35AA4EC3FFC48EB01E0A34A5AA27E12704A5A7E 0018130F001C131300060123C7FC380381C1D800FEC8FC212479A226>I<9039FFF87FFC 90390F000780A3011EEB0F00A449131EA4495BA490B512F89038F00078A348485BA44848 485AA44848485AA4000F130739FFF07FF826227DA124>II76 D<90B512E090380F0038151E150E011E1307A449130FA3151E5B15 3C157815E09038F003C09038FFFE0001F0C7FCA2485AA4485AA4485AA4120FEAFFF02022 7DA121>80 D<90B512C090380F0070153C151C011E130EA2150FA249131EA3153C491338 1570EC01E0EC07809038FFFC00EBF00E80EC0380D801E013C0A43903C00780A43907800F 001501A2EC0702120F39FFF0038CC812F020237DA124>82 D<903801F02090380E0C4090 381802C0EB3001136001E0138013C01201A200031400A291C7FCA27FEA01F813FF6C13E0 6D7EEB1FF8EB03FCEB007C143C80A30020131CA3141800601338143000705B5C38C80180 D8C607C7FCEA81FC1B247DA21B>I<001FB512F8391E03C03800181418123038200780A2 00401410A2EB0F001280A200001400131EA45BA45BA45BA4485AA41203B5FC1D2277A123 >I97 DI<137EEA01C138030180EA0703EA0E07121C003CC7FC12 381278A35AA45B12701302EA300CEA1830EA0FC011157B9416>I<143CEB03F8EB0038A3 1470A414E0A4EB01C013F9EA0185EA0705380E0380A2121C123C383807001278A3EAF00E A31410EB1C201270133C38305C40138C380F078016237BA219>I<13F8EA0384EA0E0212 1C123C1238EA7804EAF018EAFFE0EAF000A25AA41302A2EA6004EA7018EA3060EA0F800F 157A9416>I<143E144714CFEB018F1486EB0380A3EB0700A5130EEBFFF0EB0E00A35BA5 5BA55BA55BA45B1201A2EA718012F100F3C7FC1262123C182D82A20F>II<13F0EA0FE01200 A3485AA4485AA448C7FC131FEB2180EBC0C0380F00E0A2120EA2381C01C0A438380380A3 EB070400701308130E1410130600E01320386003C016237DA219>I<13C0EA01E013C0A2 C7FCA8121E12231243A25AA3120EA25AA35AA21340EA7080A3EA71001232121C0B217BA0 0F>I<13F0EA07E01200A3485AA4485AA448C7FCEB01E0EB0210EB0470380E08F01310EB 2060EB4000EA1D80001EC7FCEA1FC0EA1C70487EA27F142038703840A3EB188012E03860 0F0014237DA216>107 DI<391C0F80F8392610C10C394760660639878078 07A2EB0070A2000EEBE00EA44848485AA3ED38202638038013401570168015303A700700 3100D83003131E23157B9428>I<38380F80384C30C0384E4060388E8070EA8F00128EA2 4813E0A4383801C0A3EB03840070138814081307EB031012E0386001E016157B941B>I< 137EEA01C338038180380701C0120E001C13E0123C12381278A338F003C0A21480130700 701300130E130CEA3018EA1870EA07C013157B9419>I<3801C1F0380262183804741C38 08780CEB700EA2141EEA00E0A43801C03CA3147838038070A2EBC0E0EBC1C038072380EB 1E0090C7FCA2120EA45AA3EAFFC0171F7F9419>III<13FCEA018338020080EA0401EA0C03140090C7FC120F13F0EA 07FC6C7EEA003E130F7F1270EAF006A2EAE004EA4008EA2030EA1FC011157D9414>I<13 C01201A4EA0380A4EA0700EAFFF8EA0700A2120EA45AA45AA31310EA7020A213401380EA 3100121E0D1F7C9E10>I<001E1360002313E0EA4380EB81C01283EA8701A23807038012 0EA3381C0700A31408EB0E101218121CEB1E20EA0C263807C3C015157B941A>I<381C01 80382603C0EA47071303EA8701EA8E00A2000E13805AA338380100A31302A25B5B1218EA 0C30EA07C012157B9416>I<001EEB60E00023EBE0F0384380E1EB81C000831470D88701 1330A23907038020120EA3391C070040A31580A2EC0100130F380C0B02380613843803E0 F81C157B9420>I<3803C1E0380462103808347038103CF0EA203814601400C65AA45BA3 14203861C04012F1148038E2C100EA4462EA383C14157D9416>I<001E133000231370EA 438014E01283EA8700A2380701C0120EA3381C0380A4EB0700A35BEA0C3EEA03CEEA000E A25B1260EAF0381330485AEA80C0EA4380003EC7FC141F7B9418>I<3801E0203803F060 3807F8C038041F80380801001302C65A5B5B5B5B5B48C7FC120248138038080100485AEA 3F06EA61FEEA40FCEA807013157D9414>I 127 D E /Fo 18 123 df45 D<127012F8A312700505788416> I<13F8EA03FC487EEA0F07381C3B80EA38FF12793873C7C01383EAE701A73873838013C7 3879FF00EA38FEEA1C38380F03C0EA07FF6C1300EA00FC12197E9816>64 D97 D99 D<133FA31307A4EA03C7EA0F F748B4FCEA3C1F487EEA700712E0A6EA700F12786C5A381FFFE0EA0FF7EA07C713197F98 16>II<12FCA3121CA41378EA1DFCEA1FFE130F EA1E07121CAA38FF8FE0139F138F13197F9816>104 D<1203EA0780A2EA0300C7FCA4EA FF80A31203ACEAFFFC13FE13FC0F1A7C9916>I<127E12FE127E120EA4EB7FE0A3EB0F00 131E5B5B5B120F7F13BC131EEA0E0E7F1480387F87F0EAFFCFEA7F871419809816>107 D<38F9C38038FFEFC0EBFFE0EA3C78A2EA3870AA38FE7CF8A31512809116>109 DI<387F0F C038FF3FE0EA7F7F3807F040EBC0005BA290C7FCA8EA7FFC12FF127F13127F9116>114 DI<12035AA4EA7FFFB5FCA20007C7FCA75B EB0380A3EB8700EA03FE6C5A6C5A11177F9616>II<38FF1FE0A338380380A4EA39F3A20019130013B3A3EA1DB7 1317EA1F1FEA0F1EEA0E0E13127F9116>119 D<383FFFC05AA238700780EB0F00131EC6 5A5B485A485AEA078048C7FC381E01C0123C1278B5FCA312127F9116>122 D E /Fp 38 128 df25 D<1306ADB612E0A2D80006C7FCAD1B1C7E9720>43 D<126012F0A212701210A41220A212 401280040C7C830C>II<126012F0A2126004047C830C>I48 D<5A1207123F12C71207B3A5EAFFF80D1C7C9B15>III<130CA2131C 133CA2135C13DC139CEA011C120312021204120C1208121012301220124012C0B512C038 001C00A73801FFC0121C7F9B15>II56 DI68 D70 D<90381F8080EBE0613801801938070007000E13035A14015A00781300A2127000F01400 A6ECFFF0EC0F80007013071278A212387EA27E6C130B380180113800E06090381F80001C 1E7E9C21>I73 D77 D80 D<007FB512C038700F010060 130000401440A200C014201280A300001400B1497E3803FFFC1B1C7F9B1E>84 D<39FFF01FF0390F000380EC0100B3A26C1302138000035BEA01C03800E018EB7060EB0F 801C1D7F9B1F>I97 D99 DII<12FC121CAA137C1387 EA1D03001E1380121CAD38FF9FF0141D7F9C17>104 D<1218123CA21218C7FCA712FC12 1CB0EAFF80091D7F9C0C>I<39FC7E07E0391C838838391D019018001EEBE01C001C13C0 AD3AFF8FF8FF8021127F9124>109 DII114 DI<1204A4120C A2121C123CEAFFE0EA1C00A91310A5120CEA0E20EA03C00C1A7F9910>I<38FC1F80EA1C 03AD1307120CEA0E1B3803E3F014127F9117>I<38FF07E0383C0380381C0100A2EA0E02 A2EA0F06EA0704A2EA0388A213C8EA01D0A2EA00E0A3134013127F9116>I<38FF0FE038 1E0700EA1C06EA0E046C5AEA039013B0EA01E012007F12011338EA021C1204EA0C0E487E 003C138038FE1FF014127F9116>120 D<38FF07E0383C0380381C0100A2EA0E02A2EA0F 06EA0704A2EA0388A213C8EA01D0A2EA00E0A31340A25BA212F000F1C7FC12F312661238 131A7F9116>I127 D E /Fq 1 4 df<1204A3EAC460EAF5E0EA3F80EA0E00EA3F80EAF5E0EAC460EA0400A30B0D7E8D 11>3 D E /Fr 53 127 df<143EECC18090380300C013044913E05BA25B5BEC01C01380 158014033901000700EB01FEEB021CEB03EE38020007A21580A25AA448EB0F00A2140E14 1E0014131C5C00125B00135B382081C0017EC7FC90C8FCA25AA45AA41B2D7FA21C>12 D<12035AA2120EA45AA35AA35A1308131012E01320EA6040EA6180EA3E000D157E9411> 19 D21 DI<000FB5FC5A 5A3870418000401300EA8081A21200EA01831303A21203A21206A2120EA2000C1380121C A2EA180118157E941C>25 DI<90387FFF8048B5FC5A390783C000EA0E01486C7E5AA25AA348485AA3495A91 C7FCEA6007130EEA3018EA1870EA07C019157E941C>I<380FFFF84813FC4813F8387020 001240128013601200A25BA412015BA21203A348C7FC7E16157E9415>I<133F3801FFC0 380381E0380400404813005AA31360EA0B98EA0FF80010C7FC5A5AA35A6C138012403860 0100EA300EEA1FFCEA07E013177F9517>34 D<127012F8A3127005057C840E>58 D<127012F812FCA212741204A41208A21210A212201240060F7C840E>I<15181578EC01 E0EC0780EC1E001478EB03E0EB0F80013CC7FC13F0EA03C0000FC8FC123C12F0A2123C12 0FEA03C0EA00F0133CEB0F80EB03E0EB0078141EEC0780EC01E0EC007815181D1C7C9926 >I<14801301A2EB0300A31306A35BA35BA35BA35BA35BA3485AA448C7FCA31206A35AA3 5AA35AA35AA35AA311317DA418>I<12C012F0123C120FEA03C0EA00F0133EEB0F80EB01 E0EB0078141EEC0780EC01E0EC0078A2EC01E0EC0780EC1E001478EB01E0EB0F80013EC7 FC13F0EA03C0000FC8FC123C12F012C01D1C7C9926>I<8114018114031407A2140BA214 1314331423EC43E0A21481EB0101A21302A213041308A201107FEB1FFFEB20005BA25BA2 48C7FC120281481478120C001E14F83AFF800FFF8021237EA225>65 D<90B512F090380F001E81ED0780011E1303A216C0A24914801507A2ED0F0049131E5D5D EC03E090B55A9038F000F0157881485A151C151EA248485BA35D485A5D4A5AEC0380000F 010FC7FCB512F822227DA125>I<027F138090390380810090380E00630138132749131F 49130E485A485A48C7FC481404120E121E5A5D4891C7FCA35AA55A1520A25DA26C5C1270 4AC7FC6C130200185B001C5B00061330380381C0D800FEC8FC21247DA223>I<90B512F0 90380F003C150E81011EEB0380A2ED01C0A25B16E0A35BA449EB03C0A44848EB0780A216 005D4848130E5D153C153848485B5D4A5A0207C7FC000F131CB512F023227DA128>I<02 7F1340903903C0C08090380E00214913130170130F49EB0700485A485A48C7FC48140212 0E121E5A5D4891C7FCA35AA4EC3FFF48EB00F0A34A5A7EA212704A5A7E001813076C1309 6CEB1180380380E0D8007FC8FC22247DA226>71 D<9039FFF83FFE90390F0003C0A3011E EB0780A449EB0F00A449131EA490B512FC9038F0003CA348485BA448485BA44848485AA4 000F130339FFF83FFE27227DA128>I<9039FFF801FF010FC71278166016C0011EEB0100 15025D5D4913205D5D0202C7FC495A5C141C147CEBF0BEEBF11E13F2EBF80FEA01F001E0 7F1407A248486C7EA36E7EEA0780811400A2000F497E39FFF80FFF28227DA129>75 DII<9039FF8007FE010FEB00F016C0D90BC013 4001131480A2EB11E0A2903921F001001320A2147801401302147C143CA2496C5AA3140F D801005B15881407A20002EB03D0A215F01401485C1400A2120C001E1440EAFFC027227D A127>I<90B512E090380F0038151E150E011E1307A449130FA3151E5B153C157815E090 38F003C09038FFFE0001F0C7FCA2485AA4485AA4485AA4120FEAFFF820227DA11F>80 D<147F90380381C090380E0060013813385B49131C4848131E4848130E48C7FC48140F12 0E121E5AA25AA348141EA3151C153C5A1578A215F015E06C130190381E03C0D870211380 39784087000038138E001C13B8000E13F03907C1C0203800FE8013000101134015C0ECC0 8014C3ECFF007F5C1478202D7DA227>I<90B512C090380F0078151C81011E130F811680 A249EB0F00A3151E495B5D15E0EC0380D9FFFCC7FCEBF0076E7E8148486C7EA44848485A A44848485A1680A29138038100120F39FFF801C6C8127821237DA125>I<903803F81090 380E0420903818026090382001E0EB400001C013C05B1201A200031480A21500A27FEA01 F013FE3800FFE06D7EEB1FF8EB01FCEB003C141C80A30020130CA3140800601318141000 705B5C00C85BD8C603C7FCEA81FC1C247DA21E>I<001FB512FE391E01E00E0018140612 30382003C0A200401404A2EB07801280A20000140049C7FCA4131EA45BA45BA45BA41201 387FFFC01F227EA11D>I96 DII<133FEBE080380380C0EA0701EA0E03121C003CC7FCA25AA35AA4007013 40A23830018038380200EA1C1CEA07E012157E9415>I<141EEC638014C71301ECC30014 801303A449C7FCA4EBFFF8010EC7FCA65BA55BA55BA4136013E0A25BA21271EAF18090C8 FC1262123C192D7EA218>102 DI<13F0EA07E01200A3485AA4485AA448C7FCEB 0F80EB30C0EB4060380E8070EA0F00120EA24813E0A4383801C0A2EB0380148200701384 EB07041408130300E01310386001E017237EA21C>I<13E0A21201EA00C01300A9121E12 23EA4380A21283EA8700A21207120EA35AA3EA38201340127013801230EA3100121E0B22 7EA111>I<147014F0A214601400A9130FEB3180EB41C01381A2EA0101A238000380A4EB 0700A4130EA45BA45BA3EA7070EAF0605BEA6380003EC7FC142C81A114>I<13F0EA0FE0 1200A3485AA4485AA448C7FC1478EB0184EB021C380E0C3C1310EB2018EB4000485A001F C7FC13E0EA1C38487EA27F140838701C10A3EB0C20EAE006386003C016237EA219>I<39 3C07E01F3A46183061803A47201880C03A87401D00E0EB801E141C1300000E90383801C0 A4489038700380A2ED070016044801E01308150EA2ED0610267001C01320D83000EB03C0 26157E942B>109 D<383C07C038461860384720303887403813801300A2000E1370A448 13E0A2EB01C014C1003813C2EB03821484130100701388383000F018157E941D>I<3803 C0F03804631CEB740EEA0878EB7007A2140FEA00E0A43801C01EA3143C38038038A2EBC0 7014E038072180EB1E0090C7FCA2120EA45AA3B47E181F819418>112 DII<137E 138138030080EA0201EA0603140090C7FC120713F0EA03FC6CB4FCEA003FEB0780130312 7000F01300A2EAE002EA4004EA3018EA0FE011157E9417>I<136013E0A4EA01C0A4EA03 80EAFFFCEA0380A2EA0700A4120EA45AA31308EA3810A21320EA184013C0EA0F000E1F7F 9E12>I<001E131800231338EA438014701283A2EA8700000713E0120EA3381C01C0A314 C2EB0384A21307380C0988EA0E113803E0F017157E941C>I<001E13E0EA2301384381F0 1380008313701430EA870000071320120EA3481340A21480A2EB0100A21302EA0C04EA06 18EA03E014157E9418>I<001EEB181C0023EB383CD84380133EEC701E0083140E1506EA 87000007EBE004120EA3391C01C008A31510A2152001031340EA0C0439070861803901F0 3E001F157E9423>I<3801E0F03806310C38081A1C0010133CEA201C14181400C65AA45B A314083860E01012F0142038E1704038423080383C1F0016157E941C>I<001E13180023 1338EA438014701283EA8700A2000713E0120EA3381C01C0A4EB0380A21307EA0C0B380E 1700EA03E7EA0007A2130E1260EAF01C1318485AEA8060EA41C0003FC7FC151F7E9418> II<14C0A31460B5 12F0A2C712E0EB0180EB03001302140A77A318>126 D E /Fs 25 107 df0 D<127012F8A3127005057C8E0E>I<6C13026C130600 60130C6C13186C13306C13606C13C03803018038018300EA00C6136C1338A2136C13C6EA 018338030180380600C048136048133048131848130C4813064813021718789727>I<13 C0A538E0C1C0EAF0C33838C700EA0EDCEA03F0EA00C0EA03F0EA0EDCEA38C738F0C3C0EA E0C13800C000A512157D9619>I<801301AFB7FCA23900018000AEB7FCA220227DA027>6 D15 D17 D<4B7EA46F7EA2166082A2161C8282B812E0A2C9EA0700160E5E1630A25E5EA24B5AA42B 1A7D9832>33 D<01601303A4496D7EA248486D7E48C81260A2000E153848814881B812C0 A20038C8EA0E006C5D6C5D00031560A26C6C5C6C6C495AA2016049C7FCA42A1A7C9832> 36 D<14C0495AA249C9FCA213065B5B013FB612E090B7FCD801C0C9FC0007CAFC123E12 F8123C120FEA0380C67E017FB612E07F0118C9FC7F7F7FA26D7EA26D7E2B1C7D9932>40 D<156081A281A2818181B77E16E0C91270161CEE0F80EE03E0EE0780EE1E0016381660B7 5A5EC80003C7FC15065D5DA25DA25D2B1C7D9932>I50 D<1403A21406A2140CA21418A21430A21460A214C0A3EB0180A2EB03 00A21306A25BA25BA25BA25BA25BA2485AA248C7FCA31206A25AA25AA25AA25AA25A1240 183079A300>54 D<12C0A812E0A212C0A803127D9400>I<0040141000C0143000601460 A36C14C0A36CEB0180A26CEB0300A33807FFFEA23803000CA36C6C5AA36C6C5AA2EB6060 A36D5AA2EB1980A3010FC7FCA31306A21C2480A21D>III<5B5BB3ABB612FEA2 1F207C9F27>63 D<90380FFFF8017F13FF48B612803A0387803FC0D80C07EB07E0001814 030038EB00011270EA600F00C015C01200ED0380010E14001506011E5B5D15E090381C1F C04AC7FCEB3C7FEB381F6E7E137890387007C0A29038F003E013E06E7E000115039039C0 00F806160C0003EC7C1849EB7FE090C7EA3FC00004EC1F0028237FA12A>82 D<130CA2131EA31333A2EB6180A2EBC0C0A338018060A248487EA300067FA2487FA3487F A2487FA248EB0180A348EB00C015401A1F7D9D21>94 D102 D<12F8120FEA03806C7E6C7EB113707F131EEB03C0EB1E0013385B5BB1485A485A000FC7 FC12F812317DA419>I<1320136013C0A3EA0180A3EA0300A21206A35AA35AA25AA35AA3 5AA21260A37EA37EA27EA37EA37EA2EA0180A3EA00C0A3136013200B327CA413>I<12C0 A21260A37EA37EA27EA37EA37EA2EA0180A3EA00C0A31360A213C0A3EA0180A3EA0300A2 1206A35AA35AA25AA35AA35AA20B327DA413>I<12C0B3B3AD02317AA40E>I E /Ft 42 122 df12 D<13181330136013C01201EA0380 EA0700A2120E121E121C123CA35AA412F85AAB7E1278A47EA3121C121E120E7EA2EA0380 EA01C012001360133013180D317BA416>40 D<12C012607E7E121C7E7EA2EA038013C012 0113E0A3EA00F0A413F81378AB13F813F0A4EA01E0A313C012031380EA0700A2120E5A12 185A5A5A0D317DA416>I<1238127C12FEA3127C123807077C8610>46 D<13FE3807FFC0380F83E0381F01F0383E00F8A248137CA312FC147EAD007C137CA36C13 F8A2381F01F0380F83E03807FFC03800FE0017207E9F1C>48 D<13181378EA01F812FFA2 1201B3A7387FFFE0A213207C9F1C>II<13FE3807FFC038 0F07E0381E03F0123FEB81F8A3EA1F0314F0120014E0EB07C0EB1F803801FE007F380007 C0EB01F014F8EB00FCA2003C13FE127EB4FCA314FCEA7E01007813F8381E07F0380FFFC0 3801FE0017207E9F1C>I<14E013011303A21307130F131FA21337137713E7EA01C71387 EA03071207120E120C12181238127012E0B6FCA2380007E0A790B5FCA218207E9F1C>I< 00301320383E01E0383FFFC0148014005B13F8EA33C00030C7FCA4EA31FCEA37FF383E0F C0383807E0EA3003000013F0A214F8A21238127C12FEA200FC13F0A2387007E0003013C0 383C1F80380FFF00EA03F815207D9F1C>I I<12601278387FFFFEA214FC14F8A214F038E0006014C038C00180EB0300A2EA00065B13 1C131813381378A25BA31201A31203A76C5A17227DA11C>I<13FE3803FFC0380703E038 0E00F05A1478123C123E123F1380EBE0F0381FF9E0EBFFC06C13806C13C06C13E04813F0 381E7FF8383C1FFCEA7807EB01FEEAF000143E141EA36C131C007813387E001F13F0380F FFC00001130017207E9F1C>II66 DII71 D73 D76 D80 D<3801FE023807FF86381F01FE383C007E007C13 1E0078130EA200F81306A27E1400B4FC13E06CB4FC14C06C13F06C13F86C13FC000313FE EA003F1303EB007F143FA200C0131FA36C131EA26C133C12FCB413F838C7FFE000801380 18227DA11F>83 D<007FB61280A2397E03F80F00781407007014030060140100E015C0A2 00C01400A400001500B3A248B512F0A222227EA127>I97 D99 DI<13FE3807FF80380F87 C0381E01E0003E13F0EA7C0014F812FCA2B5FCA200FCC7FCA3127CA2127E003E13186C13 30380FC0703803FFC0C6130015167E951A>II<3801FE0F3907FFBF8038 0F87C7381F03E7391E01E000003E7FA5001E5BEA1F03380F87C0EBFF80D809FEC7FC0018 C8FCA2121C381FFFE06C13F86C13FE001F7F383C003F48EB0F80481307A40078EB0F006C 131E001F137C6CB45A000113C019217F951C>II<121C123E127FA3123E121CC7FCA7 B4FCA2121FB2EAFFE0A20B247EA310>I107 DI<3AFF07F007F090391FFC1FFC 3A1F303E303E01401340496C487EA201001300AE3BFFE0FFE0FFE0A22B167E9530>I<38 FF07E0EB1FF8381F307CEB403CEB803EA21300AE39FFE1FFC0A21A167E951F>I<13FE38 07FFC0380F83E0381E00F0003E13F848137CA300FC137EA7007C137CA26C13F8381F01F0 380F83E03807FFC03800FE0017167E951C>I<38FF0FE0EB3FF8381FE07CEB803E497E15 80A2EC0FC0A8EC1F80A29038803F00EBC03EEBE0FCEB3FF8EB0FC090C8FCA8EAFFE0A21A 207E951F>I114 D I<487EA41203A21207A2120F123FB5FCA2EA0F80ABEB8180A5EB8300EA07C3EA03FEEA00 F811207F9F16>I<38FF01FEA2381F003EAF147E14FE380F81BE3907FF3FC0EA01FC1A16 7E951F>I<39FFE01FE0A2391F800700000F1306EBC00E0007130C13E000035BA26C6C5A A26C6C5AA2EB7CC0A2137F6D5AA26DC7FCA2130EA2130CA25B1278EAFC3813305BEA69C0 EA7F80001FC8FC1B207F951E>121 D E /Fu 13 107 df0 D<126012F0A2126004047D890A>II<1202A3EAC218EAF278EA3AE0EA0F80A2EA3AE0EAF278EAC218EA0200A30D0E7E8E12> I<1406A380A2EC0180EC00C01560B612FCA2C8126015C0EC0180EC0300A21406A31E127E 9023>33 D<1206120FA2120E121EA2121C123C1238A212301270A2126012E012C0124008 117F910A>48 D<1303A21306A2130CA21318A21330A21360A213C0A2EA0180A2EA0300A2 1206A25AA25AA25AA25AA25A1240101E7B9600>54 D<0040131000C0133000601360A36C 13C0A238180180EA1FFF6C1300EA0C03A2EA0606A26C5AA2EA0198A3EA00F0A21360A214 17809615>56 D58 D<13201360B3B512F8A215167D95 1B>63 D<3801FFF8000F13FE3818E03F0020130F00607F12C000001306A2495A14080001 5B1460EB8780018FC7FC00037FEB07C01303486C7E1206903800F02048EBF8C0EC7F0048 133C1B177F961E>82 D<134013E0A2EA01B0A2EA0318A2EA060CA2487EA2487EA2383001 80A2386000C0A2481360142013137E9218>94 D<12C0B3AF02217C980A>106 D E /Fv 79 128 df0 D<90381FC1F090387037189038C03E3C3801807C00031378390700 3800A9B612C03907003800B2143C397FE1FFC01E2380A21C>11 DI<90380FC07F90397031C0809039E00B00402601801E13E00003EB3E013807003C91 381C00C01600A7B712E03907001C011500B23A7FF1FFCFFE272380A229>14 D22 D34 D<127012F812FCA212741204A41208A21210A2122012 40060F7CA20E>39 D<132013401380EA01005A12061204120CA25AA25AA312701260A312 E0AE1260A312701230A37EA27EA2120412067E7EEA0080134013200B327CA413>I<7E12 407E7E12187E12041206A27EA2EA0180A313C01200A313E0AE13C0A312011380A3EA0300 A21206A21204120C5A12105A5A5A0B327DA413>I<497EB0B612FEA23900018000B01F22 7D9C26>43 D<127012F812FCA212741204A41208A21210A212201240060F7C840E>II<127012F8A3127005057C840E>I48 D<13801203120F12F31203B3A9EA07C0EAFFFE0F217CA018>I< EA03F0EA0C1CEA100700201380384003C0A2008013E012F0EAF801A3EA2003120014C0A2 EB07801400130E5B13185B5B5B485A90C7FC000213205A5A00181360481340383FFFC05A B5FC13217EA018>II<1303A25BA25B1317A2 1327136713471387120113071202120612041208A212101220A2124012C0B512F8380007 00A7EB0F80EB7FF015217FA018>I<00101380381E0700EA1FFF5B13F8EA17E00010C7FC A6EA11F8EA120CEA1C07381803801210380001C0A214E0A4127012F0A200E013C01280EA 4003148038200700EA1006EA0C1CEA03F013227EA018>I<137EEA01C138030080380601 C0EA0C03121C381801800038C7FCA212781270A2EAF0F8EAF30CEAF4067F00F81380EB01 C012F014E0A51270A3003813C0A238180380001C1300EA0C06EA070CEA01F013227EA018 >I<12401260387FFFE014C0A23840008038C0010012801302A2485A5BA25B5BA2136013 4013C0A21201A25B1203A41207A76CC7FC13237DA118>III<127012F8A312701200AB127012F8A3127005157C 940E>I<127012F8A312701200AB127012F8A312781208A41210A312201240A2051F7C94 0E>I61 D<497EA3497EA3EB05E0A2EB09F013 08A2EB1078A3497EA3497EA2EBC01F497EA248B51280EB0007A20002EB03C0A348EB01E0 A348EB00F0121C003EEB01F839FF800FFF20237EA225>65 DI<9038 07E0109038381830EBE0063901C0017039038000F048C7FC000E1470121E001C1430123C A2007C14101278A200F81400A812781510127C123CA2001C1420121E000E14407E6C6C13 803901C001003800E002EB381CEB07E01C247DA223>IIII<903807F0 0890383C0C18EBE0023901C001B839038000F848C71278481438121E15185AA2007C1408 1278A200F81400A7EC1FFF0078EB00F81578127C123CA27EA27E7E6C6C13B86C7E3900E0 031890383C0C08903807F00020247DA226>I<39FFFC3FFF390FC003F039078001E0AE90 B5FCEB8001AF390FC003F039FFFC3FFF20227EA125>II<3803FFE038001F007FB3A6127012F8A2130EEAF01EEA401C6C 5AEA1870EA07C013237EA119>IIII< 39FF8007FF3907C000F81570D805E01320EA04F0A21378137C133C7F131F7FEB0780A2EB 03C0EB01E0A2EB00F014F81478143C143E141E140FA2EC07A0EC03E0A21401A21400000E 1460121FD8FFE0132020227EA125>II82 D<3803F020380C0C60EA1802383001E0EA700000601360 12E0A21420A36C1300A21278127FEA3FF0EA1FFE6C7E0003138038003FC0EB07E01301EB 00F0A214707EA46C1360A26C13C07E38C8018038C60700EA81FC14247DA21B>I<007FB5 12F839780780780060141800401408A300C0140C00801404A400001400B3A3497E3801FF FE1E227EA123>I<39FFFC07FF390FC000F86C4813701520B3A5000314407FA200011480 6C7E9038600100EB3006EB1C08EB03F020237EA125>I<3BFFF03FFC03FE3B1F8007E000 F86C486C48137017206E7ED807801540A24A7E2603C0021480A39039E004780100011600 A2EC083CD800F01402A2EC101E01785CA2EC200F013C5CA20260138890391E400790A216 D090391F8003F0010F5CA2EC00016D5CA20106130001025C2F237FA132>87 D89 D<12FEA212C0B3B3A912FEA207317BA40E>91 DI<12FEA21206B3B3 A912FEA207317FA40E>I97 D<120E12FE121E120EAB131FEB61C0EB8060380F0030000E1338143C141C141EA7141C14 3C1438000F1370380C8060EB41C038083F0017237FA21B>II<14E0130F13011300ABEA01F8EA0704EA0C02EA1C01EA38001278127012F0 A7127012781238EA1801EA0C0238070CF03801F0FE17237EA21B>II<133E13E33801C780EA0387130748C7FCA9EAFFF8 0007C7FCB27FEA7FF0112380A20F>I<14703803F198380E1E18EA1C0E38380700A20078 1380A400381300A2EA1C0EEA1E1CEA33F00020C7FCA212301238EA3FFE381FFFC06C13E0 383000F0481330481318A400601330A2003813E0380E03803803FE0015217F9518>I<12 0E12FE121E120EABEB1F80EB60C0EB80E0380F0070A2120EAF38FFE7FF18237FA21B>I< 121C123EA3121CC7FCA8120E127E121E120EB1EAFFC00A227FA10E>I<13E0EA01F0A3EA 00E01300A81370EA07F012001370B3A51260EAF0E013C0EA6180EA3F000C2C83A10F>I< 120E12FE121E120EABEB03FCEB01F014C01480EB02005B5B5B133813F8EA0F1CEA0E1E13 0E7F1480EB03C0130114E0EB00F014F838FFE3FE17237FA21A>I<120E12FE121E120EB3 ADEAFFE00B237FA20E>I<390E1FC07F3AFE60E183803A1E807201C03A0F003C00E0A200 0E1338AF3AFFE3FF8FFE27157F942A>I<380E1F8038FE60C0381E80E0380F0070A2120E AF38FFE7FF18157F941B>I II<3801F82038070460EA0E02EA1C 01003813E0EA7800A25AA71278A2EA3801121CEA0C02EA070CEA01F0C7FCA9EB0FFE171F 7E941A>III<1202A41206A3120E121E123EEAFF FCEA0E00AB1304A6EA07081203EA01F00E1F7F9E13>I<000E137038FE07F0EA1E00000E 1370AD14F0A238060170380382783800FC7F18157F941B>I<38FF80FE381E0078143000 0E1320A26C1340A2EB80C000031380A23801C100A2EA00E2A31374A21338A3131017157F 941A>I<39FF8FF87F393E01E03C001CEBC01814E0000E1410EB0260147000071420EB04 301438D803841340EB8818141CD801C81380EBD00C140E3900F00F00497EA2EB6006EB40 0220157F9423>I<38FF83FE381F00F0000E13C06C1380EB8100EA0383EA01C2EA00E413 78A21338133C134E138FEA0187EB0380380201C0000413E0EA0C00383E01F038FF03FE17 157F941A>I<38FF80FE381E00781430000E1320A26C1340A2EB80C000031380A23801C1 00A2EA00E2A31374A21338A31310A25BA35B12F05B12F10043C7FC123C171F7F941A>I< 383FFFC038380380EA300700201300EA600EEA401C133C1338C65A5B12015B38038040EA 07005A000E13C04813805AEA7801EA7007B5FC12157F9416>II126 DI E /Fw 23 121 df12 D<121C123E127FEAFF80A3EA7F00123E121CC7FCB3121C123E127FEAFF80A3EA7F00123E 121C092579A418>58 D67 D69 D80 D82 DI97 D99 DII<147F903801FFC0903807C0E090380F81 F090381F03F8EB3E07137CA29038FC03F09038F801E0000190C7FCAEB512FCA3D801F8C7 FCB3AC487E387FFFF8A31D3D7FBC1A>I<903907F001F890393FFE0FFC90397C1F1E3E90 38F007F03A01E003E01C2603C00113080007ECF000000F80EB8000001F80A7000F5CEBC0 0100075C00035C6C6C485A6D485A26037C1FC7FC38073FFE380607F090C9FC120EA3120F A2EA07C090B512C06C14FC6C14FF6C1580000315C03A0F80003FE048C7EA07F0003EEC01 F8003C1400127C0078157C12F8A5007C15F8A26CEC01F06CEC03E06C6CEB07C0D803E0EB 1F00D801FC13FE39003FFFF00107138027397EA52B>I105 D108 D<2701F803F8EB03F800FFD91FFFEB1FFF913B3C0F803C0F80913BE007C0E007C03D07F9 C003E1C003E02601FB00D9F3007F0301140101FE02FE80A2495CA2495CB3A5486C496C49 7EB500F0B500F0B512F0A344267EA549>I<3901F807F800FFEB1FFEEC781F9138E00F80 3A07F98007C02601FB007F150301FE805BA35BB3A5486C497EB500F1B512E0A32B267EA5 30>II<3903F00F8000FFEB3FE0EC70F0ECC1F83807F1833801F303 A29038F601F0EC004001FC1300A45BB3A3487EB512F8A31D267EA522>114 D<90387F81803803FFE3380F807F381E001F00381307A2481303A200F01301A37EA200FE 90C7FCEA7F8013FC383FFFC06C13F06C13FC00037F6C7FD8001F13801300EC1FC0004013 0F00C0EB07E014036C1301A47E15C06C13036C1480EC070000F7130E38E3C03C38C0FFF8 EB3FC01B287DA622>I<1330A61370A413F0A21201A212031207001FB5FCB6FCA2D803F0 C7FCB2EC0180A912019038F80300A21200EB7C066D5AEB1FF8EB03F019367EB421>II120 D E end %%EndProlog %%BeginSetup %%Feature: *Resolution 300dpi TeXDict begin %%PaperSize: a4 %%EndSetup %%Page: 1 1 1 0 bop 106 255 a Fw(Re\014ned)29 b(Program)e(Extraction)k(from)c (Classical)414 358 y(Pro)r(ofs:)38 b(Some)28 b(Case)h(Studies)669 492 y Fv(Helm)o(ut)14 b(Sc)o(h)o(wic)o(h)o(ten)o(b)q(erg)1173 474 y Fu(\003)-1 675 y Ft(1)56 b(In)n(tro)r(duction)-1 785 y Fv(It)19 b(is)g(w)o(ell)f(kno)o(wn)i(that)g(it)f(is)h (undecidable)e(in)i(general)f(whether)g(a)h(giv)o(en)f(program)h(meets) d(its)-1 845 y(sp)q(eci\014cation.)j(In)14 b(con)o(trast,)g(it)g(can)h (b)q(e)f(c)o(hec)o(k)o(ed)e(easily)h(b)o(y)h(a)g(mac)o(hine)e(whether)i (a)h(formal)e(pro)q(of)-1 905 y(is)h(correct,)f(and)i(from)e(a)h (constructiv)o(e)f(pro)q(of)i(one)f(can)h(automatically)d(extract)i(a)g (corresp)q(onding)-1 965 y(program,)g(whic)o(h)g(b)o(y)g(its)g(v)o(ery) g(construction)g(is)h(correct)f(as)h(w)o(ell.)k(This)c({)g(at)g(least)g (in)f(principle)f({)-1 1026 y(op)q(ens)i(a)g(w)o(a)o(y)g(to)g(pro)q (duce)g(correct)f(soft)o(w)o(are,)h(e.g.)f(for)h(safet)o(y-critical)e (applications.)21 b(Moreo)o(v)o(er,)-1 1086 y(programs)16 b(obtained)g(from)f(pro)q(ofs)j(are)e(\\commen)o(ted")d(in)j(a)h (rather)f(extreme)d(sense.)22 b(Therefore)-1 1146 y(it)15 b(is)h(easy)h(to)f(main)o(tain)f(them,)f(and)j(also)g(to)f(adapt)i (them)c(to)j(particular)f(situations.)72 1206 y(W)l(e)d(will)g(concen)o (trate)h(on)g(the)g(question)g(of)g(classical)f(v)o(ersus)h (constructiv)o(e)e(pro)q(ofs.)22 b(It)14 b(is)f(w)o(ell)-1 1266 y(kno)o(wn)j(that)g(an)o(y)g(classical)f(pro)q(of)i(of)f(a)h(sp)q (eci\014cation)e(of)i(the)e(form)g Fs(8)p Fr(x)p Fs(9)p Fr(y)r(B)h Fv(with)g Fr(B)j Fv(quan)o(ti\014er-)-1 1327 y(free)c(can)h(b)q(e)g(transformed)g(in)o(to)g(a)g(constructiv)o(e)f (pro)q(of)i(of)f(the)g(same)f(form)o(ula)g(\(for)h(particularly)-1 1387 y(simple)c(pro)q(ofs,)k(cf.)e(F)l(riedman)e([5])i(or)h(Leiv)m(an)o (t)g([7]\).)20 b(Ho)o(w)o(ev)o(er,)13 b(when)h(it)h(comes)e(to)i (extraction)f(of)-1 1447 y(a)f(program)g(from)f(a)h(pro)q(of)h (obtained)g(in)e(this)h(w)o(a)o(y)l(,)g(one)g(easily)f(ends)i(up)f (with)g(a)g(mess.)19 b(Therefore,)-1 1507 y(some)c(re\014nemen)o(ts)f (of)i(the)g(standard)i(transformation)e(are)g(necessary)l(.)72 1567 y(In)g(the)g(presen)o(t)f(pap)q(er)i(w)o(e)f(mak)o(e)f(use)h(of)g (a)h(re\014ned)f(metho)q(d)g(of)g(extracting)g(programs)g(from)-1 1628 y(classical)e(pro)q(ofs;)j(it)d(is)h(dev)o(elop)q(ed)g(in)g (detail)f(in)h([1].)20 b(W)l(e)15 b(demonstrate)g(its)g(use)g(with)g(t) o(w)o(o)g(rather)-1 1688 y(detailed)21 b(case)i(studies.)40 b(Sp)q(eci\014cally)l(,)22 b(w)o(e)g(extract)g(programs)g(from)g (classical)g(pro)q(ofs)i(of)e(the)-1 1748 y(existence)14 b(of)71 1846 y Fs(\017)25 b Fv(in)o(teger)15 b(square)h(ro)q(ots,)h (and)71 1946 y Fs(\017)25 b Fv(in)o(teger)15 b(co)q(e\016cien)o(ts)h (to)h(linearly)f(com)o(bine)e(the)j(greatest)g(common)e(divisor)h(of)i (t)o(w)o(o)e(n)o(um-)121 2006 y(b)q(ers)g(from)f(these)h(n)o(um)o(b)q (ers,)-1 2104 y(The)i(latter)f(example)f(has)i(already)g(b)q(een)g (treated)g(in)f([2];)h(here)f(w)o(e)h(sho)o(w)h(ho)o(w)f(it)f(can)h(b)q (e)g(dealt)-1 2165 y(with)13 b(in)h(the)g(presen)o(t)f(form)g(of)h(the) f(theory)l(.)21 b(It)13 b(turns)h(out)h(that)f(the)g(algorithm)f(do)q (es)h(not)h(c)o(hange;)-1 2225 y(ho)o(w)o(ev)o(er,)20 b(the)g(metho)q(d)g(of)h(ho)o(w)g(to)g(extract)f(a)h(program)g(from)e (this)i(classical)f(pro)q(of)h(b)q(ecomes)-1 2285 y(more)15 b(p)q(erspicious.)72 2345 y(Other)k(in)o(teresting)g(examples)f(of)i (program)f(extraction)g(from)g(classical)g(pro)q(ofs)i(ha)o(v)o(e)e(b)q (een)-1 2405 y(studied)i(b)o(y)h(Murth)o(y)f([8],)h(the)g(group)h (around)g(Co)q(quand)g(\(see)e(e.g.)h([3)o(]\))g(in)f(a)i(t)o(yp)q(e)e (theoretic)-1 2466 y(con)o(text)15 b(and)i(b)o(y)f(Kohlen)o(bac)o(h)f ([6])h(using)h(a)f(Dialectica-in)o(terpretation.)72 2526 y(The)e(pap)q(er)g(is)g(organized)h(as)f(follo)o(ws.)21 b(In)13 b(section)h(2)h(the)e(general)h(bac)o(kground)h(is)f(dev)o (elop)q(ed.)-1 2586 y(W)l(e)f(start)i(in)e(2.1)h(with)g(a)g(short)g (exp)q(osition)g(of)g(G\177)-24 b(odel's)14 b(system)e Fr(T)7 b Fv(.)20 b(T)l(ait's)14 b(pro)q(of)h(of)f(termination)-1 2646 y(for)g(the)h(simply)d(t)o(yp)q(ed)i Fr(\025)p Fv(-calculus)g(is)h (presen)o(ted)e(in)h(detail,)g(and)h(is)f(then)g(extended)g(to)h Fr(T)7 b Fv(.)20 b(In)14 b(2.2)-1 2706 y(w)o(e)19 b(\014x)g(our)g(v)o (ersion)g(of)h(in)o(tuitionistic)d(arithmetic)g(for)i(functionals,)h (and)g(recall)e(ho)o(w)i(classical)-1 2766 y(arithmetic)d(can)i(b)q(e)h (seen)f(as)i(a)f(subsystem.)30 b(Subsection)19 b(2.3)h(dev)o(elops)f (the)g(basic)h(mac)o(hinery)-1 2827 y(of)d(mo)q(di\014ed)f (realizabilit)o(y)l(,)e(and)k(con)o(tains)g(a)f(detailed)f(pro)q(of)j (of)e(the)g(soundness)i(theorem.)j(The)p -1 2869 737 2 v 54 2900 a Fq(\003)73 2915 y Fp(Mathematisc)o(hes)17 b(Institut)h(der)g(Univ)o(ersit\177)-21 b(at)17 b(M)q(\177)-22 b(unc)o(hen,)19 b(Theresienstra\031e)g(39,)e(D-80333)f(M)q(\177)-22 b(unc)o(hen,)18 b(Ger-)-1 2965 y(man)o(y)m(.)d(Phone)g(+49)e(89)h(2394) f(4413,)f(F)m(ax)h(+49)h(89)f(280)g(5248,)g Fo(schwicht@rz.mat)o(hemat) o(ik.un)o(i-mue)o(nchen)o(.de)p eop %%Page: 2 2 2 1 bop -1 53 a Fv(main)15 b(part)j(of)f(the)g(pap)q(er)h(is)f(section) g(3.)24 b(There)17 b(de\014nite)f(and)i(goal)g(form)o(ulas)e(are)h (de\014ned,)g(and)-1 114 y(the)e(main)f(theorem)f(on)j(program)f (extraction)g(from)f(classical)g(pro)q(ofs)j(\(Theorem)d(3.2\))h(is)g (stated;)-1 174 y(for)g(the)h(pro)q(of)g(w)o(e)f(ha)o(v)o(e)g(to)h (refer)f(to)h([1].)k(Subsections)c(3.2)g(and)g(3.3)g(then)f(dev)o(elop) f(the)i(t)o(w)o(o)f(case)-1 234 y(studies)h(men)o(tioned)e(ab)q(o)o(v)o (e.)-1 363 y Fn(A)n(cknow)r(le)n(dgements)52 b Fv(The)23 b(pro)q(of)h(of)f(termination)e(for)i(G\177)-24 b(odel's)22 b(system)f Fr(T)30 b Fv(uses)23 b(ideas)f(from)-1 423 y(Ulric)o(h)16 b(Berger,)i(Holger)f(Benl,)h(Ralph)g(Matthes)g(and)h (Thorsten)g(Altenkirc)o(h.)25 b(Monik)m(a)19 b(Seisen-)-1 483 y(b)q(erger)14 b(and)g(F)l(elix)f(Joac)o(himski)f(ha)o(v)o(e)h(con) o(tributed)g(a)i(lot)e(to)i(the)f Fm(Minlog)f Fv(system,)f (particularly)-1 544 y(to)k(the)g(implem)o(en)o(tation)d(of)k(the)f (translation)h(of)f(classical)g(pro)q(ofs)h(in)o(to)f(constructiv)o(e)f (ones.)-1 678 y Ft(2)56 b(General)17 b(Bac)n(kground)-1 787 y Fn(2.1)49 b(G\177)-25 b(odel's)18 b(System)g Fr(T)-1 897 y Fv(W)l(e)d(in)o(tro)q(duce)g(G\177)-24 b(odel's)16 b(system)e Fr(T)22 b Fv(of)16 b(primitiv)o(e)c(recursiv)o(e)i (functionals)i(of)g(\014nite)f(t)o(yp)q(e,)g(form)o(u-)-1 957 y(lated)h(as)g(a)h(simply)d(t)o(yp)q(ed)i(lam)o(b)q(da)f(calculus)h (with)g(higher)g(t)o(yp)q(e)g(recursion)g(constan)o(ts.)72 1017 y Fn(T)l(yp)n(es)j Fv(are)d(as)h(for)f(the)f(simply)f(t)o(yp)q(ed) h(lam)o(b)q(da)g(calculus,)g(but)h(with)g(concrete)f(ground)h(t)o(yp)q (es)-1 1078 y Fr(\023)g Fv(for)h(the)f(natural)g(n)o(um)o(b)q(ers)f (and)i Fl(o)i Fv(for)e(the)f(b)q(o)q(olean)h(ob)s(jects)f Fl(true)j Fv(and)e Fl(false)r Fv(.)706 1182 y Fr(\023)d Fs(j)g Fl(o)j Fs(j)c Fr(\032)f Fs(\002)e Fr(\033)16 b Fs(j)d Fr(\032)h Fs(!)g Fr(\033)o(:)-1 1286 y Fv(The)i Fn(c)n(onstants)21 b Fv(are)537 1346 y Fl(true)627 1326 y Fk(o)666 1346 y Fs(j)13 b Fl(false)790 1325 y Fk(o)828 1346 y Fs(j)h Fv(0)880 1326 y Fj(\023)909 1346 y Fs(j)g Fv(S)964 1326 y Fj(\023)p Fu(!)p Fj(\023)1040 1346 y Fs(j)g(R)1110 1353 y Fk(o)r Fj(;\032)1176 1346 y Fs(j)g(R)1246 1353 y Fj(\023;\032)1289 1346 y Fr(:)-1 1431 y Fs(R)41 1438 y Fj(\023;\032)101 1431 y Fv(is)j(the)g Fn(primitive)h(r)n(e)n (cursion)g(op)n(er)n(ator)j Fv(of)d(t)o(yp)q(e)e Fr(\032)g Fs(!)g Fv(\()p Fr(\023)g Fs(!)f Fr(\032)h Fs(!)f Fr(\032)p Fv(\))h Fs(!)g Fr(\023)f Fs(!)h Fr(\032)p Fv(.)24 b Fs(R)1681 1438 y Fk(o)r Fj(;\032)1752 1431 y Fv(is)17 b(of)-1 1491 y(t)o(yp)q(e)e Fr(\032)f Fs(!)f Fr(\032)h Fs(!)g Fl(o)j Fs(!)c Fr(\032)j Fv(and)g(represen)o(ts)f Fn(b)n(o)n(ole)n(an)i (induction)t Fv(,)g(i.e.)d(de\014nition)h(b)o(y)g(cases.)21 b(Instead)-1 1551 y(of)16 b Fs(R)96 1558 y Fk(o)r Fj(;\032)149 1551 y Fr(M)5 b(N)g(K)21 b Fv(w)o(e)16 b(will)f(often)h(write)g Ft(if)21 b Fr(K)f Ft(then)c Fr(M)22 b Ft(else)15 b Fr(N)5 b Fv(.)72 1612 y Fn(T)l(erms)20 b Fv(are)257 1716 y Fr(x)285 1695 y Fj(\032)319 1716 y Fs(j)13 b Fr(c)367 1695 y Fj(\032)404 1716 y Fv(\()p Fr(c)444 1698 y Fj(\032)480 1716 y Fv(a)k(constan)o(t\)) d Fs(j)g(h)p Fr(M)r(;)8 b(N)d Fs(i)15 b(j)f Fr(\031)986 1723 y Fi(0)1005 1716 y Fv(\()p Fr(M)5 b Fv(\))14 b Fs(j)g Fr(\031)1165 1723 y Fi(1)1184 1716 y Fv(\()p Fr(M)5 b Fv(\))14 b Fs(j)g Fr(\025x)1372 1695 y Fj(\032)1392 1716 y Fr(M)20 b Fs(j)13 b Fr(M)5 b(N)-1 1820 y Fv(with)19 b(the)g(usual)h(t)o(yping)f(rules.)31 b(The)19 b Fn(c)n(onversions)25 b Fv(are)19 b(those)h(for)g(the)f(simply)f(t)o(yp)q(ed)h(lam)o(b)q(da) -1 1880 y(calculus,)c(plus)h(some)f(new)h(ones)h(for)g(the)f(recursion) g(op)q(erators.)22 b(W)l(e)16 b(write)g Fr(K)f Fv(+)c(1)17 b(for)f(S)p Fr(K)t Fv(.)511 1980 y Fs(R)553 1987 y Fk(o)r Fj(;\032)606 1980 y Fr(M)5 b(N)14 b Fl(true)92 b Fs(7!)940 1987 y Fu(R)1035 1980 y Fr(M)504 2040 y Fs(R)546 2047 y Fk(o)r Fj(;\032)599 2040 y Fr(M)5 b(N)14 b Fl(false)92 b Fs(7!)940 2047 y Fu(R)1035 2040 y Fr(N)594 2101 y Fs(R)636 2108 y Fj(\023;\032)679 2101 y Fr(M)5 b(N)g Fv(0)91 b Fs(7!)940 2108 y Fu(R)1035 2101 y Fr(M)451 2161 y Fs(R)493 2168 y Fj(\023;\032)536 2161 y Fr(M)5 b(N)g Fv(\()p Fr(K)16 b Fv(+)11 b(1\))90 b Fs(7!)940 2168 y Fu(R)1035 2161 y Fr(N)5 b(K)t Fv(\()p Fs(R)1185 2168 y Fj(\023;\032)1228 2161 y Fr(M)g(N)g(K)t Fv(\))-1 2262 y(W)l(e)17 b(will)f(pro)o(v)o(e)g (that)i(for)g(this)f(system)f(of)h(terms)f(ev)o(ery)g(term)g(strongly)h (normalizes.)23 b(Since)16 b(the)-1 2322 y(normal)11 b(form)f(is)i(uniquely)e(determined,)g(the)i(relation)f Fr(M)20 b Fv(=)1132 2329 y Fj(\014)r Fu(R)1199 2322 y Fr(N)d Fv(is)12 b(decidable)f(\(b)o(y)g(normalizing)-1 2382 y Fr(M)21 b Fv(and)c Fr(N)5 b Fv(\).)22 b(By)16 b(iden)o(tifying)e(=)618 2389 y Fj(\014)r Fu(R)672 2382 y Fv(-equal)i(terms)f(\(i.e.)f(treating)j(equations)f(on)h(the)f(meta)f (lev)o(el\))-1 2442 y(w)o(e)g(can)i(greatly)f(simplify)d(man)o(y)i (formal)g(deriv)m(ations.)-1 2571 y Fn(T)l(ait's)i(Pr)n(o)n(of)f(of)h (T)l(ermination)h(for)f(the)h(Simply)g(T)l(yp)n(e)n(d)e(L)n(amb)n(da)g (Calculus)-1 2664 y Fv(W)l(e)h(\014rst)i(giv)o(e)e(a)h(w)o(ell-kno)o (wn)f(pro)q(of)j(of)e Fn(termination)k Fv(of)d(the)f(simply)d(t)o(yp)q (ed)j(lam)o(b)q(da)f(calculus,)-1 2724 y(using)h(metho)q(d)e(due)i(to)g (W.W.)f(T)l(ait.)25 b(This)18 b(pro)q(of)g(will)f(later)g(b)q(e)h (extended)e(to)i(G\177)-24 b(odel's)18 b(system)-1 2784 y Fr(T)7 b Fv(.)72 2844 y(T)l(ait's)17 b(pro)q(of)h(rests)g(on)g (de\014ning)f(so-called)g Fn(str)n(ong)h(c)n(omputability)h(pr)n(e)n (dic)n(ates)t Fv(.)24 b(W)l(e)17 b(presen)o(t)-1 2904 y(the)22 b(pro)q(of)i(here)e(in)g(a)h(form)f(whic)o(h)f(a)o(v)o(oids)i (in)o(tuitiv)o(e)d(argumen)o(ts)i(concerning)g(reduction)g(se-)-1 2965 y(quences)15 b(and)i(therefore)f(is)g(suitable)f(for)i (formalization)e(in)h(a)g(theory)g(of)h(inductiv)o(e)d(de\014nitions.)p eop %%Page: 3 3 3 2 bop 72 53 a Fv(W)l(e)22 b(b)q(egin)g(with)g(a)g(de\014nition)g(of)g Fn(str)n(ongly)h(normalizable)h(terms)t Fv(,)f(b)o(y)f(a)g(strictly)f (p)q(ositiv)o(e)-1 114 y(induction.)103 218 y(If)16 b(all)f Fr(M)271 200 y Fu(0)300 218 y Fv(suc)o(h)h(that)g Fr(M)k Fs(\000)-9 b(!)662 225 y Fj(\014)699 218 y Fr(M)751 200 y Fu(0)780 218 y Fv(are)16 b(strongly)h(normalizable)d(\(sn\),)i(then)g (so)h(is)f Fr(M)5 b Fv(.)-1 322 y(Ob)o(viously)15 b Fr(M)23 b Fv(is)16 b(sn)h(if)f(and)i(only)e(if)h(ev)o(ery)e(reduction)h (sequence)g(starting)h(with)g Fr(M)22 b Fv(terminates)-1 382 y(after)f(a)g(\014nite)g(n)o(um)o(b)q(er)e(of)j(steps.)36 b(This)22 b(can)f(b)q(e)g(seen)g(as)h(follo)o(ws.)36 b(=)-8 b Fs(\))p Fv(.)36 b(Induction)21 b(on)g(the)-1 442 y(de\014nition)c(of)h(\\strongly)g(normalizable".)25 b(Consider)18 b(a)g(reduction)f(sequence)g(starting)h(with)g Fr(M)-1 502 y Fv(and)d(therein)g(the)f(\014rst)i(reduct)f Fr(M)642 484 y Fu(0)654 502 y Fv(.)20 b(The)c(IH)e(for)h Fr(M)982 484 y Fu(0)1010 502 y Fv(yields)f(the)g(assertion.)22 b Fs(\()-8 b Fv(=.)20 b(By)15 b(induction)-1 563 y(on)h(the)g(length)g (of)h(the)f(longest)h(reduction)e(sequence)g(\(K\177)-24 b(onig's)17 b(lemm)o(a\).)72 623 y(W)l(e)j(note)g(a)g(n)o(um)o(b)q(er)f (of)h(the)g(prop)q(erties)g(of)g(the)g(notion)h(\\strongly)g (normalizable",)e(to)h(b)q(e)-1 683 y(used)c(b)q(elo)o(w.)524 743 y(If)g(all)f(terms)790 731 y Fr(~)776 743 y(M)22 b Fv(are)16 b(sn,)g(then)g(so)h(is)f Fr(x)1264 731 y(~)1250 743 y(M)5 b Fv(.)463 b(\(1\))72 832 y Fn(Pr)n(o)n(of)9 b Fv(.)20 b(Induction)13 b(on)h(the)f(de\014nition)g(of)h(sn)f(for)1006 820 y Fr(~)992 832 y(M)6 b Fv(.)20 b(Let)13 b Fr(x)1205 820 y(~)1191 832 y(M)19 b Fs(\000)-8 b(!)1338 839 y Fj(\014)1375 832 y Fr(N)19 b Fv(b)q(e)13 b(giv)o(en.)20 b(It)13 b(su\016ces)-1 898 y(to)k(sho)o(w)g(that)g Fr(N)22 b Fv(is)17 b(sn.)23 b(F)l(rom)16 b Fr(x)651 886 y(~)637 898 y(M)k Fs(\000)-9 b(!)784 905 y Fj(\014)822 898 y Fr(N)22 b Fv(it)17 b(follo)o(ws)f(that) i Fr(N)i Fv(=)14 b Fr(x)1353 886 y(~)1339 898 y(M)1391 880 y Fu(0)1403 898 y Fv(,)j(where)1589 886 y Fr(~)1575 898 y(M)1627 880 y Fu(0)1656 898 y Fv(arises)g(b)o(y)-1 965 y(substitution)i(of)g Fr(M)378 972 y Fj(i)411 965 y Fv(b)o(y)f Fr(M)533 947 y Fu(0)528 977 y Fj(i)564 965 y Fv(with)h Fr(M)725 972 y Fj(i)758 965 y Fs(\000)-9 b(!)838 972 y Fj(\014)880 965 y Fr(M)932 947 y Fu(0)927 977 y Fj(i)944 965 y Fv(.)29 b(It)18 b(is)h(to)g(b)q(e)g(pro)o(v)o(ed)f (that)h Fr(x)1536 952 y(~)1522 965 y(M)1574 947 y Fu(0)1605 965 y Fv(is)g(sn.)29 b(This)-1 1031 y(follo)o(ws)16 b(from)f(the)h(IH)f (for)517 1018 y Fr(~)503 1031 y(M)555 1013 y Fu(0)567 1031 y Fv(.)p 1821 1001 21 2 v 1821 1029 2 28 v 1839 1029 V 1821 1031 21 2 v 642 1151 a(If)g Fr(M)5 b(x)17 b Fv(is)f(sn,)g(then)g(so)h(is)f Fr(M)5 b Fv(.)581 b(\(2\))72 1236 y Fn(Pr)n(o)n(of)9 b Fv(.)36 b(Induction)21 b(on)g(the)g (de\014nition)g(of)h(sn)f(for)h Fr(M)5 b(x)p Fv(.)36 b(Let)22 b Fr(M)27 b Fs(\000)-8 b(!)1441 1243 y Fj(\014)1487 1236 y Fr(M)1539 1218 y Fu(0)1572 1236 y Fv(b)q(e)21 b(giv)o(en.)36 b(It)-1 1296 y(su\016ces)18 b(to)h(sho)o(w)h(that)f Fr(M)513 1278 y Fu(0)544 1296 y Fv(is)g(sn.)30 b(F)l(rom)17 b Fr(M)24 b Fs(\000)-8 b(!)968 1303 y Fj(\014)1010 1296 y Fr(M)1062 1278 y Fu(0)1092 1296 y Fv(w)o(e)19 b(get)g Fr(M)5 b(x)19 b Fs(\000)-9 b(!)1430 1303 y Fj(\014)1472 1296 y Fr(M)1524 1278 y Fu(0)1536 1296 y Fr(x)p Fv(.)29 b(The)19 b(IH)f(for)-1 1356 y Fr(M)51 1338 y Fu(0)63 1356 y Fr(x)e Fv(then)g(yields)f(that)i Fr(M)513 1338 y Fu(0)541 1356 y Fv(is)f(sn.)p 1821 1327 V 1821 1355 2 28 v 1839 1355 V 1821 1357 21 2 v 72 1416 a(W)l(e)j(no)o(w)g (de\014ne)g(when)g(a)g(term)f Fr(M)752 1398 y Fj(\032)791 1416 y Fv(is)h(strongly)h(computable)d(\(sc\),)j(b)o(y)e(induction)h (on)g(the)-1 1477 y(t)o(yp)q(e)c Fr(\032)p Fv(.)71 1573 y Fs(\017)25 b Fr(M)173 1555 y Fj(\023)204 1573 y Fv(is)16 b(sc)g(if)g Fr(M)407 1555 y Fj(\023)438 1573 y Fv(is)g(sn.)71 1673 y Fs(\017)25 b Fr(M)173 1655 y Fj(\032)p Fu(!)p Fj(\033)266 1673 y Fv(is)16 b(sc)g(if)g(for)g(ev)o(ery)f(sc)h Fr(N)721 1655 y Fj(\032)758 1673 y Fv(also)h(\()p Fr(M)5 b(N)g Fv(\))990 1655 y Fj(\033)1030 1673 y Fv(is)16 b(sc.)-1 1774 y(A)i(term)e Fr(M)24 b Fv(is)19 b(called)e Fn(str)n(ongly)i(c)n (omputable)i(under)f(substitution)j Fv(if)18 b(for)h(an)o(y)f(sc)h (terms)1707 1762 y Fr(~)1697 1774 y(N)24 b Fv(also)-1 1835 y Fr(M)5 b Fv([)o Fr(~)-23 b(x)13 b Fv(:=)182 1822 y Fr(~)171 1835 y(N)6 b Fv(])15 b(is)i(sc.)72 1895 y(W)l(e)f(note)g(a)h (prop)q(ert)o(y)f(of)h(the)f(notion)g(\\strongly)h(computable")e(whic)o (h)h(will)f(b)q(e)i(used)f(b)q(elo)o(w.)449 1999 y Fr(M)21 b Fv(is)16 b(sc)g(if)g(and)h(only)f(if)g Fr(M)977 1986 y(~)967 1999 y(N)22 b Fv(is)16 b(sc)g(for)g(all)g(sc)1344 1986 y Fr(~)1333 1999 y(N)6 b Fv(.)387 b(\(3\))72 2107 y Fn(Pr)n(o)n(of)9 b Fv(.)21 b(Induction)16 b(on)g(the)g(length)g(of) 818 2095 y Fr(~)808 2107 y(N)5 b Fv(.)p 1821 2078 V 1821 2106 2 28 v 1839 2106 V 1821 2108 21 2 v -1 2215 a Ft(Lemm)o(a)16 b(2.1)82 b Fn(a.)24 b(Every)18 b(sc)f(term)h Fr(M)783 2197 y Fj(\032)821 2215 y Fn(is)f(sn.)59 2315 y(b.)25 b(If)186 2302 y Fr(~)172 2315 y(M)e Fn(ar)n(e)16 b(sn,)i(then)g Fv(\()p Fr(x)573 2302 y(~)559 2315 y(M)5 b Fv(\))630 2297 y Fj(\032)668 2315 y Fn(is)17 b(sc.)72 2422 y(Pr)n(o)n(of)9 b Fv(.)25 b(By)17 b(sim)o(ultaneous)f(induction)h(on)h(the)f(t)o(yp)q (e)g Fr(\032)p Fv(.)26 b Fn(Case)21 b Fr(\023)p Fv(.)k(a.)h(By)17 b(de\014nition.)25 b(b.)g(By)-1 2483 y(\(1\).)72 2547 y Fn(Case)f Fr(\032)d Fs(!)f Fr(\033)i Fv(a.)33 b(Let)20 b Fr(M)578 2529 y Fj(\032)p Fu(!)p Fj(\033)676 2547 y Fv(b)q(e)g(sc.)33 b(By)19 b(IHb)h(\(with)1164 2535 y Fr(~)1150 2547 y(M)25 b Fv(empt)o(y\))18 b(and)j(the)f(de\014nition)g (of)-1 2607 y(strong)i(computabilit)o(y)c(\()p Fr(M)5 b(x)p Fv(\))587 2589 y Fj(\033)631 2607 y Fv(is)21 b(sc.)36 b(By)20 b(IHa)g Fr(M)5 b(x)22 b Fv(then)e(is)h(sn.)36 b(By)20 b(\(2\))h Fr(M)27 b Fv(is)21 b(sn)g(to)q(o.)36 b(b.)-1 2672 y(Consider)15 b(\()p Fr(x)262 2660 y(~)248 2672 y(M)5 b Fv(\))319 2654 y Fj(\032)p Fu(!)p Fj(\033)411 2672 y Fv(with)536 2660 y Fr(~)521 2672 y(M)21 b Fv(sn.)g(Let)16 b Fr(N)801 2654 y Fj(\032)837 2672 y Fv(b)q(e)f(sc.)21 b(W)l(e)15 b(ha)o(v)o(e)f(to)i(sho)o(w)g(that)g(\()p Fr(x)1517 2660 y(~)1503 2672 y(M)5 b(N)g Fv(\))1618 2654 y Fj(\033)1657 2672 y Fv(is)15 b(sc.)21 b(By)-1 2737 y(IHa)15 b Fr(N)22 b Fv(is)16 b(sn,)g(hence)g Fr(x)457 2724 y(~)443 2737 y(M)5 b(N)21 b Fv(is)16 b(sc)g(b)o(y)g(IHb.)p 1821 2707 V 1821 2735 2 28 v 1839 2735 V 1821 2737 21 2 v 72 2797 a(If)11 b Fr(M)19 b Fs(\000)-8 b(!)263 2804 y Fj(\014)300 2797 y Fr(M)352 2779 y Fu(0)376 2797 y Fv(and)13 b Fr(M)k Fv(is)12 b(sn,)g(then)g(b)o(y)g(the)f(de\014nition)h (of)g(strong)h(normalizabilit)o(y)c(also)j Fr(M)1784 2779 y Fu(0)1808 2797 y Fv(is)-1 2857 y(sn.)20 b(W)l(e)12 b(no)o(w)h(sho)o(w)g(that)g(the)g(corresp)q(onding)g(assertion)g(is)g (also)g(v)m(alid)f(for)h(strong)g(computabilit)o(y)l(.)-1 2965 y Ft(Lemm)o(a)j(2.2)24 b Fn(If)17 b Fr(M)j Fs(\000)-9 b(!)491 2972 y Fj(\014)528 2965 y Fr(M)580 2947 y Fu(0)610 2965 y Fn(and)17 b Fr(M)23 b Fn(is)17 b(sc,)h(then)h(so)e(is)g Fr(M)1176 2947 y Fu(0)1188 2965 y Fn(.)p eop %%Page: 4 4 4 3 bop 72 60 a Fn(Pr)n(o)n(of)9 b Fv(.)28 b(W)l(e)19 b(use)f(\(3\).)29 b(Let)616 47 y Fr(~)606 60 y(N)24 b Fv(b)q(e)19 b(a)g(list)f(of)h(sc)g(terms)e(suc)o(h)h(that)h Fr(M)1404 47 y(~)1393 60 y(N)25 b Fv(is)18 b(of)h(ground)h(t)o(yp)q(e.) -1 125 y(Then)i Fr(M)194 112 y(~)184 125 y(N)28 b Fv(is)22 b(sc)g(b)o(y)g(\(3\),)h(hence)e(also)i(sn.)40 b(F)l(urthermore)20 b(w)o(e)i(ha)o(v)o(e)f Fr(M)1434 112 y(~)1423 125 y(N)30 b Fs(\000)-9 b(!)1572 132 y Fj(\014)1620 125 y Fr(M)1672 107 y Fu(0)1694 112 y Fr(~)1684 125 y(N)5 b Fv(.)39 b(By)-1 191 y(de\014nition)15 b(of)i(strong)g(normalizablilit)o(y)c Fr(M)822 173 y Fu(0)844 178 y Fr(~)834 191 y(N)21 b Fv(is)16 b(sn.)22 b(Th)o(us)17 b(b)o(y)e(\(3\))i Fr(M)1347 173 y Fu(0)1375 191 y Fv(is)f(sc.)p 1821 161 21 2 v 1821 189 2 28 v 1839 189 V 1821 191 21 2 v -1 310 a Ft(Lemm)o(a)g(2.3)24 b Fn(L)n(et)f Fr(N)29 b Fn(b)n(e)24 b(sn.)42 b(If)23 b Fr(M)5 b Fv([)p Fr(x)25 b Fv(:=)g Fr(N)5 b Fv(])934 297 y Fr(~)932 310 y(L)24 b Fn(is)f(sn)h(and)g(of)f(a)h(gr)n(ound)f (typ)n(e,)i(then)g(so)e(is)-1 374 y Fv(\()p Fr(\025x)8 b(M)d Fv(\))p Fr(N)199 362 y(~)197 374 y(L)q Fn(.)72 493 y(Pr)n(o)n(of)k Fv(.)25 b(By)17 b(induction)g(on)i(the)e(strong)i (normalizabilit)o(y)14 b(for)k Fr(N)23 b Fv(and)18 b Fr(M)5 b Fv([)p Fr(x)16 b Fv(:=)g Fr(N)5 b Fv(])1646 480 y Fr(~)1644 493 y(L)p Fv(.)25 b(So)19 b(w)o(e)-1 558 y(consider)c(all)g(the)h(reducts)f Fr(K)20 b Fv(of)c(\()p Fr(\025x)8 b(M)d Fv(\))p Fr(N)825 545 y(~)823 558 y(L)q Fv(.)21 b(Clearly)15 b(it)g(su\016ces)g(to)h(sho)o(w)g(that)h(ev)o(ery) d(suc)o(h)h Fr(K)-1 618 y Fv(is)h(sn.)72 678 y Fn(Case)25 b Fr(K)i Fv(=)c Fr(M)5 b Fv([)p Fr(x)23 b Fv(:=)f Fr(N)5 b Fv(])579 665 y Fr(~)577 678 y(L)p Fv(,)23 b(i.e.)d(w)o(e)h(ha)o(v)o (e)g(an)h(outer)f Fr(\014)s Fv(-con)o(v)o(ersion.)36 b(Hence)21 b Fr(K)k Fv(is)d(sn)g(b)o(y)-1 738 y(assumption.)72 798 y Fn(Case)e Fr(K)e Fv(=)c(\()p Fr(\025x)8 b(M)440 780 y Fu(0)453 798 y Fv(\))p Fr(N)518 786 y(~)516 798 y(L)17 b Fv(with)f Fr(M)k Fs(\000)-9 b(!)824 805 y Fj(\014)862 798 y Fr(M)914 780 y Fu(0)926 798 y Fv(.)21 b(Then)c(w)o(e)f(ha)o(v)o (e)g Fr(M)5 b Fv([)p Fr(x)13 b Fv(:=)h Fr(N)5 b Fv(])1507 786 y Fr(~)1505 798 y(L)14 b Fs(\000)-8 b(!)1633 805 y Fj(\014)1670 798 y Fr(M)1722 780 y Fu(0)1734 798 y Fv([)p Fr(x)14 b Fv(:=)-1 865 y Fr(N)5 b Fv(])59 852 y Fr(~)57 865 y(L)p Fv(.)21 b(By)15 b(de\014nition)h(of)h(strong)g (normalizabilit)o(y)c Fr(M)1011 846 y Fu(0)1023 865 y Fv([)p Fr(x)g Fv(:=)g Fr(N)5 b Fv(])1203 852 y Fr(~)1201 865 y(L)17 b Fv(is)f(sn.)21 b(Hence)15 b(b)o(y)h(IH)f Fr(K)21 b Fv(is)16 b(sn.)72 929 y Fn(Case)21 b Fr(K)f Fv(=)c(\()p Fr(\025x)8 b(M)d Fv(\))p Fr(N)508 911 y Fu(0)523 917 y Fr(~)521 929 y(L)18 b Fv(with)f Fr(N)22 b Fs(\000)-9 b(!)825 936 y Fj(\014)865 929 y Fr(N)909 911 y Fu(0)921 929 y Fv(.)25 b(Then)18 b(w)o(e)f(ha)o(v)o(e)f Fr(M)5 b Fv([)p Fr(x)16 b Fv(:=)g Fr(N)5 b Fv(])1513 917 y Fr(~)1511 929 y(L)16 b Fs(\000)-9 b(!)1640 911 y Fu(\003)1640 942 y Fj(\014)1680 929 y Fr(M)5 b Fv([)p Fr(x)16 b Fv(:=)-1 1000 y Fr(N)43 982 y Fu(0)55 1000 y Fv(])71 988 y Fr(~)69 1000 y(L)o Fv(.)21 b(By)14 b(de\014nition)g(of)h(strong)h (normalizabilit)o(y)11 b Fr(M)5 b Fv([)p Fr(x)14 b Fv(:=)f Fr(N)1179 982 y Fu(0)1191 1000 y Fv(])1207 988 y Fr(~)1205 1000 y(L)i Fv(and)g Fr(N)1390 982 y Fu(0)1417 1000 y Fv(are)f(sn.)21 b(Hence)14 b(b)o(y)g(IH)-1 1060 y Fr(K)20 b Fv(is)c(sn.)72 1121 y Fn(Case)21 b Fr(K)e Fv(=)d(\()p Fr(\025x)8 b(M)d Fv(\))p Fr(N)509 1108 y(~)507 1121 y(L)540 1103 y Fu(0)570 1121 y Fv(with)17 b Fr(L)715 1128 y Fj(i)744 1121 y Fs(\000)-8 b(!)825 1128 y Fj(\014)864 1121 y Fr(L)897 1103 y Fu(0)897 1133 y Fj(i)928 1121 y Fv(for)18 b Fr(i)e Fv(and)i Fr(L)1166 1128 y Fj(j)1200 1121 y Fv(=)d Fr(L)1286 1103 y Fu(0)1286 1133 y Fj(j)1322 1121 y Fv(for)j Fr(j)g Fs(6)p Fv(=)d Fr(i)p Fv(.)24 b(Then)17 b(w)o(e)g(ha)o(v)o(e)-1 1192 y Fr(M)5 b Fv([)p Fr(x)15 b Fv(:=)h Fr(N)5 b Fv(])236 1179 y Fr(~)234 1192 y(L)16 b Fs(\000)-9 b(!)363 1199 y Fj(\014)402 1192 y Fr(M)5 b Fv([)p Fr(x)16 b Fv(:=)f Fr(N)5 b Fv(])639 1179 y Fr(~)637 1192 y(L)670 1174 y Fu(0)682 1192 y Fv(.)25 b(By)17 b(de\014nition)g(of)h(strong)g (normalizabilit)o(y)c Fr(M)5 b Fv([)p Fr(x)16 b Fv(:=)f Fr(N)5 b Fv(])1798 1179 y Fr(~)1796 1192 y(L)1829 1174 y Fu(0)-1 1252 y Fv(is)16 b(sn.)21 b(Hence)15 b(b)o(y)h(IH)f Fr(K)21 b Fv(is)16 b(sn.)p 1821 1222 V 1821 1250 2 28 v 1839 1250 V 1821 1252 21 2 v -1 1366 a Ft(Corollary)i(2.4)24 b Fn(If)17 b Fr(M)5 b Fv([)p Fr(x)13 b Fv(:=)g Fr(N)5 b Fv(])18 b Fn(is)f(sc)h(for)f(al)r(l)h(sc)g Fr(N)5 b Fn(,)18 b(then)g(also)g Fr(\025x)8 b(M)23 b Fn(is)17 b(sc.)72 1480 y(Pr)n(o)n(of)9 b Fv(.)22 b(Let)17 b Fr(M)5 b Fv([)p Fr(x)14 b Fv(:=)g Fr(N)5 b Fv(])16 b(b)q(e)h(sc)g(for)g(all)f (sc)g Fr(N)5 b Fv(.)23 b(W)l(e)16 b(ha)o(v)o(e)g(to)h(sho)o(w)g(that)h Fr(\025x)8 b(M)22 b Fv(is)16 b(sc.)23 b(So)17 b(let)-1 1545 y Fr(N)j Fv(and)154 1532 y Fr(~)152 1545 y(L)c Fv(b)q(e)g(sc)f (suc)o(h)g(that)h(\()p Fr(\025x)8 b(M)d Fv(\))p Fr(N)737 1532 y(~)735 1545 y(L)17 b Fv(is)e(of)h(ground)g(t)o(yp)q(e.)21 b(W)l(e)15 b(m)o(ust)f(sho)o(w)i(that)g(\()p Fr(\025x)8 b(M)d Fv(\))p Fr(N)1809 1532 y(~)1807 1545 y(L)-1 1610 y Fv(is)17 b(sc.)26 b(Since)17 b Fr(M)5 b Fv([)p Fr(x)16 b Fv(:=)g Fr(N)5 b Fv(])18 b(is)f(sc)h(b)o(y)g(assumption,)f Fr(M)5 b Fv([)p Fr(x)16 b Fv(:=)g Fr(N)5 b Fv(])1203 1597 y Fr(~)1201 1610 y(L)18 b Fv(is)g(sc)f(to)q(o)i(and)g(hence)e (also)h(sn.)-1 1674 y(Since)g(b)o(y)g(lemma)e(2.1a)k Fr(N)k Fv(is)19 b(also)g(sn,)h(b)o(y)e(lemma)e(2.3)j(it)g(follo)o(ws)g (that)g(\()p Fr(\025x)8 b(M)d Fv(\))p Fr(N)1594 1662 y(~)1592 1674 y(L)20 b Fv(is)f(sn)h(and)-1 1734 y(hence)15 b(also)i(sc.)p 1821 1705 V 1821 1733 2 28 v 1839 1733 V 1821 1735 21 2 v -1 1849 a Ft(Lemm)o(a)f(2.5)24 b Fn(Every)18 b(term)f Fr(M)23 b Fn(is)17 b(sc)h(under)g(substitution.)72 1963 y(Pr)n(o)n(of)9 b Fv(.)35 b(By)21 b(induction)f(on)i Fr(M)5 b Fv(.)36 b Fn(Case)25 b Fr(x)p Fv(.)36 b(The)21 b(claim)e(follo)o(ws)i(from)f(lemm)o(a)f(2.1b)i(or)h(b)o(y)-1 2023 y(assumption.)72 2083 y Fn(Case)i Fr(M)5 b(N)g Fv(.)351 2071 y Fr(~)342 2083 y(K)25 b Fv(b)q(e)20 b(sc.)33 b(W)l(e)20 b(ha)o(v)o(e)g(to)h(sho)o(w)g(that)f Fr(M)5 b Fv([)o Fr(~)-23 b(x)21 b Fv(:=)1265 2071 y Fr(~)1256 2083 y(K)t Fv(])p Fr(N)5 b Fv([)o Fr(~)-23 b(x)20 b Fv(:=)1503 2071 y Fr(~)1493 2083 y(K)t Fv(])g(are)h(sc.)33 b(This)-1 2148 y(clearly)14 b(holds,)j(since)e(b)o(y)h(IH)f Fr(M)5 b Fv([)o Fr(~)-23 b(x)14 b Fv(:=)735 2135 y Fr(~)726 2148 y(K)t Fv(])i(as)h(w)o(ell)e(as)i Fr(N)5 b Fv([)o Fr(~)-23 b(x)13 b Fv(:=)1194 2135 y Fr(~)1184 2148 y(K)t Fv(])j(are)g(sc.)72 2213 y Fn(Case)27 b Fr(\025x)8 b(M)d Fv(.)383 2200 y Fr(~)374 2213 y(K)27 b Fv(b)q(e)d(sc.)42 b(W)l(e)23 b(ha)o(v)o(e)f(to)i(sho)o(w)g(that)g Fr(\025x)8 b Fv(\()p Fr(M)d Fv([)o Fr(~)-23 b(x)25 b Fv(:=)1420 2200 y Fr(~)1411 2213 y(K)t Fv(]\))e(is)g(sc.)42 b(W)l(e)23 b(no)o(w)-1 2277 y(apply)18 b(corollary)f(2.4.)28 b(Let)18 b Fr(N)23 b Fv(b)q(e)c(sc.)27 b(By)17 b(IH)g(for)i Fr(M)k Fv(also)c Fr(M)5 b Fv([)p Fr(x;)i(~)-23 b(x)16 b Fv(:=)h Fr(N)r(;)1442 2265 y(~)1433 2277 y(K)t Fv(])h(is)g(sc.)27 b(Hence)17 b(b)o(y)-1 2337 y(corollary)e(2.4)i(the)f(claim)e(follo)o (ws.)p 1821 2308 V 1821 2336 2 28 v 1839 2336 V 1821 2338 21 2 v 72 2398 a(F)l(rom)h(lemm)o(a)f(2.5)j(and)f(lemma)e(2.1)i(w) o(e)g(directly)e(get)-1 2512 y Ft(Theorem)i(2.6)24 b Fs(\000)-8 b(!)413 2519 y Fj(\014)453 2512 y Fn(is)18 b(terminating,)g(i.e.)g(every)g(term)f Fr(M)23 b Fn(is)17 b(sn.)p eop %%Page: 5 5 5 4 bop -1 53 a Fn(Extension)19 b(of)e(the)h(T)l(ermination)g(Pr)n(o)n (of)e(to)h(G\177)-25 b(odel's)18 b(System)g Fr(T)-1 146 y Fv(This)24 b(pro)q(of)h(can)f(easily)g(b)q(e)g(extended)f(to)i(terms) d(with)i(pairing)g Fs(h)p Fr(M)1351 153 y Fi(0)1372 146 y Fr(;)8 b(M)1441 153 y Fi(1)1460 146 y Fs(i)25 b Fv(and)f(pro)s (jections)-1 206 y Fr(\031)27 213 y Fi(0)46 206 y Fv(\()p Fr(M)5 b Fv(\),)19 b Fr(\031)197 213 y Fi(1)217 206 y Fv(\()p Fr(M)5 b Fv(\).)28 b(W)l(e)19 b(no)o(w)g(sho)o(w)g(that)g (addition)g(of)g(the)f(con)o(v)o(ersion)g(rules)g(ab)q(o)o(v)o(e)h(for) g Fs(R)f Fv(do)q(es)-1 266 y(not)e(destro)o(y)g(termination.)72 326 y(W)l(e)h(\014rst)h(c)o(hange)g(the)f(de\014nition)h(of)g(sc)f(for) h(the)g(ground)g(t)o(yp)q(e)g Fr(\023)p Fv(.)25 b(It)18 b(is)f(not)h(de\014ned)g(just)g(to)-1 386 y(b)q(e)e(sn)h(\(as)f(b)q (efore\),)g(but)h(no)o(w)f(is)g(de\014ned)g(inductiv)o(ely)l(,)e(as)i (follo)o(ws.)-1 501 y Ft(De\014nition)h(2.7)24 b Fr(M)f Fn(is)17 b(sc,)h(if)71 602 y Fs(\017)25 b Fn(al)r(l)18 b Fr(M)242 584 y Fu(0)272 602 y Fn(such)g(that)f Fr(M)i Fs(\000)-8 b(!)629 609 y Fj(\014)666 602 y Fr(M)718 584 y Fu(0)748 602 y Fn(ar)n(e)16 b(sc,)i(and)g(in)g(addition)71 704 y Fs(\017)25 b Fn(if)17 b Fr(M)i Fv(=)14 b(S)p Fr(M)360 711 y Fi(0)380 704 y Fn(,)j(then)i Fr(M)568 711 y Fi(0)605 704 y Fn(is)e(sc.)-1 818 y Ft(Theorem)f(2.8)24 b Fs(\000)-8 b(!)413 825 y Fj(\014)r Fu(R)484 818 y Fn(is)17 b(terminating.)72 932 y(Pr)n(o)n(of)9 b Fv(.)20 b(W)l(e)12 b(extend)f(the)h(argumen)o(t)g (ab)q(o)o(v)o(e.)20 b(Clearly)11 b(it)h(su\016ces)g(to)h(sho)o(w)g (that)f(the)g(constan)o(ts)-1 993 y Fs(R)41 1000 y Fj(\023;\032)103 993 y Fv(and)21 b Fs(R)244 1000 y Fk(o)r Fj(;\032)317 993 y Fv(are)f(sc.)32 b(W)l(e)19 b(restrict)g(ourselv)o(es)h(to)g Fs(R)1064 1000 y Fj(\023;\032)1107 993 y Fv(;)h(for)f Fs(R)1262 1000 y Fk(o)r Fj(;\032)1335 993 y Fv(the)g(argumen)o(t)f(is)g (similar)-1 1053 y(\(and)d(simpler\).)j(So)e(let)f Fr(M)r(;)8 b(N)r(;)g(K)21 b Fv(b)q(e)16 b(sc.)21 b(W)l(e)16 b(m)o(ust)f(sho)o(w)i (that)g Fs(R)p Fr(M)5 b(N)g(K)21 b Fv(is)16 b(sc.)72 1117 y(The)f(pro)q(of)h(is)f(b)o(y)f(induction)h(on)h(sn)f(for)g Fr(M)r(;)8 b(N)21 b Fv(and)16 b(on)f(sc)g(for)h Fr(K)t Fv(.)21 b(So)15 b(let)1466 1105 y Fr(~)1465 1117 y(L)g Fv(b)q(e)g(sc.)21 b(W)l(e)15 b(m)o(ust)-1 1178 y(sho)o(w)f(that)g Fs(R)p Fr(M)5 b(N)g(K)405 1165 y(~)403 1178 y(L)14 b Fv(is)g(sc.)20 b(Since)13 b(this)g(term)f(is)h(not)h(of)g(the)f(form)g (S)p Fr(M)1354 1185 y Fi(0)1374 1178 y Fv(,)g(it)g(su\016ces)h(to)f (consider)-1 1238 y(all)i(reducts)h Fr(Q)g Fv(of)h Fs(R)p Fr(M)5 b(N)g(K)533 1225 y(~)531 1238 y(L)17 b Fv(and)g(to)g(sho)o(w)f (that)h(ev)o(ery)e(suc)o(h)h(reduct)g Fr(Q)g Fv(is)g(sc.)72 1298 y Fn(Case)i Fr(K)g Fv(=)13 b Fr(K)343 1305 y Fi(0)370 1298 y Fv(+)7 b(1,)14 b Fr(Q)g Fv(=)f Fr(N)5 b(K)656 1305 y Fi(0)677 1298 y Fv(\()p Fs(R)p Fr(M)g(N)g(K)875 1305 y Fi(0)896 1298 y Fv(\))917 1285 y Fr(~)915 1298 y(L)p Fv(.)21 b(W)l(e)13 b(\014rst)i(sho)o(w)f(that)h Fs(R)p Fr(M)5 b(N)g(K)1564 1305 y Fi(0)1599 1298 y Fv(is)14 b(sc.)20 b(So)15 b(let)1 1350 y Fr(~)-1 1363 y(L)32 1345 y Fu(0)60 1363 y Fv(b)q(e)i(sc.)23 b(Since)16 b Fr(K)j Fv(=)c Fr(K)487 1370 y Fi(0)519 1363 y Fv(+)c(1)18 b(is)e(sc,)h(b)o(y)f (de\014nition)g(also)i Fr(K)1156 1370 y Fi(0)1193 1363 y Fv(is.)23 b(So)17 b(b)o(y)g(induction)f(h)o(yp)q(othesis)-1 1423 y Fs(R)p Fr(M)5 b(N)g(K)178 1430 y Fi(0)215 1423 y Fv(is)16 b(sc,)g(and)h(w)o(e)e(obtain)i(that)g Fr(Q)f Fv(is)g(sc.)72 1483 y(If)d(the)g(reduction)g(tak)o(es)g(place)g(within) g(a)h(subterm)e Fr(M)r(;)c(N)r(;)g(K)q(;)1232 1471 y(~)1229 1483 y(L)15 b Fv(the)f(claim)d(follo)o(ws)i(b)o(y)g(induc-)-1 1543 y(tion)j(h)o(yp)q(othesis)g(\(here)g(w)o(e)g(need)f(that)i(strong) g(computabilit)o(y)d(is)i(preserv)o(ed)f(under)h(con)o(v)o(ersion)-1 1608 y(steps;)i(cf.)e(lemma)f(2.2\).)25 b(Since)17 b(the)g(case)g Fr(K)j Fv(=)c(0,)i Fr(Q)e Fv(=)g Fr(M)1135 1595 y(~)1133 1608 y(L)i Fv(is)f(trivial)f(this)i(pro)o(v)o(es)f(the)g(claim.)p -1 1639 21 2 v -1 1667 2 28 v 17 1667 V -1 1669 21 2 v 72 1728 a(No)o(w)i(w)o(e)g(can)g(conclude)g(via)g(Newman's)e(Lemma)g ([9])i(that)h(the)f(normal)f(form)h(is)g(uniquely)-1 1789 y(determined.)26 b(F)l(or)19 b(simplicit)o(y)c(w)o(e)k(iden)o (tify)e(terms)g(with)i(the)g(same)f Fr(\014)s Fs(R)p Fv(-normal)f(form.)28 b(Hence)-1 1849 y(ev)o(ery)19 b(closed)h(term)f (of)i(t)o(yp)q(e)f Fr(\023)h Fv(is)f(iden)o(ti\014ed)f(with)h(a)h(term) e(of)i(the)f(form)g Fr(S)s Fv(\()p Fr(S)s Fv(\()p Fr(S)11 b(:)d(:)g(:)f Fv(\()p Fr(S)s Fv(0\))h Fr(:)g(:)g(:)p Fv(\)\))-1 1909 y(and)18 b(ev)o(ery)e(closed)h(term)f(of)i(t)o(yp)q(e)f Fl(o)j Fv(is)e(iden)o(ti\014ed)e(with)h(either)f Fl(true)k Fv(or)e Fl(false)s Fv(.)25 b(Suc)o(h)17 b(terms)f(are)-1 1969 y(denoted)g(b)o(y)g Fr(n)p 251 1976 30 2 v 16 w Fv(and)h(called)e Fn(numer)n(als)21 b Fv(\(ev)o(en)15 b(if)g(they)h(are)g(of)h(t)o(yp)q(e)f Fl(o)s Fv(\).)-1 2099 y Fn(2.2)49 b(Intuitionistic)19 b(A)o(rithmetic)f(for)f(F)l (unctionals)-1 2209 y Fv(The)f(system)f(w)o(e)h(consider)g(is)h(essen)o (tially)e(Heyting's)g(in)o(tuitionistic)f(arithmetic)g(in)i(\014nite)g (t)o(yp)q(es)-1 2269 y Fl(HA)72 2248 y Fj(!)116 2269 y Fv(as)k(describ)q(ed)f(e.g.)f(in)h([4].)29 b(It)19 b(is)g(based)h(on)f(G\177)-24 b(odel's)19 b(system)f Fr(T)26 b Fv(and)19 b(just)h(adds)g(the)f(cor-)-1 2329 y(resp)q(onding)i(logical)f(and)h(arithmetical)c(apparatus)22 b(to)f(it.)33 b(Classical)20 b(arithmetic)e(is)i(obtained)-1 2389 y(b)o(y)e(restriction)g(to)h(form)o(ulas)e(without)i(the)g (constructiv)o(e)e(existen)o(tial)g(quan)o(ti\014er)h Fs(9)1600 2371 y Fu(\003)1638 2389 y Fv(but)h(using)-1 2449 y(the)f(classical)h(de\014nition)f Fs(9)g Fv(=)h Fs(:8:)f Fv(instead.)29 b(Equations)20 b(are)f(treated)g(on)g(the)g (meta)f(lev)o(el)f(b)o(y)-1 2510 y(iden)o(tifying)d(terms)h(with)h(the) g(same)f(normal)g(form.)72 2570 y(W)l(e)k(no)o(w)g(write)g Fr(r)o(;)8 b(s;)g(t;)g(:)g(:)g(:)17 b Fv(for)i(\(ob)s(ject\))f(terms,)g (and)i(reserv)o(e)e Fr(M)r(;)8 b(N)r(;)g(K)q(;)g(:)g(:)g(:)19 b Fv(for)g(deriv)m(ation)-1 2630 y(terms.)p eop %%Page: 6 6 6 5 bop -1 53 a Fn(A)o(rithmetic:)22 b(Pr)n(e)n(dic)n(ate)17 b(symb)n(ols)g(and)h(atomic)f(formulas)-1 146 y Fv(Ev)o(ery)e (predicate)h(sym)o(b)q(ol)f Fr(P)24 b Fv(no)o(w)17 b(has)g(a)g(\014xed) f(arit)o(y)l(,)f(whic)o(h)h(is)h(a)g(tup)q(el)f(of)h(t)o(yp)q(es)f(\()p Fr(\032)1633 153 y Fi(1)1653 146 y Fr(;)8 b(:)g(:)g(:)f(;)h(\032)1787 153 y Fj(k)1809 146 y Fv(\).)-1 206 y(So)14 b(atomic)f(form)o(ulas)f (are)i(of)g(the)g(form)f Fr(P)7 b Fv(\()p Fr(r)824 182 y Fj(\032)842 187 y Fh(1)823 217 y Fi(1)862 206 y Fr(;)h(:)g(:)g(:)f(;) h(r)994 182 y Fj(\032)1012 188 y Fg(k)993 218 y Fj(k)1034 206 y Fv(\).)20 b(The)14 b(c)o(hoice)e(of)j(the)e(predicate)g(sym)o(b)q (ols)-1 266 y(dep)q(ends)21 b(on)g(the)f(particular)h(problem)e(under)h (consideration.)35 b(In)20 b(most)g(cases)h(there)f(will)g(b)q(e)-1 326 y(the)j(predicate)g(sym)o(b)q(ols)g Fs(?)h Fv(\(falsit)o(y\))e(of)j (arit)o(y)e(\(\))g(and)i Fl(atom)e Fv(of)h(arit)o(y)f(\()p Fl(o)s Fv(\).)44 b(The)24 b(in)o(tended)-1 386 y(in)o(terpretation)18 b(of)i Fl(atom)g Fv(is)f(the)h(set)f Fs(f)p Fl(true)s Fs(g)p Fv(.)31 b(Hence)19 b(\\)p Fl(atom)p Fv(\()p Fr(t)p Fv(\)")g(means)g(\\)p Fr(t)h Fv(=)g Fl(true)r Fv(".)32 b(Ev)o(ery)-1 447 y(decidable)14 b(relation)g(\(i.e.,)f(ev)o(ery)h (relation)h(giv)o(en)f(b)o(y)h(a)g(term)f Fr(t)g Fv(of)i(t)o(yp)q(e)e Fl(o)s Fv(\),)h(can)g(then)g(b)q(e)h(written)-1 507 y(in)k(the)g(form)g Fl(atom)o Fv(\()p Fr(t)p Fv(\).)34 b(If)20 b(confusion)h(is)g(unlik)o (ely)l(,)e(w)o(e)h(will)f(write)h Fr(t)h Fv(instead)f(of)h Fl(atom)p Fv(\()p Fr(t)p Fv(\).)34 b(So)-1 567 y(form)o(ulas)15 b(are)411 627 y Fr(P)7 b Fv(\()p Fr(r)491 604 y Fj(\032)509 609 y Fh(1)490 638 y Fi(1)529 627 y Fr(;)h(:)g(:)g(:)g(;)g(r)662 604 y Fj(\032)680 610 y Fg(k)661 640 y Fj(k)701 627 y Fv(\))14 b Fs(j)f Fr(A)e Fs(^)g Fr(B)17 b Fs(j)c Fr(A)h Fs(!)f Fr(B)k Fs(j)d(8)p Fr(x)1187 607 y Fj(\032)1205 627 y Fr(A)f Fs(j)h(9)1311 607 y Fu(\003)1331 627 y Fr(x)1359 607 y Fj(\032)1378 627 y Fr(A:)72 714 y Fv(T)l(o)j(accomo)q(date)f(the) g(sp)q(eci\014c)g(ground)h(t)o(yp)q(es)f Fr(\023)h Fv(and)g Fl(o)s Fv(,)f(w)o(e)g(need)g(an)h(induction)f(sc)o(heme)e(for)-1 775 y(b)q(oth)j(t)o(yp)q(es,)e(and)i(in)f(addition)g(a)h(\\truth)g (axiom")e(.)329 880 y Fl(Ind)402 887 y Fj(p;A)458 880 y Fv(:)90 b Fr(A)p Fv([)p Fr(p)14 b Fv(:=)f Fl(true)r Fv(])h Fs(!)f Fr(A)p Fv([)p Fr(p)h Fv(:=)f Fl(false)s Fv(])g Fs(!)h(8)p Fr(pA)325 941 y Fl(Ind)399 948 y Fj(n;A)458 941 y Fv(:)90 b Fr(A)p Fv([)p Fr(n)13 b Fv(:=)h(0])f Fs(!)h Fv(\()p Fs(8)p Fr(n:A)e Fs(!)h Fr(A)p Fv([)p Fr(n)h Fv(:=)f Fr(n)e Fv(+)g(1]\))j Fs(!)f(8)p Fr(nA)420 1001 y Fl(T)t Fv(:)89 b Fl(atom)p Fv(\()p Fl(true)r Fv(\))-1 1107 y(W)l(e)16 b(also)g(need)g Fs(9)322 1089 y Fu(\003)342 1107 y Fv(-axioms:)369 1204 y Fs(9)397 1183 y Fu(\003)p Fi(+)397 1216 y Fj(x;A)454 1204 y Fv(:)58 b Fs(8)p Fr(x:A)11 b Fs(!)j(9)737 1185 y Fu(\003)756 1204 y Fr(xA)331 1264 y Fs(9)359 1244 y Fu(\003\000)359 1276 y Fj(x;A;B)454 1264 y Fv(:)58 b Fs(9)554 1246 y Fu(\003)573 1264 y Fr(x)601 1246 y Fj(\032)621 1264 y Fr(A)13 b Fs(!)h Fv(\()p Fs(8)p Fr(x)811 1246 y Fj(\032)830 1264 y Fr(:A)f Fs(!)g Fr(B)s Fv(\))h Fs(!)f Fr(B)100 b Fv(\()p Fr(x)20 b(=)-30 b Fs(2)14 b Fl(FV)6 b Fv(\()p Fr(B)s Fv(\)\))-1 1371 y Fn(Derivations)20 b Fv(are)d(within)f(minim)o(al)d(logic.)21 b(They)16 b(are)h(written)e(in)h(natural)h(deduction)f(st)o(yle,)f(i.e.)-1 1432 y(as)h(t)o(yp)q(ed)g Fr(\025)p Fv(-terms)g(via)g(the)g(w)o (ell-kno)o(wn)f(Curry-Ho)o(w)o(ard)i(corresp)q(ondence.)595 1537 y Fr(u)623 1519 y Fj(B)702 1537 y Fv(\(assumptions\))d Fs(j)g Fv(axioms)e Fs(j)595 1598 y(h)p Fr(M)666 1580 y Fj(A)696 1598 y Fr(;)c(N)762 1580 y Fj(B)792 1598 y Fs(i)811 1580 y Fj(A)p Fu(^)p Fj(B)906 1598 y Fs(j)13 b Fr(\031)961 1605 y Fj(i)975 1598 y Fv(\()p Fr(M)1046 1580 y Fj(A)1072 1585 y Fh(0)1090 1580 y Fu(^)p Fj(A)1140 1585 y Fh(1)1159 1598 y Fv(\))1178 1580 y Fj(A)1204 1585 y Fg(i)1234 1598 y Fs(j)595 1658 y Fv(\()p Fr(\025u)670 1640 y Fj(A)699 1658 y Fr(M)751 1640 y Fj(B)782 1658 y Fv(\))801 1640 y Fj(A)p Fu(!)p Fj(B)907 1658 y Fs(j)g Fv(\()p Fr(M)1005 1640 y Fj(A)p Fu(!)p Fj(B)1098 1658 y Fr(N)1142 1640 y Fj(A)1170 1658 y Fv(\))1189 1640 y Fj(B)1234 1658 y Fs(j)595 1719 y Fv(\()p Fr(\025x)670 1701 y Fj(\032)691 1719 y Fr(M)743 1701 y Fj(A)772 1719 y Fv(\))791 1701 y Fu(8)p Fj(x)832 1689 y Fg(\032)848 1701 y Fj(A)890 1719 y Fs(j)h Fv(\()p Fr(M)989 1701 y Fu(8)p Fj(x)1030 1689 y Fg(\032)1047 1701 y Fj(A)1075 1719 y Fr(t)1093 1701 y Fj(\032)1113 1719 y Fv(\))1132 1701 y Fj(A)p Fi([)p Fj(x)1188 1689 y Fg(\032)1206 1701 y Fi(:=)p Fj(t)1256 1689 y Fg(\032)1274 1701 y Fi(])-1 1832 y Fv(where)i(in)f(the)h Fs(8)p Fv(-in)o(tro)q(duction)f Fr(\025xM)711 1814 y Fj(A)741 1832 y Fv(,)g Fr(x)h Fv(m)o(ust)f(not)i (b)q(e)f(free)g(in)g(an)o(y)g Fr(B)j Fv(with)d Fr(u)1526 1814 y Fj(B)1570 1832 y Fs(2)e Fl(F)-5 b(A)o Fv(\()p Fr(M)5 b Fv(\).)-1 1962 y Fn(Classic)n(al)17 b(lo)n(gic)-1 2054 y Fv(Assume)f(that)j Fl(atom)e Fv(is)h(the)g(only)g(predicate)f (sym)o(b)q(ol,)g(and)h(replace)f Fs(?)h Fv(b)o(y)g Fl(atom)o Fv(\()p Fl(false)r Fv(\).)27 b(Then)-1 2114 y(w)o(e)15 b(ha)o(v)o(e)664 2160 y Fs(:)p Fr(A)42 b Fv(:=)13 b Fr(A)g Fs(!)h Fl(atom)o Fv(\()p Fl(false)s Fv(\))642 2221 y Fs(9)p Fr(xA)41 b Fv(:=)13 b Fs(:8)p Fr(x)p Fs(:)p Fr(A;)-1 2304 y Fv(and)k(stabilit)o(y)e Fs(::)p Fr(A)g Fs(!)f Fr(A)i Fv(is)h(pro)o(v)m(able)f(for)h(all)g Fs(9)936 2286 y Fu(\003)955 2304 y Fv(-free)f(form)o(ulas)g Fr(A)p Fv(,)g(using)h(b)q(o)q(olean)h(induction)-1 2365 y(for)g(the)g(case)h Fl(atom)o Fv(\()p Fr(t)p Fv(\).)27 b(Hence)17 b(classical)g(arithmetic) f(\(in)i(all)g(\014nite)g(t)o(yp)q(es\))g(is)g(a)h(subsystem)e(of)-1 2425 y(our)f(presen)o(t)g(system)f(based)h(on)h(minimal)c(logic.)72 2485 y(So)19 b(for)h Fs(9)248 2467 y Fu(\003)267 2485 y Fv(-free)f(form)o(ulas)f(\(no)i(restriction)e(from)g(a)h(classical)g (p)q(oin)o(t)g(of)h(view\))e(w)o(e)h(ha)o(v)o(e)f(full)-1 2545 y(classical)d(logic.)72 2605 y(Note)h(also)g(that)h(for)g(quan)o (ti\014er-free)e(form)o(ulas)g Fr(B)k Fv(built)c(from)g(prime)g(form)o (ulas)g(of)h(the)g(form)-1 2665 y Fl(atom)o Fv(\()p Fr(t)p Fv(\))g(w)o(e)g(can)g(easily)f(construct)i(a)f(b)q(o)q(olean)i(term)c Fr(t)1045 2672 y Fj(B)1075 2665 y Fv(:)8 b Fl(o)19 b Fv(suc)o(h)d(that)764 2776 y Fl(atom)p Fv(\()p Fr(t)910 2783 y Fj(B)940 2776 y Fv(\))d Fs($)h Fr(B)-1 2886 y Fv(is)22 b(deriv)m(able.)40 b(Therefore)23 b(w)o(e)f(can)h(use)g(b)q(o) q(olean)h(induction)f(to)g(deriv)o(e)e Fn(c)n(ase)j(distinction)k Fv(for)-1 2946 y(quan)o(ti\014er-free)15 b(form)o(ulas.)p eop %%Page: 7 7 7 6 bop -1 53 a Fn(2.3)49 b(Pr)n(o)n(gr)n(am)15 b(Extr)n(action)j(fr)n (om)e(Constructive)j(Pr)n(o)n(ofs)-1 163 y Fv(W)l(e)14 b(no)o(w)i(come)d(bac)o(k)i(to)g(the)g(full)f(system,)f(and)j(assign)g (to)f(ev)o(ery)e(form)o(ula)h Fr(A)h Fv(an)g(ob)s(ject)g Fr(\034)6 b Fv(\()p Fr(A)p Fv(\))14 b(\(a)-1 223 y(t)o(yp)q(e)h(or)i (the)f(sym)o(b)q(ol)e Fs(\003)p Fv(\).)21 b Fr(\034)6 b Fv(\()p Fr(A)p Fv(\))16 b(is)g(in)o(tended)f(to)h(b)q(e)g(the)g(t)o (yp)q(e)g(of)g(the)g(program)g(to)h(b)q(e)f(extracted)-1 283 y(from)g(a)h(pro)q(of)i(of)e Fr(A)p Fv(.)24 b(In)17 b(case)h Fr(\034)6 b Fv(\()p Fr(A)p Fv(\))14 b(=)i Fs(\003)h Fv(pro)q(ofs)i(of)e Fr(A)g Fv(ha)o(v)o(e)g(no)g(computational)g(con)o (ten)o(t;)f(suc)o(h)-1 343 y(form)o(ulas)f Fr(A)h Fv(are)g(called)f Fn(Harr)n(op)h(formulas)t Fv(.)473 449 y Fr(\034)6 b Fv(\()p Fr(P)h Fv(\()n Fr(~)-22 b(s)p Fv(\)\))41 b(:=)14 b Fs(\003)440 535 y Fr(\034)6 b Fv(\()p Fs(9)514 517 y Fu(\003)534 535 y Fr(x)562 517 y Fj(\032)581 535 y Fr(A)p Fv(\))41 b(:=)744 474 y Ff(\032)783 505 y Fr(\032)211 b Fv(if)16 b Fr(\034)6 b Fv(\()p Fr(A)p Fv(\))13 b(=)h Fs(\003)783 565 y Fr(\032)d Fs(\002)g Fr(\034)6 b Fv(\()p Fr(A)p Fv(\))48 b(otherwise)460 645 y Fr(\034)6 b Fv(\()p Fs(8)p Fr(x)563 627 y Fj(\032)581 645 y Fr(A)p Fv(\))41 b(:=)744 584 y Ff(\032)783 615 y Fs(\003)228 b Fv(if)16 b Fr(\034)6 b Fv(\()p Fr(A)p Fv(\))13 b(=)g Fs(\003)783 675 y Fr(\032)h Fs(!)g Fr(\034)6 b Fv(\()p Fr(A)p Fv(\))48 b(otherwise)404 755 y Fr(\034)6 b Fv(\()p Fr(A)487 762 y Fi(0)517 755 y Fs(^)12 b Fr(A)599 762 y Fi(1)618 755 y Fv(\))41 b(:=)744 694 y Ff(\032)783 725 y Fr(\034)6 b Fv(\()p Fr(A)866 732 y Fj(i)880 725 y Fv(\))236 b(if)15 b Fr(\034)6 b Fv(\()p Fr(A)1262 732 y Fi(1)p Fu(\000)p Fj(i)1321 725 y Fv(\))14 b(=)g Fs(\003)783 785 y Fr(\034)6 b Fv(\()p Fr(A)866 792 y Fi(0)885 785 y Fv(\))11 b Fs(\002)g Fr(\034)6 b Fv(\()p Fr(A)1048 792 y Fi(1)1067 785 y Fv(\))49 b(otherwise)419 897 y Fr(\034)6 b Fv(\()p Fr(A)13 b Fs(!)g Fr(B)s Fv(\))41 b(:=)744 797 y Ff(8)744 835 y(>)744 847 y(<)744 922 y(>)744 934 y(:)789 837 y Fr(\034)6 b Fv(\()p Fr(B)s Fv(\))227 b(if)15 b Fr(\034)6 b Fv(\()p Fr(A)p Fv(\))14 b(=)f Fs(\003)789 897 y(\003)307 b Fv(if)15 b Fr(\034)6 b Fv(\()p Fr(B)s Fv(\))14 b(=)f Fs(\003)789 957 y Fr(\034)6 b Fv(\()p Fr(A)p Fv(\))13 b Fs(!)h Fr(\034)6 b Fv(\()p Fr(B)s Fv(\))48 b(otherwise)-1 1063 y(W)l(e)18 b(no)o(w)h(de\014ne,)g(for)g(a)g(giv)o(en)f(deriv)m(ation)g Fr(M)24 b Fv(of)19 b(a)g(form)o(ula)e Fr(A)i Fv(with)f Fr(\034)6 b Fv(\()p Fr(A)p Fv(\))18 b Fs(6)p Fv(=)f Fs(\003)p Fv(,)i(its)g Fn(extr)n(acte)n(d)-1 1123 y(pr)n(o)n(gr)n(am)e Fv([)-8 b([)p Fr(M)5 b Fv(])-8 b(])14 b(of)j(t)o(yp)q(e)f Fr(\034)6 b Fv(\()p Fr(A)p Fv(\).)458 1233 y([)-8 b([)p Fr(u)506 1215 y Fj(A)533 1233 y Fv(])g(])41 b(:=)13 b Fr(x)687 1215 y Fj(\034)t Fi(\()p Fj(A)p Fi(\))687 1245 y Fj(u)827 1233 y Fv(\()p Fr(x)874 1215 y Fj(\034)t Fi(\()p Fj(A)p Fi(\))874 1245 y Fj(u)966 1233 y Fv(uniquely)h(asso)q(ciated)k (with)e Fr(u)1535 1215 y Fj(A)1563 1233 y Fv(\))378 1318 y([)-8 b([)p Fr(\025u)454 1300 y Fj(A)481 1318 y Fr(M)5 b Fv(])-8 b(])41 b(:=)659 1257 y Ff(\032)699 1288 y Fv([)-8 b([)p Fr(M)5 b Fv(])-8 b(])178 b(if)16 b Fr(\034)6 b Fv(\()p Fr(A)p Fv(\))13 b(=)g Fs(\003)699 1348 y Fr(\025x)755 1330 y Fj(\034)t Fi(\()p Fj(A)p Fi(\))755 1361 y Fj(u)830 1348 y Fv([)-8 b([)p Fr(M)5 b Fv(])-8 b(])47 b(otherwise)326 1428 y([)-8 b([)p Fr(M)398 1410 y Fj(A)p Fu(!)p Fj(B)489 1428 y Fr(N)5 b Fv(])-8 b(])41 b(:=)659 1367 y Ff(\032)699 1398 y Fv([)-8 b([)p Fr(M)5 b Fv(])-8 b(])128 b(if)16 b Fr(\034)6 b Fv(\()p Fr(A)p Fv(\))13 b(=)h Fs(\003)699 1458 y Fv([)-8 b([)p Fr(M)5 b Fv(])-8 b(][)g([)o Fr(N)5 b Fv(])-8 b(])45 b(otherwise)258 1538 y([)-8 b([)p Fs(h)p Fr(M)349 1516 y Fj(A)375 1521 y Fh(0)344 1549 y Fi(0)394 1538 y Fr(;)8 b(M)468 1516 y Fj(A)494 1521 y Fh(1)463 1549 y Fi(1)514 1538 y Fs(i)p Fv(])-8 b(])41 b(:=)659 1477 y Ff(\032)699 1508 y Fv([)-8 b([)p Fr(M)766 1515 y Fj(i)779 1508 y Fv(])g(])218 b(if)16 b Fr(\034)6 b Fv(\()p Fr(A)1145 1515 y Fi(1)p Fu(\000)p Fj(i)1203 1508 y Fv(\))14 b(=)g Fs(\003)699 1568 y(h)p Fv([)-8 b([)p Fr(M)785 1575 y Fi(0)804 1568 y Fv(])g(])p Fr(;)8 b Fv([)-8 b([)p Fr(M)913 1575 y Fi(1)930 1568 y Fv(])g(])p Fs(i)48 b Fv(otherwise)270 1648 y([)-8 b([)p Fr(\031)318 1655 y Fj(i)330 1648 y Fv(\()p Fr(M)401 1630 y Fj(A)427 1635 y Fh(0)445 1630 y Fu(^)p Fj(A)495 1635 y Fh(1)515 1648 y Fv(\)])g(])40 b(:=)659 1587 y Ff(\032)699 1618 y Fv([)-8 b([)p Fr(M)5 b Fv(])-8 b(])88 b(if)16 b Fr(\034)6 b Fv(\()p Fr(A)1007 1625 y Fi(1)p Fu(\000)p Fj(i)1065 1618 y Fv(\))14 b(=)g Fs(\003)699 1678 y Fr(\031)727 1685 y Fj(i)740 1678 y Fv([)-8 b([)p Fr(M)5 b Fv(])-8 b(])47 b(otherwise)386 1733 y([)-8 b([)p Fr(\025x)462 1715 y Fj(\032)481 1733 y Fr(M)5 b Fv(])-8 b(])41 b(:=)13 b Fr(\025x)715 1715 y Fj(\032)735 1733 y Fv([)-8 b([)p Fr(M)5 b Fv(])-8 b(])445 1793 y([)g([)p Fr(M)5 b(t)p Fv(])-8 b(])39 b(:=)13 b([)-8 b([)p Fr(M)5 b Fv(])-8 b(])p Fr(t)-1 1900 y Fv(W)l(e)11 b(also)h(need)f(extracted)f(programs)i(for)g(induction)f(and)h Fs(9)1100 1882 y Fu(\003)1119 1900 y Fv(-axioms.)19 b(F)l(or)11 b(the)h(induction)e(sc)o(heme)-1 1960 y Fl(Ind)72 1967 y Fj(n;A)132 1960 y Fv(:)e Fr(A)p Fv([)p Fr(n)13 b Fv(:=)g(0])h Fs(!)g Fv(\()p Fs(8)p Fr(n:A)d Fs(!)j Fr(A)p Fv([)p Fr(n)f Fv(:=)g Fr(n)f Fv(+)f(1]\))i Fs(!)h(8)p Fr(nA)h Fv(let)455 2070 y([)-8 b([)p Fl(Ind)547 2077 y Fj(n;A)607 2070 y Fv(])g(])12 b(:=)i Fs(R)747 2077 y Fj(\023;\032)789 2070 y Fv(:)8 b Fr(\032)14 b Fs(!)g Fv(\()p Fr(\023)g Fs(!)g Fr(\032)g Fs(!)f Fr(\032)p Fv(\))h Fs(!)g Fr(\023)g Fs(!)g Fr(\032;)-1 2180 y Fv(where)i Fr(\032)e Fv(=)f Fr(\034)6 b Fv(\()p Fr(A)p Fv(\).)21 b(Similarly)13 b(b)q(o)q(olean)18 b(induction)d(is)h(realized)f(b)o(y)h Fs(R)1310 2187 y Fk(o)r Fj(;\032)1363 2180 y Fv(.)72 2240 y(F)l(or)g(the)g Fs(9)271 2222 y Fu(\003)291 2240 y Fv(-axioms)f(w)o(e)h(set)281 2361 y([)-8 b([)p Fs(9)329 2341 y Fu(\003)p Fi(+)329 2374 y Fj(x)349 2364 y Fg(\032)366 2374 y Fj(;A)404 2361 y Fv(])g(])40 b(:=)530 2301 y Ff(\032)569 2331 y Fr(\025x)625 2313 y Fj(\032)645 2331 y Fr(x)265 b Fv(if)15 b Fr(\034)6 b Fv(\()p Fr(A)p Fv(\))13 b(=)h Fs(\003)569 2391 y Fr(\025x)625 2373 y Fj(\032)645 2391 y Fr(\025y)699 2373 y Fj(\034)t Fi(\()p Fj(A)p Fi(\))775 2391 y Fs(h)p Fr(x;)8 b(y)r Fs(i)49 b Fv(otherwise)243 2479 y([)-8 b([)p Fs(9)291 2458 y Fu(\003\000)291 2491 y Fj(x)311 2481 y Fg(\032)328 2491 y Fj(;A;B)404 2479 y Fv(])g(])40 b(:=)530 2406 y Ff(\()571 2451 y Fr(\025x)627 2433 y Fj(\032)648 2451 y Fr(\025f)705 2433 y Fj(\032)p Fu(!)p Fj(\034)t Fi(\()p Fj(B)r Fi(\))836 2451 y Fr(f)5 b(x)462 b Fv(if)16 b Fr(\034)6 b Fv(\()p Fr(A)p Fv(\))13 b(=)g Fs(\003)571 2512 y Fr(\025z)624 2494 y Fj(\032)p Fu(\002)p Fj(\034)t Fi(\()p Fj(A)p Fi(\))746 2512 y Fr(\025f)803 2494 y Fj(\032)p Fu(!)p Fj(\034)t Fi(\()p Fj(A)p Fi(\))p Fu(!)p Fj(\034)t Fi(\()p Fj(B)r Fi(\))1043 2512 y Fr(:f)5 b(\031)1114 2519 y Fi(0)1133 2512 y Fv(\()p Fr(z)r Fv(\))p Fr(\031)1224 2519 y Fi(1)1243 2512 y Fv(\()p Fr(z)r Fv(\))49 b(otherwise)-1 2623 y(F)l(or)16 b(deriv)m(ations)f Fr(M)385 2605 y Fj(A)430 2623 y Fv(where)g Fr(\034)6 b Fv(\()p Fr(A)p Fv(\))13 b(=)h Fs(\003)i Fv(\(i.e.)e Fr(A)h Fv(is)h(a)g(Harrop-form)o(ula\))f(w)o(e)g(de\014ne)h([)-8 b([)p Fr(M)5 b Fv(])-8 b(])11 b(:=)j Fr(")h Fv(\()p Fr(")-1 2683 y Fv(some)g(new)h(sym)o(b)q(ol\).)k(This)c(applies)g(in)g (particular)g(if)g Fr(A)g Fv(is)g Fs(9)1157 2665 y Fu(\003)1176 2683 y Fv(-free.)72 2744 y(Finally)22 b(w)o(e)h(de\014ne)h(the)f (notion)h(of)g Fn(mo)n(di\014e)n(d)f(r)n(e)n(alizability)t Fv(.)44 b(More)23 b(precisely)l(,)g(w)o(e)g(de\014ne)-1 2804 y(form)o(ulas)14 b Fr(r)h Ft(mr)e Fr(A)p Fv(,)h(where)i Fr(A)f Fv(is)g(a)h(form)o(ula)e(and)j Fr(r)g Fv(is)e(either)g(a)h(term) d(of)j(t)o(yp)q(e)f Fr(\034)6 b Fv(\()p Fr(A)p Fv(\))15 b(if)g(the)h(latter)p eop %%Page: 8 8 8 7 bop -1 53 a Fv(is)16 b(a)g(t)o(yp)q(e,)g(or)g(the)g(sym)o(b)q(ol)f Fr(")h Fv(if)g Fr(\034)6 b Fv(\()p Fr(A)p Fv(\))13 b(=)h Fs(\003)p Fv(.)289 148 y Fr(")g Ft(mr)e Fr(P)7 b Fv(\()n Fr(~)-22 b(s)p Fv(\))56 b(=)27 b Fr(P)7 b Fv(\()n Fr(~)-22 b(s)p Fv(\))238 234 y Fr(r)15 b Ft(mr)e Fv(\()p Fs(9)406 216 y Fu(\003)425 234 y Fr(xA)p Fv(\))55 b(=)629 173 y Ff(\032)669 204 y Fr(")13 b Ft(mr)g Fr(A)p Fv([)p Fr(x)f Fv(:=)i Fr(r)q Fv(])219 b(if)16 b Fr(\034)6 b Fv(\()p Fr(A)p Fv(\))13 b(=)h Fs(\003)669 264 y Fr(\031)697 271 y Fi(1)716 264 y Fv(\()p Fr(r)q Fv(\))g Ft(mr)f Fr(A)p Fv([)p Fr(x)f Fv(:=)i Fr(\031)1060 271 y Fi(0)1079 264 y Fv(\()p Fr(r)q Fv(\)])48 b(otherwise)258 338 y Fr(r)15 b Ft(mr)d Fv(\()p Fs(8)p Fr(xA)p Fv(\))54 b(=)629 278 y Ff(\032)669 315 y Fs(8)p Fr(x:")11 b Ft(mr)i Fr(A)76 b Fv(if)16 b Fr(\034)6 b Fv(\()p Fr(A)p Fv(\))13 b(=)h Fs(\003)669 375 y(8)p Fr(x:r)q(x)d Ft(mr)i Fr(A)48 b Fv(otherwise)196 467 y Fr(r)15 b Ft(mr)e Fv(\()p Fr(A)g Fs(!)h Fr(B)s Fv(\))55 b(=)629 380 y Ff(8)629 417 y(<)629 492 y(:)674 413 y Fr(")14 b Ft(mr)e Fr(A)28 b Fs(!)f Fr(r)15 b Ft(mr)e Fr(B)153 b Fv(if)15 b Fr(\034)6 b Fv(\()p Fr(A)p Fv(\))13 b(=)h Fs(\003)674 473 y(8)p Fr(x:x)e Ft(mr)g Fr(A)28 b Fs(!)f Fr(")14 b Ft(mr)e Fr(B)80 b Fv(if)15 b Fr(\034)6 b Fv(\()p Fr(A)p Fv(\))13 b Fs(6)p Fv(=)h Fs(\003)g Fv(=)g Fr(\034)6 b Fv(\()p Fr(B)s Fv(\))674 534 y Fs(8)p Fr(x:x)12 b Ft(mr)g Fr(A)28 b Fs(!)f Fr(r)q(x)14 b Ft(mr)e Fr(B)52 b Fv(otherwise)182 633 y Fr(r)15 b Ft(mr)d Fv(\()p Fr(A)358 640 y Fi(0)389 633 y Fs(^)f Fr(A)470 640 y Fi(1)489 633 y Fv(\))56 b(=)629 534 y Ff(8)629 571 y(>)629 583 y(<)629 658 y(>)629 671 y(:)674 573 y Fr(")14 b Ft(mr)e Fr(A)831 580 y Fi(0)876 573 y Fs(^)25 b Fr(r)15 b Ft(mr)d Fr(A)1091 580 y Fi(1)1331 573 y Fv(if)j Fr(\034)6 b Fv(\()p Fr(A)1458 580 y Fi(0)1477 573 y Fv(\))14 b(=)g Fs(\003)674 633 y Fr(r)i Ft(mr)c Fr(A)832 640 y Fi(0)876 633 y Fs(^)25 b Fr(")14 b Ft(mr)e Fr(A)1091 640 y Fi(1)1331 633 y Fv(if)j Fr(\034)6 b Fv(\()p Fr(A)1458 640 y Fi(1)1477 633 y Fv(\))14 b(=)g Fs(\003)674 693 y Fr(\031)702 700 y Fi(0)722 693 y Fv(\()p Fr(r)q Fv(\))g Ft(mr)e Fr(A)917 700 y Fi(0)961 693 y Fs(^)26 b Fr(\031)1048 700 y Fi(1)1067 693 y Fv(\()p Fr(r)q Fv(\))14 b Ft(mr)f Fr(A)1263 700 y Fi(1)1331 693 y Fv(otherwise)-1 785 y(Note)i(that)i(for)f Fr(A)f Fs(9)376 767 y Fu(\003)396 785 y Fv(-free)g(w)o(e)h(ha)o(v)o(e)f Fr(\034)6 b Fv(\()p Fr(A)p Fv(\))13 b(=)h Fs(\003)h Fv(and)i Fr(")d Ft(mr)e Fr(A)h Fv(=)h Fr(A)p Fv(.)21 b(F)l(or)16 b(the)g(form)o(ulation)e(of)i (the)-1 846 y(soundness)g(theorem)d(b)q(elo)o(w)i(it)g(will)f(b)q(e)h (useful)g(to)g(let)f Fr(x)1049 853 y Fj(u)1085 846 y Fv(:=)g Fr(")h Fv(if)f Fr(u)1260 828 y Fj(A)1303 846 y Fv(is)h(an)h(assumption)e(v)m(ariable)-1 906 y(with)i(a)g (Harrop-form)o(ula)g Fr(A)p Fv(.)-1 1004 y Ft(Theorem)g(2.9)i (\(Soundness\))25 b Fn(If)f Fr(M)30 b Fn(is)24 b(a)h(derivation)g(of)f (a)h(formula)f Fr(B)s Fn(,)i(then)f(ther)n(e)g(is)f(a)-1 1064 y(derivation)18 b Fr(\026)p Fv(\()p Fr(M)5 b Fv(\))18 b Fn(of)f Fv([)-8 b([)p Fr(M)5 b Fv(])-8 b(])12 b Ft(mr)g Fr(B)20 b Fn(fr)n(om)c Fs(f)8 b Fr(x)844 1071 y Fj(u)881 1064 y Ft(mr)k Fr(C)17 b Fs(j)d Fr(u)1072 1046 y Fj(C)1115 1064 y Fs(2)g Fl(F)-5 b(A)o Fv(\()p Fr(M)5 b Fv(\))j Fs(g)p Fn(.)72 1163 y(Pr)n(o)n(of)h Fv(.)21 b(Induction)16 b(on)g Fr(M)5 b Fv(.)22 b Fn(Case)e Fr(u)p Fv(:)8 b Fr(A)p Fv(.)21 b(Then)16 b(w)o(e)g(ha)o(v)o(e)i(\026)-27 b Fr(u)p Fv(:)8 b Fr(x)1240 1170 y Fj(u)1276 1163 y Ft(mr)k Fr(A)p Fv(.)21 b(Let)16 b Fr(\026)p Fv(\()p Fr(u)p Fv(\))e(:=)j(\026)-27 b Fr(u)o Fv(.)72 1223 y Fn(Case)20 b Fr(\025u)250 1205 y Fj(A)279 1223 y Fr(M)331 1205 y Fj(B)361 1223 y Fv(.)i(W)l(e)16 b(m)o(ust)e(\014nd)j(a)g(deriv)m(ation)f Fr(\026)p Fv(\()p Fr(\025uM)5 b Fv(\))17 b(of)696 1319 y([)-8 b([)p Fr(\025uM)5 b Fv(])-8 b(])12 b Ft(mr)g Fv(\()p Fr(A)h Fs(!)h Fr(B)s Fv(\))p Fr(:)-1 1415 y Fn(Sub)n(c)n(ase)20 b Fr(\034)6 b Fv(\()p Fr(A)p Fv(\))13 b(=)h Fs(\003)p Fv(.)21 b(Then)c(w)o(e)e(ha)o (v)o(e)h([)-8 b([)p Fr(\025uM)5 b Fv(])-8 b(])12 b(=)i([)-8 b([)p Fr(M)5 b Fv(])-8 b(],)13 b(hence)391 1512 y([)-8 b([)p Fr(\025uM)5 b Fv(])-8 b(])12 b Ft(mr)g Fv(\()p Fr(A)i Fs(!)f Fr(B)s Fv(\))41 b(=)h Fr(")13 b Ft(mr)g Fr(A)27 b Fs(!)h Fv([)-8 b([)p Fr(M)5 b Fv(])-8 b(])11 b Ft(mr)i Fr(B)s(:)-1 1608 y Fv(By)18 b(induction)g(h)o(yp)q(othesis)h (w)o(e)f(can)i(de\014ne)e Fr(\026)p Fv(\()p Fr(\025uM)5 b Fv(\))19 b(:=)f Fr(\025)s Fv(\026)-27 b Fr(u\026)p Fv(\()p Fr(M)5 b Fv(\))20 b(with)h(\026)-27 b Fr(u)p Fv(:)8 b Fr(")18 b Ft(mr)f Fr(A)p Fv(.)28 b Fn(Sub)n(c)n(ase)-1 1668 y Fr(\034)6 b Fv(\()p Fr(A)p Fv(\))13 b Fs(6)p Fv(=)g Fs(\003)h Fv(=)g Fr(\034)6 b Fv(\()p Fr(B)s Fv(\).)20 b(Then)d(w)o(e)f(ha)o(v)o(e)f([)-8 b([)p Fr(\025uM)5 b Fv(])-8 b(])12 b(=)i Fr(")i Fv(and)387 1764 y([)-8 b([)p Fr(\025uM)5 b Fv(])-8 b(])12 b Ft(mr)h Fv(\()p Fr(A)g Fs(!)h Fr(B)s Fv(\))41 b(=)g Fs(8)p Fr(x:x)12 b Ft(mr)g Fr(A)28 b Fs(!)f Fr(")14 b Ft(mr)e Fr(B)s(:)-1 1861 y Fv(By)22 b(induction)g(h)o(yp)q(othesis)h(de\014ne)f Fr(\026)p Fv(\()p Fr(\025uM)5 b Fv(\))26 b(:=)e Fr(\025x)1032 1868 y Fj(u)1054 1861 y Fr(\025)s Fv(\026)-27 b Fr(u)q(\026)p Fv(\()p Fr(M)5 b Fv(\))23 b(with)j(\026)-28 b Fr(u)p Fv(:)8 b Fr(x)1448 1868 y Fj(u)1495 1861 y Ft(mr)23 b Fr(A)p Fv(.)40 b Fn(Sub)n(c)n(ase)-1 1921 y Fr(\034)6 b Fv(\()p Fr(A)p Fv(\))13 b Fs(6)p Fv(=)g Fs(\003)h(6)p Fv(=)g Fr(\034)6 b Fv(\()p Fr(B)s Fv(\).)20 b(Then)d(w)o(e)f(ha)o(v)o (e)319 2017 y([)-8 b([)p Fr(\025uM)5 b Fv(])-8 b(])12 b Ft(mr)g Fv(\()p Fr(A)i Fs(!)f Fr(B)s Fv(\))41 b(=)h Fs(8)p Fr(x:x)11 b Ft(mr)i Fr(A)27 b Fs(!)g Fv([)-8 b([)p Fr(\025uM)5 b Fv(])-8 b(])p Fr(x)12 b Ft(mr)g Fr(B)-1 2113 y Fv(Because)g(of)i([)-8 b([)p Fr(\025uM)5 b Fv(])-8 b(])12 b(=)h Fr(\025x)502 2120 y Fj(u)525 2113 y Fv([)-8 b([)p Fr(M)5 b Fv(])-8 b(])11 b(and)j(since)e(w)o(e)h(iden)o(tify)e (terms)h(with)h(the)g(same)f Fr(\014)s Fv(-normal)g(form,)-1 2173 y(b)o(y)j(induction)h(h)o(yp)q(othesis)g(w)o(e)g(can)h(de\014ne)f Fr(\026)p Fv(\()p Fr(\025uM)5 b Fv(\))14 b(:=)g Fr(\025x)1137 2180 y Fj(u)1159 2173 y Fr(\025)s Fv(\026)-27 b Fr(u)q(\026)p Fv(\()p Fr(M)5 b Fv(\).)72 2234 y Fn(Case)27 b Fr(M)253 2215 y Fj(A)p Fu(!)p Fj(B)345 2234 y Fr(N)389 2215 y Fj(A)418 2234 y Fv(.)42 b(W)l(e)23 b(m)o(ust)f(\014nd)h(a)h(deriv)m (ation)e Fr(\026)p Fv(\()p Fr(M)5 b(N)g Fv(\))25 b(of)e([)-8 b([)p Fr(M)5 b(N)g Fv(])-8 b(])24 b Ft(mr)g Fr(B)s Fv(.)41 b Fn(Sub)n(c)n(ase)-1 2294 y Fr(\034)6 b Fv(\()p Fr(A)p Fv(\))15 b(=)h Fs(\003)p Fv(.)26 b(Then)17 b(w)o(e)g(ha)o(v)o(e)g([)-8 b([)p Fr(M)5 b(N)g Fv(])-8 b(])15 b(=)h([)-8 b([)p Fr(M)5 b Fv(])-8 b(].)23 b(By)17 b(induction)g(h)o(yp)q(othesis)h(w)o(e)f(ha)o (v)o(e)g(deriv)m(ations)-1 2354 y Fr(\026)p Fv(\()p Fr(M)5 b Fv(\))17 b(of)426 2414 y([)-8 b([)p Fr(M)5 b Fv(])-8 b(])12 b Ft(mr)g Fv(\()p Fr(A)h Fs(!)h Fr(B)s Fv(\))41 b(=)g Fr(")14 b Ft(mr)f Fr(A)27 b Fs(!)g Fv([)-8 b([)p Fr(M)5 b Fv(])-8 b(])12 b Ft(mr)g Fr(B)-1 2495 y Fv(and)17 b Fr(\026)p Fv(\()p Fr(N)5 b Fv(\))17 b(of)g Fr(")d Ft(mr)f Fr(A)p Fv(;)i(hence)h(w)o(e)g(can)h(de\014ne)f Fr(\026)p Fv(\()p Fr(M)5 b(N)g Fv(\))15 b(:=)f Fr(\026)p Fv(\()p Fr(M)5 b Fv(\))p Fr(\026)p Fv(\()p Fr(N)g Fv(\).)23 b Fn(Sub)n(c)n(ase)e Fr(\034)6 b Fv(\()p Fr(A)p Fv(\))14 b Fs(6)p Fv(=)g Fs(\003)g Fv(=)-1 2556 y Fr(\034)6 b Fv(\()p Fr(B)s Fv(\).)20 b(Then)15 b(w)o(e)h(ha)o(v)o(e)e([)-8 b([)p Fr(M)5 b(N)g Fv(])-8 b(])12 b(=)i Fr(")p Fv(.)21 b(By)15 b(induction)g(h)o(yp)q(othesis)g(w)o(e)g(ha)o(v)o(e)g(deriv)m (ations)h Fr(\026)p Fv(\()p Fr(M)5 b Fv(\))16 b(of)422 2652 y([)-8 b([)p Fr(M)5 b Fv(])-8 b(])12 b Ft(mr)h Fv(\()p Fr(A)g Fs(!)h Fr(B)s Fv(\))41 b(=)g Fs(8)p Fr(x:x)12 b Ft(mr)g Fr(A)27 b Fs(!)h Fr(")13 b Ft(mr)g Fr(B)-1 2748 y Fv(and)24 b Fr(\026)p Fv(\()p Fr(N)5 b Fv(\))23 b(of)h([)-8 b([)p Fr(N)5 b Fv(])-8 b(])24 b Ft(mr)g Fr(A)p Fv(;)i(hence)d(w)o(e)f(can)i(de\014ne)f Fr(\026)p Fv(\()p Fr(M)5 b(N)g Fv(\))27 b(:=)e Fr(\026)p Fv(\()p Fr(M)5 b Fv(\)[)-8 b([)p Fr(N)5 b Fv(])-8 b(])p Fr(\026)p Fv(\()p Fr(N)5 b Fv(\).)41 b Fn(Sub)n(c)n(ase)-1 2808 y Fr(\034)6 b Fv(\()p Fr(A)p Fv(\))15 b Fs(6)p Fv(=)g Fs(\003)h(6)p Fv(=)f Fr(\034)6 b Fv(\()p Fr(B)s Fv(\).)24 b(Then)18 b(w)o(e)f(ha)o(v)o(e)f([)-8 b([)p Fr(M)5 b(N)g Fv(])-8 b(])14 b(=)i([)-8 b([)p Fr(M)5 b Fv(])-8 b(][)g([)o Fr(N)5 b Fv(])-8 b(].)21 b(By)c(induction)g(h)o(yp)q(othesis)g(w)o(e)g(ha)o(v) o(e)-1 2868 y(deriv)m(ations)f Fr(\026)p Fv(\()p Fr(M)5 b Fv(\))17 b(of)375 2965 y([)-8 b([)p Fr(M)5 b Fv(])-8 b(])12 b Ft(mr)g Fv(\()p Fr(A)i Fs(!)f Fr(B)s Fv(\))41 b(=)h Fs(8)p Fr(x:x)11 b Ft(mr)i Fr(A)27 b Fs(!)g Fv([)-8 b([)p Fr(M)5 b Fv(])-8 b(])p Fr(x)12 b Ft(mr)g Fr(B)p eop %%Page: 9 9 9 8 bop -1 53 a Fv(and)16 b Fr(\026)p Fv(\()p Fr(N)5 b Fv(\))17 b(of)g([)-8 b([)p Fr(N)5 b Fv(])-8 b(])11 b Ft(mr)i Fr(A)p Fv(;)i(hence)h(w)o(e)g(can)g(de\014ne)g Fr(\026)p Fv(\()p Fr(M)5 b(N)g Fv(\))15 b(:=)e Fr(\026)p Fv(\()p Fr(M)5 b Fv(\)[)-8 b([)p Fr(N)5 b Fv(])-8 b(])p Fr(\026)p Fv(\()p Fr(N)5 b Fv(\).)72 114 y Fn(Case)20 b Fs(h)p Fr(M)265 92 y Fj(A)291 97 y Fh(0)260 124 y Fi(0)311 114 y Fr(;)8 b(M)385 92 y Fj(A)411 97 y Fh(1)380 124 y Fi(1)431 114 y Fs(i)p Fv(.)22 b(W)l(e)16 b(m)o(ust)f(\014nd)h(a)h (deriv)m(ation)f Fr(\026)p Fv(\()p Fs(h)p Fr(M)1172 121 y Fi(0)1193 114 y Fr(;)8 b(M)1262 121 y Fi(1)1281 114 y Fs(i)p Fv(\))17 b(of)646 222 y([)-8 b([)p Fs(h)p Fr(M)732 229 y Fi(0)751 222 y Fr(;)8 b(M)820 229 y Fi(1)839 222 y Fs(i)p Fv(])-8 b(])13 b Ft(mr)g Fv(\()p Fr(A)1031 229 y Fi(0)1061 222 y Fs(^)e Fr(A)1142 229 y Fi(1)1162 222 y Fv(\))p Fr(:)-1 330 y Fn(Sub)n(c)n(ase)20 b Fr(\034)6 b Fv(\()p Fr(A)262 337 y Fi(0)281 330 y Fv(\))14 b(=)g Fs(\003)g Fv(=)f Fr(\034)6 b Fv(\()p Fr(A)539 337 y Fi(1)558 330 y Fv(\).)22 b(Then)16 b(w)o(e)g(ha)o(v)o(e)f([)-8 b([)p Fs(h)p Fr(M)1010 337 y Fi(0)1029 330 y Fr(;)8 b(M)1098 337 y Fi(1)1118 330 y Fs(i)p Fv(])-8 b(])13 b(=)h Fr(")p Fv(,)h(hence)374 438 y([)-8 b([)p Fs(h)p Fr(M)460 445 y Fi(0)479 438 y Fr(;)8 b(M)548 445 y Fi(1)568 438 y Fs(i)p Fv(])-8 b(])13 b Ft(mr)f Fv(\()p Fr(A)759 445 y Fi(0)790 438 y Fs(^)f Fr(A)871 445 y Fi(1)890 438 y Fv(\))42 b(=)f Fr(")14 b Ft(mr)e Fr(A)1187 445 y Fi(0)1231 438 y Fs(^)25 b Fr(")14 b Ft(mr)f Fr(A)1447 445 y Fi(1)-1 546 y Fv(and)21 b(b)o(y)e(induction)h(h)o(yp)q(othesis)h(w)o(e)f(can)g (de\014ne)g Fr(\026)p Fv(\()p Fs(h)p Fr(M)1063 553 y Fi(0)1084 546 y Fr(;)8 b(M)1153 553 y Fi(1)1173 546 y Fs(i)p Fv(\))21 b(:=)f Fs(h)p Fr(\026)p Fv(\()p Fr(M)1418 553 y Fi(0)1439 546 y Fv(\))p Fr(;)8 b(\026)p Fv(\()p Fr(M)1575 553 y Fi(1)1595 546 y Fv(\))p Fs(i)p Fv(.)33 b Fn(Sub)n(c)n(ase)-1 607 y Fr(\034)6 b Fv(\()p Fr(A)82 614 y Fi(0)101 607 y Fv(\))13 b(=)h Fs(\003)g(6)p Fv(=)g Fr(\034)6 b Fv(\()p Fr(A)359 614 y Fi(1)378 607 y Fv(\).)21 b(Then)16 b(w)o(e)g(ha)o(v)o(e)g([)-8 b([)p Fs(h)p Fr(M)830 614 y Fi(0)849 607 y Fr(;)8 b(M)918 614 y Fi(1)937 607 y Fs(i)p Fv(])-8 b(])13 b(=)h([)-8 b([)p Fr(M)1108 614 y Fi(1)1127 607 y Fv(])g(],)14 b(hence)333 715 y([)-8 b([)p Fs(h)p Fr(M)419 722 y Fi(0)438 715 y Fr(;)8 b(M)507 722 y Fi(1)527 715 y Fs(i)p Fv(])-8 b(])13 b Ft(mr)f Fv(\()p Fr(A)718 722 y Fi(0)749 715 y Fs(^)f Fr(A)830 722 y Fi(1)849 715 y Fv(\))42 b(=)f Fr(")14 b Ft(mr)e Fr(A)1146 722 y Fi(0)1190 715 y Fs(^)26 b Fv([)-8 b([)p Fr(M)1316 722 y Fi(1)1334 715 y Fv(])g(])13 b Ft(mr)f Fr(A)1487 722 y Fi(1)-1 823 y Fv(and)21 b(b)o(y)e(induction)h(h)o(yp)q (othesis)h(w)o(e)f(can)g(de\014ne)g Fr(\026)p Fv(\()p Fs(h)p Fr(M)1063 830 y Fi(0)1084 823 y Fr(;)8 b(M)1153 830 y Fi(1)1173 823 y Fs(i)p Fv(\))21 b(:=)f Fs(h)p Fr(\026)p Fv(\()p Fr(M)1418 830 y Fi(0)1439 823 y Fv(\))p Fr(;)8 b(\026)p Fv(\()p Fr(M)1575 830 y Fi(1)1595 823 y Fv(\))p Fs(i)p Fv(.)33 b Fn(Sub)n(c)n(ase)-1 883 y Fr(\034)6 b Fv(\()p Fr(A)82 890 y Fi(0)101 883 y Fv(\))14 b Fs(6)p Fv(=)h Fs(\003)f Fv(=)h Fr(\034)6 b Fv(\()p Fr(A)362 890 y Fi(1)381 883 y Fv(\).)22 b(Similar.)f Fn(Sub)n(c)n(ase)g Fr(\034)6 b Fv(\()p Fr(A)889 890 y Fi(0)908 883 y Fv(\))14 b Fs(6)p Fv(=)h Fs(\003)f(6)p Fv(=)h Fr(\034)6 b Fv(\()p Fr(A)1169 890 y Fi(1)1188 883 y Fv(\).)23 b(Then)16 b(w)o(e)h(ha)o(v)o (e)f([)-8 b([)p Fs(h)p Fr(M)1643 890 y Fi(0)1662 883 y Fr(;)8 b(M)1731 890 y Fi(1)1750 883 y Fs(i)p Fv(])-8 b(])14 b(=)-1 944 y Fs(h)p Fv([)-8 b([)p Fr(M)85 951 y Fi(0)104 944 y Fv(])g(])p Fr(;)8 b Fv([)-8 b([)p Fr(M)213 951 y Fi(1)230 944 y Fv(])g(])p Fs(i)p Fv(,)15 b(hence)292 1052 y([)-8 b([)p Fs(h)p Fr(M)378 1059 y Fi(0)397 1052 y Fr(;)8 b(M)466 1059 y Fi(1)486 1052 y Fs(i)p Fv(])-8 b(])13 b Ft(mr)g Fv(\()p Fr(A)678 1059 y Fi(0)708 1052 y Fs(^)e Fr(A)789 1059 y Fi(1)808 1052 y Fv(\))42 b(=)f([)-8 b([)p Fr(M)1015 1059 y Fi(0)1034 1052 y Fv(])g(])13 b Ft(mr)f Fr(A)1187 1059 y Fi(0)1231 1052 y Fs(^)25 b Fv([)-8 b([)p Fr(M)1356 1059 y Fi(1)1375 1052 y Fv(])g(])13 b Ft(mr)f Fr(A)1528 1059 y Fi(1)-1 1160 y Fv(and)k(b)o(y)g(induction)g(h) o(yp)q(othesis)g(w)o(e)g(can)h(de\014ne)e Fr(\026)p Fv(\()p Fs(h)p Fr(M)1034 1167 y Fi(0)1055 1160 y Fr(;)8 b(M)1124 1167 y Fi(1)1144 1160 y Fs(i)p Fv(\))14 b(:=)f Fs(h)p Fr(\026)p Fv(\()p Fr(M)1375 1167 y Fj(i)1390 1160 y Fv(\))p Fr(;)8 b(\026)p Fv(\()p Fr(M)1526 1167 y Fi(1)p Fu(\000)p Fj(i)1586 1160 y Fv(\))p Fs(i)p Fv(.)72 1220 y Fn(Case)20 b Fr(\031)222 1227 y Fi(0)241 1220 y Fv(\()p Fr(M)312 1202 y Fj(A)338 1207 y Fh(0)356 1202 y Fu(^)p Fj(A)406 1207 y Fh(1)426 1220 y Fv(\).)h(W)l(e)16 b(m)o(ust)f(\014nd)h(a)h (deriv)m(ation)f Fr(\026)p Fv(\()p Fr(\031)1128 1227 y Fi(0)1148 1220 y Fv(\()p Fr(M)5 b Fv(\)\))16 b(of)749 1328 y([)-8 b([)p Fr(\031)797 1335 y Fi(0)815 1328 y Fv(\()p Fr(M)5 b Fv(\)])-8 b(])13 b Ft(mr)f Fr(A)1058 1335 y Fi(0)1078 1328 y Fr(:)-1 1437 y Fn(Sub)n(c)n(ase)20 b Fr(\034)6 b Fv(\()p Fr(A)262 1444 y Fi(1)281 1437 y Fv(\))15 b(=)f Fs(\003)p Fv(.)21 b(Then)c(w)o(e)f(ha)o(v)o(e)f([)-8 b([)p Fr(\031)787 1444 y Fi(0)806 1437 y Fv(\()p Fr(M)5 b Fv(\)])-8 b(])13 b(=)h([)-8 b([)p Fr(M)5 b Fv(])-8 b(].)20 b(b)o(y)c(induction)g(h)o(yp)q(othesis)g(w)o(e)g(ha)o(v)o(e)g (a)-1 1497 y(deriv)m(ation)g Fr(\026)p Fv(\()p Fr(M)5 b Fv(\))17 b(of)405 1605 y([)-8 b([)p Fr(M)5 b Fv(])-8 b(])11 b Ft(mr)i Fv(\()p Fr(A)648 1612 y Fi(0)678 1605 y Fs(^)e Fr(A)759 1612 y Fi(1)779 1605 y Fv(\))41 b(=)h([)-8 b([)p Fr(M)5 b Fv(])-8 b(])11 b Ft(mr)i Fr(A)1143 1612 y Fi(0)1187 1605 y Fs(^)25 b Fr(")14 b Ft(mr)e Fr(A)1402 1612 y Fi(1)1422 1605 y Fr(:)-1 1713 y Fv(hence)19 b(w)o(e)g(can)i (de\014ne)e Fr(\026)p Fv(\()p Fr(\031)527 1720 y Fi(0)547 1713 y Fv(\()p Fr(M)5 b Fv(\)\))21 b(:=)e Fr(\031)776 1720 y Fi(0)796 1713 y Fv(\()p Fr(\026)p Fv(\()p Fr(M)5 b Fv(\)\).)33 b Fn(Sub)n(c)n(ase)24 b Fr(\034)6 b Fv(\()p Fr(A)1267 1720 y Fi(0)1286 1713 y Fv(\))20 b(=)h Fs(\003)f(6)p Fv(=)g Fr(\034)6 b Fv(\()p Fr(A)1570 1720 y Fi(1)1589 1713 y Fv(\).)32 b(Then)21 b(w)o(e)-1 1773 y(ha)o(v)o(e)15 b([)-8 b([)p Fr(\031)159 1780 y Fi(0)177 1773 y Fv(\()p Fr(M)5 b Fv(\)])-8 b(])13 b(=)h Fr(")p Fv(.)21 b(b)o(y)16 b(induction)g(h)o(yp)q(othesis)g(w)o(e)g(ha)o(v)o(e)f(a)i(deriv)m (ation)f Fr(\026)p Fv(\()p Fr(M)5 b Fv(\))17 b(of)405 1882 y([)-8 b([)p Fr(M)5 b Fv(])-8 b(])11 b Ft(mr)i Fv(\()p Fr(A)648 1889 y Fi(0)678 1882 y Fs(^)e Fr(A)759 1889 y Fi(1)779 1882 y Fv(\))41 b(=)h Fr(")13 b Ft(mr)g Fr(A)1076 1889 y Fi(0)1120 1882 y Fs(^)25 b Fv([)-8 b([)p Fr(M)5 b Fv(])-8 b(])12 b Ft(mr)g Fr(A)1402 1889 y Fi(1)1422 1882 y Fr(:)-1 1990 y Fv(hence)k(w)o(e)i(can)f(de\014ne)g Fr(\026)p Fv(\()p Fr(\031)517 1997 y Fi(0)537 1990 y Fv(\()p Fr(M)5 b Fv(\)\))16 b(:=)g Fr(\031)758 1997 y Fi(0)777 1990 y Fv(\()p Fr(\026)p Fv(\()p Fr(M)5 b Fv(\)\).)26 b Fn(Sub)n(c)n(ase)c Fr(\034)6 b Fv(\()p Fr(A)1239 1997 y Fi(0)1258 1990 y Fv(\))16 b Fs(6)p Fv(=)g Fs(\003)g(6)p Fv(=)g Fr(\034)6 b Fv(\()p Fr(A)1525 1997 y Fi(1)1544 1990 y Fv(\).)25 b(Similar;)16 b(w)o(e)-1 2050 y(can)g(de\014ne)g Fr(\026)p Fv(\()p Fs(h)p Fr(M)343 2057 y Fi(0)364 2050 y Fr(;)8 b(M)433 2057 y Fi(1)452 2050 y Fs(i)p Fv(\))14 b(:=)g Fs(h)p Fr(\026)p Fv(\()p Fr(M)684 2057 y Fi(0)704 2050 y Fv(\))p Fr(;)8 b(\026)p Fv(\()p Fr(M)840 2057 y Fi(1)860 2050 y Fv(\))p Fs(i)p Fv(.)72 2110 y Fn(Case)20 b Fr(\031)222 2117 y Fi(1)241 2110 y Fv(\()p Fr(M)312 2092 y Fj(A)338 2097 y Fh(0)356 2092 y Fu(^)p Fj(A)406 2097 y Fh(1)426 2110 y Fv(\).)h(Similar.)72 2171 y Fn(Case)g Fr(\025z)r(M)300 2152 y Fj(A)329 2171 y Fv(.)j(W)l(e)17 b(m)o(ust)f(\014nd)i(a)g(deriv)m(ation)f Fr(\026)p Fv(\()p Fr(\025z)r(M)5 b Fv(\))18 b(of)g([)-8 b([)p Fr(\025z)r(M)5 b Fv(])-8 b(])13 b Ft(mr)i Fs(8)p Fr(z)r(A)p Fv(.)22 b(By)17 b(de\014nition)-1 2231 y([)-8 b([)p Fr(\025z)r(M)5 b Fv(])-8 b(])12 b(=)i Fr(\025z)r Fv([)-8 b([)p Fr(M)5 b Fv(])-8 b(].)19 b Fn(Sub)n(c)n(ase)i Fr(\034)6 b Fv(\()p Fr(A)p Fv(\))13 b(=)h Fs(\003)p Fv(.)21 b(Then)16 b(w)o(e)g(ha)o(v)o(e) 583 2339 y Fr(\025z)r Fv([)-8 b([)p Fr(M)5 b Fv(])-8 b(])12 b Ft(mr)h Fs(8)p Fr(z)r(A)39 b Fv(=)j Fs(8)p Fr(z)r(:")12 b Ft(mr)g Fr(A)-1 2447 y Fv(and)20 b(b)o(y)e(induction)h(h)o(yp)q (othesis)h(w)o(e)e(can)i(de\014ne)f Fr(\026)p Fv(\()p Fr(\025z)r(M)5 b Fv(\))20 b(:=)e Fr(\025z)r(\026)p Fv(\()p Fr(M)5 b Fv(\).)32 b(The)19 b(v)m(ariable)g(condi-)-1 2507 y(tion)f(is)h(satis\014ed,)g(since)f Fr(\025z)r(M)584 2489 y Fj(A)632 2507 y Fv(is)g(a)h(deriv)m(ation)f(term,)g(and)h(hence) f Fr(z)i Fv(do)q(es)g(not)f(o)q(ccur)g(free)e(in)-1 2568 y(an)o(y)j(assumption)h(v)m(ariable)f Fr(u)p Fv(:)8 b Fr(B)23 b Fv(free)d(in)h Fr(M)867 2549 y Fj(A)896 2568 y Fv(,)g(hence)f(also)i(do)q(es)f(not)h(o)q(ccur)f(free)f(in)g(the)h (free)-1 2628 y(assumption)e(\026)-27 b Fr(u)o Fv(:)8 b Fr(x)334 2635 y Fj(u)370 2628 y Ft(mr)13 b Fr(B)s Fv(.)20 b Fn(Sub)n(c)n(ase)h Fr(\034)6 b Fv(\()p Fr(A)p Fv(\))13 b Fs(6)p Fv(=)h Fs(\003)p Fv(.)21 b(Then)16 b(w)o(e)g(ha)o(v)o(e)485 2736 y Fr(\025z)r Fv([)-8 b([)p Fr(M)5 b Fv(])-8 b(])12 b Ft(mr)g Fs(8)p Fr(z)r(A)40 b Fv(=)h Fs(8)p Fr(z)r(:)p Fv(\()p Fr(\025z)r Fv([)-8 b([)p Fr(M)5 b Fv(])-8 b(]\))p Fr(z)12 b Ft(mr)h Fr(A:)-1 2844 y Fv(Since)f(w)o(e)h(iden)o(tify)e (terms)h(with)h(the)g(same)f Fr(\014)s Fv(-normal)g(form,)h(b)o(y)f (induction)h(h)o(yp)q(othesis)h(w)o(e)e(again)-1 2904 y(can)19 b(de\014ne)g Fr(\026)p Fv(\()p Fr(\025z)r(M)5 b Fv(\))21 b(:=)e Fr(\025z)r(\026)p Fv(\()p Fr(M)5 b Fv(\).)32 b(As)19 b(b)q(efore)g(one)h(can)g(see)f(that)h(the)f(v)m (ariable)g(condition)g(is)-1 2965 y(satis\014ed.)p eop %%Page: 10 10 10 9 bop 72 53 a Fn(Case)19 b Fr(M)245 35 y Fu(8)p Fj(z)q(A)311 53 y Fr(t)p Fv(.)i(W)l(e)15 b(m)o(ust)e(\014nd)j(a)f(deriv)m(ation)g Fr(\026)p Fv(\()p Fr(M)5 b(t)p Fv(\))16 b(of)f([)-8 b([)p Fr(M)5 b(t)p Fv(])-8 b(])12 b Ft(mr)g Fr(A)p Fv([)p Fr(x)h Fv(:=)g Fr(t)p Fv(].)20 b(By)15 b(de\014nition)-1 114 y(w)o(e)d(ha)o(v)o(e)f([)-8 b([)p Fr(M)5 b(t)p Fv(])-8 b(])12 b(=)h([)-8 b([)p Fr(M)5 b Fv(])-8 b(])p Fr(t)p Fv(.)18 b Fn(Sub)n(c)n(ase)f Fr(\034)6 b Fv(\()p Fr(A)p Fv(\))13 b(=)h Fs(\003)p Fv(.)20 b(By)11 b(induction)h(h)o(yp)q (othesis)h(w)o(e)f(ha)o(v)o(e)g(a)g(deriv)m(ation)-1 174 y(of)610 234 y([)-8 b([)p Fr(M)5 b Fv(])-8 b(])12 b Ft(mr)g Fs(8)p Fr(z)r(A)40 b Fv(=)h Fs(8)p Fr(z)r(:")12 b Ft(mr)g Fr(A)-1 314 y Fv(hence)k(w)o(e)h(can)g(de\014ne)g Fr(\026)p Fv(\()p Fr(M)5 b(t)p Fv(\))16 b(:=)e Fr(\026)p Fv(\()p Fr(M)5 b Fv(\))p Fr(t)p Fv(.)25 b Fn(Sub)n(c)n(ase)c Fr(\034)6 b Fv(\()p Fr(A)p Fv(\))15 b Fs(6)p Fv(=)g Fs(\003)p Fv(.)24 b(By)17 b(induction)f(h)o(yp)q(othesis)i(w)o(e)-1 375 y(ha)o(v)o(e)d(a)i(deriv)m(ation)f(of)557 435 y([)-8 b([)p Fr(M)5 b Fv(])-8 b(])12 b Ft(mr)g Fs(8)p Fr(z)r(A)40 b Fv(=)h Fs(8)p Fr(z)r(:)p Fv([)-8 b([)p Fr(M)5 b Fv(])-8 b(])o Fr(z)13 b Ft(mr)g Fr(A;)-1 515 y Fv(hence)i(w)o(e)h(again)h(can)f (de\014ne)g Fr(\026)p Fv(\()p Fr(M)5 b(t)p Fv(\))14 b(:=)g Fr(\026)p Fv(\()p Fr(M)5 b Fv(\))p Fr(t)p Fv(.)72 575 y Fn(Case)20 b Fs(9)222 555 y Fu(\003)p Fi(+)222 587 y Fj(x;A)280 575 y Fv(:)8 b Fs(8)o Fr(~)-23 b(x)n Fs(8)p Fr(x:A)11 b Fs(!)j(9)568 557 y Fu(\003)587 575 y Fr(x)615 557 y Fj(\032)635 575 y Fr(A)p Fv(.)21 b(W)l(e)16 b(m)o(ust)f(\014nd)h (a)h(deriv)m(ation)f Fr(\026)p Fv(\()p Fs(9)1355 555 y Fu(\003)p Fi(+)1355 587 y Fj(x;A)1413 575 y Fv(\))g(of)618 669 y([)-8 b([)p Fs(9)666 649 y Fu(\003)p Fi(+)666 682 y Fj(x;A)722 669 y Fv(])g(])13 b Ft(mr)f Fs(8)o Fr(~)-23 b(x)o Fs(8)p Fr(x:A)11 b Fs(!)j(9)1105 649 y Fu(\003)1124 669 y Fr(x)1152 649 y Fj(\032)1172 669 y Fr(A:)-1 764 y Fn(Sub)n(c)n(ase)20 b Fr(\034)6 b Fv(\()p Fr(A)p Fv(\))13 b(=)h Fs(\003)p Fv(.)21 b(Then)c(w)o(e)e(ha)o(v)o(e)h Fs(9)746 743 y Fu(\003)p Fi(+)746 776 y Fj(x;A)818 764 y Fv(=)d Fr(\025)o(~)-23 b(x\025xx)17 b Fv(and)f(w)o(e)g(obtain)263 862 y(\()p Fr(\025)o(~)-23 b(x\025xx)p Fv(\))14 b Ft(mr)e Fs(8)o Fr(~)-23 b(x)o Fs(8)p Fr(x:A)11 b Fs(!)j(9)805 844 y Fu(\003)824 862 y Fr(xA)41 b Fv(=)14 b Fs(8)o Fr(~)-23 b(x)n Fs(8)p Fr(x:x)11 b Ft(mr)i Fv(\()p Fr(A)g Fs(!)h(9)1392 844 y Fu(\003)1411 862 y Fr(xA)p Fv(\))930 923 y(=)g Fs(8)o Fr(~)-23 b(x)n Fs(8)p Fr(x:")12 b Ft(mr)g Fr(A)h Fs(!)h Fr(x)g Ft(mr)e Fs(9)1493 904 y Fu(\003)1512 923 y Fr(xA)930 983 y Fv(=)i Fs(8)o Fr(~)-23 b(x)n Fs(8)p Fr(x:")12 b Ft(mr)g Fr(A)h Fs(!)h Fr(")g Ft(mr)e Fr(A:)-1 1080 y Fv(Hence)18 b(w)o(e)i(can)h(de\014ne)e Fr(\026)p Fv(\()p Fs(9)537 1059 y Fu(\003)p Fi(+)537 1092 y Fj(x;A)596 1080 y Fv(\))h(=)g Fr(\025)o(~)-23 b(x)q(\025x\025uu)p Fv(.)33 b Fn(Sub)n(c)n(ase)24 b Fr(\034)6 b Fv(\()p Fr(A)p Fv(\))20 b Fs(6)p Fv(=)h Fs(\003)p Fv(.)32 b(Then)21 b(w)o(e)e(ha)o(v)o(e)h Fs(9)1725 1059 y Fu(\003)p Fi(+)1725 1092 y Fj(x;A)1803 1080 y Fv(=)-1 1140 y Fr(\025)o(~)-23 b(x\025x\025y)r Fs(h)p Fr(x;)8 b(y)r Fs(i)16 b Fv(and)h(w)o(e)f(obtain) 546 1232 y Fr(\025)o(~)-23 b(x\025x\025y)r Fs(h)p Fr(x;)8 b(y)r Fs(i)14 b Ft(mr)f Fs(8)o Fr(~)-23 b(x)n Fs(8)p Fr(x:A)11 b Fs(!)j(9)1190 1214 y Fu(\003)1209 1232 y Fr(xA)546 1293 y Fv(=)g Fs(8)o Fr(~)-23 b(x)n Fs(8)p Fr(x)p Fs(8)p Fr(y)r(:)o(y)13 b Ft(mr)f Fr(A)i Fs(!)f(h)p Fr(x;)8 b(y)r Fs(i)14 b Ft(mr)e Fs(9)1251 1275 y Fu(\003)1271 1293 y Fr(xA)546 1353 y Fv(=)i Fs(8)o Fr(~)-23 b(x)n Fs(8)p Fr(x)p Fs(8)p Fr(y)r(:)o(y)13 b Ft(mr)f Fr(A)i Fs(!)f Fr(y)j Ft(mr)c Fr(A)-1 1450 y Fv(Hence)j(w)o(e)g(can)i(de\014ne) f Fr(\026)p Fv(\()p Fs(9)522 1429 y Fu(\003)p Fi(+)522 1462 y Fj(x;A)580 1450 y Fv(\))e(=)f Fr(\025)o(~)-23 b(x)q(\025x\025y)r(\025uu)p Fv(.)72 1510 y Fn(Case)25 b Fs(9)227 1489 y Fu(\003\000)227 1522 y Fj(x;A;B)323 1510 y Fv(:)8 b Fs(8)o Fr(~)-23 b(x)n Fv([)p Fs(9)442 1492 y Fu(\003)461 1510 y Fr(xA)23 b Fs(!)g Fv(\()p Fs(8)p Fr(x:A)d Fs(!)j Fr(B)s Fv(\))f Fs(!)h Fr(B)s Fv(])e(with)h Fr(x)28 b(=)-30 b Fs(2)23 b Fl(FV)6 b Fv(\()p Fr(B)s Fv(\).)37 b(W)l(e)22 b(m)o(ust)e(\014nd)i(a)-1 1570 y(deriv)m(ation)e Fr(\026)p Fv(\()p Fs(9)308 1549 y Fu(\003\000)308 1582 y Fj(x;A;B)404 1570 y Fv(\))h(of)g Fs(8)o Fr(~)-23 b(x)o Fv([)p Fs(9)602 1552 y Fu(\003)621 1570 y Fr(xA)21 b Fs(!)g Fv(\()p Fs(8)p Fr(x:A)e Fs(!)j Fr(B)s Fv(\))f Fs(!)g Fr(B)s Fv(].)34 b Fn(Sub)n(c)n(ase)26 b Fr(\034)6 b Fv(\()p Fr(A)p Fv(\))21 b(=)g Fs(\003)h Fv(=)f Fr(\034)6 b Fv(\()p Fr(B)s Fv(\).)-1 1630 y(Then)16 b(w)o(e)g(ha)o(v)o(e)f([)-8 b([)p Fs(9)358 1610 y Fu(\003\000)358 1642 y Fj(x;A;B)453 1630 y Fv(])g(])13 b(=)g Fr(")j Fv(and)h(w)o(e)f(obtain)360 1729 y Fr(")d Ft(mr)g Fs(8)o Fr(~)-23 b(x)n Fv([)p Fs(9)577 1711 y Fu(\003)596 1729 y Fr(xA)13 b Fs(!)h Fv(\()p Fs(8)p Fr(x:A)d Fs(!)j Fr(B)s Fv(\))f Fs(!)h Fr(B)s Fv(])360 1789 y(=)g Fs(8)o Fr(~)-23 b(x)n Fs(8)p Fr(x:x)11 b Ft(mr)i Fs(9)689 1771 y Fu(\003)708 1789 y Fr(xA)g Fs(!)h Fr(")g Ft(mr)e Fv(\(\()p Fs(8)p Fr(x:A)f Fs(!)j Fr(B)s Fv(\))f Fs(!)h Fr(B)s Fv(\))360 1849 y(=)g Fs(8)o Fr(~)-23 b(x)n Fs(8)p Fr(x:")12 b Ft(mr)g Fr(A)h Fs(!)h Fr(")g Ft(mr)e Fv(\()p Fs(8)p Fr(x:A)f Fs(!)j Fr(B)s Fv(\))f Fs(!)h Fr(")g Ft(mr)e Fr(B)360 1910 y Fv(=)i Fs(8)o Fr(~)-23 b(x)n Fs(8)p Fr(x:")12 b Ft(mr)g Fr(A)h Fs(!)h(8)p Fr(x)8 b(")k Ft(mr)h Fv(\()p Fr(A)g Fs(!)h Fr(B)s Fv(\))f Fs(!)h Fr(")g Ft(mr)e Fr(B)360 1970 y Fv(=)i Fs(8)o Fr(~)-23 b(x)n Fs(8)p Fr(x:")12 b Ft(mr)g Fr(A)h Fs(!)h Fv(\()p Fs(8)p Fr(x:")e Ft(mr)g Fr(A)h Fs(!)h Fr(")g Ft(mr)e Fr(B)s Fv(\))i Fs(!)f Fr(")h Ft(mr)e Fr(B)s(:)-1 2067 y Fv(Hence)k(w)o(e)h(can)g(de\014ne)g Fr(\026)p Fv(\()p Fs(9)526 2046 y Fu(\003\000)526 2079 y Fj(x;A;B)623 2067 y Fv(\))e(=)h Fr(\025)o(~)-23 b(x\025x\025u\025v)r(:v)r(xu)p Fv(.)24 b Fn(Sub)n(c)n(ase)e Fr(\034)6 b Fv(\()p Fr(A)p Fv(\))15 b Fs(6)p Fv(=)g Fs(\003)h Fv(=)g Fr(\034)6 b Fv(\()p Fr(B)s Fv(\).)24 b(Then)18 b(w)o(e)-1 2127 y(again)f(ha)o(v)o (e)e([)-8 b([)p Fs(9)289 2106 y Fu(\003\000)289 2139 y Fj(x;A;B)384 2127 y Fv(])g(])12 b(=)i Fr(")i Fv(and)h(w)o(e)f(obtain) 170 2226 y Fr(")e Ft(mr)e Fs(8)o Fr(~)-23 b(x)n Fv([)p Fs(9)387 2208 y Fu(\003)406 2226 y Fr(xA)14 b Fs(!)f Fv(\()p Fs(8)p Fr(x:A)e Fs(!)j Fr(B)s Fv(\))g Fs(!)f Fr(B)s Fv(])170 2286 y(=)h Fs(8)o Fr(~)-23 b(x)n Fs(8)p Fr(x:x)12 b Ft(mr)g Fs(9)499 2268 y Fu(\003)518 2286 y Fr(xA)i Fs(!)f Fr(")h Ft(mr)e Fv(\(\()p Fs(8)p Fr(x:A)g Fs(!)h Fr(B)s Fv(\))h Fs(!)f Fr(B)s Fv(\))170 2346 y(=)h Fs(8)o Fr(~)-23 b(x)n Fs(8)p Fr(x:\031)376 2353 y Fi(1)393 2346 y Fv(\()p Fr(x)p Fv(\))14 b Ft(mr)e Fr(A)p Fv([)p Fr(x)h Fv(:=)g Fr(\031)741 2353 y Fi(0)761 2346 y Fv(\()p Fr(x)p Fv(\)])g Fs(!)g Fr(")h Ft(mr)f Fv(\()p Fs(8)p Fr(x:A)e Fs(!)j Fr(B)s Fv(\))f Fs(!)h Fr(")f Ft(mr)g Fr(B)170 2406 y Fv(=)h Fs(8)o Fr(~)-23 b(x)n Fs(8)p Fr(x:\031)376 2413 y Fi(1)393 2406 y Fv(\()p Fr(x)p Fv(\))14 b Ft(mr)e Fr(A)p Fv([)p Fr(x)h Fv(:=)g Fr(\031)741 2413 y Fi(0)761 2406 y Fv(\()p Fr(x)p Fv(\)])g Fs(!)g(8)p Fr(x)8 b(")13 b Ft(mr)f Fv(\()p Fr(A)i Fs(!)f Fr(B)s Fv(\))h Fs(!)f Fr(")h Ft(mr)e Fr(B)170 2467 y Fv(=)i Fs(8)o Fr(~)-23 b(x)n Fs(8)p Fr(x:\031)376 2474 y Fi(1)393 2467 y Fv(\()p Fr(x)p Fv(\))14 b Ft(mr)e Fr(A)p Fv([)p Fr(x)h Fv(:=)g Fr(\031)741 2474 y Fi(0)761 2467 y Fv(\()p Fr(x)p Fv(\)])g Fs(!)g(8)p Fr(x)p Fs(8)p Fr(y)r Fv(\()p Fr(y)f Ft(mr)h Fr(A)g Fs(!)h Fr(")g Ft(mr)e Fr(B)s Fv(\))h Fs(!)h Fr(")g Ft(mr)e Fr(B)s(:)-1 2563 y Fv(Hence)k(w)o(e)i(can)g(de\014ne)g Fr(\026)p Fv(\()p Fs(9)529 2543 y Fu(\003\000)529 2576 y Fj(x;A;B)625 2563 y Fv(\))f(=)g Fr(\025)o(~)-23 b(x\025x\025u\025v)r (:v)r(\031)1006 2570 y Fi(0)1024 2563 y Fv(\()p Fr(x)p Fv(\))p Fr(\031)1118 2570 y Fi(1)1137 2563 y Fv(\()p Fr(x)p Fv(\))p Fr(u)p Fv(.)26 b Fn(Sub)n(c)n(ase)d Fr(\034)6 b Fv(\()p Fr(A)p Fv(\))16 b(=)h Fs(\003)g(6)p Fv(=)f Fr(\034)6 b Fv(\()p Fr(B)s Fv(\).)-1 2624 y(Then)16 b(w)o(e)g(ha)o(v)o (e)f([)-8 b([)p Fs(9)358 2603 y Fu(\003\000)358 2636 y Fj(x;A;B)453 2624 y Fv(])g(])13 b(=)g Fr(\025)o(~)-23 b(x\025x\025z)r Fv(\()p Fr(z)r(x)p Fv(\))17 b(and)g(w)o(e)e(obtain)297 2722 y Fr(\025)o(~)-23 b(x\025x\025z)r Fv(\()p Fr(z)r(x)p Fv(\))14 b Ft(mr)e Fs(8)o Fr(~)-23 b(x)o Fv([)p Fs(9)748 2704 y Fu(\003)767 2722 y Fr(xA)13 b Fs(!)h Fv(\()p Fs(8)p Fr(x:A)d Fs(!)j Fr(B)s Fv(\))f Fs(!)h Fr(B)s Fv(])297 2783 y(=)g Fs(8)o Fr(~)-23 b(x)n Fs(8)p Fr(x:x)12 b Ft(mr)g Fs(9)626 2765 y Fu(\003)645 2783 y Fr(xA)i Fs(!)f Fr(\025z)r Fv(\()p Fr(z)r(x)p Fv(\))h Ft(mr)e Fv(\(\()p Fs(8)p Fr(x:A)g Fs(!)h Fr(B)s Fv(\))h Fs(!)f Fr(B)s Fv(\))297 2843 y(=)h Fs(8)o Fr(~)-23 b(x)n Fs(8)p Fr(x:")12 b Ft(mr)g Fr(A)i Fs(!)f(8)p Fr(z)r(:z)h Ft(mr)e Fv(\()p Fs(8)p Fr(x:A)g Fs(!)h Fr(B)s Fv(\))h Fs(!)f Fr(z)r(x)h Ft(mr)e Fr(B)297 2903 y Fv(=)i Fs(8)o Fr(~)-23 b(x)n Fs(8)p Fr(x:")12 b Ft(mr)g Fr(A)i Fs(!)f(8)p Fr(z)r(:)p Fs(8)p Fr(x)8 b(z)r(x)i Ft(mr)j Fv(\()p Fr(A)g Fs(!)h Fr(B)s Fv(\))f Fs(!)h Fr(z)r(x)f Ft(mr)g Fr(B)297 2963 y Fv(=)h Fs(8)o Fr(~)-23 b(x)n Fs(8)p Fr(x:")12 b Ft(mr)g Fr(A)i Fs(!)f(8)p Fr(z)r(:)p Fv(\()p Fs(8)p Fr(x:)o(")e Ft(mr)h Fr(A)i Fs(!)f Fr(z)r(x)h Ft(mr)e Fr(B)s Fv(\))i Fs(!)f Fr(z)r(x)h Ft(mr)e Fr(B)s(:)p eop %%Page: 11 11 11 10 bop -1 53 a Fv(Hence)16 b(w)o(e)h(can)g(de\014ne)g Fr(\026)p Fv(\()p Fs(9)526 33 y Fu(\003\000)526 66 y Fj(x;A;B)623 53 y Fv(\))e(=)h Fr(\025)o(~)-23 b(x\025x\025u\025v)r(:v)r (xu)p Fv(.)24 b Fn(Sub)n(c)n(ase)e Fr(\034)6 b Fv(\()p Fr(A)p Fv(\))15 b Fs(6)p Fv(=)g Fs(\003)h(6)p Fv(=)g Fr(\034)6 b Fv(\()p Fr(B)s Fv(\).)24 b(Then)18 b(w)o(e)-1 114 y(ha)o(v)o(e)d([)-8 b([)p Fs(9)159 93 y Fu(\003\000)159 126 y Fj(x;A;B)254 114 y Fv(])g(])12 b(=)i Fr(\025)o(~)-23 b(x\025x\025z)r Fv(\()p Fr(z)r(\031)575 121 y Fi(0)595 114 y Fv(\()p Fr(x)p Fv(\))p Fr(\031)689 121 y Fi(1)708 114 y Fv(\()p Fr(x)p Fv(\)\))16 b(and)h(w)o(e)f(obtain)268 228 y Fr(\025)o(~)-23 b(x\025x\025z)r Fv(\()p Fr(z)r(\031)505 235 y Fi(0)525 228 y Fv(\()p Fr(x)p Fv(\))p Fr(\031)619 235 y Fi(1)638 228 y Fv(\()p Fr(x)p Fv(\)\))13 b Ft(mr)g Fs(8)o Fr(~)-23 b(x)n Fv([)p Fs(9)917 210 y Fu(\003)936 228 y Fr(xA)13 b Fs(!)h Fv(\()p Fs(8)p Fr(x:A)d Fs(!)j Fr(B)s Fv(\))f Fs(!)h Fr(B)s Fv(])268 288 y(=)g Fs(8)o Fr(~)-23 b(x)n Fs(8)p Fr(x:x)12 b Ft(mr)g Fs(9)597 270 y Fu(\003)616 288 y Fr(xA)i Fs(!)f Fr(\025z)r Fv(\()p Fr(z)r(\031)883 295 y Fi(0)903 288 y Fv(\()p Fr(x)p Fv(\))p Fr(\031)997 295 y Fi(1)1016 288 y Fv(\()p Fr(x)p Fv(\)\))g Ft(mr)g Fv(\(\()p Fs(8)p Fr(x:A)e Fs(!)j Fr(B)s Fv(\))f Fs(!)h Fr(B)s Fv(\))268 349 y(=)g Fs(8)o Fr(~)-23 b(x)n Fs(8)p Fr(x:\031)474 356 y Fi(1)492 349 y Fv(\()p Fr(x)p Fv(\))13 b Ft(mr)f Fr(A)p Fv([)p Fr(x)h Fv(:=)g Fr(\031)839 356 y Fi(0)859 349 y Fv(\()p Fr(x)p Fv(\)])g Fs(!)366 409 y(8)p Fr(z)r(:z)g Ft(mr)g Fv(\()p Fs(8)p Fr(x:A)e Fs(!)j Fr(B)s Fv(\))f Fs(!)h Fr(z)r(\031)945 416 y Fi(0)964 409 y Fv(\()p Fr(x)p Fv(\))p Fr(\031)1058 416 y Fi(1)1077 409 y Fv(\()p Fr(x)p Fv(\))g Ft(mr)e Fr(B)268 469 y Fv(=)i Fs(8)o Fr(~)-23 b(x)n Fs(8)p Fr(x:\031)474 476 y Fi(1)492 469 y Fv(\()p Fr(x)p Fv(\))13 b Ft(mr)f Fr(A)p Fv([)p Fr(x)h Fv(:=)g Fr(\031)839 476 y Fi(0)859 469 y Fv(\()p Fr(x)p Fv(\)])g Fs(!)366 529 y(8)p Fr(z)r(:)p Fs(8)o Fr(x)p Fs(8)o Fr(y)q Fv(\()p Fr(y)g Ft(mr)f Fr(A)i Fs(!)f Fr(z)r(xy)i Ft(mr)e Fr(B)s Fv(\))g Fs(!)h Fr(z)r(\031)1161 536 y Fi(0)1180 529 y Fv(\()p Fr(x)p Fv(\))p Fr(\031)1274 536 y Fi(1)1293 529 y Fv(\()p Fr(x)p Fv(\))f Ft(mr)g Fr(B)s(:)-1 642 y Fv(Hence)i(w)o(e)g(can)i(de\014ne)f Fr(\026)p Fv(\()p Fs(9)522 621 y Fu(\003\000)522 654 y Fj(x;A;B)618 642 y Fv(\))e(=)f Fr(\025)o(~)-23 b(x)q(\025x\025u\025z) r(\025v)r(:v)r(\031)1046 649 y Fi(0)1064 642 y Fv(\()p Fr(x)p Fv(\))p Fr(\031)1158 649 y Fi(1)1178 642 y Fv(\()p Fr(x)p Fv(\))p Fr(u)p Fv(.)p 1821 612 21 2 v 1821 640 2 28 v 1839 640 V 1821 642 21 2 v 72 702 a(If)20 b Fr(B)j Fv(is)d Fs(9)266 684 y Fu(\003)286 702 y Fv(-free,)g(then)h Fr(")g Ft(mr)e Fr(B)24 b Fv(=)d Fr(B)s Fv(.)34 b(Hence)19 b(for)i Fs(8)p Fr(x)1157 684 y Fj(\032)1175 702 y Fs(9)1203 684 y Fu(\003)1223 702 y Fr(y)1249 684 y Fj(\033)1272 702 y Fr(B)i Fv(with)d Fs(9)1475 684 y Fu(\003)1495 702 y Fv(-free)g Fr(B)j Fv(w)o(e)d(ha)o(v)o(e)-1 762 y Fr(\034)6 b Fv(\()p Fs(8)p Fr(x)p Fs(9)p Fr(y)156 744 y Fu(\003)173 762 y Fr(B)s Fv(\))13 b(=)h Fr(\032)g Fs(!)f Fr(\033)18 b Fv(and)603 872 y Fr(t)13 b Ft(mr)g Fs(8)p Fr(x)p Fs(9)803 852 y Fu(\003)820 872 y Fr(y)r(B)j Fv(=)e Fs(8)p Fr(xB)s Fv([)p Fr(y)f Fv(:=)g Fr(tx)p Fv(])p Fr(:)-1 982 y Fv(Then)j(as)h(a)g (corollary)e(to)i(the)f(soundness)h(theorem)e(w)o(e)h(obtain)h(the)f (extraction)f(theorem)-1 1096 y Ft(Theorem)h(2.10)24 b Fn(F)l(r)n(om)18 b(a)g(derivation)h Fr(M)5 b Fv(:)j Fs(8)p Fr(x)896 1078 y Fj(\032)915 1096 y Fs(9)943 1078 y Fu(\003)962 1096 y Fr(y)988 1078 y Fj(\033)1011 1096 y Fr(B)21 b Fn(with)e Fr(B)i Fs(9)1262 1078 y Fu(\003)1282 1096 y Fn(-fr)n(e)n(e)d(fr)n(om)f Fs(9)1537 1078 y Fu(\003)1557 1096 y Fn(-fr)n(e)n(e)h(assump-)-1 1157 y(tions)h Fv(\000)h Fn(one)g(c)n(an)f(extr)n(act)h(a)f(close)n(d)h(term)f Fv([)-8 b([)p Fr(M)5 b Fv(])-8 b(])916 1139 y Fj(\032)p Fu(!)p Fj(\033)1010 1157 y Fn(such)20 b(that)f(the)h(formula)f Fs(8)p Fr(xB)s Fv([)p Fr(y)d Fv(:=)h([)-8 b([)p Fr(M)5 b Fv(])-8 b(])p Fr(x)p Fv(])-1 1217 y Fn(is)17 b(pr)n(ovable)h(fr)n(om) e Fv(\000)p Fn(.)72 1331 y Fv(Here)f(\000)i(should)f(b)q(e)h(view)o(ed) d(as)j(lemmata,)c(i.e.)i(true)h(form)o(ulas)f(\(pro)o(v)o(ed)g (separately)l(,)h(to)g(k)o(eep)-1 1391 y Fr(M)25 b Fv(short\).)33 b(The)20 b(theorem)e(sa)o(ys)j(that)f(the)g(extracted)f(program)h(is)g (indep)q(enden)o(t)f(of)h(ho)o(w)g(this)-1 1451 y(shortcut)c(is)g(ac)o (hiev)o(ed.)-1 1587 y Ft(3)56 b(Computational)17 b(Con)n(ten)n(t)j(of)e (Classical)h(Pro)r(ofs)-1 1696 y Fn(3.1)49 b(De\014nite)19 b(and)f(Go)n(al)f(F)l(ormulas)-1 1806 y Fv(F)l(or)23 b(simplicit)o(y)d(w)o(e)j(only)g(treat)h(form)o(ulas)e(in)i(the)f Fs(!8)f Fv(fragmen)o(t;)j(this)f(is)f(not)h(an)g(essen)o(tial)-1 1866 y(restriction,)14 b(since)i(conjunctions)g(can)h(b)q(e)f(easily)g (remo)o(v)o(ed.)72 1926 y(A)21 b(form)o(ula)f(is)h Fn(r)n(elevant)28 b Fv(if)21 b(it)g(\\ends")h(with)g Fs(?)p Fv(.)36 b(More)22 b(precisely)l(,)e(relev)m(an)o(t)h(form)o(ulas)f(are)-1 1986 y(de\014ned)c(inductiv)o(ely)d(b)o(y)j(the)g(clauses)71 2088 y Fs(\017)25 b(?)16 b Fv(is)g(relev)m(an)o(t,)71 2190 y Fs(\017)25 b Fv(if)15 b Fr(C)20 b Fv(is)c(relev)m(an)o(t)f(and)i Fr(B)i Fv(is)d(an)h(arbitrary)f(form)o(ula,)e(then)j Fr(B)f Fs(!)e Fr(C)19 b Fv(is)d(relev)m(an)o(t,)f(and)71 2291 y Fs(\017)25 b Fv(if)15 b Fr(C)20 b Fv(is)c(relev)m(an)o(t,)f (then)h Fs(8)p Fr(xC)i Fv(is)e(relev)m(an)o(t.)-1 2393 y(A)f(form)o(ula)g(whic)o(h)h(is)g(not)h(relev)m(an)o(t)e(is)h(called)f Fn(irr)n(elevant)5 b Fv(.)72 2453 y(W)l(e)17 b(de\014ne)g Fn(go)n(al)h(formulas)j Fr(G)d Fv(and)g Fn(de\014nite)i(formulas)h Fr(D)e Fv(inductiv)o(ely)l(.)i(These)c(notions)h(are)-1 2513 y(related)g(to)h(similar)e(ones)i(common)e(under)i(the)g(same)f (name)g(in)g(the)h(con)o(text)f(of)h(extensions)g(of)-1 2574 y(logic)c(programming.)20 b(Let)d Fr(P)23 b Fv(range)17 b(o)o(v)o(er)e(atoms)h(\(including)f Fs(?)p Fv(\).)185 2682 y Fr(G)42 b Fv(:=)f Fr(P)52 b Fs(j)14 b Fr(D)h Fs(!)f Fr(G)132 b Fv(pro)o(vided)16 b Fr(D)i Fv(irrelev)m(an)o(t)d Fs(\))h Fr(D)i Fv(quan)o(ti\014er-free)441 2742 y Fs(j)c(8)p Fr(xG)194 b Fv(pro)o(vided)16 b Fr(G)h Fv(irrelev)m(an)o(t)185 2828 y Fr(D)43 b Fv(:=)e Fr(P)49 b Fs(j)14 b Fr(G)g Fs(!)g Fr(D)133 b Fv(pro)o(vided)16 b Fr(D)i Fv(irrelev)m(an)o(t)d Fs(\))h Fr(G)h Fv(irrelev)m(an)o(t)441 2888 y Fs(j)d(8)p Fr(xD)p eop %%Page: 12 12 12 11 bop -1 53 a Ft(Lemm)o(a)16 b(3.1)24 b Fn(F)l(or)19 b(de\014nite)i(formulas)e Fr(D)q Fn(,)i(r)n(elevant)g(go)n(al)e (formulas)g Fr(G)h Fn(and)g(an)g(arbitr)n(ary)d(for-)-1 114 y(mula)g Fr(A)g Fn(we)i(have)f(derivations)687 193 y Fr(N)731 175 y Fj(A)726 206 y(D)801 193 y Fv(:)8 b Fr(D)16 b Fs(!)d Fr(D)983 175 y Fj(A)687 253 y Fr(H)731 235 y Fj(A)727 266 y(G)801 253 y Fv(:)8 b Fr(G)861 235 y Fj(A)904 253 y Fs(!)13 b(:)p Fr(G)i Fs(!)e Fr(A)72 345 y Fv(The)21 b(pro)q(of)h(is)f(b)o(y)f(induction)h(on)g(de\014nite)f (and)i(goal)g(form)o(ulas;)g(it)e(is)h(necessary)g(to)g(pro)o(v)o(e)-1 406 y(sev)o(eral)16 b(additional)i(claims)e(sim)o(ultaneously)l(,)f(to) j(get)g(the)g(induction)f(through.)27 b(F)l(or)17 b(details)h(w)o(e)-1 466 y(refer)d(to)i([1].)-1 561 y Ft(Theorem)f(3.2)24 b Fn(L)n(et)13 b Fr(D)452 568 y Fi(1)472 561 y Fr(;)8 b(:)g(:)g(:)g(;)g(D)622 568 y Fj(l)648 561 y Fn(b)n(e)14 b(r)n(elevant)g(and)g Fr(D)1014 568 y Fj(l)p Fi(+1)1072 561 y Fr(;)8 b(:)g(:)g(:)g(;)g(D)1222 568 y Fj(n)1259 561 y Fn(irr)n(elevant)14 b(de\014nite)h(formulas,)-1 621 y(and)21 b Fr(G)135 628 y Fi(1)155 621 y Fr(;)8 b(:)g(:)g(:)f(;)h (G)302 628 y Fj(k)345 621 y Fn(b)n(e)21 b(r)n(elevant)i (quanti\014er-fr)n(e)n(e)f(and)f Fr(G)1048 628 y Fj(k)q Fi(+1)1115 621 y Fr(;)8 b(:)g(:)g(:)f(;)h(G)1262 628 y Fj(m)1317 621 y Fn(irr)n(elevant)21 b(go)n(al)h(formulas.)-1 681 y(L)n(et)17 b Fr(A)c Fv(:=)g Fs(9)226 663 y Fu(\003)246 681 y Fr(y)279 669 y(~)272 681 y(G)k Fn(and)128 775 y Fr(t)d Fv(:=)f Fr(\025y)r(;)7 b(~)-23 b(x:)p Ft(if)22 b Fs(:)p Fr(G)469 782 y Fi(1)506 775 y Ft(then)c Fv([)-8 b([)p Fr(H)698 757 y Fj(A)694 787 y(G)721 792 y Fh(1)740 775 y Fv(])g(]\()p Fr(x)807 782 y Fi(1)825 775 y Fv(\))17 b Ft(else)f Fr(:)8 b(:)g(:)17 b Ft(if)22 b Fs(:)p Fr(G)1168 782 y Fj(k)1208 775 y Ft(then)17 b Fv([)-8 b([)p Fr(H)1399 757 y Fj(A)1395 787 y(G)1422 793 y Fg(k)1443 775 y Fv(])g(]\()p Fr(x)1510 782 y Fj(k)1530 775 y Fv(\))17 b Ft(else)f Fr(y)r(:)-1 869 y Fn(Assume)i(that)f(we)h(have)g(a)g(derivation)628 962 y Fr(M)5 b Fv(:)710 949 y Fr(~)702 962 y(D)16 b Fs(!)e Fv(\()p Fs(8)p Fr(y)r(:)917 949 y(~)910 962 y(G)e Fs(!)i(?)p Fv(\))f Fs(!)h(?)p Fr(:)-1 1056 y Fn(L)n(et)i Fr(M)134 1037 y Fj(A)179 1056 y Fn(denote)i(the)f(r)n(esult)f(of)g(substituting) j Fs(?)d Fn(by)g Fr(A)g Fn(everywher)n(e)h(in)g Fr(M)5 b Fn(.)23 b(Then)17 b(we)g(c)n(an)f(derive)529 1137 y Fr(~)522 1149 y(D)f Fs(!)f Fv([)-8 b([)p Fr(M)713 1129 y Fj(A)741 1149 y Fv(])g(][)g([)p Fr(N)825 1129 y Fj(A)820 1161 y(D)849 1166 y Fh(1)866 1149 y Fv(])g(])8 b Fr(:)g(:)g(:)e Fv([)-8 b([)p Fr(N)1022 1129 y Fj(A)1017 1161 y(D)1046 1167 y Fg(l)1059 1149 y Fv(])g(])p Fr(t)13 b Ft(mr)f Fs(9)1221 1129 y Fu(\003)1240 1149 y Fr(y)1273 1137 y(~)1266 1149 y(G:)72 1244 y Fv(The)i(pro)q(of)h(uses)f(the)f(soundness)i (theorem)e(2.9)h(and)g(lemma)d(3.1.)21 b(F)l(or)14 b(details)f(w)o(e)g (again)i(ha)o(v)o(e)-1 1305 y(to)h(refer)g(to)g([1].)-1 1432 y Fn(3.2)49 b(Example:)24 b(Inte)n(ger)18 b(Squar)n(e)f(R)n(o)n (ots)-1 1542 y Fv(Let)g Fr(f)5 b Fv(:)j Fr(\023)17 b Fs(!)f Fr(\023)h Fv(b)q(e)h(un)o(b)q(ounded)g(with)g Fr(f)5 b Fv(0)16 b(=)g(0;)i(think)f(of)h Fr(f)23 b Fv(as)18 b(the)f(square)h(function)f Fr(f)5 b Fv(\()p Fr(n)p Fv(\))17 b(=)f Fr(n)1808 1524 y Fi(2)1828 1542 y Fv(.)-1 1602 y(W)l(e)j(w)o(an)o(t)g(to)h(pro)o(v)o(e)f(that)h(in)o(teger)e(square)i (ro)q(ots)h(alw)o(a)o(ys)e(exist,)g(or)h(more)e(precisely)g(a)h (general)-1 1662 y(form)h(of)j(this)f(prop)q(osition,)i(using)e(only)g (the)f(t)o(w)o(o)h(prop)q(erties)g(of)g Fr(f)28 b Fv(ab)q(o)o(v)o(e.)38 b(W)l(e)21 b(sp)q(ecify)h(our)-1 1722 y(problem)15 b(as)j(follo)o(ws.) 23 b(Here)16 b Fr(f)s(;)8 b(g)r(;)g(n)17 b Fv(are)g(parameters;)f Fr(g)k Fv(is)c(used)i(as)f(an)h(explicit)d(witness)i(of)g(the)-1 1782 y(un)o(b)q(oundedness)g(of)f Fr(f)5 b Fv(.)173 1876 y Fs(8)p Fr(n)j Fs(:)p Fr(n)g Fv(0)j(\(using)f(the)g(fact)g(that)h(this)f(do)q (esn't)h(c)o(hange)f(the)g(ideal\).)-1 2583 y Fn(Implementation)-1 2675 y Fv(The)h(gcd)g(example)e(has)j(b)q(een)g(implem)o(e)o(n)o(ted)c (in)j(the)g(in)o(teractiv)o(e)e(pro)q(of)j(system)e Fm(Minlog)p Fv(.)23 b(W)l(e)-1 2735 y(sho)o(w)16 b(the)g(term)f(whic)o(h)h(w)o(as)g (extracted)g(automatically)e(from)h(a)i(deriv)m(ation)f(of)h(the)f (theorem.)-1 2837 y Fd(\(lambda)23 b(\(a1\))24 2897 y(\(lambda)g (\(a2\))50 2957 y(\(\(\(\(\(\(nat-)o(re)o(c-a)o(t)g('\(arrow)g(nat)h (\(arrow)g(nat)g(\(star)g(nat)h(nat\)\)\)\))p eop %%Page: 20 20 20 19 bop 178 53 a Fd(\(lambda)23 b(\(k1\))h(\(lambda)f(\(k2\))i (\(cons)e(n000)h(n000\)\)\)\))152 114 y(\(lambda)f(\(n\))178 174 y(\(lambda)g(\(w\))204 234 y(\(lambda)g(\(k1\))229 294 y(\(lambda)g(\(k2\))255 354 y(\(\(\(\(if-at)f('\(star)i(nat)g (nat\)\))332 415 y(\(\(<-strict)o(-n)o(at)e(0\))j(r2\)\))306 475 y(\(\(w)g(l21\))f(l22\)\))306 535 y(\(\(\(\(if-at)f('\(star)g(nat)i (nat\)\))357 595 y(\(\(<-strict-)o(nat)d(0\))j(r1\)\))357 655 y(\(\(w)g(l11\))f(l12\)\))332 715 y(\(cons)g(k1)h(k2\)\)\)\)\)\)\)) o(\))127 776 y(\(\(plus-na)o(t)e(a2\))h(1\)\))101 836 y(0\))76 896 y(1\)\)\))-1 998 y Fv(W)l(e)f(ha)o(v)o(e)f(man)o(ually)f (in)o(tro)q(duced)i Fd(r1,)i(r2,)f(l11,)g(l12,)g(l21,)h(l22)d Fv(for)h(somewhat)g(length)o(y)-1 1058 y(terms)14 b(corresp)q(onding)i (to)g(our)h(abbreviations)e Fr(r)915 1065 y Fj(i)929 1058 y Fv(,)958 1045 y Fr(~)959 1058 y(`)979 1065 y Fj(i)993 1058 y Fv(.)21 b(The)16 b(un)o(b)q(ound)h(v)m(ariable)e Fd(n000)f Fv(app)q(earing)-1 1118 y(in)j(the)h(base)g(case)g(is)g(a)g (dumm)o(y)d(v)m(ariable)j(used)g(b)o(y)f(the)h(system)e(when)i(it)g(is) g(ask)o(ed)f(to)i(pro)q(duce)-1 1178 y(a)e(realizing)e(term)g(for)i (the)g(instance)f Fs(?)f(!)f(9)p Fr(k)r(A)p Fv(\()p Fr(k)r Fv(\))i(of)h(ex-falso-quo)q(dlib)q(et.)23 b(In)16 b(our)i(case,)e(when) -1 1239 y(the)h(existen)o(tial)f(quan)o(ti\014er)h(is)h(of)g(t)o(yp)q (e)f Fr(\023)i Fv(one)f(migh)o(t)e(as)i(w)o(ell)f(pic)o(k)f(the)i (constan)o(t)g(0)h(\(as)f(w)o(e)f(did)-1 1299 y(in)f(the)g(text\).)-1 1421 y Fc(References)-1 1517 y Fb([1])23 b(Ulric)o(h)11 b(Berger,)f(Wilfried)i(Buc)o(hholz,)f(and)g(Helm)o(ut)f(Sc)o(h)o(wic)o (h)o(ten)o(b)q(erg.)i(Re\014ned)g(program)d(extraction)71 1564 y(from)14 b(classical)j(pro)q(ofs.)j(In)15 b(preparation.)-1 1629 y([2])23 b(Ulric)o(h)d(Berger)f(and)g(Helm)o(ut)g(Sc)o(h)o(wic)o (h)o(ten)o(b)q(erg.)31 b(The)19 b(greatest)f(common)g(divisor:)i(a)e (case)h(study)71 1676 y(for)c(program)f(extraction)h(from)g(classical)i (pro)q(ofs.)j(In)c(S.)f(Berardi)h(and)g(M.)e(Copp)q(o,)h(editors,)h Fa(T)m(yp)n(es)71 1723 y(for)h(Pr)n(o)n(ofs)e(and)i(Pr)n(o)n(gr)n(ams.) f(International)f(Workshop)i(TYPES)e('95,)i(T)m(orino,)e(Italy,)h(June) g(1995.)71 1770 y(Sele)n(cte)n(d)c(Pap)n(ers)p Fb(,)f(v)o(olume)h(1158) f(of)h Fa(L)n(e)n(ctur)n(e)g(Notes)h(in)f(Computer)i(Scienc)n(e)p Fb(,)c(pages)i(36{46.)e(Springer)71 1817 y(V)l(erlag,)15 b(Berlin,)i(Heidelb)q(erg,)g(New)e(Y)l(ork,)g(1996.)-1 1883 y([3])23 b(Thierry)14 b(Co)q(quand)f(and)g(Hendrik)i(P)o(ersson.)g (Gr\177)-23 b(obner)13 b(Bases)g(in)h(T)o(yp)q(e)g(Theory.)i(In)e(T.)e (Altenkirc)o(h,)71 1930 y(W.)k(Narasc)o(hewski,)h(and)g(B.)g(Reus,)h (editors,)f Fa(T)m(yp)n(es)f(for)j(Pr)n(o)n(ofs)e(and)h(Pr)n(o)n(gr)n (ams)p Fb(,)e(v)o(olume)i(1657)e(of)71 1976 y Fa(L)n(e)n(ctur)n(e)e (Notes)h(in)g(Computer)h(Scienc)n(e)p Fb(.)c(Springer)j(V)l(erlag,)f (Berlin,)h(Heidelb)q(erg,)h(New)e(Y)l(ork,)g(1999.)-1 2042 y([4])23 b(Anne)c(S.)f(T)l(ro)q(elstra)g(\(editor\).)29 b Fa(Metamathematic)n(al)19 b(Investigation)f(of)h(Intuitionistic)f(A)o (rithmetic)71 2089 y(and)e(A)o(nalysis)p Fb(,)d(v)o(olume)j(344)f(of)g Fa(L)n(e)n(ctur)n(e)g(Notes)h(in)g(Mathematics)p Fb(.)k(Springer)c(V)l (erlag,)f(Berlin,)i(Hei-)71 2136 y(delb)q(erg,)f(New)f(Y)l(ork,)g (1973.)-1 2201 y([5])23 b(Harv)o(ey)16 b(F)l(riedman.)22 b(Classically)c(and)e(in)o(tuitionisticall)q(y)j(pro)o(v)m(ably)d (recursiv)o(e)h(functions.)23 b(In)17 b(D.S.)71 2248 y(Scott)d(and)g(G.H.)f(M)q(\177)-24 b(uller,)15 b(editors,)f Fa(Higher)i(Set)f(The)n(ory)p Fb(,)e(v)o(olume)i(669)e(of)h Fa(L)n(e)n(ctur)n(e)h(Notes)g(in)g(Math-)71 2295 y(ematics)p Fb(,)g(pages)g(21{28.)e(Springer)j(V)l(erlag,)f(Berlin,)i(Heidelb)q (erg,)g(New)e(Y)l(ork,)g(1978.)-1 2361 y([6])23 b(Ulric)o(h)14 b(Kohlen)o(bac)o(h.)j(Analyzing)d(pro)q(ofs)e(in)h(analysis.)k(In)c(W.) f(Ho)q(dges,)g(M.)g(Hyland,)h(C.)f(Steinhorn,)71 2408 y(and)g(J.)f(T)l(russ,)h(editors,)f Fa(L)n(o)n(gic:)h(fr)n(om)h(F)m (oundations)f(to)i(Applic)n(ations.)e(Eur)n(op)n(e)n(an)g(L)n(o)n(gic)g (Col)r(lo)n(quium)71 2455 y(\(Ke)n(ele,)j(1993\))p Fb(,)g(pages)g (225{260.)e(Oxford)i(Univ)o(ersit)o(y)h(Press,)e(1996.)-1 2520 y([7])23 b(Daniel)18 b(Leiv)m(an)o(t.)26 b(Syn)o(tactic)17 b(translations)g(and)g(pro)o(v)m(ably)h(recursiv)o(e)g(functions.)25 b Fa(The)18 b(Journal)g(of)71 2567 y(Symb)n(olic)d(L)n(o)n(gic)p Fb(,)f(50\(3\):682{68)o(8,)e(Septem)o(b)q(er)k(1985.)-1 2633 y([8])23 b(Chetan)16 b(Murth)o(y)l(.)22 b(Extracting)15 b(constructiv)o(e)i(con)o(ten)o(t)e(from)g(classical)j(pro)q(ofs.)k(T)l (ec)o(hnical)c(Rep)q(ort)71 2680 y(90{1151,)13 b(Dep.of)h (Comp.Science,)i(Cornell)h(Univ.,)e(Ithaca,)g(New)g(Y)l(ork,)g(1990.)j (PhD)d(thesis.)-1 2745 y([9])23 b(M.H.A.)12 b(Newman.)17 b(On)e(theories)f(with)g(a)f(com)o(binatorial)h(de\014nition)h(of)f (\\equiv)m(alence".)19 b Fa(A)o(nnals)13 b(of)71 2792 y(Mathematics)p Fb(,)i(43\(2\):223{24)o(3,)d(1942.)p eop %%Trailer end userdict /end-hook known{end-hook}if %%EOF