4 2ソートのThm

s-Form（集合）を「もの」、c-Form（クラス）を「箱」と見なし、「入っている」を表す word ∈_ を使います。表示では ∈_ は ∈ と、X_ は X と同じ形になるので、ソースで区別します。最初の例はクラス変数 X_ を含むので、表のとおり ◀ … v; で投げます（次の Hall の例もクラス定数 |A_ を含むので ◀ … v; で投げます）。
word(sc,p) … \(\in\)
1つの箱 \(X\) は、ものを「\(X\) に入っている／いない」の2通りに分けます。入っているかどうか（真か偽か）だけでは、3つのもの x1, x2, x3 を互いに区別できません（2通りに3つを入れる鳩の巣原理）。
ソースの読み方：\\{ And A \\ B \\ C \\} は A and B and C を縦に並べて書く形、{/}⇔ は ⇔ の否定（「真偽が違う」）。
\(\neg \begin{cases} x_{1} \in X \not\Leftrightarrow x_{2} \in X \\ x_{2} \in X \not\Leftrightarrow x_{3} \in X \\ x_{3} \in X \not\Leftrightarrow x_{1} \in X \end{cases}\) \(\blacktriangleleft\) O

次は Hall の定理（各箱から異なるものを選べる条件）の小さな具体例です。3つの箱に何が入っているかを具体的に与え（prop Hall）、そこから「各箱から異なるものを1つずつ選べる」ことを示します。|p などは定数です（変数だと「すべての」の意味になる）。
ソースの読み方：[ |p ; |q col ∈_ |A_ ] は |p ∈_ |A_ and |q ∈_ |A_（col は 2.book）、[ ∃ x ∈_ |A_ . P ] は ∃ x (x ∈_ |A_ and P)、{/}= は ≠。
Hall … \(\begin{cases} \mathrm{p} , \mathrm{q} \in \mathrm{A} \\ \mathrm{q} , \mathrm{r} \in \mathrm{B} \\ \mathrm{r} , \mathrm{p} \in \mathrm{C} \end{cases}\)
neq … \(\mathrm{p} \neq \mathrm{q} , \mathrm{q} \neq \mathrm{r} , \mathrm{r} \neq \mathrm{p}\)
\(\exists x \in \mathrm{A} . \exists y \in \mathrm{B} . \exists z \in \mathrm{C} . ( x \neq y , y \neq z , z \neq x )\) \(\blacktriangleleft\) Hall ，neq
Vampire は一瞬で割り当て（\(\mathrm{A}\)→\(\mathrm{p}\), \(\mathrm{B}\)→\(\mathrm{q}\), \(\mathrm{C}\)→\(\mathrm{r}\) など）を見つけます。

5 補題と hyperion

次の Thm は -| … p; や ◀ … v; なら1段・探索時間1ms未満で通ります（実際に書くならそれで十分）。ここでは補題と h; を見せるため、あえて遅い ◀ … p; を使います。◀ … p; の1段では100秒待っても探索が終わりません（default.thmel の Prover9 の制限時間は20秒なので 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 にします）。ラベルには、その位置までに紹介した prop の名前は使えません（「introduced Prop label redefined in proof: 名」で FAIL）。

5.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 します。

示していない prop が前提に残ると「conclusion: no derivation found; composition missing 名」で FAIL します（失敗の見分け方は practice.book）。

5.2 h; がすること

h; の段は式の証明探索をせず（例外は下の「h; の段の関係」の確かめ直し）、積まれた Thm（OK になった段の Thm と、この位置までに示した Thm）だけから、次の規則のどれかで段（goal ◀ sos）を導けるかを確かめます。どの規則で通ったかは OK の印の詳細に出ます（例 composition・∀ -introduction checked）。h の段の 〇 を押すと、小窓の先頭に導出の記録（段の Thm を、どの Thm からどの規則〈合成・∀導入・∃除去 など〉で作ったか）が出ます。
　・ 合成：G ◀ Δ が積まれていて、Δ の各項が段の sos に入っているか、積まれた別の Thm によって段の sos から導けるなら、G ◀（段の sos）。上の例はこれです。
　　そのため thm の主張の sos には、prf の段で使った補題の Thm の sos も含めます（例 articles3/0.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 も）の実例（7.book）は、示さずに使えます。
　・ 書き換えだけの違い：ラベルを中身に置き換えた・同じ式を綴りだけ変えて書いた、という違いは同じ Thm とみなします。
　・ 存在導入（多ソートの段だけ）：F ◀ Γ から ∃_ X_ φ ◀ Γ（F は φ の X_ にクラスを入れたもの）。

5.3 h; の段の関係

積まれた Thm には関係が付いています。-| の段（p; v; s;）は「-| の Thm」、◀ と --| の段は「多ソートの Thm」（{s,c}ソートのまま確かめたもの）です。h; の段も、-| … h; は -| の Thm を、◀ … h;・--| … h; は多ソートの Thm を作ります。
　・ 同じ関係の Thm はそのまま使えます。基本は、つなぐ段と同じ関係で h; を書きます。ただし thm を結ぶ最後の段は thm に合わせます（thm が --| なら最後も --| … h;。-| … h; では thm と違うとして落ちます・6.book の ¬Exi𝕍）。
　・ -| の 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「--| の仕組み：fn-elim と cls-elim」の規定にある -| と --| の同値と同じ問題）。〇 がこの規則に頼っているとき（その段が直接使ったときも、使った前の定理が頼っていたときも）、結果の欄に「※ 健全性未証明の規則 multisort→tfl（証明書なしの持ち上げ）に依存」と出ます。
クラス変数の Thm（帰納法など、多ソートの段 --| … v; で示すもの）を結ぶときの選び方：

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

5.4 途中の段が落ちたとき

段のどれかが落ちると、FAIL の行にはthm の ファイル:行、落ちた段の行と綴り、理由（原因と直し方・証明器の元の文は「内部：」の後）が出ます。例えば上の Le2 を Le2 <- `…` ◀ O v;（前提なし）にすると #5-1 3.book:行 FAIL: N行目の段 `Le2 <- … ◀ O v;` で落ちました：Vampire が反例のモデルを見つけました＝この sos からは導けません。…（内部：多ソート step: ax_s0 Vampire not_proved (CounterSatisfiable)） のようになります。その段が証明器に投げた入力は CLI の --inputs（1.book）で読めます。

5.5 示した 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 の中だけで thm の goal の式を指す呼び名です（ここでも goal はこの thm の式）。後で前提として使う式には prop/thm で prop 名を付けます。

5.6 固定化：定数で示して変数に戻す（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「集合に名前を付けて、最後に消す」）。

5.7 途中の段で変数に戻す

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）。