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

minus_active(0, y) → 0
mark(0) → 0
minus_active(s(x), s(y)) → minus_active(x, y)
mark(s(x)) → s(mark(x))
ge_active(x, 0) → true
mark(minus(x, y)) → minus_active(x, y)
ge_active(0, s(y)) → false
mark(ge(x, y)) → ge_active(x, y)
ge_active(s(x), s(y)) → ge_active(x, y)
mark(div(x, y)) → div_active(mark(x), y)
div_active(0, s(y)) → 0
mark(if(x, y, z)) → if_active(mark(x), y, z)
div_active(s(x), s(y)) → if_active(ge_active(x, y), s(div(minus(x, y), s(y))), 0)
if_active(true, x, y) → mark(x)
minus_active(x, y) → minus(x, y)
if_active(false, x, y) → mark(y)
ge_active(x, y) → ge(x, y)
if_active(x, y, z) → if(x, y, z)
div_active(x, y) → div(x, y)

Rewrite Strategy: INNERMOST

Renamed function symbols to avoid clashes with predefined symbol.

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

minus_active'(0', y) → 0'
mark'(0') → 0'
minus_active'(s'(x), s'(y)) → minus_active'(x, y)
mark'(s'(x)) → s'(mark'(x))
ge_active'(x, 0') → true'
mark'(minus'(x, y)) → minus_active'(x, y)
ge_active'(0', s'(y)) → false'
mark'(ge'(x, y)) → ge_active'(x, y)
ge_active'(s'(x), s'(y)) → ge_active'(x, y)
mark'(div'(x, y)) → div_active'(mark'(x), y)
div_active'(0', s'(y)) → 0'
mark'(if'(x, y, z)) → if_active'(mark'(x), y, z)
div_active'(s'(x), s'(y)) → if_active'(ge_active'(x, y), s'(div'(minus'(x, y), s'(y))), 0')
if_active'(true', x, y) → mark'(x)
minus_active'(x, y) → minus'(x, y)
if_active'(false', x, y) → mark'(y)
ge_active'(x, y) → ge'(x, y)
if_active'(x, y, z) → if'(x, y, z)
div_active'(x, y) → div'(x, y)

Rewrite Strategy: INNERMOST

Infered types.

Rules:
minus_active'(0', y) → 0'
mark'(0') → 0'
minus_active'(s'(x), s'(y)) → minus_active'(x, y)
mark'(s'(x)) → s'(mark'(x))
ge_active'(x, 0') → true'
mark'(minus'(x, y)) → minus_active'(x, y)
ge_active'(0', s'(y)) → false'
mark'(ge'(x, y)) → ge_active'(x, y)
ge_active'(s'(x), s'(y)) → ge_active'(x, y)
mark'(div'(x, y)) → div_active'(mark'(x), y)
div_active'(0', s'(y)) → 0'
mark'(if'(x, y, z)) → if_active'(mark'(x), y, z)
div_active'(s'(x), s'(y)) → if_active'(ge_active'(x, y), s'(div'(minus'(x, y), s'(y))), 0')
if_active'(true', x, y) → mark'(x)
minus_active'(x, y) → minus'(x, y)
if_active'(false', x, y) → mark'(y)
ge_active'(x, y) → ge'(x, y)
if_active'(x, y, z) → if'(x, y, z)
div_active'(x, y) → div'(x, y)

