FORMALIZED RECURSIVE FUNCTIONALS 21
(J)
(Oo=bV
£ (c)0=(b)0,
ii(f)2 ^ (cX^Cb)^, iL(f)2 o (c)i=(b)i„
c(f)2.=bi ^(f)2.=^i
(f)2"L(b)0 3 (C^Kb)^ (f)2"i(b)0 O (c^-ft)^
(b)0 i •= (0)3=0. (b)0 L = (C^O.
Using (b)0=(b)0, (e) (C)0=(C)0. Using (f)2 - (y)QQ , (y)02,0 ^ CPg ^ "
(b)Q, l3.(b)0~lL(f)2 V i=(f)2' V (f)2"L(b)Q;'so by cases,using (d) and
(5) with 7c)0=(b)0=(F)0 and Vi1^(b)o(b)ill(b)i, (f) VtLsl
(c)o
(C)il|(C)i.
By --19.2 (with (d) and CX)above), (b)=(c')QC; and so by--\L9.16,*B15and the
(*C)
last equation of (d)with ^.1, *B13and ---127: (g)0=TT. ,—.p. i. Nowusing
(a), (b),(c),(e),(g)and (f), thehyp. ind.applies to (y)- and gives
3uCCp(u) & (u)0=(f)1,a,C,w]# Omit 3u.Lety^f,a,b,w,u,so
(y)=f,a,b,w. Weeasily deduce Cpg(y), whence Cp(y).
*31.6b. From *31.6a as *31.5b from *31.5a, except that nowwe must verify
that (^b^^,...,^^^^,^,..^^^^^ and /,b1,..#,b^=
«
i
, b
1
, . . .
J
b ^ »
0
= i = «
i
, b
1
, . . . , b
i
»
0
. 1 1 . n . ^ ^ ^ ^ p , - ' i ' - ' 1 i
" ^ ^ P i " ' 1,##** i i [-X-25.I ] = Po*Pi1#**»*pX^ [evaluating theproduct
TT^n ... (= rT» p|..«)byit successive applications of *B4and one of ---B3,
i Fl
and then evaluating the exponents by*25.1J =
pn#p-,x•••••?Ar
Lsincep.=w
numeralwise represents p., by FIM Lemma 5.2]= i,F, ,##.#Fp [bydef. FIM p.
40]. III. Using *25.1, what we need reduces to Vi^.^ n (£,b- ,...,b^). ||
(^^p b p).. Assume 1LJI* Then i=l V ...V i=i by*137j, since i=0 and
3b(i=%^-!0 E^3b(i=*«+JK) ii] each contradict lii. Nowwe can
deduce (i,bn,...,b/?). I I (i,Fn,...,Fj?). bycases with the numerals l,...,i
successively replacing i, using --25.1 and b,,...,bp I I b,,..•,F/j.
*31.7« I " Cp(y) & (y^^^a^...,^^^^
:=:)3y3x;3c-CCp(y)& (y)0=:f,^,a1,...,ak,i,^(x),...,^£(x),w].
Previous Page Next Page