YES
TRS:
 {     1024_1(x) -> if(lt(x, 10()), x),
          1024() -> 1024_1(0()),
   if(true(), x) -> double(1024_1(s(x))),
  if(false(), x) -> s(0()),
      lt(x, 0()) -> false(),
   lt(0(), s(y)) -> true(),
  lt(s(x), s(y)) -> lt(x, y),
            10() -> double(s(double(s(s(0()))))),
     double(0()) -> 0(),
    double(s(x)) -> s(s(double(x)))}
 DP:
  Strict:
   {     1024_1#(x) -> if#(lt(x, 10()), x),
         1024_1#(x) -> lt#(x, 10()),
         1024_1#(x) -> 10#(),
            1024#() -> 1024_1#(0()),
     if#(true(), x) -> 1024_1#(s(x)),
     if#(true(), x) -> double#(1024_1(s(x))),
    lt#(s(x), s(y)) -> lt#(x, y),
              10#() -> double#(s(double(s(s(0()))))),
              10#() -> double#(s(s(0()))),
      double#(s(x)) -> double#(x)}
  Weak:
  {     1024_1(x) -> if(lt(x, 10()), x),
           1024() -> 1024_1(0()),
    if(true(), x) -> double(1024_1(s(x))),
   if(false(), x) -> s(0()),
       lt(x, 0()) -> false(),
    lt(0(), s(y)) -> true(),
   lt(s(x), s(y)) -> lt(x, y),
             10() -> double(s(double(s(s(0()))))),
      double(0()) -> 0(),
     double(s(x)) -> s(s(double(x)))}
  EDG:
   {(if#(true(), x) -> 1024_1#(s(x)), 1024_1#(x) -> 10#())
    (if#(true(), x) -> 1024_1#(s(x)), 1024_1#(x) -> lt#(x, 10()))
    (if#(true(), x) -> 1024_1#(s(x)), 1024_1#(x) -> if#(lt(x, 10()), x))
    (1024_1#(x) -> lt#(x, 10()), lt#(s(x), s(y)) -> lt#(x, y))
    (1024_1#(x) -> if#(lt(x, 10()), x), if#(true(), x) -> double#(1024_1(s(x))))
    (1024_1#(x) -> if#(lt(x, 10()), x), if#(true(), x) -> 1024_1#(s(x)))
    (10#() -> double#(s(double(s(s(0()))))), double#(s(x)) -> double#(x))
    (if#(true(), x) -> double#(1024_1(s(x))), double#(s(x)) -> double#(x))
    (10#() -> double#(s(s(0()))), double#(s(x)) -> double#(x))
    (1024#() -> 1024_1#(0()), 1024_1#(x) -> if#(lt(x, 10()), x))
    (1024#() -> 1024_1#(0()), 1024_1#(x) -> lt#(x, 10()))
    (1024#() -> 1024_1#(0()), 1024_1#(x) -> 10#())
    (lt#(s(x), s(y)) -> lt#(x, y), lt#(s(x), s(y)) -> lt#(x, y))
    (1024_1#(x) -> 10#(), 10#() -> double#(s(double(s(s(0()))))))
    (1024_1#(x) -> 10#(), 10#() -> double#(s(s(0()))))
    (double#(s(x)) -> double#(x), double#(s(x)) -> double#(x))}
   SCCS:
    Scc:
     {double#(s(x)) -> double#(x)}
    Scc:
     {lt#(s(x), s(y)) -> lt#(x, y)}
    Scc:
     {    1024_1#(x) -> if#(lt(x, 10()), x),
      if#(true(), x) -> 1024_1#(s(x))}
    SCC:
     Strict:
      {double#(s(x)) -> double#(x)}
     Weak:
     {     1024_1(x) -> if(lt(x, 10()), x),
              1024() -> 1024_1(0()),
       if(true(), x) -> double(1024_1(s(x))),
      if(false(), x) -> s(0()),
          lt(x, 0()) -> false(),
       lt(0(), s(y)) -> true(),
      lt(s(x), s(y)) -> lt(x, y),
                10() -> double(s(double(s(s(0()))))),
         double(0()) -> 0(),
        double(s(x)) -> s(s(double(x)))}
     SPSC:
      Simple Projection:
       pi(double#) = 0
      Strict:
       {}
      Qed
    SCC:
     Strict:
      {lt#(s(x), s(y)) -> lt#(x, y)}
     Weak:
     {     1024_1(x) -> if(lt(x, 10()), x),
              1024() -> 1024_1(0()),
       if(true(), x) -> double(1024_1(s(x))),
      if(false(), x) -> s(0()),
          lt(x, 0()) -> false(),
       lt(0(), s(y)) -> true(),
      lt(s(x), s(y)) -> lt(x, y),
                10() -> double(s(double(s(s(0()))))),
         double(0()) -> 0(),
        double(s(x)) -> s(s(double(x)))}
     SPSC:
      Simple Projection:
       pi(lt#) = 0
      Strict:
       {}
      Qed
    SCC:
     Strict:
      {    1024_1#(x) -> if#(lt(x, 10()), x),
       if#(true(), x) -> 1024_1#(s(x))}
     Weak:
     {     1024_1(x) -> if(lt(x, 10()), x),
              1024() -> 1024_1(0()),
       if(true(), x) -> double(1024_1(s(x))),
      if(false(), x) -> s(0()),
          lt(x, 0()) -> false(),
       lt(0(), s(y)) -> true(),
      lt(s(x), s(y)) -> lt(x, y),
                10() -> double(s(double(s(s(0()))))),
         double(0()) -> 0(),
        double(s(x)) -> s(s(double(x)))}
     BOUND:
      Bound: top(-raise)-DP-bounded by 9
      Automaton:
       {
              false_9() -> 187*
              false_8() -> 165*
              false_7() -> 143*
              false_6() -> 121*
              false_5() -> 99*
              false_4() -> 77*
              false_3() -> 53*
              false_2() -> 29*
              false_1() -> 11*
              false_0() -> 6*
               true_8() -> 165*
               true_7() -> 143*
               true_6() -> 121*
               true_5() -> 99*
               true_4() -> 77*
               true_3() -> 53*
               true_2() -> 29*
               true_1() -> 11*
               true_0() -> 7 | 6
               s_9(206) -> 203*
               s_9(205) -> 206*
               s_9(204) -> 201*
               s_9(203) -> 204*
               s_9(202) -> 199*
               s_9(201) -> 202*
               s_9(200) -> 195*
               s_9(199) -> 200*
               s_9(198) -> 193*
               s_9(197) -> 198*
               s_9(196) -> 186*
               s_9(195) -> 196*
               s_9(194) -> 191*
               s_9(193) -> 194*
               s_9(191) -> 192*
               s_9(189) -> 190*
               s_9(188) -> 189*
               s_9(163) -> 185*
               s_8(184) -> 181*
               s_8(183) -> 184*
               s_8(182) -> 179*
               s_8(181) -> 182*
               s_8(180) -> 177*
               s_8(179) -> 180*
               s_8(178) -> 173*
               s_8(177) -> 178*
               s_8(176) -> 171*
               s_8(175) -> 176*
               s_8(174) -> 164*
               s_8(173) -> 174*
               s_8(172) -> 169*
               s_8(171) -> 172*
               s_8(169) -> 170*
               s_8(167) -> 168*
               s_8(166) -> 167*
               s_8(141) -> 163*
               s_7(162) -> 159*
               s_7(161) -> 162*
               s_7(160) -> 157*
               s_7(159) -> 160*
               s_7(158) -> 155*
               s_7(157) -> 158*
               s_7(156) -> 151*
               s_7(155) -> 156*
               s_7(154) -> 149*
               s_7(153) -> 154*
               s_7(152) -> 142*
               s_7(151) -> 152*
               s_7(150) -> 147*
               s_7(149) -> 150*
               s_7(147) -> 148*
               s_7(145) -> 146*
               s_7(144) -> 145*
               s_7(119) -> 141*
               s_6(140) -> 137*
               s_6(139) -> 140*
               s_6(138) -> 135*
               s_6(137) -> 138*
               s_6(136) -> 133*
               s_6(135) -> 136*
               s_6(134) -> 129*
               s_6(133) -> 134*
               s_6(132) -> 127*
               s_6(131) -> 132*
               s_6(130) -> 120*
               s_6(129) -> 130*
               s_6(128) -> 125*
               s_6(127) -> 128*
               s_6(125) -> 126*
               s_6(123) -> 124*
               s_6(122) -> 123*
                s_6(97) -> 119*
               s_5(118) -> 115*
               s_5(117) -> 118*
               s_5(116) -> 113*
               s_5(115) -> 116*
               s_5(114) -> 111*
               s_5(113) -> 114*
               s_5(112) -> 107*
               s_5(111) -> 112*
               s_5(110) -> 105*
               s_5(109) -> 110*
               s_5(108) -> 98*
               s_5(107) -> 108*
               s_5(106) -> 103*
               s_5(105) -> 106*
               s_5(103) -> 104*
               s_5(101) -> 102*
               s_5(100) -> 101*
                s_5(75) -> 97*
                s_4(96) -> 93*
                s_4(95) -> 96*
                s_4(94) -> 91*
                s_4(93) -> 94*
                s_4(92) -> 89*
                s_4(91) -> 92*
                s_4(90) -> 85*
                s_4(89) -> 90*
                s_4(88) -> 83*
                s_4(87) -> 88*
                s_4(86) -> 76*
                s_4(85) -> 86*
                s_4(84) -> 81*
                s_4(83) -> 84*
                s_4(81) -> 82*
                s_4(79) -> 80*
                s_4(78) -> 79*
                s_4(51) -> 75*
                s_3(74) -> 71*
                s_3(73) -> 74*
                s_3(72) -> 69*
                s_3(71) -> 72*
                s_3(70) -> 67*
                s_3(69) -> 70*
                s_3(68) -> 63*
                s_3(67) -> 68*
                s_3(66) -> 61*
                s_3(65) -> 66*
                s_3(64) -> 52*
                s_3(63) -> 64*
                s_3(62) -> 59*
                s_3(61) -> 62*
                s_3(59) -> 60*
                s_3(57) -> 58*
                s_3(56) -> 57*
                s_3(27) -> 51*
                s_2(55) -> 49*
                s_2(54) -> 55*
                s_2(50) -> 47*
                s_2(49) -> 50*
                s_2(48) -> 45*
                s_2(47) -> 48*
                s_2(46) -> 41*
                s_2(45) -> 46*
                s_2(44) -> 39*
                s_2(43) -> 44*
                s_2(42) -> 28*
                s_2(41) -> 42*
                s_2(40) -> 37*
                s_2(39) -> 40*
                s_2(37) -> 38*
                s_2(35) -> 36*
                s_2(34) -> 35*
                 s_2(9) -> 27*
                s_1(33) -> 30*
                s_1(32) -> 33*
                s_1(31) -> 25*
                s_1(30) -> 31*
                s_1(26) -> 23*
                s_1(25) -> 26*
                s_1(24) -> 19*
                s_1(23) -> 24*
                s_1(22) -> 17*
                s_1(21) -> 22*
                s_1(20) -> 10*
                s_1(19) -> 20*
                s_1(18) -> 15*
                s_1(17) -> 18*
                s_1(15) -> 16*
                s_1(13) -> 14*
                s_1(12) -> 13*
                 s_1(8) -> 9*
                 s_0(8) -> 8*
                 s_0(7) -> 8*
                 s_0(6) -> 8 | 6
          double_9(198) -> 203*
          double_9(197) -> 205*
          double_9(194) -> 199*
          double_9(193) -> 201*
          double_9(192) -> 186*
          double_9(191) -> 195*
          double_9(190) -> 191*
          double_9(189) -> 193*
          double_9(188) -> 197*
          double_8(176) -> 181*
          double_8(175) -> 183*
          double_8(172) -> 177*
          double_8(171) -> 179*
          double_8(170) -> 164*
          double_8(169) -> 173*
          double_8(168) -> 169*
          double_8(167) -> 171*
          double_8(166) -> 175*
          double_7(154) -> 159*
          double_7(153) -> 161*
          double_7(150) -> 155*
          double_7(149) -> 157*
          double_7(148) -> 142*
          double_7(147) -> 151*
          double_7(146) -> 147*
          double_7(145) -> 149*
          double_7(144) -> 153*
          double_6(132) -> 137*
          double_6(131) -> 139*
          double_6(128) -> 133*
          double_6(127) -> 135*
          double_6(126) -> 120*
          double_6(125) -> 129*
          double_6(124) -> 125*
          double_6(123) -> 127*
          double_6(122) -> 131*
          double_5(110) -> 115*
          double_5(109) -> 117*
          double_5(106) -> 111*
          double_5(105) -> 113*
          double_5(104) -> 98*
          double_5(103) -> 107*
          double_5(102) -> 103*
          double_5(101) -> 105*
          double_5(100) -> 109*
           double_4(88) -> 93*
           double_4(87) -> 95*
           double_4(84) -> 89*
           double_4(83) -> 91*
           double_4(82) -> 76*
           double_4(81) -> 85*
           double_4(80) -> 81*
           double_4(79) -> 83*
           double_4(78) -> 87*
           double_3(66) -> 71*
           double_3(65) -> 73*
           double_3(62) -> 67*
           double_3(61) -> 69*
           double_3(60) -> 52*
           double_3(59) -> 63*
           double_3(58) -> 59*
           double_3(57) -> 61*
           double_3(56) -> 65*
           double_2(44) -> 49*
           double_2(43) -> 54*
           double_2(40) -> 45*
           double_2(39) -> 47*
           double_2(38) -> 28*
           double_2(37) -> 41*
           double_2(36) -> 37*
           double_2(35) -> 39*
           double_2(34) -> 43*
           double_1(22) -> 30*
           double_1(21) -> 32*
           double_1(18) -> 23*
           double_1(17) -> 25*
           double_1(16) -> 10*
           double_1(15) -> 19*
           double_1(14) -> 15*
           double_1(13) -> 17*
           double_1(12) -> 21*
            double_0(8) -> 6*
            double_0(7) -> 6*
            double_0(6) -> 6*
                 10_9() -> 186*
                 10_8() -> 164*
                 10_7() -> 142*
                 10_6() -> 120*
                 10_5() -> 98*
                 10_4() -> 76*
                 10_3() -> 52*
                 10_2() -> 28*
                 10_1() -> 10*
                 10_0() -> 6*
         lt_9(185, 186) -> 187*
         lt_9(163, 196) -> 187*
         lt_9(141, 195) -> 187*
         lt_9(119, 200) -> 187*
          lt_9(97, 199) -> 187*
          lt_9(75, 202) -> 187*
          lt_9(51, 201) -> 187*
          lt_9(27, 204) -> 187*
           lt_9(9, 203) -> 187*
           lt_9(8, 206) -> 187*
           lt_9(8, 205) -> 187*
           lt_9(7, 205) -> 187*
           lt_9(6, 205) -> 187*
         lt_8(163, 164) -> 165*
         lt_8(141, 174) -> 165*
         lt_8(119, 173) -> 165*
          lt_8(97, 178) -> 165*
          lt_8(75, 177) -> 165*
          lt_8(51, 180) -> 165*
          lt_8(27, 179) -> 165*
           lt_8(9, 182) -> 165*
           lt_8(8, 184) -> 165*
           lt_8(8, 183) -> 165*
           lt_8(8, 181) -> 165*
           lt_8(7, 184) -> 165*
           lt_8(7, 183) -> 165*
           lt_8(6, 184) -> 165*
           lt_8(6, 183) -> 165*
         lt_7(141, 142) -> 143*
         lt_7(119, 152) -> 143*
          lt_7(97, 151) -> 143*
          lt_7(75, 156) -> 143*
          lt_7(51, 155) -> 143*
          lt_7(27, 158) -> 143*
           lt_7(9, 157) -> 143*
           lt_7(8, 162) -> 143*
           lt_7(8, 161) -> 143*
           lt_7(8, 160) -> 143*
           lt_7(8, 159) -> 143*
           lt_7(7, 162) -> 143*
           lt_7(7, 161) -> 143*
           lt_7(7, 159) -> 143*
           lt_7(6, 162) -> 143*
           lt_7(6, 161) -> 143*
           lt_7(6, 159) -> 143*
         lt_6(119, 120) -> 121*
          lt_6(97, 130) -> 121*
          lt_6(75, 129) -> 121*
          lt_6(51, 134) -> 121*
          lt_6(27, 133) -> 121*
           lt_6(9, 136) -> 121*
           lt_6(8, 140) -> 121*
           lt_6(8, 139) -> 121*
           lt_6(8, 138) -> 121*
           lt_6(8, 137) -> 121*
           lt_6(8, 135) -> 121*
           lt_6(7, 140) -> 121*
           lt_6(7, 139) -> 121*
           lt_6(7, 138) -> 121*
           lt_6(7, 137) -> 121*
           lt_6(6, 140) -> 121*
           lt_6(6, 139) -> 121*
           lt_6(6, 138) -> 121*
           lt_6(6, 137) -> 121*
           lt_5(97, 98) -> 99*
          lt_5(75, 108) -> 99*
          lt_5(51, 107) -> 99*
          lt_5(27, 112) -> 99*
           lt_5(9, 111) -> 99*
           lt_5(8, 118) -> 99*
           lt_5(8, 117) -> 99*
           lt_5(8, 116) -> 99*
           lt_5(8, 115) -> 99*
           lt_5(8, 114) -> 99*
           lt_5(8, 113) -> 99*
           lt_5(7, 118) -> 99*
           lt_5(7, 117) -> 99*
           lt_5(7, 116) -> 99*
           lt_5(7, 115) -> 99*
           lt_5(7, 113) -> 99*
           lt_5(6, 118) -> 99*
           lt_5(6, 117) -> 99*
           lt_5(6, 116) -> 99*
           lt_5(6, 115) -> 99*
           lt_5(6, 113) -> 99*
           lt_4(75, 76) -> 77*
           lt_4(51, 86) -> 77*
           lt_4(27, 85) -> 77*
            lt_4(9, 90) -> 77*
            lt_4(8, 96) -> 77*
            lt_4(8, 95) -> 77*
            lt_4(8, 94) -> 77*
            lt_4(8, 93) -> 77*
            lt_4(8, 92) -> 77*
            lt_4(8, 91) -> 77*
            lt_4(8, 89) -> 77*
            lt_4(7, 96) -> 77*
            lt_4(7, 95) -> 77*
            lt_4(7, 94) -> 77*
            lt_4(7, 93) -> 77*
            lt_4(7, 92) -> 77*
            lt_4(7, 91) -> 77*
            lt_4(6, 96) -> 77*
            lt_4(6, 95) -> 77*
            lt_4(6, 94) -> 77*
            lt_4(6, 93) -> 77*
            lt_4(6, 92) -> 77*
            lt_4(6, 91) -> 77*
           lt_3(51, 52) -> 53*
           lt_3(27, 64) -> 53*
            lt_3(9, 63) -> 53*
            lt_3(8, 74) -> 53*
            lt_3(8, 73) -> 53*
            lt_3(8, 72) -> 53*
            lt_3(8, 71) -> 53*
            lt_3(8, 70) -> 53*
            lt_3(8, 69) -> 53*
            lt_3(8, 68) -> 53*
            lt_3(8, 67) -> 53*
            lt_3(7, 74) -> 53*
            lt_3(7, 73) -> 53*
            lt_3(7, 72) -> 53*
            lt_3(7, 71) -> 53*
            lt_3(7, 70) -> 53*
            lt_3(7, 69) -> 53*
            lt_3(7, 67) -> 53*
            lt_3(6, 74) -> 53*
            lt_3(6, 73) -> 53*
            lt_3(6, 72) -> 53*
            lt_3(6, 71) -> 53*
            lt_3(6, 70) -> 53*
            lt_3(6, 69) -> 53*
            lt_3(6, 67) -> 53*
           lt_2(27, 28) -> 29*
            lt_2(9, 42) -> 29*
            lt_2(8, 55) -> 29*
            lt_2(8, 54) -> 29*
            lt_2(8, 50) -> 29*
            lt_2(8, 49) -> 29*
            lt_2(8, 48) -> 29*
            lt_2(8, 47) -> 29*
            lt_2(8, 46) -> 29*
            lt_2(8, 45) -> 29*
            lt_2(8, 41) -> 29*
            lt_2(7, 55) -> 29*
            lt_2(7, 54) -> 29*
            lt_2(7, 50) -> 29*
            lt_2(7, 49) -> 29*
            lt_2(7, 48) -> 29*
            lt_2(7, 47) -> 29*
            lt_2(7, 46) -> 29*
            lt_2(7, 45) -> 29*
            lt_2(6, 55) -> 29*
            lt_2(6, 54) -> 29*
            lt_2(6, 50) -> 29*
            lt_2(6, 49) -> 29*
            lt_2(6, 48) -> 29*
            lt_2(6, 47) -> 29*
            lt_2(6, 46) -> 29*
            lt_2(6, 45) -> 29*
            lt_1(9, 10) -> 11*
            lt_1(8, 33) -> 11*
            lt_1(8, 32) -> 11*
            lt_1(8, 31) -> 11*
            lt_1(8, 30) -> 11*
            lt_1(8, 26) -> 11*
            lt_1(8, 25) -> 11*
            lt_1(8, 24) -> 11*
            lt_1(8, 23) -> 11*
            lt_1(8, 20) -> 11*
            lt_1(8, 19) -> 11*
            lt_1(7, 33) -> 11*
            lt_1(7, 32) -> 11*
            lt_1(7, 31) -> 11*
            lt_1(7, 30) -> 11*
            lt_1(7, 26) -> 11*
            lt_1(7, 25) -> 11*
            lt_1(7, 24) -> 11*
            lt_1(7, 23) -> 11*
            lt_1(7, 19) -> 11*
            lt_1(6, 33) -> 11*
            lt_1(6, 32) -> 11*
            lt_1(6, 31) -> 11*
            lt_1(6, 30) -> 11*
            lt_1(6, 26) -> 11*
            lt_1(6, 25) -> 11*
            lt_1(6, 24) -> 11*
            lt_1(6, 23) -> 11*
            lt_1(6, 19) -> 11*
             lt_0(8, 8) -> 6*
             lt_0(8, 7) -> 6*
             lt_0(8, 6) -> 6*
             lt_0(7, 8) -> 6*
             lt_0(7, 7) -> 6*
             lt_0(7, 6) -> 6*
             lt_0(6, 8) -> 6*
             lt_0(6, 7) -> 6*
             lt_0(6, 6) -> 6*
        if#_9(187, 185) -> 4*
        if#_8(165, 163) -> 4*
        if#_7(143, 141) -> 4*
        if#_6(121, 119) -> 4*
          if#_5(99, 97) -> 4*
          if#_4(77, 75) -> 4*
          if#_3(53, 51) -> 4*
          if#_2(29, 27) -> 4*
           if#_1(11, 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*
               1024_0() -> 6*
                  0_9() -> 205 | 197 | 188
                  0_8() -> 183 | 175 | 166
                  0_7() -> 161 | 153 | 144
                  0_6() -> 139 | 131 | 122
                  0_5() -> 117 | 109 | 100
                  0_4() -> 95 | 87 | 78
                  0_3() -> 73 | 65 | 56
                  0_2() -> 54 | 43 | 34
                  0_1() -> 32 | 21 | 12
                  0_0() -> 6*
         1024_1#_9(185) -> 4*
         1024_1#_8(163) -> 4*
         1024_1#_7(141) -> 4*
         1024_1#_6(119) -> 4*
          1024_1#_5(97) -> 4*
          1024_1#_4(75) -> 4*
          1024_1#_3(51) -> 4*
          1024_1#_2(27) -> 4*
           1024_1#_1(9) -> 4*
           1024_1#_0(8) -> 4*
            1024_1_0(8) -> 6*
            1024_1_0(7) -> 6*
            1024_1_0(6) -> 6*
       }
      Strict:
       {1024_1#(x) -> if#(lt(x, 10()), x)}
      EDG:
       {}
       SCCS:
        
        Qed