:: deftheorem defines valid_Lucas_input_pred NOMIN_9:def 10 :
for V, A being set
for x0, y0, p0, q0 being Integer
for n0 being Nat
for d being object
for val being FinSequence holds
( valid_Lucas_input_pred V,A,val,x0,y0,p0,q0,n0,d iff Lucas_input (x0,y0,p0,q0,n0) is_valid_input V,A,val,d );