\begin{frame}[fragile]
\frametitle{Bellman Ford - Correctness}
How do we know it actually works? We would like to prove.
\begin{theorem}
If $G=(V,E)$ contains no negatively weighted cycles, then after the Bellman Ford algorithm executes, $d[v]=\delta(s,v)$ for all $v\in V$.
\end{theorem}
\begin{proof}
\only<1>{
Let $v \in V$ be any vertex and consider a shortest path $p$ from $s$ to $v$ with the minimum number of edges. Call the vertices on this path $v_0,\dots,v_k$ where the target vertex is $v_k = v$. Since $p$ is a shortest path we have
$$\delta(s,v_i) = \delta(s,v_{i-1})+w(v_{i-1},v_i)$$
[...]
}
\only<2>{
[...]\\
Initially $d[v_0] = 0 = \delta(s, v_0)$ and $d[v_0]$
\begin{itemize}
\item After $1$ iteration of the outer loop, we are guaranteed that $d[v_1] = \delta(s, v_1)$
\item After $2$ iterations of the outer loop, we are guaranteed that $d[v_2] = \delta(s, v_2)$
\item After $k$ iterations of the outer loop, we are guaranteed that $d[v_k] = \delta(s, v_k)$
\end{itemize}
Since $G$ contains no negatively weighted cycles, $p$ has no loops and therefore the longest path has $\leq |V| -1$ edges.
\qedhere}
\end{proof}
\end{frame}