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

U11(tt, V2) → U12(isNat(activate(V2)))
U12(tt) → tt
U21(tt) → tt
U31(tt, N) → activate(N)
U41(tt, M, N) → U42(isNat(activate(N)), activate(M), activate(N))
U42(tt, M, N) → s(plus(activate(N), activate(M)))
isNat(n__0) → tt
isNat(n__plus(V1, V2)) → U11(isNat(activate(V1)), activate(V2))
isNat(n__s(V1)) → U21(isNat(activate(V1)))
plus(N, 0) → U31(isNat(N), N)
plus(N, s(M)) → U41(isNat(M), M, N)
0 → n__0
plus(X1, X2) → n__plus(X1, X2)
s(X) → n__s(X)
activate(n__0) → 0
activate(n__plus(X1, X2)) → plus(activate(X1), activate(X2))
activate(n__s(X)) → s(activate(X))
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', V2) → U12'(isNat'(activate'(V2)))
U12'(tt') → tt'
U21'(tt') → tt'
U31'(tt', N) → activate'(N)
U41'(tt', M, N) → U42'(isNat'(activate'(N)), activate'(M), activate'(N))
U42'(tt', M, N) → s'(plus'(activate'(N), activate'(M)))
isNat'(n__0') → tt'
isNat'(n__plus'(V1, V2)) → U11'(isNat'(activate'(V1)), activate'(V2))
isNat'(n__s'(V1)) → U21'(isNat'(activate'(V1)))
plus'(N, 0') → U31'(isNat'(N), N)
plus'(N, s'(M)) → U41'(isNat'(M), M, N)
0' → n__0'
plus'(X1, X2) → n__plus'(X1, X2)
s'(X) → n__s'(X)
activate'(n__0') → 0'
activate'(n__plus'(X1, X2)) → plus'(activate'(X1), activate'(X2))
activate'(n__s'(X)) → s'(activate'(X))
activate'(X) → X

Rewrite Strategy: INNERMOST

Infered types.

Rules:
U11'(tt', V2) → U12'(isNat'(activate'(V2)))
U12'(tt') → tt'
U21'(tt') → tt'
U31'(tt', N) → activate'(N)
U41'(tt', M, N) → U42'(isNat'(activate'(N)), activate'(M), activate'(N))
U42'(tt', M, N) → s'(plus'(activate'(N), activate'(M)))
isNat'(n__0') → tt'
isNat'(n__plus'(V1, V2)) → U11'(isNat'(activate'(V1)), activate'(V2))
isNat'(n__s'(V1)) → U21'(isNat'(activate'(V1)))
plus'(N, 0') → U31'(isNat'(N), N)
plus'(N, s'(M)) → U41'(isNat'(M), M, N)
0' → n__0'
plus'(X1, X2) → n__plus'(X1, X2)
s'(X) → n__s'(X)
activate'(n__0') → 0'
activate'(n__plus'(X1, X2)) → plus'(activate'(X1), activate'(X2))
activate'(n__s'(X)) → s'(activate'(X))
activate'(X) → X

Types:
U11' :: tt' → n__0':n__plus':n__s' → tt'
tt' :: tt'
U12' :: tt' → tt'
isNat' :: n__0':n__plus':n__s' → tt'
activate' :: n__0':n__plus':n__s' → n__0':n__plus':n__s'
U21' :: tt' → tt'
U31' :: tt' → n__0':n__plus':n__s' → n__0':n__plus':n__s'
U41' :: tt' → n__0':n__plus':n__s' → n__0':n__plus':n__s' → n__0':n__plus':n__s'
U42' :: tt' → n__0':n__plus':n__s' → n__0':n__plus':n__s' → n__0':n__plus':n__s'
s' :: n__0':n__plus':n__s' → n__0':n__plus':n__s'
plus' :: n__0':n__plus':n__s' → n__0':n__plus':n__s' → n__0':n__plus':n__s'
n__0' :: n__0':n__plus':n__s'
n__plus' :: n__0':n__plus':n__s' → n__0':n__plus':n__s' → n__0':n__plus':n__s'
n__s' :: n__0':n__plus':n__s' → n__0':n__plus':n__s'
0' :: n__0':n__plus':n__s'
_hole_tt'1 :: tt'
_hole_n__0':n__plus':n__s'2 :: n__0':n__plus':n__s'
_gen_n__0':n__plus':n__s'3 :: Nat → n__0':n__plus':n__s'

