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

U11(tt, N) → activate(N)
U21(tt, M, N) → s(plus(activate(N), activate(M)))
and(tt, X) → activate(X)
isNat(n__0) → tt
isNat(n__plus(V1, V2)) → and(isNat(activate(V1)), n__isNat(activate(V2)))
isNat(n__s(V1)) → isNat(activate(V1))
plus(N, 0) → U11(isNat(N), N)
plus(N, s(M)) → U21(and(isNat(M), n__isNat(N)), M, N)
0 → n__0
plus(X1, X2) → n__plus(X1, X2)
isNat(X) → n__isNat(X)
s(X) → n__s(X)
activate(n__0) → 0
activate(n__plus(X1, X2)) → plus(X1, X2)
activate(n__isNat(X)) → isNat(X)
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', N) → activate'(N)
U21'(tt', M, N) → s'(plus'(activate'(N), activate'(M)))
and'(tt', X) → activate'(X)
isNat'(n__0') → tt'
isNat'(n__plus'(V1, V2)) → and'(isNat'(activate'(V1)), n__isNat'(activate'(V2)))
isNat'(n__s'(V1)) → isNat'(activate'(V1))
plus'(N, 0') → U11'(isNat'(N), N)
plus'(N, s'(M)) → U21'(and'(isNat'(M), n__isNat'(N)), M, N)
0' → n__0'
plus'(X1, X2) → n__plus'(X1, X2)
isNat'(X) → n__isNat'(X)
s'(X) → n__s'(X)
activate'(n__0') → 0'
activate'(n__plus'(X1, X2)) → plus'(X1, X2)
activate'(n__isNat'(X)) → isNat'(X)
activate'(n__s'(X)) → s'(X)
activate'(X) → X

Rewrite Strategy: INNERMOST

Infered types.

Rules:
U11'(tt', N) → activate'(N)
U21'(tt', M, N) → s'(plus'(activate'(N), activate'(M)))
and'(tt', X) → activate'(X)
isNat'(n__0') → tt'
isNat'(n__plus'(V1, V2)) → and'(isNat'(activate'(V1)), n__isNat'(activate'(V2)))
isNat'(n__s'(V1)) → isNat'(activate'(V1))
plus'(N, 0') → U11'(isNat'(N), N)
plus'(N, s'(M)) → U21'(and'(isNat'(M), n__isNat'(N)), M, N)
0' → n__0'
plus'(X1, X2) → n__plus'(X1, X2)
isNat'(X) → n__isNat'(X)
s'(X) → n__s'(X)
activate'(n__0') → 0'
activate'(n__plus'(X1, X2)) → plus'(X1, X2)
activate'(n__isNat'(X)) → isNat'(X)
activate'(n__s'(X)) → s'(X)
activate'(X) → X

Types:
U11' :: tt':n__0':n__plus':n__isNat':n__s' → tt':n__0':n__plus':n__isNat':n__s' → tt':n__0':n__plus':n__isNat':n__s'
tt' :: tt':n__0':n__plus':n__isNat':n__s'
activate' :: tt':n__0':n__plus':n__isNat':n__s' → tt':n__0':n__plus':n__isNat':n__s'
U21' :: tt':n__0':n__plus':n__isNat':n__s' → tt':n__0':n__plus':n__isNat':n__s' → tt':n__0':n__plus':n__isNat':n__s' → tt':n__0':n__plus':n__isNat':n__s'
s' :: tt':n__0':n__plus':n__isNat':n__s' → tt':n__0':n__plus':n__isNat':n__s'
plus' :: tt':n__0':n__plus':n__isNat':n__s' → tt':n__0':n__plus':n__isNat':n__s' → tt':n__0':n__plus':n__isNat':n__s'
and' :: tt':n__0':n__plus':n__isNat':n__s' → tt':n__0':n__plus':n__isNat':n__s' → tt':n__0':n__plus':n__isNat':n__s'
isNat' :: tt':n__0':n__plus':n__isNat':n__s' → tt':n__0':n__plus':n__isNat':n__s'
n__0' :: tt':n__0':n__plus':n__isNat':n__s'
n__plus' :: tt':n__0':n__plus':n__isNat':n__s' → tt':n__0':n__plus':n__isNat':n__s' → tt':n__0':n__plus':n__isNat':n__s'
n__isNat' :: tt':n__0':n__plus':n__isNat':n__s' → tt':n__0':n__plus':n__isNat':n__s'
n__s' :: tt':n__0':n__plus':n__isNat':n__s' → tt':n__0':n__plus':n__isNat':n__s'
0' :: tt':n__0':n__plus':n__isNat':n__s'
_hole_tt':n__0':n__plus':n__isNat':n__s'1 :: tt':n__0':n__plus':n__isNat':n__s'
_gen_tt':n__0':n__plus':n__isNat':n__s'2 :: Nat → tt':n__0':n__plus':n__isNat':n__s'

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

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

