$(c_2) \mbox{ x does not occur free in X }$

$\begin{array} & \begin{array}{llll} (c) & [M/x][N/y]X &≡ [N'/y][M/x]X & \mbox{ ;; (b) より } \\ & [M/x][N/y]X &≡ [N'/y]X. \end{array} \end{array}$

$\begin{array} & \begin{array}{lll} X\ast &≡ [M/x]X. & \mbox{ ;; (b) より } \\ &≡ X. & \mbox{ ;; } (c_2) \mbox{ の前提より } \\ X\# &≡ [M/x]X. & \mbox{ ;; (b) より } \\ &≡ X. & \mbox{ ;; } (c_2) \mbox{ の前提より } \\ \end{array} \\ \therefore X\ast ≡ X\#. \end{array}$

$\begin{array} & \begin{array}{lll} N' &≡ [M/x]N & \mbox{ ;; なので ( (c) より) } \\ &≡ N & \mbox{ ;; 前提より } \\ \end{array} \\ \mbox{ ;; Case 1 (a) は } (c_2) \mbox{ の前提によりなりたたない} \\ \mbox{ ;; Case 1 (b) } X ≡ y ≠ x \\ \begin{array}{lll} X\ast &≡ [M/x][N/y]y & \\ &≡ [M/x]N & \mbox{ ;; 前提より } \\ &≡ N & \\ X\# &≡ [N/y]y & \\ &≡ N & \end{array} \\ \therefore X\ast ≡ X\#. \\ \\ \mbox{ ;; Case 2 } \\ \mbox{ 帰納法により } \\ X\ast ≡ X\astY\ast ≡ X\#Y\# ≡ X\# \\ \therefore X\ast ≡ X\#. \\ \mbox{ ;; Case 3 (a)} \\ X ≡ λzY \mbox{ と置く } \\ \mbox { ;; 前提より (x does not occur in N) から z ≡ x が成り立つ} \\ \begin{array}{lll} X\ast &≡ [M/x][N/y]λxY & \\ &≡ [M/x]λx.[N/y]Y & \\ &≡ λx.[N/y]Y & \\ X\# &≡ [N/y]λxY & \\ &≡ λx.[N/y]Y & \\ \end{array} \\ \\ \mbox { ;; Case 3 (a)} \\ X ≡ λzY \mbox{ と置く } \\ \mbox { ;; 前提より } (c_2) \mbox{ z ≡ y が成り立つ} \\ \begin{array}{lll} X\ast &≡ [M/x][N/y]λyY & \\ &≡ [M/x]λyY & \\ &≡ λy.[M/x]Y & \mbox{ ;; 前提より } (c_2) \\ && \mbox{ x does not occur free in X }\\ && (X ≡ λyY) \\ &≡ λyY & \\ X\# &≡ [N/y]λyY & \\ &≡ λyY & \\ \end{array} \\ \therefore X\ast ≡ X\#. \\ \\ \mbox { ;; Case 3 (b)} \\ \mbox { ;; もともとの前提より } \\ \mbox { ;; (c) If no variables which occur free in M or N are boun in X } \\ \mbox { ;; z ≠ x, z ≠ y なので、 成り立たない} \\ \\ \end{array}$