検査に合格した版だけが公開される

版 $c$ に対する決定的な検査を $\chi$、生成を $\mathrm{gen}$ とし、公開されている成果物の時間的な列を $a_0, a_1, a_2, \ldots$ とする。

(a) 次の 3 つを仮定する。(G1) 公開物が更新されるのは、パイプライン「検査 → 生成 → 公開」が最後まで成功したときだけである。(G2) 生成は、検査が合格を返したのと同じ版 $c$ を入力にする。(G3) 公開は、その生成の出力 $\mathrm{gen}(c)$ をそのまま公開物にする。このとき、$a_0$ が「ある版 $c$ について $\chi(c) = \text{合格}$ かつ $a_0 = \mathrm{gen}(c)$」を満たせば、すべての $k$ について $a_k$ も同じ条件を満たす。

(b) （台帳つきの検査）違反の集合を返す決定的な検査 $\kappa$ と、許容する違反の集合 $A$（台帳）に対し、$\chi_A(c) = \text{合格}$ を $\kappa(c) \subseteq A$ で定める。検査を導入する時点の版を $c_0$ とし、$A_0 = \kappa(c_0)$ とおく。以後、合格した版の列 $c_1, c_2, \ldots$ について、台帳を $A_{k} = A_{k-1} \cap \kappa(c_k)$ と更新する（$c_k$ は $\chi_{A_{k-1}}$ に合格したものとする）。このとき

• $\chi_{A_0}(c_0) = \text{合格}$（導入した瞬間にパイプラインは止まらない）、
• すべての $k \ge 1$ で $\kappa(c_k) = A_k \subseteq A_{k-1} \subseteq \cdots \subseteq A_0$（台帳にない違反は 1 件も入らず、台帳は増えない）、
• $A_k = \emptyset$ となった後は、$\chi_{A_k}$ は「違反が 1 件もない」という台帳なしの検査に一致する。