Rules:
U11'(tt', N) → activate'(N)
U21'(tt', M, N) → s'(plus'(activate'(N), activate'(M)))
and'(tt', X) → activate'(X)
isNat'(n__0') → tt'
isNat'(n__plus'(V1, V2)) → and'(isNat'(activate'(V1)), n__isNat'(activate'(V2)))
isNat'(n__s'(V1)) → isNat'(activate'(V1))
plus'(N, 0') → U11'(isNat'(N), N)
plus'(N, s'(M)) → U21'(and'(isNat'(M), n__isNat'(N)), M, N)
0' → n__0'
plus'(X1, X2) → n__plus'(X1, X2)
isNat'(X) → n__isNat'(X)
s'(X) → n__s'(X)
activate'(n__0') → 0'
activate'(n__plus'(X1, X2)) → plus'(X1, X2)
activate'(n__isNat'(X)) → isNat'(X)
activate'(n__s'(X)) → s'(X)
activate'(X) → X

Types:
U11' :: tt':n__0':n__plus':n__isNat':n__s' → tt':n__0':n__plus':n__isNat':n__s' → tt':n__0':n__plus':n__isNat':n__s'
tt' :: tt':n__0':n__plus':n__isNat':n__s'
activate' :: tt':n__0':n__plus':n__isNat':n__s' → tt':n__0':n__plus':n__isNat':n__s'
U21' :: tt':n__0':n__plus':n__isNat':n__s' → tt':n__0':n__plus':n__isNat':n__s' → tt':n__0':n__plus':n__isNat':n__s' → tt':n__0':n__plus':n__isNat':n__s'
s' :: tt':n__0':n__plus':n__isNat':n__s' → tt':n__0':n__plus':n__isNat':n__s'
plus' :: tt':n__0':n__plus':n__isNat':n__s' → tt':n__0':n__plus':n__isNat':n__s' → tt':n__0':n__plus':n__isNat':n__s'
and' :: tt':n__0':n__plus':n__isNat':n__s' → tt':n__0':n__plus':n__isNat':n__s' → tt':n__0':n__plus':n__isNat':n__s'
isNat' :: tt':n__0':n__plus':n__isNat':n__s' → tt':n__0':n__plus':n__isNat':n__s'
n__0' :: tt':n__0':n__plus':n__isNat':n__s'
n__plus' :: tt':n__0':n__plus':n__isNat':n__s' → tt':n__0':n__plus':n__isNat':n__s' → tt':n__0':n__plus':n__isNat':n__s'
n__isNat' :: tt':n__0':n__plus':n__isNat':n__s' → tt':n__0':n__plus':n__isNat':n__s'
n__s' :: tt':n__0':n__plus':n__isNat':n__s' → tt':n__0':n__plus':n__isNat':n__s'
0' :: tt':n__0':n__plus':n__isNat':n__s'
_hole_tt':n__0':n__plus':n__isNat':n__s'1 :: tt':n__0':n__plus':n__isNat':n__s'
_gen_tt':n__0':n__plus':n__isNat':n__s'2 :: Nat → tt':n__0':n__plus':n__isNat':n__s'

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

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

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

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

Rules:
U11'(tt', N) → activate'(N)
U21'(tt', M, N) → s'(plus'(activate'(N), activate'(M)))
and'(tt', X) → activate'(X)
isNat'(n__0') → tt'
isNat'(n__plus'(V1, V2)) → and'(isNat'(activate'(V1)), n__isNat'(activate'(V2)))
isNat'(n__s'(V1)) → isNat'(activate'(V1))
plus'(N, 0') → U11'(isNat'(N), N)
plus'(N, s'(M)) → U21'(and'(isNat'(M), n__isNat'(N)), M, N)
0' → n__0'
plus'(X1, X2) → n__plus'(X1, X2)
isNat'(X) → n__isNat'(X)
s'(X) → n__s'(X)
activate'(n__0') → 0'
activate'(n__plus'(X1, X2)) → plus'(X1, X2)
activate'(n__isNat'(X)) → isNat'(X)
activate'(n__s'(X)) → s'(X)
activate'(X) → X

