YES(?,O(n^1))
8.56/5.09	YES(?,O(n^1))
8.56/5.09	
8.56/5.09	We are left with following problem, upon which TcT provides the
8.56/5.09	certificate YES(?,O(n^1)).
8.56/5.09	
8.56/5.09	Strict Trs:
8.56/5.09	  { \(x, x) -> e()
8.56/5.09	  , \(x, .(x, y)) -> y
8.56/5.09	  , \(e(), x) -> x
8.56/5.09	  , \(/(x, y), x) -> y
8.56/5.09	  , /(x, x) -> e()
8.56/5.09	  , /(x, \(y, x)) -> y
8.56/5.09	  , /(x, e()) -> x
8.56/5.09	  , /(.(y, x), x) -> y
8.56/5.09	  , .(x, \(x, y)) -> y
8.56/5.09	  , .(x, e()) -> x
8.56/5.09	  , .(e(), x) -> x
8.56/5.09	  , .(/(y, x), x) -> y }
8.56/5.09	Obligation:
8.56/5.09	  derivational complexity
8.56/5.09	Answer:
8.56/5.09	  YES(?,O(n^1))
8.56/5.09	
8.56/5.09	TcT has computed the following matrix interpretation satisfying
8.56/5.09	not(EDA) and not(IDA(1)).
8.56/5.09	
8.56/5.09	                [1 0 0 0]      [1 0 0 0]      [1]
8.56/5.09	  [\](x1, x2) = [0 1 0 0] x1 + [0 1 0 0] x2 + [1]
8.56/5.09	                [0 0 1 0]      [0 0 1 0]      [0]
8.56/5.09	                [0 0 1 1]      [0 0 1 1]      [0]
8.56/5.09	                                                 
8.56/5.09	                [0]                              
8.56/5.09	          [e] = [0]                              
8.56/5.09	                [0]                              
8.56/5.09	                [0]                              
8.56/5.09	                                                 
8.56/5.09	                [1 0 0 0]      [1 0 0 0]      [1]
8.56/5.09	  [/](x1, x2) = [0 1 0 0] x1 + [0 1 0 0] x2 + [1]
8.56/5.09	                [0 0 1 0]      [0 0 1 1]      [0]
8.56/5.09	                [0 0 1 1]      [0 0 0 1]      [0]
8.56/5.09	                                                 
8.56/5.09	                [1 0 0 0]      [1 0 0 0]      [1]
8.56/5.09	  [.](x1, x2) = [0 1 0 0] x1 + [0 1 0 0] x2 + [0]
8.56/5.09	                [0 0 1 1]      [0 0 1 1]      [0]
8.56/5.09	                [0 0 0 1]      [0 0 0 1]      [0]
8.56/5.09	
8.56/5.09	The order satisfies the following ordering constraints:
8.56/5.09	
8.56/5.09	        [\(x, x)] = [2 0 0 0]     [1]              
8.56/5.09	                    [0 2 0 0] x + [1]              
8.56/5.09	                    [0 0 2 0]     [0]              
8.56/5.09	                    [0 0 2 2]     [0]              
8.56/5.09	                  > [0]                            
8.56/5.09	                    [0]                            
8.56/5.09	                    [0]                            
8.56/5.09	                    [0]                            
8.56/5.09	                  = [e()]                          
8.56/5.09	                                                   
8.56/5.09	  [\(x, .(x, y))] = [2 0 0 0]     [1 0 0 0]     [2]
8.56/5.09	                    [0 2 0 0] x + [0 1 0 0] y + [1]
8.56/5.09	                    [0 0 2 1]     [0 0 1 1]     [0]
8.56/5.09	                    [0 0 2 3]     [0 0 1 2]     [0]
8.56/5.09	                  > [1 0 0 0]     [0]              
8.56/5.09	                    [0 1 0 0] y + [0]              
8.56/5.09	                    [0 0 1 0]     [0]              
8.56/5.09	                    [0 0 0 1]     [0]              
8.56/5.09	                  = [y]                            
8.56/5.09	                                                   
8.56/5.09	      [\(e(), x)] = [1 0 0 0]     [1]              
8.56/5.09	                    [0 1 0 0] x + [1]              
8.56/5.09	                    [0 0 1 0]     [0]              
8.56/5.09	                    [0 0 1 1]     [0]              
8.56/5.09	                  > [1 0 0 0]     [0]              
8.56/5.09	                    [0 1 0 0] x + [0]              
8.56/5.09	                    [0 0 1 0]     [0]              
8.56/5.09	                    [0 0 0 1]     [0]              
8.56/5.09	                  = [x]                            
8.56/5.09	                                                   
8.56/5.09	  [\(/(x, y), x)] = [2 0 0 0]     [1 0 0 0]     [2]
8.56/5.09	                    [0 2 0 0] x + [0 1 0 0] y + [2]
8.56/5.09	                    [0 0 2 0]     [0 0 1 1]     [0]
8.56/5.09	                    [0 0 3 2]     [0 0 1 2]     [0]
8.56/5.09	                  > [1 0 0 0]     [0]              
8.56/5.09	                    [0 1 0 0] y + [0]              
8.56/5.09	                    [0 0 1 0]     [0]              
8.56/5.09	                    [0 0 0 1]     [0]              
8.56/5.09	                  = [y]                            
8.56/5.09	                                                   
8.56/5.09	        [/(x, x)] = [2 0 0 0]     [1]              
8.56/5.09	                    [0 2 0 0] x + [1]              
8.56/5.09	                    [0 0 2 1]     [0]              
8.56/5.09	                    [0 0 1 2]     [0]              
8.56/5.09	                  > [0]                            
8.56/5.09	                    [0]                            
8.56/5.09	                    [0]                            
8.56/5.09	                    [0]                            
8.56/5.09	                  = [e()]                          
8.56/5.09	                                                   
8.56/5.09	  [/(x, \(y, x))] = [2 0 0 0]     [1 0 0 0]     [2]
8.56/5.09	                    [0 2 0 0] x + [0 1 0 0] y + [2]
8.56/5.09	                    [0 0 3 1]     [0 0 2 1]     [0]
8.56/5.09	                    [0 0 2 2]     [0 0 1 1]     [0]
8.56/5.09	                  > [1 0 0 0]     [0]              
8.56/5.09	                    [0 1 0 0] y + [0]              
8.56/5.09	                    [0 0 1 0]     [0]              
8.56/5.09	                    [0 0 0 1]     [0]              
8.56/5.09	                  = [y]                            
8.56/5.09	                                                   
8.56/5.09	      [/(x, e())] = [1 0 0 0]     [1]              
8.56/5.09	                    [0 1 0 0] x + [1]              
8.56/5.09	                    [0 0 1 0]     [0]              
8.56/5.09	                    [0 0 1 1]     [0]              
8.56/5.09	                  > [1 0 0 0]     [0]              
8.56/5.09	                    [0 1 0 0] x + [0]              
8.56/5.09	                    [0 0 1 0]     [0]              
8.56/5.09	                    [0 0 0 1]     [0]              
8.56/5.09	                  = [x]                            
8.56/5.09	                                                   
8.56/5.09	  [/(.(y, x), x)] = [2 0 0 0]     [1 0 0 0]     [2]
8.56/5.09	                    [0 2 0 0] x + [0 1 0 0] y + [1]
8.56/5.09	                    [0 0 2 2]     [0 0 1 1]     [0]
8.56/5.09	                    [0 0 1 3]     [0 0 1 2]     [0]
8.56/5.09	                  > [1 0 0 0]     [0]              
8.56/5.09	                    [0 1 0 0] y + [0]              
8.56/5.09	                    [0 0 1 0]     [0]              
8.56/5.09	                    [0 0 0 1]     [0]              
8.56/5.09	                  = [y]                            
8.56/5.09	                                                   
8.56/5.09	  [.(x, \(x, y))] = [2 0 0 0]     [1 0 0 0]     [2]
8.56/5.09	                    [0 2 0 0] x + [0 1 0 0] y + [1]
8.56/5.09	                    [0 0 3 2]     [0 0 2 1]     [0]
8.56/5.09	                    [0 0 1 2]     [0 0 1 1]     [0]
8.56/5.09	                  > [1 0 0 0]     [0]              
8.56/5.09	                    [0 1 0 0] y + [0]              
8.56/5.09	                    [0 0 1 0]     [0]              
8.56/5.09	                    [0 0 0 1]     [0]              
8.56/5.09	                  = [y]                            
8.56/5.09	                                                   
8.56/5.09	      [.(x, e())] = [1 0 0 0]     [1]              
8.56/5.09	                    [0 1 0 0] x + [0]              
8.56/5.09	                    [0 0 1 1]     [0]              
8.56/5.09	                    [0 0 0 1]     [0]              
8.56/5.09	                  > [1 0 0 0]     [0]              
8.56/5.09	                    [0 1 0 0] x + [0]              
8.56/5.09	                    [0 0 1 0]     [0]              
8.56/5.09	                    [0 0 0 1]     [0]              
8.56/5.09	                  = [x]                            
8.56/5.09	                                                   
8.56/5.09	      [.(e(), x)] = [1 0 0 0]     [1]              
8.56/5.09	                    [0 1 0 0] x + [0]              
8.56/5.09	                    [0 0 1 1]     [0]              
8.56/5.09	                    [0 0 0 1]     [0]              
8.56/5.09	                  > [1 0 0 0]     [0]              
8.56/5.09	                    [0 1 0 0] x + [0]              
8.56/5.09	                    [0 0 1 0]     [0]              
8.56/5.09	                    [0 0 0 1]     [0]              
8.56/5.09	                  = [x]                            
8.56/5.09	                                                   
8.56/5.09	  [.(/(y, x), x)] = [2 0 0 0]     [1 0 0 0]     [2]
8.56/5.09	                    [0 2 0 0] x + [0 1 0 0] y + [1]
8.56/5.09	                    [0 0 2 3]     [0 0 2 1]     [0]
8.56/5.09	                    [0 0 0 2]     [0 0 1 1]     [0]
8.56/5.09	                  > [1 0 0 0]     [0]              
8.56/5.09	                    [0 1 0 0] y + [0]              
8.56/5.09	                    [0 0 1 0]     [0]              
8.56/5.09	                    [0 0 0 1]     [0]              
8.56/5.09	                  = [y]                            
8.56/5.09	                                                   
8.56/5.09	
8.56/5.09	Hurray, we answered YES(?,O(n^1))
8.71/5.11	EOF