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(div(minus(X, activate(Y)), n__s(activate(Y)))), n__0)
if(true, X, Y) → activate(X)
if(false, X, Y) → activate(Y)
0n__0
s(X) → n__s(X)
activate(n__0) → 0
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:

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'(div'(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)
activate'(n__0') → 0'
activate'(n__s'(X)) → s'(X)
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'(div'(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)
activate'(n__0') → 0'
activate'(n__s'(X)) → s'(X)
activate'(X) → X

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

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

They will be analysed ascendingly in the following order:
minus' < div'
geq' < div'

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'(div'(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)
activate'(n__0') → 0'
activate'(n__s'(X)) → s'(X)
activate'(X) → X

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

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

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

They will be analysed ascendingly in the following order:
minus' < div'
geq' < div'

Proved the following rewrite lemma:
minus'(_gen_n__0':n__s'3(+(2, _n5)), _gen_n__0':n__s'3(+(1, _n5))) → minus'(_gen_n__0':n__s'3(1), _gen_n__0':n__s'3(0)), rt ∈ Ω(1 + n5)

Induction Base:
minus'(_gen_n__0':n__s'3(+(2, 0)), _gen_n__0':n__s'3(+(1, 0))) →RΩ(1)
minus'(activate'(_gen_n__0':n__s'3(1)), activate'(_gen_n__0':n__s'3(0))) →RΩ(1)
minus'(_gen_n__0':n__s'3(1), activate'(_gen_n__0':n__s'3(0))) →RΩ(1)
minus'(_gen_n__0':n__s'3(1), _gen_n__0':n__s'3(0))

Induction Step:
minus'(_gen_n__0':n__s'3(+(2, +(_\$n6, 1))), _gen_n__0':n__s'3(+(1, +(_\$n6, 1)))) →RΩ(1)
minus'(activate'(_gen_n__0':n__s'3(+(2, _\$n6))), activate'(_gen_n__0':n__s'3(+(1, _\$n6)))) →RΩ(1)
minus'(_gen_n__0':n__s'3(+(2, _\$n6)), activate'(_gen_n__0':n__s'3(+(1, _\$n6)))) →RΩ(1)
minus'(_gen_n__0':n__s'3(+(2, _\$n6)), _gen_n__0':n__s'3(+(1, _\$n6))) →IH
minus'(_gen_n__0':n__s'3(1), _gen_n__0':n__s'3(0))

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'(div'(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)
activate'(n__0') → 0'
activate'(n__s'(X)) → s'(X)
activate'(X) → X

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

Lemmas:
minus'(_gen_n__0':n__s'3(+(2, _n5)), _gen_n__0':n__s'3(+(1, _n5))) → minus'(_gen_n__0':n__s'3(1), _gen_n__0':n__s'3(0)), rt ∈ Ω(1 + n5)

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

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

They will be analysed ascendingly in the following order:
geq' < div'

Proved the following rewrite lemma:
geq'(_gen_n__0':n__s'3(_n12098), _gen_n__0':n__s'3(+(1, _n12098))) → false', rt ∈ Ω(1 + n12098)

Induction Base:
geq'(_gen_n__0':n__s'3(0), _gen_n__0':n__s'3(+(1, 0))) →RΩ(1)
false'

Induction Step:
geq'(_gen_n__0':n__s'3(+(_\$n12099, 1)), _gen_n__0':n__s'3(+(1, +(_\$n12099, 1)))) →RΩ(1)
geq'(activate'(_gen_n__0':n__s'3(_\$n12099)), activate'(_gen_n__0':n__s'3(+(1, _\$n12099)))) →RΩ(1)
geq'(_gen_n__0':n__s'3(_\$n12099), activate'(_gen_n__0':n__s'3(+(1, _\$n12099)))) →RΩ(1)
geq'(_gen_n__0':n__s'3(_\$n12099), _gen_n__0':n__s'3(+(1, _\$n12099))) →IH
false'

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'(div'(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)
activate'(n__0') → 0'
activate'(n__s'(X)) → s'(X)
activate'(X) → X

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

Lemmas:
minus'(_gen_n__0':n__s'3(+(2, _n5)), _gen_n__0':n__s'3(+(1, _n5))) → minus'(_gen_n__0':n__s'3(1), _gen_n__0':n__s'3(0)), rt ∈ Ω(1 + n5)
geq'(_gen_n__0':n__s'3(_n12098), _gen_n__0':n__s'3(+(1, _n12098))) → false', rt ∈ Ω(1 + n12098)

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

The following defined symbols remain to be analysed:
div'

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

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'(div'(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)
activate'(n__0') → 0'
activate'(n__s'(X)) → s'(X)
activate'(X) → X

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

Lemmas:
minus'(_gen_n__0':n__s'3(+(2, _n5)), _gen_n__0':n__s'3(+(1, _n5))) → minus'(_gen_n__0':n__s'3(1), _gen_n__0':n__s'3(0)), rt ∈ Ω(1 + n5)
geq'(_gen_n__0':n__s'3(_n12098), _gen_n__0':n__s'3(+(1, _n12098))) → false', rt ∈ Ω(1 + n12098)

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

No more defined symbols left to analyse.

The lowerbound Ω(n) was proven with the following lemma:
minus'(_gen_n__0':n__s'3(+(2, _n5)), _gen_n__0':n__s'3(+(1, _n5))) → minus'(_gen_n__0':n__s'3(1), _gen_n__0':n__s'3(0)), rt ∈ Ω(1 + n5)