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

U11(tt, V1, V2) → U12(isNatKind(activate(V1)), activate(V1), activate(V2))
U12(tt, V1, V2) → U13(isNatKind(activate(V2)), activate(V1), activate(V2))
U13(tt, V1, V2) → U14(isNatKind(activate(V2)), activate(V1), activate(V2))
U14(tt, V1, V2) → U15(isNat(activate(V1)), activate(V2))
U15(tt, V2) → U16(isNat(activate(V2)))
U16(tt) → tt
U21(tt, V1) → U22(isNatKind(activate(V1)), activate(V1))
U22(tt, V1) → U23(isNat(activate(V1)))
U23(tt) → tt
U31(tt, V2) → U32(isNatKind(activate(V2)))
U32(tt) → tt
U41(tt) → tt
U51(tt, N) → U52(isNatKind(activate(N)), activate(N))
U52(tt, N) → activate(N)
U61(tt, M, N) → U62(isNatKind(activate(M)), activate(M), activate(N))
U62(tt, M, N) → U63(isNat(activate(N)), activate(M), activate(N))
U63(tt, M, N) → U64(isNatKind(activate(N)), activate(M), activate(N))
U64(tt, M, N) → s(plus(activate(N), activate(M)))
isNat(n__0) → tt
isNat(n__plus(V1, V2)) → U11(isNatKind(activate(V1)), activate(V1), activate(V2))
isNat(n__s(V1)) → U21(isNatKind(activate(V1)), activate(V1))
isNatKind(n__0) → tt
isNatKind(n__plus(V1, V2)) → U31(isNatKind(activate(V1)), activate(V2))
isNatKind(n__s(V1)) → U41(isNatKind(activate(V1)))
plus(N, 0) → U51(isNat(N), N)
plus(N, s(M)) → U61(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', V1, V2) → U12'(isNatKind'(activate'(V1)), activate'(V1), activate'(V2))
U12'(tt', V1, V2) → U13'(isNatKind'(activate'(V2)), activate'(V1), activate'(V2))
U13'(tt', V1, V2) → U14'(isNatKind'(activate'(V2)), activate'(V1), activate'(V2))
U14'(tt', V1, V2) → U15'(isNat'(activate'(V1)), activate'(V2))
U15'(tt', V2) → U16'(isNat'(activate'(V2)))
U16'(tt') → tt'
U21'(tt', V1) → U22'(isNatKind'(activate'(V1)), activate'(V1))
U22'(tt', V1) → U23'(isNat'(activate'(V1)))
U23'(tt') → tt'
U31'(tt', V2) → U32'(isNatKind'(activate'(V2)))
U32'(tt') → tt'
U41'(tt') → tt'
U51'(tt', N) → U52'(isNatKind'(activate'(N)), activate'(N))
U52'(tt', N) → activate'(N)
U61'(tt', M, N) → U62'(isNatKind'(activate'(M)), activate'(M), activate'(N))
U62'(tt', M, N) → U63'(isNat'(activate'(N)), activate'(M), activate'(N))
U63'(tt', M, N) → U64'(isNatKind'(activate'(N)), activate'(M), activate'(N))
U64'(tt', M, N) → s'(plus'(activate'(N), activate'(M)))
isNat'(n__0') → tt'
isNat'(n__plus'(V1, V2)) → U11'(isNatKind'(activate'(V1)), activate'(V1), activate'(V2))
isNat'(n__s'(V1)) → U21'(isNatKind'(activate'(V1)), activate'(V1))
isNatKind'(n__0') → tt'
isNatKind'(n__plus'(V1, V2)) → U31'(isNatKind'(activate'(V1)), activate'(V2))
isNatKind'(n__s'(V1)) → U41'(isNatKind'(activate'(V1)))
plus'(N, 0') → U51'(isNat'(N), N)
plus'(N, s'(M)) → U61'(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', V1, V2) → U12'(isNatKind'(activate'(V1)), activate'(V1), activate'(V2))
U12'(tt', V1, V2) → U13'(isNatKind'(activate'(V2)), activate'(V1), activate'(V2))
U13'(tt', V1, V2) → U14'(isNatKind'(activate'(V2)), activate'(V1), activate'(V2))
U14'(tt', V1, V2) → U15'(isNat'(activate'(V1)), activate'(V2))
U15'(tt', V2) → U16'(isNat'(activate'(V2)))
U16'(tt') → tt'
U21'(tt', V1) → U22'(isNatKind'(activate'(V1)), activate'(V1))
U22'(tt', V1) → U23'(isNat'(activate'(V1)))
U23'(tt') → tt'
U31'(tt', V2) → U32'(isNatKind'(activate'(V2)))
U32'(tt') → tt'
U41'(tt') → tt'
U51'(tt', N) → U52'(isNatKind'(activate'(N)), activate'(N))
U52'(tt', N) → activate'(N)
U61'(tt', M, N) → U62'(isNatKind'(activate'(M)), activate'(M), activate'(N))
U62'(tt', M, N) → U63'(isNat'(activate'(N)), activate'(M), activate'(N))
U63'(tt', M, N) → U64'(isNatKind'(activate'(N)), activate'(M), activate'(N))
U64'(tt', M, N) → s'(plus'(activate'(N), activate'(M)))
isNat'(n__0') → tt'
isNat'(n__plus'(V1, V2)) → U11'(isNatKind'(activate'(V1)), activate'(V1), activate'(V2))
isNat'(n__s'(V1)) → U21'(isNatKind'(activate'(V1)), activate'(V1))
isNatKind'(n__0') → tt'
isNatKind'(n__plus'(V1, V2)) → U31'(isNatKind'(activate'(V1)), activate'(V2))
isNatKind'(n__s'(V1)) → U41'(isNatKind'(activate'(V1)))
plus'(N, 0') → U51'(isNat'(N), N)
plus'(N, s'(M)) → U61'(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' → n__0':n__plus':n__s' → tt'
tt' :: tt'
U12' :: tt' → n__0':n__plus':n__s' → n__0':n__plus':n__s' → tt'
isNatKind' :: n__0':n__plus':n__s' → tt'
activate' :: n__0':n__plus':n__s' → n__0':n__plus':n__s'
U13' :: tt' → n__0':n__plus':n__s' → n__0':n__plus':n__s' → tt'
U14' :: tt' → n__0':n__plus':n__s' → n__0':n__plus':n__s' → tt'
U15' :: tt' → n__0':n__plus':n__s' → tt'
isNat' :: n__0':n__plus':n__s' → tt'
U16' :: tt' → tt'
U21' :: tt' → n__0':n__plus':n__s' → tt'
U22' :: tt' → n__0':n__plus':n__s' → tt'
U23' :: tt' → tt'
U31' :: tt' → n__0':n__plus':n__s' → tt'
U32' :: tt' → tt'
U41' :: tt' → tt'
U51' :: tt' → n__0':n__plus':n__s' → n__0':n__plus':n__s'
U52' :: tt' → n__0':n__plus':n__s' → n__0':n__plus':n__s'
U61' :: tt' → n__0':n__plus':n__s' → n__0':n__plus':n__s' → n__0':n__plus':n__s'
U62' :: tt' → n__0':n__plus':n__s' → n__0':n__plus':n__s' → n__0':n__plus':n__s'
U63' :: tt' → n__0':n__plus':n__s' → n__0':n__plus':n__s' → n__0':n__plus':n__s'
U64' :: 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:
isNatKind', activate', isNat', U51', U52', plus'

