1 定義と W.

1.1 定義 〇.

この Book は、定義の使い方（W. と slash）と、word を対象として扱う表現の説明です。まず、集合論の最初に出てくる記号を紹介します。
word(ss,p) … \(\in\)  \(\subset\)
⊂ の定義を prop として書きます。名前を 〇.（〇 の定義）にする決まりです。
⊂. … \(X \subset Y \Longleftrightarrow \forall x \in X . x \in Y\)
=. … \(X = Y \Longleftrightarrow \forall x \, ( x \in X \Leftrightarrow x \in Y )\)
ソース：prop ⊂. <- `X ⊂ Y ⟺ [ ∀ x ∈ X . x ∈ Y ]`（X の元はすべて Y の元）、prop =. <- `X = Y ⟺ ∀ x \, (x ∈ X ⇔ x ∈ Y)`（元が同じなら等しい。⟸ は外延性公理と呼ばれることが多い）。= は一階論理の等号のままで、=. は「元が同じなら等しい」を ∈ についての前提として置く prop です。定義のように W. に入れて使えるので便利です。

1.2 W.：定義の列

W. は「この位置までに紹介した 〇. の形の prop（〇 の gram に c を含まないもの）すべての列」です。査読器が Book を上から読みながら自動で更新します。ここでは W. ＝ ⊂. , =. です。
P ◀ W. は「定義から P が示される」と読みます。必要な定義を一々書かずに済むので、よく使います。
=.. … \(X = Y \Longleftrightarrow X \subset Y \subset X\) \(\blacktriangleleft\) \(\mathbb{W}.\)
ソース：prop/thm =.. ◀ W.、prf =.. -| W. p;。=.. は DB に登録された prop で、中身は X = Y ⟺ X ⊂ Y and Y ⊂ X（「等しい ⟺ 互いに含む」）です。W. を sos に置いて Prover9 に投げ、length:37 で示されます。W. の代わりに ⊂. , =. を sos に置いても示せます（thm の主張は ◀ W. なので、最後に =.. -| W. h; でつなぎます）。
Prover9 に投げるとき sos には必要なものだけを置く方がよいので、定義が増えたら W. でなく必要な 〇. を並べる方が速いことがあります。また、W. が無限列になったとき（例えば \n を含む word の定義があるとき）は -| W. p; とは書けません。

1.3 slash：定義で展開する

/ は Thmel の2項演算で、A / P は「A を P で展開したもの」です。P は 〇. でも W. でも構いません。
例（slash_cli での計算結果。前置記法 [頭 引数…] で示す。w1 は展開で導入された束縛変数）：
　X ⊂ Y / W. → [∀ w1 [⇒ [∈ w1 X] [∈ w1 Y]]]
　=.. / W. → [⇔ [∀ w1 [⇔ [∈ w1 X] [∈ w1 Y]]] [and [∀ w1 [⇒ [∈ w1 X] [∈ w1 Y]]] [∀ w1 [⇒ [∈ w1 Y] [∈ w1 X]]]]]（= も ⊂ も開く）
展開してから投げる prf が書けます。
=.. \(\blacktriangleleft\) \(\mathbb{W}.\)
ソース：prf =.. / W. -| O p;、続けて =.. -| W. h;。1段目は「展開した式 ◀ O」を Prover9 に投げます（この例では展開した式が前提なしで示せるので sos は O。一般には、定義以外の前提が要れば sos に残します）。goal は長くなりますが length:28 に減ります。2段目の h; は、1段目の Thm と、展開に使った W. から、thm の =.. ◀ W. を組み立てます（3.book の h;）。この形（/ の段を h; で戻す）では h; の段も -| で書きます。1段目は -| の Thm で、しかも slash を含むので多ソートで確かめ直せず、◀ h; では使えないからです（3.book「h; の段の関係」）。=.. ◀ W. h; にすると「conclusion: no derivation found (4 thms are in another relation)」で FAIL します（実測）。


1回の / の規則：式を内側の部分式から順に見て、各部分式を1回だけ、その頭の語の定義 〇. で書き換えます（頭が ∈ の所属 t ∈ f(…) なら、右側の語 f の定義を使います。定義の形に合わなければそのまま）。書き換えでできた式は、その回ではもう書き換えません。新しく現れた定義できる語は、次の / で開きます。
　// W. は / W. / W.（2回）です。開くものが無くなれば、それ以上 / を増やしても式は変わりません。例：X = Y ⟹ Y ⊂ X は / W. でも // W. でも同じ [⇒ [∀ w1 [⇔ [∈ w1 X] [∈ w1 Y]]] [∀ w1 [⇒ [∈ w1 Y] [∈ w1 X]]]]。
2回要る例は 6.book にあります：X ∩ Y ⊂ X ◀ W. は、1回目の / で ⊂ が開いて w1 ∈ X ∩ Y が新しく現れ、2回目の / でそれが ∩ の定義で開きます。そのため / W. -| O p; では FAIL、// W. -| O p; では OK です（∩ の定義を使うにはクラス版の定義の紹介も要るので、この Book では扱いません）。
　W.!〇.（空白を入れずに書く）は W. から 〇. を除いた列です。例：=.. / W.!=. → [⇔ [= X Y] [and [∀ w1 [⇒ [∈ w1 X] [∈ w1 Y]]] [∀ w1 [⇒ [∈ w1 Y] [∈ w1 X]]]]]（= だけ開かない）。
　/ のすぐ後に数字を書くと、その場所だけを展開します：A /1 P は「A の1番要素だけを P で展開したもの」。番号は前置記法での引数の順です。例：X = Y ⟹ Y ⊂ X は [⇒ [= X Y] [⊂ Y X]] なので、/1 W. → [⇒ [∀ w1 [⇔ [∈ w1 X] [∈ w1 Y]]] [⊂ Y X]]、/2 W. → [⇒ [= X Y] [∀ w1 [⇒ [∈ w1 Y] [∈ w1 X]]]]。
同じ Thm を -| W. p;（定義を sos に置く）でも / W. -| O p;（先に展開する）でも示せることが多いです。定義が増えて sos が大きくなると、先に展開する方が有利になります。
slash の結果は、証明器に投げずに確かめられます：

本が最後までに紹介した定義（W.' は本の中で証明した 〇.' も）で計算します（査読の W. は「その位置まで」なので、途中の Thm を調べるときは違うことがあります）。/ の本数を決めるとき、開かずに残った語が無いかを見るのに使います（practice.book）。