div(x, s(y)) → d(x, s(y), 0)
d(x, s(y), z) → cond(ge(x, z), x, y, z)
cond(true, x, y, z) → s(d(x, s(y), plus(s(y), z)))
cond(false, x, y, z) → 0
ge(u, 0) → true
ge(0, s(v)) → false
ge(s(u), s(v)) → ge(u, v)
plus(n, 0) → n
plus(n, s(m)) → s(plus(n, m))
Renamed function symbols to avoid clashes with predefined symbol.
Runtime Complexity TRS:
The TRS R consists of the following rules:
div'(x, s'(y)) → d'(x, s'(y), 0')
d'(x, s'(y), z) → cond'(ge'(x, z), x, y, z)
cond'(true', x, y, z) → s'(d'(x, s'(y), plus'(s'(y), z)))
cond'(false', x, y, z) → 0'
ge'(u, 0') → true'
ge'(0', s'(v)) → false'
ge'(s'(u), s'(v)) → ge'(u, v)
plus'(n, 0') → n
plus'(n, s'(m)) → s'(plus'(n, m))
Infered types.
Rules:
div'(x, s'(y)) → d'(x, s'(y), 0')
d'(x, s'(y), z) → cond'(ge'(x, z), x, y, z)
cond'(true', x, y, z) → s'(d'(x, s'(y), plus'(s'(y), z)))
cond'(false', x, y, z) → 0'
ge'(u, 0') → true'
ge'(0', s'(v)) → false'
ge'(s'(u), s'(v)) → ge'(u, v)
plus'(n, 0') → n
plus'(n, s'(m)) → s'(plus'(n, m))
Types:
div' :: s':0' → s':0' → s':0'
s' :: s':0' → s':0'
d' :: s':0' → s':0' → s':0' → s':0'
0' :: s':0'
cond' :: true':false' → s':0' → s':0' → s':0' → s':0'
ge' :: s':0' → s':0' → true':false'
true' :: true':false'
plus' :: s':0' → s':0' → s':0'
false' :: true':false'
_hole_s':0'1 :: s':0'
_hole_true':false'2 :: true':false'
_gen_s':0'3 :: Nat → s':0'
Heuristically decided to analyse the following defined symbols:
d', ge', plus'
They will be analysed ascendingly in the following order:
ge' < d'
plus' < d'
Rules:
div'(x, s'(y)) → d'(x, s'(y), 0')
d'(x, s'(y), z) → cond'(ge'(x, z), x, y, z)
cond'(true', x, y, z) → s'(d'(x, s'(y), plus'(s'(y), z)))
cond'(false', x, y, z) → 0'
ge'(u, 0') → true'
ge'(0', s'(v)) → false'
ge'(s'(u), s'(v)) → ge'(u, v)
plus'(n, 0') → n
plus'(n, s'(m)) → s'(plus'(n, m))
Types:
div' :: s':0' → s':0' → s':0'
s' :: s':0' → s':0'
d' :: s':0' → s':0' → s':0' → s':0'
0' :: s':0'
cond' :: true':false' → s':0' → s':0' → s':0' → s':0'
ge' :: s':0' → s':0' → true':false'
true' :: true':false'
plus' :: s':0' → s':0' → s':0'
false' :: true':false'
_hole_s':0'1 :: s':0'
_hole_true':false'2 :: true':false'
_gen_s':0'3 :: Nat → s':0'
Generator Equations:
_gen_s':0'3(0) ⇔ 0'
_gen_s':0'3(+(x, 1)) ⇔ s'(_gen_s':0'3(x))
The following defined symbols remain to be analysed:
ge', d', plus'
They will be analysed ascendingly in the following order:
ge' < d'
plus' < d'
Proved the following rewrite lemma:
ge'(_gen_s':0'3(_n5), _gen_s':0'3(_n5)) → true', rt ∈ Ω(1 + n5)
Induction Base:
ge'(_gen_s':0'3(0), _gen_s':0'3(0)) →RΩ(1)
true'
Induction Step:
ge'(_gen_s':0'3(+(_$n6, 1)), _gen_s':0'3(+(_$n6, 1))) →RΩ(1)
ge'(_gen_s':0'3(_$n6), _gen_s':0'3(_$n6)) →IH
true'
We have rt ∈ Ω(n) and sz ∈ O(n). Thus, we have ircR ∈ Ω(n).
Rules:
div'(x, s'(y)) → d'(x, s'(y), 0')
d'(x, s'(y), z) → cond'(ge'(x, z), x, y, z)
cond'(true', x, y, z) → s'(d'(x, s'(y), plus'(s'(y), z)))
cond'(false', x, y, z) → 0'
ge'(u, 0') → true'
ge'(0', s'(v)) → false'
ge'(s'(u), s'(v)) → ge'(u, v)
plus'(n, 0') → n
plus'(n, s'(m)) → s'(plus'(n, m))
Types:
div' :: s':0' → s':0' → s':0'
s' :: s':0' → s':0'
d' :: s':0' → s':0' → s':0' → s':0'
0' :: s':0'
cond' :: true':false' → s':0' → s':0' → s':0' → s':0'
ge' :: s':0' → s':0' → true':false'
true' :: true':false'
plus' :: s':0' → s':0' → s':0'
false' :: true':false'
_hole_s':0'1 :: s':0'
_hole_true':false'2 :: true':false'
_gen_s':0'3 :: Nat → s':0'
Lemmas:
ge'(_gen_s':0'3(_n5), _gen_s':0'3(_n5)) → true', rt ∈ Ω(1 + n5)
Generator Equations:
_gen_s':0'3(0) ⇔ 0'
_gen_s':0'3(+(x, 1)) ⇔ s'(_gen_s':0'3(x))
The following defined symbols remain to be analysed:
plus', d'
They will be analysed ascendingly in the following order:
plus' < d'
Proved the following rewrite lemma:
plus'(_gen_s':0'3(a), _gen_s':0'3(_n584)) → _gen_s':0'3(+(_n584, a)), rt ∈ Ω(1 + n584)
Induction Base:
plus'(_gen_s':0'3(a), _gen_s':0'3(0)) →RΩ(1)
_gen_s':0'3(a)
Induction Step:
plus'(_gen_s':0'3(_a717), _gen_s':0'3(+(_$n585, 1))) →RΩ(1)
s'(plus'(_gen_s':0'3(_a717), _gen_s':0'3(_$n585))) →IH
s'(_gen_s':0'3(+(_$n585, _a717)))
We have rt ∈ Ω(n) and sz ∈ O(n). Thus, we have ircR ∈ Ω(n).
Rules:
div'(x, s'(y)) → d'(x, s'(y), 0')
d'(x, s'(y), z) → cond'(ge'(x, z), x, y, z)
cond'(true', x, y, z) → s'(d'(x, s'(y), plus'(s'(y), z)))
cond'(false', x, y, z) → 0'
ge'(u, 0') → true'
ge'(0', s'(v)) → false'
ge'(s'(u), s'(v)) → ge'(u, v)
plus'(n, 0') → n
plus'(n, s'(m)) → s'(plus'(n, m))
Types:
div' :: s':0' → s':0' → s':0'
s' :: s':0' → s':0'
d' :: s':0' → s':0' → s':0' → s':0'
0' :: s':0'
cond' :: true':false' → s':0' → s':0' → s':0' → s':0'
ge' :: s':0' → s':0' → true':false'
true' :: true':false'
plus' :: s':0' → s':0' → s':0'
false' :: true':false'
_hole_s':0'1 :: s':0'
_hole_true':false'2 :: true':false'
_gen_s':0'3 :: Nat → s':0'
Lemmas:
ge'(_gen_s':0'3(_n5), _gen_s':0'3(_n5)) → true', rt ∈ Ω(1 + n5)
plus'(_gen_s':0'3(a), _gen_s':0'3(_n584)) → _gen_s':0'3(+(_n584, a)), rt ∈ Ω(1 + n584)
Generator Equations:
_gen_s':0'3(0) ⇔ 0'
_gen_s':0'3(+(x, 1)) ⇔ s'(_gen_s':0'3(x))
The following defined symbols remain to be analysed:
d'
Could not prove a rewrite lemma for the defined symbol d'.
Rules:
div'(x, s'(y)) → d'(x, s'(y), 0')
d'(x, s'(y), z) → cond'(ge'(x, z), x, y, z)
cond'(true', x, y, z) → s'(d'(x, s'(y), plus'(s'(y), z)))
cond'(false', x, y, z) → 0'
ge'(u, 0') → true'
ge'(0', s'(v)) → false'
ge'(s'(u), s'(v)) → ge'(u, v)
plus'(n, 0') → n
plus'(n, s'(m)) → s'(plus'(n, m))
Types:
div' :: s':0' → s':0' → s':0'
s' :: s':0' → s':0'
d' :: s':0' → s':0' → s':0' → s':0'
0' :: s':0'
cond' :: true':false' → s':0' → s':0' → s':0' → s':0'
ge' :: s':0' → s':0' → true':false'
true' :: true':false'
plus' :: s':0' → s':0' → s':0'
false' :: true':false'
_hole_s':0'1 :: s':0'
_hole_true':false'2 :: true':false'
_gen_s':0'3 :: Nat → s':0'
Lemmas:
ge'(_gen_s':0'3(_n5), _gen_s':0'3(_n5)) → true', rt ∈ Ω(1 + n5)
plus'(_gen_s':0'3(a), _gen_s':0'3(_n584)) → _gen_s':0'3(+(_n584, a)), rt ∈ Ω(1 + n584)
Generator Equations:
_gen_s':0'3(0) ⇔ 0'
_gen_s':0'3(+(x, 1)) ⇔ s'(_gen_s':0'3(x))
No more defined symbols left to analyse.
The lowerbound Ω(n) was proven with the following lemma:
ge'(_gen_s':0'3(_n5), _gen_s':0'3(_n5)) → true', rt ∈ Ω(1 + n5)