補助定理1.2.36と定理1.2.37の証明おわったー

終わったと同時に記事に書き起こす気力があまりなくなりましたが重要な部分だけ書きます。
「束縛変数が与えられた有限集合と重なりがないようにα変換できる」を有効に活用することでなんとか証明が完成しました。
証明の中で命題を適用する際の細かい前提条件の確認は省略します。

既知とする命題

• イコールに関する代入の交換

x ≢ y, x ∉ FV(R), y ∉ FV(Q), FV(QR) ∩ BV(M) = ∅　⇒　[Q/x][R/y]M ≡ [R/y][Q/x]M

• イコールに関する代入の短縮

FV(Q) ∩ BV(M) = ∅　⇒　[Q/z][z/x]M ≡ [Q/x]M

• 束縛変数が与えられた有限集合と重なりがないようにα変換できる

Aは変数の有限集合　⇒　M ≡α M', BV(M') ∩ A = ∅となる項M'が存在する

• 代入操作後の項に関する束縛変数全体と変数全体の集合の上からの評価

FV(N) ∩ BV(M) = ∅　⇒　BV([N/x]M) ⊂ BV(NM)
FV(N) ∩ BV(M) = ∅　⇒　V([N/x]M) ⊂ V(NM)

• α同値な二つの項にλxをつけてもα同値

M ≡α N　⇒　λx.M ≡α λx.N

M ≡α N, FV(Q) ∩ BV(N) = ∅, [Q/x]M ≡α [Q/x]Nの証明

Mの長さに関する帰納法で証明する。
M ≡ xのときとx ∉ FV(M)のときは明らかである。
M = M_1 M_2のときはM_1とM_2に対して帰納法の仮定を用いればよい。
M ≡ λy.R, x ∈ FV(M)のときを以下で議論する。

N ≡ λz.R'と表す。[Q/x]N ≡ λz.[Q/x]R'である。

y ∈ FV(Q)かどうかによって[Q/x]Mの内容は二つの場合がある。以下では省略してy ∈ FV(Q)の場合の証明のみ記す。y ∉ FV(Q)の場合の証明もだいたい同じような議論でできる。
このとき

[Q/x]M ≡ λv.[Q/x][v/y]R
と表せる。ただしvはV(xyQR)に属さない最初の変数。

変数u ∉ V(xvQMN)をとる。
R ≡α R_0, BV(R_0) ∩ FV(vuQ) = ∅となる項R_0をとる。

イコールに関する代入の交換と短縮より、

[u/v][Q/x][v/y]R_0 ≡ [Q/x][u/v][v/y]R_0 ≡ [Q/x][u/y]R_0 …(1)

そして
[u/z][Q/x]R' ≡ [Q/x][u/z]R' …(2)
である。

R ≡α R_0に帰納法の仮定を2回適用して

[Q/x][v/y]R ≡α [Q/x][v/y]R_0
両辺にλvをつけて
λv. [Q/x][v/y]R ≡α λv. [Q/x][v/y]R_0 …(3)
である。

R_0 ≡α Rの両辺にλyをつけて

λy.R_0 ≡α λy.R
λy.R ≡α λz.R'だから
λy.R_0 ≡α λz.R'
1.2.32(2)から
[u/y]R_0 ≡α [u/z]R'
帰納法の仮定から
[Q/x][u/y]R_0 ≡α [Q/x][u/z]R'
(1),(2)を代入して
[u/v][Q/x][v/y]R_0 ≡α [u/z][Q/x]R'
1.2.32(2)から
λv.[Q/x][v/y]R_0 ≡α λz.[Q/x]R'
(3)を代入して
λv.[Q/x][v_y]R ≡α λz.[Q/x]R'
すなわち
[Q/x]M ≡α [Q/x]N

□

M ≡α N　⇒　[Q/x]M ≡α [Q/x]Nの証明

M ≡α M', FV(Q) ∩ BV(M') = ∅となる項M'をとる。
すると先ほど証明した命題から[Q/x]M ≡α [Q/x]M', [Q/x]N ≡α [Q/x]M'である。
よって[Q/x]M ≡α [Q/x]N

□

この先の概略

上で示した命題を「代入操作をしてもα同値性は保たれる」と呼ぶことにする。
「イコールに関する代入の短縮」と「代入操作をしてもα同値性は保たれる」から補助定理1.2.36(1) (「代入の短縮」):

z ∉ FV(M)　⇒　[Q/z][z/x]M ≡α [Q/x]M
が従う。

また、「イコールに関する代入の交換」と「代入操作をしてもα同値性は保たれる」から「代入の交換」:

x ≢ y, x ∉ FV(R), y ∉ FV(Q)　⇒　[Q/x][R/y]M ≡α [R/y][Q/x]M
が従う。

「代入の交換」、「代入の短縮」、「代入操作をしてもα同値性は保たれる」から

Q ≡α R　⇒　[Q/x]M ≡α [R/x]M
が示せる。
これと「代入操作をしてもα同値性は保たれる」を合わせれば補助定理1.2.36(2):
M ≡α NかつQ ≡α R　⇒　[Q/x]M ≡α [R/x]N
が得られる。

「代入の短縮」と「代入操作をしてもα同値性は保たれる」から「二つの抽象の項がα同値となる条件」:

λx.Q ≡α λy.Q'　⇔　Q' ≡α [y/x]Q, y ∉ FV(λx.Q)
が示せる。

「代入の交換」と「二つの抽象の項がα同値となる条件」から定理1.2.37:

z ∉ V(xyMN)　⇒　[N/x](λy.M) ≡α λz.[N/x][z/y]M
が示せる。

追記 (2012-12-19)

y ∈ FV(Q)かどうかの場合分けをひとつにまとめていたのだが、これには間違いがあったので、場合分けはまとめず、片方の場合の証明は省略することにした