増分ビルドの正しさ

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

密閉的なビルドの記述（依存グラフ $G$ は DAG）と、入力の状態 $x, x'$ を考える。 $C = \{i \in I : x(i) \ne x'(i)\}$ を変更された入力の集合とし、

R = \{t \in T : \text{ある } c \in C \text{ から } t \text{ へ } G \text{ の歩道がある}\}

とおく。ストアが $v_x$ （ $x$ に対するビルドの結果）である状態から、入力の部分を $x'$ に書き換え、 $R$ のタスクだけを $G$ のトポロジカル順に 1 回ずつ実行する。このとき最後のストアは $v_{x'}$ に一致する。

閉包の状態

✓ 公理まで証明済み

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

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

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

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