4 実例①　定義をどこまで開くか

6.book の定義で、べき集合の和集合は元の集合、を示します。
⋃℘ … \(\bigcup ( \wp X ) = X\) \(\blacktriangleleft\) \(\mathbb{W}.\)
最初からこのprfが書けたわけではありません。試した順に並べます。
　⋃℘ / W. -| O p; … FAIL（Prover9 not_proved: No proof found）
　⋃℘ // W. -| O p; … FAIL（同じ）
　⋃℘ /// W. -| O p; … FAIL（同じ）。v; に替えても Vampire not_proved (CounterSatisfiable)
　⋃℘ //// W. -| O p; … OK（Prover9 に2本、それぞれ約0.01秒）
どれもすぐに落ちています。これは「探索が重い」ではなく「この形のままでは証明が見つからない」という落ち方です（「失敗の種類を見分ける」の2）。原因は、証明器に渡った goal を読むと分かります。/ の本数ごとに、goal には次の形が開かずに残っていました（Prover9 の入力を抜粋。wp は ℘、sub は ⊂）。
　/ … in(w1,Cup(wp(xX))) -> in(w1,xX)（⋃ の所属がまだ残る）
　// … exists w2 (in(w2,wp(xX)) & in(w1,w2)) -> in(w1,xX)（℘ の所属が残る）
　/// … exists w2 (sub(w2,xX) & in(w1,w2)) -> in(w1,xX)（⊂ が残る）
1本ごとに1層ずつ開いていきます。⊂ が開かないうちは「w2 ⊂ X かつ w1 ∈ w2 なら w1 ∈ X」が証明器には分からないので、示せません。
本数を増やすのをやめる目安：///// にしても、証明器に渡る入力は //// と1文字も変わりませんでした（もう開くものが無い）。入力が変わらなくなったら、本数を増やしても意味がありません。逆に開きすぎは、式が大きくなって timeout の元になります（最初の早見表）。
証明器に渡った入力は、査読画面で OK の印や FAIL の欄の「投げた入力を見る」を押すと見られます。CLI では review_cli.php <本の名前> --inputs と --inputs を付けると、FAIL した行の下に出ます。読み方は 1.book「CLIから査読する」・3.book「途中の段が落ちたとき」。slash の書き換えだけなら、証明器に投げずに slash_cli.php 0_tutorial_AI/6 '`⋃ (℘ X) = X` /// W.' で確かめられます（結果は前置記法で [∀ w1 [⇔ [∃ w2 [and [⊂ w2 X] [∈ w1 w2]]] [∈ w1 X]]]＝⊂ が残っている）。予測を立ててから本数を決めるのに使います。

5 実例②　前提が足りない・補題が要る

6.book では、対集合公理 ax_set2 を置換公理 ax_r から導きました。そこでは補題 le_set2（相異なる2元をもつ集合がある）を前提に加えています。この補題を外すと次のようになります。
　ax_set2 --| ax_r_atST v; … FAIL（Vampire timeout・default.thmel の待ち時間20秒）
　ax_set2 --| ax_r_atST , le_set2 v; … OK（約8秒・2026-10-16）
今度は時間切れです。ax_r の実例は「相異なる s, t をもつ集合 C があれば、その像は \(\{u,v\}\)」と言っているので、証明器はそのような C を自分で見つけなければなりません。そのような C（例えば ℘ (℘ ∅)）を作るには ℘ と ∅ の定義が要りますが、この段の前提には入っていません。つまり、この段はそもそも前提から示せない可能性があります。示せない問題でも、すぐに「示せない」と返るとは限らず、timeout になることがあります。そこで「そういう C がある」を別の Thm（le_set2）として先に示し（6.book では ℘. , ∅. , ⊂. から）、前提に置きました。
このように、証明器に証人（存在を示すための具体的なもの）を自力で発明させている段は、timeout しやすいです。証人を明示した補題を立てると通ることが多いです。
補題の切り方の目安：
　・ 証人が要る所で切る（上の例）。
　・ 数学の場合分けで切る（x ∈ A のときと x ∉ A のとき、など）。1つの段の前提が減って速くなります。
　・ 「写像である」のような部分と「単射である」のような性質の部分を分け、前者は既に示したThmを前提に置く。
　・ 他の定理でも使いそうなら、prf の中のラベルではなく、Book の中の名前付きの Thm にして後で前提に引く。
　・ 数学の要の一点で切る。技術的な細部ではなく、仮定を引く段が1つで済み、残りの段がそこから出る補題を探す（standard_math/1-2 の CSBpiece の Lkey＝X∖A が g[Y∖f[A]] に一致する）。
　・ 補題の結論には、使う段が必要とするものだけを書く。余分な and があると、その分だけ証明器に投げる本数と前提が増える。同値（⟺）の補題は ⟹ と ⟸ に分け、使う段ごとに要る方だけ引く（使わない結論を1つ外しただけで、投げる本数が2本から1本になった例があります）。
　・ 1回しか使わない補題の段は、使う段にまとめる（articles1/25 の証明①では f' ∈ X →IS Y を示す段を置かず、goal が |X =# |Y の段で /// W.' を当てて直接示す。投げ先は v;）。

