YES(?,O(n^1))
0.00/0.34	YES(?,O(n^1))
0.00/0.34	
0.00/0.34	We are left with following problem, upon which TcT provides the
0.00/0.34	certificate YES(?,O(n^1)).
0.00/0.34	
0.00/0.34	Strict Trs:
0.00/0.34	  { merge(Cons(x', xs'), Cons(x, xs)) ->
0.00/0.34	    merge[Ite][False][Ite][False][Ite](<=(x', x),
0.00/0.34	                                       Cons(x', xs'),
0.00/0.34	                                       Cons(x, xs))
0.00/0.34	  , merge(Cons(x, xs), Nil()) -> Cons(x, xs)
0.00/0.34	  , merge(Nil(), ys) -> ys
0.00/0.34	  , goal(xs, ys) -> merge(xs, ys) }
0.00/0.34	Weak Trs:
0.00/0.34	  { <=(S(x), S(y)) -> <=(x, y)
0.00/0.34	  , <=(S(x), 0()) -> False()
0.00/0.34	  , <=(0(), y) -> True() }
0.00/0.34	Obligation:
0.00/0.34	  innermost runtime complexity
0.00/0.34	Answer:
0.00/0.34	  YES(?,O(n^1))
0.00/0.34	
0.00/0.34	The input was oriented with the instance of 'Small Polynomial Path
0.00/0.34	Order (PS,1-bounded)' as induced by the safe mapping
0.00/0.34	
0.00/0.34	 safe(<=) = {1}, safe(True) = {}, safe(S) = {1},
0.00/0.34	 safe(merge[Ite][False][Ite][False][Ite]) = {1, 2, 3},
0.00/0.34	 safe(Cons) = {1, 2}, safe(Nil) = {}, safe(0) = {},
0.00/0.34	 safe(merge) = {1}, safe(goal) = {1}, safe(False) = {}
0.00/0.34	
0.00/0.34	and precedence
0.00/0.34	
0.00/0.34	 merge > <=, goal > <=, goal > merge .
0.00/0.34	
0.00/0.34	Following symbols are considered recursive:
0.00/0.34	
0.00/0.34	 {<=}
0.00/0.34	
0.00/0.34	The recursion depth is 1.
0.00/0.34	
0.00/0.34	For your convenience, here are the satisfied ordering constraints:
0.00/0.34	
0.00/0.34	                    <=(S(; y); S(; x)) > <=(y; x)                                            
0.00/0.34	                                                                                                   
0.00/0.34	                       <=(0(); S(; x)) > False()                                                
0.00/0.34	                                                                                                   
0.00/0.34	                            <=(y; 0()) > True()                                                 
0.00/0.34	                                                                                                   
0.00/0.34	  merge(Cons(; x,  xs); Cons(; x',  xs')) > merge[Ite][False][Ite][False][Ite](; <=(x; x'),     
0.00/0.34	                                                                                 Cons(; x',  xs'), 
0.00/0.34	                                                                                 Cons(; x,  xs))   
0.00/0.34	                                                                                                   
0.00/0.34	             merge(Nil(); Cons(; x,  xs)) > Cons(; x,  xs)                                         
0.00/0.34	                                                                                                   
0.00/0.34	                         merge(ys; Nil()) > ys                                                     
0.00/0.34	                                                                                                   
0.00/0.34	                             goal(ys; xs) > merge(ys; xs)                                          
0.00/0.34	                                                                                                   
0.00/0.34	
0.00/0.34	Hurray, we answered YES(?,O(n^1))
0.00/0.34	EOF