:: deftheorem Def10 defines primrec COMPUT_1:def 10 :
for f1, f2 being NAT * -defined to-naturals homogeneous Function
for i being Nat
for p being FinSequence of NAT
for b₅ being Element of HFuncs NAT holds
( b₅ = primrec (f1,f2,i,p) iff ex F being sequence of (HFuncs NAT) st
( b₅ = F . (p /. i) & ( i in dom p & Del (p,i) in dom f1 implies F . 0 = (p +* (i,0)) .--> (f1 . (Del (p,i))) ) & ( ( not i in dom p or not Del (p,i) in dom f1 ) implies F . 0 = {} ) & ( for m being Nat holds
( ( i in dom p & p +* (i,m) in dom (F . m) & (p +* (i,m)) ^ <*((F . m) . (p +* (i,m)))*> in dom f2 implies F . (m + 1) = (F . m) +* ((p +* (i,(m + 1))) .--> (f2 . ((p +* (i,m)) ^ <*((F . m) . (p +* (i,m)))*>))) ) & ( ( not i in dom p or not p +* (i,m) in dom (F . m) or not (p +* (i,m)) ^ <*((F . m) . (p +* (i,m)))*> in dom f2 ) implies F . (m + 1) = F . m ) ) ) ) );