WORST_CASE(Omega(n^1),O(n^1))
* Step 1: Sum WORST_CASE(Omega(n^1),O(n^1))
    + Considered Problem:
        - Strict TRS:
            compS_f#1(compS_f(x2),x1) -> compS_f#1(x2,S(x1))
            compS_f#1(id(),x3) -> S(x3)
            iter#3(0()) -> id()
            iter#3(S(x6)) -> compS_f(iter#3(x6))
            main(0()) -> 0()
            main(S(x9)) -> compS_f#1(iter#3(x9),0())
        - Signature:
            {compS_f#1/2,iter#3/1,main/1} / {0/0,S/1,compS_f/1,id/0}
        - Obligation:
            innermost runtime complexity wrt. defined symbols {compS_f#1,iter#3,main} and constructors {0,S,compS_f,id}
    + Applied Processor:
        Sum {left = someStrategy, right = someStrategy}
    + Details:
        ()
** Step 1.a:1: DecreasingLoops WORST_CASE(Omega(n^1),?)
    + Considered Problem:
        - Strict TRS:
            compS_f#1(compS_f(x2),x1) -> compS_f#1(x2,S(x1))
            compS_f#1(id(),x3) -> S(x3)
            iter#3(0()) -> id()
            iter#3(S(x6)) -> compS_f(iter#3(x6))
            main(0()) -> 0()
            main(S(x9)) -> compS_f#1(iter#3(x9),0())
        - Signature:
            {compS_f#1/2,iter#3/1,main/1} / {0/0,S/1,compS_f/1,id/0}
        - Obligation:
            innermost runtime complexity wrt. defined symbols {compS_f#1,iter#3,main} and constructors {0,S,compS_f,id}
    + Applied Processor:
        DecreasingLoops {bound = AnyLoop, narrow = 10}
    + Details:
        The system has following decreasing Loops:
          compS_f#1(x,y){x -> compS_f(x)} =
            compS_f#1(compS_f(x),y) ->^+ compS_f#1(x,S(y))
              = C[compS_f#1(x,S(y)) = compS_f#1(x,y){y -> S(y)}]

** Step 1.b:1: NaturalPI WORST_CASE(?,O(n^1))
    + Considered Problem:
        - Strict TRS:
            compS_f#1(compS_f(x2),x1) -> compS_f#1(x2,S(x1))
            compS_f#1(id(),x3) -> S(x3)
            iter#3(0()) -> id()
            iter#3(S(x6)) -> compS_f(iter#3(x6))
            main(0()) -> 0()
            main(S(x9)) -> compS_f#1(iter#3(x9),0())
        - Signature:
            {compS_f#1/2,iter#3/1,main/1} / {0/0,S/1,compS_f/1,id/0}
        - Obligation:
            innermost runtime complexity wrt. defined symbols {compS_f#1,iter#3,main} and constructors {0,S,compS_f,id}
    + 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(compS_f) = {1},
          uargs(compS_f#1) = {1}
        
        Following symbols are considered usable:
          {compS_f#1,iter#3,main}
        TcT has computed the following interpretation:
                  p(0) = 2          
                  p(S) = 1 + x1     
            p(compS_f) = 1 + x1     
          p(compS_f#1) = 4 + x1 + x2
                 p(id) = 11         
             p(iter#3) = 5 + 4*x1   
               p(main) = 12 + 4*x1  
        
        Following rules are strictly oriented:
        compS_f#1(id(),x3) = 15 + x3                  
                           > 1 + x3                   
                           = S(x3)                    
        
               iter#3(0()) = 13                       
                           > 11                       
                           = id()                     
        
             iter#3(S(x6)) = 9 + 4*x6                 
                           > 6 + 4*x6                 
                           = compS_f(iter#3(x6))      
        
                 main(0()) = 20                       
                           > 2                        
                           = 0()                      
        
               main(S(x9)) = 16 + 4*x9                
                           > 11 + 4*x9                
                           = compS_f#1(iter#3(x9),0())
        
        
        Following rules are (at-least) weakly oriented:
        compS_f#1(compS_f(x2),x1) =  5 + x1 + x2        
                                  >= 5 + x1 + x2        
                                  =  compS_f#1(x2,S(x1))
        
** Step 1.b:2: NaturalPI WORST_CASE(?,O(n^1))
    + Considered Problem:
        - Strict TRS:
            compS_f#1(compS_f(x2),x1) -> compS_f#1(x2,S(x1))
        - Weak TRS:
            compS_f#1(id(),x3) -> S(x3)
            iter#3(0()) -> id()
            iter#3(S(x6)) -> compS_f(iter#3(x6))
            main(0()) -> 0()
            main(S(x9)) -> compS_f#1(iter#3(x9),0())
        - Signature:
            {compS_f#1/2,iter#3/1,main/1} / {0/0,S/1,compS_f/1,id/0}
        - Obligation:
            innermost runtime complexity wrt. defined symbols {compS_f#1,iter#3,main} and constructors {0,S,compS_f,id}
    + 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(compS_f) = {1},
          uargs(compS_f#1) = {1}
        
        Following symbols are considered usable:
          {compS_f#1,iter#3,main}
        TcT has computed the following interpretation:
                  p(0) = 1         
                  p(S) = 1 + x1    
            p(compS_f) = 1 + x1    
          p(compS_f#1) = 3*x1 + x2 
                 p(id) = 3         
             p(iter#3) = 9 + x1    
               p(main) = 15 + 13*x1
        
        Following rules are strictly oriented:
        compS_f#1(compS_f(x2),x1) = 3 + x1 + 3*x2      
                                  > 1 + x1 + 3*x2      
                                  = compS_f#1(x2,S(x1))
        
        
        Following rules are (at-least) weakly oriented:
        compS_f#1(id(),x3) =  9 + x3                   
                           >= 1 + x3                   
                           =  S(x3)                    
        
               iter#3(0()) =  10                       
                           >= 3                        
                           =  id()                     
        
             iter#3(S(x6)) =  10 + x6                  
                           >= 10 + x6                  
                           =  compS_f(iter#3(x6))      
        
                 main(0()) =  28                       
                           >= 1                        
                           =  0()                      
        
               main(S(x9)) =  28 + 13*x9               
                           >= 28 + 3*x9                
                           =  compS_f#1(iter#3(x9),0())
        
** Step 1.b:3: EmptyProcessor WORST_CASE(?,O(1))
    + Considered Problem:
        - Weak TRS:
            compS_f#1(compS_f(x2),x1) -> compS_f#1(x2,S(x1))
            compS_f#1(id(),x3) -> S(x3)
            iter#3(0()) -> id()
            iter#3(S(x6)) -> compS_f(iter#3(x6))
            main(0()) -> 0()
            main(S(x9)) -> compS_f#1(iter#3(x9),0())
        - Signature:
            {compS_f#1/2,iter#3/1,main/1} / {0/0,S/1,compS_f/1,id/0}
        - Obligation:
            innermost runtime complexity wrt. defined symbols {compS_f#1,iter#3,main} and constructors {0,S,compS_f,id}
    + Applied Processor:
        EmptyProcessor
    + Details:
        The problem is already closed. The intended complexity is O(1).

WORST_CASE(Omega(n^1),O(n^1))