YES
Time: 0.004306
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:
   {}
  DP:
   DP:
    {h# g x -> h# f x,
     h# g x -> f# x,
     f# a() -> h# a()}
   TRS:
   {h g x -> g h f x,
    f a() -> g h a()}
   EDG:
    {(h# g x -> h# f x, h# g x -> f# x)
     (h# g x -> h# f x, h# g x -> h# f x)
     (h# g x -> f# x, f# a() -> h# a())}
    SCCS (1):
     Scc:
      {h# g x -> h# f x}
     SCC (1):
      Strict:
       {h# g x -> h# f x}
      Weak:
      {h g x -> g h f x,
       f a() -> g h a()}
      BOUND:
       Bound: match(-raise)-bounded by 2
       Automaton:
        { f_2(12) -> 13*
          f_1(10) -> 11*
           f_1(2) -> 3*
           f_0(1) -> 1*
            a_1() -> 5*
            a_0() -> 1*
         h#_2(13) -> 14*
          h#_1(3) -> 4*
          h#_0(1) -> 1*
          h_2(15) -> 16*
           h_1(8) -> 9*
           h_1(5) -> 6*
           h_0(1) -> 1*
          g_2(16) -> 17*
           g_1(6) -> 7*
           g_0(1) -> 1*
               17 -> 9*
               14 -> 4*
               13 -> 15*
               11 -> 3*
                9 -> 6*
                7 -> 3 | 1
                6 -> 12 | 10
                4 -> 1*
                3 -> 8*
                1 -> 2*}
       Strict:
        {}
       Qed