* Step 1: Sum WORST_CASE(Omega(n^1),O(n^2))
    + Considered Problem:
        - Strict TRS:
            Concat(Concat(s,t),u) -> Concat(s,Concat(t,u))
            Concat(Cons_sum(xi,k,s),t) -> Cons_sum(xi,k,Concat(s,t))
            Concat(Cons_usual(x,m,s),t) -> Cons_usual(x,Term_sub(m,t),Concat(s,t))
            Concat(Id(),s) -> s
            Frozen(m,Sum_constant(Left()),n,s) -> Term_sub(m,s)
            Frozen(m,Sum_constant(Right()),n,s) -> Term_sub(n,s)
            Frozen(m,Sum_term_var(xi),n,s) -> Case(Term_sub(m,s),xi,Term_sub(n,s))
            Sum_sub(xi,Cons_sum(psi,k,s)) -> Sum_constant(k)
            Sum_sub(xi,Cons_sum(psi,k,s)) -> Sum_sub(xi,s)
            Sum_sub(xi,Cons_usual(y,m,s)) -> Sum_sub(xi,s)
            Sum_sub(xi,Id()) -> Sum_term_var(xi)
            Term_sub(Case(m,xi,n),s) -> Frozen(m,Sum_sub(xi,s),n,s)
            Term_sub(Term_app(m,n),s) -> Term_app(Term_sub(m,s),Term_sub(n,s))
            Term_sub(Term_inl(m),s) -> Term_inl(Term_sub(m,s))
            Term_sub(Term_inr(m),s) -> Term_inr(Term_sub(m,s))
            Term_sub(Term_pair(m,n),s) -> Term_pair(Term_sub(m,s),Term_sub(n,s))
            Term_sub(Term_sub(m,s),t) -> Term_sub(m,Concat(s,t))
            Term_sub(Term_var(x),Cons_sum(xi,k,s)) -> Term_sub(Term_var(x),s)
            Term_sub(Term_var(x),Cons_usual(y,m,s)) -> m
            Term_sub(Term_var(x),Cons_usual(y,m,s)) -> Term_sub(Term_var(x),s)
            Term_sub(Term_var(x),Id()) -> Term_var(x)
        - Signature:
            {Concat/2,Frozen/4,Sum_sub/2,Term_sub/2} / {Case/3,Cons_sum/3,Cons_usual/3,Id/0,Left/0,Right/0
            ,Sum_constant/1,Sum_term_var/1,Term_app/2,Term_inl/1,Term_inr/1,Term_pair/2,Term_var/1}
        - Obligation:
            innermost runtime complexity wrt. defined symbols {Concat,Frozen,Sum_sub,Term_sub} and constructors {Case
            ,Cons_sum,Cons_usual,Id,Left,Right,Sum_constant,Sum_term_var,Term_app,Term_inl,Term_inr,Term_pair,Term_var}
    + Applied Processor:
        Sum {left = someStrategy, right = someStrategy}
    + Details:
        ()
** Step 1.a:1: DecreasingLoops WORST_CASE(Omega(n^1),?)
    + Considered Problem:
        - Strict TRS:
            Concat(Concat(s,t),u) -> Concat(s,Concat(t,u))
            Concat(Cons_sum(xi,k,s),t) -> Cons_sum(xi,k,Concat(s,t))
            Concat(Cons_usual(x,m,s),t) -> Cons_usual(x,Term_sub(m,t),Concat(s,t))
            Concat(Id(),s) -> s
            Frozen(m,Sum_constant(Left()),n,s) -> Term_sub(m,s)
            Frozen(m,Sum_constant(Right()),n,s) -> Term_sub(n,s)
            Frozen(m,Sum_term_var(xi),n,s) -> Case(Term_sub(m,s),xi,Term_sub(n,s))
            Sum_sub(xi,Cons_sum(psi,k,s)) -> Sum_constant(k)
            Sum_sub(xi,Cons_sum(psi,k,s)) -> Sum_sub(xi,s)
            Sum_sub(xi,Cons_usual(y,m,s)) -> Sum_sub(xi,s)
            Sum_sub(xi,Id()) -> Sum_term_var(xi)
            Term_sub(Case(m,xi,n),s) -> Frozen(m,Sum_sub(xi,s),n,s)
            Term_sub(Term_app(m,n),s) -> Term_app(Term_sub(m,s),Term_sub(n,s))
            Term_sub(Term_inl(m),s) -> Term_inl(Term_sub(m,s))
            Term_sub(Term_inr(m),s) -> Term_inr(Term_sub(m,s))
            Term_sub(Term_pair(m,n),s) -> Term_pair(Term_sub(m,s),Term_sub(n,s))
            Term_sub(Term_sub(m,s),t) -> Term_sub(m,Concat(s,t))
            Term_sub(Term_var(x),Cons_sum(xi,k,s)) -> Term_sub(Term_var(x),s)
            Term_sub(Term_var(x),Cons_usual(y,m,s)) -> m
            Term_sub(Term_var(x),Cons_usual(y,m,s)) -> Term_sub(Term_var(x),s)
            Term_sub(Term_var(x),Id()) -> Term_var(x)
        - Signature:
            {Concat/2,Frozen/4,Sum_sub/2,Term_sub/2} / {Case/3,Cons_sum/3,Cons_usual/3,Id/0,Left/0,Right/0
            ,Sum_constant/1,Sum_term_var/1,Term_app/2,Term_inl/1,Term_inr/1,Term_pair/2,Term_var/1}
        - Obligation:
            innermost runtime complexity wrt. defined symbols {Concat,Frozen,Sum_sub,Term_sub} and constructors {Case
            ,Cons_sum,Cons_usual,Id,Left,Right,Sum_constant,Sum_term_var,Term_app,Term_inl,Term_inr,Term_pair,Term_var}
    + Applied Processor:
        DecreasingLoops {bound = AnyLoop, narrow = 10}
    + Details:
        The system has following decreasing Loops:
          Concat(z,u){z -> Cons_sum(x,y,z)} =
            Concat(Cons_sum(x,y,z),u) ->^+ Cons_sum(x,y,Concat(z,u))
              = C[Concat(z,u) = Concat(z,u){}]

** Step 1.b:1: NaturalPI WORST_CASE(?,O(n^2))
    + Considered Problem:
        - Strict TRS:
            Concat(Concat(s,t),u) -> Concat(s,Concat(t,u))
            Concat(Cons_sum(xi,k,s),t) -> Cons_sum(xi,k,Concat(s,t))
            Concat(Cons_usual(x,m,s),t) -> Cons_usual(x,Term_sub(m,t),Concat(s,t))
            Concat(Id(),s) -> s
            Frozen(m,Sum_constant(Left()),n,s) -> Term_sub(m,s)
            Frozen(m,Sum_constant(Right()),n,s) -> Term_sub(n,s)
            Frozen(m,Sum_term_var(xi),n,s) -> Case(Term_sub(m,s),xi,Term_sub(n,s))
            Sum_sub(xi,Cons_sum(psi,k,s)) -> Sum_constant(k)
            Sum_sub(xi,Cons_sum(psi,k,s)) -> Sum_sub(xi,s)
            Sum_sub(xi,Cons_usual(y,m,s)) -> Sum_sub(xi,s)
            Sum_sub(xi,Id()) -> Sum_term_var(xi)
            Term_sub(Case(m,xi,n),s) -> Frozen(m,Sum_sub(xi,s),n,s)
            Term_sub(Term_app(m,n),s) -> Term_app(Term_sub(m,s),Term_sub(n,s))
            Term_sub(Term_inl(m),s) -> Term_inl(Term_sub(m,s))
            Term_sub(Term_inr(m),s) -> Term_inr(Term_sub(m,s))
            Term_sub(Term_pair(m,n),s) -> Term_pair(Term_sub(m,s),Term_sub(n,s))
            Term_sub(Term_sub(m,s),t) -> Term_sub(m,Concat(s,t))
            Term_sub(Term_var(x),Cons_sum(xi,k,s)) -> Term_sub(Term_var(x),s)
            Term_sub(Term_var(x),Cons_usual(y,m,s)) -> m
            Term_sub(Term_var(x),Cons_usual(y,m,s)) -> Term_sub(Term_var(x),s)
            Term_sub(Term_var(x),Id()) -> Term_var(x)
        - Signature:
            {Concat/2,Frozen/4,Sum_sub/2,Term_sub/2} / {Case/3,Cons_sum/3,Cons_usual/3,Id/0,Left/0,Right/0
            ,Sum_constant/1,Sum_term_var/1,Term_app/2,Term_inl/1,Term_inr/1,Term_pair/2,Term_var/1}
        - Obligation:
            innermost runtime complexity wrt. defined symbols {Concat,Frozen,Sum_sub,Term_sub} and constructors {Case
            ,Cons_sum,Cons_usual,Id,Left,Right,Sum_constant,Sum_term_var,Term_app,Term_inl,Term_inr,Term_pair,Term_var}
    + Applied Processor:
        NaturalPI {shape = Mixed 2, restrict = Restrict, uargs = UArgs, urules = URules, selector = Just any strict-rules}
    + Details:
        We apply a polynomial interpretation of kind constructor-based(mixed(2)):
        The following argument positions are considered usable:
          uargs(Case) = {1,3},
          uargs(Concat) = {2},
          uargs(Cons_sum) = {3},
          uargs(Cons_usual) = {2,3},
          uargs(Frozen) = {2},
          uargs(Term_app) = {1,2},
          uargs(Term_inl) = {1},
          uargs(Term_inr) = {1},
          uargs(Term_pair) = {1,2},
          uargs(Term_sub) = {2}
        
        Following symbols are considered usable:
          {Concat,Frozen,Sum_sub,Term_sub}
        TcT has computed the following interpretation:
                  p(Case) = 1 + x1 + x3                                    
                p(Concat) = x1 + x1*x2 + x2                                
              p(Cons_sum) = x2 + x3                                        
            p(Cons_usual) = 1 + x2 + x3                                    
                p(Frozen) = 1 + x1 + x1*x2 + x1*x4 + x2 + x3 + x3*x4 + 2*x4
                    p(Id) = 1                                              
                  p(Left) = 0                                              
                 p(Right) = 0                                              
          p(Sum_constant) = 0                                              
               p(Sum_sub) = 0                                              
          p(Sum_term_var) = 0                                              
              p(Term_app) = 1 + x1 + x2                                    
              p(Term_inl) = 1 + x1                                         
              p(Term_inr) = x1                                             
             p(Term_pair) = 1 + x1 + x2                                    
              p(Term_sub) = x1 + x1*x2 + x2                                
              p(Term_var) = 0                                              
        
        Following rules are strictly oriented:
                                 Concat(Id(),s) = 1 + 2*s                    
                                                > s                          
                                                = s                          
        
             Frozen(m,Sum_constant(Left()),n,s) = 1 + m + m*s + n + n*s + 2*s
                                                > m + m*s + s                
                                                = Term_sub(m,s)              
        
            Frozen(m,Sum_constant(Right()),n,s) = 1 + m + m*s + n + n*s + 2*s
                                                > n + n*s + s                
                                                = Term_sub(n,s)              
        
        Term_sub(Term_var(x),Cons_usual(y,m,s)) = 1 + m + s                  
                                                > m                          
                                                = m                          
        
        Term_sub(Term_var(x),Cons_usual(y,m,s)) = 1 + m + s                  
                                                > s                          
                                                = Term_sub(Term_var(x),s)    
        
                     Term_sub(Term_var(x),Id()) = 1                          
                                                > 0                          
                                                = Term_var(x)                
        
        
        Following rules are (at-least) weakly oriented:
                         Concat(Concat(s,t),u) =  s + s*t + s*t*u + s*u + t + t*u + u    
                                               >= s + s*t + s*t*u + s*u + t + t*u + u    
                                               =  Concat(s,Concat(t,u))                  
        
                    Concat(Cons_sum(xi,k,s),t) =  k + k*t + s + s*t + t                  
                                               >= k + s + s*t + t                        
                                               =  Cons_sum(xi,k,Concat(s,t))             
        
                   Concat(Cons_usual(x,m,s),t) =  1 + m + m*t + s + s*t + 2*t            
                                               >= 1 + m + m*t + s + s*t + 2*t            
                                               =  Cons_usual(x,Term_sub(m,t),Concat(s,t))
        
                Frozen(m,Sum_term_var(xi),n,s) =  1 + m + m*s + n + n*s + 2*s            
                                               >= 1 + m + m*s + n + n*s + 2*s            
                                               =  Case(Term_sub(m,s),xi,Term_sub(n,s))   
        
                 Sum_sub(xi,Cons_sum(psi,k,s)) =  0                                      
                                               >= 0                                      
                                               =  Sum_constant(k)                        
        
                 Sum_sub(xi,Cons_sum(psi,k,s)) =  0                                      
                                               >= 0                                      
                                               =  Sum_sub(xi,s)                          
        
                 Sum_sub(xi,Cons_usual(y,m,s)) =  0                                      
                                               >= 0                                      
                                               =  Sum_sub(xi,s)                          
        
                              Sum_sub(xi,Id()) =  0                                      
                                               >= 0                                      
                                               =  Sum_term_var(xi)                       
        
                      Term_sub(Case(m,xi,n),s) =  1 + m + m*s + n + n*s + 2*s            
                                               >= 1 + m + m*s + n + n*s + 2*s            
                                               =  Frozen(m,Sum_sub(xi,s),n,s)            
        
                     Term_sub(Term_app(m,n),s) =  1 + m + m*s + n + n*s + 2*s            
                                               >= 1 + m + m*s + n + n*s + 2*s            
                                               =  Term_app(Term_sub(m,s),Term_sub(n,s))  
        
                       Term_sub(Term_inl(m),s) =  1 + m + m*s + 2*s                      
                                               >= 1 + m + m*s + s                        
                                               =  Term_inl(Term_sub(m,s))                
        
                       Term_sub(Term_inr(m),s) =  m + m*s + s                            
                                               >= m + m*s + s                            
                                               =  Term_inr(Term_sub(m,s))                
        
                    Term_sub(Term_pair(m,n),s) =  1 + m + m*s + n + n*s + 2*s            
                                               >= 1 + m + m*s + n + n*s + 2*s            
                                               =  Term_pair(Term_sub(m,s),Term_sub(n,s)) 
        
                     Term_sub(Term_sub(m,s),t) =  m + m*s + m*s*t + m*t + s + s*t + t    
                                               >= m + m*s + m*s*t + m*t + s + s*t + t    
                                               =  Term_sub(m,Concat(s,t))                
        
        Term_sub(Term_var(x),Cons_sum(xi,k,s)) =  k + s                                  
                                               >= s                                      
                                               =  Term_sub(Term_var(x),s)                
        
