:: deftheorem defines -recursive POLNOT_1:def 43 :
for L being non trivial Polish-language
for E being Polish-arity-function of L
for D being non empty set
for g being Polish-recursion-function of E,D
for J being Subset of (Polish-WFF-set (L,E))
for H being Function of J,D holds
( H is g -recursive iff for F being Polish-WFF of L,E st F in J & rng (Polish-WFF-args F) c= J holds
H . F = g . [(L -head F),(H * (Polish-WFF-args F))] );