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

** Step 1.b:1: NaturalPI WORST_CASE(?,O(n^1))
    + Considered Problem:
        - Strict TRS:
            div2(0()) -> 0()
            div2(S(0())) -> 0()
            div2(S(S(x))) -> +(S(0()),div2(x))
        - Weak TRS:
            +(x,S(0())) -> S(x)
            +(S(0()),y) -> S(y)
        - Signature:
            {+/2,div2/1} / {0/0,S/1}
        - Obligation:
            innermost runtime complexity wrt. defined symbols {+,div2} and constructors {0,S}
    + 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(+) = {2}
        
        Following symbols are considered usable:
          {+,div2}
        TcT has computed the following interpretation:
             p(+) = x1 + x2
             p(0) = 0      
             p(S) = x1     
          p(div2) = 8      
        
        Following rules are strictly oriented:
           div2(0()) = 8  
                     > 0  
                     = 0()
        
        div2(S(0())) = 8  
                     > 0  
                     = 0()
        
        
        Following rules are (at-least) weakly oriented:
          +(x,S(0())) =  x                
                      >= x                
                      =  S(x)             
        
          +(S(0()),y) =  y                
                      >= y                
                      =  S(y)             
        
        div2(S(S(x))) =  8                
                      >= 8                
                      =  +(S(0()),div2(x))
        
** Step 1.b:2: NaturalPI WORST_CASE(?,O(n^1))
    + Considered Problem:
        - Strict TRS:
            div2(S(S(x))) -> +(S(0()),div2(x))
        - Weak TRS:
            +(x,S(0())) -> S(x)
            +(S(0()),y) -> S(y)
            div2(0()) -> 0()
            div2(S(0())) -> 0()
        - Signature:
            {+/2,div2/1} / {0/0,S/1}
        - Obligation:
            innermost runtime complexity wrt. defined symbols {+,div2} and constructors {0,S}
    + 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(+) = {2}
        
        Following symbols are considered usable:
          {+,div2}
        TcT has computed the following interpretation:
             p(+) = 4 + 2*x1 + x2
             p(0) = 1            
             p(S) = 1 + x1       
          p(div2) = 8*x1         
        
        Following rules are strictly oriented:
        div2(S(S(x))) = 16 + 8*x         
                      > 8 + 8*x          
                      = +(S(0()),div2(x))
        
        
        Following rules are (at-least) weakly oriented:
         +(x,S(0())) =  6 + 2*x
                     >= 1 + x  
                     =  S(x)   
        
         +(S(0()),y) =  8 + y  
                     >= 1 + y  
                     =  S(y)   
        
           div2(0()) =  8      
                     >= 1      
                     =  0()    
        
        div2(S(0())) =  16     
                     >= 1      
                     =  0()    
        
** Step 1.b:3: EmptyProcessor WORST_CASE(?,O(1))
    + Considered Problem:
        - Weak TRS:
            +(x,S(0())) -> S(x)
            +(S(0()),y) -> S(y)
            div2(0()) -> 0()
            div2(S(0())) -> 0()
            div2(S(S(x))) -> +(S(0()),div2(x))
        - Signature:
            {+/2,div2/1} / {0/0,S/1}
        - Obligation:
            innermost runtime complexity wrt. defined symbols {+,div2} and constructors {0,S}
    + Applied Processor:
        EmptyProcessor
    + Details:
        The problem is already closed. The intended complexity is O(1).

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