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