(VAR X Y) (RULES nats -> adx(zeros) zeros -> cons(n__0,n__zeros) incr(cons(X,Y)) -> cons(n__s(activate(X)),n__incr(activate(Y))) adx(cons(X,Y)) -> incr(cons(activate(X),n__adx(activate(Y)))) hd(cons(X,Y)) -> activate(X) tl(cons(X,Y)) -> activate(Y) 0 -> n__0 zeros -> n__zeros s(X) -> n__s(X) incr(X) -> n__incr(X) adx(X) -> n__adx(X) activate(n__0) -> 0 activate(n__zeros) -> zeros activate(n__s(X)) -> s(X) activate(n__incr(X)) -> incr(X) activate(n__adx(X)) -> adx(X) activate(X) -> X )