4 --| の仕組み：cls-elim

4.1 cls-elim変換

|cls-elim は、Thm \(\mathcal{T}\) に次のことを最大限繰り返すThm の変換です。内包を新しいクラス定数に置き換え、その定義を sos に足します。
〇 \(\{ x \mid P \}\) （この内包全体が自由な v-Form, v_-Form を含まない）があれば \(\mathrm{X}\) に置き替え、sos に \(x \in \mathrm{X} \Leftrightarrow P\) を追加する（\(\mathrm{X}\) は \(\mathcal{T}\) に現れない）
〇 \(\{ x \mid P \}\) （この内包全体の自由な v-Form, v_-Form は v-Form \(z\) だけ）があれば \({\mathrm{X}} ( z )\) に置き替え、sos に \(x \in {\mathrm{X}} ( z ) \Leftrightarrow P\) を追加する（\({\mathrm{X}}\) は \(\mathcal{T}\) に現れない）
〇 \(\{ x \mid P \}\) （この内包全体の自由な v-Form, v_-Form は v_-Form $Y_ だけ）があれば |?_X_ ($Y_) に置き替え、sos に x ∈_ |?_X_ ($Y_) ⇔ $P を追加する（|?_X_ は \(\mathcal{T}\) に現れない）
〇 自由変数が2個以上でも同様
$P の中の x は cls が束縛するので自由な出現に数えません。例えば \(\{ x \mid x = x \}\) は自由な変数を含みません。
例　( \(y \in \{ x \mid x = x \}\) ◀ O)|cls-elim … \(y \in \mathrm{X}\) ◀ \(x \in \mathrm{X} \Leftrightarrow x = x\)

4.2 規定

Book 内の自動変数 \(\mathbb{W}_+.\) は「〇.（〇 は gram に c を含む）という形の prop すべての列」です（W. は c を含まないもの・4.book）。ここでは =_. です。
Thm の簡単な演算に +sos があります。(\({\tt P}\) ◀ \(\Gamma\)) +sos \(\Delta\) は \({\tt P}\) ◀ \(\Gamma,\Delta\) です。
default.thmel の規定：
　\(\mathcal{T}\) holds in \(\mathbb{L}_*\) \(\Longleftrightarrow\) \(\mathcal{T}\)|cls-elim +sos \(\mathbb{W}_+.\) holds in \(\mathbb{L}_\mathrm{Hsc}\)
　\({\tt P}\) --| \(\Gamma\) … (\({\tt P}\) ◀ \(\Gamma\))|cls-elim +sos \(\mathbb{W}_+.\)
-| と --| が「どちらも意味を持つとき」同値か、は重要な問題で、まだ一般には示されていません（両方で通る Thm の例：1.1 の y ∈_ \{ cls x | x = x \} ◀ O は -| O p; でも --| O v; でも OK＝実測）。

4.3 前提の書き方の注意

\(x \in \mathrm{B}\) \(\blacktriangleleft\) \(x \in A\)
ソース：thm `x ∈_ |B_` ◀ `x ∈_ A_`、prf `x ∈_ |B_` --| `x ∈_ A_` v;。