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