YES(?,O(n^1))
10.23/5.58	YES(?,O(n^1))
10.23/5.58	
10.23/5.58	We are left with following problem, upon which TcT provides the
10.23/5.58	certificate YES(?,O(n^1)).
10.23/5.58	
10.23/5.58	Strict Trs:
10.23/5.58	  { f(a()) -> g(h(a()))
10.23/5.58	  , h(g(x)) -> g(h(f(x)))
10.23/5.58	  , k(x, h(x), a()) -> h(x)
10.23/5.58	  , k(f(x), y, x) -> f(x) }
10.23/5.58	Obligation:
10.23/5.58	  derivational complexity
10.23/5.58	Answer:
10.23/5.58	  YES(?,O(n^1))
10.23/5.58	
10.23/5.58	TcT has computed the following matrix interpretation satisfying
10.23/5.58	not(EDA) and not(IDA(1)).
10.23/5.58	
10.23/5.58	                    [1 0 1 0]      [0]                              
10.23/5.58	          [f](x1) = [0 0 0 1] x1 + [0]                              
10.23/5.58	                    [0 0 0 0]      [0]                              
10.23/5.58	                    [0 0 0 0]      [0]                              
10.23/5.58	                                                                    
10.23/5.58	                    [0]                                             
10.23/5.58	              [a] = [0]                                             
10.23/5.58	                    [1]                                             
10.23/5.58	                    [1]                                             
10.23/5.58	                                                                    
10.23/5.58	                    [1 0 0 0]      [0]                              
10.23/5.58	          [g](x1) = [0 0 1 1] x1 + [1]                              
10.23/5.58	                    [0 0 0 0]      [0]                              
10.23/5.58	                    [0 0 0 0]      [0]                              
10.23/5.58	                                                                    
10.23/5.58	                    [1 1 0 0]      [0]                              
10.23/5.58	          [h](x1) = [0 0 0 0] x1 + [1]                              
10.23/5.58	                    [0 0 0 0]      [0]                              
10.23/5.58	                    [0 0 0 0]      [0]                              
10.23/5.58	                                                                    
10.23/5.58	                    [1 0 1 0]      [1 0 0 0]      [1 0 0 0]      [1]
10.23/5.58	  [k](x1, x2, x3) = [0 0 0 1] x1 + [0 0 1 1] x2 + [0 0 1 1] x3 + [0]
10.23/5.58	                    [0 0 0 0]      [0 0 0 0]      [0 0 0 0]      [0]
10.23/5.58	                    [0 0 0 0]      [0 0 0 0]      [0 0 0 0]      [0]
10.23/5.58	
10.23/5.58	The order satisfies the following ordering constraints:
10.23/5.58	
10.23/5.58	           [f(a())] = [1]                            
10.23/5.58	                      [1]                            
10.23/5.58	                      [0]                            
10.23/5.58	                      [0]                            
10.23/5.58	                    > [0]                            
10.23/5.58	                      [1]                            
10.23/5.58	                      [0]                            
10.23/5.58	                      [0]                            
10.23/5.58	                    = [g(h(a()))]                    
10.23/5.58	                                                     
10.23/5.58	          [h(g(x))] = [1 0 1 1]     [1]              
10.23/5.58	                      [0 0 0 0] x + [1]              
10.23/5.58	                      [0 0 0 0]     [0]              
10.23/5.58	                      [0 0 0 0]     [0]              
10.23/5.58	                    > [1 0 1 1]     [0]              
10.23/5.58	                      [0 0 0 0] x + [1]              
10.23/5.58	                      [0 0 0 0]     [0]              
10.23/5.58	                      [0 0 0 0]     [0]              
10.23/5.58	                    = [g(h(f(x)))]                   
10.23/5.58	                                                     
10.23/5.58	  [k(x, h(x), a())] = [2 1 1 0]     [1]              
10.23/5.58	                      [0 0 0 1] x + [2]              
10.23/5.58	                      [0 0 0 0]     [0]              
10.23/5.58	                      [0 0 0 0]     [0]              
10.23/5.58	                    > [1 1 0 0]     [0]              
10.23/5.58	                      [0 0 0 0] x + [1]              
10.23/5.58	                      [0 0 0 0]     [0]              
10.23/5.58	                      [0 0 0 0]     [0]              
10.23/5.58	                    = [h(x)]                         
10.23/5.58	                                                     
10.23/5.58	    [k(f(x), y, x)] = [2 0 1 0]     [1 0 0 0]     [1]
10.23/5.58	                      [0 0 1 1] x + [0 0 1 1] y + [0]
10.23/5.58	                      [0 0 0 0]     [0 0 0 0]     [0]
10.23/5.58	                      [0 0 0 0]     [0 0 0 0]     [0]
10.23/5.58	                    > [1 0 1 0]     [0]              
10.23/5.58	                      [0 0 0 1] x + [0]              
10.23/5.58	                      [0 0 0 0]     [0]              
10.23/5.58	                      [0 0 0 0]     [0]              
10.23/5.58	                    = [f(x)]                         
10.23/5.58	                                                     
10.23/5.58	
10.23/5.58	Hurray, we answered YES(?,O(n^1))
10.37/5.60	EOF