YES
Time: 0.004892
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)-DP-bounded by 2
       Automaton:
        { f_2(25) -> 26*
          f_1(20) -> 21*
          f_1(18) -> 19*
          f_1(16) -> 17*
          f_1(13) -> 14*
          f_0(12) -> 12*
          f_0(11) -> 12*
           f_0(9) -> 12*
           f_0(8) -> 12*
            a_1() -> 22*
            a_0() -> 11*
         h#_2(26) -> 27*
         h#_1(14) -> 15*
         h#_0(12) -> 6*
          h_1(22) -> 23*
          h_0(12) -> 9*
          h_0(11) -> 9*
           h_0(9) -> 9*
           h_0(8) -> 9*
          g_1(23) -> 24*
          g_0(12) -> 8*
          g_0(11) -> 8*
           g_0(9) -> 8*
           g_0(8) -> 8*
               27 -> 15*
               24 -> 19*
               23 -> 25*
               21 -> 14*
               19 -> 14*
               17 -> 14*
               15 -> 6*
               12 -> 20*
               11 -> 18*
                9 -> 16*
                8 -> 13 | 12 | 9}
       Strict:
        {}
       Qed