:: deftheorem defines -recursive POLNOT_1:def 42 :
for T being Polish-language
for A being Polish-arity-function of T
for D being non empty set
for f being Polish-recursion-function of A,D
for K being Function of (Polish-WFF-set (T,A)),D holds
( K is f -recursive iff for F being Polish-WFF of T,A holds K . F = f . [(T -head F),(K * (Polish-WFF-args F))] );