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)
0n__0
plus(X1, X2) → n__plus(X1, X2)
s(X) → n__s(X)
activate(n__0) → 0
activate(n__plus(X1, X2)) → plus(X1, X2)
activate(n__s(X)) → s(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'(X1, X2)
activate'(n__s'(X)) → s'(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'(X1, X2)
activate'(n__s'(X)) → s'(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'

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'(X1, X2)
activate'(n__s'(X)) → s'(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'

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'

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

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'(X1, X2)
activate'(n__s'(X)) → s'(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'

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'.

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'(X1, X2)
activate'(n__s'(X)) → s'(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'

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'.

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'(X1, X2)
activate'(n__s'(X)) → s'(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'

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(_n231)) → tt', rt ∈ Ω(1 + n231)

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(+(_\$n232, 1))) →RΩ(1)
U11'(isNat'(activate'(_gen_n__0':n__plus':n__s'3(_\$n232))), activate'(n__0')) →RΩ(1)
U11'(isNat'(_gen_n__0':n__plus':n__s'3(_\$n232)), 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 ircR ∈ Ω(n).

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'(X1, X2)
activate'(n__s'(X)) → s'(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'

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

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'

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

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'(X1, X2)
activate'(n__s'(X)) → s'(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'

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

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'.

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'(X1, X2)
activate'(n__s'(X)) → s'(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'

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

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'.

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'(X1, X2)
activate'(n__s'(X)) → s'(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'

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

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(_n231)) → tt', rt ∈ Ω(1 + n231)