6 失敗の種類を見分ける

FAIL の文言は、大きく4種類に分かれます。種類によって次の一手が違います。
1. 証明器が動く前に落ちた（「本が紹介していない word」「翻訳不可」「… が余っています」など）：書き方か、関係（-| と --|）の選び方の問題です。数学の中身はまだ試されていません。文言が指す語・行を直します。
2. すぐに「示せない」（Prover9 の No proof found が短時間で出る、Vampire の CounterSatisfiable）：この前提とこの展開のままでは証明が見つからなかった、ということです（Prover9 は探索を制限しているので、「示せないことが確定した」とまでは言えません）。考えられるのは、定義が開ききっていない（実例①）、前提が足りない、主張が偽、のどれかです。CounterSatisfiable は、証明器に渡した問題（翻訳した後の式）に反例があるという意味で、元の主張が偽だとは限りません。開いていない記号が入力に残っていないか、足りない定義・補題が無いかを先に疑います。
3. 時間切れ（timeout）：探索が重い、ということです。開きすぎ（W.!名. で、名の定義を開かないようにする）、証人を自力で探させている（実例②）、1つの段に詰め込みすぎ（補題に分ける）、のどれかを疑います。前提を削りすぎた場合も timeout になることがあります。
4. 証明器の段は通ったのに、最後の h; の段で落ちた：各段は示せていますが、それらを組み合わせても thm の主張にならない、ということです。多くは段どうしのつなぎ方の問題です。最後の段の goal・sos が thm の行と合っているか、途中で使った定義が W. に入っているか（入っていない定義で開いた段はつなげません）を確かめます。「使おうとした Thm の sos の項（…）を、この段の sos から導けませんでした」は、その項を結論に持つ段も前の Thm も見つからなかった、という意味です。項がラベルを含む式なら、ラベルの名前が前の Thm の変数とそろっているか（「名前の付け方」の4）も確かめます。
投げ先（p; v; s;）の選び方は最初の早見表にあります。

6.1 実例：症状から直すまで

・ 2. すぐに示せない → / を足す。最初に書いた prf `X ⊂ X ∪ Y` / W. -| O p; `X ⊂ X ∪ Y` -| W. h; は「Prover9 not_proved: No proof found.」。--inputs で見た入力は formulas(sos).end_of_list.formulas(goals).(all w1 (in(w1,xX) -> in(w1,cup(xX,xY)))).end_of_list. で、⊂ は開いたが ∪ の所属 cup(xX,xY) が残っています。/ を2本にすると通ります。
\(X \subset X \cup Y\) \(\blacktriangleleft\) \(\mathbb{W}.\)
　ソース：thm `X ⊂ X ∪ Y` ◀ W.　prf `X ⊂ X ∪ Y` // W. -| O p; `X ⊂ X ∪ Y` -| W. h;
・ 1. 証明器が動く前に落ちた → 関係を替える。クラス変数の推移律に -| O p; と書くと「capsule-error: |0 翻訳不可: cvt+ 後に ∈_ が残っています。クラス変数への所属は述語に置き換えられません。」。{s,c}ソートのまま Vampire に投げると通ります（◀ O v; でも同じく OK＝実測）。
\(X \subset Y \subset Z \Longrightarrow X \subset Z\) \(\blacktriangleleft\) O
　ソース：thm `[ chain X_ ⊂_ Y_ ⊂_ Z_ ] ⟹ X_ ⊂_ Z_` ◀ O　prf `[ chain X_ ⊂_ Y_ ⊂_ Z_ ] ⟹ X_ ⊂_ Z_` --| O v;

