(VAR X Y) (STRATEGY CONTEXTSENSITIVE (p 1) (0) (s 1) (leq 1 2) (true) (false) (if 1) (diff 1 2) ) (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) -> X if(false,X,Y) -> Y diff(X,Y) -> if(leq(X,Y),0,s(diff(p(X),Y))) )