YES
Time: 0.001413
TRS:
 {         h g x -> g h f x,
           f a() -> g h a(),
  k(x, h x, a()) -> h x,
    k(f x, y, x) -> f x}
 RUF:
  Strict:
   {h g x -> g h f x,
    f a() -> g h a()}
  Weak:
   {}
  BOUND:
   Bound: top(-raise)-bounded by 2
   Automaton:
    {f_2(12) -> 13*
     f_1(10) -> 11*
      f_1(5) -> 6*
      f_0(1) -> 1*
       a_2() -> 7*
       a_1() -> 2*
       a_0() -> 1*
     h_2(13) -> 14*
      h_2(7) -> 8*
      h_1(2) -> 3*
      h_0(1) -> 1*
     g_2(14) -> 15*
      g_2(8) -> 9*
      g_1(3) -> 4*
      g_0(1) -> 1*
          15 -> 3*
          11 -> 2*
           9 -> 6*
           8 -> 12*
           6 -> 2*
           4 -> 1*
           3 -> 10*
           1 -> 5*}
   Strict:
    {}
   Qed