情報科学 › ソフトウェア設計とテスト › 事例研究
出現順の関数としての採番は決定的である
各文書 は節に分かれ、各環境 はある節 に属するとする。
(a) 環境 （文書 の成分）の番号を
と定めると、 は文書 の内容だけで決まる。したがって採番は決定的である。
(b) サイト全体で 1 つのカウンタを持ち、文書をある順序 で読みながら、環境に出会うたびにカウンタを 増やしてその値を番号にする方式を考える。文書が 2 つ以上あり、どの文書も環境を 1 つ以上もつならば、この方式の番号は に依存する。
(c) 文書 のページが、文書 の環境 への参照を「定理 」と表示するならば、 のページを作るタスクの出力は の内容に依存する。このタスクが番号の表（索引）を依存に宣言していれば、増分ビルドの結果はクリーンビルドの結果と一致する。
閉包の状態
✓ 公理まで証明済み
証明が使う定理を 前提 としてたどると、Rikai の中の証明だけで定義・公理（物理では基本仮定）までつながっています（前提の定理類 13 件、定義なども含めて 15 件）。
印の意味: ✓公理まで証明済み ・ △証明あり（閉包未完）・ ※主張のみ。テーマごとの集計は 閉包の状況。
前提をたどる 証明が使う定理・定義（直接 1 件）
▸ を開くと、その項目の証明が使う前提が出ます。深い先は各項目のページでたどれます。
増分ビルドの正しさ✓定理 4.2・ビルドと依存関係
クリーンビルドの一意性✓定理 4.1・ビルドと依存関係
トポロジカル順の存在と計算✓定理 3.2・ビルドと依存関係
- 2 つの表現の計算量✓命題 2.6・グラフアルゴリズム この先をたどる →
- 閉路のないグラフには入次数 0 の頂点がある✓補題 3.1・ビルドと依存関係 この先をたどる →
- 灰色頂点の構造✓補題 4.1・グラフアルゴリズム
- 有向閉路の検出✓定理 4.2・グラフアルゴリズム この先をたどる →
- 密閉性定義 2.2・ビルドと依存関係
- 完全帰納法✓定理 4.3・証明の技術（上で展開済み）
これを使っている定理
証明で明示的に参照している定理は、まだありません。