book集

section 早見表
txt この Book は、prf を実際に書くときの判断（どの投げ先に投げるか・FAIL したら何をするか・難しい定理をどう進めるか）をまとめた実践編です。定義や記号は 6.book のもの（ヘッダは <code>import 6</code> だけ。thmel 行を書かないので .thmel は /common/default）。基本の書き方は 3.book、slash の規則は 4.book、クラスと -|・--| は 5.book にあります。灰色の枠の prf の例は、ソースでは1行ですが、表示（Web の画面か <code>ai_reading.php</code>）では段ごとに改行されます。
txt まず表にまとめます。理由と実測は後の節にあります。
txt <table border="1"><tr><th>段の式に含まれるもの</th><th>書く段</th><th>理由・実測</th></tr><tr><td>クラス変数も述語変数も無い（一階の式）</td><td><code>-| … p;</code></td><td>掲載した例では最速。まず試す候補（「一階の式」の小節）</td></tr><tr><td>クラス変数（X_ など）</td><td><code>◀ … v;</code> か <code>--| … v;</code>（本が紹介した Wc. の定義も前提に入る＝5.book）</td><td>-| は「|0 翻訳不可」。◀ … p; も通るが、相対化で式が大きくなるので項が増えると遅くなりやすい（「クラス変数」の小節。遅くなる実例は「一階の式」の小節の5項）。◀ … v; と --| … v; はどちらも通る例が多い（--| はアロー関数を fn-elim・内包を cls-elim し Wc. を足す＝5.book）</td></tr><tr><td>内包 \{ cls x | … \} を含む多ソートの段</td><td><code>v;</code></td><td>掲載した例では vampire+ が速かった（「内包記法と分出公理」の小節）</td></tr><tr><td>述語への代入が要る（schema を使う段）</td><td>実例 <code>SOURCE[P:=θ]</code> を sos に書いて <code>v;</code> など</td><td>証明器に述語を探させない。prop の高階変数にはどの backend でも代入しない（「述語変数の代入」の小節）</td></tr><tr><td>goal の断片が自明で数が多い</td><td><code>p[whole];</code></td><td>起動の回数が減る（4.book）</td></tr><tr><td>1段で通らない</td><td>補題に切って段ごとに投げ先を選び、最後を h; で結ぶ</td><td>p; で timeout する段も v; なら一瞬で通ることがある（「一階の式」の小節の5項：◀ p; は timeout、◀ v; は 0.012秒）</td></tr></table>
txt 証明器は、時間内に証明が見つからないと timeout を返します。探索を早く打ち切って not_proved を返すこともあります（Prover9 の not_proved は「証明が見つからなかった」で、無いことが確定したわけではありません）。Vampire の CounterSatisfiable は「渡した問題には反例がある」という答えです。どちらも FAIL で、主張が偽という判定ではありません。
txt FAIL したときの次の一手（原因は候補で、どれかを確かめながら試します）。FAIL の行の頭（<code>zz.book:11</code>）は thm の行、文言の「13行目の段」は落ちた段の行です。直す所（ラベルの定義など）はその前の行にあることもあります。
txt <table border="1"><tr><th>症状（FAIL の文言）</th><th>意味</th><th>次の一手</th></tr><tr><td>「|0 翻訳不可: … ∈_ が残っています」</td><td>クラス変数を含む段を -| で投げた</td><td><code>◀ … v;</code> か <code>--| … v;</code> にする</td></tr><tr><td>すぐ not_proved（Vampire なら CounterSatisfiable）</td><td>この前提とこの展開では証明が見つからなかった（CounterSatisfiable なら、渡した問題には反例がある）。定義が開ききっていない・前提（橋渡しの定義や補題）が足りない・主張が偽のどれか</td><td><code>review_cli.php … --inputs</code> で投げた入力を読み、開いていない記号が残っていれば、goal と、同じ記号を含む sos の項の両方に / を足し（「goal と sos で形を揃える」）、足りない補題は前提に置く（「実例①」「実例②」）</td></tr><tr><td>timeout</td><td>考えられる原因：定義を開きすぎ（/ W. の本数が多い・=. の外延性など）か、1段に詰め込みすぎ。必要な前提を消した場合もある</td><td><code>W.!名.</code>（名は開かない定義の名前。例 <code>W.!=.</code>）で開く定義を減らす・補題に切る・投げ先を替える</td></tr><tr><td>h; の段で落ちる</td><td>各段は示せたが、組み合わせても thm の主張にならない</td><td>最後の段（h;）の goal・sos が thm の行と同じか、途中で使った定義が W. に入っているか、h; の段の関係がつなぐ段と合っているか（/ で展開した段をつなぐなら -| h;・3.book「h; の段の関係」）を確かめる。sos の項がラベルを含む式なら、ラベルの名前を前の Thm の変数にそろえる（「名前の付け方」4）</td></tr><tr><td>「前の段に出てきた名前「a」に後からラベル…」「本が紹介した prop と同じ名前「A」にラベル…」「thm の行の主張に出てくる名前「x」に…」「ラベル &#96;u&#96; と同じ名前が、後の段の式の中に…」</td><td>ラベルの付け方の誤り</td><td>定義を使う段より前へ移す／別の名前に替える（「名前の付け方」）</td></tr><tr><td>「prf の最後の段が thm の主張と違います」</td><td>最後の段の goal・sos が thm の行と綴りで違う（中身が同じラベルの名前でも違う）</td><td>最後の段を thm の行と同じ綴りに直す（「名前の付け方」）</td></tr><tr><td>「Prop の名前 … は付けられません」</td><td>名前の付け方の誤り（「名前の付け方」）</td><td>名前を替え、使う所も替える。査読はここで止まるので、直すと次の FAIL が出ることがある</td></tr></table>
txt 表の各行の詳しい見分け方と、実際に直した例は「失敗の種類を見分ける」の節にあります。
subsection backend
txt prfの各段は、末尾の投げ先の文字で backend を選びます（仕組みは3.book）。どれに投げるかで、通るか・どれだけ速いかが大きく変わります。
txt ・<i>prover+</i>（p;）… Prover9 を使います。一階言語のThmを受け取ります。<code>-|</code> の段は Thm を <span style="color:brown">|cvt+|0</span> で翻訳して、<code>◀</code> の段は{s,c}ソートを一項述語で相対化して投げます。goal を断片に割って投げ、すべて証明できたら OK です（割らない p[whole]; は4.book）。
txt ・<i>vampire+</i>（v;）… Vampire を使います。{s,c}ソート言語のThmを、ソートを保ったまま（多ソートの TFF 形式で）受け取ります。
txt ・<i>satallax+</i>（s;）… Satallax を使います。高階言語のThmを受け取ります。Thm に自由に現れる命題変数・述語変数は、Thm 全体で1つの記号として渡します（<span style="color:brown">|v-elim</span> をした p; v; と同じ意味・7.book）。 ただし .thmel に <code>satallax+ predicate:all</code> と書いた本で、<code>--| … s;</code> の段の sos に素の名前で書いた <code>∀ ?R^ ( … )</code> の prop だけは、その式の中で ?R^ を ∀ で閉じた高階の公理として渡します（下の「述語変数の代入」）。
txt ・<i>hyperion</i>（h;）… 証明器ではありません。prf の前の段で示したThmを組み合わせて、thm の主張を導けるかを確かめます（例外：関係をまたいで Thm を確かめ直すときだけ Vampire を呼ぶ・3.book「h; の段の関係」）。
txt 投げ先の文字は .thmel の backend 行が決めます（1.book の .thmel の節に表があります）。今ある .thmel はどれも p v h s の4つを持ちます。

