:: deftheorem defines newpathcost GRAPHSP:def 12 :
for f being Element of REAL *
for n, k being Nat holds newpathcost (f,n,k) = (f /. ((2 * n) + (f /. (((n * n) + (3 * n)) + 1)))) + (f /. (((2 * n) + (n * (f /. (((n * n) + (3 * n)) + 1)))) + k));