book集

!txt default.thmel — 現行の Thmel
!txt
!txt 第1段では、既存 PHP の Thmel をそのまま使用する。
!txt 推論関係・Rite列・prover設定は、意味を決めたものから順にここへ移す。
!txt
!txt ★`backend` は文字と投げ先の**宣言**（prf の段 `G -| Γ p;` の `p` は Prover+）。
!txt ★`target` は**制限**＝この本が投げられる先はここに書いたものだけ。
!txt   既定は3つとも書いてある＝**読めば既定の動作が分かる**（隠れ規則にしない）。
!txt ★`=|` `e-|` `a-|` `ae-|` `d-|` は文字を持たないが hyperion を要求する
!txt   （あれらは投げ先の文字ではなく Hyperion の**演算**の綴り）。
!txt ★`translate` は**この本が持つ翻訳の宣言**＝`0`（Thm全体への「高階言語」への翻訳・
!txt   FCL→TFL・cvt）と `sc`（{s,c}ソート）。
!txt   ★★**翻訳の名前がそのまま印**＝`inference` 行に `goal|0` として出るのはこの名前
!txt   （2026-09-01 須田さん。08-29 の `文字=翻訳` の表は無くなった。
!txt   2026-09-06＝対象言語の名前`TFL`/`TML`を撤回し、論理の添字`1`/`sc`へ戻した。
!txt   ★★★2026-09-14夜＝翻訳の名前を`1`から`0`へ再改称＝`0_tutorial/3.book`「prop, Thm」節の
!txt   `\|0`と綴りを揃えた。中身は不変＝「`\|0`は以前の`\|1`」（須田さん））。
!txt   **この行は許可を与えない**。
!txt ★★`inference` 行が**この本の書ける関係**を決める（2026-08-29 須田さん）。
!txt   読み方＝`-|` は「Thm全体`(goal ◀ sos)`を`\|0`で「高階言語」へ翻訳し、結果の`◁`のThmで
!txt   推論できる」（★★2026-09-14夜 訂正＝以前は「goalとsosを個別に一階翻訳してから`◀1`で」
!txt   だったが、goal・sosを個別に翻訳する規則はBookに無い（須田さん指摘）ため撤回。
!txt   `0_tutorial/3.book`「prop, Thm」節の`P -\| Γ … (P ◀ Γ)\|0`が正本）。
!txt   ★`\|0`＝**c-Formを含まなければ高階言語へ自然に翻訳したもの、そうでなければエラー**
!txt   （`0_tutorial/3.book`「prop, Thm」節が正本）。結果の`◁`のThmは、c-Formが無い内容では
!txt   単ソート一階論理（等号公理＋領域の非空性公理・Prover9の論理）としてそのまま確かめられる。
!txt   ★**素の `◀` はこれとは別の関係 `◀sc`**（{s,c}ソート論理と v^-Formのメタ論理・ソートを消さない段。
!txt   `0_tutorial/3_Thmel1.book`「命題変数を含むThm」節が正本）へ縮む＝段が違う。
!txt   `--|` は同じことを{s,c}ソート翻訳で行う。
!txt   ★★★2026-09-06 訂正＝**旧行はここで「そのとき使った W+ の語の定義（`W+.`）が仮定に
!txt   添えられる」としていたが撤回した**（「その `,, W+.` は間違いのハズ」＝書かれていない
!txt   仮定を機械が足していた）。`--|` は今 `◀sc` と同じ仮定だけを見る。
!txt   ★`backend` と同じ「宣言であって定義ではない」＝実装の表と食い違えば理由付きで拒否される。
!txt   ★素の `◀` は宣言が要らない（どの本でも書ける＝翻訳に何も頼っていない主張だから）。
backend p=prover+ v=vampire+ h=hyperion
target p v h

!txt ★`search:` の印が付く行は**探索設定**＝同じ問題を同じ形で投げ、待つ長さや戦略だけが変わる
!txt   （数学的な意味は変えない）。意味を変える規則を足すときは、この印を持たない綴りにする。
!txt ★下の 10 秒は 2026-08-24 まで PHP に直書きされていた値そのもの＝挙動は変わっていない。
prover9 search:seconds 10
!txt ★Vampire の秒も同じ形（2026-08-29）。20 は 2026-08-29 まで査読器に直書きされていた値そのもの。
vampire search:seconds 20

!txt ★★`prover+` は**役**の設定＝上の2行（実行ファイル宛）とは層が違う。
!txt   `problem:` は「投げる問題の形」の印で、`search:`（待つ長さだけ）とは**別の印**。
!txt   `split`（既定）＝Prover+ が1つの Thm を複数のリクエストへ割る／`whole`＝割らずに1本で投げる。
!txt   ★どちらでも**主張している Thm は同じ**＝変わるのは何本の問題を何回投げるかだけ。
!txt   ★Vampire+ には効かない（あちらは元から割らない）。
prover+ problem:split

common/default.thmel

`common/default.thmel`