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