(VAR x y ) (STRATEGY INNERMOST) (RULES gcd(x,0) -> x gcd(0,y) -> y gcd(s(x),s(y)) -> if(<(x,y),gcd(s(x),-(y,x)),gcd(-(x,y),s(y))) )