- * := \lrf.l(rf)
- * 3 4 := (\lrf.l(rf)) 3 4
- ~~> (\rf.3(rf)) 4
- ~~> \f.3(4f)
- == \f.(\fz.f(f(fz)))(4f)
- ~~> \fz.(4f)((4f)((4f)z))
- == \fz.((\fz.f(f(f(fz))))f) (((\fz.f(f(f(fz))))f) (((\fz.f(f(f(fz))))f) z))
- ~~> \fz.((\z.f(f(f(fz)))) ((\z.f(f(f(fz)))) ((\z.f(f(f(fz))))z)))
- ~~> \fz.((\z.f(f(f(fz)))) ((\z.f(f(f(fz)))) (f(f(f(fz))))))
- ~~> \fz.((\z.f(f(f(fz)))) (f(f(f(f(f(f(f(fz)))))))))
- ~~> \fz.f(f(f(f(f(f(f(f(f(f(f(fz)))))))))))
- == 12
-
-Is the final result simpler? This time, the answer is not so straightfoward.
+ mul ≡ \l r. \f z. r (l f) z
+
+ mul 4 3 ≡ (\l r. \f z. r (l f) z) 4 3
+ ~~> \f z. 3 (4 f) z
+ ≡ \f z. (\f z. f (f (f z))) (4 f) z
+ ~~> \f z. (4 f) ((4 f) (4 f z))
+ ≡ \f z. ((\f z. f (f (f (f z)))) f) (((\f z. f (f (f (f z)))) f) ((\f z. f (f (f (f z)))) f z))
+ ~~> \f z. (\z. f (f (f (f z)))) ((\z. f (f (f (f z)))) (f (f (f (f z)))))
+ ~~> \f z. (\z. f (f (f (f z)))) (f (f (f (f (f (f (f (f z))))))))
+ ~~> \f z. f (f (f (f (f (f (f (f (f (f (f (f z)))))))))))
+ ≡ 12
+
+Is the final result simpler? This time, the answer is not so straightforward.