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


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

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

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

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

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

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

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

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

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

Proved the following rewrite lemma:
activate'(_gen_tt':n__0':n__plus':n__isNat':n__s':n__x'2(+(1, _n4))) → _*3, rt ∈ Ω(n4)

Induction Base:
activate'(_gen_tt':n__0':n__plus':n__isNat':n__s':n__x'2(+(1, 0)))

Induction Step:
activate'(_gen_tt':n__0':n__plus':n__isNat':n__s':n__x'2(+(1, +(_$n5, 1)))) →RΩ(1)
plus'(activate'(_gen_tt':n__0':n__plus':n__isNat':n__s':n__x'2(+(1, _$n5))), activate'(tt')) →IH
plus'(_*3, activate'(tt')) →RΩ(1)
plus'(_*3, 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)))
U31'(tt') → 0'
U41'(tt', M, N) → plus'(x'(activate'(N), activate'(M)), activate'(N))
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))
isNat'(n__x'(V1, V2)) → and'(isNat'(activate'(V1)), n__isNat'(activate'(V2)))
plus'(N, 0') → U11'(isNat'(N), N)
plus'(N, s'(M)) → U21'(and'(isNat'(M), n__isNat'(N)), M, N)
x'(N, 0') → U31'(isNat'(N))
x'(N, s'(M)) → U41'(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)
x'(X1, X2) → n__x'(X1, X2)
activate'(n__0') → 0'
activate'(n__plus'(X1, X2)) → plus'(activate'(X1), activate'(X2))
activate'(n__isNat'(X)) → isNat'(X)
activate'(n__s'(X)) → s'(activate'(X))
activate'(n__x'(X1, X2)) → x'(activate'(X1), activate'(X2))
activate'(X) → X

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

Lemmas:
activate'(_gen_tt':n__0':n__plus':n__isNat':n__s':n__x'2(+(1, _n4))) → _*3, rt ∈ Ω(n4)

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

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

They will be analysed ascendingly in the following order:
U11' = activate'
U11' = plus'
U11' = x'
U11' = and'
U11' = isNat'
activate' = plus'
activate' = x'
activate' = and'
activate' = isNat'
plus' = x'
plus' = and'
plus' = isNat'
x' = and'
x' = 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)))
U31'(tt') → 0'
U41'(tt', M, N) → plus'(x'(activate'(N), activate'(M)), activate'(N))
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))
isNat'(n__x'(V1, V2)) → and'(isNat'(activate'(V1)), n__isNat'(activate'(V2)))
plus'(N, 0') → U11'(isNat'(N), N)
plus'(N, s'(M)) → U21'(and'(isNat'(M), n__isNat'(N)), M, N)
x'(N, 0') → U31'(isNat'(N))
x'(N, s'(M)) → U41'(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)
x'(X1, X2) → n__x'(X1, X2)
activate'(n__0') → 0'
activate'(n__plus'(X1, X2)) → plus'(activate'(X1), activate'(X2))
activate'(n__isNat'(X)) → isNat'(X)
activate'(n__s'(X)) → s'(activate'(X))
activate'(n__x'(X1, X2)) → x'(activate'(X1), activate'(X2))
activate'(X) → X

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

Lemmas:
activate'(_gen_tt':n__0':n__plus':n__isNat':n__s':n__x'2(+(1, _n4))) → _*3, rt ∈ Ω(n4)

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

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

They will be analysed ascendingly in the following order:
U11' = activate'
U11' = plus'
U11' = x'
U11' = and'
U11' = isNat'
activate' = plus'
activate' = x'
activate' = and'
activate' = isNat'
plus' = x'
plus' = and'
plus' = isNat'
x' = and'
x' = 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)))
U31'(tt') → 0'
U41'(tt', M, N) → plus'(x'(activate'(N), activate'(M)), activate'(N))
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))
isNat'(n__x'(V1, V2)) → and'(isNat'(activate'(V1)), n__isNat'(activate'(V2)))
plus'(N, 0') → U11'(isNat'(N), N)
plus'(N, s'(M)) → U21'(and'(isNat'(M), n__isNat'(N)), M, N)
x'(N, 0') → U31'(isNat'(N))
x'(N, s'(M)) → U41'(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)
x'(X1, X2) → n__x'(X1, X2)
activate'(n__0') → 0'
activate'(n__plus'(X1, X2)) → plus'(activate'(X1), activate'(X2))
activate'(n__isNat'(X)) → isNat'(X)
activate'(n__s'(X)) → s'(activate'(X))
activate'(n__x'(X1, X2)) → x'(activate'(X1), activate'(X2))
activate'(X) → X

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

Lemmas:
activate'(_gen_tt':n__0':n__plus':n__isNat':n__s':n__x'2(+(1, _n4))) → _*3, rt ∈ Ω(n4)

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

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

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

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

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

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

Lemmas:
activate'(_gen_tt':n__0':n__plus':n__isNat':n__s':n__x'2(+(1, _n4))) → _*3, rt ∈ Ω(n4)

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

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

They will be analysed ascendingly in the following order:
U11' = activate'
U11' = plus'
U11' = x'
U11' = and'
U11' = isNat'
activate' = plus'
activate' = x'
activate' = and'
activate' = isNat'
plus' = x'
plus' = and'
plus' = isNat'
x' = and'
x' = 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)))
U31'(tt') → 0'
U41'(tt', M, N) → plus'(x'(activate'(N), activate'(M)), activate'(N))
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))
isNat'(n__x'(V1, V2)) → and'(isNat'(activate'(V1)), n__isNat'(activate'(V2)))
plus'(N, 0') → U11'(isNat'(N), N)
plus'(N, s'(M)) → U21'(and'(isNat'(M), n__isNat'(N)), M, N)
x'(N, 0') → U31'(isNat'(N))
x'(N, s'(M)) → U41'(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)
x'(X1, X2) → n__x'(X1, X2)
activate'(n__0') → 0'
activate'(n__plus'(X1, X2)) → plus'(activate'(X1), activate'(X2))
activate'(n__isNat'(X)) → isNat'(X)
activate'(n__s'(X)) → s'(activate'(X))
activate'(n__x'(X1, X2)) → x'(activate'(X1), activate'(X2))
activate'(X) → X

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

Lemmas:
activate'(_gen_tt':n__0':n__plus':n__isNat':n__s':n__x'2(+(1, _n4))) → _*3, rt ∈ Ω(n4)

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

The following defined symbols remain to be analysed:
x'

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

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

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

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

Lemmas:
activate'(_gen_tt':n__0':n__plus':n__isNat':n__s':n__x'2(+(1, _n4))) → _*3, rt ∈ Ω(n4)

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

No more defined symbols left to analyse.

The lowerbound Ω(n) was proven with the following lemma:
activate'(_gen_tt':n__0':n__plus':n__isNat':n__s':n__x'2(+(1, _n4))) → _*3, rt ∈ Ω(n4)