1 例から

1.1 クラスと内包

この Book はクラス（c-Form）と、クラスを含む Thm の証明の仕方の説明です。ヘッダに thmel 行が無いので default.thmel（-| と --| の両方が書ける）を読みます。
クラスは素朴に「ものの集まり」と捉えます。基本は「属する」です。
word(sc,p) … \(\in\)
=_. … \(X = Y \Longleftrightarrow \forall x \, ( x \in X \Leftrightarrow x \in Y )\)
ソース：word ∈_（x ∈_ X_ で「もの x がクラス X_ に入っている」。表示は ∈ と同じ）、prop =_.（クラスの等号 =_ の定義。DB に登録された prop で、X_ =_ Y_ ⟺ ∀ x (x ∈_ X_ ⇔ x ∈_ Y_)）。表示では =_ も = と同じ記号なので、ソースで区別します。

クラスを作る標準的な道具が内包記法です。
word(vp,c)F … \(\mathsf{cls}\)
abbr … \(\{ x \mid P \}\) ≈ \(\mathsf{cls} ( x , P )\)
ソース：word \cls、abbr cls（\{ cls x | P \} と書けるようにする略記）。\{ cls x | P \} は「P を満たす x の集まり」で、x は cls が束縛する変数です（∀ x と同じ規則）。
\(y \in \{ x \mid x = x \}\) \(\blacktriangleleft\) O
ソース：thm `y ∈_ \{ cls x | x = x \}` ◀ O、prf `y ∈_ \{ cls x | x = x \}` -| O p;。「y は『自分自身に等しいもの』の集まりに入る」。-| の変換が内包の所属を y = y に書き換えるので（下の cvt(cls.)）、Prover9 には一階の式が渡ります。

1.2 クラス変数を含むThm：--|

復習（2.book）：先頭に | が付く |A_ はクラス定数（ある特定のクラス）、付かない X_ はクラス変数（すべてのクラス）です。この違いで、書ける関係（-| か --|）が分かれます。
\(X = Y \Longrightarrow Y = X\) \(\blacktriangleleft\) O
ソース：prf `X_ =_ Y_ ⟹ Y_ =_ X_` --| O v;。X_, Y_ はクラス変数（すべてのクラスについて）です。-| O p; と書くと「|0 翻訳不可: cvt+ 後に ∈_ が残っています。クラス変数への所属は述語に置き換えられません。」で FAIL します（実測）。--| はクラスを残したまま（{s,c}ソートのまま）Vampire に投げるので通ります。
クラス定数（|A_ など）なら -| でも通ります：`|A_ =_ |B_ ⟹ |B_ =_ |A_` ◀ O は -| O p; で OK（|cvt+ がクラス定数への所属を述語に置き換える）。

1.3 アロー関数：-|

word(ss,s) … \(+\)
word(vs,(s,s))F … \(\mathsf{fn}\)
abbr … \(\lceil x \mapsto X \rfloor\) ≈ \(\mathsf{fn} ( x , X )\)
\(\lceil \bullet + a \rfloor ( b ) = b + a\) \(\blacktriangleleft\) O
ソース：word \fn、abbr fn、prf `｢ fn ● + a ｣ ( b ) = b + a` -| O p;。｢ fn ● + a ｣ は「x を x + a に写す関数」（アロー関数）で、直後の ( b ) で b に適用します。-| の変換が適用を b + a に書き換えます（下の cvt(fn.)）。--| O v; でも示せます（下の fn-elim）。

2 どちらで書くか

Thm に含まれるもの	-| … p;（|cvt+|0）	--| … v;（|fn-elim|cls-elim +sos Wc.）
内包 \{ cls x | P \} への所属	OK（P に書き換える）	OK
クラス定数 |A_	OK（述語に置き換える）	OK
クラス変数 X_	FAIL（∈_ が残る）	OK
アロー関数 ｢ fn … ｣	OK（適用を書き換える）	適用したものは OK（関数記号に置き換える）（関数定数に置き換える）

表は変換が通るかの目安で、証明が見つかる保証ではありません。goal と sos の両方を見ます。内包でも、条件 P にクラス変数への所属があれば展開後に残るので -| は FAIL します（例 y ∈_ \{ cls x | x ∈_ X_ \} ◀ y ∈_ X_ は -| p; で FAIL、--| v; で OK＝実測）。let |C_ := `\{ cls x | … \}` で置いた |C_ は内包そのものなので、内包の行に当たります（未定義のクラス定数 |A_ とは違う）。

3.book の「クラス変数があれば ◀ … v;」との関係：`X_ =_ Y_ ⟹ Y_ =_ X_` ◀ O v; も通ります（実測）。どの .thmel でも ◀ と --| はどちらも、投げる前に内包を除き、本が紹介した Wc.（c を含む語の定義）を sos に足します（実測：prop ⊂_. を紹介せずに `X_ ⊂_ X_` ◀ O v; と書くと「本が紹介していない定義を翻訳で使っています: ⊂_.」で FAIL）。