newpage

section 進め方
txt 難しい定理になると、一回で良いprfを書くことはまずできません。試して、失敗の仕方を読んで、次の一手を決める、の繰り返しになります。このBookはその進め方を、実際に試した記録で見せます。定義や記号は 6.book のものを使います（ヘッダで <code>import 6</code>）。
txt 1回の試みは次の順で進めます。
txt 　① あらすじ：紙で証明するなら、どの定義を開き、どこで場合分けし、どんな補題が要るかを先に書く。
txt 　② 予測：試す前に「これで通るはず」「落ちるならこう落ちる」を決める。
txt 　③ 試す：1回に変えるのは1か所だけ（slashの本数・前提・投げ先のどれか1つ）。
txt 　④ 症状を読む：FAILの文言で、どの種類の失敗かを見分ける（「失敗の種類を見分ける」の節）。
txt 　⑤ 通ったら：前提を1つずつ外して最小にし、前提が強すぎないかを点検する（「通ったあとで」の節）。思ったより速く通ったときほど疑います。
txt 同じ方向の失敗が2〜3回続いたら、同じ所をいじり続けずに、あらすじ（補題の切り方）から考え直します。
subsection 速く試す：prf_trial
txt 1か所ずつ変えて何度も試すときは、本を書き換えずに <code>.claude/prf_trial.php &lt;本&gt; &lt;Thm の行番号か行の一部&gt; &lt;候補&gt; …</code> で、1つの Thm に prf の候補をまとめて当てます（<code>=</code> だけの候補は今の prf）。前の Thm は1回だけ流し、証明器の結果をディスクに覚えるので、候補ごとに走るのは変えた段だけです。
txt 　・ 結果の JSON は<b>良い順に並べ替えて</b>出ます。どの候補が通ったかは、候補の文字列と照らして確かめます（取り違えて誤った prf を書いたことがあります）。
txt 　・ <code>--quick</code> は最後の h; のつなぎを省いた速い試しです。ok は「証明器の段が通った」だけなので、決めた prf は最後に本に書いて <code>review_cli.php</code> で査読します。
txt 　・ 秒を比べるときは、<code>MATHEL_PROVER_CACHE_DIR</code> を候補ごとに新しい場所にして（同じ場所だと後の候補が覚えた結果で得をする）、複数回測ります。1本目は暖機で遅く出ます。測り終えたキャッシュは消します。

section 実測で見る使い分け
txt 以下の時間はこのサーバーでの実測です。「一階の式」「クラス変数」の小節は 2026-10-16 にこの本と同じ default.thmel で測り直し（キャッシュ無し・2回）、「内包記法」「述語変数」の小節は 6.book の段の実測（2026-09-28）です。時間は負荷で揺れます。待ち時間は default.thmel で Prover9・Vampire とも20秒です（zf.thmel は Prover9 10秒・Vampire 90秒）。
subsection 一階の式：まず -| … p;
word +
prop +結合則 <- `x + (y + z) = (x + y) + z`
thm `x + (y + (z + (w + u))) = (((x + y) + z) + w) + u` ◀ +結合則
prf `x + (y + (z + (w + u))) = (((x + y) + z) + w) + u` -| +結合則 p;
txt 同じThmを、関係と投げ先の組み合わせだけ替えて比べました（4項は `x + (y + (z + w)) = ((x + y) + z) + w`）。
txt 　4項 … -| p; 0.009秒　◀ v; 0.011秒　◀ p; 0.38秒　-| s; 0.63秒
txt 　5項 … -| p; 0.007秒　◀ v; 0.012秒　-| s; 0.63秒　◀ p; timeout（20秒）
txt c-Form を含まない一階の式なら、-| … p; が速く確実です。◀ … p; は{s,c}ソートの相対化で式が大きくなり、項が増えると急に遅くなります。satallax+ は高階の探索をするので、一階の式には割高です。

subsection クラス変数：◀ に替える
thm `∀ x (x ∈_ X_ ⟹ x ∈_ Y_) and y ∈_ X_ ⟹ y ∈_ Y_` ◀ O
prf `∀ x (x ∈_ X_ ⟹ x ∈_ Y_) and y ∈_ X_ ⟹ y ∈_ Y_` ◀ O v;
txt クラス変数（| の付かない X_）を含むThmは、-| では翻訳できず「|0 翻訳不可: cvt+ 後に ∈_ が残っています」という査読エラーになります。◀ … v; なら{s,c}ソートのまま投げられます。
txt 　◀ v; 0.010秒　◀ p; 0.008秒　◀ s; 0.010秒　-| p; 翻訳不可
txt この小さい例では ◀ p; が最速ですが、差はわずかです。上の理由で、c-Form を含む段は ◀ … v; を勧めます。
txt クラス定数（|A_ など）だけなら、-| は <span style="color:brown">|cvt+</span> で翻訳できます（3.book の Hall の例は ◀ v; で示しています）。

