(VAR X Y X1 X2) (RULES p(0) -> 0 p(s(X)) -> X leq(0,Y) -> true leq(s(X),0) -> false leq(s(X),s(Y)) -> leq(X,Y) if(true,X,Y) -> activate(X) if(false,X,Y) -> activate(Y) diff(X,Y) -> if(leq(X,Y),n__0,n__s(n__diff(n__p(X),Y))) 0 -> n__0 s(X) -> n__s(X) diff(X1,X2) -> n__diff(X1,X2) p(X) -> n__p(X) activate(n__0) -> 0 activate(n__s(X)) -> s(activate(X)) activate(n__diff(X1,X2)) -> diff(activate(X1),activate(X2)) activate(n__p(X)) -> p(activate(X)) activate(X) -> X )