3 -| の仕組み：cvt と cvt+

3.1 cvt変換

〇. は自然に cvt(〇.) という規則を生成します。例えば cvt(=_.) は
cvt … \(X = Y\) ≃ \(\forall x \, ( x \in X \Leftrightarrow x \in Y )\)
内包とアロー関数には、定義 prop（cls. や fn.）は無いのに、次の規則があります。
cvt … \(t \in \{ x \mid P \}\) ≃ substitution(\(P\), \(x\) ↦ \(t\))　（所属を、P の x に t を代入したものに）
cvt … \(\lceil x \mapsto X \rfloor ( t )\) ≃ substitution(\(X\), \(x\) ↦ \(t\))　（適用を、X の x に t を代入したものに）
（$X などは 2.book の「穴」、ｘ は全角で v-Form の穴です。）
|cvt は「cvt 規則を最大限繰り返し適用したもの」です。入れ子は内側からやる方が楽です： \(x \in \{ y \mid z \in \{ x \mid x = y \} \}\) |cvt … \(z = x\) 。外側からだと \(\int f(x)dx = \int f(y)dy\) のような束縛変数の名前替えが要ります。

3.2 cvt+変換

|cvt+ は、Thm \(\mathcal{T}\) に次のことを最大限繰り返すThm の変換です。
・ \(\mathcal{T}\)|cvt をとる。
・ cvt(\({\tt w}\).) がない gram(,c) で v_-Form でない word \({\tt w}\)（クラス定数など）があれば $x ∈_ w を \({\mathrm{p}} ( x )\) に替える（\({\mathrm{p}}\) は \(\mathcal{T}\) に現れない新しい述語）。
・ cvt(\({\tt w}\).) がない gram(s,c) で ?v_-Form でない word \({\tt w}\) があれば $x ∈_ w ($t) を \(\mathbin{\mathrm{p}} ( t , x )\) に替える。
・ gram(ss,c) などの word \({\tt w}\) に対しても同様。
新しい述語の名前は査読器が選びます（下の例では |?X^）。割当ては Thm 全体で保持し、既存の word とは衝突させず、引数の順序とソートを保存します。例　( \(\mathrm{X} = \mathrm{X}\) ◀ O )|cvt+ … \(\forall x ( {\mathrm{X}} ( x ) \Leftrightarrow {\mathrm{X}} ( x ) )\) ◀ O
クラス変数 X_ への所属はどの規則にも当たらないので残り、続く |0（3.book）がエラーになります。これが表の「FAIL（∈_ が残る）」です。

3.3 規定

Thmel の規定：
　\(\mathcal{T}\)|cvt+|0 がエラーでなければ　\(\mathcal{T}\) holds in \(\mathbb{L}_*\) \(\Longleftrightarrow\) \(\mathcal{T}\)|cvt+|0 holds in \(\mathbb{L}_\mathrm{H}\)
　\({\tt P}\) -| \(\Gamma\) … (\({\tt P}\) ◀ \(\Gamma\))|cvt+|0
|0 は 3.book のとおり高階言語（ソートの無い言語）への翻訳なので、右辺は \(\mathbb{L}_\mathrm{H}\) です（\(\mathbb{L}_1\) ではありません）。|?X^ のような新しい述語は記号（定数）です。Thm に高階変数（P^ など）が残っていれば、prover+ は投げる前に |v-elim（3.book）で一階言語 \(\mathbb{L}_1\) の Thm にします。
クラスを使った定理の例：演算の中心。+ が結合的なら、すべての元と可換な元どうしの和も、すべての元と可換です。
\(\mathrm{C}\) … \(\{ x \mid \forall y \; x + y = y + x \}\)
\(\forall u , v , w \; u + ( v + w ) = ( u + v ) + w \Longrightarrow \forall a , b \in \mathrm{C} . \, a + b \in \mathrm{C}\) \(\blacktriangleleft\) O
ソース：let |C_ := `\{ cls x | ∀ y \; x + y = y + x \}`（|C_ を「すべての y と可換な x の集まり」という内包の名前として置く）、thm `[ ∀ u ; v ; w \; u + (v + w) = (u + v) + w ] ⟹ [ ∀ a ; b ∈_ |C_ . \, a + b ∈_ |C_ ]` ◀ O、prf goal -| O p;。|C_ は内包なので -| で書き換えられます。[ ∀ u ; v ; w \; P ] は ∀ u ∀ v ∀ w P（\; は区切り）、[ ∀ a ; b ∈_ |C_ . \, P ] は ∀ a ∀ b (a ∈_ |C_ and b ∈_ |C_ ⇒ P) です（slash_cli で確認）。