ソート問題

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

$(S, \le)$ を全順序集合とする。入力は $S$ の元からなる長さ $n$ の列 $a = (a_0, a_1, \ldots, a_{n-1})$ である。出力は $\{0, 1, \ldots, n-1\}$ 上の置換 $\pi$ であって

a_{\pi(0)} \le a_{\pi(1)} \le \cdots \le a_{\pi(n-1)}

を満たすもの（あるいは並べ替えた列そのもの）である。

閉包の状態

定義

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

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

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