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