2 進め方

難しい定理になると、一回で良いprfを書くことはまずできません。試して、失敗の仕方を読んで、次の一手を決める、の繰り返しになります。このBookはその進め方を、実際に試した記録で見せます。定義や記号は 6.book のものを使います（ヘッダで import 6）。
1回の試みは次の順で進めます。
　① あらすじ：紙で証明するなら、どの定義を開き、どこで場合分けし、どんな補題が要るかを先に書く。
　② 予測：試す前に「これで通るはず」「落ちるならこう落ちる」を決める。
　③ 試す：1回に変えるのは1か所だけ（slashの本数・前提・投げ先のどれか1つ）。
　④ 症状を読む：FAILの文言で、どの種類の失敗かを見分ける（「失敗の種類を見分ける」の節）。
　⑤ 通ったら：前提を1つずつ外して最小にし、前提が強すぎないかを点検する（「通ったあとで」の節）。思ったより速く通ったときほど疑います。
同じ方向の失敗が2〜3回続いたら、同じ所をいじり続けずに、あらすじ（補題の切り方）から考え直します。

2.1 速く試す：prf_trial

1か所ずつ変えて何度も試すときは、本を書き換えずに .claude/prf_trial.php <本> <Thm の行番号か行の一部> <候補> … で、1つの Thm に prf の候補をまとめて当てます（= だけの候補は今の prf）。前の Thm は1回だけ流し、証明器の結果をディスクに覚えるので、候補ごとに走るのは変えた段だけです。
　・ 結果の JSON は良い順に並べ替えて出ます。どの候補が通ったかは、候補の文字列と照らして確かめます（取り違えて誤った prf を書いたことがあります）。
　・ --quick は最後の h; のつなぎを省いた速い試しです。ok は「証明器の段が通った」だけなので、決めた prf は最後に本に書いて review_cli.php で査読します。
　・ 秒を比べるときは、MATHEL_PROVER_CACHE_DIR を候補ごとに新しい場所にして（同じ場所だと後の候補が覚えた結果で得をする）、複数回測ります。1本目は暖機で遅く出ます。測り終えたキャッシュは消します。

3 実測で見る使い分け

以下の時間はこのサーバーでの実測です。「一階の式」「クラス変数」の小節は 2026-10-16 にこの本と同じ default.thmel で測り直し（キャッシュ無し・2回）、「内包記法」「述語変数」の小節は 6.book の段の実測（2026-09-28）です。時間は負荷で揺れます。待ち時間は default.thmel で Prover9・Vampire とも20秒です（zf.thmel は Prover9 10秒・Vampire 90秒）。

3.1 一階の式：まず -| … p;

word(ss,s) … \(+\)
+結合則 … \(x + ( y + z ) = ( x + y ) + z\)
\(x + ( y + ( z + ( w + u ) ) ) = ( ( ( x + y ) + z ) + w ) + u\) \(\blacktriangleleft\) +結合則
同じThmを、関係と投げ先の組み合わせだけ替えて比べました（4項は \(x + ( y + ( z + w ) ) = ( ( x + y ) + z ) + w\) ）。
　4項 … -| p; 0.009秒　◀ v; 0.011秒　◀ p; 0.38秒　-| s; 0.63秒
　5項 … -| p; 0.007秒　◀ v; 0.012秒　-| s; 0.63秒　◀ p; timeout（20秒）
c-Form を含まない一階の式なら、-| … p; が速く確実です。◀ … p; は{s,c}ソートの相対化で式が大きくなり、項が増えると急に遅くなります。satallax+ は高階の探索をするので、一階の式には割高です。

3.2 クラス変数：◀ に替える

\(\forall x ( x \in X \Longrightarrow x \in Y ) , y \in X \Longrightarrow y \in Y\) \(\blacktriangleleft\) O
クラス変数（| の付かない X_）を含むThmは、-| では翻訳できず「|0 翻訳不可: cvt+ 後に ∈_ が残っています」という査読エラーになります。◀ … v; なら{s,c}ソートのまま投げられます。
　◀ v; 0.010秒　◀ p; 0.008秒　◀ s; 0.010秒　-| p; 翻訳不可
この小さい例では ◀ p; が最速ですが、差はわずかです。上の理由で、c-Form を含む段は ◀ … v; を勧めます。
クラス定数（|A_ など）だけなら、-| は |cvt+ で翻訳できます（3.book の Hall の例は ◀ v; で示しています）。

3.3 内包記法と分出公理：v;

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

3.4 述語変数の代入：実例を sos に・satallax+ に探させる

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