1 例から

1.1 最初のThm

この Book は Thmel（定理とその証明の書き方）の説明です。ヘッダの thmel /common/min で min.thmel を読み込んでいます。
まず、いちばん小さい定理を書きます。ソースは次の2行です。
　thm `⊤` ◀ O
　prf `⊤` -| O p;
\(\top\) \(\blacktriangleleft\) O
1行目（thm）が主張です。「O（前提なし）から ⊤ が推論できる」と読みます。◀ の左を goal、右（前提の列）を sos と言います。O は空の列です。
2行目（prf）が証明の指示で、表示はされません（ソースで読みます）。「(⊤ ◀ O) を -| の変換にかけて p（prover+。内部で Prover9 を使う）に投げる」と読みます。末尾の1文字が投げ先（backend）です。
thm は ◀、prf の段は -| ですが、それで構いません。段 goal -| sos が OK なら、thm goal ◀ sos は示されたことになります（min.thmel が -| を「◀ の Thm を変換して確かめる」ものと規定しているため・「仕組み」の節）。1.book の例のように ◀ のまま ◀ … p; と書いても OK で、違うのは投げ方と速さです（次の節）。
右の「査読（この頁）」ボタンを押すと、Thm査読の表に「OK」と出ます。#列の 1.1-1 は 1.1節の1番目の Thm です。OK をクリックすると 〇 の印が出て、Prover9 が length:2 の証明を見つけたことが分かります（〇＝backend が確かめた印）。投げた入力はコレです（\(\top\) は $T）。

1.2 前提のあるThm

word(ss,s) … \(+\)
+結合則 … \(x + ( y + z ) = ( x + y ) + z\)
\(x + ( y + ( z + w ) ) = ( ( x + y ) + z ) + w\) \(\blacktriangleleft\) +結合則
ソース：
　word + … 記号 + を紹介する（gram (ss,s)。+ の意味は決めていない＝前提が唯一の手がかり）
　prop +結合則 <- `x + (y + z) = (x + y) + z` … 式に名前を付ける（prop）。x, y, z は自由変数で、「すべての x, y, z について」の意味
　thm `x + (y + (z + w)) = ((x + y) + z) + w` ◀ +結合則 … 主張を式で書いた thm。その prf の中では goal がこの式を指す
　prf goal -| +結合則 p; … 前の例と同じ指示を、名前で書いたもの
投げた入力はコレで、length:5 の証明が見つかります。Prover9 への入力に + の gram は書かれません。

2 書き方の一覧

2.1 prf の1段

prf の1段は goal 関係 sos 投げ先; です（例 goal -| +結合則 p;）。sos が複数なら ,（前後に半角スペース）で区切ります。関係と投げ先の組み合わせ（min.thmel）：

書き方	投げる前にすること	c-Form を含むThm
goal -| sos p;　goal -| sos v;　goal -| sos s;	Thm 全体を |0 で「高階言語」へ変換（「仕組み」の節）	FAIL（min.thmel は |cvt+ を掛けないので、クラスの語を含むと |0 がエラー）。クラスは ◀ … v; で扱う。default.thmel の -| は |cvt+|0（5.book）
goal ◀ sos p;	-| の変換はしない。prover+ がソートを一項述語にして相対化し、一階言語へ	扱える
goal ◀ sos v;	-| の変換はしない。vampire+ がソートを型として保った TFF にする	扱える
goal ◀ sos h;	証明器に投げない。前の段で示した Thm を組み合わせて主張を導く	—

goal ◀ sos s; も書けます（この Book では扱いません）。

段の書き方ごとに、Thm がどの変換を通ってどの証明器に届くかを図にすると次のとおりです（"→" は変換）。

default.thmel・zf.thmel では --|（{s,c}ソートのまま翻訳）も書けます。min.thmel には無く、書くと査読エラーです。

2.2 同じThmを別の投げ先へ

同じ Thm に、投げ方だけ違う prf を付けます。どれも OK です。
\(x + ( y + ( z + w ) ) = ( ( x + y ) + z ) + w\) \(\blacktriangleleft\) +結合則
　prf goal ◀ +結合則 v; … -| の変換をせず（◀ のまま）v（vampire+。内部で Vampire を使う）へ。ソート s を型として保ったTFF形式で投げます（plus: (mathel_s * mathel_s) > mathel_s が + の型）。
\(x + ( y + ( z + w ) ) = ( ( x + y ) + z ) + w\) \(\blacktriangleleft\) +結合則
　prf goal -| +結合則 s; … -| の変換をして s（satallax+。内部で Satallax を使う）へ。THF形式で投げます（関数はカリー化 plus @ X @ Y）。
\(x + ( y + ( z + w ) ) = ( ( x + y ) + z ) + w\) \(\blacktriangleleft\) +結合則
　prf goal ◀ +結合則 p; … -| の変換をせず p へ。prover+ が自分でソートを一項述語にして（相対化・6節）コレを投げます。約400ms・length:18 で、-| p; より遅くなります。

