MAYBE

Problem:
 tower(x) -> f(a(),x,s(0()))
 f(a(),0(),y) -> y
 f(a(),s(x),y) -> f(b(),y,s(x))
 f(b(),y,x) -> f(a(),half(x),exp(y))
 exp(0()) -> s(0())
 exp(s(x)) -> double(exp(x))
 double(0()) -> 0()
 double(s(x)) -> s(s(double(x)))
 half(0()) -> double(0())
 half(s(0())) -> half(0())
 half(s(s(x))) -> s(half(x))

Proof:
 DP Processor:
  DPs:
   tower#(x) -> f#(a(),x,s(0()))
   f#(a(),s(x),y) -> f#(b(),y,s(x))
   f#(b(),y,x) -> exp#(y)
   f#(b(),y,x) -> half#(x)
   f#(b(),y,x) -> f#(a(),half(x),exp(y))
   exp#(s(x)) -> exp#(x)
   exp#(s(x)) -> double#(exp(x))
   double#(s(x)) -> double#(x)
   half#(0()) -> double#(0())
   half#(s(0())) -> half#(0())
   half#(s(s(x))) -> half#(x)
  TRS:
   tower(x) -> f(a(),x,s(0()))
   f(a(),0(),y) -> y
   f(a(),s(x),y) -> f(b(),y,s(x))
   f(b(),y,x) -> f(a(),half(x),exp(y))
   exp(0()) -> s(0())
   exp(s(x)) -> double(exp(x))
   double(0()) -> 0()
   double(s(x)) -> s(s(double(x)))
   half(0()) -> double(0())
   half(s(0())) -> half(0())
   half(s(s(x))) -> s(half(x))
  TDG Processor:
   DPs:
    tower#(x) -> f#(a(),x,s(0()))
    f#(a(),s(x),y) -> f#(b(),y,s(x))
    f#(b(),y,x) -> exp#(y)
    f#(b(),y,x) -> half#(x)
    f#(b(),y,x) -> f#(a(),half(x),exp(y))
    exp#(s(x)) -> exp#(x)
    exp#(s(x)) -> double#(exp(x))
    double#(s(x)) -> double#(x)
    half#(0()) -> double#(0())
    half#(s(0())) -> half#(0())
    half#(s(s(x))) -> half#(x)
   TRS:
    tower(x) -> f(a(),x,s(0()))
    f(a(),0(),y) -> y
    f(a(),s(x),y) -> f(b(),y,s(x))
    f(b(),y,x) -> f(a(),half(x),exp(y))
    exp(0()) -> s(0())
    exp(s(x)) -> double(exp(x))
    double(0()) -> 0()
    double(s(x)) -> s(s(double(x)))
    half(0()) -> double(0())
    half(s(0())) -> half(0())
    half(s(s(x))) -> s(half(x))
   graph:
    double#(s(x)) -> double#(x) -> double#(s(x)) -> double#(x)
    half#(s(s(x))) -> half#(x) -> half#(s(s(x))) -> half#(x)
    half#(s(s(x))) -> half#(x) -> half#(s(0())) -> half#(0())
    half#(s(s(x))) -> half#(x) -> half#(0()) -> double#(0())
    half#(s(0())) -> half#(0()) -> half#(s(s(x))) -> half#(x)
    half#(s(0())) -> half#(0()) -> half#(s(0())) -> half#(0())
    half#(s(0())) -> half#(0()) -> half#(0()) -> double#(0())
    half#(0()) -> double#(0()) -> double#(s(x)) -> double#(x)
    exp#(s(x)) -> double#(exp(x)) -> double#(s(x)) -> double#(x)
    exp#(s(x)) -> exp#(x) -> exp#(s(x)) -> double#(exp(x))
    exp#(s(x)) -> exp#(x) -> exp#(s(x)) -> exp#(x)
    f#(b(),y,x) -> half#(x) -> half#(s(s(x))) -> half#(x)
    f#(b(),y,x) -> half#(x) -> half#(s(0())) -> half#(0())
    f#(b(),y,x) -> half#(x) -> half#(0()) -> double#(0())
    f#(b(),y,x) -> exp#(y) -> exp#(s(x)) -> double#(exp(x))
    f#(b(),y,x) -> exp#(y) -> exp#(s(x)) -> exp#(x)
    f#(b(),y,x) -> f#(a(),half(x),exp(y)) ->
    f#(b(),y,x) -> f#(a(),half(x),exp(y))
    f#(b(),y,x) -> f#(a(),half(x),exp(y)) ->
    f#(b(),y,x) -> half#(x)
    f#(b(),y,x) -> f#(a(),half(x),exp(y)) ->
    f#(b(),y,x) -> exp#(y)
    f#(b(),y,x) -> f#(a(),half(x),exp(y)) ->
    f#(a(),s(x),y) -> f#(b(),y,s(x))
    f#(a(),s(x),y) -> f#(b(),y,s(x)) ->
    f#(b(),y,x) -> f#(a(),half(x),exp(y))
    f#(a(),s(x),y) -> f#(b(),y,s(x)) -> f#(b(),y,x) -> half#(x)
    f#(a(),s(x),y) -> f#(b(),y,s(x)) -> f#(b(),y,x) -> exp#(y)
    f#(a(),s(x),y) -> f#(b(),y,s(x)) ->
    f#(a(),s(x),y) -> f#(b(),y,s(x))
    tower#(x) -> f#(a(),x,s(0())) ->
    f#(b(),y,x) -> f#(a(),half(x),exp(y))
    tower#(x) -> f#(a(),x,s(0())) -> f#(b(),y,x) -> half#(x)
    tower#(x) -> f#(a(),x,s(0())) -> f#(b(),y,x) -> exp#(y)
    tower#(x) -> f#(a(),x,s(0())) -> f#(a(),s(x),y) -> f#(b(),y,s(x))
   SCC Processor:
    #sccs: 4
    #rules: 6
    #arcs: 28/121
    DPs:
     f#(b(),y,x) -> f#(a(),half(x),exp(y))
     f#(a(),s(x),y) -> f#(b(),y,s(x))
    TRS:
     tower(x) -> f(a(),x,s(0()))
     f(a(),0(),y) -> y
     f(a(),s(x),y) -> f(b(),y,s(x))
     f(b(),y,x) -> f(a(),half(x),exp(y))
     exp(0()) -> s(0())
     exp(s(x)) -> double(exp(x))
     double(0()) -> 0()
     double(s(x)) -> s(s(double(x)))
     half(0()) -> double(0())
     half(s(0())) -> half(0())
     half(s(s(x))) -> s(half(x))
    EDG Processor:
     DPs:
      f#(b(),y,x) -> f#(a(),half(x),exp(y))
      f#(a(),s(x),y) -> f#(b(),y,s(x))
     TRS:
      tower(x) -> f(a(),x,s(0()))
      f(a(),0(),y) -> y
      f(a(),s(x),y) -> f(b(),y,s(x))
      f(b(),y,x) -> f(a(),half(x),exp(y))
      exp(0()) -> s(0())
      exp(s(x)) -> double(exp(x))
      double(0()) -> 0()
      double(s(x)) -> s(s(double(x)))
      half(0()) -> double(0())
      half(s(0())) -> half(0())
      half(s(s(x))) -> s(half(x))
     graph:
      f#(b(),y,x) -> f#(a(),half(x),exp(y)) ->
      f#(a(),s(x),y) -> f#(b(),y,s(x))
      f#(a(),s(x),y) -> f#(b(),y,s(x)) -> f#(b(),y,x) -> f#(a(),half(x),exp(y))
     Open
    
    DPs:
     exp#(s(x)) -> exp#(x)
    TRS:
     tower(x) -> f(a(),x,s(0()))
     f(a(),0(),y) -> y
     f(a(),s(x),y) -> f(b(),y,s(x))
     f(b(),y,x) -> f(a(),half(x),exp(y))
     exp(0()) -> s(0())
     exp(s(x)) -> double(exp(x))
     double(0()) -> 0()
     double(s(x)) -> s(s(double(x)))
     half(0()) -> double(0())
     half(s(0())) -> half(0())
     half(s(s(x))) -> s(half(x))
    Subterm Criterion Processor:
     simple projection:
      pi(exp#) = 0
     problem:
      DPs:
       
      TRS:
       tower(x) -> f(a(),x,s(0()))
       f(a(),0(),y) -> y
       f(a(),s(x),y) -> f(b(),y,s(x))
       f(b(),y,x) -> f(a(),half(x),exp(y))
       exp(0()) -> s(0())
       exp(s(x)) -> double(exp(x))
       double(0()) -> 0()
       double(s(x)) -> s(s(double(x)))
       half(0()) -> double(0())
       half(s(0())) -> half(0())
       half(s(s(x))) -> s(half(x))
     Qed
    
    DPs:
     half#(s(s(x))) -> half#(x)
     half#(s(0())) -> half#(0())
    TRS:
     tower(x) -> f(a(),x,s(0()))
     f(a(),0(),y) -> y
     f(a(),s(x),y) -> f(b(),y,s(x))
     f(b(),y,x) -> f(a(),half(x),exp(y))
     exp(0()) -> s(0())
     exp(s(x)) -> double(exp(x))
     double(0()) -> 0()
     double(s(x)) -> s(s(double(x)))
     half(0()) -> double(0())
     half(s(0())) -> half(0())
     half(s(s(x))) -> s(half(x))
    Subterm Criterion Processor:
     simple projection:
      pi(half#) = 0
     problem:
      DPs:
       
      TRS:
       tower(x) -> f(a(),x,s(0()))
       f(a(),0(),y) -> y
       f(a(),s(x),y) -> f(b(),y,s(x))
       f(b(),y,x) -> f(a(),half(x),exp(y))
       exp(0()) -> s(0())
       exp(s(x)) -> double(exp(x))
       double(0()) -> 0()
       double(s(x)) -> s(s(double(x)))
       half(0()) -> double(0())
       half(s(0())) -> half(0())
       half(s(s(x))) -> s(half(x))
     Qed
    
    DPs:
     double#(s(x)) -> double#(x)
    TRS:
     tower(x) -> f(a(),x,s(0()))
     f(a(),0(),y) -> y
     f(a(),s(x),y) -> f(b(),y,s(x))
     f(b(),y,x) -> f(a(),half(x),exp(y))
     exp(0()) -> s(0())
     exp(s(x)) -> double(exp(x))
     double(0()) -> 0()
     double(s(x)) -> s(s(double(x)))
     half(0()) -> double(0())
     half(s(0())) -> half(0())
     half(s(s(x))) -> s(half(x))
    Subterm Criterion Processor:
     simple projection:
      pi(double#) = 0
     problem:
      DPs:
       
      TRS:
       tower(x) -> f(a(),x,s(0()))
       f(a(),0(),y) -> y
       f(a(),s(x),y) -> f(b(),y,s(x))
       f(b(),y,x) -> f(a(),half(x),exp(y))
       exp(0()) -> s(0())
       exp(s(x)) -> double(exp(x))
       double(0()) -> 0()
       double(s(x)) -> s(s(double(x)))
       half(0()) -> double(0())
       half(s(0())) -> half(0())
       half(s(s(x))) -> s(half(x))
     Qed