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