YES (VAR x y) (RULES plus(x,s(y)) -> s(plus(x,y)) plus(x,z()) -> x ) (COMMENT Termination is shown by KBO with weight w0 = 1 w(plus) = 0 w(z) = 1 w(s) = 1 and precedence: plus > s > z )