7 通ったあとで

7.1 前提を最小にする

通ったら、前提を1つずつ外して試します。外しても通る前提は要らなかったものです。前提が少ないほど探索は速く、読む人にも何を使ったかが分かります。

7.2 前提が強すぎないかを点検する

前提に量化子で縛られていない変数を書くと、「すべての〜について」の意味になります。そのせいで前提が矛盾していると、何でも証明できてしまいます。4.book の例がそれです。
\({\perp}\) \(\blacktriangleleft\) \(x \neq y\)
前提から ⊥（偽）が示せてしまうなら、その前提は矛盾しています。思ったより簡単に通ったときは、goal を ⊥ に替えて同じ前提で試すと点検できます。
ただし、⊥ が示せないことは、前提が矛盾していないことの証明にはなりません（見つからなかっただけかもしれません）。また、矛盾していなくても強すぎる前提があります。
例：5.book の x ∈_ |B_ ◀ x ∈_ A_。前提 x ∈_ A_ は自由な x・A_ を含むので「すべてのもの x が、すべてのクラス A_ に属する」という式です。A_ に |B_ を入れれば goal そのものになります。この前提から ⊥ は示せません（実測で反例あり）が、どんな式 … ∈_ |B_ も示せてしまいます。
点検には、主張に出てこない定数についての式を使います（|a ∈_ |D_ など。この前提からは示せてしまいます＝実測）。変数の名前を替えただけの y ∈_ |B_ は goal と同じ意味（自由な変数は「すべての」）なので点検になりません。
集合版の完全な例：`|a ∈ |B` ◀ `x ∈ A` は -| `x ∈ A` p; で一瞬で通りますが、前提 x ∈ A は「すべての x がすべての A に属する」です。点検の式 `|c ∈ |D` ◀ `x ∈ A` も通ってしまう（実測）ので、前提が強すぎると分かります。「A の元はすべて B の元で、a は A の元」という意図なら、定数で書きます。
\(\mathrm{a} \in \mathrm{B}\) \(\blacktriangleleft\) \(\forall x ( x \in \mathrm{A} \Longrightarrow x \in \mathrm{B} )\) ，\(\mathrm{a} \in \mathrm{A}\)
　ソース：thm `|a ∈ |B` ◀ `∀ x (x ∈ |A ⟹ x ∈ |B)` , `|a ∈ |A`　prf `|a ∈ |B` -| `∀ x (x ∈ |A ⟹ x ∈ |B)` , `|a ∈ |A` p;

7.3 探索の結論を本に残す

速くするために試した形、うまくいかなかった形、その理由は、本の末尾などに表示しないメモ !txt で残します。次に同じ本を直す人（AI）が同じ試行を繰り返さずに済みます。例：articles1/25.book の !txt ∃除去に置き換えた（10-06）：… prf 1623→1182字・証明器 約0.34→0.20秒。

8 よく使う証明の形

articles の prf で何度も出てくる形です。例はどれも実際の本の行で、査読を通っています。

8.1 帰納法：IND𝕄 にクラスを代入する

「すべての k ∈ 𝕄 で P(k)」は、帰納法の公理 IND𝕄（0 ∈_ C_ で、m ∈_ C_ ⟹ m suc ∈_ C_ なら 𝕄 ⊂_ C_）の C_ に \{ cls k | P(k) \} を代入して示します。底の段 Lb と一歩の段 Ls を先に置き、代入した IND𝕄 と並べて sos に書きます。例：articles3/0.book の +A（結合法則）。

