YES(?,O(n^1)) 9.24/5.31 YES(?,O(n^1)) 9.24/5.31 9.24/5.31 We are left with following problem, upon which TcT provides the 9.24/5.31 certificate YES(?,O(n^1)). 9.24/5.31 9.24/5.31 Strict Trs: 9.24/5.31 { f(a(), f(a(), x)) -> f(a(), f(x, f(f(a(), a()), a()))) } 9.24/5.31 Obligation: 9.24/5.31 derivational complexity 9.24/5.31 Answer: 9.24/5.31 YES(?,O(n^1)) 9.24/5.31 9.24/5.31 We uncurry the input using the following uncurry rules. 9.24/5.31 9.24/5.31 { f(a_1(x_1), x_2) -> a_2(x_1, x_2) 9.24/5.31 , f(a(), x_1) -> a_1(x_1) } 9.24/5.31 9.24/5.31 We are left with following problem, upon which TcT provides the 9.24/5.31 certificate YES(?,O(n^1)). 9.24/5.31 9.24/5.31 Strict Trs: { a_2(a_1(x), x_1) -> a_2(f(x, a_2(a(), a())), x_1) } 9.24/5.31 Weak Trs: 9.24/5.31 { f(a_1(x_1), x_2) -> a_2(x_1, x_2) 9.24/5.31 , f(a(), x_1) -> a_1(x_1) } 9.24/5.31 Obligation: 9.24/5.31 derivational complexity 9.24/5.31 Answer: 9.24/5.31 YES(?,O(n^1)) 9.24/5.31 9.24/5.31 TcT has computed the following matrix interpretation satisfying 9.24/5.31 not(EDA) and not(IDA(1)). 9.24/5.31 9.24/5.31 [1 0 1 0] [1 0 0 0] [0] 9.24/5.31 [f](x1, x2) = [0 0 0 0] x1 + [0 0 0 0] x2 + [0] 9.24/5.31 [0 1 0 0] [0 1 1 0] [0] 9.24/5.31 [0 0 0 0] [0 0 0 0] [0] 9.24/5.31 9.24/5.31 [1 0 1 0] [1 0 0 0] [0] 9.24/5.31 [a_2](x1, x2) = [0 0 0 0] x1 + [0 0 0 0] x2 + [0] 9.24/5.31 [0 0 0 0] [0 0 0 0] [0] 9.24/5.31 [0 0 0 0] [0 0 0 0] [0] 9.24/5.31 9.24/5.31 [1 0 0 0] [0] 9.24/5.31 [a_1](x1) = [0 0 0 0] x1 + [0] 9.24/5.31 [0 1 1 0] [1] 9.24/5.31 [0 0 0 0] [0] 9.24/5.31 9.24/5.31 [0] 9.24/5.31 [a] = [1] 9.24/5.31 [0] 9.24/5.31 [0] 9.24/5.31 9.24/5.31 The order satisfies the following ordering constraints: 9.24/5.31 9.24/5.31 [f(a_1(x_1), x_2)] = [1 1 1 0] [1 0 0 0] [1] 9.24/5.31 [0 0 0 0] x_1 + [0 0 0 0] x_2 + [0] 9.24/5.31 [0 0 0 0] [0 1 1 0] [0] 9.24/5.31 [0 0 0 0] [0 0 0 0] [0] 9.24/5.31 > [1 0 1 0] [1 0 0 0] [0] 9.24/5.31 [0 0 0 0] x_1 + [0 0 0 0] x_2 + [0] 9.24/5.31 [0 0 0 0] [0 0 0 0] [0] 9.24/5.31 [0 0 0 0] [0 0 0 0] [0] 9.24/5.31 = [a_2(x_1, x_2)] 9.24/5.31 9.24/5.31 [f(a(), x_1)] = [1 0 0 0] [0] 9.24/5.31 [0 0 0 0] x_1 + [0] 9.24/5.31 [0 1 1 0] [1] 9.24/5.31 [0 0 0 0] [0] 9.24/5.31 >= [1 0 0 0] [0] 9.24/5.31 [0 0 0 0] x_1 + [0] 9.24/5.31 [0 1 1 0] [1] 9.24/5.31 [0 0 0 0] [0] 9.24/5.31 = [a_1(x_1)] 9.24/5.31 9.24/5.31 [a_2(a_1(x), x_1)] = [1 0 0 0] [1 1 1 0] [1] 9.24/5.31 [0 0 0 0] x_1 + [0 0 0 0] x + [0] 9.24/5.31 [0 0 0 0] [0 0 0 0] [0] 9.24/5.31 [0 0 0 0] [0 0 0 0] [0] 9.24/5.31 > [1 0 0 0] [1 1 1 0] [0] 9.24/5.31 [0 0 0 0] x_1 + [0 0 0 0] x + [0] 9.24/5.31 [0 0 0 0] [0 0 0 0] [0] 9.24/5.31 [0 0 0 0] [0 0 0 0] [0] 9.24/5.31 = [a_2(f(x, a_2(a(), a())), x_1)] 9.24/5.31 9.24/5.31 9.24/5.31 Hurray, we answered YES(?,O(n^1)) 9.24/5.33 EOF