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