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