Изменения
→Доказательство
{{Лемма
|statement= Алгоритм отработает за конечное время
|proof= Не теряя общности, будем считать, что граф связен. Тогда в конце работы алгоритма все вершины должны оказаться алгоритм завершит работу, когда в <tex>M_0.</tex> На каждом шаге мы гарантированно либо уменьшаем окажутся все вершины. Так как в исходном графе нет отрицательных циклов, то для каждой вершины существует кратчайший путь. Тогда расстояние до какой-то каждой вершины (возможноможет уменьшится только конечное число раз и, как следствие, она перейдет вершина будет переведена из <tex>M_0</tex> в <tex>M_1^{''}</tex>)тоже конечное число раз. С другой стороны, либо перемещаем текущую вершину на каждом шаге текущая вершина гарантированно помещается в <tex>M_0</tex>. Так как в графе нет отрицательных циклов, то уменьшить расстояние можно только конечное число раз. Количество вершин тоже конечно. Следовательно, будет произведено Тогда за конечное число шаговвсе вершины окажутся в <tex>M_0</tex>.
}}
|proof= Предположим обратное. Тогда рассмотрим 2 случая:
# Вершина <tex>u</tex> попала в <tex>M_0</tex> позже <tex>v</tex>. Тогда должна была произойти релаксация ребра <tex>uv</tex> и она была неуспешной. Значит, такого варианта не может быть
# Вершина <tex>u</tex> попала в <tex>_0M_0</tex> раньше <tex>v</tex>. Заметим, что с момента последнего попадания <tex>u</tex> в <tex>M_0</tex> расстояние до нее не менялось(иначе, вершина была бы извлечена из <tex>M_0</tex>). Вес ребра <tex>uv</tex> тоже не меняется. Значит, и релаксация ребра <tex>uv</tex> ничего не даст
Противоречие.
}}
