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

U101(tt, M, N) → U102(isNatKind(activate(M)), activate(M), activate(N))
U102(tt, M, N) → U103(isNat(activate(N)), activate(M), activate(N))
U103(tt, M, N) → U104(isNatKind(activate(N)), activate(M), activate(N))
U104(tt, M, N) → plus(x(activate(N), activate(M)), activate(N))
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, V1, V2) → U32(isNatKind(activate(V1)), activate(V1), activate(V2))
U32(tt, V1, V2) → U33(isNatKind(activate(V2)), activate(V1), activate(V2))
U33(tt, V1, V2) → U34(isNatKind(activate(V2)), activate(V1), activate(V2))
U34(tt, V1, V2) → U35(isNat(activate(V1)), activate(V2))
U35(tt, V2) → U36(isNat(activate(V2)))
U36(tt) → tt
U41(tt, V2) → U42(isNatKind(activate(V2)))
U42(tt) → tt
U51(tt) → tt
U61(tt, V2) → U62(isNatKind(activate(V2)))
U62(tt) → tt
U71(tt, N) → U72(isNatKind(activate(N)), activate(N))
U72(tt, N) → activate(N)
U81(tt, M, N) → U82(isNatKind(activate(M)), activate(M), activate(N))
U82(tt, M, N) → U83(isNat(activate(N)), activate(M), activate(N))
U83(tt, M, N) → U84(isNatKind(activate(N)), activate(M), activate(N))
U84(tt, M, N) → s(plus(activate(N), activate(M)))
U91(tt, N) → U92(isNatKind(activate(N)))
U92(tt) → 0
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))
isNat(n__x(V1, V2)) → U31(isNatKind(activate(V1)), activate(V1), activate(V2))
isNatKind(n__0) → tt
isNatKind(n__plus(V1, V2)) → U41(isNatKind(activate(V1)), activate(V2))
isNatKind(n__s(V1)) → U51(isNatKind(activate(V1)))
isNatKind(n__x(V1, V2)) → U61(isNatKind(activate(V1)), activate(V2))
plus(N, 0) → U71(isNat(N), N)
plus(N, s(M)) → U81(isNat(M), M, N)
x(N, 0) → U91(isNat(N), N)
x(N, s(M)) → U101(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(activate(X1), activate(X2))
activate(n__s(X)) → s(activate(X))
activate(n__x(X1, X2)) → x(activate(X1), activate(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:

U101'(tt', M, N) → U102'(isNatKind'(activate'(M)), activate'(M), activate'(N))
U102'(tt', M, N) → U103'(isNat'(activate'(N)), activate'(M), activate'(N))
U103'(tt', M, N) → U104'(isNatKind'(activate'(N)), activate'(M), activate'(N))
U104'(tt', M, N) → plus'(x'(activate'(N), activate'(M)), activate'(N))
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', V1, V2) → U32'(isNatKind'(activate'(V1)), activate'(V1), activate'(V2))
U32'(tt', V1, V2) → U33'(isNatKind'(activate'(V2)), activate'(V1), activate'(V2))
U33'(tt', V1, V2) → U34'(isNatKind'(activate'(V2)), activate'(V1), activate'(V2))
U34'(tt', V1, V2) → U35'(isNat'(activate'(V1)), activate'(V2))
U35'(tt', V2) → U36'(isNat'(activate'(V2)))
U36'(tt') → tt'
U41'(tt', V2) → U42'(isNatKind'(activate'(V2)))
U42'(tt') → tt'
U51'(tt') → tt'
U61'(tt', V2) → U62'(isNatKind'(activate'(V2)))
U62'(tt') → tt'
U71'(tt', N) → U72'(isNatKind'(activate'(N)), activate'(N))
U72'(tt', N) → activate'(N)
U81'(tt', M, N) → U82'(isNatKind'(activate'(M)), activate'(M), activate'(N))
U82'(tt', M, N) → U83'(isNat'(activate'(N)), activate'(M), activate'(N))
U83'(tt', M, N) → U84'(isNatKind'(activate'(N)), activate'(M), activate'(N))
U84'(tt', M, N) → s'(plus'(activate'(N), activate'(M)))
U91'(tt', N) → U92'(isNatKind'(activate'(N)))
U92'(tt') → 0'
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))
isNat'(n__x'(V1, V2)) → U31'(isNatKind'(activate'(V1)), activate'(V1), activate'(V2))
isNatKind'(n__0') → tt'
isNatKind'(n__plus'(V1, V2)) → U41'(isNatKind'(activate'(V1)), activate'(V2))
isNatKind'(n__s'(V1)) → U51'(isNatKind'(activate'(V1)))
isNatKind'(n__x'(V1, V2)) → U61'(isNatKind'(activate'(V1)), activate'(V2))
plus'(N, 0') → U71'(isNat'(N), N)
plus'(N, s'(M)) → U81'(isNat'(M), M, N)
x'(N, 0') → U91'(isNat'(N), N)
x'(N, s'(M)) → U101'(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'(activate'(X1), activate'(X2))
activate'(n__s'(X)) → s'(activate'(X))
activate'(n__x'(X1, X2)) → x'(activate'(X1), activate'(X2))
activate'(X) → X

