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.
Previous Page Next Page