情報科学 › アルゴリズムとデータ構造 › グラフアルゴリズム
灰色頂点の構造
上の DFS の実行中の任意の時点について、次が成り立つ。
(a) そのとき灰色である頂点を、再帰スタックの底から順に とすると、各 について は の子である。特に は の歩道であり、 は現在隣接リストを走査中の頂点である。
(b) 頂点 が灰色である間に発見された頂点 （）は、DFS 森において の子孫であり、 を満たす。
閉包の状態
✓ 公理まで証明済み
証明が使う定理を 前提 としてたどると、Rikai の中の証明だけで定義・公理（物理では基本仮定）までつながっています。
印の意味: ✓公理まで証明済み ・ △証明あり（閉包未完）・ ※主張のみ。テーマごとの集計は 閉包の状況。
前提をたどる 証明が使う定理・定義
証明は Rikai の他の定理を参照していません（定義と論理だけで示されています）。
これを使っている定理 証明で参照している 2 件
- 有向閉路の検出✓定理 4.2・グラフアルゴリズム
- トポロジカル順の存在と計算✓定理 3.2・ビルドと依存関係