YES(?,O(1))
0.00/0.20	YES(?,O(1))
0.00/0.20	
0.00/0.20	We are left with following problem, upon which TcT provides the
0.00/0.20	certificate YES(?,O(1)).
0.00/0.20	
0.00/0.20	Strict Trs:
0.00/0.20	  { rewrite(Op(Op(x, y), y')) ->
0.00/0.20	    rewrite[Ite][True][Let][Ite](True(), Op(Op(x, y), y'), Op(x, y))
0.00/0.20	  , rewrite(Op(Val(n), y)) ->
0.00/0.20	    rewrite[Ite][True][Let][Ite](False(), Op(Val(n), y), Val(n))
0.00/0.20	  , rewrite(Val(n)) -> Val(n)
0.00/0.20	  , second(Op(x, y)) -> y
0.00/0.20	  , isOp(Op(x, y)) -> True()
0.00/0.20	  , isOp(Val(n)) -> False()
0.00/0.20	  , first(Op(x, y)) -> x
0.00/0.20	  , first(Val(n)) -> Val(n)
0.00/0.20	  , assrewrite(exp) -> rewrite(exp) }
0.00/0.20	Obligation:
0.00/0.20	  innermost runtime complexity
0.00/0.20	Answer:
0.00/0.20	  YES(?,O(1))
0.00/0.20	
0.00/0.20	The input was oriented with the instance of 'Small Polynomial Path
0.00/0.20	Order (PS,0-bounded)' as induced by the safe mapping
0.00/0.20	
0.00/0.20	 safe(rewrite) = {1}, safe(Op) = {1, 2}, safe(Val) = {1},
0.00/0.20	 safe(rewrite[Ite][True][Let][Ite]) = {1, 2, 3}, safe(False) = {},
0.00/0.20	 safe(True) = {}, safe(second) = {}, safe(isOp) = {},
0.00/0.20	 safe(first) = {}, safe(assrewrite) = {}
0.00/0.20	
0.00/0.20	and precedence
0.00/0.20	
0.00/0.20	 rewrite > first, second > rewrite, second > isOp, second > first,
0.00/0.20	 isOp > first, assrewrite > rewrite, assrewrite > isOp,
0.00/0.20	 assrewrite > first, rewrite ~ isOp, second ~ assrewrite .
0.00/0.20	
0.00/0.20	Following symbols are considered recursive:
0.00/0.20	
0.00/0.20	 {}
0.00/0.20	
0.00/0.20	The recursion depth is 0.
0.00/0.20	
0.00/0.20	For your convenience, here are the satisfied ordering constraints:
0.00/0.20	
0.00/0.20	  rewrite(; Op(; Op(; x,  y),  y')) > rewrite[Ite][True][Let][Ite](; True(),                 
0.00/0.20	                                                                     Op(; Op(; x,  y),  y'), 
0.00/0.20	                                                                     Op(; x,  y))            
0.00/0.20	                                                                                             
0.00/0.20	      rewrite(; Op(; Val(; n),  y)) > rewrite[Ite][True][Let][Ite](; False(),                
0.00/0.20	                                                                     Op(; Val(; n),  y),     
0.00/0.20	                                                                     Val(; n))               
0.00/0.20	                                                                                             
0.00/0.20	                rewrite(; Val(; n)) > Val(; n)                                               
0.00/0.20	                                                                                             
0.00/0.20	               second(Op(; x,  y);) > y                                                      
0.00/0.20	                                                                                             
0.00/0.20	                 isOp(Op(; x,  y);) > True()                                                 
0.00/0.20	                                                                                             
0.00/0.20	                    isOp(Val(; n);) > False()                                                
0.00/0.20	                                                                                             
0.00/0.20	                first(Op(; x,  y);) > x                                                      
0.00/0.20	                                                                                             
0.00/0.20	                   first(Val(; n);) > Val(; n)                                               
0.00/0.20	                                                                                             
0.00/0.20	                   assrewrite(exp;) > rewrite(; exp)                                         
0.00/0.20	                                                                                             
0.00/0.20	
0.00/0.20	Hurray, we answered YES(?,O(1))
0.00/0.21	EOF