** Step 1.b:2: NaturalPI WORST_CASE(?,O(n^2))
    + Considered Problem:
        - Strict TRS:
            Concat(Concat(s,t),u) -> Concat(s,Concat(t,u))
            Concat(Cons_sum(xi,k,s),t) -> Cons_sum(xi,k,Concat(s,t))
            Concat(Cons_usual(x,m,s),t) -> Cons_usual(x,Term_sub(m,t),Concat(s,t))
            Frozen(m,Sum_term_var(xi),n,s) -> Case(Term_sub(m,s),xi,Term_sub(n,s))
            Sum_sub(xi,Cons_sum(psi,k,s)) -> Sum_constant(k)
            Sum_sub(xi,Cons_sum(psi,k,s)) -> Sum_sub(xi,s)
            Sum_sub(xi,Cons_usual(y,m,s)) -> Sum_sub(xi,s)
            Sum_sub(xi,Id()) -> Sum_term_var(xi)
            Term_sub(Case(m,xi,n),s) -> Frozen(m,Sum_sub(xi,s),n,s)
            Term_sub(Term_app(m,n),s) -> Term_app(Term_sub(m,s),Term_sub(n,s))
            Term_sub(Term_inl(m),s) -> Term_inl(Term_sub(m,s))
            Term_sub(Term_inr(m),s) -> Term_inr(Term_sub(m,s))
            Term_sub(Term_pair(m,n),s) -> Term_pair(Term_sub(m,s),Term_sub(n,s))
            Term_sub(Term_sub(m,s),t) -> Term_sub(m,Concat(s,t))
            Term_sub(Term_var(x),Cons_sum(xi,k,s)) -> Term_sub(Term_var(x),s)
        - Weak TRS:
            Concat(Id(),s) -> s
            Frozen(m,Sum_constant(Left()),n,s) -> Term_sub(m,s)
            Frozen(m,Sum_constant(Right()),n,s) -> Term_sub(n,s)
            Term_sub(Term_var(x),Cons_usual(y,m,s)) -> m
            Term_sub(Term_var(x),Cons_usual(y,m,s)) -> Term_sub(Term_var(x),s)
            Term_sub(Term_var(x),Id()) -> Term_var(x)
        - Signature:
            {Concat/2,Frozen/4,Sum_sub/2,Term_sub/2} / {Case/3,Cons_sum/3,Cons_usual/3,Id/0,Left/0,Right/0
            ,Sum_constant/1,Sum_term_var/1,Term_app/2,Term_inl/1,Term_inr/1,Term_pair/2,Term_var/1}
        - Obligation:
            innermost runtime complexity wrt. defined symbols {Concat,Frozen,Sum_sub,Term_sub} and constructors {Case
            ,Cons_sum,Cons_usual,Id,Left,Right,Sum_constant,Sum_term_var,Term_app,Term_inl,Term_inr,Term_pair,Term_var}
    + Applied Processor:
        NaturalPI {shape = Mixed 2, restrict = Restrict, uargs = UArgs, urules = URules, selector = Just any strict-rules}
    + Details:
        We apply a polynomial interpretation of kind constructor-based(mixed(2)):
        The following argument positions are considered usable:
          uargs(Case) = {1,3},
          uargs(Concat) = {2},
          uargs(Cons_sum) = {3},
          uargs(Cons_usual) = {2,3},
          uargs(Frozen) = {2},
          uargs(Term_app) = {1,2},
          uargs(Term_inl) = {1},
          uargs(Term_inr) = {1},
          uargs(Term_pair) = {1,2},
          uargs(Term_sub) = {2}
        
        Following symbols are considered usable:
          {Concat,Frozen,Sum_sub,Term_sub}
        TcT has computed the following interpretation:
                  p(Case) = 1 + x1 + x3                                
                p(Concat) = x1 + 2*x1*x2 + x2                          
              p(Cons_sum) = 1 + x2 + x3                                
            p(Cons_usual) = 1 + x1 + x2 + x3                           
                p(Frozen) = 1 + x1 + 2*x1*x4 + x2 + x3 + 2*x3*x4 + 2*x4
                    p(Id) = 0                                          
                  p(Left) = 0                                          
                 p(Right) = 0                                          
          p(Sum_constant) = 0                                          
               p(Sum_sub) = 0                                          
          p(Sum_term_var) = 0                                          
              p(Term_app) = 1 + x1 + x2                                
              p(Term_inl) = x1                                         
              p(Term_inr) = x1                                         
             p(Term_pair) = 1 + x1 + x2                                
              p(Term_sub) = x1 + 2*x1*x2 + x2                          
              p(Term_var) = x1                                         
        
        Following rules are strictly oriented:
        Term_sub(Term_var(x),Cons_sum(xi,k,s)) = 1 + k + 2*k*x + s + 2*s*x + 3*x
                                               > s + 2*s*x + x                  
                                               = Term_sub(Term_var(x),s)        
        
        
        Following rules are (at-least) weakly oriented:
                          Concat(Concat(s,t),u) =  s + 2*s*t + 4*s*t*u + 2*s*u + t + 2*t*u + u
                                                >= s + 2*s*t + 4*s*t*u + 2*s*u + t + 2*t*u + u
                                                =  Concat(s,Concat(t,u))                      
        
                     Concat(Cons_sum(xi,k,s),t) =  1 + k + 2*k*t + s + 2*s*t + 3*t            
                                                >= 1 + k + s + 2*s*t + t                      
                                                =  Cons_sum(xi,k,Concat(s,t))                 
        
                    Concat(Cons_usual(x,m,s),t) =  1 + m + 2*m*t + s + 2*s*t + 3*t + 2*t*x + x
                                                >= 1 + m + 2*m*t + s + 2*s*t + 2*t + x        
                                                =  Cons_usual(x,Term_sub(m,t),Concat(s,t))    
        
                                 Concat(Id(),s) =  s                                          
                                                >= s                                          
                                                =  s                                          
        
             Frozen(m,Sum_constant(Left()),n,s) =  1 + m + 2*m*s + n + 2*n*s + 2*s            
                                                >= m + 2*m*s + s                              
                                                =  Term_sub(m,s)                              
        
            Frozen(m,Sum_constant(Right()),n,s) =  1 + m + 2*m*s + n + 2*n*s + 2*s            
                                                >= n + 2*n*s + s                              
                                                =  Term_sub(n,s)                              
        
                 Frozen(m,Sum_term_var(xi),n,s) =  1 + m + 2*m*s + n + 2*n*s + 2*s            
                                                >= 1 + m + 2*m*s + n + 2*n*s + 2*s            
                                                =  Case(Term_sub(m,s),xi,Term_sub(n,s))       
        
                  Sum_sub(xi,Cons_sum(psi,k,s)) =  0                                          
                                                >= 0                                          
                                                =  Sum_constant(k)                            
        
                  Sum_sub(xi,Cons_sum(psi,k,s)) =  0                                          
                                                >= 0                                          
                                                =  Sum_sub(xi,s)                              
        
                  Sum_sub(xi,Cons_usual(y,m,s)) =  0                                          
                                                >= 0                                          
                                                =  Sum_sub(xi,s)                              
        
                               Sum_sub(xi,Id()) =  0                                          
                                                >= 0                                          
                                                =  Sum_term_var(xi)                           
        
                       Term_sub(Case(m,xi,n),s) =  1 + m + 2*m*s + n + 2*n*s + 3*s            
                                                >= 1 + m + 2*m*s + n + 2*n*s + 2*s            
                                                =  Frozen(m,Sum_sub(xi,s),n,s)                
        
                      Term_sub(Term_app(m,n),s) =  1 + m + 2*m*s + n + 2*n*s + 3*s            
                                                >= 1 + m + 2*m*s + n + 2*n*s + 2*s            
                                                =  Term_app(Term_sub(m,s),Term_sub(n,s))      
        
                        Term_sub(Term_inl(m),s) =  m + 2*m*s + s                              
                                                >= m + 2*m*s + s                              
                                                =  Term_inl(Term_sub(m,s))                    
        
                        Term_sub(Term_inr(m),s) =  m + 2*m*s + s                              
                                                >= m + 2*m*s + s                              
                                                =  Term_inr(Term_sub(m,s))                    
        
                     Term_sub(Term_pair(m,n),s) =  1 + m + 2*m*s + n + 2*n*s + 3*s            
                                                >= 1 + m + 2*m*s + n + 2*n*s + 2*s            
                                                =  Term_pair(Term_sub(m,s),Term_sub(n,s))     
        
                      Term_sub(Term_sub(m,s),t) =  m + 2*m*s + 4*m*s*t + 2*m*t + s + 2*s*t + t
                                                >= m + 2*m*s + 4*m*s*t + 2*m*t + s + 2*s*t + t
                                                =  Term_sub(m,Concat(s,t))                    
        
        Term_sub(Term_var(x),Cons_usual(y,m,s)) =  1 + m + 2*m*x + s + 2*s*x + 3*x + 2*x*y + y
                                                >= m                                          
                                                =  m                                          
        
        Term_sub(Term_var(x),Cons_usual(y,m,s)) =  1 + m + 2*m*x + s + 2*s*x + 3*x + 2*x*y + y
                                                >= s + 2*s*x + x                              
                                                =  Term_sub(Term_var(x),s)                    
        
                     Term_sub(Term_var(x),Id()) =  x                                          
                                                >= x                                          
                                                =  Term_var(x)                                
        
