チャーチ＝ロッサーの帰結

系 4.6（「型なしラムダ計算」§4）・ ✓公理まで証明済み

(1) $M=_\beta N$ であることと、 $M\twoheadrightarrow_\beta P$ かつ $N\twoheadrightarrow_\beta P$ となる $P$ が存在することは同値である。

(2) 正規形は、存在すればただ一つである。さらに $M=_\beta N$ で $N$ が正規形なら $M\twoheadrightarrow_\beta N$ 。

(3) $\lambda xy.x\ne_\beta\lambda xy.y$ 。とくに $=_\beta$ はすべての項を等しくするような自明な関係ではない。

閉包の状態

✓ 公理まで証明済み

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

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

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

チャーチ＝ロッサーの定理✓定理 4.1・型なしラムダ計算
- 三角補題✓補題 4.5・型なしラムダ計算
  - 並行簡約と置換✓補題 4.4・型なしラムダ計算
    置換補題✓補題 2.3・型なしラムダ計算
- 並行簡約の基本性質✓補題 4.3・型なしラムダ計算