define Y (lambda f . (lambda x . f (x x))(lambda x . f( x x)));
define T (lambda x y . x);
define F (lambda x y . y);
define K33 (lambda x y z . z);
define Pair (lambda x y z . z x y);
define K (lambda x y . x);

define Isn (lambda x . (x K33 K K I (K I) K));

define N1 (lambda x y z . x);
define N0 (lambda x y z . y);
define Nm1 (lambda x y z . z);


define Hdr (lambda x . (Isn x) N0 (x K));
define Ftr (lambda x . (Isn x) x (x (K I)));


define Add1  lambda x y z .
  (x (y (z N1 N1 N0) (z N1 N0 N0) N0)
     (y (z N1 N0 N0) N0 (z N0 N0 Nm1))
     (y N0 (z N0 N0 Nm1) (z N0 Nm1 Nm1)));

define Add2  lambda x y z .
  (x (y (z N1 N0 N1) (z N0 N1 N0) z)
     (y (z N0 N1 N0) z (z N0 Nm1 N0))
     (y z (z N0 Nm1 N0) (z Nm1 N0 Nm1)));

define Add3 lambda f x y z .
  (Isn y)
    ((Isn z)
       (Pair (Add1 x y z) (Add2 x y z))
       (Pair (f (Add1 x (Ftr y) (Ftr z))(Hdr y) (Hdr z))
          (Add2 x (Ftr y) (Ftr z))))
     (Pair (f (Add1 x (Ftr y) (Ftr z)) (Hdr y) (Hdr z))
        (Add2 x (Ftr y) (Ftr z)));

define Add4 lambda x . Y Add3 x;

define Add Add4 N0;


Add N1 N1;

Add (lambda x . x N1 N1)(lambda x . x (lambda x . x N1 N0)N0);



Add
(lambda x.x(lambda x.x(lambda x.x(lambda x.x(lambda x.x(lambda x.x(lambda x.x N1 N0)Nm1)N1)N0)N0)Nm1)N1)
(lambda x.x(lambda x.x(lambda x.x(lambda x.x(lambda x.x(lambda x.x(lambda x.x(lambda x.x(lambda x.x(lambda x.x N1 Nm1)N0)Nm1)N1)N1)N1)N0)Nm1)Nm1)N0);