1.4 cls-elim変換

|cls-elim というThmの変換も作ります。「\(\mathcal{T}\)に対し次のものを作る」ことを最大限繰り返します。
内包 \(\{ x \mid P \}\) のようなc-Formを、新しいクラス定数に置き替え、その定数への所属の公理（x ∈_ その定数 ⇔ P）を sos に足します。内包が自由な変数を含むときは、それを引数に取る記号に置き替えます（細かい規則はAI用tutorial）。
例えば
　( \(y \in \{ x \mid x = x \}\) ◀ O)|cls-elim … \(y \in \mathrm{X}\) ◀ \(x \in \mathrm{X} \Leftrightarrow x = x\)

1.5 --|

Book内の自動変数 \(\mathbb{W}_\mathrm{c}.\) は「〇. （〇 は gram に c を含む）という形の prop すべての列」です。\(\mathbb{W}.\) と違い、クラスの語の定義（=_. ・𝕍. など）が入ります。
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}_\mathrm{c}.\) holds in \(\mathbb{L}_\mathrm{Hsc}\)
　\({\tt P}\) --| \(\Gamma\) … (\({\tt P}\) ◀ \(\Gamma\))|cls-elim +sos \(\mathbb{W}_\mathrm{c}.\)

--| の段ではクラスの語の定義は（sos に書かなくても）前提に入ります。-| の段では展開をします。
\(\mathbb{L}_*\) の2つの定義が同値なのか、は非常に重要な問題です。メタ定理の為、必要な場合に各Thmに対してcheckをします。

次のThmはソース67行目の --| を -| に替えると通りません。|cvt+ で \(x \in A\) が残るため。
\(x \in \mathrm{B}\) \(\blacktriangleleft\) \(x \in A\)
このsosは「すべての x がすべてのクラス A_ に属する」という（強すぎる）主張です。
\(A\) に \(\mathrm{B}\) を代入することを明示した証明（ソース71行目）も書けます。
\(x \in \mathrm{B}\) \(\blacktriangleleft\) \(x \in A\)

2 アロー関数

\(\in\) と \(\mathsf{cls}\) はp-Formへのs-Formのsubstitutionを作る道具でしたが、s-Formへのs-Formのsubstitutionも可能にします。
word(vs,(s,s))F … \(\mathsf{fn}\)
abbr … \(\lceil x \mapsto X \rfloor\) ≈ \(\mathsf{fn} ( x , X )\)
次の cvt(fn.) という規則が重要です（fn.はありません）。なおソースの ｢ ｣ は半角のかぎ括弧です。
cvt … \(\lceil x \mapsto X \rfloor ( t )\) ≃ substitution(\(X\), \(x\) ↦ \(t\))
例　 \(\lceil x \mapsto x + a \rfloor ( b )\) ≃ \(b + a\)
★アロー関数は -| で使って下さい。--| ではまだ未対応です。

\(\mapsto\) の前のv-Formを \(\bullet\) に替えられます。その際 \(\bullet \mapsto\) は略されます。
例　 \(\lceil \bullet + a \rfloor\) ≈ \(\lceil x \mapsto x + a \rfloor\)
\(\lceil \bullet \rfloor\) は恒等写像です。
\(\bullet\) は入れ子では使用すべきでありませんが、必ず内側から計算されます。
例　 \(\lceil \bullet + \lceil \bullet + a \rfloor ( x ) \rfloor\) ≈ \(\lceil \bullet + ( x + a ) \rfloor\)