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