YES(?,O(n^1)) 6.79/3.68 YES(?,O(n^1)) 6.79/3.68 6.79/3.68 We are left with following problem, upon which TcT provides the 6.79/3.68 certificate YES(?,O(n^1)). 6.79/3.68 6.79/3.68 Strict Trs: 6.79/3.68 { f(h(x)) -> f(i(x)) 6.79/3.68 , h(a()) -> b() 6.79/3.68 , i(a()) -> b() 6.79/3.68 , g(i(x)) -> g(h(x)) } 6.79/3.68 Obligation: 6.79/3.68 derivational complexity 6.79/3.68 Answer: 6.79/3.68 YES(?,O(n^1)) 6.79/3.68 6.79/3.68 TcT has computed the following matrix interpretation satisfying 6.79/3.68 not(EDA) and not(IDA(1)). 6.79/3.68 6.79/3.68 [1 0 1 0] [0] 6.79/3.68 [f](x1) = [0 0 0 1] x1 + [0] 6.79/3.68 [0 0 0 0] [0] 6.79/3.68 [0 0 0 0] [0] 6.79/3.68 6.79/3.68 [1 0 0 0] [0] 6.79/3.68 [h](x1) = [0 0 0 0] x1 + [0] 6.79/3.68 [0 0 0 0] [1] 6.79/3.68 [0 0 0 1] [0] 6.79/3.68 6.79/3.68 [1 0 0 0] [0] 6.79/3.68 [i](x1) = [0 0 0 0] x1 + [1] 6.79/3.68 [0 0 0 0] [0] 6.79/3.68 [0 0 0 0] [0] 6.79/3.68 6.79/3.68 [1 1 0 0] [1] 6.79/3.68 [g](x1) = [0 0 0 0] x1 + [0] 6.79/3.68 [0 0 0 0] [0] 6.79/3.68 [0 0 0 0] [0] 6.79/3.68 6.79/3.68 [1] 6.79/3.68 [a] = [0] 6.79/3.68 [0] 6.79/3.68 [0] 6.79/3.68 6.79/3.68 [0] 6.79/3.68 [b] = [0] 6.79/3.68 [0] 6.79/3.68 [0] 6.79/3.68 6.79/3.68 The order satisfies the following ordering constraints: 6.79/3.68 6.79/3.68 [f(h(x))] = [1 0 0 0] [1] 6.79/3.68 [0 0 0 1] x + [0] 6.79/3.68 [0 0 0 0] [0] 6.79/3.68 [0 0 0 0] [0] 6.79/3.68 > [1 0 0 0] [0] 6.79/3.68 [0 0 0 0] x + [0] 6.79/3.68 [0 0 0 0] [0] 6.79/3.68 [0 0 0 0] [0] 6.79/3.68 = [f(i(x))] 6.79/3.68 6.79/3.68 [h(a())] = [1] 6.79/3.68 [0] 6.79/3.68 [1] 6.79/3.68 [0] 6.79/3.68 > [0] 6.79/3.68 [0] 6.79/3.68 [0] 6.79/3.68 [0] 6.79/3.68 = [b()] 6.79/3.68 6.79/3.68 [i(a())] = [1] 6.79/3.68 [1] 6.79/3.68 [0] 6.79/3.68 [0] 6.79/3.68 > [0] 6.79/3.68 [0] 6.79/3.68 [0] 6.79/3.68 [0] 6.79/3.68 = [b()] 6.79/3.68 6.79/3.68 [g(i(x))] = [1 0 0 0] [2] 6.79/3.68 [0 0 0 0] x + [0] 6.79/3.68 [0 0 0 0] [0] 6.79/3.68 [0 0 0 0] [0] 6.79/3.68 > [1 0 0 0] [1] 6.79/3.68 [0 0 0 0] x + [0] 6.79/3.68 [0 0 0 0] [0] 6.79/3.68 [0 0 0 0] [0] 6.79/3.68 = [g(h(x))] 6.79/3.68 6.79/3.68 6.79/3.68 Hurray, we answered YES(?,O(n^1)) 6.93/3.70 EOF