YES
Time: 0.001328
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: roof(-raise)-bounded by 2
   Automaton:
    { f_2(9) -> 10*
      f_1(7) -> 8*
      f_1(5) -> 6*
      f_0(1) -> 1*
       a_1() -> 2*
       a_0() -> 1*
     h_2(10) -> 11*
      h_1(2) -> 3*
      h_0(1) -> 1*
     g_2(11) -> 12*
      g_1(3) -> 4*
      g_0(1) -> 1*
          12 -> 3*
           8 -> 2*
           6 -> 2*
           4 -> 6 | 1
           3 -> 9 | 7
           1 -> 5*}
   Strict:
    {}
   Qed