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