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)))
U21(tt, M, N) → U22(tt, activate(M), activate(N))
U22(tt, M, N) → plus(x(activate(N), activate(M)), activate(N))
plus(N, 0) → N
plus(N, s(M)) → U11(tt, M, N)
x(N, 0) → 0
x(N, s(M)) → U21(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)))
U21'(tt', M, N) → U22'(tt', activate'(M), activate'(N))
U22'(tt', M, N) → plus'(x'(activate'(N), activate'(M)), activate'(N))
plus'(N, 0') → N
plus'(N, s'(M)) → U11'(tt', M, N)
x'(N, 0') → 0'
x'(N, s'(M)) → U21'(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)))
U21'(tt', M, N) → U22'(tt', activate'(M), activate'(N))
U22'(tt', M, N) → plus'(x'(activate'(N), activate'(M)), activate'(N))
plus'(N, 0') → N
plus'(N, s'(M)) → U11'(tt', M, N)
x'(N, 0') → 0'
x'(N, s'(M)) → U21'(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'
U21' :: tt' → s':0' → s':0' → s':0'
U22' :: tt' → s':0' → s':0' → s':0'
x' :: 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', x'

They will be analysed ascendingly in the following order:
plus' < x'

Rules:
U11'(tt', M, N) → U12'(tt', activate'(M), activate'(N))
U12'(tt', M, N) → s'(plus'(activate'(N), activate'(M)))
U21'(tt', M, N) → U22'(tt', activate'(M), activate'(N))
U22'(tt', M, N) → plus'(x'(activate'(N), activate'(M)), activate'(N))
plus'(N, 0') → N
plus'(N, s'(M)) → U11'(tt', M, N)
x'(N, 0') → 0'
x'(N, s'(M)) → U21'(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'
U21' :: tt' → s':0' → s':0' → s':0'
U22' :: tt' → s':0' → s':0' → s':0'
x' :: 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', x'

They will be analysed ascendingly in the following order:
plus' < x'

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)))
U21'(tt', M, N) → U22'(tt', activate'(M), activate'(N))
U22'(tt', M, N) → plus'(x'(activate'(N), activate'(M)), activate'(N))
plus'(N, 0') → N
plus'(N, s'(M)) → U11'(tt', M, N)
x'(N, 0') → 0'
x'(N, s'(M)) → U21'(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'
U21' :: tt' → s':0' → s':0' → s':0'
U22' :: tt' → s':0' → s':0' → s':0'
x' :: 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))

The following defined symbols remain to be analysed:
x'

Proved the following rewrite lemma:
x'(_gen_s':0'3(a), _gen_s':0'3(_n1337)) → _gen_s':0'3(*(_n1337, a)), rt ∈ Ω(1 + a1614·n1337 + n1337)

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

Induction Step:
x'(_gen_s':0'3(_a1614), _gen_s':0'3(+(_\$n1338, 1))) →RΩ(1)
U21'(tt', _gen_s':0'3(_\$n1338), _gen_s':0'3(_a1614)) →RΩ(1)
U22'(tt', activate'(_gen_s':0'3(_\$n1338)), activate'(_gen_s':0'3(_a1614))) →RΩ(1)
U22'(tt', _gen_s':0'3(_\$n1338), activate'(_gen_s':0'3(_a1614))) →RΩ(1)
U22'(tt', _gen_s':0'3(_\$n1338), _gen_s':0'3(_a1614)) →RΩ(1)
plus'(x'(activate'(_gen_s':0'3(_a1614)), activate'(_gen_s':0'3(_\$n1338))), activate'(_gen_s':0'3(_a1614))) →RΩ(1)
plus'(x'(_gen_s':0'3(_a1614), activate'(_gen_s':0'3(_\$n1338))), activate'(_gen_s':0'3(_a1614))) →RΩ(1)
plus'(x'(_gen_s':0'3(_a1614), _gen_s':0'3(_\$n1338)), activate'(_gen_s':0'3(_a1614))) →IH
plus'(_gen_s':0'3(*(_\$n1338, _a1614)), activate'(_gen_s':0'3(_a1614))) →RΩ(1)
plus'(_gen_s':0'3(*(_\$n1338, _a1614)), _gen_s':0'3(_a1614)) →LΩ(1 + a1614)
_gen_s':0'3(+(_a1614, *(_\$n1338, _a1614)))

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

Rules:
U11'(tt', M, N) → U12'(tt', activate'(M), activate'(N))
U12'(tt', M, N) → s'(plus'(activate'(N), activate'(M)))
U21'(tt', M, N) → U22'(tt', activate'(M), activate'(N))
U22'(tt', M, N) → plus'(x'(activate'(N), activate'(M)), activate'(N))
plus'(N, 0') → N
plus'(N, s'(M)) → U11'(tt', M, N)
x'(N, 0') → 0'
x'(N, s'(M)) → U21'(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'
U21' :: tt' → s':0' → s':0' → s':0'
U22' :: tt' → s':0' → s':0' → s':0'
x' :: 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)
x'(_gen_s':0'3(a), _gen_s':0'3(_n1337)) → _gen_s':0'3(*(_n1337, a)), rt ∈ Ω(1 + a1614·n1337 + n1337)

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 Ω(n2) was proven with the following lemma:
x'(_gen_s':0'3(a), _gen_s':0'3(_n1337)) → _gen_s':0'3(*(_n1337, a)), rt ∈ Ω(1 + a1614·n1337 + n1337)