* Step 1: Sum WORST_CASE(Omega(n^1),O(n^2))
+ Considered Problem:
- Strict TRS:
__(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)) -> __(activate(X1),activate(X2))
activate(n__a()) -> a()
activate(n__e()) -> e()
activate(n__i()) -> i()
activate(n__isList(X)) -> isList(X)
activate(n__isNeList(X)) -> isNeList(X)
activate(n__isPal(X)) -> isPal(X)
activate(n__nil()) -> nil()
activate(n__o()) -> o()
activate(n__u()) -> u()
and(tt(),X) -> activate(X)
e() -> n__e()
i() -> n__i()
isList(V) -> isNeList(activate(V))
isList(X) -> n__isList(X)
isList(n____(V1,V2)) -> and(isList(activate(V1)),n__isList(activate(V2)))
isList(n__nil()) -> tt()
isNeList(V) -> isQid(activate(V))
isNeList(X) -> n__isNeList(X)
isNeList(n____(V1,V2)) -> and(isList(activate(V1)),n__isNeList(activate(V2)))
isNeList(n____(V1,V2)) -> and(isNeList(activate(V1)),n__isList(activate(V2)))
isNePal(V) -> isQid(activate(V))
isNePal(n____(I,n____(P,I))) -> and(isQid(activate(I)),n__isPal(activate(P)))
isPal(V) -> isNePal(activate(V))
isPal(X) -> n__isPal(X)
isPal(n__nil()) -> tt()
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:
{__/2,a/0,activate/1,and/2,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__isList/1,n__isNeList/1,n__isPal/1,n__nil/0,n__o/0,n__u/0,tt/0}
- Obligation:
innermost runtime complexity wrt. defined symbols {__,a,activate,and,e,i,isList,isNeList,isNePal,isPal,isQid
,nil,o,u} and constructors {n____,n__a,n__e,n__i,n__isList,n__isNeList,n__isPal,n__nil,n__o,n__u,tt}
+ Applied Processor:
Sum {left = someStrategy, right = someStrategy}
+ Details:
()
** Step 1.a:1: DecreasingLoops WORST_CASE(Omega(n^1),?)
+ Considered Problem:
- Strict TRS:
__(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)) -> __(activate(X1),activate(X2))
activate(n__a()) -> a()
activate(n__e()) -> e()
activate(n__i()) -> i()
activate(n__isList(X)) -> isList(X)
activate(n__isNeList(X)) -> isNeList(X)
activate(n__isPal(X)) -> isPal(X)
activate(n__nil()) -> nil()
activate(n__o()) -> o()
activate(n__u()) -> u()
and(tt(),X) -> activate(X)
e() -> n__e()
i() -> n__i()
isList(V) -> isNeList(activate(V))
isList(X) -> n__isList(X)
isList(n____(V1,V2)) -> and(isList(activate(V1)),n__isList(activate(V2)))
isList(n__nil()) -> tt()
isNeList(V) -> isQid(activate(V))
isNeList(X) -> n__isNeList(X)
isNeList(n____(V1,V2)) -> and(isList(activate(V1)),n__isNeList(activate(V2)))
isNeList(n____(V1,V2)) -> and(isNeList(activate(V1)),n__isList(activate(V2)))
isNePal(V) -> isQid(activate(V))
isNePal(n____(I,n____(P,I))) -> and(isQid(activate(I)),n__isPal(activate(P)))
isPal(V) -> isNePal(activate(V))
isPal(X) -> n__isPal(X)
isPal(n__nil()) -> tt()
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:
{__/2,a/0,activate/1,and/2,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__isList/1,n__isNeList/1,n__isPal/1,n__nil/0,n__o/0,n__u/0,tt/0}
- Obligation:
innermost runtime complexity wrt. defined symbols {__,a,activate,and,e,i,isList,isNeList,isNePal,isPal,isQid
,nil,o,u} and constructors {n____,n__a,n__e,n__i,n__isList,n__isNeList,n__isPal,n__nil,n__o,n__u,tt}
+ Applied Processor:
DecreasingLoops {bound = AnyLoop, narrow = 10}
+ Details:
The system has following decreasing Loops:
activate(x){x -> n____(x,y)} =
activate(n____(x,y)) ->^+ __(activate(x),activate(y))
= C[activate(x) = activate(x){}]
** Step 1.b:1: InnermostRuleRemoval WORST_CASE(?,O(n^2))
+ Considered Problem:
- Strict TRS:
__(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)) -> __(activate(X1),activate(X2))
activate(n__a()) -> a()
activate(n__e()) -> e()
activate(n__i()) -> i()
activate(n__isList(X)) -> isList(X)
activate(n__isNeList(X)) -> isNeList(X)
activate(n__isPal(X)) -> isPal(X)
activate(n__nil()) -> nil()
activate(n__o()) -> o()
activate(n__u()) -> u()
and(tt(),X) -> activate(X)
e() -> n__e()
i() -> n__i()
isList(V) -> isNeList(activate(V))
isList(X) -> n__isList(X)
isList(n____(V1,V2)) -> and(isList(activate(V1)),n__isList(activate(V2)))
isList(n__nil()) -> tt()
isNeList(V) -> isQid(activate(V))
isNeList(X) -> n__isNeList(X)
isNeList(n____(V1,V2)) -> and(isList(activate(V1)),n__isNeList(activate(V2)))
isNeList(n____(V1,V2)) -> and(isNeList(activate(V1)),n__isList(activate(V2)))
isNePal(V) -> isQid(activate(V))
isNePal(n____(I,n____(P,I))) -> and(isQid(activate(I)),n__isPal(activate(P)))
isPal(V) -> isNePal(activate(V))
isPal(X) -> n__isPal(X)
isPal(n__nil()) -> tt()
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:
{__/2,a/0,activate/1,and/2,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__isList/1,n__isNeList/1,n__isPal/1,n__nil/0,n__o/0,n__u/0,tt/0}
- Obligation:
innermost runtime complexity wrt. defined symbols {__,a,activate,and,e,i,isList,isNeList,isNePal,isPal,isQid
,nil,o,u} and constructors {n____,n__a,n__e,n__i,n__isList,n__isNeList,n__isPal,n__nil,n__o,n__u,tt}
+ Applied Processor:
InnermostRuleRemoval
+ Details:
Arguments of following rules are not normal-forms.
__(X,nil()) -> X
__(__(X,Y),Z) -> __(X,__(Y,Z))
__(nil(),X) -> X
All above mentioned rules can be savely removed.
** Step 1.b:2: WeightGap WORST_CASE(?,O(n^2))
+ Considered Problem:
- Strict TRS:
__(X1,X2) -> n____(X1,X2)
a() -> n__a()
activate(X) -> X
activate(n____(X1,X2)) -> __(activate(X1),activate(X2))
activate(n__a()) -> a()
activate(n__e()) -> e()
activate(n__i()) -> i()
activate(n__isList(X)) -> isList(X)
activate(n__isNeList(X)) -> isNeList(X)
activate(n__isPal(X)) -> isPal(X)
activate(n__nil()) -> nil()
activate(n__o()) -> o()
activate(n__u()) -> u()
and(tt(),X) -> activate(X)
e() -> n__e()
i() -> n__i()
isList(V) -> isNeList(activate(V))
isList(X) -> n__isList(X)
isList(n____(V1,V2)) -> and(isList(activate(V1)),n__isList(activate(V2)))
isList(n__nil()) -> tt()
isNeList(V) -> isQid(activate(V))
isNeList(X) -> n__isNeList(X)
isNeList(n____(V1,V2)) -> and(isList(activate(V1)),n__isNeList(activate(V2)))
isNeList(n____(V1,V2)) -> and(isNeList(activate(V1)),n__isList(activate(V2)))
isNePal(V) -> isQid(activate(V))
isNePal(n____(I,n____(P,I))) -> and(isQid(activate(I)),n__isPal(activate(P)))
isPal(V) -> isNePal(activate(V))
isPal(X) -> n__isPal(X)
isPal(n__nil()) -> tt()
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:
{__/2,a/0,activate/1,and/2,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__isList/1,n__isNeList/1,n__isPal/1,n__nil/0,n__o/0,n__u/0,tt/0}
- Obligation:
innermost runtime complexity wrt. defined symbols {__,a,activate,and,e,i,isList,isNeList,isNePal,isPal,isQid
,nil,o,u} and constructors {n____,n__a,n__e,n__i,n__isList,n__isNeList,n__isPal,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(__) = {1,2},
uargs(and) = {1,2},
uargs(isList) = {1},
uargs(isNeList) = {1},
uargs(isNePal) = {1},
uargs(isQid) = {1},
uargs(n__isList) = {1},
uargs(n__isNeList) = {1},
uargs(n__isPal) = {1}
Following symbols are considered usable:
all
TcT has computed the following interpretation:
p(__) = [1] x1 + [1] x2 + [1]
p(a) = [0]
p(activate) = [1] x1 + [0]
p(and) = [1] x1 + [1] x2 + [5]
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__isList) = [1] x1 + [0]
p(n__isNeList) = [1] x1 + [3]
p(n__isPal) = [1] x1 + [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:
__(X1,X2) = [1] X1 + [1] X2 + [1]
> [1] X1 + [1] X2 + [0]
= n____(X1,X2)
activate(n__a()) = [5]
> [0]
= a()
activate(n__isNeList(X)) = [1] X + [3]
> [1] X + [0]
= isNeList(X)
and(tt(),X) = [1] X + [5]
> [1] X + [0]
= activate(X)
isQid(n__a()) = [5]
> [0]
= tt()
Following rules are (at-least) weakly oriented:
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 + [1]
= __(activate(X1),activate(X2))
activate(n__e()) = [0]
>= [0]
= e()
activate(n__i()) = [0]
>= [0]
= i()
activate(n__isList(X)) = [1] X + [0]
>= [1] X + [0]
= isList(X)
activate(n__isPal(X)) = [1] X + [0]
>= [1] X + [0]
= isPal(X)
activate(n__nil()) = [0]
>= [0]
= nil()
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 + [0]
>= [1] V + [0]
= isNeList(activate(V))
isList(X) = [1] X + [0]
>= [1] X + [0]
= n__isList(X)
isList(n____(V1,V2)) = [1] V1 + [1] V2 + [0]
>= [1] V1 + [1] V2 + [5]
= and(isList(activate(V1)),n__isList(activate(V2)))
isList(n__nil()) = [0]
>= [0]
= tt()
isNeList(V) = [1] V + [0]
>= [1] V + [0]
= isQid(activate(V))
isNeList(X) = [1] X + [0]
>= [1] X + [3]
= n__isNeList(X)
isNeList(n____(V1,V2)) = [1] V1 + [1] V2 + [0]
>= [1] V1 + [1] V2 + [8]
= and(isList(activate(V1)),n__isNeList(activate(V2)))
isNeList(n____(V1,V2)) = [1] V1 + [1] V2 + [0]
>= [1] V1 + [1] V2 + [5]
= and(isNeList(activate(V1)),n__isList(activate(V2)))
isNePal(V) = [1] V + [0]
>= [1] V + [0]
= isQid(activate(V))
isNePal(n____(I,n____(P,I))) = [2] I + [1] P + [0]
>= [1] I + [1] P + [5]
= and(isQid(activate(I)),n__isPal(activate(P)))
isPal(V) = [1] V + [0]
>= [1] V + [0]
= isNePal(activate(V))
isPal(X) = [1] X + [0]
>= [1] X + [0]
= n__isPal(X)
isPal(n__nil()) = [0]
>= [0]
= tt()
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()
u() = [0]
>= [0]
= n__u()
Further, it can be verified that all rules not oriented are covered by the weightgap condition.
** Step 1.b:3: WeightGap WORST_CASE(?,O(n^2))
+ Considered Problem:
- Strict TRS:
a() -> n__a()
activate(X) -> X
activate(n____(X1,X2)) -> __(activate(X1),activate(X2))
activate(n__e()) -> e()
activate(n__i()) -> i()
activate(n__isList(X)) -> isList(X)
activate(n__isPal(X)) -> isPal(X)
activate(n__nil()) -> nil()
activate(n__o()) -> o()
activate(n__u()) -> u()
e() -> n__e()
i() -> n__i()
isList(V) -> isNeList(activate(V))
isList(X) -> n__isList(X)
isList(n____(V1,V2)) -> and(isList(activate(V1)),n__isList(activate(V2)))
isList(n__nil()) -> tt()
isNeList(V) -> isQid(activate(V))
isNeList(X) -> n__isNeList(X)
isNeList(n____(V1,V2)) -> and(isList(activate(V1)),n__isNeList(activate(V2)))
isNeList(n____(V1,V2)) -> and(isNeList(activate(V1)),n__isList(activate(V2)))
isNePal(V) -> isQid(activate(V))
isNePal(n____(I,n____(P,I))) -> and(isQid(activate(I)),n__isPal(activate(P)))
isPal(V) -> isNePal(activate(V))
isPal(X) -> n__isPal(X)
isPal(n__nil()) -> tt()
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 TRS:
__(X1,X2) -> n____(X1,X2)
activate(n__a()) -> a()
activate(n__isNeList(X)) -> isNeList(X)
and(tt(),X) -> activate(X)
isQid(n__a()) -> tt()
- Signature:
{__/2,a/0,activate/1,and/2,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__isList/1,n__isNeList/1,n__isPal/1,n__nil/0,n__o/0,n__u/0,tt/0}
- Obligation:
innermost runtime complexity wrt. defined symbols {__,a,activate,and,e,i,isList,isNeList,isNePal,isPal,isQid
,nil,o,u} and constructors {n____,n__a,n__e,n__i,n__isList,n__isNeList,n__isPal,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(__) = {1,2},
uargs(and) = {1,2},
uargs(isList) = {1},
uargs(isNeList) = {1},
uargs(isNePal) = {1},
uargs(isQid) = {1},
uargs(n__isList) = {1},
uargs(n__isNeList) = {1},
uargs(n__isPal) = {1}
Following symbols are considered usable:
all
TcT has computed the following interpretation:
p(__) = [1] x1 + [1] x2 + [5]
p(a) = [0]
p(activate) = [1] x1 + [0]
p(and) = [1] x1 + [1] x2 + [0]
p(e) = [1]
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) = [0]
p(n__i) = [0]
p(n__isList) = [1] x1 + [0]
p(n__isNeList) = [1] x1 + [0]
p(n__isPal) = [1] x1 + [0]
p(n__nil) = [5]
p(n__o) = [0]
p(n__u) = [4]
p(nil) = [0]
p(o) = [0]
p(tt) = [0]
p(u) = [5]
Following rules are strictly oriented:
activate(n__nil()) = [5]
> [0]
= nil()
e() = [1]
> [0]
= n__e()
isList(n__nil()) = [5]
> [0]
= tt()
isPal(n__nil()) = [5]
> [0]
= tt()
isQid(n__u()) = [4]
> [0]
= tt()
u() = [5]
> [4]
= n__u()
Following rules are (at-least) weakly oriented:
__(X1,X2) = [1] X1 + [1] X2 + [5]
>= [1] X1 + [1] X2 + [0]
= n____(X1,X2)
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 + [5]
= __(activate(X1),activate(X2))
activate(n__a()) = [0]
>= [0]
= a()
activate(n__e()) = [0]
>= [1]
= e()
activate(n__i()) = [0]
>= [0]
= i()
activate(n__isList(X)) = [1] X + [0]
>= [1] X + [0]
= isList(X)
activate(n__isNeList(X)) = [1] X + [0]
>= [1] X + [0]
= isNeList(X)
activate(n__isPal(X)) = [1] X + [0]
>= [1] X + [0]
= isPal(X)
activate(n__o()) = [0]
>= [0]
= o()
activate(n__u()) = [4]
>= [5]
= u()
and(tt(),X) = [1] X + [0]
>= [1] X + [0]
= activate(X)
i() = [0]
>= [0]
= n__i()
isList(V) = [1] V + [0]
>= [1] V + [0]
= isNeList(activate(V))
isList(X) = [1] X + [0]
>= [1] X + [0]
= n__isList(X)
isList(n____(V1,V2)) = [1] V1 + [1] V2 + [0]
>= [1] V1 + [1] V2 + [0]
= and(isList(activate(V1)),n__isList(activate(V2)))
isNeList(V) = [1] V + [0]
>= [1] V + [0]
= isQid(activate(V))
isNeList(X) = [1] X + [0]
>= [1] X + [0]
= n__isNeList(X)
isNeList(n____(V1,V2)) = [1] V1 + [1] V2 + [0]
>= [1] V1 + [1] V2 + [0]
= and(isList(activate(V1)),n__isNeList(activate(V2)))
isNeList(n____(V1,V2)) = [1] V1 + [1] V2 + [0]
>= [1] V1 + [1] V2 + [0]
= and(isNeList(activate(V1)),n__isList(activate(V2)))
isNePal(V) = [1] V + [0]
>= [1] V + [0]
= isQid(activate(V))
isNePal(n____(I,n____(P,I))) = [2] I + [1] P + [0]
>= [1] I + [1] P + [0]
= and(isQid(activate(I)),n__isPal(activate(P)))
isPal(V) = [1] V + [0]
>= [1] V + [0]
= isNePal(activate(V))
isPal(X) = [1] X + [0]
>= [1] X + [0]
= n__isPal(X)
isQid(n__a()) = [0]
>= [0]
= tt()
isQid(n__e()) = [0]
>= [0]
= tt()
isQid(n__i()) = [0]
>= [0]
= tt()
isQid(n__o()) = [0]
>= [0]
= tt()
nil() = [0]
>= [5]
= n__nil()
o() = [0]
>= [0]
= n__o()
Further, it can be verified that all rules not oriented are covered by the weightgap condition.
** Step 1.b:4: WeightGap WORST_CASE(?,O(n^2))
+ Considered Problem:
- Strict TRS:
a() -> n__a()
activate(X) -> X
activate(n____(X1,X2)) -> __(activate(X1),activate(X2))
activate(n__e()) -> e()
activate(n__i()) -> i()
activate(n__isList(X)) -> isList(X)
activate(n__isPal(X)) -> isPal(X)
activate(n__o()) -> o()
activate(n__u()) -> u()
i() -> n__i()
isList(V) -> isNeList(activate(V))
isList(X) -> n__isList(X)
isList(n____(V1,V2)) -> and(isList(activate(V1)),n__isList(activate(V2)))
isNeList(V) -> isQid(activate(V))
isNeList(X) -> n__isNeList(X)
isNeList(n____(V1,V2)) -> and(isList(activate(V1)),n__isNeList(activate(V2)))
isNeList(n____(V1,V2)) -> and(isNeList(activate(V1)),n__isList(activate(V2)))
isNePal(V) -> isQid(activate(V))
isNePal(n____(I,n____(P,I))) -> and(isQid(activate(I)),n__isPal(activate(P)))
isPal(V) -> isNePal(activate(V))
isPal(X) -> n__isPal(X)
isQid(n__e()) -> tt()
isQid(n__i()) -> tt()
isQid(n__o()) -> tt()
nil() -> n__nil()
o() -> n__o()
- Weak TRS:
__(X1,X2) -> n____(X1,X2)
activate(n__a()) -> a()
activate(n__isNeList(X)) -> isNeList(X)
activate(n__nil()) -> nil()
and(tt(),X) -> activate(X)
e() -> n__e()
isList(n__nil()) -> tt()
isPal(n__nil()) -> tt()
isQid(n__a()) -> tt()
isQid(n__u()) -> tt()
u() -> n__u()
- Signature:
{__/2,a/0,activate/1,and/2,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__isList/1,n__isNeList/1,n__isPal/1,n__nil/0,n__o/0,n__u/0,tt/0}
- Obligation:
innermost runtime complexity wrt. defined symbols {__,a,activate,and,e,i,isList,isNeList,isNePal,isPal,isQid
,nil,o,u} and constructors {n____,n__a,n__e,n__i,n__isList,n__isNeList,n__isPal,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(__) = {1,2},
uargs(and) = {1,2},
uargs(isList) = {1},
uargs(isNeList) = {1},
uargs(isNePal) = {1},
uargs(isQid) = {1},
uargs(n__isList) = {1},
uargs(n__isNeList) = {1},
uargs(n__isPal) = {1}
Following symbols are considered usable:
all
TcT has computed the following interpretation:
p(__) = [1] x1 + [1] x2 + [0]
p(a) = [0]
p(activate) = [1] x1 + [0]
p(and) = [1] x1 + [1] x2 + [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) = [0]
p(n__i) = [0]
p(n__isList) = [1] x1 + [0]
p(n__isNeList) = [1] x1 + [0]
p(n__isPal) = [1] x1 + [0]
p(n__nil) = [0]
p(n__o) = [2]
p(n__u) = [0]
p(nil) = [0]
p(o) = [3]
p(tt) = [0]
p(u) = [0]
Following rules are strictly oriented:
isQid(n__o()) = [2]
> [0]
= tt()
o() = [3]
> [2]
= n__o()
Following rules are (at-least) weakly oriented:
__(X1,X2) = [1] X1 + [1] X2 + [0]
>= [1] X1 + [1] X2 + [0]
= n____(X1,X2)
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]
= __(activate(X1),activate(X2))
activate(n__a()) = [0]
>= [0]
= a()
activate(n__e()) = [0]
>= [0]
= e()
activate(n__i()) = [0]
>= [0]
= i()
activate(n__isList(X)) = [1] X + [0]
>= [1] X + [0]
= isList(X)
activate(n__isNeList(X)) = [1] X + [0]
>= [1] X + [0]
= isNeList(X)
activate(n__isPal(X)) = [1] X + [0]
>= [1] X + [0]
= isPal(X)
activate(n__nil()) = [0]
>= [0]
= nil()
activate(n__o()) = [2]
>= [3]
= o()
activate(n__u()) = [0]
>= [0]
= u()
and(tt(),X) = [1] X + [0]
>= [1] X + [0]
= activate(X)
e() = [0]
>= [0]
= n__e()
i() = [0]
>= [0]
= n__i()
isList(V) = [1] V + [0]
>= [1] V + [0]
= isNeList(activate(V))
isList(X) = [1] X + [0]
>= [1] X + [0]
= n__isList(X)
isList(n____(V1,V2)) = [1] V1 + [1] V2 + [0]
>= [1] V1 + [1] V2 + [0]
= and(isList(activate(V1)),n__isList(activate(V2)))
isList(n__nil()) = [0]
>= [0]
= tt()
isNeList(V) = [1] V + [0]
>= [1] V + [0]
= isQid(activate(V))
isNeList(X) = [1] X + [0]
>= [1] X + [0]
= n__isNeList(X)
isNeList(n____(V1,V2)) = [1] V1 + [1] V2 + [0]
>= [1] V1 + [1] V2 + [0]
= and(isList(activate(V1)),n__isNeList(activate(V2)))
isNeList(n____(V1,V2)) = [1] V1 + [1] V2 + [0]
>= [1] V1 + [1] V2 + [0]
= and(isNeList(activate(V1)),n__isList(activate(V2)))
isNePal(V) = [1] V + [0]
>= [1] V + [0]
= isQid(activate(V))
isNePal(n____(I,n____(P,I))) = [2] I + [1] P + [0]
>= [1] I + [1] P + [0]
= and(isQid(activate(I)),n__isPal(activate(P)))
isPal(V) = [1] V + [0]
>= [1] V + [0]
= isNePal(activate(V))
isPal(X) = [1] X + [0]
>= [1] X + [0]
= n__isPal(X)
isPal(n__nil()) = [0]
>= [0]
= tt()
isQid(n__a()) = [0]
>= [0]
= tt()
isQid(n__e()) = [0]
>= [0]
= tt()
isQid(n__i()) = [0]
>= [0]
= tt()
isQid(n__u()) = [0]
>= [0]
= tt()
nil() = [0]
>= [0]
= n__nil()
u() = [0]
>= [0]
= n__u()
Further, it can be verified that all rules not oriented are covered by the weightgap condition.
** Step 1.b:5: WeightGap WORST_CASE(?,O(n^2))
+ Considered Problem:
- Strict TRS:
a() -> n__a()
activate(X) -> X
activate(n____(X1,X2)) -> __(activate(X1),activate(X2))
activate(n__e()) -> e()
activate(n__i()) -> i()
activate(n__isList(X)) -> isList(X)
activate(n__isPal(X)) -> isPal(X)
activate(n__o()) -> o()
activate(n__u()) -> u()
i() -> n__i()
isList(V) -> isNeList(activate(V))
isList(X) -> n__isList(X)
isList(n____(V1,V2)) -> and(isList(activate(V1)),n__isList(activate(V2)))
isNeList(V) -> isQid(activate(V))
isNeList(X) -> n__isNeList(X)
isNeList(n____(V1,V2)) -> and(isList(activate(V1)),n__isNeList(activate(V2)))
isNeList(n____(V1,V2)) -> and(isNeList(activate(V1)),n__isList(activate(V2)))
isNePal(V) -> isQid(activate(V))
isNePal(n____(I,n____(P,I))) -> and(isQid(activate(I)),n__isPal(activate(P)))
isPal(V) -> isNePal(activate(V))
isPal(X) -> n__isPal(X)
isQid(n__e()) -> tt()
isQid(n__i()) -> tt()
nil() -> n__nil()
- Weak TRS:
__(X1,X2) -> n____(X1,X2)
activate(n__a()) -> a()
activate(n__isNeList(X)) -> isNeList(X)
activate(n__nil()) -> nil()
and(tt(),X) -> activate(X)
e() -> n__e()
isList(n__nil()) -> tt()
isPal(n__nil()) -> tt()
isQid(n__a()) -> tt()
isQid(n__o()) -> tt()
isQid(n__u()) -> tt()
o() -> n__o()
u() -> n__u()
- Signature:
{__/2,a/0,activate/1,and/2,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__isList/1,n__isNeList/1,n__isPal/1,n__nil/0,n__o/0,n__u/0,tt/0}
- Obligation:
innermost runtime complexity wrt. defined symbols {__,a,activate,and,e,i,isList,isNeList,isNePal,isPal,isQid
,nil,o,u} and constructors {n____,n__a,n__e,n__i,n__isList,n__isNeList,n__isPal,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(__) = {1,2},
uargs(and) = {1,2},
uargs(isList) = {1},
uargs(isNeList) = {1},
uargs(isNePal) = {1},
uargs(isQid) = {1},
uargs(n__isList) = {1},
uargs(n__isNeList) = {1},
uargs(n__isPal) = {1}
Following symbols are considered usable:
all
TcT has computed the following interpretation:
p(__) = [1] x1 + [1] x2 + [3]
p(a) = [3]
p(activate) = [1] x1 + [2]
p(and) = [1] x1 + [1] x2 + [1]
p(e) = [5]
p(i) = [0]
p(isList) = [1] x1 + [2]
p(isNeList) = [1] x1 + [2]
p(isNePal) = [1] x1 + [0]
p(isPal) = [1] x1 + [3]
p(isQid) = [1] x1 + [0]
p(n____) = [1] x1 + [1] x2 + [2]
p(n__a) = [1]
p(n__e) = [5]
p(n__i) = [0]
p(n__isList) = [1] x1 + [1]
p(n__isNeList) = [1] x1 + [0]
p(n__isPal) = [1] x1 + [0]
p(n__nil) = [0]
p(n__o) = [1]
p(n__u) = [2]
p(nil) = [0]
p(o) = [1]
p(tt) = [1]
p(u) = [2]
Following rules are strictly oriented:
a() = [3]
> [1]
= n__a()
activate(X) = [1] X + [2]
> [1] X + [0]
= X
activate(n__e()) = [7]
> [5]
= e()
activate(n__i()) = [2]
> [0]
= i()
activate(n__isList(X)) = [1] X + [3]
> [1] X + [2]
= isList(X)
activate(n__o()) = [3]
> [1]
= o()
activate(n__u()) = [4]
> [2]
= u()
isList(X) = [1] X + [2]
> [1] X + [1]
= n__isList(X)
isNeList(X) = [1] X + [2]
> [1] X + [0]
= n__isNeList(X)
isPal(V) = [1] V + [3]
> [1] V + [2]
= isNePal(activate(V))
isPal(X) = [1] X + [3]
> [1] X + [0]
= n__isPal(X)
isQid(n__e()) = [5]
> [1]
= tt()
Following rules are (at-least) weakly oriented:
__(X1,X2) = [1] X1 + [1] X2 + [3]
>= [1] X1 + [1] X2 + [2]
= n____(X1,X2)
activate(n____(X1,X2)) = [1] X1 + [1] X2 + [4]
>= [1] X1 + [1] X2 + [7]
= __(activate(X1),activate(X2))
activate(n__a()) = [3]
>= [3]
= a()
activate(n__isNeList(X)) = [1] X + [2]
>= [1] X + [2]
= isNeList(X)
activate(n__isPal(X)) = [1] X + [2]
>= [1] X + [3]
= isPal(X)
activate(n__nil()) = [2]
>= [0]
= nil()
and(tt(),X) = [1] X + [2]
>= [1] X + [2]
= activate(X)
e() = [5]
>= [5]
= n__e()
i() = [0]
>= [0]
= n__i()
isList(V) = [1] V + [2]
>= [1] V + [4]
= isNeList(activate(V))
isList(n____(V1,V2)) = [1] V1 + [1] V2 + [4]
>= [1] V1 + [1] V2 + [8]
= and(isList(activate(V1)),n__isList(activate(V2)))
isList(n__nil()) = [2]
>= [1]
= tt()
isNeList(V) = [1] V + [2]
>= [1] V + [2]
= isQid(activate(V))
isNeList(n____(V1,V2)) = [1] V1 + [1] V2 + [4]
>= [1] V1 + [1] V2 + [7]
= and(isList(activate(V1)),n__isNeList(activate(V2)))
isNeList(n____(V1,V2)) = [1] V1 + [1] V2 + [4]
>= [1] V1 + [1] V2 + [8]
= and(isNeList(activate(V1)),n__isList(activate(V2)))
isNePal(V) = [1] V + [0]
>= [1] V + [2]
= isQid(activate(V))
isNePal(n____(I,n____(P,I))) = [2] I + [1] P + [4]
>= [1] I + [1] P + [5]
= and(isQid(activate(I)),n__isPal(activate(P)))
isPal(n__nil()) = [3]
>= [1]
= tt()
isQid(n__a()) = [1]
>= [1]
= tt()
isQid(n__i()) = [0]
>= [1]
= tt()
isQid(n__o()) = [1]
>= [1]
= tt()
isQid(n__u()) = [2]
>= [1]
= tt()
nil() = [0]
>= [0]
= n__nil()
o() = [1]
>= [1]
= n__o()
u() = [2]
>= [2]
= n__u()
Further, it can be verified that all rules not oriented are covered by the weightgap condition.
** Step 1.b:6: WeightGap WORST_CASE(?,O(n^2))
+ Considered Problem:
- Strict TRS:
activate(n____(X1,X2)) -> __(activate(X1),activate(X2))
activate(n__isPal(X)) -> isPal(X)
i() -> n__i()
isList(V) -> isNeList(activate(V))
isList(n____(V1,V2)) -> and(isList(activate(V1)),n__isList(activate(V2)))
isNeList(V) -> isQid(activate(V))
isNeList(n____(V1,V2)) -> and(isList(activate(V1)),n__isNeList(activate(V2)))
isNeList(n____(V1,V2)) -> and(isNeList(activate(V1)),n__isList(activate(V2)))
isNePal(V) -> isQid(activate(V))
isNePal(n____(I,n____(P,I))) -> and(isQid(activate(I)),n__isPal(activate(P)))
isQid(n__i()) -> tt()
nil() -> n__nil()
- Weak TRS:
__(X1,X2) -> n____(X1,X2)
a() -> n__a()
activate(X) -> X
activate(n__a()) -> a()
activate(n__e()) -> e()
activate(n__i()) -> i()
activate(n__isList(X)) -> isList(X)
activate(n__isNeList(X)) -> isNeList(X)
activate(n__nil()) -> nil()
activate(n__o()) -> o()
activate(n__u()) -> u()
and(tt(),X) -> activate(X)
e() -> n__e()
isList(X) -> n__isList(X)
isList(n__nil()) -> tt()
isNeList(X) -> n__isNeList(X)
isPal(V) -> isNePal(activate(V))
isPal(X) -> n__isPal(X)
isPal(n__nil()) -> tt()
isQid(n__a()) -> tt()
isQid(n__e()) -> tt()
isQid(n__o()) -> tt()
isQid(n__u()) -> tt()
o() -> n__o()
u() -> n__u()
- Signature:
{__/2,a/0,activate/1,and/2,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__isList/1,n__isNeList/1,n__isPal/1,n__nil/0,n__o/0,n__u/0,tt/0}
- Obligation:
innermost runtime complexity wrt. defined symbols {__,a,activate,and,e,i,isList,isNeList,isNePal,isPal,isQid
,nil,o,u} and constructors {n____,n__a,n__e,n__i,n__isList,n__isNeList,n__isPal,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(__) = {1,2},
uargs(and) = {1,2},
uargs(isList) = {1},
uargs(isNeList) = {1},
uargs(isNePal) = {1},
uargs(isQid) = {1},
uargs(n__isList) = {1},
uargs(n__isNeList) = {1},
uargs(n__isPal) = {1}
Following symbols are considered usable:
all
TcT has computed the following interpretation:
p(__) = [1] x1 + [1] x2 + [4]
p(a) = [0]
p(activate) = [1] x1 + [0]
p(and) = [1] x1 + [1] x2 + [0]
p(e) = [0]
p(i) = [1]
p(isList) = [1] x1 + [4]
p(isNeList) = [1] x1 + [0]
p(isNePal) = [1] x1 + [5]
p(isPal) = [1] x1 + [5]
p(isQid) = [1] x1 + [6]
p(n____) = [1] x1 + [1] x2 + [3]
p(n__a) = [0]
p(n__e) = [0]
p(n__i) = [1]
p(n__isList) = [1] x1 + [4]
p(n__isNeList) = [1] x1 + [0]
p(n__isPal) = [1] x1 + [4]
p(n__nil) = [2]
p(n__o) = [2]
p(n__u) = [0]
p(nil) = [0]
p(o) = [2]
p(tt) = [6]
p(u) = [0]
Following rules are strictly oriented:
isList(V) = [1] V + [4]
> [1] V + [0]
= isNeList(activate(V))
isNePal(n____(I,n____(P,I))) = [2] I + [1] P + [11]
> [1] I + [1] P + [10]
= and(isQid(activate(I)),n__isPal(activate(P)))
isQid(n__i()) = [7]
> [6]
= tt()
Following rules are (at-least) weakly oriented:
__(X1,X2) = [1] X1 + [1] X2 + [4]
>= [1] X1 + [1] X2 + [3]
= n____(X1,X2)
a() = [0]
>= [0]
= n__a()
activate(X) = [1] X + [0]
>= [1] X + [0]
= X
activate(n____(X1,X2)) = [1] X1 + [1] X2 + [3]
>= [1] X1 + [1] X2 + [4]
= __(activate(X1),activate(X2))
activate(n__a()) = [0]
>= [0]
= a()
activate(n__e()) = [0]
>= [0]
= e()
activate(n__i()) = [1]
>= [1]
= i()
activate(n__isList(X)) = [1] X + [4]
>= [1] X + [4]
= isList(X)
activate(n__isNeList(X)) = [1] X + [0]
>= [1] X + [0]
= isNeList(X)
activate(n__isPal(X)) = [1] X + [4]
>= [1] X + [5]
= isPal(X)
activate(n__nil()) = [2]
>= [0]
= nil()
activate(n__o()) = [2]
>= [2]
= o()
activate(n__u()) = [0]
>= [0]
= u()
and(tt(),X) = [1] X + [6]
>= [1] X + [0]
= activate(X)
e() = [0]
>= [0]
= n__e()
i() = [1]
>= [1]
= n__i()
isList(X) = [1] X + [4]
>= [1] X + [4]
= n__isList(X)
isList(n____(V1,V2)) = [1] V1 + [1] V2 + [7]
>= [1] V1 + [1] V2 + [8]
= and(isList(activate(V1)),n__isList(activate(V2)))
isList(n__nil()) = [6]
>= [6]
= tt()
isNeList(V) = [1] V + [0]
>= [1] V + [6]
= isQid(activate(V))
isNeList(X) = [1] X + [0]
>= [1] X + [0]
= n__isNeList(X)
isNeList(n____(V1,V2)) = [1] V1 + [1] V2 + [3]
>= [1] V1 + [1] V2 + [4]
= and(isList(activate(V1)),n__isNeList(activate(V2)))
isNeList(n____(V1,V2)) = [1] V1 + [1] V2 + [3]
>= [1] V1 + [1] V2 + [4]
= and(isNeList(activate(V1)),n__isList(activate(V2)))
isNePal(V) = [1] V + [5]
>= [1] V + [6]
= isQid(activate(V))
isPal(V) = [1] V + [5]
>= [1] V + [5]
= isNePal(activate(V))
isPal(X) = [1] X + [5]
>= [1] X + [4]
= n__isPal(X)
isPal(n__nil()) = [7]
>= [6]
= tt()
isQid(n__a()) = [6]
>= [6]
= tt()
isQid(n__e()) = [6]
>= [6]
= tt()
isQid(n__o()) = [8]
>= [6]
= tt()
isQid(n__u()) = [6]
>= [6]
= tt()
nil() = [0]
>= [2]
= n__nil()
o() = [2]
>= [2]
= n__o()
u() = [0]
>= [0]
= n__u()
Further, it can be verified that all rules not oriented are covered by the weightgap condition.
** Step 1.b:7: WeightGap WORST_CASE(?,O(n^2))
+ Considered Problem:
- Strict TRS:
activate(n____(X1,X2)) -> __(activate(X1),activate(X2))
activate(n__isPal(X)) -> isPal(X)
i() -> n__i()
isList(n____(V1,V2)) -> and(isList(activate(V1)),n__isList(activate(V2)))
isNeList(V) -> isQid(activate(V))
isNeList(n____(V1,V2)) -> and(isList(activate(V1)),n__isNeList(activate(V2)))
isNeList(n____(V1,V2)) -> and(isNeList(activate(V1)),n__isList(activate(V2)))
isNePal(V) -> isQid(activate(V))
nil() -> n__nil()
- Weak TRS:
__(X1,X2) -> n____(X1,X2)
a() -> n__a()
activate(X) -> X
activate(n__a()) -> a()
activate(n__e()) -> e()
activate(n__i()) -> i()
activate(n__isList(X)) -> isList(X)
activate(n__isNeList(X)) -> isNeList(X)
activate(n__nil()) -> nil()
activate(n__o()) -> o()
activate(n__u()) -> u()
and(tt(),X) -> activate(X)
e() -> n__e()
isList(V) -> isNeList(activate(V))
isList(X) -> n__isList(X)
isList(n__nil()) -> tt()
isNeList(X) -> n__isNeList(X)
isNePal(n____(I,n____(P,I))) -> and(isQid(activate(I)),n__isPal(activate(P)))
isPal(V) -> isNePal(activate(V))
isPal(X) -> n__isPal(X)
isPal(n__nil()) -> tt()
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:
{__/2,a/0,activate/1,and/2,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__isList/1,n__isNeList/1,n__isPal/1,n__nil/0,n__o/0,n__u/0,tt/0}
- Obligation:
innermost runtime complexity wrt. defined symbols {__,a,activate,and,e,i,isList,isNeList,isNePal,isPal,isQid
,nil,o,u} and constructors {n____,n__a,n__e,n__i,n__isList,n__isNeList,n__isPal,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(__) = {1,2},
uargs(and) = {1,2},
uargs(isList) = {1},
uargs(isNeList) = {1},
uargs(isNePal) = {1},
uargs(isQid) = {1},
uargs(n__isList) = {1},
uargs(n__isNeList) = {1},
uargs(n__isPal) = {1}
Following symbols are considered usable:
all
TcT has computed the following interpretation:
p(__) = [1] x1 + [1] x2 + [1]
p(a) = [2]
p(activate) = [1] x1 + [0]
p(and) = [1] x1 + [1] x2 + [0]
p(e) = [2]
p(i) = [0]
p(isList) = [1] x1 + [0]
p(isNeList) = [1] x1 + [0]
p(isNePal) = [1] x1 + [4]
p(isPal) = [1] x1 + [4]
p(isQid) = [1] x1 + [2]
p(n____) = [1] x1 + [1] x2 + [1]
p(n__a) = [2]
p(n__e) = [2]
p(n__i) = [0]
p(n__isList) = [1] x1 + [0]
p(n__isNeList) = [1] x1 + [0]
p(n__isPal) = [1] x1 + [4]
p(n__nil) = [4]
p(n__o) = [1]
p(n__u) = [7]
p(nil) = [4]
p(o) = [1]
p(tt) = [0]
p(u) = [7]
Following rules are strictly oriented:
isList(n____(V1,V2)) = [1] V1 + [1] V2 + [1]
> [1] V1 + [1] V2 + [0]
= and(isList(activate(V1)),n__isList(activate(V2)))
isNeList(n____(V1,V2)) = [1] V1 + [1] V2 + [1]
> [1] V1 + [1] V2 + [0]
= and(isList(activate(V1)),n__isNeList(activate(V2)))
isNeList(n____(V1,V2)) = [1] V1 + [1] V2 + [1]
> [1] V1 + [1] V2 + [0]
= and(isNeList(activate(V1)),n__isList(activate(V2)))
isNePal(V) = [1] V + [4]
> [1] V + [2]
= isQid(activate(V))
Following rules are (at-least) weakly oriented:
__(X1,X2) = [1] X1 + [1] X2 + [1]
>= [1] X1 + [1] X2 + [1]
= n____(X1,X2)
a() = [2]
>= [2]
= 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]
= __(activate(X1),activate(X2))
activate(n__a()) = [2]
>= [2]
= a()
activate(n__e()) = [2]
>= [2]
= e()
activate(n__i()) = [0]
>= [0]
= i()
activate(n__isList(X)) = [1] X + [0]
>= [1] X + [0]
= isList(X)
activate(n__isNeList(X)) = [1] X + [0]
>= [1] X + [0]
= isNeList(X)
activate(n__isPal(X)) = [1] X + [4]
>= [1] X + [4]
= isPal(X)
activate(n__nil()) = [4]
>= [4]
= nil()
activate(n__o()) = [1]
>= [1]
= o()
activate(n__u()) = [7]
>= [7]
= u()
and(tt(),X) = [1] X + [0]
>= [1] X + [0]
= activate(X)
e() = [2]
>= [2]
= n__e()
i() = [0]
>= [0]
= n__i()
isList(V) = [1] V + [0]
>= [1] V + [0]
= isNeList(activate(V))
isList(X) = [1] X + [0]
>= [1] X + [0]
= n__isList(X)
isList(n__nil()) = [4]
>= [0]
= tt()
isNeList(V) = [1] V + [0]
>= [1] V + [2]
= isQid(activate(V))
isNeList(X) = [1] X + [0]
>= [1] X + [0]
= n__isNeList(X)
isNePal(n____(I,n____(P,I))) = [2] I + [1] P + [6]
>= [1] I + [1] P + [6]
= and(isQid(activate(I)),n__isPal(activate(P)))
isPal(V) = [1] V + [4]
>= [1] V + [4]
= isNePal(activate(V))
isPal(X) = [1] X + [4]
>= [1] X + [4]
= n__isPal(X)
isPal(n__nil()) = [8]
>= [0]
= tt()
isQid(n__a()) = [4]
>= [0]
= tt()
isQid(n__e()) = [4]
>= [0]
= tt()
isQid(n__i()) = [2]
>= [0]
= tt()
isQid(n__o()) = [3]
>= [0]
= tt()
isQid(n__u()) = [9]
>= [0]
= tt()
nil() = [4]
>= [4]
= n__nil()
o() = [1]
>= [1]
= n__o()
u() = [7]
>= [7]
= n__u()
Further, it can be verified that all rules not oriented are covered by the weightgap condition.
** Step 1.b:8: WeightGap WORST_CASE(?,O(n^2))
+ Considered Problem:
- Strict TRS:
activate(n____(X1,X2)) -> __(activate(X1),activate(X2))
activate(n__isPal(X)) -> isPal(X)
i() -> n__i()
isNeList(V) -> isQid(activate(V))
nil() -> n__nil()
- Weak TRS:
__(X1,X2) -> n____(X1,X2)
a() -> n__a()
activate(X) -> X
activate(n__a()) -> a()
activate(n__e()) -> e()
activate(n__i()) -> i()
activate(n__isList(X)) -> isList(X)
activate(n__isNeList(X)) -> isNeList(X)
activate(n__nil()) -> nil()
activate(n__o()) -> o()
activate(n__u()) -> u()
and(tt(),X) -> activate(X)
e() -> n__e()
isList(V) -> isNeList(activate(V))
isList(X) -> n__isList(X)
isList(n____(V1,V2)) -> and(isList(activate(V1)),n__isList(activate(V2)))
isList(n__nil()) -> tt()
isNeList(X) -> n__isNeList(X)
isNeList(n____(V1,V2)) -> and(isList(activate(V1)),n__isNeList(activate(V2)))
isNeList(n____(V1,V2)) -> and(isNeList(activate(V1)),n__isList(activate(V2)))
isNePal(V) -> isQid(activate(V))
isNePal(n____(I,n____(P,I))) -> and(isQid(activate(I)),n__isPal(activate(P)))
isPal(V) -> isNePal(activate(V))
isPal(X) -> n__isPal(X)
isPal(n__nil()) -> tt()
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:
{__/2,a/0,activate/1,and/2,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__isList/1,n__isNeList/1,n__isPal/1,n__nil/0,n__o/0,n__u/0,tt/0}
- Obligation:
innermost runtime complexity wrt. defined symbols {__,a,activate,and,e,i,isList,isNeList,isNePal,isPal,isQid
,nil,o,u} and constructors {n____,n__a,n__e,n__i,n__isList,n__isNeList,n__isPal,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(__) = {1,2},
uargs(and) = {1,2},
uargs(isList) = {1},
uargs(isNeList) = {1},
uargs(isNePal) = {1},
uargs(isQid) = {1},
uargs(n__isList) = {1},
uargs(n__isNeList) = {1},
uargs(n__isPal) = {1}
Following symbols are considered usable:
all
TcT has computed the following interpretation:
p(__) = [1] x1 + [1] x2 + [2]
p(a) = [6]
p(activate) = [1] x1 + [0]
p(and) = [1] x1 + [1] x2 + [0]
p(e) = [0]
p(i) = [0]
p(isList) = [1] x1 + [1]
p(isNeList) = [1] x1 + [1]
p(isNePal) = [1] x1 + [0]
p(isPal) = [1] x1 + [0]
p(isQid) = [1] x1 + [0]
p(n____) = [1] x1 + [1] x2 + [2]
p(n__a) = [6]
p(n__e) = [0]
p(n__i) = [0]
p(n__isList) = [1] x1 + [1]
p(n__isNeList) = [1] x1 + [1]
p(n__isPal) = [1] x1 + [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:
isNeList(V) = [1] V + [1]
> [1] V + [0]
= isQid(activate(V))
Following rules are (at-least) weakly oriented:
__(X1,X2) = [1] X1 + [1] X2 + [2]
>= [1] X1 + [1] X2 + [2]
= n____(X1,X2)
a() = [6]
>= [6]
= n__a()
activate(X) = [1] X + [0]
>= [1] X + [0]
= X
activate(n____(X1,X2)) = [1] X1 + [1] X2 + [2]
>= [1] X1 + [1] X2 + [2]
= __(activate(X1),activate(X2))
activate(n__a()) = [6]
>= [6]
= a()
activate(n__e()) = [0]
>= [0]
= e()
activate(n__i()) = [0]
>= [0]
= i()
activate(n__isList(X)) = [1] X + [1]
>= [1] X + [1]
= isList(X)
activate(n__isNeList(X)) = [1] X + [1]
>= [1] X + [1]
= isNeList(X)
activate(n__isPal(X)) = [1] X + [0]
>= [1] X + [0]
= isPal(X)
activate(n__nil()) = [0]
>= [0]
= nil()
activate(n__o()) = [0]
>= [0]
= o()
activate(n__u()) = [0]
>= [0]
= u()
and(tt(),X) = [1] X + [0]
>= [1] X + [0]
= activate(X)
e() = [0]
>= [0]
= n__e()
i() = [0]
>= [0]
= n__i()
isList(V) = [1] V + [1]
>= [1] V + [1]
= isNeList(activate(V))
isList(X) = [1] X + [1]
>= [1] X + [1]
= n__isList(X)
isList(n____(V1,V2)) = [1] V1 + [1] V2 + [3]
>= [1] V1 + [1] V2 + [2]
= and(isList(activate(V1)),n__isList(activate(V2)))
isList(n__nil()) = [1]
>= [0]
= tt()
isNeList(X) = [1] X + [1]
>= [1] X + [1]
= n__isNeList(X)
isNeList(n____(V1,V2)) = [1] V1 + [1] V2 + [3]
>= [1] V1 + [1] V2 + [2]
= and(isList(activate(V1)),n__isNeList(activate(V2)))
isNeList(n____(V1,V2)) = [1] V1 + [1] V2 + [3]
>= [1] V1 + [1] V2 + [2]
= and(isNeList(activate(V1)),n__isList(activate(V2)))
isNePal(V) = [1] V + [0]
>= [1] V + [0]
= isQid(activate(V))
isNePal(n____(I,n____(P,I))) = [2] I + [1] P + [4]
>= [1] I + [1] P + [0]
= and(isQid(activate(I)),n__isPal(activate(P)))
isPal(V) = [1] V + [0]
>= [1] V + [0]
= isNePal(activate(V))
isPal(X) = [1] X + [0]
>= [1] X + [0]
= n__isPal(X)
isPal(n__nil()) = [0]
>= [0]
= tt()
isQid(n__a()) = [6]
>= [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()
u() = [0]
>= [0]
= n__u()
Further, it can be verified that all rules not oriented are covered by the weightgap condition.
** Step 1.b:9: WeightGap WORST_CASE(?,O(n^2))
+ Considered Problem:
- Strict TRS:
activate(n____(X1,X2)) -> __(activate(X1),activate(X2))
activate(n__isPal(X)) -> isPal(X)
i() -> n__i()
nil() -> n__nil()
- Weak TRS:
__(X1,X2) -> n____(X1,X2)
a() -> n__a()
activate(X) -> X
activate(n__a()) -> a()
activate(n__e()) -> e()
activate(n__i()) -> i()
activate(n__isList(X)) -> isList(X)
activate(n__isNeList(X)) -> isNeList(X)
activate(n__nil()) -> nil()
activate(n__o()) -> o()
activate(n__u()) -> u()
and(tt(),X) -> activate(X)
e() -> n__e()
isList(V) -> isNeList(activate(V))
isList(X) -> n__isList(X)
isList(n____(V1,V2)) -> and(isList(activate(V1)),n__isList(activate(V2)))
isList(n__nil()) -> tt()
isNeList(V) -> isQid(activate(V))
isNeList(X) -> n__isNeList(X)
isNeList(n____(V1,V2)) -> and(isList(activate(V1)),n__isNeList(activate(V2)))
isNeList(n____(V1,V2)) -> and(isNeList(activate(V1)),n__isList(activate(V2)))
isNePal(V) -> isQid(activate(V))
isNePal(n____(I,n____(P,I))) -> and(isQid(activate(I)),n__isPal(activate(P)))
isPal(V) -> isNePal(activate(V))
isPal(X) -> n__isPal(X)
isPal(n__nil()) -> tt()
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:
{__/2,a/0,activate/1,and/2,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__isList/1,n__isNeList/1,n__isPal/1,n__nil/0,n__o/0,n__u/0,tt/0}
- Obligation:
innermost runtime complexity wrt. defined symbols {__,a,activate,and,e,i,isList,isNeList,isNePal,isPal,isQid
,nil,o,u} and constructors {n____,n__a,n__e,n__i,n__isList,n__isNeList,n__isPal,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(__) = {1,2},
uargs(and) = {1,2},
uargs(isList) = {1},
uargs(isNeList) = {1},
uargs(isNePal) = {1},
uargs(isQid) = {1},
uargs(n__isList) = {1},
uargs(n__isNeList) = {1},
uargs(n__isPal) = {1}
Following symbols are considered usable:
all
TcT has computed the following interpretation:
p(__) = [1] x1 + [1] x2 + [7]
p(a) = [3]
p(activate) = [1] x1 + [2]
p(and) = [1] x1 + [1] x2 + [0]
p(e) = [4]
p(i) = [0]
p(isList) = [1] x1 + [4]
p(isNeList) = [1] x1 + [2]
p(isNePal) = [1] x1 + [3]
p(isPal) = [1] x1 + [5]
p(isQid) = [1] x1 + [0]
p(n____) = [1] x1 + [1] x2 + [6]
p(n__a) = [3]
p(n__e) = [4]
p(n__i) = [3]
p(n__isList) = [1] x1 + [2]
p(n__isNeList) = [1] x1 + [0]
p(n__isPal) = [1] x1 + [0]
p(n__nil) = [6]
p(n__o) = [4]
p(n__u) = [3]
p(nil) = [7]
p(o) = [5]
p(tt) = [3]
p(u) = [3]
Following rules are strictly oriented:
nil() = [7]
> [6]
= n__nil()
Following rules are (at-least) weakly oriented:
__(X1,X2) = [1] X1 + [1] X2 + [7]
>= [1] X1 + [1] X2 + [6]
= n____(X1,X2)
a() = [3]
>= [3]
= n__a()
activate(X) = [1] X + [2]
>= [1] X + [0]
= X
activate(n____(X1,X2)) = [1] X1 + [1] X2 + [8]
>= [1] X1 + [1] X2 + [11]
= __(activate(X1),activate(X2))
activate(n__a()) = [5]
>= [3]
= a()
activate(n__e()) = [6]
>= [4]
= e()
activate(n__i()) = [5]
>= [0]
= i()
activate(n__isList(X)) = [1] X + [4]
>= [1] X + [4]
= isList(X)
activate(n__isNeList(X)) = [1] X + [2]
>= [1] X + [2]
= isNeList(X)
activate(n__isPal(X)) = [1] X + [2]
>= [1] X + [5]
= isPal(X)
activate(n__nil()) = [8]
>= [7]
= nil()
activate(n__o()) = [6]
>= [5]
= o()
activate(n__u()) = [5]
>= [3]
= u()
and(tt(),X) = [1] X + [3]
>= [1] X + [2]
= activate(X)
e() = [4]
>= [4]
= n__e()
i() = [0]
>= [3]
= n__i()
isList(V) = [1] V + [4]
>= [1] V + [4]
= isNeList(activate(V))
isList(X) = [1] X + [4]
>= [1] X + [2]
= n__isList(X)
isList(n____(V1,V2)) = [1] V1 + [1] V2 + [10]
>= [1] V1 + [1] V2 + [10]
= and(isList(activate(V1)),n__isList(activate(V2)))
isList(n__nil()) = [10]
>= [3]
= tt()
isNeList(V) = [1] V + [2]
>= [1] V + [2]
= isQid(activate(V))
isNeList(X) = [1] X + [2]
>= [1] X + [0]
= n__isNeList(X)
isNeList(n____(V1,V2)) = [1] V1 + [1] V2 + [8]
>= [1] V1 + [1] V2 + [8]
= and(isList(activate(V1)),n__isNeList(activate(V2)))
isNeList(n____(V1,V2)) = [1] V1 + [1] V2 + [8]
>= [1] V1 + [1] V2 + [8]
= and(isNeList(activate(V1)),n__isList(activate(V2)))
isNePal(V) = [1] V + [3]
>= [1] V + [2]
= isQid(activate(V))
isNePal(n____(I,n____(P,I))) = [2] I + [1] P + [15]
>= [1] I + [1] P + [4]
= and(isQid(activate(I)),n__isPal(activate(P)))
isPal(V) = [1] V + [5]
>= [1] V + [5]
= isNePal(activate(V))
isPal(X) = [1] X + [5]
>= [1] X + [0]
= n__isPal(X)
isPal(n__nil()) = [11]
>= [3]
= tt()
isQid(n__a()) = [3]
>= [3]
= tt()
isQid(n__e()) = [4]
>= [3]
= tt()
isQid(n__i()) = [3]
>= [3]
= tt()
isQid(n__o()) = [4]
>= [3]
= tt()
isQid(n__u()) = [3]
>= [3]
= tt()
o() = [5]
>= [4]
= n__o()
u() = [3]
>= [3]
= n__u()
Further, it can be verified that all rules not oriented are covered by the weightgap condition.
** Step 1.b:10: WeightGap WORST_CASE(?,O(n^2))
+ Considered Problem:
- Strict TRS:
activate(n____(X1,X2)) -> __(activate(X1),activate(X2))
activate(n__isPal(X)) -> isPal(X)
i() -> n__i()
- Weak TRS:
__(X1,X2) -> n____(X1,X2)
a() -> n__a()
activate(X) -> X
activate(n__a()) -> a()
activate(n__e()) -> e()
activate(n__i()) -> i()
activate(n__isList(X)) -> isList(X)
activate(n__isNeList(X)) -> isNeList(X)
activate(n__nil()) -> nil()
activate(n__o()) -> o()
activate(n__u()) -> u()
and(tt(),X) -> activate(X)
e() -> n__e()
isList(V) -> isNeList(activate(V))
isList(X) -> n__isList(X)
isList(n____(V1,V2)) -> and(isList(activate(V1)),n__isList(activate(V2)))
isList(n__nil()) -> tt()
isNeList(V) -> isQid(activate(V))
isNeList(X) -> n__isNeList(X)
isNeList(n____(V1,V2)) -> and(isList(activate(V1)),n__isNeList(activate(V2)))
isNeList(n____(V1,V2)) -> and(isNeList(activate(V1)),n__isList(activate(V2)))
isNePal(V) -> isQid(activate(V))
isNePal(n____(I,n____(P,I))) -> and(isQid(activate(I)),n__isPal(activate(P)))
isPal(V) -> isNePal(activate(V))
isPal(X) -> n__isPal(X)
isPal(n__nil()) -> tt()
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:
{__/2,a/0,activate/1,and/2,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__isList/1,n__isNeList/1,n__isPal/1,n__nil/0,n__o/0,n__u/0,tt/0}
- Obligation:
innermost runtime complexity wrt. defined symbols {__,a,activate,and,e,i,isList,isNeList,isNePal,isPal,isQid
,nil,o,u} and constructors {n____,n__a,n__e,n__i,n__isList,n__isNeList,n__isPal,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(__) = {1,2},
uargs(and) = {1,2},
uargs(isList) = {1},
uargs(isNeList) = {1},
uargs(isNePal) = {1},
uargs(isQid) = {1},
uargs(n__isList) = {1},
uargs(n__isNeList) = {1},
uargs(n__isPal) = {1}
Following symbols are considered usable:
all
TcT has computed the following interpretation:
p(__) = [1] x1 + [1] x2 + [7]
p(a) = [2]
p(activate) = [1] x1 + [1]
p(and) = [1] x1 + [1] x2 + [0]
p(e) = [4]
p(i) = [3]
p(isList) = [1] x1 + [2]
p(isNeList) = [1] x1 + [1]
p(isNePal) = [1] x1 + [3]
p(isPal) = [1] x1 + [5]
p(isQid) = [1] x1 + [0]
p(n____) = [1] x1 + [1] x2 + [4]
p(n__a) = [1]
p(n__e) = [4]
p(n__i) = [2]
p(n__isList) = [1] x1 + [1]
p(n__isNeList) = [1] x1 + [0]
p(n__isPal) = [1] x1 + [0]
p(n__nil) = [2]
p(n__o) = [1]
p(n__u) = [2]
p(nil) = [3]
p(o) = [1]
p(tt) = [1]
p(u) = [3]
Following rules are strictly oriented:
i() = [3]
> [2]
= n__i()
Following rules are (at-least) weakly oriented:
__(X1,X2) = [1] X1 + [1] X2 + [7]
>= [1] X1 + [1] X2 + [4]
= n____(X1,X2)
a() = [2]
>= [1]
= n__a()
activate(X) = [1] X + [1]
>= [1] X + [0]
= X
activate(n____(X1,X2)) = [1] X1 + [1] X2 + [5]
>= [1] X1 + [1] X2 + [9]
= __(activate(X1),activate(X2))
activate(n__a()) = [2]
>= [2]
= a()
activate(n__e()) = [5]
>= [4]
= e()
activate(n__i()) = [3]
>= [3]
= i()
activate(n__isList(X)) = [1] X + [2]
>= [1] X + [2]
= isList(X)
activate(n__isNeList(X)) = [1] X + [1]
>= [1] X + [1]
= isNeList(X)
activate(n__isPal(X)) = [1] X + [1]
>= [1] X + [5]
= isPal(X)
activate(n__nil()) = [3]
>= [3]
= nil()
activate(n__o()) = [2]
>= [1]
= o()
activate(n__u()) = [3]
>= [3]
= u()
and(tt(),X) = [1] X + [1]
>= [1] X + [1]
= activate(X)
e() = [4]
>= [4]
= n__e()
isList(V) = [1] V + [2]
>= [1] V + [2]
= isNeList(activate(V))
isList(X) = [1] X + [2]
>= [1] X + [1]
= n__isList(X)
isList(n____(V1,V2)) = [1] V1 + [1] V2 + [6]
>= [1] V1 + [1] V2 + [5]
= and(isList(activate(V1)),n__isList(activate(V2)))
isList(n__nil()) = [4]
>= [1]
= tt()
isNeList(V) = [1] V + [1]
>= [1] V + [1]
= isQid(activate(V))
isNeList(X) = [1] X + [1]
>= [1] X + [0]
= n__isNeList(X)
isNeList(n____(V1,V2)) = [1] V1 + [1] V2 + [5]
>= [1] V1 + [1] V2 + [4]
= and(isList(activate(V1)),n__isNeList(activate(V2)))
isNeList(n____(V1,V2)) = [1] V1 + [1] V2 + [5]
>= [1] V1 + [1] V2 + [4]
= and(isNeList(activate(V1)),n__isList(activate(V2)))
isNePal(V) = [1] V + [3]
>= [1] V + [1]
= isQid(activate(V))
isNePal(n____(I,n____(P,I))) = [2] I + [1] P + [11]
>= [1] I + [1] P + [2]
= and(isQid(activate(I)),n__isPal(activate(P)))
isPal(V) = [1] V + [5]
>= [1] V + [4]
= isNePal(activate(V))
isPal(X) = [1] X + [5]
>= [1] X + [0]
= n__isPal(X)
isPal(n__nil()) = [7]
>= [1]
= tt()
isQid(n__a()) = [1]
>= [1]
= tt()
isQid(n__e()) = [4]
>= [1]
= tt()
isQid(n__i()) = [2]
>= [1]
= tt()
isQid(n__o()) = [1]
>= [1]
= tt()
isQid(n__u()) = [2]
>= [1]
= tt()
nil() = [3]
>= [2]
= n__nil()
o() = [1]
>= [1]
= n__o()
u() = [3]
>= [2]
= n__u()
Further, it can be verified that all rules not oriented are covered by the weightgap condition.
** Step 1.b:11: WeightGap WORST_CASE(?,O(n^2))
+ Considered Problem:
- Strict TRS:
activate(n____(X1,X2)) -> __(activate(X1),activate(X2))
activate(n__isPal(X)) -> isPal(X)
- Weak TRS:
__(X1,X2) -> n____(X1,X2)
a() -> n__a()
activate(X) -> X
activate(n__a()) -> a()
activate(n__e()) -> e()
activate(n__i()) -> i()
activate(n__isList(X)) -> isList(X)
activate(n__isNeList(X)) -> isNeList(X)
activate(n__nil()) -> nil()
activate(n__o()) -> o()
activate(n__u()) -> u()
and(tt(),X) -> activate(X)
e() -> n__e()
i() -> n__i()
isList(V) -> isNeList(activate(V))
isList(X) -> n__isList(X)
isList(n____(V1,V2)) -> and(isList(activate(V1)),n__isList(activate(V2)))
isList(n__nil()) -> tt()
isNeList(V) -> isQid(activate(V))
isNeList(X) -> n__isNeList(X)
isNeList(n____(V1,V2)) -> and(isList(activate(V1)),n__isNeList(activate(V2)))
isNeList(n____(V1,V2)) -> and(isNeList(activate(V1)),n__isList(activate(V2)))
isNePal(V) -> isQid(activate(V))
isNePal(n____(I,n____(P,I))) -> and(isQid(activate(I)),n__isPal(activate(P)))
isPal(V) -> isNePal(activate(V))
isPal(X) -> n__isPal(X)
isPal(n__nil()) -> tt()
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:
{__/2,a/0,activate/1,and/2,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__isList/1,n__isNeList/1,n__isPal/1,n__nil/0,n__o/0,n__u/0,tt/0}
- Obligation:
innermost runtime complexity wrt. defined symbols {__,a,activate,and,e,i,isList,isNeList,isNePal,isPal,isQid
,nil,o,u} and constructors {n____,n__a,n__e,n__i,n__isList,n__isNeList,n__isPal,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(__) = {1,2},
uargs(and) = {1,2},
uargs(isList) = {1},
uargs(isNeList) = {1},
uargs(isNePal) = {1},
uargs(isQid) = {1},
uargs(n__isList) = {1},
uargs(n__isNeList) = {1},
uargs(n__isPal) = {1}
Following symbols are considered usable:
all
TcT has computed the following interpretation:
p(__) = [1] x1 + [1] x2 + [4]
p(a) = [4]
p(activate) = [1] x1 + [1]
p(and) = [1] x1 + [1] x2 + [0]
p(e) = [2]
p(i) = [5]
p(isList) = [1] x1 + [2]
p(isNeList) = [1] x1 + [1]
p(isNePal) = [1] x1 + [1]
p(isPal) = [1] x1 + [4]
p(isQid) = [1] x1 + [0]
p(n____) = [1] x1 + [1] x2 + [4]
p(n__a) = [4]
p(n__e) = [2]
p(n__i) = [4]
p(n__isList) = [1] x1 + [2]
p(n__isNeList) = [1] x1 + [0]
p(n__isPal) = [1] x1 + [4]
p(n__nil) = [0]
p(n__o) = [1]
p(n__u) = [2]
p(nil) = [1]
p(o) = [2]
p(tt) = [1]
p(u) = [2]
Following rules are strictly oriented:
activate(n__isPal(X)) = [1] X + [5]
> [1] X + [4]
= isPal(X)
Following rules are (at-least) weakly oriented:
__(X1,X2) = [1] X1 + [1] X2 + [4]
>= [1] X1 + [1] X2 + [4]
= n____(X1,X2)
a() = [4]
>= [4]
= n__a()
activate(X) = [1] X + [1]
>= [1] X + [0]
= X
activate(n____(X1,X2)) = [1] X1 + [1] X2 + [5]
>= [1] X1 + [1] X2 + [6]
= __(activate(X1),activate(X2))
activate(n__a()) = [5]
>= [4]
= a()
activate(n__e()) = [3]
>= [2]
= e()
activate(n__i()) = [5]
>= [5]
= i()
activate(n__isList(X)) = [1] X + [3]
>= [1] X + [2]
= isList(X)
activate(n__isNeList(X)) = [1] X + [1]
>= [1] X + [1]
= isNeList(X)
activate(n__nil()) = [1]
>= [1]
= nil()
activate(n__o()) = [2]
>= [2]
= o()
activate(n__u()) = [3]
>= [2]
= u()
and(tt(),X) = [1] X + [1]
>= [1] X + [1]
= activate(X)
e() = [2]
>= [2]
= n__e()
i() = [5]
>= [4]
= n__i()
isList(V) = [1] V + [2]
>= [1] V + [2]
= isNeList(activate(V))
isList(X) = [1] X + [2]
>= [1] X + [2]
= n__isList(X)
isList(n____(V1,V2)) = [1] V1 + [1] V2 + [6]
>= [1] V1 + [1] V2 + [6]
= and(isList(activate(V1)),n__isList(activate(V2)))
isList(n__nil()) = [2]
>= [1]
= tt()
isNeList(V) = [1] V + [1]
>= [1] V + [1]
= isQid(activate(V))
isNeList(X) = [1] X + [1]
>= [1] X + [0]
= n__isNeList(X)
isNeList(n____(V1,V2)) = [1] V1 + [1] V2 + [5]
>= [1] V1 + [1] V2 + [4]
= and(isList(activate(V1)),n__isNeList(activate(V2)))
isNeList(n____(V1,V2)) = [1] V1 + [1] V2 + [5]
>= [1] V1 + [1] V2 + [5]
= and(isNeList(activate(V1)),n__isList(activate(V2)))
isNePal(V) = [1] V + [1]
>= [1] V + [1]
= isQid(activate(V))
isNePal(n____(I,n____(P,I))) = [2] I + [1] P + [9]
>= [1] I + [1] P + [6]
= and(isQid(activate(I)),n__isPal(activate(P)))
isPal(V) = [1] V + [4]
>= [1] V + [2]
= isNePal(activate(V))
isPal(X) = [1] X + [4]
>= [1] X + [4]
= n__isPal(X)
isPal(n__nil()) = [4]
>= [1]
= tt()
isQid(n__a()) = [4]
>= [1]
= tt()
isQid(n__e()) = [2]
>= [1]
= tt()
isQid(n__i()) = [4]
>= [1]
= tt()
isQid(n__o()) = [1]
>= [1]
= tt()
isQid(n__u()) = [2]
>= [1]
= tt()
nil() = [1]
>= [0]
= n__nil()
o() = [2]
>= [1]
= n__o()
u() = [2]
>= [2]
= n__u()
Further, it can be verified that all rules not oriented are covered by the weightgap condition.
** Step 1.b:12: MI WORST_CASE(?,O(n^2))
+ Considered Problem:
- Strict TRS:
activate(n____(X1,X2)) -> __(activate(X1),activate(X2))
- Weak TRS:
__(X1,X2) -> n____(X1,X2)
a() -> n__a()
activate(X) -> X
activate(n__a()) -> a()
activate(n__e()) -> e()
activate(n__i()) -> i()
activate(n__isList(X)) -> isList(X)
activate(n__isNeList(X)) -> isNeList(X)
activate(n__isPal(X)) -> isPal(X)
activate(n__nil()) -> nil()
activate(n__o()) -> o()
activate(n__u()) -> u()
and(tt(),X) -> activate(X)
e() -> n__e()
i() -> n__i()
isList(V) -> isNeList(activate(V))
isList(X) -> n__isList(X)
isList(n____(V1,V2)) -> and(isList(activate(V1)),n__isList(activate(V2)))
isList(n__nil()) -> tt()
isNeList(V) -> isQid(activate(V))
isNeList(X) -> n__isNeList(X)
isNeList(n____(V1,V2)) -> and(isList(activate(V1)),n__isNeList(activate(V2)))
isNeList(n____(V1,V2)) -> and(isNeList(activate(V1)),n__isList(activate(V2)))
isNePal(V) -> isQid(activate(V))
isNePal(n____(I,n____(P,I))) -> and(isQid(activate(I)),n__isPal(activate(P)))
isPal(V) -> isNePal(activate(V))
isPal(X) -> n__isPal(X)
isPal(n__nil()) -> tt()
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:
{__/2,a/0,activate/1,and/2,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__isList/1,n__isNeList/1,n__isPal/1,n__nil/0,n__o/0,n__u/0,tt/0}
- Obligation:
innermost runtime complexity wrt. defined symbols {__,a,activate,and,e,i,isList,isNeList,isNePal,isPal,isQid
,nil,o,u} and constructors {n____,n__a,n__e,n__i,n__isList,n__isNeList,n__isPal,n__nil,n__o,n__u,tt}
+ Applied Processor:
MI {miKind = MaximalMatrix (UpperTriangular (Multiplicity Nothing)), miDimension = 2, miUArgs = UArgs, miURules = URules, miSelector = Just any strict-rules}
+ Details:
We apply a matrix interpretation of kind MaximalMatrix (UpperTriangular (Multiplicity Nothing)):
The following argument positions are considered usable:
uargs(__) = {1,2},
uargs(and) = {1,2},
uargs(isList) = {1},
uargs(isNeList) = {1},
uargs(isNePal) = {1},
uargs(isQid) = {1},
uargs(n__isList) = {1},
uargs(n__isNeList) = {1},
uargs(n__isPal) = {1}
Following symbols are considered usable:
{__,a,activate,and,e,i,isList,isNeList,isNePal,isPal,isQid,nil,o,u}
TcT has computed the following interpretation:
p(__) = [1 3] x_1 + [1 2] x_2 + [0]
[0 1] [0 1] [1]
p(a) = [2]
[0]
p(activate) = [1 1] x_1 + [0]
[0 1] [0]
p(and) = [1 0] x_1 + [1 1] x_2 + [0]
[0 0] [0 1] [0]
p(e) = [0]
[0]
p(i) = [5]
[2]
p(isList) = [1 3] x_1 + [0]
[0 1] [2]
p(isNeList) = [1 2] x_1 + [0]
[0 1] [2]
p(isNePal) = [1 2] x_1 + [0]
[0 0] [0]
p(isPal) = [1 3] x_1 + [0]
[0 0] [0]
p(isQid) = [1 0] x_1 + [0]
[0 0] [0]
p(n____) = [1 3] x_1 + [1 2] x_2 + [0]
[0 1] [0 1] [1]
p(n__a) = [2]
[0]
p(n__e) = [0]
[0]
p(n__i) = [5]
[2]
p(n__isList) = [1 2] x_1 + [0]
[0 1] [2]
p(n__isNeList) = [1 2] x_1 + [0]
[0 1] [2]
p(n__isPal) = [1 3] x_1 + [0]
[0 0] [0]
p(n__nil) = [0]
[0]
p(n__o) = [4]
[2]
p(n__u) = [0]
[2]
p(nil) = [0]
[0]
p(o) = [4]
[2]
p(tt) = [0]
[0]
p(u) = [1]
[2]
Following rules are strictly oriented:
activate(n____(X1,X2)) = [1 4] X1 + [1 3] X2 + [1]
[0 1] [0 1] [1]
> [1 4] X1 + [1 3] X2 + [0]
[0 1] [0 1] [1]
= __(activate(X1),activate(X2))
Following rules are (at-least) weakly oriented:
__(X1,X2) = [1 3] X1 + [1 2] X2 + [0]
[0 1] [0 1] [1]
>= [1 3] X1 + [1 2] X2 + [0]
[0 1] [0 1] [1]
= n____(X1,X2)
a() = [2]
[0]
>= [2]
[0]
= n__a()
activate(X) = [1 1] X + [0]
[0 1] [0]
>= [1 0] X + [0]
[0 1] [0]
= X
activate(n__a()) = [2]
[0]
>= [2]
[0]
= a()
activate(n__e()) = [0]
[0]
>= [0]
[0]
= e()
activate(n__i()) = [7]
[2]
>= [5]
[2]
= i()
activate(n__isList(X)) = [1 3] X + [2]
[0 1] [2]
>= [1 3] X + [0]
[0 1] [2]
= isList(X)
activate(n__isNeList(X)) = [1 3] X + [2]
[0 1] [2]
>= [1 2] X + [0]
[0 1] [2]
= isNeList(X)
activate(n__isPal(X)) = [1 3] X + [0]
[0 0] [0]
>= [1 3] X + [0]
[0 0] [0]
= isPal(X)
activate(n__nil()) = [0]
[0]
>= [0]
[0]
= nil()
activate(n__o()) = [6]
[2]
>= [4]
[2]
= o()
activate(n__u()) = [2]
[2]
>= [1]
[2]
= u()
and(tt(),X) = [1 1] X + [0]
[0 1] [0]
>= [1 1] X + [0]
[0 1] [0]
= activate(X)
e() = [0]
[0]
>= [0]
[0]
= n__e()
i() = [5]
[2]
>= [5]
[2]
= n__i()
isList(V) = [1 3] V + [0]
[0 1] [2]
>= [1 3] V + [0]
[0 1] [2]
= isNeList(activate(V))
isList(X) = [1 3] X + [0]
[0 1] [2]
>= [1 2] X + [0]
[0 1] [2]
= n__isList(X)
isList(n____(V1,V2)) = [1 6] V1 + [1 5] V2 + [3]
[0 1] [0 1] [3]
>= [1 4] V1 + [1 4] V2 + [2]
[0 0] [0 1] [2]
= and(isList(activate(V1)),n__isList(activate(V2)))
isList(n__nil()) = [0]
[2]
>= [0]
[0]
= tt()
isNeList(V) = [1 2] V + [0]
[0 1] [2]
>= [1 1] V + [0]
[0 0] [0]
= isQid(activate(V))
isNeList(X) = [1 2] X + [0]
[0 1] [2]
>= [1 2] X + [0]
[0 1] [2]
= n__isNeList(X)
isNeList(n____(V1,V2)) = [1 5] V1 + [1 4] V2 + [2]
[0 1] [0 1] [3]
>= [1 4] V1 + [1 4] V2 + [2]
[0 0] [0 1] [2]
= and(isList(activate(V1)),n__isNeList(activate(V2)))
isNeList(n____(V1,V2)) = [1 5] V1 + [1 4] V2 + [2]
[0 1] [0 1] [3]
>= [1 3] V1 + [1 4] V2 + [2]
[0 0] [0 1] [2]
= and(isNeList(activate(V1)),n__isList(activate(V2)))
isNePal(V) = [1 2] V + [0]
[0 0] [0]
>= [1 1] V + [0]
[0 0] [0]
= isQid(activate(V))
isNePal(n____(I,n____(P,I))) = [2 11] I + [1 7] P + [6]
[0 0] [0 0] [0]
>= [1 1] I + [1 4] P + [0]
[0 0] [0 0] [0]
= and(isQid(activate(I)),n__isPal(activate(P)))
isPal(V) = [1 3] V + [0]
[0 0] [0]
>= [1 3] V + [0]
[0 0] [0]
= isNePal(activate(V))
isPal(X) = [1 3] X + [0]
[0 0] [0]
>= [1 3] X + [0]
[0 0] [0]
= n__isPal(X)
isPal(n__nil()) = [0]
[0]
>= [0]
[0]
= tt()
isQid(n__a()) = [2]
[0]
>= [0]
[0]
= tt()
isQid(n__e()) = [0]
[0]
>= [0]
[0]
= tt()
isQid(n__i()) = [5]
[0]
>= [0]
[0]
= tt()
isQid(n__o()) = [4]
[0]
>= [0]
[0]
= tt()
isQid(n__u()) = [0]
[0]
>= [0]
[0]
= tt()
nil() = [0]
[0]
>= [0]
[0]
= n__nil()
o() = [4]
[2]
>= [4]
[2]
= n__o()
u() = [1]
[2]
>= [0]
[2]
= n__u()
** Step 1.b:13: EmptyProcessor WORST_CASE(?,O(1))
+ Considered Problem:
- Weak TRS:
__(X1,X2) -> n____(X1,X2)
a() -> n__a()
activate(X) -> X
activate(n____(X1,X2)) -> __(activate(X1),activate(X2))
activate(n__a()) -> a()
activate(n__e()) -> e()
activate(n__i()) -> i()
activate(n__isList(X)) -> isList(X)
activate(n__isNeList(X)) -> isNeList(X)
activate(n__isPal(X)) -> isPal(X)
activate(n__nil()) -> nil()
activate(n__o()) -> o()
activate(n__u()) -> u()
and(tt(),X) -> activate(X)
e() -> n__e()
i() -> n__i()
isList(V) -> isNeList(activate(V))
isList(X) -> n__isList(X)
isList(n____(V1,V2)) -> and(isList(activate(V1)),n__isList(activate(V2)))
isList(n__nil()) -> tt()
isNeList(V) -> isQid(activate(V))
isNeList(X) -> n__isNeList(X)
isNeList(n____(V1,V2)) -> and(isList(activate(V1)),n__isNeList(activate(V2)))
isNeList(n____(V1,V2)) -> and(isNeList(activate(V1)),n__isList(activate(V2)))
isNePal(V) -> isQid(activate(V))
isNePal(n____(I,n____(P,I))) -> and(isQid(activate(I)),n__isPal(activate(P)))
isPal(V) -> isNePal(activate(V))
isPal(X) -> n__isPal(X)
isPal(n__nil()) -> tt()
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:
{__/2,a/0,activate/1,and/2,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__isList/1,n__isNeList/1,n__isPal/1,n__nil/0,n__o/0,n__u/0,tt/0}
- Obligation:
innermost runtime complexity wrt. defined symbols {__,a,activate,and,e,i,isList,isNeList,isNePal,isPal,isQid
,nil,o,u} and constructors {n____,n__a,n__e,n__i,n__isList,n__isNeList,n__isPal,n__nil,n__o,n__u,tt}
+ Applied Processor:
EmptyProcessor
+ Details:
The problem is already closed. The intended complexity is O(1).
WORST_CASE(Omega(n^1),O(n^2))