Types:
minus_active' :: 0':s':true':minus':false':ge':div':if' → 0':s':true':minus':false':ge':div':if' → 0':s':true':minus':false':ge':div':if'
0' :: 0':s':true':minus':false':ge':div':if'
mark' :: 0':s':true':minus':false':ge':div':if' → 0':s':true':minus':false':ge':div':if'
s' :: 0':s':true':minus':false':ge':div':if' → 0':s':true':minus':false':ge':div':if'
ge_active' :: 0':s':true':minus':false':ge':div':if' → 0':s':true':minus':false':ge':div':if' → 0':s':true':minus':false':ge':div':if'
true' :: 0':s':true':minus':false':ge':div':if'
minus' :: 0':s':true':minus':false':ge':div':if' → 0':s':true':minus':false':ge':div':if' → 0':s':true':minus':false':ge':div':if'
false' :: 0':s':true':minus':false':ge':div':if'
ge' :: 0':s':true':minus':false':ge':div':if' → 0':s':true':minus':false':ge':div':if' → 0':s':true':minus':false':ge':div':if'
div' :: 0':s':true':minus':false':ge':div':if' → 0':s':true':minus':false':ge':div':if' → 0':s':true':minus':false':ge':div':if'
div_active' :: 0':s':true':minus':false':ge':div':if' → 0':s':true':minus':false':ge':div':if' → 0':s':true':minus':false':ge':div':if'
if' :: 0':s':true':minus':false':ge':div':if' → 0':s':true':minus':false':ge':div':if' → 0':s':true':minus':false':ge':div':if' → 0':s':true':minus':false':ge':div':if'
if_active' :: 0':s':true':minus':false':ge':div':if' → 0':s':true':minus':false':ge':div':if' → 0':s':true':minus':false':ge':div':if' → 0':s':true':minus':false':ge':div':if'
_hole_0':s':true':minus':false':ge':div':if'1 :: 0':s':true':minus':false':ge':div':if'
_gen_0':s':true':minus':false':ge':div':if'2 :: Nat → 0':s':true':minus':false':ge':div':if'

Heuristically decided to analyse the following defined symbols:
minus_active', mark', ge_active'

They will be analysed ascendingly in the following order:
minus_active' < mark'
ge_active' < mark'

Rules:
minus_active'(0', y) → 0'
mark'(0') → 0'
minus_active'(s'(x), s'(y)) → minus_active'(x, y)
mark'(s'(x)) → s'(mark'(x))
ge_active'(x, 0') → true'
mark'(minus'(x, y)) → minus_active'(x, y)
ge_active'(0', s'(y)) → false'
mark'(ge'(x, y)) → ge_active'(x, y)
ge_active'(s'(x), s'(y)) → ge_active'(x, y)
mark'(div'(x, y)) → div_active'(mark'(x), y)
div_active'(0', s'(y)) → 0'
mark'(if'(x, y, z)) → if_active'(mark'(x), y, z)
div_active'(s'(x), s'(y)) → if_active'(ge_active'(x, y), s'(div'(minus'(x, y), s'(y))), 0')
if_active'(true', x, y) → mark'(x)
minus_active'(x, y) → minus'(x, y)
if_active'(false', x, y) → mark'(y)
ge_active'(x, y) → ge'(x, y)
if_active'(x, y, z) → if'(x, y, z)
div_active'(x, y) → div'(x, y)

Types:
minus_active' :: 0':s':true':minus':false':ge':div':if' → 0':s':true':minus':false':ge':div':if' → 0':s':true':minus':false':ge':div':if'
0' :: 0':s':true':minus':false':ge':div':if'
mark' :: 0':s':true':minus':false':ge':div':if' → 0':s':true':minus':false':ge':div':if'
s' :: 0':s':true':minus':false':ge':div':if' → 0':s':true':minus':false':ge':div':if'
ge_active' :: 0':s':true':minus':false':ge':div':if' → 0':s':true':minus':false':ge':div':if' → 0':s':true':minus':false':ge':div':if'
true' :: 0':s':true':minus':false':ge':div':if'
minus' :: 0':s':true':minus':false':ge':div':if' → 0':s':true':minus':false':ge':div':if' → 0':s':true':minus':false':ge':div':if'
false' :: 0':s':true':minus':false':ge':div':if'
ge' :: 0':s':true':minus':false':ge':div':if' → 0':s':true':minus':false':ge':div':if' → 0':s':true':minus':false':ge':div':if'
div' :: 0':s':true':minus':false':ge':div':if' → 0':s':true':minus':false':ge':div':if' → 0':s':true':minus':false':ge':div':if'
div_active' :: 0':s':true':minus':false':ge':div':if' → 0':s':true':minus':false':ge':div':if' → 0':s':true':minus':false':ge':div':if'
if' :: 0':s':true':minus':false':ge':div':if' → 0':s':true':minus':false':ge':div':if' → 0':s':true':minus':false':ge':div':if' → 0':s':true':minus':false':ge':div':if'
if_active' :: 0':s':true':minus':false':ge':div':if' → 0':s':true':minus':false':ge':div':if' → 0':s':true':minus':false':ge':div':if' → 0':s':true':minus':false':ge':div':if'
_hole_0':s':true':minus':false':ge':div':if'1 :: 0':s':true':minus':false':ge':div':if'
_gen_0':s':true':minus':false':ge':div':if'2 :: Nat → 0':s':true':minus':false':ge':div':if'