Heuristically decided to analyse the following defined symbols:
isNat', activate', U31', plus'

They will be analysed ascendingly in the following order:
isNat' = activate'
isNat' = U31'
isNat' = plus'
activate' = U31'
activate' = plus'
U31' = plus'

Generator Equations:
_gen_n__0':n__plus':n__s'3(0) ⇔ n__0'
_gen_n__0':n__plus':n__s'3(+(x, 1)) ⇔ n__plus'(_gen_n__0':n__plus':n__s'3(x), n__0')

The following defined symbols remain to be analysed:
activate', isNat', U31', plus'

They will be analysed ascendingly in the following order:
isNat' = activate'
isNat' = U31'
isNat' = plus'
activate' = U31'
activate' = plus'
U31' = plus'

Proved the following rewrite lemma:
activate'(_gen_n__0':n__plus':n__s'3(_n5)) → _gen_n__0':n__plus':n__s'3(_n5), rt ∈ Ω(1 + _n5)

Induction Base:
activate'(_gen_n__0':n__plus':n__s'3(0)) →_R^Ω(1)
_gen_n__0':n__plus':n__s'3(0)

Induction Step:
activate'(_gen_n__0':n__plus':n__s'3(+(_$n6, 1))) →_R^Ω(1)
plus'(activate'(_gen_n__0':n__plus':n__s'3(_$n6)), activate'(n__0')) →_IH
plus'(_gen_n__0':n__plus':n__s'3(_$n6), activate'(n__0')) →_R^Ω(1)
plus'(_gen_n__0':n__plus':n__s'3(_$n6), n__0') →_R^Ω(1)
n__plus'(_gen_n__0':n__plus':n__s'3(_$n6), n__0')

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

Lemmas:
activate'(_gen_n__0':n__plus':n__s'3(_n5)) → _gen_n__0':n__plus':n__s'3(_n5), rt ∈ Ω(1 + _n5)

Generator Equations:
_gen_n__0':n__plus':n__s'3(0) ⇔ n__0'
_gen_n__0':n__plus':n__s'3(+(x, 1)) ⇔ n__plus'(_gen_n__0':n__plus':n__s'3(x), n__0')

The following defined symbols remain to be analysed:
plus', isNat', U31'

They will be analysed ascendingly in the following order:
isNat' = activate'
isNat' = U31'
isNat' = plus'
activate' = U31'
activate' = plus'
U31' = plus'

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

Lemmas:
activate'(_gen_n__0':n__plus':n__s'3(_n5)) → _gen_n__0':n__plus':n__s'3(_n5), rt ∈ Ω(1 + _n5)

Generator Equations:
_gen_n__0':n__plus':n__s'3(0) ⇔ n__0'
_gen_n__0':n__plus':n__s'3(+(x, 1)) ⇔ n__plus'(_gen_n__0':n__plus':n__s'3(x), n__0')

The following defined symbols remain to be analysed:
U31', isNat'

They will be analysed ascendingly in the following order:
isNat' = activate'
isNat' = U31'
isNat' = plus'
activate' = U31'
activate' = plus'
U31' = plus'

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

Lemmas:
activate'(_gen_n__0':n__plus':n__s'3(_n5)) → _gen_n__0':n__plus':n__s'3(_n5), rt ∈ Ω(1 + _n5)

Generator Equations:
_gen_n__0':n__plus':n__s'3(0) ⇔ n__0'
_gen_n__0':n__plus':n__s'3(+(x, 1)) ⇔ n__plus'(_gen_n__0':n__plus':n__s'3(x), n__0')

The following defined symbols remain to be analysed:
isNat'

They will be analysed ascendingly in the following order:
isNat' = activate'
isNat' = U31'
isNat' = plus'
activate' = U31'
activate' = plus'
U31' = plus'

Proved the following rewrite lemma:
isNat'(_gen_n__0':n__plus':n__s'3(_n3495)) → tt', rt ∈ Ω(1 + _n3495 + _n3495²)

Induction Base:
isNat'(_gen_n__0':n__plus':n__s'3(0)) →_R^Ω(1)
tt'

