YES
Time: 0.302786
TRS:
 {  f(X, X) -> c X,
  f(X, c X) -> f(s X, X),
  f(s X, X) -> f(X, a X)}
 BOUND:
  Bound: top(-raise)-bounded by 4
  Automaton:
   {
        c_4(35) -> 1*
        c_4(34) -> 1*
        c_4(33) -> 1*
        c_4(29) -> 1*
        c_4(28) -> 1*
        c_4(27) -> 1*
        c_4(23) -> 1*
        c_3(30) -> 1*
        c_3(26) -> 1*
        c_3(25) -> 1*
        c_3(24) -> 1*
        c_3(22) -> 1*
        c_3(15) -> 1*
        c_3(14) -> 1*
        c_3(13) -> 1*
        c_3(11) -> 1*
        c_3(10) -> 1*
        c_2(12) -> 1*
         c_2(5) -> 1*
         c_2(4) -> 1*
         c_1(1) -> 1*
        s_2(11) -> 11* | 9 | 4 | 3 | 1
         s_2(4) -> 11* | 9 | 4 | 3 | 1
        s_1(35) -> 4* | 3 | 1
        s_1(34) -> 4* | 3 | 1
        s_1(33) -> 4* | 3 | 1
        s_1(30) -> 4* | 3 | 1
        s_1(29) -> 4* | 3 | 1
        s_1(28) -> 4* | 3 | 1
        s_1(27) -> 4* | 3 | 1
        s_1(26) -> 4* | 3 | 1
        s_1(25) -> 4* | 3 | 1
        s_1(24) -> 4* | 3 | 1
        s_1(23) -> 4* | 3 | 1
        s_1(22) -> 4* | 3 | 1
        s_1(15) -> 4* | 3 | 1
        s_1(14) -> 4* | 3 | 1
        s_1(13) -> 4* | 3 | 1
        s_1(12) -> 4* | 3 | 1
        s_1(10) -> 4* | 3 | 1
         s_1(5) -> 4* | 3 | 1
         s_1(1) -> 4* | 3 | 1
        a_4(30) -> 35* | 34 | 33 | 32 | 31 | 28 | 26 | 25 | 23 | 20 | 19 | 17 | 15 | 13 | 10 | 8 | 6 | 5 | 2 | 1
        a_4(22) -> 33* | 31 | 28 | 26 | 25 | 23 | 20 | 19 | 17 | 15 | 13 | 10 | 8 | 6 | 5 | 2 | 1
        a_3(35) -> 29* | 27 | 23 | 21 | 17 | 15 | 13 | 10 | 8 | 6 | 5 | 2 | 1
        a_3(34) -> 29* | 27 | 23 | 21 | 17 | 15 | 13 | 10 | 8 | 6 | 5 | 2 | 1
        a_3(33) -> 29* | 27 | 23 | 21 | 17 | 15 | 13 | 10 | 8 | 6 | 5 | 2 | 1
        a_3(29) -> 29* | 27 | 23 | 21 | 17 | 15 | 13 | 10 | 8 | 6 | 5 | 2 | 1
        a_3(28) -> 29* | 27 | 23 | 21 | 17 | 15 | 13 | 10 | 8 | 6 | 5 | 2 | 1
        a_3(27) -> 29* | 27 | 23 | 21 | 17 | 15 | 13 | 10 | 8 | 6 | 5 | 2 | 1
        a_3(26) -> 29* | 27 | 23 | 21 | 17 | 15 | 13 | 10 | 8 | 6 | 5 | 2 | 1
        a_3(25) -> 29* | 27 | 23 | 21 | 17 | 15 | 13 | 10 | 8 | 6 | 5 | 2 | 1
        a_3(24) -> 28* | 26 | 25 | 23 | 20 | 19 | 17 | 15 | 13 | 10 | 8 | 6 | 5 | 2 | 1
        a_3(23) -> 29* | 27 | 23 | 21 | 17 | 15 | 13 | 10 | 8 | 6 | 5 | 2 | 1
        a_3(15) -> 29* | 27 | 23 | 21 | 17 | 15 | 13 | 10 | 8 | 6 | 5 | 2 | 1
        a_3(14) -> 26* | 20 | 15 | 13 | 10 | 8 | 6 | 5 | 2 | 1
        a_3(12) -> 25* | 19 | 15 | 13 | 10 | 8 | 6 | 5 | 2 | 1
        a_3(11) -> 30* | 24 | 22 | 18 | 16 | 14 | 12 | 10 | 7 | 6 | 5 | 2 | 1
        a_3(10) -> 23* | 17 | 15 | 13 | 10 | 8 | 6 | 5 | 2 | 1
         a_3(4) -> 22* | 16 | 14 | 12 | 10 | 7 | 6 | 5 | 2 | 1
        a_2(13) -> 15* | 13 | 10 | 8 | 6 | 5 | 2 | 1
         a_2(5) -> 13* | 8 | 5 | 2 | 1
         a_2(1) -> 10* | 6 | 5 | 2 | 1
    f_4(30, 35) -> 1*
    f_4(30, 34) -> 1*
    f_4(30, 33) -> 1*
    f_4(30, 32) -> 1*
    f_4(30, 31) -> 1*
    f_4(22, 35) -> 1*
    f_4(22, 33) -> 1*
    f_4(22, 31) -> 1*
    f_3(35, 35) -> 1*
    f_3(35, 34) -> 1*
    f_3(35, 33) -> 1*
    f_3(35, 29) -> 1*
    f_3(35, 28) -> 1*
    f_3(35, 27) -> 1*
    f_3(35, 23) -> 1*
    f_3(35, 21) -> 1*
    f_3(35, 17) -> 1*
    f_3(34, 35) -> 1*
    f_3(34, 34) -> 1*
    f_3(34, 33) -> 1*
    f_3(34, 29) -> 1*
    f_3(34, 28) -> 1*
    f_3(34, 27) -> 1*
    f_3(34, 23) -> 1*
    f_3(34, 21) -> 1*
    f_3(34, 17) -> 1*
    f_3(33, 35) -> 1*
    f_3(33, 34) -> 1*
    f_3(33, 33) -> 1*
    f_3(33, 29) -> 1*
    f_3(33, 28) -> 1*
    f_3(33, 27) -> 1*
    f_3(33, 23) -> 1*
    f_3(33, 21) -> 1*
    f_3(33, 17) -> 1*
    f_3(30, 29) -> 1*
    f_3(30, 28) -> 1*
    f_3(30, 26) -> 1*
    f_3(30, 25) -> 1*
    f_3(30, 23) -> 1*
    f_3(30, 20) -> 1*
    f_3(30, 19) -> 1*
    f_3(30, 17) -> 1*
    f_3(29, 35) -> 1*
    f_3(29, 34) -> 1*
    f_3(29, 33) -> 1*
    f_3(29, 29) -> 1*
    f_3(29, 28) -> 1*
    f_3(29, 27) -> 1*
    f_3(29, 23) -> 1*
    f_3(29, 21) -> 1*
    f_3(29, 17) -> 1*
    f_3(28, 35) -> 1*
    f_3(28, 34) -> 1*
    f_3(28, 33) -> 1*
    f_3(28, 29) -> 1*
    f_3(28, 28) -> 1*
    f_3(28, 27) -> 1*
    f_3(28, 23) -> 1*
    f_3(28, 21) -> 1*
    f_3(28, 17) -> 1*
    f_3(27, 35) -> 1*
    f_3(27, 34) -> 1*
    f_3(27, 33) -> 1*
    f_3(27, 29) -> 1*
    f_3(27, 28) -> 1*
    f_3(27, 27) -> 1*
    f_3(27, 23) -> 1*
    f_3(27, 21) -> 1*
    f_3(27, 17) -> 1*
    f_3(26, 35) -> 1*
    f_3(26, 34) -> 1*
    f_3(26, 33) -> 1*
    f_3(26, 29) -> 1*
    f_3(26, 28) -> 1*
    f_3(26, 27) -> 1*
    f_3(26, 23) -> 1*
    f_3(26, 21) -> 1*
    f_3(26, 17) -> 1*
    f_3(25, 35) -> 1*
    f_3(25, 34) -> 1*
    f_3(25, 33) -> 1*
    f_3(25, 29) -> 1*
    f_3(25, 28) -> 1*
    f_3(25, 27) -> 1*
    f_3(25, 23) -> 1*
    f_3(25, 21) -> 1*
    f_3(25, 17) -> 1*
    f_3(24, 35) -> 1*
    f_3(24, 34) -> 1*
    f_3(24, 33) -> 1*
    f_3(24, 29) -> 1*
    f_3(24, 28) -> 1*
    f_3(24, 26) -> 1*
    f_3(24, 25) -> 1*
    f_3(24, 23) -> 1*
    f_3(24, 20) -> 1*
    f_3(24, 19) -> 1*
    f_3(24, 17) -> 1*
    f_3(23, 35) -> 1*
    f_3(23, 34) -> 1*
    f_3(23, 33) -> 1*
    f_3(23, 29) -> 1*
    f_3(23, 28) -> 1*
    f_3(23, 27) -> 1*
    f_3(23, 23) -> 1*
    f_3(23, 21) -> 1*
    f_3(23, 17) -> 1*
    f_3(22, 34) -> 1*
    f_3(22, 29) -> 1*
    f_3(22, 28) -> 1*
    f_3(22, 26) -> 1*
    f_3(22, 25) -> 1*
    f_3(22, 23) -> 1*
    f_3(22, 20) -> 1*
    f_3(22, 19) -> 1*
    f_3(22, 17) -> 1*
    f_3(15, 35) -> 1*
    f_3(15, 34) -> 1*
    f_3(15, 33) -> 1*
    f_3(15, 29) -> 1*
    f_3(15, 28) -> 1*
    f_3(15, 27) -> 1*
    f_3(15, 23) -> 1*
    f_3(15, 21) -> 1*
    f_3(15, 17) -> 1*
    f_3(14, 35) -> 1*
    f_3(14, 34) -> 1*
    f_3(14, 33) -> 1*
    f_3(14, 28) -> 1*
    f_3(14, 26) -> 1*
    f_3(14, 20) -> 1*
    f_3(12, 35) -> 1*
    f_3(12, 34) -> 1*
    f_3(12, 33) -> 1*
    f_3(12, 28) -> 1*
    f_3(12, 25) -> 1*
    f_3(12, 19) -> 1*
    f_3(11, 30) -> 1*
    f_3(11, 24) -> 1*
    f_3(11, 22) -> 1*
    f_3(11, 18) -> 1*
    f_3(11, 16) -> 1*
    f_3(10, 35) -> 1*
    f_3(10, 34) -> 1*
    f_3(10, 33) -> 1*
    f_3(10, 29) -> 1*
    f_3(10, 28) -> 1*
    f_3(10, 23) -> 1*
    f_3(10, 17) -> 1*
     f_3(4, 30) -> 1*
     f_3(4, 22) -> 1*
     f_3(4, 16) -> 1*
    f_2(35, 30) -> 1*
    f_2(35, 26) -> 1*
    f_2(35, 25) -> 1*
    f_2(35, 24) -> 1*
    f_2(35, 22) -> 1*
    f_2(35, 15) -> 1*
    f_2(35, 14) -> 1*
    f_2(35, 13) -> 1*
    f_2(35, 10) -> 1*
     f_2(35, 8) -> 1*
     f_2(35, 6) -> 1*
    f_2(34, 30) -> 1*
    f_2(34, 26) -> 1*
    f_2(34, 25) -> 1*
    f_2(34, 24) -> 1*
    f_2(34, 22) -> 1*
    f_2(34, 15) -> 1*
    f_2(34, 14) -> 1*
    f_2(34, 13) -> 1*
    f_2(34, 10) -> 1*
     f_2(34, 8) -> 1*
     f_2(34, 6) -> 1*
    f_2(33, 30) -> 1*
    f_2(33, 26) -> 1*
    f_2(33, 25) -> 1*
    f_2(33, 24) -> 1*
    f_2(33, 22) -> 1*
    f_2(33, 15) -> 1*
    f_2(33, 14) -> 1*
    f_2(33, 13) -> 1*
    f_2(33, 10) -> 1*
     f_2(33, 8) -> 1*
     f_2(33, 6) -> 1*
    f_2(30, 30) -> 1*
    f_2(30, 27) -> 1*
    f_2(30, 24) -> 1*
    f_2(30, 22) -> 1*
    f_2(30, 15) -> 1*
    f_2(30, 14) -> 1*
    f_2(30, 13) -> 1*
    f_2(30, 10) -> 1*
     f_2(30, 8) -> 1*
     f_2(30, 6) -> 1*
    f_2(29, 30) -> 1*
    f_2(29, 26) -> 1*
    f_2(29, 25) -> 1*
    f_2(29, 24) -> 1*
    f_2(29, 22) -> 1*
    f_2(29, 15) -> 1*
    f_2(29, 14) -> 1*
    f_2(29, 13) -> 1*
    f_2(29, 10) -> 1*
     f_2(29, 8) -> 1*
     f_2(29, 6) -> 1*
    f_2(28, 30) -> 1*
    f_2(28, 26) -> 1*
    f_2(28, 25) -> 1*
    f_2(28, 24) -> 1*
    f_2(28, 22) -> 1*
    f_2(28, 15) -> 1*
    f_2(28, 14) -> 1*
    f_2(28, 13) -> 1*
    f_2(28, 10) -> 1*
     f_2(28, 8) -> 1*
     f_2(28, 6) -> 1*
    f_2(27, 30) -> 1*
    f_2(27, 26) -> 1*
    f_2(27, 25) -> 1*
    f_2(27, 24) -> 1*
    f_2(27, 22) -> 1*
    f_2(27, 15) -> 1*
    f_2(27, 14) -> 1*
    f_2(27, 13) -> 1*
    f_2(27, 10) -> 1*
     f_2(27, 8) -> 1*
     f_2(27, 6) -> 1*
    f_2(26, 30) -> 1*
    f_2(26, 26) -> 1*
    f_2(26, 25) -> 1*
    f_2(26, 24) -> 1*
    f_2(26, 22) -> 1*
    f_2(26, 15) -> 1*
    f_2(26, 14) -> 1*
    f_2(26, 13) -> 1*
    f_2(26, 10) -> 1*
     f_2(26, 8) -> 1*
     f_2(26, 6) -> 1*
    f_2(25, 30) -> 1*
    f_2(25, 26) -> 1*
    f_2(25, 25) -> 1*
    f_2(25, 24) -> 1*
    f_2(25, 22) -> 1*
    f_2(25, 15) -> 1*
    f_2(25, 14) -> 1*
    f_2(25, 13) -> 1*
    f_2(25, 10) -> 1*
     f_2(25, 8) -> 1*
     f_2(25, 6) -> 1*
    f_2(24, 30) -> 1*
    f_2(24, 27) -> 1*
    f_2(24, 24) -> 1*
    f_2(24, 22) -> 1*
    f_2(24, 15) -> 1*
    f_2(24, 14) -> 1*
    f_2(24, 13) -> 1*
    f_2(24, 10) -> 1*
     f_2(24, 8) -> 1*
     f_2(24, 6) -> 1*
    f_2(23, 30) -> 1*
    f_2(23, 26) -> 1*
    f_2(23, 25) -> 1*
    f_2(23, 24) -> 1*
    f_2(23, 22) -> 1*
    f_2(23, 15) -> 1*
    f_2(23, 14) -> 1*
    f_2(23, 13) -> 1*
    f_2(23, 10) -> 1*
     f_2(23, 8) -> 1*
     f_2(23, 6) -> 1*
    f_2(22, 30) -> 1*
    f_2(22, 27) -> 1*
    f_2(22, 24) -> 1*
    f_2(22, 22) -> 1*
    f_2(22, 15) -> 1*
    f_2(22, 14) -> 1*
    f_2(22, 13) -> 1*
    f_2(22, 10) -> 1*
     f_2(22, 8) -> 1*
     f_2(22, 6) -> 1*
    f_2(15, 30) -> 1*
    f_2(15, 26) -> 1*
    f_2(15, 25) -> 1*
    f_2(15, 24) -> 1*
    f_2(15, 22) -> 1*
    f_2(15, 15) -> 1*
    f_2(15, 14) -> 1*
    f_2(15, 13) -> 1*
    f_2(15, 10) -> 1*
     f_2(15, 8) -> 1*
     f_2(15, 6) -> 1*
    f_2(14, 30) -> 1*
    f_2(14, 29) -> 1*
    f_2(14, 27) -> 1*
    f_2(14, 25) -> 1*
    f_2(14, 24) -> 1*
    f_2(14, 23) -> 1*
    f_2(14, 22) -> 1*
    f_2(14, 15) -> 1*
    f_2(14, 14) -> 1*
    f_2(14, 13) -> 1*
    f_2(14, 10) -> 1*
     f_2(14, 8) -> 1*
     f_2(14, 6) -> 1*
    f_2(13, 35) -> 1*
    f_2(13, 34) -> 1*
    f_2(13, 33) -> 1*
    f_2(13, 30) -> 1*
    f_2(13, 29) -> 1*
    f_2(13, 28) -> 1*
    f_2(13, 27) -> 1*
    f_2(13, 26) -> 1*
    f_2(13, 25) -> 1*
    f_2(13, 24) -> 1*
    f_2(13, 23) -> 1*
    f_2(13, 22) -> 1*
    f_2(13, 15) -> 1*
    f_2(13, 14) -> 1*
    f_2(13, 13) -> 1*
    f_2(13, 10) -> 1*
     f_2(13, 8) -> 1*
     f_2(13, 6) -> 1*
    f_2(12, 30) -> 1*
    f_2(12, 29) -> 1*
    f_2(12, 27) -> 1*
    f_2(12, 26) -> 1*
    f_2(12, 24) -> 1*
    f_2(12, 23) -> 1*
    f_2(12, 22) -> 1*
    f_2(12, 15) -> 1*
    f_2(12, 14) -> 1*
    f_2(12, 13) -> 1*
    f_2(12, 10) -> 1*
     f_2(12, 8) -> 1*
     f_2(12, 6) -> 1*
    f_2(11, 35) -> 1*
    f_2(11, 34) -> 1*
    f_2(11, 33) -> 1*
    f_2(11, 29) -> 1*
    f_2(11, 28) -> 1*
    f_2(11, 27) -> 1*
    f_2(11, 26) -> 1*
    f_2(11, 25) -> 1*
    f_2(11, 23) -> 1*
    f_2(11, 15) -> 1*
    f_2(11, 14) -> 1*
    f_2(11, 12) -> 1*
    f_2(11, 11) -> 1*
    f_2(11, 10) -> 1*
     f_2(11, 7) -> 1*
     f_2(11, 6) -> 1*
     f_2(11, 4) -> 1*
    f_2(10, 30) -> 1*
    f_2(10, 27) -> 1*
    f_2(10, 26) -> 1*
    f_2(10, 25) -> 1*
    f_2(10, 24) -> 1*
    f_2(10, 22) -> 1*
    f_2(10, 15) -> 1*
    f_2(10, 14) -> 1*
    f_2(10, 13) -> 1*
    f_2(10, 10) -> 1*
     f_2(10, 8) -> 1*
     f_2(10, 6) -> 1*
     f_2(9, 11) -> 1*
      f_2(9, 4) -> 1*
     f_2(5, 35) -> 1*
     f_2(5, 34) -> 1*
     f_2(5, 33) -> 1*
     f_2(5, 29) -> 1*
     f_2(5, 28) -> 1*
     f_2(5, 27) -> 1*
     f_2(5, 26) -> 1*
     f_2(5, 25) -> 1*
     f_2(5, 23) -> 1*
     f_2(5, 15) -> 1*
     f_2(5, 13) -> 1*
      f_2(5, 8) -> 1*
     f_2(4, 35) -> 1*
     f_2(4, 34) -> 1*
     f_2(4, 33) -> 1*
     f_2(4, 29) -> 1*
     f_2(4, 28) -> 1*
     f_2(4, 27) -> 1*
     f_2(4, 26) -> 1*
     f_2(4, 25) -> 1*
     f_2(4, 24) -> 1*
     f_2(4, 23) -> 1*
     f_2(4, 15) -> 1*
     f_2(4, 14) -> 1*
     f_2(4, 12) -> 1*
     f_2(4, 10) -> 1*
      f_2(4, 7) -> 1*
      f_2(4, 6) -> 1*
     f_2(1, 35) -> 1*
     f_2(1, 34) -> 1*
     f_2(1, 33) -> 1*
     f_2(1, 30) -> 1*
     f_2(1, 29) -> 1*
     f_2(1, 28) -> 1*
     f_2(1, 27) -> 1*
     f_2(1, 26) -> 1*
     f_2(1, 25) -> 1*
     f_2(1, 24) -> 1*
     f_2(1, 23) -> 1*
     f_2(1, 22) -> 1*
     f_2(1, 15) -> 1*
     f_2(1, 14) -> 1*
     f_2(1, 10) -> 1*
      f_2(1, 6) -> 1*
    f_1(35, 12) -> 1*
     f_1(35, 5) -> 1*
     f_1(35, 2) -> 1*
    f_1(34, 12) -> 1*
     f_1(34, 5) -> 1*
     f_1(34, 2) -> 1*
    f_1(33, 12) -> 1*
     f_1(33, 5) -> 1*
     f_1(33, 2) -> 1*
    f_1(30, 12) -> 1*
     f_1(30, 5) -> 1*
     f_1(30, 2) -> 1*
    f_1(29, 12) -> 1*
     f_1(29, 5) -> 1*
     f_1(29, 2) -> 1*
    f_1(28, 12) -> 1*
     f_1(28, 5) -> 1*
     f_1(28, 2) -> 1*
    f_1(27, 12) -> 1*
     f_1(27, 5) -> 1*
     f_1(27, 2) -> 1*
    f_1(26, 12) -> 1*
     f_1(26, 5) -> 1*
     f_1(26, 2) -> 1*
    f_1(25, 12) -> 1*
     f_1(25, 5) -> 1*
     f_1(25, 2) -> 1*
    f_1(24, 12) -> 1*
     f_1(24, 5) -> 1*
     f_1(24, 2) -> 1*
    f_1(23, 12) -> 1*
     f_1(23, 5) -> 1*
     f_1(23, 2) -> 1*
    f_1(22, 12) -> 1*
     f_1(22, 5) -> 1*
     f_1(22, 2) -> 1*
    f_1(15, 12) -> 1*
     f_1(15, 5) -> 1*
     f_1(15, 2) -> 1*
    f_1(14, 12) -> 1*
     f_1(14, 5) -> 1*
     f_1(14, 2) -> 1*
    f_1(13, 12) -> 1*
     f_1(13, 5) -> 1*
     f_1(13, 2) -> 1*
    f_1(12, 12) -> 1*
     f_1(12, 5) -> 1*
     f_1(12, 2) -> 1*
    f_1(11, 13) -> 1*
     f_1(11, 5) -> 1*
     f_1(11, 2) -> 1*
     f_1(11, 1) -> 1*
    f_1(10, 12) -> 1*
     f_1(10, 5) -> 1*
     f_1(10, 2) -> 1*
     f_1(5, 30) -> 1*
     f_1(5, 24) -> 1*
     f_1(5, 22) -> 1*
     f_1(5, 14) -> 1*
     f_1(5, 12) -> 1*
     f_1(5, 10) -> 1*
      f_1(5, 5) -> 1*
      f_1(5, 2) -> 1*
     f_1(4, 13) -> 1*
     f_1(4, 11) -> 1*
      f_1(4, 5) -> 1*
      f_1(4, 4) -> 1*
      f_1(4, 2) -> 1*
      f_1(4, 1) -> 1*
     f_1(3, 35) -> 1*
     f_1(3, 34) -> 1*
     f_1(3, 33) -> 1*
     f_1(3, 30) -> 1*
     f_1(3, 29) -> 1*
     f_1(3, 28) -> 1*
     f_1(3, 27) -> 1*
     f_1(3, 26) -> 1*
     f_1(3, 25) -> 1*
     f_1(3, 24) -> 1*
     f_1(3, 23) -> 1*
     f_1(3, 22) -> 1*
     f_1(3, 15) -> 1*
     f_1(3, 14) -> 1*
     f_1(3, 13) -> 1*
     f_1(3, 12) -> 1*
     f_1(3, 11) -> 1*
     f_1(3, 10) -> 1*
      f_1(3, 5) -> 1*
      f_1(3, 4) -> 1*
      f_1(3, 1) -> 1*
     f_1(1, 13) -> 1*
     f_1(1, 12) -> 1*
      f_1(1, 5) -> 1*
      f_1(1, 2) -> 1*
    f_0(35, 11) -> 1*
     f_0(35, 4) -> 1*
     f_0(35, 1) -> 1*
    f_0(34, 11) -> 1*
     f_0(34, 4) -> 1*
     f_0(34, 1) -> 1*
    f_0(33, 11) -> 1*
     f_0(33, 4) -> 1*
     f_0(33, 1) -> 1*
    f_0(30, 11) -> 1*
     f_0(30, 4) -> 1*
     f_0(30, 1) -> 1*
    f_0(29, 11) -> 1*
     f_0(29, 4) -> 1*
     f_0(29, 1) -> 1*
    f_0(28, 11) -> 1*
     f_0(28, 4) -> 1*
     f_0(28, 1) -> 1*
    f_0(27, 11) -> 1*
     f_0(27, 4) -> 1*
     f_0(27, 1) -> 1*
    f_0(26, 11) -> 1*
     f_0(26, 4) -> 1*
     f_0(26, 1) -> 1*
    f_0(25, 11) -> 1*
     f_0(25, 4) -> 1*
     f_0(25, 1) -> 1*
    f_0(24, 11) -> 1*
     f_0(24, 4) -> 1*
     f_0(24, 1) -> 1*
    f_0(23, 11) -> 1*
     f_0(23, 4) -> 1*
     f_0(23, 1) -> 1*
    f_0(22, 11) -> 1*
     f_0(22, 4) -> 1*
     f_0(22, 1) -> 1*
    f_0(15, 11) -> 1*
     f_0(15, 4) -> 1*
     f_0(15, 1) -> 1*
    f_0(14, 11) -> 1*
     f_0(14, 4) -> 1*
     f_0(14, 1) -> 1*
    f_0(13, 11) -> 1*
     f_0(13, 4) -> 1*
     f_0(13, 1) -> 1*
    f_0(12, 11) -> 1*
     f_0(12, 4) -> 1*
     f_0(12, 1) -> 1*
    f_0(10, 11) -> 1*
     f_0(10, 4) -> 1*
     f_0(10, 1) -> 1*
     f_0(5, 11) -> 1*
      f_0(5, 4) -> 1*
      f_0(5, 1) -> 1*
     f_0(1, 11) -> 1*
      f_0(1, 4) -> 1*
      f_0(1, 1) -> 1*
   }
  Strict:
   {}
  Qed