*** 1 Progress [(O(1),O(n^1))] ***
Considered Problem:
Strict DP Rules:
Strict TRS Rules:
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()
__(X,nil()) -> X
__(X1,X2) -> n____(X1,X2)
__(__(X,Y),Z) -> __(X,__(Y,Z))
__(nil(),X) -> X
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()
Weak DP Rules:
Weak TRS Rules:
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:
Full
basic terms: {U11,U21,U22,U31,U41,U42,U51,U52,U61,U71,U72,U81,__,a,activate,e,i,isList,isNeList,isNePal,isPal,isQid,nil,o,u}/{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}
Proof:
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(__) = {2},
uargs(activate) = {1},
uargs(isList) = {1},
uargs(isNeList) = {1},
uargs(isNePal) = {1},
uargs(isPal) = {1},
uargs(isQid) = {1},
uargs(n____) = {2}
Following symbols are considered usable:
{}
TcT has computed the following interpretation:
p(U11) = [1] x1 + [3]
p(U21) = [1] x1 + [1] x2 + [0]
p(U22) = [1] x1 + [0]
p(U31) = [1] x1 + [2]
p(U41) = [1] x1 + [1] x2 + [0]
p(U42) = [1] x1 + [0]
p(U51) = [1] x1 + [1] x2 + [4]
p(U52) = [1] x1 + [0]
p(U61) = [1] x1 + [0]
p(U71) = [1] x1 + [1] x2 + [0]
p(U72) = [1] x1 + [0]
p(U81) = [1] x1 + [0]
p(__) = [1] x1 + [1] x2 + [1]
p(a) = [0]
p(activate) = [1] x1 + [0]
p(e) = [0]
p(i) = [0]
p(isList) = [1] x1 + [0]
p(isNeList) = [1] x1 + [0]
p(isNePal) = [1] x1 + [0]
p(isPal) = [1] x1 + [0]
p(isQid) = [1] x1 + [0]
p(n____) = [1] x1 + [1] x2 + [0]
p(n__a) = [0]
p(n__e) = [7]
p(n__i) = [0]
p(n__nil) = [0]
p(n__o) = [0]
p(n__u) = [0]
p(nil) = [0]
p(o) = [0]
p(tt) = [0]
p(u) = [0]
Following rules are strictly oriented:
U11(tt()) = [3]
> [0]
= tt()
U31(tt()) = [2]
> [0]
= tt()
U51(tt(),V2) = [1] V2 + [4]
> [1] V2 + [0]
= U52(isList(activate(V2)))
__(X,nil()) = [1] X + [1]
> [1] X + [0]
= X
__(X1,X2) = [1] X1 + [1] X2 + [1]
> [1] X1 + [1] X2 + [0]
= n____(X1,X2)
__(nil(),X) = [1] X + [1]
> [1] X + [0]
= X
activate(n__e()) = [7]
> [0]
= e()
isNePal(n____(I,__(P,I))) = [2] I + [1] P + [1]
> [1] I + [1] P + [0]
= U71(isQid(activate(I))
,activate(P))
isQid(n__e()) = [7]
> [0]
= tt()
Following rules are (at-least) weakly oriented:
U21(tt(),V2) = [1] V2 + [0]
>= [1] V2 + [0]
= U22(isList(activate(V2)))
U22(tt()) = [0]
>= [0]
= tt()
U41(tt(),V2) = [1] V2 + [0]
>= [1] V2 + [0]
= U42(isNeList(activate(V2)))
U42(tt()) = [0]
>= [0]
= tt()
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()
U81(tt()) = [0]
>= [0]
= tt()
__(__(X,Y),Z) = [1] X + [1] Y + [1] Z + [2]
>= [1] X + [1] Y + [1] Z + [2]
= __(X,__(Y,Z))
a() = [0]
>= [0]
= n__a()
activate(X) = [1] X + [0]
>= [1] X + [0]
= X
activate(n____(X1,X2)) = [1] X1 + [1] X2 + [0]
>= [1] X1 + [1] X2 + [1]
= __(X1,X2)
activate(n__a()) = [0]
>= [0]
= a()
activate(n__i()) = [0]
>= [0]
= i()
activate(n__nil()) = [0]
>= [0]
= nil()
activate(n__o()) = [0]
>= [0]
= o()
activate(n__u()) = [0]
>= [0]
= u()
e() = [0]
>= [7]
= n__e()
i() = [0]
>= [0]
= n__i()
isList(V) = [1] V + [0]
>= [1] V + [3]
= U11(isNeList(activate(V)))
isList(n____(V1,V2)) = [1] V1 + [1] V2 + [0]
>= [1] V1 + [1] V2 + [0]
= U21(isList(activate(V1))
,activate(V2))
isList(n__nil()) = [0]
>= [0]
= tt()
isNeList(V) = [1] V + [0]
>= [1] V + [2]
= U31(isQid(activate(V)))
isNeList(n____(V1,V2)) = [1] V1 + [1] V2 + [0]
>= [1] V1 + [1] V2 + [0]
= U41(isList(activate(V1))
,activate(V2))
isNeList(n____(V1,V2)) = [1] V1 + [1] V2 + [0]
>= [1] V1 + [1] V2 + [4]
= U51(isNeList(activate(V1))
,activate(V2))
isNePal(V) = [1] V + [0]
>= [1] V + [0]
= U61(isQid(activate(V)))
isPal(V) = [1] V + [0]
>= [1] V + [0]
= U81(isNePal(activate(V)))
isPal(n__nil()) = [0]
>= [0]
= tt()
isQid(n__a()) = [0]
>= [0]
= tt()
isQid(n__i()) = [0]
>= [0]
= tt()
isQid(n__o()) = [0]
>= [0]
= tt()
isQid(n__u()) = [0]
>= [0]
= tt()
nil() = [0]
>= [0]
= n__nil()
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.
*** 1.1 Progress [(O(1),O(n^1))] ***
Considered Problem:
Strict DP Rules:
Strict TRS Rules:
U21(tt(),V2) -> U22(isList(activate(V2)))
U22(tt()) -> tt()
U41(tt(),V2) -> U42(isNeList(activate(V2)))
U42(tt()) -> tt()
U52(tt()) -> tt()
U61(tt()) -> tt()
U71(tt(),P) -> U72(isPal(activate(P)))
U72(tt()) -> tt()
U81(tt()) -> tt()
__(__(X,Y),Z) -> __(X,__(Y,Z))
a() -> n__a()
activate(X) -> X
activate(n____(X1,X2)) -> __(X1,X2)
activate(n__a()) -> a()
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)))
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()
nil() -> n__nil()
o() -> n__o()
u() -> n__u()
Weak DP Rules:
Weak TRS Rules:
U11(tt()) -> tt()
U31(tt()) -> tt()
U51(tt(),V2) -> U52(isList(activate(V2)))
__(X,nil()) -> X
__(X1,X2) -> n____(X1,X2)
__(nil(),X) -> X
activate(n__e()) -> e()
isNePal(n____(I,__(P,I))) -> U71(isQid(activate(I)),activate(P))
isQid(n__e()) -> tt()
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:
Full
basic terms: {U11,U21,U22,U31,U41,U42,U51,U52,U61,U71,U72,U81,__,a,activate,e,i,isList,isNeList,isNePal,isPal,isQid,nil,o,u}/{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}
Proof:
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(__) = {2},
uargs(activate) = {1},
uargs(isList) = {1},
uargs(isNeList) = {1},
uargs(isNePal) = {1},
uargs(isPal) = {1},
uargs(isQid) = {1},
uargs(n____) = {2}
Following symbols are considered usable:
{}
TcT has computed the following interpretation:
p(U11) = [1] x1 + [0]
p(U21) = [1] x1 + [1] x2 + [0]
p(U22) = [1] x1 + [0]
p(U31) = [1] x1 + [0]
p(U41) = [1] x1 + [1] x2 + [0]
p(U42) = [1] x1 + [0]
p(U51) = [1] x1 + [1] x2 + [7]
p(U52) = [1] x1 + [7]
p(U61) = [1] x1 + [7]
p(U71) = [1] x1 + [1] x2 + [0]
p(U72) = [1] x1 + [0]
p(U81) = [1] x1 + [0]
p(__) = [1] x1 + [1] x2 + [0]
p(a) = [0]
p(activate) = [1] x1 + [0]
p(e) = [0]
p(i) = [0]
p(isList) = [1] x1 + [0]
p(isNeList) = [1] x1 + [0]
p(isNePal) = [1] x1 + [0]
p(isPal) = [1] x1 + [0]
p(isQid) = [1] x1 + [0]
p(n____) = [1] x1 + [1] x2 + [0]
p(n__a) = [5]
p(n__e) = [0]
p(n__i) = [0]
p(n__nil) = [0]
p(n__o) = [0]
p(n__u) = [0]
p(nil) = [0]
p(o) = [0]
p(tt) = [0]
p(u) = [1]
Following rules are strictly oriented:
U52(tt()) = [7]
> [0]
= tt()
U61(tt()) = [7]
> [0]
= tt()
activate(n__a()) = [5]
> [0]
= a()
isQid(n__a()) = [5]
> [0]
= tt()
u() = [1]
> [0]
= n__u()
Following rules are (at-least) weakly oriented:
U11(tt()) = [0]
>= [0]
= tt()
U21(tt(),V2) = [1] V2 + [0]
>= [1] V2 + [0]
= U22(isList(activate(V2)))
U22(tt()) = [0]
>= [0]
= tt()
U31(tt()) = [0]
>= [0]
= tt()
U41(tt(),V2) = [1] V2 + [0]
>= [1] V2 + [0]
= U42(isNeList(activate(V2)))
U42(tt()) = [0]
>= [0]
= tt()
U51(tt(),V2) = [1] V2 + [7]
>= [1] V2 + [7]
= U52(isList(activate(V2)))
U71(tt(),P) = [1] P + [0]
>= [1] P + [0]
= U72(isPal(activate(P)))
U72(tt()) = [0]
>= [0]
= tt()
U81(tt()) = [0]
>= [0]
= tt()
__(X,nil()) = [1] X + [0]
>= [1] X + [0]
= X
__(X1,X2) = [1] X1 + [1] X2 + [0]
>= [1] X1 + [1] X2 + [0]
= n____(X1,X2)
__(__(X,Y),Z) = [1] X + [1] Y + [1] Z + [0]
>= [1] X + [1] Y + [1] Z + [0]
= __(X,__(Y,Z))
__(nil(),X) = [1] X + [0]
>= [1] X + [0]
= X
a() = [0]
>= [5]
= n__a()
activate(X) = [1] X + [0]
>= [1] X + [0]
= X
activate(n____(X1,X2)) = [1] X1 + [1] X2 + [0]
>= [1] X1 + [1] X2 + [0]
= __(X1,X2)
activate(n__e()) = [0]
>= [0]
= e()
activate(n__i()) = [0]
>= [0]
= i()
activate(n__nil()) = [0]
>= [0]
= nil()
activate(n__o()) = [0]
>= [0]
= o()
activate(n__u()) = [0]
>= [1]
= u()
e() = [0]
>= [0]
= n__e()
i() = [0]
>= [0]
= n__i()
isList(V) = [1] V + [0]
>= [1] V + [0]
= U11(isNeList(activate(V)))
isList(n____(V1,V2)) = [1] V1 + [1] V2 + [0]
>= [1] V1 + [1] V2 + [0]
= U21(isList(activate(V1))
,activate(V2))
isList(n__nil()) = [0]
>= [0]
= tt()
isNeList(V) = [1] V + [0]
>= [1] V + [0]
= U31(isQid(activate(V)))
isNeList(n____(V1,V2)) = [1] V1 + [1] V2 + [0]
>= [1] V1 + [1] V2 + [0]
= U41(isList(activate(V1))
,activate(V2))
isNeList(n____(V1,V2)) = [1] V1 + [1] V2 + [0]
>= [1] V1 + [1] V2 + [7]
= U51(isNeList(activate(V1))
,activate(V2))
isNePal(V) = [1] V + [0]
>= [1] V + [7]
= U61(isQid(activate(V)))
isNePal(n____(I,__(P,I))) = [2] I + [1] P + [0]
>= [1] I + [1] P + [0]
= U71(isQid(activate(I))
,activate(P))
isPal(V) = [1] V + [0]
>= [1] V + [0]
= U81(isNePal(activate(V)))
isPal(n__nil()) = [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()
nil() = [0]
>= [0]
= n__nil()
o() = [0]
>= [0]
= n__o()
Further, it can be verified that all rules not oriented are covered by the weightgap condition.
*** 1.1.1 Progress [(O(1),O(n^1))] ***
Considered Problem:
Strict DP Rules:
Strict TRS Rules:
U21(tt(),V2) -> U22(isList(activate(V2)))
U22(tt()) -> tt()
U41(tt(),V2) -> U42(isNeList(activate(V2)))
U42(tt()) -> tt()
U71(tt(),P) -> U72(isPal(activate(P)))
U72(tt()) -> tt()
U81(tt()) -> tt()
__(__(X,Y),Z) -> __(X,__(Y,Z))
a() -> n__a()
activate(X) -> X
activate(n____(X1,X2)) -> __(X1,X2)
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)))
isPal(V) -> U81(isNePal(activate(V)))
isPal(n__nil()) -> tt()
isQid(n__i()) -> tt()
isQid(n__o()) -> tt()
isQid(n__u()) -> tt()
nil() -> n__nil()
o() -> n__o()
Weak DP Rules:
Weak TRS Rules:
U11(tt()) -> tt()
U31(tt()) -> tt()
U51(tt(),V2) -> U52(isList(activate(V2)))
U52(tt()) -> tt()
U61(tt()) -> tt()
__(X,nil()) -> X
__(X1,X2) -> n____(X1,X2)
__(nil(),X) -> X
activate(n__a()) -> a()
activate(n__e()) -> e()
isNePal(n____(I,__(P,I))) -> U71(isQid(activate(I)),activate(P))
isQid(n__a()) -> tt()
isQid(n__e()) -> 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:
Full
basic terms: {U11,U21,U22,U31,U41,U42,U51,U52,U61,U71,U72,U81,__,a,activate,e,i,isList,isNeList,isNePal,isPal,isQid,nil,o,u}/{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}
Proof:
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(__) = {2},
uargs(activate) = {1},
uargs(isList) = {1},
uargs(isNeList) = {1},
uargs(isNePal) = {1},
uargs(isPal) = {1},
uargs(isQid) = {1},
uargs(n____) = {2}
Following symbols are considered usable:
{}
TcT has computed the following interpretation:
p(U11) = [1] x1 + [0]
p(U21) = [1] x1 + [1] x2 + [0]
p(U22) = [1] x1 + [0]
p(U31) = [1] x1 + [0]
p(U41) = [1] x1 + [1] x2 + [4]
p(U42) = [1] x1 + [0]
p(U51) = [1] x1 + [1] x2 + [1]
p(U52) = [1] x1 + [0]
p(U61) = [1] x1 + [0]
p(U71) = [1] x1 + [1] x2 + [0]
p(U72) = [1] x1 + [0]
p(U81) = [1] x1 + [0]
p(__) = [1] x1 + [1] x2 + [0]
p(a) = [0]
p(activate) = [1] x1 + [0]
p(e) = [0]
p(i) = [0]
p(isList) = [1] x1 + [5]
p(isNeList) = [1] x1 + [5]
p(isNePal) = [1] x1 + [4]
p(isPal) = [1] x1 + [0]
p(isQid) = [1] x1 + [4]
p(n____) = [1] x1 + [1] x2 + [0]
p(n__a) = [0]
p(n__e) = [0]
p(n__i) = [0]
p(n__nil) = [0]
p(n__o) = [4]
p(n__u) = [0]
p(nil) = [0]
p(o) = [0]
p(tt) = [4]
p(u) = [0]
Following rules are strictly oriented:
U41(tt(),V2) = [1] V2 + [8]
> [1] V2 + [5]
= U42(isNeList(activate(V2)))
U71(tt(),P) = [1] P + [4]
> [1] P + [0]
= U72(isPal(activate(P)))
activate(n__o()) = [4]
> [0]
= o()
isList(n__nil()) = [5]
> [4]
= tt()
isNeList(V) = [1] V + [5]
> [1] V + [4]
= U31(isQid(activate(V)))
isQid(n__o()) = [8]
> [4]
= tt()
Following rules are (at-least) weakly oriented:
U11(tt()) = [4]
>= [4]
= tt()
U21(tt(),V2) = [1] V2 + [4]
>= [1] V2 + [5]
= U22(isList(activate(V2)))
U22(tt()) = [4]
>= [4]
= tt()
U31(tt()) = [4]
>= [4]
= tt()
U42(tt()) = [4]
>= [4]
= tt()
U51(tt(),V2) = [1] V2 + [5]
>= [1] V2 + [5]
= U52(isList(activate(V2)))
U52(tt()) = [4]
>= [4]
= tt()
U61(tt()) = [4]
>= [4]
= tt()
U72(tt()) = [4]
>= [4]
= tt()
U81(tt()) = [4]
>= [4]
= tt()
__(X,nil()) = [1] X + [0]
>= [1] X + [0]
= X
__(X1,X2) = [1] X1 + [1] X2 + [0]
>= [1] X1 + [1] X2 + [0]
= n____(X1,X2)
__(__(X,Y),Z) = [1] X + [1] Y + [1] Z + [0]
>= [1] X + [1] Y + [1] Z + [0]
= __(X,__(Y,Z))
__(nil(),X) = [1] X + [0]
>= [1] X + [0]
= X
a() = [0]
>= [0]
= n__a()
activate(X) = [1] X + [0]
>= [1] X + [0]
= X
activate(n____(X1,X2)) = [1] X1 + [1] X2 + [0]
>= [1] X1 + [1] X2 + [0]
= __(X1,X2)
activate(n__a()) = [0]
>= [0]
= a()
activate(n__e()) = [0]
>= [0]
= e()
activate(n__i()) = [0]
>= [0]
= i()
activate(n__nil()) = [0]
>= [0]
= nil()
activate(n__u()) = [0]
>= [0]
= u()
e() = [0]
>= [0]
= n__e()
i() = [0]
>= [0]
= n__i()
isList(V) = [1] V + [5]
>= [1] V + [5]
= U11(isNeList(activate(V)))
isList(n____(V1,V2)) = [1] V1 + [1] V2 + [5]
>= [1] V1 + [1] V2 + [5]
= U21(isList(activate(V1))
,activate(V2))
isNeList(n____(V1,V2)) = [1] V1 + [1] V2 + [5]
>= [1] V1 + [1] V2 + [9]
= U41(isList(activate(V1))
,activate(V2))
isNeList(n____(V1,V2)) = [1] V1 + [1] V2 + [5]
>= [1] V1 + [1] V2 + [6]
= U51(isNeList(activate(V1))
,activate(V2))
isNePal(V) = [1] V + [4]
>= [1] V + [4]
= U61(isQid(activate(V)))
isNePal(n____(I,__(P,I))) = [2] I + [1] P + [4]
>= [1] I + [1] P + [4]
= U71(isQid(activate(I))
,activate(P))
isPal(V) = [1] V + [0]
>= [1] V + [4]
= U81(isNePal(activate(V)))
isPal(n__nil()) = [0]
>= [4]
= tt()
isQid(n__a()) = [4]
>= [4]
= tt()
isQid(n__e()) = [4]
>= [4]
= tt()
isQid(n__i()) = [4]
>= [4]
= tt()
isQid(n__u()) = [4]
>= [4]
= tt()
nil() = [0]
>= [0]
= n__nil()
o() = [0]
>= [4]
= n__o()
u() = [0]
>= [0]
= n__u()
Further, it can be verified that all rules not oriented are covered by the weightgap condition.
*** 1.1.1.1 Progress [(O(1),O(n^1))] ***
Considered Problem:
Strict DP Rules:
Strict TRS Rules:
U21(tt(),V2) -> U22(isList(activate(V2)))
U22(tt()) -> tt()
U42(tt()) -> tt()
U72(tt()) -> tt()
U81(tt()) -> tt()
__(__(X,Y),Z) -> __(X,__(Y,Z))
a() -> n__a()
activate(X) -> X
activate(n____(X1,X2)) -> __(X1,X2)
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____(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(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 DP Rules:
Weak TRS Rules:
U11(tt()) -> tt()
U31(tt()) -> tt()
U41(tt(),V2) -> U42(isNeList(activate(V2)))
U51(tt(),V2) -> U52(isList(activate(V2)))
U52(tt()) -> tt()
U61(tt()) -> tt()
U71(tt(),P) -> U72(isPal(activate(P)))
__(X,nil()) -> X
__(X1,X2) -> n____(X1,X2)
__(nil(),X) -> X
activate(n__a()) -> a()
activate(n__e()) -> e()
activate(n__o()) -> o()
isList(n__nil()) -> tt()
isNeList(V) -> U31(isQid(activate(V)))
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:
Full
basic terms: {U11,U21,U22,U31,U41,U42,U51,U52,U61,U71,U72,U81,__,a,activate,e,i,isList,isNeList,isNePal,isPal,isQid,nil,o,u}/{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}
Proof:
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(__) = {2},
uargs(activate) = {1},
uargs(isList) = {1},
uargs(isNeList) = {1},
uargs(isNePal) = {1},
uargs(isPal) = {1},
uargs(isQid) = {1},
uargs(n____) = {2}
Following symbols are considered usable:
{}
TcT has computed the following interpretation:
p(U11) = [1] x1 + [0]
p(U21) = [1] x1 + [1] x2 + [5]
p(U22) = [1] x1 + [0]
p(U31) = [1] x1 + [0]
p(U41) = [1] x1 + [1] x2 + [4]
p(U42) = [1] x1 + [2]
p(U51) = [1] x1 + [1] x2 + [0]
p(U52) = [1] x1 + [0]
p(U61) = [1] x1 + [0]
p(U71) = [1] x1 + [1] x2 + [3]
p(U72) = [1] x1 + [5]
p(U81) = [1] x1 + [0]
p(__) = [1] x1 + [1] x2 + [0]
p(a) = [0]
p(activate) = [1] x1 + [0]
p(e) = [7]
p(i) = [1]
p(isList) = [1] x1 + [2]
p(isNeList) = [1] x1 + [4]
p(isNePal) = [1] x1 + [7]
p(isPal) = [1] x1 + [0]
p(isQid) = [1] x1 + [4]
p(n____) = [1] x1 + [1] x2 + [0]
p(n__a) = [0]
p(n__e) = [7]
p(n__i) = [0]
p(n__nil) = [0]
p(n__o) = [4]
p(n__u) = [2]
p(nil) = [0]
p(o) = [4]
p(tt) = [2]
p(u) = [5]
Following rules are strictly oriented:
U21(tt(),V2) = [1] V2 + [7]
> [1] V2 + [2]
= U22(isList(activate(V2)))
U42(tt()) = [4]
> [2]
= tt()
U72(tt()) = [7]
> [2]
= tt()
i() = [1]
> [0]
= n__i()
isNePal(V) = [1] V + [7]
> [1] V + [4]
= U61(isQid(activate(V)))
isQid(n__i()) = [4]
> [2]
= tt()
isQid(n__u()) = [6]
> [2]
= tt()
Following rules are (at-least) weakly oriented:
U11(tt()) = [2]
>= [2]
= tt()
U22(tt()) = [2]
>= [2]
= tt()
U31(tt()) = [2]
>= [2]
= tt()
U41(tt(),V2) = [1] V2 + [6]
>= [1] V2 + [6]
= U42(isNeList(activate(V2)))
U51(tt(),V2) = [1] V2 + [2]
>= [1] V2 + [2]
= U52(isList(activate(V2)))
U52(tt()) = [2]
>= [2]
= tt()
U61(tt()) = [2]
>= [2]
= tt()
U71(tt(),P) = [1] P + [5]
>= [1] P + [5]
= U72(isPal(activate(P)))
U81(tt()) = [2]
>= [2]
= tt()
__(X,nil()) = [1] X + [0]
>= [1] X + [0]
= X
__(X1,X2) = [1] X1 + [1] X2 + [0]
>= [1] X1 + [1] X2 + [0]
= n____(X1,X2)
__(__(X,Y),Z) = [1] X + [1] Y + [1] Z + [0]
>= [1] X + [1] Y + [1] Z + [0]
= __(X,__(Y,Z))
__(nil(),X) = [1] X + [0]
>= [1] X + [0]
= X
a() = [0]
>= [0]
= n__a()
activate(X) = [1] X + [0]
>= [1] X + [0]
= X
activate(n____(X1,X2)) = [1] X1 + [1] X2 + [0]
>= [1] X1 + [1] X2 + [0]
= __(X1,X2)
activate(n__a()) = [0]
>= [0]
= a()
activate(n__e()) = [7]
>= [7]
= e()
activate(n__i()) = [0]
>= [1]
= i()
activate(n__nil()) = [0]
>= [0]
= nil()
activate(n__o()) = [4]
>= [4]
= o()
activate(n__u()) = [2]
>= [5]
= u()
e() = [7]
>= [7]
= n__e()
isList(V) = [1] V + [2]
>= [1] V + [4]
= U11(isNeList(activate(V)))
isList(n____(V1,V2)) = [1] V1 + [1] V2 + [2]
>= [1] V1 + [1] V2 + [7]
= U21(isList(activate(V1))
,activate(V2))
isList(n__nil()) = [2]
>= [2]
= tt()
isNeList(V) = [1] V + [4]
>= [1] V + [4]
= U31(isQid(activate(V)))
isNeList(n____(V1,V2)) = [1] V1 + [1] V2 + [4]
>= [1] V1 + [1] V2 + [6]
= U41(isList(activate(V1))
,activate(V2))
isNeList(n____(V1,V2)) = [1] V1 + [1] V2 + [4]
>= [1] V1 + [1] V2 + [4]
= U51(isNeList(activate(V1))
,activate(V2))
isNePal(n____(I,__(P,I))) = [2] I + [1] P + [7]
>= [1] I + [1] P + [7]
= U71(isQid(activate(I))
,activate(P))
isPal(V) = [1] V + [0]
>= [1] V + [7]
= U81(isNePal(activate(V)))
isPal(n__nil()) = [0]
>= [2]
= tt()
isQid(n__a()) = [4]
>= [2]
= tt()
isQid(n__e()) = [11]
>= [2]
= tt()
isQid(n__o()) = [8]
>= [2]
= tt()
nil() = [0]
>= [0]
= n__nil()
o() = [4]
>= [4]
= n__o()
u() = [5]
>= [2]
= n__u()
Further, it can be verified that all rules not oriented are covered by the weightgap condition.
*** 1.1.1.1.1 Progress [(O(1),O(n^1))] ***
Considered Problem:
Strict DP Rules:
Strict TRS Rules:
U22(tt()) -> tt()
U81(tt()) -> tt()
__(__(X,Y),Z) -> __(X,__(Y,Z))
a() -> n__a()
activate(X) -> X
activate(n____(X1,X2)) -> __(X1,X2)
activate(n__i()) -> i()
activate(n__nil()) -> nil()
activate(n__u()) -> u()
e() -> n__e()
isList(V) -> U11(isNeList(activate(V)))
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))
isPal(V) -> U81(isNePal(activate(V)))
isPal(n__nil()) -> tt()
nil() -> n__nil()
o() -> n__o()
Weak DP Rules:
Weak TRS Rules:
U11(tt()) -> tt()
U21(tt(),V2) -> U22(isList(activate(V2)))
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()
__(X,nil()) -> X
__(X1,X2) -> n____(X1,X2)
__(nil(),X) -> X
activate(n__a()) -> a()
activate(n__e()) -> e()
activate(n__o()) -> o()
i() -> n__i()
isList(n__nil()) -> tt()
isNeList(V) -> U31(isQid(activate(V)))
isNePal(V) -> U61(isQid(activate(V)))
isNePal(n____(I,__(P,I))) -> U71(isQid(activate(I)),activate(P))
isQid(n__a()) -> tt()
isQid(n__e()) -> tt()
isQid(n__i()) -> tt()
isQid(n__o()) -> tt()
isQid(n__u()) -> 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:
Full
basic terms: {U11,U21,U22,U31,U41,U42,U51,U52,U61,U71,U72,U81,__,a,activate,e,i,isList,isNeList,isNePal,isPal,isQid,nil,o,u}/{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}
Proof:
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(__) = {2},
uargs(activate) = {1},
uargs(isList) = {1},
uargs(isNeList) = {1},
uargs(isNePal) = {1},
uargs(isPal) = {1},
uargs(isQid) = {1},
uargs(n____) = {2}
Following symbols are considered usable:
{}
TcT has computed the following interpretation:
p(U11) = [1] x1 + [2]
p(U21) = [1] x1 + [1] x2 + [6]
p(U22) = [1] x1 + [0]
p(U31) = [1] x1 + [1]
p(U41) = [1] x1 + [1] x2 + [6]
p(U42) = [1] x1 + [4]
p(U51) = [1] x1 + [1] x2 + [3]
p(U52) = [1] x1 + [0]
p(U61) = [1] x1 + [0]
p(U71) = [1] x1 + [1] x2 + [0]
p(U72) = [1] x1 + [0]
p(U81) = [1] x1 + [7]
p(__) = [1] x1 + [1] x2 + [1]
p(a) = [0]
p(activate) = [1] x1 + [0]
p(e) = [0]
p(i) = [0]
p(isList) = [1] x1 + [4]
p(isNeList) = [1] x1 + [3]
p(isNePal) = [1] x1 + [4]
p(isPal) = [1] x1 + [0]
p(isQid) = [1] x1 + [2]
p(n____) = [1] x1 + [1] x2 + [1]
p(n__a) = [5]
p(n__e) = [0]
p(n__i) = [0]
p(n__nil) = [5]
p(n__o) = [0]
p(n__u) = [0]
p(nil) = [0]
p(o) = [0]
p(tt) = [1]
p(u) = [0]
Following rules are strictly oriented:
U81(tt()) = [8]
> [1]
= tt()
activate(n__nil()) = [5]
> [0]
= nil()
isPal(n__nil()) = [5]
> [1]
= tt()
Following rules are (at-least) weakly oriented:
U11(tt()) = [3]
>= [1]
= tt()
U21(tt(),V2) = [1] V2 + [7]
>= [1] V2 + [4]
= U22(isList(activate(V2)))
U22(tt()) = [1]
>= [1]
= tt()
U31(tt()) = [2]
>= [1]
= tt()
U41(tt(),V2) = [1] V2 + [7]
>= [1] V2 + [7]
= U42(isNeList(activate(V2)))
U42(tt()) = [5]
>= [1]
= tt()
U51(tt(),V2) = [1] V2 + [4]
>= [1] V2 + [4]
= U52(isList(activate(V2)))
U52(tt()) = [1]
>= [1]
= tt()
U61(tt()) = [1]
>= [1]
= tt()
U71(tt(),P) = [1] P + [1]
>= [1] P + [0]
= U72(isPal(activate(P)))
U72(tt()) = [1]
>= [1]
= tt()
__(X,nil()) = [1] X + [1]
>= [1] X + [0]
= X
__(X1,X2) = [1] X1 + [1] X2 + [1]
>= [1] X1 + [1] X2 + [1]
= n____(X1,X2)
__(__(X,Y),Z) = [1] X + [1] Y + [1] Z + [2]
>= [1] X + [1] Y + [1] Z + [2]
= __(X,__(Y,Z))
__(nil(),X) = [1] X + [1]
>= [1] X + [0]
= X
a() = [0]
>= [5]
= n__a()
activate(X) = [1] X + [0]
>= [1] X + [0]
= X
activate(n____(X1,X2)) = [1] X1 + [1] X2 + [1]
>= [1] X1 + [1] X2 + [1]
= __(X1,X2)
activate(n__a()) = [5]
>= [0]
= a()
activate(n__e()) = [0]
>= [0]
= e()
activate(n__i()) = [0]
>= [0]
= i()
activate(n__o()) = [0]
>= [0]
= o()
activate(n__u()) = [0]
>= [0]
= u()
e() = [0]
>= [0]
= n__e()
i() = [0]
>= [0]
= n__i()
isList(V) = [1] V + [4]
>= [1] V + [5]
= U11(isNeList(activate(V)))
isList(n____(V1,V2)) = [1] V1 + [1] V2 + [5]
>= [1] V1 + [1] V2 + [10]
= U21(isList(activate(V1))
,activate(V2))
isList(n__nil()) = [9]
>= [1]
= tt()
isNeList(V) = [1] V + [3]
>= [1] V + [3]
= U31(isQid(activate(V)))
isNeList(n____(V1,V2)) = [1] V1 + [1] V2 + [4]
>= [1] V1 + [1] V2 + [10]
= U41(isList(activate(V1))
,activate(V2))
isNeList(n____(V1,V2)) = [1] V1 + [1] V2 + [4]
>= [1] V1 + [1] V2 + [6]
= U51(isNeList(activate(V1))
,activate(V2))
isNePal(V) = [1] V + [4]
>= [1] V + [2]
= U61(isQid(activate(V)))
isNePal(n____(I,__(P,I))) = [2] I + [1] P + [6]
>= [1] I + [1] P + [2]
= U71(isQid(activate(I))
,activate(P))
isPal(V) = [1] V + [0]
>= [1] V + [11]
= U81(isNePal(activate(V)))
isQid(n__a()) = [7]
>= [1]
= tt()
isQid(n__e()) = [2]
>= [1]
= tt()
isQid(n__i()) = [2]
>= [1]
= tt()
isQid(n__o()) = [2]
>= [1]
= tt()
isQid(n__u()) = [2]
>= [1]
= tt()
nil() = [0]
>= [5]
= n__nil()
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.
*** 1.1.1.1.1.1 Progress [(O(1),O(n^1))] ***
Considered Problem:
Strict DP Rules:
Strict TRS Rules:
U22(tt()) -> tt()
__(__(X,Y),Z) -> __(X,__(Y,Z))
a() -> n__a()
activate(X) -> X
activate(n____(X1,X2)) -> __(X1,X2)
activate(n__i()) -> i()
activate(n__u()) -> u()
e() -> n__e()
isList(V) -> U11(isNeList(activate(V)))
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))
isPal(V) -> U81(isNePal(activate(V)))
nil() -> n__nil()
o() -> n__o()
Weak DP Rules:
Weak TRS Rules:
U11(tt()) -> tt()
U21(tt(),V2) -> U22(isList(activate(V2)))
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()
__(X,nil()) -> X
__(X1,X2) -> n____(X1,X2)
__(nil(),X) -> X
activate(n__a()) -> a()
activate(n__e()) -> e()
activate(n__nil()) -> nil()
activate(n__o()) -> o()
i() -> n__i()
isList(n__nil()) -> tt()
isNeList(V) -> U31(isQid(activate(V)))
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()
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:
Full
basic terms: {U11,U21,U22,U31,U41,U42,U51,U52,U61,U71,U72,U81,__,a,activate,e,i,isList,isNeList,isNePal,isPal,isQid,nil,o,u}/{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}
Proof:
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(__) = {2},
uargs(activate) = {1},
uargs(isList) = {1},
uargs(isNeList) = {1},
uargs(isNePal) = {1},
uargs(isPal) = {1},
uargs(isQid) = {1},
uargs(n____) = {2}
Following symbols are considered usable:
{}
TcT has computed the following interpretation:
p(U11) = [1] x1 + [5]
p(U21) = [1] x1 + [1] x2 + [2]
p(U22) = [1] x1 + [2]
p(U31) = [1] x1 + [0]
p(U41) = [1] x1 + [1] x2 + [2]
p(U42) = [1] x1 + [0]
p(U51) = [1] x1 + [1] x2 + [0]
p(U52) = [1] x1 + [0]
p(U61) = [1] x1 + [0]
p(U71) = [1] x1 + [1] x2 + [4]
p(U72) = [1] x1 + [1]
p(U81) = [1] x1 + [6]
p(__) = [1] x1 + [1] x2 + [1]
p(a) = [0]
p(activate) = [1] x1 + [0]
p(e) = [4]
p(i) = [0]
p(isList) = [1] x1 + [0]
p(isNeList) = [1] x1 + [2]
p(isNePal) = [1] x1 + [2]
p(isPal) = [1] x1 + [3]
p(isQid) = [1] x1 + [0]
p(n____) = [1] x1 + [1] x2 + [1]
p(n__a) = [1]
p(n__e) = [6]
p(n__i) = [0]
p(n__nil) = [5]
p(n__o) = [0]
p(n__u) = [0]
p(nil) = [2]
p(o) = [0]
p(tt) = [0]
p(u) = [2]
Following rules are strictly oriented:
U22(tt()) = [2]
> [0]
= tt()
isNeList(n____(V1,V2)) = [1] V1 + [1] V2 + [3]
> [1] V1 + [1] V2 + [2]
= U41(isList(activate(V1))
,activate(V2))
isNeList(n____(V1,V2)) = [1] V1 + [1] V2 + [3]
> [1] V1 + [1] V2 + [2]
= U51(isNeList(activate(V1))
,activate(V2))
Following rules are (at-least) weakly oriented:
U11(tt()) = [5]
>= [0]
= tt()
U21(tt(),V2) = [1] V2 + [2]
>= [1] V2 + [2]
= U22(isList(activate(V2)))
U31(tt()) = [0]
>= [0]
= tt()
U41(tt(),V2) = [1] V2 + [2]
>= [1] V2 + [2]
= U42(isNeList(activate(V2)))
U42(tt()) = [0]
>= [0]
= tt()
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 + [4]
= U72(isPal(activate(P)))
U72(tt()) = [1]
>= [0]
= tt()
U81(tt()) = [6]
>= [0]
= tt()
__(X,nil()) = [1] X + [3]
>= [1] X + [0]
= X
__(X1,X2) = [1] X1 + [1] X2 + [1]
>= [1] X1 + [1] X2 + [1]
= n____(X1,X2)
__(__(X,Y),Z) = [1] X + [1] Y + [1] Z + [2]
>= [1] X + [1] Y + [1] Z + [2]
= __(X,__(Y,Z))
__(nil(),X) = [1] X + [3]
>= [1] X + [0]
= X
a() = [0]
>= [1]
= n__a()
activate(X) = [1] X + [0]
>= [1] X + [0]
= X
activate(n____(X1,X2)) = [1] X1 + [1] X2 + [1]
>= [1] X1 + [1] X2 + [1]
= __(X1,X2)
activate(n__a()) = [1]
>= [0]
= a()
activate(n__e()) = [6]
>= [4]
= e()
activate(n__i()) = [0]
>= [0]
= i()
activate(n__nil()) = [5]
>= [2]
= nil()
activate(n__o()) = [0]
>= [0]
= o()
activate(n__u()) = [0]
>= [2]
= u()
e() = [4]
>= [6]
= n__e()
i() = [0]
>= [0]
= n__i()
isList(V) = [1] V + [0]
>= [1] V + [7]
= U11(isNeList(activate(V)))
isList(n____(V1,V2)) = [1] V1 + [1] V2 + [1]
>= [1] V1 + [1] V2 + [2]
= U21(isList(activate(V1))
,activate(V2))
isList(n__nil()) = [5]
>= [0]
= tt()
isNeList(V) = [1] V + [2]
>= [1] V + [0]
= U31(isQid(activate(V)))
isNePal(V) = [1] V + [2]
>= [1] V + [0]
= U61(isQid(activate(V)))
isNePal(n____(I,__(P,I))) = [2] I + [1] P + [4]
>= [1] I + [1] P + [4]
= U71(isQid(activate(I))
,activate(P))
isPal(V) = [1] V + [3]
>= [1] V + [8]
= U81(isNePal(activate(V)))
isPal(n__nil()) = [8]
>= [0]
= tt()
isQid(n__a()) = [1]
>= [0]
= tt()
isQid(n__e()) = [6]
>= [0]
= tt()
isQid(n__i()) = [0]
>= [0]
= tt()
isQid(n__o()) = [0]
>= [0]
= tt()
isQid(n__u()) = [0]
>= [0]
= tt()
nil() = [2]
>= [5]
= n__nil()
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.
*** 1.1.1.1.1.1.1 Progress [(O(1),O(n^1))] ***
Considered Problem:
Strict DP Rules:
Strict TRS Rules:
__(__(X,Y),Z) -> __(X,__(Y,Z))
a() -> n__a()
activate(X) -> X
activate(n____(X1,X2)) -> __(X1,X2)
activate(n__i()) -> i()
activate(n__u()) -> u()
e() -> n__e()
isList(V) -> U11(isNeList(activate(V)))
isList(n____(V1,V2)) -> U21(isList(activate(V1)),activate(V2))
isPal(V) -> U81(isNePal(activate(V)))
nil() -> n__nil()
o() -> n__o()
Weak DP Rules:
Weak TRS Rules:
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()
__(X,nil()) -> X
__(X1,X2) -> n____(X1,X2)
__(nil(),X) -> X
activate(n__a()) -> a()
activate(n__e()) -> e()
activate(n__nil()) -> nil()
activate(n__o()) -> o()
i() -> n__i()
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()
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:
Full
basic terms: {U11,U21,U22,U31,U41,U42,U51,U52,U61,U71,U72,U81,__,a,activate,e,i,isList,isNeList,isNePal,isPal,isQid,nil,o,u}/{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}
Proof:
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(__) = {2},
uargs(activate) = {1},
uargs(isList) = {1},
uargs(isNeList) = {1},
uargs(isNePal) = {1},
uargs(isPal) = {1},
uargs(isQid) = {1},
uargs(n____) = {2}
Following symbols are considered usable:
{}
TcT has computed the following interpretation:
p(U11) = [1] x1 + [0]
p(U21) = [1] x1 + [1] x2 + [3]
p(U22) = [1] x1 + [0]
p(U31) = [1] x1 + [0]
p(U41) = [1] x1 + [1] x2 + [0]
p(U42) = [1] x1 + [0]
p(U51) = [1] x1 + [1] x2 + [4]
p(U52) = [1] x1 + [1]
p(U61) = [1] x1 + [0]
p(U71) = [1] x1 + [1] x2 + [3]
p(U72) = [1] x1 + [1]
p(U81) = [1] x1 + [0]
p(__) = [1] x1 + [1] x2 + [4]
p(a) = [2]
p(activate) = [1] x1 + [0]
p(e) = [2]
p(i) = [3]
p(isList) = [1] x1 + [5]
p(isNeList) = [1] x1 + [2]
p(isNePal) = [1] x1 + [6]
p(isPal) = [1] x1 + [4]
p(isQid) = [1] x1 + [0]
p(n____) = [1] x1 + [1] x2 + [4]
p(n__a) = [2]
p(n__e) = [2]
p(n__i) = [2]
p(n__nil) = [1]
p(n__o) = [3]
p(n__u) = [2]
p(nil) = [0]
p(o) = [3]
p(tt) = [2]
p(u) = [2]
Following rules are strictly oriented:
isList(V) = [1] V + [5]
> [1] V + [2]
= U11(isNeList(activate(V)))
isList(n____(V1,V2)) = [1] V1 + [1] V2 + [9]
> [1] V1 + [1] V2 + [8]
= U21(isList(activate(V1))
,activate(V2))
Following rules are (at-least) weakly oriented:
U11(tt()) = [2]
>= [2]
= tt()
U21(tt(),V2) = [1] V2 + [5]
>= [1] V2 + [5]
= U22(isList(activate(V2)))
U22(tt()) = [2]
>= [2]
= tt()
U31(tt()) = [2]
>= [2]
= tt()
U41(tt(),V2) = [1] V2 + [2]
>= [1] V2 + [2]
= U42(isNeList(activate(V2)))
U42(tt()) = [2]
>= [2]
= tt()
U51(tt(),V2) = [1] V2 + [6]
>= [1] V2 + [6]
= U52(isList(activate(V2)))
U52(tt()) = [3]
>= [2]
= tt()
U61(tt()) = [2]
>= [2]
= tt()
U71(tt(),P) = [1] P + [5]
>= [1] P + [5]
= U72(isPal(activate(P)))
U72(tt()) = [3]
>= [2]
= tt()
U81(tt()) = [2]
>= [2]
= tt()
__(X,nil()) = [1] X + [4]
>= [1] X + [0]
= X
__(X1,X2) = [1] X1 + [1] X2 + [4]
>= [1] X1 + [1] X2 + [4]
= n____(X1,X2)
__(__(X,Y),Z) = [1] X + [1] Y + [1] Z + [8]
>= [1] X + [1] Y + [1] Z + [8]
= __(X,__(Y,Z))
__(nil(),X) = [1] X + [4]
>= [1] X + [0]
= X
a() = [2]
>= [2]
= n__a()
activate(X) = [1] X + [0]
>= [1] X + [0]
= X
activate(n____(X1,X2)) = [1] X1 + [1] X2 + [4]
>= [1] X1 + [1] X2 + [4]
= __(X1,X2)
activate(n__a()) = [2]
>= [2]
= a()
activate(n__e()) = [2]
>= [2]
= e()
activate(n__i()) = [2]
>= [3]
= i()
activate(n__nil()) = [1]
>= [0]
= nil()
activate(n__o()) = [3]
>= [3]
= o()
activate(n__u()) = [2]
>= [2]
= u()
e() = [2]
>= [2]
= n__e()
i() = [3]
>= [2]
= n__i()
isList(n__nil()) = [6]
>= [2]
= tt()
isNeList(V) = [1] V + [2]
>= [1] V + [0]
= U31(isQid(activate(V)))
isNeList(n____(V1,V2)) = [1] V1 + [1] V2 + [6]
>= [1] V1 + [1] V2 + [5]
= U41(isList(activate(V1))
,activate(V2))
isNeList(n____(V1,V2)) = [1] V1 + [1] V2 + [6]
>= [1] V1 + [1] V2 + [6]
= U51(isNeList(activate(V1))
,activate(V2))
isNePal(V) = [1] V + [6]
>= [1] V + [0]
= U61(isQid(activate(V)))
isNePal(n____(I,__(P,I))) = [2] I + [1] P + [14]
>= [1] I + [1] P + [3]
= U71(isQid(activate(I))
,activate(P))
isPal(V) = [1] V + [4]
>= [1] V + [6]
= U81(isNePal(activate(V)))
isPal(n__nil()) = [5]
>= [2]
= tt()
isQid(n__a()) = [2]
>= [2]
= tt()
isQid(n__e()) = [2]
>= [2]
= tt()
isQid(n__i()) = [2]
>= [2]
= tt()
isQid(n__o()) = [3]
>= [2]
= tt()
isQid(n__u()) = [2]
>= [2]
= tt()
nil() = [0]
>= [1]
= n__nil()
o() = [3]
>= [3]
= n__o()
u() = [2]
>= [2]
= n__u()
Further, it can be verified that all rules not oriented are covered by the weightgap condition.
*** 1.1.1.1.1.1.1.1 Progress [(O(1),O(n^1))] ***
Considered Problem:
Strict DP Rules:
Strict TRS Rules:
__(__(X,Y),Z) -> __(X,__(Y,Z))
a() -> n__a()
activate(X) -> X
activate(n____(X1,X2)) -> __(X1,X2)
activate(n__i()) -> i()
activate(n__u()) -> u()
e() -> n__e()
isPal(V) -> U81(isNePal(activate(V)))
nil() -> n__nil()
o() -> n__o()
Weak DP Rules:
Weak TRS Rules:
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()
__(X,nil()) -> X
__(X1,X2) -> n____(X1,X2)
__(nil(),X) -> X
activate(n__a()) -> a()
activate(n__e()) -> e()
activate(n__nil()) -> nil()
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()
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:
Full
basic terms: {U11,U21,U22,U31,U41,U42,U51,U52,U61,U71,U72,U81,__,a,activate,e,i,isList,isNeList,isNePal,isPal,isQid,nil,o,u}/{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}
Proof:
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(__) = {2},
uargs(activate) = {1},
uargs(isList) = {1},
uargs(isNeList) = {1},
uargs(isNePal) = {1},
uargs(isPal) = {1},
uargs(isQid) = {1},
uargs(n____) = {2}
Following symbols are considered usable:
{}
TcT has computed the following interpretation:
p(U11) = [1] x1 + [0]
p(U21) = [1] x1 + [1] x2 + [1]
p(U22) = [1] x1 + [0]
p(U31) = [1] x1 + [0]
p(U41) = [1] x1 + [1] x2 + [0]
p(U42) = [1] x1 + [0]
p(U51) = [1] x1 + [1] x2 + [1]
p(U52) = [1] x1 + [0]
p(U61) = [1] x1 + [0]
p(U71) = [1] x1 + [1] x2 + [2]
p(U72) = [1] x1 + [0]
p(U81) = [1] x1 + [0]
p(__) = [1] x1 + [1] x2 + [1]
p(a) = [0]
p(activate) = [1] x1 + [0]
p(e) = [0]
p(i) = [0]
p(isList) = [1] x1 + [1]
p(isNeList) = [1] x1 + [0]
p(isNePal) = [1] x1 + [0]
p(isPal) = [1] x1 + [1]
p(isQid) = [1] x1 + [0]
p(n____) = [1] x1 + [1] x2 + [1]
p(n__a) = [0]
p(n__e) = [0]
p(n__i) = [0]
p(n__nil) = [5]
p(n__o) = [1]
p(n__u) = [0]
p(nil) = [4]
p(o) = [0]
p(tt) = [0]
p(u) = [0]
Following rules are strictly oriented:
isPal(V) = [1] V + [1]
> [1] V + [0]
= U81(isNePal(activate(V)))
Following rules are (at-least) weakly oriented:
U11(tt()) = [0]
>= [0]
= tt()
U21(tt(),V2) = [1] V2 + [1]
>= [1] V2 + [1]
= U22(isList(activate(V2)))
U22(tt()) = [0]
>= [0]
= tt()
U31(tt()) = [0]
>= [0]
= tt()
U41(tt(),V2) = [1] V2 + [0]
>= [1] V2 + [0]
= U42(isNeList(activate(V2)))
U42(tt()) = [0]
>= [0]
= tt()
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 + [2]
>= [1] P + [1]
= U72(isPal(activate(P)))
U72(tt()) = [0]
>= [0]
= tt()
U81(tt()) = [0]
>= [0]
= tt()
__(X,nil()) = [1] X + [5]
>= [1] X + [0]
= X
__(X1,X2) = [1] X1 + [1] X2 + [1]
>= [1] X1 + [1] X2 + [1]
= n____(X1,X2)
__(__(X,Y),Z) = [1] X + [1] Y + [1] Z + [2]
>= [1] X + [1] Y + [1] Z + [2]
= __(X,__(Y,Z))
__(nil(),X) = [1] X + [5]
>= [1] X + [0]
= X
a() = [0]
>= [0]
= n__a()
activate(X) = [1] X + [0]
>= [1] X + [0]
= X
activate(n____(X1,X2)) = [1] X1 + [1] X2 + [1]
>= [1] X1 + [1] X2 + [1]
= __(X1,X2)
activate(n__a()) = [0]
>= [0]
= a()
activate(n__e()) = [0]
>= [0]
= e()
activate(n__i()) = [0]
>= [0]
= i()
activate(n__nil()) = [5]
>= [4]
= nil()
activate(n__o()) = [1]
>= [0]
= o()
activate(n__u()) = [0]
>= [0]
= u()
e() = [0]
>= [0]
= n__e()
i() = [0]
>= [0]
= n__i()
isList(V) = [1] V + [1]
>= [1] V + [0]
= U11(isNeList(activate(V)))
isList(n____(V1,V2)) = [1] V1 + [1] V2 + [2]
>= [1] V1 + [1] V2 + [2]
= U21(isList(activate(V1))
,activate(V2))
isList(n__nil()) = [6]
>= [0]
= tt()
isNeList(V) = [1] V + [0]
>= [1] V + [0]
= U31(isQid(activate(V)))
isNeList(n____(V1,V2)) = [1] V1 + [1] V2 + [1]
>= [1] V1 + [1] V2 + [1]
= U41(isList(activate(V1))
,activate(V2))
isNeList(n____(V1,V2)) = [1] V1 + [1] V2 + [1]
>= [1] V1 + [1] V2 + [1]
= U51(isNeList(activate(V1))
,activate(V2))
isNePal(V) = [1] V + [0]
>= [1] V + [0]
= U61(isQid(activate(V)))
isNePal(n____(I,__(P,I))) = [2] I + [1] P + [2]
>= [1] I + [1] P + [2]
= U71(isQid(activate(I))
,activate(P))
isPal(n__nil()) = [6]
>= [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()
nil() = [4]
>= [5]
= n__nil()
o() = [0]
>= [1]
= n__o()
u() = [0]
>= [0]
= n__u()
Further, it can be verified that all rules not oriented are covered by the weightgap condition.
*** 1.1.1.1.1.1.1.1.1 Progress [(O(1),O(n^1))] ***
Considered Problem:
Strict DP Rules:
Strict TRS Rules:
__(__(X,Y),Z) -> __(X,__(Y,Z))
a() -> n__a()
activate(X) -> X
activate(n____(X1,X2)) -> __(X1,X2)
activate(n__i()) -> i()
activate(n__u()) -> u()
e() -> n__e()
nil() -> n__nil()
o() -> n__o()
Weak DP Rules:
Weak TRS Rules:
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()
__(X,nil()) -> X
__(X1,X2) -> n____(X1,X2)
__(nil(),X) -> X
activate(n__a()) -> a()
activate(n__e()) -> e()
activate(n__nil()) -> nil()
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()
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:
Full
basic terms: {U11,U21,U22,U31,U41,U42,U51,U52,U61,U71,U72,U81,__,a,activate,e,i,isList,isNeList,isNePal,isPal,isQid,nil,o,u}/{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}
Proof:
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(__) = {2},
uargs(activate) = {1},
uargs(isList) = {1},
uargs(isNeList) = {1},
uargs(isNePal) = {1},
uargs(isPal) = {1},
uargs(isQid) = {1},
uargs(n____) = {2}
Following symbols are considered usable:
{}
TcT has computed the following interpretation:
p(U11) = [1] x1 + [0]
p(U21) = [1] x1 + [1] x2 + [1]
p(U22) = [1] x1 + [0]
p(U31) = [1] x1 + [0]
p(U41) = [1] x1 + [1] x2 + [0]
p(U42) = [1] x1 + [0]
p(U51) = [1] x1 + [1] x2 + [0]
p(U52) = [1] x1 + [0]
p(U61) = [1] x1 + [0]
p(U71) = [1] x1 + [1] x2 + [6]
p(U72) = [1] x1 + [6]
p(U81) = [1] x1 + [0]
p(__) = [1] x1 + [1] x2 + [5]
p(a) = [4]
p(activate) = [1] x1 + [1]
p(e) = [0]
p(i) = [4]
p(isList) = [1] x1 + [5]
p(isNeList) = [1] x1 + [4]
p(isNePal) = [1] x1 + [4]
p(isPal) = [1] x1 + [5]
p(isQid) = [1] x1 + [3]
p(n____) = [1] x1 + [1] x2 + [3]
p(n__a) = [3]
p(n__e) = [5]
p(n__i) = [4]
p(n__nil) = [3]
p(n__o) = [6]
p(n__u) = [6]
p(nil) = [0]
p(o) = [7]
p(tt) = [6]
p(u) = [6]
Following rules are strictly oriented:
a() = [4]
> [3]
= n__a()
activate(X) = [1] X + [1]
> [1] X + [0]
= X
activate(n__i()) = [5]
> [4]
= i()
activate(n__u()) = [7]
> [6]
= u()
o() = [7]
> [6]
= n__o()
Following rules are (at-least) weakly oriented:
U11(tt()) = [6]
>= [6]
= tt()
U21(tt(),V2) = [1] V2 + [7]
>= [1] V2 + [6]
= U22(isList(activate(V2)))
U22(tt()) = [6]
>= [6]
= tt()
U31(tt()) = [6]
>= [6]
= tt()
U41(tt(),V2) = [1] V2 + [6]
>= [1] V2 + [5]
= U42(isNeList(activate(V2)))
U42(tt()) = [6]
>= [6]
= tt()
U51(tt(),V2) = [1] V2 + [6]
>= [1] V2 + [6]
= U52(isList(activate(V2)))
U52(tt()) = [6]
>= [6]
= tt()
U61(tt()) = [6]
>= [6]
= tt()
U71(tt(),P) = [1] P + [12]
>= [1] P + [12]
= U72(isPal(activate(P)))
U72(tt()) = [12]
>= [6]
= tt()
U81(tt()) = [6]
>= [6]
= tt()
__(X,nil()) = [1] X + [5]
>= [1] X + [0]
= X
__(X1,X2) = [1] X1 + [1] X2 + [5]
>= [1] X1 + [1] X2 + [3]
= n____(X1,X2)
__(__(X,Y),Z) = [1] X + [1] Y + [1] Z + [10]
>= [1] X + [1] Y + [1] Z + [10]
= __(X,__(Y,Z))
__(nil(),X) = [1] X + [5]
>= [1] X + [0]
= X
activate(n____(X1,X2)) = [1] X1 + [1] X2 + [4]
>= [1] X1 + [1] X2 + [5]
= __(X1,X2)
activate(n__a()) = [4]
>= [4]
= a()
activate(n__e()) = [6]
>= [0]
= e()
activate(n__nil()) = [4]
>= [0]
= nil()
activate(n__o()) = [7]
>= [7]
= o()
e() = [0]
>= [5]
= n__e()
i() = [4]
>= [4]
= n__i()
isList(V) = [1] V + [5]
>= [1] V + [5]
= U11(isNeList(activate(V)))
isList(n____(V1,V2)) = [1] V1 + [1] V2 + [8]
>= [1] V1 + [1] V2 + [8]
= U21(isList(activate(V1))
,activate(V2))
isList(n__nil()) = [8]
>= [6]
= tt()
isNeList(V) = [1] V + [4]
>= [1] V + [4]
= U31(isQid(activate(V)))
isNeList(n____(V1,V2)) = [1] V1 + [1] V2 + [7]
>= [1] V1 + [1] V2 + [7]
= U41(isList(activate(V1))
,activate(V2))
isNeList(n____(V1,V2)) = [1] V1 + [1] V2 + [7]
>= [1] V1 + [1] V2 + [6]
= U51(isNeList(activate(V1))
,activate(V2))
isNePal(V) = [1] V + [4]
>= [1] V + [4]
= U61(isQid(activate(V)))
isNePal(n____(I,__(P,I))) = [2] I + [1] P + [12]
>= [1] I + [1] P + [11]
= U71(isQid(activate(I))
,activate(P))
isPal(V) = [1] V + [5]
>= [1] V + [5]
= U81(isNePal(activate(V)))
isPal(n__nil()) = [8]
>= [6]
= tt()
isQid(n__a()) = [6]
>= [6]
= tt()
isQid(n__e()) = [8]
>= [6]
= tt()
isQid(n__i()) = [7]
>= [6]
= tt()
isQid(n__o()) = [9]
>= [6]
= tt()
isQid(n__u()) = [9]
>= [6]
= tt()
nil() = [0]
>= [3]
= n__nil()
u() = [6]
>= [6]
= n__u()
Further, it can be verified that all rules not oriented are covered by the weightgap condition.
*** 1.1.1.1.1.1.1.1.1.1 Progress [(O(1),O(n^1))] ***
Considered Problem:
Strict DP Rules:
Strict TRS Rules:
__(__(X,Y),Z) -> __(X,__(Y,Z))
activate(n____(X1,X2)) -> __(X1,X2)
e() -> n__e()
nil() -> n__nil()
Weak DP Rules:
Weak TRS Rules:
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()
__(X,nil()) -> X
__(X1,X2) -> n____(X1,X2)
__(nil(),X) -> X
a() -> n__a()
activate(X) -> X
activate(n__a()) -> a()
activate(n__e()) -> e()
activate(n__i()) -> i()
activate(n__nil()) -> nil()
activate(n__o()) -> o()
activate(n__u()) -> u()
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()
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:
Full
basic terms: {U11,U21,U22,U31,U41,U42,U51,U52,U61,U71,U72,U81,__,a,activate,e,i,isList,isNeList,isNePal,isPal,isQid,nil,o,u}/{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}
Proof:
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(__) = {2},
uargs(activate) = {1},
uargs(isList) = {1},
uargs(isNeList) = {1},
uargs(isNePal) = {1},
uargs(isPal) = {1},
uargs(isQid) = {1},
uargs(n____) = {2}
Following symbols are considered usable:
{}
TcT has computed the following interpretation:
p(U11) = [1] x1 + [0]
p(U21) = [1] x1 + [1] x2 + [2]
p(U22) = [1] x1 + [2]
p(U31) = [1] x1 + [0]
p(U41) = [1] x1 + [1] x2 + [0]
p(U42) = [1] x1 + [0]
p(U51) = [1] x1 + [1] x2 + [0]
p(U52) = [1] x1 + [0]
p(U61) = [1] x1 + [0]
p(U71) = [1] x1 + [1] x2 + [3]
p(U72) = [1] x1 + [0]
p(U81) = [1] x1 + [0]
p(__) = [1] x1 + [1] x2 + [6]
p(a) = [6]
p(activate) = [1] x1 + [2]
p(e) = [0]
p(i) = [6]
p(isList) = [1] x1 + [4]
p(isNeList) = [1] x1 + [2]
p(isNePal) = [1] x1 + [2]
p(isPal) = [1] x1 + [4]
p(isQid) = [1] x1 + [0]
p(n____) = [1] x1 + [1] x2 + [6]
p(n__a) = [6]
p(n__e) = [6]
p(n__i) = [6]
p(n__nil) = [4]
p(n__o) = [7]
p(n__u) = [6]
p(nil) = [5]
p(o) = [7]
p(tt) = [6]
p(u) = [7]
Following rules are strictly oriented:
activate(n____(X1,X2)) = [1] X1 + [1] X2 + [8]
> [1] X1 + [1] X2 + [6]
= __(X1,X2)
nil() = [5]
> [4]
= n__nil()
Following rules are (at-least) weakly oriented:
U11(tt()) = [6]
>= [6]
= tt()
U21(tt(),V2) = [1] V2 + [8]
>= [1] V2 + [8]
= U22(isList(activate(V2)))
U22(tt()) = [8]
>= [6]
= tt()
U31(tt()) = [6]
>= [6]
= tt()
U41(tt(),V2) = [1] V2 + [6]
>= [1] V2 + [4]
= U42(isNeList(activate(V2)))
U42(tt()) = [6]
>= [6]
= tt()
U51(tt(),V2) = [1] V2 + [6]
>= [1] V2 + [6]
= U52(isList(activate(V2)))
U52(tt()) = [6]
>= [6]
= tt()
U61(tt()) = [6]
>= [6]
= tt()
U71(tt(),P) = [1] P + [9]
>= [1] P + [6]
= U72(isPal(activate(P)))
U72(tt()) = [6]
>= [6]
= tt()
U81(tt()) = [6]
>= [6]
= tt()
__(X,nil()) = [1] X + [11]
>= [1] X + [0]
= X
__(X1,X2) = [1] X1 + [1] X2 + [6]
>= [1] X1 + [1] X2 + [6]
= n____(X1,X2)
__(__(X,Y),Z) = [1] X + [1] Y + [1] Z + [12]
>= [1] X + [1] Y + [1] Z + [12]
= __(X,__(Y,Z))
__(nil(),X) = [1] X + [11]
>= [1] X + [0]
= X
a() = [6]
>= [6]
= n__a()
activate(X) = [1] X + [2]
>= [1] X + [0]
= X
activate(n__a()) = [8]
>= [6]
= a()
activate(n__e()) = [8]
>= [0]
= e()
activate(n__i()) = [8]
>= [6]
= i()
activate(n__nil()) = [6]
>= [5]
= nil()
activate(n__o()) = [9]
>= [7]
= o()
activate(n__u()) = [8]
>= [7]
= u()
e() = [0]
>= [6]
= n__e()
i() = [6]
>= [6]
= n__i()
isList(V) = [1] V + [4]
>= [1] V + [4]
= U11(isNeList(activate(V)))
isList(n____(V1,V2)) = [1] V1 + [1] V2 + [10]
>= [1] V1 + [1] V2 + [10]
= U21(isList(activate(V1))
,activate(V2))
isList(n__nil()) = [8]
>= [6]
= tt()
isNeList(V) = [1] V + [2]
>= [1] V + [2]
= U31(isQid(activate(V)))
isNeList(n____(V1,V2)) = [1] V1 + [1] V2 + [8]
>= [1] V1 + [1] V2 + [8]
= U41(isList(activate(V1))
,activate(V2))
isNeList(n____(V1,V2)) = [1] V1 + [1] V2 + [8]
>= [1] V1 + [1] V2 + [6]
= U51(isNeList(activate(V1))
,activate(V2))
isNePal(V) = [1] V + [2]
>= [1] V + [2]
= U61(isQid(activate(V)))
isNePal(n____(I,__(P,I))) = [2] I + [1] P + [14]
>= [1] I + [1] P + [7]
= U71(isQid(activate(I))
,activate(P))
isPal(V) = [1] V + [4]
>= [1] V + [4]
= U81(isNePal(activate(V)))
isPal(n__nil()) = [8]
>= [6]
= tt()
isQid(n__a()) = [6]
>= [6]
= tt()
isQid(n__e()) = [6]
>= [6]
= tt()
isQid(n__i()) = [6]
>= [6]
= tt()
isQid(n__o()) = [7]
>= [6]
= tt()
isQid(n__u()) = [6]
>= [6]
= tt()
o() = [7]
>= [7]
= n__o()
u() = [7]
>= [6]
= n__u()
Further, it can be verified that all rules not oriented are covered by the weightgap condition.
*** 1.1.1.1.1.1.1.1.1.1.1 Progress [(O(1),O(n^1))] ***
Considered Problem:
Strict DP Rules:
Strict TRS Rules:
__(__(X,Y),Z) -> __(X,__(Y,Z))
e() -> n__e()
Weak DP Rules:
Weak TRS Rules:
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()
__(X,nil()) -> X
__(X1,X2) -> n____(X1,X2)
__(nil(),X) -> X
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()
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:
Full
basic terms: {U11,U21,U22,U31,U41,U42,U51,U52,U61,U71,U72,U81,__,a,activate,e,i,isList,isNeList,isNePal,isPal,isQid,nil,o,u}/{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}
Proof:
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(__) = {2},
uargs(activate) = {1},
uargs(isList) = {1},
uargs(isNeList) = {1},
uargs(isNePal) = {1},
uargs(isPal) = {1},
uargs(isQid) = {1},
uargs(n____) = {2}
Following symbols are considered usable:
{}
TcT has computed the following interpretation:
p(U11) = [1] x1 + [1]
p(U21) = [1] x1 + [1] x2 + [5]
p(U22) = [1] x1 + [0]
p(U31) = [1] x1 + [1]
p(U41) = [1] x1 + [1] x2 + [3]
p(U42) = [1] x1 + [0]
p(U51) = [1] x1 + [1] x2 + [5]
p(U52) = [1] x1 + [0]
p(U61) = [1] x1 + [0]
p(U71) = [1] x1 + [1] x2 + [6]
p(U72) = [1] x1 + [0]
p(U81) = [1] x1 + [0]
p(__) = [1] x1 + [1] x2 + [7]
p(a) = [4]
p(activate) = [1] x1 + [1]
p(e) = [3]
p(i) = [2]
p(isList) = [1] x1 + [4]
p(isNeList) = [1] x1 + [2]
p(isNePal) = [1] x1 + [1]
p(isPal) = [1] x1 + [5]
p(isQid) = [1] x1 + [0]
p(n____) = [1] x1 + [1] x2 + [7]
p(n__a) = [4]
p(n__e) = [2]
p(n__i) = [1]
p(n__nil) = [0]
p(n__o) = [0]
p(n__u) = [0]
p(nil) = [0]
p(o) = [0]
p(tt) = [0]
p(u) = [0]
Following rules are strictly oriented:
e() = [3]
> [2]
= n__e()
Following rules are (at-least) weakly oriented:
U11(tt()) = [1]
>= [0]
= tt()
U21(tt(),V2) = [1] V2 + [5]
>= [1] V2 + [5]
= U22(isList(activate(V2)))
U22(tt()) = [0]
>= [0]
= tt()
U31(tt()) = [1]
>= [0]
= tt()
U41(tt(),V2) = [1] V2 + [3]
>= [1] V2 + [3]
= U42(isNeList(activate(V2)))
U42(tt()) = [0]
>= [0]
= tt()
U51(tt(),V2) = [1] V2 + [5]
>= [1] V2 + [5]
= U52(isList(activate(V2)))
U52(tt()) = [0]
>= [0]
= tt()
U61(tt()) = [0]
>= [0]
= tt()
U71(tt(),P) = [1] P + [6]
>= [1] P + [6]
= U72(isPal(activate(P)))
U72(tt()) = [0]
>= [0]
= tt()
U81(tt()) = [0]
>= [0]
= tt()
__(X,nil()) = [1] X + [7]
>= [1] X + [0]
= X
__(X1,X2) = [1] X1 + [1] X2 + [7]
>= [1] X1 + [1] X2 + [7]
= n____(X1,X2)
__(__(X,Y),Z) = [1] X + [1] Y + [1] Z + [14]
>= [1] X + [1] Y + [1] Z + [14]
= __(X,__(Y,Z))
__(nil(),X) = [1] X + [7]
>= [1] X + [0]
= X
a() = [4]
>= [4]
= n__a()
activate(X) = [1] X + [1]
>= [1] X + [0]
= X
activate(n____(X1,X2)) = [1] X1 + [1] X2 + [8]
>= [1] X1 + [1] X2 + [7]
= __(X1,X2)
activate(n__a()) = [5]
>= [4]
= a()
activate(n__e()) = [3]
>= [3]
= e()
activate(n__i()) = [2]
>= [2]
= i()
activate(n__nil()) = [1]
>= [0]
= nil()
activate(n__o()) = [1]
>= [0]
= o()
activate(n__u()) = [1]
>= [0]
= u()
i() = [2]
>= [1]
= n__i()
isList(V) = [1] V + [4]
>= [1] V + [4]
= U11(isNeList(activate(V)))
isList(n____(V1,V2)) = [1] V1 + [1] V2 + [11]
>= [1] V1 + [1] V2 + [11]
= U21(isList(activate(V1))
,activate(V2))
isList(n__nil()) = [4]
>= [0]
= tt()
isNeList(V) = [1] V + [2]
>= [1] V + [2]
= U31(isQid(activate(V)))
isNeList(n____(V1,V2)) = [1] V1 + [1] V2 + [9]
>= [1] V1 + [1] V2 + [9]
= U41(isList(activate(V1))
,activate(V2))
isNeList(n____(V1,V2)) = [1] V1 + [1] V2 + [9]
>= [1] V1 + [1] V2 + [9]
= U51(isNeList(activate(V1))
,activate(V2))
isNePal(V) = [1] V + [1]
>= [1] V + [1]
= U61(isQid(activate(V)))
isNePal(n____(I,__(P,I))) = [2] I + [1] P + [15]
>= [1] I + [1] P + [8]
= U71(isQid(activate(I))
,activate(P))
isPal(V) = [1] V + [5]
>= [1] V + [2]
= U81(isNePal(activate(V)))
isPal(n__nil()) = [5]
>= [0]
= tt()
isQid(n__a()) = [4]
>= [0]
= tt()
isQid(n__e()) = [2]
>= [0]
= tt()
isQid(n__i()) = [1]
>= [0]
= tt()
isQid(n__o()) = [0]
>= [0]
= tt()
isQid(n__u()) = [0]
>= [0]
= tt()
nil() = [0]
>= [0]
= n__nil()
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.
*** 1.1.1.1.1.1.1.1.1.1.1.1 Progress [(O(1),O(n^1))] ***
Considered Problem:
Strict DP Rules:
Strict TRS Rules:
__(__(X,Y),Z) -> __(X,__(Y,Z))
Weak DP Rules:
Weak TRS Rules:
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()
__(X,nil()) -> X
__(X1,X2) -> n____(X1,X2)
__(nil(),X) -> X
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:
Full
basic terms: {U11,U21,U22,U31,U41,U42,U51,U52,U61,U71,U72,U81,__,a,activate,e,i,isList,isNeList,isNePal,isPal,isQid,nil,o,u}/{n____,n__a,n__e,n__i,n__nil,n__o,n__u,tt}
Applied Processor:
NaturalMI {miDimension = 2, miDegree = 2, miKind = Algebraic, uargs = UArgs, urules = URules, selector = Just any strict-rules, greedy = NoGreedy}
Proof:
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(__) = {2},
uargs(activate) = {1},
uargs(isList) = {1},
uargs(isNeList) = {1},
uargs(isNePal) = {1},
uargs(isPal) = {1},
uargs(isQid) = {1},
uargs(n____) = {2}
Following symbols are considered usable:
{}
TcT has computed the following interpretation:
p(U11) = [1 0] x1 + [0]
[0 2] [1]
p(U21) = [1 0] x1 + [2 0] x2 + [0]
[0 0] [0 0] [1]
p(U22) = [1 0] x1 + [0]
[0 0] [1]
p(U31) = [1 0] x1 + [0]
[0 0] [0]
p(U41) = [1 0] x1 + [2 0] x2 + [0]
[0 0] [1 0] [0]
p(U42) = [1 0] x1 + [0]
[0 0] [0]
p(U51) = [1 0] x1 + [2 0] x2 + [0]
[0 0] [0 0] [0]
p(U52) = [1 0] x1 + [0]
[0 0] [0]
p(U61) = [1 0] x1 + [1]
[0 0] [0]
p(U71) = [2 0] x1 + [2 0] x2 + [2]
[0 0] [0 0] [0]
p(U72) = [1 0] x1 + [0]
[0 0] [0]
p(U81) = [1 0] x1 + [0]
[1 0] [1]
p(__) = [1 2] x1 + [1 0] x2 + [0]
[0 1] [0 1] [2]
p(a) = [0]
[0]
p(activate) = [1 0] x1 + [0]
[2 2] [0]
p(e) = [1]
[1]
p(i) = [0]
[2]
p(isList) = [2 0] x1 + [0]
[2 0] [1]
p(isNeList) = [2 0] x1 + [0]
[1 0] [0]
p(isNePal) = [2 0] x1 + [2]
[0 0] [0]
p(isPal) = [2 0] x1 + [2]
[2 1] [3]
p(isQid) = [2 0] x1 + [0]
[0 0] [0]
p(n____) = [1 2] x1 + [1 0] x2 + [0]
[0 0] [0 1] [2]
p(n__a) = [0]
[0]
p(n__e) = [1]
[1]
p(n__i) = [0]
[1]
p(n__nil) = [0]
[0]
p(n__o) = [3]
[0]
p(n__u) = [0]
[0]
p(nil) = [0]
[0]
p(o) = [3]
[0]
p(tt) = [0]
[0]
p(u) = [0]
[0]
Following rules are strictly oriented:
__(__(X,Y),Z) = [1 4] X + [1 2] Y + [1
0] Z + [4]
[0 1] [0 1] [0
1] [4]
> [1 2] X + [1 2] Y + [1
0] Z + [0]
[0 1] [0 1] [0
1] [4]
= __(X,__(Y,Z))
Following rules are (at-least) weakly oriented:
U11(tt()) = [0]
[1]
>= [0]
[0]
= tt()
U21(tt(),V2) = [2 0] V2 + [0]
[0 0] [1]
>= [2 0] V2 + [0]
[0 0] [1]
= U22(isList(activate(V2)))
U22(tt()) = [0]
[1]
>= [0]
[0]
= tt()
U31(tt()) = [0]
[0]
>= [0]
[0]
= tt()
U41(tt(),V2) = [2 0] V2 + [0]
[1 0] [0]
>= [2 0] V2 + [0]
[0 0] [0]
= U42(isNeList(activate(V2)))
U42(tt()) = [0]
[0]
>= [0]
[0]
= tt()
U51(tt(),V2) = [2 0] V2 + [0]
[0 0] [0]
>= [2 0] V2 + [0]
[0 0] [0]
= U52(isList(activate(V2)))
U52(tt()) = [0]
[0]
>= [0]
[0]
= tt()
U61(tt()) = [1]
[0]
>= [0]
[0]
= tt()
U71(tt(),P) = [2 0] P + [2]
[0 0] [0]
>= [2 0] P + [2]
[0 0] [0]
= U72(isPal(activate(P)))
U72(tt()) = [0]
[0]
>= [0]
[0]
= tt()
U81(tt()) = [0]
[1]
>= [0]
[0]
= tt()
__(X,nil()) = [1 2] X + [0]
[0 1] [2]
>= [1 0] X + [0]
[0 1] [0]
= X
__(X1,X2) = [1 2] X1 + [1 0] X2 + [0]
[0 1] [0 1] [2]
>= [1 2] X1 + [1 0] X2 + [0]
[0 0] [0 1] [2]
= n____(X1,X2)
__(nil(),X) = [1 0] X + [0]
[0 1] [2]
>= [1 0] X + [0]
[0 1] [0]
= X
a() = [0]
[0]
>= [0]
[0]
= n__a()
activate(X) = [1 0] X + [0]
[2 2] [0]
>= [1 0] X + [0]
[0 1] [0]
= X
activate(n____(X1,X2)) = [1 2] X1 + [1 0] X2 + [0]
[2 4] [2 2] [4]
>= [1 2] X1 + [1 0] X2 + [0]
[0 1] [0 1] [2]
= __(X1,X2)
activate(n__a()) = [0]
[0]
>= [0]
[0]
= a()
activate(n__e()) = [1]
[4]
>= [1]
[1]
= e()
activate(n__i()) = [0]
[2]
>= [0]
[2]
= i()
activate(n__nil()) = [0]
[0]
>= [0]
[0]
= nil()
activate(n__o()) = [3]
[6]
>= [3]
[0]
= o()
activate(n__u()) = [0]
[0]
>= [0]
[0]
= u()
e() = [1]
[1]
>= [1]
[1]
= n__e()
i() = [0]
[2]
>= [0]
[1]
= n__i()
isList(V) = [2 0] V + [0]
[2 0] [1]
>= [2 0] V + [0]
[2 0] [1]
= U11(isNeList(activate(V)))
isList(n____(V1,V2)) = [2 4] V1 + [2 0] V2 + [0]
[2 4] [2 0] [1]
>= [2 0] V1 + [2 0] V2 + [0]
[0 0] [0 0] [1]
= U21(isList(activate(V1))
,activate(V2))
isList(n__nil()) = [0]
[1]
>= [0]
[0]
= tt()
isNeList(V) = [2 0] V + [0]
[1 0] [0]
>= [2 0] V + [0]
[0 0] [0]
= U31(isQid(activate(V)))
isNeList(n____(V1,V2)) = [2 4] V1 + [2 0] V2 + [0]
[1 2] [1 0] [0]
>= [2 0] V1 + [2 0] V2 + [0]
[0 0] [1 0] [0]
= U41(isList(activate(V1))
,activate(V2))
isNeList(n____(V1,V2)) = [2 4] V1 + [2 0] V2 + [0]
[1 2] [1 0] [0]
>= [2 0] V1 + [2 0] V2 + [0]
[0 0] [0 0] [0]
= U51(isNeList(activate(V1))
,activate(V2))
isNePal(V) = [2 0] V + [2]
[0 0] [0]
>= [2 0] V + [1]
[0 0] [0]
= U61(isQid(activate(V)))
isNePal(n____(I,__(P,I))) = [4 4] I + [2 4] P + [2]
[0 0] [0 0] [0]
>= [4 0] I + [2 0] P + [2]
[0 0] [0 0] [0]
= U71(isQid(activate(I))
,activate(P))
isPal(V) = [2 0] V + [2]
[2 1] [3]
>= [2 0] V + [2]
[2 0] [3]
= U81(isNePal(activate(V)))
isPal(n__nil()) = [2]
[3]
>= [0]
[0]
= tt()
isQid(n__a()) = [0]
[0]
>= [0]
[0]
= tt()
isQid(n__e()) = [2]
[0]
>= [0]
[0]
= tt()
isQid(n__i()) = [0]
[0]
>= [0]
[0]
= tt()
isQid(n__o()) = [6]
[0]
>= [0]
[0]
= tt()
isQid(n__u()) = [0]
[0]
>= [0]
[0]
= tt()
nil() = [0]
[0]
>= [0]
[0]
= n__nil()
o() = [3]
[0]
>= [3]
[0]
= n__o()
u() = [0]
[0]
>= [0]
[0]
= n__u()
*** 1.1.1.1.1.1.1.1.1.1.1.1.1 Progress [(O(1),O(1))] ***
Considered Problem:
Strict DP Rules:
Strict TRS Rules:
Weak DP Rules:
Weak TRS Rules:
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()
__(X,nil()) -> X
__(X1,X2) -> n____(X1,X2)
__(__(X,Y),Z) -> __(X,__(Y,Z))
__(nil(),X) -> X
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:
Full
basic terms: {U11,U21,U22,U31,U41,U42,U51,U52,U61,U71,U72,U81,__,a,activate,e,i,isList,isNeList,isNePal,isPal,isQid,nil,o,u}/{n____,n__a,n__e,n__i,n__nil,n__o,n__u,tt}
Applied Processor:
EmptyProcessor
Proof:
The problem is already closed. The intended complexity is O(1).