The Runtime Complexity (innermost) of the given CpxTRS could be proven to be BOUNDS(n^1, INF).

(0) Obligation:

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

(1) DecreasingLoopProof (EQUIVALENT transformation)

The following loop(s) give(s) rise to the lower bound Ω(n¹):
The rewrite sequence
minus_active(s(x), s(y)) →⁺ minus_active(x, y)
gives rise to a decreasing loop by considering the right hand sides subterm at position [].
The pumping substitution is [x / s(x), y / s(y)].
The result substitution is [ ].

(2) BOUNDS(n^1, INF)