2.3 backend

　p … prover+：Prover9 を使う。一階論理 \(\mathbb{L}_1\) を判定。◀ で受けたときは一階翻訳をして \(\mathbb{L}_\mathrm{1sc}\) も判定（6節）
　v … vampire+：Vampire を使う。一階{s,c}ソート論理 \(\mathbb{L}_\mathrm{1sc}\) を判定
　s … satallax+：Satallax を使う。高階{s,c}ソート論理 \(\mathbb{L}_\mathrm{Hsc}\) を判定
　h … hyperion：証明器ではなくメタ推論のソフト。式の証明探索はせず、示した Thm を組み合わせるだけなので、証明器を待つ時間がかからない（例外は、関係をまたいで Thm を確かめ直すときに Vampire を呼ぶこと。W. を含む Thm の確かめ直しは何分もかかることがある・下の「h; の段の関係」）
1節と 2.2 の例（◀ … p; を除く）の時間は、Prover9・Vampire は約10ms（ほぼプロセス起動の分）、Satallax は \(\top\) で10ms・結合則で600ms程です。Satallax は常に高階の探索をするので、一階の内容には割に合わないコストがかかります。

3 補題と hyperion

次の Thm は -| … p; や ◀ … v; なら1段・探索時間1ms未満で通ります（実際に書くならそれで十分）。ここでは補題と h; を見せるため、あえて遅い ◀ … p; を使います。◀ … p; の1段では100秒待っても探索が終わりません（査読の制限時間は10秒なので timeout）が、補題に分けると通ります。
\(x + ( y + ( z + ( w + u ) ) ) = ( ( ( x + y ) + z ) + w ) + u\) \(\blacktriangleleft\) +結合則
ソース（prf は表示されないので全行）：
　prf Le1 <- `x + (y + (z + w)) = ((x + y) + z) + w` ◀ +結合則 p;
　 Le2 <- `x + (y + (z + (w + u))) = ((x + y) + z) + (w + u)` ◀ Le1 p;
　 Le3 <- `((x + y) + z) + (w + u) = (((x + y) + z) + w) + u` ◀ +結合則 p;
　 goal ◀ Le2 , Le3 p;
　 goal ◀ +結合則 h;
読み方：Le1 <- `…` ◀ +結合則 p; は「式に名前 Le1 を付け、Le1 ◀ +結合則 を p に投げる」。示した Le1 は次の段の sos に使えます。最後の goal ◀ +結合則 h; は、前の段（goal ◀ Le2 , Le3、Le2 ◀ Le1、Le1 ◀ +結合則、Le3 ◀ +結合則）をつなぐと thm の主張 goal ◀ +結合則 になることを hyperion が確かめる段です。4段目までに示したのは goal ◀ Le2 , Le3 で、thm（goal ◀ +結合則）とは sos が違うので、この段が要ります。
Prover9 の探索時間は Le1 / Le2 / Le3 / goal の段の順に約 400ms / 40ms / 15ms / 800ms、証明は length:18 / 14 / 17 / 14 です。Le1 を作らずに Le2 ◀ +結合則 p; だと 2200ms・length:20 になります。
Le1〜Le3 はこの prf の中だけのラベルで、後の thm からは引けません（後で使う式は下の prop/thm にします）。

3.1 h; が要るとき

prf の最後の段が thm と同じ goal・sos なら（関係は ◀ でも -| でもよく、sos の順序は問わない）、その段で thm が示されたことになり h; は要りません。上の例は最後の投げる段が goal ◀ Le2 , Le3 で sos が違うので h; が要ります。h; を書かないと査読は「prf の最後の段が thm の主張と違います（thm: `goal ◀ +結合則` / prf: `goal ◀ Le2 , Le3 p;`）＝最後に `goal ◀ +結合則 h;` を足すか、最後の段を主張の形にしてください」で FAIL します。

h; は式の証明探索をせず、prf の段と、この位置までに示した Thm を組み合わせるだけです。示していない prop が前提に残ると「conclusion: no derivation found; composition missing 名」で FAIL します（失敗の見分け方は 6b.book）。

3.2 示した Thm を後で使う

