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