** Step 1.b:3: NaturalPI WORST_CASE(?,O(n^2))
    + Considered Problem:
        - Strict TRS:
            Concat(Concat(s,t),u) -> Concat(s,Concat(t,u))
            Concat(Cons_sum(xi,k,s),t) -> Cons_sum(xi,k,Concat(s,t))
            Concat(Cons_usual(x,m,s),t) -> Cons_usual(x,Term_sub(m,t),Concat(s,t))
            Frozen(m,Sum_term_var(xi),n,s) -> Case(Term_sub(m,s),xi,Term_sub(n,s))
            Sum_sub(xi,Cons_sum(psi,k,s)) -> Sum_constant(k)
            Sum_sub(xi,Cons_sum(psi,k,s)) -> Sum_sub(xi,s)
            Sum_sub(xi,Cons_usual(y,m,s)) -> Sum_sub(xi,s)
            Sum_sub(xi,Id()) -> Sum_term_var(xi)
            Term_sub(Case(m,xi,n),s) -> Frozen(m,Sum_sub(xi,s),n,s)
            Term_sub(Term_app(m,n),s) -> Term_app(Term_sub(m,s),Term_sub(n,s))
            Term_sub(Term_inl(m),s) -> Term_inl(Term_sub(m,s))
            Term_sub(Term_inr(m),s) -> Term_inr(Term_sub(m,s))
            Term_sub(Term_pair(m,n),s) -> Term_pair(Term_sub(m,s),Term_sub(n,s))
            Term_sub(Term_sub(m,s),t) -> Term_sub(m,Concat(s,t))
        - Weak TRS:
            Concat(Id(),s) -> s
            Frozen(m,Sum_constant(Left()),n,s) -> Term_sub(m,s)
            Frozen(m,Sum_constant(Right()),n,s) -> Term_sub(n,s)
            Term_sub(Term_var(x),Cons_sum(xi,k,s)) -> Term_sub(Term_var(x),s)
            Term_sub(Term_var(x),Cons_usual(y,m,s)) -> m
            Term_sub(Term_var(x),Cons_usual(y,m,s)) -> Term_sub(Term_var(x),s)
            Term_sub(Term_var(x),Id()) -> Term_var(x)
        - Signature:
            {Concat/2,Frozen/4,Sum_sub/2,Term_sub/2} / {Case/3,Cons_sum/3,Cons_usual/3,Id/0,Left/0,Right/0
            ,Sum_constant/1,Sum_term_var/1,Term_app/2,Term_inl/1,Term_inr/1,Term_pair/2,Term_var/1}
        - Obligation:
            innermost runtime complexity wrt. defined symbols {Concat,Frozen,Sum_sub,Term_sub} and constructors {Case
            ,Cons_sum,Cons_usual,Id,Left,Right,Sum_constant,Sum_term_var,Term_app,Term_inl,Term_inr,Term_pair,Term_var}
    + Applied Processor:
        NaturalPI {shape = Mixed 2, restrict = Restrict, uargs = UArgs, urules = URules, selector = Just any strict-rules}
    + Details:
        We apply a polynomial interpretation of kind constructor-based(mixed(2)):
        The following argument positions are considered usable:
          uargs(Case) = {1,3},
          uargs(Concat) = {2},
          uargs(Cons_sum) = {3},
          uargs(Cons_usual) = {2,3},
          uargs(Frozen) = {2},
          uargs(Term_app) = {1,2},
          uargs(Term_inl) = {1},
          uargs(Term_inr) = {1},
          uargs(Term_pair) = {1,2},
          uargs(Term_sub) = {2}
        
        Following symbols are considered usable:
          {Concat,Frozen,Sum_sub,Term_sub}
        TcT has computed the following interpretation:
                  p(Case) = 1 + x1 + x2 + x3                                         
                p(Concat) = 2*x1 + x1*x2 + x1^2 + x2                                 
              p(Cons_sum) = x3                                                       
            p(Cons_usual) = 1 + x1 + x2 + x3                                         
                p(Frozen) = 2 + 2*x1 + x1*x4 + x1^2 + x2 + 3*x3 + x3*x4 + x3^2 + 2*x4
                    p(Id) = 1                                                        
                  p(Left) = 0                                                        
                 p(Right) = 0                                                        
          p(Sum_constant) = 0                                                        
               p(Sum_sub) = 2*x1 + x1*x2                                             
          p(Sum_term_var) = x1                                                       
              p(Term_app) = 1 + x1 + x2                                              
              p(Term_inl) = x1                                                       
              p(Term_inr) = 1 + x1                                                   
             p(Term_pair) = 1 + x1 + x2                                              
              p(Term_sub) = 2*x1 + x1*x2 + x1^2 + x2                                 
              p(Term_var) = 0                                                        
        
        Following rules are strictly oriented:
           Concat(Cons_usual(x,m,s),t) = 3 + 4*m + 2*m*s + m*t + 2*m*x + m^2 + 4*s + s*t + 2*s*x + s^2 + 2*t + t*x + 4*x + x^2     
                                       > 1 + 2*m + m*t + m^2 + 2*s + s*t + s^2 + 2*t + x                                           
                                       = Cons_usual(x,Term_sub(m,t),Concat(s,t))                                                   
        
        Frozen(m,Sum_term_var(xi),n,s) = 2 + 2*m + m*s + m^2 + 3*n + n*s + n^2 + 2*s + xi                                          
                                       > 1 + 2*m + m*s + m^2 + 2*n + n*s + n^2 + 2*s + xi                                          
                                       = Case(Term_sub(m,s),xi,Term_sub(n,s))                                                      
        
              Term_sub(Case(m,xi,n),s) = 3 + 4*m + 2*m*n + m*s + 2*m*xi + m^2 + 4*n + n*s + 2*n*xi + n^2 + 2*s + s*xi + 4*xi + xi^2
                                       > 2 + 2*m + m*s + m^2 + 3*n + n*s + n^2 + 2*s + s*xi + 2*xi                                 
                                       = Frozen(m,Sum_sub(xi,s),n,s)                                                               
        
             Term_sub(Term_app(m,n),s) = 3 + 4*m + 2*m*n + m*s + m^2 + 4*n + n*s + n^2 + 2*s                                       
                                       > 1 + 2*m + m*s + m^2 + 2*n + n*s + n^2 + 2*s                                               
                                       = Term_app(Term_sub(m,s),Term_sub(n,s))                                                     
        
               Term_sub(Term_inr(m),s) = 3 + 4*m + m*s + m^2 + 2*s                                                                 
                                       > 1 + 2*m + m*s + m^2 + s                                                                   
                                       = Term_inr(Term_sub(m,s))                                                                   
        
            Term_sub(Term_pair(m,n),s) = 3 + 4*m + 2*m*n + m*s + m^2 + 4*n + n*s + n^2 + 2*s                                       
                                       > 1 + 2*m + m*s + m^2 + 2*n + n*s + n^2 + 2*s                                               
                                       = Term_pair(Term_sub(m,s),Term_sub(n,s))                                                    
        
        
        Following rules are (at-least) weakly oriented:
                          Concat(Concat(s,t),u) =  4*s + 6*s*t + s*t*u + 2*s*t^2 + 2*s*u + 6*s^2 + 6*s^2*t + s^2*t^2 + s^2*u + 4*s^3 + 2*s^3*t + s^4 + 2*t + t*u + t^2 + u
                                                >= 2*s + 2*s*t + s*t*u + s*t^2 + s*u + s^2 + 2*t + t*u + t^2 + u                                                          
                                                =  Concat(s,Concat(t,u))                                                                                                  
        
                     Concat(Cons_sum(xi,k,s),t) =  2*s + s*t + s^2 + t                                                                                                    
                                                >= 2*s + s*t + s^2 + t                                                                                                    
                                                =  Cons_sum(xi,k,Concat(s,t))                                                                                             
        
                                 Concat(Id(),s) =  3 + 2*s                                                                                                                
                                                >= s                                                                                                                      
                                                =  s                                                                                                                      
        
             Frozen(m,Sum_constant(Left()),n,s) =  2 + 2*m + m*s + m^2 + 3*n + n*s + n^2 + 2*s                                                                            
                                                >= 2*m + m*s + m^2 + s                                                                                                    
                                                =  Term_sub(m,s)                                                                                                          
        
            Frozen(m,Sum_constant(Right()),n,s) =  2 + 2*m + m*s + m^2 + 3*n + n*s + n^2 + 2*s                                                                            
                                                >= 2*n + n*s + n^2 + s                                                                                                    
                                                =  Term_sub(n,s)                                                                                                          
        
                  Sum_sub(xi,Cons_sum(psi,k,s)) =  s*xi + 2*xi                                                                                                            
                                                >= 0                                                                                                                      
                                                =  Sum_constant(k)                                                                                                        
        
                  Sum_sub(xi,Cons_sum(psi,k,s)) =  s*xi + 2*xi                                                                                                            
                                                >= s*xi + 2*xi                                                                                                            
                                                =  Sum_sub(xi,s)                                                                                                          
        
                  Sum_sub(xi,Cons_usual(y,m,s)) =  m*xi + s*xi + 3*xi + xi*y                                                                                              
                                                >= s*xi + 2*xi                                                                                                            
                                                =  Sum_sub(xi,s)                                                                                                          
        
                               Sum_sub(xi,Id()) =  3*xi                                                                                                                   
                                                >= xi                                                                                                                     
                                                =  Sum_term_var(xi)                                                                                                       
        
                        Term_sub(Term_inl(m),s) =  2*m + m*s + m^2 + s                                                                                                    
                                                >= 2*m + m*s + m^2 + s                                                                                                    
                                                =  Term_inl(Term_sub(m,s))                                                                                                
        
                      Term_sub(Term_sub(m,s),t) =  4*m + 6*m*s + m*s*t + 2*m*s^2 + 2*m*t + 6*m^2 + 6*m^2*s + m^2*s^2 + m^2*t + 4*m^3 + 2*m^3*s + m^4 + 2*s + s*t + s^2 + t
                                                >= 2*m + 2*m*s + m*s*t + m*s^2 + m*t + m^2 + 2*s + s*t + s^2 + t                                                          
                                                =  Term_sub(m,Concat(s,t))                                                                                                
        
         Term_sub(Term_var(x),Cons_sum(xi,k,s)) =  s                                                                                                                      
                                                >= s                                                                                                                      
                                                =  Term_sub(Term_var(x),s)                                                                                                
        
        Term_sub(Term_var(x),Cons_usual(y,m,s)) =  1 + m + s + y                                                                                                          
                                                >= m                                                                                                                      
                                                =  m                                                                                                                      
        
        Term_sub(Term_var(x),Cons_usual(y,m,s)) =  1 + m + s + y                                                                                                          
                                                >= s                                                                                                                      
                                                =  Term_sub(Term_var(x),s)                                                                                                
        
                     Term_sub(Term_var(x),Id()) =  1                                                                                                                      
                                                >= 0                                                                                                                      
                                                =  Term_var(x)                                                                                                            
        
