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

minus(n__0, Y) → 0
minus(n__s(X), n__s(Y)) → minus(activate(X), activate(Y))
geq(X, n__0) → true
geq(n__0, n__s(Y)) → false
geq(n__s(X), n__s(Y)) → geq(activate(X), activate(Y))
div(0, n__s(Y)) → 0
div(s(X), n__s(Y)) → if(geq(X, activate(Y)), n__s(n__div(n__minus(X, activate(Y)), n__s(activate(Y)))), n__0)
if(true, X, Y) → activate(X)
if(false, X, Y) → activate(Y)
0 → n__0
s(X) → n__s(X)
div(X1, X2) → n__div(X1, X2)
minus(X1, X2) → n__minus(X1, X2)
activate(n__0) → 0
activate(n__s(X)) → s(activate(X))
activate(n__div(X1, X2)) → div(activate(X1), X2)
activate(n__minus(X1, X2)) → minus(X1, X2)
activate(X) → X

Rewrite Strategy: INNERMOST

Renamed function symbols to avoid clashes with predefined symbol.

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


minus'(n__0', Y) → 0'
minus'(n__s'(X), n__s'(Y)) → minus'(activate'(X), activate'(Y))
geq'(X, n__0') → true'
geq'(n__0', n__s'(Y)) → false'
geq'(n__s'(X), n__s'(Y)) → geq'(activate'(X), activate'(Y))
div'(0', n__s'(Y)) → 0'
div'(s'(X), n__s'(Y)) → if'(geq'(X, activate'(Y)), n__s'(n__div'(n__minus'(X, activate'(Y)), n__s'(activate'(Y)))), n__0')
if'(true', X, Y) → activate'(X)
if'(false', X, Y) → activate'(Y)
0' → n__0'
s'(X) → n__s'(X)
div'(X1, X2) → n__div'(X1, X2)
minus'(X1, X2) → n__minus'(X1, X2)
activate'(n__0') → 0'
activate'(n__s'(X)) → s'(activate'(X))
activate'(n__div'(X1, X2)) → div'(activate'(X1), X2)
activate'(n__minus'(X1, X2)) → minus'(X1, X2)
activate'(X) → X

Rewrite Strategy: INNERMOST

Infered types.

Rules:
minus'(n__0', Y) → 0'
minus'(n__s'(X), n__s'(Y)) → minus'(activate'(X), activate'(Y))
geq'(X, n__0') → true'
geq'(n__0', n__s'(Y)) → false'
geq'(n__s'(X), n__s'(Y)) → geq'(activate'(X), activate'(Y))
div'(0', n__s'(Y)) → 0'
div'(s'(X), n__s'(Y)) → if'(geq'(X, activate'(Y)), n__s'(n__div'(n__minus'(X, activate'(Y)), n__s'(activate'(Y)))), n__0')
if'(true', X, Y) → activate'(X)
if'(false', X, Y) → activate'(Y)
0' → n__0'
s'(X) → n__s'(X)
div'(X1, X2) → n__div'(X1, X2)
minus'(X1, X2) → n__minus'(X1, X2)
activate'(n__0') → 0'
activate'(n__s'(X)) → s'(activate'(X))
activate'(n__div'(X1, X2)) → div'(activate'(X1), X2)
activate'(n__minus'(X1, X2)) → minus'(X1, X2)
activate'(X) → X