Types:
U11' :: tt':n__0':n__plus':n__isNat':n__s' → tt':n__0':n__plus':n__isNat':n__s' → tt':n__0':n__plus':n__isNat':n__s'
tt' :: tt':n__0':n__plus':n__isNat':n__s'
activate' :: tt':n__0':n__plus':n__isNat':n__s' → tt':n__0':n__plus':n__isNat':n__s'
U21' :: tt':n__0':n__plus':n__isNat':n__s' → tt':n__0':n__plus':n__isNat':n__s' → tt':n__0':n__plus':n__isNat':n__s' → tt':n__0':n__plus':n__isNat':n__s'
s' :: tt':n__0':n__plus':n__isNat':n__s' → tt':n__0':n__plus':n__isNat':n__s'
plus' :: tt':n__0':n__plus':n__isNat':n__s' → tt':n__0':n__plus':n__isNat':n__s' → tt':n__0':n__plus':n__isNat':n__s'
and' :: tt':n__0':n__plus':n__isNat':n__s' → tt':n__0':n__plus':n__isNat':n__s' → tt':n__0':n__plus':n__isNat':n__s'
isNat' :: tt':n__0':n__plus':n__isNat':n__s' → tt':n__0':n__plus':n__isNat':n__s'
n__0' :: tt':n__0':n__plus':n__isNat':n__s'
n__plus' :: tt':n__0':n__plus':n__isNat':n__s' → tt':n__0':n__plus':n__isNat':n__s' → tt':n__0':n__plus':n__isNat':n__s'
n__isNat' :: tt':n__0':n__plus':n__isNat':n__s' → tt':n__0':n__plus':n__isNat':n__s'
n__s' :: tt':n__0':n__plus':n__isNat':n__s' → tt':n__0':n__plus':n__isNat':n__s'
0' :: tt':n__0':n__plus':n__isNat':n__s'
_hole_tt':n__0':n__plus':n__isNat':n__s'1 :: tt':n__0':n__plus':n__isNat':n__s'
_gen_tt':n__0':n__plus':n__isNat':n__s'2 :: Nat → tt':n__0':n__plus':n__isNat':n__s'

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

The following defined symbols remain to be analysed:
plus', U11', and', isNat'

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

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

Rules:
U11'(tt', N) → activate'(N)
U21'(tt', M, N) → s'(plus'(activate'(N), activate'(M)))
and'(tt', X) → activate'(X)
isNat'(n__0') → tt'
isNat'(n__plus'(V1, V2)) → and'(isNat'(activate'(V1)), n__isNat'(activate'(V2)))
isNat'(n__s'(V1)) → isNat'(activate'(V1))
plus'(N, 0') → U11'(isNat'(N), N)
plus'(N, s'(M)) → U21'(and'(isNat'(M), n__isNat'(N)), M, N)
0' → n__0'
plus'(X1, X2) → n__plus'(X1, X2)
isNat'(X) → n__isNat'(X)
s'(X) → n__s'(X)
activate'(n__0') → 0'
activate'(n__plus'(X1, X2)) → plus'(X1, X2)
activate'(n__isNat'(X)) → isNat'(X)
activate'(n__s'(X)) → s'(X)
activate'(X) → X