Generator Equations:
_gen_0':s':true':minus':false':ge':div':if'2(0) ⇔ 0'
_gen_0':s':true':minus':false':ge':div':if'2(+(x, 1)) ⇔ s'(_gen_0':s':true':minus':false':ge':div':if'2(x))

The following defined symbols remain to be analysed:
minus_active', mark', ge_active'

They will be analysed ascendingly in the following order:
minus_active' < mark'
ge_active' < mark'

Proved the following rewrite lemma:
minus_active'(_gen_0':s':true':minus':false':ge':div':if'2(_n4), _gen_0':s':true':minus':false':ge':div':if'2(_n4)) → _gen_0':s':true':minus':false':ge':div':if'2(0), rt ∈ Ω(1 + n4)

Induction Base:
minus_active'(_gen_0':s':true':minus':false':ge':div':if'2(0), _gen_0':s':true':minus':false':ge':div':if'2(0)) →RΩ(1)
0'

Induction Step:
minus_active'(_gen_0':s':true':minus':false':ge':div':if'2(+(_\$n5, 1)), _gen_0':s':true':minus':false':ge':div':if'2(+(_\$n5, 1))) →RΩ(1)
minus_active'(_gen_0':s':true':minus':false':ge':div':if'2(_\$n5), _gen_0':s':true':minus':false':ge':div':if'2(_\$n5)) →IH
_gen_0':s':true':minus':false':ge':div':if'2(0)

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

Rules:
minus_active'(0', y) → 0'
mark'(0') → 0'
minus_active'(s'(x), s'(y)) → minus_active'(x, y)
mark'(s'(x)) → s'(mark'(x))
ge_active'(x, 0') → true'
mark'(minus'(x, y)) → minus_active'(x, y)
ge_active'(0', s'(y)) → false'
mark'(ge'(x, y)) → ge_active'(x, y)
ge_active'(s'(x), s'(y)) → ge_active'(x, y)
mark'(div'(x, y)) → div_active'(mark'(x), y)
div_active'(0', s'(y)) → 0'
mark'(if'(x, y, z)) → if_active'(mark'(x), y, z)
div_active'(s'(x), s'(y)) → if_active'(ge_active'(x, y), s'(div'(minus'(x, y), s'(y))), 0')
if_active'(true', x, y) → mark'(x)
minus_active'(x, y) → minus'(x, y)
if_active'(false', x, y) → mark'(y)
ge_active'(x, y) → ge'(x, y)
if_active'(x, y, z) → if'(x, y, z)
div_active'(x, y) → div'(x, y)

