book集

!txt min.thmel — 最小の Thmel（2026-09-01 須田さん）
!txt
!txt ★★★**Formel は {s,c}-ソート言語なので、backendへ送るときもソートを保つ**。
!txt   素の `◀` は一階翻訳を通らない。Prover+へはソートを一項述語にした相対化、Vampire+へは
!txt   多ソートTFFとして送り、元の関係 `◀sc` を確かめる。
!txt   `-|` だけが、Thm全体を `|0` で「高階言語」へ翻訳し（c-Formが残っていれば失敗）、
!txt   結果の `◁` のThmを確かめる（`0_tutorial/3.book`「prop, Thm」節の `(P ◀ Γ)|0` が正本。
!txt   ★★2026-09-14夜 訂正＝以前ここは「単ソートの関係 `◀1` を確かめる」だったが、
!txt   goal・sosを個別に翻訳する規則はBookに無い（須田さん指摘）ため撤回。中身（FCL→TFL・cvt）は
!txt   不変で、名前だけ `|1` から `|0` へ変わった＝「`|0`は以前の`|1`」（須田さん））。
!txt
!txt ★`backend` は**宣言**＝どの文字がどの投げ先を指すか（prf の段 `G ◀ Γ p;` の `p`）。
!txt ★`target` は**制限**＝ここに書いていない投げ先へ投げる綴りは理由付きで拒否される。
!txt ★★2026-09-14＝**`s=satallax+` を追加**（`-| … s;`＝単ソートMCL→TFLのみ。多ソート`--| … s;`・
!txt   命題変数量化`---| … s;`はまだSatallax+ backend実装の対象外＝この本が書けるのは`-| … s;`だけ）。
backend p=prover+ v=vampire+ s=satallax+ h=hyperion
target p v s h

!txt ★★★**この本の対象言語が持つソート**（2026-09-02 須田さん「.thmelファイルで指定する。
!txt   min.thmelではs,cのみ。少なくとも最初の説明では f は出さないで欲しい」）。
!txt   ★**Formel は {s,c}-ソート言語**なので、min はその2つ。
!txt   ★**`f`（関数値のソート）は書かない**＝`\fn` / `ap` / `Rest` を送るときに翻訳の側で生まれる
!txt     ソートで、min.formel はその語を持たない。**書いていないソートが出たら理由付きで拒否される**
!txt     （`target` と同じ「制限」）。
!txt   ★**効くのは多ソートを送る道**＝Vampire へ出す TFF の型宣言（`tff(mathel_s: $tType).` …）。
!txt     相対化して Prover9 へ送る道の Ax は、これとは別に**実際に出たソートだけ**に添える
!txt     （型宣言は仮定を増やさないが、非空性の公理は仮定を増やすため）。
sort s c

!txt ★**翻訳の宣言**＝この本が使ってよい翻訳。一階翻訳と{s,c}ソート翻訳の両方（2026-09-06 須田さん決定）。
!txt   ★★これで `--|`（{s,c}ソート翻訳した ◀）が書けるようになる。**`◀ … v;`（Vampireへ素の関係）は
!txt   Thm査読を通らない**（須田さん「v◀ は不可・ただし禁止はコンパイルでなく査読で」＝
!txt   `BookThmReviewer::assertBareVampireRelationAllowed()`）＝`cls` を含む
!txt   Thm を bare `◀` で検査すると `ax_s0/class_comprehension.php::lowerProblem()` が
!txt   **書かれていない**クラス内包公理を黙って足す穴があるため（`◀ … p;` にも同じ穴が残るが、
!txt   須田さんが査読で塞いだのは `◀ … v;` だけ）。
!txt   ★★★2026-09-06 その2＝翻訳の名前を`TFL`/`TML`から論理の添字`1`/`sc`へ戻した
!txt   （`◀1`/`◀sc`と同じ添字）＝「対象言語に新しい名前を立てる」よりも「使う論理の名前で
!txt   直接呼ぶ」方が説明が要らない、という判断（`0_tutorial/3_Thmel.book`「一階翻訳、
!txt   {s,c}ソート翻訳」節）。あわせて `--|` が仮定へ `,, W+.` を自動で添えていたのも撤回した
!txt   （「その `,, W+.` は間違いのハズ」＝書かれていない仮定を機械が足していた）。
!txt   `--|` はいま `◀sc` と同じ仮定だけを見る。
!txt   ★★2026-09-14夜＝`-|` が使う翻訳の名前を `1` から `0` へ改称した（`|0`＝Thm全体への翻訳。
!txt   下の「一階翻訳の宣言」を参照）。`L_1`（prover+が判定する論理）という名前自体は不変で、
!txt   変わったのは`.thmel`内部の翻訳トークンの綴りだけ。
translate 0 sc

