不変量の原理

定理 8.2（「証明の技術」§8）・ ✓公理まで証明済み

$I$ が不変量で $x\to^*x'$ ならば $I(x)=I(x')$ である。したがって $I(a)\ne I(b)$ なら、 $b$ は $a$ から到達できない。
$V$ が単調量ならば、操作を無限にくり返せる状態列 $x_0\to x_1\to x_2\to\cdots$ は存在しない。とくに、 $x_0$ から始めて操作を続けると、必ず $V(x_0)$ 回以内に、これ以上操作できない状態に行き着く。

閉包の状態

✓ 公理まで証明済み

証明が使う定理を前提としてたどると、Rikai の中の証明だけで定義・公理（物理では基本仮定）までつながっています（前提の定理類 0 件、定義なども含めて 1 件）。

印の意味: ✓公理まで証明済み・ △証明あり（閉包未完）・ ※主張のみ。テーマごとの集計は閉包の状況。

▸ を開くと、その項目の証明が使う前提が出ます。深い先は各項目のページでたどれます。

証明で明示的に参照している定理は、まだありません。