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