!txt ★★**`◀` が何を意味するかを綴る行**（2026-09-04 須田さん＝右辺は `◀1` ではなく `◀sc`）。
!txt   `◀sc` ＝ **{s,c}ソート論理と v^-Form のみを含むメタ論理**の推論関係（`0_tutorial/3_Thmel1.book`
!txt   「命題変数を含むThm」節が正本）。**ソートを消さない段**＝素の `◀` はここで検査する。
!txt   ★下の `-|` とは段が違う＝あちらはThm全体を `|0` で「高階言語」へ翻訳した後の段（`◁`）。
!txt   ★**各ソートの非空性は、この論理を名指しした時点で最初から入っている**（多ソート構造の
!txt     標準的な定義そのもの＝単ソート一階論理で領域が空でないのと同じ立場）。Mathelia が
!txt     足しているのではないので「暗黙」ではなく、**論理を正しく名指ししているだけ**。
!txt   ★**この行は式を1本も増やさない**＝ソート宣言そのものが持つ性質を、名前で引き受けている。
inference goal ◀ sos <-> goal ◀sc sos

!txt ★★**`|0`（Thm全体への翻訳）の宣言**（2026-09-01。旧称 TFL翻訳。★★2026-09-14夜＝
!txt   翻訳の名前を`1`から`0`へ改称し、右辺をgoal・sos個別の`◀1`から「Thm全体を`|0`で
!txt   変換する」形`(goal ◀ sos)|0`へ訂正＝`0_tutorial/3.book`「prop, Thm」節の
!txt   `P -| Γ … (P ◀ Γ)|0`が正本。中身は不変、綴りだけの訂正）。**この行が無いと c を使った
!txt   Thm が査読で拒否される**（実測＝「この本の Thmel は「高階言語」への翻訳を持ちません」）。
!txt   ★`min.formel` は c を持つ（`∈_` `∀_ ∃_` `=_`）ので、この行は**必須**。
!txt   ★この行は `-|` の翻訳を引き受ける宣言であり、素の `◀` の検査経路は変えない。
inference goal -| sos <-> (goal ◀ sos)|cvt+|0

!txt ★★**{s,c}ソート翻訳の宣言**（2026-09-06。旧称 TML翻訳）。`--|` は{s,c}ソート言語のまま
!txt   推論できることを主張する。
!txt   ★投げ先は綴りに出す＝`--| … p;` は Prover+（ソートを相対化）、`--| … v;` は Vampire+（多ソートTFF）。
!txt   ★★2026-09-06 訂正＝旧行は仮定へ `,, W+.`（使った wordG1 の語の定義）を自動で添えていたが、
!txt   「書かれていない仮定を機械が足さない」原則に反するため撤回した。W+ の語を使う証明は、
!txt   その定義Propを `◀` の右に自分で引用する（`compileTml()` の「仮定は引用したものだけ」）。

!txt ★`search:` の印が付く行は**探索設定**＝同じ問題を同じ形で投げ、待つ長さだけが変わる。
prover9 search:seconds 10

common/min.thmel

`common/min.thmel`