18 S. C. KLEENE

*31.5a. * - Vy Vf VaVbYwVwfcp(y) & (y)0=f ,a,b,w &

Cp(y) & (y)0=f ,a,b,w 3 y=^ & w=w}.

*31.5b. f - Gp(y) & (y)

0

=f,^a

1

,..

#

,a

k

,i,b

1

,.

#

.,b

i

,w &

Cp(y) & (y)

0

=f,^a

1

,...,a

k

,^b

1

,...

f

b

i

,w3y= y & w=£.

(The part w=wineach follows by-*25.1from y=ywith (y)Q^...,w,(y)==...,w.)

PROOFS. *31.5a. Weusecourse-of-values induction ony (IMp. 193*l62b).

Assume thehyp. ind., sayvz(zy 3A(z)). Wemust deduce --31.5a as itstands,

i.e. A(y). Assume theantecedent oftheimplication inA(y).By Cp(y) with *3L3,

we have eleven cases Cp^Cy),...,Cpg(y). Twowill suffice forillustration.

CASE Ob: Cp0b(y). Byy=(y)0,(y)1,(y)2 inCP()b(y)with (vii) in the

proof of*31.3-*31.4, (y)^& (j)2y* - Now0= (y)Q^0

Q

Cby

(y)0=«0,(y)0^0 ±,... inCP()b(y)with *25.1 twice] = (f)Q [by (y)Q=f,a,b,w

similarly] = (y)Q

Q

[by (y)0=f,a,b,w]. But,using *31.3, in every casefor

Cp(y) except Cp0a(y) andCpob(y), (y)QQ ^0; so Cp0a(y) V CpQb(y). - Now

Cp0b(y) with (y)Q=f,a,b,w yields (y)Q

Q

^(f )

±

, (y)Qx=a, (y)Q2=b and

Gp((y)1) &

(J^O^WV^IW^O^.

Similarly either Cp~ (y) orCp^Cy) with (y)=f,a,b,w yields

So, since (y)^, thehyp. ind. ony applies to (y)1 with (y)-^,(f)1,a,b,

(y)-L o y(j\ o 3 as the ^f a^b*w^ and Sives (y)1=(y)1 & (y)1Q 3=(y)1

0

y

or more explicitly: First,we eliminate Vz from Vz(zy 3 A(z))using(y),

for z,i.e. as theterm t IMp. 99•Second, weusetheresult with (j)-^r and

3-elim. togetA((y)1). Third, we eliminate VyVfVaVbVwVw fromA^y^)

employing therespective terms listed above. Fourth, weusetheresult with

the conjunction ofthetwolast-displayed formulas via D-elim# to get

j)jr®l

&

^ l ^ ' ^ O ^ ~

B

^ ^ O ^

by GP0b(y)' ^ile Gp0a(^

_

would give (y)1

Q

j=0. Hence Cp^Cy). - NowGpQb(y), (y)Q=f,a,b,w, CpQb(y),

(y)0=f,a,b,w yield

Cp((y)2) & (y)2^0=f,3a,b,w & Cp((y)2) & (y)2^0=f,3a,b,w.

So thehyp. ind. applies again, to (y)2now, with (y)2,f,3a,b,w,w as the y,f,

a,b,w,w, andgives (y)2=s(y)2 & ***'• Hence also (y)Q=f,a,b,wf,a,b,w=y)0.