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