YES
TRS:
{ mark(adx(X)) -> active(adx(mark(X))),
mark(zeros()) -> active(zeros()),
mark(nats()) -> active(nats()),
mark(cons(X1, X2)) -> active(cons(X1, X2)),
mark(0()) -> active(0()),
mark(s(X)) -> active(s(X)),
mark(incr(X)) -> active(incr(mark(X))),
mark(hd(X)) -> active(hd(mark(X))),
mark(tl(X)) -> active(tl(mark(X))),
adx(mark(X)) -> adx(X),
adx(active(X)) -> adx(X),
active(adx(cons(X, Y))) -> mark(incr(cons(X, adx(Y)))),
active(zeros()) -> mark(cons(0(), zeros())),
active(nats()) -> mark(adx(zeros())),
active(incr(cons(X, Y))) -> mark(cons(s(X), incr(Y))),
active(hd(cons(X, Y))) -> mark(X),
active(tl(cons(X, Y))) -> mark(Y),
cons(X1, mark(X2)) -> cons(X1, X2),
cons(X1, active(X2)) -> cons(X1, X2),
cons(mark(X1), X2) -> cons(X1, X2),
cons(active(X1), X2) -> cons(X1, X2),
s(mark(X)) -> s(X),
s(active(X)) -> s(X),
incr(mark(X)) -> incr(X),
incr(active(X)) -> incr(X),
hd(mark(X)) -> hd(X),
hd(active(X)) -> hd(X),
tl(mark(X)) -> tl(X),
tl(active(X)) -> tl(X)}
DP:
Strict:
{ mark#(adx(X)) -> mark#(X),
mark#(adx(X)) -> adx#(mark(X)),
mark#(adx(X)) -> active#(adx(mark(X))),
mark#(zeros()) -> active#(zeros()),
mark#(nats()) -> active#(nats()),
mark#(cons(X1, X2)) -> active#(cons(X1, X2)),
mark#(0()) -> active#(0()),
mark#(s(X)) -> active#(s(X)),
mark#(incr(X)) -> mark#(X),
mark#(incr(X)) -> active#(incr(mark(X))),
mark#(incr(X)) -> incr#(mark(X)),
mark#(hd(X)) -> mark#(X),
mark#(hd(X)) -> active#(hd(mark(X))),
mark#(hd(X)) -> hd#(mark(X)),
mark#(tl(X)) -> mark#(X),
mark#(tl(X)) -> active#(tl(mark(X))),
mark#(tl(X)) -> tl#(mark(X)),
adx#(mark(X)) -> adx#(X),
adx#(active(X)) -> adx#(X),
active#(adx(cons(X, Y))) -> mark#(incr(cons(X, adx(Y)))),
active#(adx(cons(X, Y))) -> adx#(Y),
active#(adx(cons(X, Y))) -> cons#(X, adx(Y)),
active#(adx(cons(X, Y))) -> incr#(cons(X, adx(Y))),
active#(zeros()) -> mark#(cons(0(), zeros())),
active#(zeros()) -> cons#(0(), zeros()),
active#(nats()) -> mark#(adx(zeros())),
active#(nats()) -> adx#(zeros()),
active#(incr(cons(X, Y))) -> mark#(cons(s(X), incr(Y))),
active#(incr(cons(X, Y))) -> cons#(s(X), incr(Y)),
active#(incr(cons(X, Y))) -> s#(X),
active#(incr(cons(X, Y))) -> incr#(Y),
active#(hd(cons(X, Y))) -> mark#(X),
active#(tl(cons(X, Y))) -> mark#(Y),
cons#(X1, mark(X2)) -> cons#(X1, X2),
cons#(X1, active(X2)) -> cons#(X1, X2),
cons#(mark(X1), X2) -> cons#(X1, X2),
cons#(active(X1), X2) -> cons#(X1, X2),
s#(mark(X)) -> s#(X),
s#(active(X)) -> s#(X),
incr#(mark(X)) -> incr#(X),
incr#(active(X)) -> incr#(X),
hd#(mark(X)) -> hd#(X),
hd#(active(X)) -> hd#(X),
tl#(mark(X)) -> tl#(X),
tl#(active(X)) -> tl#(X)}
Weak:
{ mark(adx(X)) -> active(adx(mark(X))),
mark(zeros()) -> active(zeros()),
mark(nats()) -> active(nats()),
mark(cons(X1, X2)) -> active(cons(X1, X2)),
mark(0()) -> active(0()),
mark(s(X)) -> active(s(X)),
mark(incr(X)) -> active(incr(mark(X))),
mark(hd(X)) -> active(hd(mark(X))),
mark(tl(X)) -> active(tl(mark(X))),
adx(mark(X)) -> adx(X),
adx(active(X)) -> adx(X),
active(adx(cons(X, Y))) -> mark(incr(cons(X, adx(Y)))),
active(zeros()) -> mark(cons(0(), zeros())),
active(nats()) -> mark(adx(zeros())),
active(incr(cons(X, Y))) -> mark(cons(s(X), incr(Y))),
active(hd(cons(X, Y))) -> mark(X),
active(tl(cons(X, Y))) -> mark(Y),
cons(X1, mark(X2)) -> cons(X1, X2),
cons(X1, active(X2)) -> cons(X1, X2),
cons(mark(X1), X2) -> cons(X1, X2),
cons(active(X1), X2) -> cons(X1, X2),
s(mark(X)) -> s(X),
s(active(X)) -> s(X),
incr(mark(X)) -> incr(X),
incr(active(X)) -> incr(X),
hd(mark(X)) -> hd(X),
hd(active(X)) -> hd(X),
tl(mark(X)) -> tl(X),
tl(active(X)) -> tl(X)}
EDG:
{
(active#(nats()) -> mark#(adx(zeros())), mark#(adx(X)) -> active#(adx(mark(X))))
(active#(nats()) -> mark#(adx(zeros())), mark#(adx(X)) -> adx#(mark(X)))
(active#(nats()) -> mark#(adx(zeros())), mark#(adx(X)) -> mark#(X))
(mark#(incr(X)) -> active#(incr(mark(X))), active#(tl(cons(X, Y))) -> mark#(Y))
(mark#(incr(X)) -> active#(incr(mark(X))), active#(hd(cons(X, Y))) -> mark#(X))
(mark#(incr(X)) -> active#(incr(mark(X))), active#(incr(cons(X, Y))) -> incr#(Y))
(mark#(incr(X)) -> active#(incr(mark(X))), active#(incr(cons(X, Y))) -> s#(X))
(mark#(incr(X)) -> active#(incr(mark(X))), active#(incr(cons(X, Y))) -> cons#(s(X), incr(Y)))
(mark#(incr(X)) -> active#(incr(mark(X))), active#(incr(cons(X, Y))) -> mark#(cons(s(X), incr(Y))))
(mark#(incr(X)) -> active#(incr(mark(X))), active#(adx(cons(X, Y))) -> incr#(cons(X, adx(Y))))
(mark#(incr(X)) -> active#(incr(mark(X))), active#(adx(cons(X, Y))) -> cons#(X, adx(Y)))
(mark#(incr(X)) -> active#(incr(mark(X))), active#(adx(cons(X, Y))) -> adx#(Y))
(mark#(incr(X)) -> active#(incr(mark(X))), active#(adx(cons(X, Y))) -> mark#(incr(cons(X, adx(Y)))))
(mark#(tl(X)) -> active#(tl(mark(X))), active#(tl(cons(X, Y))) -> mark#(Y))
(mark#(tl(X)) -> active#(tl(mark(X))), active#(hd(cons(X, Y))) -> mark#(X))
(mark#(tl(X)) -> active#(tl(mark(X))), active#(incr(cons(X, Y))) -> incr#(Y))
(mark#(tl(X)) -> active#(tl(mark(X))), active#(incr(cons(X, Y))) -> s#(X))
(mark#(tl(X)) -> active#(tl(mark(X))), active#(incr(cons(X, Y))) -> cons#(s(X), incr(Y)))
(mark#(tl(X)) -> active#(tl(mark(X))), active#(incr(cons(X, Y))) -> mark#(cons(s(X), incr(Y))))
(mark#(tl(X)) -> active#(tl(mark(X))), active#(adx(cons(X, Y))) -> incr#(cons(X, adx(Y))))
(mark#(tl(X)) -> active#(tl(mark(X))), active#(adx(cons(X, Y))) -> cons#(X, adx(Y)))
(mark#(tl(X)) -> active#(tl(mark(X))), active#(adx(cons(X, Y))) -> adx#(Y))
(mark#(tl(X)) -> active#(tl(mark(X))), active#(adx(cons(X, Y))) -> mark#(incr(cons(X, adx(Y)))))
(mark#(adx(X)) -> mark#(X), mark#(tl(X)) -> tl#(mark(X)))
(mark#(adx(X)) -> mark#(X), mark#(tl(X)) -> active#(tl(mark(X))))
(mark#(adx(X)) -> mark#(X), mark#(tl(X)) -> mark#(X))
(mark#(adx(X)) -> mark#(X), mark#(hd(X)) -> hd#(mark(X)))
(mark#(adx(X)) -> mark#(X), mark#(hd(X)) -> active#(hd(mark(X))))
(mark#(adx(X)) -> mark#(X), mark#(hd(X)) -> mark#(X))
(mark#(adx(X)) -> mark#(X), mark#(incr(X)) -> incr#(mark(X)))
(mark#(adx(X)) -> mark#(X), mark#(incr(X)) -> active#(incr(mark(X))))
(mark#(adx(X)) -> mark#(X), mark#(incr(X)) -> mark#(X))
(mark#(adx(X)) -> mark#(X), mark#(s(X)) -> active#(s(X)))
(mark#(adx(X)) -> mark#(X), mark#(0()) -> active#(0()))
(mark#(adx(X)) -> mark#(X), mark#(cons(X1, X2)) -> active#(cons(X1, X2)))
(mark#(adx(X)) -> mark#(X), mark#(nats()) -> active#(nats()))
(mark#(adx(X)) -> mark#(X), mark#(zeros()) -> active#(zeros()))
(mark#(adx(X)) -> mark#(X), mark#(adx(X)) -> active#(adx(mark(X))))
(mark#(adx(X)) -> mark#(X), mark#(adx(X)) -> adx#(mark(X)))
(mark#(adx(X)) -> mark#(X), mark#(adx(X)) -> mark#(X))
(mark#(hd(X)) -> mark#(X), mark#(tl(X)) -> tl#(mark(X)))
(mark#(hd(X)) -> mark#(X), mark#(tl(X)) -> active#(tl(mark(X))))
(mark#(hd(X)) -> mark#(X), mark#(tl(X)) -> mark#(X))
(mark#(hd(X)) -> mark#(X), mark#(hd(X)) -> hd#(mark(X)))
(mark#(hd(X)) -> mark#(X), mark#(hd(X)) -> active#(hd(mark(X))))
(mark#(hd(X)) -> mark#(X), mark#(hd(X)) -> mark#(X))
(mark#(hd(X)) -> mark#(X), mark#(incr(X)) -> incr#(mark(X)))
(mark#(hd(X)) -> mark#(X), mark#(incr(X)) -> active#(incr(mark(X))))
(mark#(hd(X)) -> mark#(X), mark#(incr(X)) -> mark#(X))
(mark#(hd(X)) -> mark#(X), mark#(s(X)) -> active#(s(X)))
(mark#(hd(X)) -> mark#(X), mark#(0()) -> active#(0()))
(mark#(hd(X)) -> mark#(X), mark#(cons(X1, X2)) -> active#(cons(X1, X2)))
(mark#(hd(X)) -> mark#(X), mark#(nats()) -> active#(nats()))
(mark#(hd(X)) -> mark#(X), mark#(zeros()) -> active#(zeros()))
(mark#(hd(X)) -> mark#(X), mark#(adx(X)) -> active#(adx(mark(X))))
(mark#(hd(X)) -> mark#(X), mark#(adx(X)) -> adx#(mark(X)))
(mark#(hd(X)) -> mark#(X), mark#(adx(X)) -> mark#(X))
(adx#(mark(X)) -> adx#(X), adx#(active(X)) -> adx#(X))
(adx#(mark(X)) -> adx#(X), adx#(mark(X)) -> adx#(X))
(active#(incr(cons(X, Y))) -> s#(X), s#(active(X)) -> s#(X))
(active#(incr(cons(X, Y))) -> s#(X), s#(mark(X)) -> s#(X))
(s#(mark(X)) -> s#(X), s#(active(X)) -> s#(X))
(s#(mark(X)) -> s#(X), s#(mark(X)) -> s#(X))
(incr#(mark(X)) -> incr#(X), incr#(active(X)) -> incr#(X))
(incr#(mark(X)) -> incr#(X), incr#(mark(X)) -> incr#(X))
(hd#(mark(X)) -> hd#(X), hd#(active(X)) -> hd#(X))
(hd#(mark(X)) -> hd#(X), hd#(mark(X)) -> hd#(X))
(tl#(mark(X)) -> tl#(X), tl#(active(X)) -> tl#(X))
(tl#(mark(X)) -> tl#(X), tl#(mark(X)) -> tl#(X))
(mark#(zeros()) -> active#(zeros()), active#(zeros()) -> cons#(0(), zeros()))
(mark#(zeros()) -> active#(zeros()), active#(zeros()) -> mark#(cons(0(), zeros())))
(active#(adx(cons(X, Y))) -> adx#(Y), adx#(active(X)) -> adx#(X))
(active#(adx(cons(X, Y))) -> adx#(Y), adx#(mark(X)) -> adx#(X))
(active#(tl(cons(X, Y))) -> mark#(Y), mark#(tl(X)) -> tl#(mark(X)))
(active#(tl(cons(X, Y))) -> mark#(Y), mark#(tl(X)) -> active#(tl(mark(X))))
(active#(tl(cons(X, Y))) -> mark#(Y), mark#(tl(X)) -> mark#(X))
(active#(tl(cons(X, Y))) -> mark#(Y), mark#(hd(X)) -> hd#(mark(X)))
(active#(tl(cons(X, Y))) -> mark#(Y), mark#(hd(X)) -> active#(hd(mark(X))))
(active#(tl(cons(X, Y))) -> mark#(Y), mark#(hd(X)) -> mark#(X))
(active#(tl(cons(X, Y))) -> mark#(Y), mark#(incr(X)) -> incr#(mark(X)))
(active#(tl(cons(X, Y))) -> mark#(Y), mark#(incr(X)) -> active#(incr(mark(X))))
(active#(tl(cons(X, Y))) -> mark#(Y), mark#(incr(X)) -> mark#(X))
(active#(tl(cons(X, Y))) -> mark#(Y), mark#(s(X)) -> active#(s(X)))
(active#(tl(cons(X, Y))) -> mark#(Y), mark#(0()) -> active#(0()))
(active#(tl(cons(X, Y))) -> mark#(Y), mark#(cons(X1, X2)) -> active#(cons(X1, X2)))
(active#(tl(cons(X, Y))) -> mark#(Y), mark#(nats()) -> active#(nats()))
(active#(tl(cons(X, Y))) -> mark#(Y), mark#(zeros()) -> active#(zeros()))
(active#(tl(cons(X, Y))) -> mark#(Y), mark#(adx(X)) -> active#(adx(mark(X))))
(active#(tl(cons(X, Y))) -> mark#(Y), mark#(adx(X)) -> adx#(mark(X)))
(active#(tl(cons(X, Y))) -> mark#(Y), mark#(adx(X)) -> mark#(X))
(active#(zeros()) -> mark#(cons(0(), zeros())), mark#(cons(X1, X2)) -> active#(cons(X1, X2)))
(active#(adx(cons(X, Y))) -> cons#(X, adx(Y)), cons#(active(X1), X2) -> cons#(X1, X2))
(active#(adx(cons(X, Y))) -> cons#(X, adx(Y)), cons#(mark(X1), X2) -> cons#(X1, X2))
(active#(adx(cons(X, Y))) -> cons#(X, adx(Y)), cons#(X1, active(X2)) -> cons#(X1, X2))
(active#(adx(cons(X, Y))) -> cons#(X, adx(Y)), cons#(X1, mark(X2)) -> cons#(X1, X2))
(mark#(adx(X)) -> adx#(mark(X)), adx#(active(X)) -> adx#(X))
(mark#(adx(X)) -> adx#(mark(X)), adx#(mark(X)) -> adx#(X))
(mark#(incr(X)) -> incr#(mark(X)), incr#(active(X)) -> incr#(X))
(mark#(incr(X)) -> incr#(mark(X)), incr#(mark(X)) -> incr#(X))
(mark#(tl(X)) -> tl#(mark(X)), tl#(active(X)) -> tl#(X))
(mark#(tl(X)) -> tl#(mark(X)), tl#(mark(X)) -> tl#(X))
(cons#(X1, active(X2)) -> cons#(X1, X2), cons#(active(X1), X2) -> cons#(X1, X2))
(cons#(X1, active(X2)) -> cons#(X1, X2), cons#(mark(X1), X2) -> cons#(X1, X2))
(cons#(X1, active(X2)) -> cons#(X1, X2), cons#(X1, active(X2)) -> cons#(X1, X2))
(cons#(X1, active(X2)) -> cons#(X1, X2), cons#(X1, mark(X2)) -> cons#(X1, X2))
(cons#(active(X1), X2) -> cons#(X1, X2), cons#(active(X1), X2) -> cons#(X1, X2))
(cons#(active(X1), X2) -> cons#(X1, X2), cons#(mark(X1), X2) -> cons#(X1, X2))
(cons#(active(X1), X2) -> cons#(X1, X2), cons#(X1, active(X2)) -> cons#(X1, X2))
(cons#(active(X1), X2) -> cons#(X1, X2), cons#(X1, mark(X2)) -> cons#(X1, X2))
(mark#(cons(X1, X2)) -> active#(cons(X1, X2)), active#(adx(cons(X, Y))) -> mark#(incr(cons(X, adx(Y)))))
(mark#(cons(X1, X2)) -> active#(cons(X1, X2)), active#(adx(cons(X, Y))) -> adx#(Y))
(mark#(cons(X1, X2)) -> active#(cons(X1, X2)), active#(adx(cons(X, Y))) -> cons#(X, adx(Y)))
(mark#(cons(X1, X2)) -> active#(cons(X1, X2)), active#(adx(cons(X, Y))) -> incr#(cons(X, adx(Y))))
(mark#(cons(X1, X2)) -> active#(cons(X1, X2)), active#(incr(cons(X, Y))) -> mark#(cons(s(X), incr(Y))))
(mark#(cons(X1, X2)) -> active#(cons(X1, X2)), active#(incr(cons(X, Y))) -> cons#(s(X), incr(Y)))
(mark#(cons(X1, X2)) -> active#(cons(X1, X2)), active#(incr(cons(X, Y))) -> s#(X))
(mark#(cons(X1, X2)) -> active#(cons(X1, X2)), active#(incr(cons(X, Y))) -> incr#(Y))
(mark#(cons(X1, X2)) -> active#(cons(X1, X2)), active#(hd(cons(X, Y))) -> mark#(X))
(mark#(cons(X1, X2)) -> active#(cons(X1, X2)), active#(tl(cons(X, Y))) -> mark#(Y))
(cons#(mark(X1), X2) -> cons#(X1, X2), cons#(X1, mark(X2)) -> cons#(X1, X2))
(cons#(mark(X1), X2) -> cons#(X1, X2), cons#(X1, active(X2)) -> cons#(X1, X2))
(cons#(mark(X1), X2) -> cons#(X1, X2), cons#(mark(X1), X2) -> cons#(X1, X2))
(cons#(mark(X1), X2) -> cons#(X1, X2), cons#(active(X1), X2) -> cons#(X1, X2))
(cons#(X1, mark(X2)) -> cons#(X1, X2), cons#(X1, mark(X2)) -> cons#(X1, X2))
(cons#(X1, mark(X2)) -> cons#(X1, X2), cons#(X1, active(X2)) -> cons#(X1, X2))
(cons#(X1, mark(X2)) -> cons#(X1, X2), cons#(mark(X1), X2) -> cons#(X1, X2))
(cons#(X1, mark(X2)) -> cons#(X1, X2), cons#(active(X1), X2) -> cons#(X1, X2))
(mark#(hd(X)) -> hd#(mark(X)), hd#(mark(X)) -> hd#(X))
(mark#(hd(X)) -> hd#(mark(X)), hd#(active(X)) -> hd#(X))
(mark#(s(X)) -> active#(s(X)), active#(adx(cons(X, Y))) -> mark#(incr(cons(X, adx(Y)))))
(mark#(s(X)) -> active#(s(X)), active#(adx(cons(X, Y))) -> adx#(Y))
(mark#(s(X)) -> active#(s(X)), active#(adx(cons(X, Y))) -> cons#(X, adx(Y)))
(mark#(s(X)) -> active#(s(X)), active#(adx(cons(X, Y))) -> incr#(cons(X, adx(Y))))
(mark#(s(X)) -> active#(s(X)), active#(incr(cons(X, Y))) -> mark#(cons(s(X), incr(Y))))
(mark#(s(X)) -> active#(s(X)), active#(incr(cons(X, Y))) -> cons#(s(X), incr(Y)))
(mark#(s(X)) -> active#(s(X)), active#(incr(cons(X, Y))) -> s#(X))
(mark#(s(X)) -> active#(s(X)), active#(incr(cons(X, Y))) -> incr#(Y))
(mark#(s(X)) -> active#(s(X)), active#(hd(cons(X, Y))) -> mark#(X))
(mark#(s(X)) -> active#(s(X)), active#(tl(cons(X, Y))) -> mark#(Y))
(active#(incr(cons(X, Y))) -> cons#(s(X), incr(Y)), cons#(X1, mark(X2)) -> cons#(X1, X2))
(active#(incr(cons(X, Y))) -> cons#(s(X), incr(Y)), cons#(X1, active(X2)) -> cons#(X1, X2))
(active#(incr(cons(X, Y))) -> cons#(s(X), incr(Y)), cons#(mark(X1), X2) -> cons#(X1, X2))
(active#(incr(cons(X, Y))) -> cons#(s(X), incr(Y)), cons#(active(X1), X2) -> cons#(X1, X2))
(active#(incr(cons(X, Y))) -> mark#(cons(s(X), incr(Y))), mark#(adx(X)) -> mark#(X))
(active#(incr(cons(X, Y))) -> mark#(cons(s(X), incr(Y))), mark#(adx(X)) -> adx#(mark(X)))
(active#(incr(cons(X, Y))) -> mark#(cons(s(X), incr(Y))), mark#(adx(X)) -> active#(adx(mark(X))))
(active#(incr(cons(X, Y))) -> mark#(cons(s(X), incr(Y))), mark#(cons(X1, X2)) -> active#(cons(X1, X2)))
(active#(incr(cons(X, Y))) -> mark#(cons(s(X), incr(Y))), mark#(s(X)) -> active#(s(X)))
(active#(incr(cons(X, Y))) -> mark#(cons(s(X), incr(Y))), mark#(incr(X)) -> mark#(X))
(active#(incr(cons(X, Y))) -> mark#(cons(s(X), incr(Y))), mark#(incr(X)) -> active#(incr(mark(X))))
(active#(incr(cons(X, Y))) -> mark#(cons(s(X), incr(Y))), mark#(incr(X)) -> incr#(mark(X)))
(active#(incr(cons(X, Y))) -> mark#(cons(s(X), incr(Y))), mark#(hd(X)) -> mark#(X))
(active#(incr(cons(X, Y))) -> mark#(cons(s(X), incr(Y))), mark#(hd(X)) -> active#(hd(mark(X))))
(active#(incr(cons(X, Y))) -> mark#(cons(s(X), incr(Y))), mark#(hd(X)) -> hd#(mark(X)))
(active#(incr(cons(X, Y))) -> mark#(cons(s(X), incr(Y))), mark#(tl(X)) -> mark#(X))
(active#(incr(cons(X, Y))) -> mark#(cons(s(X), incr(Y))), mark#(tl(X)) -> active#(tl(mark(X))))
(active#(incr(cons(X, Y))) -> mark#(cons(s(X), incr(Y))), mark#(tl(X)) -> tl#(mark(X)))
(active#(adx(cons(X, Y))) -> incr#(cons(X, adx(Y))), incr#(mark(X)) -> incr#(X))
(active#(adx(cons(X, Y))) -> incr#(cons(X, adx(Y))), incr#(active(X)) -> incr#(X))
(active#(incr(cons(X, Y))) -> incr#(Y), incr#(mark(X)) -> incr#(X))
(active#(incr(cons(X, Y))) -> incr#(Y), incr#(active(X)) -> incr#(X))
(mark#(nats()) -> active#(nats()), active#(nats()) -> mark#(adx(zeros())))
(mark#(nats()) -> active#(nats()), active#(nats()) -> adx#(zeros()))
(tl#(active(X)) -> tl#(X), tl#(mark(X)) -> tl#(X))
(tl#(active(X)) -> tl#(X), tl#(active(X)) -> tl#(X))
(hd#(active(X)) -> hd#(X), hd#(mark(X)) -> hd#(X))
(hd#(active(X)) -> hd#(X), hd#(active(X)) -> hd#(X))
(incr#(active(X)) -> incr#(X), incr#(mark(X)) -> incr#(X))
(incr#(active(X)) -> incr#(X), incr#(active(X)) -> incr#(X))
(s#(active(X)) -> s#(X), s#(mark(X)) -> s#(X))
(s#(active(X)) -> s#(X), s#(active(X)) -> s#(X))
(active#(hd(cons(X, Y))) -> mark#(X), mark#(adx(X)) -> mark#(X))
(active#(hd(cons(X, Y))) -> mark#(X), mark#(adx(X)) -> adx#(mark(X)))
(active#(hd(cons(X, Y))) -> mark#(X), mark#(adx(X)) -> active#(adx(mark(X))))
(active#(hd(cons(X, Y))) -> mark#(X), mark#(zeros()) -> active#(zeros()))
(active#(hd(cons(X, Y))) -> mark#(X), mark#(nats()) -> active#(nats()))
(active#(hd(cons(X, Y))) -> mark#(X), mark#(cons(X1, X2)) -> active#(cons(X1, X2)))
(active#(hd(cons(X, Y))) -> mark#(X), mark#(0()) -> active#(0()))
(active#(hd(cons(X, Y))) -> mark#(X), mark#(s(X)) -> active#(s(X)))
(active#(hd(cons(X, Y))) -> mark#(X), mark#(incr(X)) -> mark#(X))
(active#(hd(cons(X, Y))) -> mark#(X), mark#(incr(X)) -> active#(incr(mark(X))))
(active#(hd(cons(X, Y))) -> mark#(X), mark#(incr(X)) -> incr#(mark(X)))
(active#(hd(cons(X, Y))) -> mark#(X), mark#(hd(X)) -> mark#(X))
(active#(hd(cons(X, Y))) -> mark#(X), mark#(hd(X)) -> active#(hd(mark(X))))
(active#(hd(cons(X, Y))) -> mark#(X), mark#(hd(X)) -> hd#(mark(X)))
(active#(hd(cons(X, Y))) -> mark#(X), mark#(tl(X)) -> mark#(X))
(active#(hd(cons(X, Y))) -> mark#(X), mark#(tl(X)) -> active#(tl(mark(X))))
(active#(hd(cons(X, Y))) -> mark#(X), mark#(tl(X)) -> tl#(mark(X)))
(adx#(active(X)) -> adx#(X), adx#(mark(X)) -> adx#(X))
(adx#(active(X)) -> adx#(X), adx#(active(X)) -> adx#(X))
(mark#(tl(X)) -> mark#(X), mark#(adx(X)) -> mark#(X))
(mark#(tl(X)) -> mark#(X), mark#(adx(X)) -> adx#(mark(X)))
(mark#(tl(X)) -> mark#(X), mark#(adx(X)) -> active#(adx(mark(X))))
(mark#(tl(X)) -> mark#(X), mark#(zeros()) -> active#(zeros()))
(mark#(tl(X)) -> mark#(X), mark#(nats()) -> active#(nats()))
(mark#(tl(X)) -> mark#(X), mark#(cons(X1, X2)) -> active#(cons(X1, X2)))
(mark#(tl(X)) -> mark#(X), mark#(0()) -> active#(0()))
(mark#(tl(X)) -> mark#(X), mark#(s(X)) -> active#(s(X)))
(mark#(tl(X)) -> mark#(X), mark#(incr(X)) -> mark#(X))
(mark#(tl(X)) -> mark#(X), mark#(incr(X)) -> active#(incr(mark(X))))
(mark#(tl(X)) -> mark#(X), mark#(incr(X)) -> incr#(mark(X)))
(mark#(tl(X)) -> mark#(X), mark#(hd(X)) -> mark#(X))
(mark#(tl(X)) -> mark#(X), mark#(hd(X)) -> active#(hd(mark(X))))
(mark#(tl(X)) -> mark#(X), mark#(hd(X)) -> hd#(mark(X)))
(mark#(tl(X)) -> mark#(X), mark#(tl(X)) -> mark#(X))
(mark#(tl(X)) -> mark#(X), mark#(tl(X)) -> active#(tl(mark(X))))
(mark#(tl(X)) -> mark#(X), mark#(tl(X)) -> tl#(mark(X)))
(mark#(incr(X)) -> mark#(X), mark#(adx(X)) -> mark#(X))
(mark#(incr(X)) -> mark#(X), mark#(adx(X)) -> adx#(mark(X)))
(mark#(incr(X)) -> mark#(X), mark#(adx(X)) -> active#(adx(mark(X))))
(mark#(incr(X)) -> mark#(X), mark#(zeros()) -> active#(zeros()))
(mark#(incr(X)) -> mark#(X), mark#(nats()) -> active#(nats()))
(mark#(incr(X)) -> mark#(X), mark#(cons(X1, X2)) -> active#(cons(X1, X2)))
(mark#(incr(X)) -> mark#(X), mark#(0()) -> active#(0()))
(mark#(incr(X)) -> mark#(X), mark#(s(X)) -> active#(s(X)))
(mark#(incr(X)) -> mark#(X), mark#(incr(X)) -> mark#(X))
(mark#(incr(X)) -> mark#(X), mark#(incr(X)) -> active#(incr(mark(X))))
(mark#(incr(X)) -> mark#(X), mark#(incr(X)) -> incr#(mark(X)))
(mark#(incr(X)) -> mark#(X), mark#(hd(X)) -> mark#(X))
(mark#(incr(X)) -> mark#(X), mark#(hd(X)) -> active#(hd(mark(X))))
(mark#(incr(X)) -> mark#(X), mark#(hd(X)) -> hd#(mark(X)))
(mark#(incr(X)) -> mark#(X), mark#(tl(X)) -> mark#(X))
(mark#(incr(X)) -> mark#(X), mark#(tl(X)) -> active#(tl(mark(X))))
(mark#(incr(X)) -> mark#(X), mark#(tl(X)) -> tl#(mark(X)))
(active#(adx(cons(X, Y))) -> mark#(incr(cons(X, adx(Y)))), mark#(adx(X)) -> mark#(X))
(active#(adx(cons(X, Y))) -> mark#(incr(cons(X, adx(Y)))), mark#(adx(X)) -> adx#(mark(X)))
(active#(adx(cons(X, Y))) -> mark#(incr(cons(X, adx(Y)))), mark#(adx(X)) -> active#(adx(mark(X))))
(active#(adx(cons(X, Y))) -> mark#(incr(cons(X, adx(Y)))), mark#(cons(X1, X2)) -> active#(cons(X1, X2)))
(active#(adx(cons(X, Y))) -> mark#(incr(cons(X, adx(Y)))), mark#(s(X)) -> active#(s(X)))
(active#(adx(cons(X, Y))) -> mark#(incr(cons(X, adx(Y)))), mark#(incr(X)) -> mark#(X))
(active#(adx(cons(X, Y))) -> mark#(incr(cons(X, adx(Y)))), mark#(incr(X)) -> active#(incr(mark(X))))
(active#(adx(cons(X, Y))) -> mark#(incr(cons(X, adx(Y)))), mark#(incr(X)) -> incr#(mark(X)))
(active#(adx(cons(X, Y))) -> mark#(incr(cons(X, adx(Y)))), mark#(hd(X)) -> mark#(X))
(active#(adx(cons(X, Y))) -> mark#(incr(cons(X, adx(Y)))), mark#(hd(X)) -> active#(hd(mark(X))))
(active#(adx(cons(X, Y))) -> mark#(incr(cons(X, adx(Y)))), mark#(hd(X)) -> hd#(mark(X)))
(active#(adx(cons(X, Y))) -> mark#(incr(cons(X, adx(Y)))), mark#(tl(X)) -> mark#(X))
(active#(adx(cons(X, Y))) -> mark#(incr(cons(X, adx(Y)))), mark#(tl(X)) -> active#(tl(mark(X))))
(active#(adx(cons(X, Y))) -> mark#(incr(cons(X, adx(Y)))), mark#(tl(X)) -> tl#(mark(X)))
(mark#(hd(X)) -> active#(hd(mark(X))), active#(adx(cons(X, Y))) -> mark#(incr(cons(X, adx(Y)))))
(mark#(hd(X)) -> active#(hd(mark(X))), active#(adx(cons(X, Y))) -> adx#(Y))
(mark#(hd(X)) -> active#(hd(mark(X))), active#(adx(cons(X, Y))) -> cons#(X, adx(Y)))
(mark#(hd(X)) -> active#(hd(mark(X))), active#(adx(cons(X, Y))) -> incr#(cons(X, adx(Y))))
(mark#(hd(X)) -> active#(hd(mark(X))), active#(incr(cons(X, Y))) -> mark#(cons(s(X), incr(Y))))
(mark#(hd(X)) -> active#(hd(mark(X))), active#(incr(cons(X, Y))) -> cons#(s(X), incr(Y)))
(mark#(hd(X)) -> active#(hd(mark(X))), active#(incr(cons(X, Y))) -> s#(X))
(mark#(hd(X)) -> active#(hd(mark(X))), active#(incr(cons(X, Y))) -> incr#(Y))
(mark#(hd(X)) -> active#(hd(mark(X))), active#(hd(cons(X, Y))) -> mark#(X))
(mark#(hd(X)) -> active#(hd(mark(X))), active#(tl(cons(X, Y))) -> mark#(Y))
(mark#(adx(X)) -> active#(adx(mark(X))), active#(adx(cons(X, Y))) -> mark#(incr(cons(X, adx(Y)))))
(mark#(adx(X)) -> active#(adx(mark(X))), active#(adx(cons(X, Y))) -> adx#(Y))
(mark#(adx(X)) -> active#(adx(mark(X))), active#(adx(cons(X, Y))) -> cons#(X, adx(Y)))
(mark#(adx(X)) -> active#(adx(mark(X))), active#(adx(cons(X, Y))) -> incr#(cons(X, adx(Y))))
(mark#(adx(X)) -> active#(adx(mark(X))), active#(incr(cons(X, Y))) -> mark#(cons(s(X), incr(Y))))
(mark#(adx(X)) -> active#(adx(mark(X))), active#(incr(cons(X, Y))) -> cons#(s(X), incr(Y)))
(mark#(adx(X)) -> active#(adx(mark(X))), active#(incr(cons(X, Y))) -> s#(X))
(mark#(adx(X)) -> active#(adx(mark(X))), active#(incr(cons(X, Y))) -> incr#(Y))
(mark#(adx(X)) -> active#(adx(mark(X))), active#(hd(cons(X, Y))) -> mark#(X))
(mark#(adx(X)) -> active#(adx(mark(X))), active#(tl(cons(X, Y))) -> mark#(Y))
}
SCCS:
Scc:
{ tl#(mark(X)) -> tl#(X),
tl#(active(X)) -> tl#(X)}
Scc:
{ hd#(mark(X)) -> hd#(X),
hd#(active(X)) -> hd#(X)}
Scc:
{ incr#(mark(X)) -> incr#(X),
incr#(active(X)) -> incr#(X)}
Scc:
{ s#(mark(X)) -> s#(X),
s#(active(X)) -> s#(X)}
Scc:
{ cons#(X1, mark(X2)) -> cons#(X1, X2),
cons#(X1, active(X2)) -> cons#(X1, X2),
cons#(mark(X1), X2) -> cons#(X1, X2),
cons#(active(X1), X2) -> cons#(X1, X2)}
Scc:
{ adx#(mark(X)) -> adx#(X),
adx#(active(X)) -> adx#(X)}
Scc:
{ mark#(adx(X)) -> mark#(X),
mark#(adx(X)) -> active#(adx(mark(X))),
mark#(zeros()) -> active#(zeros()),
mark#(nats()) -> active#(nats()),
mark#(cons(X1, X2)) -> active#(cons(X1, X2)),
mark#(s(X)) -> active#(s(X)),
mark#(incr(X)) -> mark#(X),
mark#(incr(X)) -> active#(incr(mark(X))),
mark#(hd(X)) -> mark#(X),
mark#(hd(X)) -> active#(hd(mark(X))),
mark#(tl(X)) -> mark#(X),
mark#(tl(X)) -> active#(tl(mark(X))),
active#(adx(cons(X, Y))) -> mark#(incr(cons(X, adx(Y)))),
active#(zeros()) -> mark#(cons(0(), zeros())),
active#(nats()) -> mark#(adx(zeros())),
active#(incr(cons(X, Y))) -> mark#(cons(s(X), incr(Y))),
active#(hd(cons(X, Y))) -> mark#(X),
active#(tl(cons(X, Y))) -> mark#(Y)}
SCC:
Strict:
{ tl#(mark(X)) -> tl#(X),
tl#(active(X)) -> tl#(X)}
Weak:
{ mark(adx(X)) -> active(adx(mark(X))),
mark(zeros()) -> active(zeros()),
mark(nats()) -> active(nats()),
mark(cons(X1, X2)) -> active(cons(X1, X2)),
mark(0()) -> active(0()),
mark(s(X)) -> active(s(X)),
mark(incr(X)) -> active(incr(mark(X))),
mark(hd(X)) -> active(hd(mark(X))),
mark(tl(X)) -> active(tl(mark(X))),
adx(mark(X)) -> adx(X),
adx(active(X)) -> adx(X),
active(adx(cons(X, Y))) -> mark(incr(cons(X, adx(Y)))),
active(zeros()) -> mark(cons(0(), zeros())),
active(nats()) -> mark(adx(zeros())),
active(incr(cons(X, Y))) -> mark(cons(s(X), incr(Y))),
active(hd(cons(X, Y))) -> mark(X),
active(tl(cons(X, Y))) -> mark(Y),
cons(X1, mark(X2)) -> cons(X1, X2),
cons(X1, active(X2)) -> cons(X1, X2),
cons(mark(X1), X2) -> cons(X1, X2),
cons(active(X1), X2) -> cons(X1, X2),
s(mark(X)) -> s(X),
s(active(X)) -> s(X),
incr(mark(X)) -> incr(X),
incr(active(X)) -> incr(X),
hd(mark(X)) -> hd(X),
hd(active(X)) -> hd(X),
tl(mark(X)) -> tl(X),
tl(active(X)) -> tl(X)}
SPSC:
Simple Projection:
pi(tl#) = 0
Strict:
{tl#(active(X)) -> tl#(X)}
EDG:
{(tl#(active(X)) -> tl#(X), tl#(active(X)) -> tl#(X))}
SCCS:
Scc:
{tl#(active(X)) -> tl#(X)}
SCC:
Strict:
{tl#(active(X)) -> tl#(X)}
Weak:
{ mark(adx(X)) -> active(adx(mark(X))),
mark(zeros()) -> active(zeros()),
mark(nats()) -> active(nats()),
mark(cons(X1, X2)) -> active(cons(X1, X2)),
mark(0()) -> active(0()),
mark(s(X)) -> active(s(X)),
mark(incr(X)) -> active(incr(mark(X))),
mark(hd(X)) -> active(hd(mark(X))),
mark(tl(X)) -> active(tl(mark(X))),
adx(mark(X)) -> adx(X),
adx(active(X)) -> adx(X),
active(adx(cons(X, Y))) -> mark(incr(cons(X, adx(Y)))),
active(zeros()) -> mark(cons(0(), zeros())),
active(nats()) -> mark(adx(zeros())),
active(incr(cons(X, Y))) -> mark(cons(s(X), incr(Y))),
active(hd(cons(X, Y))) -> mark(X),
active(tl(cons(X, Y))) -> mark(Y),
cons(X1, mark(X2)) -> cons(X1, X2),
cons(X1, active(X2)) -> cons(X1, X2),
cons(mark(X1), X2) -> cons(X1, X2),
cons(active(X1), X2) -> cons(X1, X2),
s(mark(X)) -> s(X),
s(active(X)) -> s(X),
incr(mark(X)) -> incr(X),
incr(active(X)) -> incr(X),
hd(mark(X)) -> hd(X),
hd(active(X)) -> hd(X),
tl(mark(X)) -> tl(X),
tl(active(X)) -> tl(X)}
SPSC:
Simple Projection:
pi(tl#) = 0
Strict:
{}
Qed
SCC:
Strict:
{ hd#(mark(X)) -> hd#(X),
hd#(active(X)) -> hd#(X)}
Weak:
{ mark(adx(X)) -> active(adx(mark(X))),
mark(zeros()) -> active(zeros()),
mark(nats()) -> active(nats()),
mark(cons(X1, X2)) -> active(cons(X1, X2)),
mark(0()) -> active(0()),
mark(s(X)) -> active(s(X)),
mark(incr(X)) -> active(incr(mark(X))),
mark(hd(X)) -> active(hd(mark(X))),
mark(tl(X)) -> active(tl(mark(X))),
adx(mark(X)) -> adx(X),
adx(active(X)) -> adx(X),
active(adx(cons(X, Y))) -> mark(incr(cons(X, adx(Y)))),
active(zeros()) -> mark(cons(0(), zeros())),
active(nats()) -> mark(adx(zeros())),
active(incr(cons(X, Y))) -> mark(cons(s(X), incr(Y))),
active(hd(cons(X, Y))) -> mark(X),
active(tl(cons(X, Y))) -> mark(Y),
cons(X1, mark(X2)) -> cons(X1, X2),
cons(X1, active(X2)) -> cons(X1, X2),
cons(mark(X1), X2) -> cons(X1, X2),
cons(active(X1), X2) -> cons(X1, X2),
s(mark(X)) -> s(X),
s(active(X)) -> s(X),
incr(mark(X)) -> incr(X),
incr(active(X)) -> incr(X),
hd(mark(X)) -> hd(X),
hd(active(X)) -> hd(X),
tl(mark(X)) -> tl(X),
tl(active(X)) -> tl(X)}
SPSC:
Simple Projection:
pi(hd#) = 0
Strict:
{hd#(active(X)) -> hd#(X)}
EDG:
{(hd#(active(X)) -> hd#(X), hd#(active(X)) -> hd#(X))}
SCCS:
Scc:
{hd#(active(X)) -> hd#(X)}
SCC:
Strict:
{hd#(active(X)) -> hd#(X)}
Weak:
{ mark(adx(X)) -> active(adx(mark(X))),
mark(zeros()) -> active(zeros()),
mark(nats()) -> active(nats()),
mark(cons(X1, X2)) -> active(cons(X1, X2)),
mark(0()) -> active(0()),
mark(s(X)) -> active(s(X)),
mark(incr(X)) -> active(incr(mark(X))),
mark(hd(X)) -> active(hd(mark(X))),
mark(tl(X)) -> active(tl(mark(X))),
adx(mark(X)) -> adx(X),
adx(active(X)) -> adx(X),
active(adx(cons(X, Y))) -> mark(incr(cons(X, adx(Y)))),
active(zeros()) -> mark(cons(0(), zeros())),
active(nats()) -> mark(adx(zeros())),
active(incr(cons(X, Y))) -> mark(cons(s(X), incr(Y))),
active(hd(cons(X, Y))) -> mark(X),
active(tl(cons(X, Y))) -> mark(Y),
cons(X1, mark(X2)) -> cons(X1, X2),
cons(X1, active(X2)) -> cons(X1, X2),
cons(mark(X1), X2) -> cons(X1, X2),
cons(active(X1), X2) -> cons(X1, X2),
s(mark(X)) -> s(X),
s(active(X)) -> s(X),
incr(mark(X)) -> incr(X),
incr(active(X)) -> incr(X),
hd(mark(X)) -> hd(X),
hd(active(X)) -> hd(X),
tl(mark(X)) -> tl(X),
tl(active(X)) -> tl(X)}
SPSC:
Simple Projection:
pi(hd#) = 0
Strict:
{}
Qed
SCC:
Strict:
{ incr#(mark(X)) -> incr#(X),
incr#(active(X)) -> incr#(X)}
Weak:
{ mark(adx(X)) -> active(adx(mark(X))),
mark(zeros()) -> active(zeros()),
mark(nats()) -> active(nats()),
mark(cons(X1, X2)) -> active(cons(X1, X2)),
mark(0()) -> active(0()),
mark(s(X)) -> active(s(X)),
mark(incr(X)) -> active(incr(mark(X))),
mark(hd(X)) -> active(hd(mark(X))),
mark(tl(X)) -> active(tl(mark(X))),
adx(mark(X)) -> adx(X),
adx(active(X)) -> adx(X),
active(adx(cons(X, Y))) -> mark(incr(cons(X, adx(Y)))),
active(zeros()) -> mark(cons(0(), zeros())),
active(nats()) -> mark(adx(zeros())),
active(incr(cons(X, Y))) -> mark(cons(s(X), incr(Y))),
active(hd(cons(X, Y))) -> mark(X),
active(tl(cons(X, Y))) -> mark(Y),
cons(X1, mark(X2)) -> cons(X1, X2),
cons(X1, active(X2)) -> cons(X1, X2),
cons(mark(X1), X2) -> cons(X1, X2),
cons(active(X1), X2) -> cons(X1, X2),
s(mark(X)) -> s(X),
s(active(X)) -> s(X),
incr(mark(X)) -> incr(X),
incr(active(X)) -> incr(X),
hd(mark(X)) -> hd(X),
hd(active(X)) -> hd(X),
tl(mark(X)) -> tl(X),
tl(active(X)) -> tl(X)}
SPSC:
Simple Projection:
pi(incr#) = 0
Strict:
{incr#(active(X)) -> incr#(X)}
EDG:
{(incr#(active(X)) -> incr#(X), incr#(active(X)) -> incr#(X))}
SCCS:
Scc:
{incr#(active(X)) -> incr#(X)}
SCC:
Strict:
{incr#(active(X)) -> incr#(X)}
Weak:
{ mark(adx(X)) -> active(adx(mark(X))),
mark(zeros()) -> active(zeros()),
mark(nats()) -> active(nats()),
mark(cons(X1, X2)) -> active(cons(X1, X2)),
mark(0()) -> active(0()),
mark(s(X)) -> active(s(X)),
mark(incr(X)) -> active(incr(mark(X))),
mark(hd(X)) -> active(hd(mark(X))),
mark(tl(X)) -> active(tl(mark(X))),
adx(mark(X)) -> adx(X),
adx(active(X)) -> adx(X),
active(adx(cons(X, Y))) -> mark(incr(cons(X, adx(Y)))),
active(zeros()) -> mark(cons(0(), zeros())),
active(nats()) -> mark(adx(zeros())),
active(incr(cons(X, Y))) -> mark(cons(s(X), incr(Y))),
active(hd(cons(X, Y))) -> mark(X),
active(tl(cons(X, Y))) -> mark(Y),
cons(X1, mark(X2)) -> cons(X1, X2),
cons(X1, active(X2)) -> cons(X1, X2),
cons(mark(X1), X2) -> cons(X1, X2),
cons(active(X1), X2) -> cons(X1, X2),
s(mark(X)) -> s(X),
s(active(X)) -> s(X),
incr(mark(X)) -> incr(X),
incr(active(X)) -> incr(X),
hd(mark(X)) -> hd(X),
hd(active(X)) -> hd(X),
tl(mark(X)) -> tl(X),
tl(active(X)) -> tl(X)}
SPSC:
Simple Projection:
pi(incr#) = 0
Strict:
{}
Qed
SCC:
Strict:
{ s#(mark(X)) -> s#(X),
s#(active(X)) -> s#(X)}
Weak:
{ mark(adx(X)) -> active(adx(mark(X))),
mark(zeros()) -> active(zeros()),
mark(nats()) -> active(nats()),
mark(cons(X1, X2)) -> active(cons(X1, X2)),
mark(0()) -> active(0()),
mark(s(X)) -> active(s(X)),
mark(incr(X)) -> active(incr(mark(X))),
mark(hd(X)) -> active(hd(mark(X))),
mark(tl(X)) -> active(tl(mark(X))),
adx(mark(X)) -> adx(X),
adx(active(X)) -> adx(X),
active(adx(cons(X, Y))) -> mark(incr(cons(X, adx(Y)))),
active(zeros()) -> mark(cons(0(), zeros())),
active(nats()) -> mark(adx(zeros())),
active(incr(cons(X, Y))) -> mark(cons(s(X), incr(Y))),
active(hd(cons(X, Y))) -> mark(X),
active(tl(cons(X, Y))) -> mark(Y),
cons(X1, mark(X2)) -> cons(X1, X2),
cons(X1, active(X2)) -> cons(X1, X2),
cons(mark(X1), X2) -> cons(X1, X2),
cons(active(X1), X2) -> cons(X1, X2),
s(mark(X)) -> s(X),
s(active(X)) -> s(X),
incr(mark(X)) -> incr(X),
incr(active(X)) -> incr(X),
hd(mark(X)) -> hd(X),
hd(active(X)) -> hd(X),
tl(mark(X)) -> tl(X),
tl(active(X)) -> tl(X)}
SPSC:
Simple Projection:
pi(s#) = 0
Strict:
{s#(active(X)) -> s#(X)}
EDG:
{(s#(active(X)) -> s#(X), s#(active(X)) -> s#(X))}
SCCS:
Scc:
{s#(active(X)) -> s#(X)}
SCC:
Strict:
{s#(active(X)) -> s#(X)}
Weak:
{ mark(adx(X)) -> active(adx(mark(X))),
mark(zeros()) -> active(zeros()),
mark(nats()) -> active(nats()),
mark(cons(X1, X2)) -> active(cons(X1, X2)),
mark(0()) -> active(0()),
mark(s(X)) -> active(s(X)),
mark(incr(X)) -> active(incr(mark(X))),
mark(hd(X)) -> active(hd(mark(X))),
mark(tl(X)) -> active(tl(mark(X))),
adx(mark(X)) -> adx(X),
adx(active(X)) -> adx(X),
active(adx(cons(X, Y))) -> mark(incr(cons(X, adx(Y)))),
active(zeros()) -> mark(cons(0(), zeros())),
active(nats()) -> mark(adx(zeros())),
active(incr(cons(X, Y))) -> mark(cons(s(X), incr(Y))),
active(hd(cons(X, Y))) -> mark(X),
active(tl(cons(X, Y))) -> mark(Y),
cons(X1, mark(X2)) -> cons(X1, X2),
cons(X1, active(X2)) -> cons(X1, X2),
cons(mark(X1), X2) -> cons(X1, X2),
cons(active(X1), X2) -> cons(X1, X2),
s(mark(X)) -> s(X),
s(active(X)) -> s(X),
incr(mark(X)) -> incr(X),
incr(active(X)) -> incr(X),
hd(mark(X)) -> hd(X),
hd(active(X)) -> hd(X),
tl(mark(X)) -> tl(X),
tl(active(X)) -> tl(X)}
SPSC:
Simple Projection:
pi(s#) = 0
Strict:
{}
Qed
SCC:
Strict:
{ cons#(X1, mark(X2)) -> cons#(X1, X2),
cons#(X1, active(X2)) -> cons#(X1, X2),
cons#(mark(X1), X2) -> cons#(X1, X2),
cons#(active(X1), X2) -> cons#(X1, X2)}
Weak:
{ mark(adx(X)) -> active(adx(mark(X))),
mark(zeros()) -> active(zeros()),
mark(nats()) -> active(nats()),
mark(cons(X1, X2)) -> active(cons(X1, X2)),
mark(0()) -> active(0()),
mark(s(X)) -> active(s(X)),
mark(incr(X)) -> active(incr(mark(X))),
mark(hd(X)) -> active(hd(mark(X))),
mark(tl(X)) -> active(tl(mark(X))),
adx(mark(X)) -> adx(X),
adx(active(X)) -> adx(X),
active(adx(cons(X, Y))) -> mark(incr(cons(X, adx(Y)))),
active(zeros()) -> mark(cons(0(), zeros())),
active(nats()) -> mark(adx(zeros())),
active(incr(cons(X, Y))) -> mark(cons(s(X), incr(Y))),
active(hd(cons(X, Y))) -> mark(X),
active(tl(cons(X, Y))) -> mark(Y),
cons(X1, mark(X2)) -> cons(X1, X2),
cons(X1, active(X2)) -> cons(X1, X2),
cons(mark(X1), X2) -> cons(X1, X2),
cons(active(X1), X2) -> cons(X1, X2),
s(mark(X)) -> s(X),
s(active(X)) -> s(X),
incr(mark(X)) -> incr(X),
incr(active(X)) -> incr(X),
hd(mark(X)) -> hd(X),
hd(active(X)) -> hd(X),
tl(mark(X)) -> tl(X),
tl(active(X)) -> tl(X)}
SPSC:
Simple Projection:
pi(cons#) = 0
Strict:
{ cons#(X1, mark(X2)) -> cons#(X1, X2),
cons#(X1, active(X2)) -> cons#(X1, X2),
cons#(mark(X1), X2) -> cons#(X1, X2)}
EDG:
{(cons#(X1, active(X2)) -> cons#(X1, X2), cons#(mark(X1), X2) -> cons#(X1, X2))
(cons#(X1, active(X2)) -> cons#(X1, X2), cons#(X1, active(X2)) -> cons#(X1, X2))
(cons#(X1, active(X2)) -> cons#(X1, X2), cons#(X1, mark(X2)) -> cons#(X1, X2))
(cons#(mark(X1), X2) -> cons#(X1, X2), cons#(X1, mark(X2)) -> cons#(X1, X2))
(cons#(mark(X1), X2) -> cons#(X1, X2), cons#(X1, active(X2)) -> cons#(X1, X2))
(cons#(mark(X1), X2) -> cons#(X1, X2), cons#(mark(X1), X2) -> cons#(X1, X2))
(cons#(X1, mark(X2)) -> cons#(X1, X2), cons#(X1, mark(X2)) -> cons#(X1, X2))
(cons#(X1, mark(X2)) -> cons#(X1, X2), cons#(X1, active(X2)) -> cons#(X1, X2))
(cons#(X1, mark(X2)) -> cons#(X1, X2), cons#(mark(X1), X2) -> cons#(X1, X2))}
SCCS:
Scc:
{ cons#(X1, mark(X2)) -> cons#(X1, X2),
cons#(X1, active(X2)) -> cons#(X1, X2),
cons#(mark(X1), X2) -> cons#(X1, X2)}
SCC:
Strict:
{ cons#(X1, mark(X2)) -> cons#(X1, X2),
cons#(X1, active(X2)) -> cons#(X1, X2),
cons#(mark(X1), X2) -> cons#(X1, X2)}
Weak:
{ mark(adx(X)) -> active(adx(mark(X))),
mark(zeros()) -> active(zeros()),
mark(nats()) -> active(nats()),
mark(cons(X1, X2)) -> active(cons(X1, X2)),
mark(0()) -> active(0()),
mark(s(X)) -> active(s(X)),
mark(incr(X)) -> active(incr(mark(X))),
mark(hd(X)) -> active(hd(mark(X))),
mark(tl(X)) -> active(tl(mark(X))),
adx(mark(X)) -> adx(X),
adx(active(X)) -> adx(X),
active(adx(cons(X, Y))) -> mark(incr(cons(X, adx(Y)))),
active(zeros()) -> mark(cons(0(), zeros())),
active(nats()) -> mark(adx(zeros())),
active(incr(cons(X, Y))) -> mark(cons(s(X), incr(Y))),
active(hd(cons(X, Y))) -> mark(X),
active(tl(cons(X, Y))) -> mark(Y),
cons(X1, mark(X2)) -> cons(X1, X2),
cons(X1, active(X2)) -> cons(X1, X2),
cons(mark(X1), X2) -> cons(X1, X2),
cons(active(X1), X2) -> cons(X1, X2),
s(mark(X)) -> s(X),
s(active(X)) -> s(X),
incr(mark(X)) -> incr(X),
incr(active(X)) -> incr(X),
hd(mark(X)) -> hd(X),
hd(active(X)) -> hd(X),
tl(mark(X)) -> tl(X),
tl(active(X)) -> tl(X)}
SPSC:
Simple Projection:
pi(cons#) = 0
Strict:
{ cons#(X1, mark(X2)) -> cons#(X1, X2),
cons#(X1, active(X2)) -> cons#(X1, X2)}
EDG:
{(cons#(X1, active(X2)) -> cons#(X1, X2), cons#(X1, active(X2)) -> cons#(X1, X2))
(cons#(X1, active(X2)) -> cons#(X1, X2), cons#(X1, mark(X2)) -> cons#(X1, X2))
(cons#(X1, mark(X2)) -> cons#(X1, X2), cons#(X1, mark(X2)) -> cons#(X1, X2))
(cons#(X1, mark(X2)) -> cons#(X1, X2), cons#(X1, active(X2)) -> cons#(X1, X2))}
SCCS:
Scc:
{ cons#(X1, mark(X2)) -> cons#(X1, X2),
cons#(X1, active(X2)) -> cons#(X1, X2)}
SCC:
Strict:
{ cons#(X1, mark(X2)) -> cons#(X1, X2),
cons#(X1, active(X2)) -> cons#(X1, X2)}
Weak:
{ mark(adx(X)) -> active(adx(mark(X))),
mark(zeros()) -> active(zeros()),
mark(nats()) -> active(nats()),
mark(cons(X1, X2)) -> active(cons(X1, X2)),
mark(0()) -> active(0()),
mark(s(X)) -> active(s(X)),
mark(incr(X)) -> active(incr(mark(X))),
mark(hd(X)) -> active(hd(mark(X))),
mark(tl(X)) -> active(tl(mark(X))),
adx(mark(X)) -> adx(X),
adx(active(X)) -> adx(X),
active(adx(cons(X, Y))) -> mark(incr(cons(X, adx(Y)))),
active(zeros()) -> mark(cons(0(), zeros())),
active(nats()) -> mark(adx(zeros())),
active(incr(cons(X, Y))) -> mark(cons(s(X), incr(Y))),
active(hd(cons(X, Y))) -> mark(X),
active(tl(cons(X, Y))) -> mark(Y),
cons(X1, mark(X2)) -> cons(X1, X2),
cons(X1, active(X2)) -> cons(X1, X2),
cons(mark(X1), X2) -> cons(X1, X2),
cons(active(X1), X2) -> cons(X1, X2),
s(mark(X)) -> s(X),
s(active(X)) -> s(X),
incr(mark(X)) -> incr(X),
incr(active(X)) -> incr(X),
hd(mark(X)) -> hd(X),
hd(active(X)) -> hd(X),
tl(mark(X)) -> tl(X),
tl(active(X)) -> tl(X)}
SPSC:
Simple Projection:
pi(cons#) = 1
Strict:
{cons#(X1, active(X2)) -> cons#(X1, X2)}
EDG:
{(cons#(X1, active(X2)) -> cons#(X1, X2), cons#(X1, active(X2)) -> cons#(X1, X2))}
SCCS:
Scc:
{cons#(X1, active(X2)) -> cons#(X1, X2)}
SCC:
Strict:
{cons#(X1, active(X2)) -> cons#(X1, X2)}
Weak:
{ mark(adx(X)) -> active(adx(mark(X))),
mark(zeros()) -> active(zeros()),
mark(nats()) -> active(nats()),
mark(cons(X1, X2)) -> active(cons(X1, X2)),
mark(0()) -> active(0()),
mark(s(X)) -> active(s(X)),
mark(incr(X)) -> active(incr(mark(X))),
mark(hd(X)) -> active(hd(mark(X))),
mark(tl(X)) -> active(tl(mark(X))),
adx(mark(X)) -> adx(X),
adx(active(X)) -> adx(X),
active(adx(cons(X, Y))) -> mark(incr(cons(X, adx(Y)))),
active(zeros()) -> mark(cons(0(), zeros())),
active(nats()) -> mark(adx(zeros())),
active(incr(cons(X, Y))) -> mark(cons(s(X), incr(Y))),
active(hd(cons(X, Y))) -> mark(X),
active(tl(cons(X, Y))) -> mark(Y),
cons(X1, mark(X2)) -> cons(X1, X2),
cons(X1, active(X2)) -> cons(X1, X2),
cons(mark(X1), X2) -> cons(X1, X2),
cons(active(X1), X2) -> cons(X1, X2),
s(mark(X)) -> s(X),
s(active(X)) -> s(X),
incr(mark(X)) -> incr(X),
incr(active(X)) -> incr(X),
hd(mark(X)) -> hd(X),
hd(active(X)) -> hd(X),
tl(mark(X)) -> tl(X),
tl(active(X)) -> tl(X)}
SPSC:
Simple Projection:
pi(cons#) = 1
Strict:
{}
Qed
SCC:
Strict:
{ adx#(mark(X)) -> adx#(X),
adx#(active(X)) -> adx#(X)}
Weak:
{ mark(adx(X)) -> active(adx(mark(X))),
mark(zeros()) -> active(zeros()),
mark(nats()) -> active(nats()),
mark(cons(X1, X2)) -> active(cons(X1, X2)),
mark(0()) -> active(0()),
mark(s(X)) -> active(s(X)),
mark(incr(X)) -> active(incr(mark(X))),
mark(hd(X)) -> active(hd(mark(X))),
mark(tl(X)) -> active(tl(mark(X))),
adx(mark(X)) -> adx(X),
adx(active(X)) -> adx(X),
active(adx(cons(X, Y))) -> mark(incr(cons(X, adx(Y)))),
active(zeros()) -> mark(cons(0(), zeros())),
active(nats()) -> mark(adx(zeros())),
active(incr(cons(X, Y))) -> mark(cons(s(X), incr(Y))),
active(hd(cons(X, Y))) -> mark(X),
active(tl(cons(X, Y))) -> mark(Y),
cons(X1, mark(X2)) -> cons(X1, X2),
cons(X1, active(X2)) -> cons(X1, X2),
cons(mark(X1), X2) -> cons(X1, X2),
cons(active(X1), X2) -> cons(X1, X2),
s(mark(X)) -> s(X),
s(active(X)) -> s(X),
incr(mark(X)) -> incr(X),
incr(active(X)) -> incr(X),
hd(mark(X)) -> hd(X),
hd(active(X)) -> hd(X),
tl(mark(X)) -> tl(X),
tl(active(X)) -> tl(X)}
SPSC:
Simple Projection:
pi(adx#) = 0
Strict:
{adx#(mark(X)) -> adx#(X)}
EDG:
{(adx#(mark(X)) -> adx#(X), adx#(mark(X)) -> adx#(X))}
SCCS:
Scc:
{adx#(mark(X)) -> adx#(X)}
SCC:
Strict:
{adx#(mark(X)) -> adx#(X)}
Weak:
{ mark(adx(X)) -> active(adx(mark(X))),
mark(zeros()) -> active(zeros()),
mark(nats()) -> active(nats()),
mark(cons(X1, X2)) -> active(cons(X1, X2)),
mark(0()) -> active(0()),
mark(s(X)) -> active(s(X)),
mark(incr(X)) -> active(incr(mark(X))),
mark(hd(X)) -> active(hd(mark(X))),
mark(tl(X)) -> active(tl(mark(X))),
adx(mark(X)) -> adx(X),
adx(active(X)) -> adx(X),
active(adx(cons(X, Y))) -> mark(incr(cons(X, adx(Y)))),
active(zeros()) -> mark(cons(0(), zeros())),
active(nats()) -> mark(adx(zeros())),
active(incr(cons(X, Y))) -> mark(cons(s(X), incr(Y))),
active(hd(cons(X, Y))) -> mark(X),
active(tl(cons(X, Y))) -> mark(Y),
cons(X1, mark(X2)) -> cons(X1, X2),
cons(X1, active(X2)) -> cons(X1, X2),
cons(mark(X1), X2) -> cons(X1, X2),
cons(active(X1), X2) -> cons(X1, X2),
s(mark(X)) -> s(X),
s(active(X)) -> s(X),
incr(mark(X)) -> incr(X),
incr(active(X)) -> incr(X),
hd(mark(X)) -> hd(X),
hd(active(X)) -> hd(X),
tl(mark(X)) -> tl(X),
tl(active(X)) -> tl(X)}
SPSC:
Simple Projection:
pi(adx#) = 0
Strict:
{}
Qed
SCC:
Strict:
{ mark#(adx(X)) -> mark#(X),
mark#(adx(X)) -> active#(adx(mark(X))),
mark#(zeros()) -> active#(zeros()),
mark#(nats()) -> active#(nats()),
mark#(cons(X1, X2)) -> active#(cons(X1, X2)),
mark#(s(X)) -> active#(s(X)),
mark#(incr(X)) -> mark#(X),
mark#(incr(X)) -> active#(incr(mark(X))),
mark#(hd(X)) -> mark#(X),
mark#(hd(X)) -> active#(hd(mark(X))),
mark#(tl(X)) -> mark#(X),
mark#(tl(X)) -> active#(tl(mark(X))),
active#(adx(cons(X, Y))) -> mark#(incr(cons(X, adx(Y)))),
active#(zeros()) -> mark#(cons(0(), zeros())),
active#(nats()) -> mark#(adx(zeros())),
active#(incr(cons(X, Y))) -> mark#(cons(s(X), incr(Y))),
active#(hd(cons(X, Y))) -> mark#(X),
active#(tl(cons(X, Y))) -> mark#(Y)}
Weak:
{ mark(adx(X)) -> active(adx(mark(X))),
mark(zeros()) -> active(zeros()),
mark(nats()) -> active(nats()),
mark(cons(X1, X2)) -> active(cons(X1, X2)),
mark(0()) -> active(0()),
mark(s(X)) -> active(s(X)),
mark(incr(X)) -> active(incr(mark(X))),
mark(hd(X)) -> active(hd(mark(X))),
mark(tl(X)) -> active(tl(mark(X))),
adx(mark(X)) -> adx(X),
adx(active(X)) -> adx(X),
active(adx(cons(X, Y))) -> mark(incr(cons(X, adx(Y)))),
active(zeros()) -> mark(cons(0(), zeros())),
active(nats()) -> mark(adx(zeros())),
active(incr(cons(X, Y))) -> mark(cons(s(X), incr(Y))),
active(hd(cons(X, Y))) -> mark(X),
active(tl(cons(X, Y))) -> mark(Y),
cons(X1, mark(X2)) -> cons(X1, X2),
cons(X1, active(X2)) -> cons(X1, X2),
cons(mark(X1), X2) -> cons(X1, X2),
cons(active(X1), X2) -> cons(X1, X2),
s(mark(X)) -> s(X),
s(active(X)) -> s(X),
incr(mark(X)) -> incr(X),
incr(active(X)) -> incr(X),
hd(mark(X)) -> hd(X),
hd(active(X)) -> hd(X),
tl(mark(X)) -> tl(X),
tl(active(X)) -> tl(X)}
POLY:
Argument Filtering:
pi(tl) = [], pi(hd) = [], pi(incr) = [], pi(s) = [], pi(0) = [], pi(cons) = [], pi(nats) = [], pi(active#) = 0, pi(active) = [], pi(zeros) = [], pi(adx) = [], pi(mark#) = [], pi(mark) = []
Usable Rules:
{}
Interpretation:
[mark#] = 1,
[cons] = 0,
[tl] = 1,
[hd] = 1,
[incr] = 1,
[s] = 0,
[adx] = 1,
[nats] = 1,
[zeros] = 1
Strict:
{ mark#(adx(X)) -> mark#(X),
mark#(adx(X)) -> active#(adx(mark(X))),
mark#(zeros()) -> active#(zeros()),
mark#(nats()) -> active#(nats()),
mark#(incr(X)) -> mark#(X),
mark#(incr(X)) -> active#(incr(mark(X))),
mark#(hd(X)) -> mark#(X),
mark#(hd(X)) -> active#(hd(mark(X))),
mark#(tl(X)) -> mark#(X),
mark#(tl(X)) -> active#(tl(mark(X))),
active#(adx(cons(X, Y))) -> mark#(incr(cons(X, adx(Y)))),
active#(zeros()) -> mark#(cons(0(), zeros())),
active#(nats()) -> mark#(adx(zeros())),
active#(incr(cons(X, Y))) -> mark#(cons(s(X), incr(Y))),
active#(hd(cons(X, Y))) -> mark#(X),
active#(tl(cons(X, Y))) -> mark#(Y)}
Weak:
{ mark(adx(X)) -> active(adx(mark(X))),
mark(zeros()) -> active(zeros()),
mark(nats()) -> active(nats()),
mark(cons(X1, X2)) -> active(cons(X1, X2)),
mark(0()) -> active(0()),
mark(s(X)) -> active(s(X)),
mark(incr(X)) -> active(incr(mark(X))),
mark(hd(X)) -> active(hd(mark(X))),
mark(tl(X)) -> active(tl(mark(X))),
adx(mark(X)) -> adx(X),
adx(active(X)) -> adx(X),
active(adx(cons(X, Y))) -> mark(incr(cons(X, adx(Y)))),
active(zeros()) -> mark(cons(0(), zeros())),
active(nats()) -> mark(adx(zeros())),
active(incr(cons(X, Y))) -> mark(cons(s(X), incr(Y))),
active(hd(cons(X, Y))) -> mark(X),
active(tl(cons(X, Y))) -> mark(Y),
cons(X1, mark(X2)) -> cons(X1, X2),
cons(X1, active(X2)) -> cons(X1, X2),
cons(mark(X1), X2) -> cons(X1, X2),
cons(active(X1), X2) -> cons(X1, X2),
s(mark(X)) -> s(X),
s(active(X)) -> s(X),
incr(mark(X)) -> incr(X),
incr(active(X)) -> incr(X),
hd(mark(X)) -> hd(X),
hd(active(X)) -> hd(X),
tl(mark(X)) -> tl(X),
tl(active(X)) -> tl(X)}
EDG:
{(mark#(zeros()) -> active#(zeros()), active#(zeros()) -> mark#(cons(0(), zeros())))
(mark#(adx(X)) -> active#(adx(mark(X))), active#(tl(cons(X, Y))) -> mark#(Y))
(mark#(adx(X)) -> active#(adx(mark(X))), active#(hd(cons(X, Y))) -> mark#(X))
(mark#(adx(X)) -> active#(adx(mark(X))), active#(incr(cons(X, Y))) -> mark#(cons(s(X), incr(Y))))
(mark#(adx(X)) -> active#(adx(mark(X))), active#(adx(cons(X, Y))) -> mark#(incr(cons(X, adx(Y)))))
(mark#(hd(X)) -> active#(hd(mark(X))), active#(tl(cons(X, Y))) -> mark#(Y))
(mark#(hd(X)) -> active#(hd(mark(X))), active#(hd(cons(X, Y))) -> mark#(X))
(mark#(hd(X)) -> active#(hd(mark(X))), active#(incr(cons(X, Y))) -> mark#(cons(s(X), incr(Y))))
(mark#(hd(X)) -> active#(hd(mark(X))), active#(adx(cons(X, Y))) -> mark#(incr(cons(X, adx(Y)))))
(active#(adx(cons(X, Y))) -> mark#(incr(cons(X, adx(Y)))), mark#(tl(X)) -> active#(tl(mark(X))))
(active#(adx(cons(X, Y))) -> mark#(incr(cons(X, adx(Y)))), mark#(tl(X)) -> mark#(X))
(active#(adx(cons(X, Y))) -> mark#(incr(cons(X, adx(Y)))), mark#(hd(X)) -> active#(hd(mark(X))))
(active#(adx(cons(X, Y))) -> mark#(incr(cons(X, adx(Y)))), mark#(hd(X)) -> mark#(X))
(active#(adx(cons(X, Y))) -> mark#(incr(cons(X, adx(Y)))), mark#(incr(X)) -> active#(incr(mark(X))))
(active#(adx(cons(X, Y))) -> mark#(incr(cons(X, adx(Y)))), mark#(incr(X)) -> mark#(X))
(active#(adx(cons(X, Y))) -> mark#(incr(cons(X, adx(Y)))), mark#(adx(X)) -> active#(adx(mark(X))))
(active#(adx(cons(X, Y))) -> mark#(incr(cons(X, adx(Y)))), mark#(adx(X)) -> mark#(X))
(mark#(adx(X)) -> mark#(X), mark#(tl(X)) -> active#(tl(mark(X))))
(mark#(adx(X)) -> mark#(X), mark#(tl(X)) -> mark#(X))
(mark#(adx(X)) -> mark#(X), mark#(hd(X)) -> active#(hd(mark(X))))
(mark#(adx(X)) -> mark#(X), mark#(hd(X)) -> mark#(X))
(mark#(adx(X)) -> mark#(X), mark#(incr(X)) -> active#(incr(mark(X))))
(mark#(adx(X)) -> mark#(X), mark#(incr(X)) -> mark#(X))
(mark#(adx(X)) -> mark#(X), mark#(nats()) -> active#(nats()))
(mark#(adx(X)) -> mark#(X), mark#(zeros()) -> active#(zeros()))
(mark#(adx(X)) -> mark#(X), mark#(adx(X)) -> active#(adx(mark(X))))
(mark#(adx(X)) -> mark#(X), mark#(adx(X)) -> mark#(X))
(mark#(hd(X)) -> mark#(X), mark#(tl(X)) -> active#(tl(mark(X))))
(mark#(hd(X)) -> mark#(X), mark#(tl(X)) -> mark#(X))
(mark#(hd(X)) -> mark#(X), mark#(hd(X)) -> active#(hd(mark(X))))
(mark#(hd(X)) -> mark#(X), mark#(hd(X)) -> mark#(X))
(mark#(hd(X)) -> mark#(X), mark#(incr(X)) -> active#(incr(mark(X))))
(mark#(hd(X)) -> mark#(X), mark#(incr(X)) -> mark#(X))
(mark#(hd(X)) -> mark#(X), mark#(nats()) -> active#(nats()))
(mark#(hd(X)) -> mark#(X), mark#(zeros()) -> active#(zeros()))
(mark#(hd(X)) -> mark#(X), mark#(adx(X)) -> active#(adx(mark(X))))
(mark#(hd(X)) -> mark#(X), mark#(adx(X)) -> mark#(X))
(active#(hd(cons(X, Y))) -> mark#(X), mark#(tl(X)) -> active#(tl(mark(X))))
(active#(hd(cons(X, Y))) -> mark#(X), mark#(tl(X)) -> mark#(X))
(active#(hd(cons(X, Y))) -> mark#(X), mark#(hd(X)) -> active#(hd(mark(X))))
(active#(hd(cons(X, Y))) -> mark#(X), mark#(hd(X)) -> mark#(X))
(active#(hd(cons(X, Y))) -> mark#(X), mark#(incr(X)) -> active#(incr(mark(X))))
(active#(hd(cons(X, Y))) -> mark#(X), mark#(incr(X)) -> mark#(X))
(active#(hd(cons(X, Y))) -> mark#(X), mark#(nats()) -> active#(nats()))
(active#(hd(cons(X, Y))) -> mark#(X), mark#(zeros()) -> active#(zeros()))
(active#(hd(cons(X, Y))) -> mark#(X), mark#(adx(X)) -> active#(adx(mark(X))))
(active#(hd(cons(X, Y))) -> mark#(X), mark#(adx(X)) -> mark#(X))
(mark#(tl(X)) -> mark#(X), mark#(adx(X)) -> mark#(X))
(mark#(tl(X)) -> mark#(X), mark#(adx(X)) -> active#(adx(mark(X))))
(mark#(tl(X)) -> mark#(X), mark#(zeros()) -> active#(zeros()))
(mark#(tl(X)) -> mark#(X), mark#(nats()) -> active#(nats()))
(mark#(tl(X)) -> mark#(X), mark#(incr(X)) -> mark#(X))
(mark#(tl(X)) -> mark#(X), mark#(incr(X)) -> active#(incr(mark(X))))
(mark#(tl(X)) -> mark#(X), mark#(hd(X)) -> mark#(X))
(mark#(tl(X)) -> mark#(X), mark#(hd(X)) -> active#(hd(mark(X))))
(mark#(tl(X)) -> mark#(X), mark#(tl(X)) -> mark#(X))
(mark#(tl(X)) -> mark#(X), mark#(tl(X)) -> active#(tl(mark(X))))
(mark#(incr(X)) -> mark#(X), mark#(adx(X)) -> mark#(X))
(mark#(incr(X)) -> mark#(X), mark#(adx(X)) -> active#(adx(mark(X))))
(mark#(incr(X)) -> mark#(X), mark#(zeros()) -> active#(zeros()))
(mark#(incr(X)) -> mark#(X), mark#(nats()) -> active#(nats()))
(mark#(incr(X)) -> mark#(X), mark#(incr(X)) -> mark#(X))
(mark#(incr(X)) -> mark#(X), mark#(incr(X)) -> active#(incr(mark(X))))
(mark#(incr(X)) -> mark#(X), mark#(hd(X)) -> mark#(X))
(mark#(incr(X)) -> mark#(X), mark#(hd(X)) -> active#(hd(mark(X))))
(mark#(incr(X)) -> mark#(X), mark#(tl(X)) -> mark#(X))
(mark#(incr(X)) -> mark#(X), mark#(tl(X)) -> active#(tl(mark(X))))
(active#(incr(cons(X, Y))) -> mark#(cons(s(X), incr(Y))), mark#(adx(X)) -> mark#(X))
(active#(incr(cons(X, Y))) -> mark#(cons(s(X), incr(Y))), mark#(adx(X)) -> active#(adx(mark(X))))
(active#(incr(cons(X, Y))) -> mark#(cons(s(X), incr(Y))), mark#(incr(X)) -> mark#(X))
(active#(incr(cons(X, Y))) -> mark#(cons(s(X), incr(Y))), mark#(incr(X)) -> active#(incr(mark(X))))
(active#(incr(cons(X, Y))) -> mark#(cons(s(X), incr(Y))), mark#(hd(X)) -> mark#(X))
(active#(incr(cons(X, Y))) -> mark#(cons(s(X), incr(Y))), mark#(hd(X)) -> active#(hd(mark(X))))
(active#(incr(cons(X, Y))) -> mark#(cons(s(X), incr(Y))), mark#(tl(X)) -> mark#(X))
(active#(incr(cons(X, Y))) -> mark#(cons(s(X), incr(Y))), mark#(tl(X)) -> active#(tl(mark(X))))
(active#(nats()) -> mark#(adx(zeros())), mark#(adx(X)) -> mark#(X))
(active#(nats()) -> mark#(adx(zeros())), mark#(adx(X)) -> active#(adx(mark(X))))
(mark#(tl(X)) -> active#(tl(mark(X))), active#(adx(cons(X, Y))) -> mark#(incr(cons(X, adx(Y)))))
(mark#(tl(X)) -> active#(tl(mark(X))), active#(incr(cons(X, Y))) -> mark#(cons(s(X), incr(Y))))
(mark#(tl(X)) -> active#(tl(mark(X))), active#(hd(cons(X, Y))) -> mark#(X))
(mark#(tl(X)) -> active#(tl(mark(X))), active#(tl(cons(X, Y))) -> mark#(Y))
(mark#(incr(X)) -> active#(incr(mark(X))), active#(adx(cons(X, Y))) -> mark#(incr(cons(X, adx(Y)))))
(mark#(incr(X)) -> active#(incr(mark(X))), active#(incr(cons(X, Y))) -> mark#(cons(s(X), incr(Y))))
(mark#(incr(X)) -> active#(incr(mark(X))), active#(hd(cons(X, Y))) -> mark#(X))
(mark#(incr(X)) -> active#(incr(mark(X))), active#(tl(cons(X, Y))) -> mark#(Y))
(mark#(nats()) -> active#(nats()), active#(nats()) -> mark#(adx(zeros())))
(active#(tl(cons(X, Y))) -> mark#(Y), mark#(adx(X)) -> mark#(X))
(active#(tl(cons(X, Y))) -> mark#(Y), mark#(adx(X)) -> active#(adx(mark(X))))
(active#(tl(cons(X, Y))) -> mark#(Y), mark#(zeros()) -> active#(zeros()))
(active#(tl(cons(X, Y))) -> mark#(Y), mark#(nats()) -> active#(nats()))
(active#(tl(cons(X, Y))) -> mark#(Y), mark#(incr(X)) -> mark#(X))
(active#(tl(cons(X, Y))) -> mark#(Y), mark#(incr(X)) -> active#(incr(mark(X))))
(active#(tl(cons(X, Y))) -> mark#(Y), mark#(hd(X)) -> mark#(X))
(active#(tl(cons(X, Y))) -> mark#(Y), mark#(hd(X)) -> active#(hd(mark(X))))
(active#(tl(cons(X, Y))) -> mark#(Y), mark#(tl(X)) -> mark#(X))
(active#(tl(cons(X, Y))) -> mark#(Y), mark#(tl(X)) -> active#(tl(mark(X))))}
SCCS:
Scc:
{ mark#(adx(X)) -> mark#(X),
mark#(adx(X)) -> active#(adx(mark(X))),
mark#(nats()) -> active#(nats()),
mark#(incr(X)) -> mark#(X),
mark#(incr(X)) -> active#(incr(mark(X))),
mark#(hd(X)) -> mark#(X),
mark#(hd(X)) -> active#(hd(mark(X))),
mark#(tl(X)) -> mark#(X),
mark#(tl(X)) -> active#(tl(mark(X))),
active#(adx(cons(X, Y))) -> mark#(incr(cons(X, adx(Y)))),
active#(nats()) -> mark#(adx(zeros())),
active#(incr(cons(X, Y))) -> mark#(cons(s(X), incr(Y))),
active#(hd(cons(X, Y))) -> mark#(X),
active#(tl(cons(X, Y))) -> mark#(Y)}
SCC:
Strict:
{ mark#(adx(X)) -> mark#(X),
mark#(adx(X)) -> active#(adx(mark(X))),
mark#(nats()) -> active#(nats()),
mark#(incr(X)) -> mark#(X),
mark#(incr(X)) -> active#(incr(mark(X))),
mark#(hd(X)) -> mark#(X),
mark#(hd(X)) -> active#(hd(mark(X))),
mark#(tl(X)) -> mark#(X),
mark#(tl(X)) -> active#(tl(mark(X))),
active#(adx(cons(X, Y))) -> mark#(incr(cons(X, adx(Y)))),
active#(nats()) -> mark#(adx(zeros())),
active#(incr(cons(X, Y))) -> mark#(cons(s(X), incr(Y))),
active#(hd(cons(X, Y))) -> mark#(X),
active#(tl(cons(X, Y))) -> mark#(Y)}
Weak:
{ mark(adx(X)) -> active(adx(mark(X))),
mark(zeros()) -> active(zeros()),
mark(nats()) -> active(nats()),
mark(cons(X1, X2)) -> active(cons(X1, X2)),
mark(0()) -> active(0()),
mark(s(X)) -> active(s(X)),
mark(incr(X)) -> active(incr(mark(X))),
mark(hd(X)) -> active(hd(mark(X))),
mark(tl(X)) -> active(tl(mark(X))),
adx(mark(X)) -> adx(X),
adx(active(X)) -> adx(X),
active(adx(cons(X, Y))) -> mark(incr(cons(X, adx(Y)))),
active(zeros()) -> mark(cons(0(), zeros())),
active(nats()) -> mark(adx(zeros())),
active(incr(cons(X, Y))) -> mark(cons(s(X), incr(Y))),
active(hd(cons(X, Y))) -> mark(X),
active(tl(cons(X, Y))) -> mark(Y),
cons(X1, mark(X2)) -> cons(X1, X2),
cons(X1, active(X2)) -> cons(X1, X2),
cons(mark(X1), X2) -> cons(X1, X2),
cons(active(X1), X2) -> cons(X1, X2),
s(mark(X)) -> s(X),
s(active(X)) -> s(X),
incr(mark(X)) -> incr(X),
incr(active(X)) -> incr(X),
hd(mark(X)) -> hd(X),
hd(active(X)) -> hd(X),
tl(mark(X)) -> tl(X),
tl(active(X)) -> tl(X)}
POLY:
Argument Filtering:
pi(tl) = [0], pi(hd) = 0, pi(incr) = 0, pi(s) = [], pi(0) = [], pi(cons) = [0,1], pi(nats) = [], pi(active#) = 0, pi(active) = 0, pi(zeros) = [], pi(adx) = 0, pi(mark#) = 0, pi(mark) = 0
Usable Rules:
{}
Interpretation:
[cons](x0, x1) = x0 + x1,
[tl](x0) = x0 + 1,
[s] = 0,
[nats] = 0,
[zeros] = 0
Strict:
{ mark#(adx(X)) -> mark#(X),
mark#(adx(X)) -> active#(adx(mark(X))),
mark#(nats()) -> active#(nats()),
mark#(incr(X)) -> mark#(X),
mark#(incr(X)) -> active#(incr(mark(X))),
mark#(hd(X)) -> mark#(X),
mark#(hd(X)) -> active#(hd(mark(X))),
mark#(tl(X)) -> active#(tl(mark(X))),
active#(adx(cons(X, Y))) -> mark#(incr(cons(X, adx(Y)))),
active#(nats()) -> mark#(adx(zeros())),
active#(incr(cons(X, Y))) -> mark#(cons(s(X), incr(Y))),
active#(hd(cons(X, Y))) -> mark#(X)}
Weak:
{ mark(adx(X)) -> active(adx(mark(X))),
mark(zeros()) -> active(zeros()),
mark(nats()) -> active(nats()),
mark(cons(X1, X2)) -> active(cons(X1, X2)),
mark(0()) -> active(0()),
mark(s(X)) -> active(s(X)),
mark(incr(X)) -> active(incr(mark(X))),
mark(hd(X)) -> active(hd(mark(X))),
mark(tl(X)) -> active(tl(mark(X))),
adx(mark(X)) -> adx(X),
adx(active(X)) -> adx(X),
active(adx(cons(X, Y))) -> mark(incr(cons(X, adx(Y)))),
active(zeros()) -> mark(cons(0(), zeros())),
active(nats()) -> mark(adx(zeros())),
active(incr(cons(X, Y))) -> mark(cons(s(X), incr(Y))),
active(hd(cons(X, Y))) -> mark(X),
active(tl(cons(X, Y))) -> mark(Y),
cons(X1, mark(X2)) -> cons(X1, X2),
cons(X1, active(X2)) -> cons(X1, X2),
cons(mark(X1), X2) -> cons(X1, X2),
cons(active(X1), X2) -> cons(X1, X2),
s(mark(X)) -> s(X),
s(active(X)) -> s(X),
incr(mark(X)) -> incr(X),
incr(active(X)) -> incr(X),
hd(mark(X)) -> hd(X),
hd(active(X)) -> hd(X),
tl(mark(X)) -> tl(X),
tl(active(X)) -> tl(X)}
EDG:
{(mark#(incr(X)) -> active#(incr(mark(X))), active#(hd(cons(X, Y))) -> mark#(X))
(mark#(incr(X)) -> active#(incr(mark(X))), active#(incr(cons(X, Y))) -> mark#(cons(s(X), incr(Y))))
(mark#(incr(X)) -> active#(incr(mark(X))), active#(adx(cons(X, Y))) -> mark#(incr(cons(X, adx(Y)))))
(mark#(tl(X)) -> active#(tl(mark(X))), active#(hd(cons(X, Y))) -> mark#(X))
(mark#(tl(X)) -> active#(tl(mark(X))), active#(incr(cons(X, Y))) -> mark#(cons(s(X), incr(Y))))
(mark#(tl(X)) -> active#(tl(mark(X))), active#(adx(cons(X, Y))) -> mark#(incr(cons(X, adx(Y)))))
(mark#(nats()) -> active#(nats()), active#(nats()) -> mark#(adx(zeros())))
(mark#(incr(X)) -> mark#(X), mark#(tl(X)) -> active#(tl(mark(X))))
(mark#(incr(X)) -> mark#(X), mark#(hd(X)) -> active#(hd(mark(X))))
(mark#(incr(X)) -> mark#(X), mark#(hd(X)) -> mark#(X))
(mark#(incr(X)) -> mark#(X), mark#(incr(X)) -> active#(incr(mark(X))))
(mark#(incr(X)) -> mark#(X), mark#(incr(X)) -> mark#(X))
(mark#(incr(X)) -> mark#(X), mark#(nats()) -> active#(nats()))
(mark#(incr(X)) -> mark#(X), mark#(adx(X)) -> active#(adx(mark(X))))
(mark#(incr(X)) -> mark#(X), mark#(adx(X)) -> mark#(X))
(active#(hd(cons(X, Y))) -> mark#(X), mark#(tl(X)) -> active#(tl(mark(X))))
(active#(hd(cons(X, Y))) -> mark#(X), mark#(hd(X)) -> active#(hd(mark(X))))
(active#(hd(cons(X, Y))) -> mark#(X), mark#(hd(X)) -> mark#(X))
(active#(hd(cons(X, Y))) -> mark#(X), mark#(incr(X)) -> active#(incr(mark(X))))
(active#(hd(cons(X, Y))) -> mark#(X), mark#(incr(X)) -> mark#(X))
(active#(hd(cons(X, Y))) -> mark#(X), mark#(nats()) -> active#(nats()))
(active#(hd(cons(X, Y))) -> mark#(X), mark#(adx(X)) -> active#(adx(mark(X))))
(active#(hd(cons(X, Y))) -> mark#(X), mark#(adx(X)) -> mark#(X))
(active#(nats()) -> mark#(adx(zeros())), mark#(adx(X)) -> active#(adx(mark(X))))
(active#(nats()) -> mark#(adx(zeros())), mark#(adx(X)) -> mark#(X))
(active#(incr(cons(X, Y))) -> mark#(cons(s(X), incr(Y))), mark#(adx(X)) -> mark#(X))
(active#(incr(cons(X, Y))) -> mark#(cons(s(X), incr(Y))), mark#(adx(X)) -> active#(adx(mark(X))))
(active#(incr(cons(X, Y))) -> mark#(cons(s(X), incr(Y))), mark#(incr(X)) -> mark#(X))
(active#(incr(cons(X, Y))) -> mark#(cons(s(X), incr(Y))), mark#(incr(X)) -> active#(incr(mark(X))))
(active#(incr(cons(X, Y))) -> mark#(cons(s(X), incr(Y))), mark#(hd(X)) -> mark#(X))
(active#(incr(cons(X, Y))) -> mark#(cons(s(X), incr(Y))), mark#(hd(X)) -> active#(hd(mark(X))))
(active#(incr(cons(X, Y))) -> mark#(cons(s(X), incr(Y))), mark#(tl(X)) -> active#(tl(mark(X))))
(mark#(hd(X)) -> mark#(X), mark#(adx(X)) -> mark#(X))
(mark#(hd(X)) -> mark#(X), mark#(adx(X)) -> active#(adx(mark(X))))
(mark#(hd(X)) -> mark#(X), mark#(nats()) -> active#(nats()))
(mark#(hd(X)) -> mark#(X), mark#(incr(X)) -> mark#(X))
(mark#(hd(X)) -> mark#(X), mark#(incr(X)) -> active#(incr(mark(X))))
(mark#(hd(X)) -> mark#(X), mark#(hd(X)) -> mark#(X))
(mark#(hd(X)) -> mark#(X), mark#(hd(X)) -> active#(hd(mark(X))))
(mark#(hd(X)) -> mark#(X), mark#(tl(X)) -> active#(tl(mark(X))))
(mark#(adx(X)) -> mark#(X), mark#(adx(X)) -> mark#(X))
(mark#(adx(X)) -> mark#(X), mark#(adx(X)) -> active#(adx(mark(X))))
(mark#(adx(X)) -> mark#(X), mark#(nats()) -> active#(nats()))
(mark#(adx(X)) -> mark#(X), mark#(incr(X)) -> mark#(X))
(mark#(adx(X)) -> mark#(X), mark#(incr(X)) -> active#(incr(mark(X))))
(mark#(adx(X)) -> mark#(X), mark#(hd(X)) -> mark#(X))
(mark#(adx(X)) -> mark#(X), mark#(hd(X)) -> active#(hd(mark(X))))
(mark#(adx(X)) -> mark#(X), mark#(tl(X)) -> active#(tl(mark(X))))
(active#(adx(cons(X, Y))) -> mark#(incr(cons(X, adx(Y)))), mark#(adx(X)) -> mark#(X))
(active#(adx(cons(X, Y))) -> mark#(incr(cons(X, adx(Y)))), mark#(adx(X)) -> active#(adx(mark(X))))
(active#(adx(cons(X, Y))) -> mark#(incr(cons(X, adx(Y)))), mark#(incr(X)) -> mark#(X))
(active#(adx(cons(X, Y))) -> mark#(incr(cons(X, adx(Y)))), mark#(incr(X)) -> active#(incr(mark(X))))
(active#(adx(cons(X, Y))) -> mark#(incr(cons(X, adx(Y)))), mark#(hd(X)) -> mark#(X))
(active#(adx(cons(X, Y))) -> mark#(incr(cons(X, adx(Y)))), mark#(hd(X)) -> active#(hd(mark(X))))
(active#(adx(cons(X, Y))) -> mark#(incr(cons(X, adx(Y)))), mark#(tl(X)) -> active#(tl(mark(X))))
(mark#(hd(X)) -> active#(hd(mark(X))), active#(adx(cons(X, Y))) -> mark#(incr(cons(X, adx(Y)))))
(mark#(hd(X)) -> active#(hd(mark(X))), active#(incr(cons(X, Y))) -> mark#(cons(s(X), incr(Y))))
(mark#(hd(X)) -> active#(hd(mark(X))), active#(hd(cons(X, Y))) -> mark#(X))
(mark#(adx(X)) -> active#(adx(mark(X))), active#(adx(cons(X, Y))) -> mark#(incr(cons(X, adx(Y)))))
(mark#(adx(X)) -> active#(adx(mark(X))), active#(incr(cons(X, Y))) -> mark#(cons(s(X), incr(Y))))
(mark#(adx(X)) -> active#(adx(mark(X))), active#(hd(cons(X, Y))) -> mark#(X))}
SCCS:
Scc:
{ mark#(adx(X)) -> mark#(X),
mark#(adx(X)) -> active#(adx(mark(X))),
mark#(nats()) -> active#(nats()),
mark#(incr(X)) -> mark#(X),
mark#(incr(X)) -> active#(incr(mark(X))),
mark#(hd(X)) -> mark#(X),
mark#(hd(X)) -> active#(hd(mark(X))),
mark#(tl(X)) -> active#(tl(mark(X))),
active#(adx(cons(X, Y))) -> mark#(incr(cons(X, adx(Y)))),
active#(nats()) -> mark#(adx(zeros())),
active#(incr(cons(X, Y))) -> mark#(cons(s(X), incr(Y))),
active#(hd(cons(X, Y))) -> mark#(X)}
SCC:
Strict:
{ mark#(adx(X)) -> mark#(X),
mark#(adx(X)) -> active#(adx(mark(X))),
mark#(nats()) -> active#(nats()),
mark#(incr(X)) -> mark#(X),
mark#(incr(X)) -> active#(incr(mark(X))),
mark#(hd(X)) -> mark#(X),
mark#(hd(X)) -> active#(hd(mark(X))),
mark#(tl(X)) -> active#(tl(mark(X))),
active#(adx(cons(X, Y))) -> mark#(incr(cons(X, adx(Y)))),
active#(nats()) -> mark#(adx(zeros())),
active#(incr(cons(X, Y))) -> mark#(cons(s(X), incr(Y))),
active#(hd(cons(X, Y))) -> mark#(X)}
Weak:
{ mark(adx(X)) -> active(adx(mark(X))),
mark(zeros()) -> active(zeros()),
mark(nats()) -> active(nats()),
mark(cons(X1, X2)) -> active(cons(X1, X2)),
mark(0()) -> active(0()),
mark(s(X)) -> active(s(X)),
mark(incr(X)) -> active(incr(mark(X))),
mark(hd(X)) -> active(hd(mark(X))),
mark(tl(X)) -> active(tl(mark(X))),
adx(mark(X)) -> adx(X),
adx(active(X)) -> adx(X),
active(adx(cons(X, Y))) -> mark(incr(cons(X, adx(Y)))),
active(zeros()) -> mark(cons(0(), zeros())),
active(nats()) -> mark(adx(zeros())),
active(incr(cons(X, Y))) -> mark(cons(s(X), incr(Y))),
active(hd(cons(X, Y))) -> mark(X),
active(tl(cons(X, Y))) -> mark(Y),
cons(X1, mark(X2)) -> cons(X1, X2),
cons(X1, active(X2)) -> cons(X1, X2),
cons(mark(X1), X2) -> cons(X1, X2),
cons(active(X1), X2) -> cons(X1, X2),
s(mark(X)) -> s(X),
s(active(X)) -> s(X),
incr(mark(X)) -> incr(X),
incr(active(X)) -> incr(X),
hd(mark(X)) -> hd(X),
hd(active(X)) -> hd(X),
tl(mark(X)) -> tl(X),
tl(active(X)) -> tl(X)}
POLY:
Argument Filtering:
pi(tl) = 0, pi(hd) = 0, pi(incr) = 0, pi(s) = 0, pi(0) = [], pi(cons) = [0,1], pi(nats) = [], pi(active#) = 0, pi(active) = 0, pi(zeros) = [], pi(adx) = 0, pi(mark#) = 0, pi(mark) = 0
Usable Rules:
{}
Interpretation:
[cons](x0, x1) = x0 + x1,
[nats] = 1,
[zeros] = 0
Strict:
{ mark#(adx(X)) -> mark#(X),
mark#(adx(X)) -> active#(adx(mark(X))),
mark#(nats()) -> active#(nats()),
mark#(incr(X)) -> mark#(X),
mark#(incr(X)) -> active#(incr(mark(X))),
mark#(hd(X)) -> mark#(X),
mark#(hd(X)) -> active#(hd(mark(X))),
mark#(tl(X)) -> active#(tl(mark(X))),
active#(adx(cons(X, Y))) -> mark#(incr(cons(X, adx(Y)))),
active#(incr(cons(X, Y))) -> mark#(cons(s(X), incr(Y))),
active#(hd(cons(X, Y))) -> mark#(X)}
Weak:
{ mark(adx(X)) -> active(adx(mark(X))),
mark(zeros()) -> active(zeros()),
mark(nats()) -> active(nats()),
mark(cons(X1, X2)) -> active(cons(X1, X2)),
mark(0()) -> active(0()),
mark(s(X)) -> active(s(X)),
mark(incr(X)) -> active(incr(mark(X))),
mark(hd(X)) -> active(hd(mark(X))),
mark(tl(X)) -> active(tl(mark(X))),
adx(mark(X)) -> adx(X),
adx(active(X)) -> adx(X),
active(adx(cons(X, Y))) -> mark(incr(cons(X, adx(Y)))),
active(zeros()) -> mark(cons(0(), zeros())),
active(nats()) -> mark(adx(zeros())),
active(incr(cons(X, Y))) -> mark(cons(s(X), incr(Y))),
active(hd(cons(X, Y))) -> mark(X),
active(tl(cons(X, Y))) -> mark(Y),
cons(X1, mark(X2)) -> cons(X1, X2),
cons(X1, active(X2)) -> cons(X1, X2),
cons(mark(X1), X2) -> cons(X1, X2),
cons(active(X1), X2) -> cons(X1, X2),
s(mark(X)) -> s(X),
s(active(X)) -> s(X),
incr(mark(X)) -> incr(X),
incr(active(X)) -> incr(X),
hd(mark(X)) -> hd(X),
hd(active(X)) -> hd(X),
tl(mark(X)) -> tl(X),
tl(active(X)) -> tl(X)}
EDG:
{(mark#(incr(X)) -> mark#(X), mark#(tl(X)) -> active#(tl(mark(X))))
(mark#(incr(X)) -> mark#(X), mark#(hd(X)) -> active#(hd(mark(X))))
(mark#(incr(X)) -> mark#(X), mark#(hd(X)) -> mark#(X))
(mark#(incr(X)) -> mark#(X), mark#(incr(X)) -> active#(incr(mark(X))))
(mark#(incr(X)) -> mark#(X), mark#(incr(X)) -> mark#(X))
(mark#(incr(X)) -> mark#(X), mark#(nats()) -> active#(nats()))
(mark#(incr(X)) -> mark#(X), mark#(adx(X)) -> active#(adx(mark(X))))
(mark#(incr(X)) -> mark#(X), mark#(adx(X)) -> mark#(X))
(active#(hd(cons(X, Y))) -> mark#(X), mark#(tl(X)) -> active#(tl(mark(X))))
(active#(hd(cons(X, Y))) -> mark#(X), mark#(hd(X)) -> active#(hd(mark(X))))
(active#(hd(cons(X, Y))) -> mark#(X), mark#(hd(X)) -> mark#(X))
(active#(hd(cons(X, Y))) -> mark#(X), mark#(incr(X)) -> active#(incr(mark(X))))
(active#(hd(cons(X, Y))) -> mark#(X), mark#(incr(X)) -> mark#(X))
(active#(hd(cons(X, Y))) -> mark#(X), mark#(nats()) -> active#(nats()))
(active#(hd(cons(X, Y))) -> mark#(X), mark#(adx(X)) -> active#(adx(mark(X))))
(active#(hd(cons(X, Y))) -> mark#(X), mark#(adx(X)) -> mark#(X))
(mark#(incr(X)) -> active#(incr(mark(X))), active#(hd(cons(X, Y))) -> mark#(X))
(mark#(incr(X)) -> active#(incr(mark(X))), active#(incr(cons(X, Y))) -> mark#(cons(s(X), incr(Y))))
(mark#(incr(X)) -> active#(incr(mark(X))), active#(adx(cons(X, Y))) -> mark#(incr(cons(X, adx(Y)))))
(mark#(tl(X)) -> active#(tl(mark(X))), active#(hd(cons(X, Y))) -> mark#(X))
(mark#(tl(X)) -> active#(tl(mark(X))), active#(incr(cons(X, Y))) -> mark#(cons(s(X), incr(Y))))
(mark#(tl(X)) -> active#(tl(mark(X))), active#(adx(cons(X, Y))) -> mark#(incr(cons(X, adx(Y)))))
(active#(incr(cons(X, Y))) -> mark#(cons(s(X), incr(Y))), mark#(tl(X)) -> active#(tl(mark(X))))
(active#(incr(cons(X, Y))) -> mark#(cons(s(X), incr(Y))), mark#(hd(X)) -> active#(hd(mark(X))))
(active#(incr(cons(X, Y))) -> mark#(cons(s(X), incr(Y))), mark#(hd(X)) -> mark#(X))
(active#(incr(cons(X, Y))) -> mark#(cons(s(X), incr(Y))), mark#(incr(X)) -> active#(incr(mark(X))))
(active#(incr(cons(X, Y))) -> mark#(cons(s(X), incr(Y))), mark#(incr(X)) -> mark#(X))
(active#(incr(cons(X, Y))) -> mark#(cons(s(X), incr(Y))), mark#(adx(X)) -> active#(adx(mark(X))))
(active#(incr(cons(X, Y))) -> mark#(cons(s(X), incr(Y))), mark#(adx(X)) -> mark#(X))
(active#(adx(cons(X, Y))) -> mark#(incr(cons(X, adx(Y)))), mark#(adx(X)) -> mark#(X))
(active#(adx(cons(X, Y))) -> mark#(incr(cons(X, adx(Y)))), mark#(adx(X)) -> active#(adx(mark(X))))
(active#(adx(cons(X, Y))) -> mark#(incr(cons(X, adx(Y)))), mark#(incr(X)) -> mark#(X))
(active#(adx(cons(X, Y))) -> mark#(incr(cons(X, adx(Y)))), mark#(incr(X)) -> active#(incr(mark(X))))
(active#(adx(cons(X, Y))) -> mark#(incr(cons(X, adx(Y)))), mark#(hd(X)) -> mark#(X))
(active#(adx(cons(X, Y))) -> mark#(incr(cons(X, adx(Y)))), mark#(hd(X)) -> active#(hd(mark(X))))
(active#(adx(cons(X, Y))) -> mark#(incr(cons(X, adx(Y)))), mark#(tl(X)) -> active#(tl(mark(X))))
(mark#(hd(X)) -> active#(hd(mark(X))), active#(adx(cons(X, Y))) -> mark#(incr(cons(X, adx(Y)))))
(mark#(hd(X)) -> active#(hd(mark(X))), active#(incr(cons(X, Y))) -> mark#(cons(s(X), incr(Y))))
(mark#(hd(X)) -> active#(hd(mark(X))), active#(hd(cons(X, Y))) -> mark#(X))
(mark#(adx(X)) -> active#(adx(mark(X))), active#(adx(cons(X, Y))) -> mark#(incr(cons(X, adx(Y)))))
(mark#(adx(X)) -> active#(adx(mark(X))), active#(incr(cons(X, Y))) -> mark#(cons(s(X), incr(Y))))
(mark#(adx(X)) -> active#(adx(mark(X))), active#(hd(cons(X, Y))) -> mark#(X))
(mark#(hd(X)) -> mark#(X), mark#(adx(X)) -> mark#(X))
(mark#(hd(X)) -> mark#(X), mark#(adx(X)) -> active#(adx(mark(X))))
(mark#(hd(X)) -> mark#(X), mark#(nats()) -> active#(nats()))
(mark#(hd(X)) -> mark#(X), mark#(incr(X)) -> mark#(X))
(mark#(hd(X)) -> mark#(X), mark#(incr(X)) -> active#(incr(mark(X))))
(mark#(hd(X)) -> mark#(X), mark#(hd(X)) -> mark#(X))
(mark#(hd(X)) -> mark#(X), mark#(hd(X)) -> active#(hd(mark(X))))
(mark#(hd(X)) -> mark#(X), mark#(tl(X)) -> active#(tl(mark(X))))
(mark#(adx(X)) -> mark#(X), mark#(adx(X)) -> mark#(X))
(mark#(adx(X)) -> mark#(X), mark#(adx(X)) -> active#(adx(mark(X))))
(mark#(adx(X)) -> mark#(X), mark#(nats()) -> active#(nats()))
(mark#(adx(X)) -> mark#(X), mark#(incr(X)) -> mark#(X))
(mark#(adx(X)) -> mark#(X), mark#(incr(X)) -> active#(incr(mark(X))))
(mark#(adx(X)) -> mark#(X), mark#(hd(X)) -> mark#(X))
(mark#(adx(X)) -> mark#(X), mark#(hd(X)) -> active#(hd(mark(X))))
(mark#(adx(X)) -> mark#(X), mark#(tl(X)) -> active#(tl(mark(X))))}
SCCS:
Scc:
{ mark#(adx(X)) -> mark#(X),
mark#(adx(X)) -> active#(adx(mark(X))),
mark#(incr(X)) -> mark#(X),
mark#(incr(X)) -> active#(incr(mark(X))),
mark#(hd(X)) -> mark#(X),
mark#(hd(X)) -> active#(hd(mark(X))),
mark#(tl(X)) -> active#(tl(mark(X))),
active#(adx(cons(X, Y))) -> mark#(incr(cons(X, adx(Y)))),
active#(incr(cons(X, Y))) -> mark#(cons(s(X), incr(Y))),
active#(hd(cons(X, Y))) -> mark#(X)}
SCC:
Strict:
{ mark#(adx(X)) -> mark#(X),
mark#(adx(X)) -> active#(adx(mark(X))),
mark#(incr(X)) -> mark#(X),
mark#(incr(X)) -> active#(incr(mark(X))),
mark#(hd(X)) -> mark#(X),
mark#(hd(X)) -> active#(hd(mark(X))),
mark#(tl(X)) -> active#(tl(mark(X))),
active#(adx(cons(X, Y))) -> mark#(incr(cons(X, adx(Y)))),
active#(incr(cons(X, Y))) -> mark#(cons(s(X), incr(Y))),
active#(hd(cons(X, Y))) -> mark#(X)}
Weak:
{ mark(adx(X)) -> active(adx(mark(X))),
mark(zeros()) -> active(zeros()),
mark(nats()) -> active(nats()),
mark(cons(X1, X2)) -> active(cons(X1, X2)),
mark(0()) -> active(0()),
mark(s(X)) -> active(s(X)),
mark(incr(X)) -> active(incr(mark(X))),
mark(hd(X)) -> active(hd(mark(X))),
mark(tl(X)) -> active(tl(mark(X))),
adx(mark(X)) -> adx(X),
adx(active(X)) -> adx(X),
active(adx(cons(X, Y))) -> mark(incr(cons(X, adx(Y)))),
active(zeros()) -> mark(cons(0(), zeros())),
active(nats()) -> mark(adx(zeros())),
active(incr(cons(X, Y))) -> mark(cons(s(X), incr(Y))),
active(hd(cons(X, Y))) -> mark(X),
active(tl(cons(X, Y))) -> mark(Y),
cons(X1, mark(X2)) -> cons(X1, X2),
cons(X1, active(X2)) -> cons(X1, X2),
cons(mark(X1), X2) -> cons(X1, X2),
cons(active(X1), X2) -> cons(X1, X2),
s(mark(X)) -> s(X),
s(active(X)) -> s(X),
incr(mark(X)) -> incr(X),
incr(active(X)) -> incr(X),
hd(mark(X)) -> hd(X),
hd(active(X)) -> hd(X),
tl(mark(X)) -> tl(X),
tl(active(X)) -> tl(X)}
POLY:
Argument Filtering:
pi(tl) = 0, pi(hd) = [0], pi(incr) = 0, pi(s) = [], pi(0) = [], pi(cons) = [0,1], pi(nats) = [], pi(active#) = 0, pi(active) = 0, pi(zeros) = [], pi(adx) = 0, pi(mark#) = 0, pi(mark) = 0
Usable Rules:
{}
Interpretation:
[cons](x0, x1) = x0 + x1,
[hd](x0) = x0 + 1,
[s] = 0
Strict:
{ mark#(adx(X)) -> mark#(X),
mark#(adx(X)) -> active#(adx(mark(X))),
mark#(incr(X)) -> mark#(X),
mark#(incr(X)) -> active#(incr(mark(X))),
mark#(hd(X)) -> active#(hd(mark(X))),
mark#(tl(X)) -> active#(tl(mark(X))),
active#(adx(cons(X, Y))) -> mark#(incr(cons(X, adx(Y)))),
active#(incr(cons(X, Y))) -> mark#(cons(s(X), incr(Y)))}
Weak:
{ mark(adx(X)) -> active(adx(mark(X))),
mark(zeros()) -> active(zeros()),
mark(nats()) -> active(nats()),
mark(cons(X1, X2)) -> active(cons(X1, X2)),
mark(0()) -> active(0()),
mark(s(X)) -> active(s(X)),
mark(incr(X)) -> active(incr(mark(X))),
mark(hd(X)) -> active(hd(mark(X))),
mark(tl(X)) -> active(tl(mark(X))),
adx(mark(X)) -> adx(X),
adx(active(X)) -> adx(X),
active(adx(cons(X, Y))) -> mark(incr(cons(X, adx(Y)))),
active(zeros()) -> mark(cons(0(), zeros())),
active(nats()) -> mark(adx(zeros())),
active(incr(cons(X, Y))) -> mark(cons(s(X), incr(Y))),
active(hd(cons(X, Y))) -> mark(X),
active(tl(cons(X, Y))) -> mark(Y),
cons(X1, mark(X2)) -> cons(X1, X2),
cons(X1, active(X2)) -> cons(X1, X2),
cons(mark(X1), X2) -> cons(X1, X2),
cons(active(X1), X2) -> cons(X1, X2),
s(mark(X)) -> s(X),
s(active(X)) -> s(X),
incr(mark(X)) -> incr(X),
incr(active(X)) -> incr(X),
hd(mark(X)) -> hd(X),
hd(active(X)) -> hd(X),
tl(mark(X)) -> tl(X),
tl(active(X)) -> tl(X)}
EDG:
{(mark#(incr(X)) -> active#(incr(mark(X))), active#(incr(cons(X, Y))) -> mark#(cons(s(X), incr(Y))))
(mark#(incr(X)) -> active#(incr(mark(X))), active#(adx(cons(X, Y))) -> mark#(incr(cons(X, adx(Y)))))
(mark#(tl(X)) -> active#(tl(mark(X))), active#(incr(cons(X, Y))) -> mark#(cons(s(X), incr(Y))))
(mark#(tl(X)) -> active#(tl(mark(X))), active#(adx(cons(X, Y))) -> mark#(incr(cons(X, adx(Y)))))
(active#(incr(cons(X, Y))) -> mark#(cons(s(X), incr(Y))), mark#(tl(X)) -> active#(tl(mark(X))))
(active#(incr(cons(X, Y))) -> mark#(cons(s(X), incr(Y))), mark#(hd(X)) -> active#(hd(mark(X))))
(active#(incr(cons(X, Y))) -> mark#(cons(s(X), incr(Y))), mark#(incr(X)) -> active#(incr(mark(X))))
(active#(incr(cons(X, Y))) -> mark#(cons(s(X), incr(Y))), mark#(incr(X)) -> mark#(X))
(active#(incr(cons(X, Y))) -> mark#(cons(s(X), incr(Y))), mark#(adx(X)) -> active#(adx(mark(X))))
(active#(incr(cons(X, Y))) -> mark#(cons(s(X), incr(Y))), mark#(adx(X)) -> mark#(X))
(mark#(incr(X)) -> mark#(X), mark#(tl(X)) -> active#(tl(mark(X))))
(mark#(incr(X)) -> mark#(X), mark#(hd(X)) -> active#(hd(mark(X))))
(mark#(incr(X)) -> mark#(X), mark#(incr(X)) -> active#(incr(mark(X))))
(mark#(incr(X)) -> mark#(X), mark#(incr(X)) -> mark#(X))
(mark#(incr(X)) -> mark#(X), mark#(adx(X)) -> active#(adx(mark(X))))
(mark#(incr(X)) -> mark#(X), mark#(adx(X)) -> mark#(X))
(mark#(adx(X)) -> mark#(X), mark#(adx(X)) -> mark#(X))
(mark#(adx(X)) -> mark#(X), mark#(adx(X)) -> active#(adx(mark(X))))
(mark#(adx(X)) -> mark#(X), mark#(incr(X)) -> mark#(X))
(mark#(adx(X)) -> mark#(X), mark#(incr(X)) -> active#(incr(mark(X))))
(mark#(adx(X)) -> mark#(X), mark#(hd(X)) -> active#(hd(mark(X))))
(mark#(adx(X)) -> mark#(X), mark#(tl(X)) -> active#(tl(mark(X))))
(active#(adx(cons(X, Y))) -> mark#(incr(cons(X, adx(Y)))), mark#(adx(X)) -> mark#(X))
(active#(adx(cons(X, Y))) -> mark#(incr(cons(X, adx(Y)))), mark#(adx(X)) -> active#(adx(mark(X))))
(active#(adx(cons(X, Y))) -> mark#(incr(cons(X, adx(Y)))), mark#(incr(X)) -> mark#(X))
(active#(adx(cons(X, Y))) -> mark#(incr(cons(X, adx(Y)))), mark#(incr(X)) -> active#(incr(mark(X))))
(active#(adx(cons(X, Y))) -> mark#(incr(cons(X, adx(Y)))), mark#(hd(X)) -> active#(hd(mark(X))))
(active#(adx(cons(X, Y))) -> mark#(incr(cons(X, adx(Y)))), mark#(tl(X)) -> active#(tl(mark(X))))
(mark#(hd(X)) -> active#(hd(mark(X))), active#(adx(cons(X, Y))) -> mark#(incr(cons(X, adx(Y)))))
(mark#(hd(X)) -> active#(hd(mark(X))), active#(incr(cons(X, Y))) -> mark#(cons(s(X), incr(Y))))
(mark#(adx(X)) -> active#(adx(mark(X))), active#(adx(cons(X, Y))) -> mark#(incr(cons(X, adx(Y)))))
(mark#(adx(X)) -> active#(adx(mark(X))), active#(incr(cons(X, Y))) -> mark#(cons(s(X), incr(Y))))}
SCCS:
Scc:
{ mark#(adx(X)) -> mark#(X),
mark#(adx(X)) -> active#(adx(mark(X))),
mark#(incr(X)) -> mark#(X),
mark#(incr(X)) -> active#(incr(mark(X))),
mark#(hd(X)) -> active#(hd(mark(X))),
mark#(tl(X)) -> active#(tl(mark(X))),
active#(adx(cons(X, Y))) -> mark#(incr(cons(X, adx(Y)))),
active#(incr(cons(X, Y))) -> mark#(cons(s(X), incr(Y)))}
SCC:
Strict:
{ mark#(adx(X)) -> mark#(X),
mark#(adx(X)) -> active#(adx(mark(X))),
mark#(incr(X)) -> mark#(X),
mark#(incr(X)) -> active#(incr(mark(X))),
mark#(hd(X)) -> active#(hd(mark(X))),
mark#(tl(X)) -> active#(tl(mark(X))),
active#(adx(cons(X, Y))) -> mark#(incr(cons(X, adx(Y)))),
active#(incr(cons(X, Y))) -> mark#(cons(s(X), incr(Y)))}
Weak:
{ mark(adx(X)) -> active(adx(mark(X))),
mark(zeros()) -> active(zeros()),
mark(nats()) -> active(nats()),
mark(cons(X1, X2)) -> active(cons(X1, X2)),
mark(0()) -> active(0()),
mark(s(X)) -> active(s(X)),
mark(incr(X)) -> active(incr(mark(X))),
mark(hd(X)) -> active(hd(mark(X))),
mark(tl(X)) -> active(tl(mark(X))),
adx(mark(X)) -> adx(X),
adx(active(X)) -> adx(X),
active(adx(cons(X, Y))) -> mark(incr(cons(X, adx(Y)))),
active(zeros()) -> mark(cons(0(), zeros())),
active(nats()) -> mark(adx(zeros())),
active(incr(cons(X, Y))) -> mark(cons(s(X), incr(Y))),
active(hd(cons(X, Y))) -> mark(X),
active(tl(cons(X, Y))) -> mark(Y),
cons(X1, mark(X2)) -> cons(X1, X2),
cons(X1, active(X2)) -> cons(X1, X2),
cons(mark(X1), X2) -> cons(X1, X2),
cons(active(X1), X2) -> cons(X1, X2),
s(mark(X)) -> s(X),
s(active(X)) -> s(X),
incr(mark(X)) -> incr(X),
incr(active(X)) -> incr(X),
hd(mark(X)) -> hd(X),
hd(active(X)) -> hd(X),
tl(mark(X)) -> tl(X),
tl(active(X)) -> tl(X)}
POLY:
Argument Filtering:
pi(tl) = [], pi(hd) = [], pi(incr) = [], pi(s) = [], pi(0) = [], pi(cons) = [], pi(nats) = [], pi(active#) = 0, pi(active) = [], pi(zeros) = [], pi(adx) = [], pi(mark#) = [], pi(mark) = []
Usable Rules:
{}
Interpretation:
[mark#] = 1,
[tl] = 0,
[hd] = 0,
[incr] = 1,
[adx] = 1
Strict:
{ mark#(adx(X)) -> mark#(X),
mark#(adx(X)) -> active#(adx(mark(X))),
mark#(incr(X)) -> mark#(X),
mark#(incr(X)) -> active#(incr(mark(X))),
active#(adx(cons(X, Y))) -> mark#(incr(cons(X, adx(Y)))),
active#(incr(cons(X, Y))) -> mark#(cons(s(X), incr(Y)))}
Weak:
{ mark(adx(X)) -> active(adx(mark(X))),
mark(zeros()) -> active(zeros()),
mark(nats()) -> active(nats()),
mark(cons(X1, X2)) -> active(cons(X1, X2)),
mark(0()) -> active(0()),
mark(s(X)) -> active(s(X)),
mark(incr(X)) -> active(incr(mark(X))),
mark(hd(X)) -> active(hd(mark(X))),
mark(tl(X)) -> active(tl(mark(X))),
adx(mark(X)) -> adx(X),
adx(active(X)) -> adx(X),
active(adx(cons(X, Y))) -> mark(incr(cons(X, adx(Y)))),
active(zeros()) -> mark(cons(0(), zeros())),
active(nats()) -> mark(adx(zeros())),
active(incr(cons(X, Y))) -> mark(cons(s(X), incr(Y))),
active(hd(cons(X, Y))) -> mark(X),
active(tl(cons(X, Y))) -> mark(Y),
cons(X1, mark(X2)) -> cons(X1, X2),
cons(X1, active(X2)) -> cons(X1, X2),
cons(mark(X1), X2) -> cons(X1, X2),
cons(active(X1), X2) -> cons(X1, X2),
s(mark(X)) -> s(X),
s(active(X)) -> s(X),
incr(mark(X)) -> incr(X),
incr(active(X)) -> incr(X),
hd(mark(X)) -> hd(X),
hd(active(X)) -> hd(X),
tl(mark(X)) -> tl(X),
tl(active(X)) -> tl(X)}
EDG:
{(mark#(incr(X)) -> active#(incr(mark(X))), active#(incr(cons(X, Y))) -> mark#(cons(s(X), incr(Y))))
(mark#(incr(X)) -> active#(incr(mark(X))), active#(adx(cons(X, Y))) -> mark#(incr(cons(X, adx(Y)))))
(mark#(adx(X)) -> mark#(X), mark#(incr(X)) -> active#(incr(mark(X))))
(mark#(adx(X)) -> mark#(X), mark#(incr(X)) -> mark#(X))
(mark#(adx(X)) -> mark#(X), mark#(adx(X)) -> active#(adx(mark(X))))
(mark#(adx(X)) -> mark#(X), mark#(adx(X)) -> mark#(X))
(active#(incr(cons(X, Y))) -> mark#(cons(s(X), incr(Y))), mark#(incr(X)) -> active#(incr(mark(X))))
(active#(incr(cons(X, Y))) -> mark#(cons(s(X), incr(Y))), mark#(incr(X)) -> mark#(X))
(active#(incr(cons(X, Y))) -> mark#(cons(s(X), incr(Y))), mark#(adx(X)) -> active#(adx(mark(X))))
(active#(incr(cons(X, Y))) -> mark#(cons(s(X), incr(Y))), mark#(adx(X)) -> mark#(X))
(mark#(incr(X)) -> mark#(X), mark#(adx(X)) -> mark#(X))
(mark#(incr(X)) -> mark#(X), mark#(adx(X)) -> active#(adx(mark(X))))
(mark#(incr(X)) -> mark#(X), mark#(incr(X)) -> mark#(X))
(mark#(incr(X)) -> mark#(X), mark#(incr(X)) -> active#(incr(mark(X))))
(active#(adx(cons(X, Y))) -> mark#(incr(cons(X, adx(Y)))), mark#(adx(X)) -> mark#(X))
(active#(adx(cons(X, Y))) -> mark#(incr(cons(X, adx(Y)))), mark#(adx(X)) -> active#(adx(mark(X))))
(active#(adx(cons(X, Y))) -> mark#(incr(cons(X, adx(Y)))), mark#(incr(X)) -> mark#(X))
(active#(adx(cons(X, Y))) -> mark#(incr(cons(X, adx(Y)))), mark#(incr(X)) -> active#(incr(mark(X))))
(mark#(adx(X)) -> active#(adx(mark(X))), active#(adx(cons(X, Y))) -> mark#(incr(cons(X, adx(Y)))))
(mark#(adx(X)) -> active#(adx(mark(X))), active#(incr(cons(X, Y))) -> mark#(cons(s(X), incr(Y))))}
SCCS:
Scc:
{ mark#(adx(X)) -> mark#(X),
mark#(adx(X)) -> active#(adx(mark(X))),
mark#(incr(X)) -> mark#(X),
mark#(incr(X)) -> active#(incr(mark(X))),
active#(adx(cons(X, Y))) -> mark#(incr(cons(X, adx(Y)))),
active#(incr(cons(X, Y))) -> mark#(cons(s(X), incr(Y)))}
SCC:
Strict:
{ mark#(adx(X)) -> mark#(X),
mark#(adx(X)) -> active#(adx(mark(X))),
mark#(incr(X)) -> mark#(X),
mark#(incr(X)) -> active#(incr(mark(X))),
active#(adx(cons(X, Y))) -> mark#(incr(cons(X, adx(Y)))),
active#(incr(cons(X, Y))) -> mark#(cons(s(X), incr(Y)))}
Weak:
{ mark(adx(X)) -> active(adx(mark(X))),
mark(zeros()) -> active(zeros()),
mark(nats()) -> active(nats()),
mark(cons(X1, X2)) -> active(cons(X1, X2)),
mark(0()) -> active(0()),
mark(s(X)) -> active(s(X)),
mark(incr(X)) -> active(incr(mark(X))),
mark(hd(X)) -> active(hd(mark(X))),
mark(tl(X)) -> active(tl(mark(X))),
adx(mark(X)) -> adx(X),
adx(active(X)) -> adx(X),
active(adx(cons(X, Y))) -> mark(incr(cons(X, adx(Y)))),
active(zeros()) -> mark(cons(0(), zeros())),
active(nats()) -> mark(adx(zeros())),
active(incr(cons(X, Y))) -> mark(cons(s(X), incr(Y))),
active(hd(cons(X, Y))) -> mark(X),
active(tl(cons(X, Y))) -> mark(Y),
cons(X1, mark(X2)) -> cons(X1, X2),
cons(X1, active(X2)) -> cons(X1, X2),
cons(mark(X1), X2) -> cons(X1, X2),
cons(active(X1), X2) -> cons(X1, X2),
s(mark(X)) -> s(X),
s(active(X)) -> s(X),
incr(mark(X)) -> incr(X),
incr(active(X)) -> incr(X),
hd(mark(X)) -> hd(X),
hd(active(X)) -> hd(X),
tl(mark(X)) -> tl(X),
tl(active(X)) -> tl(X)}
POLY:
Argument Filtering:
pi(tl) = [], pi(hd) = [], pi(incr) = 0, pi(s) = [], pi(0) = [], pi(cons) = [], pi(nats) = [], pi(active#) = [], pi(active) = 0, pi(zeros) = [], pi(adx) = [0], pi(mark#) = 0, pi(mark) = 0
Usable Rules:
{}
Interpretation:
[active#] = 0,
[cons] = 0,
[adx](x0) = x0 + 1
Strict:
{ mark#(incr(X)) -> mark#(X),
mark#(incr(X)) -> active#(incr(mark(X))),
active#(adx(cons(X, Y))) -> mark#(incr(cons(X, adx(Y)))),
active#(incr(cons(X, Y))) -> mark#(cons(s(X), incr(Y)))}
Weak:
{ mark(adx(X)) -> active(adx(mark(X))),
mark(zeros()) -> active(zeros()),
mark(nats()) -> active(nats()),
mark(cons(X1, X2)) -> active(cons(X1, X2)),
mark(0()) -> active(0()),
mark(s(X)) -> active(s(X)),
mark(incr(X)) -> active(incr(mark(X))),
mark(hd(X)) -> active(hd(mark(X))),
mark(tl(X)) -> active(tl(mark(X))),
adx(mark(X)) -> adx(X),
adx(active(X)) -> adx(X),
active(adx(cons(X, Y))) -> mark(incr(cons(X, adx(Y)))),
active(zeros()) -> mark(cons(0(), zeros())),
active(nats()) -> mark(adx(zeros())),
active(incr(cons(X, Y))) -> mark(cons(s(X), incr(Y))),
active(hd(cons(X, Y))) -> mark(X),
active(tl(cons(X, Y))) -> mark(Y),
cons(X1, mark(X2)) -> cons(X1, X2),
cons(X1, active(X2)) -> cons(X1, X2),
cons(mark(X1), X2) -> cons(X1, X2),
cons(active(X1), X2) -> cons(X1, X2),
s(mark(X)) -> s(X),
s(active(X)) -> s(X),
incr(mark(X)) -> incr(X),
incr(active(X)) -> incr(X),
hd(mark(X)) -> hd(X),
hd(active(X)) -> hd(X),
tl(mark(X)) -> tl(X),
tl(active(X)) -> tl(X)}
EDG:
{(active#(adx(cons(X, Y))) -> mark#(incr(cons(X, adx(Y)))), mark#(incr(X)) -> active#(incr(mark(X))))
(active#(adx(cons(X, Y))) -> mark#(incr(cons(X, adx(Y)))), mark#(incr(X)) -> mark#(X))
(mark#(incr(X)) -> mark#(X), mark#(incr(X)) -> active#(incr(mark(X))))
(mark#(incr(X)) -> mark#(X), mark#(incr(X)) -> mark#(X))
(active#(incr(cons(X, Y))) -> mark#(cons(s(X), incr(Y))), mark#(incr(X)) -> mark#(X))
(active#(incr(cons(X, Y))) -> mark#(cons(s(X), incr(Y))), mark#(incr(X)) -> active#(incr(mark(X))))
(mark#(incr(X)) -> active#(incr(mark(X))), active#(adx(cons(X, Y))) -> mark#(incr(cons(X, adx(Y)))))
(mark#(incr(X)) -> active#(incr(mark(X))), active#(incr(cons(X, Y))) -> mark#(cons(s(X), incr(Y))))}
SCCS:
Scc:
{ mark#(incr(X)) -> mark#(X),
mark#(incr(X)) -> active#(incr(mark(X))),
active#(adx(cons(X, Y))) -> mark#(incr(cons(X, adx(Y)))),
active#(incr(cons(X, Y))) -> mark#(cons(s(X), incr(Y)))}
SCC:
Strict:
{ mark#(incr(X)) -> mark#(X),
mark#(incr(X)) -> active#(incr(mark(X))),
active#(adx(cons(X, Y))) -> mark#(incr(cons(X, adx(Y)))),
active#(incr(cons(X, Y))) -> mark#(cons(s(X), incr(Y)))}
Weak:
{ mark(adx(X)) -> active(adx(mark(X))),
mark(zeros()) -> active(zeros()),
mark(nats()) -> active(nats()),
mark(cons(X1, X2)) -> active(cons(X1, X2)),
mark(0()) -> active(0()),
mark(s(X)) -> active(s(X)),
mark(incr(X)) -> active(incr(mark(X))),
mark(hd(X)) -> active(hd(mark(X))),
mark(tl(X)) -> active(tl(mark(X))),
adx(mark(X)) -> adx(X),
adx(active(X)) -> adx(X),
active(adx(cons(X, Y))) -> mark(incr(cons(X, adx(Y)))),
active(zeros()) -> mark(cons(0(), zeros())),
active(nats()) -> mark(adx(zeros())),
active(incr(cons(X, Y))) -> mark(cons(s(X), incr(Y))),
active(hd(cons(X, Y))) -> mark(X),
active(tl(cons(X, Y))) -> mark(Y),
cons(X1, mark(X2)) -> cons(X1, X2),
cons(X1, active(X2)) -> cons(X1, X2),
cons(mark(X1), X2) -> cons(X1, X2),
cons(active(X1), X2) -> cons(X1, X2),
s(mark(X)) -> s(X),
s(active(X)) -> s(X),
incr(mark(X)) -> incr(X),
incr(active(X)) -> incr(X),
hd(mark(X)) -> hd(X),
hd(active(X)) -> hd(X),
tl(mark(X)) -> tl(X),
tl(active(X)) -> tl(X)}
POLY:
Argument Filtering:
pi(tl) = [], pi(hd) = [], pi(incr) = [], pi(s) = [], pi(0) = [], pi(cons) = [], pi(nats) = [], pi(active#) = 0, pi(active) = [], pi(zeros) = [], pi(adx) = [0], pi(mark#) = [], pi(mark) = []
Usable Rules:
{}
Interpretation:
[mark#] = 0,
[cons] = 1,
[incr] = 0,
[adx](x0) = x0 + 1
Strict:
{ mark#(incr(X)) -> mark#(X),
mark#(incr(X)) -> active#(incr(mark(X))),
active#(incr(cons(X, Y))) -> mark#(cons(s(X), incr(Y)))}
Weak:
{ mark(adx(X)) -> active(adx(mark(X))),
mark(zeros()) -> active(zeros()),
mark(nats()) -> active(nats()),
mark(cons(X1, X2)) -> active(cons(X1, X2)),
mark(0()) -> active(0()),
mark(s(X)) -> active(s(X)),
mark(incr(X)) -> active(incr(mark(X))),
mark(hd(X)) -> active(hd(mark(X))),
mark(tl(X)) -> active(tl(mark(X))),
adx(mark(X)) -> adx(X),
adx(active(X)) -> adx(X),
active(adx(cons(X, Y))) -> mark(incr(cons(X, adx(Y)))),
active(zeros()) -> mark(cons(0(), zeros())),
active(nats()) -> mark(adx(zeros())),
active(incr(cons(X, Y))) -> mark(cons(s(X), incr(Y))),
active(hd(cons(X, Y))) -> mark(X),
active(tl(cons(X, Y))) -> mark(Y),
cons(X1, mark(X2)) -> cons(X1, X2),
cons(X1, active(X2)) -> cons(X1, X2),
cons(mark(X1), X2) -> cons(X1, X2),
cons(active(X1), X2) -> cons(X1, X2),
s(mark(X)) -> s(X),
s(active(X)) -> s(X),
incr(mark(X)) -> incr(X),
incr(active(X)) -> incr(X),
hd(mark(X)) -> hd(X),
hd(active(X)) -> hd(X),
tl(mark(X)) -> tl(X),
tl(active(X)) -> tl(X)}
EDG:
{(active#(incr(cons(X, Y))) -> mark#(cons(s(X), incr(Y))), mark#(incr(X)) -> active#(incr(mark(X))))
(active#(incr(cons(X, Y))) -> mark#(cons(s(X), incr(Y))), mark#(incr(X)) -> mark#(X))
(mark#(incr(X)) -> mark#(X), mark#(incr(X)) -> mark#(X))
(mark#(incr(X)) -> mark#(X), mark#(incr(X)) -> active#(incr(mark(X))))
(mark#(incr(X)) -> active#(incr(mark(X))), active#(incr(cons(X, Y))) -> mark#(cons(s(X), incr(Y))))}
SCCS:
Scc:
{ mark#(incr(X)) -> mark#(X),
mark#(incr(X)) -> active#(incr(mark(X))),
active#(incr(cons(X, Y))) -> mark#(cons(s(X), incr(Y)))}
SCC:
Strict:
{ mark#(incr(X)) -> mark#(X),
mark#(incr(X)) -> active#(incr(mark(X))),
active#(incr(cons(X, Y))) -> mark#(cons(s(X), incr(Y)))}
Weak:
{ mark(adx(X)) -> active(adx(mark(X))),
mark(zeros()) -> active(zeros()),
mark(nats()) -> active(nats()),
mark(cons(X1, X2)) -> active(cons(X1, X2)),
mark(0()) -> active(0()),
mark(s(X)) -> active(s(X)),
mark(incr(X)) -> active(incr(mark(X))),
mark(hd(X)) -> active(hd(mark(X))),
mark(tl(X)) -> active(tl(mark(X))),
adx(mark(X)) -> adx(X),
adx(active(X)) -> adx(X),
active(adx(cons(X, Y))) -> mark(incr(cons(X, adx(Y)))),
active(zeros()) -> mark(cons(0(), zeros())),
active(nats()) -> mark(adx(zeros())),
active(incr(cons(X, Y))) -> mark(cons(s(X), incr(Y))),
active(hd(cons(X, Y))) -> mark(X),
active(tl(cons(X, Y))) -> mark(Y),
cons(X1, mark(X2)) -> cons(X1, X2),
cons(X1, active(X2)) -> cons(X1, X2),
cons(mark(X1), X2) -> cons(X1, X2),
cons(active(X1), X2) -> cons(X1, X2),
s(mark(X)) -> s(X),
s(active(X)) -> s(X),
incr(mark(X)) -> incr(X),
incr(active(X)) -> incr(X),
hd(mark(X)) -> hd(X),
hd(active(X)) -> hd(X),
tl(mark(X)) -> tl(X),
tl(active(X)) -> tl(X)}
POLY:
Argument Filtering:
pi(tl) = [], pi(hd) = [], pi(incr) = [0], pi(s) = [], pi(0) = [], pi(cons) = [], pi(nats) = [], pi(active#) = [], pi(active) = [], pi(zeros) = [], pi(adx) = [], pi(mark#) = 0, pi(mark) = []
Usable Rules:
{}
Interpretation:
[active#] = 0,
[cons] = 0,
[incr](x0) = x0 + 1
Strict:
{active#(incr(cons(X, Y))) -> mark#(cons(s(X), incr(Y)))}
Weak:
{ mark(adx(X)) -> active(adx(mark(X))),
mark(zeros()) -> active(zeros()),
mark(nats()) -> active(nats()),
mark(cons(X1, X2)) -> active(cons(X1, X2)),
mark(0()) -> active(0()),
mark(s(X)) -> active(s(X)),
mark(incr(X)) -> active(incr(mark(X))),
mark(hd(X)) -> active(hd(mark(X))),
mark(tl(X)) -> active(tl(mark(X))),
adx(mark(X)) -> adx(X),
adx(active(X)) -> adx(X),
active(adx(cons(X, Y))) -> mark(incr(cons(X, adx(Y)))),
active(zeros()) -> mark(cons(0(), zeros())),
active(nats()) -> mark(adx(zeros())),
active(incr(cons(X, Y))) -> mark(cons(s(X), incr(Y))),
active(hd(cons(X, Y))) -> mark(X),
active(tl(cons(X, Y))) -> mark(Y),
cons(X1, mark(X2)) -> cons(X1, X2),
cons(X1, active(X2)) -> cons(X1, X2),
cons(mark(X1), X2) -> cons(X1, X2),
cons(active(X1), X2) -> cons(X1, X2),
s(mark(X)) -> s(X),
s(active(X)) -> s(X),
incr(mark(X)) -> incr(X),
incr(active(X)) -> incr(X),
hd(mark(X)) -> hd(X),
hd(active(X)) -> hd(X),
tl(mark(X)) -> tl(X),
tl(active(X)) -> tl(X)}
EDG:
{}
SCCS:
Qed