7 function to_int(expr) {
8 var reduced = reduce(expr, g_eta, g_cbv);
10 return reduce(reduced, false, false).to_int(0);
12 return "not a church numeral";
16 function to_string(expr) {
17 var reduced = reduce(expr, g_eta, g_cbv);
18 return reduced.to_string();
24 function make_lam2(a, b, aa) {
25 return make_lam(a, make_lam(b, aa));
27 function make_lam3(a, b, c, aa) {
28 return make_lam(a, make_lam(b, make_lam(c, aa)));
30 function make_lam4(a, b, c, d, aa) {
31 return make_lam(a, make_lam(b, make_lam(c, make_lam(d, aa))));
33 function make_lam5(a, b, c, d, e, aa) {
34 return make_lam(a, make_lam(b, make_lam(c, make_lam(d, make_lam(e, aa)))));
36 function make_app3(aa, bb, cc) {
37 return make_app(make_app(aa, bb), cc);
39 function make_app4(aa, bb, cc, dd) {
40 return make_app(make_app(make_app(aa, bb), cc), dd);
42 function make_app5(aa, bb, cc, dd, ee) {
43 return make_app(make_app(make_app(make_app(aa, bb), cc), dd), ee);
46 var s = make_var("s");
47 var z = make_var("z");
48 var m = make_var("m");
49 var n = make_var("n");
50 var u = make_var("u");
51 var v = make_var("v");
52 var d = make_var("d");
53 var ss = new Lambda_var(s);
54 var zz = new Lambda_var(z);
55 var mm = new Lambda_var(m);
56 var nn = new Lambda_var(n);
57 var uu = new Lambda_var(u);
58 var vv = new Lambda_var(v);
59 var dd = new Lambda_var(d);
60 var succ = make_lam3(m, s, z, make_app(ss, make_app3(mm, ss, zz)));
61 var tt = make_lam2(m, n, mm);
62 var ff = make_lam2(m, n, nn);
66 var id = make_lam(s, ss);
67 var ww = make_lam(s, make_app(ss, ss));
68 var pair = make_lam3(m, n, s, make_app3(ss, mm, nn));
69 var zero = make_lam2(s, z, zz);
70 var one = make_lam2(s, z, make_app(ss, zz));
71 var two = make_lam2(s, z, make_app(ss, make_app(ss, zz)));
72 var three = make_lam2(s, z, make_app(ss, make_app(ss, make_app(ss, zz))));
73 var four = make_lam2(s, z, make_app(ss, make_app(ss, make_app(ss, make_app(ss, zz)))));
74 var five = make_lam2(s, z, make_app(ss, make_app(ss, make_app(ss, make_app(ss, make_app(ss, zz))))));
75 var iszero = make_lam(m, make_app3(mm, make_lam(s, ff), tt));
76 var add = make_lam2(m, n, make_app3(mm, succ, nn));
77 var mul = make_lam3(m, n, s, make_app(mm, make_app(nn, ss)));
78 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));
80 var shift = make_lam(s, make_app(ss, make_lam2(m, n, make_app3(pair, make_app(succ, mm), mm))));
81 var pred2 = make_lam(n, make_app4(nn, shift, make_app3(pair, zero, zero), get2));
85 var mzero = make_app(make_app(pair, zero), id);
86 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))))));
87 var mtail = make_lam(s, make_app(make_app(ss, get2), ss));
88 return make_lam(m, make_lam(n, make_app(make_app(make_app(nn, mtail), make_app(make_app(mm, msucc), mzero)), get1)));
92 var min = make_lam(m, make_lam(n, make_app(make_app(sub, mm), make_app(make_app(sub, mm), nn))));
93 var max = make_lam(m, make_lam(n, make_app(make_app(add, nn), make_app(make_app(sub, mm), nn))));
96 var mzero = make_app(make_app(pair, zero), id);
97 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))))));
98 var mtail = make_lam(s, make_app(make_app(ss, get2), ss));
99 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)));
103 function make_leq() {
104 var mzero = make_app(make_app(pair, zero), id);
105 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))))));
106 var mtail = make_lam(s, make_app(make_app(ss, get2), ss));
107 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)));
109 var leq = make_leq();
112 var mzero = make_app(make_app(pair, zero), make_app(kk, make_app(make_app(pair, one), id)));
113 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))))));
114 var mtail = make_lam(s, make_app(make_app(ss, get2), ss));
115 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)));
119 function make_divmod() {
120 var triple = make_lam4(m, n, z, s, make_app4(ss, mm, nn, zz));
121 var mzero = make_app4(triple, succ, make_app(kk, zero), id);
122 var msucc = make_lam(u, make_app4(triple, id, succ, make_app(kk, uu)));
123 // mtail is open in d
124 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)))))));
125 var res = make_lam2(n, u, make_app3(
126 make_lam(d, make_app3(nn, mtail, make_lam(s, make_app(dd, make_app3(ss, zero, zero))))),
127 make_app4(uu, msucc, mzero, make_lam3(m, n, s, make_app(ss, zz))),
128 make_lam5(m, n, u, v, s, make_app3(pair, mm, nn))
132 var divmod = make_divmod();
133 var div = make_lam2(n, m, make_app4(divmod, nn, mm, get1));
134 var mod = make_lam2(n, m, make_app4(divmod, nn, mm, get2));
136 var yhalf = make_lam(u, make_app(vv, make_app(uu, uu)));
137 var y = make_lam(v, make_app(yhalf, yhalf));
138 var yyhalf = make_lam(u, make_app(vv, make_lam(n, make_app3(uu, uu, nn))))
139 var yy = make_lam(v, make_app(yyhalf, yyhalf));
141 var turinghalf = make_lam2(u, v, make_app(vv, make_app3(uu, uu, vv)));
142 var turing = make_app(turinghalf, turinghalf);
143 var tturinghalf = make_lam2(u, v, make_app(vv, make_lam(m, make_app4(uu, uu, vv, mm))));
144 var tturing = make_app(tturinghalf, tturinghalf);
146 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) )));
148 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)));
149 function make_fact(y) {
150 return make_app(y, make_lam2(u, n, make_app4(ifzero, nn, make_lam(s, make_app3(mul, nn, make_app(uu, ss))), one)));
152 var fact2 = make_fact(y);
153 var fact3 = make_fact(yy);
154 var fact4 = make_fact(turing);
155 var fact5 = make_fact(tturing);
157 function check(expect, formula) {
158 var i = to_int(formula);
159 print(expect, expect === i);
162 function checkbool(expect, index, formula) {
164 print(index, equal(reduce(formula, g_eta, g_cbv), tt));
166 print(index, equal(reduce(formula, g_eta, g_cbv), ff));
177 check(1, make_app(succ, zero));
178 check(2, make_app(succ, make_app(succ, zero)));
179 check(3, make_app(succ, make_app(succ, make_app(succ, zero))));
180 check(4, make_app(succ, make_app(succ, make_app(succ, make_app(succ, zero)))));
181 check(5, make_app(succ, make_app(succ, make_app(succ, make_app(succ, make_app(succ, zero))))));
184 check(2, make_app(succ, one));
185 check(3, make_app(succ, make_app(succ, one)));
186 check(4, make_app(succ, make_app(succ, make_app(succ, one))));
187 check(5, make_app(succ, make_app(succ, make_app(succ, make_app(succ, one)))));
189 check(3, make_app(succ, two));
190 check(4, make_app(succ, make_app(succ, two)));
191 check(5, make_app(succ, make_app(succ, make_app(succ, two))));
193 print("checking iszero");
194 checkbool(true, 0, make_app(iszero, zero));
195 checkbool(true, 1, make_app(iszero, one));
196 checkbool(true, 2, make_app(iszero, two));
197 checkbool(true, 3, make_app(iszero, three));
198 checkbool(true, 4, make_app(iszero, four));
199 checkbool(true, 5, make_app(iszero, five));
201 print("checking add");
202 check(0, make_app(make_app(add, zero), zero));
203 check(1, make_app(make_app(add, zero), one));
204 check(2, make_app(make_app(add, zero), two));
205 check(3, make_app(make_app(add, zero), three));
206 check(4, make_app(make_app(add, zero), four));
207 check(5, make_app(make_app(add, zero), five));
208 check(1, make_app(make_app(add, one), zero));
209 check(2, make_app(make_app(add, one), one));
210 check(3, make_app(make_app(add, one), two));
211 check(4, make_app(make_app(add, one), three));
212 check(5, make_app(make_app(add, one), four));
213 check(6, make_app(make_app(add, one), five));
214 check(2, make_app(make_app(add, two), zero));
215 check(3, make_app(make_app(add, two), one));
216 check(4, make_app(make_app(add, two), two));
217 check(5, make_app(make_app(add, two), three));
218 check(6, make_app(make_app(add, two), four));
219 check(7, make_app(make_app(add, two), five));
220 check(3, make_app(make_app(add, three), zero));
221 check(4, make_app(make_app(add, three), one));
222 check(5, make_app(make_app(add, three), two));
223 check(6, make_app(make_app(add, three), three));
224 check(7, make_app(make_app(add, three), four));
225 check(8, make_app(make_app(add, three), five));
226 check(4, make_app(make_app(add, four), zero));
227 check(5, make_app(make_app(add, four), one));
228 check(6, make_app(make_app(add, four), two));
229 check(7, make_app(make_app(add, four), three));
230 check(8, make_app(make_app(add, four), four));
231 check(9, make_app(make_app(add, four), five));
233 print("checking mul");
234 check(0, make_app(make_app(mul, zero), zero));
235 check(0, make_app(make_app(mul, zero), one));
236 check(0, make_app(make_app(mul, zero), two));
237 check(0, make_app(make_app(mul, zero), three));
238 check(0, make_app(make_app(mul, zero), four));
239 check(0, make_app(make_app(mul, zero), five));
240 check(0, make_app(make_app(mul, one), zero));
241 check(1, make_app(make_app(mul, one), one));
242 check(2, make_app(make_app(mul, one), two));
243 check(3, make_app(make_app(mul, one), three));
244 check(4, make_app(make_app(mul, one), four));
245 check(5, make_app(make_app(mul, one), five));
246 check(0, make_app(make_app(mul, two), zero));
247 check(2, make_app(make_app(mul, two), one));
248 check(4, make_app(make_app(mul, two), two));
249 check(6, make_app(make_app(mul, two), three));
250 check(8, make_app(make_app(mul, two), four));
251 check(10, make_app(make_app(mul, two), five));
252 check(0, make_app(make_app(mul, three), zero));
253 check(3, make_app(make_app(mul, three), one));
254 check(6, make_app(make_app(mul, three), two));
255 check(9, make_app(make_app(mul, three), three));
256 check(12, make_app(make_app(mul, three), four));
257 check(15, make_app(make_app(mul, three), five));
258 check(0, make_app(make_app(mul, four), zero));
259 check(4, make_app(make_app(mul, four), one));
260 check(8, make_app(make_app(mul, four), two));
261 check(12, make_app(make_app(mul, four), three));
262 check(16, make_app(make_app(mul, four), four));
263 check(20, make_app(make_app(mul, four), five));
266 function check_pred(pred) {
267 check(0, make_app(pred, zero));
268 check(0, make_app(pred, make_app(pred, zero)));
269 check(0, make_app(pred, make_app(pred, make_app(pred, zero))));
270 check(0, make_app(pred, make_app(pred, make_app(pred, make_app(pred, zero)))));
271 check(0, make_app(pred, make_app(pred, make_app(pred, make_app(pred, make_app(pred, zero))))));
273 check(0, make_app(pred, one));
274 check(0, make_app(pred, make_app(pred, one)));
275 check(0, make_app(pred, make_app(pred, make_app(pred, one))));
276 check(0, make_app(pred, make_app(pred, make_app(pred, make_app(pred, one)))));
277 check(0, make_app(pred, make_app(pred, make_app(pred, make_app(pred, make_app(pred, one))))));
279 check(1, make_app(pred, two));
280 check(0, make_app(pred, make_app(pred, two)));
281 check(0, make_app(pred, make_app(pred, make_app(pred, two))));
282 check(0, make_app(pred, make_app(pred, make_app(pred, make_app(pred, two)))));
283 check(0, make_app(pred, make_app(pred, make_app(pred, make_app(pred, make_app(pred, two))))));
285 check(2, make_app(pred, three));
286 check(1, make_app(pred, make_app(pred, three)));
287 check(0, make_app(pred, make_app(pred, make_app(pred, three))));
288 check(0, make_app(pred, make_app(pred, make_app(pred, make_app(pred, three)))));
289 check(0, make_app(pred, make_app(pred, make_app(pred, make_app(pred, make_app(pred, three))))));
291 check(3, make_app(pred, four));
292 check(2, make_app(pred, make_app(pred, four)));
293 check(1, make_app(pred, make_app(pred, make_app(pred, four))));
294 check(0, make_app(pred, make_app(pred, make_app(pred, make_app(pred, four)))));
295 check(0, make_app(pred, make_app(pred, make_app(pred, make_app(pred, make_app(pred, four))))));
297 check(4, make_app(pred, five));
298 check(3, make_app(pred, make_app(pred, five)));
299 check(2, make_app(pred, make_app(pred, make_app(pred, five))));
300 check(1, make_app(pred, make_app(pred, make_app(pred, make_app(pred, five)))));
301 check(0, make_app(pred, make_app(pred, make_app(pred, make_app(pred, make_app(pred, five))))));
304 print("checking pred1");
307 print("checking pred2");
310 print("checking sub");
311 check(0, make_app(make_app(sub, zero), zero));
312 check(0, make_app(make_app(sub, zero), one));
313 check(0, make_app(make_app(sub, zero), two));
314 check(0, make_app(make_app(sub, zero), three));
315 check(0, make_app(make_app(sub, zero), four));
316 check(0, make_app(make_app(sub, zero), five));
317 check(1, make_app(make_app(sub, one), zero));
318 check(0, make_app(make_app(sub, one), one));
319 check(0, make_app(make_app(sub, one), two));
320 check(0, make_app(make_app(sub, one), three));
321 check(0, make_app(make_app(sub, one), four));
322 check(0, make_app(make_app(sub, one), five));
323 check(2, make_app(make_app(sub, two), zero));
324 check(1, make_app(make_app(sub, two), one));
325 check(0, make_app(make_app(sub, two), two));
326 check(0, make_app(make_app(sub, two), three));
327 check(0, make_app(make_app(sub, two), four));
328 check(0, make_app(make_app(sub, two), five));
329 check(3, make_app(make_app(sub, three), zero));
330 check(2, make_app(make_app(sub, three), one));
331 check(1, make_app(make_app(sub, three), two));
332 check(0, make_app(make_app(sub, three), three));
333 check(0, make_app(make_app(sub, three), four));
334 check(0, make_app(make_app(sub, three), five));
335 check(4, make_app(make_app(sub, four), zero));
336 check(3, make_app(make_app(sub, four), one));
337 check(2, make_app(make_app(sub, four), two));
338 check(1, make_app(make_app(sub, four), three));
339 check(0, make_app(make_app(sub, four), four));
340 check(0, make_app(make_app(sub, four), five));
341 check(5, make_app(make_app(sub, five), zero));
342 check(4, make_app(make_app(sub, five), one));
343 check(3, make_app(make_app(sub, five), two));
344 check(2, make_app(make_app(sub, five), three));
345 check(1, make_app(make_app(sub, five), four));
346 check(0, make_app(make_app(sub, five), five));
348 print("checking min");
349 check(0, make_app(make_app(min, zero), zero));
350 check(0, make_app(make_app(min, zero), one));
351 check(0, make_app(make_app(min, zero), two));
352 check(0, make_app(make_app(min, zero), three));
353 check(0, make_app(make_app(min, zero), four));
354 check(0, make_app(make_app(min, zero), five));
355 check(0, make_app(make_app(min, one), zero));
356 check(1, make_app(make_app(min, one), one));
357 check(1, make_app(make_app(min, one), two));
358 check(1, make_app(make_app(min, one), three));
359 check(1, make_app(make_app(min, one), four));
360 check(1, make_app(make_app(min, one), five));
361 check(0, make_app(make_app(min, two), zero));
362 check(1, make_app(make_app(min, two), one));
363 check(2, make_app(make_app(min, two), two));
364 check(2, make_app(make_app(min, two), three));
365 check(2, make_app(make_app(min, two), four));
366 check(2, make_app(make_app(min, two), five));
367 check(0, make_app(make_app(min, three), zero));
368 check(1, make_app(make_app(min, three), one));
369 check(2, make_app(make_app(min, three), two));
370 check(3, make_app(make_app(min, three), three));
371 check(3, make_app(make_app(min, three), four));
372 check(3, make_app(make_app(min, three), five));
373 check(0, make_app(make_app(min, four), zero));
374 check(1, make_app(make_app(min, four), one));
375 check(2, make_app(make_app(min, four), two));
376 check(3, make_app(make_app(min, four), three));
377 check(4, make_app(make_app(min, four), four));
378 check(4, make_app(make_app(min, four), five));
379 check(0, make_app(make_app(min, five), zero));
380 check(1, make_app(make_app(min, five), one));
381 check(2, make_app(make_app(min, five), two));
382 check(3, make_app(make_app(min, five), three));
383 check(4, make_app(make_app(min, five), four));
384 check(5, make_app(make_app(min, five), five));
386 print("checking max");
387 check(0, make_app(make_app(max, zero), zero));
388 check(1, make_app(make_app(max, zero), one));
389 check(2, make_app(make_app(max, zero), two));
390 check(3, make_app(make_app(max, zero), three));
391 check(4, make_app(make_app(max, zero), four));
392 check(5, make_app(make_app(max, zero), five));
393 check(1, make_app(make_app(max, one), zero));
394 check(1, make_app(make_app(max, one), one));
395 check(2, make_app(make_app(max, one), two));
396 check(3, make_app(make_app(max, one), three));
397 check(4, make_app(make_app(max, one), four));
398 check(5, make_app(make_app(max, one), five));
399 check(2, make_app(make_app(max, two), zero));
400 check(2, make_app(make_app(max, two), one));
401 check(2, make_app(make_app(max, two), two));
402 check(3, make_app(make_app(max, two), three));
403 check(4, make_app(make_app(max, two), four));
404 check(5, make_app(make_app(max, two), five));
405 check(3, make_app(make_app(max, three), zero));
406 check(3, make_app(make_app(max, three), one));
407 check(3, make_app(make_app(max, three), two));
408 check(3, make_app(make_app(max, three), three));
409 check(4, make_app(make_app(max, three), four));
410 check(5, make_app(make_app(max, three), five));
411 check(4, make_app(make_app(max, four), zero));
412 check(4, make_app(make_app(max, four), one));
413 check(4, make_app(make_app(max, four), two));
414 check(4, make_app(make_app(max, four), three));
415 check(4, make_app(make_app(max, four), four));
416 check(5, make_app(make_app(max, four), five));
417 check(5, make_app(make_app(max, five), zero));
418 check(5, make_app(make_app(max, five), one));
419 check(5, make_app(make_app(max, five), two));
420 check(5, make_app(make_app(max, five), three));
421 check(5, make_app(make_app(max, five), four));
422 check(5, make_app(make_app(max, five), five));
424 print("checking lt");
425 checkbool(false, 0, make_app(make_app(lt, zero), zero));
426 checkbool(true, 0, make_app(make_app(lt, zero), one));
427 checkbool(true, 0, make_app(make_app(lt, zero), two));
428 checkbool(true, 0, make_app(make_app(lt, zero), three));
429 checkbool(true, 0, make_app(make_app(lt, zero), four));
430 checkbool(true, 0, make_app(make_app(lt, zero), five));
431 checkbool(false, 1, make_app(make_app(lt, one), zero));
432 checkbool(false, 1, make_app(make_app(lt, one), one));
433 checkbool(true, 1, make_app(make_app(lt, one), two));
434 checkbool(true, 1, make_app(make_app(lt, one), three));
435 checkbool(true, 1, make_app(make_app(lt, one), four));
436 checkbool(true, 1, make_app(make_app(lt, one), five));
437 checkbool(false, 2, make_app(make_app(lt, two), zero));
438 checkbool(false, 2, make_app(make_app(lt, two), one));
439 checkbool(false, 2, make_app(make_app(lt, two), two));
440 checkbool(true, 2, make_app(make_app(lt, two), three));
441 checkbool(true, 2, make_app(make_app(lt, two), four));
442 checkbool(true, 2, make_app(make_app(lt, two), five));
443 checkbool(false, 3, make_app(make_app(lt, three), zero));
444 checkbool(false, 3, make_app(make_app(lt, three), one));
445 checkbool(false, 3, make_app(make_app(lt, three), two));
446 checkbool(false, 3, make_app(make_app(lt, three), three));
447 checkbool(true, 3, make_app(make_app(lt, three), four));
448 checkbool(true, 3, make_app(make_app(lt, three), five));
449 checkbool(false, 4, make_app(make_app(lt, four), zero));
450 checkbool(false, 4, make_app(make_app(lt, four), one));
451 checkbool(false, 4, make_app(make_app(lt, four), two));
452 checkbool(false, 4, make_app(make_app(lt, four), three));
453 checkbool(false, 4, make_app(make_app(lt, four), four));
454 checkbool(true, 4, make_app(make_app(lt, four), five));
455 checkbool(false, 5, make_app(make_app(lt, five), zero));
456 checkbool(false, 5, make_app(make_app(lt, five), one));
457 checkbool(false, 5, make_app(make_app(lt, five), two));
458 checkbool(false, 5, make_app(make_app(lt, five), three));
459 checkbool(false, 5, make_app(make_app(lt, five), four));
460 checkbool(false, 5, make_app(make_app(lt, five), five));
462 print("checking leq");
463 checkbool(true, 0, make_app(make_app(leq, zero), zero));
464 checkbool(true, 0, make_app(make_app(leq, zero), one));
465 checkbool(true, 0, make_app(make_app(leq, zero), two));
466 checkbool(true, 0, make_app(make_app(leq, zero), three));
467 checkbool(true, 0, make_app(make_app(leq, zero), four));
468 checkbool(true, 0, make_app(make_app(leq, zero), five));
469 checkbool(false, 1, make_app(make_app(leq, one), zero));
470 checkbool(true, 1, make_app(make_app(leq, one), one));
471 checkbool(true, 1, make_app(make_app(leq, one), two));
472 checkbool(true, 1, make_app(make_app(leq, one), three));
473 checkbool(true, 1, make_app(make_app(leq, one), four));
474 checkbool(true, 1, make_app(make_app(leq, one), five));
475 checkbool(false, 2, make_app(make_app(leq, two), zero));
476 checkbool(false, 2, make_app(make_app(leq, two), one));
477 checkbool(true, 2, make_app(make_app(leq, two), two));
478 checkbool(true, 2, make_app(make_app(leq, two), three));
479 checkbool(true, 2, make_app(make_app(leq, two), four));
480 checkbool(true, 2, make_app(make_app(leq, two), five));
481 checkbool(false, 3, make_app(make_app(leq, three), zero));
482 checkbool(false, 3, make_app(make_app(leq, three), one));
483 checkbool(false, 3, make_app(make_app(leq, three), two));
484 checkbool(true, 3, make_app(make_app(leq, three), three));
485 checkbool(true, 3, make_app(make_app(leq, three), four));
486 checkbool(true, 3, make_app(make_app(leq, three), five));
487 checkbool(false, 4, make_app(make_app(leq, four), zero));
488 checkbool(false, 4, make_app(make_app(leq, four), one));
489 checkbool(false, 4, make_app(make_app(leq, four), two));
490 checkbool(false, 4, make_app(make_app(leq, four), three));
491 checkbool(true, 4, make_app(make_app(leq, four), four));
492 checkbool(true, 4, make_app(make_app(leq, four), five));
493 checkbool(false, 5, make_app(make_app(leq, five), zero));
494 checkbool(false, 5, make_app(make_app(leq, five), one));
495 checkbool(false, 5, make_app(make_app(leq, five), two));
496 checkbool(false, 5, make_app(make_app(leq, five), three));
497 checkbool(false, 5, make_app(make_app(leq, five), four));
498 checkbool(true, 5, make_app(make_app(leq, five), five));
500 print("checking eq");
501 checkbool(true, 0, make_app(make_app(eq, zero), zero));
502 checkbool(false, 0, make_app(make_app(eq, zero), one));
503 checkbool(false, 0, make_app(make_app(eq, zero), two));
504 checkbool(false, 0, make_app(make_app(eq, zero), three));
505 checkbool(false, 0, make_app(make_app(eq, zero), four));
506 checkbool(false, 0, make_app(make_app(eq, zero), five));
507 checkbool(false, 1, make_app(make_app(eq, one), zero));
508 checkbool(true, 1, make_app(make_app(eq, one), one));
509 checkbool(false, 1, make_app(make_app(eq, one), two));
510 checkbool(false, 1, make_app(make_app(eq, one), three));
511 checkbool(false, 1, make_app(make_app(eq, one), four));
512 checkbool(false, 1, make_app(make_app(eq, one), five));
513 checkbool(false, 2, make_app(make_app(eq, two), zero));
514 checkbool(false, 2, make_app(make_app(eq, two), one));
515 checkbool(true, 2, make_app(make_app(eq, two), two));
516 checkbool(false, 2, make_app(make_app(eq, two), three));
517 checkbool(false, 2, make_app(make_app(eq, two), four));
518 checkbool(false, 2, make_app(make_app(eq, two), five));
519 checkbool(false, 3, make_app(make_app(eq, three), zero));
520 checkbool(false, 3, make_app(make_app(eq, three), one));
521 checkbool(false, 3, make_app(make_app(eq, three), two));
522 checkbool(true, 3, make_app(make_app(eq, three), three));
523 checkbool(false, 3, make_app(make_app(eq, three), four));
524 checkbool(false, 3, make_app(make_app(eq, three), five));
525 checkbool(false, 4, make_app(make_app(eq, four), zero));
526 checkbool(false, 4, make_app(make_app(eq, four), one));
527 checkbool(false, 4, make_app(make_app(eq, four), two));
528 checkbool(false, 4, make_app(make_app(eq, four), three));
529 checkbool(true, 4, make_app(make_app(eq, four), four));
530 checkbool(false, 4, make_app(make_app(eq, four), five));
531 checkbool(false, 5, make_app(make_app(eq, five), zero));
532 checkbool(false, 5, make_app(make_app(eq, five), one));
533 checkbool(false, 5, make_app(make_app(eq, five), two));
534 checkbool(false, 5, make_app(make_app(eq, five), three));
535 checkbool(false, 5, make_app(make_app(eq, five), four));
536 checkbool(true, 5, make_app(make_app(eq, five), five));
538 print("checking div");
539 check(0, make_app(make_app(div, zero), one));
540 check(0, make_app(make_app(div, zero), two));
541 check(0, make_app(make_app(div, zero), three));
542 check(0, make_app(make_app(div, zero), four));
543 check(0, make_app(make_app(div, zero), five));
544 check(1, make_app(make_app(div, one), one));
545 check(0, make_app(make_app(div, one), two));
546 check(0, make_app(make_app(div, one), three));
547 check(0, make_app(make_app(div, one), four));
548 check(0, make_app(make_app(div, one), five));
549 check(2, make_app(make_app(div, two), one));
550 check(1, make_app(make_app(div, two), two));
551 check(0, make_app(make_app(div, two), three));
552 check(0, make_app(make_app(div, two), four));
553 check(0, make_app(make_app(div, two), five));
554 check(3, make_app(make_app(div, three), one));
555 check(1, make_app(make_app(div, three), two));
556 check(1, make_app(make_app(div, three), three));
557 check(0, make_app(make_app(div, three), four));
558 check(0, make_app(make_app(div, three), five));
559 check(4, make_app(make_app(div, four), one));
560 check(2, make_app(make_app(div, four), two));
561 check(1, make_app(make_app(div, four), three));
562 check(1, make_app(make_app(div, four), four));
563 check(0, make_app(make_app(div, four), five));
564 check(5, make_app(make_app(div, five), one));
565 check(2, make_app(make_app(div, five), two));
566 check(1, make_app(make_app(div, five), three));
567 check(1, make_app(make_app(div, five), four));
568 check(1, make_app(make_app(div, five), five));
570 print("checking mod");
571 check(0, make_app(make_app(mod, zero), one));
572 check(0, make_app(make_app(mod, zero), two));
573 check(0, make_app(make_app(mod, zero), three));
574 check(0, make_app(make_app(mod, zero), four));
575 check(0, make_app(make_app(mod, zero), five));
576 check(0, make_app(make_app(mod, one), one));
577 check(1, make_app(make_app(mod, one), two));
578 check(1, make_app(make_app(mod, one), three));
579 check(1, make_app(make_app(mod, one), four));
580 check(1, make_app(make_app(mod, one), five));
581 check(0, make_app(make_app(mod, two), one));
582 check(0, make_app(make_app(mod, two), two));
583 check(2, make_app(make_app(mod, two), three));
584 check(2, make_app(make_app(mod, two), four));
585 check(2, make_app(make_app(mod, two), five));
586 check(0, make_app(make_app(mod, three), one));
587 check(1, make_app(make_app(mod, three), two));
588 check(0, make_app(make_app(mod, three), three));
589 check(3, make_app(make_app(mod, three), four));
590 check(3, make_app(make_app(mod, three), five));
591 check(0, make_app(make_app(mod, four), one));
592 check(0, make_app(make_app(mod, four), two));
593 check(1, make_app(make_app(mod, four), three));
594 check(0, make_app(make_app(mod, four), four));
595 check(4, make_app(make_app(mod, four), five));
596 check(0, make_app(make_app(mod, five), one));
597 check(1, make_app(make_app(mod, five), two));
598 check(2, make_app(make_app(mod, five), three));
599 check(1, make_app(make_app(mod, five), four));
600 check(0, make_app(make_app(mod, five), five));
603 print("checking fact1");
604 check(1, make_app(fact1, zero));
605 check(1, make_app(fact1, one));
606 check(2, make_app(fact1, two));
607 check(6, make_app(fact1, three));
608 check(24, make_app(fact1, four));
612 print("checking fact2");
613 check(1, make_app(fact2, zero));
614 check(1, make_app(fact2, one));
615 check(2, make_app(fact2, two));
616 check(6, make_app(fact2, three));
617 check(24, make_app(fact2, four));
621 print("checking fact3");
622 check(1, make_app(fact3, zero));
623 check(1, make_app(fact3, one));
624 check(2, make_app(fact3, two));
625 check(6, make_app(fact3, three));
626 check(24, make_app(fact3, four));
630 print("checking fact4");
631 check(1, make_app(fact4, zero));
632 check(1, make_app(fact4, one));
633 check(2, make_app(fact4, two));
634 check(6, make_app(fact4, three));
635 check(24, make_app(fact4, four));
639 print("checking fact5");
640 check(1, make_app(fact5, zero));
641 check(1, make_app(fact5, one));
642 check(2, make_app(fact5, two));
643 check(6, make_app(fact5, three));
644 check(24, make_app(fact5, four));