/* Standard definition of booleans */
tru = lambda t. lambda f. t;
fls = lambda t. lambda f. f;
not = lambda b. b fls tru;

/* Test: */
not (not (not fls));

/* Standard definition of pairs */
fst = lambda p. p tru;
snd = lambda p. p fls;
pair = lambda x. lambda y. lambda sel. sel x y;

/* Standard definitions of church numerals and arithmetic operations */
c0 = lambda s. lambda z. z;
c1 = lambda s. lambda z. s z;
c2 = lambda s. lambda z. s (s z);
c3 = lambda s. lambda z. s (s (s z));
scc = lambda n. lambda s. lambda z. s (n s z);
plus = lambda m. lambda n. m scc n;
iszro = lambda m. m (lambda dummy. fls) tru;
zz = pair c0 c0;
ss = lambda p. pair (snd p) (plus c1 (snd p));
prd = lambda m. fst (m ss zz);
double = lambda n. plus n n;

/* Test: */
iszro (prd (prd (double c1)));

/* Standard call-by-value fixed point function. */
fix = lambda f. (lambda x. f (lambda y. x x y)) (lambda x. f (lambda y. x x y));