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