```* Step 1: WeightGap WORST_CASE(?,O(n^1))
+ Considered Problem:
- Strict TRS:
U11(tt()) -> tt()
U21(tt(),V2) -> U22(isList(activate(V2)))
U22(tt()) -> tt()
U31(tt()) -> tt()
U41(tt(),V2) -> U42(isNeList(activate(V2)))
U42(tt()) -> tt()
U51(tt(),V2) -> U52(isList(activate(V2)))
U52(tt()) -> tt()
U61(tt()) -> tt()
U71(tt(),P) -> U72(isPal(activate(P)))
U72(tt()) -> tt()
U81(tt()) -> tt()
__(X1,X2) -> n____(X1,X2)
a() -> n__a()
activate(X) -> X
activate(n____(X1,X2)) -> __(X1,X2)
activate(n__a()) -> a()
activate(n__e()) -> e()
activate(n__i()) -> i()
activate(n__nil()) -> nil()
activate(n__o()) -> o()
activate(n__u()) -> u()
e() -> n__e()
i() -> n__i()
isList(V) -> U11(isNeList(activate(V)))
isList(n____(V1,V2)) -> U21(isList(activate(V1)),activate(V2))
isList(n__nil()) -> 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))
isNePal(V) -> U61(isQid(activate(V)))
isNePal(n____(I,__(P,I))) -> U71(isQid(activate(I)),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()
nil() -> n__nil()
o() -> n__o()
u() -> n__u()
- Signature:
{U11/1,U21/2,U22/1,U31/1,U41/2,U42/1,U51/2,U52/1,U61/1,U71/2,U72/1,U81/1,__/2,a/0,activate/1,e/0,i/0
,isList/1,isNeList/1,isNePal/1,isPal/1,isQid/1,nil/0,o/0,u/0} / {n____/2,n__a/0,n__e/0,n__i/0,n__nil/0
,n__o/0,n__u/0,tt/0}
- Obligation:
runtime complexity wrt. defined symbols {U11,U21,U22,U31,U41,U42,U51,U52,U61,U71,U72,U81,__,a,activate,e,i
,isList,isNeList,isNePal,isPal,isQid,nil,o,u} and constructors {n____,n__a,n__e,n__i,n__nil,n__o,n__u,tt}
+ Applied Processor:
WeightGap {wgDimension = 1, wgDegree = 1, wgKind = Algebraic, wgUArgs = UArgs, wgOn = WgOnAny}
+ Details:
The weightgap principle applies using the following nonconstant growth matrix-interpretation:
We apply a matrix interpretation of kind constructor based matrix interpretation:
The following argument positions are considered usable:
uargs(U11) = {1},
uargs(U21) = {1,2},
uargs(U22) = {1},
uargs(U31) = {1},
uargs(U41) = {1,2},
uargs(U42) = {1},
uargs(U51) = {1,2},
uargs(U52) = {1},
uargs(U61) = {1},
uargs(U71) = {1,2},
uargs(U72) = {1},
uargs(U81) = {1},
uargs(activate) = {1},
uargs(isList) = {1},
uargs(isNeList) = {1},
uargs(isNePal) = {1},
uargs(isPal) = {1},
uargs(isQid) = {1}

Following symbols are considered usable:
all
TcT has computed the following interpretation:
p(U11) =  x1 + 
p(U21) =  x1 +  x2 + 
p(U22) =  x1 + 
p(U31) =  x1 + 
p(U41) =  x1 +  x2 + 
p(U42) =  x1 + 
p(U51) =  x1 +  x2 + 
p(U52) =  x1 + 
p(U61) =  x1 + 
p(U71) =  x1 +  x2 + 
p(U72) =  x1 + 
p(U81) =  x1 + 
p(__) =  x1 +  x2 + 
p(a) = 
p(activate) =  x1 + 
p(e) = 
p(i) = 
p(isList) =  x1 + 
p(isNeList) =  x1 + 
p(isNePal) =  x1 + 
p(isPal) =  x1 + 
p(isQid) =  x1 + 
p(n____) =  x1 +  x2 + 
p(n__a) = 
p(n__e) = 
p(n__i) = 
p(n__nil) = 
p(n__o) = 
p(n__u) = 
p(nil) = 
p(o) = 
p(tt) = 
p(u) = 

Following rules are strictly oriented:
U21(tt(),V2) =  V2 + 
>  V2 + 
= U22(isList(activate(V2)))

U71(tt(),P) =  P + 
>  P + 
= U72(isPal(activate(P)))

u() = 
> 
= n__u()

Following rules are (at-least) weakly oriented:
U11(tt()) =  
>= 
=  tt()

U22(tt()) =  
>= 
=  tt()

U31(tt()) =  
>= 
=  tt()

U41(tt(),V2) =   V2 + 
>=  V2 + 
=  U42(isNeList(activate(V2)))

U42(tt()) =  
>= 
=  tt()

U51(tt(),V2) =   V2 + 
>=  V2 + 
=  U52(isList(activate(V2)))

U52(tt()) =  
>= 
=  tt()

U61(tt()) =  
>= 
=  tt()

U72(tt()) =  
>= 
=  tt()

U81(tt()) =  
>= 
=  tt()

__(X1,X2) =   X1 +  X2 + 
>=  X1 +  X2 + 
=  n____(X1,X2)

a() =  
>= 
=  n__a()

activate(X) =   X + 
>=  X + 
=  X

activate(n____(X1,X2)) =   X1 +  X2 + 
>=  X1 +  X2 + 
=  __(X1,X2)

activate(n__a()) =  
>= 
=  a()

activate(n__e()) =  
>= 
=  e()

activate(n__i()) =  
>= 
=  i()

activate(n__nil()) =  
>= 
=  nil()

activate(n__o()) =  
>= 
=  o()

activate(n__u()) =  
>= 
=  u()

e() =  
>= 
=  n__e()

i() =  
>= 
=  n__i()

isList(V) =   V + 
>=  V + 
=  U11(isNeList(activate(V)))

isList(n____(V1,V2)) =   V1 +  V2 + 
>=  V1 +  V2 + 
=  U21(isList(activate(V1)),activate(V2))

isList(n__nil()) =  
>= 
=  tt()

isNeList(V) =   V + 
>=  V + 
=  U31(isQid(activate(V)))

isNeList(n____(V1,V2)) =   V1 +  V2 + 
>=  V1 +  V2 + 
=  U41(isList(activate(V1)),activate(V2))

isNeList(n____(V1,V2)) =   V1 +  V2 + 
>=  V1 +  V2 + 
=  U51(isNeList(activate(V1)),activate(V2))

isNePal(V) =   V + 
>=  V + 
=  U61(isQid(activate(V)))

isNePal(n____(I,__(P,I))) =   I +  P + 
>=  I +  P + 
=  U71(isQid(activate(I)),activate(P))

isPal(V) =   V + 
>=  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()

nil() =  
>= 
=  n__nil()

o() =  
>= 
=  n__o()

Further, it can be verified that all rules not oriented are covered by the weightgap condition.
* Step 2: WeightGap WORST_CASE(?,O(n^1))
+ Considered Problem:
- Strict TRS:
U11(tt()) -> tt()
U22(tt()) -> tt()
U31(tt()) -> tt()
U41(tt(),V2) -> U42(isNeList(activate(V2)))
U42(tt()) -> tt()
U51(tt(),V2) -> U52(isList(activate(V2)))
U52(tt()) -> tt()
U61(tt()) -> tt()
U72(tt()) -> tt()
U81(tt()) -> tt()
__(X1,X2) -> n____(X1,X2)
a() -> n__a()
activate(X) -> X
activate(n____(X1,X2)) -> __(X1,X2)
activate(n__a()) -> a()
activate(n__e()) -> e()
activate(n__i()) -> i()
activate(n__nil()) -> nil()
activate(n__o()) -> o()
activate(n__u()) -> u()
e() -> n__e()
i() -> n__i()
isList(V) -> U11(isNeList(activate(V)))
isList(n____(V1,V2)) -> U21(isList(activate(V1)),activate(V2))
isList(n__nil()) -> 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))
isNePal(V) -> U61(isQid(activate(V)))
isNePal(n____(I,__(P,I))) -> U71(isQid(activate(I)),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()
nil() -> n__nil()
o() -> n__o()
- Weak TRS:
U21(tt(),V2) -> U22(isList(activate(V2)))
U71(tt(),P) -> U72(isPal(activate(P)))
u() -> n__u()
- Signature:
{U11/1,U21/2,U22/1,U31/1,U41/2,U42/1,U51/2,U52/1,U61/1,U71/2,U72/1,U81/1,__/2,a/0,activate/1,e/0,i/0
,isList/1,isNeList/1,isNePal/1,isPal/1,isQid/1,nil/0,o/0,u/0} / {n____/2,n__a/0,n__e/0,n__i/0,n__nil/0
,n__o/0,n__u/0,tt/0}
- Obligation:
runtime complexity wrt. defined symbols {U11,U21,U22,U31,U41,U42,U51,U52,U61,U71,U72,U81,__,a,activate,e,i
,isList,isNeList,isNePal,isPal,isQid,nil,o,u} and constructors {n____,n__a,n__e,n__i,n__nil,n__o,n__u,tt}
+ Applied Processor:
WeightGap {wgDimension = 1, wgDegree = 1, wgKind = Algebraic, wgUArgs = UArgs, wgOn = WgOnAny}
+ Details:
The weightgap principle applies using the following nonconstant growth matrix-interpretation:
We apply a matrix interpretation of kind constructor based matrix interpretation:
The following argument positions are considered usable:
uargs(U11) = {1},
uargs(U21) = {1,2},
uargs(U22) = {1},
uargs(U31) = {1},
uargs(U41) = {1,2},
uargs(U42) = {1},
uargs(U51) = {1,2},
uargs(U52) = {1},
uargs(U61) = {1},
uargs(U71) = {1,2},
uargs(U72) = {1},
uargs(U81) = {1},
uargs(activate) = {1},
uargs(isList) = {1},
uargs(isNeList) = {1},
uargs(isNePal) = {1},
uargs(isPal) = {1},
uargs(isQid) = {1}

Following symbols are considered usable:
all
TcT has computed the following interpretation:
p(U11) =  x1 + 
p(U21) =  x1 +  x2 + 
p(U22) =  x1 + 
p(U31) =  x1 + 
p(U41) =  x1 +  x2 + 
p(U42) =  x1 + 
p(U51) =  x1 +  x2 + 
p(U52) =  x1 + 
p(U61) =  x1 + 
p(U71) =  x1 +  x2 + 
p(U72) =  x1 + 
p(U81) =  x1 + 
p(__) =  x1 +  x2 + 
p(a) = 
p(activate) =  x1 + 
p(e) = 
p(i) = 
p(isList) =  x1 + 
p(isNeList) =  x1 + 
p(isNePal) =  x1 + 
p(isPal) =  x1 + 
p(isQid) =  x1 + 
p(n____) =  x1 +  x2 + 
p(n__a) = 
p(n__e) = 
p(n__i) = 
p(n__nil) = 
p(n__o) = 
p(n__u) = 
p(nil) = 
p(o) = 
p(tt) = 
p(u) = 

Following rules are strictly oriented:
U11(tt()) = 
> 
= tt()

U31(tt()) = 
> 
= tt()

U42(tt()) = 
> 
= tt()

activate(n____(X1,X2)) =  X1 +  X2 + 
>  X1 +  X2 + 
= __(X1,X2)

activate(n__a()) = 
> 
= a()

activate(n__e()) = 
> 
= e()

activate(n__o()) = 
> 
= o()

isList(n____(V1,V2)) =  V1 +  V2 + 
>  V1 +  V2 + 
= U21(isList(activate(V1)),activate(V2))

isNeList(n____(V1,V2)) =  V1 +  V2 + 
>  V1 +  V2 + 
= U41(isList(activate(V1)),activate(V2))

isNeList(n____(V1,V2)) =  V1 +  V2 + 
>  V1 +  V2 + 
= U51(isNeList(activate(V1)),activate(V2))

isNePal(n____(I,__(P,I))) =  I +  P + 
>  I +  P + 
= U71(isQid(activate(I)),activate(P))

isQid(n__a()) = 
> 
= tt()

isQid(n__e()) = 
> 
= tt()

isQid(n__o()) = 
> 
= tt()

Following rules are (at-least) weakly oriented:
U21(tt(),V2) =   V2 + 
>=  V2 + 
=  U22(isList(activate(V2)))

U22(tt()) =  
>= 
=  tt()

U41(tt(),V2) =   V2 + 
>=  V2 + 
=  U42(isNeList(activate(V2)))

U51(tt(),V2) =   V2 + 
>=  V2 + 
=  U52(isList(activate(V2)))

U52(tt()) =  
>= 
=  tt()

U61(tt()) =  
>= 
=  tt()

U71(tt(),P) =   P + 
>=  P + 
=  U72(isPal(activate(P)))

U72(tt()) =  
>= 
=  tt()

U81(tt()) =  
>= 
=  tt()

__(X1,X2) =   X1 +  X2 + 
>=  X1 +  X2 + 
=  n____(X1,X2)

a() =  
>= 
=  n__a()

activate(X) =   X + 
>=  X + 
=  X

activate(n__i()) =  
>= 
=  i()

activate(n__nil()) =  
>= 
=  nil()

activate(n__u()) =  
>= 
=  u()

e() =  
>= 
=  n__e()

i() =  
>= 
=  n__i()

isList(V) =   V + 
>=  V + 
=  U11(isNeList(activate(V)))

isList(n__nil()) =  
>= 
=  tt()

isNeList(V) =   V + 
>=  V + 
=  U31(isQid(activate(V)))

isNePal(V) =   V + 
>=  V + 
=  U61(isQid(activate(V)))

isPal(V) =   V + 
>=  V + 
=  U81(isNePal(activate(V)))

isPal(n__nil()) =  
>= 
=  tt()

isQid(n__i()) =  
>= 
=  tt()

isQid(n__u()) =  
>= 
=  tt()

nil() =  
>= 
=  n__nil()

o() =  
>= 
=  n__o()

u() =  
>= 
=  n__u()

Further, it can be verified that all rules not oriented are covered by the weightgap condition.
* Step 3: WeightGap WORST_CASE(?,O(n^1))
+ Considered Problem:
- Strict TRS:
U22(tt()) -> tt()
U41(tt(),V2) -> U42(isNeList(activate(V2)))
U51(tt(),V2) -> U52(isList(activate(V2)))
U52(tt()) -> tt()
U61(tt()) -> tt()
U72(tt()) -> tt()
U81(tt()) -> tt()
__(X1,X2) -> n____(X1,X2)
a() -> n__a()
activate(X) -> X
activate(n__i()) -> i()
activate(n__nil()) -> nil()
activate(n__u()) -> u()
e() -> n__e()
i() -> n__i()
isList(V) -> U11(isNeList(activate(V)))
isList(n__nil()) -> tt()
isNeList(V) -> U31(isQid(activate(V)))
isNePal(V) -> U61(isQid(activate(V)))
isPal(V) -> U81(isNePal(activate(V)))
isPal(n__nil()) -> tt()
isQid(n__i()) -> tt()
isQid(n__u()) -> tt()
nil() -> n__nil()
o() -> n__o()
- Weak TRS:
U11(tt()) -> tt()
U21(tt(),V2) -> U22(isList(activate(V2)))
U31(tt()) -> tt()
U42(tt()) -> tt()
U71(tt(),P) -> U72(isPal(activate(P)))
activate(n____(X1,X2)) -> __(X1,X2)
activate(n__a()) -> a()
activate(n__e()) -> e()
activate(n__o()) -> o()
isList(n____(V1,V2)) -> U21(isList(activate(V1)),activate(V2))
isNeList(n____(V1,V2)) -> U41(isList(activate(V1)),activate(V2))
isNeList(n____(V1,V2)) -> U51(isNeList(activate(V1)),activate(V2))
isNePal(n____(I,__(P,I))) -> U71(isQid(activate(I)),activate(P))
isQid(n__a()) -> tt()
isQid(n__e()) -> tt()
isQid(n__o()) -> tt()
u() -> n__u()
- Signature:
{U11/1,U21/2,U22/1,U31/1,U41/2,U42/1,U51/2,U52/1,U61/1,U71/2,U72/1,U81/1,__/2,a/0,activate/1,e/0,i/0
,isList/1,isNeList/1,isNePal/1,isPal/1,isQid/1,nil/0,o/0,u/0} / {n____/2,n__a/0,n__e/0,n__i/0,n__nil/0
,n__o/0,n__u/0,tt/0}
- Obligation:
runtime complexity wrt. defined symbols {U11,U21,U22,U31,U41,U42,U51,U52,U61,U71,U72,U81,__,a,activate,e,i
,isList,isNeList,isNePal,isPal,isQid,nil,o,u} and constructors {n____,n__a,n__e,n__i,n__nil,n__o,n__u,tt}
+ Applied Processor:
WeightGap {wgDimension = 1, wgDegree = 1, wgKind = Algebraic, wgUArgs = UArgs, wgOn = WgOnAny}
+ Details:
The weightgap principle applies using the following nonconstant growth matrix-interpretation:
We apply a matrix interpretation of kind constructor based matrix interpretation:
The following argument positions are considered usable:
uargs(U11) = {1},
uargs(U21) = {1,2},
uargs(U22) = {1},
uargs(U31) = {1},
uargs(U41) = {1,2},
uargs(U42) = {1},
uargs(U51) = {1,2},
uargs(U52) = {1},
uargs(U61) = {1},
uargs(U71) = {1,2},
uargs(U72) = {1},
uargs(U81) = {1},
uargs(activate) = {1},
uargs(isList) = {1},
uargs(isNeList) = {1},
uargs(isNePal) = {1},
uargs(isPal) = {1},
uargs(isQid) = {1}

Following symbols are considered usable:
all
TcT has computed the following interpretation:
p(U11) =  x1 + 
p(U21) =  x1 +  x2 + 
p(U22) =  x1 + 
p(U31) =  x1 + 
p(U41) =  x1 +  x2 + 
p(U42) =  x1 + 
p(U51) =  x1 +  x2 + 
p(U52) =  x1 + 
p(U61) =  x1 + 
p(U71) =  x1 +  x2 + 
p(U72) =  x1 + 
p(U81) =  x1 + 
p(__) =  x1 +  x2 + 
p(a) = 
p(activate) =  x1 + 
p(e) = 
p(i) = 
p(isList) =  x1 + 
p(isNeList) =  x1 + 
p(isNePal) =  x1 + 
p(isPal) =  x1 + 
p(isQid) =  x1 + 
p(n____) =  x1 +  x2 + 
p(n__a) = 
p(n__e) = 
p(n__i) = 
p(n__nil) = 
p(n__o) = 
p(n__u) = 
p(nil) = 
p(o) = 
p(tt) = 
p(u) = 

Following rules are strictly oriented:
U22(tt()) = 
> 
= tt()

U41(tt(),V2) =  V2 + 
>  V2 + 
= U42(isNeList(activate(V2)))

U51(tt(),V2) =  V2 + 
>  V2 + 
= U52(isList(activate(V2)))

U61(tt()) = 
> 
= tt()

U81(tt()) = 
> 
= tt()

isNeList(V) =  V + 
>  V + 
= U31(isQid(activate(V)))

isPal(n__nil()) = 
> 
= tt()

nil() = 
> 
= n__nil()

Following rules are (at-least) weakly oriented:
U11(tt()) =  
>= 
=  tt()

U21(tt(),V2) =   V2 + 
>=  V2 + 
=  U22(isList(activate(V2)))

U31(tt()) =  
>= 
=  tt()

U42(tt()) =  
>= 
=  tt()

U52(tt()) =  
>= 
=  tt()

U71(tt(),P) =   P + 
>=  P + 
=  U72(isPal(activate(P)))

U72(tt()) =  
>= 
=  tt()

__(X1,X2) =   X1 +  X2 + 
>=  X1 +  X2 + 
=  n____(X1,X2)

a() =  
>= 
=  n__a()

activate(X) =   X + 
>=  X + 
=  X

activate(n____(X1,X2)) =   X1 +  X2 + 
>=  X1 +  X2 + 
=  __(X1,X2)

activate(n__a()) =  
>= 
=  a()

activate(n__e()) =  
>= 
=  e()

activate(n__i()) =  
>= 
=  i()

activate(n__nil()) =  
>= 
=  nil()

activate(n__o()) =  
>= 
=  o()

activate(n__u()) =  
>= 
=  u()

e() =  
>= 
=  n__e()

i() =  
>= 
=  n__i()

isList(V) =   V + 
>=  V + 
=  U11(isNeList(activate(V)))

isList(n____(V1,V2)) =   V1 +  V2 + 
>=  V1 +  V2 + 
=  U21(isList(activate(V1)),activate(V2))

isList(n__nil()) =  
>= 
=  tt()

isNeList(n____(V1,V2)) =   V1 +  V2 + 
>=  V1 +  V2 + 
=  U41(isList(activate(V1)),activate(V2))

isNeList(n____(V1,V2)) =   V1 +  V2 + 
>=  V1 +  V2 + 
=  U51(isNeList(activate(V1)),activate(V2))

isNePal(V) =   V + 
>=  V + 
=  U61(isQid(activate(V)))

isNePal(n____(I,__(P,I))) =   I +  P + 
>=  I +  P + 
=  U71(isQid(activate(I)),activate(P))

isPal(V) =   V + 
>=  V + 
=  U81(isNePal(activate(V)))

isQid(n__a()) =  
>= 
=  tt()

isQid(n__e()) =  
>= 
=  tt()

isQid(n__i()) =  
>= 
=  tt()

isQid(n__o()) =  
>= 
=  tt()

isQid(n__u()) =  
>= 
=  tt()

o() =  
>= 
=  n__o()

u() =  
>= 
=  n__u()

Further, it can be verified that all rules not oriented are covered by the weightgap condition.
* Step 4: WeightGap WORST_CASE(?,O(n^1))
+ Considered Problem:
- Strict TRS:
U52(tt()) -> tt()
U72(tt()) -> tt()
__(X1,X2) -> n____(X1,X2)
a() -> n__a()
activate(X) -> X
activate(n__i()) -> i()
activate(n__nil()) -> nil()
activate(n__u()) -> u()
e() -> n__e()
i() -> n__i()
isList(V) -> U11(isNeList(activate(V)))
isList(n__nil()) -> tt()
isNePal(V) -> U61(isQid(activate(V)))
isPal(V) -> U81(isNePal(activate(V)))
isQid(n__i()) -> tt()
isQid(n__u()) -> tt()
o() -> n__o()
- Weak TRS:
U11(tt()) -> tt()
U21(tt(),V2) -> U22(isList(activate(V2)))
U22(tt()) -> tt()
U31(tt()) -> tt()
U41(tt(),V2) -> U42(isNeList(activate(V2)))
U42(tt()) -> tt()
U51(tt(),V2) -> U52(isList(activate(V2)))
U61(tt()) -> tt()
U71(tt(),P) -> U72(isPal(activate(P)))
U81(tt()) -> tt()
activate(n____(X1,X2)) -> __(X1,X2)
activate(n__a()) -> a()
activate(n__e()) -> e()
activate(n__o()) -> o()
isList(n____(V1,V2)) -> U21(isList(activate(V1)),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))
isNePal(n____(I,__(P,I))) -> U71(isQid(activate(I)),activate(P))
isPal(n__nil()) -> tt()
isQid(n__a()) -> tt()
isQid(n__e()) -> tt()
isQid(n__o()) -> tt()
nil() -> n__nil()
u() -> n__u()
- Signature:
{U11/1,U21/2,U22/1,U31/1,U41/2,U42/1,U51/2,U52/1,U61/1,U71/2,U72/1,U81/1,__/2,a/0,activate/1,e/0,i/0
,isList/1,isNeList/1,isNePal/1,isPal/1,isQid/1,nil/0,o/0,u/0} / {n____/2,n__a/0,n__e/0,n__i/0,n__nil/0
,n__o/0,n__u/0,tt/0}
- Obligation:
runtime complexity wrt. defined symbols {U11,U21,U22,U31,U41,U42,U51,U52,U61,U71,U72,U81,__,a,activate,e,i
,isList,isNeList,isNePal,isPal,isQid,nil,o,u} and constructors {n____,n__a,n__e,n__i,n__nil,n__o,n__u,tt}
+ Applied Processor:
WeightGap {wgDimension = 1, wgDegree = 1, wgKind = Algebraic, wgUArgs = UArgs, wgOn = WgOnAny}
+ Details:
The weightgap principle applies using the following nonconstant growth matrix-interpretation:
We apply a matrix interpretation of kind constructor based matrix interpretation:
The following argument positions are considered usable:
uargs(U11) = {1},
uargs(U21) = {1,2},
uargs(U22) = {1},
uargs(U31) = {1},
uargs(U41) = {1,2},
uargs(U42) = {1},
uargs(U51) = {1,2},
uargs(U52) = {1},
uargs(U61) = {1},
uargs(U71) = {1,2},
uargs(U72) = {1},
uargs(U81) = {1},
uargs(activate) = {1},
uargs(isList) = {1},
uargs(isNeList) = {1},
uargs(isNePal) = {1},
uargs(isPal) = {1},
uargs(isQid) = {1}

Following symbols are considered usable:
all
TcT has computed the following interpretation:
p(U11) =  x1 + 
p(U21) =  x1 +  x2 + 
p(U22) =  x1 + 
p(U31) =  x1 + 
p(U41) =  x1 +  x2 + 
p(U42) =  x1 + 
p(U51) =  x1 +  x2 + 
p(U52) =  x1 + 
p(U61) =  x1 + 
p(U71) =  x1 +  x2 + 
p(U72) =  x1 + 
p(U81) =  x1 + 
p(__) =  x1 +  x2 + 
p(a) = 
p(activate) =  x1 + 
p(e) = 
p(i) = 
p(isList) =  x1 + 
p(isNeList) =  x1 + 
p(isNePal) =  x1 + 
p(isPal) =  x1 + 
p(isQid) =  x1 + 
p(n____) =  x1 +  x2 + 
p(n__a) = 
p(n__e) = 
p(n__i) = 
p(n__nil) = 
p(n__o) = 
p(n__u) = 
p(nil) = 
p(o) = 
p(tt) = 
p(u) = 

Following rules are strictly oriented:
U52(tt()) = 
> 
= tt()

U72(tt()) = 
> 
= tt()

i() = 
> 
= n__i()

isNePal(V) =  V + 
>  V + 
= U61(isQid(activate(V)))

Following rules are (at-least) weakly oriented:
U11(tt()) =  
>= 
=  tt()

U21(tt(),V2) =   V2 + 
>=  V2 + 
=  U22(isList(activate(V2)))

U22(tt()) =  
>= 
=  tt()

U31(tt()) =  
>= 
=  tt()

U41(tt(),V2) =   V2 + 
>=  V2 + 
=  U42(isNeList(activate(V2)))

U42(tt()) =  
>= 
=  tt()

U51(tt(),V2) =   V2 + 
>=  V2 + 
=  U52(isList(activate(V2)))

U61(tt()) =  
>= 
=  tt()

U71(tt(),P) =   P + 
>=  P + 
=  U72(isPal(activate(P)))

U81(tt()) =  
>= 
=  tt()

__(X1,X2) =   X1 +  X2 + 
>=  X1 +  X2 + 
=  n____(X1,X2)

a() =  
>= 
=  n__a()

activate(X) =   X + 
>=  X + 
=  X

activate(n____(X1,X2)) =   X1 +  X2 + 
>=  X1 +  X2 + 
=  __(X1,X2)

activate(n__a()) =  
>= 
=  a()

activate(n__e()) =  
>= 
=  e()

activate(n__i()) =  
>= 
=  i()

activate(n__nil()) =  
>= 
=  nil()

activate(n__o()) =  
>= 
=  o()

activate(n__u()) =  
>= 
=  u()

e() =  
>= 
=  n__e()

isList(V) =   V + 
>=  V + 
=  U11(isNeList(activate(V)))

isList(n____(V1,V2)) =   V1 +  V2 + 
>=  V1 +  V2 + 
=  U21(isList(activate(V1)),activate(V2))

isList(n__nil()) =  
>= 
=  tt()

isNeList(V) =   V + 
>=  V + 
=  U31(isQid(activate(V)))

isNeList(n____(V1,V2)) =   V1 +  V2 + 
>=  V1 +  V2 + 
=  U41(isList(activate(V1)),activate(V2))

isNeList(n____(V1,V2)) =   V1 +  V2 + 
>=  V1 +  V2 + 
=  U51(isNeList(activate(V1)),activate(V2))

isNePal(n____(I,__(P,I))) =   I +  P + 
>=  I +  P + 
=  U71(isQid(activate(I)),activate(P))

isPal(V) =   V + 
>=  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()

nil() =  
>= 
=  n__nil()

o() =  
>= 
=  n__o()

u() =  
>= 
=  n__u()

Further, it can be verified that all rules not oriented are covered by the weightgap condition.
* Step 5: WeightGap WORST_CASE(?,O(n^1))
+ Considered Problem:
- Strict TRS:
__(X1,X2) -> n____(X1,X2)
a() -> n__a()
activate(X) -> X
activate(n__i()) -> i()
activate(n__nil()) -> nil()
activate(n__u()) -> u()
e() -> n__e()
isList(V) -> U11(isNeList(activate(V)))
isList(n__nil()) -> tt()
isPal(V) -> U81(isNePal(activate(V)))
isQid(n__i()) -> tt()
isQid(n__u()) -> tt()
o() -> n__o()
- Weak TRS:
U11(tt()) -> tt()
U21(tt(),V2) -> U22(isList(activate(V2)))
U22(tt()) -> tt()
U31(tt()) -> tt()
U41(tt(),V2) -> U42(isNeList(activate(V2)))
U42(tt()) -> tt()
U51(tt(),V2) -> U52(isList(activate(V2)))
U52(tt()) -> tt()
U61(tt()) -> tt()
U71(tt(),P) -> U72(isPal(activate(P)))
U72(tt()) -> tt()
U81(tt()) -> tt()
activate(n____(X1,X2)) -> __(X1,X2)
activate(n__a()) -> a()
activate(n__e()) -> e()
activate(n__o()) -> o()
i() -> n__i()
isList(n____(V1,V2)) -> U21(isList(activate(V1)),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))
isNePal(V) -> U61(isQid(activate(V)))
isNePal(n____(I,__(P,I))) -> U71(isQid(activate(I)),activate(P))
isPal(n__nil()) -> tt()
isQid(n__a()) -> tt()
isQid(n__e()) -> tt()
isQid(n__o()) -> tt()
nil() -> n__nil()
u() -> n__u()
- Signature:
{U11/1,U21/2,U22/1,U31/1,U41/2,U42/1,U51/2,U52/1,U61/1,U71/2,U72/1,U81/1,__/2,a/0,activate/1,e/0,i/0
,isList/1,isNeList/1,isNePal/1,isPal/1,isQid/1,nil/0,o/0,u/0} / {n____/2,n__a/0,n__e/0,n__i/0,n__nil/0
,n__o/0,n__u/0,tt/0}
- Obligation:
runtime complexity wrt. defined symbols {U11,U21,U22,U31,U41,U42,U51,U52,U61,U71,U72,U81,__,a,activate,e,i
,isList,isNeList,isNePal,isPal,isQid,nil,o,u} and constructors {n____,n__a,n__e,n__i,n__nil,n__o,n__u,tt}
+ Applied Processor:
WeightGap {wgDimension = 1, wgDegree = 1, wgKind = Algebraic, wgUArgs = UArgs, wgOn = WgOnAny}
+ Details:
The weightgap principle applies using the following nonconstant growth matrix-interpretation:
We apply a matrix interpretation of kind constructor based matrix interpretation:
The following argument positions are considered usable:
uargs(U11) = {1},
uargs(U21) = {1,2},
uargs(U22) = {1},
uargs(U31) = {1},
uargs(U41) = {1,2},
uargs(U42) = {1},
uargs(U51) = {1,2},
uargs(U52) = {1},
uargs(U61) = {1},
uargs(U71) = {1,2},
uargs(U72) = {1},
uargs(U81) = {1},
uargs(activate) = {1},
uargs(isList) = {1},
uargs(isNeList) = {1},
uargs(isNePal) = {1},
uargs(isPal) = {1},
uargs(isQid) = {1}

Following symbols are considered usable:
all
TcT has computed the following interpretation:
p(U11) =  x1 + 
p(U21) =  x1 +  x2 + 
p(U22) =  x1 + 
p(U31) =  x1 + 
p(U41) =  x1 +  x2 + 
p(U42) =  x1 + 
p(U51) =  x1 +  x2 + 
p(U52) =  x1 + 
p(U61) =  x1 + 
p(U71) =  x1 +  x2 + 
p(U72) =  x1 + 
p(U81) =  x1 + 
p(__) =  x1 +  x2 + 
p(a) = 
p(activate) =  x1 + 
p(e) = 
p(i) = 
p(isList) =  x1 + 
p(isNeList) =  x1 + 
p(isNePal) =  x1 + 
p(isPal) =  x1 + 
p(isQid) =  x1 + 
p(n____) =  x1 +  x2 + 
p(n__a) = 
p(n__e) = 
p(n__i) = 
p(n__nil) = 
p(n__o) = 
p(n__u) = 
p(nil) = 
p(o) = 
p(tt) = 
p(u) = 

Following rules are strictly oriented:
isList(V) =  V + 
>  V + 
= U11(isNeList(activate(V)))

isList(n__nil()) = 
> 
= tt()

Following rules are (at-least) weakly oriented:
U11(tt()) =  
>= 
=  tt()

U21(tt(),V2) =   V2 + 
>=  V2 + 
=  U22(isList(activate(V2)))

U22(tt()) =  
>= 
=  tt()

U31(tt()) =  
>= 
=  tt()

U41(tt(),V2) =   V2 + 
>=  V2 + 
=  U42(isNeList(activate(V2)))

U42(tt()) =  
>= 
=  tt()

U51(tt(),V2) =   V2 + 
>=  V2 + 
=  U52(isList(activate(V2)))

U52(tt()) =  
>= 
=  tt()

U61(tt()) =  
>= 
=  tt()

U71(tt(),P) =   P + 
>=  P + 
=  U72(isPal(activate(P)))

U72(tt()) =  
>= 
=  tt()

U81(tt()) =  
>= 
=  tt()

__(X1,X2) =   X1 +  X2 + 
>=  X1 +  X2 + 
=  n____(X1,X2)

a() =  
>= 
=  n__a()

activate(X) =   X + 
>=  X + 
=  X

activate(n____(X1,X2)) =   X1 +  X2 + 
>=  X1 +  X2 + 
=  __(X1,X2)

activate(n__a()) =  
>= 
=  a()

activate(n__e()) =  
>= 
=  e()

activate(n__i()) =  
>= 
=  i()

activate(n__nil()) =  
>= 
=  nil()

activate(n__o()) =  
>= 
=  o()

activate(n__u()) =  
>= 
=  u()

e() =  
>= 
=  n__e()

i() =  
>= 
=  n__i()

isList(n____(V1,V2)) =   V1 +  V2 + 
>=  V1 +  V2 + 
=  U21(isList(activate(V1)),activate(V2))

isNeList(V) =   V + 
>=  V + 
=  U31(isQid(activate(V)))

isNeList(n____(V1,V2)) =   V1 +  V2 + 
>=  V1 +  V2 + 
=  U41(isList(activate(V1)),activate(V2))

isNeList(n____(V1,V2)) =   V1 +  V2 + 
>=  V1 +  V2 + 
=  U51(isNeList(activate(V1)),activate(V2))

isNePal(V) =   V + 
>=  V + 
=  U61(isQid(activate(V)))

isNePal(n____(I,__(P,I))) =   I +  P + 
>=  I +  P + 
=  U71(isQid(activate(I)),activate(P))

isPal(V) =   V + 
>=  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()

nil() =  
>= 
=  n__nil()

o() =  
>= 
=  n__o()

u() =  
>= 
=  n__u()

Further, it can be verified that all rules not oriented are covered by the weightgap condition.
* Step 6: WeightGap WORST_CASE(?,O(n^1))
+ Considered Problem:
- Strict TRS:
__(X1,X2) -> n____(X1,X2)
a() -> n__a()
activate(X) -> X
activate(n__i()) -> i()
activate(n__nil()) -> nil()
activate(n__u()) -> u()
e() -> n__e()
isPal(V) -> U81(isNePal(activate(V)))
isQid(n__i()) -> tt()
isQid(n__u()) -> tt()
o() -> n__o()
- Weak TRS:
U11(tt()) -> tt()
U21(tt(),V2) -> U22(isList(activate(V2)))
U22(tt()) -> tt()
U31(tt()) -> tt()
U41(tt(),V2) -> U42(isNeList(activate(V2)))
U42(tt()) -> tt()
U51(tt(),V2) -> U52(isList(activate(V2)))
U52(tt()) -> tt()
U61(tt()) -> tt()
U71(tt(),P) -> U72(isPal(activate(P)))
U72(tt()) -> tt()
U81(tt()) -> tt()
activate(n____(X1,X2)) -> __(X1,X2)
activate(n__a()) -> a()
activate(n__e()) -> e()
activate(n__o()) -> o()
i() -> n__i()
isList(V) -> U11(isNeList(activate(V)))
isList(n____(V1,V2)) -> U21(isList(activate(V1)),activate(V2))
isList(n__nil()) -> 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))
isNePal(V) -> U61(isQid(activate(V)))
isNePal(n____(I,__(P,I))) -> U71(isQid(activate(I)),activate(P))
isPal(n__nil()) -> tt()
isQid(n__a()) -> tt()
isQid(n__e()) -> tt()
isQid(n__o()) -> tt()
nil() -> n__nil()
u() -> n__u()
- Signature:
{U11/1,U21/2,U22/1,U31/1,U41/2,U42/1,U51/2,U52/1,U61/1,U71/2,U72/1,U81/1,__/2,a/0,activate/1,e/0,i/0
,isList/1,isNeList/1,isNePal/1,isPal/1,isQid/1,nil/0,o/0,u/0} / {n____/2,n__a/0,n__e/0,n__i/0,n__nil/0
,n__o/0,n__u/0,tt/0}
- Obligation:
runtime complexity wrt. defined symbols {U11,U21,U22,U31,U41,U42,U51,U52,U61,U71,U72,U81,__,a,activate,e,i
,isList,isNeList,isNePal,isPal,isQid,nil,o,u} and constructors {n____,n__a,n__e,n__i,n__nil,n__o,n__u,tt}
+ Applied Processor:
WeightGap {wgDimension = 1, wgDegree = 1, wgKind = Algebraic, wgUArgs = UArgs, wgOn = WgOnAny}
+ Details:
The weightgap principle applies using the following nonconstant growth matrix-interpretation:
We apply a matrix interpretation of kind constructor based matrix interpretation:
The following argument positions are considered usable:
uargs(U11) = {1},
uargs(U21) = {1,2},
uargs(U22) = {1},
uargs(U31) = {1},
uargs(U41) = {1,2},
uargs(U42) = {1},
uargs(U51) = {1,2},
uargs(U52) = {1},
uargs(U61) = {1},
uargs(U71) = {1,2},
uargs(U72) = {1},
uargs(U81) = {1},
uargs(activate) = {1},
uargs(isList) = {1},
uargs(isNeList) = {1},
uargs(isNePal) = {1},
uargs(isPal) = {1},
uargs(isQid) = {1}

Following symbols are considered usable:
all
TcT has computed the following interpretation:
p(U11) =  x1 + 
p(U21) =  x1 +  x2 + 
p(U22) =  x1 + 
p(U31) =  x1 + 
p(U41) =  x1 +  x2 + 
p(U42) =  x1 + 
p(U51) =  x1 +  x2 + 
p(U52) =  x1 + 
p(U61) =  x1 + 
p(U71) =  x1 +  x2 + 
p(U72) =  x1 + 
p(U81) =  x1 + 
p(__) =  x1 +  x2 + 
p(a) = 
p(activate) =  x1 + 
p(e) = 
p(i) = 
p(isList) =  x1 + 
p(isNeList) =  x1 + 
p(isNePal) =  x1 + 
p(isPal) =  x1 + 
p(isQid) =  x1 + 
p(n____) =  x1 +  x2 + 
p(n__a) = 
p(n__e) = 
p(n__i) = 
p(n__nil) = 
p(n__o) = 
p(n__u) = 
p(nil) = 
p(o) = 
p(tt) = 
p(u) = 

Following rules are strictly oriented:
isQid(n__i()) = 
> 
= tt()

Following rules are (at-least) weakly oriented:
U11(tt()) =  
>= 
=  tt()

U21(tt(),V2) =   V2 + 
>=  V2 + 
=  U22(isList(activate(V2)))

U22(tt()) =  
>= 
=  tt()

U31(tt()) =  
>= 
=  tt()

U41(tt(),V2) =   V2 + 
>=  V2 + 
=  U42(isNeList(activate(V2)))

U42(tt()) =  
>= 
=  tt()

U51(tt(),V2) =   V2 + 
>=  V2 + 
=  U52(isList(activate(V2)))

U52(tt()) =  
>= 
=  tt()

U61(tt()) =  
>= 
=  tt()

U71(tt(),P) =   P + 
>=  P + 
=  U72(isPal(activate(P)))

U72(tt()) =  
>= 
=  tt()

U81(tt()) =  
>= 
=  tt()

__(X1,X2) =   X1 +  X2 + 
>=  X1 +  X2 + 
=  n____(X1,X2)

a() =  
>= 
=  n__a()

activate(X) =   X + 
>=  X + 
=  X

activate(n____(X1,X2)) =   X1 +  X2 + 
>=  X1 +  X2 + 
=  __(X1,X2)

activate(n__a()) =  
>= 
=  a()

activate(n__e()) =  
>= 
=  e()

activate(n__i()) =  
>= 
=  i()

activate(n__nil()) =  
>= 
=  nil()

activate(n__o()) =  
>= 
=  o()

activate(n__u()) =  
>= 
=  u()

e() =  
>= 
=  n__e()

i() =  
>= 
=  n__i()

isList(V) =   V + 
>=  V + 
=  U11(isNeList(activate(V)))

isList(n____(V1,V2)) =   V1 +  V2 + 
>=  V1 +  V2 + 
=  U21(isList(activate(V1)),activate(V2))

isList(n__nil()) =  
>= 
=  tt()

isNeList(V) =   V + 
>=  V + 
=  U31(isQid(activate(V)))

isNeList(n____(V1,V2)) =   V1 +  V2 + 
>=  V1 +  V2 + 
=  U41(isList(activate(V1)),activate(V2))

isNeList(n____(V1,V2)) =   V1 +  V2 + 
>=  V1 +  V2 + 
=  U51(isNeList(activate(V1)),activate(V2))

isNePal(V) =   V + 
>=  V + 
=  U61(isQid(activate(V)))

isNePal(n____(I,__(P,I))) =   I +  P + 
>=  I +  P + 
=  U71(isQid(activate(I)),activate(P))

isPal(V) =   V + 
>=  V + 
=  U81(isNePal(activate(V)))

isPal(n__nil()) =  
>= 
=  tt()

isQid(n__a()) =  
>= 
=  tt()

isQid(n__e()) =  
>= 
=  tt()

isQid(n__o()) =  
>= 
=  tt()

isQid(n__u()) =  
>= 
=  tt()

nil() =  
>= 
=  n__nil()

o() =  
>= 
=  n__o()

u() =  
>= 
=  n__u()

Further, it can be verified that all rules not oriented are covered by the weightgap condition.
* Step 7: WeightGap WORST_CASE(?,O(n^1))
+ Considered Problem:
- Strict TRS:
__(X1,X2) -> n____(X1,X2)
a() -> n__a()
activate(X) -> X
activate(n__i()) -> i()
activate(n__nil()) -> nil()
activate(n__u()) -> u()
e() -> n__e()
isPal(V) -> U81(isNePal(activate(V)))
isQid(n__u()) -> tt()
o() -> n__o()
- Weak TRS:
U11(tt()) -> tt()
U21(tt(),V2) -> U22(isList(activate(V2)))
U22(tt()) -> tt()
U31(tt()) -> tt()
U41(tt(),V2) -> U42(isNeList(activate(V2)))
U42(tt()) -> tt()
U51(tt(),V2) -> U52(isList(activate(V2)))
U52(tt()) -> tt()
U61(tt()) -> tt()
U71(tt(),P) -> U72(isPal(activate(P)))
U72(tt()) -> tt()
U81(tt()) -> tt()
activate(n____(X1,X2)) -> __(X1,X2)
activate(n__a()) -> a()
activate(n__e()) -> e()
activate(n__o()) -> o()
i() -> n__i()
isList(V) -> U11(isNeList(activate(V)))
isList(n____(V1,V2)) -> U21(isList(activate(V1)),activate(V2))
isList(n__nil()) -> 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))
isNePal(V) -> U61(isQid(activate(V)))
isNePal(n____(I,__(P,I))) -> U71(isQid(activate(I)),activate(P))
isPal(n__nil()) -> tt()
isQid(n__a()) -> tt()
isQid(n__e()) -> tt()
isQid(n__i()) -> tt()
isQid(n__o()) -> tt()
nil() -> n__nil()
u() -> n__u()
- Signature:
{U11/1,U21/2,U22/1,U31/1,U41/2,U42/1,U51/2,U52/1,U61/1,U71/2,U72/1,U81/1,__/2,a/0,activate/1,e/0,i/0
,isList/1,isNeList/1,isNePal/1,isPal/1,isQid/1,nil/0,o/0,u/0} / {n____/2,n__a/0,n__e/0,n__i/0,n__nil/0
,n__o/0,n__u/0,tt/0}
- Obligation:
runtime complexity wrt. defined symbols {U11,U21,U22,U31,U41,U42,U51,U52,U61,U71,U72,U81,__,a,activate,e,i
,isList,isNeList,isNePal,isPal,isQid,nil,o,u} and constructors {n____,n__a,n__e,n__i,n__nil,n__o,n__u,tt}
+ Applied Processor:
WeightGap {wgDimension = 1, wgDegree = 1, wgKind = Algebraic, wgUArgs = UArgs, wgOn = WgOnAny}
+ Details:
The weightgap principle applies using the following nonconstant growth matrix-interpretation:
We apply a matrix interpretation of kind constructor based matrix interpretation:
The following argument positions are considered usable:
uargs(U11) = {1},
uargs(U21) = {1,2},
uargs(U22) = {1},
uargs(U31) = {1},
uargs(U41) = {1,2},
uargs(U42) = {1},
uargs(U51) = {1,2},
uargs(U52) = {1},
uargs(U61) = {1},
uargs(U71) = {1,2},
uargs(U72) = {1},
uargs(U81) = {1},
uargs(activate) = {1},
uargs(isList) = {1},
uargs(isNeList) = {1},
uargs(isNePal) = {1},
uargs(isPal) = {1},
uargs(isQid) = {1}

Following symbols are considered usable:
all
TcT has computed the following interpretation:
p(U11) =  x1 + 
p(U21) =  x1 +  x2 + 
p(U22) =  x1 + 
p(U31) =  x1 + 
p(U41) =  x1 +  x2 + 
p(U42) =  x1 + 
p(U51) =  x1 +  x2 + 
p(U52) =  x1 + 
p(U61) =  x1 + 
p(U71) =  x1 +  x2 + 
p(U72) =  x1 + 
p(U81) =  x1 + 
p(__) =  x1 +  x2 + 
p(a) = 
p(activate) =  x1 + 
p(e) = 
p(i) = 
p(isList) =  x1 + 
p(isNeList) =  x1 + 
p(isNePal) =  x1 + 
p(isPal) =  x1 + 
p(isQid) =  x1 + 
p(n____) =  x1 +  x2 + 
p(n__a) = 
p(n__e) = 
p(n__i) = 
p(n__nil) = 
p(n__o) = 
p(n__u) = 
p(nil) = 
p(o) = 
p(tt) = 
p(u) = 

Following rules are strictly oriented:
isQid(n__u()) = 
> 
= tt()

Following rules are (at-least) weakly oriented:
U11(tt()) =  
>= 
=  tt()

U21(tt(),V2) =   V2 + 
>=  V2 + 
=  U22(isList(activate(V2)))

U22(tt()) =  
>= 
=  tt()

U31(tt()) =  
>= 
=  tt()

U41(tt(),V2) =   V2 + 
>=  V2 + 
=  U42(isNeList(activate(V2)))

U42(tt()) =  
>= 
=  tt()

U51(tt(),V2) =   V2 + 
>=  V2 + 
=  U52(isList(activate(V2)))

U52(tt()) =  
>= 
=  tt()

U61(tt()) =  
>= 
=  tt()

U71(tt(),P) =   P + 
>=  P + 
=  U72(isPal(activate(P)))

U72(tt()) =  
>= 
=  tt()

U81(tt()) =  
>= 
=  tt()

__(X1,X2) =   X1 +  X2 + 
>=  X1 +  X2 + 
=  n____(X1,X2)

a() =  
>= 
=  n__a()

activate(X) =   X + 
>=  X + 
=  X

activate(n____(X1,X2)) =   X1 +  X2 + 
>=  X1 +  X2 + 
=  __(X1,X2)

activate(n__a()) =  
>= 
=  a()

activate(n__e()) =  
>= 
=  e()

activate(n__i()) =  
>= 
=  i()

activate(n__nil()) =  
>= 
=  nil()

activate(n__o()) =  
>= 
=  o()

activate(n__u()) =  
>= 
=  u()

e() =  
>= 
=  n__e()

i() =  
>= 
=  n__i()

isList(V) =   V + 
>=  V + 
=  U11(isNeList(activate(V)))

isList(n____(V1,V2)) =   V1 +  V2 + 
>=  V1 +  V2 + 
=  U21(isList(activate(V1)),activate(V2))

isList(n__nil()) =  
>= 
=  tt()

isNeList(V) =   V + 
>=  V + 
=  U31(isQid(activate(V)))

isNeList(n____(V1,V2)) =   V1 +  V2 + 
>=  V1 +  V2 + 
=  U41(isList(activate(V1)),activate(V2))

isNeList(n____(V1,V2)) =   V1 +  V2 + 
>=  V1 +  V2 + 
=  U51(isNeList(activate(V1)),activate(V2))

isNePal(V) =   V + 
>=  V + 
=  U61(isQid(activate(V)))

isNePal(n____(I,__(P,I))) =   I +  P + 
>=  I +  P + 
=  U71(isQid(activate(I)),activate(P))

isPal(V) =   V + 
>=  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()

nil() =  
>= 
=  n__nil()

o() =  
>= 
=  n__o()

u() =  
>= 
=  n__u()

Further, it can be verified that all rules not oriented are covered by the weightgap condition.
* Step 8: WeightGap WORST_CASE(?,O(n^1))
+ Considered Problem:
- Strict TRS:
__(X1,X2) -> n____(X1,X2)
a() -> n__a()
activate(X) -> X
activate(n__i()) -> i()
activate(n__nil()) -> nil()
activate(n__u()) -> u()
e() -> n__e()
isPal(V) -> U81(isNePal(activate(V)))
o() -> n__o()
- Weak TRS:
U11(tt()) -> tt()
U21(tt(),V2) -> U22(isList(activate(V2)))
U22(tt()) -> tt()
U31(tt()) -> tt()
U41(tt(),V2) -> U42(isNeList(activate(V2)))
U42(tt()) -> tt()
U51(tt(),V2) -> U52(isList(activate(V2)))
U52(tt()) -> tt()
U61(tt()) -> tt()
U71(tt(),P) -> U72(isPal(activate(P)))
U72(tt()) -> tt()
U81(tt()) -> tt()
activate(n____(X1,X2)) -> __(X1,X2)
activate(n__a()) -> a()
activate(n__e()) -> e()
activate(n__o()) -> o()
i() -> n__i()
isList(V) -> U11(isNeList(activate(V)))
isList(n____(V1,V2)) -> U21(isList(activate(V1)),activate(V2))
isList(n__nil()) -> 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))
isNePal(V) -> U61(isQid(activate(V)))
isNePal(n____(I,__(P,I))) -> U71(isQid(activate(I)),activate(P))
isPal(n__nil()) -> tt()
isQid(n__a()) -> tt()
isQid(n__e()) -> tt()
isQid(n__i()) -> tt()
isQid(n__o()) -> tt()
isQid(n__u()) -> tt()
nil() -> n__nil()
u() -> n__u()
- Signature:
{U11/1,U21/2,U22/1,U31/1,U41/2,U42/1,U51/2,U52/1,U61/1,U71/2,U72/1,U81/1,__/2,a/0,activate/1,e/0,i/0
,isList/1,isNeList/1,isNePal/1,isPal/1,isQid/1,nil/0,o/0,u/0} / {n____/2,n__a/0,n__e/0,n__i/0,n__nil/0
,n__o/0,n__u/0,tt/0}
- Obligation:
runtime complexity wrt. defined symbols {U11,U21,U22,U31,U41,U42,U51,U52,U61,U71,U72,U81,__,a,activate,e,i
,isList,isNeList,isNePal,isPal,isQid,nil,o,u} and constructors {n____,n__a,n__e,n__i,n__nil,n__o,n__u,tt}
+ Applied Processor:
WeightGap {wgDimension = 1, wgDegree = 1, wgKind = Algebraic, wgUArgs = UArgs, wgOn = WgOnAny}
+ Details:
The weightgap principle applies using the following nonconstant growth matrix-interpretation:
We apply a matrix interpretation of kind constructor based matrix interpretation:
The following argument positions are considered usable:
uargs(U11) = {1},
uargs(U21) = {1,2},
uargs(U22) = {1},
uargs(U31) = {1},
uargs(U41) = {1,2},
uargs(U42) = {1},
uargs(U51) = {1,2},
uargs(U52) = {1},
uargs(U61) = {1},
uargs(U71) = {1,2},
uargs(U72) = {1},
uargs(U81) = {1},
uargs(activate) = {1},
uargs(isList) = {1},
uargs(isNeList) = {1},
uargs(isNePal) = {1},
uargs(isPal) = {1},
uargs(isQid) = {1}

Following symbols are considered usable:
all
TcT has computed the following interpretation:
p(U11) =  x1 + 
p(U21) =  x1 +  x2 + 
p(U22) =  x1 + 
p(U31) =  x1 + 
p(U41) =  x1 +  x2 + 
p(U42) =  x1 + 
p(U51) =  x1 +  x2 + 
p(U52) =  x1 + 
p(U61) =  x1 + 
p(U71) =  x1 +  x2 + 
p(U72) =  x1 + 
p(U81) =  x1 + 
p(__) =  x1 +  x2 + 
p(a) = 
p(activate) =  x1 + 
p(e) = 
p(i) = 
p(isList) =  x1 + 
p(isNeList) =  x1 + 
p(isNePal) =  x1 + 
p(isPal) =  x1 + 
p(isQid) =  x1 + 
p(n____) =  x1 +  x2 + 
p(n__a) = 
p(n__e) = 
p(n__i) = 
p(n__nil) = 
p(n__o) = 
p(n__u) = 
p(nil) = 
p(o) = 
p(tt) = 
p(u) = 

Following rules are strictly oriented:
isPal(V) =  V + 
>  V + 
= U81(isNePal(activate(V)))

Following rules are (at-least) weakly oriented:
U11(tt()) =  
>= 
=  tt()

U21(tt(),V2) =   V2 + 
>=  V2 + 
=  U22(isList(activate(V2)))

U22(tt()) =  
>= 
=  tt()

U31(tt()) =  
>= 
=  tt()

U41(tt(),V2) =   V2 + 
>=  V2 + 
=  U42(isNeList(activate(V2)))

U42(tt()) =  
>= 
=  tt()

U51(tt(),V2) =   V2 + 
>=  V2 + 
=  U52(isList(activate(V2)))

U52(tt()) =  
>= 
=  tt()

U61(tt()) =  
>= 
=  tt()

U71(tt(),P) =   P + 
>=  P + 
=  U72(isPal(activate(P)))

U72(tt()) =  
>= 
=  tt()

U81(tt()) =  
>= 
=  tt()

__(X1,X2) =   X1 +  X2 + 
>=  X1 +  X2 + 
=  n____(X1,X2)

a() =  
>= 
=  n__a()

activate(X) =   X + 
>=  X + 
=  X

activate(n____(X1,X2)) =   X1 +  X2 + 
>=  X1 +  X2 + 
=  __(X1,X2)

activate(n__a()) =  
>= 
=  a()

activate(n__e()) =  
>= 
=  e()

activate(n__i()) =  
>= 
=  i()

activate(n__nil()) =  
>= 
=  nil()

activate(n__o()) =  
>= 
=  o()

activate(n__u()) =  
>= 
=  u()

e() =  
>= 
=  n__e()

i() =  
>= 
=  n__i()

isList(V) =   V + 
>=  V + 
=  U11(isNeList(activate(V)))

isList(n____(V1,V2)) =   V1 +  V2 + 
>=  V1 +  V2 + 
=  U21(isList(activate(V1)),activate(V2))

isList(n__nil()) =  
>= 
=  tt()

isNeList(V) =   V + 
>=  V + 
=  U31(isQid(activate(V)))

isNeList(n____(V1,V2)) =   V1 +  V2 + 
>=  V1 +  V2 + 
=  U41(isList(activate(V1)),activate(V2))

isNeList(n____(V1,V2)) =   V1 +  V2 + 
>=  V1 +  V2 + 
=  U51(isNeList(activate(V1)),activate(V2))

isNePal(V) =   V + 
>=  V + 
=  U61(isQid(activate(V)))

isNePal(n____(I,__(P,I))) =   I +  P + 
>=  I +  P + 
=  U71(isQid(activate(I)),activate(P))

isPal(n__nil()) =  
>= 
=  tt()

isQid(n__a()) =  
>= 
=  tt()

isQid(n__e()) =  
>= 
=  tt()

isQid(n__i()) =  
>= 
=  tt()

isQid(n__o()) =  
>= 
=  tt()

isQid(n__u()) =  
>= 
=  tt()

nil() =  
>= 
=  n__nil()

o() =  
>= 
=  n__o()

u() =  
>= 
=  n__u()

Further, it can be verified that all rules not oriented are covered by the weightgap condition.
* Step 9: WeightGap WORST_CASE(?,O(n^1))
+ Considered Problem:
- Strict TRS:
__(X1,X2) -> n____(X1,X2)
a() -> n__a()
activate(X) -> X
activate(n__i()) -> i()
activate(n__nil()) -> nil()
activate(n__u()) -> u()
e() -> n__e()
o() -> n__o()
- Weak TRS:
U11(tt()) -> tt()
U21(tt(),V2) -> U22(isList(activate(V2)))
U22(tt()) -> tt()
U31(tt()) -> tt()
U41(tt(),V2) -> U42(isNeList(activate(V2)))
U42(tt()) -> tt()
U51(tt(),V2) -> U52(isList(activate(V2)))
U52(tt()) -> tt()
U61(tt()) -> tt()
U71(tt(),P) -> U72(isPal(activate(P)))
U72(tt()) -> tt()
U81(tt()) -> tt()
activate(n____(X1,X2)) -> __(X1,X2)
activate(n__a()) -> a()
activate(n__e()) -> e()
activate(n__o()) -> o()
i() -> n__i()
isList(V) -> U11(isNeList(activate(V)))
isList(n____(V1,V2)) -> U21(isList(activate(V1)),activate(V2))
isList(n__nil()) -> 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))
isNePal(V) -> U61(isQid(activate(V)))
isNePal(n____(I,__(P,I))) -> U71(isQid(activate(I)),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()
nil() -> n__nil()
u() -> n__u()
- Signature:
{U11/1,U21/2,U22/1,U31/1,U41/2,U42/1,U51/2,U52/1,U61/1,U71/2,U72/1,U81/1,__/2,a/0,activate/1,e/0,i/0
,isList/1,isNeList/1,isNePal/1,isPal/1,isQid/1,nil/0,o/0,u/0} / {n____/2,n__a/0,n__e/0,n__i/0,n__nil/0
,n__o/0,n__u/0,tt/0}
- Obligation:
runtime complexity wrt. defined symbols {U11,U21,U22,U31,U41,U42,U51,U52,U61,U71,U72,U81,__,a,activate,e,i
,isList,isNeList,isNePal,isPal,isQid,nil,o,u} and constructors {n____,n__a,n__e,n__i,n__nil,n__o,n__u,tt}
+ Applied Processor:
WeightGap {wgDimension = 1, wgDegree = 1, wgKind = Algebraic, wgUArgs = UArgs, wgOn = WgOnAny}
+ Details:
The weightgap principle applies using the following nonconstant growth matrix-interpretation:
We apply a matrix interpretation of kind constructor based matrix interpretation:
The following argument positions are considered usable:
uargs(U11) = {1},
uargs(U21) = {1,2},
uargs(U22) = {1},
uargs(U31) = {1},
uargs(U41) = {1,2},
uargs(U42) = {1},
uargs(U51) = {1,2},
uargs(U52) = {1},
uargs(U61) = {1},
uargs(U71) = {1,2},
uargs(U72) = {1},
uargs(U81) = {1},
uargs(activate) = {1},
uargs(isList) = {1},
uargs(isNeList) = {1},
uargs(isNePal) = {1},
uargs(isPal) = {1},
uargs(isQid) = {1}

Following symbols are considered usable:
all
TcT has computed the following interpretation:
p(U11) =  x1 + 
p(U21) =  x1 +  x2 + 
p(U22) =  x1 + 
p(U31) =  x1 + 
p(U41) =  x1 +  x2 + 
p(U42) =  x1 + 
p(U51) =  x1 +  x2 + 
p(U52) =  x1 + 
p(U61) =  x1 + 
p(U71) =  x1 +  x2 + 
p(U72) =  x1 + 
p(U81) =  x1 + 
p(__) =  x1 +  x2 + 
p(a) = 
p(activate) =  x1 + 
p(e) = 
p(i) = 
p(isList) =  x1 + 
p(isNeList) =  x1 + 
p(isNePal) =  x1 + 
p(isPal) =  x1 + 
p(isQid) =  x1 + 
p(n____) =  x1 +  x2 + 
p(n__a) = 
p(n__e) = 
p(n__i) = 
p(n__nil) = 
p(n__o) = 
p(n__u) = 
p(nil) = 
p(o) = 
p(tt) = 
p(u) = 

Following rules are strictly oriented:
a() = 
> 
= n__a()

activate(X) =  X + 
>  X + 
= X

activate(n__i()) = 
> 
= i()

activate(n__nil()) = 
> 
= nil()

activate(n__u()) = 
> 
= u()

e() = 
> 
= n__e()

o() = 
> 
= n__o()

Following rules are (at-least) weakly oriented:
U11(tt()) =  
>= 
=  tt()

U21(tt(),V2) =   V2 + 
>=  V2 + 
=  U22(isList(activate(V2)))

U22(tt()) =  
>= 
=  tt()

U31(tt()) =  
>= 
=  tt()

U41(tt(),V2) =   V2 + 
>=  V2 + 
=  U42(isNeList(activate(V2)))

U42(tt()) =  
>= 
=  tt()

U51(tt(),V2) =   V2 + 
>=  V2 + 
=  U52(isList(activate(V2)))

U52(tt()) =  
>= 
=  tt()

U61(tt()) =  
>= 
=  tt()

U71(tt(),P) =   P + 
>=  P + 
=  U72(isPal(activate(P)))

U72(tt()) =  
>= 
=  tt()

U81(tt()) =  
>= 
=  tt()

__(X1,X2) =   X1 +  X2 + 
>=  X1 +  X2 + 
=  n____(X1,X2)

activate(n____(X1,X2)) =   X1 +  X2 + 
>=  X1 +  X2 + 
=  __(X1,X2)

activate(n__a()) =  
>= 
=  a()

activate(n__e()) =  
>= 
=  e()

activate(n__o()) =  
>= 
=  o()

i() =  
>= 
=  n__i()

isList(V) =   V + 
>=  V + 
=  U11(isNeList(activate(V)))

isList(n____(V1,V2)) =   V1 +  V2 + 
>=  V1 +  V2 + 
=  U21(isList(activate(V1)),activate(V2))

isList(n__nil()) =  
>= 
=  tt()

isNeList(V) =   V + 
>=  V + 
=  U31(isQid(activate(V)))

isNeList(n____(V1,V2)) =   V1 +  V2 + 
>=  V1 +  V2 + 
=  U41(isList(activate(V1)),activate(V2))

isNeList(n____(V1,V2)) =   V1 +  V2 + 
>=  V1 +  V2 + 
=  U51(isNeList(activate(V1)),activate(V2))

isNePal(V) =   V + 
>=  V + 
=  U61(isQid(activate(V)))

isNePal(n____(I,__(P,I))) =   I +  P + 
>=  I +  P + 
=  U71(isQid(activate(I)),activate(P))

isPal(V) =   V + 
>=  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()

nil() =  
>= 
=  n__nil()

u() =  
>= 
=  n__u()

Further, it can be verified that all rules not oriented are covered by the weightgap condition.
* Step 10: WeightGap WORST_CASE(?,O(n^1))
+ Considered Problem:
- Strict TRS:
__(X1,X2) -> n____(X1,X2)
- Weak TRS:
U11(tt()) -> tt()
U21(tt(),V2) -> U22(isList(activate(V2)))
U22(tt()) -> tt()
U31(tt()) -> tt()
U41(tt(),V2) -> U42(isNeList(activate(V2)))
U42(tt()) -> tt()
U51(tt(),V2) -> U52(isList(activate(V2)))
U52(tt()) -> tt()
U61(tt()) -> tt()
U71(tt(),P) -> U72(isPal(activate(P)))
U72(tt()) -> tt()
U81(tt()) -> tt()
a() -> n__a()
activate(X) -> X
activate(n____(X1,X2)) -> __(X1,X2)
activate(n__a()) -> a()
activate(n__e()) -> e()
activate(n__i()) -> i()
activate(n__nil()) -> nil()
activate(n__o()) -> o()
activate(n__u()) -> u()
e() -> n__e()
i() -> n__i()
isList(V) -> U11(isNeList(activate(V)))
isList(n____(V1,V2)) -> U21(isList(activate(V1)),activate(V2))
isList(n__nil()) -> 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))
isNePal(V) -> U61(isQid(activate(V)))
isNePal(n____(I,__(P,I))) -> U71(isQid(activate(I)),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()
nil() -> n__nil()
o() -> n__o()
u() -> n__u()
- Signature:
{U11/1,U21/2,U22/1,U31/1,U41/2,U42/1,U51/2,U52/1,U61/1,U71/2,U72/1,U81/1,__/2,a/0,activate/1,e/0,i/0
,isList/1,isNeList/1,isNePal/1,isPal/1,isQid/1,nil/0,o/0,u/0} / {n____/2,n__a/0,n__e/0,n__i/0,n__nil/0
,n__o/0,n__u/0,tt/0}
- Obligation:
runtime complexity wrt. defined symbols {U11,U21,U22,U31,U41,U42,U51,U52,U61,U71,U72,U81,__,a,activate,e,i
,isList,isNeList,isNePal,isPal,isQid,nil,o,u} and constructors {n____,n__a,n__e,n__i,n__nil,n__o,n__u,tt}
+ Applied Processor:
WeightGap {wgDimension = 1, wgDegree = 1, wgKind = Algebraic, wgUArgs = UArgs, wgOn = WgOnAny}
+ Details:
The weightgap principle applies using the following nonconstant growth matrix-interpretation:
We apply a matrix interpretation of kind constructor based matrix interpretation:
The following argument positions are considered usable:
uargs(U11) = {1},
uargs(U21) = {1,2},
uargs(U22) = {1},
uargs(U31) = {1},
uargs(U41) = {1,2},
uargs(U42) = {1},
uargs(U51) = {1,2},
uargs(U52) = {1},
uargs(U61) = {1},
uargs(U71) = {1,2},
uargs(U72) = {1},
uargs(U81) = {1},
uargs(activate) = {1},
uargs(isList) = {1},
uargs(isNeList) = {1},
uargs(isNePal) = {1},
uargs(isPal) = {1},
uargs(isQid) = {1}

Following symbols are considered usable:
all
TcT has computed the following interpretation:
p(U11) =  x1 + 
p(U21) =  x1 +  x2 + 
p(U22) =  x1 + 
p(U31) =  x1 + 
p(U41) =  x1 +  x2 + 
p(U42) =  x1 + 
p(U51) =  x1 +  x2 + 
p(U52) =  x1 + 
p(U61) =  x1 + 
p(U71) =  x1 +  x2 + 
p(U72) =  x1 + 
p(U81) =  x1 + 
p(__) =  x1 +  x2 + 
p(a) = 
p(activate) =  x1 + 
p(e) = 
p(i) = 
p(isList) =  x1 + 
p(isNeList) =  x1 + 
p(isNePal) =  x1 + 
p(isPal) =  x1 + 
p(isQid) =  x1 + 
p(n____) =  x1 +  x2 + 
p(n__a) = 
p(n__e) = 
p(n__i) = 
p(n__nil) = 
p(n__o) = 
p(n__u) = 
p(nil) = 
p(o) = 
p(tt) = 
p(u) = 

Following rules are strictly oriented:
__(X1,X2) =  X1 +  X2 + 
>  X1 +  X2 + 
= n____(X1,X2)

Following rules are (at-least) weakly oriented:
U11(tt()) =  
>= 
=  tt()

U21(tt(),V2) =   V2 + 
>=  V2 + 
=  U22(isList(activate(V2)))

U22(tt()) =  
>= 
=  tt()

U31(tt()) =  
>= 
=  tt()

U41(tt(),V2) =   V2 + 
>=  V2 + 
=  U42(isNeList(activate(V2)))

U42(tt()) =  
>= 
=  tt()

U51(tt(),V2) =   V2 + 
>=  V2 + 
=  U52(isList(activate(V2)))

U52(tt()) =  
>= 
=  tt()

U61(tt()) =  
>= 
=  tt()

U71(tt(),P) =   P + 
>=  P + 
=  U72(isPal(activate(P)))

U72(tt()) =  
>= 
=  tt()

U81(tt()) =  
>= 
=  tt()

a() =  
>= 
=  n__a()

activate(X) =   X + 
>=  X + 
=  X

activate(n____(X1,X2)) =   X1 +  X2 + 
>=  X1 +  X2 + 
=  __(X1,X2)

activate(n__a()) =  
>= 
=  a()

activate(n__e()) =  
>= 
=  e()

activate(n__i()) =  
>= 
=  i()

activate(n__nil()) =  
>= 
=  nil()

activate(n__o()) =  
>= 
=  o()

activate(n__u()) =  
>= 
=  u()

e() =  
>= 
=  n__e()

i() =  
>= 
=  n__i()

isList(V) =   V + 
>=  V + 
=  U11(isNeList(activate(V)))

isList(n____(V1,V2)) =   V1 +  V2 + 
>=  V1 +  V2 + 
=  U21(isList(activate(V1)),activate(V2))

isList(n__nil()) =  
>= 
=  tt()

isNeList(V) =   V + 
>=  V + 
=  U31(isQid(activate(V)))

isNeList(n____(V1,V2)) =   V1 +  V2 + 
>=  V1 +  V2 + 
=  U41(isList(activate(V1)),activate(V2))

isNeList(n____(V1,V2)) =   V1 +  V2 + 
>=  V1 +  V2 + 
=  U51(isNeList(activate(V1)),activate(V2))

isNePal(V) =   V + 
>=  V + 
=  U61(isQid(activate(V)))

isNePal(n____(I,__(P,I))) =   I +  P + 
>=  I +  P + 
=  U71(isQid(activate(I)),activate(P))

isPal(V) =   V + 
>=  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()

nil() =  
>= 
=  n__nil()

o() =  
>= 
=  n__o()

u() =  
>= 
=  n__u()

Further, it can be verified that all rules not oriented are covered by the weightgap condition.
* Step 11: EmptyProcessor WORST_CASE(?,O(1))
+ Considered Problem:
- Weak TRS:
U11(tt()) -> tt()
U21(tt(),V2) -> U22(isList(activate(V2)))
U22(tt()) -> tt()
U31(tt()) -> tt()
U41(tt(),V2) -> U42(isNeList(activate(V2)))
U42(tt()) -> tt()
U51(tt(),V2) -> U52(isList(activate(V2)))
U52(tt()) -> tt()
U61(tt()) -> tt()
U71(tt(),P) -> U72(isPal(activate(P)))
U72(tt()) -> tt()
U81(tt()) -> tt()
__(X1,X2) -> n____(X1,X2)
a() -> n__a()
activate(X) -> X
activate(n____(X1,X2)) -> __(X1,X2)
activate(n__a()) -> a()
activate(n__e()) -> e()
activate(n__i()) -> i()
activate(n__nil()) -> nil()
activate(n__o()) -> o()
activate(n__u()) -> u()
e() -> n__e()
i() -> n__i()
isList(V) -> U11(isNeList(activate(V)))
isList(n____(V1,V2)) -> U21(isList(activate(V1)),activate(V2))
isList(n__nil()) -> 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))
isNePal(V) -> U61(isQid(activate(V)))
isNePal(n____(I,__(P,I))) -> U71(isQid(activate(I)),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()
nil() -> n__nil()
o() -> n__o()
u() -> n__u()
- Signature:
{U11/1,U21/2,U22/1,U31/1,U41/2,U42/1,U51/2,U52/1,U61/1,U71/2,U72/1,U81/1,__/2,a/0,activate/1,e/0,i/0
,isList/1,isNeList/1,isNePal/1,isPal/1,isQid/1,nil/0,o/0,u/0} / {n____/2,n__a/0,n__e/0,n__i/0,n__nil/0
,n__o/0,n__u/0,tt/0}
- Obligation:
runtime complexity wrt. defined symbols {U11,U21,U22,U31,U41,U42,U51,U52,U61,U71,U72,U81,__,a,activate,e,i
,isList,isNeList,isNePal,isPal,isQid,nil,o,u} and constructors {n____,n__a,n__e,n__i,n__nil,n__o,n__u,tt}
+ Applied Processor:
EmptyProcessor
+ Details:
The problem is already closed. The intended complexity is O(1).

WORST_CASE(?,O(n^1))
```