主ブランチの不変条件

定義 2.2（「継続的インテグレーション」§2）

主ブランチの先頭が指す版の時間的な列を $h_0, h_1, h_2, \ldots$ とする。決定的な検査 $\chi$ について、

\chi(h_k) = \text{合格} \qquad (k = 0, 1, 2, \ldots)

が成り立つことを主ブランチの不変条件という。

閉包の状態

定義

定義は閉包の起点です（証明を要しません）。

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

証明で明示的に参照している定理は、まだありません。