YES (VAR x y) (RULES f(x) -> a() g(x,y) -> a() h(x,y) -> a() ) (COMMENT Termination is shown by EKBO with interpretations on natural numbers h_A(x1,x2) = 0 f_A(x1) = 0 g_A(x1,x2) = 0 a_A = 0 h#_A(x1,x2) = x1 + x2 g#_A(x1,x2) = x1 + x2 a#_A = 0 weights w0 = 1 w(h) = 1 w(f) = 1 w(g) = 0 w(a) = 1 and precedence: g > h > f > a )