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