MAYBE
* Step 1: DependencyPairs MAYBE
    + Considered Problem:
        - Strict TRS:
            double(0()) -> 0()
            double(s(x)) -> s(s(double(x)))
            exp(0()) -> s(0())
            exp(s(x)) -> double(exp(x))
            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))
            half(0()) -> double(0())
            half(s(0())) -> half(0())
            half(s(s(x))) -> s(half(x))
            tower(x) -> f(a(),x,s(0()))
        - Signature:
            {double/1,exp/1,f/3,half/1,tower/1} / {0/0,a/0,b/0,s/1}
        - Obligation:
            innermost runtime complexity wrt. defined symbols {double,exp,f,half,tower} and constructors {0,a,b,s}
    + Applied Processor:
        DependencyPairs {dpKind_ = DT}
    + Details:
        We add the following dependency tuples:
        
        Strict DPs
          double#(0()) -> c_1()
          double#(s(x)) -> c_2(double#(x))
          exp#(0()) -> c_3()
          exp#(s(x)) -> c_4(double#(exp(x)),exp#(x))
          f#(a(),0(),y) -> c_5()
          f#(a(),s(x),y) -> c_6(f#(b(),y,s(x)))
          f#(b(),y,x) -> c_7(f#(a(),half(x),exp(y)),half#(x),exp#(y))
          half#(0()) -> c_8(double#(0()))
          half#(s(0())) -> c_9(half#(0()))
          half#(s(s(x))) -> c_10(half#(x))
          tower#(x) -> c_11(f#(a(),x,s(0())))
        Weak DPs
          
        
        and mark the set of starting terms.
