クリーンビルドの一意性

定理 4.1（「ビルドと依存関係」§4）・ ✓公理まで証明済み

密閉的なビルドの記述（依存グラフは DAG）と入力の状態 $x : I \to \mathcal{V}$ に対し、次が成り立つ。

(a) 写像 $v_x : N \to \mathcal{V}$ で

v_x(i) = x(i)\ \ (i \in I), \qquad v_x(t) = f_t\bigl(v_x|_{D(t)}\bigr)\ \ (t \in T)

を満たすものがただ 1 つ存在する。

(b) ストアの入力の部分を $x$ にしてから、すべてのタスクを依存グラフのトポロジカル順に 1 回ずつ実行すると、トポロジカル順の選び方によらず、最後のストアは $v_x$ に一致する。

$v_x$ を入力 $x$ に対するビルドの結果と呼ぶ。

閉包の状態

✓ 公理まで証明済み

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

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

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

トポロジカル順の存在と計算✓定理 3.2・ビルドと依存関係
- 2 つの表現の計算量✓命題 2.6・グラフアルゴリズム
  - 握手補題✓補題 2.5・グラフアルゴリズム
- 閉路のないグラフには入次数 0 の頂点がある✓補題 3.1・ビルドと依存関係
  - 鳩の巣原理✓定理 7.5・数え上げと母関数
    非交和の性質✓命題 4.8・数学の国語
- 灰色頂点の構造✓補題 4.1・グラフアルゴリズム
- 有向閉路の検出✓定理 4.2・グラフアルゴリズム
  - 灰色頂点の構造✓補題 4.1・グラフアルゴリズム
  - 2 つの表現の計算量✓命題 2.6・グラフアルゴリズム（上で展開済み）
密閉性定義 2.2・ビルドと依存関係
完全帰納法✓定理 4.3・証明の技術
- 数学的帰納法の原理✓定理 3.2・証明の技術
  - 背理法の正当性✓命題 6.2・証明の技術
  - 整列性公理 3.1・証明の技術