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