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