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