English version
では調子に乗って SUCC 1 を計算してみよう．
SUCC 1
= (λ n f x. f (n f x))(λ f x. f x)
= (λ f x. f ((λ f x. f x) f x))
= (λ f x. f ((λ x. f x) x))
= (λ f x. f (f x))
= λ f x. f (f x)
= 2
下線部分が置き替わっていくところである。
SUCC 1 は 2 である．
((λ f x. f x) f x))
がわかりにくい場合にはまた変数名を変えておこう．
((λ f x. f x) f x)) は ((λ f x. f x) f x)) と同じである。
((λ g h. g h) f x)) ... f を g に代入
((λ h. f h) x)) ... h を x に代入
(f x)
いかがだろうか．