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, V2) → U32(isNat(activate(V2)))
U32(tt) → tt
U41(tt, N) → activate(N)
U51(tt, M, N) → U52(isNat(activate(N)), activate(M), activate(N))
U52(tt, M, N) → s(plus(activate(N), activate(M)))
U61(tt) → 0
U71(tt, M, N) → U72(isNat(activate(N)), activate(M), activate(N))
U72(tt, M, N) → plus(x(activate(N), activate(M)), activate(N))
isNat(n__0) → tt
isNat(n__plus(V1, V2)) → U11(isNat(activate(V1)), activate(V2))
isNat(n__s(V1)) → U21(isNat(activate(V1)))
isNat(n__x(V1, V2)) → U31(isNat(activate(V1)), activate(V2))
plus(N, 0) → U41(isNat(N), N)
plus(N, s(M)) → U51(isNat(M), M, N)
x(N, 0) → U61(isNat(N))
x(N, s(M)) → U71(isNat(M), M, N)
0 → n__0
plus(X1, X2) → n__plus(X1, X2)
s(X) → n__s(X)
x(X1, X2) → n__x(X1, X2)
activate(n__0) → 0
activate(n__plus(X1, X2)) → plus(X1, X2)
activate(n__s(X)) → s(X)
activate(n__x(X1, X2)) → x(X1, X2)
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', V2) → U32'(isNat'(activate'(V2)))
U32'(tt') → tt'
U41'(tt', N) → activate'(N)
U51'(tt', M, N) → U52'(isNat'(activate'(N)), activate'(M), activate'(N))
U52'(tt', M, N) → s'(plus'(activate'(N), activate'(M)))
U61'(tt') → 0'
U71'(tt', M, N) → U72'(isNat'(activate'(N)), activate'(M), activate'(N))
U72'(tt', M, N) → plus'(x'(activate'(N), activate'(M)), activate'(N))
isNat'(n__0') → tt'
isNat'(n__plus'(V1, V2)) → U11'(isNat'(activate'(V1)), activate'(V2))
isNat'(n__s'(V1)) → U21'(isNat'(activate'(V1)))
isNat'(n__x'(V1, V2)) → U31'(isNat'(activate'(V1)), activate'(V2))
plus'(N, 0') → U41'(isNat'(N), N)
plus'(N, s'(M)) → U51'(isNat'(M), M, N)
x'(N, 0') → U61'(isNat'(N))
x'(N, s'(M)) → U71'(isNat'(M), M, N)
0' → n__0'
plus'(X1, X2) → n__plus'(X1, X2)
s'(X) → n__s'(X)
x'(X1, X2) → n__x'(X1, X2)
activate'(n__0') → 0'
activate'(n__plus'(X1, X2)) → plus'(X1, X2)
activate'(n__s'(X)) → s'(X)
activate'(n__x'(X1, X2)) → x'(X1, X2)
activate'(X) → X

Rewrite Strategy: INNERMOST

Infered types.

Rules:
U11'(tt', V2) → U12'(isNat'(activate'(V2)))
U12'(tt') → tt'
U21'(tt') → tt'
U31'(tt', V2) → U32'(isNat'(activate'(V2)))
U32'(tt') → tt'
U41'(tt', N) → activate'(N)
U51'(tt', M, N) → U52'(isNat'(activate'(N)), activate'(M), activate'(N))
U52'(tt', M, N) → s'(plus'(activate'(N), activate'(M)))
U61'(tt') → 0'
U71'(tt', M, N) → U72'(isNat'(activate'(N)), activate'(M), activate'(N))
U72'(tt', M, N) → plus'(x'(activate'(N), activate'(M)), activate'(N))
isNat'(n__0') → tt'
isNat'(n__plus'(V1, V2)) → U11'(isNat'(activate'(V1)), activate'(V2))
isNat'(n__s'(V1)) → U21'(isNat'(activate'(V1)))
isNat'(n__x'(V1, V2)) → U31'(isNat'(activate'(V1)), activate'(V2))
plus'(N, 0') → U41'(isNat'(N), N)
plus'(N, s'(M)) → U51'(isNat'(M), M, N)
x'(N, 0') → U61'(isNat'(N))
x'(N, s'(M)) → U71'(isNat'(M), M, N)
0' → n__0'
plus'(X1, X2) → n__plus'(X1, X2)
s'(X) → n__s'(X)
x'(X1, X2) → n__x'(X1, X2)
activate'(n__0') → 0'
activate'(n__plus'(X1, X2)) → plus'(X1, X2)
activate'(n__s'(X)) → s'(X)
activate'(n__x'(X1, X2)) → x'(X1, X2)
activate'(X) → X

