:: deftheorem defines recursively_enumerable HILB10_5:def 4 :
for n being Nat
for A being Subset of (n -xtuples_of NAT) holds
( A is recursively_enumerable iff ex m being Nat ex P being INT -valued Polynomial of ((2 + n) + m),F_Real st
for X being b₁ -element XFinSequence of NAT holds
( X in A iff ex x being Element of NAT st
for z being Element of NAT st z <= x holds
ex Y being b₃ -element XFinSequence of NAT st
( ( for i being object st i in dom Y holds
Y . i <= x ) & eval (P,(@ ((<%z,x%> ^ X) ^ Y))) = 0 ) ) );