Rewrite Strategy: INNERMOST

Infered types.

Rules:
U101'(tt', M, N) → U102'(isNatKind'(activate'(M)), activate'(M), activate'(N))
U102'(tt', M, N) → U103'(isNat'(activate'(N)), activate'(M), activate'(N))
U103'(tt', M, N) → U104'(isNatKind'(activate'(N)), activate'(M), activate'(N))
U104'(tt', M, N) → plus'(x'(activate'(N), activate'(M)), activate'(N))
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', V1, V2) → U32'(isNatKind'(activate'(V1)), activate'(V1), activate'(V2))
U32'(tt', V1, V2) → U33'(isNatKind'(activate'(V2)), activate'(V1), activate'(V2))
U33'(tt', V1, V2) → U34'(isNatKind'(activate'(V2)), activate'(V1), activate'(V2))
U34'(tt', V1, V2) → U35'(isNat'(activate'(V1)), activate'(V2))
U35'(tt', V2) → U36'(isNat'(activate'(V2)))
U36'(tt') → tt'
U41'(tt', V2) → U42'(isNatKind'(activate'(V2)))
U42'(tt') → tt'
U51'(tt') → tt'
U61'(tt', V2) → U62'(isNatKind'(activate'(V2)))
U62'(tt') → tt'
U71'(tt', N) → U72'(isNatKind'(activate'(N)), activate'(N))
U72'(tt', N) → activate'(N)
U81'(tt', M, N) → U82'(isNatKind'(activate'(M)), activate'(M), activate'(N))
U82'(tt', M, N) → U83'(isNat'(activate'(N)), activate'(M), activate'(N))
U83'(tt', M, N) → U84'(isNatKind'(activate'(N)), activate'(M), activate'(N))
U84'(tt', M, N) → s'(plus'(activate'(N), activate'(M)))
U91'(tt', N) → U92'(isNatKind'(activate'(N)))
U92'(tt') → 0'
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))
isNat'(n__x'(V1, V2)) → U31'(isNatKind'(activate'(V1)), activate'(V1), activate'(V2))
isNatKind'(n__0') → tt'
isNatKind'(n__plus'(V1, V2)) → U41'(isNatKind'(activate'(V1)), activate'(V2))
isNatKind'(n__s'(V1)) → U51'(isNatKind'(activate'(V1)))
isNatKind'(n__x'(V1, V2)) → U61'(isNatKind'(activate'(V1)), activate'(V2))
plus'(N, 0') → U71'(isNat'(N), N)
plus'(N, s'(M)) → U81'(isNat'(M), M, N)
x'(N, 0') → U91'(isNat'(N), N)
x'(N, s'(M)) → U101'(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'(activate'(X1), activate'(X2))
activate'(n__s'(X)) → s'(activate'(X))
activate'(n__x'(X1, X2)) → x'(activate'(X1), activate'(X2))
activate'(X) → X

Types:
U101' :: 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'
tt' :: tt'
U102' :: 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'
isNatKind' :: 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'
U103' :: 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'
isNat' :: n__0':n__plus':n__s':n__x' → tt'
U104' :: 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'
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'
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'
U11' :: tt' → n__0':n__plus':n__s':n__x' → n__0':n__plus':n__s':n__x' → tt'
U12' :: tt' → n__0':n__plus':n__s':n__x' → n__0':n__plus':n__s':n__x' → tt'
U13' :: tt' → n__0':n__plus':n__s':n__x' → n__0':n__plus':n__s':n__x' → tt'
U14' :: tt' → n__0':n__plus':n__s':n__x' → n__0':n__plus':n__s':n__x' → tt'
U15' :: tt' → n__0':n__plus':n__s':n__x' → tt'
U16' :: tt' → tt'
U21' :: tt' → n__0':n__plus':n__s':n__x' → tt'
U22' :: tt' → n__0':n__plus':n__s':n__x' → tt'
U23' :: tt' → tt'
U31' :: tt' → n__0':n__plus':n__s':n__x' → n__0':n__plus':n__s':n__x' → tt'
U32' :: tt' → n__0':n__plus':n__s':n__x' → n__0':n__plus':n__s':n__x' → tt'
U33' :: tt' → n__0':n__plus':n__s':n__x' → n__0':n__plus':n__s':n__x' → tt'
U34' :: tt' → n__0':n__plus':n__s':n__x' → n__0':n__plus':n__s':n__x' → tt'
U35' :: tt' → n__0':n__plus':n__s':n__x' → tt'
U36' :: tt' → tt'
U41' :: tt' → n__0':n__plus':n__s':n__x' → tt'
U42' :: tt' → tt'
U51' :: tt' → tt'
U61' :: tt' → n__0':n__plus':n__s':n__x' → tt'
U62' :: tt' → tt'
U71' :: tt' → 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'
U81' :: 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'
U82' :: 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'
U83' :: 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'
U84' :: 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'
U91' :: tt' → n__0':n__plus':n__s':n__x' → n__0':n__plus':n__s':n__x'
U92' :: tt' → n__0':n__plus':n__s':n__x'
0' :: 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_n__0':n__plus':n__s':n__x'1 :: n__0':n__plus':n__s':n__x'
_hole_tt'2 :: tt'
_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:
isNatKind', activate', isNat', plus', x', U71', U72', U91'

