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

din(der(plus(X, Y))) → u21(din(der(X)), X, Y)
u21(dout(DX), X, Y) → u22(din(der(Y)), X, Y, DX)
u22(dout(DY), X, Y, DX) → dout(plus(DX, DY))
din(der(times(X, Y))) → u31(din(der(X)), X, Y)
u31(dout(DX), X, Y) → u32(din(der(Y)), X, Y, DX)
u32(dout(DY), X, Y, DX) → dout(plus(times(X, DY), times(Y, DX)))
din(der(der(X))) → u41(din(der(X)), X)
u41(dout(DX), X) → u42(din(der(DX)), X, DX)
u42(dout(DDX), X, DX) → dout(DDX)

Rewrite Strategy: INNERMOST

Renamed function symbols to avoid clashes with predefined symbol.

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

din'(der'(plus'(X, Y))) → u21'(din'(der'(X)), X, Y)
u21'(dout'(DX), X, Y) → u22'(din'(der'(Y)), X, Y, DX)
u22'(dout'(DY), X, Y, DX) → dout'(plus'(DX, DY))
din'(der'(times'(X, Y))) → u31'(din'(der'(X)), X, Y)
u31'(dout'(DX), X, Y) → u32'(din'(der'(Y)), X, Y, DX)
u32'(dout'(DY), X, Y, DX) → dout'(plus'(times'(X, DY), times'(Y, DX)))
din'(der'(der'(X))) → u41'(din'(der'(X)), X)
u41'(dout'(DX), X) → u42'(din'(der'(DX)), X, DX)
u42'(dout'(DDX), X, DX) → dout'(DDX)

Rewrite Strategy: INNERMOST

Sliced the following arguments:
u21'/1
u22'/1
u22'/2
u41'/1
u42'/1
u42'/2

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

din'(der'(plus'(X, Y))) → u21'(din'(der'(X)), Y)
u21'(dout'(DX), Y) → u22'(din'(der'(Y)), DX)
u22'(dout'(DY), DX) → dout'(plus'(DX, DY))
din'(der'(times'(X, Y))) → u31'(din'(der'(X)), X, Y)
u31'(dout'(DX), X, Y) → u32'(din'(der'(Y)), X, Y, DX)
u32'(dout'(DY), X, Y, DX) → dout'(plus'(times'(X, DY), times'(Y, DX)))
din'(der'(der'(X))) → u41'(din'(der'(X)))
u41'(dout'(DX)) → u42'(din'(der'(DX)))
u42'(dout'(DDX)) → dout'(DDX)

Rewrite Strategy: INNERMOST

Infered types.

Rules:
din'(der'(plus'(X, Y))) → u21'(din'(der'(X)), Y)
u21'(dout'(DX), Y) → u22'(din'(der'(Y)), DX)
u22'(dout'(DY), DX) → dout'(plus'(DX, DY))
din'(der'(times'(X, Y))) → u31'(din'(der'(X)), X, Y)
u31'(dout'(DX), X, Y) → u32'(din'(der'(Y)), X, Y, DX)
u32'(dout'(DY), X, Y, DX) → dout'(plus'(times'(X, DY), times'(Y, DX)))
din'(der'(der'(X))) → u41'(din'(der'(X)))
u41'(dout'(DX)) → u42'(din'(der'(DX)))
u42'(dout'(DDX)) → dout'(DDX)

Types:
din' :: plus':der':times' → dout'
der' :: plus':der':times' → plus':der':times'
plus' :: plus':der':times' → plus':der':times' → plus':der':times'
u21' :: dout' → plus':der':times' → dout'
dout' :: plus':der':times' → dout'
u22' :: dout' → plus':der':times' → dout'
times' :: plus':der':times' → plus':der':times' → plus':der':times'
u31' :: dout' → plus':der':times' → plus':der':times' → dout'
u32' :: dout' → plus':der':times' → plus':der':times' → plus':der':times' → dout'
u41' :: dout' → dout'
u42' :: dout' → dout'
_hole_dout'1 :: dout'
_hole_plus':der':times'2 :: plus':der':times'
_gen_plus':der':times'3 :: Nat → plus':der':times'

Heuristically decided to analyse the following defined symbols:
din', u41'

They will be analysed ascendingly in the following order:
din' = u41'

Generator Equations:
_gen_plus':der':times'3(0) ⇔ _hole_plus':der':times'2
_gen_plus':der':times'3(+(x, 1)) ⇔ der'(_gen_plus':der':times'3(x))

The following defined symbols remain to be analysed:
u41', din'

They will be analysed ascendingly in the following order:
din' = u41'

Could not prove a rewrite lemma for the defined symbol u41'.

Generator Equations:
_gen_plus':der':times'3(0) ⇔ _hole_plus':der':times'2
_gen_plus':der':times'3(+(x, 1)) ⇔ der'(_gen_plus':der':times'3(x))

The following defined symbols remain to be analysed:
din'

They will be analysed ascendingly in the following order:
din' = u41'

Proved the following rewrite lemma:
din'(_gen_plus':der':times'3(+(2, _n41))) → _*4, rt ∈ Ω(_n41)

Induction Base:
din'(_gen_plus':der':times'3(+(2, 0)))

Induction Step:
din'(_gen_plus':der':times'3(+(2, +(_$n42, 1)))) →_R^Ω(1)
u41'(din'(der'(_gen_plus':der':times'3(+(1, _$n42))))) →_IH
u41'(_*4)

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

Lemmas:
din'(_gen_plus':der':times'3(+(2, _n41))) → _*4, rt ∈ Ω(_n41)

Generator Equations:
_gen_plus':der':times'3(0) ⇔ _hole_plus':der':times'2
_gen_plus':der':times'3(+(x, 1)) ⇔ der'(_gen_plus':der':times'3(x))

The following defined symbols remain to be analysed:
u41'

They will be analysed ascendingly in the following order:
din' = u41'

Could not prove a rewrite lemma for the defined symbol u41'.

Lemmas:
din'(_gen_plus':der':times'3(+(2, _n41))) → _*4, rt ∈ Ω(_n41)

Generator Equations:
_gen_plus':der':times'3(0) ⇔ _hole_plus':der':times'2
_gen_plus':der':times'3(+(x, 1)) ⇔ der'(_gen_plus':der':times'3(x))

No more defined symbols left to analyse.

The lowerbound Ω(n) was proven with the following lemma:
din'(_gen_plus':der':times'3(+(2, _n41))) → _*4, rt ∈ Ω(_n41)