ddmin の正しさと実行回数

定理 5.5（「性質ベーステスト」§5）・ ✓公理まで証明済み

$c$ を相異なる $n \ge 1$ 個の要素の列とし、 $\mathrm{fails}(c)$ は真、空の列については偽とする。

ddmin は止まり、 $c$ の部分列で、失敗し、1-最小であるものを返す。
$\mathrm{fails}$ の実行回数は $6n^2$ より小さい。
失敗の原因が 1 要素である（ある要素 $e$ があって、 $\mathrm{fails}(s)$ が「 $e$ が $s$ に含まれる」と同値である）ならば、ddmin は $e$ だけからなる列を返し、実行回数は高々 $2\lceil \log_2 n \rceil$ である。

閉包の状態

✓ 公理まで証明済み

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

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

証明は Rikai の他の定理を参照していません（定義と論理だけで示されています）。

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