[[[y-combinator [/. ADD [/. X [/. Y [if [= X 0] Y [[ADD [-- X]] [++ Y]]]]]]]  2] 3]


[[[y-combinator [/. ADD [/. X [/. Y [if [= X 0] Y [[ADD [-- X]] [++ Y]]]]]]] 33] 4]

[[[/. [@p X Y] X] 
[y-combinator  [/. T 
[@p [/. A [cases [[/. 1 false] A]
                 [[/. X [[[/. [@p X Y] Y] T] [-- X]]] A]]]
    [/. A [cases [[/. 1 true] A]
                 [[/. X [[[/. [@p X Y] X] T] [-- X]]] A]]]]]]] 6]