1 クラスの導入

このシステムではクラスというものも扱えます。gramにcが入ったwordが登場します。
クラスは素朴に「ものの集まり」と捉えるのが良いです。「属する」が基本になります。
\(\mathbb{W}_+\)(sc,p) … \(\in\)
クラスを走る変数がv_-Formです。gramが(,c)で \(X\) などがあります。
\(x \in X\) はp-Formです。「\(x\)というものがクラス\(X\)に入っている」と読むと良いでしょう。
\(X \in X\) はp-Formではありません(s-Formとc-Formは区別されます)。

クラスを扱うときには、「クラスの等号」が出てきます。
\(\mathbb{W}_+\)(cc,p) … \(=\)
これは次の「定義」を持ちます。一般に 〇. は 〇の定義 という位置づけになります。
=_. … \(X = Y \Longleftrightarrow \forall x \, ( x \in X \Leftrightarrow x \in Y )\)

cvtという規則が重要です。
〇. は自然にcvt規則を生成します。=_. は次のようなcvtを生成します。
cvt … \(X = Y\) ≃ \(\forall x \, ( x \in X \Leftrightarrow x \in Y )\)

「単ソート翻訳」では cvt規則 によって \(\mathbb{W}_+\) が処理されます。
次のthmはgoalが \(\forall x \, ( x \in X \Leftrightarrow x \in X )\) となり、自明です。
\(X = X\) \(\blacktriangleleft\) O

2 内包記法

内包記法はクラスを生成する標準的な道具です。 \(\{ x \mid P \}\) という自然な形で使用できるようにしておきます。
\(\mathbb{W}_+\)(vp,c)F … \(\mathsf{cls}\)
abbr … \(\{ x \mid P \}\) ≈ \(\mathsf{cls} ( x , P )\)

次のcvtが重要です。
cvt … \(X \in \{ x \mid P \}\) ≃ substitution(\(P\), \(x\) ↦ \(X\))
次の翻訳は内側からやる方が楽です。
　 \(x \in \{ y \mid z \in \{ x \mid x = y \} \}\) ≅ \(z = x\)
外側からだと \(\int f(x)dx = \int f(y)dy\) みたいな「束縛変数の名前替え」が必要になります。