我正在尝试了解 lambda 演算和 Church 数字的基础知识。我一直在做大量的阅读和练习，但我似乎一直在试图了解某些功能是如何工作的。
我坚持的例子如下。也许有人可以解释我哪里出错了。
1 的教堂数字可以表示为：
λf. λx. f x
Church 数 (m n ) 的幂函数可以表示为：
λm. λn. n m
我要做的就是证明，通过将幂函数应用于 1 和 1，我得到了 1，因为 1 1 = 1。我正在这样做，所以我更好地理解了这些函数是如何工作的。我的工作如下，每次都卡住：
// Exp (1 1)
(λm. λn. n m) (λf1. λx1. f1 x1) (λf2. λx2. f2 x2)
// Substitute for m
(λn. n (λf1. λx1. f1 x1)) (λf2. λx2. f2 x2)
// Substitute for n
(λf2. λx2. f2 x2) (λf1. λx1. f1 x1)
// Substitute for f2
(λx2. (λf1. λx1. f1 x1) x2)
// Substitute for f1
λx2. (λx1. x2 x1)
我被困住了。我已经失去了两个f'，只剩下x'，我没有得到 1 回来。我哪里错了？