~P(t), The p a r a l l e l - i n n e r m o s t t" such hence t'~t ° p.

D. 39: L e t t be in M ( F u ~ , V ) , t' in M(F,V) and S * Q > t' a computation sequence of t in t'. > t", c o n s i s t i n g of q-

29 Let m be the occurrence of function variable in rewritten to obtain t' t which is Hence, tim = Gi(tm/v ) and = t(t"/m) where t" belongs to Ti(~m/~). 26 appropriately extended to allow substitutions of vectors of subsets to vectors of symbols: t' C~/~) = (t (w/m) tCSC~)/~) = ¢~/~) ) (t" (~/~) / w) ¢tCwlm) Now, since ~ c ~(~) t"(Q/G) c (SC@/$)) CGi¢{m/~) , t(w/m) Gi(tm/V ) (S(Q)/G) to T i(t+m/$) (~/~) = T i(~/~) G i (tm/V) (~/~) c ¢S(9)/G)/w) t(w/m) (S(~)/~). The inclusion is no less clear, since t"(Q/G) belongs (~m(~/~)/~), and (S(@/G) = {t~(tm(S(Q)/G)/v) , for t"l in S(Q) i} where S(Q) i denotes the i-th component of S(Q); now, it is clear by the definitions that Ti(Q/~) = S(~)i is contained in S(Q)i, and that ~m (~/~) is contained in ~m(S (~)/9).