Чистое лямбда исчисление

[overwriter]

Доказать I = SKK:

Расписал комбинаторы через лямбда исчисление, оно ведь должно доказываться и так, далее провожу некоторые подстановки и получаю (последняя строчка) какой-то не преобразуемый к нужному результат.


$ $\lambda$x.x = ($\lambda$fgs.f s (g s)) ($\lambda$pq.p) $\lambda$zw.z $\lambda$x.x = ($\lambda$gs.($\lambda$pq.p) s (g s)) $\lambda$zw.z $\lambda$x.x = ($\lambda$s.($\lambda$pq.p) s (($\lambda$zw.z) s)) $\lambda$x.x = $\lambda$s.($\lambda$pq.p) s (($\lambda$zw.z) s) $\lambda$x.x = $\lambda$s.($\lambda$pq.p) s ($\lambda$w.s) $\lambda$x.x = $\lambda$s.($\lambda$q.s) ($\lambda$w.s) $

[arseniiv]

А аппликацию $(\lambda q.s)(\lambda w.s)$ допреобразовать не хотите?

P. S. Надо только формулу целиком долларами окружать, а не $\lambda$ в ней. Да и, наверно, это очень неудобно!