Types:
minus' :: n__0':n__s':n__minus':n__div' → n__0':n__s':n__minus':n__div' → n__0':n__s':n__minus':n__div'
n__0' :: n__0':n__s':n__minus':n__div'
0' :: n__0':n__s':n__minus':n__div'
n__s' :: n__0':n__s':n__minus':n__div' → n__0':n__s':n__minus':n__div'
activate' :: n__0':n__s':n__minus':n__div' → n__0':n__s':n__minus':n__div'
geq' :: n__0':n__s':n__minus':n__div' → n__0':n__s':n__minus':n__div' → true':false'
true' :: true':false'
false' :: true':false'
div' :: n__0':n__s':n__minus':n__div' → n__0':n__s':n__minus':n__div' → n__0':n__s':n__minus':n__div'
s' :: n__0':n__s':n__minus':n__div' → n__0':n__s':n__minus':n__div'
if' :: true':false' → n__0':n__s':n__minus':n__div' → n__0':n__s':n__minus':n__div' → n__0':n__s':n__minus':n__div'
n__div' :: n__0':n__s':n__minus':n__div' → n__0':n__s':n__minus':n__div' → n__0':n__s':n__minus':n__div'
n__minus' :: n__0':n__s':n__minus':n__div' → n__0':n__s':n__minus':n__div' → n__0':n__s':n__minus':n__div'
_hole_n__0':n__s':n__minus':n__div'1 :: n__0':n__s':n__minus':n__div'
_hole_true':false'2 :: true':false'
_gen_n__0':n__s':n__minus':n__div'3 :: Nat → n__0':n__s':n__minus':n__div'

Heuristically decided to analyse the following defined symbols:
minus', activate', geq'

They will be analysed ascendingly in the following order:
minus' = activate'
minus' = geq'
activate' = geq'

Rules:
minus'(n__0', Y) → 0'
minus'(n__s'(X), n__s'(Y)) → minus'(activate'(X), activate'(Y))
geq'(X, n__0') → true'
geq'(n__0', n__s'(Y)) → false'
geq'(n__s'(X), n__s'(Y)) → geq'(activate'(X), activate'(Y))
div'(0', n__s'(Y)) → 0'
div'(s'(X), n__s'(Y)) → if'(geq'(X, activate'(Y)), n__s'(n__div'(n__minus'(X, activate'(Y)), n__s'(activate'(Y)))), n__0')
if'(true', X, Y) → activate'(X)
if'(false', X, Y) → activate'(Y)
0' → n__0'
s'(X) → n__s'(X)
div'(X1, X2) → n__div'(X1, X2)
minus'(X1, X2) → n__minus'(X1, X2)
activate'(n__0') → 0'
activate'(n__s'(X)) → s'(activate'(X))
activate'(n__div'(X1, X2)) → div'(activate'(X1), X2)
activate'(n__minus'(X1, X2)) → minus'(X1, X2)
activate'(X) → X

Types:
minus' :: n__0':n__s':n__minus':n__div' → n__0':n__s':n__minus':n__div' → n__0':n__s':n__minus':n__div'
n__0' :: n__0':n__s':n__minus':n__div'
0' :: n__0':n__s':n__minus':n__div'
n__s' :: n__0':n__s':n__minus':n__div' → n__0':n__s':n__minus':n__div'
activate' :: n__0':n__s':n__minus':n__div' → n__0':n__s':n__minus':n__div'
geq' :: n__0':n__s':n__minus':n__div' → n__0':n__s':n__minus':n__div' → true':false'
true' :: true':false'
false' :: true':false'
div' :: n__0':n__s':n__minus':n__div' → n__0':n__s':n__minus':n__div' → n__0':n__s':n__minus':n__div'
s' :: n__0':n__s':n__minus':n__div' → n__0':n__s':n__minus':n__div'
if' :: true':false' → n__0':n__s':n__minus':n__div' → n__0':n__s':n__minus':n__div' → n__0':n__s':n__minus':n__div'
n__div' :: n__0':n__s':n__minus':n__div' → n__0':n__s':n__minus':n__div' → n__0':n__s':n__minus':n__div'
n__minus' :: n__0':n__s':n__minus':n__div' → n__0':n__s':n__minus':n__div' → n__0':n__s':n__minus':n__div'
_hole_n__0':n__s':n__minus':n__div'1 :: n__0':n__s':n__minus':n__div'
_hole_true':false'2 :: true':false'
_gen_n__0':n__s':n__minus':n__div'3 :: Nat → n__0':n__s':n__minus':n__div'

Generator Equations:
_gen_n__0':n__s':n__minus':n__div'3(0) ⇔ n__0'
_gen_n__0':n__s':n__minus':n__div'3(+(x, 1)) ⇔ n__s'(_gen_n__0':n__s':n__minus':n__div'3(x))

