I x      = x;
K x y    = x;
S x y z  = x y(x z);
B x y z  = x (y z);
C x y z  = x z y;
W x y    = x y y;
SOMEGA x = x x;
OMEGA    = SOMEGA SOMEGA;
Y g      = (\x.g (x x))(\x.g (x x));

ZERO f x  = x;
SUCC n f x = f (n f x);
PLUS m n   = m SUCC n;
MULT m n   = m (PLUS n) 0;
EXP b e    = e b;

PRED n f x = n(\g h.h(g f))(\u.x)(\u.u);
SUB m n    = n PRED m;

ISZERO n   = n (\x.false) true;
LEQ m n    = ISZERO (MINUS m n);

AND p q = p q p;
OR p    = p p;