:: deftheorem defines valid_Lucas_input NOMIN_9:def 11 :
for V, A being set
for x0, y0, p0, q0 being Integer
for n0 being Nat
for val being FinSequence holds valid_Lucas_input (V,A,val,x0,y0,p0,q0,n0) = valid_input (V,A,val,(Lucas_input (x0,y0,p0,q0,n0)));