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