MAYBE
Time: 0.410950
TRS:
{ __(X1, mark X2) -> mark __(X1, X2),
__(mark X1, X2) -> mark __(X1, X2),
__(ok X1, ok X2) -> ok __(X1, X2),
active __(X, nil()) -> mark X,
active __(X1, X2) -> __(X1, active X2),
active __(X1, X2) -> __(active X1, X2),
active __(__(X, Y), Z) -> mark __(X, __(Y, Z)),
active __(nil(), X) -> mark X,
active U12 X -> U12 active X,
active U12 tt() -> mark tt(),
active U11 X -> U11 active X,
active U11 tt() -> mark U12 tt(),
active isNePal X -> isNePal active X,
active isNePal __(I, __(P, I)) -> mark U11 tt(),
U12 mark X -> mark U12 X,
U12 ok X -> ok U12 X,
U11 mark X -> mark U11 X,
U11 ok X -> ok U11 X,
isNePal mark X -> mark isNePal X,
isNePal ok X -> ok isNePal X,
proper __(X1, X2) -> __(proper X1, proper X2),
proper nil() -> ok nil(),
proper U12 X -> U12 proper X,
proper tt() -> ok tt(),
proper U11 X -> U11 proper X,
proper isNePal X -> isNePal proper X,
top mark X -> top proper X,
top ok X -> top active X}
DP:
DP:
{ __#(X1, mark X2) -> __#(X1, X2),
__#(mark X1, X2) -> __#(X1, X2),
__#(ok X1, ok X2) -> __#(X1, X2),
active# __(X1, X2) -> __#(X1, active X2),
active# __(X1, X2) -> __#(active X1, X2),
active# __(X1, X2) -> active# X1,
active# __(X1, X2) -> active# X2,
active# __(__(X, Y), Z) -> __#(X, __(Y, Z)),
active# __(__(X, Y), Z) -> __#(Y, Z),
active# U12 X -> active# X,
active# U12 X -> U12# active X,
active# U11 X -> active# X,
active# U11 X -> U11# active X,
active# U11 tt() -> U12# tt(),
active# isNePal X -> active# X,
active# isNePal X -> isNePal# active X,
active# isNePal __(I, __(P, I)) -> U11# tt(),
U12# mark X -> U12# X,
U12# ok X -> U12# X,
U11# mark X -> U11# X,
U11# ok X -> U11# X,
isNePal# mark X -> isNePal# X,
isNePal# ok X -> isNePal# X,
proper# __(X1, X2) -> __#(proper X1, proper X2),
proper# __(X1, X2) -> proper# X1,
proper# __(X1, X2) -> proper# X2,
proper# U12 X -> U12# proper X,
proper# U12 X -> proper# X,
proper# U11 X -> U11# proper X,
proper# U11 X -> proper# X,
proper# isNePal X -> isNePal# proper X,
proper# isNePal X -> proper# X,
top# mark X -> proper# X,
top# mark X -> top# proper X,
top# ok X -> active# X,
top# ok X -> top# active X}
TRS:
{ __(X1, mark X2) -> mark __(X1, X2),
__(mark X1, X2) -> mark __(X1, X2),
__(ok X1, ok X2) -> ok __(X1, X2),
active __(X, nil()) -> mark X,
active __(X1, X2) -> __(X1, active X2),
active __(X1, X2) -> __(active X1, X2),
active __(__(X, Y), Z) -> mark __(X, __(Y, Z)),
active __(nil(), X) -> mark X,
active U12 X -> U12 active X,
active U12 tt() -> mark tt(),
active U11 X -> U11 active X,
active U11 tt() -> mark U12 tt(),
active isNePal X -> isNePal active X,
active isNePal __(I, __(P, I)) -> mark U11 tt(),
U12 mark X -> mark U12 X,
U12 ok X -> ok U12 X,
U11 mark X -> mark U11 X,
U11 ok X -> ok U11 X,
isNePal mark X -> mark isNePal X,
isNePal ok X -> ok isNePal X,
proper __(X1, X2) -> __(proper X1, proper X2),
proper nil() -> ok nil(),
proper U12 X -> U12 proper X,
proper tt() -> ok tt(),
proper U11 X -> U11 proper X,
proper isNePal X -> isNePal proper X,
top mark X -> top proper X,
top ok X -> top active X}
UR:
{ __(X1, mark X2) -> mark __(X1, X2),
__(mark X1, X2) -> mark __(X1, X2),
__(ok X1, ok X2) -> ok __(X1, X2),
active __(X, nil()) -> mark X,
active __(X1, X2) -> __(X1, active X2),
active __(X1, X2) -> __(active X1, X2),
active __(__(X, Y), Z) -> mark __(X, __(Y, Z)),
active __(nil(), X) -> mark X,
active U12 X -> U12 active X,
active U12 tt() -> mark tt(),
active U11 X -> U11 active X,
active U11 tt() -> mark U12 tt(),
active isNePal X -> isNePal active X,
active isNePal __(I, __(P, I)) -> mark U11 tt(),
U12 mark X -> mark U12 X,
U12 ok X -> ok U12 X,
U11 mark X -> mark U11 X,
U11 ok X -> ok U11 X,
isNePal mark X -> mark isNePal X,
isNePal ok X -> ok isNePal X,
proper __(X1, X2) -> __(proper X1, proper X2),
proper nil() -> ok nil(),
proper U12 X -> U12 proper X,
proper tt() -> ok tt(),
proper U11 X -> U11 proper X,
proper isNePal X -> isNePal proper X}
EDG:
{
(active# U12 X -> active# X, active# isNePal __(I, __(P, I)) -> U11# tt())
(active# U12 X -> active# X, active# isNePal X -> isNePal# active X)
(active# U12 X -> active# X, active# isNePal X -> active# X)
(active# U12 X -> active# X, active# U11 tt() -> U12# tt())
(active# U12 X -> active# X, active# U11 X -> U11# active X)
(active# U12 X -> active# X, active# U11 X -> active# X)
(active# U12 X -> active# X, active# U12 X -> U12# active X)
(active# U12 X -> active# X, active# U12 X -> active# X)
(active# U12 X -> active# X, active# __(__(X, Y), Z) -> __#(Y, Z))
(active# U12 X -> active# X, active# __(__(X, Y), Z) -> __#(X, __(Y, Z)))
(active# U12 X -> active# X, active# __(X1, X2) -> active# X2)
(active# U12 X -> active# X, active# __(X1, X2) -> active# X1)
(active# U12 X -> active# X, active# __(X1, X2) -> __#(active X1, X2))
(active# U12 X -> active# X, active# __(X1, X2) -> __#(X1, active X2))
(active# isNePal X -> active# X, active# isNePal __(I, __(P, I)) -> U11# tt())
(active# isNePal X -> active# X, active# isNePal X -> isNePal# active X)
(active# isNePal X -> active# X, active# isNePal X -> active# X)
(active# isNePal X -> active# X, active# U11 tt() -> U12# tt())
(active# isNePal X -> active# X, active# U11 X -> U11# active X)
(active# isNePal X -> active# X, active# U11 X -> active# X)
(active# isNePal X -> active# X, active# U12 X -> U12# active X)
(active# isNePal X -> active# X, active# U12 X -> active# X)
(active# isNePal X -> active# X, active# __(__(X, Y), Z) -> __#(Y, Z))
(active# isNePal X -> active# X, active# __(__(X, Y), Z) -> __#(X, __(Y, Z)))
(active# isNePal X -> active# X, active# __(X1, X2) -> active# X2)
(active# isNePal X -> active# X, active# __(X1, X2) -> active# X1)
(active# isNePal X -> active# X, active# __(X1, X2) -> __#(active X1, X2))
(active# isNePal X -> active# X, active# __(X1, X2) -> __#(X1, active X2))
(U12# ok X -> U12# X, U12# ok X -> U12# X)
(U12# ok X -> U12# X, U12# mark X -> U12# X)
(U11# ok X -> U11# X, U11# ok X -> U11# X)
(U11# ok X -> U11# X, U11# mark X -> U11# X)
(isNePal# ok X -> isNePal# X, isNePal# ok X -> isNePal# X)
(isNePal# ok X -> isNePal# X, isNePal# mark X -> isNePal# X)
(proper# U11 X -> proper# X, proper# isNePal X -> proper# X)
(proper# U11 X -> proper# X, proper# isNePal X -> isNePal# proper X)
(proper# U11 X -> proper# X, proper# U11 X -> proper# X)
(proper# U11 X -> proper# X, proper# U11 X -> U11# proper X)
(proper# U11 X -> proper# X, proper# U12 X -> proper# X)
(proper# U11 X -> proper# X, proper# U12 X -> U12# proper X)
(proper# U11 X -> proper# X, proper# __(X1, X2) -> proper# X2)
(proper# U11 X -> proper# X, proper# __(X1, X2) -> proper# X1)
(proper# U11 X -> proper# X, proper# __(X1, X2) -> __#(proper X1, proper X2))
(top# mark X -> proper# X, proper# isNePal X -> proper# X)
(top# mark X -> proper# X, proper# isNePal X -> isNePal# proper X)
(top# mark X -> proper# X, proper# U11 X -> proper# X)
(top# mark X -> proper# X, proper# U11 X -> U11# proper X)
(top# mark X -> proper# X, proper# U12 X -> proper# X)
(top# mark X -> proper# X, proper# U12 X -> U12# proper X)
(top# mark X -> proper# X, proper# __(X1, X2) -> proper# X2)
(top# mark X -> proper# X, proper# __(X1, X2) -> proper# X1)
(top# mark X -> proper# X, proper# __(X1, X2) -> __#(proper X1, proper X2))
(active# __(X1, X2) -> __#(active X1, X2), __#(ok X1, ok X2) -> __#(X1, X2))
(active# __(X1, X2) -> __#(active X1, X2), __#(mark X1, X2) -> __#(X1, X2))
(active# __(X1, X2) -> __#(active X1, X2), __#(X1, mark X2) -> __#(X1, X2))
(active# U11 X -> U11# active X, U11# ok X -> U11# X)
(active# U11 X -> U11# active X, U11# mark X -> U11# X)
(active# isNePal X -> isNePal# active X, isNePal# ok X -> isNePal# X)
(active# isNePal X -> isNePal# active X, isNePal# mark X -> isNePal# X)
(proper# U12 X -> U12# proper X, U12# ok X -> U12# X)
(proper# U12 X -> U12# proper X, U12# mark X -> U12# X)
(proper# isNePal X -> isNePal# proper X, isNePal# ok X -> isNePal# X)
(proper# isNePal X -> isNePal# proper X, isNePal# mark X -> isNePal# X)
(top# ok X -> top# active X, top# ok X -> top# active X)
(top# ok X -> top# active X, top# ok X -> active# X)
(top# ok X -> top# active X, top# mark X -> top# proper X)
(top# ok X -> top# active X, top# mark X -> proper# X)
(proper# __(X1, X2) -> proper# X2, proper# isNePal X -> proper# X)
(proper# __(X1, X2) -> proper# X2, proper# isNePal X -> isNePal# proper X)
(proper# __(X1, X2) -> proper# X2, proper# U11 X -> proper# X)
(proper# __(X1, X2) -> proper# X2, proper# U11 X -> U11# proper X)
(proper# __(X1, X2) -> proper# X2, proper# U12 X -> proper# X)
(proper# __(X1, X2) -> proper# X2, proper# U12 X -> U12# proper X)
(proper# __(X1, X2) -> proper# X2, proper# __(X1, X2) -> proper# X2)
(proper# __(X1, X2) -> proper# X2, proper# __(X1, X2) -> proper# X1)
(proper# __(X1, X2) -> proper# X2, proper# __(X1, X2) -> __#(proper X1, proper X2))
(proper# __(X1, X2) -> __#(proper X1, proper X2), __#(ok X1, ok X2) -> __#(X1, X2))
(proper# __(X1, X2) -> __#(proper X1, proper X2), __#(mark X1, X2) -> __#(X1, X2))
(proper# __(X1, X2) -> __#(proper X1, proper X2), __#(X1, mark X2) -> __#(X1, X2))
(proper# __(X1, X2) -> proper# X1, proper# isNePal X -> proper# X)
(proper# __(X1, X2) -> proper# X1, proper# isNePal X -> isNePal# proper X)
(proper# __(X1, X2) -> proper# X1, proper# U11 X -> proper# X)
(proper# __(X1, X2) -> proper# X1, proper# U11 X -> U11# proper X)
(proper# __(X1, X2) -> proper# X1, proper# U12 X -> proper# X)
(proper# __(X1, X2) -> proper# X1, proper# U12 X -> U12# proper X)
(proper# __(X1, X2) -> proper# X1, proper# __(X1, X2) -> proper# X2)
(proper# __(X1, X2) -> proper# X1, proper# __(X1, X2) -> proper# X1)
(proper# __(X1, X2) -> proper# X1, proper# __(X1, X2) -> __#(proper X1, proper X2))
(__#(mark X1, X2) -> __#(X1, X2), __#(ok X1, ok X2) -> __#(X1, X2))
(__#(mark X1, X2) -> __#(X1, X2), __#(mark X1, X2) -> __#(X1, X2))
(__#(mark X1, X2) -> __#(X1, X2), __#(X1, mark X2) -> __#(X1, X2))
(active# __(__(X, Y), Z) -> __#(Y, Z), __#(ok X1, ok X2) -> __#(X1, X2))
(active# __(__(X, Y), Z) -> __#(Y, Z), __#(mark X1, X2) -> __#(X1, X2))
(active# __(__(X, Y), Z) -> __#(Y, Z), __#(X1, mark X2) -> __#(X1, X2))
(__#(ok X1, ok X2) -> __#(X1, X2), __#(X1, mark X2) -> __#(X1, X2))
(__#(ok X1, ok X2) -> __#(X1, X2), __#(mark X1, X2) -> __#(X1, X2))
(__#(ok X1, ok X2) -> __#(X1, X2), __#(ok X1, ok X2) -> __#(X1, X2))
(__#(X1, mark X2) -> __#(X1, X2), __#(X1, mark X2) -> __#(X1, X2))
(__#(X1, mark X2) -> __#(X1, X2), __#(mark X1, X2) -> __#(X1, X2))
(__#(X1, mark X2) -> __#(X1, X2), __#(ok X1, ok X2) -> __#(X1, X2))
(active# __(X1, X2) -> active# X1, active# __(X1, X2) -> __#(X1, active X2))
(active# __(X1, X2) -> active# X1, active# __(X1, X2) -> __#(active X1, X2))
(active# __(X1, X2) -> active# X1, active# __(X1, X2) -> active# X1)
(active# __(X1, X2) -> active# X1, active# __(X1, X2) -> active# X2)
(active# __(X1, X2) -> active# X1, active# __(__(X, Y), Z) -> __#(X, __(Y, Z)))
(active# __(X1, X2) -> active# X1, active# __(__(X, Y), Z) -> __#(Y, Z))
(active# __(X1, X2) -> active# X1, active# U12 X -> active# X)
(active# __(X1, X2) -> active# X1, active# U12 X -> U12# active X)
(active# __(X1, X2) -> active# X1, active# U11 X -> active# X)
(active# __(X1, X2) -> active# X1, active# U11 X -> U11# active X)
(active# __(X1, X2) -> active# X1, active# U11 tt() -> U12# tt())
(active# __(X1, X2) -> active# X1, active# isNePal X -> active# X)
(active# __(X1, X2) -> active# X1, active# isNePal X -> isNePal# active X)
(active# __(X1, X2) -> active# X1, active# isNePal __(I, __(P, I)) -> U11# tt())
(active# __(X1, X2) -> __#(X1, active X2), __#(X1, mark X2) -> __#(X1, X2))
(active# __(X1, X2) -> __#(X1, active X2), __#(mark X1, X2) -> __#(X1, X2))
(active# __(X1, X2) -> __#(X1, active X2), __#(ok X1, ok X2) -> __#(X1, X2))
(active# __(X1, X2) -> active# X2, active# __(X1, X2) -> __#(X1, active X2))
(active# __(X1, X2) -> active# X2, active# __(X1, X2) -> __#(active X1, X2))
(active# __(X1, X2) -> active# X2, active# __(X1, X2) -> active# X1)
(active# __(X1, X2) -> active# X2, active# __(X1, X2) -> active# X2)
(active# __(X1, X2) -> active# X2, active# __(__(X, Y), Z) -> __#(X, __(Y, Z)))
(active# __(X1, X2) -> active# X2, active# __(__(X, Y), Z) -> __#(Y, Z))
(active# __(X1, X2) -> active# X2, active# U12 X -> active# X)
(active# __(X1, X2) -> active# X2, active# U12 X -> U12# active X)
(active# __(X1, X2) -> active# X2, active# U11 X -> active# X)
(active# __(X1, X2) -> active# X2, active# U11 X -> U11# active X)
(active# __(X1, X2) -> active# X2, active# U11 tt() -> U12# tt())
(active# __(X1, X2) -> active# X2, active# isNePal X -> active# X)
(active# __(X1, X2) -> active# X2, active# isNePal X -> isNePal# active X)
(active# __(X1, X2) -> active# X2, active# isNePal __(I, __(P, I)) -> U11# tt())
(top# mark X -> top# proper X, top# mark X -> proper# X)
(top# mark X -> top# proper X, top# mark X -> top# proper X)
(top# mark X -> top# proper X, top# ok X -> active# X)
(top# mark X -> top# proper X, top# ok X -> top# active X)
(proper# U11 X -> U11# proper X, U11# mark X -> U11# X)
(proper# U11 X -> U11# proper X, U11# ok X -> U11# X)
(active# isNePal __(I, __(P, I)) -> U11# tt(), U11# mark X -> U11# X)
(active# isNePal __(I, __(P, I)) -> U11# tt(), U11# ok X -> U11# X)
(active# U11 tt() -> U12# tt(), U12# mark X -> U12# X)
(active# U11 tt() -> U12# tt(), U12# ok X -> U12# X)
(active# U12 X -> U12# active X, U12# mark X -> U12# X)
(active# U12 X -> U12# active X, U12# ok X -> U12# X)
(top# ok X -> active# X, active# __(X1, X2) -> __#(X1, active X2))
(top# ok X -> active# X, active# __(X1, X2) -> __#(active X1, X2))
(top# ok X -> active# X, active# __(X1, X2) -> active# X1)
(top# ok X -> active# X, active# __(X1, X2) -> active# X2)
(top# ok X -> active# X, active# __(__(X, Y), Z) -> __#(X, __(Y, Z)))
(top# ok X -> active# X, active# __(__(X, Y), Z) -> __#(Y, Z))
(top# ok X -> active# X, active# U12 X -> active# X)
(top# ok X -> active# X, active# U12 X -> U12# active X)
(top# ok X -> active# X, active# U11 X -> active# X)
(top# ok X -> active# X, active# U11 X -> U11# active X)
(top# ok X -> active# X, active# U11 tt() -> U12# tt())
(top# ok X -> active# X, active# isNePal X -> active# X)
(top# ok X -> active# X, active# isNePal X -> isNePal# active X)
(top# ok X -> active# X, active# isNePal __(I, __(P, I)) -> U11# tt())
(proper# isNePal X -> proper# X, proper# __(X1, X2) -> __#(proper X1, proper X2))
(proper# isNePal X -> proper# X, proper# __(X1, X2) -> proper# X1)
(proper# isNePal X -> proper# X, proper# __(X1, X2) -> proper# X2)
(proper# isNePal X -> proper# X, proper# U12 X -> U12# proper X)
(proper# isNePal X -> proper# X, proper# U12 X -> proper# X)
(proper# isNePal X -> proper# X, proper# U11 X -> U11# proper X)
(proper# isNePal X -> proper# X, proper# U11 X -> proper# X)
(proper# isNePal X -> proper# X, proper# isNePal X -> isNePal# proper X)
(proper# isNePal X -> proper# X, proper# isNePal X -> proper# X)
(proper# U12 X -> proper# X, proper# __(X1, X2) -> __#(proper X1, proper X2))
(proper# U12 X -> proper# X, proper# __(X1, X2) -> proper# X1)
(proper# U12 X -> proper# X, proper# __(X1, X2) -> proper# X2)
(proper# U12 X -> proper# X, proper# U12 X -> U12# proper X)
(proper# U12 X -> proper# X, proper# U12 X -> proper# X)
(proper# U12 X -> proper# X, proper# U11 X -> U11# proper X)
(proper# U12 X -> proper# X, proper# U11 X -> proper# X)
(proper# U12 X -> proper# X, proper# isNePal X -> isNePal# proper X)
(proper# U12 X -> proper# X, proper# isNePal X -> proper# X)
(isNePal# mark X -> isNePal# X, isNePal# mark X -> isNePal# X)
(isNePal# mark X -> isNePal# X, isNePal# ok X -> isNePal# X)
(U11# mark X -> U11# X, U11# mark X -> U11# X)
(U11# mark X -> U11# X, U11# ok X -> U11# X)
(U12# mark X -> U12# X, U12# mark X -> U12# X)
(U12# mark X -> U12# X, U12# ok X -> U12# X)
(active# U11 X -> active# X, active# __(X1, X2) -> __#(X1, active X2))
(active# U11 X -> active# X, active# __(X1, X2) -> __#(active X1, X2))
(active# U11 X -> active# X, active# __(X1, X2) -> active# X1)
(active# U11 X -> active# X, active# __(X1, X2) -> active# X2)
(active# U11 X -> active# X, active# __(__(X, Y), Z) -> __#(X, __(Y, Z)))
(active# U11 X -> active# X, active# __(__(X, Y), Z) -> __#(Y, Z))
(active# U11 X -> active# X, active# U12 X -> active# X)
(active# U11 X -> active# X, active# U12 X -> U12# active X)
(active# U11 X -> active# X, active# U11 X -> active# X)
(active# U11 X -> active# X, active# U11 X -> U11# active X)
(active# U11 X -> active# X, active# U11 tt() -> U12# tt())
(active# U11 X -> active# X, active# isNePal X -> active# X)
(active# U11 X -> active# X, active# isNePal X -> isNePal# active X)
(active# U11 X -> active# X, active# isNePal __(I, __(P, I)) -> U11# tt())
(active# __(__(X, Y), Z) -> __#(X, __(Y, Z)), __#(X1, mark X2) -> __#(X1, X2))
(active# __(__(X, Y), Z) -> __#(X, __(Y, Z)), __#(mark X1, X2) -> __#(X1, X2))
(active# __(__(X, Y), Z) -> __#(X, __(Y, Z)), __#(ok X1, ok X2) -> __#(X1, X2))
}
STATUS:
arrows: 0.847222
SCCS (7):
Scc:
{top# mark X -> top# proper X,
top# ok X -> top# active X}
Scc:
{proper# __(X1, X2) -> proper# X1,
proper# __(X1, X2) -> proper# X2,
proper# U12 X -> proper# X,
proper# U11 X -> proper# X,
proper# isNePal X -> proper# X}
Scc:
{active# __(X1, X2) -> active# X1,
active# __(X1, X2) -> active# X2,
active# U12 X -> active# X,
active# U11 X -> active# X,
active# isNePal X -> active# X}
Scc:
{isNePal# mark X -> isNePal# X,
isNePal# ok X -> isNePal# X}
Scc:
{U11# mark X -> U11# X,
U11# ok X -> U11# X}
Scc:
{U12# mark X -> U12# X,
U12# ok X -> U12# X}
Scc:
{ __#(X1, mark X2) -> __#(X1, X2),
__#(mark X1, X2) -> __#(X1, X2),
__#(ok X1, ok X2) -> __#(X1, X2)}
SCC (2):
Strict:
{top# mark X -> top# proper X,
top# ok X -> top# active X}
Weak:
{ __(X1, mark X2) -> mark __(X1, X2),
__(mark X1, X2) -> mark __(X1, X2),
__(ok X1, ok X2) -> ok __(X1, X2),
active __(X, nil()) -> mark X,
active __(X1, X2) -> __(X1, active X2),
active __(X1, X2) -> __(active X1, X2),
active __(__(X, Y), Z) -> mark __(X, __(Y, Z)),
active __(nil(), X) -> mark X,
active U12 X -> U12 active X,
active U12 tt() -> mark tt(),
active U11 X -> U11 active X,
active U11 tt() -> mark U12 tt(),
active isNePal X -> isNePal active X,
active isNePal __(I, __(P, I)) -> mark U11 tt(),
U12 mark X -> mark U12 X,
U12 ok X -> ok U12 X,
U11 mark X -> mark U11 X,
U11 ok X -> ok U11 X,
isNePal mark X -> mark isNePal X,
isNePal ok X -> ok isNePal X,
proper __(X1, X2) -> __(proper X1, proper X2),
proper nil() -> ok nil(),
proper U12 X -> U12 proper X,
proper tt() -> ok tt(),
proper U11 X -> U11 proper X,
proper isNePal X -> isNePal proper X,
top mark X -> top proper X,
top ok X -> top active X}
Fail
SCC (5):
Strict:
{proper# __(X1, X2) -> proper# X1,
proper# __(X1, X2) -> proper# X2,
proper# U12 X -> proper# X,
proper# U11 X -> proper# X,
proper# isNePal X -> proper# X}
Weak:
{ __(X1, mark X2) -> mark __(X1, X2),
__(mark X1, X2) -> mark __(X1, X2),
__(ok X1, ok X2) -> ok __(X1, X2),
active __(X, nil()) -> mark X,
active __(X1, X2) -> __(X1, active X2),
active __(X1, X2) -> __(active X1, X2),
active __(__(X, Y), Z) -> mark __(X, __(Y, Z)),
active __(nil(), X) -> mark X,
active U12 X -> U12 active X,
active U12 tt() -> mark tt(),
active U11 X -> U11 active X,
active U11 tt() -> mark U12 tt(),
active isNePal X -> isNePal active X,
active isNePal __(I, __(P, I)) -> mark U11 tt(),
U12 mark X -> mark U12 X,
U12 ok X -> ok U12 X,
U11 mark X -> mark U11 X,
U11 ok X -> ok U11 X,
isNePal mark X -> mark isNePal X,
isNePal ok X -> ok isNePal X,
proper __(X1, X2) -> __(proper X1, proper X2),
proper nil() -> ok nil(),
proper U12 X -> U12 proper X,
proper tt() -> ok tt(),
proper U11 X -> U11 proper X,
proper isNePal X -> isNePal proper X,
top mark X -> top proper X,
top ok X -> top active X}
POLY:
Mode: weak, max_in=1, output_bits=-1, dnum=1, ur=true
Interpretation:
[__](x0, x1) = x0 + x1,
[mark](x0) = 0,
[active](x0) = 0,
[U12](x0) = x0,
[U11](x0) = x0,
[isNePal](x0) = x0 + 1,
[proper](x0) = 0,
[ok](x0) = x0 + 1,
[top](x0) = 0,
[nil] = 0,
[tt] = 0,
[proper#](x0) = x0
Strict:
proper# isNePal X -> proper# X
1 + 1X >= 0 + 1X
proper# U11 X -> proper# X
0 + 1X >= 0 + 1X
proper# U12 X -> proper# X
0 + 1X >= 0 + 1X
proper# __(X1, X2) -> proper# X2
0 + 1X1 + 1X2 >= 0 + 1X2
proper# __(X1, X2) -> proper# X1
0 + 1X1 + 1X2 >= 0 + 1X1
Weak:
top ok X -> top active X
0 + 0X >= 0 + 0X
top mark X -> top proper X
0 + 0X >= 0 + 0X
proper isNePal X -> isNePal proper X
0 + 0X >= 1 + 0X
proper U11 X -> U11 proper X
0 + 0X >= 0 + 0X
proper tt() -> ok tt()
0 >= 1
proper U12 X -> U12 proper X
0 + 0X >= 0 + 0X
proper nil() -> ok nil()
0 >= 1
proper __(X1, X2) -> __(proper X1, proper X2)
0 + 0X1 + 0X2 >= 0 + 0X1 + 0X2
isNePal ok X -> ok isNePal X
2 + 1X >= 2 + 1X
isNePal mark X -> mark isNePal X
1 + 0X >= 0 + 0X
U11 ok X -> ok U11 X
1 + 1X >= 1 + 1X
U11 mark X -> mark U11 X
0 + 0X >= 0 + 0X
U12 ok X -> ok U12 X
1 + 1X >= 1 + 1X
U12 mark X -> mark U12 X
0 + 0X >= 0 + 0X
active isNePal __(I, __(P, I)) -> mark U11 tt()
0 + 0I + 0P >= 0
active isNePal X -> isNePal active X
0 + 0X >= 1 + 0X
active U11 tt() -> mark U12 tt()
0 >= 0
active U11 X -> U11 active X
0 + 0X >= 0 + 0X
active U12 tt() -> mark tt()
0 >= 0
active U12 X -> U12 active X
0 + 0X >= 0 + 0X
active __(nil(), X) -> mark X
0 + 0X >= 0 + 0X
active __(__(X, Y), Z) -> mark __(X, __(Y, Z))
0 + 0X + 0Y + 0Z >= 0 + 0X + 0Y + 0Z
active __(X1, X2) -> __(active X1, X2)
0 + 0X1 + 0X2 >= 0 + 0X1 + 1X2
active __(X1, X2) -> __(X1, active X2)
0 + 0X1 + 0X2 >= 0 + 1X1 + 0X2
active __(X, nil()) -> mark X
0 + 0X >= 0 + 0X
__(ok X1, ok X2) -> ok __(X1, X2)
2 + 1X1 + 1X2 >= 1 + 1X1 + 1X2
__(mark X1, X2) -> mark __(X1, X2)
0 + 0X1 + 1X2 >= 0 + 0X1 + 0X2
__(X1, mark X2) -> mark __(X1, X2)
0 + 1X1 + 0X2 >= 0 + 0X1 + 0X2
SCCS (1):
Scc:
{proper# __(X1, X2) -> proper# X1,
proper# __(X1, X2) -> proper# X2,
proper# U12 X -> proper# X,
proper# U11 X -> proper# X}
SCC (4):
Strict:
{proper# __(X1, X2) -> proper# X1,
proper# __(X1, X2) -> proper# X2,
proper# U12 X -> proper# X,
proper# U11 X -> proper# X}
Weak:
{ __(X1, mark X2) -> mark __(X1, X2),
__(mark X1, X2) -> mark __(X1, X2),
__(ok X1, ok X2) -> ok __(X1, X2),
active __(X, nil()) -> mark X,
active __(X1, X2) -> __(X1, active X2),
active __(X1, X2) -> __(active X1, X2),
active __(__(X, Y), Z) -> mark __(X, __(Y, Z)),
active __(nil(), X) -> mark X,
active U12 X -> U12 active X,
active U12 tt() -> mark tt(),
active U11 X -> U11 active X,
active U11 tt() -> mark U12 tt(),
active isNePal X -> isNePal active X,
active isNePal __(I, __(P, I)) -> mark U11 tt(),
U12 mark X -> mark U12 X,
U12 ok X -> ok U12 X,
U11 mark X -> mark U11 X,
U11 ok X -> ok U11 X,
isNePal mark X -> mark isNePal X,
isNePal ok X -> ok isNePal X,
proper __(X1, X2) -> __(proper X1, proper X2),
proper nil() -> ok nil(),
proper U12 X -> U12 proper X,
proper tt() -> ok tt(),
proper U11 X -> U11 proper X,
proper isNePal X -> isNePal proper X,
top mark X -> top proper X,
top ok X -> top active X}
POLY:
Mode: weak, max_in=1, output_bits=-1, dnum=1, ur=true
Interpretation:
[__](x0, x1) = x0 + x1,
[mark](x0) = 0,
[active](x0) = 0,
[U12](x0) = x0,
[U11](x0) = x0 + 1,
[isNePal](x0) = 0,
[proper](x0) = 0,
[ok](x0) = x0 + 1,
[top](x0) = 0,
[nil] = 0,
[tt] = 0,
[proper#](x0) = x0
Strict:
proper# U11 X -> proper# X
1 + 1X >= 0 + 1X
proper# U12 X -> proper# X
0 + 1X >= 0 + 1X
proper# __(X1, X2) -> proper# X2
0 + 1X1 + 1X2 >= 0 + 1X2
proper# __(X1, X2) -> proper# X1
0 + 1X1 + 1X2 >= 0 + 1X1
Weak:
top ok X -> top active X
0 + 0X >= 0 + 0X
top mark X -> top proper X
0 + 0X >= 0 + 0X
proper isNePal X -> isNePal proper X
0 + 0X >= 0 + 0X
proper U11 X -> U11 proper X
0 + 0X >= 1 + 0X
proper tt() -> ok tt()
0 >= 1
proper U12 X -> U12 proper X
0 + 0X >= 0 + 0X
proper nil() -> ok nil()
0 >= 1
proper __(X1, X2) -> __(proper X1, proper X2)
0 + 0X1 + 0X2 >= 0 + 0X1 + 0X2
isNePal ok X -> ok isNePal X
0 + 0X >= 1 + 0X
isNePal mark X -> mark isNePal X
0 + 0X >= 0 + 0X
U11 ok X -> ok U11 X
2 + 1X >= 2 + 1X
U11 mark X -> mark U11 X
1 + 0X >= 0 + 0X
U12 ok X -> ok U12 X
1 + 1X >= 1 + 1X
U12 mark X -> mark U12 X
0 + 0X >= 0 + 0X
active isNePal __(I, __(P, I)) -> mark U11 tt()
0 + 0I + 0P >= 0
active isNePal X -> isNePal active X
0 + 0X >= 0 + 0X
active U11 tt() -> mark U12 tt()
0 >= 0
active U11 X -> U11 active X
0 + 0X >= 1 + 0X
active U12 tt() -> mark tt()
0 >= 0
active U12 X -> U12 active X
0 + 0X >= 0 + 0X
active __(nil(), X) -> mark X
0 + 0X >= 0 + 0X
active __(__(X, Y), Z) -> mark __(X, __(Y, Z))
0 + 0X + 0Y + 0Z >= 0 + 0X + 0Y + 0Z
active __(X1, X2) -> __(active X1, X2)
0 + 0X1 + 0X2 >= 0 + 0X1 + 1X2
active __(X1, X2) -> __(X1, active X2)
0 + 0X1 + 0X2 >= 0 + 1X1 + 0X2
active __(X, nil()) -> mark X
0 + 0X >= 0 + 0X
__(ok X1, ok X2) -> ok __(X1, X2)
2 + 1X1 + 1X2 >= 1 + 1X1 + 1X2
__(mark X1, X2) -> mark __(X1, X2)
0 + 0X1 + 1X2 >= 0 + 0X1 + 0X2
__(X1, mark X2) -> mark __(X1, X2)
0 + 1X1 + 0X2 >= 0 + 0X1 + 0X2
SCCS (1):
Scc:
{proper# __(X1, X2) -> proper# X1,
proper# __(X1, X2) -> proper# X2,
proper# U12 X -> proper# X}
SCC (3):
Strict:
{proper# __(X1, X2) -> proper# X1,
proper# __(X1, X2) -> proper# X2,
proper# U12 X -> proper# X}
Weak:
{ __(X1, mark X2) -> mark __(X1, X2),
__(mark X1, X2) -> mark __(X1, X2),
__(ok X1, ok X2) -> ok __(X1, X2),
active __(X, nil()) -> mark X,
active __(X1, X2) -> __(X1, active X2),
active __(X1, X2) -> __(active X1, X2),
active __(__(X, Y), Z) -> mark __(X, __(Y, Z)),
active __(nil(), X) -> mark X,
active U12 X -> U12 active X,
active U12 tt() -> mark tt(),
active U11 X -> U11 active X,
active U11 tt() -> mark U12 tt(),
active isNePal X -> isNePal active X,
active isNePal __(I, __(P, I)) -> mark U11 tt(),
U12 mark X -> mark U12 X,
U12 ok X -> ok U12 X,
U11 mark X -> mark U11 X,
U11 ok X -> ok U11 X,
isNePal mark X -> mark isNePal X,
isNePal ok X -> ok isNePal X,
proper __(X1, X2) -> __(proper X1, proper X2),
proper nil() -> ok nil(),
proper U12 X -> U12 proper X,
proper tt() -> ok tt(),
proper U11 X -> U11 proper X,
proper isNePal X -> isNePal proper X,
top mark X -> top proper X,
top ok X -> top active X}
POLY:
Mode: weak, max_in=1, output_bits=-1, dnum=1, ur=true
Interpretation:
[__](x0, x1) = x0 + x1,
[mark](x0) = 0,
[active](x0) = 0,
[U12](x0) = x0 + 1,
[U11](x0) = 0,
[isNePal](x0) = 1,
[proper](x0) = 0,
[ok](x0) = x0,
[top](x0) = 0,
[nil] = 0,
[tt] = 1,
[proper#](x0) = x0
Strict:
proper# U12 X -> proper# X
1 + 1X >= 0 + 1X
proper# __(X1, X2) -> proper# X2
0 + 1X1 + 1X2 >= 0 + 1X2
proper# __(X1, X2) -> proper# X1
0 + 1X1 + 1X2 >= 0 + 1X1
Weak:
top ok X -> top active X
0 + 0X >= 0 + 0X
top mark X -> top proper X
0 + 0X >= 0 + 0X
proper isNePal X -> isNePal proper X
0 + 0X >= 1 + 0X
proper U11 X -> U11 proper X
0 + 0X >= 0 + 0X
proper tt() -> ok tt()
0 >= 1
proper U12 X -> U12 proper X
0 + 0X >= 1 + 0X
proper nil() -> ok nil()
0 >= 0
proper __(X1, X2) -> __(proper X1, proper X2)
0 + 0X1 + 0X2 >= 0 + 0X1 + 0X2
isNePal ok X -> ok isNePal X
1 + 0X >= 1 + 0X
isNePal mark X -> mark isNePal X
1 + 0X >= 0 + 0X
U11 ok X -> ok U11 X
0 + 0X >= 0 + 0X
U11 mark X -> mark U11 X
0 + 0X >= 0 + 0X
U12 ok X -> ok U12 X
1 + 1X >= 1 + 1X
U12 mark X -> mark U12 X
1 + 0X >= 0 + 0X
active isNePal __(I, __(P, I)) -> mark U11 tt()
0 + 0I + 0P >= 0
active isNePal X -> isNePal active X
0 + 0X >= 1 + 0X
active U11 tt() -> mark U12 tt()
0 >= 0
active U11 X -> U11 active X
0 + 0X >= 0 + 0X
active U12 tt() -> mark tt()
0 >= 0
active U12 X -> U12 active X
0 + 0X >= 1 + 0X
active __(nil(), X) -> mark X
0 + 0X >= 0 + 0X
active __(__(X, Y), Z) -> mark __(X, __(Y, Z))
0 + 0X + 0Y + 0Z >= 0 + 0X + 0Y + 0Z
active __(X1, X2) -> __(active X1, X2)
0 + 0X1 + 0X2 >= 0 + 0X1 + 1X2
active __(X1, X2) -> __(X1, active X2)
0 + 0X1 + 0X2 >= 0 + 1X1 + 0X2
active __(X, nil()) -> mark X
0 + 0X >= 0 + 0X
__(ok X1, ok X2) -> ok __(X1, X2)
0 + 1X1 + 1X2 >= 0 + 1X1 + 1X2
__(mark X1, X2) -> mark __(X1, X2)
0 + 0X1 + 1X2 >= 0 + 0X1 + 0X2
__(X1, mark X2) -> mark __(X1, X2)
0 + 1X1 + 0X2 >= 0 + 0X1 + 0X2
SCCS (1):
Scc:
{proper# __(X1, X2) -> proper# X1,
proper# __(X1, X2) -> proper# X2}
SCC (2):
Strict:
{proper# __(X1, X2) -> proper# X1,
proper# __(X1, X2) -> proper# X2}
Weak:
{ __(X1, mark X2) -> mark __(X1, X2),
__(mark X1, X2) -> mark __(X1, X2),
__(ok X1, ok X2) -> ok __(X1, X2),
active __(X, nil()) -> mark X,
active __(X1, X2) -> __(X1, active X2),
active __(X1, X2) -> __(active X1, X2),
active __(__(X, Y), Z) -> mark __(X, __(Y, Z)),
active __(nil(), X) -> mark X,
active U12 X -> U12 active X,
active U12 tt() -> mark tt(),
active U11 X -> U11 active X,
active U11 tt() -> mark U12 tt(),
active isNePal X -> isNePal active X,
active isNePal __(I, __(P, I)) -> mark U11 tt(),
U12 mark X -> mark U12 X,
U12 ok X -> ok U12 X,
U11 mark X -> mark U11 X,
U11 ok X -> ok U11 X,
isNePal mark X -> mark isNePal X,
isNePal ok X -> ok isNePal X,
proper __(X1, X2) -> __(proper X1, proper X2),
proper nil() -> ok nil(),
proper U12 X -> U12 proper X,
proper tt() -> ok tt(),
proper U11 X -> U11 proper X,
proper isNePal X -> isNePal proper X,
top mark X -> top proper X,
top ok X -> top active X}
POLY:
Mode: weak, max_in=1, output_bits=-1, dnum=1, ur=true
Interpretation:
[__](x0, x1) = x0 + x1 + 1,
[mark](x0) = x0 + 1,
[active](x0) = x0 + 1,
[U12](x0) = x0 + 1,
[U11](x0) = 0,
[isNePal](x0) = x0 + 1,
[proper](x0) = 0,
[ok](x0) = 0,
[top](x0) = 0,
[nil] = 0,
[tt] = 0,
[proper#](x0) = x0 + 1
Strict:
proper# __(X1, X2) -> proper# X2
2 + 1X1 + 1X2 >= 1 + 1X2
proper# __(X1, X2) -> proper# X1
2 + 1X1 + 1X2 >= 1 + 1X1
Weak:
top ok X -> top active X
0 + 0X >= 0 + 0X
top mark X -> top proper X
0 + 0X >= 0 + 0X
proper isNePal X -> isNePal proper X
0 + 0X >= 1 + 0X
proper U11 X -> U11 proper X
0 + 0X >= 0 + 0X
proper tt() -> ok tt()
0 >= 0
proper U12 X -> U12 proper X
0 + 0X >= 1 + 0X
proper nil() -> ok nil()
0 >= 0
proper __(X1, X2) -> __(proper X1, proper X2)
0 + 0X1 + 0X2 >= 1 + 0X1 + 0X2
isNePal ok X -> ok isNePal X
1 + 0X >= 0 + 0X
isNePal mark X -> mark isNePal X
2 + 1X >= 2 + 1X
U11 ok X -> ok U11 X
0 + 0X >= 0 + 0X
U11 mark X -> mark U11 X
0 + 0X >= 1 + 0X
U12 ok X -> ok U12 X
1 + 0X >= 0 + 0X
U12 mark X -> mark U12 X
2 + 1X >= 2 + 1X
active isNePal __(I, __(P, I)) -> mark U11 tt()
4 + 2I + 1P >= 1
active isNePal X -> isNePal active X
2 + 1X >= 2 + 1X
active U11 tt() -> mark U12 tt()
1 >= 2
active U11 X -> U11 active X
1 + 0X >= 0 + 0X
active U12 tt() -> mark tt()
2 >= 1
active U12 X -> U12 active X
2 + 1X >= 2 + 1X
active __(nil(), X) -> mark X
2 + 1X >= 1 + 1X
active __(__(X, Y), Z) -> mark __(X, __(Y, Z))
3 + 1X + 1Y + 1Z >= 3 + 1X + 1Y + 1Z
active __(X1, X2) -> __(active X1, X2)
2 + 1X1 + 1X2 >= 2 + 1X1 + 1X2
active __(X1, X2) -> __(X1, active X2)
2 + 1X1 + 1X2 >= 2 + 1X1 + 1X2
active __(X, nil()) -> mark X
2 + 1X >= 1 + 1X
__(ok X1, ok X2) -> ok __(X1, X2)
1 + 0X1 + 0X2 >= 0 + 0X1 + 0X2
__(mark X1, X2) -> mark __(X1, X2)
2 + 1X1 + 1X2 >= 2 + 1X1 + 1X2
__(X1, mark X2) -> mark __(X1, X2)
2 + 1X1 + 1X2 >= 2 + 1X1 + 1X2
Qed
SCC (5):
Strict:
{active# __(X1, X2) -> active# X1,
active# __(X1, X2) -> active# X2,
active# U12 X -> active# X,
active# U11 X -> active# X,
active# isNePal X -> active# X}
Weak:
{ __(X1, mark X2) -> mark __(X1, X2),
__(mark X1, X2) -> mark __(X1, X2),
__(ok X1, ok X2) -> ok __(X1, X2),
active __(X, nil()) -> mark X,
active __(X1, X2) -> __(X1, active X2),
active __(X1, X2) -> __(active X1, X2),
active __(__(X, Y), Z) -> mark __(X, __(Y, Z)),
active __(nil(), X) -> mark X,
active U12 X -> U12 active X,
active U12 tt() -> mark tt(),
active U11 X -> U11 active X,
active U11 tt() -> mark U12 tt(),
active isNePal X -> isNePal active X,
active isNePal __(I, __(P, I)) -> mark U11 tt(),
U12 mark X -> mark U12 X,
U12 ok X -> ok U12 X,
U11 mark X -> mark U11 X,
U11 ok X -> ok U11 X,
isNePal mark X -> mark isNePal X,
isNePal ok X -> ok isNePal X,
proper __(X1, X2) -> __(proper X1, proper X2),
proper nil() -> ok nil(),
proper U12 X -> U12 proper X,
proper tt() -> ok tt(),
proper U11 X -> U11 proper X,
proper isNePal X -> isNePal proper X,
top mark X -> top proper X,
top ok X -> top active X}
POLY:
Mode: weak, max_in=1, output_bits=-1, dnum=1, ur=true
Interpretation:
[__](x0, x1) = x0 + x1,
[mark](x0) = 0,
[active](x0) = 0,
[U12](x0) = x0,
[U11](x0) = x0,
[isNePal](x0) = x0 + 1,
[proper](x0) = 0,
[ok](x0) = x0 + 1,
[top](x0) = 0,
[nil] = 0,
[tt] = 0,
[active#](x0) = x0
Strict:
active# isNePal X -> active# X
1 + 1X >= 0 + 1X
active# U11 X -> active# X
0 + 1X >= 0 + 1X
active# U12 X -> active# X
0 + 1X >= 0 + 1X
active# __(X1, X2) -> active# X2
0 + 1X1 + 1X2 >= 0 + 1X2
active# __(X1, X2) -> active# X1
0 + 1X1 + 1X2 >= 0 + 1X1
Weak:
top ok X -> top active X
0 + 0X >= 0 + 0X
top mark X -> top proper X
0 + 0X >= 0 + 0X
proper isNePal X -> isNePal proper X
0 + 0X >= 1 + 0X
proper U11 X -> U11 proper X
0 + 0X >= 0 + 0X
proper tt() -> ok tt()
0 >= 1
proper U12 X -> U12 proper X
0 + 0X >= 0 + 0X
proper nil() -> ok nil()
0 >= 1
proper __(X1, X2) -> __(proper X1, proper X2)
0 + 0X1 + 0X2 >= 0 + 0X1 + 0X2
isNePal ok X -> ok isNePal X
2 + 1X >= 2 + 1X
isNePal mark X -> mark isNePal X
1 + 0X >= 0 + 0X
U11 ok X -> ok U11 X
1 + 1X >= 1 + 1X
U11 mark X -> mark U11 X
0 + 0X >= 0 + 0X
U12 ok X -> ok U12 X
1 + 1X >= 1 + 1X
U12 mark X -> mark U12 X
0 + 0X >= 0 + 0X
active isNePal __(I, __(P, I)) -> mark U11 tt()
0 + 0I + 0P >= 0
active isNePal X -> isNePal active X
0 + 0X >= 1 + 0X
active U11 tt() -> mark U12 tt()
0 >= 0
active U11 X -> U11 active X
0 + 0X >= 0 + 0X
active U12 tt() -> mark tt()
0 >= 0
active U12 X -> U12 active X
0 + 0X >= 0 + 0X
active __(nil(), X) -> mark X
0 + 0X >= 0 + 0X
active __(__(X, Y), Z) -> mark __(X, __(Y, Z))
0 + 0X + 0Y + 0Z >= 0 + 0X + 0Y + 0Z
active __(X1, X2) -> __(active X1, X2)
0 + 0X1 + 0X2 >= 0 + 0X1 + 1X2
active __(X1, X2) -> __(X1, active X2)
0 + 0X1 + 0X2 >= 0 + 1X1 + 0X2
active __(X, nil()) -> mark X
0 + 0X >= 0 + 0X
__(ok X1, ok X2) -> ok __(X1, X2)
2 + 1X1 + 1X2 >= 1 + 1X1 + 1X2
__(mark X1, X2) -> mark __(X1, X2)
0 + 0X1 + 1X2 >= 0 + 0X1 + 0X2
__(X1, mark X2) -> mark __(X1, X2)
0 + 1X1 + 0X2 >= 0 + 0X1 + 0X2
SCCS (1):
Scc:
{active# __(X1, X2) -> active# X1,
active# __(X1, X2) -> active# X2,
active# U12 X -> active# X,
active# U11 X -> active# X}
SCC (4):
Strict:
{active# __(X1, X2) -> active# X1,
active# __(X1, X2) -> active# X2,
active# U12 X -> active# X,
active# U11 X -> active# X}
Weak:
{ __(X1, mark X2) -> mark __(X1, X2),
__(mark X1, X2) -> mark __(X1, X2),
__(ok X1, ok X2) -> ok __(X1, X2),
active __(X, nil()) -> mark X,
active __(X1, X2) -> __(X1, active X2),
active __(X1, X2) -> __(active X1, X2),
active __(__(X, Y), Z) -> mark __(X, __(Y, Z)),
active __(nil(), X) -> mark X,
active U12 X -> U12 active X,
active U12 tt() -> mark tt(),
active U11 X -> U11 active X,
active U11 tt() -> mark U12 tt(),
active isNePal X -> isNePal active X,
active isNePal __(I, __(P, I)) -> mark U11 tt(),
U12 mark X -> mark U12 X,
U12 ok X -> ok U12 X,
U11 mark X -> mark U11 X,
U11 ok X -> ok U11 X,
isNePal mark X -> mark isNePal X,
isNePal ok X -> ok isNePal X,
proper __(X1, X2) -> __(proper X1, proper X2),
proper nil() -> ok nil(),
proper U12 X -> U12 proper X,
proper tt() -> ok tt(),
proper U11 X -> U11 proper X,
proper isNePal X -> isNePal proper X,
top mark X -> top proper X,
top ok X -> top active X}
POLY:
Mode: weak, max_in=1, output_bits=-1, dnum=1, ur=true
Interpretation:
[__](x0, x1) = x0 + x1,
[mark](x0) = 0,
[active](x0) = 0,
[U12](x0) = x0,
[U11](x0) = x0 + 1,
[isNePal](x0) = 0,
[proper](x0) = 0,
[ok](x0) = x0 + 1,
[top](x0) = 0,
[nil] = 0,
[tt] = 0,
[active#](x0) = x0
Strict:
active# U11 X -> active# X
1 + 1X >= 0 + 1X
active# U12 X -> active# X
0 + 1X >= 0 + 1X
active# __(X1, X2) -> active# X2
0 + 1X1 + 1X2 >= 0 + 1X2
active# __(X1, X2) -> active# X1
0 + 1X1 + 1X2 >= 0 + 1X1
Weak:
top ok X -> top active X
0 + 0X >= 0 + 0X
top mark X -> top proper X
0 + 0X >= 0 + 0X
proper isNePal X -> isNePal proper X
0 + 0X >= 0 + 0X
proper U11 X -> U11 proper X
0 + 0X >= 1 + 0X
proper tt() -> ok tt()
0 >= 1
proper U12 X -> U12 proper X
0 + 0X >= 0 + 0X
proper nil() -> ok nil()
0 >= 1
proper __(X1, X2) -> __(proper X1, proper X2)
0 + 0X1 + 0X2 >= 0 + 0X1 + 0X2
isNePal ok X -> ok isNePal X
0 + 0X >= 1 + 0X
isNePal mark X -> mark isNePal X
0 + 0X >= 0 + 0X
U11 ok X -> ok U11 X
2 + 1X >= 2 + 1X
U11 mark X -> mark U11 X
1 + 0X >= 0 + 0X
U12 ok X -> ok U12 X
1 + 1X >= 1 + 1X
U12 mark X -> mark U12 X
0 + 0X >= 0 + 0X
active isNePal __(I, __(P, I)) -> mark U11 tt()
0 + 0I + 0P >= 0
active isNePal X -> isNePal active X
0 + 0X >= 0 + 0X
active U11 tt() -> mark U12 tt()
0 >= 0
active U11 X -> U11 active X
0 + 0X >= 1 + 0X
active U12 tt() -> mark tt()
0 >= 0
active U12 X -> U12 active X
0 + 0X >= 0 + 0X
active __(nil(), X) -> mark X
0 + 0X >= 0 + 0X
active __(__(X, Y), Z) -> mark __(X, __(Y, Z))
0 + 0X + 0Y + 0Z >= 0 + 0X + 0Y + 0Z
active __(X1, X2) -> __(active X1, X2)
0 + 0X1 + 0X2 >= 0 + 0X1 + 1X2
active __(X1, X2) -> __(X1, active X2)
0 + 0X1 + 0X2 >= 0 + 1X1 + 0X2
active __(X, nil()) -> mark X
0 + 0X >= 0 + 0X
__(ok X1, ok X2) -> ok __(X1, X2)
2 + 1X1 + 1X2 >= 1 + 1X1 + 1X2
__(mark X1, X2) -> mark __(X1, X2)
0 + 0X1 + 1X2 >= 0 + 0X1 + 0X2
__(X1, mark X2) -> mark __(X1, X2)
0 + 1X1 + 0X2 >= 0 + 0X1 + 0X2
SCCS (1):
Scc:
{active# __(X1, X2) -> active# X1,
active# __(X1, X2) -> active# X2,
active# U12 X -> active# X}
SCC (3):
Strict:
{active# __(X1, X2) -> active# X1,
active# __(X1, X2) -> active# X2,
active# U12 X -> active# X}
Weak:
{ __(X1, mark X2) -> mark __(X1, X2),
__(mark X1, X2) -> mark __(X1, X2),
__(ok X1, ok X2) -> ok __(X1, X2),
active __(X, nil()) -> mark X,
active __(X1, X2) -> __(X1, active X2),
active __(X1, X2) -> __(active X1, X2),
active __(__(X, Y), Z) -> mark __(X, __(Y, Z)),
active __(nil(), X) -> mark X,
active U12 X -> U12 active X,
active U12 tt() -> mark tt(),
active U11 X -> U11 active X,
active U11 tt() -> mark U12 tt(),
active isNePal X -> isNePal active X,
active isNePal __(I, __(P, I)) -> mark U11 tt(),
U12 mark X -> mark U12 X,
U12 ok X -> ok U12 X,
U11 mark X -> mark U11 X,
U11 ok X -> ok U11 X,
isNePal mark X -> mark isNePal X,
isNePal ok X -> ok isNePal X,
proper __(X1, X2) -> __(proper X1, proper X2),
proper nil() -> ok nil(),
proper U12 X -> U12 proper X,
proper tt() -> ok tt(),
proper U11 X -> U11 proper X,
proper isNePal X -> isNePal proper X,
top mark X -> top proper X,
top ok X -> top active X}
POLY:
Mode: weak, max_in=1, output_bits=-1, dnum=1, ur=true
Interpretation:
[__](x0, x1) = x0 + x1,
[mark](x0) = 0,
[active](x0) = 0,
[U12](x0) = x0 + 1,
[U11](x0) = 0,
[isNePal](x0) = 1,
[proper](x0) = 0,
[ok](x0) = x0,
[top](x0) = 0,
[nil] = 0,
[tt] = 1,
[active#](x0) = x0
Strict:
active# U12 X -> active# X
1 + 1X >= 0 + 1X
active# __(X1, X2) -> active# X2
0 + 1X1 + 1X2 >= 0 + 1X2
active# __(X1, X2) -> active# X1
0 + 1X1 + 1X2 >= 0 + 1X1
Weak:
top ok X -> top active X
0 + 0X >= 0 + 0X
top mark X -> top proper X
0 + 0X >= 0 + 0X
proper isNePal X -> isNePal proper X
0 + 0X >= 1 + 0X
proper U11 X -> U11 proper X
0 + 0X >= 0 + 0X
proper tt() -> ok tt()
0 >= 1
proper U12 X -> U12 proper X
0 + 0X >= 1 + 0X
proper nil() -> ok nil()
0 >= 0
proper __(X1, X2) -> __(proper X1, proper X2)
0 + 0X1 + 0X2 >= 0 + 0X1 + 0X2
isNePal ok X -> ok isNePal X
1 + 0X >= 1 + 0X
isNePal mark X -> mark isNePal X
1 + 0X >= 0 + 0X
U11 ok X -> ok U11 X
0 + 0X >= 0 + 0X
U11 mark X -> mark U11 X
0 + 0X >= 0 + 0X
U12 ok X -> ok U12 X
1 + 1X >= 1 + 1X
U12 mark X -> mark U12 X
1 + 0X >= 0 + 0X
active isNePal __(I, __(P, I)) -> mark U11 tt()
0 + 0I + 0P >= 0
active isNePal X -> isNePal active X
0 + 0X >= 1 + 0X
active U11 tt() -> mark U12 tt()
0 >= 0
active U11 X -> U11 active X
0 + 0X >= 0 + 0X
active U12 tt() -> mark tt()
0 >= 0
active U12 X -> U12 active X
0 + 0X >= 1 + 0X
active __(nil(), X) -> mark X
0 + 0X >= 0 + 0X
active __(__(X, Y), Z) -> mark __(X, __(Y, Z))
0 + 0X + 0Y + 0Z >= 0 + 0X + 0Y + 0Z
active __(X1, X2) -> __(active X1, X2)
0 + 0X1 + 0X2 >= 0 + 0X1 + 1X2
active __(X1, X2) -> __(X1, active X2)
0 + 0X1 + 0X2 >= 0 + 1X1 + 0X2
active __(X, nil()) -> mark X
0 + 0X >= 0 + 0X
__(ok X1, ok X2) -> ok __(X1, X2)
0 + 1X1 + 1X2 >= 0 + 1X1 + 1X2
__(mark X1, X2) -> mark __(X1, X2)
0 + 0X1 + 1X2 >= 0 + 0X1 + 0X2
__(X1, mark X2) -> mark __(X1, X2)
0 + 1X1 + 0X2 >= 0 + 0X1 + 0X2
SCCS (1):
Scc:
{active# __(X1, X2) -> active# X1,
active# __(X1, X2) -> active# X2}
SCC (2):
Strict:
{active# __(X1, X2) -> active# X1,
active# __(X1, X2) -> active# X2}
Weak:
{ __(X1, mark X2) -> mark __(X1, X2),
__(mark X1, X2) -> mark __(X1, X2),
__(ok X1, ok X2) -> ok __(X1, X2),
active __(X, nil()) -> mark X,
active __(X1, X2) -> __(X1, active X2),
active __(X1, X2) -> __(active X1, X2),
active __(__(X, Y), Z) -> mark __(X, __(Y, Z)),
active __(nil(), X) -> mark X,
active U12 X -> U12 active X,
active U12 tt() -> mark tt(),
active U11 X -> U11 active X,
active U11 tt() -> mark U12 tt(),
active isNePal X -> isNePal active X,
active isNePal __(I, __(P, I)) -> mark U11 tt(),
U12 mark X -> mark U12 X,
U12 ok X -> ok U12 X,
U11 mark X -> mark U11 X,
U11 ok X -> ok U11 X,
isNePal mark X -> mark isNePal X,
isNePal ok X -> ok isNePal X,
proper __(X1, X2) -> __(proper X1, proper X2),
proper nil() -> ok nil(),
proper U12 X -> U12 proper X,
proper tt() -> ok tt(),
proper U11 X -> U11 proper X,
proper isNePal X -> isNePal proper X,
top mark X -> top proper X,
top ok X -> top active X}
POLY:
Mode: weak, max_in=1, output_bits=-1, dnum=1, ur=true
Interpretation:
[__](x0, x1) = x0 + x1 + 1,
[mark](x0) = x0 + 1,
[active](x0) = x0 + 1,
[U12](x0) = x0 + 1,
[U11](x0) = 0,
[isNePal](x0) = x0 + 1,
[proper](x0) = 0,
[ok](x0) = 0,
[top](x0) = 0,
[nil] = 0,
[tt] = 0,
[active#](x0) = x0 + 1
Strict:
active# __(X1, X2) -> active# X2
2 + 1X1 + 1X2 >= 1 + 1X2
active# __(X1, X2) -> active# X1
2 + 1X1 + 1X2 >= 1 + 1X1
Weak:
top ok X -> top active X
0 + 0X >= 0 + 0X
top mark X -> top proper X
0 + 0X >= 0 + 0X
proper isNePal X -> isNePal proper X
0 + 0X >= 1 + 0X
proper U11 X -> U11 proper X
0 + 0X >= 0 + 0X
proper tt() -> ok tt()
0 >= 0
proper U12 X -> U12 proper X
0 + 0X >= 1 + 0X
proper nil() -> ok nil()
0 >= 0
proper __(X1, X2) -> __(proper X1, proper X2)
0 + 0X1 + 0X2 >= 1 + 0X1 + 0X2
isNePal ok X -> ok isNePal X
1 + 0X >= 0 + 0X
isNePal mark X -> mark isNePal X
2 + 1X >= 2 + 1X
U11 ok X -> ok U11 X
0 + 0X >= 0 + 0X
U11 mark X -> mark U11 X
0 + 0X >= 1 + 0X
U12 ok X -> ok U12 X
1 + 0X >= 0 + 0X
U12 mark X -> mark U12 X
2 + 1X >= 2 + 1X
active isNePal __(I, __(P, I)) -> mark U11 tt()
4 + 2I + 1P >= 1
active isNePal X -> isNePal active X
2 + 1X >= 2 + 1X
active U11 tt() -> mark U12 tt()
1 >= 2
active U11 X -> U11 active X
1 + 0X >= 0 + 0X
active U12 tt() -> mark tt()
2 >= 1
active U12 X -> U12 active X
2 + 1X >= 2 + 1X
active __(nil(), X) -> mark X
2 + 1X >= 1 + 1X
active __(__(X, Y), Z) -> mark __(X, __(Y, Z))
3 + 1X + 1Y + 1Z >= 3 + 1X + 1Y + 1Z
active __(X1, X2) -> __(active X1, X2)
2 + 1X1 + 1X2 >= 2 + 1X1 + 1X2
active __(X1, X2) -> __(X1, active X2)
2 + 1X1 + 1X2 >= 2 + 1X1 + 1X2
active __(X, nil()) -> mark X
2 + 1X >= 1 + 1X
__(ok X1, ok X2) -> ok __(X1, X2)
1 + 0X1 + 0X2 >= 0 + 0X1 + 0X2
__(mark X1, X2) -> mark __(X1, X2)
2 + 1X1 + 1X2 >= 2 + 1X1 + 1X2
__(X1, mark X2) -> mark __(X1, X2)
2 + 1X1 + 1X2 >= 2 + 1X1 + 1X2
Qed
SCC (2):
Strict:
{isNePal# mark X -> isNePal# X,
isNePal# ok X -> isNePal# X}
Weak:
{ __(X1, mark X2) -> mark __(X1, X2),
__(mark X1, X2) -> mark __(X1, X2),
__(ok X1, ok X2) -> ok __(X1, X2),
active __(X, nil()) -> mark X,
active __(X1, X2) -> __(X1, active X2),
active __(X1, X2) -> __(active X1, X2),
active __(__(X, Y), Z) -> mark __(X, __(Y, Z)),
active __(nil(), X) -> mark X,
active U12 X -> U12 active X,
active U12 tt() -> mark tt(),
active U11 X -> U11 active X,
active U11 tt() -> mark U12 tt(),
active isNePal X -> isNePal active X,
active isNePal __(I, __(P, I)) -> mark U11 tt(),
U12 mark X -> mark U12 X,
U12 ok X -> ok U12 X,
U11 mark X -> mark U11 X,
U11 ok X -> ok U11 X,
isNePal mark X -> mark isNePal X,
isNePal ok X -> ok isNePal X,
proper __(X1, X2) -> __(proper X1, proper X2),
proper nil() -> ok nil(),
proper U12 X -> U12 proper X,
proper tt() -> ok tt(),
proper U11 X -> U11 proper X,
proper isNePal X -> isNePal proper X,
top mark X -> top proper X,
top ok X -> top active X}
POLY:
Mode: weak, max_in=1, output_bits=-1, dnum=1, ur=true
Interpretation:
[__](x0, x1) = 0,
[mark](x0) = x0,
[active](x0) = 0,
[U12](x0) = 0,
[U11](x0) = 0,
[isNePal](x0) = 0,
[proper](x0) = 0,
[ok](x0) = x0 + 1,
[top](x0) = 0,
[nil] = 1,
[tt] = 0,
[isNePal#](x0) = x0
Strict:
isNePal# ok X -> isNePal# X
1 + 1X >= 0 + 1X
isNePal# mark X -> isNePal# X
0 + 1X >= 0 + 1X
Weak:
top ok X -> top active X
0 + 0X >= 0 + 0X
top mark X -> top proper X
0 + 0X >= 0 + 0X
proper isNePal X -> isNePal proper X
0 + 0X >= 0 + 0X
proper U11 X -> U11 proper X
0 + 0X >= 0 + 0X
proper tt() -> ok tt()
0 >= 1
proper U12 X -> U12 proper X
0 + 0X >= 0 + 0X
proper nil() -> ok nil()
0 >= 2
proper __(X1, X2) -> __(proper X1, proper X2)
0 + 0X1 + 0X2 >= 0 + 0X1 + 0X2
isNePal ok X -> ok isNePal X
0 + 0X >= 1 + 0X
isNePal mark X -> mark isNePal X
0 + 0X >= 0 + 0X
U11 ok X -> ok U11 X
0 + 0X >= 1 + 0X
U11 mark X -> mark U11 X
0 + 0X >= 0 + 0X
U12 ok X -> ok U12 X
0 + 0X >= 1 + 0X
U12 mark X -> mark U12 X
0 + 0X >= 0 + 0X
active isNePal __(I, __(P, I)) -> mark U11 tt()
0 + 0I + 0P >= 0
active isNePal X -> isNePal active X
0 + 0X >= 0 + 0X
active U11 tt() -> mark U12 tt()
0 >= 0
active U11 X -> U11 active X
0 + 0X >= 0 + 0X
active U12 tt() -> mark tt()
0 >= 0
active U12 X -> U12 active X
0 + 0X >= 0 + 0X
active __(nil(), X) -> mark X
0 + 0X >= 0 + 1X
active __(__(X, Y), Z) -> mark __(X, __(Y, Z))
0 + 0X + 0Y + 0Z >= 0 + 0X + 0Y + 0Z
active __(X1, X2) -> __(active X1, X2)
0 + 0X1 + 0X2 >= 0 + 0X1 + 0X2
active __(X1, X2) -> __(X1, active X2)
0 + 0X1 + 0X2 >= 0 + 0X1 + 0X2
active __(X, nil()) -> mark X
0 + 0X >= 0 + 1X
__(ok X1, ok X2) -> ok __(X1, X2)
0 + 0X1 + 0X2 >= 1 + 0X1 + 0X2
__(mark X1, X2) -> mark __(X1, X2)
0 + 0X1 + 0X2 >= 0 + 0X1 + 0X2
__(X1, mark X2) -> mark __(X1, X2)
0 + 0X1 + 0X2 >= 0 + 0X1 + 0X2
SCCS (1):
Scc:
{isNePal# mark X -> isNePal# X}
SCC (1):
Strict:
{isNePal# mark X -> isNePal# X}
Weak:
{ __(X1, mark X2) -> mark __(X1, X2),
__(mark X1, X2) -> mark __(X1, X2),
__(ok X1, ok X2) -> ok __(X1, X2),
active __(X, nil()) -> mark X,
active __(X1, X2) -> __(X1, active X2),
active __(X1, X2) -> __(active X1, X2),
active __(__(X, Y), Z) -> mark __(X, __(Y, Z)),
active __(nil(), X) -> mark X,
active U12 X -> U12 active X,
active U12 tt() -> mark tt(),
active U11 X -> U11 active X,
active U11 tt() -> mark U12 tt(),
active isNePal X -> isNePal active X,
active isNePal __(I, __(P, I)) -> mark U11 tt(),
U12 mark X -> mark U12 X,
U12 ok X -> ok U12 X,
U11 mark X -> mark U11 X,
U11 ok X -> ok U11 X,
isNePal mark X -> mark isNePal X,
isNePal ok X -> ok isNePal X,
proper __(X1, X2) -> __(proper X1, proper X2),
proper nil() -> ok nil(),
proper U12 X -> U12 proper X,
proper tt() -> ok tt(),
proper U11 X -> U11 proper X,
proper isNePal X -> isNePal proper X,
top mark X -> top proper X,
top ok X -> top active X}
POLY:
Mode: weak, max_in=1, output_bits=-1, dnum=1, ur=true
Interpretation:
[__](x0, x1) = x0 + x1 + 1,
[mark](x0) = x0 + 1,
[active](x0) = x0 + 1,
[U12](x0) = x0 + 1,
[U11](x0) = x0 + 1,
[isNePal](x0) = 0,
[proper](x0) = 0,
[ok](x0) = 0,
[top](x0) = 0,
[nil] = 0,
[tt] = 0,
[isNePal#](x0) = x0
Strict:
isNePal# mark X -> isNePal# X
1 + 1X >= 0 + 1X
Weak:
top ok X -> top active X
0 + 0X >= 0 + 0X
top mark X -> top proper X
0 + 0X >= 0 + 0X
proper isNePal X -> isNePal proper X
0 + 0X >= 0 + 0X
proper U11 X -> U11 proper X
0 + 0X >= 1 + 0X
proper tt() -> ok tt()
0 >= 0
proper U12 X -> U12 proper X
0 + 0X >= 1 + 0X
proper nil() -> ok nil()
0 >= 0
proper __(X1, X2) -> __(proper X1, proper X2)
0 + 0X1 + 0X2 >= 1 + 0X1 + 0X2
isNePal ok X -> ok isNePal X
0 + 0X >= 0 + 0X
isNePal mark X -> mark isNePal X
0 + 0X >= 1 + 0X
U11 ok X -> ok U11 X
1 + 0X >= 0 + 0X
U11 mark X -> mark U11 X
2 + 1X >= 2 + 1X
U12 ok X -> ok U12 X
1 + 0X >= 0 + 0X
U12 mark X -> mark U12 X
2 + 1X >= 2 + 1X
active isNePal __(I, __(P, I)) -> mark U11 tt()
1 + 0I + 0P >= 2
active isNePal X -> isNePal active X
1 + 0X >= 0 + 0X
active U11 tt() -> mark U12 tt()
2 >= 2
active U11 X -> U11 active X
2 + 1X >= 2 + 1X
active U12 tt() -> mark tt()
2 >= 1
active U12 X -> U12 active X
2 + 1X >= 2 + 1X
active __(nil(), X) -> mark X
2 + 1X >= 1 + 1X
active __(__(X, Y), Z) -> mark __(X, __(Y, Z))
3 + 1X + 1Y + 1Z >= 3 + 1X + 1Y + 1Z
active __(X1, X2) -> __(active X1, X2)
2 + 1X1 + 1X2 >= 2 + 1X1 + 1X2
active __(X1, X2) -> __(X1, active X2)
2 + 1X1 + 1X2 >= 2 + 1X1 + 1X2
active __(X, nil()) -> mark X
2 + 1X >= 1 + 1X
__(ok X1, ok X2) -> ok __(X1, X2)
1 + 0X1 + 0X2 >= 0 + 0X1 + 0X2
__(mark X1, X2) -> mark __(X1, X2)
2 + 1X1 + 1X2 >= 2 + 1X1 + 1X2
__(X1, mark X2) -> mark __(X1, X2)
2 + 1X1 + 1X2 >= 2 + 1X1 + 1X2
Qed
SCC (2):
Strict:
{U11# mark X -> U11# X,
U11# ok X -> U11# X}
Weak:
{ __(X1, mark X2) -> mark __(X1, X2),
__(mark X1, X2) -> mark __(X1, X2),
__(ok X1, ok X2) -> ok __(X1, X2),
active __(X, nil()) -> mark X,
active __(X1, X2) -> __(X1, active X2),
active __(X1, X2) -> __(active X1, X2),
active __(__(X, Y), Z) -> mark __(X, __(Y, Z)),
active __(nil(), X) -> mark X,
active U12 X -> U12 active X,
active U12 tt() -> mark tt(),
active U11 X -> U11 active X,
active U11 tt() -> mark U12 tt(),
active isNePal X -> isNePal active X,
active isNePal __(I, __(P, I)) -> mark U11 tt(),
U12 mark X -> mark U12 X,
U12 ok X -> ok U12 X,
U11 mark X -> mark U11 X,
U11 ok X -> ok U11 X,
isNePal mark X -> mark isNePal X,
isNePal ok X -> ok isNePal X,
proper __(X1, X2) -> __(proper X1, proper X2),
proper nil() -> ok nil(),
proper U12 X -> U12 proper X,
proper tt() -> ok tt(),
proper U11 X -> U11 proper X,
proper isNePal X -> isNePal proper X,
top mark X -> top proper X,
top ok X -> top active X}
POLY:
Mode: weak, max_in=1, output_bits=-1, dnum=1, ur=true
Interpretation:
[__](x0, x1) = 0,
[mark](x0) = x0,
[active](x0) = 0,
[U12](x0) = 0,
[U11](x0) = 0,
[isNePal](x0) = 0,
[proper](x0) = 0,
[ok](x0) = x0 + 1,
[top](x0) = 0,
[nil] = 1,
[tt] = 0,
[U11#](x0) = x0
Strict:
U11# ok X -> U11# X
1 + 1X >= 0 + 1X
U11# mark X -> U11# X
0 + 1X >= 0 + 1X
Weak:
top ok X -> top active X
0 + 0X >= 0 + 0X
top mark X -> top proper X
0 + 0X >= 0 + 0X
proper isNePal X -> isNePal proper X
0 + 0X >= 0 + 0X
proper U11 X -> U11 proper X
0 + 0X >= 0 + 0X
proper tt() -> ok tt()
0 >= 1
proper U12 X -> U12 proper X
0 + 0X >= 0 + 0X
proper nil() -> ok nil()
0 >= 2
proper __(X1, X2) -> __(proper X1, proper X2)
0 + 0X1 + 0X2 >= 0 + 0X1 + 0X2
isNePal ok X -> ok isNePal X
0 + 0X >= 1 + 0X
isNePal mark X -> mark isNePal X
0 + 0X >= 0 + 0X
U11 ok X -> ok U11 X
0 + 0X >= 1 + 0X
U11 mark X -> mark U11 X
0 + 0X >= 0 + 0X
U12 ok X -> ok U12 X
0 + 0X >= 1 + 0X
U12 mark X -> mark U12 X
0 + 0X >= 0 + 0X
active isNePal __(I, __(P, I)) -> mark U11 tt()
0 + 0I + 0P >= 0
active isNePal X -> isNePal active X
0 + 0X >= 0 + 0X
active U11 tt() -> mark U12 tt()
0 >= 0
active U11 X -> U11 active X
0 + 0X >= 0 + 0X
active U12 tt() -> mark tt()
0 >= 0
active U12 X -> U12 active X
0 + 0X >= 0 + 0X
active __(nil(), X) -> mark X
0 + 0X >= 0 + 1X
active __(__(X, Y), Z) -> mark __(X, __(Y, Z))
0 + 0X + 0Y + 0Z >= 0 + 0X + 0Y + 0Z
active __(X1, X2) -> __(active X1, X2)
0 + 0X1 + 0X2 >= 0 + 0X1 + 0X2
active __(X1, X2) -> __(X1, active X2)
0 + 0X1 + 0X2 >= 0 + 0X1 + 0X2
active __(X, nil()) -> mark X
0 + 0X >= 0 + 1X
__(ok X1, ok X2) -> ok __(X1, X2)
0 + 0X1 + 0X2 >= 1 + 0X1 + 0X2
__(mark X1, X2) -> mark __(X1, X2)
0 + 0X1 + 0X2 >= 0 + 0X1 + 0X2
__(X1, mark X2) -> mark __(X1, X2)
0 + 0X1 + 0X2 >= 0 + 0X1 + 0X2
SCCS (1):
Scc:
{U11# mark X -> U11# X}
SCC (1):
Strict:
{U11# mark X -> U11# X}
Weak:
{ __(X1, mark X2) -> mark __(X1, X2),
__(mark X1, X2) -> mark __(X1, X2),
__(ok X1, ok X2) -> ok __(X1, X2),
active __(X, nil()) -> mark X,
active __(X1, X2) -> __(X1, active X2),
active __(X1, X2) -> __(active X1, X2),
active __(__(X, Y), Z) -> mark __(X, __(Y, Z)),
active __(nil(), X) -> mark X,
active U12 X -> U12 active X,
active U12 tt() -> mark tt(),
active U11 X -> U11 active X,
active U11 tt() -> mark U12 tt(),
active isNePal X -> isNePal active X,
active isNePal __(I, __(P, I)) -> mark U11 tt(),
U12 mark X -> mark U12 X,
U12 ok X -> ok U12 X,
U11 mark X -> mark U11 X,
U11 ok X -> ok U11 X,
isNePal mark X -> mark isNePal X,
isNePal ok X -> ok isNePal X,
proper __(X1, X2) -> __(proper X1, proper X2),
proper nil() -> ok nil(),
proper U12 X -> U12 proper X,
proper tt() -> ok tt(),
proper U11 X -> U11 proper X,
proper isNePal X -> isNePal proper X,
top mark X -> top proper X,
top ok X -> top active X}
POLY:
Mode: weak, max_in=1, output_bits=-1, dnum=1, ur=true
Interpretation:
[__](x0, x1) = x0 + x1 + 1,
[mark](x0) = x0 + 1,
[active](x0) = x0 + 1,
[U12](x0) = x0 + 1,
[U11](x0) = x0 + 1,
[isNePal](x0) = 0,
[proper](x0) = 0,
[ok](x0) = 0,
[top](x0) = 0,
[nil] = 0,
[tt] = 0,
[U11#](x0) = x0
Strict:
U11# mark X -> U11# X
1 + 1X >= 0 + 1X
Weak:
top ok X -> top active X
0 + 0X >= 0 + 0X
top mark X -> top proper X
0 + 0X >= 0 + 0X
proper isNePal X -> isNePal proper X
0 + 0X >= 0 + 0X
proper U11 X -> U11 proper X
0 + 0X >= 1 + 0X
proper tt() -> ok tt()
0 >= 0
proper U12 X -> U12 proper X
0 + 0X >= 1 + 0X
proper nil() -> ok nil()
0 >= 0
proper __(X1, X2) -> __(proper X1, proper X2)
0 + 0X1 + 0X2 >= 1 + 0X1 + 0X2
isNePal ok X -> ok isNePal X
0 + 0X >= 0 + 0X
isNePal mark X -> mark isNePal X
0 + 0X >= 1 + 0X
U11 ok X -> ok U11 X
1 + 0X >= 0 + 0X
U11 mark X -> mark U11 X
2 + 1X >= 2 + 1X
U12 ok X -> ok U12 X
1 + 0X >= 0 + 0X
U12 mark X -> mark U12 X
2 + 1X >= 2 + 1X
active isNePal __(I, __(P, I)) -> mark U11 tt()
1 + 0I + 0P >= 2
active isNePal X -> isNePal active X
1 + 0X >= 0 + 0X
active U11 tt() -> mark U12 tt()
2 >= 2
active U11 X -> U11 active X
2 + 1X >= 2 + 1X
active U12 tt() -> mark tt()
2 >= 1
active U12 X -> U12 active X
2 + 1X >= 2 + 1X
active __(nil(), X) -> mark X
2 + 1X >= 1 + 1X
active __(__(X, Y), Z) -> mark __(X, __(Y, Z))
3 + 1X + 1Y + 1Z >= 3 + 1X + 1Y + 1Z
active __(X1, X2) -> __(active X1, X2)
2 + 1X1 + 1X2 >= 2 + 1X1 + 1X2
active __(X1, X2) -> __(X1, active X2)
2 + 1X1 + 1X2 >= 2 + 1X1 + 1X2
active __(X, nil()) -> mark X
2 + 1X >= 1 + 1X
__(ok X1, ok X2) -> ok __(X1, X2)
1 + 0X1 + 0X2 >= 0 + 0X1 + 0X2
__(mark X1, X2) -> mark __(X1, X2)
2 + 1X1 + 1X2 >= 2 + 1X1 + 1X2
__(X1, mark X2) -> mark __(X1, X2)
2 + 1X1 + 1X2 >= 2 + 1X1 + 1X2
Qed
SCC (2):
Strict:
{U12# mark X -> U12# X,
U12# ok X -> U12# X}
Weak:
{ __(X1, mark X2) -> mark __(X1, X2),
__(mark X1, X2) -> mark __(X1, X2),
__(ok X1, ok X2) -> ok __(X1, X2),
active __(X, nil()) -> mark X,
active __(X1, X2) -> __(X1, active X2),
active __(X1, X2) -> __(active X1, X2),
active __(__(X, Y), Z) -> mark __(X, __(Y, Z)),
active __(nil(), X) -> mark X,
active U12 X -> U12 active X,
active U12 tt() -> mark tt(),
active U11 X -> U11 active X,
active U11 tt() -> mark U12 tt(),
active isNePal X -> isNePal active X,
active isNePal __(I, __(P, I)) -> mark U11 tt(),
U12 mark X -> mark U12 X,
U12 ok X -> ok U12 X,
U11 mark X -> mark U11 X,
U11 ok X -> ok U11 X,
isNePal mark X -> mark isNePal X,
isNePal ok X -> ok isNePal X,
proper __(X1, X2) -> __(proper X1, proper X2),
proper nil() -> ok nil(),
proper U12 X -> U12 proper X,
proper tt() -> ok tt(),
proper U11 X -> U11 proper X,
proper isNePal X -> isNePal proper X,
top mark X -> top proper X,
top ok X -> top active X}
POLY:
Mode: weak, max_in=1, output_bits=-1, dnum=1, ur=true
Interpretation:
[__](x0, x1) = 0,
[mark](x0) = x0,
[active](x0) = 0,
[U12](x0) = 0,
[U11](x0) = 0,
[isNePal](x0) = 0,
[proper](x0) = 0,
[ok](x0) = x0 + 1,
[top](x0) = 0,
[nil] = 1,
[tt] = 0,
[U12#](x0) = x0
Strict:
U12# ok X -> U12# X
1 + 1X >= 0 + 1X
U12# mark X -> U12# X
0 + 1X >= 0 + 1X
Weak:
top ok X -> top active X
0 + 0X >= 0 + 0X
top mark X -> top proper X
0 + 0X >= 0 + 0X
proper isNePal X -> isNePal proper X
0 + 0X >= 0 + 0X
proper U11 X -> U11 proper X
0 + 0X >= 0 + 0X
proper tt() -> ok tt()
0 >= 1
proper U12 X -> U12 proper X
0 + 0X >= 0 + 0X
proper nil() -> ok nil()
0 >= 2
proper __(X1, X2) -> __(proper X1, proper X2)
0 + 0X1 + 0X2 >= 0 + 0X1 + 0X2
isNePal ok X -> ok isNePal X
0 + 0X >= 1 + 0X
isNePal mark X -> mark isNePal X
0 + 0X >= 0 + 0X
U11 ok X -> ok U11 X
0 + 0X >= 1 + 0X
U11 mark X -> mark U11 X
0 + 0X >= 0 + 0X
U12 ok X -> ok U12 X
0 + 0X >= 1 + 0X
U12 mark X -> mark U12 X
0 + 0X >= 0 + 0X
active isNePal __(I, __(P, I)) -> mark U11 tt()
0 + 0I + 0P >= 0
active isNePal X -> isNePal active X
0 + 0X >= 0 + 0X
active U11 tt() -> mark U12 tt()
0 >= 0
active U11 X -> U11 active X
0 + 0X >= 0 + 0X
active U12 tt() -> mark tt()
0 >= 0
active U12 X -> U12 active X
0 + 0X >= 0 + 0X
active __(nil(), X) -> mark X
0 + 0X >= 0 + 1X
active __(__(X, Y), Z) -> mark __(X, __(Y, Z))
0 + 0X + 0Y + 0Z >= 0 + 0X + 0Y + 0Z
active __(X1, X2) -> __(active X1, X2)
0 + 0X1 + 0X2 >= 0 + 0X1 + 0X2
active __(X1, X2) -> __(X1, active X2)
0 + 0X1 + 0X2 >= 0 + 0X1 + 0X2
active __(X, nil()) -> mark X
0 + 0X >= 0 + 1X
__(ok X1, ok X2) -> ok __(X1, X2)
0 + 0X1 + 0X2 >= 1 + 0X1 + 0X2
__(mark X1, X2) -> mark __(X1, X2)
0 + 0X1 + 0X2 >= 0 + 0X1 + 0X2
__(X1, mark X2) -> mark __(X1, X2)
0 + 0X1 + 0X2 >= 0 + 0X1 + 0X2
SCCS (1):
Scc:
{U12# mark X -> U12# X}
SCC (1):
Strict:
{U12# mark X -> U12# X}
Weak:
{ __(X1, mark X2) -> mark __(X1, X2),
__(mark X1, X2) -> mark __(X1, X2),
__(ok X1, ok X2) -> ok __(X1, X2),
active __(X, nil()) -> mark X,
active __(X1, X2) -> __(X1, active X2),
active __(X1, X2) -> __(active X1, X2),
active __(__(X, Y), Z) -> mark __(X, __(Y, Z)),
active __(nil(), X) -> mark X,
active U12 X -> U12 active X,
active U12 tt() -> mark tt(),
active U11 X -> U11 active X,
active U11 tt() -> mark U12 tt(),
active isNePal X -> isNePal active X,
active isNePal __(I, __(P, I)) -> mark U11 tt(),
U12 mark X -> mark U12 X,
U12 ok X -> ok U12 X,
U11 mark X -> mark U11 X,
U11 ok X -> ok U11 X,
isNePal mark X -> mark isNePal X,
isNePal ok X -> ok isNePal X,
proper __(X1, X2) -> __(proper X1, proper X2),
proper nil() -> ok nil(),
proper U12 X -> U12 proper X,
proper tt() -> ok tt(),
proper U11 X -> U11 proper X,
proper isNePal X -> isNePal proper X,
top mark X -> top proper X,
top ok X -> top active X}
POLY:
Mode: weak, max_in=1, output_bits=-1, dnum=1, ur=true
Interpretation:
[__](x0, x1) = x0 + x1 + 1,
[mark](x0) = x0 + 1,
[active](x0) = x0 + 1,
[U12](x0) = x0 + 1,
[U11](x0) = x0 + 1,
[isNePal](x0) = 0,
[proper](x0) = 0,
[ok](x0) = 0,
[top](x0) = 0,
[nil] = 0,
[tt] = 0,
[U12#](x0) = x0
Strict:
U12# mark X -> U12# X
1 + 1X >= 0 + 1X
Weak:
top ok X -> top active X
0 + 0X >= 0 + 0X
top mark X -> top proper X
0 + 0X >= 0 + 0X
proper isNePal X -> isNePal proper X
0 + 0X >= 0 + 0X
proper U11 X -> U11 proper X
0 + 0X >= 1 + 0X
proper tt() -> ok tt()
0 >= 0
proper U12 X -> U12 proper X
0 + 0X >= 1 + 0X
proper nil() -> ok nil()
0 >= 0
proper __(X1, X2) -> __(proper X1, proper X2)
0 + 0X1 + 0X2 >= 1 + 0X1 + 0X2
isNePal ok X -> ok isNePal X
0 + 0X >= 0 + 0X
isNePal mark X -> mark isNePal X
0 + 0X >= 1 + 0X
U11 ok X -> ok U11 X
1 + 0X >= 0 + 0X
U11 mark X -> mark U11 X
2 + 1X >= 2 + 1X
U12 ok X -> ok U12 X
1 + 0X >= 0 + 0X
U12 mark X -> mark U12 X
2 + 1X >= 2 + 1X
active isNePal __(I, __(P, I)) -> mark U11 tt()
1 + 0I + 0P >= 2
active isNePal X -> isNePal active X
1 + 0X >= 0 + 0X
active U11 tt() -> mark U12 tt()
2 >= 2
active U11 X -> U11 active X
2 + 1X >= 2 + 1X
active U12 tt() -> mark tt()
2 >= 1
active U12 X -> U12 active X
2 + 1X >= 2 + 1X
active __(nil(), X) -> mark X
2 + 1X >= 1 + 1X
active __(__(X, Y), Z) -> mark __(X, __(Y, Z))
3 + 1X + 1Y + 1Z >= 3 + 1X + 1Y + 1Z
active __(X1, X2) -> __(active X1, X2)
2 + 1X1 + 1X2 >= 2 + 1X1 + 1X2
active __(X1, X2) -> __(X1, active X2)
2 + 1X1 + 1X2 >= 2 + 1X1 + 1X2
active __(X, nil()) -> mark X
2 + 1X >= 1 + 1X
__(ok X1, ok X2) -> ok __(X1, X2)
1 + 0X1 + 0X2 >= 0 + 0X1 + 0X2
__(mark X1, X2) -> mark __(X1, X2)
2 + 1X1 + 1X2 >= 2 + 1X1 + 1X2
__(X1, mark X2) -> mark __(X1, X2)
2 + 1X1 + 1X2 >= 2 + 1X1 + 1X2
Qed
SCC (3):
Strict:
{ __#(X1, mark X2) -> __#(X1, X2),
__#(mark X1, X2) -> __#(X1, X2),
__#(ok X1, ok X2) -> __#(X1, X2)}
Weak:
{ __(X1, mark X2) -> mark __(X1, X2),
__(mark X1, X2) -> mark __(X1, X2),
__(ok X1, ok X2) -> ok __(X1, X2),
active __(X, nil()) -> mark X,
active __(X1, X2) -> __(X1, active X2),
active __(X1, X2) -> __(active X1, X2),
active __(__(X, Y), Z) -> mark __(X, __(Y, Z)),
active __(nil(), X) -> mark X,
active U12 X -> U12 active X,
active U12 tt() -> mark tt(),
active U11 X -> U11 active X,
active U11 tt() -> mark U12 tt(),
active isNePal X -> isNePal active X,
active isNePal __(I, __(P, I)) -> mark U11 tt(),
U12 mark X -> mark U12 X,
U12 ok X -> ok U12 X,
U11 mark X -> mark U11 X,
U11 ok X -> ok U11 X,
isNePal mark X -> mark isNePal X,
isNePal ok X -> ok isNePal X,
proper __(X1, X2) -> __(proper X1, proper X2),
proper nil() -> ok nil(),
proper U12 X -> U12 proper X,
proper tt() -> ok tt(),
proper U11 X -> U11 proper X,
proper isNePal X -> isNePal proper X,
top mark X -> top proper X,
top ok X -> top active X}
POLY:
Mode: weak, max_in=1, output_bits=-1, dnum=1, ur=true
Interpretation:
[__](x0, x1) = x0 + 1,
[mark](x0) = x0 + 1,
[active](x0) = 0,
[U12](x0) = 0,
[U11](x0) = 0,
[isNePal](x0) = x0 + 1,
[proper](x0) = 0,
[ok](x0) = x0 + 1,
[top](x0) = 0,
[nil] = 1,
[tt] = 1,
[__#](x0, x1) = x0 + 1
Strict:
__#(ok X1, ok X2) -> __#(X1, X2)
2 + 1X1 + 0X2 >= 1 + 1X1 + 0X2
__#(mark X1, X2) -> __#(X1, X2)
2 + 1X1 + 0X2 >= 1 + 1X1 + 0X2
__#(X1, mark X2) -> __#(X1, X2)
1 + 1X1 + 0X2 >= 1 + 1X1 + 0X2
Weak:
top ok X -> top active X
0 + 0X >= 0 + 0X
top mark X -> top proper X
0 + 0X >= 0 + 0X
proper isNePal X -> isNePal proper X
0 + 0X >= 1 + 0X
proper U11 X -> U11 proper X
0 + 0X >= 0 + 0X
proper tt() -> ok tt()
0 >= 2
proper U12 X -> U12 proper X
0 + 0X >= 0 + 0X
proper nil() -> ok nil()
0 >= 2
proper __(X1, X2) -> __(proper X1, proper X2)
0 + 0X1 + 0X2 >= 1 + 0X1 + 0X2
isNePal ok X -> ok isNePal X
2 + 1X >= 2 + 1X
isNePal mark X -> mark isNePal X
2 + 1X >= 2 + 1X
U11 ok X -> ok U11 X
0 + 0X >= 1 + 0X
U11 mark X -> mark U11 X
0 + 0X >= 1 + 0X
U12 ok X -> ok U12 X
0 + 0X >= 1 + 0X
U12 mark X -> mark U12 X
0 + 0X >= 1 + 0X
active isNePal __(I, __(P, I)) -> mark U11 tt()
0 + 0I + 0P >= 1
active isNePal X -> isNePal active X
0 + 0X >= 1 + 0X
active U11 tt() -> mark U12 tt()
0 >= 1
active U11 X -> U11 active X
0 + 0X >= 0 + 0X
active U12 tt() -> mark tt()
0 >= 2
active U12 X -> U12 active X
0 + 0X >= 0 + 0X
active __(nil(), X) -> mark X
0 + 0X >= 1 + 1X
active __(__(X, Y), Z) -> mark __(X, __(Y, Z))
0 + 0X + 0Y + 0Z >= 3 + 0X + 0Y + 1Z
active __(X1, X2) -> __(active X1, X2)
0 + 0X1 + 0X2 >= 1 + 0X1 + 1X2
active __(X1, X2) -> __(X1, active X2)
0 + 0X1 + 0X2 >= 1 + 0X1 + 0X2
active __(X, nil()) -> mark X
0 + 0X >= 1 + 1X
__(ok X1, ok X2) -> ok __(X1, X2)
2 + 0X1 + 1X2 >= 2 + 0X1 + 1X2
__(mark X1, X2) -> mark __(X1, X2)
1 + 0X1 + 1X2 >= 2 + 0X1 + 1X2
__(X1, mark X2) -> mark __(X1, X2)
2 + 0X1 + 1X2 >= 2 + 0X1 + 1X2
SCCS (1):
Scc:
{__#(X1, mark X2) -> __#(X1, X2)}
SCC (1):
Strict:
{__#(X1, mark X2) -> __#(X1, X2)}
Weak:
{ __(X1, mark X2) -> mark __(X1, X2),
__(mark X1, X2) -> mark __(X1, X2),
__(ok X1, ok X2) -> ok __(X1, X2),
active __(X, nil()) -> mark X,
active __(X1, X2) -> __(X1, active X2),
active __(X1, X2) -> __(active X1, X2),
active __(__(X, Y), Z) -> mark __(X, __(Y, Z)),
active __(nil(), X) -> mark X,
active U12 X -> U12 active X,
active U12 tt() -> mark tt(),
active U11 X -> U11 active X,
active U11 tt() -> mark U12 tt(),
active isNePal X -> isNePal active X,
active isNePal __(I, __(P, I)) -> mark U11 tt(),
U12 mark X -> mark U12 X,
U12 ok X -> ok U12 X,
U11 mark X -> mark U11 X,
U11 ok X -> ok U11 X,
isNePal mark X -> mark isNePal X,
isNePal ok X -> ok isNePal X,
proper __(X1, X2) -> __(proper X1, proper X2),
proper nil() -> ok nil(),
proper U12 X -> U12 proper X,
proper tt() -> ok tt(),
proper U11 X -> U11 proper X,
proper isNePal X -> isNePal proper X,
top mark X -> top proper X,
top ok X -> top active X}
POLY:
Mode: weak, max_in=1, output_bits=-1, dnum=1, ur=true
Interpretation:
[__](x0, x1) = x0 + x1 + 1,
[mark](x0) = x0 + 1,
[active](x0) = x0 + 1,
[U12](x0) = x0 + 1,
[U11](x0) = x0 + 1,
[isNePal](x0) = 0,
[proper](x0) = 0,
[ok](x0) = 0,
[top](x0) = 0,
[nil] = 0,
[tt] = 0,
[__#](x0, x1) = x0
Strict:
__#(X1, mark X2) -> __#(X1, X2)
1 + 0X1 + 1X2 >= 0 + 0X1 + 1X2
Weak:
top ok X -> top active X
0 + 0X >= 0 + 0X
top mark X -> top proper X
0 + 0X >= 0 + 0X
proper isNePal X -> isNePal proper X
0 + 0X >= 0 + 0X
proper U11 X -> U11 proper X
0 + 0X >= 1 + 0X
proper tt() -> ok tt()
0 >= 0
proper U12 X -> U12 proper X
0 + 0X >= 1 + 0X
proper nil() -> ok nil()
0 >= 0
proper __(X1, X2) -> __(proper X1, proper X2)
0 + 0X1 + 0X2 >= 1 + 0X1 + 0X2
isNePal ok X -> ok isNePal X
0 + 0X >= 0 + 0X
isNePal mark X -> mark isNePal X
0 + 0X >= 1 + 0X
U11 ok X -> ok U11 X
1 + 0X >= 0 + 0X
U11 mark X -> mark U11 X
2 + 1X >= 2 + 1X
U12 ok X -> ok U12 X
1 + 0X >= 0 + 0X
U12 mark X -> mark U12 X
2 + 1X >= 2 + 1X
active isNePal __(I, __(P, I)) -> mark U11 tt()
1 + 0I + 0P >= 2
active isNePal X -> isNePal active X
1 + 0X >= 0 + 0X
active U11 tt() -> mark U12 tt()
2 >= 2
active U11 X -> U11 active X
2 + 1X >= 2 + 1X
active U12 tt() -> mark tt()
2 >= 1
active U12 X -> U12 active X
2 + 1X >= 2 + 1X
active __(nil(), X) -> mark X
2 + 1X >= 1 + 1X
active __(__(X, Y), Z) -> mark __(X, __(Y, Z))
3 + 1X + 1Y + 1Z >= 3 + 1X + 1Y + 1Z
active __(X1, X2) -> __(active X1, X2)
2 + 1X1 + 1X2 >= 2 + 1X1 + 1X2
active __(X1, X2) -> __(X1, active X2)
2 + 1X1 + 1X2 >= 2 + 1X1 + 1X2
active __(X, nil()) -> mark X
2 + 1X >= 1 + 1X
__(ok X1, ok X2) -> ok __(X1, X2)
1 + 0X1 + 0X2 >= 0 + 0X1 + 0X2
__(mark X1, X2) -> mark __(X1, X2)
2 + 1X1 + 1X2 >= 2 + 1X1 + 1X2
__(X1, mark X2) -> mark __(X1, X2)
2 + 1X1 + 1X2 >= 2 + 1X1 + 1X2
Qed