The following defined symbols remain to be analysed:
activate', minus', geq'

They will be analysed ascendingly in the following order:
minus' = activate'
minus' = geq'
activate' = geq'

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

Induction Base:
activate'(_gen_n__0':n__s':n__minus':n__div'3(0)) →RΩ(1)
_gen_n__0':n__s':n__minus':n__div'3(0)

Induction Step:
activate'(_gen_n__0':n__s':n__minus':n__div'3(+(_$n6, 1))) →RΩ(1)
s'(activate'(_gen_n__0':n__s':n__minus':n__div'3(_$n6))) →IH
s'(_gen_n__0':n__s':n__minus':n__div'3(_$n6)) →RΩ(1)
n__s'(_gen_n__0':n__s':n__minus':n__div'3(_$n6))

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

Rules:
minus'(n__0', Y) → 0'
minus'(n__s'(X), n__s'(Y)) → minus'(activate'(X), activate'(Y))
geq'(X, n__0') → true'
geq'(n__0', n__s'(Y)) → false'
geq'(n__s'(X), n__s'(Y)) → geq'(activate'(X), activate'(Y))
div'(0', n__s'(Y)) → 0'
div'(s'(X), n__s'(Y)) → if'(geq'(X, activate'(Y)), n__s'(n__div'(n__minus'(X, activate'(Y)), n__s'(activate'(Y)))), n__0')
if'(true', X, Y) → activate'(X)
if'(false', X, Y) → activate'(Y)
0' → n__0'
s'(X) → n__s'(X)
div'(X1, X2) → n__div'(X1, X2)
minus'(X1, X2) → n__minus'(X1, X2)
activate'(n__0') → 0'
activate'(n__s'(X)) → s'(activate'(X))
activate'(n__div'(X1, X2)) → div'(activate'(X1), X2)
activate'(n__minus'(X1, X2)) → minus'(X1, X2)
activate'(X) → X

Types:
minus' :: n__0':n__s':n__minus':n__div' → n__0':n__s':n__minus':n__div' → n__0':n__s':n__minus':n__div'
n__0' :: n__0':n__s':n__minus':n__div'
0' :: n__0':n__s':n__minus':n__div'
n__s' :: n__0':n__s':n__minus':n__div' → n__0':n__s':n__minus':n__div'
activate' :: n__0':n__s':n__minus':n__div' → n__0':n__s':n__minus':n__div'
geq' :: n__0':n__s':n__minus':n__div' → n__0':n__s':n__minus':n__div' → true':false'
true' :: true':false'
false' :: true':false'
div' :: n__0':n__s':n__minus':n__div' → n__0':n__s':n__minus':n__div' → n__0':n__s':n__minus':n__div'
s' :: n__0':n__s':n__minus':n__div' → n__0':n__s':n__minus':n__div'
if' :: true':false' → n__0':n__s':n__minus':n__div' → n__0':n__s':n__minus':n__div' → n__0':n__s':n__minus':n__div'
n__div' :: n__0':n__s':n__minus':n__div' → n__0':n__s':n__minus':n__div' → n__0':n__s':n__minus':n__div'
n__minus' :: n__0':n__s':n__minus':n__div' → n__0':n__s':n__minus':n__div' → n__0':n__s':n__minus':n__div'
_hole_n__0':n__s':n__minus':n__div'1 :: n__0':n__s':n__minus':n__div'
_hole_true':false'2 :: true':false'
_gen_n__0':n__s':n__minus':n__div'3 :: Nat → n__0':n__s':n__minus':n__div'

Lemmas:
activate'(_gen_n__0':n__s':n__minus':n__div'3(_n5)) → _gen_n__0':n__s':n__minus':n__div'3(_n5), rt ∈ Ω(1 + n5)

Generator Equations:
_gen_n__0':n__s':n__minus':n__div'3(0) ⇔ n__0'
_gen_n__0':n__s':n__minus':n__div'3(+(x, 1)) ⇔ n__s'(_gen_n__0':n__s':n__minus':n__div'3(x))

The following defined symbols remain to be analysed:
minus', geq'

