重み付きグラフの最短経路

段 1（回り道を 1 つ除く）．道 $v_0\to v_1\to\dots\to v_k$ が同じ頂点を 2 度通るとする。つまり $i< j$ で $v_i=v_j$ となるものがある。このとき、$v_i$ から $v_j$ までの部分を除いた列
$$ v_0\to\dots\to v_i\to v_{j+1}\to\dots\to v_k $$
も道である（$j< k$ なら、$v_i=v_j$ と $v_{j+1}$ は辺で結ばれているから。$j=k$ なら、列は $v_0\to\dots\to v_i$ で、終点は $v_i=v_k$ のまま変わらない）。除いた部分の長さは $w(v_iv_{i+1})+\dots+w(v_{j-1}v_j)$ で、辺の長さが $0$ 以上なのでこの和は $0$ 以上である。よって新しい道の長さは、もとの長さ以下である。
段 2（くり返す）．段 1 を行うたびに、列の頂点の数は $j-i\ge1$ 個以上減る。頂点の数は $0$ 以上の整数なので、段 1 は有限回しか行えない。段 1 を行えなくなったとき、道は同じ頂点を 2 度通らない、つまり単純な道である。長さは途中で増えないので、もとの道の長さ以下である。
段 3（最小値がある）．単純な道は頂点を 2 度通らないので、頂点の数を $n$ とすると、並べ方は有限通りしかない。よって $s$ から $v$ への単純な道は有限個で、その長さには最小値 $m$ がある（連結なので $s$ から $v$ への道があり、段 2 から単純な道も少なくとも 1 本ある）。どの道の長さも、段 2 で作った単純な道の長さ以上、つまり $m$ 以上である。$m$ は単純な道の長さとして実際にとる値なので、$m$ はすべての道の長さの最小値で、$d(s,v)=m$ である。

途中までの道 $u_0\to\dots\to u_j$ の長さを $a$、残りの道 $u_j\to\dots\to u_k$ の長さを $b$ とすると、最短の道の長さは $d(s,v)=a+b$ である。
背理法で示す。$s$ から $u_j$ への道で、長さが $a$ より小さい $a'$ のものがあったとする。その道の後ろに残りの道 $u_j\to\dots\to u_k$ をつなぐと、$s$ から $v$ への道になり（つなぎ目は同じ頂点 $u_j$）、長さは $a'+b< a+b=d(s,v)$ である。これは $d(s,v)$ が道の長さの最小値であることに反する。よって途中までの道は最短の道で、$d(s,u_j)=a$ である。
$j\ge1$ のとき、$u_0\to\dots\to u_{j-1}$ も（同じ理由で）最短の道なので、その長さは $d(s,u_{j-1})$ である。$u_0\to\dots\to u_j$ の長さはそれに $w(u_{j-1}u_j)$ を足したものなので、$d(s,u_j)=d(s,u_{j-1})+w(u_{j-1}u_j)$ である。

$s$ から $u$ への最短の道の後ろに辺 $uv$ をつなぐと、$s$ から $v$ への道になる。その長さは $d(s,u)+w(uv)$ である。$d(s,v)$ は道の長さの最小値なので、この長さ以下である。

