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)
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)
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)