MAYBE TRS: { mark(sel(X1, X2)) -> active(sel(mark(X1), mark(X2))), mark(fib1(X1, X2)) -> active(fib1(mark(X1), mark(X2))), mark(s(X)) -> active(s(mark(X))), mark(0()) -> active(0()), mark(fib(X)) -> active(fib(mark(X))), mark(cons(X1, X2)) -> active(cons(mark(X1), X2)), mark(add(X1, X2)) -> active(add(mark(X1), mark(X2))), sel(X1, mark(X2)) -> sel(X1, X2), sel(X1, active(X2)) -> sel(X1, X2), sel(mark(X1), X2) -> sel(X1, X2), sel(active(X1), X2) -> sel(X1, X2), fib1(X1, mark(X2)) -> fib1(X1, X2), fib1(X1, active(X2)) -> fib1(X1, X2), fib1(mark(X1), X2) -> fib1(X1, X2), fib1(active(X1), X2) -> fib1(X1, X2), s(mark(X)) -> s(X), s(active(X)) -> s(X), active(sel(s(N), cons(X, XS))) -> mark(sel(N, XS)), active(sel(0(), cons(X, XS))) -> mark(X), active(fib1(X, Y)) -> mark(cons(X, fib1(Y, add(X, Y)))), active(fib(N)) -> mark(sel(N, fib1(s(0()), s(0())))), active(add(s(X), Y)) -> mark(s(add(X, Y))), active(add(0(), X)) -> mark(X), fib(mark(X)) -> fib(X), fib(active(X)) -> fib(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), 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)} DP: Strict: { mark#(sel(X1, X2)) -> mark#(X1), mark#(sel(X1, X2)) -> mark#(X2), mark#(sel(X1, X2)) -> sel#(mark(X1), mark(X2)), mark#(sel(X1, X2)) -> active#(sel(mark(X1), mark(X2))), mark#(fib1(X1, X2)) -> mark#(X1), mark#(fib1(X1, X2)) -> mark#(X2), mark#(fib1(X1, X2)) -> fib1#(mark(X1), mark(X2)), mark#(fib1(X1, X2)) -> active#(fib1(mark(X1), mark(X2))), mark#(s(X)) -> mark#(X), mark#(s(X)) -> s#(mark(X)), mark#(s(X)) -> active#(s(mark(X))), mark#(0()) -> active#(0()), mark#(fib(X)) -> mark#(X), mark#(fib(X)) -> active#(fib(mark(X))), mark#(fib(X)) -> fib#(mark(X)), mark#(cons(X1, X2)) -> mark#(X1), mark#(cons(X1, X2)) -> active#(cons(mark(X1), X2)), mark#(cons(X1, X2)) -> cons#(mark(X1), X2), 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)), sel#(X1, mark(X2)) -> sel#(X1, X2), sel#(X1, active(X2)) -> sel#(X1, X2), sel#(mark(X1), X2) -> sel#(X1, X2), sel#(active(X1), X2) -> sel#(X1, X2), fib1#(X1, mark(X2)) -> fib1#(X1, X2), fib1#(X1, active(X2)) -> fib1#(X1, X2), fib1#(mark(X1), X2) -> fib1#(X1, X2), fib1#(active(X1), X2) -> fib1#(X1, X2), s#(mark(X)) -> s#(X), s#(active(X)) -> s#(X), active#(sel(s(N), cons(X, XS))) -> mark#(sel(N, XS)), active#(sel(s(N), cons(X, XS))) -> sel#(N, XS), active#(sel(0(), cons(X, XS))) -> mark#(X), active#(fib1(X, Y)) -> mark#(cons(X, fib1(Y, add(X, Y)))), active#(fib1(X, Y)) -> fib1#(Y, add(X, Y)), active#(fib1(X, Y)) -> cons#(X, fib1(Y, add(X, Y))), active#(fib1(X, Y)) -> add#(X, Y), active#(fib(N)) -> mark#(sel(N, fib1(s(0()), s(0())))), active#(fib(N)) -> sel#(N, fib1(s(0()), s(0()))), active#(fib(N)) -> fib1#(s(0()), s(0())), active#(fib(N)) -> s#(0()), 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#(add(0(), X)) -> mark#(X), fib#(mark(X)) -> fib#(X), fib#(active(X)) -> fib#(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), 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(sel(X1, X2)) -> active(sel(mark(X1), mark(X2))), mark(fib1(X1, X2)) -> active(fib1(mark(X1), mark(X2))), mark(s(X)) -> active(s(mark(X))), mark(0()) -> active(0()), mark(fib(X)) -> active(fib(mark(X))), mark(cons(X1, X2)) -> active(cons(mark(X1), X2)), mark(add(X1, X2)) -> active(add(mark(X1), mark(X2))), sel(X1, mark(X2)) -> sel(X1, X2), sel(X1, active(X2)) -> sel(X1, X2), sel(mark(X1), X2) -> sel(X1, X2), sel(active(X1), X2) -> sel(X1, X2), fib1(X1, mark(X2)) -> fib1(X1, X2), fib1(X1, active(X2)) -> fib1(X1, X2), fib1(mark(X1), X2) -> fib1(X1, X2), fib1(active(X1), X2) -> fib1(X1, X2), s(mark(X)) -> s(X), s(active(X)) -> s(X), active(sel(s(N), cons(X, XS))) -> mark(sel(N, XS)), active(sel(0(), cons(X, XS))) -> mark(X), active(fib1(X, Y)) -> mark(cons(X, fib1(Y, add(X, Y)))), active(fib(N)) -> mark(sel(N, fib1(s(0()), s(0())))), active(add(s(X), Y)) -> mark(s(add(X, Y))), active(add(0(), X)) -> mark(X), fib(mark(X)) -> fib(X), fib(active(X)) -> fib(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), 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)} EDG: { (mark#(fib1(X1, X2)) -> fib1#(mark(X1), mark(X2)), fib1#(active(X1), X2) -> fib1#(X1, X2)) (mark#(fib1(X1, X2)) -> fib1#(mark(X1), mark(X2)), fib1#(mark(X1), X2) -> fib1#(X1, X2)) (mark#(fib1(X1, X2)) -> fib1#(mark(X1), mark(X2)), fib1#(X1, active(X2)) -> fib1#(X1, X2)) (mark#(fib1(X1, X2)) -> fib1#(mark(X1), mark(X2)), fib1#(X1, mark(X2)) -> fib1#(X1, X2)) (mark#(s(X)) -> mark#(X), mark#(add(X1, X2)) -> add#(mark(X1), mark(X2))) (mark#(s(X)) -> mark#(X), mark#(add(X1, X2)) -> active#(add(mark(X1), mark(X2)))) (mark#(s(X)) -> mark#(X), mark#(add(X1, X2)) -> mark#(X2)) (mark#(s(X)) -> mark#(X), mark#(add(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#(cons(X1, X2)) -> mark#(X1)) (mark#(s(X)) -> mark#(X), mark#(fib(X)) -> fib#(mark(X))) (mark#(s(X)) -> mark#(X), mark#(fib(X)) -> active#(fib(mark(X)))) (mark#(s(X)) -> mark#(X), mark#(fib(X)) -> mark#(X)) (mark#(s(X)) -> mark#(X), mark#(0()) -> active#(0())) (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#(s(X)) -> mark#(X)) (mark#(s(X)) -> mark#(X), mark#(fib1(X1, X2)) -> active#(fib1(mark(X1), mark(X2)))) (mark#(s(X)) -> mark#(X), mark#(fib1(X1, X2)) -> fib1#(mark(X1), mark(X2))) (mark#(s(X)) -> mark#(X), mark#(fib1(X1, X2)) -> mark#(X2)) (mark#(s(X)) -> mark#(X), mark#(fib1(X1, X2)) -> mark#(X1)) (mark#(s(X)) -> mark#(X), mark#(sel(X1, X2)) -> active#(sel(mark(X1), mark(X2)))) (mark#(s(X)) -> mark#(X), mark#(sel(X1, X2)) -> sel#(mark(X1), mark(X2))) (mark#(s(X)) -> mark#(X), mark#(sel(X1, X2)) -> mark#(X2)) (mark#(s(X)) -> mark#(X), mark#(sel(X1, X2)) -> mark#(X1)) (s#(mark(X)) -> s#(X), s#(active(X)) -> s#(X)) (s#(mark(X)) -> s#(X), s#(mark(X)) -> s#(X)) (active#(sel(0(), cons(X, XS))) -> mark#(X), mark#(add(X1, X2)) -> add#(mark(X1), mark(X2))) (active#(sel(0(), cons(X, XS))) -> mark#(X), mark#(add(X1, X2)) -> active#(add(mark(X1), mark(X2)))) (active#(sel(0(), cons(X, XS))) -> mark#(X), mark#(add(X1, X2)) -> mark#(X2)) (active#(sel(0(), cons(X, XS))) -> mark#(X), mark#(add(X1, X2)) -> mark#(X1)) (active#(sel(0(), cons(X, XS))) -> mark#(X), mark#(cons(X1, X2)) -> cons#(mark(X1), X2)) (active#(sel(0(), cons(X, XS))) -> mark#(X), mark#(cons(X1, X2)) -> active#(cons(mark(X1), X2))) (active#(sel(0(), cons(X, XS))) -> mark#(X), mark#(cons(X1, X2)) -> mark#(X1)) (active#(sel(0(), cons(X, XS))) -> mark#(X), mark#(fib(X)) -> fib#(mark(X))) (active#(sel(0(), cons(X, XS))) -> mark#(X), mark#(fib(X)) -> active#(fib(mark(X)))) (active#(sel(0(), cons(X, XS))) -> mark#(X), mark#(fib(X)) -> mark#(X)) (active#(sel(0(), cons(X, XS))) -> mark#(X), mark#(0()) -> active#(0())) (active#(sel(0(), cons(X, XS))) -> mark#(X), mark#(s(X)) -> active#(s(mark(X)))) (active#(sel(0(), cons(X, XS))) -> mark#(X), mark#(s(X)) -> s#(mark(X))) (active#(sel(0(), cons(X, XS))) -> mark#(X), mark#(s(X)) -> mark#(X)) (active#(sel(0(), cons(X, XS))) -> mark#(X), mark#(fib1(X1, X2)) -> active#(fib1(mark(X1), mark(X2)))) (active#(sel(0(), cons(X, XS))) -> mark#(X), mark#(fib1(X1, X2)) -> fib1#(mark(X1), mark(X2))) (active#(sel(0(), cons(X, XS))) -> mark#(X), mark#(fib1(X1, X2)) -> mark#(X2)) (active#(sel(0(), cons(X, XS))) -> mark#(X), mark#(fib1(X1, X2)) -> mark#(X1)) (active#(sel(0(), cons(X, XS))) -> mark#(X), mark#(sel(X1, X2)) -> active#(sel(mark(X1), mark(X2)))) (active#(sel(0(), cons(X, XS))) -> mark#(X), mark#(sel(X1, X2)) -> sel#(mark(X1), mark(X2))) (active#(sel(0(), cons(X, XS))) -> mark#(X), mark#(sel(X1, X2)) -> mark#(X2)) (active#(sel(0(), cons(X, XS))) -> mark#(X), mark#(sel(X1, X2)) -> mark#(X1)) (fib#(mark(X)) -> fib#(X), fib#(active(X)) -> fib#(X)) (fib#(mark(X)) -> fib#(X), fib#(mark(X)) -> fib#(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)) (mark#(fib1(X1, X2)) -> active#(fib1(mark(X1), mark(X2))), active#(add(0(), X)) -> mark#(X)) (mark#(fib1(X1, X2)) -> active#(fib1(mark(X1), mark(X2))), active#(add(s(X), Y)) -> add#(X, Y)) (mark#(fib1(X1, X2)) -> active#(fib1(mark(X1), mark(X2))), active#(add(s(X), Y)) -> s#(add(X, Y))) (mark#(fib1(X1, X2)) -> active#(fib1(mark(X1), mark(X2))), active#(add(s(X), Y)) -> mark#(s(add(X, Y)))) (mark#(fib1(X1, X2)) -> active#(fib1(mark(X1), mark(X2))), active#(fib(N)) -> s#(0())) (mark#(fib1(X1, X2)) -> active#(fib1(mark(X1), mark(X2))), active#(fib(N)) -> fib1#(s(0()), s(0()))) (mark#(fib1(X1, X2)) -> active#(fib1(mark(X1), mark(X2))), active#(fib(N)) -> sel#(N, fib1(s(0()), s(0())))) (mark#(fib1(X1, X2)) -> active#(fib1(mark(X1), mark(X2))), active#(fib(N)) -> mark#(sel(N, fib1(s(0()), s(0()))))) (mark#(fib1(X1, X2)) -> active#(fib1(mark(X1), mark(X2))), active#(fib1(X, Y)) -> add#(X, Y)) (mark#(fib1(X1, X2)) -> active#(fib1(mark(X1), mark(X2))), active#(fib1(X, Y)) -> cons#(X, fib1(Y, add(X, Y)))) (mark#(fib1(X1, X2)) -> active#(fib1(mark(X1), mark(X2))), active#(fib1(X, Y)) -> fib1#(Y, add(X, Y))) (mark#(fib1(X1, X2)) -> active#(fib1(mark(X1), mark(X2))), active#(fib1(X, Y)) -> mark#(cons(X, fib1(Y, add(X, Y))))) (mark#(fib1(X1, X2)) -> active#(fib1(mark(X1), mark(X2))), active#(sel(0(), cons(X, XS))) -> mark#(X)) (mark#(fib1(X1, X2)) -> active#(fib1(mark(X1), mark(X2))), active#(sel(s(N), cons(X, XS))) -> sel#(N, XS)) (mark#(fib1(X1, X2)) -> active#(fib1(mark(X1), mark(X2))), active#(sel(s(N), cons(X, XS))) -> mark#(sel(N, XS))) (mark#(fib(X)) -> active#(fib(mark(X))), active#(add(0(), X)) -> mark#(X)) (mark#(fib(X)) -> active#(fib(mark(X))), active#(add(s(X), Y)) -> add#(X, Y)) (mark#(fib(X)) -> active#(fib(mark(X))), active#(add(s(X), Y)) -> s#(add(X, Y))) (mark#(fib(X)) -> active#(fib(mark(X))), active#(add(s(X), Y)) -> mark#(s(add(X, Y)))) (mark#(fib(X)) -> active#(fib(mark(X))), active#(fib(N)) -> s#(0())) (mark#(fib(X)) -> active#(fib(mark(X))), active#(fib(N)) -> fib1#(s(0()), s(0()))) (mark#(fib(X)) -> active#(fib(mark(X))), active#(fib(N)) -> sel#(N, fib1(s(0()), s(0())))) (mark#(fib(X)) -> active#(fib(mark(X))), active#(fib(N)) -> mark#(sel(N, fib1(s(0()), s(0()))))) (mark#(fib(X)) -> active#(fib(mark(X))), active#(fib1(X, Y)) -> add#(X, Y)) (mark#(fib(X)) -> active#(fib(mark(X))), active#(fib1(X, Y)) -> cons#(X, fib1(Y, add(X, Y)))) (mark#(fib(X)) -> active#(fib(mark(X))), active#(fib1(X, Y)) -> fib1#(Y, add(X, Y))) (mark#(fib(X)) -> active#(fib(mark(X))), active#(fib1(X, Y)) -> mark#(cons(X, fib1(Y, add(X, Y))))) (mark#(fib(X)) -> active#(fib(mark(X))), active#(sel(0(), cons(X, XS))) -> mark#(X)) (mark#(fib(X)) -> active#(fib(mark(X))), active#(sel(s(N), cons(X, XS))) -> sel#(N, XS)) (mark#(fib(X)) -> active#(fib(mark(X))), active#(sel(s(N), cons(X, XS))) -> mark#(sel(N, XS))) (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#(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#(fib(X)) -> fib#(mark(X))) (active#(add(s(X), Y)) -> mark#(s(add(X, Y))), mark#(fib(X)) -> active#(fib(mark(X)))) (active#(add(s(X), Y)) -> mark#(s(add(X, Y))), mark#(fib(X)) -> mark#(X)) (active#(add(s(X), Y)) -> mark#(s(add(X, Y))), mark#(s(X)) -> active#(s(mark(X)))) (active#(add(s(X), Y)) -> mark#(s(add(X, Y))), mark#(s(X)) -> s#(mark(X))) (active#(add(s(X), Y)) -> mark#(s(add(X, Y))), mark#(s(X)) -> mark#(X)) (active#(add(s(X), Y)) -> mark#(s(add(X, Y))), mark#(fib1(X1, X2)) -> active#(fib1(mark(X1), mark(X2)))) (active#(add(s(X), Y)) -> mark#(s(add(X, Y))), mark#(fib1(X1, X2)) -> fib1#(mark(X1), mark(X2))) (active#(add(s(X), Y)) -> mark#(s(add(X, Y))), mark#(fib1(X1, X2)) -> mark#(X2)) (active#(add(s(X), Y)) -> mark#(s(add(X, Y))), mark#(fib1(X1, X2)) -> mark#(X1)) (active#(add(s(X), Y)) -> mark#(s(add(X, Y))), mark#(sel(X1, X2)) -> active#(sel(mark(X1), mark(X2)))) (active#(add(s(X), Y)) -> mark#(s(add(X, Y))), mark#(sel(X1, X2)) -> sel#(mark(X1), mark(X2))) (active#(add(s(X), Y)) -> mark#(s(add(X, Y))), mark#(sel(X1, X2)) -> mark#(X2)) (active#(add(s(X), Y)) -> mark#(s(add(X, Y))), mark#(sel(X1, X2)) -> mark#(X1)) (sel#(X1, active(X2)) -> sel#(X1, X2), sel#(active(X1), X2) -> sel#(X1, X2)) (sel#(X1, active(X2)) -> sel#(X1, X2), sel#(mark(X1), X2) -> sel#(X1, X2)) (sel#(X1, active(X2)) -> sel#(X1, X2), sel#(X1, active(X2)) -> sel#(X1, X2)) (sel#(X1, active(X2)) -> sel#(X1, X2), sel#(X1, mark(X2)) -> sel#(X1, X2)) (sel#(active(X1), X2) -> sel#(X1, X2), sel#(active(X1), X2) -> sel#(X1, X2)) (sel#(active(X1), X2) -> sel#(X1, X2), sel#(mark(X1), X2) -> sel#(X1, X2)) (sel#(active(X1), X2) -> sel#(X1, X2), sel#(X1, active(X2)) -> sel#(X1, X2)) (sel#(active(X1), X2) -> sel#(X1, X2), sel#(X1, mark(X2)) -> sel#(X1, X2)) (fib1#(X1, active(X2)) -> fib1#(X1, X2), fib1#(active(X1), X2) -> fib1#(X1, X2)) (fib1#(X1, active(X2)) -> fib1#(X1, X2), fib1#(mark(X1), X2) -> fib1#(X1, X2)) (fib1#(X1, active(X2)) -> fib1#(X1, X2), fib1#(X1, active(X2)) -> fib1#(X1, X2)) (fib1#(X1, active(X2)) -> fib1#(X1, X2), fib1#(X1, mark(X2)) -> fib1#(X1, X2)) (fib1#(active(X1), X2) -> fib1#(X1, X2), fib1#(active(X1), X2) -> fib1#(X1, X2)) (fib1#(active(X1), X2) -> fib1#(X1, X2), fib1#(mark(X1), X2) -> fib1#(X1, X2)) (fib1#(active(X1), X2) -> fib1#(X1, X2), fib1#(X1, active(X2)) -> fib1#(X1, X2)) (fib1#(active(X1), X2) -> fib1#(X1, X2), fib1#(X1, mark(X2)) -> fib1#(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)) (add#(X1, active(X2)) -> add#(X1, X2), add#(active(X1), 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#(X1, active(X2)) -> add#(X1, X2)) (add#(X1, active(X2)) -> add#(X1, X2), add#(X1, mark(X2)) -> add#(X1, X2)) (add#(active(X1), X2) -> add#(X1, X2), add#(active(X1), 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#(X1, active(X2)) -> add#(X1, X2)) (add#(active(X1), X2) -> add#(X1, X2), add#(X1, mark(X2)) -> add#(X1, X2)) (active#(sel(s(N), cons(X, XS))) -> mark#(sel(N, XS)), mark#(add(X1, X2)) -> add#(mark(X1), mark(X2))) (active#(sel(s(N), cons(X, XS))) -> mark#(sel(N, XS)), mark#(add(X1, X2)) -> active#(add(mark(X1), mark(X2)))) (active#(sel(s(N), cons(X, XS))) -> mark#(sel(N, XS)), mark#(add(X1, X2)) -> mark#(X2)) (active#(sel(s(N), cons(X, XS))) -> mark#(sel(N, XS)), mark#(add(X1, X2)) -> mark#(X1)) (active#(sel(s(N), cons(X, XS))) -> mark#(sel(N, XS)), mark#(cons(X1, X2)) -> cons#(mark(X1), X2)) (active#(sel(s(N), cons(X, XS))) -> mark#(sel(N, XS)), mark#(cons(X1, X2)) -> active#(cons(mark(X1), X2))) (active#(sel(s(N), cons(X, XS))) -> mark#(sel(N, XS)), mark#(cons(X1, X2)) -> mark#(X1)) (active#(sel(s(N), cons(X, XS))) -> mark#(sel(N, XS)), mark#(fib(X)) -> fib#(mark(X))) (active#(sel(s(N), cons(X, XS))) -> mark#(sel(N, XS)), mark#(fib(X)) -> active#(fib(mark(X)))) (active#(sel(s(N), cons(X, XS))) -> mark#(sel(N, XS)), mark#(fib(X)) -> mark#(X)) (active#(sel(s(N), cons(X, XS))) -> mark#(sel(N, XS)), mark#(s(X)) -> active#(s(mark(X)))) (active#(sel(s(N), cons(X, XS))) -> mark#(sel(N, XS)), mark#(s(X)) -> s#(mark(X))) (active#(sel(s(N), cons(X, XS))) -> mark#(sel(N, XS)), mark#(s(X)) -> mark#(X)) (active#(sel(s(N), cons(X, XS))) -> mark#(sel(N, XS)), mark#(fib1(X1, X2)) -> active#(fib1(mark(X1), mark(X2)))) (active#(sel(s(N), cons(X, XS))) -> mark#(sel(N, XS)), mark#(fib1(X1, X2)) -> fib1#(mark(X1), mark(X2))) (active#(sel(s(N), cons(X, XS))) -> mark#(sel(N, XS)), mark#(fib1(X1, X2)) -> mark#(X2)) (active#(sel(s(N), cons(X, XS))) -> mark#(sel(N, XS)), mark#(fib1(X1, X2)) -> mark#(X1)) (active#(sel(s(N), cons(X, XS))) -> mark#(sel(N, XS)), mark#(sel(X1, X2)) -> active#(sel(mark(X1), mark(X2)))) (active#(sel(s(N), cons(X, XS))) -> mark#(sel(N, XS)), mark#(sel(X1, X2)) -> sel#(mark(X1), mark(X2))) (active#(sel(s(N), cons(X, XS))) -> mark#(sel(N, XS)), mark#(sel(X1, X2)) -> mark#(X2)) (active#(sel(s(N), cons(X, XS))) -> mark#(sel(N, XS)), mark#(sel(X1, X2)) -> mark#(X1)) (mark#(sel(X1, X2)) -> mark#(X2), mark#(add(X1, X2)) -> add#(mark(X1), mark(X2))) (mark#(sel(X1, X2)) -> mark#(X2), mark#(add(X1, X2)) -> active#(add(mark(X1), mark(X2)))) (mark#(sel(X1, X2)) -> mark#(X2), mark#(add(X1, X2)) -> mark#(X2)) (mark#(sel(X1, X2)) -> mark#(X2), mark#(add(X1, X2)) -> mark#(X1)) (mark#(sel(X1, X2)) -> mark#(X2), mark#(cons(X1, X2)) -> cons#(mark(X1), X2)) (mark#(sel(X1, X2)) -> mark#(X2), mark#(cons(X1, X2)) -> active#(cons(mark(X1), X2))) (mark#(sel(X1, X2)) -> mark#(X2), mark#(cons(X1, X2)) -> mark#(X1)) (mark#(sel(X1, X2)) -> mark#(X2), mark#(fib(X)) -> fib#(mark(X))) (mark#(sel(X1, X2)) -> mark#(X2), mark#(fib(X)) -> active#(fib(mark(X)))) (mark#(sel(X1, X2)) -> mark#(X2), mark#(fib(X)) -> mark#(X)) (mark#(sel(X1, X2)) -> mark#(X2), mark#(0()) -> active#(0())) (mark#(sel(X1, X2)) -> mark#(X2), mark#(s(X)) -> active#(s(mark(X)))) (mark#(sel(X1, X2)) -> mark#(X2), mark#(s(X)) -> s#(mark(X))) (mark#(sel(X1, X2)) -> mark#(X2), mark#(s(X)) -> mark#(X)) (mark#(sel(X1, X2)) -> mark#(X2), mark#(fib1(X1, X2)) -> active#(fib1(mark(X1), mark(X2)))) (mark#(sel(X1, X2)) -> mark#(X2), mark#(fib1(X1, X2)) -> fib1#(mark(X1), mark(X2))) (mark#(sel(X1, X2)) -> mark#(X2), mark#(fib1(X1, X2)) -> mark#(X2)) (mark#(sel(X1, X2)) -> mark#(X2), mark#(fib1(X1, X2)) -> mark#(X1)) (mark#(sel(X1, X2)) -> mark#(X2), mark#(sel(X1, X2)) -> active#(sel(mark(X1), mark(X2)))) (mark#(sel(X1, X2)) -> mark#(X2), mark#(sel(X1, X2)) -> sel#(mark(X1), mark(X2))) (mark#(sel(X1, X2)) -> mark#(X2), mark#(sel(X1, X2)) -> mark#(X2)) (mark#(sel(X1, X2)) -> mark#(X2), mark#(sel(X1, X2)) -> mark#(X1)) (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#(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#(fib(X)) -> fib#(mark(X))) (mark#(add(X1, X2)) -> mark#(X2), mark#(fib(X)) -> active#(fib(mark(X)))) (mark#(add(X1, X2)) -> mark#(X2), mark#(fib(X)) -> mark#(X)) (mark#(add(X1, X2)) -> mark#(X2), mark#(0()) -> active#(0())) (mark#(add(X1, X2)) -> mark#(X2), mark#(s(X)) -> active#(s(mark(X)))) (mark#(add(X1, X2)) -> mark#(X2), mark#(s(X)) -> s#(mark(X))) (mark#(add(X1, X2)) -> mark#(X2), mark#(s(X)) -> mark#(X)) (mark#(add(X1, X2)) -> mark#(X2), mark#(fib1(X1, X2)) -> active#(fib1(mark(X1), mark(X2)))) (mark#(add(X1, X2)) -> mark#(X2), mark#(fib1(X1, X2)) -> fib1#(mark(X1), mark(X2))) (mark#(add(X1, X2)) -> mark#(X2), mark#(fib1(X1, X2)) -> mark#(X2)) (mark#(add(X1, X2)) -> mark#(X2), mark#(fib1(X1, X2)) -> mark#(X1)) (mark#(add(X1, X2)) -> mark#(X2), mark#(sel(X1, X2)) -> active#(sel(mark(X1), mark(X2)))) (mark#(add(X1, X2)) -> mark#(X2), mark#(sel(X1, X2)) -> sel#(mark(X1), mark(X2))) (mark#(add(X1, X2)) -> mark#(X2), mark#(sel(X1, X2)) -> mark#(X2)) (mark#(add(X1, X2)) -> mark#(X2), mark#(sel(X1, X2)) -> mark#(X1)) (mark#(fib1(X1, X2)) -> mark#(X1), mark#(add(X1, X2)) -> add#(mark(X1), mark(X2))) (mark#(fib1(X1, X2)) -> mark#(X1), mark#(add(X1, X2)) -> active#(add(mark(X1), mark(X2)))) (mark#(fib1(X1, X2)) -> mark#(X1), mark#(add(X1, X2)) -> mark#(X2)) (mark#(fib1(X1, X2)) -> mark#(X1), mark#(add(X1, X2)) -> mark#(X1)) (mark#(fib1(X1, X2)) -> mark#(X1), mark#(cons(X1, X2)) -> cons#(mark(X1), X2)) (mark#(fib1(X1, X2)) -> mark#(X1), mark#(cons(X1, X2)) -> active#(cons(mark(X1), X2))) (mark#(fib1(X1, X2)) -> mark#(X1), mark#(cons(X1, X2)) -> mark#(X1)) (mark#(fib1(X1, X2)) -> mark#(X1), mark#(fib(X)) -> fib#(mark(X))) (mark#(fib1(X1, X2)) -> mark#(X1), mark#(fib(X)) -> active#(fib(mark(X)))) (mark#(fib1(X1, X2)) -> mark#(X1), mark#(fib(X)) -> mark#(X)) (mark#(fib1(X1, X2)) -> mark#(X1), mark#(0()) -> active#(0())) (mark#(fib1(X1, X2)) -> mark#(X1), mark#(s(X)) -> active#(s(mark(X)))) (mark#(fib1(X1, X2)) -> mark#(X1), mark#(s(X)) -> s#(mark(X))) (mark#(fib1(X1, X2)) -> mark#(X1), mark#(s(X)) -> mark#(X)) (mark#(fib1(X1, X2)) -> mark#(X1), mark#(fib1(X1, X2)) -> active#(fib1(mark(X1), mark(X2)))) (mark#(fib1(X1, X2)) -> mark#(X1), mark#(fib1(X1, X2)) -> fib1#(mark(X1), mark(X2))) (mark#(fib1(X1, X2)) -> mark#(X1), mark#(fib1(X1, X2)) -> mark#(X2)) (mark#(fib1(X1, X2)) -> mark#(X1), mark#(fib1(X1, X2)) -> mark#(X1)) (mark#(fib1(X1, X2)) -> mark#(X1), mark#(sel(X1, X2)) -> active#(sel(mark(X1), mark(X2)))) (mark#(fib1(X1, X2)) -> mark#(X1), mark#(sel(X1, X2)) -> sel#(mark(X1), mark(X2))) (mark#(fib1(X1, X2)) -> mark#(X1), mark#(sel(X1, X2)) -> mark#(X2)) (mark#(fib1(X1, X2)) -> mark#(X1), mark#(sel(X1, X2)) -> mark#(X1)) (mark#(add(X1, X2)) -> mark#(X1), mark#(add(X1, X2)) -> add#(mark(X1), 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)) -> mark#(X2)) (mark#(add(X1, X2)) -> mark#(X1), mark#(add(X1, X2)) -> mark#(X1)) (mark#(add(X1, X2)) -> mark#(X1), mark#(cons(X1, X2)) -> cons#(mark(X1), X2)) (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#(fib(X)) -> fib#(mark(X))) (mark#(add(X1, X2)) -> mark#(X1), mark#(fib(X)) -> active#(fib(mark(X)))) (mark#(add(X1, X2)) -> mark#(X1), mark#(fib(X)) -> mark#(X)) (mark#(add(X1, X2)) -> mark#(X1), mark#(0()) -> active#(0())) (mark#(add(X1, X2)) -> mark#(X1), mark#(s(X)) -> active#(s(mark(X)))) (mark#(add(X1, X2)) -> mark#(X1), mark#(s(X)) -> s#(mark(X))) (mark#(add(X1, X2)) -> mark#(X1), mark#(s(X)) -> mark#(X)) (mark#(add(X1, X2)) -> mark#(X1), mark#(fib1(X1, X2)) -> active#(fib1(mark(X1), mark(X2)))) (mark#(add(X1, X2)) -> mark#(X1), mark#(fib1(X1, X2)) -> fib1#(mark(X1), mark(X2))) (mark#(add(X1, X2)) -> mark#(X1), mark#(fib1(X1, X2)) -> mark#(X2)) (mark#(add(X1, X2)) -> mark#(X1), mark#(fib1(X1, X2)) -> mark#(X1)) (mark#(add(X1, X2)) -> mark#(X1), mark#(sel(X1, X2)) -> active#(sel(mark(X1), mark(X2)))) (mark#(add(X1, X2)) -> mark#(X1), mark#(sel(X1, X2)) -> sel#(mark(X1), mark(X2))) (mark#(add(X1, X2)) -> mark#(X1), mark#(sel(X1, X2)) -> mark#(X2)) (mark#(add(X1, X2)) -> mark#(X1), mark#(sel(X1, X2)) -> mark#(X1)) (active#(fib(N)) -> mark#(sel(N, fib1(s(0()), s(0())))), mark#(add(X1, X2)) -> add#(mark(X1), mark(X2))) (active#(fib(N)) -> mark#(sel(N, fib1(s(0()), s(0())))), mark#(add(X1, X2)) -> active#(add(mark(X1), mark(X2)))) (active#(fib(N)) -> mark#(sel(N, fib1(s(0()), s(0())))), mark#(add(X1, X2)) -> mark#(X2)) (active#(fib(N)) -> mark#(sel(N, fib1(s(0()), s(0())))), mark#(add(X1, X2)) -> mark#(X1)) (active#(fib(N)) -> mark#(sel(N, fib1(s(0()), s(0())))), mark#(cons(X1, X2)) -> cons#(mark(X1), X2)) (active#(fib(N)) -> mark#(sel(N, fib1(s(0()), s(0())))), mark#(cons(X1, X2)) -> active#(cons(mark(X1), X2))) (active#(fib(N)) -> mark#(sel(N, fib1(s(0()), s(0())))), mark#(cons(X1, X2)) -> mark#(X1)) (active#(fib(N)) -> mark#(sel(N, fib1(s(0()), s(0())))), mark#(fib(X)) -> fib#(mark(X))) (active#(fib(N)) -> mark#(sel(N, fib1(s(0()), s(0())))), mark#(fib(X)) -> active#(fib(mark(X)))) (active#(fib(N)) -> mark#(sel(N, fib1(s(0()), s(0())))), mark#(fib(X)) -> mark#(X)) (active#(fib(N)) -> mark#(sel(N, fib1(s(0()), s(0())))), mark#(s(X)) -> active#(s(mark(X)))) (active#(fib(N)) -> mark#(sel(N, fib1(s(0()), s(0())))), mark#(s(X)) -> s#(mark(X))) (active#(fib(N)) -> mark#(sel(N, fib1(s(0()), s(0())))), mark#(s(X)) -> mark#(X)) (active#(fib(N)) -> mark#(sel(N, fib1(s(0()), s(0())))), mark#(fib1(X1, X2)) -> active#(fib1(mark(X1), mark(X2)))) (active#(fib(N)) -> mark#(sel(N, fib1(s(0()), s(0())))), mark#(fib1(X1, X2)) -> fib1#(mark(X1), mark(X2))) (active#(fib(N)) -> mark#(sel(N, fib1(s(0()), s(0())))), mark#(fib1(X1, X2)) -> mark#(X2)) (active#(fib(N)) -> mark#(sel(N, fib1(s(0()), s(0())))), mark#(fib1(X1, X2)) -> mark#(X1)) (active#(fib(N)) -> mark#(sel(N, fib1(s(0()), s(0())))), mark#(sel(X1, X2)) -> active#(sel(mark(X1), mark(X2)))) (active#(fib(N)) -> mark#(sel(N, fib1(s(0()), s(0())))), mark#(sel(X1, X2)) -> sel#(mark(X1), mark(X2))) (active#(fib(N)) -> mark#(sel(N, fib1(s(0()), s(0())))), mark#(sel(X1, X2)) -> mark#(X2)) (active#(fib(N)) -> mark#(sel(N, fib1(s(0()), s(0())))), mark#(sel(X1, X2)) -> mark#(X1)) (active#(fib(N)) -> sel#(N, fib1(s(0()), s(0()))), sel#(active(X1), X2) -> sel#(X1, X2)) (active#(fib(N)) -> sel#(N, fib1(s(0()), s(0()))), sel#(mark(X1), X2) -> sel#(X1, X2)) (mark#(s(X)) -> s#(mark(X)), s#(active(X)) -> s#(X)) (mark#(s(X)) -> s#(mark(X)), s#(mark(X)) -> s#(X)) (active#(fib1(X, Y)) -> fib1#(Y, add(X, Y)), fib1#(active(X1), X2) -> fib1#(X1, X2)) (active#(fib1(X, Y)) -> fib1#(Y, add(X, Y)), fib1#(mark(X1), X2) -> fib1#(X1, X2)) (active#(fib1(X, Y)) -> fib1#(Y, add(X, Y)), fib1#(X1, active(X2)) -> fib1#(X1, X2)) (active#(fib1(X, Y)) -> fib1#(Y, add(X, Y)), fib1#(X1, mark(X2)) -> fib1#(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)) (active#(fib1(X, Y)) -> add#(X, Y), add#(X1, mark(X2)) -> add#(X1, X2)) (active#(fib1(X, Y)) -> add#(X, Y), add#(X1, active(X2)) -> add#(X1, X2)) (active#(fib1(X, Y)) -> add#(X, Y), add#(mark(X1), X2) -> add#(X1, X2)) (active#(fib1(X, Y)) -> add#(X, Y), add#(active(X1), X2) -> add#(X1, X2)) (mark#(fib(X)) -> fib#(mark(X)), fib#(mark(X)) -> fib#(X)) (mark#(fib(X)) -> fib#(mark(X)), fib#(active(X)) -> fib#(X)) (active#(sel(s(N), cons(X, XS))) -> sel#(N, XS), sel#(X1, mark(X2)) -> sel#(X1, X2)) (active#(sel(s(N), cons(X, XS))) -> sel#(N, XS), sel#(X1, active(X2)) -> sel#(X1, X2)) (active#(sel(s(N), cons(X, XS))) -> sel#(N, XS), sel#(mark(X1), X2) -> sel#(X1, X2)) (active#(sel(s(N), cons(X, XS))) -> sel#(N, XS), sel#(active(X1), X2) -> sel#(X1, X2)) (active#(fib1(X, Y)) -> cons#(X, fib1(Y, add(X, Y))), cons#(X1, mark(X2)) -> cons#(X1, X2)) (active#(fib1(X, Y)) -> cons#(X, fib1(Y, add(X, Y))), cons#(X1, active(X2)) -> cons#(X1, X2)) (active#(fib1(X, Y)) -> cons#(X, fib1(Y, add(X, Y))), cons#(mark(X1), X2) -> cons#(X1, X2)) (active#(fib1(X, Y)) -> cons#(X, fib1(Y, add(X, Y))), cons#(active(X1), X2) -> cons#(X1, X2)) (active#(fib1(X, Y)) -> mark#(cons(X, fib1(Y, add(X, Y)))), mark#(sel(X1, X2)) -> mark#(X1)) (active#(fib1(X, Y)) -> mark#(cons(X, fib1(Y, add(X, Y)))), mark#(sel(X1, X2)) -> mark#(X2)) (active#(fib1(X, Y)) -> mark#(cons(X, fib1(Y, add(X, Y)))), mark#(sel(X1, X2)) -> sel#(mark(X1), mark(X2))) (active#(fib1(X, Y)) -> mark#(cons(X, fib1(Y, add(X, Y)))), mark#(sel(X1, X2)) -> active#(sel(mark(X1), mark(X2)))) (active#(fib1(X, Y)) -> mark#(cons(X, fib1(Y, add(X, Y)))), mark#(fib1(X1, X2)) -> mark#(X1)) (active#(fib1(X, Y)) -> mark#(cons(X, fib1(Y, add(X, Y)))), mark#(fib1(X1, X2)) -> mark#(X2)) (active#(fib1(X, Y)) -> mark#(cons(X, fib1(Y, add(X, Y)))), mark#(fib1(X1, X2)) -> fib1#(mark(X1), mark(X2))) (active#(fib1(X, Y)) -> mark#(cons(X, fib1(Y, add(X, Y)))), mark#(fib1(X1, X2)) -> active#(fib1(mark(X1), mark(X2)))) (active#(fib1(X, Y)) -> mark#(cons(X, fib1(Y, add(X, Y)))), mark#(s(X)) -> mark#(X)) (active#(fib1(X, Y)) -> mark#(cons(X, fib1(Y, add(X, Y)))), mark#(s(X)) -> s#(mark(X))) (active#(fib1(X, Y)) -> mark#(cons(X, fib1(Y, add(X, Y)))), mark#(s(X)) -> active#(s(mark(X)))) (active#(fib1(X, Y)) -> mark#(cons(X, fib1(Y, add(X, Y)))), mark#(fib(X)) -> mark#(X)) (active#(fib1(X, Y)) -> mark#(cons(X, fib1(Y, add(X, Y)))), mark#(fib(X)) -> active#(fib(mark(X)))) (active#(fib1(X, Y)) -> mark#(cons(X, fib1(Y, add(X, Y)))), mark#(fib(X)) -> fib#(mark(X))) (active#(fib1(X, Y)) -> mark#(cons(X, fib1(Y, add(X, Y)))), mark#(cons(X1, X2)) -> mark#(X1)) (active#(fib1(X, Y)) -> mark#(cons(X, fib1(Y, add(X, Y)))), mark#(cons(X1, X2)) -> active#(cons(mark(X1), X2))) (active#(fib1(X, Y)) -> mark#(cons(X, fib1(Y, add(X, Y)))), mark#(cons(X1, X2)) -> cons#(mark(X1), X2)) (active#(fib1(X, Y)) -> mark#(cons(X, fib1(Y, add(X, Y)))), mark#(add(X1, X2)) -> mark#(X1)) (active#(fib1(X, Y)) -> mark#(cons(X, fib1(Y, add(X, Y)))), mark#(add(X1, X2)) -> mark#(X2)) (active#(fib1(X, Y)) -> mark#(cons(X, fib1(Y, add(X, Y)))), mark#(add(X1, X2)) -> active#(add(mark(X1), mark(X2)))) (active#(fib1(X, Y)) -> mark#(cons(X, fib1(Y, add(X, Y)))), mark#(add(X1, X2)) -> add#(mark(X1), mark(X2))) (mark#(cons(X1, X2)) -> mark#(X1), mark#(sel(X1, X2)) -> mark#(X1)) (mark#(cons(X1, X2)) -> mark#(X1), mark#(sel(X1, X2)) -> mark#(X2)) (mark#(cons(X1, X2)) -> mark#(X1), mark#(sel(X1, X2)) -> sel#(mark(X1), mark(X2))) (mark#(cons(X1, X2)) -> mark#(X1), mark#(sel(X1, X2)) -> active#(sel(mark(X1), mark(X2)))) (mark#(cons(X1, X2)) -> mark#(X1), mark#(fib1(X1, X2)) -> mark#(X1)) (mark#(cons(X1, X2)) -> mark#(X1), mark#(fib1(X1, X2)) -> mark#(X2)) (mark#(cons(X1, X2)) -> mark#(X1), mark#(fib1(X1, X2)) -> fib1#(mark(X1), mark(X2))) (mark#(cons(X1, X2)) -> mark#(X1), mark#(fib1(X1, X2)) -> active#(fib1(mark(X1), mark(X2)))) (mark#(cons(X1, X2)) -> mark#(X1), mark#(s(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#(0()) -> active#(0())) (mark#(cons(X1, X2)) -> mark#(X1), mark#(fib(X)) -> mark#(X)) (mark#(cons(X1, X2)) -> mark#(X1), mark#(fib(X)) -> active#(fib(mark(X)))) (mark#(cons(X1, X2)) -> mark#(X1), mark#(fib(X)) -> fib#(mark(X))) (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#(cons(X1, X2)) -> cons#(mark(X1), X2)) (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#(add(X1, X2)) -> add#(mark(X1), mark(X2))) (mark#(sel(X1, X2)) -> mark#(X1), mark#(sel(X1, X2)) -> mark#(X1)) (mark#(sel(X1, X2)) -> mark#(X1), mark#(sel(X1, X2)) -> mark#(X2)) (mark#(sel(X1, X2)) -> mark#(X1), mark#(sel(X1, X2)) -> sel#(mark(X1), mark(X2))) (mark#(sel(X1, X2)) -> mark#(X1), mark#(sel(X1, X2)) -> active#(sel(mark(X1), mark(X2)))) (mark#(sel(X1, X2)) -> mark#(X1), mark#(fib1(X1, X2)) -> mark#(X1)) (mark#(sel(X1, X2)) -> mark#(X1), mark#(fib1(X1, X2)) -> mark#(X2)) (mark#(sel(X1, X2)) -> mark#(X1), mark#(fib1(X1, X2)) -> fib1#(mark(X1), mark(X2))) (mark#(sel(X1, X2)) -> mark#(X1), mark#(fib1(X1, X2)) -> active#(fib1(mark(X1), mark(X2)))) (mark#(sel(X1, X2)) -> mark#(X1), mark#(s(X)) -> mark#(X)) (mark#(sel(X1, X2)) -> mark#(X1), mark#(s(X)) -> s#(mark(X))) (mark#(sel(X1, X2)) -> mark#(X1), mark#(s(X)) -> active#(s(mark(X)))) (mark#(sel(X1, X2)) -> mark#(X1), mark#(0()) -> active#(0())) (mark#(sel(X1, X2)) -> mark#(X1), mark#(fib(X)) -> mark#(X)) (mark#(sel(X1, X2)) -> mark#(X1), mark#(fib(X)) -> active#(fib(mark(X)))) (mark#(sel(X1, X2)) -> mark#(X1), mark#(fib(X)) -> fib#(mark(X))) (mark#(sel(X1, X2)) -> mark#(X1), mark#(cons(X1, X2)) -> mark#(X1)) (mark#(sel(X1, X2)) -> mark#(X1), mark#(cons(X1, X2)) -> active#(cons(mark(X1), X2))) (mark#(sel(X1, X2)) -> mark#(X1), mark#(cons(X1, X2)) -> cons#(mark(X1), X2)) (mark#(sel(X1, X2)) -> mark#(X1), mark#(add(X1, X2)) -> mark#(X1)) (mark#(sel(X1, X2)) -> mark#(X1), mark#(add(X1, X2)) -> mark#(X2)) (mark#(sel(X1, X2)) -> mark#(X1), mark#(add(X1, X2)) -> active#(add(mark(X1), mark(X2)))) (mark#(sel(X1, X2)) -> mark#(X1), mark#(add(X1, X2)) -> add#(mark(X1), mark(X2))) (mark#(fib1(X1, X2)) -> mark#(X2), mark#(sel(X1, X2)) -> mark#(X1)) (mark#(fib1(X1, X2)) -> mark#(X2), mark#(sel(X1, X2)) -> mark#(X2)) (mark#(fib1(X1, X2)) -> mark#(X2), mark#(sel(X1, X2)) -> sel#(mark(X1), mark(X2))) (mark#(fib1(X1, X2)) -> mark#(X2), mark#(sel(X1, X2)) -> active#(sel(mark(X1), mark(X2)))) (mark#(fib1(X1, X2)) -> mark#(X2), mark#(fib1(X1, X2)) -> mark#(X1)) (mark#(fib1(X1, X2)) -> mark#(X2), mark#(fib1(X1, X2)) -> mark#(X2)) (mark#(fib1(X1, X2)) -> mark#(X2), mark#(fib1(X1, X2)) -> fib1#(mark(X1), mark(X2))) (mark#(fib1(X1, X2)) -> mark#(X2), mark#(fib1(X1, X2)) -> active#(fib1(mark(X1), mark(X2)))) (mark#(fib1(X1, X2)) -> mark#(X2), mark#(s(X)) -> mark#(X)) (mark#(fib1(X1, X2)) -> mark#(X2), mark#(s(X)) -> s#(mark(X))) (mark#(fib1(X1, X2)) -> mark#(X2), mark#(s(X)) -> active#(s(mark(X)))) (mark#(fib1(X1, X2)) -> mark#(X2), mark#(0()) -> active#(0())) (mark#(fib1(X1, X2)) -> mark#(X2), mark#(fib(X)) -> mark#(X)) (mark#(fib1(X1, X2)) -> mark#(X2), mark#(fib(X)) -> active#(fib(mark(X)))) (mark#(fib1(X1, X2)) -> mark#(X2), mark#(fib(X)) -> fib#(mark(X))) (mark#(fib1(X1, X2)) -> mark#(X2), mark#(cons(X1, X2)) -> mark#(X1)) (mark#(fib1(X1, X2)) -> mark#(X2), mark#(cons(X1, X2)) -> active#(cons(mark(X1), X2))) (mark#(fib1(X1, X2)) -> mark#(X2), mark#(cons(X1, X2)) -> cons#(mark(X1), X2)) (mark#(fib1(X1, X2)) -> mark#(X2), mark#(add(X1, X2)) -> mark#(X1)) (mark#(fib1(X1, X2)) -> mark#(X2), mark#(add(X1, X2)) -> mark#(X2)) (mark#(fib1(X1, X2)) -> mark#(X2), mark#(add(X1, X2)) -> active#(add(mark(X1), mark(X2)))) (mark#(fib1(X1, X2)) -> mark#(X2), mark#(add(X1, X2)) -> add#(mark(X1), mark(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)) (mark#(cons(X1, X2)) -> active#(cons(mark(X1), X2)), active#(sel(s(N), cons(X, XS))) -> mark#(sel(N, XS))) (mark#(cons(X1, X2)) -> active#(cons(mark(X1), X2)), active#(sel(s(N), cons(X, XS))) -> sel#(N, XS)) (mark#(cons(X1, X2)) -> active#(cons(mark(X1), X2)), active#(sel(0(), cons(X, XS))) -> mark#(X)) (mark#(cons(X1, X2)) -> active#(cons(mark(X1), X2)), active#(fib1(X, Y)) -> mark#(cons(X, fib1(Y, add(X, Y))))) (mark#(cons(X1, X2)) -> active#(cons(mark(X1), X2)), active#(fib1(X, Y)) -> fib1#(Y, add(X, Y))) (mark#(cons(X1, X2)) -> active#(cons(mark(X1), X2)), active#(fib1(X, Y)) -> cons#(X, fib1(Y, add(X, Y)))) (mark#(cons(X1, X2)) -> active#(cons(mark(X1), X2)), active#(fib1(X, Y)) -> add#(X, Y)) (mark#(cons(X1, X2)) -> active#(cons(mark(X1), X2)), active#(fib(N)) -> mark#(sel(N, fib1(s(0()), s(0()))))) (mark#(cons(X1, X2)) -> active#(cons(mark(X1), X2)), active#(fib(N)) -> sel#(N, fib1(s(0()), s(0())))) (mark#(cons(X1, X2)) -> active#(cons(mark(X1), X2)), active#(fib(N)) -> fib1#(s(0()), s(0()))) (mark#(cons(X1, X2)) -> active#(cons(mark(X1), X2)), active#(fib(N)) -> s#(0())) (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(s(X), Y)) -> s#(add(X, Y))) (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(0(), X)) -> mark#(X)) (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#(mark(X1), X2) -> add#(X1, X2), add#(active(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)) (add#(X1, mark(X2)) -> add#(X1, X2), add#(active(X1), X2) -> add#(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#(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)) (fib1#(mark(X1), X2) -> fib1#(X1, X2), fib1#(X1, mark(X2)) -> fib1#(X1, X2)) (fib1#(mark(X1), X2) -> fib1#(X1, X2), fib1#(X1, active(X2)) -> fib1#(X1, X2)) (fib1#(mark(X1), X2) -> fib1#(X1, X2), fib1#(mark(X1), X2) -> fib1#(X1, X2)) (fib1#(mark(X1), X2) -> fib1#(X1, X2), fib1#(active(X1), X2) -> fib1#(X1, X2)) (fib1#(X1, mark(X2)) -> fib1#(X1, X2), fib1#(X1, mark(X2)) -> fib1#(X1, X2)) (fib1#(X1, mark(X2)) -> fib1#(X1, X2), fib1#(X1, active(X2)) -> fib1#(X1, X2)) (fib1#(X1, mark(X2)) -> fib1#(X1, X2), fib1#(mark(X1), X2) -> fib1#(X1, X2)) (fib1#(X1, mark(X2)) -> fib1#(X1, X2), fib1#(active(X1), X2) -> fib1#(X1, X2)) (sel#(mark(X1), X2) -> sel#(X1, X2), sel#(X1, mark(X2)) -> sel#(X1, X2)) (sel#(mark(X1), X2) -> sel#(X1, X2), sel#(X1, active(X2)) -> sel#(X1, X2)) (sel#(mark(X1), X2) -> sel#(X1, X2), sel#(mark(X1), X2) -> sel#(X1, X2)) (sel#(mark(X1), X2) -> sel#(X1, X2), sel#(active(X1), X2) -> sel#(X1, X2)) (sel#(X1, mark(X2)) -> sel#(X1, X2), sel#(X1, mark(X2)) -> sel#(X1, X2)) (sel#(X1, mark(X2)) -> sel#(X1, X2), sel#(X1, active(X2)) -> sel#(X1, X2)) (sel#(X1, mark(X2)) -> sel#(X1, X2), sel#(mark(X1), X2) -> sel#(X1, X2)) (sel#(X1, mark(X2)) -> sel#(X1, X2), sel#(active(X1), X2) -> sel#(X1, X2)) (mark#(add(X1, X2)) -> active#(add(mark(X1), mark(X2))), active#(sel(s(N), cons(X, XS))) -> mark#(sel(N, XS))) (mark#(add(X1, X2)) -> active#(add(mark(X1), mark(X2))), active#(sel(s(N), cons(X, XS))) -> sel#(N, XS)) (mark#(add(X1, X2)) -> active#(add(mark(X1), mark(X2))), active#(sel(0(), cons(X, XS))) -> mark#(X)) (mark#(add(X1, X2)) -> active#(add(mark(X1), mark(X2))), active#(fib1(X, Y)) -> mark#(cons(X, fib1(Y, add(X, Y))))) (mark#(add(X1, X2)) -> active#(add(mark(X1), mark(X2))), active#(fib1(X, Y)) -> fib1#(Y, add(X, Y))) (mark#(add(X1, X2)) -> active#(add(mark(X1), mark(X2))), active#(fib1(X, Y)) -> cons#(X, fib1(Y, add(X, Y)))) (mark#(add(X1, X2)) -> active#(add(mark(X1), mark(X2))), active#(fib1(X, Y)) -> add#(X, Y)) (mark#(add(X1, X2)) -> active#(add(mark(X1), mark(X2))), active#(fib(N)) -> mark#(sel(N, fib1(s(0()), s(0()))))) (mark#(add(X1, X2)) -> active#(add(mark(X1), mark(X2))), active#(fib(N)) -> sel#(N, fib1(s(0()), s(0())))) (mark#(add(X1, X2)) -> active#(add(mark(X1), mark(X2))), active#(fib(N)) -> fib1#(s(0()), s(0()))) (mark#(add(X1, X2)) -> active#(add(mark(X1), mark(X2))), active#(fib(N)) -> s#(0())) (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#(add(0(), X)) -> mark#(X)) (mark#(s(X)) -> active#(s(mark(X))), active#(sel(s(N), cons(X, XS))) -> mark#(sel(N, XS))) (mark#(s(X)) -> active#(s(mark(X))), active#(sel(s(N), cons(X, XS))) -> sel#(N, XS)) (mark#(s(X)) -> active#(s(mark(X))), active#(sel(0(), cons(X, XS))) -> mark#(X)) (mark#(s(X)) -> active#(s(mark(X))), active#(fib1(X, Y)) -> mark#(cons(X, fib1(Y, add(X, Y))))) (mark#(s(X)) -> active#(s(mark(X))), active#(fib1(X, Y)) -> fib1#(Y, add(X, Y))) (mark#(s(X)) -> active#(s(mark(X))), active#(fib1(X, Y)) -> cons#(X, fib1(Y, add(X, Y)))) (mark#(s(X)) -> active#(s(mark(X))), active#(fib1(X, Y)) -> add#(X, Y)) (mark#(s(X)) -> active#(s(mark(X))), active#(fib(N)) -> mark#(sel(N, fib1(s(0()), s(0()))))) (mark#(s(X)) -> active#(s(mark(X))), active#(fib(N)) -> sel#(N, fib1(s(0()), s(0())))) (mark#(s(X)) -> active#(s(mark(X))), active#(fib(N)) -> fib1#(s(0()), s(0()))) (mark#(s(X)) -> active#(s(mark(X))), active#(fib(N)) -> s#(0())) (mark#(s(X)) -> active#(s(mark(X))), active#(add(s(X), Y)) -> mark#(s(add(X, Y)))) (mark#(s(X)) -> active#(s(mark(X))), active#(add(s(X), Y)) -> s#(add(X, Y))) (mark#(s(X)) -> active#(s(mark(X))), active#(add(s(X), Y)) -> add#(X, Y)) (mark#(s(X)) -> active#(s(mark(X))), active#(add(0(), X)) -> mark#(X)) (mark#(sel(X1, X2)) -> active#(sel(mark(X1), mark(X2))), active#(sel(s(N), cons(X, XS))) -> mark#(sel(N, XS))) (mark#(sel(X1, X2)) -> active#(sel(mark(X1), mark(X2))), active#(sel(s(N), cons(X, XS))) -> sel#(N, XS)) (mark#(sel(X1, X2)) -> active#(sel(mark(X1), mark(X2))), active#(sel(0(), cons(X, XS))) -> mark#(X)) (mark#(sel(X1, X2)) -> active#(sel(mark(X1), mark(X2))), active#(fib1(X, Y)) -> mark#(cons(X, fib1(Y, add(X, Y))))) (mark#(sel(X1, X2)) -> active#(sel(mark(X1), mark(X2))), active#(fib1(X, Y)) -> fib1#(Y, add(X, Y))) (mark#(sel(X1, X2)) -> active#(sel(mark(X1), mark(X2))), active#(fib1(X, Y)) -> cons#(X, fib1(Y, add(X, Y)))) (mark#(sel(X1, X2)) -> active#(sel(mark(X1), mark(X2))), active#(fib1(X, Y)) -> add#(X, Y)) (mark#(sel(X1, X2)) -> active#(sel(mark(X1), mark(X2))), active#(fib(N)) -> mark#(sel(N, fib1(s(0()), s(0()))))) (mark#(sel(X1, X2)) -> active#(sel(mark(X1), mark(X2))), active#(fib(N)) -> sel#(N, fib1(s(0()), s(0())))) (mark#(sel(X1, X2)) -> active#(sel(mark(X1), mark(X2))), active#(fib(N)) -> fib1#(s(0()), s(0()))) (mark#(sel(X1, X2)) -> active#(sel(mark(X1), mark(X2))), active#(fib(N)) -> s#(0())) (mark#(sel(X1, X2)) -> active#(sel(mark(X1), mark(X2))), active#(add(s(X), Y)) -> mark#(s(add(X, Y)))) (mark#(sel(X1, X2)) -> active#(sel(mark(X1), mark(X2))), active#(add(s(X), Y)) -> s#(add(X, Y))) (mark#(sel(X1, X2)) -> active#(sel(mark(X1), mark(X2))), active#(add(s(X), Y)) -> add#(X, Y)) (mark#(sel(X1, X2)) -> active#(sel(mark(X1), mark(X2))), active#(add(0(), X)) -> mark#(X)) (fib#(active(X)) -> fib#(X), fib#(mark(X)) -> fib#(X)) (fib#(active(X)) -> fib#(X), fib#(active(X)) -> fib#(X)) (active#(add(0(), X)) -> mark#(X), mark#(sel(X1, X2)) -> mark#(X1)) (active#(add(0(), X)) -> mark#(X), mark#(sel(X1, X2)) -> mark#(X2)) (active#(add(0(), X)) -> mark#(X), mark#(sel(X1, X2)) -> sel#(mark(X1), mark(X2))) (active#(add(0(), X)) -> mark#(X), mark#(sel(X1, X2)) -> active#(sel(mark(X1), mark(X2)))) (active#(add(0(), X)) -> mark#(X), mark#(fib1(X1, X2)) -> mark#(X1)) (active#(add(0(), X)) -> mark#(X), mark#(fib1(X1, X2)) -> mark#(X2)) (active#(add(0(), X)) -> mark#(X), mark#(fib1(X1, X2)) -> fib1#(mark(X1), mark(X2))) (active#(add(0(), X)) -> mark#(X), mark#(fib1(X1, X2)) -> active#(fib1(mark(X1), mark(X2)))) (active#(add(0(), X)) -> mark#(X), mark#(s(X)) -> mark#(X)) (active#(add(0(), X)) -> mark#(X), mark#(s(X)) -> s#(mark(X))) (active#(add(0(), X)) -> mark#(X), mark#(s(X)) -> active#(s(mark(X)))) (active#(add(0(), X)) -> mark#(X), mark#(0()) -> active#(0())) (active#(add(0(), X)) -> mark#(X), mark#(fib(X)) -> mark#(X)) (active#(add(0(), X)) -> mark#(X), mark#(fib(X)) -> active#(fib(mark(X)))) (active#(add(0(), X)) -> mark#(X), mark#(fib(X)) -> fib#(mark(X))) (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#(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))) (s#(active(X)) -> s#(X), s#(mark(X)) -> s#(X)) (s#(active(X)) -> s#(X), s#(active(X)) -> s#(X)) (mark#(fib(X)) -> mark#(X), mark#(sel(X1, X2)) -> mark#(X1)) (mark#(fib(X)) -> mark#(X), mark#(sel(X1, X2)) -> mark#(X2)) (mark#(fib(X)) -> mark#(X), mark#(sel(X1, X2)) -> sel#(mark(X1), mark(X2))) (mark#(fib(X)) -> mark#(X), mark#(sel(X1, X2)) -> active#(sel(mark(X1), mark(X2)))) (mark#(fib(X)) -> mark#(X), mark#(fib1(X1, X2)) -> mark#(X1)) (mark#(fib(X)) -> mark#(X), mark#(fib1(X1, X2)) -> mark#(X2)) (mark#(fib(X)) -> mark#(X), mark#(fib1(X1, X2)) -> fib1#(mark(X1), mark(X2))) (mark#(fib(X)) -> mark#(X), mark#(fib1(X1, X2)) -> active#(fib1(mark(X1), mark(X2)))) (mark#(fib(X)) -> mark#(X), mark#(s(X)) -> mark#(X)) (mark#(fib(X)) -> mark#(X), mark#(s(X)) -> s#(mark(X))) (mark#(fib(X)) -> mark#(X), mark#(s(X)) -> active#(s(mark(X)))) (mark#(fib(X)) -> mark#(X), mark#(0()) -> active#(0())) (mark#(fib(X)) -> mark#(X), mark#(fib(X)) -> mark#(X)) (mark#(fib(X)) -> mark#(X), mark#(fib(X)) -> active#(fib(mark(X)))) (mark#(fib(X)) -> mark#(X), mark#(fib(X)) -> fib#(mark(X))) (mark#(fib(X)) -> mark#(X), mark#(cons(X1, X2)) -> mark#(X1)) (mark#(fib(X)) -> mark#(X), mark#(cons(X1, X2)) -> active#(cons(mark(X1), X2))) (mark#(fib(X)) -> mark#(X), mark#(cons(X1, X2)) -> cons#(mark(X1), X2)) (mark#(fib(X)) -> mark#(X), mark#(add(X1, X2)) -> mark#(X1)) (mark#(fib(X)) -> mark#(X), mark#(add(X1, X2)) -> mark#(X2)) (mark#(fib(X)) -> mark#(X), mark#(add(X1, X2)) -> active#(add(mark(X1), mark(X2)))) (mark#(fib(X)) -> mark#(X), mark#(add(X1, X2)) -> add#(mark(X1), mark(X2))) (mark#(add(X1, X2)) -> add#(mark(X1), mark(X2)), add#(X1, mark(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#(mark(X1), X2) -> add#(X1, X2)) (mark#(add(X1, X2)) -> add#(mark(X1), mark(X2)), add#(active(X1), X2) -> add#(X1, X2)) (mark#(sel(X1, X2)) -> sel#(mark(X1), mark(X2)), sel#(X1, mark(X2)) -> sel#(X1, X2)) (mark#(sel(X1, X2)) -> sel#(mark(X1), mark(X2)), sel#(X1, active(X2)) -> sel#(X1, X2)) (mark#(sel(X1, X2)) -> sel#(mark(X1), mark(X2)), sel#(mark(X1), X2) -> sel#(X1, X2)) (mark#(sel(X1, X2)) -> sel#(mark(X1), mark(X2)), sel#(active(X1), X2) -> sel#(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), add#(active(X1), X2) -> add#(X1, X2)} 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: { fib#(mark(X)) -> fib#(X), fib#(active(X)) -> fib#(X)} Scc: { s#(mark(X)) -> s#(X), s#(active(X)) -> s#(X)} Scc: { fib1#(X1, mark(X2)) -> fib1#(X1, X2), fib1#(X1, active(X2)) -> fib1#(X1, X2), fib1#(mark(X1), X2) -> fib1#(X1, X2), fib1#(active(X1), X2) -> fib1#(X1, X2)} Scc: { sel#(X1, mark(X2)) -> sel#(X1, X2), sel#(X1, active(X2)) -> sel#(X1, X2), sel#(mark(X1), X2) -> sel#(X1, X2), sel#(active(X1), X2) -> sel#(X1, X2)} Scc: { mark#(sel(X1, X2)) -> mark#(X1), mark#(sel(X1, X2)) -> mark#(X2), mark#(sel(X1, X2)) -> active#(sel(mark(X1), mark(X2))), mark#(fib1(X1, X2)) -> mark#(X1), mark#(fib1(X1, X2)) -> mark#(X2), mark#(fib1(X1, X2)) -> active#(fib1(mark(X1), mark(X2))), mark#(s(X)) -> mark#(X), mark#(s(X)) -> active#(s(mark(X))), mark#(fib(X)) -> mark#(X), mark#(fib(X)) -> active#(fib(mark(X))), mark#(cons(X1, X2)) -> mark#(X1), mark#(cons(X1, X2)) -> active#(cons(mark(X1), X2)), mark#(add(X1, X2)) -> mark#(X1), mark#(add(X1, X2)) -> mark#(X2), mark#(add(X1, X2)) -> active#(add(mark(X1), mark(X2))), active#(sel(s(N), cons(X, XS))) -> mark#(sel(N, XS)), active#(sel(0(), cons(X, XS))) -> mark#(X), active#(fib1(X, Y)) -> mark#(cons(X, fib1(Y, add(X, Y)))), active#(fib(N)) -> mark#(sel(N, fib1(s(0()), s(0())))), active#(add(s(X), Y)) -> mark#(s(add(X, Y))), active#(add(0(), X)) -> mark#(X)} 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(sel(X1, X2)) -> active(sel(mark(X1), mark(X2))), mark(fib1(X1, X2)) -> active(fib1(mark(X1), mark(X2))), mark(s(X)) -> active(s(mark(X))), mark(0()) -> active(0()), mark(fib(X)) -> active(fib(mark(X))), mark(cons(X1, X2)) -> active(cons(mark(X1), X2)), mark(add(X1, X2)) -> active(add(mark(X1), mark(X2))), sel(X1, mark(X2)) -> sel(X1, X2), sel(X1, active(X2)) -> sel(X1, X2), sel(mark(X1), X2) -> sel(X1, X2), sel(active(X1), X2) -> sel(X1, X2), fib1(X1, mark(X2)) -> fib1(X1, X2), fib1(X1, active(X2)) -> fib1(X1, X2), fib1(mark(X1), X2) -> fib1(X1, X2), fib1(active(X1), X2) -> fib1(X1, X2), s(mark(X)) -> s(X), s(active(X)) -> s(X), active(sel(s(N), cons(X, XS))) -> mark(sel(N, XS)), active(sel(0(), cons(X, XS))) -> mark(X), active(fib1(X, Y)) -> mark(cons(X, fib1(Y, add(X, Y)))), active(fib(N)) -> mark(sel(N, fib1(s(0()), s(0())))), active(add(s(X), Y)) -> mark(s(add(X, Y))), active(add(0(), X)) -> mark(X), fib(mark(X)) -> fib(X), fib(active(X)) -> fib(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), 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)} 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(sel(X1, X2)) -> active(sel(mark(X1), mark(X2))), mark(fib1(X1, X2)) -> active(fib1(mark(X1), mark(X2))), mark(s(X)) -> active(s(mark(X))), mark(0()) -> active(0()), mark(fib(X)) -> active(fib(mark(X))), mark(cons(X1, X2)) -> active(cons(mark(X1), X2)), mark(add(X1, X2)) -> active(add(mark(X1), mark(X2))), sel(X1, mark(X2)) -> sel(X1, X2), sel(X1, active(X2)) -> sel(X1, X2), sel(mark(X1), X2) -> sel(X1, X2), sel(active(X1), X2) -> sel(X1, X2), fib1(X1, mark(X2)) -> fib1(X1, X2), fib1(X1, active(X2)) -> fib1(X1, X2), fib1(mark(X1), X2) -> fib1(X1, X2), fib1(active(X1), X2) -> fib1(X1, X2), s(mark(X)) -> s(X), s(active(X)) -> s(X), active(sel(s(N), cons(X, XS))) -> mark(sel(N, XS)), active(sel(0(), cons(X, XS))) -> mark(X), active(fib1(X, Y)) -> mark(cons(X, fib1(Y, add(X, Y)))), active(fib(N)) -> mark(sel(N, fib1(s(0()), s(0())))), active(add(s(X), Y)) -> mark(s(add(X, Y))), active(add(0(), X)) -> mark(X), fib(mark(X)) -> fib(X), fib(active(X)) -> fib(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), 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)} 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(sel(X1, X2)) -> active(sel(mark(X1), mark(X2))), mark(fib1(X1, X2)) -> active(fib1(mark(X1), mark(X2))), mark(s(X)) -> active(s(mark(X))), mark(0()) -> active(0()), mark(fib(X)) -> active(fib(mark(X))), mark(cons(X1, X2)) -> active(cons(mark(X1), X2)), mark(add(X1, X2)) -> active(add(mark(X1), mark(X2))), sel(X1, mark(X2)) -> sel(X1, X2), sel(X1, active(X2)) -> sel(X1, X2), sel(mark(X1), X2) -> sel(X1, X2), sel(active(X1), X2) -> sel(X1, X2), fib1(X1, mark(X2)) -> fib1(X1, X2), fib1(X1, active(X2)) -> fib1(X1, X2), fib1(mark(X1), X2) -> fib1(X1, X2), fib1(active(X1), X2) -> fib1(X1, X2), s(mark(X)) -> s(X), s(active(X)) -> s(X), active(sel(s(N), cons(X, XS))) -> mark(sel(N, XS)), active(sel(0(), cons(X, XS))) -> mark(X), active(fib1(X, Y)) -> mark(cons(X, fib1(Y, add(X, Y)))), active(fib(N)) -> mark(sel(N, fib1(s(0()), s(0())))), active(add(s(X), Y)) -> mark(s(add(X, Y))), active(add(0(), X)) -> mark(X), fib(mark(X)) -> fib(X), fib(active(X)) -> fib(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), 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)} 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(sel(X1, X2)) -> active(sel(mark(X1), mark(X2))), mark(fib1(X1, X2)) -> active(fib1(mark(X1), mark(X2))), mark(s(X)) -> active(s(mark(X))), mark(0()) -> active(0()), mark(fib(X)) -> active(fib(mark(X))), mark(cons(X1, X2)) -> active(cons(mark(X1), X2)), mark(add(X1, X2)) -> active(add(mark(X1), mark(X2))), sel(X1, mark(X2)) -> sel(X1, X2), sel(X1, active(X2)) -> sel(X1, X2), sel(mark(X1), X2) -> sel(X1, X2), sel(active(X1), X2) -> sel(X1, X2), fib1(X1, mark(X2)) -> fib1(X1, X2), fib1(X1, active(X2)) -> fib1(X1, X2), fib1(mark(X1), X2) -> fib1(X1, X2), fib1(active(X1), X2) -> fib1(X1, X2), s(mark(X)) -> s(X), s(active(X)) -> s(X), active(sel(s(N), cons(X, XS))) -> mark(sel(N, XS)), active(sel(0(), cons(X, XS))) -> mark(X), active(fib1(X, Y)) -> mark(cons(X, fib1(Y, add(X, Y)))), active(fib(N)) -> mark(sel(N, fib1(s(0()), s(0())))), active(add(s(X), Y)) -> mark(s(add(X, Y))), active(add(0(), X)) -> mark(X), fib(mark(X)) -> fib(X), fib(active(X)) -> fib(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), 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)} SPSC: Simple Projection: pi(add#) = 1 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(sel(X1, X2)) -> active(sel(mark(X1), mark(X2))), mark(fib1(X1, X2)) -> active(fib1(mark(X1), mark(X2))), mark(s(X)) -> active(s(mark(X))), mark(0()) -> active(0()), mark(fib(X)) -> active(fib(mark(X))), mark(cons(X1, X2)) -> active(cons(mark(X1), X2)), mark(add(X1, X2)) -> active(add(mark(X1), mark(X2))), sel(X1, mark(X2)) -> sel(X1, X2), sel(X1, active(X2)) -> sel(X1, X2), sel(mark(X1), X2) -> sel(X1, X2), sel(active(X1), X2) -> sel(X1, X2), fib1(X1, mark(X2)) -> fib1(X1, X2), fib1(X1, active(X2)) -> fib1(X1, X2), fib1(mark(X1), X2) -> fib1(X1, X2), fib1(active(X1), X2) -> fib1(X1, X2), s(mark(X)) -> s(X), s(active(X)) -> s(X), active(sel(s(N), cons(X, XS))) -> mark(sel(N, XS)), active(sel(0(), cons(X, XS))) -> mark(X), active(fib1(X, Y)) -> mark(cons(X, fib1(Y, add(X, Y)))), active(fib(N)) -> mark(sel(N, fib1(s(0()), s(0())))), active(add(s(X), Y)) -> mark(s(add(X, Y))), active(add(0(), X)) -> mark(X), fib(mark(X)) -> fib(X), fib(active(X)) -> fib(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), 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)} 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(sel(X1, X2)) -> active(sel(mark(X1), mark(X2))), mark(fib1(X1, X2)) -> active(fib1(mark(X1), mark(X2))), mark(s(X)) -> active(s(mark(X))), mark(0()) -> active(0()), mark(fib(X)) -> active(fib(mark(X))), mark(cons(X1, X2)) -> active(cons(mark(X1), X2)), mark(add(X1, X2)) -> active(add(mark(X1), mark(X2))), sel(X1, mark(X2)) -> sel(X1, X2), sel(X1, active(X2)) -> sel(X1, X2), sel(mark(X1), X2) -> sel(X1, X2), sel(active(X1), X2) -> sel(X1, X2), fib1(X1, mark(X2)) -> fib1(X1, X2), fib1(X1, active(X2)) -> fib1(X1, X2), fib1(mark(X1), X2) -> fib1(X1, X2), fib1(active(X1), X2) -> fib1(X1, X2), s(mark(X)) -> s(X), s(active(X)) -> s(X), active(sel(s(N), cons(X, XS))) -> mark(sel(N, XS)), active(sel(0(), cons(X, XS))) -> mark(X), active(fib1(X, Y)) -> mark(cons(X, fib1(Y, add(X, Y)))), active(fib(N)) -> mark(sel(N, fib1(s(0()), s(0())))), active(add(s(X), Y)) -> mark(s(add(X, Y))), active(add(0(), X)) -> mark(X), fib(mark(X)) -> fib(X), fib(active(X)) -> fib(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), 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)} 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(sel(X1, X2)) -> active(sel(mark(X1), mark(X2))), mark(fib1(X1, X2)) -> active(fib1(mark(X1), mark(X2))), mark(s(X)) -> active(s(mark(X))), mark(0()) -> active(0()), mark(fib(X)) -> active(fib(mark(X))), mark(cons(X1, X2)) -> active(cons(mark(X1), X2)), mark(add(X1, X2)) -> active(add(mark(X1), mark(X2))), sel(X1, mark(X2)) -> sel(X1, X2), sel(X1, active(X2)) -> sel(X1, X2), sel(mark(X1), X2) -> sel(X1, X2), sel(active(X1), X2) -> sel(X1, X2), fib1(X1, mark(X2)) -> fib1(X1, X2), fib1(X1, active(X2)) -> fib1(X1, X2), fib1(mark(X1), X2) -> fib1(X1, X2), fib1(active(X1), X2) -> fib1(X1, X2), s(mark(X)) -> s(X), s(active(X)) -> s(X), active(sel(s(N), cons(X, XS))) -> mark(sel(N, XS)), active(sel(0(), cons(X, XS))) -> mark(X), active(fib1(X, Y)) -> mark(cons(X, fib1(Y, add(X, Y)))), active(fib(N)) -> mark(sel(N, fib1(s(0()), s(0())))), active(add(s(X), Y)) -> mark(s(add(X, Y))), active(add(0(), X)) -> mark(X), fib(mark(X)) -> fib(X), fib(active(X)) -> fib(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), 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)} 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(sel(X1, X2)) -> active(sel(mark(X1), mark(X2))), mark(fib1(X1, X2)) -> active(fib1(mark(X1), mark(X2))), mark(s(X)) -> active(s(mark(X))), mark(0()) -> active(0()), mark(fib(X)) -> active(fib(mark(X))), mark(cons(X1, X2)) -> active(cons(mark(X1), X2)), mark(add(X1, X2)) -> active(add(mark(X1), mark(X2))), sel(X1, mark(X2)) -> sel(X1, X2), sel(X1, active(X2)) -> sel(X1, X2), sel(mark(X1), X2) -> sel(X1, X2), sel(active(X1), X2) -> sel(X1, X2), fib1(X1, mark(X2)) -> fib1(X1, X2), fib1(X1, active(X2)) -> fib1(X1, X2), fib1(mark(X1), X2) -> fib1(X1, X2), fib1(active(X1), X2) -> fib1(X1, X2), s(mark(X)) -> s(X), s(active(X)) -> s(X), active(sel(s(N), cons(X, XS))) -> mark(sel(N, XS)), active(sel(0(), cons(X, XS))) -> mark(X), active(fib1(X, Y)) -> mark(cons(X, fib1(Y, add(X, Y)))), active(fib(N)) -> mark(sel(N, fib1(s(0()), s(0())))), active(add(s(X), Y)) -> mark(s(add(X, Y))), active(add(0(), X)) -> mark(X), fib(mark(X)) -> fib(X), fib(active(X)) -> fib(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), 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)} SPSC: Simple Projection: pi(cons#) = 1 Strict: {} Qed SCC: Strict: { fib#(mark(X)) -> fib#(X), fib#(active(X)) -> fib#(X)} Weak: { mark(sel(X1, X2)) -> active(sel(mark(X1), mark(X2))), mark(fib1(X1, X2)) -> active(fib1(mark(X1), mark(X2))), mark(s(X)) -> active(s(mark(X))), mark(0()) -> active(0()), mark(fib(X)) -> active(fib(mark(X))), mark(cons(X1, X2)) -> active(cons(mark(X1), X2)), mark(add(X1, X2)) -> active(add(mark(X1), mark(X2))), sel(X1, mark(X2)) -> sel(X1, X2), sel(X1, active(X2)) -> sel(X1, X2), sel(mark(X1), X2) -> sel(X1, X2), sel(active(X1), X2) -> sel(X1, X2), fib1(X1, mark(X2)) -> fib1(X1, X2), fib1(X1, active(X2)) -> fib1(X1, X2), fib1(mark(X1), X2) -> fib1(X1, X2), fib1(active(X1), X2) -> fib1(X1, X2), s(mark(X)) -> s(X), s(active(X)) -> s(X), active(sel(s(N), cons(X, XS))) -> mark(sel(N, XS)), active(sel(0(), cons(X, XS))) -> mark(X), active(fib1(X, Y)) -> mark(cons(X, fib1(Y, add(X, Y)))), active(fib(N)) -> mark(sel(N, fib1(s(0()), s(0())))), active(add(s(X), Y)) -> mark(s(add(X, Y))), active(add(0(), X)) -> mark(X), fib(mark(X)) -> fib(X), fib(active(X)) -> fib(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), 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)} SPSC: Simple Projection: pi(fib#) = 0 Strict: {fib#(active(X)) -> fib#(X)} EDG: {(fib#(active(X)) -> fib#(X), fib#(active(X)) -> fib#(X))} SCCS: Scc: {fib#(active(X)) -> fib#(X)} SCC: Strict: {fib#(active(X)) -> fib#(X)} Weak: { mark(sel(X1, X2)) -> active(sel(mark(X1), mark(X2))), mark(fib1(X1, X2)) -> active(fib1(mark(X1), mark(X2))), mark(s(X)) -> active(s(mark(X))), mark(0()) -> active(0()), mark(fib(X)) -> active(fib(mark(X))), mark(cons(X1, X2)) -> active(cons(mark(X1), X2)), mark(add(X1, X2)) -> active(add(mark(X1), mark(X2))), sel(X1, mark(X2)) -> sel(X1, X2), sel(X1, active(X2)) -> sel(X1, X2), sel(mark(X1), X2) -> sel(X1, X2), sel(active(X1), X2) -> sel(X1, X2), fib1(X1, mark(X2)) -> fib1(X1, X2), fib1(X1, active(X2)) -> fib1(X1, X2), fib1(mark(X1), X2) -> fib1(X1, X2), fib1(active(X1), X2) -> fib1(X1, X2), s(mark(X)) -> s(X), s(active(X)) -> s(X), active(sel(s(N), cons(X, XS))) -> mark(sel(N, XS)), active(sel(0(), cons(X, XS))) -> mark(X), active(fib1(X, Y)) -> mark(cons(X, fib1(Y, add(X, Y)))), active(fib(N)) -> mark(sel(N, fib1(s(0()), s(0())))), active(add(s(X), Y)) -> mark(s(add(X, Y))), active(add(0(), X)) -> mark(X), fib(mark(X)) -> fib(X), fib(active(X)) -> fib(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), 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)} SPSC: Simple Projection: pi(fib#) = 0 Strict: {} Qed SCC: Strict: { s#(mark(X)) -> s#(X), s#(active(X)) -> s#(X)} Weak: { mark(sel(X1, X2)) -> active(sel(mark(X1), mark(X2))), mark(fib1(X1, X2)) -> active(fib1(mark(X1), mark(X2))), mark(s(X)) -> active(s(mark(X))), mark(0()) -> active(0()), mark(fib(X)) -> active(fib(mark(X))), mark(cons(X1, X2)) -> active(cons(mark(X1), X2)), mark(add(X1, X2)) -> active(add(mark(X1), mark(X2))), sel(X1, mark(X2)) -> sel(X1, X2), sel(X1, active(X2)) -> sel(X1, X2), sel(mark(X1), X2) -> sel(X1, X2), sel(active(X1), X2) -> sel(X1, X2), fib1(X1, mark(X2)) -> fib1(X1, X2), fib1(X1, active(X2)) -> fib1(X1, X2), fib1(mark(X1), X2) -> fib1(X1, X2), fib1(active(X1), X2) -> fib1(X1, X2), s(mark(X)) -> s(X), s(active(X)) -> s(X), active(sel(s(N), cons(X, XS))) -> mark(sel(N, XS)), active(sel(0(), cons(X, XS))) -> mark(X), active(fib1(X, Y)) -> mark(cons(X, fib1(Y, add(X, Y)))), active(fib(N)) -> mark(sel(N, fib1(s(0()), s(0())))), active(add(s(X), Y)) -> mark(s(add(X, Y))), active(add(0(), X)) -> mark(X), fib(mark(X)) -> fib(X), fib(active(X)) -> fib(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), 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)} SPSC: Simple Projection: pi(s#) = 0 Strict: {s#(mark(X)) -> s#(X)} EDG: {(s#(mark(X)) -> s#(X), s#(mark(X)) -> s#(X))} SCCS: Scc: {s#(mark(X)) -> s#(X)} SCC: Strict: {s#(mark(X)) -> s#(X)} Weak: { mark(sel(X1, X2)) -> active(sel(mark(X1), mark(X2))), mark(fib1(X1, X2)) -> active(fib1(mark(X1), mark(X2))), mark(s(X)) -> active(s(mark(X))), mark(0()) -> active(0()), mark(fib(X)) -> active(fib(mark(X))), mark(cons(X1, X2)) -> active(cons(mark(X1), X2)), mark(add(X1, X2)) -> active(add(mark(X1), mark(X2))), sel(X1, mark(X2)) -> sel(X1, X2), sel(X1, active(X2)) -> sel(X1, X2), sel(mark(X1), X2) -> sel(X1, X2), sel(active(X1), X2) -> sel(X1, X2), fib1(X1, mark(X2)) -> fib1(X1, X2), fib1(X1, active(X2)) -> fib1(X1, X2), fib1(mark(X1), X2) -> fib1(X1, X2), fib1(active(X1), X2) -> fib1(X1, X2), s(mark(X)) -> s(X), s(active(X)) -> s(X), active(sel(s(N), cons(X, XS))) -> mark(sel(N, XS)), active(sel(0(), cons(X, XS))) -> mark(X), active(fib1(X, Y)) -> mark(cons(X, fib1(Y, add(X, Y)))), active(fib(N)) -> mark(sel(N, fib1(s(0()), s(0())))), active(add(s(X), Y)) -> mark(s(add(X, Y))), active(add(0(), X)) -> mark(X), fib(mark(X)) -> fib(X), fib(active(X)) -> fib(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), 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)} SPSC: Simple Projection: pi(s#) = 0 Strict: {} Qed SCC: Strict: { fib1#(X1, mark(X2)) -> fib1#(X1, X2), fib1#(X1, active(X2)) -> fib1#(X1, X2), fib1#(mark(X1), X2) -> fib1#(X1, X2), fib1#(active(X1), X2) -> fib1#(X1, X2)} Weak: { mark(sel(X1, X2)) -> active(sel(mark(X1), mark(X2))), mark(fib1(X1, X2)) -> active(fib1(mark(X1), mark(X2))), mark(s(X)) -> active(s(mark(X))), mark(0()) -> active(0()), mark(fib(X)) -> active(fib(mark(X))), mark(cons(X1, X2)) -> active(cons(mark(X1), X2)), mark(add(X1, X2)) -> active(add(mark(X1), mark(X2))), sel(X1, mark(X2)) -> sel(X1, X2), sel(X1, active(X2)) -> sel(X1, X2), sel(mark(X1), X2) -> sel(X1, X2), sel(active(X1), X2) -> sel(X1, X2), fib1(X1, mark(X2)) -> fib1(X1, X2), fib1(X1, active(X2)) -> fib1(X1, X2), fib1(mark(X1), X2) -> fib1(X1, X2), fib1(active(X1), X2) -> fib1(X1, X2), s(mark(X)) -> s(X), s(active(X)) -> s(X), active(sel(s(N), cons(X, XS))) -> mark(sel(N, XS)), active(sel(0(), cons(X, XS))) -> mark(X), active(fib1(X, Y)) -> mark(cons(X, fib1(Y, add(X, Y)))), active(fib(N)) -> mark(sel(N, fib1(s(0()), s(0())))), active(add(s(X), Y)) -> mark(s(add(X, Y))), active(add(0(), X)) -> mark(X), fib(mark(X)) -> fib(X), fib(active(X)) -> fib(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), 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)} SPSC: Simple Projection: pi(fib1#) = 0 Strict: { fib1#(X1, mark(X2)) -> fib1#(X1, X2), fib1#(X1, active(X2)) -> fib1#(X1, X2), fib1#(mark(X1), X2) -> fib1#(X1, X2)} EDG: {(fib1#(X1, active(X2)) -> fib1#(X1, X2), fib1#(mark(X1), X2) -> fib1#(X1, X2)) (fib1#(X1, active(X2)) -> fib1#(X1, X2), fib1#(X1, active(X2)) -> fib1#(X1, X2)) (fib1#(X1, active(X2)) -> fib1#(X1, X2), fib1#(X1, mark(X2)) -> fib1#(X1, X2)) (fib1#(mark(X1), X2) -> fib1#(X1, X2), fib1#(X1, mark(X2)) -> fib1#(X1, X2)) (fib1#(mark(X1), X2) -> fib1#(X1, X2), fib1#(X1, active(X2)) -> fib1#(X1, X2)) (fib1#(mark(X1), X2) -> fib1#(X1, X2), fib1#(mark(X1), X2) -> fib1#(X1, X2)) (fib1#(X1, mark(X2)) -> fib1#(X1, X2), fib1#(X1, mark(X2)) -> fib1#(X1, X2)) (fib1#(X1, mark(X2)) -> fib1#(X1, X2), fib1#(X1, active(X2)) -> fib1#(X1, X2)) (fib1#(X1, mark(X2)) -> fib1#(X1, X2), fib1#(mark(X1), X2) -> fib1#(X1, X2))} SCCS: Scc: { fib1#(X1, mark(X2)) -> fib1#(X1, X2), fib1#(X1, active(X2)) -> fib1#(X1, X2), fib1#(mark(X1), X2) -> fib1#(X1, X2)} SCC: Strict: { fib1#(X1, mark(X2)) -> fib1#(X1, X2), fib1#(X1, active(X2)) -> fib1#(X1, X2), fib1#(mark(X1), X2) -> fib1#(X1, X2)} Weak: { mark(sel(X1, X2)) -> active(sel(mark(X1), mark(X2))), mark(fib1(X1, X2)) -> active(fib1(mark(X1), mark(X2))), mark(s(X)) -> active(s(mark(X))), mark(0()) -> active(0()), mark(fib(X)) -> active(fib(mark(X))), mark(cons(X1, X2)) -> active(cons(mark(X1), X2)), mark(add(X1, X2)) -> active(add(mark(X1), mark(X2))), sel(X1, mark(X2)) -> sel(X1, X2), sel(X1, active(X2)) -> sel(X1, X2), sel(mark(X1), X2) -> sel(X1, X2), sel(active(X1), X2) -> sel(X1, X2), fib1(X1, mark(X2)) -> fib1(X1, X2), fib1(X1, active(X2)) -> fib1(X1, X2), fib1(mark(X1), X2) -> fib1(X1, X2), fib1(active(X1), X2) -> fib1(X1, X2), s(mark(X)) -> s(X), s(active(X)) -> s(X), active(sel(s(N), cons(X, XS))) -> mark(sel(N, XS)), active(sel(0(), cons(X, XS))) -> mark(X), active(fib1(X, Y)) -> mark(cons(X, fib1(Y, add(X, Y)))), active(fib(N)) -> mark(sel(N, fib1(s(0()), s(0())))), active(add(s(X), Y)) -> mark(s(add(X, Y))), active(add(0(), X)) -> mark(X), fib(mark(X)) -> fib(X), fib(active(X)) -> fib(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), 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)} SPSC: Simple Projection: pi(fib1#) = 0 Strict: { fib1#(X1, mark(X2)) -> fib1#(X1, X2), fib1#(X1, active(X2)) -> fib1#(X1, X2)} EDG: {(fib1#(X1, active(X2)) -> fib1#(X1, X2), fib1#(X1, active(X2)) -> fib1#(X1, X2)) (fib1#(X1, active(X2)) -> fib1#(X1, X2), fib1#(X1, mark(X2)) -> fib1#(X1, X2)) (fib1#(X1, mark(X2)) -> fib1#(X1, X2), fib1#(X1, mark(X2)) -> fib1#(X1, X2)) (fib1#(X1, mark(X2)) -> fib1#(X1, X2), fib1#(X1, active(X2)) -> fib1#(X1, X2))} SCCS: Scc: { fib1#(X1, mark(X2)) -> fib1#(X1, X2), fib1#(X1, active(X2)) -> fib1#(X1, X2)} SCC: Strict: { fib1#(X1, mark(X2)) -> fib1#(X1, X2), fib1#(X1, active(X2)) -> fib1#(X1, X2)} Weak: { mark(sel(X1, X2)) -> active(sel(mark(X1), mark(X2))), mark(fib1(X1, X2)) -> active(fib1(mark(X1), mark(X2))), mark(s(X)) -> active(s(mark(X))), mark(0()) -> active(0()), mark(fib(X)) -> active(fib(mark(X))), mark(cons(X1, X2)) -> active(cons(mark(X1), X2)), mark(add(X1, X2)) -> active(add(mark(X1), mark(X2))), sel(X1, mark(X2)) -> sel(X1, X2), sel(X1, active(X2)) -> sel(X1, X2), sel(mark(X1), X2) -> sel(X1, X2), sel(active(X1), X2) -> sel(X1, X2), fib1(X1, mark(X2)) -> fib1(X1, X2), fib1(X1, active(X2)) -> fib1(X1, X2), fib1(mark(X1), X2) -> fib1(X1, X2), fib1(active(X1), X2) -> fib1(X1, X2), s(mark(X)) -> s(X), s(active(X)) -> s(X), active(sel(s(N), cons(X, XS))) -> mark(sel(N, XS)), active(sel(0(), cons(X, XS))) -> mark(X), active(fib1(X, Y)) -> mark(cons(X, fib1(Y, add(X, Y)))), active(fib(N)) -> mark(sel(N, fib1(s(0()), s(0())))), active(add(s(X), Y)) -> mark(s(add(X, Y))), active(add(0(), X)) -> mark(X), fib(mark(X)) -> fib(X), fib(active(X)) -> fib(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), 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)} SPSC: Simple Projection: pi(fib1#) = 1 Strict: {fib1#(X1, active(X2)) -> fib1#(X1, X2)} EDG: {(fib1#(X1, active(X2)) -> fib1#(X1, X2), fib1#(X1, active(X2)) -> fib1#(X1, X2))} SCCS: Scc: {fib1#(X1, active(X2)) -> fib1#(X1, X2)} SCC: Strict: {fib1#(X1, active(X2)) -> fib1#(X1, X2)} Weak: { mark(sel(X1, X2)) -> active(sel(mark(X1), mark(X2))), mark(fib1(X1, X2)) -> active(fib1(mark(X1), mark(X2))), mark(s(X)) -> active(s(mark(X))), mark(0()) -> active(0()), mark(fib(X)) -> active(fib(mark(X))), mark(cons(X1, X2)) -> active(cons(mark(X1), X2)), mark(add(X1, X2)) -> active(add(mark(X1), mark(X2))), sel(X1, mark(X2)) -> sel(X1, X2), sel(X1, active(X2)) -> sel(X1, X2), sel(mark(X1), X2) -> sel(X1, X2), sel(active(X1), X2) -> sel(X1, X2), fib1(X1, mark(X2)) -> fib1(X1, X2), fib1(X1, active(X2)) -> fib1(X1, X2), fib1(mark(X1), X2) -> fib1(X1, X2), fib1(active(X1), X2) -> fib1(X1, X2), s(mark(X)) -> s(X), s(active(X)) -> s(X), active(sel(s(N), cons(X, XS))) -> mark(sel(N, XS)), active(sel(0(), cons(X, XS))) -> mark(X), active(fib1(X, Y)) -> mark(cons(X, fib1(Y, add(X, Y)))), active(fib(N)) -> mark(sel(N, fib1(s(0()), s(0())))), active(add(s(X), Y)) -> mark(s(add(X, Y))), active(add(0(), X)) -> mark(X), fib(mark(X)) -> fib(X), fib(active(X)) -> fib(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), 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)} SPSC: Simple Projection: pi(fib1#) = 1 Strict: {} Qed SCC: Strict: { sel#(X1, mark(X2)) -> sel#(X1, X2), sel#(X1, active(X2)) -> sel#(X1, X2), sel#(mark(X1), X2) -> sel#(X1, X2), sel#(active(X1), X2) -> sel#(X1, X2)} Weak: { mark(sel(X1, X2)) -> active(sel(mark(X1), mark(X2))), mark(fib1(X1, X2)) -> active(fib1(mark(X1), mark(X2))), mark(s(X)) -> active(s(mark(X))), mark(0()) -> active(0()), mark(fib(X)) -> active(fib(mark(X))), mark(cons(X1, X2)) -> active(cons(mark(X1), X2)), mark(add(X1, X2)) -> active(add(mark(X1), mark(X2))), sel(X1, mark(X2)) -> sel(X1, X2), sel(X1, active(X2)) -> sel(X1, X2), sel(mark(X1), X2) -> sel(X1, X2), sel(active(X1), X2) -> sel(X1, X2), fib1(X1, mark(X2)) -> fib1(X1, X2), fib1(X1, active(X2)) -> fib1(X1, X2), fib1(mark(X1), X2) -> fib1(X1, X2), fib1(active(X1), X2) -> fib1(X1, X2), s(mark(X)) -> s(X), s(active(X)) -> s(X), active(sel(s(N), cons(X, XS))) -> mark(sel(N, XS)), active(sel(0(), cons(X, XS))) -> mark(X), active(fib1(X, Y)) -> mark(cons(X, fib1(Y, add(X, Y)))), active(fib(N)) -> mark(sel(N, fib1(s(0()), s(0())))), active(add(s(X), Y)) -> mark(s(add(X, Y))), active(add(0(), X)) -> mark(X), fib(mark(X)) -> fib(X), fib(active(X)) -> fib(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), 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)} SPSC: Simple Projection: pi(sel#) = 0 Strict: { sel#(X1, mark(X2)) -> sel#(X1, X2), sel#(X1, active(X2)) -> sel#(X1, X2), sel#(mark(X1), X2) -> sel#(X1, X2)} EDG: {(sel#(X1, active(X2)) -> sel#(X1, X2), sel#(mark(X1), X2) -> sel#(X1, X2)) (sel#(X1, active(X2)) -> sel#(X1, X2), sel#(X1, active(X2)) -> sel#(X1, X2)) (sel#(X1, active(X2)) -> sel#(X1, X2), sel#(X1, mark(X2)) -> sel#(X1, X2)) (sel#(mark(X1), X2) -> sel#(X1, X2), sel#(X1, mark(X2)) -> sel#(X1, X2)) (sel#(mark(X1), X2) -> sel#(X1, X2), sel#(X1, active(X2)) -> sel#(X1, X2)) (sel#(mark(X1), X2) -> sel#(X1, X2), sel#(mark(X1), X2) -> sel#(X1, X2)) (sel#(X1, mark(X2)) -> sel#(X1, X2), sel#(X1, mark(X2)) -> sel#(X1, X2)) (sel#(X1, mark(X2)) -> sel#(X1, X2), sel#(X1, active(X2)) -> sel#(X1, X2)) (sel#(X1, mark(X2)) -> sel#(X1, X2), sel#(mark(X1), X2) -> sel#(X1, X2))} SCCS: Scc: { sel#(X1, mark(X2)) -> sel#(X1, X2), sel#(X1, active(X2)) -> sel#(X1, X2), sel#(mark(X1), X2) -> sel#(X1, X2)} SCC: Strict: { sel#(X1, mark(X2)) -> sel#(X1, X2), sel#(X1, active(X2)) -> sel#(X1, X2), sel#(mark(X1), X2) -> sel#(X1, X2)} Weak: { mark(sel(X1, X2)) -> active(sel(mark(X1), mark(X2))), mark(fib1(X1, X2)) -> active(fib1(mark(X1), mark(X2))), mark(s(X)) -> active(s(mark(X))), mark(0()) -> active(0()), mark(fib(X)) -> active(fib(mark(X))), mark(cons(X1, X2)) -> active(cons(mark(X1), X2)), mark(add(X1, X2)) -> active(add(mark(X1), mark(X2))), sel(X1, mark(X2)) -> sel(X1, X2), sel(X1, active(X2)) -> sel(X1, X2), sel(mark(X1), X2) -> sel(X1, X2), sel(active(X1), X2) -> sel(X1, X2), fib1(X1, mark(X2)) -> fib1(X1, X2), fib1(X1, active(X2)) -> fib1(X1, X2), fib1(mark(X1), X2) -> fib1(X1, X2), fib1(active(X1), X2) -> fib1(X1, X2), s(mark(X)) -> s(X), s(active(X)) -> s(X), active(sel(s(N), cons(X, XS))) -> mark(sel(N, XS)), active(sel(0(), cons(X, XS))) -> mark(X), active(fib1(X, Y)) -> mark(cons(X, fib1(Y, add(X, Y)))), active(fib(N)) -> mark(sel(N, fib1(s(0()), s(0())))), active(add(s(X), Y)) -> mark(s(add(X, Y))), active(add(0(), X)) -> mark(X), fib(mark(X)) -> fib(X), fib(active(X)) -> fib(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), 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)} SPSC: Simple Projection: pi(sel#) = 0 Strict: { sel#(X1, mark(X2)) -> sel#(X1, X2), sel#(X1, active(X2)) -> sel#(X1, X2)} EDG: {(sel#(X1, active(X2)) -> sel#(X1, X2), sel#(X1, active(X2)) -> sel#(X1, X2)) (sel#(X1, active(X2)) -> sel#(X1, X2), sel#(X1, mark(X2)) -> sel#(X1, X2)) (sel#(X1, mark(X2)) -> sel#(X1, X2), sel#(X1, mark(X2)) -> sel#(X1, X2)) (sel#(X1, mark(X2)) -> sel#(X1, X2), sel#(X1, active(X2)) -> sel#(X1, X2))} SCCS: Scc: { sel#(X1, mark(X2)) -> sel#(X1, X2), sel#(X1, active(X2)) -> sel#(X1, X2)} SCC: Strict: { sel#(X1, mark(X2)) -> sel#(X1, X2), sel#(X1, active(X2)) -> sel#(X1, X2)} Weak: { mark(sel(X1, X2)) -> active(sel(mark(X1), mark(X2))), mark(fib1(X1, X2)) -> active(fib1(mark(X1), mark(X2))), mark(s(X)) -> active(s(mark(X))), mark(0()) -> active(0()), mark(fib(X)) -> active(fib(mark(X))), mark(cons(X1, X2)) -> active(cons(mark(X1), X2)), mark(add(X1, X2)) -> active(add(mark(X1), mark(X2))), sel(X1, mark(X2)) -> sel(X1, X2), sel(X1, active(X2)) -> sel(X1, X2), sel(mark(X1), X2) -> sel(X1, X2), sel(active(X1), X2) -> sel(X1, X2), fib1(X1, mark(X2)) -> fib1(X1, X2), fib1(X1, active(X2)) -> fib1(X1, X2), fib1(mark(X1), X2) -> fib1(X1, X2), fib1(active(X1), X2) -> fib1(X1, X2), s(mark(X)) -> s(X), s(active(X)) -> s(X), active(sel(s(N), cons(X, XS))) -> mark(sel(N, XS)), active(sel(0(), cons(X, XS))) -> mark(X), active(fib1(X, Y)) -> mark(cons(X, fib1(Y, add(X, Y)))), active(fib(N)) -> mark(sel(N, fib1(s(0()), s(0())))), active(add(s(X), Y)) -> mark(s(add(X, Y))), active(add(0(), X)) -> mark(X), fib(mark(X)) -> fib(X), fib(active(X)) -> fib(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), 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)} SPSC: Simple Projection: pi(sel#) = 1 Strict: {sel#(X1, active(X2)) -> sel#(X1, X2)} EDG: {(sel#(X1, active(X2)) -> sel#(X1, X2), sel#(X1, active(X2)) -> sel#(X1, X2))} SCCS: Scc: {sel#(X1, active(X2)) -> sel#(X1, X2)} SCC: Strict: {sel#(X1, active(X2)) -> sel#(X1, X2)} Weak: { mark(sel(X1, X2)) -> active(sel(mark(X1), mark(X2))), mark(fib1(X1, X2)) -> active(fib1(mark(X1), mark(X2))), mark(s(X)) -> active(s(mark(X))), mark(0()) -> active(0()), mark(fib(X)) -> active(fib(mark(X))), mark(cons(X1, X2)) -> active(cons(mark(X1), X2)), mark(add(X1, X2)) -> active(add(mark(X1), mark(X2))), sel(X1, mark(X2)) -> sel(X1, X2), sel(X1, active(X2)) -> sel(X1, X2), sel(mark(X1), X2) -> sel(X1, X2), sel(active(X1), X2) -> sel(X1, X2), fib1(X1, mark(X2)) -> fib1(X1, X2), fib1(X1, active(X2)) -> fib1(X1, X2), fib1(mark(X1), X2) -> fib1(X1, X2), fib1(active(X1), X2) -> fib1(X1, X2), s(mark(X)) -> s(X), s(active(X)) -> s(X), active(sel(s(N), cons(X, XS))) -> mark(sel(N, XS)), active(sel(0(), cons(X, XS))) -> mark(X), active(fib1(X, Y)) -> mark(cons(X, fib1(Y, add(X, Y)))), active(fib(N)) -> mark(sel(N, fib1(s(0()), s(0())))), active(add(s(X), Y)) -> mark(s(add(X, Y))), active(add(0(), X)) -> mark(X), fib(mark(X)) -> fib(X), fib(active(X)) -> fib(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), 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)} SPSC: Simple Projection: pi(sel#) = 1 Strict: {} Qed SCC: Strict: { mark#(sel(X1, X2)) -> mark#(X1), mark#(sel(X1, X2)) -> mark#(X2), mark#(sel(X1, X2)) -> active#(sel(mark(X1), mark(X2))), mark#(fib1(X1, X2)) -> mark#(X1), mark#(fib1(X1, X2)) -> mark#(X2), mark#(fib1(X1, X2)) -> active#(fib1(mark(X1), mark(X2))), mark#(s(X)) -> mark#(X), mark#(s(X)) -> active#(s(mark(X))), mark#(fib(X)) -> mark#(X), mark#(fib(X)) -> active#(fib(mark(X))), mark#(cons(X1, X2)) -> mark#(X1), mark#(cons(X1, X2)) -> active#(cons(mark(X1), X2)), mark#(add(X1, X2)) -> mark#(X1), mark#(add(X1, X2)) -> mark#(X2), mark#(add(X1, X2)) -> active#(add(mark(X1), mark(X2))), active#(sel(s(N), cons(X, XS))) -> mark#(sel(N, XS)), active#(sel(0(), cons(X, XS))) -> mark#(X), active#(fib1(X, Y)) -> mark#(cons(X, fib1(Y, add(X, Y)))), active#(fib(N)) -> mark#(sel(N, fib1(s(0()), s(0())))), active#(add(s(X), Y)) -> mark#(s(add(X, Y))), active#(add(0(), X)) -> mark#(X)} Weak: { mark(sel(X1, X2)) -> active(sel(mark(X1), mark(X2))), mark(fib1(X1, X2)) -> active(fib1(mark(X1), mark(X2))), mark(s(X)) -> active(s(mark(X))), mark(0()) -> active(0()), mark(fib(X)) -> active(fib(mark(X))), mark(cons(X1, X2)) -> active(cons(mark(X1), X2)), mark(add(X1, X2)) -> active(add(mark(X1), mark(X2))), sel(X1, mark(X2)) -> sel(X1, X2), sel(X1, active(X2)) -> sel(X1, X2), sel(mark(X1), X2) -> sel(X1, X2), sel(active(X1), X2) -> sel(X1, X2), fib1(X1, mark(X2)) -> fib1(X1, X2), fib1(X1, active(X2)) -> fib1(X1, X2), fib1(mark(X1), X2) -> fib1(X1, X2), fib1(active(X1), X2) -> fib1(X1, X2), s(mark(X)) -> s(X), s(active(X)) -> s(X), active(sel(s(N), cons(X, XS))) -> mark(sel(N, XS)), active(sel(0(), cons(X, XS))) -> mark(X), active(fib1(X, Y)) -> mark(cons(X, fib1(Y, add(X, Y)))), active(fib(N)) -> mark(sel(N, fib1(s(0()), s(0())))), active(add(s(X), Y)) -> mark(s(add(X, Y))), active(add(0(), X)) -> mark(X), fib(mark(X)) -> fib(X), fib(active(X)) -> fib(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), 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)} POLY: Argument Filtering: pi(add) = [], pi(cons) = [], pi(fib) = [], pi(active#) = 0, pi(active) = [], pi(0) = [], pi(s) = [], pi(fib1) = [], pi(sel) = [], pi(mark#) = [], pi(mark) = [] Usable Rules: {} Interpretation: [mark#] = 1, [add] = 1, [cons] = 0, [fib1] = 1, [sel] = 1, [fib] = 1, [s] = 0 Strict: { mark#(sel(X1, X2)) -> mark#(X1), mark#(sel(X1, X2)) -> mark#(X2), mark#(sel(X1, X2)) -> active#(sel(mark(X1), mark(X2))), mark#(fib1(X1, X2)) -> mark#(X1), mark#(fib1(X1, X2)) -> mark#(X2), mark#(fib1(X1, X2)) -> active#(fib1(mark(X1), mark(X2))), mark#(s(X)) -> mark#(X), mark#(fib(X)) -> mark#(X), mark#(fib(X)) -> active#(fib(mark(X))), mark#(cons(X1, X2)) -> mark#(X1), mark#(add(X1, X2)) -> mark#(X1), mark#(add(X1, X2)) -> mark#(X2), mark#(add(X1, X2)) -> active#(add(mark(X1), mark(X2))), active#(sel(s(N), cons(X, XS))) -> mark#(sel(N, XS)), active#(sel(0(), cons(X, XS))) -> mark#(X), active#(fib1(X, Y)) -> mark#(cons(X, fib1(Y, add(X, Y)))), active#(fib(N)) -> mark#(sel(N, fib1(s(0()), s(0())))), active#(add(s(X), Y)) -> mark#(s(add(X, Y))), active#(add(0(), X)) -> mark#(X)} Weak: { mark(sel(X1, X2)) -> active(sel(mark(X1), mark(X2))), mark(fib1(X1, X2)) -> active(fib1(mark(X1), mark(X2))), mark(s(X)) -> active(s(mark(X))), mark(0()) -> active(0()), mark(fib(X)) -> active(fib(mark(X))), mark(cons(X1, X2)) -> active(cons(mark(X1), X2)), mark(add(X1, X2)) -> active(add(mark(X1), mark(X2))), sel(X1, mark(X2)) -> sel(X1, X2), sel(X1, active(X2)) -> sel(X1, X2), sel(mark(X1), X2) -> sel(X1, X2), sel(active(X1), X2) -> sel(X1, X2), fib1(X1, mark(X2)) -> fib1(X1, X2), fib1(X1, active(X2)) -> fib1(X1, X2), fib1(mark(X1), X2) -> fib1(X1, X2), fib1(active(X1), X2) -> fib1(X1, X2), s(mark(X)) -> s(X), s(active(X)) -> s(X), active(sel(s(N), cons(X, XS))) -> mark(sel(N, XS)), active(sel(0(), cons(X, XS))) -> mark(X), active(fib1(X, Y)) -> mark(cons(X, fib1(Y, add(X, Y)))), active(fib(N)) -> mark(sel(N, fib1(s(0()), s(0())))), active(add(s(X), Y)) -> mark(s(add(X, Y))), active(add(0(), X)) -> mark(X), fib(mark(X)) -> fib(X), fib(active(X)) -> fib(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), 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)} EDG: { (mark#(sel(X1, X2)) -> mark#(X2), mark#(add(X1, X2)) -> active#(add(mark(X1), mark(X2)))) (mark#(sel(X1, X2)) -> mark#(X2), mark#(add(X1, X2)) -> mark#(X2)) (mark#(sel(X1, X2)) -> mark#(X2), mark#(add(X1, X2)) -> mark#(X1)) (mark#(sel(X1, X2)) -> mark#(X2), mark#(cons(X1, X2)) -> mark#(X1)) (mark#(sel(X1, X2)) -> mark#(X2), mark#(fib(X)) -> active#(fib(mark(X)))) (mark#(sel(X1, X2)) -> mark#(X2), mark#(fib(X)) -> mark#(X)) (mark#(sel(X1, X2)) -> mark#(X2), mark#(s(X)) -> mark#(X)) (mark#(sel(X1, X2)) -> mark#(X2), mark#(fib1(X1, X2)) -> active#(fib1(mark(X1), mark(X2)))) (mark#(sel(X1, X2)) -> mark#(X2), mark#(fib1(X1, X2)) -> mark#(X2)) (mark#(sel(X1, X2)) -> mark#(X2), mark#(fib1(X1, X2)) -> mark#(X1)) (mark#(sel(X1, X2)) -> mark#(X2), mark#(sel(X1, X2)) -> active#(sel(mark(X1), mark(X2)))) (mark#(sel(X1, X2)) -> mark#(X2), mark#(sel(X1, X2)) -> mark#(X2)) (mark#(sel(X1, X2)) -> mark#(X2), mark#(sel(X1, X2)) -> mark#(X1)) (mark#(s(X)) -> mark#(X), mark#(add(X1, X2)) -> active#(add(mark(X1), mark(X2)))) (mark#(s(X)) -> mark#(X), mark#(add(X1, X2)) -> mark#(X2)) (mark#(s(X)) -> mark#(X), mark#(add(X1, X2)) -> mark#(X1)) (mark#(s(X)) -> mark#(X), mark#(cons(X1, X2)) -> mark#(X1)) (mark#(s(X)) -> mark#(X), mark#(fib(X)) -> active#(fib(mark(X)))) (mark#(s(X)) -> mark#(X), mark#(fib(X)) -> mark#(X)) (mark#(s(X)) -> mark#(X), mark#(s(X)) -> mark#(X)) (mark#(s(X)) -> mark#(X), mark#(fib1(X1, X2)) -> active#(fib1(mark(X1), mark(X2)))) (mark#(s(X)) -> mark#(X), mark#(fib1(X1, X2)) -> mark#(X2)) (mark#(s(X)) -> mark#(X), mark#(fib1(X1, X2)) -> mark#(X1)) (mark#(s(X)) -> mark#(X), mark#(sel(X1, X2)) -> active#(sel(mark(X1), mark(X2)))) (mark#(s(X)) -> mark#(X), mark#(sel(X1, X2)) -> mark#(X2)) (mark#(s(X)) -> mark#(X), mark#(sel(X1, X2)) -> mark#(X1)) (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#(cons(X1, X2)) -> mark#(X1)) (mark#(add(X1, X2)) -> mark#(X2), mark#(fib(X)) -> active#(fib(mark(X)))) (mark#(add(X1, X2)) -> mark#(X2), mark#(fib(X)) -> mark#(X)) (mark#(add(X1, X2)) -> mark#(X2), mark#(s(X)) -> mark#(X)) (mark#(add(X1, X2)) -> mark#(X2), mark#(fib1(X1, X2)) -> active#(fib1(mark(X1), mark(X2)))) (mark#(add(X1, X2)) -> mark#(X2), mark#(fib1(X1, X2)) -> mark#(X2)) (mark#(add(X1, X2)) -> mark#(X2), mark#(fib1(X1, X2)) -> mark#(X1)) (mark#(add(X1, X2)) -> mark#(X2), mark#(sel(X1, X2)) -> active#(sel(mark(X1), mark(X2)))) (mark#(add(X1, X2)) -> mark#(X2), mark#(sel(X1, X2)) -> mark#(X2)) (mark#(add(X1, X2)) -> mark#(X2), mark#(sel(X1, X2)) -> mark#(X1)) (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#(cons(X1, X2)) -> mark#(X1)) (active#(add(0(), X)) -> mark#(X), mark#(fib(X)) -> active#(fib(mark(X)))) (active#(add(0(), X)) -> mark#(X), mark#(fib(X)) -> mark#(X)) (active#(add(0(), X)) -> mark#(X), mark#(s(X)) -> mark#(X)) (active#(add(0(), X)) -> mark#(X), mark#(fib1(X1, X2)) -> active#(fib1(mark(X1), mark(X2)))) (active#(add(0(), X)) -> mark#(X), mark#(fib1(X1, X2)) -> mark#(X2)) (active#(add(0(), X)) -> mark#(X), mark#(fib1(X1, X2)) -> mark#(X1)) (active#(add(0(), X)) -> mark#(X), mark#(sel(X1, X2)) -> active#(sel(mark(X1), mark(X2)))) (active#(add(0(), X)) -> mark#(X), mark#(sel(X1, X2)) -> mark#(X2)) (active#(add(0(), X)) -> mark#(X), mark#(sel(X1, X2)) -> mark#(X1)) (mark#(fib1(X1, X2)) -> active#(fib1(mark(X1), mark(X2))), active#(add(0(), X)) -> mark#(X)) (mark#(fib1(X1, X2)) -> active#(fib1(mark(X1), mark(X2))), active#(add(s(X), Y)) -> mark#(s(add(X, Y)))) (mark#(fib1(X1, X2)) -> active#(fib1(mark(X1), mark(X2))), active#(fib(N)) -> mark#(sel(N, fib1(s(0()), s(0()))))) (mark#(fib1(X1, X2)) -> active#(fib1(mark(X1), mark(X2))), active#(fib1(X, Y)) -> mark#(cons(X, fib1(Y, add(X, Y))))) (mark#(fib1(X1, X2)) -> active#(fib1(mark(X1), mark(X2))), active#(sel(0(), cons(X, XS))) -> mark#(X)) (mark#(fib1(X1, X2)) -> active#(fib1(mark(X1), mark(X2))), active#(sel(s(N), cons(X, XS))) -> mark#(sel(N, XS))) (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#(fib(N)) -> mark#(sel(N, fib1(s(0()), s(0()))))) (mark#(add(X1, X2)) -> active#(add(mark(X1), mark(X2))), active#(fib1(X, Y)) -> mark#(cons(X, fib1(Y, add(X, Y))))) (mark#(add(X1, X2)) -> active#(add(mark(X1), mark(X2))), active#(sel(0(), cons(X, XS))) -> mark#(X)) (mark#(add(X1, X2)) -> active#(add(mark(X1), mark(X2))), active#(sel(s(N), cons(X, XS))) -> mark#(sel(N, XS))) (mark#(sel(X1, X2)) -> mark#(X1), mark#(add(X1, X2)) -> active#(add(mark(X1), mark(X2)))) (mark#(sel(X1, X2)) -> mark#(X1), mark#(add(X1, X2)) -> mark#(X2)) (mark#(sel(X1, X2)) -> mark#(X1), mark#(add(X1, X2)) -> mark#(X1)) (mark#(sel(X1, X2)) -> mark#(X1), mark#(cons(X1, X2)) -> mark#(X1)) (mark#(sel(X1, X2)) -> mark#(X1), mark#(fib(X)) -> active#(fib(mark(X)))) (mark#(sel(X1, X2)) -> mark#(X1), mark#(fib(X)) -> mark#(X)) (mark#(sel(X1, X2)) -> mark#(X1), mark#(s(X)) -> mark#(X)) (mark#(sel(X1, X2)) -> mark#(X1), mark#(fib1(X1, X2)) -> active#(fib1(mark(X1), mark(X2)))) (mark#(sel(X1, X2)) -> mark#(X1), mark#(fib1(X1, X2)) -> mark#(X2)) (mark#(sel(X1, X2)) -> mark#(X1), mark#(fib1(X1, X2)) -> mark#(X1)) (mark#(sel(X1, X2)) -> mark#(X1), mark#(sel(X1, X2)) -> active#(sel(mark(X1), mark(X2)))) (mark#(sel(X1, X2)) -> mark#(X1), mark#(sel(X1, X2)) -> mark#(X2)) (mark#(sel(X1, X2)) -> mark#(X1), mark#(sel(X1, X2)) -> mark#(X1)) (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#(cons(X1, X2)) -> mark#(X1)) (mark#(cons(X1, X2)) -> mark#(X1), mark#(fib(X)) -> active#(fib(mark(X)))) (mark#(cons(X1, X2)) -> mark#(X1), mark#(fib(X)) -> mark#(X)) (mark#(cons(X1, X2)) -> mark#(X1), mark#(s(X)) -> mark#(X)) (mark#(cons(X1, X2)) -> mark#(X1), mark#(fib1(X1, X2)) -> active#(fib1(mark(X1), mark(X2)))) (mark#(cons(X1, X2)) -> mark#(X1), mark#(fib1(X1, X2)) -> mark#(X2)) (mark#(cons(X1, X2)) -> mark#(X1), mark#(fib1(X1, X2)) -> mark#(X1)) (mark#(cons(X1, X2)) -> mark#(X1), mark#(sel(X1, X2)) -> active#(sel(mark(X1), mark(X2)))) (mark#(cons(X1, X2)) -> mark#(X1), mark#(sel(X1, X2)) -> mark#(X2)) (mark#(cons(X1, X2)) -> mark#(X1), mark#(sel(X1, X2)) -> mark#(X1)) (active#(fib1(X, Y)) -> mark#(cons(X, fib1(Y, add(X, Y)))), mark#(add(X1, X2)) -> active#(add(mark(X1), mark(X2)))) (active#(fib1(X, Y)) -> mark#(cons(X, fib1(Y, add(X, Y)))), mark#(add(X1, X2)) -> mark#(X2)) (active#(fib1(X, Y)) -> mark#(cons(X, fib1(Y, add(X, Y)))), mark#(add(X1, X2)) -> mark#(X1)) (active#(fib1(X, Y)) -> mark#(cons(X, fib1(Y, add(X, Y)))), mark#(cons(X1, X2)) -> mark#(X1)) (active#(fib1(X, Y)) -> mark#(cons(X, fib1(Y, add(X, Y)))), mark#(fib(X)) -> active#(fib(mark(X)))) (active#(fib1(X, Y)) -> mark#(cons(X, fib1(Y, add(X, Y)))), mark#(fib(X)) -> mark#(X)) (active#(fib1(X, Y)) -> mark#(cons(X, fib1(Y, add(X, Y)))), mark#(s(X)) -> mark#(X)) (active#(fib1(X, Y)) -> mark#(cons(X, fib1(Y, add(X, Y)))), mark#(fib1(X1, X2)) -> active#(fib1(mark(X1), mark(X2)))) (active#(fib1(X, Y)) -> mark#(cons(X, fib1(Y, add(X, Y)))), mark#(fib1(X1, X2)) -> mark#(X2)) (active#(fib1(X, Y)) -> mark#(cons(X, fib1(Y, add(X, Y)))), mark#(fib1(X1, X2)) -> mark#(X1)) (active#(fib1(X, Y)) -> mark#(cons(X, fib1(Y, add(X, Y)))), mark#(sel(X1, X2)) -> active#(sel(mark(X1), mark(X2)))) (active#(fib1(X, Y)) -> mark#(cons(X, fib1(Y, add(X, Y)))), mark#(sel(X1, X2)) -> mark#(X2)) (active#(fib1(X, Y)) -> mark#(cons(X, fib1(Y, add(X, Y)))), mark#(sel(X1, X2)) -> mark#(X1)) (active#(fib(N)) -> mark#(sel(N, fib1(s(0()), s(0())))), mark#(sel(X1, X2)) -> mark#(X1)) (active#(fib(N)) -> mark#(sel(N, fib1(s(0()), s(0())))), mark#(sel(X1, X2)) -> mark#(X2)) (active#(fib(N)) -> mark#(sel(N, fib1(s(0()), s(0())))), mark#(sel(X1, X2)) -> active#(sel(mark(X1), mark(X2)))) (active#(fib(N)) -> mark#(sel(N, fib1(s(0()), s(0())))), mark#(fib1(X1, X2)) -> mark#(X1)) (active#(fib(N)) -> mark#(sel(N, fib1(s(0()), s(0())))), mark#(fib1(X1, X2)) -> mark#(X2)) (active#(fib(N)) -> mark#(sel(N, fib1(s(0()), s(0())))), mark#(fib1(X1, X2)) -> active#(fib1(mark(X1), mark(X2)))) (active#(fib(N)) -> mark#(sel(N, fib1(s(0()), s(0())))), mark#(s(X)) -> mark#(X)) (active#(fib(N)) -> mark#(sel(N, fib1(s(0()), s(0())))), mark#(fib(X)) -> mark#(X)) (active#(fib(N)) -> mark#(sel(N, fib1(s(0()), s(0())))), mark#(fib(X)) -> active#(fib(mark(X)))) (active#(fib(N)) -> mark#(sel(N, fib1(s(0()), s(0())))), mark#(cons(X1, X2)) -> mark#(X1)) (active#(fib(N)) -> mark#(sel(N, fib1(s(0()), s(0())))), mark#(add(X1, X2)) -> mark#(X1)) (active#(fib(N)) -> mark#(sel(N, fib1(s(0()), s(0())))), mark#(add(X1, X2)) -> mark#(X2)) (active#(fib(N)) -> mark#(sel(N, fib1(s(0()), s(0())))), mark#(add(X1, X2)) -> active#(add(mark(X1), mark(X2)))) (mark#(add(X1, X2)) -> mark#(X1), mark#(sel(X1, X2)) -> mark#(X1)) (mark#(add(X1, X2)) -> mark#(X1), mark#(sel(X1, X2)) -> mark#(X2)) (mark#(add(X1, X2)) -> mark#(X1), mark#(sel(X1, X2)) -> active#(sel(mark(X1), mark(X2)))) (mark#(add(X1, X2)) -> mark#(X1), mark#(fib1(X1, X2)) -> mark#(X1)) (mark#(add(X1, X2)) -> mark#(X1), mark#(fib1(X1, X2)) -> mark#(X2)) (mark#(add(X1, X2)) -> mark#(X1), mark#(fib1(X1, X2)) -> active#(fib1(mark(X1), mark(X2)))) (mark#(add(X1, X2)) -> mark#(X1), mark#(s(X)) -> mark#(X)) (mark#(add(X1, X2)) -> mark#(X1), mark#(fib(X)) -> mark#(X)) (mark#(add(X1, X2)) -> mark#(X1), mark#(fib(X)) -> active#(fib(mark(X)))) (mark#(add(X1, X2)) -> mark#(X1), mark#(cons(X1, X2)) -> mark#(X1)) (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#(fib1(X1, X2)) -> mark#(X1), mark#(sel(X1, X2)) -> mark#(X1)) (mark#(fib1(X1, X2)) -> mark#(X1), mark#(sel(X1, X2)) -> mark#(X2)) (mark#(fib1(X1, X2)) -> mark#(X1), mark#(sel(X1, X2)) -> active#(sel(mark(X1), mark(X2)))) (mark#(fib1(X1, X2)) -> mark#(X1), mark#(fib1(X1, X2)) -> mark#(X1)) (mark#(fib1(X1, X2)) -> mark#(X1), mark#(fib1(X1, X2)) -> mark#(X2)) (mark#(fib1(X1, X2)) -> mark#(X1), mark#(fib1(X1, X2)) -> active#(fib1(mark(X1), mark(X2)))) (mark#(fib1(X1, X2)) -> mark#(X1), mark#(s(X)) -> mark#(X)) (mark#(fib1(X1, X2)) -> mark#(X1), mark#(fib(X)) -> mark#(X)) (mark#(fib1(X1, X2)) -> mark#(X1), mark#(fib(X)) -> active#(fib(mark(X)))) (mark#(fib1(X1, X2)) -> mark#(X1), mark#(cons(X1, X2)) -> mark#(X1)) (mark#(fib1(X1, X2)) -> mark#(X1), mark#(add(X1, X2)) -> mark#(X1)) (mark#(fib1(X1, X2)) -> mark#(X1), mark#(add(X1, X2)) -> mark#(X2)) (mark#(fib1(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#(sel(X1, X2)) -> mark#(X1)) (active#(add(s(X), Y)) -> mark#(s(add(X, Y))), mark#(sel(X1, X2)) -> mark#(X2)) (active#(add(s(X), Y)) -> mark#(s(add(X, Y))), mark#(sel(X1, X2)) -> active#(sel(mark(X1), mark(X2)))) (active#(add(s(X), Y)) -> mark#(s(add(X, Y))), mark#(fib1(X1, X2)) -> mark#(X1)) (active#(add(s(X), Y)) -> mark#(s(add(X, Y))), mark#(fib1(X1, X2)) -> mark#(X2)) (active#(add(s(X), Y)) -> mark#(s(add(X, Y))), mark#(fib1(X1, X2)) -> active#(fib1(mark(X1), mark(X2)))) (active#(add(s(X), Y)) -> mark#(s(add(X, Y))), mark#(s(X)) -> mark#(X)) (active#(add(s(X), Y)) -> mark#(s(add(X, Y))), mark#(fib(X)) -> mark#(X)) (active#(add(s(X), Y)) -> mark#(s(add(X, Y))), mark#(fib(X)) -> active#(fib(mark(X)))) (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#(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)))) (mark#(fib(X)) -> active#(fib(mark(X))), active#(sel(s(N), cons(X, XS))) -> mark#(sel(N, XS))) (mark#(fib(X)) -> active#(fib(mark(X))), active#(sel(0(), cons(X, XS))) -> mark#(X)) (mark#(fib(X)) -> active#(fib(mark(X))), active#(fib1(X, Y)) -> mark#(cons(X, fib1(Y, add(X, Y))))) (mark#(fib(X)) -> active#(fib(mark(X))), active#(fib(N)) -> mark#(sel(N, fib1(s(0()), s(0()))))) (mark#(fib(X)) -> active#(fib(mark(X))), active#(add(s(X), Y)) -> mark#(s(add(X, Y)))) (mark#(fib(X)) -> active#(fib(mark(X))), active#(add(0(), X)) -> mark#(X)) (mark#(sel(X1, X2)) -> active#(sel(mark(X1), mark(X2))), active#(sel(s(N), cons(X, XS))) -> mark#(sel(N, XS))) (mark#(sel(X1, X2)) -> active#(sel(mark(X1), mark(X2))), active#(sel(0(), cons(X, XS))) -> mark#(X)) (mark#(sel(X1, X2)) -> active#(sel(mark(X1), mark(X2))), active#(fib1(X, Y)) -> mark#(cons(X, fib1(Y, add(X, Y))))) (mark#(sel(X1, X2)) -> active#(sel(mark(X1), mark(X2))), active#(fib(N)) -> mark#(sel(N, fib1(s(0()), s(0()))))) (mark#(sel(X1, X2)) -> active#(sel(mark(X1), mark(X2))), active#(add(s(X), Y)) -> mark#(s(add(X, Y)))) (mark#(sel(X1, X2)) -> active#(sel(mark(X1), mark(X2))), active#(add(0(), X)) -> mark#(X)) (active#(sel(0(), cons(X, XS))) -> mark#(X), mark#(sel(X1, X2)) -> mark#(X1)) (active#(sel(0(), cons(X, XS))) -> mark#(X), mark#(sel(X1, X2)) -> mark#(X2)) (active#(sel(0(), cons(X, XS))) -> mark#(X), mark#(sel(X1, X2)) -> active#(sel(mark(X1), mark(X2)))) (active#(sel(0(), cons(X, XS))) -> mark#(X), mark#(fib1(X1, X2)) -> mark#(X1)) (active#(sel(0(), cons(X, XS))) -> mark#(X), mark#(fib1(X1, X2)) -> mark#(X2)) (active#(sel(0(), cons(X, XS))) -> mark#(X), mark#(fib1(X1, X2)) -> active#(fib1(mark(X1), mark(X2)))) (active#(sel(0(), cons(X, XS))) -> mark#(X), mark#(s(X)) -> mark#(X)) (active#(sel(0(), cons(X, XS))) -> mark#(X), mark#(fib(X)) -> mark#(X)) (active#(sel(0(), cons(X, XS))) -> mark#(X), mark#(fib(X)) -> active#(fib(mark(X)))) (active#(sel(0(), cons(X, XS))) -> mark#(X), mark#(cons(X1, X2)) -> mark#(X1)) (active#(sel(0(), cons(X, XS))) -> mark#(X), mark#(add(X1, X2)) -> mark#(X1)) (active#(sel(0(), cons(X, XS))) -> mark#(X), mark#(add(X1, X2)) -> mark#(X2)) (active#(sel(0(), cons(X, XS))) -> mark#(X), mark#(add(X1, X2)) -> active#(add(mark(X1), mark(X2)))) (mark#(fib(X)) -> mark#(X), mark#(sel(X1, X2)) -> mark#(X1)) (mark#(fib(X)) -> mark#(X), mark#(sel(X1, X2)) -> mark#(X2)) (mark#(fib(X)) -> mark#(X), mark#(sel(X1, X2)) -> active#(sel(mark(X1), mark(X2)))) (mark#(fib(X)) -> mark#(X), mark#(fib1(X1, X2)) -> mark#(X1)) (mark#(fib(X)) -> mark#(X), mark#(fib1(X1, X2)) -> mark#(X2)) (mark#(fib(X)) -> mark#(X), mark#(fib1(X1, X2)) -> active#(fib1(mark(X1), mark(X2)))) (mark#(fib(X)) -> mark#(X), mark#(s(X)) -> mark#(X)) (mark#(fib(X)) -> mark#(X), mark#(fib(X)) -> mark#(X)) (mark#(fib(X)) -> mark#(X), mark#(fib(X)) -> active#(fib(mark(X)))) (mark#(fib(X)) -> mark#(X), mark#(cons(X1, X2)) -> mark#(X1)) (mark#(fib(X)) -> mark#(X), mark#(add(X1, X2)) -> mark#(X1)) (mark#(fib(X)) -> mark#(X), mark#(add(X1, X2)) -> mark#(X2)) (mark#(fib(X)) -> mark#(X), mark#(add(X1, X2)) -> active#(add(mark(X1), mark(X2)))) (mark#(fib1(X1, X2)) -> mark#(X2), mark#(sel(X1, X2)) -> mark#(X1)) (mark#(fib1(X1, X2)) -> mark#(X2), mark#(sel(X1, X2)) -> mark#(X2)) (mark#(fib1(X1, X2)) -> mark#(X2), mark#(sel(X1, X2)) -> active#(sel(mark(X1), mark(X2)))) (mark#(fib1(X1, X2)) -> mark#(X2), mark#(fib1(X1, X2)) -> mark#(X1)) (mark#(fib1(X1, X2)) -> mark#(X2), mark#(fib1(X1, X2)) -> mark#(X2)) (mark#(fib1(X1, X2)) -> mark#(X2), mark#(fib1(X1, X2)) -> active#(fib1(mark(X1), mark(X2)))) (mark#(fib1(X1, X2)) -> mark#(X2), mark#(s(X)) -> mark#(X)) (mark#(fib1(X1, X2)) -> mark#(X2), mark#(fib(X)) -> mark#(X)) (mark#(fib1(X1, X2)) -> mark#(X2), mark#(fib(X)) -> active#(fib(mark(X)))) (mark#(fib1(X1, X2)) -> mark#(X2), mark#(cons(X1, X2)) -> mark#(X1)) (mark#(fib1(X1, X2)) -> mark#(X2), mark#(add(X1, X2)) -> mark#(X1)) (mark#(fib1(X1, X2)) -> mark#(X2), mark#(add(X1, X2)) -> mark#(X2)) (mark#(fib1(X1, X2)) -> mark#(X2), mark#(add(X1, X2)) -> active#(add(mark(X1), mark(X2)))) (active#(sel(s(N), cons(X, XS))) -> mark#(sel(N, XS)), mark#(sel(X1, X2)) -> mark#(X1)) (active#(sel(s(N), cons(X, XS))) -> mark#(sel(N, XS)), mark#(sel(X1, X2)) -> mark#(X2)) (active#(sel(s(N), cons(X, XS))) -> mark#(sel(N, XS)), mark#(sel(X1, X2)) -> active#(sel(mark(X1), mark(X2)))) (active#(sel(s(N), cons(X, XS))) -> mark#(sel(N, XS)), mark#(fib1(X1, X2)) -> mark#(X1)) (active#(sel(s(N), cons(X, XS))) -> mark#(sel(N, XS)), mark#(fib1(X1, X2)) -> mark#(X2)) (active#(sel(s(N), cons(X, XS))) -> mark#(sel(N, XS)), mark#(fib1(X1, X2)) -> active#(fib1(mark(X1), mark(X2)))) (active#(sel(s(N), cons(X, XS))) -> mark#(sel(N, XS)), mark#(s(X)) -> mark#(X)) (active#(sel(s(N), cons(X, XS))) -> mark#(sel(N, XS)), mark#(fib(X)) -> mark#(X)) (active#(sel(s(N), cons(X, XS))) -> mark#(sel(N, XS)), mark#(fib(X)) -> active#(fib(mark(X)))) (active#(sel(s(N), cons(X, XS))) -> mark#(sel(N, XS)), mark#(cons(X1, X2)) -> mark#(X1)) (active#(sel(s(N), cons(X, XS))) -> mark#(sel(N, XS)), mark#(add(X1, X2)) -> mark#(X1)) (active#(sel(s(N), cons(X, XS))) -> mark#(sel(N, XS)), mark#(add(X1, X2)) -> mark#(X2)) (active#(sel(s(N), cons(X, XS))) -> mark#(sel(N, XS)), mark#(add(X1, X2)) -> active#(add(mark(X1), mark(X2)))) } SCCS: Scc: { mark#(sel(X1, X2)) -> mark#(X1), mark#(sel(X1, X2)) -> mark#(X2), mark#(sel(X1, X2)) -> active#(sel(mark(X1), mark(X2))), mark#(fib1(X1, X2)) -> mark#(X1), mark#(fib1(X1, X2)) -> mark#(X2), mark#(fib1(X1, X2)) -> active#(fib1(mark(X1), mark(X2))), mark#(s(X)) -> mark#(X), mark#(fib(X)) -> mark#(X), mark#(fib(X)) -> active#(fib(mark(X))), mark#(cons(X1, X2)) -> mark#(X1), mark#(add(X1, X2)) -> mark#(X1), mark#(add(X1, X2)) -> mark#(X2), mark#(add(X1, X2)) -> active#(add(mark(X1), mark(X2))), active#(sel(s(N), cons(X, XS))) -> mark#(sel(N, XS)), active#(sel(0(), cons(X, XS))) -> mark#(X), active#(fib1(X, Y)) -> mark#(cons(X, fib1(Y, add(X, Y)))), active#(fib(N)) -> mark#(sel(N, fib1(s(0()), s(0())))), active#(add(s(X), Y)) -> mark#(s(add(X, Y))), active#(add(0(), X)) -> mark#(X)} SCC: Strict: { mark#(sel(X1, X2)) -> mark#(X1), mark#(sel(X1, X2)) -> mark#(X2), mark#(sel(X1, X2)) -> active#(sel(mark(X1), mark(X2))), mark#(fib1(X1, X2)) -> mark#(X1), mark#(fib1(X1, X2)) -> mark#(X2), mark#(fib1(X1, X2)) -> active#(fib1(mark(X1), mark(X2))), mark#(s(X)) -> mark#(X), mark#(fib(X)) -> mark#(X), mark#(fib(X)) -> active#(fib(mark(X))), mark#(cons(X1, X2)) -> mark#(X1), mark#(add(X1, X2)) -> mark#(X1), mark#(add(X1, X2)) -> mark#(X2), mark#(add(X1, X2)) -> active#(add(mark(X1), mark(X2))), active#(sel(s(N), cons(X, XS))) -> mark#(sel(N, XS)), active#(sel(0(), cons(X, XS))) -> mark#(X), active#(fib1(X, Y)) -> mark#(cons(X, fib1(Y, add(X, Y)))), active#(fib(N)) -> mark#(sel(N, fib1(s(0()), s(0())))), active#(add(s(X), Y)) -> mark#(s(add(X, Y))), active#(add(0(), X)) -> mark#(X)} Weak: { mark(sel(X1, X2)) -> active(sel(mark(X1), mark(X2))), mark(fib1(X1, X2)) -> active(fib1(mark(X1), mark(X2))), mark(s(X)) -> active(s(mark(X))), mark(0()) -> active(0()), mark(fib(X)) -> active(fib(mark(X))), mark(cons(X1, X2)) -> active(cons(mark(X1), X2)), mark(add(X1, X2)) -> active(add(mark(X1), mark(X2))), sel(X1, mark(X2)) -> sel(X1, X2), sel(X1, active(X2)) -> sel(X1, X2), sel(mark(X1), X2) -> sel(X1, X2), sel(active(X1), X2) -> sel(X1, X2), fib1(X1, mark(X2)) -> fib1(X1, X2), fib1(X1, active(X2)) -> fib1(X1, X2), fib1(mark(X1), X2) -> fib1(X1, X2), fib1(active(X1), X2) -> fib1(X1, X2), s(mark(X)) -> s(X), s(active(X)) -> s(X), active(sel(s(N), cons(X, XS))) -> mark(sel(N, XS)), active(sel(0(), cons(X, XS))) -> mark(X), active(fib1(X, Y)) -> mark(cons(X, fib1(Y, add(X, Y)))), active(fib(N)) -> mark(sel(N, fib1(s(0()), s(0())))), active(add(s(X), Y)) -> mark(s(add(X, Y))), active(add(0(), X)) -> mark(X), fib(mark(X)) -> fib(X), fib(active(X)) -> fib(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), 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)} Fail