Types:
U11' :: tt':n__0':n__plus':n__isNat':n__s' → tt':n__0':n__plus':n__isNat':n__s' → tt':n__0':n__plus':n__isNat':n__s'
tt' :: tt':n__0':n__plus':n__isNat':n__s'
activate' :: tt':n__0':n__plus':n__isNat':n__s' → tt':n__0':n__plus':n__isNat':n__s'
U21' :: tt':n__0':n__plus':n__isNat':n__s' → tt':n__0':n__plus':n__isNat':n__s' → tt':n__0':n__plus':n__isNat':n__s' → tt':n__0':n__plus':n__isNat':n__s'
s' :: tt':n__0':n__plus':n__isNat':n__s' → tt':n__0':n__plus':n__isNat':n__s'
plus' :: tt':n__0':n__plus':n__isNat':n__s' → tt':n__0':n__plus':n__isNat':n__s' → tt':n__0':n__plus':n__isNat':n__s'
and' :: tt':n__0':n__plus':n__isNat':n__s' → tt':n__0':n__plus':n__isNat':n__s' → tt':n__0':n__plus':n__isNat':n__s'
isNat' :: tt':n__0':n__plus':n__isNat':n__s' → tt':n__0':n__plus':n__isNat':n__s'
n__0' :: tt':n__0':n__plus':n__isNat':n__s'
n__plus' :: tt':n__0':n__plus':n__isNat':n__s' → tt':n__0':n__plus':n__isNat':n__s' → tt':n__0':n__plus':n__isNat':n__s'
n__isNat' :: tt':n__0':n__plus':n__isNat':n__s' → tt':n__0':n__plus':n__isNat':n__s'
n__s' :: tt':n__0':n__plus':n__isNat':n__s' → tt':n__0':n__plus':n__isNat':n__s'
0' :: tt':n__0':n__plus':n__isNat':n__s'
_hole_tt':n__0':n__plus':n__isNat':n__s'1 :: tt':n__0':n__plus':n__isNat':n__s'
_gen_tt':n__0':n__plus':n__isNat':n__s'2 :: Nat → tt':n__0':n__plus':n__isNat':n__s'

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

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

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

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

Rules:
U11'(tt', N) → activate'(N)
U21'(tt', M, N) → s'(plus'(activate'(N), activate'(M)))
and'(tt', X) → activate'(X)
isNat'(n__0') → tt'
isNat'(n__plus'(V1, V2)) → and'(isNat'(activate'(V1)), n__isNat'(activate'(V2)))
isNat'(n__s'(V1)) → isNat'(activate'(V1))
plus'(N, 0') → U11'(isNat'(N), N)
plus'(N, s'(M)) → U21'(and'(isNat'(M), n__isNat'(N)), M, N)
0' → n__0'
plus'(X1, X2) → n__plus'(X1, X2)
isNat'(X) → n__isNat'(X)
s'(X) → n__s'(X)
activate'(n__0') → 0'
activate'(n__plus'(X1, X2)) → plus'(X1, X2)
activate'(n__isNat'(X)) → isNat'(X)
activate'(n__s'(X)) → s'(X)
activate'(X) → X

Types:
U11' :: tt':n__0':n__plus':n__isNat':n__s' → tt':n__0':n__plus':n__isNat':n__s' → tt':n__0':n__plus':n__isNat':n__s'
tt' :: tt':n__0':n__plus':n__isNat':n__s'
activate' :: tt':n__0':n__plus':n__isNat':n__s' → tt':n__0':n__plus':n__isNat':n__s'
U21' :: tt':n__0':n__plus':n__isNat':n__s' → tt':n__0':n__plus':n__isNat':n__s' → tt':n__0':n__plus':n__isNat':n__s' → tt':n__0':n__plus':n__isNat':n__s'
s' :: tt':n__0':n__plus':n__isNat':n__s' → tt':n__0':n__plus':n__isNat':n__s'
plus' :: tt':n__0':n__plus':n__isNat':n__s' → tt':n__0':n__plus':n__isNat':n__s' → tt':n__0':n__plus':n__isNat':n__s'
and' :: tt':n__0':n__plus':n__isNat':n__s' → tt':n__0':n__plus':n__isNat':n__s' → tt':n__0':n__plus':n__isNat':n__s'
isNat' :: tt':n__0':n__plus':n__isNat':n__s' → tt':n__0':n__plus':n__isNat':n__s'
n__0' :: tt':n__0':n__plus':n__isNat':n__s'
n__plus' :: tt':n__0':n__plus':n__isNat':n__s' → tt':n__0':n__plus':n__isNat':n__s' → tt':n__0':n__plus':n__isNat':n__s'
n__isNat' :: tt':n__0':n__plus':n__isNat':n__s' → tt':n__0':n__plus':n__isNat':n__s'
n__s' :: tt':n__0':n__plus':n__isNat':n__s' → tt':n__0':n__plus':n__isNat':n__s'
0' :: tt':n__0':n__plus':n__isNat':n__s'
_hole_tt':n__0':n__plus':n__isNat':n__s'1 :: tt':n__0':n__plus':n__isNat':n__s'
_gen_tt':n__0':n__plus':n__isNat':n__s'2 :: Nat → tt':n__0':n__plus':n__isNat':n__s'

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

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

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

Proved the following rewrite lemma:
isNat'(_gen_tt':n__0':n__plus':n__isNat':n__s'2(_n176)) → tt', rt ∈ Ω(1 + n176)

