幅優先探索

キューが変わるたびにこの性質が保たれることを示す。最初はキューが $s$ だけなので成り立つ。
先頭の $u_1$ を取り出すと、残りは $u_2,\dots,u_r$ で、$\ell(u_2)\le\dots\le\ell(u_r)\le\ell(u_1)+1\le\ell(u_2)+1$ なので性質は保たれる。
$u_1$ を調べている間に末尾へ加わる頂点 $v$ の番号はすべて $\ell(u_1)+1$ である。加える前のキューは $u_2,\dots,u_r$ と、すでに加えた番号 $\ell(u_1)+1$ の頂点からなり、その番号はすべて $\ell(u_1)$ 以上 $\ell(u_1)+1$ 以下で小さい順に並んでいる。末尾に $\ell(u_1)+1$ を加えても小さい順のままであり、先頭の番号は $\ell(u_1)$ 以上なので、末尾と先頭の差は $1$ 以下である。
後半：$u_1$ を取り出した直後に次に取り出される頂点は、$r\ge2$ ならそのときキューにある $u_2$ で、前半により $\ell(u_2)\ge\ell(u_1)$ である。$r=1$ なら、$u_1$ を調べて加えた番号 $\ell(u_1)+1$ の頂点である（加えたものがなければキューは空になり手順は終わる）。どちらの場合も、続けて取り出される頂点の番号は前の頂点の番号以上である。$\square$

段 1（番号は距離以上）．印の付いた頂点 $v$ について、$v,p(v),p(p(v)),\dots$ は $G$ の歩道で、親をとるたびに番号が $1$ ずつ減るので、ちょうど $\ell(v)$ 歩で番号 $0$ の頂点 $s$ に着く。よって $v$ は $s$ と長さ $\ell(v)$ の歩道で結ばれ、$\operatorname{dist}(s,v)\le\ell(v)$ である。とくに印の付いた頂点は $s$ と同じ連結成分にある。
段 2（距離有限なら印が付き、番号は距離以下）．$s$ との距離が有限で、「印が付かない」か「$\ell(v)\ne\operatorname{dist}(s,v)$」となる頂点 $v$ があったとして矛盾を導く。そのような $v$ のうち $k:=\operatorname{dist}(s,v)$ が最小のものをとる。$s$ には印が付き $\ell(s)=0$ なので $k\ge1$ である。$s$ と $v$ を結ぶ長さ $k$ の道の、$v$ の 1 つ手前の頂点を $u$ とすると、$\operatorname{dist}(s,u)=k-1$ である（$k-1$ 歩で行け、それより短く行けるなら $v$ へ $k$ 歩未満で行けてしまう）。$k$ の最小性から $u$ には印が付き $\ell(u)=k-1$ である。
印の付いた頂点はキューに加わり、手順はキューが空になるまで続くので、$u$ はいつか取り出されて調べられる。そのとき $v$ に印が付いていなければ、$v$ に印が付き $\ell(v)=\ell(u)+1=k$ となり、$v$ の選び方に反する。よって $v$ には $u$ を調べるより前に印が付いている。$v\ne s$ なので、$v$ はある頂点 $w=p(v)$ を調べているときに印が付き、$w$ は $u$ より前に取り出されている。lem-bfs-monotone の後半により $\ell(w)\le\ell(u)$ なので
$$ \ell(v)=\ell(w)+1\le\ell(u)+1=k=\operatorname{dist}(s,v) $$
である。段 1 と合わせて $\ell(v)=\operatorname{dist}(s,v)$ となり、やはり $v$ の選び方に反する。
段 3（結論）．段 1・段 2 から 1 と 2 が従う。3：$s$ の連結成分の頂点を $c$ 個とすると、$T$ の辺は印の付いた $s$ 以外の頂点ごとに 1 本で $c-1$ 本ある。段 1 により、どの頂点も親をたどって $s$ に着くので、$T$ からなるグラフは連結である。$c$ 頂点 $c-1$ 本の辺の連結グラフは木である（全域木 の記事の命題「木の判定」）。$v$ から $s$ への $T$ の中の道は長さ $\ell(v)=\operatorname{dist}(s,v)$ なので、$G$ における最短の道である。$\square$

thm-bfs-correctness の 1 により、印の付く頂点は $s$ の連結成分の頂点である。前半はこれから従う。後半：2 回目以降の探索でも、すでに印の付いた頂点は別の連結成分にあり、新しい始点の連結成分の頂点にはまだ印が付いていないので、同じ定理の 1 がそのまま当てはまる。$\square$

