4 --| の仕組み：fn-elim と 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 fn-elim変換

|fn-elim は、Thm \(\mathcal{T}\) に次のことを最大限繰り返すThm の変換です。適用したアロー関数を新しい関数記号の適用に置き換え、その定義を sos に足します。
・ \(\lceil x \mapsto X \rfloor ( t )\) （アロー関数の全体の自由な v-Form, v_-Form は $z1, …, $zn）があれば F($z1, …, $zn, $t) に置き替え、sos に F($z1, …, $zn, ｘ) = $X を追加する（F は \(\mathcal{T}\) に現れない新しい関数記号）
例　( \(\lceil x \mapsto x + a \rfloor ( b ) = b + a\) ◀ O)|fn-elim … F(a, b) = b + a ◀ F(a, x) = x + a
適用しないアロー関数（関数の値そのもの）は一階の項にならないので、--| では拒否します（次の Rest の引数は除く）。
関数の値を受け取る語（例えば standard_math/1-2 の Rest＝関数と集合から、その関数のグラフをその集合に制限したものを作る語）の出現 \(\lceil x \mapsto X \rfloor | _ Y\) は、先に新しい記号 R($z1, …, $zn)（出現の自由な v-Form, v_-Form）に置き替え、Rest. の定義にその出現を入れた式（R は集合なので sc で包んで =_＝sc 変換は 6.book）を sos に足します（その式の中のアロー関数も fn-elim が消す）。Rest. を紹介していない本、Rest. の定義がその出現に当てはまらない本（「その定義 Rest. が当てはまりません」）では拒否します。
これら（Rest の記号への置き替えと fn-elim）の前に、すべてのアロー関数の本体をβ正規形にします（本体の中の \(\lceil y \mapsto Y \rfloor ( s )\) を $Y の ｙ に $s を入れた式に置き替える。束縛変数は改名して捕獲しない）。だから β同値なアロー関数は同じ記号になります（例 `[ ｢ fn x ↦ x ｣ ] Rest _ X = [ ｢ fn x ↦ ｢ fn y ↦ y ｣ ( x ) ｣ ] Rest _ X` ◀ O は --| O v; で OK＝実測）。アロー関数の外の適用は β簡約せず、上の F に置き替えます。
fn-elim を cls-elim より先に当てます。だから内包の中のアロー関数も、アロー関数の本体の内包も残りません（例 `b ∈_ \{ cls x | ｢ fn ● + a ｣ ( x ) = c \} ⟺ b + a = c` ◀ O は --| O v; で OK＝実測）。本体に命題変数（P^ など）が自由に現れるアロー関数はまだ扱えません。

4.3 規定

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

4.4 前提の書き方の注意

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