Induction Step:
isNat'(_gen_n__0':n__plus':n__s'3(+(_$n3496, 1))) →_R^Ω(1)
U11'(isNat'(activate'(_gen_n__0':n__plus':n__s'3(_$n3496))), activate'(n__0')) →_L^{Ω(1 + _$n3496)}
U11'(isNat'(_gen_n__0':n__plus':n__s'3(_$n3496)), activate'(n__0')) →_IH
U11'(tt', activate'(n__0')) →_L^Ω(1)
U11'(tt', _gen_n__0':n__plus':n__s'3(0)) →_R^Ω(1)
U12'(isNat'(activate'(_gen_n__0':n__plus':n__s'3(0)))) →_L^Ω(1)
U12'(isNat'(_gen_n__0':n__plus':n__s'3(0))) →_R^Ω(1)
U12'(tt') →_R^Ω(1)
tt'

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

Lemmas:
activate'(_gen_n__0':n__plus':n__s'3(_n5)) → _gen_n__0':n__plus':n__s'3(_n5), rt ∈ Ω(1 + _n5)
isNat'(_gen_n__0':n__plus':n__s'3(_n3495)) → tt', rt ∈ Ω(1 + _n3495 + _n3495²)

Generator Equations:
_gen_n__0':n__plus':n__s'3(0) ⇔ n__0'
_gen_n__0':n__plus':n__s'3(+(x, 1)) ⇔ n__plus'(_gen_n__0':n__plus':n__s'3(x), n__0')

The following defined symbols remain to be analysed:
activate', U31', plus'

They will be analysed ascendingly in the following order:
isNat' = activate'
isNat' = U31'
isNat' = plus'
activate' = U31'
activate' = plus'
U31' = plus'

Proved the following rewrite lemma:
activate'(_gen_n__0':n__plus':n__s'3(_n9743)) → _gen_n__0':n__plus':n__s'3(_n9743), rt ∈ Ω(1 + _n9743)

Induction Base:
activate'(_gen_n__0':n__plus':n__s'3(0)) →_R^Ω(1)
_gen_n__0':n__plus':n__s'3(0)

Induction Step:
activate'(_gen_n__0':n__plus':n__s'3(+(_$n9744, 1))) →_R^Ω(1)
plus'(activate'(_gen_n__0':n__plus':n__s'3(_$n9744)), activate'(n__0')) →_IH
plus'(_gen_n__0':n__plus':n__s'3(_$n9744), activate'(n__0')) →_R^Ω(1)
plus'(_gen_n__0':n__plus':n__s'3(_$n9744), n__0') →_R^Ω(1)
n__plus'(_gen_n__0':n__plus':n__s'3(_$n9744), n__0')

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

Lemmas:
activate'(_gen_n__0':n__plus':n__s'3(_n9743)) → _gen_n__0':n__plus':n__s'3(_n9743), rt ∈ Ω(1 + _n9743)
isNat'(_gen_n__0':n__plus':n__s'3(_n3495)) → tt', rt ∈ Ω(1 + _n3495 + _n3495²)

Generator Equations:
_gen_n__0':n__plus':n__s'3(0) ⇔ n__0'
_gen_n__0':n__plus':n__s'3(+(x, 1)) ⇔ n__plus'(_gen_n__0':n__plus':n__s'3(x), n__0')

The following defined symbols remain to be analysed:
plus', U31'

They will be analysed ascendingly in the following order:
isNat' = activate'
isNat' = U31'
isNat' = plus'
activate' = U31'
activate' = plus'
U31' = plus'

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

Generator Equations:
_gen_n__0':n__plus':n__s'3(0) ⇔ n__0'
_gen_n__0':n__plus':n__s'3(+(x, 1)) ⇔ n__plus'(_gen_n__0':n__plus':n__s'3(x), n__0')

The following defined symbols remain to be analysed:
U31'

They will be analysed ascendingly in the following order:
isNat' = activate'
isNat' = U31'
isNat' = plus'
activate' = U31'
activate' = plus'
U31' = plus'

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

Generator Equations:
_gen_n__0':n__plus':n__s'3(0) ⇔ n__0'
_gen_n__0':n__plus':n__s'3(+(x, 1)) ⇔ n__plus'(_gen_n__0':n__plus':n__s'3(x), n__0')

No more defined symbols left to analyse.

The lowerbound Ω(n²) was proven with the following lemma:
isNat'(_gen_n__0':n__plus':n__s'3(_n3495)) → tt', rt ∈ Ω(1 + _n3495 + _n3495²)