　代入するクラスの中のほかの変数（ここでは x・y）は自由なままでかまいません。前提の自由変数は「すべての x・y について」の意味です（4.book「自由変数の罠」）。Lb・Ls の m・n と名前が違っても、どちらも「すべての」と読むので同じことです。集合で自然数を作る本（articles2/01.book）では、IND𝕄 の代わりに INDC[D_:=…] を使います（01.book の Lpred）。
　ただし、公理の結論の変数と同じ名前の自由変数を、代入するクラスの中に書いてはいけません。INDC（… and n ∈ 𝕄 ⟹ n ∈_ D_）の D_ に \{ cls k | m + (n + k) = … \} を入れると、クラスの中の n と結論の n は同じ自由変数のまま（付け替えない）なので、「P(n, n)」という弱い主張になって示したいことが出ません。クラスの中は別の名前にするか、[ ∀ n ∈ 𝕄 . … ] のように束縛します（articles2/01.book の L=#𝕄）。

8.2 強い帰納法

「b より小さいすべての数で成り立てば b でも成り立つ」の形は、性質を [ ∀ z ∈ 𝕄 . (z < b ⟹ P(z)) ] にして普通の帰納法を使います。底は「z < 0 となる z は無い」、一歩は L<S（z < b suc ⟹ z < b or z = b）で場合を分けます。最後に L<s（n < n suc）で P(n) を取り出します。例：articles3/0.book の SIND𝕄（性質をクラス変数 D_ への所属にしたもの・次の小節）。

8.3 強い帰納法を定理にする

強い帰納法を何度も使う本では、上の形を1つのクラス変数の Thm にしておくと、使う段は代入した実例を引く1段になります。段の末尾に {D_.-}（D_ への所属を新しい述語に置き替える・1.book の辞書）を付けると -| の段のまま示せ、h; で結べます（多ソートの段 --| … v; で示して -| … h[lift]; で結ぶ書き方もありますが、その OK（〇）は multisort→tfl に依存します・3.book「h; の段の関係」）。名前は prop/thm、自由なクラス変数は D_ にします（6.book「分出公理」の注意）。

　（この Thm は articles3/0.book にあり、1・11・23-1・3b・60・69・69b・80-1・80 が使っています。）

8.4 𝕄 の上の段：閉包の補題と数字の定義を並べる

𝕄 に制限した量化子（[ ∀ m ∈ 𝕄 . … ]・[ m ; n col ∈ 𝕄 ]）を使う段では、式に出てくる m + n・m ⋅ n・N + 1 が 𝕄 に入ることを、証明器は前提からしか知りません。そこで前提に、閉包の補題（+∈𝕄・⋅∈𝕄）と 𝕄0s（0 ∈ 𝕄 と suc で閉じること）を並べ、数字を使うなら定義 1.・2. も並べます。例：articles3/0.book の LA1。

　これらを1つ外しただけで timeout することがあります（外部の AI の試験では、articles3/0 の上で m ⋅ 1 = m（articles3/0 の隠し補題 L⋅1 と同じ式）を示す段から L0+ を外すと timeout しました）。段が落ちたら、まずこの並びが揃っているかを見ます。

8.5 and の片側だけ引く：P&l・P&r

公理や定理が「A かつ B」の形のとき、段に要るのが片側だけなら、Prop を分けずに P&l（左）・P&r（右）と書いて引けます。前提の付いた H ⟹ A and B は H ⟹ A／H ⟹ B、\\{ And A \\ B \\} は A／B です。片側だけを sos に置くと、証明器が探す範囲が狭くなります。