They will be analysed ascendingly in the following order:
minus' = activate'
minus' = geq'
activate' = geq'

Proved the following rewrite lemma:
minus'(_gen_n__0':n__s':n__minus':n__div'3(_n2121), _gen_n__0':n__s':n__minus':n__div'3(_n2121)) → _gen_n__0':n__s':n__minus':n__div'3(0), rt ∈ Ω(1 + n2121 + n21212)

Induction Base:
minus'(_gen_n__0':n__s':n__minus':n__div'3(0), _gen_n__0':n__s':n__minus':n__div'3(0)) →RΩ(1)
0' →RΩ(1)
n__0'

Induction Step:
minus'(_gen_n__0':n__s':n__minus':n__div'3(+(_$n2122, 1)), _gen_n__0':n__s':n__minus':n__div'3(+(_$n2122, 1))) →RΩ(1)
minus'(activate'(_gen_n__0':n__s':n__minus':n__div'3(_$n2122)), activate'(_gen_n__0':n__s':n__minus':n__div'3(_$n2122))) →LΩ(1 + $n2122)
minus'(_gen_n__0':n__s':n__minus':n__div'3(_$n2122), activate'(_gen_n__0':n__s':n__minus':n__div'3(_$n2122))) →LΩ(1 + $n2122)
minus'(_gen_n__0':n__s':n__minus':n__div'3(_$n2122), _gen_n__0':n__s':n__minus':n__div'3(_$n2122)) →IH
_gen_n__0':n__s':n__minus':n__div'3(0)

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

Rules:
minus'(n__0', Y) → 0'
minus'(n__s'(X), n__s'(Y)) → minus'(activate'(X), activate'(Y))
geq'(X, n__0') → true'
geq'(n__0', n__s'(Y)) → false'
geq'(n__s'(X), n__s'(Y)) → geq'(activate'(X), activate'(Y))
div'(0', n__s'(Y)) → 0'
div'(s'(X), n__s'(Y)) → if'(geq'(X, activate'(Y)), n__s'(n__div'(n__minus'(X, activate'(Y)), n__s'(activate'(Y)))), n__0')
if'(true', X, Y) → activate'(X)
if'(false', X, Y) → activate'(Y)
0' → n__0'
s'(X) → n__s'(X)
div'(X1, X2) → n__div'(X1, X2)
minus'(X1, X2) → n__minus'(X1, X2)
activate'(n__0') → 0'
activate'(n__s'(X)) → s'(activate'(X))
activate'(n__div'(X1, X2)) → div'(activate'(X1), X2)
activate'(n__minus'(X1, X2)) → minus'(X1, X2)
activate'(X) → X

Types:
minus' :: n__0':n__s':n__minus':n__div' → n__0':n__s':n__minus':n__div' → n__0':n__s':n__minus':n__div'
n__0' :: n__0':n__s':n__minus':n__div'
0' :: n__0':n__s':n__minus':n__div'
n__s' :: n__0':n__s':n__minus':n__div' → n__0':n__s':n__minus':n__div'
activate' :: n__0':n__s':n__minus':n__div' → n__0':n__s':n__minus':n__div'
geq' :: n__0':n__s':n__minus':n__div' → n__0':n__s':n__minus':n__div' → true':false'
true' :: true':false'
false' :: true':false'
div' :: n__0':n__s':n__minus':n__div' → n__0':n__s':n__minus':n__div' → n__0':n__s':n__minus':n__div'
s' :: n__0':n__s':n__minus':n__div' → n__0':n__s':n__minus':n__div'
if' :: true':false' → n__0':n__s':n__minus':n__div' → n__0':n__s':n__minus':n__div' → n__0':n__s':n__minus':n__div'
n__div' :: n__0':n__s':n__minus':n__div' → n__0':n__s':n__minus':n__div' → n__0':n__s':n__minus':n__div'
n__minus' :: n__0':n__s':n__minus':n__div' → n__0':n__s':n__minus':n__div' → n__0':n__s':n__minus':n__div'
_hole_n__0':n__s':n__minus':n__div'1 :: n__0':n__s':n__minus':n__div'
_hole_true':false'2 :: true':false'
_gen_n__0':n__s':n__minus':n__div'3 :: Nat → n__0':n__s':n__minus':n__div'

