YES
Time: 0.425293
TRS:
{ active first(X1, X2) -> first(X1, active X2),
active first(X1, X2) -> first(active X1, X2),
active first(0(), X) -> mark nil(),
active first(s X, cons(Y, Z)) -> mark cons(Y, first(X, Z)),
active cons(X1, X2) -> cons(active X1, X2),
active s X -> s active X,
active from X -> mark cons(X, from s X),
active from X -> from active X,
first(X1, mark X2) -> mark first(X1, X2),
first(mark X1, X2) -> mark first(X1, X2),
first(ok X1, ok X2) -> ok first(X1, X2),
cons(mark X1, X2) -> mark cons(X1, X2),
cons(ok X1, ok X2) -> ok cons(X1, X2),
s mark X -> mark s X,
s ok X -> ok s X,
from mark X -> mark from X,
from ok X -> ok from X,
proper nil() -> ok nil(),
proper first(X1, X2) -> first(proper X1, proper X2),
proper 0() -> ok 0(),
proper cons(X1, X2) -> cons(proper X1, proper X2),
proper s X -> s proper X,
proper from X -> from proper X,
top mark X -> top proper X,
top ok X -> top active X}
DP:
DP:
{ active# first(X1, X2) -> active# X1,
active# first(X1, X2) -> active# X2,
active# first(X1, X2) -> first#(X1, active X2),
active# first(X1, X2) -> first#(active X1, X2),
active# first(s X, cons(Y, Z)) -> first#(X, Z),
active# first(s X, cons(Y, Z)) -> cons#(Y, first(X, Z)),
active# cons(X1, X2) -> active# X1,
active# cons(X1, X2) -> cons#(active X1, X2),
active# s X -> active# X,
active# s X -> s# active X,
active# from X -> active# X,
active# from X -> cons#(X, from s X),
active# from X -> s# X,
active# from X -> from# active X,
active# from X -> from# s X,
first#(X1, mark X2) -> first#(X1, X2),
first#(mark X1, X2) -> first#(X1, X2),
first#(ok X1, ok X2) -> first#(X1, X2),
cons#(mark X1, X2) -> cons#(X1, X2),
cons#(ok X1, ok X2) -> cons#(X1, X2),
s# mark X -> s# X,
s# ok X -> s# X,
from# mark X -> from# X,
from# ok X -> from# X,
proper# first(X1, X2) -> first#(proper X1, proper X2),
proper# first(X1, X2) -> proper# X1,
proper# first(X1, X2) -> proper# X2,
proper# cons(X1, X2) -> cons#(proper X1, proper X2),
proper# cons(X1, X2) -> proper# X1,
proper# cons(X1, X2) -> proper# X2,
proper# s X -> s# proper X,
proper# s X -> proper# X,
proper# from X -> from# proper X,
proper# from 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:
{ active first(X1, X2) -> first(X1, active X2),
active first(X1, X2) -> first(active X1, X2),
active first(0(), X) -> mark nil(),
active first(s X, cons(Y, Z)) -> mark cons(Y, first(X, Z)),
active cons(X1, X2) -> cons(active X1, X2),
active s X -> s active X,
active from X -> mark cons(X, from s X),
active from X -> from active X,
first(X1, mark X2) -> mark first(X1, X2),
first(mark X1, X2) -> mark first(X1, X2),
first(ok X1, ok X2) -> ok first(X1, X2),
cons(mark X1, X2) -> mark cons(X1, X2),
cons(ok X1, ok X2) -> ok cons(X1, X2),
s mark X -> mark s X,
s ok X -> ok s X,
from mark X -> mark from X,
from ok X -> ok from X,
proper nil() -> ok nil(),
proper first(X1, X2) -> first(proper X1, proper X2),
proper 0() -> ok 0(),
proper cons(X1, X2) -> cons(proper X1, proper X2),
proper s X -> s proper X,
proper from X -> from proper X,
top mark X -> top proper X,
top ok X -> top active X}
EDG:
{
(active# s X -> s# active X, s# ok X -> s# X)
(active# s X -> s# active X, s# mark X -> s# X)
(active# from X -> from# s X, from# ok X -> from# X)
(active# from X -> from# s X, from# mark X -> from# X)
(proper# from X -> from# proper X, from# ok X -> from# X)
(proper# from X -> from# proper X, from# mark X -> from# 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)
(active# cons(X1, X2) -> cons#(active X1, X2), cons#(ok X1, ok X2) -> cons#(X1, X2))
(active# cons(X1, X2) -> cons#(active X1, X2), cons#(mark X1, X2) -> cons#(X1, X2))
(first#(mark X1, X2) -> first#(X1, X2), first#(ok X1, ok X2) -> first#(X1, X2))
(first#(mark X1, X2) -> first#(X1, X2), first#(mark X1, X2) -> first#(X1, X2))
(first#(mark X1, X2) -> first#(X1, X2), first#(X1, mark X2) -> first#(X1, X2))
(cons#(mark X1, X2) -> cons#(X1, X2), cons#(ok X1, ok X2) -> cons#(X1, X2))
(cons#(mark X1, X2) -> cons#(X1, X2), cons#(mark X1, X2) -> cons#(X1, X2))
(active# first(X1, X2) -> first#(X1, active X2), first#(ok X1, ok X2) -> first#(X1, X2))
(active# first(X1, X2) -> first#(X1, active X2), first#(mark X1, X2) -> first#(X1, X2))
(active# first(X1, X2) -> first#(X1, active X2), first#(X1, mark X2) -> first#(X1, X2))
(proper# cons(X1, X2) -> cons#(proper X1, proper X2), cons#(ok X1, ok X2) -> cons#(X1, X2))
(proper# cons(X1, X2) -> cons#(proper X1, proper X2), cons#(mark X1, X2) -> cons#(X1, X2))
(active# s X -> active# X, active# from X -> from# s X)
(active# s X -> active# X, active# from X -> from# active X)
(active# s X -> active# X, active# from X -> s# X)
(active# s X -> active# X, active# from X -> cons#(X, from s X))
(active# s X -> active# X, active# from X -> active# X)
(active# s X -> active# X, active# s X -> s# active X)
(active# s X -> active# X, active# s X -> active# X)
(active# s X -> active# X, active# cons(X1, X2) -> cons#(active X1, X2))
(active# s X -> active# X, active# cons(X1, X2) -> active# X1)
(active# s X -> active# X, active# first(s X, cons(Y, Z)) -> cons#(Y, first(X, Z)))
(active# s X -> active# X, active# first(s X, cons(Y, Z)) -> first#(X, Z))
(active# s X -> active# X, active# first(X1, X2) -> first#(active X1, X2))
(active# s X -> active# X, active# first(X1, X2) -> first#(X1, active X2))
(active# s X -> active# X, active# first(X1, X2) -> active# X2)
(active# s X -> active# X, active# first(X1, X2) -> active# X1)
(active# from X -> s# X, s# ok X -> s# X)
(active# from X -> s# X, s# mark X -> s# X)
(s# ok X -> s# X, s# ok X -> s# X)
(s# ok X -> s# X, s# mark X -> s# X)
(from# ok X -> from# X, from# ok X -> from# X)
(from# ok X -> from# X, from# mark X -> from# X)
(proper# cons(X1, X2) -> proper# X2, proper# from X -> proper# X)
(proper# cons(X1, X2) -> proper# X2, proper# from X -> from# proper X)
(proper# cons(X1, X2) -> proper# X2, proper# s X -> proper# X)
(proper# cons(X1, X2) -> proper# X2, proper# s X -> s# proper X)
(proper# cons(X1, X2) -> proper# X2, proper# cons(X1, X2) -> proper# X2)
(proper# cons(X1, X2) -> proper# X2, proper# cons(X1, X2) -> proper# X1)
(proper# cons(X1, X2) -> proper# X2, proper# cons(X1, X2) -> cons#(proper X1, proper X2))
(proper# cons(X1, X2) -> proper# X2, proper# first(X1, X2) -> proper# X2)
(proper# cons(X1, X2) -> proper# X2, proper# first(X1, X2) -> proper# X1)
(proper# cons(X1, X2) -> proper# X2, proper# first(X1, X2) -> first#(proper X1, proper X2))
(proper# from X -> proper# X, proper# from X -> proper# X)
(proper# from X -> proper# X, proper# from X -> from# proper X)
(proper# from X -> proper# X, proper# s X -> proper# X)
(proper# from X -> proper# X, proper# s X -> s# proper X)
(proper# from X -> proper# X, proper# cons(X1, X2) -> proper# X2)
(proper# from X -> proper# X, proper# cons(X1, X2) -> proper# X1)
(proper# from X -> proper# X, proper# cons(X1, X2) -> cons#(proper X1, proper X2))
(proper# from X -> proper# X, proper# first(X1, X2) -> proper# X2)
(proper# from X -> proper# X, proper# first(X1, X2) -> proper# X1)
(proper# from X -> proper# X, proper# first(X1, X2) -> first#(proper X1, proper X2))
(top# ok X -> active# X, active# from X -> from# s X)
(top# ok X -> active# X, active# from X -> from# active X)
(top# ok X -> active# X, active# from X -> s# X)
(top# ok X -> active# X, active# from X -> cons#(X, from s X))
(top# ok X -> active# X, active# from X -> active# X)
(top# ok X -> active# X, active# s X -> s# active X)
(top# ok X -> active# X, active# s X -> active# X)
(top# ok X -> active# X, active# cons(X1, X2) -> cons#(active X1, X2))
(top# ok X -> active# X, active# cons(X1, X2) -> active# X1)
(top# ok X -> active# X, active# first(s X, cons(Y, Z)) -> cons#(Y, first(X, Z)))
(top# ok X -> active# X, active# first(s X, cons(Y, Z)) -> first#(X, Z))
(top# ok X -> active# X, active# first(X1, X2) -> first#(active X1, X2))
(top# ok X -> active# X, active# first(X1, X2) -> first#(X1, active X2))
(top# ok X -> active# X, active# first(X1, X2) -> active# X2)
(top# ok X -> active# X, active# first(X1, X2) -> active# X1)
(active# from X -> cons#(X, from s X), cons#(ok X1, ok X2) -> cons#(X1, X2))
(active# from X -> cons#(X, from s X), cons#(mark X1, X2) -> cons#(X1, X2))
(active# cons(X1, X2) -> active# X1, active# from X -> from# s X)
(active# cons(X1, X2) -> active# X1, active# from X -> from# active X)
(active# cons(X1, X2) -> active# X1, active# from X -> s# X)
(active# cons(X1, X2) -> active# X1, active# from X -> cons#(X, from s X))
(active# cons(X1, X2) -> active# X1, active# from X -> active# X)
(active# cons(X1, X2) -> active# X1, active# s X -> s# active X)
(active# cons(X1, X2) -> active# X1, active# s X -> active# X)
(active# cons(X1, X2) -> active# X1, active# cons(X1, X2) -> cons#(active X1, X2))
(active# cons(X1, X2) -> active# X1, active# cons(X1, X2) -> active# X1)
(active# cons(X1, X2) -> active# X1, active# first(s X, cons(Y, Z)) -> cons#(Y, first(X, Z)))
(active# cons(X1, X2) -> active# X1, active# first(s X, cons(Y, Z)) -> first#(X, Z))
(active# cons(X1, X2) -> active# X1, active# first(X1, X2) -> first#(active X1, X2))
(active# cons(X1, X2) -> active# X1, active# first(X1, X2) -> first#(X1, active X2))
(active# cons(X1, X2) -> active# X1, active# first(X1, X2) -> active# X2)
(active# cons(X1, X2) -> active# X1, active# first(X1, X2) -> active# X1)
(proper# cons(X1, X2) -> proper# X1, proper# from X -> proper# X)
(proper# cons(X1, X2) -> proper# X1, proper# from X -> from# proper X)
(proper# cons(X1, X2) -> proper# X1, proper# s X -> proper# X)
(proper# cons(X1, X2) -> proper# X1, proper# s X -> s# proper X)
(proper# cons(X1, X2) -> proper# X1, proper# cons(X1, X2) -> proper# X2)
(proper# cons(X1, X2) -> proper# X1, proper# cons(X1, X2) -> proper# X1)
(proper# cons(X1, X2) -> proper# X1, proper# cons(X1, X2) -> cons#(proper X1, proper X2))
(proper# cons(X1, X2) -> proper# X1, proper# first(X1, X2) -> proper# X2)
(proper# cons(X1, X2) -> proper# X1, proper# first(X1, X2) -> proper# X1)
(proper# cons(X1, X2) -> proper# X1, proper# first(X1, X2) -> first#(proper X1, proper X2))
(proper# first(X1, X2) -> proper# X1, proper# first(X1, X2) -> first#(proper X1, proper X2))
(proper# first(X1, X2) -> proper# X1, proper# first(X1, X2) -> proper# X1)
(proper# first(X1, X2) -> proper# X1, proper# first(X1, X2) -> proper# X2)
(proper# first(X1, X2) -> proper# X1, proper# cons(X1, X2) -> cons#(proper X1, proper X2))
(proper# first(X1, X2) -> proper# X1, proper# cons(X1, X2) -> proper# X1)
(proper# first(X1, X2) -> proper# X1, proper# cons(X1, X2) -> proper# X2)
(proper# first(X1, X2) -> proper# X1, proper# s X -> s# proper X)
(proper# first(X1, X2) -> proper# X1, proper# s X -> proper# X)
(proper# first(X1, X2) -> proper# X1, proper# from X -> from# proper X)
(proper# first(X1, X2) -> proper# X1, proper# from X -> proper# X)
(active# first(X1, X2) -> active# X1, active# first(X1, X2) -> active# X1)
(active# first(X1, X2) -> active# X1, active# first(X1, X2) -> active# X2)
(active# first(X1, X2) -> active# X1, active# first(X1, X2) -> first#(X1, active X2))
(active# first(X1, X2) -> active# X1, active# first(X1, X2) -> first#(active X1, X2))
(active# first(X1, X2) -> active# X1, active# first(s X, cons(Y, Z)) -> first#(X, Z))
(active# first(X1, X2) -> active# X1, active# first(s X, cons(Y, Z)) -> cons#(Y, first(X, Z)))
(active# first(X1, X2) -> active# X1, active# cons(X1, X2) -> active# X1)
(active# first(X1, X2) -> active# X1, active# cons(X1, X2) -> cons#(active X1, X2))
(active# first(X1, X2) -> active# X1, active# s X -> active# X)
(active# first(X1, X2) -> active# X1, active# s X -> s# active X)
(active# first(X1, X2) -> active# X1, active# from X -> active# X)
(active# first(X1, X2) -> active# X1, active# from X -> cons#(X, from s X))
(active# first(X1, X2) -> active# X1, active# from X -> s# X)
(active# first(X1, X2) -> active# X1, active# from X -> from# active X)
(active# first(X1, X2) -> active# X1, active# from X -> from# s X)
(active# first(s X, cons(Y, Z)) -> cons#(Y, first(X, Z)), cons#(mark X1, X2) -> cons#(X1, X2))
(active# first(s X, cons(Y, Z)) -> cons#(Y, first(X, Z)), cons#(ok X1, ok X2) -> cons#(X1, X2))
(top# mark X -> proper# X, proper# first(X1, X2) -> first#(proper X1, proper X2))
(top# mark X -> proper# X, proper# first(X1, X2) -> proper# X1)
(top# mark X -> proper# X, proper# first(X1, X2) -> proper# X2)
(top# mark X -> proper# X, proper# cons(X1, X2) -> cons#(proper X1, proper X2))
(top# mark X -> proper# X, proper# cons(X1, X2) -> proper# X1)
(top# mark X -> proper# X, proper# cons(X1, X2) -> proper# X2)
(top# mark X -> proper# X, proper# s X -> s# proper X)
(top# mark X -> proper# X, proper# s X -> proper# X)
(top# mark X -> proper# X, proper# from X -> from# proper X)
(top# mark X -> proper# X, proper# from X -> proper# X)
(proper# s X -> proper# X, proper# first(X1, X2) -> first#(proper X1, proper X2))
(proper# s X -> proper# X, proper# first(X1, X2) -> proper# X1)
(proper# s X -> proper# X, proper# first(X1, X2) -> proper# X2)
(proper# s X -> proper# X, proper# cons(X1, X2) -> cons#(proper X1, proper X2))
(proper# s X -> proper# X, proper# cons(X1, X2) -> proper# X1)
(proper# s X -> proper# X, proper# cons(X1, X2) -> proper# X2)
(proper# s X -> proper# X, proper# s X -> s# proper X)
(proper# s X -> proper# X, proper# s X -> proper# X)
(proper# s X -> proper# X, proper# from X -> from# proper X)
(proper# s X -> proper# X, proper# from X -> proper# X)
(proper# first(X1, X2) -> proper# X2, proper# first(X1, X2) -> first#(proper X1, proper X2))
(proper# first(X1, X2) -> proper# X2, proper# first(X1, X2) -> proper# X1)
(proper# first(X1, X2) -> proper# X2, proper# first(X1, X2) -> proper# X2)
(proper# first(X1, X2) -> proper# X2, proper# cons(X1, X2) -> cons#(proper X1, proper X2))
(proper# first(X1, X2) -> proper# X2, proper# cons(X1, X2) -> proper# X1)
(proper# first(X1, X2) -> proper# X2, proper# cons(X1, X2) -> proper# X2)
(proper# first(X1, X2) -> proper# X2, proper# s X -> s# proper X)
(proper# first(X1, X2) -> proper# X2, proper# s X -> proper# X)
(proper# first(X1, X2) -> proper# X2, proper# from X -> from# proper X)
(proper# first(X1, X2) -> proper# X2, proper# from X -> proper# X)
(from# mark X -> from# X, from# mark X -> from# X)
(from# mark X -> from# X, from# ok X -> from# X)
(s# mark X -> s# X, s# mark X -> s# X)
(s# mark X -> s# X, s# ok X -> s# X)
(active# from X -> active# X, active# first(X1, X2) -> active# X1)
(active# from X -> active# X, active# first(X1, X2) -> active# X2)
(active# from X -> active# X, active# first(X1, X2) -> first#(X1, active X2))
(active# from X -> active# X, active# first(X1, X2) -> first#(active X1, X2))
(active# from X -> active# X, active# first(s X, cons(Y, Z)) -> first#(X, Z))
(active# from X -> active# X, active# first(s X, cons(Y, Z)) -> cons#(Y, first(X, Z)))
(active# from X -> active# X, active# cons(X1, X2) -> active# X1)
(active# from X -> active# X, active# cons(X1, X2) -> cons#(active X1, X2))
(active# from X -> active# X, active# s X -> active# X)
(active# from X -> active# X, active# s X -> s# active X)
(active# from X -> active# X, active# from X -> active# X)
(active# from X -> active# X, active# from X -> cons#(X, from s X))
(active# from X -> active# X, active# from X -> s# X)
(active# from X -> active# X, active# from X -> from# active X)
(active# from X -> active# X, active# from X -> from# s X)
(active# first(X1, X2) -> active# X2, active# first(X1, X2) -> active# X1)
(active# first(X1, X2) -> active# X2, active# first(X1, X2) -> active# X2)
(active# first(X1, X2) -> active# X2, active# first(X1, X2) -> first#(X1, active X2))
(active# first(X1, X2) -> active# X2, active# first(X1, X2) -> first#(active X1, X2))
(active# first(X1, X2) -> active# X2, active# first(s X, cons(Y, Z)) -> first#(X, Z))
(active# first(X1, X2) -> active# X2, active# first(s X, cons(Y, Z)) -> cons#(Y, first(X, Z)))
(active# first(X1, X2) -> active# X2, active# cons(X1, X2) -> active# X1)
(active# first(X1, X2) -> active# X2, active# cons(X1, X2) -> cons#(active X1, X2))
(active# first(X1, X2) -> active# X2, active# s X -> active# X)
(active# first(X1, X2) -> active# X2, active# s X -> s# active X)
(active# first(X1, X2) -> active# X2, active# from X -> active# X)
(active# first(X1, X2) -> active# X2, active# from X -> cons#(X, from s X))
(active# first(X1, X2) -> active# X2, active# from X -> s# X)
(active# first(X1, X2) -> active# X2, active# from X -> from# active X)
(active# first(X1, X2) -> active# X2, active# from X -> from# s X)
(proper# first(X1, X2) -> first#(proper X1, proper X2), first#(X1, mark X2) -> first#(X1, X2))
(proper# first(X1, X2) -> first#(proper X1, proper X2), first#(mark X1, X2) -> first#(X1, X2))
(proper# first(X1, X2) -> first#(proper X1, proper X2), first#(ok X1, ok X2) -> first#(X1, X2))
(cons#(ok X1, ok X2) -> cons#(X1, X2), cons#(mark X1, X2) -> cons#(X1, X2))
(cons#(ok X1, ok X2) -> cons#(X1, X2), cons#(ok X1, ok X2) -> cons#(X1, X2))
(first#(ok X1, ok X2) -> first#(X1, X2), first#(X1, mark X2) -> first#(X1, X2))
(first#(ok X1, ok X2) -> first#(X1, X2), first#(mark X1, X2) -> first#(X1, X2))
(first#(ok X1, ok X2) -> first#(X1, X2), first#(ok X1, ok X2) -> first#(X1, X2))
(first#(X1, mark X2) -> first#(X1, X2), first#(X1, mark X2) -> first#(X1, X2))
(first#(X1, mark X2) -> first#(X1, X2), first#(mark X1, X2) -> first#(X1, X2))
(first#(X1, mark X2) -> first#(X1, X2), first#(ok X1, ok X2) -> first#(X1, X2))
(active# first(X1, X2) -> first#(active X1, X2), first#(X1, mark X2) -> first#(X1, X2))
(active# first(X1, X2) -> first#(active X1, X2), first#(mark X1, X2) -> first#(X1, X2))
(active# first(X1, X2) -> first#(active X1, X2), first#(ok X1, ok X2) -> first#(X1, X2))
(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# s X -> s# proper X, s# mark X -> s# X)
(proper# s X -> s# proper X, s# ok X -> s# X)
(active# from X -> from# active X, from# mark X -> from# X)
(active# from X -> from# active X, from# ok X -> from# X)
(active# first(s X, cons(Y, Z)) -> first#(X, Z), first#(X1, mark X2) -> first#(X1, X2))
(active# first(s X, cons(Y, Z)) -> first#(X, Z), first#(mark X1, X2) -> first#(X1, X2))
(active# first(s X, cons(Y, Z)) -> first#(X, Z), first#(ok X1, ok X2) -> first#(X1, X2))
}
STATUS:
arrows: 0.846953
SCCS (7):
Scc:
{top# mark X -> top# proper X,
top# ok X -> top# active X}
Scc:
{active# first(X1, X2) -> active# X1,
active# first(X1, X2) -> active# X2,
active# cons(X1, X2) -> active# X1,
active# s X -> active# X,
active# from X -> active# X}
Scc:
{proper# first(X1, X2) -> proper# X1,
proper# first(X1, X2) -> proper# X2,
proper# cons(X1, X2) -> proper# X1,
proper# cons(X1, X2) -> proper# X2,
proper# s X -> proper# X,
proper# from X -> proper# X}
Scc:
{ cons#(mark X1, X2) -> cons#(X1, X2),
cons#(ok X1, ok X2) -> cons#(X1, X2)}
Scc:
{from# mark X -> from# X,
from# ok X -> from# X}
Scc:
{s# mark X -> s# X,
s# ok X -> s# X}
Scc:
{ first#(X1, mark X2) -> first#(X1, X2),
first#(mark X1, X2) -> first#(X1, X2),
first#(ok X1, ok X2) -> first#(X1, X2)}
SCC (2):
Strict:
{top# mark X -> top# proper X,
top# ok X -> top# active X}
Weak:
{ active first(X1, X2) -> first(X1, active X2),
active first(X1, X2) -> first(active X1, X2),
active first(0(), X) -> mark nil(),
active first(s X, cons(Y, Z)) -> mark cons(Y, first(X, Z)),
active cons(X1, X2) -> cons(active X1, X2),
active s X -> s active X,
active from X -> mark cons(X, from s X),
active from X -> from active X,
first(X1, mark X2) -> mark first(X1, X2),
first(mark X1, X2) -> mark first(X1, X2),
first(ok X1, ok X2) -> ok first(X1, X2),
cons(mark X1, X2) -> mark cons(X1, X2),
cons(ok X1, ok X2) -> ok cons(X1, X2),
s mark X -> mark s X,
s ok X -> ok s X,
from mark X -> mark from X,
from ok X -> ok from X,
proper nil() -> ok nil(),
proper first(X1, X2) -> first(proper X1, proper X2),
proper 0() -> ok 0(),
proper cons(X1, X2) -> cons(proper X1, proper X2),
proper s X -> s proper X,
proper from X -> from 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:
[first](x0, x1) = x0 + x1,
[cons](x0, x1) = x0,
[mark](x0) = x0 + 1,
[active](x0) = x0,
[s](x0) = x0 + 1,
[from](x0) = x0 + 1,
[proper](x0) = x0,
[ok](x0) = x0,
[top](x0) = 0,
[nil] = 0,
[0] = 1,
[top#](x0) = x0
Strict:
top# ok X -> top# active X
0 + 1X >= 0 + 1X
top# mark X -> top# proper 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 from X -> from proper X
1 + 1X >= 1 + 1X
proper s X -> s proper X
1 + 1X >= 1 + 1X
proper cons(X1, X2) -> cons(proper X1, proper X2)
0 + 1X1 + 0X2 >= 0 + 1X1 + 0X2
proper 0() -> ok 0()
1 >= 1
proper first(X1, X2) -> first(proper X1, proper X2)
0 + 1X1 + 1X2 >= 0 + 1X1 + 1X2
proper nil() -> ok nil()
0 >= 0
from ok X -> ok from X
1 + 1X >= 1 + 1X
from mark X -> mark from X
2 + 1X >= 2 + 1X
s ok X -> ok s X
1 + 1X >= 1 + 1X
s mark X -> mark s X
2 + 1X >= 2 + 1X
cons(ok X1, ok X2) -> ok cons(X1, X2)
0 + 1X1 + 0X2 >= 0 + 1X1 + 0X2
cons(mark X1, X2) -> mark cons(X1, X2)
1 + 1X1 + 0X2 >= 1 + 1X1 + 0X2
first(ok X1, ok X2) -> ok first(X1, X2)
0 + 1X1 + 1X2 >= 0 + 1X1 + 1X2
first(mark X1, X2) -> mark first(X1, X2)
1 + 1X1 + 1X2 >= 1 + 1X1 + 1X2
first(X1, mark X2) -> mark first(X1, X2)
1 + 1X1 + 1X2 >= 1 + 1X1 + 1X2
active from X -> from active X
1 + 1X >= 1 + 1X
active from X -> mark cons(X, from s X)
1 + 1X >= 1 + 1X
active s X -> s active X
1 + 1X >= 1 + 1X
active cons(X1, X2) -> cons(active X1, X2)
0 + 1X1 + 0X2 >= 0 + 1X1 + 0X2
active first(s X, cons(Y, Z)) -> mark cons(Y, first(X, Z))
1 + 1X + 1Y + 0Z >= 1 + 0X + 1Y + 0Z
active first(0(), X) -> mark nil()
1 + 1X >= 1
active first(X1, X2) -> first(active X1, X2)
0 + 1X1 + 1X2 >= 0 + 1X1 + 1X2
active first(X1, X2) -> first(X1, active X2)
0 + 1X1 + 1X2 >= 0 + 1X1 + 1X2
SCCS (1):
Scc:
{top# ok X -> top# active X}
SCC (1):
Strict:
{top# ok X -> top# active X}
Weak:
{ active first(X1, X2) -> first(X1, active X2),
active first(X1, X2) -> first(active X1, X2),
active first(0(), X) -> mark nil(),
active first(s X, cons(Y, Z)) -> mark cons(Y, first(X, Z)),
active cons(X1, X2) -> cons(active X1, X2),
active s X -> s active X,
active from X -> mark cons(X, from s X),
active from X -> from active X,
first(X1, mark X2) -> mark first(X1, X2),
first(mark X1, X2) -> mark first(X1, X2),
first(ok X1, ok X2) -> ok first(X1, X2),
cons(mark X1, X2) -> mark cons(X1, X2),
cons(ok X1, ok X2) -> ok cons(X1, X2),
s mark X -> mark s X,
s ok X -> ok s X,
from mark X -> mark from X,
from ok X -> ok from X,
proper nil() -> ok nil(),
proper first(X1, X2) -> first(proper X1, proper X2),
proper 0() -> ok 0(),
proper cons(X1, X2) -> cons(proper X1, proper X2),
proper s X -> s proper X,
proper from X -> from 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:
[first](x0, x1) = x0 + 1,
[cons](x0, x1) = x0 + x1 + 1,
[mark](x0) = 0,
[active](x0) = x0,
[s](x0) = x0 + 1,
[from](x0) = x0,
[proper](x0) = x0 + 1,
[ok](x0) = x0 + 1,
[top](x0) = 0,
[nil] = 1,
[0] = 0,
[top#](x0) = x0
Strict:
top# ok X -> top# active 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 from X -> from proper X
1 + 1X >= 1 + 1X
proper s X -> s proper X
2 + 1X >= 2 + 1X
proper cons(X1, X2) -> cons(proper X1, proper X2)
2 + 1X1 + 1X2 >= 3 + 1X1 + 1X2
proper 0() -> ok 0()
1 >= 1
proper first(X1, X2) -> first(proper X1, proper X2)
2 + 1X1 + 0X2 >= 2 + 1X1 + 0X2
proper nil() -> ok nil()
2 >= 2
from ok X -> ok from X
1 + 1X >= 1 + 1X
from mark X -> mark from X
0 + 0X >= 0 + 0X
s ok X -> ok s X
2 + 1X >= 2 + 1X
s mark X -> mark s X
1 + 0X >= 0 + 0X
cons(ok X1, ok X2) -> ok cons(X1, X2)
3 + 1X1 + 1X2 >= 2 + 1X1 + 1X2
cons(mark X1, X2) -> mark cons(X1, X2)
1 + 0X1 + 1X2 >= 0 + 0X1 + 0X2
first(ok X1, ok X2) -> ok first(X1, X2)
2 + 1X1 + 0X2 >= 2 + 1X1 + 0X2
first(mark X1, X2) -> mark first(X1, X2)
1 + 0X1 + 0X2 >= 0 + 0X1 + 0X2
first(X1, mark X2) -> mark first(X1, X2)
1 + 1X1 + 0X2 >= 0 + 0X1 + 0X2
active from X -> from active X
0 + 1X >= 0 + 1X
active from X -> mark cons(X, from s X)
0 + 1X >= 0 + 0X
active s X -> s active X
1 + 1X >= 1 + 1X
active cons(X1, X2) -> cons(active X1, X2)
1 + 1X1 + 1X2 >= 1 + 1X1 + 1X2
active first(s X, cons(Y, Z)) -> mark cons(Y, first(X, Z))
2 + 1X + 0Y + 0Z >= 0 + 0X + 0Y + 0Z
active first(0(), X) -> mark nil()
1 + 0X >= 0
active first(X1, X2) -> first(active X1, X2)
1 + 1X1 + 0X2 >= 1 + 1X1 + 0X2
active first(X1, X2) -> first(X1, active X2)
1 + 1X1 + 0X2 >= 1 + 1X1 + 0X2
Qed
SCC (5):
Strict:
{active# first(X1, X2) -> active# X1,
active# first(X1, X2) -> active# X2,
active# cons(X1, X2) -> active# X1,
active# s X -> active# X,
active# from X -> active# X}
Weak:
{ active first(X1, X2) -> first(X1, active X2),
active first(X1, X2) -> first(active X1, X2),
active first(0(), X) -> mark nil(),
active first(s X, cons(Y, Z)) -> mark cons(Y, first(X, Z)),
active cons(X1, X2) -> cons(active X1, X2),
active s X -> s active X,
active from X -> mark cons(X, from s X),
active from X -> from active X,
first(X1, mark X2) -> mark first(X1, X2),
first(mark X1, X2) -> mark first(X1, X2),
first(ok X1, ok X2) -> ok first(X1, X2),
cons(mark X1, X2) -> mark cons(X1, X2),
cons(ok X1, ok X2) -> ok cons(X1, X2),
s mark X -> mark s X,
s ok X -> ok s X,
from mark X -> mark from X,
from ok X -> ok from X,
proper nil() -> ok nil(),
proper first(X1, X2) -> first(proper X1, proper X2),
proper 0() -> ok 0(),
proper cons(X1, X2) -> cons(proper X1, proper X2),
proper s X -> s proper X,
proper from X -> from 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:
[first](x0, x1) = x0 + x1,
[cons](x0, x1) = x0,
[mark](x0) = x0 + 1,
[active](x0) = 0,
[s](x0) = x0,
[from](x0) = x0 + 1,
[proper](x0) = 0,
[ok](x0) = x0 + 1,
[top](x0) = 0,
[nil] = 1,
[0] = 0,
[active#](x0) = x0
Strict:
active# from X -> active# X
1 + 1X >= 0 + 1X
active# s X -> active# X
0 + 1X >= 0 + 1X
active# cons(X1, X2) -> active# X1
0 + 1X1 + 0X2 >= 0 + 1X1
active# first(X1, X2) -> active# X2
0 + 1X1 + 1X2 >= 0 + 1X2
active# first(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 from X -> from proper X
0 + 0X >= 1 + 0X
proper s X -> s proper X
0 + 0X >= 0 + 0X
proper cons(X1, X2) -> cons(proper X1, proper X2)
0 + 0X1 + 0X2 >= 0 + 0X1 + 0X2
proper 0() -> ok 0()
0 >= 1
proper first(X1, X2) -> first(proper X1, proper X2)
0 + 0X1 + 0X2 >= 0 + 0X1 + 0X2
proper nil() -> ok nil()
0 >= 2
from ok X -> ok from X
2 + 1X >= 2 + 1X
from mark X -> mark from X
2 + 1X >= 2 + 1X
s ok X -> ok s X
1 + 1X >= 1 + 1X
s mark X -> mark s X
1 + 1X >= 1 + 1X
cons(ok X1, ok X2) -> ok cons(X1, X2)
1 + 1X1 + 0X2 >= 1 + 1X1 + 0X2
cons(mark X1, X2) -> mark cons(X1, X2)
1 + 1X1 + 0X2 >= 1 + 1X1 + 0X2
first(ok X1, ok X2) -> ok first(X1, X2)
2 + 1X1 + 1X2 >= 1 + 1X1 + 1X2
first(mark X1, X2) -> mark first(X1, X2)
1 + 1X1 + 1X2 >= 1 + 1X1 + 1X2
first(X1, mark X2) -> mark first(X1, X2)
1 + 1X1 + 1X2 >= 1 + 1X1 + 1X2
active from X -> from active X
0 + 0X >= 1 + 0X
active from X -> mark cons(X, from s X)
0 + 0X >= 1 + 1X
active s X -> s active X
0 + 0X >= 0 + 0X
active cons(X1, X2) -> cons(active X1, X2)
0 + 0X1 + 0X2 >= 0 + 0X1 + 0X2
active first(s X, cons(Y, Z)) -> mark cons(Y, first(X, Z))
0 + 0X + 0Y + 0Z >= 1 + 0X + 1Y + 0Z
active first(0(), X) -> mark nil()
0 + 0X >= 2
active first(X1, X2) -> first(active X1, X2)
0 + 0X1 + 0X2 >= 0 + 0X1 + 1X2
active first(X1, X2) -> first(X1, active X2)
0 + 0X1 + 0X2 >= 0 + 1X1 + 0X2
SCCS (1):
Scc:
{active# first(X1, X2) -> active# X1,
active# first(X1, X2) -> active# X2,
active# cons(X1, X2) -> active# X1,
active# s X -> active# X}
SCC (4):
Strict:
{active# first(X1, X2) -> active# X1,
active# first(X1, X2) -> active# X2,
active# cons(X1, X2) -> active# X1,
active# s X -> active# X}
Weak:
{ active first(X1, X2) -> first(X1, active X2),
active first(X1, X2) -> first(active X1, X2),
active first(0(), X) -> mark nil(),
active first(s X, cons(Y, Z)) -> mark cons(Y, first(X, Z)),
active cons(X1, X2) -> cons(active X1, X2),
active s X -> s active X,
active from X -> mark cons(X, from s X),
active from X -> from active X,
first(X1, mark X2) -> mark first(X1, X2),
first(mark X1, X2) -> mark first(X1, X2),
first(ok X1, ok X2) -> ok first(X1, X2),
cons(mark X1, X2) -> mark cons(X1, X2),
cons(ok X1, ok X2) -> ok cons(X1, X2),
s mark X -> mark s X,
s ok X -> ok s X,
from mark X -> mark from X,
from ok X -> ok from X,
proper nil() -> ok nil(),
proper first(X1, X2) -> first(proper X1, proper X2),
proper 0() -> ok 0(),
proper cons(X1, X2) -> cons(proper X1, proper X2),
proper s X -> s proper X,
proper from X -> from 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:
[first](x0, x1) = x0 + x1,
[cons](x0, x1) = x0,
[mark](x0) = 0,
[active](x0) = 0,
[s](x0) = x0 + 1,
[from](x0) = x0 + 1,
[proper](x0) = 0,
[ok](x0) = x0 + 1,
[top](x0) = 0,
[nil] = 0,
[0] = 0,
[active#](x0) = x0
Strict:
active# s X -> active# X
1 + 1X >= 0 + 1X
active# cons(X1, X2) -> active# X1
0 + 1X1 + 0X2 >= 0 + 1X1
active# first(X1, X2) -> active# X2
0 + 1X1 + 1X2 >= 0 + 1X2
active# first(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 from X -> from proper X
0 + 0X >= 1 + 0X
proper s X -> s proper X
0 + 0X >= 1 + 0X
proper cons(X1, X2) -> cons(proper X1, proper X2)
0 + 0X1 + 0X2 >= 0 + 0X1 + 0X2
proper 0() -> ok 0()
0 >= 1
proper first(X1, X2) -> first(proper X1, proper X2)
0 + 0X1 + 0X2 >= 0 + 0X1 + 0X2
proper nil() -> ok nil()
0 >= 1
from ok X -> ok from X
2 + 1X >= 2 + 1X
from mark X -> mark from X
1 + 0X >= 0 + 0X
s ok X -> ok s X
2 + 1X >= 2 + 1X
s mark X -> mark s X
1 + 0X >= 0 + 0X
cons(ok X1, ok X2) -> ok cons(X1, X2)
1 + 1X1 + 0X2 >= 1 + 1X1 + 0X2
cons(mark X1, X2) -> mark cons(X1, X2)
0 + 0X1 + 0X2 >= 0 + 0X1 + 0X2
first(ok X1, ok X2) -> ok first(X1, X2)
2 + 1X1 + 1X2 >= 1 + 1X1 + 1X2
first(mark X1, X2) -> mark first(X1, X2)
0 + 0X1 + 1X2 >= 0 + 0X1 + 0X2
first(X1, mark X2) -> mark first(X1, X2)
0 + 1X1 + 0X2 >= 0 + 0X1 + 0X2
active from X -> from active X
0 + 0X >= 1 + 0X
active from X -> mark cons(X, from s X)
0 + 0X >= 0 + 0X
active s X -> s active X
0 + 0X >= 1 + 0X
active cons(X1, X2) -> cons(active X1, X2)
0 + 0X1 + 0X2 >= 0 + 0X1 + 0X2
active first(s X, cons(Y, Z)) -> mark cons(Y, first(X, Z))
0 + 0X + 0Y + 0Z >= 0 + 0X + 0Y + 0Z
active first(0(), X) -> mark nil()
0 + 0X >= 0
active first(X1, X2) -> first(active X1, X2)
0 + 0X1 + 0X2 >= 0 + 0X1 + 1X2
active first(X1, X2) -> first(X1, active X2)
0 + 0X1 + 0X2 >= 0 + 1X1 + 0X2
SCCS (1):
Scc:
{active# first(X1, X2) -> active# X1,
active# first(X1, X2) -> active# X2,
active# cons(X1, X2) -> active# X1}
SCC (3):
Strict:
{active# first(X1, X2) -> active# X1,
active# first(X1, X2) -> active# X2,
active# cons(X1, X2) -> active# X1}
Weak:
{ active first(X1, X2) -> first(X1, active X2),
active first(X1, X2) -> first(active X1, X2),
active first(0(), X) -> mark nil(),
active first(s X, cons(Y, Z)) -> mark cons(Y, first(X, Z)),
active cons(X1, X2) -> cons(active X1, X2),
active s X -> s active X,
active from X -> mark cons(X, from s X),
active from X -> from active X,
first(X1, mark X2) -> mark first(X1, X2),
first(mark X1, X2) -> mark first(X1, X2),
first(ok X1, ok X2) -> ok first(X1, X2),
cons(mark X1, X2) -> mark cons(X1, X2),
cons(ok X1, ok X2) -> ok cons(X1, X2),
s mark X -> mark s X,
s ok X -> ok s X,
from mark X -> mark from X,
from ok X -> ok from X,
proper nil() -> ok nil(),
proper first(X1, X2) -> first(proper X1, proper X2),
proper 0() -> ok 0(),
proper cons(X1, X2) -> cons(proper X1, proper X2),
proper s X -> s proper X,
proper from X -> from 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:
[first](x0, x1) = x0 + x1,
[cons](x0, x1) = x0 + 1,
[mark](x0) = x0 + 1,
[active](x0) = 0,
[s](x0) = 1,
[from](x0) = x0 + 1,
[proper](x0) = 0,
[ok](x0) = x0 + 1,
[top](x0) = 0,
[nil] = 1,
[0] = 0,
[active#](x0) = x0
Strict:
active# cons(X1, X2) -> active# X1
1 + 1X1 + 0X2 >= 0 + 1X1
active# first(X1, X2) -> active# X2
0 + 1X1 + 1X2 >= 0 + 1X2
active# first(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 from X -> from proper X
0 + 0X >= 1 + 0X
proper s X -> s proper X
0 + 0X >= 1 + 0X
proper cons(X1, X2) -> cons(proper X1, proper X2)
0 + 0X1 + 0X2 >= 1 + 0X1 + 0X2
proper 0() -> ok 0()
0 >= 1
proper first(X1, X2) -> first(proper X1, proper X2)
0 + 0X1 + 0X2 >= 0 + 0X1 + 0X2
proper nil() -> ok nil()
0 >= 2
from ok X -> ok from X
2 + 1X >= 2 + 1X
from mark X -> mark from X
2 + 1X >= 2 + 1X
s ok X -> ok s X
1 + 0X >= 2 + 0X
s mark X -> mark s X
1 + 0X >= 2 + 0X
cons(ok X1, ok X2) -> ok cons(X1, X2)
2 + 1X1 + 0X2 >= 2 + 1X1 + 0X2
cons(mark X1, X2) -> mark cons(X1, X2)
2 + 1X1 + 0X2 >= 2 + 1X1 + 0X2
first(ok X1, ok X2) -> ok first(X1, X2)
2 + 1X1 + 1X2 >= 1 + 1X1 + 1X2
first(mark X1, X2) -> mark first(X1, X2)
1 + 1X1 + 1X2 >= 1 + 1X1 + 1X2
first(X1, mark X2) -> mark first(X1, X2)
1 + 1X1 + 1X2 >= 1 + 1X1 + 1X2
active from X -> from active X
0 + 0X >= 1 + 0X
active from X -> mark cons(X, from s X)
0 + 0X >= 2 + 1X
active s X -> s active X
0 + 0X >= 1 + 0X
active cons(X1, X2) -> cons(active X1, X2)
0 + 0X1 + 0X2 >= 1 + 0X1 + 0X2
active first(s X, cons(Y, Z)) -> mark cons(Y, first(X, Z))
0 + 0X + 0Y + 0Z >= 2 + 0X + 1Y + 0Z
active first(0(), X) -> mark nil()
0 + 0X >= 2
active first(X1, X2) -> first(active X1, X2)
0 + 0X1 + 0X2 >= 0 + 0X1 + 1X2
active first(X1, X2) -> first(X1, active X2)
0 + 0X1 + 0X2 >= 0 + 1X1 + 0X2
SCCS (1):
Scc:
{active# first(X1, X2) -> active# X1,
active# first(X1, X2) -> active# X2}
SCC (2):
Strict:
{active# first(X1, X2) -> active# X1,
active# first(X1, X2) -> active# X2}
Weak:
{ active first(X1, X2) -> first(X1, active X2),
active first(X1, X2) -> first(active X1, X2),
active first(0(), X) -> mark nil(),
active first(s X, cons(Y, Z)) -> mark cons(Y, first(X, Z)),
active cons(X1, X2) -> cons(active X1, X2),
active s X -> s active X,
active from X -> mark cons(X, from s X),
active from X -> from active X,
first(X1, mark X2) -> mark first(X1, X2),
first(mark X1, X2) -> mark first(X1, X2),
first(ok X1, ok X2) -> ok first(X1, X2),
cons(mark X1, X2) -> mark cons(X1, X2),
cons(ok X1, ok X2) -> ok cons(X1, X2),
s mark X -> mark s X,
s ok X -> ok s X,
from mark X -> mark from X,
from ok X -> ok from X,
proper nil() -> ok nil(),
proper first(X1, X2) -> first(proper X1, proper X2),
proper 0() -> ok 0(),
proper cons(X1, X2) -> cons(proper X1, proper X2),
proper s X -> s proper X,
proper from X -> from 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:
[first](x0, x1) = x0 + x1 + 1,
[cons](x0, x1) = 0,
[mark](x0) = x0 + 1,
[active](x0) = 0,
[s](x0) = 1,
[from](x0) = x0,
[proper](x0) = x0 + 1,
[ok](x0) = 0,
[top](x0) = x0,
[nil] = 1,
[0] = 0,
[active#](x0) = x0 + 1
Strict:
active# first(X1, X2) -> active# X2
2 + 1X1 + 1X2 >= 1 + 1X2
active# first(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
1 + 1X >= 1 + 1X
proper from X -> from proper X
1 + 1X >= 1 + 1X
proper s X -> s proper X
2 + 0X >= 1 + 0X
proper cons(X1, X2) -> cons(proper X1, proper X2)
1 + 0X1 + 0X2 >= 0 + 0X1 + 0X2
proper 0() -> ok 0()
1 >= 0
proper first(X1, X2) -> first(proper X1, proper X2)
2 + 1X1 + 1X2 >= 3 + 1X1 + 1X2
proper nil() -> ok nil()
2 >= 0
from ok X -> ok from X
0 + 0X >= 0 + 0X
from mark X -> mark from X
1 + 1X >= 1 + 1X
s ok X -> ok s X
1 + 0X >= 0 + 0X
s mark X -> mark s X
1 + 0X >= 2 + 0X
cons(ok X1, ok X2) -> ok cons(X1, X2)
0 + 0X1 + 0X2 >= 0 + 0X1 + 0X2
cons(mark X1, X2) -> mark cons(X1, X2)
0 + 0X1 + 0X2 >= 1 + 0X1 + 0X2
first(ok X1, ok X2) -> ok first(X1, X2)
1 + 0X1 + 0X2 >= 0 + 0X1 + 0X2
first(mark X1, X2) -> mark first(X1, X2)
2 + 1X1 + 1X2 >= 2 + 1X1 + 1X2
first(X1, mark X2) -> mark first(X1, X2)
2 + 1X1 + 1X2 >= 2 + 1X1 + 1X2
active from X -> from active X
0 + 0X >= 0 + 0X
active from X -> mark cons(X, from s X)
0 + 0X >= 1 + 0X
active s X -> s active X
0 + 0X >= 1 + 0X
active cons(X1, X2) -> cons(active X1, X2)
0 + 0X1 + 0X2 >= 0 + 0X1 + 0X2
active first(s X, cons(Y, Z)) -> mark cons(Y, first(X, Z))
0 + 0X + 0Y + 0Z >= 1 + 0X + 0Y + 0Z
active first(0(), X) -> mark nil()
0 + 0X >= 2
active first(X1, X2) -> first(active X1, X2)
0 + 0X1 + 0X2 >= 1 + 0X1 + 1X2
active first(X1, X2) -> first(X1, active X2)
0 + 0X1 + 0X2 >= 1 + 1X1 + 0X2
Qed
SCC (6):
Strict:
{proper# first(X1, X2) -> proper# X1,
proper# first(X1, X2) -> proper# X2,
proper# cons(X1, X2) -> proper# X1,
proper# cons(X1, X2) -> proper# X2,
proper# s X -> proper# X,
proper# from X -> proper# X}
Weak:
{ active first(X1, X2) -> first(X1, active X2),
active first(X1, X2) -> first(active X1, X2),
active first(0(), X) -> mark nil(),
active first(s X, cons(Y, Z)) -> mark cons(Y, first(X, Z)),
active cons(X1, X2) -> cons(active X1, X2),
active s X -> s active X,
active from X -> mark cons(X, from s X),
active from X -> from active X,
first(X1, mark X2) -> mark first(X1, X2),
first(mark X1, X2) -> mark first(X1, X2),
first(ok X1, ok X2) -> ok first(X1, X2),
cons(mark X1, X2) -> mark cons(X1, X2),
cons(ok X1, ok X2) -> ok cons(X1, X2),
s mark X -> mark s X,
s ok X -> ok s X,
from mark X -> mark from X,
from ok X -> ok from X,
proper nil() -> ok nil(),
proper first(X1, X2) -> first(proper X1, proper X2),
proper 0() -> ok 0(),
proper cons(X1, X2) -> cons(proper X1, proper X2),
proper s X -> s proper X,
proper from X -> from 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:
[first](x0, x1) = x0 + x1,
[cons](x0, x1) = x0 + x1,
[mark](x0) = x0 + 1,
[active](x0) = 0,
[s](x0) = x0,
[from](x0) = x0 + 1,
[proper](x0) = 0,
[ok](x0) = x0 + 1,
[top](x0) = 0,
[nil] = 1,
[0] = 0,
[proper#](x0) = x0
Strict:
proper# from X -> proper# X
1 + 1X >= 0 + 1X
proper# s X -> proper# X
0 + 1X >= 0 + 1X
proper# cons(X1, X2) -> proper# X2
0 + 1X1 + 1X2 >= 0 + 1X2
proper# cons(X1, X2) -> proper# X1
0 + 1X1 + 1X2 >= 0 + 1X1
proper# first(X1, X2) -> proper# X2
0 + 1X1 + 1X2 >= 0 + 1X2
proper# first(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 from X -> from proper X
0 + 0X >= 1 + 0X
proper s X -> s proper X
0 + 0X >= 0 + 0X
proper cons(X1, X2) -> cons(proper X1, proper X2)
0 + 0X1 + 0X2 >= 0 + 0X1 + 0X2
proper 0() -> ok 0()
0 >= 1
proper first(X1, X2) -> first(proper X1, proper X2)
0 + 0X1 + 0X2 >= 0 + 0X1 + 0X2
proper nil() -> ok nil()
0 >= 2
from ok X -> ok from X
2 + 1X >= 2 + 1X
from mark X -> mark from X
2 + 1X >= 2 + 1X
s ok X -> ok s X
1 + 1X >= 1 + 1X
s mark X -> mark s X
1 + 1X >= 1 + 1X
cons(ok X1, ok X2) -> ok cons(X1, X2)
2 + 1X1 + 1X2 >= 1 + 1X1 + 1X2
cons(mark X1, X2) -> mark cons(X1, X2)
1 + 1X1 + 1X2 >= 1 + 1X1 + 1X2
first(ok X1, ok X2) -> ok first(X1, X2)
2 + 1X1 + 1X2 >= 1 + 1X1 + 1X2
first(mark X1, X2) -> mark first(X1, X2)
1 + 1X1 + 1X2 >= 1 + 1X1 + 1X2
first(X1, mark X2) -> mark first(X1, X2)
1 + 1X1 + 1X2 >= 1 + 1X1 + 1X2
active from X -> from active X
0 + 0X >= 1 + 0X
active from X -> mark cons(X, from s X)
0 + 0X >= 2 + 2X
active s X -> s active X
0 + 0X >= 0 + 0X
active cons(X1, X2) -> cons(active X1, X2)
0 + 0X1 + 0X2 >= 0 + 0X1 + 1X2
active first(s X, cons(Y, Z)) -> mark cons(Y, first(X, Z))
0 + 0X + 0Y + 0Z >= 1 + 1X + 1Y + 1Z
active first(0(), X) -> mark nil()
0 + 0X >= 2
active first(X1, X2) -> first(active X1, X2)
0 + 0X1 + 0X2 >= 0 + 0X1 + 1X2
active first(X1, X2) -> first(X1, active X2)
0 + 0X1 + 0X2 >= 0 + 1X1 + 0X2
SCCS (1):
Scc:
{proper# first(X1, X2) -> proper# X1,
proper# first(X1, X2) -> proper# X2,
proper# cons(X1, X2) -> proper# X1,
proper# cons(X1, X2) -> proper# X2,
proper# s X -> proper# X}
SCC (5):
Strict:
{proper# first(X1, X2) -> proper# X1,
proper# first(X1, X2) -> proper# X2,
proper# cons(X1, X2) -> proper# X1,
proper# cons(X1, X2) -> proper# X2,
proper# s X -> proper# X}
Weak:
{ active first(X1, X2) -> first(X1, active X2),
active first(X1, X2) -> first(active X1, X2),
active first(0(), X) -> mark nil(),
active first(s X, cons(Y, Z)) -> mark cons(Y, first(X, Z)),
active cons(X1, X2) -> cons(active X1, X2),
active s X -> s active X,
active from X -> mark cons(X, from s X),
active from X -> from active X,
first(X1, mark X2) -> mark first(X1, X2),
first(mark X1, X2) -> mark first(X1, X2),
first(ok X1, ok X2) -> ok first(X1, X2),
cons(mark X1, X2) -> mark cons(X1, X2),
cons(ok X1, ok X2) -> ok cons(X1, X2),
s mark X -> mark s X,
s ok X -> ok s X,
from mark X -> mark from X,
from ok X -> ok from X,
proper nil() -> ok nil(),
proper first(X1, X2) -> first(proper X1, proper X2),
proper 0() -> ok 0(),
proper cons(X1, X2) -> cons(proper X1, proper X2),
proper s X -> s proper X,
proper from X -> from 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:
[first](x0, x1) = x0 + x1,
[cons](x0, x1) = x0 + x1,
[mark](x0) = 0,
[active](x0) = 0,
[s](x0) = x0 + 1,
[from](x0) = x0 + 1,
[proper](x0) = 0,
[ok](x0) = x0 + 1,
[top](x0) = 0,
[nil] = 0,
[0] = 0,
[proper#](x0) = x0
Strict:
proper# s X -> proper# X
1 + 1X >= 0 + 1X
proper# cons(X1, X2) -> proper# X2
0 + 1X1 + 1X2 >= 0 + 1X2
proper# cons(X1, X2) -> proper# X1
0 + 1X1 + 1X2 >= 0 + 1X1
proper# first(X1, X2) -> proper# X2
0 + 1X1 + 1X2 >= 0 + 1X2
proper# first(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 from X -> from proper X
0 + 0X >= 1 + 0X
proper s X -> s proper X
0 + 0X >= 1 + 0X
proper cons(X1, X2) -> cons(proper X1, proper X2)
0 + 0X1 + 0X2 >= 0 + 0X1 + 0X2
proper 0() -> ok 0()
0 >= 1
proper first(X1, X2) -> first(proper X1, proper X2)
0 + 0X1 + 0X2 >= 0 + 0X1 + 0X2
proper nil() -> ok nil()
0 >= 1
from ok X -> ok from X
2 + 1X >= 2 + 1X
from mark X -> mark from X
1 + 0X >= 0 + 0X
s ok X -> ok s X
2 + 1X >= 2 + 1X
s mark X -> mark s X
1 + 0X >= 0 + 0X
cons(ok X1, ok X2) -> ok cons(X1, X2)
2 + 1X1 + 1X2 >= 1 + 1X1 + 1X2
cons(mark X1, X2) -> mark cons(X1, X2)
0 + 0X1 + 1X2 >= 0 + 0X1 + 0X2
first(ok X1, ok X2) -> ok first(X1, X2)
2 + 1X1 + 1X2 >= 1 + 1X1 + 1X2
first(mark X1, X2) -> mark first(X1, X2)
0 + 0X1 + 1X2 >= 0 + 0X1 + 0X2
first(X1, mark X2) -> mark first(X1, X2)
0 + 1X1 + 0X2 >= 0 + 0X1 + 0X2
active from X -> from active X
0 + 0X >= 1 + 0X
active from X -> mark cons(X, from s X)
0 + 0X >= 0 + 0X
active s X -> s active X
0 + 0X >= 1 + 0X
active cons(X1, X2) -> cons(active X1, X2)
0 + 0X1 + 0X2 >= 0 + 0X1 + 1X2
active first(s X, cons(Y, Z)) -> mark cons(Y, first(X, Z))
0 + 0X + 0Y + 0Z >= 0 + 0X + 0Y + 0Z
active first(0(), X) -> mark nil()
0 + 0X >= 0
active first(X1, X2) -> first(active X1, X2)
0 + 0X1 + 0X2 >= 0 + 0X1 + 1X2
active first(X1, X2) -> first(X1, active X2)
0 + 0X1 + 0X2 >= 0 + 1X1 + 0X2
SCCS (1):
Scc:
{proper# first(X1, X2) -> proper# X1,
proper# first(X1, X2) -> proper# X2,
proper# cons(X1, X2) -> proper# X1,
proper# cons(X1, X2) -> proper# X2}
SCC (4):
Strict:
{proper# first(X1, X2) -> proper# X1,
proper# first(X1, X2) -> proper# X2,
proper# cons(X1, X2) -> proper# X1,
proper# cons(X1, X2) -> proper# X2}
Weak:
{ active first(X1, X2) -> first(X1, active X2),
active first(X1, X2) -> first(active X1, X2),
active first(0(), X) -> mark nil(),
active first(s X, cons(Y, Z)) -> mark cons(Y, first(X, Z)),
active cons(X1, X2) -> cons(active X1, X2),
active s X -> s active X,
active from X -> mark cons(X, from s X),
active from X -> from active X,
first(X1, mark X2) -> mark first(X1, X2),
first(mark X1, X2) -> mark first(X1, X2),
first(ok X1, ok X2) -> ok first(X1, X2),
cons(mark X1, X2) -> mark cons(X1, X2),
cons(ok X1, ok X2) -> ok cons(X1, X2),
s mark X -> mark s X,
s ok X -> ok s X,
from mark X -> mark from X,
from ok X -> ok from X,
proper nil() -> ok nil(),
proper first(X1, X2) -> first(proper X1, proper X2),
proper 0() -> ok 0(),
proper cons(X1, X2) -> cons(proper X1, proper X2),
proper s X -> s proper X,
proper from X -> from 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:
[first](x0, x1) = x0 + x1,
[cons](x0, x1) = x0 + x1 + 1,
[mark](x0) = x0 + 1,
[active](x0) = 0,
[s](x0) = 1,
[from](x0) = 0,
[proper](x0) = 0,
[ok](x0) = x0 + 1,
[top](x0) = 0,
[nil] = 1,
[0] = 0,
[proper#](x0) = x0
Strict:
proper# cons(X1, X2) -> proper# X2
1 + 1X1 + 1X2 >= 0 + 1X2
proper# cons(X1, X2) -> proper# X1
1 + 1X1 + 1X2 >= 0 + 1X1
proper# first(X1, X2) -> proper# X2
0 + 1X1 + 1X2 >= 0 + 1X2
proper# first(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 from X -> from proper X
0 + 0X >= 0 + 0X
proper s X -> s proper X
0 + 0X >= 1 + 0X
proper cons(X1, X2) -> cons(proper X1, proper X2)
0 + 0X1 + 0X2 >= 1 + 0X1 + 0X2
proper 0() -> ok 0()
0 >= 1
proper first(X1, X2) -> first(proper X1, proper X2)
0 + 0X1 + 0X2 >= 0 + 0X1 + 0X2
proper nil() -> ok nil()
0 >= 2
from ok X -> ok from X
0 + 0X >= 1 + 0X
from mark X -> mark from X
0 + 0X >= 1 + 0X
s ok X -> ok s X
1 + 0X >= 2 + 0X
s mark X -> mark s X
1 + 0X >= 2 + 0X
cons(ok X1, ok X2) -> ok cons(X1, X2)
3 + 1X1 + 1X2 >= 2 + 1X1 + 1X2
cons(mark X1, X2) -> mark cons(X1, X2)
2 + 1X1 + 1X2 >= 2 + 1X1 + 1X2
first(ok X1, ok X2) -> ok first(X1, X2)
2 + 1X1 + 1X2 >= 1 + 1X1 + 1X2
first(mark X1, X2) -> mark first(X1, X2)
1 + 1X1 + 1X2 >= 1 + 1X1 + 1X2
first(X1, mark X2) -> mark first(X1, X2)
1 + 1X1 + 1X2 >= 1 + 1X1 + 1X2
active from X -> from active X
0 + 0X >= 0 + 0X
active from X -> mark cons(X, from s X)
0 + 0X >= 2 + 1X
active s X -> s active X
0 + 0X >= 1 + 0X
active cons(X1, X2) -> cons(active X1, X2)
0 + 0X1 + 0X2 >= 1 + 0X1 + 1X2
active first(s X, cons(Y, Z)) -> mark cons(Y, first(X, Z))
0 + 0X + 0Y + 0Z >= 2 + 1X + 1Y + 1Z
active first(0(), X) -> mark nil()
0 + 0X >= 2
active first(X1, X2) -> first(active X1, X2)
0 + 0X1 + 0X2 >= 0 + 0X1 + 1X2
active first(X1, X2) -> first(X1, active X2)
0 + 0X1 + 0X2 >= 0 + 1X1 + 0X2
SCCS (1):
Scc:
{proper# first(X1, X2) -> proper# X1,
proper# first(X1, X2) -> proper# X2}
SCC (2):
Strict:
{proper# first(X1, X2) -> proper# X1,
proper# first(X1, X2) -> proper# X2}
Weak:
{ active first(X1, X2) -> first(X1, active X2),
active first(X1, X2) -> first(active X1, X2),
active first(0(), X) -> mark nil(),
active first(s X, cons(Y, Z)) -> mark cons(Y, first(X, Z)),
active cons(X1, X2) -> cons(active X1, X2),
active s X -> s active X,
active from X -> mark cons(X, from s X),
active from X -> from active X,
first(X1, mark X2) -> mark first(X1, X2),
first(mark X1, X2) -> mark first(X1, X2),
first(ok X1, ok X2) -> ok first(X1, X2),
cons(mark X1, X2) -> mark cons(X1, X2),
cons(ok X1, ok X2) -> ok cons(X1, X2),
s mark X -> mark s X,
s ok X -> ok s X,
from mark X -> mark from X,
from ok X -> ok from X,
proper nil() -> ok nil(),
proper first(X1, X2) -> first(proper X1, proper X2),
proper 0() -> ok 0(),
proper cons(X1, X2) -> cons(proper X1, proper X2),
proper s X -> s proper X,
proper from X -> from 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:
[first](x0, x1) = x0 + x1 + 1,
[cons](x0, x1) = 0,
[mark](x0) = x0 + 1,
[active](x0) = 0,
[s](x0) = 1,
[from](x0) = x0,
[proper](x0) = x0 + 1,
[ok](x0) = 0,
[top](x0) = x0,
[nil] = 1,
[0] = 0,
[proper#](x0) = x0 + 1
Strict:
proper# first(X1, X2) -> proper# X2
2 + 1X1 + 1X2 >= 1 + 1X2
proper# first(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
1 + 1X >= 1 + 1X
proper from X -> from proper X
1 + 1X >= 1 + 1X
proper s X -> s proper X
2 + 0X >= 1 + 0X
proper cons(X1, X2) -> cons(proper X1, proper X2)
1 + 0X1 + 0X2 >= 0 + 0X1 + 0X2
proper 0() -> ok 0()
1 >= 0
proper first(X1, X2) -> first(proper X1, proper X2)
2 + 1X1 + 1X2 >= 3 + 1X1 + 1X2
proper nil() -> ok nil()
2 >= 0
from ok X -> ok from X
0 + 0X >= 0 + 0X
from mark X -> mark from X
1 + 1X >= 1 + 1X
s ok X -> ok s X
1 + 0X >= 0 + 0X
s mark X -> mark s X
1 + 0X >= 2 + 0X
cons(ok X1, ok X2) -> ok cons(X1, X2)
0 + 0X1 + 0X2 >= 0 + 0X1 + 0X2
cons(mark X1, X2) -> mark cons(X1, X2)
0 + 0X1 + 0X2 >= 1 + 0X1 + 0X2
first(ok X1, ok X2) -> ok first(X1, X2)
1 + 0X1 + 0X2 >= 0 + 0X1 + 0X2
first(mark X1, X2) -> mark first(X1, X2)
2 + 1X1 + 1X2 >= 2 + 1X1 + 1X2
first(X1, mark X2) -> mark first(X1, X2)
2 + 1X1 + 1X2 >= 2 + 1X1 + 1X2
active from X -> from active X
0 + 0X >= 0 + 0X
active from X -> mark cons(X, from s X)
0 + 0X >= 1 + 0X
active s X -> s active X
0 + 0X >= 1 + 0X
active cons(X1, X2) -> cons(active X1, X2)
0 + 0X1 + 0X2 >= 0 + 0X1 + 0X2
active first(s X, cons(Y, Z)) -> mark cons(Y, first(X, Z))
0 + 0X + 0Y + 0Z >= 1 + 0X + 0Y + 0Z
active first(0(), X) -> mark nil()
0 + 0X >= 2
active first(X1, X2) -> first(active X1, X2)
0 + 0X1 + 0X2 >= 1 + 0X1 + 1X2
active first(X1, X2) -> first(X1, active X2)
0 + 0X1 + 0X2 >= 1 + 1X1 + 0X2
Qed
SCC (2):
Strict:
{ cons#(mark X1, X2) -> cons#(X1, X2),
cons#(ok X1, ok X2) -> cons#(X1, X2)}
Weak:
{ active first(X1, X2) -> first(X1, active X2),
active first(X1, X2) -> first(active X1, X2),
active first(0(), X) -> mark nil(),
active first(s X, cons(Y, Z)) -> mark cons(Y, first(X, Z)),
active cons(X1, X2) -> cons(active X1, X2),
active s X -> s active X,
active from X -> mark cons(X, from s X),
active from X -> from active X,
first(X1, mark X2) -> mark first(X1, X2),
first(mark X1, X2) -> mark first(X1, X2),
first(ok X1, ok X2) -> ok first(X1, X2),
cons(mark X1, X2) -> mark cons(X1, X2),
cons(ok X1, ok X2) -> ok cons(X1, X2),
s mark X -> mark s X,
s ok X -> ok s X,
from mark X -> mark from X,
from ok X -> ok from X,
proper nil() -> ok nil(),
proper first(X1, X2) -> first(proper X1, proper X2),
proper 0() -> ok 0(),
proper cons(X1, X2) -> cons(proper X1, proper X2),
proper s X -> s proper X,
proper from X -> from 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:
[first](x0, x1) = x0 + 1,
[cons](x0, x1) = x0 + 1,
[mark](x0) = x0 + 1,
[active](x0) = x0 + 1,
[s](x0) = x0 + 1,
[from](x0) = 0,
[proper](x0) = 0,
[ok](x0) = x0 + 1,
[top](x0) = 0,
[nil] = 1,
[0] = 1,
[cons#](x0, x1) = x0
Strict:
cons#(ok X1, ok X2) -> cons#(X1, X2)
1 + 0X1 + 1X2 >= 0 + 0X1 + 1X2
cons#(mark X1, X2) -> cons#(X1, X2)
0 + 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 from X -> from proper X
0 + 0X >= 0 + 0X
proper s X -> s proper X
0 + 0X >= 1 + 0X
proper cons(X1, X2) -> cons(proper X1, proper X2)
0 + 0X1 + 0X2 >= 1 + 0X1 + 0X2
proper 0() -> ok 0()
0 >= 2
proper first(X1, X2) -> first(proper X1, proper X2)
0 + 0X1 + 0X2 >= 1 + 0X1 + 0X2
proper nil() -> ok nil()
0 >= 2
from ok X -> ok from X
0 + 0X >= 1 + 0X
from mark X -> mark from X
0 + 0X >= 1 + 0X
s ok X -> ok s X
2 + 1X >= 2 + 1X
s mark X -> mark s X
2 + 1X >= 2 + 1X
cons(ok X1, ok X2) -> ok cons(X1, X2)
2 + 0X1 + 1X2 >= 2 + 0X1 + 1X2
cons(mark X1, X2) -> mark cons(X1, X2)
1 + 0X1 + 1X2 >= 2 + 0X1 + 1X2
first(ok X1, ok X2) -> ok first(X1, X2)
2 + 0X1 + 1X2 >= 2 + 0X1 + 1X2
first(mark X1, X2) -> mark first(X1, X2)
1 + 0X1 + 1X2 >= 2 + 0X1 + 1X2
first(X1, mark X2) -> mark first(X1, X2)
2 + 0X1 + 1X2 >= 2 + 0X1 + 1X2
active from X -> from active X
1 + 0X >= 0 + 0X
active from X -> mark cons(X, from s X)
1 + 0X >= 2 + 0X
active s X -> s active X
2 + 1X >= 2 + 1X
active cons(X1, X2) -> cons(active X1, X2)
2 + 0X1 + 1X2 >= 1 + 0X1 + 1X2
active first(s X, cons(Y, Z)) -> mark cons(Y, first(X, Z))
3 + 0X + 0Y + 1Z >= 3 + 0X + 0Y + 1Z
active first(0(), X) -> mark nil()
2 + 1X >= 2
active first(X1, X2) -> first(active X1, X2)
2 + 0X1 + 1X2 >= 1 + 0X1 + 1X2
active first(X1, X2) -> first(X1, active X2)
2 + 0X1 + 1X2 >= 2 + 0X1 + 1X2
SCCS (1):
Scc:
{cons#(mark X1, X2) -> cons#(X1, X2)}
SCC (1):
Strict:
{cons#(mark X1, X2) -> cons#(X1, X2)}
Weak:
{ active first(X1, X2) -> first(X1, active X2),
active first(X1, X2) -> first(active X1, X2),
active first(0(), X) -> mark nil(),
active first(s X, cons(Y, Z)) -> mark cons(Y, first(X, Z)),
active cons(X1, X2) -> cons(active X1, X2),
active s X -> s active X,
active from X -> mark cons(X, from s X),
active from X -> from active X,
first(X1, mark X2) -> mark first(X1, X2),
first(mark X1, X2) -> mark first(X1, X2),
first(ok X1, ok X2) -> ok first(X1, X2),
cons(mark X1, X2) -> mark cons(X1, X2),
cons(ok X1, ok X2) -> ok cons(X1, X2),
s mark X -> mark s X,
s ok X -> ok s X,
from mark X -> mark from X,
from ok X -> ok from X,
proper nil() -> ok nil(),
proper first(X1, X2) -> first(proper X1, proper X2),
proper 0() -> ok 0(),
proper cons(X1, X2) -> cons(proper X1, proper X2),
proper s X -> s proper X,
proper from X -> from 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:
[first](x0, x1) = x0 + x1 + 1,
[cons](x0, x1) = 0,
[mark](x0) = x0 + 1,
[active](x0) = x0 + 1,
[s](x0) = 1,
[from](x0) = x0,
[proper](x0) = 1,
[ok](x0) = 0,
[top](x0) = x0,
[nil] = 0,
[0] = 1,
[cons#](x0, x1) = x0
Strict:
cons#(mark X1, X2) -> cons#(X1, X2)
1 + 1X1 + 0X2 >= 0 + 1X1 + 0X2
Weak:
top ok X -> top active X
0 + 0X >= 1 + 1X
top mark X -> top proper X
1 + 1X >= 1 + 0X
proper from X -> from proper X
1 + 0X >= 1 + 0X
proper s X -> s proper X
1 + 0X >= 1 + 0X
proper cons(X1, X2) -> cons(proper X1, proper X2)
1 + 0X1 + 0X2 >= 0 + 0X1 + 0X2
proper 0() -> ok 0()
1 >= 0
proper first(X1, X2) -> first(proper X1, proper X2)
1 + 0X1 + 0X2 >= 3 + 0X1 + 0X2
proper nil() -> ok nil()
1 >= 0
from ok X -> ok from X
0 + 0X >= 0 + 0X
from mark X -> mark from X
1 + 1X >= 1 + 1X
s ok X -> ok s X
1 + 0X >= 0 + 0X
s mark X -> mark s X
1 + 0X >= 2 + 0X
cons(ok X1, ok X2) -> ok cons(X1, X2)
0 + 0X1 + 0X2 >= 0 + 0X1 + 0X2
cons(mark X1, X2) -> mark cons(X1, X2)
0 + 0X1 + 0X2 >= 1 + 0X1 + 0X2
first(ok X1, ok X2) -> ok first(X1, X2)
1 + 0X1 + 0X2 >= 0 + 0X1 + 0X2
first(mark X1, X2) -> mark first(X1, X2)
2 + 1X1 + 1X2 >= 2 + 1X1 + 1X2
first(X1, mark X2) -> mark first(X1, X2)
2 + 1X1 + 1X2 >= 2 + 1X1 + 1X2
active from X -> from active X
1 + 1X >= 1 + 1X
active from X -> mark cons(X, from s X)
1 + 1X >= 1 + 0X
active s X -> s active X
2 + 0X >= 1 + 0X
active cons(X1, X2) -> cons(active X1, X2)
1 + 0X1 + 0X2 >= 0 + 0X1 + 0X2
active first(s X, cons(Y, Z)) -> mark cons(Y, first(X, Z))
3 + 0X + 0Y + 0Z >= 1 + 0X + 0Y + 0Z
active first(0(), X) -> mark nil()
3 + 1X >= 1
active first(X1, X2) -> first(active X1, X2)
2 + 1X1 + 1X2 >= 2 + 1X1 + 1X2
active first(X1, X2) -> first(X1, active X2)
2 + 1X1 + 1X2 >= 2 + 1X1 + 1X2
Qed
SCC (2):
Strict:
{from# mark X -> from# X,
from# ok X -> from# X}
Weak:
{ active first(X1, X2) -> first(X1, active X2),
active first(X1, X2) -> first(active X1, X2),
active first(0(), X) -> mark nil(),
active first(s X, cons(Y, Z)) -> mark cons(Y, first(X, Z)),
active cons(X1, X2) -> cons(active X1, X2),
active s X -> s active X,
active from X -> mark cons(X, from s X),
active from X -> from active X,
first(X1, mark X2) -> mark first(X1, X2),
first(mark X1, X2) -> mark first(X1, X2),
first(ok X1, ok X2) -> ok first(X1, X2),
cons(mark X1, X2) -> mark cons(X1, X2),
cons(ok X1, ok X2) -> ok cons(X1, X2),
s mark X -> mark s X,
s ok X -> ok s X,
from mark X -> mark from X,
from ok X -> ok from X,
proper nil() -> ok nil(),
proper first(X1, X2) -> first(proper X1, proper X2),
proper 0() -> ok 0(),
proper cons(X1, X2) -> cons(proper X1, proper X2),
proper s X -> s proper X,
proper from X -> from 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:
[first](x0, x1) = x0 + 1,
[cons](x0, x1) = x0 + 1,
[mark](x0) = x0,
[active](x0) = x0 + 1,
[s](x0) = x0 + 1,
[from](x0) = 1,
[proper](x0) = 0,
[ok](x0) = x0 + 1,
[top](x0) = 0,
[nil] = 0,
[0] = 1,
[from#](x0) = x0
Strict:
from# ok X -> from# X
1 + 1X >= 0 + 1X
from# mark X -> from# 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 from X -> from proper X
0 + 0X >= 1 + 0X
proper s X -> s proper X
0 + 0X >= 1 + 0X
proper cons(X1, X2) -> cons(proper X1, proper X2)
0 + 0X1 + 0X2 >= 1 + 0X1 + 0X2
proper 0() -> ok 0()
0 >= 2
proper first(X1, X2) -> first(proper X1, proper X2)
0 + 0X1 + 0X2 >= 1 + 0X1 + 0X2
proper nil() -> ok nil()
0 >= 1
from ok X -> ok from X
1 + 0X >= 2 + 0X
from mark X -> mark from X
1 + 0X >= 1 + 0X
s ok X -> ok s X
2 + 1X >= 2 + 1X
s mark X -> mark s X
1 + 1X >= 1 + 1X
cons(ok X1, ok X2) -> ok cons(X1, X2)
2 + 0X1 + 1X2 >= 2 + 0X1 + 1X2
cons(mark X1, X2) -> mark cons(X1, X2)
1 + 0X1 + 1X2 >= 1 + 0X1 + 1X2
first(ok X1, ok X2) -> ok first(X1, X2)
2 + 0X1 + 1X2 >= 2 + 0X1 + 1X2
first(mark X1, X2) -> mark first(X1, X2)
1 + 0X1 + 1X2 >= 1 + 0X1 + 1X2
first(X1, mark X2) -> mark first(X1, X2)
1 + 0X1 + 1X2 >= 1 + 0X1 + 1X2
active from X -> from active X
2 + 0X >= 1 + 0X
active from X -> mark cons(X, from s X)
2 + 0X >= 2 + 0X
active s X -> s active X
2 + 1X >= 2 + 1X
active cons(X1, X2) -> cons(active X1, X2)
2 + 0X1 + 1X2 >= 1 + 0X1 + 1X2
active first(s X, cons(Y, Z)) -> mark cons(Y, first(X, Z))
3 + 0X + 0Y + 1Z >= 2 + 0X + 0Y + 1Z
active first(0(), X) -> mark nil()
2 + 1X >= 0
active first(X1, X2) -> first(active X1, X2)
2 + 0X1 + 1X2 >= 1 + 0X1 + 1X2
active first(X1, X2) -> first(X1, active X2)
2 + 0X1 + 1X2 >= 2 + 0X1 + 1X2
SCCS (1):
Scc:
{from# mark X -> from# X}
SCC (1):
Strict:
{from# mark X -> from# X}
Weak:
{ active first(X1, X2) -> first(X1, active X2),
active first(X1, X2) -> first(active X1, X2),
active first(0(), X) -> mark nil(),
active first(s X, cons(Y, Z)) -> mark cons(Y, first(X, Z)),
active cons(X1, X2) -> cons(active X1, X2),
active s X -> s active X,
active from X -> mark cons(X, from s X),
active from X -> from active X,
first(X1, mark X2) -> mark first(X1, X2),
first(mark X1, X2) -> mark first(X1, X2),
first(ok X1, ok X2) -> ok first(X1, X2),
cons(mark X1, X2) -> mark cons(X1, X2),
cons(ok X1, ok X2) -> ok cons(X1, X2),
s mark X -> mark s X,
s ok X -> ok s X,
from mark X -> mark from X,
from ok X -> ok from X,
proper nil() -> ok nil(),
proper first(X1, X2) -> first(proper X1, proper X2),
proper 0() -> ok 0(),
proper cons(X1, X2) -> cons(proper X1, proper X2),
proper s X -> s proper X,
proper from X -> from 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:
[first](x0, x1) = x0 + x1 + 1,
[cons](x0, x1) = 0,
[mark](x0) = x0 + 1,
[active](x0) = x0 + 1,
[s](x0) = 1,
[from](x0) = x0,
[proper](x0) = 1,
[ok](x0) = 0,
[top](x0) = x0,
[nil] = 0,
[0] = 1,
[from#](x0) = x0
Strict:
from# mark X -> from# X
1 + 1X >= 0 + 1X
Weak:
top ok X -> top active X
0 + 0X >= 1 + 1X
top mark X -> top proper X
1 + 1X >= 1 + 0X
proper from X -> from proper X
1 + 0X >= 1 + 0X
proper s X -> s proper X
1 + 0X >= 1 + 0X
proper cons(X1, X2) -> cons(proper X1, proper X2)
1 + 0X1 + 0X2 >= 0 + 0X1 + 0X2
proper 0() -> ok 0()
1 >= 0
proper first(X1, X2) -> first(proper X1, proper X2)
1 + 0X1 + 0X2 >= 3 + 0X1 + 0X2
proper nil() -> ok nil()
1 >= 0
from ok X -> ok from X
0 + 0X >= 0 + 0X
from mark X -> mark from X
1 + 1X >= 1 + 1X
s ok X -> ok s X
1 + 0X >= 0 + 0X
s mark X -> mark s X
1 + 0X >= 2 + 0X
cons(ok X1, ok X2) -> ok cons(X1, X2)
0 + 0X1 + 0X2 >= 0 + 0X1 + 0X2
cons(mark X1, X2) -> mark cons(X1, X2)
0 + 0X1 + 0X2 >= 1 + 0X1 + 0X2
first(ok X1, ok X2) -> ok first(X1, X2)
1 + 0X1 + 0X2 >= 0 + 0X1 + 0X2
first(mark X1, X2) -> mark first(X1, X2)
2 + 1X1 + 1X2 >= 2 + 1X1 + 1X2
first(X1, mark X2) -> mark first(X1, X2)
2 + 1X1 + 1X2 >= 2 + 1X1 + 1X2
active from X -> from active X
1 + 1X >= 1 + 1X
active from X -> mark cons(X, from s X)
1 + 1X >= 1 + 0X
active s X -> s active X
2 + 0X >= 1 + 0X
active cons(X1, X2) -> cons(active X1, X2)
1 + 0X1 + 0X2 >= 0 + 0X1 + 0X2
active first(s X, cons(Y, Z)) -> mark cons(Y, first(X, Z))
3 + 0X + 0Y + 0Z >= 1 + 0X + 0Y + 0Z
active first(0(), X) -> mark nil()
3 + 1X >= 1
active first(X1, X2) -> first(active X1, X2)
2 + 1X1 + 1X2 >= 2 + 1X1 + 1X2
active first(X1, X2) -> first(X1, active X2)
2 + 1X1 + 1X2 >= 2 + 1X1 + 1X2
Qed
SCC (2):
Strict:
{s# mark X -> s# X,
s# ok X -> s# X}
Weak:
{ active first(X1, X2) -> first(X1, active X2),
active first(X1, X2) -> first(active X1, X2),
active first(0(), X) -> mark nil(),
active first(s X, cons(Y, Z)) -> mark cons(Y, first(X, Z)),
active cons(X1, X2) -> cons(active X1, X2),
active s X -> s active X,
active from X -> mark cons(X, from s X),
active from X -> from active X,
first(X1, mark X2) -> mark first(X1, X2),
first(mark X1, X2) -> mark first(X1, X2),
first(ok X1, ok X2) -> ok first(X1, X2),
cons(mark X1, X2) -> mark cons(X1, X2),
cons(ok X1, ok X2) -> ok cons(X1, X2),
s mark X -> mark s X,
s ok X -> ok s X,
from mark X -> mark from X,
from ok X -> ok from X,
proper nil() -> ok nil(),
proper first(X1, X2) -> first(proper X1, proper X2),
proper 0() -> ok 0(),
proper cons(X1, X2) -> cons(proper X1, proper X2),
proper s X -> s proper X,
proper from X -> from 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:
[first](x0, x1) = x0 + 1,
[cons](x0, x1) = x0 + 1,
[mark](x0) = x0,
[active](x0) = x0 + 1,
[s](x0) = x0 + 1,
[from](x0) = 1,
[proper](x0) = 0,
[ok](x0) = x0 + 1,
[top](x0) = 0,
[nil] = 0,
[0] = 1,
[s#](x0) = x0
Strict:
s# ok X -> s# X
1 + 1X >= 0 + 1X
s# mark X -> s# 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 from X -> from proper X
0 + 0X >= 1 + 0X
proper s X -> s proper X
0 + 0X >= 1 + 0X
proper cons(X1, X2) -> cons(proper X1, proper X2)
0 + 0X1 + 0X2 >= 1 + 0X1 + 0X2
proper 0() -> ok 0()
0 >= 2
proper first(X1, X2) -> first(proper X1, proper X2)
0 + 0X1 + 0X2 >= 1 + 0X1 + 0X2
proper nil() -> ok nil()
0 >= 1
from ok X -> ok from X
1 + 0X >= 2 + 0X
from mark X -> mark from X
1 + 0X >= 1 + 0X
s ok X -> ok s X
2 + 1X >= 2 + 1X
s mark X -> mark s X
1 + 1X >= 1 + 1X
cons(ok X1, ok X2) -> ok cons(X1, X2)
2 + 0X1 + 1X2 >= 2 + 0X1 + 1X2
cons(mark X1, X2) -> mark cons(X1, X2)
1 + 0X1 + 1X2 >= 1 + 0X1 + 1X2
first(ok X1, ok X2) -> ok first(X1, X2)
2 + 0X1 + 1X2 >= 2 + 0X1 + 1X2
first(mark X1, X2) -> mark first(X1, X2)
1 + 0X1 + 1X2 >= 1 + 0X1 + 1X2
first(X1, mark X2) -> mark first(X1, X2)
1 + 0X1 + 1X2 >= 1 + 0X1 + 1X2
active from X -> from active X
2 + 0X >= 1 + 0X
active from X -> mark cons(X, from s X)
2 + 0X >= 2 + 0X
active s X -> s active X
2 + 1X >= 2 + 1X
active cons(X1, X2) -> cons(active X1, X2)
2 + 0X1 + 1X2 >= 1 + 0X1 + 1X2
active first(s X, cons(Y, Z)) -> mark cons(Y, first(X, Z))
3 + 0X + 0Y + 1Z >= 2 + 0X + 0Y + 1Z
active first(0(), X) -> mark nil()
2 + 1X >= 0
active first(X1, X2) -> first(active X1, X2)
2 + 0X1 + 1X2 >= 1 + 0X1 + 1X2
active first(X1, X2) -> first(X1, active X2)
2 + 0X1 + 1X2 >= 2 + 0X1 + 1X2
SCCS (1):
Scc:
{s# mark X -> s# X}
SCC (1):
Strict:
{s# mark X -> s# X}
Weak:
{ active first(X1, X2) -> first(X1, active X2),
active first(X1, X2) -> first(active X1, X2),
active first(0(), X) -> mark nil(),
active first(s X, cons(Y, Z)) -> mark cons(Y, first(X, Z)),
active cons(X1, X2) -> cons(active X1, X2),
active s X -> s active X,
active from X -> mark cons(X, from s X),
active from X -> from active X,
first(X1, mark X2) -> mark first(X1, X2),
first(mark X1, X2) -> mark first(X1, X2),
first(ok X1, ok X2) -> ok first(X1, X2),
cons(mark X1, X2) -> mark cons(X1, X2),
cons(ok X1, ok X2) -> ok cons(X1, X2),
s mark X -> mark s X,
s ok X -> ok s X,
from mark X -> mark from X,
from ok X -> ok from X,
proper nil() -> ok nil(),
proper first(X1, X2) -> first(proper X1, proper X2),
proper 0() -> ok 0(),
proper cons(X1, X2) -> cons(proper X1, proper X2),
proper s X -> s proper X,
proper from X -> from 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:
[first](x0, x1) = x0 + x1 + 1,
[cons](x0, x1) = 0,
[mark](x0) = x0 + 1,
[active](x0) = x0 + 1,
[s](x0) = 1,
[from](x0) = x0,
[proper](x0) = 1,
[ok](x0) = 0,
[top](x0) = x0,
[nil] = 0,
[0] = 1,
[s#](x0) = x0
Strict:
s# mark X -> s# X
1 + 1X >= 0 + 1X
Weak:
top ok X -> top active X
0 + 0X >= 1 + 1X
top mark X -> top proper X
1 + 1X >= 1 + 0X
proper from X -> from proper X
1 + 0X >= 1 + 0X
proper s X -> s proper X
1 + 0X >= 1 + 0X
proper cons(X1, X2) -> cons(proper X1, proper X2)
1 + 0X1 + 0X2 >= 0 + 0X1 + 0X2
proper 0() -> ok 0()
1 >= 0
proper first(X1, X2) -> first(proper X1, proper X2)
1 + 0X1 + 0X2 >= 3 + 0X1 + 0X2
proper nil() -> ok nil()
1 >= 0
from ok X -> ok from X
0 + 0X >= 0 + 0X
from mark X -> mark from X
1 + 1X >= 1 + 1X
s ok X -> ok s X
1 + 0X >= 0 + 0X
s mark X -> mark s X
1 + 0X >= 2 + 0X
cons(ok X1, ok X2) -> ok cons(X1, X2)
0 + 0X1 + 0X2 >= 0 + 0X1 + 0X2
cons(mark X1, X2) -> mark cons(X1, X2)
0 + 0X1 + 0X2 >= 1 + 0X1 + 0X2
first(ok X1, ok X2) -> ok first(X1, X2)
1 + 0X1 + 0X2 >= 0 + 0X1 + 0X2
first(mark X1, X2) -> mark first(X1, X2)
2 + 1X1 + 1X2 >= 2 + 1X1 + 1X2
first(X1, mark X2) -> mark first(X1, X2)
2 + 1X1 + 1X2 >= 2 + 1X1 + 1X2
active from X -> from active X
1 + 1X >= 1 + 1X
active from X -> mark cons(X, from s X)
1 + 1X >= 1 + 0X
active s X -> s active X
2 + 0X >= 1 + 0X
active cons(X1, X2) -> cons(active X1, X2)
1 + 0X1 + 0X2 >= 0 + 0X1 + 0X2
active first(s X, cons(Y, Z)) -> mark cons(Y, first(X, Z))
3 + 0X + 0Y + 0Z >= 1 + 0X + 0Y + 0Z
active first(0(), X) -> mark nil()
3 + 1X >= 1
active first(X1, X2) -> first(active X1, X2)
2 + 1X1 + 1X2 >= 2 + 1X1 + 1X2
active first(X1, X2) -> first(X1, active X2)
2 + 1X1 + 1X2 >= 2 + 1X1 + 1X2
Qed
SCC (3):
Strict:
{ first#(X1, mark X2) -> first#(X1, X2),
first#(mark X1, X2) -> first#(X1, X2),
first#(ok X1, ok X2) -> first#(X1, X2)}
Weak:
{ active first(X1, X2) -> first(X1, active X2),
active first(X1, X2) -> first(active X1, X2),
active first(0(), X) -> mark nil(),
active first(s X, cons(Y, Z)) -> mark cons(Y, first(X, Z)),
active cons(X1, X2) -> cons(active X1, X2),
active s X -> s active X,
active from X -> mark cons(X, from s X),
active from X -> from active X,
first(X1, mark X2) -> mark first(X1, X2),
first(mark X1, X2) -> mark first(X1, X2),
first(ok X1, ok X2) -> ok first(X1, X2),
cons(mark X1, X2) -> mark cons(X1, X2),
cons(ok X1, ok X2) -> ok cons(X1, X2),
s mark X -> mark s X,
s ok X -> ok s X,
from mark X -> mark from X,
from ok X -> ok from X,
proper nil() -> ok nil(),
proper first(X1, X2) -> first(proper X1, proper X2),
proper 0() -> ok 0(),
proper cons(X1, X2) -> cons(proper X1, proper X2),
proper s X -> s proper X,
proper from X -> from 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:
[first](x0, x1) = 0,
[cons](x0, x1) = 0,
[mark](x0) = x0 + 1,
[active](x0) = 0,
[s](x0) = x0,
[from](x0) = 0,
[proper](x0) = 0,
[ok](x0) = x0 + 1,
[top](x0) = 0,
[nil] = 1,
[0] = 1,
[first#](x0, x1) = x0 + 1
Strict:
first#(ok X1, ok X2) -> first#(X1, X2)
2 + 1X1 + 0X2 >= 1 + 1X1 + 0X2
first#(mark X1, X2) -> first#(X1, X2)
2 + 1X1 + 0X2 >= 1 + 1X1 + 0X2
first#(X1, mark X2) -> first#(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 from X -> from proper X
0 + 0X >= 0 + 0X
proper s X -> s proper X
0 + 0X >= 0 + 0X
proper cons(X1, X2) -> cons(proper X1, proper X2)
0 + 0X1 + 0X2 >= 0 + 0X1 + 0X2
proper 0() -> ok 0()
0 >= 2
proper first(X1, X2) -> first(proper X1, proper X2)
0 + 0X1 + 0X2 >= 0 + 0X1 + 0X2
proper nil() -> ok nil()
0 >= 2
from ok X -> ok from X
0 + 0X >= 1 + 0X
from mark X -> mark from X
0 + 0X >= 1 + 0X
s ok X -> ok s X
1 + 1X >= 1 + 1X
s mark X -> mark s X
1 + 1X >= 1 + 1X
cons(ok X1, ok X2) -> ok cons(X1, X2)
0 + 0X1 + 0X2 >= 1 + 0X1 + 0X2
cons(mark X1, X2) -> mark cons(X1, X2)
0 + 0X1 + 0X2 >= 1 + 0X1 + 0X2
first(ok X1, ok X2) -> ok first(X1, X2)
0 + 0X1 + 0X2 >= 1 + 0X1 + 0X2
first(mark X1, X2) -> mark first(X1, X2)
0 + 0X1 + 0X2 >= 1 + 0X1 + 0X2
first(X1, mark X2) -> mark first(X1, X2)
0 + 0X1 + 0X2 >= 1 + 0X1 + 0X2
active from X -> from active X
0 + 0X >= 0 + 0X
active from X -> mark cons(X, from s X)
0 + 0X >= 1 + 0X
active s X -> s active X
0 + 0X >= 0 + 0X
active cons(X1, X2) -> cons(active X1, X2)
0 + 0X1 + 0X2 >= 0 + 0X1 + 0X2
active first(s X, cons(Y, Z)) -> mark cons(Y, first(X, Z))
0 + 0X + 0Y + 0Z >= 1 + 0X + 0Y + 0Z
active first(0(), X) -> mark nil()
0 + 0X >= 2
active first(X1, X2) -> first(active X1, X2)
0 + 0X1 + 0X2 >= 0 + 0X1 + 0X2
active first(X1, X2) -> first(X1, active X2)
0 + 0X1 + 0X2 >= 0 + 0X1 + 0X2
SCCS (1):
Scc:
{first#(X1, mark X2) -> first#(X1, X2)}
SCC (1):
Strict:
{first#(X1, mark X2) -> first#(X1, X2)}
Weak:
{ active first(X1, X2) -> first(X1, active X2),
active first(X1, X2) -> first(active X1, X2),
active first(0(), X) -> mark nil(),
active first(s X, cons(Y, Z)) -> mark cons(Y, first(X, Z)),
active cons(X1, X2) -> cons(active X1, X2),
active s X -> s active X,
active from X -> mark cons(X, from s X),
active from X -> from active X,
first(X1, mark X2) -> mark first(X1, X2),
first(mark X1, X2) -> mark first(X1, X2),
first(ok X1, ok X2) -> ok first(X1, X2),
cons(mark X1, X2) -> mark cons(X1, X2),
cons(ok X1, ok X2) -> ok cons(X1, X2),
s mark X -> mark s X,
s ok X -> ok s X,
from mark X -> mark from X,
from ok X -> ok from X,
proper nil() -> ok nil(),
proper first(X1, X2) -> first(proper X1, proper X2),
proper 0() -> ok 0(),
proper cons(X1, X2) -> cons(proper X1, proper X2),
proper s X -> s proper X,
proper from X -> from 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:
[first](x0, x1) = x0 + x1 + 1,
[cons](x0, x1) = 0,
[mark](x0) = x0 + 1,
[active](x0) = x0 + 1,
[s](x0) = 1,
[from](x0) = x0,
[proper](x0) = 1,
[ok](x0) = 0,
[top](x0) = x0,
[nil] = 0,
[0] = 1,
[first#](x0, x1) = x0
Strict:
first#(X1, mark X2) -> first#(X1, X2)
1 + 0X1 + 1X2 >= 0 + 0X1 + 1X2
Weak:
top ok X -> top active X
0 + 0X >= 1 + 1X
top mark X -> top proper X
1 + 1X >= 1 + 0X
proper from X -> from proper X
1 + 0X >= 1 + 0X
proper s X -> s proper X
1 + 0X >= 1 + 0X
proper cons(X1, X2) -> cons(proper X1, proper X2)
1 + 0X1 + 0X2 >= 0 + 0X1 + 0X2
proper 0() -> ok 0()
1 >= 0
proper first(X1, X2) -> first(proper X1, proper X2)
1 + 0X1 + 0X2 >= 3 + 0X1 + 0X2
proper nil() -> ok nil()
1 >= 0
from ok X -> ok from X
0 + 0X >= 0 + 0X
from mark X -> mark from X
1 + 1X >= 1 + 1X
s ok X -> ok s X
1 + 0X >= 0 + 0X
s mark X -> mark s X
1 + 0X >= 2 + 0X
cons(ok X1, ok X2) -> ok cons(X1, X2)
0 + 0X1 + 0X2 >= 0 + 0X1 + 0X2
cons(mark X1, X2) -> mark cons(X1, X2)
0 + 0X1 + 0X2 >= 1 + 0X1 + 0X2
first(ok X1, ok X2) -> ok first(X1, X2)
1 + 0X1 + 0X2 >= 0 + 0X1 + 0X2
first(mark X1, X2) -> mark first(X1, X2)
2 + 1X1 + 1X2 >= 2 + 1X1 + 1X2
first(X1, mark X2) -> mark first(X1, X2)
2 + 1X1 + 1X2 >= 2 + 1X1 + 1X2
active from X -> from active X
1 + 1X >= 1 + 1X
active from X -> mark cons(X, from s X)
1 + 1X >= 1 + 0X
active s X -> s active X
2 + 0X >= 1 + 0X
active cons(X1, X2) -> cons(active X1, X2)
1 + 0X1 + 0X2 >= 0 + 0X1 + 0X2
active first(s X, cons(Y, Z)) -> mark cons(Y, first(X, Z))
3 + 0X + 0Y + 0Z >= 1 + 0X + 0Y + 0Z
active first(0(), X) -> mark nil()
3 + 1X >= 1
active first(X1, X2) -> first(active X1, X2)
2 + 1X1 + 1X2 >= 2 + 1X1 + 1X2
active first(X1, X2) -> first(X1, active X2)
2 + 1X1 + 1X2 >= 2 + 1X1 + 1X2
Qed