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