頂点は印を付けるときにだけキューに加わり、印はいったん付けたら消えないので、各頂点は高々 1 回加わり、高々 1 回取り出される。頂点 $u$ を調べるとき、隣接頂点を確かめる回数は $\deg u$ である。各頂点は高々 1 回しか調べられないので、合計は $\sum_u\deg u=2m$ 以下である（握手補題、次数(グラフ) の記事の定理「次数の総和と辺数」）。すべての頂点から探索を続ける場合は、どの頂点もちょうど 1 回加わり、ちょうど 1 回調べられる。$\square$

距離の三角不等式（グラフの距離 の記事の命題「距離空間の公理」）により $\operatorname{dist}(s,v)\le\operatorname{dist}(s,u)+1$ であり、$u,v$ を入れ替えても同じなので $\lvert\operatorname{dist}(s,u)-\operatorname{dist}(s,v)\rvert\le1$ である。$\square$

1：prop-bfs-edges により、どの辺も同じ層か隣の層を結び、仮定により同じ層は結ばないので、どの辺も番号の偶奇が異なる 2 頂点を結ぶ。よって偶数の層の和と奇数の層の和は二部分割である。
2：$T$ の中の $s$ から頂点 $x$ への道を $P_x$ と書く。$P_x$ は $x$ から親をたどって得られる道を逆に並べたもので、$P_x$ の上の頂点 $z$ について、$P_x$ の $s$ から $z$ までの部分は $P_z$ に一致する（$z$ から親をたどる列は、$x$ から親をたどる列の後半だから）。よって $P_u$ と $P_v$ に共通する頂点 $z$ があれば、$P_u$ と $P_v$ はどちらも $P_z$ で始まる。$w$ を共通の頂点のうち番号が最大のものとすると、$P_u$ の $w$ 以降の部分 $Q_u$（長さ $t-\ell(w)$）と $P_v$ の $w$ 以降の部分 $Q_v$（長さ $t-\ell(w)$）は $w$ 以外に共通の頂点をもたない。$w$ 以外の共通の頂点 $z$ があれば、$z$ は $P_u$ と $P_v$ の共通の頂点で、$Q_u$ の上で $w$ より後にあるので $\ell(z)>\ell(w)$ となり、$w$ の選び方に反するからである。
$u\ne v$ で $\ell(u)=\ell(v)=t$ なので、$w$ は $u$ とも $v$ とも異なり（$w=u$ なら $u$ が $P_v$ の上にあって番号 $t$ をもつが、$P_v$ の上で番号 $t$ の頂点は $v$ だけ）、$\ell(w)< t$ である。$Q_u$、辺 $uv$、$Q_v$ を逆にたどった道をつなぐと、$w$ に戻る閉じた歩道で、$w$ 以外の頂点は重複しない。長さは $2(t-\ell(w))+1\ge3$ なので、これは奇数の長さの閉路である。奇数の長さの閉路をもつグラフは二部グラフでない（二部グラフ の記事の定理「閉路の長さによる特徴付け」）。
最後の主張は 1 と 2 を合わせたものである。$\square$

長さ $0$ の道は $s$ だけなので $\sigma(s)=1$ である。$v\in L_i$（$i\ge1$）とし、$s$ と $v$ を結ぶ長さ $i$ の道全体を $\mathcal{P}_v$ と書く。$P=(s=x_0,x_1,\dots,x_i=v)\in\mathcal{P}_v$ について、$x_{i-1}$ は $v$ と隣接し、$P$ の $x_{i-1}$ までの部分は $s$ と $x_{i-1}$ を結ぶ長さ $i-1$ の道である。$\operatorname{dist}(s,x_{i-1})\ge\operatorname{dist}(s,v)-1=i-1$ なので $x_{i-1}\in L_{i-1}$ で、その部分は最短の道である。
逆に、$u\in L_{i-1}$ が $v$ と隣接し、$Q$ が $s$ と $u$ を結ぶ最短の道（長さ $i-1$）なら、$Q$ の頂点は $s$ からの距離が $0,1,\dots,i-1$ なので $v$（距離 $i$）を含まず、$Q$ の後に $v$ をつないだものは $\mathcal{P}_v$ の元である。この 2 つの対応は互いに逆なので、$\mathcal{P}_v$ は、$v$ と隣接する $u\in L_{i-1}$ と $s$ から $u$ への最短の道の組の全体と 1 対 1 に対応する。個数を数えれば漸化式を得る。$\square$