YES

Problem:
 1024() -> 1024_1(0())
 1024_1(x) -> if(lt(x,10()),x)
 if(true(),x) -> double(1024_1(s(x)))
 if(false(),x) -> s(0())
 lt(0(),s(y)) -> true()
 lt(x,0()) -> false()
 lt(s(x),s(y)) -> lt(x,y)
 double(0()) -> 0()
 double(s(x)) -> s(s(double(x)))
 10() -> double(s(double(s(s(0())))))

Proof:
 DP Processor:
  DPs:
   1024#() -> 1024_1#(0())
   1024_1#(x) -> 10#()
   1024_1#(x) -> lt#(x,10())
   1024_1#(x) -> if#(lt(x,10()),x)
   if#(true(),x) -> 1024_1#(s(x))
   if#(true(),x) -> double#(1024_1(s(x)))
   lt#(s(x),s(y)) -> lt#(x,y)
   double#(s(x)) -> double#(x)
   10#() -> double#(s(s(0())))
   10#() -> double#(s(double(s(s(0())))))
  TRS:
   1024() -> 1024_1(0())
   1024_1(x) -> if(lt(x,10()),x)
   if(true(),x) -> double(1024_1(s(x)))
   if(false(),x) -> s(0())
   lt(0(),s(y)) -> true()
   lt(x,0()) -> false()
   lt(s(x),s(y)) -> lt(x,y)
   double(0()) -> 0()
   double(s(x)) -> s(s(double(x)))
   10() -> double(s(double(s(s(0())))))
  EDG Processor:
   DPs:
    1024#() -> 1024_1#(0())
    1024_1#(x) -> 10#()
    1024_1#(x) -> lt#(x,10())
    1024_1#(x) -> if#(lt(x,10()),x)
    if#(true(),x) -> 1024_1#(s(x))
    if#(true(),x) -> double#(1024_1(s(x)))
    lt#(s(x),s(y)) -> lt#(x,y)
    double#(s(x)) -> double#(x)
    10#() -> double#(s(s(0())))
    10#() -> double#(s(double(s(s(0())))))
   TRS:
    1024() -> 1024_1(0())
    1024_1(x) -> if(lt(x,10()),x)
    if(true(),x) -> double(1024_1(s(x)))
    if(false(),x) -> s(0())
    lt(0(),s(y)) -> true()
    lt(x,0()) -> false()
    lt(s(x),s(y)) -> lt(x,y)
    double(0()) -> 0()
    double(s(x)) -> s(s(double(x)))
    10() -> double(s(double(s(s(0())))))
   graph:
    double#(s(x)) -> double#(x) ->
    double#(s(x)) -> double#(x)
    if#(true(),x) -> double#(1024_1(s(x))) ->
    double#(s(x)) -> double#(x)
    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)
    lt#(s(x),s(y)) -> lt#(x,y) -> lt#(s(x),s(y)) -> lt#(x,y)
    10#() -> double#(s(double(s(s(0()))))) ->
    double#(s(x)) -> double#(x)
    10#() -> double#(s(s(0()))) -> double#(s(x)) -> double#(x)
    1024_1#(x) -> if#(lt(x,10()),x) ->
    if#(true(),x) -> 1024_1#(s(x))
    1024_1#(x) -> if#(lt(x,10()),x) ->
    if#(true(),x) -> double#(1024_1(s(x)))
    1024_1#(x) -> lt#(x,10()) -> lt#(s(x),s(y)) -> lt#(x,y)
    1024_1#(x) -> 10#() -> 10#() -> double#(s(s(0())))
    1024_1#(x) -> 10#() -> 10#() -> double#(s(double(s(s(0())))))
    1024#() -> 1024_1#(0()) -> 1024_1#(x) -> 10#()
    1024#() -> 1024_1#(0()) -> 1024_1#(x) -> lt#(x,10())
    1024#() -> 1024_1#(0()) -> 1024_1#(x) -> if#(lt(x,10()),x)
   SCC Processor:
    #sccs: 3
    #rules: 4
    #arcs: 16/100
    DPs:
     if#(true(),x) -> 1024_1#(s(x))
     1024_1#(x) -> if#(lt(x,10()),x)
    TRS:
     1024() -> 1024_1(0())
     1024_1(x) -> if(lt(x,10()),x)
     if(true(),x) -> double(1024_1(s(x)))
     if(false(),x) -> s(0())
     lt(0(),s(y)) -> true()
     lt(x,0()) -> false()
     lt(s(x),s(y)) -> lt(x,y)
     double(0()) -> 0()
     double(s(x)) -> s(s(double(x)))
     10() -> double(s(double(s(s(0())))))
    Usable Rule Processor:
     DPs:
      if#(true(),x) -> 1024_1#(s(x))
      1024_1#(x) -> if#(lt(x,10()),x)
     TRS:
      f16(x,y) -> x
      f16(x,y) -> y
      10() -> double(s(double(s(s(0())))))
      double(s(x)) -> s(s(double(x)))
      double(0()) -> 0()
      lt(0(),s(y)) -> true()
      lt(x,0()) -> false()
      lt(s(x),s(y)) -> lt(x,y)
     Bounds Processor:
      bound: 10
      enrichment: top-dp
      automaton:
       final states: {25}
       transitions:
        lt7(25,271) -> 251*
        lt7(20,271) -> 251*
        lt7(20,273) -> 251*
        lt7(15,273) -> 251*
        lt7(223,258) -> 251*
        lt7(21,274) -> 251*
        lt7(16,274) -> 251*
        lt7(189,257) -> 251*
        lt7(22,273) -> 251*
        lt7(98,270) -> 251*
        lt7(124,263) -> 251*
        lt7(23,274) -> 251*
        lt7(18,274) -> 251*
        lt7(24,273) -> 251*
        lt7(19,273) -> 251*
        lt7(14,273) -> 251*
        lt7(25,272) -> 251*
        lt7(20,272) -> 251*
        lt7(20,274) -> 251*
        lt7(15,274) -> 251*
        lt7(51,269) -> 251*
        lt7(249,250) -> 251*
        lt7(21,273) -> 251*
        lt7(16,273) -> 251*
        lt7(22,274) -> 251*
        lt7(23,273) -> 251*
        lt7(18,273) -> 251*
        lt7(24,274) -> 251*
        lt7(19,274) -> 251*
        lt7(14,274) -> 251*
        lt7(161,264) -> 251*
        107() -> 250*
        double7(267) -> 273*
        double7(252) -> 267*
        double7(259) -> 269*
        double7(254) -> 255*
        double7(256) -> 250*
        double7(268) -> 271*
        double7(253) -> 259*
        double7(260) -> 263*
        double7(255) -> 257*
        07() -> 273,267,252
        false6() -> 225*
        true7() -> 251*
        1024_1{#,8}(275) -> 16,14,25
        s8(297) -> 298*
        s8(292) -> 285*
        s8(287) -> 288*
        s8(294) -> 289*
        s8(289) -> 290*
        s8(279) -> 280*
        s8(249) -> 275*
        s8(296) -> 293*
        s8(291) -> 292*
        s8(286) -> 281*
        s8(281) -> 282*
        s8(298) -> 295*
        s8(293) -> 294*
        s8(288) -> 276*
        s8(278) -> 279*
        s8(295) -> 296*
        s8(290) -> 287*
        s8(285) -> 286*
        if{#,8}(277,275) -> 25,16,14
        lt8(25,295) -> 277*
        lt8(20,295) -> 277*
        lt8(25,297) -> 277*
        lt8(20,297) -> 277*
        lt8(51,296) -> 277*
        lt8(275,276) -> 277*
        lt8(161,289) -> 277*
        lt8(25,298) -> 277*
        lt8(20,298) -> 277*
        lt8(223,287) -> 277*
        lt8(249,288) -> 277*
        lt8(189,290) -> 277*
        lt8(98,293) -> 277*
        lt8(124,294) -> 277*
        108() -> 276*
        double8(292) -> 295*
        double8(282) -> 276*
        double8(279) -> 285*
        double8(291) -> 297*
        double8(286) -> 289*
        double8(281) -> 287*
        double8(278) -> 291*
        double8(285) -> 293*
        double8(280) -> 281*
        08() -> 297,291,278
        false7() -> 251*
        true8() -> 277*
        1024_1{#,9}(301) -> 16,14,25
        s9(327) -> 324*
        s9(317) -> 314*
        s9(307) -> 308*
        s9(324) -> 325*
        s9(319) -> 310*
        s9(314) -> 315*
        s9(304) -> 305*
        s9(326) -> 327*
        s9(321) -> 318*
        s9(316) -> 317*
        s9(311) -> 302*
        s9(318) -> 319*
        s9(325) -> 320*
        s9(320) -> 321*
        s9(315) -> 307*
        s9(310) -> 311*
        s9(305) -> 306*
        s9(275) -> 301*
        if{#,9}(303,301) -> 25,16,14
        if{#,0}(22,14) -> 14*
        if{#,0}(22,16) -> 14*
        if{#,0}(22,18) -> 14*
        if{#,0}(22,20) -> 14*
        if{#,0}(22,22) -> 14*
        if{#,0}(22,24) -> 14*
        if{#,0}(23,15) -> 14*
        if{#,0}(18,15) -> 16,14
        if{#,0}(23,19) -> 14*
        if{#,0}(18,19) -> 16,14
        if{#,0}(23,21) -> 14*
        if{#,0}(18,21) -> 16,14
        if{#,0}(23,23) -> 14*
        if{#,0}(18,23) -> 16,14
        if{#,0}(23,25) -> 14*
        if{#,0}(18,25) -> 16,14
        if{#,0}(24,14) -> 14*
        if{#,0}(19,14) -> 14*
        if{#,0}(24,16) -> 14*
        if{#,0}(14,14) -> 14*
        if{#,0}(19,16) -> 14*
        if{#,0}(24,18) -> 14*
        if{#,0}(14,16) -> 14*
        if{#,0}(19,18) -> 14*
        if{#,0}(24,20) -> 14*
        if{#,0}(14,18) -> 14*
        if{#,0}(19,20) -> 14*
        if{#,0}(24,22) -> 14*
        if{#,0}(14,20) -> 14*
        if{#,0}(19,22) -> 14*
        if{#,0}(24,24) -> 14*
        if{#,0}(14,22) -> 14*
        if{#,0}(19,24) -> 14*
        if{#,0}(14,24) -> 14*
        if{#,0}(25,15) -> 14*
        if{#,0}(20,15) -> 14*
        if{#,0}(15,15) -> 14*
        if{#,0}(25,19) -> 14*
        if{#,0}(20,19) -> 14*
        if{#,0}(25,21) -> 14*
        if{#,0}(15,19) -> 14*
        if{#,0}(20,21) -> 14*
        if{#,0}(25,23) -> 14*
        if{#,0}(15,21) -> 14*
        if{#,0}(20,23) -> 14*
        if{#,0}(25,25) -> 14*
        if{#,0}(15,23) -> 14*
        if{#,0}(20,25) -> 14*
        if{#,0}(15,25) -> 14*
        if{#,0}(21,14) -> 14*
        if{#,0}(16,14) -> 14*
        if{#,0}(21,16) -> 14*
        if{#,0}(16,16) -> 14*
        if{#,0}(21,18) -> 14*
        if{#,0}(16,18) -> 14*
        if{#,0}(21,20) -> 14*
        if{#,0}(16,20) -> 14*
        if{#,0}(21,22) -> 14*
        if{#,0}(16,22) -> 14*
        if{#,0}(21,24) -> 14*
        if{#,0}(16,24) -> 14*
        if{#,0}(22,15) -> 14*
        if{#,0}(22,19) -> 14*
        if{#,0}(22,21) -> 14*
        if{#,0}(22,23) -> 14*
        if{#,0}(22,25) -> 14*
        if{#,0}(23,14) -> 14*
        if{#,0}(18,14) -> 16,14
        if{#,0}(23,16) -> 14*
        if{#,0}(18,16) -> 16,14
        if{#,0}(23,18) -> 14*
        if{#,0}(18,18) -> 16,14
        if{#,0}(23,20) -> 14*
        if{#,0}(18,20) -> 16,14
        if{#,0}(23,22) -> 14*
        if{#,0}(18,22) -> 16,14
        if{#,0}(23,24) -> 14*
        if{#,0}(18,24) -> 25,14
        if{#,0}(24,15) -> 14*
        if{#,0}(19,15) -> 14*
        if{#,0}(14,15) -> 14*
        if{#,0}(24,19) -> 14*
        if{#,0}(19,19) -> 14*
        if{#,0}(24,21) -> 14*
        if{#,0}(14,19) -> 14*
        if{#,0}(19,21) -> 14*
        if{#,0}(24,23) -> 14*
        if{#,0}(14,21) -> 14*
        if{#,0}(19,23) -> 14*
        if{#,0}(24,25) -> 14*
        if{#,0}(14,23) -> 14*
        if{#,0}(19,25) -> 14*
        if{#,0}(14,25) -> 14*
        if{#,0}(25,14) -> 14*
        if{#,0}(20,14) -> 14*
        if{#,0}(25,16) -> 14*
        if{#,0}(15,14) -> 14*
        if{#,0}(20,16) -> 14*
        if{#,0}(25,18) -> 14*
        if{#,0}(15,16) -> 14*
        if{#,0}(20,18) -> 14*
        if{#,0}(25,20) -> 14*
        if{#,0}(15,18) -> 14*
        if{#,0}(20,20) -> 14*
        if{#,0}(25,22) -> 14*
        if{#,0}(15,20) -> 14*
        if{#,0}(20,22) -> 14*
        if{#,0}(25,24) -> 14*
        if{#,0}(15,22) -> 14*
        if{#,0}(20,24) -> 14*
        if{#,0}(15,24) -> 14*
        if{#,0}(21,15) -> 14*
        if{#,0}(16,15) -> 14*
        if{#,0}(21,19) -> 14*
        if{#,0}(16,19) -> 14*
        if{#,0}(21,21) -> 14*
        if{#,0}(16,21) -> 14*
        if{#,0}(21,23) -> 14*
        if{#,0}(16,23) -> 14*
        if{#,0}(21,25) -> 14*
        if{#,0}(16,25) -> 14*
        lt9(98,325) -> 303*
        lt9(124,320) -> 303*
        lt9(25,327) -> 303*
        lt9(20,327) -> 303*
        lt9(51,324) -> 303*
        lt9(161,321) -> 303*
        lt9(25,326) -> 303*
        lt9(20,326) -> 303*
        lt9(223,319) -> 303*
        lt9(249,310) -> 303*
        lt9(275,311) -> 303*
        lt9(189,318) -> 303*
        lt9(301,302) -> 303*
        true0() -> 18,15
        109() -> 302*
        1024_1{#,0}(25) -> 16*
        1024_1{#,0}(20) -> 16*
        1024_1{#,0}(15) -> 16*
        1024_1{#,0}(22) -> 16*
        1024_1{#,0}(24) -> 25*
        1024_1{#,0}(19) -> 16*
        1024_1{#,0}(14) -> 16*
        1024_1{#,0}(21) -> 16*
        1024_1{#,0}(16) -> 16*
        1024_1{#,0}(23) -> 16*
        1024_1{#,0}(18) -> 16*
        false8() -> 277*
        s0(25) -> 24*
        s0(20) -> 24*
        s0(15) -> 24*
        s0(22) -> 24*
        s0(24) -> 19,21,24
        s0(19) -> 24*
        s0(14) -> 24*
        s0(21) -> 24*
        s0(16) -> 24*
        s0(23) -> 24*
        s0(18) -> 24*
        double9(317) -> 324*
        double9(307) -> 310*
        double9(314) -> 320*
        double9(304) -> 316*
        double9(316) -> 326*
        double9(306) -> 307*
        double9(308) -> 302*
        double9(315) -> 318*
        double9(305) -> 314*
        lt0(22,14) -> 18*
        lt0(22,16) -> 18*
        lt0(22,18) -> 18*
        lt0(22,20) -> 18*
        lt0(22,22) -> 18*
        lt0(22,24) -> 18*
        lt0(23,15) -> 18*
        lt0(18,15) -> 18*
        lt0(23,19) -> 18*
        lt0(18,19) -> 18*
        lt0(23,21) -> 18*
        lt0(18,21) -> 18*
        lt0(23,23) -> 18*
        lt0(18,23) -> 18*
        lt0(23,25) -> 18*
        lt0(18,25) -> 18*
        lt0(24,14) -> 18*
        lt0(19,14) -> 18*
        lt0(24,16) -> 18*
        lt0(14,14) -> 18*
        lt0(19,16) -> 18*
        lt0(24,18) -> 18*
        lt0(14,16) -> 18*
        lt0(19,18) -> 18*
        lt0(24,20) -> 18*
        lt0(14,18) -> 18*
        lt0(19,20) -> 18*
        lt0(24,22) -> 18*
        lt0(14,20) -> 18*
        lt0(19,22) -> 18*
        lt0(24,24) -> 18*
        lt0(14,22) -> 18*
        lt0(19,24) -> 18*
        lt0(14,24) -> 18*
        lt0(25,15) -> 18*
        lt0(20,15) -> 18*
        lt0(15,15) -> 18*
        lt0(25,19) -> 18*
        lt0(20,19) -> 18*
        lt0(25,21) -> 18*
        lt0(15,19) -> 18*
        lt0(20,21) -> 18*
        lt0(25,23) -> 18*
        lt0(15,21) -> 18*
        lt0(20,23) -> 18*
        lt0(25,25) -> 18*
        lt0(15,23) -> 18*
        lt0(20,25) -> 18*
        lt0(15,25) -> 18*
        lt0(21,14) -> 18*
        lt0(16,14) -> 18*
        lt0(21,16) -> 18*
        lt0(16,16) -> 18*
        lt0(21,18) -> 18*
        lt0(16,18) -> 18*
        lt0(21,20) -> 18*
        lt0(16,20) -> 18*
        lt0(21,22) -> 18*
        lt0(16,22) -> 18*
        lt0(21,24) -> 18*
        lt0(16,24) -> 18*
        lt0(22,15) -> 18*
        lt0(22,19) -> 18*
        lt0(22,21) -> 18*
        lt0(22,23) -> 18*
        lt0(22,25) -> 18*
        lt0(23,14) -> 18*
        lt0(18,14) -> 18*
        lt0(23,16) -> 18*
        lt0(18,16) -> 18*
        lt0(23,18) -> 18*
        lt0(18,18) -> 18*
        lt0(23,20) -> 18*
        lt0(18,20) -> 18*
        lt0(23,22) -> 18*
        lt0(18,22) -> 18*
        lt0(23,24) -> 18*
        lt0(18,24) -> 18*
        lt0(24,15) -> 18*
        lt0(19,15) -> 18*
        lt0(14,15) -> 18*
        lt0(24,19) -> 18*
        lt0(19,19) -> 18*
        lt0(24,21) -> 18*
        lt0(14,19) -> 18*
        lt0(19,21) -> 18*
        lt0(24,23) -> 18*
        lt0(14,21) -> 18*
        lt0(19,23) -> 18*
        lt0(24,25) -> 18*
        lt0(14,23) -> 18*
        lt0(19,25) -> 18*
        lt0(14,25) -> 18*
        lt0(25,14) -> 18*
        lt0(20,14) -> 18*
        lt0(25,16) -> 18*
        lt0(15,14) -> 18*
        lt0(20,16) -> 18*
        lt0(25,18) -> 18*
        lt0(15,16) -> 18*
        lt0(20,18) -> 18*
        lt0(25,20) -> 18*
        lt0(15,18) -> 18*
        lt0(20,20) -> 18*
        lt0(25,22) -> 18*
        lt0(15,20) -> 18*
        lt0(20,22) -> 18*
        lt0(25,24) -> 18*
        lt0(15,22) -> 18*
        lt0(20,24) -> 18*
        lt0(15,24) -> 18*
        lt0(21,15) -> 18*
        lt0(16,15) -> 18*
        lt0(21,19) -> 18*
        lt0(16,19) -> 18*
        lt0(21,21) -> 18*
        lt0(16,21) -> 18*
        lt0(21,23) -> 18*
        lt0(16,23) -> 18*
        lt0(21,25) -> 18*
        lt0(16,25) -> 18*
        09() -> 326,316,304
        100() -> 19*
        true9() -> 303*
        f160(22,14) -> 20*
        f160(22,16) -> 20*
        f160(22,18) -> 20*
        f160(22,20) -> 20*
        f160(22,22) -> 20*
        f160(22,24) -> 20*
        f160(23,15) -> 20*
        f160(18,15) -> 20*
        f160(23,19) -> 20*
        f160(18,19) -> 20*
        f160(23,21) -> 20*
        f160(18,21) -> 20*
        f160(23,23) -> 20*
        f160(18,23) -> 20*
        f160(23,25) -> 20*
        f160(18,25) -> 20*
        f160(24,14) -> 20*
        f160(19,14) -> 20*
        f160(24,16) -> 20*
        f160(14,14) -> 20*
        f160(19,16) -> 20*
        f160(24,18) -> 20*
        f160(14,16) -> 20*
        f160(19,18) -> 20*
        f160(24,20) -> 20*
        f160(14,18) -> 20*
        f160(19,20) -> 20*
        f160(24,22) -> 20*
        f160(14,20) -> 20*
        f160(19,22) -> 20*
        f160(24,24) -> 20*
        f160(14,22) -> 20*
        f160(19,24) -> 20*
        f160(14,24) -> 20*
        f160(25,15) -> 20*
        f160(20,15) -> 20*
        f160(15,15) -> 20*
        f160(25,19) -> 20*
        f160(20,19) -> 20*
        f160(25,21) -> 20*
        f160(15,19) -> 20*
        f160(20,21) -> 20*
        f160(25,23) -> 20*
        f160(15,21) -> 20*
        f160(20,23) -> 20*
        f160(25,25) -> 20*
        f160(15,23) -> 20*
        f160(20,25) -> 20*
        f160(15,25) -> 20*
        f160(21,14) -> 20*
        f160(16,14) -> 20*
        f160(21,16) -> 20*
        f160(16,16) -> 20*
        f160(21,18) -> 20*
        f160(16,18) -> 20*
        f160(21,20) -> 20*
        f160(16,20) -> 20*
        f160(21,22) -> 20*
        f160(16,22) -> 20*
        f160(21,24) -> 20*
        f160(16,24) -> 20*
        f160(22,15) -> 20*
        f160(22,19) -> 20*
        f160(22,21) -> 20*
        f160(22,23) -> 20*
        f160(22,25) -> 20*
        f160(23,14) -> 20*
        f160(18,14) -> 20*
        f160(23,16) -> 20*
        f160(18,16) -> 20*
        f160(23,18) -> 20*
        f160(18,18) -> 20*
        f160(23,20) -> 20*
        f160(18,20) -> 20*
        f160(23,22) -> 20*
        f160(18,22) -> 20*
        f160(23,24) -> 20*
        f160(18,24) -> 20*
        f160(24,15) -> 20*
        f160(19,15) -> 20*
        f160(14,15) -> 20*
        f160(24,19) -> 20*
        f160(19,19) -> 20*
        f160(24,21) -> 20*
        f160(14,19) -> 20*
        f160(19,21) -> 20*
        f160(24,23) -> 20*
        f160(14,21) -> 20*
        f160(19,23) -> 20*
        f160(24,25) -> 20*
        f160(14,23) -> 20*
        f160(19,25) -> 20*
        f160(14,25) -> 20*
        f160(25,14) -> 20*
        f160(20,14) -> 20*
        f160(25,16) -> 20*
        f160(15,14) -> 20*
        f160(20,16) -> 20*
        f160(25,18) -> 20*
        f160(15,16) -> 20*
        f160(20,18) -> 20*
        f160(25,20) -> 20*
        f160(15,18) -> 20*
        f160(20,20) -> 20*
        f160(25,22) -> 20*
        f160(15,20) -> 20*
        f160(20,22) -> 20*
        f160(25,24) -> 20*
        f160(15,22) -> 20*
        f160(20,24) -> 20*
        f160(15,24) -> 20*
        f160(21,15) -> 20*
        f160(16,15) -> 20*
        f160(21,19) -> 20*
        f160(16,19) -> 20*
        f160(21,21) -> 20*
        f160(16,21) -> 20*
        f160(21,23) -> 20*
        f160(16,23) -> 20*
        f160(21,25) -> 20*
        f160(16,25) -> 20*
        1024_1{#,10}(328) -> 16,14,25
        double0(25) -> 21*
        double0(20) -> 21*
        double0(15) -> 21*
        double0(22) -> 21*
        double0(24) -> 19,21
        double0(19) -> 21*
        double0(14) -> 21*
        double0(21) -> 21*
        double0(16) -> 21*
        double0(23) -> 21*
        double0(18) -> 21*
        s10(352) -> 349*
        s10(347) -> 348*
        s10(342) -> 329*
        s10(337) -> 338*
        s10(354) -> 351*
        s10(349) -> 350*
        s10(344) -> 339*
        s10(339) -> 340*
        s10(351) -> 352*
        s10(346) -> 341*
        s10(341) -> 342*
        s10(336) -> 337*
        s10(301) -> 328*
        s10(353) -> 354*
        s10(348) -> 343*
        s10(343) -> 344*
        s10(350) -> 345*
        s10(345) -> 346*
        00() -> 21,22
        false9() -> 303*
        false0() -> 18,23
        if{#,10}(330,328) -> 25,16,14
        1024_1{#,1}(51) -> 16,25,14
        lt10(223,345) -> 330*
        lt10(249,346) -> 330*
        lt10(275,341) -> 330*
        lt10(98,351) -> 330*
        lt10(189,350) -> 330*
        lt10(301,342) -> 330*
        lt10(124,352) -> 330*
        lt10(25,353) -> 330*
        lt10(20,353) -> 330*
        lt10(51,354) -> 330*
        lt10(328,329) -> 330*
        lt10(161,349) -> 330*
        s1(90) -> 85*
        s1(85) -> 86*
        s1(80) -> 81*
        s1(25) -> 51*
        s1(20) -> 51*
        s1(15) -> 51*
        s1(92) -> 87*
        s1(87) -> 88*
        s1(22) -> 51*
        s1(104) -> 93*
        s1(94) -> 89*
        s1(89) -> 90*
        s1(24) -> 51*
        s1(19) -> 51*
        s1(14) -> 51*
        s1(111) -> 103*
        s1(91) -> 92*
        s1(86) -> 65*
        s1(81) -> 82*
        s1(21) -> 51*
        s1(16) -> 51*
        s1(103) -> 104*
        s1(93) -> 94*
        s1(88) -> 83*
        s1(83) -> 84*
        s1(23) -> 51*
        s1(18) -> 51*
        s1(110) -> 111*
        1010() -> 329*
        if{#,1}(66,51) -> 25,16,14
        double10(347) -> 353*
        double10(337) -> 343*
        double10(344) -> 345*
        double10(339) -> 341*
        double10(336) -> 347*
        double10(348) -> 351*
        double10(343) -> 349*
        double10(338) -> 339*
        double10(340) -> 329*
        lt1(22,111) -> 66*
        lt1(23,94) -> 66*
        lt1(18,94) -> 66*
        lt1(23,104) -> 66*
        lt1(18,104) -> 66*
        lt1(24,89) -> 66*
        lt1(19,89) -> 66*
        lt1(23,110) -> 66*
        lt1(14,89) -> 66*
        lt1(18,110) -> 66*
        lt1(24,93) -> 66*
        lt1(19,93) -> 66*
        lt1(14,93) -> 66*
        lt1(51,65) -> 66*
        lt1(24,103) -> 66*
        lt1(19,103) -> 66*
        lt1(14,103) -> 66*
        lt1(25,86) -> 66*
        lt1(20,86) -> 66*
        lt1(25,90) -> 66*
        lt1(20,90) -> 66*
        lt1(24,111) -> 66*
        lt1(19,111) -> 66*
        lt1(14,111) -> 66*
        lt1(20,94) -> 66*
        lt1(15,94) -> 66*
        lt1(20,104) -> 66*
        lt1(15,104) -> 66*
        lt1(21,89) -> 66*
        lt1(16,89) -> 66*
        lt1(20,110) -> 66*
        lt1(15,110) -> 66*
        lt1(21,93) -> 66*
        lt1(16,93) -> 66*
        lt1(21,103) -> 66*
        lt1(16,103) -> 66*
        lt1(21,111) -> 66*
        lt1(16,111) -> 66*
        lt1(22,94) -> 66*
        lt1(22,104) -> 66*
        lt1(23,89) -> 66*
        lt1(18,89) -> 66*
        lt1(22,110) -> 66*
        lt1(23,93) -> 66*
        lt1(18,93) -> 66*
        lt1(23,103) -> 66*
        lt1(18,103) -> 66*
        lt1(23,111) -> 66*
        lt1(18,111) -> 66*
        lt1(24,94) -> 66*
        lt1(19,94) -> 66*
        lt1(14,94) -> 66*
        lt1(24,104) -> 66*
        lt1(25,85) -> 66*
        lt1(19,104) -> 66*
        lt1(20,85) -> 66*
        lt1(14,104) -> 66*
        lt1(20,89) -> 66*
        lt1(24,110) -> 66*
        lt1(15,89) -> 66*
        lt1(19,110) -> 66*
        lt1(14,110) -> 66*
        lt1(20,93) -> 66*
        lt1(15,93) -> 66*
        lt1(20,103) -> 66*
        lt1(15,103) -> 66*
        lt1(20,111) -> 66*
        lt1(15,111) -> 66*
        lt1(21,94) -> 66*
        lt1(16,94) -> 66*
        lt1(21,104) -> 66*
        lt1(16,104) -> 66*
        lt1(22,89) -> 66*
        lt1(21,110) -> 66*
        lt1(16,110) -> 66*
        lt1(22,93) -> 66*
        lt1(22,103) -> 66*
        010() -> 353,347,336
        101() -> 65*
        false10() -> 330*
        double1(80) -> 91*
        double1(92) -> 103*
        double1(87) -> 93*
        double1(82) -> 83*
        double1(84) -> 65*
        double1(91) -> 110*
        double1(81) -> 87*
        double1(88) -> 89*
        double1(83) -> 85*
        01() -> 110,91,80
        true1() -> 66*
        if{#,2}(102,98) -> 25,16,14
        lt2(25,117) -> 102*
        lt2(20,117) -> 102*
        lt2(20,121) -> 102*
        lt2(15,121) -> 102*
        lt2(20,123) -> 102*
        lt2(15,123) -> 102*
        lt2(20,127) -> 102*
        lt2(15,127) -> 102*
        lt2(21,116) -> 102*
        lt2(16,116) -> 102*
        lt2(21,120) -> 102*
        lt2(16,120) -> 102*
        lt2(21,122) -> 102*
        lt2(16,122) -> 102*
        lt2(21,128) -> 102*
        lt2(16,128) -> 102*
        lt2(22,121) -> 102*
        lt2(22,123) -> 102*
        lt2(22,127) -> 102*
        lt2(23,116) -> 102*
        lt2(25,112) -> 102*
        lt2(18,116) -> 102*
        lt2(20,112) -> 102*
        lt2(23,120) -> 102*
        lt2(18,120) -> 102*
        lt2(23,122) -> 102*
        lt2(18,122) -> 102*
        lt2(23,128) -> 102*
        lt2(18,128) -> 102*
        lt2(24,121) -> 102*
        lt2(19,121) -> 102*
        lt2(24,123) -> 102*
        lt2(14,121) -> 102*
        lt2(19,123) -> 102*
        lt2(14,123) -> 102*
        lt2(24,127) -> 102*
        lt2(19,127) -> 102*
        lt2(14,127) -> 102*
        lt2(98,101) -> 102*
        lt2(20,116) -> 102*
        lt2(15,116) -> 102*
        lt2(20,120) -> 102*
        lt2(15,120) -> 102*
        lt2(20,122) -> 102*
        lt2(15,122) -> 102*
        lt2(51,113) -> 102*
        lt2(20,128) -> 102*
        lt2(15,128) -> 102*
        lt2(21,121) -> 102*
        lt2(16,121) -> 102*
        lt2(21,123) -> 102*
        lt2(16,123) -> 102*
        lt2(21,127) -> 102*
        lt2(16,127) -> 102*
        lt2(22,116) -> 102*
        lt2(22,120) -> 102*
        lt2(22,122) -> 102*
        lt2(22,128) -> 102*
        lt2(23,121) -> 102*
        lt2(18,121) -> 102*
        lt2(23,123) -> 102*
        lt2(18,123) -> 102*
        lt2(23,127) -> 102*
        lt2(18,127) -> 102*
        lt2(24,116) -> 102*
        lt2(19,116) -> 102*
        lt2(14,116) -> 102*
        lt2(24,120) -> 102*
        lt2(19,120) -> 102*
        lt2(24,122) -> 102*
        lt2(14,120) -> 102*
        lt2(19,122) -> 102*
        lt2(14,122) -> 102*
        lt2(24,128) -> 102*
        lt2(19,128) -> 102*
        lt2(14,128) -> 102*
        102() -> 101*
        1024_1{#,2}(98) -> 16,14,25
        s2(105) -> 106*
        s2(127) -> 128*
        s2(122) -> 123*
        s2(117) -> 112*
        s2(112) -> 113*
        s2(119) -> 114*
        s2(114) -> 115*
        s2(121) -> 116*
        s2(116) -> 117*
        s2(106) -> 107*
        s2(51) -> 98*
        s2(128) -> 122*
        s2(123) -> 120*
        s2(118) -> 119*
        s2(113) -> 101*
        s2(108) -> 109*
        s2(120) -> 121*
        s2(115) -> 108*
        double2(105) -> 118*
        double2(107) -> 108*
        double2(119) -> 122*
        double2(114) -> 120*
        double2(109) -> 101*
        double2(106) -> 114*
        double2(118) -> 127*
        double2(108) -> 112*
        double2(115) -> 116*
        02() -> 127,118,105
        true2() -> 102*
        1024_1{#,3}(124) -> 16,14,25
        s3(157) -> 158*
        s3(147) -> 148*
        s3(142) -> 125*
        s3(132) -> 133*
        s3(159) -> 160*
        s3(149) -> 150*
        s3(144) -> 132*
        s3(129) -> 130*
        s3(146) -> 143*
        s3(141) -> 142*
        s3(158) -> 149*
        s3(148) -> 141*
        s3(143) -> 144*
        s3(98) -> 124*
        s3(160) -> 157*
        s3(150) -> 147*
        s3(145) -> 146*
        s3(130) -> 131*
        if{#,3}(126,124) -> 25,16,14
        lt3(23,157) -> 126*
        lt3(18,157) -> 126*
        lt3(23,159) -> 126*
        lt3(18,159) -> 126*
        lt3(24,150) -> 126*
        lt3(19,150) -> 126*
        lt3(14,150) -> 126*
        lt3(24,158) -> 126*
        lt3(19,158) -> 126*
        lt3(24,160) -> 126*
        lt3(14,158) -> 126*
        lt3(19,160) -> 126*
        lt3(14,160) -> 126*
        lt3(25,147) -> 126*
        lt3(20,147) -> 126*
        lt3(20,149) -> 126*
        lt3(15,149) -> 126*
        lt3(20,157) -> 126*
        lt3(15,157) -> 126*
        lt3(20,159) -> 126*
        lt3(15,159) -> 126*
        lt3(21,150) -> 126*
        lt3(16,150) -> 126*
        lt3(21,158) -> 126*
        lt3(16,158) -> 126*
        lt3(21,160) -> 126*
        lt3(16,160) -> 126*
        lt3(124,125) -> 126*
        lt3(98,142) -> 126*
        lt3(22,149) -> 126*
        lt3(22,157) -> 126*
        lt3(22,159) -> 126*
        lt3(23,150) -> 126*
        lt3(18,150) -> 126*
        lt3(23,158) -> 126*
        lt3(18,158) -> 126*
        lt3(23,160) -> 126*
        lt3(18,160) -> 126*
        lt3(24,149) -> 126*
        lt3(19,149) -> 126*
        lt3(14,149) -> 126*
        lt3(24,157) -> 126*
        lt3(19,157) -> 126*
        lt3(24,159) -> 126*
        lt3(14,157) -> 126*
        lt3(19,159) -> 126*
        lt3(14,159) -> 126*
        lt3(25,148) -> 126*
        lt3(20,148) -> 126*
        lt3(20,150) -> 126*
        lt3(15,150) -> 126*
        lt3(51,141) -> 126*
        lt3(20,158) -> 126*
        lt3(15,158) -> 126*
        lt3(20,160) -> 126*
        lt3(15,160) -> 126*
        lt3(21,149) -> 126*
        lt3(16,149) -> 126*
        lt3(21,157) -> 126*
        lt3(16,157) -> 126*
        lt3(21,159) -> 126*
        lt3(16,159) -> 126*
        lt3(22,150) -> 126*
        lt3(22,158) -> 126*
        lt3(22,160) -> 126*
        lt3(23,149) -> 126*
        lt3(18,149) -> 126*
        103() -> 125*
        double3(132) -> 141*
        double3(144) -> 147*
        double3(129) -> 145*
        double3(146) -> 157*
        double3(131) -> 132*
        double3(143) -> 149*
        double3(133) -> 125*
        double3(145) -> 159*
        double3(130) -> 143*
        03() -> 159,145,129
        false1() -> 66*
        true3() -> 126*
        1024_1{#,4}(161) -> 16,14,25
        s4(187) -> 188*
        s4(182) -> 173*
        s4(184) -> 179*
        s4(179) -> 180*
        s4(174) -> 171*
        s4(169) -> 170*
        s4(124) -> 161*
        s4(186) -> 183*
        s4(181) -> 182*
        s4(176) -> 166*
        s4(171) -> 172*
        s4(188) -> 185*
        s4(183) -> 184*
        s4(173) -> 174*
        s4(168) -> 169*
        s4(185) -> 186*
        s4(180) -> 175*
        s4(175) -> 176*
        false2() -> 102*
        if{#,4}(167,161) -> 25,16,14
        lt4(98,175) -> 167*
        lt4(22,186) -> 167*
        lt4(22,188) -> 167*
        lt4(124,176) -> 167*
        lt4(23,185) -> 167*
        lt4(18,185) -> 167*
        lt4(23,187) -> 167*
        lt4(18,187) -> 167*
        lt4(161,166) -> 167*
        lt4(24,186) -> 167*
        lt4(19,186) -> 167*
        lt4(24,188) -> 167*
        lt4(14,186) -> 167*
        lt4(19,188) -> 167*
        lt4(14,188) -> 167*
        lt4(25,179) -> 167*
        lt4(20,179) -> 167*
        lt4(25,183) -> 167*
        lt4(20,183) -> 167*
        lt4(20,185) -> 167*
        lt4(15,185) -> 167*
        lt4(20,187) -> 167*
        lt4(15,187) -> 167*
        lt4(51,180) -> 167*
        lt4(21,186) -> 167*
        lt4(16,186) -> 167*
        lt4(21,188) -> 167*
        lt4(16,188) -> 167*
        lt4(22,185) -> 167*
        lt4(22,187) -> 167*
        lt4(23,186) -> 167*
        lt4(18,186) -> 167*
        lt4(23,188) -> 167*
        lt4(18,188) -> 167*
        lt4(24,185) -> 167*
        lt4(19,185) -> 167*
        lt4(24,187) -> 167*
        lt4(14,185) -> 167*
        lt4(19,187) -> 167*
        lt4(14,187) -> 167*
        lt4(25,184) -> 167*
        lt4(20,184) -> 167*
        lt4(20,186) -> 167*
        lt4(15,186) -> 167*
        lt4(20,188) -> 167*
        lt4(15,188) -> 167*
        lt4(21,185) -> 167*
        lt4(16,185) -> 167*
        lt4(21,187) -> 167*
        lt4(16,187) -> 167*
        104() -> 166*
        double4(182) -> 185*
        double4(172) -> 166*
        double4(174) -> 179*
        double4(169) -> 173*
        double4(181) -> 187*
        double4(171) -> 175*
        double4(173) -> 183*
        double4(168) -> 181*
        double4(170) -> 171*
        04() -> 187,181,168
        false3() -> 126*
        true4() -> 167*
        1024_1{#,5}(189) -> 16,14,25
        s5(212) -> 213*
        s5(207) -> 202*
        s5(202) -> 203*
        s5(197) -> 198*
        s5(219) -> 220*
        s5(209) -> 204*
        s5(204) -> 205*
        s5(211) -> 206*
        s5(206) -> 207*
        s5(161) -> 189*
        s5(213) -> 210*
        s5(208) -> 209*
        s5(203) -> 193*
        s5(198) -> 199*
        s5(220) -> 212*
        s5(210) -> 211*
        s5(205) -> 200*
        s5(200) -> 201*
        if{#,5}(194,189) -> 25,16,14
        lt5(25,210) -> 194*
        lt5(20,210) -> 194*
        lt5(20,212) -> 194*
        lt5(15,212) -> 194*
        lt5(20,220) -> 194*
        lt5(15,220) -> 194*
        lt5(21,213) -> 194*
        lt5(16,213) -> 194*
        lt5(21,219) -> 194*
        lt5(16,219) -> 194*
        lt5(98,207) -> 194*
        lt5(22,212) -> 194*
        lt5(22,220) -> 194*
        lt5(124,202) -> 194*
        lt5(23,213) -> 194*
        lt5(18,213) -> 194*
        lt5(23,219) -> 194*
        lt5(18,219) -> 194*
        lt5(24,212) -> 194*
        lt5(19,212) -> 194*
        lt5(14,212) -> 194*
        lt5(24,220) -> 194*
        lt5(19,220) -> 194*
        lt5(14,220) -> 194*
        lt5(25,211) -> 194*
        lt5(20,211) -> 194*
        lt5(20,213) -> 194*
        lt5(15,213) -> 194*
        lt5(20,219) -> 194*
        lt5(51,206) -> 194*
        lt5(15,219) -> 194*
        lt5(21,212) -> 194*
        lt5(16,212) -> 194*
        lt5(189,193) -> 194*
        lt5(21,220) -> 194*
        lt5(16,220) -> 194*
        lt5(22,213) -> 194*
        lt5(22,219) -> 194*
        lt5(23,212) -> 194*
        lt5(18,212) -> 194*
        lt5(23,220) -> 194*
        lt5(18,220) -> 194*
        lt5(24,213) -> 194*
        lt5(19,213) -> 194*
        lt5(14,213) -> 194*
        lt5(161,203) -> 194*
        lt5(24,219) -> 194*
        lt5(19,219) -> 194*
        lt5(14,219) -> 194*
        105() -> 193*
        double5(197) -> 208*
        double5(209) -> 212*
        double5(204) -> 210*
        double5(199) -> 200*
        double5(201) -> 193*
        double5(208) -> 219*
        double5(198) -> 204*
        double5(205) -> 206*
        double5(200) -> 202*
        05() -> 219,208,197
        false4() -> 167*
        true5() -> 194*
        1024_1{#,6}(223) -> 16,14,25
        s6(247) -> 248*
        s6(237) -> 238*
        s6(232) -> 224*
        s6(227) -> 228*
        s6(244) -> 235*
        s6(234) -> 229*
        s6(229) -> 230*
        s6(189) -> 223*
        s6(246) -> 243*
        s6(236) -> 231*
        s6(231) -> 232*
        s6(226) -> 227*
        s6(248) -> 245*
        s6(243) -> 244*
        s6(238) -> 233*
        s6(233) -> 234*
        s6(245) -> 246*
        s6(235) -> 236*
        if{#,6}(225,223) -> 25,16,14
        lt6(22,245) -> 225*
        lt6(22,247) -> 225*
        lt6(161,231) -> 225*
        lt6(23,248) -> 225*
        lt6(18,248) -> 225*
        lt6(24,245) -> 225*
        lt6(19,245) -> 225*
        lt6(24,247) -> 225*
        lt6(14,245) -> 225*
        lt6(19,247) -> 225*
        lt6(14,247) -> 225*
        lt6(189,232) -> 225*
        lt6(98,235) -> 225*
        lt6(25,246) -> 225*
        lt6(20,246) -> 225*
        lt6(20,248) -> 225*
        lt6(15,248) -> 225*
        lt6(124,236) -> 225*
        lt6(21,245) -> 225*
        lt6(16,245) -> 225*
        lt6(21,247) -> 225*
        lt6(16,247) -> 225*
        lt6(22,248) -> 225*
        lt6(23,245) -> 225*
        lt6(18,245) -> 225*
        lt6(23,247) -> 225*
        lt6(18,247) -> 225*
        lt6(223,224) -> 225*
        lt6(24,248) -> 225*
        lt6(19,248) -> 225*
        lt6(14,248) -> 225*
        lt6(25,243) -> 225*
        lt6(20,243) -> 225*
        lt6(20,245) -> 225*
        lt6(15,245) -> 225*
        lt6(20,247) -> 225*
        lt6(15,247) -> 225*
        lt6(51,244) -> 225*
        lt6(21,248) -> 225*
        lt6(16,248) -> 225*
        106() -> 224*
        double6(237) -> 247*
        double6(227) -> 233*
        double6(234) -> 235*
        double6(229) -> 231*
        double6(226) -> 237*
        double6(238) -> 245*
        double6(233) -> 243*
        double6(228) -> 229*
        double6(230) -> 224*
        06() -> 247,237,226
        false5() -> 194*
        true6() -> 225*
        1024_1{#,7}(249) -> 16,14,25
        s7(272) -> 269*
        s7(267) -> 268*
        s7(257) -> 258*
        s7(252) -> 253*
        s7(274) -> 271*
        s7(269) -> 270*
        s7(264) -> 257*
        s7(259) -> 260*
        s7(271) -> 272*
        s7(273) -> 274*
        s7(268) -> 259*
        s7(263) -> 264*
        s7(258) -> 250*
        s7(253) -> 254*
        s7(223) -> 249*
        s7(270) -> 263*
        s7(260) -> 255*
        s7(255) -> 256*
        if{#,7}(251,249) -> 25,16,14
        14 -> 20*
        15 -> 20*
        16 -> 20*
        18 -> 20*
        19 -> 20*
        21 -> 20*
        22 -> 20*
        23 -> 20*
        24 -> 20*
        25 -> 20*
      problem:
       DPs:
        1024_1#(x) -> if#(lt(x,10()),x)
       TRS:
        f16(x,y) -> x
        f16(x,y) -> y
        10() -> double(s(double(s(s(0())))))
        double(s(x)) -> s(s(double(x)))
        double(0()) -> 0()
        lt(0(),s(y)) -> true()
        lt(x,0()) -> false()
        lt(s(x),s(y)) -> lt(x,y)
      Restore Modifier:
       DPs:
        1024_1#(x) -> if#(lt(x,10()),x)
       TRS:
        1024() -> 1024_1(0())
        1024_1(x) -> if(lt(x,10()),x)
        if(true(),x) -> double(1024_1(s(x)))
        if(false(),x) -> s(0())
        lt(0(),s(y)) -> true()
        lt(x,0()) -> false()
        lt(s(x),s(y)) -> lt(x,y)
        double(0()) -> 0()
        double(s(x)) -> s(s(double(x)))
        10() -> double(s(double(s(s(0())))))
       Matrix Interpretation Processor:
        dimension: 1
        interpretation:
         [if#](x0, x1) = 0,
         
         [1024_1#](x0) = 1,
         
         [false] = 0,
         
         [double](x0) = 0,
         
         [s](x0) = 0,
         
         [true] = 0,
         
         [if](x0, x1) = 0,
         
         [lt](x0, x1) = 0,
         
         [10] = 0,
         
         [1024_1](x0) = 0,
         
         [0] = 0,
         
         [1024] = 0
        orientation:
         1024_1#(x) = 1 >= 0 = if#(lt(x,10()),x)
         
         1024() = 0 >= 0 = 1024_1(0())
         
         1024_1(x) = 0 >= 0 = if(lt(x,10()),x)
         
         if(true(),x) = 0 >= 0 = double(1024_1(s(x)))
         
         if(false(),x) = 0 >= 0 = s(0())
         
         lt(0(),s(y)) = 0 >= 0 = true()
         
         lt(x,0()) = 0 >= 0 = false()
         
         lt(s(x),s(y)) = 0 >= 0 = lt(x,y)
         
         double(0()) = 0 >= 0 = 0()
         
         double(s(x)) = 0 >= 0 = s(s(double(x)))
         
         10() = 0 >= 0 = double(s(double(s(s(0())))))
        problem:
         DPs:
          
         TRS:
          1024() -> 1024_1(0())
          1024_1(x) -> if(lt(x,10()),x)
          if(true(),x) -> double(1024_1(s(x)))
          if(false(),x) -> s(0())
          lt(0(),s(y)) -> true()
          lt(x,0()) -> false()
          lt(s(x),s(y)) -> lt(x,y)
          double(0()) -> 0()
          double(s(x)) -> s(s(double(x)))
          10() -> double(s(double(s(s(0())))))
        Qed
    
    DPs:
     lt#(s(x),s(y)) -> lt#(x,y)
    TRS:
     1024() -> 1024_1(0())
     1024_1(x) -> if(lt(x,10()),x)
     if(true(),x) -> double(1024_1(s(x)))
     if(false(),x) -> s(0())
     lt(0(),s(y)) -> true()
     lt(x,0()) -> false()
     lt(s(x),s(y)) -> lt(x,y)
     double(0()) -> 0()
     double(s(x)) -> s(s(double(x)))
     10() -> double(s(double(s(s(0())))))
    Subterm Criterion Processor:
     simple projection:
      pi(lt#) = 1
     problem:
      DPs:
       
      TRS:
       1024() -> 1024_1(0())
       1024_1(x) -> if(lt(x,10()),x)
       if(true(),x) -> double(1024_1(s(x)))
       if(false(),x) -> s(0())
       lt(0(),s(y)) -> true()
       lt(x,0()) -> false()
       lt(s(x),s(y)) -> lt(x,y)
       double(0()) -> 0()
       double(s(x)) -> s(s(double(x)))
       10() -> double(s(double(s(s(0())))))
     Qed
    
    DPs:
     double#(s(x)) -> double#(x)
    TRS:
     1024() -> 1024_1(0())
     1024_1(x) -> if(lt(x,10()),x)
     if(true(),x) -> double(1024_1(s(x)))
     if(false(),x) -> s(0())
     lt(0(),s(y)) -> true()
     lt(x,0()) -> false()
     lt(s(x),s(y)) -> lt(x,y)
     double(0()) -> 0()
     double(s(x)) -> s(s(double(x)))
     10() -> double(s(double(s(s(0())))))
    Subterm Criterion Processor:
     simple projection:
      pi(double#) = 0
     problem:
      DPs:
       
      TRS:
       1024() -> 1024_1(0())
       1024_1(x) -> if(lt(x,10()),x)
       if(true(),x) -> double(1024_1(s(x)))
       if(false(),x) -> s(0())
       lt(0(),s(y)) -> true()
       lt(x,0()) -> false()
       lt(s(x),s(y)) -> lt(x,y)
       double(0()) -> 0()
       double(s(x)) -> s(s(double(x)))
       10() -> double(s(double(s(s(0())))))
     Qed