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