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