Induction Base:
isNat'(_gen_tt':n__0':n__plus':n__isNat':n__s'2(0)) →RΩ(1)
tt'

Induction Step:
isNat'(_gen_tt':n__0':n__plus':n__isNat':n__s'2(+(_$n177, 1))) →RΩ(1)
and'(isNat'(activate'(_gen_tt':n__0':n__plus':n__isNat':n__s'2(_$n177))), n__isNat'(activate'(n__0'))) →RΩ(1)
and'(isNat'(_gen_tt':n__0':n__plus':n__isNat':n__s'2(_$n177)), n__isNat'(activate'(n__0'))) →IH
and'(tt', n__isNat'(activate'(n__0'))) →RΩ(1)
and'(tt', n__isNat'(n__0')) →RΩ(1)
activate'(n__isNat'(n__0')) →RΩ(1)
isNat'(n__0') →RΩ(1)
tt'

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

Rules:
U11'(tt', N) → activate'(N)
U21'(tt', M, N) → s'(plus'(activate'(N), activate'(M)))
and'(tt', X) → activate'(X)
isNat'(n__0') → tt'
isNat'(n__plus'(V1, V2)) → and'(isNat'(activate'(V1)), n__isNat'(activate'(V2)))
isNat'(n__s'(V1)) → isNat'(activate'(V1))
plus'(N, 0') → U11'(isNat'(N), N)
plus'(N, s'(M)) → U21'(and'(isNat'(M), n__isNat'(N)), M, N)
0' → n__0'
plus'(X1, X2) → n__plus'(X1, X2)
isNat'(X) → n__isNat'(X)
s'(X) → n__s'(X)
activate'(n__0') → 0'
activate'(n__plus'(X1, X2)) → plus'(X1, X2)
activate'(n__isNat'(X)) → isNat'(X)
activate'(n__s'(X)) → s'(X)
activate'(X) → X

Types:
U11' :: tt':n__0':n__plus':n__isNat':n__s' → tt':n__0':n__plus':n__isNat':n__s' → tt':n__0':n__plus':n__isNat':n__s'
tt' :: tt':n__0':n__plus':n__isNat':n__s'
activate' :: tt':n__0':n__plus':n__isNat':n__s' → tt':n__0':n__plus':n__isNat':n__s'
U21' :: tt':n__0':n__plus':n__isNat':n__s' → tt':n__0':n__plus':n__isNat':n__s' → tt':n__0':n__plus':n__isNat':n__s' → tt':n__0':n__plus':n__isNat':n__s'
s' :: tt':n__0':n__plus':n__isNat':n__s' → tt':n__0':n__plus':n__isNat':n__s'
plus' :: tt':n__0':n__plus':n__isNat':n__s' → tt':n__0':n__plus':n__isNat':n__s' → tt':n__0':n__plus':n__isNat':n__s'
and' :: tt':n__0':n__plus':n__isNat':n__s' → tt':n__0':n__plus':n__isNat':n__s' → tt':n__0':n__plus':n__isNat':n__s'
isNat' :: tt':n__0':n__plus':n__isNat':n__s' → tt':n__0':n__plus':n__isNat':n__s'
n__0' :: tt':n__0':n__plus':n__isNat':n__s'
n__plus' :: tt':n__0':n__plus':n__isNat':n__s' → tt':n__0':n__plus':n__isNat':n__s' → tt':n__0':n__plus':n__isNat':n__s'
n__isNat' :: tt':n__0':n__plus':n__isNat':n__s' → tt':n__0':n__plus':n__isNat':n__s'
n__s' :: tt':n__0':n__plus':n__isNat':n__s' → tt':n__0':n__plus':n__isNat':n__s'
0' :: tt':n__0':n__plus':n__isNat':n__s'
_hole_tt':n__0':n__plus':n__isNat':n__s'1 :: tt':n__0':n__plus':n__isNat':n__s'
_gen_tt':n__0':n__plus':n__isNat':n__s'2 :: Nat → tt':n__0':n__plus':n__isNat':n__s'

Lemmas:
isNat'(_gen_tt':n__0':n__plus':n__isNat':n__s'2(_n176)) → tt', rt ∈ Ω(1 + n176)

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

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

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

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

