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

sum(0) → 0
sum(s(x)) → +(sqr(s(x)), sum(x))
sqr(x) → *(x, x)
sum(s(x)) → +(*(s(x), s(x)), sum(x))

Rewrite Strategy: INNERMOST

Renamed function symbols to avoid clashes with predefined symbol.

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

sum'(0') → 0'
sum'(s'(x)) → +'(sqr'(s'(x)), sum'(x))
sqr'(x) → *'(x, x)
sum'(s'(x)) → +'(*'(s'(x), s'(x)), sum'(x))

Rewrite Strategy: INNERMOST

Sliced the following arguments:
sqr'/0
*'/0
*'/1

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

sum'(0') → 0'
sum'(s'(x)) → +'(sqr', sum'(x))
sqr' → *'
sum'(s'(x)) → +'(*', sum'(x))

Rewrite Strategy: INNERMOST

Infered types.

Rules:
sum'(0') → 0'
sum'(s'(x)) → +'(sqr', sum'(x))
sqr' → *'
sum'(s'(x)) → +'(*', sum'(x))

Types:
sum' :: 0':s':+' → 0':s':+'
0' :: 0':s':+'
s' :: 0':s':+' → 0':s':+'
+' :: *' → 0':s':+' → 0':s':+'
sqr' :: *'
*' :: *'
_hole_0':s':+'1 :: 0':s':+'
_hole_*'2 :: *'
_gen_0':s':+'3 :: Nat → 0':s':+'

Heuristically decided to analyse the following defined symbols:
sum'

Generator Equations:
_gen_0':s':+'3(0) ⇔ 0'
_gen_0':s':+'3(+(x, 1)) ⇔ s'(_gen_0':s':+'3(x))

The following defined symbols remain to be analysed:
sum'

Proved the following rewrite lemma:
sum'(_gen_0':s':+'3(_n5)) → _*4, rt ∈ Ω(_n5)

Induction Base:
sum'(_gen_0':s':+'3(0))

Induction Step:
sum'(_gen_0':s':+'3(+(_$n6, 1))) →_R^Ω(1)
+'(*', sum'(_gen_0':s':+'3(_$n6))) →_IH
+'(*', _*4)

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

Lemmas:
sum'(_gen_0':s':+'3(_n5)) → _*4, rt ∈ Ω(_n5)

Generator Equations:
_gen_0':s':+'3(0) ⇔ 0'
_gen_0':s':+'3(+(x, 1)) ⇔ s'(_gen_0':s':+'3(x))

No more defined symbols left to analyse.

The lowerbound Ω(n) was proven with the following lemma:
sum'(_gen_0':s':+'3(_n5)) → _*4, rt ∈ Ω(_n5)