YES
Time: 0.057284
TRS:
 {f(f(0(), x), 1()) -> f(g f(x, x), x),
          f(g x, y) -> g f(x, y)}
 DP:
  DP:
   {f#(f(0(), x), 1()) -> f#(x, x),
    f#(f(0(), x), 1()) -> f#(g f(x, x), x),
            f#(g x, y) -> f#(x, y)}
  TRS:
  {f(f(0(), x), 1()) -> f(g f(x, x), x),
           f(g x, y) -> g f(x, y)}
  EDG:
   {(f#(g x, y) -> f#(x, y), f#(g x, y) -> f#(x, y))
    (f#(g x, y) -> f#(x, y), f#(f(0(), x), 1()) -> f#(g f(x, x), x))
    (f#(g x, y) -> f#(x, y), f#(f(0(), x), 1()) -> f#(x, x))
    (f#(f(0(), x), 1()) -> f#(x, x), f#(g x, y) -> f#(x, y))
    (f#(f(0(), x), 1()) -> f#(g f(x, x), x), f#(g x, y) -> f#(x, y))}
   SCCS (1):
    Scc:
     {f#(f(0(), x), 1()) -> f#(x, x),
      f#(f(0(), x), 1()) -> f#(g f(x, x), x),
              f#(g x, y) -> f#(x, y)}
    SCC (3):
     Strict:
      {f#(f(0(), x), 1()) -> f#(x, x),
       f#(f(0(), x), 1()) -> f#(g f(x, x), x),
               f#(g x, y) -> f#(x, y)}
     Weak:
     {f(f(0(), x), 1()) -> f(g f(x, x), x),
              f(g x, y) -> g f(x, y)}
     BOUND:
      Bound: top(-raise)-DP-bounded by 1
      Automaton:
       {       1_0() -> 10*
               0_0() -> 9*
             g_0(10) -> 8*
              g_0(9) -> 8*
              g_0(8) -> 8*
              g_0(7) -> 8 | 7
        f#_1(10, 10) -> 6*
         f#_1(10, 8) -> 6*
          f#_1(9, 9) -> 6*
          f#_1(9, 8) -> 6*
          f#_1(8, 8) -> 6*
          f#_1(7, 8) -> 6*
          f#_1(7, 7) -> 6*
        f#_0(10, 10) -> 6*
         f#_0(10, 9) -> 6*
         f#_0(10, 8) -> 6*
         f#_0(10, 7) -> 6*
         f#_0(9, 10) -> 6*
          f#_0(9, 9) -> 6*
          f#_0(9, 8) -> 6*
          f#_0(9, 7) -> 6*
         f#_0(8, 10) -> 6*
          f#_0(8, 9) -> 6*
          f#_0(8, 8) -> 6*
          f#_0(8, 7) -> 6*
         f#_0(7, 10) -> 6*
          f#_0(7, 9) -> 6*
          f#_0(7, 8) -> 6*
          f#_0(7, 7) -> 6*
         f_0(10, 10) -> 7*
          f_0(10, 9) -> 7*
          f_0(10, 8) -> 7*
          f_0(10, 7) -> 7*
          f_0(9, 10) -> 7*
           f_0(9, 9) -> 7*
           f_0(9, 8) -> 7*
           f_0(9, 7) -> 7*
          f_0(8, 10) -> 7*
           f_0(8, 9) -> 7*
           f_0(8, 8) -> 7*
           f_0(8, 7) -> 7*
          f_0(7, 10) -> 7*
           f_0(7, 9) -> 7*
           f_0(7, 8) -> 7*
           f_0(7, 7) -> 7*}
      Strict:
       {f#(f(0(), x), 1()) -> f#(g f(x, x), x),
                f#(g x, y) -> f#(x, y)}
      EDG:
       {(f#(g x, y) -> f#(x, y), f#(g x, y) -> f#(x, y))
        (f#(g x, y) -> f#(x, y), f#(f(0(), x), 1()) -> f#(g f(x, x), x))
        (f#(f(0(), x), 1()) -> f#(g f(x, x), x), f#(g x, y) -> f#(x, y))}
       SCCS (1):
        Scc:
         {f#(f(0(), x), 1()) -> f#(g f(x, x), x),
                  f#(g x, y) -> f#(x, y)}
        SCC (2):
         Strict:
          {f#(f(0(), x), 1()) -> f#(g f(x, x), x),
                   f#(g x, y) -> f#(x, y)}
         Weak:
         {f(f(0(), x), 1()) -> f(g f(x, x), x),
                  f(g x, y) -> g f(x, y)}
         BOUND:
          Bound: top(-raise)-DP-bounded by 1
          Automaton:
           {       1_0() -> 12*
                   0_0() -> 11*
                 g_1(25) -> 25 | 23
                 g_1(23) -> 24*
                 g_1(21) -> 22 | 21
                 g_1(19) -> 20*
                 g_1(17) -> 18*
                 g_1(15) -> 16 | 15
                 g_0(14) -> 10*
                 g_0(13) -> 14 | 13
                 g_0(12) -> 10*
                 g_0(11) -> 10*
                 g_0(10) -> 10*
            f#_1(25, 14) -> 6*
            f#_1(24, 14) -> 6*
            f#_1(23, 14) -> 6*
            f#_1(22, 13) -> 6*
            f#_1(21, 13) -> 6*
            f#_1(20, 12) -> 6*
            f#_1(19, 12) -> 6*
            f#_1(18, 11) -> 6*
            f#_1(17, 11) -> 6*
            f#_1(16, 10) -> 6*
            f#_1(15, 10) -> 6*
            f#_0(14, 14) -> 6*
            f#_0(14, 13) -> 6*
            f#_0(14, 12) -> 6*
            f#_0(14, 11) -> 6*
            f#_0(14, 10) -> 6*
            f#_0(13, 14) -> 6*
            f#_0(13, 13) -> 6*
            f#_0(13, 12) -> 6*
            f#_0(13, 11) -> 6*
            f#_0(13, 10) -> 6*
             f_1(14, 14) -> 23*
             f_1(14, 10) -> 15*
             f_1(13, 14) -> 25*
             f_1(13, 13) -> 21*
             f_1(13, 10) -> 15*
             f_1(12, 12) -> 19*
             f_1(12, 10) -> 15*
             f_1(11, 11) -> 17*
             f_1(11, 10) -> 15*
             f_1(10, 10) -> 15*
             f_0(14, 14) -> 13*
             f_0(14, 13) -> 13*
             f_0(14, 12) -> 13*
             f_0(14, 11) -> 13*
             f_0(14, 10) -> 13*
             f_0(13, 14) -> 13*
             f_0(13, 13) -> 13*
             f_0(13, 12) -> 13*
             f_0(13, 11) -> 13*
             f_0(13, 10) -> 13*
             f_0(12, 14) -> 13*
             f_0(12, 13) -> 13*
             f_0(12, 12) -> 13*
             f_0(12, 11) -> 13*
             f_0(12, 10) -> 13*
             f_0(11, 14) -> 13*
             f_0(11, 13) -> 13*
             f_0(11, 12) -> 13*
             f_0(11, 11) -> 13*
             f_0(11, 10) -> 13*
             f_0(10, 14) -> 13*
             f_0(10, 13) -> 13*
             f_0(10, 12) -> 13*
             f_0(10, 11) -> 13*
             f_0(10, 10) -> 13*}
          Strict:
           {f#(g x, y) -> f#(x, y)}
          EDG:
           {(f#(g x, y) -> f#(x, y), f#(g x, y) -> f#(x, y))}
           SCCS (1):
            Scc:
             {f#(g x, y) -> f#(x, y)}
            SCC (1):
             Strict:
              {f#(g x, y) -> f#(x, y)}
             Weak:
             {f(f(0(), x), 1()) -> f(g f(x, x), x),
                      f(g x, y) -> g f(x, y)}
             SPSC:
              Simple Projection:
               pi(f#) = 0
              Strict:
               {}
              Qed