** Step 1.b:4: NaturalPI WORST_CASE(?,O(n^2))
    + Considered Problem:
        - Strict TRS:
            Concat(Concat(s,t),u) -> Concat(s,Concat(t,u))
            Concat(Cons_sum(xi,k,s),t) -> Cons_sum(xi,k,Concat(s,t))
            Sum_sub(xi,Cons_sum(psi,k,s)) -> Sum_constant(k)
            Sum_sub(xi,Cons_sum(psi,k,s)) -> Sum_sub(xi,s)
            Sum_sub(xi,Cons_usual(y,m,s)) -> Sum_sub(xi,s)
            Sum_sub(xi,Id()) -> Sum_term_var(xi)
            Term_sub(Term_inl(m),s) -> Term_inl(Term_sub(m,s))
            Term_sub(Term_sub(m,s),t) -> Term_sub(m,Concat(s,t))
        - Weak TRS:
            Concat(Cons_usual(x,m,s),t) -> Cons_usual(x,Term_sub(m,t),Concat(s,t))
            Concat(Id(),s) -> s
            Frozen(m,Sum_constant(Left()),n,s) -> Term_sub(m,s)
            Frozen(m,Sum_constant(Right()),n,s) -> Term_sub(n,s)
            Frozen(m,Sum_term_var(xi),n,s) -> Case(Term_sub(m,s),xi,Term_sub(n,s))
            Term_sub(Case(m,xi,n),s) -> Frozen(m,Sum_sub(xi,s),n,s)
            Term_sub(Term_app(m,n),s) -> Term_app(Term_sub(m,s),Term_sub(n,s))
            Term_sub(Term_inr(m),s) -> Term_inr(Term_sub(m,s))
            Term_sub(Term_pair(m,n),s) -> Term_pair(Term_sub(m,s),Term_sub(n,s))
            Term_sub(Term_var(x),Cons_sum(xi,k,s)) -> Term_sub(Term_var(x),s)
            Term_sub(Term_var(x),Cons_usual(y,m,s)) -> m
            Term_sub(Term_var(x),Cons_usual(y,m,s)) -> Term_sub(Term_var(x),s)
            Term_sub(Term_var(x),Id()) -> Term_var(x)
        - Signature:
            {Concat/2,Frozen/4,Sum_sub/2,Term_sub/2} / {Case/3,Cons_sum/3,Cons_usual/3,Id/0,Left/0,Right/0
            ,Sum_constant/1,Sum_term_var/1,Term_app/2,Term_inl/1,Term_inr/1,Term_pair/2,Term_var/1}
        - Obligation:
            innermost runtime complexity wrt. defined symbols {Concat,Frozen,Sum_sub,Term_sub} and constructors {Case
            ,Cons_sum,Cons_usual,Id,Left,Right,Sum_constant,Sum_term_var,Term_app,Term_inl,Term_inr,Term_pair,Term_var}
    + Applied Processor:
        NaturalPI {shape = Mixed 2, restrict = Restrict, uargs = UArgs, urules = URules, selector = Just any strict-rules}
    + Details:
        We apply a polynomial interpretation of kind constructor-based(mixed(2)):
        The following argument positions are considered usable:
          uargs(Case) = {1,3},
          uargs(Concat) = {2},
          uargs(Cons_sum) = {3},
          uargs(Cons_usual) = {2,3},
          uargs(Frozen) = {2},
          uargs(Term_app) = {1,2},
          uargs(Term_inl) = {1},
          uargs(Term_inr) = {1},
          uargs(Term_pair) = {1,2},
          uargs(Term_sub) = {2}
        
        Following symbols are considered usable:
          {Concat,Frozen,Sum_sub,Term_sub}
        TcT has computed the following interpretation:
                  p(Case) = 1 + x1 + x3                                  
                p(Concat) = x1 + 2*x1*x2 + x2                            
              p(Cons_sum) = x2 + x3                                      
            p(Cons_usual) = 1 + x2 + x3                                  
                p(Frozen) = x1 + 2*x1*x4 + x2 + x2*x4 + x3 + 2*x3*x4 + x4
                    p(Id) = 0                                            
                  p(Left) = 0                                            
                 p(Right) = 1                                            
          p(Sum_constant) = 0                                            
               p(Sum_sub) = 1                                            
          p(Sum_term_var) = 1                                            
              p(Term_app) = 1 + x1 + x2                                  
              p(Term_inl) = x1                                           
              p(Term_inr) = x1                                           
             p(Term_pair) = 1 + x1 + x2                                  
              p(Term_sub) = x1 + 2*x1*x2 + x2                            
              p(Term_var) = 0                                            
        
        Following rules are strictly oriented:
        Sum_sub(xi,Cons_sum(psi,k,s)) = 1              
                                      > 0              
                                      = Sum_constant(k)
        
        
        Following rules are (at-least) weakly oriented:
                          Concat(Concat(s,t),u) =  s + 2*s*t + 4*s*t*u + 2*s*u + t + 2*t*u + u
                                                >= s + 2*s*t + 4*s*t*u + 2*s*u + t + 2*t*u + u
                                                =  Concat(s,Concat(t,u))                      
        
                     Concat(Cons_sum(xi,k,s),t) =  k + 2*k*t + s + 2*s*t + t                  
                                                >= k + s + 2*s*t + t                          
                                                =  Cons_sum(xi,k,Concat(s,t))                 
        
                    Concat(Cons_usual(x,m,s),t) =  1 + m + 2*m*t + s + 2*s*t + 3*t            
                                                >= 1 + m + 2*m*t + s + 2*s*t + 2*t            
                                                =  Cons_usual(x,Term_sub(m,t),Concat(s,t))    
        
                                 Concat(Id(),s) =  s                                          
                                                >= s                                          
                                                =  s                                          
        
             Frozen(m,Sum_constant(Left()),n,s) =  m + 2*m*s + n + 2*n*s + s                  
                                                >= m + 2*m*s + s                              
                                                =  Term_sub(m,s)                              
        
            Frozen(m,Sum_constant(Right()),n,s) =  m + 2*m*s + n + 2*n*s + s                  
                                                >= n + 2*n*s + s                              
                                                =  Term_sub(n,s)                              
        
                 Frozen(m,Sum_term_var(xi),n,s) =  1 + m + 2*m*s + n + 2*n*s + 2*s            
                                                >= 1 + m + 2*m*s + n + 2*n*s + 2*s            
                                                =  Case(Term_sub(m,s),xi,Term_sub(n,s))       
        
                  Sum_sub(xi,Cons_sum(psi,k,s)) =  1                                          
                                                >= 1                                          
                                                =  Sum_sub(xi,s)                              
        
                  Sum_sub(xi,Cons_usual(y,m,s)) =  1                                          
                                                >= 1                                          
                                                =  Sum_sub(xi,s)                              
        
                               Sum_sub(xi,Id()) =  1                                          
                                                >= 1                                          
                                                =  Sum_term_var(xi)                           
        
                       Term_sub(Case(m,xi,n),s) =  1 + m + 2*m*s + n + 2*n*s + 3*s            
                                                >= 1 + m + 2*m*s + n + 2*n*s + 2*s            
                                                =  Frozen(m,Sum_sub(xi,s),n,s)                
        
                      Term_sub(Term_app(m,n),s) =  1 + m + 2*m*s + n + 2*n*s + 3*s            
                                                >= 1 + m + 2*m*s + n + 2*n*s + 2*s            
                                                =  Term_app(Term_sub(m,s),Term_sub(n,s))      
        
                        Term_sub(Term_inl(m),s) =  m + 2*m*s + s                              
                                                >= m + 2*m*s + s                              
                                                =  Term_inl(Term_sub(m,s))                    
        
                        Term_sub(Term_inr(m),s) =  m + 2*m*s + s                              
                                                >= m + 2*m*s + s                              
                                                =  Term_inr(Term_sub(m,s))                    
        
                     Term_sub(Term_pair(m,n),s) =  1 + m + 2*m*s + n + 2*n*s + 3*s            
                                                >= 1 + m + 2*m*s + n + 2*n*s + 2*s            
                                                =  Term_pair(Term_sub(m,s),Term_sub(n,s))     
        
                      Term_sub(Term_sub(m,s),t) =  m + 2*m*s + 4*m*s*t + 2*m*t + s + 2*s*t + t
                                                >= m + 2*m*s + 4*m*s*t + 2*m*t + s + 2*s*t + t
                                                =  Term_sub(m,Concat(s,t))                    
        
         Term_sub(Term_var(x),Cons_sum(xi,k,s)) =  k + s                                      
                                                >= s                                          
                                                =  Term_sub(Term_var(x),s)                    
        
        Term_sub(Term_var(x),Cons_usual(y,m,s)) =  1 + m + s                                  
                                                >= m                                          
                                                =  m                                          
        
        Term_sub(Term_var(x),Cons_usual(y,m,s)) =  1 + m + s                                  
                                                >= s                                          
                                                =  Term_sub(Term_var(x),s)                    
        
                     Term_sub(Term_var(x),Id()) =  0                                          
                                                >= 0                                          
                                                =  Term_var(x)                                
        
** Step 1.b:5: NaturalPI WORST_CASE(?,O(n^2))
    + Considered Problem:
        - Strict TRS:
            Concat(Concat(s,t),u) -> Concat(s,Concat(t,u))
            Concat(Cons_sum(xi,k,s),t) -> Cons_sum(xi,k,Concat(s,t))
            Sum_sub(xi,Cons_sum(psi,k,s)) -> Sum_sub(xi,s)
            Sum_sub(xi,Cons_usual(y,m,s)) -> Sum_sub(xi,s)
            Sum_sub(xi,Id()) -> Sum_term_var(xi)
            Term_sub(Term_inl(m),s) -> Term_inl(Term_sub(m,s))
            Term_sub(Term_sub(m,s),t) -> Term_sub(m,Concat(s,t))
        - Weak TRS:
            Concat(Cons_usual(x,m,s),t) -> Cons_usual(x,Term_sub(m,t),Concat(s,t))
            Concat(Id(),s) -> s
            Frozen(m,Sum_constant(Left()),n,s) -> Term_sub(m,s)
            Frozen(m,Sum_constant(Right()),n,s) -> Term_sub(n,s)
            Frozen(m,Sum_term_var(xi),n,s) -> Case(Term_sub(m,s),xi,Term_sub(n,s))
            Sum_sub(xi,Cons_sum(psi,k,s)) -> Sum_constant(k)
            Term_sub(Case(m,xi,n),s) -> Frozen(m,Sum_sub(xi,s),n,s)
            Term_sub(Term_app(m,n),s) -> Term_app(Term_sub(m,s),Term_sub(n,s))
            Term_sub(Term_inr(m),s) -> Term_inr(Term_sub(m,s))
            Term_sub(Term_pair(m,n),s) -> Term_pair(Term_sub(m,s),Term_sub(n,s))
            Term_sub(Term_var(x),Cons_sum(xi,k,s)) -> Term_sub(Term_var(x),s)
            Term_sub(Term_var(x),Cons_usual(y,m,s)) -> m
            Term_sub(Term_var(x),Cons_usual(y,m,s)) -> Term_sub(Term_var(x),s)
            Term_sub(Term_var(x),Id()) -> Term_var(x)
        - Signature:
            {Concat/2,Frozen/4,Sum_sub/2,Term_sub/2} / {Case/3,Cons_sum/3,Cons_usual/3,Id/0,Left/0,Right/0
            ,Sum_constant/1,Sum_term_var/1,Term_app/2,Term_inl/1,Term_inr/1,Term_pair/2,Term_var/1}
        - Obligation:
            innermost runtime complexity wrt. defined symbols {Concat,Frozen,Sum_sub,Term_sub} and constructors {Case
            ,Cons_sum,Cons_usual,Id,Left,Right,Sum_constant,Sum_term_var,Term_app,Term_inl,Term_inr,Term_pair,Term_var}
    + Applied Processor:
        NaturalPI {shape = Mixed 2, restrict = Restrict, uargs = UArgs, urules = URules, selector = Just any strict-rules}
    + Details:
        We apply a polynomial interpretation of kind constructor-based(mixed(2)):
        The following argument positions are considered usable:
          uargs(Case) = {1,3},
          uargs(Concat) = {2},
          uargs(Cons_sum) = {3},
          uargs(Cons_usual) = {2,3},
          uargs(Frozen) = {2},
          uargs(Term_app) = {1,2},
          uargs(Term_inl) = {1},
          uargs(Term_inr) = {1},
          uargs(Term_pair) = {1,2},
          uargs(Term_sub) = {2}
        
        Following symbols are considered usable:
          {Concat,Frozen,Sum_sub,Term_sub}
        TcT has computed the following interpretation:
                  p(Case) = 1 + x1 + x2 + x3                           
                p(Concat) = x1 + 2*x1*x2 + x2                          
              p(Cons_sum) = x1 + x3                                    
            p(Cons_usual) = 1 + x1 + x2 + x3                           
                p(Frozen) = 1 + x1 + 2*x1*x4 + x2 + x3 + 2*x3*x4 + 2*x4
                    p(Id) = 1                                          
                  p(Left) = 1                                          
                 p(Right) = 0                                          
          p(Sum_constant) = 0                                          
               p(Sum_sub) = x1*x2 + x2                                 
          p(Sum_term_var) = x1                                         
              p(Term_app) = 1 + x1 + x2                                
              p(Term_inl) = x1                                         
              p(Term_inr) = x1                                         
             p(Term_pair) = 1 + x1 + x2                                
              p(Term_sub) = x1 + 2*x1*x2 + x2                          
              p(Term_var) = 0                                          
        
        Following rules are strictly oriented:
        Sum_sub(xi,Cons_usual(y,m,s)) = 1 + m + m*xi + s + s*xi + xi + xi*y + y
                                      > s + s*xi                               
                                      = Sum_sub(xi,s)                          
        
                     Sum_sub(xi,Id()) = 1 + xi                                 
                                      > xi                                     
                                      = Sum_term_var(xi)                       
        
        
        Following rules are (at-least) weakly oriented:
                          Concat(Concat(s,t),u) =  s + 2*s*t + 4*s*t*u + 2*s*u + t + 2*t*u + u  
                                                >= s + 2*s*t + 4*s*t*u + 2*s*u + t + 2*t*u + u  
                                                =  Concat(s,Concat(t,u))                        
        
                     Concat(Cons_sum(xi,k,s),t) =  s + 2*s*t + t + 2*t*xi + xi                  
                                                >= s + 2*s*t + t + xi                           
                                                =  Cons_sum(xi,k,Concat(s,t))                   
        
                    Concat(Cons_usual(x,m,s),t) =  1 + m + 2*m*t + s + 2*s*t + 3*t + 2*t*x + x  
                                                >= 1 + m + 2*m*t + s + 2*s*t + 2*t + x          
                                                =  Cons_usual(x,Term_sub(m,t),Concat(s,t))      
        
                                 Concat(Id(),s) =  1 + 3*s                                      
                                                >= s                                            
                                                =  s                                            
        
             Frozen(m,Sum_constant(Left()),n,s) =  1 + m + 2*m*s + n + 2*n*s + 2*s              
                                                >= m + 2*m*s + s                                
                                                =  Term_sub(m,s)                                
        
            Frozen(m,Sum_constant(Right()),n,s) =  1 + m + 2*m*s + n + 2*n*s + 2*s              
                                                >= n + 2*n*s + s                                
                                                =  Term_sub(n,s)                                
        
                 Frozen(m,Sum_term_var(xi),n,s) =  1 + m + 2*m*s + n + 2*n*s + 2*s + xi         
                                                >= 1 + m + 2*m*s + n + 2*n*s + 2*s + xi         
                                                =  Case(Term_sub(m,s),xi,Term_sub(n,s))         
        
                  Sum_sub(xi,Cons_sum(psi,k,s)) =  psi + psi*xi + s + s*xi                      
                                                >= 0                                            
                                                =  Sum_constant(k)                              
        
                  Sum_sub(xi,Cons_sum(psi,k,s)) =  psi + psi*xi + s + s*xi                      
                                                >= s + s*xi                                     
                                                =  Sum_sub(xi,s)                                
        
                       Term_sub(Case(m,xi,n),s) =  1 + m + 2*m*s + n + 2*n*s + 3*s + 2*s*xi + xi
                                                >= 1 + m + 2*m*s + n + 2*n*s + 3*s + s*xi       
                                                =  Frozen(m,Sum_sub(xi,s),n,s)                  
        
                      Term_sub(Term_app(m,n),s) =  1 + m + 2*m*s + n + 2*n*s + 3*s              
                                                >= 1 + m + 2*m*s + n + 2*n*s + 2*s              
                                                =  Term_app(Term_sub(m,s),Term_sub(n,s))        
        
                        Term_sub(Term_inl(m),s) =  m + 2*m*s + s                                
                                                >= m + 2*m*s + s                                
                                                =  Term_inl(Term_sub(m,s))                      
        
                        Term_sub(Term_inr(m),s) =  m + 2*m*s + s                                
                                                >= m + 2*m*s + s                                
                                                =  Term_inr(Term_sub(m,s))                      
        
                     Term_sub(Term_pair(m,n),s) =  1 + m + 2*m*s + n + 2*n*s + 3*s              
                                                >= 1 + m + 2*m*s + n + 2*n*s + 2*s              
                                                =  Term_pair(Term_sub(m,s),Term_sub(n,s))       
        
                      Term_sub(Term_sub(m,s),t) =  m + 2*m*s + 4*m*s*t + 2*m*t + s + 2*s*t + t  
                                                >= m + 2*m*s + 4*m*s*t + 2*m*t + s + 2*s*t + t  
                                                =  Term_sub(m,Concat(s,t))                      
        
         Term_sub(Term_var(x),Cons_sum(xi,k,s)) =  s + xi                                       
                                                >= s                                            
                                                =  Term_sub(Term_var(x),s)                      
        
        Term_sub(Term_var(x),Cons_usual(y,m,s)) =  1 + m + s + y                                
                                                >= m                                            
                                                =  m                                            
        
        Term_sub(Term_var(x),Cons_usual(y,m,s)) =  1 + m + s + y                                
                                                >= s                                            
                                                =  Term_sub(Term_var(x),s)                      
        
                     Term_sub(Term_var(x),Id()) =  1                                            
                                                >= 0                                            
                                                =  Term_var(x)                                  
        
