MAYBE
* Step 1: InnermostRuleRemoval MAYBE
    + Considered Problem:
        - Strict TRS:
            0() -> n__0()
            activate(X) -> X
            activate(n__0()) -> 0()
            activate(n__s(X)) -> s(X)
            diff(X,Y) -> if(leq(X,Y),n__0(),n__s(diff(p(X),Y)))
            if(false(),X,Y) -> activate(Y)
            if(true(),X,Y) -> activate(X)
            leq(0(),Y) -> true()
            leq(s(X),0()) -> false()
            leq(s(X),s(Y)) -> leq(X,Y)
            p(0()) -> 0()
            p(s(X)) -> X
            s(X) -> n__s(X)
        - Signature:
            {0/0,activate/1,diff/2,if/3,leq/2,p/1,s/1} / {false/0,n__0/0,n__s/1,true/0}
        - Obligation:
            innermost runtime complexity wrt. defined symbols {0,activate,diff,if,leq,p,s} and constructors {false,n__0
            ,n__s,true}
    + Applied Processor:
        InnermostRuleRemoval
    + Details:
        Arguments of following rules are not normal-forms.
          leq(0(),Y) -> true()
          leq(s(X),0()) -> false()
          leq(s(X),s(Y)) -> leq(X,Y)
          p(0()) -> 0()
          p(s(X)) -> X
        All above mentioned rules can be savely removed.
* Step 2: WeightGap MAYBE
    + Considered Problem:
        - Strict TRS:
            0() -> n__0()
            activate(X) -> X
            activate(n__0()) -> 0()
            activate(n__s(X)) -> s(X)
            diff(X,Y) -> if(leq(X,Y),n__0(),n__s(diff(p(X),Y)))
            if(false(),X,Y) -> activate(Y)
            if(true(),X,Y) -> activate(X)
            s(X) -> n__s(X)
        - Signature:
            {0/0,activate/1,diff/2,if/3,leq/2,p/1,s/1} / {false/0,n__0/0,n__s/1,true/0}
        - Obligation:
            innermost runtime complexity wrt. defined symbols {0,activate,diff,if,leq,p,s} and constructors {false,n__0
            ,n__s,true}
    + Applied Processor:
        WeightGap {wgDimension = 1, wgDegree = 1, wgKind = Algebraic, wgUArgs = UArgs, wgOn = WgOnAny}
    + Details:
        The weightgap principle applies using the following nonconstant growth matrix-interpretation:
          We apply a matrix interpretation of kind constructor based matrix interpretation:
          The following argument positions are considered usable:
            uargs(if) = {3},
            uargs(n__s) = {1}
          
          Following symbols are considered usable:
            all
          TcT has computed the following interpretation:
                   p(0) = [0]                           
            p(activate) = [1] x1 + [12]                 
                p(diff) = [1] x1 + [0]                  
               p(false) = [0]                           
                  p(if) = [1] x1 + [1] x2 + [1] x3 + [3]
                 p(leq) = [8]                           
                p(n__0) = [4]                           
                p(n__s) = [1] x1 + [0]                  
                   p(p) = [1] x1 + [0]                  
                   p(s) = [1] x1 + [1]                  
                p(true) = [8]                           
          
          Following rules are strictly oriented:
                activate(X) = [1] X + [12]
                            > [1] X + [0] 
                            = X           
          
           activate(n__0()) = [16]        
                            > [0]         
                            = 0()         
          
          activate(n__s(X)) = [1] X + [12]
                            > [1] X + [1] 
                            = s(X)        
          
                       s(X) = [1] X + [1] 
                            > [1] X + [0] 
                            = n__s(X)     
          
          
          Following rules are (at-least) weakly oriented:
                      0() =  [0]                                   
                          >= [4]                                   
                          =  n__0()                                
          
                diff(X,Y) =  [1] X + [0]                           
                          >= [1] X + [15]                          
                          =  if(leq(X,Y),n__0(),n__s(diff(p(X),Y)))
          
          if(false(),X,Y) =  [1] X + [1] Y + [3]                   
                          >= [1] Y + [12]                          
                          =  activate(Y)                           
          
           if(true(),X,Y) =  [1] X + [1] Y + [11]                  
                          >= [1] X + [12]                          
                          =  activate(X)                           
          
        Further, it can be verified that all rules not oriented are covered by the weightgap condition.
