MAYBE

Problem:
 g(x,0()) -> 0()
 g(d(),s(x)) -> s(s(g(d(),x)))
 g(h(),s(0())) -> 0()
 g(h(),s(s(x))) -> s(g(h(),x))
 double(x) -> g(d(),x)
 half(x) -> g(h(),x)
 f(s(x),y) -> f(half(s(x)),double(y))
 f(s(0()),y) -> y
 id(x) -> f(x,s(0()))

Proof:
 DP Processor:
  DPs:
   g#(d(),s(x)) -> g#(d(),x)
   g#(h(),s(s(x))) -> g#(h(),x)
   double#(x) -> g#(d(),x)
   half#(x) -> g#(h(),x)
   f#(s(x),y) -> double#(y)
   f#(s(x),y) -> half#(s(x))
   f#(s(x),y) -> f#(half(s(x)),double(y))
   id#(x) -> f#(x,s(0()))
  TRS:
   g(x,0()) -> 0()
   g(d(),s(x)) -> s(s(g(d(),x)))
   g(h(),s(0())) -> 0()
   g(h(),s(s(x))) -> s(g(h(),x))
   double(x) -> g(d(),x)
   half(x) -> g(h(),x)
   f(s(x),y) -> f(half(s(x)),double(y))
   f(s(0()),y) -> y
   id(x) -> f(x,s(0()))
  TDG Processor:
   DPs:
    g#(d(),s(x)) -> g#(d(),x)
    g#(h(),s(s(x))) -> g#(h(),x)
    double#(x) -> g#(d(),x)
    half#(x) -> g#(h(),x)
    f#(s(x),y) -> double#(y)
    f#(s(x),y) -> half#(s(x))
    f#(s(x),y) -> f#(half(s(x)),double(y))
    id#(x) -> f#(x,s(0()))
   TRS:
    g(x,0()) -> 0()
    g(d(),s(x)) -> s(s(g(d(),x)))
    g(h(),s(0())) -> 0()
    g(h(),s(s(x))) -> s(g(h(),x))
    double(x) -> g(d(),x)
    half(x) -> g(h(),x)
    f(s(x),y) -> f(half(s(x)),double(y))
    f(s(0()),y) -> y
    id(x) -> f(x,s(0()))
   graph:
    id#(x) -> f#(x,s(0())) -> f#(s(x),y) -> f#(half(s(x)),double(y))
    id#(x) -> f#(x,s(0())) -> f#(s(x),y) -> half#(s(x))
    id#(x) -> f#(x,s(0())) -> f#(s(x),y) -> double#(y)
    f#(s(x),y) -> f#(half(s(x)),double(y)) ->
    f#(s(x),y) -> f#(half(s(x)),double(y))
    f#(s(x),y) -> f#(half(s(x)),double(y)) ->
    f#(s(x),y) -> half#(s(x))
    f#(s(x),y) -> f#(half(s(x)),double(y)) -> f#(s(x),y) -> double#(y)
    f#(s(x),y) -> half#(s(x)) -> half#(x) -> g#(h(),x)
    f#(s(x),y) -> double#(y) -> double#(x) -> g#(d(),x)
    half#(x) -> g#(h(),x) -> g#(h(),s(s(x))) -> g#(h(),x)
    half#(x) -> g#(h(),x) -> g#(d(),s(x)) -> g#(d(),x)
    double#(x) -> g#(d(),x) -> g#(h(),s(s(x))) -> g#(h(),x)
    double#(x) -> g#(d(),x) -> g#(d(),s(x)) -> g#(d(),x)
    g#(h(),s(s(x))) -> g#(h(),x) -> g#(h(),s(s(x))) -> g#(h(),x)
    g#(h(),s(s(x))) -> g#(h(),x) -> g#(d(),s(x)) -> g#(d(),x)
    g#(d(),s(x)) -> g#(d(),x) -> g#(h(),s(s(x))) -> g#(h(),x)
    g#(d(),s(x)) -> g#(d(),x) -> g#(d(),s(x)) -> g#(d(),x)
   SCC Processor:
    #sccs: 2
    #rules: 3
    #arcs: 16/64
    DPs:
     f#(s(x),y) -> f#(half(s(x)),double(y))
    TRS:
     g(x,0()) -> 0()
     g(d(),s(x)) -> s(s(g(d(),x)))
     g(h(),s(0())) -> 0()
     g(h(),s(s(x))) -> s(g(h(),x))
     double(x) -> g(d(),x)
     half(x) -> g(h(),x)
     f(s(x),y) -> f(half(s(x)),double(y))
     f(s(0()),y) -> y
     id(x) -> f(x,s(0()))
    Open
    
    DPs:
     g#(d(),s(x)) -> g#(d(),x)
     g#(h(),s(s(x))) -> g#(h(),x)
    TRS:
     g(x,0()) -> 0()
     g(d(),s(x)) -> s(s(g(d(),x)))
     g(h(),s(0())) -> 0()
     g(h(),s(s(x))) -> s(g(h(),x))
     double(x) -> g(d(),x)
     half(x) -> g(h(),x)
     f(s(x),y) -> f(half(s(x)),double(y))
     f(s(0()),y) -> y
     id(x) -> f(x,s(0()))
    Subterm Criterion Processor:
     simple projection:
      pi(g#) = 1
     problem:
      DPs:
       
      TRS:
       g(x,0()) -> 0()
       g(d(),s(x)) -> s(s(g(d(),x)))
       g(h(),s(0())) -> 0()
       g(h(),s(s(x))) -> s(g(h(),x))
       double(x) -> g(d(),x)
       half(x) -> g(h(),x)
       f(s(x),y) -> f(half(s(x)),double(y))
       f(s(0()),y) -> y
       id(x) -> f(x,s(0()))
     Qed