:: deftheorem defines is_Input_of_Dijkstra_Alg GRAPHSP:def 20 :
for f being Element of REAL *
for G being oriented Graph
for n being Nat
for W being Function of the carrier' of G,Real>=0 holds
( f is_Input_of_Dijkstra_Alg G,n,W iff ( len f = ((n * n) + (3 * n)) + 1 & Seg n = the carrier of G & ( for i being Nat st 1 <= i & i <= n holds
( f . i = 1 & f . ((2 * n) + i) = 0 ) ) & f . (n + 1) = 0 & ( for i being Nat st 2 <= i & i <= n holds
f . (n + i) = - 1 ) & ( for i, j being Vertex of G
for k, m being Nat st k = i & m = j holds
f . (((2 * n) + (n * k)) + m) = Weight (i,j,W) ) ) );