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

bin(x, 0) → s(0)
bin(0, s(y)) → 0
bin(s(x), s(y)) → +(bin(x, s(y)), bin(x, y))

Rewrite Strategy: INNERMOST

Renamed function symbols to avoid clashes with predefined symbol.

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


bin'(x, 0') → s'(0')
bin'(0', s'(y)) → 0'
bin'(s'(x), s'(y)) → +'(bin'(x, s'(y)), bin'(x, y))

Rewrite Strategy: INNERMOST

Infered types.

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

Types:
bin' :: 0':s':+' → 0':s':+' → 0':s':+'
0' :: 0':s':+'
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:
bin'

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

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

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:
bin'

Proved the following rewrite lemma:
bin'(_gen_0':s':+'2(+(1, _n4)), _gen_0':s':+'2(1)) → _*3, rt ∈ Ω(n4)

Induction Base:
bin'(_gen_0':s':+'2(+(1, 0)), _gen_0':s':+'2(1))

Induction Step:
bin'(_gen_0':s':+'2(+(1, +(_$n5, 1))), _gen_0':s':+'2(1)) →RΩ(1)
+'(bin'(_gen_0':s':+'2(+(1, _$n5)), s'(_gen_0':s':+'2(0))), bin'(_gen_0':s':+'2(+(1, _$n5)), _gen_0':s':+'2(0))) →IH
+'(_*3, bin'(_gen_0':s':+'2(+(1, _$n5)), _gen_0':s':+'2(0))) →RΩ(1)
+'(_*3, s'(0'))

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

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

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

Lemmas:
bin'(_gen_0':s':+'2(+(1, _n4)), _gen_0':s':+'2(1)) → _*3, rt ∈ Ω(n4)

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.

The lowerbound Ω(n) was proven with the following lemma:
bin'(_gen_0':s':+'2(+(1, _n4)), _gen_0':s':+'2(1)) → _*3, rt ∈ Ω(n4)