(VAR x y ) (STRATEGY INNERMOST) (RULES -(0,y) -> 0 -(x,0) -> x -(x,s(y)) -> if(greater(x,s(y)),s(-(x,p(s(y)))),0) p(0) -> 0 p(s(x)) -> x )