MAYBE TRS: { active(p(X)) -> p(active(X)), active(p(0())) -> mark(0()), active(p(s(X))) -> mark(X), active(s(X)) -> s(active(X)), active(leq(X1, X2)) -> leq(X1, active(X2)), active(leq(X1, X2)) -> leq(active(X1), X2), active(leq(0(), Y)) -> mark(true()), active(leq(s(X), 0())) -> mark(false()), active(leq(s(X), s(Y))) -> mark(leq(X, Y)), active(if(X1, X2, X3)) -> if(active(X1), X2, X3), active(if(true(), X, Y)) -> mark(X), active(if(false(), X, Y)) -> mark(Y), active(diff(X, Y)) -> mark(if(leq(X, Y), 0(), s(diff(p(X), Y)))), active(diff(X1, X2)) -> diff(X1, active(X2)), active(diff(X1, X2)) -> diff(active(X1), X2), p(mark(X)) -> mark(p(X)), p(ok(X)) -> ok(p(X)), s(mark(X)) -> mark(s(X)), s(ok(X)) -> ok(s(X)), leq(X1, mark(X2)) -> mark(leq(X1, X2)), leq(mark(X1), X2) -> mark(leq(X1, X2)), leq(ok(X1), ok(X2)) -> ok(leq(X1, X2)), if(mark(X1), X2, X3) -> mark(if(X1, X2, X3)), if(ok(X1), ok(X2), ok(X3)) -> ok(if(X1, X2, X3)), diff(X1, mark(X2)) -> mark(diff(X1, X2)), diff(mark(X1), X2) -> mark(diff(X1, X2)), diff(ok(X1), ok(X2)) -> ok(diff(X1, X2)), proper(0()) -> ok(0()), proper(p(X)) -> p(proper(X)), proper(s(X)) -> s(proper(X)), proper(true()) -> ok(true()), proper(leq(X1, X2)) -> leq(proper(X1), proper(X2)), proper(false()) -> ok(false()), proper(if(X1, X2, X3)) -> if(proper(X1), proper(X2), proper(X3)), proper(diff(X1, X2)) -> diff(proper(X1), proper(X2)), top(mark(X)) -> top(proper(X)), top(ok(X)) -> top(active(X))} DP: Strict: { active#(p(X)) -> active#(X), active#(p(X)) -> p#(active(X)), active#(s(X)) -> active#(X), active#(s(X)) -> s#(active(X)), active#(leq(X1, X2)) -> active#(X1), active#(leq(X1, X2)) -> active#(X2), active#(leq(X1, X2)) -> leq#(X1, active(X2)), active#(leq(X1, X2)) -> leq#(active(X1), X2), active#(leq(s(X), s(Y))) -> leq#(X, Y), active#(if(X1, X2, X3)) -> active#(X1), active#(if(X1, X2, X3)) -> if#(active(X1), X2, X3), active#(diff(X, Y)) -> p#(X), active#(diff(X, Y)) -> s#(diff(p(X), Y)), active#(diff(X, Y)) -> leq#(X, Y), active#(diff(X, Y)) -> if#(leq(X, Y), 0(), s(diff(p(X), Y))), active#(diff(X, Y)) -> diff#(p(X), Y), active#(diff(X1, X2)) -> active#(X1), active#(diff(X1, X2)) -> active#(X2), active#(diff(X1, X2)) -> diff#(X1, active(X2)), active#(diff(X1, X2)) -> diff#(active(X1), X2), p#(mark(X)) -> p#(X), p#(ok(X)) -> p#(X), s#(mark(X)) -> s#(X), s#(ok(X)) -> s#(X), leq#(X1, mark(X2)) -> leq#(X1, X2), leq#(mark(X1), X2) -> leq#(X1, X2), leq#(ok(X1), ok(X2)) -> leq#(X1, X2), if#(mark(X1), X2, X3) -> if#(X1, X2, X3), if#(ok(X1), ok(X2), ok(X3)) -> if#(X1, X2, X3), diff#(X1, mark(X2)) -> diff#(X1, X2), diff#(mark(X1), X2) -> diff#(X1, X2), diff#(ok(X1), ok(X2)) -> diff#(X1, X2), proper#(p(X)) -> p#(proper(X)), proper#(p(X)) -> proper#(X), proper#(s(X)) -> s#(proper(X)), proper#(s(X)) -> proper#(X), proper#(leq(X1, X2)) -> leq#(proper(X1), proper(X2)), proper#(leq(X1, X2)) -> proper#(X1), proper#(leq(X1, X2)) -> proper#(X2), proper#(if(X1, X2, X3)) -> if#(proper(X1), proper(X2), proper(X3)), proper#(if(X1, X2, X3)) -> proper#(X1), proper#(if(X1, X2, X3)) -> proper#(X2), proper#(if(X1, X2, X3)) -> proper#(X3), proper#(diff(X1, X2)) -> diff#(proper(X1), proper(X2)), proper#(diff(X1, X2)) -> proper#(X1), proper#(diff(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: { active(p(X)) -> p(active(X)), active(p(0())) -> mark(0()), active(p(s(X))) -> mark(X), active(s(X)) -> s(active(X)), active(leq(X1, X2)) -> leq(X1, active(X2)), active(leq(X1, X2)) -> leq(active(X1), X2), active(leq(0(), Y)) -> mark(true()), active(leq(s(X), 0())) -> mark(false()), active(leq(s(X), s(Y))) -> mark(leq(X, Y)), active(if(X1, X2, X3)) -> if(active(X1), X2, X3), active(if(true(), X, Y)) -> mark(X), active(if(false(), X, Y)) -> mark(Y), active(diff(X, Y)) -> mark(if(leq(X, Y), 0(), s(diff(p(X), Y)))), active(diff(X1, X2)) -> diff(X1, active(X2)), active(diff(X1, X2)) -> diff(active(X1), X2), p(mark(X)) -> mark(p(X)), p(ok(X)) -> ok(p(X)), s(mark(X)) -> mark(s(X)), s(ok(X)) -> ok(s(X)), leq(X1, mark(X2)) -> mark(leq(X1, X2)), leq(mark(X1), X2) -> mark(leq(X1, X2)), leq(ok(X1), ok(X2)) -> ok(leq(X1, X2)), if(mark(X1), X2, X3) -> mark(if(X1, X2, X3)), if(ok(X1), ok(X2), ok(X3)) -> ok(if(X1, X2, X3)), diff(X1, mark(X2)) -> mark(diff(X1, X2)), diff(mark(X1), X2) -> mark(diff(X1, X2)), diff(ok(X1), ok(X2)) -> ok(diff(X1, X2)), proper(0()) -> ok(0()), proper(p(X)) -> p(proper(X)), proper(s(X)) -> s(proper(X)), proper(true()) -> ok(true()), proper(leq(X1, X2)) -> leq(proper(X1), proper(X2)), proper(false()) -> ok(false()), proper(if(X1, X2, X3)) -> if(proper(X1), proper(X2), proper(X3)), proper(diff(X1, X2)) -> diff(proper(X1), proper(X2)), top(mark(X)) -> top(proper(X)), top(ok(X)) -> top(active(X))} EDG: { (active#(s(X)) -> active#(X), active#(diff(X1, X2)) -> diff#(active(X1), X2)) (active#(s(X)) -> active#(X), active#(diff(X1, X2)) -> diff#(X1, active(X2))) (active#(s(X)) -> active#(X), active#(diff(X1, X2)) -> active#(X2)) (active#(s(X)) -> active#(X), active#(diff(X1, X2)) -> active#(X1)) (active#(s(X)) -> active#(X), active#(diff(X, Y)) -> diff#(p(X), Y)) (active#(s(X)) -> active#(X), active#(diff(X, Y)) -> if#(leq(X, Y), 0(), s(diff(p(X), Y)))) (active#(s(X)) -> active#(X), active#(diff(X, Y)) -> leq#(X, Y)) (active#(s(X)) -> active#(X), active#(diff(X, Y)) -> s#(diff(p(X), Y))) (active#(s(X)) -> active#(X), active#(diff(X, Y)) -> p#(X)) (active#(s(X)) -> active#(X), active#(if(X1, X2, X3)) -> if#(active(X1), X2, X3)) (active#(s(X)) -> active#(X), active#(if(X1, X2, X3)) -> active#(X1)) (active#(s(X)) -> active#(X), active#(leq(s(X), s(Y))) -> leq#(X, Y)) (active#(s(X)) -> active#(X), active#(leq(X1, X2)) -> leq#(active(X1), X2)) (active#(s(X)) -> active#(X), active#(leq(X1, X2)) -> leq#(X1, active(X2))) (active#(s(X)) -> active#(X), active#(leq(X1, X2)) -> active#(X2)) (active#(s(X)) -> active#(X), active#(leq(X1, X2)) -> active#(X1)) (active#(s(X)) -> active#(X), active#(s(X)) -> s#(active(X))) (active#(s(X)) -> active#(X), active#(s(X)) -> active#(X)) (active#(s(X)) -> active#(X), active#(p(X)) -> p#(active(X))) (active#(s(X)) -> active#(X), active#(p(X)) -> active#(X)) (p#(mark(X)) -> p#(X), p#(ok(X)) -> p#(X)) (p#(mark(X)) -> p#(X), p#(mark(X)) -> p#(X)) (s#(mark(X)) -> s#(X), s#(ok(X)) -> s#(X)) (s#(mark(X)) -> s#(X), s#(mark(X)) -> s#(X)) (proper#(p(X)) -> proper#(X), proper#(diff(X1, X2)) -> proper#(X2)) (proper#(p(X)) -> proper#(X), proper#(diff(X1, X2)) -> proper#(X1)) (proper#(p(X)) -> proper#(X), proper#(diff(X1, X2)) -> diff#(proper(X1), proper(X2))) (proper#(p(X)) -> proper#(X), proper#(if(X1, X2, X3)) -> proper#(X3)) (proper#(p(X)) -> proper#(X), proper#(if(X1, X2, X3)) -> proper#(X2)) (proper#(p(X)) -> proper#(X), proper#(if(X1, X2, X3)) -> proper#(X1)) (proper#(p(X)) -> proper#(X), proper#(if(X1, X2, X3)) -> if#(proper(X1), proper(X2), proper(X3))) (proper#(p(X)) -> proper#(X), proper#(leq(X1, X2)) -> proper#(X2)) (proper#(p(X)) -> proper#(X), proper#(leq(X1, X2)) -> proper#(X1)) (proper#(p(X)) -> proper#(X), proper#(leq(X1, X2)) -> leq#(proper(X1), proper(X2))) (proper#(p(X)) -> proper#(X), proper#(s(X)) -> proper#(X)) (proper#(p(X)) -> proper#(X), proper#(s(X)) -> s#(proper(X))) (proper#(p(X)) -> proper#(X), proper#(p(X)) -> proper#(X)) (proper#(p(X)) -> proper#(X), proper#(p(X)) -> p#(proper(X))) (top#(mark(X)) -> proper#(X), proper#(diff(X1, X2)) -> proper#(X2)) (top#(mark(X)) -> proper#(X), proper#(diff(X1, X2)) -> proper#(X1)) (top#(mark(X)) -> proper#(X), proper#(diff(X1, X2)) -> diff#(proper(X1), proper(X2))) (top#(mark(X)) -> proper#(X), proper#(if(X1, X2, X3)) -> proper#(X3)) (top#(mark(X)) -> proper#(X), proper#(if(X1, X2, X3)) -> proper#(X2)) (top#(mark(X)) -> proper#(X), proper#(if(X1, X2, X3)) -> proper#(X1)) (top#(mark(X)) -> proper#(X), proper#(if(X1, X2, X3)) -> if#(proper(X1), proper(X2), proper(X3))) (top#(mark(X)) -> proper#(X), proper#(leq(X1, X2)) -> proper#(X2)) (top#(mark(X)) -> proper#(X), proper#(leq(X1, X2)) -> proper#(X1)) (top#(mark(X)) -> proper#(X), proper#(leq(X1, X2)) -> leq#(proper(X1), proper(X2))) (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#(p(X)) -> proper#(X)) (top#(mark(X)) -> proper#(X), proper#(p(X)) -> p#(proper(X))) (active#(leq(X1, X2)) -> leq#(active(X1), X2), leq#(ok(X1), ok(X2)) -> leq#(X1, X2)) (active#(leq(X1, X2)) -> leq#(active(X1), X2), leq#(mark(X1), X2) -> leq#(X1, X2)) (active#(leq(X1, X2)) -> leq#(active(X1), X2), leq#(X1, mark(X2)) -> leq#(X1, X2)) (active#(leq(X1, X2)) -> active#(X1), active#(diff(X1, X2)) -> diff#(active(X1), X2)) (active#(leq(X1, X2)) -> active#(X1), active#(diff(X1, X2)) -> diff#(X1, active(X2))) (active#(leq(X1, X2)) -> active#(X1), active#(diff(X1, X2)) -> active#(X2)) (active#(leq(X1, X2)) -> active#(X1), active#(diff(X1, X2)) -> active#(X1)) (active#(leq(X1, X2)) -> active#(X1), active#(diff(X, Y)) -> diff#(p(X), Y)) (active#(leq(X1, X2)) -> active#(X1), active#(diff(X, Y)) -> if#(leq(X, Y), 0(), s(diff(p(X), Y)))) (active#(leq(X1, X2)) -> active#(X1), active#(diff(X, Y)) -> leq#(X, Y)) (active#(leq(X1, X2)) -> active#(X1), active#(diff(X, Y)) -> s#(diff(p(X), Y))) (active#(leq(X1, X2)) -> active#(X1), active#(diff(X, Y)) -> p#(X)) (active#(leq(X1, X2)) -> active#(X1), active#(if(X1, X2, X3)) -> if#(active(X1), X2, X3)) (active#(leq(X1, X2)) -> active#(X1), active#(if(X1, X2, X3)) -> active#(X1)) (active#(leq(X1, X2)) -> active#(X1), active#(leq(s(X), s(Y))) -> leq#(X, Y)) (active#(leq(X1, X2)) -> active#(X1), active#(leq(X1, X2)) -> leq#(active(X1), X2)) (active#(leq(X1, X2)) -> active#(X1), active#(leq(X1, X2)) -> leq#(X1, active(X2))) (active#(leq(X1, X2)) -> active#(X1), active#(leq(X1, X2)) -> active#(X2)) (active#(leq(X1, X2)) -> active#(X1), active#(leq(X1, X2)) -> active#(X1)) (active#(leq(X1, X2)) -> active#(X1), active#(s(X)) -> s#(active(X))) (active#(leq(X1, X2)) -> active#(X1), active#(s(X)) -> active#(X)) (active#(leq(X1, X2)) -> active#(X1), active#(p(X)) -> p#(active(X))) (active#(leq(X1, X2)) -> active#(X1), active#(p(X)) -> active#(X)) (active#(diff(X1, X2)) -> active#(X1), active#(diff(X1, X2)) -> diff#(active(X1), X2)) (active#(diff(X1, X2)) -> active#(X1), active#(diff(X1, X2)) -> diff#(X1, active(X2))) (active#(diff(X1, X2)) -> active#(X1), active#(diff(X1, X2)) -> active#(X2)) (active#(diff(X1, X2)) -> active#(X1), active#(diff(X1, X2)) -> active#(X1)) (active#(diff(X1, X2)) -> active#(X1), active#(diff(X, Y)) -> diff#(p(X), Y)) (active#(diff(X1, X2)) -> active#(X1), active#(diff(X, Y)) -> if#(leq(X, Y), 0(), s(diff(p(X), Y)))) (active#(diff(X1, X2)) -> active#(X1), active#(diff(X, Y)) -> leq#(X, Y)) (active#(diff(X1, X2)) -> active#(X1), active#(diff(X, Y)) -> s#(diff(p(X), Y))) (active#(diff(X1, X2)) -> active#(X1), active#(diff(X, Y)) -> p#(X)) (active#(diff(X1, X2)) -> active#(X1), active#(if(X1, X2, X3)) -> if#(active(X1), X2, X3)) (active#(diff(X1, X2)) -> active#(X1), active#(if(X1, X2, X3)) -> active#(X1)) (active#(diff(X1, X2)) -> active#(X1), active#(leq(s(X), s(Y))) -> leq#(X, Y)) (active#(diff(X1, X2)) -> active#(X1), active#(leq(X1, X2)) -> leq#(active(X1), X2)) (active#(diff(X1, X2)) -> active#(X1), active#(leq(X1, X2)) -> leq#(X1, active(X2))) (active#(diff(X1, X2)) -> active#(X1), active#(leq(X1, X2)) -> active#(X2)) (active#(diff(X1, X2)) -> active#(X1), active#(leq(X1, X2)) -> active#(X1)) (active#(diff(X1, X2)) -> active#(X1), active#(s(X)) -> s#(active(X))) (active#(diff(X1, X2)) -> active#(X1), active#(s(X)) -> active#(X)) (active#(diff(X1, X2)) -> active#(X1), active#(p(X)) -> p#(active(X))) (active#(diff(X1, X2)) -> active#(X1), active#(p(X)) -> active#(X)) (proper#(if(X1, X2, X3)) -> proper#(X1), proper#(diff(X1, X2)) -> proper#(X2)) (proper#(if(X1, X2, X3)) -> proper#(X1), proper#(diff(X1, X2)) -> proper#(X1)) (proper#(if(X1, X2, X3)) -> proper#(X1), proper#(diff(X1, X2)) -> diff#(proper(X1), proper(X2))) (proper#(if(X1, X2, X3)) -> proper#(X1), proper#(if(X1, X2, X3)) -> proper#(X3)) (proper#(if(X1, X2, X3)) -> proper#(X1), proper#(if(X1, X2, X3)) -> proper#(X2)) (proper#(if(X1, X2, X3)) -> proper#(X1), proper#(if(X1, X2, X3)) -> proper#(X1)) (proper#(if(X1, X2, X3)) -> proper#(X1), proper#(if(X1, X2, X3)) -> if#(proper(X1), proper(X2), proper(X3))) (proper#(if(X1, X2, X3)) -> proper#(X1), proper#(leq(X1, X2)) -> proper#(X2)) (proper#(if(X1, X2, X3)) -> proper#(X1), proper#(leq(X1, X2)) -> proper#(X1)) (proper#(if(X1, X2, X3)) -> proper#(X1), proper#(leq(X1, X2)) -> leq#(proper(X1), proper(X2))) (proper#(if(X1, X2, X3)) -> proper#(X1), proper#(s(X)) -> proper#(X)) (proper#(if(X1, X2, X3)) -> proper#(X1), proper#(s(X)) -> s#(proper(X))) (proper#(if(X1, X2, X3)) -> proper#(X1), proper#(p(X)) -> proper#(X)) (proper#(if(X1, X2, X3)) -> proper#(X1), proper#(p(X)) -> p#(proper(X))) (leq#(X1, mark(X2)) -> leq#(X1, X2), leq#(ok(X1), ok(X2)) -> leq#(X1, X2)) (leq#(X1, mark(X2)) -> leq#(X1, X2), leq#(mark(X1), X2) -> leq#(X1, X2)) (leq#(X1, mark(X2)) -> leq#(X1, X2), leq#(X1, mark(X2)) -> leq#(X1, X2)) (leq#(ok(X1), ok(X2)) -> leq#(X1, X2), leq#(ok(X1), ok(X2)) -> leq#(X1, X2)) (leq#(ok(X1), ok(X2)) -> leq#(X1, X2), leq#(mark(X1), X2) -> leq#(X1, X2)) (leq#(ok(X1), ok(X2)) -> leq#(X1, X2), leq#(X1, mark(X2)) -> leq#(X1, X2)) (diff#(mark(X1), X2) -> diff#(X1, X2), diff#(ok(X1), ok(X2)) -> diff#(X1, X2)) (diff#(mark(X1), X2) -> diff#(X1, X2), diff#(mark(X1), X2) -> diff#(X1, X2)) (diff#(mark(X1), X2) -> diff#(X1, X2), diff#(X1, mark(X2)) -> diff#(X1, X2)) (active#(diff(X, Y)) -> if#(leq(X, Y), 0(), s(diff(p(X), Y))), if#(mark(X1), X2, X3) -> if#(X1, X2, X3)) (active#(if(X1, X2, X3)) -> if#(active(X1), X2, X3), if#(ok(X1), ok(X2), ok(X3)) -> if#(X1, X2, X3)) (active#(if(X1, X2, X3)) -> if#(active(X1), X2, X3), if#(mark(X1), X2, X3) -> if#(X1, X2, X3)) (if#(ok(X1), ok(X2), ok(X3)) -> if#(X1, X2, X3), if#(ok(X1), ok(X2), ok(X3)) -> if#(X1, X2, X3)) (if#(ok(X1), ok(X2), ok(X3)) -> if#(X1, X2, X3), if#(mark(X1), X2, X3) -> if#(X1, X2, X3)) (active#(p(X)) -> p#(active(X)), p#(ok(X)) -> p#(X)) (active#(p(X)) -> p#(active(X)), p#(mark(X)) -> p#(X)) (proper#(p(X)) -> p#(proper(X)), p#(ok(X)) -> p#(X)) (proper#(p(X)) -> p#(proper(X)), p#(mark(X)) -> p#(X)) (top#(mark(X)) -> top#(proper(X)), top#(ok(X)) -> top#(active(X))) (top#(mark(X)) -> top#(proper(X)), top#(ok(X)) -> active#(X)) (top#(mark(X)) -> top#(proper(X)), top#(mark(X)) -> top#(proper(X))) (top#(mark(X)) -> top#(proper(X)), top#(mark(X)) -> proper#(X)) (active#(leq(s(X), s(Y))) -> leq#(X, Y), leq#(ok(X1), ok(X2)) -> leq#(X1, X2)) (active#(leq(s(X), s(Y))) -> leq#(X, Y), leq#(mark(X1), X2) -> leq#(X1, X2)) (active#(leq(s(X), s(Y))) -> leq#(X, Y), leq#(X1, mark(X2)) -> leq#(X1, X2)) (proper#(if(X1, X2, X3)) -> if#(proper(X1), proper(X2), proper(X3)), if#(ok(X1), ok(X2), ok(X3)) -> if#(X1, X2, X3)) (proper#(if(X1, X2, X3)) -> if#(proper(X1), proper(X2), proper(X3)), if#(mark(X1), X2, X3) -> if#(X1, X2, X3)) (active#(leq(X1, X2)) -> leq#(X1, active(X2)), leq#(ok(X1), ok(X2)) -> leq#(X1, X2)) (active#(leq(X1, X2)) -> leq#(X1, active(X2)), leq#(mark(X1), X2) -> leq#(X1, X2)) (active#(leq(X1, X2)) -> leq#(X1, active(X2)), leq#(X1, mark(X2)) -> leq#(X1, X2)) (proper#(leq(X1, X2)) -> leq#(proper(X1), proper(X2)), leq#(ok(X1), ok(X2)) -> leq#(X1, X2)) (proper#(leq(X1, X2)) -> leq#(proper(X1), proper(X2)), leq#(mark(X1), X2) -> leq#(X1, X2)) (proper#(leq(X1, X2)) -> leq#(proper(X1), proper(X2)), leq#(X1, mark(X2)) -> leq#(X1, X2)) (active#(leq(X1, X2)) -> active#(X2), active#(diff(X1, X2)) -> diff#(active(X1), X2)) (active#(leq(X1, X2)) -> active#(X2), active#(diff(X1, X2)) -> diff#(X1, active(X2))) (active#(leq(X1, X2)) -> active#(X2), active#(diff(X1, X2)) -> active#(X2)) (active#(leq(X1, X2)) -> active#(X2), active#(diff(X1, X2)) -> active#(X1)) (active#(leq(X1, X2)) -> active#(X2), active#(diff(X, Y)) -> diff#(p(X), Y)) (active#(leq(X1, X2)) -> active#(X2), active#(diff(X, Y)) -> if#(leq(X, Y), 0(), s(diff(p(X), Y)))) (active#(leq(X1, X2)) -> active#(X2), active#(diff(X, Y)) -> leq#(X, Y)) (active#(leq(X1, X2)) -> active#(X2), active#(diff(X, Y)) -> s#(diff(p(X), Y))) (active#(leq(X1, X2)) -> active#(X2), active#(diff(X, Y)) -> p#(X)) (active#(leq(X1, X2)) -> active#(X2), active#(if(X1, X2, X3)) -> if#(active(X1), X2, X3)) (active#(leq(X1, X2)) -> active#(X2), active#(if(X1, X2, X3)) -> active#(X1)) (active#(leq(X1, X2)) -> active#(X2), active#(leq(s(X), s(Y))) -> leq#(X, Y)) (active#(leq(X1, X2)) -> active#(X2), active#(leq(X1, X2)) -> leq#(active(X1), X2)) (active#(leq(X1, X2)) -> active#(X2), active#(leq(X1, X2)) -> leq#(X1, active(X2))) (active#(leq(X1, X2)) -> active#(X2), active#(leq(X1, X2)) -> active#(X2)) (active#(leq(X1, X2)) -> active#(X2), active#(leq(X1, X2)) -> active#(X1)) (active#(leq(X1, X2)) -> active#(X2), active#(s(X)) -> s#(active(X))) (active#(leq(X1, X2)) -> active#(X2), active#(s(X)) -> active#(X)) (active#(leq(X1, X2)) -> active#(X2), active#(p(X)) -> p#(active(X))) (active#(leq(X1, X2)) -> active#(X2), active#(p(X)) -> active#(X)) (proper#(leq(X1, X2)) -> proper#(X2), proper#(diff(X1, X2)) -> proper#(X2)) (proper#(leq(X1, X2)) -> proper#(X2), proper#(diff(X1, X2)) -> proper#(X1)) (proper#(leq(X1, X2)) -> proper#(X2), proper#(diff(X1, X2)) -> diff#(proper(X1), proper(X2))) (proper#(leq(X1, X2)) -> proper#(X2), proper#(if(X1, X2, X3)) -> proper#(X3)) (proper#(leq(X1, X2)) -> proper#(X2), proper#(if(X1, X2, X3)) -> proper#(X2)) (proper#(leq(X1, X2)) -> proper#(X2), proper#(if(X1, X2, X3)) -> proper#(X1)) (proper#(leq(X1, X2)) -> proper#(X2), proper#(if(X1, X2, X3)) -> if#(proper(X1), proper(X2), proper(X3))) (proper#(leq(X1, X2)) -> proper#(X2), proper#(leq(X1, X2)) -> proper#(X2)) (proper#(leq(X1, X2)) -> proper#(X2), proper#(leq(X1, X2)) -> proper#(X1)) (proper#(leq(X1, X2)) -> proper#(X2), proper#(leq(X1, X2)) -> leq#(proper(X1), proper(X2))) (proper#(leq(X1, X2)) -> proper#(X2), proper#(s(X)) -> proper#(X)) (proper#(leq(X1, X2)) -> proper#(X2), proper#(s(X)) -> s#(proper(X))) (proper#(leq(X1, X2)) -> proper#(X2), proper#(p(X)) -> proper#(X)) (proper#(leq(X1, X2)) -> proper#(X2), proper#(p(X)) -> p#(proper(X))) (proper#(diff(X1, X2)) -> proper#(X2), proper#(diff(X1, X2)) -> proper#(X2)) (proper#(diff(X1, X2)) -> proper#(X2), proper#(diff(X1, X2)) -> proper#(X1)) (proper#(diff(X1, X2)) -> proper#(X2), proper#(diff(X1, X2)) -> diff#(proper(X1), proper(X2))) (proper#(diff(X1, X2)) -> proper#(X2), proper#(if(X1, X2, X3)) -> proper#(X3)) (proper#(diff(X1, X2)) -> proper#(X2), proper#(if(X1, X2, X3)) -> proper#(X2)) (proper#(diff(X1, X2)) -> proper#(X2), proper#(if(X1, X2, X3)) -> proper#(X1)) (proper#(diff(X1, X2)) -> proper#(X2), proper#(if(X1, X2, X3)) -> if#(proper(X1), proper(X2), proper(X3))) (proper#(diff(X1, X2)) -> proper#(X2), proper#(leq(X1, X2)) -> proper#(X2)) (proper#(diff(X1, X2)) -> proper#(X2), proper#(leq(X1, X2)) -> proper#(X1)) (proper#(diff(X1, X2)) -> proper#(X2), proper#(leq(X1, X2)) -> leq#(proper(X1), proper(X2))) (proper#(diff(X1, X2)) -> proper#(X2), proper#(s(X)) -> proper#(X)) (proper#(diff(X1, X2)) -> proper#(X2), proper#(s(X)) -> s#(proper(X))) (proper#(diff(X1, X2)) -> proper#(X2), proper#(p(X)) -> proper#(X)) (proper#(diff(X1, X2)) -> proper#(X2), proper#(p(X)) -> p#(proper(X))) (proper#(if(X1, X2, X3)) -> proper#(X2), proper#(p(X)) -> p#(proper(X))) (proper#(if(X1, X2, X3)) -> proper#(X2), proper#(p(X)) -> proper#(X)) (proper#(if(X1, X2, X3)) -> proper#(X2), proper#(s(X)) -> s#(proper(X))) (proper#(if(X1, X2, X3)) -> proper#(X2), proper#(s(X)) -> proper#(X)) (proper#(if(X1, X2, X3)) -> proper#(X2), proper#(leq(X1, X2)) -> leq#(proper(X1), proper(X2))) (proper#(if(X1, X2, X3)) -> proper#(X2), proper#(leq(X1, X2)) -> proper#(X1)) (proper#(if(X1, X2, X3)) -> proper#(X2), proper#(leq(X1, X2)) -> proper#(X2)) (proper#(if(X1, X2, X3)) -> proper#(X2), proper#(if(X1, X2, X3)) -> if#(proper(X1), proper(X2), proper(X3))) (proper#(if(X1, X2, X3)) -> proper#(X2), proper#(if(X1, X2, X3)) -> proper#(X1)) (proper#(if(X1, X2, X3)) -> proper#(X2), proper#(if(X1, X2, X3)) -> proper#(X2)) (proper#(if(X1, X2, X3)) -> proper#(X2), proper#(if(X1, X2, X3)) -> proper#(X3)) (proper#(if(X1, X2, X3)) -> proper#(X2), proper#(diff(X1, X2)) -> diff#(proper(X1), proper(X2))) (proper#(if(X1, X2, X3)) -> proper#(X2), proper#(diff(X1, X2)) -> proper#(X1)) (proper#(if(X1, X2, X3)) -> proper#(X2), proper#(diff(X1, X2)) -> proper#(X2)) (active#(diff(X1, X2)) -> active#(X2), active#(p(X)) -> active#(X)) (active#(diff(X1, X2)) -> active#(X2), active#(p(X)) -> p#(active(X))) (active#(diff(X1, X2)) -> active#(X2), active#(s(X)) -> active#(X)) (active#(diff(X1, X2)) -> active#(X2), active#(s(X)) -> s#(active(X))) (active#(diff(X1, X2)) -> active#(X2), active#(leq(X1, X2)) -> active#(X1)) (active#(diff(X1, X2)) -> active#(X2), active#(leq(X1, X2)) -> active#(X2)) (active#(diff(X1, X2)) -> active#(X2), active#(leq(X1, X2)) -> leq#(X1, active(X2))) (active#(diff(X1, X2)) -> active#(X2), active#(leq(X1, X2)) -> leq#(active(X1), X2)) (active#(diff(X1, X2)) -> active#(X2), active#(leq(s(X), s(Y))) -> leq#(X, Y)) (active#(diff(X1, X2)) -> active#(X2), active#(if(X1, X2, X3)) -> active#(X1)) (active#(diff(X1, X2)) -> active#(X2), active#(if(X1, X2, X3)) -> if#(active(X1), X2, X3)) (active#(diff(X1, X2)) -> active#(X2), active#(diff(X, Y)) -> p#(X)) (active#(diff(X1, X2)) -> active#(X2), active#(diff(X, Y)) -> s#(diff(p(X), Y))) (active#(diff(X1, X2)) -> active#(X2), active#(diff(X, Y)) -> leq#(X, Y)) (active#(diff(X1, X2)) -> active#(X2), active#(diff(X, Y)) -> if#(leq(X, Y), 0(), s(diff(p(X), Y)))) (active#(diff(X1, X2)) -> active#(X2), active#(diff(X, Y)) -> diff#(p(X), Y)) (active#(diff(X1, X2)) -> active#(X2), active#(diff(X1, X2)) -> active#(X1)) (active#(diff(X1, X2)) -> active#(X2), active#(diff(X1, X2)) -> active#(X2)) (active#(diff(X1, X2)) -> active#(X2), active#(diff(X1, X2)) -> diff#(X1, active(X2))) (active#(diff(X1, X2)) -> active#(X2), active#(diff(X1, X2)) -> diff#(active(X1), X2)) (proper#(diff(X1, X2)) -> diff#(proper(X1), proper(X2)), diff#(X1, mark(X2)) -> diff#(X1, X2)) (proper#(diff(X1, X2)) -> diff#(proper(X1), proper(X2)), diff#(mark(X1), X2) -> diff#(X1, X2)) (proper#(diff(X1, X2)) -> diff#(proper(X1), proper(X2)), diff#(ok(X1), ok(X2)) -> diff#(X1, X2)) (active#(diff(X1, X2)) -> diff#(X1, active(X2)), diff#(X1, mark(X2)) -> diff#(X1, X2)) (active#(diff(X1, X2)) -> diff#(X1, active(X2)), diff#(mark(X1), X2) -> diff#(X1, X2)) (active#(diff(X1, X2)) -> diff#(X1, active(X2)), diff#(ok(X1), ok(X2)) -> diff#(X1, X2)) (active#(diff(X, Y)) -> s#(diff(p(X), Y)), s#(mark(X)) -> s#(X)) (active#(diff(X, Y)) -> s#(diff(p(X), Y)), s#(ok(X)) -> s#(X)) (active#(diff(X, Y)) -> leq#(X, Y), leq#(X1, mark(X2)) -> leq#(X1, X2)) (active#(diff(X, Y)) -> leq#(X, Y), leq#(mark(X1), X2) -> leq#(X1, X2)) (active#(diff(X, Y)) -> leq#(X, Y), leq#(ok(X1), ok(X2)) -> leq#(X1, X2)) (top#(ok(X)) -> top#(active(X)), top#(mark(X)) -> proper#(X)) (top#(ok(X)) -> top#(active(X)), top#(mark(X)) -> top#(proper(X))) (top#(ok(X)) -> top#(active(X)), top#(ok(X)) -> active#(X)) (top#(ok(X)) -> top#(active(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)) (proper#(if(X1, X2, X3)) -> proper#(X3), proper#(p(X)) -> p#(proper(X))) (proper#(if(X1, X2, X3)) -> proper#(X3), proper#(p(X)) -> proper#(X)) (proper#(if(X1, X2, X3)) -> proper#(X3), proper#(s(X)) -> s#(proper(X))) (proper#(if(X1, X2, X3)) -> proper#(X3), proper#(s(X)) -> proper#(X)) (proper#(if(X1, X2, X3)) -> proper#(X3), proper#(leq(X1, X2)) -> leq#(proper(X1), proper(X2))) (proper#(if(X1, X2, X3)) -> proper#(X3), proper#(leq(X1, X2)) -> proper#(X1)) (proper#(if(X1, X2, X3)) -> proper#(X3), proper#(leq(X1, X2)) -> proper#(X2)) (proper#(if(X1, X2, X3)) -> proper#(X3), proper#(if(X1, X2, X3)) -> if#(proper(X1), proper(X2), proper(X3))) (proper#(if(X1, X2, X3)) -> proper#(X3), proper#(if(X1, X2, X3)) -> proper#(X1)) (proper#(if(X1, X2, X3)) -> proper#(X3), proper#(if(X1, X2, X3)) -> proper#(X2)) (proper#(if(X1, X2, X3)) -> proper#(X3), proper#(if(X1, X2, X3)) -> proper#(X3)) (proper#(if(X1, X2, X3)) -> proper#(X3), proper#(diff(X1, X2)) -> diff#(proper(X1), proper(X2))) (proper#(if(X1, X2, X3)) -> proper#(X3), proper#(diff(X1, X2)) -> proper#(X1)) (proper#(if(X1, X2, X3)) -> proper#(X3), proper#(diff(X1, X2)) -> proper#(X2)) (if#(mark(X1), X2, X3) -> if#(X1, X2, X3), if#(mark(X1), X2, X3) -> if#(X1, X2, X3)) (if#(mark(X1), X2, X3) -> if#(X1, X2, X3), if#(ok(X1), ok(X2), ok(X3)) -> if#(X1, X2, X3)) (active#(diff(X, Y)) -> diff#(p(X), Y), diff#(X1, mark(X2)) -> diff#(X1, X2)) (active#(diff(X, Y)) -> diff#(p(X), Y), diff#(mark(X1), X2) -> diff#(X1, X2)) (active#(diff(X, Y)) -> diff#(p(X), Y), diff#(ok(X1), ok(X2)) -> diff#(X1, X2)) (diff#(ok(X1), ok(X2)) -> diff#(X1, X2), diff#(X1, mark(X2)) -> diff#(X1, X2)) (diff#(ok(X1), ok(X2)) -> diff#(X1, X2), diff#(mark(X1), X2) -> diff#(X1, X2)) (diff#(ok(X1), ok(X2)) -> diff#(X1, X2), diff#(ok(X1), ok(X2)) -> diff#(X1, X2)) (diff#(X1, mark(X2)) -> diff#(X1, X2), diff#(X1, mark(X2)) -> diff#(X1, X2)) (diff#(X1, mark(X2)) -> diff#(X1, X2), diff#(mark(X1), X2) -> diff#(X1, X2)) (diff#(X1, mark(X2)) -> diff#(X1, X2), diff#(ok(X1), ok(X2)) -> diff#(X1, X2)) (leq#(mark(X1), X2) -> leq#(X1, X2), leq#(X1, mark(X2)) -> leq#(X1, X2)) (leq#(mark(X1), X2) -> leq#(X1, X2), leq#(mark(X1), X2) -> leq#(X1, X2)) (leq#(mark(X1), X2) -> leq#(X1, X2), leq#(ok(X1), ok(X2)) -> leq#(X1, X2)) (proper#(diff(X1, X2)) -> proper#(X1), proper#(p(X)) -> p#(proper(X))) (proper#(diff(X1, X2)) -> proper#(X1), proper#(p(X)) -> proper#(X)) (proper#(diff(X1, X2)) -> proper#(X1), proper#(s(X)) -> s#(proper(X))) (proper#(diff(X1, X2)) -> proper#(X1), proper#(s(X)) -> proper#(X)) (proper#(diff(X1, X2)) -> proper#(X1), proper#(leq(X1, X2)) -> leq#(proper(X1), proper(X2))) (proper#(diff(X1, X2)) -> proper#(X1), proper#(leq(X1, X2)) -> proper#(X1)) (proper#(diff(X1, X2)) -> proper#(X1), proper#(leq(X1, X2)) -> proper#(X2)) (proper#(diff(X1, X2)) -> proper#(X1), proper#(if(X1, X2, X3)) -> if#(proper(X1), proper(X2), proper(X3))) (proper#(diff(X1, X2)) -> proper#(X1), proper#(if(X1, X2, X3)) -> proper#(X1)) (proper#(diff(X1, X2)) -> proper#(X1), proper#(if(X1, X2, X3)) -> proper#(X2)) (proper#(diff(X1, X2)) -> proper#(X1), proper#(if(X1, X2, X3)) -> proper#(X3)) (proper#(diff(X1, X2)) -> proper#(X1), proper#(diff(X1, X2)) -> diff#(proper(X1), proper(X2))) (proper#(diff(X1, X2)) -> proper#(X1), proper#(diff(X1, X2)) -> proper#(X1)) (proper#(diff(X1, X2)) -> proper#(X1), proper#(diff(X1, X2)) -> proper#(X2)) (proper#(leq(X1, X2)) -> proper#(X1), proper#(p(X)) -> p#(proper(X))) (proper#(leq(X1, X2)) -> proper#(X1), proper#(p(X)) -> proper#(X)) (proper#(leq(X1, X2)) -> proper#(X1), proper#(s(X)) -> s#(proper(X))) (proper#(leq(X1, X2)) -> proper#(X1), proper#(s(X)) -> proper#(X)) (proper#(leq(X1, X2)) -> proper#(X1), proper#(leq(X1, X2)) -> leq#(proper(X1), proper(X2))) (proper#(leq(X1, X2)) -> proper#(X1), proper#(leq(X1, X2)) -> proper#(X1)) (proper#(leq(X1, X2)) -> proper#(X1), proper#(leq(X1, X2)) -> proper#(X2)) (proper#(leq(X1, X2)) -> proper#(X1), proper#(if(X1, X2, X3)) -> if#(proper(X1), proper(X2), proper(X3))) (proper#(leq(X1, X2)) -> proper#(X1), proper#(if(X1, X2, X3)) -> proper#(X1)) (proper#(leq(X1, X2)) -> proper#(X1), proper#(if(X1, X2, X3)) -> proper#(X2)) (proper#(leq(X1, X2)) -> proper#(X1), proper#(if(X1, X2, X3)) -> proper#(X3)) (proper#(leq(X1, X2)) -> proper#(X1), proper#(diff(X1, X2)) -> diff#(proper(X1), proper(X2))) (proper#(leq(X1, X2)) -> proper#(X1), proper#(diff(X1, X2)) -> proper#(X1)) (proper#(leq(X1, X2)) -> proper#(X1), proper#(diff(X1, X2)) -> proper#(X2)) (active#(if(X1, X2, X3)) -> active#(X1), active#(p(X)) -> active#(X)) (active#(if(X1, X2, X3)) -> active#(X1), active#(p(X)) -> p#(active(X))) (active#(if(X1, X2, X3)) -> active#(X1), active#(s(X)) -> active#(X)) (active#(if(X1, X2, X3)) -> active#(X1), active#(s(X)) -> s#(active(X))) (active#(if(X1, X2, X3)) -> active#(X1), active#(leq(X1, X2)) -> active#(X1)) (active#(if(X1, X2, X3)) -> active#(X1), active#(leq(X1, X2)) -> active#(X2)) (active#(if(X1, X2, X3)) -> active#(X1), active#(leq(X1, X2)) -> leq#(X1, active(X2))) (active#(if(X1, X2, X3)) -> active#(X1), active#(leq(X1, X2)) -> leq#(active(X1), X2)) (active#(if(X1, X2, X3)) -> active#(X1), active#(leq(s(X), s(Y))) -> leq#(X, Y)) (active#(if(X1, X2, X3)) -> active#(X1), active#(if(X1, X2, X3)) -> active#(X1)) (active#(if(X1, X2, X3)) -> active#(X1), active#(if(X1, X2, X3)) -> if#(active(X1), X2, X3)) (active#(if(X1, X2, X3)) -> active#(X1), active#(diff(X, Y)) -> p#(X)) (active#(if(X1, X2, X3)) -> active#(X1), active#(diff(X, Y)) -> s#(diff(p(X), Y))) (active#(if(X1, X2, X3)) -> active#(X1), active#(diff(X, Y)) -> leq#(X, Y)) (active#(if(X1, X2, X3)) -> active#(X1), active#(diff(X, Y)) -> if#(leq(X, Y), 0(), s(diff(p(X), Y)))) (active#(if(X1, X2, X3)) -> active#(X1), active#(diff(X, Y)) -> diff#(p(X), Y)) (active#(if(X1, X2, X3)) -> active#(X1), active#(diff(X1, X2)) -> active#(X1)) (active#(if(X1, X2, X3)) -> active#(X1), active#(diff(X1, X2)) -> active#(X2)) (active#(if(X1, X2, X3)) -> active#(X1), active#(diff(X1, X2)) -> diff#(X1, active(X2))) (active#(if(X1, X2, X3)) -> active#(X1), active#(diff(X1, X2)) -> diff#(active(X1), X2)) (active#(diff(X1, X2)) -> diff#(active(X1), X2), diff#(X1, mark(X2)) -> diff#(X1, X2)) (active#(diff(X1, X2)) -> diff#(active(X1), X2), diff#(mark(X1), X2) -> diff#(X1, X2)) (active#(diff(X1, X2)) -> diff#(active(X1), X2), diff#(ok(X1), ok(X2)) -> diff#(X1, X2)) (top#(ok(X)) -> active#(X), active#(p(X)) -> active#(X)) (top#(ok(X)) -> active#(X), active#(p(X)) -> p#(active(X))) (top#(ok(X)) -> active#(X), active#(s(X)) -> active#(X)) (top#(ok(X)) -> active#(X), active#(s(X)) -> s#(active(X))) (top#(ok(X)) -> active#(X), active#(leq(X1, X2)) -> active#(X1)) (top#(ok(X)) -> active#(X), active#(leq(X1, X2)) -> active#(X2)) (top#(ok(X)) -> active#(X), active#(leq(X1, X2)) -> leq#(X1, active(X2))) (top#(ok(X)) -> active#(X), active#(leq(X1, X2)) -> leq#(active(X1), X2)) (top#(ok(X)) -> active#(X), active#(leq(s(X), s(Y))) -> leq#(X, Y)) (top#(ok(X)) -> active#(X), active#(if(X1, X2, X3)) -> active#(X1)) (top#(ok(X)) -> active#(X), active#(if(X1, X2, X3)) -> if#(active(X1), X2, X3)) (top#(ok(X)) -> active#(X), active#(diff(X, Y)) -> p#(X)) (top#(ok(X)) -> active#(X), active#(diff(X, Y)) -> s#(diff(p(X), Y))) (top#(ok(X)) -> active#(X), active#(diff(X, Y)) -> leq#(X, Y)) (top#(ok(X)) -> active#(X), active#(diff(X, Y)) -> if#(leq(X, Y), 0(), s(diff(p(X), Y)))) (top#(ok(X)) -> active#(X), active#(diff(X, Y)) -> diff#(p(X), Y)) (top#(ok(X)) -> active#(X), active#(diff(X1, X2)) -> active#(X1)) (top#(ok(X)) -> active#(X), active#(diff(X1, X2)) -> active#(X2)) (top#(ok(X)) -> active#(X), active#(diff(X1, X2)) -> diff#(X1, active(X2))) (top#(ok(X)) -> active#(X), active#(diff(X1, X2)) -> diff#(active(X1), X2)) (proper#(s(X)) -> proper#(X), proper#(p(X)) -> p#(proper(X))) (proper#(s(X)) -> proper#(X), proper#(p(X)) -> proper#(X)) (proper#(s(X)) -> proper#(X), proper#(s(X)) -> s#(proper(X))) (proper#(s(X)) -> proper#(X), proper#(s(X)) -> proper#(X)) (proper#(s(X)) -> proper#(X), proper#(leq(X1, X2)) -> leq#(proper(X1), proper(X2))) (proper#(s(X)) -> proper#(X), proper#(leq(X1, X2)) -> proper#(X1)) (proper#(s(X)) -> proper#(X), proper#(leq(X1, X2)) -> proper#(X2)) (proper#(s(X)) -> proper#(X), proper#(if(X1, X2, X3)) -> if#(proper(X1), proper(X2), proper(X3))) (proper#(s(X)) -> proper#(X), proper#(if(X1, X2, X3)) -> proper#(X1)) (proper#(s(X)) -> proper#(X), proper#(if(X1, X2, X3)) -> proper#(X2)) (proper#(s(X)) -> proper#(X), proper#(if(X1, X2, X3)) -> proper#(X3)) (proper#(s(X)) -> proper#(X), proper#(diff(X1, X2)) -> diff#(proper(X1), proper(X2))) (proper#(s(X)) -> proper#(X), proper#(diff(X1, X2)) -> proper#(X1)) (proper#(s(X)) -> proper#(X), proper#(diff(X1, X2)) -> proper#(X2)) (s#(ok(X)) -> s#(X), s#(mark(X)) -> s#(X)) (s#(ok(X)) -> s#(X), s#(ok(X)) -> s#(X)) (p#(ok(X)) -> p#(X), p#(mark(X)) -> p#(X)) (p#(ok(X)) -> p#(X), p#(ok(X)) -> p#(X)) (active#(diff(X, Y)) -> p#(X), p#(mark(X)) -> p#(X)) (active#(diff(X, Y)) -> p#(X), p#(ok(X)) -> p#(X)) (active#(p(X)) -> active#(X), active#(p(X)) -> active#(X)) (active#(p(X)) -> active#(X), active#(p(X)) -> p#(active(X))) (active#(p(X)) -> active#(X), active#(s(X)) -> active#(X)) (active#(p(X)) -> active#(X), active#(s(X)) -> s#(active(X))) (active#(p(X)) -> active#(X), active#(leq(X1, X2)) -> active#(X1)) (active#(p(X)) -> active#(X), active#(leq(X1, X2)) -> active#(X2)) (active#(p(X)) -> active#(X), active#(leq(X1, X2)) -> leq#(X1, active(X2))) (active#(p(X)) -> active#(X), active#(leq(X1, X2)) -> leq#(active(X1), X2)) (active#(p(X)) -> active#(X), active#(leq(s(X), s(Y))) -> leq#(X, Y)) (active#(p(X)) -> active#(X), active#(if(X1, X2, X3)) -> active#(X1)) (active#(p(X)) -> active#(X), active#(if(X1, X2, X3)) -> if#(active(X1), X2, X3)) (active#(p(X)) -> active#(X), active#(diff(X, Y)) -> p#(X)) (active#(p(X)) -> active#(X), active#(diff(X, Y)) -> s#(diff(p(X), Y))) (active#(p(X)) -> active#(X), active#(diff(X, Y)) -> leq#(X, Y)) (active#(p(X)) -> active#(X), active#(diff(X, Y)) -> if#(leq(X, Y), 0(), s(diff(p(X), Y)))) (active#(p(X)) -> active#(X), active#(diff(X, Y)) -> diff#(p(X), Y)) (active#(p(X)) -> active#(X), active#(diff(X1, X2)) -> active#(X1)) (active#(p(X)) -> active#(X), active#(diff(X1, X2)) -> active#(X2)) (active#(p(X)) -> active#(X), active#(diff(X1, X2)) -> diff#(X1, active(X2))) (active#(p(X)) -> active#(X), active#(diff(X1, X2)) -> diff#(active(X1), X2)) } SCCS: Scc: {top#(mark(X)) -> top#(proper(X)), top#(ok(X)) -> top#(active(X))} Scc: { proper#(p(X)) -> proper#(X), proper#(s(X)) -> proper#(X), proper#(leq(X1, X2)) -> proper#(X1), proper#(leq(X1, X2)) -> proper#(X2), proper#(if(X1, X2, X3)) -> proper#(X1), proper#(if(X1, X2, X3)) -> proper#(X2), proper#(if(X1, X2, X3)) -> proper#(X3), proper#(diff(X1, X2)) -> proper#(X1), proper#(diff(X1, X2)) -> proper#(X2)} Scc: { diff#(X1, mark(X2)) -> diff#(X1, X2), diff#(mark(X1), X2) -> diff#(X1, X2), diff#(ok(X1), ok(X2)) -> diff#(X1, X2)} Scc: { if#(mark(X1), X2, X3) -> if#(X1, X2, X3), if#(ok(X1), ok(X2), ok(X3)) -> if#(X1, X2, X3)} Scc: { leq#(X1, mark(X2)) -> leq#(X1, X2), leq#(mark(X1), X2) -> leq#(X1, X2), leq#(ok(X1), ok(X2)) -> leq#(X1, X2)} Scc: {s#(mark(X)) -> s#(X), s#(ok(X)) -> s#(X)} Scc: {p#(mark(X)) -> p#(X), p#(ok(X)) -> p#(X)} Scc: { active#(p(X)) -> active#(X), active#(s(X)) -> active#(X), active#(leq(X1, X2)) -> active#(X1), active#(leq(X1, X2)) -> active#(X2), active#(if(X1, X2, X3)) -> active#(X1), active#(diff(X1, X2)) -> active#(X1), active#(diff(X1, X2)) -> active#(X2)} SCC: Strict: {top#(mark(X)) -> top#(proper(X)), top#(ok(X)) -> top#(active(X))} Weak: { active(p(X)) -> p(active(X)), active(p(0())) -> mark(0()), active(p(s(X))) -> mark(X), active(s(X)) -> s(active(X)), active(leq(X1, X2)) -> leq(X1, active(X2)), active(leq(X1, X2)) -> leq(active(X1), X2), active(leq(0(), Y)) -> mark(true()), active(leq(s(X), 0())) -> mark(false()), active(leq(s(X), s(Y))) -> mark(leq(X, Y)), active(if(X1, X2, X3)) -> if(active(X1), X2, X3), active(if(true(), X, Y)) -> mark(X), active(if(false(), X, Y)) -> mark(Y), active(diff(X, Y)) -> mark(if(leq(X, Y), 0(), s(diff(p(X), Y)))), active(diff(X1, X2)) -> diff(X1, active(X2)), active(diff(X1, X2)) -> diff(active(X1), X2), p(mark(X)) -> mark(p(X)), p(ok(X)) -> ok(p(X)), s(mark(X)) -> mark(s(X)), s(ok(X)) -> ok(s(X)), leq(X1, mark(X2)) -> mark(leq(X1, X2)), leq(mark(X1), X2) -> mark(leq(X1, X2)), leq(ok(X1), ok(X2)) -> ok(leq(X1, X2)), if(mark(X1), X2, X3) -> mark(if(X1, X2, X3)), if(ok(X1), ok(X2), ok(X3)) -> ok(if(X1, X2, X3)), diff(X1, mark(X2)) -> mark(diff(X1, X2)), diff(mark(X1), X2) -> mark(diff(X1, X2)), diff(ok(X1), ok(X2)) -> ok(diff(X1, X2)), proper(0()) -> ok(0()), proper(p(X)) -> p(proper(X)), proper(s(X)) -> s(proper(X)), proper(true()) -> ok(true()), proper(leq(X1, X2)) -> leq(proper(X1), proper(X2)), proper(false()) -> ok(false()), proper(if(X1, X2, X3)) -> if(proper(X1), proper(X2), proper(X3)), proper(diff(X1, X2)) -> diff(proper(X1), proper(X2)), top(mark(X)) -> top(proper(X)), top(ok(X)) -> top(active(X))} Fail SCC: Strict: { proper#(p(X)) -> proper#(X), proper#(s(X)) -> proper#(X), proper#(leq(X1, X2)) -> proper#(X1), proper#(leq(X1, X2)) -> proper#(X2), proper#(if(X1, X2, X3)) -> proper#(X1), proper#(if(X1, X2, X3)) -> proper#(X2), proper#(if(X1, X2, X3)) -> proper#(X3), proper#(diff(X1, X2)) -> proper#(X1), proper#(diff(X1, X2)) -> proper#(X2)} Weak: { active(p(X)) -> p(active(X)), active(p(0())) -> mark(0()), active(p(s(X))) -> mark(X), active(s(X)) -> s(active(X)), active(leq(X1, X2)) -> leq(X1, active(X2)), active(leq(X1, X2)) -> leq(active(X1), X2), active(leq(0(), Y)) -> mark(true()), active(leq(s(X), 0())) -> mark(false()), active(leq(s(X), s(Y))) -> mark(leq(X, Y)), active(if(X1, X2, X3)) -> if(active(X1), X2, X3), active(if(true(), X, Y)) -> mark(X), active(if(false(), X, Y)) -> mark(Y), active(diff(X, Y)) -> mark(if(leq(X, Y), 0(), s(diff(p(X), Y)))), active(diff(X1, X2)) -> diff(X1, active(X2)), active(diff(X1, X2)) -> diff(active(X1), X2), p(mark(X)) -> mark(p(X)), p(ok(X)) -> ok(p(X)), s(mark(X)) -> mark(s(X)), s(ok(X)) -> ok(s(X)), leq(X1, mark(X2)) -> mark(leq(X1, X2)), leq(mark(X1), X2) -> mark(leq(X1, X2)), leq(ok(X1), ok(X2)) -> ok(leq(X1, X2)), if(mark(X1), X2, X3) -> mark(if(X1, X2, X3)), if(ok(X1), ok(X2), ok(X3)) -> ok(if(X1, X2, X3)), diff(X1, mark(X2)) -> mark(diff(X1, X2)), diff(mark(X1), X2) -> mark(diff(X1, X2)), diff(ok(X1), ok(X2)) -> ok(diff(X1, X2)), proper(0()) -> ok(0()), proper(p(X)) -> p(proper(X)), proper(s(X)) -> s(proper(X)), proper(true()) -> ok(true()), proper(leq(X1, X2)) -> leq(proper(X1), proper(X2)), proper(false()) -> ok(false()), proper(if(X1, X2, X3)) -> if(proper(X1), proper(X2), proper(X3)), proper(diff(X1, X2)) -> diff(proper(X1), proper(X2)), top(mark(X)) -> top(proper(X)), top(ok(X)) -> top(active(X))} SPSC: Simple Projection: pi(proper#) = 0 Strict: { proper#(p(X)) -> proper#(X), proper#(s(X)) -> proper#(X), proper#(leq(X1, X2)) -> proper#(X1), proper#(leq(X1, X2)) -> proper#(X2), proper#(if(X1, X2, X3)) -> proper#(X2), proper#(if(X1, X2, X3)) -> proper#(X3), proper#(diff(X1, X2)) -> proper#(X1), proper#(diff(X1, X2)) -> proper#(X2)} EDG: {(proper#(leq(X1, X2)) -> proper#(X2), proper#(diff(X1, X2)) -> proper#(X2)) (proper#(leq(X1, X2)) -> proper#(X2), proper#(diff(X1, X2)) -> proper#(X1)) (proper#(leq(X1, X2)) -> proper#(X2), proper#(if(X1, X2, X3)) -> proper#(X3)) (proper#(leq(X1, X2)) -> proper#(X2), proper#(if(X1, X2, X3)) -> proper#(X2)) (proper#(leq(X1, X2)) -> proper#(X2), proper#(leq(X1, X2)) -> proper#(X2)) (proper#(leq(X1, X2)) -> proper#(X2), proper#(leq(X1, X2)) -> proper#(X1)) (proper#(leq(X1, X2)) -> proper#(X2), proper#(s(X)) -> proper#(X)) (proper#(leq(X1, X2)) -> proper#(X2), proper#(p(X)) -> proper#(X)) (proper#(diff(X1, X2)) -> proper#(X2), proper#(diff(X1, X2)) -> proper#(X2)) (proper#(diff(X1, X2)) -> proper#(X2), proper#(diff(X1, X2)) -> proper#(X1)) (proper#(diff(X1, X2)) -> proper#(X2), proper#(if(X1, X2, X3)) -> proper#(X3)) (proper#(diff(X1, X2)) -> proper#(X2), proper#(if(X1, X2, X3)) -> proper#(X2)) (proper#(diff(X1, X2)) -> proper#(X2), proper#(leq(X1, X2)) -> proper#(X2)) (proper#(diff(X1, X2)) -> proper#(X2), proper#(leq(X1, X2)) -> proper#(X1)) (proper#(diff(X1, X2)) -> proper#(X2), proper#(s(X)) -> proper#(X)) (proper#(diff(X1, X2)) -> proper#(X2), proper#(p(X)) -> proper#(X)) (proper#(s(X)) -> proper#(X), proper#(diff(X1, X2)) -> proper#(X2)) (proper#(s(X)) -> proper#(X), proper#(diff(X1, X2)) -> proper#(X1)) (proper#(s(X)) -> proper#(X), proper#(if(X1, X2, X3)) -> proper#(X3)) (proper#(s(X)) -> proper#(X), proper#(if(X1, X2, X3)) -> proper#(X2)) (proper#(s(X)) -> proper#(X), proper#(leq(X1, X2)) -> proper#(X2)) (proper#(s(X)) -> proper#(X), proper#(leq(X1, X2)) -> proper#(X1)) (proper#(s(X)) -> proper#(X), proper#(s(X)) -> proper#(X)) (proper#(s(X)) -> proper#(X), proper#(p(X)) -> proper#(X)) (proper#(diff(X1, X2)) -> proper#(X1), proper#(diff(X1, X2)) -> proper#(X2)) (proper#(diff(X1, X2)) -> proper#(X1), proper#(diff(X1, X2)) -> proper#(X1)) (proper#(diff(X1, X2)) -> proper#(X1), proper#(if(X1, X2, X3)) -> proper#(X3)) (proper#(diff(X1, X2)) -> proper#(X1), proper#(if(X1, X2, X3)) -> proper#(X2)) (proper#(diff(X1, X2)) -> proper#(X1), proper#(leq(X1, X2)) -> proper#(X2)) (proper#(diff(X1, X2)) -> proper#(X1), proper#(leq(X1, X2)) -> proper#(X1)) (proper#(diff(X1, X2)) -> proper#(X1), proper#(s(X)) -> proper#(X)) (proper#(diff(X1, X2)) -> proper#(X1), proper#(p(X)) -> proper#(X)) (proper#(leq(X1, X2)) -> proper#(X1), proper#(p(X)) -> proper#(X)) (proper#(leq(X1, X2)) -> proper#(X1), proper#(s(X)) -> proper#(X)) (proper#(leq(X1, X2)) -> proper#(X1), proper#(leq(X1, X2)) -> proper#(X1)) (proper#(leq(X1, X2)) -> proper#(X1), proper#(leq(X1, X2)) -> proper#(X2)) (proper#(leq(X1, X2)) -> proper#(X1), proper#(if(X1, X2, X3)) -> proper#(X2)) (proper#(leq(X1, X2)) -> proper#(X1), proper#(if(X1, X2, X3)) -> proper#(X3)) (proper#(leq(X1, X2)) -> proper#(X1), proper#(diff(X1, X2)) -> proper#(X1)) (proper#(leq(X1, X2)) -> proper#(X1), proper#(diff(X1, X2)) -> proper#(X2)) (proper#(p(X)) -> proper#(X), proper#(p(X)) -> proper#(X)) (proper#(p(X)) -> proper#(X), proper#(s(X)) -> proper#(X)) (proper#(p(X)) -> proper#(X), proper#(leq(X1, X2)) -> proper#(X1)) (proper#(p(X)) -> proper#(X), proper#(leq(X1, X2)) -> proper#(X2)) (proper#(p(X)) -> proper#(X), proper#(if(X1, X2, X3)) -> proper#(X2)) (proper#(p(X)) -> proper#(X), proper#(if(X1, X2, X3)) -> proper#(X3)) (proper#(p(X)) -> proper#(X), proper#(diff(X1, X2)) -> proper#(X1)) (proper#(p(X)) -> proper#(X), proper#(diff(X1, X2)) -> proper#(X2)) (proper#(if(X1, X2, X3)) -> proper#(X2), proper#(p(X)) -> proper#(X)) (proper#(if(X1, X2, X3)) -> proper#(X2), proper#(s(X)) -> proper#(X)) (proper#(if(X1, X2, X3)) -> proper#(X2), proper#(leq(X1, X2)) -> proper#(X1)) (proper#(if(X1, X2, X3)) -> proper#(X2), proper#(leq(X1, X2)) -> proper#(X2)) (proper#(if(X1, X2, X3)) -> proper#(X2), proper#(if(X1, X2, X3)) -> proper#(X2)) (proper#(if(X1, X2, X3)) -> proper#(X2), proper#(if(X1, X2, X3)) -> proper#(X3)) (proper#(if(X1, X2, X3)) -> proper#(X2), proper#(diff(X1, X2)) -> proper#(X1)) (proper#(if(X1, X2, X3)) -> proper#(X2), proper#(diff(X1, X2)) -> proper#(X2)) (proper#(if(X1, X2, X3)) -> proper#(X3), proper#(p(X)) -> proper#(X)) (proper#(if(X1, X2, X3)) -> proper#(X3), proper#(s(X)) -> proper#(X)) (proper#(if(X1, X2, X3)) -> proper#(X3), proper#(leq(X1, X2)) -> proper#(X1)) (proper#(if(X1, X2, X3)) -> proper#(X3), proper#(leq(X1, X2)) -> proper#(X2)) (proper#(if(X1, X2, X3)) -> proper#(X3), proper#(if(X1, X2, X3)) -> proper#(X2)) (proper#(if(X1, X2, X3)) -> proper#(X3), proper#(if(X1, X2, X3)) -> proper#(X3)) (proper#(if(X1, X2, X3)) -> proper#(X3), proper#(diff(X1, X2)) -> proper#(X1)) (proper#(if(X1, X2, X3)) -> proper#(X3), proper#(diff(X1, X2)) -> proper#(X2))} SCCS: Scc: { proper#(p(X)) -> proper#(X), proper#(s(X)) -> proper#(X), proper#(leq(X1, X2)) -> proper#(X1), proper#(leq(X1, X2)) -> proper#(X2), proper#(if(X1, X2, X3)) -> proper#(X2), proper#(if(X1, X2, X3)) -> proper#(X3), proper#(diff(X1, X2)) -> proper#(X1), proper#(diff(X1, X2)) -> proper#(X2)} SCC: Strict: { proper#(p(X)) -> proper#(X), proper#(s(X)) -> proper#(X), proper#(leq(X1, X2)) -> proper#(X1), proper#(leq(X1, X2)) -> proper#(X2), proper#(if(X1, X2, X3)) -> proper#(X2), proper#(if(X1, X2, X3)) -> proper#(X3), proper#(diff(X1, X2)) -> proper#(X1), proper#(diff(X1, X2)) -> proper#(X2)} Weak: { active(p(X)) -> p(active(X)), active(p(0())) -> mark(0()), active(p(s(X))) -> mark(X), active(s(X)) -> s(active(X)), active(leq(X1, X2)) -> leq(X1, active(X2)), active(leq(X1, X2)) -> leq(active(X1), X2), active(leq(0(), Y)) -> mark(true()), active(leq(s(X), 0())) -> mark(false()), active(leq(s(X), s(Y))) -> mark(leq(X, Y)), active(if(X1, X2, X3)) -> if(active(X1), X2, X3), active(if(true(), X, Y)) -> mark(X), active(if(false(), X, Y)) -> mark(Y), active(diff(X, Y)) -> mark(if(leq(X, Y), 0(), s(diff(p(X), Y)))), active(diff(X1, X2)) -> diff(X1, active(X2)), active(diff(X1, X2)) -> diff(active(X1), X2), p(mark(X)) -> mark(p(X)), p(ok(X)) -> ok(p(X)), s(mark(X)) -> mark(s(X)), s(ok(X)) -> ok(s(X)), leq(X1, mark(X2)) -> mark(leq(X1, X2)), leq(mark(X1), X2) -> mark(leq(X1, X2)), leq(ok(X1), ok(X2)) -> ok(leq(X1, X2)), if(mark(X1), X2, X3) -> mark(if(X1, X2, X3)), if(ok(X1), ok(X2), ok(X3)) -> ok(if(X1, X2, X3)), diff(X1, mark(X2)) -> mark(diff(X1, X2)), diff(mark(X1), X2) -> mark(diff(X1, X2)), diff(ok(X1), ok(X2)) -> ok(diff(X1, X2)), proper(0()) -> ok(0()), proper(p(X)) -> p(proper(X)), proper(s(X)) -> s(proper(X)), proper(true()) -> ok(true()), proper(leq(X1, X2)) -> leq(proper(X1), proper(X2)), proper(false()) -> ok(false()), proper(if(X1, X2, X3)) -> if(proper(X1), proper(X2), proper(X3)), proper(diff(X1, X2)) -> diff(proper(X1), proper(X2)), top(mark(X)) -> top(proper(X)), top(ok(X)) -> top(active(X))} SPSC: Simple Projection: pi(proper#) = 0 Strict: { proper#(p(X)) -> proper#(X), proper#(s(X)) -> proper#(X), proper#(leq(X1, X2)) -> proper#(X1), proper#(leq(X1, X2)) -> proper#(X2), proper#(if(X1, X2, X3)) -> proper#(X2), proper#(if(X1, X2, X3)) -> proper#(X3), proper#(diff(X1, X2)) -> proper#(X2)} EDG: {(proper#(leq(X1, X2)) -> proper#(X2), proper#(diff(X1, X2)) -> proper#(X2)) (proper#(leq(X1, X2)) -> proper#(X2), proper#(if(X1, X2, X3)) -> proper#(X3)) (proper#(leq(X1, X2)) -> proper#(X2), proper#(if(X1, X2, X3)) -> proper#(X2)) (proper#(leq(X1, X2)) -> proper#(X2), proper#(leq(X1, X2)) -> proper#(X2)) (proper#(leq(X1, X2)) -> proper#(X2), proper#(leq(X1, X2)) -> proper#(X1)) (proper#(leq(X1, X2)) -> proper#(X2), proper#(s(X)) -> proper#(X)) (proper#(leq(X1, X2)) -> proper#(X2), proper#(p(X)) -> proper#(X)) (proper#(diff(X1, X2)) -> proper#(X2), proper#(diff(X1, X2)) -> proper#(X2)) (proper#(diff(X1, X2)) -> proper#(X2), proper#(if(X1, X2, X3)) -> proper#(X3)) (proper#(diff(X1, X2)) -> proper#(X2), proper#(if(X1, X2, X3)) -> proper#(X2)) (proper#(diff(X1, X2)) -> proper#(X2), proper#(leq(X1, X2)) -> proper#(X2)) (proper#(diff(X1, X2)) -> proper#(X2), proper#(leq(X1, X2)) -> proper#(X1)) (proper#(diff(X1, X2)) -> proper#(X2), proper#(s(X)) -> proper#(X)) (proper#(diff(X1, X2)) -> proper#(X2), proper#(p(X)) -> proper#(X)) (proper#(p(X)) -> proper#(X), proper#(diff(X1, X2)) -> proper#(X2)) (proper#(p(X)) -> proper#(X), proper#(if(X1, X2, X3)) -> proper#(X3)) (proper#(p(X)) -> proper#(X), proper#(if(X1, X2, X3)) -> proper#(X2)) (proper#(p(X)) -> proper#(X), proper#(leq(X1, X2)) -> proper#(X2)) (proper#(p(X)) -> proper#(X), proper#(leq(X1, X2)) -> proper#(X1)) (proper#(p(X)) -> proper#(X), proper#(s(X)) -> proper#(X)) (proper#(p(X)) -> proper#(X), proper#(p(X)) -> proper#(X)) (proper#(s(X)) -> proper#(X), proper#(p(X)) -> proper#(X)) (proper#(s(X)) -> proper#(X), proper#(s(X)) -> proper#(X)) (proper#(s(X)) -> proper#(X), proper#(leq(X1, X2)) -> proper#(X1)) (proper#(s(X)) -> proper#(X), proper#(leq(X1, X2)) -> proper#(X2)) (proper#(s(X)) -> proper#(X), proper#(if(X1, X2, X3)) -> proper#(X2)) (proper#(s(X)) -> proper#(X), proper#(if(X1, X2, X3)) -> proper#(X3)) (proper#(s(X)) -> proper#(X), proper#(diff(X1, X2)) -> proper#(X2)) (proper#(leq(X1, X2)) -> proper#(X1), proper#(p(X)) -> proper#(X)) (proper#(leq(X1, X2)) -> proper#(X1), proper#(s(X)) -> proper#(X)) (proper#(leq(X1, X2)) -> proper#(X1), proper#(leq(X1, X2)) -> proper#(X1)) (proper#(leq(X1, X2)) -> proper#(X1), proper#(leq(X1, X2)) -> proper#(X2)) (proper#(leq(X1, X2)) -> proper#(X1), proper#(if(X1, X2, X3)) -> proper#(X2)) (proper#(leq(X1, X2)) -> proper#(X1), proper#(if(X1, X2, X3)) -> proper#(X3)) (proper#(leq(X1, X2)) -> proper#(X1), proper#(diff(X1, X2)) -> proper#(X2)) (proper#(if(X1, X2, X3)) -> proper#(X2), proper#(p(X)) -> proper#(X)) (proper#(if(X1, X2, X3)) -> proper#(X2), proper#(s(X)) -> proper#(X)) (proper#(if(X1, X2, X3)) -> proper#(X2), proper#(leq(X1, X2)) -> proper#(X1)) (proper#(if(X1, X2, X3)) -> proper#(X2), proper#(leq(X1, X2)) -> proper#(X2)) (proper#(if(X1, X2, X3)) -> proper#(X2), proper#(if(X1, X2, X3)) -> proper#(X2)) (proper#(if(X1, X2, X3)) -> proper#(X2), proper#(if(X1, X2, X3)) -> proper#(X3)) (proper#(if(X1, X2, X3)) -> proper#(X2), proper#(diff(X1, X2)) -> proper#(X2)) (proper#(if(X1, X2, X3)) -> proper#(X3), proper#(p(X)) -> proper#(X)) (proper#(if(X1, X2, X3)) -> proper#(X3), proper#(s(X)) -> proper#(X)) (proper#(if(X1, X2, X3)) -> proper#(X3), proper#(leq(X1, X2)) -> proper#(X1)) (proper#(if(X1, X2, X3)) -> proper#(X3), proper#(leq(X1, X2)) -> proper#(X2)) (proper#(if(X1, X2, X3)) -> proper#(X3), proper#(if(X1, X2, X3)) -> proper#(X2)) (proper#(if(X1, X2, X3)) -> proper#(X3), proper#(if(X1, X2, X3)) -> proper#(X3)) (proper#(if(X1, X2, X3)) -> proper#(X3), proper#(diff(X1, X2)) -> proper#(X2))} SCCS: Scc: { proper#(p(X)) -> proper#(X), proper#(s(X)) -> proper#(X), proper#(leq(X1, X2)) -> proper#(X1), proper#(leq(X1, X2)) -> proper#(X2), proper#(if(X1, X2, X3)) -> proper#(X2), proper#(if(X1, X2, X3)) -> proper#(X3), proper#(diff(X1, X2)) -> proper#(X2)} SCC: Strict: { proper#(p(X)) -> proper#(X), proper#(s(X)) -> proper#(X), proper#(leq(X1, X2)) -> proper#(X1), proper#(leq(X1, X2)) -> proper#(X2), proper#(if(X1, X2, X3)) -> proper#(X2), proper#(if(X1, X2, X3)) -> proper#(X3), proper#(diff(X1, X2)) -> proper#(X2)} Weak: { active(p(X)) -> p(active(X)), active(p(0())) -> mark(0()), active(p(s(X))) -> mark(X), active(s(X)) -> s(active(X)), active(leq(X1, X2)) -> leq(X1, active(X2)), active(leq(X1, X2)) -> leq(active(X1), X2), active(leq(0(), Y)) -> mark(true()), active(leq(s(X), 0())) -> mark(false()), active(leq(s(X), s(Y))) -> mark(leq(X, Y)), active(if(X1, X2, X3)) -> if(active(X1), X2, X3), active(if(true(), X, Y)) -> mark(X), active(if(false(), X, Y)) -> mark(Y), active(diff(X, Y)) -> mark(if(leq(X, Y), 0(), s(diff(p(X), Y)))), active(diff(X1, X2)) -> diff(X1, active(X2)), active(diff(X1, X2)) -> diff(active(X1), X2), p(mark(X)) -> mark(p(X)), p(ok(X)) -> ok(p(X)), s(mark(X)) -> mark(s(X)), s(ok(X)) -> ok(s(X)), leq(X1, mark(X2)) -> mark(leq(X1, X2)), leq(mark(X1), X2) -> mark(leq(X1, X2)), leq(ok(X1), ok(X2)) -> ok(leq(X1, X2)), if(mark(X1), X2, X3) -> mark(if(X1, X2, X3)), if(ok(X1), ok(X2), ok(X3)) -> ok(if(X1, X2, X3)), diff(X1, mark(X2)) -> mark(diff(X1, X2)), diff(mark(X1), X2) -> mark(diff(X1, X2)), diff(ok(X1), ok(X2)) -> ok(diff(X1, X2)), proper(0()) -> ok(0()), proper(p(X)) -> p(proper(X)), proper(s(X)) -> s(proper(X)), proper(true()) -> ok(true()), proper(leq(X1, X2)) -> leq(proper(X1), proper(X2)), proper(false()) -> ok(false()), proper(if(X1, X2, X3)) -> if(proper(X1), proper(X2), proper(X3)), proper(diff(X1, X2)) -> diff(proper(X1), proper(X2)), top(mark(X)) -> top(proper(X)), top(ok(X)) -> top(active(X))} SPSC: Simple Projection: pi(proper#) = 0 Strict: { proper#(p(X)) -> proper#(X), proper#(s(X)) -> proper#(X), proper#(leq(X1, X2)) -> proper#(X1), proper#(leq(X1, X2)) -> proper#(X2), proper#(if(X1, X2, X3)) -> proper#(X2), proper#(diff(X1, X2)) -> proper#(X2)} EDG: {(proper#(p(X)) -> proper#(X), proper#(diff(X1, X2)) -> proper#(X2)) (proper#(p(X)) -> proper#(X), proper#(if(X1, X2, X3)) -> proper#(X2)) (proper#(p(X)) -> proper#(X), proper#(leq(X1, X2)) -> proper#(X2)) (proper#(p(X)) -> proper#(X), proper#(leq(X1, X2)) -> proper#(X1)) (proper#(p(X)) -> proper#(X), proper#(s(X)) -> proper#(X)) (proper#(p(X)) -> proper#(X), proper#(p(X)) -> proper#(X)) (proper#(leq(X1, X2)) -> proper#(X2), proper#(diff(X1, X2)) -> proper#(X2)) (proper#(leq(X1, X2)) -> proper#(X2), proper#(if(X1, X2, X3)) -> proper#(X2)) (proper#(leq(X1, X2)) -> proper#(X2), proper#(leq(X1, X2)) -> proper#(X2)) (proper#(leq(X1, X2)) -> proper#(X2), proper#(leq(X1, X2)) -> proper#(X1)) (proper#(leq(X1, X2)) -> proper#(X2), proper#(s(X)) -> proper#(X)) (proper#(leq(X1, X2)) -> proper#(X2), proper#(p(X)) -> proper#(X)) (proper#(diff(X1, X2)) -> proper#(X2), proper#(diff(X1, X2)) -> proper#(X2)) (proper#(diff(X1, X2)) -> proper#(X2), proper#(if(X1, X2, X3)) -> proper#(X2)) (proper#(diff(X1, X2)) -> proper#(X2), proper#(leq(X1, X2)) -> proper#(X2)) (proper#(diff(X1, X2)) -> proper#(X2), proper#(leq(X1, X2)) -> proper#(X1)) (proper#(diff(X1, X2)) -> proper#(X2), proper#(s(X)) -> proper#(X)) (proper#(diff(X1, X2)) -> proper#(X2), proper#(p(X)) -> proper#(X)) (proper#(if(X1, X2, X3)) -> proper#(X2), proper#(p(X)) -> proper#(X)) (proper#(if(X1, X2, X3)) -> proper#(X2), proper#(s(X)) -> proper#(X)) (proper#(if(X1, X2, X3)) -> proper#(X2), proper#(leq(X1, X2)) -> proper#(X1)) (proper#(if(X1, X2, X3)) -> proper#(X2), proper#(leq(X1, X2)) -> proper#(X2)) (proper#(if(X1, X2, X3)) -> proper#(X2), proper#(if(X1, X2, X3)) -> proper#(X2)) (proper#(if(X1, X2, X3)) -> proper#(X2), proper#(diff(X1, X2)) -> proper#(X2)) (proper#(s(X)) -> proper#(X), proper#(p(X)) -> proper#(X)) (proper#(s(X)) -> proper#(X), proper#(s(X)) -> proper#(X)) (proper#(s(X)) -> proper#(X), proper#(leq(X1, X2)) -> proper#(X1)) (proper#(s(X)) -> proper#(X), proper#(leq(X1, X2)) -> proper#(X2)) (proper#(s(X)) -> proper#(X), proper#(if(X1, X2, X3)) -> proper#(X2)) (proper#(s(X)) -> proper#(X), proper#(diff(X1, X2)) -> proper#(X2)) (proper#(leq(X1, X2)) -> proper#(X1), proper#(p(X)) -> proper#(X)) (proper#(leq(X1, X2)) -> proper#(X1), proper#(s(X)) -> proper#(X)) (proper#(leq(X1, X2)) -> proper#(X1), proper#(leq(X1, X2)) -> proper#(X1)) (proper#(leq(X1, X2)) -> proper#(X1), proper#(leq(X1, X2)) -> proper#(X2)) (proper#(leq(X1, X2)) -> proper#(X1), proper#(if(X1, X2, X3)) -> proper#(X2)) (proper#(leq(X1, X2)) -> proper#(X1), proper#(diff(X1, X2)) -> proper#(X2))} SCCS: Scc: { proper#(p(X)) -> proper#(X), proper#(s(X)) -> proper#(X), proper#(leq(X1, X2)) -> proper#(X1), proper#(leq(X1, X2)) -> proper#(X2), proper#(if(X1, X2, X3)) -> proper#(X2), proper#(diff(X1, X2)) -> proper#(X2)} SCC: Strict: { proper#(p(X)) -> proper#(X), proper#(s(X)) -> proper#(X), proper#(leq(X1, X2)) -> proper#(X1), proper#(leq(X1, X2)) -> proper#(X2), proper#(if(X1, X2, X3)) -> proper#(X2), proper#(diff(X1, X2)) -> proper#(X2)} Weak: { active(p(X)) -> p(active(X)), active(p(0())) -> mark(0()), active(p(s(X))) -> mark(X), active(s(X)) -> s(active(X)), active(leq(X1, X2)) -> leq(X1, active(X2)), active(leq(X1, X2)) -> leq(active(X1), X2), active(leq(0(), Y)) -> mark(true()), active(leq(s(X), 0())) -> mark(false()), active(leq(s(X), s(Y))) -> mark(leq(X, Y)), active(if(X1, X2, X3)) -> if(active(X1), X2, X3), active(if(true(), X, Y)) -> mark(X), active(if(false(), X, Y)) -> mark(Y), active(diff(X, Y)) -> mark(if(leq(X, Y), 0(), s(diff(p(X), Y)))), active(diff(X1, X2)) -> diff(X1, active(X2)), active(diff(X1, X2)) -> diff(active(X1), X2), p(mark(X)) -> mark(p(X)), p(ok(X)) -> ok(p(X)), s(mark(X)) -> mark(s(X)), s(ok(X)) -> ok(s(X)), leq(X1, mark(X2)) -> mark(leq(X1, X2)), leq(mark(X1), X2) -> mark(leq(X1, X2)), leq(ok(X1), ok(X2)) -> ok(leq(X1, X2)), if(mark(X1), X2, X3) -> mark(if(X1, X2, X3)), if(ok(X1), ok(X2), ok(X3)) -> ok(if(X1, X2, X3)), diff(X1, mark(X2)) -> mark(diff(X1, X2)), diff(mark(X1), X2) -> mark(diff(X1, X2)), diff(ok(X1), ok(X2)) -> ok(diff(X1, X2)), proper(0()) -> ok(0()), proper(p(X)) -> p(proper(X)), proper(s(X)) -> s(proper(X)), proper(true()) -> ok(true()), proper(leq(X1, X2)) -> leq(proper(X1), proper(X2)), proper(false()) -> ok(false()), proper(if(X1, X2, X3)) -> if(proper(X1), proper(X2), proper(X3)), proper(diff(X1, X2)) -> diff(proper(X1), proper(X2)), top(mark(X)) -> top(proper(X)), top(ok(X)) -> top(active(X))} SPSC: Simple Projection: pi(proper#) = 0 Strict: { proper#(p(X)) -> proper#(X), proper#(s(X)) -> proper#(X), proper#(leq(X1, X2)) -> proper#(X1), proper#(if(X1, X2, X3)) -> proper#(X2), proper#(diff(X1, X2)) -> proper#(X2)} EDG: {(proper#(s(X)) -> proper#(X), proper#(diff(X1, X2)) -> proper#(X2)) (proper#(s(X)) -> proper#(X), proper#(if(X1, X2, X3)) -> proper#(X2)) (proper#(s(X)) -> proper#(X), proper#(leq(X1, X2)) -> proper#(X1)) (proper#(s(X)) -> proper#(X), proper#(s(X)) -> proper#(X)) (proper#(s(X)) -> proper#(X), proper#(p(X)) -> proper#(X)) (proper#(if(X1, X2, X3)) -> proper#(X2), proper#(diff(X1, X2)) -> proper#(X2)) (proper#(if(X1, X2, X3)) -> proper#(X2), proper#(if(X1, X2, X3)) -> proper#(X2)) (proper#(if(X1, X2, X3)) -> proper#(X2), proper#(leq(X1, X2)) -> proper#(X1)) (proper#(if(X1, X2, X3)) -> proper#(X2), proper#(s(X)) -> proper#(X)) (proper#(if(X1, X2, X3)) -> proper#(X2), proper#(p(X)) -> proper#(X)) (proper#(diff(X1, X2)) -> proper#(X2), proper#(p(X)) -> proper#(X)) (proper#(diff(X1, X2)) -> proper#(X2), proper#(s(X)) -> proper#(X)) (proper#(diff(X1, X2)) -> proper#(X2), proper#(leq(X1, X2)) -> proper#(X1)) (proper#(diff(X1, X2)) -> proper#(X2), proper#(if(X1, X2, X3)) -> proper#(X2)) (proper#(diff(X1, X2)) -> proper#(X2), proper#(diff(X1, X2)) -> proper#(X2)) (proper#(leq(X1, X2)) -> proper#(X1), proper#(p(X)) -> proper#(X)) (proper#(leq(X1, X2)) -> proper#(X1), proper#(s(X)) -> proper#(X)) (proper#(leq(X1, X2)) -> proper#(X1), proper#(leq(X1, X2)) -> proper#(X1)) (proper#(leq(X1, X2)) -> proper#(X1), proper#(if(X1, X2, X3)) -> proper#(X2)) (proper#(leq(X1, X2)) -> proper#(X1), proper#(diff(X1, X2)) -> proper#(X2)) (proper#(p(X)) -> proper#(X), proper#(p(X)) -> proper#(X)) (proper#(p(X)) -> proper#(X), proper#(s(X)) -> proper#(X)) (proper#(p(X)) -> proper#(X), proper#(leq(X1, X2)) -> proper#(X1)) (proper#(p(X)) -> proper#(X), proper#(if(X1, X2, X3)) -> proper#(X2)) (proper#(p(X)) -> proper#(X), proper#(diff(X1, X2)) -> proper#(X2))} SCCS: Scc: { proper#(p(X)) -> proper#(X), proper#(s(X)) -> proper#(X), proper#(leq(X1, X2)) -> proper#(X1), proper#(if(X1, X2, X3)) -> proper#(X2), proper#(diff(X1, X2)) -> proper#(X2)} SCC: Strict: { proper#(p(X)) -> proper#(X), proper#(s(X)) -> proper#(X), proper#(leq(X1, X2)) -> proper#(X1), proper#(if(X1, X2, X3)) -> proper#(X2), proper#(diff(X1, X2)) -> proper#(X2)} Weak: { active(p(X)) -> p(active(X)), active(p(0())) -> mark(0()), active(p(s(X))) -> mark(X), active(s(X)) -> s(active(X)), active(leq(X1, X2)) -> leq(X1, active(X2)), active(leq(X1, X2)) -> leq(active(X1), X2), active(leq(0(), Y)) -> mark(true()), active(leq(s(X), 0())) -> mark(false()), active(leq(s(X), s(Y))) -> mark(leq(X, Y)), active(if(X1, X2, X3)) -> if(active(X1), X2, X3), active(if(true(), X, Y)) -> mark(X), active(if(false(), X, Y)) -> mark(Y), active(diff(X, Y)) -> mark(if(leq(X, Y), 0(), s(diff(p(X), Y)))), active(diff(X1, X2)) -> diff(X1, active(X2)), active(diff(X1, X2)) -> diff(active(X1), X2), p(mark(X)) -> mark(p(X)), p(ok(X)) -> ok(p(X)), s(mark(X)) -> mark(s(X)), s(ok(X)) -> ok(s(X)), leq(X1, mark(X2)) -> mark(leq(X1, X2)), leq(mark(X1), X2) -> mark(leq(X1, X2)), leq(ok(X1), ok(X2)) -> ok(leq(X1, X2)), if(mark(X1), X2, X3) -> mark(if(X1, X2, X3)), if(ok(X1), ok(X2), ok(X3)) -> ok(if(X1, X2, X3)), diff(X1, mark(X2)) -> mark(diff(X1, X2)), diff(mark(X1), X2) -> mark(diff(X1, X2)), diff(ok(X1), ok(X2)) -> ok(diff(X1, X2)), proper(0()) -> ok(0()), proper(p(X)) -> p(proper(X)), proper(s(X)) -> s(proper(X)), proper(true()) -> ok(true()), proper(leq(X1, X2)) -> leq(proper(X1), proper(X2)), proper(false()) -> ok(false()), proper(if(X1, X2, X3)) -> if(proper(X1), proper(X2), proper(X3)), proper(diff(X1, X2)) -> diff(proper(X1), proper(X2)), top(mark(X)) -> top(proper(X)), top(ok(X)) -> top(active(X))} SPSC: Simple Projection: pi(proper#) = 0 Strict: { proper#(p(X)) -> proper#(X), proper#(s(X)) -> proper#(X), proper#(leq(X1, X2)) -> proper#(X1), proper#(diff(X1, X2)) -> proper#(X2)} EDG: {(proper#(s(X)) -> proper#(X), proper#(diff(X1, X2)) -> proper#(X2)) (proper#(s(X)) -> proper#(X), proper#(leq(X1, X2)) -> proper#(X1)) (proper#(s(X)) -> proper#(X), proper#(s(X)) -> proper#(X)) (proper#(s(X)) -> proper#(X), proper#(p(X)) -> proper#(X)) (proper#(diff(X1, X2)) -> proper#(X2), proper#(diff(X1, X2)) -> proper#(X2)) (proper#(diff(X1, X2)) -> proper#(X2), proper#(leq(X1, X2)) -> proper#(X1)) (proper#(diff(X1, X2)) -> proper#(X2), proper#(s(X)) -> proper#(X)) (proper#(diff(X1, X2)) -> proper#(X2), proper#(p(X)) -> proper#(X)) (proper#(leq(X1, X2)) -> proper#(X1), proper#(p(X)) -> proper#(X)) (proper#(leq(X1, X2)) -> proper#(X1), proper#(s(X)) -> proper#(X)) (proper#(leq(X1, X2)) -> proper#(X1), proper#(leq(X1, X2)) -> proper#(X1)) (proper#(leq(X1, X2)) -> proper#(X1), proper#(diff(X1, X2)) -> proper#(X2)) (proper#(p(X)) -> proper#(X), proper#(p(X)) -> proper#(X)) (proper#(p(X)) -> proper#(X), proper#(s(X)) -> proper#(X)) (proper#(p(X)) -> proper#(X), proper#(leq(X1, X2)) -> proper#(X1)) (proper#(p(X)) -> proper#(X), proper#(diff(X1, X2)) -> proper#(X2))} SCCS: Scc: { proper#(p(X)) -> proper#(X), proper#(s(X)) -> proper#(X), proper#(leq(X1, X2)) -> proper#(X1), proper#(diff(X1, X2)) -> proper#(X2)} SCC: Strict: { proper#(p(X)) -> proper#(X), proper#(s(X)) -> proper#(X), proper#(leq(X1, X2)) -> proper#(X1), proper#(diff(X1, X2)) -> proper#(X2)} Weak: { active(p(X)) -> p(active(X)), active(p(0())) -> mark(0()), active(p(s(X))) -> mark(X), active(s(X)) -> s(active(X)), active(leq(X1, X2)) -> leq(X1, active(X2)), active(leq(X1, X2)) -> leq(active(X1), X2), active(leq(0(), Y)) -> mark(true()), active(leq(s(X), 0())) -> mark(false()), active(leq(s(X), s(Y))) -> mark(leq(X, Y)), active(if(X1, X2, X3)) -> if(active(X1), X2, X3), active(if(true(), X, Y)) -> mark(X), active(if(false(), X, Y)) -> mark(Y), active(diff(X, Y)) -> mark(if(leq(X, Y), 0(), s(diff(p(X), Y)))), active(diff(X1, X2)) -> diff(X1, active(X2)), active(diff(X1, X2)) -> diff(active(X1), X2), p(mark(X)) -> mark(p(X)), p(ok(X)) -> ok(p(X)), s(mark(X)) -> mark(s(X)), s(ok(X)) -> ok(s(X)), leq(X1, mark(X2)) -> mark(leq(X1, X2)), leq(mark(X1), X2) -> mark(leq(X1, X2)), leq(ok(X1), ok(X2)) -> ok(leq(X1, X2)), if(mark(X1), X2, X3) -> mark(if(X1, X2, X3)), if(ok(X1), ok(X2), ok(X3)) -> ok(if(X1, X2, X3)), diff(X1, mark(X2)) -> mark(diff(X1, X2)), diff(mark(X1), X2) -> mark(diff(X1, X2)), diff(ok(X1), ok(X2)) -> ok(diff(X1, X2)), proper(0()) -> ok(0()), proper(p(X)) -> p(proper(X)), proper(s(X)) -> s(proper(X)), proper(true()) -> ok(true()), proper(leq(X1, X2)) -> leq(proper(X1), proper(X2)), proper(false()) -> ok(false()), proper(if(X1, X2, X3)) -> if(proper(X1), proper(X2), proper(X3)), proper(diff(X1, X2)) -> diff(proper(X1), proper(X2)), top(mark(X)) -> top(proper(X)), top(ok(X)) -> top(active(X))} SPSC: Simple Projection: pi(proper#) = 0 Strict: { proper#(p(X)) -> proper#(X), proper#(s(X)) -> proper#(X), proper#(diff(X1, X2)) -> proper#(X2)} EDG: {(proper#(p(X)) -> proper#(X), proper#(diff(X1, X2)) -> proper#(X2)) (proper#(p(X)) -> proper#(X), proper#(s(X)) -> proper#(X)) (proper#(p(X)) -> proper#(X), proper#(p(X)) -> proper#(X)) (proper#(s(X)) -> proper#(X), proper#(p(X)) -> proper#(X)) (proper#(s(X)) -> proper#(X), proper#(s(X)) -> proper#(X)) (proper#(s(X)) -> proper#(X), proper#(diff(X1, X2)) -> proper#(X2)) (proper#(diff(X1, X2)) -> proper#(X2), proper#(p(X)) -> proper#(X)) (proper#(diff(X1, X2)) -> proper#(X2), proper#(s(X)) -> proper#(X)) (proper#(diff(X1, X2)) -> proper#(X2), proper#(diff(X1, X2)) -> proper#(X2))} SCCS: Scc: { proper#(p(X)) -> proper#(X), proper#(s(X)) -> proper#(X), proper#(diff(X1, X2)) -> proper#(X2)} SCC: Strict: { proper#(p(X)) -> proper#(X), proper#(s(X)) -> proper#(X), proper#(diff(X1, X2)) -> proper#(X2)} Weak: { active(p(X)) -> p(active(X)), active(p(0())) -> mark(0()), active(p(s(X))) -> mark(X), active(s(X)) -> s(active(X)), active(leq(X1, X2)) -> leq(X1, active(X2)), active(leq(X1, X2)) -> leq(active(X1), X2), active(leq(0(), Y)) -> mark(true()), active(leq(s(X), 0())) -> mark(false()), active(leq(s(X), s(Y))) -> mark(leq(X, Y)), active(if(X1, X2, X3)) -> if(active(X1), X2, X3), active(if(true(), X, Y)) -> mark(X), active(if(false(), X, Y)) -> mark(Y), active(diff(X, Y)) -> mark(if(leq(X, Y), 0(), s(diff(p(X), Y)))), active(diff(X1, X2)) -> diff(X1, active(X2)), active(diff(X1, X2)) -> diff(active(X1), X2), p(mark(X)) -> mark(p(X)), p(ok(X)) -> ok(p(X)), s(mark(X)) -> mark(s(X)), s(ok(X)) -> ok(s(X)), leq(X1, mark(X2)) -> mark(leq(X1, X2)), leq(mark(X1), X2) -> mark(leq(X1, X2)), leq(ok(X1), ok(X2)) -> ok(leq(X1, X2)), if(mark(X1), X2, X3) -> mark(if(X1, X2, X3)), if(ok(X1), ok(X2), ok(X3)) -> ok(if(X1, X2, X3)), diff(X1, mark(X2)) -> mark(diff(X1, X2)), diff(mark(X1), X2) -> mark(diff(X1, X2)), diff(ok(X1), ok(X2)) -> ok(diff(X1, X2)), proper(0()) -> ok(0()), proper(p(X)) -> p(proper(X)), proper(s(X)) -> s(proper(X)), proper(true()) -> ok(true()), proper(leq(X1, X2)) -> leq(proper(X1), proper(X2)), proper(false()) -> ok(false()), proper(if(X1, X2, X3)) -> if(proper(X1), proper(X2), proper(X3)), proper(diff(X1, X2)) -> diff(proper(X1), proper(X2)), top(mark(X)) -> top(proper(X)), top(ok(X)) -> top(active(X))} SPSC: Simple Projection: pi(proper#) = 0 Strict: { proper#(p(X)) -> proper#(X), proper#(diff(X1, X2)) -> proper#(X2)} EDG: {(proper#(diff(X1, X2)) -> proper#(X2), proper#(diff(X1, X2)) -> proper#(X2)) (proper#(diff(X1, X2)) -> proper#(X2), proper#(p(X)) -> proper#(X)) (proper#(p(X)) -> proper#(X), proper#(p(X)) -> proper#(X)) (proper#(p(X)) -> proper#(X), proper#(diff(X1, X2)) -> proper#(X2))} SCCS: Scc: { proper#(p(X)) -> proper#(X), proper#(diff(X1, X2)) -> proper#(X2)} SCC: Strict: { proper#(p(X)) -> proper#(X), proper#(diff(X1, X2)) -> proper#(X2)} Weak: { active(p(X)) -> p(active(X)), active(p(0())) -> mark(0()), active(p(s(X))) -> mark(X), active(s(X)) -> s(active(X)), active(leq(X1, X2)) -> leq(X1, active(X2)), active(leq(X1, X2)) -> leq(active(X1), X2), active(leq(0(), Y)) -> mark(true()), active(leq(s(X), 0())) -> mark(false()), active(leq(s(X), s(Y))) -> mark(leq(X, Y)), active(if(X1, X2, X3)) -> if(active(X1), X2, X3), active(if(true(), X, Y)) -> mark(X), active(if(false(), X, Y)) -> mark(Y), active(diff(X, Y)) -> mark(if(leq(X, Y), 0(), s(diff(p(X), Y)))), active(diff(X1, X2)) -> diff(X1, active(X2)), active(diff(X1, X2)) -> diff(active(X1), X2), p(mark(X)) -> mark(p(X)), p(ok(X)) -> ok(p(X)), s(mark(X)) -> mark(s(X)), s(ok(X)) -> ok(s(X)), leq(X1, mark(X2)) -> mark(leq(X1, X2)), leq(mark(X1), X2) -> mark(leq(X1, X2)), leq(ok(X1), ok(X2)) -> ok(leq(X1, X2)), if(mark(X1), X2, X3) -> mark(if(X1, X2, X3)), if(ok(X1), ok(X2), ok(X3)) -> ok(if(X1, X2, X3)), diff(X1, mark(X2)) -> mark(diff(X1, X2)), diff(mark(X1), X2) -> mark(diff(X1, X2)), diff(ok(X1), ok(X2)) -> ok(diff(X1, X2)), proper(0()) -> ok(0()), proper(p(X)) -> p(proper(X)), proper(s(X)) -> s(proper(X)), proper(true()) -> ok(true()), proper(leq(X1, X2)) -> leq(proper(X1), proper(X2)), proper(false()) -> ok(false()), proper(if(X1, X2, X3)) -> if(proper(X1), proper(X2), proper(X3)), proper(diff(X1, X2)) -> diff(proper(X1), proper(X2)), top(mark(X)) -> top(proper(X)), top(ok(X)) -> top(active(X))} SPSC: Simple Projection: pi(proper#) = 0 Strict: {proper#(diff(X1, X2)) -> proper#(X2)} EDG: {(proper#(diff(X1, X2)) -> proper#(X2), proper#(diff(X1, X2)) -> proper#(X2))} SCCS: Scc: {proper#(diff(X1, X2)) -> proper#(X2)} SCC: Strict: {proper#(diff(X1, X2)) -> proper#(X2)} Weak: { active(p(X)) -> p(active(X)), active(p(0())) -> mark(0()), active(p(s(X))) -> mark(X), active(s(X)) -> s(active(X)), active(leq(X1, X2)) -> leq(X1, active(X2)), active(leq(X1, X2)) -> leq(active(X1), X2), active(leq(0(), Y)) -> mark(true()), active(leq(s(X), 0())) -> mark(false()), active(leq(s(X), s(Y))) -> mark(leq(X, Y)), active(if(X1, X2, X3)) -> if(active(X1), X2, X3), active(if(true(), X, Y)) -> mark(X), active(if(false(), X, Y)) -> mark(Y), active(diff(X, Y)) -> mark(if(leq(X, Y), 0(), s(diff(p(X), Y)))), active(diff(X1, X2)) -> diff(X1, active(X2)), active(diff(X1, X2)) -> diff(active(X1), X2), p(mark(X)) -> mark(p(X)), p(ok(X)) -> ok(p(X)), s(mark(X)) -> mark(s(X)), s(ok(X)) -> ok(s(X)), leq(X1, mark(X2)) -> mark(leq(X1, X2)), leq(mark(X1), X2) -> mark(leq(X1, X2)), leq(ok(X1), ok(X2)) -> ok(leq(X1, X2)), if(mark(X1), X2, X3) -> mark(if(X1, X2, X3)), if(ok(X1), ok(X2), ok(X3)) -> ok(if(X1, X2, X3)), diff(X1, mark(X2)) -> mark(diff(X1, X2)), diff(mark(X1), X2) -> mark(diff(X1, X2)), diff(ok(X1), ok(X2)) -> ok(diff(X1, X2)), proper(0()) -> ok(0()), proper(p(X)) -> p(proper(X)), proper(s(X)) -> s(proper(X)), proper(true()) -> ok(true()), proper(leq(X1, X2)) -> leq(proper(X1), proper(X2)), proper(false()) -> ok(false()), proper(if(X1, X2, X3)) -> if(proper(X1), proper(X2), proper(X3)), proper(diff(X1, X2)) -> diff(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: { diff#(X1, mark(X2)) -> diff#(X1, X2), diff#(mark(X1), X2) -> diff#(X1, X2), diff#(ok(X1), ok(X2)) -> diff#(X1, X2)} Weak: { active(p(X)) -> p(active(X)), active(p(0())) -> mark(0()), active(p(s(X))) -> mark(X), active(s(X)) -> s(active(X)), active(leq(X1, X2)) -> leq(X1, active(X2)), active(leq(X1, X2)) -> leq(active(X1), X2), active(leq(0(), Y)) -> mark(true()), active(leq(s(X), 0())) -> mark(false()), active(leq(s(X), s(Y))) -> mark(leq(X, Y)), active(if(X1, X2, X3)) -> if(active(X1), X2, X3), active(if(true(), X, Y)) -> mark(X), active(if(false(), X, Y)) -> mark(Y), active(diff(X, Y)) -> mark(if(leq(X, Y), 0(), s(diff(p(X), Y)))), active(diff(X1, X2)) -> diff(X1, active(X2)), active(diff(X1, X2)) -> diff(active(X1), X2), p(mark(X)) -> mark(p(X)), p(ok(X)) -> ok(p(X)), s(mark(X)) -> mark(s(X)), s(ok(X)) -> ok(s(X)), leq(X1, mark(X2)) -> mark(leq(X1, X2)), leq(mark(X1), X2) -> mark(leq(X1, X2)), leq(ok(X1), ok(X2)) -> ok(leq(X1, X2)), if(mark(X1), X2, X3) -> mark(if(X1, X2, X3)), if(ok(X1), ok(X2), ok(X3)) -> ok(if(X1, X2, X3)), diff(X1, mark(X2)) -> mark(diff(X1, X2)), diff(mark(X1), X2) -> mark(diff(X1, X2)), diff(ok(X1), ok(X2)) -> ok(diff(X1, X2)), proper(0()) -> ok(0()), proper(p(X)) -> p(proper(X)), proper(s(X)) -> s(proper(X)), proper(true()) -> ok(true()), proper(leq(X1, X2)) -> leq(proper(X1), proper(X2)), proper(false()) -> ok(false()), proper(if(X1, X2, X3)) -> if(proper(X1), proper(X2), proper(X3)), proper(diff(X1, X2)) -> diff(proper(X1), proper(X2)), top(mark(X)) -> top(proper(X)), top(ok(X)) -> top(active(X))} SPSC: Simple Projection: pi(diff#) = 0 Strict: {diff#(X1, mark(X2)) -> diff#(X1, X2), diff#(mark(X1), X2) -> diff#(X1, X2)} EDG: {(diff#(mark(X1), X2) -> diff#(X1, X2), diff#(mark(X1), X2) -> diff#(X1, X2)) (diff#(mark(X1), X2) -> diff#(X1, X2), diff#(X1, mark(X2)) -> diff#(X1, X2)) (diff#(X1, mark(X2)) -> diff#(X1, X2), diff#(X1, mark(X2)) -> diff#(X1, X2)) (diff#(X1, mark(X2)) -> diff#(X1, X2), diff#(mark(X1), X2) -> diff#(X1, X2))} SCCS: Scc: {diff#(X1, mark(X2)) -> diff#(X1, X2), diff#(mark(X1), X2) -> diff#(X1, X2)} SCC: Strict: {diff#(X1, mark(X2)) -> diff#(X1, X2), diff#(mark(X1), X2) -> diff#(X1, X2)} Weak: { active(p(X)) -> p(active(X)), active(p(0())) -> mark(0()), active(p(s(X))) -> mark(X), active(s(X)) -> s(active(X)), active(leq(X1, X2)) -> leq(X1, active(X2)), active(leq(X1, X2)) -> leq(active(X1), X2), active(leq(0(), Y)) -> mark(true()), active(leq(s(X), 0())) -> mark(false()), active(leq(s(X), s(Y))) -> mark(leq(X, Y)), active(if(X1, X2, X3)) -> if(active(X1), X2, X3), active(if(true(), X, Y)) -> mark(X), active(if(false(), X, Y)) -> mark(Y), active(diff(X, Y)) -> mark(if(leq(X, Y), 0(), s(diff(p(X), Y)))), active(diff(X1, X2)) -> diff(X1, active(X2)), active(diff(X1, X2)) -> diff(active(X1), X2), p(mark(X)) -> mark(p(X)), p(ok(X)) -> ok(p(X)), s(mark(X)) -> mark(s(X)), s(ok(X)) -> ok(s(X)), leq(X1, mark(X2)) -> mark(leq(X1, X2)), leq(mark(X1), X2) -> mark(leq(X1, X2)), leq(ok(X1), ok(X2)) -> ok(leq(X1, X2)), if(mark(X1), X2, X3) -> mark(if(X1, X2, X3)), if(ok(X1), ok(X2), ok(X3)) -> ok(if(X1, X2, X3)), diff(X1, mark(X2)) -> mark(diff(X1, X2)), diff(mark(X1), X2) -> mark(diff(X1, X2)), diff(ok(X1), ok(X2)) -> ok(diff(X1, X2)), proper(0()) -> ok(0()), proper(p(X)) -> p(proper(X)), proper(s(X)) -> s(proper(X)), proper(true()) -> ok(true()), proper(leq(X1, X2)) -> leq(proper(X1), proper(X2)), proper(false()) -> ok(false()), proper(if(X1, X2, X3)) -> if(proper(X1), proper(X2), proper(X3)), proper(diff(X1, X2)) -> diff(proper(X1), proper(X2)), top(mark(X)) -> top(proper(X)), top(ok(X)) -> top(active(X))} SPSC: Simple Projection: pi(diff#) = 0 Strict: {diff#(X1, mark(X2)) -> diff#(X1, X2)} EDG: {(diff#(X1, mark(X2)) -> diff#(X1, X2), diff#(X1, mark(X2)) -> diff#(X1, X2))} SCCS: Scc: {diff#(X1, mark(X2)) -> diff#(X1, X2)} SCC: Strict: {diff#(X1, mark(X2)) -> diff#(X1, X2)} Weak: { active(p(X)) -> p(active(X)), active(p(0())) -> mark(0()), active(p(s(X))) -> mark(X), active(s(X)) -> s(active(X)), active(leq(X1, X2)) -> leq(X1, active(X2)), active(leq(X1, X2)) -> leq(active(X1), X2), active(leq(0(), Y)) -> mark(true()), active(leq(s(X), 0())) -> mark(false()), active(leq(s(X), s(Y))) -> mark(leq(X, Y)), active(if(X1, X2, X3)) -> if(active(X1), X2, X3), active(if(true(), X, Y)) -> mark(X), active(if(false(), X, Y)) -> mark(Y), active(diff(X, Y)) -> mark(if(leq(X, Y), 0(), s(diff(p(X), Y)))), active(diff(X1, X2)) -> diff(X1, active(X2)), active(diff(X1, X2)) -> diff(active(X1), X2), p(mark(X)) -> mark(p(X)), p(ok(X)) -> ok(p(X)), s(mark(X)) -> mark(s(X)), s(ok(X)) -> ok(s(X)), leq(X1, mark(X2)) -> mark(leq(X1, X2)), leq(mark(X1), X2) -> mark(leq(X1, X2)), leq(ok(X1), ok(X2)) -> ok(leq(X1, X2)), if(mark(X1), X2, X3) -> mark(if(X1, X2, X3)), if(ok(X1), ok(X2), ok(X3)) -> ok(if(X1, X2, X3)), diff(X1, mark(X2)) -> mark(diff(X1, X2)), diff(mark(X1), X2) -> mark(diff(X1, X2)), diff(ok(X1), ok(X2)) -> ok(diff(X1, X2)), proper(0()) -> ok(0()), proper(p(X)) -> p(proper(X)), proper(s(X)) -> s(proper(X)), proper(true()) -> ok(true()), proper(leq(X1, X2)) -> leq(proper(X1), proper(X2)), proper(false()) -> ok(false()), proper(if(X1, X2, X3)) -> if(proper(X1), proper(X2), proper(X3)), proper(diff(X1, X2)) -> diff(proper(X1), proper(X2)), top(mark(X)) -> top(proper(X)), top(ok(X)) -> top(active(X))} SPSC: Simple Projection: pi(diff#) = 1 Strict: {} Qed SCC: Strict: { if#(mark(X1), X2, X3) -> if#(X1, X2, X3), if#(ok(X1), ok(X2), ok(X3)) -> if#(X1, X2, X3)} Weak: { active(p(X)) -> p(active(X)), active(p(0())) -> mark(0()), active(p(s(X))) -> mark(X), active(s(X)) -> s(active(X)), active(leq(X1, X2)) -> leq(X1, active(X2)), active(leq(X1, X2)) -> leq(active(X1), X2), active(leq(0(), Y)) -> mark(true()), active(leq(s(X), 0())) -> mark(false()), active(leq(s(X), s(Y))) -> mark(leq(X, Y)), active(if(X1, X2, X3)) -> if(active(X1), X2, X3), active(if(true(), X, Y)) -> mark(X), active(if(false(), X, Y)) -> mark(Y), active(diff(X, Y)) -> mark(if(leq(X, Y), 0(), s(diff(p(X), Y)))), active(diff(X1, X2)) -> diff(X1, active(X2)), active(diff(X1, X2)) -> diff(active(X1), X2), p(mark(X)) -> mark(p(X)), p(ok(X)) -> ok(p(X)), s(mark(X)) -> mark(s(X)), s(ok(X)) -> ok(s(X)), leq(X1, mark(X2)) -> mark(leq(X1, X2)), leq(mark(X1), X2) -> mark(leq(X1, X2)), leq(ok(X1), ok(X2)) -> ok(leq(X1, X2)), if(mark(X1), X2, X3) -> mark(if(X1, X2, X3)), if(ok(X1), ok(X2), ok(X3)) -> ok(if(X1, X2, X3)), diff(X1, mark(X2)) -> mark(diff(X1, X2)), diff(mark(X1), X2) -> mark(diff(X1, X2)), diff(ok(X1), ok(X2)) -> ok(diff(X1, X2)), proper(0()) -> ok(0()), proper(p(X)) -> p(proper(X)), proper(s(X)) -> s(proper(X)), proper(true()) -> ok(true()), proper(leq(X1, X2)) -> leq(proper(X1), proper(X2)), proper(false()) -> ok(false()), proper(if(X1, X2, X3)) -> if(proper(X1), proper(X2), proper(X3)), proper(diff(X1, X2)) -> diff(proper(X1), proper(X2)), top(mark(X)) -> top(proper(X)), top(ok(X)) -> top(active(X))} SPSC: Simple Projection: pi(if#) = 0 Strict: {if#(mark(X1), X2, X3) -> if#(X1, X2, X3)} EDG: {(if#(mark(X1), X2, X3) -> if#(X1, X2, X3), if#(mark(X1), X2, X3) -> if#(X1, X2, X3))} SCCS: Scc: {if#(mark(X1), X2, X3) -> if#(X1, X2, X3)} SCC: Strict: {if#(mark(X1), X2, X3) -> if#(X1, X2, X3)} Weak: { active(p(X)) -> p(active(X)), active(p(0())) -> mark(0()), active(p(s(X))) -> mark(X), active(s(X)) -> s(active(X)), active(leq(X1, X2)) -> leq(X1, active(X2)), active(leq(X1, X2)) -> leq(active(X1), X2), active(leq(0(), Y)) -> mark(true()), active(leq(s(X), 0())) -> mark(false()), active(leq(s(X), s(Y))) -> mark(leq(X, Y)), active(if(X1, X2, X3)) -> if(active(X1), X2, X3), active(if(true(), X, Y)) -> mark(X), active(if(false(), X, Y)) -> mark(Y), active(diff(X, Y)) -> mark(if(leq(X, Y), 0(), s(diff(p(X), Y)))), active(diff(X1, X2)) -> diff(X1, active(X2)), active(diff(X1, X2)) -> diff(active(X1), X2), p(mark(X)) -> mark(p(X)), p(ok(X)) -> ok(p(X)), s(mark(X)) -> mark(s(X)), s(ok(X)) -> ok(s(X)), leq(X1, mark(X2)) -> mark(leq(X1, X2)), leq(mark(X1), X2) -> mark(leq(X1, X2)), leq(ok(X1), ok(X2)) -> ok(leq(X1, X2)), if(mark(X1), X2, X3) -> mark(if(X1, X2, X3)), if(ok(X1), ok(X2), ok(X3)) -> ok(if(X1, X2, X3)), diff(X1, mark(X2)) -> mark(diff(X1, X2)), diff(mark(X1), X2) -> mark(diff(X1, X2)), diff(ok(X1), ok(X2)) -> ok(diff(X1, X2)), proper(0()) -> ok(0()), proper(p(X)) -> p(proper(X)), proper(s(X)) -> s(proper(X)), proper(true()) -> ok(true()), proper(leq(X1, X2)) -> leq(proper(X1), proper(X2)), proper(false()) -> ok(false()), proper(if(X1, X2, X3)) -> if(proper(X1), proper(X2), proper(X3)), proper(diff(X1, X2)) -> diff(proper(X1), proper(X2)), top(mark(X)) -> top(proper(X)), top(ok(X)) -> top(active(X))} SPSC: Simple Projection: pi(if#) = 0 Strict: {} Qed SCC: Strict: { leq#(X1, mark(X2)) -> leq#(X1, X2), leq#(mark(X1), X2) -> leq#(X1, X2), leq#(ok(X1), ok(X2)) -> leq#(X1, X2)} Weak: { active(p(X)) -> p(active(X)), active(p(0())) -> mark(0()), active(p(s(X))) -> mark(X), active(s(X)) -> s(active(X)), active(leq(X1, X2)) -> leq(X1, active(X2)), active(leq(X1, X2)) -> leq(active(X1), X2), active(leq(0(), Y)) -> mark(true()), active(leq(s(X), 0())) -> mark(false()), active(leq(s(X), s(Y))) -> mark(leq(X, Y)), active(if(X1, X2, X3)) -> if(active(X1), X2, X3), active(if(true(), X, Y)) -> mark(X), active(if(false(), X, Y)) -> mark(Y), active(diff(X, Y)) -> mark(if(leq(X, Y), 0(), s(diff(p(X), Y)))), active(diff(X1, X2)) -> diff(X1, active(X2)), active(diff(X1, X2)) -> diff(active(X1), X2), p(mark(X)) -> mark(p(X)), p(ok(X)) -> ok(p(X)), s(mark(X)) -> mark(s(X)), s(ok(X)) -> ok(s(X)), leq(X1, mark(X2)) -> mark(leq(X1, X2)), leq(mark(X1), X2) -> mark(leq(X1, X2)), leq(ok(X1), ok(X2)) -> ok(leq(X1, X2)), if(mark(X1), X2, X3) -> mark(if(X1, X2, X3)), if(ok(X1), ok(X2), ok(X3)) -> ok(if(X1, X2, X3)), diff(X1, mark(X2)) -> mark(diff(X1, X2)), diff(mark(X1), X2) -> mark(diff(X1, X2)), diff(ok(X1), ok(X2)) -> ok(diff(X1, X2)), proper(0()) -> ok(0()), proper(p(X)) -> p(proper(X)), proper(s(X)) -> s(proper(X)), proper(true()) -> ok(true()), proper(leq(X1, X2)) -> leq(proper(X1), proper(X2)), proper(false()) -> ok(false()), proper(if(X1, X2, X3)) -> if(proper(X1), proper(X2), proper(X3)), proper(diff(X1, X2)) -> diff(proper(X1), proper(X2)), top(mark(X)) -> top(proper(X)), top(ok(X)) -> top(active(X))} SPSC: Simple Projection: pi(leq#) = 0 Strict: { leq#(X1, mark(X2)) -> leq#(X1, X2), leq#(ok(X1), ok(X2)) -> leq#(X1, X2)} EDG: {(leq#(ok(X1), ok(X2)) -> leq#(X1, X2), leq#(ok(X1), ok(X2)) -> leq#(X1, X2)) (leq#(ok(X1), ok(X2)) -> leq#(X1, X2), leq#(X1, mark(X2)) -> leq#(X1, X2)) (leq#(X1, mark(X2)) -> leq#(X1, X2), leq#(X1, mark(X2)) -> leq#(X1, X2)) (leq#(X1, mark(X2)) -> leq#(X1, X2), leq#(ok(X1), ok(X2)) -> leq#(X1, X2))} SCCS: Scc: { leq#(X1, mark(X2)) -> leq#(X1, X2), leq#(ok(X1), ok(X2)) -> leq#(X1, X2)} SCC: Strict: { leq#(X1, mark(X2)) -> leq#(X1, X2), leq#(ok(X1), ok(X2)) -> leq#(X1, X2)} Weak: { active(p(X)) -> p(active(X)), active(p(0())) -> mark(0()), active(p(s(X))) -> mark(X), active(s(X)) -> s(active(X)), active(leq(X1, X2)) -> leq(X1, active(X2)), active(leq(X1, X2)) -> leq(active(X1), X2), active(leq(0(), Y)) -> mark(true()), active(leq(s(X), 0())) -> mark(false()), active(leq(s(X), s(Y))) -> mark(leq(X, Y)), active(if(X1, X2, X3)) -> if(active(X1), X2, X3), active(if(true(), X, Y)) -> mark(X), active(if(false(), X, Y)) -> mark(Y), active(diff(X, Y)) -> mark(if(leq(X, Y), 0(), s(diff(p(X), Y)))), active(diff(X1, X2)) -> diff(X1, active(X2)), active(diff(X1, X2)) -> diff(active(X1), X2), p(mark(X)) -> mark(p(X)), p(ok(X)) -> ok(p(X)), s(mark(X)) -> mark(s(X)), s(ok(X)) -> ok(s(X)), leq(X1, mark(X2)) -> mark(leq(X1, X2)), leq(mark(X1), X2) -> mark(leq(X1, X2)), leq(ok(X1), ok(X2)) -> ok(leq(X1, X2)), if(mark(X1), X2, X3) -> mark(if(X1, X2, X3)), if(ok(X1), ok(X2), ok(X3)) -> ok(if(X1, X2, X3)), diff(X1, mark(X2)) -> mark(diff(X1, X2)), diff(mark(X1), X2) -> mark(diff(X1, X2)), diff(ok(X1), ok(X2)) -> ok(diff(X1, X2)), proper(0()) -> ok(0()), proper(p(X)) -> p(proper(X)), proper(s(X)) -> s(proper(X)), proper(true()) -> ok(true()), proper(leq(X1, X2)) -> leq(proper(X1), proper(X2)), proper(false()) -> ok(false()), proper(if(X1, X2, X3)) -> if(proper(X1), proper(X2), proper(X3)), proper(diff(X1, X2)) -> diff(proper(X1), proper(X2)), top(mark(X)) -> top(proper(X)), top(ok(X)) -> top(active(X))} SPSC: Simple Projection: pi(leq#) = 0 Strict: {leq#(X1, mark(X2)) -> leq#(X1, X2)} EDG: {(leq#(X1, mark(X2)) -> leq#(X1, X2), leq#(X1, mark(X2)) -> leq#(X1, X2))} SCCS: Scc: {leq#(X1, mark(X2)) -> leq#(X1, X2)} SCC: Strict: {leq#(X1, mark(X2)) -> leq#(X1, X2)} Weak: { active(p(X)) -> p(active(X)), active(p(0())) -> mark(0()), active(p(s(X))) -> mark(X), active(s(X)) -> s(active(X)), active(leq(X1, X2)) -> leq(X1, active(X2)), active(leq(X1, X2)) -> leq(active(X1), X2), active(leq(0(), Y)) -> mark(true()), active(leq(s(X), 0())) -> mark(false()), active(leq(s(X), s(Y))) -> mark(leq(X, Y)), active(if(X1, X2, X3)) -> if(active(X1), X2, X3), active(if(true(), X, Y)) -> mark(X), active(if(false(), X, Y)) -> mark(Y), active(diff(X, Y)) -> mark(if(leq(X, Y), 0(), s(diff(p(X), Y)))), active(diff(X1, X2)) -> diff(X1, active(X2)), active(diff(X1, X2)) -> diff(active(X1), X2), p(mark(X)) -> mark(p(X)), p(ok(X)) -> ok(p(X)), s(mark(X)) -> mark(s(X)), s(ok(X)) -> ok(s(X)), leq(X1, mark(X2)) -> mark(leq(X1, X2)), leq(mark(X1), X2) -> mark(leq(X1, X2)), leq(ok(X1), ok(X2)) -> ok(leq(X1, X2)), if(mark(X1), X2, X3) -> mark(if(X1, X2, X3)), if(ok(X1), ok(X2), ok(X3)) -> ok(if(X1, X2, X3)), diff(X1, mark(X2)) -> mark(diff(X1, X2)), diff(mark(X1), X2) -> mark(diff(X1, X2)), diff(ok(X1), ok(X2)) -> ok(diff(X1, X2)), proper(0()) -> ok(0()), proper(p(X)) -> p(proper(X)), proper(s(X)) -> s(proper(X)), proper(true()) -> ok(true()), proper(leq(X1, X2)) -> leq(proper(X1), proper(X2)), proper(false()) -> ok(false()), proper(if(X1, X2, X3)) -> if(proper(X1), proper(X2), proper(X3)), proper(diff(X1, X2)) -> diff(proper(X1), proper(X2)), top(mark(X)) -> top(proper(X)), top(ok(X)) -> top(active(X))} SPSC: Simple Projection: pi(leq#) = 1 Strict: {} Qed SCC: Strict: {s#(mark(X)) -> s#(X), s#(ok(X)) -> s#(X)} Weak: { active(p(X)) -> p(active(X)), active(p(0())) -> mark(0()), active(p(s(X))) -> mark(X), active(s(X)) -> s(active(X)), active(leq(X1, X2)) -> leq(X1, active(X2)), active(leq(X1, X2)) -> leq(active(X1), X2), active(leq(0(), Y)) -> mark(true()), active(leq(s(X), 0())) -> mark(false()), active(leq(s(X), s(Y))) -> mark(leq(X, Y)), active(if(X1, X2, X3)) -> if(active(X1), X2, X3), active(if(true(), X, Y)) -> mark(X), active(if(false(), X, Y)) -> mark(Y), active(diff(X, Y)) -> mark(if(leq(X, Y), 0(), s(diff(p(X), Y)))), active(diff(X1, X2)) -> diff(X1, active(X2)), active(diff(X1, X2)) -> diff(active(X1), X2), p(mark(X)) -> mark(p(X)), p(ok(X)) -> ok(p(X)), s(mark(X)) -> mark(s(X)), s(ok(X)) -> ok(s(X)), leq(X1, mark(X2)) -> mark(leq(X1, X2)), leq(mark(X1), X2) -> mark(leq(X1, X2)), leq(ok(X1), ok(X2)) -> ok(leq(X1, X2)), if(mark(X1), X2, X3) -> mark(if(X1, X2, X3)), if(ok(X1), ok(X2), ok(X3)) -> ok(if(X1, X2, X3)), diff(X1, mark(X2)) -> mark(diff(X1, X2)), diff(mark(X1), X2) -> mark(diff(X1, X2)), diff(ok(X1), ok(X2)) -> ok(diff(X1, X2)), proper(0()) -> ok(0()), proper(p(X)) -> p(proper(X)), proper(s(X)) -> s(proper(X)), proper(true()) -> ok(true()), proper(leq(X1, X2)) -> leq(proper(X1), proper(X2)), proper(false()) -> ok(false()), proper(if(X1, X2, X3)) -> if(proper(X1), proper(X2), proper(X3)), proper(diff(X1, X2)) -> diff(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: { active(p(X)) -> p(active(X)), active(p(0())) -> mark(0()), active(p(s(X))) -> mark(X), active(s(X)) -> s(active(X)), active(leq(X1, X2)) -> leq(X1, active(X2)), active(leq(X1, X2)) -> leq(active(X1), X2), active(leq(0(), Y)) -> mark(true()), active(leq(s(X), 0())) -> mark(false()), active(leq(s(X), s(Y))) -> mark(leq(X, Y)), active(if(X1, X2, X3)) -> if(active(X1), X2, X3), active(if(true(), X, Y)) -> mark(X), active(if(false(), X, Y)) -> mark(Y), active(diff(X, Y)) -> mark(if(leq(X, Y), 0(), s(diff(p(X), Y)))), active(diff(X1, X2)) -> diff(X1, active(X2)), active(diff(X1, X2)) -> diff(active(X1), X2), p(mark(X)) -> mark(p(X)), p(ok(X)) -> ok(p(X)), s(mark(X)) -> mark(s(X)), s(ok(X)) -> ok(s(X)), leq(X1, mark(X2)) -> mark(leq(X1, X2)), leq(mark(X1), X2) -> mark(leq(X1, X2)), leq(ok(X1), ok(X2)) -> ok(leq(X1, X2)), if(mark(X1), X2, X3) -> mark(if(X1, X2, X3)), if(ok(X1), ok(X2), ok(X3)) -> ok(if(X1, X2, X3)), diff(X1, mark(X2)) -> mark(diff(X1, X2)), diff(mark(X1), X2) -> mark(diff(X1, X2)), diff(ok(X1), ok(X2)) -> ok(diff(X1, X2)), proper(0()) -> ok(0()), proper(p(X)) -> p(proper(X)), proper(s(X)) -> s(proper(X)), proper(true()) -> ok(true()), proper(leq(X1, X2)) -> leq(proper(X1), proper(X2)), proper(false()) -> ok(false()), proper(if(X1, X2, X3)) -> if(proper(X1), proper(X2), proper(X3)), proper(diff(X1, X2)) -> diff(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: {p#(mark(X)) -> p#(X), p#(ok(X)) -> p#(X)} Weak: { active(p(X)) -> p(active(X)), active(p(0())) -> mark(0()), active(p(s(X))) -> mark(X), active(s(X)) -> s(active(X)), active(leq(X1, X2)) -> leq(X1, active(X2)), active(leq(X1, X2)) -> leq(active(X1), X2), active(leq(0(), Y)) -> mark(true()), active(leq(s(X), 0())) -> mark(false()), active(leq(s(X), s(Y))) -> mark(leq(X, Y)), active(if(X1, X2, X3)) -> if(active(X1), X2, X3), active(if(true(), X, Y)) -> mark(X), active(if(false(), X, Y)) -> mark(Y), active(diff(X, Y)) -> mark(if(leq(X, Y), 0(), s(diff(p(X), Y)))), active(diff(X1, X2)) -> diff(X1, active(X2)), active(diff(X1, X2)) -> diff(active(X1), X2), p(mark(X)) -> mark(p(X)), p(ok(X)) -> ok(p(X)), s(mark(X)) -> mark(s(X)), s(ok(X)) -> ok(s(X)), leq(X1, mark(X2)) -> mark(leq(X1, X2)), leq(mark(X1), X2) -> mark(leq(X1, X2)), leq(ok(X1), ok(X2)) -> ok(leq(X1, X2)), if(mark(X1), X2, X3) -> mark(if(X1, X2, X3)), if(ok(X1), ok(X2), ok(X3)) -> ok(if(X1, X2, X3)), diff(X1, mark(X2)) -> mark(diff(X1, X2)), diff(mark(X1), X2) -> mark(diff(X1, X2)), diff(ok(X1), ok(X2)) -> ok(diff(X1, X2)), proper(0()) -> ok(0()), proper(p(X)) -> p(proper(X)), proper(s(X)) -> s(proper(X)), proper(true()) -> ok(true()), proper(leq(X1, X2)) -> leq(proper(X1), proper(X2)), proper(false()) -> ok(false()), proper(if(X1, X2, X3)) -> if(proper(X1), proper(X2), proper(X3)), proper(diff(X1, X2)) -> diff(proper(X1), proper(X2)), top(mark(X)) -> top(proper(X)), top(ok(X)) -> top(active(X))} SPSC: Simple Projection: pi(p#) = 0 Strict: {p#(ok(X)) -> p#(X)} EDG: {(p#(ok(X)) -> p#(X), p#(ok(X)) -> p#(X))} SCCS: Scc: {p#(ok(X)) -> p#(X)} SCC: Strict: {p#(ok(X)) -> p#(X)} Weak: { active(p(X)) -> p(active(X)), active(p(0())) -> mark(0()), active(p(s(X))) -> mark(X), active(s(X)) -> s(active(X)), active(leq(X1, X2)) -> leq(X1, active(X2)), active(leq(X1, X2)) -> leq(active(X1), X2), active(leq(0(), Y)) -> mark(true()), active(leq(s(X), 0())) -> mark(false()), active(leq(s(X), s(Y))) -> mark(leq(X, Y)), active(if(X1, X2, X3)) -> if(active(X1), X2, X3), active(if(true(), X, Y)) -> mark(X), active(if(false(), X, Y)) -> mark(Y), active(diff(X, Y)) -> mark(if(leq(X, Y), 0(), s(diff(p(X), Y)))), active(diff(X1, X2)) -> diff(X1, active(X2)), active(diff(X1, X2)) -> diff(active(X1), X2), p(mark(X)) -> mark(p(X)), p(ok(X)) -> ok(p(X)), s(mark(X)) -> mark(s(X)), s(ok(X)) -> ok(s(X)), leq(X1, mark(X2)) -> mark(leq(X1, X2)), leq(mark(X1), X2) -> mark(leq(X1, X2)), leq(ok(X1), ok(X2)) -> ok(leq(X1, X2)), if(mark(X1), X2, X3) -> mark(if(X1, X2, X3)), if(ok(X1), ok(X2), ok(X3)) -> ok(if(X1, X2, X3)), diff(X1, mark(X2)) -> mark(diff(X1, X2)), diff(mark(X1), X2) -> mark(diff(X1, X2)), diff(ok(X1), ok(X2)) -> ok(diff(X1, X2)), proper(0()) -> ok(0()), proper(p(X)) -> p(proper(X)), proper(s(X)) -> s(proper(X)), proper(true()) -> ok(true()), proper(leq(X1, X2)) -> leq(proper(X1), proper(X2)), proper(false()) -> ok(false()), proper(if(X1, X2, X3)) -> if(proper(X1), proper(X2), proper(X3)), proper(diff(X1, X2)) -> diff(proper(X1), proper(X2)), top(mark(X)) -> top(proper(X)), top(ok(X)) -> top(active(X))} SPSC: Simple Projection: pi(p#) = 0 Strict: {} Qed SCC: Strict: { active#(p(X)) -> active#(X), active#(s(X)) -> active#(X), active#(leq(X1, X2)) -> active#(X1), active#(leq(X1, X2)) -> active#(X2), active#(if(X1, X2, X3)) -> active#(X1), active#(diff(X1, X2)) -> active#(X1), active#(diff(X1, X2)) -> active#(X2)} Weak: { active(p(X)) -> p(active(X)), active(p(0())) -> mark(0()), active(p(s(X))) -> mark(X), active(s(X)) -> s(active(X)), active(leq(X1, X2)) -> leq(X1, active(X2)), active(leq(X1, X2)) -> leq(active(X1), X2), active(leq(0(), Y)) -> mark(true()), active(leq(s(X), 0())) -> mark(false()), active(leq(s(X), s(Y))) -> mark(leq(X, Y)), active(if(X1, X2, X3)) -> if(active(X1), X2, X3), active(if(true(), X, Y)) -> mark(X), active(if(false(), X, Y)) -> mark(Y), active(diff(X, Y)) -> mark(if(leq(X, Y), 0(), s(diff(p(X), Y)))), active(diff(X1, X2)) -> diff(X1, active(X2)), active(diff(X1, X2)) -> diff(active(X1), X2), p(mark(X)) -> mark(p(X)), p(ok(X)) -> ok(p(X)), s(mark(X)) -> mark(s(X)), s(ok(X)) -> ok(s(X)), leq(X1, mark(X2)) -> mark(leq(X1, X2)), leq(mark(X1), X2) -> mark(leq(X1, X2)), leq(ok(X1), ok(X2)) -> ok(leq(X1, X2)), if(mark(X1), X2, X3) -> mark(if(X1, X2, X3)), if(ok(X1), ok(X2), ok(X3)) -> ok(if(X1, X2, X3)), diff(X1, mark(X2)) -> mark(diff(X1, X2)), diff(mark(X1), X2) -> mark(diff(X1, X2)), diff(ok(X1), ok(X2)) -> ok(diff(X1, X2)), proper(0()) -> ok(0()), proper(p(X)) -> p(proper(X)), proper(s(X)) -> s(proper(X)), proper(true()) -> ok(true()), proper(leq(X1, X2)) -> leq(proper(X1), proper(X2)), proper(false()) -> ok(false()), proper(if(X1, X2, X3)) -> if(proper(X1), proper(X2), proper(X3)), proper(diff(X1, X2)) -> diff(proper(X1), proper(X2)), top(mark(X)) -> top(proper(X)), top(ok(X)) -> top(active(X))} SPSC: Simple Projection: pi(active#) = 0 Strict: { active#(p(X)) -> active#(X), active#(s(X)) -> active#(X), active#(leq(X1, X2)) -> active#(X1), active#(leq(X1, X2)) -> active#(X2), active#(if(X1, X2, X3)) -> active#(X1), active#(diff(X1, X2)) -> active#(X2)} EDG: {(active#(if(X1, X2, X3)) -> active#(X1), active#(diff(X1, X2)) -> active#(X2)) (active#(if(X1, X2, X3)) -> active#(X1), active#(if(X1, X2, X3)) -> active#(X1)) (active#(if(X1, X2, X3)) -> active#(X1), active#(leq(X1, X2)) -> active#(X2)) (active#(if(X1, X2, X3)) -> active#(X1), active#(leq(X1, X2)) -> active#(X1)) (active#(if(X1, X2, X3)) -> active#(X1), active#(s(X)) -> active#(X)) (active#(if(X1, X2, X3)) -> active#(X1), active#(p(X)) -> active#(X)) (active#(s(X)) -> active#(X), active#(diff(X1, X2)) -> active#(X2)) (active#(s(X)) -> active#(X), active#(if(X1, X2, X3)) -> active#(X1)) (active#(s(X)) -> active#(X), active#(leq(X1, X2)) -> active#(X2)) (active#(s(X)) -> active#(X), active#(leq(X1, X2)) -> active#(X1)) (active#(s(X)) -> active#(X), active#(s(X)) -> active#(X)) (active#(s(X)) -> active#(X), active#(p(X)) -> active#(X)) (active#(diff(X1, X2)) -> active#(X2), active#(diff(X1, X2)) -> active#(X2)) (active#(diff(X1, X2)) -> active#(X2), active#(if(X1, X2, X3)) -> active#(X1)) (active#(diff(X1, X2)) -> active#(X2), active#(leq(X1, X2)) -> active#(X2)) (active#(diff(X1, X2)) -> active#(X2), active#(leq(X1, X2)) -> active#(X1)) (active#(diff(X1, X2)) -> active#(X2), active#(s(X)) -> active#(X)) (active#(diff(X1, X2)) -> active#(X2), active#(p(X)) -> active#(X)) (active#(leq(X1, X2)) -> active#(X2), active#(p(X)) -> active#(X)) (active#(leq(X1, X2)) -> active#(X2), active#(s(X)) -> active#(X)) (active#(leq(X1, X2)) -> active#(X2), active#(leq(X1, X2)) -> active#(X1)) (active#(leq(X1, X2)) -> active#(X2), active#(leq(X1, X2)) -> active#(X2)) (active#(leq(X1, X2)) -> active#(X2), active#(if(X1, X2, X3)) -> active#(X1)) (active#(leq(X1, X2)) -> active#(X2), active#(diff(X1, X2)) -> active#(X2)) (active#(p(X)) -> active#(X), active#(p(X)) -> active#(X)) (active#(p(X)) -> active#(X), active#(s(X)) -> active#(X)) (active#(p(X)) -> active#(X), active#(leq(X1, X2)) -> active#(X1)) (active#(p(X)) -> active#(X), active#(leq(X1, X2)) -> active#(X2)) (active#(p(X)) -> active#(X), active#(if(X1, X2, X3)) -> active#(X1)) (active#(p(X)) -> active#(X), active#(diff(X1, X2)) -> active#(X2)) (active#(leq(X1, X2)) -> active#(X1), active#(p(X)) -> active#(X)) (active#(leq(X1, X2)) -> active#(X1), active#(s(X)) -> active#(X)) (active#(leq(X1, X2)) -> active#(X1), active#(leq(X1, X2)) -> active#(X1)) (active#(leq(X1, X2)) -> active#(X1), active#(leq(X1, X2)) -> active#(X2)) (active#(leq(X1, X2)) -> active#(X1), active#(if(X1, X2, X3)) -> active#(X1)) (active#(leq(X1, X2)) -> active#(X1), active#(diff(X1, X2)) -> active#(X2))} SCCS: Scc: { active#(p(X)) -> active#(X), active#(s(X)) -> active#(X), active#(leq(X1, X2)) -> active#(X1), active#(leq(X1, X2)) -> active#(X2), active#(if(X1, X2, X3)) -> active#(X1), active#(diff(X1, X2)) -> active#(X2)} SCC: Strict: { active#(p(X)) -> active#(X), active#(s(X)) -> active#(X), active#(leq(X1, X2)) -> active#(X1), active#(leq(X1, X2)) -> active#(X2), active#(if(X1, X2, X3)) -> active#(X1), active#(diff(X1, X2)) -> active#(X2)} Weak: { active(p(X)) -> p(active(X)), active(p(0())) -> mark(0()), active(p(s(X))) -> mark(X), active(s(X)) -> s(active(X)), active(leq(X1, X2)) -> leq(X1, active(X2)), active(leq(X1, X2)) -> leq(active(X1), X2), active(leq(0(), Y)) -> mark(true()), active(leq(s(X), 0())) -> mark(false()), active(leq(s(X), s(Y))) -> mark(leq(X, Y)), active(if(X1, X2, X3)) -> if(active(X1), X2, X3), active(if(true(), X, Y)) -> mark(X), active(if(false(), X, Y)) -> mark(Y), active(diff(X, Y)) -> mark(if(leq(X, Y), 0(), s(diff(p(X), Y)))), active(diff(X1, X2)) -> diff(X1, active(X2)), active(diff(X1, X2)) -> diff(active(X1), X2), p(mark(X)) -> mark(p(X)), p(ok(X)) -> ok(p(X)), s(mark(X)) -> mark(s(X)), s(ok(X)) -> ok(s(X)), leq(X1, mark(X2)) -> mark(leq(X1, X2)), leq(mark(X1), X2) -> mark(leq(X1, X2)), leq(ok(X1), ok(X2)) -> ok(leq(X1, X2)), if(mark(X1), X2, X3) -> mark(if(X1, X2, X3)), if(ok(X1), ok(X2), ok(X3)) -> ok(if(X1, X2, X3)), diff(X1, mark(X2)) -> mark(diff(X1, X2)), diff(mark(X1), X2) -> mark(diff(X1, X2)), diff(ok(X1), ok(X2)) -> ok(diff(X1, X2)), proper(0()) -> ok(0()), proper(p(X)) -> p(proper(X)), proper(s(X)) -> s(proper(X)), proper(true()) -> ok(true()), proper(leq(X1, X2)) -> leq(proper(X1), proper(X2)), proper(false()) -> ok(false()), proper(if(X1, X2, X3)) -> if(proper(X1), proper(X2), proper(X3)), proper(diff(X1, X2)) -> diff(proper(X1), proper(X2)), top(mark(X)) -> top(proper(X)), top(ok(X)) -> top(active(X))} SPSC: Simple Projection: pi(active#) = 0 Strict: { active#(p(X)) -> active#(X), active#(s(X)) -> active#(X), active#(leq(X1, X2)) -> active#(X1), active#(leq(X1, X2)) -> active#(X2), active#(diff(X1, X2)) -> active#(X2)} EDG: {(active#(s(X)) -> active#(X), active#(diff(X1, X2)) -> active#(X2)) (active#(s(X)) -> active#(X), active#(leq(X1, X2)) -> active#(X2)) (active#(s(X)) -> active#(X), active#(leq(X1, X2)) -> active#(X1)) (active#(s(X)) -> active#(X), active#(s(X)) -> active#(X)) (active#(s(X)) -> active#(X), active#(p(X)) -> active#(X)) (active#(leq(X1, X2)) -> active#(X2), active#(diff(X1, X2)) -> active#(X2)) (active#(leq(X1, X2)) -> active#(X2), active#(leq(X1, X2)) -> active#(X2)) (active#(leq(X1, X2)) -> active#(X2), active#(leq(X1, X2)) -> active#(X1)) (active#(leq(X1, X2)) -> active#(X2), active#(s(X)) -> active#(X)) (active#(leq(X1, X2)) -> active#(X2), active#(p(X)) -> active#(X)) (active#(diff(X1, X2)) -> active#(X2), active#(p(X)) -> active#(X)) (active#(diff(X1, X2)) -> active#(X2), active#(s(X)) -> active#(X)) (active#(diff(X1, X2)) -> active#(X2), active#(leq(X1, X2)) -> active#(X1)) (active#(diff(X1, X2)) -> active#(X2), active#(leq(X1, X2)) -> active#(X2)) (active#(diff(X1, X2)) -> active#(X2), active#(diff(X1, X2)) -> active#(X2)) (active#(leq(X1, X2)) -> active#(X1), active#(p(X)) -> active#(X)) (active#(leq(X1, X2)) -> active#(X1), active#(s(X)) -> active#(X)) (active#(leq(X1, X2)) -> active#(X1), active#(leq(X1, X2)) -> active#(X1)) (active#(leq(X1, X2)) -> active#(X1), active#(leq(X1, X2)) -> active#(X2)) (active#(leq(X1, X2)) -> active#(X1), active#(diff(X1, X2)) -> active#(X2)) (active#(p(X)) -> active#(X), active#(p(X)) -> active#(X)) (active#(p(X)) -> active#(X), active#(s(X)) -> active#(X)) (active#(p(X)) -> active#(X), active#(leq(X1, X2)) -> active#(X1)) (active#(p(X)) -> active#(X), active#(leq(X1, X2)) -> active#(X2)) (active#(p(X)) -> active#(X), active#(diff(X1, X2)) -> active#(X2))} SCCS: Scc: { active#(p(X)) -> active#(X), active#(s(X)) -> active#(X), active#(leq(X1, X2)) -> active#(X1), active#(leq(X1, X2)) -> active#(X2), active#(diff(X1, X2)) -> active#(X2)} SCC: Strict: { active#(p(X)) -> active#(X), active#(s(X)) -> active#(X), active#(leq(X1, X2)) -> active#(X1), active#(leq(X1, X2)) -> active#(X2), active#(diff(X1, X2)) -> active#(X2)} Weak: { active(p(X)) -> p(active(X)), active(p(0())) -> mark(0()), active(p(s(X))) -> mark(X), active(s(X)) -> s(active(X)), active(leq(X1, X2)) -> leq(X1, active(X2)), active(leq(X1, X2)) -> leq(active(X1), X2), active(leq(0(), Y)) -> mark(true()), active(leq(s(X), 0())) -> mark(false()), active(leq(s(X), s(Y))) -> mark(leq(X, Y)), active(if(X1, X2, X3)) -> if(active(X1), X2, X3), active(if(true(), X, Y)) -> mark(X), active(if(false(), X, Y)) -> mark(Y), active(diff(X, Y)) -> mark(if(leq(X, Y), 0(), s(diff(p(X), Y)))), active(diff(X1, X2)) -> diff(X1, active(X2)), active(diff(X1, X2)) -> diff(active(X1), X2), p(mark(X)) -> mark(p(X)), p(ok(X)) -> ok(p(X)), s(mark(X)) -> mark(s(X)), s(ok(X)) -> ok(s(X)), leq(X1, mark(X2)) -> mark(leq(X1, X2)), leq(mark(X1), X2) -> mark(leq(X1, X2)), leq(ok(X1), ok(X2)) -> ok(leq(X1, X2)), if(mark(X1), X2, X3) -> mark(if(X1, X2, X3)), if(ok(X1), ok(X2), ok(X3)) -> ok(if(X1, X2, X3)), diff(X1, mark(X2)) -> mark(diff(X1, X2)), diff(mark(X1), X2) -> mark(diff(X1, X2)), diff(ok(X1), ok(X2)) -> ok(diff(X1, X2)), proper(0()) -> ok(0()), proper(p(X)) -> p(proper(X)), proper(s(X)) -> s(proper(X)), proper(true()) -> ok(true()), proper(leq(X1, X2)) -> leq(proper(X1), proper(X2)), proper(false()) -> ok(false()), proper(if(X1, X2, X3)) -> if(proper(X1), proper(X2), proper(X3)), proper(diff(X1, X2)) -> diff(proper(X1), proper(X2)), top(mark(X)) -> top(proper(X)), top(ok(X)) -> top(active(X))} SPSC: Simple Projection: pi(active#) = 0 Strict: { active#(p(X)) -> active#(X), active#(leq(X1, X2)) -> active#(X1), active#(leq(X1, X2)) -> active#(X2), active#(diff(X1, X2)) -> active#(X2)} EDG: {(active#(leq(X1, X2)) -> active#(X1), active#(diff(X1, X2)) -> active#(X2)) (active#(leq(X1, X2)) -> active#(X1), active#(leq(X1, X2)) -> active#(X2)) (active#(leq(X1, X2)) -> active#(X1), active#(leq(X1, X2)) -> active#(X1)) (active#(leq(X1, X2)) -> active#(X1), active#(p(X)) -> active#(X)) (active#(diff(X1, X2)) -> active#(X2), active#(diff(X1, X2)) -> active#(X2)) (active#(diff(X1, X2)) -> active#(X2), active#(leq(X1, X2)) -> active#(X2)) (active#(diff(X1, X2)) -> active#(X2), active#(leq(X1, X2)) -> active#(X1)) (active#(diff(X1, X2)) -> active#(X2), active#(p(X)) -> active#(X)) (active#(leq(X1, X2)) -> active#(X2), active#(p(X)) -> active#(X)) (active#(leq(X1, X2)) -> active#(X2), active#(leq(X1, X2)) -> active#(X1)) (active#(leq(X1, X2)) -> active#(X2), active#(leq(X1, X2)) -> active#(X2)) (active#(leq(X1, X2)) -> active#(X2), active#(diff(X1, X2)) -> active#(X2)) (active#(p(X)) -> active#(X), active#(p(X)) -> active#(X)) (active#(p(X)) -> active#(X), active#(leq(X1, X2)) -> active#(X1)) (active#(p(X)) -> active#(X), active#(leq(X1, X2)) -> active#(X2)) (active#(p(X)) -> active#(X), active#(diff(X1, X2)) -> active#(X2))} SCCS: Scc: { active#(p(X)) -> active#(X), active#(leq(X1, X2)) -> active#(X1), active#(leq(X1, X2)) -> active#(X2), active#(diff(X1, X2)) -> active#(X2)} SCC: Strict: { active#(p(X)) -> active#(X), active#(leq(X1, X2)) -> active#(X1), active#(leq(X1, X2)) -> active#(X2), active#(diff(X1, X2)) -> active#(X2)} Weak: { active(p(X)) -> p(active(X)), active(p(0())) -> mark(0()), active(p(s(X))) -> mark(X), active(s(X)) -> s(active(X)), active(leq(X1, X2)) -> leq(X1, active(X2)), active(leq(X1, X2)) -> leq(active(X1), X2), active(leq(0(), Y)) -> mark(true()), active(leq(s(X), 0())) -> mark(false()), active(leq(s(X), s(Y))) -> mark(leq(X, Y)), active(if(X1, X2, X3)) -> if(active(X1), X2, X3), active(if(true(), X, Y)) -> mark(X), active(if(false(), X, Y)) -> mark(Y), active(diff(X, Y)) -> mark(if(leq(X, Y), 0(), s(diff(p(X), Y)))), active(diff(X1, X2)) -> diff(X1, active(X2)), active(diff(X1, X2)) -> diff(active(X1), X2), p(mark(X)) -> mark(p(X)), p(ok(X)) -> ok(p(X)), s(mark(X)) -> mark(s(X)), s(ok(X)) -> ok(s(X)), leq(X1, mark(X2)) -> mark(leq(X1, X2)), leq(mark(X1), X2) -> mark(leq(X1, X2)), leq(ok(X1), ok(X2)) -> ok(leq(X1, X2)), if(mark(X1), X2, X3) -> mark(if(X1, X2, X3)), if(ok(X1), ok(X2), ok(X3)) -> ok(if(X1, X2, X3)), diff(X1, mark(X2)) -> mark(diff(X1, X2)), diff(mark(X1), X2) -> mark(diff(X1, X2)), diff(ok(X1), ok(X2)) -> ok(diff(X1, X2)), proper(0()) -> ok(0()), proper(p(X)) -> p(proper(X)), proper(s(X)) -> s(proper(X)), proper(true()) -> ok(true()), proper(leq(X1, X2)) -> leq(proper(X1), proper(X2)), proper(false()) -> ok(false()), proper(if(X1, X2, X3)) -> if(proper(X1), proper(X2), proper(X3)), proper(diff(X1, X2)) -> diff(proper(X1), proper(X2)), top(mark(X)) -> top(proper(X)), top(ok(X)) -> top(active(X))} SPSC: Simple Projection: pi(active#) = 0 Strict: { active#(p(X)) -> active#(X), active#(leq(X1, X2)) -> active#(X1), active#(diff(X1, X2)) -> active#(X2)} EDG: {(active#(leq(X1, X2)) -> active#(X1), active#(diff(X1, X2)) -> active#(X2)) (active#(leq(X1, X2)) -> active#(X1), active#(leq(X1, X2)) -> active#(X1)) (active#(leq(X1, X2)) -> active#(X1), active#(p(X)) -> active#(X)) (active#(p(X)) -> active#(X), active#(p(X)) -> active#(X)) (active#(p(X)) -> active#(X), active#(leq(X1, X2)) -> active#(X1)) (active#(p(X)) -> active#(X), active#(diff(X1, X2)) -> active#(X2)) (active#(diff(X1, X2)) -> active#(X2), active#(p(X)) -> active#(X)) (active#(diff(X1, X2)) -> active#(X2), active#(leq(X1, X2)) -> active#(X1)) (active#(diff(X1, X2)) -> active#(X2), active#(diff(X1, X2)) -> active#(X2))} SCCS: Scc: { active#(p(X)) -> active#(X), active#(leq(X1, X2)) -> active#(X1), active#(diff(X1, X2)) -> active#(X2)} SCC: Strict: { active#(p(X)) -> active#(X), active#(leq(X1, X2)) -> active#(X1), active#(diff(X1, X2)) -> active#(X2)} Weak: { active(p(X)) -> p(active(X)), active(p(0())) -> mark(0()), active(p(s(X))) -> mark(X), active(s(X)) -> s(active(X)), active(leq(X1, X2)) -> leq(X1, active(X2)), active(leq(X1, X2)) -> leq(active(X1), X2), active(leq(0(), Y)) -> mark(true()), active(leq(s(X), 0())) -> mark(false()), active(leq(s(X), s(Y))) -> mark(leq(X, Y)), active(if(X1, X2, X3)) -> if(active(X1), X2, X3), active(if(true(), X, Y)) -> mark(X), active(if(false(), X, Y)) -> mark(Y), active(diff(X, Y)) -> mark(if(leq(X, Y), 0(), s(diff(p(X), Y)))), active(diff(X1, X2)) -> diff(X1, active(X2)), active(diff(X1, X2)) -> diff(active(X1), X2), p(mark(X)) -> mark(p(X)), p(ok(X)) -> ok(p(X)), s(mark(X)) -> mark(s(X)), s(ok(X)) -> ok(s(X)), leq(X1, mark(X2)) -> mark(leq(X1, X2)), leq(mark(X1), X2) -> mark(leq(X1, X2)), leq(ok(X1), ok(X2)) -> ok(leq(X1, X2)), if(mark(X1), X2, X3) -> mark(if(X1, X2, X3)), if(ok(X1), ok(X2), ok(X3)) -> ok(if(X1, X2, X3)), diff(X1, mark(X2)) -> mark(diff(X1, X2)), diff(mark(X1), X2) -> mark(diff(X1, X2)), diff(ok(X1), ok(X2)) -> ok(diff(X1, X2)), proper(0()) -> ok(0()), proper(p(X)) -> p(proper(X)), proper(s(X)) -> s(proper(X)), proper(true()) -> ok(true()), proper(leq(X1, X2)) -> leq(proper(X1), proper(X2)), proper(false()) -> ok(false()), proper(if(X1, X2, X3)) -> if(proper(X1), proper(X2), proper(X3)), proper(diff(X1, X2)) -> diff(proper(X1), proper(X2)), top(mark(X)) -> top(proper(X)), top(ok(X)) -> top(active(X))} SPSC: Simple Projection: pi(active#) = 0 Strict: { active#(p(X)) -> active#(X), active#(diff(X1, X2)) -> active#(X2)} EDG: {(active#(diff(X1, X2)) -> active#(X2), active#(diff(X1, X2)) -> active#(X2)) (active#(diff(X1, X2)) -> active#(X2), active#(p(X)) -> active#(X)) (active#(p(X)) -> active#(X), active#(p(X)) -> active#(X)) (active#(p(X)) -> active#(X), active#(diff(X1, X2)) -> active#(X2))} SCCS: Scc: { active#(p(X)) -> active#(X), active#(diff(X1, X2)) -> active#(X2)} SCC: Strict: { active#(p(X)) -> active#(X), active#(diff(X1, X2)) -> active#(X2)} Weak: { active(p(X)) -> p(active(X)), active(p(0())) -> mark(0()), active(p(s(X))) -> mark(X), active(s(X)) -> s(active(X)), active(leq(X1, X2)) -> leq(X1, active(X2)), active(leq(X1, X2)) -> leq(active(X1), X2), active(leq(0(), Y)) -> mark(true()), active(leq(s(X), 0())) -> mark(false()), active(leq(s(X), s(Y))) -> mark(leq(X, Y)), active(if(X1, X2, X3)) -> if(active(X1), X2, X3), active(if(true(), X, Y)) -> mark(X), active(if(false(), X, Y)) -> mark(Y), active(diff(X, Y)) -> mark(if(leq(X, Y), 0(), s(diff(p(X), Y)))), active(diff(X1, X2)) -> diff(X1, active(X2)), active(diff(X1, X2)) -> diff(active(X1), X2), p(mark(X)) -> mark(p(X)), p(ok(X)) -> ok(p(X)), s(mark(X)) -> mark(s(X)), s(ok(X)) -> ok(s(X)), leq(X1, mark(X2)) -> mark(leq(X1, X2)), leq(mark(X1), X2) -> mark(leq(X1, X2)), leq(ok(X1), ok(X2)) -> ok(leq(X1, X2)), if(mark(X1), X2, X3) -> mark(if(X1, X2, X3)), if(ok(X1), ok(X2), ok(X3)) -> ok(if(X1, X2, X3)), diff(X1, mark(X2)) -> mark(diff(X1, X2)), diff(mark(X1), X2) -> mark(diff(X1, X2)), diff(ok(X1), ok(X2)) -> ok(diff(X1, X2)), proper(0()) -> ok(0()), proper(p(X)) -> p(proper(X)), proper(s(X)) -> s(proper(X)), proper(true()) -> ok(true()), proper(leq(X1, X2)) -> leq(proper(X1), proper(X2)), proper(false()) -> ok(false()), proper(if(X1, X2, X3)) -> if(proper(X1), proper(X2), proper(X3)), proper(diff(X1, X2)) -> diff(proper(X1), proper(X2)), top(mark(X)) -> top(proper(X)), top(ok(X)) -> top(active(X))} SPSC: Simple Projection: pi(active#) = 0 Strict: {active#(diff(X1, X2)) -> active#(X2)} EDG: {(active#(diff(X1, X2)) -> active#(X2), active#(diff(X1, X2)) -> active#(X2))} SCCS: Scc: {active#(diff(X1, X2)) -> active#(X2)} SCC: Strict: {active#(diff(X1, X2)) -> active#(X2)} Weak: { active(p(X)) -> p(active(X)), active(p(0())) -> mark(0()), active(p(s(X))) -> mark(X), active(s(X)) -> s(active(X)), active(leq(X1, X2)) -> leq(X1, active(X2)), active(leq(X1, X2)) -> leq(active(X1), X2), active(leq(0(), Y)) -> mark(true()), active(leq(s(X), 0())) -> mark(false()), active(leq(s(X), s(Y))) -> mark(leq(X, Y)), active(if(X1, X2, X3)) -> if(active(X1), X2, X3), active(if(true(), X, Y)) -> mark(X), active(if(false(), X, Y)) -> mark(Y), active(diff(X, Y)) -> mark(if(leq(X, Y), 0(), s(diff(p(X), Y)))), active(diff(X1, X2)) -> diff(X1, active(X2)), active(diff(X1, X2)) -> diff(active(X1), X2), p(mark(X)) -> mark(p(X)), p(ok(X)) -> ok(p(X)), s(mark(X)) -> mark(s(X)), s(ok(X)) -> ok(s(X)), leq(X1, mark(X2)) -> mark(leq(X1, X2)), leq(mark(X1), X2) -> mark(leq(X1, X2)), leq(ok(X1), ok(X2)) -> ok(leq(X1, X2)), if(mark(X1), X2, X3) -> mark(if(X1, X2, X3)), if(ok(X1), ok(X2), ok(X3)) -> ok(if(X1, X2, X3)), diff(X1, mark(X2)) -> mark(diff(X1, X2)), diff(mark(X1), X2) -> mark(diff(X1, X2)), diff(ok(X1), ok(X2)) -> ok(diff(X1, X2)), proper(0()) -> ok(0()), proper(p(X)) -> p(proper(X)), proper(s(X)) -> s(proper(X)), proper(true()) -> ok(true()), proper(leq(X1, X2)) -> leq(proper(X1), proper(X2)), proper(false()) -> ok(false()), proper(if(X1, X2, X3)) -> if(proper(X1), proper(X2), proper(X3)), proper(diff(X1, X2)) -> diff(proper(X1), proper(X2)), top(mark(X)) -> top(proper(X)), top(ok(X)) -> top(active(X))} SPSC: Simple Projection: pi(active#) = 0 Strict: {} Qed