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

average(s(x), y) → average(x, s(y))
average(x, s(s(s(y)))) → s(average(s(x), y))
average(0, 0) → 0
average(0, s(0)) → 0
average(0, s(s(0))) → s(0)

Rewrite Strategy: INNERMOST

Renamed function symbols to avoid clashes with predefined symbol.

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

average'(s'(x), y) → average'(x, s'(y))
average'(x, s'(s'(s'(y)))) → s'(average'(s'(x), y))
average'(0', 0') → 0'
average'(0', s'(0')) → 0'
average'(0', s'(s'(0'))) → s'(0')

Rewrite Strategy: INNERMOST

Infered types.

Rules:
average'(s'(x), y) → average'(x, s'(y))
average'(x, s'(s'(s'(y)))) → s'(average'(s'(x), y))
average'(0', 0') → 0'
average'(0', s'(0')) → 0'
average'(0', s'(s'(0'))) → s'(0')

Types:
average' :: s':0' → s':0' → s':0'
s' :: s':0' → s':0'
0' :: s':0'
_hole_s':0'1 :: s':0'
_gen_s':0'2 :: Nat → s':0'

Heuristically decided to analyse the following defined symbols:
average'

Rules:
average'(s'(x), y) → average'(x, s'(y))
average'(x, s'(s'(s'(y)))) → s'(average'(s'(x), y))
average'(0', 0') → 0'
average'(0', s'(0')) → 0'
average'(0', s'(s'(0'))) → s'(0')

Types:
average' :: s':0' → s':0' → s':0'
s' :: s':0' → s':0'
0' :: s':0'
_hole_s':0'1 :: s':0'
_gen_s':0'2 :: Nat → s':0'

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

The following defined symbols remain to be analysed:
average'

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

The following conjecture could not be proven:

average'(_gen_s':0'2(+(1, _n4)), _gen_s':0'2(b)) →? _*3

Rules:
average'(s'(x), y) → average'(x, s'(y))
average'(x, s'(s'(s'(y)))) → s'(average'(s'(x), y))
average'(0', 0') → 0'
average'(0', s'(0')) → 0'
average'(0', s'(s'(0'))) → s'(0')

Types:
average' :: s':0' → s':0' → s':0'
s' :: s':0' → s':0'
0' :: s':0'
_hole_s':0'1 :: s':0'
_gen_s':0'2 :: Nat → s':0'

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

No more defined symbols left to analyse.