段 1（暫定値は実際の道の長さ）．Dijkstra 法のどの時点でも、次の (a)(b) が成り立つことを示す。
(a) 確定した頂点の暫定値は、その後変わらない。
(b) $v\ne s$ で $D(v)<\infty$ なら、$p(v)$ は $v$ より前に確定した頂点で、$D(v)=D(p(v))+w(p(v)\,v)$ である。
(a) は、手順 2 で書き換えるのが未確定の頂点の暫定値だけであることから分かる。(b) について：$D(v)$ が $\infty$ でなくなるのは手順 2 で書き換えたときだけで、そのとき $u$ を確定したばかりで、$D(v)=D(u)+w(uv)$、$p(v)=u$ と記録する。$u$ は確定しているので、(a) より $D(u)$ はその後変わらない。$D(v)$ がさらに書き換えられれば、そのときの新しい $u$ で同じことが言える。よって (b) がいつも成り立つ。
さて、$v\ne s$ で $D(v)<\infty$ とする。(b) を $v$、$p(v)$、$p(p(v))$、… とくり返し当てる。$p(v)$ が確定したのは、$p(v)$ の暫定値が最後に書き換えられた後である。その書き換えのとき $p(p(v))$ はすでに確定していたので、$p(p(v))$ は $p(v)$ より前に確定した頂点である。このように、たどるたびに「確定した時点」が前にさかのぼる。確定した頂点は有限個なので、この列は有限回で止まる。止まるのは直前の頂点が記録されていない頂点、つまり暫定値を一度も書き換えられていない確定した頂点で、それは暫定値が $\infty$ でない頂点のうち $s$ だけである。こうして
$$ v=x_0,\quad x_1=p(x_0),\quad x_2=p(x_1),\quad \dots,\quad x_m=s $$
が得られる。(b) より $D(x_{i-1})=D(x_i)+w(x_ix_{i-1})$ なので、これを $i=1,\dots,m$ について足すと、$D(s)=0$ より
$$ D(v)=w(x_mx_{m-1})+\dots+w(x_2x_1)+w(x_1x_0) $$
である。右辺は道 $s=x_m\to x_{m-1}\to\dots\to x_0=v$ の長さである。距離は道の長さの最小値なので、
$$ D(v)\ge d(s,v)\qquad\text{（暫定値が } \infty \text{ でない頂点すべてについて）} $$
が成り立つ。$v=s$ でも $D(s)=0=d(s,s)$ である。
段 2（確定するときは距離以下）．確定する順番についての帰納法で、「確定したときの暫定値は距離に等しい」ことを示す。
最初に確定するのは $s$ である（準備の直後、暫定値が $\infty$ でないのは $D(s)=0$ だけだから）。$D(s)=0=d(s,s)$ なので成り立つ。
$u\ne s$ を確定する回を考え、それより前に確定した頂点 $x$ ではすべて $D(x)=d(s,x)$ が成り立っているとする。lem-spp-simple より、$s$ から $u$ への最短の道
$$ s=u_0\to u_1\to\dots\to u_k=u $$
がある。$u_0=s$ は確定しており、$u_k=u$ はまだ確定していない。そこで、この道の上で初めて現れる未確定の頂点を $u_j$ とする（$1\le j\le k$）。その 1 つ前の $u_{j-1}$ は確定している。
帰納法の仮定より $D(u_{j-1})=d(s,u_{j-1})$ である。$u_{j-1}$ を確定した回の手順 2 で、未確定だった $u_j$ を調べたので、その直後に $D(u_j)\le D(u_{j-1})+w(u_{j-1}u_j)$ となった。暫定値は手順 2 で小さくなるだけなので、今も
$$ D(u_j)\le d(s,u_{j-1})+w(u_{j-1}u_j)=d(s,u_j) $$
である。等号は lem-spp-sub による（最短の道の途中まで）。さらに、同じ補題から $d(s,u_j)$ は最短の道の $u_j$ までの部分の長さで、
$$ d(s,u)=d(s,u_j)+\underbrace{w(u_ju_{j+1})+\dots+w(u_{k-1}u_k)}_{\text{残りの辺の長さの和。}\ 0\ \text{以上}}\ \ge\ d(s,u_j) $$
である。辺の長さが $0$ 以上であることを使ったのはここである。
手順 1 で $u$ を選んだのは、$u$ の暫定値が未確定の頂点の中で最小だからで、$u_j$ も未確定なので $D(u)\le D(u_j)$ である。以上をつなぐと
$$ D(u)\le D(u_j)\le d(s,u_j)\le d(s,u) $$
となる。段 1 より $D(u)\ge d(s,u)$ なので、$D(u)=d(s,u)$ である。これで (1) が示された。
段 3（(2) の証明）．$u\ne s$ を確定したとき、段 2 より $D(u)=d(s,u)<\infty$ である。段 1 より、$u$ から直前の頂点をたどると有限回で $s$ に着き、その逆順の道の長さは $D(u)=d(s,u)$ である。よってこの道は最短の道である。

要点：最短の道に沿って不等式を足し合わせると、途中の項が打ち消し合う。