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