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