WORST_CASE(?,O(n^1))
* Step 1: Sum.  WORST_CASE(?,O(n^1))
    + Considered Problem:
        - Strict TRS:
            f(0(),y,0(),u) -> true()
            f(0(),y,s(z),u) -> false()
            f(s(x),0(),z,u) -> f(x,u,minus(z,s(x)),u)
            f(s(x),s(y),z,u) -> if(le(x,y),f(s(x),minus(y,x),z,u),f(x,u,z,u))
            perfectp(0()) -> false()
            perfectp(s(x)) -> f(x,s(0()),s(x),s(x))
        - Signature:
            {f/4,perfectp/1} / {0/0,false/0,if/3,le/2,minus/2,s/1,true/0}
        - Obligation:
            innermost runtime complexity wrt. defined symbols {f,perfectp} and constructors {0,false,if,le,minus,s,true}
    + Applied Processor:
        Sum {left = someStrategy, right = someStrategy}
    + Details:
        ()
* Step 2: NaturalMI.  WORST_CASE(?,O(n^1))
    + Considered Problem:
        - Strict TRS:
            f(0(),y,0(),u) -> true()
            f(0(),y,s(z),u) -> false()
            f(s(x),0(),z,u) -> f(x,u,minus(z,s(x)),u)
            f(s(x),s(y),z,u) -> if(le(x,y),f(s(x),minus(y,x),z,u),f(x,u,z,u))
            perfectp(0()) -> false()
            perfectp(s(x)) -> f(x,s(0()),s(x),s(x))
        - Signature:
            {f/4,perfectp/1} / {0/0,false/0,if/3,le/2,minus/2,s/1,true/0}
        - Obligation:
            innermost runtime complexity wrt. defined symbols {f,perfectp} and constructors {0,false,if,le,minus,s,true}
    + Applied Processor:
        NaturalMI {miDimension = 1, miDegree = 1, miKind = Algebraic, uargs = UArgs, urules = URules, selector = Just any strict-rules}
    + Details:
        We apply a matrix interpretation of kind constructor based matrix interpretation:
        The following argument positions are considered usable:
          uargs(if) = {3}
        
        Following symbols are considered usable:
          {f,perfectp}
        TcT has computed the following interpretation:
                 p(0) = [0]         
                 p(f) = [9] x3 + [0]
             p(false) = [0]         
                p(if) = [1] x3 + [0]
                p(le) = [1] x1 + [0]
             p(minus) = [0]         
          p(perfectp) = [9] x1 + [0]
                 p(s) = [1] x1 + [1]
              p(true) = [0]         
        
        Following rules are strictly oriented:
        f(0(),y,s(z),u) = [9] z + [9]
                        > [0]        
                        = false()    
        
        
        Following rules are (at-least) weakly oriented:
          f(0(),y,0(),u) =  [0]                                          
                         >= [0]                                          
                         =  true()                                       
        
         f(s(x),0(),z,u) =  [9] z + [0]                                  
                         >= [0]                                          
                         =  f(x,u,minus(z,s(x)),u)                       
        
        f(s(x),s(y),z,u) =  [9] z + [0]                                  
                         >= [9] z + [0]                                  
                         =  if(le(x,y),f(s(x),minus(y,x),z,u),f(x,u,z,u))
        
           perfectp(0()) =  [0]                                          
                         >= [0]                                          
                         =  false()                                      
        
          perfectp(s(x)) =  [9] x + [9]                                  
                         >= [9] x + [9]                                  
                         =  f(x,s(0()),s(x),s(x))                        
        
* Step 3: NaturalMI.  WORST_CASE(?,O(n^1))
    + Considered Problem:
        - Strict TRS:
            f(0(),y,0(),u) -> true()
            f(s(x),0(),z,u) -> f(x,u,minus(z,s(x)),u)
            f(s(x),s(y),z,u) -> if(le(x,y),f(s(x),minus(y,x),z,u),f(x,u,z,u))
            perfectp(0()) -> false()
            perfectp(s(x)) -> f(x,s(0()),s(x),s(x))
        - Weak TRS:
            f(0(),y,s(z),u) -> false()
        - Signature:
            {f/4,perfectp/1} / {0/0,false/0,if/3,le/2,minus/2,s/1,true/0}
        - Obligation:
            innermost runtime complexity wrt. defined symbols {f,perfectp} and constructors {0,false,if,le,minus,s,true}
    + Applied Processor:
        NaturalMI {miDimension = 1, miDegree = 1, miKind = Algebraic, uargs = UArgs, urules = URules, selector = Just any strict-rules}
    + Details:
        We apply a matrix interpretation of kind constructor based matrix interpretation:
        The following argument positions are considered usable:
          uargs(if) = {3}
        
        Following symbols are considered usable:
          {f,perfectp}
        TcT has computed the following interpretation:
                 p(0) = [0]         
                 p(f) = [7]         
             p(false) = [0]         
                p(if) = [1] x3 + [0]
                p(le) = [1]         
             p(minus) = [2]         
          p(perfectp) = [8]         
                 p(s) = [1] x1 + [1]
              p(true) = [7]         
        
        Following rules are strictly oriented:
         perfectp(0()) = [8]                  
                       > [0]                  
                       = false()              
        
        perfectp(s(x)) = [8]                  
                       > [7]                  
                       = f(x,s(0()),s(x),s(x))
        
        
        Following rules are (at-least) weakly oriented:
          f(0(),y,0(),u) =  [7]                                          
                         >= [7]                                          
                         =  true()                                       
        
         f(0(),y,s(z),u) =  [7]                                          
                         >= [0]                                          
                         =  false()                                      
        
         f(s(x),0(),z,u) =  [7]                                          
                         >= [7]                                          
                         =  f(x,u,minus(z,s(x)),u)                       
        
        f(s(x),s(y),z,u) =  [7]                                          
                         >= [7]                                          
                         =  if(le(x,y),f(s(x),minus(y,x),z,u),f(x,u,z,u))
        
