YES
Time: 0.034862
TRS:
 {h f(x, y) -> f(f(a(), h h y), x)}
 DP:
  DP:
   {h# f(x, y) -> h# y,
    h# f(x, y) -> h# h y}
  TRS:
  {h f(x, y) -> f(f(a(), h h y), x)}
  EDG:
   {(h# f(x, y) -> h# y, h# f(x, y) -> h# h y)
    (h# f(x, y) -> h# y, h# f(x, y) -> h# y)
    (h# f(x, y) -> h# h y, h# f(x, y) -> h# y)
    (h# f(x, y) -> h# h y, h# f(x, y) -> h# h y)}
   SCCS (1):
    Scc:
     {h# f(x, y) -> h# y,
      h# f(x, y) -> h# h y}
    SCC (2):
     Strict:
      {h# f(x, y) -> h# y,
       h# f(x, y) -> h# h y}
     Weak:
     {h f(x, y) -> f(f(a(), h h y), x)}
     BOUND:
      Bound: match(-raise)-DP-bounded by 2
      Automaton:
       {   h#_2(15) -> 5*
           h#_2(10) -> 5*
            h#_2(9) -> 5*
            h#_2(7) -> 5*
           h#_1(11) -> 5*
           h#_1(10) -> 5*
            h#_1(9) -> 5*
            h#_1(7) -> 5*
           h#_0(10) -> 5*
            h#_0(9) -> 5*
            h#_0(7) -> 5*
            h_2(10) -> 15*
             h_2(9) -> 15*
             h_2(7) -> 15*
            h_1(11) -> 13*
            h_1(10) -> 11*
             h_1(9) -> 11*
             h_1(7) -> 11*
            h_0(10) -> 10*
             h_0(9) -> 10*
             h_0(7) -> 10*
              a_1() -> 12*
              a_0() -> 9*
        f_1(14, 14) -> 13*
        f_1(14, 10) -> 15 | 11
         f_1(14, 9) -> 15 | 11
         f_1(14, 7) -> 15 | 11
        f_1(12, 13) -> 14*
        f_0(10, 10) -> 7*
         f_0(10, 9) -> 7*
         f_0(10, 7) -> 7*
         f_0(9, 10) -> 7*
          f_0(9, 9) -> 7*
          f_0(9, 7) -> 7*
         f_0(7, 10) -> 10 | 7
          f_0(7, 9) -> 10 | 7
          f_0(7, 7) -> 10 | 7}
      Strict:
       {h# f(x, y) -> h# y}
      EDG:
       {(h# f(x, y) -> h# y, h# f(x, y) -> h# y)}
       SCCS (1):
        Scc:
         {h# f(x, y) -> h# y}
        SCC (1):
         Strict:
          {h# f(x, y) -> h# y}
         Weak:
         {h f(x, y) -> f(f(a(), h h y), x)}
         SPSC:
          Simple Projection:
           pi(h#) = 0
          Strict:
           {}
          Qed