; TeX output 1995.04.01:1531g\32\ܚ@P7"Vff cmbx10ProgramExtractionfromClassicalProuofs#}ZrK`y cmr10UlrichUUBergerandHelmutSchwichtenbGergi6o cmr9Mathematisc9hesTInstitutderUniversit`atMA;unchen,D{80333MA;unchen,Germany Hst : cmbx9Abstract.y&Di eren9t)methoAdsforextractingprogramsfromaclassical HsproAofsarein9vestigated.AzdirectmethodbasedonnormalizationandtheHsw9ellknownnegativetranslationcombinedwitharealizabilityinterpreta-Hstion*arecomparedandsho9wntoyieldequalresults.F:urthermore,theHstranslationȽmethoAdisre nedinordertoobtainoptimizedprograms.AnHsanalysisoftheproAoftranslationsho9wsthatinmanycasesonlysmallHspartsUofaclassicalproAofneedtobetranslated.ProofsextractedfromHssuc9hre nedtranslationshavesimplertypAeandcontrolstructure.TheHse ectTofthere nemen9tsisdemonstratedattwoexamples.#@,0N cmbx121 Intro`ductionM,ItGiswellknownthatfromaclassicalproGofof!", cmsy108 b> cmmi10x9yBq(x;y[),GBBquanti er{free, ,onevcanextractaprogramtsuchthat8xBq(x;tx)vholds.W*ediscusstwopGossi-,bilitiestodothis.1.AdirectmethoGd,whichusestheclassicalproofandproof,normalizationFdirectlyasanalgorithm.2.AFtranslationoftheclassicalproGof,intoXanintuitionisticonefromwhichviaarealizabilityinterpretationaprogram,canUUbGeextracted.W*eshowthatbothmethodsyieldthesamealgorithm. [܍;F*urthermoreLwetrytoanswerthequestionif\programsfromclassicalproGofs",isYeausefuldevicepractically*.WeapplytheproGoftranslationtoasimplebut,informativeexample:W*eproveclassicallythatw.r.t.anunbGoundedfunction,f:IUXNI!-'IUXN1suchthatf(0)-'=0eachnhasaroGotm,i.e.,f(m)-'nthetermsofGodel'ssystemT,i.e.builtfromtypGedvqariablesx^ 0ercmmi7$, cRtheconstantstrueRHٓRcmr7b7oole(Ӭ,falseğb7oole*>W,0^nat  ,S^nat ^ O!cmsy7!nat ,R:Ǵ!(nat !!)!nat!͍nat ;Z8(recur-} Rsion),R1ɍǴ!!b7oole!vb7oole;:(caseanalysis)bypairinghr;si^Ȼ,pro8jectioniTL(rG^Zcmr50 1!)^O \cmmi5i,RabstractionUU(x^$rG^)^!andapplication(rG^!ȼs^)^b.aW*eUUhavetheusualconversions(writingt8+1forSt)tۈ (xrG)s$! rG[s=x];iTLhr0|s;r1i$! riTL;a7Rnat ;DrGs0$! r;Rnat ;DrGs(t8+1)$! st(Rnat ;DrGst);Rb7oole;rGstrue$! r;a7Rb7oole;rGsfalse$! s:RIt/iswellknownthateachtermreducestoauniquenormalformw.r.t.these Rconversions(cf.[10 ]).T*osimplifythecalculuswewillidentifytermswiththeRsamenormalform.W*ewillwrite=forequalitymoGdulonormalformsandforRsyntacticalUUidentity*. 7aAtomic+formulasDare#?andPc("V cmbx10tx)wherePisapredicatesymbGolandt (isalistRof\terms.ThetypGesiofthetermstiarespGeci edbythearity(NDF cmmib10N7)ofPc.W*ehaveRatleastonepredicatesymbGolatom.ofarity(bGooleUZ).Theformulaatom3(t)willRplaythesameroleasusuallyti=0doGes.F*requentlywewillabreviateatom(t)Rbypt.W*eassumethatwehaveassignedtoeverypredicatesymbGolPX6=atomofg\32\ܚ,arity(N7)aclosedtermtP oftypGeN n!boolede ningthecharacteristicfunction ,ofUUPc.Thismeansthatweconsideronlydecidablepredicates. V:;F;ormulas4arebuiltfromatomicformulasbyconjunctionA!^^Bq,implica-,tionA2!BM)!Al0/,andd::atom(tmA>)!:Al1=:xarederivqationswhichexistaccordingtoRthecdecidabilityofAandtheaxiomsandassumptionvqariableswithindicesareR(writingUUtforatom=(t))̺.Inds:p;(p!BW=)!(:p!B)!B/U;Ru^A!Bl1ށ,UUu^:A!Bl2B,u^true8!Bl3,u^:true8!Bl4"wh,u^falses!Bl5N,u^:falses!Bl6#o,u͍tmAٍ7 andu͍:tmAٍ8#. aConversionforUUderivqationsisde nedsimilaryasfortermsintheusualway*.kiTL(hd0|s;d1i) ! diTL;ȁ(ud)A!Bށe ! d[e=u];|(xd)8x]A2t ! d[t=x];aIndGn;AUr`de0 ! d;yInd2ٟn;ArXde(t8+1) ! et(Indn;Ar!Jedet)oInd(p;A+srdetrue ! d;Ind˽p;Ar}9defalse ! e:RAgainذitcanbGeshownbystandardmethoGds|justasforGodel'sTv.1.Thesecanbede-R nedeasily*.Furthermorenotethatifets_(d) =r1|s;:::;rk bandets(e)=s#,thenRets^G(d)ets G(e)&=r1|ss ;:::;rks and'xmets(d)=xmr1|s;:::;xrk.'InthelastclauseRtheUU(omitted)typGesare?x$; (y:)(A)Band5_>zWp!(A)!j4=j.);썑RwhereUU!(Bq)=1|s;:::;nq~. KaTheUUfollowingcanbGeprovedeasily*.RLemma.#FVN+(ets G(d))FV(d)8[fx:Ŵ(A)]"Ŵu:u^A J2FA(d)g.]+RLemma.#Wehaveets(d[t=x])=ets5(d)[t=x]andets(d[e=u])=ets5(d)[ets G(e)=xşu L'],Randkifdandehavethesamenormalformthenets(d)andets(e)havethesameRnormalformto}'o.RSoundnessTheorem.p0J cmsl10Assume\thattoanyassumptionvqariableu^A wehave cRassigned?alistx:Q(A)]"Quandanewassumptionvqariable~u<:x:m(A)]"mumr(A.RelativetothisRassignmentc=wecan ndforanyderivqationd:AwithFAM(d)=fu1|s:A1;:::;unq~:AngRaUUderivqation ۩(d):ets (d)mrRA RwithUUFA@((d))f~u1 5:xm1 mr2A1|s;:::;N~un դ:xmnؓmr=Anq~g. RPr}'oof.qUIInductionUUond.RAs anexamplewecomputetheextractedtermsofthederivqationCases9EA;B/)forRcaseUUsplitting. etsf(Cases:A;B')=y:;z:ifntAy 9z Rwhereif!:ʘR j(y:1 ;z1 C:y:1)(y:1;z1:zp1 )andy L;z;yQ1 a;z1.arelistsofvqariablesofRtypGesUUN ::!(Bq).UUClearly썍?ifLJUtrue8r߼s =r; if!false*Mr.s6=sPT:RF*orUUbGetterreadabilityweuseforif !tAr @sthenotation|if͌A then*Pr9AelseUmsd jt6: ܍R3 Pro`oftranslationandthedirectmethodtvRAsTiswellknownaproGofofa89{theoremwithaquanti er{freekernel|where R9isviewedasde nedby:8:|canbGeusedasaprogram.W*edescribea\directRmethoGd"7tousesuchaproofasaprogram(cf.[8]),andcompareitwithGodel'sRnegativetranslationfollowedbyHarveyF*riedman'sA{translation(cf.[2])andRtheUUprogramextractiondescribGedabove.OYg\32\ܚ,3.1 TheTdirectmethoQd,AssumeRwehaveaclassicalderivqationd:8x9yQBq[x;yQ],RBquanti er{free,from ,closedL{assumptionsFA(d)t=fv1|s:8xş1 8C1;:::;vnq~:8xşn -Cng.LW*edescribGean,algorithmgwhich,appliedtoclosedtermsr #,returnstermss XLsuchthatBq[rq;s3],holdsʥprovidedtheassumptionsv1|s;:::;vn <#aretrue.ThealgorithmproGceedsin,threeUUsteps.,081.=InstanciateUUdtor.W*egetdrq:9yQBq[r;yQ],UUi.e.,Xsgdrq:(8y::Bq[r;yQ]!?)!?:ߍ082.=ApplyUUdrtoafreshassumptionvqariableu:8y::Bq[rq;yQ]!?.UUW*egetҺdrqu:?:083.=NormalizeUUdrqu:?.F*romitsnormalform(dru)#UVreado the rstinstanc}'eYs̩:j(drqu)#j:,BelowUUwedescribGehowthe rstinstancej(drqu)#jisobtained. ;ClearlySpwemayassumethatthe{assumptionsviTL:8xşi Cidonotcontain^ ,andthattheformulaBq[rq;yQ]isoftheformCu cmex10CV4V riqBiTL[y:]wheretheBi-donotcontain,^.KThereforethefreshassumptionu:8y::Bq[rq;yQ]!?Kinstep2.mayassumedto,bGe_u:8y::B1|s[y]ب!:::[!Bm[y:]!?._Finallywemayassumethatdcontainsno,freeUUob8jectvqariables.IfitdoGes,substitutearbitraryclosedtermsforthem.;Letd:?(correspGondingto(drqu)#:?abGove)beanormalderivqationwith,FV:*(d)=;UUof?fromassumptionsXNu:8y::B1|s[y]!:::8!Bm[y:]!?;Nv1|s:8C1;:::;vnq~:8Cn,whereB8y::B1|s[y]!:::8!Bm[y:]!?isafalseand8C1|s;:::;8Cnaretrueclosed ,{formulas.W*ede nealistjdjofclosedterms,calledthe rstinstanc}'e^ofd,,suchTthatB1|s[jdj];:::;Bm[jdj]aretrue.jdjisde nedbyinductionond.Sinced,is!normalandFVL(d)=;!itdoGesnotcontainaxioms(exeptthetruthaxiom,,whichisaclosed{formulasandhencemaybGeassumedtobeamongthe{,assumptionsB8CiTL).T*oseethisrecallthatthenormalformofanyclosedtermof,typGe$nat`is$oftheformS(S(S>5:::(S0)::: UO))$andofanyclosedtermoftypGeboole,isxeithertrue+orfalse^;henceallinductionaxiomsunfold.Thereforedisofthe,form -dwDsd1':::|jdk;卑,where^s Fare^closedtermsandd1|s;:::;dkJparederivqationsofclosedquanti er{free,formulas.UUW*edistinguishtwocases.081.=d1|s;:::;dkEuderiveYonlytrueformulas(whichcanbGedecided,sincetheformulas=arebquanti er{freeandclosed).ThenwMEcannotbGeoneofthevi\sinceall8Ci=areUUtrue.Henced=usprinciplethenegativetranslationisnotnecessarysincewecouldpr}'oveRstabilityforallatomicformulasbycasesplitting.However,theseproGofswouldRintroGduceUUcharacteristicfunctionstP Dwhichmightleadtoinecientprograms.aThenegativetranslationreplaceseachatomicformulaP=by(P!>?)!?RandtheA{translationinturnreplacesP7byP_^6mA,whereA:9^xBq.So,attheRend,%Pisreplacedby((P;_^q(A)!A)!A%whichisintuitionisticallyequivqalentRto(PI!sA)!A.Hencewemergethetwostepsandde netheA{tr}'anslationRBq^A ofaformulaB2htobGeobtainedbyreplacinganyatomicsubformulaPofB2hbyR(P{!dA)!A(includingP=d?;thisis,ofcourse,notoptimalbutconvenientRfor`comparisonwiththedirectmethoGd).A0similartranslationfor rstorderlogicRisUUdescribGedin[9],2.3.,page63,Theorem3.16(i).aNote^thatanyderivqationdofsomeformulaBcfromassumptionsC1|s;:::;CnRbGecomesaftertheA{translationaderivqationofBq^A fromC^Al1:;;:::;C^An.T*oseeRthisacrecallthatourlogicalrulesarethoseofminimallogicandhencegivenoextraRtreatment:Stofalsity*.Alsotheaxiomschemes(exeptthetruthaxiom,thefalsityRaxiomSandEfqqƳatom%,whichwillbGeviewedas{assumptions)remaininstancesRofUUthesameaxiomschemeaftertheA{translation.E.g.bGooleanUUinduction Bq[true;=p]!B[false8=p]!8pBRisUUtranslatedinto p}'BqA[true;=p]!BqA[false8=p]!8pBqA;YRwhichUUagainisaninstanceofbGooleanUUinduction.aLetxusloGokatwhathappenswith{assumptionsundertheA{translation.RAgainUUwemayassumethatallformulasconsidereddonotcontain^.RLemmaT1 F;oranyquanti er{fr}'eeformulaCKther}'eisaderivationd:C~4!C^A:. o,g\32\ܚ,Pr}'oof.KUIInductiononC.LetC  B1d!:::ĉ!Bm !R,withanatomR.W*e ,mustUUderive X'(B N!R)!BA?!(R!A)!A:닍,SoUUassumeRs~ϲuU:B3!R;{~\viU:BAፒiޛ;wU:R!A:,W*eUUmustshowA. ;Caseu䍵i::BiforUUsomei.LetBidCci,!PiwithatomsPiTL.Then.kD~evi:Cci AL!(Pid!A)!A,andUUwehaveYۍneeij [u䍵i]:StabCij#jv[ٟ:Cijc:u䍵iuccCi:Efq#qƴPi(v[uj6):Cij ;kneeiTL[u䍵i]:w:DPi;Zi <:u䍵iuccCiwi::Pi:,ByUUIHwehavedCij :Cij !C^A;Zij:.HencektQ~tvvi|(dCi1 pei1P):::(dCin1ieini p)(w:DPi;Zi <:Efq#qƴA!(eiTLwi)):A:;Caseu䍳+i:BiforUUalli.Then?wD(~u~u䍳+1N8:::u+፴m):A;TheUUextractedtermsforthisderivqationareE)dets Zxş1 8;:::;xmmU;z:ifLo:B1|tthen/x519dets፴C115@:::dets፴C1n1r0"2else:::ifLo:Bmthen2x8/m?Kdets፴Cm1:::GOdets፴Cmnm0'elsez ::: z;,whereUUx gi f;z mareUUthelistsofvqariablesassoGciatedwith~vi :B^qA;Zi;wD.:č;HereUUwehaveusedcasesplittingformulasBiTL. ;Updtonow,theformulaAcouldhavebGeenarbitrarilychosen.Ifwewantto ,usetheA{translationtoextractthecomputationalcontentfromaclassicalproGof,weUUhavetochoGoseaparticularAinvolvingthestrongexistentialquanti er.Iu,LemmaT2_ L}'etBiTL[x;yQ]bequanti er{freeformulaswithout^,andA[x]:9y ~5CVhVtXTigBiTL[x;yQ]:Ǎ,Thenwec}'an ndaderivationof(8y::B1|s[x;yQ]!:::8!Bm[x;yQ]!?)^A[x]s. g\32\ܚRPr}'oof.qUILetUUy SbGeUUgivenandassume~vi :B^ ޴A;Z iandwD:?!A.UUW*emustshowA. aCaseu䍵i::BiforUUsomei.LetBidCci,!PiwithatomsPiTL.ThentD~eviВ:Cci AL!(Pid!A)!A'RandUUwehave&eij [u䍵i]:StabCij#jv[ٟ^:Cijc:u䍵iuccCi:Efq#qƴPi(v[uj6):Cij ;k0eiTL[u䍵i]:w:DPi;Zi <:u䍵iuccCiwi::Pi:RUsingUUdCij :Cij !C^A;Zij fromLemma1weobtainXQ~vvi(dCi1 pei1P):::(dCin1ieini p)(w:DPi;Zi <:Efq#qƴA!(eiTLwi)):A:?aCaseu䍳+i:BiforUUalli.Thenԉ%9+y 9hu䍳+1;:::;u+፴mi:AaNote@thattheassumptionwD:?O!A[x]@hasnotbGeenused.TheextractedRtermsUUforthisderivqationareedets Zy:;xm1 8;:::;xmmU;z:Rif碦:B1|tthen/x519dets፴C115@:::dets፴C1n1r0"2elseR:::Rif碦:Bmthen2x8/m?Kdets፴Cm1:::GOdets፴Cmnm0'elseRy' 60:::  ;'RwhereUUx gi f;z mareUUthelistsofvqariablesassoGciatedwith~vi :B^qA;Zi;wD.RTheoremT(F riedman).fF;oranyderivationuwd[u:8y::B1|s[x;yQ]!:::8!Bm[x;yQ]!?;v1|s:8C1;:::;vnq~:8Cn]:?RwithBiTL,Cjʓquanti er{fr}'eeandwithout^wec}'an ndaderivationndtr[v1|s:8C1;:::;vnq~:8Cn]:9y ~5CVhVtXTigBiTL[x;yQ]:҆RPr}'oof.qUILetUUA[x]:9^y ~5CVӈV(ߟi'BiTL[x;yQ]UUandconsidertheA[x]{translationʦdA[xų]s[u09;v[ٵ0፳1|s]:(?!A[x])!A[x]Rwherey[u09:z(8y::B1|s[x;yQ]!:::8!Bm[x;yQ]!?)A[x]s;v[ٵ0፳1|s:z(8C1|s)A[xų]s;:::v[ٵ0፴nq~:(8Cn)A[xų]]RofUUd,obtainedbyjustchangingsomeformulas.ByLemma1wehavedvi[viTL:8Ci]:(8Ci)A[xų]s: g\32\ܚ,ByLemma2(nowusingtheparticularchoiceofA[x])theA[x]{translationof ,theUUassumptionuisprovqablewithoutassumptions:yjdu:b:(8y::B1|s[x;yQ]!:::8!Bm[x;yQ]!?)A[x],SubstitutingUUdvi[viTL:8Ci]forv^[ٵ0;Ziandduforu^0#weobtain\dtr[v1|s:8C1;:::;vnq~:8Cn]:9y ~5CVӈVtidiӇBiTL[x;yQ];,where K\dtr dA[xų]s[du:b;dv1g";:::;dvn gn]Efq#qƴA[xų] @:;Having}obtainedaproGofd^tr ofanexistentialformula9^y ~5CVӈV(ߟi'BiTL[x;yQ]wecan,thenUUapplythegeneralmethoGdofextractingtermstothisproof.Ityields(dtr)ets Z(dA[xų]s)ets YB[dets፴u;dets፴v1;:::;dets፴vn]0;zX(1),3.3 Comparison,W*eMnowprovethatthevqalueoftheextractedtermswheninstanciatedwitha,listUUr gofUUclosedtermsisinfactthesameastheresultofthedirectmethoGd.;SoUUconsideragainthesituationofF*riedman'sTheorem,i.e.aderivqationOwd[u:8y::B1|s[x;yQ]!:::8!Bm[x;yQ]!?;v1|s:8C1;:::;vnq~:8Cn]:?,withBiTL,Cjcquanti er{freeandwithout^.W*ejustobservedthattheprogram,(d^tr)^ets extractedkfromthetranslatedderivqationhastheform(1)abGove.kLetus,trytounderstandhowthisprogramworks.First,(d^A[xų]s)^ets!Vcloselyfollowsthe,structureofd.Thereasonisthatd^A[xų]di ersfromdonlywithrespGecttothe,formulasaxed,andwhenformingtheextractedtermsthisa ectsonlythe,typGesvandthearitiesofthelistsofob8jectvqariablesassociatedwithassumption,vqariables.;InAordertocomprehendd^ets፴vi andd^ets፴uletushaveAasecondloGokattheproofsof Yፑ,Lemma1land2.Firstnotethatdvi[viTL:8Ci]:(8Ci)^A[xų]8islobtainedfromdiTL:Cid! ƍ,C:A[xų]Zi(constructedUUintheproGofofLemma1by0dvi ry:i :diTL(viyi A):,Sincelvi!hastypGe8CiTL,whichisaHarropformula,wehaved^ets፴vi GBy:i 9d^ets;Zi YB.Now,fromUUtheproGofofLemma1weobtainE)dets፴i Zxş1 8;:::;xmmU;z:ifLo:B1|tthen/x519dets፴C115@:::dets፴C1n1r0"2else:::ifLo:Bmthen2x8/m?Kdets፴Cm1:::GOdets፴Cmnm0'elsez ::: z;=(2),whereCi&{/B1N!:::O!Bm j!R ^withBi&{C eiF!PiIandx \i [;z arethelists,of}vqariablesassoGciatedwith~vi ;wD.F*urthermore,d^etsbCij!Faretheextractedtermsof %g\32\N`Rderivqations_dCij :Cij !C:A[xų]ZijconstructedbypreviousapplicationsofLemma1. RSimilarlyJedets፴u Zy:;xm1 8;:::;xmmU;z:Rif碦:B1|tthen/x519dets፴C115@:::dets፴C1n1r0"2elseR:::Rif碦:Bmthen2x8/m?Kdets፴Cm1:::GOdets፴Cmnm0'elseRy' 60:::  ;=(3)RwhereBi,$C &iR2!PiMHandx i _ ;z arethelistsofvqariablesassoGciatedwithZw~vi &,;wD. cRF*urthermore,"d^etsbCijCaretheextractedtermsofderivqationsdCij :Cij !C:A[xų]Zij!con- RstructedUUbypreviousapplicationsofLemma1. [aThisanalysismakesitpGossibletoprovethatthevqalueoftheextractedtermsRwhen|jinstanciatedwithalistr EofclosedtermsisinfactthesameastheresultRofthedirectmethoGdtoreado the rstinstanceprovidedbytheinstanciatedRderivqation\qxvd|r[u~:8y::B1|s[rq;yQ]!:::8!Bm[r;yQ]!?;v1|s:8C1;:::;vnq~:8Cn]:?faBelowUUwewillshowthefollowingRClaim.F*orUUanynormalderivqationw9e[u~:8y::B1|s[rq;yQ]!:::8!Bm[r;yQ]!?;v1|s:8C1;:::;vnq~:8Cn]:?RwithUUFV(e)=;UUwehave;jej=[UX[(eA[rq])ets YB[dets፴u[rq=x];dets፴v1;:::;dets፴vn]0]UX]:RW*e7thenobtainthattheinstanciationoftheextractedterms(1)withr dn(v1|sn)u(g[(n))(v2n):?:RNowUUlet *%tA:9m::ndn(v1|sn)u(g[(n))(v2n):?:,NowUUlet <%tA:9m::nF*romUUtheproGoftermTwKd=ux0|s(Indo~pX8v1(x;y[;w1ɍ~Dpd5xxݍ1 mw1ɍ~Dpd5yxݍ2 2:v2|sxy(uxw1)(uyw2)w1w2)x0)v3,weUUobtaintheprogram: (dtr)ets Z=dets፴u YBx0|s(Rdets፴v1(x;y[;w1w2:dets፴v2 YBxy[(dets፴uxw1)(dets፴uy[w2)w1w2)x0)dets፴v3,whered^ets፴u andthed^ets፴vistillhavetobGecalculated.Lookingatourassumptions ,u*andvivitisclearthatonlyg~p $Tisrelevqant.Hence,usingtherecipGegiveninthe,proGofUUofLemma2^,weobtainHUdets፴u Z=x;w:wDx and$wdets፴v1=dets፴v3=id o:,TheUUcalculationofd^ets፴v2 isalittlebitmoreinvolved.UUW*ehavehdets፴v2 Z=z1|s;z2;w1;zp:g[ٳets፵:pxz1(g[ٳets፵:pyQhz2(g[ٳetsፍ~pRx w1(g[ٳetsፍ~pRyw2zp))),ands@Yg[ٳets፵:pxR=z1|s;z2':if_px then*Pz1|telse*z2|t Ds@Yg[ٳets፵:py=z1|s;z2':if_py [then*)z1|telse*z2|t s@Yg[ٳetsፍ~pRx |3=g[ٳetsፍ~pRy=id o:,Hence2dets፴v2Do\=OFz1|s;z2;w1;w2;z?:YGifipx~wthenz1|telse*if;wspyOlthenpGz2|telse*w1|s(w2zp)  :,ThereforeUUwegetKt(dtr)ets Z=R$id$(x;y[;w1|sw2;zp:$ifnpxјthenw1|sx else$ifnpy$gthenw2|sy [else&w1(w2zp)  )$x0$x0|s:,ThisUUmeans(d^tr)^ets YB(x0|s)=g[(x0;x0)UUwherec44g[(";zp)=vzp;Pg[(hx;yi;zp)=vif,pxthenplg[(x;x) elsevif,pyvthenHg[(y;y) else&Eg(x;g(y;zp))  :=g\32\ܚRReferencesR1.^1CoAquand,T.:AьproofofHigman'slemmab9ystructuralinduction.Manuscript ^1(1993)R2.^1F:riedman,ZH.:Classicallyandin9tuitionisticallyprov|rablyrecursivefunctions.In:^1HigherTSetTheory:,SLNCS699(1978)21{28R3.^1Higman,G.:Orderingb9ydivisibilityinabstractalgebras.ProAc.LondonMath.Soc.^12T(1952)236{366R4.^1Kreisel,[G.:In9terpretationofanalysisbymeansofconstructivefunctionalsof nite^1t9ypAes.TIn:ConstructivityinMathematics,North{Holland,(1959)101{128R5.^1Murth9y:,1C.:ExtractingConstructiveContentfromClassicalProAofs.PhD1Ithesis.^1T:ec9hnicalMqRepAort,Nr.90{1151,Dep.ofComp.Science,CornellUniv,Ithaca,New^1Y:orkT(1990)R6.^1Nash-Williams,HC.:Onw9ell{quasi{ordering nitetrees.ProAc.CambridgePhil.SoAc.^159T(1963)833{835R7.^1Sc9hA;utte,:K.,Simpson,S.G:EininderreinenZahlentheorieunbAeweisbarerSatz;ubAer^1endlic9heTFolgennatA;urlicherZahlen.Arch.Math.Logik25(1985)75{89R8.^1Sc9hwichtenbAerg,H.:Proofsasprograms.In:ProofTheory:.Aselectionofpapers^1fromtheLeedsProAofTheoryProgramme1990,Cam9bridgeUniversityPress(1992)^181{113R9.^1T:roAelstra,%A.S.,v|ranDalen,D.:ConstructivisminMathematicsVol.1.AnIn9tro-^1duction.B4In:StudiesinLogicandtheF:oundationsofMathematics,North{Holland^1121T(1988)R10.bT:roAelstra,A.S.:MetamathematicalIn9vestigationsofIn9tuitionisticArithmeticand^1Analysis.TSLNM344(1973)mRThisTarticlew9asproAcessedusingtheLfQ- cmcsc10QavTuAdEXmacropack|ragewithLLNCSstyleJQ;g\ Q- cmcsc10NDF cmmib10Cu cmex107"Vff cmbx100N cmbx12"V cmbx10p0J cmsl10': cmti10!", cmsy10 b> cmmi10K`y cmr10t : cmbx9o cmr9 O!cmsy7 0ercmmi7ٓRcmr7O \cmmi5Zcmr5R