Rules:
U11'(tt', N) → activate'(N)
U21'(tt', M, N) → s'(plus'(activate'(N), activate'(M)))
and'(tt', X) → activate'(X)
isNat'(n__0') → tt'
isNat'(n__plus'(V1, V2)) → and'(isNat'(activate'(V1)), n__isNat'(activate'(V2)))
isNat'(n__s'(V1)) → isNat'(activate'(V1))
plus'(N, 0') → U11'(isNat'(N), N)
plus'(N, s'(M)) → U21'(and'(isNat'(M), n__isNat'(N)), M, N)
0' → n__0'
plus'(X1, X2) → n__plus'(X1, X2)
isNat'(X) → n__isNat'(X)
s'(X) → n__s'(X)
activate'(n__0') → 0'
activate'(n__plus'(X1, X2)) → plus'(X1, X2)
activate'(n__isNat'(X)) → isNat'(X)
activate'(n__s'(X)) → s'(X)
activate'(X) → X

Types:
U11' :: tt':n__0':n__plus':n__isNat':n__s' → tt':n__0':n__plus':n__isNat':n__s' → tt':n__0':n__plus':n__isNat':n__s'
tt' :: tt':n__0':n__plus':n__isNat':n__s'
activate' :: tt':n__0':n__plus':n__isNat':n__s' → tt':n__0':n__plus':n__isNat':n__s'
U21' :: tt':n__0':n__plus':n__isNat':n__s' → tt':n__0':n__plus':n__isNat':n__s' → tt':n__0':n__plus':n__isNat':n__s' → tt':n__0':n__plus':n__isNat':n__s'
s' :: tt':n__0':n__plus':n__isNat':n__s' → tt':n__0':n__plus':n__isNat':n__s'
plus' :: tt':n__0':n__plus':n__isNat':n__s' → tt':n__0':n__plus':n__isNat':n__s' → tt':n__0':n__plus':n__isNat':n__s'
and' :: tt':n__0':n__plus':n__isNat':n__s' → tt':n__0':n__plus':n__isNat':n__s' → tt':n__0':n__plus':n__isNat':n__s'
isNat' :: tt':n__0':n__plus':n__isNat':n__s' → tt':n__0':n__plus':n__isNat':n__s'
n__0' :: tt':n__0':n__plus':n__isNat':n__s'
n__plus' :: tt':n__0':n__plus':n__isNat':n__s' → tt':n__0':n__plus':n__isNat':n__s' → tt':n__0':n__plus':n__isNat':n__s'
n__isNat' :: tt':n__0':n__plus':n__isNat':n__s' → tt':n__0':n__plus':n__isNat':n__s'
n__s' :: tt':n__0':n__plus':n__isNat':n__s' → tt':n__0':n__plus':n__isNat':n__s'
0' :: tt':n__0':n__plus':n__isNat':n__s'
_hole_tt':n__0':n__plus':n__isNat':n__s'1 :: tt':n__0':n__plus':n__isNat':n__s'
_gen_tt':n__0':n__plus':n__isNat':n__s'2 :: Nat → tt':n__0':n__plus':n__isNat':n__s'

Lemmas:
isNat'(_gen_tt':n__0':n__plus':n__isNat':n__s'2(_n176)) → tt', rt ∈ Ω(1 + n176)

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

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

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

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

Rules:
U11'(tt', N) → activate'(N)
U21'(tt', M, N) → s'(plus'(activate'(N), activate'(M)))
and'(tt', X) → activate'(X)
isNat'(n__0') → tt'
isNat'(n__plus'(V1, V2)) → and'(isNat'(activate'(V1)), n__isNat'(activate'(V2)))
isNat'(n__s'(V1)) → isNat'(activate'(V1))
plus'(N, 0') → U11'(isNat'(N), N)
plus'(N, s'(M)) → U21'(and'(isNat'(M), n__isNat'(N)), M, N)
0' → n__0'
plus'(X1, X2) → n__plus'(X1, X2)
isNat'(X) → n__isNat'(X)
s'(X) → n__s'(X)
activate'(n__0') → 0'
activate'(n__plus'(X1, X2)) → plus'(X1, X2)
activate'(n__isNat'(X)) → isNat'(X)
activate'(n__s'(X)) → s'(X)
activate'(X) → X

