:: deftheorem defines is_primitive-recursively_expressed_by COMPUT_1:def 9 :
for g, f1, f2 being NAT * -defined to-naturals homogeneous Function
for i being Nat holds
( g is_primitive-recursively_expressed_by f1,f2,i iff ex n being Element of NAT st
( dom g c= n -tuples_on NAT & 1 <= i & i <= n & (arity f1) + 1 = n & n + 1 = arity f2 & ( for p being FinSequence of NAT st len p = n holds
( ( p +* (i,0) in dom g implies Del (p,i) in dom f1 ) & ( Del (p,i) in dom f1 implies p +* (i,0) in dom g ) & ( p +* (i,0) in dom g implies g . (p +* (i,0)) = f1 . (Del (p,i)) ) & ( for m being Nat holds
( ( p +* (i,(m + 1)) in dom g implies ( p +* (i,m) in dom g & (p +* (i,m)) ^ <*(g . (p +* (i,m)))*> in dom f2 ) ) & ( p +* (i,m) in dom g & (p +* (i,m)) ^ <*(g . (p +* (i,m)))*> in dom f2 implies p +* (i,(m + 1)) in dom g ) & ( p +* (i,(m + 1)) in dom g implies g . (p +* (i,(m + 1))) = f2 . ((p +* (i,m)) ^ <*(g . (p +* (i,m)))*>) ) ) ) ) ) ) );