We consider the following Problem:
Strict Trs:
{ __(__(X, Y), Z) -> __(X, __(Y, Z))
, __(X, nil()) -> X
, __(nil(), X) -> X
, and(tt(), X) -> activate(X)
, isList(V) -> isNeList(activate(V))
, isList(n__nil()) -> tt()
, isList(n____(V1, V2)) ->
and(isList(activate(V1)), n__isList(activate(V2)))
, isNeList(V) -> isQid(activate(V))
, isNeList(n____(V1, V2)) ->
and(isList(activate(V1)), n__isNeList(activate(V2)))
, isNeList(n____(V1, V2)) ->
and(isNeList(activate(V1)), n__isList(activate(V2)))
, isNePal(V) -> isQid(activate(V))
, isNePal(n____(I, __(P, I))) ->
and(isQid(activate(I)), n__isPal(activate(P)))
, isPal(V) -> 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()
, __(X1, X2) -> n____(X1, X2)
, isList(X) -> n__isList(X)
, isNeList(X) -> n__isNeList(X)
, isPal(X) -> n__isPal(X)
, a() -> n__a()
, e() -> n__e()
, i() -> n__i()
, o() -> n__o()
, u() -> n__u()
, activate(n__nil()) -> nil()
, activate(n____(X1, X2)) -> __(X1, X2)
, activate(n__isList(X)) -> isList(X)
, activate(n__isNeList(X)) -> isNeList(X)
, activate(n__isPal(X)) -> isPal(X)
, activate(n__a()) -> a()
, activate(n__e()) -> e()
, activate(n__i()) -> i()
, activate(n__o()) -> o()
, activate(n__u()) -> u()
, activate(X) -> X}
StartTerms: basic terms
Strategy: innermost
Certificate: YES(?,O(n^1))
Proof:
Arguments of following rules are not normal-forms:
{ __(__(X, Y), Z) -> __(X, __(Y, Z))
, isNePal(n____(I, __(P, I))) ->
and(isQid(activate(I)), n__isPal(activate(P)))
, __(X, nil()) -> X
, __(nil(), X) -> X}
All above mentioned rules can be savely removed.
We consider the following Problem:
Strict Trs:
{ and(tt(), X) -> activate(X)
, isList(V) -> isNeList(activate(V))
, isList(n__nil()) -> tt()
, isList(n____(V1, V2)) ->
and(isList(activate(V1)), n__isList(activate(V2)))
, isNeList(V) -> isQid(activate(V))
, isNeList(n____(V1, V2)) ->
and(isList(activate(V1)), n__isNeList(activate(V2)))
, isNeList(n____(V1, V2)) ->
and(isNeList(activate(V1)), n__isList(activate(V2)))
, isNePal(V) -> isQid(activate(V))
, isPal(V) -> 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()
, __(X1, X2) -> n____(X1, X2)
, isList(X) -> n__isList(X)
, isNeList(X) -> n__isNeList(X)
, isPal(X) -> n__isPal(X)
, a() -> n__a()
, e() -> n__e()
, i() -> n__i()
, o() -> n__o()
, u() -> n__u()
, activate(n__nil()) -> nil()
, activate(n____(X1, X2)) -> __(X1, X2)
, activate(n__isList(X)) -> isList(X)
, activate(n__isNeList(X)) -> isNeList(X)
, activate(n__isPal(X)) -> isPal(X)
, activate(n__a()) -> a()
, activate(n__e()) -> e()
, activate(n__i()) -> i()
, activate(n__o()) -> o()
, activate(n__u()) -> u()
, activate(X) -> X}
StartTerms: basic terms
Strategy: innermost
Certificate: YES(?,O(n^1))
Proof:
The weightgap principle applies, where following rules are oriented strictly:
TRS Component:
{ and(tt(), X) -> activate(X)
, isList(n__nil()) -> tt()
, isPal(n__nil()) -> tt()
, isQid(n__a()) -> tt()
, isQid(n__e()) -> tt()
, isQid(n__i()) -> tt()
, isQid(n__o()) -> tt()
, isQid(n__u()) -> tt()
, isList(X) -> n__isList(X)
, isNeList(X) -> n__isNeList(X)
, isPal(X) -> n__isPal(X)}
Interpretation of nonconstant growth:
-------------------------------------
The following argument positions are usable:
Uargs(__) = {}, Uargs(and) = {1, 2}, Uargs(activate) = {},
Uargs(isList) = {1}, Uargs(isNeList) = {1}, Uargs(n____) = {},
Uargs(n__isList) = {1}, Uargs(isQid) = {1},
Uargs(n__isNeList) = {1}, Uargs(isNePal) = {1},
Uargs(n__isPal) = {}, Uargs(isPal) = {}
We have the following EDA-non-satisfying and IDA(1)-non-satisfying matrix interpretation:
Interpretation Functions:
__(x1, x2) = [0 0] x1 + [1 0] x2 + [0]
[0 0] [0 0] [0]
nil() = [0]
[0]
and(x1, x2) = [1 0] x1 + [1 0] x2 + [1]
[0 0] [0 0] [1]
tt() = [0]
[0]
activate(x1) = [1 0] x1 + [0]
[0 0] [0]
isList(x1) = [1 1] x1 + [1]
[0 0] [1]
isNeList(x1) = [1 1] x1 + [1]
[0 0] [1]
n__nil() = [0]
[0]
n____(x1, x2) = [0 0] x1 + [1 0] x2 + [0]
[1 0] [0 0] [0]
n__isList(x1) = [1 1] x1 + [0]
[0 0] [0]
isQid(x1) = [1 0] x1 + [1]
[0 0] [1]
n__isNeList(x1) = [1 1] x1 + [0]
[0 0] [0]
isNePal(x1) = [1 0] x1 + [1]
[0 0] [1]
n__isPal(x1) = [1 0] x1 + [0]
[0 0] [0]
isPal(x1) = [1 0] x1 + [1]
[0 0] [1]
n__a() = [0]
[0]
n__e() = [0]
[0]
n__i() = [0]
[0]
n__o() = [0]
[0]
n__u() = [0]
[0]
a() = [0]
[0]
e() = [0]
[0]
i() = [0]
[0]
o() = [0]
[0]
u() = [0]
[0]
The strictly oriented rules are moved into the weak component.
We consider the following Problem:
Strict Trs:
{ 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))
, isPal(V) -> isNePal(activate(V))
, nil() -> n__nil()
, __(X1, X2) -> n____(X1, X2)
, a() -> n__a()
, e() -> n__e()
, i() -> n__i()
, o() -> n__o()
, u() -> n__u()
, activate(n__nil()) -> nil()
, activate(n____(X1, X2)) -> __(X1, X2)
, activate(n__isList(X)) -> isList(X)
, activate(n__isNeList(X)) -> isNeList(X)
, activate(n__isPal(X)) -> isPal(X)
, activate(n__a()) -> a()
, activate(n__e()) -> e()
, activate(n__i()) -> i()
, activate(n__o()) -> o()
, activate(n__u()) -> u()
, activate(X) -> X}
Weak Trs:
{ and(tt(), X) -> activate(X)
, isList(n__nil()) -> tt()
, isPal(n__nil()) -> tt()
, isQid(n__a()) -> tt()
, isQid(n__e()) -> tt()
, isQid(n__i()) -> tt()
, isQid(n__o()) -> tt()
, isQid(n__u()) -> tt()
, isList(X) -> n__isList(X)
, isNeList(X) -> n__isNeList(X)
, isPal(X) -> n__isPal(X)}
StartTerms: basic terms
Strategy: innermost
Certificate: YES(?,O(n^1))
Proof:
The weightgap principle applies, where following rules are oriented strictly:
TRS Component: {nil() -> n__nil()}
Interpretation of nonconstant growth:
-------------------------------------
The following argument positions are usable:
Uargs(__) = {}, Uargs(and) = {1, 2}, Uargs(activate) = {},
Uargs(isList) = {1}, Uargs(isNeList) = {1}, Uargs(n____) = {},
Uargs(n__isList) = {1}, Uargs(isQid) = {1},
Uargs(n__isNeList) = {1}, Uargs(isNePal) = {1},
Uargs(n__isPal) = {}, Uargs(isPal) = {}
We have the following EDA-non-satisfying and IDA(1)-non-satisfying matrix interpretation:
Interpretation Functions:
__(x1, x2) = [0 0] x1 + [1 0] x2 + [0]
[0 0] [0 0] [0]
nil() = [2]
[0]
and(x1, x2) = [1 0] x1 + [1 0] x2 + [0]
[0 0] [0 0] [1]
tt() = [0]
[0]
activate(x1) = [1 0] x1 + [0]
[0 0] [0]
isList(x1) = [1 1] x1 + [1]
[0 0] [1]
isNeList(x1) = [1 1] x1 + [1]
[0 0] [1]
n__nil() = [0]
[0]
n____(x1, x2) = [0 0] x1 + [1 0] x2 + [0]
[1 0] [0 0] [0]
n__isList(x1) = [1 1] x1 + [0]
[0 0] [0]
isQid(x1) = [1 0] x1 + [1]
[0 0] [1]
n__isNeList(x1) = [1 1] x1 + [0]
[0 0] [0]
isNePal(x1) = [1 0] x1 + [1]
[0 0] [1]
n__isPal(x1) = [1 0] x1 + [0]
[0 0] [0]
isPal(x1) = [1 0] x1 + [1]
[0 0] [1]
n__a() = [0]
[0]
n__e() = [0]
[0]
n__i() = [0]
[0]
n__o() = [0]
[0]
n__u() = [0]
[0]
a() = [0]
[0]
e() = [0]
[0]
i() = [0]
[0]
o() = [0]
[0]
u() = [0]
[0]
The strictly oriented rules are moved into the weak component.
We consider the following Problem:
Strict Trs:
{ 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))
, isPal(V) -> isNePal(activate(V))
, __(X1, X2) -> n____(X1, X2)
, a() -> n__a()
, e() -> n__e()
, i() -> n__i()
, o() -> n__o()
, u() -> n__u()
, activate(n__nil()) -> nil()
, activate(n____(X1, X2)) -> __(X1, X2)
, activate(n__isList(X)) -> isList(X)
, activate(n__isNeList(X)) -> isNeList(X)
, activate(n__isPal(X)) -> isPal(X)
, activate(n__a()) -> a()
, activate(n__e()) -> e()
, activate(n__i()) -> i()
, activate(n__o()) -> o()
, activate(n__u()) -> u()
, activate(X) -> X}
Weak Trs:
{ nil() -> n__nil()
, and(tt(), X) -> activate(X)
, isList(n__nil()) -> tt()
, isPal(n__nil()) -> tt()
, isQid(n__a()) -> tt()
, isQid(n__e()) -> tt()
, isQid(n__i()) -> tt()
, isQid(n__o()) -> tt()
, isQid(n__u()) -> tt()
, isList(X) -> n__isList(X)
, isNeList(X) -> n__isNeList(X)
, isPal(X) -> n__isPal(X)}
StartTerms: basic terms
Strategy: innermost
Certificate: YES(?,O(n^1))
Proof:
The weightgap principle applies, where following rules are oriented strictly:
TRS Component: {__(X1, X2) -> n____(X1, X2)}
Interpretation of nonconstant growth:
-------------------------------------
The following argument positions are usable:
Uargs(__) = {}, Uargs(and) = {1, 2}, Uargs(activate) = {},
Uargs(isList) = {1}, Uargs(isNeList) = {1}, Uargs(n____) = {},
Uargs(n__isList) = {1}, Uargs(isQid) = {1},
Uargs(n__isNeList) = {1}, Uargs(isNePal) = {1},
Uargs(n__isPal) = {}, Uargs(isPal) = {}
We have the following EDA-non-satisfying and IDA(1)-non-satisfying matrix interpretation:
Interpretation Functions:
__(x1, x2) = [0 0] x1 + [1 0] x2 + [2]
[1 0] [0 0] [0]
nil() = [0]
[0]
and(x1, x2) = [1 0] x1 + [1 0] x2 + [0]
[0 0] [0 0] [1]
tt() = [0]
[0]
activate(x1) = [1 0] x1 + [0]
[0 0] [0]
isList(x1) = [1 1] x1 + [1]
[0 0] [1]
isNeList(x1) = [1 1] x1 + [1]
[0 0] [1]
n__nil() = [0]
[0]
n____(x1, x2) = [0 0] x1 + [1 0] x2 + [0]
[1 0] [0 0] [0]
n__isList(x1) = [1 1] x1 + [0]
[0 0] [0]
isQid(x1) = [1 0] x1 + [1]
[0 0] [1]
n__isNeList(x1) = [1 1] x1 + [0]
[0 0] [0]
isNePal(x1) = [1 0] x1 + [1]
[0 0] [1]
n__isPal(x1) = [1 0] x1 + [0]
[0 0] [0]
isPal(x1) = [1 0] x1 + [1]
[0 0] [1]
n__a() = [0]
[0]
n__e() = [0]
[0]
n__i() = [0]
[0]
n__o() = [0]
[0]
n__u() = [0]
[0]
a() = [0]
[0]
e() = [0]
[0]
i() = [0]
[0]
o() = [0]
[0]
u() = [0]
[0]
The strictly oriented rules are moved into the weak component.
We consider the following Problem:
Strict Trs:
{ 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))
, isPal(V) -> isNePal(activate(V))
, a() -> n__a()
, e() -> n__e()
, i() -> n__i()
, o() -> n__o()
, u() -> n__u()
, activate(n__nil()) -> nil()
, activate(n____(X1, X2)) -> __(X1, X2)
, activate(n__isList(X)) -> isList(X)
, activate(n__isNeList(X)) -> isNeList(X)
, activate(n__isPal(X)) -> isPal(X)
, activate(n__a()) -> a()
, activate(n__e()) -> e()
, activate(n__i()) -> i()
, activate(n__o()) -> o()
, activate(n__u()) -> u()
, activate(X) -> X}
Weak Trs:
{ __(X1, X2) -> n____(X1, X2)
, nil() -> n__nil()
, and(tt(), X) -> activate(X)
, isList(n__nil()) -> tt()
, isPal(n__nil()) -> tt()
, isQid(n__a()) -> tt()
, isQid(n__e()) -> tt()
, isQid(n__i()) -> tt()
, isQid(n__o()) -> tt()
, isQid(n__u()) -> tt()
, isList(X) -> n__isList(X)
, isNeList(X) -> n__isNeList(X)
, isPal(X) -> n__isPal(X)}
StartTerms: basic terms
Strategy: innermost
Certificate: YES(?,O(n^1))
Proof:
The weightgap principle applies, where following rules are oriented strictly:
TRS Component: {a() -> n__a()}
Interpretation of nonconstant growth:
-------------------------------------
The following argument positions are usable:
Uargs(__) = {}, Uargs(and) = {1, 2}, Uargs(activate) = {},
Uargs(isList) = {1}, Uargs(isNeList) = {1}, Uargs(n____) = {},
Uargs(n__isList) = {1}, Uargs(isQid) = {1},
Uargs(n__isNeList) = {1}, Uargs(isNePal) = {1},
Uargs(n__isPal) = {}, Uargs(isPal) = {}
We have the following EDA-non-satisfying and IDA(1)-non-satisfying matrix interpretation:
Interpretation Functions:
__(x1, x2) = [0 0] x1 + [1 0] x2 + [0]
[1 0] [0 0] [0]
nil() = [0]
[0]
and(x1, x2) = [1 0] x1 + [1 0] x2 + [0]
[0 0] [0 0] [1]
tt() = [0]
[0]
activate(x1) = [1 0] x1 + [0]
[0 0] [0]
isList(x1) = [1 1] x1 + [1]
[0 0] [1]
isNeList(x1) = [1 1] x1 + [1]
[0 0] [1]
n__nil() = [0]
[0]
n____(x1, x2) = [0 0] x1 + [1 0] x2 + [0]
[1 0] [0 0] [0]
n__isList(x1) = [1 1] x1 + [0]
[0 0] [0]
isQid(x1) = [1 0] x1 + [1]
[0 0] [1]
n__isNeList(x1) = [1 1] x1 + [0]
[0 0] [0]
isNePal(x1) = [1 0] x1 + [1]
[0 0] [1]
n__isPal(x1) = [1 0] x1 + [0]
[0 0] [0]
isPal(x1) = [1 0] x1 + [1]
[0 0] [1]
n__a() = [0]
[0]
n__e() = [0]
[0]
n__i() = [0]
[0]
n__o() = [0]
[0]
n__u() = [0]
[0]
a() = [2]
[0]
e() = [0]
[0]
i() = [0]
[0]
o() = [0]
[0]
u() = [0]
[0]
The strictly oriented rules are moved into the weak component.
We consider the following Problem:
Strict Trs:
{ 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))
, isPal(V) -> isNePal(activate(V))
, e() -> n__e()
, i() -> n__i()
, o() -> n__o()
, u() -> n__u()
, activate(n__nil()) -> nil()
, activate(n____(X1, X2)) -> __(X1, X2)
, activate(n__isList(X)) -> isList(X)
, activate(n__isNeList(X)) -> isNeList(X)
, activate(n__isPal(X)) -> isPal(X)
, activate(n__a()) -> a()
, activate(n__e()) -> e()
, activate(n__i()) -> i()
, activate(n__o()) -> o()
, activate(n__u()) -> u()
, activate(X) -> X}
Weak Trs:
{ a() -> n__a()
, __(X1, X2) -> n____(X1, X2)
, nil() -> n__nil()
, and(tt(), X) -> activate(X)
, isList(n__nil()) -> tt()
, isPal(n__nil()) -> tt()
, isQid(n__a()) -> tt()
, isQid(n__e()) -> tt()
, isQid(n__i()) -> tt()
, isQid(n__o()) -> tt()
, isQid(n__u()) -> tt()
, isList(X) -> n__isList(X)
, isNeList(X) -> n__isNeList(X)
, isPal(X) -> n__isPal(X)}
StartTerms: basic terms
Strategy: innermost
Certificate: YES(?,O(n^1))
Proof:
The weightgap principle applies, where following rules are oriented strictly:
TRS Component: {e() -> n__e()}
Interpretation of nonconstant growth:
-------------------------------------
The following argument positions are usable:
Uargs(__) = {}, Uargs(and) = {1, 2}, Uargs(activate) = {},
Uargs(isList) = {1}, Uargs(isNeList) = {1}, Uargs(n____) = {},
Uargs(n__isList) = {1}, Uargs(isQid) = {1},
Uargs(n__isNeList) = {1}, Uargs(isNePal) = {1},
Uargs(n__isPal) = {}, Uargs(isPal) = {}
We have the following EDA-non-satisfying and IDA(1)-non-satisfying matrix interpretation:
Interpretation Functions:
__(x1, x2) = [0 0] x1 + [1 0] x2 + [0]
[1 0] [0 0] [0]
nil() = [0]
[0]
and(x1, x2) = [1 0] x1 + [1 0] x2 + [0]
[0 0] [0 0] [1]
tt() = [0]
[0]
activate(x1) = [1 0] x1 + [0]
[0 0] [0]
isList(x1) = [1 1] x1 + [1]
[0 0] [1]
isNeList(x1) = [1 1] x1 + [1]
[0 0] [1]
n__nil() = [0]
[0]
n____(x1, x2) = [0 0] x1 + [1 0] x2 + [0]
[1 0] [0 0] [0]
n__isList(x1) = [1 1] x1 + [0]
[0 0] [0]
isQid(x1) = [1 0] x1 + [1]
[0 0] [1]
n__isNeList(x1) = [1 1] x1 + [0]
[0 0] [0]
isNePal(x1) = [1 0] x1 + [1]
[0 0] [1]
n__isPal(x1) = [1 0] x1 + [0]
[0 0] [0]
isPal(x1) = [1 0] x1 + [1]
[0 0] [1]
n__a() = [0]
[0]
n__e() = [0]
[0]
n__i() = [0]
[0]
n__o() = [0]
[0]
n__u() = [0]
[0]
a() = [0]
[0]
e() = [2]
[0]
i() = [0]
[0]
o() = [0]
[0]
u() = [0]
[0]
The strictly oriented rules are moved into the weak component.
We consider the following Problem:
Strict Trs:
{ 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))
, isPal(V) -> isNePal(activate(V))
, i() -> n__i()
, o() -> n__o()
, u() -> n__u()
, activate(n__nil()) -> nil()
, activate(n____(X1, X2)) -> __(X1, X2)
, activate(n__isList(X)) -> isList(X)
, activate(n__isNeList(X)) -> isNeList(X)
, activate(n__isPal(X)) -> isPal(X)
, activate(n__a()) -> a()
, activate(n__e()) -> e()
, activate(n__i()) -> i()
, activate(n__o()) -> o()
, activate(n__u()) -> u()
, activate(X) -> X}
Weak Trs:
{ e() -> n__e()
, a() -> n__a()
, __(X1, X2) -> n____(X1, X2)
, nil() -> n__nil()
, and(tt(), X) -> activate(X)
, isList(n__nil()) -> tt()
, isPal(n__nil()) -> tt()
, isQid(n__a()) -> tt()
, isQid(n__e()) -> tt()
, isQid(n__i()) -> tt()
, isQid(n__o()) -> tt()
, isQid(n__u()) -> tt()
, isList(X) -> n__isList(X)
, isNeList(X) -> n__isNeList(X)
, isPal(X) -> n__isPal(X)}
StartTerms: basic terms
Strategy: innermost
Certificate: YES(?,O(n^1))
Proof:
The weightgap principle applies, where following rules are oriented strictly:
TRS Component: {i() -> n__i()}
Interpretation of nonconstant growth:
-------------------------------------
The following argument positions are usable:
Uargs(__) = {}, Uargs(and) = {1, 2}, Uargs(activate) = {},
Uargs(isList) = {1}, Uargs(isNeList) = {1}, Uargs(n____) = {},
Uargs(n__isList) = {1}, Uargs(isQid) = {1},
Uargs(n__isNeList) = {1}, Uargs(isNePal) = {1},
Uargs(n__isPal) = {}, Uargs(isPal) = {}
We have the following EDA-non-satisfying and IDA(1)-non-satisfying matrix interpretation:
Interpretation Functions:
__(x1, x2) = [0 0] x1 + [1 0] x2 + [0]
[1 0] [0 0] [0]
nil() = [0]
[0]
and(x1, x2) = [1 0] x1 + [1 0] x2 + [0]
[0 0] [0 0] [1]
tt() = [0]
[0]
activate(x1) = [1 0] x1 + [0]
[0 0] [0]
isList(x1) = [1 1] x1 + [1]
[0 0] [1]
isNeList(x1) = [1 1] x1 + [1]
[0 0] [1]
n__nil() = [0]
[0]
n____(x1, x2) = [0 0] x1 + [1 0] x2 + [0]
[1 0] [0 0] [0]
n__isList(x1) = [1 1] x1 + [0]
[0 0] [0]
isQid(x1) = [1 0] x1 + [1]
[0 0] [1]
n__isNeList(x1) = [1 1] x1 + [0]
[0 0] [0]
isNePal(x1) = [1 0] x1 + [1]
[0 0] [1]
n__isPal(x1) = [1 0] x1 + [0]
[0 0] [0]
isPal(x1) = [1 0] x1 + [1]
[0 0] [1]
n__a() = [0]
[0]
n__e() = [0]
[0]
n__i() = [0]
[0]
n__o() = [0]
[0]
n__u() = [0]
[0]
a() = [0]
[0]
e() = [0]
[0]
i() = [2]
[0]
o() = [0]
[0]
u() = [0]
[0]
The strictly oriented rules are moved into the weak component.
We consider the following Problem:
Strict Trs:
{ 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))
, isPal(V) -> isNePal(activate(V))
, o() -> n__o()
, u() -> n__u()
, activate(n__nil()) -> nil()
, activate(n____(X1, X2)) -> __(X1, X2)
, activate(n__isList(X)) -> isList(X)
, activate(n__isNeList(X)) -> isNeList(X)
, activate(n__isPal(X)) -> isPal(X)
, activate(n__a()) -> a()
, activate(n__e()) -> e()
, activate(n__i()) -> i()
, activate(n__o()) -> o()
, activate(n__u()) -> u()
, activate(X) -> X}
Weak Trs:
{ i() -> n__i()
, e() -> n__e()
, a() -> n__a()
, __(X1, X2) -> n____(X1, X2)
, nil() -> n__nil()
, and(tt(), X) -> activate(X)
, isList(n__nil()) -> tt()
, isPal(n__nil()) -> tt()
, isQid(n__a()) -> tt()
, isQid(n__e()) -> tt()
, isQid(n__i()) -> tt()
, isQid(n__o()) -> tt()
, isQid(n__u()) -> tt()
, isList(X) -> n__isList(X)
, isNeList(X) -> n__isNeList(X)
, isPal(X) -> n__isPal(X)}
StartTerms: basic terms
Strategy: innermost
Certificate: YES(?,O(n^1))
Proof:
The weightgap principle applies, where following rules are oriented strictly:
TRS Component: {o() -> n__o()}
Interpretation of nonconstant growth:
-------------------------------------
The following argument positions are usable:
Uargs(__) = {}, Uargs(and) = {1, 2}, Uargs(activate) = {},
Uargs(isList) = {1}, Uargs(isNeList) = {1}, Uargs(n____) = {},
Uargs(n__isList) = {1}, Uargs(isQid) = {1},
Uargs(n__isNeList) = {1}, Uargs(isNePal) = {1},
Uargs(n__isPal) = {}, Uargs(isPal) = {}
We have the following EDA-non-satisfying and IDA(1)-non-satisfying matrix interpretation:
Interpretation Functions:
__(x1, x2) = [0 0] x1 + [1 0] x2 + [0]
[1 0] [0 0] [0]
nil() = [0]
[0]
and(x1, x2) = [1 0] x1 + [1 0] x2 + [0]
[0 0] [0 0] [1]
tt() = [0]
[0]
activate(x1) = [1 0] x1 + [0]
[0 0] [0]
isList(x1) = [1 1] x1 + [1]
[0 0] [1]
isNeList(x1) = [1 1] x1 + [1]
[0 0] [1]
n__nil() = [0]
[0]
n____(x1, x2) = [0 0] x1 + [1 0] x2 + [0]
[1 0] [0 0] [0]
n__isList(x1) = [1 1] x1 + [0]
[0 0] [0]
isQid(x1) = [1 0] x1 + [1]
[0 0] [1]
n__isNeList(x1) = [1 1] x1 + [0]
[0 0] [0]
isNePal(x1) = [1 0] x1 + [1]
[0 0] [1]
n__isPal(x1) = [1 0] x1 + [0]
[0 0] [0]
isPal(x1) = [1 0] x1 + [1]
[0 0] [1]
n__a() = [0]
[0]
n__e() = [0]
[0]
n__i() = [0]
[0]
n__o() = [0]
[0]
n__u() = [0]
[0]
a() = [0]
[0]
e() = [0]
[0]
i() = [0]
[0]
o() = [2]
[0]
u() = [0]
[0]
The strictly oriented rules are moved into the weak component.
We consider the following Problem:
Strict Trs:
{ 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))
, isPal(V) -> isNePal(activate(V))
, u() -> n__u()
, activate(n__nil()) -> nil()
, activate(n____(X1, X2)) -> __(X1, X2)
, activate(n__isList(X)) -> isList(X)
, activate(n__isNeList(X)) -> isNeList(X)
, activate(n__isPal(X)) -> isPal(X)
, activate(n__a()) -> a()
, activate(n__e()) -> e()
, activate(n__i()) -> i()
, activate(n__o()) -> o()
, activate(n__u()) -> u()
, activate(X) -> X}
Weak Trs:
{ o() -> n__o()
, i() -> n__i()
, e() -> n__e()
, a() -> n__a()
, __(X1, X2) -> n____(X1, X2)
, nil() -> n__nil()
, and(tt(), X) -> activate(X)
, isList(n__nil()) -> tt()
, isPal(n__nil()) -> tt()
, isQid(n__a()) -> tt()
, isQid(n__e()) -> tt()
, isQid(n__i()) -> tt()
, isQid(n__o()) -> tt()
, isQid(n__u()) -> tt()
, isList(X) -> n__isList(X)
, isNeList(X) -> n__isNeList(X)
, isPal(X) -> n__isPal(X)}
StartTerms: basic terms
Strategy: innermost
Certificate: YES(?,O(n^1))
Proof:
The weightgap principle applies, where following rules are oriented strictly:
TRS Component: {u() -> n__u()}
Interpretation of nonconstant growth:
-------------------------------------
The following argument positions are usable:
Uargs(__) = {}, Uargs(and) = {1, 2}, Uargs(activate) = {},
Uargs(isList) = {1}, Uargs(isNeList) = {1}, Uargs(n____) = {},
Uargs(n__isList) = {1}, Uargs(isQid) = {1},
Uargs(n__isNeList) = {1}, Uargs(isNePal) = {1},
Uargs(n__isPal) = {}, Uargs(isPal) = {}
We have the following EDA-non-satisfying and IDA(1)-non-satisfying matrix interpretation:
Interpretation Functions:
__(x1, x2) = [0 0] x1 + [1 0] x2 + [0]
[1 0] [0 0] [0]
nil() = [0]
[0]
and(x1, x2) = [1 0] x1 + [1 0] x2 + [0]
[0 0] [0 0] [1]
tt() = [0]
[0]
activate(x1) = [1 0] x1 + [0]
[0 0] [0]
isList(x1) = [1 1] x1 + [1]
[0 0] [1]
isNeList(x1) = [1 1] x1 + [1]
[0 0] [1]
n__nil() = [0]
[0]
n____(x1, x2) = [0 0] x1 + [1 0] x2 + [0]
[1 0] [0 0] [0]
n__isList(x1) = [1 1] x1 + [0]
[0 0] [0]
isQid(x1) = [1 0] x1 + [1]
[0 0] [1]
n__isNeList(x1) = [1 1] x1 + [0]
[0 0] [0]
isNePal(x1) = [1 0] x1 + [1]
[0 0] [1]
n__isPal(x1) = [1 0] x1 + [0]
[0 0] [0]
isPal(x1) = [1 0] x1 + [1]
[0 0] [1]
n__a() = [0]
[0]
n__e() = [0]
[0]
n__i() = [0]
[0]
n__o() = [0]
[0]
n__u() = [0]
[0]
a() = [0]
[0]
e() = [0]
[0]
i() = [0]
[0]
o() = [0]
[0]
u() = [2]
[0]
The strictly oriented rules are moved into the weak component.
We consider the following Problem:
Strict Trs:
{ 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))
, isPal(V) -> isNePal(activate(V))
, activate(n__nil()) -> nil()
, activate(n____(X1, X2)) -> __(X1, X2)
, activate(n__isList(X)) -> isList(X)
, activate(n__isNeList(X)) -> isNeList(X)
, activate(n__isPal(X)) -> isPal(X)
, activate(n__a()) -> a()
, activate(n__e()) -> e()
, activate(n__i()) -> i()
, activate(n__o()) -> o()
, activate(n__u()) -> u()
, activate(X) -> X}
Weak Trs:
{ u() -> n__u()
, o() -> n__o()
, i() -> n__i()
, e() -> n__e()
, a() -> n__a()
, __(X1, X2) -> n____(X1, X2)
, nil() -> n__nil()
, and(tt(), X) -> activate(X)
, isList(n__nil()) -> tt()
, isPal(n__nil()) -> tt()
, isQid(n__a()) -> tt()
, isQid(n__e()) -> tt()
, isQid(n__i()) -> tt()
, isQid(n__o()) -> tt()
, isQid(n__u()) -> tt()
, isList(X) -> n__isList(X)
, isNeList(X) -> n__isNeList(X)
, isPal(X) -> n__isPal(X)}
StartTerms: basic terms
Strategy: innermost
Certificate: YES(?,O(n^1))
Proof:
The weightgap principle applies, where following rules are oriented strictly:
TRS Component: {isPal(V) -> isNePal(activate(V))}
Interpretation of nonconstant growth:
-------------------------------------
The following argument positions are usable:
Uargs(__) = {}, Uargs(and) = {1, 2}, Uargs(activate) = {},
Uargs(isList) = {1}, Uargs(isNeList) = {1}, Uargs(n____) = {},
Uargs(n__isList) = {1}, Uargs(isQid) = {1},
Uargs(n__isNeList) = {1}, Uargs(isNePal) = {1},
Uargs(n__isPal) = {}, Uargs(isPal) = {}
We have the following EDA-non-satisfying and IDA(1)-non-satisfying matrix interpretation:
Interpretation Functions:
__(x1, x2) = [0 0] x1 + [1 0] x2 + [0]
[1 0] [0 0] [0]
nil() = [0]
[0]
and(x1, x2) = [1 0] x1 + [1 0] x2 + [0]
[0 0] [0 0] [1]
tt() = [0]
[0]
activate(x1) = [1 0] x1 + [0]
[0 0] [0]
isList(x1) = [1 1] x1 + [1]
[0 0] [1]
isNeList(x1) = [1 1] x1 + [1]
[0 0] [1]
n__nil() = [0]
[0]
n____(x1, x2) = [0 0] x1 + [1 0] x2 + [0]
[1 0] [0 0] [0]
n__isList(x1) = [1 1] x1 + [0]
[0 0] [0]
isQid(x1) = [1 0] x1 + [1]
[0 0] [1]
n__isNeList(x1) = [1 1] x1 + [0]
[0 0] [0]
isNePal(x1) = [1 0] x1 + [1]
[0 0] [1]
n__isPal(x1) = [1 0] x1 + [0]
[0 0] [0]
isPal(x1) = [1 0] x1 + [3]
[0 0] [1]
n__a() = [0]
[0]
n__e() = [0]
[0]
n__i() = [0]
[0]
n__o() = [0]
[0]
n__u() = [0]
[0]
a() = [0]
[0]
e() = [0]
[0]
i() = [0]
[0]
o() = [0]
[0]
u() = [0]
[0]
The strictly oriented rules are moved into the weak component.
We consider the following Problem:
Strict Trs:
{ 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))
, activate(n__nil()) -> nil()
, activate(n____(X1, X2)) -> __(X1, X2)
, activate(n__isList(X)) -> isList(X)
, activate(n__isNeList(X)) -> isNeList(X)
, activate(n__isPal(X)) -> isPal(X)
, activate(n__a()) -> a()
, activate(n__e()) -> e()
, activate(n__i()) -> i()
, activate(n__o()) -> o()
, activate(n__u()) -> u()
, activate(X) -> X}
Weak Trs:
{ isPal(V) -> isNePal(activate(V))
, u() -> n__u()
, o() -> n__o()
, i() -> n__i()
, e() -> n__e()
, a() -> n__a()
, __(X1, X2) -> n____(X1, X2)
, nil() -> n__nil()
, and(tt(), X) -> activate(X)
, isList(n__nil()) -> tt()
, isPal(n__nil()) -> tt()
, isQid(n__a()) -> tt()
, isQid(n__e()) -> tt()
, isQid(n__i()) -> tt()
, isQid(n__o()) -> tt()
, isQid(n__u()) -> tt()
, isList(X) -> n__isList(X)
, isNeList(X) -> n__isNeList(X)
, isPal(X) -> n__isPal(X)}
StartTerms: basic terms
Strategy: innermost
Certificate: YES(?,O(n^1))
Proof:
The weightgap principle applies, where following rules are oriented strictly:
TRS Component: {isNePal(V) -> isQid(activate(V))}
Interpretation of nonconstant growth:
-------------------------------------
The following argument positions are usable:
Uargs(__) = {}, Uargs(and) = {1, 2}, Uargs(activate) = {},
Uargs(isList) = {1}, Uargs(isNeList) = {1}, Uargs(n____) = {},
Uargs(n__isList) = {1}, Uargs(isQid) = {1},
Uargs(n__isNeList) = {1}, Uargs(isNePal) = {1},
Uargs(n__isPal) = {}, Uargs(isPal) = {}
We have the following EDA-non-satisfying and IDA(1)-non-satisfying matrix interpretation:
Interpretation Functions:
__(x1, x2) = [0 0] x1 + [1 0] x2 + [0]
[1 0] [0 0] [0]
nil() = [0]
[0]
and(x1, x2) = [1 0] x1 + [1 0] x2 + [0]
[0 0] [0 0] [1]
tt() = [0]
[0]
activate(x1) = [1 0] x1 + [0]
[0 0] [0]
isList(x1) = [1 1] x1 + [1]
[0 0] [1]
isNeList(x1) = [1 1] x1 + [1]
[0 0] [1]
n__nil() = [0]
[0]
n____(x1, x2) = [0 0] x1 + [1 0] x2 + [0]
[1 0] [0 0] [0]
n__isList(x1) = [1 1] x1 + [0]
[0 0] [0]
isQid(x1) = [1 0] x1 + [1]
[0 0] [1]
n__isNeList(x1) = [1 1] x1 + [0]
[0 0] [0]
isNePal(x1) = [1 0] x1 + [3]
[0 0] [1]
n__isPal(x1) = [1 0] x1 + [0]
[0 0] [0]
isPal(x1) = [1 0] x1 + [3]
[0 0] [1]
n__a() = [0]
[0]
n__e() = [0]
[0]
n__i() = [0]
[0]
n__o() = [0]
[0]
n__u() = [0]
[0]
a() = [0]
[0]
e() = [0]
[0]
i() = [0]
[0]
o() = [0]
[0]
u() = [0]
[0]
The strictly oriented rules are moved into the weak component.
We consider the following Problem:
Strict Trs:
{ 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)))
, activate(n__nil()) -> nil()
, activate(n____(X1, X2)) -> __(X1, X2)
, activate(n__isList(X)) -> isList(X)
, activate(n__isNeList(X)) -> isNeList(X)
, activate(n__isPal(X)) -> isPal(X)
, activate(n__a()) -> a()
, activate(n__e()) -> e()
, activate(n__i()) -> i()
, activate(n__o()) -> o()
, activate(n__u()) -> u()
, activate(X) -> X}
Weak Trs:
{ isNePal(V) -> isQid(activate(V))
, isPal(V) -> isNePal(activate(V))
, u() -> n__u()
, o() -> n__o()
, i() -> n__i()
, e() -> n__e()
, a() -> n__a()
, __(X1, X2) -> n____(X1, X2)
, nil() -> n__nil()
, and(tt(), X) -> activate(X)
, isList(n__nil()) -> tt()
, isPal(n__nil()) -> tt()
, isQid(n__a()) -> tt()
, isQid(n__e()) -> tt()
, isQid(n__i()) -> tt()
, isQid(n__o()) -> tt()
, isQid(n__u()) -> tt()
, isList(X) -> n__isList(X)
, isNeList(X) -> n__isNeList(X)
, isPal(X) -> n__isPal(X)}
StartTerms: basic terms
Strategy: innermost
Certificate: YES(?,O(n^1))
Proof:
The weightgap principle applies, where following rules are oriented strictly:
TRS Component: {isNeList(V) -> isQid(activate(V))}
Interpretation of nonconstant growth:
-------------------------------------
The following argument positions are usable:
Uargs(__) = {}, Uargs(and) = {1, 2}, Uargs(activate) = {},
Uargs(isList) = {1}, Uargs(isNeList) = {1}, Uargs(n____) = {},
Uargs(n__isList) = {1}, Uargs(isQid) = {1},
Uargs(n__isNeList) = {1}, Uargs(isNePal) = {1},
Uargs(n__isPal) = {}, Uargs(isPal) = {}
We have the following EDA-non-satisfying and IDA(1)-non-satisfying matrix interpretation:
Interpretation Functions:
__(x1, x2) = [0 0] x1 + [1 0] x2 + [0]
[1 0] [0 0] [0]
nil() = [0]
[0]
and(x1, x2) = [1 0] x1 + [1 0] x2 + [0]
[0 0] [0 0] [1]
tt() = [0]
[0]
activate(x1) = [1 0] x1 + [0]
[0 0] [0]
isList(x1) = [1 1] x1 + [1]
[0 0] [1]
isNeList(x1) = [1 1] x1 + [1]
[0 0] [1]
n__nil() = [0]
[0]
n____(x1, x2) = [0 0] x1 + [1 0] x2 + [0]
[1 0] [0 0] [0]
n__isList(x1) = [1 1] x1 + [0]
[0 0] [0]
isQid(x1) = [1 0] x1 + [0]
[0 0] [0]
n__isNeList(x1) = [1 1] x1 + [0]
[0 0] [0]
isNePal(x1) = [1 0] x1 + [1]
[0 0] [0]
n__isPal(x1) = [1 0] x1 + [0]
[0 0] [0]
isPal(x1) = [1 0] x1 + [1]
[0 0] [0]
n__a() = [1]
[0]
n__e() = [1]
[0]
n__i() = [0]
[0]
n__o() = [1]
[0]
n__u() = [0]
[0]
a() = [1]
[0]
e() = [1]
[0]
i() = [0]
[0]
o() = [1]
[0]
u() = [0]
[0]
The strictly oriented rules are moved into the weak component.
We consider the following Problem:
Strict Trs:
{ isList(V) -> isNeList(activate(V))
, isList(n____(V1, V2)) ->
and(isList(activate(V1)), n__isList(activate(V2)))
, isNeList(n____(V1, V2)) ->
and(isList(activate(V1)), n__isNeList(activate(V2)))
, isNeList(n____(V1, V2)) ->
and(isNeList(activate(V1)), n__isList(activate(V2)))
, activate(n__nil()) -> nil()
, activate(n____(X1, X2)) -> __(X1, X2)
, activate(n__isList(X)) -> isList(X)
, activate(n__isNeList(X)) -> isNeList(X)
, activate(n__isPal(X)) -> isPal(X)
, activate(n__a()) -> a()
, activate(n__e()) -> e()
, activate(n__i()) -> i()
, activate(n__o()) -> o()
, activate(n__u()) -> u()
, activate(X) -> X}
Weak Trs:
{ isNeList(V) -> isQid(activate(V))
, isNePal(V) -> isQid(activate(V))
, isPal(V) -> isNePal(activate(V))
, u() -> n__u()
, o() -> n__o()
, i() -> n__i()
, e() -> n__e()
, a() -> n__a()
, __(X1, X2) -> n____(X1, X2)
, nil() -> n__nil()
, and(tt(), X) -> activate(X)
, isList(n__nil()) -> tt()
, isPal(n__nil()) -> tt()
, isQid(n__a()) -> tt()
, isQid(n__e()) -> tt()
, isQid(n__i()) -> tt()
, isQid(n__o()) -> tt()
, isQid(n__u()) -> tt()
, isList(X) -> n__isList(X)
, isNeList(X) -> n__isNeList(X)
, isPal(X) -> n__isPal(X)}
StartTerms: basic terms
Strategy: innermost
Certificate: YES(?,O(n^1))
Proof:
The weightgap principle applies, where following rules are oriented strictly:
TRS Component: {isList(V) -> isNeList(activate(V))}
Interpretation of nonconstant growth:
-------------------------------------
The following argument positions are usable:
Uargs(__) = {}, Uargs(and) = {1, 2}, Uargs(activate) = {},
Uargs(isList) = {1}, Uargs(isNeList) = {1}, Uargs(n____) = {},
Uargs(n__isList) = {1}, Uargs(isQid) = {1},
Uargs(n__isNeList) = {1}, Uargs(isNePal) = {1},
Uargs(n__isPal) = {}, Uargs(isPal) = {}
We have the following EDA-non-satisfying and IDA(1)-non-satisfying matrix interpretation:
Interpretation Functions:
__(x1, x2) = [0 0] x1 + [1 0] x2 + [0]
[1 0] [0 0] [0]
nil() = [0]
[0]
and(x1, x2) = [1 1] x1 + [1 0] x2 + [0]
[0 0] [0 0] [1]
tt() = [0]
[0]
activate(x1) = [1 0] x1 + [0]
[0 0] [1]
isList(x1) = [1 1] x1 + [3]
[0 0] [3]
isNeList(x1) = [1 1] x1 + [0]
[0 0] [3]
n__nil() = [0]
[0]
n____(x1, x2) = [0 0] x1 + [1 0] x2 + [0]
[1 0] [0 0] [0]
n__isList(x1) = [1 1] x1 + [0]
[0 0] [0]
isQid(x1) = [1 0] x1 + [0]
[0 0] [1]
n__isNeList(x1) = [1 1] x1 + [0]
[0 0] [0]
isNePal(x1) = [1 0] x1 + [0]
[0 0] [1]
n__isPal(x1) = [1 0] x1 + [0]
[0 0] [0]
isPal(x1) = [1 0] x1 + [0]
[0 0] [1]
n__a() = [0]
[0]
n__e() = [0]
[0]
n__i() = [1]
[0]
n__o() = [0]
[0]
n__u() = [1]
[0]
a() = [0]
[0]
e() = [0]
[0]
i() = [1]
[0]
o() = [0]
[0]
u() = [1]
[0]
The strictly oriented rules are moved into the weak component.
We consider the following Problem:
Strict Trs:
{ isList(n____(V1, V2)) ->
and(isList(activate(V1)), n__isList(activate(V2)))
, isNeList(n____(V1, V2)) ->
and(isList(activate(V1)), n__isNeList(activate(V2)))
, isNeList(n____(V1, V2)) ->
and(isNeList(activate(V1)), n__isList(activate(V2)))
, activate(n__nil()) -> nil()
, activate(n____(X1, X2)) -> __(X1, X2)
, activate(n__isList(X)) -> isList(X)
, activate(n__isNeList(X)) -> isNeList(X)
, activate(n__isPal(X)) -> isPal(X)
, activate(n__a()) -> a()
, activate(n__e()) -> e()
, activate(n__i()) -> i()
, activate(n__o()) -> o()
, activate(n__u()) -> u()
, activate(X) -> X}
Weak Trs:
{ isList(V) -> isNeList(activate(V))
, isNeList(V) -> isQid(activate(V))
, isNePal(V) -> isQid(activate(V))
, isPal(V) -> isNePal(activate(V))
, u() -> n__u()
, o() -> n__o()
, i() -> n__i()
, e() -> n__e()
, a() -> n__a()
, __(X1, X2) -> n____(X1, X2)
, nil() -> n__nil()
, and(tt(), X) -> activate(X)
, isList(n__nil()) -> tt()
, isPal(n__nil()) -> tt()
, isQid(n__a()) -> tt()
, isQid(n__e()) -> tt()
, isQid(n__i()) -> tt()
, isQid(n__o()) -> tt()
, isQid(n__u()) -> tt()
, isList(X) -> n__isList(X)
, isNeList(X) -> n__isNeList(X)
, isPal(X) -> n__isPal(X)}
StartTerms: basic terms
Strategy: innermost
Certificate: YES(?,O(n^1))
Proof:
The weightgap principle applies, where following rules are oriented strictly:
TRS Component:
{ isList(n____(V1, V2)) ->
and(isList(activate(V1)), n__isList(activate(V2)))
, isNeList(n____(V1, V2)) ->
and(isList(activate(V1)), n__isNeList(activate(V2)))
, isNeList(n____(V1, V2)) ->
and(isNeList(activate(V1)), n__isList(activate(V2)))}
Interpretation of nonconstant growth:
-------------------------------------
The following argument positions are usable:
Uargs(__) = {}, Uargs(and) = {1, 2}, Uargs(activate) = {},
Uargs(isList) = {1}, Uargs(isNeList) = {1}, Uargs(n____) = {},
Uargs(n__isList) = {1}, Uargs(isQid) = {1},
Uargs(n__isNeList) = {1}, Uargs(isNePal) = {1},
Uargs(n__isPal) = {}, Uargs(isPal) = {}
We have the following EDA-non-satisfying and IDA(1)-non-satisfying matrix interpretation:
Interpretation Functions:
__(x1, x2) = [0 0] x1 + [1 1] x2 + [0]
[1 0] [0 0] [2]
nil() = [0]
[0]
and(x1, x2) = [1 0] x1 + [1 0] x2 + [0]
[0 0] [0 0] [0]
tt() = [0]
[0]
activate(x1) = [1 0] x1 + [0]
[0 0] [0]
isList(x1) = [1 1] x1 + [0]
[0 0] [0]
isNeList(x1) = [1 1] x1 + [0]
[0 0] [0]
n__nil() = [0]
[0]
n____(x1, x2) = [0 0] x1 + [1 1] x2 + [0]
[1 0] [0 0] [1]
n__isList(x1) = [1 1] x1 + [0]
[0 0] [0]
isQid(x1) = [1 0] x1 + [0]
[0 0] [0]
n__isNeList(x1) = [1 1] x1 + [0]
[0 0] [0]
isNePal(x1) = [1 0] x1 + [1]
[0 0] [1]
n__isPal(x1) = [1 0] x1 + [1]
[0 0] [0]
isPal(x1) = [1 0] x1 + [1]
[0 0] [1]
n__a() = [1]
[0]
n__e() = [1]
[0]
n__i() = [0]
[0]
n__o() = [0]
[0]
n__u() = [0]
[0]
a() = [1]
[0]
e() = [1]
[0]
i() = [0]
[0]
o() = [0]
[0]
u() = [0]
[0]
The strictly oriented rules are moved into the weak component.
We consider the following Problem:
Strict Trs:
{ activate(n__nil()) -> nil()
, activate(n____(X1, X2)) -> __(X1, X2)
, activate(n__isList(X)) -> isList(X)
, activate(n__isNeList(X)) -> isNeList(X)
, activate(n__isPal(X)) -> isPal(X)
, activate(n__a()) -> a()
, activate(n__e()) -> e()
, activate(n__i()) -> i()
, activate(n__o()) -> o()
, activate(n__u()) -> u()
, activate(X) -> X}
Weak Trs:
{ isList(n____(V1, V2)) ->
and(isList(activate(V1)), n__isList(activate(V2)))
, isNeList(n____(V1, V2)) ->
and(isList(activate(V1)), n__isNeList(activate(V2)))
, isNeList(n____(V1, V2)) ->
and(isNeList(activate(V1)), n__isList(activate(V2)))
, isList(V) -> isNeList(activate(V))
, isNeList(V) -> isQid(activate(V))
, isNePal(V) -> isQid(activate(V))
, isPal(V) -> isNePal(activate(V))
, u() -> n__u()
, o() -> n__o()
, i() -> n__i()
, e() -> n__e()
, a() -> n__a()
, __(X1, X2) -> n____(X1, X2)
, nil() -> n__nil()
, and(tt(), X) -> activate(X)
, isList(n__nil()) -> tt()
, isPal(n__nil()) -> tt()
, isQid(n__a()) -> tt()
, isQid(n__e()) -> tt()
, isQid(n__i()) -> tt()
, isQid(n__o()) -> tt()
, isQid(n__u()) -> tt()
, isList(X) -> n__isList(X)
, isNeList(X) -> n__isNeList(X)
, isPal(X) -> n__isPal(X)}
StartTerms: basic terms
Strategy: innermost
Certificate: YES(?,O(n^1))
Proof:
The weightgap principle applies, where following rules are oriented strictly:
TRS Component:
{ activate(n__nil()) -> nil()
, activate(n____(X1, X2)) -> __(X1, X2)
, activate(n__a()) -> a()
, activate(n__e()) -> e()
, activate(n__i()) -> i()
, activate(n__o()) -> o()
, activate(n__u()) -> u()
, activate(X) -> X}
Interpretation of nonconstant growth:
-------------------------------------
The following argument positions are usable:
Uargs(__) = {}, Uargs(and) = {1, 2}, Uargs(activate) = {},
Uargs(isList) = {1}, Uargs(isNeList) = {1}, Uargs(n____) = {},
Uargs(n__isList) = {1}, Uargs(isQid) = {1},
Uargs(n__isNeList) = {1}, Uargs(isNePal) = {1},
Uargs(n__isPal) = {}, Uargs(isPal) = {}
We have the following EDA-non-satisfying and IDA(1)-non-satisfying matrix interpretation:
Interpretation Functions:
__(x1, x2) = [1 0] x1 + [1 0] x2 + [3]
[0 1] [0 1] [0]
nil() = [0]
[0]
and(x1, x2) = [1 0] x1 + [1 0] x2 + [0]
[0 0] [0 1] [1]
tt() = [1]
[0]
activate(x1) = [1 0] x1 + [1]
[0 1] [1]
isList(x1) = [1 0] x1 + [2]
[0 0] [1]
isNeList(x1) = [1 0] x1 + [1]
[0 0] [1]
n__nil() = [0]
[0]
n____(x1, x2) = [1 0] x1 + [1 0] x2 + [3]
[0 1] [0 1] [0]
n__isList(x1) = [1 0] x1 + [0]
[0 0] [0]
isQid(x1) = [1 0] x1 + [0]
[0 0] [1]
n__isNeList(x1) = [1 0] x1 + [0]
[0 0] [0]
isNePal(x1) = [1 0] x1 + [1]
[0 0] [1]
n__isPal(x1) = [1 0] x1 + [0]
[0 0] [0]
isPal(x1) = [1 0] x1 + [2]
[0 0] [1]
n__a() = [2]
[0]
n__e() = [2]
[0]
n__i() = [2]
[0]
n__o() = [2]
[0]
n__u() = [2]
[0]
a() = [2]
[0]
e() = [2]
[0]
i() = [2]
[0]
o() = [2]
[0]
u() = [2]
[0]
The strictly oriented rules are moved into the weak component.
We consider the following Problem:
Strict Trs:
{ activate(n__isList(X)) -> isList(X)
, activate(n__isNeList(X)) -> isNeList(X)
, activate(n__isPal(X)) -> isPal(X)}
Weak Trs:
{ activate(n__nil()) -> nil()
, activate(n____(X1, X2)) -> __(X1, X2)
, activate(n__a()) -> a()
, activate(n__e()) -> e()
, activate(n__i()) -> i()
, activate(n__o()) -> o()
, activate(n__u()) -> u()
, activate(X) -> X
, isList(n____(V1, V2)) ->
and(isList(activate(V1)), n__isList(activate(V2)))
, isNeList(n____(V1, V2)) ->
and(isList(activate(V1)), n__isNeList(activate(V2)))
, isNeList(n____(V1, V2)) ->
and(isNeList(activate(V1)), n__isList(activate(V2)))
, isList(V) -> isNeList(activate(V))
, isNeList(V) -> isQid(activate(V))
, isNePal(V) -> isQid(activate(V))
, isPal(V) -> isNePal(activate(V))
, u() -> n__u()
, o() -> n__o()
, i() -> n__i()
, e() -> n__e()
, a() -> n__a()
, __(X1, X2) -> n____(X1, X2)
, nil() -> n__nil()
, and(tt(), X) -> activate(X)
, isList(n__nil()) -> tt()
, isPal(n__nil()) -> tt()
, isQid(n__a()) -> tt()
, isQid(n__e()) -> tt()
, isQid(n__i()) -> tt()
, isQid(n__o()) -> tt()
, isQid(n__u()) -> tt()
, isList(X) -> n__isList(X)
, isNeList(X) -> n__isNeList(X)
, isPal(X) -> n__isPal(X)}
StartTerms: basic terms
Strategy: innermost
Certificate: YES(?,O(n^1))
Proof:
The weightgap principle applies, where following rules are oriented strictly:
TRS Component: {activate(n__isPal(X)) -> isPal(X)}
Interpretation of nonconstant growth:
-------------------------------------
The following argument positions are usable:
Uargs(__) = {}, Uargs(and) = {1, 2}, Uargs(activate) = {},
Uargs(isList) = {1}, Uargs(isNeList) = {1}, Uargs(n____) = {},
Uargs(n__isList) = {1}, Uargs(isQid) = {1},
Uargs(n__isNeList) = {1}, Uargs(isNePal) = {1},
Uargs(n__isPal) = {}, Uargs(isPal) = {}
We have the following EDA-non-satisfying and IDA(1)-non-satisfying matrix interpretation:
Interpretation Functions:
__(x1, x2) = [1 0] x1 + [1 0] x2 + [3]
[0 0] [0 0] [0]
nil() = [3]
[0]
and(x1, x2) = [1 0] x1 + [1 0] x2 + [0]
[0 0] [0 1] [0]
tt() = [2]
[0]
activate(x1) = [1 0] x1 + [1]
[0 1] [0]
isList(x1) = [1 0] x1 + [2]
[0 0] [2]
isNeList(x1) = [1 0] x1 + [1]
[0 0] [1]
n__nil() = [3]
[0]
n____(x1, x2) = [1 0] x1 + [1 0] x2 + [3]
[0 0] [0 0] [0]
n__isList(x1) = [1 0] x1 + [0]
[0 0] [1]
isQid(x1) = [1 0] x1 + [0]
[0 0] [0]
n__isNeList(x1) = [1 0] x1 + [0]
[0 0] [0]
isNePal(x1) = [1 0] x1 + [1]
[0 0] [1]
n__isPal(x1) = [1 0] x1 + [3]
[0 0] [1]
isPal(x1) = [1 0] x1 + [3]
[0 0] [1]
n__a() = [2]
[0]
n__e() = [2]
[0]
n__i() = [2]
[0]
n__o() = [2]
[0]
n__u() = [2]
[0]
a() = [2]
[0]
e() = [2]
[0]
i() = [2]
[0]
o() = [2]
[0]
u() = [2]
[0]
The strictly oriented rules are moved into the weak component.
We consider the following Problem:
Strict Trs:
{ activate(n__isList(X)) -> isList(X)
, activate(n__isNeList(X)) -> isNeList(X)}
Weak Trs:
{ activate(n__isPal(X)) -> isPal(X)
, activate(n__nil()) -> nil()
, activate(n____(X1, X2)) -> __(X1, X2)
, activate(n__a()) -> a()
, activate(n__e()) -> e()
, activate(n__i()) -> i()
, activate(n__o()) -> o()
, activate(n__u()) -> u()
, activate(X) -> X
, isList(n____(V1, V2)) ->
and(isList(activate(V1)), n__isList(activate(V2)))
, isNeList(n____(V1, V2)) ->
and(isList(activate(V1)), n__isNeList(activate(V2)))
, isNeList(n____(V1, V2)) ->
and(isNeList(activate(V1)), n__isList(activate(V2)))
, isList(V) -> isNeList(activate(V))
, isNeList(V) -> isQid(activate(V))
, isNePal(V) -> isQid(activate(V))
, isPal(V) -> isNePal(activate(V))
, u() -> n__u()
, o() -> n__o()
, i() -> n__i()
, e() -> n__e()
, a() -> n__a()
, __(X1, X2) -> n____(X1, X2)
, nil() -> n__nil()
, and(tt(), X) -> activate(X)
, isList(n__nil()) -> tt()
, isPal(n__nil()) -> tt()
, isQid(n__a()) -> tt()
, isQid(n__e()) -> tt()
, isQid(n__i()) -> tt()
, isQid(n__o()) -> tt()
, isQid(n__u()) -> tt()
, isList(X) -> n__isList(X)
, isNeList(X) -> n__isNeList(X)
, isPal(X) -> n__isPal(X)}
StartTerms: basic terms
Strategy: innermost
Certificate: YES(?,O(n^1))
Proof:
The weightgap principle applies, where following rules are oriented strictly:
TRS Component: {activate(n__isNeList(X)) -> isNeList(X)}
Interpretation of nonconstant growth:
-------------------------------------
The following argument positions are usable:
Uargs(__) = {}, Uargs(and) = {1, 2}, Uargs(activate) = {},
Uargs(isList) = {1}, Uargs(isNeList) = {1}, Uargs(n____) = {},
Uargs(n__isList) = {1}, Uargs(isQid) = {1},
Uargs(n__isNeList) = {1}, Uargs(isNePal) = {1},
Uargs(n__isPal) = {}, Uargs(isPal) = {}
We have the following EDA-non-satisfying and IDA(1)-non-satisfying matrix interpretation:
Interpretation Functions:
__(x1, x2) = [1 2] x1 + [1 2] x2 + [2]
[0 0] [0 0] [2]
nil() = [0]
[0]
and(x1, x2) = [1 0] x1 + [1 0] x2 + [0]
[0 1] [0 1] [0]
tt() = [1]
[0]
activate(x1) = [1 0] x1 + [1]
[0 1] [0]
isList(x1) = [1 2] x1 + [2]
[0 0] [0]
isNeList(x1) = [1 1] x1 + [1]
[0 0] [0]
n__nil() = [0]
[0]
n____(x1, x2) = [1 2] x1 + [1 2] x2 + [2]
[0 0] [0 0] [2]
n__isList(x1) = [1 2] x1 + [0]
[0 0] [0]
isQid(x1) = [1 0] x1 + [0]
[0 0] [0]
n__isNeList(x1) = [1 1] x1 + [1]
[0 0] [0]
isNePal(x1) = [1 1] x1 + [1]
[0 0] [1]
n__isPal(x1) = [1 1] x1 + [2]
[0 0] [1]
isPal(x1) = [1 1] x1 + [2]
[0 0] [1]
n__a() = [2]
[0]
n__e() = [1]
[0]
n__i() = [2]
[0]
n__o() = [2]
[0]
n__u() = [1]
[0]
a() = [2]
[0]
e() = [1]
[0]
i() = [2]
[0]
o() = [2]
[0]
u() = [2]
[0]
The strictly oriented rules are moved into the weak component.
We consider the following Problem:
Strict Trs: {activate(n__isList(X)) -> isList(X)}
Weak Trs:
{ activate(n__isNeList(X)) -> isNeList(X)
, activate(n__isPal(X)) -> isPal(X)
, activate(n__nil()) -> nil()
, activate(n____(X1, X2)) -> __(X1, X2)
, activate(n__a()) -> a()
, activate(n__e()) -> e()
, activate(n__i()) -> i()
, activate(n__o()) -> o()
, activate(n__u()) -> u()
, activate(X) -> X
, isList(n____(V1, V2)) ->
and(isList(activate(V1)), n__isList(activate(V2)))
, isNeList(n____(V1, V2)) ->
and(isList(activate(V1)), n__isNeList(activate(V2)))
, isNeList(n____(V1, V2)) ->
and(isNeList(activate(V1)), n__isList(activate(V2)))
, isList(V) -> isNeList(activate(V))
, isNeList(V) -> isQid(activate(V))
, isNePal(V) -> isQid(activate(V))
, isPal(V) -> isNePal(activate(V))
, u() -> n__u()
, o() -> n__o()
, i() -> n__i()
, e() -> n__e()
, a() -> n__a()
, __(X1, X2) -> n____(X1, X2)
, nil() -> n__nil()
, and(tt(), X) -> activate(X)
, isList(n__nil()) -> tt()
, isPal(n__nil()) -> tt()
, isQid(n__a()) -> tt()
, isQid(n__e()) -> tt()
, isQid(n__i()) -> tt()
, isQid(n__o()) -> tt()
, isQid(n__u()) -> tt()
, isList(X) -> n__isList(X)
, isNeList(X) -> n__isNeList(X)
, isPal(X) -> n__isPal(X)}
StartTerms: basic terms
Strategy: innermost
Certificate: YES(?,O(n^1))
Proof:
The weightgap principle applies, where following rules are oriented strictly:
TRS Component: {activate(n__isList(X)) -> isList(X)}
Interpretation of nonconstant growth:
-------------------------------------
The following argument positions are usable:
Uargs(__) = {}, Uargs(and) = {1, 2}, Uargs(activate) = {},
Uargs(isList) = {1}, Uargs(isNeList) = {1},
Uargs(n____) = {}, Uargs(n__isList) = {1},
Uargs(isQid) = {1}, Uargs(n__isNeList) = {1},
Uargs(isNePal) = {1}, Uargs(n__isPal) = {},
Uargs(isPal) = {}
We have the following EDA-non-satisfying and IDA(1)-non-satisfying matrix interpretation:
Interpretation Functions:
__(x1, x2) = [1 0] x1 + [1 0] x2 + [3]
[0 1] [0 1] [3]
nil() = [0]
[0]
and(x1, x2) = [1 1] x1 + [1 0] x2 + [0]
[0 0] [0 1] [0]
tt() = [0]
[1]
activate(x1) = [1 0] x1 + [1]
[0 1] [0]
isList(x1) = [1 1] x1 + [2]
[0 0] [1]
isNeList(x1) = [1 1] x1 + [1]
[0 0] [1]
n__nil() = [0]
[0]
n____(x1, x2) = [1 0] x1 + [1 0] x2 + [3]
[0 1] [0 1] [3]
n__isList(x1) = [1 1] x1 + [2]
[0 0] [1]
isQid(x1) = [1 0] x1 + [0]
[0 0] [1]
n__isNeList(x1) = [1 1] x1 + [0]
[0 0] [1]
isNePal(x1) = [1 0] x1 + [2]
[0 0] [1]
n__isPal(x1) = [1 0] x1 + [3]
[0 1] [2]
isPal(x1) = [1 0] x1 + [3]
[0 1] [2]
n__a() = [0]
[0]
n__e() = [0]
[0]
n__i() = [0]
[1]
n__o() = [0]
[1]
n__u() = [0]
[0]
a() = [0]
[0]
e() = [0]
[0]
i() = [0]
[1]
o() = [0]
[1]
u() = [0]
[0]
The strictly oriented rules are moved into the weak component.
We consider the following Problem:
Weak Trs:
{ activate(n__isList(X)) -> isList(X)
, activate(n__isNeList(X)) -> isNeList(X)
, activate(n__isPal(X)) -> isPal(X)
, activate(n__nil()) -> nil()
, activate(n____(X1, X2)) -> __(X1, X2)
, activate(n__a()) -> a()
, activate(n__e()) -> e()
, activate(n__i()) -> i()
, activate(n__o()) -> o()
, activate(n__u()) -> u()
, activate(X) -> X
, isList(n____(V1, V2)) ->
and(isList(activate(V1)), n__isList(activate(V2)))
, isNeList(n____(V1, V2)) ->
and(isList(activate(V1)), n__isNeList(activate(V2)))
, isNeList(n____(V1, V2)) ->
and(isNeList(activate(V1)), n__isList(activate(V2)))
, isList(V) -> isNeList(activate(V))
, isNeList(V) -> isQid(activate(V))
, isNePal(V) -> isQid(activate(V))
, isPal(V) -> isNePal(activate(V))
, u() -> n__u()
, o() -> n__o()
, i() -> n__i()
, e() -> n__e()
, a() -> n__a()
, __(X1, X2) -> n____(X1, X2)
, nil() -> n__nil()
, and(tt(), X) -> activate(X)
, isList(n__nil()) -> tt()
, isPal(n__nil()) -> tt()
, isQid(n__a()) -> tt()
, isQid(n__e()) -> tt()
, isQid(n__i()) -> tt()
, isQid(n__o()) -> tt()
, isQid(n__u()) -> tt()
, isList(X) -> n__isList(X)
, isNeList(X) -> n__isNeList(X)
, isPal(X) -> n__isPal(X)}
StartTerms: basic terms
Strategy: innermost
Certificate: YES(O(1),O(1))
Proof:
We consider the following Problem:
Weak Trs:
{ activate(n__isList(X)) -> isList(X)
, activate(n__isNeList(X)) -> isNeList(X)
, activate(n__isPal(X)) -> isPal(X)
, activate(n__nil()) -> nil()
, activate(n____(X1, X2)) -> __(X1, X2)
, activate(n__a()) -> a()
, activate(n__e()) -> e()
, activate(n__i()) -> i()
, activate(n__o()) -> o()
, activate(n__u()) -> u()
, activate(X) -> X
, isList(n____(V1, V2)) ->
and(isList(activate(V1)), n__isList(activate(V2)))
, isNeList(n____(V1, V2)) ->
and(isList(activate(V1)), n__isNeList(activate(V2)))
, isNeList(n____(V1, V2)) ->
and(isNeList(activate(V1)), n__isList(activate(V2)))
, isList(V) -> isNeList(activate(V))
, isNeList(V) -> isQid(activate(V))
, isNePal(V) -> isQid(activate(V))
, isPal(V) -> isNePal(activate(V))
, u() -> n__u()
, o() -> n__o()
, i() -> n__i()
, e() -> n__e()
, a() -> n__a()
, __(X1, X2) -> n____(X1, X2)
, nil() -> n__nil()
, and(tt(), X) -> activate(X)
, isList(n__nil()) -> tt()
, isPal(n__nil()) -> tt()
, isQid(n__a()) -> tt()
, isQid(n__e()) -> tt()
, isQid(n__i()) -> tt()
, isQid(n__o()) -> tt()
, isQid(n__u()) -> tt()
, isList(X) -> n__isList(X)
, isNeList(X) -> n__isNeList(X)
, isPal(X) -> n__isPal(X)}
StartTerms: basic terms
Strategy: innermost
Certificate: YES(O(1),O(1))
Proof:
Empty rules are trivially bounded
Hurray, we answered YES(?,O(n^1))