$\mbox{(a) } [P/v][v/x]M ≡ [P/x]M \mbox{ if } v \notin FV(M);$

$\begin{array} & \mbox{(1) } M=x \mbox{ の時 (1.12(a))} \\ \mbox{左辺 } [P/v][v/x]x = [P/v]v = P \\ \mbox{右辺 } [P/x]x = P \\ \therefore \mbox{(1)の時、左辺 ≡ 右辺} \\ \mbox{(2) } M=a \mbox{ の時 (1.12(b)) } \\ \mbox{左辺 } [P/v][v/x]a = [P/v]a = a \\ \mbox{右辺 } [P/x]a = a \\ \therefore \mbox{(2)の時、左辺 ≡ 右辺} \\ \mbox{(3) } M=(RS) \mbox{ の時 (1.12(c))} \\ \mbox{左辺 } [P/v][v/x](RS) = [P/v]([v/x]R [v/x]S) \\ = ([P/v][v/x]R [P/v][v/x]S) \\ \mbox{;; ここで帰納法により } \\ \mbox{;; } [Z/w][w/u]N ≡ [Z/u]N \\ \mbox{;; が正しいと仮定して以下を導きます} \\ = ([P/x]R \, [P/x]S) \\ \mbox{右辺 } [P/x](RS) = ([P/x]R \, [P/x]S) \\ \therefore \mbox{(3)の時、左辺 ≡ 右辺} \\ \mbox{(4) } M=λx.L \mbox{ の時 (1.12(d))} \\ \mbox{左辺 } [P/v][v/x](λx.L) = [P/v](λx.L) \\ \mbox{;; ここで条件 } v \notin FV(M) \mbox{ より} \\ \mbox{;; } v \notin FV(λx.L) \Rightarrow v \notin FV(L) \mbox{ だから } \\ = λx.L \\ \mbox{右辺 } [P/x](λx.L) = λx.L \\ \therefore \mbox{(4)の時、左辺 ≡ 右辺} \\ \mbox{(5) } M=λy.L, \; x \notin FV(L) \mbox{ の時 (1.12(e))} \\ \mbox{左辺 } [P/v][v/x](λy.L) = [P/v](λy.L) \\ \mbox{;; ここで条件 } v \notin FV(M) \mbox{ より} \\ \mbox{;; } v \notin FV(λy.L) \Rightarrow v \notin FV(L) \mbox{ だから } \\ = λy.L \\ \mbox{右辺 } [P/x](λy.L) = λy.L \\ \therefore \mbox{(5)の時、左辺 ≡ 右辺} \\ \mbox{(6) } M=λy.L, \; x \in FV(L) \mbox{ and } y ≠ x \mbox{ (1.12(f)) では} \\ \mbox{;; “and let no variable bound in M be free in vPQ.” つまり} \\ \mbox{;; } y \notin FV(vPQ) \mbox{ より} \\ \mbox{;; 特に } y \notin FV(PQ) \mbox{ より} \\ \mbox{左辺 } [P/v][v/x](λy.L) = [P/v](λy.[v/x]L) = λy.[P/v][v/x]L \\ \mbox{;; ここで帰納法により } \\ \mbox{;; } [Z/w][w/u]N ≡ [Z/u]N \\ \mbox{;; が正しいと仮定して以下を導きます} \\ = λy.[P/x]L \\ \mbox{右辺 } [P/x](λy.L) \\ \mbox{;; (6)の左辺と同様に} \\ \mbox{;; “and let no variable bound in M be free in vPQ.” つまり} \\ \mbox{;; } y \notin FV(vPQ) \mbox{ より} \\ = λy.[P/x]L \\ \therefore \mbox{(6)の時、左辺 ≡ 右辺} \\ \mbox{(1) 〜 (6) より } [P/v][v/x]M ≡ [P/x]M \mbox{ if } v \notin FV(M). \end{array}$

$\mbox{(b) } [x/v][v/x]M ≡ M \mbox{ if } v \notin FV(M);$

$\begin{array} & \mbox{(a) より} \\ \mbox{左辺 } [x/v][v/x]M = [x/x]M \\ \mbox{1.15(a) より } [x/x]M ≡ M \mbox{ だから} \\ = M \\ \therefore \mbox{左辺 ≡ 右辺 なので} \\ [x/v][v/x]M ≡ M \mbox{ if } v \notin FV(M);. \end{array}$

$\mbox{(c) } [P/x][Q/y]M ≡ [([P/x]Q)/y][P/x]M \mbox{ if } y \notin FV(P);$

