YES(?,O(n^5))
55.39/18.21	YES(?,O(n^5))
55.39/18.21	
55.39/18.21	We are left with following problem, upon which TcT provides the
55.39/18.21	certificate YES(?,O(n^5)).
55.39/18.21	
55.39/18.21	Strict Trs:
55.39/18.21	  { f_0(x) -> a()
55.39/18.21	  , f_1(x) -> g_1(x, x)
55.39/18.21	  , g_1(s(x), y) -> b(f_0(y), g_1(x, y))
55.39/18.21	  , f_2(x) -> g_2(x, x)
55.39/18.21	  , g_2(s(x), y) -> b(f_1(y), g_2(x, y))
55.39/18.21	  , f_3(x) -> g_3(x, x)
55.39/18.21	  , g_3(s(x), y) -> b(f_2(y), g_3(x, y))
55.39/18.21	  , f_4(x) -> g_4(x, x)
55.39/18.21	  , g_4(s(x), y) -> b(f_3(y), g_4(x, y))
55.39/18.21	  , f_5(x) -> g_5(x, x)
55.39/18.21	  , g_5(s(x), y) -> b(f_4(y), g_5(x, y)) }
55.39/18.21	Obligation:
55.39/18.21	  innermost runtime complexity
55.39/18.21	Answer:
55.39/18.21	  YES(?,O(n^5))
55.39/18.21	
55.39/18.21	The input was oriented with the instance of 'Small Polynomial Path
55.39/18.21	Order (PS,5-bounded)' as induced by the safe mapping
55.39/18.21	
55.39/18.21	 safe(f_0) = {1}, safe(a) = {}, safe(f_1) = {}, safe(g_1) = {2},
55.39/18.21	 safe(s) = {1}, safe(b) = {1, 2}, safe(f_2) = {}, safe(g_2) = {},
55.39/18.21	 safe(f_3) = {}, safe(g_3) = {}, safe(f_4) = {}, safe(g_4) = {},
55.39/18.21	 safe(f_5) = {}, safe(g_5) = {}
55.39/18.21	
55.39/18.21	and precedence
55.39/18.21	
55.39/18.21	 f_1 > f_0, f_1 > g_1, g_1 > f_0, f_2 > f_0, f_2 > f_1, f_2 > g_1,
55.39/18.21	 f_2 > g_2, g_2 > f_0, g_2 > f_1, g_2 > g_1, f_3 > f_0, f_3 > f_1,
55.39/18.21	 f_3 > g_1, f_3 > f_2, f_3 > g_2, f_3 > g_3, g_3 > f_0, g_3 > f_1,
55.39/18.21	 g_3 > g_1, g_3 > f_2, g_3 > g_2, f_4 > f_0, f_4 > f_1, f_4 > g_1,
55.39/18.21	 f_4 > f_2, f_4 > g_2, f_4 > f_3, f_4 > g_3, f_4 > g_4, g_4 > f_0,
55.39/18.21	 g_4 > f_1, g_4 > g_1, g_4 > f_2, g_4 > g_2, g_4 > f_3, g_4 > g_3,
55.39/18.21	 f_5 > f_0, f_5 > f_1, f_5 > g_1, f_5 > f_2, f_5 > g_2, f_5 > f_3,
55.39/18.21	 f_5 > g_3, f_5 > f_4, f_5 > g_4, f_5 > g_5, g_5 > f_0, g_5 > f_1,
55.39/18.21	 g_5 > g_1, g_5 > f_2, g_5 > g_2, g_5 > f_3, g_5 > g_3, g_5 > f_4,
55.39/18.21	 g_5 > g_4 .
55.39/18.21	
55.39/18.21	Following symbols are considered recursive:
55.39/18.21	
55.39/18.21	 {g_1, g_2, g_3, g_4, g_5}
55.39/18.21	
55.39/18.21	The recursion depth is 5.
55.39/18.21	
55.39/18.21	For your convenience, here are the satisfied ordering constraints:
55.39/18.21	
55.39/18.21	          f_0(; x) > a()                       
55.39/18.21	                                               
55.39/18.21	           f_1(x;) > g_1(x; x)                 
55.39/18.21	                                               
55.39/18.21	    g_1(s(; x); y) > b(; f_0(; y),  g_1(x; y)) 
55.39/18.21	                                               
55.39/18.21	           f_2(x;) > g_2(x,  x;)               
55.39/18.21	                                               
55.39/18.21	  g_2(s(; x),  y;) > b(; f_1(y;),  g_2(x,  y;))
55.39/18.21	                                               
55.39/18.21	           f_3(x;) > g_3(x,  x;)               
55.39/18.21	                                               
55.39/18.21	  g_3(s(; x),  y;) > b(; f_2(y;),  g_3(x,  y;))
55.39/18.21	                                               
55.39/18.21	           f_4(x;) > g_4(x,  x;)               
55.39/18.21	                                               
55.39/18.21	  g_4(s(; x),  y;) > b(; f_3(y;),  g_4(x,  y;))
55.39/18.21	                                               
55.39/18.21	           f_5(x;) > g_5(x,  x;)               
55.39/18.21	                                               
55.39/18.21	  g_5(s(; x),  y;) > b(; f_4(y;),  g_5(x,  y;))
55.39/18.21	                                               
55.39/18.21	
55.39/18.21	Hurray, we answered YES(?,O(n^5))
55.39/18.23	EOF