preamble

   1 I x      = x;
   2 K x y    = x;
   3 S x y z  = x y(x z);
   4 B x y z  = x (y z);
   5 C x y z  = x z y;
   6 W x y    = x y y;
   7 SOMEGA x = x x;
   8 OMEGA    = SOMEGA SOMEGA;
   9 Y g      = (\x.g (x x))(\x.g (x x));
  10
  11 ZERO f x  = x;
  12 SUCC n f x = f (n f x);
  13 PLUS m n   = m SUCC n;
  14 MULT m n   = m (PLUS n) 0;
  15 EXP b e    = e b;
  16
  17 PRED n f x = n(\g h.h(g f))(\u.x)(\u.u);
  18 SUB m n    = n PRED m;
  19
  20 ISZERO n   = n (\x.false) true;
  21 LEQ m n    = ISZERO (MINUS m n);
  22
  23 AND p q = p q p;
  24 OR p    = p p;