YES
O(n^3)
TRS:
{
__(X, nil()) -> X,
__(X1, X2) -> n____(X1, X2),
__(__(X, Y), Z) -> __(X, __(Y, Z)),
__(nil(), X) -> X,
nil() -> n__nil(),
U11(tt()) -> tt(),
U22(tt()) -> tt(),
isList(V) -> U11(isNeList(activate(V))),
isList(n__nil()) -> tt(),
isList(n____(V1, V2)) -> U21(isList(activate(V1)), activate(V2)),
activate(X) -> X,
activate(n__nil()) -> nil(),
activate(n____(X1, X2)) -> __(X1, X2),
activate(n__a()) -> a(),
activate(n__e()) -> e(),
activate(n__i()) -> i(),
activate(n__o()) -> o(),
activate(n__u()) -> u(),
U21(tt(), V2) -> U22(isList(activate(V2))),
U31(tt()) -> tt(),
U42(tt()) -> tt(),
isNeList(V) -> U31(isQid(activate(V))),
isNeList(n____(V1, V2)) -> U41(isList(activate(V1)), activate(V2)),
isNeList(n____(V1, V2)) -> U51(isNeList(activate(V1)), activate(V2)),
U41(tt(), V2) -> U42(isNeList(activate(V2))),
U52(tt()) -> tt(),
U51(tt(), V2) -> U52(isList(activate(V2))),
U61(tt()) -> tt(),
U72(tt()) -> tt(),
isPal(V) -> U81(isNePal(activate(V))),
isPal(n__nil()) -> tt(),
U71(tt(), P) -> U72(isPal(activate(P))),
U81(tt()) -> tt(),
isQid(n__a()) -> tt(),
isQid(n__e()) -> tt(),
isQid(n__i()) -> tt(),
isQid(n__o()) -> tt(),
isQid(n__u()) -> tt(),
isNePal(V) -> U61(isQid(activate(V))),
isNePal(n____(I, __(P, I))) -> U71(isQid(activate(I)), activate(P)),
a() -> n__a(),
e() -> n__e(),
i() -> n__i(),
o() -> n__o(),
u() -> n__u()
}
DUP: We consider a non-duplicating system.
Trs:
{
__(X, nil()) -> X,
__(X1, X2) -> n____(X1, X2),
__(__(X, Y), Z) -> __(X, __(Y, Z)),
__(nil(), X) -> X,
nil() -> n__nil(),
U11(tt()) -> tt(),
U22(tt()) -> tt(),
isList(V) -> U11(isNeList(activate(V))),
isList(n__nil()) -> tt(),
isList(n____(V1, V2)) -> U21(isList(activate(V1)), activate(V2)),
activate(X) -> X,
activate(n__nil()) -> nil(),
activate(n____(X1, X2)) -> __(X1, X2),
activate(n__a()) -> a(),
activate(n__e()) -> e(),
activate(n__i()) -> i(),
activate(n__o()) -> o(),
activate(n__u()) -> u(),
U21(tt(), V2) -> U22(isList(activate(V2))),
U31(tt()) -> tt(),
U42(tt()) -> tt(),
isNeList(V) -> U31(isQid(activate(V))),
isNeList(n____(V1, V2)) -> U41(isList(activate(V1)), activate(V2)),
isNeList(n____(V1, V2)) -> U51(isNeList(activate(V1)), activate(V2)),
U41(tt(), V2) -> U42(isNeList(activate(V2))),
U52(tt()) -> tt(),
U51(tt(), V2) -> U52(isList(activate(V2))),
U61(tt()) -> tt(),
U72(tt()) -> tt(),
isPal(V) -> U81(isNePal(activate(V))),
isPal(n__nil()) -> tt(),
U71(tt(), P) -> U72(isPal(activate(P))),
U81(tt()) -> tt(),
isQid(n__a()) -> tt(),
isQid(n__e()) -> tt(),
isQid(n__i()) -> tt(),
isQid(n__o()) -> tt(),
isQid(n__u()) -> tt(),
isNePal(V) -> U61(isQid(activate(V))),
isNePal(n____(I, __(P, I))) -> U71(isQid(activate(I)), activate(P)),
a() -> n__a(),
e() -> n__e(),
i() -> n__i(),
o() -> n__o(),
u() -> n__u()
}
Matrix Interpretation:
Interpretation class: triangular
[7]
[u] = [0]
[4]
[7]
[o] = [1]
[4]
[7]
[i] = [0]
[4]
[7]
[e] = [7]
[4]
[7]
[a] = [0]
[4]
[6]
[n__u] = [0]
[4]
[6]
[n__o] = [1]
[4]
[6]
[n__i] = [0]
[4]
[6]
[n__e] = [7]
[4]
[6]
[n__a] = [0]
[4]
[X2] [1 1 4][X2] [3]
[isNePal]([X1]) = [0 0 1][X1] + [0]
[X0] [0 0 0][X0] [0]
[X2] [1 0 0][X2] [0]
[isQid]([X1]) = [0 0 1][X1] + [0]
[X0] [0 0 0][X0] [4]
[X5] [X2] [1 1 7][X5] [1 0 0][X2] [6]
[n____]([X4], [X1]) = [0 1 0][X4] + [0 1 0][X1] + [0]
[X3] [X0] [0 0 1][X3] [0 0 1][X0] [4]
[3]
[n__nil] = [0]
[4]
[X2] [1 2 0][X2] [0]
[U81]([X1]) = [0 0 0][X1] + [4]
[X0] [0 0 0][X0] [0]
[X5] [X2] [1 7 0][X5] [1 2 7][X2] [0]
[U71]([X4], [X1]) = [0 1 0][X4] + [0 0 1][X1] + [0]
[X3] [X0] [0 0 0][X3] [0 0 0][X0] [0]
[X2] [1 2 6][X2] [7]
[isPal]([X1]) = [0 0 1][X1] + [4]
[X0] [0 0 0][X0] [2]
[X2] [1 1 4][X2] [0]
[U72]([X1]) = [0 1 0][X1] + [0]
[X0] [0 0 0][X0] [0]
[X2] [1 4 0][X2] [0]
[U61]([X1]) = [0 1 0][X1] + [0]
[X0] [0 0 0][X0] [0]
[X5] [X2] [1 4 0][X5] [1 0 1][X2] [0]
[U51]([X4], [X1]) = [0 1 0][X4] + [0 0 0][X1] + [4]
[X3] [X0] [0 0 0][X3] [0 0 0][X0] [0]
[X2] [1 0 0][X2] [2]
[U52]([X1]) = [0 0 0][X1] + [4]
[X0] [0 0 0][X0] [0]
[X5] [X2] [1 2 0][X5] [1 0 1][X2] [1]
[U41]([X4], [X1]) = [0 0 0][X4] + [0 0 1][X1] + [0]
[X3] [X0] [0 0 0][X3] [0 0 0][X0] [0]
[X2] [1 0 1][X2] [3]
[isNeList]([X1]) = [0 0 1][X1] + [0]
[X0] [0 0 0][X0] [4]
[X2] [1 0 0][X2] [7]
[U42]([X1]) = [0 1 0][X1] + [0]
[X0] [0 0 0][X0] [0]
[X2] [1 1 0][X2] [0]
[U31]([X1]) = [0 1 0][X1] + [0]
[X0] [0 0 0][X0] [0]
[X5] [X2] [1 7 0][X5] [1 0 1][X2] [0]
[U21]([X4], [X1]) = [0 0 0][X4] + [0 0 1][X1] + [0]
[X3] [X0] [0 0 0][X3] [0 0 0][X0] [0]
[X2] [1 0 0][X2] [2]
[activate]([X1]) = [0 1 0][X1] + [1]
[X0] [0 0 1][X0] [0]
[X2] [1 0 1][X2] [7]
[isList]([X1]) = [0 0 1][X1] + [0]
[X0] [0 0 0][X0] [4]
[X2] [1 0 2][X2] [1]
[U22]([X1]) = [0 1 0][X1] + [0]
[X0] [0 0 0][X0] [0]
[X2] [1 0 0][X2] [1]
[U11]([X1]) = [0 1 0][X1] + [0]
[X0] [0 0 0][X0] [0]
[5]
[tt] = [4]
[0]
[4]
[nil] = [0]
[4]
[X5] [X2] [1 1 7][X5] [1 0 0][X2] [7]
[__]([X4], [X1]) = [0 1 0][X4] + [0 1 0][X1] + [1]
[X3] [X0] [0 0 1][X3] [0 0 1][X0] [4]
Qed