YES(O(1),O(n^6))
198.54/60.03	YES(O(1),O(n^6))
198.54/60.03	
198.54/60.03	We are left with following problem, upon which TcT provides the
198.54/60.03	certificate YES(O(1),O(n^6)).
198.54/60.03	
198.54/60.03	Strict Trs:
198.54/60.03	  { .(y, .(i(y), z)) -> z
198.54/60.03	  , .(x, 1()) -> x
198.54/60.03	  , .(x, i(x)) -> 1()
198.54/60.03	  , .(.(x, y), z) -> .(x, .(y, z))
198.54/60.03	  , .(1(), x) -> x
198.54/60.03	  , .(i(x), x) -> 1()
198.54/60.03	  , .(i(y), .(y, z)) -> z
198.54/60.03	  , i(.(x, y)) -> .(i(y), i(x))
198.54/60.03	  , i(1()) -> 1()
198.54/60.03	  , i(i(x)) -> x }
198.54/60.03	Obligation:
198.54/60.03	  derivational complexity
198.54/60.03	Answer:
198.54/60.03	  YES(O(1),O(n^6))
198.54/60.03	
198.54/60.03	We use the processor 'matrix interpretation of dimension 2' to
198.54/60.03	orient following rules strictly.
198.54/60.03	
198.54/60.03	Trs:
198.54/60.03	  { .(y, .(i(y), z)) -> z
198.54/60.03	  , .(x, 1()) -> x
198.54/60.03	  , .(x, i(x)) -> 1()
198.54/60.03	  , .(1(), x) -> x
198.54/60.03	  , .(i(x), x) -> 1()
198.54/60.03	  , .(i(y), .(y, z)) -> z
198.54/60.03	  , i(.(x, y)) -> .(i(y), i(x))
198.54/60.03	  , i(1()) -> 1()
198.54/60.03	  , i(i(x)) -> x }
198.54/60.03	
198.54/60.03	The induced complexity on above rules (modulo remaining rules) is
198.54/60.03	YES(?,O(n^2)) . These rules are removed from the problem. Note that
198.54/60.03	none of the weakly oriented rules is size-increasing. The overall
198.54/60.03	complexity is obtained by composition .
198.54/60.03	
198.54/60.03	Sub-proof:
198.54/60.03	----------
198.54/60.03	  TcT has computed the following triangular matrix interpretation.
198.54/60.03	  
198.54/60.03	    [.](x1, x2) = [1 0] x1 + [1 0] x2 + [2]
198.54/60.03	                  [0 1]      [0 1]      [1]
198.54/60.03	                                           
198.54/60.03	            [1] = [0]                      
198.54/60.03	                  [0]                      
198.54/60.03	                                           
198.54/60.03	        [i](x1) = [1 2] x1 + [1]           
198.54/60.03	                  [0 1]      [0]           
198.54/60.03	  
198.54/60.03	  The order satisfies the following ordering constraints:
198.54/60.03	  
198.54/60.03	    [.(y, .(i(y), z))] =  [2 2] y + [1 0] z + [5]          
198.54/60.03	                          [0 2]     [0 1]     [2]          
198.54/60.03	                       >  [1 0] z + [0]                    
198.54/60.03	                          [0 1]     [0]                    
198.54/60.03	                       =  [z]                              
198.54/60.03	                                                           
198.54/60.03	           [.(x, 1())] =  [1 0] x + [2]                    
198.54/60.03	                          [0 1]     [1]                    
198.54/60.03	                       >  [1 0] x + [0]                    
198.54/60.03	                          [0 1]     [0]                    
198.54/60.03	                       =  [x]                              
198.54/60.03	                                                           
198.54/60.03	          [.(x, i(x))] =  [2 2] x + [3]                    
198.54/60.03	                          [0 2]     [1]                    
198.54/60.03	                       >  [0]                              
198.54/60.03	                          [0]                              
198.54/60.03	                       =  [1()]                            
198.54/60.03	                                                           
198.54/60.03	       [.(.(x, y), z)] =  [1 0] x + [1 0] y + [1 0] z + [4]
198.54/60.03	                          [0 1]     [0 1]     [0 1]     [2]
198.54/60.03	                       >= [1 0] x + [1 0] y + [1 0] z + [4]
198.54/60.03	                          [0 1]     [0 1]     [0 1]     [2]
198.54/60.03	                       =  [.(x, .(y, z))]                  
198.54/60.03	                                                           
198.54/60.03	           [.(1(), x)] =  [1 0] x + [2]                    
198.54/60.03	                          [0 1]     [1]                    
198.54/60.03	                       >  [1 0] x + [0]                    
198.54/60.03	                          [0 1]     [0]                    
198.54/60.03	                       =  [x]                              
198.54/60.03	                                                           
198.54/60.03	          [.(i(x), x)] =  [2 2] x + [3]                    
198.54/60.03	                          [0 2]     [1]                    
198.54/60.03	                       >  [0]                              
198.54/60.03	                          [0]                              
198.54/60.03	                       =  [1()]                            
198.54/60.03	                                                           
198.54/60.03	    [.(i(y), .(y, z))] =  [2 2] y + [1 0] z + [5]          
198.54/60.03	                          [0 2]     [0 1]     [2]          
198.54/60.03	                       >  [1 0] z + [0]                    
198.54/60.03	                          [0 1]     [0]                    
198.54/60.03	                       =  [z]                              
198.54/60.03	                                                           
198.54/60.03	          [i(.(x, y))] =  [1 2] x + [1 2] y + [5]          
198.54/60.03	                          [0 1]     [0 1]     [1]          
198.54/60.03	                       >  [1 2] x + [1 2] y + [4]          
198.54/60.03	                          [0 1]     [0 1]     [1]          
198.54/60.03	                       =  [.(i(y), i(x))]                  
198.54/60.03	                                                           
198.54/60.03	              [i(1())] =  [1]                              
198.54/60.03	                          [0]                              
198.54/60.03	                       >  [0]                              
198.54/60.03	                          [0]                              
198.54/60.03	                       =  [1()]                            
198.54/60.03	                                                           
198.54/60.03	             [i(i(x))] =  [1 4] x + [2]                    
198.54/60.03	                          [0 1]     [0]                    
198.54/60.03	                       >  [1 0] x + [0]                    
198.54/60.03	                          [0 1]     [0]                    
198.54/60.03	                       =  [x]                              
198.54/60.03	                                                           
198.54/60.03	
198.54/60.03	We return to the main proof.
198.54/60.03	
198.54/60.03	We are left with following problem, upon which TcT provides the
198.54/60.03	certificate YES(?,O(n^2)).
198.54/60.03	
198.54/60.03	Strict Trs: { .(.(x, y), z) -> .(x, .(y, z)) }
198.54/60.03	Obligation:
198.54/60.03	  derivational complexity
198.54/60.03	Answer:
198.54/60.03	  YES(?,O(n^2))
198.54/60.03	
198.54/60.03	TcT has computed the following triangular matrix interpretation.
198.54/60.03	
198.54/60.03	  [.](x1, x2) = [1 1] x1 + [1 0] x2 + [0]
198.54/60.03	                [0 1]      [0 1]      [4]
198.54/60.03	
198.54/60.03	The order satisfies the following ordering constraints:
198.54/60.03	
198.54/60.03	  [.(.(x, y), z)] = [1 2] x + [1 1] y + [1 0] z + [4]
198.54/60.03	                    [0 1]     [0 1]     [0 1]     [8]
198.54/60.03	                  > [1 1] x + [1 1] y + [1 0] z + [0]
198.54/60.03	                    [0 1]     [0 1]     [0 1]     [8]
198.54/60.03	                  = [.(x, .(y, z))]                  
198.54/60.03	                                                     
198.54/60.03	
198.54/60.03	Hurray, we answered YES(O(1),O(n^6))
198.54/60.03	EOF