** Step 1.b:6: NaturalPI WORST_CASE(?,O(n^2))
    + Considered Problem:
        - Strict TRS:
            Concat(Concat(s,t),u) -> Concat(s,Concat(t,u))
            Concat(Cons_sum(xi,k,s),t) -> Cons_sum(xi,k,Concat(s,t))
            Sum_sub(xi,Cons_sum(psi,k,s)) -> Sum_sub(xi,s)
            Term_sub(Term_inl(m),s) -> Term_inl(Term_sub(m,s))
            Term_sub(Term_sub(m,s),t) -> Term_sub(m,Concat(s,t))
        - Weak TRS:
            Concat(Cons_usual(x,m,s),t) -> Cons_usual(x,Term_sub(m,t),Concat(s,t))
            Concat(Id(),s) -> s
            Frozen(m,Sum_constant(Left()),n,s) -> Term_sub(m,s)
            Frozen(m,Sum_constant(Right()),n,s) -> Term_sub(n,s)
            Frozen(m,Sum_term_var(xi),n,s) -> Case(Term_sub(m,s),xi,Term_sub(n,s))
            Sum_sub(xi,Cons_sum(psi,k,s)) -> Sum_constant(k)
            Sum_sub(xi,Cons_usual(y,m,s)) -> Sum_sub(xi,s)
            Sum_sub(xi,Id()) -> Sum_term_var(xi)
            Term_sub(Case(m,xi,n),s) -> Frozen(m,Sum_sub(xi,s),n,s)
            Term_sub(Term_app(m,n),s) -> Term_app(Term_sub(m,s),Term_sub(n,s))
            Term_sub(Term_inr(m),s) -> Term_inr(Term_sub(m,s))
            Term_sub(Term_pair(m,n),s) -> Term_pair(Term_sub(m,s),Term_sub(n,s))
            Term_sub(Term_var(x),Cons_sum(xi,k,s)) -> Term_sub(Term_var(x),s)
            Term_sub(Term_var(x),Cons_usual(y,m,s)) -> m
            Term_sub(Term_var(x),Cons_usual(y,m,s)) -> Term_sub(Term_var(x),s)
            Term_sub(Term_var(x),Id()) -> Term_var(x)
        - Signature:
            {Concat/2,Frozen/4,Sum_sub/2,Term_sub/2} / {Case/3,Cons_sum/3,Cons_usual/3,Id/0,Left/0,Right/0
            ,Sum_constant/1,Sum_term_var/1,Term_app/2,Term_inl/1,Term_inr/1,Term_pair/2,Term_var/1}
        - Obligation:
            innermost runtime complexity wrt. defined symbols {Concat,Frozen,Sum_sub,Term_sub} and constructors {Case
            ,Cons_sum,Cons_usual,Id,Left,Right,Sum_constant,Sum_term_var,Term_app,Term_inl,Term_inr,Term_pair,Term_var}
    + Applied Processor:
        NaturalPI {shape = Mixed 2, restrict = Restrict, uargs = UArgs, urules = URules, selector = Just any strict-rules}
    + Details:
        We apply a polynomial interpretation of kind constructor-based(mixed(2)):
        The following argument positions are considered usable:
          uargs(Case) = {1,3},
          uargs(Concat) = {2},
          uargs(Cons_sum) = {3},
          uargs(Cons_usual) = {2,3},
          uargs(Frozen) = {2},
          uargs(Term_app) = {1,2},
          uargs(Term_inl) = {1},
          uargs(Term_inr) = {1},
          uargs(Term_pair) = {1,2},
          uargs(Term_sub) = {2}
        
        Following symbols are considered usable:
          {Concat,Frozen,Sum_sub,Term_sub}
        TcT has computed the following interpretation:
                  p(Case) = 1 + x1 + x3                                  
                p(Concat) = 2*x1 + x1*x2 + x2                            
              p(Cons_sum) = x3                                           
            p(Cons_usual) = 1 + x1 + x2 + x3                             
                p(Frozen) = 2 + 2*x1 + x1*x4 + 2*x2 + 2*x3 + x3*x4 + 2*x4
                    p(Id) = 0                                            
                  p(Left) = 0                                            
                 p(Right) = 0                                            
          p(Sum_constant) = 0                                            
               p(Sum_sub) = 0                                            
          p(Sum_term_var) = 0                                            
              p(Term_app) = 1 + x1 + x2                                  
              p(Term_inl) = 1 + x1                                       
              p(Term_inr) = x1                                           
             p(Term_pair) = 1 + x1 + x2                                  
              p(Term_sub) = 2*x1 + x1*x2 + x2                            
              p(Term_var) = x1                                           
        
        Following rules are strictly oriented:
        Term_sub(Term_inl(m),s) = 2 + 2*m + m*s + 2*s    
                                > 1 + 2*m + m*s + s      
                                = Term_inl(Term_sub(m,s))
        
        
        Following rules are (at-least) weakly oriented:
                          Concat(Concat(s,t),u) =  4*s + 2*s*t + s*t*u + 2*s*u + 2*t + t*u + u
                                                >= 2*s + 2*s*t + s*t*u + s*u + 2*t + t*u + u  
                                                =  Concat(s,Concat(t,u))                      
        
                     Concat(Cons_sum(xi,k,s),t) =  2*s + s*t + t                              
                                                >= 2*s + s*t + t                              
                                                =  Cons_sum(xi,k,Concat(s,t))                 
        
                    Concat(Cons_usual(x,m,s),t) =  2 + 2*m + m*t + 2*s + s*t + 2*t + t*x + 2*x
                                                >= 1 + 2*m + m*t + 2*s + s*t + 2*t + x        
                                                =  Cons_usual(x,Term_sub(m,t),Concat(s,t))    
        
                                 Concat(Id(),s) =  s                                          
                                                >= s                                          
                                                =  s                                          
        
             Frozen(m,Sum_constant(Left()),n,s) =  2 + 2*m + m*s + 2*n + n*s + 2*s            
                                                >= 2*m + m*s + s                              
                                                =  Term_sub(m,s)                              
        
            Frozen(m,Sum_constant(Right()),n,s) =  2 + 2*m + m*s + 2*n + n*s + 2*s            
                                                >= 2*n + n*s + s                              
                                                =  Term_sub(n,s)                              
        
                 Frozen(m,Sum_term_var(xi),n,s) =  2 + 2*m + m*s + 2*n + n*s + 2*s            
                                                >= 1 + 2*m + m*s + 2*n + n*s + 2*s            
                                                =  Case(Term_sub(m,s),xi,Term_sub(n,s))       
        
                  Sum_sub(xi,Cons_sum(psi,k,s)) =  0                                          
                                                >= 0                                          
                                                =  Sum_constant(k)                            
        
                  Sum_sub(xi,Cons_sum(psi,k,s)) =  0                                          
                                                >= 0                                          
                                                =  Sum_sub(xi,s)                              
        
                  Sum_sub(xi,Cons_usual(y,m,s)) =  0                                          
                                                >= 0                                          
                                                =  Sum_sub(xi,s)                              
        
                               Sum_sub(xi,Id()) =  0                                          
                                                >= 0                                          
                                                =  Sum_term_var(xi)                           
        
                       Term_sub(Case(m,xi,n),s) =  2 + 2*m + m*s + 2*n + n*s + 2*s            
                                                >= 2 + 2*m + m*s + 2*n + n*s + 2*s            
                                                =  Frozen(m,Sum_sub(xi,s),n,s)                
        
                      Term_sub(Term_app(m,n),s) =  2 + 2*m + m*s + 2*n + n*s + 2*s            
                                                >= 1 + 2*m + m*s + 2*n + n*s + 2*s            
                                                =  Term_app(Term_sub(m,s),Term_sub(n,s))      
        
                        Term_sub(Term_inr(m),s) =  2*m + m*s + s                              
                                                >= 2*m + m*s + s                              
                                                =  Term_inr(Term_sub(m,s))                    
        
                     Term_sub(Term_pair(m,n),s) =  2 + 2*m + m*s + 2*n + n*s + 2*s            
                                                >= 1 + 2*m + m*s + 2*n + n*s + 2*s            
                                                =  Term_pair(Term_sub(m,s),Term_sub(n,s))     
        
                      Term_sub(Term_sub(m,s),t) =  4*m + 2*m*s + m*s*t + 2*m*t + 2*s + s*t + t
                                                >= 2*m + 2*m*s + m*s*t + m*t + 2*s + s*t + t  
                                                =  Term_sub(m,Concat(s,t))                    
        
         Term_sub(Term_var(x),Cons_sum(xi,k,s)) =  s + s*x + 2*x                              
                                                >= s + s*x + 2*x                              
                                                =  Term_sub(Term_var(x),s)                    
        
        Term_sub(Term_var(x),Cons_usual(y,m,s)) =  1 + m + m*x + s + s*x + 3*x + x*y + y      
                                                >= m                                          
                                                =  m                                          
        
        Term_sub(Term_var(x),Cons_usual(y,m,s)) =  1 + m + m*x + s + s*x + 3*x + x*y + y      
                                                >= s + s*x + 2*x                              
                                                =  Term_sub(Term_var(x),s)                    
        
                     Term_sub(Term_var(x),Id()) =  2*x                                        
                                                >= x                                          
                                                =  Term_var(x)                                
        
