macro if ((;
macro then )(;
macro else )(;
macro endif ));
macro begin (;
macro end );

K = lambda x y x;
I = lambda x x;

N1 = lambda x y z x;
N0 = lambda x y z y;
Nm1 = lambda x y z z;

K33 = lambda x y z z;

Pair = lambda x y z (z x y);

Isn = lambda x (x K33 K K I (K I) K);

%<----- ----- ----- ----- test ----- ----- ----- ----->%
Isn N1 t f;
Isn N0 t f;
Isn Nm1 t f;
Isn (Pair N0 N0) t f;
%<----- ----- ----- ----- /test ----- ----- ----- ----->%

HDR = lambda x
  if (Isn x) then N0 else (x K) endif;
FTR = lambda x
  if (Isn x) then x else (x (K I)) endif;

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));
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));
_Add = lambda x y z
  if (Isn y) then
    if (Isn z) then (Pair (Add1 x y z) (Add2 x y z))
    else (Pair (_Add (Add1 x (FTR y) (FTR z)) (HDR y) (HDR z)) (Add2 x (FTR y) (FTR z)))
    endif
  else (Pair (_Add (Add1 x (FTR y) (FTR z)) (HDR y) (HDR z)) (Add2 x (FTR y) (FTR z)))
  endif;
Add = _Add N0;

%<----- ----- ----- ----- test ----- ----- ----- ----->%
(HDR (Add  N1  N1)) 1 0 -1;
(FTR (Add  N1  N1)) 1 0 -1;
(HDR (Add  N1  Nm1)) 1 0 -1;
(FTR (Add  N1  Nm1)) 1 0 -1;
(HDR (Add Nm1 Nm1)) 1 0 -1;
(FTR (Add Nm1 Nm1)) 1 0 -1;
%<----- ----- ----- ----- /test ----- ----- ----- ----->%

Iz = lambda x
  if (Isn x) then
    x (K I) K (K I)
  else
    K I
  endif;

Tr = lambda x
  if (Isn (HDR x)) then
    (HDR x) x (FTR x) x
  else
    if (Iz (Tr (HDR x))) then
      (FTR x)
    else
      Pair (Tr (HDR x)) (FTR x)
    endif
  endif;

%<----- ----- ----- ----- test ----- ----- ----- ----->%
(Isn (Tr (Pair N1 N0))) t f;
(Isn (Tr (Pair N0 N0))) t f;
(Isn (Tr (Pair N0 N1))) t f;
(Iz (Tr (Pair N0 N0))) t f;
(Iz (Tr (Pair N0 N1))) t f;
Tr N0;
%<----- ----- ----- ----- /test ----- ----- ----- ----->%

_STD = lambda x y
  if (Isn y) then
    if (Iz x) then y
    else N0
    endif
  else
    if (Iz x) then
      (FTR y)
        (Pair (_STD N0 (HDR y)) (FTR y))
        (Pair (_STD N0 (HDR y)) (FTR y))
        (Pair (_STD Nm1 (HDR y)) N1)
    else
      (FTR y)
        (Pair (_STD N0 (HDR y)) N0)
        (Pair (_STD Nm1 (HDR y)) N1)
        ((FTR (HDR y))
           (Pair (_STD N0 (HDR y)) N1)
           (Pair (_STD Nm1 (HDR y)) N0)
           (Pair (_STD Nm1 (HDR y)) N1))
    endif
  endif;

STD1 = _STD N0;

%<----- ----- ----- ----- test ----- ----- ----- ----->%
(STD1 N1) 1 0 -1;
X = STD1 (Pair N0 N1);
(HDR X) 1 0 -1;
(FTR X) 1 0 -1;
X = STD1 (Pair (Pair N1 N0) Nm1);
(HDR (HDR X)) 1 0 -1;
(FTR (HDR X)) 1 0 -1;
(FTR X) 1 0 -1;
(Isn (HDR X)) t f;
%<----- ----- ----- ----- /test ----- ----- ----- ----->%