* Step 4: NaturalPI.  WORST_CASE(?,O(n^1))
    + Considered Problem:
        - Strict TRS:
            f(0(),y,0(),u) -> true()
            f(s(x),0(),z,u) -> f(x,u,minus(z,s(x)),u)
            f(s(x),s(y),z,u) -> if(le(x,y),f(s(x),minus(y,x),z,u),f(x,u,z,u))
        - Weak TRS:
            f(0(),y,s(z),u) -> false()
            perfectp(0()) -> false()
            perfectp(s(x)) -> f(x,s(0()),s(x),s(x))
        - Signature:
            {f/4,perfectp/1} / {0/0,false/0,if/3,le/2,minus/2,s/1,true/0}
        - Obligation:
            innermost runtime complexity wrt. defined symbols {f,perfectp} and constructors {0,false,if,le,minus,s,true}
    + Applied Processor:
        NaturalPI {shape = Linear, restrict = Restrict, uargs = UArgs, urules = URules, selector = Just any strict-rules}
    + Details:
        We apply a polynomial interpretation of kind constructor-based(linear):
        The following argument positions are considered usable:
          uargs(if) = {3}
        
        Following symbols are considered usable:
          {f,perfectp}
        TcT has computed the following interpretation:
                 p(0) = 0      
                 p(f) = 1      
             p(false) = 1      
                p(if) = x1 + x3
                p(le) = 0      
             p(minus) = 0      
          p(perfectp) = 1      
                 p(s) = 0      
              p(true) = 0      
        
        Following rules are strictly oriented:
        f(0(),y,0(),u) = 1     
                       > 0     
                       = true()
        
        
        Following rules are (at-least) weakly oriented:
         f(0(),y,s(z),u) =  1                                            
                         >= 1                                            
                         =  false()                                      
        
         f(s(x),0(),z,u) =  1                                            
                         >= 1                                            
                         =  f(x,u,minus(z,s(x)),u)                       
        
        f(s(x),s(y),z,u) =  1                                            
                         >= 1                                            
                         =  if(le(x,y),f(s(x),minus(y,x),z,u),f(x,u,z,u))
        
           perfectp(0()) =  1                                            
                         >= 1                                            
                         =  false()                                      
        
          perfectp(s(x)) =  1                                            
                         >= 1                                            
                         =  f(x,s(0()),s(x),s(x))                        
        
* Step 5: NaturalMI.  WORST_CASE(?,O(n^1))
    + Considered Problem:
        - Strict TRS:
            f(s(x),0(),z,u) -> f(x,u,minus(z,s(x)),u)
            f(s(x),s(y),z,u) -> if(le(x,y),f(s(x),minus(y,x),z,u),f(x,u,z,u))
        - Weak TRS:
            f(0(),y,0(),u) -> true()
            f(0(),y,s(z),u) -> false()
            perfectp(0()) -> false()
            perfectp(s(x)) -> f(x,s(0()),s(x),s(x))
        - Signature:
            {f/4,perfectp/1} / {0/0,false/0,if/3,le/2,minus/2,s/1,true/0}
        - Obligation:
            innermost runtime complexity wrt. defined symbols {f,perfectp} and constructors {0,false,if,le,minus,s,true}
    + Applied Processor:
        NaturalMI {miDimension = 1, miDegree = 1, miKind = Algebraic, uargs = UArgs, urules = URules, selector = Just any strict-rules}
    + Details:
        We apply a matrix interpretation of kind constructor based matrix interpretation:
        The following argument positions are considered usable:
          uargs(if) = {3}
        
        Following symbols are considered usable:
          {f,perfectp}
        TcT has computed the following interpretation:
                 p(0) = [0]                           
                 p(f) = [8] x1 + [2] x3 + [1] x4 + [0]
             p(false) = [2]                           
                p(if) = [1] x3 + [14]                 
                p(le) = [8]                           
             p(minus) = [8]                           
          p(perfectp) = [12] x1 + [2]                 
                 p(s) = [1] x1 + [2]                  
              p(true) = [0]                           
        
        Following rules are strictly oriented:
        f(s(x),s(y),z,u) = [1] u + [8] x + [2] z + [16]                 
                         > [1] u + [8] x + [2] z + [14]                 
                         = if(le(x,y),f(s(x),minus(y,x),z,u),f(x,u,z,u))
        
        
        Following rules are (at-least) weakly oriented:
         f(0(),y,0(),u) =  [1] u + [0]                 
                        >= [0]                         
                        =  true()                      
        
        f(0(),y,s(z),u) =  [1] u + [2] z + [4]         
                        >= [2]                         
                        =  false()                     
        
        f(s(x),0(),z,u) =  [1] u + [8] x + [2] z + [16]
                        >= [1] u + [8] x + [16]        
                        =  f(x,u,minus(z,s(x)),u)      
        
          perfectp(0()) =  [2]                         
                        >= [2]                         
                        =  false()                     
        
         perfectp(s(x)) =  [12] x + [26]               
                        >= [11] x + [6]                
                        =  f(x,s(0()),s(x),s(x))       
        