** Step 1.b:7: NaturalPI WORST_CASE(?,O(n^2))
    + Considered Problem:
        - Strict TRS:
            Concat(Concat(s,t),u) -> Concat(s,Concat(t,u))
            Concat(Cons_sum(xi,k,s),t) -> Cons_sum(xi,k,Concat(s,t))
            Sum_sub(xi,Cons_sum(psi,k,s)) -> Sum_sub(xi,s)
            Term_sub(Term_sub(m,s),t) -> Term_sub(m,Concat(s,t))
        - Weak TRS:
            Concat(Cons_usual(x,m,s),t) -> Cons_usual(x,Term_sub(m,t),Concat(s,t))
            Concat(Id(),s) -> s
            Frozen(m,Sum_constant(Left()),n,s) -> Term_sub(m,s)
            Frozen(m,Sum_constant(Right()),n,s) -> Term_sub(n,s)
            Frozen(m,Sum_term_var(xi),n,s) -> Case(Term_sub(m,s),xi,Term_sub(n,s))
            Sum_sub(xi,Cons_sum(psi,k,s)) -> Sum_constant(k)
            Sum_sub(xi,Cons_usual(y,m,s)) -> Sum_sub(xi,s)
            Sum_sub(xi,Id()) -> Sum_term_var(xi)
            Term_sub(Case(m,xi,n),s) -> Frozen(m,Sum_sub(xi,s),n,s)
            Term_sub(Term_app(m,n),s) -> Term_app(Term_sub(m,s),Term_sub(n,s))
            Term_sub(Term_inl(m),s) -> Term_inl(Term_sub(m,s))
            Term_sub(Term_inr(m),s) -> Term_inr(Term_sub(m,s))
            Term_sub(Term_pair(m,n),s) -> Term_pair(Term_sub(m,s),Term_sub(n,s))
            Term_sub(Term_var(x),Cons_sum(xi,k,s)) -> Term_sub(Term_var(x),s)
            Term_sub(Term_var(x),Cons_usual(y,m,s)) -> m
            Term_sub(Term_var(x),Cons_usual(y,m,s)) -> Term_sub(Term_var(x),s)
            Term_sub(Term_var(x),Id()) -> Term_var(x)
        - Signature:
            {Concat/2,Frozen/4,Sum_sub/2,Term_sub/2} / {Case/3,Cons_sum/3,Cons_usual/3,Id/0,Left/0,Right/0
            ,Sum_constant/1,Sum_term_var/1,Term_app/2,Term_inl/1,Term_inr/1,Term_pair/2,Term_var/1}
        - Obligation:
            innermost runtime complexity wrt. defined symbols {Concat,Frozen,Sum_sub,Term_sub} and constructors {Case
            ,Cons_sum,Cons_usual,Id,Left,Right,Sum_constant,Sum_term_var,Term_app,Term_inl,Term_inr,Term_pair,Term_var}
    + Applied Processor:
        NaturalPI {shape = Mixed 2, restrict = Restrict, uargs = UArgs, urules = URules, selector = Just any strict-rules}
    + Details:
        We apply a polynomial interpretation of kind constructor-based(mixed(2)):
        The following argument positions are considered usable:
          uargs(Case) = {1,3},
          uargs(Concat) = {2},
          uargs(Cons_sum) = {3},
          uargs(Cons_usual) = {2,3},
          uargs(Frozen) = {2},
          uargs(Term_app) = {1,2},
          uargs(Term_inl) = {1},
          uargs(Term_inr) = {1},
          uargs(Term_pair) = {1,2},
          uargs(Term_sub) = {2}
        
        Following symbols are considered usable:
          {Concat,Frozen,Sum_sub,Term_sub}
        TcT has computed the following interpretation:
                  p(Case) = 1 + x1 + x3                                                
                p(Concat) = 2*x1 + x1*x2 + x1^2 + x2                                   
              p(Cons_sum) = 1 + x1 + x3                                                
            p(Cons_usual) = 1 + x2 + x3                                                
                p(Frozen) = 1 + 2*x1 + x1*x4 + x1^2 + 2*x2 + 2*x3 + x3*x4 + x3^2 + 2*x4
                    p(Id) = 0                                                          
                  p(Left) = 1                                                          
                 p(Right) = 0                                                          
          p(Sum_constant) = 0                                                          
               p(Sum_sub) = 0                                                          
          p(Sum_term_var) = 0                                                          
              p(Term_app) = 1 + x1 + x2                                                
              p(Term_inl) = 1 + x1                                                     
              p(Term_inr) = x1                                                         
             p(Term_pair) = 1 + x1 + x2                                                
              p(Term_sub) = 2*x1 + x1*x2 + x1^2 + x2                                   
              p(Term_var) = 0                                                          
        
        Following rules are strictly oriented:
        Concat(Cons_sum(xi,k,s),t) = 3 + 4*s + s*t + 2*s*xi + s^2 + 2*t + t*xi + 4*xi + xi^2
                                   > 1 + 2*s + s*t + s^2 + t + xi                           
                                   = Cons_sum(xi,k,Concat(s,t))                             
        
        
        Following rules are (at-least) weakly oriented:
                          Concat(Concat(s,t),u) =  4*s + 6*s*t + s*t*u + 2*s*t^2 + 2*s*u + 6*s^2 + 6*s^2*t + s^2*t^2 + s^2*u + 4*s^3 + 2*s^3*t + s^4 + 2*t + t*u + t^2 + u
                                                >= 2*s + 2*s*t + s*t*u + s*t^2 + s*u + s^2 + 2*t + t*u + t^2 + u                                                          
                                                =  Concat(s,Concat(t,u))                                                                                                  
        
                    Concat(Cons_usual(x,m,s),t) =  3 + 4*m + 2*m*s + m*t + m^2 + 4*s + s*t + s^2 + 2*t                                                                    
                                                >= 1 + 2*m + m*t + m^2 + 2*s + s*t + s^2 + 2*t                                                                            
                                                =  Cons_usual(x,Term_sub(m,t),Concat(s,t))                                                                                
        
                                 Concat(Id(),s) =  s                                                                                                                      
                                                >= s                                                                                                                      
                                                =  s                                                                                                                      
        
             Frozen(m,Sum_constant(Left()),n,s) =  1 + 2*m + m*s + m^2 + 2*n + n*s + n^2 + 2*s                                                                            
                                                >= 2*m + m*s + m^2 + s                                                                                                    
                                                =  Term_sub(m,s)                                                                                                          
        
            Frozen(m,Sum_constant(Right()),n,s) =  1 + 2*m + m*s + m^2 + 2*n + n*s + n^2 + 2*s                                                                            
                                                >= 2*n + n*s + n^2 + s                                                                                                    
                                                =  Term_sub(n,s)                                                                                                          
        
                 Frozen(m,Sum_term_var(xi),n,s) =  1 + 2*m + m*s + m^2 + 2*n + n*s + n^2 + 2*s                                                                            
                                                >= 1 + 2*m + m*s + m^2 + 2*n + n*s + n^2 + 2*s                                                                            
                                                =  Case(Term_sub(m,s),xi,Term_sub(n,s))                                                                                   
        
                  Sum_sub(xi,Cons_sum(psi,k,s)) =  0                                                                                                                      
                                                >= 0                                                                                                                      
                                                =  Sum_constant(k)                                                                                                        
        
                  Sum_sub(xi,Cons_sum(psi,k,s)) =  0                                                                                                                      
                                                >= 0                                                                                                                      
                                                =  Sum_sub(xi,s)                                                                                                          
        
                  Sum_sub(xi,Cons_usual(y,m,s)) =  0                                                                                                                      
                                                >= 0                                                                                                                      
                                                =  Sum_sub(xi,s)                                                                                                          
        
                               Sum_sub(xi,Id()) =  0                                                                                                                      
                                                >= 0                                                                                                                      
                                                =  Sum_term_var(xi)                                                                                                       
        
                       Term_sub(Case(m,xi,n),s) =  3 + 4*m + 2*m*n + m*s + m^2 + 4*n + n*s + n^2 + 2*s                                                                    
                                                >= 1 + 2*m + m*s + m^2 + 2*n + n*s + n^2 + 2*s                                                                            
                                                =  Frozen(m,Sum_sub(xi,s),n,s)                                                                                            
        
                      Term_sub(Term_app(m,n),s) =  3 + 4*m + 2*m*n + m*s + m^2 + 4*n + n*s + n^2 + 2*s                                                                    
                                                >= 1 + 2*m + m*s + m^2 + 2*n + n*s + n^2 + 2*s                                                                            
                                                =  Term_app(Term_sub(m,s),Term_sub(n,s))                                                                                  
        
                        Term_sub(Term_inl(m),s) =  3 + 4*m + m*s + m^2 + 2*s                                                                                              
                                                >= 1 + 2*m + m*s + m^2 + s                                                                                                
                                                =  Term_inl(Term_sub(m,s))                                                                                                
        
                        Term_sub(Term_inr(m),s) =  2*m + m*s + m^2 + s                                                                                                    
                                                >= 2*m + m*s + m^2 + s                                                                                                    
                                                =  Term_inr(Term_sub(m,s))                                                                                                
        
                     Term_sub(Term_pair(m,n),s) =  3 + 4*m + 2*m*n + m*s + m^2 + 4*n + n*s + n^2 + 2*s                                                                    
                                                >= 1 + 2*m + m*s + m^2 + 2*n + n*s + n^2 + 2*s                                                                            
                                                =  Term_pair(Term_sub(m,s),Term_sub(n,s))                                                                                 
        
                      Term_sub(Term_sub(m,s),t) =  4*m + 6*m*s + m*s*t + 2*m*s^2 + 2*m*t + 6*m^2 + 6*m^2*s + m^2*s^2 + m^2*t + 4*m^3 + 2*m^3*s + m^4 + 2*s + s*t + s^2 + t
                                                >= 2*m + 2*m*s + m*s*t + m*s^2 + m*t + m^2 + 2*s + s*t + s^2 + t                                                          
                                                =  Term_sub(m,Concat(s,t))                                                                                                
        
         Term_sub(Term_var(x),Cons_sum(xi,k,s)) =  1 + s + xi                                                                                                             
                                                >= s                                                                                                                      
                                                =  Term_sub(Term_var(x),s)                                                                                                
        
        Term_sub(Term_var(x),Cons_usual(y,m,s)) =  1 + m + s                                                                                                              
                                                >= m                                                                                                                      
                                                =  m                                                                                                                      
        
        Term_sub(Term_var(x),Cons_usual(y,m,s)) =  1 + m + s                                                                                                              
                                                >= s                                                                                                                      
                                                =  Term_sub(Term_var(x),s)                                                                                                
        
                     Term_sub(Term_var(x),Id()) =  0                                                                                                                      
                                                >= 0                                                                                                                      
                                                =  Term_var(x)                                                                                                            
        