Lemmas:
activate'(_gen_n__0':n__s':n__minus':n__div'3(_n5)) → _gen_n__0':n__s':n__minus':n__div'3(_n5), rt ∈ Ω(1 + n5)
minus'(_gen_n__0':n__s':n__minus':n__div'3(_n2121), _gen_n__0':n__s':n__minus':n__div'3(_n2121)) → _gen_n__0':n__s':n__minus':n__div'3(0), rt ∈ Ω(1 + n2121 + n21212)

Generator Equations:
_gen_n__0':n__s':n__minus':n__div'3(0) ⇔ n__0'
_gen_n__0':n__s':n__minus':n__div'3(+(x, 1)) ⇔ n__s'(_gen_n__0':n__s':n__minus':n__div'3(x))

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

They will be analysed ascendingly in the following order:
minus' = activate'
minus' = geq'
activate' = geq'

Proved the following rewrite lemma:
geq'(_gen_n__0':n__s':n__minus':n__div'3(_n7215), _gen_n__0':n__s':n__minus':n__div'3(_n7215)) → true', rt ∈ Ω(1 + n7215 + n72152)

Induction Base:
geq'(_gen_n__0':n__s':n__minus':n__div'3(0), _gen_n__0':n__s':n__minus':n__div'3(0)) →RΩ(1)
true'

Induction Step:
geq'(_gen_n__0':n__s':n__minus':n__div'3(+(_$n7216, 1)), _gen_n__0':n__s':n__minus':n__div'3(+(_$n7216, 1))) →RΩ(1)
geq'(activate'(_gen_n__0':n__s':n__minus':n__div'3(_$n7216)), activate'(_gen_n__0':n__s':n__minus':n__div'3(_$n7216))) →LΩ(1 + $n7216)
geq'(_gen_n__0':n__s':n__minus':n__div'3(_$n7216), activate'(_gen_n__0':n__s':n__minus':n__div'3(_$n7216))) →LΩ(1 + $n7216)
geq'(_gen_n__0':n__s':n__minus':n__div'3(_$n7216), _gen_n__0':n__s':n__minus':n__div'3(_$n7216)) →IH
true'

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

Rules:
minus'(n__0', Y) → 0'
minus'(n__s'(X), n__s'(Y)) → minus'(activate'(X), activate'(Y))
geq'(X, n__0') → true'
geq'(n__0', n__s'(Y)) → false'
geq'(n__s'(X), n__s'(Y)) → geq'(activate'(X), activate'(Y))
div'(0', n__s'(Y)) → 0'
div'(s'(X), n__s'(Y)) → if'(geq'(X, activate'(Y)), n__s'(n__div'(n__minus'(X, activate'(Y)), n__s'(activate'(Y)))), n__0')
if'(true', X, Y) → activate'(X)
if'(false', X, Y) → activate'(Y)
0' → n__0'
s'(X) → n__s'(X)
div'(X1, X2) → n__div'(X1, X2)
minus'(X1, X2) → n__minus'(X1, X2)
activate'(n__0') → 0'
activate'(n__s'(X)) → s'(activate'(X))
activate'(n__div'(X1, X2)) → div'(activate'(X1), X2)
activate'(n__minus'(X1, X2)) → minus'(X1, X2)
activate'(X) → X

