YES(?,O(n^2))
7.14/3.11	YES(?,O(n^2))
7.14/3.11	
7.14/3.11	We are left with following problem, upon which TcT provides the
7.14/3.11	certificate YES(?,O(n^2)).
7.14/3.11	
7.14/3.11	Strict Trs:
7.14/3.11	  { and(tt(), X) -> activate(X)
7.14/3.11	  , activate(X) -> X
7.14/3.11	  , plus(N, 0()) -> N
7.14/3.11	  , plus(N, s(M)) -> s(plus(N, M))
7.14/3.11	  , x(N, 0()) -> 0()
7.14/3.11	  , x(N, s(M)) -> plus(x(N, M), N) }
7.14/3.11	Obligation:
7.14/3.11	  innermost runtime complexity
7.14/3.11	Answer:
7.14/3.11	  YES(?,O(n^2))
7.14/3.11	
7.14/3.11	The input was oriented with the instance of 'Small Polynomial Path
7.14/3.11	Order (PS)' as induced by the safe mapping
7.14/3.11	
7.14/3.11	 safe(and) = {1, 2}, safe(tt) = {}, safe(activate) = {1},
7.14/3.11	 safe(plus) = {1}, safe(0) = {}, safe(s) = {1}, safe(x) = {}
7.14/3.11	
7.14/3.11	and precedence
7.14/3.11	
7.14/3.11	 and > activate, and > plus, x > activate, x > plus, and ~ x,
7.14/3.11	 activate ~ plus .
7.14/3.11	
7.14/3.11	Following symbols are considered recursive:
7.14/3.11	
7.14/3.11	 {and, activate, plus, x}
7.14/3.11	
7.14/3.11	The recursion depth is 2.
7.14/3.11	
7.14/3.11	For your convenience, here are the satisfied ordering constraints:
7.14/3.11	
7.14/3.11	  and(; tt(),  X) > activate(; X)     
7.14/3.11	                                      
7.14/3.11	    activate(; X) > X                 
7.14/3.11	                                      
7.14/3.11	     plus(0(); N) > N                 
7.14/3.11	                                      
7.14/3.11	  plus(s(; M); N) > s(; plus(M; N))   
7.14/3.11	                                      
7.14/3.11	      x(N,  0();) > 0()               
7.14/3.11	                                      
7.14/3.11	   x(N,  s(; M);) > plus(N; x(N,  M;))
7.14/3.11	                                      
7.14/3.11	
7.14/3.11	Hurray, we answered YES(?,O(n^2))
7.14/3.13	EOF