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

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

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