:: deftheorem defines primitive-recursion_closed COMPUT_1:def 13 :
for X being set holds
( X is primitive-recursion_closed iff for g, f1, f2 being Element of HFuncs NAT
for i being Element of NAT st g is_primitive-recursively_expressed_by f1,f2,i & f1 in X & f2 in X holds
g in X );