YES(O(1),O(n^2))
877.91/297.40	YES(O(1),O(n^2))
877.91/297.40	
877.91/297.40	We are left with following problem, upon which TcT provides the
877.91/297.40	certificate YES(O(1),O(n^2)).
877.91/297.40	
877.91/297.40	Strict Trs:
877.91/297.40	  { Term_sub(Term_sub(m, s), t) -> Term_sub(m, Concat(s, t))
877.91/297.40	  , Term_sub(Case(m, xi, n), s) -> Frozen(m, Sum_sub(xi, s), n, s)
877.91/297.40	  , Term_sub(Term_app(m, n), s) ->
877.91/297.40	    Term_app(Term_sub(m, s), Term_sub(n, s))
877.91/297.40	  , Term_sub(Term_pair(m, n), s) ->
877.91/297.40	    Term_pair(Term_sub(m, s), Term_sub(n, s))
877.91/297.40	  , Term_sub(Term_inl(m), s) -> Term_inl(Term_sub(m, s))
877.91/297.40	  , Term_sub(Term_inr(m), s) -> Term_inr(Term_sub(m, s))
877.91/297.40	  , Term_sub(Term_var(x), Id()) -> Term_var(x)
877.91/297.40	  , Term_sub(Term_var(x), Cons_usual(y, m, s)) -> m
877.91/297.40	  , Term_sub(Term_var(x), Cons_usual(y, m, s)) ->
877.91/297.40	    Term_sub(Term_var(x), s)
877.91/297.40	  , Term_sub(Term_var(x), Cons_sum(xi, k, s)) ->
877.91/297.40	    Term_sub(Term_var(x), s)
877.91/297.40	  , Frozen(m, Sum_constant(Left()), n, s) -> Term_sub(m, s)
877.91/297.40	  , Frozen(m, Sum_constant(Right()), n, s) -> Term_sub(n, s)
877.91/297.40	  , Frozen(m, Sum_term_var(xi), n, s) ->
877.91/297.40	    Case(Term_sub(m, s), xi, Term_sub(n, s))
877.91/297.40	  , Sum_sub(xi, Id()) -> Sum_term_var(xi)
877.91/297.40	  , Sum_sub(xi, Cons_usual(y, m, s)) -> Sum_sub(xi, s)
877.91/297.40	  , Sum_sub(xi, Cons_sum(psi, k, s)) -> Sum_sub(xi, s)
877.91/297.40	  , Sum_sub(xi, Cons_sum(psi, k, s)) -> Sum_constant(k)
877.91/297.40	  , Concat(Id(), s) -> s
877.91/297.40	  , Concat(Cons_usual(x, m, s), t) ->
877.91/297.40	    Cons_usual(x, Term_sub(m, t), Concat(s, t))
877.91/297.40	  , Concat(Cons_sum(xi, k, s), t) -> Cons_sum(xi, k, Concat(s, t))
877.91/297.40	  , Concat(Concat(s, t), u) -> Concat(s, Concat(t, u)) }
877.91/297.40	Obligation:
877.91/297.40	  runtime complexity
877.91/297.40	Answer:
877.91/297.40	  YES(O(1),O(n^2))
877.91/297.40	
877.91/297.40	We use the processor 'polynomial interpretation' to orient
877.91/297.40	following rules strictly.
877.91/297.40	
877.91/297.40	Trs:
877.91/297.40	  { Term_sub(Case(m, xi, n), s) -> Frozen(m, Sum_sub(xi, s), n, s)
877.91/297.40	  , Term_sub(Term_app(m, n), s) ->
877.91/297.40	    Term_app(Term_sub(m, s), Term_sub(n, s))
877.91/297.40	  , Term_sub(Term_var(x), Id()) -> Term_var(x)
877.91/297.40	  , Term_sub(Term_var(x), Cons_usual(y, m, s)) -> m
877.91/297.40	  , Term_sub(Term_var(x), Cons_usual(y, m, s)) ->
877.91/297.40	    Term_sub(Term_var(x), s)
877.91/297.40	  , Term_sub(Term_var(x), Cons_sum(xi, k, s)) ->
877.91/297.40	    Term_sub(Term_var(x), s)
877.91/297.40	  , Frozen(m, Sum_constant(Left()), n, s) -> Term_sub(m, s)
877.91/297.40	  , Frozen(m, Sum_constant(Right()), n, s) -> Term_sub(n, s)
877.91/297.40	  , Sum_sub(xi, Cons_usual(y, m, s)) -> Sum_sub(xi, s)
877.91/297.40	  , Sum_sub(xi, Cons_sum(psi, k, s)) -> Sum_sub(xi, s)
877.91/297.40	  , Sum_sub(xi, Cons_sum(psi, k, s)) -> Sum_constant(k)
877.91/297.40	  , Concat(Id(), s) -> s
877.91/297.40	  , Concat(Cons_sum(xi, k, s), t) -> Cons_sum(xi, k, Concat(s, t)) }
877.91/297.40	
877.91/297.40	The induced complexity on above rules (modulo remaining rules) is
877.91/297.40	YES(?,O(n^2)) . These rules are moved into the corresponding weak
877.91/297.40	component(s).
877.91/297.40	
877.91/297.40	Sub-proof:
877.91/297.40	----------
877.91/297.40	  We consider the following typing:
877.91/297.40	  
877.91/297.40	    Term_sub :: (g,b) -> g
877.91/297.40	    Case :: (g,c,g) -> g
877.91/297.40	    Frozen :: (g,a,g,b) -> g
877.91/297.40	    Sum_sub :: (c,b) -> a
877.91/297.40	    Sum_constant :: d -> a
877.91/297.40	    Left :: d
877.91/297.40	    Right :: d
877.91/297.40	    Sum_term_var :: c -> a
877.91/297.40	    Term_app :: (g,g) -> g
877.91/297.40	    Term_pair :: (g,g) -> g
877.91/297.40	    Term_inl :: g -> g
877.91/297.40	    Term_inr :: g -> g
877.91/297.40	    Term_var :: e -> g
877.91/297.40	    Id :: b
877.91/297.40	    Cons_usual :: (f,g,b) -> b
877.91/297.40	    Cons_sum :: (h,d,b) -> b
877.91/297.40	    Concat :: (b,b) -> b
877.91/297.40	  
877.91/297.40	  The following argument positions are considered usable:
877.91/297.40	  
877.91/297.40	    Uargs(Term_sub) = {2}, Uargs(Case) = {1, 3},
877.91/297.40	    Uargs(Frozen) = {2, 4}, Uargs(Sum_sub) = {2},
877.91/297.40	    Uargs(Term_app) = {1, 2}, Uargs(Term_pair) = {1, 2},
877.91/297.40	    Uargs(Term_inl) = {1}, Uargs(Term_inr) = {1},
877.91/297.40	    Uargs(Cons_usual) = {2, 3}, Uargs(Cons_sum) = {3},
877.91/297.40	    Uargs(Concat) = {2}
877.91/297.40	  
877.91/297.40	  TcT has computed the following constructor-restricted
877.91/297.40	  typedpolynomial interpretation.
877.91/297.40	  
877.91/297.40	        [Term_sub](x1, x2) = 1 + 2*x1 + x1*x2 + x2                      
877.91/297.40	                                                                        
877.91/297.40	        [Case](x1, x2, x3) = 2 + x1 + x3                                
877.91/297.40	                                                                        
877.91/297.40	  [Frozen](x1, x2, x3, x4) = 2 + 2*x1 + x1*x4 + x2 + 2*x3 + x3*x4 + 2*x4
877.91/297.40	                                                                        
877.91/297.40	         [Sum_sub](x1, x2) = 2 + x2                                     
877.91/297.40	                                                                        
877.91/297.40	        [Sum_constant](x1) = 0                                          
877.91/297.40	                                                                        
877.91/297.40	                  [Left]() = 0                                          
877.91/297.40	                                                                        
877.91/297.40	                 [Right]() = 0                                          
877.91/297.40	                                                                        
877.91/297.40	        [Sum_term_var](x1) = 2                                          
877.91/297.40	                                                                        
877.91/297.40	        [Term_app](x1, x2) = 2 + x1 + x2                                
877.91/297.40	                                                                        
877.91/297.40	       [Term_pair](x1, x2) = 1 + x1 + x2                                
877.91/297.40	                                                                        
877.91/297.40	            [Term_inl](x1) = x1                                         
877.91/297.40	                                                                        
877.91/297.40	            [Term_inr](x1) = x1                                         
877.91/297.40	                                                                        
877.91/297.40	            [Term_var](x1) = 0                                          
877.91/297.40	                                                                        
877.91/297.40	                    [Id]() = 0                                          
877.91/297.40	                                                                        
877.91/297.40	  [Cons_usual](x1, x2, x3) = 1 + x2 + x3                                
877.91/297.40	                                                                        
877.91/297.40	    [Cons_sum](x1, x2, x3) = 2 + x3                                     
877.91/297.40	                                                                        
877.91/297.40	          [Concat](x1, x2) = 2 + 2*x1 + x1*x2 + 2*x2                    
877.91/297.40	                                                                        
877.91/297.40	  
877.91/297.40	  This order satisfies the following ordering constraints.
877.91/297.40	  
877.91/297.40	                   [Term_sub(Term_sub(m, s), t)] =  3 + 4*m + 2*m*s + 2*s + 2*t + 2*m*t + m*s*t + s*t  
877.91/297.40	                                                 >= 3 + 4*m + 2*m*s + m*s*t + 2*m*t + 2*s + s*t + 2*t  
877.91/297.40	                                                 =  [Term_sub(m, Concat(s, t))]                        
877.91/297.40	                                                                                                       
877.91/297.40	                   [Term_sub(Case(m, xi, n), s)] =  5 + 2*m + 2*n + 3*s + m*s + n*s                    
877.91/297.40	                                                 >  4 + 2*m + m*s + 3*s + 2*n + n*s                    
877.91/297.40	                                                 =  [Frozen(m, Sum_sub(xi, s), n, s)]                  
877.91/297.40	                                                                                                       
877.91/297.40	                   [Term_sub(Term_app(m, n), s)] =  5 + 2*m + 2*n + 3*s + m*s + n*s                    
877.91/297.40	                                                 >  4 + 2*m + m*s + 2*s + 2*n + n*s                    
877.91/297.40	                                                 =  [Term_app(Term_sub(m, s), Term_sub(n, s))]         
877.91/297.40	                                                                                                       
877.91/297.40	                  [Term_sub(Term_pair(m, n), s)] =  3 + 2*m + 2*n + 2*s + m*s + n*s                    
877.91/297.40	                                                 >= 3 + 2*m + m*s + 2*s + 2*n + n*s                    
877.91/297.40	                                                 =  [Term_pair(Term_sub(m, s), Term_sub(n, s))]        
877.91/297.40	                                                                                                       
877.91/297.40	                      [Term_sub(Term_inl(m), s)] =  1 + 2*m + m*s + s                                  
877.91/297.40	                                                 >= 1 + 2*m + m*s + s                                  
877.91/297.40	                                                 =  [Term_inl(Term_sub(m, s))]                         
877.91/297.40	                                                                                                       
877.91/297.40	                      [Term_sub(Term_inr(m), s)] =  1 + 2*m + m*s + s                                  
877.91/297.40	                                                 >= 1 + 2*m + m*s + s                                  
877.91/297.40	                                                 =  [Term_inr(Term_sub(m, s))]                         
877.91/297.40	                                                                                                       
877.91/297.40	                   [Term_sub(Term_var(x), Id())] =  1                                                  
877.91/297.40	                                                 >                                                     
877.91/297.40	                                                 =  [Term_var(x)]                                      
877.91/297.40	                                                                                                       
877.91/297.40	    [Term_sub(Term_var(x), Cons_usual(y, m, s))] =  2 + m + s                                          
877.91/297.40	                                                 >  m                                                  
877.91/297.40	                                                 =  [m]                                                
877.91/297.40	                                                                                                       
877.91/297.40	    [Term_sub(Term_var(x), Cons_usual(y, m, s))] =  2 + m + s                                          
877.91/297.40	                                                 >  1 + s                                              
877.91/297.40	                                                 =  [Term_sub(Term_var(x), s)]                         
877.91/297.40	                                                                                                       
877.91/297.40	     [Term_sub(Term_var(x), Cons_sum(xi, k, s))] =  3 + s                                              
877.91/297.40	                                                 >  1 + s                                              
877.91/297.40	                                                 =  [Term_sub(Term_var(x), s)]                         
877.91/297.40	                                                                                                       
877.91/297.40	         [Frozen(m, Sum_constant(Left()), n, s)] =  2 + 2*m + m*s + 2*n + n*s + 2*s                    
877.91/297.40	                                                 >  1 + 2*m + m*s + s                                  
877.91/297.40	                                                 =  [Term_sub(m, s)]                                   
877.91/297.40	                                                                                                       
877.91/297.40	        [Frozen(m, Sum_constant(Right()), n, s)] =  2 + 2*m + m*s + 2*n + n*s + 2*s                    
877.91/297.40	                                                 >  1 + 2*n + n*s + s                                  
877.91/297.40	                                                 =  [Term_sub(n, s)]                                   
877.91/297.40	                                                                                                       
877.91/297.40	             [Frozen(m, Sum_term_var(xi), n, s)] =  4 + 2*m + m*s + 2*n + n*s + 2*s                    
877.91/297.40	                                                 >= 4 + 2*m + m*s + 2*s + 2*n + n*s                    
877.91/297.40	                                                 =  [Case(Term_sub(m, s), xi, Term_sub(n, s))]         
877.91/297.40	                                                                                                       
877.91/297.40	                             [Sum_sub(xi, Id())] =  2                                                  
877.91/297.40	                                                 >= 2                                                  
877.91/297.40	                                                 =  [Sum_term_var(xi)]                                 
877.91/297.40	                                                                                                       
877.91/297.40	              [Sum_sub(xi, Cons_usual(y, m, s))] =  3 + m + s                                          
877.91/297.40	                                                 >  2 + s                                              
877.91/297.40	                                                 =  [Sum_sub(xi, s)]                                   
877.91/297.40	                                                                                                       
877.91/297.40	              [Sum_sub(xi, Cons_sum(psi, k, s))] =  4 + s                                              
877.91/297.40	                                                 >  2 + s                                              
877.91/297.40	                                                 =  [Sum_sub(xi, s)]                                   
877.91/297.40	                                                                                                       
877.91/297.40	              [Sum_sub(xi, Cons_sum(psi, k, s))] =  4 + s                                              
877.91/297.40	                                                 >                                                     
877.91/297.40	                                                 =  [Sum_constant(k)]                                  
877.91/297.40	                                                                                                       
877.91/297.40	                               [Concat(Id(), s)] =  2 + 2*s                                            
877.91/297.40	                                                 >  s                                                  
877.91/297.40	                                                 =  [s]                                                
877.91/297.40	                                                                                                       
877.91/297.40	                [Concat(Cons_usual(x, m, s), t)] =  4 + 2*m + 2*s + 3*t + m*t + s*t                    
877.91/297.40	                                                 >= 4 + 2*m + m*t + 3*t + 2*s + s*t                    
877.91/297.40	                                                 =  [Cons_usual(x, Term_sub(m, t), Concat(s, t))]      
877.91/297.40	                                                                                                       
877.91/297.40	                 [Concat(Cons_sum(xi, k, s), t)] =  6 + 2*s + 4*t + s*t                                
877.91/297.40	                                                 >  4 + 2*s + s*t + 2*t                                
877.91/297.40	                                                 =  [Cons_sum(xi, k, Concat(s, t))]                    
877.91/297.40	                                                                                                       
877.91/297.40	                       [Concat(Concat(s, t), u)] =  6 + 4*s + 2*s*t + 4*t + 4*u + 2*s*u + s*t*u + 2*t*u
877.91/297.40	                                                 >= 6 + 4*s + 2*s*t + s*t*u + 2*s*u + 4*t + 2*t*u + 4*u
877.91/297.40	                                                 =  [Concat(s, Concat(t, u))]                          
877.91/297.40	                                                                                                       
877.91/297.40	
877.91/297.40	We return to the main proof.
877.91/297.40	
877.91/297.40	We are left with following problem, upon which TcT provides the
877.91/297.40	certificate YES(O(1),O(n^2)).
877.91/297.40	
877.91/297.40	Strict Trs:
877.91/297.40	  { Term_sub(Term_sub(m, s), t) -> Term_sub(m, Concat(s, t))
877.91/297.40	  , Term_sub(Term_pair(m, n), s) ->
877.91/297.40	    Term_pair(Term_sub(m, s), Term_sub(n, s))
877.91/297.40	  , Term_sub(Term_inl(m), s) -> Term_inl(Term_sub(m, s))
877.91/297.40	  , Term_sub(Term_inr(m), s) -> Term_inr(Term_sub(m, s))
877.91/297.40	  , Frozen(m, Sum_term_var(xi), n, s) ->
877.91/297.40	    Case(Term_sub(m, s), xi, Term_sub(n, s))
877.91/297.40	  , Sum_sub(xi, Id()) -> Sum_term_var(xi)
877.91/297.40	  , Concat(Cons_usual(x, m, s), t) ->
877.91/297.40	    Cons_usual(x, Term_sub(m, t), Concat(s, t))
877.91/297.40	  , Concat(Concat(s, t), u) -> Concat(s, Concat(t, u)) }
877.91/297.40	Weak Trs:
877.91/297.40	  { Term_sub(Case(m, xi, n), s) -> Frozen(m, Sum_sub(xi, s), n, s)
877.91/297.40	  , Term_sub(Term_app(m, n), s) ->
877.91/297.40	    Term_app(Term_sub(m, s), Term_sub(n, s))
877.91/297.40	  , Term_sub(Term_var(x), Id()) -> Term_var(x)
877.91/297.40	  , Term_sub(Term_var(x), Cons_usual(y, m, s)) -> m
877.91/297.40	  , Term_sub(Term_var(x), Cons_usual(y, m, s)) ->
877.91/297.40	    Term_sub(Term_var(x), s)
877.91/297.40	  , Term_sub(Term_var(x), Cons_sum(xi, k, s)) ->
877.91/297.40	    Term_sub(Term_var(x), s)
877.91/297.40	  , Frozen(m, Sum_constant(Left()), n, s) -> Term_sub(m, s)
877.91/297.40	  , Frozen(m, Sum_constant(Right()), n, s) -> Term_sub(n, s)
877.91/297.40	  , Sum_sub(xi, Cons_usual(y, m, s)) -> Sum_sub(xi, s)
877.91/297.40	  , Sum_sub(xi, Cons_sum(psi, k, s)) -> Sum_sub(xi, s)
877.91/297.40	  , Sum_sub(xi, Cons_sum(psi, k, s)) -> Sum_constant(k)
877.91/297.40	  , Concat(Id(), s) -> s
877.91/297.40	  , Concat(Cons_sum(xi, k, s), t) -> Cons_sum(xi, k, Concat(s, t)) }
877.91/297.40	Obligation:
877.91/297.40	  runtime complexity
877.91/297.40	Answer:
877.91/297.40	  YES(O(1),O(n^2))
877.91/297.40	
877.91/297.40	We use the processor 'polynomial interpretation' to orient
877.91/297.40	following rules strictly.
877.91/297.40	
877.91/297.40	Trs:
877.91/297.40	  { Term_sub(Term_pair(m, n), s) ->
877.91/297.40	    Term_pair(Term_sub(m, s), Term_sub(n, s))
877.91/297.40	  , Term_sub(Term_inr(m), s) -> Term_inr(Term_sub(m, s)) }
877.91/297.40	
877.91/297.40	The induced complexity on above rules (modulo remaining rules) is
877.91/297.40	YES(?,O(n^2)) . These rules are moved into the corresponding weak
877.91/297.40	component(s).
877.91/297.40	
877.91/297.40	Sub-proof:
877.91/297.40	----------
877.91/297.40	  We consider the following typing:
877.91/297.40	  
877.91/297.40	    Term_sub :: (g,b) -> g
877.91/297.40	    Case :: (g,c,g) -> g
877.91/297.40	    Frozen :: (g,a,g,b) -> g
877.91/297.40	    Sum_sub :: (c,b) -> a
877.91/297.40	    Sum_constant :: d -> a
877.91/297.40	    Left :: d
877.91/297.40	    Right :: d
877.91/297.40	    Sum_term_var :: c -> a
877.91/297.40	    Term_app :: (g,g) -> g
877.91/297.40	    Term_pair :: (g,g) -> g
877.91/297.40	    Term_inl :: g -> g
877.91/297.40	    Term_inr :: g -> g
877.91/297.40	    Term_var :: e -> g
877.91/297.40	    Id :: b
877.91/297.40	    Cons_usual :: (f,g,b) -> b
877.91/297.40	    Cons_sum :: (h,d,b) -> b
877.91/297.40	    Concat :: (b,b) -> b
877.91/297.40	  
877.91/297.40	  The following argument positions are considered usable:
877.91/297.40	  
877.91/297.40	    Uargs(Term_sub) = {2}, Uargs(Case) = {1, 3},
877.91/297.40	    Uargs(Frozen) = {2, 4}, Uargs(Sum_sub) = {2},
877.91/297.40	    Uargs(Term_app) = {1, 2}, Uargs(Term_pair) = {1, 2},
877.91/297.40	    Uargs(Term_inl) = {1}, Uargs(Term_inr) = {1},
877.91/297.40	    Uargs(Cons_usual) = {2, 3}, Uargs(Cons_sum) = {3},
877.91/297.40	    Uargs(Concat) = {2}
877.91/297.40	  
877.91/297.40	  TcT has computed the following constructor-restricted
877.91/297.40	  typedpolynomial interpretation.
877.91/297.40	  
877.91/297.40	        [Term_sub](x1, x2) = 1 + 2*x1 + x1*x2 + x2                      
877.91/297.40	                                                                        
877.91/297.40	        [Case](x1, x2, x3) = 2 + x1 + x3                                
877.91/297.40	                                                                        
877.91/297.40	  [Frozen](x1, x2, x3, x4) = 2 + 2*x1 + x1*x4 + x2 + 2*x3 + x3*x4 + 2*x4
877.91/297.40	                                                                        
877.91/297.40	         [Sum_sub](x1, x2) = 2 + x2                                     
877.91/297.40	                                                                        
877.91/297.40	        [Sum_constant](x1) = 0                                          
877.91/297.40	                                                                        
877.91/297.40	                  [Left]() = 0                                          
877.91/297.40	                                                                        
877.91/297.40	                 [Right]() = 0                                          
877.91/297.40	                                                                        
877.91/297.40	        [Sum_term_var](x1) = 2                                          
877.91/297.40	                                                                        
877.91/297.40	        [Term_app](x1, x2) = 2 + x1 + x2                                
877.91/297.40	                                                                        
877.91/297.40	       [Term_pair](x1, x2) = 2 + x1 + x2                                
877.91/297.40	                                                                        
877.91/297.40	            [Term_inl](x1) = x1                                         
877.91/297.40	                                                                        
877.91/297.40	            [Term_inr](x1) = 2 + x1                                     
877.91/297.40	                                                                        
877.91/297.40	            [Term_var](x1) = 0                                          
877.91/297.40	                                                                        
877.91/297.40	                    [Id]() = 0                                          
877.91/297.40	                                                                        
877.91/297.40	  [Cons_usual](x1, x2, x3) = 1 + x2 + x3                                
877.91/297.40	                                                                        
877.91/297.40	    [Cons_sum](x1, x2, x3) = x3                                         
877.91/297.40	                                                                        
877.91/297.40	          [Concat](x1, x2) = 2 + 2*x1 + x1*x2 + 2*x2                    
877.91/297.40	                                                                        
877.91/297.40	  
877.91/297.40	  This order satisfies the following ordering constraints.
877.91/297.40	  
877.91/297.40	                   [Term_sub(Term_sub(m, s), t)] =  3 + 4*m + 2*m*s + 2*s + 2*t + 2*m*t + m*s*t + s*t  
877.91/297.40	                                                 >= 3 + 4*m + 2*m*s + m*s*t + 2*m*t + 2*s + s*t + 2*t  
877.91/297.40	                                                 =  [Term_sub(m, Concat(s, t))]                        
877.91/297.40	                                                                                                       
877.91/297.40	                   [Term_sub(Case(m, xi, n), s)] =  5 + 2*m + 2*n + 3*s + m*s + n*s                    
877.91/297.40	                                                 >  4 + 2*m + m*s + 3*s + 2*n + n*s                    
877.91/297.40	                                                 =  [Frozen(m, Sum_sub(xi, s), n, s)]                  
877.91/297.40	                                                                                                       
877.91/297.40	                   [Term_sub(Term_app(m, n), s)] =  5 + 2*m + 2*n + 3*s + m*s + n*s                    
877.91/297.40	                                                 >  4 + 2*m + m*s + 2*s + 2*n + n*s                    
877.91/297.40	                                                 =  [Term_app(Term_sub(m, s), Term_sub(n, s))]         
877.91/297.40	                                                                                                       
877.91/297.40	                  [Term_sub(Term_pair(m, n), s)] =  5 + 2*m + 2*n + 3*s + m*s + n*s                    
877.91/297.40	                                                 >  4 + 2*m + m*s + 2*s + 2*n + n*s                    
877.91/297.40	                                                 =  [Term_pair(Term_sub(m, s), Term_sub(n, s))]        
877.91/297.40	                                                                                                       
877.91/297.40	                      [Term_sub(Term_inl(m), s)] =  1 + 2*m + m*s + s                                  
877.91/297.40	                                                 >= 1 + 2*m + m*s + s                                  
877.91/297.40	                                                 =  [Term_inl(Term_sub(m, s))]                         
877.91/297.40	                                                                                                       
877.91/297.40	                      [Term_sub(Term_inr(m), s)] =  5 + 2*m + 3*s + m*s                                
877.91/297.40	                                                 >  3 + 2*m + m*s + s                                  
877.91/297.40	                                                 =  [Term_inr(Term_sub(m, s))]                         
877.91/297.40	                                                                                                       
877.91/297.40	                   [Term_sub(Term_var(x), Id())] =  1                                                  
877.91/297.40	                                                 >                                                     
877.91/297.40	                                                 =  [Term_var(x)]                                      
877.91/297.40	                                                                                                       
877.91/297.40	    [Term_sub(Term_var(x), Cons_usual(y, m, s))] =  2 + m + s                                          
877.91/297.40	                                                 >  m                                                  
877.91/297.40	                                                 =  [m]                                                
877.91/297.40	                                                                                                       
877.91/297.40	    [Term_sub(Term_var(x), Cons_usual(y, m, s))] =  2 + m + s                                          
877.91/297.40	                                                 >  1 + s                                              
877.91/297.40	                                                 =  [Term_sub(Term_var(x), s)]                         
877.91/297.40	                                                                                                       
877.91/297.40	     [Term_sub(Term_var(x), Cons_sum(xi, k, s))] =  1 + s                                              
877.91/297.40	                                                 >= 1 + s                                              
877.91/297.40	                                                 =  [Term_sub(Term_var(x), s)]                         
877.91/297.40	                                                                                                       
877.91/297.40	         [Frozen(m, Sum_constant(Left()), n, s)] =  2 + 2*m + m*s + 2*n + n*s + 2*s                    
877.91/297.40	                                                 >  1 + 2*m + m*s + s                                  
877.91/297.40	                                                 =  [Term_sub(m, s)]                                   
877.91/297.40	                                                                                                       
877.91/297.40	        [Frozen(m, Sum_constant(Right()), n, s)] =  2 + 2*m + m*s + 2*n + n*s + 2*s                    
877.91/297.40	                                                 >  1 + 2*n + n*s + s                                  
877.91/297.40	                                                 =  [Term_sub(n, s)]                                   
877.91/297.40	                                                                                                       
877.91/297.40	             [Frozen(m, Sum_term_var(xi), n, s)] =  4 + 2*m + m*s + 2*n + n*s + 2*s                    
877.91/297.40	                                                 >= 4 + 2*m + m*s + 2*s + 2*n + n*s                    
877.91/297.40	                                                 =  [Case(Term_sub(m, s), xi, Term_sub(n, s))]         
877.91/297.40	                                                                                                       
877.91/297.40	                             [Sum_sub(xi, Id())] =  2                                                  
877.91/297.40	                                                 >= 2                                                  
877.91/297.40	                                                 =  [Sum_term_var(xi)]                                 
877.91/297.40	                                                                                                       
877.91/297.40	              [Sum_sub(xi, Cons_usual(y, m, s))] =  3 + m + s                                          
877.91/297.40	                                                 >  2 + s                                              
877.91/297.40	                                                 =  [Sum_sub(xi, s)]                                   
877.91/297.40	                                                                                                       
877.91/297.40	              [Sum_sub(xi, Cons_sum(psi, k, s))] =  2 + s                                              
877.91/297.40	                                                 >= 2 + s                                              
877.91/297.40	                                                 =  [Sum_sub(xi, s)]                                   
877.91/297.40	                                                                                                       
877.91/297.40	              [Sum_sub(xi, Cons_sum(psi, k, s))] =  2 + s                                              
877.91/297.40	                                                 >                                                     
877.91/297.40	                                                 =  [Sum_constant(k)]                                  
877.91/297.40	                                                                                                       
877.91/297.40	                               [Concat(Id(), s)] =  2 + 2*s                                            
877.91/297.40	                                                 >  s                                                  
877.91/297.40	                                                 =  [s]                                                
877.91/297.40	                                                                                                       
877.91/297.40	                [Concat(Cons_usual(x, m, s), t)] =  4 + 2*m + 2*s + 3*t + m*t + s*t                    
877.91/297.40	                                                 >= 4 + 2*m + m*t + 3*t + 2*s + s*t                    
877.91/297.40	                                                 =  [Cons_usual(x, Term_sub(m, t), Concat(s, t))]      
877.91/297.40	                                                                                                       
877.91/297.40	                 [Concat(Cons_sum(xi, k, s), t)] =  2 + 2*s + s*t + 2*t                                
877.91/297.40	                                                 >= 2 + 2*s + s*t + 2*t                                
877.91/297.40	                                                 =  [Cons_sum(xi, k, Concat(s, t))]                    
877.91/297.40	                                                                                                       
877.91/297.40	                       [Concat(Concat(s, t), u)] =  6 + 4*s + 2*s*t + 4*t + 4*u + 2*s*u + s*t*u + 2*t*u
877.91/297.40	                                                 >= 6 + 4*s + 2*s*t + s*t*u + 2*s*u + 4*t + 2*t*u + 4*u
877.91/297.40	                                                 =  [Concat(s, Concat(t, u))]                          
877.91/297.40	                                                                                                       
877.91/297.40	
877.91/297.40	We return to the main proof.
877.91/297.40	
877.91/297.40	We are left with following problem, upon which TcT provides the
877.91/297.40	certificate YES(O(1),O(n^2)).
877.91/297.40	
877.91/297.40	Strict Trs:
877.91/297.40	  { Term_sub(Term_sub(m, s), t) -> Term_sub(m, Concat(s, t))
877.91/297.40	  , Term_sub(Term_inl(m), s) -> Term_inl(Term_sub(m, s))
877.91/297.40	  , Frozen(m, Sum_term_var(xi), n, s) ->
877.91/297.40	    Case(Term_sub(m, s), xi, Term_sub(n, s))
877.91/297.40	  , Sum_sub(xi, Id()) -> Sum_term_var(xi)
877.91/297.40	  , Concat(Cons_usual(x, m, s), t) ->
877.91/297.40	    Cons_usual(x, Term_sub(m, t), Concat(s, t))
877.91/297.40	  , Concat(Concat(s, t), u) -> Concat(s, Concat(t, u)) }
877.91/297.40	Weak Trs:
877.91/297.40	  { Term_sub(Case(m, xi, n), s) -> Frozen(m, Sum_sub(xi, s), n, s)
877.91/297.40	  , Term_sub(Term_app(m, n), s) ->
877.91/297.40	    Term_app(Term_sub(m, s), Term_sub(n, s))
877.91/297.40	  , Term_sub(Term_pair(m, n), s) ->
877.91/297.40	    Term_pair(Term_sub(m, s), Term_sub(n, s))
877.91/297.40	  , Term_sub(Term_inr(m), s) -> Term_inr(Term_sub(m, s))
877.91/297.40	  , Term_sub(Term_var(x), Id()) -> Term_var(x)
877.91/297.40	  , Term_sub(Term_var(x), Cons_usual(y, m, s)) -> m
877.91/297.40	  , Term_sub(Term_var(x), Cons_usual(y, m, s)) ->
877.91/297.40	    Term_sub(Term_var(x), s)
877.91/297.40	  , Term_sub(Term_var(x), Cons_sum(xi, k, s)) ->
877.91/297.40	    Term_sub(Term_var(x), s)
877.91/297.40	  , Frozen(m, Sum_constant(Left()), n, s) -> Term_sub(m, s)
877.91/297.40	  , Frozen(m, Sum_constant(Right()), n, s) -> Term_sub(n, s)
877.91/297.40	  , Sum_sub(xi, Cons_usual(y, m, s)) -> Sum_sub(xi, s)
877.91/297.40	  , Sum_sub(xi, Cons_sum(psi, k, s)) -> Sum_sub(xi, s)
877.91/297.40	  , Sum_sub(xi, Cons_sum(psi, k, s)) -> Sum_constant(k)
877.91/297.40	  , Concat(Id(), s) -> s
877.91/297.40	  , Concat(Cons_sum(xi, k, s), t) -> Cons_sum(xi, k, Concat(s, t)) }
877.91/297.40	Obligation:
877.91/297.40	  runtime complexity
877.91/297.40	Answer:
877.91/297.40	  YES(O(1),O(n^2))
877.91/297.40	
877.91/297.40	We use the processor 'polynomial interpretation' to orient
877.91/297.40	following rules strictly.
877.91/297.40	
877.91/297.40	Trs: { Sum_sub(xi, Id()) -> Sum_term_var(xi) }
877.91/297.40	
877.91/297.40	The induced complexity on above rules (modulo remaining rules) is
877.91/297.40	YES(?,O(n^2)) . These rules are moved into the corresponding weak
877.91/297.40	component(s).
877.91/297.40	
877.91/297.40	Sub-proof:
877.91/297.40	----------
877.91/297.40	  We consider the following typing:
877.91/297.40	  
877.91/297.40	    Term_sub :: (g,b) -> g
877.91/297.40	    Case :: (g,c,g) -> g
877.91/297.40	    Frozen :: (g,a,g,b) -> g
877.91/297.40	    Sum_sub :: (c,b) -> a
877.91/297.40	    Sum_constant :: d -> a
877.91/297.40	    Left :: d
877.91/297.40	    Right :: d
877.91/297.40	    Sum_term_var :: c -> a
877.91/297.40	    Term_app :: (g,g) -> g
877.91/297.40	    Term_pair :: (g,g) -> g
877.91/297.40	    Term_inl :: g -> g
877.91/297.40	    Term_inr :: g -> g
877.91/297.40	    Term_var :: e -> g
877.91/297.40	    Id :: b
877.91/297.40	    Cons_usual :: (f,g,b) -> b
877.91/297.40	    Cons_sum :: (h,d,b) -> b
877.91/297.40	    Concat :: (b,b) -> b
877.91/297.40	  
877.91/297.40	  The following argument positions are considered usable:
877.91/297.40	  
877.91/297.40	    Uargs(Term_sub) = {2}, Uargs(Case) = {1, 3},
877.91/297.40	    Uargs(Frozen) = {2, 4}, Uargs(Sum_sub) = {2},
877.91/297.40	    Uargs(Term_app) = {1, 2}, Uargs(Term_pair) = {1, 2},
877.91/297.40	    Uargs(Term_inl) = {1}, Uargs(Term_inr) = {1},
877.91/297.40	    Uargs(Cons_usual) = {2, 3}, Uargs(Cons_sum) = {3},
877.91/297.40	    Uargs(Concat) = {2}
877.91/297.40	  
877.91/297.40	  TcT has computed the following constructor-restricted
877.91/297.40	  typedpolynomial interpretation.
877.91/297.40	  
877.91/297.40	        [Term_sub](x1, x2) = x1 + x1*x2 + x2                        
877.91/297.40	                                                                    
877.91/297.40	        [Case](x1, x2, x3) = 2 + x1 + x3                            
877.91/297.40	                                                                    
877.91/297.40	  [Frozen](x1, x2, x3, x4) = 2 + x1 + x1*x4 + x2 + x3 + x3*x4 + 2*x4
877.91/297.40	                                                                    
877.91/297.40	         [Sum_sub](x1, x2) = x2                                     
877.91/297.40	                                                                    
877.91/297.40	        [Sum_constant](x1) = 0                                      
877.91/297.40	                                                                    
877.91/297.40	                  [Left]() = 0                                      
877.91/297.40	                                                                    
877.91/297.40	                 [Right]() = 0                                      
877.91/297.40	                                                                    
877.91/297.40	        [Sum_term_var](x1) = 0                                      
877.91/297.40	                                                                    
877.91/297.40	        [Term_app](x1, x2) = 1 + x1 + x2                            
877.91/297.40	                                                                    
877.91/297.40	       [Term_pair](x1, x2) = 1 + x1 + x2                            
877.91/297.40	                                                                    
877.91/297.40	            [Term_inl](x1) = x1                                     
877.91/297.40	                                                                    
877.91/297.40	            [Term_inr](x1) = x1                                     
877.91/297.40	                                                                    
877.91/297.40	            [Term_var](x1) = 0                                      
877.91/297.40	                                                                    
877.91/297.40	                    [Id]() = 1                                      
877.91/297.40	                                                                    
877.91/297.40	  [Cons_usual](x1, x2, x3) = 2 + x2 + x3                            
877.91/297.40	                                                                    
877.91/297.40	    [Cons_sum](x1, x2, x3) = x3                                     
877.91/297.40	                                                                    
877.91/297.40	          [Concat](x1, x2) = x1 + x1*x2 + x2                        
877.91/297.40	                                                                    
877.91/297.40	  
877.91/297.40	  This order satisfies the following ordering constraints.
877.91/297.40	  
877.91/297.40	                   [Term_sub(Term_sub(m, s), t)] =  m + m*s + s + m*t + m*s*t + s*t + t          
877.91/297.40	                                                 >= m + m*s + m*s*t + m*t + s + s*t + t          
877.91/297.40	                                                 =  [Term_sub(m, Concat(s, t))]                  
877.91/297.40	                                                                                                 
877.91/297.40	                   [Term_sub(Case(m, xi, n), s)] =  2 + m + n + 3*s + m*s + n*s                  
877.91/297.40	                                                 >= 2 + m + m*s + 3*s + n + n*s                  
877.91/297.40	                                                 =  [Frozen(m, Sum_sub(xi, s), n, s)]            
877.91/297.40	                                                                                                 
877.91/297.40	                   [Term_sub(Term_app(m, n), s)] =  1 + m + n + 2*s + m*s + n*s                  
877.91/297.40	                                                 >= 1 + m + m*s + 2*s + n + n*s                  
877.91/297.40	                                                 =  [Term_app(Term_sub(m, s), Term_sub(n, s))]   
877.91/297.40	                                                                                                 
877.91/297.40	                  [Term_sub(Term_pair(m, n), s)] =  1 + m + n + 2*s + m*s + n*s                  
877.91/297.40	                                                 >= 1 + m + m*s + 2*s + n + n*s                  
877.91/297.40	                                                 =  [Term_pair(Term_sub(m, s), Term_sub(n, s))]  
877.91/297.40	                                                                                                 
877.91/297.40	                      [Term_sub(Term_inl(m), s)] =  m + m*s + s                                  
877.91/297.40	                                                 >= m + m*s + s                                  
877.91/297.40	                                                 =  [Term_inl(Term_sub(m, s))]                   
877.91/297.40	                                                                                                 
877.91/297.40	                      [Term_sub(Term_inr(m), s)] =  m + m*s + s                                  
877.91/297.40	                                                 >= m + m*s + s                                  
877.91/297.40	                                                 =  [Term_inr(Term_sub(m, s))]                   
877.91/297.40	                                                                                                 
877.91/297.40	                   [Term_sub(Term_var(x), Id())] =  1                                            
877.91/297.40	                                                 >                                               
877.91/297.40	                                                 =  [Term_var(x)]                                
877.91/297.40	                                                                                                 
877.91/297.40	    [Term_sub(Term_var(x), Cons_usual(y, m, s))] =  2 + m + s                                    
877.91/297.40	                                                 >  m                                            
877.91/297.40	                                                 =  [m]                                          
877.91/297.40	                                                                                                 
877.91/297.40	    [Term_sub(Term_var(x), Cons_usual(y, m, s))] =  2 + m + s                                    
877.91/297.40	                                                 >  s                                            
877.91/297.40	                                                 =  [Term_sub(Term_var(x), s)]                   
877.91/297.40	                                                                                                 
877.91/297.40	     [Term_sub(Term_var(x), Cons_sum(xi, k, s))] =  s                                            
877.91/297.40	                                                 >= s                                            
877.91/297.40	                                                 =  [Term_sub(Term_var(x), s)]                   
877.91/297.40	                                                                                                 
877.91/297.40	         [Frozen(m, Sum_constant(Left()), n, s)] =  2 + m + m*s + n + n*s + 2*s                  
877.91/297.40	                                                 >  m + m*s + s                                  
877.91/297.40	                                                 =  [Term_sub(m, s)]                             
877.91/297.40	                                                                                                 
877.91/297.40	        [Frozen(m, Sum_constant(Right()), n, s)] =  2 + m + m*s + n + n*s + 2*s                  
877.91/297.40	                                                 >  n + n*s + s                                  
877.91/297.40	                                                 =  [Term_sub(n, s)]                             
877.91/297.40	                                                                                                 
877.91/297.40	             [Frozen(m, Sum_term_var(xi), n, s)] =  2 + m + m*s + n + n*s + 2*s                  
877.91/297.40	                                                 >= 2 + m + m*s + 2*s + n + n*s                  
877.91/297.40	                                                 =  [Case(Term_sub(m, s), xi, Term_sub(n, s))]   
877.91/297.40	                                                                                                 
877.91/297.40	                             [Sum_sub(xi, Id())] =  1                                            
877.91/297.40	                                                 >                                               
877.91/297.40	                                                 =  [Sum_term_var(xi)]                           
877.91/297.40	                                                                                                 
877.91/297.40	              [Sum_sub(xi, Cons_usual(y, m, s))] =  2 + m + s                                    
877.91/297.40	                                                 >  s                                            
877.91/297.40	                                                 =  [Sum_sub(xi, s)]                             
877.91/297.40	                                                                                                 
877.91/297.40	              [Sum_sub(xi, Cons_sum(psi, k, s))] =  s                                            
877.91/297.40	                                                 >= s                                            
877.91/297.40	                                                 =  [Sum_sub(xi, s)]                             
877.91/297.40	                                                                                                 
877.91/297.40	              [Sum_sub(xi, Cons_sum(psi, k, s))] =  s                                            
877.91/297.40	                                                 >=                                              
877.91/297.40	                                                 =  [Sum_constant(k)]                            
877.91/297.41	                                                                                                 
877.91/297.41	                               [Concat(Id(), s)] =  1 + 2*s                                      
877.91/297.41	                                                 >  s                                            
877.91/297.41	                                                 =  [s]                                          
877.91/297.41	                                                                                                 
877.91/297.41	                [Concat(Cons_usual(x, m, s), t)] =  2 + m + s + 3*t + m*t + s*t                  
877.91/297.41	                                                 >= 2 + m + m*t + 2*t + s + s*t                  
877.91/297.41	                                                 =  [Cons_usual(x, Term_sub(m, t), Concat(s, t))]
877.91/297.41	                                                                                                 
877.91/297.41	                 [Concat(Cons_sum(xi, k, s), t)] =  s + s*t + t                                  
877.91/297.41	                                                 >= s + s*t + t                                  
877.91/297.41	                                                 =  [Cons_sum(xi, k, Concat(s, t))]              
877.91/297.41	                                                                                                 
877.91/297.41	                       [Concat(Concat(s, t), u)] =  s + s*t + t + s*u + s*t*u + t*u + u          
877.91/297.41	                                                 >= s + s*t + s*t*u + s*u + t + t*u + u          
877.91/297.41	                                                 =  [Concat(s, Concat(t, u))]                    
877.91/297.41	                                                                                                 
877.91/297.41	
877.91/297.41	We return to the main proof.
877.91/297.41	
877.91/297.41	We are left with following problem, upon which TcT provides the
877.91/297.41	certificate YES(O(1),O(n^2)).
877.91/297.41	
877.91/297.41	Strict Trs:
877.91/297.41	  { Term_sub(Term_sub(m, s), t) -> Term_sub(m, Concat(s, t))
877.91/297.41	  , Term_sub(Term_inl(m), s) -> Term_inl(Term_sub(m, s))
877.91/297.41	  , Frozen(m, Sum_term_var(xi), n, s) ->
877.91/297.41	    Case(Term_sub(m, s), xi, Term_sub(n, s))
877.91/297.41	  , Concat(Cons_usual(x, m, s), t) ->
877.91/297.41	    Cons_usual(x, Term_sub(m, t), Concat(s, t))
877.91/297.41	  , Concat(Concat(s, t), u) -> Concat(s, Concat(t, u)) }
877.91/297.41	Weak Trs:
877.91/297.41	  { Term_sub(Case(m, xi, n), s) -> Frozen(m, Sum_sub(xi, s), n, s)
877.91/297.41	  , Term_sub(Term_app(m, n), s) ->
877.91/297.41	    Term_app(Term_sub(m, s), Term_sub(n, s))
877.91/297.41	  , Term_sub(Term_pair(m, n), s) ->
877.91/297.41	    Term_pair(Term_sub(m, s), Term_sub(n, s))
877.91/297.41	  , Term_sub(Term_inr(m), s) -> Term_inr(Term_sub(m, s))
877.91/297.41	  , Term_sub(Term_var(x), Id()) -> Term_var(x)
877.91/297.41	  , Term_sub(Term_var(x), Cons_usual(y, m, s)) -> m
877.91/297.41	  , Term_sub(Term_var(x), Cons_usual(y, m, s)) ->
877.91/297.41	    Term_sub(Term_var(x), s)
877.91/297.41	  , Term_sub(Term_var(x), Cons_sum(xi, k, s)) ->
877.91/297.41	    Term_sub(Term_var(x), s)
877.91/297.41	  , Frozen(m, Sum_constant(Left()), n, s) -> Term_sub(m, s)
877.91/297.41	  , Frozen(m, Sum_constant(Right()), n, s) -> Term_sub(n, s)
877.91/297.41	  , Sum_sub(xi, Id()) -> Sum_term_var(xi)
877.91/297.41	  , Sum_sub(xi, Cons_usual(y, m, s)) -> Sum_sub(xi, s)
877.91/297.41	  , Sum_sub(xi, Cons_sum(psi, k, s)) -> Sum_sub(xi, s)
877.91/297.41	  , Sum_sub(xi, Cons_sum(psi, k, s)) -> Sum_constant(k)
877.91/297.41	  , Concat(Id(), s) -> s
877.91/297.41	  , Concat(Cons_sum(xi, k, s), t) -> Cons_sum(xi, k, Concat(s, t)) }
877.91/297.41	Obligation:
877.91/297.41	  runtime complexity
877.91/297.41	Answer:
877.91/297.41	  YES(O(1),O(n^2))
877.91/297.41	
877.91/297.41	We use the processor 'polynomial interpretation' to orient
877.91/297.41	following rules strictly.
877.91/297.41	
877.91/297.41	Trs:
877.91/297.41	  { Frozen(m, Sum_term_var(xi), n, s) ->
877.91/297.41	    Case(Term_sub(m, s), xi, Term_sub(n, s)) }
877.91/297.41	
877.91/297.41	The induced complexity on above rules (modulo remaining rules) is
877.91/297.41	YES(?,O(n^2)) . These rules are moved into the corresponding weak
877.91/297.41	component(s).
877.91/297.41	
877.91/297.41	Sub-proof:
877.91/297.41	----------
877.91/297.41	  We consider the following typing:
877.91/297.41	  
877.91/297.41	    Term_sub :: (g,b) -> g
877.91/297.41	    Case :: (g,c,g) -> g
877.91/297.41	    Frozen :: (g,a,g,b) -> g
877.91/297.41	    Sum_sub :: (c,b) -> a
877.91/297.41	    Sum_constant :: d -> a
877.91/297.41	    Left :: d
877.91/297.41	    Right :: d
877.91/297.41	    Sum_term_var :: c -> a
877.91/297.41	    Term_app :: (g,g) -> g
877.91/297.41	    Term_pair :: (g,g) -> g
877.91/297.41	    Term_inl :: g -> g
877.91/297.41	    Term_inr :: g -> g
877.91/297.41	    Term_var :: e -> g
877.91/297.41	    Id :: b
877.91/297.41	    Cons_usual :: (f,g,b) -> b
877.91/297.41	    Cons_sum :: (h,d,b) -> b
877.91/297.41	    Concat :: (b,b) -> b
877.91/297.41	  
877.91/297.41	  The following argument positions are considered usable:
877.91/297.41	  
877.91/297.41	    Uargs(Term_sub) = {2}, Uargs(Case) = {1, 3},
877.91/297.41	    Uargs(Frozen) = {2, 4}, Uargs(Sum_sub) = {2},
877.91/297.41	    Uargs(Term_app) = {1, 2}, Uargs(Term_pair) = {1, 2},
877.91/297.41	    Uargs(Term_inl) = {1}, Uargs(Term_inr) = {1},
877.91/297.41	    Uargs(Cons_usual) = {2, 3}, Uargs(Cons_sum) = {3},
877.91/297.41	    Uargs(Concat) = {2}
877.91/297.41	  
877.91/297.41	  TcT has computed the following constructor-restricted
877.91/297.41	  typedpolynomial interpretation.
877.91/297.41	  
877.91/297.41	        [Term_sub](x1, x2) = 1 + 2*x1 + x1*x2 + x2                      
877.91/297.41	                                                                        
877.91/297.41	        [Case](x1, x2, x3) = 2 + x1 + x3                                
877.91/297.41	                                                                        
877.91/297.41	  [Frozen](x1, x2, x3, x4) = 3 + 2*x1 + x1*x4 + x2 + 2*x3 + x3*x4 + 2*x4
877.91/297.41	                                                                        
877.91/297.41	         [Sum_sub](x1, x2) = x2                                         
877.91/297.41	                                                                        
877.91/297.41	        [Sum_constant](x1) = 0                                          
877.91/297.41	                                                                        
877.91/297.41	                  [Left]() = 0                                          
877.91/297.41	                                                                        
877.91/297.41	                 [Right]() = 0                                          
877.91/297.41	                                                                        
877.91/297.41	        [Sum_term_var](x1) = 2                                          
877.91/297.41	                                                                        
877.91/297.41	        [Term_app](x1, x2) = 1 + x1 + x2                                
877.91/297.41	                                                                        
877.91/297.41	       [Term_pair](x1, x2) = 2 + x1 + x2                                
877.91/297.41	                                                                        
877.91/297.41	            [Term_inl](x1) = x1                                         
877.91/297.41	                                                                        
877.91/297.41	            [Term_inr](x1) = x1                                         
877.91/297.41	                                                                        
877.91/297.41	            [Term_var](x1) = 0                                          
877.91/297.41	                                                                        
877.91/297.41	                    [Id]() = 2                                          
877.91/297.41	                                                                        
877.91/297.41	  [Cons_usual](x1, x2, x3) = 2 + 2*x2 + x3                              
877.91/297.41	                                                                        
877.91/297.41	    [Cons_sum](x1, x2, x3) = 2 + x3                                     
877.91/297.41	                                                                        
877.91/297.41	          [Concat](x1, x2) = 2 + 2*x1 + x1*x2 + 2*x2                    
877.91/297.41	                                                                        
877.91/297.41	  
877.91/297.41	  This order satisfies the following ordering constraints.
877.91/297.41	  
877.91/297.41	                   [Term_sub(Term_sub(m, s), t)] =  3 + 4*m + 2*m*s + 2*s + 2*t + 2*m*t + m*s*t + s*t  
877.91/297.41	                                                 >= 3 + 4*m + 2*m*s + m*s*t + 2*m*t + 2*s + s*t + 2*t  
877.91/297.41	                                                 =  [Term_sub(m, Concat(s, t))]                        
877.91/297.41	                                                                                                       
877.91/297.41	                   [Term_sub(Case(m, xi, n), s)] =  5 + 2*m + 2*n + 3*s + m*s + n*s                    
877.91/297.41	                                                 >  3 + 2*m + m*s + 3*s + 2*n + n*s                    
877.91/297.41	                                                 =  [Frozen(m, Sum_sub(xi, s), n, s)]                  
877.91/297.41	                                                                                                       
877.91/297.41	                   [Term_sub(Term_app(m, n), s)] =  3 + 2*m + 2*n + 2*s + m*s + n*s                    
877.91/297.41	                                                 >= 3 + 2*m + m*s + 2*s + 2*n + n*s                    
877.91/297.41	                                                 =  [Term_app(Term_sub(m, s), Term_sub(n, s))]         
877.91/297.41	                                                                                                       
877.91/297.41	                  [Term_sub(Term_pair(m, n), s)] =  5 + 2*m + 2*n + 3*s + m*s + n*s                    
877.91/297.41	                                                 >  4 + 2*m + m*s + 2*s + 2*n + n*s                    
877.91/297.41	                                                 =  [Term_pair(Term_sub(m, s), Term_sub(n, s))]        
877.91/297.41	                                                                                                       
877.91/297.41	                      [Term_sub(Term_inl(m), s)] =  1 + 2*m + m*s + s                                  
877.91/297.41	                                                 >= 1 + 2*m + m*s + s                                  
877.91/297.41	                                                 =  [Term_inl(Term_sub(m, s))]                         
877.91/297.41	                                                                                                       
877.91/297.41	                      [Term_sub(Term_inr(m), s)] =  1 + 2*m + m*s + s                                  
877.91/297.41	                                                 >= 1 + 2*m + m*s + s                                  
877.91/297.41	                                                 =  [Term_inr(Term_sub(m, s))]                         
877.91/297.41	                                                                                                       
877.91/297.41	                   [Term_sub(Term_var(x), Id())] =  3                                                  
877.91/297.41	                                                 >                                                     
877.91/297.41	                                                 =  [Term_var(x)]                                      
877.91/297.41	                                                                                                       
877.91/297.41	    [Term_sub(Term_var(x), Cons_usual(y, m, s))] =  3 + 2*m + s                                        
877.91/297.41	                                                 >  m                                                  
877.91/297.41	                                                 =  [m]                                                
877.91/297.41	                                                                                                       
877.91/297.41	    [Term_sub(Term_var(x), Cons_usual(y, m, s))] =  3 + 2*m + s                                        
877.91/297.41	                                                 >  1 + s                                              
877.91/297.41	                                                 =  [Term_sub(Term_var(x), s)]                         
877.91/297.41	                                                                                                       
877.91/297.41	     [Term_sub(Term_var(x), Cons_sum(xi, k, s))] =  3 + s                                              
877.91/297.41	                                                 >  1 + s                                              
877.91/297.41	                                                 =  [Term_sub(Term_var(x), s)]                         
877.91/297.41	                                                                                                       
877.91/297.41	         [Frozen(m, Sum_constant(Left()), n, s)] =  3 + 2*m + m*s + 2*n + n*s + 2*s                    
877.91/297.41	                                                 >  1 + 2*m + m*s + s                                  
877.91/297.41	                                                 =  [Term_sub(m, s)]                                   
877.91/297.41	                                                                                                       
877.91/297.41	        [Frozen(m, Sum_constant(Right()), n, s)] =  3 + 2*m + m*s + 2*n + n*s + 2*s                    
877.91/297.41	                                                 >  1 + 2*n + n*s + s                                  
877.91/297.41	                                                 =  [Term_sub(n, s)]                                   
877.91/297.41	                                                                                                       
877.91/297.41	             [Frozen(m, Sum_term_var(xi), n, s)] =  5 + 2*m + m*s + 2*n + n*s + 2*s                    
877.91/297.41	                                                 >  4 + 2*m + m*s + 2*s + 2*n + n*s                    
877.91/297.41	                                                 =  [Case(Term_sub(m, s), xi, Term_sub(n, s))]         
877.91/297.41	                                                                                                       
877.91/297.41	                             [Sum_sub(xi, Id())] =  2                                                  
877.91/297.41	                                                 >= 2                                                  
877.91/297.41	                                                 =  [Sum_term_var(xi)]                                 
877.91/297.41	                                                                                                       
877.91/297.41	              [Sum_sub(xi, Cons_usual(y, m, s))] =  2 + 2*m + s                                        
877.91/297.41	                                                 >  s                                                  
877.91/297.41	                                                 =  [Sum_sub(xi, s)]                                   
877.91/297.41	                                                                                                       
877.91/297.41	              [Sum_sub(xi, Cons_sum(psi, k, s))] =  2 + s                                              
877.91/297.41	                                                 >  s                                                  
877.91/297.41	                                                 =  [Sum_sub(xi, s)]                                   
877.91/297.41	                                                                                                       
877.91/297.41	              [Sum_sub(xi, Cons_sum(psi, k, s))] =  2 + s                                              
877.91/297.41	                                                 >                                                     
877.91/297.41	                                                 =  [Sum_constant(k)]                                  
877.91/297.41	                                                                                                       
877.91/297.41	                               [Concat(Id(), s)] =  6 + 4*s                                            
877.91/297.41	                                                 >  s                                                  
877.91/297.41	                                                 =  [s]                                                
877.91/297.41	                                                                                                       
877.91/297.41	                [Concat(Cons_usual(x, m, s), t)] =  6 + 4*m + 2*s + 4*t + 2*m*t + s*t                  
877.91/297.41	                                                 >= 6 + 4*m + 2*m*t + 4*t + 2*s + s*t                  
877.91/297.41	                                                 =  [Cons_usual(x, Term_sub(m, t), Concat(s, t))]      
877.91/297.41	                                                                                                       
877.91/297.41	                 [Concat(Cons_sum(xi, k, s), t)] =  6 + 2*s + 4*t + s*t                                
877.91/297.41	                                                 >  4 + 2*s + s*t + 2*t                                
877.91/297.41	                                                 =  [Cons_sum(xi, k, Concat(s, t))]                    
877.91/297.41	                                                                                                       
877.91/297.41	                       [Concat(Concat(s, t), u)] =  6 + 4*s + 2*s*t + 4*t + 4*u + 2*s*u + s*t*u + 2*t*u
877.91/297.41	                                                 >= 6 + 4*s + 2*s*t + s*t*u + 2*s*u + 4*t + 2*t*u + 4*u
877.91/297.41	                                                 =  [Concat(s, Concat(t, u))]                          
877.91/297.41	                                                                                                       
877.91/297.41	
877.91/297.41	We return to the main proof.
877.91/297.41	
877.91/297.41	We are left with following problem, upon which TcT provides the
877.91/297.41	certificate YES(O(1),O(n^2)).
877.91/297.41	
877.91/297.41	Strict Trs:
877.91/297.41	  { Term_sub(Term_sub(m, s), t) -> Term_sub(m, Concat(s, t))
877.91/297.41	  , Term_sub(Term_inl(m), s) -> Term_inl(Term_sub(m, s))
877.91/297.41	  , Concat(Cons_usual(x, m, s), t) ->
877.91/297.41	    Cons_usual(x, Term_sub(m, t), Concat(s, t))
877.91/297.41	  , Concat(Concat(s, t), u) -> Concat(s, Concat(t, u)) }
877.91/297.41	Weak Trs:
877.91/297.41	  { Term_sub(Case(m, xi, n), s) -> Frozen(m, Sum_sub(xi, s), n, s)
877.91/297.41	  , Term_sub(Term_app(m, n), s) ->
877.91/297.41	    Term_app(Term_sub(m, s), Term_sub(n, s))
877.91/297.41	  , Term_sub(Term_pair(m, n), s) ->
877.91/297.41	    Term_pair(Term_sub(m, s), Term_sub(n, s))
877.91/297.41	  , Term_sub(Term_inr(m), s) -> Term_inr(Term_sub(m, s))
877.91/297.41	  , Term_sub(Term_var(x), Id()) -> Term_var(x)
877.91/297.41	  , Term_sub(Term_var(x), Cons_usual(y, m, s)) -> m
877.91/297.41	  , Term_sub(Term_var(x), Cons_usual(y, m, s)) ->
877.91/297.41	    Term_sub(Term_var(x), s)
877.91/297.41	  , Term_sub(Term_var(x), Cons_sum(xi, k, s)) ->
877.91/297.41	    Term_sub(Term_var(x), s)
877.91/297.41	  , Frozen(m, Sum_constant(Left()), n, s) -> Term_sub(m, s)
877.91/297.41	  , Frozen(m, Sum_constant(Right()), n, s) -> Term_sub(n, s)
877.91/297.41	  , Frozen(m, Sum_term_var(xi), n, s) ->
877.91/297.41	    Case(Term_sub(m, s), xi, Term_sub(n, s))
877.91/297.41	  , Sum_sub(xi, Id()) -> Sum_term_var(xi)
877.91/297.41	  , Sum_sub(xi, Cons_usual(y, m, s)) -> Sum_sub(xi, s)
877.91/297.41	  , Sum_sub(xi, Cons_sum(psi, k, s)) -> Sum_sub(xi, s)
877.91/297.41	  , Sum_sub(xi, Cons_sum(psi, k, s)) -> Sum_constant(k)
877.91/297.41	  , Concat(Id(), s) -> s
877.91/297.41	  , Concat(Cons_sum(xi, k, s), t) -> Cons_sum(xi, k, Concat(s, t)) }
877.91/297.41	Obligation:
877.91/297.41	  runtime complexity
877.91/297.41	Answer:
877.91/297.41	  YES(O(1),O(n^2))
877.91/297.41	
877.91/297.41	We use the processor 'polynomial interpretation' to orient
877.91/297.41	following rules strictly.
877.91/297.41	
877.91/297.41	Trs:
877.91/297.41	  { Concat(Cons_usual(x, m, s), t) ->
877.91/297.41	    Cons_usual(x, Term_sub(m, t), Concat(s, t)) }
877.91/297.41	
877.91/297.41	The induced complexity on above rules (modulo remaining rules) is
877.91/297.41	YES(?,O(n^2)) . These rules are moved into the corresponding weak
877.91/297.41	component(s).
877.91/297.41	
877.91/297.41	Sub-proof:
877.91/297.41	----------
877.91/297.41	  We consider the following typing:
877.91/297.41	  
877.91/297.41	    Term_sub :: (g,b) -> g
877.91/297.41	    Case :: (g,c,g) -> g
877.91/297.41	    Frozen :: (g,a,g,b) -> g
877.91/297.41	    Sum_sub :: (c,b) -> a
877.91/297.41	    Sum_constant :: d -> a
877.91/297.41	    Left :: d
877.91/297.41	    Right :: d
877.91/297.41	    Sum_term_var :: c -> a
877.91/297.41	    Term_app :: (g,g) -> g
877.91/297.41	    Term_pair :: (g,g) -> g
877.91/297.41	    Term_inl :: g -> g
877.91/297.41	    Term_inr :: g -> g
877.91/297.41	    Term_var :: e -> g
877.91/297.41	    Id :: b
877.91/297.41	    Cons_usual :: (f,g,b) -> b
877.91/297.41	    Cons_sum :: (h,d,b) -> b
877.91/297.41	    Concat :: (b,b) -> b
877.91/297.41	  
877.91/297.41	  The following argument positions are considered usable:
877.91/297.41	  
877.91/297.41	    Uargs(Term_sub) = {2}, Uargs(Case) = {1, 3},
877.91/297.41	    Uargs(Frozen) = {2, 4}, Uargs(Sum_sub) = {2},
877.91/297.41	    Uargs(Term_app) = {1, 2}, Uargs(Term_pair) = {1, 2},
877.91/297.41	    Uargs(Term_inl) = {1}, Uargs(Term_inr) = {1},
877.91/297.41	    Uargs(Cons_usual) = {2, 3}, Uargs(Cons_sum) = {3},
877.91/297.41	    Uargs(Concat) = {2}
877.91/297.41	  
877.91/297.41	  TcT has computed the following constructor-restricted
877.91/297.41	  typedpolynomial interpretation.
877.91/297.41	  
877.91/297.41	        [Term_sub](x1, x2) = x1 + 2*x1*x2 + x1^2 + x2                                         
877.91/297.41	                                                                                              
877.91/297.41	        [Case](x1, x2, x3) = 1 + x1 + x3                                                      
877.91/297.41	                                                                                              
877.91/297.41	  [Frozen](x1, x2, x3, x4) = 1 + x1 + x1*x3 + 2*x1*x4 + x1^2 + x2 + x3 + 2*x3*x4 + x3^2 + 2*x4
877.91/297.41	                                                                                              
877.91/297.41	         [Sum_sub](x1, x2) = 1 + x2                                                           
877.91/297.41	                                                                                              
877.91/297.41	        [Sum_constant](x1) = 0                                                                
877.91/297.41	                                                                                              
877.91/297.41	                  [Left]() = 0                                                                
877.91/297.41	                                                                                              
877.91/297.41	                 [Right]() = 0                                                                
877.91/297.41	                                                                                              
877.91/297.41	        [Sum_term_var](x1) = 0                                                                
877.91/297.41	                                                                                              
877.91/297.41	        [Term_app](x1, x2) = 2 + x1 + x2                                                      
877.91/297.41	                                                                                              
877.91/297.41	       [Term_pair](x1, x2) = 2 + x1 + x2                                                      
877.91/297.41	                                                                                              
877.91/297.41	            [Term_inl](x1) = x1                                                               
877.91/297.41	                                                                                              
877.91/297.41	            [Term_inr](x1) = 1 + x1                                                           
877.91/297.41	                                                                                              
877.91/297.41	            [Term_var](x1) = x1                                                               
877.91/297.41	                                                                                              
877.91/297.41	                    [Id]() = 0                                                                
877.91/297.41	                                                                                              
877.91/297.41	  [Cons_usual](x1, x2, x3) = 2 + x2 + x3                                                      
877.91/297.41	                                                                                              
877.91/297.41	    [Cons_sum](x1, x2, x3) = x3                                                               
877.91/297.41	                                                                                              
877.91/297.41	          [Concat](x1, x2) = x1 + 2*x1*x2 + x1^2 + x2                                         
877.91/297.41	                                                                                              
877.91/297.41	  
877.91/297.41	  This order satisfies the following ordering constraints.
877.91/297.41	  
877.91/297.41	                   [Term_sub(Term_sub(m, s), t)] =  m + 3*m*s + 2*m^2 + s + 2*m*t + 4*m*s*t + 2*m^2*t + 2*s*t + 5*m^2*s + 2*m^3 + 4*m^2*s^2 + 4*m^3*s + 2*m*s^2 + m^4 + s*m + 2*s^2*m + s*m^2 + s^2 + t
877.91/297.41	                                                 >= m + 2*m*s + 4*m*s*t + 2*m*s^2 + 2*m*t + m^2 + s + 2*s*t + s^2 + t                                                                                  
877.91/297.41	                                                 =  [Term_sub(m, Concat(s, t))]                                                                                                                        
877.91/297.41	                                                                                                                                                                                                       
877.91/297.41	                   [Term_sub(Case(m, xi, n), s)] =  2 + 3*m + 3*n + 3*s + 2*m*s + 2*n*s + m^2 + m*n + n*m + n^2                                                                                        
877.91/297.41	                                                 >= 2 + m + m*n + 2*m*s + m^2 + 3*s + n + 2*n*s + n^2                                                                                                  
877.91/297.41	                                                 =  [Frozen(m, Sum_sub(xi, s), n, s)]                                                                                                                  
877.91/297.41	                                                                                                                                                                                                       
877.91/297.41	                   [Term_sub(Term_app(m, n), s)] =  6 + 5*m + 5*n + 5*s + 2*m*s + 2*n*s + m^2 + m*n + n*m + n^2                                                                                        
877.91/297.41	                                                 >  2 + m + 2*m*s + m^2 + 2*s + n + 2*n*s + n^2                                                                                                        
877.91/297.41	                                                 =  [Term_app(Term_sub(m, s), Term_sub(n, s))]                                                                                                         
877.91/297.41	                                                                                                                                                                                                       
877.91/297.41	                  [Term_sub(Term_pair(m, n), s)] =  6 + 5*m + 5*n + 5*s + 2*m*s + 2*n*s + m^2 + m*n + n*m + n^2                                                                                        
877.91/297.41	                                                 >  2 + m + 2*m*s + m^2 + 2*s + n + 2*n*s + n^2                                                                                                        
877.91/297.41	                                                 =  [Term_pair(Term_sub(m, s), Term_sub(n, s))]                                                                                                        
877.91/297.41	                                                                                                                                                                                                       
877.91/297.41	                      [Term_sub(Term_inl(m), s)] =  m + 2*m*s + m^2 + s                                                                                                                                
877.91/297.41	                                                 >= m + 2*m*s + m^2 + s                                                                                                                                
877.91/297.41	                                                 =  [Term_inl(Term_sub(m, s))]                                                                                                                         
877.91/297.41	                                                                                                                                                                                                       
877.91/297.41	                      [Term_sub(Term_inr(m), s)] =  2 + 3*m + 3*s + 2*m*s + m^2                                                                                                                        
877.91/297.41	                                                 >  1 + m + 2*m*s + m^2 + s                                                                                                                            
877.91/297.41	                                                 =  [Term_inr(Term_sub(m, s))]                                                                                                                         
877.91/297.41	                                                                                                                                                                                                       
877.91/297.41	                   [Term_sub(Term_var(x), Id())] =  x + x^2                                                                                                                                            
877.91/297.41	                                                 >= x                                                                                                                                                  
877.91/297.41	                                                 =  [Term_var(x)]                                                                                                                                      
877.91/297.41	                                                                                                                                                                                                       
877.91/297.41	    [Term_sub(Term_var(x), Cons_usual(y, m, s))] =  5*x + 2*x*m + 2*x*s + x^2 + 2 + m + s                                                                                                              
877.91/297.41	                                                 >  m                                                                                                                                                  
877.91/297.41	                                                 =  [m]                                                                                                                                                
877.91/297.41	                                                                                                                                                                                                       
877.91/297.41	    [Term_sub(Term_var(x), Cons_usual(y, m, s))] =  5*x + 2*x*m + 2*x*s + x^2 + 2 + m + s                                                                                                              
877.91/297.41	                                                 >  x + 2*x*s + x^2 + s                                                                                                                                
877.91/297.41	                                                 =  [Term_sub(Term_var(x), s)]                                                                                                                         
877.91/297.41	                                                                                                                                                                                                       
877.91/297.41	     [Term_sub(Term_var(x), Cons_sum(xi, k, s))] =  x + 2*x*s + x^2 + s                                                                                                                                
877.91/297.41	                                                 >= x + 2*x*s + x^2 + s                                                                                                                                
877.91/297.41	                                                 =  [Term_sub(Term_var(x), s)]                                                                                                                         
877.91/297.41	                                                                                                                                                                                                       
877.91/297.41	         [Frozen(m, Sum_constant(Left()), n, s)] =  1 + m + m*n + 2*m*s + m^2 + n + 2*n*s + n^2 + 2*s                                                                                                  
877.91/297.41	                                                 >  m + 2*m*s + m^2 + s                                                                                                                                
877.91/297.41	                                                 =  [Term_sub(m, s)]                                                                                                                                   
877.91/297.41	                                                                                                                                                                                                       
877.91/297.41	        [Frozen(m, Sum_constant(Right()), n, s)] =  1 + m + m*n + 2*m*s + m^2 + n + 2*n*s + n^2 + 2*s                                                                                                  
877.91/297.41	                                                 >  n + 2*n*s + n^2 + s                                                                                                                                
877.91/297.41	                                                 =  [Term_sub(n, s)]                                                                                                                                   
877.91/297.41	                                                                                                                                                                                                       
877.91/297.41	             [Frozen(m, Sum_term_var(xi), n, s)] =  1 + m + m*n + 2*m*s + m^2 + n + 2*n*s + n^2 + 2*s                                                                                                  
877.91/297.41	                                                 >= 1 + m + 2*m*s + m^2 + 2*s + n + 2*n*s + n^2                                                                                                        
877.91/297.41	                                                 =  [Case(Term_sub(m, s), xi, Term_sub(n, s))]                                                                                                         
877.91/297.41	                                                                                                                                                                                                       
877.91/297.41	                             [Sum_sub(xi, Id())] =  1                                                                                                                                                  
877.91/297.41	                                                 >                                                                                                                                                     
877.91/297.41	                                                 =  [Sum_term_var(xi)]                                                                                                                                 
877.91/297.41	                                                                                                                                                                                                       
877.91/297.41	              [Sum_sub(xi, Cons_usual(y, m, s))] =  3 + m + s                                                                                                                                          
877.91/297.41	                                                 >  1 + s                                                                                                                                              
877.91/297.41	                                                 =  [Sum_sub(xi, s)]                                                                                                                                   
877.91/297.41	                                                                                                                                                                                                       
877.91/297.41	              [Sum_sub(xi, Cons_sum(psi, k, s))] =  1 + s                                                                                                                                              
877.91/297.41	                                                 >= 1 + s                                                                                                                                              
877.91/297.41	                                                 =  [Sum_sub(xi, s)]                                                                                                                                   
877.91/297.41	                                                                                                                                                                                                       
877.91/297.41	              [Sum_sub(xi, Cons_sum(psi, k, s))] =  1 + s                                                                                                                                              
877.91/297.41	                                                 >                                                                                                                                                     
877.91/297.41	                                                 =  [Sum_constant(k)]                                                                                                                                  
877.91/297.41	                                                                                                                                                                                                       
877.91/297.41	                               [Concat(Id(), s)] =  s                                                                                                                                                  
877.91/297.41	                                                 >= s                                                                                                                                                  
877.91/297.41	                                                 =  [s]                                                                                                                                                
877.91/297.41	                                                                                                                                                                                                       
877.91/297.41	                [Concat(Cons_usual(x, m, s), t)] =  6 + 5*m + 5*s + 5*t + 2*m*t + 2*s*t + m^2 + m*s + s*m + s^2                                                                                        
877.91/297.41	                                                 >  2 + m + 2*m*t + m^2 + 2*t + s + 2*s*t + s^2                                                                                                        
877.91/297.41	                                                 =  [Cons_usual(x, Term_sub(m, t), Concat(s, t))]                                                                                                      
877.91/297.41	                                                                                                                                                                                                       
877.91/297.41	                 [Concat(Cons_sum(xi, k, s), t)] =  s + 2*s*t + s^2 + t                                                                                                                                
877.91/297.41	                                                 >= s + 2*s*t + s^2 + t                                                                                                                                
877.91/297.41	                                                 =  [Cons_sum(xi, k, Concat(s, t))]                                                                                                                    
877.91/297.41	                                                                                                                                                                                                       
877.91/297.41	                       [Concat(Concat(s, t), u)] =  s + 3*s*t + 2*s^2 + t + 2*s*u + 4*s*t*u + 2*s^2*u + 2*t*u + 5*s^2*t + 2*s^3 + 4*s^2*t^2 + 4*s^3*t + 2*s*t^2 + s^4 + t*s + 2*t^2*s + t*s^2 + t^2 + u
877.91/297.41	                                                 >= s + 2*s*t + 4*s*t*u + 2*s*t^2 + 2*s*u + s^2 + t + 2*t*u + t^2 + u                                                                                  
877.91/297.41	                                                 =  [Concat(s, Concat(t, u))]                                                                                                                          
877.91/297.41	                                                                                                                                                                                                       
877.91/297.41	
877.91/297.41	We return to the main proof.
877.91/297.41	
877.91/297.41	We are left with following problem, upon which TcT provides the
877.91/297.41	certificate YES(O(1),O(n^2)).
877.91/297.41	
877.91/297.41	Strict Trs:
877.91/297.41	  { Term_sub(Term_sub(m, s), t) -> Term_sub(m, Concat(s, t))
877.91/297.41	  , Term_sub(Term_inl(m), s) -> Term_inl(Term_sub(m, s))
877.91/297.41	  , Concat(Concat(s, t), u) -> Concat(s, Concat(t, u)) }
877.91/297.41	Weak Trs:
877.91/297.41	  { Term_sub(Case(m, xi, n), s) -> Frozen(m, Sum_sub(xi, s), n, s)
877.91/297.41	  , Term_sub(Term_app(m, n), s) ->
877.91/297.41	    Term_app(Term_sub(m, s), Term_sub(n, s))
877.91/297.41	  , Term_sub(Term_pair(m, n), s) ->
877.91/297.41	    Term_pair(Term_sub(m, s), Term_sub(n, s))
877.91/297.41	  , Term_sub(Term_inr(m), s) -> Term_inr(Term_sub(m, s))
877.91/297.41	  , Term_sub(Term_var(x), Id()) -> Term_var(x)
877.91/297.41	  , Term_sub(Term_var(x), Cons_usual(y, m, s)) -> m
877.91/297.41	  , Term_sub(Term_var(x), Cons_usual(y, m, s)) ->
877.91/297.41	    Term_sub(Term_var(x), s)
877.91/297.41	  , Term_sub(Term_var(x), Cons_sum(xi, k, s)) ->
877.91/297.41	    Term_sub(Term_var(x), s)
877.91/297.41	  , Frozen(m, Sum_constant(Left()), n, s) -> Term_sub(m, s)
877.91/297.41	  , Frozen(m, Sum_constant(Right()), n, s) -> Term_sub(n, s)
877.91/297.41	  , Frozen(m, Sum_term_var(xi), n, s) ->
877.91/297.41	    Case(Term_sub(m, s), xi, Term_sub(n, s))
877.91/297.41	  , Sum_sub(xi, Id()) -> Sum_term_var(xi)
877.91/297.41	  , Sum_sub(xi, Cons_usual(y, m, s)) -> Sum_sub(xi, s)
877.91/297.41	  , Sum_sub(xi, Cons_sum(psi, k, s)) -> Sum_sub(xi, s)
877.91/297.41	  , Sum_sub(xi, Cons_sum(psi, k, s)) -> Sum_constant(k)
877.91/297.41	  , Concat(Id(), s) -> s
877.91/297.41	  , Concat(Cons_usual(x, m, s), t) ->
877.91/297.41	    Cons_usual(x, Term_sub(m, t), Concat(s, t))
877.91/297.41	  , Concat(Cons_sum(xi, k, s), t) -> Cons_sum(xi, k, Concat(s, t)) }
877.91/297.41	Obligation:
877.91/297.41	  runtime complexity
877.91/297.41	Answer:
877.91/297.41	  YES(O(1),O(n^2))
877.91/297.41	
877.91/297.41	We use the processor 'polynomial interpretation' to orient
877.91/297.41	following rules strictly.
877.91/297.41	
877.91/297.41	Trs: { Term_sub(Term_inl(m), s) -> Term_inl(Term_sub(m, s)) }
877.91/297.41	
877.91/297.41	The induced complexity on above rules (modulo remaining rules) is
877.91/297.41	YES(?,O(n^2)) . These rules are moved into the corresponding weak
877.91/297.41	component(s).
877.91/297.41	
877.91/297.41	Sub-proof:
877.91/297.41	----------
877.91/297.41	  We consider the following typing:
877.91/297.41	  
877.91/297.41	    Term_sub :: (g,b) -> g
877.91/297.41	    Case :: (g,c,g) -> g
877.91/297.41	    Frozen :: (g,a,g,b) -> g
877.91/297.41	    Sum_sub :: (c,b) -> a
877.91/297.41	    Sum_constant :: d -> a
877.91/297.41	    Left :: d
877.91/297.41	    Right :: d
877.91/297.41	    Sum_term_var :: c -> a
877.91/297.41	    Term_app :: (g,g) -> g
877.91/297.41	    Term_pair :: (g,g) -> g
877.91/297.41	    Term_inl :: g -> g
877.91/297.41	    Term_inr :: g -> g
877.91/297.41	    Term_var :: e -> g
877.91/297.41	    Id :: b
877.91/297.41	    Cons_usual :: (f,g,b) -> b
877.91/297.41	    Cons_sum :: (h,d,b) -> b
877.91/297.41	    Concat :: (b,b) -> b
877.91/297.41	  
877.91/297.41	  The following argument positions are considered usable:
877.91/297.41	  
877.91/297.41	    Uargs(Term_sub) = {2}, Uargs(Case) = {1, 3},
877.91/297.41	    Uargs(Frozen) = {2, 4}, Uargs(Sum_sub) = {2},
877.91/297.41	    Uargs(Term_app) = {1, 2}, Uargs(Term_pair) = {1, 2},
877.91/297.41	    Uargs(Term_inl) = {1}, Uargs(Term_inr) = {1},
877.91/297.41	    Uargs(Cons_usual) = {2, 3}, Uargs(Cons_sum) = {3},
877.91/297.41	    Uargs(Concat) = {2}
877.91/297.41	  
877.91/297.41	  TcT has computed the following constructor-restricted
877.91/297.41	  typedpolynomial interpretation.
877.91/297.41	  
877.91/297.41	        [Term_sub](x1, x2) = x1 + x1*x2 + x1^2 + x2                                       
877.91/297.41	                                                                                          
877.91/297.41	        [Case](x1, x2, x3) = 2 + x1 + x3                                                  
877.91/297.41	                                                                                          
877.91/297.41	  [Frozen](x1, x2, x3, x4) = 2 + x1 + x1*x3 + x1*x4 + x1^2 + x2 + x3 + x3*x4 + x3^2 + 2*x4
877.91/297.41	                                                                                          
877.91/297.41	         [Sum_sub](x1, x2) = x2                                                           
877.91/297.41	                                                                                          
877.91/297.41	        [Sum_constant](x1) = 0                                                            
877.91/297.41	                                                                                          
877.91/297.41	                  [Left]() = 0                                                            
877.91/297.41	                                                                                          
877.91/297.41	                 [Right]() = 0                                                            
877.91/297.41	                                                                                          
877.91/297.41	        [Sum_term_var](x1) = 0                                                            
877.91/297.41	                                                                                          
877.91/297.41	        [Term_app](x1, x2) = 1 + x1 + x2                                                  
877.91/297.41	                                                                                          
877.91/297.41	       [Term_pair](x1, x2) = 2 + x1 + x2                                                  
877.91/297.41	                                                                                          
877.91/297.41	            [Term_inl](x1) = 2 + x1                                                       
877.91/297.41	                                                                                          
877.91/297.41	            [Term_inr](x1) = x1                                                           
877.91/297.41	                                                                                          
877.91/297.41	            [Term_var](x1) = 0                                                            
877.91/297.41	                                                                                          
877.91/297.41	                    [Id]() = 0                                                            
877.91/297.41	                                                                                          
877.91/297.41	  [Cons_usual](x1, x2, x3) = 2 + x2 + x3                                                  
877.91/297.41	                                                                                          
877.91/297.41	    [Cons_sum](x1, x2, x3) = x3                                                           
877.91/297.41	                                                                                          
877.91/297.41	          [Concat](x1, x2) = x1 + x1*x2 + x1^2 + x2                                       
877.91/297.41	                                                                                          
877.91/297.41	  
877.91/297.41	  This order satisfies the following ordering constraints.
877.91/297.41	  
877.91/297.41	                   [Term_sub(Term_sub(m, s), t)] =  m + 2*m*s + 2*m^2 + s + m*t + m*s*t + m^2*t + s*t + 3*m^2*s + 2*m^3 + m^2*s^2 + 2*m^3*s + m*s^2 + m^4 + s*m + s^2*m + s*m^2 + s^2 + t
877.91/297.41	                                                 >= m + m*s + m*s*t + m*s^2 + m*t + m^2 + s + s*t + s^2 + t                                                                              
877.91/297.41	                                                 =  [Term_sub(m, Concat(s, t))]                                                                                                          
877.91/297.41	                                                                                                                                                                                         
877.91/297.41	                   [Term_sub(Case(m, xi, n), s)] =  6 + 5*m + 5*n + 3*s + m*s + n*s + m^2 + m*n + n*m + n^2                                                                              
877.91/297.41	                                                 >  2 + m + m*n + m*s + m^2 + 3*s + n + n*s + n^2                                                                                        
877.91/297.41	                                                 =  [Frozen(m, Sum_sub(xi, s), n, s)]                                                                                                    
877.91/297.41	                                                                                                                                                                                         
877.91/297.41	                   [Term_sub(Term_app(m, n), s)] =  2 + 3*m + 3*n + 2*s + m*s + n*s + m^2 + m*n + n*m + n^2                                                                              
877.91/297.41	                                                 >  1 + m + m*s + m^2 + 2*s + n + n*s + n^2                                                                                              
877.91/297.41	                                                 =  [Term_app(Term_sub(m, s), Term_sub(n, s))]                                                                                           
877.91/297.41	                                                                                                                                                                                         
877.91/297.41	                  [Term_sub(Term_pair(m, n), s)] =  6 + 5*m + 5*n + 3*s + m*s + n*s + m^2 + m*n + n*m + n^2                                                                              
877.91/297.41	                                                 >  2 + m + m*s + m^2 + 2*s + n + n*s + n^2                                                                                              
877.91/297.41	                                                 =  [Term_pair(Term_sub(m, s), Term_sub(n, s))]                                                                                          
877.91/297.41	                                                                                                                                                                                         
877.91/297.41	                      [Term_sub(Term_inl(m), s)] =  6 + 5*m + 3*s + m*s + m^2                                                                                                            
877.91/297.41	                                                 >  2 + m + m*s + m^2 + s                                                                                                                
877.91/297.41	                                                 =  [Term_inl(Term_sub(m, s))]                                                                                                           
877.91/297.41	                                                                                                                                                                                         
877.91/297.41	                      [Term_sub(Term_inr(m), s)] =  m + m*s + m^2 + s                                                                                                                    
877.91/297.41	                                                 >= m + m*s + m^2 + s                                                                                                                    
877.91/297.41	                                                 =  [Term_inr(Term_sub(m, s))]                                                                                                           
877.91/297.41	                                                                                                                                                                                         
877.91/297.41	                   [Term_sub(Term_var(x), Id())] =                                                                                                                                       
877.91/297.41	                                                 >=                                                                                                                                      
877.91/297.41	                                                 =  [Term_var(x)]                                                                                                                        
877.91/297.41	                                                                                                                                                                                         
877.91/297.41	    [Term_sub(Term_var(x), Cons_usual(y, m, s))] =  2 + m + s                                                                                                                            
877.91/297.41	                                                 >  m                                                                                                                                    
877.91/297.41	                                                 =  [m]                                                                                                                                  
877.91/297.41	                                                                                                                                                                                         
877.91/297.41	    [Term_sub(Term_var(x), Cons_usual(y, m, s))] =  2 + m + s                                                                                                                            
877.91/297.41	                                                 >  s                                                                                                                                    
877.91/297.41	                                                 =  [Term_sub(Term_var(x), s)]                                                                                                           
877.91/297.41	                                                                                                                                                                                         
877.91/297.41	     [Term_sub(Term_var(x), Cons_sum(xi, k, s))] =  s                                                                                                                                    
877.91/297.41	                                                 >= s                                                                                                                                    
877.91/297.41	                                                 =  [Term_sub(Term_var(x), s)]                                                                                                           
877.91/297.41	                                                                                                                                                                                         
877.91/297.41	         [Frozen(m, Sum_constant(Left()), n, s)] =  2 + m + m*n + m*s + m^2 + n + n*s + n^2 + 2*s                                                                                        
877.91/297.41	                                                 >  m + m*s + m^2 + s                                                                                                                    
877.91/297.41	                                                 =  [Term_sub(m, s)]                                                                                                                     
877.91/297.41	                                                                                                                                                                                         
877.91/297.41	        [Frozen(m, Sum_constant(Right()), n, s)] =  2 + m + m*n + m*s + m^2 + n + n*s + n^2 + 2*s                                                                                        
877.91/297.41	                                                 >  n + n*s + n^2 + s                                                                                                                    
877.91/297.41	                                                 =  [Term_sub(n, s)]                                                                                                                     
877.91/297.41	                                                                                                                                                                                         
877.91/297.41	             [Frozen(m, Sum_term_var(xi), n, s)] =  2 + m + m*n + m*s + m^2 + n + n*s + n^2 + 2*s                                                                                        
877.91/297.41	                                                 >= 2 + m + m*s + m^2 + 2*s + n + n*s + n^2                                                                                              
877.91/297.41	                                                 =  [Case(Term_sub(m, s), xi, Term_sub(n, s))]                                                                                           
877.91/297.41	                                                                                                                                                                                         
877.91/297.41	                             [Sum_sub(xi, Id())] =                                                                                                                                       
877.91/297.41	                                                 >=                                                                                                                                      
877.91/297.41	                                                 =  [Sum_term_var(xi)]                                                                                                                   
877.91/297.41	                                                                                                                                                                                         
877.91/297.41	              [Sum_sub(xi, Cons_usual(y, m, s))] =  2 + m + s                                                                                                                            
877.91/297.41	                                                 >  s                                                                                                                                    
877.91/297.41	                                                 =  [Sum_sub(xi, s)]                                                                                                                     
877.91/297.41	                                                                                                                                                                                         
877.91/297.41	              [Sum_sub(xi, Cons_sum(psi, k, s))] =  s                                                                                                                                    
877.91/297.41	                                                 >= s                                                                                                                                    
877.91/297.41	                                                 =  [Sum_sub(xi, s)]                                                                                                                     
877.91/297.41	                                                                                                                                                                                         
877.91/297.41	              [Sum_sub(xi, Cons_sum(psi, k, s))] =  s                                                                                                                                    
877.91/297.41	                                                 >=                                                                                                                                      
877.91/297.42	                                                 =  [Sum_constant(k)]                                                                                                                    
877.91/297.42	                                                                                                                                                                                         
877.91/297.42	                               [Concat(Id(), s)] =  s                                                                                                                                    
877.91/297.42	                                                 >= s                                                                                                                                    
877.91/297.42	                                                 =  [s]                                                                                                                                  
877.91/297.42	                                                                                                                                                                                         
877.91/297.42	                [Concat(Cons_usual(x, m, s), t)] =  6 + 5*m + 5*s + 3*t + m*t + s*t + m^2 + m*s + s*m + s^2                                                                              
877.91/297.42	                                                 >  2 + m + m*t + m^2 + 2*t + s + s*t + s^2                                                                                              
877.91/297.42	                                                 =  [Cons_usual(x, Term_sub(m, t), Concat(s, t))]                                                                                        
877.91/297.42	                                                                                                                                                                                         
877.91/297.42	                 [Concat(Cons_sum(xi, k, s), t)] =  s + s*t + s^2 + t                                                                                                                    
877.91/297.42	                                                 >= s + s*t + s^2 + t                                                                                                                    
877.91/297.42	                                                 =  [Cons_sum(xi, k, Concat(s, t))]                                                                                                      
877.91/297.42	                                                                                                                                                                                         
877.91/297.42	                       [Concat(Concat(s, t), u)] =  s + 2*s*t + 2*s^2 + t + s*u + s*t*u + s^2*u + t*u + 3*s^2*t + 2*s^3 + s^2*t^2 + 2*s^3*t + s*t^2 + s^4 + t*s + t^2*s + t*s^2 + t^2 + u
877.91/297.42	                                                 >= s + s*t + s*t*u + s*t^2 + s*u + s^2 + t + t*u + t^2 + u                                                                              
877.91/297.42	                                                 =  [Concat(s, Concat(t, u))]                                                                                                            
877.91/297.42	                                                                                                                                                                                         
877.91/297.42	
877.91/297.42	We return to the main proof.
877.91/297.42	
877.91/297.42	We are left with following problem, upon which TcT provides the
877.91/297.42	certificate YES(O(1),O(n^2)).
877.91/297.42	
877.91/297.42	Strict Trs:
877.91/297.42	  { Term_sub(Term_sub(m, s), t) -> Term_sub(m, Concat(s, t))
877.91/297.42	  , Concat(Concat(s, t), u) -> Concat(s, Concat(t, u)) }
877.91/297.42	Weak Trs:
877.91/297.42	  { Term_sub(Case(m, xi, n), s) -> Frozen(m, Sum_sub(xi, s), n, s)
877.91/297.42	  , Term_sub(Term_app(m, n), s) ->
877.91/297.42	    Term_app(Term_sub(m, s), Term_sub(n, s))
877.91/297.42	  , Term_sub(Term_pair(m, n), s) ->
877.91/297.42	    Term_pair(Term_sub(m, s), Term_sub(n, s))
877.91/297.42	  , Term_sub(Term_inl(m), s) -> Term_inl(Term_sub(m, s))
877.91/297.42	  , Term_sub(Term_inr(m), s) -> Term_inr(Term_sub(m, s))
877.91/297.42	  , Term_sub(Term_var(x), Id()) -> Term_var(x)
877.91/297.42	  , Term_sub(Term_var(x), Cons_usual(y, m, s)) -> m
877.91/297.42	  , Term_sub(Term_var(x), Cons_usual(y, m, s)) ->
877.91/297.42	    Term_sub(Term_var(x), s)
877.91/297.42	  , Term_sub(Term_var(x), Cons_sum(xi, k, s)) ->
877.91/297.42	    Term_sub(Term_var(x), s)
877.91/297.42	  , Frozen(m, Sum_constant(Left()), n, s) -> Term_sub(m, s)
877.91/297.42	  , Frozen(m, Sum_constant(Right()), n, s) -> Term_sub(n, s)
877.91/297.42	  , Frozen(m, Sum_term_var(xi), n, s) ->
877.91/297.42	    Case(Term_sub(m, s), xi, Term_sub(n, s))
877.91/297.42	  , Sum_sub(xi, Id()) -> Sum_term_var(xi)
877.91/297.42	  , Sum_sub(xi, Cons_usual(y, m, s)) -> Sum_sub(xi, s)
877.91/297.42	  , Sum_sub(xi, Cons_sum(psi, k, s)) -> Sum_sub(xi, s)
877.91/297.42	  , Sum_sub(xi, Cons_sum(psi, k, s)) -> Sum_constant(k)
877.91/297.42	  , Concat(Id(), s) -> s
877.91/297.42	  , Concat(Cons_usual(x, m, s), t) ->
877.91/297.42	    Cons_usual(x, Term_sub(m, t), Concat(s, t))
877.91/297.42	  , Concat(Cons_sum(xi, k, s), t) -> Cons_sum(xi, k, Concat(s, t)) }
877.91/297.42	Obligation:
877.91/297.42	  runtime complexity
877.91/297.42	Answer:
877.91/297.42	  YES(O(1),O(n^2))
877.91/297.42	
877.91/297.42	We use the processor 'polynomial interpretation' to orient
877.91/297.42	following rules strictly.
877.91/297.42	
877.91/297.42	Trs: { Term_sub(Term_sub(m, s), t) -> Term_sub(m, Concat(s, t)) }
877.91/297.42	
877.91/297.42	The induced complexity on above rules (modulo remaining rules) is
877.91/297.42	YES(?,O(n^2)) . These rules are moved into the corresponding weak
877.91/297.42	component(s).
877.91/297.42	
877.91/297.42	Sub-proof:
877.91/297.42	----------
877.91/297.42	  We consider the following typing:
877.91/297.42	  
877.91/297.42	    Term_sub :: (g,b) -> g
877.91/297.42	    Case :: (g,c,g) -> g
877.91/297.42	    Frozen :: (g,a,g,b) -> g
877.91/297.42	    Sum_sub :: (c,b) -> a
877.91/297.42	    Sum_constant :: d -> a
877.91/297.42	    Left :: d
877.91/297.42	    Right :: d
877.91/297.42	    Sum_term_var :: c -> a
877.91/297.42	    Term_app :: (g,g) -> g
877.91/297.42	    Term_pair :: (g,g) -> g
877.91/297.42	    Term_inl :: g -> g
877.91/297.42	    Term_inr :: g -> g
877.91/297.42	    Term_var :: e -> g
877.91/297.42	    Id :: b
877.91/297.42	    Cons_usual :: (f,g,b) -> b
877.91/297.42	    Cons_sum :: (h,d,b) -> b
877.91/297.42	    Concat :: (b,b) -> b
877.91/297.42	  
877.91/297.42	  The following argument positions are considered usable:
877.91/297.42	  
877.91/297.42	    Uargs(Term_sub) = {2}, Uargs(Case) = {1, 3},
877.91/297.42	    Uargs(Frozen) = {2, 4}, Uargs(Sum_sub) = {2},
877.91/297.42	    Uargs(Term_app) = {1, 2}, Uargs(Term_pair) = {1, 2},
877.91/297.42	    Uargs(Term_inl) = {1}, Uargs(Term_inr) = {1},
877.91/297.42	    Uargs(Cons_usual) = {2, 3}, Uargs(Cons_sum) = {3},
877.91/297.42	    Uargs(Concat) = {2}
877.91/297.42	  
877.91/297.42	  TcT has computed the following constructor-restricted
877.91/297.42	  typedpolynomial interpretation.
877.91/297.42	  
877.91/297.42	        [Term_sub](x1, x2) = 1 + x1 + x1*x2 + x1^2 + x2                                   
877.91/297.42	                                                                                          
877.91/297.42	        [Case](x1, x2, x3) = 2 + x1 + x3                                                  
877.91/297.42	                                                                                          
877.91/297.42	  [Frozen](x1, x2, x3, x4) = 3 + x1 + x1*x3 + x1*x4 + x1^2 + x2 + x3 + x3*x4 + x3^2 + 2*x4
877.91/297.42	                                                                                          
877.91/297.42	         [Sum_sub](x1, x2) = 1 + x2                                                       
877.91/297.42	                                                                                          
877.91/297.42	        [Sum_constant](x1) = 1                                                            
877.91/297.42	                                                                                          
877.91/297.42	                  [Left]() = 0                                                            
877.91/297.42	                                                                                          
877.91/297.42	                 [Right]() = 0                                                            
877.91/297.42	                                                                                          
877.91/297.42	        [Sum_term_var](x1) = 1                                                            
877.91/297.42	                                                                                          
877.91/297.42	        [Term_app](x1, x2) = 1 + x1 + x2                                                  
877.91/297.42	                                                                                          
877.91/297.42	       [Term_pair](x1, x2) = 1 + x1 + x2                                                  
877.91/297.42	                                                                                          
877.91/297.42	            [Term_inl](x1) = x1                                                           
877.91/297.42	                                                                                          
877.91/297.42	            [Term_inr](x1) = x1                                                           
877.91/297.42	                                                                                          
877.91/297.42	            [Term_var](x1) = 0                                                            
877.91/297.42	                                                                                          
877.91/297.42	                    [Id]() = 0                                                            
877.91/297.42	                                                                                          
877.91/297.42	  [Cons_usual](x1, x2, x3) = 2 + x2 + x3                                                  
877.91/297.42	                                                                                          
877.91/297.42	    [Cons_sum](x1, x2, x3) = x3                                                           
877.91/297.42	                                                                                          
877.91/297.42	          [Concat](x1, x2) = x1 + x1*x2 + x1^2 + x2                                       
877.91/297.42	                                                                                          
877.91/297.42	  
877.91/297.42	  This order satisfies the following ordering constraints.
877.91/297.42	  
877.91/297.42	                   [Term_sub(Term_sub(m, s), t)] =  3 + 3*m + 4*m*s + 4*m^2 + 3*s + 2*t + m*t + m*s*t + m^2*t + s*t + 3*m^2*s + 2*m^3 + m^2*s^2 + 2*m^3*s + m*s^2 + m^4 + s*m + s^2*m + s*m^2 + s^2
877.91/297.42	                                                 >  1 + m + m*s + m*s*t + m*s^2 + m*t + m^2 + s + s*t + s^2 + t                                                                                    
877.91/297.42	                                                 =  [Term_sub(m, Concat(s, t))]                                                                                                                    
877.91/297.42	                                                                                                                                                                                                   
877.91/297.42	                   [Term_sub(Case(m, xi, n), s)] =  7 + 5*m + 5*n + 3*s + m*s + n*s + m^2 + m*n + n*m + n^2                                                                                        
877.91/297.42	                                                 >  4 + m + m*n + m*s + m^2 + 3*s + n + n*s + n^2                                                                                                  
877.91/297.42	                                                 =  [Frozen(m, Sum_sub(xi, s), n, s)]                                                                                                              
877.91/297.42	                                                                                                                                                                                                   
877.91/297.42	                   [Term_sub(Term_app(m, n), s)] =  3 + 3*m + 3*n + 2*s + m*s + n*s + m^2 + m*n + n*m + n^2                                                                                        
877.91/297.42	                                                 >= 3 + m + m*s + m^2 + 2*s + n + n*s + n^2                                                                                                        
877.91/297.42	                                                 =  [Term_app(Term_sub(m, s), Term_sub(n, s))]                                                                                                     
877.91/297.42	                                                                                                                                                                                                   
877.91/297.42	                  [Term_sub(Term_pair(m, n), s)] =  3 + 3*m + 3*n + 2*s + m*s + n*s + m^2 + m*n + n*m + n^2                                                                                        
877.91/297.42	                                                 >= 3 + m + m*s + m^2 + 2*s + n + n*s + n^2                                                                                                        
877.91/297.42	                                                 =  [Term_pair(Term_sub(m, s), Term_sub(n, s))]                                                                                                    
877.91/297.42	                                                                                                                                                                                                   
877.91/297.42	                      [Term_sub(Term_inl(m), s)] =  1 + m + m*s + m^2 + s                                                                                                                          
877.91/297.42	                                                 >= 1 + m + m*s + m^2 + s                                                                                                                          
877.91/297.42	                                                 =  [Term_inl(Term_sub(m, s))]                                                                                                                     
877.91/297.42	                                                                                                                                                                                                   
877.91/297.42	                      [Term_sub(Term_inr(m), s)] =  1 + m + m*s + m^2 + s                                                                                                                          
877.91/297.42	                                                 >= 1 + m + m*s + m^2 + s                                                                                                                          
877.91/297.42	                                                 =  [Term_inr(Term_sub(m, s))]                                                                                                                     
877.91/297.42	                                                                                                                                                                                                   
877.91/297.42	                   [Term_sub(Term_var(x), Id())] =  1                                                                                                                                              
877.91/297.42	                                                 >                                                                                                                                                 
877.91/297.42	                                                 =  [Term_var(x)]                                                                                                                                  
877.91/297.42	                                                                                                                                                                                                   
877.91/297.42	    [Term_sub(Term_var(x), Cons_usual(y, m, s))] =  3 + m + s                                                                                                                                      
877.91/297.42	                                                 >  m                                                                                                                                              
877.91/297.42	                                                 =  [m]                                                                                                                                            
877.91/297.42	                                                                                                                                                                                                   
877.91/297.42	    [Term_sub(Term_var(x), Cons_usual(y, m, s))] =  3 + m + s                                                                                                                                      
877.91/297.42	                                                 >  1 + s                                                                                                                                          
877.91/297.42	                                                 =  [Term_sub(Term_var(x), s)]                                                                                                                     
877.91/297.42	                                                                                                                                                                                                   
877.91/297.42	     [Term_sub(Term_var(x), Cons_sum(xi, k, s))] =  1 + s                                                                                                                                          
877.91/297.42	                                                 >= 1 + s                                                                                                                                          
877.91/297.42	                                                 =  [Term_sub(Term_var(x), s)]                                                                                                                     
877.91/297.42	                                                                                                                                                                                                   
877.91/297.42	         [Frozen(m, Sum_constant(Left()), n, s)] =  4 + m + m*n + m*s + m^2 + n + n*s + n^2 + 2*s                                                                                                  
877.91/297.42	                                                 >  1 + m + m*s + m^2 + s                                                                                                                          
877.91/297.42	                                                 =  [Term_sub(m, s)]                                                                                                                               
877.91/297.42	                                                                                                                                                                                                   
877.91/297.42	        [Frozen(m, Sum_constant(Right()), n, s)] =  4 + m + m*n + m*s + m^2 + n + n*s + n^2 + 2*s                                                                                                  
877.91/297.42	                                                 >  1 + n + n*s + n^2 + s                                                                                                                          
877.91/297.42	                                                 =  [Term_sub(n, s)]                                                                                                                               
877.91/297.42	                                                                                                                                                                                                   
877.91/297.42	             [Frozen(m, Sum_term_var(xi), n, s)] =  4 + m + m*n + m*s + m^2 + n + n*s + n^2 + 2*s                                                                                                  
877.91/297.42	                                                 >= 4 + m + m*s + m^2 + 2*s + n + n*s + n^2                                                                                                        
877.91/297.42	                                                 =  [Case(Term_sub(m, s), xi, Term_sub(n, s))]                                                                                                     
877.91/297.42	                                                                                                                                                                                                   
877.91/297.42	                             [Sum_sub(xi, Id())] =  1                                                                                                                                              
877.91/297.42	                                                 >= 1                                                                                                                                              
877.91/297.42	                                                 =  [Sum_term_var(xi)]                                                                                                                             
877.91/297.42	                                                                                                                                                                                                   
877.91/297.42	              [Sum_sub(xi, Cons_usual(y, m, s))] =  3 + m + s                                                                                                                                      
877.91/297.42	                                                 >  1 + s                                                                                                                                          
877.91/297.42	                                                 =  [Sum_sub(xi, s)]                                                                                                                               
877.91/297.42	                                                                                                                                                                                                   
877.91/297.42	              [Sum_sub(xi, Cons_sum(psi, k, s))] =  1 + s                                                                                                                                          
877.91/297.42	                                                 >= 1 + s                                                                                                                                          
877.91/297.42	                                                 =  [Sum_sub(xi, s)]                                                                                                                               
877.91/297.42	                                                                                                                                                                                                   
877.91/297.42	              [Sum_sub(xi, Cons_sum(psi, k, s))] =  1 + s                                                                                                                                          
877.91/297.42	                                                 >= 1                                                                                                                                              
877.91/297.42	                                                 =  [Sum_constant(k)]                                                                                                                              
877.91/297.42	                                                                                                                                                                                                   
877.91/297.42	                               [Concat(Id(), s)] =  s                                                                                                                                              
877.91/297.42	                                                 >= s                                                                                                                                              
877.91/297.42	                                                 =  [s]                                                                                                                                            
877.91/297.42	                                                                                                                                                                                                   
877.91/297.42	                [Concat(Cons_usual(x, m, s), t)] =  6 + 5*m + 5*s + 3*t + m*t + s*t + m^2 + m*s + s*m + s^2                                                                                        
877.91/297.42	                                                 >  3 + m + m*t + m^2 + 2*t + s + s*t + s^2                                                                                                        
877.91/297.42	                                                 =  [Cons_usual(x, Term_sub(m, t), Concat(s, t))]                                                                                                  
877.91/297.42	                                                                                                                                                                                                   
877.91/297.42	                 [Concat(Cons_sum(xi, k, s), t)] =  s + s*t + s^2 + t                                                                                                                              
877.91/297.42	                                                 >= s + s*t + s^2 + t                                                                                                                              
877.91/297.42	                                                 =  [Cons_sum(xi, k, Concat(s, t))]                                                                                                                
877.91/297.42	                                                                                                                                                                                                   
877.91/297.42	                       [Concat(Concat(s, t), u)] =  s + 2*s*t + 2*s^2 + t + s*u + s*t*u + s^2*u + t*u + 3*s^2*t + 2*s^3 + s^2*t^2 + 2*s^3*t + s*t^2 + s^4 + t*s + t^2*s + t*s^2 + t^2 + u          
877.91/297.42	                                                 >= s + s*t + s*t*u + s*t^2 + s*u + s^2 + t + t*u + t^2 + u                                                                                        
877.91/297.42	                                                 =  [Concat(s, Concat(t, u))]                                                                                                                      
877.91/297.42	                                                                                                                                                                                                   
877.91/297.42	
877.91/297.42	We return to the main proof.
877.91/297.42	
877.91/297.42	We are left with following problem, upon which TcT provides the
877.91/297.42	certificate YES(O(1),O(n^2)).
877.91/297.42	
877.91/297.42	Strict Trs: { Concat(Concat(s, t), u) -> Concat(s, Concat(t, u)) }
877.91/297.42	Weak Trs:
877.91/297.42	  { Term_sub(Term_sub(m, s), t) -> Term_sub(m, Concat(s, t))
877.91/297.42	  , Term_sub(Case(m, xi, n), s) -> Frozen(m, Sum_sub(xi, s), n, s)
877.91/297.42	  , Term_sub(Term_app(m, n), s) ->
877.91/297.42	    Term_app(Term_sub(m, s), Term_sub(n, s))
877.91/297.42	  , Term_sub(Term_pair(m, n), s) ->
877.91/297.42	    Term_pair(Term_sub(m, s), Term_sub(n, s))
877.91/297.42	  , Term_sub(Term_inl(m), s) -> Term_inl(Term_sub(m, s))
877.91/297.42	  , Term_sub(Term_inr(m), s) -> Term_inr(Term_sub(m, s))
877.91/297.42	  , Term_sub(Term_var(x), Id()) -> Term_var(x)
877.91/297.42	  , Term_sub(Term_var(x), Cons_usual(y, m, s)) -> m
877.91/297.42	  , Term_sub(Term_var(x), Cons_usual(y, m, s)) ->
877.91/297.42	    Term_sub(Term_var(x), s)
877.91/297.42	  , Term_sub(Term_var(x), Cons_sum(xi, k, s)) ->
877.91/297.42	    Term_sub(Term_var(x), s)
877.91/297.42	  , Frozen(m, Sum_constant(Left()), n, s) -> Term_sub(m, s)
877.91/297.42	  , Frozen(m, Sum_constant(Right()), n, s) -> Term_sub(n, s)
877.91/297.42	  , Frozen(m, Sum_term_var(xi), n, s) ->
877.91/297.42	    Case(Term_sub(m, s), xi, Term_sub(n, s))
877.91/297.42	  , Sum_sub(xi, Id()) -> Sum_term_var(xi)
877.91/297.42	  , Sum_sub(xi, Cons_usual(y, m, s)) -> Sum_sub(xi, s)
877.91/297.42	  , Sum_sub(xi, Cons_sum(psi, k, s)) -> Sum_sub(xi, s)
877.91/297.42	  , Sum_sub(xi, Cons_sum(psi, k, s)) -> Sum_constant(k)
877.91/297.42	  , Concat(Id(), s) -> s
877.91/297.42	  , Concat(Cons_usual(x, m, s), t) ->
877.91/297.42	    Cons_usual(x, Term_sub(m, t), Concat(s, t))
877.91/297.42	  , Concat(Cons_sum(xi, k, s), t) -> Cons_sum(xi, k, Concat(s, t)) }
877.91/297.42	Obligation:
877.91/297.42	  runtime complexity
877.91/297.42	Answer:
877.91/297.42	  YES(O(1),O(n^2))
877.91/297.42	
877.91/297.42	We use the processor 'polynomial interpretation' to orient
877.91/297.42	following rules strictly.
877.91/297.42	
877.91/297.42	Trs: { Concat(Concat(s, t), u) -> Concat(s, Concat(t, u)) }
877.91/297.42	
877.91/297.42	The induced complexity on above rules (modulo remaining rules) is
877.91/297.42	YES(?,O(n^2)) . These rules are moved into the corresponding weak
877.91/297.42	component(s).
877.91/297.42	
877.91/297.42	Sub-proof:
877.91/297.42	----------
877.91/297.42	  We consider the following typing:
877.91/297.42	  
877.91/297.42	    Term_sub :: (g,b) -> g
877.91/297.42	    Case :: (g,c,g) -> g
877.91/297.42	    Frozen :: (g,a,g,b) -> g
877.91/297.42	    Sum_sub :: (c,b) -> a
877.91/297.42	    Sum_constant :: d -> a
877.91/297.42	    Left :: d
877.91/297.42	    Right :: d
877.91/297.42	    Sum_term_var :: c -> a
877.91/297.42	    Term_app :: (g,g) -> g
877.91/297.42	    Term_pair :: (g,g) -> g
877.91/297.42	    Term_inl :: g -> g
877.91/297.42	    Term_inr :: g -> g
877.91/297.42	    Term_var :: e -> g
877.91/297.42	    Id :: b
877.91/297.42	    Cons_usual :: (f,g,b) -> b
877.91/297.42	    Cons_sum :: (h,d,b) -> b
877.91/297.42	    Concat :: (b,b) -> b
877.91/297.42	  
877.91/297.42	  The following argument positions are considered usable:
877.91/297.42	  
877.91/297.42	    Uargs(Term_sub) = {2}, Uargs(Case) = {1, 3},
877.91/297.42	    Uargs(Frozen) = {2, 4}, Uargs(Sum_sub) = {2},
877.91/297.42	    Uargs(Term_app) = {1, 2}, Uargs(Term_pair) = {1, 2},
877.91/297.42	    Uargs(Term_inl) = {1}, Uargs(Term_inr) = {1},
877.91/297.42	    Uargs(Cons_usual) = {2, 3}, Uargs(Cons_sum) = {3},
877.91/297.42	    Uargs(Concat) = {2}
877.91/297.42	  
877.91/297.42	  TcT has computed the following constructor-restricted
877.91/297.42	  typedpolynomial interpretation.
877.91/297.42	  
877.91/297.42	        [Term_sub](x1, x2) = 1 + 2*x1 + 2*x1*x2 + x2                        
877.91/297.42	                                                                            
877.91/297.42	        [Case](x1, x2, x3) = 2 + x1 + x3                                    
877.91/297.42	                                                                            
877.91/297.42	  [Frozen](x1, x2, x3, x4) = 3 + 2*x1 + 2*x1*x4 + x2 + 2*x3 + 2*x3*x4 + 2*x4
877.91/297.42	                                                                            
877.91/297.42	         [Sum_sub](x1, x2) = 1 + x2                                         
877.91/297.42	                                                                            
877.91/297.42	        [Sum_constant](x1) = 0                                              
877.91/297.42	                                                                            
877.91/297.42	                  [Left]() = 0                                              
877.91/297.42	                                                                            
877.91/297.42	                 [Right]() = 0                                              
877.91/297.42	                                                                            
877.91/297.42	        [Sum_term_var](x1) = 1                                              
877.91/297.42	                                                                            
877.91/297.42	        [Term_app](x1, x2) = 1 + x1 + x2                                    
877.91/297.42	                                                                            
877.91/297.42	       [Term_pair](x1, x2) = 1 + x1 + x2                                    
877.91/297.42	                                                                            
877.91/297.42	            [Term_inl](x1) = x1                                             
877.91/297.42	                                                                            
877.91/297.42	            [Term_inr](x1) = 2 + x1                                         
877.91/297.42	                                                                            
877.91/297.42	            [Term_var](x1) = 0                                              
877.91/297.42	                                                                            
877.91/297.42	                    [Id]() = 0                                              
877.91/297.42	                                                                            
877.91/297.42	  [Cons_usual](x1, x2, x3) = 1 + x2 + x3                                    
877.91/297.42	                                                                            
877.91/297.42	    [Cons_sum](x1, x2, x3) = x3                                             
877.91/297.42	                                                                            
877.91/297.42	          [Concat](x1, x2) = 1 + 2*x1 + 2*x1*x2 + x2                        
877.91/297.42	                                                                            
877.91/297.42	  
877.91/297.42	  This order satisfies the following ordering constraints.
877.91/297.42	  
877.91/297.42	                   [Term_sub(Term_sub(m, s), t)] =  3 + 4*m + 4*m*s + 2*s + 3*t + 4*m*t + 4*m*s*t + 2*s*t
877.91/297.42	                                                 >  2 + 4*m + 4*m*s + 4*m*s*t + 2*m*t + 2*s + 2*s*t + t  
877.91/297.42	                                                 =  [Term_sub(m, Concat(s, t))]                          
877.91/297.42	                                                                                                         
877.91/297.42	                   [Term_sub(Case(m, xi, n), s)] =  5 + 2*m + 2*n + 5*s + 2*m*s + 2*n*s                  
877.91/297.42	                                                 >  4 + 2*m + 2*m*s + 3*s + 2*n + 2*n*s                  
877.91/297.42	                                                 =  [Frozen(m, Sum_sub(xi, s), n, s)]                    
877.91/297.42	                                                                                                         
877.91/297.42	                   [Term_sub(Term_app(m, n), s)] =  3 + 2*m + 2*n + 3*s + 2*m*s + 2*n*s                  
877.91/297.42	                                                 >= 3 + 2*m + 2*m*s + 2*s + 2*n + 2*n*s                  
877.91/297.42	                                                 =  [Term_app(Term_sub(m, s), Term_sub(n, s))]           
877.91/297.42	                                                                                                         
877.91/297.42	                  [Term_sub(Term_pair(m, n), s)] =  3 + 2*m + 2*n + 3*s + 2*m*s + 2*n*s                  
877.91/297.42	                                                 >= 3 + 2*m + 2*m*s + 2*s + 2*n + 2*n*s                  
877.91/297.42	                                                 =  [Term_pair(Term_sub(m, s), Term_sub(n, s))]          
877.91/297.42	                                                                                                         
877.91/297.42	                      [Term_sub(Term_inl(m), s)] =  1 + 2*m + 2*m*s + s                                  
877.91/297.42	                                                 >= 1 + 2*m + 2*m*s + s                                  
877.91/297.42	                                                 =  [Term_inl(Term_sub(m, s))]                           
877.91/297.42	                                                                                                         
877.91/297.42	                      [Term_sub(Term_inr(m), s)] =  5 + 2*m + 5*s + 2*m*s                                
877.91/297.42	                                                 >  3 + 2*m + 2*m*s + s                                  
877.91/297.42	                                                 =  [Term_inr(Term_sub(m, s))]                           
877.91/297.42	                                                                                                         
877.91/297.42	                   [Term_sub(Term_var(x), Id())] =  1                                                    
877.91/297.42	                                                 >                                                       
877.91/297.42	                                                 =  [Term_var(x)]                                        
877.91/297.42	                                                                                                         
877.91/297.42	    [Term_sub(Term_var(x), Cons_usual(y, m, s))] =  2 + m + s                                            
877.91/297.42	                                                 >  m                                                    
877.91/297.42	                                                 =  [m]                                                  
877.91/297.42	                                                                                                         
877.91/297.42	    [Term_sub(Term_var(x), Cons_usual(y, m, s))] =  2 + m + s                                            
877.91/297.42	                                                 >  1 + s                                                
877.91/297.42	                                                 =  [Term_sub(Term_var(x), s)]                           
877.91/297.42	                                                                                                         
877.91/297.42	     [Term_sub(Term_var(x), Cons_sum(xi, k, s))] =  1 + s                                                
877.91/297.42	                                                 >= 1 + s                                                
877.91/297.42	                                                 =  [Term_sub(Term_var(x), s)]                           
877.91/297.42	                                                                                                         
877.91/297.42	         [Frozen(m, Sum_constant(Left()), n, s)] =  3 + 2*m + 2*m*s + 2*n + 2*n*s + 2*s                  
877.91/297.42	                                                 >  1 + 2*m + 2*m*s + s                                  
877.91/297.42	                                                 =  [Term_sub(m, s)]                                     
877.91/297.42	                                                                                                         
877.91/297.42	        [Frozen(m, Sum_constant(Right()), n, s)] =  3 + 2*m + 2*m*s + 2*n + 2*n*s + 2*s                  
877.91/297.42	                                                 >  1 + 2*n + 2*n*s + s                                  
877.91/297.42	                                                 =  [Term_sub(n, s)]                                     
877.91/297.42	                                                                                                         
877.91/297.42	             [Frozen(m, Sum_term_var(xi), n, s)] =  4 + 2*m + 2*m*s + 2*n + 2*n*s + 2*s                  
877.91/297.42	                                                 >= 4 + 2*m + 2*m*s + 2*s + 2*n + 2*n*s                  
877.91/297.42	                                                 =  [Case(Term_sub(m, s), xi, Term_sub(n, s))]           
877.91/297.42	                                                                                                         
877.91/297.42	                             [Sum_sub(xi, Id())] =  1                                                    
877.91/297.42	                                                 >= 1                                                    
877.91/297.42	                                                 =  [Sum_term_var(xi)]                                   
877.91/297.42	                                                                                                         
877.91/297.42	              [Sum_sub(xi, Cons_usual(y, m, s))] =  2 + m + s                                            
877.91/297.42	                                                 >  1 + s                                                
877.91/297.42	                                                 =  [Sum_sub(xi, s)]                                     
877.91/297.42	                                                                                                         
877.91/297.42	              [Sum_sub(xi, Cons_sum(psi, k, s))] =  1 + s                                                
877.91/297.42	                                                 >= 1 + s                                                
877.91/297.42	                                                 =  [Sum_sub(xi, s)]                                     
877.91/297.42	                                                                                                         
877.91/297.42	              [Sum_sub(xi, Cons_sum(psi, k, s))] =  1 + s                                                
877.91/297.42	                                                 >                                                       
877.91/297.42	                                                 =  [Sum_constant(k)]                                    
877.91/297.42	                                                                                                         
877.91/297.42	                               [Concat(Id(), s)] =  1 + s                                                
877.91/297.42	                                                 >  s                                                    
877.91/297.42	                                                 =  [s]                                                  
877.91/297.42	                                                                                                         
877.91/297.42	                [Concat(Cons_usual(x, m, s), t)] =  3 + 2*m + 2*s + 3*t + 2*m*t + 2*s*t                  
877.91/297.42	                                                 >= 3 + 2*m + 2*m*t + 2*t + 2*s + 2*s*t                  
877.91/297.42	                                                 =  [Cons_usual(x, Term_sub(m, t), Concat(s, t))]        
877.91/297.42	                                                                                                         
877.91/297.42	                 [Concat(Cons_sum(xi, k, s), t)] =  1 + 2*s + 2*s*t + t                                  
877.91/297.42	                                                 >= 1 + 2*s + 2*s*t + t                                  
877.91/297.42	                                                 =  [Cons_sum(xi, k, Concat(s, t))]                      
877.91/297.42	                                                                                                         
877.91/297.42	                       [Concat(Concat(s, t), u)] =  3 + 4*s + 4*s*t + 2*t + 3*u + 4*s*u + 4*s*t*u + 2*t*u
877.91/297.42	                                                 >  2 + 4*s + 4*s*t + 4*s*t*u + 2*s*u + 2*t + 2*t*u + u  
877.91/297.42	                                                 =  [Concat(s, Concat(t, u))]                            
877.91/297.42	                                                                                                         
877.91/297.42	
877.91/297.42	We return to the main proof.
877.91/297.42	
877.91/297.42	We are left with following problem, upon which TcT provides the
877.91/297.42	certificate YES(O(1),O(1)).
877.91/297.42	
877.91/297.42	Weak Trs:
877.91/297.42	  { Term_sub(Term_sub(m, s), t) -> Term_sub(m, Concat(s, t))
877.91/297.42	  , Term_sub(Case(m, xi, n), s) -> Frozen(m, Sum_sub(xi, s), n, s)
877.91/297.42	  , Term_sub(Term_app(m, n), s) ->
877.91/297.42	    Term_app(Term_sub(m, s), Term_sub(n, s))
877.91/297.42	  , Term_sub(Term_pair(m, n), s) ->
877.91/297.42	    Term_pair(Term_sub(m, s), Term_sub(n, s))
877.91/297.42	  , Term_sub(Term_inl(m), s) -> Term_inl(Term_sub(m, s))
877.91/297.42	  , Term_sub(Term_inr(m), s) -> Term_inr(Term_sub(m, s))
877.91/297.42	  , Term_sub(Term_var(x), Id()) -> Term_var(x)
877.91/297.42	  , Term_sub(Term_var(x), Cons_usual(y, m, s)) -> m
877.91/297.42	  , Term_sub(Term_var(x), Cons_usual(y, m, s)) ->
877.91/297.42	    Term_sub(Term_var(x), s)
877.91/297.42	  , Term_sub(Term_var(x), Cons_sum(xi, k, s)) ->
877.91/297.42	    Term_sub(Term_var(x), s)
877.91/297.42	  , Frozen(m, Sum_constant(Left()), n, s) -> Term_sub(m, s)
877.91/297.42	  , Frozen(m, Sum_constant(Right()), n, s) -> Term_sub(n, s)
877.91/297.42	  , Frozen(m, Sum_term_var(xi), n, s) ->
877.91/297.42	    Case(Term_sub(m, s), xi, Term_sub(n, s))
877.91/297.42	  , Sum_sub(xi, Id()) -> Sum_term_var(xi)
877.91/297.42	  , Sum_sub(xi, Cons_usual(y, m, s)) -> Sum_sub(xi, s)
877.91/297.42	  , Sum_sub(xi, Cons_sum(psi, k, s)) -> Sum_sub(xi, s)
877.91/297.42	  , Sum_sub(xi, Cons_sum(psi, k, s)) -> Sum_constant(k)
877.91/297.42	  , Concat(Id(), s) -> s
877.91/297.42	  , Concat(Cons_usual(x, m, s), t) ->
877.91/297.42	    Cons_usual(x, Term_sub(m, t), Concat(s, t))
877.91/297.42	  , Concat(Cons_sum(xi, k, s), t) -> Cons_sum(xi, k, Concat(s, t))
877.91/297.42	  , Concat(Concat(s, t), u) -> Concat(s, Concat(t, u)) }
877.91/297.42	Obligation:
877.91/297.42	  runtime complexity
877.91/297.42	Answer:
877.91/297.42	  YES(O(1),O(1))
877.91/297.42	
877.91/297.42	Empty rules are trivially bounded
877.91/297.42	
877.91/297.42	Hurray, we answered YES(O(1),O(n^2))
878.16/297.65	EOF