Types:
minus' :: n__0':n__s':n__minus':n__div' → n__0':n__s':n__minus':n__div' → n__0':n__s':n__minus':n__div'
n__0' :: n__0':n__s':n__minus':n__div'
0' :: n__0':n__s':n__minus':n__div'
n__s' :: n__0':n__s':n__minus':n__div' → n__0':n__s':n__minus':n__div'
activate' :: n__0':n__s':n__minus':n__div' → n__0':n__s':n__minus':n__div'
geq' :: n__0':n__s':n__minus':n__div' → n__0':n__s':n__minus':n__div' → true':false'
true' :: true':false'
false' :: true':false'
div' :: n__0':n__s':n__minus':n__div' → n__0':n__s':n__minus':n__div' → n__0':n__s':n__minus':n__div'
s' :: n__0':n__s':n__minus':n__div' → n__0':n__s':n__minus':n__div'
if' :: true':false' → n__0':n__s':n__minus':n__div' → n__0':n__s':n__minus':n__div' → n__0':n__s':n__minus':n__div'
n__div' :: n__0':n__s':n__minus':n__div' → n__0':n__s':n__minus':n__div' → n__0':n__s':n__minus':n__div'
n__minus' :: n__0':n__s':n__minus':n__div' → n__0':n__s':n__minus':n__div' → n__0':n__s':n__minus':n__div'
_hole_n__0':n__s':n__minus':n__div'1 :: n__0':n__s':n__minus':n__div'
_hole_true':false'2 :: true':false'
_gen_n__0':n__s':n__minus':n__div'3 :: Nat → n__0':n__s':n__minus':n__div'

Lemmas:
activate'(_gen_n__0':n__s':n__minus':n__div'3(_n5)) → _gen_n__0':n__s':n__minus':n__div'3(_n5), rt ∈ Ω(1 + n5)
minus'(_gen_n__0':n__s':n__minus':n__div'3(_n2121), _gen_n__0':n__s':n__minus':n__div'3(_n2121)) → _gen_n__0':n__s':n__minus':n__div'3(0), rt ∈ Ω(1 + n2121 + n21212)
geq'(_gen_n__0':n__s':n__minus':n__div'3(_n7215), _gen_n__0':n__s':n__minus':n__div'3(_n7215)) → true', rt ∈ Ω(1 + n7215 + n72152)

Generator Equations:
_gen_n__0':n__s':n__minus':n__div'3(0) ⇔ n__0'
_gen_n__0':n__s':n__minus':n__div'3(+(x, 1)) ⇔ n__s'(_gen_n__0':n__s':n__minus':n__div'3(x))

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

They will be analysed ascendingly in the following order:
minus' = activate'
minus' = geq'
activate' = geq'

Proved the following rewrite lemma:
activate'(_gen_n__0':n__s':n__minus':n__div'3(_n10092)) → _gen_n__0':n__s':n__minus':n__div'3(_n10092), rt ∈ Ω(1 + n10092)

Induction Base:
activate'(_gen_n__0':n__s':n__minus':n__div'3(0)) →RΩ(1)
_gen_n__0':n__s':n__minus':n__div'3(0)

Induction Step:
activate'(_gen_n__0':n__s':n__minus':n__div'3(+(_$n10093, 1))) →RΩ(1)
s'(activate'(_gen_n__0':n__s':n__minus':n__div'3(_$n10093))) →IH
s'(_gen_n__0':n__s':n__minus':n__div'3(_$n10093)) →RΩ(1)
n__s'(_gen_n__0':n__s':n__minus':n__div'3(_$n10093))

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

Rules:
minus'(n__0', Y) → 0'
minus'(n__s'(X), n__s'(Y)) → minus'(activate'(X), activate'(Y))
geq'(X, n__0') → true'
geq'(n__0', n__s'(Y)) → false'
geq'(n__s'(X), n__s'(Y)) → geq'(activate'(X), activate'(Y))
div'(0', n__s'(Y)) → 0'
div'(s'(X), n__s'(Y)) → if'(geq'(X, activate'(Y)), n__s'(n__div'(n__minus'(X, activate'(Y)), n__s'(activate'(Y)))), n__0')
if'(true', X, Y) → activate'(X)
if'(false', X, Y) → activate'(Y)
0' → n__0'
s'(X) → n__s'(X)
div'(X1, X2) → n__div'(X1, X2)
minus'(X1, X2) → n__minus'(X1, X2)
activate'(n__0') → 0'
activate'(n__s'(X)) → s'(activate'(X))
activate'(n__div'(X1, X2)) → div'(activate'(X1), X2)
activate'(n__minus'(X1, X2)) → minus'(X1, X2)
activate'(X) → X

