Editing Bellman–Ford algorithm (section)

== Proof of correctness ==
The correctness of the algorithm can be shown by [[mathematical induction|induction]]:<ref name="web.stanford.edu"/><ref>{{Cite journal |last=Dinitz |first=Yefim |last2=Itzhak |first2=Rotem |date=2017-01-01 |title=Hybrid Bellman–Ford–Dijkstra algorithm |url=https://www.sciencedirect.com/science/article/pii/S1570866717300011 |journal=Journal of Discrete Algorithms |volume=42 |pages=35–44 |doi=10.1016/j.jda.2017.01.001 |issn=1570-8667}}</ref>

'''Lemma'''. After ''i'' repetitions of ''for'' loop,
* if Distance(''u'') is not infinity, it is equal to the length of some path from ''s'' to ''u''; and
* if there is a path from ''s'' to ''u'' with at most ''i'' edges, then Distance(u) is at most the length of the shortest path from ''s'' to ''u'' with at most ''i'' edges.

'''Proof'''. For the base case of induction, consider <code>i=0</code> and the moment before ''for'' loop is executed for the first time. Then, for the source vertex, <code>source.distance = 0</code>, which is correct. For other vertices ''u'', <code>u.distance = '''infinity'''</code>, which is also correct because there is no path from ''source'' to ''u'' with 0 edges.

For the inductive case, we first prove the first part. Consider a moment when a vertex's distance is updated by
<code>v.distance := u.distance + uv.weight</code>. By inductive assumption, <code>u.distance</code> is the length of some path from ''source'' to ''u''. Then <code>u.distance + uv.weight</code> is the length of the path from ''source'' to ''v'' that follows the path from  ''source'' to ''u'' and then goes to ''v''.

For the second part, consider a shortest path ''P'' (there may be more than one) from ''source'' to ''v'' with at most ''i'' edges. Let ''u'' be the last vertex before ''v'' on this path. Then, the part of the path from ''source'' to ''u'' is a shortest path from ''source'' to ''u'' with at most ''i-1'' edges, since if it were not, then there must be some strictly shorter path from ''source'' to ''u'' with at most ''i-1'' edges, and we could then append the edge ''uv'' to this path to obtain a path with at most ''i'' edges that is strictly shorter than ''P''—a contradiction. By inductive assumption, <code>u.distance</code> after ''i''−1 iterations is at most the length of this path from ''source'' to ''u''. Therefore, <code>uv.weight + u.distance</code> is at most the length of ''P''. In the ''i<sup>th</sup>'' iteration, <code>v.distance</code> gets compared with <code>uv.weight + u.distance</code>, and is set equal to it if <code>uv.weight + u.distance</code> is smaller. Therefore, after ''i'' iterations, <code>v.distance</code> is at most the length of ''P'', i.e., the length of the shortest path from ''source'' to ''v'' that uses at most ''i'' edges.

If there are no negative-weight cycles, then every shortest path visits each vertex at most once, so at step 3 no further improvements can be made. Conversely, suppose no improvement can be made. Then for any cycle with vertices ''v''[0], ..., ''v''[''k''−1],

<code>v[i].distance <= v[i-1 (mod k)].distance + v[i-1 (mod k)]v[i].weight</code>

Summing around the cycle, the ''v''[''i''].distance and ''v''[''i''−1 (mod ''k'')].distance terms cancel, leaving

<code>0 <= sum from 1 to k of v[i-1 (mod k)]v[i].weight</code>

I.e., every cycle has nonnegative weight.