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: NaturalPI 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:
        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) = 4 
             p(false) = 4 
                p(if) = x3
                p(le) = 0 
             p(minus) = 0 
          p(perfectp) = 4 
                 p(s) = 10
              p(true) = 0 
        
        Following rules are strictly oriented:
        f(0(),y,0(),u) = 4     
                       > 0     
                       = true()
        
        
        Following rules are (at-least) weakly oriented:
         f(0(),y,s(z),u) =  4                                            
                         >= 4                                            
                         =  false()                                      
        
         f(s(x),0(),z,u) =  4                                            
                         >= 4                                            
                         =  f(x,u,minus(z,s(x)),u)                       
        
        f(s(x),s(y),z,u) =  4                                            
                         >= 4                                            
                         =  if(le(x,y),f(s(x),minus(y,x),z,u),f(x,u,z,u))
        
           perfectp(0()) =  4                                            
                         >= 4                                            
                         =  false()                                      
        
          perfectp(s(x)) =  4                                            
                         >= 4                                            
                         =  f(x,s(0()),s(x),s(x))                        
        
* Step 3: NaturalPI WORST_CASE(?,O(n^1))
    + Considered Problem:
        - Strict TRS:
            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))
        - Weak TRS:
            f(0(),y,0(),u) -> true()
        - 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) = 8 + x4  
             p(false) = 0       
                p(if) = x3      
                p(le) = 2       
             p(minus) = x1      
          p(perfectp) = 3 + 2*x1
                 p(s) = 8       
              p(true) = 5       
        
        Following rules are strictly oriented:
        f(0(),y,s(z),u) = 8 + u                
                        > 0                    
                        = false()              
        
          perfectp(0()) = 3                    
                        > 0                    
                        = false()              
        
         perfectp(s(x)) = 19                   
                        > 16                   
                        = f(x,s(0()),s(x),s(x))
        
        
        Following rules are (at-least) weakly oriented:
          f(0(),y,0(),u) =  8 + u                                        
                         >= 5                                            
                         =  true()                                       
        
         f(s(x),0(),z,u) =  8 + u                                        
                         >= 8 + u                                        
                         =  f(x,u,minus(z,s(x)),u)                       
        
        f(s(x),s(y),z,u) =  8 + u                                        
                         >= 8 + u                                        
                         =  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(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:
        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 + 2*x1 + 2*x4
             p(false) = 0              
                p(if) = 4 + x1 + x3    
                p(le) = 1              
             p(minus) = x1 + x2        
          p(perfectp) = 4*x1           
                 p(s) = 4 + x1         
              p(true) = 1              
        
        Following rules are strictly oriented:
         f(s(x),0(),z,u) = 9 + 2*u + 2*x                                
                         > 1 + 2*u + 2*x                                
                         = f(x,u,minus(z,s(x)),u)                       
        
        f(s(x),s(y),z,u) = 9 + 2*u + 2*x                                
                         > 6 + 2*u + 2*x                                
                         = 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 + 2*u              
                        >= 1                    
                        =  true()               
        
        f(0(),y,s(z),u) =  1 + 2*u              
                        >= 0                    
                        =  false()              
        
          perfectp(0()) =  0                    
                        >= 0                    
                        =  false()              
        
         perfectp(s(x)) =  16 + 4*x             
                        >= 9 + 4*x              
                        =  f(x,s(0()),s(x),s(x))
        
* Step 5: 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))