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