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