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