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