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