Runtime Complexity TRS:
The TRS R consists of the following rules:

dx(X) → one
dx(a) → zero
dx(plus(ALPHA, BETA)) → plus(dx(ALPHA), dx(BETA))
dx(times(ALPHA, BETA)) → plus(times(BETA, dx(ALPHA)), times(ALPHA, dx(BETA)))
dx(minus(ALPHA, BETA)) → minus(dx(ALPHA), dx(BETA))
dx(neg(ALPHA)) → neg(dx(ALPHA))
dx(div(ALPHA, BETA)) → minus(div(dx(ALPHA), BETA), times(ALPHA, div(dx(BETA), exp(BETA, two))))
dx(ln(ALPHA)) → div(dx(ALPHA), ALPHA)
dx(exp(ALPHA, BETA)) → plus(times(BETA, times(exp(ALPHA, minus(BETA, one)), dx(ALPHA))), times(exp(ALPHA, BETA), times(ln(ALPHA), dx(BETA))))

Rewrite Strategy: INNERMOST

Renamed function symbols to avoid clashes with predefined symbol.

Runtime Complexity TRS:
The TRS R consists of the following rules:

dx'(X) → one'
dx'(a') → zero'
dx'(plus'(ALPHA, BETA)) → plus'(dx'(ALPHA), dx'(BETA))
dx'(times'(ALPHA, BETA)) → plus'(times'(BETA, dx'(ALPHA)), times'(ALPHA, dx'(BETA)))
dx'(minus'(ALPHA, BETA)) → minus'(dx'(ALPHA), dx'(BETA))
dx'(neg'(ALPHA)) → neg'(dx'(ALPHA))
dx'(div'(ALPHA, BETA)) → minus'(div'(dx'(ALPHA), BETA), times'(ALPHA, div'(dx'(BETA), exp'(BETA, two'))))
dx'(ln'(ALPHA)) → div'(dx'(ALPHA), ALPHA)
dx'(exp'(ALPHA, BETA)) → plus'(times'(BETA, times'(exp'(ALPHA, minus'(BETA, one')), dx'(ALPHA))), times'(exp'(ALPHA, BETA), times'(ln'(ALPHA), dx'(BETA))))

Rewrite Strategy: INNERMOST

Infered types.

Rules:
dx'(X) → one'
dx'(a') → zero'
dx'(plus'(ALPHA, BETA)) → plus'(dx'(ALPHA), dx'(BETA))
dx'(times'(ALPHA, BETA)) → plus'(times'(BETA, dx'(ALPHA)), times'(ALPHA, dx'(BETA)))
dx'(minus'(ALPHA, BETA)) → minus'(dx'(ALPHA), dx'(BETA))
dx'(neg'(ALPHA)) → neg'(dx'(ALPHA))
dx'(div'(ALPHA, BETA)) → minus'(div'(dx'(ALPHA), BETA), times'(ALPHA, div'(dx'(BETA), exp'(BETA, two'))))
dx'(ln'(ALPHA)) → div'(dx'(ALPHA), ALPHA)
dx'(exp'(ALPHA, BETA)) → plus'(times'(BETA, times'(exp'(ALPHA, minus'(BETA, one')), dx'(ALPHA))), times'(exp'(ALPHA, BETA), times'(ln'(ALPHA), dx'(BETA))))

Types:
dx' :: one':a':zero':plus':times':minus':neg':div':two':exp':ln' → one':a':zero':plus':times':minus':neg':div':two':exp':ln'
one' :: one':a':zero':plus':times':minus':neg':div':two':exp':ln'
a' :: one':a':zero':plus':times':minus':neg':div':two':exp':ln'
zero' :: one':a':zero':plus':times':minus':neg':div':two':exp':ln'
plus' :: one':a':zero':plus':times':minus':neg':div':two':exp':ln' → one':a':zero':plus':times':minus':neg':div':two':exp':ln' → one':a':zero':plus':times':minus':neg':div':two':exp':ln'
times' :: one':a':zero':plus':times':minus':neg':div':two':exp':ln' → one':a':zero':plus':times':minus':neg':div':two':exp':ln' → one':a':zero':plus':times':minus':neg':div':two':exp':ln'
minus' :: one':a':zero':plus':times':minus':neg':div':two':exp':ln' → one':a':zero':plus':times':minus':neg':div':two':exp':ln' → one':a':zero':plus':times':minus':neg':div':two':exp':ln'
neg' :: one':a':zero':plus':times':minus':neg':div':two':exp':ln' → one':a':zero':plus':times':minus':neg':div':two':exp':ln'
div' :: one':a':zero':plus':times':minus':neg':div':two':exp':ln' → one':a':zero':plus':times':minus':neg':div':two':exp':ln' → one':a':zero':plus':times':minus':neg':div':two':exp':ln'
exp' :: one':a':zero':plus':times':minus':neg':div':two':exp':ln' → one':a':zero':plus':times':minus':neg':div':two':exp':ln' → one':a':zero':plus':times':minus':neg':div':two':exp':ln'
two' :: one':a':zero':plus':times':minus':neg':div':two':exp':ln'
ln' :: one':a':zero':plus':times':minus':neg':div':two':exp':ln' → one':a':zero':plus':times':minus':neg':div':two':exp':ln'
_hole_one':a':zero':plus':times':minus':neg':div':two':exp':ln'1 :: one':a':zero':plus':times':minus':neg':div':two':exp':ln'
_gen_one':a':zero':plus':times':minus':neg':div':two':exp':ln'2 :: Nat → one':a':zero':plus':times':minus':neg':div':two':exp':ln'

Heuristically decided to analyse the following defined symbols:
dx'

Generator Equations:
_gen_one':a':zero':plus':times':minus':neg':div':two':exp':ln'2(0) ⇔ a'
_gen_one':a':zero':plus':times':minus':neg':div':two':exp':ln'2(+(x, 1)) ⇔ plus'(a', _gen_one':a':zero':plus':times':minus':neg':div':two':exp':ln'2(x))

The following defined symbols remain to be analysed:
dx'

Proved the following rewrite lemma:
dx'(_gen_one':a':zero':plus':times':minus':neg':div':two':exp':ln'2(_n4)) → _*3, rt ∈ Ω(_n4)

Induction Base:
dx'(_gen_one':a':zero':plus':times':minus':neg':div':two':exp':ln'2(0))

Induction Step:
dx'(_gen_one':a':zero':plus':times':minus':neg':div':two':exp':ln'2(+(_$n5, 1))) →_R^Ω(1)
plus'(dx'(a'), dx'(_gen_one':a':zero':plus':times':minus':neg':div':two':exp':ln'2(_$n5))) →_R^Ω(1)
plus'(one', dx'(_gen_one':a':zero':plus':times':minus':neg':div':two':exp':ln'2(_$n5))) →_IH
plus'(one', _*3)

We have rt ∈ Ω(n) and sz ∈ O(n). Thus, we have irc_R ∈ Ω(n).

Lemmas:
dx'(_gen_one':a':zero':plus':times':minus':neg':div':two':exp':ln'2(_n4)) → _*3, rt ∈ Ω(_n4)

No more defined symbols left to analyse.

The lowerbound Ω(n) was proven with the following lemma:
dx'(_gen_one':a':zero':plus':times':minus':neg':div':two':exp':ln'2(_n4)) → _*3, rt ∈ Ω(_n4)