* Step 2: UsableRules MAYBE
    + Considered Problem:
        - Strict DPs:
            double#(0()) -> c_1()
            double#(s(x)) -> c_2(double#(x))
            exp#(0()) -> c_3()
            exp#(s(x)) -> c_4(double#(exp(x)),exp#(x))
            f#(a(),0(),y) -> c_5()
            f#(a(),s(x),y) -> c_6(f#(b(),y,s(x)))
            f#(b(),y,x) -> c_7(f#(a(),half(x),exp(y)),half#(x),exp#(y))
            half#(0()) -> c_8(double#(0()))
            half#(s(0())) -> c_9(half#(0()))
            half#(s(s(x))) -> c_10(half#(x))
            tower#(x) -> c_11(f#(a(),x,s(0())))
        - Weak TRS:
            double(0()) -> 0()
            double(s(x)) -> s(s(double(x)))
            exp(0()) -> s(0())
            exp(s(x)) -> double(exp(x))
            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))
            half(0()) -> double(0())
            half(s(0())) -> half(0())
            half(s(s(x))) -> s(half(x))
            tower(x) -> f(a(),x,s(0()))
        - Signature:
            {double/1,exp/1,f/3,half/1,tower/1,double#/1,exp#/1,f#/3,half#/1,tower#/1} / {0/0,a/0,b/0,s/1,c_1/0,c_2/1
            ,c_3/0,c_4/2,c_5/0,c_6/1,c_7/3,c_8/1,c_9/1,c_10/1,c_11/1}
        - Obligation:
            innermost runtime complexity wrt. defined symbols {double#,exp#,f#,half#,tower#} and constructors {0,a,b,s}
    + Applied Processor:
        UsableRules
    + Details:
        We replace rewrite rules by usable rules:
          double(0()) -> 0()
          double(s(x)) -> s(s(double(x)))
          exp(0()) -> s(0())
          exp(s(x)) -> double(exp(x))
          half(0()) -> double(0())
          half(s(0())) -> half(0())
          half(s(s(x))) -> s(half(x))
          double#(0()) -> c_1()
          double#(s(x)) -> c_2(double#(x))
          exp#(0()) -> c_3()
          exp#(s(x)) -> c_4(double#(exp(x)),exp#(x))
          f#(a(),0(),y) -> c_5()
          f#(a(),s(x),y) -> c_6(f#(b(),y,s(x)))
          f#(b(),y,x) -> c_7(f#(a(),half(x),exp(y)),half#(x),exp#(y))
          half#(0()) -> c_8(double#(0()))
          half#(s(0())) -> c_9(half#(0()))
          half#(s(s(x))) -> c_10(half#(x))
          tower#(x) -> c_11(f#(a(),x,s(0())))
* Step 3: PredecessorEstimation MAYBE
    + Considered Problem:
        - Strict DPs:
            double#(0()) -> c_1()
            double#(s(x)) -> c_2(double#(x))
            exp#(0()) -> c_3()
            exp#(s(x)) -> c_4(double#(exp(x)),exp#(x))
            f#(a(),0(),y) -> c_5()
            f#(a(),s(x),y) -> c_6(f#(b(),y,s(x)))
            f#(b(),y,x) -> c_7(f#(a(),half(x),exp(y)),half#(x),exp#(y))
            half#(0()) -> c_8(double#(0()))
            half#(s(0())) -> c_9(half#(0()))
            half#(s(s(x))) -> c_10(half#(x))
            tower#(x) -> c_11(f#(a(),x,s(0())))
        - Weak TRS:
            double(0()) -> 0()
            double(s(x)) -> s(s(double(x)))
            exp(0()) -> s(0())
            exp(s(x)) -> double(exp(x))
            half(0()) -> double(0())
            half(s(0())) -> half(0())
            half(s(s(x))) -> s(half(x))
        - Signature:
            {double/1,exp/1,f/3,half/1,tower/1,double#/1,exp#/1,f#/3,half#/1,tower#/1} / {0/0,a/0,b/0,s/1,c_1/0,c_2/1
            ,c_3/0,c_4/2,c_5/0,c_6/1,c_7/3,c_8/1,c_9/1,c_10/1,c_11/1}
        - Obligation:
            innermost runtime complexity wrt. defined symbols {double#,exp#,f#,half#,tower#} and constructors {0,a,b,s}
    + Applied Processor:
        PredecessorEstimation {onSelection = all simple predecessor estimation selector}
    + Details:
        We estimate the number of application of
          {1,3,5}
        by application of
          Pre({1,3,5}) = {2,4,7,8,11}.
        Here rules are labelled as follows:
          1: double#(0()) -> c_1()
          2: double#(s(x)) -> c_2(double#(x))
          3: exp#(0()) -> c_3()
          4: exp#(s(x)) -> c_4(double#(exp(x)),exp#(x))
          5: f#(a(),0(),y) -> c_5()
          6: f#(a(),s(x),y) -> c_6(f#(b(),y,s(x)))
          7: f#(b(),y,x) -> c_7(f#(a(),half(x),exp(y)),half#(x),exp#(y))
          8: half#(0()) -> c_8(double#(0()))
          9: half#(s(0())) -> c_9(half#(0()))
          10: half#(s(s(x))) -> c_10(half#(x))
          11: tower#(x) -> c_11(f#(a(),x,s(0())))
* Step 4: PredecessorEstimation MAYBE
    + Considered Problem:
        - Strict DPs:
            double#(s(x)) -> c_2(double#(x))
            exp#(s(x)) -> c_4(double#(exp(x)),exp#(x))
            f#(a(),s(x),y) -> c_6(f#(b(),y,s(x)))
            f#(b(),y,x) -> c_7(f#(a(),half(x),exp(y)),half#(x),exp#(y))
            half#(0()) -> c_8(double#(0()))
            half#(s(0())) -> c_9(half#(0()))
            half#(s(s(x))) -> c_10(half#(x))
            tower#(x) -> c_11(f#(a(),x,s(0())))
        - Weak DPs:
            double#(0()) -> c_1()
            exp#(0()) -> c_3()
            f#(a(),0(),y) -> c_5()
        - Weak TRS:
            double(0()) -> 0()
            double(s(x)) -> s(s(double(x)))
            exp(0()) -> s(0())
            exp(s(x)) -> double(exp(x))
            half(0()) -> double(0())
            half(s(0())) -> half(0())
            half(s(s(x))) -> s(half(x))
        - Signature:
            {double/1,exp/1,f/3,half/1,tower/1,double#/1,exp#/1,f#/3,half#/1,tower#/1} / {0/0,a/0,b/0,s/1,c_1/0,c_2/1
            ,c_3/0,c_4/2,c_5/0,c_6/1,c_7/3,c_8/1,c_9/1,c_10/1,c_11/1}
        - Obligation:
            innermost runtime complexity wrt. defined symbols {double#,exp#,f#,half#,tower#} and constructors {0,a,b,s}
    + Applied Processor:
        PredecessorEstimation {onSelection = all simple predecessor estimation selector}
    + Details:
        We estimate the number of application of
          {5}
        by application of
          Pre({5}) = {4,6,7}.
        Here rules are labelled as follows:
          1: double#(s(x)) -> c_2(double#(x))
          2: exp#(s(x)) -> c_4(double#(exp(x)),exp#(x))
          3: f#(a(),s(x),y) -> c_6(f#(b(),y,s(x)))
          4: f#(b(),y,x) -> c_7(f#(a(),half(x),exp(y)),half#(x),exp#(y))
          5: half#(0()) -> c_8(double#(0()))
          6: half#(s(0())) -> c_9(half#(0()))
          7: half#(s(s(x))) -> c_10(half#(x))
          8: tower#(x) -> c_11(f#(a(),x,s(0())))
          9: double#(0()) -> c_1()
          10: exp#(0()) -> c_3()
          11: f#(a(),0(),y) -> c_5()
* Step 5: PredecessorEstimation MAYBE
    + Considered Problem:
        - Strict DPs:
            double#(s(x)) -> c_2(double#(x))
            exp#(s(x)) -> c_4(double#(exp(x)),exp#(x))
            f#(a(),s(x),y) -> c_6(f#(b(),y,s(x)))
            f#(b(),y,x) -> c_7(f#(a(),half(x),exp(y)),half#(x),exp#(y))
            half#(s(0())) -> c_9(half#(0()))
            half#(s(s(x))) -> c_10(half#(x))
            tower#(x) -> c_11(f#(a(),x,s(0())))
        - Weak DPs:
            double#(0()) -> c_1()
            exp#(0()) -> c_3()
            f#(a(),0(),y) -> c_5()
            half#(0()) -> c_8(double#(0()))
        - Weak TRS:
            double(0()) -> 0()
            double(s(x)) -> s(s(double(x)))
            exp(0()) -> s(0())
            exp(s(x)) -> double(exp(x))
            half(0()) -> double(0())
            half(s(0())) -> half(0())
            half(s(s(x))) -> s(half(x))
        - Signature:
            {double/1,exp/1,f/3,half/1,tower/1,double#/1,exp#/1,f#/3,half#/1,tower#/1} / {0/0,a/0,b/0,s/1,c_1/0,c_2/1
            ,c_3/0,c_4/2,c_5/0,c_6/1,c_7/3,c_8/1,c_9/1,c_10/1,c_11/1}
        - Obligation:
            innermost runtime complexity wrt. defined symbols {double#,exp#,f#,half#,tower#} and constructors {0,a,b,s}
    + Applied Processor:
        PredecessorEstimation {onSelection = all simple predecessor estimation selector}
    + Details:
        We estimate the number of application of
          {5}
        by application of
          Pre({5}) = {4,6}.
        Here rules are labelled as follows:
          1: double#(s(x)) -> c_2(double#(x))
          2: exp#(s(x)) -> c_4(double#(exp(x)),exp#(x))
          3: f#(a(),s(x),y) -> c_6(f#(b(),y,s(x)))
          4: f#(b(),y,x) -> c_7(f#(a(),half(x),exp(y)),half#(x),exp#(y))
          5: half#(s(0())) -> c_9(half#(0()))
          6: half#(s(s(x))) -> c_10(half#(x))
          7: tower#(x) -> c_11(f#(a(),x,s(0())))
          8: double#(0()) -> c_1()
          9: exp#(0()) -> c_3()
          10: f#(a(),0(),y) -> c_5()
          11: half#(0()) -> c_8(double#(0()))
* Step 6: RemoveWeakSuffixes MAYBE
    + Considered Problem:
        - Strict DPs:
            double#(s(x)) -> c_2(double#(x))
            exp#(s(x)) -> c_4(double#(exp(x)),exp#(x))
            f#(a(),s(x),y) -> c_6(f#(b(),y,s(x)))
            f#(b(),y,x) -> c_7(f#(a(),half(x),exp(y)),half#(x),exp#(y))
            half#(s(s(x))) -> c_10(half#(x))
            tower#(x) -> c_11(f#(a(),x,s(0())))
        - Weak DPs:
            double#(0()) -> c_1()
            exp#(0()) -> c_3()
            f#(a(),0(),y) -> c_5()
            half#(0()) -> c_8(double#(0()))
            half#(s(0())) -> c_9(half#(0()))
        - Weak TRS:
            double(0()) -> 0()
            double(s(x)) -> s(s(double(x)))
            exp(0()) -> s(0())
            exp(s(x)) -> double(exp(x))
            half(0()) -> double(0())
            half(s(0())) -> half(0())
            half(s(s(x))) -> s(half(x))
        - Signature:
            {double/1,exp/1,f/3,half/1,tower/1,double#/1,exp#/1,f#/3,half#/1,tower#/1} / {0/0,a/0,b/0,s/1,c_1/0,c_2/1
            ,c_3/0,c_4/2,c_5/0,c_6/1,c_7/3,c_8/1,c_9/1,c_10/1,c_11/1}
        - Obligation:
            innermost runtime complexity wrt. defined symbols {double#,exp#,f#,half#,tower#} and constructors {0,a,b,s}
    + Applied Processor:
        RemoveWeakSuffixes
    + Details:
        Consider the dependency graph
          1:S:double#(s(x)) -> c_2(double#(x))
             -->_1 double#(0()) -> c_1():7
             -->_1 double#(s(x)) -> c_2(double#(x)):1
          
          2:S:exp#(s(x)) -> c_4(double#(exp(x)),exp#(x))
             -->_2 exp#(0()) -> c_3():8
             -->_1 double#(0()) -> c_1():7
             -->_2 exp#(s(x)) -> c_4(double#(exp(x)),exp#(x)):2
             -->_1 double#(s(x)) -> c_2(double#(x)):1
          
          3:S:f#(a(),s(x),y) -> c_6(f#(b(),y,s(x)))
             -->_1 f#(b(),y,x) -> c_7(f#(a(),half(x),exp(y)),half#(x),exp#(y)):4
          
          4:S:f#(b(),y,x) -> c_7(f#(a(),half(x),exp(y)),half#(x),exp#(y))
             -->_2 half#(s(0())) -> c_9(half#(0())):11
             -->_2 half#(0()) -> c_8(double#(0())):10
             -->_2 half#(s(s(x))) -> c_10(half#(x)):5
             -->_1 f#(a(),0(),y) -> c_5():9
             -->_3 exp#(0()) -> c_3():8
             -->_1 f#(a(),s(x),y) -> c_6(f#(b(),y,s(x))):3
             -->_3 exp#(s(x)) -> c_4(double#(exp(x)),exp#(x)):2
          
          5:S:half#(s(s(x))) -> c_10(half#(x))
             -->_1 half#(s(0())) -> c_9(half#(0())):11
             -->_1 half#(0()) -> c_8(double#(0())):10
             -->_1 half#(s(s(x))) -> c_10(half#(x)):5
          
          6:S:tower#(x) -> c_11(f#(a(),x,s(0())))
             -->_1 f#(a(),0(),y) -> c_5():9
             -->_1 f#(a(),s(x),y) -> c_6(f#(b(),y,s(x))):3
          
          7:W:double#(0()) -> c_1()
             
          
          8:W:exp#(0()) -> c_3()
             
          
          9:W:f#(a(),0(),y) -> c_5()
             
          
          10:W:half#(0()) -> c_8(double#(0()))
             -->_1 double#(0()) -> c_1():7
          
          11:W:half#(s(0())) -> c_9(half#(0()))
             -->_1 half#(0()) -> c_8(double#(0())):10
          
        The following weak DPs constitute a sub-graph of the DG that is closed under successors. The DPs are removed.
          9: f#(a(),0(),y) -> c_5()
          11: half#(s(0())) -> c_9(half#(0()))
          10: half#(0()) -> c_8(double#(0()))
          8: exp#(0()) -> c_3()
          7: double#(0()) -> c_1()
* Step 7: RemoveHeads MAYBE
    + Considered Problem:
        - Strict DPs:
            double#(s(x)) -> c_2(double#(x))
            exp#(s(x)) -> c_4(double#(exp(x)),exp#(x))
            f#(a(),s(x),y) -> c_6(f#(b(),y,s(x)))
            f#(b(),y,x) -> c_7(f#(a(),half(x),exp(y)),half#(x),exp#(y))
            half#(s(s(x))) -> c_10(half#(x))
            tower#(x) -> c_11(f#(a(),x,s(0())))
        - Weak TRS:
            double(0()) -> 0()
            double(s(x)) -> s(s(double(x)))
            exp(0()) -> s(0())
            exp(s(x)) -> double(exp(x))
            half(0()) -> double(0())
            half(s(0())) -> half(0())
            half(s(s(x))) -> s(half(x))
        - Signature:
            {double/1,exp/1,f/3,half/1,tower/1,double#/1,exp#/1,f#/3,half#/1,tower#/1} / {0/0,a/0,b/0,s/1,c_1/0,c_2/1
            ,c_3/0,c_4/2,c_5/0,c_6/1,c_7/3,c_8/1,c_9/1,c_10/1,c_11/1}
        - Obligation:
            innermost runtime complexity wrt. defined symbols {double#,exp#,f#,half#,tower#} and constructors {0,a,b,s}
    + Applied Processor:
        RemoveHeads
    + Details:
        Consider the dependency graph
        
        1:S:double#(s(x)) -> c_2(double#(x))
           -->_1 double#(s(x)) -> c_2(double#(x)):1
        
        2:S:exp#(s(x)) -> c_4(double#(exp(x)),exp#(x))
           -->_2 exp#(s(x)) -> c_4(double#(exp(x)),exp#(x)):2
           -->_1 double#(s(x)) -> c_2(double#(x)):1
        
        3:S:f#(a(),s(x),y) -> c_6(f#(b(),y,s(x)))
           -->_1 f#(b(),y,x) -> c_7(f#(a(),half(x),exp(y)),half#(x),exp#(y)):4
        
        4:S:f#(b(),y,x) -> c_7(f#(a(),half(x),exp(y)),half#(x),exp#(y))
           -->_2 half#(s(s(x))) -> c_10(half#(x)):5
           -->_1 f#(a(),s(x),y) -> c_6(f#(b(),y,s(x))):3
           -->_3 exp#(s(x)) -> c_4(double#(exp(x)),exp#(x)):2
        
        5:S:half#(s(s(x))) -> c_10(half#(x))
           -->_1 half#(s(s(x))) -> c_10(half#(x)):5
        
        6:S:tower#(x) -> c_11(f#(a(),x,s(0())))
           -->_1 f#(a(),s(x),y) -> c_6(f#(b(),y,s(x))):3
        
        
        Following roots of the dependency graph are removed, as the considered set of starting terms is closed under reduction with respect to these rules (modulo compound contexts).
        
        [(6,tower#(x) -> c_11(f#(a(),x,s(0()))))]
* Step 8: Failure MAYBE
  + Considered Problem:
      - Strict DPs:
          double#(s(x)) -> c_2(double#(x))
          exp#(s(x)) -> c_4(double#(exp(x)),exp#(x))
          f#(a(),s(x),y) -> c_6(f#(b(),y,s(x)))
          f#(b(),y,x) -> c_7(f#(a(),half(x),exp(y)),half#(x),exp#(y))
          half#(s(s(x))) -> c_10(half#(x))
      - Weak TRS:
          double(0()) -> 0()
          double(s(x)) -> s(s(double(x)))
          exp(0()) -> s(0())
          exp(s(x)) -> double(exp(x))
          half(0()) -> double(0())
          half(s(0())) -> half(0())
          half(s(s(x))) -> s(half(x))
      - Signature:
          {double/1,exp/1,f/3,half/1,tower/1,double#/1,exp#/1,f#/3,half#/1,tower#/1} / {0/0,a/0,b/0,s/1,c_1/0,c_2/1
          ,c_3/0,c_4/2,c_5/0,c_6/1,c_7/3,c_8/1,c_9/1,c_10/1,c_11/1}
      - Obligation:
          innermost runtime complexity wrt. defined symbols {double#,exp#,f#,half#,tower#} and constructors {0,a,b,s}
  + Applied Processor:
      EmptyProcessor
  + Details:
      The problem is still open.
MAYBE