minus(X, s(Y)) → pred(minus(X, Y))
minus(X, 0) → X
pred(s(X)) → X
le(s(X), s(Y)) → le(X, Y)
le(s(X), 0) → false
le(0, Y) → true
gcd(0, Y) → 0
gcd(s(X), 0) → s(X)
gcd(s(X), s(Y)) → if(le(Y, X), s(X), s(Y))
if(true, s(X), s(Y)) → gcd(minus(X, Y), s(Y))
if(false, s(X), s(Y)) → gcd(minus(Y, X), s(X))
Renamed function symbols to avoid clashes with predefined symbol.
Runtime Complexity TRS:
The TRS R consists of the following rules:
minus'(X, s'(Y)) → pred'(minus'(X, Y))
minus'(X, 0') → X
pred'(s'(X)) → X
le'(s'(X), s'(Y)) → le'(X, Y)
le'(s'(X), 0') → false'
le'(0', Y) → true'
gcd'(0', Y) → 0'
gcd'(s'(X), 0') → s'(X)
gcd'(s'(X), s'(Y)) → if'(le'(Y, X), s'(X), s'(Y))
if'(true', s'(X), s'(Y)) → gcd'(minus'(X, Y), s'(Y))
if'(false', s'(X), s'(Y)) → gcd'(minus'(Y, X), s'(X))
Infered types.
Rules:
minus'(X, s'(Y)) → pred'(minus'(X, Y))
minus'(X, 0') → X
pred'(s'(X)) → X
le'(s'(X), s'(Y)) → le'(X, Y)
le'(s'(X), 0') → false'
le'(0', Y) → true'
gcd'(0', Y) → 0'
gcd'(s'(X), 0') → s'(X)
gcd'(s'(X), s'(Y)) → if'(le'(Y, X), s'(X), s'(Y))
if'(true', s'(X), s'(Y)) → gcd'(minus'(X, Y), s'(Y))
if'(false', s'(X), s'(Y)) → gcd'(minus'(Y, X), s'(X))
Types:
minus' :: s':0' → s':0' → s':0'
s' :: s':0' → s':0'
pred' :: s':0' → s':0'
0' :: s':0'
le' :: s':0' → s':0' → false':true'
false' :: false':true'
true' :: false':true'
gcd' :: s':0' → s':0' → s':0'
if' :: false':true' → s':0' → s':0' → s':0'
_hole_s':0'1 :: s':0'
_hole_false':true'2 :: false':true'
_gen_s':0'3 :: Nat → s':0'
Heuristically decided to analyse the following defined symbols:
minus', le', gcd'
They will be analysed ascendingly in the following order:
minus' < gcd'
le' < gcd'
Rules:
minus'(X, s'(Y)) → pred'(minus'(X, Y))
minus'(X, 0') → X
pred'(s'(X)) → X
le'(s'(X), s'(Y)) → le'(X, Y)
le'(s'(X), 0') → false'
le'(0', Y) → true'
gcd'(0', Y) → 0'
gcd'(s'(X), 0') → s'(X)
gcd'(s'(X), s'(Y)) → if'(le'(Y, X), s'(X), s'(Y))
if'(true', s'(X), s'(Y)) → gcd'(minus'(X, Y), s'(Y))
if'(false', s'(X), s'(Y)) → gcd'(minus'(Y, X), s'(X))
Types:
minus' :: s':0' → s':0' → s':0'
s' :: s':0' → s':0'
pred' :: s':0' → s':0'
0' :: s':0'
le' :: s':0' → s':0' → false':true'
false' :: false':true'
true' :: false':true'
gcd' :: s':0' → s':0' → s':0'
if' :: false':true' → s':0' → s':0' → s':0'
_hole_s':0'1 :: s':0'
_hole_false':true'2 :: false':true'
_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:
minus', le', gcd'
They will be analysed ascendingly in the following order:
minus' < gcd'
le' < gcd'
Proved the following rewrite lemma:
minus'(_gen_s':0'3(a), _gen_s':0'3(+(1, _n5))) → _*4, rt ∈ Ω(n5)
Induction Base:
minus'(_gen_s':0'3(a), _gen_s':0'3(+(1, 0)))
Induction Step:
minus'(_gen_s':0'3(_a955), _gen_s':0'3(+(1, +(_$n6, 1)))) →RΩ(1)
pred'(minus'(_gen_s':0'3(_a955), _gen_s':0'3(+(1, _$n6)))) →IH
pred'(_*4)
We have rt ∈ Ω(n) and sz ∈ O(n). Thus, we have ircR ∈ Ω(n).
Rules:
minus'(X, s'(Y)) → pred'(minus'(X, Y))
minus'(X, 0') → X
pred'(s'(X)) → X
le'(s'(X), s'(Y)) → le'(X, Y)
le'(s'(X), 0') → false'
le'(0', Y) → true'
gcd'(0', Y) → 0'
gcd'(s'(X), 0') → s'(X)
gcd'(s'(X), s'(Y)) → if'(le'(Y, X), s'(X), s'(Y))
if'(true', s'(X), s'(Y)) → gcd'(minus'(X, Y), s'(Y))
if'(false', s'(X), s'(Y)) → gcd'(minus'(Y, X), s'(X))
Types:
minus' :: s':0' → s':0' → s':0'
s' :: s':0' → s':0'
pred' :: s':0' → s':0'
0' :: s':0'
le' :: s':0' → s':0' → false':true'
false' :: false':true'
true' :: false':true'
gcd' :: s':0' → s':0' → s':0'
if' :: false':true' → s':0' → s':0' → s':0'
_hole_s':0'1 :: s':0'
_hole_false':true'2 :: false':true'
_gen_s':0'3 :: Nat → s':0'
Lemmas:
minus'(_gen_s':0'3(a), _gen_s':0'3(+(1, _n5))) → _*4, rt ∈ Ω(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:
le', gcd'
They will be analysed ascendingly in the following order:
le' < gcd'
Proved the following rewrite lemma:
le'(_gen_s':0'3(+(1, _n1418)), _gen_s':0'3(_n1418)) → false', rt ∈ Ω(1 + n1418)
Induction Base:
le'(_gen_s':0'3(+(1, 0)), _gen_s':0'3(0)) →RΩ(1)
false'
Induction Step:
le'(_gen_s':0'3(+(1, +(_$n1419, 1))), _gen_s':0'3(+(_$n1419, 1))) →RΩ(1)
le'(_gen_s':0'3(+(1, _$n1419)), _gen_s':0'3(_$n1419)) →IH
false'
We have rt ∈ Ω(n) and sz ∈ O(n). Thus, we have ircR ∈ Ω(n).
Rules:
minus'(X, s'(Y)) → pred'(minus'(X, Y))
minus'(X, 0') → X
pred'(s'(X)) → X
le'(s'(X), s'(Y)) → le'(X, Y)
le'(s'(X), 0') → false'
le'(0', Y) → true'
gcd'(0', Y) → 0'
gcd'(s'(X), 0') → s'(X)
gcd'(s'(X), s'(Y)) → if'(le'(Y, X), s'(X), s'(Y))
if'(true', s'(X), s'(Y)) → gcd'(minus'(X, Y), s'(Y))
if'(false', s'(X), s'(Y)) → gcd'(minus'(Y, X), s'(X))
Types:
minus' :: s':0' → s':0' → s':0'
s' :: s':0' → s':0'
pred' :: s':0' → s':0'
0' :: s':0'
le' :: s':0' → s':0' → false':true'
false' :: false':true'
true' :: false':true'
gcd' :: s':0' → s':0' → s':0'
if' :: false':true' → s':0' → s':0' → s':0'
_hole_s':0'1 :: s':0'
_hole_false':true'2 :: false':true'
_gen_s':0'3 :: Nat → s':0'
Lemmas:
minus'(_gen_s':0'3(a), _gen_s':0'3(+(1, _n5))) → _*4, rt ∈ Ω(n5)
le'(_gen_s':0'3(+(1, _n1418)), _gen_s':0'3(_n1418)) → false', rt ∈ Ω(1 + n1418)
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:
gcd'
Could not prove a rewrite lemma for the defined symbol gcd'.
Rules:
minus'(X, s'(Y)) → pred'(minus'(X, Y))
minus'(X, 0') → X
pred'(s'(X)) → X
le'(s'(X), s'(Y)) → le'(X, Y)
le'(s'(X), 0') → false'
le'(0', Y) → true'
gcd'(0', Y) → 0'
gcd'(s'(X), 0') → s'(X)
gcd'(s'(X), s'(Y)) → if'(le'(Y, X), s'(X), s'(Y))
if'(true', s'(X), s'(Y)) → gcd'(minus'(X, Y), s'(Y))
if'(false', s'(X), s'(Y)) → gcd'(minus'(Y, X), s'(X))
Types:
minus' :: s':0' → s':0' → s':0'
s' :: s':0' → s':0'
pred' :: s':0' → s':0'
0' :: s':0'
le' :: s':0' → s':0' → false':true'
false' :: false':true'
true' :: false':true'
gcd' :: s':0' → s':0' → s':0'
if' :: false':true' → s':0' → s':0' → s':0'
_hole_s':0'1 :: s':0'
_hole_false':true'2 :: false':true'
_gen_s':0'3 :: Nat → s':0'
Lemmas:
minus'(_gen_s':0'3(a), _gen_s':0'3(+(1, _n5))) → _*4, rt ∈ Ω(n5)
le'(_gen_s':0'3(+(1, _n1418)), _gen_s':0'3(_n1418)) → false', rt ∈ Ω(1 + n1418)
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:
minus'(_gen_s':0'3(a), _gen_s':0'3(+(1, _n5))) → _*4, rt ∈ Ω(n5)