* Step 3: WeightGap MAYBE
    + Considered Problem:
        - Strict TRS:
            0() -> n__0()
            diff(X,Y) -> if(leq(X,Y),n__0(),n__s(diff(p(X),Y)))
            if(false(),X,Y) -> activate(Y)
            if(true(),X,Y) -> activate(X)
        - Weak TRS:
            activate(X) -> X
            activate(n__0()) -> 0()
            activate(n__s(X)) -> s(X)
            s(X) -> n__s(X)
        - Signature:
            {0/0,activate/1,diff/2,if/3,leq/2,p/1,s/1} / {false/0,n__0/0,n__s/1,true/0}
        - Obligation:
            innermost runtime complexity wrt. defined symbols {0,activate,diff,if,leq,p,s} and constructors {false,n__0
            ,n__s,true}
    + Applied Processor:
        WeightGap {wgDimension = 1, wgDegree = 1, wgKind = Algebraic, wgUArgs = UArgs, wgOn = WgOnAny}
    + Details:
        The weightgap principle applies using the following nonconstant growth matrix-interpretation:
          We apply a matrix interpretation of kind constructor based matrix interpretation:
          The following argument positions are considered usable:
            uargs(if) = {3},
            uargs(n__s) = {1}
          
          Following symbols are considered usable:
            all
          TcT has computed the following interpretation:
                   p(0) = [1]                   
            p(activate) = [1] x1 + [1]          
                p(diff) = [1] x1 + [0]          
               p(false) = [0]                   
                  p(if) = [1] x2 + [1] x3 + [11]
                 p(leq) = [0]                   
                p(n__0) = [0]                   
                p(n__s) = [1] x1 + [0]          
                   p(p) = [0]                   
                   p(s) = [1] x1 + [1]          
                p(true) = [0]                   
          
          Following rules are strictly oriented:
                      0() = [1]                 
                          > [0]                 
                          = n__0()              
          
          if(false(),X,Y) = [1] X + [1] Y + [11]
                          > [1] Y + [1]         
                          = activate(Y)         
          
           if(true(),X,Y) = [1] X + [1] Y + [11]
                          > [1] X + [1]         
                          = activate(X)         
          
          
          Following rules are (at-least) weakly oriented:
                activate(X) =  [1] X + [1]                           
                            >= [1] X + [0]                           
                            =  X                                     
          
           activate(n__0()) =  [1]                                   
                            >= [1]                                   
                            =  0()                                   
          
          activate(n__s(X)) =  [1] X + [1]                           
                            >= [1] X + [1]                           
                            =  s(X)                                  
          
                  diff(X,Y) =  [1] X + [0]                           
                            >= [11]                                  
                            =  if(leq(X,Y),n__0(),n__s(diff(p(X),Y)))
          
                       s(X) =  [1] X + [1]                           
                            >= [1] X + [0]                           
                            =  n__s(X)                               
          
        Further, it can be verified that all rules not oriented are covered by the weightgap condition.
* Step 4: Failure MAYBE
  + Considered Problem:
      - Strict TRS:
          diff(X,Y) -> if(leq(X,Y),n__0(),n__s(diff(p(X),Y)))
      - Weak TRS:
          0() -> n__0()
          activate(X) -> X
          activate(n__0()) -> 0()
          activate(n__s(X)) -> s(X)
          if(false(),X,Y) -> activate(Y)
          if(true(),X,Y) -> activate(X)
          s(X) -> n__s(X)
      - Signature:
          {0/0,activate/1,diff/2,if/3,leq/2,p/1,s/1} / {false/0,n__0/0,n__s/1,true/0}
      - Obligation:
          innermost runtime complexity wrt. defined symbols {0,activate,diff,if,leq,p,s} and constructors {false,n__0
          ,n__s,true}
  + Applied Processor:
      EmptyProcessor
  + Details:
      The problem is still open.
MAYBE