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()
, U11(tt()) -> tt()
, U21(tt(), V2) -> U22(isList(activate(V2)))
, U22(tt()) -> tt()
, isList(V) -> U11(isNeList(activate(V)))
, isList(n__nil()) -> tt()
, isList(n____(V1, V2)) -> U21(isList(activate(V1)), activate(V2))
, activate(X) -> X
, activate(n__nil()) -> nil()
, activate(n____(X1, X2)) -> __(X1, X2)
, activate(n__a()) -> a()
, activate(n__e()) -> e()
, activate(n__i()) -> i()
, activate(n__o()) -> o()
, activate(n__u()) -> u()
, U31(tt()) -> tt()
, U41(tt(), V2) -> U42(isNeList(activate(V2)))
, U42(tt()) -> tt()
, isNeList(V) -> U31(isQid(activate(V)))
, isNeList(n____(V1, V2)) ->
U41(isList(activate(V1)), activate(V2))
, isNeList(n____(V1, V2)) ->
U51(isNeList(activate(V1)), activate(V2))
, U51(tt(), V2) -> U52(isList(activate(V2)))
, U52(tt()) -> tt()
, U61(tt()) -> tt()
, U71(tt(), P) -> U72(isPal(activate(P)))
, U72(tt()) -> tt()
, isPal(V) -> U81(isNePal(activate(V)))
, isPal(n__nil()) -> tt()
, U81(tt()) -> tt()
, isQid(n__a()) -> tt()
, isQid(n__e()) -> tt()
, isQid(n__i()) -> tt()
, isQid(n__o()) -> tt()
, isQid(n__u()) -> tt()
, isNePal(V) -> U61(isQid(activate(V)))
, isNePal(n____(I, __(P, I))) ->
U71(isQid(activate(I)), activate(P))
, a() -> n__a()
, e() -> n__e()
, i() -> n__i()
, o() -> n__o()
, u() -> n__u() }
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))) ->
U71(isQid(activate(I)), 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()
, U11(tt()) -> tt()
, U21(tt(), V2) -> U22(isList(activate(V2)))
, U22(tt()) -> tt()
, isList(V) -> U11(isNeList(activate(V)))
, isList(n__nil()) -> tt()
, isList(n____(V1, V2)) -> U21(isList(activate(V1)), activate(V2))
, activate(X) -> X
, activate(n__nil()) -> nil()
, activate(n____(X1, X2)) -> __(X1, X2)
, activate(n__a()) -> a()
, activate(n__e()) -> e()
, activate(n__i()) -> i()
, activate(n__o()) -> o()
, activate(n__u()) -> u()
, U31(tt()) -> tt()
, U41(tt(), V2) -> U42(isNeList(activate(V2)))
, U42(tt()) -> tt()
, isNeList(V) -> U31(isQid(activate(V)))
, isNeList(n____(V1, V2)) ->
U41(isList(activate(V1)), activate(V2))
, isNeList(n____(V1, V2)) ->
U51(isNeList(activate(V1)), activate(V2))
, U51(tt(), V2) -> U52(isList(activate(V2)))
, U52(tt()) -> tt()
, U61(tt()) -> tt()
, U71(tt(), P) -> U72(isPal(activate(P)))
, U72(tt()) -> tt()
, isPal(V) -> U81(isNePal(activate(V)))
, isPal(n__nil()) -> tt()
, U81(tt()) -> tt()
, isQid(n__a()) -> tt()
, isQid(n__e()) -> tt()
, isQid(n__i()) -> tt()
, isQid(n__o()) -> tt()
, isQid(n__u()) -> tt()
, isNePal(V) -> U61(isQid(activate(V)))
, 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(U11) = {1}, Uargs(U21) = {1, 2}, Uargs(U22) = {1},
Uargs(isList) = {1}, Uargs(U31) = {1}, Uargs(U41) = {1, 2},
Uargs(U42) = {1}, Uargs(isNeList) = {1}, Uargs(U51) = {1, 2},
Uargs(U52) = {1}, Uargs(U61) = {1}, Uargs(U72) = {1},
Uargs(isPal) = {1}, Uargs(U81) = {1}, Uargs(isQid) = {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]
[U11](x1) = [1] x1 + [0]
[tt] = [0]
[U21](x1, x2) = [1] x1 + [1] x2 + [0]
[U22](x1) = [1] x1 + [0]
[isList](x1) = [1] x1 + [0]
[activate](x1) = [1] x1 + [0]
[U31](x1) = [1] x1 + [0]
[U41](x1, x2) = [1] x1 + [1] x2 + [0]
[U42](x1) = [1] x1 + [0]
[isNeList](x1) = [1] x1 + [0]
[U51](x1, x2) = [1] x1 + [1] x2 + [0]
[U52](x1) = [1] x1 + [0]
[U61](x1) = [1] x1 + [0]
[U71](x1, x2) = [1] x1 + [1] x2 + [2]
[U72](x1) = [1] x1 + [0]
[isPal](x1) = [1] x1 + [0]
[U81](x1) = [1] x1 + [0]
[n__nil] = [0]
[n____](x1, x2) = [1] x1 + [1] x2 + [0]
[isQid](x1) = [1] x1 + [0]
[isNePal](x1) = [1] x1 + [0]
[n__a] = [0]
[n__e] = [0]
[n__i] = [0]
[n__o] = [0]
[n__u] = [0]
[a] = [0]
[e] = [0]
[i] = [2]
[o] = [0]
[u] = [0]
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()]
[U11(tt())] = [0]
>= [0]
= [tt()]
[U21(tt(), V2)] = [1] V2 + [0]
>= [1] V2 + [0]
= [U22(isList(activate(V2)))]
[U22(tt())] = [0]
>= [0]
= [tt()]
[isList(V)] = [1] V + [0]
>= [1] V + [0]
= [U11(isNeList(activate(V)))]
[isList(n__nil())] = [0]
>= [0]
= [tt()]
[isList(n____(V1, V2))] = [1] V2 + [1] V1 + [0]
>= [1] V2 + [1] V1 + [0]
= [U21(isList(activate(V1)), activate(V2))]
[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__a())] = [0]
>= [0]
= [a()]
[activate(n__e())] = [0]
>= [0]
= [e()]
[activate(n__i())] = [0]
? [2]
= [i()]
[activate(n__o())] = [0]
>= [0]
= [o()]
[activate(n__u())] = [0]
>= [0]
= [u()]
[U31(tt())] = [0]
>= [0]
= [tt()]
[U41(tt(), V2)] = [1] V2 + [0]
>= [1] V2 + [0]
= [U42(isNeList(activate(V2)))]
[U42(tt())] = [0]
>= [0]
= [tt()]
[isNeList(V)] = [1] V + [0]
>= [1] V + [0]
= [U31(isQid(activate(V)))]
[isNeList(n____(V1, V2))] = [1] V2 + [1] V1 + [0]
>= [1] V2 + [1] V1 + [0]
= [U41(isList(activate(V1)), activate(V2))]
[isNeList(n____(V1, V2))] = [1] V2 + [1] V1 + [0]
>= [1] V2 + [1] V1 + [0]
= [U51(isNeList(activate(V1)), activate(V2))]
[U51(tt(), V2)] = [1] V2 + [0]
>= [1] V2 + [0]
= [U52(isList(activate(V2)))]
[U52(tt())] = [0]
>= [0]
= [tt()]
[U61(tt())] = [0]
>= [0]
= [tt()]
[U71(tt(), P)] = [1] P + [2]
> [1] P + [0]
= [U72(isPal(activate(P)))]
[U72(tt())] = [0]
>= [0]
= [tt()]
[isPal(V)] = [1] V + [0]
>= [1] V + [0]
= [U81(isNePal(activate(V)))]
[isPal(n__nil())] = [0]
>= [0]
= [tt()]
[U81(tt())] = [0]
>= [0]
= [tt()]
[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]
= [U61(isQid(activate(V)))]
[a()] = [0]
>= [0]
= [n__a()]
[e()] = [0]
>= [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^1)).
Strict Trs:
{ nil() -> n__nil()
, U11(tt()) -> tt()
, U21(tt(), V2) -> U22(isList(activate(V2)))
, U22(tt()) -> tt()
, isList(V) -> U11(isNeList(activate(V)))
, isList(n__nil()) -> tt()
, isList(n____(V1, V2)) -> U21(isList(activate(V1)), activate(V2))
, activate(X) -> X
, activate(n__nil()) -> nil()
, activate(n____(X1, X2)) -> __(X1, X2)
, activate(n__a()) -> a()
, activate(n__e()) -> e()
, activate(n__i()) -> i()
, activate(n__o()) -> o()
, activate(n__u()) -> u()
, U31(tt()) -> tt()
, U41(tt(), V2) -> U42(isNeList(activate(V2)))
, U42(tt()) -> tt()
, isNeList(V) -> U31(isQid(activate(V)))
, isNeList(n____(V1, V2)) ->
U41(isList(activate(V1)), activate(V2))
, isNeList(n____(V1, V2)) ->
U51(isNeList(activate(V1)), activate(V2))
, U51(tt(), V2) -> U52(isList(activate(V2)))
, U52(tt()) -> tt()
, U61(tt()) -> tt()
, U72(tt()) -> tt()
, isPal(V) -> U81(isNePal(activate(V)))
, isPal(n__nil()) -> tt()
, U81(tt()) -> tt()
, isQid(n__a()) -> tt()
, isQid(n__e()) -> tt()
, isQid(n__i()) -> tt()
, isQid(n__o()) -> tt()
, isQid(n__u()) -> tt()
, isNePal(V) -> U61(isQid(activate(V)))
, a() -> n__a()
, e() -> n__e()
, o() -> n__o()
, u() -> n__u() }
Weak Trs:
{ __(X1, X2) -> n____(X1, X2)
, U71(tt(), P) -> U72(isPal(activate(P)))
, i() -> n__i() }
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(U11) = {1}, Uargs(U21) = {1, 2}, Uargs(U22) = {1},
Uargs(isList) = {1}, Uargs(U31) = {1}, Uargs(U41) = {1, 2},
Uargs(U42) = {1}, Uargs(isNeList) = {1}, Uargs(U51) = {1, 2},
Uargs(U52) = {1}, Uargs(U61) = {1}, Uargs(U72) = {1},
Uargs(isPal) = {1}, Uargs(U81) = {1}, Uargs(isQid) = {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] = [5]
[U11](x1) = [1] x1 + [0]
[tt] = [0]
[U21](x1, x2) = [1] x1 + [1] x2 + [0]
[U22](x1) = [1] x1 + [0]
[isList](x1) = [1] x1 + [0]
[activate](x1) = [1] x1 + [0]
[U31](x1) = [1] x1 + [0]
[U41](x1, x2) = [1] x1 + [1] x2 + [0]
[U42](x1) = [1] x1 + [0]
[isNeList](x1) = [1] x1 + [0]
[U51](x1, x2) = [1] x1 + [1] x2 + [0]
[U52](x1) = [1] x1 + [0]
[U61](x1) = [1] x1 + [0]
[U71](x1, x2) = [1] x1 + [1] x2 + [0]
[U72](x1) = [1] x1 + [0]
[isPal](x1) = [1] x1 + [0]
[U81](x1) = [1] x1 + [0]
[n__nil] = [0]
[n____](x1, x2) = [1] x1 + [1] x2 + [0]
[isQid](x1) = [1] x1 + [0]
[isNePal](x1) = [1] x1 + [0]
[n__a] = [0]
[n__e] = [0]
[n__i] = [0]
[n__o] = [0]
[n__u] = [0]
[a] = [0]
[e] = [0]
[i] = [5]
[o] = [0]
[u] = [0]
The order satisfies the following ordering constraints:
[__(X1, X2)] = [1] X1 + [1] X2 + [5]
> [1] X1 + [1] X2 + [0]
= [n____(X1, X2)]
[nil()] = [5]
> [0]
= [n__nil()]
[U11(tt())] = [0]
>= [0]
= [tt()]
[U21(tt(), V2)] = [1] V2 + [0]
>= [1] V2 + [0]
= [U22(isList(activate(V2)))]
[U22(tt())] = [0]
>= [0]
= [tt()]
[isList(V)] = [1] V + [0]
>= [1] V + [0]
= [U11(isNeList(activate(V)))]
[isList(n__nil())] = [0]
>= [0]
= [tt()]
[isList(n____(V1, V2))] = [1] V2 + [1] V1 + [0]
>= [1] V2 + [1] V1 + [0]
= [U21(isList(activate(V1)), activate(V2))]
[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 + [5]
= [__(X1, X2)]
[activate(n__a())] = [0]
>= [0]
= [a()]
[activate(n__e())] = [0]
>= [0]
= [e()]
[activate(n__i())] = [0]
? [5]
= [i()]
[activate(n__o())] = [0]
>= [0]
= [o()]
[activate(n__u())] = [0]
>= [0]
= [u()]
[U31(tt())] = [0]
>= [0]
= [tt()]
[U41(tt(), V2)] = [1] V2 + [0]
>= [1] V2 + [0]
= [U42(isNeList(activate(V2)))]
[U42(tt())] = [0]
>= [0]
= [tt()]
[isNeList(V)] = [1] V + [0]
>= [1] V + [0]
= [U31(isQid(activate(V)))]
[isNeList(n____(V1, V2))] = [1] V2 + [1] V1 + [0]
>= [1] V2 + [1] V1 + [0]
= [U41(isList(activate(V1)), activate(V2))]
[isNeList(n____(V1, V2))] = [1] V2 + [1] V1 + [0]
>= [1] V2 + [1] V1 + [0]
= [U51(isNeList(activate(V1)), activate(V2))]
[U51(tt(), V2)] = [1] V2 + [0]
>= [1] V2 + [0]
= [U52(isList(activate(V2)))]
[U52(tt())] = [0]
>= [0]
= [tt()]
[U61(tt())] = [0]
>= [0]
= [tt()]
[U71(tt(), P)] = [1] P + [0]
>= [1] P + [0]
= [U72(isPal(activate(P)))]
[U72(tt())] = [0]
>= [0]
= [tt()]
[isPal(V)] = [1] V + [0]
>= [1] V + [0]
= [U81(isNePal(activate(V)))]
[isPal(n__nil())] = [0]
>= [0]
= [tt()]
[U81(tt())] = [0]
>= [0]
= [tt()]
[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]
= [U61(isQid(activate(V)))]
[a()] = [0]
>= [0]
= [n__a()]
[e()] = [0]
>= [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^1)).
Strict Trs:
{ U11(tt()) -> tt()
, U21(tt(), V2) -> U22(isList(activate(V2)))
, U22(tt()) -> tt()
, isList(V) -> U11(isNeList(activate(V)))
, isList(n__nil()) -> tt()
, isList(n____(V1, V2)) -> U21(isList(activate(V1)), activate(V2))
, activate(X) -> X
, activate(n__nil()) -> nil()
, activate(n____(X1, X2)) -> __(X1, X2)
, activate(n__a()) -> a()
, activate(n__e()) -> e()
, activate(n__i()) -> i()
, activate(n__o()) -> o()
, activate(n__u()) -> u()
, U31(tt()) -> tt()
, U41(tt(), V2) -> U42(isNeList(activate(V2)))
, U42(tt()) -> tt()
, isNeList(V) -> U31(isQid(activate(V)))
, isNeList(n____(V1, V2)) ->
U41(isList(activate(V1)), activate(V2))
, isNeList(n____(V1, V2)) ->
U51(isNeList(activate(V1)), activate(V2))
, U51(tt(), V2) -> U52(isList(activate(V2)))
, U52(tt()) -> tt()
, U61(tt()) -> tt()
, U72(tt()) -> tt()
, isPal(V) -> U81(isNePal(activate(V)))
, isPal(n__nil()) -> tt()
, U81(tt()) -> tt()
, isQid(n__a()) -> tt()
, isQid(n__e()) -> tt()
, isQid(n__i()) -> tt()
, isQid(n__o()) -> tt()
, isQid(n__u()) -> tt()
, isNePal(V) -> U61(isQid(activate(V)))
, a() -> n__a()
, e() -> n__e()
, o() -> n__o()
, u() -> n__u() }
Weak Trs:
{ __(X1, X2) -> n____(X1, X2)
, nil() -> n__nil()
, U71(tt(), P) -> U72(isPal(activate(P)))
, i() -> n__i() }
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(U11) = {1}, Uargs(U21) = {1, 2}, Uargs(U22) = {1},
Uargs(isList) = {1}, Uargs(U31) = {1}, Uargs(U41) = {1, 2},
Uargs(U42) = {1}, Uargs(isNeList) = {1}, Uargs(U51) = {1, 2},
Uargs(U52) = {1}, Uargs(U61) = {1}, Uargs(U72) = {1},
Uargs(isPal) = {1}, Uargs(U81) = {1}, Uargs(isQid) = {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] = [5]
[U11](x1) = [1] x1 + [0]
[tt] = [0]
[U21](x1, x2) = [1] x1 + [1] x2 + [0]
[U22](x1) = [1] x1 + [0]
[isList](x1) = [1] x1 + [0]
[activate](x1) = [1] x1 + [0]
[U31](x1) = [1] x1 + [0]
[U41](x1, x2) = [1] x1 + [1] x2 + [0]
[U42](x1) = [1] x1 + [0]
[isNeList](x1) = [1] x1 + [0]
[U51](x1, x2) = [1] x1 + [1] x2 + [0]
[U52](x1) = [1] x1 + [0]
[U61](x1) = [1] x1 + [0]
[U71](x1, x2) = [1] x2 + [0]
[U72](x1) = [1] x1 + [0]
[isPal](x1) = [1] x1 + [0]
[U81](x1) = [1] x1 + [0]
[n__nil] = [0]
[n____](x1, x2) = [1] x1 + [1] x2 + [0]
[isQid](x1) = [1] x1 + [0]
[isNePal](x1) = [1] x1 + [4]
[n__a] = [0]
[n__e] = [0]
[n__i] = [0]
[n__o] = [0]
[n__u] = [0]
[a] = [0]
[e] = [0]
[i] = [5]
[o] = [0]
[u] = [2]
The order satisfies the following ordering constraints:
[__(X1, X2)] = [1] X1 + [1] X2 + [5]
> [1] X1 + [1] X2 + [0]
= [n____(X1, X2)]
[nil()] = [5]
> [0]
= [n__nil()]
[U11(tt())] = [0]
>= [0]
= [tt()]
[U21(tt(), V2)] = [1] V2 + [0]
>= [1] V2 + [0]
= [U22(isList(activate(V2)))]
[U22(tt())] = [0]
>= [0]
= [tt()]
[isList(V)] = [1] V + [0]
>= [1] V + [0]
= [U11(isNeList(activate(V)))]
[isList(n__nil())] = [0]
>= [0]
= [tt()]
[isList(n____(V1, V2))] = [1] V2 + [1] V1 + [0]
>= [1] V2 + [1] V1 + [0]
= [U21(isList(activate(V1)), activate(V2))]
[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 + [5]
= [__(X1, X2)]
[activate(n__a())] = [0]
>= [0]
= [a()]
[activate(n__e())] = [0]
>= [0]
= [e()]
[activate(n__i())] = [0]
? [5]
= [i()]
[activate(n__o())] = [0]
>= [0]
= [o()]
[activate(n__u())] = [0]
? [2]
= [u()]
[U31(tt())] = [0]
>= [0]
= [tt()]
[U41(tt(), V2)] = [1] V2 + [0]
>= [1] V2 + [0]
= [U42(isNeList(activate(V2)))]
[U42(tt())] = [0]
>= [0]
= [tt()]
[isNeList(V)] = [1] V + [0]
>= [1] V + [0]
= [U31(isQid(activate(V)))]
[isNeList(n____(V1, V2))] = [1] V2 + [1] V1 + [0]
>= [1] V2 + [1] V1 + [0]
= [U41(isList(activate(V1)), activate(V2))]
[isNeList(n____(V1, V2))] = [1] V2 + [1] V1 + [0]
>= [1] V2 + [1] V1 + [0]
= [U51(isNeList(activate(V1)), activate(V2))]
[U51(tt(), V2)] = [1] V2 + [0]
>= [1] V2 + [0]
= [U52(isList(activate(V2)))]
[U52(tt())] = [0]
>= [0]
= [tt()]
[U61(tt())] = [0]
>= [0]
= [tt()]
[U71(tt(), P)] = [1] P + [0]
>= [1] P + [0]
= [U72(isPal(activate(P)))]
[U72(tt())] = [0]
>= [0]
= [tt()]
[isPal(V)] = [1] V + [0]
? [1] V + [4]
= [U81(isNePal(activate(V)))]
[isPal(n__nil())] = [0]
>= [0]
= [tt()]
[U81(tt())] = [0]
>= [0]
= [tt()]
[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 + [4]
> [1] V + [0]
= [U61(isQid(activate(V)))]
[a()] = [0]
>= [0]
= [n__a()]
[e()] = [0]
>= [0]
= [n__e()]
[i()] = [5]
> [0]
= [n__i()]
[o()] = [0]
>= [0]
= [n__o()]
[u()] = [2]
> [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:
{ U11(tt()) -> tt()
, U21(tt(), V2) -> U22(isList(activate(V2)))
, U22(tt()) -> tt()
, isList(V) -> U11(isNeList(activate(V)))
, isList(n__nil()) -> tt()
, isList(n____(V1, V2)) -> U21(isList(activate(V1)), activate(V2))
, activate(X) -> X
, activate(n__nil()) -> nil()
, activate(n____(X1, X2)) -> __(X1, X2)
, activate(n__a()) -> a()
, activate(n__e()) -> e()
, activate(n__i()) -> i()
, activate(n__o()) -> o()
, activate(n__u()) -> u()
, U31(tt()) -> tt()
, U41(tt(), V2) -> U42(isNeList(activate(V2)))
, U42(tt()) -> tt()
, isNeList(V) -> U31(isQid(activate(V)))
, isNeList(n____(V1, V2)) ->
U41(isList(activate(V1)), activate(V2))
, isNeList(n____(V1, V2)) ->
U51(isNeList(activate(V1)), activate(V2))
, U51(tt(), V2) -> U52(isList(activate(V2)))
, U52(tt()) -> tt()
, U61(tt()) -> tt()
, U72(tt()) -> tt()
, isPal(V) -> U81(isNePal(activate(V)))
, isPal(n__nil()) -> tt()
, U81(tt()) -> tt()
, isQid(n__a()) -> tt()
, isQid(n__e()) -> tt()
, isQid(n__i()) -> tt()
, isQid(n__o()) -> tt()
, isQid(n__u()) -> tt()
, a() -> n__a()
, e() -> n__e()
, o() -> n__o() }
Weak Trs:
{ __(X1, X2) -> n____(X1, X2)
, nil() -> n__nil()
, U71(tt(), P) -> U72(isPal(activate(P)))
, isNePal(V) -> U61(isQid(activate(V)))
, i() -> n__i()
, 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(U11) = {1}, Uargs(U21) = {1, 2}, Uargs(U22) = {1},
Uargs(isList) = {1}, Uargs(U31) = {1}, Uargs(U41) = {1, 2},
Uargs(U42) = {1}, Uargs(isNeList) = {1}, Uargs(U51) = {1, 2},
Uargs(U52) = {1}, Uargs(U61) = {1}, Uargs(U72) = {1},
Uargs(isPal) = {1}, Uargs(U81) = {1}, Uargs(isQid) = {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] = [5]
[U11](x1) = [1] x1 + [0]
[tt] = [1]
[U21](x1, x2) = [1] x1 + [1] x2 + [0]
[U22](x1) = [1] x1 + [0]
[isList](x1) = [1] x1 + [0]
[activate](x1) = [1] x1 + [0]
[U31](x1) = [1] x1 + [0]
[U41](x1, x2) = [1] x1 + [1] x2 + [0]
[U42](x1) = [1] x1 + [0]
[isNeList](x1) = [1] x1 + [0]
[U51](x1, x2) = [1] x1 + [1] x2 + [0]
[U52](x1) = [1] x1 + [0]
[U61](x1) = [1] x1 + [0]
[U71](x1, x2) = [1] x1 + [1] x2 + [7]
[U72](x1) = [1] x1 + [0]
[isPal](x1) = [1] x1 + [4]
[U81](x1) = [1] x1 + [0]
[n__nil] = [0]
[n____](x1, x2) = [1] x1 + [1] x2 + [0]
[isQid](x1) = [1] x1 + [0]
[isNePal](x1) = [1] x1 + [4]
[n__a] = [0]
[n__e] = [0]
[n__i] = [0]
[n__o] = [0]
[n__u] = [0]
[a] = [1]
[e] = [0]
[i] = [5]
[o] = [2]
[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]
> [0]
= [n__nil()]
[U11(tt())] = [1]
>= [1]
= [tt()]
[U21(tt(), V2)] = [1] V2 + [1]
> [1] V2 + [0]
= [U22(isList(activate(V2)))]
[U22(tt())] = [1]
>= [1]
= [tt()]
[isList(V)] = [1] V + [0]
>= [1] V + [0]
= [U11(isNeList(activate(V)))]
[isList(n__nil())] = [0]
? [1]
= [tt()]
[isList(n____(V1, V2))] = [1] V2 + [1] V1 + [0]
>= [1] V2 + [1] V1 + [0]
= [U21(isList(activate(V1)), activate(V2))]
[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 + [5]
= [__(X1, X2)]
[activate(n__a())] = [0]
? [1]
= [a()]
[activate(n__e())] = [0]
>= [0]
= [e()]
[activate(n__i())] = [0]
? [5]
= [i()]
[activate(n__o())] = [0]
? [2]
= [o()]
[activate(n__u())] = [0]
? [5]
= [u()]
[U31(tt())] = [1]
>= [1]
= [tt()]
[U41(tt(), V2)] = [1] V2 + [1]
> [1] V2 + [0]
= [U42(isNeList(activate(V2)))]
[U42(tt())] = [1]
>= [1]
= [tt()]
[isNeList(V)] = [1] V + [0]
>= [1] V + [0]
= [U31(isQid(activate(V)))]
[isNeList(n____(V1, V2))] = [1] V2 + [1] V1 + [0]
>= [1] V2 + [1] V1 + [0]
= [U41(isList(activate(V1)), activate(V2))]
[isNeList(n____(V1, V2))] = [1] V2 + [1] V1 + [0]
>= [1] V2 + [1] V1 + [0]
= [U51(isNeList(activate(V1)), activate(V2))]
[U51(tt(), V2)] = [1] V2 + [1]
> [1] V2 + [0]
= [U52(isList(activate(V2)))]
[U52(tt())] = [1]
>= [1]
= [tt()]
[U61(tt())] = [1]
>= [1]
= [tt()]
[U71(tt(), P)] = [1] P + [8]
> [1] P + [4]
= [U72(isPal(activate(P)))]
[U72(tt())] = [1]
>= [1]
= [tt()]
[isPal(V)] = [1] V + [4]
>= [1] V + [4]
= [U81(isNePal(activate(V)))]
[isPal(n__nil())] = [4]
> [1]
= [tt()]
[U81(tt())] = [1]
>= [1]
= [tt()]
[isQid(n__a())] = [0]
? [1]
= [tt()]
[isQid(n__e())] = [0]
? [1]
= [tt()]
[isQid(n__i())] = [0]
? [1]
= [tt()]
[isQid(n__o())] = [0]
? [1]
= [tt()]
[isQid(n__u())] = [0]
? [1]
= [tt()]
[isNePal(V)] = [1] V + [4]
> [1] V + [0]
= [U61(isQid(activate(V)))]
[a()] = [1]
> [0]
= [n__a()]
[e()] = [0]
>= [0]
= [n__e()]
[i()] = [5]
> [0]
= [n__i()]
[o()] = [2]
> [0]
= [n__o()]
[u()] = [5]
> [0]
= [n__u()]
Further, it can be verified that all rules not oriented are covered by the weightgap condition.
We are left with following problem, upon which TcT provides the
certificate YES(O(1),O(n^1)).
Strict Trs:
{ U11(tt()) -> tt()
, U22(tt()) -> tt()
, isList(V) -> U11(isNeList(activate(V)))
, isList(n__nil()) -> tt()
, isList(n____(V1, V2)) -> U21(isList(activate(V1)), activate(V2))
, activate(X) -> X
, activate(n__nil()) -> nil()
, activate(n____(X1, X2)) -> __(X1, X2)
, activate(n__a()) -> a()
, activate(n__e()) -> e()
, activate(n__i()) -> i()
, activate(n__o()) -> o()
, activate(n__u()) -> u()
, U31(tt()) -> tt()
, U42(tt()) -> tt()
, isNeList(V) -> U31(isQid(activate(V)))
, isNeList(n____(V1, V2)) ->
U41(isList(activate(V1)), activate(V2))
, isNeList(n____(V1, V2)) ->
U51(isNeList(activate(V1)), activate(V2))
, U52(tt()) -> tt()
, U61(tt()) -> tt()
, U72(tt()) -> tt()
, isPal(V) -> U81(isNePal(activate(V)))
, U81(tt()) -> tt()
, isQid(n__a()) -> tt()
, isQid(n__e()) -> tt()
, isQid(n__i()) -> tt()
, isQid(n__o()) -> tt()
, isQid(n__u()) -> tt()
, e() -> n__e() }
Weak Trs:
{ __(X1, X2) -> n____(X1, X2)
, nil() -> n__nil()
, U21(tt(), V2) -> U22(isList(activate(V2)))
, U41(tt(), V2) -> U42(isNeList(activate(V2)))
, U51(tt(), V2) -> U52(isList(activate(V2)))
, U71(tt(), P) -> U72(isPal(activate(P)))
, isPal(n__nil()) -> tt()
, isNePal(V) -> U61(isQid(activate(V)))
, a() -> n__a()
, 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(U11) = {1}, Uargs(U21) = {1, 2}, Uargs(U22) = {1},
Uargs(isList) = {1}, Uargs(U31) = {1}, Uargs(U41) = {1, 2},
Uargs(U42) = {1}, Uargs(isNeList) = {1}, Uargs(U51) = {1, 2},
Uargs(U52) = {1}, Uargs(U61) = {1}, Uargs(U72) = {1},
Uargs(isPal) = {1}, Uargs(U81) = {1}, Uargs(isQid) = {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] = [5]
[U11](x1) = [1] x1 + [0]
[tt] = [1]
[U21](x1, x2) = [1] x1 + [1] x2 + [0]
[U22](x1) = [1] x1 + [0]
[isList](x1) = [1] x1 + [0]
[activate](x1) = [1] x1 + [0]
[U31](x1) = [1] x1 + [0]
[U41](x1, x2) = [1] x1 + [1] x2 + [0]
[U42](x1) = [1] x1 + [0]
[isNeList](x1) = [1] x1 + [0]
[U51](x1, x2) = [1] x1 + [1] x2 + [0]
[U52](x1) = [1] x1 + [0]
[U61](x1) = [1] x1 + [0]
[U71](x1, x2) = [1] x1 + [1] x2 + [7]
[U72](x1) = [1] x1 + [0]
[isPal](x1) = [1] x1 + [4]
[U81](x1) = [1] x1 + [0]
[n__nil] = [0]
[n____](x1, x2) = [1] x1 + [1] x2 + [0]
[isQid](x1) = [1] x1 + [0]
[isNePal](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()] = [5]
> [0]
= [n__nil()]
[U11(tt())] = [1]
>= [1]
= [tt()]
[U21(tt(), V2)] = [1] V2 + [1]
> [1] V2 + [0]
= [U22(isList(activate(V2)))]
[U22(tt())] = [1]
>= [1]
= [tt()]
[isList(V)] = [1] V + [0]
>= [1] V + [0]
= [U11(isNeList(activate(V)))]
[isList(n__nil())] = [0]
? [1]
= [tt()]
[isList(n____(V1, V2))] = [1] V2 + [1] V1 + [0]
>= [1] V2 + [1] V1 + [0]
= [U21(isList(activate(V1)), activate(V2))]
[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 + [5]
= [__(X1, X2)]
[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()]
[U31(tt())] = [1]
>= [1]
= [tt()]
[U41(tt(), V2)] = [1] V2 + [1]
> [1] V2 + [0]
= [U42(isNeList(activate(V2)))]
[U42(tt())] = [1]
>= [1]
= [tt()]
[isNeList(V)] = [1] V + [0]
>= [1] V + [0]
= [U31(isQid(activate(V)))]
[isNeList(n____(V1, V2))] = [1] V2 + [1] V1 + [0]
>= [1] V2 + [1] V1 + [0]
= [U41(isList(activate(V1)), activate(V2))]
[isNeList(n____(V1, V2))] = [1] V2 + [1] V1 + [0]
>= [1] V2 + [1] V1 + [0]
= [U51(isNeList(activate(V1)), activate(V2))]
[U51(tt(), V2)] = [1] V2 + [1]
> [1] V2 + [0]
= [U52(isList(activate(V2)))]
[U52(tt())] = [1]
>= [1]
= [tt()]
[U61(tt())] = [1]
>= [1]
= [tt()]
[U71(tt(), P)] = [1] P + [8]
> [1] P + [4]
= [U72(isPal(activate(P)))]
[U72(tt())] = [1]
>= [1]
= [tt()]
[isPal(V)] = [1] V + [4]
>= [1] V + [4]
= [U81(isNePal(activate(V)))]
[isPal(n__nil())] = [4]
> [1]
= [tt()]
[U81(tt())] = [1]
>= [1]
= [tt()]
[isQid(n__a())] = [0]
? [1]
= [tt()]
[isQid(n__e())] = [0]
? [1]
= [tt()]
[isQid(n__i())] = [0]
? [1]
= [tt()]
[isQid(n__o())] = [0]
? [1]
= [tt()]
[isQid(n__u())] = [0]
? [1]
= [tt()]
[isNePal(V)] = [1] V + [4]
> [1] V + [0]
= [U61(isQid(activate(V)))]
[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:
{ U11(tt()) -> tt()
, U22(tt()) -> tt()
, isList(V) -> U11(isNeList(activate(V)))
, isList(n__nil()) -> tt()
, isList(n____(V1, V2)) -> U21(isList(activate(V1)), activate(V2))
, activate(X) -> X
, activate(n__nil()) -> nil()
, activate(n____(X1, X2)) -> __(X1, X2)
, activate(n__a()) -> a()
, activate(n__e()) -> e()
, activate(n__i()) -> i()
, activate(n__o()) -> o()
, activate(n__u()) -> u()
, U31(tt()) -> tt()
, U42(tt()) -> tt()
, isNeList(V) -> U31(isQid(activate(V)))
, isNeList(n____(V1, V2)) ->
U41(isList(activate(V1)), activate(V2))
, isNeList(n____(V1, V2)) ->
U51(isNeList(activate(V1)), activate(V2))
, U52(tt()) -> tt()
, U61(tt()) -> tt()
, U72(tt()) -> tt()
, isPal(V) -> U81(isNePal(activate(V)))
, U81(tt()) -> tt()
, 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)
, nil() -> n__nil()
, U21(tt(), V2) -> U22(isList(activate(V2)))
, U41(tt(), V2) -> U42(isNeList(activate(V2)))
, U51(tt(), V2) -> U52(isList(activate(V2)))
, U71(tt(), P) -> U72(isPal(activate(P)))
, isPal(n__nil()) -> tt()
, isNePal(V) -> U61(isQid(activate(V)))
, 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(U11) = {1}, Uargs(U21) = {1, 2}, Uargs(U22) = {1},
Uargs(isList) = {1}, Uargs(U31) = {1}, Uargs(U41) = {1, 2},
Uargs(U42) = {1}, Uargs(isNeList) = {1}, Uargs(U51) = {1, 2},
Uargs(U52) = {1}, Uargs(U61) = {1}, Uargs(U72) = {1},
Uargs(isPal) = {1}, Uargs(U81) = {1}, Uargs(isQid) = {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] = [5]
[U11](x1) = [1] x1 + [0]
[tt] = [0]
[U21](x1, x2) = [1] x1 + [1] x2 + [0]
[U22](x1) = [1] x1 + [0]
[isList](x1) = [1] x1 + [0]
[activate](x1) = [1] x1 + [0]
[U31](x1) = [1] x1 + [0]
[U41](x1, x2) = [1] x1 + [1] x2 + [0]
[U42](x1) = [1] x1 + [0]
[isNeList](x1) = [1] x1 + [0]
[U51](x1, x2) = [1] x1 + [1] x2 + [0]
[U52](x1) = [1] x1 + [0]
[U61](x1) = [1] x1 + [0]
[U71](x1, x2) = [1] x2 + [1]
[U72](x1) = [1] x1 + [0]
[isPal](x1) = [1] x1 + [1]
[U81](x1) = [1] x1 + [0]
[n__nil] = [0]
[n____](x1, x2) = [1] x1 + [1] x2 + [1]
[isQid](x1) = [1] x1 + [0]
[isNePal](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 + [1]
= [n____(X1, X2)]
[nil()] = [5]
> [0]
= [n__nil()]
[U11(tt())] = [0]
>= [0]
= [tt()]
[U21(tt(), V2)] = [1] V2 + [0]
>= [1] V2 + [0]
= [U22(isList(activate(V2)))]
[U22(tt())] = [0]
>= [0]
= [tt()]
[isList(V)] = [1] V + [0]
>= [1] V + [0]
= [U11(isNeList(activate(V)))]
[isList(n__nil())] = [0]
>= [0]
= [tt()]
[isList(n____(V1, V2))] = [1] V2 + [1] V1 + [1]
> [1] V2 + [1] V1 + [0]
= [U21(isList(activate(V1)), activate(V2))]
[activate(X)] = [1] X + [0]
>= [1] X + [0]
= [X]
[activate(n__nil())] = [0]
? [5]
= [nil()]
[activate(n____(X1, X2))] = [1] X1 + [1] X2 + [1]
? [1] X1 + [1] X2 + [5]
= [__(X1, X2)]
[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()]
[U31(tt())] = [0]
>= [0]
= [tt()]
[U41(tt(), V2)] = [1] V2 + [0]
>= [1] V2 + [0]
= [U42(isNeList(activate(V2)))]
[U42(tt())] = [0]
>= [0]
= [tt()]
[isNeList(V)] = [1] V + [0]
>= [1] V + [0]
= [U31(isQid(activate(V)))]
[isNeList(n____(V1, V2))] = [1] V2 + [1] V1 + [1]
> [1] V2 + [1] V1 + [0]
= [U41(isList(activate(V1)), activate(V2))]
[isNeList(n____(V1, V2))] = [1] V2 + [1] V1 + [1]
> [1] V2 + [1] V1 + [0]
= [U51(isNeList(activate(V1)), activate(V2))]
[U51(tt(), V2)] = [1] V2 + [0]
>= [1] V2 + [0]
= [U52(isList(activate(V2)))]
[U52(tt())] = [0]
>= [0]
= [tt()]
[U61(tt())] = [0]
>= [0]
= [tt()]
[U71(tt(), P)] = [1] P + [1]
>= [1] P + [1]
= [U72(isPal(activate(P)))]
[U72(tt())] = [0]
>= [0]
= [tt()]
[isPal(V)] = [1] V + [1]
> [1] V + [0]
= [U81(isNePal(activate(V)))]
[isPal(n__nil())] = [1]
> [0]
= [tt()]
[U81(tt())] = [0]
>= [0]
= [tt()]
[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]
= [U61(isQid(activate(V)))]
[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:
{ U11(tt()) -> tt()
, U22(tt()) -> tt()
, isList(V) -> U11(isNeList(activate(V)))
, isList(n__nil()) -> tt()
, activate(X) -> X
, activate(n__nil()) -> nil()
, activate(n____(X1, X2)) -> __(X1, X2)
, activate(n__a()) -> a()
, activate(n__e()) -> e()
, activate(n__i()) -> i()
, activate(n__o()) -> o()
, activate(n__u()) -> u()
, U31(tt()) -> tt()
, U42(tt()) -> tt()
, isNeList(V) -> U31(isQid(activate(V)))
, U52(tt()) -> tt()
, U61(tt()) -> tt()
, U72(tt()) -> tt()
, U81(tt()) -> tt()
, 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)
, nil() -> n__nil()
, U21(tt(), V2) -> U22(isList(activate(V2)))
, isList(n____(V1, V2)) -> U21(isList(activate(V1)), activate(V2))
, U41(tt(), V2) -> U42(isNeList(activate(V2)))
, isNeList(n____(V1, V2)) ->
U41(isList(activate(V1)), activate(V2))
, isNeList(n____(V1, V2)) ->
U51(isNeList(activate(V1)), activate(V2))
, U51(tt(), V2) -> U52(isList(activate(V2)))
, U71(tt(), P) -> U72(isPal(activate(P)))
, isPal(V) -> U81(isNePal(activate(V)))
, isPal(n__nil()) -> tt()
, isNePal(V) -> U61(isQid(activate(V)))
, 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(U11) = {1}, Uargs(U21) = {1, 2}, Uargs(U22) = {1},
Uargs(isList) = {1}, Uargs(U31) = {1}, Uargs(U41) = {1, 2},
Uargs(U42) = {1}, Uargs(isNeList) = {1}, Uargs(U51) = {1, 2},
Uargs(U52) = {1}, Uargs(U61) = {1}, Uargs(U72) = {1},
Uargs(isPal) = {1}, Uargs(U81) = {1}, Uargs(isQid) = {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] = [5]
[U11](x1) = [1] x1 + [0]
[tt] = [1]
[U21](x1, x2) = [1] x1 + [1] x2 + [0]
[U22](x1) = [1] x1 + [0]
[isList](x1) = [1] x1 + [1]
[activate](x1) = [1] x1 + [0]
[U31](x1) = [1] x1 + [0]
[U41](x1, x2) = [1] x1 + [1] x2 + [0]
[U42](x1) = [1] x1 + [0]
[isNeList](x1) = [1] x1 + [1]
[U51](x1, x2) = [1] x1 + [1] x2 + [0]
[U52](x1) = [1] x1 + [0]
[U61](x1) = [1] x1 + [0]
[U71](x1, x2) = [1] x1 + [1] x2 + [7]
[U72](x1) = [1] x1 + [0]
[isPal](x1) = [1] x1 + [4]
[U81](x1) = [1] x1 + [0]
[n__nil] = [0]
[n____](x1, x2) = [1] x1 + [1] x2 + [0]
[isQid](x1) = [1] x1 + [0]
[isNePal](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 + [1]
> [1] X1 + [1] X2 + [0]
= [n____(X1, X2)]
[nil()] = [5]
> [0]
= [n__nil()]
[U11(tt())] = [1]
>= [1]
= [tt()]
[U21(tt(), V2)] = [1] V2 + [1]
>= [1] V2 + [1]
= [U22(isList(activate(V2)))]
[U22(tt())] = [1]
>= [1]
= [tt()]
[isList(V)] = [1] V + [1]
>= [1] V + [1]
= [U11(isNeList(activate(V)))]
[isList(n__nil())] = [1]
>= [1]
= [tt()]
[isList(n____(V1, V2))] = [1] V2 + [1] V1 + [1]
>= [1] V2 + [1] V1 + [1]
= [U21(isList(activate(V1)), activate(V2))]
[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 + [1]
= [__(X1, X2)]
[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()]
[U31(tt())] = [1]
>= [1]
= [tt()]
[U41(tt(), V2)] = [1] V2 + [1]
>= [1] V2 + [1]
= [U42(isNeList(activate(V2)))]
[U42(tt())] = [1]
>= [1]
= [tt()]
[isNeList(V)] = [1] V + [1]
> [1] V + [0]
= [U31(isQid(activate(V)))]
[isNeList(n____(V1, V2))] = [1] V2 + [1] V1 + [1]
>= [1] V2 + [1] V1 + [1]
= [U41(isList(activate(V1)), activate(V2))]
[isNeList(n____(V1, V2))] = [1] V2 + [1] V1 + [1]
>= [1] V2 + [1] V1 + [1]
= [U51(isNeList(activate(V1)), activate(V2))]
[U51(tt(), V2)] = [1] V2 + [1]
>= [1] V2 + [1]
= [U52(isList(activate(V2)))]
[U52(tt())] = [1]
>= [1]
= [tt()]
[U61(tt())] = [1]
>= [1]
= [tt()]
[U71(tt(), P)] = [1] P + [8]
> [1] P + [4]
= [U72(isPal(activate(P)))]
[U72(tt())] = [1]
>= [1]
= [tt()]
[isPal(V)] = [1] V + [4]
>= [1] V + [4]
= [U81(isNePal(activate(V)))]
[isPal(n__nil())] = [4]
> [1]
= [tt()]
[U81(tt())] = [1]
>= [1]
= [tt()]
[isQid(n__a())] = [0]
? [1]
= [tt()]
[isQid(n__e())] = [0]
? [1]
= [tt()]
[isQid(n__i())] = [0]
? [1]
= [tt()]
[isQid(n__o())] = [0]
? [1]
= [tt()]
[isQid(n__u())] = [0]
? [1]
= [tt()]
[isNePal(V)] = [1] V + [4]
> [1] V + [0]
= [U61(isQid(activate(V)))]
[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:
{ U11(tt()) -> tt()
, U22(tt()) -> tt()
, isList(V) -> U11(isNeList(activate(V)))
, isList(n__nil()) -> tt()
, activate(X) -> X
, activate(n__nil()) -> nil()
, activate(n____(X1, X2)) -> __(X1, X2)
, activate(n__a()) -> a()
, activate(n__e()) -> e()
, activate(n__i()) -> i()
, activate(n__o()) -> o()
, activate(n__u()) -> u()
, U31(tt()) -> tt()
, U42(tt()) -> tt()
, U52(tt()) -> tt()
, U61(tt()) -> tt()
, U72(tt()) -> tt()
, U81(tt()) -> tt()
, 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)
, nil() -> n__nil()
, U21(tt(), V2) -> U22(isList(activate(V2)))
, isList(n____(V1, V2)) -> U21(isList(activate(V1)), activate(V2))
, U41(tt(), V2) -> U42(isNeList(activate(V2)))
, isNeList(V) -> U31(isQid(activate(V)))
, isNeList(n____(V1, V2)) ->
U41(isList(activate(V1)), activate(V2))
, isNeList(n____(V1, V2)) ->
U51(isNeList(activate(V1)), activate(V2))
, U51(tt(), V2) -> U52(isList(activate(V2)))
, U71(tt(), P) -> U72(isPal(activate(P)))
, isPal(V) -> U81(isNePal(activate(V)))
, isPal(n__nil()) -> tt()
, isNePal(V) -> U61(isQid(activate(V)))
, 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(U11) = {1}, Uargs(U21) = {1, 2}, Uargs(U22) = {1},
Uargs(isList) = {1}, Uargs(U31) = {1}, Uargs(U41) = {1, 2},
Uargs(U42) = {1}, Uargs(isNeList) = {1}, Uargs(U51) = {1, 2},
Uargs(U52) = {1}, Uargs(U61) = {1}, Uargs(U72) = {1},
Uargs(isPal) = {1}, Uargs(U81) = {1}, Uargs(isQid) = {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] = [1]
[U11](x1) = [1] x1 + [0]
[tt] = [0]
[U21](x1, x2) = [1] x1 + [1] x2 + [0]
[U22](x1) = [1] x1 + [0]
[isList](x1) = [1] x1 + [0]
[activate](x1) = [1] x1 + [0]
[U31](x1) = [1] x1 + [0]
[U41](x1, x2) = [1] x1 + [1] x2 + [0]
[U42](x1) = [1] x1 + [0]
[isNeList](x1) = [1] x1 + [0]
[U51](x1, x2) = [1] x1 + [1] x2 + [0]
[U52](x1) = [1] x1 + [0]
[U61](x1) = [1] x1 + [0]
[U71](x1, x2) = [1] x2 + [5]
[U72](x1) = [1] x1 + [0]
[isPal](x1) = [1] x1 + [1]
[U81](x1) = [1] x1 + [0]
[n__nil] = [0]
[n____](x1, x2) = [1] x1 + [1] x2 + [0]
[isQid](x1) = [1] x1 + [0]
[isNePal](x1) = [1] x1 + [0]
[n__a] = [0]
[n__e] = [0]
[n__i] = [1]
[n__o] = [0]
[n__u] = [1]
[a] = [1]
[e] = [1]
[i] = [2]
[o] = [1]
[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()] = [1]
> [0]
= [n__nil()]
[U11(tt())] = [0]
>= [0]
= [tt()]
[U21(tt(), V2)] = [1] V2 + [0]
>= [1] V2 + [0]
= [U22(isList(activate(V2)))]
[U22(tt())] = [0]
>= [0]
= [tt()]
[isList(V)] = [1] V + [0]
>= [1] V + [0]
= [U11(isNeList(activate(V)))]
[isList(n__nil())] = [0]
>= [0]
= [tt()]
[isList(n____(V1, V2))] = [1] V2 + [1] V1 + [0]
>= [1] V2 + [1] V1 + [0]
= [U21(isList(activate(V1)), activate(V2))]
[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 + [1]
= [__(X1, X2)]
[activate(n__a())] = [0]
? [1]
= [a()]
[activate(n__e())] = [0]
? [1]
= [e()]
[activate(n__i())] = [1]
? [2]
= [i()]
[activate(n__o())] = [0]
? [1]
= [o()]
[activate(n__u())] = [1]
? [5]
= [u()]
[U31(tt())] = [0]
>= [0]
= [tt()]
[U41(tt(), V2)] = [1] V2 + [0]
>= [1] V2 + [0]
= [U42(isNeList(activate(V2)))]
[U42(tt())] = [0]
>= [0]
= [tt()]
[isNeList(V)] = [1] V + [0]
>= [1] V + [0]
= [U31(isQid(activate(V)))]
[isNeList(n____(V1, V2))] = [1] V2 + [1] V1 + [0]
>= [1] V2 + [1] V1 + [0]
= [U41(isList(activate(V1)), activate(V2))]
[isNeList(n____(V1, V2))] = [1] V2 + [1] V1 + [0]
>= [1] V2 + [1] V1 + [0]
= [U51(isNeList(activate(V1)), activate(V2))]
[U51(tt(), V2)] = [1] V2 + [0]
>= [1] V2 + [0]
= [U52(isList(activate(V2)))]
[U52(tt())] = [0]
>= [0]
= [tt()]
[U61(tt())] = [0]
>= [0]
= [tt()]
[U71(tt(), P)] = [1] P + [5]
> [1] P + [1]
= [U72(isPal(activate(P)))]
[U72(tt())] = [0]
>= [0]
= [tt()]
[isPal(V)] = [1] V + [1]
> [1] V + [0]
= [U81(isNePal(activate(V)))]
[isPal(n__nil())] = [1]
> [0]
= [tt()]
[U81(tt())] = [0]
>= [0]
= [tt()]
[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())] = [1]
> [0]
= [tt()]
[isNePal(V)] = [1] V + [0]
>= [1] V + [0]
= [U61(isQid(activate(V)))]
[a()] = [1]
> [0]
= [n__a()]
[e()] = [1]
> [0]
= [n__e()]
[i()] = [2]
> [1]
= [n__i()]
[o()] = [1]
> [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:
{ U11(tt()) -> tt()
, U22(tt()) -> tt()
, isList(V) -> U11(isNeList(activate(V)))
, isList(n__nil()) -> tt()
, activate(X) -> X
, activate(n__nil()) -> nil()
, activate(n____(X1, X2)) -> __(X1, X2)
, activate(n__a()) -> a()
, activate(n__e()) -> e()
, activate(n__i()) -> i()
, activate(n__o()) -> o()
, activate(n__u()) -> u()
, U31(tt()) -> tt()
, U42(tt()) -> tt()
, U52(tt()) -> tt()
, U61(tt()) -> tt()
, U72(tt()) -> tt()
, U81(tt()) -> tt()
, isQid(n__a()) -> tt()
, isQid(n__e()) -> tt()
, isQid(n__o()) -> tt() }
Weak Trs:
{ __(X1, X2) -> n____(X1, X2)
, nil() -> n__nil()
, U21(tt(), V2) -> U22(isList(activate(V2)))
, isList(n____(V1, V2)) -> U21(isList(activate(V1)), activate(V2))
, U41(tt(), V2) -> U42(isNeList(activate(V2)))
, isNeList(V) -> U31(isQid(activate(V)))
, isNeList(n____(V1, V2)) ->
U41(isList(activate(V1)), activate(V2))
, isNeList(n____(V1, V2)) ->
U51(isNeList(activate(V1)), activate(V2))
, U51(tt(), V2) -> U52(isList(activate(V2)))
, U71(tt(), P) -> U72(isPal(activate(P)))
, isPal(V) -> U81(isNePal(activate(V)))
, isPal(n__nil()) -> tt()
, isQid(n__i()) -> tt()
, isQid(n__u()) -> tt()
, isNePal(V) -> U61(isQid(activate(V)))
, 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(U11) = {1}, Uargs(U21) = {1, 2}, Uargs(U22) = {1},
Uargs(isList) = {1}, Uargs(U31) = {1}, Uargs(U41) = {1, 2},
Uargs(U42) = {1}, Uargs(isNeList) = {1}, Uargs(U51) = {1, 2},
Uargs(U52) = {1}, Uargs(U61) = {1}, Uargs(U72) = {1},
Uargs(isPal) = {1}, Uargs(U81) = {1}, Uargs(isQid) = {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] = [1]
[U11](x1) = [1] x1 + [0]
[tt] = [0]
[U21](x1, x2) = [1] x1 + [1] x2 + [0]
[U22](x1) = [1] x1 + [0]
[isList](x1) = [1] x1 + [0]
[activate](x1) = [1] x1 + [0]
[U31](x1) = [1] x1 + [0]
[U41](x1, x2) = [1] x1 + [1] x2 + [0]
[U42](x1) = [1] x1 + [0]
[isNeList](x1) = [1] x1 + [0]
[U51](x1, x2) = [1] x1 + [1] x2 + [0]
[U52](x1) = [1] x1 + [0]
[U61](x1) = [1] x1 + [0]
[U71](x1, x2) = [1] x2 + [1]
[U72](x1) = [1] x1 + [0]
[isPal](x1) = [1] x1 + [1]
[U81](x1) = [1] x1 + [0]
[n__nil] = [0]
[n____](x1, x2) = [1] x1 + [1] x2 + [0]
[isQid](x1) = [1] x1 + [0]
[isNePal](x1) = [1] x1 + [0]
[n__a] = [0]
[n__e] = [0]
[n__i] = [0]
[n__o] = [1]
[n__u] = [0]
[a] = [5]
[e] = [5]
[i] = [5]
[o] = [5]
[u] = [5]
The order satisfies the following ordering constraints:
[__(X1, X2)] = [1] X1 + [1] X2 + [5]
> [1] X1 + [1] X2 + [0]
= [n____(X1, X2)]
[nil()] = [1]
> [0]
= [n__nil()]
[U11(tt())] = [0]
>= [0]
= [tt()]
[U21(tt(), V2)] = [1] V2 + [0]
>= [1] V2 + [0]
= [U22(isList(activate(V2)))]
[U22(tt())] = [0]
>= [0]
= [tt()]
[isList(V)] = [1] V + [0]
>= [1] V + [0]
= [U11(isNeList(activate(V)))]
[isList(n__nil())] = [0]
>= [0]
= [tt()]
[isList(n____(V1, V2))] = [1] V2 + [1] V1 + [0]
>= [1] V2 + [1] V1 + [0]
= [U21(isList(activate(V1)), activate(V2))]
[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 + [5]
= [__(X1, X2)]
[activate(n__a())] = [0]
? [5]
= [a()]
[activate(n__e())] = [0]
? [5]
= [e()]
[activate(n__i())] = [0]
? [5]
= [i()]
[activate(n__o())] = [1]
? [5]
= [o()]
[activate(n__u())] = [0]
? [5]
= [u()]
[U31(tt())] = [0]
>= [0]
= [tt()]
[U41(tt(), V2)] = [1] V2 + [0]
>= [1] V2 + [0]
= [U42(isNeList(activate(V2)))]
[U42(tt())] = [0]
>= [0]
= [tt()]
[isNeList(V)] = [1] V + [0]
>= [1] V + [0]
= [U31(isQid(activate(V)))]
[isNeList(n____(V1, V2))] = [1] V2 + [1] V1 + [0]
>= [1] V2 + [1] V1 + [0]
= [U41(isList(activate(V1)), activate(V2))]
[isNeList(n____(V1, V2))] = [1] V2 + [1] V1 + [0]
>= [1] V2 + [1] V1 + [0]
= [U51(isNeList(activate(V1)), activate(V2))]
[U51(tt(), V2)] = [1] V2 + [0]
>= [1] V2 + [0]
= [U52(isList(activate(V2)))]
[U52(tt())] = [0]
>= [0]
= [tt()]
[U61(tt())] = [0]
>= [0]
= [tt()]
[U71(tt(), P)] = [1] P + [1]
>= [1] P + [1]
= [U72(isPal(activate(P)))]
[U72(tt())] = [0]
>= [0]
= [tt()]
[isPal(V)] = [1] V + [1]
> [1] V + [0]
= [U81(isNePal(activate(V)))]
[isPal(n__nil())] = [1]
> [0]
= [tt()]
[U81(tt())] = [0]
>= [0]
= [tt()]
[isQid(n__a())] = [0]
>= [0]
= [tt()]
[isQid(n__e())] = [0]
>= [0]
= [tt()]
[isQid(n__i())] = [0]
>= [0]
= [tt()]
[isQid(n__o())] = [1]
> [0]
= [tt()]
[isQid(n__u())] = [0]
>= [0]
= [tt()]
[isNePal(V)] = [1] V + [0]
>= [1] V + [0]
= [U61(isQid(activate(V)))]
[a()] = [5]
> [0]
= [n__a()]
[e()] = [5]
> [0]
= [n__e()]
[i()] = [5]
> [0]
= [n__i()]
[o()] = [5]
> [1]
= [n__o()]
[u()] = [5]
> [0]
= [n__u()]
Further, it can be verified that all rules not oriented are covered by the weightgap condition.
We are left with following problem, upon which TcT provides the
certificate YES(O(1),O(n^1)).
Strict Trs:
{ U11(tt()) -> tt()
, U22(tt()) -> tt()
, isList(V) -> U11(isNeList(activate(V)))
, isList(n__nil()) -> tt()
, activate(X) -> X
, activate(n__nil()) -> nil()
, activate(n____(X1, X2)) -> __(X1, X2)
, activate(n__a()) -> a()
, activate(n__e()) -> e()
, activate(n__i()) -> i()
, activate(n__o()) -> o()
, activate(n__u()) -> u()
, U31(tt()) -> tt()
, U42(tt()) -> tt()
, U52(tt()) -> tt()
, U61(tt()) -> tt()
, U72(tt()) -> tt()
, U81(tt()) -> tt()
, isQid(n__a()) -> tt()
, isQid(n__e()) -> tt() }
Weak Trs:
{ __(X1, X2) -> n____(X1, X2)
, nil() -> n__nil()
, U21(tt(), V2) -> U22(isList(activate(V2)))
, isList(n____(V1, V2)) -> U21(isList(activate(V1)), activate(V2))
, U41(tt(), V2) -> U42(isNeList(activate(V2)))
, isNeList(V) -> U31(isQid(activate(V)))
, isNeList(n____(V1, V2)) ->
U41(isList(activate(V1)), activate(V2))
, isNeList(n____(V1, V2)) ->
U51(isNeList(activate(V1)), activate(V2))
, U51(tt(), V2) -> U52(isList(activate(V2)))
, U71(tt(), P) -> U72(isPal(activate(P)))
, isPal(V) -> U81(isNePal(activate(V)))
, isPal(n__nil()) -> tt()
, isQid(n__i()) -> tt()
, isQid(n__o()) -> tt()
, isQid(n__u()) -> tt()
, isNePal(V) -> U61(isQid(activate(V)))
, 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(U11) = {1}, Uargs(U21) = {1, 2}, Uargs(U22) = {1},
Uargs(isList) = {1}, Uargs(U31) = {1}, Uargs(U41) = {1, 2},
Uargs(U42) = {1}, Uargs(isNeList) = {1}, Uargs(U51) = {1, 2},
Uargs(U52) = {1}, Uargs(U61) = {1}, Uargs(U72) = {1},
Uargs(isPal) = {1}, Uargs(U81) = {1}, Uargs(isQid) = {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] = [1]
[U11](x1) = [1] x1 + [0]
[tt] = [0]
[U21](x1, x2) = [1] x1 + [1] x2 + [0]
[U22](x1) = [1] x1 + [0]
[isList](x1) = [1] x1 + [0]
[activate](x1) = [1] x1 + [0]
[U31](x1) = [1] x1 + [0]
[U41](x1, x2) = [1] x1 + [1] x2 + [0]
[U42](x1) = [1] x1 + [0]
[isNeList](x1) = [1] x1 + [0]
[U51](x1, x2) = [1] x1 + [1] x2 + [0]
[U52](x1) = [1] x1 + [0]
[U61](x1) = [1] x1 + [0]
[U71](x1, x2) = [1] x2 + [4]
[U72](x1) = [1] x1 + [0]
[isPal](x1) = [1] x1 + [1]
[U81](x1) = [1] x1 + [0]
[n__nil] = [0]
[n____](x1, x2) = [1] x1 + [1] x2 + [0]
[isQid](x1) = [1] x1 + [0]
[isNePal](x1) = [1] x1 + [0]
[n__a] = [1]
[n__e] = [0]
[n__i] = [1]
[n__o] = [1]
[n__u] = [1]
[a] = [1]
[e] = [1]
[i] = [2]
[o] = [4]
[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()] = [1]
> [0]
= [n__nil()]
[U11(tt())] = [0]
>= [0]
= [tt()]
[U21(tt(), V2)] = [1] V2 + [0]
>= [1] V2 + [0]
= [U22(isList(activate(V2)))]
[U22(tt())] = [0]
>= [0]
= [tt()]
[isList(V)] = [1] V + [0]
>= [1] V + [0]
= [U11(isNeList(activate(V)))]
[isList(n__nil())] = [0]
>= [0]
= [tt()]
[isList(n____(V1, V2))] = [1] V2 + [1] V1 + [0]
>= [1] V2 + [1] V1 + [0]
= [U21(isList(activate(V1)), activate(V2))]
[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 + [5]
= [__(X1, X2)]
[activate(n__a())] = [1]
>= [1]
= [a()]
[activate(n__e())] = [0]
? [1]
= [e()]
[activate(n__i())] = [1]
? [2]
= [i()]
[activate(n__o())] = [1]
? [4]
= [o()]
[activate(n__u())] = [1]
? [5]
= [u()]
[U31(tt())] = [0]
>= [0]
= [tt()]
[U41(tt(), V2)] = [1] V2 + [0]
>= [1] V2 + [0]
= [U42(isNeList(activate(V2)))]
[U42(tt())] = [0]
>= [0]
= [tt()]
[isNeList(V)] = [1] V + [0]
>= [1] V + [0]
= [U31(isQid(activate(V)))]
[isNeList(n____(V1, V2))] = [1] V2 + [1] V1 + [0]
>= [1] V2 + [1] V1 + [0]
= [U41(isList(activate(V1)), activate(V2))]
[isNeList(n____(V1, V2))] = [1] V2 + [1] V1 + [0]
>= [1] V2 + [1] V1 + [0]
= [U51(isNeList(activate(V1)), activate(V2))]
[U51(tt(), V2)] = [1] V2 + [0]
>= [1] V2 + [0]
= [U52(isList(activate(V2)))]
[U52(tt())] = [0]
>= [0]
= [tt()]
[U61(tt())] = [0]
>= [0]
= [tt()]
[U71(tt(), P)] = [1] P + [4]
> [1] P + [1]
= [U72(isPal(activate(P)))]
[U72(tt())] = [0]
>= [0]
= [tt()]
[isPal(V)] = [1] V + [1]
> [1] V + [0]
= [U81(isNePal(activate(V)))]
[isPal(n__nil())] = [1]
> [0]
= [tt()]
[U81(tt())] = [0]
>= [0]
= [tt()]
[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())] = [1]
> [0]
= [tt()]
[isNePal(V)] = [1] V + [0]
>= [1] V + [0]
= [U61(isQid(activate(V)))]
[a()] = [1]
>= [1]
= [n__a()]
[e()] = [1]
> [0]
= [n__e()]
[i()] = [2]
> [1]
= [n__i()]
[o()] = [4]
> [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^1)).
Strict Trs:
{ U11(tt()) -> tt()
, U22(tt()) -> tt()
, isList(V) -> U11(isNeList(activate(V)))
, isList(n__nil()) -> tt()
, activate(X) -> X
, activate(n__nil()) -> nil()
, activate(n____(X1, X2)) -> __(X1, X2)
, activate(n__a()) -> a()
, activate(n__e()) -> e()
, activate(n__i()) -> i()
, activate(n__o()) -> o()
, activate(n__u()) -> u()
, U31(tt()) -> tt()
, U42(tt()) -> tt()
, U52(tt()) -> tt()
, U61(tt()) -> tt()
, U72(tt()) -> tt()
, U81(tt()) -> tt()
, isQid(n__e()) -> tt() }
Weak Trs:
{ __(X1, X2) -> n____(X1, X2)
, nil() -> n__nil()
, U21(tt(), V2) -> U22(isList(activate(V2)))
, isList(n____(V1, V2)) -> U21(isList(activate(V1)), activate(V2))
, U41(tt(), V2) -> U42(isNeList(activate(V2)))
, isNeList(V) -> U31(isQid(activate(V)))
, isNeList(n____(V1, V2)) ->
U41(isList(activate(V1)), activate(V2))
, isNeList(n____(V1, V2)) ->
U51(isNeList(activate(V1)), activate(V2))
, U51(tt(), V2) -> U52(isList(activate(V2)))
, U71(tt(), P) -> U72(isPal(activate(P)))
, isPal(V) -> U81(isNePal(activate(V)))
, isPal(n__nil()) -> tt()
, isQid(n__a()) -> tt()
, isQid(n__i()) -> tt()
, isQid(n__o()) -> tt()
, isQid(n__u()) -> tt()
, isNePal(V) -> U61(isQid(activate(V)))
, 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(U11) = {1}, Uargs(U21) = {1, 2}, Uargs(U22) = {1},
Uargs(isList) = {1}, Uargs(U31) = {1}, Uargs(U41) = {1, 2},
Uargs(U42) = {1}, Uargs(isNeList) = {1}, Uargs(U51) = {1, 2},
Uargs(U52) = {1}, Uargs(U61) = {1}, Uargs(U72) = {1},
Uargs(isPal) = {1}, Uargs(U81) = {1}, Uargs(isQid) = {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] = [1]
[U11](x1) = [1] x1 + [0]
[tt] = [0]
[U21](x1, x2) = [1] x1 + [1] x2 + [0]
[U22](x1) = [1] x1 + [0]
[isList](x1) = [1] x1 + [0]
[activate](x1) = [1] x1 + [0]
[U31](x1) = [1] x1 + [0]
[U41](x1, x2) = [1] x1 + [1] x2 + [0]
[U42](x1) = [1] x1 + [0]
[isNeList](x1) = [1] x1 + [0]
[U51](x1, x2) = [1] x1 + [1] x2 + [0]
[U52](x1) = [1] x1 + [0]
[U61](x1) = [1] x1 + [0]
[U71](x1, x2) = [1] x2 + [5]
[U72](x1) = [1] x1 + [0]
[isPal](x1) = [1] x1 + [0]
[U81](x1) = [1] x1 + [0]
[n__nil] = [1]
[n____](x1, x2) = [1] x1 + [1] x2 + [0]
[isQid](x1) = [1] x1 + [0]
[isNePal](x1) = [1] x1 + [0]
[n__a] = [1]
[n__e] = [0]
[n__i] = [1]
[n__o] = [1]
[n__u] = [1]
[a] = [2]
[e] = [1]
[i] = [4]
[o] = [4]
[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()] = [1]
>= [1]
= [n__nil()]
[U11(tt())] = [0]
>= [0]
= [tt()]
[U21(tt(), V2)] = [1] V2 + [0]
>= [1] V2 + [0]
= [U22(isList(activate(V2)))]
[U22(tt())] = [0]
>= [0]
= [tt()]
[isList(V)] = [1] V + [0]
>= [1] V + [0]
= [U11(isNeList(activate(V)))]
[isList(n__nil())] = [1]
> [0]
= [tt()]
[isList(n____(V1, V2))] = [1] V2 + [1] V1 + [0]
>= [1] V2 + [1] V1 + [0]
= [U21(isList(activate(V1)), activate(V2))]
[activate(X)] = [1] X + [0]
>= [1] X + [0]
= [X]
[activate(n__nil())] = [1]
>= [1]
= [nil()]
[activate(n____(X1, X2))] = [1] X1 + [1] X2 + [0]
? [1] X1 + [1] X2 + [5]
= [__(X1, X2)]
[activate(n__a())] = [1]
? [2]
= [a()]
[activate(n__e())] = [0]
? [1]
= [e()]
[activate(n__i())] = [1]
? [4]
= [i()]
[activate(n__o())] = [1]
? [4]
= [o()]
[activate(n__u())] = [1]
? [5]
= [u()]
[U31(tt())] = [0]
>= [0]
= [tt()]
[U41(tt(), V2)] = [1] V2 + [0]
>= [1] V2 + [0]
= [U42(isNeList(activate(V2)))]
[U42(tt())] = [0]
>= [0]
= [tt()]
[isNeList(V)] = [1] V + [0]
>= [1] V + [0]
= [U31(isQid(activate(V)))]
[isNeList(n____(V1, V2))] = [1] V2 + [1] V1 + [0]
>= [1] V2 + [1] V1 + [0]
= [U41(isList(activate(V1)), activate(V2))]
[isNeList(n____(V1, V2))] = [1] V2 + [1] V1 + [0]
>= [1] V2 + [1] V1 + [0]
= [U51(isNeList(activate(V1)), activate(V2))]
[U51(tt(), V2)] = [1] V2 + [0]
>= [1] V2 + [0]
= [U52(isList(activate(V2)))]
[U52(tt())] = [0]
>= [0]
= [tt()]
[U61(tt())] = [0]
>= [0]
= [tt()]
[U71(tt(), P)] = [1] P + [5]
> [1] P + [0]
= [U72(isPal(activate(P)))]
[U72(tt())] = [0]
>= [0]
= [tt()]
[isPal(V)] = [1] V + [0]
>= [1] V + [0]
= [U81(isNePal(activate(V)))]
[isPal(n__nil())] = [1]
> [0]
= [tt()]
[U81(tt())] = [0]
>= [0]
= [tt()]
[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())] = [1]
> [0]
= [tt()]
[isNePal(V)] = [1] V + [0]
>= [1] V + [0]
= [U61(isQid(activate(V)))]
[a()] = [2]
> [1]
= [n__a()]
[e()] = [1]
> [0]
= [n__e()]
[i()] = [4]
> [1]
= [n__i()]
[o()] = [4]
> [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^1)).
Strict Trs:
{ U11(tt()) -> tt()
, U22(tt()) -> tt()
, isList(V) -> U11(isNeList(activate(V)))
, activate(X) -> X
, activate(n__nil()) -> nil()
, activate(n____(X1, X2)) -> __(X1, X2)
, activate(n__a()) -> a()
, activate(n__e()) -> e()
, activate(n__i()) -> i()
, activate(n__o()) -> o()
, activate(n__u()) -> u()
, U31(tt()) -> tt()
, U42(tt()) -> tt()
, U52(tt()) -> tt()
, U61(tt()) -> tt()
, U72(tt()) -> tt()
, U81(tt()) -> tt()
, isQid(n__e()) -> tt() }
Weak Trs:
{ __(X1, X2) -> n____(X1, X2)
, nil() -> n__nil()
, U21(tt(), V2) -> U22(isList(activate(V2)))
, isList(n__nil()) -> tt()
, isList(n____(V1, V2)) -> U21(isList(activate(V1)), activate(V2))
, U41(tt(), V2) -> U42(isNeList(activate(V2)))
, isNeList(V) -> U31(isQid(activate(V)))
, isNeList(n____(V1, V2)) ->
U41(isList(activate(V1)), activate(V2))
, isNeList(n____(V1, V2)) ->
U51(isNeList(activate(V1)), activate(V2))
, U51(tt(), V2) -> U52(isList(activate(V2)))
, U71(tt(), P) -> U72(isPal(activate(P)))
, isPal(V) -> U81(isNePal(activate(V)))
, isPal(n__nil()) -> tt()
, isQid(n__a()) -> tt()
, isQid(n__i()) -> tt()
, isQid(n__o()) -> tt()
, isQid(n__u()) -> tt()
, isNePal(V) -> U61(isQid(activate(V)))
, 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(U11) = {1}, Uargs(U21) = {1, 2}, Uargs(U22) = {1},
Uargs(isList) = {1}, Uargs(U31) = {1}, Uargs(U41) = {1, 2},
Uargs(U42) = {1}, Uargs(isNeList) = {1}, Uargs(U51) = {1, 2},
Uargs(U52) = {1}, Uargs(U61) = {1}, Uargs(U72) = {1},
Uargs(isPal) = {1}, Uargs(U81) = {1}, Uargs(isQid) = {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] = [1]
[U11](x1) = [1] x1 + [0]
[tt] = [0]
[U21](x1, x2) = [1] x1 + [1] x2 + [0]
[U22](x1) = [1] x1 + [0]
[isList](x1) = [1] x1 + [0]
[activate](x1) = [1] x1 + [0]
[U31](x1) = [1] x1 + [0]
[U41](x1, x2) = [1] x1 + [1] x2 + [0]
[U42](x1) = [1] x1 + [0]
[isNeList](x1) = [1] x1 + [0]
[U51](x1, x2) = [1] x1 + [1] x2 + [0]
[U52](x1) = [1] x1 + [0]
[U61](x1) = [1] x1 + [0]
[U71](x1, x2) = [1] x2 + [5]
[U72](x1) = [1] x1 + [0]
[isPal](x1) = [1] x1 + [0]
[U81](x1) = [1] x1 + [0]
[n__nil] = [0]
[n____](x1, x2) = [1] x1 + [1] x2 + [0]
[isQid](x1) = [1] x1 + [0]
[isNePal](x1) = [1] x1 + [0]
[n__a] = [1]
[n__e] = [1]
[n__i] = [0]
[n__o] = [0]
[n__u] = [1]
[a] = [2]
[e] = [1]
[i] = [1]
[o] = [1]
[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()] = [1]
> [0]
= [n__nil()]
[U11(tt())] = [0]
>= [0]
= [tt()]
[U21(tt(), V2)] = [1] V2 + [0]
>= [1] V2 + [0]
= [U22(isList(activate(V2)))]
[U22(tt())] = [0]
>= [0]
= [tt()]
[isList(V)] = [1] V + [0]
>= [1] V + [0]
= [U11(isNeList(activate(V)))]
[isList(n__nil())] = [0]
>= [0]
= [tt()]
[isList(n____(V1, V2))] = [1] V2 + [1] V1 + [0]
>= [1] V2 + [1] V1 + [0]
= [U21(isList(activate(V1)), activate(V2))]
[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 + [1]
= [__(X1, X2)]
[activate(n__a())] = [1]
? [2]
= [a()]
[activate(n__e())] = [1]
>= [1]
= [e()]
[activate(n__i())] = [0]
? [1]
= [i()]
[activate(n__o())] = [0]
? [1]
= [o()]
[activate(n__u())] = [1]
? [5]
= [u()]
[U31(tt())] = [0]
>= [0]
= [tt()]
[U41(tt(), V2)] = [1] V2 + [0]
>= [1] V2 + [0]
= [U42(isNeList(activate(V2)))]
[U42(tt())] = [0]
>= [0]
= [tt()]
[isNeList(V)] = [1] V + [0]
>= [1] V + [0]
= [U31(isQid(activate(V)))]
[isNeList(n____(V1, V2))] = [1] V2 + [1] V1 + [0]
>= [1] V2 + [1] V1 + [0]
= [U41(isList(activate(V1)), activate(V2))]
[isNeList(n____(V1, V2))] = [1] V2 + [1] V1 + [0]
>= [1] V2 + [1] V1 + [0]
= [U51(isNeList(activate(V1)), activate(V2))]
[U51(tt(), V2)] = [1] V2 + [0]
>= [1] V2 + [0]
= [U52(isList(activate(V2)))]
[U52(tt())] = [0]
>= [0]
= [tt()]
[U61(tt())] = [0]
>= [0]
= [tt()]
[U71(tt(), P)] = [1] P + [5]
> [1] P + [0]
= [U72(isPal(activate(P)))]
[U72(tt())] = [0]
>= [0]
= [tt()]
[isPal(V)] = [1] V + [0]
>= [1] V + [0]
= [U81(isNePal(activate(V)))]
[isPal(n__nil())] = [0]
>= [0]
= [tt()]
[U81(tt())] = [0]
>= [0]
= [tt()]
[isQid(n__a())] = [1]
> [0]
= [tt()]
[isQid(n__e())] = [1]
> [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]
= [U61(isQid(activate(V)))]
[a()] = [2]
> [1]
= [n__a()]
[e()] = [1]
>= [1]
= [n__e()]
[i()] = [1]
> [0]
= [n__i()]
[o()] = [1]
> [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:
{ U11(tt()) -> tt()
, U22(tt()) -> tt()
, isList(V) -> U11(isNeList(activate(V)))
, activate(X) -> X
, activate(n__nil()) -> nil()
, activate(n____(X1, X2)) -> __(X1, X2)
, activate(n__a()) -> a()
, activate(n__e()) -> e()
, activate(n__i()) -> i()
, activate(n__o()) -> o()
, activate(n__u()) -> u()
, U31(tt()) -> tt()
, U42(tt()) -> tt()
, U52(tt()) -> tt()
, U61(tt()) -> tt()
, U72(tt()) -> tt()
, U81(tt()) -> tt() }
Weak Trs:
{ __(X1, X2) -> n____(X1, X2)
, nil() -> n__nil()
, U21(tt(), V2) -> U22(isList(activate(V2)))
, isList(n__nil()) -> tt()
, isList(n____(V1, V2)) -> U21(isList(activate(V1)), activate(V2))
, U41(tt(), V2) -> U42(isNeList(activate(V2)))
, isNeList(V) -> U31(isQid(activate(V)))
, isNeList(n____(V1, V2)) ->
U41(isList(activate(V1)), activate(V2))
, isNeList(n____(V1, V2)) ->
U51(isNeList(activate(V1)), activate(V2))
, U51(tt(), V2) -> U52(isList(activate(V2)))
, U71(tt(), P) -> U72(isPal(activate(P)))
, isPal(V) -> U81(isNePal(activate(V)))
, isPal(n__nil()) -> tt()
, isQid(n__a()) -> tt()
, isQid(n__e()) -> tt()
, isQid(n__i()) -> tt()
, isQid(n__o()) -> tt()
, isQid(n__u()) -> tt()
, isNePal(V) -> U61(isQid(activate(V)))
, 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(U11) = {1}, Uargs(U21) = {1, 2}, Uargs(U22) = {1},
Uargs(isList) = {1}, Uargs(U31) = {1}, Uargs(U41) = {1, 2},
Uargs(U42) = {1}, Uargs(isNeList) = {1}, Uargs(U51) = {1, 2},
Uargs(U52) = {1}, Uargs(U61) = {1}, Uargs(U72) = {1},
Uargs(isPal) = {1}, Uargs(U81) = {1}, Uargs(isQid) = {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] = [1]
[U11](x1) = [1] x1 + [0]
[tt] = [1]
[U21](x1, x2) = [1] x1 + [1] x2 + [0]
[U22](x1) = [1] x1 + [0]
[isList](x1) = [1] x1 + [0]
[activate](x1) = [1] x1 + [0]
[U31](x1) = [1] x1 + [0]
[U41](x1, x2) = [1] x1 + [1] x2 + [0]
[U42](x1) = [1] x1 + [0]
[isNeList](x1) = [1] x1 + [0]
[U51](x1, x2) = [1] x1 + [1] x2 + [0]
[U52](x1) = [1] x1 + [0]
[U61](x1) = [1] x1 + [4]
[U71](x1, x2) = [1] x1 + [1] x2 + [7]
[U72](x1) = [1] x1 + [0]
[isPal](x1) = [1] x1 + [4]
[U81](x1) = [1] x1 + [0]
[n__nil] = [1]
[n____](x1, x2) = [1] x1 + [1] x2 + [0]
[isQid](x1) = [1] x1 + [0]
[isNePal](x1) = [1] x1 + [4]
[n__a] = [1]
[n__e] = [1]
[n__i] = [1]
[n__o] = [1]
[n__u] = [1]
[a] = [5]
[e] = [4]
[i] = [4]
[o] = [4]
[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()] = [1]
>= [1]
= [n__nil()]
[U11(tt())] = [1]
>= [1]
= [tt()]
[U21(tt(), V2)] = [1] V2 + [1]
> [1] V2 + [0]
= [U22(isList(activate(V2)))]
[U22(tt())] = [1]
>= [1]
= [tt()]
[isList(V)] = [1] V + [0]
>= [1] V + [0]
= [U11(isNeList(activate(V)))]
[isList(n__nil())] = [1]
>= [1]
= [tt()]
[isList(n____(V1, V2))] = [1] V2 + [1] V1 + [0]
>= [1] V2 + [1] V1 + [0]
= [U21(isList(activate(V1)), activate(V2))]
[activate(X)] = [1] X + [0]
>= [1] X + [0]
= [X]
[activate(n__nil())] = [1]
>= [1]
= [nil()]
[activate(n____(X1, X2))] = [1] X1 + [1] X2 + [0]
? [1] X1 + [1] X2 + [1]
= [__(X1, X2)]
[activate(n__a())] = [1]
? [5]
= [a()]
[activate(n__e())] = [1]
? [4]
= [e()]
[activate(n__i())] = [1]
? [4]
= [i()]
[activate(n__o())] = [1]
? [4]
= [o()]
[activate(n__u())] = [1]
? [5]
= [u()]
[U31(tt())] = [1]
>= [1]
= [tt()]
[U41(tt(), V2)] = [1] V2 + [1]
> [1] V2 + [0]
= [U42(isNeList(activate(V2)))]
[U42(tt())] = [1]
>= [1]
= [tt()]
[isNeList(V)] = [1] V + [0]
>= [1] V + [0]
= [U31(isQid(activate(V)))]
[isNeList(n____(V1, V2))] = [1] V2 + [1] V1 + [0]
>= [1] V2 + [1] V1 + [0]
= [U41(isList(activate(V1)), activate(V2))]
[isNeList(n____(V1, V2))] = [1] V2 + [1] V1 + [0]
>= [1] V2 + [1] V1 + [0]
= [U51(isNeList(activate(V1)), activate(V2))]
[U51(tt(), V2)] = [1] V2 + [1]
> [1] V2 + [0]
= [U52(isList(activate(V2)))]
[U52(tt())] = [1]
>= [1]
= [tt()]
[U61(tt())] = [5]
> [1]
= [tt()]
[U71(tt(), P)] = [1] P + [8]
> [1] P + [4]
= [U72(isPal(activate(P)))]
[U72(tt())] = [1]
>= [1]
= [tt()]
[isPal(V)] = [1] V + [4]
>= [1] V + [4]
= [U81(isNePal(activate(V)))]
[isPal(n__nil())] = [5]
> [1]
= [tt()]
[U81(tt())] = [1]
>= [1]
= [tt()]
[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 + [4]
>= [1] V + [4]
= [U61(isQid(activate(V)))]
[a()] = [5]
> [1]
= [n__a()]
[e()] = [4]
> [1]
= [n__e()]
[i()] = [4]
> [1]
= [n__i()]
[o()] = [4]
> [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^1)).
Strict Trs:
{ U11(tt()) -> tt()
, U22(tt()) -> tt()
, isList(V) -> U11(isNeList(activate(V)))
, activate(X) -> X
, activate(n__nil()) -> nil()
, activate(n____(X1, X2)) -> __(X1, X2)
, activate(n__a()) -> a()
, activate(n__e()) -> e()
, activate(n__i()) -> i()
, activate(n__o()) -> o()
, activate(n__u()) -> u()
, U31(tt()) -> tt()
, U42(tt()) -> tt()
, U52(tt()) -> tt()
, U72(tt()) -> tt()
, U81(tt()) -> tt() }
Weak Trs:
{ __(X1, X2) -> n____(X1, X2)
, nil() -> n__nil()
, U21(tt(), V2) -> U22(isList(activate(V2)))
, isList(n__nil()) -> tt()
, isList(n____(V1, V2)) -> U21(isList(activate(V1)), activate(V2))
, U41(tt(), V2) -> U42(isNeList(activate(V2)))
, isNeList(V) -> U31(isQid(activate(V)))
, isNeList(n____(V1, V2)) ->
U41(isList(activate(V1)), activate(V2))
, isNeList(n____(V1, V2)) ->
U51(isNeList(activate(V1)), activate(V2))
, U51(tt(), V2) -> U52(isList(activate(V2)))
, U61(tt()) -> tt()
, U71(tt(), P) -> U72(isPal(activate(P)))
, isPal(V) -> U81(isNePal(activate(V)))
, isPal(n__nil()) -> tt()
, isQid(n__a()) -> tt()
, isQid(n__e()) -> tt()
, isQid(n__i()) -> tt()
, isQid(n__o()) -> tt()
, isQid(n__u()) -> tt()
, isNePal(V) -> U61(isQid(activate(V)))
, 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(U11) = {1}, Uargs(U21) = {1, 2}, Uargs(U22) = {1},
Uargs(isList) = {1}, Uargs(U31) = {1}, Uargs(U41) = {1, 2},
Uargs(U42) = {1}, Uargs(isNeList) = {1}, Uargs(U51) = {1, 2},
Uargs(U52) = {1}, Uargs(U61) = {1}, Uargs(U72) = {1},
Uargs(isPal) = {1}, Uargs(U81) = {1}, Uargs(isQid) = {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] = [1]
[U11](x1) = [1] x1 + [0]
[tt] = [0]
[U21](x1, x2) = [1] x1 + [1] x2 + [0]
[U22](x1) = [1] x1 + [0]
[isList](x1) = [1] x1 + [0]
[activate](x1) = [1] x1 + [0]
[U31](x1) = [1] x1 + [1]
[U41](x1, x2) = [1] x1 + [1] x2 + [1]
[U42](x1) = [1] x1 + [0]
[isNeList](x1) = [1] x1 + [1]
[U51](x1, x2) = [1] x1 + [1] x2 + [0]
[U52](x1) = [1] x1 + [0]
[U61](x1) = [1] x1 + [0]
[U71](x1, x2) = [1] x2 + [4]
[U72](x1) = [1] x1 + [0]
[isPal](x1) = [1] x1 + [1]
[U81](x1) = [1] x1 + [0]
[n__nil] = [0]
[n____](x1, x2) = [1] x1 + [1] x2 + [0]
[isQid](x1) = [1] x1 + [0]
[isNePal](x1) = [1] x1 + [0]
[n__a] = [0]
[n__e] = [0]
[n__i] = [0]
[n__o] = [0]
[n__u] = [0]
[a] = [1]
[e] = [1]
[i] = [1]
[o] = [1]
[u] = [1]
The order satisfies the following ordering constraints:
[__(X1, X2)] = [1] X1 + [1] X2 + [1]
> [1] X1 + [1] X2 + [0]
= [n____(X1, X2)]
[nil()] = [1]
> [0]
= [n__nil()]
[U11(tt())] = [0]
>= [0]
= [tt()]
[U21(tt(), V2)] = [1] V2 + [0]
>= [1] V2 + [0]
= [U22(isList(activate(V2)))]
[U22(tt())] = [0]
>= [0]
= [tt()]
[isList(V)] = [1] V + [0]
? [1] V + [1]
= [U11(isNeList(activate(V)))]
[isList(n__nil())] = [0]
>= [0]
= [tt()]
[isList(n____(V1, V2))] = [1] V2 + [1] V1 + [0]
>= [1] V2 + [1] V1 + [0]
= [U21(isList(activate(V1)), activate(V2))]
[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 + [1]
= [__(X1, X2)]
[activate(n__a())] = [0]
? [1]
= [a()]
[activate(n__e())] = [0]
? [1]
= [e()]
[activate(n__i())] = [0]
? [1]
= [i()]
[activate(n__o())] = [0]
? [1]
= [o()]
[activate(n__u())] = [0]
? [1]
= [u()]
[U31(tt())] = [1]
> [0]
= [tt()]
[U41(tt(), V2)] = [1] V2 + [1]
>= [1] V2 + [1]
= [U42(isNeList(activate(V2)))]
[U42(tt())] = [0]
>= [0]
= [tt()]
[isNeList(V)] = [1] V + [1]
>= [1] V + [1]
= [U31(isQid(activate(V)))]
[isNeList(n____(V1, V2))] = [1] V2 + [1] V1 + [1]
>= [1] V2 + [1] V1 + [1]
= [U41(isList(activate(V1)), activate(V2))]
[isNeList(n____(V1, V2))] = [1] V2 + [1] V1 + [1]
>= [1] V2 + [1] V1 + [1]
= [U51(isNeList(activate(V1)), activate(V2))]
[U51(tt(), V2)] = [1] V2 + [0]
>= [1] V2 + [0]
= [U52(isList(activate(V2)))]
[U52(tt())] = [0]
>= [0]
= [tt()]
[U61(tt())] = [0]
>= [0]
= [tt()]
[U71(tt(), P)] = [1] P + [4]
> [1] P + [1]
= [U72(isPal(activate(P)))]
[U72(tt())] = [0]
>= [0]
= [tt()]
[isPal(V)] = [1] V + [1]
> [1] V + [0]
= [U81(isNePal(activate(V)))]
[isPal(n__nil())] = [1]
> [0]
= [tt()]
[U81(tt())] = [0]
>= [0]
= [tt()]
[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]
= [U61(isQid(activate(V)))]
[a()] = [1]
> [0]
= [n__a()]
[e()] = [1]
> [0]
= [n__e()]
[i()] = [1]
> [0]
= [n__i()]
[o()] = [1]
> [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:
{ U11(tt()) -> tt()
, U22(tt()) -> tt()
, isList(V) -> U11(isNeList(activate(V)))
, activate(X) -> X
, activate(n__nil()) -> nil()
, activate(n____(X1, X2)) -> __(X1, X2)
, activate(n__a()) -> a()
, activate(n__e()) -> e()
, activate(n__i()) -> i()
, activate(n__o()) -> o()
, activate(n__u()) -> u()
, U42(tt()) -> tt()
, U52(tt()) -> tt()
, U72(tt()) -> tt()
, U81(tt()) -> tt() }
Weak Trs:
{ __(X1, X2) -> n____(X1, X2)
, nil() -> n__nil()
, U21(tt(), V2) -> U22(isList(activate(V2)))
, isList(n__nil()) -> tt()
, isList(n____(V1, V2)) -> U21(isList(activate(V1)), activate(V2))
, U31(tt()) -> tt()
, U41(tt(), V2) -> U42(isNeList(activate(V2)))
, isNeList(V) -> U31(isQid(activate(V)))
, isNeList(n____(V1, V2)) ->
U41(isList(activate(V1)), activate(V2))
, isNeList(n____(V1, V2)) ->
U51(isNeList(activate(V1)), activate(V2))
, U51(tt(), V2) -> U52(isList(activate(V2)))
, U61(tt()) -> tt()
, U71(tt(), P) -> U72(isPal(activate(P)))
, isPal(V) -> U81(isNePal(activate(V)))
, isPal(n__nil()) -> tt()
, isQid(n__a()) -> tt()
, isQid(n__e()) -> tt()
, isQid(n__i()) -> tt()
, isQid(n__o()) -> tt()
, isQid(n__u()) -> tt()
, isNePal(V) -> U61(isQid(activate(V)))
, 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(U11) = {1}, Uargs(U21) = {1, 2}, Uargs(U22) = {1},
Uargs(isList) = {1}, Uargs(U31) = {1}, Uargs(U41) = {1, 2},
Uargs(U42) = {1}, Uargs(isNeList) = {1}, Uargs(U51) = {1, 2},
Uargs(U52) = {1}, Uargs(U61) = {1}, Uargs(U72) = {1},
Uargs(isPal) = {1}, Uargs(U81) = {1}, Uargs(isQid) = {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] = [1]
[U11](x1) = [1] x1 + [0]
[tt] = [1]
[U21](x1, x2) = [1] x1 + [1] x2 + [0]
[U22](x1) = [1] x1 + [0]
[isList](x1) = [1] x1 + [1]
[activate](x1) = [1] x1 + [0]
[U31](x1) = [1] x1 + [0]
[U41](x1, x2) = [1] x1 + [1] x2 + [3]
[U42](x1) = [1] x1 + [0]
[isNeList](x1) = [1] x1 + [4]
[U51](x1, x2) = [1] x1 + [1] x2 + [0]
[U52](x1) = [1] x1 + [0]
[U61](x1) = [1] x1 + [0]
[U71](x1, x2) = [1] x2 + [7]
[U72](x1) = [1] x1 + [0]
[isPal](x1) = [1] x1 + [7]
[U81](x1) = [1] x1 + [3]
[n__nil] = [0]
[n____](x1, x2) = [1] x1 + [1] x2 + [0]
[isQid](x1) = [1] x1 + [4]
[isNePal](x1) = [1] x1 + [4]
[n__a] = [0]
[n__e] = [0]
[n__i] = [0]
[n__o] = [0]
[n__u] = [0]
[a] = [1]
[e] = [1]
[i] = [1]
[o] = [1]
[u] = [1]
The order satisfies the following ordering constraints:
[__(X1, X2)] = [1] X1 + [1] X2 + [1]
> [1] X1 + [1] X2 + [0]
= [n____(X1, X2)]
[nil()] = [1]
> [0]
= [n__nil()]
[U11(tt())] = [1]
>= [1]
= [tt()]
[U21(tt(), V2)] = [1] V2 + [1]
>= [1] V2 + [1]
= [U22(isList(activate(V2)))]
[U22(tt())] = [1]
>= [1]
= [tt()]
[isList(V)] = [1] V + [1]
? [1] V + [4]
= [U11(isNeList(activate(V)))]
[isList(n__nil())] = [1]
>= [1]
= [tt()]
[isList(n____(V1, V2))] = [1] V2 + [1] V1 + [1]
>= [1] V2 + [1] V1 + [1]
= [U21(isList(activate(V1)), activate(V2))]
[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 + [1]
= [__(X1, X2)]
[activate(n__a())] = [0]
? [1]
= [a()]
[activate(n__e())] = [0]
? [1]
= [e()]
[activate(n__i())] = [0]
? [1]
= [i()]
[activate(n__o())] = [0]
? [1]
= [o()]
[activate(n__u())] = [0]
? [1]
= [u()]
[U31(tt())] = [1]
>= [1]
= [tt()]
[U41(tt(), V2)] = [1] V2 + [4]
>= [1] V2 + [4]
= [U42(isNeList(activate(V2)))]
[U42(tt())] = [1]
>= [1]
= [tt()]
[isNeList(V)] = [1] V + [4]
>= [1] V + [4]
= [U31(isQid(activate(V)))]
[isNeList(n____(V1, V2))] = [1] V2 + [1] V1 + [4]
>= [1] V2 + [1] V1 + [4]
= [U41(isList(activate(V1)), activate(V2))]
[isNeList(n____(V1, V2))] = [1] V2 + [1] V1 + [4]
>= [1] V2 + [1] V1 + [4]
= [U51(isNeList(activate(V1)), activate(V2))]
[U51(tt(), V2)] = [1] V2 + [1]
>= [1] V2 + [1]
= [U52(isList(activate(V2)))]
[U52(tt())] = [1]
>= [1]
= [tt()]
[U61(tt())] = [1]
>= [1]
= [tt()]
[U71(tt(), P)] = [1] P + [7]
>= [1] P + [7]
= [U72(isPal(activate(P)))]
[U72(tt())] = [1]
>= [1]
= [tt()]
[isPal(V)] = [1] V + [7]
>= [1] V + [7]
= [U81(isNePal(activate(V)))]
[isPal(n__nil())] = [7]
> [1]
= [tt()]
[U81(tt())] = [4]
> [1]
= [tt()]
[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 + [4]
>= [1] V + [4]
= [U61(isQid(activate(V)))]
[a()] = [1]
> [0]
= [n__a()]
[e()] = [1]
> [0]
= [n__e()]
[i()] = [1]
> [0]
= [n__i()]
[o()] = [1]
> [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:
{ U11(tt()) -> tt()
, U22(tt()) -> tt()
, isList(V) -> U11(isNeList(activate(V)))
, activate(X) -> X
, activate(n__nil()) -> nil()
, activate(n____(X1, X2)) -> __(X1, X2)
, activate(n__a()) -> a()
, activate(n__e()) -> e()
, activate(n__i()) -> i()
, activate(n__o()) -> o()
, activate(n__u()) -> u()
, U42(tt()) -> tt()
, U52(tt()) -> tt()
, U72(tt()) -> tt() }
Weak Trs:
{ __(X1, X2) -> n____(X1, X2)
, nil() -> n__nil()
, U21(tt(), V2) -> U22(isList(activate(V2)))
, isList(n__nil()) -> tt()
, isList(n____(V1, V2)) -> U21(isList(activate(V1)), activate(V2))
, U31(tt()) -> tt()
, U41(tt(), V2) -> U42(isNeList(activate(V2)))
, isNeList(V) -> U31(isQid(activate(V)))
, isNeList(n____(V1, V2)) ->
U41(isList(activate(V1)), activate(V2))
, isNeList(n____(V1, V2)) ->
U51(isNeList(activate(V1)), activate(V2))
, U51(tt(), V2) -> U52(isList(activate(V2)))
, U61(tt()) -> tt()
, U71(tt(), P) -> U72(isPal(activate(P)))
, isPal(V) -> U81(isNePal(activate(V)))
, isPal(n__nil()) -> tt()
, U81(tt()) -> tt()
, isQid(n__a()) -> tt()
, isQid(n__e()) -> tt()
, isQid(n__i()) -> tt()
, isQid(n__o()) -> tt()
, isQid(n__u()) -> tt()
, isNePal(V) -> U61(isQid(activate(V)))
, 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(U11) = {1}, Uargs(U21) = {1, 2}, Uargs(U22) = {1},
Uargs(isList) = {1}, Uargs(U31) = {1}, Uargs(U41) = {1, 2},
Uargs(U42) = {1}, Uargs(isNeList) = {1}, Uargs(U51) = {1, 2},
Uargs(U52) = {1}, Uargs(U61) = {1}, Uargs(U72) = {1},
Uargs(isPal) = {1}, Uargs(U81) = {1}, Uargs(isQid) = {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] = [1]
[U11](x1) = [1] x1 + [0]
[tt] = [1]
[U21](x1, x2) = [1] x1 + [1] x2 + [0]
[U22](x1) = [1] x1 + [0]
[isList](x1) = [1] x1 + [1]
[activate](x1) = [1] x1 + [0]
[U31](x1) = [1] x1 + [0]
[U41](x1, x2) = [1] x1 + [1] x2 + [0]
[U42](x1) = [1] x1 + [0]
[isNeList](x1) = [1] x1 + [1]
[U51](x1, x2) = [1] x1 + [1] x2 + [0]
[U52](x1) = [1] x1 + [0]
[U61](x1) = [1] x1 + [0]
[U71](x1, x2) = [1] x1 + [1] x2 + [7]
[U72](x1) = [1] x1 + [7]
[isPal](x1) = [1] x1 + [1]
[U81](x1) = [1] x1 + [0]
[n__nil] = [0]
[n____](x1, x2) = [1] x1 + [1] x2 + [0]
[isQid](x1) = [1] x1 + [1]
[isNePal](x1) = [1] x1 + [1]
[n__a] = [0]
[n__e] = [0]
[n__i] = [0]
[n__o] = [0]
[n__u] = [0]
[a] = [1]
[e] = [1]
[i] = [1]
[o] = [1]
[u] = [1]
The order satisfies the following ordering constraints:
[__(X1, X2)] = [1] X1 + [1] X2 + [1]
> [1] X1 + [1] X2 + [0]
= [n____(X1, X2)]
[nil()] = [1]
> [0]
= [n__nil()]
[U11(tt())] = [1]
>= [1]
= [tt()]
[U21(tt(), V2)] = [1] V2 + [1]
>= [1] V2 + [1]
= [U22(isList(activate(V2)))]
[U22(tt())] = [1]
>= [1]
= [tt()]
[isList(V)] = [1] V + [1]
>= [1] V + [1]
= [U11(isNeList(activate(V)))]
[isList(n__nil())] = [1]
>= [1]
= [tt()]
[isList(n____(V1, V2))] = [1] V2 + [1] V1 + [1]
>= [1] V2 + [1] V1 + [1]
= [U21(isList(activate(V1)), activate(V2))]
[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 + [1]
= [__(X1, X2)]
[activate(n__a())] = [0]
? [1]
= [a()]
[activate(n__e())] = [0]
? [1]
= [e()]
[activate(n__i())] = [0]
? [1]
= [i()]
[activate(n__o())] = [0]
? [1]
= [o()]
[activate(n__u())] = [0]
? [1]
= [u()]
[U31(tt())] = [1]
>= [1]
= [tt()]
[U41(tt(), V2)] = [1] V2 + [1]
>= [1] V2 + [1]
= [U42(isNeList(activate(V2)))]
[U42(tt())] = [1]
>= [1]
= [tt()]
[isNeList(V)] = [1] V + [1]
>= [1] V + [1]
= [U31(isQid(activate(V)))]
[isNeList(n____(V1, V2))] = [1] V2 + [1] V1 + [1]
>= [1] V2 + [1] V1 + [1]
= [U41(isList(activate(V1)), activate(V2))]
[isNeList(n____(V1, V2))] = [1] V2 + [1] V1 + [1]
>= [1] V2 + [1] V1 + [1]
= [U51(isNeList(activate(V1)), activate(V2))]
[U51(tt(), V2)] = [1] V2 + [1]
>= [1] V2 + [1]
= [U52(isList(activate(V2)))]
[U52(tt())] = [1]
>= [1]
= [tt()]
[U61(tt())] = [1]
>= [1]
= [tt()]
[U71(tt(), P)] = [1] P + [8]
>= [1] P + [8]
= [U72(isPal(activate(P)))]
[U72(tt())] = [8]
> [1]
= [tt()]
[isPal(V)] = [1] V + [1]
>= [1] V + [1]
= [U81(isNePal(activate(V)))]
[isPal(n__nil())] = [1]
>= [1]
= [tt()]
[U81(tt())] = [1]
>= [1]
= [tt()]
[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]
= [U61(isQid(activate(V)))]
[a()] = [1]
> [0]
= [n__a()]
[e()] = [1]
> [0]
= [n__e()]
[i()] = [1]
> [0]
= [n__i()]
[o()] = [1]
> [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:
{ U11(tt()) -> tt()
, U22(tt()) -> tt()
, isList(V) -> U11(isNeList(activate(V)))
, activate(X) -> X
, activate(n__nil()) -> nil()
, activate(n____(X1, X2)) -> __(X1, X2)
, activate(n__a()) -> a()
, activate(n__e()) -> e()
, activate(n__i()) -> i()
, activate(n__o()) -> o()
, activate(n__u()) -> u()
, U42(tt()) -> tt()
, U52(tt()) -> tt() }
Weak Trs:
{ __(X1, X2) -> n____(X1, X2)
, nil() -> n__nil()
, U21(tt(), V2) -> U22(isList(activate(V2)))
, isList(n__nil()) -> tt()
, isList(n____(V1, V2)) -> U21(isList(activate(V1)), activate(V2))
, U31(tt()) -> tt()
, U41(tt(), V2) -> U42(isNeList(activate(V2)))
, isNeList(V) -> U31(isQid(activate(V)))
, isNeList(n____(V1, V2)) ->
U41(isList(activate(V1)), activate(V2))
, isNeList(n____(V1, V2)) ->
U51(isNeList(activate(V1)), activate(V2))
, U51(tt(), V2) -> U52(isList(activate(V2)))
, U61(tt()) -> tt()
, U71(tt(), P) -> U72(isPal(activate(P)))
, U72(tt()) -> tt()
, isPal(V) -> U81(isNePal(activate(V)))
, isPal(n__nil()) -> tt()
, U81(tt()) -> tt()
, isQid(n__a()) -> tt()
, isQid(n__e()) -> tt()
, isQid(n__i()) -> tt()
, isQid(n__o()) -> tt()
, isQid(n__u()) -> tt()
, isNePal(V) -> U61(isQid(activate(V)))
, 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(U11) = {1}, Uargs(U21) = {1, 2}, Uargs(U22) = {1},
Uargs(isList) = {1}, Uargs(U31) = {1}, Uargs(U41) = {1, 2},
Uargs(U42) = {1}, Uargs(isNeList) = {1}, Uargs(U51) = {1, 2},
Uargs(U52) = {1}, Uargs(U61) = {1}, Uargs(U72) = {1},
Uargs(isPal) = {1}, Uargs(U81) = {1}, Uargs(isQid) = {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] = [1]
[U11](x1) = [1] x1 + [0]
[tt] = [1]
[U21](x1, x2) = [1] x1 + [1] x2 + [0]
[U22](x1) = [1] x1 + [0]
[isList](x1) = [1] x1 + [1]
[activate](x1) = [1] x1 + [0]
[U31](x1) = [1] x1 + [0]
[U41](x1, x2) = [1] x1 + [1] x2 + [0]
[U42](x1) = [1] x1 + [0]
[isNeList](x1) = [1] x1 + [0]
[U51](x1, x2) = [1] x1 + [1] x2 + [0]
[U52](x1) = [1] x1 + [0]
[U61](x1) = [1] x1 + [0]
[U71](x1, x2) = [1] x2 + [4]
[U72](x1) = [1] x1 + [0]
[isPal](x1) = [1] x1 + [4]
[U81](x1) = [1] x1 + [0]
[n__nil] = [0]
[n____](x1, x2) = [1] x1 + [1] x2 + [1]
[isQid](x1) = [1] x1 + [0]
[isNePal](x1) = [1] x1 + [4]
[n__a] = [1]
[n__e] = [1]
[n__i] = [3]
[n__o] = [2]
[n__u] = [3]
[a] = [4]
[e] = [2]
[i] = [4]
[o] = [3]
[u] = [4]
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()]
[U11(tt())] = [1]
>= [1]
= [tt()]
[U21(tt(), V2)] = [1] V2 + [1]
>= [1] V2 + [1]
= [U22(isList(activate(V2)))]
[U22(tt())] = [1]
>= [1]
= [tt()]
[isList(V)] = [1] V + [1]
> [1] V + [0]
= [U11(isNeList(activate(V)))]
[isList(n__nil())] = [1]
>= [1]
= [tt()]
[isList(n____(V1, V2))] = [1] V2 + [1] V1 + [2]
> [1] V2 + [1] V1 + [1]
= [U21(isList(activate(V1)), activate(V2))]
[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]
= [__(X1, X2)]
[activate(n__a())] = [1]
? [4]
= [a()]
[activate(n__e())] = [1]
? [2]
= [e()]
[activate(n__i())] = [3]
? [4]
= [i()]
[activate(n__o())] = [2]
? [3]
= [o()]
[activate(n__u())] = [3]
? [4]
= [u()]
[U31(tt())] = [1]
>= [1]
= [tt()]
[U41(tt(), V2)] = [1] V2 + [1]
> [1] V2 + [0]
= [U42(isNeList(activate(V2)))]
[U42(tt())] = [1]
>= [1]
= [tt()]
[isNeList(V)] = [1] V + [0]
>= [1] V + [0]
= [U31(isQid(activate(V)))]
[isNeList(n____(V1, V2))] = [1] V2 + [1] V1 + [1]
>= [1] V2 + [1] V1 + [1]
= [U41(isList(activate(V1)), activate(V2))]
[isNeList(n____(V1, V2))] = [1] V2 + [1] V1 + [1]
> [1] V2 + [1] V1 + [0]
= [U51(isNeList(activate(V1)), activate(V2))]
[U51(tt(), V2)] = [1] V2 + [1]
>= [1] V2 + [1]
= [U52(isList(activate(V2)))]
[U52(tt())] = [1]
>= [1]
= [tt()]
[U61(tt())] = [1]
>= [1]
= [tt()]
[U71(tt(), P)] = [1] P + [4]
>= [1] P + [4]
= [U72(isPal(activate(P)))]
[U72(tt())] = [1]
>= [1]
= [tt()]
[isPal(V)] = [1] V + [4]
>= [1] V + [4]
= [U81(isNePal(activate(V)))]
[isPal(n__nil())] = [4]
> [1]
= [tt()]
[U81(tt())] = [1]
>= [1]
= [tt()]
[isQid(n__a())] = [1]
>= [1]
= [tt()]
[isQid(n__e())] = [1]
>= [1]
= [tt()]
[isQid(n__i())] = [3]
> [1]
= [tt()]
[isQid(n__o())] = [2]
> [1]
= [tt()]
[isQid(n__u())] = [3]
> [1]
= [tt()]
[isNePal(V)] = [1] V + [4]
> [1] V + [0]
= [U61(isQid(activate(V)))]
[a()] = [4]
> [1]
= [n__a()]
[e()] = [2]
> [1]
= [n__e()]
[i()] = [4]
> [3]
= [n__i()]
[o()] = [3]
> [2]
= [n__o()]
[u()] = [4]
> [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^1)).
Strict Trs:
{ U11(tt()) -> tt()
, U22(tt()) -> tt()
, activate(X) -> X
, activate(n__nil()) -> nil()
, activate(n____(X1, X2)) -> __(X1, X2)
, activate(n__a()) -> a()
, activate(n__e()) -> e()
, activate(n__i()) -> i()
, activate(n__o()) -> o()
, activate(n__u()) -> u()
, U42(tt()) -> tt()
, U52(tt()) -> tt() }
Weak Trs:
{ __(X1, X2) -> n____(X1, X2)
, nil() -> n__nil()
, U21(tt(), V2) -> U22(isList(activate(V2)))
, isList(V) -> U11(isNeList(activate(V)))
, isList(n__nil()) -> tt()
, isList(n____(V1, V2)) -> U21(isList(activate(V1)), activate(V2))
, U31(tt()) -> tt()
, U41(tt(), V2) -> U42(isNeList(activate(V2)))
, isNeList(V) -> U31(isQid(activate(V)))
, isNeList(n____(V1, V2)) ->
U41(isList(activate(V1)), activate(V2))
, isNeList(n____(V1, V2)) ->
U51(isNeList(activate(V1)), activate(V2))
, U51(tt(), V2) -> U52(isList(activate(V2)))
, U61(tt()) -> tt()
, U71(tt(), P) -> U72(isPal(activate(P)))
, U72(tt()) -> tt()
, isPal(V) -> U81(isNePal(activate(V)))
, isPal(n__nil()) -> tt()
, U81(tt()) -> tt()
, isQid(n__a()) -> tt()
, isQid(n__e()) -> tt()
, isQid(n__i()) -> tt()
, isQid(n__o()) -> tt()
, isQid(n__u()) -> tt()
, isNePal(V) -> U61(isQid(activate(V)))
, 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(U11) = {1}, Uargs(U21) = {1, 2}, Uargs(U22) = {1},
Uargs(isList) = {1}, Uargs(U31) = {1}, Uargs(U41) = {1, 2},
Uargs(U42) = {1}, Uargs(isNeList) = {1}, Uargs(U51) = {1, 2},
Uargs(U52) = {1}, Uargs(U61) = {1}, Uargs(U72) = {1},
Uargs(isPal) = {1}, Uargs(U81) = {1}, Uargs(isQid) = {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]
[U11](x1) = [1] x1 + [1]
[tt] = [0]
[U21](x1, x2) = [1] x1 + [1] x2 + [1]
[U22](x1) = [1] x1 + [0]
[isList](x1) = [1] x1 + [1]
[activate](x1) = [1] x1 + [0]
[U31](x1) = [1] x1 + [0]
[U41](x1, x2) = [1] x1 + [1] x2 + [0]
[U42](x1) = [1] x1 + [0]
[isNeList](x1) = [1] x1 + [0]
[U51](x1, x2) = [1] x1 + [1] x2 + [1]
[U52](x1) = [1] x1 + [0]
[U61](x1) = [1] x1 + [0]
[U71](x1, x2) = [1] x2 + [4]
[U72](x1) = [1] x1 + [0]
[isPal](x1) = [1] x1 + [0]
[U81](x1) = [1] x1 + [0]
[n__nil] = [0]
[n____](x1, x2) = [1] x1 + [1] x2 + [1]
[isQid](x1) = [1] x1 + [0]
[isNePal](x1) = [1] x1 + [0]
[n__a] = [1]
[n__e] = [0]
[n__i] = [1]
[n__o] = [5]
[n__u] = [0]
[a] = [1]
[e] = [1]
[i] = [4]
[o] = [6]
[u] = [1]
The order satisfies the following ordering constraints:
[__(X1, X2)] = [1] X1 + [1] X2 + [4]
> [1] X1 + [1] X2 + [1]
= [n____(X1, X2)]
[nil()] = [1]
> [0]
= [n__nil()]
[U11(tt())] = [1]
> [0]
= [tt()]
[U21(tt(), V2)] = [1] V2 + [1]
>= [1] V2 + [1]
= [U22(isList(activate(V2)))]
[U22(tt())] = [0]
>= [0]
= [tt()]
[isList(V)] = [1] V + [1]
>= [1] V + [1]
= [U11(isNeList(activate(V)))]
[isList(n__nil())] = [1]
> [0]
= [tt()]
[isList(n____(V1, V2))] = [1] V2 + [1] V1 + [2]
>= [1] V2 + [1] V1 + [2]
= [U21(isList(activate(V1)), activate(V2))]
[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 + [4]
= [__(X1, X2)]
[activate(n__a())] = [1]
>= [1]
= [a()]
[activate(n__e())] = [0]
? [1]
= [e()]
[activate(n__i())] = [1]
? [4]
= [i()]
[activate(n__o())] = [5]
? [6]
= [o()]
[activate(n__u())] = [0]
? [1]
= [u()]
[U31(tt())] = [0]
>= [0]
= [tt()]
[U41(tt(), V2)] = [1] V2 + [0]
>= [1] V2 + [0]
= [U42(isNeList(activate(V2)))]
[U42(tt())] = [0]
>= [0]
= [tt()]
[isNeList(V)] = [1] V + [0]
>= [1] V + [0]
= [U31(isQid(activate(V)))]
[isNeList(n____(V1, V2))] = [1] V2 + [1] V1 + [1]
>= [1] V2 + [1] V1 + [1]
= [U41(isList(activate(V1)), activate(V2))]
[isNeList(n____(V1, V2))] = [1] V2 + [1] V1 + [1]
>= [1] V2 + [1] V1 + [1]
= [U51(isNeList(activate(V1)), activate(V2))]
[U51(tt(), V2)] = [1] V2 + [1]
>= [1] V2 + [1]
= [U52(isList(activate(V2)))]
[U52(tt())] = [0]
>= [0]
= [tt()]
[U61(tt())] = [0]
>= [0]
= [tt()]
[U71(tt(), P)] = [1] P + [4]
> [1] P + [0]
= [U72(isPal(activate(P)))]
[U72(tt())] = [0]
>= [0]
= [tt()]
[isPal(V)] = [1] V + [0]
>= [1] V + [0]
= [U81(isNePal(activate(V)))]
[isPal(n__nil())] = [0]
>= [0]
= [tt()]
[U81(tt())] = [0]
>= [0]
= [tt()]
[isQid(n__a())] = [1]
> [0]
= [tt()]
[isQid(n__e())] = [0]
>= [0]
= [tt()]
[isQid(n__i())] = [1]
> [0]
= [tt()]
[isQid(n__o())] = [5]
> [0]
= [tt()]
[isQid(n__u())] = [0]
>= [0]
= [tt()]
[isNePal(V)] = [1] V + [0]
>= [1] V + [0]
= [U61(isQid(activate(V)))]
[a()] = [1]
>= [1]
= [n__a()]
[e()] = [1]
> [0]
= [n__e()]
[i()] = [4]
> [1]
= [n__i()]
[o()] = [6]
> [5]
= [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:
{ U22(tt()) -> tt()
, activate(X) -> X
, activate(n__nil()) -> nil()
, activate(n____(X1, X2)) -> __(X1, X2)
, activate(n__a()) -> a()
, activate(n__e()) -> e()
, activate(n__i()) -> i()
, activate(n__o()) -> o()
, activate(n__u()) -> u()
, U42(tt()) -> tt()
, U52(tt()) -> tt() }
Weak Trs:
{ __(X1, X2) -> n____(X1, X2)
, nil() -> n__nil()
, U11(tt()) -> tt()
, U21(tt(), V2) -> U22(isList(activate(V2)))
, isList(V) -> U11(isNeList(activate(V)))
, isList(n__nil()) -> tt()
, isList(n____(V1, V2)) -> U21(isList(activate(V1)), activate(V2))
, U31(tt()) -> tt()
, U41(tt(), V2) -> U42(isNeList(activate(V2)))
, isNeList(V) -> U31(isQid(activate(V)))
, isNeList(n____(V1, V2)) ->
U41(isList(activate(V1)), activate(V2))
, isNeList(n____(V1, V2)) ->
U51(isNeList(activate(V1)), activate(V2))
, U51(tt(), V2) -> U52(isList(activate(V2)))
, U61(tt()) -> tt()
, U71(tt(), P) -> U72(isPal(activate(P)))
, U72(tt()) -> tt()
, isPal(V) -> U81(isNePal(activate(V)))
, isPal(n__nil()) -> tt()
, U81(tt()) -> tt()
, isQid(n__a()) -> tt()
, isQid(n__e()) -> tt()
, isQid(n__i()) -> tt()
, isQid(n__o()) -> tt()
, isQid(n__u()) -> tt()
, isNePal(V) -> U61(isQid(activate(V)))
, 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(U11) = {1}, Uargs(U21) = {1, 2}, Uargs(U22) = {1},
Uargs(isList) = {1}, Uargs(U31) = {1}, Uargs(U41) = {1, 2},
Uargs(U42) = {1}, Uargs(isNeList) = {1}, Uargs(U51) = {1, 2},
Uargs(U52) = {1}, Uargs(U61) = {1}, Uargs(U72) = {1},
Uargs(isPal) = {1}, Uargs(U81) = {1}, Uargs(isQid) = {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] = [1]
[U11](x1) = [1] x1 + [0]
[tt] = [0]
[U21](x1, x2) = [1] x1 + [1] x2 + [0]
[U22](x1) = [1] x1 + [0]
[isList](x1) = [1] x1 + [0]
[activate](x1) = [1] x1 + [0]
[U31](x1) = [1] x1 + [0]
[U41](x1, x2) = [1] x1 + [1] x2 + [1]
[U42](x1) = [1] x1 + [0]
[isNeList](x1) = [1] x1 + [0]
[U51](x1, x2) = [1] x1 + [1] x2 + [1]
[U52](x1) = [1] x1 + [1]
[U61](x1) = [1] x1 + [0]
[U71](x1, x2) = [1] x2 + [5]
[U72](x1) = [1] x1 + [0]
[isPal](x1) = [1] x1 + [4]
[U81](x1) = [1] x1 + [0]
[n__nil] = [1]
[n____](x1, x2) = [1] x1 + [1] x2 + [1]
[isQid](x1) = [1] x1 + [0]
[isNePal](x1) = [1] x1 + [4]
[n__a] = [0]
[n__e] = [0]
[n__i] = [0]
[n__o] = [0]
[n__u] = [0]
[a] = [1]
[e] = [1]
[i] = [1]
[o] = [1]
[u] = [1]
The order satisfies the following ordering constraints:
[__(X1, X2)] = [1] X1 + [1] X2 + [1]
>= [1] X1 + [1] X2 + [1]
= [n____(X1, X2)]
[nil()] = [1]
>= [1]
= [n__nil()]
[U11(tt())] = [0]
>= [0]
= [tt()]
[U21(tt(), V2)] = [1] V2 + [0]
>= [1] V2 + [0]
= [U22(isList(activate(V2)))]
[U22(tt())] = [0]
>= [0]
= [tt()]
[isList(V)] = [1] V + [0]
>= [1] V + [0]
= [U11(isNeList(activate(V)))]
[isList(n__nil())] = [1]
> [0]
= [tt()]
[isList(n____(V1, V2))] = [1] V2 + [1] V1 + [1]
> [1] V2 + [1] V1 + [0]
= [U21(isList(activate(V1)), activate(V2))]
[activate(X)] = [1] X + [0]
>= [1] X + [0]
= [X]
[activate(n__nil())] = [1]
>= [1]
= [nil()]
[activate(n____(X1, X2))] = [1] X1 + [1] X2 + [1]
>= [1] X1 + [1] X2 + [1]
= [__(X1, X2)]
[activate(n__a())] = [0]
? [1]
= [a()]
[activate(n__e())] = [0]
? [1]
= [e()]
[activate(n__i())] = [0]
? [1]
= [i()]
[activate(n__o())] = [0]
? [1]
= [o()]
[activate(n__u())] = [0]
? [1]
= [u()]
[U31(tt())] = [0]
>= [0]
= [tt()]
[U41(tt(), V2)] = [1] V2 + [1]
> [1] V2 + [0]
= [U42(isNeList(activate(V2)))]
[U42(tt())] = [0]
>= [0]
= [tt()]
[isNeList(V)] = [1] V + [0]
>= [1] V + [0]
= [U31(isQid(activate(V)))]
[isNeList(n____(V1, V2))] = [1] V2 + [1] V1 + [1]
>= [1] V2 + [1] V1 + [1]
= [U41(isList(activate(V1)), activate(V2))]
[isNeList(n____(V1, V2))] = [1] V2 + [1] V1 + [1]
>= [1] V2 + [1] V1 + [1]
= [U51(isNeList(activate(V1)), activate(V2))]
[U51(tt(), V2)] = [1] V2 + [1]
>= [1] V2 + [1]
= [U52(isList(activate(V2)))]
[U52(tt())] = [1]
> [0]
= [tt()]
[U61(tt())] = [0]
>= [0]
= [tt()]
[U71(tt(), P)] = [1] P + [5]
> [1] P + [4]
= [U72(isPal(activate(P)))]
[U72(tt())] = [0]
>= [0]
= [tt()]
[isPal(V)] = [1] V + [4]
>= [1] V + [4]
= [U81(isNePal(activate(V)))]
[isPal(n__nil())] = [5]
> [0]
= [tt()]
[U81(tt())] = [0]
>= [0]
= [tt()]
[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 + [4]
> [1] V + [0]
= [U61(isQid(activate(V)))]
[a()] = [1]
> [0]
= [n__a()]
[e()] = [1]
> [0]
= [n__e()]
[i()] = [1]
> [0]
= [n__i()]
[o()] = [1]
> [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:
{ U22(tt()) -> tt()
, activate(X) -> X
, activate(n__nil()) -> nil()
, activate(n____(X1, X2)) -> __(X1, X2)
, activate(n__a()) -> a()
, activate(n__e()) -> e()
, activate(n__i()) -> i()
, activate(n__o()) -> o()
, activate(n__u()) -> u()
, U42(tt()) -> tt() }
Weak Trs:
{ __(X1, X2) -> n____(X1, X2)
, nil() -> n__nil()
, U11(tt()) -> tt()
, U21(tt(), V2) -> U22(isList(activate(V2)))
, isList(V) -> U11(isNeList(activate(V)))
, isList(n__nil()) -> tt()
, isList(n____(V1, V2)) -> U21(isList(activate(V1)), activate(V2))
, U31(tt()) -> tt()
, U41(tt(), V2) -> U42(isNeList(activate(V2)))
, isNeList(V) -> U31(isQid(activate(V)))
, isNeList(n____(V1, V2)) ->
U41(isList(activate(V1)), activate(V2))
, isNeList(n____(V1, V2)) ->
U51(isNeList(activate(V1)), activate(V2))
, U51(tt(), V2) -> U52(isList(activate(V2)))
, U52(tt()) -> tt()
, U61(tt()) -> tt()
, U71(tt(), P) -> U72(isPal(activate(P)))
, U72(tt()) -> tt()
, isPal(V) -> U81(isNePal(activate(V)))
, isPal(n__nil()) -> tt()
, U81(tt()) -> tt()
, isQid(n__a()) -> tt()
, isQid(n__e()) -> tt()
, isQid(n__i()) -> tt()
, isQid(n__o()) -> tt()
, isQid(n__u()) -> tt()
, isNePal(V) -> U61(isQid(activate(V)))
, 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(U11) = {1}, Uargs(U21) = {1, 2}, Uargs(U22) = {1},
Uargs(isList) = {1}, Uargs(U31) = {1}, Uargs(U41) = {1, 2},
Uargs(U42) = {1}, Uargs(isNeList) = {1}, Uargs(U51) = {1, 2},
Uargs(U52) = {1}, Uargs(U61) = {1}, Uargs(U72) = {1},
Uargs(isPal) = {1}, Uargs(U81) = {1}, Uargs(isQid) = {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] = [4]
[U11](x1) = [1] x1 + [0]
[tt] = [5]
[U21](x1, x2) = [1] x1 + [1] x2 + [0]
[U22](x1) = [1] x1 + [0]
[isList](x1) = [1] x1 + [4]
[activate](x1) = [1] x1 + [0]
[U31](x1) = [1] x1 + [0]
[U41](x1, x2) = [1] x1 + [1] x2 + [1]
[U42](x1) = [1] x1 + [2]
[isNeList](x1) = [1] x1 + [4]
[U51](x1, x2) = [1] x1 + [1] x2 + [0]
[U52](x1) = [1] x1 + [0]
[U61](x1) = [1] x1 + [0]
[U71](x1, x2) = [1] x2 + [7]
[U72](x1) = [1] x1 + [0]
[isPal](x1) = [1] x1 + [7]
[U81](x1) = [1] x1 + [0]
[n__nil] = [1]
[n____](x1, x2) = [1] x1 + [1] x2 + [1]
[isQid](x1) = [1] x1 + [4]
[isNePal](x1) = [1] x1 + [6]
[n__a] = [1]
[n__e] = [1]
[n__i] = [1]
[n__o] = [1]
[n__u] = [1]
[a] = [1]
[e] = [1]
[i] = [1]
[o] = [1]
[u] = [1]
The order satisfies the following ordering constraints:
[__(X1, X2)] = [1] X1 + [1] X2 + [1]
>= [1] X1 + [1] X2 + [1]
= [n____(X1, X2)]
[nil()] = [4]
> [1]
= [n__nil()]
[U11(tt())] = [5]
>= [5]
= [tt()]
[U21(tt(), V2)] = [1] V2 + [5]
> [1] V2 + [4]
= [U22(isList(activate(V2)))]
[U22(tt())] = [5]
>= [5]
= [tt()]
[isList(V)] = [1] V + [4]
>= [1] V + [4]
= [U11(isNeList(activate(V)))]
[isList(n__nil())] = [5]
>= [5]
= [tt()]
[isList(n____(V1, V2))] = [1] V2 + [1] V1 + [5]
> [1] V2 + [1] V1 + [4]
= [U21(isList(activate(V1)), activate(V2))]
[activate(X)] = [1] X + [0]
>= [1] X + [0]
= [X]
[activate(n__nil())] = [1]
? [4]
= [nil()]
[activate(n____(X1, X2))] = [1] X1 + [1] X2 + [1]
>= [1] X1 + [1] X2 + [1]
= [__(X1, X2)]
[activate(n__a())] = [1]
>= [1]
= [a()]
[activate(n__e())] = [1]
>= [1]
= [e()]
[activate(n__i())] = [1]
>= [1]
= [i()]
[activate(n__o())] = [1]
>= [1]
= [o()]
[activate(n__u())] = [1]
>= [1]
= [u()]
[U31(tt())] = [5]
>= [5]
= [tt()]
[U41(tt(), V2)] = [1] V2 + [6]
>= [1] V2 + [6]
= [U42(isNeList(activate(V2)))]
[U42(tt())] = [7]
> [5]
= [tt()]
[isNeList(V)] = [1] V + [4]
>= [1] V + [4]
= [U31(isQid(activate(V)))]
[isNeList(n____(V1, V2))] = [1] V2 + [1] V1 + [5]
>= [1] V2 + [1] V1 + [5]
= [U41(isList(activate(V1)), activate(V2))]
[isNeList(n____(V1, V2))] = [1] V2 + [1] V1 + [5]
> [1] V2 + [1] V1 + [4]
= [U51(isNeList(activate(V1)), activate(V2))]
[U51(tt(), V2)] = [1] V2 + [5]
> [1] V2 + [4]
= [U52(isList(activate(V2)))]
[U52(tt())] = [5]
>= [5]
= [tt()]
[U61(tt())] = [5]
>= [5]
= [tt()]
[U71(tt(), P)] = [1] P + [7]
>= [1] P + [7]
= [U72(isPal(activate(P)))]
[U72(tt())] = [5]
>= [5]
= [tt()]
[isPal(V)] = [1] V + [7]
> [1] V + [6]
= [U81(isNePal(activate(V)))]
[isPal(n__nil())] = [8]
> [5]
= [tt()]
[U81(tt())] = [5]
>= [5]
= [tt()]
[isQid(n__a())] = [5]
>= [5]
= [tt()]
[isQid(n__e())] = [5]
>= [5]
= [tt()]
[isQid(n__i())] = [5]
>= [5]
= [tt()]
[isQid(n__o())] = [5]
>= [5]
= [tt()]
[isQid(n__u())] = [5]
>= [5]
= [tt()]
[isNePal(V)] = [1] V + [6]
> [1] V + [4]
= [U61(isQid(activate(V)))]
[a()] = [1]
>= [1]
= [n__a()]
[e()] = [1]
>= [1]
= [n__e()]
[i()] = [1]
>= [1]
= [n__i()]
[o()] = [1]
>= [1]
= [n__o()]
[u()] = [1]
>= [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:
{ U22(tt()) -> tt()
, activate(X) -> X
, activate(n__nil()) -> nil()
, activate(n____(X1, X2)) -> __(X1, X2)
, activate(n__a()) -> a()
, activate(n__e()) -> e()
, activate(n__i()) -> i()
, activate(n__o()) -> o()
, activate(n__u()) -> u() }
Weak Trs:
{ __(X1, X2) -> n____(X1, X2)
, nil() -> n__nil()
, U11(tt()) -> tt()
, U21(tt(), V2) -> U22(isList(activate(V2)))
, isList(V) -> U11(isNeList(activate(V)))
, isList(n__nil()) -> tt()
, isList(n____(V1, V2)) -> U21(isList(activate(V1)), activate(V2))
, U31(tt()) -> tt()
, U41(tt(), V2) -> U42(isNeList(activate(V2)))
, U42(tt()) -> tt()
, isNeList(V) -> U31(isQid(activate(V)))
, isNeList(n____(V1, V2)) ->
U41(isList(activate(V1)), activate(V2))
, isNeList(n____(V1, V2)) ->
U51(isNeList(activate(V1)), activate(V2))
, U51(tt(), V2) -> U52(isList(activate(V2)))
, U52(tt()) -> tt()
, U61(tt()) -> tt()
, U71(tt(), P) -> U72(isPal(activate(P)))
, U72(tt()) -> tt()
, isPal(V) -> U81(isNePal(activate(V)))
, isPal(n__nil()) -> tt()
, U81(tt()) -> tt()
, isQid(n__a()) -> tt()
, isQid(n__e()) -> tt()
, isQid(n__i()) -> tt()
, isQid(n__o()) -> tt()
, isQid(n__u()) -> tt()
, isNePal(V) -> U61(isQid(activate(V)))
, 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(U11) = {1}, Uargs(U21) = {1, 2}, Uargs(U22) = {1},
Uargs(isList) = {1}, Uargs(U31) = {1}, Uargs(U41) = {1, 2},
Uargs(U42) = {1}, Uargs(isNeList) = {1}, Uargs(U51) = {1, 2},
Uargs(U52) = {1}, Uargs(U61) = {1}, Uargs(U72) = {1},
Uargs(isPal) = {1}, Uargs(U81) = {1}, Uargs(isQid) = {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] = [4]
[U11](x1) = [1] x1 + [0]
[tt] = [4]
[U21](x1, x2) = [1] x1 + [1] x2 + [1]
[U22](x1) = [1] x1 + [1]
[isList](x1) = [1] x1 + [4]
[activate](x1) = [1] x1 + [0]
[U31](x1) = [1] x1 + [0]
[U41](x1, x2) = [1] x1 + [1] x2 + [0]
[U42](x1) = [1] x1 + [0]
[isNeList](x1) = [1] x1 + [4]
[U51](x1, x2) = [1] x1 + [1] x2 + [0]
[U52](x1) = [1] x1 + [0]
[U61](x1) = [1] x1 + [0]
[U71](x1, x2) = [1] x2 + [4]
[U72](x1) = [1] x1 + [0]
[isPal](x1) = [1] x1 + [4]
[U81](x1) = [1] x1 + [0]
[n__nil] = [1]
[n____](x1, x2) = [1] x1 + [1] x2 + [1]
[isQid](x1) = [1] x1 + [4]
[isNePal](x1) = [1] x1 + [4]
[n__a] = [0]
[n__e] = [0]
[n__i] = [0]
[n__o] = [0]
[n__u] = [6]
[a] = [1]
[e] = [1]
[i] = [1]
[o] = [1]
[u] = [7]
The order satisfies the following ordering constraints:
[__(X1, X2)] = [1] X1 + [1] X2 + [4]
> [1] X1 + [1] X2 + [1]
= [n____(X1, X2)]
[nil()] = [4]
> [1]
= [n__nil()]
[U11(tt())] = [4]
>= [4]
= [tt()]
[U21(tt(), V2)] = [1] V2 + [5]
>= [1] V2 + [5]
= [U22(isList(activate(V2)))]
[U22(tt())] = [5]
> [4]
= [tt()]
[isList(V)] = [1] V + [4]
>= [1] V + [4]
= [U11(isNeList(activate(V)))]
[isList(n__nil())] = [5]
> [4]
= [tt()]
[isList(n____(V1, V2))] = [1] V2 + [1] V1 + [5]
>= [1] V2 + [1] V1 + [5]
= [U21(isList(activate(V1)), activate(V2))]
[activate(X)] = [1] X + [0]
>= [1] X + [0]
= [X]
[activate(n__nil())] = [1]
? [4]
= [nil()]
[activate(n____(X1, X2))] = [1] X1 + [1] X2 + [1]
? [1] X1 + [1] X2 + [4]
= [__(X1, X2)]
[activate(n__a())] = [0]
? [1]
= [a()]
[activate(n__e())] = [0]
? [1]
= [e()]
[activate(n__i())] = [0]
? [1]
= [i()]
[activate(n__o())] = [0]
? [1]
= [o()]
[activate(n__u())] = [6]
? [7]
= [u()]
[U31(tt())] = [4]
>= [4]
= [tt()]
[U41(tt(), V2)] = [1] V2 + [4]
>= [1] V2 + [4]
= [U42(isNeList(activate(V2)))]
[U42(tt())] = [4]
>= [4]
= [tt()]
[isNeList(V)] = [1] V + [4]
>= [1] V + [4]
= [U31(isQid(activate(V)))]
[isNeList(n____(V1, V2))] = [1] V2 + [1] V1 + [5]
> [1] V2 + [1] V1 + [4]
= [U41(isList(activate(V1)), activate(V2))]
[isNeList(n____(V1, V2))] = [1] V2 + [1] V1 + [5]
> [1] V2 + [1] V1 + [4]
= [U51(isNeList(activate(V1)), activate(V2))]
[U51(tt(), V2)] = [1] V2 + [4]
>= [1] V2 + [4]
= [U52(isList(activate(V2)))]
[U52(tt())] = [4]
>= [4]
= [tt()]
[U61(tt())] = [4]
>= [4]
= [tt()]
[U71(tt(), P)] = [1] P + [4]
>= [1] P + [4]
= [U72(isPal(activate(P)))]
[U72(tt())] = [4]
>= [4]
= [tt()]
[isPal(V)] = [1] V + [4]
>= [1] V + [4]
= [U81(isNePal(activate(V)))]
[isPal(n__nil())] = [5]
> [4]
= [tt()]
[U81(tt())] = [4]
>= [4]
= [tt()]
[isQid(n__a())] = [4]
>= [4]
= [tt()]
[isQid(n__e())] = [4]
>= [4]
= [tt()]
[isQid(n__i())] = [4]
>= [4]
= [tt()]
[isQid(n__o())] = [4]
>= [4]
= [tt()]
[isQid(n__u())] = [10]
> [4]
= [tt()]
[isNePal(V)] = [1] V + [4]
>= [1] V + [4]
= [U61(isQid(activate(V)))]
[a()] = [1]
> [0]
= [n__a()]
[e()] = [1]
> [0]
= [n__e()]
[i()] = [1]
> [0]
= [n__i()]
[o()] = [1]
> [0]
= [n__o()]
[u()] = [7]
> [6]
= [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:
{ activate(X) -> X
, activate(n__nil()) -> nil()
, activate(n____(X1, X2)) -> __(X1, X2)
, activate(n__a()) -> a()
, activate(n__e()) -> e()
, activate(n__i()) -> i()
, activate(n__o()) -> o()
, activate(n__u()) -> u() }
Weak Trs:
{ __(X1, X2) -> n____(X1, X2)
, nil() -> n__nil()
, U11(tt()) -> tt()
, U21(tt(), V2) -> U22(isList(activate(V2)))
, U22(tt()) -> tt()
, isList(V) -> U11(isNeList(activate(V)))
, isList(n__nil()) -> tt()
, isList(n____(V1, V2)) -> U21(isList(activate(V1)), activate(V2))
, U31(tt()) -> tt()
, U41(tt(), V2) -> U42(isNeList(activate(V2)))
, U42(tt()) -> tt()
, isNeList(V) -> U31(isQid(activate(V)))
, isNeList(n____(V1, V2)) ->
U41(isList(activate(V1)), activate(V2))
, isNeList(n____(V1, V2)) ->
U51(isNeList(activate(V1)), activate(V2))
, U51(tt(), V2) -> U52(isList(activate(V2)))
, U52(tt()) -> tt()
, U61(tt()) -> tt()
, U71(tt(), P) -> U72(isPal(activate(P)))
, U72(tt()) -> tt()
, isPal(V) -> U81(isNePal(activate(V)))
, isPal(n__nil()) -> tt()
, U81(tt()) -> tt()
, isQid(n__a()) -> tt()
, isQid(n__e()) -> tt()
, isQid(n__i()) -> tt()
, isQid(n__o()) -> tt()
, isQid(n__u()) -> tt()
, isNePal(V) -> U61(isQid(activate(V)))
, 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(U11) = {1}, Uargs(U21) = {1, 2}, Uargs(U22) = {1},
Uargs(isList) = {1}, Uargs(U31) = {1}, Uargs(U41) = {1, 2},
Uargs(U42) = {1}, Uargs(isNeList) = {1}, Uargs(U51) = {1, 2},
Uargs(U52) = {1}, Uargs(U61) = {1}, Uargs(U72) = {1},
Uargs(isPal) = {1}, Uargs(U81) = {1}, Uargs(isQid) = {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] = [5]
[U11](x1) = [1] x1 + [0]
[tt] = [5]
[U21](x1, x2) = [1] x1 + [1] x2 + [4]
[U22](x1) = [1] x1 + [0]
[isList](x1) = [1] x1 + [5]
[activate](x1) = [1] x1 + [1]
[U31](x1) = [1] x1 + [0]
[U41](x1, x2) = [1] x1 + [1] x2 + [4]
[U42](x1) = [1] x1 + [4]
[isNeList](x1) = [1] x1 + [4]
[U51](x1, x2) = [1] x1 + [1] x2 + [2]
[U52](x1) = [1] x1 + [0]
[U61](x1) = [1] x1 + [0]
[U71](x1, x2) = [1] x2 + [7]
[U72](x1) = [1] x1 + [0]
[isPal](x1) = [1] x1 + [6]
[U81](x1) = [1] x1 + [0]
[n__nil] = [4]
[n____](x1, x2) = [1] x1 + [1] x2 + [7]
[isQid](x1) = [1] x1 + [0]
[isNePal](x1) = [1] x1 + [4]
[n__a] = [5]
[n__e] = [5]
[n__i] = [5]
[n__o] = [5]
[n__u] = [5]
[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 + [7]
= [n____(X1, X2)]
[nil()] = [5]
> [4]
= [n__nil()]
[U11(tt())] = [5]
>= [5]
= [tt()]
[U21(tt(), V2)] = [1] V2 + [9]
> [1] V2 + [6]
= [U22(isList(activate(V2)))]
[U22(tt())] = [5]
>= [5]
= [tt()]
[isList(V)] = [1] V + [5]
>= [1] V + [5]
= [U11(isNeList(activate(V)))]
[isList(n__nil())] = [9]
> [5]
= [tt()]
[isList(n____(V1, V2))] = [1] V2 + [1] V1 + [12]
> [1] V2 + [1] V1 + [11]
= [U21(isList(activate(V1)), activate(V2))]
[activate(X)] = [1] X + [1]
> [1] X + [0]
= [X]
[activate(n__nil())] = [5]
>= [5]
= [nil()]
[activate(n____(X1, X2))] = [1] X1 + [1] X2 + [8]
> [1] X1 + [1] X2 + [7]
= [__(X1, X2)]
[activate(n__a())] = [6]
> [5]
= [a()]
[activate(n__e())] = [6]
> [5]
= [e()]
[activate(n__i())] = [6]
> [5]
= [i()]
[activate(n__o())] = [6]
> [5]
= [o()]
[activate(n__u())] = [6]
> [5]
= [u()]
[U31(tt())] = [5]
>= [5]
= [tt()]
[U41(tt(), V2)] = [1] V2 + [9]
>= [1] V2 + [9]
= [U42(isNeList(activate(V2)))]
[U42(tt())] = [9]
> [5]
= [tt()]
[isNeList(V)] = [1] V + [4]
> [1] V + [1]
= [U31(isQid(activate(V)))]
[isNeList(n____(V1, V2))] = [1] V2 + [1] V1 + [11]
>= [1] V2 + [1] V1 + [11]
= [U41(isList(activate(V1)), activate(V2))]
[isNeList(n____(V1, V2))] = [1] V2 + [1] V1 + [11]
> [1] V2 + [1] V1 + [8]
= [U51(isNeList(activate(V1)), activate(V2))]
[U51(tt(), V2)] = [1] V2 + [7]
> [1] V2 + [6]
= [U52(isList(activate(V2)))]
[U52(tt())] = [5]
>= [5]
= [tt()]
[U61(tt())] = [5]
>= [5]
= [tt()]
[U71(tt(), P)] = [1] P + [7]
>= [1] P + [7]
= [U72(isPal(activate(P)))]
[U72(tt())] = [5]
>= [5]
= [tt()]
[isPal(V)] = [1] V + [6]
> [1] V + [5]
= [U81(isNePal(activate(V)))]
[isPal(n__nil())] = [10]
> [5]
= [tt()]
[U81(tt())] = [5]
>= [5]
= [tt()]
[isQid(n__a())] = [5]
>= [5]
= [tt()]
[isQid(n__e())] = [5]
>= [5]
= [tt()]
[isQid(n__i())] = [5]
>= [5]
= [tt()]
[isQid(n__o())] = [5]
>= [5]
= [tt()]
[isQid(n__u())] = [5]
>= [5]
= [tt()]
[isNePal(V)] = [1] V + [4]
> [1] V + [1]
= [U61(isQid(activate(V)))]
[a()] = [5]
>= [5]
= [n__a()]
[e()] = [5]
>= [5]
= [n__e()]
[i()] = [5]
>= [5]
= [n__i()]
[o()] = [5]
>= [5]
= [n__o()]
[u()] = [5]
>= [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^1)).
Strict Trs: { activate(n__nil()) -> nil() }
Weak Trs:
{ __(X1, X2) -> n____(X1, X2)
, nil() -> n__nil()
, U11(tt()) -> tt()
, U21(tt(), V2) -> U22(isList(activate(V2)))
, U22(tt()) -> tt()
, isList(V) -> U11(isNeList(activate(V)))
, isList(n__nil()) -> tt()
, isList(n____(V1, V2)) -> U21(isList(activate(V1)), activate(V2))
, activate(X) -> X
, activate(n____(X1, X2)) -> __(X1, X2)
, activate(n__a()) -> a()
, activate(n__e()) -> e()
, activate(n__i()) -> i()
, activate(n__o()) -> o()
, activate(n__u()) -> u()
, U31(tt()) -> tt()
, U41(tt(), V2) -> U42(isNeList(activate(V2)))
, U42(tt()) -> tt()
, isNeList(V) -> U31(isQid(activate(V)))
, isNeList(n____(V1, V2)) ->
U41(isList(activate(V1)), activate(V2))
, isNeList(n____(V1, V2)) ->
U51(isNeList(activate(V1)), activate(V2))
, U51(tt(), V2) -> U52(isList(activate(V2)))
, U52(tt()) -> tt()
, U61(tt()) -> tt()
, U71(tt(), P) -> U72(isPal(activate(P)))
, U72(tt()) -> tt()
, isPal(V) -> U81(isNePal(activate(V)))
, isPal(n__nil()) -> tt()
, U81(tt()) -> tt()
, isQid(n__a()) -> tt()
, isQid(n__e()) -> tt()
, isQid(n__i()) -> tt()
, isQid(n__o()) -> tt()
, isQid(n__u()) -> tt()
, isNePal(V) -> U61(isQid(activate(V)))
, 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(U11) = {1}, Uargs(U21) = {1, 2}, Uargs(U22) = {1},
Uargs(isList) = {1}, Uargs(U31) = {1}, Uargs(U41) = {1, 2},
Uargs(U42) = {1}, Uargs(isNeList) = {1}, Uargs(U51) = {1, 2},
Uargs(U52) = {1}, Uargs(U61) = {1}, Uargs(U72) = {1},
Uargs(isPal) = {1}, Uargs(U81) = {1}, Uargs(isQid) = {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]
[U11](x1) = [1] x1 + [0]
[tt] = [5]
[U21](x1, x2) = [1] x1 + [1] x2 + [4]
[U22](x1) = [1] x1 + [2]
[isList](x1) = [1] x1 + [5]
[activate](x1) = [1] x1 + [1]
[U31](x1) = [1] x1 + [3]
[U41](x1, x2) = [1] x1 + [1] x2 + [0]
[U42](x1) = [1] x1 + [0]
[isNeList](x1) = [1] x1 + [4]
[U51](x1, x2) = [1] x1 + [1] x2 + [4]
[U52](x1) = [1] x1 + [0]
[U61](x1) = [1] x1 + [0]
[U71](x1, x2) = [1] x1 + [1] x2 + [7]
[U72](x1) = [1] x1 + [0]
[isPal](x1) = [1] x1 + [7]
[U81](x1) = [1] x1 + [1]
[n__nil] = [0]
[n____](x1, x2) = [1] x1 + [1] x2 + [7]
[isQid](x1) = [1] x1 + [0]
[isNePal](x1) = [1] x1 + [5]
[n__a] = [5]
[n__e] = [5]
[n__i] = [5]
[n__o] = [5]
[n__u] = [5]
[a] = [6]
[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 + [7]
= [n____(X1, X2)]
[nil()] = [0]
>= [0]
= [n__nil()]
[U11(tt())] = [5]
>= [5]
= [tt()]
[U21(tt(), V2)] = [1] V2 + [9]
> [1] V2 + [8]
= [U22(isList(activate(V2)))]
[U22(tt())] = [7]
> [5]
= [tt()]
[isList(V)] = [1] V + [5]
>= [1] V + [5]
= [U11(isNeList(activate(V)))]
[isList(n__nil())] = [5]
>= [5]
= [tt()]
[isList(n____(V1, V2))] = [1] V2 + [1] V1 + [12]
> [1] V2 + [1] V1 + [11]
= [U21(isList(activate(V1)), activate(V2))]
[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__a())] = [6]
>= [6]
= [a()]
[activate(n__e())] = [6]
> [5]
= [e()]
[activate(n__i())] = [6]
> [5]
= [i()]
[activate(n__o())] = [6]
> [5]
= [o()]
[activate(n__u())] = [6]
> [5]
= [u()]
[U31(tt())] = [8]
> [5]
= [tt()]
[U41(tt(), V2)] = [1] V2 + [5]
>= [1] V2 + [5]
= [U42(isNeList(activate(V2)))]
[U42(tt())] = [5]
>= [5]
= [tt()]
[isNeList(V)] = [1] V + [4]
>= [1] V + [4]
= [U31(isQid(activate(V)))]
[isNeList(n____(V1, V2))] = [1] V2 + [1] V1 + [11]
> [1] V2 + [1] V1 + [7]
= [U41(isList(activate(V1)), activate(V2))]
[isNeList(n____(V1, V2))] = [1] V2 + [1] V1 + [11]
> [1] V2 + [1] V1 + [10]
= [U51(isNeList(activate(V1)), activate(V2))]
[U51(tt(), V2)] = [1] V2 + [9]
> [1] V2 + [6]
= [U52(isList(activate(V2)))]
[U52(tt())] = [5]
>= [5]
= [tt()]
[U61(tt())] = [5]
>= [5]
= [tt()]
[U71(tt(), P)] = [1] P + [12]
> [1] P + [8]
= [U72(isPal(activate(P)))]
[U72(tt())] = [5]
>= [5]
= [tt()]
[isPal(V)] = [1] V + [7]
>= [1] V + [7]
= [U81(isNePal(activate(V)))]
[isPal(n__nil())] = [7]
> [5]
= [tt()]
[U81(tt())] = [6]
> [5]
= [tt()]
[isQid(n__a())] = [5]
>= [5]
= [tt()]
[isQid(n__e())] = [5]
>= [5]
= [tt()]
[isQid(n__i())] = [5]
>= [5]
= [tt()]
[isQid(n__o())] = [5]
>= [5]
= [tt()]
[isQid(n__u())] = [5]
>= [5]
= [tt()]
[isNePal(V)] = [1] V + [5]
> [1] V + [1]
= [U61(isQid(activate(V)))]
[a()] = [6]
> [5]
= [n__a()]
[e()] = [5]
>= [5]
= [n__e()]
[i()] = [5]
>= [5]
= [n__i()]
[o()] = [5]
>= [5]
= [n__o()]
[u()] = [5]
>= [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(1)).
Weak Trs:
{ __(X1, X2) -> n____(X1, X2)
, nil() -> n__nil()
, U11(tt()) -> tt()
, U21(tt(), V2) -> U22(isList(activate(V2)))
, U22(tt()) -> tt()
, isList(V) -> U11(isNeList(activate(V)))
, isList(n__nil()) -> tt()
, isList(n____(V1, V2)) -> U21(isList(activate(V1)), activate(V2))
, activate(X) -> X
, activate(n__nil()) -> nil()
, activate(n____(X1, X2)) -> __(X1, X2)
, activate(n__a()) -> a()
, activate(n__e()) -> e()
, activate(n__i()) -> i()
, activate(n__o()) -> o()
, activate(n__u()) -> u()
, U31(tt()) -> tt()
, U41(tt(), V2) -> U42(isNeList(activate(V2)))
, U42(tt()) -> tt()
, isNeList(V) -> U31(isQid(activate(V)))
, isNeList(n____(V1, V2)) ->
U41(isList(activate(V1)), activate(V2))
, isNeList(n____(V1, V2)) ->
U51(isNeList(activate(V1)), activate(V2))
, U51(tt(), V2) -> U52(isList(activate(V2)))
, U52(tt()) -> tt()
, U61(tt()) -> tt()
, U71(tt(), P) -> U72(isPal(activate(P)))
, U72(tt()) -> tt()
, isPal(V) -> U81(isNePal(activate(V)))
, isPal(n__nil()) -> tt()
, U81(tt()) -> tt()
, isQid(n__a()) -> tt()
, isQid(n__e()) -> tt()
, isQid(n__i()) -> tt()
, isQid(n__o()) -> tt()
, isQid(n__u()) -> tt()
, isNePal(V) -> U61(isQid(activate(V)))
, 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))