:: deftheorem defines cost GRAPH_5:def 16 :
for G being Graph
for p being FinSequence of the carrier' of G
for W being Function holds cost (p,W) = Sum (RealSequence (p,W));