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

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)))

Rewrite Strategy: INNERMOST

Renamed function symbols to avoid clashes with predefined symbol.

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

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)))

Rewrite Strategy: INNERMOST

Infered types.

Rules:
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)))

Types:
D' :: t':1':constant':0':+':*':-':minus':div':2':pow':ln' → t':1':constant':0':+':*':-':minus':div':2':pow':ln'
t' :: t':1':constant':0':+':*':-':minus':div':2':pow':ln'
1' :: t':1':constant':0':+':*':-':minus':div':2':pow':ln'
constant' :: t':1':constant':0':+':*':-':minus':div':2':pow':ln'
0' :: t':1':constant':0':+':*':-':minus':div':2':pow':ln'
+' :: t':1':constant':0':+':*':-':minus':div':2':pow':ln' → t':1':constant':0':+':*':-':minus':div':2':pow':ln' → t':1':constant':0':+':*':-':minus':div':2':pow':ln'
*' :: t':1':constant':0':+':*':-':minus':div':2':pow':ln' → t':1':constant':0':+':*':-':minus':div':2':pow':ln' → t':1':constant':0':+':*':-':minus':div':2':pow':ln'
-' :: t':1':constant':0':+':*':-':minus':div':2':pow':ln' → t':1':constant':0':+':*':-':minus':div':2':pow':ln' → t':1':constant':0':+':*':-':minus':div':2':pow':ln'
minus' :: t':1':constant':0':+':*':-':minus':div':2':pow':ln' → t':1':constant':0':+':*':-':minus':div':2':pow':ln'
div' :: t':1':constant':0':+':*':-':minus':div':2':pow':ln' → t':1':constant':0':+':*':-':minus':div':2':pow':ln' → t':1':constant':0':+':*':-':minus':div':2':pow':ln'
pow' :: t':1':constant':0':+':*':-':minus':div':2':pow':ln' → t':1':constant':0':+':*':-':minus':div':2':pow':ln' → t':1':constant':0':+':*':-':minus':div':2':pow':ln'
2' :: t':1':constant':0':+':*':-':minus':div':2':pow':ln'
ln' :: t':1':constant':0':+':*':-':minus':div':2':pow':ln' → t':1':constant':0':+':*':-':minus':div':2':pow':ln'
_hole_t':1':constant':0':+':*':-':minus':div':2':pow':ln'1 :: t':1':constant':0':+':*':-':minus':div':2':pow':ln'
_gen_t':1':constant':0':+':*':-':minus':div':2':pow':ln'2 :: Nat → t':1':constant':0':+':*':-':minus':div':2':pow':ln'

Heuristically decided to analyse the following defined symbols:
D'

Generator Equations:
_gen_t':1':constant':0':+':*':-':minus':div':2':pow':ln'2(0) ⇔ t'
_gen_t':1':constant':0':+':*':-':minus':div':2':pow':ln'2(+(x, 1)) ⇔ +'(t', _gen_t':1':constant':0':+':*':-':minus':div':2':pow':ln'2(x))

The following defined symbols remain to be analysed:
D'

Proved the following rewrite lemma:
D'(_gen_t':1':constant':0':+':*':-':minus':div':2':pow':ln'2(_n4)) → _*3, rt ∈ Ω(_n4)

Induction Base:
D'(_gen_t':1':constant':0':+':*':-':minus':div':2':pow':ln'2(0))

Induction Step:
D'(_gen_t':1':constant':0':+':*':-':minus':div':2':pow':ln'2(+(_$n5, 1))) →_R^Ω(1)
+'(D'(t'), D'(_gen_t':1':constant':0':+':*':-':minus':div':2':pow':ln'2(_$n5))) →_R^Ω(1)
+'(1', D'(_gen_t':1':constant':0':+':*':-':minus':div':2':pow':ln'2(_$n5))) →_IH
+'(1', _*3)

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

Lemmas:
D'(_gen_t':1':constant':0':+':*':-':minus':div':2':pow':ln'2(_n4)) → _*3, rt ∈ Ω(_n4)

No more defined symbols left to analyse.

The lowerbound Ω(n) was proven with the following lemma:
D'(_gen_t':1':constant':0':+':*':-':minus':div':2':pow':ln'2(_n4)) → _*3, rt ∈ Ω(_n4)