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