2 進め方
難しい定理になると、一回で良いprfを書くことはまずできません。試して、失敗の仕方を読んで、次の一手を決める、の繰り返しになります。このBookはその進め方を、実際に試した記録で見せます。定義や記号は 6.book のものを使います（ヘッダで
import 6）。
1回の試みは次の順で進めます。
① あらすじ：紙で証明するなら、どの定義を開き、どこで場合分けし、どんな補題が要るかを先に書く。
② 予測：試す前に「これで通るはず」「落ちるならこう落ちる」を決める。
③ 試す：1回に変えるのは1か所だけ（slashの本数・前提・投げ先のどれか1つ）。
④ 症状を読む：FAILの文言で、どの種類の失敗かを見分ける（第6章）。
⑤ 通ったら：前提を1つずつ外して最小にし、前提が強すぎないかを点検する（第7章）。思ったより速く通ったときほど疑います。
同じ方向の失敗が2〜3回続いたら、同じ所をいじり続けずに、あらすじ（補題の切り方）から考え直します。
3 実測で見る使い分け
以下の時間はこのサーバーでの実測（2026-09-28）です。3.1・3.2 は min.thmel の本で、3.3・3.4 は 6.book（zf.thmel）で測りました。時間は負荷で揺れ、.thmel によって待ち時間（Vampire は min 20秒・zf 90秒）も違うので、目安として読んでください。この Book の thm と prf は zf で査読しています。
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.011秒 ◀ v; 0.13秒 ◀ p; 0.62秒 -| s; 0.70秒
5項 … -| p; 0.011秒 ◀ v; 0.016秒 -| s; 0.64秒 ◀ p; timeout（10秒）
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.025秒 ◀ p; 0.018秒 ◀ s; 0.030秒 -| p; 翻訳不可
この小さい例では ◀ p; が最速ですが、差はわずかです。上の理由で、c-Form を含む段は ◀ … v; を勧めます。
クラス定数（|A_ など）だけなら、default.thmel の -| は
|cvt+ で翻訳できます（min.thmel の -| は
|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 でも代入しません（HOL.book）。