YES (VAR x) (RULES g(x) -> f(f(x)) ) (COMMENT Termination is shown by EKBO with interpretations on natural numbers f_A(x1) = 1 g_A(x1) = 2 weights w0 = 1 w(f) = 1 w(g) = 3 and precedence: g > f )