YES
TRS:
{ mark(nil()) -> active(nil()),
mark(fst(X1, X2)) -> active(fst(mark(X1), mark(X2))),
mark(0()) -> active(0()),
mark(cons(X1, X2)) -> active(cons(mark(X1), X2)),
mark(s(X)) -> active(s(X)),
mark(from(X)) -> active(from(mark(X))),
mark(add(X1, X2)) -> active(add(mark(X1), mark(X2))),
mark(len(X)) -> active(len(mark(X))),
active(fst(0(), Z)) -> mark(nil()),
active(fst(s(X), cons(Y, Z))) -> mark(cons(Y, fst(X, Z))),
active(from(X)) -> mark(cons(X, from(s(X)))),
active(add(0(), X)) -> mark(X),
active(add(s(X), Y)) -> mark(s(add(X, Y))),
active(len(nil())) -> mark(0()),
active(len(cons(X, Z))) -> mark(s(len(Z))),
fst(X1, mark(X2)) -> fst(X1, X2),
fst(X1, active(X2)) -> fst(X1, X2),
fst(mark(X1), X2) -> fst(X1, X2),
fst(active(X1), X2) -> fst(X1, X2),
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),
from(mark(X)) -> from(X),
from(active(X)) -> from(X),
add(X1, mark(X2)) -> add(X1, X2),
add(X1, active(X2)) -> add(X1, X2),
add(mark(X1), X2) -> add(X1, X2),
add(active(X1), X2) -> add(X1, X2),
len(mark(X)) -> len(X),
len(active(X)) -> len(X)}
DP:
Strict:
{ mark#(nil()) -> active#(nil()),
mark#(fst(X1, X2)) -> mark#(X1),
mark#(fst(X1, X2)) -> mark#(X2),
mark#(fst(X1, X2)) -> active#(fst(mark(X1), mark(X2))),
mark#(fst(X1, X2)) -> fst#(mark(X1), mark(X2)),
mark#(0()) -> active#(0()),
mark#(cons(X1, X2)) -> mark#(X1),
mark#(cons(X1, X2)) -> active#(cons(mark(X1), X2)),
mark#(cons(X1, X2)) -> cons#(mark(X1), X2),
mark#(s(X)) -> active#(s(X)),
mark#(from(X)) -> mark#(X),
mark#(from(X)) -> active#(from(mark(X))),
mark#(from(X)) -> from#(mark(X)),
mark#(add(X1, X2)) -> mark#(X1),
mark#(add(X1, X2)) -> mark#(X2),
mark#(add(X1, X2)) -> active#(add(mark(X1), mark(X2))),
mark#(add(X1, X2)) -> add#(mark(X1), mark(X2)),
mark#(len(X)) -> mark#(X),
mark#(len(X)) -> active#(len(mark(X))),
mark#(len(X)) -> len#(mark(X)),
active#(fst(0(), Z)) -> mark#(nil()),
active#(fst(s(X), cons(Y, Z))) -> mark#(cons(Y, fst(X, Z))),
active#(fst(s(X), cons(Y, Z))) -> fst#(X, Z),
active#(fst(s(X), cons(Y, Z))) -> cons#(Y, fst(X, Z)),
active#(from(X)) -> mark#(cons(X, from(s(X)))),
active#(from(X)) -> cons#(X, from(s(X))),
active#(from(X)) -> s#(X),
active#(from(X)) -> from#(s(X)),
active#(add(0(), X)) -> mark#(X),
active#(add(s(X), Y)) -> mark#(s(add(X, Y))),
active#(add(s(X), Y)) -> s#(add(X, Y)),
active#(add(s(X), Y)) -> add#(X, Y),
active#(len(nil())) -> mark#(0()),
active#(len(cons(X, Z))) -> mark#(s(len(Z))),
active#(len(cons(X, Z))) -> s#(len(Z)),
active#(len(cons(X, Z))) -> len#(Z),
fst#(X1, mark(X2)) -> fst#(X1, X2),
fst#(X1, active(X2)) -> fst#(X1, X2),
fst#(mark(X1), X2) -> fst#(X1, X2),
fst#(active(X1), X2) -> fst#(X1, X2),
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),
from#(mark(X)) -> from#(X),
from#(active(X)) -> from#(X),
add#(X1, mark(X2)) -> add#(X1, X2),
add#(X1, active(X2)) -> add#(X1, X2),
add#(mark(X1), X2) -> add#(X1, X2),
add#(active(X1), X2) -> add#(X1, X2),
len#(mark(X)) -> len#(X),
len#(active(X)) -> len#(X)}
Weak:
{ mark(nil()) -> active(nil()),
mark(fst(X1, X2)) -> active(fst(mark(X1), mark(X2))),
mark(0()) -> active(0()),
mark(cons(X1, X2)) -> active(cons(mark(X1), X2)),
mark(s(X)) -> active(s(X)),
mark(from(X)) -> active(from(mark(X))),
mark(add(X1, X2)) -> active(add(mark(X1), mark(X2))),
mark(len(X)) -> active(len(mark(X))),
active(fst(0(), Z)) -> mark(nil()),
active(fst(s(X), cons(Y, Z))) -> mark(cons(Y, fst(X, Z))),
active(from(X)) -> mark(cons(X, from(s(X)))),
active(add(0(), X)) -> mark(X),
active(add(s(X), Y)) -> mark(s(add(X, Y))),
active(len(nil())) -> mark(0()),
active(len(cons(X, Z))) -> mark(s(len(Z))),
fst(X1, mark(X2)) -> fst(X1, X2),
fst(X1, active(X2)) -> fst(X1, X2),
fst(mark(X1), X2) -> fst(X1, X2),
fst(active(X1), X2) -> fst(X1, X2),
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),
from(mark(X)) -> from(X),
from(active(X)) -> from(X),
add(X1, mark(X2)) -> add(X1, X2),
add(X1, active(X2)) -> add(X1, X2),
add(mark(X1), X2) -> add(X1, X2),
add(active(X1), X2) -> add(X1, X2),
len(mark(X)) -> len(X),
len(active(X)) -> len(X)}
EDG:
{
(mark#(add(X1, X2)) -> mark#(X2), mark#(len(X)) -> len#(mark(X)))
(mark#(add(X1, X2)) -> mark#(X2), mark#(len(X)) -> active#(len(mark(X))))
(mark#(add(X1, X2)) -> mark#(X2), mark#(len(X)) -> mark#(X))
(mark#(add(X1, X2)) -> mark#(X2), mark#(add(X1, X2)) -> add#(mark(X1), mark(X2)))
(mark#(add(X1, X2)) -> mark#(X2), mark#(add(X1, X2)) -> active#(add(mark(X1), mark(X2))))
(mark#(add(X1, X2)) -> mark#(X2), mark#(add(X1, X2)) -> mark#(X2))
(mark#(add(X1, X2)) -> mark#(X2), mark#(add(X1, X2)) -> mark#(X1))
(mark#(add(X1, X2)) -> mark#(X2), mark#(from(X)) -> from#(mark(X)))
(mark#(add(X1, X2)) -> mark#(X2), mark#(from(X)) -> active#(from(mark(X))))
(mark#(add(X1, X2)) -> mark#(X2), mark#(from(X)) -> mark#(X))
(mark#(add(X1, X2)) -> mark#(X2), mark#(s(X)) -> active#(s(X)))
(mark#(add(X1, X2)) -> mark#(X2), mark#(cons(X1, X2)) -> cons#(mark(X1), X2))
(mark#(add(X1, X2)) -> mark#(X2), mark#(cons(X1, X2)) -> active#(cons(mark(X1), X2)))
(mark#(add(X1, X2)) -> mark#(X2), mark#(cons(X1, X2)) -> mark#(X1))
(mark#(add(X1, X2)) -> mark#(X2), mark#(0()) -> active#(0()))
(mark#(add(X1, X2)) -> mark#(X2), mark#(fst(X1, X2)) -> fst#(mark(X1), mark(X2)))
(mark#(add(X1, X2)) -> mark#(X2), mark#(fst(X1, X2)) -> active#(fst(mark(X1), mark(X2))))
(mark#(add(X1, X2)) -> mark#(X2), mark#(fst(X1, X2)) -> mark#(X2))
(mark#(add(X1, X2)) -> mark#(X2), mark#(fst(X1, X2)) -> mark#(X1))
(mark#(add(X1, X2)) -> mark#(X2), mark#(nil()) -> active#(nil()))
(active#(len(nil())) -> mark#(0()), mark#(0()) -> active#(0()))
(mark#(add(X1, X2)) -> add#(mark(X1), mark(X2)), add#(active(X1), X2) -> add#(X1, X2))
(mark#(add(X1, X2)) -> add#(mark(X1), mark(X2)), add#(mark(X1), X2) -> add#(X1, X2))
(mark#(add(X1, X2)) -> add#(mark(X1), mark(X2)), add#(X1, active(X2)) -> add#(X1, X2))
(mark#(add(X1, X2)) -> add#(mark(X1), mark(X2)), add#(X1, mark(X2)) -> add#(X1, X2))
(mark#(cons(X1, X2)) -> active#(cons(mark(X1), X2)), active#(len(cons(X, Z))) -> len#(Z))
(mark#(cons(X1, X2)) -> active#(cons(mark(X1), X2)), active#(len(cons(X, Z))) -> s#(len(Z)))
(mark#(cons(X1, X2)) -> active#(cons(mark(X1), X2)), active#(len(cons(X, Z))) -> mark#(s(len(Z))))
(mark#(cons(X1, X2)) -> active#(cons(mark(X1), X2)), active#(len(nil())) -> mark#(0()))
(mark#(cons(X1, X2)) -> active#(cons(mark(X1), X2)), active#(add(s(X), Y)) -> add#(X, Y))
(mark#(cons(X1, X2)) -> active#(cons(mark(X1), X2)), active#(add(s(X), Y)) -> s#(add(X, Y)))
(mark#(cons(X1, X2)) -> active#(cons(mark(X1), X2)), active#(add(s(X), Y)) -> mark#(s(add(X, Y))))
(mark#(cons(X1, X2)) -> active#(cons(mark(X1), X2)), active#(add(0(), X)) -> mark#(X))
(mark#(cons(X1, X2)) -> active#(cons(mark(X1), X2)), active#(from(X)) -> from#(s(X)))
(mark#(cons(X1, X2)) -> active#(cons(mark(X1), X2)), active#(from(X)) -> s#(X))
(mark#(cons(X1, X2)) -> active#(cons(mark(X1), X2)), active#(from(X)) -> cons#(X, from(s(X))))
(mark#(cons(X1, X2)) -> active#(cons(mark(X1), X2)), active#(from(X)) -> mark#(cons(X, from(s(X)))))
(mark#(cons(X1, X2)) -> active#(cons(mark(X1), X2)), active#(fst(s(X), cons(Y, Z))) -> cons#(Y, fst(X, Z)))
(mark#(cons(X1, X2)) -> active#(cons(mark(X1), X2)), active#(fst(s(X), cons(Y, Z))) -> fst#(X, Z))
(mark#(cons(X1, X2)) -> active#(cons(mark(X1), X2)), active#(fst(s(X), cons(Y, Z))) -> mark#(cons(Y, fst(X, Z))))
(mark#(cons(X1, X2)) -> active#(cons(mark(X1), X2)), active#(fst(0(), Z)) -> mark#(nil()))
(mark#(cons(X1, X2)) -> cons#(mark(X1), X2), cons#(active(X1), X2) -> cons#(X1, X2))
(mark#(cons(X1, X2)) -> cons#(mark(X1), X2), cons#(mark(X1), X2) -> cons#(X1, X2))
(mark#(cons(X1, X2)) -> cons#(mark(X1), X2), cons#(X1, active(X2)) -> cons#(X1, X2))
(mark#(cons(X1, X2)) -> cons#(mark(X1), X2), cons#(X1, mark(X2)) -> cons#(X1, X2))
(mark#(from(X)) -> mark#(X), mark#(len(X)) -> len#(mark(X)))
(mark#(from(X)) -> mark#(X), mark#(len(X)) -> active#(len(mark(X))))
(mark#(from(X)) -> mark#(X), mark#(len(X)) -> mark#(X))
(mark#(from(X)) -> mark#(X), mark#(add(X1, X2)) -> add#(mark(X1), mark(X2)))
(mark#(from(X)) -> mark#(X), mark#(add(X1, X2)) -> active#(add(mark(X1), mark(X2))))
(mark#(from(X)) -> mark#(X), mark#(add(X1, X2)) -> mark#(X2))
(mark#(from(X)) -> mark#(X), mark#(add(X1, X2)) -> mark#(X1))
(mark#(from(X)) -> mark#(X), mark#(from(X)) -> from#(mark(X)))
(mark#(from(X)) -> mark#(X), mark#(from(X)) -> active#(from(mark(X))))
(mark#(from(X)) -> mark#(X), mark#(from(X)) -> mark#(X))
(mark#(from(X)) -> mark#(X), mark#(s(X)) -> active#(s(X)))
(mark#(from(X)) -> mark#(X), mark#(cons(X1, X2)) -> cons#(mark(X1), X2))
(mark#(from(X)) -> mark#(X), mark#(cons(X1, X2)) -> active#(cons(mark(X1), X2)))
(mark#(from(X)) -> mark#(X), mark#(cons(X1, X2)) -> mark#(X1))
(mark#(from(X)) -> mark#(X), mark#(0()) -> active#(0()))
(mark#(from(X)) -> mark#(X), mark#(fst(X1, X2)) -> fst#(mark(X1), mark(X2)))
(mark#(from(X)) -> mark#(X), mark#(fst(X1, X2)) -> active#(fst(mark(X1), mark(X2))))
(mark#(from(X)) -> mark#(X), mark#(fst(X1, X2)) -> mark#(X2))
(mark#(from(X)) -> mark#(X), mark#(fst(X1, X2)) -> mark#(X1))
(mark#(from(X)) -> mark#(X), mark#(nil()) -> active#(nil()))
(active#(from(X)) -> s#(X), s#(active(X)) -> s#(X))
(active#(from(X)) -> 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))
(from#(mark(X)) -> from#(X), from#(active(X)) -> from#(X))
(from#(mark(X)) -> from#(X), from#(mark(X)) -> from#(X))
(len#(mark(X)) -> len#(X), len#(active(X)) -> len#(X))
(len#(mark(X)) -> len#(X), len#(mark(X)) -> len#(X))
(mark#(from(X)) -> active#(from(mark(X))), active#(len(cons(X, Z))) -> len#(Z))
(mark#(from(X)) -> active#(from(mark(X))), active#(len(cons(X, Z))) -> s#(len(Z)))
(mark#(from(X)) -> active#(from(mark(X))), active#(len(cons(X, Z))) -> mark#(s(len(Z))))
(mark#(from(X)) -> active#(from(mark(X))), active#(len(nil())) -> mark#(0()))
(mark#(from(X)) -> active#(from(mark(X))), active#(add(s(X), Y)) -> add#(X, Y))
(mark#(from(X)) -> active#(from(mark(X))), active#(add(s(X), Y)) -> s#(add(X, Y)))
(mark#(from(X)) -> active#(from(mark(X))), active#(add(s(X), Y)) -> mark#(s(add(X, Y))))
(mark#(from(X)) -> active#(from(mark(X))), active#(add(0(), X)) -> mark#(X))
(mark#(from(X)) -> active#(from(mark(X))), active#(from(X)) -> from#(s(X)))
(mark#(from(X)) -> active#(from(mark(X))), active#(from(X)) -> s#(X))
(mark#(from(X)) -> active#(from(mark(X))), active#(from(X)) -> cons#(X, from(s(X))))
(mark#(from(X)) -> active#(from(mark(X))), active#(from(X)) -> mark#(cons(X, from(s(X)))))
(mark#(from(X)) -> active#(from(mark(X))), active#(fst(s(X), cons(Y, Z))) -> cons#(Y, fst(X, Z)))
(mark#(from(X)) -> active#(from(mark(X))), active#(fst(s(X), cons(Y, Z))) -> fst#(X, Z))
(mark#(from(X)) -> active#(from(mark(X))), active#(fst(s(X), cons(Y, Z))) -> mark#(cons(Y, fst(X, Z))))
(mark#(from(X)) -> active#(from(mark(X))), active#(fst(0(), Z)) -> mark#(nil()))
(active#(add(s(X), Y)) -> mark#(s(add(X, Y))), mark#(len(X)) -> len#(mark(X)))
(active#(add(s(X), Y)) -> mark#(s(add(X, Y))), mark#(len(X)) -> active#(len(mark(X))))
(active#(add(s(X), Y)) -> mark#(s(add(X, Y))), mark#(len(X)) -> mark#(X))
(active#(add(s(X), Y)) -> mark#(s(add(X, Y))), mark#(add(X1, X2)) -> add#(mark(X1), mark(X2)))
(active#(add(s(X), Y)) -> mark#(s(add(X, Y))), mark#(add(X1, X2)) -> active#(add(mark(X1), mark(X2))))
(active#(add(s(X), Y)) -> mark#(s(add(X, Y))), mark#(add(X1, X2)) -> mark#(X2))
(active#(add(s(X), Y)) -> mark#(s(add(X, Y))), mark#(add(X1, X2)) -> mark#(X1))
(active#(add(s(X), Y)) -> mark#(s(add(X, Y))), mark#(from(X)) -> from#(mark(X)))
(active#(add(s(X), Y)) -> mark#(s(add(X, Y))), mark#(from(X)) -> active#(from(mark(X))))
(active#(add(s(X), Y)) -> mark#(s(add(X, Y))), mark#(from(X)) -> mark#(X))
(active#(add(s(X), Y)) -> mark#(s(add(X, Y))), mark#(s(X)) -> active#(s(X)))
(active#(add(s(X), Y)) -> mark#(s(add(X, Y))), mark#(cons(X1, X2)) -> cons#(mark(X1), X2))
(active#(add(s(X), Y)) -> mark#(s(add(X, Y))), mark#(cons(X1, X2)) -> active#(cons(mark(X1), X2)))
(active#(add(s(X), Y)) -> mark#(s(add(X, Y))), mark#(cons(X1, X2)) -> mark#(X1))
(active#(add(s(X), Y)) -> mark#(s(add(X, Y))), mark#(fst(X1, X2)) -> fst#(mark(X1), mark(X2)))
(active#(add(s(X), Y)) -> mark#(s(add(X, Y))), mark#(fst(X1, X2)) -> active#(fst(mark(X1), mark(X2))))
(active#(add(s(X), Y)) -> mark#(s(add(X, Y))), mark#(fst(X1, X2)) -> mark#(X2))
(active#(add(s(X), Y)) -> mark#(s(add(X, Y))), mark#(fst(X1, X2)) -> mark#(X1))
(fst#(X1, mark(X2)) -> fst#(X1, X2), fst#(active(X1), X2) -> fst#(X1, X2))
(fst#(X1, mark(X2)) -> fst#(X1, X2), fst#(mark(X1), X2) -> fst#(X1, X2))
(fst#(X1, mark(X2)) -> fst#(X1, X2), fst#(X1, active(X2)) -> fst#(X1, X2))
(fst#(X1, mark(X2)) -> fst#(X1, X2), fst#(X1, mark(X2)) -> fst#(X1, X2))
(fst#(mark(X1), X2) -> fst#(X1, X2), fst#(active(X1), X2) -> fst#(X1, X2))
(fst#(mark(X1), X2) -> fst#(X1, X2), fst#(mark(X1), X2) -> fst#(X1, X2))
(fst#(mark(X1), X2) -> fst#(X1, X2), fst#(X1, active(X2)) -> fst#(X1, X2))
(fst#(mark(X1), X2) -> fst#(X1, X2), fst#(X1, mark(X2)) -> fst#(X1, X2))
(cons#(X1, mark(X2)) -> cons#(X1, X2), cons#(active(X1), 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#(X1, active(X2)) -> cons#(X1, X2))
(cons#(X1, mark(X2)) -> cons#(X1, X2), cons#(X1, mark(X2)) -> cons#(X1, X2))
(cons#(mark(X1), X2) -> cons#(X1, X2), cons#(active(X1), 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#(X1, active(X2)) -> cons#(X1, X2))
(cons#(mark(X1), X2) -> cons#(X1, X2), cons#(X1, mark(X2)) -> cons#(X1, X2))
(add#(X1, mark(X2)) -> add#(X1, X2), add#(active(X1), X2) -> add#(X1, X2))
(add#(X1, mark(X2)) -> add#(X1, X2), add#(mark(X1), X2) -> add#(X1, X2))
(add#(X1, mark(X2)) -> add#(X1, X2), add#(X1, active(X2)) -> add#(X1, X2))
(add#(X1, mark(X2)) -> add#(X1, X2), add#(X1, mark(X2)) -> add#(X1, X2))
(add#(mark(X1), X2) -> add#(X1, X2), add#(active(X1), X2) -> add#(X1, X2))
(add#(mark(X1), X2) -> add#(X1, X2), add#(mark(X1), X2) -> add#(X1, X2))
(add#(mark(X1), X2) -> add#(X1, X2), add#(X1, active(X2)) -> add#(X1, X2))
(add#(mark(X1), X2) -> add#(X1, X2), add#(X1, mark(X2)) -> add#(X1, X2))
(active#(add(s(X), Y)) -> add#(X, Y), add#(active(X1), X2) -> add#(X1, X2))
(active#(add(s(X), Y)) -> add#(X, Y), add#(mark(X1), X2) -> add#(X1, X2))
(active#(add(s(X), Y)) -> add#(X, Y), add#(X1, active(X2)) -> add#(X1, X2))
(active#(add(s(X), Y)) -> add#(X, Y), add#(X1, mark(X2)) -> add#(X1, X2))
(mark#(fst(X1, X2)) -> active#(fst(mark(X1), mark(X2))), active#(len(cons(X, Z))) -> len#(Z))
(mark#(fst(X1, X2)) -> active#(fst(mark(X1), mark(X2))), active#(len(cons(X, Z))) -> s#(len(Z)))
(mark#(fst(X1, X2)) -> active#(fst(mark(X1), mark(X2))), active#(len(cons(X, Z))) -> mark#(s(len(Z))))
(mark#(fst(X1, X2)) -> active#(fst(mark(X1), mark(X2))), active#(len(nil())) -> mark#(0()))
(mark#(fst(X1, X2)) -> active#(fst(mark(X1), mark(X2))), active#(add(s(X), Y)) -> add#(X, Y))
(mark#(fst(X1, X2)) -> active#(fst(mark(X1), mark(X2))), active#(add(s(X), Y)) -> s#(add(X, Y)))
(mark#(fst(X1, X2)) -> active#(fst(mark(X1), mark(X2))), active#(add(s(X), Y)) -> mark#(s(add(X, Y))))
(mark#(fst(X1, X2)) -> active#(fst(mark(X1), mark(X2))), active#(add(0(), X)) -> mark#(X))
(mark#(fst(X1, X2)) -> active#(fst(mark(X1), mark(X2))), active#(from(X)) -> from#(s(X)))
(mark#(fst(X1, X2)) -> active#(fst(mark(X1), mark(X2))), active#(from(X)) -> s#(X))
(mark#(fst(X1, X2)) -> active#(fst(mark(X1), mark(X2))), active#(from(X)) -> cons#(X, from(s(X))))
(mark#(fst(X1, X2)) -> active#(fst(mark(X1), mark(X2))), active#(from(X)) -> mark#(cons(X, from(s(X)))))
(mark#(fst(X1, X2)) -> active#(fst(mark(X1), mark(X2))), active#(fst(s(X), cons(Y, Z))) -> cons#(Y, fst(X, Z)))
(mark#(fst(X1, X2)) -> active#(fst(mark(X1), mark(X2))), active#(fst(s(X), cons(Y, Z))) -> fst#(X, Z))
(mark#(fst(X1, X2)) -> active#(fst(mark(X1), mark(X2))), active#(fst(s(X), cons(Y, Z))) -> mark#(cons(Y, fst(X, Z))))
(mark#(fst(X1, X2)) -> active#(fst(mark(X1), mark(X2))), active#(fst(0(), Z)) -> mark#(nil()))
(active#(from(X)) -> mark#(cons(X, from(s(X)))), mark#(len(X)) -> len#(mark(X)))
(active#(from(X)) -> mark#(cons(X, from(s(X)))), mark#(len(X)) -> active#(len(mark(X))))
(active#(from(X)) -> mark#(cons(X, from(s(X)))), mark#(len(X)) -> mark#(X))
(active#(from(X)) -> mark#(cons(X, from(s(X)))), mark#(add(X1, X2)) -> add#(mark(X1), mark(X2)))
(active#(from(X)) -> mark#(cons(X, from(s(X)))), mark#(add(X1, X2)) -> active#(add(mark(X1), mark(X2))))
(active#(from(X)) -> mark#(cons(X, from(s(X)))), mark#(add(X1, X2)) -> mark#(X2))
(active#(from(X)) -> mark#(cons(X, from(s(X)))), mark#(add(X1, X2)) -> mark#(X1))
(active#(from(X)) -> mark#(cons(X, from(s(X)))), mark#(from(X)) -> from#(mark(X)))
(active#(from(X)) -> mark#(cons(X, from(s(X)))), mark#(from(X)) -> active#(from(mark(X))))
(active#(from(X)) -> mark#(cons(X, from(s(X)))), mark#(from(X)) -> mark#(X))
(active#(from(X)) -> mark#(cons(X, from(s(X)))), mark#(s(X)) -> active#(s(X)))
(active#(from(X)) -> mark#(cons(X, from(s(X)))), mark#(cons(X1, X2)) -> cons#(mark(X1), X2))
(active#(from(X)) -> mark#(cons(X, from(s(X)))), mark#(cons(X1, X2)) -> active#(cons(mark(X1), X2)))
(active#(from(X)) -> mark#(cons(X, from(s(X)))), mark#(cons(X1, X2)) -> mark#(X1))
(active#(from(X)) -> mark#(cons(X, from(s(X)))), mark#(fst(X1, X2)) -> fst#(mark(X1), mark(X2)))
(active#(from(X)) -> mark#(cons(X, from(s(X)))), mark#(fst(X1, X2)) -> active#(fst(mark(X1), mark(X2))))
(active#(from(X)) -> mark#(cons(X, from(s(X)))), mark#(fst(X1, X2)) -> mark#(X2))
(active#(from(X)) -> mark#(cons(X, from(s(X)))), mark#(fst(X1, X2)) -> mark#(X1))
(mark#(cons(X1, X2)) -> mark#(X1), mark#(len(X)) -> len#(mark(X)))
(mark#(cons(X1, X2)) -> mark#(X1), mark#(len(X)) -> active#(len(mark(X))))
(mark#(cons(X1, X2)) -> mark#(X1), mark#(len(X)) -> mark#(X))
(mark#(cons(X1, X2)) -> mark#(X1), mark#(add(X1, X2)) -> add#(mark(X1), mark(X2)))
(mark#(cons(X1, X2)) -> mark#(X1), mark#(add(X1, X2)) -> active#(add(mark(X1), mark(X2))))
(mark#(cons(X1, X2)) -> mark#(X1), mark#(add(X1, X2)) -> mark#(X2))
(mark#(cons(X1, X2)) -> mark#(X1), mark#(add(X1, X2)) -> mark#(X1))
(mark#(cons(X1, X2)) -> mark#(X1), mark#(from(X)) -> from#(mark(X)))
(mark#(cons(X1, X2)) -> mark#(X1), mark#(from(X)) -> active#(from(mark(X))))
(mark#(cons(X1, X2)) -> mark#(X1), mark#(from(X)) -> mark#(X))
(mark#(cons(X1, X2)) -> mark#(X1), mark#(s(X)) -> active#(s(X)))
(mark#(cons(X1, X2)) -> mark#(X1), mark#(cons(X1, X2)) -> cons#(mark(X1), X2))
(mark#(cons(X1, X2)) -> mark#(X1), mark#(cons(X1, X2)) -> active#(cons(mark(X1), X2)))
(mark#(cons(X1, X2)) -> mark#(X1), mark#(cons(X1, X2)) -> mark#(X1))
(mark#(cons(X1, X2)) -> mark#(X1), mark#(0()) -> active#(0()))
(mark#(cons(X1, X2)) -> mark#(X1), mark#(fst(X1, X2)) -> fst#(mark(X1), mark(X2)))
(mark#(cons(X1, X2)) -> mark#(X1), mark#(fst(X1, X2)) -> active#(fst(mark(X1), mark(X2))))
(mark#(cons(X1, X2)) -> mark#(X1), mark#(fst(X1, X2)) -> mark#(X2))
(mark#(cons(X1, X2)) -> mark#(X1), mark#(fst(X1, X2)) -> mark#(X1))
(mark#(cons(X1, X2)) -> mark#(X1), mark#(nil()) -> active#(nil()))
(mark#(s(X)) -> active#(s(X)), active#(len(cons(X, Z))) -> len#(Z))
(mark#(s(X)) -> active#(s(X)), active#(len(cons(X, Z))) -> s#(len(Z)))
(mark#(s(X)) -> active#(s(X)), active#(len(cons(X, Z))) -> mark#(s(len(Z))))
(mark#(s(X)) -> active#(s(X)), active#(len(nil())) -> mark#(0()))
(mark#(s(X)) -> active#(s(X)), active#(add(s(X), Y)) -> add#(X, Y))
(mark#(s(X)) -> active#(s(X)), active#(add(s(X), Y)) -> s#(add(X, Y)))
(mark#(s(X)) -> active#(s(X)), active#(add(s(X), Y)) -> mark#(s(add(X, Y))))
(mark#(s(X)) -> active#(s(X)), active#(add(0(), X)) -> mark#(X))
(mark#(s(X)) -> active#(s(X)), active#(from(X)) -> from#(s(X)))
(mark#(s(X)) -> active#(s(X)), active#(from(X)) -> s#(X))
(mark#(s(X)) -> active#(s(X)), active#(from(X)) -> cons#(X, from(s(X))))
(mark#(s(X)) -> active#(s(X)), active#(from(X)) -> mark#(cons(X, from(s(X)))))
(mark#(s(X)) -> active#(s(X)), active#(fst(s(X), cons(Y, Z))) -> cons#(Y, fst(X, Z)))
(mark#(s(X)) -> active#(s(X)), active#(fst(s(X), cons(Y, Z))) -> fst#(X, Z))
(mark#(s(X)) -> active#(s(X)), active#(fst(s(X), cons(Y, Z))) -> mark#(cons(Y, fst(X, Z))))
(mark#(s(X)) -> active#(s(X)), active#(fst(0(), Z)) -> mark#(nil()))
(mark#(len(X)) -> len#(mark(X)), len#(active(X)) -> len#(X))
(mark#(len(X)) -> len#(mark(X)), len#(mark(X)) -> len#(X))
(active#(len(cons(X, Z))) -> s#(len(Z)), s#(active(X)) -> s#(X))
(active#(len(cons(X, Z))) -> s#(len(Z)), s#(mark(X)) -> s#(X))
(active#(len(cons(X, Z))) -> len#(Z), len#(active(X)) -> len#(X))
(active#(len(cons(X, Z))) -> len#(Z), len#(mark(X)) -> len#(X))
(active#(fst(s(X), cons(Y, Z))) -> fst#(X, Z), fst#(X1, mark(X2)) -> fst#(X1, X2))
(active#(fst(s(X), cons(Y, Z))) -> fst#(X, Z), fst#(X1, active(X2)) -> fst#(X1, X2))
(active#(fst(s(X), cons(Y, Z))) -> fst#(X, Z), fst#(mark(X1), X2) -> fst#(X1, X2))
(active#(fst(s(X), cons(Y, Z))) -> fst#(X, Z), fst#(active(X1), X2) -> fst#(X1, X2))
(active#(from(X)) -> from#(s(X)), from#(mark(X)) -> from#(X))
(active#(from(X)) -> from#(s(X)), from#(active(X)) -> from#(X))
(mark#(from(X)) -> from#(mark(X)), from#(mark(X)) -> from#(X))
(mark#(from(X)) -> from#(mark(X)), from#(active(X)) -> from#(X))
(mark#(add(X1, X2)) -> mark#(X1), mark#(nil()) -> active#(nil()))
(mark#(add(X1, X2)) -> mark#(X1), mark#(fst(X1, X2)) -> mark#(X1))
(mark#(add(X1, X2)) -> mark#(X1), mark#(fst(X1, X2)) -> mark#(X2))
(mark#(add(X1, X2)) -> mark#(X1), mark#(fst(X1, X2)) -> active#(fst(mark(X1), mark(X2))))
(mark#(add(X1, X2)) -> mark#(X1), mark#(fst(X1, X2)) -> fst#(mark(X1), mark(X2)))
(mark#(add(X1, X2)) -> mark#(X1), mark#(0()) -> active#(0()))
(mark#(add(X1, X2)) -> mark#(X1), mark#(cons(X1, X2)) -> mark#(X1))
(mark#(add(X1, X2)) -> mark#(X1), mark#(cons(X1, X2)) -> active#(cons(mark(X1), X2)))
(mark#(add(X1, X2)) -> mark#(X1), mark#(cons(X1, X2)) -> cons#(mark(X1), X2))
(mark#(add(X1, X2)) -> mark#(X1), mark#(s(X)) -> active#(s(X)))
(mark#(add(X1, X2)) -> mark#(X1), mark#(from(X)) -> mark#(X))
(mark#(add(X1, X2)) -> mark#(X1), mark#(from(X)) -> active#(from(mark(X))))
(mark#(add(X1, X2)) -> mark#(X1), mark#(from(X)) -> from#(mark(X)))
(mark#(add(X1, X2)) -> mark#(X1), mark#(add(X1, X2)) -> mark#(X1))
(mark#(add(X1, X2)) -> mark#(X1), mark#(add(X1, X2)) -> mark#(X2))
(mark#(add(X1, X2)) -> mark#(X1), mark#(add(X1, X2)) -> active#(add(mark(X1), mark(X2))))
(mark#(add(X1, X2)) -> mark#(X1), mark#(add(X1, X2)) -> add#(mark(X1), mark(X2)))
(mark#(add(X1, X2)) -> mark#(X1), mark#(len(X)) -> mark#(X))
(mark#(add(X1, X2)) -> mark#(X1), mark#(len(X)) -> active#(len(mark(X))))
(mark#(add(X1, X2)) -> mark#(X1), mark#(len(X)) -> len#(mark(X)))
(mark#(fst(X1, X2)) -> mark#(X1), mark#(nil()) -> active#(nil()))
(mark#(fst(X1, X2)) -> mark#(X1), mark#(fst(X1, X2)) -> mark#(X1))
(mark#(fst(X1, X2)) -> mark#(X1), mark#(fst(X1, X2)) -> mark#(X2))
(mark#(fst(X1, X2)) -> mark#(X1), mark#(fst(X1, X2)) -> active#(fst(mark(X1), mark(X2))))
(mark#(fst(X1, X2)) -> mark#(X1), mark#(fst(X1, X2)) -> fst#(mark(X1), mark(X2)))
(mark#(fst(X1, X2)) -> mark#(X1), mark#(0()) -> active#(0()))
(mark#(fst(X1, X2)) -> mark#(X1), mark#(cons(X1, X2)) -> mark#(X1))
(mark#(fst(X1, X2)) -> mark#(X1), mark#(cons(X1, X2)) -> active#(cons(mark(X1), X2)))
(mark#(fst(X1, X2)) -> mark#(X1), mark#(cons(X1, X2)) -> cons#(mark(X1), X2))
(mark#(fst(X1, X2)) -> mark#(X1), mark#(s(X)) -> active#(s(X)))
(mark#(fst(X1, X2)) -> mark#(X1), mark#(from(X)) -> mark#(X))
(mark#(fst(X1, X2)) -> mark#(X1), mark#(from(X)) -> active#(from(mark(X))))
(mark#(fst(X1, X2)) -> mark#(X1), mark#(from(X)) -> from#(mark(X)))
(mark#(fst(X1, X2)) -> mark#(X1), mark#(add(X1, X2)) -> mark#(X1))
(mark#(fst(X1, X2)) -> mark#(X1), mark#(add(X1, X2)) -> mark#(X2))
(mark#(fst(X1, X2)) -> mark#(X1), mark#(add(X1, X2)) -> active#(add(mark(X1), mark(X2))))
(mark#(fst(X1, X2)) -> mark#(X1), mark#(add(X1, X2)) -> add#(mark(X1), mark(X2)))
(mark#(fst(X1, X2)) -> mark#(X1), mark#(len(X)) -> mark#(X))
(mark#(fst(X1, X2)) -> mark#(X1), mark#(len(X)) -> active#(len(mark(X))))
(mark#(fst(X1, X2)) -> mark#(X1), mark#(len(X)) -> len#(mark(X)))
(mark#(add(X1, X2)) -> active#(add(mark(X1), mark(X2))), active#(fst(0(), Z)) -> mark#(nil()))
(mark#(add(X1, X2)) -> active#(add(mark(X1), mark(X2))), active#(fst(s(X), cons(Y, Z))) -> mark#(cons(Y, fst(X, Z))))
(mark#(add(X1, X2)) -> active#(add(mark(X1), mark(X2))), active#(fst(s(X), cons(Y, Z))) -> fst#(X, Z))
(mark#(add(X1, X2)) -> active#(add(mark(X1), mark(X2))), active#(fst(s(X), cons(Y, Z))) -> cons#(Y, fst(X, Z)))
(mark#(add(X1, X2)) -> active#(add(mark(X1), mark(X2))), active#(from(X)) -> mark#(cons(X, from(s(X)))))
(mark#(add(X1, X2)) -> active#(add(mark(X1), mark(X2))), active#(from(X)) -> cons#(X, from(s(X))))
(mark#(add(X1, X2)) -> active#(add(mark(X1), mark(X2))), active#(from(X)) -> s#(X))
(mark#(add(X1, X2)) -> active#(add(mark(X1), mark(X2))), active#(from(X)) -> from#(s(X)))
(mark#(add(X1, X2)) -> active#(add(mark(X1), mark(X2))), active#(add(0(), X)) -> mark#(X))
(mark#(add(X1, X2)) -> active#(add(mark(X1), mark(X2))), active#(add(s(X), Y)) -> mark#(s(add(X, Y))))
(mark#(add(X1, X2)) -> active#(add(mark(X1), mark(X2))), active#(add(s(X), Y)) -> s#(add(X, Y)))
(mark#(add(X1, X2)) -> active#(add(mark(X1), mark(X2))), active#(add(s(X), Y)) -> add#(X, Y))
(mark#(add(X1, X2)) -> active#(add(mark(X1), mark(X2))), active#(len(nil())) -> mark#(0()))
(mark#(add(X1, X2)) -> active#(add(mark(X1), mark(X2))), active#(len(cons(X, Z))) -> mark#(s(len(Z))))
(mark#(add(X1, X2)) -> active#(add(mark(X1), mark(X2))), active#(len(cons(X, Z))) -> s#(len(Z)))
(mark#(add(X1, X2)) -> active#(add(mark(X1), mark(X2))), active#(len(cons(X, Z))) -> len#(Z))
(active#(from(X)) -> cons#(X, from(s(X))), cons#(X1, mark(X2)) -> cons#(X1, X2))
(active#(from(X)) -> cons#(X, from(s(X))), cons#(X1, active(X2)) -> cons#(X1, X2))
(active#(from(X)) -> cons#(X, from(s(X))), cons#(mark(X1), X2) -> cons#(X1, X2))
(active#(from(X)) -> cons#(X, from(s(X))), cons#(active(X1), X2) -> cons#(X1, X2))
(add#(active(X1), X2) -> add#(X1, X2), add#(X1, mark(X2)) -> add#(X1, X2))
(add#(active(X1), X2) -> add#(X1, X2), add#(X1, active(X2)) -> add#(X1, X2))
(add#(active(X1), X2) -> add#(X1, X2), add#(mark(X1), X2) -> add#(X1, X2))
(add#(active(X1), X2) -> add#(X1, X2), add#(active(X1), X2) -> add#(X1, X2))
(add#(X1, active(X2)) -> add#(X1, X2), add#(X1, mark(X2)) -> add#(X1, X2))
(add#(X1, active(X2)) -> add#(X1, X2), add#(X1, active(X2)) -> add#(X1, X2))
(add#(X1, active(X2)) -> add#(X1, X2), add#(mark(X1), X2) -> add#(X1, X2))
(add#(X1, active(X2)) -> add#(X1, X2), add#(active(X1), X2) -> add#(X1, X2))
(cons#(active(X1), X2) -> cons#(X1, X2), cons#(X1, mark(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#(mark(X1), X2) -> cons#(X1, X2))
(cons#(active(X1), X2) -> cons#(X1, X2), cons#(active(X1), X2) -> cons#(X1, X2))
(cons#(X1, active(X2)) -> cons#(X1, X2), cons#(X1, mark(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#(mark(X1), X2) -> cons#(X1, X2))
(cons#(X1, active(X2)) -> cons#(X1, X2), cons#(active(X1), X2) -> cons#(X1, X2))
(fst#(active(X1), X2) -> fst#(X1, X2), fst#(X1, mark(X2)) -> fst#(X1, X2))
(fst#(active(X1), X2) -> fst#(X1, X2), fst#(X1, active(X2)) -> fst#(X1, X2))
(fst#(active(X1), X2) -> fst#(X1, X2), fst#(mark(X1), X2) -> fst#(X1, X2))
(fst#(active(X1), X2) -> fst#(X1, X2), fst#(active(X1), X2) -> fst#(X1, X2))
(fst#(X1, active(X2)) -> fst#(X1, X2), fst#(X1, mark(X2)) -> fst#(X1, X2))
(fst#(X1, active(X2)) -> fst#(X1, X2), fst#(X1, active(X2)) -> fst#(X1, X2))
(fst#(X1, active(X2)) -> fst#(X1, X2), fst#(mark(X1), X2) -> fst#(X1, X2))
(fst#(X1, active(X2)) -> fst#(X1, X2), fst#(active(X1), X2) -> fst#(X1, X2))
(active#(len(cons(X, Z))) -> mark#(s(len(Z))), mark#(fst(X1, X2)) -> mark#(X1))
(active#(len(cons(X, Z))) -> mark#(s(len(Z))), mark#(fst(X1, X2)) -> mark#(X2))
(active#(len(cons(X, Z))) -> mark#(s(len(Z))), mark#(fst(X1, X2)) -> active#(fst(mark(X1), mark(X2))))
(active#(len(cons(X, Z))) -> mark#(s(len(Z))), mark#(fst(X1, X2)) -> fst#(mark(X1), mark(X2)))
(active#(len(cons(X, Z))) -> mark#(s(len(Z))), mark#(cons(X1, X2)) -> mark#(X1))
(active#(len(cons(X, Z))) -> mark#(s(len(Z))), mark#(cons(X1, X2)) -> active#(cons(mark(X1), X2)))
(active#(len(cons(X, Z))) -> mark#(s(len(Z))), mark#(cons(X1, X2)) -> cons#(mark(X1), X2))
(active#(len(cons(X, Z))) -> mark#(s(len(Z))), mark#(s(X)) -> active#(s(X)))
(active#(len(cons(X, Z))) -> mark#(s(len(Z))), mark#(from(X)) -> mark#(X))
(active#(len(cons(X, Z))) -> mark#(s(len(Z))), mark#(from(X)) -> active#(from(mark(X))))
(active#(len(cons(X, Z))) -> mark#(s(len(Z))), mark#(from(X)) -> from#(mark(X)))
(active#(len(cons(X, Z))) -> mark#(s(len(Z))), mark#(add(X1, X2)) -> mark#(X1))
(active#(len(cons(X, Z))) -> mark#(s(len(Z))), mark#(add(X1, X2)) -> mark#(X2))
(active#(len(cons(X, Z))) -> mark#(s(len(Z))), mark#(add(X1, X2)) -> active#(add(mark(X1), mark(X2))))
(active#(len(cons(X, Z))) -> mark#(s(len(Z))), mark#(add(X1, X2)) -> add#(mark(X1), mark(X2)))
(active#(len(cons(X, Z))) -> mark#(s(len(Z))), mark#(len(X)) -> mark#(X))
(active#(len(cons(X, Z))) -> mark#(s(len(Z))), mark#(len(X)) -> active#(len(mark(X))))
(active#(len(cons(X, Z))) -> mark#(s(len(Z))), mark#(len(X)) -> len#(mark(X)))
(mark#(len(X)) -> active#(len(mark(X))), active#(fst(0(), Z)) -> mark#(nil()))
(mark#(len(X)) -> active#(len(mark(X))), active#(fst(s(X), cons(Y, Z))) -> mark#(cons(Y, fst(X, Z))))
(mark#(len(X)) -> active#(len(mark(X))), active#(fst(s(X), cons(Y, Z))) -> fst#(X, Z))
(mark#(len(X)) -> active#(len(mark(X))), active#(fst(s(X), cons(Y, Z))) -> cons#(Y, fst(X, Z)))
(mark#(len(X)) -> active#(len(mark(X))), active#(from(X)) -> mark#(cons(X, from(s(X)))))
(mark#(len(X)) -> active#(len(mark(X))), active#(from(X)) -> cons#(X, from(s(X))))
(mark#(len(X)) -> active#(len(mark(X))), active#(from(X)) -> s#(X))
(mark#(len(X)) -> active#(len(mark(X))), active#(from(X)) -> from#(s(X)))
(mark#(len(X)) -> active#(len(mark(X))), active#(add(0(), X)) -> mark#(X))
(mark#(len(X)) -> active#(len(mark(X))), active#(add(s(X), Y)) -> mark#(s(add(X, Y))))
(mark#(len(X)) -> active#(len(mark(X))), active#(add(s(X), Y)) -> s#(add(X, Y)))
(mark#(len(X)) -> active#(len(mark(X))), active#(add(s(X), Y)) -> add#(X, Y))
(mark#(len(X)) -> active#(len(mark(X))), active#(len(nil())) -> mark#(0()))
(mark#(len(X)) -> active#(len(mark(X))), active#(len(cons(X, Z))) -> mark#(s(len(Z))))
(mark#(len(X)) -> active#(len(mark(X))), active#(len(cons(X, Z))) -> s#(len(Z)))
(mark#(len(X)) -> active#(len(mark(X))), active#(len(cons(X, Z))) -> len#(Z))
(len#(active(X)) -> len#(X), len#(mark(X)) -> len#(X))
(len#(active(X)) -> len#(X), len#(active(X)) -> len#(X))
(from#(active(X)) -> from#(X), from#(mark(X)) -> from#(X))
(from#(active(X)) -> from#(X), from#(active(X)) -> from#(X))
(s#(active(X)) -> s#(X), s#(mark(X)) -> s#(X))
(s#(active(X)) -> s#(X), s#(active(X)) -> s#(X))
(active#(add(0(), X)) -> mark#(X), mark#(nil()) -> active#(nil()))
(active#(add(0(), X)) -> mark#(X), mark#(fst(X1, X2)) -> mark#(X1))
(active#(add(0(), X)) -> mark#(X), mark#(fst(X1, X2)) -> mark#(X2))
(active#(add(0(), X)) -> mark#(X), mark#(fst(X1, X2)) -> active#(fst(mark(X1), mark(X2))))
(active#(add(0(), X)) -> mark#(X), mark#(fst(X1, X2)) -> fst#(mark(X1), mark(X2)))
(active#(add(0(), X)) -> mark#(X), mark#(0()) -> active#(0()))
(active#(add(0(), X)) -> mark#(X), mark#(cons(X1, X2)) -> mark#(X1))
(active#(add(0(), X)) -> mark#(X), mark#(cons(X1, X2)) -> active#(cons(mark(X1), X2)))
(active#(add(0(), X)) -> mark#(X), mark#(cons(X1, X2)) -> cons#(mark(X1), X2))
(active#(add(0(), X)) -> mark#(X), mark#(s(X)) -> active#(s(X)))
(active#(add(0(), X)) -> mark#(X), mark#(from(X)) -> mark#(X))
(active#(add(0(), X)) -> mark#(X), mark#(from(X)) -> active#(from(mark(X))))
(active#(add(0(), X)) -> mark#(X), mark#(from(X)) -> from#(mark(X)))
(active#(add(0(), X)) -> mark#(X), mark#(add(X1, X2)) -> mark#(X1))
(active#(add(0(), X)) -> mark#(X), mark#(add(X1, X2)) -> mark#(X2))
(active#(add(0(), X)) -> mark#(X), mark#(add(X1, X2)) -> active#(add(mark(X1), mark(X2))))
(active#(add(0(), X)) -> mark#(X), mark#(add(X1, X2)) -> add#(mark(X1), mark(X2)))
(active#(add(0(), X)) -> mark#(X), mark#(len(X)) -> mark#(X))
(active#(add(0(), X)) -> mark#(X), mark#(len(X)) -> active#(len(mark(X))))
(active#(add(0(), X)) -> mark#(X), mark#(len(X)) -> len#(mark(X)))
(mark#(len(X)) -> mark#(X), mark#(nil()) -> active#(nil()))
(mark#(len(X)) -> mark#(X), mark#(fst(X1, X2)) -> mark#(X1))
(mark#(len(X)) -> mark#(X), mark#(fst(X1, X2)) -> mark#(X2))
(mark#(len(X)) -> mark#(X), mark#(fst(X1, X2)) -> active#(fst(mark(X1), mark(X2))))
(mark#(len(X)) -> mark#(X), mark#(fst(X1, X2)) -> fst#(mark(X1), mark(X2)))
(mark#(len(X)) -> mark#(X), mark#(0()) -> active#(0()))
(mark#(len(X)) -> mark#(X), mark#(cons(X1, X2)) -> mark#(X1))
(mark#(len(X)) -> mark#(X), mark#(cons(X1, X2)) -> active#(cons(mark(X1), X2)))
(mark#(len(X)) -> mark#(X), mark#(cons(X1, X2)) -> cons#(mark(X1), X2))
(mark#(len(X)) -> mark#(X), mark#(s(X)) -> active#(s(X)))
(mark#(len(X)) -> mark#(X), mark#(from(X)) -> mark#(X))
(mark#(len(X)) -> mark#(X), mark#(from(X)) -> active#(from(mark(X))))
(mark#(len(X)) -> mark#(X), mark#(from(X)) -> from#(mark(X)))
(mark#(len(X)) -> mark#(X), mark#(add(X1, X2)) -> mark#(X1))
(mark#(len(X)) -> mark#(X), mark#(add(X1, X2)) -> mark#(X2))
(mark#(len(X)) -> mark#(X), mark#(add(X1, X2)) -> active#(add(mark(X1), mark(X2))))
(mark#(len(X)) -> mark#(X), mark#(add(X1, X2)) -> add#(mark(X1), mark(X2)))
(mark#(len(X)) -> mark#(X), mark#(len(X)) -> mark#(X))
(mark#(len(X)) -> mark#(X), mark#(len(X)) -> active#(len(mark(X))))
(mark#(len(X)) -> mark#(X), mark#(len(X)) -> len#(mark(X)))
(active#(fst(s(X), cons(Y, Z))) -> cons#(Y, fst(X, Z)), cons#(X1, mark(X2)) -> cons#(X1, X2))
(active#(fst(s(X), cons(Y, Z))) -> cons#(Y, fst(X, Z)), cons#(X1, active(X2)) -> cons#(X1, X2))
(active#(fst(s(X), cons(Y, Z))) -> cons#(Y, fst(X, Z)), cons#(mark(X1), X2) -> cons#(X1, X2))
(active#(fst(s(X), cons(Y, Z))) -> cons#(Y, fst(X, Z)), cons#(active(X1), X2) -> cons#(X1, X2))
(active#(add(s(X), Y)) -> s#(add(X, Y)), s#(mark(X)) -> s#(X))
(active#(add(s(X), Y)) -> s#(add(X, Y)), s#(active(X)) -> s#(X))
(active#(fst(s(X), cons(Y, Z))) -> mark#(cons(Y, fst(X, Z))), mark#(fst(X1, X2)) -> mark#(X1))
(active#(fst(s(X), cons(Y, Z))) -> mark#(cons(Y, fst(X, Z))), mark#(fst(X1, X2)) -> mark#(X2))
(active#(fst(s(X), cons(Y, Z))) -> mark#(cons(Y, fst(X, Z))), mark#(fst(X1, X2)) -> active#(fst(mark(X1), mark(X2))))
(active#(fst(s(X), cons(Y, Z))) -> mark#(cons(Y, fst(X, Z))), mark#(fst(X1, X2)) -> fst#(mark(X1), mark(X2)))
(active#(fst(s(X), cons(Y, Z))) -> mark#(cons(Y, fst(X, Z))), mark#(cons(X1, X2)) -> mark#(X1))
(active#(fst(s(X), cons(Y, Z))) -> mark#(cons(Y, fst(X, Z))), mark#(cons(X1, X2)) -> active#(cons(mark(X1), X2)))
(active#(fst(s(X), cons(Y, Z))) -> mark#(cons(Y, fst(X, Z))), mark#(cons(X1, X2)) -> cons#(mark(X1), X2))
(active#(fst(s(X), cons(Y, Z))) -> mark#(cons(Y, fst(X, Z))), mark#(s(X)) -> active#(s(X)))
(active#(fst(s(X), cons(Y, Z))) -> mark#(cons(Y, fst(X, Z))), mark#(from(X)) -> mark#(X))
(active#(fst(s(X), cons(Y, Z))) -> mark#(cons(Y, fst(X, Z))), mark#(from(X)) -> active#(from(mark(X))))
(active#(fst(s(X), cons(Y, Z))) -> mark#(cons(Y, fst(X, Z))), mark#(from(X)) -> from#(mark(X)))
(active#(fst(s(X), cons(Y, Z))) -> mark#(cons(Y, fst(X, Z))), mark#(add(X1, X2)) -> mark#(X1))
(active#(fst(s(X), cons(Y, Z))) -> mark#(cons(Y, fst(X, Z))), mark#(add(X1, X2)) -> mark#(X2))
(active#(fst(s(X), cons(Y, Z))) -> mark#(cons(Y, fst(X, Z))), mark#(add(X1, X2)) -> active#(add(mark(X1), mark(X2))))
(active#(fst(s(X), cons(Y, Z))) -> mark#(cons(Y, fst(X, Z))), mark#(add(X1, X2)) -> add#(mark(X1), mark(X2)))
(active#(fst(s(X), cons(Y, Z))) -> mark#(cons(Y, fst(X, Z))), mark#(len(X)) -> mark#(X))
(active#(fst(s(X), cons(Y, Z))) -> mark#(cons(Y, fst(X, Z))), mark#(len(X)) -> active#(len(mark(X))))
(active#(fst(s(X), cons(Y, Z))) -> mark#(cons(Y, fst(X, Z))), mark#(len(X)) -> len#(mark(X)))
(mark#(fst(X1, X2)) -> fst#(mark(X1), mark(X2)), fst#(X1, mark(X2)) -> fst#(X1, X2))
(mark#(fst(X1, X2)) -> fst#(mark(X1), mark(X2)), fst#(X1, active(X2)) -> fst#(X1, X2))
(mark#(fst(X1, X2)) -> fst#(mark(X1), mark(X2)), fst#(mark(X1), X2) -> fst#(X1, X2))
(mark#(fst(X1, X2)) -> fst#(mark(X1), mark(X2)), fst#(active(X1), X2) -> fst#(X1, X2))
(active#(fst(0(), Z)) -> mark#(nil()), mark#(nil()) -> active#(nil()))
(mark#(fst(X1, X2)) -> mark#(X2), mark#(nil()) -> active#(nil()))
(mark#(fst(X1, X2)) -> mark#(X2), mark#(fst(X1, X2)) -> mark#(X1))
(mark#(fst(X1, X2)) -> mark#(X2), mark#(fst(X1, X2)) -> mark#(X2))
(mark#(fst(X1, X2)) -> mark#(X2), mark#(fst(X1, X2)) -> active#(fst(mark(X1), mark(X2))))
(mark#(fst(X1, X2)) -> mark#(X2), mark#(fst(X1, X2)) -> fst#(mark(X1), mark(X2)))
(mark#(fst(X1, X2)) -> mark#(X2), mark#(0()) -> active#(0()))
(mark#(fst(X1, X2)) -> mark#(X2), mark#(cons(X1, X2)) -> mark#(X1))
(mark#(fst(X1, X2)) -> mark#(X2), mark#(cons(X1, X2)) -> active#(cons(mark(X1), X2)))
(mark#(fst(X1, X2)) -> mark#(X2), mark#(cons(X1, X2)) -> cons#(mark(X1), X2))
(mark#(fst(X1, X2)) -> mark#(X2), mark#(s(X)) -> active#(s(X)))
(mark#(fst(X1, X2)) -> mark#(X2), mark#(from(X)) -> mark#(X))
(mark#(fst(X1, X2)) -> mark#(X2), mark#(from(X)) -> active#(from(mark(X))))
(mark#(fst(X1, X2)) -> mark#(X2), mark#(from(X)) -> from#(mark(X)))
(mark#(fst(X1, X2)) -> mark#(X2), mark#(add(X1, X2)) -> mark#(X1))
(mark#(fst(X1, X2)) -> mark#(X2), mark#(add(X1, X2)) -> mark#(X2))
(mark#(fst(X1, X2)) -> mark#(X2), mark#(add(X1, X2)) -> active#(add(mark(X1), mark(X2))))
(mark#(fst(X1, X2)) -> mark#(X2), mark#(add(X1, X2)) -> add#(mark(X1), mark(X2)))
(mark#(fst(X1, X2)) -> mark#(X2), mark#(len(X)) -> mark#(X))
(mark#(fst(X1, X2)) -> mark#(X2), mark#(len(X)) -> active#(len(mark(X))))
(mark#(fst(X1, X2)) -> mark#(X2), mark#(len(X)) -> len#(mark(X)))
}
SCCS:
Scc:
{ len#(mark(X)) -> len#(X),
len#(active(X)) -> len#(X)}
Scc:
{ add#(X1, mark(X2)) -> add#(X1, X2),
add#(X1, active(X2)) -> add#(X1, X2),
add#(mark(X1), X2) -> add#(X1, X2),
add#(active(X1), X2) -> add#(X1, X2)}
Scc:
{ from#(mark(X)) -> from#(X),
from#(active(X)) -> from#(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:
{ fst#(X1, mark(X2)) -> fst#(X1, X2),
fst#(X1, active(X2)) -> fst#(X1, X2),
fst#(mark(X1), X2) -> fst#(X1, X2),
fst#(active(X1), X2) -> fst#(X1, X2)}
Scc:
{ mark#(fst(X1, X2)) -> mark#(X1),
mark#(fst(X1, X2)) -> mark#(X2),
mark#(fst(X1, X2)) -> active#(fst(mark(X1), mark(X2))),
mark#(cons(X1, X2)) -> mark#(X1),
mark#(cons(X1, X2)) -> active#(cons(mark(X1), X2)),
mark#(s(X)) -> active#(s(X)),
mark#(from(X)) -> mark#(X),
mark#(from(X)) -> active#(from(mark(X))),
mark#(add(X1, X2)) -> mark#(X1),
mark#(add(X1, X2)) -> mark#(X2),
mark#(add(X1, X2)) -> active#(add(mark(X1), mark(X2))),
mark#(len(X)) -> mark#(X),
mark#(len(X)) -> active#(len(mark(X))),
active#(fst(s(X), cons(Y, Z))) -> mark#(cons(Y, fst(X, Z))),
active#(from(X)) -> mark#(cons(X, from(s(X)))),
active#(add(0(), X)) -> mark#(X),
active#(add(s(X), Y)) -> mark#(s(add(X, Y))),
active#(len(cons(X, Z))) -> mark#(s(len(Z)))}
SCC:
Strict:
{ len#(mark(X)) -> len#(X),
len#(active(X)) -> len#(X)}
Weak:
{ mark(nil()) -> active(nil()),
mark(fst(X1, X2)) -> active(fst(mark(X1), mark(X2))),
mark(0()) -> active(0()),
mark(cons(X1, X2)) -> active(cons(mark(X1), X2)),
mark(s(X)) -> active(s(X)),
mark(from(X)) -> active(from(mark(X))),
mark(add(X1, X2)) -> active(add(mark(X1), mark(X2))),
mark(len(X)) -> active(len(mark(X))),
active(fst(0(), Z)) -> mark(nil()),
active(fst(s(X), cons(Y, Z))) -> mark(cons(Y, fst(X, Z))),
active(from(X)) -> mark(cons(X, from(s(X)))),
active(add(0(), X)) -> mark(X),
active(add(s(X), Y)) -> mark(s(add(X, Y))),
active(len(nil())) -> mark(0()),
active(len(cons(X, Z))) -> mark(s(len(Z))),
fst(X1, mark(X2)) -> fst(X1, X2),
fst(X1, active(X2)) -> fst(X1, X2),
fst(mark(X1), X2) -> fst(X1, X2),
fst(active(X1), X2) -> fst(X1, X2),
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),
from(mark(X)) -> from(X),
from(active(X)) -> from(X),
add(X1, mark(X2)) -> add(X1, X2),
add(X1, active(X2)) -> add(X1, X2),
add(mark(X1), X2) -> add(X1, X2),
add(active(X1), X2) -> add(X1, X2),
len(mark(X)) -> len(X),
len(active(X)) -> len(X)}
SPSC:
Simple Projection:
pi(len#) = 0
Strict:
{len#(active(X)) -> len#(X)}
EDG:
{(len#(active(X)) -> len#(X), len#(active(X)) -> len#(X))}
SCCS:
Scc:
{len#(active(X)) -> len#(X)}
SCC:
Strict:
{len#(active(X)) -> len#(X)}
Weak:
{ mark(nil()) -> active(nil()),
mark(fst(X1, X2)) -> active(fst(mark(X1), mark(X2))),
mark(0()) -> active(0()),
mark(cons(X1, X2)) -> active(cons(mark(X1), X2)),
mark(s(X)) -> active(s(X)),
mark(from(X)) -> active(from(mark(X))),
mark(add(X1, X2)) -> active(add(mark(X1), mark(X2))),
mark(len(X)) -> active(len(mark(X))),
active(fst(0(), Z)) -> mark(nil()),
active(fst(s(X), cons(Y, Z))) -> mark(cons(Y, fst(X, Z))),
active(from(X)) -> mark(cons(X, from(s(X)))),
active(add(0(), X)) -> mark(X),
active(add(s(X), Y)) -> mark(s(add(X, Y))),
active(len(nil())) -> mark(0()),
active(len(cons(X, Z))) -> mark(s(len(Z))),
fst(X1, mark(X2)) -> fst(X1, X2),
fst(X1, active(X2)) -> fst(X1, X2),
fst(mark(X1), X2) -> fst(X1, X2),
fst(active(X1), X2) -> fst(X1, X2),
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),
from(mark(X)) -> from(X),
from(active(X)) -> from(X),
add(X1, mark(X2)) -> add(X1, X2),
add(X1, active(X2)) -> add(X1, X2),
add(mark(X1), X2) -> add(X1, X2),
add(active(X1), X2) -> add(X1, X2),
len(mark(X)) -> len(X),
len(active(X)) -> len(X)}
SPSC:
Simple Projection:
pi(len#) = 0
Strict:
{}
Qed
SCC:
Strict:
{ add#(X1, mark(X2)) -> add#(X1, X2),
add#(X1, active(X2)) -> add#(X1, X2),
add#(mark(X1), X2) -> add#(X1, X2),
add#(active(X1), X2) -> add#(X1, X2)}
Weak:
{ mark(nil()) -> active(nil()),
mark(fst(X1, X2)) -> active(fst(mark(X1), mark(X2))),
mark(0()) -> active(0()),
mark(cons(X1, X2)) -> active(cons(mark(X1), X2)),
mark(s(X)) -> active(s(X)),
mark(from(X)) -> active(from(mark(X))),
mark(add(X1, X2)) -> active(add(mark(X1), mark(X2))),
mark(len(X)) -> active(len(mark(X))),
active(fst(0(), Z)) -> mark(nil()),
active(fst(s(X), cons(Y, Z))) -> mark(cons(Y, fst(X, Z))),
active(from(X)) -> mark(cons(X, from(s(X)))),
active(add(0(), X)) -> mark(X),
active(add(s(X), Y)) -> mark(s(add(X, Y))),
active(len(nil())) -> mark(0()),
active(len(cons(X, Z))) -> mark(s(len(Z))),
fst(X1, mark(X2)) -> fst(X1, X2),
fst(X1, active(X2)) -> fst(X1, X2),
fst(mark(X1), X2) -> fst(X1, X2),
fst(active(X1), X2) -> fst(X1, X2),
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),
from(mark(X)) -> from(X),
from(active(X)) -> from(X),
add(X1, mark(X2)) -> add(X1, X2),
add(X1, active(X2)) -> add(X1, X2),
add(mark(X1), X2) -> add(X1, X2),
add(active(X1), X2) -> add(X1, X2),
len(mark(X)) -> len(X),
len(active(X)) -> len(X)}
SPSC:
Simple Projection:
pi(add#) = 0
Strict:
{ add#(X1, mark(X2)) -> add#(X1, X2),
add#(X1, active(X2)) -> add#(X1, X2),
add#(mark(X1), X2) -> add#(X1, X2)}
EDG:
{(add#(X1, active(X2)) -> add#(X1, X2), add#(mark(X1), X2) -> add#(X1, X2))
(add#(X1, active(X2)) -> add#(X1, X2), add#(X1, active(X2)) -> add#(X1, X2))
(add#(X1, active(X2)) -> add#(X1, X2), add#(X1, mark(X2)) -> add#(X1, X2))
(add#(mark(X1), X2) -> add#(X1, X2), add#(X1, mark(X2)) -> add#(X1, X2))
(add#(mark(X1), X2) -> add#(X1, X2), add#(X1, active(X2)) -> add#(X1, X2))
(add#(mark(X1), X2) -> add#(X1, X2), add#(mark(X1), X2) -> add#(X1, X2))
(add#(X1, mark(X2)) -> add#(X1, X2), add#(X1, mark(X2)) -> add#(X1, X2))
(add#(X1, mark(X2)) -> add#(X1, X2), add#(X1, active(X2)) -> add#(X1, X2))
(add#(X1, mark(X2)) -> add#(X1, X2), add#(mark(X1), X2) -> add#(X1, X2))}
SCCS:
Scc:
{ add#(X1, mark(X2)) -> add#(X1, X2),
add#(X1, active(X2)) -> add#(X1, X2),
add#(mark(X1), X2) -> add#(X1, X2)}
SCC:
Strict:
{ add#(X1, mark(X2)) -> add#(X1, X2),
add#(X1, active(X2)) -> add#(X1, X2),
add#(mark(X1), X2) -> add#(X1, X2)}
Weak:
{ mark(nil()) -> active(nil()),
mark(fst(X1, X2)) -> active(fst(mark(X1), mark(X2))),
mark(0()) -> active(0()),
mark(cons(X1, X2)) -> active(cons(mark(X1), X2)),
mark(s(X)) -> active(s(X)),
mark(from(X)) -> active(from(mark(X))),
mark(add(X1, X2)) -> active(add(mark(X1), mark(X2))),
mark(len(X)) -> active(len(mark(X))),
active(fst(0(), Z)) -> mark(nil()),
active(fst(s(X), cons(Y, Z))) -> mark(cons(Y, fst(X, Z))),
active(from(X)) -> mark(cons(X, from(s(X)))),
active(add(0(), X)) -> mark(X),
active(add(s(X), Y)) -> mark(s(add(X, Y))),
active(len(nil())) -> mark(0()),
active(len(cons(X, Z))) -> mark(s(len(Z))),
fst(X1, mark(X2)) -> fst(X1, X2),
fst(X1, active(X2)) -> fst(X1, X2),
fst(mark(X1), X2) -> fst(X1, X2),
fst(active(X1), X2) -> fst(X1, X2),
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),
from(mark(X)) -> from(X),
from(active(X)) -> from(X),
add(X1, mark(X2)) -> add(X1, X2),
add(X1, active(X2)) -> add(X1, X2),
add(mark(X1), X2) -> add(X1, X2),
add(active(X1), X2) -> add(X1, X2),
len(mark(X)) -> len(X),
len(active(X)) -> len(X)}
SPSC:
Simple Projection:
pi(add#) = 0
Strict:
{ add#(X1, mark(X2)) -> add#(X1, X2),
add#(X1, active(X2)) -> add#(X1, X2)}
EDG:
{(add#(X1, active(X2)) -> add#(X1, X2), add#(X1, active(X2)) -> add#(X1, X2))
(add#(X1, active(X2)) -> add#(X1, X2), add#(X1, mark(X2)) -> add#(X1, X2))
(add#(X1, mark(X2)) -> add#(X1, X2), add#(X1, mark(X2)) -> add#(X1, X2))
(add#(X1, mark(X2)) -> add#(X1, X2), add#(X1, active(X2)) -> add#(X1, X2))}
SCCS:
Scc:
{ add#(X1, mark(X2)) -> add#(X1, X2),
add#(X1, active(X2)) -> add#(X1, X2)}
SCC:
Strict:
{ add#(X1, mark(X2)) -> add#(X1, X2),
add#(X1, active(X2)) -> add#(X1, X2)}
Weak:
{ mark(nil()) -> active(nil()),
mark(fst(X1, X2)) -> active(fst(mark(X1), mark(X2))),
mark(0()) -> active(0()),
mark(cons(X1, X2)) -> active(cons(mark(X1), X2)),
mark(s(X)) -> active(s(X)),
mark(from(X)) -> active(from(mark(X))),
mark(add(X1, X2)) -> active(add(mark(X1), mark(X2))),
mark(len(X)) -> active(len(mark(X))),
active(fst(0(), Z)) -> mark(nil()),
active(fst(s(X), cons(Y, Z))) -> mark(cons(Y, fst(X, Z))),
active(from(X)) -> mark(cons(X, from(s(X)))),
active(add(0(), X)) -> mark(X),
active(add(s(X), Y)) -> mark(s(add(X, Y))),
active(len(nil())) -> mark(0()),
active(len(cons(X, Z))) -> mark(s(len(Z))),
fst(X1, mark(X2)) -> fst(X1, X2),
fst(X1, active(X2)) -> fst(X1, X2),
fst(mark(X1), X2) -> fst(X1, X2),
fst(active(X1), X2) -> fst(X1, X2),
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),
from(mark(X)) -> from(X),
from(active(X)) -> from(X),
add(X1, mark(X2)) -> add(X1, X2),
add(X1, active(X2)) -> add(X1, X2),
add(mark(X1), X2) -> add(X1, X2),
add(active(X1), X2) -> add(X1, X2),
len(mark(X)) -> len(X),
len(active(X)) -> len(X)}
SPSC:
Simple Projection:
pi(add#) = 1
Strict:
{add#(X1, active(X2)) -> add#(X1, X2)}
EDG:
{(add#(X1, active(X2)) -> add#(X1, X2), add#(X1, active(X2)) -> add#(X1, X2))}
SCCS:
Scc:
{add#(X1, active(X2)) -> add#(X1, X2)}
SCC:
Strict:
{add#(X1, active(X2)) -> add#(X1, X2)}
Weak:
{ mark(nil()) -> active(nil()),
mark(fst(X1, X2)) -> active(fst(mark(X1), mark(X2))),
mark(0()) -> active(0()),
mark(cons(X1, X2)) -> active(cons(mark(X1), X2)),
mark(s(X)) -> active(s(X)),
mark(from(X)) -> active(from(mark(X))),
mark(add(X1, X2)) -> active(add(mark(X1), mark(X2))),
mark(len(X)) -> active(len(mark(X))),
active(fst(0(), Z)) -> mark(nil()),
active(fst(s(X), cons(Y, Z))) -> mark(cons(Y, fst(X, Z))),
active(from(X)) -> mark(cons(X, from(s(X)))),
active(add(0(), X)) -> mark(X),
active(add(s(X), Y)) -> mark(s(add(X, Y))),
active(len(nil())) -> mark(0()),
active(len(cons(X, Z))) -> mark(s(len(Z))),
fst(X1, mark(X2)) -> fst(X1, X2),
fst(X1, active(X2)) -> fst(X1, X2),
fst(mark(X1), X2) -> fst(X1, X2),
fst(active(X1), X2) -> fst(X1, X2),
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),
from(mark(X)) -> from(X),
from(active(X)) -> from(X),
add(X1, mark(X2)) -> add(X1, X2),
add(X1, active(X2)) -> add(X1, X2),
add(mark(X1), X2) -> add(X1, X2),
add(active(X1), X2) -> add(X1, X2),
len(mark(X)) -> len(X),
len(active(X)) -> len(X)}
SPSC:
Simple Projection:
pi(add#) = 1
Strict:
{}
Qed
SCC:
Strict:
{ from#(mark(X)) -> from#(X),
from#(active(X)) -> from#(X)}
Weak:
{ mark(nil()) -> active(nil()),
mark(fst(X1, X2)) -> active(fst(mark(X1), mark(X2))),
mark(0()) -> active(0()),
mark(cons(X1, X2)) -> active(cons(mark(X1), X2)),
mark(s(X)) -> active(s(X)),
mark(from(X)) -> active(from(mark(X))),
mark(add(X1, X2)) -> active(add(mark(X1), mark(X2))),
mark(len(X)) -> active(len(mark(X))),
active(fst(0(), Z)) -> mark(nil()),
active(fst(s(X), cons(Y, Z))) -> mark(cons(Y, fst(X, Z))),
active(from(X)) -> mark(cons(X, from(s(X)))),
active(add(0(), X)) -> mark(X),
active(add(s(X), Y)) -> mark(s(add(X, Y))),
active(len(nil())) -> mark(0()),
active(len(cons(X, Z))) -> mark(s(len(Z))),
fst(X1, mark(X2)) -> fst(X1, X2),
fst(X1, active(X2)) -> fst(X1, X2),
fst(mark(X1), X2) -> fst(X1, X2),
fst(active(X1), X2) -> fst(X1, X2),
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),
from(mark(X)) -> from(X),
from(active(X)) -> from(X),
add(X1, mark(X2)) -> add(X1, X2),
add(X1, active(X2)) -> add(X1, X2),
add(mark(X1), X2) -> add(X1, X2),
add(active(X1), X2) -> add(X1, X2),
len(mark(X)) -> len(X),
len(active(X)) -> len(X)}
SPSC:
Simple Projection:
pi(from#) = 0
Strict:
{from#(active(X)) -> from#(X)}
EDG:
{(from#(active(X)) -> from#(X), from#(active(X)) -> from#(X))}
SCCS:
Scc:
{from#(active(X)) -> from#(X)}
SCC:
Strict:
{from#(active(X)) -> from#(X)}
Weak:
{ mark(nil()) -> active(nil()),
mark(fst(X1, X2)) -> active(fst(mark(X1), mark(X2))),
mark(0()) -> active(0()),
mark(cons(X1, X2)) -> active(cons(mark(X1), X2)),
mark(s(X)) -> active(s(X)),
mark(from(X)) -> active(from(mark(X))),
mark(add(X1, X2)) -> active(add(mark(X1), mark(X2))),
mark(len(X)) -> active(len(mark(X))),
active(fst(0(), Z)) -> mark(nil()),
active(fst(s(X), cons(Y, Z))) -> mark(cons(Y, fst(X, Z))),
active(from(X)) -> mark(cons(X, from(s(X)))),
active(add(0(), X)) -> mark(X),
active(add(s(X), Y)) -> mark(s(add(X, Y))),
active(len(nil())) -> mark(0()),
active(len(cons(X, Z))) -> mark(s(len(Z))),
fst(X1, mark(X2)) -> fst(X1, X2),
fst(X1, active(X2)) -> fst(X1, X2),
fst(mark(X1), X2) -> fst(X1, X2),
fst(active(X1), X2) -> fst(X1, X2),
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),
from(mark(X)) -> from(X),
from(active(X)) -> from(X),
add(X1, mark(X2)) -> add(X1, X2),
add(X1, active(X2)) -> add(X1, X2),
add(mark(X1), X2) -> add(X1, X2),
add(active(X1), X2) -> add(X1, X2),
len(mark(X)) -> len(X),
len(active(X)) -> len(X)}
SPSC:
Simple Projection:
pi(from#) = 0
Strict:
{}
Qed
SCC:
Strict:
{ s#(mark(X)) -> s#(X),
s#(active(X)) -> s#(X)}
Weak:
{ mark(nil()) -> active(nil()),
mark(fst(X1, X2)) -> active(fst(mark(X1), mark(X2))),
mark(0()) -> active(0()),
mark(cons(X1, X2)) -> active(cons(mark(X1), X2)),
mark(s(X)) -> active(s(X)),
mark(from(X)) -> active(from(mark(X))),
mark(add(X1, X2)) -> active(add(mark(X1), mark(X2))),
mark(len(X)) -> active(len(mark(X))),
active(fst(0(), Z)) -> mark(nil()),
active(fst(s(X), cons(Y, Z))) -> mark(cons(Y, fst(X, Z))),
active(from(X)) -> mark(cons(X, from(s(X)))),
active(add(0(), X)) -> mark(X),
active(add(s(X), Y)) -> mark(s(add(X, Y))),
active(len(nil())) -> mark(0()),
active(len(cons(X, Z))) -> mark(s(len(Z))),
fst(X1, mark(X2)) -> fst(X1, X2),
fst(X1, active(X2)) -> fst(X1, X2),
fst(mark(X1), X2) -> fst(X1, X2),
fst(active(X1), X2) -> fst(X1, X2),
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),
from(mark(X)) -> from(X),
from(active(X)) -> from(X),
add(X1, mark(X2)) -> add(X1, X2),
add(X1, active(X2)) -> add(X1, X2),
add(mark(X1), X2) -> add(X1, X2),
add(active(X1), X2) -> add(X1, X2),
len(mark(X)) -> len(X),
len(active(X)) -> len(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(nil()) -> active(nil()),
mark(fst(X1, X2)) -> active(fst(mark(X1), mark(X2))),
mark(0()) -> active(0()),
mark(cons(X1, X2)) -> active(cons(mark(X1), X2)),
mark(s(X)) -> active(s(X)),
mark(from(X)) -> active(from(mark(X))),
mark(add(X1, X2)) -> active(add(mark(X1), mark(X2))),
mark(len(X)) -> active(len(mark(X))),
active(fst(0(), Z)) -> mark(nil()),
active(fst(s(X), cons(Y, Z))) -> mark(cons(Y, fst(X, Z))),
active(from(X)) -> mark(cons(X, from(s(X)))),
active(add(0(), X)) -> mark(X),
active(add(s(X), Y)) -> mark(s(add(X, Y))),
active(len(nil())) -> mark(0()),
active(len(cons(X, Z))) -> mark(s(len(Z))),
fst(X1, mark(X2)) -> fst(X1, X2),
fst(X1, active(X2)) -> fst(X1, X2),
fst(mark(X1), X2) -> fst(X1, X2),
fst(active(X1), X2) -> fst(X1, X2),
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),
from(mark(X)) -> from(X),
from(active(X)) -> from(X),
add(X1, mark(X2)) -> add(X1, X2),
add(X1, active(X2)) -> add(X1, X2),
add(mark(X1), X2) -> add(X1, X2),
add(active(X1), X2) -> add(X1, X2),
len(mark(X)) -> len(X),
len(active(X)) -> len(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(nil()) -> active(nil()),
mark(fst(X1, X2)) -> active(fst(mark(X1), mark(X2))),
mark(0()) -> active(0()),
mark(cons(X1, X2)) -> active(cons(mark(X1), X2)),
mark(s(X)) -> active(s(X)),
mark(from(X)) -> active(from(mark(X))),
mark(add(X1, X2)) -> active(add(mark(X1), mark(X2))),
mark(len(X)) -> active(len(mark(X))),
active(fst(0(), Z)) -> mark(nil()),
active(fst(s(X), cons(Y, Z))) -> mark(cons(Y, fst(X, Z))),
active(from(X)) -> mark(cons(X, from(s(X)))),
active(add(0(), X)) -> mark(X),
active(add(s(X), Y)) -> mark(s(add(X, Y))),
active(len(nil())) -> mark(0()),
active(len(cons(X, Z))) -> mark(s(len(Z))),
fst(X1, mark(X2)) -> fst(X1, X2),
fst(X1, active(X2)) -> fst(X1, X2),
fst(mark(X1), X2) -> fst(X1, X2),
fst(active(X1), X2) -> fst(X1, X2),
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),
from(mark(X)) -> from(X),
from(active(X)) -> from(X),
add(X1, mark(X2)) -> add(X1, X2),
add(X1, active(X2)) -> add(X1, X2),
add(mark(X1), X2) -> add(X1, X2),
add(active(X1), X2) -> add(X1, X2),
len(mark(X)) -> len(X),
len(active(X)) -> len(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(nil()) -> active(nil()),
mark(fst(X1, X2)) -> active(fst(mark(X1), mark(X2))),
mark(0()) -> active(0()),
mark(cons(X1, X2)) -> active(cons(mark(X1), X2)),
mark(s(X)) -> active(s(X)),
mark(from(X)) -> active(from(mark(X))),
mark(add(X1, X2)) -> active(add(mark(X1), mark(X2))),
mark(len(X)) -> active(len(mark(X))),
active(fst(0(), Z)) -> mark(nil()),
active(fst(s(X), cons(Y, Z))) -> mark(cons(Y, fst(X, Z))),
active(from(X)) -> mark(cons(X, from(s(X)))),
active(add(0(), X)) -> mark(X),
active(add(s(X), Y)) -> mark(s(add(X, Y))),
active(len(nil())) -> mark(0()),
active(len(cons(X, Z))) -> mark(s(len(Z))),
fst(X1, mark(X2)) -> fst(X1, X2),
fst(X1, active(X2)) -> fst(X1, X2),
fst(mark(X1), X2) -> fst(X1, X2),
fst(active(X1), X2) -> fst(X1, X2),
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),
from(mark(X)) -> from(X),
from(active(X)) -> from(X),
add(X1, mark(X2)) -> add(X1, X2),
add(X1, active(X2)) -> add(X1, X2),
add(mark(X1), X2) -> add(X1, X2),
add(active(X1), X2) -> add(X1, X2),
len(mark(X)) -> len(X),
len(active(X)) -> len(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(nil()) -> active(nil()),
mark(fst(X1, X2)) -> active(fst(mark(X1), mark(X2))),
mark(0()) -> active(0()),
mark(cons(X1, X2)) -> active(cons(mark(X1), X2)),
mark(s(X)) -> active(s(X)),
mark(from(X)) -> active(from(mark(X))),
mark(add(X1, X2)) -> active(add(mark(X1), mark(X2))),
mark(len(X)) -> active(len(mark(X))),
active(fst(0(), Z)) -> mark(nil()),
active(fst(s(X), cons(Y, Z))) -> mark(cons(Y, fst(X, Z))),
active(from(X)) -> mark(cons(X, from(s(X)))),
active(add(0(), X)) -> mark(X),
active(add(s(X), Y)) -> mark(s(add(X, Y))),
active(len(nil())) -> mark(0()),
active(len(cons(X, Z))) -> mark(s(len(Z))),
fst(X1, mark(X2)) -> fst(X1, X2),
fst(X1, active(X2)) -> fst(X1, X2),
fst(mark(X1), X2) -> fst(X1, X2),
fst(active(X1), X2) -> fst(X1, X2),
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),
from(mark(X)) -> from(X),
from(active(X)) -> from(X),
add(X1, mark(X2)) -> add(X1, X2),
add(X1, active(X2)) -> add(X1, X2),
add(mark(X1), X2) -> add(X1, X2),
add(active(X1), X2) -> add(X1, X2),
len(mark(X)) -> len(X),
len(active(X)) -> len(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(nil()) -> active(nil()),
mark(fst(X1, X2)) -> active(fst(mark(X1), mark(X2))),
mark(0()) -> active(0()),
mark(cons(X1, X2)) -> active(cons(mark(X1), X2)),
mark(s(X)) -> active(s(X)),
mark(from(X)) -> active(from(mark(X))),
mark(add(X1, X2)) -> active(add(mark(X1), mark(X2))),
mark(len(X)) -> active(len(mark(X))),
active(fst(0(), Z)) -> mark(nil()),
active(fst(s(X), cons(Y, Z))) -> mark(cons(Y, fst(X, Z))),
active(from(X)) -> mark(cons(X, from(s(X)))),
active(add(0(), X)) -> mark(X),
active(add(s(X), Y)) -> mark(s(add(X, Y))),
active(len(nil())) -> mark(0()),
active(len(cons(X, Z))) -> mark(s(len(Z))),
fst(X1, mark(X2)) -> fst(X1, X2),
fst(X1, active(X2)) -> fst(X1, X2),
fst(mark(X1), X2) -> fst(X1, X2),
fst(active(X1), X2) -> fst(X1, X2),
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),
from(mark(X)) -> from(X),
from(active(X)) -> from(X),
add(X1, mark(X2)) -> add(X1, X2),
add(X1, active(X2)) -> add(X1, X2),
add(mark(X1), X2) -> add(X1, X2),
add(active(X1), X2) -> add(X1, X2),
len(mark(X)) -> len(X),
len(active(X)) -> len(X)}
SPSC:
Simple Projection:
pi(cons#) = 1
Strict:
{}
Qed
SCC:
Strict:
{ fst#(X1, mark(X2)) -> fst#(X1, X2),
fst#(X1, active(X2)) -> fst#(X1, X2),
fst#(mark(X1), X2) -> fst#(X1, X2),
fst#(active(X1), X2) -> fst#(X1, X2)}
Weak:
{ mark(nil()) -> active(nil()),
mark(fst(X1, X2)) -> active(fst(mark(X1), mark(X2))),
mark(0()) -> active(0()),
mark(cons(X1, X2)) -> active(cons(mark(X1), X2)),
mark(s(X)) -> active(s(X)),
mark(from(X)) -> active(from(mark(X))),
mark(add(X1, X2)) -> active(add(mark(X1), mark(X2))),
mark(len(X)) -> active(len(mark(X))),
active(fst(0(), Z)) -> mark(nil()),
active(fst(s(X), cons(Y, Z))) -> mark(cons(Y, fst(X, Z))),
active(from(X)) -> mark(cons(X, from(s(X)))),
active(add(0(), X)) -> mark(X),
active(add(s(X), Y)) -> mark(s(add(X, Y))),
active(len(nil())) -> mark(0()),
active(len(cons(X, Z))) -> mark(s(len(Z))),
fst(X1, mark(X2)) -> fst(X1, X2),
fst(X1, active(X2)) -> fst(X1, X2),
fst(mark(X1), X2) -> fst(X1, X2),
fst(active(X1), X2) -> fst(X1, X2),
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),
from(mark(X)) -> from(X),
from(active(X)) -> from(X),
add(X1, mark(X2)) -> add(X1, X2),
add(X1, active(X2)) -> add(X1, X2),
add(mark(X1), X2) -> add(X1, X2),
add(active(X1), X2) -> add(X1, X2),
len(mark(X)) -> len(X),
len(active(X)) -> len(X)}
SPSC:
Simple Projection:
pi(fst#) = 0
Strict:
{ fst#(X1, mark(X2)) -> fst#(X1, X2),
fst#(X1, active(X2)) -> fst#(X1, X2),
fst#(mark(X1), X2) -> fst#(X1, X2)}
EDG:
{(fst#(X1, active(X2)) -> fst#(X1, X2), fst#(mark(X1), X2) -> fst#(X1, X2))
(fst#(X1, active(X2)) -> fst#(X1, X2), fst#(X1, active(X2)) -> fst#(X1, X2))
(fst#(X1, active(X2)) -> fst#(X1, X2), fst#(X1, mark(X2)) -> fst#(X1, X2))
(fst#(mark(X1), X2) -> fst#(X1, X2), fst#(X1, mark(X2)) -> fst#(X1, X2))
(fst#(mark(X1), X2) -> fst#(X1, X2), fst#(X1, active(X2)) -> fst#(X1, X2))
(fst#(mark(X1), X2) -> fst#(X1, X2), fst#(mark(X1), X2) -> fst#(X1, X2))
(fst#(X1, mark(X2)) -> fst#(X1, X2), fst#(X1, mark(X2)) -> fst#(X1, X2))
(fst#(X1, mark(X2)) -> fst#(X1, X2), fst#(X1, active(X2)) -> fst#(X1, X2))
(fst#(X1, mark(X2)) -> fst#(X1, X2), fst#(mark(X1), X2) -> fst#(X1, X2))}
SCCS:
Scc:
{ fst#(X1, mark(X2)) -> fst#(X1, X2),
fst#(X1, active(X2)) -> fst#(X1, X2),
fst#(mark(X1), X2) -> fst#(X1, X2)}
SCC:
Strict:
{ fst#(X1, mark(X2)) -> fst#(X1, X2),
fst#(X1, active(X2)) -> fst#(X1, X2),
fst#(mark(X1), X2) -> fst#(X1, X2)}
Weak:
{ mark(nil()) -> active(nil()),
mark(fst(X1, X2)) -> active(fst(mark(X1), mark(X2))),
mark(0()) -> active(0()),
mark(cons(X1, X2)) -> active(cons(mark(X1), X2)),
mark(s(X)) -> active(s(X)),
mark(from(X)) -> active(from(mark(X))),
mark(add(X1, X2)) -> active(add(mark(X1), mark(X2))),
mark(len(X)) -> active(len(mark(X))),
active(fst(0(), Z)) -> mark(nil()),
active(fst(s(X), cons(Y, Z))) -> mark(cons(Y, fst(X, Z))),
active(from(X)) -> mark(cons(X, from(s(X)))),
active(add(0(), X)) -> mark(X),
active(add(s(X), Y)) -> mark(s(add(X, Y))),
active(len(nil())) -> mark(0()),
active(len(cons(X, Z))) -> mark(s(len(Z))),
fst(X1, mark(X2)) -> fst(X1, X2),
fst(X1, active(X2)) -> fst(X1, X2),
fst(mark(X1), X2) -> fst(X1, X2),
fst(active(X1), X2) -> fst(X1, X2),
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),
from(mark(X)) -> from(X),
from(active(X)) -> from(X),
add(X1, mark(X2)) -> add(X1, X2),
add(X1, active(X2)) -> add(X1, X2),
add(mark(X1), X2) -> add(X1, X2),
add(active(X1), X2) -> add(X1, X2),
len(mark(X)) -> len(X),
len(active(X)) -> len(X)}
SPSC:
Simple Projection:
pi(fst#) = 0
Strict:
{ fst#(X1, mark(X2)) -> fst#(X1, X2),
fst#(X1, active(X2)) -> fst#(X1, X2)}
EDG:
{(fst#(X1, active(X2)) -> fst#(X1, X2), fst#(X1, active(X2)) -> fst#(X1, X2))
(fst#(X1, active(X2)) -> fst#(X1, X2), fst#(X1, mark(X2)) -> fst#(X1, X2))
(fst#(X1, mark(X2)) -> fst#(X1, X2), fst#(X1, mark(X2)) -> fst#(X1, X2))
(fst#(X1, mark(X2)) -> fst#(X1, X2), fst#(X1, active(X2)) -> fst#(X1, X2))}
SCCS:
Scc:
{ fst#(X1, mark(X2)) -> fst#(X1, X2),
fst#(X1, active(X2)) -> fst#(X1, X2)}
SCC:
Strict:
{ fst#(X1, mark(X2)) -> fst#(X1, X2),
fst#(X1, active(X2)) -> fst#(X1, X2)}
Weak:
{ mark(nil()) -> active(nil()),
mark(fst(X1, X2)) -> active(fst(mark(X1), mark(X2))),
mark(0()) -> active(0()),
mark(cons(X1, X2)) -> active(cons(mark(X1), X2)),
mark(s(X)) -> active(s(X)),
mark(from(X)) -> active(from(mark(X))),
mark(add(X1, X2)) -> active(add(mark(X1), mark(X2))),
mark(len(X)) -> active(len(mark(X))),
active(fst(0(), Z)) -> mark(nil()),
active(fst(s(X), cons(Y, Z))) -> mark(cons(Y, fst(X, Z))),
active(from(X)) -> mark(cons(X, from(s(X)))),
active(add(0(), X)) -> mark(X),
active(add(s(X), Y)) -> mark(s(add(X, Y))),
active(len(nil())) -> mark(0()),
active(len(cons(X, Z))) -> mark(s(len(Z))),
fst(X1, mark(X2)) -> fst(X1, X2),
fst(X1, active(X2)) -> fst(X1, X2),
fst(mark(X1), X2) -> fst(X1, X2),
fst(active(X1), X2) -> fst(X1, X2),
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),
from(mark(X)) -> from(X),
from(active(X)) -> from(X),
add(X1, mark(X2)) -> add(X1, X2),
add(X1, active(X2)) -> add(X1, X2),
add(mark(X1), X2) -> add(X1, X2),
add(active(X1), X2) -> add(X1, X2),
len(mark(X)) -> len(X),
len(active(X)) -> len(X)}
SPSC:
Simple Projection:
pi(fst#) = 1
Strict:
{fst#(X1, active(X2)) -> fst#(X1, X2)}
EDG:
{(fst#(X1, active(X2)) -> fst#(X1, X2), fst#(X1, active(X2)) -> fst#(X1, X2))}
SCCS:
Scc:
{fst#(X1, active(X2)) -> fst#(X1, X2)}
SCC:
Strict:
{fst#(X1, active(X2)) -> fst#(X1, X2)}
Weak:
{ mark(nil()) -> active(nil()),
mark(fst(X1, X2)) -> active(fst(mark(X1), mark(X2))),
mark(0()) -> active(0()),
mark(cons(X1, X2)) -> active(cons(mark(X1), X2)),
mark(s(X)) -> active(s(X)),
mark(from(X)) -> active(from(mark(X))),
mark(add(X1, X2)) -> active(add(mark(X1), mark(X2))),
mark(len(X)) -> active(len(mark(X))),
active(fst(0(), Z)) -> mark(nil()),
active(fst(s(X), cons(Y, Z))) -> mark(cons(Y, fst(X, Z))),
active(from(X)) -> mark(cons(X, from(s(X)))),
active(add(0(), X)) -> mark(X),
active(add(s(X), Y)) -> mark(s(add(X, Y))),
active(len(nil())) -> mark(0()),
active(len(cons(X, Z))) -> mark(s(len(Z))),
fst(X1, mark(X2)) -> fst(X1, X2),
fst(X1, active(X2)) -> fst(X1, X2),
fst(mark(X1), X2) -> fst(X1, X2),
fst(active(X1), X2) -> fst(X1, X2),
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),
from(mark(X)) -> from(X),
from(active(X)) -> from(X),
add(X1, mark(X2)) -> add(X1, X2),
add(X1, active(X2)) -> add(X1, X2),
add(mark(X1), X2) -> add(X1, X2),
add(active(X1), X2) -> add(X1, X2),
len(mark(X)) -> len(X),
len(active(X)) -> len(X)}
SPSC:
Simple Projection:
pi(fst#) = 1
Strict:
{}
Qed
SCC:
Strict:
{ mark#(fst(X1, X2)) -> mark#(X1),
mark#(fst(X1, X2)) -> mark#(X2),
mark#(fst(X1, X2)) -> active#(fst(mark(X1), mark(X2))),
mark#(cons(X1, X2)) -> mark#(X1),
mark#(cons(X1, X2)) -> active#(cons(mark(X1), X2)),
mark#(s(X)) -> active#(s(X)),
mark#(from(X)) -> mark#(X),
mark#(from(X)) -> active#(from(mark(X))),
mark#(add(X1, X2)) -> mark#(X1),
mark#(add(X1, X2)) -> mark#(X2),
mark#(add(X1, X2)) -> active#(add(mark(X1), mark(X2))),
mark#(len(X)) -> mark#(X),
mark#(len(X)) -> active#(len(mark(X))),
active#(fst(s(X), cons(Y, Z))) -> mark#(cons(Y, fst(X, Z))),
active#(from(X)) -> mark#(cons(X, from(s(X)))),
active#(add(0(), X)) -> mark#(X),
active#(add(s(X), Y)) -> mark#(s(add(X, Y))),
active#(len(cons(X, Z))) -> mark#(s(len(Z)))}
Weak:
{ mark(nil()) -> active(nil()),
mark(fst(X1, X2)) -> active(fst(mark(X1), mark(X2))),
mark(0()) -> active(0()),
mark(cons(X1, X2)) -> active(cons(mark(X1), X2)),
mark(s(X)) -> active(s(X)),
mark(from(X)) -> active(from(mark(X))),
mark(add(X1, X2)) -> active(add(mark(X1), mark(X2))),
mark(len(X)) -> active(len(mark(X))),
active(fst(0(), Z)) -> mark(nil()),
active(fst(s(X), cons(Y, Z))) -> mark(cons(Y, fst(X, Z))),
active(from(X)) -> mark(cons(X, from(s(X)))),
active(add(0(), X)) -> mark(X),
active(add(s(X), Y)) -> mark(s(add(X, Y))),
active(len(nil())) -> mark(0()),
active(len(cons(X, Z))) -> mark(s(len(Z))),
fst(X1, mark(X2)) -> fst(X1, X2),
fst(X1, active(X2)) -> fst(X1, X2),
fst(mark(X1), X2) -> fst(X1, X2),
fst(active(X1), X2) -> fst(X1, X2),
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),
from(mark(X)) -> from(X),
from(active(X)) -> from(X),
add(X1, mark(X2)) -> add(X1, X2),
add(X1, active(X2)) -> add(X1, X2),
add(mark(X1), X2) -> add(X1, X2),
add(active(X1), X2) -> add(X1, X2),
len(mark(X)) -> len(X),
len(active(X)) -> len(X)}
POLY:
Argument Filtering:
pi(len) = 0, pi(add) = [0,1], pi(from) = [0], pi(s) = [], pi(cons) = 0, pi(0) = [], pi(fst) = [0,1], pi(active#) = 0, pi(active) = 0, pi(nil) = [], pi(mark#) = 0, pi(mark) = 0
Usable Rules:
{}
Interpretation:
[add](x0, x1) = x0 + x1,
[fst](x0, x1) = x0 + x1,
[from](x0) = x0 + 1,
[s] = 0,
[0] = 0
Strict:
{ mark#(fst(X1, X2)) -> mark#(X1),
mark#(fst(X1, X2)) -> mark#(X2),
mark#(fst(X1, X2)) -> active#(fst(mark(X1), mark(X2))),
mark#(cons(X1, X2)) -> mark#(X1),
mark#(cons(X1, X2)) -> active#(cons(mark(X1), X2)),
mark#(s(X)) -> active#(s(X)),
mark#(from(X)) -> active#(from(mark(X))),
mark#(add(X1, X2)) -> mark#(X1),
mark#(add(X1, X2)) -> mark#(X2),
mark#(add(X1, X2)) -> active#(add(mark(X1), mark(X2))),
mark#(len(X)) -> mark#(X),
mark#(len(X)) -> active#(len(mark(X))),
active#(fst(s(X), cons(Y, Z))) -> mark#(cons(Y, fst(X, Z))),
active#(add(0(), X)) -> mark#(X),
active#(add(s(X), Y)) -> mark#(s(add(X, Y))),
active#(len(cons(X, Z))) -> mark#(s(len(Z)))}
Weak:
{ mark(nil()) -> active(nil()),
mark(fst(X1, X2)) -> active(fst(mark(X1), mark(X2))),
mark(0()) -> active(0()),
mark(cons(X1, X2)) -> active(cons(mark(X1), X2)),
mark(s(X)) -> active(s(X)),
mark(from(X)) -> active(from(mark(X))),
mark(add(X1, X2)) -> active(add(mark(X1), mark(X2))),
mark(len(X)) -> active(len(mark(X))),
active(fst(0(), Z)) -> mark(nil()),
active(fst(s(X), cons(Y, Z))) -> mark(cons(Y, fst(X, Z))),
active(from(X)) -> mark(cons(X, from(s(X)))),
active(add(0(), X)) -> mark(X),
active(add(s(X), Y)) -> mark(s(add(X, Y))),
active(len(nil())) -> mark(0()),
active(len(cons(X, Z))) -> mark(s(len(Z))),
fst(X1, mark(X2)) -> fst(X1, X2),
fst(X1, active(X2)) -> fst(X1, X2),
fst(mark(X1), X2) -> fst(X1, X2),
fst(active(X1), X2) -> fst(X1, X2),
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),
from(mark(X)) -> from(X),
from(active(X)) -> from(X),
add(X1, mark(X2)) -> add(X1, X2),
add(X1, active(X2)) -> add(X1, X2),
add(mark(X1), X2) -> add(X1, X2),
add(active(X1), X2) -> add(X1, X2),
len(mark(X)) -> len(X),
len(active(X)) -> len(X)}
EDG:
{
(mark#(add(X1, X2)) -> mark#(X2), mark#(len(X)) -> active#(len(mark(X))))
(mark#(add(X1, X2)) -> mark#(X2), mark#(len(X)) -> mark#(X))
(mark#(add(X1, X2)) -> mark#(X2), mark#(add(X1, X2)) -> active#(add(mark(X1), mark(X2))))
(mark#(add(X1, X2)) -> mark#(X2), mark#(add(X1, X2)) -> mark#(X2))
(mark#(add(X1, X2)) -> mark#(X2), mark#(add(X1, X2)) -> mark#(X1))
(mark#(add(X1, X2)) -> mark#(X2), mark#(from(X)) -> active#(from(mark(X))))
(mark#(add(X1, X2)) -> mark#(X2), mark#(s(X)) -> active#(s(X)))
(mark#(add(X1, X2)) -> mark#(X2), mark#(cons(X1, X2)) -> active#(cons(mark(X1), X2)))
(mark#(add(X1, X2)) -> mark#(X2), mark#(cons(X1, X2)) -> mark#(X1))
(mark#(add(X1, X2)) -> mark#(X2), mark#(fst(X1, X2)) -> active#(fst(mark(X1), mark(X2))))
(mark#(add(X1, X2)) -> mark#(X2), mark#(fst(X1, X2)) -> mark#(X2))
(mark#(add(X1, X2)) -> mark#(X2), mark#(fst(X1, X2)) -> mark#(X1))
(mark#(cons(X1, X2)) -> active#(cons(mark(X1), X2)), active#(len(cons(X, Z))) -> mark#(s(len(Z))))
(mark#(cons(X1, X2)) -> active#(cons(mark(X1), X2)), active#(add(s(X), Y)) -> mark#(s(add(X, Y))))
(mark#(cons(X1, X2)) -> active#(cons(mark(X1), X2)), active#(add(0(), X)) -> mark#(X))
(mark#(cons(X1, X2)) -> active#(cons(mark(X1), X2)), active#(fst(s(X), cons(Y, Z))) -> mark#(cons(Y, fst(X, Z))))
(active#(add(0(), X)) -> mark#(X), mark#(len(X)) -> active#(len(mark(X))))
(active#(add(0(), X)) -> mark#(X), mark#(len(X)) -> mark#(X))
(active#(add(0(), X)) -> mark#(X), mark#(add(X1, X2)) -> active#(add(mark(X1), mark(X2))))
(active#(add(0(), X)) -> mark#(X), mark#(add(X1, X2)) -> mark#(X2))
(active#(add(0(), X)) -> mark#(X), mark#(add(X1, X2)) -> mark#(X1))
(active#(add(0(), X)) -> mark#(X), mark#(from(X)) -> active#(from(mark(X))))
(active#(add(0(), X)) -> mark#(X), mark#(s(X)) -> active#(s(X)))
(active#(add(0(), X)) -> mark#(X), mark#(cons(X1, X2)) -> active#(cons(mark(X1), X2)))
(active#(add(0(), X)) -> mark#(X), mark#(cons(X1, X2)) -> mark#(X1))
(active#(add(0(), X)) -> mark#(X), mark#(fst(X1, X2)) -> active#(fst(mark(X1), mark(X2))))
(active#(add(0(), X)) -> mark#(X), mark#(fst(X1, X2)) -> mark#(X2))
(active#(add(0(), X)) -> mark#(X), mark#(fst(X1, X2)) -> mark#(X1))
(mark#(len(X)) -> active#(len(mark(X))), active#(len(cons(X, Z))) -> mark#(s(len(Z))))
(mark#(len(X)) -> active#(len(mark(X))), active#(add(s(X), Y)) -> mark#(s(add(X, Y))))
(mark#(len(X)) -> active#(len(mark(X))), active#(add(0(), X)) -> mark#(X))
(mark#(len(X)) -> active#(len(mark(X))), active#(fst(s(X), cons(Y, Z))) -> mark#(cons(Y, fst(X, Z))))
(active#(len(cons(X, Z))) -> mark#(s(len(Z))), mark#(len(X)) -> active#(len(mark(X))))
(active#(len(cons(X, Z))) -> mark#(s(len(Z))), mark#(len(X)) -> mark#(X))
(active#(len(cons(X, Z))) -> mark#(s(len(Z))), mark#(add(X1, X2)) -> active#(add(mark(X1), mark(X2))))
(active#(len(cons(X, Z))) -> mark#(s(len(Z))), mark#(add(X1, X2)) -> mark#(X2))
(active#(len(cons(X, Z))) -> mark#(s(len(Z))), mark#(add(X1, X2)) -> mark#(X1))
(active#(len(cons(X, Z))) -> mark#(s(len(Z))), mark#(from(X)) -> active#(from(mark(X))))
(active#(len(cons(X, Z))) -> mark#(s(len(Z))), mark#(s(X)) -> active#(s(X)))
(active#(len(cons(X, Z))) -> mark#(s(len(Z))), mark#(cons(X1, X2)) -> active#(cons(mark(X1), X2)))
(active#(len(cons(X, Z))) -> mark#(s(len(Z))), mark#(cons(X1, X2)) -> mark#(X1))
(active#(len(cons(X, Z))) -> mark#(s(len(Z))), mark#(fst(X1, X2)) -> active#(fst(mark(X1), mark(X2))))
(active#(len(cons(X, Z))) -> mark#(s(len(Z))), mark#(fst(X1, X2)) -> mark#(X2))
(active#(len(cons(X, Z))) -> mark#(s(len(Z))), mark#(fst(X1, X2)) -> mark#(X1))
(mark#(cons(X1, X2)) -> mark#(X1), mark#(len(X)) -> active#(len(mark(X))))
(mark#(cons(X1, X2)) -> mark#(X1), mark#(len(X)) -> mark#(X))
(mark#(cons(X1, X2)) -> mark#(X1), mark#(add(X1, X2)) -> active#(add(mark(X1), mark(X2))))
(mark#(cons(X1, X2)) -> mark#(X1), mark#(add(X1, X2)) -> mark#(X2))
(mark#(cons(X1, X2)) -> mark#(X1), mark#(add(X1, X2)) -> mark#(X1))
(mark#(cons(X1, X2)) -> mark#(X1), mark#(from(X)) -> active#(from(mark(X))))
(mark#(cons(X1, X2)) -> mark#(X1), mark#(s(X)) -> active#(s(X)))
(mark#(cons(X1, X2)) -> mark#(X1), mark#(cons(X1, X2)) -> active#(cons(mark(X1), X2)))
(mark#(cons(X1, X2)) -> mark#(X1), mark#(cons(X1, X2)) -> mark#(X1))
(mark#(cons(X1, X2)) -> mark#(X1), mark#(fst(X1, X2)) -> active#(fst(mark(X1), mark(X2))))
(mark#(cons(X1, X2)) -> mark#(X1), mark#(fst(X1, X2)) -> mark#(X2))
(mark#(cons(X1, X2)) -> mark#(X1), mark#(fst(X1, X2)) -> mark#(X1))
(mark#(fst(X1, X2)) -> active#(fst(mark(X1), mark(X2))), active#(len(cons(X, Z))) -> mark#(s(len(Z))))
(mark#(fst(X1, X2)) -> active#(fst(mark(X1), mark(X2))), active#(add(s(X), Y)) -> mark#(s(add(X, Y))))
(mark#(fst(X1, X2)) -> active#(fst(mark(X1), mark(X2))), active#(add(0(), X)) -> mark#(X))
(mark#(fst(X1, X2)) -> active#(fst(mark(X1), mark(X2))), active#(fst(s(X), cons(Y, Z))) -> mark#(cons(Y, fst(X, Z))))
(active#(fst(s(X), cons(Y, Z))) -> mark#(cons(Y, fst(X, Z))), mark#(len(X)) -> active#(len(mark(X))))
(active#(fst(s(X), cons(Y, Z))) -> mark#(cons(Y, fst(X, Z))), mark#(len(X)) -> mark#(X))
(active#(fst(s(X), cons(Y, Z))) -> mark#(cons(Y, fst(X, Z))), mark#(add(X1, X2)) -> active#(add(mark(X1), mark(X2))))
(active#(fst(s(X), cons(Y, Z))) -> mark#(cons(Y, fst(X, Z))), mark#(add(X1, X2)) -> mark#(X2))
(active#(fst(s(X), cons(Y, Z))) -> mark#(cons(Y, fst(X, Z))), mark#(add(X1, X2)) -> mark#(X1))
(active#(fst(s(X), cons(Y, Z))) -> mark#(cons(Y, fst(X, Z))), mark#(from(X)) -> active#(from(mark(X))))
(active#(fst(s(X), cons(Y, Z))) -> mark#(cons(Y, fst(X, Z))), mark#(s(X)) -> active#(s(X)))
(active#(fst(s(X), cons(Y, Z))) -> mark#(cons(Y, fst(X, Z))), mark#(cons(X1, X2)) -> active#(cons(mark(X1), X2)))
(active#(fst(s(X), cons(Y, Z))) -> mark#(cons(Y, fst(X, Z))), mark#(cons(X1, X2)) -> mark#(X1))
(active#(fst(s(X), cons(Y, Z))) -> mark#(cons(Y, fst(X, Z))), mark#(fst(X1, X2)) -> active#(fst(mark(X1), mark(X2))))
(active#(fst(s(X), cons(Y, Z))) -> mark#(cons(Y, fst(X, Z))), mark#(fst(X1, X2)) -> mark#(X2))
(active#(fst(s(X), cons(Y, Z))) -> mark#(cons(Y, fst(X, Z))), mark#(fst(X1, X2)) -> mark#(X1))
(mark#(add(X1, X2)) -> active#(add(mark(X1), mark(X2))), active#(fst(s(X), cons(Y, Z))) -> mark#(cons(Y, fst(X, Z))))
(mark#(add(X1, X2)) -> active#(add(mark(X1), mark(X2))), active#(add(0(), X)) -> mark#(X))
(mark#(add(X1, X2)) -> active#(add(mark(X1), mark(X2))), active#(add(s(X), Y)) -> mark#(s(add(X, Y))))
(mark#(add(X1, X2)) -> active#(add(mark(X1), mark(X2))), active#(len(cons(X, Z))) -> mark#(s(len(Z))))
(mark#(add(X1, X2)) -> mark#(X1), mark#(fst(X1, X2)) -> mark#(X1))
(mark#(add(X1, X2)) -> mark#(X1), mark#(fst(X1, X2)) -> mark#(X2))
(mark#(add(X1, X2)) -> mark#(X1), mark#(fst(X1, X2)) -> active#(fst(mark(X1), mark(X2))))
(mark#(add(X1, X2)) -> mark#(X1), mark#(cons(X1, X2)) -> mark#(X1))
(mark#(add(X1, X2)) -> mark#(X1), mark#(cons(X1, X2)) -> active#(cons(mark(X1), X2)))
(mark#(add(X1, X2)) -> mark#(X1), mark#(s(X)) -> active#(s(X)))
(mark#(add(X1, X2)) -> mark#(X1), mark#(from(X)) -> active#(from(mark(X))))
(mark#(add(X1, X2)) -> mark#(X1), mark#(add(X1, X2)) -> mark#(X1))
(mark#(add(X1, X2)) -> mark#(X1), mark#(add(X1, X2)) -> mark#(X2))
(mark#(add(X1, X2)) -> mark#(X1), mark#(add(X1, X2)) -> active#(add(mark(X1), mark(X2))))
(mark#(add(X1, X2)) -> mark#(X1), mark#(len(X)) -> mark#(X))
(mark#(add(X1, X2)) -> mark#(X1), mark#(len(X)) -> active#(len(mark(X))))
(mark#(fst(X1, X2)) -> mark#(X1), mark#(fst(X1, X2)) -> mark#(X1))
(mark#(fst(X1, X2)) -> mark#(X1), mark#(fst(X1, X2)) -> mark#(X2))
(mark#(fst(X1, X2)) -> mark#(X1), mark#(fst(X1, X2)) -> active#(fst(mark(X1), mark(X2))))
(mark#(fst(X1, X2)) -> mark#(X1), mark#(cons(X1, X2)) -> mark#(X1))
(mark#(fst(X1, X2)) -> mark#(X1), mark#(cons(X1, X2)) -> active#(cons(mark(X1), X2)))
(mark#(fst(X1, X2)) -> mark#(X1), mark#(s(X)) -> active#(s(X)))
(mark#(fst(X1, X2)) -> mark#(X1), mark#(from(X)) -> active#(from(mark(X))))
(mark#(fst(X1, X2)) -> mark#(X1), mark#(add(X1, X2)) -> mark#(X1))
(mark#(fst(X1, X2)) -> mark#(X1), mark#(add(X1, X2)) -> mark#(X2))
(mark#(fst(X1, X2)) -> mark#(X1), mark#(add(X1, X2)) -> active#(add(mark(X1), mark(X2))))
(mark#(fst(X1, X2)) -> mark#(X1), mark#(len(X)) -> mark#(X))
(mark#(fst(X1, X2)) -> mark#(X1), mark#(len(X)) -> active#(len(mark(X))))
(active#(add(s(X), Y)) -> mark#(s(add(X, Y))), mark#(fst(X1, X2)) -> mark#(X1))
(active#(add(s(X), Y)) -> mark#(s(add(X, Y))), mark#(fst(X1, X2)) -> mark#(X2))
(active#(add(s(X), Y)) -> mark#(s(add(X, Y))), mark#(fst(X1, X2)) -> active#(fst(mark(X1), mark(X2))))
(active#(add(s(X), Y)) -> mark#(s(add(X, Y))), mark#(cons(X1, X2)) -> mark#(X1))
(active#(add(s(X), Y)) -> mark#(s(add(X, Y))), mark#(cons(X1, X2)) -> active#(cons(mark(X1), X2)))
(active#(add(s(X), Y)) -> mark#(s(add(X, Y))), mark#(s(X)) -> active#(s(X)))
(active#(add(s(X), Y)) -> mark#(s(add(X, Y))), mark#(from(X)) -> active#(from(mark(X))))
(active#(add(s(X), Y)) -> mark#(s(add(X, Y))), mark#(add(X1, X2)) -> mark#(X1))
(active#(add(s(X), Y)) -> mark#(s(add(X, Y))), mark#(add(X1, X2)) -> mark#(X2))
(active#(add(s(X), Y)) -> mark#(s(add(X, Y))), mark#(add(X1, X2)) -> active#(add(mark(X1), mark(X2))))
(active#(add(s(X), Y)) -> mark#(s(add(X, Y))), mark#(len(X)) -> mark#(X))
(active#(add(s(X), Y)) -> mark#(s(add(X, Y))), mark#(len(X)) -> active#(len(mark(X))))
(mark#(from(X)) -> active#(from(mark(X))), active#(fst(s(X), cons(Y, Z))) -> mark#(cons(Y, fst(X, Z))))
(mark#(from(X)) -> active#(from(mark(X))), active#(add(0(), X)) -> mark#(X))
(mark#(from(X)) -> active#(from(mark(X))), active#(add(s(X), Y)) -> mark#(s(add(X, Y))))
(mark#(from(X)) -> active#(from(mark(X))), active#(len(cons(X, Z))) -> mark#(s(len(Z))))
(mark#(len(X)) -> mark#(X), mark#(fst(X1, X2)) -> mark#(X1))
(mark#(len(X)) -> mark#(X), mark#(fst(X1, X2)) -> mark#(X2))
(mark#(len(X)) -> mark#(X), mark#(fst(X1, X2)) -> active#(fst(mark(X1), mark(X2))))
(mark#(len(X)) -> mark#(X), mark#(cons(X1, X2)) -> mark#(X1))
(mark#(len(X)) -> mark#(X), mark#(cons(X1, X2)) -> active#(cons(mark(X1), X2)))
(mark#(len(X)) -> mark#(X), mark#(s(X)) -> active#(s(X)))
(mark#(len(X)) -> mark#(X), mark#(from(X)) -> active#(from(mark(X))))
(mark#(len(X)) -> mark#(X), mark#(add(X1, X2)) -> mark#(X1))
(mark#(len(X)) -> mark#(X), mark#(add(X1, X2)) -> mark#(X2))
(mark#(len(X)) -> mark#(X), mark#(add(X1, X2)) -> active#(add(mark(X1), mark(X2))))
(mark#(len(X)) -> mark#(X), mark#(len(X)) -> mark#(X))
(mark#(len(X)) -> mark#(X), mark#(len(X)) -> active#(len(mark(X))))
(mark#(s(X)) -> active#(s(X)), active#(fst(s(X), cons(Y, Z))) -> mark#(cons(Y, fst(X, Z))))
(mark#(s(X)) -> active#(s(X)), active#(add(0(), X)) -> mark#(X))
(mark#(s(X)) -> active#(s(X)), active#(add(s(X), Y)) -> mark#(s(add(X, Y))))
(mark#(s(X)) -> active#(s(X)), active#(len(cons(X, Z))) -> mark#(s(len(Z))))
(mark#(fst(X1, X2)) -> mark#(X2), mark#(fst(X1, X2)) -> mark#(X1))
(mark#(fst(X1, X2)) -> mark#(X2), mark#(fst(X1, X2)) -> mark#(X2))
(mark#(fst(X1, X2)) -> mark#(X2), mark#(fst(X1, X2)) -> active#(fst(mark(X1), mark(X2))))
(mark#(fst(X1, X2)) -> mark#(X2), mark#(cons(X1, X2)) -> mark#(X1))
(mark#(fst(X1, X2)) -> mark#(X2), mark#(cons(X1, X2)) -> active#(cons(mark(X1), X2)))
(mark#(fst(X1, X2)) -> mark#(X2), mark#(s(X)) -> active#(s(X)))
(mark#(fst(X1, X2)) -> mark#(X2), mark#(from(X)) -> active#(from(mark(X))))
(mark#(fst(X1, X2)) -> mark#(X2), mark#(add(X1, X2)) -> mark#(X1))
(mark#(fst(X1, X2)) -> mark#(X2), mark#(add(X1, X2)) -> mark#(X2))
(mark#(fst(X1, X2)) -> mark#(X2), mark#(add(X1, X2)) -> active#(add(mark(X1), mark(X2))))
(mark#(fst(X1, X2)) -> mark#(X2), mark#(len(X)) -> mark#(X))
(mark#(fst(X1, X2)) -> mark#(X2), mark#(len(X)) -> active#(len(mark(X))))
}
SCCS:
Scc:
{ mark#(fst(X1, X2)) -> mark#(X1),
mark#(fst(X1, X2)) -> mark#(X2),
mark#(fst(X1, X2)) -> active#(fst(mark(X1), mark(X2))),
mark#(cons(X1, X2)) -> mark#(X1),
mark#(cons(X1, X2)) -> active#(cons(mark(X1), X2)),
mark#(s(X)) -> active#(s(X)),
mark#(from(X)) -> active#(from(mark(X))),
mark#(add(X1, X2)) -> mark#(X1),
mark#(add(X1, X2)) -> mark#(X2),
mark#(add(X1, X2)) -> active#(add(mark(X1), mark(X2))),
mark#(len(X)) -> mark#(X),
mark#(len(X)) -> active#(len(mark(X))),
active#(fst(s(X), cons(Y, Z))) -> mark#(cons(Y, fst(X, Z))),
active#(add(0(), X)) -> mark#(X),
active#(add(s(X), Y)) -> mark#(s(add(X, Y))),
active#(len(cons(X, Z))) -> mark#(s(len(Z)))}
SCC:
Strict:
{ mark#(fst(X1, X2)) -> mark#(X1),
mark#(fst(X1, X2)) -> mark#(X2),
mark#(fst(X1, X2)) -> active#(fst(mark(X1), mark(X2))),
mark#(cons(X1, X2)) -> mark#(X1),
mark#(cons(X1, X2)) -> active#(cons(mark(X1), X2)),
mark#(s(X)) -> active#(s(X)),
mark#(from(X)) -> active#(from(mark(X))),
mark#(add(X1, X2)) -> mark#(X1),
mark#(add(X1, X2)) -> mark#(X2),
mark#(add(X1, X2)) -> active#(add(mark(X1), mark(X2))),
mark#(len(X)) -> mark#(X),
mark#(len(X)) -> active#(len(mark(X))),
active#(fst(s(X), cons(Y, Z))) -> mark#(cons(Y, fst(X, Z))),
active#(add(0(), X)) -> mark#(X),
active#(add(s(X), Y)) -> mark#(s(add(X, Y))),
active#(len(cons(X, Z))) -> mark#(s(len(Z)))}
Weak:
{ mark(nil()) -> active(nil()),
mark(fst(X1, X2)) -> active(fst(mark(X1), mark(X2))),
mark(0()) -> active(0()),
mark(cons(X1, X2)) -> active(cons(mark(X1), X2)),
mark(s(X)) -> active(s(X)),
mark(from(X)) -> active(from(mark(X))),
mark(add(X1, X2)) -> active(add(mark(X1), mark(X2))),
mark(len(X)) -> active(len(mark(X))),
active(fst(0(), Z)) -> mark(nil()),
active(fst(s(X), cons(Y, Z))) -> mark(cons(Y, fst(X, Z))),
active(from(X)) -> mark(cons(X, from(s(X)))),
active(add(0(), X)) -> mark(X),
active(add(s(X), Y)) -> mark(s(add(X, Y))),
active(len(nil())) -> mark(0()),
active(len(cons(X, Z))) -> mark(s(len(Z))),
fst(X1, mark(X2)) -> fst(X1, X2),
fst(X1, active(X2)) -> fst(X1, X2),
fst(mark(X1), X2) -> fst(X1, X2),
fst(active(X1), X2) -> fst(X1, X2),
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),
from(mark(X)) -> from(X),
from(active(X)) -> from(X),
add(X1, mark(X2)) -> add(X1, X2),
add(X1, active(X2)) -> add(X1, X2),
add(mark(X1), X2) -> add(X1, X2),
add(active(X1), X2) -> add(X1, X2),
len(mark(X)) -> len(X),
len(active(X)) -> len(X)}
POLY:
Argument Filtering:
pi(len) = [0], pi(add) = [0,1], pi(from) = 0, pi(s) = [], pi(cons) = 0, pi(0) = [], pi(fst) = [0,1], pi(active#) = 0, pi(active) = 0, pi(nil) = [], pi(mark#) = 0, pi(mark) = 0
Usable Rules:
{}
Interpretation:
[add](x0, x1) = x0 + x1,
[fst](x0, x1) = x0 + x1,
[len](x0) = x0 + 1,
[s] = 0,
[0] = 0
Strict:
{ mark#(fst(X1, X2)) -> mark#(X1),
mark#(fst(X1, X2)) -> mark#(X2),
mark#(fst(X1, X2)) -> active#(fst(mark(X1), mark(X2))),
mark#(cons(X1, X2)) -> mark#(X1),
mark#(cons(X1, X2)) -> active#(cons(mark(X1), X2)),
mark#(s(X)) -> active#(s(X)),
mark#(from(X)) -> active#(from(mark(X))),
mark#(add(X1, X2)) -> mark#(X1),
mark#(add(X1, X2)) -> mark#(X2),
mark#(add(X1, X2)) -> active#(add(mark(X1), mark(X2))),
mark#(len(X)) -> active#(len(mark(X))),
active#(fst(s(X), cons(Y, Z))) -> mark#(cons(Y, fst(X, Z))),
active#(add(0(), X)) -> mark#(X),
active#(add(s(X), Y)) -> mark#(s(add(X, Y)))}
Weak:
{ mark(nil()) -> active(nil()),
mark(fst(X1, X2)) -> active(fst(mark(X1), mark(X2))),
mark(0()) -> active(0()),
mark(cons(X1, X2)) -> active(cons(mark(X1), X2)),
mark(s(X)) -> active(s(X)),
mark(from(X)) -> active(from(mark(X))),
mark(add(X1, X2)) -> active(add(mark(X1), mark(X2))),
mark(len(X)) -> active(len(mark(X))),
active(fst(0(), Z)) -> mark(nil()),
active(fst(s(X), cons(Y, Z))) -> mark(cons(Y, fst(X, Z))),
active(from(X)) -> mark(cons(X, from(s(X)))),
active(add(0(), X)) -> mark(X),
active(add(s(X), Y)) -> mark(s(add(X, Y))),
active(len(nil())) -> mark(0()),
active(len(cons(X, Z))) -> mark(s(len(Z))),
fst(X1, mark(X2)) -> fst(X1, X2),
fst(X1, active(X2)) -> fst(X1, X2),
fst(mark(X1), X2) -> fst(X1, X2),
fst(active(X1), X2) -> fst(X1, X2),
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),
from(mark(X)) -> from(X),
from(active(X)) -> from(X),
add(X1, mark(X2)) -> add(X1, X2),
add(X1, active(X2)) -> add(X1, X2),
add(mark(X1), X2) -> add(X1, X2),
add(active(X1), X2) -> add(X1, X2),
len(mark(X)) -> len(X),
len(active(X)) -> len(X)}
EDG:
{(mark#(len(X)) -> active#(len(mark(X))), active#(add(s(X), Y)) -> mark#(s(add(X, Y))))
(mark#(len(X)) -> active#(len(mark(X))), active#(add(0(), X)) -> mark#(X))
(mark#(len(X)) -> active#(len(mark(X))), active#(fst(s(X), cons(Y, Z))) -> mark#(cons(Y, fst(X, Z))))
(mark#(fst(X1, X2)) -> mark#(X2), mark#(len(X)) -> active#(len(mark(X))))
(mark#(fst(X1, X2)) -> mark#(X2), mark#(add(X1, X2)) -> active#(add(mark(X1), mark(X2))))
(mark#(fst(X1, X2)) -> mark#(X2), mark#(add(X1, X2)) -> mark#(X2))
(mark#(fst(X1, X2)) -> mark#(X2), mark#(add(X1, X2)) -> mark#(X1))
(mark#(fst(X1, X2)) -> mark#(X2), mark#(from(X)) -> active#(from(mark(X))))
(mark#(fst(X1, X2)) -> mark#(X2), mark#(s(X)) -> active#(s(X)))
(mark#(fst(X1, X2)) -> mark#(X2), mark#(cons(X1, X2)) -> active#(cons(mark(X1), X2)))
(mark#(fst(X1, X2)) -> mark#(X2), mark#(cons(X1, X2)) -> mark#(X1))
(mark#(fst(X1, X2)) -> mark#(X2), mark#(fst(X1, X2)) -> active#(fst(mark(X1), mark(X2))))
(mark#(fst(X1, X2)) -> mark#(X2), mark#(fst(X1, X2)) -> mark#(X2))
(mark#(fst(X1, X2)) -> mark#(X2), mark#(fst(X1, X2)) -> mark#(X1))
(active#(fst(s(X), cons(Y, Z))) -> mark#(cons(Y, fst(X, Z))), mark#(len(X)) -> active#(len(mark(X))))
(active#(fst(s(X), cons(Y, Z))) -> mark#(cons(Y, fst(X, Z))), mark#(add(X1, X2)) -> active#(add(mark(X1), mark(X2))))
(active#(fst(s(X), cons(Y, Z))) -> mark#(cons(Y, fst(X, Z))), mark#(add(X1, X2)) -> mark#(X2))
(active#(fst(s(X), cons(Y, Z))) -> mark#(cons(Y, fst(X, Z))), mark#(add(X1, X2)) -> mark#(X1))
(active#(fst(s(X), cons(Y, Z))) -> mark#(cons(Y, fst(X, Z))), mark#(from(X)) -> active#(from(mark(X))))
(active#(fst(s(X), cons(Y, Z))) -> mark#(cons(Y, fst(X, Z))), mark#(s(X)) -> active#(s(X)))
(active#(fst(s(X), cons(Y, Z))) -> mark#(cons(Y, fst(X, Z))), mark#(cons(X1, X2)) -> active#(cons(mark(X1), X2)))
(active#(fst(s(X), cons(Y, Z))) -> mark#(cons(Y, fst(X, Z))), mark#(cons(X1, X2)) -> mark#(X1))
(active#(fst(s(X), cons(Y, Z))) -> mark#(cons(Y, fst(X, Z))), mark#(fst(X1, X2)) -> active#(fst(mark(X1), mark(X2))))
(active#(fst(s(X), cons(Y, Z))) -> mark#(cons(Y, fst(X, Z))), mark#(fst(X1, X2)) -> mark#(X2))
(active#(fst(s(X), cons(Y, Z))) -> mark#(cons(Y, fst(X, Z))), mark#(fst(X1, X2)) -> mark#(X1))
(mark#(s(X)) -> active#(s(X)), active#(add(s(X), Y)) -> mark#(s(add(X, Y))))
(mark#(s(X)) -> active#(s(X)), active#(add(0(), X)) -> mark#(X))
(mark#(s(X)) -> active#(s(X)), active#(fst(s(X), cons(Y, Z))) -> mark#(cons(Y, fst(X, Z))))
(mark#(fst(X1, X2)) -> mark#(X1), mark#(len(X)) -> active#(len(mark(X))))
(mark#(fst(X1, X2)) -> mark#(X1), mark#(add(X1, X2)) -> active#(add(mark(X1), mark(X2))))
(mark#(fst(X1, X2)) -> mark#(X1), mark#(add(X1, X2)) -> mark#(X2))
(mark#(fst(X1, X2)) -> mark#(X1), mark#(add(X1, X2)) -> mark#(X1))
(mark#(fst(X1, X2)) -> mark#(X1), mark#(from(X)) -> active#(from(mark(X))))
(mark#(fst(X1, X2)) -> mark#(X1), mark#(s(X)) -> active#(s(X)))
(mark#(fst(X1, X2)) -> mark#(X1), mark#(cons(X1, X2)) -> active#(cons(mark(X1), X2)))
(mark#(fst(X1, X2)) -> mark#(X1), mark#(cons(X1, X2)) -> mark#(X1))
(mark#(fst(X1, X2)) -> mark#(X1), mark#(fst(X1, X2)) -> active#(fst(mark(X1), mark(X2))))
(mark#(fst(X1, X2)) -> mark#(X1), mark#(fst(X1, X2)) -> mark#(X2))
(mark#(fst(X1, X2)) -> mark#(X1), mark#(fst(X1, X2)) -> mark#(X1))
(mark#(add(X1, X2)) -> mark#(X1), mark#(len(X)) -> active#(len(mark(X))))
(mark#(add(X1, X2)) -> mark#(X1), mark#(add(X1, X2)) -> active#(add(mark(X1), mark(X2))))
(mark#(add(X1, X2)) -> mark#(X1), mark#(add(X1, X2)) -> mark#(X2))
(mark#(add(X1, X2)) -> mark#(X1), mark#(add(X1, X2)) -> mark#(X1))
(mark#(add(X1, X2)) -> mark#(X1), mark#(from(X)) -> active#(from(mark(X))))
(mark#(add(X1, X2)) -> mark#(X1), mark#(s(X)) -> active#(s(X)))
(mark#(add(X1, X2)) -> mark#(X1), mark#(cons(X1, X2)) -> active#(cons(mark(X1), X2)))
(mark#(add(X1, X2)) -> mark#(X1), mark#(cons(X1, X2)) -> mark#(X1))
(mark#(add(X1, X2)) -> mark#(X1), mark#(fst(X1, X2)) -> active#(fst(mark(X1), mark(X2))))
(mark#(add(X1, X2)) -> mark#(X1), mark#(fst(X1, X2)) -> mark#(X2))
(mark#(add(X1, X2)) -> mark#(X1), mark#(fst(X1, X2)) -> mark#(X1))
(mark#(add(X1, X2)) -> active#(add(mark(X1), mark(X2))), active#(add(s(X), Y)) -> mark#(s(add(X, Y))))
(mark#(add(X1, X2)) -> active#(add(mark(X1), mark(X2))), active#(add(0(), X)) -> mark#(X))
(mark#(add(X1, X2)) -> active#(add(mark(X1), mark(X2))), active#(fst(s(X), cons(Y, Z))) -> mark#(cons(Y, fst(X, Z))))
(mark#(fst(X1, X2)) -> active#(fst(mark(X1), mark(X2))), active#(fst(s(X), cons(Y, Z))) -> mark#(cons(Y, fst(X, Z))))
(mark#(fst(X1, X2)) -> active#(fst(mark(X1), mark(X2))), active#(add(0(), X)) -> mark#(X))
(mark#(fst(X1, X2)) -> active#(fst(mark(X1), mark(X2))), active#(add(s(X), Y)) -> mark#(s(add(X, Y))))
(mark#(cons(X1, X2)) -> mark#(X1), mark#(fst(X1, X2)) -> mark#(X1))
(mark#(cons(X1, X2)) -> mark#(X1), mark#(fst(X1, X2)) -> mark#(X2))
(mark#(cons(X1, X2)) -> mark#(X1), mark#(fst(X1, X2)) -> active#(fst(mark(X1), mark(X2))))
(mark#(cons(X1, X2)) -> mark#(X1), mark#(cons(X1, X2)) -> mark#(X1))
(mark#(cons(X1, X2)) -> mark#(X1), mark#(cons(X1, X2)) -> active#(cons(mark(X1), X2)))
(mark#(cons(X1, X2)) -> mark#(X1), mark#(s(X)) -> active#(s(X)))
(mark#(cons(X1, X2)) -> mark#(X1), mark#(from(X)) -> active#(from(mark(X))))
(mark#(cons(X1, X2)) -> mark#(X1), mark#(add(X1, X2)) -> mark#(X1))
(mark#(cons(X1, X2)) -> mark#(X1), mark#(add(X1, X2)) -> mark#(X2))
(mark#(cons(X1, X2)) -> mark#(X1), mark#(add(X1, X2)) -> active#(add(mark(X1), mark(X2))))
(mark#(cons(X1, X2)) -> mark#(X1), mark#(len(X)) -> active#(len(mark(X))))
(mark#(cons(X1, X2)) -> active#(cons(mark(X1), X2)), active#(fst(s(X), cons(Y, Z))) -> mark#(cons(Y, fst(X, Z))))
(mark#(cons(X1, X2)) -> active#(cons(mark(X1), X2)), active#(add(0(), X)) -> mark#(X))
(mark#(cons(X1, X2)) -> active#(cons(mark(X1), X2)), active#(add(s(X), Y)) -> mark#(s(add(X, Y))))
(active#(add(0(), X)) -> mark#(X), mark#(fst(X1, X2)) -> mark#(X1))
(active#(add(0(), X)) -> mark#(X), mark#(fst(X1, X2)) -> mark#(X2))
(active#(add(0(), X)) -> mark#(X), mark#(fst(X1, X2)) -> active#(fst(mark(X1), mark(X2))))
(active#(add(0(), X)) -> mark#(X), mark#(cons(X1, X2)) -> mark#(X1))
(active#(add(0(), X)) -> mark#(X), mark#(cons(X1, X2)) -> active#(cons(mark(X1), X2)))
(active#(add(0(), X)) -> mark#(X), mark#(s(X)) -> active#(s(X)))
(active#(add(0(), X)) -> mark#(X), mark#(from(X)) -> active#(from(mark(X))))
(active#(add(0(), X)) -> mark#(X), mark#(add(X1, X2)) -> mark#(X1))
(active#(add(0(), X)) -> mark#(X), mark#(add(X1, X2)) -> mark#(X2))
(active#(add(0(), X)) -> mark#(X), mark#(add(X1, X2)) -> active#(add(mark(X1), mark(X2))))
(active#(add(0(), X)) -> mark#(X), mark#(len(X)) -> active#(len(mark(X))))
(mark#(add(X1, X2)) -> mark#(X2), mark#(fst(X1, X2)) -> mark#(X1))
(mark#(add(X1, X2)) -> mark#(X2), mark#(fst(X1, X2)) -> mark#(X2))
(mark#(add(X1, X2)) -> mark#(X2), mark#(fst(X1, X2)) -> active#(fst(mark(X1), mark(X2))))
(mark#(add(X1, X2)) -> mark#(X2), mark#(cons(X1, X2)) -> mark#(X1))
(mark#(add(X1, X2)) -> mark#(X2), mark#(cons(X1, X2)) -> active#(cons(mark(X1), X2)))
(mark#(add(X1, X2)) -> mark#(X2), mark#(s(X)) -> active#(s(X)))
(mark#(add(X1, X2)) -> mark#(X2), mark#(from(X)) -> active#(from(mark(X))))
(mark#(add(X1, X2)) -> mark#(X2), mark#(add(X1, X2)) -> mark#(X1))
(mark#(add(X1, X2)) -> mark#(X2), mark#(add(X1, X2)) -> mark#(X2))
(mark#(add(X1, X2)) -> mark#(X2), mark#(add(X1, X2)) -> active#(add(mark(X1), mark(X2))))
(mark#(add(X1, X2)) -> mark#(X2), mark#(len(X)) -> active#(len(mark(X))))
(active#(add(s(X), Y)) -> mark#(s(add(X, Y))), mark#(fst(X1, X2)) -> mark#(X1))
(active#(add(s(X), Y)) -> mark#(s(add(X, Y))), mark#(fst(X1, X2)) -> mark#(X2))
(active#(add(s(X), Y)) -> mark#(s(add(X, Y))), mark#(fst(X1, X2)) -> active#(fst(mark(X1), mark(X2))))
(active#(add(s(X), Y)) -> mark#(s(add(X, Y))), mark#(cons(X1, X2)) -> mark#(X1))
(active#(add(s(X), Y)) -> mark#(s(add(X, Y))), mark#(cons(X1, X2)) -> active#(cons(mark(X1), X2)))
(active#(add(s(X), Y)) -> mark#(s(add(X, Y))), mark#(s(X)) -> active#(s(X)))
(active#(add(s(X), Y)) -> mark#(s(add(X, Y))), mark#(from(X)) -> active#(from(mark(X))))
(active#(add(s(X), Y)) -> mark#(s(add(X, Y))), mark#(add(X1, X2)) -> mark#(X1))
(active#(add(s(X), Y)) -> mark#(s(add(X, Y))), mark#(add(X1, X2)) -> mark#(X2))
(active#(add(s(X), Y)) -> mark#(s(add(X, Y))), mark#(add(X1, X2)) -> active#(add(mark(X1), mark(X2))))
(active#(add(s(X), Y)) -> mark#(s(add(X, Y))), mark#(len(X)) -> active#(len(mark(X))))
(mark#(from(X)) -> active#(from(mark(X))), active#(fst(s(X), cons(Y, Z))) -> mark#(cons(Y, fst(X, Z))))
(mark#(from(X)) -> active#(from(mark(X))), active#(add(0(), X)) -> mark#(X))
(mark#(from(X)) -> active#(from(mark(X))), active#(add(s(X), Y)) -> mark#(s(add(X, Y))))}
SCCS:
Scc:
{ mark#(fst(X1, X2)) -> mark#(X1),
mark#(fst(X1, X2)) -> mark#(X2),
mark#(fst(X1, X2)) -> active#(fst(mark(X1), mark(X2))),
mark#(cons(X1, X2)) -> mark#(X1),
mark#(cons(X1, X2)) -> active#(cons(mark(X1), X2)),
mark#(s(X)) -> active#(s(X)),
mark#(from(X)) -> active#(from(mark(X))),
mark#(add(X1, X2)) -> mark#(X1),
mark#(add(X1, X2)) -> mark#(X2),
mark#(add(X1, X2)) -> active#(add(mark(X1), mark(X2))),
mark#(len(X)) -> active#(len(mark(X))),
active#(fst(s(X), cons(Y, Z))) -> mark#(cons(Y, fst(X, Z))),
active#(add(0(), X)) -> mark#(X),
active#(add(s(X), Y)) -> mark#(s(add(X, Y)))}
SCC:
Strict:
{ mark#(fst(X1, X2)) -> mark#(X1),
mark#(fst(X1, X2)) -> mark#(X2),
mark#(fst(X1, X2)) -> active#(fst(mark(X1), mark(X2))),
mark#(cons(X1, X2)) -> mark#(X1),
mark#(cons(X1, X2)) -> active#(cons(mark(X1), X2)),
mark#(s(X)) -> active#(s(X)),
mark#(from(X)) -> active#(from(mark(X))),
mark#(add(X1, X2)) -> mark#(X1),
mark#(add(X1, X2)) -> mark#(X2),
mark#(add(X1, X2)) -> active#(add(mark(X1), mark(X2))),
mark#(len(X)) -> active#(len(mark(X))),
active#(fst(s(X), cons(Y, Z))) -> mark#(cons(Y, fst(X, Z))),
active#(add(0(), X)) -> mark#(X),
active#(add(s(X), Y)) -> mark#(s(add(X, Y)))}
Weak:
{ mark(nil()) -> active(nil()),
mark(fst(X1, X2)) -> active(fst(mark(X1), mark(X2))),
mark(0()) -> active(0()),
mark(cons(X1, X2)) -> active(cons(mark(X1), X2)),
mark(s(X)) -> active(s(X)),
mark(from(X)) -> active(from(mark(X))),
mark(add(X1, X2)) -> active(add(mark(X1), mark(X2))),
mark(len(X)) -> active(len(mark(X))),
active(fst(0(), Z)) -> mark(nil()),
active(fst(s(X), cons(Y, Z))) -> mark(cons(Y, fst(X, Z))),
active(from(X)) -> mark(cons(X, from(s(X)))),
active(add(0(), X)) -> mark(X),
active(add(s(X), Y)) -> mark(s(add(X, Y))),
active(len(nil())) -> mark(0()),
active(len(cons(X, Z))) -> mark(s(len(Z))),
fst(X1, mark(X2)) -> fst(X1, X2),
fst(X1, active(X2)) -> fst(X1, X2),
fst(mark(X1), X2) -> fst(X1, X2),
fst(active(X1), X2) -> fst(X1, X2),
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),
from(mark(X)) -> from(X),
from(active(X)) -> from(X),
add(X1, mark(X2)) -> add(X1, X2),
add(X1, active(X2)) -> add(X1, X2),
add(mark(X1), X2) -> add(X1, X2),
add(active(X1), X2) -> add(X1, X2),
len(mark(X)) -> len(X),
len(active(X)) -> len(X)}
POLY:
Argument Filtering:
pi(len) = 0, pi(add) = [0,1], pi(from) = 0, pi(s) = [], pi(cons) = 0, pi(0) = [], pi(fst) = [0,1], pi(active#) = 0, pi(active) = 0, pi(nil) = [], pi(mark#) = 0, pi(mark) = 0
Usable Rules:
{}
Interpretation:
[add](x0, x1) = x0 + x1,
[fst](x0, x1) = x0 + x1,
[s] = 0,
[0] = 1
Strict:
{ mark#(fst(X1, X2)) -> mark#(X1),
mark#(fst(X1, X2)) -> mark#(X2),
mark#(fst(X1, X2)) -> active#(fst(mark(X1), mark(X2))),
mark#(cons(X1, X2)) -> mark#(X1),
mark#(cons(X1, X2)) -> active#(cons(mark(X1), X2)),
mark#(s(X)) -> active#(s(X)),
mark#(from(X)) -> active#(from(mark(X))),
mark#(add(X1, X2)) -> mark#(X1),
mark#(add(X1, X2)) -> mark#(X2),
mark#(add(X1, X2)) -> active#(add(mark(X1), mark(X2))),
mark#(len(X)) -> active#(len(mark(X))),
active#(fst(s(X), cons(Y, Z))) -> mark#(cons(Y, fst(X, Z))),
active#(add(s(X), Y)) -> mark#(s(add(X, Y)))}
Weak:
{ mark(nil()) -> active(nil()),
mark(fst(X1, X2)) -> active(fst(mark(X1), mark(X2))),
mark(0()) -> active(0()),
mark(cons(X1, X2)) -> active(cons(mark(X1), X2)),
mark(s(X)) -> active(s(X)),
mark(from(X)) -> active(from(mark(X))),
mark(add(X1, X2)) -> active(add(mark(X1), mark(X2))),
mark(len(X)) -> active(len(mark(X))),
active(fst(0(), Z)) -> mark(nil()),
active(fst(s(X), cons(Y, Z))) -> mark(cons(Y, fst(X, Z))),
active(from(X)) -> mark(cons(X, from(s(X)))),
active(add(0(), X)) -> mark(X),
active(add(s(X), Y)) -> mark(s(add(X, Y))),
active(len(nil())) -> mark(0()),
active(len(cons(X, Z))) -> mark(s(len(Z))),
fst(X1, mark(X2)) -> fst(X1, X2),
fst(X1, active(X2)) -> fst(X1, X2),
fst(mark(X1), X2) -> fst(X1, X2),
fst(active(X1), X2) -> fst(X1, X2),
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),
from(mark(X)) -> from(X),
from(active(X)) -> from(X),
add(X1, mark(X2)) -> add(X1, X2),
add(X1, active(X2)) -> add(X1, X2),
add(mark(X1), X2) -> add(X1, X2),
add(active(X1), X2) -> add(X1, X2),
len(mark(X)) -> len(X),
len(active(X)) -> len(X)}
EDG:
{(mark#(cons(X1, X2)) -> active#(cons(mark(X1), X2)), active#(add(s(X), Y)) -> mark#(s(add(X, Y))))
(mark#(cons(X1, X2)) -> active#(cons(mark(X1), X2)), active#(fst(s(X), cons(Y, Z))) -> mark#(cons(Y, fst(X, Z))))
(mark#(len(X)) -> active#(len(mark(X))), active#(add(s(X), Y)) -> mark#(s(add(X, Y))))
(mark#(len(X)) -> active#(len(mark(X))), active#(fst(s(X), cons(Y, Z))) -> mark#(cons(Y, fst(X, Z))))
(mark#(fst(X1, X2)) -> mark#(X1), mark#(len(X)) -> active#(len(mark(X))))
(mark#(fst(X1, X2)) -> mark#(X1), mark#(add(X1, X2)) -> active#(add(mark(X1), mark(X2))))
(mark#(fst(X1, X2)) -> mark#(X1), mark#(add(X1, X2)) -> mark#(X2))
(mark#(fst(X1, X2)) -> mark#(X1), mark#(add(X1, X2)) -> mark#(X1))
(mark#(fst(X1, X2)) -> mark#(X1), mark#(from(X)) -> active#(from(mark(X))))
(mark#(fst(X1, X2)) -> mark#(X1), mark#(s(X)) -> active#(s(X)))
(mark#(fst(X1, X2)) -> mark#(X1), mark#(cons(X1, X2)) -> active#(cons(mark(X1), X2)))
(mark#(fst(X1, X2)) -> mark#(X1), mark#(cons(X1, X2)) -> mark#(X1))
(mark#(fst(X1, X2)) -> mark#(X1), mark#(fst(X1, X2)) -> active#(fst(mark(X1), mark(X2))))
(mark#(fst(X1, X2)) -> mark#(X1), mark#(fst(X1, X2)) -> mark#(X2))
(mark#(fst(X1, X2)) -> mark#(X1), mark#(fst(X1, X2)) -> mark#(X1))
(mark#(add(X1, X2)) -> mark#(X1), mark#(len(X)) -> active#(len(mark(X))))
(mark#(add(X1, X2)) -> mark#(X1), mark#(add(X1, X2)) -> active#(add(mark(X1), mark(X2))))
(mark#(add(X1, X2)) -> mark#(X1), mark#(add(X1, X2)) -> mark#(X2))
(mark#(add(X1, X2)) -> mark#(X1), mark#(add(X1, X2)) -> mark#(X1))
(mark#(add(X1, X2)) -> mark#(X1), mark#(from(X)) -> active#(from(mark(X))))
(mark#(add(X1, X2)) -> mark#(X1), mark#(s(X)) -> active#(s(X)))
(mark#(add(X1, X2)) -> mark#(X1), mark#(cons(X1, X2)) -> active#(cons(mark(X1), X2)))
(mark#(add(X1, X2)) -> mark#(X1), mark#(cons(X1, X2)) -> mark#(X1))
(mark#(add(X1, X2)) -> mark#(X1), mark#(fst(X1, X2)) -> active#(fst(mark(X1), mark(X2))))
(mark#(add(X1, X2)) -> mark#(X1), mark#(fst(X1, X2)) -> mark#(X2))
(mark#(add(X1, X2)) -> mark#(X1), mark#(fst(X1, X2)) -> mark#(X1))
(mark#(add(X1, X2)) -> active#(add(mark(X1), mark(X2))), active#(add(s(X), Y)) -> mark#(s(add(X, Y))))
(mark#(add(X1, X2)) -> active#(add(mark(X1), mark(X2))), active#(fst(s(X), cons(Y, Z))) -> mark#(cons(Y, fst(X, Z))))
(mark#(add(X1, X2)) -> mark#(X2), mark#(len(X)) -> active#(len(mark(X))))
(mark#(add(X1, X2)) -> mark#(X2), mark#(add(X1, X2)) -> active#(add(mark(X1), mark(X2))))
(mark#(add(X1, X2)) -> mark#(X2), mark#(add(X1, X2)) -> mark#(X2))
(mark#(add(X1, X2)) -> mark#(X2), mark#(add(X1, X2)) -> mark#(X1))
(mark#(add(X1, X2)) -> mark#(X2), mark#(from(X)) -> active#(from(mark(X))))
(mark#(add(X1, X2)) -> mark#(X2), mark#(s(X)) -> active#(s(X)))
(mark#(add(X1, X2)) -> mark#(X2), mark#(cons(X1, X2)) -> active#(cons(mark(X1), X2)))
(mark#(add(X1, X2)) -> mark#(X2), mark#(cons(X1, X2)) -> mark#(X1))
(mark#(add(X1, X2)) -> mark#(X2), mark#(fst(X1, X2)) -> active#(fst(mark(X1), mark(X2))))
(mark#(add(X1, X2)) -> mark#(X2), mark#(fst(X1, X2)) -> mark#(X2))
(mark#(add(X1, X2)) -> mark#(X2), mark#(fst(X1, X2)) -> mark#(X1))
(mark#(s(X)) -> active#(s(X)), active#(fst(s(X), cons(Y, Z))) -> mark#(cons(Y, fst(X, Z))))
(mark#(s(X)) -> active#(s(X)), active#(add(s(X), Y)) -> mark#(s(add(X, Y))))
(mark#(fst(X1, X2)) -> mark#(X2), mark#(fst(X1, X2)) -> mark#(X1))
(mark#(fst(X1, X2)) -> mark#(X2), mark#(fst(X1, X2)) -> mark#(X2))
(mark#(fst(X1, X2)) -> mark#(X2), mark#(fst(X1, X2)) -> active#(fst(mark(X1), mark(X2))))
(mark#(fst(X1, X2)) -> mark#(X2), mark#(cons(X1, X2)) -> mark#(X1))
(mark#(fst(X1, X2)) -> mark#(X2), mark#(cons(X1, X2)) -> active#(cons(mark(X1), X2)))
(mark#(fst(X1, X2)) -> mark#(X2), mark#(s(X)) -> active#(s(X)))
(mark#(fst(X1, X2)) -> mark#(X2), mark#(from(X)) -> active#(from(mark(X))))
(mark#(fst(X1, X2)) -> mark#(X2), mark#(add(X1, X2)) -> mark#(X1))
(mark#(fst(X1, X2)) -> mark#(X2), mark#(add(X1, X2)) -> mark#(X2))
(mark#(fst(X1, X2)) -> mark#(X2), mark#(add(X1, X2)) -> active#(add(mark(X1), mark(X2))))
(mark#(fst(X1, X2)) -> mark#(X2), mark#(len(X)) -> active#(len(mark(X))))
(mark#(fst(X1, X2)) -> active#(fst(mark(X1), mark(X2))), active#(fst(s(X), cons(Y, Z))) -> mark#(cons(Y, fst(X, Z))))
(mark#(fst(X1, X2)) -> active#(fst(mark(X1), mark(X2))), active#(add(s(X), Y)) -> mark#(s(add(X, Y))))
(mark#(cons(X1, X2)) -> mark#(X1), mark#(fst(X1, X2)) -> mark#(X1))
(mark#(cons(X1, X2)) -> mark#(X1), mark#(fst(X1, X2)) -> mark#(X2))
(mark#(cons(X1, X2)) -> mark#(X1), mark#(fst(X1, X2)) -> active#(fst(mark(X1), mark(X2))))
(mark#(cons(X1, X2)) -> mark#(X1), mark#(cons(X1, X2)) -> mark#(X1))
(mark#(cons(X1, X2)) -> mark#(X1), mark#(cons(X1, X2)) -> active#(cons(mark(X1), X2)))
(mark#(cons(X1, X2)) -> mark#(X1), mark#(s(X)) -> active#(s(X)))
(mark#(cons(X1, X2)) -> mark#(X1), mark#(from(X)) -> active#(from(mark(X))))
(mark#(cons(X1, X2)) -> mark#(X1), mark#(add(X1, X2)) -> mark#(X1))
(mark#(cons(X1, X2)) -> mark#(X1), mark#(add(X1, X2)) -> mark#(X2))
(mark#(cons(X1, X2)) -> mark#(X1), mark#(add(X1, X2)) -> active#(add(mark(X1), mark(X2))))
(mark#(cons(X1, X2)) -> mark#(X1), mark#(len(X)) -> active#(len(mark(X))))
(active#(add(s(X), Y)) -> mark#(s(add(X, Y))), mark#(fst(X1, X2)) -> mark#(X1))
(active#(add(s(X), Y)) -> mark#(s(add(X, Y))), mark#(fst(X1, X2)) -> mark#(X2))
(active#(add(s(X), Y)) -> mark#(s(add(X, Y))), mark#(fst(X1, X2)) -> active#(fst(mark(X1), mark(X2))))
(active#(add(s(X), Y)) -> mark#(s(add(X, Y))), mark#(cons(X1, X2)) -> mark#(X1))
(active#(add(s(X), Y)) -> mark#(s(add(X, Y))), mark#(cons(X1, X2)) -> active#(cons(mark(X1), X2)))
(active#(add(s(X), Y)) -> mark#(s(add(X, Y))), mark#(s(X)) -> active#(s(X)))
(active#(add(s(X), Y)) -> mark#(s(add(X, Y))), mark#(from(X)) -> active#(from(mark(X))))
(active#(add(s(X), Y)) -> mark#(s(add(X, Y))), mark#(add(X1, X2)) -> mark#(X1))
(active#(add(s(X), Y)) -> mark#(s(add(X, Y))), mark#(add(X1, X2)) -> mark#(X2))
(active#(add(s(X), Y)) -> mark#(s(add(X, Y))), mark#(add(X1, X2)) -> active#(add(mark(X1), mark(X2))))
(active#(add(s(X), Y)) -> mark#(s(add(X, Y))), mark#(len(X)) -> active#(len(mark(X))))
(mark#(from(X)) -> active#(from(mark(X))), active#(fst(s(X), cons(Y, Z))) -> mark#(cons(Y, fst(X, Z))))
(mark#(from(X)) -> active#(from(mark(X))), active#(add(s(X), Y)) -> mark#(s(add(X, Y))))
(active#(fst(s(X), cons(Y, Z))) -> mark#(cons(Y, fst(X, Z))), mark#(fst(X1, X2)) -> mark#(X1))
(active#(fst(s(X), cons(Y, Z))) -> mark#(cons(Y, fst(X, Z))), mark#(fst(X1, X2)) -> mark#(X2))
(active#(fst(s(X), cons(Y, Z))) -> mark#(cons(Y, fst(X, Z))), mark#(fst(X1, X2)) -> active#(fst(mark(X1), mark(X2))))
(active#(fst(s(X), cons(Y, Z))) -> mark#(cons(Y, fst(X, Z))), mark#(cons(X1, X2)) -> mark#(X1))
(active#(fst(s(X), cons(Y, Z))) -> mark#(cons(Y, fst(X, Z))), mark#(cons(X1, X2)) -> active#(cons(mark(X1), X2)))
(active#(fst(s(X), cons(Y, Z))) -> mark#(cons(Y, fst(X, Z))), mark#(s(X)) -> active#(s(X)))
(active#(fst(s(X), cons(Y, Z))) -> mark#(cons(Y, fst(X, Z))), mark#(from(X)) -> active#(from(mark(X))))
(active#(fst(s(X), cons(Y, Z))) -> mark#(cons(Y, fst(X, Z))), mark#(add(X1, X2)) -> mark#(X1))
(active#(fst(s(X), cons(Y, Z))) -> mark#(cons(Y, fst(X, Z))), mark#(add(X1, X2)) -> mark#(X2))
(active#(fst(s(X), cons(Y, Z))) -> mark#(cons(Y, fst(X, Z))), mark#(add(X1, X2)) -> active#(add(mark(X1), mark(X2))))
(active#(fst(s(X), cons(Y, Z))) -> mark#(cons(Y, fst(X, Z))), mark#(len(X)) -> active#(len(mark(X))))}
SCCS:
Scc:
{ mark#(fst(X1, X2)) -> mark#(X1),
mark#(fst(X1, X2)) -> mark#(X2),
mark#(fst(X1, X2)) -> active#(fst(mark(X1), mark(X2))),
mark#(cons(X1, X2)) -> mark#(X1),
mark#(cons(X1, X2)) -> active#(cons(mark(X1), X2)),
mark#(s(X)) -> active#(s(X)),
mark#(from(X)) -> active#(from(mark(X))),
mark#(add(X1, X2)) -> mark#(X1),
mark#(add(X1, X2)) -> mark#(X2),
mark#(add(X1, X2)) -> active#(add(mark(X1), mark(X2))),
mark#(len(X)) -> active#(len(mark(X))),
active#(fst(s(X), cons(Y, Z))) -> mark#(cons(Y, fst(X, Z))),
active#(add(s(X), Y)) -> mark#(s(add(X, Y)))}
SCC:
Strict:
{ mark#(fst(X1, X2)) -> mark#(X1),
mark#(fst(X1, X2)) -> mark#(X2),
mark#(fst(X1, X2)) -> active#(fst(mark(X1), mark(X2))),
mark#(cons(X1, X2)) -> mark#(X1),
mark#(cons(X1, X2)) -> active#(cons(mark(X1), X2)),
mark#(s(X)) -> active#(s(X)),
mark#(from(X)) -> active#(from(mark(X))),
mark#(add(X1, X2)) -> mark#(X1),
mark#(add(X1, X2)) -> mark#(X2),
mark#(add(X1, X2)) -> active#(add(mark(X1), mark(X2))),
mark#(len(X)) -> active#(len(mark(X))),
active#(fst(s(X), cons(Y, Z))) -> mark#(cons(Y, fst(X, Z))),
active#(add(s(X), Y)) -> mark#(s(add(X, Y)))}
Weak:
{ mark(nil()) -> active(nil()),
mark(fst(X1, X2)) -> active(fst(mark(X1), mark(X2))),
mark(0()) -> active(0()),
mark(cons(X1, X2)) -> active(cons(mark(X1), X2)),
mark(s(X)) -> active(s(X)),
mark(from(X)) -> active(from(mark(X))),
mark(add(X1, X2)) -> active(add(mark(X1), mark(X2))),
mark(len(X)) -> active(len(mark(X))),
active(fst(0(), Z)) -> mark(nil()),
active(fst(s(X), cons(Y, Z))) -> mark(cons(Y, fst(X, Z))),
active(from(X)) -> mark(cons(X, from(s(X)))),
active(add(0(), X)) -> mark(X),
active(add(s(X), Y)) -> mark(s(add(X, Y))),
active(len(nil())) -> mark(0()),
active(len(cons(X, Z))) -> mark(s(len(Z))),
fst(X1, mark(X2)) -> fst(X1, X2),
fst(X1, active(X2)) -> fst(X1, X2),
fst(mark(X1), X2) -> fst(X1, X2),
fst(active(X1), X2) -> fst(X1, X2),
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),
from(mark(X)) -> from(X),
from(active(X)) -> from(X),
add(X1, mark(X2)) -> add(X1, X2),
add(X1, active(X2)) -> add(X1, X2),
add(mark(X1), X2) -> add(X1, X2),
add(active(X1), X2) -> add(X1, X2),
len(mark(X)) -> len(X),
len(active(X)) -> len(X)}
POLY:
Argument Filtering:
pi(len) = [], pi(add) = [0,1], pi(from) = 0, pi(s) = [], pi(cons) = 0, pi(0) = [], pi(fst) = [0,1], pi(active#) = [0], pi(active) = 0, pi(nil) = [], pi(mark#) = [0], pi(mark) = 0
Usable Rules:
{}
Interpretation:
[active#](x0) = x0 + 1,
[mark#](x0) = x0 + 1,
[add](x0, x1) = x0 + x1 + 1,
[fst](x0, x1) = x0 + x1,
[len] = 0,
[s] = 0
Strict:
{ mark#(fst(X1, X2)) -> mark#(X1),
mark#(fst(X1, X2)) -> mark#(X2),
mark#(fst(X1, X2)) -> active#(fst(mark(X1), mark(X2))),
mark#(cons(X1, X2)) -> mark#(X1),
mark#(cons(X1, X2)) -> active#(cons(mark(X1), X2)),
mark#(s(X)) -> active#(s(X)),
mark#(from(X)) -> active#(from(mark(X))),
mark#(add(X1, X2)) -> active#(add(mark(X1), mark(X2))),
mark#(len(X)) -> active#(len(mark(X))),
active#(fst(s(X), cons(Y, Z))) -> mark#(cons(Y, fst(X, Z)))}
Weak:
{ mark(nil()) -> active(nil()),
mark(fst(X1, X2)) -> active(fst(mark(X1), mark(X2))),
mark(0()) -> active(0()),
mark(cons(X1, X2)) -> active(cons(mark(X1), X2)),
mark(s(X)) -> active(s(X)),
mark(from(X)) -> active(from(mark(X))),
mark(add(X1, X2)) -> active(add(mark(X1), mark(X2))),
mark(len(X)) -> active(len(mark(X))),
active(fst(0(), Z)) -> mark(nil()),
active(fst(s(X), cons(Y, Z))) -> mark(cons(Y, fst(X, Z))),
active(from(X)) -> mark(cons(X, from(s(X)))),
active(add(0(), X)) -> mark(X),
active(add(s(X), Y)) -> mark(s(add(X, Y))),
active(len(nil())) -> mark(0()),
active(len(cons(X, Z))) -> mark(s(len(Z))),
fst(X1, mark(X2)) -> fst(X1, X2),
fst(X1, active(X2)) -> fst(X1, X2),
fst(mark(X1), X2) -> fst(X1, X2),
fst(active(X1), X2) -> fst(X1, X2),
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),
from(mark(X)) -> from(X),
from(active(X)) -> from(X),
add(X1, mark(X2)) -> add(X1, X2),
add(X1, active(X2)) -> add(X1, X2),
add(mark(X1), X2) -> add(X1, X2),
add(active(X1), X2) -> add(X1, X2),
len(mark(X)) -> len(X),
len(active(X)) -> len(X)}
EDG:
{(mark#(cons(X1, X2)) -> mark#(X1), mark#(len(X)) -> active#(len(mark(X))))
(mark#(cons(X1, X2)) -> mark#(X1), mark#(add(X1, X2)) -> active#(add(mark(X1), mark(X2))))
(mark#(cons(X1, X2)) -> mark#(X1), mark#(from(X)) -> active#(from(mark(X))))
(mark#(cons(X1, X2)) -> mark#(X1), mark#(s(X)) -> active#(s(X)))
(mark#(cons(X1, X2)) -> mark#(X1), mark#(cons(X1, X2)) -> active#(cons(mark(X1), X2)))
(mark#(cons(X1, X2)) -> mark#(X1), mark#(cons(X1, X2)) -> mark#(X1))
(mark#(cons(X1, X2)) -> mark#(X1), mark#(fst(X1, X2)) -> active#(fst(mark(X1), mark(X2))))
(mark#(cons(X1, X2)) -> mark#(X1), mark#(fst(X1, X2)) -> mark#(X2))
(mark#(cons(X1, X2)) -> mark#(X1), mark#(fst(X1, X2)) -> mark#(X1))
(mark#(s(X)) -> active#(s(X)), active#(fst(s(X), cons(Y, Z))) -> mark#(cons(Y, fst(X, Z))))
(mark#(add(X1, X2)) -> active#(add(mark(X1), mark(X2))), active#(fst(s(X), cons(Y, Z))) -> mark#(cons(Y, fst(X, Z))))
(mark#(cons(X1, X2)) -> active#(cons(mark(X1), X2)), active#(fst(s(X), cons(Y, Z))) -> mark#(cons(Y, fst(X, Z))))
(mark#(len(X)) -> active#(len(mark(X))), active#(fst(s(X), cons(Y, Z))) -> mark#(cons(Y, fst(X, Z))))
(mark#(from(X)) -> active#(from(mark(X))), active#(fst(s(X), cons(Y, Z))) -> mark#(cons(Y, fst(X, Z))))
(active#(fst(s(X), cons(Y, Z))) -> mark#(cons(Y, fst(X, Z))), mark#(fst(X1, X2)) -> mark#(X1))
(active#(fst(s(X), cons(Y, Z))) -> mark#(cons(Y, fst(X, Z))), mark#(fst(X1, X2)) -> mark#(X2))
(active#(fst(s(X), cons(Y, Z))) -> mark#(cons(Y, fst(X, Z))), mark#(fst(X1, X2)) -> active#(fst(mark(X1), mark(X2))))
(active#(fst(s(X), cons(Y, Z))) -> mark#(cons(Y, fst(X, Z))), mark#(cons(X1, X2)) -> mark#(X1))
(active#(fst(s(X), cons(Y, Z))) -> mark#(cons(Y, fst(X, Z))), mark#(cons(X1, X2)) -> active#(cons(mark(X1), X2)))
(active#(fst(s(X), cons(Y, Z))) -> mark#(cons(Y, fst(X, Z))), mark#(s(X)) -> active#(s(X)))
(active#(fst(s(X), cons(Y, Z))) -> mark#(cons(Y, fst(X, Z))), mark#(from(X)) -> active#(from(mark(X))))
(active#(fst(s(X), cons(Y, Z))) -> mark#(cons(Y, fst(X, Z))), mark#(add(X1, X2)) -> active#(add(mark(X1), mark(X2))))
(active#(fst(s(X), cons(Y, Z))) -> mark#(cons(Y, fst(X, Z))), mark#(len(X)) -> active#(len(mark(X))))
(mark#(fst(X1, X2)) -> active#(fst(mark(X1), mark(X2))), active#(fst(s(X), cons(Y, Z))) -> mark#(cons(Y, fst(X, Z))))
(mark#(fst(X1, X2)) -> mark#(X2), mark#(fst(X1, X2)) -> mark#(X1))
(mark#(fst(X1, X2)) -> mark#(X2), mark#(fst(X1, X2)) -> mark#(X2))
(mark#(fst(X1, X2)) -> mark#(X2), mark#(fst(X1, X2)) -> active#(fst(mark(X1), mark(X2))))
(mark#(fst(X1, X2)) -> mark#(X2), mark#(cons(X1, X2)) -> mark#(X1))
(mark#(fst(X1, X2)) -> mark#(X2), mark#(cons(X1, X2)) -> active#(cons(mark(X1), X2)))
(mark#(fst(X1, X2)) -> mark#(X2), mark#(s(X)) -> active#(s(X)))
(mark#(fst(X1, X2)) -> mark#(X2), mark#(from(X)) -> active#(from(mark(X))))
(mark#(fst(X1, X2)) -> mark#(X2), mark#(add(X1, X2)) -> active#(add(mark(X1), mark(X2))))
(mark#(fst(X1, X2)) -> mark#(X2), mark#(len(X)) -> active#(len(mark(X))))
(mark#(fst(X1, X2)) -> mark#(X1), mark#(fst(X1, X2)) -> mark#(X1))
(mark#(fst(X1, X2)) -> mark#(X1), mark#(fst(X1, X2)) -> mark#(X2))
(mark#(fst(X1, X2)) -> mark#(X1), mark#(fst(X1, X2)) -> active#(fst(mark(X1), mark(X2))))
(mark#(fst(X1, X2)) -> mark#(X1), mark#(cons(X1, X2)) -> mark#(X1))
(mark#(fst(X1, X2)) -> mark#(X1), mark#(cons(X1, X2)) -> active#(cons(mark(X1), X2)))
(mark#(fst(X1, X2)) -> mark#(X1), mark#(s(X)) -> active#(s(X)))
(mark#(fst(X1, X2)) -> mark#(X1), mark#(from(X)) -> active#(from(mark(X))))
(mark#(fst(X1, X2)) -> mark#(X1), mark#(add(X1, X2)) -> active#(add(mark(X1), mark(X2))))
(mark#(fst(X1, X2)) -> mark#(X1), mark#(len(X)) -> active#(len(mark(X))))}
SCCS:
Scc:
{ mark#(fst(X1, X2)) -> mark#(X1),
mark#(fst(X1, X2)) -> mark#(X2),
mark#(fst(X1, X2)) -> active#(fst(mark(X1), mark(X2))),
mark#(cons(X1, X2)) -> mark#(X1),
mark#(cons(X1, X2)) -> active#(cons(mark(X1), X2)),
mark#(s(X)) -> active#(s(X)),
mark#(from(X)) -> active#(from(mark(X))),
mark#(add(X1, X2)) -> active#(add(mark(X1), mark(X2))),
mark#(len(X)) -> active#(len(mark(X))),
active#(fst(s(X), cons(Y, Z))) -> mark#(cons(Y, fst(X, Z)))}
SCC:
Strict:
{ mark#(fst(X1, X2)) -> mark#(X1),
mark#(fst(X1, X2)) -> mark#(X2),
mark#(fst(X1, X2)) -> active#(fst(mark(X1), mark(X2))),
mark#(cons(X1, X2)) -> mark#(X1),
mark#(cons(X1, X2)) -> active#(cons(mark(X1), X2)),
mark#(s(X)) -> active#(s(X)),
mark#(from(X)) -> active#(from(mark(X))),
mark#(add(X1, X2)) -> active#(add(mark(X1), mark(X2))),
mark#(len(X)) -> active#(len(mark(X))),
active#(fst(s(X), cons(Y, Z))) -> mark#(cons(Y, fst(X, Z)))}
Weak:
{ mark(nil()) -> active(nil()),
mark(fst(X1, X2)) -> active(fst(mark(X1), mark(X2))),
mark(0()) -> active(0()),
mark(cons(X1, X2)) -> active(cons(mark(X1), X2)),
mark(s(X)) -> active(s(X)),
mark(from(X)) -> active(from(mark(X))),
mark(add(X1, X2)) -> active(add(mark(X1), mark(X2))),
mark(len(X)) -> active(len(mark(X))),
active(fst(0(), Z)) -> mark(nil()),
active(fst(s(X), cons(Y, Z))) -> mark(cons(Y, fst(X, Z))),
active(from(X)) -> mark(cons(X, from(s(X)))),
active(add(0(), X)) -> mark(X),
active(add(s(X), Y)) -> mark(s(add(X, Y))),
active(len(nil())) -> mark(0()),
active(len(cons(X, Z))) -> mark(s(len(Z))),
fst(X1, mark(X2)) -> fst(X1, X2),
fst(X1, active(X2)) -> fst(X1, X2),
fst(mark(X1), X2) -> fst(X1, X2),
fst(active(X1), X2) -> fst(X1, X2),
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),
from(mark(X)) -> from(X),
from(active(X)) -> from(X),
add(X1, mark(X2)) -> add(X1, X2),
add(X1, active(X2)) -> add(X1, X2),
add(mark(X1), X2) -> add(X1, X2),
add(active(X1), X2) -> add(X1, X2),
len(mark(X)) -> len(X),
len(active(X)) -> len(X)}
POLY:
Argument Filtering:
pi(len) = [], pi(add) = [], pi(from) = [], pi(s) = [], pi(cons) = [], pi(0) = [], pi(fst) = [], pi(active#) = 0, pi(active) = [], pi(nil) = [], pi(mark#) = [], pi(mark) = []
Usable Rules:
{}
Interpretation:
[mark#] = 1,
[add] = 0,
[cons] = 0,
[fst] = 1,
[len] = 0,
[from] = 0,
[s] = 0
Strict:
{ mark#(fst(X1, X2)) -> mark#(X1),
mark#(fst(X1, X2)) -> mark#(X2),
mark#(fst(X1, X2)) -> active#(fst(mark(X1), mark(X2))),
mark#(cons(X1, X2)) -> mark#(X1),
active#(fst(s(X), cons(Y, Z))) -> mark#(cons(Y, fst(X, Z)))}
Weak:
{ mark(nil()) -> active(nil()),
mark(fst(X1, X2)) -> active(fst(mark(X1), mark(X2))),
mark(0()) -> active(0()),
mark(cons(X1, X2)) -> active(cons(mark(X1), X2)),
mark(s(X)) -> active(s(X)),
mark(from(X)) -> active(from(mark(X))),
mark(add(X1, X2)) -> active(add(mark(X1), mark(X2))),
mark(len(X)) -> active(len(mark(X))),
active(fst(0(), Z)) -> mark(nil()),
active(fst(s(X), cons(Y, Z))) -> mark(cons(Y, fst(X, Z))),
active(from(X)) -> mark(cons(X, from(s(X)))),
active(add(0(), X)) -> mark(X),
active(add(s(X), Y)) -> mark(s(add(X, Y))),
active(len(nil())) -> mark(0()),
active(len(cons(X, Z))) -> mark(s(len(Z))),
fst(X1, mark(X2)) -> fst(X1, X2),
fst(X1, active(X2)) -> fst(X1, X2),
fst(mark(X1), X2) -> fst(X1, X2),
fst(active(X1), X2) -> fst(X1, X2),
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),
from(mark(X)) -> from(X),
from(active(X)) -> from(X),
add(X1, mark(X2)) -> add(X1, X2),
add(X1, active(X2)) -> add(X1, X2),
add(mark(X1), X2) -> add(X1, X2),
add(active(X1), X2) -> add(X1, X2),
len(mark(X)) -> len(X),
len(active(X)) -> len(X)}
EDG:
{(mark#(cons(X1, X2)) -> mark#(X1), mark#(cons(X1, X2)) -> mark#(X1))
(mark#(cons(X1, X2)) -> mark#(X1), mark#(fst(X1, X2)) -> active#(fst(mark(X1), mark(X2))))
(mark#(cons(X1, X2)) -> mark#(X1), mark#(fst(X1, X2)) -> mark#(X2))
(mark#(cons(X1, X2)) -> mark#(X1), mark#(fst(X1, X2)) -> mark#(X1))
(mark#(fst(X1, X2)) -> active#(fst(mark(X1), mark(X2))), active#(fst(s(X), cons(Y, Z))) -> mark#(cons(Y, fst(X, Z))))
(active#(fst(s(X), cons(Y, Z))) -> mark#(cons(Y, fst(X, Z))), mark#(fst(X1, X2)) -> mark#(X1))
(active#(fst(s(X), cons(Y, Z))) -> mark#(cons(Y, fst(X, Z))), mark#(fst(X1, X2)) -> mark#(X2))
(active#(fst(s(X), cons(Y, Z))) -> mark#(cons(Y, fst(X, Z))), mark#(fst(X1, X2)) -> active#(fst(mark(X1), mark(X2))))
(active#(fst(s(X), cons(Y, Z))) -> mark#(cons(Y, fst(X, Z))), mark#(cons(X1, X2)) -> mark#(X1))
(mark#(fst(X1, X2)) -> mark#(X2), mark#(fst(X1, X2)) -> mark#(X1))
(mark#(fst(X1, X2)) -> mark#(X2), mark#(fst(X1, X2)) -> mark#(X2))
(mark#(fst(X1, X2)) -> mark#(X2), mark#(fst(X1, X2)) -> active#(fst(mark(X1), mark(X2))))
(mark#(fst(X1, X2)) -> mark#(X2), mark#(cons(X1, X2)) -> mark#(X1))
(mark#(fst(X1, X2)) -> mark#(X1), mark#(fst(X1, X2)) -> mark#(X1))
(mark#(fst(X1, X2)) -> mark#(X1), mark#(fst(X1, X2)) -> mark#(X2))
(mark#(fst(X1, X2)) -> mark#(X1), mark#(fst(X1, X2)) -> active#(fst(mark(X1), mark(X2))))
(mark#(fst(X1, X2)) -> mark#(X1), mark#(cons(X1, X2)) -> mark#(X1))}
SCCS:
Scc:
{ mark#(fst(X1, X2)) -> mark#(X1),
mark#(fst(X1, X2)) -> mark#(X2),
mark#(fst(X1, X2)) -> active#(fst(mark(X1), mark(X2))),
mark#(cons(X1, X2)) -> mark#(X1),
active#(fst(s(X), cons(Y, Z))) -> mark#(cons(Y, fst(X, Z)))}
SCC:
Strict:
{ mark#(fst(X1, X2)) -> mark#(X1),
mark#(fst(X1, X2)) -> mark#(X2),
mark#(fst(X1, X2)) -> active#(fst(mark(X1), mark(X2))),
mark#(cons(X1, X2)) -> mark#(X1),
active#(fst(s(X), cons(Y, Z))) -> mark#(cons(Y, fst(X, Z)))}
Weak:
{ mark(nil()) -> active(nil()),
mark(fst(X1, X2)) -> active(fst(mark(X1), mark(X2))),
mark(0()) -> active(0()),
mark(cons(X1, X2)) -> active(cons(mark(X1), X2)),
mark(s(X)) -> active(s(X)),
mark(from(X)) -> active(from(mark(X))),
mark(add(X1, X2)) -> active(add(mark(X1), mark(X2))),
mark(len(X)) -> active(len(mark(X))),
active(fst(0(), Z)) -> mark(nil()),
active(fst(s(X), cons(Y, Z))) -> mark(cons(Y, fst(X, Z))),
active(from(X)) -> mark(cons(X, from(s(X)))),
active(add(0(), X)) -> mark(X),
active(add(s(X), Y)) -> mark(s(add(X, Y))),
active(len(nil())) -> mark(0()),
active(len(cons(X, Z))) -> mark(s(len(Z))),
fst(X1, mark(X2)) -> fst(X1, X2),
fst(X1, active(X2)) -> fst(X1, X2),
fst(mark(X1), X2) -> fst(X1, X2),
fst(active(X1), X2) -> fst(X1, X2),
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),
from(mark(X)) -> from(X),
from(active(X)) -> from(X),
add(X1, mark(X2)) -> add(X1, X2),
add(X1, active(X2)) -> add(X1, X2),
add(mark(X1), X2) -> add(X1, X2),
add(active(X1), X2) -> add(X1, X2),
len(mark(X)) -> len(X),
len(active(X)) -> len(X)}
POLY:
Argument Filtering:
pi(len) = [], pi(add) = [0,1], pi(from) = 0, pi(s) = [], pi(cons) = 0, pi(0) = [], pi(fst) = [0,1], pi(active#) = 0, pi(active) = 0, pi(nil) = [], pi(mark#) = 0, pi(mark) = 0
Usable Rules:
{}
Interpretation:
[fst](x0, x1) = x0 + x1,
[s] = 1
Strict:
{ mark#(fst(X1, X2)) -> mark#(X1),
mark#(fst(X1, X2)) -> mark#(X2),
mark#(fst(X1, X2)) -> active#(fst(mark(X1), mark(X2))),
mark#(cons(X1, X2)) -> mark#(X1)}
Weak:
{ mark(nil()) -> active(nil()),
mark(fst(X1, X2)) -> active(fst(mark(X1), mark(X2))),
mark(0()) -> active(0()),
mark(cons(X1, X2)) -> active(cons(mark(X1), X2)),
mark(s(X)) -> active(s(X)),
mark(from(X)) -> active(from(mark(X))),
mark(add(X1, X2)) -> active(add(mark(X1), mark(X2))),
mark(len(X)) -> active(len(mark(X))),
active(fst(0(), Z)) -> mark(nil()),
active(fst(s(X), cons(Y, Z))) -> mark(cons(Y, fst(X, Z))),
active(from(X)) -> mark(cons(X, from(s(X)))),
active(add(0(), X)) -> mark(X),
active(add(s(X), Y)) -> mark(s(add(X, Y))),
active(len(nil())) -> mark(0()),
active(len(cons(X, Z))) -> mark(s(len(Z))),
fst(X1, mark(X2)) -> fst(X1, X2),
fst(X1, active(X2)) -> fst(X1, X2),
fst(mark(X1), X2) -> fst(X1, X2),
fst(active(X1), X2) -> fst(X1, X2),
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),
from(mark(X)) -> from(X),
from(active(X)) -> from(X),
add(X1, mark(X2)) -> add(X1, X2),
add(X1, active(X2)) -> add(X1, X2),
add(mark(X1), X2) -> add(X1, X2),
add(active(X1), X2) -> add(X1, X2),
len(mark(X)) -> len(X),
len(active(X)) -> len(X)}
EDG:
{(mark#(cons(X1, X2)) -> mark#(X1), mark#(cons(X1, X2)) -> mark#(X1))
(mark#(cons(X1, X2)) -> mark#(X1), mark#(fst(X1, X2)) -> active#(fst(mark(X1), mark(X2))))
(mark#(cons(X1, X2)) -> mark#(X1), mark#(fst(X1, X2)) -> mark#(X2))
(mark#(cons(X1, X2)) -> mark#(X1), mark#(fst(X1, X2)) -> mark#(X1))
(mark#(fst(X1, X2)) -> mark#(X1), mark#(fst(X1, X2)) -> mark#(X1))
(mark#(fst(X1, X2)) -> mark#(X1), mark#(fst(X1, X2)) -> mark#(X2))
(mark#(fst(X1, X2)) -> mark#(X1), mark#(fst(X1, X2)) -> active#(fst(mark(X1), mark(X2))))
(mark#(fst(X1, X2)) -> mark#(X1), mark#(cons(X1, X2)) -> mark#(X1))
(mark#(fst(X1, X2)) -> mark#(X2), mark#(fst(X1, X2)) -> mark#(X1))
(mark#(fst(X1, X2)) -> mark#(X2), mark#(fst(X1, X2)) -> mark#(X2))
(mark#(fst(X1, X2)) -> mark#(X2), mark#(fst(X1, X2)) -> active#(fst(mark(X1), mark(X2))))
(mark#(fst(X1, X2)) -> mark#(X2), mark#(cons(X1, X2)) -> mark#(X1))}
SCCS:
Scc:
{ mark#(fst(X1, X2)) -> mark#(X1),
mark#(fst(X1, X2)) -> mark#(X2),
mark#(cons(X1, X2)) -> mark#(X1)}
SCC:
Strict:
{ mark#(fst(X1, X2)) -> mark#(X1),
mark#(fst(X1, X2)) -> mark#(X2),
mark#(cons(X1, X2)) -> mark#(X1)}
Weak:
{ mark(nil()) -> active(nil()),
mark(fst(X1, X2)) -> active(fst(mark(X1), mark(X2))),
mark(0()) -> active(0()),
mark(cons(X1, X2)) -> active(cons(mark(X1), X2)),
mark(s(X)) -> active(s(X)),
mark(from(X)) -> active(from(mark(X))),
mark(add(X1, X2)) -> active(add(mark(X1), mark(X2))),
mark(len(X)) -> active(len(mark(X))),
active(fst(0(), Z)) -> mark(nil()),
active(fst(s(X), cons(Y, Z))) -> mark(cons(Y, fst(X, Z))),
active(from(X)) -> mark(cons(X, from(s(X)))),
active(add(0(), X)) -> mark(X),
active(add(s(X), Y)) -> mark(s(add(X, Y))),
active(len(nil())) -> mark(0()),
active(len(cons(X, Z))) -> mark(s(len(Z))),
fst(X1, mark(X2)) -> fst(X1, X2),
fst(X1, active(X2)) -> fst(X1, X2),
fst(mark(X1), X2) -> fst(X1, X2),
fst(active(X1), X2) -> fst(X1, X2),
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),
from(mark(X)) -> from(X),
from(active(X)) -> from(X),
add(X1, mark(X2)) -> add(X1, X2),
add(X1, active(X2)) -> add(X1, X2),
add(mark(X1), X2) -> add(X1, X2),
add(active(X1), X2) -> add(X1, X2),
len(mark(X)) -> len(X),
len(active(X)) -> len(X)}
SPSC:
Simple Projection:
pi(mark#) = 0
Strict:
{ mark#(fst(X1, X2)) -> mark#(X1),
mark#(cons(X1, X2)) -> mark#(X1)}
EDG:
{(mark#(cons(X1, X2)) -> mark#(X1), mark#(cons(X1, X2)) -> mark#(X1))
(mark#(cons(X1, X2)) -> mark#(X1), mark#(fst(X1, X2)) -> mark#(X1))
(mark#(fst(X1, X2)) -> mark#(X1), mark#(fst(X1, X2)) -> mark#(X1))
(mark#(fst(X1, X2)) -> mark#(X1), mark#(cons(X1, X2)) -> mark#(X1))}
SCCS:
Scc:
{ mark#(fst(X1, X2)) -> mark#(X1),
mark#(cons(X1, X2)) -> mark#(X1)}
SCC:
Strict:
{ mark#(fst(X1, X2)) -> mark#(X1),
mark#(cons(X1, X2)) -> mark#(X1)}
Weak:
{ mark(nil()) -> active(nil()),
mark(fst(X1, X2)) -> active(fst(mark(X1), mark(X2))),
mark(0()) -> active(0()),
mark(cons(X1, X2)) -> active(cons(mark(X1), X2)),
mark(s(X)) -> active(s(X)),
mark(from(X)) -> active(from(mark(X))),
mark(add(X1, X2)) -> active(add(mark(X1), mark(X2))),
mark(len(X)) -> active(len(mark(X))),
active(fst(0(), Z)) -> mark(nil()),
active(fst(s(X), cons(Y, Z))) -> mark(cons(Y, fst(X, Z))),
active(from(X)) -> mark(cons(X, from(s(X)))),
active(add(0(), X)) -> mark(X),
active(add(s(X), Y)) -> mark(s(add(X, Y))),
active(len(nil())) -> mark(0()),
active(len(cons(X, Z))) -> mark(s(len(Z))),
fst(X1, mark(X2)) -> fst(X1, X2),
fst(X1, active(X2)) -> fst(X1, X2),
fst(mark(X1), X2) -> fst(X1, X2),
fst(active(X1), X2) -> fst(X1, X2),
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),
from(mark(X)) -> from(X),
from(active(X)) -> from(X),
add(X1, mark(X2)) -> add(X1, X2),
add(X1, active(X2)) -> add(X1, X2),
add(mark(X1), X2) -> add(X1, X2),
add(active(X1), X2) -> add(X1, X2),
len(mark(X)) -> len(X),
len(active(X)) -> len(X)}
SPSC:
Simple Projection:
pi(mark#) = 0
Strict:
{mark#(cons(X1, X2)) -> mark#(X1)}
EDG:
{(mark#(cons(X1, X2)) -> mark#(X1), mark#(cons(X1, X2)) -> mark#(X1))}
SCCS:
Scc:
{mark#(cons(X1, X2)) -> mark#(X1)}
SCC:
Strict:
{mark#(cons(X1, X2)) -> mark#(X1)}
Weak:
{ mark(nil()) -> active(nil()),
mark(fst(X1, X2)) -> active(fst(mark(X1), mark(X2))),
mark(0()) -> active(0()),
mark(cons(X1, X2)) -> active(cons(mark(X1), X2)),
mark(s(X)) -> active(s(X)),
mark(from(X)) -> active(from(mark(X))),
mark(add(X1, X2)) -> active(add(mark(X1), mark(X2))),
mark(len(X)) -> active(len(mark(X))),
active(fst(0(), Z)) -> mark(nil()),
active(fst(s(X), cons(Y, Z))) -> mark(cons(Y, fst(X, Z))),
active(from(X)) -> mark(cons(X, from(s(X)))),
active(add(0(), X)) -> mark(X),
active(add(s(X), Y)) -> mark(s(add(X, Y))),
active(len(nil())) -> mark(0()),
active(len(cons(X, Z))) -> mark(s(len(Z))),
fst(X1, mark(X2)) -> fst(X1, X2),
fst(X1, active(X2)) -> fst(X1, X2),
fst(mark(X1), X2) -> fst(X1, X2),
fst(active(X1), X2) -> fst(X1, X2),
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),
from(mark(X)) -> from(X),
from(active(X)) -> from(X),
add(X1, mark(X2)) -> add(X1, X2),
add(X1, active(X2)) -> add(X1, X2),
add(mark(X1), X2) -> add(X1, X2),
add(active(X1), X2) -> add(X1, X2),
len(mark(X)) -> len(X),
len(active(X)) -> len(X)}
SPSC:
Simple Projection:
pi(mark#) = 0
Strict:
{}
Qed