Арифметика с церковными числами

Я работаю через SICP, и проблема 2.6 поставила меня в затруднительное положение. . Имея дело с числами Чёрча, концепция кодирования нуля и 1 как произвольных функций, удовлетворяющих определенным аксиомам, кажется разумной. Кроме того, имеет смысл получение прямой формулировки отдельных чисел с использованием определения нуля и функции сложения-1. Я не понимаю, как может быть сформирован оператор плюса.

Пока что у меня есть это.

(define zero (lambda (f) (lambda (x) x)))
(define (add-1 n)
  (lambda (f) (lambda (x) (f ((n f) x)))))

(define one (lambda (f) (lambda (x) (f x))))
(define two (lambda (f) (lambda (x) (f (f x)))))

Просматривая запись в википедии для лямбда-исчисления , Я обнаружил, что определение плюса было PLUS: = λmnfx.mf (nfx). Используя это определение, я смог сформулировать следующую процедуру.

(define (plus n m)
  (lambda (f) (lambda (x) ((m f) ((n f) x)))))

Чего я не понимаю, так это того, как эта процедура может быть получена напрямую, используя только информацию, предоставленную ранее полученными процедурами. Может ли кто-нибудь ответить на этот вопрос в какой-нибудь строгой доказательной форме? Интуитивно я думаю, что понимаю, что происходит, но, как однажды сказал Ричард Фейнман: «Если я не могу построить это, я не могу этого понять ...»