:: deftheorem defines valid_Lucas_output_pred NOMIN_9:def 12 :
for V, A being set
for z being Element of V
for x0, y0, p0, q0 being Integer
for n0 being Nat
for d being object holds
( valid_Lucas_output_pred A,z,x0,y0,p0,q0,n0,d iff <*(Lucas (x0,y0,p0,q0,n0))*> is_valid_output V,A,<*z*>,d );