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