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

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

Rewrite Strategy: INNERMOST

Infered types.

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

Types:
U11' :: tt':n__0':n__plus':n__isNatKind':n__s':n__and' → tt':n__0':n__plus':n__isNatKind':n__s':n__and' → tt':n__0':n__plus':n__isNatKind':n__s':n__and' → tt':n__0':n__plus':n__isNatKind':n__s':n__and'
tt' :: tt':n__0':n__plus':n__isNatKind':n__s':n__and'
U12' :: tt':n__0':n__plus':n__isNatKind':n__s':n__and' → tt':n__0':n__plus':n__isNatKind':n__s':n__and' → tt':n__0':n__plus':n__isNatKind':n__s':n__and'
isNat' :: tt':n__0':n__plus':n__isNatKind':n__s':n__and' → tt':n__0':n__plus':n__isNatKind':n__s':n__and'
activate' :: tt':n__0':n__plus':n__isNatKind':n__s':n__and' → tt':n__0':n__plus':n__isNatKind':n__s':n__and'
U13' :: tt':n__0':n__plus':n__isNatKind':n__s':n__and' → tt':n__0':n__plus':n__isNatKind':n__s':n__and'
U21' :: tt':n__0':n__plus':n__isNatKind':n__s':n__and' → tt':n__0':n__plus':n__isNatKind':n__s':n__and' → tt':n__0':n__plus':n__isNatKind':n__s':n__and'
U22' :: tt':n__0':n__plus':n__isNatKind':n__s':n__and' → tt':n__0':n__plus':n__isNatKind':n__s':n__and'
U31' :: tt':n__0':n__plus':n__isNatKind':n__s':n__and' → tt':n__0':n__plus':n__isNatKind':n__s':n__and' → tt':n__0':n__plus':n__isNatKind':n__s':n__and'
U41' :: tt':n__0':n__plus':n__isNatKind':n__s':n__and' → tt':n__0':n__plus':n__isNatKind':n__s':n__and' → tt':n__0':n__plus':n__isNatKind':n__s':n__and' → tt':n__0':n__plus':n__isNatKind':n__s':n__and'
s' :: tt':n__0':n__plus':n__isNatKind':n__s':n__and' → tt':n__0':n__plus':n__isNatKind':n__s':n__and'
plus' :: tt':n__0':n__plus':n__isNatKind':n__s':n__and' → tt':n__0':n__plus':n__isNatKind':n__s':n__and' → tt':n__0':n__plus':n__isNatKind':n__s':n__and'
and' :: tt':n__0':n__plus':n__isNatKind':n__s':n__and' → tt':n__0':n__plus':n__isNatKind':n__s':n__and' → tt':n__0':n__plus':n__isNatKind':n__s':n__and'
n__0' :: tt':n__0':n__plus':n__isNatKind':n__s':n__and'
n__plus' :: tt':n__0':n__plus':n__isNatKind':n__s':n__and' → tt':n__0':n__plus':n__isNatKind':n__s':n__and' → tt':n__0':n__plus':n__isNatKind':n__s':n__and'
isNatKind' :: tt':n__0':n__plus':n__isNatKind':n__s':n__and' → tt':n__0':n__plus':n__isNatKind':n__s':n__and'
n__isNatKind' :: tt':n__0':n__plus':n__isNatKind':n__s':n__and' → tt':n__0':n__plus':n__isNatKind':n__s':n__and'
n__s' :: tt':n__0':n__plus':n__isNatKind':n__s':n__and' → tt':n__0':n__plus':n__isNatKind':n__s':n__and'
0' :: tt':n__0':n__plus':n__isNatKind':n__s':n__and'
n__and' :: tt':n__0':n__plus':n__isNatKind':n__s':n__and' → tt':n__0':n__plus':n__isNatKind':n__s':n__and' → tt':n__0':n__plus':n__isNatKind':n__s':n__and'
_hole_tt':n__0':n__plus':n__isNatKind':n__s':n__and'1 :: tt':n__0':n__plus':n__isNatKind':n__s':n__and'
_gen_tt':n__0':n__plus':n__isNatKind':n__s':n__and'2 :: Nat → tt':n__0':n__plus':n__isNatKind':n__s':n__and'

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

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

Generator Equations:
_gen_tt':n__0':n__plus':n__isNatKind':n__s':n__and'2(0) ⇔ tt'
_gen_tt':n__0':n__plus':n__isNatKind':n__s':n__and'2(+(x, 1)) ⇔ n__plus'(_gen_tt':n__0':n__plus':n__isNatKind':n__s':n__and'2(x), tt')

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

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

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

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

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

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

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

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

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

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

The following defined symbols remain to be analysed:
isNatKind'

Proved the following rewrite lemma:
isNatKind'(_gen_tt':n__0':n__plus':n__isNatKind':n__s':n__and'2(+(1, _n6152))) → _*3, rt ∈ Ω(_n6152)

Induction Base:
isNatKind'(_gen_tt':n__0':n__plus':n__isNatKind':n__s':n__and'2(+(1, 0)))

Induction Step:
isNatKind'(_gen_tt':n__0':n__plus':n__isNatKind':n__s':n__and'2(+(1, +(_$n6153, 1)))) →_R^Ω(1)
and'(isNatKind'(activate'(_gen_tt':n__0':n__plus':n__isNatKind':n__s':n__and'2(+(1, _$n6153)))), n__isNatKind'(activate'(tt'))) →_R^Ω(1)
and'(isNatKind'(_gen_tt':n__0':n__plus':n__isNatKind':n__s':n__and'2(+(1, _$n6153))), n__isNatKind'(activate'(tt'))) →_IH
and'(_*3, n__isNatKind'(activate'(tt'))) →_R^Ω(1)
and'(_*3, n__isNatKind'(tt'))

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