　（articles2/01.book の公理 Ax+ と、同じ本の段。Ax+&l は [ m ; n col ∈ 𝕄 ] ⟹ m + n ∈ 𝕄 です。）
仕組み：compile が prf の頭に段 Ax+&l <- `[ m ; n col ∈ 𝕄 ] ⟹ m + n ∈ 𝕄` -| Ax+ v; を足します（投げ先は Vampire。クラスの語・変数 ∈_・X_ などを含む Prop では --| Ax+ v;）。切り出した式が本当に Ax+ から出るかは、この段を証明器がいつも通り確かめます。決まりは次の4つです。
　・◀ の右には元の名前を書く（◀ W. , ax_s , Ax+）のが基本です。主張に Ax+&l と書くと、その前提は片側の式として公開され、後の Thm で使うときはその式を支える必要があります。最後の h; の段の sos も主張と同じにします。
　・P は本で式を書いた Prop（prop 名 <- `式`・prop/thm 名 <- `式`）で、import した本の Prop でも使えます。DB の Prop（式が本に無いもの）には使えません。
　・切るのは、括弧の外の and がちょうど1つのときだけです（結論全体を囲む ( … ) は外して見ます）。or・⟺ がある式や、and が2つ以上ある式は切らず、FAIL: unintroduced sos name: P&l で落ちます。P&r&l のような重ね書きはできません。
　・prf の中で同じ名前 P&l <- … を自分で定義したときは、その定義が使われます（compile は段を足しません）。

8.6 同じ前提の列に名前を付ける：props

◀ の右や sos に同じ Prop の並びを何度も書くときは、props 名 <- P1 , P2 , … で列に名前を付けられます。sos の項にその名前を書くと、compile が中身の並びに置き換えます（査読するのは置き換えた後・◀ の右の表示は書いた名前のまま）。

　置き換えるのは sos の項そのものだけです（slash の / 名・段の名前・代入 名[…] は置き換えません）。列はその本の中だけで使え、import した本には運びません。前に定義した列の名前を中に書くと、その中身に展開されます。prf の中で同じ名前のラベルを定義した prf では展開しません。
　列の名前には . , ! ' ` [ ] / | : & と O を使えません。紹介した Prop・import した Prop・let と同じ名前も compile が拒否します（後から同じ名前を置くのも拒否）。本で紹介していない DB の Prop（ax_s など）と同じ名前は compile では見分けられず、列の方が優先されるので、そういう名前は付けないでください。

8.7 等号を開かない：W.!=.

common/word_basis.book は =. を X = Y ⟺ X =_ Y（外延の形）と定義しています。そのため / W. は等号もすべて ∀ w (w ∈ X ⟺ w ∈ Y) の形に開きます。Book 内定数の定義 |g =_ |g_ のように、証明で等号として置き換えに使いたい式まで開くと、証明器は置き換えに使えなくなります。
等号を残したいときは、=. を除いた W.!=.（所属の形で開くなら W.'!=.）を使います（4.book の W.!名.＝名の定義だけ開かない）。例：articles2/00.book の Lgi -| hyg ///// W.'!=. , …。

8.8 goal と sos で形を揃える

slash で開くと、同じものが goal と sos で違う形になることがあります（goal は A ∈ ℘ X のまま、sos は A ⊂ X まで開いた、など）。2つを結ぶ定義が sos に無いと、証明器は証明できません。slash_cli で両方の開いた形を見て、残った方の定義（℘.'・⊂. など）を sos に足すか、両方を同じ深さまで開きます。
goal に付けた slash は goal だけを開きます。sos の補題・仮定に同じ語があるなら、その項にも slash を付けます（-| 名 // W.）。一階の段（-|）の sos には定義（⊂.・→. など）を置かず、slash で開きます。sos に定義を置くのは、slash の書けない多ソートの段だけです。例：articles1/25.book の LZ（goal も仮定 hyG も2層開く）。

　開く深さは全部の項で揃えます。同じ補題を sos に2回引かないと示せないなら、「閉じたまま使う所」と「元ごとに開いて使う所」が混ざっているサインです。

8.9 演算の強さは word ごと

演算の結合の強さは word ごとに DB で決まっています。数の演算は普通の数学と同じで、後置の suc が最も強く、↑（累乗・右結合）、⋅、+ の順です。例：2 ⋅ n ↑ 2 は 2 ⋅ (n ↑ 2)、m ⋅ n + j は (m ⋅ n) + j。ほかの語との組み合わせで迷ったら括弧を書くか、slash_cli.php の前置記法（[⋅ 2 [↑ n 2]]）で確かめます。

