> reduceNF (myparse "(\\x.\\y.zxy)w") ["(\\x.\\y.zxy)w", "\\b.zwb", "zw"] > reduceNF (myparse "(\\x.\\y.zxy)(wy)") ["(\\x.\\y.zxy)(wy)", "\\b.z(wy)b", "z(wy)"] > reduceNF (myparse "(\\n.\\f.\\x.nf(fx))(\\f.\\x.fx)") ["(\\n.\\f.\\x.nf(fx))(\\f.\\x.fx)", "\\b.\\c.(\\f.\\x.fx)b(bc)", "\\b.\\c.(\\c.bc)(bc)", "\\b.\\c.b(bc)"] 

> prettyprint (chSucc (church 2)) "\\f.\\x.f(f(fx))" > prettyprint (chIsZero (church 0)) "\\x.\\y.x" > prettyprint (chPlus (chSucc (church 2)) (church 3)) "\\f.\\x.f(f(f(f(f(fx)))))" > prettyprint (chMult (church 2) (church 3)) "\\f.\\b.f(f(f(f(f(fb)))))" > prettyprint (chExp (church 2) (church 3)) "\\b.\\c.b(b(b(b(b(b(b(bc)))))))" > prettyprint (chNot chFalse) "\\x.\\y.x" > prettyprint (chSnd (chPair (church 2) (church 3))) "\\f.\\x.f(f(fx))" > prettyprint (chOr chFalse chTrue) "\\x.\\y.x"