Types:
minus_active' :: 0':s':true':minus':false':ge':div':if' → 0':s':true':minus':false':ge':div':if' → 0':s':true':minus':false':ge':div':if'
0' :: 0':s':true':minus':false':ge':div':if'
mark' :: 0':s':true':minus':false':ge':div':if' → 0':s':true':minus':false':ge':div':if'
s' :: 0':s':true':minus':false':ge':div':if' → 0':s':true':minus':false':ge':div':if'
ge_active' :: 0':s':true':minus':false':ge':div':if' → 0':s':true':minus':false':ge':div':if' → 0':s':true':minus':false':ge':div':if'
true' :: 0':s':true':minus':false':ge':div':if'
minus' :: 0':s':true':minus':false':ge':div':if' → 0':s':true':minus':false':ge':div':if' → 0':s':true':minus':false':ge':div':if'
false' :: 0':s':true':minus':false':ge':div':if'
ge' :: 0':s':true':minus':false':ge':div':if' → 0':s':true':minus':false':ge':div':if' → 0':s':true':minus':false':ge':div':if'
div' :: 0':s':true':minus':false':ge':div':if' → 0':s':true':minus':false':ge':div':if' → 0':s':true':minus':false':ge':div':if'
div_active' :: 0':s':true':minus':false':ge':div':if' → 0':s':true':minus':false':ge':div':if' → 0':s':true':minus':false':ge':div':if'
if' :: 0':s':true':minus':false':ge':div':if' → 0':s':true':minus':false':ge':div':if' → 0':s':true':minus':false':ge':div':if' → 0':s':true':minus':false':ge':div':if'
if_active' :: 0':s':true':minus':false':ge':div':if' → 0':s':true':minus':false':ge':div':if' → 0':s':true':minus':false':ge':div':if' → 0':s':true':minus':false':ge':div':if'
_hole_0':s':true':minus':false':ge':div':if'1 :: 0':s':true':minus':false':ge':div':if'
_gen_0':s':true':minus':false':ge':div':if'2 :: Nat → 0':s':true':minus':false':ge':div':if'

Lemmas:
minus_active'(_gen_0':s':true':minus':false':ge':div':if'2(_n4), _gen_0':s':true':minus':false':ge':div':if'2(_n4)) → _gen_0':s':true':minus':false':ge':div':if'2(0), rt ∈ Ω(1 + n4)

Generator Equations:
_gen_0':s':true':minus':false':ge':div':if'2(0) ⇔ 0'
_gen_0':s':true':minus':false':ge':div':if'2(+(x, 1)) ⇔ s'(_gen_0':s':true':minus':false':ge':div':if'2(x))

The following defined symbols remain to be analysed:
ge_active', mark'

They will be analysed ascendingly in the following order:
ge_active' < mark'

Proved the following rewrite lemma:
ge_active'(_gen_0':s':true':minus':false':ge':div':if'2(_n1984), _gen_0':s':true':minus':false':ge':div':if'2(_n1984)) → true', rt ∈ Ω(1 + n1984)

Induction Base:
ge_active'(_gen_0':s':true':minus':false':ge':div':if'2(0), _gen_0':s':true':minus':false':ge':div':if'2(0)) →RΩ(1)
true'

Induction Step:
ge_active'(_gen_0':s':true':minus':false':ge':div':if'2(+(_\$n1985, 1)), _gen_0':s':true':minus':false':ge':div':if'2(+(_\$n1985, 1))) →RΩ(1)
ge_active'(_gen_0':s':true':minus':false':ge':div':if'2(_\$n1985), _gen_0':s':true':minus':false':ge':div':if'2(_\$n1985)) →IH
true'

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

Rules:
minus_active'(0', y) → 0'
mark'(0') → 0'
minus_active'(s'(x), s'(y)) → minus_active'(x, y)
mark'(s'(x)) → s'(mark'(x))
ge_active'(x, 0') → true'
mark'(minus'(x, y)) → minus_active'(x, y)
ge_active'(0', s'(y)) → false'
mark'(ge'(x, y)) → ge_active'(x, y)
ge_active'(s'(x), s'(y)) → ge_active'(x, y)
mark'(div'(x, y)) → div_active'(mark'(x), y)
div_active'(0', s'(y)) → 0'
mark'(if'(x, y, z)) → if_active'(mark'(x), y, z)
div_active'(s'(x), s'(y)) → if_active'(ge_active'(x, y), s'(div'(minus'(x, y), s'(y))), 0')
if_active'(true', x, y) → mark'(x)
minus_active'(x, y) → minus'(x, y)
if_active'(false', x, y) → mark'(y)
ge_active'(x, y) → ge'(x, y)
if_active'(x, y, z) → if'(x, y, z)
div_active'(x, y) → div'(x, y)