補題を別の thm として示しておき、後の thm で名前で使うこともできます。
結合4 … \(x + ( y + ( z + w ) ) = ( ( x + y ) + z ) + w\) \(\blacktriangleleft\) +結合則
\(x + ( y + ( z + ( w + u ) ) ) = ( ( ( x + y ) + z ) + w ) + u\) \(\blacktriangleleft\) +結合則
ソース：
　prop/thm 結合4 <- `x + (y + (z + w)) = ((x + y) + z) + w` ◀ +結合則 … 式に prop 名 結合4 を付け、同時に thm（結合4 ◀ +結合則）にする
　prf 結合4 -| +結合則 p;
　thm `x + (y + (z + (w + u))) = (((x + y) + z) + w) + u` ◀ +結合則
　prf goal -| 結合4 , +結合則 p; … 結合4 を前提に置いた段
　 goal ◀ +結合則 h; … 示した 結合4 ◀ +結合則 を使って、前提から 結合4 を外す
結合4 はほかの prop と同じく sos に名前で書けます。証明していない prop を同じように前提に置くと、最後の h; が「composition missing 名」で FAIL します（仮定として残るだけ）。h; は名前でなく式で照合するので、同じ式を別の名前で示してあればそれが使われます。
goal は、その thm の prf の中だけで主張の式を指す呼び名です（ここでも goal はこの thm の式）。後で前提として使う式には prop/thm で prop 名を付けます。

3.3 h; の段の関係

積まれた Thm には関係が付いています。-| の段（p; v; s;）は「-| の Thm」、◀ と --| の段は「多ソートの Thm」（{s,c}ソートのまま確かめたもの）です。h; の段も、-| … h; は -| の Thm を、◀ … h;・--| … h; は多ソートの Thm を作ります。
　〇 同じ関係の Thm はそのまま使えます。基本は、つなぐ段と同じ関係で h; を書きます。
　〇 -| の Thm を ◀ h;・--| h; で使うときは、hyperion がその Thm を多ソートでも確かめ直し（Vampire に投げる）、通ったものだけを使います（上の 結合4 の例）。確かめ直しは Vampire の探索なので、W. や import した定理をたくさん使う Thm では何分もかかることがあります（外部の AI の試験で、強い帰納法を --| … h; で結んで20分以上）。slash を含む段（/ W. など）は多ソートで確かめ直せないので、/ で展開した段をつなぐ h; は -| で書きます（4.book）。
　〇 多ソートの Thm を -| の段で使うこと（持ち上げ multisort→tfl）は、段の末尾を h[lift];（固定化と一緒なら h[fix,lift];）と書いたときだけ、確かめ直しなしで認めます（査読の記録に multisort→tfl admitted と残ります）。書かない h; では使わず、「段の末尾を h[lift]; と書きます」という理由で落ちます。この向きが健全かはまだ示していません（5.book「--| の仕組み：cls-elim」の規定にある -| と --| の同値と同じ問題）。〇 がこの規則に頼っているとき（その段が直接使ったときも、使った前の定理が頼っていたときも）、結果の欄に「※ 健全性未証明の規則 multisort→tfl（証明書なしの持ち上げ）に依存」と出ます。
クラス変数の Thm（帰納法など、多ソートの段 --| … v; で示すもの）を結ぶときの選び方：

どちらを使うかは書き手が段ごとに選びます。後で -| の段（/ W. を使う段など）から引く Thm は、-| … h[lift]; で結ぶと使いやすくなります（articles2/0-sn.book の INDC）。

3.4 h; がすること

h; の段は式の証明探索をせず（例外は上の「h; の段の関係」の確かめ直し）、積まれた Thm（OK になった段の Thm と、この位置までに示した Thm）だけから、次の規則のどれかで段の主張を作れるかを確かめます。どの規則で通ったかは OK の印の詳細に出ます（例 composition・∀ -introduction checked）。h の段の 〇 を押すと、小窓の先頭に導出の記録（段の Thm を、どの Thm からどの規則〈合成・∀導入・∃除去 など〉で作ったか）が出ます。
　〇 合成：G ◀ Δ が積まれていて、Δ の各項が段の sos に入っているか、積まれた別の Thm によって段の sos から導けるなら、G ◀（段の sos）。最初の例（Le1〜Le3）はこれです。
　　そのため thm の主張の sos には、prf の段で使った補題の Thm の sos も含めます（例 articles3/0-pa.book の Ltot などが ◀ W. , 𝕄0s , IND𝕄 , … と、使う補題の前提を並べるのはこのため）。
　〇 slash の除去：A / R ◀ Γ が積まれていれば A ◀ R , Γ（4.book「展開して投げ、h; で戻す」）。
　〇 ∀導入：bar 付きの定数で示した Thm の bar を外して変数の Thm にします。外す定数が段の goal・sos（W. の中の定義の本文も）に現れないときだけです。h[fix]; はこれに、仮定ラベルを前件へ戻す演繹を加えたもの（下の「固定化」）。
　〇 ∃除去（h[fix]; だけ）：集合の定数に名前を付ける仮定ラベル |Y =_ θ を、θ が集合になる根拠（前の段の Exi θ、または θ ⊂_ σ と主張の sos の分出公理）があれば消します（6.book）。
　〇 公理の実例：段の sos にある Prop の自由なクラス変数に式を入れた実例 〇[C_:=`θ`]（6.book）と、段の sos にある schema（∀ を書いた prop も）の実例（HOL.book）は、示さずに使えます。
　〇 書き換えだけの違い：ラベルを中身に置き換えた・同じ式を綴りだけ変えて書いた、という違いは同じ Thm とみなします。
　〇 存在導入（多ソートの段だけ）：F ◀ Γ から ∃_ X_ φ ◀ Γ（F は φ の X_ にクラスを入れたもの）。

