:: deftheorem defines Lucas_inv_pred NOMIN_9:def 14 :
for V, A being set
for loc being b₁ -valued Function
for x0, y0, p0, q0 being Integer
for n0 being Nat
for d being object holds
( Lucas_inv_pred A,loc,x0,y0,p0,q0,n0,d iff ex d1 being NonatomicND of V,A st
( d = d1 & {(loc /. 1),(loc /. 2),(loc /. 3),(loc /. 4),(loc /. 5),(loc /. 6),(loc /. 7),(loc /. 8),(loc /. 9),(loc /. 10)} c= dom d1 & d1 . (loc /. 2) = 1 & d1 . (loc /. 3) = n0 & d1 . (loc /. 7) = p0 & d1 . (loc /. 8) = q0 & ex I being Nat st
( I = d1 . (loc /. 1) & d1 . (loc /. 4) = Lucas (x0,y0,p0,q0,I) & d1 . (loc /. 5) = Lucas (x0,y0,p0,q0,(I + 1)) ) ) );