They will be analysed ascendingly in the following order:
isNatKind' = activate'
isNatKind' = isNat'
isNatKind' = plus'
isNatKind' = x'
isNatKind' = U71'
isNatKind' = U72'
isNatKind' = U91'
activate' = isNat'
activate' = plus'
activate' = x'
activate' = U71'
activate' = U72'
activate' = U91'
isNat' = plus'
isNat' = x'
isNat' = U71'
isNat' = U72'
isNat' = U91'
plus' = x'
plus' = U71'
plus' = U72'
plus' = U91'
x' = U71'
x' = U72'
x' = U91'
U71' = U72'
U71' = U91'
U72' = U91'

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', isNatKind', isNat', plus', x', U71', U72', U91'

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

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

Induction Step:
activate'(_gen_n__0':n__plus':n__s':n__x'3(+(_$n6, 1))) →_R^Ω(1)
plus'(activate'(_gen_n__0':n__plus':n__s':n__x'3(_$n6)), activate'(n__0')) →_IH
plus'(_gen_n__0':n__plus':n__s':n__x'3(_$n6), activate'(n__0')) →_R^Ω(1)
plus'(_gen_n__0':n__plus':n__s':n__x'3(_$n6), n__0') →_R^Ω(1)
n__plus'(_gen_n__0':n__plus':n__s':n__x'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':n__x'3(_n5)) → _gen_n__0':n__plus':n__s':n__x'3(_n5), rt ∈ Ω(1 + _n5)

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', isNatKind', isNat', x', U71', U72', U91'

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

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

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:
U71', isNatKind', isNat', x', U72', U91'

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

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

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

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

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

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

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

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

Induction Step:
isNatKind'(_gen_n__0':n__plus':n__s':n__x'3(+(_$n19115, 1))) →_R^Ω(1)
U41'(isNatKind'(activate'(_gen_n__0':n__plus':n__s':n__x'3(_$n19115))), activate'(n__0')) →_L^{Ω(1 + _$n19115)}
U41'(isNatKind'(_gen_n__0':n__plus':n__s':n__x'3(_$n19115)), activate'(n__0')) →_IH
U41'(tt', activate'(n__0')) →_L^Ω(1)
U41'(tt', _gen_n__0':n__plus':n__s':n__x'3(0)) →_R^Ω(1)
U42'(isNatKind'(activate'(_gen_n__0':n__plus':n__s':n__x'3(0)))) →_L^Ω(1)
U42'(isNatKind'(_gen_n__0':n__plus':n__s':n__x'3(0))) →_R^Ω(1)
U42'(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':n__x'3(_n5)) → _gen_n__0':n__plus':n__s':n__x'3(_n5), rt ∈ Ω(1 + _n5)
isNatKind'(_gen_n__0':n__plus':n__s':n__x'3(_n19114)) → tt', rt ∈ Ω(1 + _n19114 + _n19114²)

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', activate', plus', x', U71', U72', U91'

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

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', plus', U71', U72', U91'

Could not prove a rewrite lemma for the defined symbol 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:
U91', activate', plus', U71', U72'

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

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', plus', U71', U72'

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

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

Induction Step:
activate'(_gen_n__0':n__plus':n__s':n__x'3(+(_$n40108, 1))) →_R^Ω(1)
plus'(activate'(_gen_n__0':n__plus':n__s':n__x'3(_$n40108)), activate'(n__0')) →_IH
plus'(_gen_n__0':n__plus':n__s':n__x'3(_$n40108), activate'(n__0')) →_R^Ω(1)
plus'(_gen_n__0':n__plus':n__s':n__x'3(_$n40108), n__0') →_R^Ω(1)
n__plus'(_gen_n__0':n__plus':n__s':n__x'3(_$n40108), 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':n__x'3(_n40107)) → _gen_n__0':n__plus':n__s':n__x'3(_n40107), rt ∈ Ω(1 + _n40107)
isNatKind'(_gen_n__0':n__plus':n__s':n__x'3(_n19114)) → tt', rt ∈ Ω(1 + _n19114 + _n19114²)

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', U71', U72'

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:
U71', U72'

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

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

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

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