MAYBE TRS: { mark(cons(X1, X2)) -> active(cons(mark(X1), X2)), mark(0()) -> active(0()), mark(incr(X)) -> active(incr(mark(X))), mark(nats()) -> active(nats()), mark(odds()) -> active(odds()), mark(pairs()) -> active(pairs()), mark(s(X)) -> active(s(mark(X))), mark(head(X)) -> active(head(mark(X))), mark(tail(X)) -> active(tail(mark(X))), 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), incr(mark(X)) -> incr(X), incr(active(X)) -> incr(X), active(incr(cons(X, XS))) -> mark(cons(s(X), incr(XS))), active(nats()) -> mark(cons(0(), incr(nats()))), active(odds()) -> mark(incr(pairs())), active(pairs()) -> mark(cons(0(), incr(odds()))), active(head(cons(X, XS))) -> mark(X), active(tail(cons(X, XS))) -> mark(XS), s(mark(X)) -> s(X), s(active(X)) -> s(X), head(mark(X)) -> head(X), head(active(X)) -> head(X), tail(mark(X)) -> tail(X), tail(active(X)) -> tail(X)} DP: Strict: { mark#(cons(X1, X2)) -> mark#(X1), mark#(cons(X1, X2)) -> cons#(mark(X1), X2), mark#(cons(X1, X2)) -> active#(cons(mark(X1), X2)), mark#(0()) -> active#(0()), mark#(incr(X)) -> mark#(X), mark#(incr(X)) -> incr#(mark(X)), mark#(incr(X)) -> active#(incr(mark(X))), mark#(nats()) -> active#(nats()), mark#(odds()) -> active#(odds()), mark#(pairs()) -> active#(pairs()), mark#(s(X)) -> mark#(X), mark#(s(X)) -> active#(s(mark(X))), mark#(s(X)) -> s#(mark(X)), mark#(head(X)) -> mark#(X), mark#(head(X)) -> active#(head(mark(X))), mark#(head(X)) -> head#(mark(X)), mark#(tail(X)) -> mark#(X), mark#(tail(X)) -> active#(tail(mark(X))), mark#(tail(X)) -> tail#(mark(X)), 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), incr#(mark(X)) -> incr#(X), incr#(active(X)) -> incr#(X), active#(incr(cons(X, XS))) -> mark#(cons(s(X), incr(XS))), active#(incr(cons(X, XS))) -> cons#(s(X), incr(XS)), active#(incr(cons(X, XS))) -> incr#(XS), active#(incr(cons(X, XS))) -> s#(X), active#(nats()) -> mark#(cons(0(), incr(nats()))), active#(nats()) -> cons#(0(), incr(nats())), active#(nats()) -> incr#(nats()), active#(odds()) -> mark#(incr(pairs())), active#(odds()) -> incr#(pairs()), active#(pairs()) -> mark#(cons(0(), incr(odds()))), active#(pairs()) -> cons#(0(), incr(odds())), active#(pairs()) -> incr#(odds()), active#(head(cons(X, XS))) -> mark#(X), active#(tail(cons(X, XS))) -> mark#(XS), s#(mark(X)) -> s#(X), s#(active(X)) -> s#(X), head#(mark(X)) -> head#(X), head#(active(X)) -> head#(X), tail#(mark(X)) -> tail#(X), tail#(active(X)) -> tail#(X)} Weak: { mark(cons(X1, X2)) -> active(cons(mark(X1), X2)), mark(0()) -> active(0()), mark(incr(X)) -> active(incr(mark(X))), mark(nats()) -> active(nats()), mark(odds()) -> active(odds()), mark(pairs()) -> active(pairs()), mark(s(X)) -> active(s(mark(X))), mark(head(X)) -> active(head(mark(X))), mark(tail(X)) -> active(tail(mark(X))), 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), incr(mark(X)) -> incr(X), incr(active(X)) -> incr(X), active(incr(cons(X, XS))) -> mark(cons(s(X), incr(XS))), active(nats()) -> mark(cons(0(), incr(nats()))), active(odds()) -> mark(incr(pairs())), active(pairs()) -> mark(cons(0(), incr(odds()))), active(head(cons(X, XS))) -> mark(X), active(tail(cons(X, XS))) -> mark(XS), s(mark(X)) -> s(X), s(active(X)) -> s(X), head(mark(X)) -> head(X), head(active(X)) -> head(X), tail(mark(X)) -> tail(X), tail(active(X)) -> tail(X)} EDG: { (mark#(incr(X)) -> active#(incr(mark(X))), active#(tail(cons(X, XS))) -> mark#(XS)) (mark#(incr(X)) -> active#(incr(mark(X))), active#(head(cons(X, XS))) -> mark#(X)) (mark#(incr(X)) -> active#(incr(mark(X))), active#(incr(cons(X, XS))) -> s#(X)) (mark#(incr(X)) -> active#(incr(mark(X))), active#(incr(cons(X, XS))) -> incr#(XS)) (mark#(incr(X)) -> active#(incr(mark(X))), active#(incr(cons(X, XS))) -> cons#(s(X), incr(XS))) (mark#(incr(X)) -> active#(incr(mark(X))), active#(incr(cons(X, XS))) -> mark#(cons(s(X), incr(XS)))) (mark#(head(X)) -> active#(head(mark(X))), active#(tail(cons(X, XS))) -> mark#(XS)) (mark#(head(X)) -> active#(head(mark(X))), active#(head(cons(X, XS))) -> mark#(X)) (mark#(head(X)) -> active#(head(mark(X))), active#(incr(cons(X, XS))) -> s#(X)) (mark#(head(X)) -> active#(head(mark(X))), active#(incr(cons(X, XS))) -> incr#(XS)) (mark#(head(X)) -> active#(head(mark(X))), active#(incr(cons(X, XS))) -> cons#(s(X), incr(XS))) (mark#(head(X)) -> active#(head(mark(X))), active#(incr(cons(X, XS))) -> mark#(cons(s(X), incr(XS)))) (mark#(incr(X)) -> mark#(X), mark#(tail(X)) -> tail#(mark(X))) (mark#(incr(X)) -> mark#(X), mark#(tail(X)) -> active#(tail(mark(X)))) (mark#(incr(X)) -> mark#(X), mark#(tail(X)) -> mark#(X)) (mark#(incr(X)) -> mark#(X), mark#(head(X)) -> head#(mark(X))) (mark#(incr(X)) -> mark#(X), mark#(head(X)) -> active#(head(mark(X)))) (mark#(incr(X)) -> mark#(X), mark#(head(X)) -> mark#(X)) (mark#(incr(X)) -> mark#(X), mark#(s(X)) -> s#(mark(X))) (mark#(incr(X)) -> mark#(X), mark#(s(X)) -> active#(s(mark(X)))) (mark#(incr(X)) -> mark#(X), mark#(s(X)) -> mark#(X)) (mark#(incr(X)) -> mark#(X), mark#(pairs()) -> active#(pairs())) (mark#(incr(X)) -> mark#(X), mark#(odds()) -> active#(odds())) (mark#(incr(X)) -> mark#(X), mark#(nats()) -> active#(nats())) (mark#(incr(X)) -> mark#(X), mark#(incr(X)) -> active#(incr(mark(X)))) (mark#(incr(X)) -> mark#(X), mark#(incr(X)) -> incr#(mark(X))) (mark#(incr(X)) -> mark#(X), mark#(incr(X)) -> mark#(X)) (mark#(incr(X)) -> mark#(X), mark#(0()) -> active#(0())) (mark#(incr(X)) -> mark#(X), mark#(cons(X1, X2)) -> active#(cons(mark(X1), X2))) (mark#(incr(X)) -> mark#(X), mark#(cons(X1, X2)) -> cons#(mark(X1), X2)) (mark#(incr(X)) -> mark#(X), mark#(cons(X1, X2)) -> mark#(X1)) (mark#(head(X)) -> mark#(X), mark#(tail(X)) -> tail#(mark(X))) (mark#(head(X)) -> mark#(X), mark#(tail(X)) -> active#(tail(mark(X)))) (mark#(head(X)) -> mark#(X), mark#(tail(X)) -> mark#(X)) (mark#(head(X)) -> mark#(X), mark#(head(X)) -> head#(mark(X))) (mark#(head(X)) -> mark#(X), mark#(head(X)) -> active#(head(mark(X)))) (mark#(head(X)) -> mark#(X), mark#(head(X)) -> mark#(X)) (mark#(head(X)) -> mark#(X), mark#(s(X)) -> s#(mark(X))) (mark#(head(X)) -> mark#(X), mark#(s(X)) -> active#(s(mark(X)))) (mark#(head(X)) -> mark#(X), mark#(s(X)) -> mark#(X)) (mark#(head(X)) -> mark#(X), mark#(pairs()) -> active#(pairs())) (mark#(head(X)) -> mark#(X), mark#(odds()) -> active#(odds())) (mark#(head(X)) -> mark#(X), mark#(nats()) -> active#(nats())) (mark#(head(X)) -> mark#(X), mark#(incr(X)) -> active#(incr(mark(X)))) (mark#(head(X)) -> mark#(X), mark#(incr(X)) -> incr#(mark(X))) (mark#(head(X)) -> mark#(X), mark#(incr(X)) -> mark#(X)) (mark#(head(X)) -> mark#(X), mark#(0()) -> active#(0())) (mark#(head(X)) -> mark#(X), mark#(cons(X1, X2)) -> active#(cons(mark(X1), X2))) (mark#(head(X)) -> mark#(X), mark#(cons(X1, X2)) -> cons#(mark(X1), X2)) (mark#(head(X)) -> mark#(X), mark#(cons(X1, X2)) -> mark#(X1)) (incr#(mark(X)) -> incr#(X), incr#(active(X)) -> incr#(X)) (incr#(mark(X)) -> incr#(X), incr#(mark(X)) -> incr#(X)) (active#(incr(cons(X, XS))) -> s#(X), s#(active(X)) -> s#(X)) (active#(incr(cons(X, XS))) -> 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)) (head#(mark(X)) -> head#(X), head#(active(X)) -> head#(X)) (head#(mark(X)) -> head#(X), head#(mark(X)) -> head#(X)) (tail#(mark(X)) -> tail#(X), tail#(active(X)) -> tail#(X)) (tail#(mark(X)) -> tail#(X), tail#(mark(X)) -> tail#(X)) (mark#(odds()) -> active#(odds()), active#(odds()) -> incr#(pairs())) (mark#(odds()) -> active#(odds()), active#(odds()) -> mark#(incr(pairs()))) (active#(tail(cons(X, XS))) -> mark#(XS), mark#(tail(X)) -> tail#(mark(X))) (active#(tail(cons(X, XS))) -> mark#(XS), mark#(tail(X)) -> active#(tail(mark(X)))) (active#(tail(cons(X, XS))) -> mark#(XS), mark#(tail(X)) -> mark#(X)) (active#(tail(cons(X, XS))) -> mark#(XS), mark#(head(X)) -> head#(mark(X))) (active#(tail(cons(X, XS))) -> mark#(XS), mark#(head(X)) -> active#(head(mark(X)))) (active#(tail(cons(X, XS))) -> mark#(XS), mark#(head(X)) -> mark#(X)) (active#(tail(cons(X, XS))) -> mark#(XS), mark#(s(X)) -> s#(mark(X))) (active#(tail(cons(X, XS))) -> mark#(XS), mark#(s(X)) -> active#(s(mark(X)))) (active#(tail(cons(X, XS))) -> mark#(XS), mark#(s(X)) -> mark#(X)) (active#(tail(cons(X, XS))) -> mark#(XS), mark#(pairs()) -> active#(pairs())) (active#(tail(cons(X, XS))) -> mark#(XS), mark#(odds()) -> active#(odds())) (active#(tail(cons(X, XS))) -> mark#(XS), mark#(nats()) -> active#(nats())) (active#(tail(cons(X, XS))) -> mark#(XS), mark#(incr(X)) -> active#(incr(mark(X)))) (active#(tail(cons(X, XS))) -> mark#(XS), mark#(incr(X)) -> incr#(mark(X))) (active#(tail(cons(X, XS))) -> mark#(XS), mark#(incr(X)) -> mark#(X)) (active#(tail(cons(X, XS))) -> mark#(XS), mark#(0()) -> active#(0())) (active#(tail(cons(X, XS))) -> mark#(XS), mark#(cons(X1, X2)) -> active#(cons(mark(X1), X2))) (active#(tail(cons(X, XS))) -> mark#(XS), mark#(cons(X1, X2)) -> cons#(mark(X1), X2)) (active#(tail(cons(X, XS))) -> mark#(XS), mark#(cons(X1, X2)) -> mark#(X1)) (active#(nats()) -> mark#(cons(0(), incr(nats()))), mark#(cons(X1, X2)) -> active#(cons(mark(X1), X2))) (active#(nats()) -> mark#(cons(0(), incr(nats()))), mark#(cons(X1, X2)) -> cons#(mark(X1), X2)) (active#(nats()) -> mark#(cons(0(), incr(nats()))), mark#(cons(X1, X2)) -> mark#(X1)) (mark#(cons(X1, X2)) -> mark#(X1), mark#(tail(X)) -> tail#(mark(X))) (mark#(cons(X1, X2)) -> mark#(X1), mark#(tail(X)) -> active#(tail(mark(X)))) (mark#(cons(X1, X2)) -> mark#(X1), mark#(tail(X)) -> mark#(X)) (mark#(cons(X1, X2)) -> mark#(X1), mark#(head(X)) -> head#(mark(X))) (mark#(cons(X1, X2)) -> mark#(X1), mark#(head(X)) -> active#(head(mark(X)))) (mark#(cons(X1, X2)) -> mark#(X1), mark#(head(X)) -> mark#(X)) (mark#(cons(X1, X2)) -> mark#(X1), mark#(s(X)) -> s#(mark(X))) (mark#(cons(X1, X2)) -> mark#(X1), mark#(s(X)) -> active#(s(mark(X)))) (mark#(cons(X1, X2)) -> mark#(X1), mark#(s(X)) -> mark#(X)) (mark#(cons(X1, X2)) -> mark#(X1), mark#(pairs()) -> active#(pairs())) (mark#(cons(X1, X2)) -> mark#(X1), mark#(odds()) -> active#(odds())) (mark#(cons(X1, X2)) -> mark#(X1), mark#(nats()) -> active#(nats())) (mark#(cons(X1, X2)) -> mark#(X1), mark#(incr(X)) -> active#(incr(mark(X)))) (mark#(cons(X1, X2)) -> mark#(X1), mark#(incr(X)) -> incr#(mark(X))) (mark#(cons(X1, X2)) -> mark#(X1), mark#(incr(X)) -> mark#(X)) (mark#(cons(X1, X2)) -> mark#(X1), mark#(0()) -> active#(0())) (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)) -> cons#(mark(X1), X2)) (mark#(cons(X1, X2)) -> mark#(X1), mark#(cons(X1, X2)) -> mark#(X1)) (mark#(incr(X)) -> incr#(mark(X)), incr#(active(X)) -> incr#(X)) (mark#(incr(X)) -> incr#(mark(X)), incr#(mark(X)) -> incr#(X)) (mark#(head(X)) -> head#(mark(X)), head#(active(X)) -> head#(X)) (mark#(head(X)) -> head#(mark(X)), head#(mark(X)) -> head#(X)) (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)) (cons#(X1, active(X2)) -> cons#(X1, X2), cons#(active(X1), X2) -> cons#(X1, X2)) (cons#(X1, active(X2)) -> cons#(X1, X2), cons#(mark(X1), X2) -> cons#(X1, X2)) (cons#(X1, active(X2)) -> cons#(X1, X2), cons#(X1, active(X2)) -> cons#(X1, X2)) (cons#(X1, active(X2)) -> cons#(X1, X2), cons#(X1, mark(X2)) -> cons#(X1, X2)) (cons#(active(X1), X2) -> cons#(X1, X2), cons#(active(X1), X2) -> cons#(X1, X2)) (cons#(active(X1), X2) -> cons#(X1, X2), cons#(mark(X1), X2) -> cons#(X1, X2)) (cons#(active(X1), X2) -> cons#(X1, X2), cons#(X1, active(X2)) -> cons#(X1, X2)) (cons#(active(X1), X2) -> cons#(X1, X2), cons#(X1, mark(X2)) -> cons#(X1, X2)) (mark#(cons(X1, X2)) -> active#(cons(mark(X1), X2)), active#(incr(cons(X, XS))) -> mark#(cons(s(X), incr(XS)))) (mark#(cons(X1, X2)) -> active#(cons(mark(X1), X2)), active#(incr(cons(X, XS))) -> cons#(s(X), incr(XS))) (mark#(cons(X1, X2)) -> active#(cons(mark(X1), X2)), active#(incr(cons(X, XS))) -> incr#(XS)) (mark#(cons(X1, X2)) -> active#(cons(mark(X1), X2)), active#(incr(cons(X, XS))) -> s#(X)) (mark#(cons(X1, X2)) -> active#(cons(mark(X1), X2)), active#(head(cons(X, XS))) -> mark#(X)) (mark#(cons(X1, X2)) -> active#(cons(mark(X1), X2)), active#(tail(cons(X, XS))) -> mark#(XS)) (cons#(mark(X1), X2) -> cons#(X1, X2), cons#(X1, mark(X2)) -> cons#(X1, X2)) (cons#(mark(X1), X2) -> cons#(X1, X2), cons#(X1, active(X2)) -> cons#(X1, X2)) (cons#(mark(X1), X2) -> cons#(X1, X2), cons#(mark(X1), X2) -> cons#(X1, X2)) (cons#(mark(X1), X2) -> cons#(X1, X2), cons#(active(X1), X2) -> cons#(X1, X2)) (cons#(X1, mark(X2)) -> cons#(X1, X2), cons#(X1, mark(X2)) -> cons#(X1, X2)) (cons#(X1, mark(X2)) -> cons#(X1, X2), cons#(X1, active(X2)) -> cons#(X1, X2)) (cons#(X1, mark(X2)) -> cons#(X1, X2), cons#(mark(X1), X2) -> cons#(X1, X2)) (cons#(X1, mark(X2)) -> cons#(X1, X2), cons#(active(X1), X2) -> cons#(X1, X2)) (mark#(tail(X)) -> tail#(mark(X)), tail#(mark(X)) -> tail#(X)) (mark#(tail(X)) -> tail#(mark(X)), tail#(active(X)) -> tail#(X)) (mark#(s(X)) -> s#(mark(X)), s#(mark(X)) -> s#(X)) (mark#(s(X)) -> s#(mark(X)), s#(active(X)) -> s#(X)) (active#(incr(cons(X, XS))) -> cons#(s(X), incr(XS)), cons#(X1, mark(X2)) -> cons#(X1, X2)) (active#(incr(cons(X, XS))) -> cons#(s(X), incr(XS)), cons#(X1, active(X2)) -> cons#(X1, X2)) (active#(incr(cons(X, XS))) -> cons#(s(X), incr(XS)), cons#(mark(X1), X2) -> cons#(X1, X2)) (active#(incr(cons(X, XS))) -> cons#(s(X), incr(XS)), cons#(active(X1), X2) -> cons#(X1, X2)) (active#(pairs()) -> mark#(cons(0(), incr(odds()))), mark#(cons(X1, X2)) -> mark#(X1)) (active#(pairs()) -> mark#(cons(0(), incr(odds()))), mark#(cons(X1, X2)) -> cons#(mark(X1), X2)) (active#(pairs()) -> mark#(cons(0(), incr(odds()))), mark#(cons(X1, X2)) -> active#(cons(mark(X1), X2))) (active#(incr(cons(X, XS))) -> mark#(cons(s(X), incr(XS))), mark#(cons(X1, X2)) -> mark#(X1)) (active#(incr(cons(X, XS))) -> mark#(cons(s(X), incr(XS))), mark#(cons(X1, X2)) -> cons#(mark(X1), X2)) (active#(incr(cons(X, XS))) -> mark#(cons(s(X), incr(XS))), mark#(cons(X1, X2)) -> active#(cons(mark(X1), X2))) (active#(incr(cons(X, XS))) -> mark#(cons(s(X), incr(XS))), mark#(incr(X)) -> mark#(X)) (active#(incr(cons(X, XS))) -> mark#(cons(s(X), incr(XS))), mark#(incr(X)) -> incr#(mark(X))) (active#(incr(cons(X, XS))) -> mark#(cons(s(X), incr(XS))), mark#(incr(X)) -> active#(incr(mark(X)))) (active#(incr(cons(X, XS))) -> mark#(cons(s(X), incr(XS))), mark#(s(X)) -> mark#(X)) (active#(incr(cons(X, XS))) -> mark#(cons(s(X), incr(XS))), mark#(s(X)) -> active#(s(mark(X)))) (active#(incr(cons(X, XS))) -> mark#(cons(s(X), incr(XS))), mark#(s(X)) -> s#(mark(X))) (active#(incr(cons(X, XS))) -> mark#(cons(s(X), incr(XS))), mark#(head(X)) -> mark#(X)) (active#(incr(cons(X, XS))) -> mark#(cons(s(X), incr(XS))), mark#(head(X)) -> active#(head(mark(X)))) (active#(incr(cons(X, XS))) -> mark#(cons(s(X), incr(XS))), mark#(head(X)) -> head#(mark(X))) (active#(incr(cons(X, XS))) -> mark#(cons(s(X), incr(XS))), mark#(tail(X)) -> mark#(X)) (active#(incr(cons(X, XS))) -> mark#(cons(s(X), incr(XS))), mark#(tail(X)) -> active#(tail(mark(X)))) (active#(incr(cons(X, XS))) -> mark#(cons(s(X), incr(XS))), mark#(tail(X)) -> tail#(mark(X))) (active#(incr(cons(X, XS))) -> incr#(XS), incr#(mark(X)) -> incr#(X)) (active#(incr(cons(X, XS))) -> incr#(XS), incr#(active(X)) -> incr#(X)) (mark#(pairs()) -> active#(pairs()), active#(pairs()) -> mark#(cons(0(), incr(odds())))) (mark#(pairs()) -> active#(pairs()), active#(pairs()) -> cons#(0(), incr(odds()))) (mark#(pairs()) -> active#(pairs()), active#(pairs()) -> incr#(odds())) (mark#(nats()) -> active#(nats()), active#(nats()) -> mark#(cons(0(), incr(nats())))) (mark#(nats()) -> active#(nats()), active#(nats()) -> cons#(0(), incr(nats()))) (mark#(nats()) -> active#(nats()), active#(nats()) -> incr#(nats())) (tail#(active(X)) -> tail#(X), tail#(mark(X)) -> tail#(X)) (tail#(active(X)) -> tail#(X), tail#(active(X)) -> tail#(X)) (head#(active(X)) -> head#(X), head#(mark(X)) -> head#(X)) (head#(active(X)) -> head#(X), head#(active(X)) -> head#(X)) (s#(active(X)) -> s#(X), s#(mark(X)) -> s#(X)) (s#(active(X)) -> s#(X), s#(active(X)) -> s#(X)) (active#(head(cons(X, XS))) -> mark#(X), mark#(cons(X1, X2)) -> mark#(X1)) (active#(head(cons(X, XS))) -> mark#(X), mark#(cons(X1, X2)) -> cons#(mark(X1), X2)) (active#(head(cons(X, XS))) -> mark#(X), mark#(cons(X1, X2)) -> active#(cons(mark(X1), X2))) (active#(head(cons(X, XS))) -> mark#(X), mark#(0()) -> active#(0())) (active#(head(cons(X, XS))) -> mark#(X), mark#(incr(X)) -> mark#(X)) (active#(head(cons(X, XS))) -> mark#(X), mark#(incr(X)) -> incr#(mark(X))) (active#(head(cons(X, XS))) -> mark#(X), mark#(incr(X)) -> active#(incr(mark(X)))) (active#(head(cons(X, XS))) -> mark#(X), mark#(nats()) -> active#(nats())) (active#(head(cons(X, XS))) -> mark#(X), mark#(odds()) -> active#(odds())) (active#(head(cons(X, XS))) -> mark#(X), mark#(pairs()) -> active#(pairs())) (active#(head(cons(X, XS))) -> mark#(X), mark#(s(X)) -> mark#(X)) (active#(head(cons(X, XS))) -> mark#(X), mark#(s(X)) -> active#(s(mark(X)))) (active#(head(cons(X, XS))) -> mark#(X), mark#(s(X)) -> s#(mark(X))) (active#(head(cons(X, XS))) -> mark#(X), mark#(head(X)) -> mark#(X)) (active#(head(cons(X, XS))) -> mark#(X), mark#(head(X)) -> active#(head(mark(X)))) (active#(head(cons(X, XS))) -> mark#(X), mark#(head(X)) -> head#(mark(X))) (active#(head(cons(X, XS))) -> mark#(X), mark#(tail(X)) -> mark#(X)) (active#(head(cons(X, XS))) -> mark#(X), mark#(tail(X)) -> active#(tail(mark(X)))) (active#(head(cons(X, XS))) -> mark#(X), mark#(tail(X)) -> tail#(mark(X))) (incr#(active(X)) -> incr#(X), incr#(mark(X)) -> incr#(X)) (incr#(active(X)) -> incr#(X), incr#(active(X)) -> incr#(X)) (mark#(tail(X)) -> mark#(X), mark#(cons(X1, X2)) -> mark#(X1)) (mark#(tail(X)) -> mark#(X), mark#(cons(X1, X2)) -> cons#(mark(X1), X2)) (mark#(tail(X)) -> mark#(X), mark#(cons(X1, X2)) -> active#(cons(mark(X1), X2))) (mark#(tail(X)) -> mark#(X), mark#(0()) -> active#(0())) (mark#(tail(X)) -> mark#(X), mark#(incr(X)) -> mark#(X)) (mark#(tail(X)) -> mark#(X), mark#(incr(X)) -> incr#(mark(X))) (mark#(tail(X)) -> mark#(X), mark#(incr(X)) -> active#(incr(mark(X)))) (mark#(tail(X)) -> mark#(X), mark#(nats()) -> active#(nats())) (mark#(tail(X)) -> mark#(X), mark#(odds()) -> active#(odds())) (mark#(tail(X)) -> mark#(X), mark#(pairs()) -> active#(pairs())) (mark#(tail(X)) -> mark#(X), mark#(s(X)) -> mark#(X)) (mark#(tail(X)) -> mark#(X), mark#(s(X)) -> active#(s(mark(X)))) (mark#(tail(X)) -> mark#(X), mark#(s(X)) -> s#(mark(X))) (mark#(tail(X)) -> mark#(X), mark#(head(X)) -> mark#(X)) (mark#(tail(X)) -> mark#(X), mark#(head(X)) -> active#(head(mark(X)))) (mark#(tail(X)) -> mark#(X), mark#(head(X)) -> head#(mark(X))) (mark#(tail(X)) -> mark#(X), mark#(tail(X)) -> mark#(X)) (mark#(tail(X)) -> mark#(X), mark#(tail(X)) -> active#(tail(mark(X)))) (mark#(tail(X)) -> mark#(X), mark#(tail(X)) -> tail#(mark(X))) (mark#(s(X)) -> mark#(X), mark#(cons(X1, X2)) -> mark#(X1)) (mark#(s(X)) -> mark#(X), mark#(cons(X1, X2)) -> cons#(mark(X1), X2)) (mark#(s(X)) -> mark#(X), mark#(cons(X1, X2)) -> active#(cons(mark(X1), X2))) (mark#(s(X)) -> mark#(X), mark#(0()) -> active#(0())) (mark#(s(X)) -> mark#(X), mark#(incr(X)) -> mark#(X)) (mark#(s(X)) -> mark#(X), mark#(incr(X)) -> incr#(mark(X))) (mark#(s(X)) -> mark#(X), mark#(incr(X)) -> active#(incr(mark(X)))) (mark#(s(X)) -> mark#(X), mark#(nats()) -> active#(nats())) (mark#(s(X)) -> mark#(X), mark#(odds()) -> active#(odds())) (mark#(s(X)) -> mark#(X), mark#(pairs()) -> active#(pairs())) (mark#(s(X)) -> mark#(X), mark#(s(X)) -> mark#(X)) (mark#(s(X)) -> mark#(X), mark#(s(X)) -> active#(s(mark(X)))) (mark#(s(X)) -> mark#(X), mark#(s(X)) -> s#(mark(X))) (mark#(s(X)) -> mark#(X), mark#(head(X)) -> mark#(X)) (mark#(s(X)) -> mark#(X), mark#(head(X)) -> active#(head(mark(X)))) (mark#(s(X)) -> mark#(X), mark#(head(X)) -> head#(mark(X))) (mark#(s(X)) -> mark#(X), mark#(tail(X)) -> mark#(X)) (mark#(s(X)) -> mark#(X), mark#(tail(X)) -> active#(tail(mark(X)))) (mark#(s(X)) -> mark#(X), mark#(tail(X)) -> tail#(mark(X))) (mark#(tail(X)) -> active#(tail(mark(X))), active#(incr(cons(X, XS))) -> mark#(cons(s(X), incr(XS)))) (mark#(tail(X)) -> active#(tail(mark(X))), active#(incr(cons(X, XS))) -> cons#(s(X), incr(XS))) (mark#(tail(X)) -> active#(tail(mark(X))), active#(incr(cons(X, XS))) -> incr#(XS)) (mark#(tail(X)) -> active#(tail(mark(X))), active#(incr(cons(X, XS))) -> s#(X)) (mark#(tail(X)) -> active#(tail(mark(X))), active#(head(cons(X, XS))) -> mark#(X)) (mark#(tail(X)) -> active#(tail(mark(X))), active#(tail(cons(X, XS))) -> mark#(XS)) (mark#(s(X)) -> active#(s(mark(X))), active#(incr(cons(X, XS))) -> mark#(cons(s(X), incr(XS)))) (mark#(s(X)) -> active#(s(mark(X))), active#(incr(cons(X, XS))) -> cons#(s(X), incr(XS))) (mark#(s(X)) -> active#(s(mark(X))), active#(incr(cons(X, XS))) -> incr#(XS)) (mark#(s(X)) -> active#(s(mark(X))), active#(incr(cons(X, XS))) -> s#(X)) (mark#(s(X)) -> active#(s(mark(X))), active#(head(cons(X, XS))) -> mark#(X)) (mark#(s(X)) -> active#(s(mark(X))), active#(tail(cons(X, XS))) -> mark#(XS)) (active#(odds()) -> mark#(incr(pairs())), mark#(incr(X)) -> mark#(X)) (active#(odds()) -> mark#(incr(pairs())), mark#(incr(X)) -> incr#(mark(X))) (active#(odds()) -> mark#(incr(pairs())), mark#(incr(X)) -> active#(incr(mark(X)))) } SCCS: Scc: { tail#(mark(X)) -> tail#(X), tail#(active(X)) -> tail#(X)} Scc: { head#(mark(X)) -> head#(X), head#(active(X)) -> head#(X)} Scc: { s#(mark(X)) -> s#(X), s#(active(X)) -> s#(X)} Scc: { incr#(mark(X)) -> incr#(X), incr#(active(X)) -> incr#(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: { mark#(cons(X1, X2)) -> mark#(X1), mark#(cons(X1, X2)) -> active#(cons(mark(X1), X2)), mark#(incr(X)) -> mark#(X), mark#(incr(X)) -> active#(incr(mark(X))), mark#(nats()) -> active#(nats()), mark#(odds()) -> active#(odds()), mark#(pairs()) -> active#(pairs()), mark#(s(X)) -> mark#(X), mark#(s(X)) -> active#(s(mark(X))), mark#(head(X)) -> mark#(X), mark#(head(X)) -> active#(head(mark(X))), mark#(tail(X)) -> mark#(X), mark#(tail(X)) -> active#(tail(mark(X))), active#(incr(cons(X, XS))) -> mark#(cons(s(X), incr(XS))), active#(nats()) -> mark#(cons(0(), incr(nats()))), active#(odds()) -> mark#(incr(pairs())), active#(pairs()) -> mark#(cons(0(), incr(odds()))), active#(head(cons(X, XS))) -> mark#(X), active#(tail(cons(X, XS))) -> mark#(XS)} SCC: Strict: { tail#(mark(X)) -> tail#(X), tail#(active(X)) -> tail#(X)} Weak: { mark(cons(X1, X2)) -> active(cons(mark(X1), X2)), mark(0()) -> active(0()), mark(incr(X)) -> active(incr(mark(X))), mark(nats()) -> active(nats()), mark(odds()) -> active(odds()), mark(pairs()) -> active(pairs()), mark(s(X)) -> active(s(mark(X))), mark(head(X)) -> active(head(mark(X))), mark(tail(X)) -> active(tail(mark(X))), 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), incr(mark(X)) -> incr(X), incr(active(X)) -> incr(X), active(incr(cons(X, XS))) -> mark(cons(s(X), incr(XS))), active(nats()) -> mark(cons(0(), incr(nats()))), active(odds()) -> mark(incr(pairs())), active(pairs()) -> mark(cons(0(), incr(odds()))), active(head(cons(X, XS))) -> mark(X), active(tail(cons(X, XS))) -> mark(XS), s(mark(X)) -> s(X), s(active(X)) -> s(X), head(mark(X)) -> head(X), head(active(X)) -> head(X), tail(mark(X)) -> tail(X), tail(active(X)) -> tail(X)} SPSC: Simple Projection: pi(tail#) = 0 Strict: {tail#(active(X)) -> tail#(X)} EDG: {(tail#(active(X)) -> tail#(X), tail#(active(X)) -> tail#(X))} SCCS: Scc: {tail#(active(X)) -> tail#(X)} SCC: Strict: {tail#(active(X)) -> tail#(X)} Weak: { mark(cons(X1, X2)) -> active(cons(mark(X1), X2)), mark(0()) -> active(0()), mark(incr(X)) -> active(incr(mark(X))), mark(nats()) -> active(nats()), mark(odds()) -> active(odds()), mark(pairs()) -> active(pairs()), mark(s(X)) -> active(s(mark(X))), mark(head(X)) -> active(head(mark(X))), mark(tail(X)) -> active(tail(mark(X))), 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), incr(mark(X)) -> incr(X), incr(active(X)) -> incr(X), active(incr(cons(X, XS))) -> mark(cons(s(X), incr(XS))), active(nats()) -> mark(cons(0(), incr(nats()))), active(odds()) -> mark(incr(pairs())), active(pairs()) -> mark(cons(0(), incr(odds()))), active(head(cons(X, XS))) -> mark(X), active(tail(cons(X, XS))) -> mark(XS), s(mark(X)) -> s(X), s(active(X)) -> s(X), head(mark(X)) -> head(X), head(active(X)) -> head(X), tail(mark(X)) -> tail(X), tail(active(X)) -> tail(X)} SPSC: Simple Projection: pi(tail#) = 0 Strict: {} Qed SCC: Strict: { head#(mark(X)) -> head#(X), head#(active(X)) -> head#(X)} Weak: { mark(cons(X1, X2)) -> active(cons(mark(X1), X2)), mark(0()) -> active(0()), mark(incr(X)) -> active(incr(mark(X))), mark(nats()) -> active(nats()), mark(odds()) -> active(odds()), mark(pairs()) -> active(pairs()), mark(s(X)) -> active(s(mark(X))), mark(head(X)) -> active(head(mark(X))), mark(tail(X)) -> active(tail(mark(X))), 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), incr(mark(X)) -> incr(X), incr(active(X)) -> incr(X), active(incr(cons(X, XS))) -> mark(cons(s(X), incr(XS))), active(nats()) -> mark(cons(0(), incr(nats()))), active(odds()) -> mark(incr(pairs())), active(pairs()) -> mark(cons(0(), incr(odds()))), active(head(cons(X, XS))) -> mark(X), active(tail(cons(X, XS))) -> mark(XS), s(mark(X)) -> s(X), s(active(X)) -> s(X), head(mark(X)) -> head(X), head(active(X)) -> head(X), tail(mark(X)) -> tail(X), tail(active(X)) -> tail(X)} SPSC: Simple Projection: pi(head#) = 0 Strict: {head#(active(X)) -> head#(X)} EDG: {(head#(active(X)) -> head#(X), head#(active(X)) -> head#(X))} SCCS: Scc: {head#(active(X)) -> head#(X)} SCC: Strict: {head#(active(X)) -> head#(X)} Weak: { mark(cons(X1, X2)) -> active(cons(mark(X1), X2)), mark(0()) -> active(0()), mark(incr(X)) -> active(incr(mark(X))), mark(nats()) -> active(nats()), mark(odds()) -> active(odds()), mark(pairs()) -> active(pairs()), mark(s(X)) -> active(s(mark(X))), mark(head(X)) -> active(head(mark(X))), mark(tail(X)) -> active(tail(mark(X))), 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), incr(mark(X)) -> incr(X), incr(active(X)) -> incr(X), active(incr(cons(X, XS))) -> mark(cons(s(X), incr(XS))), active(nats()) -> mark(cons(0(), incr(nats()))), active(odds()) -> mark(incr(pairs())), active(pairs()) -> mark(cons(0(), incr(odds()))), active(head(cons(X, XS))) -> mark(X), active(tail(cons(X, XS))) -> mark(XS), s(mark(X)) -> s(X), s(active(X)) -> s(X), head(mark(X)) -> head(X), head(active(X)) -> head(X), tail(mark(X)) -> tail(X), tail(active(X)) -> tail(X)} SPSC: Simple Projection: pi(head#) = 0 Strict: {} Qed SCC: Strict: { s#(mark(X)) -> s#(X), s#(active(X)) -> s#(X)} Weak: { mark(cons(X1, X2)) -> active(cons(mark(X1), X2)), mark(0()) -> active(0()), mark(incr(X)) -> active(incr(mark(X))), mark(nats()) -> active(nats()), mark(odds()) -> active(odds()), mark(pairs()) -> active(pairs()), mark(s(X)) -> active(s(mark(X))), mark(head(X)) -> active(head(mark(X))), mark(tail(X)) -> active(tail(mark(X))), 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), incr(mark(X)) -> incr(X), incr(active(X)) -> incr(X), active(incr(cons(X, XS))) -> mark(cons(s(X), incr(XS))), active(nats()) -> mark(cons(0(), incr(nats()))), active(odds()) -> mark(incr(pairs())), active(pairs()) -> mark(cons(0(), incr(odds()))), active(head(cons(X, XS))) -> mark(X), active(tail(cons(X, XS))) -> mark(XS), s(mark(X)) -> s(X), s(active(X)) -> s(X), head(mark(X)) -> head(X), head(active(X)) -> head(X), tail(mark(X)) -> tail(X), tail(active(X)) -> tail(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(cons(X1, X2)) -> active(cons(mark(X1), X2)), mark(0()) -> active(0()), mark(incr(X)) -> active(incr(mark(X))), mark(nats()) -> active(nats()), mark(odds()) -> active(odds()), mark(pairs()) -> active(pairs()), mark(s(X)) -> active(s(mark(X))), mark(head(X)) -> active(head(mark(X))), mark(tail(X)) -> active(tail(mark(X))), 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), incr(mark(X)) -> incr(X), incr(active(X)) -> incr(X), active(incr(cons(X, XS))) -> mark(cons(s(X), incr(XS))), active(nats()) -> mark(cons(0(), incr(nats()))), active(odds()) -> mark(incr(pairs())), active(pairs()) -> mark(cons(0(), incr(odds()))), active(head(cons(X, XS))) -> mark(X), active(tail(cons(X, XS))) -> mark(XS), s(mark(X)) -> s(X), s(active(X)) -> s(X), head(mark(X)) -> head(X), head(active(X)) -> head(X), tail(mark(X)) -> tail(X), tail(active(X)) -> tail(X)} SPSC: Simple Projection: pi(s#) = 0 Strict: {} Qed SCC: Strict: { incr#(mark(X)) -> incr#(X), incr#(active(X)) -> incr#(X)} Weak: { mark(cons(X1, X2)) -> active(cons(mark(X1), X2)), mark(0()) -> active(0()), mark(incr(X)) -> active(incr(mark(X))), mark(nats()) -> active(nats()), mark(odds()) -> active(odds()), mark(pairs()) -> active(pairs()), mark(s(X)) -> active(s(mark(X))), mark(head(X)) -> active(head(mark(X))), mark(tail(X)) -> active(tail(mark(X))), 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), incr(mark(X)) -> incr(X), incr(active(X)) -> incr(X), active(incr(cons(X, XS))) -> mark(cons(s(X), incr(XS))), active(nats()) -> mark(cons(0(), incr(nats()))), active(odds()) -> mark(incr(pairs())), active(pairs()) -> mark(cons(0(), incr(odds()))), active(head(cons(X, XS))) -> mark(X), active(tail(cons(X, XS))) -> mark(XS), s(mark(X)) -> s(X), s(active(X)) -> s(X), head(mark(X)) -> head(X), head(active(X)) -> head(X), tail(mark(X)) -> tail(X), tail(active(X)) -> tail(X)} SPSC: Simple Projection: pi(incr#) = 0 Strict: {incr#(active(X)) -> incr#(X)} EDG: {(incr#(active(X)) -> incr#(X), incr#(active(X)) -> incr#(X))} SCCS: Scc: {incr#(active(X)) -> incr#(X)} SCC: Strict: {incr#(active(X)) -> incr#(X)} Weak: { mark(cons(X1, X2)) -> active(cons(mark(X1), X2)), mark(0()) -> active(0()), mark(incr(X)) -> active(incr(mark(X))), mark(nats()) -> active(nats()), mark(odds()) -> active(odds()), mark(pairs()) -> active(pairs()), mark(s(X)) -> active(s(mark(X))), mark(head(X)) -> active(head(mark(X))), mark(tail(X)) -> active(tail(mark(X))), 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), incr(mark(X)) -> incr(X), incr(active(X)) -> incr(X), active(incr(cons(X, XS))) -> mark(cons(s(X), incr(XS))), active(nats()) -> mark(cons(0(), incr(nats()))), active(odds()) -> mark(incr(pairs())), active(pairs()) -> mark(cons(0(), incr(odds()))), active(head(cons(X, XS))) -> mark(X), active(tail(cons(X, XS))) -> mark(XS), s(mark(X)) -> s(X), s(active(X)) -> s(X), head(mark(X)) -> head(X), head(active(X)) -> head(X), tail(mark(X)) -> tail(X), tail(active(X)) -> tail(X)} SPSC: Simple Projection: pi(incr#) = 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(cons(X1, X2)) -> active(cons(mark(X1), X2)), mark(0()) -> active(0()), mark(incr(X)) -> active(incr(mark(X))), mark(nats()) -> active(nats()), mark(odds()) -> active(odds()), mark(pairs()) -> active(pairs()), mark(s(X)) -> active(s(mark(X))), mark(head(X)) -> active(head(mark(X))), mark(tail(X)) -> active(tail(mark(X))), 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), incr(mark(X)) -> incr(X), incr(active(X)) -> incr(X), active(incr(cons(X, XS))) -> mark(cons(s(X), incr(XS))), active(nats()) -> mark(cons(0(), incr(nats()))), active(odds()) -> mark(incr(pairs())), active(pairs()) -> mark(cons(0(), incr(odds()))), active(head(cons(X, XS))) -> mark(X), active(tail(cons(X, XS))) -> mark(XS), s(mark(X)) -> s(X), s(active(X)) -> s(X), head(mark(X)) -> head(X), head(active(X)) -> head(X), tail(mark(X)) -> tail(X), tail(active(X)) -> tail(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(cons(X1, X2)) -> active(cons(mark(X1), X2)), mark(0()) -> active(0()), mark(incr(X)) -> active(incr(mark(X))), mark(nats()) -> active(nats()), mark(odds()) -> active(odds()), mark(pairs()) -> active(pairs()), mark(s(X)) -> active(s(mark(X))), mark(head(X)) -> active(head(mark(X))), mark(tail(X)) -> active(tail(mark(X))), 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), incr(mark(X)) -> incr(X), incr(active(X)) -> incr(X), active(incr(cons(X, XS))) -> mark(cons(s(X), incr(XS))), active(nats()) -> mark(cons(0(), incr(nats()))), active(odds()) -> mark(incr(pairs())), active(pairs()) -> mark(cons(0(), incr(odds()))), active(head(cons(X, XS))) -> mark(X), active(tail(cons(X, XS))) -> mark(XS), s(mark(X)) -> s(X), s(active(X)) -> s(X), head(mark(X)) -> head(X), head(active(X)) -> head(X), tail(mark(X)) -> tail(X), tail(active(X)) -> tail(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(cons(X1, X2)) -> active(cons(mark(X1), X2)), mark(0()) -> active(0()), mark(incr(X)) -> active(incr(mark(X))), mark(nats()) -> active(nats()), mark(odds()) -> active(odds()), mark(pairs()) -> active(pairs()), mark(s(X)) -> active(s(mark(X))), mark(head(X)) -> active(head(mark(X))), mark(tail(X)) -> active(tail(mark(X))), 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), incr(mark(X)) -> incr(X), incr(active(X)) -> incr(X), active(incr(cons(X, XS))) -> mark(cons(s(X), incr(XS))), active(nats()) -> mark(cons(0(), incr(nats()))), active(odds()) -> mark(incr(pairs())), active(pairs()) -> mark(cons(0(), incr(odds()))), active(head(cons(X, XS))) -> mark(X), active(tail(cons(X, XS))) -> mark(XS), s(mark(X)) -> s(X), s(active(X)) -> s(X), head(mark(X)) -> head(X), head(active(X)) -> head(X), tail(mark(X)) -> tail(X), tail(active(X)) -> tail(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(cons(X1, X2)) -> active(cons(mark(X1), X2)), mark(0()) -> active(0()), mark(incr(X)) -> active(incr(mark(X))), mark(nats()) -> active(nats()), mark(odds()) -> active(odds()), mark(pairs()) -> active(pairs()), mark(s(X)) -> active(s(mark(X))), mark(head(X)) -> active(head(mark(X))), mark(tail(X)) -> active(tail(mark(X))), 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), incr(mark(X)) -> incr(X), incr(active(X)) -> incr(X), active(incr(cons(X, XS))) -> mark(cons(s(X), incr(XS))), active(nats()) -> mark(cons(0(), incr(nats()))), active(odds()) -> mark(incr(pairs())), active(pairs()) -> mark(cons(0(), incr(odds()))), active(head(cons(X, XS))) -> mark(X), active(tail(cons(X, XS))) -> mark(XS), s(mark(X)) -> s(X), s(active(X)) -> s(X), head(mark(X)) -> head(X), head(active(X)) -> head(X), tail(mark(X)) -> tail(X), tail(active(X)) -> tail(X)} SPSC: Simple Projection: pi(cons#) = 1 Strict: {} Qed SCC: Strict: { mark#(cons(X1, X2)) -> mark#(X1), mark#(cons(X1, X2)) -> active#(cons(mark(X1), X2)), mark#(incr(X)) -> mark#(X), mark#(incr(X)) -> active#(incr(mark(X))), mark#(nats()) -> active#(nats()), mark#(odds()) -> active#(odds()), mark#(pairs()) -> active#(pairs()), mark#(s(X)) -> mark#(X), mark#(s(X)) -> active#(s(mark(X))), mark#(head(X)) -> mark#(X), mark#(head(X)) -> active#(head(mark(X))), mark#(tail(X)) -> mark#(X), mark#(tail(X)) -> active#(tail(mark(X))), active#(incr(cons(X, XS))) -> mark#(cons(s(X), incr(XS))), active#(nats()) -> mark#(cons(0(), incr(nats()))), active#(odds()) -> mark#(incr(pairs())), active#(pairs()) -> mark#(cons(0(), incr(odds()))), active#(head(cons(X, XS))) -> mark#(X), active#(tail(cons(X, XS))) -> mark#(XS)} Weak: { mark(cons(X1, X2)) -> active(cons(mark(X1), X2)), mark(0()) -> active(0()), mark(incr(X)) -> active(incr(mark(X))), mark(nats()) -> active(nats()), mark(odds()) -> active(odds()), mark(pairs()) -> active(pairs()), mark(s(X)) -> active(s(mark(X))), mark(head(X)) -> active(head(mark(X))), mark(tail(X)) -> active(tail(mark(X))), 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), incr(mark(X)) -> incr(X), incr(active(X)) -> incr(X), active(incr(cons(X, XS))) -> mark(cons(s(X), incr(XS))), active(nats()) -> mark(cons(0(), incr(nats()))), active(odds()) -> mark(incr(pairs())), active(pairs()) -> mark(cons(0(), incr(odds()))), active(head(cons(X, XS))) -> mark(X), active(tail(cons(X, XS))) -> mark(XS), s(mark(X)) -> s(X), s(active(X)) -> s(X), head(mark(X)) -> head(X), head(active(X)) -> head(X), tail(mark(X)) -> tail(X), tail(active(X)) -> tail(X)} POLY: Argument Filtering: pi(tail) = [], pi(head) = [], pi(s) = [], pi(pairs) = [], pi(odds) = [], pi(active#) = 0, pi(active) = [], pi(nats) = [], pi(incr) = [], pi(0) = [], pi(cons) = [], pi(mark#) = [], pi(mark) = [] Usable Rules: {} Interpretation: [mark#] = 1, [cons] = 0, [tail] = 1, [head] = 1, [s] = 0, [incr] = 1, [pairs] = 1, [odds] = 1, [nats] = 1 Strict: { mark#(cons(X1, X2)) -> mark#(X1), mark#(incr(X)) -> mark#(X), mark#(incr(X)) -> active#(incr(mark(X))), mark#(nats()) -> active#(nats()), mark#(odds()) -> active#(odds()), mark#(pairs()) -> active#(pairs()), mark#(s(X)) -> mark#(X), mark#(head(X)) -> mark#(X), mark#(head(X)) -> active#(head(mark(X))), mark#(tail(X)) -> mark#(X), mark#(tail(X)) -> active#(tail(mark(X))), active#(incr(cons(X, XS))) -> mark#(cons(s(X), incr(XS))), active#(nats()) -> mark#(cons(0(), incr(nats()))), active#(odds()) -> mark#(incr(pairs())), active#(pairs()) -> mark#(cons(0(), incr(odds()))), active#(head(cons(X, XS))) -> mark#(X), active#(tail(cons(X, XS))) -> mark#(XS)} Weak: { mark(cons(X1, X2)) -> active(cons(mark(X1), X2)), mark(0()) -> active(0()), mark(incr(X)) -> active(incr(mark(X))), mark(nats()) -> active(nats()), mark(odds()) -> active(odds()), mark(pairs()) -> active(pairs()), mark(s(X)) -> active(s(mark(X))), mark(head(X)) -> active(head(mark(X))), mark(tail(X)) -> active(tail(mark(X))), 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), incr(mark(X)) -> incr(X), incr(active(X)) -> incr(X), active(incr(cons(X, XS))) -> mark(cons(s(X), incr(XS))), active(nats()) -> mark(cons(0(), incr(nats()))), active(odds()) -> mark(incr(pairs())), active(pairs()) -> mark(cons(0(), incr(odds()))), active(head(cons(X, XS))) -> mark(X), active(tail(cons(X, XS))) -> mark(XS), s(mark(X)) -> s(X), s(active(X)) -> s(X), head(mark(X)) -> head(X), head(active(X)) -> head(X), tail(mark(X)) -> tail(X), tail(active(X)) -> tail(X)} EDG: {(mark#(odds()) -> active#(odds()), active#(odds()) -> mark#(incr(pairs()))) (active#(incr(cons(X, XS))) -> mark#(cons(s(X), incr(XS))), mark#(tail(X)) -> active#(tail(mark(X)))) (active#(incr(cons(X, XS))) -> mark#(cons(s(X), incr(XS))), mark#(tail(X)) -> mark#(X)) (active#(incr(cons(X, XS))) -> mark#(cons(s(X), incr(XS))), mark#(head(X)) -> active#(head(mark(X)))) (active#(incr(cons(X, XS))) -> mark#(cons(s(X), incr(XS))), mark#(head(X)) -> mark#(X)) (active#(incr(cons(X, XS))) -> mark#(cons(s(X), incr(XS))), mark#(s(X)) -> mark#(X)) (active#(incr(cons(X, XS))) -> mark#(cons(s(X), incr(XS))), mark#(incr(X)) -> active#(incr(mark(X)))) (active#(incr(cons(X, XS))) -> mark#(cons(s(X), incr(XS))), mark#(incr(X)) -> mark#(X)) (active#(incr(cons(X, XS))) -> mark#(cons(s(X), incr(XS))), mark#(cons(X1, X2)) -> mark#(X1)) (active#(pairs()) -> mark#(cons(0(), incr(odds()))), mark#(cons(X1, X2)) -> mark#(X1)) (active#(tail(cons(X, XS))) -> mark#(XS), mark#(tail(X)) -> active#(tail(mark(X)))) (active#(tail(cons(X, XS))) -> mark#(XS), mark#(tail(X)) -> mark#(X)) (active#(tail(cons(X, XS))) -> mark#(XS), mark#(head(X)) -> active#(head(mark(X)))) (active#(tail(cons(X, XS))) -> mark#(XS), mark#(head(X)) -> mark#(X)) (active#(tail(cons(X, XS))) -> mark#(XS), mark#(s(X)) -> mark#(X)) (active#(tail(cons(X, XS))) -> mark#(XS), mark#(pairs()) -> active#(pairs())) (active#(tail(cons(X, XS))) -> mark#(XS), mark#(odds()) -> active#(odds())) (active#(tail(cons(X, XS))) -> mark#(XS), mark#(nats()) -> active#(nats())) (active#(tail(cons(X, XS))) -> mark#(XS), mark#(incr(X)) -> active#(incr(mark(X)))) (active#(tail(cons(X, XS))) -> mark#(XS), mark#(incr(X)) -> mark#(X)) (active#(tail(cons(X, XS))) -> mark#(XS), mark#(cons(X1, X2)) -> mark#(X1)) (mark#(s(X)) -> mark#(X), mark#(tail(X)) -> active#(tail(mark(X)))) (mark#(s(X)) -> mark#(X), mark#(tail(X)) -> mark#(X)) (mark#(s(X)) -> mark#(X), mark#(head(X)) -> active#(head(mark(X)))) (mark#(s(X)) -> mark#(X), mark#(head(X)) -> mark#(X)) (mark#(s(X)) -> mark#(X), mark#(s(X)) -> mark#(X)) (mark#(s(X)) -> mark#(X), mark#(pairs()) -> active#(pairs())) (mark#(s(X)) -> mark#(X), mark#(odds()) -> active#(odds())) (mark#(s(X)) -> mark#(X), mark#(nats()) -> active#(nats())) (mark#(s(X)) -> mark#(X), mark#(incr(X)) -> active#(incr(mark(X)))) (mark#(s(X)) -> mark#(X), mark#(incr(X)) -> mark#(X)) (mark#(s(X)) -> mark#(X), mark#(cons(X1, X2)) -> mark#(X1)) (mark#(tail(X)) -> mark#(X), mark#(tail(X)) -> active#(tail(mark(X)))) (mark#(tail(X)) -> mark#(X), mark#(tail(X)) -> mark#(X)) (mark#(tail(X)) -> mark#(X), mark#(head(X)) -> active#(head(mark(X)))) (mark#(tail(X)) -> mark#(X), mark#(head(X)) -> mark#(X)) (mark#(tail(X)) -> mark#(X), mark#(s(X)) -> mark#(X)) (mark#(tail(X)) -> mark#(X), mark#(pairs()) -> active#(pairs())) (mark#(tail(X)) -> mark#(X), mark#(odds()) -> active#(odds())) (mark#(tail(X)) -> mark#(X), mark#(nats()) -> active#(nats())) (mark#(tail(X)) -> mark#(X), mark#(incr(X)) -> active#(incr(mark(X)))) (mark#(tail(X)) -> mark#(X), mark#(incr(X)) -> mark#(X)) (mark#(tail(X)) -> mark#(X), mark#(cons(X1, X2)) -> mark#(X1)) (mark#(incr(X)) -> active#(incr(mark(X))), active#(tail(cons(X, XS))) -> mark#(XS)) (mark#(incr(X)) -> active#(incr(mark(X))), active#(head(cons(X, XS))) -> mark#(X)) (mark#(incr(X)) -> active#(incr(mark(X))), active#(incr(cons(X, XS))) -> mark#(cons(s(X), incr(XS)))) (mark#(tail(X)) -> active#(tail(mark(X))), active#(tail(cons(X, XS))) -> mark#(XS)) (mark#(tail(X)) -> active#(tail(mark(X))), active#(head(cons(X, XS))) -> mark#(X)) (mark#(tail(X)) -> active#(tail(mark(X))), active#(incr(cons(X, XS))) -> mark#(cons(s(X), incr(XS)))) (active#(odds()) -> mark#(incr(pairs())), mark#(incr(X)) -> mark#(X)) (active#(odds()) -> mark#(incr(pairs())), mark#(incr(X)) -> active#(incr(mark(X)))) (mark#(head(X)) -> active#(head(mark(X))), active#(incr(cons(X, XS))) -> mark#(cons(s(X), incr(XS)))) (mark#(head(X)) -> active#(head(mark(X))), active#(head(cons(X, XS))) -> mark#(X)) (mark#(head(X)) -> active#(head(mark(X))), active#(tail(cons(X, XS))) -> mark#(XS)) (active#(head(cons(X, XS))) -> mark#(X), mark#(cons(X1, X2)) -> mark#(X1)) (active#(head(cons(X, XS))) -> mark#(X), mark#(incr(X)) -> mark#(X)) (active#(head(cons(X, XS))) -> mark#(X), mark#(incr(X)) -> active#(incr(mark(X)))) (active#(head(cons(X, XS))) -> mark#(X), mark#(nats()) -> active#(nats())) (active#(head(cons(X, XS))) -> mark#(X), mark#(odds()) -> active#(odds())) (active#(head(cons(X, XS))) -> mark#(X), mark#(pairs()) -> active#(pairs())) (active#(head(cons(X, XS))) -> mark#(X), mark#(s(X)) -> mark#(X)) (active#(head(cons(X, XS))) -> mark#(X), mark#(head(X)) -> mark#(X)) (active#(head(cons(X, XS))) -> mark#(X), mark#(head(X)) -> active#(head(mark(X)))) (active#(head(cons(X, XS))) -> mark#(X), mark#(tail(X)) -> mark#(X)) (active#(head(cons(X, XS))) -> mark#(X), mark#(tail(X)) -> active#(tail(mark(X)))) (mark#(head(X)) -> mark#(X), mark#(cons(X1, X2)) -> mark#(X1)) (mark#(head(X)) -> mark#(X), mark#(incr(X)) -> mark#(X)) (mark#(head(X)) -> mark#(X), mark#(incr(X)) -> active#(incr(mark(X)))) (mark#(head(X)) -> mark#(X), mark#(nats()) -> active#(nats())) (mark#(head(X)) -> mark#(X), mark#(odds()) -> active#(odds())) (mark#(head(X)) -> mark#(X), mark#(pairs()) -> active#(pairs())) (mark#(head(X)) -> mark#(X), mark#(s(X)) -> mark#(X)) (mark#(head(X)) -> mark#(X), mark#(head(X)) -> mark#(X)) (mark#(head(X)) -> mark#(X), mark#(head(X)) -> active#(head(mark(X)))) (mark#(head(X)) -> mark#(X), mark#(tail(X)) -> mark#(X)) (mark#(head(X)) -> mark#(X), mark#(tail(X)) -> active#(tail(mark(X)))) (mark#(incr(X)) -> mark#(X), mark#(cons(X1, X2)) -> mark#(X1)) (mark#(incr(X)) -> mark#(X), mark#(incr(X)) -> mark#(X)) (mark#(incr(X)) -> mark#(X), mark#(incr(X)) -> active#(incr(mark(X)))) (mark#(incr(X)) -> mark#(X), mark#(nats()) -> active#(nats())) (mark#(incr(X)) -> mark#(X), mark#(odds()) -> active#(odds())) (mark#(incr(X)) -> mark#(X), mark#(pairs()) -> active#(pairs())) (mark#(incr(X)) -> mark#(X), mark#(s(X)) -> mark#(X)) (mark#(incr(X)) -> mark#(X), mark#(head(X)) -> mark#(X)) (mark#(incr(X)) -> mark#(X), mark#(head(X)) -> active#(head(mark(X)))) (mark#(incr(X)) -> mark#(X), mark#(tail(X)) -> mark#(X)) (mark#(incr(X)) -> mark#(X), mark#(tail(X)) -> active#(tail(mark(X)))) (mark#(cons(X1, X2)) -> mark#(X1), mark#(cons(X1, X2)) -> mark#(X1)) (mark#(cons(X1, X2)) -> mark#(X1), mark#(incr(X)) -> mark#(X)) (mark#(cons(X1, X2)) -> mark#(X1), mark#(incr(X)) -> active#(incr(mark(X)))) (mark#(cons(X1, X2)) -> mark#(X1), mark#(nats()) -> active#(nats())) (mark#(cons(X1, X2)) -> mark#(X1), mark#(odds()) -> active#(odds())) (mark#(cons(X1, X2)) -> mark#(X1), mark#(pairs()) -> active#(pairs())) (mark#(cons(X1, X2)) -> mark#(X1), mark#(s(X)) -> mark#(X)) (mark#(cons(X1, X2)) -> mark#(X1), mark#(head(X)) -> mark#(X)) (mark#(cons(X1, X2)) -> mark#(X1), mark#(head(X)) -> active#(head(mark(X)))) (mark#(cons(X1, X2)) -> mark#(X1), mark#(tail(X)) -> mark#(X)) (mark#(cons(X1, X2)) -> mark#(X1), mark#(tail(X)) -> active#(tail(mark(X)))) (active#(nats()) -> mark#(cons(0(), incr(nats()))), mark#(cons(X1, X2)) -> mark#(X1)) (mark#(pairs()) -> active#(pairs()), active#(pairs()) -> mark#(cons(0(), incr(odds())))) (mark#(nats()) -> active#(nats()), active#(nats()) -> mark#(cons(0(), incr(nats()))))} SCCS: Scc: { mark#(cons(X1, X2)) -> mark#(X1), mark#(incr(X)) -> mark#(X), mark#(incr(X)) -> active#(incr(mark(X))), mark#(nats()) -> active#(nats()), mark#(odds()) -> active#(odds()), mark#(pairs()) -> active#(pairs()), mark#(s(X)) -> mark#(X), mark#(head(X)) -> mark#(X), mark#(head(X)) -> active#(head(mark(X))), mark#(tail(X)) -> mark#(X), mark#(tail(X)) -> active#(tail(mark(X))), active#(incr(cons(X, XS))) -> mark#(cons(s(X), incr(XS))), active#(nats()) -> mark#(cons(0(), incr(nats()))), active#(odds()) -> mark#(incr(pairs())), active#(pairs()) -> mark#(cons(0(), incr(odds()))), active#(head(cons(X, XS))) -> mark#(X), active#(tail(cons(X, XS))) -> mark#(XS)} SCC: Strict: { mark#(cons(X1, X2)) -> mark#(X1), mark#(incr(X)) -> mark#(X), mark#(incr(X)) -> active#(incr(mark(X))), mark#(nats()) -> active#(nats()), mark#(odds()) -> active#(odds()), mark#(pairs()) -> active#(pairs()), mark#(s(X)) -> mark#(X), mark#(head(X)) -> mark#(X), mark#(head(X)) -> active#(head(mark(X))), mark#(tail(X)) -> mark#(X), mark#(tail(X)) -> active#(tail(mark(X))), active#(incr(cons(X, XS))) -> mark#(cons(s(X), incr(XS))), active#(nats()) -> mark#(cons(0(), incr(nats()))), active#(odds()) -> mark#(incr(pairs())), active#(pairs()) -> mark#(cons(0(), incr(odds()))), active#(head(cons(X, XS))) -> mark#(X), active#(tail(cons(X, XS))) -> mark#(XS)} Weak: { mark(cons(X1, X2)) -> active(cons(mark(X1), X2)), mark(0()) -> active(0()), mark(incr(X)) -> active(incr(mark(X))), mark(nats()) -> active(nats()), mark(odds()) -> active(odds()), mark(pairs()) -> active(pairs()), mark(s(X)) -> active(s(mark(X))), mark(head(X)) -> active(head(mark(X))), mark(tail(X)) -> active(tail(mark(X))), 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), incr(mark(X)) -> incr(X), incr(active(X)) -> incr(X), active(incr(cons(X, XS))) -> mark(cons(s(X), incr(XS))), active(nats()) -> mark(cons(0(), incr(nats()))), active(odds()) -> mark(incr(pairs())), active(pairs()) -> mark(cons(0(), incr(odds()))), active(head(cons(X, XS))) -> mark(X), active(tail(cons(X, XS))) -> mark(XS), s(mark(X)) -> s(X), s(active(X)) -> s(X), head(mark(X)) -> head(X), head(active(X)) -> head(X), tail(mark(X)) -> tail(X), tail(active(X)) -> tail(X)} POLY: Argument Filtering: pi(tail) = [0], pi(head) = 0, pi(s) = 0, pi(pairs) = [], pi(odds) = [], pi(active#) = 0, pi(active) = 0, pi(nats) = [], pi(incr) = 0, pi(0) = [], pi(cons) = [0,1], pi(mark#) = 0, pi(mark) = 0 Usable Rules: {} Interpretation: [cons](x0, x1) = x0 + x1, [tail](x0) = x0 + 1, [pairs] = 0, [odds] = 0, [nats] = 0, [0] = 0 Strict: { mark#(cons(X1, X2)) -> mark#(X1), mark#(incr(X)) -> mark#(X), mark#(incr(X)) -> active#(incr(mark(X))), mark#(nats()) -> active#(nats()), mark#(odds()) -> active#(odds()), mark#(pairs()) -> active#(pairs()), mark#(s(X)) -> mark#(X), mark#(head(X)) -> mark#(X), mark#(head(X)) -> active#(head(mark(X))), mark#(tail(X)) -> active#(tail(mark(X))), active#(incr(cons(X, XS))) -> mark#(cons(s(X), incr(XS))), active#(nats()) -> mark#(cons(0(), incr(nats()))), active#(odds()) -> mark#(incr(pairs())), active#(pairs()) -> mark#(cons(0(), incr(odds()))), active#(head(cons(X, XS))) -> mark#(X)} Weak: { mark(cons(X1, X2)) -> active(cons(mark(X1), X2)), mark(0()) -> active(0()), mark(incr(X)) -> active(incr(mark(X))), mark(nats()) -> active(nats()), mark(odds()) -> active(odds()), mark(pairs()) -> active(pairs()), mark(s(X)) -> active(s(mark(X))), mark(head(X)) -> active(head(mark(X))), mark(tail(X)) -> active(tail(mark(X))), 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), incr(mark(X)) -> incr(X), incr(active(X)) -> incr(X), active(incr(cons(X, XS))) -> mark(cons(s(X), incr(XS))), active(nats()) -> mark(cons(0(), incr(nats()))), active(odds()) -> mark(incr(pairs())), active(pairs()) -> mark(cons(0(), incr(odds()))), active(head(cons(X, XS))) -> mark(X), active(tail(cons(X, XS))) -> mark(XS), s(mark(X)) -> s(X), s(active(X)) -> s(X), head(mark(X)) -> head(X), head(active(X)) -> head(X), tail(mark(X)) -> tail(X), tail(active(X)) -> tail(X)} EDG: {(active#(odds()) -> mark#(incr(pairs())), mark#(incr(X)) -> active#(incr(mark(X)))) (active#(odds()) -> mark#(incr(pairs())), mark#(incr(X)) -> mark#(X)) (mark#(head(X)) -> active#(head(mark(X))), active#(head(cons(X, XS))) -> mark#(X)) (mark#(head(X)) -> active#(head(mark(X))), active#(incr(cons(X, XS))) -> mark#(cons(s(X), incr(XS)))) (mark#(incr(X)) -> mark#(X), mark#(tail(X)) -> active#(tail(mark(X)))) (mark#(incr(X)) -> mark#(X), mark#(head(X)) -> active#(head(mark(X)))) (mark#(incr(X)) -> mark#(X), mark#(head(X)) -> mark#(X)) (mark#(incr(X)) -> mark#(X), mark#(s(X)) -> mark#(X)) (mark#(incr(X)) -> mark#(X), mark#(pairs()) -> active#(pairs())) (mark#(incr(X)) -> mark#(X), mark#(odds()) -> active#(odds())) (mark#(incr(X)) -> mark#(X), mark#(nats()) -> active#(nats())) (mark#(incr(X)) -> mark#(X), mark#(incr(X)) -> active#(incr(mark(X)))) (mark#(incr(X)) -> mark#(X), mark#(incr(X)) -> mark#(X)) (mark#(incr(X)) -> mark#(X), mark#(cons(X1, X2)) -> mark#(X1)) (mark#(head(X)) -> mark#(X), mark#(tail(X)) -> active#(tail(mark(X)))) (mark#(head(X)) -> mark#(X), mark#(head(X)) -> active#(head(mark(X)))) (mark#(head(X)) -> mark#(X), mark#(head(X)) -> mark#(X)) (mark#(head(X)) -> mark#(X), mark#(s(X)) -> mark#(X)) (mark#(head(X)) -> mark#(X), mark#(pairs()) -> active#(pairs())) (mark#(head(X)) -> mark#(X), mark#(odds()) -> active#(odds())) (mark#(head(X)) -> mark#(X), mark#(nats()) -> active#(nats())) (mark#(head(X)) -> mark#(X), mark#(incr(X)) -> active#(incr(mark(X)))) (mark#(head(X)) -> mark#(X), mark#(incr(X)) -> mark#(X)) (mark#(head(X)) -> mark#(X), mark#(cons(X1, X2)) -> mark#(X1)) (mark#(nats()) -> active#(nats()), active#(nats()) -> mark#(cons(0(), incr(nats())))) (mark#(pairs()) -> active#(pairs()), active#(pairs()) -> mark#(cons(0(), incr(odds())))) (active#(nats()) -> mark#(cons(0(), incr(nats()))), mark#(cons(X1, X2)) -> mark#(X1)) (active#(pairs()) -> mark#(cons(0(), incr(odds()))), mark#(cons(X1, X2)) -> mark#(X1)) (active#(incr(cons(X, XS))) -> mark#(cons(s(X), incr(XS))), mark#(cons(X1, X2)) -> mark#(X1)) (active#(incr(cons(X, XS))) -> mark#(cons(s(X), incr(XS))), mark#(incr(X)) -> mark#(X)) (active#(incr(cons(X, XS))) -> mark#(cons(s(X), incr(XS))), mark#(incr(X)) -> active#(incr(mark(X)))) (active#(incr(cons(X, XS))) -> mark#(cons(s(X), incr(XS))), mark#(s(X)) -> mark#(X)) (active#(incr(cons(X, XS))) -> mark#(cons(s(X), incr(XS))), mark#(head(X)) -> mark#(X)) (active#(incr(cons(X, XS))) -> mark#(cons(s(X), incr(XS))), mark#(head(X)) -> active#(head(mark(X)))) (active#(incr(cons(X, XS))) -> mark#(cons(s(X), incr(XS))), mark#(tail(X)) -> active#(tail(mark(X)))) (mark#(odds()) -> active#(odds()), active#(odds()) -> mark#(incr(pairs()))) (active#(head(cons(X, XS))) -> mark#(X), mark#(cons(X1, X2)) -> mark#(X1)) (active#(head(cons(X, XS))) -> mark#(X), mark#(incr(X)) -> mark#(X)) (active#(head(cons(X, XS))) -> mark#(X), mark#(incr(X)) -> active#(incr(mark(X)))) (active#(head(cons(X, XS))) -> mark#(X), mark#(nats()) -> active#(nats())) (active#(head(cons(X, XS))) -> mark#(X), mark#(odds()) -> active#(odds())) (active#(head(cons(X, XS))) -> mark#(X), mark#(pairs()) -> active#(pairs())) (active#(head(cons(X, XS))) -> mark#(X), mark#(s(X)) -> mark#(X)) (active#(head(cons(X, XS))) -> mark#(X), mark#(head(X)) -> mark#(X)) (active#(head(cons(X, XS))) -> mark#(X), mark#(head(X)) -> active#(head(mark(X)))) (active#(head(cons(X, XS))) -> mark#(X), mark#(tail(X)) -> active#(tail(mark(X)))) (mark#(s(X)) -> mark#(X), mark#(cons(X1, X2)) -> mark#(X1)) (mark#(s(X)) -> mark#(X), mark#(incr(X)) -> mark#(X)) (mark#(s(X)) -> mark#(X), mark#(incr(X)) -> active#(incr(mark(X)))) (mark#(s(X)) -> mark#(X), mark#(nats()) -> active#(nats())) (mark#(s(X)) -> mark#(X), mark#(odds()) -> active#(odds())) (mark#(s(X)) -> mark#(X), mark#(pairs()) -> active#(pairs())) (mark#(s(X)) -> mark#(X), mark#(s(X)) -> mark#(X)) (mark#(s(X)) -> mark#(X), mark#(head(X)) -> mark#(X)) (mark#(s(X)) -> mark#(X), mark#(head(X)) -> active#(head(mark(X)))) (mark#(s(X)) -> mark#(X), mark#(tail(X)) -> active#(tail(mark(X)))) (mark#(tail(X)) -> active#(tail(mark(X))), active#(incr(cons(X, XS))) -> mark#(cons(s(X), incr(XS)))) (mark#(tail(X)) -> active#(tail(mark(X))), active#(head(cons(X, XS))) -> mark#(X)) (mark#(incr(X)) -> active#(incr(mark(X))), active#(incr(cons(X, XS))) -> mark#(cons(s(X), incr(XS)))) (mark#(incr(X)) -> active#(incr(mark(X))), active#(head(cons(X, XS))) -> mark#(X)) (mark#(cons(X1, X2)) -> mark#(X1), mark#(cons(X1, X2)) -> mark#(X1)) (mark#(cons(X1, X2)) -> mark#(X1), mark#(incr(X)) -> mark#(X)) (mark#(cons(X1, X2)) -> mark#(X1), mark#(incr(X)) -> active#(incr(mark(X)))) (mark#(cons(X1, X2)) -> mark#(X1), mark#(nats()) -> active#(nats())) (mark#(cons(X1, X2)) -> mark#(X1), mark#(odds()) -> active#(odds())) (mark#(cons(X1, X2)) -> mark#(X1), mark#(pairs()) -> active#(pairs())) (mark#(cons(X1, X2)) -> mark#(X1), mark#(s(X)) -> mark#(X)) (mark#(cons(X1, X2)) -> mark#(X1), mark#(head(X)) -> mark#(X)) (mark#(cons(X1, X2)) -> mark#(X1), mark#(head(X)) -> active#(head(mark(X)))) (mark#(cons(X1, X2)) -> mark#(X1), mark#(tail(X)) -> active#(tail(mark(X))))} SCCS: Scc: { mark#(cons(X1, X2)) -> mark#(X1), mark#(incr(X)) -> mark#(X), mark#(incr(X)) -> active#(incr(mark(X))), mark#(nats()) -> active#(nats()), mark#(odds()) -> active#(odds()), mark#(pairs()) -> active#(pairs()), mark#(s(X)) -> mark#(X), mark#(head(X)) -> mark#(X), mark#(head(X)) -> active#(head(mark(X))), mark#(tail(X)) -> active#(tail(mark(X))), active#(incr(cons(X, XS))) -> mark#(cons(s(X), incr(XS))), active#(nats()) -> mark#(cons(0(), incr(nats()))), active#(odds()) -> mark#(incr(pairs())), active#(pairs()) -> mark#(cons(0(), incr(odds()))), active#(head(cons(X, XS))) -> mark#(X)} SCC: Strict: { mark#(cons(X1, X2)) -> mark#(X1), mark#(incr(X)) -> mark#(X), mark#(incr(X)) -> active#(incr(mark(X))), mark#(nats()) -> active#(nats()), mark#(odds()) -> active#(odds()), mark#(pairs()) -> active#(pairs()), mark#(s(X)) -> mark#(X), mark#(head(X)) -> mark#(X), mark#(head(X)) -> active#(head(mark(X))), mark#(tail(X)) -> active#(tail(mark(X))), active#(incr(cons(X, XS))) -> mark#(cons(s(X), incr(XS))), active#(nats()) -> mark#(cons(0(), incr(nats()))), active#(odds()) -> mark#(incr(pairs())), active#(pairs()) -> mark#(cons(0(), incr(odds()))), active#(head(cons(X, XS))) -> mark#(X)} Weak: { mark(cons(X1, X2)) -> active(cons(mark(X1), X2)), mark(0()) -> active(0()), mark(incr(X)) -> active(incr(mark(X))), mark(nats()) -> active(nats()), mark(odds()) -> active(odds()), mark(pairs()) -> active(pairs()), mark(s(X)) -> active(s(mark(X))), mark(head(X)) -> active(head(mark(X))), mark(tail(X)) -> active(tail(mark(X))), 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), incr(mark(X)) -> incr(X), incr(active(X)) -> incr(X), active(incr(cons(X, XS))) -> mark(cons(s(X), incr(XS))), active(nats()) -> mark(cons(0(), incr(nats()))), active(odds()) -> mark(incr(pairs())), active(pairs()) -> mark(cons(0(), incr(odds()))), active(head(cons(X, XS))) -> mark(X), active(tail(cons(X, XS))) -> mark(XS), s(mark(X)) -> s(X), s(active(X)) -> s(X), head(mark(X)) -> head(X), head(active(X)) -> head(X), tail(mark(X)) -> tail(X), tail(active(X)) -> tail(X)} POLY: Argument Filtering: pi(tail) = [], pi(head) = [], pi(s) = [], pi(pairs) = [], pi(odds) = [], pi(active#) = 0, pi(active) = [], pi(nats) = [], pi(incr) = [], pi(0) = [], pi(cons) = [], pi(mark#) = [], pi(mark) = [] Usable Rules: {} Interpretation: [mark#] = 1, [tail] = 0, [head] = 1, [incr] = 1, [pairs] = 1, [odds] = 1, [nats] = 1 Strict: { mark#(cons(X1, X2)) -> mark#(X1), mark#(incr(X)) -> mark#(X), mark#(incr(X)) -> active#(incr(mark(X))), mark#(nats()) -> active#(nats()), mark#(odds()) -> active#(odds()), mark#(pairs()) -> active#(pairs()), mark#(s(X)) -> mark#(X), mark#(head(X)) -> mark#(X), mark#(head(X)) -> active#(head(mark(X))), active#(incr(cons(X, XS))) -> mark#(cons(s(X), incr(XS))), active#(nats()) -> mark#(cons(0(), incr(nats()))), active#(odds()) -> mark#(incr(pairs())), active#(pairs()) -> mark#(cons(0(), incr(odds()))), active#(head(cons(X, XS))) -> mark#(X)} Weak: { mark(cons(X1, X2)) -> active(cons(mark(X1), X2)), mark(0()) -> active(0()), mark(incr(X)) -> active(incr(mark(X))), mark(nats()) -> active(nats()), mark(odds()) -> active(odds()), mark(pairs()) -> active(pairs()), mark(s(X)) -> active(s(mark(X))), mark(head(X)) -> active(head(mark(X))), mark(tail(X)) -> active(tail(mark(X))), 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), incr(mark(X)) -> incr(X), incr(active(X)) -> incr(X), active(incr(cons(X, XS))) -> mark(cons(s(X), incr(XS))), active(nats()) -> mark(cons(0(), incr(nats()))), active(odds()) -> mark(incr(pairs())), active(pairs()) -> mark(cons(0(), incr(odds()))), active(head(cons(X, XS))) -> mark(X), active(tail(cons(X, XS))) -> mark(XS), s(mark(X)) -> s(X), s(active(X)) -> s(X), head(mark(X)) -> head(X), head(active(X)) -> head(X), tail(mark(X)) -> tail(X), tail(active(X)) -> tail(X)} EDG: {(mark#(head(X)) -> active#(head(mark(X))), active#(head(cons(X, XS))) -> mark#(X)) (mark#(head(X)) -> active#(head(mark(X))), active#(incr(cons(X, XS))) -> mark#(cons(s(X), incr(XS)))) (mark#(cons(X1, X2)) -> mark#(X1), mark#(head(X)) -> active#(head(mark(X)))) (mark#(cons(X1, X2)) -> mark#(X1), mark#(head(X)) -> mark#(X)) (mark#(cons(X1, X2)) -> mark#(X1), mark#(s(X)) -> mark#(X)) (mark#(cons(X1, X2)) -> mark#(X1), mark#(pairs()) -> active#(pairs())) (mark#(cons(X1, X2)) -> mark#(X1), mark#(odds()) -> active#(odds())) (mark#(cons(X1, X2)) -> mark#(X1), mark#(nats()) -> active#(nats())) (mark#(cons(X1, X2)) -> mark#(X1), mark#(incr(X)) -> active#(incr(mark(X)))) (mark#(cons(X1, X2)) -> mark#(X1), mark#(incr(X)) -> mark#(X)) (mark#(cons(X1, X2)) -> mark#(X1), mark#(cons(X1, X2)) -> mark#(X1)) (mark#(s(X)) -> mark#(X), mark#(head(X)) -> active#(head(mark(X)))) (mark#(s(X)) -> mark#(X), mark#(head(X)) -> mark#(X)) (mark#(s(X)) -> mark#(X), mark#(s(X)) -> mark#(X)) (mark#(s(X)) -> mark#(X), mark#(pairs()) -> active#(pairs())) (mark#(s(X)) -> mark#(X), mark#(odds()) -> active#(odds())) (mark#(s(X)) -> mark#(X), mark#(nats()) -> active#(nats())) (mark#(s(X)) -> mark#(X), mark#(incr(X)) -> active#(incr(mark(X)))) (mark#(s(X)) -> mark#(X), mark#(incr(X)) -> mark#(X)) (mark#(s(X)) -> mark#(X), mark#(cons(X1, X2)) -> mark#(X1)) (active#(head(cons(X, XS))) -> mark#(X), mark#(head(X)) -> active#(head(mark(X)))) (active#(head(cons(X, XS))) -> mark#(X), mark#(head(X)) -> mark#(X)) (active#(head(cons(X, XS))) -> mark#(X), mark#(s(X)) -> mark#(X)) (active#(head(cons(X, XS))) -> mark#(X), mark#(pairs()) -> active#(pairs())) (active#(head(cons(X, XS))) -> mark#(X), mark#(odds()) -> active#(odds())) (active#(head(cons(X, XS))) -> mark#(X), mark#(nats()) -> active#(nats())) (active#(head(cons(X, XS))) -> mark#(X), mark#(incr(X)) -> active#(incr(mark(X)))) (active#(head(cons(X, XS))) -> mark#(X), mark#(incr(X)) -> mark#(X)) (active#(head(cons(X, XS))) -> mark#(X), mark#(cons(X1, X2)) -> mark#(X1)) (mark#(odds()) -> active#(odds()), active#(odds()) -> mark#(incr(pairs()))) (active#(incr(cons(X, XS))) -> mark#(cons(s(X), incr(XS))), mark#(head(X)) -> active#(head(mark(X)))) (active#(incr(cons(X, XS))) -> mark#(cons(s(X), incr(XS))), mark#(head(X)) -> mark#(X)) (active#(incr(cons(X, XS))) -> mark#(cons(s(X), incr(XS))), mark#(s(X)) -> mark#(X)) (active#(incr(cons(X, XS))) -> mark#(cons(s(X), incr(XS))), mark#(incr(X)) -> active#(incr(mark(X)))) (active#(incr(cons(X, XS))) -> mark#(cons(s(X), incr(XS))), mark#(incr(X)) -> mark#(X)) (active#(incr(cons(X, XS))) -> mark#(cons(s(X), incr(XS))), mark#(cons(X1, X2)) -> mark#(X1)) (active#(pairs()) -> mark#(cons(0(), incr(odds()))), mark#(cons(X1, X2)) -> mark#(X1)) (active#(nats()) -> mark#(cons(0(), incr(nats()))), mark#(cons(X1, X2)) -> mark#(X1)) (mark#(pairs()) -> active#(pairs()), active#(pairs()) -> mark#(cons(0(), incr(odds())))) (mark#(nats()) -> active#(nats()), active#(nats()) -> mark#(cons(0(), incr(nats())))) (mark#(head(X)) -> mark#(X), mark#(cons(X1, X2)) -> mark#(X1)) (mark#(head(X)) -> mark#(X), mark#(incr(X)) -> mark#(X)) (mark#(head(X)) -> mark#(X), mark#(incr(X)) -> active#(incr(mark(X)))) (mark#(head(X)) -> mark#(X), mark#(nats()) -> active#(nats())) (mark#(head(X)) -> mark#(X), mark#(odds()) -> active#(odds())) (mark#(head(X)) -> mark#(X), mark#(pairs()) -> active#(pairs())) (mark#(head(X)) -> mark#(X), mark#(s(X)) -> mark#(X)) (mark#(head(X)) -> mark#(X), mark#(head(X)) -> mark#(X)) (mark#(head(X)) -> mark#(X), mark#(head(X)) -> active#(head(mark(X)))) (mark#(incr(X)) -> mark#(X), mark#(cons(X1, X2)) -> mark#(X1)) (mark#(incr(X)) -> mark#(X), mark#(incr(X)) -> mark#(X)) (mark#(incr(X)) -> mark#(X), mark#(incr(X)) -> active#(incr(mark(X)))) (mark#(incr(X)) -> mark#(X), mark#(nats()) -> active#(nats())) (mark#(incr(X)) -> mark#(X), mark#(odds()) -> active#(odds())) (mark#(incr(X)) -> mark#(X), mark#(pairs()) -> active#(pairs())) (mark#(incr(X)) -> mark#(X), mark#(s(X)) -> mark#(X)) (mark#(incr(X)) -> mark#(X), mark#(head(X)) -> mark#(X)) (mark#(incr(X)) -> mark#(X), mark#(head(X)) -> active#(head(mark(X)))) (active#(odds()) -> mark#(incr(pairs())), mark#(incr(X)) -> mark#(X)) (active#(odds()) -> mark#(incr(pairs())), mark#(incr(X)) -> active#(incr(mark(X)))) (mark#(incr(X)) -> active#(incr(mark(X))), active#(incr(cons(X, XS))) -> mark#(cons(s(X), incr(XS)))) (mark#(incr(X)) -> active#(incr(mark(X))), active#(head(cons(X, XS))) -> mark#(X))} SCCS: Scc: { mark#(cons(X1, X2)) -> mark#(X1), mark#(incr(X)) -> mark#(X), mark#(incr(X)) -> active#(incr(mark(X))), mark#(nats()) -> active#(nats()), mark#(odds()) -> active#(odds()), mark#(pairs()) -> active#(pairs()), mark#(s(X)) -> mark#(X), mark#(head(X)) -> mark#(X), mark#(head(X)) -> active#(head(mark(X))), active#(incr(cons(X, XS))) -> mark#(cons(s(X), incr(XS))), active#(nats()) -> mark#(cons(0(), incr(nats()))), active#(odds()) -> mark#(incr(pairs())), active#(pairs()) -> mark#(cons(0(), incr(odds()))), active#(head(cons(X, XS))) -> mark#(X)} SCC: Strict: { mark#(cons(X1, X2)) -> mark#(X1), mark#(incr(X)) -> mark#(X), mark#(incr(X)) -> active#(incr(mark(X))), mark#(nats()) -> active#(nats()), mark#(odds()) -> active#(odds()), mark#(pairs()) -> active#(pairs()), mark#(s(X)) -> mark#(X), mark#(head(X)) -> mark#(X), mark#(head(X)) -> active#(head(mark(X))), active#(incr(cons(X, XS))) -> mark#(cons(s(X), incr(XS))), active#(nats()) -> mark#(cons(0(), incr(nats()))), active#(odds()) -> mark#(incr(pairs())), active#(pairs()) -> mark#(cons(0(), incr(odds()))), active#(head(cons(X, XS))) -> mark#(X)} Weak: { mark(cons(X1, X2)) -> active(cons(mark(X1), X2)), mark(0()) -> active(0()), mark(incr(X)) -> active(incr(mark(X))), mark(nats()) -> active(nats()), mark(odds()) -> active(odds()), mark(pairs()) -> active(pairs()), mark(s(X)) -> active(s(mark(X))), mark(head(X)) -> active(head(mark(X))), mark(tail(X)) -> active(tail(mark(X))), 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), incr(mark(X)) -> incr(X), incr(active(X)) -> incr(X), active(incr(cons(X, XS))) -> mark(cons(s(X), incr(XS))), active(nats()) -> mark(cons(0(), incr(nats()))), active(odds()) -> mark(incr(pairs())), active(pairs()) -> mark(cons(0(), incr(odds()))), active(head(cons(X, XS))) -> mark(X), active(tail(cons(X, XS))) -> mark(XS), s(mark(X)) -> s(X), s(active(X)) -> s(X), head(mark(X)) -> head(X), head(active(X)) -> head(X), tail(mark(X)) -> tail(X), tail(active(X)) -> tail(X)} POLY: Argument Filtering: pi(tail) = 0, pi(head) = [0], pi(s) = 0, pi(pairs) = [], pi(odds) = [], pi(active#) = 0, pi(active) = 0, pi(nats) = [], pi(incr) = 0, pi(0) = [], pi(cons) = [0,1], pi(mark#) = 0, pi(mark) = 0 Usable Rules: {} Interpretation: [cons](x0, x1) = x0 + x1, [head](x0) = x0 + 1, [pairs] = 0, [odds] = 0, [nats] = 0, [0] = 0 Strict: { mark#(cons(X1, X2)) -> mark#(X1), mark#(incr(X)) -> mark#(X), mark#(incr(X)) -> active#(incr(mark(X))), mark#(nats()) -> active#(nats()), mark#(odds()) -> active#(odds()), mark#(pairs()) -> active#(pairs()), mark#(s(X)) -> mark#(X), mark#(head(X)) -> active#(head(mark(X))), active#(incr(cons(X, XS))) -> mark#(cons(s(X), incr(XS))), active#(nats()) -> mark#(cons(0(), incr(nats()))), active#(odds()) -> mark#(incr(pairs())), active#(pairs()) -> mark#(cons(0(), incr(odds())))} Weak: { mark(cons(X1, X2)) -> active(cons(mark(X1), X2)), mark(0()) -> active(0()), mark(incr(X)) -> active(incr(mark(X))), mark(nats()) -> active(nats()), mark(odds()) -> active(odds()), mark(pairs()) -> active(pairs()), mark(s(X)) -> active(s(mark(X))), mark(head(X)) -> active(head(mark(X))), mark(tail(X)) -> active(tail(mark(X))), 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), incr(mark(X)) -> incr(X), incr(active(X)) -> incr(X), active(incr(cons(X, XS))) -> mark(cons(s(X), incr(XS))), active(nats()) -> mark(cons(0(), incr(nats()))), active(odds()) -> mark(incr(pairs())), active(pairs()) -> mark(cons(0(), incr(odds()))), active(head(cons(X, XS))) -> mark(X), active(tail(cons(X, XS))) -> mark(XS), s(mark(X)) -> s(X), s(active(X)) -> s(X), head(mark(X)) -> head(X), head(active(X)) -> head(X), tail(mark(X)) -> tail(X), tail(active(X)) -> tail(X)} EDG: {(mark#(head(X)) -> active#(head(mark(X))), active#(incr(cons(X, XS))) -> mark#(cons(s(X), incr(XS)))) (mark#(odds()) -> active#(odds()), active#(odds()) -> mark#(incr(pairs()))) (mark#(incr(X)) -> mark#(X), mark#(head(X)) -> active#(head(mark(X)))) (mark#(incr(X)) -> mark#(X), mark#(s(X)) -> mark#(X)) (mark#(incr(X)) -> mark#(X), mark#(pairs()) -> active#(pairs())) (mark#(incr(X)) -> mark#(X), mark#(odds()) -> active#(odds())) (mark#(incr(X)) -> mark#(X), mark#(nats()) -> active#(nats())) (mark#(incr(X)) -> mark#(X), mark#(incr(X)) -> active#(incr(mark(X)))) (mark#(incr(X)) -> mark#(X), mark#(incr(X)) -> mark#(X)) (mark#(incr(X)) -> mark#(X), mark#(cons(X1, X2)) -> mark#(X1)) (mark#(cons(X1, X2)) -> mark#(X1), mark#(head(X)) -> active#(head(mark(X)))) (mark#(cons(X1, X2)) -> mark#(X1), mark#(s(X)) -> mark#(X)) (mark#(cons(X1, X2)) -> mark#(X1), mark#(pairs()) -> active#(pairs())) (mark#(cons(X1, X2)) -> mark#(X1), mark#(odds()) -> active#(odds())) (mark#(cons(X1, X2)) -> mark#(X1), mark#(nats()) -> active#(nats())) (mark#(cons(X1, X2)) -> mark#(X1), mark#(incr(X)) -> active#(incr(mark(X)))) (mark#(cons(X1, X2)) -> mark#(X1), mark#(incr(X)) -> mark#(X)) (mark#(cons(X1, X2)) -> mark#(X1), mark#(cons(X1, X2)) -> mark#(X1)) (active#(nats()) -> mark#(cons(0(), incr(nats()))), mark#(cons(X1, X2)) -> mark#(X1)) (active#(odds()) -> mark#(incr(pairs())), mark#(incr(X)) -> active#(incr(mark(X)))) (active#(odds()) -> mark#(incr(pairs())), mark#(incr(X)) -> mark#(X)) (active#(pairs()) -> mark#(cons(0(), incr(odds()))), mark#(cons(X1, X2)) -> mark#(X1)) (active#(incr(cons(X, XS))) -> mark#(cons(s(X), incr(XS))), mark#(cons(X1, X2)) -> mark#(X1)) (active#(incr(cons(X, XS))) -> mark#(cons(s(X), incr(XS))), mark#(incr(X)) -> mark#(X)) (active#(incr(cons(X, XS))) -> mark#(cons(s(X), incr(XS))), mark#(incr(X)) -> active#(incr(mark(X)))) (active#(incr(cons(X, XS))) -> mark#(cons(s(X), incr(XS))), mark#(s(X)) -> mark#(X)) (active#(incr(cons(X, XS))) -> mark#(cons(s(X), incr(XS))), mark#(head(X)) -> active#(head(mark(X)))) (mark#(s(X)) -> mark#(X), mark#(cons(X1, X2)) -> mark#(X1)) (mark#(s(X)) -> mark#(X), mark#(incr(X)) -> mark#(X)) (mark#(s(X)) -> mark#(X), mark#(incr(X)) -> active#(incr(mark(X)))) (mark#(s(X)) -> mark#(X), mark#(nats()) -> active#(nats())) (mark#(s(X)) -> mark#(X), mark#(odds()) -> active#(odds())) (mark#(s(X)) -> mark#(X), mark#(pairs()) -> active#(pairs())) (mark#(s(X)) -> mark#(X), mark#(s(X)) -> mark#(X)) (mark#(s(X)) -> mark#(X), mark#(head(X)) -> active#(head(mark(X)))) (mark#(pairs()) -> active#(pairs()), active#(pairs()) -> mark#(cons(0(), incr(odds())))) (mark#(nats()) -> active#(nats()), active#(nats()) -> mark#(cons(0(), incr(nats())))) (mark#(incr(X)) -> active#(incr(mark(X))), active#(incr(cons(X, XS))) -> mark#(cons(s(X), incr(XS))))} SCCS: Scc: { mark#(cons(X1, X2)) -> mark#(X1), mark#(incr(X)) -> mark#(X), mark#(incr(X)) -> active#(incr(mark(X))), mark#(nats()) -> active#(nats()), mark#(odds()) -> active#(odds()), mark#(pairs()) -> active#(pairs()), mark#(s(X)) -> mark#(X), mark#(head(X)) -> active#(head(mark(X))), active#(incr(cons(X, XS))) -> mark#(cons(s(X), incr(XS))), active#(nats()) -> mark#(cons(0(), incr(nats()))), active#(odds()) -> mark#(incr(pairs())), active#(pairs()) -> mark#(cons(0(), incr(odds())))} SCC: Strict: { mark#(cons(X1, X2)) -> mark#(X1), mark#(incr(X)) -> mark#(X), mark#(incr(X)) -> active#(incr(mark(X))), mark#(nats()) -> active#(nats()), mark#(odds()) -> active#(odds()), mark#(pairs()) -> active#(pairs()), mark#(s(X)) -> mark#(X), mark#(head(X)) -> active#(head(mark(X))), active#(incr(cons(X, XS))) -> mark#(cons(s(X), incr(XS))), active#(nats()) -> mark#(cons(0(), incr(nats()))), active#(odds()) -> mark#(incr(pairs())), active#(pairs()) -> mark#(cons(0(), incr(odds())))} Weak: { mark(cons(X1, X2)) -> active(cons(mark(X1), X2)), mark(0()) -> active(0()), mark(incr(X)) -> active(incr(mark(X))), mark(nats()) -> active(nats()), mark(odds()) -> active(odds()), mark(pairs()) -> active(pairs()), mark(s(X)) -> active(s(mark(X))), mark(head(X)) -> active(head(mark(X))), mark(tail(X)) -> active(tail(mark(X))), 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), incr(mark(X)) -> incr(X), incr(active(X)) -> incr(X), active(incr(cons(X, XS))) -> mark(cons(s(X), incr(XS))), active(nats()) -> mark(cons(0(), incr(nats()))), active(odds()) -> mark(incr(pairs())), active(pairs()) -> mark(cons(0(), incr(odds()))), active(head(cons(X, XS))) -> mark(X), active(tail(cons(X, XS))) -> mark(XS), s(mark(X)) -> s(X), s(active(X)) -> s(X), head(mark(X)) -> head(X), head(active(X)) -> head(X), tail(mark(X)) -> tail(X), tail(active(X)) -> tail(X)} POLY: Argument Filtering: pi(tail) = [], pi(head) = [], pi(s) = [], pi(pairs) = [], pi(odds) = [], pi(active#) = 0, pi(active) = [], pi(nats) = [], pi(incr) = [], pi(0) = [], pi(cons) = [], pi(mark#) = [], pi(mark) = [] Usable Rules: {} Interpretation: [mark#] = 1, [head] = 0, [incr] = 1, [pairs] = 1, [odds] = 1, [nats] = 1 Strict: { mark#(cons(X1, X2)) -> mark#(X1), mark#(incr(X)) -> mark#(X), mark#(incr(X)) -> active#(incr(mark(X))), mark#(nats()) -> active#(nats()), mark#(odds()) -> active#(odds()), mark#(pairs()) -> active#(pairs()), mark#(s(X)) -> mark#(X), active#(incr(cons(X, XS))) -> mark#(cons(s(X), incr(XS))), active#(nats()) -> mark#(cons(0(), incr(nats()))), active#(odds()) -> mark#(incr(pairs())), active#(pairs()) -> mark#(cons(0(), incr(odds())))} Weak: { mark(cons(X1, X2)) -> active(cons(mark(X1), X2)), mark(0()) -> active(0()), mark(incr(X)) -> active(incr(mark(X))), mark(nats()) -> active(nats()), mark(odds()) -> active(odds()), mark(pairs()) -> active(pairs()), mark(s(X)) -> active(s(mark(X))), mark(head(X)) -> active(head(mark(X))), mark(tail(X)) -> active(tail(mark(X))), 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), incr(mark(X)) -> incr(X), incr(active(X)) -> incr(X), active(incr(cons(X, XS))) -> mark(cons(s(X), incr(XS))), active(nats()) -> mark(cons(0(), incr(nats()))), active(odds()) -> mark(incr(pairs())), active(pairs()) -> mark(cons(0(), incr(odds()))), active(head(cons(X, XS))) -> mark(X), active(tail(cons(X, XS))) -> mark(XS), s(mark(X)) -> s(X), s(active(X)) -> s(X), head(mark(X)) -> head(X), head(active(X)) -> head(X), tail(mark(X)) -> tail(X), tail(active(X)) -> tail(X)} EDG: {(mark#(s(X)) -> mark#(X), mark#(s(X)) -> mark#(X)) (mark#(s(X)) -> mark#(X), mark#(pairs()) -> active#(pairs())) (mark#(s(X)) -> mark#(X), mark#(odds()) -> active#(odds())) (mark#(s(X)) -> mark#(X), mark#(nats()) -> active#(nats())) (mark#(s(X)) -> mark#(X), mark#(incr(X)) -> active#(incr(mark(X)))) (mark#(s(X)) -> mark#(X), mark#(incr(X)) -> mark#(X)) (mark#(s(X)) -> mark#(X), mark#(cons(X1, X2)) -> mark#(X1)) (mark#(incr(X)) -> active#(incr(mark(X))), active#(incr(cons(X, XS))) -> mark#(cons(s(X), incr(XS)))) (active#(nats()) -> mark#(cons(0(), incr(nats()))), mark#(cons(X1, X2)) -> mark#(X1)) (mark#(nats()) -> active#(nats()), active#(nats()) -> mark#(cons(0(), incr(nats())))) (mark#(pairs()) -> active#(pairs()), active#(pairs()) -> mark#(cons(0(), incr(odds())))) (active#(odds()) -> mark#(incr(pairs())), mark#(incr(X)) -> mark#(X)) (active#(odds()) -> mark#(incr(pairs())), mark#(incr(X)) -> active#(incr(mark(X)))) (mark#(odds()) -> active#(odds()), active#(odds()) -> mark#(incr(pairs()))) (active#(pairs()) -> mark#(cons(0(), incr(odds()))), mark#(cons(X1, X2)) -> mark#(X1)) (active#(incr(cons(X, XS))) -> mark#(cons(s(X), incr(XS))), mark#(cons(X1, X2)) -> mark#(X1)) (active#(incr(cons(X, XS))) -> mark#(cons(s(X), incr(XS))), mark#(incr(X)) -> mark#(X)) (active#(incr(cons(X, XS))) -> mark#(cons(s(X), incr(XS))), mark#(incr(X)) -> active#(incr(mark(X)))) (active#(incr(cons(X, XS))) -> mark#(cons(s(X), incr(XS))), mark#(s(X)) -> mark#(X)) (mark#(cons(X1, X2)) -> mark#(X1), mark#(cons(X1, X2)) -> mark#(X1)) (mark#(cons(X1, X2)) -> mark#(X1), mark#(incr(X)) -> mark#(X)) (mark#(cons(X1, X2)) -> mark#(X1), mark#(incr(X)) -> active#(incr(mark(X)))) (mark#(cons(X1, X2)) -> mark#(X1), mark#(nats()) -> active#(nats())) (mark#(cons(X1, X2)) -> mark#(X1), mark#(odds()) -> active#(odds())) (mark#(cons(X1, X2)) -> mark#(X1), mark#(pairs()) -> active#(pairs())) (mark#(cons(X1, X2)) -> mark#(X1), mark#(s(X)) -> mark#(X)) (mark#(incr(X)) -> mark#(X), mark#(cons(X1, X2)) -> mark#(X1)) (mark#(incr(X)) -> mark#(X), mark#(incr(X)) -> mark#(X)) (mark#(incr(X)) -> mark#(X), mark#(incr(X)) -> active#(incr(mark(X)))) (mark#(incr(X)) -> mark#(X), mark#(nats()) -> active#(nats())) (mark#(incr(X)) -> mark#(X), mark#(odds()) -> active#(odds())) (mark#(incr(X)) -> mark#(X), mark#(pairs()) -> active#(pairs())) (mark#(incr(X)) -> mark#(X), mark#(s(X)) -> mark#(X))} SCCS: Scc: { mark#(cons(X1, X2)) -> mark#(X1), mark#(incr(X)) -> mark#(X), mark#(incr(X)) -> active#(incr(mark(X))), mark#(nats()) -> active#(nats()), mark#(odds()) -> active#(odds()), mark#(pairs()) -> active#(pairs()), mark#(s(X)) -> mark#(X), active#(incr(cons(X, XS))) -> mark#(cons(s(X), incr(XS))), active#(nats()) -> mark#(cons(0(), incr(nats()))), active#(odds()) -> mark#(incr(pairs())), active#(pairs()) -> mark#(cons(0(), incr(odds())))} SCC: Strict: { mark#(cons(X1, X2)) -> mark#(X1), mark#(incr(X)) -> mark#(X), mark#(incr(X)) -> active#(incr(mark(X))), mark#(nats()) -> active#(nats()), mark#(odds()) -> active#(odds()), mark#(pairs()) -> active#(pairs()), mark#(s(X)) -> mark#(X), active#(incr(cons(X, XS))) -> mark#(cons(s(X), incr(XS))), active#(nats()) -> mark#(cons(0(), incr(nats()))), active#(odds()) -> mark#(incr(pairs())), active#(pairs()) -> mark#(cons(0(), incr(odds())))} Weak: { mark(cons(X1, X2)) -> active(cons(mark(X1), X2)), mark(0()) -> active(0()), mark(incr(X)) -> active(incr(mark(X))), mark(nats()) -> active(nats()), mark(odds()) -> active(odds()), mark(pairs()) -> active(pairs()), mark(s(X)) -> active(s(mark(X))), mark(head(X)) -> active(head(mark(X))), mark(tail(X)) -> active(tail(mark(X))), 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), incr(mark(X)) -> incr(X), incr(active(X)) -> incr(X), active(incr(cons(X, XS))) -> mark(cons(s(X), incr(XS))), active(nats()) -> mark(cons(0(), incr(nats()))), active(odds()) -> mark(incr(pairs())), active(pairs()) -> mark(cons(0(), incr(odds()))), active(head(cons(X, XS))) -> mark(X), active(tail(cons(X, XS))) -> mark(XS), s(mark(X)) -> s(X), s(active(X)) -> s(X), head(mark(X)) -> head(X), head(active(X)) -> head(X), tail(mark(X)) -> tail(X), tail(active(X)) -> tail(X)} Fail