比較ソートモデル

定義 2.2（「ソートアルゴリズム」§2）

アルゴリズムが入力の要素について得られる情報が、2 要素 $a_i, a_j$ を取り出して $a_i \le a_j$ が成り立つかを問う比較の結果だけであるとき、そのアルゴリズムを比較ソートという。要素の値そのものを添字に使う、ビットを取り出すといった操作は許さない。

閉包の状態

定義

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

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

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