YES(?,O(n^1)) 22.45/12.39 YES(?,O(n^1)) 22.45/12.39 22.45/12.39 We are left with following problem, upon which TcT provides the 22.45/12.39 certificate YES(?,O(n^1)). 22.45/12.39 22.45/12.39 Strict Trs: 22.45/12.39 { a(c(d(x))) -> c(x) 22.45/12.39 , u(b(d(d(x)))) -> b(x) 22.45/12.39 , v(a(a(x))) -> u(v(x)) 22.45/12.39 , v(a(c(x))) -> u(b(d(x))) 22.45/12.39 , v(c(x)) -> b(x) 22.45/12.39 , w(a(a(x))) -> u(w(x)) 22.45/12.39 , w(a(c(x))) -> u(b(d(x))) 22.45/12.39 , w(c(x)) -> b(x) } 22.45/12.39 Obligation: 22.45/12.39 derivational complexity 22.45/12.39 Answer: 22.45/12.39 YES(?,O(n^1)) 22.45/12.39 22.45/12.39 TcT has computed the following matrix interpretation satisfying 22.45/12.39 not(EDA) and not(IDA(1)). 22.45/12.39 22.45/12.39 [1 0 0 0] [1] 22.45/12.39 [a](x1) = [0 0 0 0] x1 + [0] 22.45/12.39 [0 0 0 0] [0] 22.45/12.39 [0 0 0 1] [0] 22.45/12.39 22.45/12.39 [1 0 0 0] [1] 22.45/12.39 [c](x1) = [0 0 0 0] x1 + [0] 22.45/12.39 [0 0 0 0] [0] 22.45/12.39 [0 0 0 0] [0] 22.45/12.39 22.45/12.39 [1 0 0 0] [0] 22.45/12.39 [d](x1) = [0 0 0 0] x1 + [0] 22.45/12.39 [0 0 0 0] [0] 22.45/12.39 [0 0 0 0] [0] 22.45/12.39 22.45/12.39 [1 0 0 0] [1] 22.45/12.39 [u](x1) = [0 0 0 0] x1 + [0] 22.45/12.39 [0 0 0 0] [0] 22.45/12.39 [0 0 0 0] [0] 22.45/12.39 22.45/12.39 [1 0 0 0] [0] 22.45/12.39 [b](x1) = [0 0 0 0] x1 + [0] 22.45/12.39 [0 0 0 0] [0] 22.45/12.39 [0 0 0 0] [0] 22.45/12.39 22.45/12.39 [1 0 0 0] [0] 22.45/12.39 [v](x1) = [0 0 0 0] x1 + [0] 22.45/12.39 [0 0 0 0] [0] 22.45/12.39 [0 0 0 0] [0] 22.45/12.39 22.45/12.39 [1 0 0 0] [0] 22.45/12.39 [w](x1) = [0 0 0 0] x1 + [0] 22.45/12.39 [0 0 0 0] [0] 22.45/12.39 [0 0 0 1] [0] 22.45/12.39 22.45/12.39 The order satisfies the following ordering constraints: 22.45/12.39 22.45/12.39 [a(c(d(x)))] = [1 0 0 0] [2] 22.45/12.39 [0 0 0 0] x + [0] 22.45/12.39 [0 0 0 0] [0] 22.45/12.39 [0 0 0 0] [0] 22.45/12.39 > [1 0 0 0] [1] 22.45/12.39 [0 0 0 0] x + [0] 22.45/12.39 [0 0 0 0] [0] 22.45/12.39 [0 0 0 0] [0] 22.45/12.39 = [c(x)] 22.45/12.39 22.45/12.39 [u(b(d(d(x))))] = [1 0 0 0] [1] 22.45/12.39 [0 0 0 0] x + [0] 22.45/12.39 [0 0 0 0] [0] 22.45/12.39 [0 0 0 0] [0] 22.45/12.39 > [1 0 0 0] [0] 22.45/12.39 [0 0 0 0] x + [0] 22.45/12.39 [0 0 0 0] [0] 22.45/12.39 [0 0 0 0] [0] 22.45/12.39 = [b(x)] 22.45/12.39 22.45/12.39 [v(a(a(x)))] = [1 0 0 0] [2] 22.45/12.39 [0 0 0 0] x + [0] 22.45/12.39 [0 0 0 0] [0] 22.45/12.39 [0 0 0 0] [0] 22.45/12.39 > [1 0 0 0] [1] 22.45/12.39 [0 0 0 0] x + [0] 22.45/12.39 [0 0 0 0] [0] 22.45/12.39 [0 0 0 0] [0] 22.45/12.39 = [u(v(x))] 22.45/12.39 22.45/12.39 [v(a(c(x)))] = [1 0 0 0] [2] 22.45/12.39 [0 0 0 0] x + [0] 22.45/12.39 [0 0 0 0] [0] 22.45/12.39 [0 0 0 0] [0] 22.45/12.39 > [1 0 0 0] [1] 22.45/12.39 [0 0 0 0] x + [0] 22.45/12.39 [0 0 0 0] [0] 22.45/12.39 [0 0 0 0] [0] 22.45/12.39 = [u(b(d(x)))] 22.45/12.39 22.45/12.39 [v(c(x))] = [1 0 0 0] [1] 22.45/12.39 [0 0 0 0] x + [0] 22.45/12.39 [0 0 0 0] [0] 22.45/12.39 [0 0 0 0] [0] 22.45/12.39 > [1 0 0 0] [0] 22.45/12.39 [0 0 0 0] x + [0] 22.45/12.39 [0 0 0 0] [0] 22.45/12.39 [0 0 0 0] [0] 22.45/12.39 = [b(x)] 22.45/12.39 22.45/12.39 [w(a(a(x)))] = [1 0 0 0] [2] 22.45/12.39 [0 0 0 0] x + [0] 22.45/12.39 [0 0 0 0] [0] 22.45/12.39 [0 0 0 1] [0] 22.45/12.39 > [1 0 0 0] [1] 22.45/12.39 [0 0 0 0] x + [0] 22.45/12.39 [0 0 0 0] [0] 22.45/12.39 [0 0 0 0] [0] 22.45/12.39 = [u(w(x))] 22.45/12.39 22.45/12.39 [w(a(c(x)))] = [1 0 0 0] [2] 22.45/12.39 [0 0 0 0] x + [0] 22.45/12.39 [0 0 0 0] [0] 22.45/12.39 [0 0 0 0] [0] 22.45/12.39 > [1 0 0 0] [1] 22.45/12.39 [0 0 0 0] x + [0] 22.45/12.39 [0 0 0 0] [0] 22.45/12.39 [0 0 0 0] [0] 22.45/12.39 = [u(b(d(x)))] 22.45/12.39 22.45/12.39 [w(c(x))] = [1 0 0 0] [1] 22.45/12.39 [0 0 0 0] x + [0] 22.45/12.39 [0 0 0 0] [0] 22.45/12.39 [0 0 0 0] [0] 22.45/12.39 > [1 0 0 0] [0] 22.45/12.39 [0 0 0 0] x + [0] 22.45/12.39 [0 0 0 0] [0] 22.45/12.39 [0 0 0 0] [0] 22.45/12.39 = [b(x)] 22.45/12.39 22.45/12.39 22.45/12.39 Hurray, we answered YES(?,O(n^1)) 22.61/12.42 EOF