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