Types:
U11' :: tt':n__0':n__plus':n__isNat':n__s' → tt':n__0':n__plus':n__isNat':n__s' → tt':n__0':n__plus':n__isNat':n__s'
tt' :: tt':n__0':n__plus':n__isNat':n__s'
activate' :: tt':n__0':n__plus':n__isNat':n__s' → tt':n__0':n__plus':n__isNat':n__s'
U21' :: tt':n__0':n__plus':n__isNat':n__s' → tt':n__0':n__plus':n__isNat':n__s' → tt':n__0':n__plus':n__isNat':n__s' → tt':n__0':n__plus':n__isNat':n__s'
s' :: tt':n__0':n__plus':n__isNat':n__s' → tt':n__0':n__plus':n__isNat':n__s'
plus' :: tt':n__0':n__plus':n__isNat':n__s' → tt':n__0':n__plus':n__isNat':n__s' → tt':n__0':n__plus':n__isNat':n__s'
and' :: tt':n__0':n__plus':n__isNat':n__s' → tt':n__0':n__plus':n__isNat':n__s' → tt':n__0':n__plus':n__isNat':n__s'
isNat' :: tt':n__0':n__plus':n__isNat':n__s' → tt':n__0':n__plus':n__isNat':n__s'
n__0' :: tt':n__0':n__plus':n__isNat':n__s'
n__plus' :: tt':n__0':n__plus':n__isNat':n__s' → tt':n__0':n__plus':n__isNat':n__s' → tt':n__0':n__plus':n__isNat':n__s'
n__isNat' :: tt':n__0':n__plus':n__isNat':n__s' → tt':n__0':n__plus':n__isNat':n__s'
n__s' :: tt':n__0':n__plus':n__isNat':n__s' → tt':n__0':n__plus':n__isNat':n__s'
0' :: tt':n__0':n__plus':n__isNat':n__s'
_hole_tt':n__0':n__plus':n__isNat':n__s'1 :: tt':n__0':n__plus':n__isNat':n__s'
_gen_tt':n__0':n__plus':n__isNat':n__s'2 :: Nat → tt':n__0':n__plus':n__isNat':n__s'

Lemmas:
isNat'(_gen_tt':n__0':n__plus':n__isNat':n__s'2(_n176)) → tt', rt ∈ Ω(1 + n176)

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

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

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

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

Rules:
U11'(tt', N) → activate'(N)
U21'(tt', M, N) → s'(plus'(activate'(N), activate'(M)))
and'(tt', X) → activate'(X)
isNat'(n__0') → tt'
isNat'(n__plus'(V1, V2)) → and'(isNat'(activate'(V1)), n__isNat'(activate'(V2)))
isNat'(n__s'(V1)) → isNat'(activate'(V1))
plus'(N, 0') → U11'(isNat'(N), N)
plus'(N, s'(M)) → U21'(and'(isNat'(M), n__isNat'(N)), M, N)
0' → n__0'
plus'(X1, X2) → n__plus'(X1, X2)
isNat'(X) → n__isNat'(X)
s'(X) → n__s'(X)
activate'(n__0') → 0'
activate'(n__plus'(X1, X2)) → plus'(X1, X2)
activate'(n__isNat'(X)) → isNat'(X)
activate'(n__s'(X)) → s'(X)
activate'(X) → X

Types:
U11' :: tt':n__0':n__plus':n__isNat':n__s' → tt':n__0':n__plus':n__isNat':n__s' → tt':n__0':n__plus':n__isNat':n__s'
tt' :: tt':n__0':n__plus':n__isNat':n__s'
activate' :: tt':n__0':n__plus':n__isNat':n__s' → tt':n__0':n__plus':n__isNat':n__s'
U21' :: tt':n__0':n__plus':n__isNat':n__s' → tt':n__0':n__plus':n__isNat':n__s' → tt':n__0':n__plus':n__isNat':n__s' → tt':n__0':n__plus':n__isNat':n__s'
s' :: tt':n__0':n__plus':n__isNat':n__s' → tt':n__0':n__plus':n__isNat':n__s'
plus' :: tt':n__0':n__plus':n__isNat':n__s' → tt':n__0':n__plus':n__isNat':n__s' → tt':n__0':n__plus':n__isNat':n__s'
and' :: tt':n__0':n__plus':n__isNat':n__s' → tt':n__0':n__plus':n__isNat':n__s' → tt':n__0':n__plus':n__isNat':n__s'
isNat' :: tt':n__0':n__plus':n__isNat':n__s' → tt':n__0':n__plus':n__isNat':n__s'
n__0' :: tt':n__0':n__plus':n__isNat':n__s'
n__plus' :: tt':n__0':n__plus':n__isNat':n__s' → tt':n__0':n__plus':n__isNat':n__s' → tt':n__0':n__plus':n__isNat':n__s'
n__isNat' :: tt':n__0':n__plus':n__isNat':n__s' → tt':n__0':n__plus':n__isNat':n__s'
n__s' :: tt':n__0':n__plus':n__isNat':n__s' → tt':n__0':n__plus':n__isNat':n__s'
0' :: tt':n__0':n__plus':n__isNat':n__s'
_hole_tt':n__0':n__plus':n__isNat':n__s'1 :: tt':n__0':n__plus':n__isNat':n__s'
_gen_tt':n__0':n__plus':n__isNat':n__s'2 :: Nat → tt':n__0':n__plus':n__isNat':n__s'