8.10 名前の付け方

Prop の名前（prop・let/thm・props）には、区切りの文字（空白・backtick・( ) [ ] { }・, ;）と、それだけで式になる綴りを使えません。それだけで式になる綴りは、| で始まる記号（|a・|q・|P^）、^ の付いた名前（P^）、⊤・∅・0 などの記号です。Q1・K・L10 のような名前にします。
prf のラベルは2種類です（段の書き方は 3.book「prf の1段」）。
　・ 名 <- `式` は主張（式）の名前で、段の goal・sos に書けます。
　・ 名 := `項` は式の中の記号を置き換える名前で、段の左に単独で書き（x := `|?f ( |a )` ;）、backtick の式の中で使います。名前だけを段の goal・sos に書くと「Form の名前 H は段の goal・sos には書けません」で落ちます。AA := ZZZ はラベル ZZZ の別名です。
後の段では名前を中身に置き換えて読むので、意味が変わる付け方は査読が落とします。ラベルの名前の規則は <- でも := でも同じです。
　1. 使う前に定義する：前の段（backtick の式の中も）に出た名前を、後からラベルにはできません（「前の段に出てきた名前「a」に後からラベルを付けています」）。定義を前へ移します。別名の鎖（ZZZ <- … ; AA := ZZZ ; B := AA）も先の名前から順に書きます。
　2. この thm の行に出る名前にしない（主張と、◀ の右の式の中。∀ で束縛した変数も。前に示した別の Thm の名前は 4）：「thm の行の主張に出てくる名前「x」に…」か「ラベル `u` と同じ名前が、後の段の式の中に出ています」で落ちます。
　3. 本で紹介した prop の名前にしない：「prf の中で、本が紹介した prop と同じ名前「A」にラベルを付けています」で落ちます。
　　2・3 の直し方：ラベルの名前を替え、ラベルを使う段も替えます。式の中の変数（|?g ( y ) の y）・prop の名前・最後の段は替えません。例 thm … ◀ K の prf の K <- …; K -| K p; goal -| K h; は K1 <- …; K1 -| K p; goal -| K h; にします（段の左のラベルだけ K1。sos の K と最後の段の K は本の prop K）。
　4. 前に示した別の Thm に出る名前（この thm の行の名前は 2）：
　　・ その Thm の sos に出る → この prf では使えません（h; の FAIL に「前に示した Thm「…」（ラベル a）は…使えません」と添えられます）。ラベルを前の Thm に出ない名前（Le1 など）に替えます。
　　・ その Thm の主張にだけ出る変数 → ラベルの名前をその変数にそろえると、中身を入れた式として使えます。例：前の Thm `x = x` ◀ O は、x := `|?f ( |a )` の prf で |?f ( |a ) = |?f ( |a ) として使えます。
　　　別の名前（w := …）にすると当たらず、h; が「この段の goal を示した段も、使える前の Thm も見つかりませんでした」か「項にこの prf のラベル（w）が入っています」で落ちます。
　　　中身は同じ種類の項（集合の変数なら集合の項）にします。中身の記号が前の Thm の主張にも出る（∃ y の y に捕まる）ときは使えません。
　5. 1語としてだけ当たる：ラベル a は |a・|?a の中を、ラベル P は P^ の中を置き換えません。|a を置き換えたいなら |a := `|b` と書きます。
照合は中身、最後の段は綴り：h; は中身で照合するので、段の sos では同じ式に付けた名前どうし・名前と式は同じ項です（3.book「書き換えだけの違い」）。ただし最後の段は thm の行と同じ綴り（goal も sos も）で書きます（違うと「prf の最後の段が thm の主張と違います」）。thm の行の ◀ の右には prop の名前か式を書きます（prf のラベルを書くと、主張が prf を読まないと分からなくなります）。

8.11 固定化：定数で示して h[fix]; で戻す