Types:
minus' :: n__0':n__s':n__minus':n__div' → n__0':n__s':n__minus':n__div' → n__0':n__s':n__minus':n__div'
n__0' :: n__0':n__s':n__minus':n__div'
0' :: n__0':n__s':n__minus':n__div'
n__s' :: n__0':n__s':n__minus':n__div' → n__0':n__s':n__minus':n__div'
activate' :: n__0':n__s':n__minus':n__div' → n__0':n__s':n__minus':n__div'
geq' :: n__0':n__s':n__minus':n__div' → n__0':n__s':n__minus':n__div' → true':false'
true' :: true':false'
false' :: true':false'
div' :: n__0':n__s':n__minus':n__div' → n__0':n__s':n__minus':n__div' → n__0':n__s':n__minus':n__div'
s' :: n__0':n__s':n__minus':n__div' → n__0':n__s':n__minus':n__div'
if' :: true':false' → n__0':n__s':n__minus':n__div' → n__0':n__s':n__minus':n__div' → n__0':n__s':n__minus':n__div'
n__div' :: n__0':n__s':n__minus':n__div' → n__0':n__s':n__minus':n__div' → n__0':n__s':n__minus':n__div'
n__minus' :: n__0':n__s':n__minus':n__div' → n__0':n__s':n__minus':n__div' → n__0':n__s':n__minus':n__div'
_hole_n__0':n__s':n__minus':n__div'1 :: n__0':n__s':n__minus':n__div'
_hole_true':false'2 :: true':false'
_gen_n__0':n__s':n__minus':n__div'3 :: Nat → n__0':n__s':n__minus':n__div'

Lemmas:
activate'(_gen_n__0':n__s':n__minus':n__div'3(_n10092)) → _gen_n__0':n__s':n__minus':n__div'3(_n10092), rt ∈ Ω(1 + n10092)
minus'(_gen_n__0':n__s':n__minus':n__div'3(_n2121), _gen_n__0':n__s':n__minus':n__div'3(_n2121)) → _gen_n__0':n__s':n__minus':n__div'3(0), rt ∈ Ω(1 + n2121 + n21212)
geq'(_gen_n__0':n__s':n__minus':n__div'3(_n7215), _gen_n__0':n__s':n__minus':n__div'3(_n7215)) → true', rt ∈ Ω(1 + n7215 + n72152)

Generator Equations:
_gen_n__0':n__s':n__minus':n__div'3(0) ⇔ n__0'
_gen_n__0':n__s':n__minus':n__div'3(+(x, 1)) ⇔ n__s'(_gen_n__0':n__s':n__minus':n__div'3(x))

The following defined symbols remain to be analysed:
minus'

They will be analysed ascendingly in the following order:
minus' = activate'
minus' = geq'
activate' = geq'

Proved the following rewrite lemma:
minus'(_gen_n__0':n__s':n__minus':n__div'3(_n12324), _gen_n__0':n__s':n__minus':n__div'3(_n12324)) → _gen_n__0':n__s':n__minus':n__div'3(0), rt ∈ Ω(1 + n12324 + n123242)

Induction Base:
minus'(_gen_n__0':n__s':n__minus':n__div'3(0), _gen_n__0':n__s':n__minus':n__div'3(0)) →RΩ(1)
0' →RΩ(1)
n__0'

Induction Step:
minus'(_gen_n__0':n__s':n__minus':n__div'3(+(_$n12325, 1)), _gen_n__0':n__s':n__minus':n__div'3(+(_$n12325, 1))) →RΩ(1)
minus'(activate'(_gen_n__0':n__s':n__minus':n__div'3(_$n12325)), activate'(_gen_n__0':n__s':n__minus':n__div'3(_$n12325))) →LΩ(1 + $n12325)
minus'(_gen_n__0':n__s':n__minus':n__div'3(_$n12325), activate'(_gen_n__0':n__s':n__minus':n__div'3(_$n12325))) →LΩ(1 + $n12325)
minus'(_gen_n__0':n__s':n__minus':n__div'3(_$n12325), _gen_n__0':n__s':n__minus':n__div'3(_$n12325)) →IH
_gen_n__0':n__s':n__minus':n__div'3(0)

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

