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:
innermost runtime complexity
Answer:
YES(O(1),O(n^1))
Arguments of following rules are not normal-forms:
{ __(X, nil()) -> X
, __(__(X, Y), Z) -> __(X, __(Y, Z))
, __(nil(), X) -> X
, isNePal(n____(I, __(P, I))) ->
and(isQid(activate(I)), n__isPal(activate(P))) }
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^1)).
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)) -> __(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))
, 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^1))
The weightgap principle applies (using the following nonconstant
growth matrix-interpretation)
The following argument positions are usable:
Uargs(and) = {1, 2}, Uargs(isList) = {1}, Uargs(isNeList) = {1},
Uargs(n__isList) = {1}, Uargs(isQid) = {1},
Uargs(n__isNeList) = {1}, Uargs(isNePal) = {1}
TcT has computed the following matrix interpretation satisfying
not(EDA) and not(IDA(1)).
[__](x1, x2) = [1] x1 + [1] x2 + [2]
[nil] = [0]
[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] = [1]
[n____](x1, x2) = [1] x1 + [1] x2 + [0]
[n__isList](x1) = [1] x1 + [0]
[isQid](x1) = [1] x1 + [1]
[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] = [2]
[a] = [1]
[e] = [2]
[i] = [0]
[o] = [1]
[u] = [2]
The order satisfies the following ordering constraints:
[__(X1, X2)] = [1] X1 + [1] X2 + [2]
> [1] X1 + [1] X2 + [0]
= [n____(X1, X2)]
[nil()] = [0]
? [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]
> [0]
= [nil()]
[activate(n____(X1, X2))] = [1] X1 + [1] X2 + [0]
? [1] X1 + [1] X2 + [2]
= [__(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]
? [2]
= [e()]
[activate(n__i())] = [0]
>= [0]
= [i()]
[activate(n__o())] = [0]
? [1]
= [o()]
[activate(n__u())] = [2]
>= [2]
= [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]
? [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 + [1]
= [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 + [4]
= [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]
? [4]
= [tt()]
[isQid(n__e())] = [1]
? [4]
= [tt()]
[isQid(n__i())] = [1]
? [4]
= [tt()]
[isQid(n__o())] = [1]
? [4]
= [tt()]
[isQid(n__u())] = [3]
? [4]
= [tt()]
[isNePal(V)] = [1] V + [0]
? [1] V + [1]
= [isQid(activate(V))]
[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]
> [4]
= [tt()]
[a()] = [1]
> [0]
= [n__a()]
[e()] = [2]
> [0]
= [n__e()]
[i()] = [0]
>= [0]
= [n__i()]
[o()] = [1]
> [0]
= [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:
{ nil() -> n__nil()
, 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(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))
, i() -> n__i()
, u() -> n__u() }
Weak Trs:
{ __(X1, X2) -> n____(X1, X2)
, and(tt(), X) -> activate(X)
, activate(n__nil()) -> nil()
, activate(n__isNeList(X)) -> isNeList(X)
, isPal(V) -> isNePal(activate(V))
, isPal(X) -> n__isPal(X)
, isPal(n__nil()) -> tt()
, a() -> n__a()
, e() -> n__e()
, o() -> n__o() }
Obligation:
innermost 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(and) = {1, 2}, Uargs(isList) = {1}, Uargs(isNeList) = {1},
Uargs(n__isList) = {1}, Uargs(isQid) = {1},
Uargs(n__isNeList) = {1}, Uargs(isNePal) = {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] = [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 + [4]
[isNePal](x1) = [1] x1 + [0]
[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] = [5]
[e] = [5]
[i] = [6]
[o] = [5]
[u] = [1]
The order satisfies the following ordering constraints:
[__(X1, X2)] = [1] X1 + [1] X2 + [5]
> [1] X1 + [1] X2 + [0]
= [n____(X1, X2)]
[nil()] = [0]
>= [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]
>= [0]
= [nil()]
[activate(n____(X1, X2))] = [1] X1 + [1] X2 + [0]
? [1] X1 + [1] X2 + [5]
= [__(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 + [4]
>= [1] X + [4]
= [isPal(X)]
[activate(n__a())] = [0]
? [5]
= [a()]
[activate(n__e())] = [0]
? [5]
= [e()]
[activate(n__i())] = [0]
? [6]
= [i()]
[activate(n__o())] = [0]
? [5]
= [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())] = [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 + [4]
= [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 + [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))]
[isPal(V)] = [1] V + [4]
> [1] V + [0]
= [isNePal(activate(V))]
[isPal(X)] = [1] X + [4]
>= [1] X + [4]
= [n__isPal(X)]
[isPal(n__nil())] = [4]
>= [4]
= [tt()]
[a()] = [5]
> [0]
= [n__a()]
[e()] = [5]
> [0]
= [n__e()]
[i()] = [6]
> [0]
= [n__i()]
[o()] = [5]
> [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:
{ nil() -> n__nil()
, 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(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)) }
Weak Trs:
{ __(X1, X2) -> n____(X1, X2)
, and(tt(), X) -> activate(X)
, activate(n__nil()) -> nil()
, activate(n__isNeList(X)) -> isNeList(X)
, 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^1))
The weightgap principle applies (using the following nonconstant
growth matrix-interpretation)
The following argument positions are usable:
Uargs(and) = {1, 2}, Uargs(isList) = {1}, Uargs(isNeList) = {1},
Uargs(n__isList) = {1}, Uargs(isQid) = {1},
Uargs(n__isNeList) = {1}, Uargs(isNePal) = {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] = [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 + [1]
[isQid](x1) = [1] x1 + [0]
[n__isNeList](x1) = [1] x1 + [4]
[isNePal](x1) = [1] x1 + [0]
[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] = [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()] = [0]
>= [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]
>= [0]
= [nil()]
[activate(n____(X1, X2))] = [1] X1 + [1] X2 + [0]
? [1] X1 + [1] X2 + [5]
= [__(X1, X2)]
[activate(n__isList(X))] = [1] X + [1]
> [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 + [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())] = [0]
? [5]
= [u()]
[isList(V)] = [1] V + [0]
>= [1] V + [0]
= [isNeList(activate(V))]
[isList(X)] = [1] X + [0]
? [1] X + [1]
= [n__isList(X)]
[isList(n__nil())] = [0]
? [4]
= [tt()]
[isList(n____(V1, V2))] = [1] V1 + [1] V2 + [0]
? [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 + [4]
= [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 + [1]
= [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))]
[isPal(V)] = [1] V + [4]
> [1] V + [0]
= [isNePal(activate(V))]
[isPal(X)] = [1] X + [4]
>= [1] X + [4]
= [n__isPal(X)]
[isPal(n__nil())] = [4]
>= [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^1)).
Strict Trs:
{ nil() -> n__nil()
, activate(X) -> X
, activate(n____(X1, X2)) -> __(X1, X2)
, 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)) }
Weak Trs:
{ __(X1, X2) -> n____(X1, X2)
, and(tt(), X) -> activate(X)
, activate(n__nil()) -> nil()
, activate(n__isList(X)) -> isList(X)
, activate(n__isNeList(X)) -> isNeList(X)
, 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^1))
The weightgap principle applies (using the following nonconstant
growth matrix-interpretation)
The following argument positions are usable:
Uargs(and) = {1, 2}, Uargs(isList) = {1}, Uargs(isNeList) = {1},
Uargs(n__isList) = {1}, Uargs(isQid) = {1},
Uargs(n__isNeList) = {1}, Uargs(isNePal) = {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] = [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 + [3]
[isNePal](x1) = [1] x1 + [0]
[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] = [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()] = [0]
>= [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]
> [0]
= [nil()]
[activate(n____(X1, X2))] = [1] X1 + [1] X2 + [1]
? [1] X1 + [1] X2 + [5]
= [__(X1, X2)]
[activate(n__isList(X))] = [1] X + [8]
> [1] X + [0]
= [isList(X)]
[activate(n__isNeList(X))] = [1] X + [4]
> [1] X + [0]
= [isNeList(X)]
[activate(n__isPal(X))] = [1] X + [5]
> [1] X + [4]
= [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 + [3]
= [n__isNeList(X)]
[isNeList(n____(V1, V2))] = [1] V1 + [1] V2 + [0]
? [1] V1 + [1] V2 + [5]
= [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))]
[isPal(V)] = [1] V + [4]
> [1] V + [1]
= [isNePal(activate(V))]
[isPal(X)] = [1] X + [4]
>= [1] X + [4]
= [n__isPal(X)]
[isPal(n__nil())] = [4]
>= [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^1)).
Strict Trs:
{ nil() -> n__nil()
, activate(n____(X1, X2)) -> __(X1, X2)
, activate(n__a()) -> a()
, activate(n__e()) -> e()
, activate(n__i()) -> i()
, activate(n__o()) -> o()
, activate(n__u()) -> u()
, 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)) }
Weak Trs:
{ __(X1, X2) -> n____(X1, X2)
, 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)
, 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^1))
The weightgap principle applies (using the following nonconstant
growth matrix-interpretation)
The following argument positions are usable:
Uargs(and) = {1, 2}, Uargs(isList) = {1}, Uargs(isNeList) = {1},
Uargs(n__isList) = {1}, Uargs(isQid) = {1},
Uargs(n__isNeList) = {1}, Uargs(isNePal) = {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] = [4]
[activate](x1) = [1] x1 + [0]
[isList](x1) = [1] x1 + [3]
[isNeList](x1) = [1] x1 + [0]
[n__nil] = [1]
[n____](x1, x2) = [1] x1 + [1] x2 + [1]
[n__isList](x1) = [1] x1 + [5]
[isQid](x1) = [1] x1 + [0]
[n__isNeList](x1) = [1] x1 + [5]
[isNePal](x1) = [1] x1 + [0]
[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] = [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 + [1]
= [n____(X1, X2)]
[nil()] = [0]
? [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]
> [0]
= [nil()]
[activate(n____(X1, X2))] = [1] X1 + [1] X2 + [1]
? [1] X1 + [1] X2 + [5]
= [__(X1, X2)]
[activate(n__isList(X))] = [1] X + [5]
> [1] X + [3]
= [isList(X)]
[activate(n__isNeList(X))] = [1] X + [5]
> [1] X + [0]
= [isNeList(X)]
[activate(n__isPal(X))] = [1] X + [4]
>= [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())] = [0]
? [5]
= [u()]
[isList(V)] = [1] V + [3]
> [1] V + [0]
= [isNeList(activate(V))]
[isList(X)] = [1] X + [3]
? [1] X + [5]
= [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 + [0]
>= [1] V + [0]
= [isQid(activate(V))]
[isNeList(X)] = [1] X + [0]
? [1] X + [5]
= [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 + [0]
>= [1] V + [0]
= [isQid(activate(V))]
[isPal(V)] = [1] V + [4]
> [1] V + [0]
= [isNePal(activate(V))]
[isPal(X)] = [1] X + [4]
>= [1] X + [4]
= [n__isPal(X)]
[isPal(n__nil())] = [5]
> [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^1)).
Strict Trs:
{ nil() -> n__nil()
, activate(n____(X1, X2)) -> __(X1, X2)
, activate(n__a()) -> a()
, activate(n__e()) -> e()
, activate(n__i()) -> i()
, activate(n__o()) -> o()
, activate(n__u()) -> u()
, 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)) }
Weak Trs:
{ __(X1, X2) -> n____(X1, X2)
, 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)
, isList(V) -> isNeList(activate(V))
, 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^1))
The weightgap principle applies (using the following nonconstant
growth matrix-interpretation)
The following argument positions are usable:
Uargs(and) = {1, 2}, Uargs(isList) = {1}, Uargs(isNeList) = {1},
Uargs(n__isList) = {1}, Uargs(isQid) = {1},
Uargs(n__isNeList) = {1}, Uargs(isNePal) = {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] = [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 + [4]
[isPal](x1) = [1] x1 + [4]
[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()] = [0]
>= [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]
>= [0]
= [nil()]
[activate(n____(X1, X2))] = [1] X1 + [1] X2 + [0]
? [1] X1 + [1] X2 + [5]
= [__(X1, 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 + [4]
>= [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())] = [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))]
[isPal(V)] = [1] V + [4]
> [1] V + [1]
= [isNePal(activate(V))]
[isPal(X)] = [1] X + [4]
>= [1] X + [4]
= [n__isPal(X)]
[isPal(n__nil())] = [4]
>= [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^1)).
Strict Trs:
{ nil() -> n__nil()
, activate(n____(X1, X2)) -> __(X1, X2)
, activate(n__a()) -> a()
, activate(n__e()) -> e()
, activate(n__i()) -> i()
, activate(n__o()) -> o()
, activate(n__u()) -> u()
, 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() }
Weak Trs:
{ __(X1, X2) -> n____(X1, X2)
, 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)
, isList(V) -> isNeList(activate(V))
, isNeList(V) -> isQid(activate(V))
, isNePal(V) -> isQid(activate(V))
, 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^1))
The weightgap principle applies (using the following nonconstant
growth matrix-interpretation)
The following argument positions are usable:
Uargs(and) = {1, 2}, Uargs(isList) = {1}, Uargs(isNeList) = {1},
Uargs(n__isList) = {1}, Uargs(isQid) = {1},
Uargs(n__isNeList) = {1}, Uargs(isNePal) = {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] = [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 + [4]
[isNePal](x1) = [1] x1 + [0]
[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] = [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()] = [0]
? [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]
> [0]
= [nil()]
[activate(n____(X1, X2))] = [1] X1 + [1] X2 + [0]
? [1] X1 + [1] X2 + [5]
= [__(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 + [4]
>= [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())] = [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 + [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 + [4]
= [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 + [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))]
[isPal(V)] = [1] V + [4]
> [1] V + [0]
= [isNePal(activate(V))]
[isPal(X)] = [1] X + [4]
>= [1] X + [4]
= [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]
> [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:
{ nil() -> n__nil()
, activate(n____(X1, X2)) -> __(X1, X2)
, activate(n__a()) -> a()
, activate(n__e()) -> e()
, activate(n__i()) -> i()
, activate(n__o()) -> o()
, activate(n__u()) -> u()
, 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() }
Weak Trs:
{ __(X1, X2) -> n____(X1, X2)
, 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)
, isList(V) -> isNeList(activate(V))
, isList(n__nil()) -> tt()
, isNeList(V) -> isQid(activate(V))
, isNePal(V) -> isQid(activate(V))
, 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^1))
The weightgap principle applies (using the following nonconstant
growth matrix-interpretation)
The following argument positions are usable:
Uargs(and) = {1, 2}, Uargs(isList) = {1}, Uargs(isNeList) = {1},
Uargs(n__isList) = {1}, Uargs(isQid) = {1},
Uargs(n__isNeList) = {1}, Uargs(isNePal) = {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] = [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 + [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 + [4]
[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 + [5]
> [1] X1 + [1] X2 + [0]
= [n____(X1, X2)]
[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 + [5]
= [__(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 + [4]
>= [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())] = [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 + [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 + [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 + [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))]
[isPal(V)] = [1] V + [4]
> [1] V + [0]
= [isNePal(activate(V))]
[isPal(X)] = [1] X + [4]
>= [1] X + [4]
= [n__isPal(X)]
[isPal(n__nil())] = [4]
> [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:
{ nil() -> n__nil()
, activate(n____(X1, X2)) -> __(X1, X2)
, activate(n__a()) -> a()
, activate(n__e()) -> e()
, activate(n__i()) -> i()
, activate(n__o()) -> o()
, activate(n__u()) -> u()
, 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__i()) -> tt()
, isQid(n__o()) -> tt()
, isQid(n__u()) -> tt() }
Weak Trs:
{ __(X1, X2) -> n____(X1, X2)
, 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)
, isList(V) -> isNeList(activate(V))
, isList(n__nil()) -> tt()
, isNeList(V) -> isQid(activate(V))
, isQid(n__a()) -> tt()
, isNePal(V) -> isQid(activate(V))
, 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^1))
The weightgap principle applies (using the following nonconstant
growth matrix-interpretation)
The following argument positions are usable:
Uargs(and) = {1, 2}, Uargs(isList) = {1}, Uargs(isNeList) = {1},
Uargs(n__isList) = {1}, Uargs(isQid) = {1},
Uargs(n__isNeList) = {1}, Uargs(isNePal) = {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] = [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 + [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 + [4]
[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 + [5]
> [1] X1 + [1] X2 + [0]
= [n____(X1, X2)]
[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 + [5]
= [__(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 + [4]
>= [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())] = [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 + [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 + [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 + [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))]
[isPal(V)] = [1] V + [4]
> [1] V + [0]
= [isNePal(activate(V))]
[isPal(X)] = [1] X + [4]
>= [1] X + [4]
= [n__isPal(X)]
[isPal(n__nil())] = [4]
> [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:
{ nil() -> n__nil()
, activate(n____(X1, X2)) -> __(X1, X2)
, activate(n__a()) -> a()
, activate(n__e()) -> e()
, activate(n__i()) -> i()
, activate(n__o()) -> o()
, activate(n__u()) -> u()
, 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__i()) -> tt()
, isQid(n__o()) -> tt()
, isQid(n__u()) -> tt() }
Weak Trs:
{ __(X1, X2) -> n____(X1, X2)
, 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)
, isList(V) -> isNeList(activate(V))
, isList(n__nil()) -> tt()
, isNeList(V) -> isQid(activate(V))
, isQid(n__a()) -> tt()
, isQid(n__e()) -> tt()
, isNePal(V) -> isQid(activate(V))
, 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^1))
The weightgap principle applies (using the following nonconstant
growth matrix-interpretation)
The following argument positions are usable:
Uargs(and) = {1, 2}, Uargs(isList) = {1}, Uargs(isNeList) = {1},
Uargs(n__isList) = {1}, Uargs(isQid) = {1},
Uargs(n__isNeList) = {1}, Uargs(isNePal) = {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 + [4]
[isNeList](x1) = [1] x1 + [4]
[n__nil] = [4]
[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 + [4]
[isPal](x1) = [1] x1 + [4]
[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 + [1]
> [1] X1 + [1] X2 + [0]
= [n____(X1, X2)]
[nil()] = [0]
? [4]
= [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())] = [4]
> [0]
= [nil()]
[activate(n____(X1, X2))] = [1] X1 + [1] X2 + [0]
? [1] X1 + [1] X2 + [1]
= [__(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 + [4]
>= [1] X + [4]
= [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 + [4]
= [n__isList(X)]
[isList(n__nil())] = [8]
> [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 + [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 + [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 + [8]
= [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))]
[isPal(V)] = [1] V + [4]
> [1] V + [0]
= [isNePal(activate(V))]
[isPal(X)] = [1] X + [4]
>= [1] X + [4]
= [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:
{ nil() -> n__nil()
, activate(n____(X1, X2)) -> __(X1, X2)
, activate(n__a()) -> a()
, activate(n__e()) -> e()
, activate(n__i()) -> i()
, activate(n__o()) -> o()
, activate(n__u()) -> u()
, 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__o()) -> tt()
, isQid(n__u()) -> tt() }
Weak Trs:
{ __(X1, X2) -> n____(X1, X2)
, 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)
, 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()
, isNePal(V) -> isQid(activate(V))
, 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^1))
The weightgap principle applies (using the following nonconstant
growth matrix-interpretation)
The following argument positions are usable:
Uargs(and) = {1, 2}, Uargs(isList) = {1}, Uargs(isNeList) = {1},
Uargs(n__isList) = {1}, Uargs(isQid) = {1},
Uargs(n__isNeList) = {1}, Uargs(isNePal) = {1}
TcT has computed the following matrix interpretation satisfying
not(EDA) and not(IDA(1)).
[__](x1, x2) = [1] x1 + [1] x2 + [5]
[nil] = [2]
[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] = [4]
[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 + [4]
[n__isPal](x1) = [1] x1 + [4]
[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] = [1]
The order satisfies the following ordering constraints:
[__(X1, X2)] = [1] X1 + [1] X2 + [5]
> [1] X1 + [1] X2 + [4]
= [n____(X1, X2)]
[nil()] = [2]
? [4]
= [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())] = [4]
> [2]
= [nil()]
[activate(n____(X1, X2))] = [1] X1 + [1] X2 + [4]
? [1] X1 + [1] X2 + [5]
= [__(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 + [4]
>= [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]
? [1]
= [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())] = [8]
> [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 + [4]
> [1] V + [0]
= [isQid(activate(V))]
[isPal(V)] = [1] V + [4]
>= [1] V + [4]
= [isNePal(activate(V))]
[isPal(X)] = [1] X + [4]
>= [1] X + [4]
= [n__isPal(X)]
[isPal(n__nil())] = [8]
> [0]
= [tt()]
[a()] = [5]
> [0]
= [n__a()]
[e()] = [5]
> [0]
= [n__e()]
[i()] = [5]
> [0]
= [n__i()]
[o()] = [5]
> [1]
= [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:
{ nil() -> n__nil()
, activate(n____(X1, X2)) -> __(X1, X2)
, activate(n__a()) -> a()
, activate(n__e()) -> e()
, activate(n__i()) -> i()
, activate(n__o()) -> o()
, activate(n__u()) -> u()
, 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() }
Weak Trs:
{ __(X1, X2) -> n____(X1, X2)
, 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)
, 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))
, 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^1))
The weightgap principle applies (using the following nonconstant
growth matrix-interpretation)
The following argument positions are usable:
Uargs(and) = {1, 2}, Uargs(isList) = {1}, Uargs(isNeList) = {1},
Uargs(n__isList) = {1}, Uargs(isQid) = {1},
Uargs(n__isNeList) = {1}, Uargs(isNePal) = {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] = [0]
[activate](x1) = [1] x1 + [0]
[isList](x1) = [1] x1 + [4]
[isNeList](x1) = [1] x1 + [4]
[n__nil] = [4]
[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 + [4]
[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 + [5]
> [1] X1 + [1] X2 + [0]
= [n____(X1, X2)]
[nil()] = [0]
? [4]
= [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())] = [4]
> [0]
= [nil()]
[activate(n____(X1, X2))] = [1] X1 + [1] X2 + [0]
? [1] X1 + [1] X2 + [5]
= [__(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 + [4]
>= [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 + [4]
>= [1] V + [4]
= [isNeList(activate(V))]
[isList(X)] = [1] X + [4]
>= [1] X + [4]
= [n__isList(X)]
[isList(n__nil())] = [8]
> [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 + [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 + [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 + [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())] = [0]
>= [0]
= [tt()]
[isQid(n__u())] = [1]
> [0]
= [tt()]
[isNePal(V)] = [1] V + [0]
>= [1] V + [0]
= [isQid(activate(V))]
[isPal(V)] = [1] V + [4]
> [1] V + [0]
= [isNePal(activate(V))]
[isPal(X)] = [1] X + [4]
>= [1] X + [4]
= [n__isPal(X)]
[isPal(n__nil())] = [8]
> [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:
{ nil() -> n__nil()
, activate(n____(X1, X2)) -> __(X1, X2)
, activate(n__a()) -> a()
, activate(n__e()) -> e()
, activate(n__i()) -> i()
, activate(n__o()) -> o()
, activate(n__u()) -> u()
, 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))) }
Weak Trs:
{ __(X1, X2) -> n____(X1, X2)
, 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)
, 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))
, 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^1))
The weightgap principle applies (using the following nonconstant
growth matrix-interpretation)
The following argument positions are usable:
Uargs(and) = {1, 2}, Uargs(isList) = {1}, Uargs(isNeList) = {1},
Uargs(n__isList) = {1}, Uargs(isQid) = {1},
Uargs(n__isNeList) = {1}, Uargs(isNePal) = {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 + [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 + [4]
[isPal](x1) = [1] x1 + [4]
[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 + [4]
> [1] X1 + [1] X2 + [1]
= [n____(X1, X2)]
[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 + [4]
= [__(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 + [4]
>= [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())] = [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 + [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())] = [0]
>= [0]
= [tt()]
[isNePal(V)] = [1] V + [0]
>= [1] V + [0]
= [isQid(activate(V))]
[isPal(V)] = [1] V + [4]
> [1] V + [0]
= [isNePal(activate(V))]
[isPal(X)] = [1] X + [4]
>= [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^1)).
Strict Trs:
{ nil() -> n__nil()
, activate(n____(X1, X2)) -> __(X1, X2)
, activate(n__a()) -> a()
, activate(n__e()) -> e()
, activate(n__i()) -> i()
, activate(n__o()) -> o()
, activate(n__u()) -> u()
, isList(X) -> n__isList(X)
, isNeList(X) -> n__isNeList(X) }
Weak Trs:
{ __(X1, X2) -> n____(X1, X2)
, 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)
, 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(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))
, 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^1))
The weightgap principle applies (using the following nonconstant
growth matrix-interpretation)
The following argument positions are usable:
Uargs(and) = {1, 2}, Uargs(isList) = {1}, Uargs(isNeList) = {1},
Uargs(n__isList) = {1}, Uargs(isQid) = {1},
Uargs(n__isNeList) = {1}, Uargs(isNePal) = {1}
TcT has computed the following matrix interpretation satisfying
not(EDA) and not(IDA(1)).
[__](x1, x2) = [1] x1 + [1] x2 + [4]
[nil] = [3]
[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] = [6]
[n____](x1, x2) = [1] x1 + [1] x2 + [4]
[n__isList](x1) = [1] x1 + [1]
[isQid](x1) = [1] x1 + [0]
[n__isNeList](x1) = [1] x1 + [1]
[isNePal](x1) = [1] x1 + [2]
[n__isPal](x1) = [1] x1 + [4]
[isPal](x1) = [1] x1 + [4]
[n__a] = [4]
[n__e] = [4]
[n__i] = [4]
[n__o] = [4]
[n__u] = [4]
[a] = [4]
[e] = [4]
[i] = [4]
[o] = [4]
[u] = [4]
The order satisfies the following ordering constraints:
[__(X1, X2)] = [1] X1 + [1] X2 + [4]
>= [1] X1 + [1] X2 + [4]
= [n____(X1, X2)]
[nil()] = [3]
? [6]
= [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())] = [7]
> [3]
= [nil()]
[activate(n____(X1, X2))] = [1] X1 + [1] X2 + [5]
> [1] X1 + [1] X2 + [4]
= [__(X1, X2)]
[activate(n__isList(X))] = [1] X + [2]
>= [1] X + [2]
= [isList(X)]
[activate(n__isNeList(X))] = [1] X + [2]
> [1] X + [1]
= [isNeList(X)]
[activate(n__isPal(X))] = [1] X + [5]
> [1] X + [4]
= [isPal(X)]
[activate(n__a())] = [5]
> [4]
= [a()]
[activate(n__e())] = [5]
> [4]
= [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 + [1]
= [n__isList(X)]
[isList(n__nil())] = [8]
> [1]
= [tt()]
[isList(n____(V1, V2))] = [1] V1 + [1] V2 + [6]
> [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 + [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 + [4]
= [and(isNeList(activate(V1)), n__isList(activate(V2)))]
[isQid(n__a())] = [4]
> [1]
= [tt()]
[isQid(n__e())] = [4]
> [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))]
[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())] = [10]
> [1]
= [tt()]
[a()] = [4]
>= [4]
= [n__a()]
[e()] = [4]
>= [4]
= [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:
{ nil() -> n__nil()
, isNeList(X) -> n__isNeList(X) }
Weak Trs:
{ __(X1, X2) -> n____(X1, X2)
, 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))
, 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^1))
The weightgap principle applies (using the following nonconstant
growth matrix-interpretation)
The following argument positions are usable:
Uargs(and) = {1, 2}, Uargs(isList) = {1}, Uargs(isNeList) = {1},
Uargs(n__isList) = {1}, Uargs(isQid) = {1},
Uargs(n__isNeList) = {1}, Uargs(isNePal) = {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] = [5]
[activate](x1) = [1] x1 + [1]
[isList](x1) = [1] x1 + [6]
[isNeList](x1) = [1] x1 + [1]
[n__nil] = [0]
[n____](x1, x2) = [1] x1 + [1] x2 + [7]
[n__isList](x1) = [1] x1 + [5]
[isQid](x1) = [1] x1 + [0]
[n__isNeList](x1) = [1] x1 + [0]
[isNePal](x1) = [1] x1 + [4]
[n__isPal](x1) = [1] x1 + [6]
[isPal](x1) = [1] x1 + [6]
[n__a] = [7]
[n__e] = [7]
[n__i] = [6]
[n__o] = [5]
[n__u] = [7]
[a] = [7]
[e] = [7]
[i] = [6]
[o] = [6]
[u] = [7]
The order satisfies the following ordering constraints:
[__(X1, X2)] = [1] X1 + [1] X2 + [7]
>= [1] X1 + [1] X2 + [7]
= [n____(X1, X2)]
[nil()] = [0]
>= [0]
= [n__nil()]
[and(tt(), X)] = [1] X + [5]
> [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 + [7]
= [__(X1, X2)]
[activate(n__isList(X))] = [1] X + [6]
>= [1] X + [6]
= [isList(X)]
[activate(n__isNeList(X))] = [1] X + [1]
>= [1] X + [1]
= [isNeList(X)]
[activate(n__isPal(X))] = [1] X + [7]
> [1] X + [6]
= [isPal(X)]
[activate(n__a())] = [8]
> [7]
= [a()]
[activate(n__e())] = [8]
> [7]
= [e()]
[activate(n__i())] = [7]
> [6]
= [i()]
[activate(n__o())] = [6]
>= [6]
= [o()]
[activate(n__u())] = [8]
> [7]
= [u()]
[isList(V)] = [1] V + [6]
> [1] V + [2]
= [isNeList(activate(V))]
[isList(X)] = [1] X + [6]
> [1] X + [5]
= [n__isList(X)]
[isList(n__nil())] = [6]
> [5]
= [tt()]
[isList(n____(V1, V2))] = [1] V1 + [1] V2 + [13]
>= [1] V1 + [1] V2 + [13]
= [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 + [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())] = [7]
> [5]
= [tt()]
[isQid(n__e())] = [7]
> [5]
= [tt()]
[isQid(n__i())] = [6]
> [5]
= [tt()]
[isQid(n__o())] = [5]
>= [5]
= [tt()]
[isQid(n__u())] = [7]
> [5]
= [tt()]
[isNePal(V)] = [1] V + [4]
> [1] V + [1]
= [isQid(activate(V))]
[isPal(V)] = [1] V + [6]
> [1] V + [5]
= [isNePal(activate(V))]
[isPal(X)] = [1] X + [6]
>= [1] X + [6]
= [n__isPal(X)]
[isPal(n__nil())] = [6]
> [5]
= [tt()]
[a()] = [7]
>= [7]
= [n__a()]
[e()] = [7]
>= [7]
= [n__e()]
[i()] = [6]
>= [6]
= [n__i()]
[o()] = [6]
> [5]
= [n__o()]
[u()] = [7]
>= [7]
= [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: { nil() -> n__nil() }
Weak Trs:
{ __(X1, X2) -> n____(X1, X2)
, 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))
, 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^1))
The weightgap principle applies (using the following nonconstant
growth matrix-interpretation)
The following argument positions are usable:
Uargs(and) = {1, 2}, Uargs(isList) = {1}, Uargs(isNeList) = {1},
Uargs(n__isList) = {1}, Uargs(isQid) = {1},
Uargs(n__isNeList) = {1}, Uargs(isNePal) = {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] = [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 + [0]
[isNePal](x1) = [1] x1 + [2]
[n__isPal](x1) = [1] x1 + [4]
[isPal](x1) = [1] x1 + [4]
[n__a] = [4]
[n__e] = [4]
[n__i] = [1]
[n__o] = [4]
[n__u] = [4]
[a] = [4]
[e] = [4]
[i] = [2]
[o] = [4]
[u] = [4]
The order satisfies the following ordering constraints:
[__(X1, X2)] = [1] X1 + [1] X2 + [4]
>= [1] X1 + [1] X2 + [4]
= [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 + [5]
> [1] X1 + [1] X2 + [4]
= [__(X1, X2)]
[activate(n__isList(X))] = [1] X + [3]
> [1] X + [2]
= [isList(X)]
[activate(n__isNeList(X))] = [1] X + [1]
>= [1] X + [1]
= [isNeList(X)]
[activate(n__isPal(X))] = [1] X + [5]
> [1] X + [4]
= [isPal(X)]
[activate(n__a())] = [5]
> [4]
= [a()]
[activate(n__e())] = [5]
> [4]
= [e()]
[activate(n__i())] = [2]
>= [2]
= [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 + [0]
= [n__isNeList(X)]
[isNeList(n____(V1, V2))] = [1] V1 + [1] V2 + [5]
> [1] V1 + [1] V2 + [4]
= [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())] = [4]
> [1]
= [tt()]
[isQid(n__i())] = [1]
>= [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))]
[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()] = [4]
>= [4]
= [n__a()]
[e()] = [4]
>= [4]
= [n__e()]
[i()] = [2]
> [1]
= [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(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)) -> __(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))
, 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^1))