置換補題

補題 3.5（「契約による設計」§3）・ ✓公理まで証明済み

算術式 $a, a'$ 、ブール式 $b$ 、変数 $x$ 、状態 $\sigma$ について

\llbracket a'[a/x] \rrbracket\sigma = \llbracket a' \rrbracket\bigl(\sigma[x \mapsto \llbracket a \rrbracket\sigma]\bigr), \qquad \llbracket b[a/x] \rrbracket\sigma = \llbracket b \rrbracket\bigl(\sigma[x \mapsto \llbracket a \rrbracket\sigma]\bigr)

が成り立つ。とくに、ブール式 $b$ を表明とみたとき、式の書き換え $b[a/x]$ が表す表明は定義 3.4 の $b[a/x]$ と一致する。

閉包の状態

✓ 公理まで証明済み

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

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

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

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