$\begin{array} & \mbox{(1) } M=x \mbox{ の時 (1.12(a))} \\ \mbox{左辺 } [P/x][Q/y]x = [P/x]x = P \\ \mbox{右辺 } [([P/x]Q)/y][P/x]x = [([P/x]Q)/y]P \\ \mbox{;; ここで } y \notin FV(P) \mbox{ なので } \\ = P \\ \therefore \mbox{(1)の時、左辺 ≡ 右辺} \\ \mbox{(1)' } M=y \mbox{ の時 (1.12(a))} \\ \mbox{左辺 } [P/x][Q/y]y = [P/x]Q \\ \mbox{右辺 } [([P/x]Q)/y][P/x]y = [([P/x]Q)/y]y = [P/x]Q \\ \therefore \mbox{(1)'の時、左辺 ≡ 右辺} \\ \mbox{(2) } M=a \mbox{ の時 (1.12(b))} \\ \mbox{左辺 } [P/x][Q/y]a = [P/x]a = a \\ \mbox{右辺 } [([P/x]Q)/y][P/x]a = [([P/x]Q)/y]a = a \\ \therefore \mbox{(2)の時、左辺 ≡ 右辺} \\ \mbox{(3) } M=(RS) \mbox{ の時 (1.12(c))} \\ \mbox{左辺 } [P/x][Q/y](RS) = [P/x]([Q/y]R [Q/y]S) \\ = ([P/x][Q/y]R \, [P/x][Q/y]S) \\ \mbox{;; ここで帰納法により } \\ \mbox{;; } [V/w][Z/u]N ≡ [([V/w]Z)/u][V/w]N \mbox{ if } u \notin FV(V); \\ \mbox{;; が正しいと仮定して以下を導きます} \\ = ([([P/x]Q)/y][P/x]R \, [([P/x]Q)/y][P/x]S) \\ \mbox{右辺 } [([P/x]Q)/y][P/x](RS) = [([P/x]Q)/y]([P/x]R [P/x]S) \\ = ([([P/x]Q)/y][P/x]R \, [([P/x]Q)/y][P/x]S) \\ \therefore \mbox{(3)の時、左辺 ≡ 右辺} \\ \mbox{(4) } M=λx.L \mbox{ の時 (1.12(d), 1.12(f))} \\ \mbox{左辺 } [P/x][Q/y](λx.L) \\ \mbox{;; 1.12(f) より} \\ = [P/x](λx.[Q/y]L) \\ \mbox{;; 1.12(d) より} \\ = λx.[Q/y]L \\ \mbox{右辺 } [([P/x]Q)/y][P/x](λx.L) \\ \mbox{;; 1.12(d) より} \\ = [([P/x]Q)/y](λx.L) \\ \mbox{;; 1.12(f) より} \\ = λx.[([P/x]Q)/y]L \\ \mbox{;; ここで定義} \\ \mbox{;; “and let no variable bound in M be free in vPQ.” つまり} \\ \mbox{;; } x \notin FV(vPQ) \mbox{ 特に } x \notin FV(Q) \mbox{ より} \\ = λx.[Q/y]L \\ \therefore \mbox{(4)の時、左辺 ≡ 右辺} \\ \mbox{(4)' } M=λy.L \mbox{ の時 (1.12(d), 1.12(f))} \\ \mbox{左辺 } [P/x][Q/y](λy.L) \\ \mbox{;; 1.12(d) より} \\ = [P/x](λy.L) \\ \mbox{;; 1.12(f) より} \\ = λy.[P/x]L \\ \mbox{右辺 } [([P/x]Q)/y][P/x](λy.L) \\ \mbox{;; 1.12(f) より} \\ = [([P/x]Q)/y](λy.[P/x]L) \\ \mbox{;; 1.12(d) より} \\ = λy.[P/x]L \\ \therefore \mbox{(4)'の時、左辺 ≡ 右辺} \\ \mbox{(5) } M=λz.L, x \notin FV(L), y \notin FV(L) \mbox{ の時 (1.12(e)))} \\ \mbox{左辺 } [P/x][Q/y](λz.L) = λz.L \\ \mbox{右辺 } [([P/x]Q)/y][P/x](λz.L) = λz.L \\ \therefore \mbox{(4)''の時、左辺 ≡ 右辺} \\ \mbox{・1.12(g) について} \\ (g) [N/x](λy.P) ≡ λz.[N/x][z/y]P \mbox{ if } x \in FV(P), y \in FV(N) \\ \mbox{ここで定義 “and let no variable bound in M be free in vPQ.” つまり} \\ x \notin FV(vPQ) \mbox{ 特に } x \notin FV(PQ) \mbox{ より} \\ \mbox{1.12(g) は成り立たない.} \\ \therefore \mbox{(1)〜(5) より} \\ [P/x][Q/y]M ≡ [([P/x]Q)/y][P/x]M \mbox{ if } y \notin FV(P);. \end{array}$