subsection 内包記法と分出公理：v;
txt 6.book の `¬ Exi 𝕍`（prop 名 ¬Exi𝕍）は、以前は分出公理の実例 <code>Le &lt;- &#96;∃ X \, 𝕍0 ⊂_ X ⟹ Exi 𝕍0&#96; --| ax_s</code> を示してから使う2段の多ソートの証明でした。
txt 今は実例を代入 <code>ax_s[C_:=&#96;𝕍0&#96;]</code> で sos に直接書き、<code>¬Exi𝕍 -| ax_s[C_:=&#96;𝕍0&#96;] p;</code> の1段で証明器に投げる段が済みます（あとは h; で結ぶ・実例を証明器に示させない分だけ速い）。
txt クラスの内包記法を含む多ソートの段は、vampire+ が安定して速いです。

subsection 述語変数の代入：実例を sos に・satallax+ に探させる
txt 6.book の <code>ax_s ◀ ax_s'</code> は、分出公理 ax_s'（<code>∀ ?R^ ( … )</code> の prop）の ?R^ に <code>x ∈_ C_</code> を代入した実例 <code>ax_s'[?R^:=&#96;x ∈_ C_&#96;]</code> を sos に直接書いた v; の段（約0.1秒）と、「ax_s' から導かれる」形にまとめる h; の段で示します。
txt .thmel に <code>satallax+ predicate:all</code>（述語変数の ∀ をλ項すべての上で読む＝高階論理）と書いた本で、∀ ?R^ を書いた prop を <code>--| … s;</code> の段の sos に素の名前で書くと、satallax+ には「すべての ?R^ について」の高階の公理（\(\forall R\,\psi(R)\)）として渡り、Satallax が代入する式を自分で探します。単純な代入なら速く見つかります（例：<code>∀ ?R^ ( [ ∃ x \, ?R^ (x) ] ⇒ [ ∀ x \, ?R^ (x) ] )</code> から <code>∀ x \, ∀ y \, x = y</code> を 0.01秒＝\(R:=\lambda z.\,z=a\) を見つけた）。置換公理から分出公理（<code>ax_s --| ax_r s;</code>）は 20秒で timeout しました（代入する式に ！ の条件とクラスの内包が要る）。
txt 代入する式が分かっているときは、実例を自分で書く方が速く確実です。素の名前をどの段に書けるかは 6.book「分出公理」の節の表のとおりです。∀ を書かない prop の高階変数は Thm の中で1つの決まった述語なので、どの backend でも代入しません（7.book）。

newpage

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

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

section 失敗の種類を見分ける
txt FAIL の文言は、大きく4種類に分かれます。種類によって次の一手が違います。
txt <b>1. 証明器が動く前に落ちた</b>（「本が紹介していない word」「翻訳不可」「… が余っています」など）：書き方か、関係（-| と --|）の選び方の問題です。数学の中身はまだ試されていません。文言が指す語・行を直します。
txt <b>2. すぐに「示せない」</b>（Prover9 の No proof found が短時間で出る、Vampire の CounterSatisfiable）：この前提とこの展開のままでは証明が見つからなかった、ということです（Prover9 は探索を制限しているので、「示せないことが確定した」とまでは言えません）。考えられるのは、定義が開ききっていない（実例①）、前提が足りない、主張が偽、のどれかです。CounterSatisfiable は、証明器に渡した問題（翻訳した後の式）に反例があるという意味で、元の主張が偽だとは限りません。開いていない記号が入力に残っていないか、足りない定義・補題が無いかを先に疑います。
txt <b>3. 時間切れ</b>（timeout）：探索が重い、ということです。開きすぎ（<code>W.!名.</code> で、名の定義を開かないようにする）、証人を自力で探させている（実例②）、1つの段に詰め込みすぎ（補題に分ける）、のどれかを疑います。前提を削りすぎた場合も timeout になることがあります。
txt <b>4. 証明器の段は通ったのに、最後の h; の段で落ちた</b>：各段は示せていますが、それらを組み合わせても thm の主張にならない、ということです。多くは段どうしのつなぎ方の問題です。最後の段の goal・sos が thm の行と合っているか、途中で使った定義が W. に入っているか（入っていない定義で開いた段はつなげません）を確かめます。「使おうとした Thm の sos の項（…）を、この段の sos から導けませんでした」は、その項を結論に持つ段も前の Thm も見つからなかった、という意味です。項がラベルを含む式なら、ラベルの名前が前の Thm の変数とそろっているか（「名前の付け方」の4）も確かめます。
txt 投げ先（p; v; s;）の選び方は最初の早見表にあります。
subsection 実例：症状から直すまで
txt ・ 2. すぐに示せない → / を足す。最初に書いた prf <code>&#96;X ⊂ X ∪ Y&#96; / W. -| O p; &#96;X ⊂ X ∪ Y&#96; -| W. h;</code> は「Prover9 not_proved: No proof found.」。<code>--inputs</code> で見た入力は <code>formulas(sos).end_of_list.formulas(goals).(all w1 (in(w1,xX) -> in(w1,cup(xX,xY)))).end_of_list.</code> で、⊂ は開いたが ∪ の所属 <code>cup(xX,xY)</code> が残っています。/ を2本にすると通ります。
thm `X ⊂ X ∪ Y` ◀ W.
prf `X ⊂ X ∪ Y` // W. -| O p; `X ⊂ X ∪ Y` -| W. h;
txt 　ソース：<code>thm &#96;X ⊂ X ∪ Y&#96; ◀ W.</code>　<code>prf &#96;X ⊂ X ∪ Y&#96; // W. -| O p; &#96;X ⊂ X ∪ Y&#96; -| W. h;</code>
txt ・ 1. 証明器が動く前に落ちた → 関係を替える。クラス変数の推移律に <code>-| O p;</code> と書くと「capsule-error: |0 翻訳不可: cvt+ 後に ∈_ が残っています。クラス変数への所属は述語に置き換えられません。」。{s,c}ソートのまま Vampire に投げると通ります（<code>◀ O v;</code> でも同じく OK＝実測）。
thm `[ chain X_ ⊂_ Y_ ⊂_ Z_ ] ⟹ X_ ⊂_ Z_` ◀ O
prf `[ chain X_ ⊂_ Y_ ⊂_ Z_ ] ⟹ X_ ⊂_ Z_` --| O v;
txt 　ソース：<code>thm &#96;[ chain X_ ⊂_ Y_ ⊂_ Z_ ] ⟹ X_ ⊂_ Z_&#96; ◀ O</code>　<code>prf &#96;[ chain X_ ⊂_ Y_ ⊂_ Z_ ] ⟹ X_ ⊂_ Z_&#96; --| O v;</code>

section 通ったあとで
subsection 前提を最小にする
txt 通ったら、前提を1つずつ外して試します。外しても通る前提は要らなかったものです。前提が少ないほど探索は速く、読む人にも何を使ったかが分かります。
subsection 前提が強すぎないかを点検する
txt 前提に量化子で縛られていない変数を書くと、「すべての〜について」の意味になります。そのせいで前提が矛盾していると、何でも証明できてしまいます。4.book の例がそれです。
thm `⊥` ◀ `x {/}= y`
prf `⊥` -| `x {/}= y` p;
txt 前提から ⊥（偽）が示せてしまうなら、その前提は矛盾しています。思ったより簡単に通ったときは、goal を ⊥ に替えて同じ前提で試すと点検できます。
txt ただし、⊥ が示せないことは、前提が矛盾していないことの証明にはなりません（見つからなかっただけかもしれません）。また、矛盾していなくても強すぎる前提があります。
txt 例：5.book の <code>x ∈_ |B_ ◀ x ∈_ A_</code>。前提 <code>x ∈_ A_</code> は自由な x・A_ を含むので「すべてのもの x が、すべてのクラス A_ に属する」という式です。A_ に |B_ を入れれば goal そのものになります。この前提から ⊥ は示せません（実測で反例あり）が、どんな式 <code>… ∈_ |B_</code> も示せてしまいます。
txt 点検には、主張に出てこない定数についての式を使います（<code>|a ∈_ |D_</code> など。この前提からは示せてしまいます＝実測）。変数の名前を替えただけの <code>y ∈_ |B_</code> は goal と同じ意味（自由な変数は「すべての」）なので点検になりません。
txt 集合版の完全な例：<code>&#96;|a ∈ |B&#96; ◀ &#96;x ∈ A&#96;</code> は <code>-| &#96;x ∈ A&#96; p;</code> で一瞬で通りますが、前提 x ∈ A は「すべての x がすべての A に属する」です。点検の式 <code>&#96;|c ∈ |D&#96; ◀ &#96;x ∈ A&#96;</code> も通ってしまう（実測）ので、前提が強すぎると分かります。「A の元はすべて B の元で、a は A の元」という意図なら、定数で書きます。
thm `|a ∈ |B` ◀ `∀ x (x ∈ |A ⟹ x ∈ |B)` , `|a ∈ |A`
prf `|a ∈ |B` -| `∀ x (x ∈ |A ⟹ x ∈ |B)` , `|a ∈ |A` p;
txt 　ソース：<code>thm &#96;|a ∈ |B&#96; ◀ &#96;∀ x (x ∈ |A ⟹ x ∈ |B)&#96; , &#96;|a ∈ |A&#96;</code>　<code>prf &#96;|a ∈ |B&#96; -| &#96;∀ x (x ∈ |A ⟹ x ∈ |B)&#96; , &#96;|a ∈ |A&#96; p;</code>
subsection 探索の結論を本に残す
txt 速くするために試した形、うまくいかなかった形、その理由は、本の末尾などに表示しないメモ <code>!txt</code> で残します。次に同じ本を直す人（AI）が同じ試行を繰り返さずに済みます。例：articles1/25.book の <code>!txt ∃除去に置き換えた（10-06）：… prf 1623→1182字・証明器 約0.34→0.20秒。</code>

section よく使う証明の形
txt articles の prf で何度も出てくる形です。例はどれも実際の本の行で、査読を通っています。
subsection 帰納法：IND𝕄 にクラスを代入する
txt 「すべての k ∈ 𝕄 で P(k)」は、帰納法の公理 IND𝕄（<code>0 ∈_ C_</code> で、<code>m ∈_ C_ ⟹ m suc ∈_ C_</code> なら <code>𝕄 ⊂_ C_</code>）の C_ に <code>\{ cls k | P(k) \}</code> を代入して示します。底の段 Lb と一歩の段 Ls を先に置き、代入した IND𝕄 と並べて sos に書きます。例：articles3/0.book の +A（結合法則）。
txt <div style="font-family:monospace;background:#f4f4f4;border:1px solid #ddd;padding:6px 10px;overflow-x:auto;white-space:nowrap">prf Lb &lt;- &#96;[ m ; n col ∈ 𝕄 ] ⟹ (m + n) + 0 = m + (n + 0)&#96; -| +𝕄 , +∈𝕄 p;<br>&nbsp;&nbsp;&nbsp;&nbsp;Ls &lt;- &#96;[ m ; n ; k col ∈ 𝕄 ] and (m + n) + k = m + (n + k) ⟹ (m + n) + k suc = m + (n + k suc)&#96; -| +𝕄 , +∈𝕄 p;<br>&nbsp;&nbsp;&nbsp;&nbsp;+A -| IND𝕄[C_:=&#96;\{ cls k | (x + y) + k = x + (y + k) \}&#96;] , Lb , Ls p;<br>&nbsp;&nbsp;&nbsp;&nbsp;+A -| 𝕄0s , IND𝕄 , +𝕄 h;</div>
txt 　代入するクラスの中のほかの変数（ここでは x・y）は自由なままでかまいません。前提の自由変数は「すべての x・y について」の意味です（4.book「自由変数の罠」）。Lb・Ls の m・n と名前が違っても、どちらも「すべての」と読むので同じことです。集合で自然数を作る本（articles2/01.book）では、IND𝕄 の代わりに INDC[D_:=…] を使います（01.book の Lpred）。
txt 　ただし、公理の結論の変数と同じ名前の自由変数を、代入するクラスの中に書いてはいけません。INDC（<code>… and n ∈ 𝕄 ⟹ n ∈_ D_</code>）の D_ に <code>\{ cls k | m + (n + k) = … \}</code> を入れると、クラスの中の n と結論の n は同じ自由変数のまま（付け替えない）なので、「P(n, n)」という弱い主張になって示したいことが出ません。クラスの中は別の名前にするか、[ ∀ n ∈ 𝕄 . … ] のように束縛します（articles2/01.book の L=#𝕄）。
subsection 強い帰納法
txt 「b より小さいすべての数で成り立てば b でも成り立つ」の形は、性質を <code>[ ∀ z ∈ 𝕄 . (z &lt; b ⟹ P(z)) ]</code> にして普通の帰納法を使います。底は「z &lt; 0 となる z は無い」、一歩は L&lt;S（<code>z &lt; b suc ⟹ z &lt; b or z = b</code>）で場合を分けます。最後に L&lt;s（<code>n &lt; n suc</code>）で P(n) を取り出します。例：articles3/0.book の SIND𝕄（性質をクラス変数 D_ への所属にしたもの・次の小節）。
txt <div style="font-family:monospace;background:#f4f4f4;border:1px solid #ddd;padding:6px 10px;overflow-x:auto;white-space:nowrap">SIND𝕄 -| IND𝕄[C_:=&#96;\{ cls b | [ ∀ z ∈ 𝕄 . (z &lt; b ⟹ z ∈_ D_) ] \}&#96;] , Lb , Ls , L&lt;s , 𝕄0s {D_.-} v;</div>
subsection 強い帰納法を定理にする
txt 強い帰納法を何度も使う本では、上の形を1つのクラス変数の Thm にしておくと、使う段は代入した実例を引く1段になります。段の末尾に <code>{D_.-}</code>（D_ への所属を新しい述語に置き替える・1.book の辞書）を付けると -| の段のまま示せ、<code>h;</code> で結べます（多ソートの段 <code>--| … v;</code> で示して <code>-| … h[lift];</code> で結ぶ書き方もありますが、その OK（〇）は multisort→tfl に依存します・3.book「h; の段の関係」）。名前は <code>prop/thm</code>、自由なクラス変数は D_ にします（6.book「分出公理」の注意）。
txt <div style="font-family:monospace;background:#f4f4f4;border:1px solid #ddd;padding:6px 10px;overflow-x:auto;white-space:nowrap">prop/thm SIND𝕄 &lt;- &#96;[ ∀ n ∈ 𝕄 . ([ ∀ z ∈ 𝕄 . (z &lt; n ⟹ z ∈_ D_) ] ⟹ n ∈_ D_) ] ⟹ 𝕄 ⊂_ D_&#96; ◀ W. , 𝕄0s , IND𝕄 , suc𝕄 , +𝕄<br>prf Lb &lt;- &#96;[ ∀ z ∈ 𝕄 . (z &lt; 0 ⟹ z ∈_ D_) ]&#96; / &lt;. -| L≤0 , suc𝕄 , 𝕄0s {D_.-} p;<br>&nbsp;&nbsp;&nbsp;&nbsp;Ls &lt;- &#96;[ ∀ n ∈ 𝕄 . (…) ] and b ∈ 𝕄 and [ ∀ z ∈ 𝕄 . (z &lt; b ⟹ z ∈_ D_) ] ⟹ [ ∀ z ∈ 𝕄 . (z &lt; b suc ⟹ z ∈_ D_) ]&#96; -| L&lt;S {D_.-} p;<br>&nbsp;&nbsp;&nbsp;&nbsp;SIND𝕄 -| IND𝕄[C_:=&#96;\{ cls b | [ ∀ z ∈ 𝕄 . (z &lt; b ⟹ z ∈_ D_) ] \}&#96;] , Lb , Ls , L&lt;s , 𝕄0s {D_.-} v;<br>&nbsp;&nbsp;&nbsp;&nbsp;SIND𝕄 -| W. , 𝕄0s , IND𝕄 , suc𝕄 , +𝕄 h;</div>
txt 　（この Thm は articles3/0.book にあり、1・11・23-1・3b・60・69・69b・80-1・80 が使っています。）
subsection 𝕄 の上の段：閉包の補題と数字の定義を並べる
txt 𝕄 に制限した量化子（<code>[ ∀ m ∈ 𝕄 . … ]</code>・<code>[ m ; n col ∈ 𝕄 ]</code>）を使う段では、式に出てくる <code>m + n</code>・<code>m ⋅ n</code>・<code>N + 1</code> が 𝕄 に入ることを、証明器は前提からしか知りません。そこで前提に、閉包の補題（<code>+∈𝕄</code>・<code>⋅∈𝕄</code>）と 𝕄0s（<code>0 ∈ 𝕄</code> と suc で閉じること）を並べ、数字を使うなら定義 <code>1.</code>・<code>2.</code> も並べます。例：articles3/0.book の LA1。
txt <div style="font-family:monospace;background:#f4f4f4;border:1px solid #ddd;padding:6px 10px;overflow-x:auto;white-space:nowrap">LA1 &lt;- &#96;[ x ; c col ∈ 𝕄 ] and 2 ⋅ x = 2 ⋅ (c + x) ⟹ 2 ⋅ c = 0&#96; -| Ldist , +C , +K , +𝕄 , ⋅∈𝕄 , 𝕄0s , 1. , 2. v;</div>
txt 　これらを1つ外しただけで timeout することがあります（外部の AI の試験では、articles3/0 の上で <code>m ⋅ 1 = m</code>（articles3/0 の隠し補題 L⋅1 と同じ式）を示す段から L0+ を外すと timeout しました）。段が落ちたら、まずこの並びが揃っているかを見ます。
subsection and の片側だけ引く：P&l・P&r
txt 公理や定理が「A かつ B」の形のとき、段に要るのが片側だけなら、Prop を分けずに <code>P&amp;l</code>（左）・<code>P&amp;r</code>（右）と書いて引けます。前提の付いた <code>H ⟹ A and B</code> は <code>H ⟹ A</code>／<code>H ⟹ B</code>、<code>\\{ And A \\ B \\}</code> は A／B です。片側だけを sos に置くと、証明器が探す範囲が狭くなります。
txt <div style="font-family:monospace;background:#f4f4f4;border:1px solid #ddd;padding:6px 10px;overflow-x:auto;white-space:nowrap">prop Ax+ &lt;- &#96;[ m ; n col ∈ 𝕄 ] ⟹ m + n ∈ 𝕄 and m + n =# m ^^pr \{ set ∅ \} ∪ n ^^pr \{ set 1 \}&#96;<br>prf Lb &lt;- &#96;[ m ; n col ∈ 𝕄 ] ⟹ (m + n) + 0 = m + (n + 0)&#96; -| +𝕄 , Ax+&amp;l p;</div>
txt 　（articles2/01.book の公理 Ax+ と、同じ本の段。Ax+&amp;l は <code>[ m ; n col ∈ 𝕄 ] ⟹ m + n ∈ 𝕄</code> です。）
txt 仕組み：compile が prf の頭に段 <code>Ax+&amp;l &lt;- &#96;[ m ; n col ∈ 𝕄 ] ⟹ m + n ∈ 𝕄&#96; -| Ax+ v;</code> を足します（投げ先は Vampire。クラスの語・変数 <code>∈_</code>・<code>X_</code> などを含む Prop では <code>--| Ax+ v;</code>）。切り出した式が本当に Ax+ から出るかは、この段を証明器がいつも通り確かめます。決まりは次の4つです。
txt 　・<b>◀ の右には元の名前を書く</b>（<code>◀ W. , ax_s , Ax+</code>）のが基本です。主張に <code>Ax+&amp;l</code> と書くと、その前提は片側の式として公開され、後の Thm で使うときはその式を支える必要があります。最後の <code>h;</code> の段の sos も主張と同じにします。
txt 　・P は本で式を書いた Prop（<code>prop 名 &lt;- &#96;式&#96;</code>・<code>prop/thm 名 &lt;- &#96;式&#96;</code>）で、import した本の Prop でも使えます。DB の Prop（式が本に無いもの）には使えません。
txt 　・切るのは、括弧の外の and がちょうど1つのときだけです（結論全体を囲む <code>( … )</code> は外して見ます）。or・⟺ がある式や、and が2つ以上ある式は切らず、<code>FAIL: unintroduced sos name: P&amp;l</code> で落ちます。<code>P&amp;r&amp;l</code> のような重ね書きはできません。
txt 　・prf の中で同じ名前 <code>P&amp;l &lt;- …</code> を自分で定義したときは、その定義が使われます（compile は段を足しません）。
subsection 同じ前提の列に名前を付ける：props
txt ◀ の右や sos に同じ Prop の並びを何度も書くときは、<code>props 名 &lt;- P1 , P2 , …</code> で列に名前を付けられます。sos の項にその名前を書くと、compile が中身の並びに置き換えます（査読するのは置き換えた後・◀ の右の表示は書いた名前のまま）。
txt <div style="font-family:monospace;background:#f4f4f4;border:1px solid #ddd;padding:6px 10px;overflow-x:auto;white-space:nowrap">props 加法 &lt;- Ax1 , Ax+<br>let/thm 0=∅ &lt;- &#96;0 = ∅&#96; ◀ W. , ax_s , 加法</div>
txt 　置き換えるのは sos の項そのものだけです（slash の <code>/ 名</code>・段の名前・代入 <code>名[…]</code> は置き換えません）。列はその本の中だけで使え、import した本には運びません。前に定義した列の名前を中に書くと、その中身に展開されます。prf の中で同じ名前のラベルを定義した prf では展開しません。
txt 　列の名前には <code>. , ! ' &#96; [ ] / | : &amp;</code> と <code>O</code> を使えません。紹介した Prop・import した Prop・let と同じ名前も compile が拒否します（後から同じ名前を置くのも拒否）。本で紹介していない DB の Prop（<code>ax_s</code> など）と同じ名前は compile では見分けられず、列の方が優先されるので、そういう名前は付けないでください。
subsection 等号を開かない：W.!=.
txt common/word_basis.book は =. を <code>X = Y ⟺ X =_ Y</code>（外延の形）と定義しています。そのため <code>/ W.</code> は等号もすべて <code>∀ w (w ∈ X ⟺ w ∈ Y)</code> の形に開きます。Book 内定数の定義 <code>|g =_ |g_</code> のように、証明で等号として置き換えに使いたい式まで開くと、証明器は置き換えに使えなくなります。
txt 等号を残したいときは、=. を除いた <code>W.!=.</code>（所属の形で開くなら <code>W.'!=.</code>）を使います（4.book の <code>W.!名.</code>＝名の定義だけ開かない）。例：articles2/00.book の Lgi <code>-| hyg ///// W.'!=. , …</code>。
subsection goal と sos で形を揃える
txt slash で開くと、同じものが goal と sos で違う形になることがあります（goal は <code>A ∈ ℘ X</code> のまま、sos は <code>A ⊂ X</code> まで開いた、など）。2つを結ぶ定義が sos に無いと、証明器は証明できません。slash_cli で両方の開いた形を見て、残った方の定義（<code>℘.'</code>・<code>⊂.</code> など）を sos に足すか、両方を同じ深さまで開きます。
txt goal に付けた slash は goal だけを開きます。sos の補題・仮定に同じ語があるなら、その項にも slash を付けます（<code>-| 名 // W.</code>）。一階の段（-|）の sos には定義（<code>⊂.</code>・<code>→.</code> など）を置かず、slash で開きます。sos に定義を置くのは、slash の書けない多ソートの段だけです。例：articles1/25.book の LZ（goal も仮定 hyG も2層開く）。
txt <div style="font-family:monospace;background:#f4f4f4;border:1px solid #ddd;padding:6px 10px;overflow-x:auto;white-space:nowrap">LZ &lt;- &#96;|g *^ap (|Y) ⊂ |X&#96; // W. -| hyG // W.&#39; , pr:0 p;</div>
txt 　開く深さは全部の項で揃えます。同じ補題を sos に2回引かないと示せないなら、「閉じたまま使う所」と「元ごとに開いて使う所」が混ざっているサインです。
subsection 演算の強さは word ごと
txt 演算の結合の強さは word ごとに DB で決まっています。数の演算は普通の数学と同じで、後置の suc が最も強く、↑（累乗・右結合）、⋅、+ の順です。例：<code>2 ⋅ n ↑ 2</code> は <code>2 ⋅ (n ↑ 2)</code>、<code>m ⋅ n + j</code> は <code>(m ⋅ n) + j</code>。ほかの語との組み合わせで迷ったら括弧を書くか、<code>slash_cli.php</code> の前置記法（<code>[⋅ 2 [↑ n 2]]</code>）で確かめます。
subsection 名前の付け方
txt <b>Prop の名前</b>（prop・let/thm・props）には、区切りの文字（空白・backtick・( ) [ ] { }・, ;）と、それだけで式になる綴りを使えません。それだけで式になる綴りは、<code>|</code> で始まる記号（<code>|a</code>・<code>|q</code>・<code>|P^</code>）、<code>^</code> の付いた名前（<code>P^</code>）、<code>⊤</code>・<code>∅</code>・<code>0</code> などの記号です。<code>Q1</code>・<code>K</code>・<code>L10</code> のような名前にします。
txt <b>prf のラベル</b>は2種類です（段の書き方は 3.book「prf の1段」）。
txt 　・ <code>名 &lt;- &#96;式&#96;</code> は<b>主張（式）の名前</b>で、段の goal・sos に書けます。
txt 　・ <code>名 := &#96;項&#96;</code> は<b>式の中の記号を置き換える名前</b>で、段の左に単独で書き（<code>x := &#96;|?f ( |a )&#96; ;</code>）、backtick の式の中で使います。名前だけを段の goal・sos に書くと「Form の名前 H は段の goal・sos には書けません」で落ちます。<code>AA := ZZZ</code> はラベル ZZZ の別名です。
txt 後の段では名前を中身に置き換えて読むので、意味が変わる付け方は査読が落とします。ラベルの名前の規則は <code>&lt;-</code> でも <code>:=</code> でも同じです。
txt 　1. <b>使う前に定義する</b>：前の段（backtick の式の中も）に出た名前を、後からラベルにはできません（「前の段に出てきた名前「a」に後からラベルを付けています」）。定義を前へ移します。別名の鎖（<code>ZZZ &lt;- … ; AA := ZZZ ; B := AA</code>）も先の名前から順に書きます。
txt 　2. <b>この thm の行に出る名前にしない</b>（主張と、◀ の右の式の中。∀ で束縛した変数も。前に示した別の Thm の名前は 4）：「thm の行の主張に出てくる名前「x」に…」か「ラベル &#96;u&#96; と同じ名前が、後の段の式の中に出ています」で落ちます。
txt 　3. <b>本で紹介した prop の名前にしない</b>：「prf の中で、本が紹介した prop と同じ名前「A」にラベルを付けています」で落ちます。
txt 　　2・3 の直し方：ラベルの名前を替え、ラベルを使う段も替えます。式の中の変数（<code>|?g ( y )</code> の y）・prop の名前・最後の段は替えません。例 <code>thm … ◀ K</code> の prf の <code>K &lt;- …; K -| K p; goal -| K h;</code> は <code>K1 &lt;- …; K1 -| K p; goal -| K h;</code> にします（段の左のラベルだけ K1。sos の K と最後の段の K は本の prop K）。
txt 　4. <b>前に示した別の Thm に出る名前</b>（この thm の行の名前は 2）：
txt 　　・ その Thm の sos に出る → この prf では使えません（h; の FAIL に「前に示した Thm「…」（ラベル a）は…使えません」と添えられます）。ラベルを前の Thm に出ない名前（Le1 など）に替えます。
txt 　　・ その Thm の主張にだけ出る変数 → ラベルの名前をその変数にそろえると、中身を入れた式として使えます。例：前の Thm <code>&#96;x = x&#96; ◀ O</code> は、<code>x := &#96;|?f ( |a )&#96;</code> の prf で <code>|?f ( |a ) = |?f ( |a )</code> として使えます。
txt 　　　別の名前（<code>w := …</code>）にすると当たらず、h; が「この段の goal を示した段も、使える前の Thm も見つかりませんでした」か「項にこの prf のラベル（w）が入っています」で落ちます。
txt 　　　中身は同じ種類の項（集合の変数なら集合の項）にします。中身の記号が前の Thm の主張にも出る（<code>∃ y</code> の y に捕まる）ときは使えません。
txt 　5. <b>1語としてだけ当たる</b>：ラベル <code>a</code> は <code>|a</code>・<code>|?a</code> の中を、ラベル <code>P</code> は <code>P^</code> の中を置き換えません。<code>|a</code> を置き換えたいなら <code>|a := &#96;|b&#96;</code> と書きます。
txt <b>照合は中身、最後の段は綴り</b>：h; は中身で照合するので、段の sos では同じ式に付けた名前どうし・名前と式は同じ項です（3.book「書き換えだけの違い」）。ただし<b>最後の段は thm の行と同じ綴り（goal も sos も）</b>で書きます（違うと「prf の最後の段が thm の主張と違います」）。thm の行の ◀ の右には prop の名前か式を書きます（prf のラベルを書くと、主張が prf を読まないと分からなくなります）。
subsection 固定化：定数で示して h[fix]; で戻す
txt 写像 f や集合 X について示す長い証明は、f・X を定数 |f・|X にして書き、最後の段で変数に戻します。証明器に渡る問題で変数が定数になるので探索が軽くなります。作るもの（単射・対角クラスなど）は <code>名_ := &#96;式&#96; ;</code> で式に名前を付け、仮定 <code>hyG &lt;- &#96;|g =_ |g_&#96; ;</code> で集合の定数 |g と結びます。
txt 戻すのは <code>h[fix];</code> の段です。結論の段 <code>goal -| W. , ax_s h[fix];</code> か、途中の段 <code>L &lt;- &#96;変数の式&#96; -| W. , ax_s h[fix];</code>（後の段で L を引ける）。h; のままでは戻りません。例：articles1/63.book の <code>X ≤# ℘ X</code>（定数 |g は ∃除去で消える）。
txt <div style="font-family:monospace;background:#f4f4f4;border:1px solid #ddd;padding:6px 10px;overflow-x:auto;white-space:nowrap">prf |g_ := &#96;\{ \&lt; pr x ; \{ set x \} \&gt; Cls x | x ∈ |X \}&#96; ;<br>&nbsp;&nbsp;&nbsp;&nbsp;hyG &lt;- &#96;|g =_ |g_&#96; ;<br>&nbsp;&nbsp;&nbsp;&nbsp;Leg &lt;- &#96;|g_ ⊂_ |X ^^pr ℘ |X&#96; // W.&#39;!=. -| set1. p;<br>&nbsp;&nbsp;&nbsp;&nbsp;LeI &lt;- &#96;|g ∈ |X →I ℘ |X&#96; /// W.&#39;!=. -| hyG /// W.&#39;!=. , pr:0 , set1. p;<br>&nbsp;&nbsp;&nbsp;&nbsp;&#96;|X ≤# ℘ |X&#96; / ≤#.&#39; -| LeI p;<br>&nbsp;&nbsp;&nbsp;&nbsp;goal -| W. , ax_s h[fix];</div>
txt 　主張の前件（f ∈ X → Y など）は、どれかの段の sos に仮定として1回は現れる必要があります。h[fix]; は、段の sos に仮定として出た式（の |f・|X を f・X に戻したもの）を集めて、主張の「前件 ⟹ 結論」を組み立てるからです。集めた仮定が前件を過不足なく覆わないと、組み立てた式が主張と一致せず落ちます。数学的には要らない仮定でも、1回は sos に引きます。途中で変数に戻して別の仮定で始め直すより、定数のまま最後まで進めて1回だけ戻す方が短くなります。小さな段の集まりや、もともと速い段は、固定化しても速くなりません（Hyperion の分だけ遅くなることもある）。
subsection 同じ塊を何度も書くなら語にする
txt 「増加列」「部分列」のような条件を毎回展開して書くと、式が長くなり証明器が遅くなります。本で word を紹介し、prop で定義して、式の中では1つの記号として書きます（引数が多いものは対 <code>\&lt; pr x ; P \&gt;</code> に包んで中置2項の語に）。証明器には原子式の照合になります。例：articles3/31.book（Ramsey）の <code>x ⇈ P</code>・<code>\&lt; pr x ; P \&gt; ⊑ \&lt; pr v ; L \&gt;</code>。展開して書いていた版では1つの段が Vampire で約30秒、語にして約1.2秒になりました（2026-10-08 の実測）。
txt 　語を開くときは <code>/ W.</code> ではなく名指し（<code>/ ⇈. / ⊑.</code>）にします。W. は =. も開くので、等号が外延性の式に化けて timeout しました。

section 本を分ける：import と private theorem
txt 何冊かで同じ準備を使うときは、準備を別の本にして import します。例：articles2/02.book（数える道具）を 58a・58b・88a が import し、どれも主定理の周りだけの小さな本になりました。import した本は証明し直さず、保存された査読結果を使います。
subsection import で運ぶもの・運ばないもの
txt 運ぶ：紹介（word・prop・abbr・lower）と、証明済みの Thm（<code><span style="color:#127a3d;font-weight:bold">thm</span></code> <code><span style="color:#127a3d;font-weight:bold">prop/thm</span></code> <code><span style="color:#127a3d;font-weight:bold">let/thm</span></code>、<code><span style="color:#127a3d;font-weight:bold">!</span></code> 付きも）。goal は名前でも <code>&#96;式&#96;</code> でもかまいません。<code>&#96;式&#96;</code> の Thm は、使う側の sos に <code>&#96;式&#96;</code> と書いて引きます（articles2/52b.book の <code>&#96;0 ∈ 𝕄&#96;</code>・<code>&#96;1 ∈ 𝕄&#96;</code> は 01.book の Thm）。let/thm の名前も引けます。import した本がさらに import した本の Thm も届きます。
txt 運ばない：<code><span style="color:#127a3d;font-weight:bold">thm-</span></code> 系（private theorem）の Thm と名前、sos に <code>&#96;式&#96;</code> を含む Thm（その本だけの定数に頼るかもしれない）、ヘッダの formel・thmel。
txt sos に let で置いた名前を含む Thm は、後の Thm からも使えません（同じ名前を後で置き直せるため）。
subsection private theorem
txt <code><span style="color:#127a3d;font-weight:bold">thm-</span></code> <code><span style="color:#127a3d;font-weight:bold">prop/thm-</span></code> <code><span style="color:#127a3d;font-weight:bold">let/thm-</span></code>（<code><span style="color:#127a3d;font-weight:bold">!</span></code> 付きも）は、その本の中（後の Thm・後の頁）では使えて、import した本には運ばない Thm です。Lean の <code>private theorem</code> と同じ考え方です。<code><span style="color:#127a3d;font-weight:bold">!</span></code> は表示するか、<code><span style="color:#127a3d;font-weight:bold">-</span></code> は運ぶか、で別のことなので、<code><span style="color:#127a3d;font-weight:bold">!thm-</span></code> と組み合わせられます。
txt 使いどころ：準備の本の中だけで使う作業用の補題です。運ばなければ、import した本は同じ名前（L01・LD など）を自由に使えます。逆に、使う側の本で使いたい Thm には <code><span style="color:#127a3d;font-weight:bold">-</span></code> を付けません。
txt 例（説明のための形・実際の 0.book では L01 は ∪=#+ の prf の中のラベル）：
txt <div style="font-family:monospace;background:#f4f4f4;border:1px solid #ddd;padding:6px 10px;overflow-x:auto;white-space:nowrap">!let/thm- L01 &lt;- &#96;0 {/}= 1&#96; ◀ W.<br>prf L01 // W. -| O p; L01 -| W. h;<br>let/thm ∪=#+ &lt;- &#96;X ∩ Y = ∅ and [ m ; k col ∈ 𝕄 ] and X =# m and Y =# k ⟹ X ∪ Y =# m + k&#96; ◀ W. , ax_s , +𝕄<br>prf … , L01 , … v; …</div>
txt 　この本の中では ∪=#+ の prf が L01 を引けます。この本を import した本からは ∪=#+ は使えますが、L01 を sos に書くと <code>FAIL: unintroduced sos name: L01</code> で落ちます。

0_tutorial_AI/practice.book

`0_tutorial_AI/practice.book`