YES
Time: 0.028590
TRS:
 {   f(x, y) -> x,
  h(x, x, y) -> g x,
       g a() -> h(a(), b(), a()),
         i x -> f(x, x)}
 BOUND:
  Bound: roof(-raise)-bounded by 2
  Automaton:
   {      i_0(9) -> 1*
          i_0(8) -> 1*
          i_0(5) -> 1*
          i_0(4) -> 1*
          i_0(1) -> 1*
          g_1(9) -> 1*
          g_1(8) -> 1*
          g_1(5) -> 1*
          g_1(4) -> 1*
          g_1(1) -> 1*
          g_0(9) -> 1*
          g_0(8) -> 1*
          g_0(5) -> 1*
          g_0(4) -> 1*
          g_0(1) -> 1*
           b_2() -> 9* | 7 | 4 | 3 | 1
           b_1() -> 4* | 3 | 1
           b_0() -> 1*
           a_2() -> 8* | 6 | 5 | 2 | 1
           a_1() -> 5* | 2 | 1
           a_0() -> 1*
    h_2(8, 9, 8) -> 1*
    h_2(8, 9, 6) -> 1*
    h_2(8, 7, 8) -> 1*
    h_2(8, 7, 6) -> 1*
    h_2(6, 9, 8) -> 1*
    h_2(6, 9, 6) -> 1*
    h_2(6, 7, 8) -> 1*
    h_2(6, 7, 6) -> 1*
    h_1(8, 9, 8) -> 1*
    h_1(8, 9, 5) -> 1*
    h_1(8, 9, 2) -> 1*
    h_1(8, 4, 8) -> 1*
    h_1(8, 4, 5) -> 1*
    h_1(8, 4, 2) -> 1*
    h_1(8, 3, 8) -> 1*
    h_1(8, 3, 5) -> 1*
    h_1(8, 3, 2) -> 1*
    h_1(5, 9, 8) -> 1*
    h_1(5, 9, 5) -> 1*
    h_1(5, 9, 2) -> 1*
    h_1(5, 4, 8) -> 1*
    h_1(5, 4, 5) -> 1*
    h_1(5, 4, 2) -> 1*
    h_1(5, 3, 8) -> 1*
    h_1(5, 3, 5) -> 1*
    h_1(5, 3, 2) -> 1*
    h_1(2, 9, 8) -> 1*
    h_1(2, 9, 5) -> 1*
    h_1(2, 9, 2) -> 1*
    h_1(2, 4, 8) -> 1*
    h_1(2, 4, 5) -> 1*
    h_1(2, 4, 2) -> 1*
    h_1(2, 3, 8) -> 1*
    h_1(2, 3, 5) -> 1*
    h_1(2, 3, 2) -> 1*
    h_0(9, 9, 9) -> 1*
    h_0(9, 9, 8) -> 1*
    h_0(9, 9, 5) -> 1*
    h_0(9, 9, 4) -> 1*
    h_0(9, 9, 1) -> 1*
    h_0(9, 8, 9) -> 1*
    h_0(9, 8, 8) -> 1*
    h_0(9, 8, 5) -> 1*
    h_0(9, 8, 4) -> 1*
    h_0(9, 8, 1) -> 1*
    h_0(9, 5, 9) -> 1*
    h_0(9, 5, 8) -> 1*
    h_0(9, 5, 5) -> 1*
    h_0(9, 5, 4) -> 1*
    h_0(9, 5, 1) -> 1*
    h_0(9, 4, 9) -> 1*
    h_0(9, 4, 8) -> 1*
    h_0(9, 4, 5) -> 1*
    h_0(9, 4, 4) -> 1*
    h_0(9, 4, 1) -> 1*
    h_0(9, 1, 9) -> 1*
    h_0(9, 1, 8) -> 1*
    h_0(9, 1, 5) -> 1*
    h_0(9, 1, 4) -> 1*
    h_0(9, 1, 1) -> 1*
    h_0(8, 9, 9) -> 1*
    h_0(8, 9, 8) -> 1*
    h_0(8, 9, 5) -> 1*
    h_0(8, 9, 4) -> 1*
    h_0(8, 9, 1) -> 1*
    h_0(8, 8, 9) -> 1*
    h_0(8, 8, 8) -> 1*
    h_0(8, 8, 5) -> 1*
    h_0(8, 8, 4) -> 1*
    h_0(8, 8, 1) -> 1*
    h_0(8, 5, 9) -> 1*
    h_0(8, 5, 8) -> 1*
    h_0(8, 5, 5) -> 1*
    h_0(8, 5, 4) -> 1*
    h_0(8, 5, 1) -> 1*
    h_0(8, 4, 9) -> 1*
    h_0(8, 4, 8) -> 1*
    h_0(8, 4, 5) -> 1*
    h_0(8, 4, 4) -> 1*
    h_0(8, 4, 1) -> 1*
    h_0(8, 1, 9) -> 1*
    h_0(8, 1, 8) -> 1*
    h_0(8, 1, 5) -> 1*
    h_0(8, 1, 4) -> 1*
    h_0(8, 1, 1) -> 1*
    h_0(5, 9, 9) -> 1*
    h_0(5, 9, 8) -> 1*
    h_0(5, 9, 5) -> 1*
    h_0(5, 9, 4) -> 1*
    h_0(5, 9, 1) -> 1*
    h_0(5, 8, 9) -> 1*
    h_0(5, 8, 8) -> 1*
    h_0(5, 8, 5) -> 1*
    h_0(5, 8, 4) -> 1*
    h_0(5, 8, 1) -> 1*
    h_0(5, 5, 9) -> 1*
    h_0(5, 5, 8) -> 1*
    h_0(5, 5, 5) -> 1*
    h_0(5, 5, 4) -> 1*
    h_0(5, 5, 1) -> 1*
    h_0(5, 4, 9) -> 1*
    h_0(5, 4, 8) -> 1*
    h_0(5, 4, 5) -> 1*
    h_0(5, 4, 4) -> 1*
    h_0(5, 4, 1) -> 1*
    h_0(5, 1, 9) -> 1*
    h_0(5, 1, 8) -> 1*
    h_0(5, 1, 5) -> 1*
    h_0(5, 1, 4) -> 1*
    h_0(5, 1, 1) -> 1*
    h_0(4, 9, 9) -> 1*
    h_0(4, 9, 8) -> 1*
    h_0(4, 9, 5) -> 1*
    h_0(4, 9, 4) -> 1*
    h_0(4, 9, 1) -> 1*
    h_0(4, 8, 9) -> 1*
    h_0(4, 8, 8) -> 1*
    h_0(4, 8, 5) -> 1*
    h_0(4, 8, 4) -> 1*
    h_0(4, 8, 1) -> 1*
    h_0(4, 5, 9) -> 1*
    h_0(4, 5, 8) -> 1*
    h_0(4, 5, 5) -> 1*
    h_0(4, 5, 4) -> 1*
    h_0(4, 5, 1) -> 1*
    h_0(4, 4, 9) -> 1*
    h_0(4, 4, 8) -> 1*
    h_0(4, 4, 5) -> 1*
    h_0(4, 4, 4) -> 1*
    h_0(4, 4, 1) -> 1*
    h_0(4, 1, 9) -> 1*
    h_0(4, 1, 8) -> 1*
    h_0(4, 1, 5) -> 1*
    h_0(4, 1, 4) -> 1*
    h_0(4, 1, 1) -> 1*
    h_0(1, 9, 9) -> 1*
    h_0(1, 9, 8) -> 1*
    h_0(1, 9, 5) -> 1*
    h_0(1, 9, 4) -> 1*
    h_0(1, 9, 1) -> 1*
    h_0(1, 8, 9) -> 1*
    h_0(1, 8, 8) -> 1*
    h_0(1, 8, 5) -> 1*
    h_0(1, 8, 4) -> 1*
    h_0(1, 8, 1) -> 1*
    h_0(1, 5, 9) -> 1*
    h_0(1, 5, 8) -> 1*
    h_0(1, 5, 5) -> 1*
    h_0(1, 5, 4) -> 1*
    h_0(1, 5, 1) -> 1*
    h_0(1, 4, 9) -> 1*
    h_0(1, 4, 8) -> 1*
    h_0(1, 4, 5) -> 1*
    h_0(1, 4, 4) -> 1*
    h_0(1, 4, 1) -> 1*
    h_0(1, 1, 9) -> 1*
    h_0(1, 1, 8) -> 1*
    h_0(1, 1, 5) -> 1*
    h_0(1, 1, 4) -> 1*
    h_0(1, 1, 1) -> 1*
       f_1(9, 9) -> 1*
       f_1(9, 8) -> 1*
       f_1(9, 5) -> 1*
       f_1(9, 4) -> 1*
       f_1(9, 1) -> 1*
       f_1(8, 9) -> 1*
       f_1(8, 8) -> 1*
       f_1(8, 5) -> 1*
       f_1(8, 4) -> 1*
       f_1(8, 1) -> 1*
       f_1(5, 9) -> 1*
       f_1(5, 8) -> 1*
       f_1(5, 5) -> 1*
       f_1(5, 4) -> 1*
       f_1(5, 1) -> 1*
       f_1(4, 9) -> 1*
       f_1(4, 8) -> 1*
       f_1(4, 5) -> 1*
       f_1(4, 4) -> 1*
       f_1(4, 1) -> 1*
       f_1(1, 9) -> 1*
       f_1(1, 8) -> 1*
       f_1(1, 5) -> 1*
       f_1(1, 4) -> 1*
       f_1(1, 1) -> 1*
       f_0(9, 9) -> 1*
       f_0(9, 8) -> 1*
       f_0(9, 5) -> 1*
       f_0(9, 4) -> 1*
       f_0(9, 1) -> 1*
       f_0(8, 9) -> 1*
       f_0(8, 8) -> 1*
       f_0(8, 5) -> 1*
       f_0(8, 4) -> 1*
       f_0(8, 1) -> 1*
       f_0(5, 9) -> 1*
       f_0(5, 8) -> 1*
       f_0(5, 5) -> 1*
       f_0(5, 4) -> 1*
       f_0(5, 1) -> 1*
       f_0(4, 9) -> 1*
       f_0(4, 8) -> 1*
       f_0(4, 5) -> 1*
       f_0(4, 4) -> 1*
       f_0(4, 1) -> 1*
       f_0(1, 9) -> 1*
       f_0(1, 8) -> 1*
       f_0(1, 5) -> 1*
       f_0(1, 4) -> 1*
       f_0(1, 1) -> 1*
               9 -> 1*
               8 -> 1*
               5 -> 1*
               4 -> 1*}
  Strict:
   {}
  Qed