They will be analysed ascendingly in the following order:
isNatKind' = activate'
isNatKind' = isNat'
isNatKind' = U51'
isNatKind' = U52'
isNatKind' = plus'
activate' = isNat'
activate' = U51'
activate' = U52'
activate' = plus'
isNat' = U51'
isNat' = U52'
isNat' = plus'
U51' = U52'
U51' = plus'
U52' = 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', isNatKind', isNat', U51', U52', 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', isNatKind', isNat', U51', U52'

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:
U51', isNatKind', isNat', U52'

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

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:
U52', isNatKind', isNat'

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

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:
isNatKind', isNat'

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

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

Induction Step:
isNatKind'(_gen_n__0':n__plus':n__s'3(+(_$n9018, 1))) →_R^Ω(1)
U31'(isNatKind'(activate'(_gen_n__0':n__plus':n__s'3(_$n9018))), activate'(n__0')) →_L^{Ω(1 + _$n9018)}
U31'(isNatKind'(_gen_n__0':n__plus':n__s'3(_$n9018)), activate'(n__0')) →_IH
U31'(tt', activate'(n__0')) →_L^Ω(1)
U31'(tt', _gen_n__0':n__plus':n__s'3(0)) →_R^Ω(1)
U32'(isNatKind'(activate'(_gen_n__0':n__plus':n__s'3(0)))) →_L^Ω(1)
U32'(isNatKind'(_gen_n__0':n__plus':n__s'3(0))) →_R^Ω(1)
U32'(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)
isNatKind'(_gen_n__0':n__plus':n__s'3(_n9017)) → tt', rt ∈ Ω(1 + _n9017 + _n9017²)

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', activate', U51', U52', plus'

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

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

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', U51', U52', plus'

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

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(+(_$n20939, 1))) →_R^Ω(1)
plus'(activate'(_gen_n__0':n__plus':n__s'3(_$n20939)), activate'(n__0')) →_IH
plus'(_gen_n__0':n__plus':n__s'3(_$n20939), activate'(n__0')) →_R^Ω(1)
plus'(_gen_n__0':n__plus':n__s'3(_$n20939), n__0') →_R^Ω(1)
n__plus'(_gen_n__0':n__plus':n__s'3(_$n20939), 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(_n20938)) → _gen_n__0':n__plus':n__s'3(_n20938), rt ∈ Ω(1 + _n20938)
isNatKind'(_gen_n__0':n__plus':n__s'3(_n9017)) → tt', rt ∈ Ω(1 + _n9017 + _n9017²)

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', U51', U52'

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:
U51', U52'

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

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

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

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:
isNatKind'(_gen_n__0':n__plus':n__s'3(_n9017)) → tt', rt ∈ Ω(1 + _n9017 + _n9017²)