* Step 6: NaturalMI.  WORST_CASE(?,O(n^1))
    + Considered Problem:
        - Strict TRS:
            f(s(x),0(),z,u) -> f(x,u,minus(z,s(x)),u)
        - Weak TRS:
            f(0(),y,0(),u) -> true()
            f(0(),y,s(z),u) -> false()
            f(s(x),s(y),z,u) -> if(le(x,y),f(s(x),minus(y,x),z,u),f(x,u,z,u))
            perfectp(0()) -> false()
            perfectp(s(x)) -> f(x,s(0()),s(x),s(x))
        - Signature:
            {f/4,perfectp/1} / {0/0,false/0,if/3,le/2,minus/2,s/1,true/0}
        - Obligation:
            innermost runtime complexity wrt. defined symbols {f,perfectp} and constructors {0,false,if,le,minus,s,true}
    + Applied Processor:
        NaturalMI {miDimension = 1, miDegree = 1, miKind = Algebraic, uargs = UArgs, urules = URules, selector = Just any strict-rules}
    + Details:
        We apply a matrix interpretation of kind constructor based matrix interpretation:
        The following argument positions are considered usable:
          uargs(if) = {3}
        
        Following symbols are considered usable:
          {f,perfectp}
        TcT has computed the following interpretation:
                 p(0) = [3]                           
                 p(f) = [1] x1 + [1] x3 + [1] x4 + [8]
             p(false) = [2]                           
                p(if) = [1] x1 + [1] x3 + [8]         
                p(le) = [0]                           
             p(minus) = [0]                           
          p(perfectp) = [3] x1 + [3]                  
                 p(s) = [1] x1 + [8]                  
              p(true) = [1]                           
        
        Following rules are strictly oriented:
        f(s(x),0(),z,u) = [1] u + [1] x + [1] z + [16]
                        > [1] u + [1] x + [8]         
                        = f(x,u,minus(z,s(x)),u)      
        
        
        Following rules are (at-least) weakly oriented:
          f(0(),y,0(),u) =  [1] u + [14]                                 
                         >= [1]                                          
                         =  true()                                       
        
         f(0(),y,s(z),u) =  [1] u + [1] z + [19]                         
                         >= [2]                                          
                         =  false()                                      
        
        f(s(x),s(y),z,u) =  [1] u + [1] x + [1] z + [16]                 
                         >= [1] u + [1] x + [1] z + [16]                 
                         =  if(le(x,y),f(s(x),minus(y,x),z,u),f(x,u,z,u))
        
           perfectp(0()) =  [12]                                         
                         >= [2]                                          
                         =  false()                                      
        
          perfectp(s(x)) =  [3] x + [27]                                 
                         >= [3] x + [24]                                 
                         =  f(x,s(0()),s(x),s(x))                        
        
* Step 7: EmptyProcessor.  WORST_CASE(?,O(1))
    + Considered Problem:
        - Weak TRS:
            f(0(),y,0(),u) -> true()
            f(0(),y,s(z),u) -> false()
            f(s(x),0(),z,u) -> f(x,u,minus(z,s(x)),u)
            f(s(x),s(y),z,u) -> if(le(x,y),f(s(x),minus(y,x),z,u),f(x,u,z,u))
            perfectp(0()) -> false()
            perfectp(s(x)) -> f(x,s(0()),s(x),s(x))
        - Signature:
            {f/4,perfectp/1} / {0/0,false/0,if/3,le/2,minus/2,s/1,true/0}
        - Obligation:
            innermost runtime complexity wrt. defined symbols {f,perfectp} and constructors {0,false,if,le,minus,s,true}
    + Applied Processor:
        EmptyProcessor
    + Details:
        The problem is already closed. The intended complexity is O(1).

WORST_CASE(?,O(n^1))