:: deftheorem Def14 defines Relax GRAPHSP:def 14 :
for f being Element of REAL *
for n being Nat
for b₃ being Element of REAL * holds
( b₃ = Relax (f,n) iff ( dom b₃ = dom f & ( for k being Nat st k in dom f holds
( ( n < k & k <= 2 * n implies ( ( f hasBetterPathAt n,k -' n implies b₃ . k = f /. (((n * n) + (3 * n)) + 1) ) & ( not f hasBetterPathAt n,k -' n implies b₃ . k = f . k ) ) ) & ( 2 * n < k & k <= 3 * n implies ( ( f hasBetterPathAt n,k -' (2 * n) implies b₃ . k = newpathcost (f,n,(k -' (2 * n))) ) & ( not f hasBetterPathAt n,k -' (2 * n) implies b₃ . k = f . k ) ) ) & ( ( k <= n or k > 3 * n ) implies b₃ . k = f . k ) ) ) ) );