load("lambda.js"); var g_eta = false; var g_cbv = false; function to_int(expr) { var reduced = reduce(expr, g_eta, g_cbv); if (reduced.to_int) { return reduce(reduced, false, false).to_int(0); } else { return "not a church numeral"; } } function to_string(expr) { var reduced = reduce(expr, g_eta, g_cbv); return reduced.to_string(); } function test() { function make_lam2(a, b, aa) { return make_lam(a, make_lam(b, aa)); } function make_lam3(a, b, c, aa) { return make_lam(a, make_lam(b, make_lam(c, aa))); } function make_lam4(a, b, c, d, aa) { return make_lam(a, make_lam(b, make_lam(c, make_lam(d, aa)))); } function make_lam5(a, b, c, d, e, aa) { return make_lam(a, make_lam(b, make_lam(c, make_lam(d, make_lam(e, aa))))); } function make_app3(aa, bb, cc) { return make_app(make_app(aa, bb), cc); } function make_app4(aa, bb, cc, dd) { return make_app(make_app(make_app(aa, bb), cc), dd); } function make_app5(aa, bb, cc, dd, ee) { return make_app(make_app(make_app(make_app(aa, bb), cc), dd), ee); } var s = make_var("s"); var z = make_var("z"); var m = make_var("m"); var n = make_var("n"); var u = make_var("u"); var v = make_var("v"); var d = make_var("d"); var ss = new Lambda_var(s); var zz = new Lambda_var(z); var mm = new Lambda_var(m); var nn = new Lambda_var(n); var uu = new Lambda_var(u); var vv = new Lambda_var(v); var dd = new Lambda_var(d); var succ = make_lam3(m, s, z, make_app(ss, make_app3(mm, ss, zz))); var tt = make_lam2(m, n, mm); var ff = make_lam2(m, n, nn); var kk = tt; var get1 = tt; var get2 = ff; var id = make_lam(s, ss); var ww = make_lam(s, make_app(ss, ss)); var pair = make_lam3(m, n, s, make_app3(ss, mm, nn)); var zero = make_lam2(s, z, zz); var one = make_lam2(s, z, make_app(ss, zz)); var two = make_lam2(s, z, make_app(ss, make_app(ss, zz))); var three = make_lam2(s, z, make_app(ss, make_app(ss, make_app(ss, zz)))); var four = make_lam2(s, z, make_app(ss, make_app(ss, make_app(ss, make_app(ss, zz))))); var five = make_lam2(s, z, make_app(ss, make_app(ss, make_app(ss, make_app(ss, make_app(ss, zz)))))); var iszero = make_lam(m, make_app3(mm, make_lam(s, ff), tt)); var add = make_lam2(m, n, make_app3(mm, succ, nn)); var mul = make_lam3(m, n, s, make_app(mm, make_app(nn, ss))); var pred1 = make_lam3(n, s, z, make_app4(nn, make_lam2(u, v, make_app(vv, make_app(uu, ss))), make_app(kk, zz), id)); var shift = make_lam(s, make_app(ss, make_lam2(m, n, make_app3(pair, make_app(succ, mm), mm)))); var pred2 = make_lam(n, make_app4(nn, shift, make_app3(pair, zero, zero), get2)); function make_sub() { var mzero = make_app(make_app(pair, zero), id); var msucc = make_lam(s, make_app(ss, make_lam(m, make_lam(n, make_app(make_app(pair, make_app(succ, mm)), make_app(kk, ss)))))); var mtail = make_lam(s, make_app(make_app(ss, get2), ss)); return make_lam(m, make_lam(n, make_app(make_app(make_app(nn, mtail), make_app(make_app(mm, msucc), mzero)), get1))); } var sub = make_sub(); var min = make_lam(m, make_lam(n, make_app(make_app(sub, mm), make_app(make_app(sub, mm), nn)))); var max = make_lam(m, make_lam(n, make_app(make_app(add, nn), make_app(make_app(sub, mm), nn)))); function make_lt() { var mzero = make_app(make_app(pair, zero), id); var msucc = make_lam(s, make_app(ss, make_lam(m, make_lam(n, make_app(make_app(pair, make_app(succ, mm)), make_app(kk, ss)))))); var mtail = make_lam(s, make_app(make_app(ss, get2), ss)); return make_lam(n, make_lam(m, make_app(make_app(make_app(make_app(make_app(nn, mtail), make_app(make_app(mm, msucc), mzero)), get1), make_lam(s, tt)), ff))); } var lt = make_lt(); function make_leq() { var mzero = make_app(make_app(pair, zero), id); var msucc = make_lam(s, make_app(ss, make_lam(m, make_lam(n, make_app(make_app(pair, make_app(succ, mm)), make_app(kk, ss)))))); var mtail = make_lam(s, make_app(make_app(ss, get2), ss)); return make_lam(m, make_lam(n, make_app(make_app(make_app(make_app(make_app(nn, mtail), make_app(make_app(mm, msucc), mzero)), get1), make_lam(s, ff)), tt))); } var leq = make_leq(); function make_eq() { var mzero = make_app(make_app(pair, zero), make_app(kk, make_app(make_app(pair, one), id))); var msucc = make_lam(s, make_app(ss, make_lam(m, make_lam(n, make_app(make_app(pair, make_app(succ, mm)), make_app(kk, ss)))))); var mtail = make_lam(s, make_app(make_app(ss, get2), ss)); return make_lam(m, make_lam(n, make_app(make_app(make_app(make_app(make_app(nn, mtail), make_app(make_app(mm, msucc), mzero)), get1), make_lam(s, ff)), tt))); } var eq = make_eq(); function make_divmod() { var triple = make_lam4(m, n, z, s, make_app4(ss, mm, nn, zz)); var mzero = make_app4(triple, succ, make_app(kk, zero), id); var msucc = make_lam(u, make_app4(triple, id, succ, make_app(kk, uu))); // mtail is open in d var mtail = make_lam(s, make_app(ss, make_lam5(m, n, u, v, z, make_lam(s, make_app3(zz, dd, make_app3(ss, make_app(uu, mm), make_app(vv, nn))))))); var res = make_lam2(n, u, make_app3( make_lam(d, make_app3(nn, mtail, make_lam(s, make_app(dd, make_app3(ss, zero, zero))))), make_app4(uu, msucc, mzero, make_lam3(m, n, s, make_app(ss, zz))), make_lam5(m, n, u, v, s, make_app3(pair, mm, nn)) )); return res; } var divmod = make_divmod(); var div = make_lam2(n, m, make_app4(divmod, nn, mm, get1)); var mod = make_lam2(n, m, make_app4(divmod, nn, mm, get2)); var yhalf = make_lam(u, make_app(vv, make_app(uu, uu))); var y = make_lam(v, make_app(yhalf, yhalf)); var yyhalf = make_lam(u, make_app(vv, make_lam(n, make_app3(uu, uu, nn)))) var yy = make_lam(v, make_app(yyhalf, yyhalf)); var turinghalf = make_lam2(u, v, make_app(vv, make_app3(uu, uu, vv))); var turing = make_app(turinghalf, turinghalf); var tturinghalf = make_lam2(u, v, make_app(vv, make_lam(m, make_app4(uu, uu, vv, mm)))); var tturing = make_app(tturinghalf, tturinghalf); var ifzero = make_lam(n, make_app4(nn, make_lam2(u, v, make_app(vv, make_app(uu, succ))), make_app(kk, zero), make_lam3(m, s, z, make_app(ss, mm) ))); var fact1 = make_app(ww, make_lam2(u, n, make_app4(ifzero, nn, make_lam(s, make_app3(mul, nn, make_app3(uu, uu, ss))), one))); function make_fact(y) { return make_app(y, make_lam2(u, n, make_app4(ifzero, nn, make_lam(s, make_app3(mul, nn, make_app(uu, ss))), one))); } var fact2 = make_fact(y); var fact3 = make_fact(yy); var fact4 = make_fact(turing); var fact5 = make_fact(tturing); function check(expect, formula) { var i = to_int(formula); print(expect, expect === i); } function checkbool(expect, index, formula) { if (expect) { print(index, equal(reduce(formula, g_eta, g_cbv), tt)); } else { print(index, equal(reduce(formula, g_eta, g_cbv), ff)); } } check(0, zero); check(1, one); check(2, two); check(3, three); check(4, four); check(5, five); check(1, make_app(succ, zero)); check(2, make_app(succ, make_app(succ, zero))); check(3, make_app(succ, make_app(succ, make_app(succ, zero)))); check(4, make_app(succ, make_app(succ, make_app(succ, make_app(succ, zero))))); check(5, make_app(succ, make_app(succ, make_app(succ, make_app(succ, make_app(succ, zero)))))); check(2, make_app(succ, one)); check(3, make_app(succ, make_app(succ, one))); check(4, make_app(succ, make_app(succ, make_app(succ, one)))); check(5, make_app(succ, make_app(succ, make_app(succ, make_app(succ, one))))); check(3, make_app(succ, two)); check(4, make_app(succ, make_app(succ, two))); check(5, make_app(succ, make_app(succ, make_app(succ, two)))); print("checking iszero"); checkbool(true, 0, make_app(iszero, zero)); checkbool(true, 1, make_app(iszero, one)); checkbool(true, 2, make_app(iszero, two)); checkbool(true, 3, make_app(iszero, three)); checkbool(true, 4, make_app(iszero, four)); checkbool(true, 5, make_app(iszero, five)); print("checking add"); check(0, make_app(make_app(add, zero), zero)); check(1, make_app(make_app(add, zero), one)); check(2, make_app(make_app(add, zero), two)); check(3, make_app(make_app(add, zero), three)); check(4, make_app(make_app(add, zero), four)); check(5, make_app(make_app(add, zero), five)); check(1, make_app(make_app(add, one), zero)); check(2, make_app(make_app(add, one), one)); check(3, make_app(make_app(add, one), two)); check(4, make_app(make_app(add, one), three)); check(5, make_app(make_app(add, one), four)); check(6, make_app(make_app(add, one), five)); check(2, make_app(make_app(add, two), zero)); check(3, make_app(make_app(add, two), one)); check(4, make_app(make_app(add, two), two)); check(5, make_app(make_app(add, two), three)); check(6, make_app(make_app(add, two), four)); check(7, make_app(make_app(add, two), five)); check(3, make_app(make_app(add, three), zero)); check(4, make_app(make_app(add, three), one)); check(5, make_app(make_app(add, three), two)); check(6, make_app(make_app(add, three), three)); check(7, make_app(make_app(add, three), four)); check(8, make_app(make_app(add, three), five)); check(4, make_app(make_app(add, four), zero)); check(5, make_app(make_app(add, four), one)); check(6, make_app(make_app(add, four), two)); check(7, make_app(make_app(add, four), three)); check(8, make_app(make_app(add, four), four)); check(9, make_app(make_app(add, four), five)); print("checking mul"); check(0, make_app(make_app(mul, zero), zero)); check(0, make_app(make_app(mul, zero), one)); check(0, make_app(make_app(mul, zero), two)); check(0, make_app(make_app(mul, zero), three)); check(0, make_app(make_app(mul, zero), four)); check(0, make_app(make_app(mul, zero), five)); check(0, make_app(make_app(mul, one), zero)); check(1, make_app(make_app(mul, one), one)); check(2, make_app(make_app(mul, one), two)); check(3, make_app(make_app(mul, one), three)); check(4, make_app(make_app(mul, one), four)); check(5, make_app(make_app(mul, one), five)); check(0, make_app(make_app(mul, two), zero)); check(2, make_app(make_app(mul, two), one)); check(4, make_app(make_app(mul, two), two)); check(6, make_app(make_app(mul, two), three)); check(8, make_app(make_app(mul, two), four)); check(10, make_app(make_app(mul, two), five)); check(0, make_app(make_app(mul, three), zero)); check(3, make_app(make_app(mul, three), one)); check(6, make_app(make_app(mul, three), two)); check(9, make_app(make_app(mul, three), three)); check(12, make_app(make_app(mul, three), four)); check(15, make_app(make_app(mul, three), five)); check(0, make_app(make_app(mul, four), zero)); check(4, make_app(make_app(mul, four), one)); check(8, make_app(make_app(mul, four), two)); check(12, make_app(make_app(mul, four), three)); check(16, make_app(make_app(mul, four), four)); check(20, make_app(make_app(mul, four), five)); function check_pred(pred) { check(0, make_app(pred, zero)); check(0, make_app(pred, make_app(pred, zero))); check(0, make_app(pred, make_app(pred, make_app(pred, zero)))); check(0, make_app(pred, make_app(pred, make_app(pred, make_app(pred, zero))))); check(0, make_app(pred, make_app(pred, make_app(pred, make_app(pred, make_app(pred, zero)))))); check(0, make_app(pred, one)); check(0, make_app(pred, make_app(pred, one))); check(0, make_app(pred, make_app(pred, make_app(pred, one)))); check(0, make_app(pred, make_app(pred, make_app(pred, make_app(pred, one))))); check(0, make_app(pred, make_app(pred, make_app(pred, make_app(pred, make_app(pred, one)))))); check(1, make_app(pred, two)); check(0, make_app(pred, make_app(pred, two))); check(0, make_app(pred, make_app(pred, make_app(pred, two)))); check(0, make_app(pred, make_app(pred, make_app(pred, make_app(pred, two))))); check(0, make_app(pred, make_app(pred, make_app(pred, make_app(pred, make_app(pred, two)))))); check(2, make_app(pred, three)); check(1, make_app(pred, make_app(pred, three))); check(0, make_app(pred, make_app(pred, make_app(pred, three)))); check(0, make_app(pred, make_app(pred, make_app(pred, make_app(pred, three))))); check(0, make_app(pred, make_app(pred, make_app(pred, make_app(pred, make_app(pred, three)))))); check(3, make_app(pred, four)); check(2, make_app(pred, make_app(pred, four))); check(1, make_app(pred, make_app(pred, make_app(pred, four)))); check(0, make_app(pred, make_app(pred, make_app(pred, make_app(pred, four))))); check(0, make_app(pred, make_app(pred, make_app(pred, make_app(pred, make_app(pred, four)))))); check(4, make_app(pred, five)); check(3, make_app(pred, make_app(pred, five))); check(2, make_app(pred, make_app(pred, make_app(pred, five)))); check(1, make_app(pred, make_app(pred, make_app(pred, make_app(pred, five))))); check(0, make_app(pred, make_app(pred, make_app(pred, make_app(pred, make_app(pred, five)))))); } print("checking pred1"); check_pred(pred1); print("checking pred2"); check_pred(pred2); print("checking sub"); check(0, make_app(make_app(sub, zero), zero)); check(0, make_app(make_app(sub, zero), one)); check(0, make_app(make_app(sub, zero), two)); check(0, make_app(make_app(sub, zero), three)); check(0, make_app(make_app(sub, zero), four)); check(0, make_app(make_app(sub, zero), five)); check(1, make_app(make_app(sub, one), zero)); check(0, make_app(make_app(sub, one), one)); check(0, make_app(make_app(sub, one), two)); check(0, make_app(make_app(sub, one), three)); check(0, make_app(make_app(sub, one), four)); check(0, make_app(make_app(sub, one), five)); check(2, make_app(make_app(sub, two), zero)); check(1, make_app(make_app(sub, two), one)); check(0, make_app(make_app(sub, two), two)); check(0, make_app(make_app(sub, two), three)); check(0, make_app(make_app(sub, two), four)); check(0, make_app(make_app(sub, two), five)); check(3, make_app(make_app(sub, three), zero)); check(2, make_app(make_app(sub, three), one)); check(1, make_app(make_app(sub, three), two)); check(0, make_app(make_app(sub, three), three)); check(0, make_app(make_app(sub, three), four)); check(0, make_app(make_app(sub, three), five)); check(4, make_app(make_app(sub, four), zero)); check(3, make_app(make_app(sub, four), one)); check(2, make_app(make_app(sub, four), two)); check(1, make_app(make_app(sub, four), three)); check(0, make_app(make_app(sub, four), four)); check(0, make_app(make_app(sub, four), five)); check(5, make_app(make_app(sub, five), zero)); check(4, make_app(make_app(sub, five), one)); check(3, make_app(make_app(sub, five), two)); check(2, make_app(make_app(sub, five), three)); check(1, make_app(make_app(sub, five), four)); check(0, make_app(make_app(sub, five), five)); print("checking min"); check(0, make_app(make_app(min, zero), zero)); check(0, make_app(make_app(min, zero), one)); check(0, make_app(make_app(min, zero), two)); check(0, make_app(make_app(min, zero), three)); check(0, make_app(make_app(min, zero), four)); check(0, make_app(make_app(min, zero), five)); check(0, make_app(make_app(min, one), zero)); check(1, make_app(make_app(min, one), one)); check(1, make_app(make_app(min, one), two)); check(1, make_app(make_app(min, one), three)); check(1, make_app(make_app(min, one), four)); check(1, make_app(make_app(min, one), five)); check(0, make_app(make_app(min, two), zero)); check(1, make_app(make_app(min, two), one)); check(2, make_app(make_app(min, two), two)); check(2, make_app(make_app(min, two), three)); check(2, make_app(make_app(min, two), four)); check(2, make_app(make_app(min, two), five)); check(0, make_app(make_app(min, three), zero)); check(1, make_app(make_app(min, three), one)); check(2, make_app(make_app(min, three), two)); check(3, make_app(make_app(min, three), three)); check(3, make_app(make_app(min, three), four)); check(3, make_app(make_app(min, three), five)); check(0, make_app(make_app(min, four), zero)); check(1, make_app(make_app(min, four), one)); check(2, make_app(make_app(min, four), two)); check(3, make_app(make_app(min, four), three)); check(4, make_app(make_app(min, four), four)); check(4, make_app(make_app(min, four), five)); check(0, make_app(make_app(min, five), zero)); check(1, make_app(make_app(min, five), one)); check(2, make_app(make_app(min, five), two)); check(3, make_app(make_app(min, five), three)); check(4, make_app(make_app(min, five), four)); check(5, make_app(make_app(min, five), five)); print("checking max"); check(0, make_app(make_app(max, zero), zero)); check(1, make_app(make_app(max, zero), one)); check(2, make_app(make_app(max, zero), two)); check(3, make_app(make_app(max, zero), three)); check(4, make_app(make_app(max, zero), four)); check(5, make_app(make_app(max, zero), five)); check(1, make_app(make_app(max, one), zero)); check(1, make_app(make_app(max, one), one)); check(2, make_app(make_app(max, one), two)); check(3, make_app(make_app(max, one), three)); check(4, make_app(make_app(max, one), four)); check(5, make_app(make_app(max, one), five)); check(2, make_app(make_app(max, two), zero)); check(2, make_app(make_app(max, two), one)); check(2, make_app(make_app(max, two), two)); check(3, make_app(make_app(max, two), three)); check(4, make_app(make_app(max, two), four)); check(5, make_app(make_app(max, two), five)); check(3, make_app(make_app(max, three), zero)); check(3, make_app(make_app(max, three), one)); check(3, make_app(make_app(max, three), two)); check(3, make_app(make_app(max, three), three)); check(4, make_app(make_app(max, three), four)); check(5, make_app(make_app(max, three), five)); check(4, make_app(make_app(max, four), zero)); check(4, make_app(make_app(max, four), one)); check(4, make_app(make_app(max, four), two)); check(4, make_app(make_app(max, four), three)); check(4, make_app(make_app(max, four), four)); check(5, make_app(make_app(max, four), five)); check(5, make_app(make_app(max, five), zero)); check(5, make_app(make_app(max, five), one)); check(5, make_app(make_app(max, five), two)); check(5, make_app(make_app(max, five), three)); check(5, make_app(make_app(max, five), four)); check(5, make_app(make_app(max, five), five)); print("checking lt"); checkbool(false, 0, make_app(make_app(lt, zero), zero)); checkbool(true, 0, make_app(make_app(lt, zero), one)); checkbool(true, 0, make_app(make_app(lt, zero), two)); checkbool(true, 0, make_app(make_app(lt, zero), three)); checkbool(true, 0, make_app(make_app(lt, zero), four)); checkbool(true, 0, make_app(make_app(lt, zero), five)); checkbool(false, 1, make_app(make_app(lt, one), zero)); checkbool(false, 1, make_app(make_app(lt, one), one)); checkbool(true, 1, make_app(make_app(lt, one), two)); checkbool(true, 1, make_app(make_app(lt, one), three)); checkbool(true, 1, make_app(make_app(lt, one), four)); checkbool(true, 1, make_app(make_app(lt, one), five)); checkbool(false, 2, make_app(make_app(lt, two), zero)); checkbool(false, 2, make_app(make_app(lt, two), one)); checkbool(false, 2, make_app(make_app(lt, two), two)); checkbool(true, 2, make_app(make_app(lt, two), three)); checkbool(true, 2, make_app(make_app(lt, two), four)); checkbool(true, 2, make_app(make_app(lt, two), five)); checkbool(false, 3, make_app(make_app(lt, three), zero)); checkbool(false, 3, make_app(make_app(lt, three), one)); checkbool(false, 3, make_app(make_app(lt, three), two)); checkbool(false, 3, make_app(make_app(lt, three), three)); checkbool(true, 3, make_app(make_app(lt, three), four)); checkbool(true, 3, make_app(make_app(lt, three), five)); checkbool(false, 4, make_app(make_app(lt, four), zero)); checkbool(false, 4, make_app(make_app(lt, four), one)); checkbool(false, 4, make_app(make_app(lt, four), two)); checkbool(false, 4, make_app(make_app(lt, four), three)); checkbool(false, 4, make_app(make_app(lt, four), four)); checkbool(true, 4, make_app(make_app(lt, four), five)); checkbool(false, 5, make_app(make_app(lt, five), zero)); checkbool(false, 5, make_app(make_app(lt, five), one)); checkbool(false, 5, make_app(make_app(lt, five), two)); checkbool(false, 5, make_app(make_app(lt, five), three)); checkbool(false, 5, make_app(make_app(lt, five), four)); checkbool(false, 5, make_app(make_app(lt, five), five)); print("checking leq"); checkbool(true, 0, make_app(make_app(leq, zero), zero)); checkbool(true, 0, make_app(make_app(leq, zero), one)); checkbool(true, 0, make_app(make_app(leq, zero), two)); checkbool(true, 0, make_app(make_app(leq, zero), three)); checkbool(true, 0, make_app(make_app(leq, zero), four)); checkbool(true, 0, make_app(make_app(leq, zero), five)); checkbool(false, 1, make_app(make_app(leq, one), zero)); checkbool(true, 1, make_app(make_app(leq, one), one)); checkbool(true, 1, make_app(make_app(leq, one), two)); checkbool(true, 1, make_app(make_app(leq, one), three)); checkbool(true, 1, make_app(make_app(leq, one), four)); checkbool(true, 1, make_app(make_app(leq, one), five)); checkbool(false, 2, make_app(make_app(leq, two), zero)); checkbool(false, 2, make_app(make_app(leq, two), one)); checkbool(true, 2, make_app(make_app(leq, two), two)); checkbool(true, 2, make_app(make_app(leq, two), three)); checkbool(true, 2, make_app(make_app(leq, two), four)); checkbool(true, 2, make_app(make_app(leq, two), five)); checkbool(false, 3, make_app(make_app(leq, three), zero)); checkbool(false, 3, make_app(make_app(leq, three), one)); checkbool(false, 3, make_app(make_app(leq, three), two)); checkbool(true, 3, make_app(make_app(leq, three), three)); checkbool(true, 3, make_app(make_app(leq, three), four)); checkbool(true, 3, make_app(make_app(leq, three), five)); checkbool(false, 4, make_app(make_app(leq, four), zero)); checkbool(false, 4, make_app(make_app(leq, four), one)); checkbool(false, 4, make_app(make_app(leq, four), two)); checkbool(false, 4, make_app(make_app(leq, four), three)); checkbool(true, 4, make_app(make_app(leq, four), four)); checkbool(true, 4, make_app(make_app(leq, four), five)); checkbool(false, 5, make_app(make_app(leq, five), zero)); checkbool(false, 5, make_app(make_app(leq, five), one)); checkbool(false, 5, make_app(make_app(leq, five), two)); checkbool(false, 5, make_app(make_app(leq, five), three)); checkbool(false, 5, make_app(make_app(leq, five), four)); checkbool(true, 5, make_app(make_app(leq, five), five)); print("checking eq"); checkbool(true, 0, make_app(make_app(eq, zero), zero)); checkbool(false, 0, make_app(make_app(eq, zero), one)); checkbool(false, 0, make_app(make_app(eq, zero), two)); checkbool(false, 0, make_app(make_app(eq, zero), three)); checkbool(false, 0, make_app(make_app(eq, zero), four)); checkbool(false, 0, make_app(make_app(eq, zero), five)); checkbool(false, 1, make_app(make_app(eq, one), zero)); checkbool(true, 1, make_app(make_app(eq, one), one)); checkbool(false, 1, make_app(make_app(eq, one), two)); checkbool(false, 1, make_app(make_app(eq, one), three)); checkbool(false, 1, make_app(make_app(eq, one), four)); checkbool(false, 1, make_app(make_app(eq, one), five)); checkbool(false, 2, make_app(make_app(eq, two), zero)); checkbool(false, 2, make_app(make_app(eq, two), one)); checkbool(true, 2, make_app(make_app(eq, two), two)); checkbool(false, 2, make_app(make_app(eq, two), three)); checkbool(false, 2, make_app(make_app(eq, two), four)); checkbool(false, 2, make_app(make_app(eq, two), five)); checkbool(false, 3, make_app(make_app(eq, three), zero)); checkbool(false, 3, make_app(make_app(eq, three), one)); checkbool(false, 3, make_app(make_app(eq, three), two)); checkbool(true, 3, make_app(make_app(eq, three), three)); checkbool(false, 3, make_app(make_app(eq, three), four)); checkbool(false, 3, make_app(make_app(eq, three), five)); checkbool(false, 4, make_app(make_app(eq, four), zero)); checkbool(false, 4, make_app(make_app(eq, four), one)); checkbool(false, 4, make_app(make_app(eq, four), two)); checkbool(false, 4, make_app(make_app(eq, four), three)); checkbool(true, 4, make_app(make_app(eq, four), four)); checkbool(false, 4, make_app(make_app(eq, four), five)); checkbool(false, 5, make_app(make_app(eq, five), zero)); checkbool(false, 5, make_app(make_app(eq, five), one)); checkbool(false, 5, make_app(make_app(eq, five), two)); checkbool(false, 5, make_app(make_app(eq, five), three)); checkbool(false, 5, make_app(make_app(eq, five), four)); checkbool(true, 5, make_app(make_app(eq, five), five)); print("checking div"); check(0, make_app(make_app(div, zero), one)); check(0, make_app(make_app(div, zero), two)); check(0, make_app(make_app(div, zero), three)); check(0, make_app(make_app(div, zero), four)); check(0, make_app(make_app(div, zero), five)); check(1, make_app(make_app(div, one), one)); check(0, make_app(make_app(div, one), two)); check(0, make_app(make_app(div, one), three)); check(0, make_app(make_app(div, one), four)); check(0, make_app(make_app(div, one), five)); check(2, make_app(make_app(div, two), one)); check(1, make_app(make_app(div, two), two)); check(0, make_app(make_app(div, two), three)); check(0, make_app(make_app(div, two), four)); check(0, make_app(make_app(div, two), five)); check(3, make_app(make_app(div, three), one)); check(1, make_app(make_app(div, three), two)); check(1, make_app(make_app(div, three), three)); check(0, make_app(make_app(div, three), four)); check(0, make_app(make_app(div, three), five)); check(4, make_app(make_app(div, four), one)); check(2, make_app(make_app(div, four), two)); check(1, make_app(make_app(div, four), three)); check(1, make_app(make_app(div, four), four)); check(0, make_app(make_app(div, four), five)); check(5, make_app(make_app(div, five), one)); check(2, make_app(make_app(div, five), two)); check(1, make_app(make_app(div, five), three)); check(1, make_app(make_app(div, five), four)); check(1, make_app(make_app(div, five), five)); print("checking mod"); check(0, make_app(make_app(mod, zero), one)); check(0, make_app(make_app(mod, zero), two)); check(0, make_app(make_app(mod, zero), three)); check(0, make_app(make_app(mod, zero), four)); check(0, make_app(make_app(mod, zero), five)); check(0, make_app(make_app(mod, one), one)); check(1, make_app(make_app(mod, one), two)); check(1, make_app(make_app(mod, one), three)); check(1, make_app(make_app(mod, one), four)); check(1, make_app(make_app(mod, one), five)); check(0, make_app(make_app(mod, two), one)); check(0, make_app(make_app(mod, two), two)); check(2, make_app(make_app(mod, two), three)); check(2, make_app(make_app(mod, two), four)); check(2, make_app(make_app(mod, two), five)); check(0, make_app(make_app(mod, three), one)); check(1, make_app(make_app(mod, three), two)); check(0, make_app(make_app(mod, three), three)); check(3, make_app(make_app(mod, three), four)); check(3, make_app(make_app(mod, three), five)); check(0, make_app(make_app(mod, four), one)); check(0, make_app(make_app(mod, four), two)); check(1, make_app(make_app(mod, four), three)); check(0, make_app(make_app(mod, four), four)); check(4, make_app(make_app(mod, four), five)); check(0, make_app(make_app(mod, five), one)); check(1, make_app(make_app(mod, five), two)); check(2, make_app(make_app(mod, five), three)); check(1, make_app(make_app(mod, five), four)); check(0, make_app(make_app(mod, five), five)); if (!g_cbv) { print("checking fact1"); check(1, make_app(fact1, zero)); check(1, make_app(fact1, one)); check(2, make_app(fact1, two)); check(6, make_app(fact1, three)); check(24, make_app(fact1, four)); } if (!g_cbv) { print("checking fact2"); check(1, make_app(fact2, zero)); check(1, make_app(fact2, one)); check(2, make_app(fact2, two)); check(6, make_app(fact2, three)); check(24, make_app(fact2, four)); } if (g_cbv<2) { print("checking fact3"); check(1, make_app(fact3, zero)); check(1, make_app(fact3, one)); check(2, make_app(fact3, two)); check(6, make_app(fact3, three)); check(24, make_app(fact3, four)); } if (!g_cbv) { print("checking fact4"); check(1, make_app(fact4, zero)); check(1, make_app(fact4, one)); check(2, make_app(fact4, two)); check(6, make_app(fact4, three)); check(24, make_app(fact4, four)); } if (g_cbv<2) { print("checking fact5"); check(1, make_app(fact5, zero)); check(1, make_app(fact5, one)); check(2, make_app(fact5, two)); check(6, make_app(fact5, three)); check(24, make_app(fact5, four)); } } test();