YES
TRS:
 {          d(x) -> if(le(x, s(s(s(s(s(s(s(s(s(0())))))))))), x),
        digits() -> d(0()),
   if(true(), x) -> cons(x, d(s(x))),
  if(false(), x) -> nil(),
      le(0(), y) -> true(),
   le(s(x), 0()) -> false(),
  le(s(x), s(y)) -> le(x, y)}
 DP:
  Strict:
   {          d#(x) -> if#(le(x, s(s(s(s(s(s(s(s(s(0())))))))))), x),
              d#(x) -> le#(x, s(s(s(s(s(s(s(s(s(0())))))))))),
          digits#() -> d#(0()),
     if#(true(), x) -> d#(s(x)),
    le#(s(x), s(y)) -> le#(x, y)}
  Weak:
  {          d(x) -> if(le(x, s(s(s(s(s(s(s(s(s(0())))))))))), x),
         digits() -> d(0()),
    if(true(), x) -> cons(x, d(s(x))),
   if(false(), x) -> nil(),
       le(0(), y) -> true(),
    le(s(x), 0()) -> false(),
   le(s(x), s(y)) -> le(x, y)}
  EDG:
   {(d#(x) -> if#(le(x, s(s(s(s(s(s(s(s(s(0())))))))))), x), if#(true(), x) -> d#(s(x)))
    (d#(x) -> le#(x, s(s(s(s(s(s(s(s(s(0())))))))))), le#(s(x), s(y)) -> le#(x, y))
    (if#(true(), x) -> d#(s(x)), d#(x) -> if#(le(x, s(s(s(s(s(s(s(s(s(0())))))))))), x))
    (if#(true(), x) -> d#(s(x)), d#(x) -> le#(x, s(s(s(s(s(s(s(s(s(0())))))))))))
    (digits#() -> d#(0()), d#(x) -> if#(le(x, s(s(s(s(s(s(s(s(s(0())))))))))), x))
    (digits#() -> d#(0()), d#(x) -> le#(x, s(s(s(s(s(s(s(s(s(0())))))))))))
    (le#(s(x), s(y)) -> le#(x, y), le#(s(x), s(y)) -> le#(x, y))}
   SCCS:
    Scc:
     {le#(s(x), s(y)) -> le#(x, y)}
    Scc:
     {         d#(x) -> if#(le(x, s(s(s(s(s(s(s(s(s(0())))))))))), x),
      if#(true(), x) -> d#(s(x))}
    SCC:
     Strict:
      {le#(s(x), s(y)) -> le#(x, y)}
     Weak:
     {          d(x) -> if(le(x, s(s(s(s(s(s(s(s(s(0())))))))))), x),
            digits() -> d(0()),
       if(true(), x) -> cons(x, d(s(x))),
      if(false(), x) -> nil(),
          le(0(), y) -> true(),
       le(s(x), 0()) -> false(),
      le(s(x), s(y)) -> le(x, y)}
     SPSC:
      Simple Projection:
       pi(le#) = 0
      Strict:
       {}
      Qed
    SCC:
     Strict:
      {         d#(x) -> if#(le(x, s(s(s(s(s(s(s(s(s(0())))))))))), x),
       if#(true(), x) -> d#(s(x))}
     Weak:
     {          d(x) -> if(le(x, s(s(s(s(s(s(s(s(s(0())))))))))), x),
            digits() -> d(0()),
       if(true(), x) -> cons(x, d(s(x))),
      if(false(), x) -> nil(),
          le(0(), y) -> true(),
       le(s(x), 0()) -> false(),
      le(s(x), s(y)) -> le(x, y)}
     UR:
      {    le(0(), y) -> true(),
        le(s(x), 0()) -> false(),
       le(s(x), s(y)) -> le(x, y),
              a(z, w) -> z,
              a(z, w) -> w}
      BOUND:
       Bound: top(-raise)-DP-bounded by 9
       Automaton:
        {    a_0(16, 16) -> 11*
             a_0(16, 15) -> 11*
             a_0(16, 14) -> 11*
             a_0(16, 13) -> 11*
             a_0(16, 11) -> 11*
             a_0(16, 10) -> 11*
             a_0(15, 16) -> 11*
             a_0(15, 15) -> 11*
             a_0(15, 14) -> 11*
             a_0(15, 13) -> 11*
             a_0(15, 11) -> 11*
             a_0(15, 10) -> 11*
             a_0(14, 16) -> 11*
             a_0(14, 15) -> 11*
             a_0(14, 14) -> 11*
             a_0(14, 13) -> 11*
             a_0(14, 11) -> 11*
             a_0(14, 10) -> 11*
             a_0(13, 16) -> 11*
             a_0(13, 15) -> 11*
             a_0(13, 14) -> 11*
             a_0(13, 13) -> 11*
             a_0(13, 11) -> 11*
             a_0(13, 10) -> 11*
             a_0(11, 16) -> 11*
             a_0(11, 15) -> 11*
             a_0(11, 14) -> 11*
             a_0(11, 13) -> 11*
             a_0(11, 11) -> 11*
             a_0(11, 10) -> 11*
             a_0(10, 16) -> 11*
             a_0(10, 15) -> 11*
             a_0(10, 14) -> 11*
             a_0(10, 13) -> 11*
             a_0(10, 11) -> 11*
             a_0(10, 10) -> 11*
               false_9() -> 124*
               false_8() -> 112*
               false_7() -> 100*
               false_6() -> 88*
               false_5() -> 76*
               false_4() -> 64*
               false_3() -> 52*
               false_2() -> 40*
               false_1() -> 28*
               false_0() -> 15 | 10
                true_8() -> 112*
                true_7() -> 100*
                true_6() -> 88*
                true_5() -> 76*
                true_4() -> 64*
                true_3() -> 52*
                true_2() -> 40*
                true_1() -> 28*
                true_0() -> 14 | 10
                s_9(122) -> 123*
                s_9(121) -> 122*
                s_9(120) -> 121*
                s_9(119) -> 120*
                s_9(118) -> 119*
                s_9(117) -> 118*
                s_9(116) -> 117*
                s_9(115) -> 116*
                s_9(114) -> 115*
                s_9(101) -> 113*
                s_8(110) -> 111*
                s_8(109) -> 110*
                s_8(108) -> 109*
                s_8(107) -> 108*
                s_8(106) -> 107*
                s_8(105) -> 106*
                s_8(104) -> 105*
                s_8(103) -> 104*
                s_8(102) -> 103*
                 s_8(89) -> 101*
                 s_7(98) -> 99*
                 s_7(97) -> 98*
                 s_7(96) -> 97*
                 s_7(95) -> 96*
                 s_7(94) -> 95*
                 s_7(93) -> 94*
                 s_7(92) -> 93*
                 s_7(91) -> 92*
                 s_7(90) -> 91*
                 s_7(77) -> 89*
                 s_6(86) -> 87*
                 s_6(85) -> 86*
                 s_6(84) -> 85*
                 s_6(83) -> 84*
                 s_6(82) -> 83*
                 s_6(81) -> 82*
                 s_6(80) -> 81*
                 s_6(79) -> 80*
                 s_6(78) -> 79*
                 s_6(65) -> 77*
                 s_5(74) -> 75*
                 s_5(73) -> 74*
                 s_5(72) -> 73*
                 s_5(71) -> 72*
                 s_5(70) -> 71*
                 s_5(69) -> 70*
                 s_5(68) -> 69*
                 s_5(67) -> 68*
                 s_5(66) -> 67*
                 s_5(53) -> 65*
                 s_4(62) -> 63*
                 s_4(61) -> 62*
                 s_4(60) -> 61*
                 s_4(59) -> 60*
                 s_4(58) -> 59*
                 s_4(57) -> 58*
                 s_4(56) -> 57*
                 s_4(55) -> 56*
                 s_4(54) -> 55*
                 s_4(41) -> 53*
                 s_3(50) -> 51*
                 s_3(49) -> 50*
                 s_3(48) -> 49*
                 s_3(47) -> 48*
                 s_3(46) -> 47*
                 s_3(45) -> 46*
                 s_3(44) -> 45*
                 s_3(43) -> 44*
                 s_3(42) -> 43*
                 s_3(29) -> 41*
                 s_2(38) -> 39*
                 s_2(37) -> 38*
                 s_2(36) -> 37*
                 s_2(35) -> 36*
                 s_2(34) -> 35*
                 s_2(33) -> 34*
                 s_2(32) -> 33*
                 s_2(31) -> 32*
                 s_2(30) -> 31*
                 s_2(17) -> 29*
                 s_1(26) -> 27*
                 s_1(25) -> 26*
                 s_1(24) -> 25*
                 s_1(23) -> 24*
                 s_1(22) -> 23*
                 s_1(21) -> 22*
                 s_1(20) -> 21*
                 s_1(19) -> 20*
                 s_1(18) -> 19*
                 s_1(16) -> 17*
                 s_0(16) -> 16*
                 s_0(15) -> 16*
                 s_0(14) -> 16*
                 s_0(13) -> 16*
                 s_0(11) -> 16*
                 s_0(10) -> 16*
          le_9(113, 123) -> 124*
          le_9(101, 122) -> 124*
           le_9(89, 121) -> 124*
           le_9(77, 120) -> 124*
           le_9(65, 119) -> 124*
           le_9(53, 118) -> 124*
           le_9(41, 117) -> 124*
           le_9(29, 116) -> 124*
           le_9(17, 115) -> 124*
           le_9(16, 114) -> 124*
          le_8(101, 111) -> 112*
           le_8(89, 110) -> 112*
           le_8(77, 109) -> 112*
           le_8(65, 108) -> 112*
           le_8(53, 107) -> 112*
           le_8(41, 106) -> 112*
           le_8(29, 105) -> 112*
           le_8(17, 104) -> 112*
           le_8(16, 103) -> 112*
           le_8(11, 102) -> 112*
           le_8(10, 102) -> 112*
            le_7(89, 99) -> 100*
            le_7(77, 98) -> 100*
            le_7(65, 97) -> 100*
            le_7(53, 96) -> 100*
            le_7(41, 95) -> 100*
            le_7(29, 94) -> 100*
            le_7(17, 93) -> 100*
            le_7(16, 92) -> 100*
            le_7(11, 91) -> 100*
            le_7(11, 90) -> 100*
            le_7(10, 91) -> 100*
            le_7(10, 90) -> 100*
            le_6(77, 87) -> 88*
            le_6(65, 86) -> 88*
            le_6(53, 85) -> 88*
            le_6(41, 84) -> 88*
            le_6(29, 83) -> 88*
            le_6(17, 82) -> 88*
            le_6(16, 81) -> 88*
            le_6(11, 80) -> 88*
            le_6(11, 79) -> 88*
            le_6(11, 78) -> 88*
            le_6(10, 80) -> 88*
            le_6(10, 79) -> 88*
            le_6(10, 78) -> 88*
            le_5(65, 75) -> 76*
            le_5(53, 74) -> 76*
            le_5(41, 73) -> 76*
            le_5(29, 72) -> 76*
            le_5(17, 71) -> 76*
            le_5(16, 70) -> 76*
            le_5(11, 69) -> 76*
            le_5(11, 68) -> 76*
            le_5(11, 67) -> 76*
            le_5(11, 66) -> 76*
            le_5(10, 69) -> 76*
            le_5(10, 68) -> 76*
            le_5(10, 67) -> 76*
            le_5(10, 66) -> 76*
            le_4(53, 63) -> 64*
            le_4(41, 62) -> 64*
            le_4(29, 61) -> 64*
            le_4(17, 60) -> 64*
            le_4(16, 59) -> 64*
            le_4(11, 58) -> 64*
            le_4(11, 57) -> 64*
            le_4(11, 56) -> 64*
            le_4(11, 55) -> 64*
            le_4(11, 54) -> 64*
            le_4(10, 58) -> 64*
            le_4(10, 57) -> 64*
            le_4(10, 56) -> 64*
            le_4(10, 55) -> 64*
            le_4(10, 54) -> 64*
            le_3(41, 51) -> 52*
            le_3(29, 50) -> 52*
            le_3(17, 49) -> 52*
            le_3(16, 48) -> 52*
            le_3(11, 47) -> 52*
            le_3(11, 46) -> 52*
            le_3(11, 45) -> 52*
            le_3(11, 44) -> 52*
            le_3(11, 43) -> 52*
            le_3(11, 42) -> 52*
            le_3(10, 47) -> 52*
            le_3(10, 46) -> 52*
            le_3(10, 45) -> 52*
            le_3(10, 44) -> 52*
            le_3(10, 43) -> 52*
            le_3(10, 42) -> 52*
            le_2(29, 39) -> 40*
            le_2(17, 38) -> 40*
            le_2(16, 37) -> 40*
            le_2(11, 36) -> 40*
            le_2(11, 35) -> 40*
            le_2(11, 34) -> 40*
            le_2(11, 33) -> 40*
            le_2(11, 32) -> 40*
            le_2(11, 31) -> 40*
            le_2(11, 30) -> 40*
            le_2(10, 36) -> 40*
            le_2(10, 35) -> 40*
            le_2(10, 34) -> 40*
            le_2(10, 33) -> 40*
            le_2(10, 32) -> 40*
            le_2(10, 31) -> 40*
            le_2(10, 30) -> 40*
            le_1(17, 27) -> 28*
            le_1(16, 26) -> 28*
            le_1(11, 25) -> 28*
            le_1(11, 24) -> 28*
            le_1(11, 23) -> 28*
            le_1(11, 22) -> 28*
            le_1(11, 21) -> 28*
            le_1(11, 20) -> 28*
            le_1(11, 19) -> 28*
            le_1(11, 18) -> 28*
            le_1(10, 25) -> 28*
            le_1(10, 24) -> 28*
            le_1(10, 23) -> 28*
            le_1(10, 22) -> 28*
            le_1(10, 21) -> 28*
            le_1(10, 20) -> 28*
            le_1(10, 19) -> 28*
            le_1(10, 18) -> 28*
            le_0(16, 16) -> 10*
            le_0(16, 15) -> 10*
            le_0(16, 14) -> 10*
            le_0(16, 13) -> 10*
            le_0(16, 11) -> 10*
            le_0(16, 10) -> 10*
            le_0(15, 16) -> 10*
            le_0(15, 15) -> 10*
            le_0(15, 14) -> 10*
            le_0(15, 13) -> 10*
            le_0(15, 11) -> 10*
            le_0(15, 10) -> 10*
            le_0(14, 16) -> 10*
            le_0(14, 15) -> 10*
            le_0(14, 14) -> 10*
            le_0(14, 13) -> 10*
            le_0(14, 11) -> 10*
            le_0(14, 10) -> 10*
            le_0(13, 16) -> 10*
            le_0(13, 15) -> 10*
            le_0(13, 14) -> 10*
            le_0(13, 13) -> 10*
            le_0(13, 11) -> 10*
            le_0(13, 10) -> 10*
            le_0(11, 16) -> 10*
            le_0(11, 15) -> 10*
            le_0(11, 14) -> 10*
            le_0(11, 13) -> 10*
            le_0(11, 11) -> 10*
            le_0(11, 10) -> 10*
            le_0(10, 16) -> 10*
            le_0(10, 15) -> 10*
            le_0(10, 14) -> 10*
            le_0(10, 13) -> 10*
            le_0(10, 11) -> 10*
            le_0(10, 10) -> 10*
         if#_9(124, 113) -> 8*
         if#_8(112, 101) -> 8*
          if#_7(100, 89) -> 8*
           if#_6(88, 77) -> 8*
           if#_5(76, 65) -> 8*
           if#_4(64, 53) -> 8*
           if#_3(52, 41) -> 8*
           if#_2(40, 29) -> 8*
           if#_1(28, 17) -> 8*
           if#_0(10, 16) -> 8*
                   0_9() -> 114*
                   0_8() -> 102*
                   0_7() -> 90*
                   0_6() -> 78*
                   0_5() -> 66*
                   0_4() -> 54*
                   0_3() -> 42*
                   0_2() -> 30*
                   0_1() -> 18*
                   0_0() -> 13*
               d#_9(113) -> 8*
               d#_8(101) -> 8*
                d#_7(89) -> 8*
                d#_6(77) -> 8*
                d#_5(65) -> 8*
                d#_4(53) -> 8*
                d#_3(41) -> 8*
                d#_2(29) -> 8*
                d#_1(17) -> 8*
                d#_0(16) -> 8*
                      16 -> 11*
                      15 -> 11*
                      14 -> 11*
                      13 -> 11*
                      10 -> 11*}
       Strict:
        {d#(x) -> if#(le(x, s(s(s(s(s(s(s(s(s(0())))))))))), x)}
       EDG:
        {}
        SCCS:
         
         Qed