** Step 1.b:8: NaturalPI WORST_CASE(?,O(n^2))
    + Considered Problem:
        - Strict TRS:
            Concat(Concat(s,t),u) -> Concat(s,Concat(t,u))
            Sum_sub(xi,Cons_sum(psi,k,s)) -> Sum_sub(xi,s)
            Term_sub(Term_sub(m,s),t) -> Term_sub(m,Concat(s,t))
        - Weak TRS:
            Concat(Cons_sum(xi,k,s),t) -> Cons_sum(xi,k,Concat(s,t))
            Concat(Cons_usual(x,m,s),t) -> Cons_usual(x,Term_sub(m,t),Concat(s,t))
            Concat(Id(),s) -> s
            Frozen(m,Sum_constant(Left()),n,s) -> Term_sub(m,s)
            Frozen(m,Sum_constant(Right()),n,s) -> Term_sub(n,s)
            Frozen(m,Sum_term_var(xi),n,s) -> Case(Term_sub(m,s),xi,Term_sub(n,s))
            Sum_sub(xi,Cons_sum(psi,k,s)) -> Sum_constant(k)
            Sum_sub(xi,Cons_usual(y,m,s)) -> Sum_sub(xi,s)
            Sum_sub(xi,Id()) -> Sum_term_var(xi)
            Term_sub(Case(m,xi,n),s) -> Frozen(m,Sum_sub(xi,s),n,s)
            Term_sub(Term_app(m,n),s) -> Term_app(Term_sub(m,s),Term_sub(n,s))
            Term_sub(Term_inl(m),s) -> Term_inl(Term_sub(m,s))
            Term_sub(Term_inr(m),s) -> Term_inr(Term_sub(m,s))
            Term_sub(Term_pair(m,n),s) -> Term_pair(Term_sub(m,s),Term_sub(n,s))
            Term_sub(Term_var(x),Cons_sum(xi,k,s)) -> Term_sub(Term_var(x),s)
            Term_sub(Term_var(x),Cons_usual(y,m,s)) -> m
            Term_sub(Term_var(x),Cons_usual(y,m,s)) -> Term_sub(Term_var(x),s)
            Term_sub(Term_var(x),Id()) -> Term_var(x)
        - Signature:
            {Concat/2,Frozen/4,Sum_sub/2,Term_sub/2} / {Case/3,Cons_sum/3,Cons_usual/3,Id/0,Left/0,Right/0
            ,Sum_constant/1,Sum_term_var/1,Term_app/2,Term_inl/1,Term_inr/1,Term_pair/2,Term_var/1}
        - Obligation:
            innermost runtime complexity wrt. defined symbols {Concat,Frozen,Sum_sub,Term_sub} and constructors {Case
            ,Cons_sum,Cons_usual,Id,Left,Right,Sum_constant,Sum_term_var,Term_app,Term_inl,Term_inr,Term_pair,Term_var}
    + Applied Processor:
        NaturalPI {shape = Mixed 2, restrict = Restrict, uargs = UArgs, urules = URules, selector = Just any strict-rules}
    + Details:
        We apply a polynomial interpretation of kind constructor-based(mixed(2)):
        The following argument positions are considered usable:
          uargs(Case) = {1,3},
          uargs(Concat) = {2},
          uargs(Cons_sum) = {3},
          uargs(Cons_usual) = {2,3},
          uargs(Frozen) = {2},
          uargs(Term_app) = {1,2},
          uargs(Term_inl) = {1},
          uargs(Term_inr) = {1},
          uargs(Term_pair) = {1,2},
          uargs(Term_sub) = {2}
        
        Following symbols are considered usable:
          {Concat,Frozen,Sum_sub,Term_sub}
        TcT has computed the following interpretation:
                  p(Case) = 1 + x1 + x3                                                  
                p(Concat) = 1 + x1 + x1*x2 + x1^2 + x2                                   
              p(Cons_sum) = x3                                                           
            p(Cons_usual) = 1 + x2 + x3                                                  
                p(Frozen) = 1 + x1*x2 + x1*x4 + x1^2 + 2*x2 + x2*x3 + x3*x4 + x3^2 + 2*x4
                    p(Id) = 0                                                            
                  p(Left) = 0                                                            
                 p(Right) = 0                                                            
          p(Sum_constant) = 1                                                            
               p(Sum_sub) = 1                                                            
          p(Sum_term_var) = 1                                                            
              p(Term_app) = 1 + x1 + x2                                                  
              p(Term_inl) = 1 + x1                                                       
              p(Term_inr) = 1 + x1                                                       
             p(Term_pair) = 1 + x1 + x2                                                  
              p(Term_sub) = 1 + x1 + x1*x2 + x1^2 + x2                                   
              p(Term_var) = 1 + x1                                                       
        
        Following rules are strictly oriented:
            Concat(Concat(s,t),u) = 3 + 3*s + 5*s*t + s*t*u + 2*s*t^2 + s*u + 4*s^2 + 4*s^2*t + s^2*t^2 + s^2*u + 2*s^3 + 2*s^3*t + s^4 + 3*t + t*u + t^2 + 2*u
                                  > 2 + 2*s + s*t + s*t*u + s*t^2 + s*u + s^2 + t + t*u + t^2 + u                                                              
                                  = Concat(s,Concat(t,u))                                                                                                      
        
        Term_sub(Term_sub(m,s),t) = 3 + 3*m + 5*m*s + m*s*t + 2*m*s^2 + m*t + 4*m^2 + 4*m^2*s + m^2*s^2 + m^2*t + 2*m^3 + 2*m^3*s + m^4 + 3*s + s*t + s^2 + 2*t
                                  > 2 + 2*m + m*s + m*s*t + m*s^2 + m*t + m^2 + s + s*t + s^2 + t                                                              
                                  = Term_sub(m,Concat(s,t))                                                                                                    
        
        
        Following rules are (at-least) weakly oriented:
                     Concat(Cons_sum(xi,k,s),t) =  1 + s + s*t + s^2 + t                              
                                                >= 1 + s + s*t + s^2 + t                              
                                                =  Cons_sum(xi,k,Concat(s,t))                         
        
                    Concat(Cons_usual(x,m,s),t) =  3 + 3*m + 2*m*s + m*t + m^2 + 3*s + s*t + s^2 + 2*t
                                                >= 3 + m + m*t + m^2 + s + s*t + s^2 + 2*t            
                                                =  Cons_usual(x,Term_sub(m,t),Concat(s,t))            
        
                                 Concat(Id(),s) =  1 + s                                              
                                                >= s                                                  
                                                =  s                                                  
        
             Frozen(m,Sum_constant(Left()),n,s) =  3 + m + m*s + m^2 + n + n*s + n^2 + 2*s            
                                                >= 1 + m + m*s + m^2 + s                              
                                                =  Term_sub(m,s)                                      
        
            Frozen(m,Sum_constant(Right()),n,s) =  3 + m + m*s + m^2 + n + n*s + n^2 + 2*s            
                                                >= 1 + n + n*s + n^2 + s                              
                                                =  Term_sub(n,s)                                      
        
                 Frozen(m,Sum_term_var(xi),n,s) =  3 + m + m*s + m^2 + n + n*s + n^2 + 2*s            
                                                >= 3 + m + m*s + m^2 + n + n*s + n^2 + 2*s            
                                                =  Case(Term_sub(m,s),xi,Term_sub(n,s))               
        
                  Sum_sub(xi,Cons_sum(psi,k,s)) =  1                                                  
                                                >= 1                                                  
                                                =  Sum_constant(k)                                    
        
                  Sum_sub(xi,Cons_sum(psi,k,s)) =  1                                                  
                                                >= 1                                                  
                                                =  Sum_sub(xi,s)                                      
        
                  Sum_sub(xi,Cons_usual(y,m,s)) =  1                                                  
                                                >= 1                                                  
                                                =  Sum_sub(xi,s)                                      
        
                               Sum_sub(xi,Id()) =  1                                                  
                                                >= 1                                                  
                                                =  Sum_term_var(xi)                                   
        
                       Term_sub(Case(m,xi,n),s) =  3 + 3*m + 2*m*n + m*s + m^2 + 3*n + n*s + n^2 + 2*s
                                                >= 3 + m + m*s + m^2 + n + n*s + n^2 + 2*s            
                                                =  Frozen(m,Sum_sub(xi,s),n,s)                        
        
                      Term_sub(Term_app(m,n),s) =  3 + 3*m + 2*m*n + m*s + m^2 + 3*n + n*s + n^2 + 2*s
                                                >= 3 + m + m*s + m^2 + n + n*s + n^2 + 2*s            
                                                =  Term_app(Term_sub(m,s),Term_sub(n,s))              
        
                        Term_sub(Term_inl(m),s) =  3 + 3*m + m*s + m^2 + 2*s                          
                                                >= 2 + m + m*s + m^2 + s                              
                                                =  Term_inl(Term_sub(m,s))                            
        
                        Term_sub(Term_inr(m),s) =  3 + 3*m + m*s + m^2 + 2*s                          
                                                >= 2 + m + m*s + m^2 + s                              
                                                =  Term_inr(Term_sub(m,s))                            
        
                     Term_sub(Term_pair(m,n),s) =  3 + 3*m + 2*m*n + m*s + m^2 + 3*n + n*s + n^2 + 2*s
                                                >= 3 + m + m*s + m^2 + n + n*s + n^2 + 2*s            
                                                =  Term_pair(Term_sub(m,s),Term_sub(n,s))             
        
         Term_sub(Term_var(x),Cons_sum(xi,k,s)) =  3 + 2*s + s*x + 3*x + x^2                          
                                                >= 3 + 2*s + s*x + 3*x + x^2                          
                                                =  Term_sub(Term_var(x),s)                            
        
        Term_sub(Term_var(x),Cons_usual(y,m,s)) =  5 + 2*m + m*x + 2*s + s*x + 4*x + x^2              
                                                >= m                                                  
                                                =  m                                                  
        
        Term_sub(Term_var(x),Cons_usual(y,m,s)) =  5 + 2*m + m*x + 2*s + s*x + 4*x + x^2              
                                                >= 3 + 2*s + s*x + 3*x + x^2                          
                                                =  Term_sub(Term_var(x),s)                            
        
                     Term_sub(Term_var(x),Id()) =  3 + 3*x + x^2                                      
                                                >= 1 + x                                              
                                                =  Term_var(x)                                        
        
