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

f(0) → s(0)
f(s(0)) → s(s(0))
f(s(0)) → *(s(s(0)), f(0))
f(+(x, s(0))) → +(s(s(0)), f(x))
f(+(x, y)) → *(f(x), f(y))

Rewrite Strategy: INNERMOST

Renamed function symbols to avoid clashes with predefined symbol.

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

f'(0') → s'(0')
f'(s'(0')) → s'(s'(0'))
f'(s'(0')) → *'(s'(s'(0')), f'(0'))
f'(+'(x, s'(0'))) → +'(s'(s'(0')), f'(x))
f'(+'(x, y)) → *'(f'(x), f'(y))

Rewrite Strategy: INNERMOST

Infered types.

Rules:
f'(0') → s'(0')
f'(s'(0')) → s'(s'(0'))
f'(s'(0')) → *'(s'(s'(0')), f'(0'))
f'(+'(x, s'(0'))) → +'(s'(s'(0')), f'(x))
f'(+'(x, y)) → *'(f'(x), f'(y))

Types:
f' :: 0':s':*':+' → 0':s':*':+'
0' :: 0':s':*':+'
s' :: 0':s':*':+' → 0':s':*':+'
*' :: 0':s':*':+' → 0':s':*':+' → 0':s':*':+'
+' :: 0':s':*':+' → 0':s':*':+' → 0':s':*':+'
_hole_0':s':*':+'1 :: 0':s':*':+'
_gen_0':s':*':+'2 :: Nat → 0':s':*':+'

Heuristically decided to analyse the following defined symbols:
f'

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

The following defined symbols remain to be analysed:
f'

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

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

No more defined symbols left to analyse.