YES Time: 0.020747 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: DP: { 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} 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)} EDG: {(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# 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# 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# 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# -(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# 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# 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# div(x, y) -> D# x, D# +(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# 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# 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# pow(x, y) -> D# x, D# -(x, y) -> D# y) (D# pow(x, y) -> D# x, D# minus 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# ln x -> D# x) (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# 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# pow(x, y) -> D# x) (D# minus x -> D# x, D# pow(x, y) -> D# y) (D# minus x -> 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# 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# pow(x, y) -> D# y, D# -(x, y) -> D# y) (D# pow(x, y) -> D# y, D# minus 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# 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# +(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)} SCCS (1): 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 (12): 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# 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# ln x -> D# x) (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# 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# 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# 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) (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# +(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)} SCCS (1): 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 (11): 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# 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# 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# 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) (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)} SCCS (1): 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 (10): 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# 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# 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# y, D# +(x, y) -> D# x) (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# +(x, y) -> D# x, D# +(x, y) -> D# x) (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# -(x, y) -> D# x, D# +(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# 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# div(x, y) -> D# x, D# +(x, y) -> 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# ln x -> D# x) (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# 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# 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# 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# 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# ln x -> D# x)} SCCS (1): 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# ln x -> D# x} SCC (9): 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# 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# 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# y, D# +(x, y) -> D# x) (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# +(x, y) -> D# x, D# +(x, y) -> D# x) (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# -(x, y) -> D# x, D# +(x, y) -> D# x) (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# 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# 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# 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# 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# 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# 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# ln x -> D# x)} SCCS (1): 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# ln x -> D# x} SCC (8): 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# 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# ln x -> D# x} EDG: {(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# +(x, y) -> D# x) (D# +(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# +(x, y) -> D# x) (D# -(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# +(x, y) -> 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# 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# 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# 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# ln x -> D# x)} SCCS (1): 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# ln x -> D# x} SCC (7): 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# 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# ln x -> D# x} EDG: {(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# 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# ln x -> D# x, 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# -(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# 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# 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# ln x -> D# x)} SCCS (1): 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# ln x -> D# x} SCC (6): 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# 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# ln x -> D# x} EDG: {(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# 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# 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# 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# 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# ln x -> D# x)} SCCS (1): Scc: {D# +(x, y) -> D# x, D# +(x, y) -> D# y, D# *(x, y) -> D# x, D# *(x, y) -> D# y, D# ln x -> D# x} SCC (5): Strict: {D# +(x, y) -> D# x, 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# 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# ln x -> D# x, 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# *(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) (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)} SCCS (1): Scc: {D# +(x, y) -> D# x, D# +(x, y) -> D# y, D# *(x, y) -> D# x, D# ln x -> D# x} SCC (4): Strict: {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# x, D# +(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# +(x, y) -> D# y) (D# +(x, y) -> D# x, D# +(x, y) -> 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# 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# ln x -> D# x)} SCCS (1): Scc: {D# +(x, y) -> D# x, D# +(x, y) -> D# y, D# ln x -> D# x} SCC (3): Strict: {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# x, 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# x) (D# +(x, y) -> D# x, D# +(x, y) -> D# x) (D# +(x, y) -> D# x, D# ln x -> D# x)} SCCS (1): Scc: {D# +(x, y) -> D# x, D# ln x -> D# x} SCC (2): Strict: {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# ln x -> D# x} EDG: {(D# ln x -> D# x, D# ln x -> D# x)} SCCS (1): Scc: {D# ln x -> D# x} SCC (1): Strict: {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: {} Qed