:: deftheorem defines hasBetterPathAt GRAPHSP:def 13 :
for n, k being Nat
for f being Element of REAL * holds
( f hasBetterPathAt n,k iff ( ( f . (n + k) = - 1 or f /. ((2 * n) + k) > newpathcost (f,n,k) ) & f /. (((2 * n) + (n * (f /. (((n * n) + (3 * n)) + 1)))) + k) >= 0 & f . k <> - 1 ) );