YES TRS: { D(t()) -> s(h()), D(constant()) -> h(), D(b(x, y)) -> b(D(x), D(y)), D(c(x, y)) -> b(c(y, D(x)), c(x, D(y))), D(m(x, y)) -> m(D(x), D(y)), D(opp(x)) -> opp(D(x)), D(div(x, y)) -> m(div(D(x), y), div(c(x, D(y)), pow(y, 2()))), D(pow(x, y)) -> b(c(c(y, pow(x, m(y, 1()))), D(x)), c(c(pow(x, y), ln(x)), D(y))), D(ln(x)) -> div(D(x), x), b(x, h()) -> x, b(s(x), s(y)) -> s(s(b(x, y))), b(h(), x) -> x, b(b(x, y), z) -> b(x, b(y, z))} DP: Strict: { D#(b(x, y)) -> D#(x), D#(b(x, y)) -> D#(y), D#(b(x, y)) -> b#(D(x), D(y)), D#(c(x, y)) -> D#(x), D#(c(x, y)) -> D#(y), D#(c(x, y)) -> b#(c(y, D(x)), c(x, D(y))), D#(m(x, y)) -> D#(x), D#(m(x, y)) -> D#(y), D#(opp(x)) -> D#(x), D#(div(x, y)) -> D#(x), D#(div(x, y)) -> D#(y), D#(pow(x, y)) -> D#(x), D#(pow(x, y)) -> D#(y), D#(pow(x, y)) -> b#(c(c(y, pow(x, m(y, 1()))), D(x)), c(c(pow(x, y), ln(x)), D(y))), D#(ln(x)) -> D#(x), b#(s(x), s(y)) -> b#(x, y), b#(b(x, y), z) -> b#(x, b(y, z)), b#(b(x, y), z) -> b#(y, z)} Weak: { D(t()) -> s(h()), D(constant()) -> h(), D(b(x, y)) -> b(D(x), D(y)), D(c(x, y)) -> b(c(y, D(x)), c(x, D(y))), D(m(x, y)) -> m(D(x), D(y)), D(opp(x)) -> opp(D(x)), D(div(x, y)) -> m(div(D(x), y), div(c(x, D(y)), pow(y, 2()))), D(pow(x, y)) -> b(c(c(y, pow(x, m(y, 1()))), D(x)), c(c(pow(x, y), ln(x)), D(y))), D(ln(x)) -> div(D(x), x), b(x, h()) -> x, b(s(x), s(y)) -> s(s(b(x, y))), b(h(), x) -> x, b(b(x, y), z) -> b(x, b(y, z))} EDG: {(D#(b(x, y)) -> b#(D(x), D(y)), b#(b(x, y), z) -> b#(y, z)) (D#(b(x, y)) -> b#(D(x), D(y)), b#(b(x, y), z) -> b#(x, b(y, z))) (D#(b(x, y)) -> b#(D(x), D(y)), b#(s(x), s(y)) -> b#(x, y)) (D#(c(x, y)) -> D#(y), D#(ln(x)) -> D#(x)) (D#(c(x, y)) -> D#(y), D#(pow(x, y)) -> b#(c(c(y, pow(x, m(y, 1()))), D(x)), c(c(pow(x, y), ln(x)), D(y)))) (D#(c(x, y)) -> D#(y), D#(pow(x, y)) -> D#(y)) (D#(c(x, y)) -> D#(y), D#(pow(x, y)) -> D#(x)) (D#(c(x, y)) -> D#(y), D#(div(x, y)) -> D#(y)) (D#(c(x, y)) -> D#(y), D#(div(x, y)) -> D#(x)) (D#(c(x, y)) -> D#(y), D#(opp(x)) -> D#(x)) (D#(c(x, y)) -> D#(y), D#(m(x, y)) -> D#(y)) (D#(c(x, y)) -> D#(y), D#(m(x, y)) -> D#(x)) (D#(c(x, y)) -> D#(y), D#(c(x, y)) -> b#(c(y, D(x)), c(x, D(y)))) (D#(c(x, y)) -> D#(y), D#(c(x, y)) -> D#(y)) (D#(c(x, y)) -> D#(y), D#(c(x, y)) -> D#(x)) (D#(c(x, y)) -> D#(y), D#(b(x, y)) -> b#(D(x), D(y))) (D#(c(x, y)) -> D#(y), D#(b(x, y)) -> D#(y)) (D#(c(x, y)) -> D#(y), D#(b(x, y)) -> D#(x)) (D#(div(x, y)) -> D#(y), D#(ln(x)) -> D#(x)) (D#(div(x, y)) -> D#(y), D#(pow(x, y)) -> b#(c(c(y, pow(x, m(y, 1()))), D(x)), c(c(pow(x, y), ln(x)), D(y)))) (D#(div(x, y)) -> D#(y), D#(pow(x, y)) -> D#(y)) (D#(div(x, y)) -> D#(y), D#(pow(x, y)) -> D#(x)) (D#(div(x, y)) -> D#(y), D#(div(x, y)) -> D#(y)) (D#(div(x, y)) -> D#(y), D#(div(x, y)) -> D#(x)) (D#(div(x, y)) -> D#(y), D#(opp(x)) -> D#(x)) (D#(div(x, y)) -> D#(y), D#(m(x, y)) -> D#(y)) (D#(div(x, y)) -> D#(y), D#(m(x, y)) -> D#(x)) (D#(div(x, y)) -> D#(y), D#(c(x, y)) -> b#(c(y, D(x)), c(x, D(y)))) (D#(div(x, y)) -> D#(y), D#(c(x, y)) -> D#(y)) (D#(div(x, y)) -> D#(y), D#(c(x, y)) -> D#(x)) (D#(div(x, y)) -> D#(y), D#(b(x, y)) -> b#(D(x), D(y))) (D#(div(x, y)) -> D#(y), D#(b(x, y)) -> D#(y)) (D#(div(x, y)) -> D#(y), D#(b(x, y)) -> D#(x)) (b#(b(x, y), z) -> b#(y, z), b#(b(x, y), z) -> b#(y, z)) (b#(b(x, y), z) -> b#(y, z), b#(b(x, y), z) -> b#(x, b(y, z))) (b#(b(x, y), z) -> b#(y, z), b#(s(x), s(y)) -> b#(x, y)) (D#(b(x, y)) -> D#(x), D#(ln(x)) -> D#(x)) (D#(b(x, y)) -> D#(x), D#(pow(x, y)) -> b#(c(c(y, pow(x, m(y, 1()))), D(x)), c(c(pow(x, y), ln(x)), D(y)))) (D#(b(x, y)) -> D#(x), D#(pow(x, y)) -> D#(y)) (D#(b(x, y)) -> D#(x), D#(pow(x, y)) -> D#(x)) (D#(b(x, y)) -> D#(x), D#(div(x, y)) -> D#(y)) (D#(b(x, y)) -> D#(x), D#(div(x, y)) -> D#(x)) (D#(b(x, y)) -> D#(x), D#(opp(x)) -> D#(x)) (D#(b(x, y)) -> D#(x), D#(m(x, y)) -> D#(y)) (D#(b(x, y)) -> D#(x), D#(m(x, y)) -> D#(x)) (D#(b(x, y)) -> D#(x), D#(c(x, y)) -> b#(c(y, D(x)), c(x, D(y)))) (D#(b(x, y)) -> D#(x), D#(c(x, y)) -> D#(y)) (D#(b(x, y)) -> D#(x), D#(c(x, y)) -> D#(x)) (D#(b(x, y)) -> D#(x), D#(b(x, y)) -> b#(D(x), D(y))) (D#(b(x, y)) -> D#(x), D#(b(x, y)) -> D#(y)) (D#(b(x, y)) -> D#(x), D#(b(x, y)) -> D#(x)) (D#(m(x, y)) -> D#(x), D#(ln(x)) -> D#(x)) (D#(m(x, y)) -> D#(x), D#(pow(x, y)) -> b#(c(c(y, pow(x, m(y, 1()))), D(x)), c(c(pow(x, y), ln(x)), D(y)))) (D#(m(x, y)) -> D#(x), D#(pow(x, y)) -> D#(y)) (D#(m(x, y)) -> D#(x), D#(pow(x, y)) -> D#(x)) (D#(m(x, y)) -> D#(x), D#(div(x, y)) -> D#(y)) (D#(m(x, y)) -> D#(x), D#(div(x, y)) -> D#(x)) (D#(m(x, y)) -> D#(x), D#(opp(x)) -> D#(x)) (D#(m(x, y)) -> D#(x), D#(m(x, y)) -> D#(y)) (D#(m(x, y)) -> D#(x), D#(m(x, y)) -> D#(x)) (D#(m(x, y)) -> D#(x), D#(c(x, y)) -> b#(c(y, D(x)), c(x, D(y)))) (D#(m(x, y)) -> D#(x), D#(c(x, y)) -> D#(y)) (D#(m(x, y)) -> D#(x), D#(c(x, y)) -> D#(x)) (D#(m(x, y)) -> D#(x), D#(b(x, y)) -> b#(D(x), D(y))) (D#(m(x, y)) -> D#(x), D#(b(x, y)) -> D#(y)) (D#(m(x, y)) -> D#(x), D#(b(x, y)) -> D#(x)) (D#(div(x, y)) -> D#(x), D#(ln(x)) -> D#(x)) (D#(div(x, y)) -> D#(x), D#(pow(x, y)) -> b#(c(c(y, pow(x, m(y, 1()))), D(x)), c(c(pow(x, y), ln(x)), D(y)))) (D#(div(x, y)) -> D#(x), D#(pow(x, y)) -> D#(y)) (D#(div(x, y)) -> D#(x), D#(pow(x, y)) -> D#(x)) (D#(div(x, y)) -> D#(x), D#(div(x, y)) -> D#(y)) (D#(div(x, y)) -> D#(x), D#(div(x, y)) -> D#(x)) (D#(div(x, y)) -> D#(x), D#(opp(x)) -> D#(x)) (D#(div(x, y)) -> D#(x), D#(m(x, y)) -> D#(y)) (D#(div(x, y)) -> D#(x), D#(m(x, y)) -> D#(x)) (D#(div(x, y)) -> D#(x), D#(c(x, y)) -> b#(c(y, D(x)), c(x, D(y)))) (D#(div(x, y)) -> D#(x), D#(c(x, y)) -> D#(y)) (D#(div(x, y)) -> D#(x), D#(c(x, y)) -> D#(x)) (D#(div(x, y)) -> D#(x), D#(b(x, y)) -> b#(D(x), D(y))) (D#(div(x, y)) -> D#(x), D#(b(x, y)) -> D#(y)) (D#(div(x, y)) -> D#(x), D#(b(x, y)) -> D#(x)) (D#(ln(x)) -> D#(x), D#(ln(x)) -> D#(x)) (D#(ln(x)) -> D#(x), D#(pow(x, y)) -> b#(c(c(y, pow(x, m(y, 1()))), D(x)), c(c(pow(x, y), ln(x)), D(y)))) (D#(ln(x)) -> D#(x), D#(pow(x, y)) -> D#(y)) (D#(ln(x)) -> D#(x), D#(pow(x, y)) -> D#(x)) (D#(ln(x)) -> D#(x), D#(div(x, y)) -> D#(y)) (D#(ln(x)) -> D#(x), D#(div(x, y)) -> D#(x)) (D#(ln(x)) -> D#(x), D#(opp(x)) -> D#(x)) (D#(ln(x)) -> D#(x), D#(m(x, y)) -> D#(y)) (D#(ln(x)) -> D#(x), D#(m(x, y)) -> D#(x)) (D#(ln(x)) -> D#(x), D#(c(x, y)) -> b#(c(y, D(x)), c(x, D(y)))) (D#(ln(x)) -> D#(x), D#(c(x, y)) -> D#(y)) (D#(ln(x)) -> D#(x), D#(c(x, y)) -> D#(x)) (D#(ln(x)) -> D#(x), D#(b(x, y)) -> b#(D(x), D(y))) (D#(ln(x)) -> D#(x), D#(b(x, y)) -> D#(y)) (D#(ln(x)) -> D#(x), D#(b(x, y)) -> D#(x)) (D#(pow(x, y)) -> D#(x), D#(b(x, y)) -> D#(x)) (D#(pow(x, y)) -> D#(x), D#(b(x, y)) -> D#(y)) (D#(pow(x, y)) -> D#(x), D#(b(x, y)) -> b#(D(x), D(y))) (D#(pow(x, y)) -> D#(x), D#(c(x, y)) -> D#(x)) (D#(pow(x, y)) -> D#(x), D#(c(x, y)) -> D#(y)) (D#(pow(x, y)) -> D#(x), D#(c(x, y)) -> b#(c(y, D(x)), c(x, D(y)))) (D#(pow(x, y)) -> D#(x), D#(m(x, y)) -> D#(x)) (D#(pow(x, y)) -> D#(x), D#(m(x, y)) -> D#(y)) (D#(pow(x, y)) -> D#(x), D#(opp(x)) -> D#(x)) (D#(pow(x, y)) -> D#(x), D#(div(x, y)) -> D#(x)) (D#(pow(x, y)) -> D#(x), D#(div(x, y)) -> D#(y)) (D#(pow(x, y)) -> D#(x), D#(pow(x, y)) -> D#(x)) (D#(pow(x, y)) -> D#(x), D#(pow(x, y)) -> D#(y)) (D#(pow(x, y)) -> D#(x), D#(pow(x, y)) -> b#(c(c(y, pow(x, m(y, 1()))), D(x)), c(c(pow(x, y), ln(x)), D(y)))) (D#(pow(x, y)) -> D#(x), D#(ln(x)) -> D#(x)) (D#(opp(x)) -> D#(x), D#(b(x, y)) -> D#(x)) (D#(opp(x)) -> D#(x), D#(b(x, y)) -> D#(y)) (D#(opp(x)) -> D#(x), D#(b(x, y)) -> b#(D(x), D(y))) (D#(opp(x)) -> D#(x), D#(c(x, y)) -> D#(x)) (D#(opp(x)) -> D#(x), D#(c(x, y)) -> D#(y)) (D#(opp(x)) -> D#(x), D#(c(x, y)) -> b#(c(y, D(x)), c(x, D(y)))) (D#(opp(x)) -> D#(x), D#(m(x, y)) -> D#(x)) (D#(opp(x)) -> D#(x), D#(m(x, y)) -> D#(y)) (D#(opp(x)) -> D#(x), D#(opp(x)) -> D#(x)) (D#(opp(x)) -> D#(x), D#(div(x, y)) -> D#(x)) (D#(opp(x)) -> D#(x), D#(div(x, y)) -> D#(y)) (D#(opp(x)) -> D#(x), D#(pow(x, y)) -> D#(x)) (D#(opp(x)) -> D#(x), D#(pow(x, y)) -> D#(y)) (D#(opp(x)) -> D#(x), D#(pow(x, y)) -> b#(c(c(y, pow(x, m(y, 1()))), D(x)), c(c(pow(x, y), ln(x)), D(y)))) (D#(opp(x)) -> D#(x), D#(ln(x)) -> D#(x)) (D#(c(x, y)) -> D#(x), D#(b(x, y)) -> D#(x)) (D#(c(x, y)) -> D#(x), D#(b(x, y)) -> D#(y)) (D#(c(x, y)) -> D#(x), D#(b(x, y)) -> b#(D(x), D(y))) (D#(c(x, y)) -> D#(x), D#(c(x, y)) -> D#(x)) (D#(c(x, y)) -> D#(x), D#(c(x, y)) -> D#(y)) (D#(c(x, y)) -> D#(x), D#(c(x, y)) -> b#(c(y, D(x)), c(x, D(y)))) (D#(c(x, y)) -> D#(x), D#(m(x, y)) -> D#(x)) (D#(c(x, y)) -> D#(x), D#(m(x, y)) -> D#(y)) (D#(c(x, y)) -> D#(x), D#(opp(x)) -> D#(x)) (D#(c(x, y)) -> D#(x), D#(div(x, y)) -> D#(x)) (D#(c(x, y)) -> D#(x), D#(div(x, y)) -> D#(y)) (D#(c(x, y)) -> D#(x), D#(pow(x, y)) -> D#(x)) (D#(c(x, y)) -> D#(x), D#(pow(x, y)) -> D#(y)) (D#(c(x, y)) -> D#(x), D#(pow(x, y)) -> b#(c(c(y, pow(x, m(y, 1()))), D(x)), c(c(pow(x, y), ln(x)), D(y)))) (D#(c(x, y)) -> D#(x), D#(ln(x)) -> D#(x)) (b#(s(x), s(y)) -> b#(x, y), b#(s(x), s(y)) -> b#(x, y)) (b#(s(x), s(y)) -> b#(x, y), b#(b(x, y), z) -> b#(x, b(y, z))) (b#(s(x), s(y)) -> b#(x, y), b#(b(x, y), z) -> b#(y, z)) (D#(pow(x, y)) -> D#(y), D#(b(x, y)) -> D#(x)) (D#(pow(x, y)) -> D#(y), D#(b(x, y)) -> D#(y)) (D#(pow(x, y)) -> D#(y), D#(b(x, y)) -> b#(D(x), D(y))) (D#(pow(x, y)) -> D#(y), D#(c(x, y)) -> D#(x)) (D#(pow(x, y)) -> D#(y), D#(c(x, y)) -> D#(y)) (D#(pow(x, y)) -> D#(y), D#(c(x, y)) -> b#(c(y, D(x)), c(x, D(y)))) (D#(pow(x, y)) -> D#(y), D#(m(x, y)) -> D#(x)) (D#(pow(x, y)) -> D#(y), D#(m(x, y)) -> D#(y)) (D#(pow(x, y)) -> D#(y), D#(opp(x)) -> D#(x)) (D#(pow(x, y)) -> D#(y), D#(div(x, y)) -> D#(x)) (D#(pow(x, y)) -> D#(y), D#(div(x, y)) -> D#(y)) (D#(pow(x, y)) -> D#(y), D#(pow(x, y)) -> D#(x)) (D#(pow(x, y)) -> D#(y), D#(pow(x, y)) -> D#(y)) (D#(pow(x, y)) -> D#(y), D#(pow(x, y)) -> b#(c(c(y, pow(x, m(y, 1()))), D(x)), c(c(pow(x, y), ln(x)), D(y)))) (D#(pow(x, y)) -> D#(y), D#(ln(x)) -> D#(x)) (D#(m(x, y)) -> D#(y), D#(b(x, y)) -> D#(x)) (D#(m(x, y)) -> D#(y), D#(b(x, y)) -> D#(y)) (D#(m(x, y)) -> D#(y), D#(b(x, y)) -> b#(D(x), D(y))) (D#(m(x, y)) -> D#(y), D#(c(x, y)) -> D#(x)) (D#(m(x, y)) -> D#(y), D#(c(x, y)) -> D#(y)) (D#(m(x, y)) -> D#(y), D#(c(x, y)) -> b#(c(y, D(x)), c(x, D(y)))) (D#(m(x, y)) -> D#(y), D#(m(x, y)) -> D#(x)) (D#(m(x, y)) -> D#(y), D#(m(x, y)) -> D#(y)) (D#(m(x, y)) -> D#(y), D#(opp(x)) -> D#(x)) (D#(m(x, y)) -> D#(y), D#(div(x, y)) -> D#(x)) (D#(m(x, y)) -> D#(y), D#(div(x, y)) -> D#(y)) (D#(m(x, y)) -> D#(y), D#(pow(x, y)) -> D#(x)) (D#(m(x, y)) -> D#(y), D#(pow(x, y)) -> D#(y)) (D#(m(x, y)) -> D#(y), D#(pow(x, y)) -> b#(c(c(y, pow(x, m(y, 1()))), D(x)), c(c(pow(x, y), ln(x)), D(y)))) (D#(m(x, y)) -> D#(y), D#(ln(x)) -> D#(x)) (D#(b(x, y)) -> D#(y), D#(b(x, y)) -> D#(x)) (D#(b(x, y)) -> D#(y), D#(b(x, y)) -> D#(y)) (D#(b(x, y)) -> D#(y), D#(b(x, y)) -> b#(D(x), D(y))) (D#(b(x, y)) -> D#(y), D#(c(x, y)) -> D#(x)) (D#(b(x, y)) -> D#(y), D#(c(x, y)) -> D#(y)) (D#(b(x, y)) -> D#(y), D#(c(x, y)) -> b#(c(y, D(x)), c(x, D(y)))) (D#(b(x, y)) -> D#(y), D#(m(x, y)) -> D#(x)) (D#(b(x, y)) -> D#(y), D#(m(x, y)) -> D#(y)) (D#(b(x, y)) -> D#(y), D#(opp(x)) -> D#(x)) (D#(b(x, y)) -> D#(y), D#(div(x, y)) -> D#(x)) (D#(b(x, y)) -> D#(y), D#(div(x, y)) -> D#(y)) (D#(b(x, y)) -> D#(y), D#(pow(x, y)) -> D#(x)) (D#(b(x, y)) -> D#(y), D#(pow(x, y)) -> D#(y)) (D#(b(x, y)) -> D#(y), D#(pow(x, y)) -> b#(c(c(y, pow(x, m(y, 1()))), D(x)), c(c(pow(x, y), ln(x)), D(y)))) (D#(b(x, y)) -> D#(y), D#(ln(x)) -> D#(x)) (b#(b(x, y), z) -> b#(x, b(y, z)), b#(s(x), s(y)) -> b#(x, y)) (b#(b(x, y), z) -> b#(x, b(y, z)), b#(b(x, y), z) -> b#(x, b(y, z))) (b#(b(x, y), z) -> b#(x, b(y, z)), b#(b(x, y), z) -> b#(y, z))} SCCS: Scc: {b#(s(x), s(y)) -> b#(x, y), b#(b(x, y), z) -> b#(x, b(y, z)), b#(b(x, y), z) -> b#(y, z)} Scc: { D#(b(x, y)) -> D#(x), D#(b(x, y)) -> D#(y), D#(c(x, y)) -> D#(x), D#(c(x, y)) -> D#(y), D#(m(x, y)) -> D#(x), D#(m(x, y)) -> D#(y), D#(opp(x)) -> D#(x), D#(div(x, y)) -> D#(x), D#(div(x, y)) -> D#(y), D#(pow(x, y)) -> D#(x), D#(pow(x, y)) -> D#(y), D#(ln(x)) -> D#(x)} SCC: Strict: {b#(s(x), s(y)) -> b#(x, y), b#(b(x, y), z) -> b#(x, b(y, z)), b#(b(x, y), z) -> b#(y, z)} Weak: { D(t()) -> s(h()), D(constant()) -> h(), D(b(x, y)) -> b(D(x), D(y)), D(c(x, y)) -> b(c(y, D(x)), c(x, D(y))), D(m(x, y)) -> m(D(x), D(y)), D(opp(x)) -> opp(D(x)), D(div(x, y)) -> m(div(D(x), y), div(c(x, D(y)), pow(y, 2()))), D(pow(x, y)) -> b(c(c(y, pow(x, m(y, 1()))), D(x)), c(c(pow(x, y), ln(x)), D(y))), D(ln(x)) -> div(D(x), x), b(x, h()) -> x, b(s(x), s(y)) -> s(s(b(x, y))), b(h(), x) -> x, b(b(x, y), z) -> b(x, b(y, z))} SPSC: Simple Projection: pi(b#) = 0 Strict: {b#(s(x), s(y)) -> b#(x, y), b#(b(x, y), z) -> b#(y, z)} EDG: {(b#(s(x), s(y)) -> b#(x, y), b#(b(x, y), z) -> b#(y, z)) (b#(s(x), s(y)) -> b#(x, y), b#(s(x), s(y)) -> b#(x, y)) (b#(b(x, y), z) -> b#(y, z), b#(s(x), s(y)) -> b#(x, y)) (b#(b(x, y), z) -> b#(y, z), b#(b(x, y), z) -> b#(y, z))} SCCS: Scc: {b#(s(x), s(y)) -> b#(x, y), b#(b(x, y), z) -> b#(y, z)} SCC: Strict: {b#(s(x), s(y)) -> b#(x, y), b#(b(x, y), z) -> b#(y, z)} Weak: { D(t()) -> s(h()), D(constant()) -> h(), D(b(x, y)) -> b(D(x), D(y)), D(c(x, y)) -> b(c(y, D(x)), c(x, D(y))), D(m(x, y)) -> m(D(x), D(y)), D(opp(x)) -> opp(D(x)), D(div(x, y)) -> m(div(D(x), y), div(c(x, D(y)), pow(y, 2()))), D(pow(x, y)) -> b(c(c(y, pow(x, m(y, 1()))), D(x)), c(c(pow(x, y), ln(x)), D(y))), D(ln(x)) -> div(D(x), x), b(x, h()) -> x, b(s(x), s(y)) -> s(s(b(x, y))), b(h(), x) -> x, b(b(x, y), z) -> b(x, b(y, z))} SPSC: Simple Projection: pi(b#) = 0 Strict: {b#(s(x), s(y)) -> b#(x, y)} EDG: {(b#(s(x), s(y)) -> b#(x, y), b#(s(x), s(y)) -> b#(x, y))} SCCS: Scc: {b#(s(x), s(y)) -> b#(x, y)} SCC: Strict: {b#(s(x), s(y)) -> b#(x, y)} Weak: { D(t()) -> s(h()), D(constant()) -> h(), D(b(x, y)) -> b(D(x), D(y)), D(c(x, y)) -> b(c(y, D(x)), c(x, D(y))), D(m(x, y)) -> m(D(x), D(y)), D(opp(x)) -> opp(D(x)), D(div(x, y)) -> m(div(D(x), y), div(c(x, D(y)), pow(y, 2()))), D(pow(x, y)) -> b(c(c(y, pow(x, m(y, 1()))), D(x)), c(c(pow(x, y), ln(x)), D(y))), D(ln(x)) -> div(D(x), x), b(x, h()) -> x, b(s(x), s(y)) -> s(s(b(x, y))), b(h(), x) -> x, b(b(x, y), z) -> b(x, b(y, z))} SPSC: Simple Projection: pi(b#) = 0 Strict: {} Qed SCC: Strict: { D#(b(x, y)) -> D#(x), D#(b(x, y)) -> D#(y), D#(c(x, y)) -> D#(x), D#(c(x, y)) -> D#(y), D#(m(x, y)) -> D#(x), D#(m(x, y)) -> D#(y), D#(opp(x)) -> D#(x), D#(div(x, y)) -> D#(x), D#(div(x, y)) -> D#(y), D#(pow(x, y)) -> D#(x), D#(pow(x, y)) -> D#(y), D#(ln(x)) -> D#(x)} Weak: { D(t()) -> s(h()), D(constant()) -> h(), D(b(x, y)) -> b(D(x), D(y)), D(c(x, y)) -> b(c(y, D(x)), c(x, D(y))), D(m(x, y)) -> m(D(x), D(y)), D(opp(x)) -> opp(D(x)), D(div(x, y)) -> m(div(D(x), y), div(c(x, D(y)), pow(y, 2()))), D(pow(x, y)) -> b(c(c(y, pow(x, m(y, 1()))), D(x)), c(c(pow(x, y), ln(x)), D(y))), D(ln(x)) -> div(D(x), x), b(x, h()) -> x, b(s(x), s(y)) -> s(s(b(x, y))), b(h(), x) -> x, b(b(x, y), z) -> b(x, b(y, z))} SPSC: Simple Projection: pi(D#) = 0 Strict: { D#(b(x, y)) -> D#(x), D#(b(x, y)) -> D#(y), D#(c(x, y)) -> D#(x), D#(c(x, y)) -> D#(y), D#(m(x, y)) -> D#(x), D#(m(x, y)) -> D#(y), D#(div(x, y)) -> D#(x), D#(div(x, y)) -> D#(y), D#(pow(x, y)) -> D#(x), D#(pow(x, y)) -> D#(y), D#(ln(x)) -> D#(x)} EDG: {(D#(c(x, y)) -> D#(x), D#(ln(x)) -> D#(x)) (D#(c(x, y)) -> D#(x), D#(pow(x, y)) -> D#(y)) (D#(c(x, y)) -> D#(x), D#(pow(x, y)) -> D#(x)) (D#(c(x, y)) -> D#(x), D#(div(x, y)) -> D#(y)) (D#(c(x, y)) -> D#(x), D#(div(x, y)) -> D#(x)) (D#(c(x, y)) -> D#(x), D#(m(x, y)) -> D#(y)) (D#(c(x, y)) -> D#(x), D#(m(x, y)) -> D#(x)) (D#(c(x, y)) -> D#(x), D#(c(x, y)) -> D#(y)) (D#(c(x, y)) -> D#(x), D#(c(x, y)) -> D#(x)) (D#(c(x, y)) -> D#(x), D#(b(x, y)) -> D#(y)) (D#(c(x, y)) -> D#(x), D#(b(x, y)) -> D#(x)) (D#(div(x, y)) -> D#(x), D#(ln(x)) -> D#(x)) (D#(div(x, y)) -> D#(x), D#(pow(x, y)) -> D#(y)) (D#(div(x, y)) -> D#(x), D#(pow(x, y)) -> D#(x)) (D#(div(x, y)) -> D#(x), D#(div(x, y)) -> D#(y)) (D#(div(x, y)) -> D#(x), D#(div(x, y)) -> D#(x)) (D#(div(x, y)) -> D#(x), D#(m(x, y)) -> D#(y)) (D#(div(x, y)) -> D#(x), D#(m(x, y)) -> D#(x)) (D#(div(x, y)) -> D#(x), D#(c(x, y)) -> D#(y)) (D#(div(x, y)) -> D#(x), D#(c(x, y)) -> D#(x)) (D#(div(x, y)) -> D#(x), D#(b(x, y)) -> D#(y)) (D#(div(x, y)) -> D#(x), D#(b(x, y)) -> D#(x)) (D#(ln(x)) -> D#(x), D#(ln(x)) -> D#(x)) (D#(ln(x)) -> D#(x), D#(pow(x, y)) -> D#(y)) (D#(ln(x)) -> D#(x), D#(pow(x, y)) -> D#(x)) (D#(ln(x)) -> D#(x), D#(div(x, y)) -> D#(y)) (D#(ln(x)) -> D#(x), D#(div(x, y)) -> D#(x)) (D#(ln(x)) -> D#(x), D#(m(x, y)) -> D#(y)) (D#(ln(x)) -> D#(x), D#(m(x, y)) -> D#(x)) (D#(ln(x)) -> D#(x), D#(c(x, y)) -> D#(y)) (D#(ln(x)) -> D#(x), D#(c(x, y)) -> D#(x)) (D#(ln(x)) -> D#(x), D#(b(x, y)) -> D#(y)) (D#(ln(x)) -> D#(x), D#(b(x, y)) -> D#(x)) (D#(c(x, y)) -> D#(y), D#(ln(x)) -> D#(x)) (D#(c(x, y)) -> D#(y), D#(pow(x, y)) -> D#(y)) (D#(c(x, y)) -> D#(y), D#(pow(x, y)) -> D#(x)) (D#(c(x, y)) -> D#(y), D#(div(x, y)) -> D#(y)) (D#(c(x, y)) -> D#(y), D#(div(x, y)) -> D#(x)) (D#(c(x, y)) -> D#(y), D#(m(x, y)) -> D#(y)) (D#(c(x, y)) -> D#(y), D#(m(x, y)) -> D#(x)) (D#(c(x, y)) -> D#(y), D#(c(x, y)) -> D#(y)) (D#(c(x, y)) -> D#(y), D#(c(x, y)) -> D#(x)) (D#(c(x, y)) -> D#(y), D#(b(x, y)) -> D#(y)) (D#(c(x, y)) -> D#(y), D#(b(x, y)) -> D#(x)) (D#(div(x, y)) -> D#(y), D#(ln(x)) -> D#(x)) (D#(div(x, y)) -> D#(y), D#(pow(x, y)) -> D#(y)) (D#(div(x, y)) -> D#(y), D#(pow(x, y)) -> D#(x)) (D#(div(x, y)) -> D#(y), D#(div(x, y)) -> D#(y)) (D#(div(x, y)) -> D#(y), D#(div(x, y)) -> D#(x)) (D#(div(x, y)) -> D#(y), D#(m(x, y)) -> D#(y)) (D#(div(x, y)) -> D#(y), D#(m(x, y)) -> D#(x)) (D#(div(x, y)) -> D#(y), D#(c(x, y)) -> D#(y)) (D#(div(x, y)) -> D#(y), D#(c(x, y)) -> D#(x)) (D#(div(x, y)) -> D#(y), D#(b(x, y)) -> D#(y)) (D#(div(x, y)) -> D#(y), D#(b(x, y)) -> D#(x)) (D#(pow(x, y)) -> D#(y), D#(b(x, y)) -> D#(x)) (D#(pow(x, y)) -> D#(y), D#(b(x, y)) -> D#(y)) (D#(pow(x, y)) -> D#(y), D#(c(x, y)) -> D#(x)) (D#(pow(x, y)) -> D#(y), D#(c(x, y)) -> D#(y)) (D#(pow(x, y)) -> D#(y), D#(m(x, y)) -> D#(x)) (D#(pow(x, y)) -> D#(y), D#(m(x, y)) -> D#(y)) (D#(pow(x, y)) -> D#(y), D#(div(x, y)) -> D#(x)) (D#(pow(x, y)) -> D#(y), D#(div(x, y)) -> D#(y)) (D#(pow(x, y)) -> D#(y), D#(pow(x, y)) -> D#(x)) (D#(pow(x, y)) -> D#(y), D#(pow(x, y)) -> D#(y)) (D#(pow(x, y)) -> D#(y), D#(ln(x)) -> D#(x)) (D#(m(x, y)) -> D#(y), D#(b(x, y)) -> D#(x)) (D#(m(x, y)) -> D#(y), D#(b(x, y)) -> D#(y)) (D#(m(x, y)) -> D#(y), D#(c(x, y)) -> D#(x)) (D#(m(x, y)) -> D#(y), D#(c(x, y)) -> D#(y)) (D#(m(x, y)) -> D#(y), D#(m(x, y)) -> D#(x)) (D#(m(x, y)) -> D#(y), D#(m(x, y)) -> D#(y)) (D#(m(x, y)) -> D#(y), D#(div(x, y)) -> D#(x)) (D#(m(x, y)) -> D#(y), D#(div(x, y)) -> D#(y)) (D#(m(x, y)) -> D#(y), D#(pow(x, y)) -> D#(x)) (D#(m(x, y)) -> D#(y), D#(pow(x, y)) -> D#(y)) (D#(m(x, y)) -> D#(y), D#(ln(x)) -> D#(x)) (D#(b(x, y)) -> D#(y), D#(b(x, y)) -> D#(x)) (D#(b(x, y)) -> D#(y), D#(b(x, y)) -> D#(y)) (D#(b(x, y)) -> D#(y), D#(c(x, y)) -> D#(x)) (D#(b(x, y)) -> D#(y), D#(c(x, y)) -> D#(y)) (D#(b(x, y)) -> D#(y), D#(m(x, y)) -> D#(x)) (D#(b(x, y)) -> D#(y), D#(m(x, y)) -> D#(y)) (D#(b(x, y)) -> D#(y), D#(div(x, y)) -> D#(x)) (D#(b(x, y)) -> D#(y), D#(div(x, y)) -> D#(y)) (D#(b(x, y)) -> D#(y), D#(pow(x, y)) -> D#(x)) (D#(b(x, y)) -> D#(y), D#(pow(x, y)) -> D#(y)) (D#(b(x, y)) -> D#(y), D#(ln(x)) -> D#(x)) (D#(pow(x, y)) -> D#(x), D#(b(x, y)) -> D#(x)) (D#(pow(x, y)) -> D#(x), D#(b(x, y)) -> D#(y)) (D#(pow(x, y)) -> D#(x), D#(c(x, y)) -> D#(x)) (D#(pow(x, y)) -> D#(x), D#(c(x, y)) -> D#(y)) (D#(pow(x, y)) -> D#(x), D#(m(x, y)) -> D#(x)) (D#(pow(x, y)) -> D#(x), D#(m(x, y)) -> D#(y)) (D#(pow(x, y)) -> D#(x), D#(div(x, y)) -> D#(x)) (D#(pow(x, y)) -> D#(x), D#(div(x, y)) -> D#(y)) (D#(pow(x, y)) -> D#(x), D#(pow(x, y)) -> D#(x)) (D#(pow(x, y)) -> D#(x), D#(pow(x, y)) -> D#(y)) (D#(pow(x, y)) -> D#(x), D#(ln(x)) -> D#(x)) (D#(m(x, y)) -> D#(x), D#(b(x, y)) -> D#(x)) (D#(m(x, y)) -> D#(x), D#(b(x, y)) -> D#(y)) (D#(m(x, y)) -> D#(x), D#(c(x, y)) -> D#(x)) (D#(m(x, y)) -> D#(x), D#(c(x, y)) -> D#(y)) (D#(m(x, y)) -> D#(x), D#(m(x, y)) -> D#(x)) (D#(m(x, y)) -> D#(x), D#(m(x, y)) -> D#(y)) (D#(m(x, y)) -> D#(x), D#(div(x, y)) -> D#(x)) (D#(m(x, y)) -> D#(x), D#(div(x, y)) -> D#(y)) (D#(m(x, y)) -> D#(x), D#(pow(x, y)) -> D#(x)) (D#(m(x, y)) -> D#(x), D#(pow(x, y)) -> D#(y)) (D#(m(x, y)) -> D#(x), D#(ln(x)) -> D#(x)) (D#(b(x, y)) -> D#(x), D#(b(x, y)) -> D#(x)) (D#(b(x, y)) -> D#(x), D#(b(x, y)) -> D#(y)) (D#(b(x, y)) -> D#(x), D#(c(x, y)) -> D#(x)) (D#(b(x, y)) -> D#(x), D#(c(x, y)) -> D#(y)) (D#(b(x, y)) -> D#(x), D#(m(x, y)) -> D#(x)) (D#(b(x, y)) -> D#(x), D#(m(x, y)) -> D#(y)) (D#(b(x, y)) -> D#(x), D#(div(x, y)) -> D#(x)) (D#(b(x, y)) -> D#(x), D#(div(x, y)) -> D#(y)) (D#(b(x, y)) -> D#(x), D#(pow(x, y)) -> D#(x)) (D#(b(x, y)) -> D#(x), D#(pow(x, y)) -> D#(y)) (D#(b(x, y)) -> D#(x), D#(ln(x)) -> D#(x))} SCCS: Scc: { D#(b(x, y)) -> D#(x), D#(b(x, y)) -> D#(y), D#(c(x, y)) -> D#(x), D#(c(x, y)) -> D#(y), D#(m(x, y)) -> D#(x), D#(m(x, y)) -> D#(y), D#(div(x, y)) -> D#(x), D#(div(x, y)) -> D#(y), D#(pow(x, y)) -> D#(x), D#(pow(x, y)) -> D#(y), D#(ln(x)) -> D#(x)} SCC: Strict: { D#(b(x, y)) -> D#(x), D#(b(x, y)) -> D#(y), D#(c(x, y)) -> D#(x), D#(c(x, y)) -> D#(y), D#(m(x, y)) -> D#(x), D#(m(x, y)) -> D#(y), D#(div(x, y)) -> D#(x), D#(div(x, y)) -> D#(y), D#(pow(x, y)) -> D#(x), D#(pow(x, y)) -> D#(y), D#(ln(x)) -> D#(x)} Weak: { D(t()) -> s(h()), D(constant()) -> h(), D(b(x, y)) -> b(D(x), D(y)), D(c(x, y)) -> b(c(y, D(x)), c(x, D(y))), D(m(x, y)) -> m(D(x), D(y)), D(opp(x)) -> opp(D(x)), D(div(x, y)) -> m(div(D(x), y), div(c(x, D(y)), pow(y, 2()))), D(pow(x, y)) -> b(c(c(y, pow(x, m(y, 1()))), D(x)), c(c(pow(x, y), ln(x)), D(y))), D(ln(x)) -> div(D(x), x), b(x, h()) -> x, b(s(x), s(y)) -> s(s(b(x, y))), b(h(), x) -> x, b(b(x, y), z) -> b(x, b(y, z))} SPSC: Simple Projection: pi(D#) = 0 Strict: { D#(b(x, y)) -> D#(x), D#(c(x, y)) -> D#(x), D#(c(x, y)) -> D#(y), D#(m(x, y)) -> D#(x), D#(m(x, y)) -> D#(y), D#(div(x, y)) -> D#(x), D#(div(x, y)) -> D#(y), D#(pow(x, y)) -> D#(x), D#(pow(x, y)) -> D#(y), D#(ln(x)) -> D#(x)} EDG: {(D#(c(x, y)) -> D#(x), D#(ln(x)) -> D#(x)) (D#(c(x, y)) -> D#(x), D#(pow(x, y)) -> D#(y)) (D#(c(x, y)) -> D#(x), D#(pow(x, y)) -> D#(x)) (D#(c(x, y)) -> D#(x), D#(div(x, y)) -> D#(y)) (D#(c(x, y)) -> D#(x), D#(div(x, y)) -> D#(x)) (D#(c(x, y)) -> D#(x), D#(m(x, y)) -> D#(y)) (D#(c(x, y)) -> D#(x), D#(m(x, y)) -> D#(x)) (D#(c(x, y)) -> D#(x), D#(c(x, y)) -> D#(y)) (D#(c(x, y)) -> D#(x), D#(c(x, y)) -> D#(x)) (D#(c(x, y)) -> D#(x), D#(b(x, y)) -> D#(x)) (D#(div(x, y)) -> D#(x), D#(ln(x)) -> D#(x)) (D#(div(x, y)) -> D#(x), D#(pow(x, y)) -> D#(y)) (D#(div(x, y)) -> D#(x), D#(pow(x, y)) -> D#(x)) (D#(div(x, y)) -> D#(x), D#(div(x, y)) -> D#(y)) (D#(div(x, y)) -> D#(x), D#(div(x, y)) -> D#(x)) (D#(div(x, y)) -> D#(x), D#(m(x, y)) -> D#(y)) (D#(div(x, y)) -> D#(x), D#(m(x, y)) -> D#(x)) (D#(div(x, y)) -> D#(x), D#(c(x, y)) -> D#(y)) (D#(div(x, y)) -> D#(x), D#(c(x, y)) -> D#(x)) (D#(div(x, y)) -> D#(x), D#(b(x, y)) -> D#(x)) (D#(ln(x)) -> D#(x), D#(ln(x)) -> D#(x)) (D#(ln(x)) -> D#(x), D#(pow(x, y)) -> D#(y)) (D#(ln(x)) -> D#(x), D#(pow(x, y)) -> D#(x)) (D#(ln(x)) -> D#(x), D#(div(x, y)) -> D#(y)) (D#(ln(x)) -> D#(x), D#(div(x, y)) -> D#(x)) (D#(ln(x)) -> D#(x), D#(m(x, y)) -> D#(y)) (D#(ln(x)) -> D#(x), D#(m(x, y)) -> D#(x)) (D#(ln(x)) -> D#(x), D#(c(x, y)) -> D#(y)) (D#(ln(x)) -> D#(x), D#(c(x, y)) -> D#(x)) (D#(ln(x)) -> D#(x), D#(b(x, y)) -> D#(x)) (D#(m(x, y)) -> D#(y), D#(ln(x)) -> D#(x)) (D#(m(x, y)) -> D#(y), D#(pow(x, y)) -> D#(y)) (D#(m(x, y)) -> D#(y), D#(pow(x, y)) -> D#(x)) (D#(m(x, y)) -> D#(y), D#(div(x, y)) -> D#(y)) (D#(m(x, y)) -> D#(y), D#(div(x, y)) -> D#(x)) (D#(m(x, y)) -> D#(y), D#(m(x, y)) -> D#(y)) (D#(m(x, y)) -> D#(y), D#(m(x, y)) -> D#(x)) (D#(m(x, y)) -> D#(y), D#(c(x, y)) -> D#(y)) (D#(m(x, y)) -> D#(y), D#(c(x, y)) -> D#(x)) (D#(m(x, y)) -> D#(y), D#(b(x, y)) -> D#(x)) (D#(pow(x, y)) -> D#(y), D#(ln(x)) -> D#(x)) (D#(pow(x, y)) -> D#(y), D#(pow(x, y)) -> D#(y)) (D#(pow(x, y)) -> D#(y), D#(pow(x, y)) -> D#(x)) (D#(pow(x, y)) -> D#(y), D#(div(x, y)) -> D#(y)) (D#(pow(x, y)) -> D#(y), D#(div(x, y)) -> D#(x)) (D#(pow(x, y)) -> D#(y), D#(m(x, y)) -> D#(y)) (D#(pow(x, y)) -> D#(y), D#(m(x, y)) -> D#(x)) (D#(pow(x, y)) -> D#(y), D#(c(x, y)) -> D#(y)) (D#(pow(x, y)) -> D#(y), D#(c(x, y)) -> D#(x)) (D#(pow(x, y)) -> D#(y), D#(b(x, y)) -> D#(x)) (D#(div(x, y)) -> D#(y), D#(b(x, y)) -> D#(x)) (D#(div(x, y)) -> D#(y), D#(c(x, y)) -> D#(x)) (D#(div(x, y)) -> D#(y), D#(c(x, y)) -> D#(y)) (D#(div(x, y)) -> D#(y), D#(m(x, y)) -> D#(x)) (D#(div(x, y)) -> D#(y), D#(m(x, y)) -> D#(y)) (D#(div(x, y)) -> D#(y), D#(div(x, y)) -> D#(x)) (D#(div(x, y)) -> D#(y), D#(div(x, y)) -> D#(y)) (D#(div(x, y)) -> D#(y), D#(pow(x, y)) -> D#(x)) (D#(div(x, y)) -> D#(y), D#(pow(x, y)) -> D#(y)) (D#(div(x, y)) -> D#(y), D#(ln(x)) -> D#(x)) (D#(c(x, y)) -> D#(y), D#(b(x, y)) -> D#(x)) (D#(c(x, y)) -> D#(y), D#(c(x, y)) -> D#(x)) (D#(c(x, y)) -> D#(y), D#(c(x, y)) -> D#(y)) (D#(c(x, y)) -> D#(y), D#(m(x, y)) -> D#(x)) (D#(c(x, y)) -> D#(y), D#(m(x, y)) -> D#(y)) (D#(c(x, y)) -> D#(y), D#(div(x, y)) -> D#(x)) (D#(c(x, y)) -> D#(y), D#(div(x, y)) -> D#(y)) (D#(c(x, y)) -> D#(y), D#(pow(x, y)) -> D#(x)) (D#(c(x, y)) -> D#(y), D#(pow(x, y)) -> D#(y)) (D#(c(x, y)) -> D#(y), D#(ln(x)) -> D#(x)) (D#(pow(x, y)) -> D#(x), D#(b(x, y)) -> D#(x)) (D#(pow(x, y)) -> D#(x), D#(c(x, y)) -> D#(x)) (D#(pow(x, y)) -> D#(x), D#(c(x, y)) -> D#(y)) (D#(pow(x, y)) -> D#(x), D#(m(x, y)) -> D#(x)) (D#(pow(x, y)) -> D#(x), D#(m(x, y)) -> D#(y)) (D#(pow(x, y)) -> D#(x), D#(div(x, y)) -> D#(x)) (D#(pow(x, y)) -> D#(x), D#(div(x, y)) -> D#(y)) (D#(pow(x, y)) -> D#(x), D#(pow(x, y)) -> D#(x)) (D#(pow(x, y)) -> D#(x), D#(pow(x, y)) -> D#(y)) (D#(pow(x, y)) -> D#(x), D#(ln(x)) -> D#(x)) (D#(m(x, y)) -> D#(x), D#(b(x, y)) -> D#(x)) (D#(m(x, y)) -> D#(x), D#(c(x, y)) -> D#(x)) (D#(m(x, y)) -> D#(x), D#(c(x, y)) -> D#(y)) (D#(m(x, y)) -> D#(x), D#(m(x, y)) -> D#(x)) (D#(m(x, y)) -> D#(x), D#(m(x, y)) -> D#(y)) (D#(m(x, y)) -> D#(x), D#(div(x, y)) -> D#(x)) (D#(m(x, y)) -> D#(x), D#(div(x, y)) -> D#(y)) (D#(m(x, y)) -> D#(x), D#(pow(x, y)) -> D#(x)) (D#(m(x, y)) -> D#(x), D#(pow(x, y)) -> D#(y)) (D#(m(x, y)) -> D#(x), D#(ln(x)) -> D#(x)) (D#(b(x, y)) -> D#(x), D#(b(x, y)) -> D#(x)) (D#(b(x, y)) -> D#(x), D#(c(x, y)) -> D#(x)) (D#(b(x, y)) -> D#(x), D#(c(x, y)) -> D#(y)) (D#(b(x, y)) -> D#(x), D#(m(x, y)) -> D#(x)) (D#(b(x, y)) -> D#(x), D#(m(x, y)) -> D#(y)) (D#(b(x, y)) -> D#(x), D#(div(x, y)) -> D#(x)) (D#(b(x, y)) -> D#(x), D#(div(x, y)) -> D#(y)) (D#(b(x, y)) -> D#(x), D#(pow(x, y)) -> D#(x)) (D#(b(x, y)) -> D#(x), D#(pow(x, y)) -> D#(y)) (D#(b(x, y)) -> D#(x), D#(ln(x)) -> D#(x))} SCCS: Scc: { D#(b(x, y)) -> D#(x), D#(c(x, y)) -> D#(x), D#(c(x, y)) -> D#(y), D#(m(x, y)) -> D#(x), D#(m(x, y)) -> D#(y), D#(div(x, y)) -> D#(x), D#(div(x, y)) -> D#(y), D#(pow(x, y)) -> D#(x), D#(pow(x, y)) -> D#(y), D#(ln(x)) -> D#(x)} SCC: Strict: { D#(b(x, y)) -> D#(x), D#(c(x, y)) -> D#(x), D#(c(x, y)) -> D#(y), D#(m(x, y)) -> D#(x), D#(m(x, y)) -> D#(y), D#(div(x, y)) -> D#(x), D#(div(x, y)) -> D#(y), D#(pow(x, y)) -> D#(x), D#(pow(x, y)) -> D#(y), D#(ln(x)) -> D#(x)} Weak: { D(t()) -> s(h()), D(constant()) -> h(), D(b(x, y)) -> b(D(x), D(y)), D(c(x, y)) -> b(c(y, D(x)), c(x, D(y))), D(m(x, y)) -> m(D(x), D(y)), D(opp(x)) -> opp(D(x)), D(div(x, y)) -> m(div(D(x), y), div(c(x, D(y)), pow(y, 2()))), D(pow(x, y)) -> b(c(c(y, pow(x, m(y, 1()))), D(x)), c(c(pow(x, y), ln(x)), D(y))), D(ln(x)) -> div(D(x), x), b(x, h()) -> x, b(s(x), s(y)) -> s(s(b(x, y))), b(h(), x) -> x, b(b(x, y), z) -> b(x, b(y, z))} SPSC: Simple Projection: pi(D#) = 0 Strict: { D#(b(x, y)) -> D#(x), D#(c(x, y)) -> D#(x), D#(c(x, y)) -> D#(y), D#(m(x, y)) -> D#(x), D#(m(x, y)) -> D#(y), D#(div(x, y)) -> D#(x), D#(div(x, y)) -> D#(y), D#(pow(x, y)) -> D#(x), D#(ln(x)) -> D#(x)} EDG: {(D#(m(x, y)) -> D#(y), D#(ln(x)) -> D#(x)) (D#(m(x, y)) -> D#(y), D#(pow(x, y)) -> D#(x)) (D#(m(x, y)) -> D#(y), D#(div(x, y)) -> D#(y)) (D#(m(x, y)) -> D#(y), D#(div(x, y)) -> D#(x)) (D#(m(x, y)) -> D#(y), D#(m(x, y)) -> D#(y)) (D#(m(x, y)) -> D#(y), D#(m(x, y)) -> D#(x)) (D#(m(x, y)) -> D#(y), D#(c(x, y)) -> D#(y)) (D#(m(x, y)) -> D#(y), D#(c(x, y)) -> D#(x)) (D#(m(x, y)) -> D#(y), D#(b(x, y)) -> D#(x)) (D#(b(x, y)) -> D#(x), D#(ln(x)) -> D#(x)) (D#(b(x, y)) -> D#(x), D#(pow(x, y)) -> D#(x)) (D#(b(x, y)) -> D#(x), D#(div(x, y)) -> D#(y)) (D#(b(x, y)) -> D#(x), D#(div(x, y)) -> D#(x)) (D#(b(x, y)) -> D#(x), D#(m(x, y)) -> D#(y)) (D#(b(x, y)) -> D#(x), D#(m(x, y)) -> D#(x)) (D#(b(x, y)) -> D#(x), D#(c(x, y)) -> D#(y)) (D#(b(x, y)) -> D#(x), D#(c(x, y)) -> D#(x)) (D#(b(x, y)) -> D#(x), D#(b(x, y)) -> D#(x)) (D#(m(x, y)) -> D#(x), D#(ln(x)) -> D#(x)) (D#(m(x, y)) -> D#(x), D#(pow(x, y)) -> D#(x)) (D#(m(x, y)) -> D#(x), D#(div(x, y)) -> D#(y)) (D#(m(x, y)) -> D#(x), D#(div(x, y)) -> D#(x)) (D#(m(x, y)) -> D#(x), D#(m(x, y)) -> D#(y)) (D#(m(x, y)) -> D#(x), D#(m(x, y)) -> D#(x)) (D#(m(x, y)) -> D#(x), D#(c(x, y)) -> D#(y)) (D#(m(x, y)) -> D#(x), D#(c(x, y)) -> D#(x)) (D#(m(x, y)) -> D#(x), D#(b(x, y)) -> D#(x)) (D#(pow(x, y)) -> D#(x), D#(ln(x)) -> D#(x)) (D#(pow(x, y)) -> D#(x), D#(pow(x, y)) -> D#(x)) (D#(pow(x, y)) -> D#(x), D#(div(x, y)) -> D#(y)) (D#(pow(x, y)) -> D#(x), D#(div(x, y)) -> D#(x)) (D#(pow(x, y)) -> D#(x), D#(m(x, y)) -> D#(y)) (D#(pow(x, y)) -> D#(x), D#(m(x, y)) -> D#(x)) (D#(pow(x, y)) -> D#(x), D#(c(x, y)) -> D#(y)) (D#(pow(x, y)) -> D#(x), D#(c(x, y)) -> D#(x)) (D#(pow(x, y)) -> D#(x), D#(b(x, y)) -> D#(x)) (D#(ln(x)) -> D#(x), D#(b(x, y)) -> D#(x)) (D#(ln(x)) -> D#(x), D#(c(x, y)) -> D#(x)) (D#(ln(x)) -> D#(x), D#(c(x, y)) -> D#(y)) (D#(ln(x)) -> D#(x), D#(m(x, y)) -> D#(x)) (D#(ln(x)) -> D#(x), D#(m(x, y)) -> D#(y)) (D#(ln(x)) -> D#(x), D#(div(x, y)) -> D#(x)) (D#(ln(x)) -> D#(x), D#(div(x, y)) -> D#(y)) (D#(ln(x)) -> D#(x), D#(pow(x, y)) -> D#(x)) (D#(ln(x)) -> D#(x), D#(ln(x)) -> D#(x)) (D#(div(x, y)) -> D#(x), D#(b(x, y)) -> D#(x)) (D#(div(x, y)) -> D#(x), D#(c(x, y)) -> D#(x)) (D#(div(x, y)) -> D#(x), D#(c(x, y)) -> D#(y)) (D#(div(x, y)) -> D#(x), D#(m(x, y)) -> D#(x)) (D#(div(x, y)) -> D#(x), D#(m(x, y)) -> D#(y)) (D#(div(x, y)) -> D#(x), D#(div(x, y)) -> D#(x)) (D#(div(x, y)) -> D#(x), D#(div(x, y)) -> D#(y)) (D#(div(x, y)) -> D#(x), D#(pow(x, y)) -> D#(x)) (D#(div(x, y)) -> D#(x), D#(ln(x)) -> D#(x)) (D#(c(x, y)) -> D#(x), D#(b(x, y)) -> D#(x)) (D#(c(x, y)) -> D#(x), D#(c(x, y)) -> D#(x)) (D#(c(x, y)) -> D#(x), D#(c(x, y)) -> D#(y)) (D#(c(x, y)) -> D#(x), D#(m(x, y)) -> D#(x)) (D#(c(x, y)) -> D#(x), D#(m(x, y)) -> D#(y)) (D#(c(x, y)) -> D#(x), D#(div(x, y)) -> D#(x)) (D#(c(x, y)) -> D#(x), D#(div(x, y)) -> D#(y)) (D#(c(x, y)) -> D#(x), D#(pow(x, y)) -> D#(x)) (D#(c(x, y)) -> D#(x), D#(ln(x)) -> D#(x)) (D#(div(x, y)) -> D#(y), D#(b(x, y)) -> D#(x)) (D#(div(x, y)) -> D#(y), D#(c(x, y)) -> D#(x)) (D#(div(x, y)) -> D#(y), D#(c(x, y)) -> D#(y)) (D#(div(x, y)) -> D#(y), D#(m(x, y)) -> D#(x)) (D#(div(x, y)) -> D#(y), D#(m(x, y)) -> D#(y)) (D#(div(x, y)) -> D#(y), D#(div(x, y)) -> D#(x)) (D#(div(x, y)) -> D#(y), D#(div(x, y)) -> D#(y)) (D#(div(x, y)) -> D#(y), D#(pow(x, y)) -> D#(x)) (D#(div(x, y)) -> D#(y), D#(ln(x)) -> D#(x)) (D#(c(x, y)) -> D#(y), D#(b(x, y)) -> D#(x)) (D#(c(x, y)) -> D#(y), D#(c(x, y)) -> D#(x)) (D#(c(x, y)) -> D#(y), D#(c(x, y)) -> D#(y)) (D#(c(x, y)) -> D#(y), D#(m(x, y)) -> D#(x)) (D#(c(x, y)) -> D#(y), D#(m(x, y)) -> D#(y)) (D#(c(x, y)) -> D#(y), D#(div(x, y)) -> D#(x)) (D#(c(x, y)) -> D#(y), D#(div(x, y)) -> D#(y)) (D#(c(x, y)) -> D#(y), D#(pow(x, y)) -> D#(x)) (D#(c(x, y)) -> D#(y), D#(ln(x)) -> D#(x))} SCCS: Scc: { D#(b(x, y)) -> D#(x), D#(c(x, y)) -> D#(x), D#(c(x, y)) -> D#(y), D#(m(x, y)) -> D#(x), D#(m(x, y)) -> D#(y), D#(div(x, y)) -> D#(x), D#(div(x, y)) -> D#(y), D#(pow(x, y)) -> D#(x), D#(ln(x)) -> D#(x)} SCC: Strict: { D#(b(x, y)) -> D#(x), D#(c(x, y)) -> D#(x), D#(c(x, y)) -> D#(y), D#(m(x, y)) -> D#(x), D#(m(x, y)) -> D#(y), D#(div(x, y)) -> D#(x), D#(div(x, y)) -> D#(y), D#(pow(x, y)) -> D#(x), D#(ln(x)) -> D#(x)} Weak: { D(t()) -> s(h()), D(constant()) -> h(), D(b(x, y)) -> b(D(x), D(y)), D(c(x, y)) -> b(c(y, D(x)), c(x, D(y))), D(m(x, y)) -> m(D(x), D(y)), D(opp(x)) -> opp(D(x)), D(div(x, y)) -> m(div(D(x), y), div(c(x, D(y)), pow(y, 2()))), D(pow(x, y)) -> b(c(c(y, pow(x, m(y, 1()))), D(x)), c(c(pow(x, y), ln(x)), D(y))), D(ln(x)) -> div(D(x), x), b(x, h()) -> x, b(s(x), s(y)) -> s(s(b(x, y))), b(h(), x) -> x, b(b(x, y), z) -> b(x, b(y, z))} SPSC: Simple Projection: pi(D#) = 0 Strict: { D#(b(x, y)) -> D#(x), D#(c(x, y)) -> D#(x), D#(c(x, y)) -> D#(y), D#(m(x, y)) -> D#(x), D#(m(x, y)) -> D#(y), D#(div(x, y)) -> D#(x), D#(div(x, y)) -> D#(y), D#(ln(x)) -> D#(x)} EDG: {(D#(m(x, y)) -> D#(y), D#(ln(x)) -> D#(x)) (D#(m(x, y)) -> D#(y), D#(div(x, y)) -> D#(y)) (D#(m(x, y)) -> D#(y), D#(div(x, y)) -> D#(x)) (D#(m(x, y)) -> D#(y), D#(m(x, y)) -> D#(y)) (D#(m(x, y)) -> D#(y), D#(m(x, y)) -> D#(x)) (D#(m(x, y)) -> D#(y), D#(c(x, y)) -> D#(y)) (D#(m(x, y)) -> D#(y), D#(c(x, y)) -> D#(x)) (D#(m(x, y)) -> D#(y), D#(b(x, y)) -> D#(x)) (D#(b(x, y)) -> D#(x), D#(ln(x)) -> D#(x)) (D#(b(x, y)) -> D#(x), D#(div(x, y)) -> D#(y)) (D#(b(x, y)) -> D#(x), D#(div(x, y)) -> D#(x)) (D#(b(x, y)) -> D#(x), D#(m(x, y)) -> D#(y)) (D#(b(x, y)) -> D#(x), D#(m(x, y)) -> D#(x)) (D#(b(x, y)) -> D#(x), D#(c(x, y)) -> D#(y)) (D#(b(x, y)) -> D#(x), D#(c(x, y)) -> D#(x)) (D#(b(x, y)) -> D#(x), D#(b(x, y)) -> D#(x)) (D#(m(x, y)) -> D#(x), D#(ln(x)) -> D#(x)) (D#(m(x, y)) -> D#(x), D#(div(x, y)) -> D#(y)) (D#(m(x, y)) -> D#(x), D#(div(x, y)) -> D#(x)) (D#(m(x, y)) -> D#(x), D#(m(x, y)) -> D#(y)) (D#(m(x, y)) -> D#(x), D#(m(x, y)) -> D#(x)) (D#(m(x, y)) -> D#(x), D#(c(x, y)) -> D#(y)) (D#(m(x, y)) -> D#(x), D#(c(x, y)) -> D#(x)) (D#(m(x, y)) -> D#(x), D#(b(x, y)) -> D#(x)) (D#(ln(x)) -> D#(x), D#(ln(x)) -> D#(x)) (D#(ln(x)) -> D#(x), D#(div(x, y)) -> D#(y)) (D#(ln(x)) -> D#(x), D#(div(x, y)) -> D#(x)) (D#(ln(x)) -> D#(x), D#(m(x, y)) -> D#(y)) (D#(ln(x)) -> D#(x), D#(m(x, y)) -> D#(x)) (D#(ln(x)) -> D#(x), D#(c(x, y)) -> D#(y)) (D#(ln(x)) -> D#(x), D#(c(x, y)) -> D#(x)) (D#(ln(x)) -> D#(x), D#(b(x, y)) -> D#(x)) (D#(div(x, y)) -> D#(x), D#(b(x, y)) -> D#(x)) (D#(div(x, y)) -> D#(x), D#(c(x, y)) -> D#(x)) (D#(div(x, y)) -> D#(x), D#(c(x, y)) -> D#(y)) (D#(div(x, y)) -> D#(x), D#(m(x, y)) -> D#(x)) (D#(div(x, y)) -> D#(x), D#(m(x, y)) -> D#(y)) (D#(div(x, y)) -> D#(x), D#(div(x, y)) -> D#(x)) (D#(div(x, y)) -> D#(x), D#(div(x, y)) -> D#(y)) (D#(div(x, y)) -> D#(x), D#(ln(x)) -> D#(x)) (D#(c(x, y)) -> D#(x), D#(b(x, y)) -> D#(x)) (D#(c(x, y)) -> D#(x), D#(c(x, y)) -> D#(x)) (D#(c(x, y)) -> D#(x), D#(c(x, y)) -> D#(y)) (D#(c(x, y)) -> D#(x), D#(m(x, y)) -> D#(x)) (D#(c(x, y)) -> D#(x), D#(m(x, y)) -> D#(y)) (D#(c(x, y)) -> D#(x), D#(div(x, y)) -> D#(x)) (D#(c(x, y)) -> D#(x), D#(div(x, y)) -> D#(y)) (D#(c(x, y)) -> D#(x), D#(ln(x)) -> D#(x)) (D#(div(x, y)) -> D#(y), D#(b(x, y)) -> D#(x)) (D#(div(x, y)) -> D#(y), D#(c(x, y)) -> D#(x)) (D#(div(x, y)) -> D#(y), D#(c(x, y)) -> D#(y)) (D#(div(x, y)) -> D#(y), D#(m(x, y)) -> D#(x)) (D#(div(x, y)) -> D#(y), D#(m(x, y)) -> D#(y)) (D#(div(x, y)) -> D#(y), D#(div(x, y)) -> D#(x)) (D#(div(x, y)) -> D#(y), D#(div(x, y)) -> D#(y)) (D#(div(x, y)) -> D#(y), D#(ln(x)) -> D#(x)) (D#(c(x, y)) -> D#(y), D#(b(x, y)) -> D#(x)) (D#(c(x, y)) -> D#(y), D#(c(x, y)) -> D#(x)) (D#(c(x, y)) -> D#(y), D#(c(x, y)) -> D#(y)) (D#(c(x, y)) -> D#(y), D#(m(x, y)) -> D#(x)) (D#(c(x, y)) -> D#(y), D#(m(x, y)) -> D#(y)) (D#(c(x, y)) -> D#(y), D#(div(x, y)) -> D#(x)) (D#(c(x, y)) -> D#(y), D#(div(x, y)) -> D#(y)) (D#(c(x, y)) -> D#(y), D#(ln(x)) -> D#(x))} SCCS: Scc: { D#(b(x, y)) -> D#(x), D#(c(x, y)) -> D#(x), D#(c(x, y)) -> D#(y), D#(m(x, y)) -> D#(x), D#(m(x, y)) -> D#(y), D#(div(x, y)) -> D#(x), D#(div(x, y)) -> D#(y), D#(ln(x)) -> D#(x)} SCC: Strict: { D#(b(x, y)) -> D#(x), D#(c(x, y)) -> D#(x), D#(c(x, y)) -> D#(y), D#(m(x, y)) -> D#(x), D#(m(x, y)) -> D#(y), D#(div(x, y)) -> D#(x), D#(div(x, y)) -> D#(y), D#(ln(x)) -> D#(x)} Weak: { D(t()) -> s(h()), D(constant()) -> h(), D(b(x, y)) -> b(D(x), D(y)), D(c(x, y)) -> b(c(y, D(x)), c(x, D(y))), D(m(x, y)) -> m(D(x), D(y)), D(opp(x)) -> opp(D(x)), D(div(x, y)) -> m(div(D(x), y), div(c(x, D(y)), pow(y, 2()))), D(pow(x, y)) -> b(c(c(y, pow(x, m(y, 1()))), D(x)), c(c(pow(x, y), ln(x)), D(y))), D(ln(x)) -> div(D(x), x), b(x, h()) -> x, b(s(x), s(y)) -> s(s(b(x, y))), b(h(), x) -> x, b(b(x, y), z) -> b(x, b(y, z))} SPSC: Simple Projection: pi(D#) = 0 Strict: { D#(c(x, y)) -> D#(x), D#(c(x, y)) -> D#(y), D#(m(x, y)) -> D#(x), D#(m(x, y)) -> D#(y), D#(div(x, y)) -> D#(x), D#(div(x, y)) -> D#(y), D#(ln(x)) -> D#(x)} EDG: {(D#(m(x, y)) -> D#(y), D#(ln(x)) -> D#(x)) (D#(m(x, y)) -> D#(y), D#(div(x, y)) -> D#(y)) (D#(m(x, y)) -> D#(y), D#(div(x, y)) -> D#(x)) (D#(m(x, y)) -> D#(y), D#(m(x, y)) -> D#(y)) (D#(m(x, y)) -> D#(y), D#(m(x, y)) -> D#(x)) (D#(m(x, y)) -> D#(y), D#(c(x, y)) -> D#(y)) (D#(m(x, y)) -> D#(y), D#(c(x, y)) -> D#(x)) (D#(c(x, y)) -> D#(x), D#(ln(x)) -> D#(x)) (D#(c(x, y)) -> D#(x), D#(div(x, y)) -> D#(y)) (D#(c(x, y)) -> D#(x), D#(div(x, y)) -> D#(x)) (D#(c(x, y)) -> D#(x), D#(m(x, y)) -> D#(y)) (D#(c(x, y)) -> D#(x), D#(m(x, y)) -> D#(x)) (D#(c(x, y)) -> D#(x), D#(c(x, y)) -> D#(y)) (D#(c(x, y)) -> D#(x), D#(c(x, y)) -> D#(x)) (D#(div(x, y)) -> D#(x), D#(ln(x)) -> D#(x)) (D#(div(x, y)) -> D#(x), D#(div(x, y)) -> D#(y)) (D#(div(x, y)) -> D#(x), D#(div(x, y)) -> D#(x)) (D#(div(x, y)) -> D#(x), D#(m(x, y)) -> D#(y)) (D#(div(x, y)) -> D#(x), D#(m(x, y)) -> D#(x)) (D#(div(x, y)) -> D#(x), D#(c(x, y)) -> D#(y)) (D#(div(x, y)) -> D#(x), D#(c(x, y)) -> D#(x)) (D#(ln(x)) -> D#(x), D#(c(x, y)) -> D#(x)) (D#(ln(x)) -> D#(x), D#(c(x, y)) -> D#(y)) (D#(ln(x)) -> D#(x), D#(m(x, y)) -> D#(x)) (D#(ln(x)) -> D#(x), D#(m(x, y)) -> D#(y)) (D#(ln(x)) -> D#(x), D#(div(x, y)) -> D#(x)) (D#(ln(x)) -> D#(x), D#(div(x, y)) -> D#(y)) (D#(ln(x)) -> D#(x), D#(ln(x)) -> D#(x)) (D#(m(x, y)) -> D#(x), D#(c(x, y)) -> D#(x)) (D#(m(x, y)) -> D#(x), D#(c(x, y)) -> D#(y)) (D#(m(x, y)) -> D#(x), D#(m(x, y)) -> D#(x)) (D#(m(x, y)) -> D#(x), D#(m(x, y)) -> D#(y)) (D#(m(x, y)) -> D#(x), D#(div(x, y)) -> D#(x)) (D#(m(x, y)) -> D#(x), D#(div(x, y)) -> D#(y)) (D#(m(x, y)) -> D#(x), D#(ln(x)) -> D#(x)) (D#(div(x, y)) -> D#(y), D#(c(x, y)) -> D#(x)) (D#(div(x, y)) -> D#(y), D#(c(x, y)) -> D#(y)) (D#(div(x, y)) -> D#(y), D#(m(x, y)) -> D#(x)) (D#(div(x, y)) -> D#(y), D#(m(x, y)) -> D#(y)) (D#(div(x, y)) -> D#(y), D#(div(x, y)) -> D#(x)) (D#(div(x, y)) -> D#(y), D#(div(x, y)) -> D#(y)) (D#(div(x, y)) -> D#(y), D#(ln(x)) -> D#(x)) (D#(c(x, y)) -> D#(y), D#(c(x, y)) -> D#(x)) (D#(c(x, y)) -> D#(y), D#(c(x, y)) -> D#(y)) (D#(c(x, y)) -> D#(y), D#(m(x, y)) -> D#(x)) (D#(c(x, y)) -> D#(y), D#(m(x, y)) -> D#(y)) (D#(c(x, y)) -> D#(y), D#(div(x, y)) -> D#(x)) (D#(c(x, y)) -> D#(y), D#(div(x, y)) -> D#(y)) (D#(c(x, y)) -> D#(y), D#(ln(x)) -> D#(x))} SCCS: Scc: { D#(c(x, y)) -> D#(x), D#(c(x, y)) -> D#(y), D#(m(x, y)) -> D#(x), D#(m(x, y)) -> D#(y), D#(div(x, y)) -> D#(x), D#(div(x, y)) -> D#(y), D#(ln(x)) -> D#(x)} SCC: Strict: { D#(c(x, y)) -> D#(x), D#(c(x, y)) -> D#(y), D#(m(x, y)) -> D#(x), D#(m(x, y)) -> D#(y), D#(div(x, y)) -> D#(x), D#(div(x, y)) -> D#(y), D#(ln(x)) -> D#(x)} Weak: { D(t()) -> s(h()), D(constant()) -> h(), D(b(x, y)) -> b(D(x), D(y)), D(c(x, y)) -> b(c(y, D(x)), c(x, D(y))), D(m(x, y)) -> m(D(x), D(y)), D(opp(x)) -> opp(D(x)), D(div(x, y)) -> m(div(D(x), y), div(c(x, D(y)), pow(y, 2()))), D(pow(x, y)) -> b(c(c(y, pow(x, m(y, 1()))), D(x)), c(c(pow(x, y), ln(x)), D(y))), D(ln(x)) -> div(D(x), x), b(x, h()) -> x, b(s(x), s(y)) -> s(s(b(x, y))), b(h(), x) -> x, b(b(x, y), z) -> b(x, b(y, z))} SPSC: Simple Projection: pi(D#) = 0 Strict: { D#(c(x, y)) -> D#(x), D#(c(x, y)) -> D#(y), D#(m(x, y)) -> D#(x), D#(m(x, y)) -> D#(y), D#(div(x, y)) -> D#(x), D#(ln(x)) -> D#(x)} EDG: {(D#(m(x, y)) -> D#(x), D#(ln(x)) -> D#(x)) (D#(m(x, y)) -> D#(x), D#(div(x, y)) -> D#(x)) (D#(m(x, y)) -> D#(x), D#(m(x, y)) -> D#(y)) (D#(m(x, y)) -> D#(x), D#(m(x, y)) -> D#(x)) (D#(m(x, y)) -> D#(x), D#(c(x, y)) -> D#(y)) (D#(m(x, y)) -> D#(x), D#(c(x, y)) -> D#(x)) (D#(ln(x)) -> D#(x), D#(ln(x)) -> D#(x)) (D#(ln(x)) -> D#(x), D#(div(x, y)) -> D#(x)) (D#(ln(x)) -> D#(x), D#(m(x, y)) -> D#(y)) (D#(ln(x)) -> D#(x), D#(m(x, y)) -> D#(x)) (D#(ln(x)) -> D#(x), D#(c(x, y)) -> D#(y)) (D#(ln(x)) -> D#(x), D#(c(x, y)) -> D#(x)) (D#(m(x, y)) -> D#(y), D#(ln(x)) -> D#(x)) (D#(m(x, y)) -> D#(y), D#(div(x, y)) -> D#(x)) (D#(m(x, y)) -> D#(y), D#(m(x, y)) -> D#(y)) (D#(m(x, y)) -> D#(y), D#(m(x, y)) -> D#(x)) (D#(m(x, y)) -> D#(y), D#(c(x, y)) -> D#(y)) (D#(m(x, y)) -> D#(y), D#(c(x, y)) -> D#(x)) (D#(c(x, y)) -> D#(y), D#(c(x, y)) -> D#(x)) (D#(c(x, y)) -> D#(y), D#(c(x, y)) -> D#(y)) (D#(c(x, y)) -> D#(y), D#(m(x, y)) -> D#(x)) (D#(c(x, y)) -> D#(y), D#(m(x, y)) -> D#(y)) (D#(c(x, y)) -> D#(y), D#(div(x, y)) -> D#(x)) (D#(c(x, y)) -> D#(y), D#(ln(x)) -> D#(x)) (D#(div(x, y)) -> D#(x), D#(c(x, y)) -> D#(x)) (D#(div(x, y)) -> D#(x), D#(c(x, y)) -> D#(y)) (D#(div(x, y)) -> D#(x), D#(m(x, y)) -> D#(x)) (D#(div(x, y)) -> D#(x), D#(m(x, y)) -> D#(y)) (D#(div(x, y)) -> D#(x), D#(div(x, y)) -> D#(x)) (D#(div(x, y)) -> D#(x), D#(ln(x)) -> D#(x)) (D#(c(x, y)) -> D#(x), D#(c(x, y)) -> D#(x)) (D#(c(x, y)) -> D#(x), D#(c(x, y)) -> D#(y)) (D#(c(x, y)) -> D#(x), D#(m(x, y)) -> D#(x)) (D#(c(x, y)) -> D#(x), D#(m(x, y)) -> D#(y)) (D#(c(x, y)) -> D#(x), D#(div(x, y)) -> D#(x)) (D#(c(x, y)) -> D#(x), D#(ln(x)) -> D#(x))} SCCS: Scc: { D#(c(x, y)) -> D#(x), D#(c(x, y)) -> D#(y), D#(m(x, y)) -> D#(x), D#(m(x, y)) -> D#(y), D#(div(x, y)) -> D#(x), D#(ln(x)) -> D#(x)} SCC: Strict: { D#(c(x, y)) -> D#(x), D#(c(x, y)) -> D#(y), D#(m(x, y)) -> D#(x), D#(m(x, y)) -> D#(y), D#(div(x, y)) -> D#(x), D#(ln(x)) -> D#(x)} Weak: { D(t()) -> s(h()), D(constant()) -> h(), D(b(x, y)) -> b(D(x), D(y)), D(c(x, y)) -> b(c(y, D(x)), c(x, D(y))), D(m(x, y)) -> m(D(x), D(y)), D(opp(x)) -> opp(D(x)), D(div(x, y)) -> m(div(D(x), y), div(c(x, D(y)), pow(y, 2()))), D(pow(x, y)) -> b(c(c(y, pow(x, m(y, 1()))), D(x)), c(c(pow(x, y), ln(x)), D(y))), D(ln(x)) -> div(D(x), x), b(x, h()) -> x, b(s(x), s(y)) -> s(s(b(x, y))), b(h(), x) -> x, b(b(x, y), z) -> b(x, b(y, z))} SPSC: Simple Projection: pi(D#) = 0 Strict: { D#(c(x, y)) -> D#(y), D#(m(x, y)) -> D#(x), D#(m(x, y)) -> D#(y), D#(div(x, y)) -> D#(x), D#(ln(x)) -> D#(x)} EDG: {(D#(div(x, y)) -> D#(x), D#(ln(x)) -> D#(x)) (D#(div(x, y)) -> D#(x), D#(div(x, y)) -> D#(x)) (D#(div(x, y)) -> D#(x), D#(m(x, y)) -> D#(y)) (D#(div(x, y)) -> D#(x), D#(m(x, y)) -> D#(x)) (D#(div(x, y)) -> D#(x), D#(c(x, y)) -> D#(y)) (D#(c(x, y)) -> D#(y), D#(ln(x)) -> D#(x)) (D#(c(x, y)) -> D#(y), D#(div(x, y)) -> D#(x)) (D#(c(x, y)) -> D#(y), D#(m(x, y)) -> D#(y)) (D#(c(x, y)) -> D#(y), D#(m(x, y)) -> D#(x)) (D#(c(x, y)) -> D#(y), D#(c(x, y)) -> D#(y)) (D#(m(x, y)) -> D#(y), D#(c(x, y)) -> D#(y)) (D#(m(x, y)) -> D#(y), D#(m(x, y)) -> D#(x)) (D#(m(x, y)) -> D#(y), D#(m(x, y)) -> D#(y)) (D#(m(x, y)) -> D#(y), D#(div(x, y)) -> D#(x)) (D#(m(x, y)) -> D#(y), D#(ln(x)) -> D#(x)) (D#(ln(x)) -> D#(x), D#(c(x, y)) -> D#(y)) (D#(ln(x)) -> D#(x), D#(m(x, y)) -> D#(x)) (D#(ln(x)) -> D#(x), D#(m(x, y)) -> D#(y)) (D#(ln(x)) -> D#(x), D#(div(x, y)) -> D#(x)) (D#(ln(x)) -> D#(x), D#(ln(x)) -> D#(x)) (D#(m(x, y)) -> D#(x), D#(c(x, y)) -> D#(y)) (D#(m(x, y)) -> D#(x), D#(m(x, y)) -> D#(x)) (D#(m(x, y)) -> D#(x), D#(m(x, y)) -> D#(y)) (D#(m(x, y)) -> D#(x), D#(div(x, y)) -> D#(x)) (D#(m(x, y)) -> D#(x), D#(ln(x)) -> D#(x))} SCCS: Scc: { D#(c(x, y)) -> D#(y), D#(m(x, y)) -> D#(x), D#(m(x, y)) -> D#(y), D#(div(x, y)) -> D#(x), D#(ln(x)) -> D#(x)} SCC: Strict: { D#(c(x, y)) -> D#(y), D#(m(x, y)) -> D#(x), D#(m(x, y)) -> D#(y), D#(div(x, y)) -> D#(x), D#(ln(x)) -> D#(x)} Weak: { D(t()) -> s(h()), D(constant()) -> h(), D(b(x, y)) -> b(D(x), D(y)), D(c(x, y)) -> b(c(y, D(x)), c(x, D(y))), D(m(x, y)) -> m(D(x), D(y)), D(opp(x)) -> opp(D(x)), D(div(x, y)) -> m(div(D(x), y), div(c(x, D(y)), pow(y, 2()))), D(pow(x, y)) -> b(c(c(y, pow(x, m(y, 1()))), D(x)), c(c(pow(x, y), ln(x)), D(y))), D(ln(x)) -> div(D(x), x), b(x, h()) -> x, b(s(x), s(y)) -> s(s(b(x, y))), b(h(), x) -> x, b(b(x, y), z) -> b(x, b(y, z))} SPSC: Simple Projection: pi(D#) = 0 Strict: {D#(c(x, y)) -> D#(y), D#(m(x, y)) -> D#(x), D#(m(x, y)) -> D#(y), D#(ln(x)) -> D#(x)} EDG: {(D#(ln(x)) -> D#(x), D#(ln(x)) -> D#(x)) (D#(ln(x)) -> D#(x), D#(m(x, y)) -> D#(y)) (D#(ln(x)) -> D#(x), D#(m(x, y)) -> D#(x)) (D#(ln(x)) -> D#(x), D#(c(x, y)) -> D#(y)) (D#(m(x, y)) -> D#(y), D#(ln(x)) -> D#(x)) (D#(m(x, y)) -> D#(y), D#(m(x, y)) -> D#(y)) (D#(m(x, y)) -> D#(y), D#(m(x, y)) -> D#(x)) (D#(m(x, y)) -> D#(y), D#(c(x, y)) -> D#(y)) (D#(c(x, y)) -> D#(y), D#(c(x, y)) -> D#(y)) (D#(c(x, y)) -> D#(y), D#(m(x, y)) -> D#(x)) (D#(c(x, y)) -> D#(y), D#(m(x, y)) -> D#(y)) (D#(c(x, y)) -> D#(y), D#(ln(x)) -> D#(x)) (D#(m(x, y)) -> D#(x), D#(c(x, y)) -> D#(y)) (D#(m(x, y)) -> D#(x), D#(m(x, y)) -> D#(x)) (D#(m(x, y)) -> D#(x), D#(m(x, y)) -> D#(y)) (D#(m(x, y)) -> D#(x), D#(ln(x)) -> D#(x))} SCCS: Scc: {D#(c(x, y)) -> D#(y), D#(m(x, y)) -> D#(x), D#(m(x, y)) -> D#(y), D#(ln(x)) -> D#(x)} SCC: Strict: {D#(c(x, y)) -> D#(y), D#(m(x, y)) -> D#(x), D#(m(x, y)) -> D#(y), D#(ln(x)) -> D#(x)} Weak: { D(t()) -> s(h()), D(constant()) -> h(), D(b(x, y)) -> b(D(x), D(y)), D(c(x, y)) -> b(c(y, D(x)), c(x, D(y))), D(m(x, y)) -> m(D(x), D(y)), D(opp(x)) -> opp(D(x)), D(div(x, y)) -> m(div(D(x), y), div(c(x, D(y)), pow(y, 2()))), D(pow(x, y)) -> b(c(c(y, pow(x, m(y, 1()))), D(x)), c(c(pow(x, y), ln(x)), D(y))), D(ln(x)) -> div(D(x), x), b(x, h()) -> x, b(s(x), s(y)) -> s(s(b(x, y))), b(h(), x) -> x, b(b(x, y), z) -> b(x, b(y, z))} SPSC: Simple Projection: pi(D#) = 0 Strict: {D#(c(x, y)) -> D#(y), D#(m(x, y)) -> D#(x), D#(ln(x)) -> D#(x)} EDG: {(D#(m(x, y)) -> D#(x), D#(ln(x)) -> D#(x)) (D#(m(x, y)) -> D#(x), D#(m(x, y)) -> D#(x)) (D#(m(x, y)) -> D#(x), D#(c(x, y)) -> D#(y)) (D#(ln(x)) -> D#(x), D#(c(x, y)) -> D#(y)) (D#(ln(x)) -> D#(x), D#(m(x, y)) -> D#(x)) (D#(ln(x)) -> D#(x), D#(ln(x)) -> D#(x)) (D#(c(x, y)) -> D#(y), D#(c(x, y)) -> D#(y)) (D#(c(x, y)) -> D#(y), D#(m(x, y)) -> D#(x)) (D#(c(x, y)) -> D#(y), D#(ln(x)) -> D#(x))} SCCS: Scc: {D#(c(x, y)) -> D#(y), D#(m(x, y)) -> D#(x), D#(ln(x)) -> D#(x)} SCC: Strict: {D#(c(x, y)) -> D#(y), D#(m(x, y)) -> D#(x), D#(ln(x)) -> D#(x)} Weak: { D(t()) -> s(h()), D(constant()) -> h(), D(b(x, y)) -> b(D(x), D(y)), D(c(x, y)) -> b(c(y, D(x)), c(x, D(y))), D(m(x, y)) -> m(D(x), D(y)), D(opp(x)) -> opp(D(x)), D(div(x, y)) -> m(div(D(x), y), div(c(x, D(y)), pow(y, 2()))), D(pow(x, y)) -> b(c(c(y, pow(x, m(y, 1()))), D(x)), c(c(pow(x, y), ln(x)), D(y))), D(ln(x)) -> div(D(x), x), b(x, h()) -> x, b(s(x), s(y)) -> s(s(b(x, y))), b(h(), x) -> x, b(b(x, y), z) -> b(x, b(y, z))} SPSC: Simple Projection: pi(D#) = 0 Strict: {D#(m(x, y)) -> D#(x), D#(ln(x)) -> D#(x)} EDG: {(D#(ln(x)) -> D#(x), D#(ln(x)) -> D#(x)) (D#(ln(x)) -> D#(x), D#(m(x, y)) -> D#(x)) (D#(m(x, y)) -> D#(x), D#(m(x, y)) -> D#(x)) (D#(m(x, y)) -> D#(x), D#(ln(x)) -> D#(x))} SCCS: Scc: {D#(m(x, y)) -> D#(x), D#(ln(x)) -> D#(x)} SCC: Strict: {D#(m(x, y)) -> D#(x), D#(ln(x)) -> D#(x)} Weak: { D(t()) -> s(h()), D(constant()) -> h(), D(b(x, y)) -> b(D(x), D(y)), D(c(x, y)) -> b(c(y, D(x)), c(x, D(y))), D(m(x, y)) -> m(D(x), D(y)), D(opp(x)) -> opp(D(x)), D(div(x, y)) -> m(div(D(x), y), div(c(x, D(y)), pow(y, 2()))), D(pow(x, y)) -> b(c(c(y, pow(x, m(y, 1()))), D(x)), c(c(pow(x, y), ln(x)), D(y))), D(ln(x)) -> div(D(x), x), b(x, h()) -> x, b(s(x), s(y)) -> s(s(b(x, y))), b(h(), x) -> x, b(b(x, y), z) -> b(x, b(y, z))} SPSC: Simple Projection: pi(D#) = 0 Strict: {D#(ln(x)) -> D#(x)} EDG: {(D#(ln(x)) -> D#(x), D#(ln(x)) -> D#(x))} SCCS: Scc: {D#(ln(x)) -> D#(x)} SCC: Strict: {D#(ln(x)) -> D#(x)} Weak: { D(t()) -> s(h()), D(constant()) -> h(), D(b(x, y)) -> b(D(x), D(y)), D(c(x, y)) -> b(c(y, D(x)), c(x, D(y))), D(m(x, y)) -> m(D(x), D(y)), D(opp(x)) -> opp(D(x)), D(div(x, y)) -> m(div(D(x), y), div(c(x, D(y)), pow(y, 2()))), D(pow(x, y)) -> b(c(c(y, pow(x, m(y, 1()))), D(x)), c(c(pow(x, y), ln(x)), D(y))), D(ln(x)) -> div(D(x), x), b(x, h()) -> x, b(s(x), s(y)) -> s(s(b(x, y))), b(h(), x) -> x, b(b(x, y), z) -> b(x, b(y, z))} SPSC: Simple Projection: pi(D#) = 0 Strict: {} Qed