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