YES(?,O(n^2))
6.91/3.08	YES(?,O(n^2))
6.91/3.08	
6.91/3.08	We are left with following problem, upon which TcT provides the
6.91/3.08	certificate YES(?,O(n^2)).
6.91/3.08	
6.91/3.08	Strict Trs:
6.91/3.08	  { times(x, plus(y, s(z))) ->
6.91/3.08	    plus(times(x, plus(y, times(s(z), 0()))), times(x, s(z)))
6.91/3.08	  , times(x, s(y)) -> plus(times(x, y), x)
6.91/3.08	  , times(x, 0()) -> 0()
6.91/3.08	  , plus(x, s(y)) -> s(plus(x, y))
6.91/3.08	  , plus(x, 0()) -> x }
6.91/3.08	Obligation:
6.91/3.08	  innermost runtime complexity
6.91/3.08	Answer:
6.91/3.08	  YES(?,O(n^2))
6.91/3.08	
6.91/3.08	Arguments of following rules are not normal-forms:
6.91/3.08	
6.91/3.08	{ times(x, plus(y, s(z))) ->
6.91/3.08	  plus(times(x, plus(y, times(s(z), 0()))), times(x, s(z))) }
6.91/3.08	
6.91/3.08	All above mentioned rules can be savely removed.
6.91/3.08	
6.91/3.08	We are left with following problem, upon which TcT provides the
6.91/3.08	certificate YES(?,O(n^2)).
6.91/3.08	
6.91/3.08	Strict Trs:
6.91/3.08	  { times(x, s(y)) -> plus(times(x, y), x)
6.91/3.08	  , times(x, 0()) -> 0()
6.91/3.08	  , plus(x, s(y)) -> s(plus(x, y))
6.91/3.08	  , plus(x, 0()) -> x }
6.91/3.08	Obligation:
6.91/3.08	  innermost runtime complexity
6.91/3.08	Answer:
6.91/3.08	  YES(?,O(n^2))
6.91/3.08	
6.91/3.08	The input was oriented with the instance of 'Small Polynomial Path
6.91/3.08	Order (PS)' as induced by the safe mapping
6.91/3.08	
6.91/3.08	 safe(times) = {}, safe(plus) = {1}, safe(s) = {1}, safe(0) = {}
6.91/3.08	
6.91/3.08	and precedence
6.91/3.08	
6.91/3.08	 times > plus .
6.91/3.08	
6.91/3.08	Following symbols are considered recursive:
6.91/3.08	
6.91/3.08	 {times, plus}
6.91/3.08	
6.91/3.08	The recursion depth is 2.
6.91/3.08	
6.91/3.08	For your convenience, here are the satisfied ordering constraints:
6.91/3.08	
6.91/3.08	  times(x,  s(; y);) > plus(x; times(x,  y;))
6.91/3.08	                                             
6.91/3.08	     times(x,  0();) > 0()                   
6.91/3.08	                                             
6.91/3.08	     plus(s(; y); x) > s(; plus(y; x))       
6.91/3.08	                                             
6.91/3.08	        plus(0(); x) > x                     
6.91/3.08	                                             
6.91/3.08	
6.91/3.08	Hurray, we answered YES(?,O(n^2))
6.91/3.09	EOF