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