%!PS-Adobe-2.0 %%Creator: dvipsk 5.58f Copyright 1986, 1994 Radical Eye Software %%Title: bnsfin2.dvi %%Pages: 12 %%PageOrder: Ascend %%BoundingBox: 0 0 596 842 %%EndComments %DVIPSCommandLine: dvips bnsfin2.dvi %DVIPSParameters: dpi=300, compressed, comments removed %DVIPSSource: TeX output 1999.08.01:0851 %%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 (bnsfin2.dvi) @start /Fa 3 81 df<1320134013801201EA0300120212065AA2121C1218A212381230 A21270A4126012E0AE12601270A41230A212381218A2121C120CA27E12021203EA018012 00134013200B36798115>0 D<7E12407E12307E1208120C7EA212077EA213801201A213 C0A4120013E0AE13C01201A41380A212031300A25A1206A25A120812185A12205A5A0B36 7E8115>I80 D E /Fb 4 122 df<1304130C1318A31330A31360A313C0A3EA0180A3EA0300A31206A35AA35AA35AA35A A35AA20E257E9B13>61 D97 D117 D121 D E /Fc 6 117 df101 D<12E0A31200A612E0AF03187E9708>105 D<38E7E1F838EFF3FC38F87E1E38F03C0EEAE038AB170F7E8E1C>109 D113 D<121FEA7FC012E01300A27E127FEA3F80EA0FC0EA01E0128012C0EAE1C012 7FEA1F000B0F7F8E0E>115 D<1238A4EAFFC0A2EA3800AA1340EA1FC013000A137F920D> I E /Fd 3 84 df<14101438A3147CA314BEA3EB011FA39038020F80A201047F1407A201 087F1403A2496C7EA3496C7EA390387FFFFCA29038C0007E49133EA248C7123F81A20002 EC0F80A21206ED07C0001FEC0FE0D8FFE0EBFFFEA2272A7EA92C>65 D82 DI E /Fe 6 111 df33 D<1204120C1200A5123012581298A21230A212601264A21268123006127E91 0B>105 D<1320A21300A5EA0380EA04C01208A21200EA0180A4EA0300A4124612CC1278 0B1780910D>I<123C120CA25AA31370EA3190EA3230EA34001238127FEA61801390A2EA C1A0EAC0C00C117E9010>I<3871F1F0389A1A18EA9C1CEA9818121838303030A2143214 62386060641438170B7E8A1B>109 DI E /Ff 1 41 df<1507ED1FC0ED38E0ED6030EDC018B6FCA2 C8FCED6030ED38E0ED1FC0ED0700250C7D8E2B>40 D E /Fg 1 34 df<4A7EA26E7EA21560A2818181B71280A2C8EA0C005D5D5DA25DA24A5AA221147E9226> 33 D E /Fh 4 51 df<13C0A9B51280A23800C000A911147E8F17>43 D<121FEA3180EA60C0EA4040EAC060A8EA4040EA60C0EA3180EA1F000B107F8F0F>48 D<1218127812981218AC12FF08107D8F0F>I<121FEA6180EA40C0EA806012C01200A213 C0EA0180EA030012065AEA10201220EA7FC012FF0B107F8F0F>I E /Fi 9 116 df70 D79 D84 D<00F0EB01E0A2007814C01403A26CEB0780A36CEB0F00A36C131EA21380 00075BA23803C0381478A23801E07014F0A26C6C5A13F1A2EB71C0137BEB3B80A2133F6D C7FCA21B207F9F1E>86 D<137EEA01FE1203EA078013005AA7EAFFF0A3EA0F00B10F2080 9F0E>102 D110 D<3803E3C0EA0FFBEA1FFFEA3F0FEA3C07EA7803A212F0A61278A2EA7C07EA3F0FEA1FFF EA0FFBEA03E3EA0003A9121D7F9317>113 DII E /Fj 54 128 df<90387E1F803901C17040390703C0600006EB80E0000E14401500A5B6 12E0380E0380AE397F8FE3FC1E1A809920>14 D34 D<126012F0A212701210A31220A21240A2040B 7D830B>44 DI<126012F0A2126004047D830B>I48 D<12035AB4FC1207B3A2EA7FF80D187D9713>I<1318A21338137813F8 13B8EA01381202A212041208121812101220124012C0B5FCEA0038A6EA03FF10187F9713 >52 DII56 DI<126012F0A212601200A8126012F0A2126004107D8F0B>I<130CA3131EA2 132F1327A2EB4380A3EB81C0A200017F1300A248B47E38020070A2487FA3487FA2003C13 1EB4EBFFC01A1A7F991D>65 D68 D70 DI73 D<39FFE01FC0390E000F00140C14085C5C5C495A0102C7FC5B130C131C13 2E1347EB8380EA0F03380E01C06D7EA2147080A280141E141F39FFE07FC01A1A7F991E> 75 DII80 D82 DI<007FB5FC38701C0700401301A200C014800080 1300A300001400B13803FFE0191A7F991C>I<39FFE07FC0390E000E001404B200065B12 076C5B6C6C5A3800E0C0013FC7FC1A1A7F991D>I<3AFF81FF07F03A3C007801C0001CEC 0080A36C90389C0100A33907010E02A33903830F04EB8207A2150C3901C40388A33900E8 01D0A390387000E0A301305B01201340241A7F9927>87 D<12FEA212C0B3AF12FEA20725 7D9B0B>91 DI<12 FEA21206B3AF12FEA20725809B0B>I97 D<12FC121CA913FCEA1D0738 1E0380381C01C0130014E0A6EB01C01480381E0300EA1906EA10F8131A809915>II<133F13 07A9EA03E7EA0C17EA180F487E127012E0A6126012706C5AEA1C373807C7E0131A7F9915 >IIII<12FC121CA913 7CEA1D87381E0380A2121CAB38FF9FF0141A809915>I<1218123CA212181200A612FC12 1CAE12FF081A80990A>I<12FC121CA9EB1FC0EB0F00130C5B13205B13E0121DEA1E70EA 1C7813387F131E7F148038FF9FE0131A809914>107 D<12FC121CB3A6EAFF80091A8099 0A>I<38FC7C1F391D8E6380391E0781C0A2001C1301AB39FF9FE7F81D107F8F20>IIII114 DI<1208A41218A21238EAFFC0EA3800A81320A41218EA1C40 EA07800B177F960F>I<38FC1F80EA1C03AB1307120CEA0E0B3803F3F01410808F15>I<38 FF0F80383C0700EA1C061304A26C5AA26C5AA3EA03A0A2EA01C0A36C5A11107F8F14>I< 39FE7F1F8039381C0700003C1306381C0C04130E380E16081317A238072310149013A338 03C1A014E0380180C0A319107F8F1C>I<38FE3F80383C1E00EA1C086C5AEA0F306C5A6C 5A12017F1203EA0270487E1208EA181CEA381E38FC3FC012107F8F14>I<38FF0F80383C 0700EA1C061304A26C5AA26C5AA3EA03A0A2EA01C0A36C5AA248C7FCA212E112E212E412 7811177F8F14>I127 D E /Fk 4 122 df<120CA2EACCC012ED EA7F80EA0C00EA7F80EAEDC012CCEA0C00A20A0B7D8B10>3 D<1208121CA21238A31230 1270A21260A212C0A2060D7E8D09>48 D<12C0B3A702197C9209>106 D<1218A512FFA21218AF08167D900E>121 D E /Fl 9 53 df<126012F0A51260A91200 A4126012F0A2126004177D960A>33 D<120112021204120C1218A21230A212701260A312 E0AA1260A312701230A21218A2120C12041202120108227D980E>40 D<12801240122012301218A2120CA2120E1206A31207AA1206A3120E120CA21218A21230 12201240128008227E980E>I<1330ABB512FCA238003000AB16187E931B>43 D48 D<1206120E12FE120EB1EAFFE00B157D9412>III<1330 A2137013F012011370120212041208121812101220124012C0EAFFFEEA0070A5EA03FE0F 157F9412>I E /Fm 36 122 df12 D<1330136013C0EA01801203EA07005A120E121E121C123CA212381278A412F85AA97E12 78A41238123CA2121C121E120E120F7EEA03801201EA00C0136013300C2D7CA114>40 D<12C012607E7E121C7E120F7E1380120313C0A2120113E0A413F01200A9120113E0A413 C01203A21380120713005A120E5A12185A5A5A0C2D7DA114>I 45 D<1238127C12FEA3127C123807077C860F>I48 D<137013F0120712FF12F91201B3A4387FFFC0A2121D7D9C1A>I III<001C13E0EA1FFF14C01480140013FC13C00018C7FCA4EA19FE381FFF80381E07 C0381803E0381001F0120014F8A2127812FCA314F0EA7803007013E0383C0FC0380FFF00 EA03FC151D7E9C1A>I66 D<903807FC0290383FFF0E9038FE03DE3903F000FE4848133E48 48131E485A48C7120EA2481406127EA200FE1400A7127E1506127F7E150C6C7E6C6C1318 6C6C13386C6C13703900FE01C090383FFF80903807FC001F1F7D9E26>III 76 D78 D<3803FC08380FFF38381E03F8EA3800481378143812 F01418A26C13007EEA7FC013FE383FFF806C13C06C13E06C13F0C613F81307EB00FC147C 143C12C0A36C1338147800F8137038FE01E038EFFFC000811300161F7D9E1D>83 D<007FB512FCA2397C07E07C0070141C0060140CA200E0140E00C01406A400001400B100 03B512C0A21F1E7E9D24>I97 D99 DI< EA01FE3807FF80380F83C0381E01E0383E00F05A14F812FCB5FCA200FCC7FCA3127CA26C 1318121E380F80703807FFE0C6138015147F9318>I<3803FC3C380FFFFE381E079E383C 03DE007C13E0A5003C13C0381E0780381FFF00EA13FC0030C7FCA21238383FFF806C13F0 6C13F84813FC3878007C0070133E00F0131EA30078133CA2383F01F8380FFFE000011300 171E7F931A>103 DI<121C123E127FA3123E121CC7FCA6B4FCA2121FB0EAFFE0A20B217EA0 0E>I108 D<3AFE0FE03F8090391FF07FC03A1E 70F9C3E09039407D01F0EB807E121FEB007CAC3AFFE3FF8FFEA227147D932C>I<38FE0F C0EB3FE0381E61F0EBC0F81380EA1F00AD38FFE7FFA218147D931D>I<48B4FC000713C0 381F83F0383E00F8A248137CA200FC137EA6007C137CA26C13F8A2381F83F03807FFC000 01130017147F931A>I<38FF1FC0EB7FF0381FE1F8EB80FCEB007EA2143E143FA6143E14 7E147CEB80FCEBC1F8EB7FE0EB1F8090C7FCA7EAFFE0A2181D7E931D>I114 DI<1203A45AA25AA2123FEA FFFCA2EA1F00AA1306A5EA0F8CEA07F8EA03F00F1D7F9C14>I<38FF07F8A2EA1F00AD13 01A2EA0F063807FCFF6C5A18147D931D>I<39FFE07F80A2391F001C00380F8018A26C6C 5AA26C6C5AA2EBF0E000015B13F900005B13FF6DC7FCA2133EA2131CA21318A2EA783012 FC5BEAC0E0EAE1C0EA7F80001EC8FC191D7F931C>121 D E /Fn 23 127 df<12081218A31230A31260A2126112C112C212441278080E7E8D0C>19 DI<3803FF805A381C3000EA181812301260A3485AA2EA4060EA6040EA2180001E C7FC110E7F8D14>27 DI<001013204813305AA2388020201360A21460EB4040EBC0C03881C18038E76700 EA7E7EEA3C3C140E7F8D16>33 D<3810078038200FC038401860EB3020EA80201340A2EB 8040A2148038610300EA390EEA1FFCEA07F06CC7FC1202A21206A2120413147E8D17>39 D<126012F0A212701210A21220A21240A2040A7D830A>59 D<0007B512803800E003EC01 00A3EA01C0A21440A248485A138113FF1381D80701C7FCA390C8FC120EA45AEAFFC01917 7F9616>70 D<130E13131337133613301360A4EA03FCEA00C0A5EA0180A5EA0300A41202 126612E65A1278101D7E9611>102 D<13E2EA031EEA060E120C130C1218A3EA1018A3EA 1838EA08F0EA07301200A2EA606012E0EAC1C0EA7F000F14808D11>I<121F1206A45AA4 EA18F0EA1B18EA1C081218EA38181230A3EA6030133113611362EAC026133810177E9614 >I<120313801300C7FCA6121C12241246A25A120C5AA31231A21232A2121C09177F960C> I<1318133813101300A6EA01C0EA0220EA0430A2EA08601200A313C0A4EA0180A4EA6300 12E312C612780D1D80960E>I<121F1206A45AA4EA181C1366138EEA190CEA3200123C12 3FEA3180EA60C013C4A3EAC0C813700F177E9612>I<123E120CA41218A41230A41260A4 12C012C8A312D0127007177E960B>I<38383C1E3844C6633847028138460301388E0703 EA0C06A338180C061520140C154039301804C0EC07001B0E7F8D1F>II114 DI<1203 A21206A4EAFFC0EA0C00A35AA45A1380A2EA31001232121C0A147F930D>I 120 D122 D<13201330A2EAFFFCA2EA007013E013400E08799712> 126 D E /Fo 46 122 df12 D<91393FC0FF809139E0E38040903A0181E600E00103EBEC01EC80DC903A07001C00C003 1813001538A2130EA25D90B7128090390E007003EE07005BA215E0160EA25BA24A485AA3 01701540EE3880EC0380A301E0EC1900ED000E4A90C7FC13C0140612013831860E38798F 0C38F31E1838620C30383C07C02B29829F28>14 D<121C123E127EA2123A12021204A212 08A21210122012401280070E769F0E>39 D<121C123CA41204A21208A212101220A21240 1280060E7D840E>44 DI<127012F8A212F012E00505 7B840E>I<3804E010EA0BF0000F1320001F1340381E19C038380E80EA30013860030012 40EA8006EA000E130C131C131813385BA213F05B1201A2485AA3485AA3120F90C7FCA212 06141F799D17>55 D<131FEB7180EBC0C0EA0180000313E0EA07005A1301121EA314C0EA 1C03A31307EB0F80120CEA06373803C700EA000F130EA25B1260EAF0385BEAE060EA80C0 EA4380003EC7FC131F7B9D17>57 D<1207120F121FA2120E1200AA127012F8A212F012E0 08147B930E>I<14021406A2140E141EA2143F142F144F14CF148FEB010FA21302A21304 1308A20110138014071320EB3FFFEB40071380A2EA0100A2120212061204001E14C039FF 807FF81D207E9F22>65 D67 D<90B5128090381E00E015701538151C5B 150EA35BA449131EA44848133CA3157848481370A215E0EC01C0380780031580EC0E005C 380F0070B512C01F1F7D9E22>I<48B512FE39001E001C150C1504A25BA4903878040815 00A2140C495AEBFFF8EBF018A23801E010A3EC001048481320A21540A248481380140115 001407380F001FB512FE1F1F7D9E1F>I<48B512FC39001E003815181508A25BA4491310 EC0800A3495A1430EBFFF0EBF0303801E020A44848C7FCA4485AA4120FEAFFF81E1F7D9E 1E>II<3801FFF038001F00131EA35BA45BA45BA4 485AA4485AA4485AA4120FEAFFF0141F7D9E12>73 D<90380FFF809038007C001478A35C A4495AA4495AA4495AA449C7FCA212301278EAF81EA2485AEA8038EA40706C5AEA1F8019 207D9E18>I<3801FFF8D8001FC7FC131EA35BA45BA45BA4485AA315803903C00100A25C 140238078006A25C141C380F0078B512F8191F7D9E1D>76 DI<48B5128039001E00E015701538153C5BA4491378 A215F015E09038F003C0EC0F00EBFFFC01F0C7FC485AA4485AA4485AA4120FEAFFF01E1F 7D9E1F>80 D<90B5FC90381E03C0EC00E0157015785BA44913F0A2EC01E015C09038F007 00141EEBFFF0EBF01C48487E140F8015803903C00F00A43807801E1508A21510000F130E D8FFF01320C7EA03C01D207D9E21>82 D<903807E04090381C18C09038300580EB600313 C000011301018013001203A391C7FC7FA213F86CB47E14E06C6C7E131FEB01F8EB0078A2 1438A21220A2143000601370146014E000705B38E80380D8C606C7FCEA81F81A217D9F1A >I<000FB512FC391E03C03800181418001014081220EB078012601240A239800F001000 001400A3131EA45BA45BA45BA41201387FFF801E1F799E21>I97 DI<137EEA 01C138030080EA0E07121E001C1300EA3C0248C7FCA35AA5EA70011302EA3004EA1838EA 07C011147C9315>I<1478EB03F8EB0070A414E0A4EB01C0A213F1EA038938070780EA0E 03121C123C383807001278A3EAF00EA31420EB1C40A2EA703C135C38308C80380F070015 207C9F17>I<137CEA01C2EA0701120E121C123CEA3802EA780CEA7BF0EA7C0012F0A412 7013011302EA3804EA1838EA07C010147C9315>I<1478EB019CEB033CA2EB07181400A2 130EA5EBFFE0EB1C00A45BA55BA55BA5485AA35B1231007BC7FC12F31266123C1629829F 0E>III<13 C0EA01E0A213C0C7FCA7120E12131223EA4380EA4700A21287120EA35AA3EA38401380A2 1270EA31001232121C0B1F7C9E0E>I108 D<391C0F80F0392630C318394740640C90 3880680EEB0070A2008E495A120EA34848485AA3ED70803A3803807100A215E115623970 070064D83003133821147C9325>I<381C0F80382630C0384740601380EB0070A2008E13 E0120EA3381C01C0A3EB038400381388A2EB0708EB031000701330383001C016147C931A >I<137CEA01C338030180000E13C0121E001C13E0123C1278A338F003C0A3EB07801400 EA700F130EEA3018EA1870EA07C013147C9317>I<3801C1E0380262183804741C1378EB 701EA2EA08E01200A33801C03CA3143838038078147014E0EBC1C038072380EB1E0090C7 FCA2120EA45AA2B47E171D809317>III<13FCEA0302EA0601EA0C03130713061300EA0F8013F0EA07F8EA03FCEA00 3E130E1270EAF00CA2EAE008EA4010EA2060EA1F8010147D9313>II<000E13C0001313E0382301C0EA4381EA4701A238870380120EA3381C0700A31410 EB0E201218A2381C1E40EA0C263807C38014147C9318>I<380E0380EA1307002313C0EA 4383EA4701130000871380120EA3381C0100A31302A25BA25BEA0E30EA03C012147C9315 >I<000EEBC1C0001313E3392301C3E0384381C1384701C015603987038040120EA3391C 070080A3EC0100A21306EB0F02000C5B380E13083803E1F01B147C931E>I<3803838038 0CC440381068E013711220EB70C03840E0001200A3485AA314403863808012F3EB810012 E5EA84C6EA787813147D9315>I<000E13C0001313E0382301C0EA4381EA4701A2388703 80120EA3381C0700A4130E1218A2EA1C1EEA0C3CEA07DCEA001CA25B12F05BEAE060485A EA4380003EC7FC131D7C9316>I E /Fp 20 107 df0 D<127012F8A3127005057C8D0D>I8 D10 D<90383FFFC090B5FCD803C0C7FC48 C8FC120C5A5AA25AA25AA81260A27EA27E7E1207EA03C0C6B512C0133F90C8FCA8007FB5 12C0A21A267C9C23>18 D<15C01403EC0F00141C1470495AEB0780011EC7FC1378EA01E0 EA0380000EC8FC123C12F0A2123C120EEA0380EA01E0EA0078131EEB0780EB01E0EB0070 141C140FEC03C014001500A8007FB51280B612C01A267C9C23>20 D<12C012F0123C120EEA0380EA01E0EA0078131EEB0780EB01E0EB0070141C140FEC03C0 A2EC0F00141C1470495AEB0780011EC7FC1378EA01E0EA0380000EC8FC123C127012C0C9 FCA8007FB51280B612C01A267C9C23>I<1506A381A216801501ED00C0166016701618B8 FCA2C912181670166016C0ED018015031600A21506A328187E962D>33 D<1360B3AA00C0133000F013F0383861C0380E6700EA076EEA036CEA01F86C5AA21360A3 132014297F9F17>35 D50 D<140CA21418A21430A21460A214C0A2EB0180A3EB0300A21306A25BA25BA25BA25BA25B A2485AA248C7FCA21206A35AA25AA25AA25AA25A1240162C7AA000>54 D<12C0A712E0A212C0A703107E9200>I<90383FFFE048B512F839071E01FE0008EB007F 0018141F007080A212C0D8001C130EA2013C131E151C151801385B5D017813800207C7FC EB70FCEB71F8EBF0FCEBE07C801201497EA200036D13100180EB806016E00007903807C1 800100EBE3000006EB03FE48EB01F024207F9E27>82 D<124012C0B3B3A7EAFFC0127F0A 2E79A114>98 D<134013C0B3B3A712FFA20A2E7EA114>III<130F1338136013E0EA01C0 AFEA0380EA0700121E12F8121E1207EA0380EA01C0AFEA00E013601338130F102D7DA117 >I<12F8121E1207EA0380EA01C0AFEA00E013601338130F1338136013E0EA01C0AFEA03 80EA0700121E12F8102D7DA117>I<12C0B3B3A9022D7BA10D>106 D E /Fq 47 127 df<14F8EB03061304EB080313101320EB4007A2138014063801000E14 0CEB07F8EB0470380207D8EB001CA2141E5AA448133CA3147800181370001413F014E038 1201C038218700EA207C90C7FCA25AA45AA318297F9F1A>12 D<381E07C038231860EBA0 30EA43C0EB8038A2388700701207A3000E13E0A4381C01C0A43838038012181200A2EB07 00A4130EA3130C151E7E9317>17 D<12061207120EA45AA35AA4EA7010132012E01340EA 6080EA6300123C0C147E9310>19 D<00061370380701F8380E02F0EB0C60EB10005B485A 5B001FC7FC13F8EA381E1307A2EB038438700708A3EB031012E0386001E016147E931A> I<1207EA01C07F12007F1370A213781338A2133C131CA2131E130EA2130F7F131FEB3780 136313C3380183C0EA0381EA0701000E13E0EA1C005A48137012F048137848133815207D 9F1B>I<38018018EBC01C38038038A438070070A4000E13E0A314E1381E01C2A21303EB 05C4EA3F083839F0780038C7FCA25AA45AA35A181E7F931B>I<380FFFFC4813FE4813FC 3860820012C01281EA010613041203A21202EA060C130E120CA2121CA2EA180FEA3807EA 300617147E931A>25 D27 D<380FFFF05A5A3860400012C0EA80C012005B1201A4120390C7FCA25AA3120E12061414 7E9314>I<0004131E48137F48EBFF80903801C1C03820030001021340EA400613045BA2 00C0C7128013100040EB01005C386020060038131C001F13F8380FFFE06C5BC648C7FC13 C0A31201A25BA21203A290C8FC1A1E7E931E>39 D<127012F8A3127005057C840D>58 D<127012F012F8A212781208A31210A31220A21240050E7C840D>I<15C01403EC0F0014 1C1470495AEB0780011EC7FC1378EA01E0EA0380000EC8FC123C12F0A2123C120EEA0380 EA01E0EA0078131EEB0780EB01E0EB0070141C140FEC03C014001A1C7C9823>I<144014 C0EB0180A3EB0300A31306A25BA35BA35BA25BA35BA3485AA348C7FCA21206A35AA35AA2 5AA35AA35AA2122D7EA117>I<12C012F0123C120EEA0380EA01E0EA0078131EEB0780EB 01E0EB0070141C140FEC03C0A2EC0F00141C1470495AEB0780011EC7FC1378EA01E0EA03 80000EC8FC123C12F012C01A1C7C9823>I<48B6FC39001E001E1506A215025BA4491304 EC0200A3495A140CEBFFFCEBF00C3801E008A44848C7FCA4485AA4120FEAFFFC201F7E9E 1D>70 D<3801FFF038001F00131EA35BA45BA45BA4485AA4485AA4485AA4120FEAFFF014 1F7E9E14>73 D<48B4EB1FF8D8001FEB03C091388001001317A2903823C002A2EB21E0A2 903841F0041340A2147801805B147C143CA248486C5AA2140FA2000214A01407A2EC03E0 485CA21401120C001E6D5AEAFFC0251F7E9E25>78 D<000FB512FC391E03C03800181418 001014081220EB078012601240A239800F001000001400A3131EA45BA45BA45BA4120138 7FFFC01E1F7F9E1B>84 D<397FFC07FE3907C000F0491340A348C71280A4001EEB0100A4 481302A4485BA4485BA35C00705BA25C6C5BD81803C7FCEA0E0CEA03F01F207D9E1F>I< 39FFF001FF390F80007890C712301520154015807F0007EB01005C14025CA25C6D5AA200 035B146014405CA201C1C7FC13E2120113E413E8A213F0A25B5B12005B20207E9E1B>I< 9039FFF01FF890390FC007809138800600010713046E5A5D01035B6E5A010113C0ECF180 02F3C7FCEB00F214FC1478147CA314BEEB011EEB021F1304EB0C0F01187FEB100701207F 1340EB8003D801007F00071301001F497E39FFC01FFE251F7F9E26>88 D97 DI<137CEA01C338070080EA0E07121E001C1300EA3C0248C7FCA35AA5EA 70011302EA3004EA1838EA0FC011147E9314>I<137CEA0182EA0701120E121C123CEA38 02EA780CEA7BF0EA7C0012F0A4127013011302EA3004EA1838EA0FC010147E9315>101 D<147C14CEEB019E1303140CEB0700A4130EA3EBFFF0EB0E00A25BA55BA55BA55BA45B12 01EA3180127948C7FC1262123C17297E9F16>III<13E01201A2EA00C01300A7120E1213EA2380 1243A3EA87001207A2120EA25AA21320EA3840A31380EA1900120E0B1F7E9E10>I<14C0 EB01E0A214C090C7FCA7131E1323EB43801383EA0103A2380207001200A3130EA45BA45B A45BA21230EA78E0EAF1C0EA6380003EC7FC1328819E13>III<391E07C07C 39231861869038A032033843C034D980381380A23A87007007001207A3000EEBE00EA3ED 1C10261C01C01320153816401518263803801380D81801EB0F0024147E9328>I<381E07 80382318C0EBA0603843C0701380A2388700E01207A3380E01C0A3EB0382001C1384EB07 041408130300381310381801E017147E931B>I<3803C1E038046218EB741CEA0878EB70 1EA2EA10E01200A33801C03CA3143838038078147014E0EBC1C038072380EB1E0090C7FC A2120EA45AA2EAFFC0171D819317>112 DII<13FCEA030338060080EA0C0113031400000EC7FCEA0F8013F86C7EEA01 FEEA001F13071270EAF006A2EAE004EA4008EA2030EA1FC011147E9315>II<000F136038118070002113E013C01241EA4380388381C0EA0701A3380E 0380A31484EB0708120CA2380E0F10EA06133803E1E016147E931A>I<381E01C0EA2303 14E0EA438113000047136000871340120EA3481380A3EB0100A213025B120CEA0E18EA03 E013147E9316>I<000FEB607039118070F00021EBE0F801C0137800411438D843801318 398381C010EA0701A3390E038020A31540A2158013070006EB8100380709C23801F07C1D 147E9321>I<3803C1C0380C622038103470EB38F012201460384070001200A35BA31420 3861C04012F1148012E238446300EA383C14147E931A>I<001E13600023137014E0EA43 8013001247388701C0120EA3381C0380A4EB07001218121C5BEA0C3EEA03CEEA000EA25B EAF0181338485AEAC060EA41C0003FC7FC141D7E9316>I<3801C0203803F0403807F8C0 380C1F8038080100EA00025B5B5B13605B48C7FC120248138038080100485AEA3F06EA63 FEEA40FCEA807013147E9315>I126 D E /Fr 81 128 df<90381F83E09038F06E303901C07878380380F89038 00F03048EB7000A7B612803907007000B2383FE3FF1D20809F1B>11 D<133FEBE0C0EA01C0380381E0EA0701A290C7FCA6B512E0EA0700B2383FC3FC1620809F 19>I<90381F81F89038F04F043901C07C06390380F80FEB00F05A0270C7FCA6B7FC3907 007007B23A3FE3FE3FE02320809F26>14 D<127012F8A71270AA1220A51200A5127012F8 A3127005217CA00D>33 DI<9038018030A349485AA501065BA549485AA2B71280A226 001803C7FCEB3006A6495AB71280A22600C018C7FC48485AA548485AA500065BA321297E 9F26>I<127012F812FCA212741204A31208A21210A212201240060E7C9F0D>39 D<13401380EA01005A12061204120C5AA212381230A212701260A412E0AC1260A4127012 30A212381218A27E120412067E7EEA008013400A2E7BA112>I<7E12407E12307E120812 0C7EA212077EA213801201A413C0AC1380A412031300A25A1206A25A120812185A12205A 5A0A2E7EA112>I<1303AFB612FCA2D80003C7FCAF1E207E9A23>43 D<127012F012F8A212781208A31210A31220A21240050E7C840D>II<127012F8A3127005057C840D>I<144014C0EB0180A3EB0300A31306A25BA35BA35B A25BA35BA3485AA348C7FCA21206A35AA35AA25AA35AA35AA2122D7EA117>II<13801203120F12F31203B3A6EA07C0EAFFFE0F1E7C9D 17>III<1306A2130EA2131E132EA2134E138EA2EA010E1202A212041208 A212101220A2124012C0B512F038000E00A7EBFFE0141E7F9D17>II<137CEA0182EA0701380E0380 EA0C0712183838030090C7FC12781270A2EAF1F0EAF21CEAF406EAF807EB0380A200F013 C0A51270A214801238EB07001218EA0C0E6C5AEA01F0121F7E9D17>I<1240387FFFE014 C0A23840008038800100A21302485AA25B5BA25BA21360A213E05B1201A41203A76C5A13 1F7E9D17>III<127012F8A312701200AA127012F8A3 127005147C930D>I<127012F8A312701200AA127012F012F8A212781208A31210A31220 A21240051D7C930D>I61 D<5B497EA3497EA3EB09E0A3EB10F0A3EB2078A3497EA2EBC03EEB801EA248B5FCEB000F A20002EB0780A348EB03C0A2120C001E14E039FF801FFE1F207F9F22>65 DI<90380FE0109038381C30 9038E002703803C00139078000F048C71270121E15305A1510127C127800F81400A91278 007C1410123CA26C1420A27E6C6C13406C6C13803900E00300EB380CEB0FF01C217E9F21 >IIII<90380FE01090 38381C309038E002703803C00139078000F048C71270121E15305A1510127C127800F814 00A7EC3FFEEC01F000781300127C123CA27EA27E6C7E3903C001703900E002309038380C 1090380FF0001F217E9F24>I<39FFF07FF8390F000780AD90B5FCEB0007AF39FFF07FF8 1D1F7E9E22>II<3807FFC038003E00131EB3A3 122012F8A3EAF01CEA403CEA6038EA1070EA0FC012207F9E17>I<39FFF007FC390F0003 E0EC0180150014025C5C5C5C5C5C49C7FC5B497E130FEB13C0EB21E01341EB80F0EB0078 A28080A280EC0780A2EC03C015E015F039FFF01FFE1F1F7E9E23>IIIIII82 D<3803F040380C0CC0EA1803EA3001EA6000A2 12E01440A36C13007E127CEA7F80EA3FF86CB4FC00071380C613C0EB1FE013031301EB00 F014707EA46C136014E06C13C038F8018038C60300EA81FC14217E9F19>I<007FB512E0 38780F010060EB006000401420A200C0143000801410A400001400B3497E3803FFFC1C1F 7E9E21>I<39FFF00FF8390F0003E0EC0080B3A46CEB01001380120314026C6C5A6C6C5A EB3830EB0FC01D207E9E22>I<39FFF003FE391F8000F86CC7126015206C6C1340A36C6C 1380A2EBE00100011400A23800F002A213F8EB7804A26D5AA36D5AA2131F6D5AA2EB07C0 A36D5AA36DC7FC1F207F9E22>I<3BFFF07FF81FF03B1F000FC007C06C90390780018017 0015C001805C00071502EC09E013C000035DEC19F01410D801E05CA2EC2078D800F05CA2 EC403C01785CA2EC801E017C1460013C144090383D000F133F6D5CA2011E1307010E91C7 FCA2010C7F010413022C207F9E2F>I<39FFF001FF391F800078000F146012076D134000 0314807F3901F001001200EBF802EB7C06EB3C04EB3E08131EEB1F10EB0FB0EB07A014E0 6D5AACEB3FFC201F7F9E22>89 D<12FFA212C0B3B3A512FFA2082D7CA10D>91 DI<12FFA21203B3B3A512FFA2082D80A10D>I 97 D<121C12FC121CAA137CEA1D87381E0180EB00C0001C13E01470A21478A6147014F0 14E0001E13C0381A018038198700EA107C15207E9F19>II< EB01C0130F1301AAEA01F1EA070DEA0C03EA180112381278127012F0A61270A21238EA18 03120CEA070D3801F1F815207F9F19>II<137CEA01C6 EA030F1207EA0E061300A7EAFFF0EA0E00B2EA7FE01020809F0E>I<14E03803E330EA0E 3CEA1C1C38380E00EA780FA5EA380E6C5AEA1E38EA33E00020C7FCA21230A2EA3FFE381F FF8014C0383001E038600070481330A4006013606C13C0381C03803803FC00141F7F9417 >I<121C12FC121CAA137C1386EA1D03001E1380A2121CAE38FF8FF014207E9F19>I<1238 127CA31238C7FCA6121C12FC121CB1EAFF80091F7F9E0C>I<13E0EA01F0A3EA00E01300 A61370EA07F012001370B3A31260EAF06013C0EA6180EA3F000C28829E0E>I<121C12FC 121CAAEB1FE0EB0780EB060013045B5B5B136013E0EA1DF0EA1E70EA1C38133C131C7F13 0F7F148014C038FF9FF014207E9F18>I<121C12FC121CB3ABEAFF8009207F9F0C>I<391C 3E03E039FCC30C30391D039038391E01E01CA2001C13C0AE3AFF8FF8FF8021147E9326> IIII<3801F0403807 0CC0EA0E02EA1C03EA38011278127012F0A6127012781238EA1C03EA0C05EA0709EA01F1 EA0001A8EB0FF8151D7F9318>III<1202A31206A2120EA2123EEA FFF8EA0E00AB1304A5EA07081203EA01F00E1C7F9B12>I<381C0380EAFC1FEA1C03AE13 07120CEA061B3803E3F014147E9319>I<38FF83F8383E00E0001C13C06C1380A3380701 00A21383EA0382A2EA01C4A213E4EA00E8A21370A3132015147F9318>I<39FF9FE1FC39 3C078070391C030060EC8020000E1440A214C0D80704138014E0A239038861001471A238 01D032143A143E3800E01CA2EB6018EB40081E147F9321>I<38FF87F8381E03C0380E01 80EB0300EA0702EA0384EA01C813D8EA00F01370137813F8139CEA010E1202EA06073804 0380000C13C0003C13E038FE07FC16147F9318>I<38FF83F8383E00E0001C13C06C1380 A338070100A21383EA0382A2EA01C4A213E4EA00E8A21370A31320A25BA3EAF080A200F1 C7FC1262123C151D7F9318>III127 D E /Fs 27 122 df45 D<130E131E137EEA07FE12FFA212F81200B3ABB5 12FEA317277BA622>49 DII<14 0FA25C5C5C5C5BA2EB03BFEB073F130E131C133C1338137013E0EA01C0EA038012071300 120E5A5A5A12F0B612F8A3C7EA7F00A890381FFFF8A31D277EA622>I<00181303381F80 1FEBFFFE5C5C5C14C091C7FC001CC8FCA7EB7FC0381DFFF8381F80FC381E003F1208C7EA 1F8015C0A215E0A21218127C12FEA315C05A0078EB3F80A26CEB7F00381F01FE6CB45A00 0313F0C613801B277DA622>I73 D80 D82 D<007FB71280A39039807F807FD87C00140F00781507A20070150300F016C0 A2481501A5C791C7FCB3A490B612C0A32A287EA72F>84 D<3803FF80000F13F0381F01FC 383F80FE147F801580EA1F00C7FCA4EB3FFF3801FC3FEA0FE0EA1F80EA3F00127E5AA414 5F007E13DF393F839FFC381FFE0F3803FC031E1B7E9A21>97 DIIIII<1207EA0F80EA1FC0EA3FE0A3EA1FC0EA0F80EA0700C7 FCA7EAFFE0A3120FB3A3EAFFFEA30F2B7EAA12>105 D108 D<26FFC07FEB1FC0903AC1FFC07FF0903AC307E0C1F8D80FC49038F101 FC9039C803F20001D801FE7F01D05BA201E05BB03CFFFE3FFF8FFFE0A3331B7D9A38>I< 38FFC07E9038C1FF809038C30FC0D80FC413E0EBC80701D813F013D0A213E0B039FFFE3F FFA3201B7D9A25>II<38FFE1FE9038EFFF809038FE0FE0390FF803F09038 F001F801E013FC140015FEA2157FA8157E15FEA215FC140101F013F89038F807F09038FC 0FE09038EFFF809038E1FC0001E0C7FCA9EAFFFEA320277E9A25>I<38FFC1F0EBC7FCEB C63E380FCC7F13D813D0A2EBF03EEBE000B0B5FCA3181B7F9A1B>114 D<3803FE30380FFFF0EA3E03EA7800127000F01370A27E00FE1300EAFFE06CB4FC14C06C 13E06C13F0000713F8C6FCEB07FC130000E0137C143C7E14387E6C137038FF01E038E7FF C000C11300161B7E9A1B>I<13E0A41201A31203A21207120F381FFFE0B5FCA2380FE000 AD1470A73807F0E0000313C03801FF8038007F0014267FA51A>I<39FFE07FF0A3000F13 07B2140FA2000713173903F067FF3801FFC738007F87201B7D9A25>I<39FFFC03FFA339 0FF000F0000714E07F0003EB01C0A2EBFC0300011480EBFE070000140013FFEB7F0EA214 9EEB3F9C14FC6D5AA26D5AA36D5AA26D5AA25CA21307003890C7FCEA7C0FEAFE0E131E13 1C5BEA74F0EA3FE0EA0F8020277F9A23>121 D E /Ft 26 123 df<137E3801C180EA03 01380703C0120EEB018090C7FCA5B512C0EA0E01B0387F87F8151D809C17>12 D<126012F0A212701210A41220A212401280040C7C830C>44 D<126012F0A2126004047C 830C>46 D73 D<007FB512C038700F01006013 0000401440A200C014201280A300001400B1497E3803FFFC1B1C7F9B1E>84 D97 D<12FC121CAA137CEA1D87381E0180381C00C014E0 14601470A6146014E014C0381E018038190700EA10FC141D7F9C17>II< EB1F801303AAEA03F3EA0E0BEA1807EA30031270126012E0A6126012701230EA1807EA0E 1B3803E3F0141D7F9C17>II<13F8EA018CEA071E1206 EA0E0C1300A6EAFFE0EA0E00B0EA7FE00F1D809C0D>II<12FC121CAA 137C1387EA1D03001E1380121CAD38FF9FF0141D7F9C17>I<1218123CA21218C7FCA712 FC121CB0EAFF80091D7F9C0C>I<12FC121CB3A9EAFF80091D7F9C0C>108 D<39FC7E07E0391C838838391D019018001EEBE01C001C13C0AD3AFF8FF8FF8021127F91 24>IIII114 DI<1204A412 0CA2121C123CEAFFE0EA1C00A91310A5120CEA0E20EA03C00C1A7F9910>I<38FC1F80EA 1C03AD1307120CEA0E1B3803E3F014127F9117>I<39FF3FC7E0393C0703C0001CEB0180 1500130B000E1382A21311000713C4A213203803A0E8A2EBC06800011370A2EB80300000 13201B127F911E>119 D<38FF07E0383C0380381C0100A2EA0E02A2EA0F06EA0704A2EA 0388A213C8EA01D0A2EA00E0A31340A25BA212F000F1C7FC12F312661238131A7F9116> 121 DI E /Fu 7 117 df65 D97 DII114 DI<1203 A45AA25AA2EA3FFC12FFEA1F00A9130CA4EA0F08EA0798EA03F00E1A7F9913>I E /Fv 9 122 df0 D<126012F0A2126004047D890A>I<1202A3 EAC218EAF278EA3AE0EA0F80A2EA3AE0EAF278EAC218EA0200A30D0E7E8E12>3 D<13FC38071380380810400010132000201310A200401308A200801304A3B512FC388010 04A400401308A200201310A20010132000081340380713803800FC0016187E931B>8 D<13FC38070380380800404813200028135000241390004413883842010838810204EA80 8413481330A213481384EA810238420108384400880024139000281350001013206C1340 380703803800FC0016187E931B>10 D<1406A380A2EC0180EC00C01560B612FCA2C81260 15C0EC0180EC0300A21406A31E127E9023>33 D<1206120FA2120E121EA2121C123C1238 A212301270A2126012E012C0124008117F910A>48 D<12C0B3AF02217C980A>106 D<1206A8EAFFF0A2EA0600B30C1D7E9611>121 D E /Fw 26 120 df<127012F812FCA212741204A41208A21210A212201240060F7C840E>44 DI<127012F8A3127005057C840E>I<13801203120F12F31203B3 A9EA07C0EAFFFE0F217CA018>49 D57 D<497EA3497EA3EB05E0A2EB09F013 08A2EB1078A3497EA3497EA2EBC01F497EA248B51280EB0007A20002EB03C0A348EB01E0 A348EB00F0121C003EEB01F839FF800FFF20237EA225>65 DI<39FF FC3FFF390FC003F039078001E0AE90B5FCEB8001AF390FC003F039FFFC3FFF20227EA125 >72 D75 D<39FF8007FF3907C000F81570D805E01320EA04F0A213 78137C133C7F131F7FEB0780A2EB03C0EB01E0A2EB00F014F81478143C143E141E140FA2 EC07A0EC03E0A21401A21400000E1460121FD8FFE0132020227EA125>78 D<3803F020380C0C60EA1802383001E0EA70000060136012E0A21420A36C1300A2127812 7FEA3FF0EA1FFE6C7E0003138038003FC0EB07E01301EB00F0A214707EA46C1360A26C13 C07E38C8018038C60700EA81FC14247DA21B>83 D97 D<120E12FE121E120EAB131FEB61C0EB8060380F0030000E1338143C141C14 1EA7141C143C1438000F1370380C8060EB41C038083F0017237FA21B>II101 D<14703803F198380E1E18EA1C0E38380700A200781380A400381300A2EA1C0EEA1E1CEA 33F00020C7FCA212301238EA3FFE381FFFC06C13E0383000F0481330481318A400601330 A2003813E0380E03803803FE0015217F9518>103 D<120E12FE121E120EABEB1F80EB60 C0EB80E0380F0070A2120EAF38FFE7FF18237FA21B>I<121C123EA3121CC7FCA8120E12 7E121E120EB1EAFFC00A227FA10E>I<120E12FE121E120EB3ADEAFFE00B237FA20E>108 D<380E1F8038FE60C0381E80E0380F0070A2120EAF38FFE7FF18157F941B>110 DI114 DI<1202A41206A3120E121E123EEAFFFCEA0E00AB1304A6EA070812 03EA01F00E1F7F9E13>I<000E137038FE07F0EA1E00000E1370AD14F0A2380601703803 82783800FC7F18157F941B>I<39FF8FF87F393E01E03C001CEBC01814E0000E1410EB02 60147000071420EB04301438D803841340EB8818141CD801C81380EBD00C140E3900F00F 00497EA2EB6006EB400220157F9423>119 D E /Fx 23 122 df12 D<127812FCA212FEA2127A1202A51204A312 08A212101220A2124007147A8512>44 D72 D80 D82 D<007FB712E0A23A7E000F800700781501007015000060166000401620A200C01630A248 1610A6C71500B3AC4A7E010FB57EA22C317EB030>84 D<13FE380303C0380C00E0001013 7080003C133C003E131C141EA21208C7FCA3EB0FFEEBFC1EEA03E0EA0F80EA1F00123E12 3C127C481404A3143EA21278007C135E6CEB8F08390F0307F03903FC03E01E1F7D9E21> 97 D99 D<15F0141FA214011400AFEB0FC0EB70303801C00C3803800238070001 120E001E13005AA2127C1278A212F8A71278A2127C123CA27E000E13016C130238038004 6C6C487E3A00F030FF80EB1FC021327EB125>II<15F090387F03083901 C1C41C380380E8390700700848EB7800001E7FA2003E133EA6001E133CA26C5B6C13706D 5A3809C1C0D8087FC7FC0018C8FCA5121C7E380FFFF86C13FF6C1480390E000FC00018EB 01E048EB00F000701470481438A500701470A26C14E06CEB01C00007EB07003801C01C38 003FE01E2F7E9F21>103 DI<120FEA1F 80A4EA0F00C7FCABEA0780127FA2120F1207B3A6EA0FC0EAFFF8A20D307EAF12>I108 D<260780FEEB1FC03BFF 83078060F0903A8C03C180783B0F9001E2003CD807A013E4DA00F47F01C013F8A2495BB3 A2486C486C133F3CFFFC1FFF83FFF0A2341F7E9E38>I<380780FE39FF83078090388C03 C0390F9001E0EA07A06E7E13C0A25BB3A2486C487E3AFFFC1FFF80A2211F7E9E25>II<380781FC39FF86078090388801C0390F9000E0D807A013 7001C01378497F153E151E151FA2811680A716005DA2151E153E153C6D5B01A013705D90 389803C0D9860FC7FCEB81F80180C8FCAB487EEAFFFCA2212D7E9E25>I<380783E038FF 8418EB887CEA0F90EA07A01438EBC000A35BB3487EEAFFFEA2161F7E9E19>114 D<3801FC10380E0330381800F048137048133012E01410A37E6C1300127EEA3FF06CB4FC 6C13C0000313E038003FF0EB01F813006C133CA2141C7EA27E14186C1338143000CC1360 38C301C03880FE00161F7E9E1A>I<1340A513C0A31201A212031207120F381FFFE0B5FC 3803C000B01410A80001132013E000001340EB78C0EB1F00142C7FAB19>II 121 D E end %%EndProlog %%BeginSetup %%Feature: *Resolution 300dpi TeXDict begin %%PaperSize: a4 %%EndSetup %%Page: 1 1 1 0 bop 106 381 a Fx(Higher)21 b(T)n(yp)r(e)g(Recursion,)g (Rami\014cation)f(and)h(P)n(olynomial)f(Time)350 516 y Fw(S.)c(Bellan)o(toni)626 497 y Fv(\003)780 516 y Fw(K.-H.)f(Niggl) 1027 497 y Fv(y)1182 516 y Fw(H.)h(Sc)o(h)o(wic)o(h)o(ten)o(b)q(erg)803 625 y(August)g(1,)g(1999)872 844 y Fu(Abstract)164 916 y Ft(It)e(is)g(sho)o(wn)g(ho)o(w)g(to)g(restrict)i(recursion)f(on)f (notation)f(in)h(all)e(\014nite)j(t)o(yp)q(es)g(so)f(as)g(to)g(c)o (haracterize)i(the)102 966 y(p)q(olynomial)11 b(time)j(computable)f (functions.)21 b(The)15 b(restrictions)h(are)f(obtained)g(b)o(y)g (using)f(a)h(rami\014ed)e(t)o(yp)q(e)102 1016 y(structure,)i(and)f(b)o (y)g(adding)f(linear)g(concepts)j(to)e(the)g(lam)o(b)q(da)e(calculus.) -12 1167 y Fs(1)67 b(In)n(tro)r(duction)-12 1276 y Fr(Recursion)16 b(in)f(all)h(\014nite)f(t)o(yp)q(es)f(w)o(as)g(in)o(tro)q(duced)i(b)o (y)e(Hilb)q(ert)i([8)o(])e(and)h(later)f(b)q(ecame)i(kno)o(wn)e(as)g (the)g(essen)o(tial)-12 1332 y(part)e(of)h(G\177)-23 b(odel's)12 b(system)h Fq(T)18 b Fr([7)o(].)h(This)13 b(system)g(has)f(long)h(b)q(een)h(view)o(ed)g(as)e(a)g(p)q(o)o(w)o (erful)h(sc)o(heme)g(unsuitable)i(for)-12 1389 y(describing)e(small)f (complexit)o(y)g(classes)f(suc)o(h)g(as)g(p)q(olynomial)i(time.)19 b(Simmons)11 b([17)o(])g(sho)o(w)o(ed)f(that)h(rami\014cation)-12 1445 y(can)20 b(b)q(e)h(used)f(to)g(c)o(haracterize)g(the)g(primitiv)o (e)h(recursiv)o(e)g(functions)g(b)o(y)e(higher)i(t)o(yp)q(e)f (recursion.)35 b(Leiv)m(an)o(t)-12 1502 y([13)o(])16 b(used)g(rami\014cation)g(notions)g(with)g(all)g(\014nite)h(t)o(yp)q (es)f(in)g(order)g(to)f(c)o(haracterize)h(the)g(Kalmar-elemen)o(tary) -12 1558 y(functions.)k(Leiv)m(an)o(t)13 b(and)g(Marion)f([15])g(sho)o (w)o(ed)g(that)g(another)g(form)f(of)i(rami\014cation)f(can)h(b)q(e)g (used)g(to)f(restrict)-12 1614 y(higher)k(t)o(yp)q(e)f(recursion)h(to)e (PSP)l(A)o(CE.)h(Ho)o(w)o(ev)o(er,)f(to)g(c)o(haracterize)h(the)g(m)o (uc)o(h)h(smaller)f(class)h(of)e(p)q(olynomial-)-12 1671 y(time)d(computable)g(functions)g(b)o(y)g(higher)g(t)o(yp)q(e)f (recursion,)i(it)f(seems)f(that)g(an)g(additional)i(principle)i(is)c (required.)-12 1727 y(By)20 b(in)o(tro)q(ducing)h(a)e(lib)q(eralize)q (d)j(form)d(of)h(linearit)o(y)g(\(allo)o(wing)h(m)o(ultiple)g(use)f(of) f(ground)h(t)o(yp)q(es)g(results\))f(in)-12 1784 y(conjunction)14 b(with)e(an)h(extension)g(of)f(rami\014cation)h(concepts)g(\(as)e (considered)j(e.g.)e(b)o(y)g(Simmons)h([17)o(],)f(Leiv)m(an)o(t)-12 1840 y([13)o(],)f(and)h(Bellan)o(toni)g(and)g(Co)q(ok)e([1]\))g(to)h (all)h(\014nite)g(t)o(yp)q(es,)f(w)o(e)g(c)o(haracterize)h(p)q (olynomial-time)h(computabilit)o(y)l(.)38 1905 y(Based)21 b(on)g(simple)h(t)o(yp)q(es)e(built)j(from)d(the)g(ground)h(t)o(yp)q(e) g Fq(\023)f Fr(of)h(binary)g(n)o(umerals)g(b)o(y)g Fp(!)p Fr(,)h Fo(r)n(e)n(cursion)e(on)-12 1961 y(notation)f Fr(in)d(t)o(yp)q(e)f Fq(\033)i Fr(is)f(a)e(mapping)i Fp(R)679 1968 y Fn(\033)717 1961 y Fr(of)f(t)o(yp)q(e)g Fq(\033)g Fp(!)e Fr(\()p Fq(\023)f Fp(!)h Fq(\033)h Fp(!)g Fq(\033)r Fr(\))d Fp(!)j Fq(\023)e Fp(!)h Fq(\033)k Fr(de\014ned)g(b)o (y)732 2060 y Fp(R)771 2067 y Fn(\033)802 2060 y Fq(g)9 b(h)f Fm(0)k Fr(=)h Fq(g)659 2129 y Fp(R)698 2136 y Fn(\033)729 2129 y Fq(g)c(h)f Fr(\()p Fm(s)833 2136 y Fn(i)846 2129 y Fm(n)p Fr(\))k(=)h Fq(h)p Fr(\()p Fm(s)1018 2136 y Fn(i)1032 2129 y Fm(n)p Fr(\)\()p Fp(R)1136 2136 y Fn(\033)1158 2129 y Fq(g)r(h)p Fm(n)p Fr(\))p Fq(:)-12 2228 y Fr(No)o(w)i(a)g (single)h(recursion)g(in)g(t)o(yp)q(e)f Fq(\023)e Fp(!)g Fq(\023)i Fr(can)h(de\014ne)g(a)f(function)h(of)f(exp)q(onen)o(tial)h (gro)o(wth:)645 2326 y Fq(e)d Fr(:=)g Fp(R)779 2333 y Fn(\023)p Fv(!)p Fn(\023)848 2326 y Fm(s)869 2333 y Fl(1)896 2326 y Fr(\()p Fq(\025u)967 2308 y Fn(\023)981 2326 y Fq(V)1017 2308 y Fn(\023)p Fv(!)p Fn(\023)1080 2326 y Fq(y)1104 2308 y Fn(\023)1118 2326 y Fq(:V)d Fr(\()p Fq(V)f(y)r Fr(\)\))-12 2425 y(satis\014es)17 b Fp(j)p Fq(e)p Fr(\()p Fq(m)p Fr(\)\()p Fq(n)p Fr(\))p Fp(j)12 b Fr(=)j(2)428 2409 y Fv(j)p Fn(m)p Fv(j)491 2425 y Fr(+)c Fp(j)p Fq(n)p Fp(j)16 b Fr(\(where)g(as)g(usual)h Fp(j)p Fq(n)p Fp(j)d Fr(=)g Fp(d)p Fr(log)1128 2436 y Fl(2)1148 2425 y Fr(\()p Fq(n)d Fr(+)g(1\))p Fp(e)p Fr(\).)22 b(Note)16 b(that)f(the)i(function)g Fq(e)f Fr(can)-12 2482 y(b)q(e)h(assigned)f (a)g(rami\014ed)h(t)o(yp)q(e)f(under)g(the)g(sc)o(heme)g(of)g(Leiv)m (an)o(t)h([15)o(],)e(in)i(whic)o(h)g Fq(m)f Fr(is)g(tier)g(1)g(and)g Fq(n)g Fr(is)h(tier)f(0.)p -12 2523 780 2 v 39 2550 a Fk(\003)57 2565 y Fj(Researc)o(h)j(supp)q(orted)g(b)o(y:)26 b(Graduiertenk)o(oll)q(eg)21 b(\\Logik)e(in)f(der)g(Informatik")g(der)g (DF)o(G,)g(M)q(\177)-20 b(unc)o(hen.)32 b(Assistance)19 b(of)e(the)-12 2611 y(Fields)e(Instituted)f(for)f(Researc)o(h)h(in)g (Mathematical)h(Sciences,)f(T)m(oron)o(to)f(is)h(gratefully)h(ac)o(kno) o(wledged.)41 2642 y Fk(y)57 2658 y Fj(T)m(ec)o(hnisc)o(he)i(Univ)o (ersit\177)-19 b(at)17 b(Ilmenau,)g(Institut)f(f)q(\177)-20 b(ur)15 b(theoretisc)o(he)i(und)f(tec)o(hnisc)o(he)h(Informatik,)f(F)m (ac)o(hgebiet)h(Komplexit\177)-19 b(ats-)-12 2704 y(theorie,)14 b(PF)f(100565,)h(98684)f(Ilmenau,)h(German)o(y)m(.)k(The)13 b(author)h(w)o(as)e(a\016liated)j(with)f(LMU)e(while)j(this)f(pap)q(er) f(w)o(as)g(written.)952 2828 y Fr(1)p eop %%Page: 2 2 2 1 bop -12 199 a Fr(What)14 b(this)h(sho)o(ws)f(is)i(that)e(another)g (requiremen)o(t,)h(in)h(addition)f(to)f(rami\014cation)i(of)e(the)h (recursion)g(v)m(ariable,)-12 256 y(is)f(required)h(to)d(restrict)i (higher)g(t)o(yp)q(e)f(recursion)h(to)f(p)q(olytime)i(computabilit)o(y) l(.)21 b(The)13 b(problem)h(seems)g(to)f(lie)h(in)-12 312 y(the)i(nested,)g(nonlinear)i(use)e(of)f(the)h Fo(pr)n(evious)h (value)i Fq(V)10 b Fr(.)22 b(Our)16 b(approac)o(h)g(is)g(to)f(in)o(tro) q(duce)i(at)e(the)h(same)g(time)-12 369 y(b)q(oth)g(rami\014cation)f (of)g(the)g(recursion)h(v)m(ariable)h(and)e(linearit)o(y)i(conditions.) 38 433 y(T)l(o)j(do)g(so)f(w)o(e)h(enric)o(h)h(the)f(t)o(yp)q(e)g (structure)f(with)i(the)f(formation)f(of)g(t)o(yp)q(es)h(!)p Fq(\033)r Fr(,)g(called)i Fo(c)n(omplete)e(typ)n(es)t Fr(;)-12 490 y(all)d(other)e(t)o(yp)q(es)g(are)h(called)h Fo(inc)n(omplete)p Fr(.)j(In)o(tuitiv)o(ely)l(,)d(ob)s(jects)e(of)g (complete)h(t)o(yp)q(es)g(are)f(completely)i(kno)o(wn;)-12 546 y(they)e(can)g(b)q(e)h(used)f(as)f(the)h(pattern)g(for)f(a)h (recursion,)g(or)f(if)h(they)g(are)g(of)f(higher)i(t)o(yp)q(e)f(they)g (can)g(b)q(e)g(used)h(in)f(a)-12 603 y(non-linear)i(w)o(a)o(y)l(.)i(Ob) s(jects)c(of)g(incomplete)i(t)o(yp)q(es)e(can)g(only)h(b)q(e)g (accessed)g(through)e(a)h(few)g(lo)o(w-order)g(bits,)h(or)-12 659 y(if)f(they)f(are)g(of)g(higher)h(t)o(yp)q(e,)f(can)g(b)q(e)h(used) g(in)g(a)f(certain)g(linear)i(w)o(a)o(y)d(only)l(.)20 b(Then)15 b(w)o(e)f(de\014ne)h(the)f(class)h(RA)g(of)-12 716 y Fo(r)n(ami\014e)n(d)i(a\016nable)j Fr(terms.)j(The)17 b(recursor)f Fp(R)808 723 y Fn(\033)847 716 y Fr(receiv)o(es)h(the)g (rami\014ed)g(t)o(yp)q(e)g Fq(\033)f Fp(!)p Fr(!\(!)p Fq(\023)e Fp(!)i Fq(\033)g Fp(!)f Fq(\033)r Fr(\))f Fp(!)p Fr(!)p Fq(\023)h Fp(!)h Fq(\033)-12 772 y Fr(and)21 b(is)g(admitted)g (for)f(an)o(y)h(!-free)f Fq(\033)r Fr(;)j(as)d(w)o(ell,)j(w)o(e)e (require)g(that)f(terms)g(of)h(complete)g(t)o(yp)q(e)g(ha)o(v)o(e)f(no) h(free)-12 829 y(v)m(ariables)d(of)d(incomplete)j(t)o(yp)q(es.)k(Input) 17 b(p)q(ositions)g(of)f(t)o(yp)q(es)g(!)p Fq(\023)g Fr(and)g Fq(\023)g Fr(corresp)q(ond)h(to)e(normal)h(/)g(tier)g(1)g(and) -12 885 y(safe)h(/)f(tier)h(0)f(input)i(p)q(ositions,)g(common)e(in)i (earlier)f(w)o(ork)f(on)h(rami\014ed)g(recursion)h(\(cf.)e([17)o(,)g (12)o(,)h(1)o(,)g(3,)f(16)o(]\).)-12 941 y Fo(A\016nability)k Fr(is)d(cen)o(tral)g(to)f(the)h(system)f(and)h(expresses)g(the)g (linearit)o(y)h(constrain)o(ts)e(for)g(b)q(ound)i(v)m(ariables)g(of)-12 998 y(incomplete)f(t)o(yp)q(es.)j(A\016nabilit)o(y)d(is)e(designed)i (suc)o(h)e(that)g(the)g(system)g(RA)h(is)f(closed)h(under)g(reduction.) 38 1063 y(W)l(e)21 b(sho)o(w)f(that)g(for)h(eac)o(h)g(closed)g(RA)q (-term)f Fq(t)i Fr(of)e(t)o(yp)q(e)h(lev)o(el)h(1,)g(one)f(can)g (\014nd)g(a)g(p)q(olynomial)h Fq(p)1815 1070 y Fn(t)1851 1063 y Fr(suc)o(h)-12 1119 y(that)14 b(for)f(all)i(n)o(umerals)f Fq(~)-22 b(n)p Fr(,)14 b(one)h(can)f(compute)g(the)h(normal)f(form)f Fi(nf)t Fr(\()p Fq(t)o(~)-22 b(n)p Fr(\))14 b(in)h(time)f Fq(p)1459 1126 y Fn(t)1474 1119 y Fr(\()p Fp(j)o Fq(~)-22 b(n)p Fp(j)p Fr(\).)19 b(Th)o(us,)13 b Fq(t)i Fr(denotes)f(a)-12 1176 y(p)q(olynomial)e(time)f(computable)g(function.)20 b(The)10 b(con)o(v)o(erse)g(also)h(holds,)h(as)e(eac)o(h)g(p)q (olynomial)j(time)d(computable)-12 1232 y(function)20 b(is)f(computed)g(b)o(y)g(some)g(RA-term.)30 b(Observ)o(e)20 b(that)e(there)h(are)f Fo(two)k Fr(normalizations)e(required)g(to)-12 1289 y(compute)d Fq(t)o(~)-22 b(x)17 b Fr(for)f(sp)q(eci\014c)j(v)m (alues)e Fq(~)-22 b(n)17 b Fr(of)e Fq(~)-22 b(x)p Fr(.)24 b(\(i\))17 b(Normalize)h Fq(t)f Fr(to)f Fq(u)p Fr(,)g(sa)o(y)l(,)h (whic)o(h)g(ma)o(y)f(tak)o(e)g(a)h(long)g(time)g(\(not)-12 1345 y(p)q(olynomial)g(in)e(the)g(length)h(of)e Fq(t)p Fr(\).)20 b(\(ii\))15 b(Normalize)h Fq(u)o(~)-22 b(n)p Fr(,)15 b(whic)o(h)g(will)i(tak)o(e)d(p)q(olynomial)i(time)g(in)f(the)g (length)h(of)-13 1401 y Fq(~)-22 b(n)p Fr(.)20 b(One)c(ma)o(y)f(view)h (\(i\))f(as)f(a)h(\(complex\))h(compilation)g(step,)f(pro)q(ducing)i (e\016cien)o(t)e(co)q(de.)38 1466 y(Recen)o(tly)l(,)i(Hofmann)e([9)o(,) g(10)o(])g(used)h(mo)q(dalities)h(of)e(rami\014cation)h(and)f(of)g (linearit)o(y)i(in)f(a)f(lam)o(b)q(da)h(calculus,)-12 1523 y(and)j(de\014ned)i(them)e(for)f(all)i(higher)g(t)o(yp)q(es.)31 b(This)19 b(in)o(teresting)h(w)o(ork)e(also)h(c)o(haracterizes)g(p)q (olynomial)i(time)-12 1579 y(computabilit)o(y)l(.)g(Ho)o(w)o(ev)o(er,) 12 b(the)h(pro)q(of)g(metho)q(ds)g(of)f(the)h(t)o(w)o(o)f(pap)q(ers)h (are)g(completely)h(di\013eren)o(t,)g(as)e(Hofmann)-12 1636 y(uses)k(a)f(category-theoretic)f(approac)o(h.)38 1700 y(There)i(are)f(some)g(connections)h(b)q(et)o(w)o(een)g(the)f (presen)o(t)g(w)o(ork)g(and)g(the)g(\\ligh)o(t)h(linear)h(logic")f(of)e (Girard)i([6)o(];)-12 1757 y(but)g(due)f(to)g(di\013ering)h(framew)o (orks)e(an)h(exact)g(comparison)g(has)g(not)g(b)q(een)h(made.)38 1822 y(The)k(approac)o(h)f(to)g(higher-t)o(yp)q(e)i(functions)f(tak)o (en)f(in)i(this)f(w)o(ork)e(con)o(trasts)h(with)h(Co)q(ok)f(and)h (Kapron's)-12 1878 y(w)o(ell-kno)o(wn)d(Basic)f(F)l(easible)g(F)l (unctions)h(\(BFF\))d(de\014ned)j(b)o(y)e(PV)1155 1860 y Fn(!)1195 1878 y Fr(terms)g([4].)20 b(There,)15 b(explicit)j(size)e (b)q(ounds)-12 1934 y(are)c(used)g(and)g(the)f(critical)i(v)m(alue)g (computed)f(during)h(the)f(recursion)g(is)g(of)f(ground)h(t)o(yp)q(e.) 19 b(A)11 b(further)h(di\013erence)-12 1991 y(can)i(b)q(e)g(seen)h(b)o (y)e(the)h(fact)f(that)g(the)h(system)f(RA)i(admits)e(the)h(iteration)g (functional)h Fq(I)i Fr(satisfying)d Fq(I)t Fr(\()p Fq(f)r(;)8 b(x;)g(y)r Fr(\))j(=)-12 2047 y Fq(f)15 2031 y Fl(\()p Fv(j)p Fn(x)p Fv(j)p Fl(\))84 2047 y Fr(\()p Fq(y)r Fr(\),)17 b(whereas)f Fq(I)21 b Fr(is)c(not)g(BFF.)f(On)h(the)h(other)e(hand,)i (one)f(in)o(tuitiv)o(ely)i(exp)q(ects)e(that)f(in)i(some)f(suitable)-12 2104 y(sense)f(BFF)f(functions)h(should)g(b)q(e)g(de\014nable)g(in)h (RA.)-12 2255 y Fs(2)67 b(T)n(yp)r(es)22 b(and)h(terms)-12 2365 y Fr(The)16 b Fo(typ)n(es)i Fr(are:)i Fq(\023)15 b Fr(is)h(a)f(t)o(yp)q(e,)g(and)g(if)h Fq(\033)h Fr(and)e Fq(\034)21 b Fr(are)15 b(t)o(yp)q(es,)g(then)g(so)g(are)g Fq(\033)f Fp(!)g Fq(\034)20 b Fr(and)15 b(!)p Fq(\033)r Fr(.)20 b(W)l(e)15 b(assume)g(!)g(binds)-12 2422 y(tigh)o(ter)g(than)g Fp(!)p Fr(,)g(and)h Fp(!)f Fr(asso)q(ciates)g(to)g(the)g(righ)o(t.)915 2405 y Fl(1)38 2486 y Fr(T)o(yp)q(es)f(of)f(the)g(form)g(!)p Fq(\033)i Fr(are)e Fo(c)n(omplete)s Fr(;)h(all)g(others)g(are)f Fo(inc)n(omplete)p Fr(.)18 b(In)c(what)f(follo)o(ws,)h(iterated)g(!'s)e (are)i(not)-12 2543 y(needed,)j(ho)o(w)o(ev)o(er,)e(for)g(tec)o(hnical) i(simplicit)o(y)l(,)h(they)e(are)g(allo)o(w)o(ed.)22 b Fo(Gr)n(ound)f Fr(t)o(yp)q(es)16 b(are)f(the)h(t)o(yp)q(es)g(of)g (lev)o(el)h(0,)-12 2599 y(de\014ning)g(lev)o(el)h(b)o(y:)i Fq(l)q Fr(\()p Fq(\023)p Fr(\))13 b(=)h(0;)h Fq(l)q Fr(\(!)p Fq(\033)r Fr(\))d(=)h Fq(l)q Fr(\()p Fq(\033)r Fr(\);)h(and)i Fq(l)q Fr(\()p Fq(\033)f Fp(!)f Fq(\034)5 b Fr(\))13 b(=)h(max)o Fp(f)p Fq(l)q Fr(\()p Fq(\034)5 b Fr(\))p Fq(;)j Fr(1)g(+)j Fq(l)q Fr(\()p Fq(\033)r Fr(\))p Fp(g)p Fr(.)20 b(A)15 b Fo(higher)21 b Fr(t)o(yp)q(e)16 b(is)g(an)o(y)p -12 2641 780 2 v 40 2668 a Fh(1)57 2684 y Fj(Linear)e(logicians)i(ma)o (y)e(read)f(\\)p Fg(!)p Fj(")h(as)f(\\)p Ff(\()p Fj(".)952 2828 y Fr(2)p eop %%Page: 3 3 3 2 bop -12 199 a Fr(t)o(yp)q(e)17 b(of)e(lev)o(el)j(at)e(least)g(1.)23 b(F)l(or)15 b(example,)i(!!)p Fq(\023)f Fr(is)h(a)f(ground)g(t)o(yp)q (e,)g(but)g Fq(\023)f Fp(!)g Fq(\023)h Fr(is)h(a)f(higher)h(t)o(yp)q (e.)23 b(!-free)16 b(t)o(yp)q(es)-12 256 y(are)f(called)i Fo(safe)p Fr(.)i(Ev)o(ery)c(ground)g(t)o(yp)q(e)h(is)f(either)h(safe)f (or)g(complete.)-12 319 y(The)h Fo(c)n(onstant)f(symb)n(ols)j Fr(are)c(listed)j(b)q(elo)o(w,)e(with)h(their)g(t)o(yp)q(es.)195 410 y Fm(0)77 b Fq(\023)195 467 y Fm(s)216 474 y Fl(0)298 467 y Fq(\023)13 b Fp(!)g Fq(\023)716 b Fr(\(binary)15 b(successor)g Fq(x)e Fp(7!)g Fr(2)s Fp(\001)s Fq(x)p Fr(\))195 523 y Fm(s)216 530 y Fl(1)298 523 y Fq(\023)g Fp(!)g Fq(\023)716 b Fr(\(binary)15 b(successor)g Fq(x)e Fp(7!)g Fr(2)s Fp(\001)s Fq(x)c Fr(+)h(1\))195 580 y Fm(p)74 b Fq(\023)13 b Fp(!)g Fq(\023)716 b Fr(\(binary)15 b(predecessor)h Fq(x)c Fp(7!)h(b)1639 562 y Fn(x)p 1639 569 20 2 v 1640 595 a Fl(2)1664 580 y Fp(c)p Fr(\))195 636 y Fm(c)218 643 y Fn(\033)298 636 y Fq(\023)g Fp(!)g Fq(\033)h Fp(!)g Fq(\033)g Fp(!)f Fq(\033)h Fp(!)f Fq(\033)47 b Fr(for)15 b Fq(\033)i Fr(safe)176 b(\(cases)14 b(in)i(t)o(yp)q(e)g Fq(\033)r Fr(\))195 693 y Fp(R)234 700 y Fn(\033)298 693 y Fq(\033)f Fp(!)p Fr(!\(!)p Fq(\023)d Fp(!)h Fq(\033)h Fp(!)f Fq(\033)r Fr(\))f Fp(!)p Fr(!)p Fq(\023)h Fp(!)g Fq(\033)47 b Fr(for)15 b Fq(\033)h Fr(safe)42 b(\(recursion)15 b(in)h(t)o(yp)q(e)g Fq(\033)r Fr(\))-12 784 y Fo(T)m(erms)h Fr(are)d(built)h(from)f(these)g(constan)o(ts)f(and)h(t)o(yp)q(ed)h(v)m (ariables)g Fq(x)1162 767 y Fn(\033)1200 784 y Fr(b)o(y)f(in)o(tro)q (duction)h(and)f(elimination)i(rules)-12 840 y(for)f(the)g(t)o(w)o(o)f (t)o(yp)q(e)h(forms)g Fq(\033)f Fp(!)f Fq(\034)20 b Fr(and)15 b(!)p Fq(\033)r Fr(,)f(i.e.)502 935 y(\()p Fq(\025x)573 917 y Fn(\033)595 935 y Fq(:r)630 917 y Fn(\034)651 935 y Fr(\))669 917 y Fn(\033)q Fv(!)p Fn(\034)747 935 y Fq(;)53 b Fr(\()p Fq(r)853 917 y Fn(\033)q Fv(!)p Fn(\034)930 935 y Fq(s)951 917 y Fn(\033)975 935 y Fr(\))993 917 y Fn(\034)1014 935 y Fq(;)g Fr(\(!)p Fq(r)1133 917 y Fn(\033)1156 935 y Fr(\))1174 917 y Fl(!)p Fn(\033)1206 935 y Fq(;)g Fr(\()p Fq(r)1312 917 y Fl(!)p Fn(\033)1345 935 y Fq(\024)p Fr(\))1389 917 y Fn(\033)1412 935 y Fq(:)-12 1030 y Fr(W)l(e)13 b(write)f Fq(r)199 1014 y Fl(!)p Fn(\033)232 1030 y Fq(\024)h Fr(\(rather)f(than)g Fq(\024r)574 1014 y Fl(!)p Fn(\033)607 1030 y Fr(\))g(in)i(order)e(to)g(ha)o(v)o(e)g(a)o (v)m(ailable)i(a)e(uniform)h(notation)f(for)g(elimination)j(terms)-12 1087 y Fq(ts)25 1094 y Fl(1)53 1087 y Fq(:)8 b(:)g(:)e(s)135 1094 y Fn(n)174 1087 y Fr(with)15 b Fq(s)298 1094 y Fn(i)328 1087 y Fr(either)h(a)f(term)f(or)h Fq(\024)p Fr(.)38 1150 y(A)f Fo(binary)h(numer)n(al)j Fr(is)d(either)g Fm(0)f Fr(or)f Fm(s)692 1157 y Fn(i)704 1162 y Fh(1)731 1150 y Fq(:)8 b(:)g(:)d Fm(s)812 1157 y Fn(i)824 1163 y Fe(k)845 1150 y Fm(s)866 1157 y Fl(1)886 1150 y Fm(0)14 b Fr(where)g Fq(i)1072 1157 y Fn(j)1102 1150 y Fp(2)f(f)p Fr(0)p Fq(;)8 b Fr(1)p Fp(g)p Fr(.)18 b(In)d(the)f Fo(c)n(onversion)f (rules)18 b Fr(b)q(elo)o(w)c(w)o(e)-12 1207 y(assume)h(that)g Fm(s)265 1214 y Fn(i)278 1207 y Fm(n)h Fr(is)f(a)g(binary)h(n)o(umeral) g(\(hence)g(distinct)g(from)e Fm(0)p Fr(\).)628 1302 y(\()p Fq(\025x:r)q Fr(\))p Fq(s)d Fp(7!)i Fq(r)q Fr([)p Fq(s=x)p Fr(])628 1371 y(\(!)p Fq(r)q Fr(\))p Fq(\024)f Fp(7!)h Fq(r)628 1440 y Fm(s)649 1447 y Fl(0)668 1440 y Fm(0)g Fp(7!)g Fm(0)628 1509 y(p0)g Fp(7!)g Fm(0)628 1578 y(p)p Fr(\()p Fm(s)696 1585 y Fn(i)709 1578 y Fm(n)p Fr(\))g Fp(7!)g Fm(n)628 1647 y(c0)p Fq(r)q(t)715 1654 y Fl(0)735 1647 y Fq(t)751 1654 y Fl(1)784 1647 y Fp(7!)g Fq(r)628 1715 y Fm(c)p Fr(\()p Fm(s)690 1722 y Fn(i)704 1715 y Fm(n)p Fr(\))p Fq(r)q(t)789 1722 y Fl(0)808 1715 y Fq(t)824 1722 y Fl(1)857 1715 y Fp(7!)g Fq(t)931 1722 y Fn(i)628 1784 y Fp(R)8 b Fq(g)g(h)g Fr(!)p Fm(0)k Fp(7!)h Fq(g)628 1853 y Fp(R)8 b Fq(g)g(h)g Fr(!\()p Fm(s)791 1860 y Fn(i)804 1853 y Fm(n)p Fr(\))k Fp(7!)h Fq(h\024)g Fr(!\()p Fm(s)1038 1860 y Fn(i)1051 1853 y Fm(n)p Fr(\))g(\()p Fp(R)8 b Fq(g)f(h)h Fr(!)p Fm(n)p Fr(\))-12 1948 y(Here)18 b(an)g(application)h(of)e(!)g(on)o(to)g(a)g(term)g(asso)q(ciates)h (tigh)o(ter)f(than)h(other)f(applications,)i(and)f(to)f(the)h(righ)o (t,)-12 2005 y(while)f(other)e(applications)h(asso)q(ciate)g(to)e(the)h (left.)21 b(Th)o(us)15 b Fp(R)p Fq(g)r(h)p Fr(!)p Fq(n)f Fr(is)i(\(\(\()p Fp(R)p Fq(g)r Fr(\))p Fq(h)p Fr(\)\(!)o Fq(n)p Fr(\)\).)38 2068 y(The)11 b Fo(length)j Fp(j)p Fq(t)p Fp(j)d Fr(of)f(a)h(term)f Fq(t)i Fr(is)f(de\014ned)i(b)o(y)d Fp(j)p Fq(x)p Fp(j)i Fr(=)h Fp(j)p Fq(c)p Fp(j)f Fr(=)h(1;)f Fp(j)p Fq(\025x:r)q Fp(j)e Fr(=)j Fp(j)p Fr(!)p Fq(r)q Fp(j)f Fr(=)h Fp(j)p Fq(r)q(\024)p Fp(j)e Fr(=)i Fp(j)p Fq(r)q Fp(j)r Fr(+)r(1;)e Fp(j)p Fq(r)q(s)p Fp(j)h Fr(=)h Fp(j)p Fq(r)q Fp(j)r Fr(+)r Fp(j)p Fq(s)p Fp(j)r Fr(+)r(1.)-12 2125 y Fo(R)n(e)n(dexes)19 b Fr(are)d(subterms)h(sho)o(wn)e(on)i(the)f (left)h(side)g(of)f(con)o(v)o(ersion)g(rules)h(ab)q(o)o(v)o(e.)23 b(A)17 b(term)e(is)i(in)g Fo(normal)h(form)-12 2181 y Fr(if)f(it)f(do)q(es)g(not)f(con)o(tain)h(a)g(redex.)22 b(F)l(or)16 b(ev)o(ery)f(term)h Fq(t)g Fr(there)g(is)g(a)g(unique)h (normal-form)f(term)f Fi(nf)t Fr(\()p Fq(t)p Fr(\))g(\(see)h(e.g.)-12 2238 y([18)o(,)i(11)o(])f(for)g(pro)q(ofs)h(of)f(normalisation)h(in)h (G\177)-23 b(odel's)17 b(system)g Fq(T)6 b Fr(\).)27 b(Tw)o(o)17 b(terms)g(are)h Fo(e)n(quivalent)j Fr(if)d(they)g(ha)o(v)o (e)-12 2294 y(the)d(same)g(normal)h(form.)38 2358 y(One)e(writes)f Fi(FV)q Fr(\()p Fq(t)p Fr(\))g(for)f(the)h(set)g(of)g(free)g(v)m (ariables)i(of)d Fq(t)p Fr(,)i(and)f Fi(F)o(O)p Fr(\()p Fq(x;)8 b(t)p Fr(\))k(for)h(the)g(n)o(um)o(b)q(er)g(of)g(free)g(o)q (ccurrences)-12 2414 y(of)i Fq(x)g Fr(in)h Fq(t)p Fr(.)k(Sa)o(y)15 b(that)g(a)g(term)f(is)i Fo(c)n(omplete)p Fr(,)f Fo(inc)n(omplete)p Fr(,)f Fo(safe)p Fr(,)g(or)h Fo(gr)n(ound)20 b Fr(if)15 b(its)h(t)o(yp)q(e)f(is.)38 2478 y(Similar)k(to)e(G\177)-23 b(odel's)18 b Fq(T)6 b Fr(,)17 b(t)o(yp)q(es)h(and)f(terms)h(are)f(in)o (terpreted)h(o)o(v)o(er)f(the)g(set)h(theoretical)g(function)g(spaces.) -12 2534 y(Th)o(us,)23 b(in)f(the)g(seman)o(tics)f(w)o(e)h(iden)o(tify) g(ob)s(jects)f(of)g(t)o(yp)q(e)h(!)p Fq(\033)h Fr(with)e(those)h(of)f (t)o(yp)q(e)g Fq(\033)r Fr(,)i(since)f(w)o(e)f(are)h(only)-12 2591 y(in)o(terested)c(in)h(the)f(computational)g(b)q(eha)o(viour)g(of) f(terms.)27 b(W)l(e)18 b(in)o(terpret)g Fq(\023)f Fr(as)h(the)f (non-negativ)o(e)h(in)o(tegers.)-12 2647 y(The)k(v)m(alue)h([)-8 b([)p Fq(t)p Fr(])g(])264 2654 y Fn(')311 2647 y Fr(of)21 b(a)g(term)h Fq(t)g Fr(in)g(an)g(en)o(vironmen)o(t)g Fq(')g Fr(is)g(de\014ned)h(as)e(usual,)j(where)e([)-8 b([!)p Fq(r)q Fr(])g(])1642 2654 y Fn(')1690 2647 y Fr(:=)23 b([)-8 b([)p Fq(r)q Fr(])g(])1819 2654 y Fn(')1865 2647 y Fr(and)-12 2704 y([)g([)p Fq(r)q(\024)p Fr(])g(])72 2711 y Fn(')109 2704 y Fr(:=)13 b([)-8 b([)p Fq(r)q Fr(])g(])228 2711 y Fn(')252 2704 y Fr(.)19 b(As)14 b(the)g(v)m(alue)g(of)f(a)h (closed)g(term)f Fq(t)h Fr(is)g(indep)q(enden)o(t)i(of)d(an)o(y)h(en)o (vironmen)o(t,)g(w)o(e)f(just)g(write)h([)-8 b([)p Fq(t)p Fr(])g(].)952 2828 y(3)p eop %%Page: 4 4 4 3 bop -12 199 a Fs(3)67 b Fd(RA)p Fs(-terms)-12 308 y Fr(Tw)o(o)14 b(subterms)h Fq(a)309 315 y Fn(i)337 308 y Fr(and)g Fq(a)449 315 y Fn(j)482 308 y Fr(o)q(ccurring)h(in)f(a)f (term)h Fq(t)g Fr(are)f Fo(sc)n(op)n(e)h(e)n(quivalent)j Fr(if)d(whenev)o(er)g Fq(\025y)h Fr(binds)g(a)f(v)m(ariable)-12 364 y(free)g(in)h(either)g Fq(a)281 371 y Fn(i)311 364 y Fr(or)e Fq(a)390 371 y Fn(j)409 364 y Fr(,)g(then)i(b)q(oth)f Fq(a)671 371 y Fn(i)701 364 y Fr(and)g Fq(a)813 371 y Fn(j)846 364 y Fr(lie)i(within)f(the)g(scop)q(e)f(of)g(the)g Fq(\025y)r Fr(.)-12 452 y Fm(De\014nition.)24 b Fr(Let)16 b Fq(x)f Fr(b)q(e)h(an)f(incomplete)h(v)m(ariable,)h(and)e(let)h Fq(s)f Fr(b)q(e)h(a)f(term.)38 515 y(1.)26 b(An)18 b Fo(a\016nation)i Fr(of)d Fq(x)g Fr(in)h Fq(s)g Fr(is)g(a)f(ground)g(t)o (yp)q(e)h(subterm)f Fq(a)1130 499 y Fn(\023)1162 515 y Fr(with)g Fi(F)o(O)p Fr(\()p Fq(x;)8 b(a)p Fr(\))15 b(=)i(1)g(suc)o(h)g(that)g(ev)o(ery)g(free)-12 572 y(o)q(ccurrence)g (of)f Fq(x)g Fr(in)h Fq(s)f Fr(is)g(in)h(an)f(o)q(ccurrence)h(of)f Fq(a)g Fr(in)g Fq(s)p Fr(,)g(where)h(the)f(o)q(ccurrences)h(of)e Fq(a)h Fr(are)g(scop)q(e)g(equiv)m(alen)o(t)-12 628 y(in)g Fq(s)p Fr(.)38 692 y(2.)k(W)l(e)15 b(call)h Fq(x)f Fo(a\016nable)j Fr(in)e Fq(s)g Fr(if)g(there)f(is)h(an)f(a\016nation)g(of)f Fq(x)i Fr(in)g Fq(s)f Fr(or)g Fi(F)o(O)p Fr(\()p Fq(x;)8 b(s)p Fr(\))j Fp(\024)i Fr(1.)38 786 y(Ev)o(ery)i(t)o(yp)q(e)g Fq(\023)g Fr(v)m(ariable)i(is)f(trivially)g(a\016nable)g(in)g(ev)o(ery) f(term,)g(b)q(ecause)h(it)f(is)h(an)f(a\016nation)g(of)g(itself.)-12 874 y Fm(De\014nition.)24 b Fq(r)16 b Fr(is)g(an)f(RA)p Fo(-term)20 b Fr(\(R)15 b(for)g(rami\014ed,)g(A)g(for)g(a\016nable\))g (if)38 937 y(\(R\))g(ev)o(ery)g(complete)h(subterm)f(con)o(tains)g (complete)h(free)g(v)m(ariables)g(only)l(,)g(and)38 1001 y(\(A\))f(for)f(ev)o(ery)h(subterm)g Fq(\025x:s)g Fr(with)h Fq(x)f Fr(incomplete,)h(the)f(v)m(ariable)i Fq(x)e Fr(is)h(a\016nable)g (in)g(a)e(reduct)i(of)f Fq(s)p Fr(.)38 1096 y(As)h(p)q(oin)o(ted)g(out) f(in)i(the)f(In)o(tro)q(duction,)g(one)g(in)o(tuition)h(is)f(that)f (terms)g(of)g(complete)h(t)o(yp)q(e)g(can)g(b)q(e)g(used)g(in)-12 1152 y(a)f(non-linear)i(w)o(a)o(y)l(,)e(while)i(ob)s(jects)d(of)i (higher)g(incomplete)h(t)o(yp)q(e)e(can)h(b)q(e)g(used)g(only)g(in)g(a) g(certain)g(linear)g(w)o(a)o(y)-12 1209 y(expressed)f(b)o(y)e(\(A\).)g (Accordingly)l(,)i(\(R\))f(requires)g(that)f(complete)i(terms)e(ha)o(v) o(e)g(no)h(incomplete)h(free)f(v)m(ariables.)-12 1265 y(Non-primitiv)o(e)j(recursiv)o(e)f(gro)o(wth)d(rate)i(is)h(ruled)g (out)e(b)o(y)h(this)h(plus)g(the)f(requiremen)o(t)h(that)e Fo(step)i(terms)j Fq(h)c Fr(in)-12 1321 y Fp(R)27 1328 y Fn(\033)50 1321 y Fq(g)r(hn)e Fr(ha)o(v)o(e)f(complete)h(t)o(yp)q(es) g(\(cf.)f(Simmons)h([17)o(]\):)18 b(The)13 b Fo(pr)n(evious)h(value)i Fr(\()p Fq(V)21 b Fr(b)q(elo)o(w\))13 b(of)g(an)f(outer)g(recursion)-12 1378 y(cannot)g(b)q(e)h(applied)i(to)c(the)i(previous)g(v)m(alue)h(of)d (an)i(inner)g(recursion.)20 b(In)13 b(con)o(trast,)e(in)i(G\177)-23 b(odel's)13 b Fq(T)18 b Fr(the)12 b(function)-12 1434 y Fq(F)17 1441 y Fn(!)43 1434 y Fr(\()p Fq(x)p Fr(\))g(=)h Fq(F)194 1441 y Fn(x)216 1434 y Fr(\()p Fq(x)p Fr(\),)h(where)h Fq(F)465 1441 y Fl(0)485 1434 y Fr(\()p Fq(x)p Fr(\))d(:=)h Fq(x)d Fr(+)g(1)15 b(and)h Fq(F)857 1441 y Fn(n)p Fl(+1)925 1434 y Fr(\()p Fq(x)p Fr(\))c(:=)h Fq(F)1089 1441 y Fn(n)1113 1416 y Fl(\()p Fn(x)p Fl(+1\))1207 1434 y Fr(\()p Fq(x)p Fr(\),)h(can)i(b)q(e)f(de\014ned)i(b)o(y)470 1529 y Fq(t)486 1536 y Fn(F)508 1540 y Fe(!)546 1529 y Fr(:=)12 b Fq(\025x)659 1510 y Fn(\023)673 1529 y Fq(:)p Fp(R)725 1536 y Fn(\023)p Fv(!)p Fn(\023)794 1529 y Fm(S)c Fr(\()p Fq(\025u)902 1510 y Fn(\023)916 1529 y Fq(V)952 1510 y Fn(\023)p Fv(!)p Fn(\023)1015 1529 y Fq(:)g Fp(R)1075 1536 y Fn(\023)1096 1529 y Fm(S0)g Fr(\()p Fq(\025u)1230 1510 y Fn(\023)1243 1529 y Fq(v)1267 1510 y Fn(\023)1281 1529 y Fq(:V)i(v)r Fr(\)\))e Fq(x)g(x)-12 1624 y Fr(T)l(o)15 b(obtain)h(p)q(olynomial)h (gro)o(wth)d(rate)h(w)o(e)g(additionally)i(require)g(that)d(recursion)j (in)f(t)o(yp)q(e)f Fq(\033)i Fr(is)f(admitted)g(for)-12 1680 y(safe)f(\(i.e.)g(!-free\))g(t)o(yp)q(es)g Fq(\033)i Fr(only)e({)g(recall)i(the)e(t)o(yp)q(e)g Fq(\033)f Fp(!)p Fr(!\(!)p Fq(\023)f Fp(!)g Fq(\033)h Fp(!)f Fq(\033)r Fr(\))f Fp(!)p Fr(!)p Fq(\023)h Fp(!)g Fq(\033)j Fr(of)f Fp(R)1554 1687 y Fn(\033)1592 1680 y Fr(in)h(RA)q(.)38 1744 y(F)l(or)22 b(ground)h(t)o(yp)q(e)g(recursion,)i(the)d(system)h (mimics)h(the)e(use)h(of)g(so-called)h(safe)e(\()p Fq(\023)p Fr(\))g(and)h(normal)g(\(!)p Fq(\023)p Fr(\))-12 1800 y(input)e(p)q(ositions)f(in)h([1)o(]:)29 b(Previous)20 b(v)m(alues)h(in)f(recursions)g(can)g(only)g(b)q(e)h(passed)f(to)f (safe)g(input)i(p)q(ositions,)-12 1856 y(i.e.)12 b(input)g(p)q (ositions)h(whic)o(h)f(do)g(not)f(induce)i(the)f(unfolding)h(of)e (recursions.)20 b(P)o(olynomially-gro)o(wing)12 b(functions)-12 1913 y Fp(\010)k Fr(satisfying)f Fp(j)p Fq(m)10 b Fp(\010)g Fq(n)p Fp(j)j Fr(=)g Fp(j)p Fq(m)p Fp(j)c Fr(+)i Fp(j)p Fq(n)p Fp(j)p Fr(,)j(and)h Fp(\012)h Fr(satisfying)f Fp(j)p Fq(m)10 b Fp(\012)g Fq(n)p Fp(j)j Fr(=)g Fp(j)p Fq(m)p Fp(j)c(\001)h(j)p Fq(n)p Fp(j)p Fr(,)k(are)h(easily)h (de\014nable)h(in)f(RA)q(:)614 2006 y Fq(t)630 2013 y Fv(\010)702 2006 y Fr(:=)c Fq(\025x)815 1990 y Fl(!)p Fn(\023)839 2006 y Fq(y)863 1990 y Fn(\023)878 2006 y Fq(:)p Fp(R)930 2013 y Fn(\023)951 2006 y Fq(y)d Fr(!\()p Fq(\025u)1066 1990 y Fl(!)p Fn(\023)1089 2006 y Fq(v)1113 1990 y Fn(\023)1128 2006 y Fq(:)f Fm(s)1170 2013 y Fl(1)1188 2006 y Fq(v)r Fr(\))g Fq(x)614 2063 y(t)630 2070 y Fv(\012)702 2063 y Fr(:=)k Fq(\025x)815 2046 y Fl(!)p Fn(\023)839 2063 y Fq(y)863 2046 y Fl(!)p Fn(\023)887 2063 y Fq(:)p Fp(R)939 2070 y Fn(\023)961 2063 y Fm(0)c Fr(!\()p Fq(\025u)1079 2046 y Fl(!)p Fn(\023)1102 2063 y Fq(v)1126 2046 y Fn(\023)1140 2063 y Fq(:)g(t)1177 2070 y Fv(\010)1213 2063 y Fq(xv)r Fr(\))g Fq(y)-12 2161 y Fr(The)15 b(abilit)o(y)h(to)f(form)f(terms)g (that)g(ha)o(v)o(e)g(recursiv)o(ely)j(computed)e(outputs)f(of)h(t)o(yp) q(e)g(!)p Fq(\023)p Fr(,)f(suc)o(h)h(as)g Fq(\025x)1736 2145 y Fl(!)p Fn(i)1759 2161 y Fq(:)p Fr(!\()p Fq(x)8 b Fp(\012)i Fq(x)p Fr(\),)-12 2218 y(distinguishes)18 b(ground)d(t)o(yp)q(e)g(recursions)h(in)g(RA)g(or)e([1])g(from)h(the)g (systems)g(of)g(Leiv)m(an)o(t)h([14)o(].)38 2281 y(F)l(or)g(higher)i(t) o(yp)q(e)g(recursion,)f(previous)h(v)m(alues)h(can)e(only)g(b)q(e)h (passed)g(to)e(safe)h(a\016nable)g(input)i(p)q(ositions.)-12 2338 y(Admitting)j(recursion)f Fp(R)454 2345 y Fn(\033)498 2338 y Fr(for)f(incomplete)j Fq(\033)f Fr(w)o(ould)f(allo)o(w)g(one)g (to)g(de\014ne)h(prop)q(er)f(Kalmar-elemen)o(tary)-12 2394 y(functions;)16 b(e.g.)e(a)h(function)h Fq(e)517 2378 y Fv(0)544 2394 y Fr(satisfying)g Fq(e)768 2378 y Fv(0)779 2394 y Fr(\()p Fq(m;)8 b(n)p Fr(\))k Fp(\025)h Fq(n)990 2378 y Fl(2)1008 2366 y Fk(j)p Fe(m)p Fk(j)1073 2394 y Fr(w)o(ould)j(then)f(ha)o(v)o(e)g(an)g(RA)h(de\014nition)576 2489 y Fp(R)615 2496 y Fl(!)p Fn(\023)p Fv(!)p Fn(\023)694 2489 y Fr(\()p Fq(\025y)763 2470 y Fl(!)p Fn(\023)787 2489 y Fq(:y)r(\024)p Fr(\))8 b(!\()p Fq(\025u)960 2470 y Fl(!)p Fn(\023)982 2489 y Fq(V)1018 2470 y Fl(!)p Fn(\023)p Fv(!)p Fn(\023)1090 2489 y Fq(y)1114 2470 y Fl(!)p Fn(\023)1139 2489 y Fq(:)g(V)16 b Fr(!\()p Fq(t)1250 2496 y Fc(sq)1291 2489 y Fq(y)r Fr(\)\))-12 2584 y(where)g Fq(t)136 2591 y Fc(sq)182 2584 y Fr(:=)d Fp(R)282 2591 y Fn(\023)304 2584 y Fr(\()p Fm(s)343 2591 y Fl(1)362 2584 y Fm(0)p Fr(\))8 b(!\()p Fq(\025u)498 2567 y Fl(!)p Fn(\023)520 2584 y Fq(v)544 2567 y Fn(\023)559 2584 y Fq(:)g Fm(s)601 2591 y Fl(0)619 2584 y Fr(\()p Fm(s)658 2591 y Fl(0)677 2584 y Fq(v)r Fr(\)\))14 b(de\014nes)j(the)e(function)h Fi(sq)q Fr(\()p Fq(n)p Fr(\))c(=)h(2)1344 2567 y Fl(2)p Fv(j)p Fn(n)p Fv(j)1404 2584 y Fr(.)38 2647 y(A\016nabilit)o(y)19 b(is)e(designed)i(to)d(rule)i(out)f(nested)h(o)q(ccurrences)g(of)f (previous)h(v)m(alues)g(in)g(recursions,)g(suc)o(h)g(as)-12 2704 y(that)h(used)i(to)e(de\014ne)h Fq(e)g Fr(in)h(the)f(In)o(tro)q (duction.)34 b(It)20 b(requires)g(that)f(if)h(w)o(e)g(lam)o(b)q(da)g (abstract)f(a)g(higher-t)o(yp)q(e)952 2828 y(4)p eop %%Page: 5 5 5 4 bop -12 199 a Fr(incomplete)19 b(v)m(ariable)g Fq(x)f Fr(in)g Fq(r)q Fr(,)f(then)h(either)g Fi(F)o(O)p Fr(\()p Fq(x;)8 b(r)q Fr(\))15 b Fp(\024)i Fr(1)g(or)g(else)h(the)g(free)f(o)q (ccurrences)i(of)e Fq(x)g Fr(in)i Fq(r)f Fr(can)f(b)q(e)-12 256 y(separated)e(b)o(y)g(the)h(o)q(ccurrences)g(of)e(one)i(and)f(the)g (same)g(ground)h(t)o(yp)q(e)f(con)o(text)f Fq(a)p Fr(,)h(the)h (a\016nation)f(of)f Fq(x)h Fr(in)h Fq(r)q Fr(.)38 320 y(If)g Fq(x)g Fr(is)g(a\016nable)h(in)f Fq(r)h Fr(and)f Fq(r)e Fp(\000)-7 b(!)14 b Fq(r)679 304 y Fv(0)691 320 y Fr(,)h(then)h Fq(x)g Fr(need)h(not)e(b)q(e)i(a\016nable)f(in)h Fq(r)1374 304 y Fv(0)1385 320 y Fr(.)22 b(T)l(o)15 b(obtain)h(a)g (system)f(closed)-12 376 y(under)h(reduction,)g(condition)g(\(A\))f (requires)h(that)e Fq(x)i Fr(is)f(a\016nable)h(in)g(a)f(reduct)h(of)e Fq(r)q Fr(.)38 441 y(T)l(erms)20 b(with)g(prop)q(ert)o(y)g(\(R\))f(are) h(not)f(closed)i(under)g(application,)h(as)e(one)g(ma)o(y)f(form)g (e.g.)g Fq(X)1754 424 y Fn(\023)p Fv(!)p Fl(!)p Fn(\023)1826 441 y Fq(y)1850 424 y Fn(\023)1864 441 y Fr(,)i(or)-12 497 y(else)c(\()p Fq(\025y)144 481 y Fn(\023)158 497 y Fq(:)8 b Fr(!)p Fm(0)p Fr(\))p Fq(y)r Fr(.)20 b(Ho)o(w)o(ev)o(er,)15 b(if)i Fq(r)q(s)f Fr(is)g(incomplete)i(and)e Fq(r)q Fr(,)g Fq(s)g Fr(satisfy)f(\(R\),)h(then)g(so)g(do)q(es)g Fq(r)q(s)p Fr(.)22 b(It)16 b(is)h(also)f(rather)-12 554 y(immediate)c(that)e (terms)h(with)g(prop)q(ert)o(y)g(\(R\))g(are)f(closed)i(under)g (reductions.)19 b(This)12 b(is)f(also)g(true)g(for)f(RA)q(-terms,)-12 610 y(as)15 b(w)o(e)g(will)i(pro)o(v)o(e)d(next.)-12 702 y Fm(Theorem)j(3.1)g(\(Closure)h(under)f(reduction\).)23 b Fo(L)n(et)16 b Fq(r)h Fo(b)n(e)e(an)h Fr(RA)q Fo(-term.)38 766 y Fr(\(1\))f Fo(If)h Fq(r)d Fp(\000)-7 b(!)13 b Fq(r)302 750 y Fv(0)314 766 y Fo(,)j(then)g Fq(r)467 750 y Fv(0)495 766 y Fo(is)f(an)i Fr(RA)p Fo(-term.)38 830 y Fr(\(2\))e Fo(If)h Fq(x)g Fo(is)g(a\016nable)g(in)g Fq(r)q Fo(,)g(then)g Fq(x)g Fo(is)g(a\016nable)g(in)f Fi(nf)t Fr(\()p Fq(r)q Fr(\))p Fo(.)-12 932 y(Pr)n(o)n(of.)23 b Fr(W)l(e)17 b(sho)o(w)f(\(1\))g Fo(and)21 b Fr(\(2\))16 b(b)o(y)h(induction)h(on)f (the)g Fo(height)22 b Fq(h)p Fr(\()p Fq(r)q Fr(\))16 b(of)g(the)h(reduction)h(tree)e(for)h Fq(r)q Fr(,)f(and)h(side)-12 988 y(induction)h(on)f Fq(r)q Fr(.)23 b(Assuming)17 b(\(1\))e Fo(and)22 b Fr(\(2\))15 b(for)h(terms)g Fq(s)g Fr(with)h Fq(h)p Fr(\()p Fq(s)p Fr(\))e Fq(<)g(h)p Fr(\()p Fq(r)q Fr(\),)g(w)o(e)h(pro)q(ceed)i(to)d(pro)o(v)o(e)h(\014rst)g(\(1\))-12 1045 y(and)g(then)f(\(2\))f(for)h Fq(r)q Fr(.)38 1109 y(F)l(or)g(the)h(pro)q(of)g(of)f(\(1\),)g(let)i Fq(r)f Fr(b)q(e)h(an)f(RA-term,)g(and)g(assume)g Fq(r)e Fp(\000)-7 b(!)14 b Fq(r)1285 1092 y Fv(0)1297 1109 y Fr(.)22 b(Since)17 b(terms)f(with)g(prop)q(ert)o(y)f(\(R\))-12 1165 y(are)f(closed)h (under)g(reductions,)g(it)f(su\016ces)h(to)e(consider)j(a)d(subterm)i Fq(\025x:s)1285 1149 y Fv(0)1310 1165 y Fr(of)f Fq(r)1383 1149 y Fv(0)1408 1165 y Fr(where)h Fq(x)f Fr(is)g(incomplete,)i(and)-12 1222 y(pro)o(v)o(e)f(that)f Fq(x)h Fr(is)h(a\016nable)g(in)g(a)f (reduct)g(of)g Fq(s)783 1205 y Fv(0)795 1222 y Fr(.)20 b(W)l(e)15 b(pro)q(ceed)h(b)o(y)f(distinguishing)j(t)o(w)o(o)c(cases.) 38 1286 y Fo(Case)k Fq(s)173 1270 y Fv(0)199 1286 y Fr(=)13 b Fq(s)p Fr([)p Fq(t=y)r Fr(])j(for)f(a)g(subterm)h Fq(\025x:s)f Fr(of)g Fq(r)q Fr(.)21 b(By)16 b(assumption)f Fq(x)h Fr(is)g(a\016nable)h(in)f(a)f(reduct)h(of)g Fq(s)p Fr(.)21 b(Then)16 b Fq(x)-12 1343 y Fr(is)g(also)f(a\016nable)h(in)g(a)f (reduct)g(of)g Fq(s)612 1326 y Fv(0)624 1343 y Fr(,)g(since)h Fq(x)i(=)-28 b Fp(2)13 b Fi(FV)q Fr(\()p Fq(t)p Fr(\).)38 1407 y Fo(Case)18 b Fq(s)13 b Fp(\000)-7 b(!)13 b Fq(s)293 1390 y Fv(0)320 1407 y Fr(for)h(a)h(subterm)g Fq(\025x:s)g Fr(of)g Fq(r)q Fr(.)k(W)l(e)d(distinguish)h(t)o(w)o(o)d(sub)q(cases.)38 1471 y Fo(Sub)n(c)n(ase)k Fq(x)d Fr(is)h(a\016nable)g(in)h Fq(s)p Fr(.)k(Then)16 b Fq(s)e Fp(\000)-8 b(!)14 b Fq(s)846 1455 y Fv(0)871 1471 y Fp(\000)-7 b(!)944 1455 y Fv(\003)977 1471 y Fi(nf)t Fr(\()p Fq(s)p Fr(\),)15 b(and)g(b)o(y)h(the)f(side)i (IH)f(\(2\))f(for)f Fq(s)p Fr(,)i Fq(x)f Fr(is)i(a\016nable)-12 1528 y(in)f Fi(nf)t Fr(\()p Fq(s)p Fr(\))c(=)h Fi(nf)t Fr(\()p Fq(s)279 1511 y Fv(0)290 1528 y Fr(\).)20 b(Hence)c Fq(x)f Fr(is)h(a\016nable)f(in)h(a)f(reduct)h(of)f Fq(s)1050 1511 y Fv(0)1062 1528 y Fr(,)f(namely)i Fi(nf)t Fr(\()p Fq(s)1327 1511 y Fv(0)1338 1528 y Fr(\).)38 1592 y Fo(Sub)n(c)n(ase)h Fq(x)f Fr(is)f(a\016nable)h(in)g(a)f(reduct)h(of)e Fq(s)p Fr(.)20 b(Then)c(w)o(e)f(\014nd)h(ourselv)o(es)f(in)i(the)e(situation:) 446 1679 y Fq(s)58 b Fp(!)g Fq(s)649 1686 y Fl(1)728 1679 y Fp(!)g Fq(:)8 b(:)g(:)56 b Fp(!)j Fq(s)1067 1686 y Fn(n)1091 1679 y Fq(;)98 b(x)15 b Fr(a\016nable)h(in)g Fq(s)1499 1686 y Fn(n)446 1735 y Fp(#)446 1791 y Fq(s)467 1775 y Fv(0)-12 1890 y Fr(By)i(the)f(side)h(IH)g(\(1\))e(at)h Fq(s)p Fr(,)h Fq(s)509 1897 y Fl(1)546 1890 y Fr(is)g(an)f(RA)q(-term.) 26 b(Successiv)o(ely)19 b(applying)g(the)e(IH)h(\(1\))e(to)h Fq(s)1621 1897 y Fl(1)1641 1890 y Fq(;)8 b(:)g(:)g(:)k(;)c(s)1771 1897 y Fn(n)p Fv(\000)p Fl(1)1840 1890 y Fr(,)17 b(one)-12 1946 y(obtains)f(that)e Fq(s)267 1953 y Fn(n)306 1946 y Fr(is)i(an)f(RA-term.)20 b(Th)o(us,)15 b(b)o(y)g(the)g(IH)h(\(2\))e (at)h Fq(s)1109 1953 y Fn(n)1132 1946 y Fr(,)g Fq(x)g Fr(is)h(a\016nable)g(in)g Fi(nf)s Fr(\()p Fq(s)1561 1953 y Fn(n)1585 1946 y Fr(\))c(=)h Fi(nf)t Fr(\()p Fq(s)1743 1930 y Fv(0)1754 1946 y Fr(\).)38 2010 y(F)l(or)i(the)h(pro)q(of)f(of)g (\(2\),)g(let)h Fq(r)g Fr(b)q(e)g(an)g(RA-term)g(and)g(assume)f(that)g Fq(x)h Fr(is)g(a\016nable)g(in)g Fq(r)q Fr(.)21 b(If)16 b Fq(r)h Fr(is)f(normal)f(w)o(e)-12 2067 y(are)g(done.)20 b(So)15 b(assume)h Fq(r)d Fp(\000)-7 b(!)13 b Fq(r)553 2050 y Fv(0)564 2067 y Fr(.)20 b(Again,)15 b(w)o(e)g(pro)q(ceed)h(b)o (y)f(distinguishing)j(t)o(w)o(o)c(cases.)38 2131 y Fo(Case)k Fr(there)e(is)h(an)e(a\016nation)h Fq(a)g Fr(of)f Fq(x)h Fr(in)g Fq(r)q Fr(.)22 b(W)l(e)16 b(ma)o(y)f(assume)g(that)h(there)f (is)i(a)e(redex)h(in)h Fq(a)f Fr(\(otherwise,)f Fq(x)-12 2188 y Fr(is)i(a\016nable)f(in)h Fq(r)293 2171 y Fv(0)320 2188 y Fr(and)f(the)g(claim)h(follo)o(ws)f(b)o(y)g(\(1\))f(giving)i (that)e Fq(r)1155 2171 y Fv(0)1182 2188 y Fr(is)i(an)e(RA)q(-term)h (and)g(then)g(IH)g(\(2\))f(giving)-12 2244 y(that)f Fq(x)h Fr(is)g(a\016nable)g(in)h Fi(nf)t Fr(\()p Fq(r)q Fr(\)\).)i(Let)d Fq(r)657 2228 y Fv(0)o(0)693 2244 y Fr(b)q(e)g(the)g(reduct)g(of)f Fq(r)i Fr(obtained)f(b)o(y)g(replacing)h(all)g(o)q(ccurrences)f(of)g Fq(a)f Fr(in)-12 2301 y Fq(r)j Fr(with)g Fi(nf)s Fr(\()p Fq(a)p Fr(\).)23 b(Hence)17 b Fq(h)p Fr(\()p Fq(r)469 2284 y Fv(0)o(0)490 2301 y Fr(\))d Fq(<)h(h)p Fr(\()p Fq(r)q Fr(\),)g(and)i Fq(r)796 2284 y Fv(0)o(0)833 2301 y Fr(is)g(an)f(RA-term)g(b)o(y)h(\(1\).)22 b(Then)17 b(the)f(claim)h(follo)o(ws)g(from)e(the)-12 2357 y(IH)h(for)e(\(2\),)g (for)h(either)g Fq(x)g Fr(has)g(at)g(most)f(one)h(free)h(o)q(ccurrence) g(in)g Fi(nf)s Fr(\()p Fq(a)p Fr(\))f(\(then)g Fi(nf)s Fr(\()p Fq(a)p Fr(\))g(is)h(an)f(a\016nation)g(of)f Fq(x)h Fr(in)-12 2413 y Fq(r)10 2397 y Fv(00)31 2413 y Fr(\),)g(or)f(else)i (there)g(is)f(an)h(a\016nation)f Fq(b)f Fr(of)h Fq(x)g Fr(in)h Fi(nf)t Fr(\()p Fq(a)p Fr(\))e(\(then)h Fq(b)g Fr(is)h(an)f(a\016nation)g(of)g Fq(x)g Fr(in)h Fq(r)1576 2397 y Fv(0)o(0)1597 2413 y Fr(\).)38 2478 y Fo(Case)f Fi(F)o(O)p Fr(\()p Fq(x;)8 b(r)q Fr(\))j Fp(\024)i Fr(1.)18 b(By)13 b(\(1\))e(and)h(the)h(IH)f(\(2\))g(w)o(e)g(ma)o(y)f(assume)h Fi(F)o(O)p Fr(\()p Fq(x;)c(r)1316 2461 y Fv(0)1327 2478 y Fr(\))k Fp(\025)h Fr(2,)f(i.e.)g(a)g(subterm)g(con)o(taining)-12 2534 y Fq(x)i Fr(is)g(duplicated)h(during)g(the)e(reduction.)21 b(Considering)14 b(all)h(reductions,)f(the)g(only)g(ones)f(whic)o(h)i (can)e(duplicate)-12 2591 y(a)j(subterm)h(are)f Fp(R)g Fr(reductions)i(and)f Fq(\014)h Fr(reductions.)25 b(But)17 b(in)h(the)e(former)g(case,)h(the)f(duplicated)j(subterm)e(of)-12 2647 y Fq(r)i Fr(has)g(complete)g(t)o(yp)q(e,)g(hence)g(b)o(y)g(the)f (prop)q(ert)o(y)g(\(R\))h(cannot)f(con)o(tain)h Fq(x)p Fr(.)29 b(In)19 b(the)g(latter)f(case,)h(there)f(is)h(a)-12 2704 y(redex)e(\()p Fq(\025y)r(:s)p Fr(\))p Fq(t)f Fr(in)i Fq(r)f Fr(with)g Fq(x)e Fp(2)h Fi(FV)q Fr(\()p Fq(t)p Fr(\))g(suc)o(h)h(that)f Fq(r)901 2687 y Fv(0)929 2704 y Fr(is)h(formed)g(b)o(y)f(replacing)i(\()p Fq(\025y)r(:s)p Fr(\))p Fq(t)e Fr(with)h Fq(s)p Fr([)p Fq(t=y)r Fr(].)24 b(Since)18 b Fq(r)952 2828 y Fr(5)p eop %%Page: 6 6 6 5 bop -12 199 a Fr(satis\014es)15 b(\(R\))g(and)f Fq(t)i Fr(con)o(tains)e(the)h(incomplete)h(v)m(ariable)h Fq(x)p Fr(,)d(it)h(m)o(ust)f(b)q(e)h(that)f Fq(t)h Fr(and)g(hence)h Fq(y)h Fr(is)e(incomplete.)-12 256 y(As)f Fq(r)g Fr(satis\014es)g (\(A\),)f Fq(y)j Fr(is)e(a\016nable)g(in)h(a)e(reduct)i Fq(s)863 239 y Fv(0)888 256 y Fr(of)f Fq(s)p Fr(.)19 b(So)14 b(let)g Fq(r)1140 239 y Fv(0)o(0)1175 256 y Fr(b)q(e)g (obtained)h(from)e Fq(r)1549 239 y Fv(0)1574 256 y Fr(b)o(y)g (replacing)j Fq(s)p Fr([)p Fq(t=y)r Fr(])-12 312 y(with)h Fq(s)114 296 y Fv(0)126 312 y Fr([)p Fq(t=y)r Fr(].)22 b(Then)17 b Fq(r)392 296 y Fv(0)o(0)429 312 y Fr(is)g(an)f(RA)q(-term)g (b)o(y)g(\(1\),)f(and)i Fq(r)996 296 y Fv(0)1021 312 y Fp(\000)-7 b(!)1094 296 y Fv(\003)1129 312 y Fq(r)1151 296 y Fv(0)o(0)1172 312 y Fr(.)23 b(F)l(urthermore,)16 b Fq(x)g Fr(is)h(a\016nable)g(in)g Fq(r)1834 296 y Fv(0)o(0)1855 312 y Fr(,)f(for)-12 369 y(if)h Fi(F)o(O)p Fr(\()p Fq(y)r(;)8 b(s)173 352 y Fv(0)184 369 y Fr(\))14 b Fp(\024)h Fr(1,)g(then)i Fi(F)o(O)p Fr(\()p Fq(x;)8 b(r)567 352 y Fv(0)n(0)587 369 y Fr(\))14 b Fp(\024)h Fr(1,)h(and)g(if)h Fq(b)f Fr(is)g(an)g(a\016nation)h(of)e Fq(y)k Fr(in)e Fq(s)1371 352 y Fv(0)1383 369 y Fr(,)f(then)g Fq(b)p Fr([)p Fq(t=y)r Fr(])f(is)i(an)f(a\016nation)-12 425 y(of)f Fq(x)h Fr(in)g Fq(r)157 409 y Fv(0)o(0)178 425 y Fr(.)21 b(Therefore,)15 b(applying)i(the)f(induction)h(h)o(yp)q(othesis)f(\(2\))f(to)g Fq(r)1274 409 y Fv(0)o(0)1295 425 y Fr(,)g(w)o(e)g(obtain)h(that)f Fq(x)g Fr(is)h(a\016nable)g(in)-12 482 y Fi(nf)t Fr(\()p Fq(r)69 465 y Fv(0)o(0)89 482 y Fr(\))d(=)g Fi(nf)s Fr(\()p Fq(r)q Fr(\).)p 1919 454 19 2 v 1919 480 2 26 v 1937 480 V 1919 482 19 2 v 38 577 a Fm(Note)p Fr(.)19 b(If)14 b Fq(t)f Fr(is)h(an)f(RA)q(-term)f(of)h(t)o(yp)q(e)f Fq(~)-22 b(\033)15 b Fp(!)p Fr(!)p Fq(\034)j Fr(with)12 b Fq(~)-22 b(\033)15 b Fr(all)f(ground)f(and)g(no)g(incomplete)i(free)e (v)m(ariables,)i(then)-12 634 y(the)g(incomplete)h(argumen)o(t)d(t)o (yp)q(es)i Fq(\033)643 641 y Fn(i)671 634 y Fr(are)f Fo(r)n(e)n(dundant)k Fr(in)e(the)e(sense)h(that)e Fq(t)i Fr(is)g(equiv)m(alen)o(t)h(to)e(some)g(RA-term)-12 690 y Fq(\025)o(~)-22 b(x)40 673 y Fn(~)-17 b(\033)64 690 y Fq(:t)93 697 y Fl(1)127 690 y Fr(where)15 b Fq(t)274 697 y Fl(1)309 690 y Fr(has)f(no)g(free)h(o)q(ccurrence)h(of)e(an)g (incomplete)i Fq(x)1132 697 y Fn(i)1146 690 y Fr(.)k(T)l(o)14 b(see)h(this,)f(\014rst)h(note)f(that)g(in)h(a)f(normal)-12 746 y(RA)q(-term)j Fq(t)g Fr(ev)o(ery)g(subterm)g Fq(s)h Fr(of)e(t)o(yp)q(e)h(!)p Fq(\033)h Fp(!)e Fq(\034)22 b Fr(whic)o(h)c(is)g(not)e(an)h(abstraction)g(can)g(b)q(e)h Fq(\021)r Fr(-expanded)g(to)e(an)-12 803 y(RA)q(-term)11 b Fq(\025x)229 786 y Fl(!)p Fn(\033)262 803 y Fq(:sx)p Fr(.)19 b(Observ)o(e)12 b(that)f(for)h Fq(\033)i Fp(!)f Fq(\034)k Fr(with)12 b Fq(\033)i Fr(incomplete)g(this)e(need)h(not)f(b) q(e)g(p)q(ossible,)i(since)f Fq(\025x)1855 786 y Fn(\033)1878 803 y Fq(:sx)-12 859 y Fr(violates)k(\(R\))f(in)i(case)e Fq(\034)21 b Fr(is)c(complete.)25 b(It)16 b(is)h(w)o(ell)g(kno)o(wn)g (that)e(suc)o(h)i Fq(\021)h Fr(expansions)f(terminate)f(in)i(a)e (unique)-12 916 y(form,)e(called)j(the)e Fo(long)h(normal)g(form)j Fr(of)c Fq(t)p Fr(.)38 977 y(No)o(w)h(w)o(e)g(argue)g(as)g(follo)o(ws.) 23 b(Let)16 b Fq(s)f Fr(:=)g Fq(\025x)797 957 y Fn(\033)817 962 y Fh(1)797 990 y Fl(1)836 977 y Fq(;)8 b(:)g(:)g(:)k(;)c(x)971 961 y Fn(\033)991 965 y Fe(m)971 988 y Fn(m)1022 977 y Fq(:t)1051 954 y Fn(\033)1071 959 y Fe(m)p Fh(+1)1139 954 y Fv(!\001\001\001)o(!)p Fn(\033)1258 958 y Fe(n)1280 954 y Fv(!)p Fl(!)p Fn(\034)1051 990 y Fl(1)1363 977 y Fr(b)q(e)17 b(the)f(long)h(normal)f(form)g(of)g Fq(t)-12 1034 y Fr(where)h Fq(t)137 1041 y Fl(1)174 1034 y Fr(is)g(not)f(an)h (abstraction.)24 b(It)16 b(su\016ces)h(to)g(sho)o(w)f(that)g Fq(m)f Fr(=)g Fq(n)p Fr(,)i(for)f(then)h Fq(t)1460 1041 y Fl(1)1497 1034 y Fr(has)f(t)o(yp)q(e)h(!)p Fq(\034)k Fr(and)c(hence)-12 1090 y(b)o(y)e(\(R\))f(has)g(no)g(free)h(o)q (ccurrence)g(of)f(an)h(incomplete)h(v)m(ariable)g Fq(x)1127 1097 y Fn(i)1141 1090 y Fr(.)j(Supp)q(ose)d(that)e Fq(m)e(<)h(n)p Fr(.)20 b(Since)c Fq(t)f Fr(is)g(in)g(long)-12 1147 y(normal)j(form,)f Fq(\033)294 1154 y Fn(m)p Fl(+1)390 1147 y Fr(m)o(ust)g(b)q(e)i (incomplete.)29 b(As)18 b Fq(t)911 1154 y Fl(1)949 1147 y Fr(is)g(not)f(an)h(abstraction,)f(the)h(head)g(of)g Fq(t)1662 1154 y Fl(1)1700 1147 y Fr(cannot)f(b)q(e)h(a)-12 1203 y(constan)o(t)c(\(b)o(y)f(the)i(t)o(yping)f(of)g(our)g(constan)o (ts\))f(and)h(hence)h(m)o(ust)f(b)q(e)h(an)f(incomplete)i(higher)f(t)o (yp)q(e)f(v)m(ariable)i Fq(y)r Fr(,)-12 1260 y(so)f(it)g(is)h(distinct) h(from)c Fq(~)-22 b(x)p Fr(.)20 b(But)15 b(this)h(con)o(tradicts)f(the) g(assumption)g(on)h Fq(t)p Fr(.)-12 1405 y Fs(4)67 b Fd(RS)p Fs(-terms)-12 1511 y Fr(In)20 b(our)f(\014nal)h(result)f(w)o(e) g(will)i(only)f(b)q(e)g(in)o(terested)f(in)h(ground)g(t)o(yp)q(e)f (terms)f Fq(t)i Fr(whose)f(free)g(v)m(ariables)i(are)e(of)-12 1568 y(ground)e(t)o(yp)q(e.)26 b(W)l(e)18 b(\014rst)f(observ)o(e)g (that)f({)h(due)h(to)f(the)g(t)o(yping)g(of)g(our)g(constan)o(ts)g({)f (in)j(the)e(normal)g(form)g(of)-12 1624 y(an)o(y)e(suc)o(h)h(term)e (all)i(v)m(ariables)h(are)e(safe)g(or)f(ground.)-12 1701 y Fm(Lemma)k(4.1.)k Fo(L)n(et)17 b Fq(t)h Fo(b)n(e)g(a)g(gr)n(ound)g (typ)n(e)g(term)g(whose)g(fr)n(e)n(e)g(variables)f(ar)n(e)h(of)g(gr)n (ound)g(typ)n(e.)26 b(Then)17 b(in)h Fi(nf)s Fr(\()p Fq(t)p Fr(\))-12 1758 y Fo(al)r(l)e(variables)g(ar)n(e)g(safe)g(or)h (gr)n(ound.)-12 1853 y(Pr)n(o)n(of.)23 b Fr(Supp)q(ose)c(a)g(v)m (ariable)h Fq(x)554 1837 y Fn(\033)596 1853 y Fr(with)f Fq(\033)h Fr(neither)g(safe)e(nor)h(ground)g(o)q(ccurs)g(in)g Fi(nf)t Fr(\()p Fq(t)p Fr(\).)30 b(It)19 b(m)o(ust)f(b)q(e)h(b)q(ound) -12 1910 y(in)f(a)e(subterm)h(\()p Fq(\025x)332 1893 y Fn(\033)354 1910 y Fq(:r)q Fr(\))407 1893 y Fn(\033)q Fv(!)p Fn(\034)501 1910 y Fr(of)f Fi(nf)t Fr(\()p Fq(t)p Fr(\).)24 b(No)o(w)16 b(from)f(the)i(structure)g(of)f(normal)g(deriv)m (ations)i(in)g(the)e(system)h(of)-12 1966 y(prop)q(ositional)h(logic)f (consisting)h(of)e(in)o(tro)q(duction)i(and)f(elimination)h(rules)g (for)e Fp(!)h Fr(and)g(!)f(it)h(follo)o(ws)g(\(cf.)e([18,)-12 2023 y(p.84]\))f(that)g Fq(\033)g Fp(!)f Fq(\034)20 b Fr(either)15 b(o)q(ccurs)h(p)q(ositiv)o(ely)g(in)g(the)f(t)o(yp)q(e)f (of)h Fi(nf)s Fr(\()p Fq(t)p Fr(\),)g(or)f(else)i(negativ)o(ely)f(in)h (the)f(t)o(yp)q(e)g(of)f(one)-12 2079 y(of)i(the)g(constan)o(ts)g(or)f (free)i(v)m(ariables)g(of)f Fi(nf)t Fr(\()p Fq(t)p Fr(\).)22 b(The)17 b(former)f(is)g(imp)q(ossible)j(since)e Fq(t)g Fr(is)g(of)e(ground)i(t)o(yp)q(e,)f(and)-12 2136 y(the)f(latter)g(b)o (y)g(insp)q(ection)j(of)c(the)i(t)o(yp)q(es)f(of)g(the)g(constan)o(ts.) p 1919 2108 V 1919 2134 2 26 v 1937 2134 V 1919 2136 19 2 v 38 2231 a(No)o(w)h(if)g(a)g Fo(normal)21 b Fr(ground)16 b(t)o(yp)q(e)g(term)g(with)h(only)f(ground)h(free)f(v)m(ariables)h (satis\014es)g(\(A\),)e(then)i(for)e(ev)o(ery)-12 2288 y(subterm)c Fq(\025x:s)f Fr(with)h Fq(x)g Fr(higher)g(t)o(yp)q(e)g (\(and)g(hence)h(safe\),)e(the)h(v)m(ariable)h Fq(x)f Fr(is)g(a\016nable)g(in)h Fq(s)f Fr(\(since)h(eac)o(h)e(reduct)i(of)-12 2344 y Fq(s)f Fr(is)h Fq(s)f Fr(itself)t(\).)19 b(Therefore)11 b(b)o(y)g(rep)q(eated)g(ground)g(t)o(yp)q(e)g Fq(\014)i Fr(expansions,)g(view)o(ed)f(as)e(a)h(kind)h(of)f(sharing)g(construct,) -12 2400 y(w)o(e)18 b(can)h(obtain)f(an)g(equiv)m(alen)o(t)i(term)e (con)o(taining)h(eac)o(h)f(higher)i(t)o(yp)q(e)e(v)m(ariable)i(at)d (most)h(once:)26 b(if)19 b(e.g.)e Fq(s)i Fr(is)-12 2457 y Fq(:)8 b(:)g(:)e(a)i(:)g(:)g(:)d(a)j(:)g(:)g(:)20 b Fr(with)c Fq(a)f Fr(an)g(a\016nation)g(of)g Fq(x)g Fr(in)h Fq(s)p Fr(,)f(replace)h Fq(\025x:)8 b(:)g(:)g(:)d(a)j(:)g(:)g(:)d(a)j (:)g(:)g(:)20 b Fr(b)o(y)15 b Fq(\025x:)p Fr(\()p Fq(\025y)1536 2440 y Fn(\023)1549 2457 y Fq(:)8 b(:)g(:)g(:)d(y)10 b(:)e(:)g(:)d(y)10 b(:)e(:)g(:)d Fr(\))p Fq(a)p Fr(.)-12 2534 y Fm(Lemma)18 b(4.2)f(\(Sharing\).)23 b Fo(L)n(et)g Fq(t)g Fo(b)n(e)g(a)h(term)f(such)h(that)g(for)f(every)g(subterm)h Fq(\025x:s)f Fo(with)g Fq(x)h Fo(higher-typ)n(e)-12 2591 y(inc)n(omplete,)e(the)g(variable)g Fq(x)f Fo(is)h(a\016nable)f(in)g Fq(s)p Fo(.)37 b(Then)21 b(by)h(r)n(ep)n(e)n(ate)n(d)f Fq(\014)1308 2598 y Fn(\023)1322 2591 y Fo(-exp)n(ansions)g Fq(r)q Fr([)p Fq(a=y)1678 2574 y Fn(\023)1691 2591 y Fr(])h Fp(7!)h Fr(\()p Fq(\025y)r(:r)q Fr(\))p Fq(a)-12 2647 y Fo(one)17 b(c)n(an)f(c)n(onstruct)g(a)h(term)g Fq(\014)r Fr(\()p Fq(t)p Fr(\))f Fo(fr)n(om)h Fq(t)g Fr(\()p Fo(henc)n(e)e Fq(\014)r Fr(\()p Fq(t)p Fr(\))e Fp(\000)-7 b(!)1051 2631 y Fv(\003)1085 2647 y Fq(t)p Fr(\))17 b Fo(such)f(that)i(for)f(every)f(subterm)h Fq(\025x:s)f Fo(in)g Fq(\014)r Fr(\()p Fq(t)p Fr(\))-12 2704 y Fo(with)h Fq(x)f Fo(higher-typ)n(e)h(inc)n(omplete,)f Fi(F)o(O)p Fr(\()p Fq(x;)8 b(s)p Fr(\))j Fp(\024)i Fr(1)p Fo(.)952 2828 y Fr(6)p eop %%Page: 7 7 7 6 bop -12 199 a Fo(Pr)n(o)n(of.)23 b Fr(By)12 b(induction)i(on)e(the) g(n)o(um)o(b)q(er)h(of)f(o)q(ccurrences)h(of)f(b)q(ound)h(higher-t)o (yp)q(e)g(incomplete)h(v)m(ariables.)20 b(Con-)-12 256 y(sider)c(an)g(outermost)e(subterm)i Fq(\025x:r)f Fr(with)h Fq(x)f Fr(higher-t)o(yp)q(e)i(incomplete)g(and)f Fi(F)o(O)p Fr(\()p Fq(x;)8 b(r)q Fr(\))j Fp(\025)j Fr(2.)20 b(By)c(assumption)-12 312 y Fq(x)f Fr(has)g(an)g(a\016nation)g Fq(a)g Fr(in)h Fq(r)q Fr(.)k(Let)15 b Fq(u)g Fr(b)q(e)h(the)f(minimal)i(subterm)e(of)f Fq(r)i Fr(suc)o(h)g(that)e Fq(u)h Fr(con)o(tains)g(all)h(o)q (ccurrences)-12 369 y(of)f Fq(a)g Fr(in)h Fq(r)q Fr(.)k(No)o(w)14 b(let)i Fq(t)372 352 y Fv(0)399 369 y Fr(result)g(from)e Fq(t)i Fr(b)o(y)f(replacing)i Fq(u)e Fr(with)g(\()p Fq(\025y)r(:u)p Fr([)p Fq(y)r(=a)p Fr(])n(\))p Fq(a)g Fr(for)f(some)h(new)h(v)m (ariable)g Fq(y)r Fr(.)1811 352 y Fl(2)38 433 y Fr(T)l(o)j(apply)h(the) f(induction)i(h)o(yp)q(othesis)f(to)e Fq(t)829 416 y Fv(0)841 433 y Fr(,)i(one)f(m)o(ust)f(sho)o(w)h(that)f(ev)o(ery)h (a\016nation)g(in)h Fq(t)f Fr(inside)i Fq(\025x:r)-12 489 y Fr(results)c(in)g(an)g(a\016nation)f(in)i Fq(t)527 473 y Fv(0)539 489 y Fr(.)24 b(T)l(o)16 b(see)h(this,)g(let)g Fq(\025z)r(:s)f Fr(b)q(e)h(a)f(subterm)h(of)f Fq(r)h Fr(suc)o(h)g(that)f Fq(z)i Fr(has)f(an)f(a\016nation)-12 546 y Fq(b)k Fr(in)g Fq(s)p Fr(.)35 b(If)20 b Fq(a)g Fr(has)f(no)h(o)q(ccurrence)h(in)g Fq(s)p Fr(,)g(then)f Fq(b)f Fr(is)i(still)g(an)f(a\016nation)g(of)f Fq(z)j Fr(in)f Fq(t)1484 529 y Fv(0)1496 546 y Fr(.)34 b(Otherwise)21 b(b)o(y)f(scop)q(e)-12 602 y(equiv)m(alence,)d(either)e(all)g(o)q (ccurrences)g(of)e Fq(a)i Fr(are)e(in)i Fq(s)g Fr(and)f Fq(z)h Fp(2)e Fi(FV)p Fr(\()p Fq(a)p Fr(\),)h(or)f(else)i(no)f(o)q (ccurrence)h(of)f Fq(a)g Fr(in)h Fq(s)g Fr(has)e(a)-12 658 y(free)g(o)q(ccurrence)h(of)f Fq(z)r Fr(.)19 b(In)14 b(the)f(latter)g(case,)g(either)g Fq(a)g Fr(o)q(ccurs)h(in)g Fq(b)p Fr(,)e(in)i(whic)o(h)g(case)f Fq(b)p Fr([)p Fq(y)r(=a)p Fr(])e(is)j(an)f(a\016nation)f(of)h Fq(z)-12 715 y Fr(in)h Fq(t)55 698 y Fv(0)67 715 y Fr(,)g(or)e(else)i Fq(a;)8 b(b)k Fr(are)h(separated,)g(in)h(whic)o(h)g(case)g Fq(b)e Fr(is)i(still)h(an)e(a\016nation)g(of)g Fq(z)i Fr(in)f Fq(t)1449 698 y Fv(0)1461 715 y Fr(.)19 b(In)14 b(the)f(former)g(case,) g(the)-12 771 y(minimalit)o(y)j(of)e Fq(u)g Fr(implies)i(that)e Fq(u)g Fr(is)h(in)g Fq(s)p Fr(.)20 b(By)14 b(construction)h Fq(t)1096 755 y Fv(0)1122 771 y Fr(results)g(from)e Fq(t)i Fr(b)o(y)f(replacing)i(the)e(subterm)g Fq(u)-12 828 y Fr(of)g Fq(s)g Fr(with)h(\()p Fq(\025y)r(:u)p Fr([)p Fq(y)r(=a)p Fr(])m(\))p Fq(a)f Fr(for)f(some)h(new)h Fq(y)r Fr(.)k(Since)d Fq(z)g Fr(has)e(a)f(free)i(o)q(ccurrence)g(in)g (b)q(oth)f Fq(a)g Fr(and)g Fq(b)p Fr(,)g(there)g(are)f(t)o(w)o(o)-12 884 y(cases.)22 b(If)17 b Fq(a)f Fr(is)g(a)g(subterm)g(of)f Fq(b)p Fr(,)h(then)g(eac)o(h)g(o)q(ccurrence)h(of)f Fq(b)f Fr(con)o(tains)h(exactly)h(one)f(o)q(ccurrence)h(of)e Fq(a)p Fr(,)h(for)g Fq(b)-12 941 y Fr(is)f(an)g(a\016nation)f(of)g Fq(z)j Fr(in)e Fq(s)p Fr(.)20 b(By)15 b(construction)g(it)g(follo)o(ws) f(that)g Fq(a)h Fr(is)g(an)f(a\016nation)g(of)h Fq(z)h Fr(in)g Fq(t)1619 924 y Fv(0)1631 941 y Fr(.)j(Otherwise)d(if)f Fq(b)-12 997 y Fr(is)h(a)f(subterm)g(of)g Fq(a)p Fr(,)f(then)i(b)o(y)f (construction)h Fq(b)e Fr(is)i(still)h(an)e(a\016nation)g(of)g Fq(z)i Fr(in)f Fq(t)1373 981 y Fv(0)1385 997 y Fr(.)p 1919 970 19 2 v 1919 996 2 26 v 1937 996 V 1919 998 19 2 v 38 1098 a(This)k(migh)o(t)f(motiv)m(ate)g(wh)o(y)g(it)g(will)i(b)q (e)f(useful)g(to)e(consider)i(a)f(subset)h(of)e(the)i(set)e(of)h(RA)q (-terms,)g(to)f(b)q(e)-12 1154 y(called)f(RS)q(-terms,)d(where)i(S)f (stands)g(for)f Fo(sharing)p Fr(.)-12 1245 y Fm(De\014nition.)24 b Fr(An)16 b(RA-term)f(is)h(an)f(RS)q Fo(-term)k Fr(if)c(it)h(has)f (safe)g(or)g(ground)g(v)m(ariables)h(only)l(,)g(and)38 1309 y(\(S\))f(ev)o(ery)g(higher)h(t)o(yp)q(e)f(v)m(ariable)i(o)q (ccurs)e(at)g(most)f(once.)38 1407 y(Ev)o(ery)20 b(RS-term)g Fq(t)h Fr(can)f(b)q(e)h(written)f(uniquely)i(in)f Fo(he)n(ad)g(form)p Fr(,)h(b)q(eing)f(of)f(the)g(form)g Fq(U)t(~)-22 b(r)p Fr(,)21 b(where)g Fq(U)k Fr(is)20 b(a)-12 1463 y(v)m(ariable,)e(a)e (constan)o(t,)g(!)p Fq(s)g Fr(or)g Fq(s\024)p Fr(;)i(or)e(else)h Fq(U)22 b Fr(is)17 b Fq(\025x:s)f Fr(with)h Fi(F)o(O)p Fr(\()p Fq(x;)8 b(s)p Fr(\))14 b Fp(\024)h Fr(1,)h(or)g Fq(U)22 b Fr(is)17 b Fq(\025x:s)f Fr(with)g Fi(F)o(O)p Fr(\()p Fq(x;)8 b(s)p Fr(\))14 b Fq(>)h Fr(1)-12 1520 y(and)i Fq(x)g Fr(ground.)25 b(Call)16 b Fq(~)-21 b(r)q Fr(,)17 b Fq(s)p Fr(,)g Fq(x)p Fr(,)g(and)g Fq(U)22 b Fr(the)17 b Fo(c)n(omp)n(onents)i Fr(of)e Fq(t)p Fr(.)25 b(Comp)q(onen)o(ts)17 b(are)f(sp)q(eci\014ed)j(b)o(y)e(n)o(um)o(b)q (ering)-12 1576 y(them)g(in)g(order)f(from)g(left)h(to)f(righ)o(t.)23 b(A)17 b Fo(gener)n(al)f(term)i(formation)i Fr(is)d(an)g(op)q(eration)f (on)h(terms,)f(resulting)h(in)-12 1633 y(the)e(formation)f(of)g(a)g (term)h Fq(t)n(~)-21 b(v)r Fr(,)14 b(\()p Fq(t\024)p Fr(\))n Fq(~)-21 b(v)r Fr(,)14 b(\(!)p Fq(t)p Fr(\))n Fq(~)-21 b(v)q Fr(,)14 b(\()p Fq(\025x:t)p Fr(\))n Fq(~)-21 b(v)q Fr(,)14 b(or)g(\()p Fq(t)p Fr([)p Fq(s=x)p Fr(]\))n Fq(~)-21 b(v)q Fr(,)14 b(where)h Fq(t)p Fr(,)g Fq(x)g Fr(and)g Fq(s)f Fr(are)h(an)o(y)f(comp)q(onen)o(ts)-12 1689 y(of)h(the)g(giv)o(en)h(terms)f(and)e Fq(~)-21 b(v)17 b Fr(are)e(optional)g(trailing)i(comp)q(onen)o(ts)e(of)g(one)g(of)g (the)g(giv)o(en)h(terms.)38 1753 y(The)h(algorithms)g Fi(nf)j Fr(and)d Fi(rf)i Fr(describ)q(ed)g(b)q(elo)o(w)e(use)g(a)g (register)g(mac)o(hine)g(mo)q(del)h(of)e(computation,)h(where)-12 1809 y(eac)o(h)c(register)h(ma)o(y)e(con)o(tain)h(a)g(term.)19 b(One)14 b(has)f(an)g(unlimited)i(supply)g(of)d(registers)h Fq(u)p Fr(,)h Fq(v)r Fr(,)e Fq(w)i Fr(etc.)20 b(A)13 b(primitiv)o(e)-12 1866 y(computation)e Fo(step)j Fr(is)e(an)o(y)f(of)g (the)g(follo)o(wing)h(op)q(erations:)19 b(cop)o(ying)11 b(from)g(one)g(register)h(to)e(another;)i(allo)q(cation)-12 1922 y(of)18 b(a)f(new)i(register)f(and)g(initializi)q(ng)i(it)f(to)e (con)o(tain)h(a)g(constan)o(t)f(or)h(a)f(new)i(v)m(ariable;)h(renaming) f(of)e(all)i(free)-12 1979 y(and)c(b)q(ound)h(v)m(ariables)g(sim)o (ultaneously;)g(test)f(on)f(the)h(head)h(form)e(and)h(branc)o(h;)g (test)f(on)h(the)g(head)g(form)f(and)-12 2035 y(p)q(erform)h(a)g (general)h(term)e(formation.)38 2099 y(In)h(particular,)f(eac)o(h)g(of) g(the)g(follo)o(wing)h(tak)o(es)e(one)h(primitiv)o(e)i(step:)j(test)13 b(on)h(the)g(head)h(form)e(of)h Fq(t)g Fr(and)g(cop)o(y)-12 2156 y(an)o(y)i(comp)q(onen)o(t)g(of)g Fq(t)g Fr(in)o(to)g(a)g (register;)g(test)g(on)g(\()p Fq(\025x:s)p Fr(\))p Fq(r~)-22 b(r)15 b Fr(with)i Fi(F)o(O)p Fr(\()p Fq(x;)8 b(s)p Fr(\))13 b Fq(>)h Fr(1)i(and)g(formation)g(of)f Fq(r)i Fr(and)f Fq(s)o(~)-22 b(r)r Fr(;)-12 2212 y(test)17 b(on)f(\()p Fq(\025x:s)p Fr(\))p Fq(r~)-22 b(r)17 b Fr(with)g Fi(F)o(O)p Fr(\()p Fq(x;)8 b(s)p Fr(\))14 b Fp(\024)i Fr(1)h(and)g(form)f(the)h (term)f Fq(s)p Fr([)p Fq(r)q(=x)p Fr(])n Fq(~)-21 b(r)p Fr(;)18 b(test)e(on)h Fm(c)1435 2219 y Fn(\033)1459 2212 y Fq(t)1475 2219 y Fl(1)1495 2212 y Fq(t)1511 2219 y Fl(2)1531 2212 y Fq(t)1547 2219 y Fl(3)1567 2212 y Fq(t)1583 2219 y Fl(4)1602 2212 y Fq(~)-22 b(r)q Fr(,)17 b(and)g(formation)-12 2269 y(of)e Fq(t)56 2276 y Fl(1)91 2269 y Fr(and)h Fq(t)196 2276 y Fn(j)213 2269 y Fq(~)-22 b(r)16 b Fr(for)f(some)g Fq(j)g Fp(2)e(f)p Fr(2)p Fq(;)8 b Fr(3)p Fq(;)g Fr(4)p Fp(g)p Fr(;)j(test)k(on)g(\(!)p Fq(s)p Fr(\))p Fq(\024)o(~)-22 b(r)p Fr(,)15 b(and)h(form)e(the)h(term)g Fq(s)o(~)-22 b(r)q Fr(.)38 2333 y(It)15 b(can)g(b)q(e)g(easily)h(seen)g(that)e (these)h(op)q(erations)g(can)g(b)q(e)h(sim)o(ulated)f(b)o(y)g(a)g(T)l (uring)g(mac)o(hine)h(in)f(p)q(olynomial)-12 2389 y(time)h(\(cf.)e (e.g.)h([5)o(]\).)38 2453 y(One)k(asso)q(ciates)e(a)h(unique)h Fo(envir)n(onment)f(r)n(e)n(gister)j Fq(u)996 2460 y Fn(x)1036 2453 y Fr(with)d(eac)o(h)g(v)m(ariable)i Fq(x)p Fr(.)27 b(A)18 b Fo(numer)n(al)23 b Fr(is)18 b(a)g(binary)-12 2510 y(n)o(umeral)i(preceeded)g(b)o(y)f(an)o(y)g(n)o(um)o(b)q(er)g(of)g (!'s.)30 b(An)19 b Fo(envir)n(onment)j Fr(is)e(a)e(list)h Fq(~)-22 b(n)p Fr(;)7 b Fq(~)-22 b(x)18 b Fr(:=)h Fq(n)1554 2517 y Fl(1)1574 2510 y Fq(;)8 b(:)g(:)g(:)d(;)j(n)1703 2517 y Fn(k)1724 2510 y Fr(;)g Fq(x)1771 2517 y Fl(1)1790 2510 y Fq(;)g(:)g(:)g(:)d(;)j(x)1918 2517 y Fn(k)-12 2566 y Fr(where)18 b(eac)o(h)g Fq(n)254 2573 y Fn(i)286 2566 y Fr(is)g(an)g(RS)q(-term)f(of)g(the)h(same)g(t)o(yp)q(e)f(as)h Fq(x)1026 2573 y Fn(i)1040 2566 y Fr(.)27 b(A)18 b Fo(numer)n(al)g (envir)n(onment)j Fr(is)d(an)g(en)o(vironmen)o(t)-13 2623 y Fq(~)-22 b(n)p Fr(;)7 b Fq(~)-22 b(x)15 b Fr(suc)o(h)g(that)g (eac)o(h)g Fq(n)407 2630 y Fn(i)437 2623 y Fr(is)g(a)g(n)o(umeral.)p -12 2661 780 2 v 40 2688 a Fh(2)57 2704 y Fj(W)m(e)e(write)h Fb(u)p Fj([)p Fb(y)q(=a)p Fj(])f(for)f Fb(u)h Fj(with)h(all)g(o)q (ccurrences)g(of)f Fb(a)g Fj(sim)o(ultaneousl)q(y)j(replaced)f(b)o(y)e Fb(y)q Fj(.)952 2828 y Fr(7)p eop %%Page: 8 8 8 7 bop -12 199 a Fm(Theorem)17 b(4.3.)22 b Fo(F)m(or)13 b(every)h Fp(R)p Fo(-fr)n(e)n(e)f Fr(RS)q Fo(-term)h Fq(t)g Fo(of)g(gr)n(ound)g(typ)n(e)f(and)h(numer)n(al)f(envir)n(onment) e Fq(~)-21 b(n)p Fr(;)7 b Fq(~)-22 b(x)13 b Fo(such)h(that)-12 256 y Fi(FV)q Fr(\()p Fq(t)p Fr(\))e Fp(\022)h Fq(~)-23 b(x)p Fo(,)38 320 y Fr(\()p Fq(i)p Fr(\))15 b Fo(one)h(c)n(an)g(c)n (ompute)h Fi(nf)s Fr(\()p Fq(t)p Fr([)o Fq(~)-22 b(n=)o(~)g(x)p Fr(]\))16 b Fo(in)f(at)i(most)f Fr(2)p Fp(j)p Fq(t)p Fp(j)g Fo(steps,)38 385 y Fr(\()p Fq(ii)p Fr(\))f Fo(the)h(numb)n(er)g (of)h(use)n(d)f(r)n(e)n(gisters)f(is)h Fp(\024)d(j)p Fq(t)p Fp(j)c Fr(+)i(#)o Fq(~)-22 b(n)p Fo(,)16 b(and)38 450 y Fr(\()p Fq(iii)p Fr(\))f Fo(every)h(term)g Fq(s)h Fo(o)n(c)n(curring)f(in)g(the)g(c)n(omputation)h(satis\014es)e Fp(j)p Fq(s)p Fp(j)d(\024)h(j)p Fq(t)p Fp(j)d Fr(+)g(max)d Fp(j)p Fq(n)1500 457 y Fn(i)1514 450 y Fp(j)p Fo(.)-12 552 y(Pr)n(o)n(of.)23 b Fr(W)l(e)17 b(describ)q(e)i(the)e(algorithm)g Fi(nf)s Fr(,)g(whic)o(h)h(at)f(input)h Fq(t;)6 b(~)-21 b(n)p Fr(;)7 b Fq(~)-22 b(x)16 b Fr(outputs)h Fi(nf)s Fr(\()p Fq(t;)6 b(~)-21 b(n)p Fr(;)7 b Fq(~)-22 b(x)o Fr(\))15 b(=)i Fi(nf)s Fr(\()p Fq(t)p Fr([)o Fq(~)-22 b(n=)o(~)g(x)p Fr(])o(\))17 b(in)h(the)-12 609 y(input)g(register)f(of) g Fq(t)p Fr(,)g(b)o(y)g(induction)i(on)e Fp(j)p Fq(t)p Fp(j)p Fr(.)26 b(F)l(or)16 b(t)o(yp)q(e)h(reasons,)g Fq(t)g Fr(is)h(of)e(the)i(form)e Fq(U)t(~)-22 b(r)18 b Fr(where)f Fq(U)22 b Fr(is)c(either)f(a)-12 665 y(v)m(ariable)e (among)e Fq(~)-23 b(x)14 b Fr(or)f(a)g(constan)o(t)g(or)g(!,)g(or)g (else)i Fq(U)k Fr(is)14 b(\()p Fq(\025x:s)p Fr(\))p Fq(r)q Fr(,)e(where)i Fi(F)o(O)p Fr(\()p Fq(x;)8 b(s)p Fr(\))j Fp(\024)i Fr(1)h(or)f Fq(x)g Fr(is)i(of)e(ground)g(t)o(yp)q(e.)38 730 y(If)i Fq(t)h Fr(is)g Fm(0)p Fr(,)f(then)g(output)g Fm(0)p Fr(.)20 b(W)l(e)15 b(ha)o(v)o(e)g(p)q(erformed)h(t)o(w)o(o)d (steps,)i(and)h(\(ii\),)f(\(iii\))h(are)f(ob)o(vious.)38 795 y(If)k Fq(t)g Fr(is)h Fq(x)198 802 y Fn(i)212 795 y Fq(\024)8 b Fp(\001)g(\001)g(\001)d Fq(\024)19 b Fr(with)g Fq(k)h Fr(o)q(ccurrences)g(of)e Fq(\024)p Fr(,)i(then)f(delete)h Fq(k)f Fr(leading)i(!'s)d(from)g(the)g(con)o(ten)o(t)h(of)f Fq(u)1811 802 y Fn(x)1831 807 y Fe(i)1865 795 y Fr(and)-12 851 y(output)e(the)g(resulting)h(n)o(umeral.)22 b(W)l(e)16 b(ha)o(v)o(e)f(p)q(erformed)h Fq(k)c Fr(+)f(2)i Fp(\024)h Fr(2)p Fp(j)p Fq(t)p Fp(j)h Fr(steps,)h(using)g(2)e Fp(\024)g(j)p Fq(t)p Fp(j)c Fr(+)h(#)o Fq(~)-22 b(n)16 b Fr(registers,)-12 907 y(and)g(\(iii\))g(is)g(ob)o(vious.)38 972 y(If)k Fq(t)h Fr(is)f Fq(U)5 b(r)21 b Fr(where)g Fq(U)k Fr(is)20 b(a)g(sym)o(b)q(ol)g Fm(s)720 979 y Fl(1)740 972 y Fq(;)8 b Fr(!,)19 b(\014rst)h(compute)g Fq(n)h Fr(:=)g Fi(nf)t Fr(\()p Fq(r)o(;)6 b(~)-21 b(n)n Fr(;)7 b Fq(~)-22 b(x)o Fr(\),)21 b(then)f(form)g Fq(U)5 b(n)p Fr(.)34 b(W)l(e)21 b(ha)o(v)o(e)-12 1029 y(p)q(erformed)16 b Fp(\024)d Fr(2)c(+)i(2)p Fp(j)p Fq(r)q Fp(j)g(\024)i Fr(2)p Fp(j)p Fq(t)p Fp(j)i Fr(steps,)g(using)g Fp(\024)e Fr(1)d(+)h Fp(j)p Fq(r)q Fp(j)e Fr(+)h(#)o Fq(~)-22 b(n)13 b Fp(\024)g(j)p Fq(t)p Fp(j)d Fr(+)g(#)o Fq(~)-22 b(n)16 b Fr(registers,)e(and)i(\(iii\))g (follo)o(ws.)38 1093 y(If)h Fq(t)g Fr(is)g Fm(s)186 1100 y Fl(0)205 1093 y Fq(r)q Fr(,)g(\014rst)f(compute)h Fq(n)e Fr(:=)g Fi(nf)t Fr(\()p Fq(r)o(;)6 b(~)-21 b(n)n Fr(;)7 b Fq(~)-22 b(x)o Fr(\),)17 b(then)g(output)f Fm(0)h Fr(if)g Fq(n)e Fr(=)h Fm(0)p Fr(,)g(otherwise)h(form)f Fm(s)1685 1100 y Fl(0)1704 1093 y Fq(n)p Fr(.)25 b(W)l(e)17 b(ha)o(v)o(e)-12 1150 y(p)q(erformed)g Fp(\024)e Fr(3)c(+)g(2)p Fp(j)p Fq(r)q Fp(j)j(\024)h Fr(2)p Fp(j)p Fq(t)p Fp(j)h Fr(steps,)g(using)i Fp(\024)d Fr(1)c(+)g Fp(j)p Fq(r)q Fp(j)f Fr(+)h(#)o Fq(~)-22 b(n)16 b Fp(\024)f(j)p Fq(t)p Fp(j)10 b Fr(+)i(#)o Fq(~)-22 b(n)16 b Fr(registers.)24 b(As)17 b(for)f(\(iii\),)h(observ)o (e)-12 1206 y Fp(j)p Fm(s)22 1213 y Fl(0)41 1206 y Fq(n)p Fp(j)c(\024)g Fr(2)c(+)i Fp(j)p Fq(r)q Fp(j)e Fr(+)i(max)c Fp(j)p Fq(n)455 1213 y Fn(i)469 1206 y Fp(j)12 b Fr(=)h Fp(j)p Fq(t)p Fp(j)d Fr(+)g(max)d Fp(j)p Fq(n)771 1213 y Fn(i)785 1206 y Fp(j)p Fr(.)38 1271 y(Similarly)l(,)17 b(if)f Fq(t)f Fr(is)h Fm(p)p Fq(r)q Fr(,)f(\014rst)f(compute)i Fq(n)d Fr(:=)f Fi(nf)t Fr(\()p Fq(r)o(;)6 b(~)-21 b(n)n Fr(;)7 b Fq(~)-22 b(x)o Fr(\),)15 b(then)g(form)g Fq(n)1271 1255 y Fv(0)1298 1271 y Fr(if)h Fq(n)d Fr(=)g Fm(s)1449 1278 y Fn(i)1462 1271 y Fq(n)1489 1255 y Fv(0)1501 1271 y Fr(,)i(else)h(output)f Fm(0)p Fr(.)38 1336 y(If)i Fq(t)f Fr(is)h(\(!)p Fq(s)p Fr(\))p Fq(\024)o(~)-22 b(r)q Fr(,)16 b(compute)g Fi(nf)t Fr(\()p Fq(s)o(~)-22 b(r)q(;)6 b(~)-21 b(n)o Fr(;)7 b Fq(~)-22 b(x)o Fr(\),)16 b(in)h Fp(\024)e Fr(4)c(+)g(2)p Fp(j)p Fq(s)o(~)-22 b(r)q Fp(j)14 b(\024)h Fr(2)p Fp(j)p Fq(t)p Fp(j)g Fr(steps,)i(using)g Fp(\024)e(j)p Fq(s)o(~)-22 b(r)p Fp(j)11 b Fr(+)g(#)o Fq(~)-22 b(n)17 b Fr(registers.)23 b(\(iii\))-12 1392 y(follo)o(ws)15 b(directly)i(from)d(the)i(induction)h(h)o(yp)q(othesis)f(on)f Fq(s)o(~)-22 b(r)q Fr(.)38 1457 y(If)19 b Fq(t)f Fr(is)h Fm(c)193 1464 y Fn(\033)217 1457 y Fq(t)233 1464 y Fl(1)253 1457 y Fq(t)269 1464 y Fl(2)289 1457 y Fq(t)305 1464 y Fl(3)325 1457 y Fq(t)341 1464 y Fl(4)360 1457 y Fq(~)-22 b(r)q Fr(,)18 b(\014rst)g(compute)h Fq(n)f Fr(:=)f Fi(nf)t Fr(\()p Fq(t)884 1464 y Fl(1)904 1457 y Fq(;)6 b(~)-21 b(n)o Fr(;)7 b Fq(~)-22 b(x)o Fr(\),)19 b(and)f(then)h(compute)f Fi(nf)t Fr(\()p Fq(t)1507 1464 y Fn(j)1523 1457 y Fq(~)-21 b(r)q(;)6 b(~)-21 b(n)o Fr(;)7 b Fq(~)-22 b(x)o Fr(\))18 b(where)h Fq(j)h Fr(:=)d(2)-12 1513 y(if)i Fq(n)f Fr(=)g Fm(0)p Fr(,)g(and)h Fq(j)h Fr(:=)d Fq(i)12 b Fr(+)g(3)18 b(if)h Fq(n)f Fr(=)g Fm(s)664 1520 y Fn(i)677 1513 y Fq(n)704 1497 y Fv(0)716 1513 y Fr(.)29 b(W)l(e)18 b(ha)o(v)o(e)g(p)q (erformed)h Fp(\024)f Fr(2)11 b(+)i(2)p Fp(j)p Fq(t)1355 1520 y Fl(1)1374 1513 y Fp(j)f Fr(+)g(2)p Fp(j)p Fq(t)1498 1520 y Fn(j)1515 1513 y Fq(~)-22 b(r)q Fp(j)17 b(\024)h Fr(2)p Fp(j)p Fq(t)p Fp(j)g Fr(steps,)g(using)-12 1570 y Fp(\024)13 b Fr(1)d(+)g(max\()p Fp(j)p Fq(t)246 1577 y Fl(1)265 1570 y Fp(j)g Fr(+)h(#)o Fq(~)-22 b(n;)8 b Fp(j)p Fq(t)449 1577 y Fn(j)465 1570 y Fq(~)-22 b(r)q Fp(j)10 b Fr(+)g(#)o Fq(~)-22 b(n)p Fr(\))13 b Fp(\024)g(j)p Fq(t)p Fp(j)c Fr(+)i(#)o Fq(~)-22 b(n)15 b Fr(registers.)20 b(\(iii\))c(follo)o(ws)g(directly)g(from)f(the)g(I.H.)g(on)g Fq(t)1834 1577 y Fn(j)1851 1570 y Fq(~)-21 b(r)p Fr(.)38 1635 y(If)14 b Fq(t)g Fr(is)g(\()p Fq(\025x:s)p Fr(\))p Fq(r~)-22 b(r)12 b Fr(with)i Fi(F)o(O)p Fr(\()p Fq(x;)8 b(s)p Fr(\))k Fq(>)h Fr(1,)g(then)h Fq(x)f Fr(has)g(ground)h(t)o(yp)q (e.)19 b(First)13 b(compute)h Fq(n)f Fr(:=)f Fi(nf)t Fr(\()p Fq(r)o(;)6 b(~)-21 b(n)n Fr(;)7 b Fq(~)-22 b(x)o Fr(\),)14 b(cop)o(y)f Fq(n)-12 1691 y Fr(to)i Fq(u)70 1698 y Fn(x)92 1691 y Fr(,)g(then)g(compute)g Fi(nf)t Fr(\()p Fq(s)o(~)-22 b(r)q(;)6 b(~)-21 b(n)o(;)8 b(n)p Fr(;)f Fq(~)-22 b(x)o(;)8 b(x)p Fr(\).)19 b(Observ)o(e)c(that)g Fq(r)h Fr(is)f(of)g(ground)g(t)o(yp)q(e,)g(and)g Fq(~)-22 b(n;)8 b(n)p Fr(;)f Fq(~)-22 b(x)o(;)8 b(x)14 b Fr(is)i(a)f(n)o(umeral) -12 1748 y(en)o(vironmen)o(t)k(suc)o(h)g(that)f Fi(FV)p Fr(\()p Fq(s)o(~)-22 b(r)q Fr(\))18 b Fp(\022)g Fq(~)-23 b(x;)8 b(x)p Fr(.)29 b(W)l(e)19 b(ha)o(v)o(e)f(p)q(erformed)g Fp(\024)h Fr(2)12 b(+)g(2)p Fp(j)p Fq(r)q Fp(j)g Fr(+)g(2)p Fp(j)p Fq(s)o(~)-22 b(r)q Fp(j)17 b(\024)i Fr(2)p Fp(j)p Fq(t)p Fp(j)f Fr(steps,)g(using)-12 1804 y Fp(\024)e Fr(1)11 b(+)g(max\()p Fp(j)p Fq(r)q Fp(j)f Fr(+)h(#)o Fq(~)-22 b(n;)8 b Fp(j)p Fq(s)o(~)-22 b(r)p Fp(j)11 b Fr(+)g(#)o Fq(~)-22 b(n)12 b Fr(+)f(1\))k Fp(\024)g(j)p Fq(t)p Fp(j)c Fr(+)h(#)o Fq(~)-22 b(n)16 b Fr(registers.)25 b(As)16 b(for)h(\(iii\),)h(observ)o(e)e Fp(j)p Fi(nf)s Fr(\()p Fq(s)o(~)-22 b(r)q(;)6 b(~)-21 b(n)o(;)8 b(n)p Fr(;)f Fq(~)-22 b(x)o(;)8 b(x)p Fr(\))p Fp(j)14 b(\024)-12 1861 y(j)p Fq(s)o(~)-22 b(r)q Fp(j)10 b Fr(+)g(max\()p Fp(j)p Fq(n)255 1868 y Fn(i)268 1861 y Fp(j)p Fq(;)e Fp(j)p Fq(n)p Fp(j)p Fr(\))j Fp(\024)i(j)p Fq(s)o(~)-22 b(r)q Fp(j)9 b Fr(+)i Fp(j)p Fq(r)q Fp(j)e Fr(+)h(max)e Fp(j)p Fq(n)791 1868 y Fn(i)805 1861 y Fp(j)k(\024)h(j)p Fq(t)p Fp(j)d Fr(+)g(max)d Fp(j)p Fq(n)1107 1868 y Fn(i)1121 1861 y Fp(j)p Fr(.)38 1925 y(If)22 b Fq(t)g Fr(is)g(\()p Fq(\025x:s)p Fr(\))p Fq(r~)-22 b(r)20 b Fr(with)i Fi(F)o(O)p Fr(\()p Fq(x;)8 b(s)p Fr(\))22 b Fp(\024)i Fr(1,)e(compute)g Fi(nf)s Fr(\()p Fq(s)p Fr([)p Fq(r)q(=x)p Fr(])m Fq(~)-21 b(r)q(;)6 b(~)-21 b(n)o Fr(;)7 b Fq(~)-22 b(x)o Fr(\).)39 b(Since)22 b Fp(j)p Fq(s)p Fr([)p Fq(r)q(=x)p Fr(])n Fq(~)-22 b(r)q Fp(j)23 b Fq(<)g Fp(j)p Fq(t)p Fp(j)p Fr(,)f(w)o(e)g(ha)o(v)o(e)-12 1982 y(p)q(erformed)16 b Fp(\024)d Fr(1)c(+)i(2)p Fp(j)p Fq(s)p Fr([)p Fq(r)q(=x)p Fr(])m Fq(~)-22 b(r)q Fp(j)12 b(\024)h Fr(2)p Fp(j)p Fq(t)p Fp(j)i Fr(steps,)g(using)h Fp(\024)c(j)p Fq(s)p Fr([)p Fq(r)q(=x)p Fr(])n Fq(~)-22 b(r)q Fp(j)10 b Fr(+)g(#)o Fq(~)-22 b(n)15 b Fr(registers,)g(and)g(\(iii\))i(is)f(ob)o(vious.)p 1919 1955 19 2 v 1919 1980 2 26 v 1937 1980 V 1919 1982 19 2 v -12 2076 a Fm(Corollary)i(4.4)f(\(Base)h(Normalisation\).)24 b Fo(L)n(et)18 b Fq(t)g Fo(b)n(e)g(a)h(close)n(d)e Fp(R)p Fo(-fr)n(e)n(e)g Fr(RS)q Fo(-term)i(of)g(gr)n(ound)f(typ)n(e.)27 b(Then)-12 2132 y(the)21 b(numer)n(al)f Fi(nf)t Fr(\()p Fq(t)p Fr(\))g Fo(c)n(an)g(b)n(e)g(c)n(ompute)n(d)h(in)f(at)g(most)h Fr(2)p Fp(j)p Fq(t)p Fp(j)f Fo(steps)g(using)f Fp(\024)i(j)p Fq(t)p Fp(j)f Fo(r)n(e)n(gisters,)g(and)h(every)f(term)h Fq(s)-12 2188 y Fo(o)n(c)n(curring)16 b(in)g(the)g(c)n(omputation)h (satis\014es)e Fp(j)p Fq(s)p Fp(j)d(\024)h(j)p Fq(t)p Fp(j)p Fo(.)p 1919 2161 V 1919 2187 2 26 v 1937 2187 V 1919 2189 19 2 v 38 2291 a Fr(In)j(order)f(to)f(compute)i Fp(R)p Fr(-free)f(RS-terms)g Fq(t)p Fr(,)g(w)o(e)g(sligh)o(tly)i (generalise)f(the)f(tec)o(hnique)i(ab)q(o)o(v)o(e.)-12 2384 y Fm(Theorem)g(4.5)g(\()p Fp(R)p Fm(-Eliminatio)q(n\).)25 b Fo(L)n(et)19 b Fq(t)g Fo(b)n(e)g(an)g Fr(RS)q Fo(-term)h(of)g(safe)f (or)g(gr)n(ound)h(typ)n(e.)30 b(Ther)n(e)19 b(is)g(a)g(p)n(oly-)-12 2441 y(nomial)h Fq(q)163 2448 y Fn(t)198 2441 y Fo(such)g(that:)29 b(if)19 b Fq(~)-22 b(n)20 b Fo(ar)n(e)g(close)n(d)g(gr)n(ound)g(typ)n (e)g Fp(R)p Fo(-fr)n(e)n(e)f Fr(RS)q Fo(-terms)h(with)g Fi(FV)q Fr(\()p Fq(t)p Fr([)o Fq(~)-22 b(n=)o(~)g(x)p Fr(]\))19 b Fo(al)r(l)h(safe,)g(then)-12 2497 y(one)d(c)n(an)g(c)n (ompute)i(an)e Fp(R)p Fo(-fr)n(e)n(e)g Fr(RS)p Fo(-term)i Fi(rf)r Fr(\()p Fq(t;)6 b(~)-21 b(n)p Fr(;)7 b Fq(~)-22 b(x)o Fr(\))17 b Fo(e)n(quivalent)g(to)h Fq(t)p Fr([)o Fq(~)-22 b(n=)o(~)g(x)p Fr(])17 b Fo(such)h(that)g(the)g(numb)n(er)f (of)h(steps,)-12 2554 y(the)k(numb)n(er)f(of)h(use)n(d)f(r)n(e)n (gisters)f(and)i(the)f(length)g(of)h(every)f(term)h(o)n(c)n(curring)f (in)g(the)h(c)n(omputation)g(al)r(l)f(ar)n(e)-12 2610 y Fp(\024)13 b Fq(q)56 2617 y Fn(t)71 2610 y Fr(\()89 2576 y Fa(P)145 2610 y Fp(j)p Fq(n)185 2617 y Fn(i)199 2610 y Fp(j)p Fr(\))p Fo(.)952 2828 y Fr(8)p eop %%Page: 9 9 9 8 bop -12 199 a Fo(Pr)n(o)n(of.)23 b Fr(By)16 b(induction)i(on)f Fp(j)p Fq(t)p Fp(j)p Fr(.)23 b(Let)17 b Fq(m)d Fr(:=)749 165 y Fa(P)804 199 y Fp(j)p Fq(n)844 206 y Fn(i)858 199 y Fp(j)p Fr(.)24 b(W)l(e)16 b(write)h(#steps)o(,)g(#registers)f(and)h (maxlength)f(for)g(the)-12 256 y(three)j(quan)o(tities)g(ab)q(o)o(v)o (e,)f(and)h(call)h(their)f(maxim)o(um)f Fo(b)n(ound)p Fr(.)30 b(Of)19 b(course,)g(the)f(computed)h(term)f Fi(rf)s Fr(\()p Fq(t;)6 b(~)-21 b(n)o Fr(;)7 b Fq(~)-22 b(x)p Fr(\))-12 312 y(will)17 b(b)q(e)f(suc)o(h)f(that)g(no)g(new)g(free)h(v) m(ariables)g(are)f(pro)q(duced,)h(i.e.)k Fi(FV)q Fr(\()p Fi(rf)r Fr(\()p Fq(t;)6 b(~)-21 b(n)p Fr(;)7 b Fq(~)-22 b(x)o Fr(\)\))12 b Fp(\022)h Fi(FV)q Fr(\()p Fq(t)p Fr([)o Fq(~)-22 b(n=)o(~)g(x)p Fr(]\).)38 377 y(If)17 b Fq(t)g Fr(is)g Fq(\025z)r(:r)q Fr(,)f(then)h(compute)g Fq(r)592 360 y Fv(\003)627 377 y Fr(:=)e Fi(rf)r Fr(\()p Fq(r)o(;)6 b(~)-21 b(n)o Fr(;)7 b Fq(~)-22 b(x)o Fr(\))16 b(and)h(form)f Fq(t)1102 360 y Fv(\003)1137 377 y Fr(:=)g Fq(\025z)r(:r)1286 360 y Fv(\003)1304 377 y Fr(.)25 b(Observ)o(e)17 b(that)f Fq(z)j Fr(and)e Fq(r)g Fr(are)f(safe)-12 433 y(b)q(ecause)g Fq(t)g Fr(has)f(safe)g(t)o(yp)q(e,)g(hence)h Fq(r)q Fr([)o Fq(~)-22 b(n=)o(~)g(x)p Fr(])15 b(has)g(safe)g(free)g(v)m(ariables)h (only)l(.)21 b(By)16 b(the)f(induction)i(h)o(yp)q(othesis)f(the)-12 490 y Fp(R)p Fr(-free)i(RS)q(-term)g Fq(r)340 473 y Fv(\003)378 490 y Fr(is)g(obtained)h(with)g(b)q(ound)g Fq(q)886 497 y Fn(r)905 490 y Fr(\()p Fq(m)p Fr(\).)29 b(Hence)19 b Fq(t)1177 473 y Fv(\003)1215 490 y Fr(is)g(an)f Fp(R)p Fr(-free)g(RS)q(-term)g(obtained)h(with)-12 546 y(b)q(ound)d Fp(j)p Fq(t)p Fp(j)10 b Fr(+)h Fq(q)246 553 y Fn(r)265 546 y Fr(\()p Fq(m)p Fr(\).)38 611 y(If)19 b Fq(t)h Fr(is)f Fq(U)5 b(r)229 618 y Fl(1)256 611 y Fq(:)j(:)g(:)e(r)338 618 y Fn(l)369 611 y Fr(with)20 b Fq(U)k Fr(a)18 b(v)m(ariable)j Fq(y)g Fp(6)p Fr(=)e Fq(x)871 618 y Fn(i)904 611 y Fr(or)g(one)g(of)g (the)g(constan)o(ts)f Fm(0)p Fq(;)8 b Fm(s)1462 618 y Fl(0)1481 611 y Fq(;)g Fm(s)1523 618 y Fl(1)1541 611 y Fq(;)g Fm(p)p Fq(;)g Fm(c)1635 618 y Fn(\033)1657 611 y Fr(,)20 b(then)f(eac)o(h)h Fq(r)1925 618 y Fn(i)-12 667 y Fr(is)f(a)e(safe)h(or)g(ground)g(t)o(yp)q(e)g(term)f(or)h(else)h (is)f Fq(\024)p Fr(.)29 b(Apply)19 b(the)f(induction)i(h)o(yp)q (othesis)f(to)e(all)i(RS)q(-terms)e Fq(r)1866 674 y Fn(i)1898 667 y Fr(to)-12 724 y(obtain)g(suitable)g Fp(R)p Fr(-free)f(RS)q (-terms)g Fq(r)667 707 y Fv(\003)666 737 y Fn(i)700 724 y Fr(:=)f Fi(rf)r Fr(\()p Fq(r)834 731 y Fn(i)847 724 y Fq(;)6 b(~)-21 b(n)p Fr(;)7 b Fq(~)-22 b(x)o Fr(\).)23 b(Then)16 b(form)g Fq(t)1239 707 y Fv(\003)1273 724 y Fr(:=)f Fq(U)5 b(r)1394 707 y Fv(\003)1393 736 y Fl(1)1421 724 y Fq(:)j(:)g(:)d(r)1503 707 y Fv(\003)1502 738 y Fn(l)1539 724 y Fr(and)16 b(rename)g Fq(t)1804 707 y Fv(\003)1841 724 y Fr(so)g(as)-12 780 y(to)e(obtain)h(an)g(RS-term.)20 b(Here)14 b(w)o(e)h(need)g(that)f(the)g Fq(~)-22 b(n)15 b Fr(are)f(closed,)h(for)f(otherwise)h(a)f(free)h(v)m(ariable)h(in)e Fq(~)-22 b(n)15 b Fr(migh)o(t)-12 837 y(b)q(e)h(duplicated,)g(th)o(us)f (violating)g(the)g(\(S\))g(prop)q(ert)o(y)l(.)k(Using)d(the)e (induction)j(h)o(yp)q(othesis,)e Fq(t)1583 820 y Fv(\003)1618 837 y Fr(is)g(obtained)h(with)-12 893 y(b)q(ound)g Fp(j)p Fq(t)p Fp(j)10 b Fr(+)h(1)e(+)304 859 y Fa(P)359 893 y Fq(q)379 900 y Fn(r)395 905 y Fe(i)411 893 y Fr(\()p Fq(m)p Fr(\).)38 958 y(If)21 b Fq(t)g Fr(is)h(\()p Fq(\025x:s)p Fr(\))p Fq(r~)-22 b(r)20 b Fr(with)h Fi(F)o(O)q Fr(\()p Fq(x;)8 b(s)p Fr(\))21 b Fq(>)h Fr(1,)g(then)f Fq(x)g Fr(m)o(ust)f(b)q(e)i(of)e(ground)h(t)o(yp)q(e,)h(since)g Fq(t)g Fr(satis\014es)f(\(S\).)f(W)l(e)-12 1015 y(distinguish)25 b(t)o(w)o(o)c(cases:)35 b(If)23 b Fq(x)g Fr(is)g(safe,)h(w)o(e)e (\014rst)g(rename)h Fq(t)p Fr(,)h(then)f(form)f Fq(r)i Fr(and)e Fq(s)o(~)-22 b(r)24 b Fr(\(in)f(one)g(step\),)h(and)-12 1071 y(compute)19 b Fq(s)197 1054 y Fv(\003)236 1071 y Fr(:=)f Fi(rf)s Fr(\()p Fq(s)o(~)-22 b(r)q(;)6 b(~)-21 b(n)o Fr(;)7 b Fq(~)-22 b(x)o Fr(\))19 b(and)g Fq(r)640 1054 y Fv(\003)678 1071 y Fr(:=)g Fi(rf)r Fr(\()p Fq(r)o(;)6 b(~)-21 b(n)o Fr(;)7 b Fq(~)-22 b(x)o Fr(\).)30 b(Finally)l(,)21 b(w)o(e)e(form)f(\()p Fq(\025x:s)1424 1054 y Fv(\003)1443 1071 y Fr(\))p Fq(r)1483 1054 y Fv(\003)1502 1071 y Fr(,)h(and)g (rename)g(it)g(so)g(as)-12 1127 y(to)h(obtain)h(an)f(RS)q(-term.)35 b(Using)21 b(the)f(induction)i(h)o(yp)q(othesis)f(the)g(result)g(term)f (is)g(obtained)h(with)g(b)q(ound)-12 1184 y Fp(j)p Fq(t)p Fp(j)9 b Fr(+)g(6)f(+)h Fq(q)178 1192 y Fn(s)o(~)-17 b(r)214 1184 y Fr(\()p Fq(m)p Fr(\))8 b(+)h Fq(q)362 1191 y Fn(r)381 1184 y Fr(\()p Fq(m)p Fr(\).)19 b(Otherwise)c(if)g Fq(x)g Fr(is)g(complete,)g(\014rst)f(form)g Fq(r)h Fr(and)g Fq(s)o(~)-22 b(r)15 b Fr(\(in)g(one)g(step\))f(and)h(compute)-12 1240 y Fq(n)j Fr(:=)f Fi(rf)s Fr(\()p Fq(r)o(;)6 b(~)-21 b(n)n Fr(;)7 b Fq(~)-22 b(x)o Fr(\),)18 b(then)h(cop)o(y)e Fq(n)i Fr(to)e Fq(u)655 1247 y Fn(x)695 1240 y Fr(and)h(compute)g Fi(rf)s Fr(\()p Fq(s)o(~)-22 b(r)q(;)6 b(~)-21 b(n)o(;)8 b(n)p Fr(;)f Fq(~)-22 b(x)o(;)8 b(x)p Fr(\).)27 b(Using)18 b(the)h(induction)g(h)o(yp)q(othesis)-12 1297 y(the)c(result)h(term)f (is)h(obtained)f(with)h(b)q(ound)g(is)g Fp(j)p Fq(t)p Fp(j)10 b Fr(+)g Fq(q)941 1304 y Fn(r)960 1297 y Fr(\()p Fq(m)p Fr(\))g(+)g Fq(q)1111 1305 y Fn(s)o(~)-17 b(r)1147 1297 y Fr(\()p Fq(m)9 b Fr(+)i Fq(q)1280 1304 y Fn(r)1299 1297 y Fr(\()p Fq(m)p Fr(\)\).)38 1362 y(If)j Fq(t)g Fr(is)h(\()p Fq(\025x:s)p Fr(\))p Fq(r~)-22 b(r)13 b Fr(with)h Fi(F)o(O)p Fr(\()p Fq(x;)8 b(s)p Fr(\))k Fp(\024)h Fr(1,)g(form)g Fq(t)831 1345 y Fv(0)856 1362 y Fr(:=)g Fq(s)p Fr([)p Fq(r)q(=x)p Fr(])m Fq(~)-21 b(r)14 b Fr(\(in)h(one)f (step\))f(and)h(compute)h Fi(rf)r Fr(\()p Fq(t)1670 1345 y Fv(0)1682 1362 y Fq(;)6 b(~)-21 b(n)o Fr(;)7 b Fq(~)-22 b(x)o Fr(\).)20 b(Using)-12 1418 y(the)15 b(induction)i(h)o(yp)q (othesis)f(the)g(result)f(term)g(is)h(obtained)g(with)f(b)q(ound)h Fp(j)p Fq(t)p Fp(j)10 b Fr(+)h Fq(q)1400 1426 y Fn(t)1413 1416 y Fk(0)1426 1418 y Fr(\()p Fq(m)p Fr(\).)38 1483 y(The)k(case)h(\(!)p Fq(s)p Fr(\))p Fq(\024)o(~)-22 b(r)15 b Fr(is)h(treated)e(similarly)j(to)e(the)g(previous)h(case,)f(and)g (the)h(case)f Fq(t)e Fr(=)g Fq(x)1538 1490 y Fn(i)1567 1483 y Fr(is)j(ob)o(vious.)38 1548 y(Because)h Fq(t)g Fr(is)f(safe,)g(the)h(only)f(remaining)i(case)e(is)h(where)f Fq(t)h Fr(is)g(of)f(the)g(form)f Fp(R)p Fq(g)r(hnr)1523 1555 y Fl(1)1550 1548 y Fq(:)8 b(:)g(:)d(r)1631 1555 y Fn(l)1644 1548 y Fr(.)23 b(Then)16 b(w)o(e)g(will)-12 1604 y(output)f(a)g(renamed)h(v)o(ersion)f(of)g(the)g(term)652 1706 y(\()p Fq(T)697 1713 y Fl(0)716 1706 y Fr(\()p Fq(T)761 1713 y Fl(1)788 1706 y Fq(:)8 b(:)g(:)d Fr(\()p Fq(T)893 1713 y Fn(k)q Fv(\000)p Fl(1)959 1706 y Fq(g)983 1687 y Fv(\003)1002 1706 y Fr(\))j Fq(:)g(:)g(:)d Fr(\)\))p Fq(r)1146 1687 y Fv(\003)1145 1717 y Fl(1)1172 1706 y Fq(:)j(:)g(:)e(r)1255 1687 y Fv(\003)1254 1718 y Fn(l)-12 1808 y Fr(with)15 b Fq(g)115 1792 y Fv(\003)147 1808 y Fr(:=)e Fi(rf)r Fr(\()p Fq(g)r(;)6 b(~)-21 b(n)o Fr(;)7 b Fq(~)-22 b(x)o Fr(\),)14 b Fq(k)g Fr(:=)e Fp(d)p Fr(log)597 1819 y Fl(2)617 1808 y Fr(\([)-8 b([)p Fq(N)5 b Fr(])-8 b(])8 b(+)h(1\))p Fp(e)15 b Fr(where)g(!)p Fq(N)h Fr(:=)d Fi(nf)t Fr(\()p Fi(rf)r Fr(\()p Fq(n;)6 b(~)-21 b(n)o Fr(;)7 b Fq(~)-22 b(x)o Fr(\)\),)14 b Fq(T)1418 1815 y Fn(i)1445 1808 y Fr(:=)e Fi(rf)s Fr(\()p Fq(h\024z)r(;)6 b(~)-21 b(n)o(;)8 b Fr(!)p Fq(N)1749 1815 y Fn(i)1762 1808 y Fr(;)f Fq(~)-22 b(x)o(;)8 b(z)r Fr(\))14 b(for)-12 1865 y(some)j(new)g(v)m(ariable)i Fq(z)r Fr(,)e(where)h Fq(N)596 1872 y Fn(i)626 1865 y Fr(is)g(obtained)g(from)e Fq(N)22 b Fr(b)o(y)17 b(deleting)i(the)e(\014rst)g Fq(i)f Fr(leading)j(constan)o(ts)d Fm(s)1861 1872 y Fl(0)1898 1865 y Fr(or)-12 1921 y Fm(s)9 1928 y Fl(1)29 1921 y Fr(,)e(and)i Fq(r)167 1905 y Fv(\003)166 1934 y Fn(j)199 1921 y Fr(:=)c Fi(rf)s Fr(\()p Fq(r)331 1928 y Fn(j)348 1921 y Fq(;)6 b(~)-21 b(n)p Fr(;)7 b Fq(~)-22 b(x)o Fr(\).)38 1986 y(Since)14 b Fq(n)e Fr(is)h(a)f(complete)h(subterm)g(of)f(a)g (term)f(satisfying)i(\(R\),)f(all)h(free)f(v)m(ariables)i(of)e Fq(n)h Fr(are)f(complete.)19 b(Hence)-12 2042 y Fq(n)p Fr([)o Fq(~)-22 b(n=)o(~)g(x)p Fr(])15 b(is)h(closed,)f(since)i(all)f (free)f(v)m(ariables)h(of)f Fq(t)p Fr([)o Fq(~)-22 b(n=)o(~)g(x)p Fr(])15 b(are)g(safe.)k(Therefore,)c Fi(nf)t Fr(\()p Fq(n)p Fr([)o Fq(~)-22 b(n)o(=)o(~)g(x)p Fr(]\))15 b(is)g(a)g(n)o (umeral.)20 b(One)-12 2099 y(obtains)c Fi(rf)r Fr(\()p Fq(n;)6 b(~)-21 b(n)p Fr(;)7 b Fq(~)-22 b(x)o Fr(\))15 b(with)h(b)q(ound)g Fp(\024)e Fq(q)665 2106 y Fn(n)688 2099 y Fr(\()p Fq(m)p Fr(\))h(b)o(y)g(the)h(induction)h(h)o(yp)q (othesis.)22 b(Then)16 b(b)o(y)f(Base)g(Normalization)-12 2155 y(\(4.4\))f(one)h(obtains)g(the)h(n)o(umeral)f(!)p Fq(N)i Fr(:=)c Fi(nf)s Fr(\()p Fi(rf)r Fr(\()p Fq(n;)6 b(~)-21 b(n)p Fr(;)7 b Fq(~)-22 b(x)o Fr(\)\))12 b(=)h Fi(nf)t Fr(\()p Fq(n)p Fr([)o Fq(~)-22 b(n)o(=)o(~)g(x)p Fr(]\))15 b(with)188 2257 y(#steps)d Fp(\024)h Fr(2)p Fp(j)p Fi(rf)r Fr(\()p Fq(n;)6 b(~)-21 b(n)p Fr(;)7 b Fq(~)-22 b(x)o Fr(\))p Fp(j)12 b(\024)h Fr(2)p Fq(q)726 2264 y Fn(n)749 2257 y Fr(\()p Fq(m)p Fr(\))p Fq(;)52 b Fr(#registers)12 b Fp(\024)h Fq(q)1173 2264 y Fn(n)1197 2257 y Fr(\()p Fq(m)p Fr(\))p Fq(;)52 b Fr(maxlength)13 b Fp(\024)g Fq(q)1627 2264 y Fn(n)1651 2257 y Fr(\()p Fq(m)p Fr(\))p Fq(:)-12 2359 y Fr(W)l(e)23 b(no)o(w)f(compute)g(the)h (term)f Fq(T)596 2366 y Fl(0)615 2359 y Fr(\()p Fq(T)660 2366 y Fl(1)687 2359 y Fq(:)8 b(:)g(:)d Fr(\()p Fq(T)792 2366 y Fn(k)q Fv(\000)p Fl(1)858 2359 y Fq(g)882 2343 y Fv(\003)901 2359 y Fr(\))j Fq(:)g(:)g(:)d Fr(\))22 b(b)o(y)g(an)h(ob)o(vious)g(lo)q(op)g(with)f Fq(k)k Fp(\024)f(j)p Fq(N)5 b Fp(j)24 b(\024)h Fq(q)1839 2366 y Fn(n)1863 2359 y Fr(\()p Fq(m)p Fr(\))-12 2416 y(rounds.)k(Ho)o(w)o(ev)o(er,)17 b(to)g(obtain)i(an)e(estimate)h(on)g(our)g(b)q(ound,)h(w)o(e)f(need)h (to)e(lo)q(ok)i(in)o(to)f(some)f(details.)29 b(First)-12 2472 y(pic)o(k)18 b(a)f(new)g(v)m(ariable)h Fq(z)i Fr(and)d(write)g Fq(h\024z)i Fr(in)o(to)e(a)g(\014xed)h(register)f Fq(v)r Fr(.)25 b(Then,)17 b(compute)h Fq(g)1550 2456 y Fv(\003)1584 2472 y Fr(:=)e Fi(rf)r Fr(\()p Fq(g)r(;)6 b(~)-21 b(n)o Fr(;)7 b Fq(~)-22 b(x)o Fr(\))17 b(with)-12 2529 y(b)q(ound)k Fp(\024)f Fq(q)208 2536 y Fn(g)229 2529 y Fr(\()p Fq(m)p Fr(\))f(in)h(a)g(result)g(register)f Fq(u)p Fr(,)i(and)f(consider)g (the)g(register)g Fq(w)g Fr(holding)h Fq(N)k Fr(=)20 b Fq(N)1678 2536 y Fl(0)1717 2529 y Fr(as)g(coun)o(ter.)-12 2585 y(If)g Fq(w)g Fr(holds)g Fq(N)251 2592 y Fn(i)284 2585 y Fr(=)g(0,)g(output)f(the)h(con)o(ten)o(t)e(of)h(register)h Fq(u)p Fr(,)g(i.e.)f Fq(g)1179 2569 y Fv(\003)1198 2585 y Fr(.)32 b(Otherwise,)21 b Fq(w)f Fr(holds)g Fq(N)1689 2592 y Fn(i)1723 2585 y Fp(6)p Fr(=)g(0)f(and)g Fq(u)-12 2642 y Fr(holds)i(\()p Fq(T)157 2649 y Fn(k)q Fv(\000)p Fn(i)225 2642 y Fq(:)8 b(:)g(:)d Fr(\()p Fq(T)330 2649 y Fn(k)q Fv(\000)p Fl(1)396 2642 y Fq(g)420 2625 y Fv(\003)439 2642 y Fr(\))j Fq(:)g(:)g(:)d Fr(\).)34 b(Compute)20 b(!)p Fq(N)842 2649 y Fn(k)q Fv(\000)p Fn(i)p Fv(\000)p Fl(1)967 2642 y Fr(from)f Fq(N)25 b Fr(and)20 b Fq(N)1271 2649 y Fn(i)1305 2642 y Fr(in)h(the)f(en)o(vironmen)o(t)h(register)f Fq(u)1906 2649 y Fn(z)1926 2642 y Fr(;)-12 2698 y(this)f(clearly)h(is)f (p)q(ossible)h(with)f(some)f(b)q(ound)h Fq(q)839 2705 y Fl(1)859 2698 y Fr(\()p Fp(j)p Fq(N)5 b Fp(j)p Fr(\))16 b Fp(\024)j Fq(q)1053 2705 y Fl(1)1073 2698 y Fr(\()p Fq(q)1111 2705 y Fn(n)1134 2698 y Fr(\()p Fq(m)p Fr(\)\))f(for)f(some)i (p)q(olynomial)h Fq(q)1694 2705 y Fl(1)1714 2698 y Fr(.)29 b(Compute)952 2828 y(9)p eop %%Page: 10 10 10 9 bop -12 199 a Fq(T)15 206 y Fn(k)q Fv(\000)p Fn(i)p Fv(\000)p Fl(1)133 199 y Fr(:=)13 b Fi(rf)r Fr(\()p Fq(h\024z)r(;)6 b(~)-21 b(n;)8 b Fr(!)p Fq(N)438 206 y Fn(k)q Fv(\000)p Fn(i)p Fv(\000)p Fl(1)542 199 y Fr(;)f Fq(~)-22 b(x;)8 b(z)r Fr(\))k(in)i Fq(v)r Fr(,)f(with)h(b)q(ound)g Fq(q)1024 206 y Fn(h\024z)1085 199 y Fr(\()p Fq(m)6 b Fr(+)g Fp(j)p Fq(N)1240 206 y Fn(k)q Fv(\000)p Fn(i)p Fv(\000)p Fl(1)1345 199 y Fp(j)p Fr(\))12 b Fp(\024)h Fq(q)1456 206 y Fn(h\024z)1517 199 y Fr(\()p Fq(m)6 b Fr(+)g Fq(q)1642 206 y Fn(n)1667 199 y Fr(\()p Fq(m)p Fr(\)\).)18 b(Up)q(date)-12 256 y Fq(u)g Fr(b)o(y)f(applying)i(the)e(con)o(ten)o(t)g(of)g Fq(v)i Fr(on)o(to)e Fq(u)p Fr('s)g(original)i(con)o(ten)o(t.)26 b(This)18 b(giv)o(es)f Fq(T)1402 263 y Fn(k)q Fv(\000)p Fn(i)p Fv(\000)p Fl(1)1508 256 y Fr(\()p Fq(T)1553 263 y Fn(k)q Fv(\000)p Fn(i)1620 256 y Fq(:)8 b(:)g(:)e Fr(\()p Fq(T)1726 263 y Fn(k)q Fv(\000)p Fl(1)1792 256 y Fq(g)1816 239 y Fv(\003)1835 256 y Fr(\))i Fq(:)g(:)g(:)d Fr(\))-12 312 y(in)18 b(one)f(step,)g(with)g(no)g(additional)h(register)f(and)g (maxlength)h(increased)g(b)o(y)f Fp(j)p Fq(T)1409 319 y Fn(k)q Fv(\000)p Fn(i)p Fv(\000)p Fl(1)1514 312 y Fp(j)e(\024)h Fq(q)1613 319 y Fn(h\024z)1673 312 y Fr(\()p Fq(m)11 b Fr(+)h Fq(q)1809 319 y Fn(n)1833 312 y Fr(\()p Fq(m)p Fr(\)\).)-12 369 y(Finally)l(,)17 b(up)q(date)e Fq(w)h Fr(to)f(hold)h Fq(N)547 376 y Fn(i)p Fl(+1)621 369 y Fr(and)f(go)g(to)f(the)i(initial)h(test)e(of)f(the)i(lo)q(op.)38 432 y(Let)g(us)h(no)o(w)f(estimate)g(our)g(b)q(ound.)24 b(W)l(e)16 b(go)g Fq(k)f Fp(\024)g(j)p Fq(N)5 b Fp(j)13 b(\024)i Fq(q)1083 439 y Fn(n)1107 432 y Fr(\()p Fq(m)p Fr(\))g(times)i(through)e(the)i(lo)q(op.)23 b(The)17 b(n)o(um)o(b)q(er)-12 488 y(of)e(steps)g(in)h(eac)o(h)f(round)h(is)167 583 y Fp(\024)d Fr(1)d(+)g Fq(q)313 590 y Fl(1)333 583 y Fr(\()p Fp(j)p Fq(N)5 b Fp(j)p Fr(\))k(+)h Fq(q)511 590 y Fn(h\024z)572 583 y Fr(\()p Fq(m)g Fr(+)g Fp(j)p Fq(N)735 590 y Fn(k)q Fv(\000)p Fn(i)p Fv(\000)p Fl(1)840 583 y Fp(j)p Fr(\))g(+)g(2)i Fp(\024)h Fr(1)d(+)h Fq(q)1108 590 y Fl(1)1128 583 y Fr(\()p Fq(q)1166 590 y Fn(n)1189 583 y Fr(\()p Fq(m)p Fr(\)\))e(+)i Fq(q)1358 590 y Fn(h\024z)1418 583 y Fr(\()p Fq(m)f Fr(+)h Fq(q)1552 590 y Fn(n)1575 583 y Fr(\()p Fq(m)p Fr(\)\))e(+)i(2)p Fq(:)-12 677 y Fr(The)16 b(n)o(um)o(b)q(er)f(of)g(register)h(used)g(is)f(3)g(\(for)g Fq(v)r(;)8 b(u;)g(u)855 684 y Fn(z)873 677 y Fr(\))15 b(plus)h Fq(q)1022 684 y Fl(1)1042 677 y Fr(\()p Fq(q)1080 684 y Fn(n)1104 677 y Fr(\()p Fq(m)p Fr(\)\))e(\(to)g(compute)i(!)p Fq(N)1520 684 y Fn(k)q Fv(\000)p Fn(i)p Fv(\000)p Fl(1)1625 677 y Fr(\))f(plus)h Fq(q)1774 684 y Fn(h\024z)1835 677 y Fr(\()p Fq(m)10 b Fr(+)-12 733 y Fq(q)8 740 y Fn(n)32 733 y Fr(\()p Fq(m)p Fr(\)\))k(\(to)g(compute)i Fq(T)425 740 y Fn(k)q Fv(\000)p Fn(i)p Fv(\000)p Fl(1)530 733 y Fr(\),)f(and)g(the)g(maxim)o(um)g(length)h(of)f(a)g(term)g(is)704 827 y Fq(q)724 834 y Fn(n)748 827 y Fr(\()p Fq(m)p Fr(\))9 b(+)i Fq(q)899 834 y Fn(h\024z)960 827 y Fr(\()p Fq(m)e Fr(+)i Fq(q)1093 834 y Fn(n)1117 827 y Fr(\()p Fq(m)p Fr(\)\))p Fq(:)-12 921 y Fr(Hence)16 b(the)g(total)e(b)q(ound)i(for)f (this)h(part)e(of)h(the)g(computation)g(is)568 979 y Fa(\000)589 1016 y Fr(3)10 b(+)g Fq(q)687 1023 y Fn(n)711 1016 y Fr(\()p Fq(m)p Fr(\))g(+)g Fq(q)862 1023 y Fn(h\024z)923 1016 y Fr(\()p Fq(m)g Fr(+)g Fq(q)1056 1023 y Fn(n)1080 1016 y Fr(\()p Fq(m)p Fr(\)\))1174 979 y Fa(\001)1204 1016 y Fp(\001)f Fq(q)1246 1023 y Fn(n)1270 1016 y Fr(\()p Fq(m)p Fr(\))p Fq(:)-12 1110 y Fr(Finally)l(,)20 b(in)e(a)f(lo)q(op)h (with)g Fq(l)g Fr(rounds,)g(compute)g Fq(r)864 1093 y Fv(\003)863 1122 y Fn(j)900 1110 y Fr(:=)e Fi(rf)s Fr(\()p Fq(r)1036 1117 y Fn(j)1053 1110 y Fq(;)6 b(~)-21 b(n)p Fr(;)7 b Fq(~)-22 b(x)o Fr(\))17 b(with)h(b)q(ound)h Fq(q)1451 1117 y Fn(r)1467 1122 y Fe(j)1485 1110 y Fr(\()p Fq(m)p Fr(\),)e(assuming)h Fq(u)f Fr(holds)-12 1166 y(\()p Fq(T)33 1173 y Fl(0)52 1166 y Fr(\()p Fq(T)97 1173 y Fl(1)124 1166 y Fq(:)8 b(:)g(:)d Fr(\()p Fq(T)229 1173 y Fn(k)q Fv(\000)p Fl(1)295 1166 y Fq(g)319 1150 y Fv(\003)338 1166 y Fr(\))j Fq(:)g(:)g(:)d Fr(\)\))p Fq(r)482 1150 y Fv(\003)481 1178 y Fl(1)508 1166 y Fq(:)j(:)g(:)e(r)591 1150 y Fv(\003)590 1179 y Fn(j)r Fv(\000)p Fl(1)653 1166 y Fr(,)14 b(and)i(up)q(date)g Fq(u)f Fr(b)o(y)g(applying)i(this)e(term) g(to)f Fq(r)1486 1150 y Fv(\003)1485 1179 y Fn(j)1506 1166 y Fr(.)38 1230 y(The)i(total)g(n)o(um)o(b)q(er)g(of)g(steps,)f (used)i(registers)f(and)g(lengths)h(of)e(used)i(terms)f(are)f (therefore)h Fp(\024)e Fq(q)1743 1237 y Fn(t)1759 1230 y Fr(\()p Fq(m)p Fr(\))h(with)-12 1286 y(a)g(p)q(olynomial)i Fq(q)281 1293 y Fn(t)311 1286 y Fr(explicitely)h(de\014nable)f(from)e Fq(q)848 1293 y Fn(n)871 1286 y Fr(,)g Fq(q)919 1293 y Fn(h\024z)980 1286 y Fr(,)g Fq(q)1028 1293 y Fn(g)1063 1286 y Fr(and)h(all)g Fq(q)1235 1293 y Fn(r)1252 1282 y Fk(\003)1251 1304 y Fe(j)1272 1286 y Fr(.)p 1919 1259 19 2 v 1919 1284 2 26 v 1937 1284 V 1919 1286 19 2 v -12 1435 a Fs(5)67 b(P)n(olynomial)24 b(time)f(computable)h(functions) -12 1543 y Fr(In)17 b(this)f(last)g(section)g(w)o(e)g(complete)g(the)g (pro)q(of)g(that)f(the)h(n)o(um)o(b)q(er)g(theoretical)h(functions)f (de\014nable)i(b)o(y)d(RA)q(-)-12 1600 y(terms)g(are)g(exactly)g(the)h (p)q(olynomial-time)h(computable)f(functions.)-12 1687 y Fm(Theorem)h(5.1)g(\(Bounding\).)24 b Fo(L)n(et)12 b Fq(t)h Fo(b)n(e)f(a)h(close)n(d)e Fr(RA)q Fo(-term)i(of)g(typ)n(e)f Fq(\033)1268 1694 y Fl(1)1288 1687 y Fq(;)c(:)g(:)g(:)k(;)c(\033)1423 1694 y Fn(k)1456 1687 y Fp(!)14 b Fq(\034)5 b Fo(,)13 b(wher)n(e)f Fq(\033)1717 1694 y Fl(1)1737 1687 y Fq(;)c(:)g(:)g(:)k(;) c(\033)1872 1694 y Fn(k)1893 1687 y Fq(;)g(\034)-12 1743 y Fo(al)r(l)16 b(ar)n(e)g(gr)n(ound.)k(Then)15 b(one)h(c)n(an)f(\014nd) g(a)h(p)n(olynomial)g Fq(p)966 1750 y Fn(t)996 1743 y Fo(such)g(that)h(for)f(al)r(l)f(numer)n(als)g Fq(n)1549 1750 y Fl(1)1569 1743 y Fq(;)8 b(:)g(:)g(:)13 b(;)8 b(n)1706 1750 y Fn(k)1742 1743 y Fo(with)17 b(typ)n(es)-12 1800 y Fq(\033)14 1807 y Fl(1)34 1800 y Fq(;)8 b(:)g(:)g(:)k(;)c(\033)169 1807 y Fn(k)206 1800 y Fo(r)n(esp)n(e)n(ctively,)15 b(one)g(c)n(an)h(c) n(ompute)h(the)g(numer)n(al)e Fi(nf)t Fr(\()p Fq(t)o(~)-22 b(n)p Fr(\))16 b Fo(in)g(time)g Fq(p)1375 1807 y Fn(t)1390 1800 y Fr(\()1408 1766 y Fa(P)1456 1813 y Fn(i)1477 1800 y Fp(j)p Fq(n)1517 1807 y Fn(i)1531 1800 y Fp(j)p Fr(\))p Fo(.)-12 1899 y(Pr)n(o)n(of.)23 b Fr(One)18 b(m)o(ust)g(\014nd)h(a)e(p) q(olynomial)j Fq(p)740 1906 y Fn(t)773 1899 y Fr(suc)o(h)e(that)g(for)f (all)i(n)o(umerals)e Fq(~)-21 b(n)18 b Fr(of)g(t)o(yp)q(es)f Fq(~)-22 b(\033)q Fr(,)19 b(one)f(can)g(compute)-12 1956 y Fi(nf)t Fr(\()p Fq(t)o(~)-22 b(n)p Fr(\))14 b(in)i(time)f Fq(p)301 1963 y Fn(t)316 1956 y Fr(\()p Fq(m)p Fr(\))f(with)h Fq(m)d Fr(:=)622 1922 y Fa(P)670 1969 y Fn(i)692 1956 y Fp(j)p Fq(n)732 1963 y Fn(i)746 1956 y Fp(j)p Fr(.)19 b(Let)14 b Fq(~)-22 b(x)15 b Fr(b)q(e)g(new)g(v)m(ariables)h(of)f(t)o (yp)q(es)e Fq(~)-22 b(\033)r Fr(.)20 b(W)l(e)14 b(consider)i(t)o(w)o(o) e(cases.)38 2019 y Fo(Case)j Fq(\034)j Fr(is)15 b(safe.)20 b(Since)c Fq(t)f Fr(is)h(an)e(RA)q(-term,)g(so)h(is)g Fq(t)o(~)-22 b(x)p Fr(.)20 b(The)15 b(normal)g(form)f(of)g Fq(t)o(~)-22 b(x)15 b Fr(is)h(computed)f(in)g(a)g(n)o(um)o(b)q(er)-12 2076 y(of)h(steps)f(that)h(is)g(large)g(but)g(still)h(only)f(a)g (constan)o(t)f(with)h(resp)q(ect)h(to)d Fq(~)-22 b(n)p Fr(.)22 b(By)16 b(closure)g(under)h(reduction)g(\(3.1\))-12 2132 y(this)g(is)f(an)h(RA-term,)f(with)g(only)h(ground)f(free)g(v)m (ariables.)25 b(Note)15 b(that)h(b)o(y)g(\(4.1\))e(all)k(v)m(ariables)f (in)g Fi(nf)t Fr(\()p Fq(t)o(~)-22 b(x)p Fr(\))15 b(are)-12 2189 y(safe)g(or)f(ground.)20 b(Since)d Fi(nf)s Fr(\()p Fq(t)o(~)-22 b(x)p Fr(\))15 b(is)h(a)e(normal)h(term)g(satisfying)g (\(A\),)f(for)h(ev)o(ery)g(subterm)g Fq(\025x:s)f Fr(with)h Fq(x)g Fr(higher)-12 2245 y(t)o(yp)q(e)f(the)g(v)m(ariable)h Fq(x)f Fr(is)g(a\016nable)g(in)h Fq(s)p Fr(.)20 b(Hence)14 b(b)o(y)g(Sharing)g(\(4.2\))f(one)g(obtains)h(an)g(RS)q(-term)f Fq(t)1671 2228 y Fv(0)1696 2245 y Fr(:=)f Fq(\014)r Fr(\()p Fi(nf)t Fr(\()p Fq(t)o(~)-22 b(x)p Fr(\)\))-12 2301 y(equiv)m(alen)o(t) 22 b(to)d Fq(t)o(~)-22 b(x)q Fr(.)34 b(Let)20 b Fq(c)g Fr(b)q(e)h(the)f(n)o(um)o(b)q(er)g(of)g(steps)g(needed)h(to)e(compute)i Fq(t)1403 2285 y Fv(0)1415 2301 y Fr(.)34 b(By)20 b Fp(R)p Fr(-Elimination)i(\(4.5\))-12 2358 y(one)c(obtains)f(an)h Fp(R)p Fr(-free)f(RS)q(-term)g Fi(rf)r Fr(\()p Fq(t)695 2341 y Fv(0)707 2358 y Fq(;)6 b(~)-21 b(n)o Fr(;)7 b Fq(~)-22 b(x)p Fr(\))17 b(equiv)m(alen)o(t)i(to)e Fq(t)1128 2341 y Fv(0)1140 2358 y Fr([)o Fq(~)-22 b(n=)o(~)g(x)o Fr(])17 b(and)h(hence)h(to)d Fq(t)o(~)-22 b(n)q Fr(.)27 b(This)18 b(requires)g(at)-12 2414 y(most)e Fq(q)121 2422 y Fn(t)134 2413 y Fk(0)147 2414 y Fr(\()p Fq(m)p Fr(\))p Fq(q)243 2421 y Fc(time)309 2414 y Fr(\()p Fq(q)347 2422 y Fn(t)360 2413 y Fk(0)373 2414 y Fr(\()p Fq(m)p Fr(\)\))f(steps,)h(and)h(uses)f(at)g(most)f(this)i(man)o(y)e(registers) h(of)g(this)h(size.)23 b(As)16 b(the)h(output)f(is)-12 2471 y(in)h(a)f(register,)f(this)i(also)f(b)q(ounds)h(the)f(length)g Fp(j)p Fi(rf)s Fr(\()p Fq(t)895 2454 y Fv(0)906 2471 y Fq(;)6 b(~)-21 b(n)p Fr(;)7 b Fq(~)-22 b(x)o Fr(\))p Fp(j)p Fr(.)21 b(Using)c(Base)f(Normalization)h(\(4.4\))d(one)i (obtains)-12 2527 y Fi(nf)t Fr(\()p Fq(t)o(~)-22 b(n)p Fr(\))19 b(=)g Fi(nf)s Fr(\()p Fi(rf)s Fr(\()p Fq(t)306 2511 y Fv(0)317 2527 y Fq(;)6 b(~)-21 b(n)p Fr(;)7 b Fq(~)-22 b(x)o Fr(\)\))18 b(in)i(a)f(total)f(of)h Fq(p)755 2534 y Fn(t)769 2527 y Fr(\()p Fq(m)p Fr(\))f(:=)h Fq(c)13 b Fr(+)g(3)p Fq(q)1054 2535 y Fn(t)1067 2525 y Fk(0)1080 2527 y Fr(\()p Fq(m)p Fr(\))p Fq(q)1176 2534 y Fc(time)1242 2527 y Fr(\()p Fq(q)1280 2535 y Fn(t)1293 2525 y Fk(0)1306 2527 y Fr(\()p Fq(m)p Fr(\)\))18 b(steps)h(using)g(registers)g(of)g(at) -12 2584 y(most)c(the)g(same)g(size.)38 2647 y Fo(Case)k Fq(\034)i Fr(is)16 b(complete.)24 b(Then)16 b(b)o(y)g(a)g(note)g(in)h (section)g(3,)e(all)i(safe)f(input)h(p)q(ositions)g Fq(\033)1530 2654 y Fn(i)1560 2647 y Fr(of)f Fq(t)g Fr(are)g(redundan)o(t.)-12 2704 y(Hence)k([)-8 b([)p Fi(nf)t Fr(\()p Fq(t)o(~)-22 b(n)p Fr(\)])-8 b(])19 b(=)g([)-8 b([)p Fi(nf)s Fr(\()p Fq(t)o(~)-22 b(n)475 2687 y Fv(0)488 2704 y Fr(\)])-8 b(])18 b(where)g Fq(~)-21 b(n)705 2687 y Fv(0)736 2704 y Fr(results)19 b(from)e Fq(~)-21 b(n)19 b Fr(b)o(y)g(replacing)i(eac)o (h)e(safe)g Fq(n)1535 2711 y Fn(i)1569 2704 y Fr(with)g Fm(0)p Fr(.)32 b(Therefore)940 2828 y(10)p eop %%Page: 11 11 11 10 bop -12 199 a Fr(it)22 b(su\016ces)g(to)e(compute)i Fi(nf)t Fr(\()p Fq(t)o(~)-22 b(n)555 183 y Fv(0)567 199 y Fr(\).)38 b(T)l(o)21 b(this)h(end,)h(consider)f(the)g(RA)q(-term)f Fq(t)o(~)-22 b(x)1418 183 y Fv(0)1451 199 y Fr(where)21 b Fq(~)-22 b(x)1615 183 y Fv(0)1648 199 y Fr(results)22 b(from)e Fq(~)-23 b(x)-12 256 y Fr(b)o(y)20 b(replacing)i(eac)o(h)e (safe)g Fq(x)484 263 y Fn(i)518 256 y Fr(with)g Fm(0)p Fr(.)35 b(Let)19 b Fq(~)-21 b(n)814 239 y Fv(0)o(0)835 256 y Fq(;)7 b(~)-22 b(x)882 239 y Fv(0)o(0)923 256 y Fr(result)20 b(from)e Fq(~)-22 b(n)q(;)7 b(~)-22 b(x)19 b Fr(resp)q(ectiv)o(ely)j(b)o(y)e(cancelling)i(all)f(safe)-12 312 y(comp)q(onen)o(ts.)37 b(Observing)22 b(that)e([)-8 b([)p Fq(t)o(~)-22 b(n)660 296 y Fv(0)672 312 y Fr(])-8 b(])22 b(=)g([)-8 b([)p Fq(t)o(~)-22 b(x)829 296 y Fv(0)841 312 y Fr([)o Fq(~)g(n)881 296 y Fv(0)o(0)902 312 y Fq(=)o(~)g(x)951 296 y Fv(0)o(0)972 312 y Fr(]])-8 b(])21 b(=)h([)-8 b([)p Fq(t)1115 296 y Fv(0)1127 312 y Fr([)o Fq(~)-22 b(n)1167 296 y Fv(00)1188 312 y Fq(=)o(~)g(x)1237 296 y Fv(00)1258 312 y Fr(]])-8 b(])20 b(where)h Fq(t)1462 296 y Fv(0)1495 312 y Fr(no)o(w)g(is)g Fq(\014)r Fr(\()p Fi(nf)s Fr(\()p Fq(t)o(~)-22 b(x)1793 296 y Fv(0)1805 312 y Fr(\)\),)21 b(the)-12 369 y(argumen)o(t)15 b(in)h(the)f(\014rst)g(case)g(carries)g (o)o(v)o(er)g(to)f Fq(t)o(~)-22 b(x)852 352 y Fv(0)879 369 y Fr(and)15 b Fq(~)-22 b(n)995 352 y Fv(00)1016 369 y Fr(;)7 b Fq(~)-22 b(x)1063 352 y Fv(0)o(0)1084 369 y Fr(.)20 b(One)c(obtains)f(the)g(same)g(b)q(ound)h Fq(p)1727 376 y Fn(t)1742 369 y Fr(.)p 1919 342 19 2 v 1919 367 2 26 v 1937 367 V 1919 369 19 2 v 38 468 a(It)j(remains)g(to)f(em)o(b)q (ed)h(the)g(p)q(olynomial)h(time)f(computable)g(functions)h(in)o(to)e (the)h(system)f(of)g(RA)q(-terms.)-12 525 y(One)13 b(could)g(use)f(an)o (y)f(of)h(the)g(resource-free)g(function)h(algebra)e(c)o (haracterizations)h([1,)f(3,)g(16])g(of)h(the)f(p)q(olynomial)-12 581 y(time)16 b(computable)g(functions;)f(w)o(e)g(pic)o(k)h([1)o(].)-12 669 y Fm(Theorem)h(5.2.)22 b Fo(Every)16 b(function)g Fq(f)22 b Fo(c)n(omputable)17 b(in)f(p)n(olynomial)g(time)g(on)g(a)h(T) m(uring)e(machine,)h(is)g(denote)n(d)-12 726 y(by)g(an)g Fr(RA)h Fo(term)g Fq(t)321 733 y Fn(f)344 726 y Fo(.)-12 825 y(Pr)n(o)n(of.)23 b Fr(In)16 b([1)o(])g(the)f(p)q(olynomial)j(time) e(computable)g(functions)h(are)e(c)o(haracterized)i(b)o(y)e(a)h (function)g(algebra)g(B)-12 882 y(based)h(on)g(the)f(sc)o(hemata)g(of)h (safe)f(recursion)h(and)g(safe)g(comp)q(osition.)25 b(There)16 b(ev)o(ery)h(function)g(is)h(written)e(in)-12 938 y(the)i(form)e Fq(f)5 b Fr(\()o Fq(~)-22 b(x)p Fr(;)7 b Fq(~)-22 b(y)q Fr(\))17 b(where)g Fq(~)-22 b(x)p Fr(;)7 b Fq(~)-22 b(y)19 b Fr(denotes)e(a)g(kind)i(of)e(b)q(o)q(okk)o(eeping)h(of)f(those)h(v)m (ariables)g Fq(~)-23 b(x)18 b Fr(in)o(v)o(olv)o(ed)g(in)g(a)f(safe)-12 995 y(recursion)g(in)f(the)g(de\014nition)h(of)f Fq(f)5 b Fr(,)15 b(whereas)g Fq(~)-22 b(y)17 b Fr(denotes)f(those)f(v)m (ariables)i(on)f(whic)o(h)g(no)g(recursion)g(has)g(b)q(een)-12 1051 y(p)q(erformed.)30 b(W)l(e)19 b(pro)q(ceed)h(b)o(y)e(induction)j (on)d(the)h(de\014nition)h(of)e Fq(f)5 b Fr(\()o Fq(~)-22 b(x)p Fr(;)7 b Fq(~)-22 b(y)q Fr(\))19 b(in)g(B,)f(asso)q(ciating)h(to) f Fq(f)24 b Fr(a)18 b(closed)-12 1108 y(RA)q(-term)d Fq(t)196 1115 y Fn(f)234 1108 y Fr(of)g(t)o(yp)q(e)387 1096 y Fq(~)388 1108 y Fr(!)p Fq(\023)p Fr(;)s Fq(~)-18 b(\023)12 b Fp(!)h Fq(\023)i Fr(suc)o(h)g(that)g Fq(t)772 1115 y Fn(f)810 1108 y Fr(is)h(denoting)g Fq(f)5 b Fr(,)15 b(i.e.)g([)-8 b([)p Fq(t)1205 1115 y Fn(f)1228 1108 y Fr(])g(])12 b(=)h Fq(f)5 b Fr(.)38 1171 y(If)15 b Fq(f)20 b Fr(is)15 b(an)f(initial)j(function)f Fm(0)p Fr(,)e Fm(s)615 1178 y Fn(i)629 1171 y Fr(\(;)8 b Fq(y)r Fr(\),)13 b Fm(p)p Fr(\(;)8 b Fq(y)r Fr(\))13 b(or)h Fm(c)p Fr(\(;)8 b Fq(y)998 1178 y Fl(1)1017 1171 y Fq(;)g(y)1060 1178 y Fl(2)1079 1171 y Fq(;)g(y)1122 1178 y Fl(3)1141 1171 y Fr(\),)14 b(then)h Fq(t)1305 1178 y Fn(f)1341 1171 y Fr(:=)e Fq(f)5 b Fr(.)20 b(If)14 b Fq(f)20 b Fr(is)15 b(a)g(pro)s(jection)f Fq(\031)1874 1149 y Fn(m;n)1872 1185 y(j)-12 1228 y Fr(satisfying)22 b Fq(\031)225 1206 y Fn(m;n)223 1241 y(j)289 1228 y Fr(\()p Fq(x)333 1235 y Fl(1)352 1228 y Fq(;)8 b(:)g(:)g(:)13 b(;)8 b(x)488 1235 y Fn(m)520 1228 y Fr(;)g Fq(x)567 1235 y Fn(m)p Fl(+1)645 1228 y Fq(;)g(:)g(:)g(:)k(;)c(x)780 1235 y Fn(m)p Fl(+)p Fn(n)862 1228 y Fr(\))22 b(=)i Fq(x)987 1235 y Fn(j)1005 1228 y Fr(,)f(then)f(w)o(e)f(de\014ne)i Fq(t)1378 1235 y Fn(f)1424 1228 y Fr(:=)g Fq(\025x)1548 1235 y Fl(1)1575 1228 y Fq(:)8 b(:)g(:)d(x)1661 1235 y Fn(m)p Fl(+)p Fn(n)1744 1228 y Fq(:u)1783 1235 y Fn(j)1822 1228 y Fr(where)-12 1284 y Fq(u)14 1291 y Fn(j)45 1284 y Fr(:=)13 b Fq(x)132 1291 y Fn(j)150 1284 y Fq(\024)i Fr(if)h Fq(j)f Fp(\024)e Fq(m)p Fr(,)i(and)g Fq(u)497 1291 y Fn(j)528 1284 y Fr(:=)d Fq(x)614 1291 y Fn(j)648 1284 y Fr(otherwise.)38 1353 y(If)g Fq(f)17 b Fr(is)12 b(de\014ned)h(b)o(y)f(safe)f(comp)q(osition)i(from)d Fq(g)r(;)c(~)-21 b(g;)899 1341 y(~)902 1353 y(h)p Fr(,)12 b(that)f(is,)h Fq(f)5 b Fr(\()o Fq(~)-22 b(x)p Fr(;)7 b Fq(~)-22 b(y)q Fr(\))12 b(:=)h Fq(g)r Fr(\()n Fq(~)-21 b(g)p Fr(\()o Fq(~)f(x)p Fr(;)8 b(\);)1474 1341 y Fq(~)1477 1353 y(h)n Fr(\()o Fq(~)-22 b(x)p Fr(;)7 b Fq(~)-22 b(y)q Fr(\)\))11 b(where)h(#)n Fq(~)-21 b(g)14 b Fr(=:)e Fq(m)-12 1410 y Fr(and)i(#)110 1398 y Fq(~)113 1410 y(h)f Fr(=:)g Fq(n)p Fr(,)h(then)g(de\014ne)h Fq(t)515 1417 y Fn(f)551 1410 y Fr(:=)d Fq(\025)o(~)-22 b(x)o(~)g(y)r(:)8 b(t)725 1417 y Fn(g)744 1410 y Fr(!\()p Fq(t)791 1417 y Fn(g)808 1422 y Fh(1)827 1410 y Fq(~)-23 b(x)p Fr(\))8 b Fq(:)g(:)g(:)n Fr(!\()p Fq(t)979 1417 y Fn(g)996 1421 y Fe(m)1026 1410 y Fq(~)-23 b(x)p Fr(\)\()p Fq(t)1104 1417 y Fn(h)1124 1422 y Fh(1)1143 1410 y Fq(~)h(x)o(~)g(y)r Fr(\))8 b Fq(:)g(:)g(:)d Fr(\()p Fq(t)1314 1417 y Fn(h)1334 1421 y Fe(n)1357 1410 y Fq(~)-23 b(x~)g(y)r Fr(\))14 b(where)f Fq(~)-22 b(x)14 b Fr(all)h(are)e(of)h(t)o(yp)q(e)g(!)p Fq(\023)p Fr(,)-12 1466 y(and)h Fq(~)-22 b(y)17 b Fr(all)f(are)f(of)f (t)o(yp)q(e)i Fq(\023)p Fr(.)38 1530 y(Finally)l(,)26 b(if)e Fq(f)k Fr(is)23 b(de\014ned)i(b)o(y)e(safe)g(recursion)g(from)g Fq(g)r Fr(,)g Fq(h)1102 1537 y Fl(0)1122 1530 y Fr(,)i(and)e Fq(h)1282 1537 y Fl(1)1302 1530 y Fr(,)i(then)e Fq(f)5 b Fr(\(0)p Fq(;)i(~)-22 b(x)o Fr(;)7 b Fq(~)-22 b(y)q Fr(\))25 b(=)h Fq(g)r Fr(\()o Fq(~)-22 b(x)o Fr(;)7 b Fq(~)-22 b(y)q Fr(\))23 b(and)-12 1586 y Fq(f)5 b Fr(\()p Fm(s)54 1593 y Fn(i)68 1586 y Fq(x;)i(~)-22 b(x)o Fr(;)7 b Fq(~)-22 b(y)q Fr(\))17 b(=)g Fq(h)297 1593 y Fn(i)311 1586 y Fr(\()p Fq(x;)7 b(~)-22 b(x)o Fr(;)7 b Fq(~)-22 b(y)q(;)8 b(f)d Fr(\()p Fq(x;)i(~)-22 b(x)o Fr(;)7 b Fq(~)-22 b(y)q Fr(\)\))17 b(for)g Fm(s)773 1593 y Fn(i)787 1586 y Fq(x)g Fp(6)p Fr(=)g(0.)28 b(Using)18 b(the)g(induction)i(h)o (yp)q(othesis)f(to)e(obtain)h Fq(t)1807 1593 y Fn(h)1827 1598 y Fh(0)1865 1586 y Fr(and)-12 1643 y Fq(t)4 1650 y Fn(h)24 1655 y Fh(1)44 1643 y Fr(,)d(\014rst)g(de\014ne)h Fq(t)313 1650 y Fn(h)349 1643 y Fr(=)d Fq(\025n)o(~)-22 b(x)o(~)f(y)r(:)8 b Fm(c)544 1650 y Fn(\023)566 1643 y Fq(n)g Fr(0)g(\()p Fq(t)666 1650 y Fn(h)686 1655 y Fh(0)705 1643 y Fr(\()p Fm(p)p Fq(n)p Fr(\))o Fq(~)-22 b(x)o(~)g(y)q Fr(\))8 b(\()p Fq(t)906 1650 y Fn(h)926 1655 y Fh(1)945 1643 y Fr(\()p Fm(p)p Fq(n)p Fr(\))o Fq(~)-22 b(x~)f(y)r Fr(\).)20 b(The)15 b(case)g(is)h(\014nished)h(b)o (y)e(de\014ning)495 1738 y Fq(t)511 1745 y Fn(f)546 1738 y Fr(:=)e Fq(\025x)o(~)-22 b(x:)8 b Fp(R)743 1746 y Fn(~)-15 b(\023)o Fv(!)p Fn(\023)814 1738 y Fr(\()p Fq(t)848 1745 y Fn(g)868 1738 y Fq(~)-23 b(x)p Fr(\))8 b(!\()p Fq(\025u)1004 1719 y Fl(!)p Fn(\023)1027 1738 y Fq(V)1061 1719 y Fn(~)-16 b(\023)q Fv(!)p Fn(\023)1125 1738 y Fq(~)-22 b(y)r(:)8 b(t)1187 1745 y Fn(h)1209 1738 y Fq(u)o(~)-22 b(x)o(~)g(y)r Fr(\()p Fq(V)8 b(~)-22 b(y)r Fr(\)\))8 b Fq(x)-12 1833 y Fr(where)16 b Fq(x;)7 b(~)-22 b(x)14 b Fr(all)i(are)f(of)g(t)o(yp)q (e)g(!)p Fq(\023)p Fr(,)f(and)h Fq(~)-22 b(y)17 b Fr(all)f(are)f(of)g (t)o(yp)q(e)g Fq(\023)p Fr(.)20 b(In)c(eac)o(h)f(case)g(one)h(easily)g (v)o(eri\014es)g([)-8 b([)p Fq(t)1676 1840 y Fn(f)1698 1833 y Fr(])g(])13 b(=)g Fq(f)5 b Fr(.)p 1919 1806 V 1919 1831 2 26 v 1937 1831 V 1919 1833 19 2 v -12 1982 a Fs(References)-12 2090 y Fr([1])22 b(S.J.)f(Bellan)o(toni)h(and)f(S.) g(Co)q(ok.)36 b(A)21 b(New)f(Recursion-Theoretic)j(Characterization)e (of)g(the)g(Polytime)59 2147 y(Functions.)f Fo(Computational)d (Complexity)p Fr(,)e(2:97{110,)d(1992.)-12 2238 y([2])22 b(S.J.)17 b(Bellan)o(toni.)28 b(Characterizing)18 b(parallel)h(p)q (olylog)g(time)f(using)g(t)o(yp)q(e)f(2)h(recursions)g(with)f(p)q (olynomial)59 2295 y(output)h(length.)29 b(In)19 b(D.)e(Leiv)m(an)o(t,) j(editor,)f Fo(L)n(o)n(gic)f(and)h(Computational)g(Complexity)p Fr(,)f(Springer)h(Lecture)59 2351 y(Notes)c(in)h(Computer)e(Science,)j (960:253{268,)12 b(1995.)-12 2443 y([3])22 b(S.J.)15 b(Bellan)o(toni)i(and)e(K.-H.)g(Niggl.)21 b(Ranking)16 b(Primitiv)o(e)g(Recursions:)21 b(The)16 b(Lo)o(w)e(Grzegorczyk)h (Classes)59 2499 y(Revisited.)22 b Fo(SIAM)15 b(Journal)h(of)g (Computing)p Fr(,)f(1998.)k(T)l(o)c(app)q(ear.)-12 2591 y([4])22 b(S.A.)15 b(Co)q(ok)g(and)h(B.M.)f(Kapron.)22 b(Characterizations)16 b(of)f(the)h(basic)g(feasible)h(functionals)g (of)f(\014nite)g(t)o(yp)q(e.)59 2647 y(In)e(S.)f(Buss)g(and)g(P)l(.)g (Scott,)g(editors,)g Fo(F)m(e)n(asible)f(Mathematics)p Fr(,)h(p.)g(71{98,)f(Birkh\177)-23 b(auser)14 b(Boston,)f(New)g(Y)l (ork,)59 2704 y(1990.)940 2828 y(11)p eop %%Page: 12 12 12 11 bop -12 199 a Fr([5])22 b(M.D.)13 b(Da)o(vis)i(and)f(E.J.)h(W)l (eyk)o(er.)j Fo(Computability,)f(c)n(omplexity)e(and)h(languages.)f(F)m (undamentals)g(of)h(the)n(o-)59 256 y(r)n(etic)n(al)f(c)n(omputer)i (scienc)n(e)p Fr(.)i(Acad.)c(Pr.,)f(New)h(Y)l(ork,)g(1983.)-12 350 y([6])22 b(J.Y.)15 b(Girard.)k(Ligh)o(t)d(Linear)g(Logic.)21 b Fo(Information)16 b(and)g(Computation)p Fr(,)f(143:175{204,)d(1998.) -12 443 y([7])22 b(K.)15 b(G\177)-23 b(odel.)276 432 y(\177)270 443 y(Ub)q(er)16 b(eine)g(bisher)f(no)q(c)o(h)h(nic)o(h)o(t) f(b)q(en)q(\177)-24 b(utzte)16 b(Erw)o(eiterung)e(des)h(\014niten)h (Standpunktes.)k Fo(Diale)n(c-)59 500 y(tic)n(a)p Fr(,)15 b(12:280{287,)c(1958.)-12 594 y([8])22 b(D.)14 b(Hilb)q(ert.)301 582 y(\177)296 594 y(Ub)q(er)h(das)h(Unendlic)o(he.)22 b Fo(Mathematische)17 b(Annalen)p Fr(,)c(95:161{190,)f(1925.)-12 687 y([9])22 b(M.)e(Hofmann.)38 b(A)21 b(mixed)h(mo)q(dal/linear)h(lam) o(b)q(da)f(calculus)h(with)e(applications)i(to)e(Bellan)o(toni-Co)q(ok) 59 744 y(safe)16 b(recursion.)25 b Fo(Pr)n(o)n(c)n(e)n(e)n(dings)15 b(of)j(CSL)e('97,)j(A)n(arhus)p Fr(.)d(Springer)h(Lecture)h(Notes)e(in) h(Computer)g(Science,)59 800 y(1414:275{294,)11 b(1998.)-12 894 y([10])22 b(M.)15 b(Hofmann.)21 b Fo(T)m(yp)n(e)n(d)16 b(lamb)n(da)g(c)n(alculi)h(for)g(p)n(olynomial-time)f(c)n(omputation)p Fr(.)23 b(Habilitation)17 b(thesis,)f(TU)59 951 y(Darmstadt,)d(1998.) -12 1044 y([11])22 b(F.)13 b(Joac)o(himski)j(and)e(R.)h(Matthes.)i (Short)e(pro)q(ofs)f(of)g(normalisation)h(for)e(the)i(simply-t)o(yp)q (ed)h Fq(\025)p Fr(-calculus,)59 1101 y(p)q(erm)o(utativ)o(e)f(con)o(v) o(ersions)g(and)h(G\177)-23 b(odel's)15 b Fi(T)p Fr(.)20 b(Submitted,)15 b(1998)-12 1195 y([12])22 b(D.)10 b(Leiv)m(an)o(t.)15 b(Subrecursion)d(and)g(lam)o(b)q(da)f(represen)o(tation)g(o)o(v)o(er)g (free)g(algebras.)i(In)f(S.)f(Buss)h(and)f(P)l(.)g(Scott,)59 1251 y(editors,)27 b Fo(F)m(e)n(asible)d(Mathematics)p Fr(,)j(P)o(ersp)q(ectiv)o(es)f(in)f(Computer)g(Science,)k(p.)c (281{291,)g(Birkh\177)-23 b(auser-)59 1308 y(Boston,)14 b(New)h(Y)l(ork,)g(1990.)-12 1401 y([13])22 b(D.)d(Leiv)m(an)o(t.)37 b(Predicativ)o(e)21 b(recurrence)h(in)f(\014nite)h(t)o(yp)q(e.)35 b(In)21 b(A.)g(Nero)q(de)g(and)f(Y.)g(V.)h(Matiy)o(asevisc)o(h,)59 1458 y(editors,)12 b Fo(L)n(o)n(gic)n(al)g(F)m(oundations)h(of)h (Computer)g(Scienc)n(e)p Fr(,)c(Springer)j(Lecture)g(Notes)f(in)h (Computer)f(Science,)59 1514 y(813:227{239,)g(1994.)-12 1608 y([14])22 b(D.)14 b(Leiv)m(an)o(t.)22 b(Rami\014ed)17 b(recurrence)g(and)e(computational)h(complexit)o(y)g(I:)g(W)l(ord)f (recurrence)h(and)g(p)q(oly-)59 1665 y(time.)24 b(In)17 b(P)l(.)g(Clote)f(and)h(J.)f(Remmel,)i(editors,)f Fo(F)m(e)n(asible)e (Mathematics)j(II)p Fr(,)d(P)o(ersp)q(ectiv)o(es)i(in)h(Computer)59 1721 y(Science,)f(p.)e(320{343,)e(Birkh\177)-23 b(auser,)15 b(1994.)-12 1815 y([15])22 b(D.)14 b(Leiv)m(an)o(t)h(and)g(J.-Y.)g (Marion.)j(Rami\014ed)e(Recurrence)h(and)d(Computational)h(Complexit)o (y)g(IV:)g(Pred-)59 1871 y(icativ)o(e)h(F)l(unctionals)g(and)g(P)o (oly-space.)k Fo(Information)c(and)g(Computation)p Fr(,)f(to)g(app)q (ear.)-12 1965 y([16])22 b(K.-H.)13 b(Niggl.)19 b(The)14 b Fq(\026)p Fr(-Measure)g(as)g(a)g(To)q(ol)g(for)f(Classifying)i (Computational)f(Complexit)o(y)l(.)k Fo(A)o(r)n(chive)d(for)59 2022 y(Mathematic)n(al)h(L)n(o)n(gic)p Fr(,)e(1999.)19 b(T)l(o)c(app)q(ear.)-12 2115 y([17])22 b(H.)13 b(Simmons.)19 b(The)14 b(Realm)h(of)e(Primitiv)o(e)i(Recursion.)k Fo(A)o(r)n(chive)c (for)g(Mathematic)n(al)h(L)n(o)n(gic)p Fr(,)c(27:177{188,)59 2172 y(1988.)-12 2266 y([18])22 b(A.S.)12 b(T)l(ro)q(elstra)g(and)h(H.) f(Sc)o(h)o(wic)o(h)o(ten)o(b)q(erg.)17 b(Basic)c(Pro)q(of)f(Theory,)g (Cam)o(bridge)h(Univ)o(ersit)o(y)g(Press,)g(1996.)940 2828 y(12)p eop %%Trailer end userdict /end-hook known{end-hook}if %%EOF