FORMALIZED RECURSIVE FUNCTIONALS 19

So y - (y)0,(y)1,(y)2 finCp0b(y)] = (y)0,(y)1,(y)2 = y tinCPob(y)].

Thus y=y& w=w.

CASE 5b: Cp^Cy). Sijnilarly wededuce Cp-a(y) V Cp-b(y). But0(y)0

x

x=

(a,)=z(y)Q - 1#ruling outCp~(y). Weusehyp, ind. twice. Thefirst

application isto (y)^ andgives (yJyKy)-! & (y)n Q Q ^ ^ I o V PrePara"torT to

the second application, we obtain Cp((y)2), CpUy^),

(a)of (a)i-l (y)l n.3 TT (a)i-n

^ 2 , 0 ^ ^ 2 ' ° ^ ^ Where C is 2 #3 #5 ^'^l l3L(a) ,P± x *

(7)2,0=(f)2,5-,b,w where C is 2 ( a ) o V a k % ^

But using (y).^Q oKy^

0

3* G==^'# So the hyp* ind# aPPlies to fa^ and Sives

(y)o==(y)o & w=w. We complete thecase asbefore.

After deducing y=y& w=w inall,eleven cases,wecomplete theinduction

step by 3~introd. and V-introds. to obtainA(y).

*31.5b. From *31.5a byusing y,y,f, ^,a1,..#,ak,f,b1,.##,b^,w,w as the

y,y,f,a,b,w,w.

-31.6a. V VfVaVbVbVwfcp(y) & (y)Q=f,a,b,w & (b)Q=(b)0 &

^ n i ( b ) p i ± ^ W ( b ) ( b )

i

l l ( b )

i

^ 3 y [ c

P

( y ) & (y)Q=f,a,D]}.

*31.6b. \- Cp(y) & (y)Q=f,^,a1,#.#,ak,J,b1,...,b£,w&

b

1

,...,b^llb

1

,...,bj 3 3yCCp(y) & (y)

0

=f

i

,^a

1

,...,a

k

,i,b

1

,...,b^,w].

PROOFS. *31.6a. Bycourse-of-values induction ony. Assume theantecedent

of theimplication.

CASE Ob: CPob(y). Asfor*31.5a, (y)^ & (y)2 y andCp((y)1) &

(y)1

0

=(f)1,a,b,(y)1Q «. Also (b)0=(b)0 etc. (byassumption). Similarly,

Cp((y)2) & (y)20r=f,3a,b,w. Sothehyp. ind. applies to (y^andto(y)^ and

gives 3utCp(u) & (u)Q=(f)1,a,b,(y)1Q 3]and 3vrCp(v) & (v)Q=f,3a,b,w].

Omit 3u and 3v preparatory to 3~elims. Nowlet y=«f,a,b,w,u,v. ^ Then

15

When t isa complicated term, wemayfind itnotationally convenient in a

deduction to say"let x=t" where x isa number variable notoccurring freein

any oftheassumption formulas, int, orintheendformula ofthededuction.

Topically,x islater removed asa free variable byan 3x-introd.$ butit may

be soremoved inother ways. Theformula x=tthus introduced istoberegarded

as anassumption for 3-elim. from 3x x=t, proved by 3-introd. from t=t.(We

could instead introduce a temporary abbreviation fort, forwhich howeverwe

prefer nottousea letter normally used as a variable.) Cf. FIMp. 39just

before Lemma 5#3forsimilar practice with a function variable.