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

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

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