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

U11(tt, M, N) → U12(tt, activate(M), activate(N))
U12(tt, M, N) → s(plus(activate(N), activate(M)))
plus(N, 0) → N
plus(N, s(M)) → U11(tt, M, N)
activate(X) → X

Rewrite Strategy: INNERMOST

Renamed function symbols to avoid clashes with predefined symbol.

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


U11'(tt', M, N) → U12'(tt', activate'(M), activate'(N))
U12'(tt', M, N) → s'(plus'(activate'(N), activate'(M)))
plus'(N, 0') → N
plus'(N, s'(M)) → U11'(tt', M, N)
activate'(X) → X

Rewrite Strategy: INNERMOST

Infered types.

Rules:
U11'(tt', M, N) → U12'(tt', activate'(M), activate'(N))
U12'(tt', M, N) → s'(plus'(activate'(N), activate'(M)))
plus'(N, 0') → N
plus'(N, s'(M)) → U11'(tt', M, N)
activate'(X) → X

Types:
U11' :: tt' → s':0' → s':0' → s':0'
tt' :: tt'
U12' :: tt' → s':0' → s':0' → s':0'
activate' :: s':0' → s':0'
s' :: s':0' → s':0'
plus' :: s':0' → s':0' → s':0'
0' :: s':0'
_hole_s':0'1 :: s':0'
_hole_tt'2 :: tt'
_gen_s':0'3 :: Nat → s':0'

Heuristically decided to analyse the following defined symbols:
plus'

Rules:
U11'(tt', M, N) → U12'(tt', activate'(M), activate'(N))
U12'(tt', M, N) → s'(plus'(activate'(N), activate'(M)))
plus'(N, 0') → N
plus'(N, s'(M)) → U11'(tt', M, N)
activate'(X) → X

Types:
U11' :: tt' → s':0' → s':0' → s':0'
tt' :: tt'
U12' :: tt' → s':0' → s':0' → s':0'
activate' :: s':0' → s':0'
s' :: s':0' → s':0'
plus' :: s':0' → s':0' → s':0'
0' :: s':0'
_hole_s':0'1 :: s':0'
_hole_tt'2 :: tt'
_gen_s':0'3 :: Nat → s':0'

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

The following defined symbols remain to be analysed:
plus'

Proved the following rewrite lemma:
plus'(_gen_s':0'3(a), _gen_s':0'3(_n5)) → _gen_s':0'3(+(_n5, a)), rt ∈ Ω(1 + n5)

Induction Base:
plus'(_gen_s':0'3(a), _gen_s':0'3(0)) →RΩ(1)
_gen_s':0'3(a)

Induction Step:
plus'(_gen_s':0'3(_a162), _gen_s':0'3(+(_$n6, 1))) →RΩ(1)
U11'(tt', _gen_s':0'3(_$n6), _gen_s':0'3(_a162)) →RΩ(1)
U12'(tt', activate'(_gen_s':0'3(_$n6)), activate'(_gen_s':0'3(_a162))) →RΩ(1)
U12'(tt', _gen_s':0'3(_$n6), activate'(_gen_s':0'3(_a162))) →RΩ(1)
U12'(tt', _gen_s':0'3(_$n6), _gen_s':0'3(_a162)) →RΩ(1)
s'(plus'(activate'(_gen_s':0'3(_a162)), activate'(_gen_s':0'3(_$n6)))) →RΩ(1)
s'(plus'(_gen_s':0'3(_a162), activate'(_gen_s':0'3(_$n6)))) →RΩ(1)
s'(plus'(_gen_s':0'3(_a162), _gen_s':0'3(_$n6))) →IH
s'(_gen_s':0'3(+(_$n6, _a162)))

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

Rules:
U11'(tt', M, N) → U12'(tt', activate'(M), activate'(N))
U12'(tt', M, N) → s'(plus'(activate'(N), activate'(M)))
plus'(N, 0') → N
plus'(N, s'(M)) → U11'(tt', M, N)
activate'(X) → X

Types:
U11' :: tt' → s':0' → s':0' → s':0'
tt' :: tt'
U12' :: tt' → s':0' → s':0' → s':0'
activate' :: s':0' → s':0'
s' :: s':0' → s':0'
plus' :: s':0' → s':0' → s':0'
0' :: s':0'
_hole_s':0'1 :: s':0'
_hole_tt'2 :: tt'
_gen_s':0'3 :: Nat → s':0'

Lemmas:
plus'(_gen_s':0'3(a), _gen_s':0'3(_n5)) → _gen_s':0'3(+(_n5, a)), rt ∈ Ω(1 + n5)

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

No more defined symbols left to analyse.

The lowerbound Ω(n) was proven with the following lemma:
plus'(_gen_s':0'3(a), _gen_s':0'3(_n5)) → _gen_s':0'3(+(_n5, a)), rt ∈ Ω(1 + n5)