YES(O(1),O(1))
0.00/0.12	YES(O(1),O(1))
0.00/0.12	
0.00/0.12	We are left with following problem, upon which TcT provides the
0.00/0.12	certificate YES(O(1),O(1)).
0.00/0.12	
0.00/0.12	Strict Trs:
0.00/0.12	  { c() -> f()
0.00/0.12	  , f() -> g() }
0.00/0.12	Obligation:
0.00/0.12	  derivational complexity
0.00/0.12	Answer:
0.00/0.12	  YES(O(1),O(1))
0.00/0.12	
0.00/0.12	We use the processor 'matrix interpretation of dimension 1' to
0.00/0.12	orient following rules strictly.
0.00/0.12	
0.00/0.12	Trs:
0.00/0.12	  { c() -> f()
0.00/0.12	  , f() -> g() }
0.00/0.12	
0.00/0.12	The induced complexity on above rules (modulo remaining rules) is
0.00/0.12	YES(?,O(1)) . These rules are removed from the problem. Note that
0.00/0.12	no rule is size-increasing. The overall complexity is obtained by
0.00/0.12	multiplication .
0.00/0.12	
0.00/0.12	Sub-proof:
0.00/0.12	----------
0.00/0.12	  TcT has computed the following triangular matrix interpretation.
0.00/0.12	  
0.00/0.12	    [c] = [2]
0.00/0.12	             
0.00/0.12	    [f] = [1]
0.00/0.12	             
0.00/0.12	    [g] = [0]
0.00/0.12	  
0.00/0.12	  The order satisfies the following ordering constraints:
0.00/0.12	  
0.00/0.12	    [c()] = [2]  
0.00/0.12	          > [1]  
0.00/0.12	          = [f()]
0.00/0.12	                 
0.00/0.12	    [f()] = [1]  
0.00/0.12	          > [0]  
0.00/0.12	          = [g()]
0.00/0.12	                 
0.00/0.12	
0.00/0.12	We return to the main proof.
0.00/0.12	
0.00/0.12	We are left with following problem, upon which TcT provides the
0.00/0.12	certificate YES(O(1),O(1)).
0.00/0.12	
0.00/0.12	Rules: Empty
0.00/0.12	Obligation:
0.00/0.12	  derivational complexity
0.00/0.12	Answer:
0.00/0.12	  YES(O(1),O(1))
0.00/0.12	
0.00/0.12	Empty rules are trivially bounded
0.00/0.12	
0.00/0.12	Hurray, we answered YES(O(1),O(1))
0.00/0.12	EOF