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