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