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