MAYBE TRS: { mark(0()) -> active(0()), mark(p(X)) -> active(p(mark(X))), mark(s(X)) -> active(s(mark(X))), mark(true()) -> active(true()), mark(leq(X1, X2)) -> active(leq(mark(X1), mark(X2))), mark(false()) -> active(false()), mark(if(X1, X2, X3)) -> active(if(mark(X1), X2, X3)), mark(diff(X1, X2)) -> active(diff(mark(X1), mark(X2))), active(p(0())) -> mark(0()), active(p(s(X))) -> mark(X), 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(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)))), p(mark(X)) -> p(X), p(active(X)) -> p(X), s(mark(X)) -> s(X), s(active(X)) -> s(X), leq(X1, mark(X2)) -> leq(X1, X2), leq(X1, active(X2)) -> leq(X1, X2), leq(mark(X1), X2) -> leq(X1, X2), leq(active(X1), X2) -> leq(X1, X2), if(X1, X2, mark(X3)) -> if(X1, X2, X3), if(X1, X2, active(X3)) -> if(X1, X2, X3), if(X1, mark(X2), X3) -> if(X1, X2, X3), if(X1, active(X2), X3) -> if(X1, X2, X3), if(mark(X1), X2, X3) -> if(X1, X2, X3), if(active(X1), X2, X3) -> if(X1, X2, X3), diff(X1, mark(X2)) -> diff(X1, X2), diff(X1, active(X2)) -> diff(X1, X2), diff(mark(X1), X2) -> diff(X1, X2), diff(active(X1), X2) -> diff(X1, X2)} DP: Strict: { mark#(0()) -> active#(0()), mark#(p(X)) -> mark#(X), mark#(p(X)) -> active#(p(mark(X))), mark#(p(X)) -> p#(mark(X)), mark#(s(X)) -> mark#(X), mark#(s(X)) -> active#(s(mark(X))), mark#(s(X)) -> s#(mark(X)), mark#(true()) -> active#(true()), mark#(leq(X1, X2)) -> mark#(X1), mark#(leq(X1, X2)) -> mark#(X2), mark#(leq(X1, X2)) -> active#(leq(mark(X1), mark(X2))), mark#(leq(X1, X2)) -> leq#(mark(X1), mark(X2)), mark#(false()) -> active#(false()), mark#(if(X1, X2, X3)) -> mark#(X1), mark#(if(X1, X2, X3)) -> active#(if(mark(X1), X2, X3)), mark#(if(X1, X2, X3)) -> if#(mark(X1), X2, X3), mark#(diff(X1, X2)) -> mark#(X1), mark#(diff(X1, X2)) -> mark#(X2), mark#(diff(X1, X2)) -> active#(diff(mark(X1), mark(X2))), mark#(diff(X1, X2)) -> diff#(mark(X1), mark(X2)), active#(p(0())) -> mark#(0()), active#(p(s(X))) -> mark#(X), active#(leq(0(), Y)) -> mark#(true()), active#(leq(s(X), 0())) -> mark#(false()), active#(leq(s(X), s(Y))) -> mark#(leq(X, Y)), active#(leq(s(X), s(Y))) -> leq#(X, Y), 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(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), p#(mark(X)) -> p#(X), p#(active(X)) -> p#(X), s#(mark(X)) -> s#(X), s#(active(X)) -> s#(X), leq#(X1, mark(X2)) -> leq#(X1, X2), leq#(X1, active(X2)) -> leq#(X1, X2), leq#(mark(X1), X2) -> leq#(X1, X2), leq#(active(X1), X2) -> leq#(X1, X2), if#(X1, X2, mark(X3)) -> if#(X1, X2, X3), if#(X1, X2, active(X3)) -> if#(X1, X2, X3), if#(X1, mark(X2), X3) -> if#(X1, X2, X3), if#(X1, active(X2), X3) -> if#(X1, X2, X3), if#(mark(X1), X2, X3) -> if#(X1, X2, X3), if#(active(X1), X2, X3) -> if#(X1, X2, X3), diff#(X1, mark(X2)) -> diff#(X1, X2), diff#(X1, active(X2)) -> diff#(X1, X2), diff#(mark(X1), X2) -> diff#(X1, X2), diff#(active(X1), X2) -> diff#(X1, X2)} Weak: { mark(0()) -> active(0()), mark(p(X)) -> active(p(mark(X))), mark(s(X)) -> active(s(mark(X))), mark(true()) -> active(true()), mark(leq(X1, X2)) -> active(leq(mark(X1), mark(X2))), mark(false()) -> active(false()), mark(if(X1, X2, X3)) -> active(if(mark(X1), X2, X3)), mark(diff(X1, X2)) -> active(diff(mark(X1), mark(X2))), active(p(0())) -> mark(0()), active(p(s(X))) -> mark(X), 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(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)))), p(mark(X)) -> p(X), p(active(X)) -> p(X), s(mark(X)) -> s(X), s(active(X)) -> s(X), leq(X1, mark(X2)) -> leq(X1, X2), leq(X1, active(X2)) -> leq(X1, X2), leq(mark(X1), X2) -> leq(X1, X2), leq(active(X1), X2) -> leq(X1, X2), if(X1, X2, mark(X3)) -> if(X1, X2, X3), if(X1, X2, active(X3)) -> if(X1, X2, X3), if(X1, mark(X2), X3) -> if(X1, X2, X3), if(X1, active(X2), X3) -> if(X1, X2, X3), if(mark(X1), X2, X3) -> if(X1, X2, X3), if(active(X1), X2, X3) -> if(X1, X2, X3), diff(X1, mark(X2)) -> diff(X1, X2), diff(X1, active(X2)) -> diff(X1, X2), diff(mark(X1), X2) -> diff(X1, X2), diff(active(X1), X2) -> diff(X1, X2)} EDG: { (active#(diff(X, Y)) -> if#(leq(X, Y), 0(), s(diff(p(X), Y))), if#(active(X1), X2, X3) -> if#(X1, X2, X3)) (active#(diff(X, Y)) -> if#(leq(X, Y), 0(), s(diff(p(X), Y))), if#(mark(X1), X2, X3) -> if#(X1, X2, X3)) (active#(diff(X, Y)) -> if#(leq(X, Y), 0(), s(diff(p(X), Y))), if#(X1, X2, active(X3)) -> if#(X1, X2, X3)) (active#(diff(X, Y)) -> if#(leq(X, Y), 0(), s(diff(p(X), Y))), if#(X1, X2, mark(X3)) -> if#(X1, X2, X3)) (mark#(p(X)) -> active#(p(mark(X))), active#(diff(X, Y)) -> diff#(p(X), Y)) (mark#(p(X)) -> active#(p(mark(X))), active#(diff(X, Y)) -> if#(leq(X, Y), 0(), s(diff(p(X), Y)))) (mark#(p(X)) -> active#(p(mark(X))), active#(diff(X, Y)) -> leq#(X, Y)) (mark#(p(X)) -> active#(p(mark(X))), active#(diff(X, Y)) -> s#(diff(p(X), Y))) (mark#(p(X)) -> active#(p(mark(X))), active#(diff(X, Y)) -> p#(X)) (mark#(p(X)) -> active#(p(mark(X))), active#(diff(X, Y)) -> mark#(if(leq(X, Y), 0(), s(diff(p(X), Y))))) (mark#(p(X)) -> active#(p(mark(X))), active#(if(false(), X, Y)) -> mark#(Y)) (mark#(p(X)) -> active#(p(mark(X))), active#(if(true(), X, Y)) -> mark#(X)) (mark#(p(X)) -> active#(p(mark(X))), active#(leq(s(X), s(Y))) -> leq#(X, Y)) (mark#(p(X)) -> active#(p(mark(X))), active#(leq(s(X), s(Y))) -> mark#(leq(X, Y))) (mark#(p(X)) -> active#(p(mark(X))), active#(leq(s(X), 0())) -> mark#(false())) (mark#(p(X)) -> active#(p(mark(X))), active#(leq(0(), Y)) -> mark#(true())) (mark#(p(X)) -> active#(p(mark(X))), active#(p(s(X))) -> mark#(X)) (mark#(p(X)) -> active#(p(mark(X))), active#(p(0())) -> mark#(0())) (active#(leq(s(X), s(Y))) -> leq#(X, Y), leq#(active(X1), 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, active(X2)) -> leq#(X1, X2)) (active#(leq(s(X), s(Y))) -> leq#(X, Y), leq#(X1, mark(X2)) -> leq#(X1, X2)) (leq#(X1, mark(X2)) -> leq#(X1, X2), leq#(active(X1), 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, active(X2)) -> leq#(X1, X2)) (leq#(X1, mark(X2)) -> leq#(X1, X2), leq#(X1, mark(X2)) -> leq#(X1, X2)) (leq#(mark(X1), X2) -> leq#(X1, X2), leq#(active(X1), 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#(X1, active(X2)) -> leq#(X1, X2)) (leq#(mark(X1), X2) -> leq#(X1, X2), leq#(X1, mark(X2)) -> leq#(X1, X2)) (diff#(X1, mark(X2)) -> diff#(X1, X2), diff#(active(X1), 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#(X1, active(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#(active(X1), 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, active(X2)) -> diff#(X1, X2)) (diff#(mark(X1), X2) -> diff#(X1, X2), diff#(X1, mark(X2)) -> diff#(X1, X2)) (mark#(p(X)) -> mark#(X), mark#(diff(X1, X2)) -> diff#(mark(X1), mark(X2))) (mark#(p(X)) -> mark#(X), mark#(diff(X1, X2)) -> active#(diff(mark(X1), mark(X2)))) (mark#(p(X)) -> mark#(X), mark#(diff(X1, X2)) -> mark#(X2)) (mark#(p(X)) -> mark#(X), mark#(diff(X1, X2)) -> mark#(X1)) (mark#(p(X)) -> mark#(X), mark#(if(X1, X2, X3)) -> if#(mark(X1), X2, X3)) (mark#(p(X)) -> mark#(X), mark#(if(X1, X2, X3)) -> active#(if(mark(X1), X2, X3))) (mark#(p(X)) -> mark#(X), mark#(if(X1, X2, X3)) -> mark#(X1)) (mark#(p(X)) -> mark#(X), mark#(false()) -> active#(false())) (mark#(p(X)) -> mark#(X), mark#(leq(X1, X2)) -> leq#(mark(X1), mark(X2))) (mark#(p(X)) -> mark#(X), mark#(leq(X1, X2)) -> active#(leq(mark(X1), mark(X2)))) (mark#(p(X)) -> mark#(X), mark#(leq(X1, X2)) -> mark#(X2)) (mark#(p(X)) -> mark#(X), mark#(leq(X1, X2)) -> mark#(X1)) (mark#(p(X)) -> mark#(X), mark#(true()) -> active#(true())) (mark#(p(X)) -> mark#(X), mark#(s(X)) -> s#(mark(X))) (mark#(p(X)) -> mark#(X), mark#(s(X)) -> active#(s(mark(X)))) (mark#(p(X)) -> mark#(X), mark#(s(X)) -> mark#(X)) (mark#(p(X)) -> mark#(X), mark#(p(X)) -> p#(mark(X))) (mark#(p(X)) -> mark#(X), mark#(p(X)) -> active#(p(mark(X)))) (mark#(p(X)) -> mark#(X), mark#(p(X)) -> mark#(X)) (mark#(p(X)) -> mark#(X), mark#(0()) -> active#(0())) (active#(p(s(X))) -> mark#(X), mark#(diff(X1, X2)) -> diff#(mark(X1), mark(X2))) (active#(p(s(X))) -> mark#(X), mark#(diff(X1, X2)) -> active#(diff(mark(X1), mark(X2)))) (active#(p(s(X))) -> mark#(X), mark#(diff(X1, X2)) -> mark#(X2)) (active#(p(s(X))) -> mark#(X), mark#(diff(X1, X2)) -> mark#(X1)) (active#(p(s(X))) -> mark#(X), mark#(if(X1, X2, X3)) -> if#(mark(X1), X2, X3)) (active#(p(s(X))) -> mark#(X), mark#(if(X1, X2, X3)) -> active#(if(mark(X1), X2, X3))) (active#(p(s(X))) -> mark#(X), mark#(if(X1, X2, X3)) -> mark#(X1)) (active#(p(s(X))) -> mark#(X), mark#(false()) -> active#(false())) (active#(p(s(X))) -> mark#(X), mark#(leq(X1, X2)) -> leq#(mark(X1), mark(X2))) (active#(p(s(X))) -> mark#(X), mark#(leq(X1, X2)) -> active#(leq(mark(X1), mark(X2)))) (active#(p(s(X))) -> mark#(X), mark#(leq(X1, X2)) -> mark#(X2)) (active#(p(s(X))) -> mark#(X), mark#(leq(X1, X2)) -> mark#(X1)) (active#(p(s(X))) -> mark#(X), mark#(true()) -> active#(true())) (active#(p(s(X))) -> mark#(X), mark#(s(X)) -> s#(mark(X))) (active#(p(s(X))) -> mark#(X), mark#(s(X)) -> active#(s(mark(X)))) (active#(p(s(X))) -> mark#(X), mark#(s(X)) -> mark#(X)) (active#(p(s(X))) -> mark#(X), mark#(p(X)) -> p#(mark(X))) (active#(p(s(X))) -> mark#(X), mark#(p(X)) -> active#(p(mark(X)))) (active#(p(s(X))) -> mark#(X), mark#(p(X)) -> mark#(X)) (active#(p(s(X))) -> mark#(X), mark#(0()) -> active#(0())) (active#(diff(X, Y)) -> mark#(if(leq(X, Y), 0(), s(diff(p(X), Y)))), mark#(diff(X1, X2)) -> diff#(mark(X1), mark(X2))) (active#(diff(X, Y)) -> mark#(if(leq(X, Y), 0(), s(diff(p(X), Y)))), mark#(diff(X1, X2)) -> active#(diff(mark(X1), mark(X2)))) (active#(diff(X, Y)) -> mark#(if(leq(X, Y), 0(), s(diff(p(X), Y)))), mark#(diff(X1, X2)) -> mark#(X2)) (active#(diff(X, Y)) -> mark#(if(leq(X, Y), 0(), s(diff(p(X), Y)))), mark#(diff(X1, X2)) -> mark#(X1)) (active#(diff(X, Y)) -> mark#(if(leq(X, Y), 0(), s(diff(p(X), Y)))), mark#(if(X1, X2, X3)) -> if#(mark(X1), X2, X3)) (active#(diff(X, Y)) -> mark#(if(leq(X, Y), 0(), s(diff(p(X), Y)))), mark#(if(X1, X2, X3)) -> active#(if(mark(X1), X2, X3))) (active#(diff(X, Y)) -> mark#(if(leq(X, Y), 0(), s(diff(p(X), Y)))), mark#(if(X1, X2, X3)) -> mark#(X1)) (active#(diff(X, Y)) -> mark#(if(leq(X, Y), 0(), s(diff(p(X), Y)))), mark#(leq(X1, X2)) -> leq#(mark(X1), mark(X2))) (active#(diff(X, Y)) -> mark#(if(leq(X, Y), 0(), s(diff(p(X), Y)))), mark#(leq(X1, X2)) -> active#(leq(mark(X1), mark(X2)))) (active#(diff(X, Y)) -> mark#(if(leq(X, Y), 0(), s(diff(p(X), Y)))), mark#(leq(X1, X2)) -> mark#(X2)) (active#(diff(X, Y)) -> mark#(if(leq(X, Y), 0(), s(diff(p(X), Y)))), mark#(leq(X1, X2)) -> mark#(X1)) (active#(diff(X, Y)) -> mark#(if(leq(X, Y), 0(), s(diff(p(X), Y)))), mark#(s(X)) -> s#(mark(X))) (active#(diff(X, Y)) -> mark#(if(leq(X, Y), 0(), s(diff(p(X), Y)))), mark#(s(X)) -> active#(s(mark(X)))) (active#(diff(X, Y)) -> mark#(if(leq(X, Y), 0(), s(diff(p(X), Y)))), mark#(s(X)) -> mark#(X)) (active#(diff(X, Y)) -> mark#(if(leq(X, Y), 0(), s(diff(p(X), Y)))), mark#(p(X)) -> p#(mark(X))) (active#(diff(X, Y)) -> mark#(if(leq(X, Y), 0(), s(diff(p(X), Y)))), mark#(p(X)) -> active#(p(mark(X)))) (active#(diff(X, Y)) -> mark#(if(leq(X, Y), 0(), s(diff(p(X), Y)))), mark#(p(X)) -> mark#(X)) (p#(mark(X)) -> p#(X), p#(active(X)) -> p#(X)) (p#(mark(X)) -> p#(X), p#(mark(X)) -> p#(X)) (s#(mark(X)) -> s#(X), s#(active(X)) -> s#(X)) (s#(mark(X)) -> s#(X), s#(mark(X)) -> s#(X)) (active#(leq(s(X), s(Y))) -> mark#(leq(X, Y)), mark#(diff(X1, X2)) -> diff#(mark(X1), mark(X2))) (active#(leq(s(X), s(Y))) -> mark#(leq(X, Y)), mark#(diff(X1, X2)) -> active#(diff(mark(X1), mark(X2)))) (active#(leq(s(X), s(Y))) -> mark#(leq(X, Y)), mark#(diff(X1, X2)) -> mark#(X2)) (active#(leq(s(X), s(Y))) -> mark#(leq(X, Y)), mark#(diff(X1, X2)) -> mark#(X1)) (active#(leq(s(X), s(Y))) -> mark#(leq(X, Y)), mark#(if(X1, X2, X3)) -> if#(mark(X1), X2, X3)) (active#(leq(s(X), s(Y))) -> mark#(leq(X, Y)), mark#(if(X1, X2, X3)) -> active#(if(mark(X1), X2, X3))) (active#(leq(s(X), s(Y))) -> mark#(leq(X, Y)), mark#(if(X1, X2, X3)) -> mark#(X1)) (active#(leq(s(X), s(Y))) -> mark#(leq(X, Y)), mark#(leq(X1, X2)) -> leq#(mark(X1), mark(X2))) (active#(leq(s(X), s(Y))) -> mark#(leq(X, Y)), mark#(leq(X1, X2)) -> active#(leq(mark(X1), mark(X2)))) (active#(leq(s(X), s(Y))) -> mark#(leq(X, Y)), mark#(leq(X1, X2)) -> mark#(X2)) (active#(leq(s(X), s(Y))) -> mark#(leq(X, Y)), mark#(leq(X1, X2)) -> mark#(X1)) (active#(leq(s(X), s(Y))) -> mark#(leq(X, Y)), mark#(s(X)) -> s#(mark(X))) (active#(leq(s(X), s(Y))) -> mark#(leq(X, Y)), mark#(s(X)) -> active#(s(mark(X)))) (active#(leq(s(X), s(Y))) -> mark#(leq(X, Y)), mark#(s(X)) -> mark#(X)) (active#(leq(s(X), s(Y))) -> mark#(leq(X, Y)), mark#(p(X)) -> p#(mark(X))) (active#(leq(s(X), s(Y))) -> mark#(leq(X, Y)), mark#(p(X)) -> active#(p(mark(X)))) (active#(leq(s(X), s(Y))) -> mark#(leq(X, Y)), mark#(p(X)) -> mark#(X)) (mark#(leq(X1, X2)) -> leq#(mark(X1), mark(X2)), leq#(active(X1), X2) -> leq#(X1, X2)) (mark#(leq(X1, X2)) -> leq#(mark(X1), mark(X2)), leq#(mark(X1), X2) -> leq#(X1, X2)) (mark#(leq(X1, X2)) -> leq#(mark(X1), mark(X2)), leq#(X1, active(X2)) -> leq#(X1, X2)) (mark#(leq(X1, X2)) -> leq#(mark(X1), mark(X2)), leq#(X1, mark(X2)) -> leq#(X1, X2)) (mark#(if(X1, X2, X3)) -> active#(if(mark(X1), X2, X3)), active#(diff(X, Y)) -> diff#(p(X), Y)) (mark#(if(X1, X2, X3)) -> active#(if(mark(X1), X2, X3)), active#(diff(X, Y)) -> if#(leq(X, Y), 0(), s(diff(p(X), Y)))) (mark#(if(X1, X2, X3)) -> active#(if(mark(X1), X2, X3)), active#(diff(X, Y)) -> leq#(X, Y)) (mark#(if(X1, X2, X3)) -> active#(if(mark(X1), X2, X3)), active#(diff(X, Y)) -> s#(diff(p(X), Y))) (mark#(if(X1, X2, X3)) -> active#(if(mark(X1), X2, X3)), active#(diff(X, Y)) -> p#(X)) (mark#(if(X1, X2, X3)) -> active#(if(mark(X1), X2, X3)), active#(diff(X, Y)) -> mark#(if(leq(X, Y), 0(), s(diff(p(X), Y))))) (mark#(if(X1, X2, X3)) -> active#(if(mark(X1), X2, X3)), active#(if(false(), X, Y)) -> mark#(Y)) (mark#(if(X1, X2, X3)) -> active#(if(mark(X1), X2, X3)), active#(if(true(), X, Y)) -> mark#(X)) (mark#(if(X1, X2, X3)) -> active#(if(mark(X1), X2, X3)), active#(leq(s(X), s(Y))) -> leq#(X, Y)) (mark#(if(X1, X2, X3)) -> active#(if(mark(X1), X2, X3)), active#(leq(s(X), s(Y))) -> mark#(leq(X, Y))) (mark#(if(X1, X2, X3)) -> active#(if(mark(X1), X2, X3)), active#(leq(s(X), 0())) -> mark#(false())) (mark#(if(X1, X2, X3)) -> active#(if(mark(X1), X2, X3)), active#(leq(0(), Y)) -> mark#(true())) (mark#(if(X1, X2, X3)) -> active#(if(mark(X1), X2, X3)), active#(p(s(X))) -> mark#(X)) (mark#(if(X1, X2, X3)) -> active#(if(mark(X1), X2, X3)), active#(p(0())) -> mark#(0())) (active#(p(0())) -> mark#(0()), mark#(0()) -> active#(0())) (active#(leq(s(X), 0())) -> mark#(false()), mark#(false()) -> active#(false())) (mark#(diff(X1, X2)) -> mark#(X2), mark#(diff(X1, X2)) -> diff#(mark(X1), mark(X2))) (mark#(diff(X1, X2)) -> mark#(X2), mark#(diff(X1, X2)) -> active#(diff(mark(X1), mark(X2)))) (mark#(diff(X1, X2)) -> mark#(X2), mark#(diff(X1, X2)) -> mark#(X2)) (mark#(diff(X1, X2)) -> mark#(X2), mark#(diff(X1, X2)) -> mark#(X1)) (mark#(diff(X1, X2)) -> mark#(X2), mark#(if(X1, X2, X3)) -> if#(mark(X1), X2, X3)) (mark#(diff(X1, X2)) -> mark#(X2), mark#(if(X1, X2, X3)) -> active#(if(mark(X1), X2, X3))) (mark#(diff(X1, X2)) -> mark#(X2), mark#(if(X1, X2, X3)) -> mark#(X1)) (mark#(diff(X1, X2)) -> mark#(X2), mark#(false()) -> active#(false())) (mark#(diff(X1, X2)) -> mark#(X2), mark#(leq(X1, X2)) -> leq#(mark(X1), mark(X2))) (mark#(diff(X1, X2)) -> mark#(X2), mark#(leq(X1, X2)) -> active#(leq(mark(X1), mark(X2)))) (mark#(diff(X1, X2)) -> mark#(X2), mark#(leq(X1, X2)) -> mark#(X2)) (mark#(diff(X1, X2)) -> mark#(X2), mark#(leq(X1, X2)) -> mark#(X1)) (mark#(diff(X1, X2)) -> mark#(X2), mark#(true()) -> active#(true())) (mark#(diff(X1, X2)) -> mark#(X2), mark#(s(X)) -> s#(mark(X))) (mark#(diff(X1, X2)) -> mark#(X2), mark#(s(X)) -> active#(s(mark(X)))) (mark#(diff(X1, X2)) -> mark#(X2), mark#(s(X)) -> mark#(X)) (mark#(diff(X1, X2)) -> mark#(X2), mark#(p(X)) -> p#(mark(X))) (mark#(diff(X1, X2)) -> mark#(X2), mark#(p(X)) -> active#(p(mark(X)))) (mark#(diff(X1, X2)) -> mark#(X2), mark#(p(X)) -> mark#(X)) (mark#(diff(X1, X2)) -> mark#(X2), mark#(0()) -> active#(0())) (mark#(if(X1, X2, X3)) -> mark#(X1), mark#(diff(X1, X2)) -> diff#(mark(X1), mark(X2))) (mark#(if(X1, X2, X3)) -> mark#(X1), mark#(diff(X1, X2)) -> active#(diff(mark(X1), mark(X2)))) (mark#(if(X1, X2, X3)) -> mark#(X1), mark#(diff(X1, X2)) -> mark#(X2)) (mark#(if(X1, X2, X3)) -> mark#(X1), mark#(diff(X1, X2)) -> mark#(X1)) (mark#(if(X1, X2, X3)) -> mark#(X1), mark#(if(X1, X2, X3)) -> if#(mark(X1), X2, X3)) (mark#(if(X1, X2, X3)) -> mark#(X1), mark#(if(X1, X2, X3)) -> active#(if(mark(X1), X2, X3))) (mark#(if(X1, X2, X3)) -> mark#(X1), mark#(if(X1, X2, X3)) -> mark#(X1)) (mark#(if(X1, X2, X3)) -> mark#(X1), mark#(false()) -> active#(false())) (mark#(if(X1, X2, X3)) -> mark#(X1), mark#(leq(X1, X2)) -> leq#(mark(X1), mark(X2))) (mark#(if(X1, X2, X3)) -> mark#(X1), mark#(leq(X1, X2)) -> active#(leq(mark(X1), mark(X2)))) (mark#(if(X1, X2, X3)) -> mark#(X1), mark#(leq(X1, X2)) -> mark#(X2)) (mark#(if(X1, X2, X3)) -> mark#(X1), mark#(leq(X1, X2)) -> mark#(X1)) (mark#(if(X1, X2, X3)) -> mark#(X1), mark#(true()) -> active#(true())) (mark#(if(X1, X2, X3)) -> mark#(X1), mark#(s(X)) -> s#(mark(X))) (mark#(if(X1, X2, X3)) -> mark#(X1), mark#(s(X)) -> active#(s(mark(X)))) (mark#(if(X1, X2, X3)) -> mark#(X1), mark#(s(X)) -> mark#(X)) (mark#(if(X1, X2, X3)) -> mark#(X1), mark#(p(X)) -> p#(mark(X))) (mark#(if(X1, X2, X3)) -> mark#(X1), mark#(p(X)) -> active#(p(mark(X)))) (mark#(if(X1, X2, X3)) -> mark#(X1), mark#(p(X)) -> mark#(X)) (mark#(if(X1, X2, X3)) -> mark#(X1), mark#(0()) -> active#(0())) (mark#(leq(X1, X2)) -> active#(leq(mark(X1), mark(X2))), active#(diff(X, Y)) -> diff#(p(X), Y)) (mark#(leq(X1, X2)) -> active#(leq(mark(X1), mark(X2))), active#(diff(X, Y)) -> if#(leq(X, Y), 0(), s(diff(p(X), Y)))) (mark#(leq(X1, X2)) -> active#(leq(mark(X1), mark(X2))), active#(diff(X, Y)) -> leq#(X, Y)) (mark#(leq(X1, X2)) -> active#(leq(mark(X1), mark(X2))), active#(diff(X, Y)) -> s#(diff(p(X), Y))) (mark#(leq(X1, X2)) -> active#(leq(mark(X1), mark(X2))), active#(diff(X, Y)) -> p#(X)) (mark#(leq(X1, X2)) -> active#(leq(mark(X1), mark(X2))), active#(diff(X, Y)) -> mark#(if(leq(X, Y), 0(), s(diff(p(X), Y))))) (mark#(leq(X1, X2)) -> active#(leq(mark(X1), mark(X2))), active#(if(false(), X, Y)) -> mark#(Y)) (mark#(leq(X1, X2)) -> active#(leq(mark(X1), mark(X2))), active#(if(true(), X, Y)) -> mark#(X)) (mark#(leq(X1, X2)) -> active#(leq(mark(X1), mark(X2))), active#(leq(s(X), s(Y))) -> leq#(X, Y)) (mark#(leq(X1, X2)) -> active#(leq(mark(X1), mark(X2))), active#(leq(s(X), s(Y))) -> mark#(leq(X, Y))) (mark#(leq(X1, X2)) -> active#(leq(mark(X1), mark(X2))), active#(leq(s(X), 0())) -> mark#(false())) (mark#(leq(X1, X2)) -> active#(leq(mark(X1), mark(X2))), active#(leq(0(), Y)) -> mark#(true())) (mark#(leq(X1, X2)) -> active#(leq(mark(X1), mark(X2))), active#(p(s(X))) -> mark#(X)) (mark#(leq(X1, X2)) -> active#(leq(mark(X1), mark(X2))), active#(p(0())) -> mark#(0())) (mark#(if(X1, X2, X3)) -> if#(mark(X1), X2, X3), if#(active(X1), X2, X3) -> if#(X1, X2, X3)) (mark#(if(X1, X2, X3)) -> if#(mark(X1), X2, X3), if#(mark(X1), X2, X3) -> if#(X1, X2, X3)) (mark#(if(X1, X2, X3)) -> if#(mark(X1), X2, X3), if#(X1, active(X2), X3) -> if#(X1, X2, X3)) (mark#(if(X1, X2, X3)) -> if#(mark(X1), X2, X3), if#(X1, mark(X2), X3) -> if#(X1, X2, X3)) (mark#(if(X1, X2, X3)) -> if#(mark(X1), X2, X3), if#(X1, X2, active(X3)) -> if#(X1, X2, X3)) (mark#(if(X1, X2, X3)) -> if#(mark(X1), X2, X3), if#(X1, X2, mark(X3)) -> if#(X1, X2, X3)) (if#(X1, X2, active(X3)) -> if#(X1, X2, X3), if#(active(X1), X2, X3) -> if#(X1, X2, X3)) (if#(X1, X2, active(X3)) -> if#(X1, X2, X3), if#(mark(X1), X2, X3) -> if#(X1, X2, X3)) (if#(X1, X2, active(X3)) -> if#(X1, X2, X3), if#(X1, active(X2), X3) -> if#(X1, X2, X3)) (if#(X1, X2, active(X3)) -> if#(X1, X2, X3), if#(X1, mark(X2), X3) -> if#(X1, X2, X3)) (if#(X1, X2, active(X3)) -> if#(X1, X2, X3), if#(X1, X2, active(X3)) -> if#(X1, X2, X3)) (if#(X1, X2, active(X3)) -> if#(X1, X2, X3), if#(X1, X2, mark(X3)) -> if#(X1, X2, X3)) (if#(X1, active(X2), X3) -> if#(X1, X2, X3), if#(active(X1), X2, X3) -> if#(X1, X2, X3)) (if#(X1, active(X2), X3) -> if#(X1, X2, X3), if#(mark(X1), X2, X3) -> if#(X1, X2, X3)) (if#(X1, active(X2), X3) -> if#(X1, X2, X3), if#(X1, active(X2), X3) -> if#(X1, X2, X3)) (if#(X1, active(X2), X3) -> if#(X1, X2, X3), if#(X1, mark(X2), X3) -> if#(X1, X2, X3)) (if#(X1, active(X2), X3) -> if#(X1, X2, X3), if#(X1, X2, active(X3)) -> if#(X1, X2, X3)) (if#(X1, active(X2), X3) -> if#(X1, X2, X3), if#(X1, X2, mark(X3)) -> if#(X1, X2, X3)) (if#(active(X1), X2, X3) -> if#(X1, X2, X3), if#(active(X1), X2, X3) -> if#(X1, X2, X3)) (if#(active(X1), X2, X3) -> if#(X1, X2, X3), if#(mark(X1), X2, X3) -> if#(X1, X2, X3)) (if#(active(X1), X2, X3) -> if#(X1, X2, X3), if#(X1, active(X2), X3) -> if#(X1, X2, X3)) (if#(active(X1), X2, X3) -> if#(X1, X2, X3), if#(X1, mark(X2), X3) -> if#(X1, X2, X3)) (if#(active(X1), X2, X3) -> if#(X1, X2, X3), if#(X1, X2, active(X3)) -> if#(X1, X2, X3)) (if#(active(X1), X2, X3) -> if#(X1, X2, X3), if#(X1, X2, mark(X3)) -> if#(X1, X2, X3)) (mark#(s(X)) -> s#(mark(X)), s#(active(X)) -> s#(X)) (mark#(s(X)) -> s#(mark(X)), s#(mark(X)) -> s#(X)) (mark#(p(X)) -> p#(mark(X)), p#(mark(X)) -> p#(X)) (mark#(p(X)) -> p#(mark(X)), p#(active(X)) -> p#(X)) (if#(mark(X1), X2, X3) -> if#(X1, X2, X3), if#(X1, X2, mark(X3)) -> if#(X1, X2, X3)) (if#(mark(X1), X2, X3) -> if#(X1, X2, X3), if#(X1, X2, active(X3)) -> if#(X1, X2, X3)) (if#(mark(X1), X2, X3) -> if#(X1, X2, X3), if#(X1, mark(X2), X3) -> if#(X1, X2, X3)) (if#(mark(X1), X2, X3) -> if#(X1, X2, X3), if#(X1, active(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#(mark(X1), X2, X3) -> if#(X1, X2, X3), if#(active(X1), X2, X3) -> if#(X1, X2, X3)) (if#(X1, mark(X2), X3) -> if#(X1, X2, X3), if#(X1, X2, mark(X3)) -> if#(X1, X2, X3)) (if#(X1, mark(X2), X3) -> if#(X1, X2, X3), if#(X1, X2, active(X3)) -> if#(X1, X2, X3)) (if#(X1, mark(X2), X3) -> if#(X1, X2, X3), if#(X1, mark(X2), X3) -> if#(X1, X2, X3)) (if#(X1, mark(X2), X3) -> if#(X1, X2, X3), if#(X1, active(X2), X3) -> if#(X1, X2, X3)) (if#(X1, mark(X2), X3) -> if#(X1, X2, X3), if#(mark(X1), X2, X3) -> if#(X1, X2, X3)) (if#(X1, mark(X2), X3) -> if#(X1, X2, X3), if#(active(X1), X2, X3) -> if#(X1, X2, X3)) (if#(X1, X2, mark(X3)) -> if#(X1, X2, X3), if#(X1, X2, mark(X3)) -> if#(X1, X2, X3)) (if#(X1, X2, mark(X3)) -> if#(X1, X2, X3), if#(X1, X2, active(X3)) -> if#(X1, X2, X3)) (if#(X1, X2, mark(X3)) -> if#(X1, X2, X3), if#(X1, mark(X2), X3) -> if#(X1, X2, X3)) (if#(X1, X2, mark(X3)) -> if#(X1, X2, X3), if#(X1, active(X2), X3) -> if#(X1, X2, X3)) (if#(X1, X2, mark(X3)) -> if#(X1, X2, X3), if#(mark(X1), X2, X3) -> if#(X1, X2, X3)) (if#(X1, X2, mark(X3)) -> if#(X1, X2, X3), if#(active(X1), X2, X3) -> if#(X1, X2, X3)) (mark#(diff(X1, X2)) -> active#(diff(mark(X1), mark(X2))), active#(p(0())) -> mark#(0())) (mark#(diff(X1, X2)) -> active#(diff(mark(X1), mark(X2))), active#(p(s(X))) -> mark#(X)) (mark#(diff(X1, X2)) -> active#(diff(mark(X1), mark(X2))), active#(leq(0(), Y)) -> mark#(true())) (mark#(diff(X1, X2)) -> active#(diff(mark(X1), mark(X2))), active#(leq(s(X), 0())) -> mark#(false())) (mark#(diff(X1, X2)) -> active#(diff(mark(X1), mark(X2))), active#(leq(s(X), s(Y))) -> mark#(leq(X, Y))) (mark#(diff(X1, X2)) -> active#(diff(mark(X1), mark(X2))), active#(leq(s(X), s(Y))) -> leq#(X, Y)) (mark#(diff(X1, X2)) -> active#(diff(mark(X1), mark(X2))), active#(if(true(), X, Y)) -> mark#(X)) (mark#(diff(X1, X2)) -> active#(diff(mark(X1), mark(X2))), active#(if(false(), X, Y)) -> mark#(Y)) (mark#(diff(X1, X2)) -> active#(diff(mark(X1), mark(X2))), active#(diff(X, Y)) -> mark#(if(leq(X, Y), 0(), s(diff(p(X), Y))))) (mark#(diff(X1, X2)) -> active#(diff(mark(X1), mark(X2))), active#(diff(X, Y)) -> p#(X)) (mark#(diff(X1, X2)) -> active#(diff(mark(X1), mark(X2))), active#(diff(X, Y)) -> s#(diff(p(X), Y))) (mark#(diff(X1, X2)) -> active#(diff(mark(X1), mark(X2))), active#(diff(X, Y)) -> leq#(X, Y)) (mark#(diff(X1, X2)) -> active#(diff(mark(X1), mark(X2))), active#(diff(X, Y)) -> if#(leq(X, Y), 0(), s(diff(p(X), Y)))) (mark#(diff(X1, X2)) -> active#(diff(mark(X1), mark(X2))), active#(diff(X, Y)) -> diff#(p(X), Y)) (mark#(diff(X1, X2)) -> mark#(X1), mark#(0()) -> active#(0())) (mark#(diff(X1, X2)) -> mark#(X1), mark#(p(X)) -> mark#(X)) (mark#(diff(X1, X2)) -> mark#(X1), mark#(p(X)) -> active#(p(mark(X)))) (mark#(diff(X1, X2)) -> mark#(X1), mark#(p(X)) -> p#(mark(X))) (mark#(diff(X1, X2)) -> mark#(X1), mark#(s(X)) -> mark#(X)) (mark#(diff(X1, X2)) -> mark#(X1), mark#(s(X)) -> active#(s(mark(X)))) (mark#(diff(X1, X2)) -> mark#(X1), mark#(s(X)) -> s#(mark(X))) (mark#(diff(X1, X2)) -> mark#(X1), mark#(true()) -> active#(true())) (mark#(diff(X1, X2)) -> mark#(X1), mark#(leq(X1, X2)) -> mark#(X1)) (mark#(diff(X1, X2)) -> mark#(X1), mark#(leq(X1, X2)) -> mark#(X2)) (mark#(diff(X1, X2)) -> mark#(X1), mark#(leq(X1, X2)) -> active#(leq(mark(X1), mark(X2)))) (mark#(diff(X1, X2)) -> mark#(X1), mark#(leq(X1, X2)) -> leq#(mark(X1), mark(X2))) (mark#(diff(X1, X2)) -> mark#(X1), mark#(false()) -> active#(false())) (mark#(diff(X1, X2)) -> mark#(X1), mark#(if(X1, X2, X3)) -> mark#(X1)) (mark#(diff(X1, X2)) -> mark#(X1), mark#(if(X1, X2, X3)) -> active#(if(mark(X1), X2, X3))) (mark#(diff(X1, X2)) -> mark#(X1), mark#(if(X1, X2, X3)) -> if#(mark(X1), X2, X3)) (mark#(diff(X1, X2)) -> mark#(X1), mark#(diff(X1, X2)) -> mark#(X1)) (mark#(diff(X1, X2)) -> mark#(X1), mark#(diff(X1, X2)) -> mark#(X2)) (mark#(diff(X1, X2)) -> mark#(X1), mark#(diff(X1, X2)) -> active#(diff(mark(X1), mark(X2)))) (mark#(diff(X1, X2)) -> mark#(X1), mark#(diff(X1, X2)) -> diff#(mark(X1), mark(X2))) (mark#(leq(X1, X2)) -> mark#(X1), mark#(0()) -> active#(0())) (mark#(leq(X1, X2)) -> mark#(X1), mark#(p(X)) -> mark#(X)) (mark#(leq(X1, X2)) -> mark#(X1), mark#(p(X)) -> active#(p(mark(X)))) (mark#(leq(X1, X2)) -> mark#(X1), mark#(p(X)) -> p#(mark(X))) (mark#(leq(X1, X2)) -> mark#(X1), mark#(s(X)) -> mark#(X)) (mark#(leq(X1, X2)) -> mark#(X1), mark#(s(X)) -> active#(s(mark(X)))) (mark#(leq(X1, X2)) -> mark#(X1), mark#(s(X)) -> s#(mark(X))) (mark#(leq(X1, X2)) -> mark#(X1), mark#(true()) -> active#(true())) (mark#(leq(X1, X2)) -> mark#(X1), mark#(leq(X1, X2)) -> mark#(X1)) (mark#(leq(X1, X2)) -> mark#(X1), mark#(leq(X1, X2)) -> mark#(X2)) (mark#(leq(X1, X2)) -> mark#(X1), mark#(leq(X1, X2)) -> active#(leq(mark(X1), mark(X2)))) (mark#(leq(X1, X2)) -> mark#(X1), mark#(leq(X1, X2)) -> leq#(mark(X1), mark(X2))) (mark#(leq(X1, X2)) -> mark#(X1), mark#(false()) -> active#(false())) (mark#(leq(X1, X2)) -> mark#(X1), mark#(if(X1, X2, X3)) -> mark#(X1)) (mark#(leq(X1, X2)) -> mark#(X1), mark#(if(X1, X2, X3)) -> active#(if(mark(X1), X2, X3))) (mark#(leq(X1, X2)) -> mark#(X1), mark#(if(X1, X2, X3)) -> if#(mark(X1), X2, X3)) (mark#(leq(X1, X2)) -> mark#(X1), mark#(diff(X1, X2)) -> mark#(X1)) (mark#(leq(X1, X2)) -> mark#(X1), mark#(diff(X1, X2)) -> mark#(X2)) (mark#(leq(X1, X2)) -> mark#(X1), mark#(diff(X1, X2)) -> active#(diff(mark(X1), mark(X2)))) (mark#(leq(X1, X2)) -> mark#(X1), mark#(diff(X1, X2)) -> diff#(mark(X1), mark(X2))) (mark#(leq(X1, X2)) -> mark#(X2), mark#(0()) -> active#(0())) (mark#(leq(X1, X2)) -> mark#(X2), mark#(p(X)) -> mark#(X)) (mark#(leq(X1, X2)) -> mark#(X2), mark#(p(X)) -> active#(p(mark(X)))) (mark#(leq(X1, X2)) -> mark#(X2), mark#(p(X)) -> p#(mark(X))) (mark#(leq(X1, X2)) -> mark#(X2), mark#(s(X)) -> mark#(X)) (mark#(leq(X1, X2)) -> mark#(X2), mark#(s(X)) -> active#(s(mark(X)))) (mark#(leq(X1, X2)) -> mark#(X2), mark#(s(X)) -> s#(mark(X))) (mark#(leq(X1, X2)) -> mark#(X2), mark#(true()) -> active#(true())) (mark#(leq(X1, X2)) -> mark#(X2), mark#(leq(X1, X2)) -> mark#(X1)) (mark#(leq(X1, X2)) -> mark#(X2), mark#(leq(X1, X2)) -> mark#(X2)) (mark#(leq(X1, X2)) -> mark#(X2), mark#(leq(X1, X2)) -> active#(leq(mark(X1), mark(X2)))) (mark#(leq(X1, X2)) -> mark#(X2), mark#(leq(X1, X2)) -> leq#(mark(X1), mark(X2))) (mark#(leq(X1, X2)) -> mark#(X2), mark#(false()) -> active#(false())) (mark#(leq(X1, X2)) -> mark#(X2), mark#(if(X1, X2, X3)) -> mark#(X1)) (mark#(leq(X1, X2)) -> mark#(X2), mark#(if(X1, X2, X3)) -> active#(if(mark(X1), X2, X3))) (mark#(leq(X1, X2)) -> mark#(X2), mark#(if(X1, X2, X3)) -> if#(mark(X1), X2, X3)) (mark#(leq(X1, X2)) -> mark#(X2), mark#(diff(X1, X2)) -> mark#(X1)) (mark#(leq(X1, X2)) -> mark#(X2), mark#(diff(X1, X2)) -> mark#(X2)) (mark#(leq(X1, X2)) -> mark#(X2), mark#(diff(X1, X2)) -> active#(diff(mark(X1), mark(X2)))) (mark#(leq(X1, X2)) -> mark#(X2), mark#(diff(X1, X2)) -> diff#(mark(X1), mark(X2))) (active#(leq(0(), Y)) -> mark#(true()), mark#(true()) -> active#(true())) (mark#(diff(X1, X2)) -> diff#(mark(X1), mark(X2)), diff#(X1, mark(X2)) -> diff#(X1, X2)) (mark#(diff(X1, X2)) -> diff#(mark(X1), mark(X2)), diff#(X1, active(X2)) -> diff#(X1, X2)) (mark#(diff(X1, X2)) -> diff#(mark(X1), mark(X2)), diff#(mark(X1), X2) -> diff#(X1, X2)) (mark#(diff(X1, X2)) -> diff#(mark(X1), mark(X2)), diff#(active(X1), 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#(active(X)) -> s#(X)) (s#(active(X)) -> s#(X), s#(mark(X)) -> s#(X)) (s#(active(X)) -> s#(X), s#(active(X)) -> s#(X)) (p#(active(X)) -> p#(X), p#(mark(X)) -> p#(X)) (p#(active(X)) -> p#(X), p#(active(X)) -> p#(X)) (active#(diff(X, Y)) -> p#(X), p#(mark(X)) -> p#(X)) (active#(diff(X, Y)) -> p#(X), p#(active(X)) -> p#(X)) (active#(if(true(), X, Y)) -> mark#(X), mark#(0()) -> active#(0())) (active#(if(true(), X, Y)) -> mark#(X), mark#(p(X)) -> mark#(X)) (active#(if(true(), X, Y)) -> mark#(X), mark#(p(X)) -> active#(p(mark(X)))) (active#(if(true(), X, Y)) -> mark#(X), mark#(p(X)) -> p#(mark(X))) (active#(if(true(), X, Y)) -> mark#(X), mark#(s(X)) -> mark#(X)) (active#(if(true(), X, Y)) -> mark#(X), mark#(s(X)) -> active#(s(mark(X)))) (active#(if(true(), X, Y)) -> mark#(X), mark#(s(X)) -> s#(mark(X))) (active#(if(true(), X, Y)) -> mark#(X), mark#(true()) -> active#(true())) (active#(if(true(), X, Y)) -> mark#(X), mark#(leq(X1, X2)) -> mark#(X1)) (active#(if(true(), X, Y)) -> mark#(X), mark#(leq(X1, X2)) -> mark#(X2)) (active#(if(true(), X, Y)) -> mark#(X), mark#(leq(X1, X2)) -> active#(leq(mark(X1), mark(X2)))) (active#(if(true(), X, Y)) -> mark#(X), mark#(leq(X1, X2)) -> leq#(mark(X1), mark(X2))) (active#(if(true(), X, Y)) -> mark#(X), mark#(false()) -> active#(false())) (active#(if(true(), X, Y)) -> mark#(X), mark#(if(X1, X2, X3)) -> mark#(X1)) (active#(if(true(), X, Y)) -> mark#(X), mark#(if(X1, X2, X3)) -> active#(if(mark(X1), X2, X3))) (active#(if(true(), X, Y)) -> mark#(X), mark#(if(X1, X2, X3)) -> if#(mark(X1), X2, X3)) (active#(if(true(), X, Y)) -> mark#(X), mark#(diff(X1, X2)) -> mark#(X1)) (active#(if(true(), X, Y)) -> mark#(X), mark#(diff(X1, X2)) -> mark#(X2)) (active#(if(true(), X, Y)) -> mark#(X), mark#(diff(X1, X2)) -> active#(diff(mark(X1), mark(X2)))) (active#(if(true(), X, Y)) -> mark#(X), mark#(diff(X1, X2)) -> diff#(mark(X1), mark(X2))) (mark#(s(X)) -> mark#(X), mark#(0()) -> active#(0())) (mark#(s(X)) -> mark#(X), mark#(p(X)) -> mark#(X)) (mark#(s(X)) -> mark#(X), mark#(p(X)) -> active#(p(mark(X)))) (mark#(s(X)) -> mark#(X), mark#(p(X)) -> p#(mark(X))) (mark#(s(X)) -> mark#(X), mark#(s(X)) -> mark#(X)) (mark#(s(X)) -> mark#(X), mark#(s(X)) -> active#(s(mark(X)))) (mark#(s(X)) -> mark#(X), mark#(s(X)) -> s#(mark(X))) (mark#(s(X)) -> mark#(X), mark#(true()) -> active#(true())) (mark#(s(X)) -> mark#(X), mark#(leq(X1, X2)) -> mark#(X1)) (mark#(s(X)) -> mark#(X), mark#(leq(X1, X2)) -> mark#(X2)) (mark#(s(X)) -> mark#(X), mark#(leq(X1, X2)) -> active#(leq(mark(X1), mark(X2)))) (mark#(s(X)) -> mark#(X), mark#(leq(X1, X2)) -> leq#(mark(X1), mark(X2))) (mark#(s(X)) -> mark#(X), mark#(false()) -> active#(false())) (mark#(s(X)) -> mark#(X), mark#(if(X1, X2, X3)) -> mark#(X1)) (mark#(s(X)) -> mark#(X), mark#(if(X1, X2, X3)) -> active#(if(mark(X1), X2, X3))) (mark#(s(X)) -> mark#(X), mark#(if(X1, X2, X3)) -> if#(mark(X1), X2, X3)) (mark#(s(X)) -> mark#(X), mark#(diff(X1, X2)) -> mark#(X1)) (mark#(s(X)) -> mark#(X), mark#(diff(X1, X2)) -> mark#(X2)) (mark#(s(X)) -> mark#(X), mark#(diff(X1, X2)) -> active#(diff(mark(X1), mark(X2)))) (mark#(s(X)) -> mark#(X), mark#(diff(X1, X2)) -> diff#(mark(X1), mark(X2))) (diff#(active(X1), X2) -> diff#(X1, X2), diff#(X1, mark(X2)) -> diff#(X1, X2)) (diff#(active(X1), X2) -> diff#(X1, X2), diff#(X1, active(X2)) -> diff#(X1, X2)) (diff#(active(X1), X2) -> diff#(X1, X2), diff#(mark(X1), X2) -> diff#(X1, X2)) (diff#(active(X1), X2) -> diff#(X1, X2), diff#(active(X1), X2) -> diff#(X1, X2)) (diff#(X1, active(X2)) -> diff#(X1, X2), diff#(X1, mark(X2)) -> diff#(X1, X2)) (diff#(X1, active(X2)) -> diff#(X1, X2), diff#(X1, active(X2)) -> diff#(X1, X2)) (diff#(X1, active(X2)) -> diff#(X1, X2), diff#(mark(X1), X2) -> diff#(X1, X2)) (diff#(X1, active(X2)) -> diff#(X1, X2), diff#(active(X1), X2) -> diff#(X1, X2)) (leq#(active(X1), X2) -> leq#(X1, X2), leq#(X1, mark(X2)) -> leq#(X1, X2)) (leq#(active(X1), X2) -> leq#(X1, X2), leq#(X1, active(X2)) -> leq#(X1, X2)) (leq#(active(X1), X2) -> leq#(X1, X2), leq#(mark(X1), X2) -> leq#(X1, X2)) (leq#(active(X1), X2) -> leq#(X1, X2), leq#(active(X1), X2) -> leq#(X1, X2)) (leq#(X1, active(X2)) -> leq#(X1, X2), leq#(X1, mark(X2)) -> leq#(X1, X2)) (leq#(X1, active(X2)) -> leq#(X1, X2), leq#(X1, active(X2)) -> leq#(X1, X2)) (leq#(X1, active(X2)) -> leq#(X1, X2), leq#(mark(X1), X2) -> leq#(X1, X2)) (leq#(X1, active(X2)) -> leq#(X1, X2), leq#(active(X1), X2) -> leq#(X1, X2)) (active#(diff(X, Y)) -> leq#(X, Y), leq#(X1, mark(X2)) -> leq#(X1, X2)) (active#(diff(X, Y)) -> leq#(X, Y), leq#(X1, active(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#(active(X1), X2) -> leq#(X1, X2)) (mark#(s(X)) -> active#(s(mark(X))), active#(p(0())) -> mark#(0())) (mark#(s(X)) -> active#(s(mark(X))), active#(p(s(X))) -> mark#(X)) (mark#(s(X)) -> active#(s(mark(X))), active#(leq(0(), Y)) -> mark#(true())) (mark#(s(X)) -> active#(s(mark(X))), active#(leq(s(X), 0())) -> mark#(false())) (mark#(s(X)) -> active#(s(mark(X))), active#(leq(s(X), s(Y))) -> mark#(leq(X, Y))) (mark#(s(X)) -> active#(s(mark(X))), active#(leq(s(X), s(Y))) -> leq#(X, Y)) (mark#(s(X)) -> active#(s(mark(X))), active#(if(true(), X, Y)) -> mark#(X)) (mark#(s(X)) -> active#(s(mark(X))), active#(if(false(), X, Y)) -> mark#(Y)) (mark#(s(X)) -> active#(s(mark(X))), active#(diff(X, Y)) -> mark#(if(leq(X, Y), 0(), s(diff(p(X), Y))))) (mark#(s(X)) -> active#(s(mark(X))), active#(diff(X, Y)) -> p#(X)) (mark#(s(X)) -> active#(s(mark(X))), active#(diff(X, Y)) -> s#(diff(p(X), Y))) (mark#(s(X)) -> active#(s(mark(X))), active#(diff(X, Y)) -> leq#(X, Y)) (mark#(s(X)) -> active#(s(mark(X))), active#(diff(X, Y)) -> if#(leq(X, Y), 0(), s(diff(p(X), Y)))) (mark#(s(X)) -> active#(s(mark(X))), active#(diff(X, Y)) -> diff#(p(X), Y)) (active#(if(false(), X, Y)) -> mark#(Y), mark#(0()) -> active#(0())) (active#(if(false(), X, Y)) -> mark#(Y), mark#(p(X)) -> mark#(X)) (active#(if(false(), X, Y)) -> mark#(Y), mark#(p(X)) -> active#(p(mark(X)))) (active#(if(false(), X, Y)) -> mark#(Y), mark#(p(X)) -> p#(mark(X))) (active#(if(false(), X, Y)) -> mark#(Y), mark#(s(X)) -> mark#(X)) (active#(if(false(), X, Y)) -> mark#(Y), mark#(s(X)) -> active#(s(mark(X)))) (active#(if(false(), X, Y)) -> mark#(Y), mark#(s(X)) -> s#(mark(X))) (active#(if(false(), X, Y)) -> mark#(Y), mark#(true()) -> active#(true())) (active#(if(false(), X, Y)) -> mark#(Y), mark#(leq(X1, X2)) -> mark#(X1)) (active#(if(false(), X, Y)) -> mark#(Y), mark#(leq(X1, X2)) -> mark#(X2)) (active#(if(false(), X, Y)) -> mark#(Y), mark#(leq(X1, X2)) -> active#(leq(mark(X1), mark(X2)))) (active#(if(false(), X, Y)) -> mark#(Y), mark#(leq(X1, X2)) -> leq#(mark(X1), mark(X2))) (active#(if(false(), X, Y)) -> mark#(Y), mark#(false()) -> active#(false())) (active#(if(false(), X, Y)) -> mark#(Y), mark#(if(X1, X2, X3)) -> mark#(X1)) (active#(if(false(), X, Y)) -> mark#(Y), mark#(if(X1, X2, X3)) -> active#(if(mark(X1), X2, X3))) (active#(if(false(), X, Y)) -> mark#(Y), mark#(if(X1, X2, X3)) -> if#(mark(X1), X2, X3)) (active#(if(false(), X, Y)) -> mark#(Y), mark#(diff(X1, X2)) -> mark#(X1)) (active#(if(false(), X, Y)) -> mark#(Y), mark#(diff(X1, X2)) -> mark#(X2)) (active#(if(false(), X, Y)) -> mark#(Y), mark#(diff(X1, X2)) -> active#(diff(mark(X1), mark(X2)))) (active#(if(false(), X, Y)) -> mark#(Y), mark#(diff(X1, X2)) -> diff#(mark(X1), mark(X2))) (active#(diff(X, Y)) -> diff#(p(X), Y), diff#(X1, mark(X2)) -> diff#(X1, X2)) (active#(diff(X, Y)) -> diff#(p(X), Y), diff#(X1, active(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#(active(X1), X2) -> diff#(X1, X2)) } SCCS: Scc: { diff#(X1, mark(X2)) -> diff#(X1, X2), diff#(X1, active(X2)) -> diff#(X1, X2), diff#(mark(X1), X2) -> diff#(X1, X2), diff#(active(X1), X2) -> diff#(X1, X2)} Scc: { if#(X1, X2, mark(X3)) -> if#(X1, X2, X3), if#(X1, X2, active(X3)) -> if#(X1, X2, X3), if#(X1, mark(X2), X3) -> if#(X1, X2, X3), if#(X1, active(X2), X3) -> if#(X1, X2, X3), if#(mark(X1), X2, X3) -> if#(X1, X2, X3), if#(active(X1), X2, X3) -> if#(X1, X2, X3)} Scc: { leq#(X1, mark(X2)) -> leq#(X1, X2), leq#(X1, active(X2)) -> leq#(X1, X2), leq#(mark(X1), X2) -> leq#(X1, X2), leq#(active(X1), X2) -> leq#(X1, X2)} Scc: { s#(mark(X)) -> s#(X), s#(active(X)) -> s#(X)} Scc: { p#(mark(X)) -> p#(X), p#(active(X)) -> p#(X)} Scc: { mark#(p(X)) -> mark#(X), mark#(p(X)) -> active#(p(mark(X))), mark#(s(X)) -> mark#(X), mark#(s(X)) -> active#(s(mark(X))), mark#(leq(X1, X2)) -> mark#(X1), mark#(leq(X1, X2)) -> mark#(X2), mark#(leq(X1, X2)) -> active#(leq(mark(X1), mark(X2))), mark#(if(X1, X2, X3)) -> mark#(X1), mark#(if(X1, X2, X3)) -> active#(if(mark(X1), X2, X3)), mark#(diff(X1, X2)) -> mark#(X1), mark#(diff(X1, X2)) -> mark#(X2), mark#(diff(X1, X2)) -> active#(diff(mark(X1), mark(X2))), active#(p(s(X))) -> mark#(X), active#(leq(s(X), s(Y))) -> mark#(leq(X, Y)), 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))))} SCC: Strict: { diff#(X1, mark(X2)) -> diff#(X1, X2), diff#(X1, active(X2)) -> diff#(X1, X2), diff#(mark(X1), X2) -> diff#(X1, X2), diff#(active(X1), X2) -> diff#(X1, X2)} Weak: { mark(0()) -> active(0()), mark(p(X)) -> active(p(mark(X))), mark(s(X)) -> active(s(mark(X))), mark(true()) -> active(true()), mark(leq(X1, X2)) -> active(leq(mark(X1), mark(X2))), mark(false()) -> active(false()), mark(if(X1, X2, X3)) -> active(if(mark(X1), X2, X3)), mark(diff(X1, X2)) -> active(diff(mark(X1), mark(X2))), active(p(0())) -> mark(0()), active(p(s(X))) -> mark(X), 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(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)))), p(mark(X)) -> p(X), p(active(X)) -> p(X), s(mark(X)) -> s(X), s(active(X)) -> s(X), leq(X1, mark(X2)) -> leq(X1, X2), leq(X1, active(X2)) -> leq(X1, X2), leq(mark(X1), X2) -> leq(X1, X2), leq(active(X1), X2) -> leq(X1, X2), if(X1, X2, mark(X3)) -> if(X1, X2, X3), if(X1, X2, active(X3)) -> if(X1, X2, X3), if(X1, mark(X2), X3) -> if(X1, X2, X3), if(X1, active(X2), X3) -> if(X1, X2, X3), if(mark(X1), X2, X3) -> if(X1, X2, X3), if(active(X1), X2, X3) -> if(X1, X2, X3), diff(X1, mark(X2)) -> diff(X1, X2), diff(X1, active(X2)) -> diff(X1, X2), diff(mark(X1), X2) -> diff(X1, X2), diff(active(X1), X2) -> diff(X1, X2)} SPSC: Simple Projection: pi(diff#) = 0 Strict: { diff#(X1, mark(X2)) -> diff#(X1, X2), diff#(X1, active(X2)) -> diff#(X1, X2), diff#(mark(X1), X2) -> diff#(X1, X2)} EDG: {(diff#(X1, active(X2)) -> diff#(X1, X2), diff#(mark(X1), X2) -> diff#(X1, X2)) (diff#(X1, active(X2)) -> diff#(X1, X2), diff#(X1, active(X2)) -> diff#(X1, X2)) (diff#(X1, active(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#(mark(X1), X2) -> diff#(X1, X2), diff#(X1, active(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, active(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#(X1, active(X2)) -> diff#(X1, X2), diff#(mark(X1), X2) -> diff#(X1, X2)} SCC: Strict: { diff#(X1, mark(X2)) -> diff#(X1, X2), diff#(X1, active(X2)) -> diff#(X1, X2), diff#(mark(X1), X2) -> diff#(X1, X2)} Weak: { mark(0()) -> active(0()), mark(p(X)) -> active(p(mark(X))), mark(s(X)) -> active(s(mark(X))), mark(true()) -> active(true()), mark(leq(X1, X2)) -> active(leq(mark(X1), mark(X2))), mark(false()) -> active(false()), mark(if(X1, X2, X3)) -> active(if(mark(X1), X2, X3)), mark(diff(X1, X2)) -> active(diff(mark(X1), mark(X2))), active(p(0())) -> mark(0()), active(p(s(X))) -> mark(X), 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(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)))), p(mark(X)) -> p(X), p(active(X)) -> p(X), s(mark(X)) -> s(X), s(active(X)) -> s(X), leq(X1, mark(X2)) -> leq(X1, X2), leq(X1, active(X2)) -> leq(X1, X2), leq(mark(X1), X2) -> leq(X1, X2), leq(active(X1), X2) -> leq(X1, X2), if(X1, X2, mark(X3)) -> if(X1, X2, X3), if(X1, X2, active(X3)) -> if(X1, X2, X3), if(X1, mark(X2), X3) -> if(X1, X2, X3), if(X1, active(X2), X3) -> if(X1, X2, X3), if(mark(X1), X2, X3) -> if(X1, X2, X3), if(active(X1), X2, X3) -> if(X1, X2, X3), diff(X1, mark(X2)) -> diff(X1, X2), diff(X1, active(X2)) -> diff(X1, X2), diff(mark(X1), X2) -> diff(X1, X2), diff(active(X1), X2) -> diff(X1, X2)} SPSC: Simple Projection: pi(diff#) = 1 Strict: {diff#(X1, active(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, active(X2)) -> diff#(X1, X2)) (diff#(X1, active(X2)) -> diff#(X1, X2), diff#(X1, active(X2)) -> diff#(X1, X2)) (diff#(X1, active(X2)) -> diff#(X1, X2), diff#(mark(X1), X2) -> diff#(X1, X2))} SCCS: Scc: {diff#(X1, active(X2)) -> diff#(X1, X2), diff#(mark(X1), X2) -> diff#(X1, X2)} SCC: Strict: {diff#(X1, active(X2)) -> diff#(X1, X2), diff#(mark(X1), X2) -> diff#(X1, X2)} Weak: { mark(0()) -> active(0()), mark(p(X)) -> active(p(mark(X))), mark(s(X)) -> active(s(mark(X))), mark(true()) -> active(true()), mark(leq(X1, X2)) -> active(leq(mark(X1), mark(X2))), mark(false()) -> active(false()), mark(if(X1, X2, X3)) -> active(if(mark(X1), X2, X3)), mark(diff(X1, X2)) -> active(diff(mark(X1), mark(X2))), active(p(0())) -> mark(0()), active(p(s(X))) -> mark(X), 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(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)))), p(mark(X)) -> p(X), p(active(X)) -> p(X), s(mark(X)) -> s(X), s(active(X)) -> s(X), leq(X1, mark(X2)) -> leq(X1, X2), leq(X1, active(X2)) -> leq(X1, X2), leq(mark(X1), X2) -> leq(X1, X2), leq(active(X1), X2) -> leq(X1, X2), if(X1, X2, mark(X3)) -> if(X1, X2, X3), if(X1, X2, active(X3)) -> if(X1, X2, X3), if(X1, mark(X2), X3) -> if(X1, X2, X3), if(X1, active(X2), X3) -> if(X1, X2, X3), if(mark(X1), X2, X3) -> if(X1, X2, X3), if(active(X1), X2, X3) -> if(X1, X2, X3), diff(X1, mark(X2)) -> diff(X1, X2), diff(X1, active(X2)) -> diff(X1, X2), diff(mark(X1), X2) -> diff(X1, X2), diff(active(X1), X2) -> diff(X1, X2)} SPSC: Simple Projection: pi(diff#) = 0 Strict: {diff#(X1, active(X2)) -> diff#(X1, X2)} EDG: {(diff#(X1, active(X2)) -> diff#(X1, X2), diff#(X1, active(X2)) -> diff#(X1, X2))} SCCS: Scc: {diff#(X1, active(X2)) -> diff#(X1, X2)} SCC: Strict: {diff#(X1, active(X2)) -> diff#(X1, X2)} Weak: { mark(0()) -> active(0()), mark(p(X)) -> active(p(mark(X))), mark(s(X)) -> active(s(mark(X))), mark(true()) -> active(true()), mark(leq(X1, X2)) -> active(leq(mark(X1), mark(X2))), mark(false()) -> active(false()), mark(if(X1, X2, X3)) -> active(if(mark(X1), X2, X3)), mark(diff(X1, X2)) -> active(diff(mark(X1), mark(X2))), active(p(0())) -> mark(0()), active(p(s(X))) -> mark(X), 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(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)))), p(mark(X)) -> p(X), p(active(X)) -> p(X), s(mark(X)) -> s(X), s(active(X)) -> s(X), leq(X1, mark(X2)) -> leq(X1, X2), leq(X1, active(X2)) -> leq(X1, X2), leq(mark(X1), X2) -> leq(X1, X2), leq(active(X1), X2) -> leq(X1, X2), if(X1, X2, mark(X3)) -> if(X1, X2, X3), if(X1, X2, active(X3)) -> if(X1, X2, X3), if(X1, mark(X2), X3) -> if(X1, X2, X3), if(X1, active(X2), X3) -> if(X1, X2, X3), if(mark(X1), X2, X3) -> if(X1, X2, X3), if(active(X1), X2, X3) -> if(X1, X2, X3), diff(X1, mark(X2)) -> diff(X1, X2), diff(X1, active(X2)) -> diff(X1, X2), diff(mark(X1), X2) -> diff(X1, X2), diff(active(X1), X2) -> diff(X1, X2)} SPSC: Simple Projection: pi(diff#) = 1 Strict: {} Qed SCC: Strict: { if#(X1, X2, mark(X3)) -> if#(X1, X2, X3), if#(X1, X2, active(X3)) -> if#(X1, X2, X3), if#(X1, mark(X2), X3) -> if#(X1, X2, X3), if#(X1, active(X2), X3) -> if#(X1, X2, X3), if#(mark(X1), X2, X3) -> if#(X1, X2, X3), if#(active(X1), X2, X3) -> if#(X1, X2, X3)} Weak: { mark(0()) -> active(0()), mark(p(X)) -> active(p(mark(X))), mark(s(X)) -> active(s(mark(X))), mark(true()) -> active(true()), mark(leq(X1, X2)) -> active(leq(mark(X1), mark(X2))), mark(false()) -> active(false()), mark(if(X1, X2, X3)) -> active(if(mark(X1), X2, X3)), mark(diff(X1, X2)) -> active(diff(mark(X1), mark(X2))), active(p(0())) -> mark(0()), active(p(s(X))) -> mark(X), 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(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)))), p(mark(X)) -> p(X), p(active(X)) -> p(X), s(mark(X)) -> s(X), s(active(X)) -> s(X), leq(X1, mark(X2)) -> leq(X1, X2), leq(X1, active(X2)) -> leq(X1, X2), leq(mark(X1), X2) -> leq(X1, X2), leq(active(X1), X2) -> leq(X1, X2), if(X1, X2, mark(X3)) -> if(X1, X2, X3), if(X1, X2, active(X3)) -> if(X1, X2, X3), if(X1, mark(X2), X3) -> if(X1, X2, X3), if(X1, active(X2), X3) -> if(X1, X2, X3), if(mark(X1), X2, X3) -> if(X1, X2, X3), if(active(X1), X2, X3) -> if(X1, X2, X3), diff(X1, mark(X2)) -> diff(X1, X2), diff(X1, active(X2)) -> diff(X1, X2), diff(mark(X1), X2) -> diff(X1, X2), diff(active(X1), X2) -> diff(X1, X2)} SPSC: Simple Projection: pi(if#) = 0 Strict: { if#(X1, X2, mark(X3)) -> if#(X1, X2, X3), if#(X1, X2, active(X3)) -> if#(X1, X2, X3), if#(X1, mark(X2), X3) -> if#(X1, X2, X3), if#(X1, active(X2), X3) -> if#(X1, X2, X3), if#(mark(X1), X2, X3) -> if#(X1, X2, X3)} EDG: {(if#(X1, X2, active(X3)) -> if#(X1, X2, X3), if#(mark(X1), X2, X3) -> if#(X1, X2, X3)) (if#(X1, X2, active(X3)) -> if#(X1, X2, X3), if#(X1, active(X2), X3) -> if#(X1, X2, X3)) (if#(X1, X2, active(X3)) -> if#(X1, X2, X3), if#(X1, mark(X2), X3) -> if#(X1, X2, X3)) (if#(X1, X2, active(X3)) -> if#(X1, X2, X3), if#(X1, X2, active(X3)) -> if#(X1, X2, X3)) (if#(X1, X2, active(X3)) -> if#(X1, X2, X3), if#(X1, X2, mark(X3)) -> if#(X1, X2, X3)) (if#(X1, active(X2), X3) -> if#(X1, X2, X3), if#(mark(X1), X2, X3) -> if#(X1, X2, X3)) (if#(X1, active(X2), X3) -> if#(X1, X2, X3), if#(X1, active(X2), X3) -> if#(X1, X2, X3)) (if#(X1, active(X2), X3) -> if#(X1, X2, X3), if#(X1, mark(X2), X3) -> if#(X1, X2, X3)) (if#(X1, active(X2), X3) -> if#(X1, X2, X3), if#(X1, X2, active(X3)) -> if#(X1, X2, X3)) (if#(X1, active(X2), X3) -> if#(X1, X2, X3), if#(X1, X2, mark(X3)) -> if#(X1, X2, X3)) (if#(mark(X1), X2, X3) -> if#(X1, X2, X3), if#(X1, X2, mark(X3)) -> if#(X1, X2, X3)) (if#(mark(X1), X2, X3) -> if#(X1, X2, X3), if#(X1, X2, active(X3)) -> if#(X1, X2, X3)) (if#(mark(X1), X2, X3) -> if#(X1, X2, X3), if#(X1, mark(X2), X3) -> if#(X1, X2, X3)) (if#(mark(X1), X2, X3) -> if#(X1, X2, X3), if#(X1, active(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#(X1, mark(X2), X3) -> if#(X1, X2, X3), if#(X1, X2, mark(X3)) -> if#(X1, X2, X3)) (if#(X1, mark(X2), X3) -> if#(X1, X2, X3), if#(X1, X2, active(X3)) -> if#(X1, X2, X3)) (if#(X1, mark(X2), X3) -> if#(X1, X2, X3), if#(X1, mark(X2), X3) -> if#(X1, X2, X3)) (if#(X1, mark(X2), X3) -> if#(X1, X2, X3), if#(X1, active(X2), X3) -> if#(X1, X2, X3)) (if#(X1, mark(X2), X3) -> if#(X1, X2, X3), if#(mark(X1), X2, X3) -> if#(X1, X2, X3)) (if#(X1, X2, mark(X3)) -> if#(X1, X2, X3), if#(X1, X2, mark(X3)) -> if#(X1, X2, X3)) (if#(X1, X2, mark(X3)) -> if#(X1, X2, X3), if#(X1, X2, active(X3)) -> if#(X1, X2, X3)) (if#(X1, X2, mark(X3)) -> if#(X1, X2, X3), if#(X1, mark(X2), X3) -> if#(X1, X2, X3)) (if#(X1, X2, mark(X3)) -> if#(X1, X2, X3), if#(X1, active(X2), X3) -> if#(X1, X2, X3)) (if#(X1, X2, mark(X3)) -> if#(X1, X2, X3), if#(mark(X1), X2, X3) -> if#(X1, X2, X3))} SCCS: Scc: { if#(X1, X2, mark(X3)) -> if#(X1, X2, X3), if#(X1, X2, active(X3)) -> if#(X1, X2, X3), if#(X1, mark(X2), X3) -> if#(X1, X2, X3), if#(X1, active(X2), X3) -> if#(X1, X2, X3), if#(mark(X1), X2, X3) -> if#(X1, X2, X3)} SCC: Strict: { if#(X1, X2, mark(X3)) -> if#(X1, X2, X3), if#(X1, X2, active(X3)) -> if#(X1, X2, X3), if#(X1, mark(X2), X3) -> if#(X1, X2, X3), if#(X1, active(X2), X3) -> if#(X1, X2, X3), if#(mark(X1), X2, X3) -> if#(X1, X2, X3)} Weak: { mark(0()) -> active(0()), mark(p(X)) -> active(p(mark(X))), mark(s(X)) -> active(s(mark(X))), mark(true()) -> active(true()), mark(leq(X1, X2)) -> active(leq(mark(X1), mark(X2))), mark(false()) -> active(false()), mark(if(X1, X2, X3)) -> active(if(mark(X1), X2, X3)), mark(diff(X1, X2)) -> active(diff(mark(X1), mark(X2))), active(p(0())) -> mark(0()), active(p(s(X))) -> mark(X), 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(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)))), p(mark(X)) -> p(X), p(active(X)) -> p(X), s(mark(X)) -> s(X), s(active(X)) -> s(X), leq(X1, mark(X2)) -> leq(X1, X2), leq(X1, active(X2)) -> leq(X1, X2), leq(mark(X1), X2) -> leq(X1, X2), leq(active(X1), X2) -> leq(X1, X2), if(X1, X2, mark(X3)) -> if(X1, X2, X3), if(X1, X2, active(X3)) -> if(X1, X2, X3), if(X1, mark(X2), X3) -> if(X1, X2, X3), if(X1, active(X2), X3) -> if(X1, X2, X3), if(mark(X1), X2, X3) -> if(X1, X2, X3), if(active(X1), X2, X3) -> if(X1, X2, X3), diff(X1, mark(X2)) -> diff(X1, X2), diff(X1, active(X2)) -> diff(X1, X2), diff(mark(X1), X2) -> diff(X1, X2), diff(active(X1), X2) -> diff(X1, X2)} SPSC: Simple Projection: pi(if#) = 2 Strict: { if#(X1, X2, mark(X3)) -> if#(X1, X2, X3), if#(X1, mark(X2), X3) -> if#(X1, X2, X3), if#(X1, active(X2), X3) -> if#(X1, X2, X3), if#(mark(X1), X2, X3) -> if#(X1, X2, X3)} EDG: {(if#(X1, mark(X2), X3) -> if#(X1, X2, X3), if#(mark(X1), X2, X3) -> if#(X1, X2, X3)) (if#(X1, mark(X2), X3) -> if#(X1, X2, X3), if#(X1, active(X2), X3) -> if#(X1, X2, X3)) (if#(X1, mark(X2), X3) -> if#(X1, X2, X3), if#(X1, mark(X2), X3) -> if#(X1, X2, X3)) (if#(X1, mark(X2), X3) -> if#(X1, X2, X3), if#(X1, X2, mark(X3)) -> if#(X1, X2, X3)) (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#(X1, active(X2), X3) -> if#(X1, X2, X3)) (if#(mark(X1), X2, X3) -> if#(X1, X2, X3), if#(X1, mark(X2), X3) -> if#(X1, X2, X3)) (if#(mark(X1), X2, X3) -> if#(X1, X2, X3), if#(X1, X2, mark(X3)) -> if#(X1, X2, X3)) (if#(X1, active(X2), X3) -> if#(X1, X2, X3), if#(X1, X2, mark(X3)) -> if#(X1, X2, X3)) (if#(X1, active(X2), X3) -> if#(X1, X2, X3), if#(X1, mark(X2), X3) -> if#(X1, X2, X3)) (if#(X1, active(X2), X3) -> if#(X1, X2, X3), if#(X1, active(X2), X3) -> if#(X1, X2, X3)) (if#(X1, active(X2), X3) -> if#(X1, X2, X3), if#(mark(X1), X2, X3) -> if#(X1, X2, X3)) (if#(X1, X2, mark(X3)) -> if#(X1, X2, X3), if#(X1, X2, mark(X3)) -> if#(X1, X2, X3)) (if#(X1, X2, mark(X3)) -> if#(X1, X2, X3), if#(X1, mark(X2), X3) -> if#(X1, X2, X3)) (if#(X1, X2, mark(X3)) -> if#(X1, X2, X3), if#(X1, active(X2), X3) -> if#(X1, X2, X3)) (if#(X1, X2, mark(X3)) -> if#(X1, X2, X3), if#(mark(X1), X2, X3) -> if#(X1, X2, X3))} SCCS: Scc: { if#(X1, X2, mark(X3)) -> if#(X1, X2, X3), if#(X1, mark(X2), X3) -> if#(X1, X2, X3), if#(X1, active(X2), X3) -> if#(X1, X2, X3), if#(mark(X1), X2, X3) -> if#(X1, X2, X3)} SCC: Strict: { if#(X1, X2, mark(X3)) -> if#(X1, X2, X3), if#(X1, mark(X2), X3) -> if#(X1, X2, X3), if#(X1, active(X2), X3) -> if#(X1, X2, X3), if#(mark(X1), X2, X3) -> if#(X1, X2, X3)} Weak: { mark(0()) -> active(0()), mark(p(X)) -> active(p(mark(X))), mark(s(X)) -> active(s(mark(X))), mark(true()) -> active(true()), mark(leq(X1, X2)) -> active(leq(mark(X1), mark(X2))), mark(false()) -> active(false()), mark(if(X1, X2, X3)) -> active(if(mark(X1), X2, X3)), mark(diff(X1, X2)) -> active(diff(mark(X1), mark(X2))), active(p(0())) -> mark(0()), active(p(s(X))) -> mark(X), 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(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)))), p(mark(X)) -> p(X), p(active(X)) -> p(X), s(mark(X)) -> s(X), s(active(X)) -> s(X), leq(X1, mark(X2)) -> leq(X1, X2), leq(X1, active(X2)) -> leq(X1, X2), leq(mark(X1), X2) -> leq(X1, X2), leq(active(X1), X2) -> leq(X1, X2), if(X1, X2, mark(X3)) -> if(X1, X2, X3), if(X1, X2, active(X3)) -> if(X1, X2, X3), if(X1, mark(X2), X3) -> if(X1, X2, X3), if(X1, active(X2), X3) -> if(X1, X2, X3), if(mark(X1), X2, X3) -> if(X1, X2, X3), if(active(X1), X2, X3) -> if(X1, X2, X3), diff(X1, mark(X2)) -> diff(X1, X2), diff(X1, active(X2)) -> diff(X1, X2), diff(mark(X1), X2) -> diff(X1, X2), diff(active(X1), X2) -> diff(X1, X2)} SPSC: Simple Projection: pi(if#) = 0 Strict: { if#(X1, X2, mark(X3)) -> if#(X1, X2, X3), if#(X1, mark(X2), X3) -> if#(X1, X2, X3), if#(X1, active(X2), X3) -> if#(X1, X2, X3)} EDG: {(if#(X1, mark(X2), X3) -> if#(X1, X2, X3), if#(X1, active(X2), X3) -> if#(X1, X2, X3)) (if#(X1, mark(X2), X3) -> if#(X1, X2, X3), if#(X1, mark(X2), X3) -> if#(X1, X2, X3)) (if#(X1, mark(X2), X3) -> if#(X1, X2, X3), if#(X1, X2, mark(X3)) -> if#(X1, X2, X3)) (if#(X1, active(X2), X3) -> if#(X1, X2, X3), if#(X1, X2, mark(X3)) -> if#(X1, X2, X3)) (if#(X1, active(X2), X3) -> if#(X1, X2, X3), if#(X1, mark(X2), X3) -> if#(X1, X2, X3)) (if#(X1, active(X2), X3) -> if#(X1, X2, X3), if#(X1, active(X2), X3) -> if#(X1, X2, X3)) (if#(X1, X2, mark(X3)) -> if#(X1, X2, X3), if#(X1, X2, mark(X3)) -> if#(X1, X2, X3)) (if#(X1, X2, mark(X3)) -> if#(X1, X2, X3), if#(X1, mark(X2), X3) -> if#(X1, X2, X3)) (if#(X1, X2, mark(X3)) -> if#(X1, X2, X3), if#(X1, active(X2), X3) -> if#(X1, X2, X3))} SCCS: Scc: { if#(X1, X2, mark(X3)) -> if#(X1, X2, X3), if#(X1, mark(X2), X3) -> if#(X1, X2, X3), if#(X1, active(X2), X3) -> if#(X1, X2, X3)} SCC: Strict: { if#(X1, X2, mark(X3)) -> if#(X1, X2, X3), if#(X1, mark(X2), X3) -> if#(X1, X2, X3), if#(X1, active(X2), X3) -> if#(X1, X2, X3)} Weak: { mark(0()) -> active(0()), mark(p(X)) -> active(p(mark(X))), mark(s(X)) -> active(s(mark(X))), mark(true()) -> active(true()), mark(leq(X1, X2)) -> active(leq(mark(X1), mark(X2))), mark(false()) -> active(false()), mark(if(X1, X2, X3)) -> active(if(mark(X1), X2, X3)), mark(diff(X1, X2)) -> active(diff(mark(X1), mark(X2))), active(p(0())) -> mark(0()), active(p(s(X))) -> mark(X), 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(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)))), p(mark(X)) -> p(X), p(active(X)) -> p(X), s(mark(X)) -> s(X), s(active(X)) -> s(X), leq(X1, mark(X2)) -> leq(X1, X2), leq(X1, active(X2)) -> leq(X1, X2), leq(mark(X1), X2) -> leq(X1, X2), leq(active(X1), X2) -> leq(X1, X2), if(X1, X2, mark(X3)) -> if(X1, X2, X3), if(X1, X2, active(X3)) -> if(X1, X2, X3), if(X1, mark(X2), X3) -> if(X1, X2, X3), if(X1, active(X2), X3) -> if(X1, X2, X3), if(mark(X1), X2, X3) -> if(X1, X2, X3), if(active(X1), X2, X3) -> if(X1, X2, X3), diff(X1, mark(X2)) -> diff(X1, X2), diff(X1, active(X2)) -> diff(X1, X2), diff(mark(X1), X2) -> diff(X1, X2), diff(active(X1), X2) -> diff(X1, X2)} SPSC: Simple Projection: pi(if#) = 1 Strict: {if#(X1, X2, mark(X3)) -> if#(X1, X2, X3), if#(X1, mark(X2), X3) -> if#(X1, X2, X3)} EDG: {(if#(X1, mark(X2), X3) -> if#(X1, X2, X3), if#(X1, mark(X2), X3) -> if#(X1, X2, X3)) (if#(X1, mark(X2), X3) -> if#(X1, X2, X3), if#(X1, X2, mark(X3)) -> if#(X1, X2, X3)) (if#(X1, X2, mark(X3)) -> if#(X1, X2, X3), if#(X1, X2, mark(X3)) -> if#(X1, X2, X3)) (if#(X1, X2, mark(X3)) -> if#(X1, X2, X3), if#(X1, mark(X2), X3) -> if#(X1, X2, X3))} SCCS: Scc: {if#(X1, X2, mark(X3)) -> if#(X1, X2, X3), if#(X1, mark(X2), X3) -> if#(X1, X2, X3)} SCC: Strict: {if#(X1, X2, mark(X3)) -> if#(X1, X2, X3), if#(X1, mark(X2), X3) -> if#(X1, X2, X3)} Weak: { mark(0()) -> active(0()), mark(p(X)) -> active(p(mark(X))), mark(s(X)) -> active(s(mark(X))), mark(true()) -> active(true()), mark(leq(X1, X2)) -> active(leq(mark(X1), mark(X2))), mark(false()) -> active(false()), mark(if(X1, X2, X3)) -> active(if(mark(X1), X2, X3)), mark(diff(X1, X2)) -> active(diff(mark(X1), mark(X2))), active(p(0())) -> mark(0()), active(p(s(X))) -> mark(X), 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(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)))), p(mark(X)) -> p(X), p(active(X)) -> p(X), s(mark(X)) -> s(X), s(active(X)) -> s(X), leq(X1, mark(X2)) -> leq(X1, X2), leq(X1, active(X2)) -> leq(X1, X2), leq(mark(X1), X2) -> leq(X1, X2), leq(active(X1), X2) -> leq(X1, X2), if(X1, X2, mark(X3)) -> if(X1, X2, X3), if(X1, X2, active(X3)) -> if(X1, X2, X3), if(X1, mark(X2), X3) -> if(X1, X2, X3), if(X1, active(X2), X3) -> if(X1, X2, X3), if(mark(X1), X2, X3) -> if(X1, X2, X3), if(active(X1), X2, X3) -> if(X1, X2, X3), diff(X1, mark(X2)) -> diff(X1, X2), diff(X1, active(X2)) -> diff(X1, X2), diff(mark(X1), X2) -> diff(X1, X2), diff(active(X1), X2) -> diff(X1, X2)} SPSC: Simple Projection: pi(if#) = 2 Strict: {if#(X1, mark(X2), X3) -> if#(X1, X2, X3)} EDG: {(if#(X1, mark(X2), X3) -> if#(X1, X2, X3), if#(X1, mark(X2), X3) -> if#(X1, X2, X3))} SCCS: Scc: {if#(X1, mark(X2), X3) -> if#(X1, X2, X3)} SCC: Strict: {if#(X1, mark(X2), X3) -> if#(X1, X2, X3)} Weak: { mark(0()) -> active(0()), mark(p(X)) -> active(p(mark(X))), mark(s(X)) -> active(s(mark(X))), mark(true()) -> active(true()), mark(leq(X1, X2)) -> active(leq(mark(X1), mark(X2))), mark(false()) -> active(false()), mark(if(X1, X2, X3)) -> active(if(mark(X1), X2, X3)), mark(diff(X1, X2)) -> active(diff(mark(X1), mark(X2))), active(p(0())) -> mark(0()), active(p(s(X))) -> mark(X), 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(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)))), p(mark(X)) -> p(X), p(active(X)) -> p(X), s(mark(X)) -> s(X), s(active(X)) -> s(X), leq(X1, mark(X2)) -> leq(X1, X2), leq(X1, active(X2)) -> leq(X1, X2), leq(mark(X1), X2) -> leq(X1, X2), leq(active(X1), X2) -> leq(X1, X2), if(X1, X2, mark(X3)) -> if(X1, X2, X3), if(X1, X2, active(X3)) -> if(X1, X2, X3), if(X1, mark(X2), X3) -> if(X1, X2, X3), if(X1, active(X2), X3) -> if(X1, X2, X3), if(mark(X1), X2, X3) -> if(X1, X2, X3), if(active(X1), X2, X3) -> if(X1, X2, X3), diff(X1, mark(X2)) -> diff(X1, X2), diff(X1, active(X2)) -> diff(X1, X2), diff(mark(X1), X2) -> diff(X1, X2), diff(active(X1), X2) -> diff(X1, X2)} SPSC: Simple Projection: pi(if#) = 1 Strict: {} Qed SCC: Strict: { leq#(X1, mark(X2)) -> leq#(X1, X2), leq#(X1, active(X2)) -> leq#(X1, X2), leq#(mark(X1), X2) -> leq#(X1, X2), leq#(active(X1), X2) -> leq#(X1, X2)} Weak: { mark(0()) -> active(0()), mark(p(X)) -> active(p(mark(X))), mark(s(X)) -> active(s(mark(X))), mark(true()) -> active(true()), mark(leq(X1, X2)) -> active(leq(mark(X1), mark(X2))), mark(false()) -> active(false()), mark(if(X1, X2, X3)) -> active(if(mark(X1), X2, X3)), mark(diff(X1, X2)) -> active(diff(mark(X1), mark(X2))), active(p(0())) -> mark(0()), active(p(s(X))) -> mark(X), 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(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)))), p(mark(X)) -> p(X), p(active(X)) -> p(X), s(mark(X)) -> s(X), s(active(X)) -> s(X), leq(X1, mark(X2)) -> leq(X1, X2), leq(X1, active(X2)) -> leq(X1, X2), leq(mark(X1), X2) -> leq(X1, X2), leq(active(X1), X2) -> leq(X1, X2), if(X1, X2, mark(X3)) -> if(X1, X2, X3), if(X1, X2, active(X3)) -> if(X1, X2, X3), if(X1, mark(X2), X3) -> if(X1, X2, X3), if(X1, active(X2), X3) -> if(X1, X2, X3), if(mark(X1), X2, X3) -> if(X1, X2, X3), if(active(X1), X2, X3) -> if(X1, X2, X3), diff(X1, mark(X2)) -> diff(X1, X2), diff(X1, active(X2)) -> diff(X1, X2), diff(mark(X1), X2) -> diff(X1, X2), diff(active(X1), X2) -> diff(X1, X2)} SPSC: Simple Projection: pi(leq#) = 1 Strict: { leq#(X1, mark(X2)) -> leq#(X1, X2), leq#(mark(X1), X2) -> leq#(X1, X2), leq#(active(X1), X2) -> leq#(X1, X2)} EDG: {(leq#(mark(X1), X2) -> leq#(X1, X2), leq#(active(X1), 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#(X1, mark(X2)) -> leq#(X1, X2)) (leq#(active(X1), X2) -> leq#(X1, X2), leq#(X1, mark(X2)) -> leq#(X1, X2)) (leq#(active(X1), X2) -> leq#(X1, X2), leq#(mark(X1), X2) -> leq#(X1, X2)) (leq#(active(X1), X2) -> leq#(X1, X2), leq#(active(X1), 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#(mark(X1), X2) -> leq#(X1, X2)) (leq#(X1, mark(X2)) -> leq#(X1, X2), leq#(active(X1), X2) -> leq#(X1, X2))} SCCS: Scc: { leq#(X1, mark(X2)) -> leq#(X1, X2), leq#(mark(X1), X2) -> leq#(X1, X2), leq#(active(X1), X2) -> leq#(X1, X2)} SCC: Strict: { leq#(X1, mark(X2)) -> leq#(X1, X2), leq#(mark(X1), X2) -> leq#(X1, X2), leq#(active(X1), X2) -> leq#(X1, X2)} Weak: { mark(0()) -> active(0()), mark(p(X)) -> active(p(mark(X))), mark(s(X)) -> active(s(mark(X))), mark(true()) -> active(true()), mark(leq(X1, X2)) -> active(leq(mark(X1), mark(X2))), mark(false()) -> active(false()), mark(if(X1, X2, X3)) -> active(if(mark(X1), X2, X3)), mark(diff(X1, X2)) -> active(diff(mark(X1), mark(X2))), active(p(0())) -> mark(0()), active(p(s(X))) -> mark(X), 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(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)))), p(mark(X)) -> p(X), p(active(X)) -> p(X), s(mark(X)) -> s(X), s(active(X)) -> s(X), leq(X1, mark(X2)) -> leq(X1, X2), leq(X1, active(X2)) -> leq(X1, X2), leq(mark(X1), X2) -> leq(X1, X2), leq(active(X1), X2) -> leq(X1, X2), if(X1, X2, mark(X3)) -> if(X1, X2, X3), if(X1, X2, active(X3)) -> if(X1, X2, X3), if(X1, mark(X2), X3) -> if(X1, X2, X3), if(X1, active(X2), X3) -> if(X1, X2, X3), if(mark(X1), X2, X3) -> if(X1, X2, X3), if(active(X1), X2, X3) -> if(X1, X2, X3), diff(X1, mark(X2)) -> diff(X1, X2), diff(X1, active(X2)) -> diff(X1, X2), diff(mark(X1), X2) -> diff(X1, X2), diff(active(X1), X2) -> diff(X1, X2)} SPSC: Simple Projection: pi(leq#) = 0 Strict: {leq#(X1, mark(X2)) -> leq#(X1, X2), leq#(mark(X1), X2) -> leq#(X1, X2)} EDG: {(leq#(mark(X1), X2) -> leq#(X1, X2), leq#(mark(X1), 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#(X1, mark(X2)) -> leq#(X1, X2)) (leq#(X1, mark(X2)) -> leq#(X1, X2), leq#(mark(X1), X2) -> leq#(X1, X2))} SCCS: Scc: {leq#(X1, mark(X2)) -> leq#(X1, X2), leq#(mark(X1), X2) -> leq#(X1, X2)} SCC: Strict: {leq#(X1, mark(X2)) -> leq#(X1, X2), leq#(mark(X1), X2) -> leq#(X1, X2)} Weak: { mark(0()) -> active(0()), mark(p(X)) -> active(p(mark(X))), mark(s(X)) -> active(s(mark(X))), mark(true()) -> active(true()), mark(leq(X1, X2)) -> active(leq(mark(X1), mark(X2))), mark(false()) -> active(false()), mark(if(X1, X2, X3)) -> active(if(mark(X1), X2, X3)), mark(diff(X1, X2)) -> active(diff(mark(X1), mark(X2))), active(p(0())) -> mark(0()), active(p(s(X))) -> mark(X), 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(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)))), p(mark(X)) -> p(X), p(active(X)) -> p(X), s(mark(X)) -> s(X), s(active(X)) -> s(X), leq(X1, mark(X2)) -> leq(X1, X2), leq(X1, active(X2)) -> leq(X1, X2), leq(mark(X1), X2) -> leq(X1, X2), leq(active(X1), X2) -> leq(X1, X2), if(X1, X2, mark(X3)) -> if(X1, X2, X3), if(X1, X2, active(X3)) -> if(X1, X2, X3), if(X1, mark(X2), X3) -> if(X1, X2, X3), if(X1, active(X2), X3) -> if(X1, X2, X3), if(mark(X1), X2, X3) -> if(X1, X2, X3), if(active(X1), X2, X3) -> if(X1, X2, X3), diff(X1, mark(X2)) -> diff(X1, X2), diff(X1, active(X2)) -> diff(X1, X2), diff(mark(X1), X2) -> diff(X1, X2), diff(active(X1), X2) -> diff(X1, X2)} 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: { mark(0()) -> active(0()), mark(p(X)) -> active(p(mark(X))), mark(s(X)) -> active(s(mark(X))), mark(true()) -> active(true()), mark(leq(X1, X2)) -> active(leq(mark(X1), mark(X2))), mark(false()) -> active(false()), mark(if(X1, X2, X3)) -> active(if(mark(X1), X2, X3)), mark(diff(X1, X2)) -> active(diff(mark(X1), mark(X2))), active(p(0())) -> mark(0()), active(p(s(X))) -> mark(X), 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(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)))), p(mark(X)) -> p(X), p(active(X)) -> p(X), s(mark(X)) -> s(X), s(active(X)) -> s(X), leq(X1, mark(X2)) -> leq(X1, X2), leq(X1, active(X2)) -> leq(X1, X2), leq(mark(X1), X2) -> leq(X1, X2), leq(active(X1), X2) -> leq(X1, X2), if(X1, X2, mark(X3)) -> if(X1, X2, X3), if(X1, X2, active(X3)) -> if(X1, X2, X3), if(X1, mark(X2), X3) -> if(X1, X2, X3), if(X1, active(X2), X3) -> if(X1, X2, X3), if(mark(X1), X2, X3) -> if(X1, X2, X3), if(active(X1), X2, X3) -> if(X1, X2, X3), diff(X1, mark(X2)) -> diff(X1, X2), diff(X1, active(X2)) -> diff(X1, X2), diff(mark(X1), X2) -> diff(X1, X2), diff(active(X1), X2) -> diff(X1, X2)} SPSC: Simple Projection: pi(leq#) = 1 Strict: {} Qed SCC: Strict: { s#(mark(X)) -> s#(X), s#(active(X)) -> s#(X)} Weak: { mark(0()) -> active(0()), mark(p(X)) -> active(p(mark(X))), mark(s(X)) -> active(s(mark(X))), mark(true()) -> active(true()), mark(leq(X1, X2)) -> active(leq(mark(X1), mark(X2))), mark(false()) -> active(false()), mark(if(X1, X2, X3)) -> active(if(mark(X1), X2, X3)), mark(diff(X1, X2)) -> active(diff(mark(X1), mark(X2))), active(p(0())) -> mark(0()), active(p(s(X))) -> mark(X), 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(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)))), p(mark(X)) -> p(X), p(active(X)) -> p(X), s(mark(X)) -> s(X), s(active(X)) -> s(X), leq(X1, mark(X2)) -> leq(X1, X2), leq(X1, active(X2)) -> leq(X1, X2), leq(mark(X1), X2) -> leq(X1, X2), leq(active(X1), X2) -> leq(X1, X2), if(X1, X2, mark(X3)) -> if(X1, X2, X3), if(X1, X2, active(X3)) -> if(X1, X2, X3), if(X1, mark(X2), X3) -> if(X1, X2, X3), if(X1, active(X2), X3) -> if(X1, X2, X3), if(mark(X1), X2, X3) -> if(X1, X2, X3), if(active(X1), X2, X3) -> if(X1, X2, X3), diff(X1, mark(X2)) -> diff(X1, X2), diff(X1, active(X2)) -> diff(X1, X2), diff(mark(X1), X2) -> diff(X1, X2), diff(active(X1), X2) -> diff(X1, X2)} SPSC: Simple Projection: pi(s#) = 0 Strict: {s#(active(X)) -> s#(X)} EDG: {(s#(active(X)) -> s#(X), s#(active(X)) -> s#(X))} SCCS: Scc: {s#(active(X)) -> s#(X)} SCC: Strict: {s#(active(X)) -> s#(X)} Weak: { mark(0()) -> active(0()), mark(p(X)) -> active(p(mark(X))), mark(s(X)) -> active(s(mark(X))), mark(true()) -> active(true()), mark(leq(X1, X2)) -> active(leq(mark(X1), mark(X2))), mark(false()) -> active(false()), mark(if(X1, X2, X3)) -> active(if(mark(X1), X2, X3)), mark(diff(X1, X2)) -> active(diff(mark(X1), mark(X2))), active(p(0())) -> mark(0()), active(p(s(X))) -> mark(X), 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(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)))), p(mark(X)) -> p(X), p(active(X)) -> p(X), s(mark(X)) -> s(X), s(active(X)) -> s(X), leq(X1, mark(X2)) -> leq(X1, X2), leq(X1, active(X2)) -> leq(X1, X2), leq(mark(X1), X2) -> leq(X1, X2), leq(active(X1), X2) -> leq(X1, X2), if(X1, X2, mark(X3)) -> if(X1, X2, X3), if(X1, X2, active(X3)) -> if(X1, X2, X3), if(X1, mark(X2), X3) -> if(X1, X2, X3), if(X1, active(X2), X3) -> if(X1, X2, X3), if(mark(X1), X2, X3) -> if(X1, X2, X3), if(active(X1), X2, X3) -> if(X1, X2, X3), diff(X1, mark(X2)) -> diff(X1, X2), diff(X1, active(X2)) -> diff(X1, X2), diff(mark(X1), X2) -> diff(X1, X2), diff(active(X1), X2) -> diff(X1, X2)} SPSC: Simple Projection: pi(s#) = 0 Strict: {} Qed SCC: Strict: { p#(mark(X)) -> p#(X), p#(active(X)) -> p#(X)} Weak: { mark(0()) -> active(0()), mark(p(X)) -> active(p(mark(X))), mark(s(X)) -> active(s(mark(X))), mark(true()) -> active(true()), mark(leq(X1, X2)) -> active(leq(mark(X1), mark(X2))), mark(false()) -> active(false()), mark(if(X1, X2, X3)) -> active(if(mark(X1), X2, X3)), mark(diff(X1, X2)) -> active(diff(mark(X1), mark(X2))), active(p(0())) -> mark(0()), active(p(s(X))) -> mark(X), 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(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)))), p(mark(X)) -> p(X), p(active(X)) -> p(X), s(mark(X)) -> s(X), s(active(X)) -> s(X), leq(X1, mark(X2)) -> leq(X1, X2), leq(X1, active(X2)) -> leq(X1, X2), leq(mark(X1), X2) -> leq(X1, X2), leq(active(X1), X2) -> leq(X1, X2), if(X1, X2, mark(X3)) -> if(X1, X2, X3), if(X1, X2, active(X3)) -> if(X1, X2, X3), if(X1, mark(X2), X3) -> if(X1, X2, X3), if(X1, active(X2), X3) -> if(X1, X2, X3), if(mark(X1), X2, X3) -> if(X1, X2, X3), if(active(X1), X2, X3) -> if(X1, X2, X3), diff(X1, mark(X2)) -> diff(X1, X2), diff(X1, active(X2)) -> diff(X1, X2), diff(mark(X1), X2) -> diff(X1, X2), diff(active(X1), X2) -> diff(X1, X2)} SPSC: Simple Projection: pi(p#) = 0 Strict: {p#(active(X)) -> p#(X)} EDG: {(p#(active(X)) -> p#(X), p#(active(X)) -> p#(X))} SCCS: Scc: {p#(active(X)) -> p#(X)} SCC: Strict: {p#(active(X)) -> p#(X)} Weak: { mark(0()) -> active(0()), mark(p(X)) -> active(p(mark(X))), mark(s(X)) -> active(s(mark(X))), mark(true()) -> active(true()), mark(leq(X1, X2)) -> active(leq(mark(X1), mark(X2))), mark(false()) -> active(false()), mark(if(X1, X2, X3)) -> active(if(mark(X1), X2, X3)), mark(diff(X1, X2)) -> active(diff(mark(X1), mark(X2))), active(p(0())) -> mark(0()), active(p(s(X))) -> mark(X), 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(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)))), p(mark(X)) -> p(X), p(active(X)) -> p(X), s(mark(X)) -> s(X), s(active(X)) -> s(X), leq(X1, mark(X2)) -> leq(X1, X2), leq(X1, active(X2)) -> leq(X1, X2), leq(mark(X1), X2) -> leq(X1, X2), leq(active(X1), X2) -> leq(X1, X2), if(X1, X2, mark(X3)) -> if(X1, X2, X3), if(X1, X2, active(X3)) -> if(X1, X2, X3), if(X1, mark(X2), X3) -> if(X1, X2, X3), if(X1, active(X2), X3) -> if(X1, X2, X3), if(mark(X1), X2, X3) -> if(X1, X2, X3), if(active(X1), X2, X3) -> if(X1, X2, X3), diff(X1, mark(X2)) -> diff(X1, X2), diff(X1, active(X2)) -> diff(X1, X2), diff(mark(X1), X2) -> diff(X1, X2), diff(active(X1), X2) -> diff(X1, X2)} SPSC: Simple Projection: pi(p#) = 0 Strict: {} Qed SCC: Strict: { mark#(p(X)) -> mark#(X), mark#(p(X)) -> active#(p(mark(X))), mark#(s(X)) -> mark#(X), mark#(s(X)) -> active#(s(mark(X))), mark#(leq(X1, X2)) -> mark#(X1), mark#(leq(X1, X2)) -> mark#(X2), mark#(leq(X1, X2)) -> active#(leq(mark(X1), mark(X2))), mark#(if(X1, X2, X3)) -> mark#(X1), mark#(if(X1, X2, X3)) -> active#(if(mark(X1), X2, X3)), mark#(diff(X1, X2)) -> mark#(X1), mark#(diff(X1, X2)) -> mark#(X2), mark#(diff(X1, X2)) -> active#(diff(mark(X1), mark(X2))), active#(p(s(X))) -> mark#(X), active#(leq(s(X), s(Y))) -> mark#(leq(X, Y)), 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))))} Weak: { mark(0()) -> active(0()), mark(p(X)) -> active(p(mark(X))), mark(s(X)) -> active(s(mark(X))), mark(true()) -> active(true()), mark(leq(X1, X2)) -> active(leq(mark(X1), mark(X2))), mark(false()) -> active(false()), mark(if(X1, X2, X3)) -> active(if(mark(X1), X2, X3)), mark(diff(X1, X2)) -> active(diff(mark(X1), mark(X2))), active(p(0())) -> mark(0()), active(p(s(X))) -> mark(X), 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(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)))), p(mark(X)) -> p(X), p(active(X)) -> p(X), s(mark(X)) -> s(X), s(active(X)) -> s(X), leq(X1, mark(X2)) -> leq(X1, X2), leq(X1, active(X2)) -> leq(X1, X2), leq(mark(X1), X2) -> leq(X1, X2), leq(active(X1), X2) -> leq(X1, X2), if(X1, X2, mark(X3)) -> if(X1, X2, X3), if(X1, X2, active(X3)) -> if(X1, X2, X3), if(X1, mark(X2), X3) -> if(X1, X2, X3), if(X1, active(X2), X3) -> if(X1, X2, X3), if(mark(X1), X2, X3) -> if(X1, X2, X3), if(active(X1), X2, X3) -> if(X1, X2, X3), diff(X1, mark(X2)) -> diff(X1, X2), diff(X1, active(X2)) -> diff(X1, X2), diff(mark(X1), X2) -> diff(X1, X2), diff(active(X1), X2) -> diff(X1, X2)} POLY: Argument Filtering: pi(diff) = [], pi(if) = [], pi(false) = [], pi(leq) = [], pi(true) = [], pi(s) = [], pi(p) = [], pi(active#) = 0, pi(active) = [], pi(0) = [], pi(mark#) = [], pi(mark) = [] Usable Rules: {} Interpretation: [mark#] = 1, [if] = 1, [diff] = 1, [leq] = 1, [s] = 0, [p] = 1 Strict: { mark#(p(X)) -> mark#(X), mark#(p(X)) -> active#(p(mark(X))), mark#(s(X)) -> mark#(X), mark#(leq(X1, X2)) -> mark#(X1), mark#(leq(X1, X2)) -> mark#(X2), mark#(leq(X1, X2)) -> active#(leq(mark(X1), mark(X2))), mark#(if(X1, X2, X3)) -> mark#(X1), mark#(if(X1, X2, X3)) -> active#(if(mark(X1), X2, X3)), mark#(diff(X1, X2)) -> mark#(X1), mark#(diff(X1, X2)) -> mark#(X2), mark#(diff(X1, X2)) -> active#(diff(mark(X1), mark(X2))), active#(p(s(X))) -> mark#(X), active#(leq(s(X), s(Y))) -> mark#(leq(X, Y)), 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))))} Weak: { mark(0()) -> active(0()), mark(p(X)) -> active(p(mark(X))), mark(s(X)) -> active(s(mark(X))), mark(true()) -> active(true()), mark(leq(X1, X2)) -> active(leq(mark(X1), mark(X2))), mark(false()) -> active(false()), mark(if(X1, X2, X3)) -> active(if(mark(X1), X2, X3)), mark(diff(X1, X2)) -> active(diff(mark(X1), mark(X2))), active(p(0())) -> mark(0()), active(p(s(X))) -> mark(X), 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(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)))), p(mark(X)) -> p(X), p(active(X)) -> p(X), s(mark(X)) -> s(X), s(active(X)) -> s(X), leq(X1, mark(X2)) -> leq(X1, X2), leq(X1, active(X2)) -> leq(X1, X2), leq(mark(X1), X2) -> leq(X1, X2), leq(active(X1), X2) -> leq(X1, X2), if(X1, X2, mark(X3)) -> if(X1, X2, X3), if(X1, X2, active(X3)) -> if(X1, X2, X3), if(X1, mark(X2), X3) -> if(X1, X2, X3), if(X1, active(X2), X3) -> if(X1, X2, X3), if(mark(X1), X2, X3) -> if(X1, X2, X3), if(active(X1), X2, X3) -> if(X1, X2, X3), diff(X1, mark(X2)) -> diff(X1, X2), diff(X1, active(X2)) -> diff(X1, X2), diff(mark(X1), X2) -> diff(X1, X2), diff(active(X1), X2) -> diff(X1, X2)} EDG: { (mark#(if(X1, X2, X3)) -> active#(if(mark(X1), X2, X3)), active#(diff(X, Y)) -> mark#(if(leq(X, Y), 0(), s(diff(p(X), Y))))) (mark#(if(X1, X2, X3)) -> active#(if(mark(X1), X2, X3)), active#(if(false(), X, Y)) -> mark#(Y)) (mark#(if(X1, X2, X3)) -> active#(if(mark(X1), X2, X3)), active#(if(true(), X, Y)) -> mark#(X)) (mark#(if(X1, X2, X3)) -> active#(if(mark(X1), X2, X3)), active#(leq(s(X), s(Y))) -> mark#(leq(X, Y))) (mark#(if(X1, X2, X3)) -> active#(if(mark(X1), X2, X3)), active#(p(s(X))) -> mark#(X)) (mark#(leq(X1, X2)) -> mark#(X1), mark#(diff(X1, X2)) -> active#(diff(mark(X1), mark(X2)))) (mark#(leq(X1, X2)) -> mark#(X1), mark#(diff(X1, X2)) -> mark#(X2)) (mark#(leq(X1, X2)) -> mark#(X1), mark#(diff(X1, X2)) -> mark#(X1)) (mark#(leq(X1, X2)) -> mark#(X1), mark#(if(X1, X2, X3)) -> active#(if(mark(X1), X2, X3))) (mark#(leq(X1, X2)) -> mark#(X1), mark#(if(X1, X2, X3)) -> mark#(X1)) (mark#(leq(X1, X2)) -> mark#(X1), mark#(leq(X1, X2)) -> active#(leq(mark(X1), mark(X2)))) (mark#(leq(X1, X2)) -> mark#(X1), mark#(leq(X1, X2)) -> mark#(X2)) (mark#(leq(X1, X2)) -> mark#(X1), mark#(leq(X1, X2)) -> mark#(X1)) (mark#(leq(X1, X2)) -> mark#(X1), mark#(s(X)) -> mark#(X)) (mark#(leq(X1, X2)) -> mark#(X1), mark#(p(X)) -> active#(p(mark(X)))) (mark#(leq(X1, X2)) -> mark#(X1), mark#(p(X)) -> mark#(X)) (mark#(diff(X1, X2)) -> mark#(X1), mark#(diff(X1, X2)) -> active#(diff(mark(X1), mark(X2)))) (mark#(diff(X1, X2)) -> mark#(X1), mark#(diff(X1, X2)) -> mark#(X2)) (mark#(diff(X1, X2)) -> mark#(X1), mark#(diff(X1, X2)) -> mark#(X1)) (mark#(diff(X1, X2)) -> mark#(X1), mark#(if(X1, X2, X3)) -> active#(if(mark(X1), X2, X3))) (mark#(diff(X1, X2)) -> mark#(X1), mark#(if(X1, X2, X3)) -> mark#(X1)) (mark#(diff(X1, X2)) -> mark#(X1), mark#(leq(X1, X2)) -> active#(leq(mark(X1), mark(X2)))) (mark#(diff(X1, X2)) -> mark#(X1), mark#(leq(X1, X2)) -> mark#(X2)) (mark#(diff(X1, X2)) -> mark#(X1), mark#(leq(X1, X2)) -> mark#(X1)) (mark#(diff(X1, X2)) -> mark#(X1), mark#(s(X)) -> mark#(X)) (mark#(diff(X1, X2)) -> mark#(X1), mark#(p(X)) -> active#(p(mark(X)))) (mark#(diff(X1, X2)) -> mark#(X1), mark#(p(X)) -> mark#(X)) (active#(diff(X, Y)) -> mark#(if(leq(X, Y), 0(), s(diff(p(X), Y)))), mark#(diff(X1, X2)) -> active#(diff(mark(X1), mark(X2)))) (active#(diff(X, Y)) -> mark#(if(leq(X, Y), 0(), s(diff(p(X), Y)))), mark#(diff(X1, X2)) -> mark#(X2)) (active#(diff(X, Y)) -> mark#(if(leq(X, Y), 0(), s(diff(p(X), Y)))), mark#(diff(X1, X2)) -> mark#(X1)) (active#(diff(X, Y)) -> mark#(if(leq(X, Y), 0(), s(diff(p(X), Y)))), mark#(if(X1, X2, X3)) -> active#(if(mark(X1), X2, X3))) (active#(diff(X, Y)) -> mark#(if(leq(X, Y), 0(), s(diff(p(X), Y)))), mark#(if(X1, X2, X3)) -> mark#(X1)) (active#(diff(X, Y)) -> mark#(if(leq(X, Y), 0(), s(diff(p(X), Y)))), mark#(leq(X1, X2)) -> active#(leq(mark(X1), mark(X2)))) (active#(diff(X, Y)) -> mark#(if(leq(X, Y), 0(), s(diff(p(X), Y)))), mark#(leq(X1, X2)) -> mark#(X2)) (active#(diff(X, Y)) -> mark#(if(leq(X, Y), 0(), s(diff(p(X), Y)))), mark#(leq(X1, X2)) -> mark#(X1)) (active#(diff(X, Y)) -> mark#(if(leq(X, Y), 0(), s(diff(p(X), Y)))), mark#(s(X)) -> mark#(X)) (active#(diff(X, Y)) -> mark#(if(leq(X, Y), 0(), s(diff(p(X), Y)))), mark#(p(X)) -> active#(p(mark(X)))) (active#(diff(X, Y)) -> mark#(if(leq(X, Y), 0(), s(diff(p(X), Y)))), mark#(p(X)) -> mark#(X)) (mark#(diff(X1, X2)) -> mark#(X2), mark#(diff(X1, X2)) -> active#(diff(mark(X1), mark(X2)))) (mark#(diff(X1, X2)) -> mark#(X2), mark#(diff(X1, X2)) -> mark#(X2)) (mark#(diff(X1, X2)) -> mark#(X2), mark#(diff(X1, X2)) -> mark#(X1)) (mark#(diff(X1, X2)) -> mark#(X2), mark#(if(X1, X2, X3)) -> active#(if(mark(X1), X2, X3))) (mark#(diff(X1, X2)) -> mark#(X2), mark#(if(X1, X2, X3)) -> mark#(X1)) (mark#(diff(X1, X2)) -> mark#(X2), mark#(leq(X1, X2)) -> active#(leq(mark(X1), mark(X2)))) (mark#(diff(X1, X2)) -> mark#(X2), mark#(leq(X1, X2)) -> mark#(X2)) (mark#(diff(X1, X2)) -> mark#(X2), mark#(leq(X1, X2)) -> mark#(X1)) (mark#(diff(X1, X2)) -> mark#(X2), mark#(s(X)) -> mark#(X)) (mark#(diff(X1, X2)) -> mark#(X2), mark#(p(X)) -> active#(p(mark(X)))) (mark#(diff(X1, X2)) -> mark#(X2), mark#(p(X)) -> mark#(X)) (mark#(diff(X1, X2)) -> active#(diff(mark(X1), mark(X2))), active#(diff(X, Y)) -> mark#(if(leq(X, Y), 0(), s(diff(p(X), Y))))) (mark#(diff(X1, X2)) -> active#(diff(mark(X1), mark(X2))), active#(if(false(), X, Y)) -> mark#(Y)) (mark#(diff(X1, X2)) -> active#(diff(mark(X1), mark(X2))), active#(if(true(), X, Y)) -> mark#(X)) (mark#(diff(X1, X2)) -> active#(diff(mark(X1), mark(X2))), active#(leq(s(X), s(Y))) -> mark#(leq(X, Y))) (mark#(diff(X1, X2)) -> active#(diff(mark(X1), mark(X2))), active#(p(s(X))) -> mark#(X)) (mark#(s(X)) -> mark#(X), mark#(diff(X1, X2)) -> active#(diff(mark(X1), mark(X2)))) (mark#(s(X)) -> mark#(X), mark#(diff(X1, X2)) -> mark#(X2)) (mark#(s(X)) -> mark#(X), mark#(diff(X1, X2)) -> mark#(X1)) (mark#(s(X)) -> mark#(X), mark#(if(X1, X2, X3)) -> active#(if(mark(X1), X2, X3))) (mark#(s(X)) -> mark#(X), mark#(if(X1, X2, X3)) -> mark#(X1)) (mark#(s(X)) -> mark#(X), mark#(leq(X1, X2)) -> active#(leq(mark(X1), mark(X2)))) (mark#(s(X)) -> mark#(X), mark#(leq(X1, X2)) -> mark#(X2)) (mark#(s(X)) -> mark#(X), mark#(leq(X1, X2)) -> mark#(X1)) (mark#(s(X)) -> mark#(X), mark#(s(X)) -> mark#(X)) (mark#(s(X)) -> mark#(X), mark#(p(X)) -> active#(p(mark(X)))) (mark#(s(X)) -> mark#(X), mark#(p(X)) -> mark#(X)) (active#(if(true(), X, Y)) -> mark#(X), mark#(diff(X1, X2)) -> active#(diff(mark(X1), mark(X2)))) (active#(if(true(), X, Y)) -> mark#(X), mark#(diff(X1, X2)) -> mark#(X2)) (active#(if(true(), X, Y)) -> mark#(X), mark#(diff(X1, X2)) -> mark#(X1)) (active#(if(true(), X, Y)) -> mark#(X), mark#(if(X1, X2, X3)) -> active#(if(mark(X1), X2, X3))) (active#(if(true(), X, Y)) -> mark#(X), mark#(if(X1, X2, X3)) -> mark#(X1)) (active#(if(true(), X, Y)) -> mark#(X), mark#(leq(X1, X2)) -> active#(leq(mark(X1), mark(X2)))) (active#(if(true(), X, Y)) -> mark#(X), mark#(leq(X1, X2)) -> mark#(X2)) (active#(if(true(), X, Y)) -> mark#(X), mark#(leq(X1, X2)) -> mark#(X1)) (active#(if(true(), X, Y)) -> mark#(X), mark#(s(X)) -> mark#(X)) (active#(if(true(), X, Y)) -> mark#(X), mark#(p(X)) -> active#(p(mark(X)))) (active#(if(true(), X, Y)) -> mark#(X), mark#(p(X)) -> mark#(X)) (active#(p(s(X))) -> mark#(X), mark#(p(X)) -> mark#(X)) (active#(p(s(X))) -> mark#(X), mark#(p(X)) -> active#(p(mark(X)))) (active#(p(s(X))) -> mark#(X), mark#(s(X)) -> mark#(X)) (active#(p(s(X))) -> mark#(X), mark#(leq(X1, X2)) -> mark#(X1)) (active#(p(s(X))) -> mark#(X), mark#(leq(X1, X2)) -> mark#(X2)) (active#(p(s(X))) -> mark#(X), mark#(leq(X1, X2)) -> active#(leq(mark(X1), mark(X2)))) (active#(p(s(X))) -> mark#(X), mark#(if(X1, X2, X3)) -> mark#(X1)) (active#(p(s(X))) -> mark#(X), mark#(if(X1, X2, X3)) -> active#(if(mark(X1), X2, X3))) (active#(p(s(X))) -> mark#(X), mark#(diff(X1, X2)) -> mark#(X1)) (active#(p(s(X))) -> mark#(X), mark#(diff(X1, X2)) -> mark#(X2)) (active#(p(s(X))) -> mark#(X), mark#(diff(X1, X2)) -> active#(diff(mark(X1), mark(X2)))) (mark#(p(X)) -> mark#(X), mark#(p(X)) -> mark#(X)) (mark#(p(X)) -> mark#(X), mark#(p(X)) -> active#(p(mark(X)))) (mark#(p(X)) -> mark#(X), mark#(s(X)) -> mark#(X)) (mark#(p(X)) -> mark#(X), mark#(leq(X1, X2)) -> mark#(X1)) (mark#(p(X)) -> mark#(X), mark#(leq(X1, X2)) -> mark#(X2)) (mark#(p(X)) -> mark#(X), mark#(leq(X1, X2)) -> active#(leq(mark(X1), mark(X2)))) (mark#(p(X)) -> mark#(X), mark#(if(X1, X2, X3)) -> mark#(X1)) (mark#(p(X)) -> mark#(X), mark#(if(X1, X2, X3)) -> active#(if(mark(X1), X2, X3))) (mark#(p(X)) -> mark#(X), mark#(diff(X1, X2)) -> mark#(X1)) (mark#(p(X)) -> mark#(X), mark#(diff(X1, X2)) -> mark#(X2)) (mark#(p(X)) -> mark#(X), mark#(diff(X1, X2)) -> active#(diff(mark(X1), mark(X2)))) (mark#(leq(X1, X2)) -> active#(leq(mark(X1), mark(X2))), active#(p(s(X))) -> mark#(X)) (mark#(leq(X1, X2)) -> active#(leq(mark(X1), mark(X2))), active#(leq(s(X), s(Y))) -> mark#(leq(X, Y))) (mark#(leq(X1, X2)) -> active#(leq(mark(X1), mark(X2))), active#(if(true(), X, Y)) -> mark#(X)) (mark#(leq(X1, X2)) -> active#(leq(mark(X1), mark(X2))), active#(if(false(), X, Y)) -> mark#(Y)) (mark#(leq(X1, X2)) -> active#(leq(mark(X1), mark(X2))), active#(diff(X, Y)) -> mark#(if(leq(X, Y), 0(), s(diff(p(X), Y))))) (mark#(leq(X1, X2)) -> mark#(X2), mark#(p(X)) -> mark#(X)) (mark#(leq(X1, X2)) -> mark#(X2), mark#(p(X)) -> active#(p(mark(X)))) (mark#(leq(X1, X2)) -> mark#(X2), mark#(s(X)) -> mark#(X)) (mark#(leq(X1, X2)) -> mark#(X2), mark#(leq(X1, X2)) -> mark#(X1)) (mark#(leq(X1, X2)) -> mark#(X2), mark#(leq(X1, X2)) -> mark#(X2)) (mark#(leq(X1, X2)) -> mark#(X2), mark#(leq(X1, X2)) -> active#(leq(mark(X1), mark(X2)))) (mark#(leq(X1, X2)) -> mark#(X2), mark#(if(X1, X2, X3)) -> mark#(X1)) (mark#(leq(X1, X2)) -> mark#(X2), mark#(if(X1, X2, X3)) -> active#(if(mark(X1), X2, X3))) (mark#(leq(X1, X2)) -> mark#(X2), mark#(diff(X1, X2)) -> mark#(X1)) (mark#(leq(X1, X2)) -> mark#(X2), mark#(diff(X1, X2)) -> mark#(X2)) (mark#(leq(X1, X2)) -> mark#(X2), mark#(diff(X1, X2)) -> active#(diff(mark(X1), mark(X2)))) (mark#(p(X)) -> active#(p(mark(X))), active#(p(s(X))) -> mark#(X)) (mark#(p(X)) -> active#(p(mark(X))), active#(leq(s(X), s(Y))) -> mark#(leq(X, Y))) (mark#(p(X)) -> active#(p(mark(X))), active#(if(true(), X, Y)) -> mark#(X)) (mark#(p(X)) -> active#(p(mark(X))), active#(if(false(), X, Y)) -> mark#(Y)) (mark#(p(X)) -> active#(p(mark(X))), active#(diff(X, Y)) -> mark#(if(leq(X, Y), 0(), s(diff(p(X), Y))))) (mark#(if(X1, X2, X3)) -> mark#(X1), mark#(p(X)) -> mark#(X)) (mark#(if(X1, X2, X3)) -> mark#(X1), mark#(p(X)) -> active#(p(mark(X)))) (mark#(if(X1, X2, X3)) -> mark#(X1), mark#(s(X)) -> mark#(X)) (mark#(if(X1, X2, X3)) -> mark#(X1), mark#(leq(X1, X2)) -> mark#(X1)) (mark#(if(X1, X2, X3)) -> mark#(X1), mark#(leq(X1, X2)) -> mark#(X2)) (mark#(if(X1, X2, X3)) -> mark#(X1), mark#(leq(X1, X2)) -> active#(leq(mark(X1), mark(X2)))) (mark#(if(X1, X2, X3)) -> mark#(X1), mark#(if(X1, X2, X3)) -> mark#(X1)) (mark#(if(X1, X2, X3)) -> mark#(X1), mark#(if(X1, X2, X3)) -> active#(if(mark(X1), X2, X3))) (mark#(if(X1, X2, X3)) -> mark#(X1), mark#(diff(X1, X2)) -> mark#(X1)) (mark#(if(X1, X2, X3)) -> mark#(X1), mark#(diff(X1, X2)) -> mark#(X2)) (mark#(if(X1, X2, X3)) -> mark#(X1), mark#(diff(X1, X2)) -> active#(diff(mark(X1), mark(X2)))) (active#(leq(s(X), s(Y))) -> mark#(leq(X, Y)), mark#(p(X)) -> mark#(X)) (active#(leq(s(X), s(Y))) -> mark#(leq(X, Y)), mark#(p(X)) -> active#(p(mark(X)))) (active#(leq(s(X), s(Y))) -> mark#(leq(X, Y)), mark#(s(X)) -> mark#(X)) (active#(leq(s(X), s(Y))) -> mark#(leq(X, Y)), mark#(leq(X1, X2)) -> mark#(X1)) (active#(leq(s(X), s(Y))) -> mark#(leq(X, Y)), mark#(leq(X1, X2)) -> mark#(X2)) (active#(leq(s(X), s(Y))) -> mark#(leq(X, Y)), mark#(leq(X1, X2)) -> active#(leq(mark(X1), mark(X2)))) (active#(leq(s(X), s(Y))) -> mark#(leq(X, Y)), mark#(if(X1, X2, X3)) -> mark#(X1)) (active#(leq(s(X), s(Y))) -> mark#(leq(X, Y)), mark#(if(X1, X2, X3)) -> active#(if(mark(X1), X2, X3))) (active#(leq(s(X), s(Y))) -> mark#(leq(X, Y)), mark#(diff(X1, X2)) -> mark#(X1)) (active#(leq(s(X), s(Y))) -> mark#(leq(X, Y)), mark#(diff(X1, X2)) -> mark#(X2)) (active#(leq(s(X), s(Y))) -> mark#(leq(X, Y)), mark#(diff(X1, X2)) -> active#(diff(mark(X1), mark(X2)))) (active#(if(false(), X, Y)) -> mark#(Y), mark#(p(X)) -> mark#(X)) (active#(if(false(), X, Y)) -> mark#(Y), mark#(p(X)) -> active#(p(mark(X)))) (active#(if(false(), X, Y)) -> mark#(Y), mark#(s(X)) -> mark#(X)) (active#(if(false(), X, Y)) -> mark#(Y), mark#(leq(X1, X2)) -> mark#(X1)) (active#(if(false(), X, Y)) -> mark#(Y), mark#(leq(X1, X2)) -> mark#(X2)) (active#(if(false(), X, Y)) -> mark#(Y), mark#(leq(X1, X2)) -> active#(leq(mark(X1), mark(X2)))) (active#(if(false(), X, Y)) -> mark#(Y), mark#(if(X1, X2, X3)) -> mark#(X1)) (active#(if(false(), X, Y)) -> mark#(Y), mark#(if(X1, X2, X3)) -> active#(if(mark(X1), X2, X3))) (active#(if(false(), X, Y)) -> mark#(Y), mark#(diff(X1, X2)) -> mark#(X1)) (active#(if(false(), X, Y)) -> mark#(Y), mark#(diff(X1, X2)) -> mark#(X2)) (active#(if(false(), X, Y)) -> mark#(Y), mark#(diff(X1, X2)) -> active#(diff(mark(X1), mark(X2)))) } SCCS: Scc: { mark#(p(X)) -> mark#(X), mark#(p(X)) -> active#(p(mark(X))), mark#(s(X)) -> mark#(X), mark#(leq(X1, X2)) -> mark#(X1), mark#(leq(X1, X2)) -> mark#(X2), mark#(leq(X1, X2)) -> active#(leq(mark(X1), mark(X2))), mark#(if(X1, X2, X3)) -> mark#(X1), mark#(if(X1, X2, X3)) -> active#(if(mark(X1), X2, X3)), mark#(diff(X1, X2)) -> mark#(X1), mark#(diff(X1, X2)) -> mark#(X2), mark#(diff(X1, X2)) -> active#(diff(mark(X1), mark(X2))), active#(p(s(X))) -> mark#(X), active#(leq(s(X), s(Y))) -> mark#(leq(X, Y)), 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))))} SCC: Strict: { mark#(p(X)) -> mark#(X), mark#(p(X)) -> active#(p(mark(X))), mark#(s(X)) -> mark#(X), mark#(leq(X1, X2)) -> mark#(X1), mark#(leq(X1, X2)) -> mark#(X2), mark#(leq(X1, X2)) -> active#(leq(mark(X1), mark(X2))), mark#(if(X1, X2, X3)) -> mark#(X1), mark#(if(X1, X2, X3)) -> active#(if(mark(X1), X2, X3)), mark#(diff(X1, X2)) -> mark#(X1), mark#(diff(X1, X2)) -> mark#(X2), mark#(diff(X1, X2)) -> active#(diff(mark(X1), mark(X2))), active#(p(s(X))) -> mark#(X), active#(leq(s(X), s(Y))) -> mark#(leq(X, Y)), 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))))} Weak: { mark(0()) -> active(0()), mark(p(X)) -> active(p(mark(X))), mark(s(X)) -> active(s(mark(X))), mark(true()) -> active(true()), mark(leq(X1, X2)) -> active(leq(mark(X1), mark(X2))), mark(false()) -> active(false()), mark(if(X1, X2, X3)) -> active(if(mark(X1), X2, X3)), mark(diff(X1, X2)) -> active(diff(mark(X1), mark(X2))), active(p(0())) -> mark(0()), active(p(s(X))) -> mark(X), 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(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)))), p(mark(X)) -> p(X), p(active(X)) -> p(X), s(mark(X)) -> s(X), s(active(X)) -> s(X), leq(X1, mark(X2)) -> leq(X1, X2), leq(X1, active(X2)) -> leq(X1, X2), leq(mark(X1), X2) -> leq(X1, X2), leq(active(X1), X2) -> leq(X1, X2), if(X1, X2, mark(X3)) -> if(X1, X2, X3), if(X1, X2, active(X3)) -> if(X1, X2, X3), if(X1, mark(X2), X3) -> if(X1, X2, X3), if(X1, active(X2), X3) -> if(X1, X2, X3), if(mark(X1), X2, X3) -> if(X1, X2, X3), if(active(X1), X2, X3) -> if(X1, X2, X3), diff(X1, mark(X2)) -> diff(X1, X2), diff(X1, active(X2)) -> diff(X1, X2), diff(mark(X1), X2) -> diff(X1, X2), diff(active(X1), X2) -> diff(X1, X2)} Fail