Types:
U11' :: tt' → n__0':n__plus':n__s':n__x' → tt'
tt' :: tt'
U12' :: tt' → tt'
isNat' :: n__0':n__plus':n__s':n__x' → tt'
activate' :: n__0':n__plus':n__s':n__x' → n__0':n__plus':n__s':n__x'
U21' :: tt' → tt'
U31' :: tt' → n__0':n__plus':n__s':n__x' → tt'
U32' :: tt' → tt'
U41' :: tt' → n__0':n__plus':n__s':n__x' → n__0':n__plus':n__s':n__x'
U51' :: tt' → n__0':n__plus':n__s':n__x' → n__0':n__plus':n__s':n__x' → n__0':n__plus':n__s':n__x'
U52' :: tt' → n__0':n__plus':n__s':n__x' → n__0':n__plus':n__s':n__x' → n__0':n__plus':n__s':n__x'
s' :: n__0':n__plus':n__s':n__x' → n__0':n__plus':n__s':n__x'
plus' :: n__0':n__plus':n__s':n__x' → n__0':n__plus':n__s':n__x' → n__0':n__plus':n__s':n__x'
U61' :: tt' → n__0':n__plus':n__s':n__x'
0' :: n__0':n__plus':n__s':n__x'
U71' :: tt' → n__0':n__plus':n__s':n__x' → n__0':n__plus':n__s':n__x' → n__0':n__plus':n__s':n__x'
U72' :: tt' → n__0':n__plus':n__s':n__x' → n__0':n__plus':n__s':n__x' → n__0':n__plus':n__s':n__x'
x' :: n__0':n__plus':n__s':n__x' → n__0':n__plus':n__s':n__x' → n__0':n__plus':n__s':n__x'
n__0' :: n__0':n__plus':n__s':n__x'
n__plus' :: n__0':n__plus':n__s':n__x' → n__0':n__plus':n__s':n__x' → n__0':n__plus':n__s':n__x'
n__s' :: n__0':n__plus':n__s':n__x' → n__0':n__plus':n__s':n__x'
n__x' :: n__0':n__plus':n__s':n__x' → n__0':n__plus':n__s':n__x' → n__0':n__plus':n__s':n__x'
_hole_tt'1 :: tt'
_hole_n__0':n__plus':n__s':n__x'2 :: n__0':n__plus':n__s':n__x'
_gen_n__0':n__plus':n__s':n__x'3 :: Nat → n__0':n__plus':n__s':n__x'

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

Induction Step:
isNat'(_gen_n__0':n__plus':n__s':n__x'3(+(_$n372, 1))) →_R^Ω(1)
U11'(isNat'(activate'(_gen_n__0':n__plus':n__s':n__x'3(_$n372))), activate'(n__0')) →_R^Ω(1)
U11'(isNat'(_gen_n__0':n__plus':n__s':n__x'3(_$n372)), activate'(n__0')) →_IH
U11'(tt', activate'(n__0')) →_R^Ω(1)
U11'(tt', n__0') →_R^Ω(1)
U12'(isNat'(activate'(n__0'))) →_R^Ω(1)
U12'(isNat'(n__0')) →_R^Ω(1)
U12'(tt') →_R^Ω(1)
tt'

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

Lemmas:
isNat'(_gen_n__0':n__plus':n__s':n__x'3(_n371)) → tt', rt ∈ Ω(1 + _n371)

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

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

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

Lemmas:
isNat'(_gen_n__0':n__plus':n__s':n__x'3(_n371)) → tt', rt ∈ Ω(1 + _n371)

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

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

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

Lemmas:
isNat'(_gen_n__0':n__plus':n__s':n__x'3(_n371)) → tt', rt ∈ Ω(1 + _n371)

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

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

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

Lemmas:
isNat'(_gen_n__0':n__plus':n__s':n__x'3(_n371)) → tt', rt ∈ Ω(1 + _n371)

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

The following defined symbols remain to be analysed:
U41'

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

Lemmas:
isNat'(_gen_n__0':n__plus':n__s':n__x'3(_n371)) → tt', rt ∈ Ω(1 + _n371)

Generator Equations:
_gen_n__0':n__plus':n__s':n__x'3(0) ⇔ n__0'
_gen_n__0':n__plus':n__s':n__x'3(+(x, 1)) ⇔ n__plus'(_gen_n__0':n__plus':n__s':n__x'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':n__x'3(_n371)) → tt', rt ∈ Ω(1 + _n371)