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