Types:
minus_active' :: 0':s':true':minus':false':ge':div':if' → 0':s':true':minus':false':ge':div':if' → 0':s':true':minus':false':ge':div':if'
0' :: 0':s':true':minus':false':ge':div':if'
mark' :: 0':s':true':minus':false':ge':div':if' → 0':s':true':minus':false':ge':div':if'
s' :: 0':s':true':minus':false':ge':div':if' → 0':s':true':minus':false':ge':div':if'
ge_active' :: 0':s':true':minus':false':ge':div':if' → 0':s':true':minus':false':ge':div':if' → 0':s':true':minus':false':ge':div':if'
true' :: 0':s':true':minus':false':ge':div':if'
minus' :: 0':s':true':minus':false':ge':div':if' → 0':s':true':minus':false':ge':div':if' → 0':s':true':minus':false':ge':div':if'
false' :: 0':s':true':minus':false':ge':div':if'
ge' :: 0':s':true':minus':false':ge':div':if' → 0':s':true':minus':false':ge':div':if' → 0':s':true':minus':false':ge':div':if'
div' :: 0':s':true':minus':false':ge':div':if' → 0':s':true':minus':false':ge':div':if' → 0':s':true':minus':false':ge':div':if'
div_active' :: 0':s':true':minus':false':ge':div':if' → 0':s':true':minus':false':ge':div':if' → 0':s':true':minus':false':ge':div':if'
if' :: 0':s':true':minus':false':ge':div':if' → 0':s':true':minus':false':ge':div':if' → 0':s':true':minus':false':ge':div':if' → 0':s':true':minus':false':ge':div':if'
if_active' :: 0':s':true':minus':false':ge':div':if' → 0':s':true':minus':false':ge':div':if' → 0':s':true':minus':false':ge':div':if' → 0':s':true':minus':false':ge':div':if'
_hole_0':s':true':minus':false':ge':div':if'1 :: 0':s':true':minus':false':ge':div':if'
_gen_0':s':true':minus':false':ge':div':if'2 :: Nat → 0':s':true':minus':false':ge':div':if'

Lemmas:
minus_active'(_gen_0':s':true':minus':false':ge':div':if'2(_n4), _gen_0':s':true':minus':false':ge':div':if'2(_n4)) → _gen_0':s':true':minus':false':ge':div':if'2(0), rt ∈ Ω(1 + n4)
ge_active'(_gen_0':s':true':minus':false':ge':div':if'2(_n1984), _gen_0':s':true':minus':false':ge':div':if'2(_n1984)) → true', rt ∈ Ω(1 + n1984)

Generator Equations:
_gen_0':s':true':minus':false':ge':div':if'2(0) ⇔ 0'
_gen_0':s':true':minus':false':ge':div':if'2(+(x, 1)) ⇔ s'(_gen_0':s':true':minus':false':ge':div':if'2(x))

The following defined symbols remain to be analysed:
mark'

Proved the following rewrite lemma:
mark'(_gen_0':s':true':minus':false':ge':div':if'2(_n3991)) → _gen_0':s':true':minus':false':ge':div':if'2(_n3991), rt ∈ Ω(1 + n3991)

Induction Base:
mark'(_gen_0':s':true':minus':false':ge':div':if'2(0)) →RΩ(1)
0'

Induction Step:
mark'(_gen_0':s':true':minus':false':ge':div':if'2(+(_\$n3992, 1))) →RΩ(1)
s'(mark'(_gen_0':s':true':minus':false':ge':div':if'2(_\$n3992))) →IH
s'(_gen_0':s':true':minus':false':ge':div':if'2(_\$n3992))

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

