MAYBE

Problem:
 f(tt(),x) -> f(eq(x,half(double(x))),s(x))
 eq(s(x),s(y)) -> eq(x,y)
 eq(0(),0()) -> tt()
 double(s(x)) -> s(s(double(x)))
 double(0()) -> 0()
 half(s(s(x))) -> s(half(x))
 half(0()) -> 0()

Proof:
 DP Processor:
  DPs:
   f#(tt(),x) -> double#(x)
   f#(tt(),x) -> half#(double(x))
   f#(tt(),x) -> eq#(x,half(double(x)))
   f#(tt(),x) -> f#(eq(x,half(double(x))),s(x))
   eq#(s(x),s(y)) -> eq#(x,y)
   double#(s(x)) -> double#(x)
   half#(s(s(x))) -> half#(x)
  TRS:
   f(tt(),x) -> f(eq(x,half(double(x))),s(x))
   eq(s(x),s(y)) -> eq(x,y)
   eq(0(),0()) -> tt()
   double(s(x)) -> s(s(double(x)))
   double(0()) -> 0()
   half(s(s(x))) -> s(half(x))
   half(0()) -> 0()
  TDG Processor:
   DPs:
    f#(tt(),x) -> double#(x)
    f#(tt(),x) -> half#(double(x))
    f#(tt(),x) -> eq#(x,half(double(x)))
    f#(tt(),x) -> f#(eq(x,half(double(x))),s(x))
    eq#(s(x),s(y)) -> eq#(x,y)
    double#(s(x)) -> double#(x)
    half#(s(s(x))) -> half#(x)
   TRS:
    f(tt(),x) -> f(eq(x,half(double(x))),s(x))
    eq(s(x),s(y)) -> eq(x,y)
    eq(0(),0()) -> tt()
    double(s(x)) -> s(s(double(x)))
    double(0()) -> 0()
    half(s(s(x))) -> s(half(x))
    half(0()) -> 0()
   graph:
    eq#(s(x),s(y)) -> eq#(x,y) -> eq#(s(x),s(y)) -> eq#(x,y)
    half#(s(s(x))) -> half#(x) -> half#(s(s(x))) -> half#(x)
    double#(s(x)) -> double#(x) -> double#(s(x)) -> double#(x)
    f#(tt(),x) -> eq#(x,half(double(x))) ->
    eq#(s(x),s(y)) -> eq#(x,y)
    f#(tt(),x) -> half#(double(x)) -> half#(s(s(x))) -> half#(x)
    f#(tt(),x) -> double#(x) ->
    double#(s(x)) -> double#(x)
    f#(tt(),x) -> f#(eq(x,half(double(x))),s(x)) ->
    f#(tt(),x) -> f#(eq(x,half(double(x))),s(x))
    f#(tt(),x) -> f#(eq(x,half(double(x))),s(x)) ->
    f#(tt(),x) -> eq#(x,half(double(x)))
    f#(tt(),x) -> f#(eq(x,half(double(x))),s(x)) ->
    f#(tt(),x) -> half#(double(x))
    f#(tt(),x) -> f#(eq(x,half(double(x))),s(x)) -> f#(tt(),x) -> double#(x)
   SCC Processor:
    #sccs: 4
    #rules: 4
    #arcs: 10/49
    DPs:
     f#(tt(),x) -> f#(eq(x,half(double(x))),s(x))
    TRS:
     f(tt(),x) -> f(eq(x,half(double(x))),s(x))
     eq(s(x),s(y)) -> eq(x,y)
     eq(0(),0()) -> tt()
     double(s(x)) -> s(s(double(x)))
     double(0()) -> 0()
     half(s(s(x))) -> s(half(x))
     half(0()) -> 0()
    Open
    
    DPs:
     double#(s(x)) -> double#(x)
    TRS:
     f(tt(),x) -> f(eq(x,half(double(x))),s(x))
     eq(s(x),s(y)) -> eq(x,y)
     eq(0(),0()) -> tt()
     double(s(x)) -> s(s(double(x)))
     double(0()) -> 0()
     half(s(s(x))) -> s(half(x))
     half(0()) -> 0()
    Subterm Criterion Processor:
     simple projection:
      pi(double#) = 0
     problem:
      DPs:
       
      TRS:
       f(tt(),x) -> f(eq(x,half(double(x))),s(x))
       eq(s(x),s(y)) -> eq(x,y)
       eq(0(),0()) -> tt()
       double(s(x)) -> s(s(double(x)))
       double(0()) -> 0()
       half(s(s(x))) -> s(half(x))
       half(0()) -> 0()
     Qed
    
    DPs:
     half#(s(s(x))) -> half#(x)
    TRS:
     f(tt(),x) -> f(eq(x,half(double(x))),s(x))
     eq(s(x),s(y)) -> eq(x,y)
     eq(0(),0()) -> tt()
     double(s(x)) -> s(s(double(x)))
     double(0()) -> 0()
     half(s(s(x))) -> s(half(x))
     half(0()) -> 0()
    Subterm Criterion Processor:
     simple projection:
      pi(half#) = 0
     problem:
      DPs:
       
      TRS:
       f(tt(),x) -> f(eq(x,half(double(x))),s(x))
       eq(s(x),s(y)) -> eq(x,y)
       eq(0(),0()) -> tt()
       double(s(x)) -> s(s(double(x)))
       double(0()) -> 0()
       half(s(s(x))) -> s(half(x))
       half(0()) -> 0()
     Qed
    
    DPs:
     eq#(s(x),s(y)) -> eq#(x,y)
    TRS:
     f(tt(),x) -> f(eq(x,half(double(x))),s(x))
     eq(s(x),s(y)) -> eq(x,y)
     eq(0(),0()) -> tt()
     double(s(x)) -> s(s(double(x)))
     double(0()) -> 0()
     half(s(s(x))) -> s(half(x))
     half(0()) -> 0()
    Subterm Criterion Processor:
     simple projection:
      pi(eq#) = 1
     problem:
      DPs:
       
      TRS:
       f(tt(),x) -> f(eq(x,half(double(x))),s(x))
       eq(s(x),s(y)) -> eq(x,y)
       eq(0(),0()) -> tt()
       double(s(x)) -> s(s(double(x)))
       double(0()) -> 0()
       half(s(s(x))) -> s(half(x))
       half(0()) -> 0()
     Qed