Lemmas:
isNat'(_gen_tt':n__0':n__plus':n__isNat':n__s'2(_n176)) → tt', rt ∈ Ω(1 + n176)

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

The following defined symbols remain to be analysed:
U11'

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

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

Rules:
U11'(tt', N) → activate'(N)
U21'(tt', M, N) → s'(plus'(activate'(N), activate'(M)))
and'(tt', X) → activate'(X)
isNat'(n__0') → tt'
isNat'(n__plus'(V1, V2)) → and'(isNat'(activate'(V1)), n__isNat'(activate'(V2)))
isNat'(n__s'(V1)) → isNat'(activate'(V1))
plus'(N, 0') → U11'(isNat'(N), N)
plus'(N, s'(M)) → U21'(and'(isNat'(M), n__isNat'(N)), M, N)
0' → n__0'
plus'(X1, X2) → n__plus'(X1, X2)
isNat'(X) → n__isNat'(X)
s'(X) → n__s'(X)
activate'(n__0') → 0'
activate'(n__plus'(X1, X2)) → plus'(X1, X2)
activate'(n__isNat'(X)) → isNat'(X)
activate'(n__s'(X)) → s'(X)
activate'(X) → X

Types:
U11' :: tt':n__0':n__plus':n__isNat':n__s' → tt':n__0':n__plus':n__isNat':n__s' → tt':n__0':n__plus':n__isNat':n__s'
tt' :: tt':n__0':n__plus':n__isNat':n__s'
activate' :: tt':n__0':n__plus':n__isNat':n__s' → tt':n__0':n__plus':n__isNat':n__s'
U21' :: tt':n__0':n__plus':n__isNat':n__s' → tt':n__0':n__plus':n__isNat':n__s' → tt':n__0':n__plus':n__isNat':n__s' → tt':n__0':n__plus':n__isNat':n__s'
s' :: tt':n__0':n__plus':n__isNat':n__s' → tt':n__0':n__plus':n__isNat':n__s'
plus' :: tt':n__0':n__plus':n__isNat':n__s' → tt':n__0':n__plus':n__isNat':n__s' → tt':n__0':n__plus':n__isNat':n__s'
and' :: tt':n__0':n__plus':n__isNat':n__s' → tt':n__0':n__plus':n__isNat':n__s' → tt':n__0':n__plus':n__isNat':n__s'
isNat' :: tt':n__0':n__plus':n__isNat':n__s' → tt':n__0':n__plus':n__isNat':n__s'
n__0' :: tt':n__0':n__plus':n__isNat':n__s'
n__plus' :: tt':n__0':n__plus':n__isNat':n__s' → tt':n__0':n__plus':n__isNat':n__s' → tt':n__0':n__plus':n__isNat':n__s'
n__isNat' :: tt':n__0':n__plus':n__isNat':n__s' → tt':n__0':n__plus':n__isNat':n__s'
n__s' :: tt':n__0':n__plus':n__isNat':n__s' → tt':n__0':n__plus':n__isNat':n__s'
0' :: tt':n__0':n__plus':n__isNat':n__s'
_hole_tt':n__0':n__plus':n__isNat':n__s'1 :: tt':n__0':n__plus':n__isNat':n__s'
_gen_tt':n__0':n__plus':n__isNat':n__s'2 :: Nat → tt':n__0':n__plus':n__isNat':n__s'

Lemmas:
isNat'(_gen_tt':n__0':n__plus':n__isNat':n__s'2(_n176)) → tt', rt ∈ Ω(1 + n176)

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

No more defined symbols left to analyse.

The lowerbound Ω(n) was proven with the following lemma:
isNat'(_gen_tt':n__0':n__plus':n__isNat':n__s'2(_n176)) → tt', rt ∈ Ω(1 + n176)