Rules:
minus_active'(0', y) → 0'
mark'(0') → 0'
minus_active'(s'(x), s'(y)) → minus_active'(x, y)
mark'(s'(x)) → s'(mark'(x))
ge_active'(x, 0') → true'
mark'(minus'(x, y)) → minus_active'(x, y)
ge_active'(0', s'(y)) → false'
mark'(ge'(x, y)) → ge_active'(x, y)
ge_active'(s'(x), s'(y)) → ge_active'(x, y)
mark'(div'(x, y)) → div_active'(mark'(x), y)
div_active'(0', s'(y)) → 0'
mark'(if'(x, y, z)) → if_active'(mark'(x), y, z)
div_active'(s'(x), s'(y)) → if_active'(ge_active'(x, y), s'(div'(minus'(x, y), s'(y))), 0')
if_active'(true', x, y) → mark'(x)
minus_active'(x, y) → minus'(x, y)
if_active'(false', x, y) → mark'(y)
ge_active'(x, y) → ge'(x, y)
if_active'(x, y, z) → if'(x, y, z)
div_active'(x, y) → div'(x, y)

Types:
minus_active' :: 0':s':true':minus':false':ge':div':if' → 0':s':true':minus':false':ge':div':if' → 0':s':true':minus':false':ge':div':if'
0' :: 0':s':true':minus':false':ge':div':if'
mark' :: 0':s':true':minus':false':ge':div':if' → 0':s':true':minus':false':ge':div':if'
s' :: 0':s':true':minus':false':ge':div':if' → 0':s':true':minus':false':ge':div':if'
ge_active' :: 0':s':true':minus':false':ge':div':if' → 0':s':true':minus':false':ge':div':if' → 0':s':true':minus':false':ge':div':if'
true' :: 0':s':true':minus':false':ge':div':if'
minus' :: 0':s':true':minus':false':ge':div':if' → 0':s':true':minus':false':ge':div':if' → 0':s':true':minus':false':ge':div':if'
false' :: 0':s':true':minus':false':ge':div':if'
ge' :: 0':s':true':minus':false':ge':div':if' → 0':s':true':minus':false':ge':div':if' → 0':s':true':minus':false':ge':div':if'
div' :: 0':s':true':minus':false':ge':div':if' → 0':s':true':minus':false':ge':div':if' → 0':s':true':minus':false':ge':div':if'
div_active' :: 0':s':true':minus':false':ge':div':if' → 0':s':true':minus':false':ge':div':if' → 0':s':true':minus':false':ge':div':if'
if' :: 0':s':true':minus':false':ge':div':if' → 0':s':true':minus':false':ge':div':if' → 0':s':true':minus':false':ge':div':if' → 0':s':true':minus':false':ge':div':if'
if_active' :: 0':s':true':minus':false':ge':div':if' → 0':s':true':minus':false':ge':div':if' → 0':s':true':minus':false':ge':div':if' → 0':s':true':minus':false':ge':div':if'
_hole_0':s':true':minus':false':ge':div':if'1 :: 0':s':true':minus':false':ge':div':if'
_gen_0':s':true':minus':false':ge':div':if'2 :: Nat → 0':s':true':minus':false':ge':div':if'

Lemmas:
minus_active'(_gen_0':s':true':minus':false':ge':div':if'2(_n4), _gen_0':s':true':minus':false':ge':div':if'2(_n4)) → _gen_0':s':true':minus':false':ge':div':if'2(0), rt ∈ Ω(1 + n4)
ge_active'(_gen_0':s':true':minus':false':ge':div':if'2(_n1984), _gen_0':s':true':minus':false':ge':div':if'2(_n1984)) → true', rt ∈ Ω(1 + n1984)
mark'(_gen_0':s':true':minus':false':ge':div':if'2(_n3991)) → _gen_0':s':true':minus':false':ge':div':if'2(_n3991), rt ∈ Ω(1 + n3991)

Generator Equations:
_gen_0':s':true':minus':false':ge':div':if'2(0) ⇔ 0'
_gen_0':s':true':minus':false':ge':div':if'2(+(x, 1)) ⇔ s'(_gen_0':s':true':minus':false':ge':div':if'2(x))

No more defined symbols left to analyse.

The lowerbound Ω(n) was proven with the following lemma:
minus_active'(_gen_0':s':true':minus':false':ge':div':if'2(_n4), _gen_0':s':true':minus':false':ge':div':if'2(_n4)) → _gen_0':s':true':minus':false':ge':div':if'2(0), rt ∈ Ω(1 + n4)