:: deftheorem Def20 defines PrimRec-Approximation COMPUT_1:def 20 :
for b₁ being sequence of (bool (HFuncs NAT)) holds
( b₁ = PrimRec-Approximation iff ( b₁ . 0 = initial-funcs & ( for m being Nat holds b₁ . (m + 1) = (PR-closure (b₁ . m)) \/ (composition-closure (b₁ . m)) ) ) );