YES(?,O(n^1)) 49.95/26.33 YES(?,O(n^1)) 49.95/26.33 49.95/26.33 We are left with following problem, upon which TcT provides the 49.95/26.33 certificate YES(?,O(n^1)). 49.95/26.33 49.95/26.33 Strict Trs: 49.95/26.33 { a(f(), a(g(), a(f(), x))) -> a(f(), a(g(), a(g(), a(f(), x)))) 49.95/26.33 , a(g(), a(f(), a(g(), x))) -> a(g(), a(f(), a(f(), a(g(), x)))) } 49.95/26.33 Obligation: 49.95/26.33 derivational complexity 49.95/26.33 Answer: 49.95/26.33 YES(?,O(n^1)) 49.95/26.33 49.95/26.33 We uncurry the input using the following uncurry rules. 49.95/26.33 49.95/26.33 { a(f(), x_1) -> f_1(x_1) 49.95/26.33 , a(g(), x_1) -> g_1(x_1) } 49.95/26.33 49.95/26.33 We are left with following problem, upon which TcT provides the 49.95/26.33 certificate YES(?,O(n^1)). 49.95/26.33 49.95/26.33 Strict Trs: 49.95/26.33 { f_1(g_1(f_1(x))) -> f_1(g_1(g_1(f_1(x)))) 49.95/26.33 , g_1(f_1(g_1(x))) -> g_1(f_1(f_1(g_1(x)))) } 49.95/26.33 Weak Trs: 49.95/26.33 { a(f(), x_1) -> f_1(x_1) 49.95/26.33 , a(g(), x_1) -> g_1(x_1) } 49.95/26.33 Obligation: 49.95/26.33 derivational complexity 49.95/26.33 Answer: 49.95/26.33 YES(?,O(n^1)) 49.95/26.33 49.95/26.33 The problem is match-bounded by 3. The enriched problem is 49.95/26.33 compatible with the following automaton. 49.95/26.33 { a_0(1, 1) -> 1 49.95/26.33 , f_1_0(1) -> 1 49.95/26.33 , f_1_1(1) -> 4 49.95/26.33 , f_1_1(2) -> 1 49.95/26.33 , f_1_1(2) -> 4 49.95/26.33 , f_1_1(2) -> 10 49.95/26.33 , f_1_1(4) -> 4 49.95/26.33 , f_1_1(6) -> 5 49.95/26.33 , f_1_1(7) -> 4 49.95/26.33 , f_1_1(7) -> 6 49.95/26.33 , f_1_1(7) -> 10 49.95/26.33 , f_1_1(7) -> 15 49.95/26.33 , f_1_1(8) -> 1 49.95/26.33 , f_1_1(11) -> 1 49.95/26.33 , f_1_1(15) -> 1 49.95/26.33 , f_1_2(1) -> 10 49.95/26.33 , f_1_2(2) -> 13 49.95/26.33 , f_1_2(4) -> 14 49.95/26.33 , f_1_2(6) -> 10 49.95/26.33 , f_1_2(7) -> 10 49.95/26.33 , f_1_2(8) -> 4 49.95/26.33 , f_1_2(8) -> 6 49.95/26.33 , f_1_2(8) -> 10 49.95/26.33 , f_1_2(8) -> 15 49.95/26.33 , f_1_2(11) -> 4 49.95/26.33 , f_1_2(11) -> 6 49.95/26.33 , f_1_2(11) -> 10 49.95/26.33 , f_1_2(11) -> 15 49.95/26.33 , f_1_2(15) -> 14 49.95/26.33 , f_1_2(16) -> 15 49.95/26.33 , f_1_3(4) -> 21 49.95/26.33 , f_1_3(8) -> 24 49.95/26.33 , f_1_3(10) -> 31 49.95/26.33 , f_1_3(11) -> 21 49.95/26.33 , f_1_3(15) -> 21 49.95/26.33 , f_1_3(19) -> 10 49.95/26.33 , f_1_3(19) -> 15 49.95/26.33 , f_1_3(19) -> 32 49.95/26.33 , f_1_3(22) -> 15 49.95/26.33 , f_1_3(32) -> 31 49.95/26.33 , f_1_3(33) -> 32 49.95/26.33 , g_1_0(1) -> 1 49.95/26.33 , g_1_1(1) -> 7 49.95/26.33 , g_1_1(3) -> 2 49.95/26.33 , g_1_1(4) -> 1 49.95/26.33 , g_1_1(4) -> 3 49.95/26.33 , g_1_1(4) -> 7 49.95/26.33 , g_1_1(4) -> 16 49.95/26.33 , g_1_1(5) -> 1 49.95/26.33 , g_1_1(5) -> 3 49.95/26.33 , g_1_1(5) -> 7 49.95/26.33 , g_1_1(5) -> 9 49.95/26.33 , g_1_1(5) -> 16 49.95/26.33 , g_1_1(7) -> 2 49.95/26.33 , g_1_1(9) -> 1 49.95/26.33 , g_1_1(12) -> 1 49.95/26.33 , g_1_1(14) -> 1 49.95/26.33 , g_1_2(1) -> 16 49.95/26.33 , g_1_2(3) -> 16 49.95/26.33 , g_1_2(4) -> 16 49.95/26.33 , g_1_2(5) -> 16 49.95/26.33 , g_1_2(7) -> 16 49.95/26.33 , g_1_2(9) -> 8 49.95/26.33 , g_1_2(10) -> 9 49.95/26.33 , g_1_2(12) -> 11 49.95/26.33 , g_1_2(13) -> 12 49.95/26.33 , g_1_2(14) -> 1 49.95/26.33 , g_1_2(14) -> 3 49.95/26.33 , g_1_2(14) -> 7 49.95/26.33 , g_1_2(14) -> 9 49.95/26.33 , g_1_2(14) -> 12 49.95/26.33 , g_1_2(14) -> 16 49.95/26.33 , g_1_3(9) -> 33 49.95/26.33 , g_1_3(12) -> 33 49.95/26.33 , g_1_3(14) -> 33 49.95/26.33 , g_1_3(20) -> 19 49.95/26.33 , g_1_3(21) -> 20 49.95/26.33 , g_1_3(23) -> 22 49.95/26.33 , g_1_3(24) -> 23 49.95/26.33 , g_1_3(31) -> 9 49.95/26.33 , g_1_3(31) -> 16 49.95/26.33 , g_1_3(31) -> 20 49.95/26.33 , g_1_3(31) -> 23 49.95/26.33 , f_0() -> 1 49.95/26.33 , g_0() -> 1 } 49.95/26.33 49.95/26.33 Hurray, we answered YES(?,O(n^1)) 49.95/26.35 EOF