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