写像 f や集合 X について示す長い証明は、f・X を定数 |f・|X にして書き、最後の段で変数に戻します。証明器に渡る問題で変数が定数になるので探索が軽くなります。作るもの（単射・対角クラスなど）は 名_ := `式` ; で式に名前を付け、その式と等しい集合は、仮定 hyG <- `|g =_ |g_` ; で定数 |g と結ぶか、ax_s[C_:=`|g_`] を sos に置いて証明器に任せます（6.book「同じ段の3つの書き方」）。
戻すのは h[fix]; の段です。結論の段 goal -| W. , ax_s h[fix]; か、途中の段 L <- `変数の式` -| W. , ax_s h[fix];（後の段で L を引ける）。h; のままでは戻りません。例：articles1/63.book の X ≤# ℘ X（定数 |X の bar を外す）。

　主張の前件（f ∈ X → Y など）は、どれかの段の sos に仮定として1回は現れる必要があります。h[fix]; は、段の sos に仮定として出た式（の |f・|X を f・X に戻したもの）を集めて、主張の「前件 ⟹ 結論」を組み立てるからです。集めた仮定が前件を過不足なく覆わないと、組み立てた式が主張と一致せず落ちます。数学的には要らない仮定でも、1回は sos に引きます。途中で変数に戻して別の仮定で始め直すより、定数のまま最後まで進めて1回だけ戻す方が短くなります。小さな段の集まりや、もともと速い段は、固定化しても速くなりません（Hyperion の分だけ遅くなることもある）。

8.12 同じ塊を何度も書くなら語にする

「増加列」「部分列」のような条件を毎回展開して書くと、式が長くなり証明器が遅くなります。本で word を紹介し、prop で定義して、式の中では1つの記号として書きます（引数が多いものは対 \< pr x ; P \> に包んで中置2項の語に）。証明器には原子式の照合になります。例：articles3/31.book（Ramsey）の x ⇈ P・\< pr x ; P \> ⊑ \< pr v ; L \>。展開して書いていた版では1つの段が Vampire で約30秒、語にして約1.2秒になりました（2026-10-08 の実測）。
　語を開くときは / W. ではなく名指し（/ ⇈. / ⊑.）にします。W. は =. も開くので、等号が外延性の式に化けて timeout しました。

9 本を分ける：import と private theorem

何冊かで同じ準備を使うときは、準備を別の本にして import します。例：articles2/02.book（数える道具）を 58a・58b・88a が import し、どれも主定理の周りだけの小さな本になりました。import した本は証明し直さず、保存された査読結果を使います。

9.1 import で運ぶもの・運ばないもの

運ぶ：紹介（word・prop・abbr・lower）と、証明済みの Thm（thm prop/thm let/thm、! 付きも）。goal は名前でも `式` でもかまいません。`式` の Thm は、使う側の sos に `式` と書いて引きます（articles2/52b.book の `0 ∈ 𝕄`・`1 ∈ 𝕄` は 01.book の Thm）。let/thm の名前も引けます。import した本がさらに import した本の Thm も届きます。
運ばない：thm- 系（private theorem）の Thm と名前、sos に `式` を含む Thm（その本だけの定数に頼るかもしれない）、ヘッダの formel・thmel。
sos に let で置いた名前を含む Thm は、後の Thm からも使えません（同じ名前を後で置き直せるため）。

9.2 private theorem

thm- prop/thm- let/thm-（! 付きも）は、その本の中（後の Thm・後の頁）では使えて、import した本には運ばない Thm です。Lean の private theorem と同じ考え方です。! は表示するか、- は運ぶか、で別のことなので、!thm- と組み合わせられます。
使いどころ：準備の本の中だけで使う作業用の補題です。運ばなければ、import した本は同じ名前（L01・LD など）を自由に使えます。逆に、使う側の本で使いたい Thm には - を付けません。
例（説明のための形・実際の 0.book では L01 は ∪=#+ の prf の中のラベル）：

　この本の中では ∪=#+ の prf が L01 を引けます。この本を import した本からは ∪=#+ は使えますが、L01 を sos に書くと FAIL: unintroduced sos name: L01 で落ちます。