BFS の不変式

補題 3.1（「グラフアルゴリズム」§3）・ ✓公理まで証明済み

グラフ $G=(V,E)$ （有向でも無向でもよい）と始点 $s \in V$ について上のアルゴリズムを実行する。実行中の任意の時点で次が成り立つ。

(a) すべての $v \in V$ について $d[v] \ge \delta(s,v)$ である（ $d[v]=\infty$ の場合も含む）。

(b) キューの中身を先頭から順に $v_1,v_2,\ldots,v_r$ （ $r \ge 1$ ）とすると

d[v_1] \le d[v_2] \le \cdots \le d[v_r] \le d[v_1] + 1

が成り立つ。

閉包の状態

✓ 公理まで証明済み

証明が使う定理を前提としてたどると、Rikai の中の証明だけで定義・公理（物理では基本仮定）までつながっています（前提の定理類 0 件、定義なども含めて 1 件）。

印の意味: ✓公理まで証明済み・ △証明あり（閉包未完）・ ※主張のみ。テーマごとの集計は閉包の状況。

▸ を開くと、その項目の証明が使う前提が出ます。深い先は各項目のページでたどれます。