$\mbox{(d) } [P/x][Q/y]M ≡ [Q/y][P/x]M \mbox{ if } y \notin FV(P), x \notin FV(Q);$

$\begin{array} & \mbox{左辺 } [P/x][Q/y]M \\ \mbox{(c) } [P/x][Q/y]M ≡ [([P/x]Q)/y][P/x]M \mbox{ if } y \notin FV(P); \mbox{ より} \\ = [([P/x]Q)/y][P/x]M \\ \mbox{;; ここで 1.15(b): } \\ x \notin FV(M) \Rightarrow [N/x]M ≡ M \mbox{ より} \\ \mbox{;; 特に } x \notin FV(Q) \Rightarrow [P/x]Q ≡ Q \\ = [Q/y][P/x]M \mbox{;; これは右辺に等しい} \\ \therefore [P/x][Q/y]M ≡ [Q/y][P/x]M \mbox{ if } y \notin FV(P), x \notin FV(Q);. \end{array}$

$\mbox{(e) } [P/x][Q/x]M ≡ [([P/x]Q)/x]M$

$\begin{array} & \mbox{(1) } M=x \mbox{ の時 (1.12(a))} \\ \mbox{左辺 } [P/x][Q/x]x = [P/x]Q \\ \mbox{右辺 } [([P/x]Q)/x]x = [P/x]Q \\ \therefore \mbox{(1)の時、左辺 ≡ 右辺} \\ \mbox{(2) } M=a \mbox{ の時 (1.12(b))} \\ \mbox{左辺 } [P/x][Q/x]a = [P/x]a = a \\ \mbox{右辺 } [([P/x]Q)/x]a = a \\ \therefore \mbox{(2)の時、左辺 ≡ 右辺} \\ \mbox{(3) } M=(RS) \mbox{ の時 (1.12(c))} \\ \mbox{左辺 } [P/x][Q/x](RS) = [P/x]([Q/x]R [Q/x]S) \\ = ([P/x][Q/x]R \, [P/x][Q/x]S) \\ \mbox{;; ここで帰納法により } \\ \mbox{;; } [V/w][Z/w]N ≡ [([V/w]Z)/w]N \\ \mbox{;; が正しいと仮定して以下を導きます} \\ = ([([P/x]Q)/x]R \, [([P/x]Q)/x]S) \\ \mbox{右辺 } [([P/x]Q)/x](RS) \\ = ([([P/x]Q)/x]R \, [([P/x]Q)/x]S) \\ \therefore \mbox{(3)の時、左辺 ≡ 右辺} \\ \mbox{(4) } M=λx.L \mbox{ の時 (1.12(d))} \\ \mbox{左辺 } [P/x][Q/x](λx.L) = [P/x](λx.L) = λx.L \\ \mbox{右辺 } [([P/x]Q)/x](λx.L) = λx.L \\ \therefore \mbox{(4)の時、左辺 ≡ 右辺} \\ \mbox{(5) } M=λy.L, \; x \notin FV(L) \mbox{ の時 (1.12(e))} \\ \mbox{左辺 } [P/x][Q/x](λy.L) = [P/x](λy.L) = λy.L \\ \mbox{右辺 } [([P/x]Q)/x](λy.L) = λy.L \\ \therefore \mbox{(5)の時、左辺 ≡ 右辺} \\ \mbox{(6) } M=λy.L, \; x \in FV(L) \mbox{ and } y ≠ x \mbox{ (1.12(f))} \\ \mbox{;; “and let no variable bound in M be free in vPQ.” つまり} \\ \mbox{;; } y \notin FV(PQ) \mbox{ より} \\ \mbox{左辺 } [P/x][Q/x](λy.L) = [P/x](λy.[Q/x]L) = λy.[P/x][Q/x]L \\ \mbox{;; ここで帰納法により } \\ \mbox{;; } [V/w][Z/w]N ≡ [([V/w]Z)/w]N \\ \mbox{;; が正しいと仮定して以下を導きます} \\ = λy.[([P/x]Q)/x]L \\ \mbox{右辺 } [([P/x]Q)/x](λy.L) \\ \mbox{;; (6)の左辺と同様に} \\ \mbox{;; “and let no variable bound in M be free in vPQ.” つまり} \\ \mbox{;; } y \notin FV(vPQ) \mbox{ より} \\ \mbox{;; 特に } y \notin FV(PQ) \mbox{ より} \\ = λy.[([P/x]Q)/x]L \\ \therefore \mbox{(6)の時、左辺 ≡ 右辺} \\ \mbox{(1) 〜 (6) より } [P/x][Q/x]M ≡ [([P/x]Q)/x]M. \end{array}$