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(ln(x)) -> div(D(x), x), D(pow(x, y)) -> +(*(*(y, pow(x, -(y, 1()))), D(x)), *(*(pow(x, y), ln(x)), D(y)))} MPO: Prec: D > 2, D > pow, D > div, D > minus, D > -, D > *, D > +, D > t ~ 1, pow > ln t ~ 1, constant ~ 0 Strict: {} Weak: {} Qed