We are left with following problem, upon which TcT provides the
certificate YES(O(1),O(n^1)).
Strict Trs:
{ __(X1, X2) -> n____(X1, X2)
, __(X, nil()) -> X
, __(__(X, Y), Z) -> __(X, __(Y, Z))
, __(nil(), X) -> X
, nil() -> n__nil()
, and(tt(), X) -> activate(X)
, activate(X) -> X
, activate(n__nil()) -> nil()
, activate(n____(X1, X2)) -> __(X1, X2)
, activate(n__isList(X)) -> isList(X)
, activate(n__isNeList(X)) -> isNeList(X)
, activate(n__isPal(X)) -> isPal(X)
, activate(n__a()) -> a()
, activate(n__e()) -> e()
, activate(n__i()) -> i()
, activate(n__o()) -> o()
, activate(n__u()) -> u()
, isList(V) -> isNeList(activate(V))
, isList(X) -> n__isList(X)
, isList(n__nil()) -> tt()
, isList(n____(V1, V2)) ->
and(isList(activate(V1)), n__isList(activate(V2)))
, isNeList(V) -> isQid(activate(V))
, isNeList(X) -> n__isNeList(X)
, isNeList(n____(V1, V2)) ->
and(isList(activate(V1)), n__isNeList(activate(V2)))
, isNeList(n____(V1, V2)) ->
and(isNeList(activate(V1)), n__isList(activate(V2)))
, isQid(n__a()) -> tt()
, isQid(n__e()) -> tt()
, isQid(n__i()) -> tt()
, isQid(n__o()) -> tt()
, isQid(n__u()) -> tt()
, isNePal(V) -> isQid(activate(V))
, isNePal(n____(I, __(P, I))) ->
and(isQid(activate(I)), n__isPal(activate(P)))
, isPal(V) -> isNePal(activate(V))
, isPal(X) -> n__isPal(X)
, isPal(n__nil()) -> tt()
, a() -> n__a()
, e() -> n__e()
, i() -> n__i()
, o() -> n__o()
, u() -> n__u() }
Obligation:
runtime complexity
Answer:
YES(O(1),O(n^1))
The weightgap principle applies (using the following nonconstant
growth matrix-interpretation)
The following argument positions are usable:
Uargs(__) = {2}, Uargs(and) = {1, 2}, Uargs(activate) = {1},
Uargs(isList) = {1}, Uargs(isNeList) = {1}, Uargs(n____) = {2},
Uargs(n__isList) = {1}, Uargs(isQid) = {1},
Uargs(n__isNeList) = {1}, Uargs(isNePal) = {1},
Uargs(n__isPal) = {1}, Uargs(isPal) = {1}
TcT has computed the following matrix interpretation satisfying
not(EDA) and not(IDA(1)).
[__](x1, x2) = [1] x1 + [1] x2 + [0]
[nil] = [1]
[and](x1, x2) = [1] x1 + [1] x2 + [0]
[tt] = [0]
[activate](x1) = [1] x1 + [0]
[isList](x1) = [1] x1 + [0]
[isNeList](x1) = [1] x1 + [0]
[n__nil] = [5]
[n____](x1, x2) = [1] x1 + [1] x2 + [0]
[n__isList](x1) = [1] x1 + [0]
[isQid](x1) = [1] x1 + [0]
[n__isNeList](x1) = [1] x1 + [0]
[isNePal](x1) = [1] x1 + [0]
[n__isPal](x1) = [1] x1 + [0]
[isPal](x1) = [1] x1 + [0]
[n__a] = [0]
[n__e] = [0]
[n__i] = [0]
[n__o] = [0]
[n__u] = [0]
[a] = [0]
[e] = [0]
[i] = [0]
[o] = [0]
[u] = [1]
The order satisfies the following ordering constraints:
[__(X1, X2)] = [1] X1 + [1] X2 + [0]
>= [1] X1 + [1] X2 + [0]
= [n____(X1, X2)]
[__(X, nil())] = [1] X + [1]
> [1] X + [0]
= [X]
[__(__(X, Y), Z)] = [1] X + [1] Y + [1] Z + [0]
>= [1] X + [1] Y + [1] Z + [0]
= [__(X, __(Y, Z))]
[__(nil(), X)] = [1] X + [1]
> [1] X + [0]
= [X]
[nil()] = [1]
? [5]
= [n__nil()]
[and(tt(), X)] = [1] X + [0]
>= [1] X + [0]
= [activate(X)]
[activate(X)] = [1] X + [0]
>= [1] X + [0]
= [X]
[activate(n__nil())] = [5]
> [1]
= [nil()]
[activate(n____(X1, X2))] = [1] X1 + [1] X2 + [0]
>= [1] X1 + [1] X2 + [0]
= [__(X1, X2)]
[activate(n__isList(X))] = [1] X + [0]
>= [1] X + [0]
= [isList(X)]
[activate(n__isNeList(X))] = [1] X + [0]
>= [1] X + [0]
= [isNeList(X)]
[activate(n__isPal(X))] = [1] X + [0]
>= [1] X + [0]
= [isPal(X)]
[activate(n__a())] = [0]
>= [0]
= [a()]
[activate(n__e())] = [0]
>= [0]
= [e()]
[activate(n__i())] = [0]
>= [0]
= [i()]
[activate(n__o())] = [0]
>= [0]
= [o()]
[activate(n__u())] = [0]
? [1]
= [u()]
[isList(V)] = [1] V + [0]
>= [1] V + [0]
= [isNeList(activate(V))]
[isList(X)] = [1] X + [0]
>= [1] X + [0]
= [n__isList(X)]
[isList(n__nil())] = [5]
> [0]
= [tt()]
[isList(n____(V1, V2))] = [1] V1 + [1] V2 + [0]
>= [1] V1 + [1] V2 + [0]
= [and(isList(activate(V1)), n__isList(activate(V2)))]
[isNeList(V)] = [1] V + [0]
>= [1] V + [0]
= [isQid(activate(V))]
[isNeList(X)] = [1] X + [0]
>= [1] X + [0]
= [n__isNeList(X)]
[isNeList(n____(V1, V2))] = [1] V1 + [1] V2 + [0]
>= [1] V1 + [1] V2 + [0]
= [and(isList(activate(V1)), n__isNeList(activate(V2)))]
[isNeList(n____(V1, V2))] = [1] V1 + [1] V2 + [0]
>= [1] V1 + [1] V2 + [0]
= [and(isNeList(activate(V1)), n__isList(activate(V2)))]
[isQid(n__a())] = [0]
>= [0]
= [tt()]
[isQid(n__e())] = [0]
>= [0]
= [tt()]
[isQid(n__i())] = [0]
>= [0]
= [tt()]
[isQid(n__o())] = [0]
>= [0]
= [tt()]
[isQid(n__u())] = [0]
>= [0]
= [tt()]
[isNePal(V)] = [1] V + [0]
>= [1] V + [0]
= [isQid(activate(V))]
[isNePal(n____(I, __(P, I)))] = [2] I + [1] P + [0]
>= [1] I + [1] P + [0]
= [and(isQid(activate(I)), n__isPal(activate(P)))]
[isPal(V)] = [1] V + [0]
>= [1] V + [0]
= [isNePal(activate(V))]
[isPal(X)] = [1] X + [0]
>= [1] X + [0]
= [n__isPal(X)]
[isPal(n__nil())] = [5]
> [0]
= [tt()]
[a()] = [0]
>= [0]
= [n__a()]
[e()] = [0]
>= [0]
= [n__e()]
[i()] = [0]
>= [0]
= [n__i()]
[o()] = [0]
>= [0]
= [n__o()]
[u()] = [1]
> [0]
= [n__u()]
Further, it can be verified that all rules not oriented are covered by the weightgap condition.
We are left with following problem, upon which TcT provides the
certificate YES(O(1),O(n^1)).
Strict Trs:
{ __(X1, X2) -> n____(X1, X2)
, __(__(X, Y), Z) -> __(X, __(Y, Z))
, nil() -> n__nil()
, and(tt(), X) -> activate(X)
, activate(X) -> X
, activate(n____(X1, X2)) -> __(X1, X2)
, activate(n__isList(X)) -> isList(X)
, activate(n__isNeList(X)) -> isNeList(X)
, activate(n__isPal(X)) -> isPal(X)
, activate(n__a()) -> a()
, activate(n__e()) -> e()
, activate(n__i()) -> i()
, activate(n__o()) -> o()
, activate(n__u()) -> u()
, isList(V) -> isNeList(activate(V))
, isList(X) -> n__isList(X)
, isList(n____(V1, V2)) ->
and(isList(activate(V1)), n__isList(activate(V2)))
, isNeList(V) -> isQid(activate(V))
, isNeList(X) -> n__isNeList(X)
, isNeList(n____(V1, V2)) ->
and(isList(activate(V1)), n__isNeList(activate(V2)))
, isNeList(n____(V1, V2)) ->
and(isNeList(activate(V1)), n__isList(activate(V2)))
, isQid(n__a()) -> tt()
, isQid(n__e()) -> tt()
, isQid(n__i()) -> tt()
, isQid(n__o()) -> tt()
, isQid(n__u()) -> tt()
, isNePal(V) -> isQid(activate(V))
, isNePal(n____(I, __(P, I))) ->
and(isQid(activate(I)), n__isPal(activate(P)))
, isPal(V) -> isNePal(activate(V))
, isPal(X) -> n__isPal(X)
, a() -> n__a()
, e() -> n__e()
, i() -> n__i()
, o() -> n__o() }
Weak Trs:
{ __(X, nil()) -> X
, __(nil(), X) -> X
, activate(n__nil()) -> nil()
, isList(n__nil()) -> tt()
, isPal(n__nil()) -> tt()
, u() -> n__u() }
Obligation:
runtime complexity
Answer:
YES(O(1),O(n^1))
The weightgap principle applies (using the following nonconstant
growth matrix-interpretation)
The following argument positions are usable:
Uargs(__) = {2}, Uargs(and) = {1, 2}, Uargs(activate) = {1},
Uargs(isList) = {1}, Uargs(isNeList) = {1}, Uargs(n____) = {2},
Uargs(n__isList) = {1}, Uargs(isQid) = {1},
Uargs(n__isNeList) = {1}, Uargs(isNePal) = {1},
Uargs(n__isPal) = {1}, Uargs(isPal) = {1}
TcT has computed the following matrix interpretation satisfying
not(EDA) and not(IDA(1)).
[__](x1, x2) = [1] x1 + [1] x2 + [0]
[nil] = [0]
[and](x1, x2) = [1] x1 + [1] x2 + [0]
[tt] = [0]
[activate](x1) = [1] x1 + [0]
[isList](x1) = [1] x1 + [4]
[isNeList](x1) = [1] x1 + [0]
[n__nil] = [0]
[n____](x1, x2) = [1] x1 + [1] x2 + [0]
[n__isList](x1) = [1] x1 + [4]
[isQid](x1) = [1] x1 + [0]
[n__isNeList](x1) = [1] x1 + [4]
[isNePal](x1) = [1] x1 + [0]
[n__isPal](x1) = [1] x1 + [0]
[isPal](x1) = [1] x1 + [4]
[n__a] = [0]
[n__e] = [0]
[n__i] = [0]
[n__o] = [0]
[n__u] = [0]
[a] = [0]
[e] = [2]
[i] = [0]
[o] = [2]
[u] = [5]
The order satisfies the following ordering constraints:
[__(X1, X2)] = [1] X1 + [1] X2 + [0]
>= [1] X1 + [1] X2 + [0]
= [n____(X1, X2)]
[__(X, nil())] = [1] X + [0]
>= [1] X + [0]
= [X]
[__(__(X, Y), Z)] = [1] X + [1] Y + [1] Z + [0]
>= [1] X + [1] Y + [1] Z + [0]
= [__(X, __(Y, Z))]
[__(nil(), X)] = [1] X + [0]
>= [1] X + [0]
= [X]
[nil()] = [0]
>= [0]
= [n__nil()]
[and(tt(), X)] = [1] X + [0]
>= [1] X + [0]
= [activate(X)]
[activate(X)] = [1] X + [0]
>= [1] X + [0]
= [X]
[activate(n__nil())] = [0]
>= [0]
= [nil()]
[activate(n____(X1, X2))] = [1] X1 + [1] X2 + [0]
>= [1] X1 + [1] X2 + [0]
= [__(X1, X2)]
[activate(n__isList(X))] = [1] X + [4]
>= [1] X + [4]
= [isList(X)]
[activate(n__isNeList(X))] = [1] X + [4]
> [1] X + [0]
= [isNeList(X)]
[activate(n__isPal(X))] = [1] X + [0]
? [1] X + [4]
= [isPal(X)]
[activate(n__a())] = [0]
>= [0]
= [a()]
[activate(n__e())] = [0]
? [2]
= [e()]
[activate(n__i())] = [0]
>= [0]
= [i()]
[activate(n__o())] = [0]
? [2]
= [o()]
[activate(n__u())] = [0]
? [5]
= [u()]
[isList(V)] = [1] V + [4]
> [1] V + [0]
= [isNeList(activate(V))]
[isList(X)] = [1] X + [4]
>= [1] X + [4]
= [n__isList(X)]
[isList(n__nil())] = [4]
> [0]
= [tt()]
[isList(n____(V1, V2))] = [1] V1 + [1] V2 + [4]
? [1] V1 + [1] V2 + [8]
= [and(isList(activate(V1)), n__isList(activate(V2)))]
[isNeList(V)] = [1] V + [0]
>= [1] V + [0]
= [isQid(activate(V))]
[isNeList(X)] = [1] X + [0]
? [1] X + [4]
= [n__isNeList(X)]
[isNeList(n____(V1, V2))] = [1] V1 + [1] V2 + [0]
? [1] V1 + [1] V2 + [8]
= [and(isList(activate(V1)), n__isNeList(activate(V2)))]
[isNeList(n____(V1, V2))] = [1] V1 + [1] V2 + [0]
? [1] V1 + [1] V2 + [4]
= [and(isNeList(activate(V1)), n__isList(activate(V2)))]
[isQid(n__a())] = [0]
>= [0]
= [tt()]
[isQid(n__e())] = [0]
>= [0]
= [tt()]
[isQid(n__i())] = [0]
>= [0]
= [tt()]
[isQid(n__o())] = [0]
>= [0]
= [tt()]
[isQid(n__u())] = [0]
>= [0]
= [tt()]
[isNePal(V)] = [1] V + [0]
>= [1] V + [0]
= [isQid(activate(V))]
[isNePal(n____(I, __(P, I)))] = [2] I + [1] P + [0]
>= [1] I + [1] P + [0]
= [and(isQid(activate(I)), n__isPal(activate(P)))]
[isPal(V)] = [1] V + [4]
> [1] V + [0]
= [isNePal(activate(V))]
[isPal(X)] = [1] X + [4]
> [1] X + [0]
= [n__isPal(X)]
[isPal(n__nil())] = [4]
> [0]
= [tt()]
[a()] = [0]
>= [0]
= [n__a()]
[e()] = [2]
> [0]
= [n__e()]
[i()] = [0]
>= [0]
= [n__i()]
[o()] = [2]
> [0]
= [n__o()]
[u()] = [5]
> [0]
= [n__u()]
Further, it can be verified that all rules not oriented are covered by the weightgap condition.
We are left with following problem, upon which TcT provides the
certificate YES(O(1),O(n^1)).
Strict Trs:
{ __(X1, X2) -> n____(X1, X2)
, __(__(X, Y), Z) -> __(X, __(Y, Z))
, nil() -> n__nil()
, and(tt(), X) -> activate(X)
, activate(X) -> X
, activate(n____(X1, X2)) -> __(X1, X2)
, activate(n__isList(X)) -> isList(X)
, activate(n__isPal(X)) -> isPal(X)
, activate(n__a()) -> a()
, activate(n__e()) -> e()
, activate(n__i()) -> i()
, activate(n__o()) -> o()
, activate(n__u()) -> u()
, isList(X) -> n__isList(X)
, isList(n____(V1, V2)) ->
and(isList(activate(V1)), n__isList(activate(V2)))
, isNeList(V) -> isQid(activate(V))
, isNeList(X) -> n__isNeList(X)
, isNeList(n____(V1, V2)) ->
and(isList(activate(V1)), n__isNeList(activate(V2)))
, isNeList(n____(V1, V2)) ->
and(isNeList(activate(V1)), n__isList(activate(V2)))
, isQid(n__a()) -> tt()
, isQid(n__e()) -> tt()
, isQid(n__i()) -> tt()
, isQid(n__o()) -> tt()
, isQid(n__u()) -> tt()
, isNePal(V) -> isQid(activate(V))
, isNePal(n____(I, __(P, I))) ->
and(isQid(activate(I)), n__isPal(activate(P)))
, a() -> n__a()
, i() -> n__i() }
Weak Trs:
{ __(X, nil()) -> X
, __(nil(), X) -> X
, activate(n__nil()) -> nil()
, activate(n__isNeList(X)) -> isNeList(X)
, isList(V) -> isNeList(activate(V))
, isList(n__nil()) -> tt()
, isPal(V) -> isNePal(activate(V))
, isPal(X) -> n__isPal(X)
, isPal(n__nil()) -> tt()
, e() -> n__e()
, o() -> n__o()
, u() -> n__u() }
Obligation:
runtime complexity
Answer:
YES(O(1),O(n^1))
The weightgap principle applies (using the following nonconstant
growth matrix-interpretation)
The following argument positions are usable:
Uargs(__) = {2}, Uargs(and) = {1, 2}, Uargs(activate) = {1},
Uargs(isList) = {1}, Uargs(isNeList) = {1}, Uargs(n____) = {2},
Uargs(n__isList) = {1}, Uargs(isQid) = {1},
Uargs(n__isNeList) = {1}, Uargs(isNePal) = {1},
Uargs(n__isPal) = {1}, Uargs(isPal) = {1}
TcT has computed the following matrix interpretation satisfying
not(EDA) and not(IDA(1)).
[__](x1, x2) = [1] x1 + [1] x2 + [0]
[nil] = [0]
[and](x1, x2) = [1] x1 + [1] x2 + [0]
[tt] = [0]
[activate](x1) = [1] x1 + [0]
[isList](x1) = [1] x1 + [4]
[isNeList](x1) = [1] x1 + [0]
[n__nil] = [0]
[n____](x1, x2) = [1] x1 + [1] x2 + [4]
[n__isList](x1) = [1] x1 + [0]
[isQid](x1) = [1] x1 + [0]
[n__isNeList](x1) = [1] x1 + [4]
[isNePal](x1) = [1] x1 + [0]
[n__isPal](x1) = [1] x1 + [0]
[isPal](x1) = [1] x1 + [4]
[n__a] = [0]
[n__e] = [0]
[n__i] = [0]
[n__o] = [0]
[n__u] = [0]
[a] = [0]
[e] = [5]
[i] = [1]
[o] = [5]
[u] = [5]
The order satisfies the following ordering constraints:
[__(X1, X2)] = [1] X1 + [1] X2 + [0]
? [1] X1 + [1] X2 + [4]
= [n____(X1, X2)]
[__(X, nil())] = [1] X + [0]
>= [1] X + [0]
= [X]
[__(__(X, Y), Z)] = [1] X + [1] Y + [1] Z + [0]
>= [1] X + [1] Y + [1] Z + [0]
= [__(X, __(Y, Z))]
[__(nil(), X)] = [1] X + [0]
>= [1] X + [0]
= [X]
[nil()] = [0]
>= [0]
= [n__nil()]
[and(tt(), X)] = [1] X + [0]
>= [1] X + [0]
= [activate(X)]
[activate(X)] = [1] X + [0]
>= [1] X + [0]
= [X]
[activate(n__nil())] = [0]
>= [0]
= [nil()]
[activate(n____(X1, X2))] = [1] X1 + [1] X2 + [4]
> [1] X1 + [1] X2 + [0]
= [__(X1, X2)]
[activate(n__isList(X))] = [1] X + [0]
? [1] X + [4]
= [isList(X)]
[activate(n__isNeList(X))] = [1] X + [4]
> [1] X + [0]
= [isNeList(X)]
[activate(n__isPal(X))] = [1] X + [0]
? [1] X + [4]
= [isPal(X)]
[activate(n__a())] = [0]
>= [0]
= [a()]
[activate(n__e())] = [0]
? [5]
= [e()]
[activate(n__i())] = [0]
? [1]
= [i()]
[activate(n__o())] = [0]
? [5]
= [o()]
[activate(n__u())] = [0]
? [5]
= [u()]
[isList(V)] = [1] V + [4]
> [1] V + [0]
= [isNeList(activate(V))]
[isList(X)] = [1] X + [4]
> [1] X + [0]
= [n__isList(X)]
[isList(n__nil())] = [4]
> [0]
= [tt()]
[isList(n____(V1, V2))] = [1] V1 + [1] V2 + [8]
> [1] V1 + [1] V2 + [4]
= [and(isList(activate(V1)), n__isList(activate(V2)))]
[isNeList(V)] = [1] V + [0]
>= [1] V + [0]
= [isQid(activate(V))]
[isNeList(X)] = [1] X + [0]
? [1] X + [4]
= [n__isNeList(X)]
[isNeList(n____(V1, V2))] = [1] V1 + [1] V2 + [4]
? [1] V1 + [1] V2 + [8]
= [and(isList(activate(V1)), n__isNeList(activate(V2)))]
[isNeList(n____(V1, V2))] = [1] V1 + [1] V2 + [4]
> [1] V1 + [1] V2 + [0]
= [and(isNeList(activate(V1)), n__isList(activate(V2)))]
[isQid(n__a())] = [0]
>= [0]
= [tt()]
[isQid(n__e())] = [0]
>= [0]
= [tt()]
[isQid(n__i())] = [0]
>= [0]
= [tt()]
[isQid(n__o())] = [0]
>= [0]
= [tt()]
[isQid(n__u())] = [0]
>= [0]
= [tt()]
[isNePal(V)] = [1] V + [0]
>= [1] V + [0]
= [isQid(activate(V))]
[isNePal(n____(I, __(P, I)))] = [2] I + [1] P + [4]
> [1] I + [1] P + [0]
= [and(isQid(activate(I)), n__isPal(activate(P)))]
[isPal(V)] = [1] V + [4]
> [1] V + [0]
= [isNePal(activate(V))]
[isPal(X)] = [1] X + [4]
> [1] X + [0]
= [n__isPal(X)]
[isPal(n__nil())] = [4]
> [0]
= [tt()]
[a()] = [0]
>= [0]
= [n__a()]
[e()] = [5]
> [0]
= [n__e()]
[i()] = [1]
> [0]
= [n__i()]
[o()] = [5]
> [0]
= [n__o()]
[u()] = [5]
> [0]
= [n__u()]
Further, it can be verified that all rules not oriented are covered by the weightgap condition.
We are left with following problem, upon which TcT provides the
certificate YES(O(1),O(n^1)).
Strict Trs:
{ __(X1, X2) -> n____(X1, X2)
, __(__(X, Y), Z) -> __(X, __(Y, Z))
, nil() -> n__nil()
, and(tt(), X) -> activate(X)
, activate(X) -> X
, activate(n__isList(X)) -> isList(X)
, activate(n__isPal(X)) -> isPal(X)
, activate(n__a()) -> a()
, activate(n__e()) -> e()
, activate(n__i()) -> i()
, activate(n__o()) -> o()
, activate(n__u()) -> u()
, isNeList(V) -> isQid(activate(V))
, isNeList(X) -> n__isNeList(X)
, isNeList(n____(V1, V2)) ->
and(isList(activate(V1)), n__isNeList(activate(V2)))
, isQid(n__a()) -> tt()
, isQid(n__e()) -> tt()
, isQid(n__i()) -> tt()
, isQid(n__o()) -> tt()
, isQid(n__u()) -> tt()
, isNePal(V) -> isQid(activate(V))
, a() -> n__a() }
Weak Trs:
{ __(X, nil()) -> X
, __(nil(), X) -> X
, activate(n__nil()) -> nil()
, activate(n____(X1, X2)) -> __(X1, X2)
, activate(n__isNeList(X)) -> isNeList(X)
, isList(V) -> isNeList(activate(V))
, isList(X) -> n__isList(X)
, isList(n__nil()) -> tt()
, isList(n____(V1, V2)) ->
and(isList(activate(V1)), n__isList(activate(V2)))
, isNeList(n____(V1, V2)) ->
and(isNeList(activate(V1)), n__isList(activate(V2)))
, isNePal(n____(I, __(P, I))) ->
and(isQid(activate(I)), n__isPal(activate(P)))
, isPal(V) -> isNePal(activate(V))
, isPal(X) -> n__isPal(X)
, isPal(n__nil()) -> tt()
, e() -> n__e()
, i() -> n__i()
, o() -> n__o()
, u() -> n__u() }
Obligation:
runtime complexity
Answer:
YES(O(1),O(n^1))
The weightgap principle applies (using the following nonconstant
growth matrix-interpretation)
The following argument positions are usable:
Uargs(__) = {2}, Uargs(and) = {1, 2}, Uargs(activate) = {1},
Uargs(isList) = {1}, Uargs(isNeList) = {1}, Uargs(n____) = {2},
Uargs(n__isList) = {1}, Uargs(isQid) = {1},
Uargs(n__isNeList) = {1}, Uargs(isNePal) = {1},
Uargs(n__isPal) = {1}, Uargs(isPal) = {1}
TcT has computed the following matrix interpretation satisfying
not(EDA) and not(IDA(1)).
[__](x1, x2) = [1] x1 + [1] x2 + [0]
[nil] = [0]
[and](x1, x2) = [1] x1 + [1] x2 + [0]
[tt] = [0]
[activate](x1) = [1] x1 + [0]
[isList](x1) = [1] x1 + [5]
[isNeList](x1) = [1] x1 + [1]
[n__nil] = [0]
[n____](x1, x2) = [1] x1 + [1] x2 + [4]
[n__isList](x1) = [1] x1 + [0]
[isQid](x1) = [1] x1 + [0]
[n__isNeList](x1) = [1] x1 + [4]
[isNePal](x1) = [1] x1 + [0]
[n__isPal](x1) = [1] x1 + [0]
[isPal](x1) = [1] x1 + [4]
[n__a] = [0]
[n__e] = [0]
[n__i] = [0]
[n__o] = [0]
[n__u] = [0]
[a] = [2]
[e] = [5]
[i] = [5]
[o] = [5]
[u] = [5]
The order satisfies the following ordering constraints:
[__(X1, X2)] = [1] X1 + [1] X2 + [0]
? [1] X1 + [1] X2 + [4]
= [n____(X1, X2)]
[__(X, nil())] = [1] X + [0]
>= [1] X + [0]
= [X]
[__(__(X, Y), Z)] = [1] X + [1] Y + [1] Z + [0]
>= [1] X + [1] Y + [1] Z + [0]
= [__(X, __(Y, Z))]
[__(nil(), X)] = [1] X + [0]
>= [1] X + [0]
= [X]
[nil()] = [0]
>= [0]
= [n__nil()]
[and(tt(), X)] = [1] X + [0]
>= [1] X + [0]
= [activate(X)]
[activate(X)] = [1] X + [0]
>= [1] X + [0]
= [X]
[activate(n__nil())] = [0]
>= [0]
= [nil()]
[activate(n____(X1, X2))] = [1] X1 + [1] X2 + [4]
> [1] X1 + [1] X2 + [0]
= [__(X1, X2)]
[activate(n__isList(X))] = [1] X + [0]
? [1] X + [5]
= [isList(X)]
[activate(n__isNeList(X))] = [1] X + [4]
> [1] X + [1]
= [isNeList(X)]
[activate(n__isPal(X))] = [1] X + [0]
? [1] X + [4]
= [isPal(X)]
[activate(n__a())] = [0]
? [2]
= [a()]
[activate(n__e())] = [0]
? [5]
= [e()]
[activate(n__i())] = [0]
? [5]
= [i()]
[activate(n__o())] = [0]
? [5]
= [o()]
[activate(n__u())] = [0]
? [5]
= [u()]
[isList(V)] = [1] V + [5]
> [1] V + [1]
= [isNeList(activate(V))]
[isList(X)] = [1] X + [5]
> [1] X + [0]
= [n__isList(X)]
[isList(n__nil())] = [5]
> [0]
= [tt()]
[isList(n____(V1, V2))] = [1] V1 + [1] V2 + [9]
> [1] V1 + [1] V2 + [5]
= [and(isList(activate(V1)), n__isList(activate(V2)))]
[isNeList(V)] = [1] V + [1]
> [1] V + [0]
= [isQid(activate(V))]
[isNeList(X)] = [1] X + [1]
? [1] X + [4]
= [n__isNeList(X)]
[isNeList(n____(V1, V2))] = [1] V1 + [1] V2 + [5]
? [1] V1 + [1] V2 + [9]
= [and(isList(activate(V1)), n__isNeList(activate(V2)))]
[isNeList(n____(V1, V2))] = [1] V1 + [1] V2 + [5]
> [1] V1 + [1] V2 + [1]
= [and(isNeList(activate(V1)), n__isList(activate(V2)))]
[isQid(n__a())] = [0]
>= [0]
= [tt()]
[isQid(n__e())] = [0]
>= [0]
= [tt()]
[isQid(n__i())] = [0]
>= [0]
= [tt()]
[isQid(n__o())] = [0]
>= [0]
= [tt()]
[isQid(n__u())] = [0]
>= [0]
= [tt()]
[isNePal(V)] = [1] V + [0]
>= [1] V + [0]
= [isQid(activate(V))]
[isNePal(n____(I, __(P, I)))] = [2] I + [1] P + [4]
> [1] I + [1] P + [0]
= [and(isQid(activate(I)), n__isPal(activate(P)))]
[isPal(V)] = [1] V + [4]
> [1] V + [0]
= [isNePal(activate(V))]
[isPal(X)] = [1] X + [4]
> [1] X + [0]
= [n__isPal(X)]
[isPal(n__nil())] = [4]
> [0]
= [tt()]
[a()] = [2]
> [0]
= [n__a()]
[e()] = [5]
> [0]
= [n__e()]
[i()] = [5]
> [0]
= [n__i()]
[o()] = [5]
> [0]
= [n__o()]
[u()] = [5]
> [0]
= [n__u()]
Further, it can be verified that all rules not oriented are covered by the weightgap condition.
We are left with following problem, upon which TcT provides the
certificate YES(O(1),O(n^1)).
Strict Trs:
{ __(X1, X2) -> n____(X1, X2)
, __(__(X, Y), Z) -> __(X, __(Y, Z))
, nil() -> n__nil()
, and(tt(), X) -> activate(X)
, activate(X) -> X
, activate(n__isList(X)) -> isList(X)
, activate(n__isPal(X)) -> isPal(X)
, activate(n__a()) -> a()
, activate(n__e()) -> e()
, activate(n__i()) -> i()
, activate(n__o()) -> o()
, activate(n__u()) -> u()
, isNeList(X) -> n__isNeList(X)
, isNeList(n____(V1, V2)) ->
and(isList(activate(V1)), n__isNeList(activate(V2)))
, isQid(n__a()) -> tt()
, isQid(n__e()) -> tt()
, isQid(n__i()) -> tt()
, isQid(n__o()) -> tt()
, isQid(n__u()) -> tt()
, isNePal(V) -> isQid(activate(V)) }
Weak Trs:
{ __(X, nil()) -> X
, __(nil(), X) -> X
, activate(n__nil()) -> nil()
, activate(n____(X1, X2)) -> __(X1, X2)
, activate(n__isNeList(X)) -> isNeList(X)
, isList(V) -> isNeList(activate(V))
, isList(X) -> n__isList(X)
, isList(n__nil()) -> tt()
, isList(n____(V1, V2)) ->
and(isList(activate(V1)), n__isList(activate(V2)))
, isNeList(V) -> isQid(activate(V))
, isNeList(n____(V1, V2)) ->
and(isNeList(activate(V1)), n__isList(activate(V2)))
, isNePal(n____(I, __(P, I))) ->
and(isQid(activate(I)), n__isPal(activate(P)))
, isPal(V) -> isNePal(activate(V))
, isPal(X) -> n__isPal(X)
, isPal(n__nil()) -> tt()
, a() -> n__a()
, e() -> n__e()
, i() -> n__i()
, o() -> n__o()
, u() -> n__u() }
Obligation:
runtime complexity
Answer:
YES(O(1),O(n^1))
The weightgap principle applies (using the following nonconstant
growth matrix-interpretation)
The following argument positions are usable:
Uargs(__) = {2}, Uargs(and) = {1, 2}, Uargs(activate) = {1},
Uargs(isList) = {1}, Uargs(isNeList) = {1}, Uargs(n____) = {2},
Uargs(n__isList) = {1}, Uargs(isQid) = {1},
Uargs(n__isNeList) = {1}, Uargs(isNePal) = {1},
Uargs(n__isPal) = {1}, Uargs(isPal) = {1}
TcT has computed the following matrix interpretation satisfying
not(EDA) and not(IDA(1)).
[__](x1, x2) = [1] x1 + [1] x2 + [1]
[nil] = [0]
[and](x1, x2) = [1] x1 + [1] x2 + [0]
[tt] = [0]
[activate](x1) = [1] x1 + [0]
[isList](x1) = [1] x1 + [0]
[isNeList](x1) = [1] x1 + [0]
[n__nil] = [0]
[n____](x1, x2) = [1] x1 + [1] x2 + [1]
[n__isList](x1) = [1] x1 + [0]
[isQid](x1) = [1] x1 + [0]
[n__isNeList](x1) = [1] x1 + [4]
[isNePal](x1) = [1] x1 + [2]
[n__isPal](x1) = [1] x1 + [0]
[isPal](x1) = [1] x1 + [4]
[n__a] = [0]
[n__e] = [0]
[n__i] = [0]
[n__o] = [0]
[n__u] = [0]
[a] = [1]
[e] = [5]
[i] = [5]
[o] = [5]
[u] = [5]
The order satisfies the following ordering constraints:
[__(X1, X2)] = [1] X1 + [1] X2 + [1]
>= [1] X1 + [1] X2 + [1]
= [n____(X1, X2)]
[__(X, nil())] = [1] X + [1]
> [1] X + [0]
= [X]
[__(__(X, Y), Z)] = [1] X + [1] Y + [1] Z + [2]
>= [1] X + [1] Y + [1] Z + [2]
= [__(X, __(Y, Z))]
[__(nil(), X)] = [1] X + [1]
> [1] X + [0]
= [X]
[nil()] = [0]
>= [0]
= [n__nil()]
[and(tt(), X)] = [1] X + [0]
>= [1] X + [0]
= [activate(X)]
[activate(X)] = [1] X + [0]
>= [1] X + [0]
= [X]
[activate(n__nil())] = [0]
>= [0]
= [nil()]
[activate(n____(X1, X2))] = [1] X1 + [1] X2 + [1]
>= [1] X1 + [1] X2 + [1]
= [__(X1, X2)]
[activate(n__isList(X))] = [1] X + [0]
>= [1] X + [0]
= [isList(X)]
[activate(n__isNeList(X))] = [1] X + [4]
> [1] X + [0]
= [isNeList(X)]
[activate(n__isPal(X))] = [1] X + [0]
? [1] X + [4]
= [isPal(X)]
[activate(n__a())] = [0]
? [1]
= [a()]
[activate(n__e())] = [0]
? [5]
= [e()]
[activate(n__i())] = [0]
? [5]
= [i()]
[activate(n__o())] = [0]
? [5]
= [o()]
[activate(n__u())] = [0]
? [5]
= [u()]
[isList(V)] = [1] V + [0]
>= [1] V + [0]
= [isNeList(activate(V))]
[isList(X)] = [1] X + [0]
>= [1] X + [0]
= [n__isList(X)]
[isList(n__nil())] = [0]
>= [0]
= [tt()]
[isList(n____(V1, V2))] = [1] V1 + [1] V2 + [1]
> [1] V1 + [1] V2 + [0]
= [and(isList(activate(V1)), n__isList(activate(V2)))]
[isNeList(V)] = [1] V + [0]
>= [1] V + [0]
= [isQid(activate(V))]
[isNeList(X)] = [1] X + [0]
? [1] X + [4]
= [n__isNeList(X)]
[isNeList(n____(V1, V2))] = [1] V1 + [1] V2 + [1]
? [1] V1 + [1] V2 + [4]
= [and(isList(activate(V1)), n__isNeList(activate(V2)))]
[isNeList(n____(V1, V2))] = [1] V1 + [1] V2 + [1]
> [1] V1 + [1] V2 + [0]
= [and(isNeList(activate(V1)), n__isList(activate(V2)))]
[isQid(n__a())] = [0]
>= [0]
= [tt()]
[isQid(n__e())] = [0]
>= [0]
= [tt()]
[isQid(n__i())] = [0]
>= [0]
= [tt()]
[isQid(n__o())] = [0]
>= [0]
= [tt()]
[isQid(n__u())] = [0]
>= [0]
= [tt()]
[isNePal(V)] = [1] V + [2]
> [1] V + [0]
= [isQid(activate(V))]
[isNePal(n____(I, __(P, I)))] = [2] I + [1] P + [4]
> [1] I + [1] P + [0]
= [and(isQid(activate(I)), n__isPal(activate(P)))]
[isPal(V)] = [1] V + [4]
> [1] V + [2]
= [isNePal(activate(V))]
[isPal(X)] = [1] X + [4]
> [1] X + [0]
= [n__isPal(X)]
[isPal(n__nil())] = [4]
> [0]
= [tt()]
[a()] = [1]
> [0]
= [n__a()]
[e()] = [5]
> [0]
= [n__e()]
[i()] = [5]
> [0]
= [n__i()]
[o()] = [5]
> [0]
= [n__o()]
[u()] = [5]
> [0]
= [n__u()]
Further, it can be verified that all rules not oriented are covered by the weightgap condition.
We are left with following problem, upon which TcT provides the
certificate YES(O(1),O(n^1)).
Strict Trs:
{ __(X1, X2) -> n____(X1, X2)
, __(__(X, Y), Z) -> __(X, __(Y, Z))
, nil() -> n__nil()
, and(tt(), X) -> activate(X)
, activate(X) -> X
, activate(n__isList(X)) -> isList(X)
, activate(n__isPal(X)) -> isPal(X)
, activate(n__a()) -> a()
, activate(n__e()) -> e()
, activate(n__i()) -> i()
, activate(n__o()) -> o()
, activate(n__u()) -> u()
, isNeList(X) -> n__isNeList(X)
, isNeList(n____(V1, V2)) ->
and(isList(activate(V1)), n__isNeList(activate(V2)))
, isQid(n__a()) -> tt()
, isQid(n__e()) -> tt()
, isQid(n__i()) -> tt()
, isQid(n__o()) -> tt()
, isQid(n__u()) -> tt() }
Weak Trs:
{ __(X, nil()) -> X
, __(nil(), X) -> X
, activate(n__nil()) -> nil()
, activate(n____(X1, X2)) -> __(X1, X2)
, activate(n__isNeList(X)) -> isNeList(X)
, isList(V) -> isNeList(activate(V))
, isList(X) -> n__isList(X)
, isList(n__nil()) -> tt()
, isList(n____(V1, V2)) ->
and(isList(activate(V1)), n__isList(activate(V2)))
, isNeList(V) -> isQid(activate(V))
, isNeList(n____(V1, V2)) ->
and(isNeList(activate(V1)), n__isList(activate(V2)))
, isNePal(V) -> isQid(activate(V))
, isNePal(n____(I, __(P, I))) ->
and(isQid(activate(I)), n__isPal(activate(P)))
, isPal(V) -> isNePal(activate(V))
, isPal(X) -> n__isPal(X)
, isPal(n__nil()) -> tt()
, a() -> n__a()
, e() -> n__e()
, i() -> n__i()
, o() -> n__o()
, u() -> n__u() }
Obligation:
runtime complexity
Answer:
YES(O(1),O(n^1))
The weightgap principle applies (using the following nonconstant
growth matrix-interpretation)
The following argument positions are usable:
Uargs(__) = {2}, Uargs(and) = {1, 2}, Uargs(activate) = {1},
Uargs(isList) = {1}, Uargs(isNeList) = {1}, Uargs(n____) = {2},
Uargs(n__isList) = {1}, Uargs(isQid) = {1},
Uargs(n__isNeList) = {1}, Uargs(isNePal) = {1},
Uargs(n__isPal) = {1}, Uargs(isPal) = {1}
TcT has computed the following matrix interpretation satisfying
not(EDA) and not(IDA(1)).
[__](x1, x2) = [1] x1 + [1] x2 + [3]
[nil] = [1]
[and](x1, x2) = [1] x1 + [1] x2 + [0]
[tt] = [0]
[activate](x1) = [1] x1 + [0]
[isList](x1) = [1] x1 + [4]
[isNeList](x1) = [1] x1 + [4]
[n__nil] = [1]
[n____](x1, x2) = [1] x1 + [1] x2 + [5]
[n__isList](x1) = [1] x1 + [0]
[isQid](x1) = [1] x1 + [0]
[n__isNeList](x1) = [1] x1 + [4]
[isNePal](x1) = [1] x1 + [0]
[n__isPal](x1) = [1] x1 + [0]
[isPal](x1) = [1] x1 + [7]
[n__a] = [0]
[n__e] = [0]
[n__i] = [1]
[n__o] = [0]
[n__u] = [0]
[a] = [5]
[e] = [5]
[i] = [5]
[o] = [5]
[u] = [5]
The order satisfies the following ordering constraints:
[__(X1, X2)] = [1] X1 + [1] X2 + [3]
? [1] X1 + [1] X2 + [5]
= [n____(X1, X2)]
[__(X, nil())] = [1] X + [4]
> [1] X + [0]
= [X]
[__(__(X, Y), Z)] = [1] X + [1] Y + [1] Z + [6]
>= [1] X + [1] Y + [1] Z + [6]
= [__(X, __(Y, Z))]
[__(nil(), X)] = [1] X + [4]
> [1] X + [0]
= [X]
[nil()] = [1]
>= [1]
= [n__nil()]
[and(tt(), X)] = [1] X + [0]
>= [1] X + [0]
= [activate(X)]
[activate(X)] = [1] X + [0]
>= [1] X + [0]
= [X]
[activate(n__nil())] = [1]
>= [1]
= [nil()]
[activate(n____(X1, X2))] = [1] X1 + [1] X2 + [5]
> [1] X1 + [1] X2 + [3]
= [__(X1, X2)]
[activate(n__isList(X))] = [1] X + [0]
? [1] X + [4]
= [isList(X)]
[activate(n__isNeList(X))] = [1] X + [4]
>= [1] X + [4]
= [isNeList(X)]
[activate(n__isPal(X))] = [1] X + [0]
? [1] X + [7]
= [isPal(X)]
[activate(n__a())] = [0]
? [5]
= [a()]
[activate(n__e())] = [0]
? [5]
= [e()]
[activate(n__i())] = [1]
? [5]
= [i()]
[activate(n__o())] = [0]
? [5]
= [o()]
[activate(n__u())] = [0]
? [5]
= [u()]
[isList(V)] = [1] V + [4]
>= [1] V + [4]
= [isNeList(activate(V))]
[isList(X)] = [1] X + [4]
> [1] X + [0]
= [n__isList(X)]
[isList(n__nil())] = [5]
> [0]
= [tt()]
[isList(n____(V1, V2))] = [1] V1 + [1] V2 + [9]
> [1] V1 + [1] V2 + [4]
= [and(isList(activate(V1)), n__isList(activate(V2)))]
[isNeList(V)] = [1] V + [4]
> [1] V + [0]
= [isQid(activate(V))]
[isNeList(X)] = [1] X + [4]
>= [1] X + [4]
= [n__isNeList(X)]
[isNeList(n____(V1, V2))] = [1] V1 + [1] V2 + [9]
> [1] V1 + [1] V2 + [8]
= [and(isList(activate(V1)), n__isNeList(activate(V2)))]
[isNeList(n____(V1, V2))] = [1] V1 + [1] V2 + [9]
> [1] V1 + [1] V2 + [4]
= [and(isNeList(activate(V1)), n__isList(activate(V2)))]
[isQid(n__a())] = [0]
>= [0]
= [tt()]
[isQid(n__e())] = [0]
>= [0]
= [tt()]
[isQid(n__i())] = [1]
> [0]
= [tt()]
[isQid(n__o())] = [0]
>= [0]
= [tt()]
[isQid(n__u())] = [0]
>= [0]
= [tt()]
[isNePal(V)] = [1] V + [0]
>= [1] V + [0]
= [isQid(activate(V))]
[isNePal(n____(I, __(P, I)))] = [2] I + [1] P + [8]
> [1] I + [1] P + [0]
= [and(isQid(activate(I)), n__isPal(activate(P)))]
[isPal(V)] = [1] V + [7]
> [1] V + [0]
= [isNePal(activate(V))]
[isPal(X)] = [1] X + [7]
> [1] X + [0]
= [n__isPal(X)]
[isPal(n__nil())] = [8]
> [0]
= [tt()]
[a()] = [5]
> [0]
= [n__a()]
[e()] = [5]
> [0]
= [n__e()]
[i()] = [5]
> [1]
= [n__i()]
[o()] = [5]
> [0]
= [n__o()]
[u()] = [5]
> [0]
= [n__u()]
Further, it can be verified that all rules not oriented are covered by the weightgap condition.
We are left with following problem, upon which TcT provides the
certificate YES(O(1),O(n^1)).
Strict Trs:
{ __(X1, X2) -> n____(X1, X2)
, __(__(X, Y), Z) -> __(X, __(Y, Z))
, nil() -> n__nil()
, and(tt(), X) -> activate(X)
, activate(X) -> X
, activate(n__isList(X)) -> isList(X)
, activate(n__isPal(X)) -> isPal(X)
, activate(n__a()) -> a()
, activate(n__e()) -> e()
, activate(n__i()) -> i()
, activate(n__o()) -> o()
, activate(n__u()) -> u()
, isNeList(X) -> n__isNeList(X)
, isQid(n__a()) -> tt()
, isQid(n__e()) -> tt()
, isQid(n__o()) -> tt()
, isQid(n__u()) -> tt() }
Weak Trs:
{ __(X, nil()) -> X
, __(nil(), X) -> X
, activate(n__nil()) -> nil()
, activate(n____(X1, X2)) -> __(X1, X2)
, activate(n__isNeList(X)) -> isNeList(X)
, isList(V) -> isNeList(activate(V))
, isList(X) -> n__isList(X)
, isList(n__nil()) -> tt()
, isList(n____(V1, V2)) ->
and(isList(activate(V1)), n__isList(activate(V2)))
, isNeList(V) -> isQid(activate(V))
, isNeList(n____(V1, V2)) ->
and(isList(activate(V1)), n__isNeList(activate(V2)))
, isNeList(n____(V1, V2)) ->
and(isNeList(activate(V1)), n__isList(activate(V2)))
, isQid(n__i()) -> tt()
, isNePal(V) -> isQid(activate(V))
, isNePal(n____(I, __(P, I))) ->
and(isQid(activate(I)), n__isPal(activate(P)))
, isPal(V) -> isNePal(activate(V))
, isPal(X) -> n__isPal(X)
, isPal(n__nil()) -> tt()
, a() -> n__a()
, e() -> n__e()
, i() -> n__i()
, o() -> n__o()
, u() -> n__u() }
Obligation:
runtime complexity
Answer:
YES(O(1),O(n^1))
The weightgap principle applies (using the following nonconstant
growth matrix-interpretation)
The following argument positions are usable:
Uargs(__) = {2}, Uargs(and) = {1, 2}, Uargs(activate) = {1},
Uargs(isList) = {1}, Uargs(isNeList) = {1}, Uargs(n____) = {2},
Uargs(n__isList) = {1}, Uargs(isQid) = {1},
Uargs(n__isNeList) = {1}, Uargs(isNePal) = {1},
Uargs(n__isPal) = {1}, Uargs(isPal) = {1}
TcT has computed the following matrix interpretation satisfying
not(EDA) and not(IDA(1)).
[__](x1, x2) = [1] x1 + [1] x2 + [3]
[nil] = [1]
[and](x1, x2) = [1] x1 + [1] x2 + [0]
[tt] = [0]
[activate](x1) = [1] x1 + [0]
[isList](x1) = [1] x1 + [4]
[isNeList](x1) = [1] x1 + [4]
[n__nil] = [1]
[n____](x1, x2) = [1] x1 + [1] x2 + [5]
[n__isList](x1) = [1] x1 + [4]
[isQid](x1) = [1] x1 + [0]
[n__isNeList](x1) = [1] x1 + [4]
[isNePal](x1) = [1] x1 + [0]
[n__isPal](x1) = [1] x1 + [0]
[isPal](x1) = [1] x1 + [4]
[n__a] = [1]
[n__e] = [0]
[n__i] = [0]
[n__o] = [0]
[n__u] = [0]
[a] = [5]
[e] = [5]
[i] = [5]
[o] = [5]
[u] = [5]
The order satisfies the following ordering constraints:
[__(X1, X2)] = [1] X1 + [1] X2 + [3]
? [1] X1 + [1] X2 + [5]
= [n____(X1, X2)]
[__(X, nil())] = [1] X + [4]
> [1] X + [0]
= [X]
[__(__(X, Y), Z)] = [1] X + [1] Y + [1] Z + [6]
>= [1] X + [1] Y + [1] Z + [6]
= [__(X, __(Y, Z))]
[__(nil(), X)] = [1] X + [4]
> [1] X + [0]
= [X]
[nil()] = [1]
>= [1]
= [n__nil()]
[and(tt(), X)] = [1] X + [0]
>= [1] X + [0]
= [activate(X)]
[activate(X)] = [1] X + [0]
>= [1] X + [0]
= [X]
[activate(n__nil())] = [1]
>= [1]
= [nil()]
[activate(n____(X1, X2))] = [1] X1 + [1] X2 + [5]
> [1] X1 + [1] X2 + [3]
= [__(X1, X2)]
[activate(n__isList(X))] = [1] X + [4]
>= [1] X + [4]
= [isList(X)]
[activate(n__isNeList(X))] = [1] X + [4]
>= [1] X + [4]
= [isNeList(X)]
[activate(n__isPal(X))] = [1] X + [0]
? [1] X + [4]
= [isPal(X)]
[activate(n__a())] = [1]
? [5]
= [a()]
[activate(n__e())] = [0]
? [5]
= [e()]
[activate(n__i())] = [0]
? [5]
= [i()]
[activate(n__o())] = [0]
? [5]
= [o()]
[activate(n__u())] = [0]
? [5]
= [u()]
[isList(V)] = [1] V + [4]
>= [1] V + [4]
= [isNeList(activate(V))]
[isList(X)] = [1] X + [4]
>= [1] X + [4]
= [n__isList(X)]
[isList(n__nil())] = [5]
> [0]
= [tt()]
[isList(n____(V1, V2))] = [1] V1 + [1] V2 + [9]
> [1] V1 + [1] V2 + [8]
= [and(isList(activate(V1)), n__isList(activate(V2)))]
[isNeList(V)] = [1] V + [4]
> [1] V + [0]
= [isQid(activate(V))]
[isNeList(X)] = [1] X + [4]
>= [1] X + [4]
= [n__isNeList(X)]
[isNeList(n____(V1, V2))] = [1] V1 + [1] V2 + [9]
> [1] V1 + [1] V2 + [8]
= [and(isList(activate(V1)), n__isNeList(activate(V2)))]
[isNeList(n____(V1, V2))] = [1] V1 + [1] V2 + [9]
> [1] V1 + [1] V2 + [8]
= [and(isNeList(activate(V1)), n__isList(activate(V2)))]
[isQid(n__a())] = [1]
> [0]
= [tt()]
[isQid(n__e())] = [0]
>= [0]
= [tt()]
[isQid(n__i())] = [0]
>= [0]
= [tt()]
[isQid(n__o())] = [0]
>= [0]
= [tt()]
[isQid(n__u())] = [0]
>= [0]
= [tt()]
[isNePal(V)] = [1] V + [0]
>= [1] V + [0]
= [isQid(activate(V))]
[isNePal(n____(I, __(P, I)))] = [2] I + [1] P + [8]
> [1] I + [1] P + [0]
= [and(isQid(activate(I)), n__isPal(activate(P)))]
[isPal(V)] = [1] V + [4]
> [1] V + [0]
= [isNePal(activate(V))]
[isPal(X)] = [1] X + [4]
> [1] X + [0]
= [n__isPal(X)]
[isPal(n__nil())] = [5]
> [0]
= [tt()]
[a()] = [5]
> [1]
= [n__a()]
[e()] = [5]
> [0]
= [n__e()]
[i()] = [5]
> [0]
= [n__i()]
[o()] = [5]
> [0]
= [n__o()]
[u()] = [5]
> [0]
= [n__u()]
Further, it can be verified that all rules not oriented are covered by the weightgap condition.
We are left with following problem, upon which TcT provides the
certificate YES(O(1),O(n^1)).
Strict Trs:
{ __(X1, X2) -> n____(X1, X2)
, __(__(X, Y), Z) -> __(X, __(Y, Z))
, nil() -> n__nil()
, and(tt(), X) -> activate(X)
, activate(X) -> X
, activate(n__isList(X)) -> isList(X)
, activate(n__isPal(X)) -> isPal(X)
, activate(n__a()) -> a()
, activate(n__e()) -> e()
, activate(n__i()) -> i()
, activate(n__o()) -> o()
, activate(n__u()) -> u()
, isNeList(X) -> n__isNeList(X)
, isQid(n__e()) -> tt()
, isQid(n__o()) -> tt()
, isQid(n__u()) -> tt() }
Weak Trs:
{ __(X, nil()) -> X
, __(nil(), X) -> X
, activate(n__nil()) -> nil()
, activate(n____(X1, X2)) -> __(X1, X2)
, activate(n__isNeList(X)) -> isNeList(X)
, isList(V) -> isNeList(activate(V))
, isList(X) -> n__isList(X)
, isList(n__nil()) -> tt()
, isList(n____(V1, V2)) ->
and(isList(activate(V1)), n__isList(activate(V2)))
, isNeList(V) -> isQid(activate(V))
, isNeList(n____(V1, V2)) ->
and(isList(activate(V1)), n__isNeList(activate(V2)))
, isNeList(n____(V1, V2)) ->
and(isNeList(activate(V1)), n__isList(activate(V2)))
, isQid(n__a()) -> tt()
, isQid(n__i()) -> tt()
, isNePal(V) -> isQid(activate(V))
, isNePal(n____(I, __(P, I))) ->
and(isQid(activate(I)), n__isPal(activate(P)))
, isPal(V) -> isNePal(activate(V))
, isPal(X) -> n__isPal(X)
, isPal(n__nil()) -> tt()
, a() -> n__a()
, e() -> n__e()
, i() -> n__i()
, o() -> n__o()
, u() -> n__u() }
Obligation:
runtime complexity
Answer:
YES(O(1),O(n^1))
The weightgap principle applies (using the following nonconstant
growth matrix-interpretation)
The following argument positions are usable:
Uargs(__) = {2}, Uargs(and) = {1, 2}, Uargs(activate) = {1},
Uargs(isList) = {1}, Uargs(isNeList) = {1}, Uargs(n____) = {2},
Uargs(n__isList) = {1}, Uargs(isQid) = {1},
Uargs(n__isNeList) = {1}, Uargs(isNePal) = {1},
Uargs(n__isPal) = {1}, Uargs(isPal) = {1}
TcT has computed the following matrix interpretation satisfying
not(EDA) and not(IDA(1)).
[__](x1, x2) = [1] x1 + [1] x2 + [4]
[nil] = [0]
[and](x1, x2) = [1] x1 + [1] x2 + [0]
[tt] = [0]
[activate](x1) = [1] x1 + [0]
[isList](x1) = [1] x1 + [4]
[isNeList](x1) = [1] x1 + [4]
[n__nil] = [0]
[n____](x1, x2) = [1] x1 + [1] x2 + [4]
[n__isList](x1) = [1] x1 + [4]
[isQid](x1) = [1] x1 + [0]
[n__isNeList](x1) = [1] x1 + [4]
[isNePal](x1) = [1] x1 + [0]
[n__isPal](x1) = [1] x1 + [0]
[isPal](x1) = [1] x1 + [4]
[n__a] = [0]
[n__e] = [0]
[n__i] = [0]
[n__o] = [1]
[n__u] = [0]
[a] = [5]
[e] = [5]
[i] = [5]
[o] = [5]
[u] = [5]
The order satisfies the following ordering constraints:
[__(X1, X2)] = [1] X1 + [1] X2 + [4]
>= [1] X1 + [1] X2 + [4]
= [n____(X1, X2)]
[__(X, nil())] = [1] X + [4]
> [1] X + [0]
= [X]
[__(__(X, Y), Z)] = [1] X + [1] Y + [1] Z + [8]
>= [1] X + [1] Y + [1] Z + [8]
= [__(X, __(Y, Z))]
[__(nil(), X)] = [1] X + [4]
> [1] X + [0]
= [X]
[nil()] = [0]
>= [0]
= [n__nil()]
[and(tt(), X)] = [1] X + [0]
>= [1] X + [0]
= [activate(X)]
[activate(X)] = [1] X + [0]
>= [1] X + [0]
= [X]
[activate(n__nil())] = [0]
>= [0]
= [nil()]
[activate(n____(X1, X2))] = [1] X1 + [1] X2 + [4]
>= [1] X1 + [1] X2 + [4]
= [__(X1, X2)]
[activate(n__isList(X))] = [1] X + [4]
>= [1] X + [4]
= [isList(X)]
[activate(n__isNeList(X))] = [1] X + [4]
>= [1] X + [4]
= [isNeList(X)]
[activate(n__isPal(X))] = [1] X + [0]
? [1] X + [4]
= [isPal(X)]
[activate(n__a())] = [0]
? [5]
= [a()]
[activate(n__e())] = [0]
? [5]
= [e()]
[activate(n__i())] = [0]
? [5]
= [i()]
[activate(n__o())] = [1]
? [5]
= [o()]
[activate(n__u())] = [0]
? [5]
= [u()]
[isList(V)] = [1] V + [4]
>= [1] V + [4]
= [isNeList(activate(V))]
[isList(X)] = [1] X + [4]
>= [1] X + [4]
= [n__isList(X)]
[isList(n__nil())] = [4]
> [0]
= [tt()]
[isList(n____(V1, V2))] = [1] V1 + [1] V2 + [8]
>= [1] V1 + [1] V2 + [8]
= [and(isList(activate(V1)), n__isList(activate(V2)))]
[isNeList(V)] = [1] V + [4]
> [1] V + [0]
= [isQid(activate(V))]
[isNeList(X)] = [1] X + [4]
>= [1] X + [4]
= [n__isNeList(X)]
[isNeList(n____(V1, V2))] = [1] V1 + [1] V2 + [8]
>= [1] V1 + [1] V2 + [8]
= [and(isList(activate(V1)), n__isNeList(activate(V2)))]
[isNeList(n____(V1, V2))] = [1] V1 + [1] V2 + [8]
>= [1] V1 + [1] V2 + [8]
= [and(isNeList(activate(V1)), n__isList(activate(V2)))]
[isQid(n__a())] = [0]
>= [0]
= [tt()]
[isQid(n__e())] = [0]
>= [0]
= [tt()]
[isQid(n__i())] = [0]
>= [0]
= [tt()]
[isQid(n__o())] = [1]
> [0]
= [tt()]
[isQid(n__u())] = [0]
>= [0]
= [tt()]
[isNePal(V)] = [1] V + [0]
>= [1] V + [0]
= [isQid(activate(V))]
[isNePal(n____(I, __(P, I)))] = [2] I + [1] P + [8]
> [1] I + [1] P + [0]
= [and(isQid(activate(I)), n__isPal(activate(P)))]
[isPal(V)] = [1] V + [4]
> [1] V + [0]
= [isNePal(activate(V))]
[isPal(X)] = [1] X + [4]
> [1] X + [0]
= [n__isPal(X)]
[isPal(n__nil())] = [4]
> [0]
= [tt()]
[a()] = [5]
> [0]
= [n__a()]
[e()] = [5]
> [0]
= [n__e()]
[i()] = [5]
> [0]
= [n__i()]
[o()] = [5]
> [1]
= [n__o()]
[u()] = [5]
> [0]
= [n__u()]
Further, it can be verified that all rules not oriented are covered by the weightgap condition.
We are left with following problem, upon which TcT provides the
certificate YES(O(1),O(n^1)).
Strict Trs:
{ __(X1, X2) -> n____(X1, X2)
, __(__(X, Y), Z) -> __(X, __(Y, Z))
, nil() -> n__nil()
, and(tt(), X) -> activate(X)
, activate(X) -> X
, activate(n__isList(X)) -> isList(X)
, activate(n__isPal(X)) -> isPal(X)
, activate(n__a()) -> a()
, activate(n__e()) -> e()
, activate(n__i()) -> i()
, activate(n__o()) -> o()
, activate(n__u()) -> u()
, isNeList(X) -> n__isNeList(X)
, isQid(n__e()) -> tt()
, isQid(n__u()) -> tt() }
Weak Trs:
{ __(X, nil()) -> X
, __(nil(), X) -> X
, activate(n__nil()) -> nil()
, activate(n____(X1, X2)) -> __(X1, X2)
, activate(n__isNeList(X)) -> isNeList(X)
, isList(V) -> isNeList(activate(V))
, isList(X) -> n__isList(X)
, isList(n__nil()) -> tt()
, isList(n____(V1, V2)) ->
and(isList(activate(V1)), n__isList(activate(V2)))
, isNeList(V) -> isQid(activate(V))
, isNeList(n____(V1, V2)) ->
and(isList(activate(V1)), n__isNeList(activate(V2)))
, isNeList(n____(V1, V2)) ->
and(isNeList(activate(V1)), n__isList(activate(V2)))
, isQid(n__a()) -> tt()
, isQid(n__i()) -> tt()
, isQid(n__o()) -> tt()
, isNePal(V) -> isQid(activate(V))
, isNePal(n____(I, __(P, I))) ->
and(isQid(activate(I)), n__isPal(activate(P)))
, isPal(V) -> isNePal(activate(V))
, isPal(X) -> n__isPal(X)
, isPal(n__nil()) -> tt()
, a() -> n__a()
, e() -> n__e()
, i() -> n__i()
, o() -> n__o()
, u() -> n__u() }
Obligation:
runtime complexity
Answer:
YES(O(1),O(n^1))
The weightgap principle applies (using the following nonconstant
growth matrix-interpretation)
The following argument positions are usable:
Uargs(__) = {2}, Uargs(and) = {1, 2}, Uargs(activate) = {1},
Uargs(isList) = {1}, Uargs(isNeList) = {1}, Uargs(n____) = {2},
Uargs(n__isList) = {1}, Uargs(isQid) = {1},
Uargs(n__isNeList) = {1}, Uargs(isNePal) = {1},
Uargs(n__isPal) = {1}, Uargs(isPal) = {1}
TcT has computed the following matrix interpretation satisfying
not(EDA) and not(IDA(1)).
[__](x1, x2) = [1] x1 + [1] x2 + [3]
[nil] = [1]
[and](x1, x2) = [1] x1 + [1] x2 + [0]
[tt] = [0]
[activate](x1) = [1] x1 + [0]
[isList](x1) = [1] x1 + [4]
[isNeList](x1) = [1] x1 + [4]
[n__nil] = [1]
[n____](x1, x2) = [1] x1 + [1] x2 + [5]
[n__isList](x1) = [1] x1 + [4]
[isQid](x1) = [1] x1 + [0]
[n__isNeList](x1) = [1] x1 + [4]
[isNePal](x1) = [1] x1 + [0]
[n__isPal](x1) = [1] x1 + [0]
[isPal](x1) = [1] x1 + [4]
[n__a] = [0]
[n__e] = [1]
[n__i] = [0]
[n__o] = [0]
[n__u] = [0]
[a] = [5]
[e] = [5]
[i] = [5]
[o] = [5]
[u] = [5]
The order satisfies the following ordering constraints:
[__(X1, X2)] = [1] X1 + [1] X2 + [3]
? [1] X1 + [1] X2 + [5]
= [n____(X1, X2)]
[__(X, nil())] = [1] X + [4]
> [1] X + [0]
= [X]
[__(__(X, Y), Z)] = [1] X + [1] Y + [1] Z + [6]
>= [1] X + [1] Y + [1] Z + [6]
= [__(X, __(Y, Z))]
[__(nil(), X)] = [1] X + [4]
> [1] X + [0]
= [X]
[nil()] = [1]
>= [1]
= [n__nil()]
[and(tt(), X)] = [1] X + [0]
>= [1] X + [0]
= [activate(X)]
[activate(X)] = [1] X + [0]
>= [1] X + [0]
= [X]
[activate(n__nil())] = [1]
>= [1]
= [nil()]
[activate(n____(X1, X2))] = [1] X1 + [1] X2 + [5]
> [1] X1 + [1] X2 + [3]
= [__(X1, X2)]
[activate(n__isList(X))] = [1] X + [4]
>= [1] X + [4]
= [isList(X)]
[activate(n__isNeList(X))] = [1] X + [4]
>= [1] X + [4]
= [isNeList(X)]
[activate(n__isPal(X))] = [1] X + [0]
? [1] X + [4]
= [isPal(X)]
[activate(n__a())] = [0]
? [5]
= [a()]
[activate(n__e())] = [1]
? [5]
= [e()]
[activate(n__i())] = [0]
? [5]
= [i()]
[activate(n__o())] = [0]
? [5]
= [o()]
[activate(n__u())] = [0]
? [5]
= [u()]
[isList(V)] = [1] V + [4]
>= [1] V + [4]
= [isNeList(activate(V))]
[isList(X)] = [1] X + [4]
>= [1] X + [4]
= [n__isList(X)]
[isList(n__nil())] = [5]
> [0]
= [tt()]
[isList(n____(V1, V2))] = [1] V1 + [1] V2 + [9]
> [1] V1 + [1] V2 + [8]
= [and(isList(activate(V1)), n__isList(activate(V2)))]
[isNeList(V)] = [1] V + [4]
> [1] V + [0]
= [isQid(activate(V))]
[isNeList(X)] = [1] X + [4]
>= [1] X + [4]
= [n__isNeList(X)]
[isNeList(n____(V1, V2))] = [1] V1 + [1] V2 + [9]
> [1] V1 + [1] V2 + [8]
= [and(isList(activate(V1)), n__isNeList(activate(V2)))]
[isNeList(n____(V1, V2))] = [1] V1 + [1] V2 + [9]
> [1] V1 + [1] V2 + [8]
= [and(isNeList(activate(V1)), n__isList(activate(V2)))]
[isQid(n__a())] = [0]
>= [0]
= [tt()]
[isQid(n__e())] = [1]
> [0]
= [tt()]
[isQid(n__i())] = [0]
>= [0]
= [tt()]
[isQid(n__o())] = [0]
>= [0]
= [tt()]
[isQid(n__u())] = [0]
>= [0]
= [tt()]
[isNePal(V)] = [1] V + [0]
>= [1] V + [0]
= [isQid(activate(V))]
[isNePal(n____(I, __(P, I)))] = [2] I + [1] P + [8]
> [1] I + [1] P + [0]
= [and(isQid(activate(I)), n__isPal(activate(P)))]
[isPal(V)] = [1] V + [4]
> [1] V + [0]
= [isNePal(activate(V))]
[isPal(X)] = [1] X + [4]
> [1] X + [0]
= [n__isPal(X)]
[isPal(n__nil())] = [5]
> [0]
= [tt()]
[a()] = [5]
> [0]
= [n__a()]
[e()] = [5]
> [1]
= [n__e()]
[i()] = [5]
> [0]
= [n__i()]
[o()] = [5]
> [0]
= [n__o()]
[u()] = [5]
> [0]
= [n__u()]
Further, it can be verified that all rules not oriented are covered by the weightgap condition.
We are left with following problem, upon which TcT provides the
certificate YES(O(1),O(n^1)).
Strict Trs:
{ __(X1, X2) -> n____(X1, X2)
, __(__(X, Y), Z) -> __(X, __(Y, Z))
, nil() -> n__nil()
, and(tt(), X) -> activate(X)
, activate(X) -> X
, activate(n__isList(X)) -> isList(X)
, activate(n__isPal(X)) -> isPal(X)
, activate(n__a()) -> a()
, activate(n__e()) -> e()
, activate(n__i()) -> i()
, activate(n__o()) -> o()
, activate(n__u()) -> u()
, isNeList(X) -> n__isNeList(X)
, isQid(n__u()) -> tt() }
Weak Trs:
{ __(X, nil()) -> X
, __(nil(), X) -> X
, activate(n__nil()) -> nil()
, activate(n____(X1, X2)) -> __(X1, X2)
, activate(n__isNeList(X)) -> isNeList(X)
, isList(V) -> isNeList(activate(V))
, isList(X) -> n__isList(X)
, isList(n__nil()) -> tt()
, isList(n____(V1, V2)) ->
and(isList(activate(V1)), n__isList(activate(V2)))
, isNeList(V) -> isQid(activate(V))
, isNeList(n____(V1, V2)) ->
and(isList(activate(V1)), n__isNeList(activate(V2)))
, isNeList(n____(V1, V2)) ->
and(isNeList(activate(V1)), n__isList(activate(V2)))
, isQid(n__a()) -> tt()
, isQid(n__e()) -> tt()
, isQid(n__i()) -> tt()
, isQid(n__o()) -> tt()
, isNePal(V) -> isQid(activate(V))
, isNePal(n____(I, __(P, I))) ->
and(isQid(activate(I)), n__isPal(activate(P)))
, isPal(V) -> isNePal(activate(V))
, isPal(X) -> n__isPal(X)
, isPal(n__nil()) -> tt()
, a() -> n__a()
, e() -> n__e()
, i() -> n__i()
, o() -> n__o()
, u() -> n__u() }
Obligation:
runtime complexity
Answer:
YES(O(1),O(n^1))
The weightgap principle applies (using the following nonconstant
growth matrix-interpretation)
The following argument positions are usable:
Uargs(__) = {2}, Uargs(and) = {1, 2}, Uargs(activate) = {1},
Uargs(isList) = {1}, Uargs(isNeList) = {1}, Uargs(n____) = {2},
Uargs(n__isList) = {1}, Uargs(isQid) = {1},
Uargs(n__isNeList) = {1}, Uargs(isNePal) = {1},
Uargs(n__isPal) = {1}, Uargs(isPal) = {1}
TcT has computed the following matrix interpretation satisfying
not(EDA) and not(IDA(1)).
[__](x1, x2) = [1] x1 + [1] x2 + [1]
[nil] = [1]
[and](x1, x2) = [1] x1 + [1] x2 + [0]
[tt] = [0]
[activate](x1) = [1] x1 + [0]
[isList](x1) = [1] x1 + [0]
[isNeList](x1) = [1] x1 + [0]
[n__nil] = [1]
[n____](x1, x2) = [1] x1 + [1] x2 + [1]
[n__isList](x1) = [1] x1 + [0]
[isQid](x1) = [1] x1 + [0]
[n__isNeList](x1) = [1] x1 + [0]
[isNePal](x1) = [1] x1 + [2]
[n__isPal](x1) = [1] x1 + [0]
[isPal](x1) = [1] x1 + [4]
[n__a] = [0]
[n__e] = [0]
[n__i] = [0]
[n__o] = [0]
[n__u] = [1]
[a] = [5]
[e] = [5]
[i] = [5]
[o] = [5]
[u] = [5]
The order satisfies the following ordering constraints:
[__(X1, X2)] = [1] X1 + [1] X2 + [1]
>= [1] X1 + [1] X2 + [1]
= [n____(X1, X2)]
[__(X, nil())] = [1] X + [2]
> [1] X + [0]
= [X]
[__(__(X, Y), Z)] = [1] X + [1] Y + [1] Z + [2]
>= [1] X + [1] Y + [1] Z + [2]
= [__(X, __(Y, Z))]
[__(nil(), X)] = [1] X + [2]
> [1] X + [0]
= [X]
[nil()] = [1]
>= [1]
= [n__nil()]
[and(tt(), X)] = [1] X + [0]
>= [1] X + [0]
= [activate(X)]
[activate(X)] = [1] X + [0]
>= [1] X + [0]
= [X]
[activate(n__nil())] = [1]
>= [1]
= [nil()]
[activate(n____(X1, X2))] = [1] X1 + [1] X2 + [1]
>= [1] X1 + [1] X2 + [1]
= [__(X1, X2)]
[activate(n__isList(X))] = [1] X + [0]
>= [1] X + [0]
= [isList(X)]
[activate(n__isNeList(X))] = [1] X + [0]
>= [1] X + [0]
= [isNeList(X)]
[activate(n__isPal(X))] = [1] X + [0]
? [1] X + [4]
= [isPal(X)]
[activate(n__a())] = [0]
? [5]
= [a()]
[activate(n__e())] = [0]
? [5]
= [e()]
[activate(n__i())] = [0]
? [5]
= [i()]
[activate(n__o())] = [0]
? [5]
= [o()]
[activate(n__u())] = [1]
? [5]
= [u()]
[isList(V)] = [1] V + [0]
>= [1] V + [0]
= [isNeList(activate(V))]
[isList(X)] = [1] X + [0]
>= [1] X + [0]
= [n__isList(X)]
[isList(n__nil())] = [1]
> [0]
= [tt()]
[isList(n____(V1, V2))] = [1] V1 + [1] V2 + [1]
> [1] V1 + [1] V2 + [0]
= [and(isList(activate(V1)), n__isList(activate(V2)))]
[isNeList(V)] = [1] V + [0]
>= [1] V + [0]
= [isQid(activate(V))]
[isNeList(X)] = [1] X + [0]
>= [1] X + [0]
= [n__isNeList(X)]
[isNeList(n____(V1, V2))] = [1] V1 + [1] V2 + [1]
> [1] V1 + [1] V2 + [0]
= [and(isList(activate(V1)), n__isNeList(activate(V2)))]
[isNeList(n____(V1, V2))] = [1] V1 + [1] V2 + [1]
> [1] V1 + [1] V2 + [0]
= [and(isNeList(activate(V1)), n__isList(activate(V2)))]
[isQid(n__a())] = [0]
>= [0]
= [tt()]
[isQid(n__e())] = [0]
>= [0]
= [tt()]
[isQid(n__i())] = [0]
>= [0]
= [tt()]
[isQid(n__o())] = [0]
>= [0]
= [tt()]
[isQid(n__u())] = [1]
> [0]
= [tt()]
[isNePal(V)] = [1] V + [2]
> [1] V + [0]
= [isQid(activate(V))]
[isNePal(n____(I, __(P, I)))] = [2] I + [1] P + [4]
> [1] I + [1] P + [0]
= [and(isQid(activate(I)), n__isPal(activate(P)))]
[isPal(V)] = [1] V + [4]
> [1] V + [2]
= [isNePal(activate(V))]
[isPal(X)] = [1] X + [4]
> [1] X + [0]
= [n__isPal(X)]
[isPal(n__nil())] = [5]
> [0]
= [tt()]
[a()] = [5]
> [0]
= [n__a()]
[e()] = [5]
> [0]
= [n__e()]
[i()] = [5]
> [0]
= [n__i()]
[o()] = [5]
> [0]
= [n__o()]
[u()] = [5]
> [1]
= [n__u()]
Further, it can be verified that all rules not oriented are covered by the weightgap condition.
We are left with following problem, upon which TcT provides the
certificate YES(O(1),O(n^1)).
Strict Trs:
{ __(X1, X2) -> n____(X1, X2)
, __(__(X, Y), Z) -> __(X, __(Y, Z))
, nil() -> n__nil()
, and(tt(), X) -> activate(X)
, activate(X) -> X
, activate(n__isList(X)) -> isList(X)
, activate(n__isPal(X)) -> isPal(X)
, activate(n__a()) -> a()
, activate(n__e()) -> e()
, activate(n__i()) -> i()
, activate(n__o()) -> o()
, activate(n__u()) -> u()
, isNeList(X) -> n__isNeList(X) }
Weak Trs:
{ __(X, nil()) -> X
, __(nil(), X) -> X
, activate(n__nil()) -> nil()
, activate(n____(X1, X2)) -> __(X1, X2)
, activate(n__isNeList(X)) -> isNeList(X)
, isList(V) -> isNeList(activate(V))
, isList(X) -> n__isList(X)
, isList(n__nil()) -> tt()
, isList(n____(V1, V2)) ->
and(isList(activate(V1)), n__isList(activate(V2)))
, isNeList(V) -> isQid(activate(V))
, isNeList(n____(V1, V2)) ->
and(isList(activate(V1)), n__isNeList(activate(V2)))
, isNeList(n____(V1, V2)) ->
and(isNeList(activate(V1)), n__isList(activate(V2)))
, isQid(n__a()) -> tt()
, isQid(n__e()) -> tt()
, isQid(n__i()) -> tt()
, isQid(n__o()) -> tt()
, isQid(n__u()) -> tt()
, isNePal(V) -> isQid(activate(V))
, isNePal(n____(I, __(P, I))) ->
and(isQid(activate(I)), n__isPal(activate(P)))
, isPal(V) -> isNePal(activate(V))
, isPal(X) -> n__isPal(X)
, isPal(n__nil()) -> tt()
, a() -> n__a()
, e() -> n__e()
, i() -> n__i()
, o() -> n__o()
, u() -> n__u() }
Obligation:
runtime complexity
Answer:
YES(O(1),O(n^1))
The weightgap principle applies (using the following nonconstant
growth matrix-interpretation)
The following argument positions are usable:
Uargs(__) = {2}, Uargs(and) = {1, 2}, Uargs(activate) = {1},
Uargs(isList) = {1}, Uargs(isNeList) = {1}, Uargs(n____) = {2},
Uargs(n__isList) = {1}, Uargs(isQid) = {1},
Uargs(n__isNeList) = {1}, Uargs(isNePal) = {1},
Uargs(n__isPal) = {1}, Uargs(isPal) = {1}
TcT has computed the following matrix interpretation satisfying
not(EDA) and not(IDA(1)).
[__](x1, x2) = [1] x1 + [1] x2 + [0]
[nil] = [0]
[and](x1, x2) = [1] x1 + [1] x2 + [1]
[tt] = [0]
[activate](x1) = [1] x1 + [0]
[isList](x1) = [1] x1 + [0]
[isNeList](x1) = [1] x1 + [0]
[n__nil] = [0]
[n____](x1, x2) = [1] x1 + [1] x2 + [1]
[n__isList](x1) = [1] x1 + [0]
[isQid](x1) = [1] x1 + [0]
[n__isNeList](x1) = [1] x1 + [0]
[isNePal](x1) = [1] x1 + [0]
[n__isPal](x1) = [1] x1 + [0]
[isPal](x1) = [1] x1 + [4]
[n__a] = [0]
[n__e] = [0]
[n__i] = [0]
[n__o] = [0]
[n__u] = [0]
[a] = [1]
[e] = [5]
[i] = [5]
[o] = [5]
[u] = [5]
The order satisfies the following ordering constraints:
[__(X1, X2)] = [1] X1 + [1] X2 + [0]
? [1] X1 + [1] X2 + [1]
= [n____(X1, X2)]
[__(X, nil())] = [1] X + [0]
>= [1] X + [0]
= [X]
[__(__(X, Y), Z)] = [1] X + [1] Y + [1] Z + [0]
>= [1] X + [1] Y + [1] Z + [0]
= [__(X, __(Y, Z))]
[__(nil(), X)] = [1] X + [0]
>= [1] X + [0]
= [X]
[nil()] = [0]
>= [0]
= [n__nil()]
[and(tt(), X)] = [1] X + [1]
> [1] X + [0]
= [activate(X)]
[activate(X)] = [1] X + [0]
>= [1] X + [0]
= [X]
[activate(n__nil())] = [0]
>= [0]
= [nil()]
[activate(n____(X1, X2))] = [1] X1 + [1] X2 + [1]
> [1] X1 + [1] X2 + [0]
= [__(X1, X2)]
[activate(n__isList(X))] = [1] X + [0]
>= [1] X + [0]
= [isList(X)]
[activate(n__isNeList(X))] = [1] X + [0]
>= [1] X + [0]
= [isNeList(X)]
[activate(n__isPal(X))] = [1] X + [0]
? [1] X + [4]
= [isPal(X)]
[activate(n__a())] = [0]
? [1]
= [a()]
[activate(n__e())] = [0]
? [5]
= [e()]
[activate(n__i())] = [0]
? [5]
= [i()]
[activate(n__o())] = [0]
? [5]
= [o()]
[activate(n__u())] = [0]
? [5]
= [u()]
[isList(V)] = [1] V + [0]
>= [1] V + [0]
= [isNeList(activate(V))]
[isList(X)] = [1] X + [0]
>= [1] X + [0]
= [n__isList(X)]
[isList(n__nil())] = [0]
>= [0]
= [tt()]
[isList(n____(V1, V2))] = [1] V1 + [1] V2 + [1]
>= [1] V1 + [1] V2 + [1]
= [and(isList(activate(V1)), n__isList(activate(V2)))]
[isNeList(V)] = [1] V + [0]
>= [1] V + [0]
= [isQid(activate(V))]
[isNeList(X)] = [1] X + [0]
>= [1] X + [0]
= [n__isNeList(X)]
[isNeList(n____(V1, V2))] = [1] V1 + [1] V2 + [1]
>= [1] V1 + [1] V2 + [1]
= [and(isList(activate(V1)), n__isNeList(activate(V2)))]
[isNeList(n____(V1, V2))] = [1] V1 + [1] V2 + [1]
>= [1] V1 + [1] V2 + [1]
= [and(isNeList(activate(V1)), n__isList(activate(V2)))]
[isQid(n__a())] = [0]
>= [0]
= [tt()]
[isQid(n__e())] = [0]
>= [0]
= [tt()]
[isQid(n__i())] = [0]
>= [0]
= [tt()]
[isQid(n__o())] = [0]
>= [0]
= [tt()]
[isQid(n__u())] = [0]
>= [0]
= [tt()]
[isNePal(V)] = [1] V + [0]
>= [1] V + [0]
= [isQid(activate(V))]
[isNePal(n____(I, __(P, I)))] = [2] I + [1] P + [1]
>= [1] I + [1] P + [1]
= [and(isQid(activate(I)), n__isPal(activate(P)))]
[isPal(V)] = [1] V + [4]
> [1] V + [0]
= [isNePal(activate(V))]
[isPal(X)] = [1] X + [4]
> [1] X + [0]
= [n__isPal(X)]
[isPal(n__nil())] = [4]
> [0]
= [tt()]
[a()] = [1]
> [0]
= [n__a()]
[e()] = [5]
> [0]
= [n__e()]
[i()] = [5]
> [0]
= [n__i()]
[o()] = [5]
> [0]
= [n__o()]
[u()] = [5]
> [0]
= [n__u()]
Further, it can be verified that all rules not oriented are covered by the weightgap condition.
We are left with following problem, upon which TcT provides the
certificate YES(O(1),O(n^1)).
Strict Trs:
{ __(X1, X2) -> n____(X1, X2)
, __(__(X, Y), Z) -> __(X, __(Y, Z))
, nil() -> n__nil()
, activate(X) -> X
, activate(n__isList(X)) -> isList(X)
, activate(n__isPal(X)) -> isPal(X)
, activate(n__a()) -> a()
, activate(n__e()) -> e()
, activate(n__i()) -> i()
, activate(n__o()) -> o()
, activate(n__u()) -> u()
, isNeList(X) -> n__isNeList(X) }
Weak Trs:
{ __(X, nil()) -> X
, __(nil(), X) -> X
, and(tt(), X) -> activate(X)
, activate(n__nil()) -> nil()
, activate(n____(X1, X2)) -> __(X1, X2)
, activate(n__isNeList(X)) -> isNeList(X)
, isList(V) -> isNeList(activate(V))
, isList(X) -> n__isList(X)
, isList(n__nil()) -> tt()
, isList(n____(V1, V2)) ->
and(isList(activate(V1)), n__isList(activate(V2)))
, isNeList(V) -> isQid(activate(V))
, isNeList(n____(V1, V2)) ->
and(isList(activate(V1)), n__isNeList(activate(V2)))
, isNeList(n____(V1, V2)) ->
and(isNeList(activate(V1)), n__isList(activate(V2)))
, isQid(n__a()) -> tt()
, isQid(n__e()) -> tt()
, isQid(n__i()) -> tt()
, isQid(n__o()) -> tt()
, isQid(n__u()) -> tt()
, isNePal(V) -> isQid(activate(V))
, isNePal(n____(I, __(P, I))) ->
and(isQid(activate(I)), n__isPal(activate(P)))
, isPal(V) -> isNePal(activate(V))
, isPal(X) -> n__isPal(X)
, isPal(n__nil()) -> tt()
, a() -> n__a()
, e() -> n__e()
, i() -> n__i()
, o() -> n__o()
, u() -> n__u() }
Obligation:
runtime complexity
Answer:
YES(O(1),O(n^1))
The weightgap principle applies (using the following nonconstant
growth matrix-interpretation)
The following argument positions are usable:
Uargs(__) = {2}, Uargs(and) = {1, 2}, Uargs(activate) = {1},
Uargs(isList) = {1}, Uargs(isNeList) = {1}, Uargs(n____) = {2},
Uargs(n__isList) = {1}, Uargs(isQid) = {1},
Uargs(n__isNeList) = {1}, Uargs(isNePal) = {1},
Uargs(n__isPal) = {1}, Uargs(isPal) = {1}
TcT has computed the following matrix interpretation satisfying
not(EDA) and not(IDA(1)).
[__](x1, x2) = [1] x1 + [1] x2 + [1]
[nil] = [0]
[and](x1, x2) = [1] x1 + [1] x2 + [0]
[tt] = [1]
[activate](x1) = [1] x1 + [1]
[isList](x1) = [1] x1 + [4]
[isNeList](x1) = [1] x1 + [3]
[n__nil] = [0]
[n____](x1, x2) = [1] x1 + [1] x2 + [7]
[n__isList](x1) = [1] x1 + [4]
[isQid](x1) = [1] x1 + [1]
[n__isNeList](x1) = [1] x1 + [3]
[isNePal](x1) = [1] x1 + [2]
[n__isPal](x1) = [1] x1 + [3]
[isPal](x1) = [1] x1 + [3]
[n__a] = [0]
[n__e] = [0]
[n__i] = [0]
[n__o] = [0]
[n__u] = [0]
[a] = [0]
[e] = [0]
[i] = [0]
[o] = [0]
[u] = [0]
The order satisfies the following ordering constraints:
[__(X1, X2)] = [1] X1 + [1] X2 + [1]
? [1] X1 + [1] X2 + [7]
= [n____(X1, X2)]
[__(X, nil())] = [1] X + [1]
> [1] X + [0]
= [X]
[__(__(X, Y), Z)] = [1] X + [1] Y + [1] Z + [2]
>= [1] X + [1] Y + [1] Z + [2]
= [__(X, __(Y, Z))]
[__(nil(), X)] = [1] X + [1]
> [1] X + [0]
= [X]
[nil()] = [0]
>= [0]
= [n__nil()]
[and(tt(), X)] = [1] X + [1]
>= [1] X + [1]
= [activate(X)]
[activate(X)] = [1] X + [1]
> [1] X + [0]
= [X]
[activate(n__nil())] = [1]
> [0]
= [nil()]
[activate(n____(X1, X2))] = [1] X1 + [1] X2 + [8]
> [1] X1 + [1] X2 + [1]
= [__(X1, X2)]
[activate(n__isList(X))] = [1] X + [5]
> [1] X + [4]
= [isList(X)]
[activate(n__isNeList(X))] = [1] X + [4]
> [1] X + [3]
= [isNeList(X)]
[activate(n__isPal(X))] = [1] X + [4]
> [1] X + [3]
= [isPal(X)]
[activate(n__a())] = [1]
> [0]
= [a()]
[activate(n__e())] = [1]
> [0]
= [e()]
[activate(n__i())] = [1]
> [0]
= [i()]
[activate(n__o())] = [1]
> [0]
= [o()]
[activate(n__u())] = [1]
> [0]
= [u()]
[isList(V)] = [1] V + [4]
>= [1] V + [4]
= [isNeList(activate(V))]
[isList(X)] = [1] X + [4]
>= [1] X + [4]
= [n__isList(X)]
[isList(n__nil())] = [4]
> [1]
= [tt()]
[isList(n____(V1, V2))] = [1] V1 + [1] V2 + [11]
> [1] V1 + [1] V2 + [10]
= [and(isList(activate(V1)), n__isList(activate(V2)))]
[isNeList(V)] = [1] V + [3]
> [1] V + [2]
= [isQid(activate(V))]
[isNeList(X)] = [1] X + [3]
>= [1] X + [3]
= [n__isNeList(X)]
[isNeList(n____(V1, V2))] = [1] V1 + [1] V2 + [10]
> [1] V1 + [1] V2 + [9]
= [and(isList(activate(V1)), n__isNeList(activate(V2)))]
[isNeList(n____(V1, V2))] = [1] V1 + [1] V2 + [10]
> [1] V1 + [1] V2 + [9]
= [and(isNeList(activate(V1)), n__isList(activate(V2)))]
[isQid(n__a())] = [1]
>= [1]
= [tt()]
[isQid(n__e())] = [1]
>= [1]
= [tt()]
[isQid(n__i())] = [1]
>= [1]
= [tt()]
[isQid(n__o())] = [1]
>= [1]
= [tt()]
[isQid(n__u())] = [1]
>= [1]
= [tt()]
[isNePal(V)] = [1] V + [2]
>= [1] V + [2]
= [isQid(activate(V))]
[isNePal(n____(I, __(P, I)))] = [2] I + [1] P + [10]
> [1] I + [1] P + [6]
= [and(isQid(activate(I)), n__isPal(activate(P)))]
[isPal(V)] = [1] V + [3]
>= [1] V + [3]
= [isNePal(activate(V))]
[isPal(X)] = [1] X + [3]
>= [1] X + [3]
= [n__isPal(X)]
[isPal(n__nil())] = [3]
> [1]
= [tt()]
[a()] = [0]
>= [0]
= [n__a()]
[e()] = [0]
>= [0]
= [n__e()]
[i()] = [0]
>= [0]
= [n__i()]
[o()] = [0]
>= [0]
= [n__o()]
[u()] = [0]
>= [0]
= [n__u()]
Further, it can be verified that all rules not oriented are covered by the weightgap condition.
We are left with following problem, upon which TcT provides the
certificate YES(O(1),O(n^1)).
Strict Trs:
{ __(X1, X2) -> n____(X1, X2)
, __(__(X, Y), Z) -> __(X, __(Y, Z))
, nil() -> n__nil()
, isNeList(X) -> n__isNeList(X) }
Weak Trs:
{ __(X, nil()) -> X
, __(nil(), X) -> X
, and(tt(), X) -> activate(X)
, activate(X) -> X
, activate(n__nil()) -> nil()
, activate(n____(X1, X2)) -> __(X1, X2)
, activate(n__isList(X)) -> isList(X)
, activate(n__isNeList(X)) -> isNeList(X)
, activate(n__isPal(X)) -> isPal(X)
, activate(n__a()) -> a()
, activate(n__e()) -> e()
, activate(n__i()) -> i()
, activate(n__o()) -> o()
, activate(n__u()) -> u()
, isList(V) -> isNeList(activate(V))
, isList(X) -> n__isList(X)
, isList(n__nil()) -> tt()
, isList(n____(V1, V2)) ->
and(isList(activate(V1)), n__isList(activate(V2)))
, isNeList(V) -> isQid(activate(V))
, isNeList(n____(V1, V2)) ->
and(isList(activate(V1)), n__isNeList(activate(V2)))
, isNeList(n____(V1, V2)) ->
and(isNeList(activate(V1)), n__isList(activate(V2)))
, isQid(n__a()) -> tt()
, isQid(n__e()) -> tt()
, isQid(n__i()) -> tt()
, isQid(n__o()) -> tt()
, isQid(n__u()) -> tt()
, isNePal(V) -> isQid(activate(V))
, isNePal(n____(I, __(P, I))) ->
and(isQid(activate(I)), n__isPal(activate(P)))
, isPal(V) -> isNePal(activate(V))
, isPal(X) -> n__isPal(X)
, isPal(n__nil()) -> tt()
, a() -> n__a()
, e() -> n__e()
, i() -> n__i()
, o() -> n__o()
, u() -> n__u() }
Obligation:
runtime complexity
Answer:
YES(O(1),O(n^1))
The weightgap principle applies (using the following nonconstant
growth matrix-interpretation)
The following argument positions are usable:
Uargs(__) = {2}, Uargs(and) = {1, 2}, Uargs(activate) = {1},
Uargs(isList) = {1}, Uargs(isNeList) = {1}, Uargs(n____) = {2},
Uargs(n__isList) = {1}, Uargs(isQid) = {1},
Uargs(n__isNeList) = {1}, Uargs(isNePal) = {1},
Uargs(n__isPal) = {1}, Uargs(isPal) = {1}
TcT has computed the following matrix interpretation satisfying
not(EDA) and not(IDA(1)).
[__](x1, x2) = [1] x1 + [1] x2 + [3]
[nil] = [1]
[and](x1, x2) = [1] x1 + [1] x2 + [0]
[tt] = [1]
[activate](x1) = [1] x1 + [1]
[isList](x1) = [1] x1 + [5]
[isNeList](x1) = [1] x1 + [3]
[n__nil] = [0]
[n____](x1, x2) = [1] x1 + [1] x2 + [7]
[n__isList](x1) = [1] x1 + [4]
[isQid](x1) = [1] x1 + [0]
[n__isNeList](x1) = [1] x1 + [3]
[isNePal](x1) = [1] x1 + [4]
[n__isPal](x1) = [1] x1 + [4]
[isPal](x1) = [1] x1 + [5]
[n__a] = [1]
[n__e] = [1]
[n__i] = [1]
[n__o] = [2]
[n__u] = [2]
[a] = [1]
[e] = [2]
[i] = [1]
[o] = [2]
[u] = [2]
The order satisfies the following ordering constraints:
[__(X1, X2)] = [1] X1 + [1] X2 + [3]
? [1] X1 + [1] X2 + [7]
= [n____(X1, X2)]
[__(X, nil())] = [1] X + [4]
> [1] X + [0]
= [X]
[__(__(X, Y), Z)] = [1] X + [1] Y + [1] Z + [6]
>= [1] X + [1] Y + [1] Z + [6]
= [__(X, __(Y, Z))]
[__(nil(), X)] = [1] X + [4]
> [1] X + [0]
= [X]
[nil()] = [1]
> [0]
= [n__nil()]
[and(tt(), X)] = [1] X + [1]
>= [1] X + [1]
= [activate(X)]
[activate(X)] = [1] X + [1]
> [1] X + [0]
= [X]
[activate(n__nil())] = [1]
>= [1]
= [nil()]
[activate(n____(X1, X2))] = [1] X1 + [1] X2 + [8]
> [1] X1 + [1] X2 + [3]
= [__(X1, X2)]
[activate(n__isList(X))] = [1] X + [5]
>= [1] X + [5]
= [isList(X)]
[activate(n__isNeList(X))] = [1] X + [4]
> [1] X + [3]
= [isNeList(X)]
[activate(n__isPal(X))] = [1] X + [5]
>= [1] X + [5]
= [isPal(X)]
[activate(n__a())] = [2]
> [1]
= [a()]
[activate(n__e())] = [2]
>= [2]
= [e()]
[activate(n__i())] = [2]
> [1]
= [i()]
[activate(n__o())] = [3]
> [2]
= [o()]
[activate(n__u())] = [3]
> [2]
= [u()]
[isList(V)] = [1] V + [5]
> [1] V + [4]
= [isNeList(activate(V))]
[isList(X)] = [1] X + [5]
> [1] X + [4]
= [n__isList(X)]
[isList(n__nil())] = [5]
> [1]
= [tt()]
[isList(n____(V1, V2))] = [1] V1 + [1] V2 + [12]
> [1] V1 + [1] V2 + [11]
= [and(isList(activate(V1)), n__isList(activate(V2)))]
[isNeList(V)] = [1] V + [3]
> [1] V + [1]
= [isQid(activate(V))]
[isNeList(X)] = [1] X + [3]
>= [1] X + [3]
= [n__isNeList(X)]
[isNeList(n____(V1, V2))] = [1] V1 + [1] V2 + [10]
>= [1] V1 + [1] V2 + [10]
= [and(isList(activate(V1)), n__isNeList(activate(V2)))]
[isNeList(n____(V1, V2))] = [1] V1 + [1] V2 + [10]
> [1] V1 + [1] V2 + [9]
= [and(isNeList(activate(V1)), n__isList(activate(V2)))]
[isQid(n__a())] = [1]
>= [1]
= [tt()]
[isQid(n__e())] = [1]
>= [1]
= [tt()]
[isQid(n__i())] = [1]
>= [1]
= [tt()]
[isQid(n__o())] = [2]
> [1]
= [tt()]
[isQid(n__u())] = [2]
> [1]
= [tt()]
[isNePal(V)] = [1] V + [4]
> [1] V + [1]
= [isQid(activate(V))]
[isNePal(n____(I, __(P, I)))] = [2] I + [1] P + [14]
> [1] I + [1] P + [6]
= [and(isQid(activate(I)), n__isPal(activate(P)))]
[isPal(V)] = [1] V + [5]
>= [1] V + [5]
= [isNePal(activate(V))]
[isPal(X)] = [1] X + [5]
> [1] X + [4]
= [n__isPal(X)]
[isPal(n__nil())] = [5]
> [1]
= [tt()]
[a()] = [1]
>= [1]
= [n__a()]
[e()] = [2]
> [1]
= [n__e()]
[i()] = [1]
>= [1]
= [n__i()]
[o()] = [2]
>= [2]
= [n__o()]
[u()] = [2]
>= [2]
= [n__u()]
Further, it can be verified that all rules not oriented are covered by the weightgap condition.
We are left with following problem, upon which TcT provides the
certificate YES(O(1),O(n^1)).
Strict Trs:
{ __(X1, X2) -> n____(X1, X2)
, __(__(X, Y), Z) -> __(X, __(Y, Z))
, isNeList(X) -> n__isNeList(X) }
Weak Trs:
{ __(X, nil()) -> X
, __(nil(), X) -> X
, nil() -> n__nil()
, and(tt(), X) -> activate(X)
, activate(X) -> X
, activate(n__nil()) -> nil()
, activate(n____(X1, X2)) -> __(X1, X2)
, activate(n__isList(X)) -> isList(X)
, activate(n__isNeList(X)) -> isNeList(X)
, activate(n__isPal(X)) -> isPal(X)
, activate(n__a()) -> a()
, activate(n__e()) -> e()
, activate(n__i()) -> i()
, activate(n__o()) -> o()
, activate(n__u()) -> u()
, isList(V) -> isNeList(activate(V))
, isList(X) -> n__isList(X)
, isList(n__nil()) -> tt()
, isList(n____(V1, V2)) ->
and(isList(activate(V1)), n__isList(activate(V2)))
, isNeList(V) -> isQid(activate(V))
, isNeList(n____(V1, V2)) ->
and(isList(activate(V1)), n__isNeList(activate(V2)))
, isNeList(n____(V1, V2)) ->
and(isNeList(activate(V1)), n__isList(activate(V2)))
, isQid(n__a()) -> tt()
, isQid(n__e()) -> tt()
, isQid(n__i()) -> tt()
, isQid(n__o()) -> tt()
, isQid(n__u()) -> tt()
, isNePal(V) -> isQid(activate(V))
, isNePal(n____(I, __(P, I))) ->
and(isQid(activate(I)), n__isPal(activate(P)))
, isPal(V) -> isNePal(activate(V))
, isPal(X) -> n__isPal(X)
, isPal(n__nil()) -> tt()
, a() -> n__a()
, e() -> n__e()
, i() -> n__i()
, o() -> n__o()
, u() -> n__u() }
Obligation:
runtime complexity
Answer:
YES(O(1),O(n^1))
The weightgap principle applies (using the following nonconstant
growth matrix-interpretation)
The following argument positions are usable:
Uargs(__) = {2}, Uargs(and) = {1, 2}, Uargs(activate) = {1},
Uargs(isList) = {1}, Uargs(isNeList) = {1}, Uargs(n____) = {2},
Uargs(n__isList) = {1}, Uargs(isQid) = {1},
Uargs(n__isNeList) = {1}, Uargs(isNePal) = {1},
Uargs(n__isPal) = {1}, Uargs(isPal) = {1}
TcT has computed the following matrix interpretation satisfying
not(EDA) and not(IDA(1)).
[__](x1, x2) = [1] x1 + [1] x2 + [5]
[nil] = [0]
[and](x1, x2) = [1] x1 + [1] x2 + [0]
[tt] = [1]
[activate](x1) = [1] x1 + [1]
[isList](x1) = [1] x1 + [5]
[isNeList](x1) = [1] x1 + [4]
[n__nil] = [0]
[n____](x1, x2) = [1] x1 + [1] x2 + [7]
[n__isList](x1) = [1] x1 + [4]
[isQid](x1) = [1] x1 + [0]
[n__isNeList](x1) = [1] x1 + [3]
[isNePal](x1) = [1] x1 + [2]
[n__isPal](x1) = [1] x1 + [4]
[isPal](x1) = [1] x1 + [4]
[n__a] = [1]
[n__e] = [1]
[n__i] = [1]
[n__o] = [1]
[n__u] = [1]
[a] = [1]
[e] = [2]
[i] = [1]
[o] = [2]
[u] = [2]
The order satisfies the following ordering constraints:
[__(X1, X2)] = [1] X1 + [1] X2 + [5]
? [1] X1 + [1] X2 + [7]
= [n____(X1, X2)]
[__(X, nil())] = [1] X + [5]
> [1] X + [0]
= [X]
[__(__(X, Y), Z)] = [1] X + [1] Y + [1] Z + [10]
>= [1] X + [1] Y + [1] Z + [10]
= [__(X, __(Y, Z))]
[__(nil(), X)] = [1] X + [5]
> [1] X + [0]
= [X]
[nil()] = [0]
>= [0]
= [n__nil()]
[and(tt(), X)] = [1] X + [1]
>= [1] X + [1]
= [activate(X)]
[activate(X)] = [1] X + [1]
> [1] X + [0]
= [X]
[activate(n__nil())] = [1]
> [0]
= [nil()]
[activate(n____(X1, X2))] = [1] X1 + [1] X2 + [8]
> [1] X1 + [1] X2 + [5]
= [__(X1, X2)]
[activate(n__isList(X))] = [1] X + [5]
>= [1] X + [5]
= [isList(X)]
[activate(n__isNeList(X))] = [1] X + [4]
>= [1] X + [4]
= [isNeList(X)]
[activate(n__isPal(X))] = [1] X + [5]
> [1] X + [4]
= [isPal(X)]
[activate(n__a())] = [2]
> [1]
= [a()]
[activate(n__e())] = [2]
>= [2]
= [e()]
[activate(n__i())] = [2]
> [1]
= [i()]
[activate(n__o())] = [2]
>= [2]
= [o()]
[activate(n__u())] = [2]
>= [2]
= [u()]
[isList(V)] = [1] V + [5]
>= [1] V + [5]
= [isNeList(activate(V))]
[isList(X)] = [1] X + [5]
> [1] X + [4]
= [n__isList(X)]
[isList(n__nil())] = [5]
> [1]
= [tt()]
[isList(n____(V1, V2))] = [1] V1 + [1] V2 + [12]
> [1] V1 + [1] V2 + [11]
= [and(isList(activate(V1)), n__isList(activate(V2)))]
[isNeList(V)] = [1] V + [4]
> [1] V + [1]
= [isQid(activate(V))]
[isNeList(X)] = [1] X + [4]
> [1] X + [3]
= [n__isNeList(X)]
[isNeList(n____(V1, V2))] = [1] V1 + [1] V2 + [11]
> [1] V1 + [1] V2 + [10]
= [and(isList(activate(V1)), n__isNeList(activate(V2)))]
[isNeList(n____(V1, V2))] = [1] V1 + [1] V2 + [11]
> [1] V1 + [1] V2 + [10]
= [and(isNeList(activate(V1)), n__isList(activate(V2)))]
[isQid(n__a())] = [1]
>= [1]
= [tt()]
[isQid(n__e())] = [1]
>= [1]
= [tt()]
[isQid(n__i())] = [1]
>= [1]
= [tt()]
[isQid(n__o())] = [1]
>= [1]
= [tt()]
[isQid(n__u())] = [1]
>= [1]
= [tt()]
[isNePal(V)] = [1] V + [2]
> [1] V + [1]
= [isQid(activate(V))]
[isNePal(n____(I, __(P, I)))] = [2] I + [1] P + [14]
> [1] I + [1] P + [6]
= [and(isQid(activate(I)), n__isPal(activate(P)))]
[isPal(V)] = [1] V + [4]
> [1] V + [3]
= [isNePal(activate(V))]
[isPal(X)] = [1] X + [4]
>= [1] X + [4]
= [n__isPal(X)]
[isPal(n__nil())] = [4]
> [1]
= [tt()]
[a()] = [1]
>= [1]
= [n__a()]
[e()] = [2]
> [1]
= [n__e()]
[i()] = [1]
>= [1]
= [n__i()]
[o()] = [2]
> [1]
= [n__o()]
[u()] = [2]
> [1]
= [n__u()]
Further, it can be verified that all rules not oriented are covered by the weightgap condition.
We are left with following problem, upon which TcT provides the
certificate YES(O(1),O(n^1)).
Strict Trs:
{ __(X1, X2) -> n____(X1, X2)
, __(__(X, Y), Z) -> __(X, __(Y, Z)) }
Weak Trs:
{ __(X, nil()) -> X
, __(nil(), X) -> X
, nil() -> n__nil()
, and(tt(), X) -> activate(X)
, activate(X) -> X
, activate(n__nil()) -> nil()
, activate(n____(X1, X2)) -> __(X1, X2)
, activate(n__isList(X)) -> isList(X)
, activate(n__isNeList(X)) -> isNeList(X)
, activate(n__isPal(X)) -> isPal(X)
, activate(n__a()) -> a()
, activate(n__e()) -> e()
, activate(n__i()) -> i()
, activate(n__o()) -> o()
, activate(n__u()) -> u()
, isList(V) -> isNeList(activate(V))
, isList(X) -> n__isList(X)
, isList(n__nil()) -> tt()
, isList(n____(V1, V2)) ->
and(isList(activate(V1)), n__isList(activate(V2)))
, isNeList(V) -> isQid(activate(V))
, isNeList(X) -> n__isNeList(X)
, isNeList(n____(V1, V2)) ->
and(isList(activate(V1)), n__isNeList(activate(V2)))
, isNeList(n____(V1, V2)) ->
and(isNeList(activate(V1)), n__isList(activate(V2)))
, isQid(n__a()) -> tt()
, isQid(n__e()) -> tt()
, isQid(n__i()) -> tt()
, isQid(n__o()) -> tt()
, isQid(n__u()) -> tt()
, isNePal(V) -> isQid(activate(V))
, isNePal(n____(I, __(P, I))) ->
and(isQid(activate(I)), n__isPal(activate(P)))
, isPal(V) -> isNePal(activate(V))
, isPal(X) -> n__isPal(X)
, isPal(n__nil()) -> tt()
, a() -> n__a()
, e() -> n__e()
, i() -> n__i()
, o() -> n__o()
, u() -> n__u() }
Obligation:
runtime complexity
Answer:
YES(O(1),O(n^1))
The weightgap principle applies (using the following nonconstant
growth matrix-interpretation)
The following argument positions are usable:
Uargs(__) = {2}, Uargs(and) = {1, 2}, Uargs(activate) = {1},
Uargs(isList) = {1}, Uargs(isNeList) = {1}, Uargs(n____) = {2},
Uargs(n__isList) = {1}, Uargs(isQid) = {1},
Uargs(n__isNeList) = {1}, Uargs(isNePal) = {1},
Uargs(n__isPal) = {1}, Uargs(isPal) = {1}
TcT has computed the following matrix interpretation satisfying
not(EDA) and not(IDA(1)).
[__](x1, x2) = [1] x1 + [1] x2 + [5]
[nil] = [0]
[and](x1, x2) = [1] x1 + [1] x2 + [0]
[tt] = [1]
[activate](x1) = [1] x1 + [1]
[isList](x1) = [1] x1 + [2]
[isNeList](x1) = [1] x1 + [1]
[n__nil] = [0]
[n____](x1, x2) = [1] x1 + [1] x2 + [4]
[n__isList](x1) = [1] x1 + [2]
[isQid](x1) = [1] x1 + [0]
[n__isNeList](x1) = [1] x1 + [1]
[isNePal](x1) = [1] x1 + [2]
[n__isPal](x1) = [1] x1 + [2]
[isPal](x1) = [1] x1 + [3]
[n__a] = [4]
[n__e] = [1]
[n__i] = [4]
[n__o] = [4]
[n__u] = [4]
[a] = [4]
[e] = [1]
[i] = [4]
[o] = [4]
[u] = [4]
The order satisfies the following ordering constraints:
[__(X1, X2)] = [1] X1 + [1] X2 + [5]
> [1] X1 + [1] X2 + [4]
= [n____(X1, X2)]
[__(X, nil())] = [1] X + [5]
> [1] X + [0]
= [X]
[__(__(X, Y), Z)] = [1] X + [1] Y + [1] Z + [10]
>= [1] X + [1] Y + [1] Z + [10]
= [__(X, __(Y, Z))]
[__(nil(), X)] = [1] X + [5]
> [1] X + [0]
= [X]
[nil()] = [0]
>= [0]
= [n__nil()]
[and(tt(), X)] = [1] X + [1]
>= [1] X + [1]
= [activate(X)]
[activate(X)] = [1] X + [1]
> [1] X + [0]
= [X]
[activate(n__nil())] = [1]
> [0]
= [nil()]
[activate(n____(X1, X2))] = [1] X1 + [1] X2 + [5]
>= [1] X1 + [1] X2 + [5]
= [__(X1, X2)]
[activate(n__isList(X))] = [1] X + [3]
> [1] X + [2]
= [isList(X)]
[activate(n__isNeList(X))] = [1] X + [2]
> [1] X + [1]
= [isNeList(X)]
[activate(n__isPal(X))] = [1] X + [3]
>= [1] X + [3]
= [isPal(X)]
[activate(n__a())] = [5]
> [4]
= [a()]
[activate(n__e())] = [2]
> [1]
= [e()]
[activate(n__i())] = [5]
> [4]
= [i()]
[activate(n__o())] = [5]
> [4]
= [o()]
[activate(n__u())] = [5]
> [4]
= [u()]
[isList(V)] = [1] V + [2]
>= [1] V + [2]
= [isNeList(activate(V))]
[isList(X)] = [1] X + [2]
>= [1] X + [2]
= [n__isList(X)]
[isList(n__nil())] = [2]
> [1]
= [tt()]
[isList(n____(V1, V2))] = [1] V1 + [1] V2 + [6]
>= [1] V1 + [1] V2 + [6]
= [and(isList(activate(V1)), n__isList(activate(V2)))]
[isNeList(V)] = [1] V + [1]
>= [1] V + [1]
= [isQid(activate(V))]
[isNeList(X)] = [1] X + [1]
>= [1] X + [1]
= [n__isNeList(X)]
[isNeList(n____(V1, V2))] = [1] V1 + [1] V2 + [5]
>= [1] V1 + [1] V2 + [5]
= [and(isList(activate(V1)), n__isNeList(activate(V2)))]
[isNeList(n____(V1, V2))] = [1] V1 + [1] V2 + [5]
>= [1] V1 + [1] V2 + [5]
= [and(isNeList(activate(V1)), n__isList(activate(V2)))]
[isQid(n__a())] = [4]
> [1]
= [tt()]
[isQid(n__e())] = [1]
>= [1]
= [tt()]
[isQid(n__i())] = [4]
> [1]
= [tt()]
[isQid(n__o())] = [4]
> [1]
= [tt()]
[isQid(n__u())] = [4]
> [1]
= [tt()]
[isNePal(V)] = [1] V + [2]
> [1] V + [1]
= [isQid(activate(V))]
[isNePal(n____(I, __(P, I)))] = [2] I + [1] P + [11]
> [1] I + [1] P + [4]
= [and(isQid(activate(I)), n__isPal(activate(P)))]
[isPal(V)] = [1] V + [3]
>= [1] V + [3]
= [isNePal(activate(V))]
[isPal(X)] = [1] X + [3]
> [1] X + [2]
= [n__isPal(X)]
[isPal(n__nil())] = [3]
> [1]
= [tt()]
[a()] = [4]
>= [4]
= [n__a()]
[e()] = [1]
>= [1]
= [n__e()]
[i()] = [4]
>= [4]
= [n__i()]
[o()] = [4]
>= [4]
= [n__o()]
[u()] = [4]
>= [4]
= [n__u()]
Further, it can be verified that all rules not oriented are covered by the weightgap condition.
We are left with following problem, upon which TcT provides the
certificate YES(O(1),O(n^1)).
Strict Trs: { __(__(X, Y), Z) -> __(X, __(Y, Z)) }
Weak Trs:
{ __(X1, X2) -> n____(X1, X2)
, __(X, nil()) -> X
, __(nil(), X) -> X
, nil() -> n__nil()
, and(tt(), X) -> activate(X)
, activate(X) -> X
, activate(n__nil()) -> nil()
, activate(n____(X1, X2)) -> __(X1, X2)
, activate(n__isList(X)) -> isList(X)
, activate(n__isNeList(X)) -> isNeList(X)
, activate(n__isPal(X)) -> isPal(X)
, activate(n__a()) -> a()
, activate(n__e()) -> e()
, activate(n__i()) -> i()
, activate(n__o()) -> o()
, activate(n__u()) -> u()
, isList(V) -> isNeList(activate(V))
, isList(X) -> n__isList(X)
, isList(n__nil()) -> tt()
, isList(n____(V1, V2)) ->
and(isList(activate(V1)), n__isList(activate(V2)))
, isNeList(V) -> isQid(activate(V))
, isNeList(X) -> n__isNeList(X)
, isNeList(n____(V1, V2)) ->
and(isList(activate(V1)), n__isNeList(activate(V2)))
, isNeList(n____(V1, V2)) ->
and(isNeList(activate(V1)), n__isList(activate(V2)))
, isQid(n__a()) -> tt()
, isQid(n__e()) -> tt()
, isQid(n__i()) -> tt()
, isQid(n__o()) -> tt()
, isQid(n__u()) -> tt()
, isNePal(V) -> isQid(activate(V))
, isNePal(n____(I, __(P, I))) ->
and(isQid(activate(I)), n__isPal(activate(P)))
, isPal(V) -> isNePal(activate(V))
, isPal(X) -> n__isPal(X)
, isPal(n__nil()) -> tt()
, a() -> n__a()
, e() -> n__e()
, i() -> n__i()
, o() -> n__o()
, u() -> n__u() }
Obligation:
runtime complexity
Answer:
YES(O(1),O(n^1))
We use the processor 'matrix interpretation of dimension 2' to
orient following rules strictly.
Trs: { __(__(X, Y), Z) -> __(X, __(Y, Z)) }
The induced complexity on above rules (modulo remaining rules) is
YES(?,O(n^1)) . These rules are moved into the corresponding weak
component(s).
Sub-proof:
----------
The following argument positions are usable:
Uargs(__) = {2}, Uargs(and) = {1, 2}, Uargs(activate) = {1},
Uargs(isList) = {1}, Uargs(isNeList) = {1}, Uargs(n____) = {2},
Uargs(n__isList) = {1}, Uargs(isQid) = {1},
Uargs(n__isNeList) = {1}, Uargs(isNePal) = {1},
Uargs(n__isPal) = {1}, Uargs(isPal) = {1}
TcT has computed the following constructor-based matrix
interpretation satisfying not(EDA) and not(IDA(1)).
[__](x1, x2) = [1 1] x1 + [1 0] x2 + [0]
[0 1] [0 1] [2]
[nil] = [4]
[0]
[and](x1, x2) = [1 0] x1 + [1 2] x2 + [0]
[1 0] [2 7] [0]
[tt] = [4]
[0]
[activate](x1) = [1 0] x1 + [0]
[2 6] [4]
[isList](x1) = [1 0] x1 + [0]
[2 0] [4]
[isNeList](x1) = [1 0] x1 + [0]
[2 0] [4]
[n__nil] = [4]
[0]
[n____](x1, x2) = [1 1] x1 + [1 0] x2 + [0]
[0 0] [0 1] [0]
[n__isList](x1) = [1 0] x1 + [0]
[0 0] [0]
[isQid](x1) = [1 0] x1 + [0]
[0 0] [0]
[n__isNeList](x1) = [1 0] x1 + [0]
[0 0] [0]
[isNePal](x1) = [1 0] x1 + [3]
[2 0] [6]
[n__isPal](x1) = [1 0] x1 + [3]
[0 0] [0]
[isPal](x1) = [1 0] x1 + [3]
[2 0] [6]
[n__a] = [5]
[0]
[n__e] = [5]
[0]
[n__i] = [5]
[0]
[n__o] = [4]
[0]
[n__u] = [4]
[0]
[a] = [5]
[0]
[e] = [5]
[0]
[i] = [5]
[0]
[o] = [4]
[0]
[u] = [4]
[0]
The order satisfies the following ordering constraints:
[__(X1, X2)] = [1 1] X1 + [1 0] X2 + [0]
[0 1] [0 1] [2]
>= [1 1] X1 + [1 0] X2 + [0]
[0 0] [0 1] [0]
= [n____(X1, X2)]
[__(X, nil())] = [1 1] X + [4]
[0 1] [2]
> [1 0] X + [0]
[0 1] [0]
= [X]
[__(__(X, Y), Z)] = [1 2] X + [1 1] Y + [1 0] Z + [2]
[0 1] [0 1] [0 1] [4]
> [1 1] X + [1 1] Y + [1 0] Z + [0]
[0 1] [0 1] [0 1] [4]
= [__(X, __(Y, Z))]
[__(nil(), X)] = [1 0] X + [4]
[0 1] [2]
> [1 0] X + [0]
[0 1] [0]
= [X]
[nil()] = [4]
[0]
>= [4]
[0]
= [n__nil()]
[and(tt(), X)] = [1 2] X + [4]
[2 7] [4]
> [1 0] X + [0]
[2 6] [4]
= [activate(X)]
[activate(X)] = [1 0] X + [0]
[2 6] [4]
>= [1 0] X + [0]
[0 1] [0]
= [X]
[activate(n__nil())] = [4]
[12]
>= [4]
[0]
= [nil()]
[activate(n____(X1, X2))] = [1 1] X1 + [1 0] X2 + [0]
[2 2] [2 6] [4]
>= [1 1] X1 + [1 0] X2 + [0]
[0 1] [0 1] [2]
= [__(X1, X2)]
[activate(n__isList(X))] = [1 0] X + [0]
[2 0] [4]
>= [1 0] X + [0]
[2 0] [4]
= [isList(X)]
[activate(n__isNeList(X))] = [1 0] X + [0]
[2 0] [4]
>= [1 0] X + [0]
[2 0] [4]
= [isNeList(X)]
[activate(n__isPal(X))] = [1 0] X + [3]
[2 0] [10]
>= [1 0] X + [3]
[2 0] [6]
= [isPal(X)]
[activate(n__a())] = [5]
[14]
>= [5]
[0]
= [a()]
[activate(n__e())] = [5]
[14]
>= [5]
[0]
= [e()]
[activate(n__i())] = [5]
[14]
>= [5]
[0]
= [i()]
[activate(n__o())] = [4]
[12]
>= [4]
[0]
= [o()]
[activate(n__u())] = [4]
[12]
>= [4]
[0]
= [u()]
[isList(V)] = [1 0] V + [0]
[2 0] [4]
>= [1 0] V + [0]
[2 0] [4]
= [isNeList(activate(V))]
[isList(X)] = [1 0] X + [0]
[2 0] [4]
>= [1 0] X + [0]
[0 0] [0]
= [n__isList(X)]
[isList(n__nil())] = [4]
[12]
>= [4]
[0]
= [tt()]
[isList(n____(V1, V2))] = [1 1] V1 + [1 0] V2 + [0]
[2 2] [2 0] [4]
>= [1 0] V1 + [1 0] V2 + [0]
[1 0] [2 0] [0]
= [and(isList(activate(V1)), n__isList(activate(V2)))]
[isNeList(V)] = [1 0] V + [0]
[2 0] [4]
>= [1 0] V + [0]
[0 0] [0]
= [isQid(activate(V))]
[isNeList(X)] = [1 0] X + [0]
[2 0] [4]
>= [1 0] X + [0]
[0 0] [0]
= [n__isNeList(X)]
[isNeList(n____(V1, V2))] = [1 1] V1 + [1 0] V2 + [0]
[2 2] [2 0] [4]
>= [1 0] V1 + [1 0] V2 + [0]
[1 0] [2 0] [0]
= [and(isList(activate(V1)), n__isNeList(activate(V2)))]
[isNeList(n____(V1, V2))] = [1 1] V1 + [1 0] V2 + [0]
[2 2] [2 0] [4]
>= [1 0] V1 + [1 0] V2 + [0]
[1 0] [2 0] [0]
= [and(isNeList(activate(V1)), n__isList(activate(V2)))]
[isQid(n__a())] = [5]
[0]
> [4]
[0]
= [tt()]
[isQid(n__e())] = [5]
[0]
> [4]
[0]
= [tt()]
[isQid(n__i())] = [5]
[0]
> [4]
[0]
= [tt()]
[isQid(n__o())] = [4]
[0]
>= [4]
[0]
= [tt()]
[isQid(n__u())] = [4]
[0]
>= [4]
[0]
= [tt()]
[isNePal(V)] = [1 0] V + [3]
[2 0] [6]
> [1 0] V + [0]
[0 0] [0]
= [isQid(activate(V))]
[isNePal(n____(I, __(P, I)))] = [2 1] I + [1 1] P + [3]
[4 2] [2 2] [6]
>= [1 0] I + [1 0] P + [3]
[1 0] [2 0] [6]
= [and(isQid(activate(I)), n__isPal(activate(P)))]
[isPal(V)] = [1 0] V + [3]
[2 0] [6]
>= [1 0] V + [3]
[2 0] [6]
= [isNePal(activate(V))]
[isPal(X)] = [1 0] X + [3]
[2 0] [6]
>= [1 0] X + [3]
[0 0] [0]
= [n__isPal(X)]
[isPal(n__nil())] = [7]
[14]
> [4]
[0]
= [tt()]
[a()] = [5]
[0]
>= [5]
[0]
= [n__a()]
[e()] = [5]
[0]
>= [5]
[0]
= [n__e()]
[i()] = [5]
[0]
>= [5]
[0]
= [n__i()]
[o()] = [4]
[0]
>= [4]
[0]
= [n__o()]
[u()] = [4]
[0]
>= [4]
[0]
= [n__u()]
We return to the main proof.
We are left with following problem, upon which TcT provides the
certificate YES(O(1),O(1)).
Weak Trs:
{ __(X1, X2) -> n____(X1, X2)
, __(X, nil()) -> X
, __(__(X, Y), Z) -> __(X, __(Y, Z))
, __(nil(), X) -> X
, nil() -> n__nil()
, and(tt(), X) -> activate(X)
, activate(X) -> X
, activate(n__nil()) -> nil()
, activate(n____(X1, X2)) -> __(X1, X2)
, activate(n__isList(X)) -> isList(X)
, activate(n__isNeList(X)) -> isNeList(X)
, activate(n__isPal(X)) -> isPal(X)
, activate(n__a()) -> a()
, activate(n__e()) -> e()
, activate(n__i()) -> i()
, activate(n__o()) -> o()
, activate(n__u()) -> u()
, isList(V) -> isNeList(activate(V))
, isList(X) -> n__isList(X)
, isList(n__nil()) -> tt()
, isList(n____(V1, V2)) ->
and(isList(activate(V1)), n__isList(activate(V2)))
, isNeList(V) -> isQid(activate(V))
, isNeList(X) -> n__isNeList(X)
, isNeList(n____(V1, V2)) ->
and(isList(activate(V1)), n__isNeList(activate(V2)))
, isNeList(n____(V1, V2)) ->
and(isNeList(activate(V1)), n__isList(activate(V2)))
, isQid(n__a()) -> tt()
, isQid(n__e()) -> tt()
, isQid(n__i()) -> tt()
, isQid(n__o()) -> tt()
, isQid(n__u()) -> tt()
, isNePal(V) -> isQid(activate(V))
, isNePal(n____(I, __(P, I))) ->
and(isQid(activate(I)), n__isPal(activate(P)))
, isPal(V) -> isNePal(activate(V))
, isPal(X) -> n__isPal(X)
, isPal(n__nil()) -> tt()
, a() -> n__a()
, e() -> n__e()
, i() -> n__i()
, o() -> n__o()
, u() -> n__u() }
Obligation:
runtime complexity
Answer:
YES(O(1),O(1))
Empty rules are trivially bounded
Hurray, we answered YES(O(1),O(n^1))