MAYBE

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())))))
  TDG 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) -> if#(lt(x,10()),x)
    if#(true(),x) -> 1024_1#(s(x)) -> 1024_1#(x) -> lt#(x,10())
    if#(true(),x) -> 1024_1#(s(x)) -> 1024_1#(x) -> 10#()
    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) -> double#(1024_1(s(x)))
    1024_1#(x) -> if#(lt(x,10()),x) -> if#(true(),x) -> 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(double(s(s(0())))))
    1024_1#(x) -> 10#() -> 10#() -> double#(s(s(0())))
    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#()
   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())))))
    Open
    
    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