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

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

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

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

Heuristically decided to analyse the following defined symbols:
D'

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

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

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

The following defined symbols remain to be analysed:
D'

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

Induction Base:
D'(_gen_t':1':constant':0':+':*':-'2(0))

Induction Step:
D'(_gen_t':1':constant':0':+':*':-'2(+(_$n5, 1))) →RΩ(1)
+'(D'(t'), D'(_gen_t':1':constant':0':+':*':-'2(_$n5))) →RΩ(1)
+'(1', D'(_gen_t':1':constant':0':+':*':-'2(_$n5))) →IH
+'(1', _*3)

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

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

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

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

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

No more defined symbols left to analyse.

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