Rules:
minus'(n__0', Y) → 0'
minus'(n__s'(X), n__s'(Y)) → minus'(activate'(X), activate'(Y))
geq'(X, n__0') → true'
geq'(n__0', n__s'(Y)) → false'
geq'(n__s'(X), n__s'(Y)) → geq'(activate'(X), activate'(Y))
div'(0', n__s'(Y)) → 0'
div'(s'(X), n__s'(Y)) → if'(geq'(X, activate'(Y)), n__s'(n__div'(n__minus'(X, activate'(Y)), n__s'(activate'(Y)))), n__0')
if'(true', X, Y) → activate'(X)
if'(false', X, Y) → activate'(Y)
0' → n__0'
s'(X) → n__s'(X)
div'(X1, X2) → n__div'(X1, X2)
minus'(X1, X2) → n__minus'(X1, X2)
activate'(n__0') → 0'
activate'(n__s'(X)) → s'(activate'(X))
activate'(n__div'(X1, X2)) → div'(activate'(X1), X2)
activate'(n__minus'(X1, X2)) → minus'(X1, X2)
activate'(X) → X

Types:
minus' :: n__0':n__s':n__minus':n__div' → n__0':n__s':n__minus':n__div' → n__0':n__s':n__minus':n__div'
n__0' :: n__0':n__s':n__minus':n__div'
0' :: n__0':n__s':n__minus':n__div'
n__s' :: n__0':n__s':n__minus':n__div' → n__0':n__s':n__minus':n__div'
activate' :: n__0':n__s':n__minus':n__div' → n__0':n__s':n__minus':n__div'
geq' :: n__0':n__s':n__minus':n__div' → n__0':n__s':n__minus':n__div' → true':false'
true' :: true':false'
false' :: true':false'
div' :: n__0':n__s':n__minus':n__div' → n__0':n__s':n__minus':n__div' → n__0':n__s':n__minus':n__div'
s' :: n__0':n__s':n__minus':n__div' → n__0':n__s':n__minus':n__div'
if' :: true':false' → n__0':n__s':n__minus':n__div' → n__0':n__s':n__minus':n__div' → n__0':n__s':n__minus':n__div'
n__div' :: n__0':n__s':n__minus':n__div' → n__0':n__s':n__minus':n__div' → n__0':n__s':n__minus':n__div'
n__minus' :: n__0':n__s':n__minus':n__div' → n__0':n__s':n__minus':n__div' → n__0':n__s':n__minus':n__div'
_hole_n__0':n__s':n__minus':n__div'1 :: n__0':n__s':n__minus':n__div'
_hole_true':false'2 :: true':false'
_gen_n__0':n__s':n__minus':n__div'3 :: Nat → n__0':n__s':n__minus':n__div'

Lemmas:
activate'(_gen_n__0':n__s':n__minus':n__div'3(_n10092)) → _gen_n__0':n__s':n__minus':n__div'3(_n10092), rt ∈ Ω(1 + n10092)
minus'(_gen_n__0':n__s':n__minus':n__div'3(_n12324), _gen_n__0':n__s':n__minus':n__div'3(_n12324)) → _gen_n__0':n__s':n__minus':n__div'3(0), rt ∈ Ω(1 + n12324 + n123242)
geq'(_gen_n__0':n__s':n__minus':n__div'3(_n7215), _gen_n__0':n__s':n__minus':n__div'3(_n7215)) → true', rt ∈ Ω(1 + n7215 + n72152)

Generator Equations:
_gen_n__0':n__s':n__minus':n__div'3(0) ⇔ n__0'
_gen_n__0':n__s':n__minus':n__div'3(+(x, 1)) ⇔ n__s'(_gen_n__0':n__s':n__minus':n__div'3(x))

No more defined symbols left to analyse.

The lowerbound Ω(n2) was proven with the following lemma:
minus'(_gen_n__0':n__s':n__minus':n__div'3(_n12324), _gen_n__0':n__s':n__minus':n__div'3(_n12324)) → _gen_n__0':n__s':n__minus':n__div'3(0), rt ∈ Ω(1 + n12324 + n123242)