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