** Step 1.b:9: NaturalPI WORST_CASE(?,O(n^2))
    + Considered Problem:
        - Strict TRS:
            Sum_sub(xi,Cons_sum(psi,k,s)) -> Sum_sub(xi,s)
        - Weak TRS:
            Concat(Concat(s,t),u) -> Concat(s,Concat(t,u))
            Concat(Cons_sum(xi,k,s),t) -> Cons_sum(xi,k,Concat(s,t))
            Concat(Cons_usual(x,m,s),t) -> Cons_usual(x,Term_sub(m,t),Concat(s,t))
            Concat(Id(),s) -> s
            Frozen(m,Sum_constant(Left()),n,s) -> Term_sub(m,s)
            Frozen(m,Sum_constant(Right()),n,s) -> Term_sub(n,s)
            Frozen(m,Sum_term_var(xi),n,s) -> Case(Term_sub(m,s),xi,Term_sub(n,s))
            Sum_sub(xi,Cons_sum(psi,k,s)) -> Sum_constant(k)
            Sum_sub(xi,Cons_usual(y,m,s)) -> Sum_sub(xi,s)
            Sum_sub(xi,Id()) -> Sum_term_var(xi)
            Term_sub(Case(m,xi,n),s) -> Frozen(m,Sum_sub(xi,s),n,s)
            Term_sub(Term_app(m,n),s) -> Term_app(Term_sub(m,s),Term_sub(n,s))
            Term_sub(Term_inl(m),s) -> Term_inl(Term_sub(m,s))
            Term_sub(Term_inr(m),s) -> Term_inr(Term_sub(m,s))
            Term_sub(Term_pair(m,n),s) -> Term_pair(Term_sub(m,s),Term_sub(n,s))
            Term_sub(Term_sub(m,s),t) -> Term_sub(m,Concat(s,t))
            Term_sub(Term_var(x),Cons_sum(xi,k,s)) -> Term_sub(Term_var(x),s)
            Term_sub(Term_var(x),Cons_usual(y,m,s)) -> m
            Term_sub(Term_var(x),Cons_usual(y,m,s)) -> Term_sub(Term_var(x),s)
            Term_sub(Term_var(x),Id()) -> Term_var(x)
        - Signature:
            {Concat/2,Frozen/4,Sum_sub/2,Term_sub/2} / {Case/3,Cons_sum/3,Cons_usual/3,Id/0,Left/0,Right/0
            ,Sum_constant/1,Sum_term_var/1,Term_app/2,Term_inl/1,Term_inr/1,Term_pair/2,Term_var/1}
        - Obligation:
            innermost runtime complexity wrt. defined symbols {Concat,Frozen,Sum_sub,Term_sub} and constructors {Case
            ,Cons_sum,Cons_usual,Id,Left,Right,Sum_constant,Sum_term_var,Term_app,Term_inl,Term_inr,Term_pair,Term_var}
    + Applied Processor:
        NaturalPI {shape = Mixed 2, restrict = Restrict, uargs = UArgs, urules = URules, selector = Just any strict-rules}
    + Details:
        We apply a polynomial interpretation of kind constructor-based(mixed(2)):
        The following argument positions are considered usable:
          uargs(Case) = {1,3},
          uargs(Concat) = {2},
          uargs(Cons_sum) = {3},
          uargs(Cons_usual) = {2,3},
          uargs(Frozen) = {2},
          uargs(Term_app) = {1,2},
          uargs(Term_inl) = {1},
          uargs(Term_inr) = {1},
          uargs(Term_pair) = {1,2},
          uargs(Term_sub) = {2}
        
        Following symbols are considered usable:
          {Concat,Frozen,Sum_sub,Term_sub}
        TcT has computed the following interpretation:
                  p(Case) = 1 + x1 + x2 + x3                                           
                p(Concat) = x1 + 2*x1*x2 + x1^2 + x2                                   
              p(Cons_sum) = 1 + x2 + x3                                                
            p(Cons_usual) = 1 + x2 + x3                                                
                p(Frozen) = 2 + x1 + 2*x1*x4 + x1^2 + x2 + 2*x3 + 2*x3*x4 + x3^2 + 2*x4
                    p(Id) = 1                                                          
                  p(Left) = 1                                                          
                 p(Right) = 1                                                          
          p(Sum_constant) = x1                                                         
               p(Sum_sub) = 2*x1 + x2                                                  
          p(Sum_term_var) = x1                                                         
              p(Term_app) = 1 + x1 + x2                                                
              p(Term_inl) = x1                                                         
              p(Term_inr) = x1                                                         
             p(Term_pair) = 1 + x1 + x2                                                
              p(Term_sub) = x1 + 2*x1*x2 + x1^2 + x2                                   
              p(Term_var) = 0                                                          
        
        Following rules are strictly oriented:
        Sum_sub(xi,Cons_sum(psi,k,s)) = 1 + k + s + 2*xi
                                      > s + 2*xi        
                                      = Sum_sub(xi,s)   
        
        
        Following rules are (at-least) weakly oriented:
                          Concat(Concat(s,t),u) =  s + 4*s*t + 4*s*t*u + 4*s*t^2 + 2*s*u + 2*s^2 + 6*s^2*t + 4*s^2*t^2 + 2*s^2*u + 2*s^3 + 4*s^3*t + s^4 + t + 2*t*u + t^2 + u
                                                >= s + 2*s*t + 4*s*t*u + 2*s*t^2 + 2*s*u + s^2 + t + 2*t*u + t^2 + u                                                          
                                                =  Concat(s,Concat(t,u))                                                                                                      
        
                     Concat(Cons_sum(xi,k,s),t) =  2 + 3*k + 2*k*s + 2*k*t + k^2 + 3*s + 2*s*t + s^2 + 3*t                                                                    
                                                >= 1 + k + s + 2*s*t + s^2 + t                                                                                                
                                                =  Cons_sum(xi,k,Concat(s,t))                                                                                                 
        
                    Concat(Cons_usual(x,m,s),t) =  2 + 3*m + 2*m*s + 2*m*t + m^2 + 3*s + 2*s*t + s^2 + 3*t                                                                    
                                                >= 1 + m + 2*m*t + m^2 + s + 2*s*t + s^2 + 2*t                                                                                
                                                =  Cons_usual(x,Term_sub(m,t),Concat(s,t))                                                                                    
        
                                 Concat(Id(),s) =  2 + 3*s                                                                                                                    
                                                >= s                                                                                                                          
                                                =  s                                                                                                                          
        
             Frozen(m,Sum_constant(Left()),n,s) =  3 + m + 2*m*s + m^2 + 2*n + 2*n*s + n^2 + 2*s                                                                              
                                                >= m + 2*m*s + m^2 + s                                                                                                        
                                                =  Term_sub(m,s)                                                                                                              
        
            Frozen(m,Sum_constant(Right()),n,s) =  3 + m + 2*m*s + m^2 + 2*n + 2*n*s + n^2 + 2*s                                                                              
                                                >= n + 2*n*s + n^2 + s                                                                                                        
                                                =  Term_sub(n,s)                                                                                                              
        
                 Frozen(m,Sum_term_var(xi),n,s) =  2 + m + 2*m*s + m^2 + 2*n + 2*n*s + n^2 + 2*s + xi                                                                         
                                                >= 1 + m + 2*m*s + m^2 + n + 2*n*s + n^2 + 2*s + xi                                                                           
                                                =  Case(Term_sub(m,s),xi,Term_sub(n,s))                                                                                       
        
                  Sum_sub(xi,Cons_sum(psi,k,s)) =  1 + k + s + 2*xi                                                                                                           
                                                >= k                                                                                                                          
                                                =  Sum_constant(k)                                                                                                            
        
                  Sum_sub(xi,Cons_usual(y,m,s)) =  1 + m + s + 2*xi                                                                                                           
                                                >= s + 2*xi                                                                                                                   
                                                =  Sum_sub(xi,s)                                                                                                              
        
                               Sum_sub(xi,Id()) =  1 + 2*xi                                                                                                                   
                                                >= xi                                                                                                                         
                                                =  Sum_term_var(xi)                                                                                                           
        
                       Term_sub(Case(m,xi,n),s) =  2 + 3*m + 2*m*n + 2*m*s + 2*m*xi + m^2 + 3*n + 2*n*s + 2*n*xi + n^2 + 3*s + 2*s*xi + 3*xi + xi^2                           
                                                >= 2 + m + 2*m*s + m^2 + 2*n + 2*n*s + n^2 + 3*s + 2*xi                                                                       
                                                =  Frozen(m,Sum_sub(xi,s),n,s)                                                                                                
        
                      Term_sub(Term_app(m,n),s) =  2 + 3*m + 2*m*n + 2*m*s + m^2 + 3*n + 2*n*s + n^2 + 3*s                                                                    
                                                >= 1 + m + 2*m*s + m^2 + n + 2*n*s + n^2 + 2*s                                                                                
                                                =  Term_app(Term_sub(m,s),Term_sub(n,s))                                                                                      
        
                        Term_sub(Term_inl(m),s) =  m + 2*m*s + m^2 + s                                                                                                        
                                                >= m + 2*m*s + m^2 + s                                                                                                        
                                                =  Term_inl(Term_sub(m,s))                                                                                                    
        
                        Term_sub(Term_inr(m),s) =  m + 2*m*s + m^2 + s                                                                                                        
                                                >= m + 2*m*s + m^2 + s                                                                                                        
                                                =  Term_inr(Term_sub(m,s))                                                                                                    
        
                     Term_sub(Term_pair(m,n),s) =  2 + 3*m + 2*m*n + 2*m*s + m^2 + 3*n + 2*n*s + n^2 + 3*s                                                                    
                                                >= 1 + m + 2*m*s + m^2 + n + 2*n*s + n^2 + 2*s                                                                                
                                                =  Term_pair(Term_sub(m,s),Term_sub(n,s))                                                                                     
        
                      Term_sub(Term_sub(m,s),t) =  m + 4*m*s + 4*m*s*t + 4*m*s^2 + 2*m*t + 2*m^2 + 6*m^2*s + 4*m^2*s^2 + 2*m^2*t + 2*m^3 + 4*m^3*s + m^4 + s + 2*s*t + s^2 + t
                                                >= m + 2*m*s + 4*m*s*t + 2*m*s^2 + 2*m*t + m^2 + s + 2*s*t + s^2 + t                                                          
                                                =  Term_sub(m,Concat(s,t))                                                                                                    
        
         Term_sub(Term_var(x),Cons_sum(xi,k,s)) =  1 + k + s                                                                                                                  
                                                >= s                                                                                                                          
                                                =  Term_sub(Term_var(x),s)                                                                                                    
        
        Term_sub(Term_var(x),Cons_usual(y,m,s)) =  1 + m + s                                                                                                                  
                                                >= m                                                                                                                          
                                                =  m                                                                                                                          
        
        Term_sub(Term_var(x),Cons_usual(y,m,s)) =  1 + m + s                                                                                                                  
                                                >= s                                                                                                                          
                                                =  Term_sub(Term_var(x),s)                                                                                                    
        
                     Term_sub(Term_var(x),Id()) =  1                                                                                                                          
                                                >= 0                                                                                                                          
                                                =  Term_var(x)                                                                                                                
        
** Step 1.b:10: EmptyProcessor WORST_CASE(?,O(1))
    + Considered Problem:
        - Weak TRS:
            Concat(Concat(s,t),u) -> Concat(s,Concat(t,u))
            Concat(Cons_sum(xi,k,s),t) -> Cons_sum(xi,k,Concat(s,t))
            Concat(Cons_usual(x,m,s),t) -> Cons_usual(x,Term_sub(m,t),Concat(s,t))
            Concat(Id(),s) -> s
            Frozen(m,Sum_constant(Left()),n,s) -> Term_sub(m,s)
            Frozen(m,Sum_constant(Right()),n,s) -> Term_sub(n,s)
            Frozen(m,Sum_term_var(xi),n,s) -> Case(Term_sub(m,s),xi,Term_sub(n,s))
            Sum_sub(xi,Cons_sum(psi,k,s)) -> Sum_constant(k)
            Sum_sub(xi,Cons_sum(psi,k,s)) -> Sum_sub(xi,s)
            Sum_sub(xi,Cons_usual(y,m,s)) -> Sum_sub(xi,s)
            Sum_sub(xi,Id()) -> Sum_term_var(xi)
            Term_sub(Case(m,xi,n),s) -> Frozen(m,Sum_sub(xi,s),n,s)
            Term_sub(Term_app(m,n),s) -> Term_app(Term_sub(m,s),Term_sub(n,s))
            Term_sub(Term_inl(m),s) -> Term_inl(Term_sub(m,s))
            Term_sub(Term_inr(m),s) -> Term_inr(Term_sub(m,s))
            Term_sub(Term_pair(m,n),s) -> Term_pair(Term_sub(m,s),Term_sub(n,s))
            Term_sub(Term_sub(m,s),t) -> Term_sub(m,Concat(s,t))
            Term_sub(Term_var(x),Cons_sum(xi,k,s)) -> Term_sub(Term_var(x),s)
            Term_sub(Term_var(x),Cons_usual(y,m,s)) -> m
            Term_sub(Term_var(x),Cons_usual(y,m,s)) -> Term_sub(Term_var(x),s)
            Term_sub(Term_var(x),Id()) -> Term_var(x)
        - Signature:
            {Concat/2,Frozen/4,Sum_sub/2,Term_sub/2} / {Case/3,Cons_sum/3,Cons_usual/3,Id/0,Left/0,Right/0
            ,Sum_constant/1,Sum_term_var/1,Term_app/2,Term_inl/1,Term_inr/1,Term_pair/2,Term_var/1}
        - Obligation:
            innermost runtime complexity wrt. defined symbols {Concat,Frozen,Sum_sub,Term_sub} and constructors {Case
            ,Cons_sum,Cons_usual,Id,Left,Right,Sum_constant,Sum_term_var,Term_app,Term_inl,Term_inr,Term_pair,Term_var}
    + Applied Processor:
        EmptyProcessor
    + Details:
        The problem is already closed. The intended complexity is O(1).

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