3.5 固定化：定数で示して変数に戻す（h[fix];）

長い証明では、主張の変数を bar 付きの定数（|x など）に置き替えて示し、最後に変数へ戻すと速くなります（証明器にとって、変数より定数の方が探索が軽い）。前提には名前を付けて（仮定ラベル）、段の sos に引きます。
\(x = y \Longrightarrow x + ( z + w ) = ( y + z ) + w\) \(\blacktriangleleft\) +結合則
ソース：
　prf hy <- `|x = |y` ;
　 L <- `|x + (|z + |w) = (|y + |z) + |w` ◀ hy , +結合則 p;
　 goal ◀ +結合則 h[fix];
読み方：hy <- `|x = |y` ; は前提に名前を付けるだけで、示す段ではありません。L の段は hy を sos に置いて定数の式を示します。最後の h[fix]; では、hyperion が段をつなぎ（L ◀ hy , +結合則）、hy を前件へ戻し（|x = |y ⟹ …）、bar を外して変数の主張 goal ◀ +結合則 にします。h; のままでは戻さず「composition no local thm for goal」で FAIL します。

仮定ラベルが |Y =_ θ（内包で作った集合に名前を付ける）の形なら、前件へ戻さずに消すこともできます（∃除去・6.book「集合に名前を付けて、最後に消す」）。

3.6 途中の段で変数に戻す

h の段は prf の途中にも書けます。導けた式は名前の付いた Thm になり、後の段で使えます。thm の主張を結ぶのは最後の h の段です。
\(x = y , y = z \Longrightarrow x + w = z + w\) \(\blacktriangleleft\) O
ソース：
　prf hy <- `|x = |y` ;
　 L <- `|x + |w = |y + |w` ◀ hy p;
　 LG <- `x = y ⟹ x + w = y + w` ◀ O h[fix]; … 途中の段で変数の式に戻す
　 goal ◀ LG p; … LG を（x, y）と（y, z）の2通りに使う
　 goal ◀ O h;
実例：articles1/25.book（Cantor-Schröder-Bernstein）は、補題を固定化して書き直すと査読が約4秒から約0.9秒になりました。f・g・A などを固定したまま1つの prf で進め、途中の段 Lall2 を h[fix]; で変数の主張に戻し、それを使って thm の主張を示しています（A・f′ に付けた集合の名前 |A・|f′ は、この段で ∃除去により消えます＝6.book）。

3.7 途中の段が落ちたとき

段のどれかが落ちると、FAIL の行にはthm の ファイル:行 と、落ちた段の理由が出ます（落ちた段そのものの行番号は今は出ません）。例えば上の Le2 を Le2 <- `…` ◀ O v;（前提なし）にすると #3-1 3.book:行 FAIL: 多ソート step: ax_s0 Vampire not_proved (CounterSatisfiable) のようになります。その段が証明器に投げた入力は CLI の --inputs（1.book）で読めます。

〇 の印を押すと開く小窓（投げた入力）では、証明器に渡すために処理した問題と、証明器への入力の原文を照合できます。上から次の順に並びます。
　① # prover+ が受け取ったもの … 翻訳した後・分割する前の前提（assumptions）と goal。1.1 の例（-| … p;）では JSON で書いた前置記法（2.book）で、goal が "⊤"、前提はありません。多ソートの段（◀ や --| の段）では、ソート付きの木の JSON で出ます
　② # prover+ がProver9に投げた … goal を分割したときは「2つにsplitして」のように本数が付きます。prover+ は、分割したすべてが proved のときに元の段を認めます。strategy は前処理の方式の名前です
　③ 1本ごとに、# 1/2 prover+ が割った1本（分割する前と同じなら出ません）と、# 1/2 Prover9 に投げた の下に Prover9 への入力の原文
小窓に出ないものもあります：slash や翻訳の途中の書き換え、証明器が返した証明。ですから、小窓だけで書いた段から 〇 までを確かめられるわけではありません。例えば articles1/63.book の最後の主定理 X <# ℘ X の1段目では、/ <#. で goal が「≤# かつ ¬=#」に開いたものを prover+ が受け取り、2本に分割して Prover9 に投げたことまでが読めます。