YES TRS: { D(t()) -> 1(), D(constant()) -> 0(), D(+(x, y)) -> +(D(x), D(y)), D(*(x, y)) -> +(*(y, D(x)), *(x, D(y))), D(-(x, y)) -> -(D(x), D(y)), D(minus(x)) -> minus(D(x)), D(div(x, y)) -> -(div(D(x), y), div(*(x, D(y)), pow(y, 2()))), D(pow(x, y)) -> +(*(*(y, pow(x, -(y, 1()))), D(x)), *(*(pow(x, y), ln(x)), D(y))), D(ln(x)) -> div(D(x), x)} DP: Strict: { D#(+(x, y)) -> D#(x), D#(+(x, y)) -> D#(y), D#(*(x, y)) -> D#(x), D#(*(x, y)) -> D#(y), D#(-(x, y)) -> D#(x), D#(-(x, y)) -> D#(y), D#(minus(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()) -> 1(), D(constant()) -> 0(), D(+(x, y)) -> +(D(x), D(y)), D(*(x, y)) -> +(*(y, D(x)), *(x, D(y))), D(-(x, y)) -> -(D(x), D(y)), D(minus(x)) -> minus(D(x)), D(div(x, y)) -> -(div(D(x), y), div(*(x, D(y)), pow(y, 2()))), D(pow(x, y)) -> +(*(*(y, pow(x, -(y, 1()))), D(x)), *(*(pow(x, y), ln(x)), D(y))), D(ln(x)) -> div(D(x), x)} EDG: {(D#(*(x, y)) -> D#(x), D#(ln(x)) -> D#(x)) (D#(*(x, y)) -> D#(x), D#(pow(x, y)) -> D#(y)) (D#(*(x, y)) -> D#(x), D#(pow(x, y)) -> D#(x)) (D#(*(x, y)) -> D#(x), D#(div(x, y)) -> D#(y)) (D#(*(x, y)) -> D#(x), D#(div(x, y)) -> D#(x)) (D#(*(x, y)) -> D#(x), D#(minus(x)) -> D#(x)) (D#(*(x, y)) -> D#(x), D#(-(x, y)) -> D#(y)) (D#(*(x, y)) -> D#(x), D#(-(x, y)) -> D#(x)) (D#(*(x, y)) -> D#(x), D#(*(x, y)) -> D#(y)) (D#(*(x, y)) -> D#(x), D#(*(x, y)) -> D#(x)) (D#(*(x, y)) -> D#(x), D#(+(x, y)) -> D#(y)) (D#(*(x, y)) -> D#(x), D#(+(x, y)) -> D#(x)) (D#(minus(x)) -> D#(x), D#(ln(x)) -> D#(x)) (D#(minus(x)) -> D#(x), D#(pow(x, y)) -> D#(y)) (D#(minus(x)) -> D#(x), D#(pow(x, y)) -> D#(x)) (D#(minus(x)) -> D#(x), D#(div(x, y)) -> D#(y)) (D#(minus(x)) -> D#(x), D#(div(x, y)) -> D#(x)) (D#(minus(x)) -> D#(x), D#(minus(x)) -> D#(x)) (D#(minus(x)) -> D#(x), D#(-(x, y)) -> D#(y)) (D#(minus(x)) -> D#(x), D#(-(x, y)) -> D#(x)) (D#(minus(x)) -> D#(x), D#(*(x, y)) -> D#(y)) (D#(minus(x)) -> D#(x), D#(*(x, y)) -> D#(x)) (D#(minus(x)) -> D#(x), D#(+(x, y)) -> D#(y)) (D#(minus(x)) -> D#(x), D#(+(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#(y)) (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#(minus(x)) -> D#(x)) (D#(pow(x, y)) -> D#(x), D#(-(x, y)) -> D#(y)) (D#(pow(x, y)) -> D#(x), D#(-(x, y)) -> D#(x)) (D#(pow(x, y)) -> D#(x), D#(*(x, y)) -> D#(y)) (D#(pow(x, y)) -> D#(x), D#(*(x, y)) -> D#(x)) (D#(pow(x, y)) -> D#(x), D#(+(x, y)) -> D#(y)) (D#(pow(x, y)) -> D#(x), D#(+(x, y)) -> D#(x)) (D#(+(x, y)) -> D#(y), D#(ln(x)) -> D#(x)) (D#(+(x, y)) -> D#(y), D#(pow(x, y)) -> D#(y)) (D#(+(x, y)) -> D#(y), D#(pow(x, y)) -> D#(x)) (D#(+(x, y)) -> D#(y), D#(div(x, y)) -> D#(y)) (D#(+(x, y)) -> D#(y), D#(div(x, y)) -> D#(x)) (D#(+(x, y)) -> D#(y), D#(minus(x)) -> D#(x)) (D#(+(x, y)) -> D#(y), D#(-(x, y)) -> D#(y)) (D#(+(x, y)) -> D#(y), D#(-(x, y)) -> D#(x)) (D#(+(x, y)) -> D#(y), D#(*(x, y)) -> D#(y)) (D#(+(x, y)) -> D#(y), D#(*(x, y)) -> D#(x)) (D#(+(x, y)) -> D#(y), D#(+(x, y)) -> D#(y)) (D#(+(x, y)) -> D#(y), D#(+(x, y)) -> D#(x)) (D#(-(x, y)) -> D#(y), D#(ln(x)) -> D#(x)) (D#(-(x, y)) -> D#(y), D#(pow(x, y)) -> D#(y)) (D#(-(x, y)) -> D#(y), D#(pow(x, y)) -> D#(x)) (D#(-(x, y)) -> D#(y), D#(div(x, y)) -> D#(y)) (D#(-(x, y)) -> D#(y), D#(div(x, y)) -> D#(x)) (D#(-(x, y)) -> D#(y), D#(minus(x)) -> D#(x)) (D#(-(x, y)) -> D#(y), D#(-(x, y)) -> D#(y)) (D#(-(x, y)) -> D#(y), D#(-(x, y)) -> D#(x)) (D#(-(x, y)) -> D#(y), D#(*(x, y)) -> D#(y)) (D#(-(x, y)) -> D#(y), D#(*(x, y)) -> D#(x)) (D#(-(x, y)) -> D#(y), D#(+(x, y)) -> D#(y)) (D#(-(x, y)) -> D#(y), D#(+(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#(minus(x)) -> D#(x)) (D#(pow(x, y)) -> D#(y), D#(-(x, y)) -> D#(y)) (D#(pow(x, y)) -> D#(y), D#(-(x, y)) -> D#(x)) (D#(pow(x, y)) -> D#(y), D#(*(x, y)) -> D#(y)) (D#(pow(x, y)) -> D#(y), D#(*(x, y)) -> D#(x)) (D#(pow(x, y)) -> D#(y), D#(+(x, y)) -> D#(y)) (D#(pow(x, y)) -> D#(y), D#(+(x, y)) -> D#(x)) (D#(div(x, y)) -> D#(y), D#(+(x, y)) -> D#(x)) (D#(div(x, y)) -> D#(y), D#(+(x, y)) -> D#(y)) (D#(div(x, y)) -> D#(y), D#(*(x, y)) -> D#(x)) (D#(div(x, y)) -> D#(y), D#(*(x, y)) -> D#(y)) (D#(div(x, y)) -> D#(y), D#(-(x, y)) -> D#(x)) (D#(div(x, y)) -> D#(y), D#(-(x, y)) -> D#(y)) (D#(div(x, y)) -> D#(y), D#(minus(x)) -> D#(x)) (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#(*(x, y)) -> D#(y), D#(+(x, y)) -> D#(x)) (D#(*(x, y)) -> D#(y), D#(+(x, y)) -> D#(y)) (D#(*(x, y)) -> D#(y), D#(*(x, y)) -> D#(x)) (D#(*(x, y)) -> D#(y), D#(*(x, y)) -> D#(y)) (D#(*(x, y)) -> D#(y), D#(-(x, y)) -> D#(x)) (D#(*(x, y)) -> D#(y), D#(-(x, y)) -> D#(y)) (D#(*(x, y)) -> D#(y), D#(minus(x)) -> D#(x)) (D#(*(x, y)) -> D#(y), D#(div(x, y)) -> D#(x)) (D#(*(x, y)) -> D#(y), D#(div(x, y)) -> D#(y)) (D#(*(x, y)) -> D#(y), D#(pow(x, y)) -> D#(x)) (D#(*(x, y)) -> D#(y), D#(pow(x, y)) -> D#(y)) (D#(*(x, y)) -> D#(y), D#(ln(x)) -> D#(x)) (D#(ln(x)) -> D#(x), D#(+(x, y)) -> D#(x)) (D#(ln(x)) -> D#(x), D#(+(x, y)) -> D#(y)) (D#(ln(x)) -> D#(x), D#(*(x, y)) -> D#(x)) (D#(ln(x)) -> D#(x), D#(*(x, y)) -> D#(y)) (D#(ln(x)) -> D#(x), D#(-(x, y)) -> D#(x)) (D#(ln(x)) -> D#(x), D#(-(x, y)) -> D#(y)) (D#(ln(x)) -> D#(x), D#(minus(x)) -> D#(x)) (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#(pow(x, y)) -> D#(y)) (D#(ln(x)) -> D#(x), D#(ln(x)) -> D#(x)) (D#(div(x, y)) -> D#(x), D#(+(x, y)) -> D#(x)) (D#(div(x, y)) -> D#(x), D#(+(x, y)) -> D#(y)) (D#(div(x, y)) -> D#(x), D#(*(x, y)) -> D#(x)) (D#(div(x, y)) -> D#(x), D#(*(x, y)) -> D#(y)) (D#(div(x, y)) -> D#(x), D#(-(x, y)) -> D#(x)) (D#(div(x, y)) -> D#(x), D#(-(x, y)) -> D#(y)) (D#(div(x, y)) -> D#(x), D#(minus(x)) -> D#(x)) (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#(pow(x, y)) -> D#(y)) (D#(div(x, y)) -> D#(x), D#(ln(x)) -> D#(x)) (D#(-(x, y)) -> D#(x), D#(+(x, y)) -> D#(x)) (D#(-(x, y)) -> D#(x), D#(+(x, y)) -> D#(y)) (D#(-(x, y)) -> D#(x), D#(*(x, y)) -> D#(x)) (D#(-(x, y)) -> D#(x), D#(*(x, y)) -> D#(y)) (D#(-(x, y)) -> D#(x), D#(-(x, y)) -> D#(x)) (D#(-(x, y)) -> D#(x), D#(-(x, y)) -> D#(y)) (D#(-(x, y)) -> D#(x), D#(minus(x)) -> D#(x)) (D#(-(x, y)) -> D#(x), D#(div(x, y)) -> D#(x)) (D#(-(x, y)) -> D#(x), D#(div(x, y)) -> D#(y)) (D#(-(x, y)) -> D#(x), D#(pow(x, y)) -> D#(x)) (D#(-(x, y)) -> D#(x), D#(pow(x, y)) -> D#(y)) (D#(-(x, y)) -> D#(x), D#(ln(x)) -> D#(x)) (D#(+(x, y)) -> D#(x), D#(+(x, y)) -> D#(x)) (D#(+(x, y)) -> D#(x), D#(+(x, y)) -> D#(y)) (D#(+(x, y)) -> D#(x), D#(*(x, y)) -> D#(x)) (D#(+(x, y)) -> D#(x), D#(*(x, y)) -> D#(y)) (D#(+(x, y)) -> D#(x), D#(-(x, y)) -> D#(x)) (D#(+(x, y)) -> D#(x), D#(-(x, y)) -> D#(y)) (D#(+(x, y)) -> D#(x), D#(minus(x)) -> D#(x)) (D#(+(x, y)) -> D#(x), D#(div(x, y)) -> D#(x)) (D#(+(x, y)) -> D#(x), D#(div(x, y)) -> D#(y)) (D#(+(x, y)) -> D#(x), D#(pow(x, y)) -> D#(x)) (D#(+(x, y)) -> D#(x), D#(pow(x, y)) -> D#(y)) (D#(+(x, y)) -> D#(x), D#(ln(x)) -> D#(x))} SCCS: Scc: { D#(+(x, y)) -> D#(x), D#(+(x, y)) -> D#(y), D#(*(x, y)) -> D#(x), D#(*(x, y)) -> D#(y), D#(-(x, y)) -> D#(x), D#(-(x, y)) -> D#(y), D#(minus(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: { D#(+(x, y)) -> D#(x), D#(+(x, y)) -> D#(y), D#(*(x, y)) -> D#(x), D#(*(x, y)) -> D#(y), D#(-(x, y)) -> D#(x), D#(-(x, y)) -> D#(y), D#(minus(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()) -> 1(), D(constant()) -> 0(), D(+(x, y)) -> +(D(x), D(y)), D(*(x, y)) -> +(*(y, D(x)), *(x, D(y))), D(-(x, y)) -> -(D(x), D(y)), D(minus(x)) -> minus(D(x)), D(div(x, y)) -> -(div(D(x), y), div(*(x, D(y)), pow(y, 2()))), D(pow(x, y)) -> +(*(*(y, pow(x, -(y, 1()))), D(x)), *(*(pow(x, y), ln(x)), D(y))), D(ln(x)) -> div(D(x), x)} SPSC: Simple Projection: pi(D#) = 0 Strict: { D#(+(x, y)) -> D#(x), D#(+(x, y)) -> D#(y), D#(*(x, y)) -> D#(x), D#(*(x, y)) -> D#(y), D#(-(x, y)) -> D#(x), D#(-(x, y)) -> D#(y), D#(minus(x)) -> D#(x), 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#(*(x, y)) -> D#(x), D#(ln(x)) -> D#(x)) (D#(*(x, y)) -> D#(x), D#(pow(x, y)) -> D#(x)) (D#(*(x, y)) -> D#(x), D#(div(x, y)) -> D#(y)) (D#(*(x, y)) -> D#(x), D#(div(x, y)) -> D#(x)) (D#(*(x, y)) -> D#(x), D#(minus(x)) -> D#(x)) (D#(*(x, y)) -> D#(x), D#(-(x, y)) -> D#(y)) (D#(*(x, y)) -> D#(x), D#(-(x, y)) -> D#(x)) (D#(*(x, y)) -> D#(x), D#(*(x, y)) -> D#(y)) (D#(*(x, y)) -> D#(x), D#(*(x, y)) -> D#(x)) (D#(*(x, y)) -> D#(x), D#(+(x, y)) -> D#(y)) (D#(*(x, y)) -> D#(x), D#(+(x, y)) -> D#(x)) (D#(minus(x)) -> D#(x), D#(ln(x)) -> D#(x)) (D#(minus(x)) -> D#(x), D#(pow(x, y)) -> D#(x)) (D#(minus(x)) -> D#(x), D#(div(x, y)) -> D#(y)) (D#(minus(x)) -> D#(x), D#(div(x, y)) -> D#(x)) (D#(minus(x)) -> D#(x), D#(minus(x)) -> D#(x)) (D#(minus(x)) -> D#(x), D#(-(x, y)) -> D#(y)) (D#(minus(x)) -> D#(x), D#(-(x, y)) -> D#(x)) (D#(minus(x)) -> D#(x), D#(*(x, y)) -> D#(y)) (D#(minus(x)) -> D#(x), D#(*(x, y)) -> D#(x)) (D#(minus(x)) -> D#(x), D#(+(x, y)) -> D#(y)) (D#(minus(x)) -> D#(x), D#(+(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#(minus(x)) -> D#(x)) (D#(pow(x, y)) -> D#(x), D#(-(x, y)) -> D#(y)) (D#(pow(x, y)) -> D#(x), D#(-(x, y)) -> D#(x)) (D#(pow(x, y)) -> D#(x), D#(*(x, y)) -> D#(y)) (D#(pow(x, y)) -> D#(x), D#(*(x, y)) -> D#(x)) (D#(pow(x, y)) -> D#(x), D#(+(x, y)) -> D#(y)) (D#(pow(x, y)) -> D#(x), D#(+(x, y)) -> D#(x)) (D#(+(x, y)) -> D#(y), D#(ln(x)) -> D#(x)) (D#(+(x, y)) -> D#(y), D#(pow(x, y)) -> D#(x)) (D#(+(x, y)) -> D#(y), D#(div(x, y)) -> D#(y)) (D#(+(x, y)) -> D#(y), D#(div(x, y)) -> D#(x)) (D#(+(x, y)) -> D#(y), D#(minus(x)) -> D#(x)) (D#(+(x, y)) -> D#(y), D#(-(x, y)) -> D#(y)) (D#(+(x, y)) -> D#(y), D#(-(x, y)) -> D#(x)) (D#(+(x, y)) -> D#(y), D#(*(x, y)) -> D#(y)) (D#(+(x, y)) -> D#(y), D#(*(x, y)) -> D#(x)) (D#(+(x, y)) -> D#(y), D#(+(x, y)) -> D#(y)) (D#(+(x, y)) -> D#(y), D#(+(x, y)) -> D#(x)) (D#(-(x, y)) -> D#(y), D#(ln(x)) -> D#(x)) (D#(-(x, y)) -> D#(y), D#(pow(x, y)) -> D#(x)) (D#(-(x, y)) -> D#(y), D#(div(x, y)) -> D#(y)) (D#(-(x, y)) -> D#(y), D#(div(x, y)) -> D#(x)) (D#(-(x, y)) -> D#(y), D#(minus(x)) -> D#(x)) (D#(-(x, y)) -> D#(y), D#(-(x, y)) -> D#(y)) (D#(-(x, y)) -> D#(y), D#(-(x, y)) -> D#(x)) (D#(-(x, y)) -> D#(y), D#(*(x, y)) -> D#(y)) (D#(-(x, y)) -> D#(y), D#(*(x, y)) -> D#(x)) (D#(-(x, y)) -> D#(y), D#(+(x, y)) -> D#(y)) (D#(-(x, y)) -> D#(y), D#(+(x, y)) -> D#(x)) (D#(div(x, y)) -> D#(y), D#(+(x, y)) -> D#(x)) (D#(div(x, y)) -> D#(y), D#(+(x, y)) -> D#(y)) (D#(div(x, y)) -> D#(y), D#(*(x, y)) -> D#(x)) (D#(div(x, y)) -> D#(y), D#(*(x, y)) -> D#(y)) (D#(div(x, y)) -> D#(y), D#(-(x, y)) -> D#(x)) (D#(div(x, y)) -> D#(y), D#(-(x, y)) -> D#(y)) (D#(div(x, y)) -> D#(y), D#(minus(x)) -> D#(x)) (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#(*(x, y)) -> D#(y), D#(+(x, y)) -> D#(x)) (D#(*(x, y)) -> D#(y), D#(+(x, y)) -> D#(y)) (D#(*(x, y)) -> D#(y), D#(*(x, y)) -> D#(x)) (D#(*(x, y)) -> D#(y), D#(*(x, y)) -> D#(y)) (D#(*(x, y)) -> D#(y), D#(-(x, y)) -> D#(x)) (D#(*(x, y)) -> D#(y), D#(-(x, y)) -> D#(y)) (D#(*(x, y)) -> D#(y), D#(minus(x)) -> D#(x)) (D#(*(x, y)) -> D#(y), D#(div(x, y)) -> D#(x)) (D#(*(x, y)) -> D#(y), D#(div(x, y)) -> D#(y)) (D#(*(x, y)) -> D#(y), D#(pow(x, y)) -> D#(x)) (D#(*(x, y)) -> D#(y), D#(ln(x)) -> D#(x)) (D#(ln(x)) -> D#(x), D#(+(x, y)) -> D#(x)) (D#(ln(x)) -> D#(x), D#(+(x, y)) -> D#(y)) (D#(ln(x)) -> D#(x), D#(*(x, y)) -> D#(x)) (D#(ln(x)) -> D#(x), D#(*(x, y)) -> D#(y)) (D#(ln(x)) -> D#(x), D#(-(x, y)) -> D#(x)) (D#(ln(x)) -> D#(x), D#(-(x, y)) -> D#(y)) (D#(ln(x)) -> D#(x), D#(minus(x)) -> D#(x)) (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#(+(x, y)) -> D#(x)) (D#(div(x, y)) -> D#(x), D#(+(x, y)) -> D#(y)) (D#(div(x, y)) -> D#(x), D#(*(x, y)) -> D#(x)) (D#(div(x, y)) -> D#(x), D#(*(x, y)) -> D#(y)) (D#(div(x, y)) -> D#(x), D#(-(x, y)) -> D#(x)) (D#(div(x, y)) -> D#(x), D#(-(x, y)) -> D#(y)) (D#(div(x, y)) -> D#(x), D#(minus(x)) -> D#(x)) (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#(-(x, y)) -> D#(x), D#(+(x, y)) -> D#(x)) (D#(-(x, y)) -> D#(x), D#(+(x, y)) -> D#(y)) (D#(-(x, y)) -> D#(x), D#(*(x, y)) -> D#(x)) (D#(-(x, y)) -> D#(x), D#(*(x, y)) -> D#(y)) (D#(-(x, y)) -> D#(x), D#(-(x, y)) -> D#(x)) (D#(-(x, y)) -> D#(x), D#(-(x, y)) -> D#(y)) (D#(-(x, y)) -> D#(x), D#(minus(x)) -> D#(x)) (D#(-(x, y)) -> D#(x), D#(div(x, y)) -> D#(x)) (D#(-(x, y)) -> D#(x), D#(div(x, y)) -> D#(y)) (D#(-(x, y)) -> D#(x), D#(pow(x, y)) -> D#(x)) (D#(-(x, y)) -> D#(x), D#(ln(x)) -> D#(x)) (D#(+(x, y)) -> D#(x), D#(+(x, y)) -> D#(x)) (D#(+(x, y)) -> D#(x), D#(+(x, y)) -> D#(y)) (D#(+(x, y)) -> D#(x), D#(*(x, y)) -> D#(x)) (D#(+(x, y)) -> D#(x), D#(*(x, y)) -> D#(y)) (D#(+(x, y)) -> D#(x), D#(-(x, y)) -> D#(x)) (D#(+(x, y)) -> D#(x), D#(-(x, y)) -> D#(y)) (D#(+(x, y)) -> D#(x), D#(minus(x)) -> D#(x)) (D#(+(x, y)) -> D#(x), D#(div(x, y)) -> D#(x)) (D#(+(x, y)) -> D#(x), D#(div(x, y)) -> D#(y)) (D#(+(x, y)) -> D#(x), D#(pow(x, y)) -> D#(x)) (D#(+(x, y)) -> D#(x), D#(ln(x)) -> D#(x))} SCCS: Scc: { D#(+(x, y)) -> D#(x), D#(+(x, y)) -> D#(y), D#(*(x, y)) -> D#(x), D#(*(x, y)) -> D#(y), D#(-(x, y)) -> D#(x), D#(-(x, y)) -> D#(y), D#(minus(x)) -> D#(x), 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#(+(x, y)) -> D#(x), D#(+(x, y)) -> D#(y), D#(*(x, y)) -> D#(x), D#(*(x, y)) -> D#(y), D#(-(x, y)) -> D#(x), D#(-(x, y)) -> D#(y), D#(minus(x)) -> D#(x), 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()) -> 1(), D(constant()) -> 0(), D(+(x, y)) -> +(D(x), D(y)), D(*(x, y)) -> +(*(y, D(x)), *(x, D(y))), D(-(x, y)) -> -(D(x), D(y)), D(minus(x)) -> minus(D(x)), D(div(x, y)) -> -(div(D(x), y), div(*(x, D(y)), pow(y, 2()))), D(pow(x, y)) -> +(*(*(y, pow(x, -(y, 1()))), D(x)), *(*(pow(x, y), ln(x)), D(y))), D(ln(x)) -> div(D(x), x)} SPSC: Simple Projection: pi(D#) = 0 Strict: { D#(+(x, y)) -> D#(x), D#(+(x, y)) -> D#(y), D#(*(x, y)) -> D#(x), D#(*(x, y)) -> D#(y), D#(-(x, y)) -> D#(x), D#(-(x, y)) -> D#(y), D#(minus(x)) -> D#(x), D#(div(x, y)) -> D#(x), D#(div(x, y)) -> D#(y), D#(ln(x)) -> D#(x)} EDG: {(D#(*(x, y)) -> D#(x), D#(ln(x)) -> D#(x)) (D#(*(x, y)) -> D#(x), D#(div(x, y)) -> D#(y)) (D#(*(x, y)) -> D#(x), D#(div(x, y)) -> D#(x)) (D#(*(x, y)) -> D#(x), D#(minus(x)) -> D#(x)) (D#(*(x, y)) -> D#(x), D#(-(x, y)) -> D#(y)) (D#(*(x, y)) -> D#(x), D#(-(x, y)) -> D#(x)) (D#(*(x, y)) -> D#(x), D#(*(x, y)) -> D#(y)) (D#(*(x, y)) -> D#(x), D#(*(x, y)) -> D#(x)) (D#(*(x, y)) -> D#(x), D#(+(x, y)) -> D#(y)) (D#(*(x, y)) -> D#(x), D#(+(x, y)) -> D#(x)) (D#(minus(x)) -> D#(x), D#(ln(x)) -> D#(x)) (D#(minus(x)) -> D#(x), D#(div(x, y)) -> D#(y)) (D#(minus(x)) -> D#(x), D#(div(x, y)) -> D#(x)) (D#(minus(x)) -> D#(x), D#(minus(x)) -> D#(x)) (D#(minus(x)) -> D#(x), D#(-(x, y)) -> D#(y)) (D#(minus(x)) -> D#(x), D#(-(x, y)) -> D#(x)) (D#(minus(x)) -> D#(x), D#(*(x, y)) -> D#(y)) (D#(minus(x)) -> D#(x), D#(*(x, y)) -> D#(x)) (D#(minus(x)) -> D#(x), D#(+(x, y)) -> D#(y)) (D#(minus(x)) -> D#(x), D#(+(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#(minus(x)) -> D#(x)) (D#(ln(x)) -> D#(x), D#(-(x, y)) -> D#(y)) (D#(ln(x)) -> D#(x), D#(-(x, y)) -> D#(x)) (D#(ln(x)) -> D#(x), D#(*(x, y)) -> D#(y)) (D#(ln(x)) -> D#(x), D#(*(x, y)) -> D#(x)) (D#(ln(x)) -> D#(x), D#(+(x, y)) -> D#(y)) (D#(ln(x)) -> D#(x), D#(+(x, y)) -> D#(x)) (D#(*(x, y)) -> D#(y), D#(ln(x)) -> D#(x)) (D#(*(x, y)) -> D#(y), D#(div(x, y)) -> D#(y)) (D#(*(x, y)) -> D#(y), D#(div(x, y)) -> D#(x)) (D#(*(x, y)) -> D#(y), D#(minus(x)) -> D#(x)) (D#(*(x, y)) -> D#(y), D#(-(x, y)) -> D#(y)) (D#(*(x, y)) -> D#(y), D#(-(x, y)) -> D#(x)) (D#(*(x, y)) -> D#(y), D#(*(x, y)) -> D#(y)) (D#(*(x, y)) -> D#(y), D#(*(x, y)) -> D#(x)) (D#(*(x, y)) -> D#(y), D#(+(x, y)) -> D#(y)) (D#(*(x, y)) -> D#(y), D#(+(x, y)) -> D#(x)) (D#(div(x, y)) -> D#(y), D#(ln(x)) -> 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#(minus(x)) -> D#(x)) (D#(div(x, y)) -> D#(y), D#(-(x, y)) -> D#(y)) (D#(div(x, y)) -> D#(y), D#(-(x, y)) -> D#(x)) (D#(div(x, y)) -> D#(y), D#(*(x, y)) -> D#(y)) (D#(div(x, y)) -> D#(y), D#(*(x, y)) -> D#(x)) (D#(div(x, y)) -> D#(y), D#(+(x, y)) -> D#(y)) (D#(div(x, y)) -> D#(y), D#(+(x, y)) -> D#(x)) (D#(-(x, y)) -> D#(y), D#(+(x, y)) -> D#(x)) (D#(-(x, y)) -> D#(y), D#(+(x, y)) -> D#(y)) (D#(-(x, y)) -> D#(y), D#(*(x, y)) -> D#(x)) (D#(-(x, y)) -> D#(y), D#(*(x, y)) -> D#(y)) (D#(-(x, y)) -> D#(y), D#(-(x, y)) -> D#(x)) (D#(-(x, y)) -> D#(y), D#(-(x, y)) -> D#(y)) (D#(-(x, y)) -> D#(y), D#(minus(x)) -> D#(x)) (D#(-(x, y)) -> D#(y), D#(div(x, y)) -> D#(x)) (D#(-(x, y)) -> D#(y), D#(div(x, y)) -> D#(y)) (D#(-(x, y)) -> D#(y), D#(ln(x)) -> D#(x)) (D#(+(x, y)) -> D#(y), D#(+(x, y)) -> D#(x)) (D#(+(x, y)) -> D#(y), D#(+(x, y)) -> D#(y)) (D#(+(x, y)) -> D#(y), D#(*(x, y)) -> D#(x)) (D#(+(x, y)) -> D#(y), D#(*(x, y)) -> D#(y)) (D#(+(x, y)) -> D#(y), D#(-(x, y)) -> D#(x)) (D#(+(x, y)) -> D#(y), D#(-(x, y)) -> D#(y)) (D#(+(x, y)) -> D#(y), D#(minus(x)) -> D#(x)) (D#(+(x, y)) -> D#(y), D#(div(x, y)) -> D#(x)) (D#(+(x, y)) -> D#(y), D#(div(x, y)) -> D#(y)) (D#(+(x, y)) -> D#(y), D#(ln(x)) -> D#(x)) (D#(div(x, y)) -> D#(x), D#(+(x, y)) -> D#(x)) (D#(div(x, y)) -> D#(x), D#(+(x, y)) -> D#(y)) (D#(div(x, y)) -> D#(x), D#(*(x, y)) -> D#(x)) (D#(div(x, y)) -> D#(x), D#(*(x, y)) -> D#(y)) (D#(div(x, y)) -> D#(x), D#(-(x, y)) -> D#(x)) (D#(div(x, y)) -> D#(x), D#(-(x, y)) -> D#(y)) (D#(div(x, y)) -> D#(x), D#(minus(x)) -> D#(x)) (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#(-(x, y)) -> D#(x), D#(+(x, y)) -> D#(x)) (D#(-(x, y)) -> D#(x), D#(+(x, y)) -> D#(y)) (D#(-(x, y)) -> D#(x), D#(*(x, y)) -> D#(x)) (D#(-(x, y)) -> D#(x), D#(*(x, y)) -> D#(y)) (D#(-(x, y)) -> D#(x), D#(-(x, y)) -> D#(x)) (D#(-(x, y)) -> D#(x), D#(-(x, y)) -> D#(y)) (D#(-(x, y)) -> D#(x), D#(minus(x)) -> D#(x)) (D#(-(x, y)) -> D#(x), D#(div(x, y)) -> D#(x)) (D#(-(x, y)) -> D#(x), D#(div(x, y)) -> D#(y)) (D#(-(x, y)) -> D#(x), D#(ln(x)) -> D#(x)) (D#(+(x, y)) -> D#(x), D#(+(x, y)) -> D#(x)) (D#(+(x, y)) -> D#(x), D#(+(x, y)) -> D#(y)) (D#(+(x, y)) -> D#(x), D#(*(x, y)) -> D#(x)) (D#(+(x, y)) -> D#(x), D#(*(x, y)) -> D#(y)) (D#(+(x, y)) -> D#(x), D#(-(x, y)) -> D#(x)) (D#(+(x, y)) -> D#(x), D#(-(x, y)) -> D#(y)) (D#(+(x, y)) -> D#(x), D#(minus(x)) -> D#(x)) (D#(+(x, y)) -> D#(x), D#(div(x, y)) -> D#(x)) (D#(+(x, y)) -> D#(x), D#(div(x, y)) -> D#(y)) (D#(+(x, y)) -> D#(x), D#(ln(x)) -> D#(x))} SCCS: Scc: { D#(+(x, y)) -> D#(x), D#(+(x, y)) -> D#(y), D#(*(x, y)) -> D#(x), D#(*(x, y)) -> D#(y), D#(-(x, y)) -> D#(x), D#(-(x, y)) -> D#(y), D#(minus(x)) -> D#(x), D#(div(x, y)) -> D#(x), D#(div(x, y)) -> D#(y), D#(ln(x)) -> D#(x)} SCC: Strict: { D#(+(x, y)) -> D#(x), D#(+(x, y)) -> D#(y), D#(*(x, y)) -> D#(x), D#(*(x, y)) -> D#(y), D#(-(x, y)) -> D#(x), D#(-(x, y)) -> D#(y), D#(minus(x)) -> D#(x), D#(div(x, y)) -> D#(x), D#(div(x, y)) -> D#(y), D#(ln(x)) -> D#(x)} Weak: { D(t()) -> 1(), D(constant()) -> 0(), D(+(x, y)) -> +(D(x), D(y)), D(*(x, y)) -> +(*(y, D(x)), *(x, D(y))), D(-(x, y)) -> -(D(x), D(y)), D(minus(x)) -> minus(D(x)), D(div(x, y)) -> -(div(D(x), y), div(*(x, D(y)), pow(y, 2()))), D(pow(x, y)) -> +(*(*(y, pow(x, -(y, 1()))), D(x)), *(*(pow(x, y), ln(x)), D(y))), D(ln(x)) -> div(D(x), x)} SPSC: Simple Projection: pi(D#) = 0 Strict: { D#(+(x, y)) -> D#(y), D#(*(x, y)) -> D#(x), D#(*(x, y)) -> D#(y), D#(-(x, y)) -> D#(x), D#(-(x, y)) -> D#(y), D#(minus(x)) -> D#(x), D#(div(x, y)) -> D#(x), D#(div(x, y)) -> D#(y), D#(ln(x)) -> D#(x)} EDG: {(D#(*(x, y)) -> D#(y), D#(ln(x)) -> D#(x)) (D#(*(x, y)) -> D#(y), D#(div(x, y)) -> D#(y)) (D#(*(x, y)) -> D#(y), D#(div(x, y)) -> D#(x)) (D#(*(x, y)) -> D#(y), D#(minus(x)) -> D#(x)) (D#(*(x, y)) -> D#(y), D#(-(x, y)) -> D#(y)) (D#(*(x, y)) -> D#(y), D#(-(x, y)) -> D#(x)) (D#(*(x, y)) -> D#(y), D#(*(x, y)) -> D#(y)) (D#(*(x, y)) -> D#(y), D#(*(x, y)) -> D#(x)) (D#(*(x, y)) -> D#(y), D#(+(x, y)) -> D#(y)) (D#(div(x, y)) -> D#(y), D#(ln(x)) -> 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#(minus(x)) -> D#(x)) (D#(div(x, y)) -> D#(y), D#(-(x, y)) -> D#(y)) (D#(div(x, y)) -> D#(y), D#(-(x, y)) -> D#(x)) (D#(div(x, y)) -> D#(y), D#(*(x, y)) -> D#(y)) (D#(div(x, y)) -> D#(y), D#(*(x, y)) -> D#(x)) (D#(div(x, y)) -> D#(y), D#(+(x, y)) -> D#(y)) (D#(-(x, y)) -> D#(x), D#(ln(x)) -> D#(x)) (D#(-(x, y)) -> D#(x), D#(div(x, y)) -> D#(y)) (D#(-(x, y)) -> D#(x), D#(div(x, y)) -> D#(x)) (D#(-(x, y)) -> D#(x), D#(minus(x)) -> D#(x)) (D#(-(x, y)) -> D#(x), D#(-(x, y)) -> D#(y)) (D#(-(x, y)) -> D#(x), D#(-(x, y)) -> D#(x)) (D#(-(x, y)) -> D#(x), D#(*(x, y)) -> D#(y)) (D#(-(x, y)) -> D#(x), D#(*(x, y)) -> D#(x)) (D#(-(x, y)) -> D#(x), D#(+(x, y)) -> D#(y)) (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#(minus(x)) -> D#(x)) (D#(div(x, y)) -> D#(x), D#(-(x, y)) -> D#(y)) (D#(div(x, y)) -> D#(x), D#(-(x, y)) -> D#(x)) (D#(div(x, y)) -> D#(x), D#(*(x, y)) -> D#(y)) (D#(div(x, y)) -> D#(x), D#(*(x, y)) -> D#(x)) (D#(div(x, y)) -> D#(x), D#(+(x, y)) -> D#(y)) (D#(ln(x)) -> D#(x), D#(+(x, y)) -> D#(y)) (D#(ln(x)) -> D#(x), D#(*(x, y)) -> D#(x)) (D#(ln(x)) -> D#(x), D#(*(x, y)) -> D#(y)) (D#(ln(x)) -> D#(x), D#(-(x, y)) -> D#(x)) (D#(ln(x)) -> D#(x), D#(-(x, y)) -> D#(y)) (D#(ln(x)) -> D#(x), D#(minus(x)) -> D#(x)) (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#(minus(x)) -> D#(x), D#(+(x, y)) -> D#(y)) (D#(minus(x)) -> D#(x), D#(*(x, y)) -> D#(x)) (D#(minus(x)) -> D#(x), D#(*(x, y)) -> D#(y)) (D#(minus(x)) -> D#(x), D#(-(x, y)) -> D#(x)) (D#(minus(x)) -> D#(x), D#(-(x, y)) -> D#(y)) (D#(minus(x)) -> D#(x), D#(minus(x)) -> D#(x)) (D#(minus(x)) -> D#(x), D#(div(x, y)) -> D#(x)) (D#(minus(x)) -> D#(x), D#(div(x, y)) -> D#(y)) (D#(minus(x)) -> D#(x), D#(ln(x)) -> D#(x)) (D#(*(x, y)) -> D#(x), D#(+(x, y)) -> D#(y)) (D#(*(x, y)) -> D#(x), D#(*(x, y)) -> D#(x)) (D#(*(x, y)) -> D#(x), D#(*(x, y)) -> D#(y)) (D#(*(x, y)) -> D#(x), D#(-(x, y)) -> D#(x)) (D#(*(x, y)) -> D#(x), D#(-(x, y)) -> D#(y)) (D#(*(x, y)) -> D#(x), D#(minus(x)) -> D#(x)) (D#(*(x, y)) -> D#(x), D#(div(x, y)) -> D#(x)) (D#(*(x, y)) -> D#(x), D#(div(x, y)) -> D#(y)) (D#(*(x, y)) -> D#(x), D#(ln(x)) -> D#(x)) (D#(-(x, y)) -> D#(y), D#(+(x, y)) -> D#(y)) (D#(-(x, y)) -> D#(y), D#(*(x, y)) -> D#(x)) (D#(-(x, y)) -> D#(y), D#(*(x, y)) -> D#(y)) (D#(-(x, y)) -> D#(y), D#(-(x, y)) -> D#(x)) (D#(-(x, y)) -> D#(y), D#(-(x, y)) -> D#(y)) (D#(-(x, y)) -> D#(y), D#(minus(x)) -> D#(x)) (D#(-(x, y)) -> D#(y), D#(div(x, y)) -> D#(x)) (D#(-(x, y)) -> D#(y), D#(div(x, y)) -> D#(y)) (D#(-(x, y)) -> D#(y), D#(ln(x)) -> D#(x)) (D#(+(x, y)) -> D#(y), D#(+(x, y)) -> D#(y)) (D#(+(x, y)) -> D#(y), D#(*(x, y)) -> D#(x)) (D#(+(x, y)) -> D#(y), D#(*(x, y)) -> D#(y)) (D#(+(x, y)) -> D#(y), D#(-(x, y)) -> D#(x)) (D#(+(x, y)) -> D#(y), D#(-(x, y)) -> D#(y)) (D#(+(x, y)) -> D#(y), D#(minus(x)) -> D#(x)) (D#(+(x, y)) -> D#(y), D#(div(x, y)) -> D#(x)) (D#(+(x, y)) -> D#(y), D#(div(x, y)) -> D#(y)) (D#(+(x, y)) -> D#(y), D#(ln(x)) -> D#(x))} SCCS: Scc: { D#(+(x, y)) -> D#(y), D#(*(x, y)) -> D#(x), D#(*(x, y)) -> D#(y), D#(-(x, y)) -> D#(x), D#(-(x, y)) -> D#(y), D#(minus(x)) -> D#(x), D#(div(x, y)) -> D#(x), D#(div(x, y)) -> D#(y), D#(ln(x)) -> D#(x)} SCC: Strict: { D#(+(x, y)) -> D#(y), D#(*(x, y)) -> D#(x), D#(*(x, y)) -> D#(y), D#(-(x, y)) -> D#(x), D#(-(x, y)) -> D#(y), D#(minus(x)) -> D#(x), D#(div(x, y)) -> D#(x), D#(div(x, y)) -> D#(y), D#(ln(x)) -> D#(x)} Weak: { D(t()) -> 1(), D(constant()) -> 0(), D(+(x, y)) -> +(D(x), D(y)), D(*(x, y)) -> +(*(y, D(x)), *(x, D(y))), D(-(x, y)) -> -(D(x), D(y)), D(minus(x)) -> minus(D(x)), D(div(x, y)) -> -(div(D(x), y), div(*(x, D(y)), pow(y, 2()))), D(pow(x, y)) -> +(*(*(y, pow(x, -(y, 1()))), D(x)), *(*(pow(x, y), ln(x)), D(y))), D(ln(x)) -> div(D(x), x)} SPSC: Simple Projection: pi(D#) = 0 Strict: { D#(+(x, y)) -> D#(y), D#(*(x, y)) -> D#(x), D#(*(x, y)) -> D#(y), D#(-(x, y)) -> D#(x), D#(-(x, y)) -> D#(y), D#(minus(x)) -> D#(x), D#(div(x, y)) -> D#(x), D#(ln(x)) -> D#(x)} EDG: {(D#(*(x, y)) -> D#(y), D#(ln(x)) -> D#(x)) (D#(*(x, y)) -> D#(y), D#(div(x, y)) -> D#(x)) (D#(*(x, y)) -> D#(y), D#(minus(x)) -> D#(x)) (D#(*(x, y)) -> D#(y), D#(-(x, y)) -> D#(y)) (D#(*(x, y)) -> D#(y), D#(-(x, y)) -> D#(x)) (D#(*(x, y)) -> D#(y), D#(*(x, y)) -> D#(y)) (D#(*(x, y)) -> D#(y), D#(*(x, y)) -> D#(x)) (D#(*(x, y)) -> D#(y), D#(+(x, y)) -> D#(y)) (D#(*(x, y)) -> D#(x), D#(ln(x)) -> D#(x)) (D#(*(x, y)) -> D#(x), D#(div(x, y)) -> D#(x)) (D#(*(x, y)) -> D#(x), D#(minus(x)) -> D#(x)) (D#(*(x, y)) -> D#(x), D#(-(x, y)) -> D#(y)) (D#(*(x, y)) -> D#(x), D#(-(x, y)) -> D#(x)) (D#(*(x, y)) -> D#(x), D#(*(x, y)) -> D#(y)) (D#(*(x, y)) -> D#(x), D#(*(x, y)) -> D#(x)) (D#(*(x, y)) -> D#(x), D#(+(x, y)) -> D#(y)) (D#(minus(x)) -> D#(x), D#(ln(x)) -> D#(x)) (D#(minus(x)) -> D#(x), D#(div(x, y)) -> D#(x)) (D#(minus(x)) -> D#(x), D#(minus(x)) -> D#(x)) (D#(minus(x)) -> D#(x), D#(-(x, y)) -> D#(y)) (D#(minus(x)) -> D#(x), D#(-(x, y)) -> D#(x)) (D#(minus(x)) -> D#(x), D#(*(x, y)) -> D#(y)) (D#(minus(x)) -> D#(x), D#(*(x, y)) -> D#(x)) (D#(minus(x)) -> D#(x), D#(+(x, y)) -> D#(y)) (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#(minus(x)) -> D#(x)) (D#(ln(x)) -> D#(x), D#(-(x, y)) -> D#(y)) (D#(ln(x)) -> D#(x), D#(-(x, y)) -> D#(x)) (D#(ln(x)) -> D#(x), D#(*(x, y)) -> D#(y)) (D#(ln(x)) -> D#(x), D#(*(x, y)) -> D#(x)) (D#(ln(x)) -> D#(x), D#(+(x, y)) -> D#(y)) (D#(div(x, y)) -> D#(x), D#(+(x, y)) -> D#(y)) (D#(div(x, y)) -> D#(x), D#(*(x, y)) -> D#(x)) (D#(div(x, y)) -> D#(x), D#(*(x, y)) -> D#(y)) (D#(div(x, y)) -> D#(x), D#(-(x, y)) -> D#(x)) (D#(div(x, y)) -> D#(x), D#(-(x, y)) -> D#(y)) (D#(div(x, y)) -> D#(x), D#(minus(x)) -> D#(x)) (D#(div(x, y)) -> D#(x), D#(div(x, y)) -> D#(x)) (D#(div(x, y)) -> D#(x), D#(ln(x)) -> D#(x)) (D#(-(x, y)) -> D#(x), D#(+(x, y)) -> D#(y)) (D#(-(x, y)) -> D#(x), D#(*(x, y)) -> D#(x)) (D#(-(x, y)) -> D#(x), D#(*(x, y)) -> D#(y)) (D#(-(x, y)) -> D#(x), D#(-(x, y)) -> D#(x)) (D#(-(x, y)) -> D#(x), D#(-(x, y)) -> D#(y)) (D#(-(x, y)) -> D#(x), D#(minus(x)) -> D#(x)) (D#(-(x, y)) -> D#(x), D#(div(x, y)) -> D#(x)) (D#(-(x, y)) -> D#(x), D#(ln(x)) -> D#(x)) (D#(-(x, y)) -> D#(y), D#(+(x, y)) -> D#(y)) (D#(-(x, y)) -> D#(y), D#(*(x, y)) -> D#(x)) (D#(-(x, y)) -> D#(y), D#(*(x, y)) -> D#(y)) (D#(-(x, y)) -> D#(y), D#(-(x, y)) -> D#(x)) (D#(-(x, y)) -> D#(y), D#(-(x, y)) -> D#(y)) (D#(-(x, y)) -> D#(y), D#(minus(x)) -> D#(x)) (D#(-(x, y)) -> D#(y), D#(div(x, y)) -> D#(x)) (D#(-(x, y)) -> D#(y), D#(ln(x)) -> D#(x)) (D#(+(x, y)) -> D#(y), D#(+(x, y)) -> D#(y)) (D#(+(x, y)) -> D#(y), D#(*(x, y)) -> D#(x)) (D#(+(x, y)) -> D#(y), D#(*(x, y)) -> D#(y)) (D#(+(x, y)) -> D#(y), D#(-(x, y)) -> D#(x)) (D#(+(x, y)) -> D#(y), D#(-(x, y)) -> D#(y)) (D#(+(x, y)) -> D#(y), D#(minus(x)) -> D#(x)) (D#(+(x, y)) -> D#(y), D#(div(x, y)) -> D#(x)) (D#(+(x, y)) -> D#(y), D#(ln(x)) -> D#(x))} SCCS: Scc: { D#(+(x, y)) -> D#(y), D#(*(x, y)) -> D#(x), D#(*(x, y)) -> D#(y), D#(-(x, y)) -> D#(x), D#(-(x, y)) -> D#(y), D#(minus(x)) -> D#(x), D#(div(x, y)) -> D#(x), D#(ln(x)) -> D#(x)} SCC: Strict: { D#(+(x, y)) -> D#(y), D#(*(x, y)) -> D#(x), D#(*(x, y)) -> D#(y), D#(-(x, y)) -> D#(x), D#(-(x, y)) -> D#(y), D#(minus(x)) -> D#(x), D#(div(x, y)) -> D#(x), D#(ln(x)) -> D#(x)} Weak: { D(t()) -> 1(), D(constant()) -> 0(), D(+(x, y)) -> +(D(x), D(y)), D(*(x, y)) -> +(*(y, D(x)), *(x, D(y))), D(-(x, y)) -> -(D(x), D(y)), D(minus(x)) -> minus(D(x)), D(div(x, y)) -> -(div(D(x), y), div(*(x, D(y)), pow(y, 2()))), D(pow(x, y)) -> +(*(*(y, pow(x, -(y, 1()))), D(x)), *(*(pow(x, y), ln(x)), D(y))), D(ln(x)) -> div(D(x), x)} SPSC: Simple Projection: pi(D#) = 0 Strict: { D#(+(x, y)) -> D#(y), D#(*(x, y)) -> D#(x), D#(*(x, y)) -> D#(y), D#(-(x, y)) -> D#(x), D#(-(x, y)) -> D#(y), D#(minus(x)) -> D#(x), D#(ln(x)) -> D#(x)} EDG: {(D#(*(x, y)) -> D#(y), D#(ln(x)) -> D#(x)) (D#(*(x, y)) -> D#(y), D#(minus(x)) -> D#(x)) (D#(*(x, y)) -> D#(y), D#(-(x, y)) -> D#(y)) (D#(*(x, y)) -> D#(y), D#(-(x, y)) -> D#(x)) (D#(*(x, y)) -> D#(y), D#(*(x, y)) -> D#(y)) (D#(*(x, y)) -> D#(y), D#(*(x, y)) -> D#(x)) (D#(*(x, y)) -> D#(y), D#(+(x, y)) -> D#(y)) (D#(*(x, y)) -> D#(x), D#(ln(x)) -> D#(x)) (D#(*(x, y)) -> D#(x), D#(minus(x)) -> D#(x)) (D#(*(x, y)) -> D#(x), D#(-(x, y)) -> D#(y)) (D#(*(x, y)) -> D#(x), D#(-(x, y)) -> D#(x)) (D#(*(x, y)) -> D#(x), D#(*(x, y)) -> D#(y)) (D#(*(x, y)) -> D#(x), D#(*(x, y)) -> D#(x)) (D#(*(x, y)) -> D#(x), D#(+(x, y)) -> D#(y)) (D#(minus(x)) -> D#(x), D#(ln(x)) -> D#(x)) (D#(minus(x)) -> D#(x), D#(minus(x)) -> D#(x)) (D#(minus(x)) -> D#(x), D#(-(x, y)) -> D#(y)) (D#(minus(x)) -> D#(x), D#(-(x, y)) -> D#(x)) (D#(minus(x)) -> D#(x), D#(*(x, y)) -> D#(y)) (D#(minus(x)) -> D#(x), D#(*(x, y)) -> D#(x)) (D#(minus(x)) -> D#(x), D#(+(x, y)) -> D#(y)) (D#(ln(x)) -> D#(x), D#(+(x, y)) -> D#(y)) (D#(ln(x)) -> D#(x), D#(*(x, y)) -> D#(x)) (D#(ln(x)) -> D#(x), D#(*(x, y)) -> D#(y)) (D#(ln(x)) -> D#(x), D#(-(x, y)) -> D#(x)) (D#(ln(x)) -> D#(x), D#(-(x, y)) -> D#(y)) (D#(ln(x)) -> D#(x), D#(minus(x)) -> D#(x)) (D#(ln(x)) -> D#(x), D#(ln(x)) -> D#(x)) (D#(-(x, y)) -> D#(x), D#(+(x, y)) -> D#(y)) (D#(-(x, y)) -> D#(x), D#(*(x, y)) -> D#(x)) (D#(-(x, y)) -> D#(x), D#(*(x, y)) -> D#(y)) (D#(-(x, y)) -> D#(x), D#(-(x, y)) -> D#(x)) (D#(-(x, y)) -> D#(x), D#(-(x, y)) -> D#(y)) (D#(-(x, y)) -> D#(x), D#(minus(x)) -> D#(x)) (D#(-(x, y)) -> D#(x), D#(ln(x)) -> D#(x)) (D#(-(x, y)) -> D#(y), D#(+(x, y)) -> D#(y)) (D#(-(x, y)) -> D#(y), D#(*(x, y)) -> D#(x)) (D#(-(x, y)) -> D#(y), D#(*(x, y)) -> D#(y)) (D#(-(x, y)) -> D#(y), D#(-(x, y)) -> D#(x)) (D#(-(x, y)) -> D#(y), D#(-(x, y)) -> D#(y)) (D#(-(x, y)) -> D#(y), D#(minus(x)) -> D#(x)) (D#(-(x, y)) -> D#(y), D#(ln(x)) -> D#(x)) (D#(+(x, y)) -> D#(y), D#(+(x, y)) -> D#(y)) (D#(+(x, y)) -> D#(y), D#(*(x, y)) -> D#(x)) (D#(+(x, y)) -> D#(y), D#(*(x, y)) -> D#(y)) (D#(+(x, y)) -> D#(y), D#(-(x, y)) -> D#(x)) (D#(+(x, y)) -> D#(y), D#(-(x, y)) -> D#(y)) (D#(+(x, y)) -> D#(y), D#(minus(x)) -> D#(x)) (D#(+(x, y)) -> D#(y), D#(ln(x)) -> D#(x))} SCCS: Scc: { D#(+(x, y)) -> D#(y), D#(*(x, y)) -> D#(x), D#(*(x, y)) -> D#(y), D#(-(x, y)) -> D#(x), D#(-(x, y)) -> D#(y), D#(minus(x)) -> D#(x), D#(ln(x)) -> D#(x)} SCC: Strict: { D#(+(x, y)) -> D#(y), D#(*(x, y)) -> D#(x), D#(*(x, y)) -> D#(y), D#(-(x, y)) -> D#(x), D#(-(x, y)) -> D#(y), D#(minus(x)) -> D#(x), D#(ln(x)) -> D#(x)} Weak: { D(t()) -> 1(), D(constant()) -> 0(), D(+(x, y)) -> +(D(x), D(y)), D(*(x, y)) -> +(*(y, D(x)), *(x, D(y))), D(-(x, y)) -> -(D(x), D(y)), D(minus(x)) -> minus(D(x)), D(div(x, y)) -> -(div(D(x), y), div(*(x, D(y)), pow(y, 2()))), D(pow(x, y)) -> +(*(*(y, pow(x, -(y, 1()))), D(x)), *(*(pow(x, y), ln(x)), D(y))), D(ln(x)) -> div(D(x), x)} SPSC: Simple Projection: pi(D#) = 0 Strict: { D#(+(x, y)) -> D#(y), D#(*(x, y)) -> D#(x), D#(*(x, y)) -> D#(y), D#(-(x, y)) -> D#(x), D#(minus(x)) -> D#(x), D#(ln(x)) -> D#(x)} EDG: {(D#(-(x, y)) -> D#(x), D#(ln(x)) -> D#(x)) (D#(-(x, y)) -> D#(x), D#(minus(x)) -> D#(x)) (D#(-(x, y)) -> D#(x), D#(-(x, y)) -> D#(x)) (D#(-(x, y)) -> D#(x), D#(*(x, y)) -> D#(y)) (D#(-(x, y)) -> D#(x), D#(*(x, y)) -> D#(x)) (D#(-(x, y)) -> D#(x), D#(+(x, y)) -> D#(y)) (D#(ln(x)) -> D#(x), D#(ln(x)) -> D#(x)) (D#(ln(x)) -> D#(x), D#(minus(x)) -> D#(x)) (D#(ln(x)) -> D#(x), D#(-(x, y)) -> D#(x)) (D#(ln(x)) -> D#(x), D#(*(x, y)) -> D#(y)) (D#(ln(x)) -> D#(x), D#(*(x, y)) -> D#(x)) (D#(ln(x)) -> D#(x), D#(+(x, y)) -> D#(y)) (D#(*(x, y)) -> D#(y), D#(ln(x)) -> D#(x)) (D#(*(x, y)) -> D#(y), D#(minus(x)) -> D#(x)) (D#(*(x, y)) -> D#(y), D#(-(x, y)) -> D#(x)) (D#(*(x, y)) -> D#(y), D#(*(x, y)) -> D#(y)) (D#(*(x, y)) -> D#(y), D#(*(x, y)) -> D#(x)) (D#(*(x, y)) -> D#(y), D#(+(x, y)) -> D#(y)) (D#(+(x, y)) -> D#(y), D#(+(x, y)) -> D#(y)) (D#(+(x, y)) -> D#(y), D#(*(x, y)) -> D#(x)) (D#(+(x, y)) -> D#(y), D#(*(x, y)) -> D#(y)) (D#(+(x, y)) -> D#(y), D#(-(x, y)) -> D#(x)) (D#(+(x, y)) -> D#(y), D#(minus(x)) -> D#(x)) (D#(+(x, y)) -> D#(y), D#(ln(x)) -> D#(x)) (D#(minus(x)) -> D#(x), D#(+(x, y)) -> D#(y)) (D#(minus(x)) -> D#(x), D#(*(x, y)) -> D#(x)) (D#(minus(x)) -> D#(x), D#(*(x, y)) -> D#(y)) (D#(minus(x)) -> D#(x), D#(-(x, y)) -> D#(x)) (D#(minus(x)) -> D#(x), D#(minus(x)) -> D#(x)) (D#(minus(x)) -> D#(x), D#(ln(x)) -> D#(x)) (D#(*(x, y)) -> D#(x), D#(+(x, y)) -> D#(y)) (D#(*(x, y)) -> D#(x), D#(*(x, y)) -> D#(x)) (D#(*(x, y)) -> D#(x), D#(*(x, y)) -> D#(y)) (D#(*(x, y)) -> D#(x), D#(-(x, y)) -> D#(x)) (D#(*(x, y)) -> D#(x), D#(minus(x)) -> D#(x)) (D#(*(x, y)) -> D#(x), D#(ln(x)) -> D#(x))} SCCS: Scc: { D#(+(x, y)) -> D#(y), D#(*(x, y)) -> D#(x), D#(*(x, y)) -> D#(y), D#(-(x, y)) -> D#(x), D#(minus(x)) -> D#(x), D#(ln(x)) -> D#(x)} SCC: Strict: { D#(+(x, y)) -> D#(y), D#(*(x, y)) -> D#(x), D#(*(x, y)) -> D#(y), D#(-(x, y)) -> D#(x), D#(minus(x)) -> D#(x), D#(ln(x)) -> D#(x)} Weak: { D(t()) -> 1(), D(constant()) -> 0(), D(+(x, y)) -> +(D(x), D(y)), D(*(x, y)) -> +(*(y, D(x)), *(x, D(y))), D(-(x, y)) -> -(D(x), D(y)), D(minus(x)) -> minus(D(x)), D(div(x, y)) -> -(div(D(x), y), div(*(x, D(y)), pow(y, 2()))), D(pow(x, y)) -> +(*(*(y, pow(x, -(y, 1()))), D(x)), *(*(pow(x, y), ln(x)), D(y))), D(ln(x)) -> div(D(x), x)} SPSC: Simple Projection: pi(D#) = 0 Strict: {D#(+(x, y)) -> D#(y), D#(*(x, y)) -> D#(x), D#(*(x, y)) -> D#(y), D#(-(x, y)) -> D#(x), D#(ln(x)) -> D#(x)} EDG: {(D#(-(x, y)) -> D#(x), D#(ln(x)) -> D#(x)) (D#(-(x, y)) -> D#(x), D#(-(x, y)) -> D#(x)) (D#(-(x, y)) -> D#(x), D#(*(x, y)) -> D#(y)) (D#(-(x, y)) -> D#(x), D#(*(x, y)) -> D#(x)) (D#(-(x, y)) -> D#(x), D#(+(x, y)) -> D#(y)) (D#(+(x, y)) -> D#(y), D#(ln(x)) -> D#(x)) (D#(+(x, y)) -> D#(y), D#(-(x, y)) -> D#(x)) (D#(+(x, y)) -> D#(y), D#(*(x, y)) -> D#(y)) (D#(+(x, y)) -> D#(y), D#(*(x, y)) -> D#(x)) (D#(+(x, y)) -> D#(y), D#(+(x, y)) -> D#(y)) (D#(*(x, y)) -> D#(y), D#(+(x, y)) -> D#(y)) (D#(*(x, y)) -> D#(y), D#(*(x, y)) -> D#(x)) (D#(*(x, y)) -> D#(y), D#(*(x, y)) -> D#(y)) (D#(*(x, y)) -> D#(y), D#(-(x, y)) -> D#(x)) (D#(*(x, y)) -> D#(y), D#(ln(x)) -> D#(x)) (D#(ln(x)) -> D#(x), D#(+(x, y)) -> D#(y)) (D#(ln(x)) -> D#(x), D#(*(x, y)) -> D#(x)) (D#(ln(x)) -> D#(x), D#(*(x, y)) -> D#(y)) (D#(ln(x)) -> D#(x), D#(-(x, y)) -> D#(x)) (D#(ln(x)) -> D#(x), D#(ln(x)) -> D#(x)) (D#(*(x, y)) -> D#(x), D#(+(x, y)) -> D#(y)) (D#(*(x, y)) -> D#(x), D#(*(x, y)) -> D#(x)) (D#(*(x, y)) -> D#(x), D#(*(x, y)) -> D#(y)) (D#(*(x, y)) -> D#(x), D#(-(x, y)) -> D#(x)) (D#(*(x, y)) -> D#(x), D#(ln(x)) -> D#(x))} SCCS: Scc: {D#(+(x, y)) -> D#(y), D#(*(x, y)) -> D#(x), D#(*(x, y)) -> D#(y), D#(-(x, y)) -> D#(x), D#(ln(x)) -> D#(x)} SCC: Strict: {D#(+(x, y)) -> D#(y), D#(*(x, y)) -> D#(x), D#(*(x, y)) -> D#(y), D#(-(x, y)) -> D#(x), D#(ln(x)) -> D#(x)} Weak: { D(t()) -> 1(), D(constant()) -> 0(), D(+(x, y)) -> +(D(x), D(y)), D(*(x, y)) -> +(*(y, D(x)), *(x, D(y))), D(-(x, y)) -> -(D(x), D(y)), D(minus(x)) -> minus(D(x)), D(div(x, y)) -> -(div(D(x), y), div(*(x, D(y)), pow(y, 2()))), D(pow(x, y)) -> +(*(*(y, pow(x, -(y, 1()))), D(x)), *(*(pow(x, y), ln(x)), D(y))), D(ln(x)) -> div(D(x), x)} SPSC: Simple Projection: pi(D#) = 0 Strict: {D#(+(x, y)) -> D#(y), D#(*(x, y)) -> D#(x), D#(*(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#(*(x, y)) -> D#(y)) (D#(ln(x)) -> D#(x), D#(*(x, y)) -> D#(x)) (D#(ln(x)) -> D#(x), D#(+(x, y)) -> D#(y)) (D#(*(x, y)) -> D#(y), D#(ln(x)) -> D#(x)) (D#(*(x, y)) -> D#(y), D#(*(x, y)) -> D#(y)) (D#(*(x, y)) -> D#(y), D#(*(x, y)) -> D#(x)) (D#(*(x, y)) -> D#(y), D#(+(x, y)) -> D#(y)) (D#(+(x, y)) -> D#(y), D#(+(x, y)) -> D#(y)) (D#(+(x, y)) -> D#(y), D#(*(x, y)) -> D#(x)) (D#(+(x, y)) -> D#(y), D#(*(x, y)) -> D#(y)) (D#(+(x, y)) -> D#(y), D#(ln(x)) -> D#(x)) (D#(*(x, y)) -> D#(x), D#(+(x, y)) -> D#(y)) (D#(*(x, y)) -> D#(x), D#(*(x, y)) -> D#(x)) (D#(*(x, y)) -> D#(x), D#(*(x, y)) -> D#(y)) (D#(*(x, y)) -> D#(x), D#(ln(x)) -> D#(x))} SCCS: Scc: {D#(+(x, y)) -> D#(y), D#(*(x, y)) -> D#(x), D#(*(x, y)) -> D#(y), D#(ln(x)) -> D#(x)} SCC: Strict: {D#(+(x, y)) -> D#(y), D#(*(x, y)) -> D#(x), D#(*(x, y)) -> D#(y), D#(ln(x)) -> D#(x)} Weak: { D(t()) -> 1(), D(constant()) -> 0(), D(+(x, y)) -> +(D(x), D(y)), D(*(x, y)) -> +(*(y, D(x)), *(x, D(y))), D(-(x, y)) -> -(D(x), D(y)), D(minus(x)) -> minus(D(x)), D(div(x, y)) -> -(div(D(x), y), div(*(x, D(y)), pow(y, 2()))), D(pow(x, y)) -> +(*(*(y, pow(x, -(y, 1()))), D(x)), *(*(pow(x, y), ln(x)), D(y))), D(ln(x)) -> div(D(x), x)} SPSC: Simple Projection: pi(D#) = 0 Strict: {D#(+(x, y)) -> D#(y), D#(*(x, y)) -> D#(x), D#(*(x, y)) -> D#(y)} EDG: {(D#(*(x, y)) -> D#(y), D#(*(x, y)) -> D#(y)) (D#(*(x, y)) -> D#(y), D#(*(x, y)) -> D#(x)) (D#(*(x, y)) -> D#(y), D#(+(x, y)) -> D#(y)) (D#(*(x, y)) -> D#(x), D#(+(x, y)) -> D#(y)) (D#(*(x, y)) -> D#(x), D#(*(x, y)) -> D#(x)) (D#(*(x, y)) -> D#(x), D#(*(x, y)) -> D#(y)) (D#(+(x, y)) -> D#(y), D#(+(x, y)) -> D#(y)) (D#(+(x, y)) -> D#(y), D#(*(x, y)) -> D#(x)) (D#(+(x, y)) -> D#(y), D#(*(x, y)) -> D#(y))} SCCS: Scc: {D#(+(x, y)) -> D#(y), D#(*(x, y)) -> D#(x), D#(*(x, y)) -> D#(y)} SCC: Strict: {D#(+(x, y)) -> D#(y), D#(*(x, y)) -> D#(x), D#(*(x, y)) -> D#(y)} Weak: { D(t()) -> 1(), D(constant()) -> 0(), D(+(x, y)) -> +(D(x), D(y)), D(*(x, y)) -> +(*(y, D(x)), *(x, D(y))), D(-(x, y)) -> -(D(x), D(y)), D(minus(x)) -> minus(D(x)), D(div(x, y)) -> -(div(D(x), y), div(*(x, D(y)), pow(y, 2()))), D(pow(x, y)) -> +(*(*(y, pow(x, -(y, 1()))), D(x)), *(*(pow(x, y), ln(x)), D(y))), D(ln(x)) -> div(D(x), x)} SPSC: Simple Projection: pi(D#) = 0 Strict: {D#(+(x, y)) -> D#(y), D#(*(x, y)) -> D#(y)} EDG: {(D#(*(x, y)) -> D#(y), D#(*(x, y)) -> D#(y)) (D#(*(x, y)) -> D#(y), D#(+(x, y)) -> D#(y)) (D#(+(x, y)) -> D#(y), D#(+(x, y)) -> D#(y)) (D#(+(x, y)) -> D#(y), D#(*(x, y)) -> D#(y))} SCCS: Scc: {D#(+(x, y)) -> D#(y), D#(*(x, y)) -> D#(y)} SCC: Strict: {D#(+(x, y)) -> D#(y), D#(*(x, y)) -> D#(y)} Weak: { D(t()) -> 1(), D(constant()) -> 0(), D(+(x, y)) -> +(D(x), D(y)), D(*(x, y)) -> +(*(y, D(x)), *(x, D(y))), D(-(x, y)) -> -(D(x), D(y)), D(minus(x)) -> minus(D(x)), D(div(x, y)) -> -(div(D(x), y), div(*(x, D(y)), pow(y, 2()))), D(pow(x, y)) -> +(*(*(y, pow(x, -(y, 1()))), D(x)), *(*(pow(x, y), ln(x)), D(y))), D(ln(x)) -> div(D(x), x)} SPSC: Simple Projection: pi(D#) = 0 Strict: {D#(*(x, y)) -> D#(y)} EDG: {(D#(*(x, y)) -> D#(y), D#(*(x, y)) -> D#(y))} SCCS: Scc: {D#(*(x, y)) -> D#(y)} SCC: Strict: {D#(*(x, y)) -> D#(y)} Weak: { D(t()) -> 1(), D(constant()) -> 0(), D(+(x, y)) -> +(D(x), D(y)), D(*(x, y)) -> +(*(y, D(x)), *(x, D(y))), D(-(x, y)) -> -(D(x), D(y)), D(minus(x)) -> minus(D(x)), D(div(x, y)) -> -(div(D(x), y), div(*(x, D(y)), pow(y, 2()))), D(pow(x, y)) -> +(*(*(y, pow(x, -(y, 1()))), D(x)), *(*(pow(x, y), ln(x)), D(y))), D(ln(x)) -> div(D(x), x)} SPSC: Simple Projection: pi(D#) = 0 Strict: {} Qed