lcm(x, y) → lcmIter(x, y, 0, times(x, y))
lcmIter(x, y, z, u) → if(or(ge(0, x), ge(z, u)), x, y, z, u)
if(true, x, y, z, u) → z
if(false, x, y, z, u) → if2(divisible(z, y), x, y, z, u)
if2(true, x, y, z, u) → z
if2(false, x, y, z, u) → lcmIter(x, y, plus(x, z), u)
plus(0, y) → y
plus(s(x), y) → s(plus(x, y))
times(x, y) → ifTimes(ge(0, x), x, y)
ifTimes(true, x, y) → 0
ifTimes(false, x, y) → plus(y, times(y, p(x)))
p(s(x)) → x
p(0) → s(s(0))
ge(x, 0) → true
ge(0, s(y)) → false
ge(s(x), s(y)) → ge(x, y)
or(true, y) → true
or(false, y) → y
divisible(0, s(y)) → true
divisible(s(x), s(y)) → div(s(x), s(y), s(y))
div(x, y, 0) → divisible(x, y)
div(0, y, s(z)) → false
div(s(x), y, s(z)) → div(x, y, z)
a → b
a → c
Renamed function symbols to avoid clashes with predefined symbol.
Runtime Complexity TRS:
The TRS R consists of the following rules:
lcm'(x, y) → lcmIter'(x, y, 0', times'(x, y))
lcmIter'(x, y, z, u) → if'(or'(ge'(0', x), ge'(z, u)), x, y, z, u)
if'(true', x, y, z, u) → z
if'(false', x, y, z, u) → if2'(divisible'(z, y), x, y, z, u)
if2'(true', x, y, z, u) → z
if2'(false', x, y, z, u) → lcmIter'(x, y, plus'(x, z), u)
plus'(0', y) → y
plus'(s'(x), y) → s'(plus'(x, y))
times'(x, y) → ifTimes'(ge'(0', x), x, y)
ifTimes'(true', x, y) → 0'
ifTimes'(false', x, y) → plus'(y, times'(y, p'(x)))
p'(s'(x)) → x
p'(0') → s'(s'(0'))
ge'(x, 0') → true'
ge'(0', s'(y)) → false'
ge'(s'(x), s'(y)) → ge'(x, y)
or'(true', y) → true'
or'(false', y) → y
divisible'(0', s'(y)) → true'
divisible'(s'(x), s'(y)) → div'(s'(x), s'(y), s'(y))
div'(x, y, 0') → divisible'(x, y)
div'(0', y, s'(z)) → false'
div'(s'(x), y, s'(z)) → div'(x, y, z)
a' → b'
a' → c'
Infered types.
Rules:
lcm'(x, y) → lcmIter'(x, y, 0', times'(x, y))
lcmIter'(x, y, z, u) → if'(or'(ge'(0', x), ge'(z, u)), x, y, z, u)
if'(true', x, y, z, u) → z
if'(false', x, y, z, u) → if2'(divisible'(z, y), x, y, z, u)
if2'(true', x, y, z, u) → z
if2'(false', x, y, z, u) → lcmIter'(x, y, plus'(x, z), u)
plus'(0', y) → y
plus'(s'(x), y) → s'(plus'(x, y))
times'(x, y) → ifTimes'(ge'(0', x), x, y)
ifTimes'(true', x, y) → 0'
ifTimes'(false', x, y) → plus'(y, times'(y, p'(x)))
p'(s'(x)) → x
p'(0') → s'(s'(0'))
ge'(x, 0') → true'
ge'(0', s'(y)) → false'
ge'(s'(x), s'(y)) → ge'(x, y)
or'(true', y) → true'
or'(false', y) → y
divisible'(0', s'(y)) → true'
divisible'(s'(x), s'(y)) → div'(s'(x), s'(y), s'(y))
div'(x, y, 0') → divisible'(x, y)
div'(0', y, s'(z)) → false'
div'(s'(x), y, s'(z)) → div'(x, y, z)
a' → b'
a' → c'
Types:
lcm' :: 0':s' → 0':s' → 0':s'
lcmIter' :: 0':s' → 0':s' → 0':s' → 0':s' → 0':s'
0' :: 0':s'
times' :: 0':s' → 0':s' → 0':s'
if' :: true':false' → 0':s' → 0':s' → 0':s' → 0':s' → 0':s'
or' :: true':false' → true':false' → true':false'
ge' :: 0':s' → 0':s' → true':false'
true' :: true':false'
false' :: true':false'
if2' :: true':false' → 0':s' → 0':s' → 0':s' → 0':s' → 0':s'
divisible' :: 0':s' → 0':s' → true':false'
plus' :: 0':s' → 0':s' → 0':s'
s' :: 0':s' → 0':s'
ifTimes' :: true':false' → 0':s' → 0':s' → 0':s'
p' :: 0':s' → 0':s'
div' :: 0':s' → 0':s' → 0':s' → true':false'
a' :: b':c'
b' :: b':c'
c' :: b':c'
_hole_0':s'1 :: 0':s'
_hole_true':false'2 :: true':false'
_hole_b':c'3 :: b':c'
_gen_0':s'4 :: Nat → 0':s'
Heuristically decided to analyse the following defined symbols:
lcmIter', times', ge', divisible', plus', div'
They will be analysed ascendingly in the following order:
ge' < lcmIter'
divisible' < lcmIter'
plus' < lcmIter'
ge' < times'
plus' < times'
divisible' = div'
Rules:
lcm'(x, y) → lcmIter'(x, y, 0', times'(x, y))
lcmIter'(x, y, z, u) → if'(or'(ge'(0', x), ge'(z, u)), x, y, z, u)
if'(true', x, y, z, u) → z
if'(false', x, y, z, u) → if2'(divisible'(z, y), x, y, z, u)
if2'(true', x, y, z, u) → z
if2'(false', x, y, z, u) → lcmIter'(x, y, plus'(x, z), u)
plus'(0', y) → y
plus'(s'(x), y) → s'(plus'(x, y))
times'(x, y) → ifTimes'(ge'(0', x), x, y)
ifTimes'(true', x, y) → 0'
ifTimes'(false', x, y) → plus'(y, times'(y, p'(x)))
p'(s'(x)) → x
p'(0') → s'(s'(0'))
ge'(x, 0') → true'
ge'(0', s'(y)) → false'
ge'(s'(x), s'(y)) → ge'(x, y)
or'(true', y) → true'
or'(false', y) → y
divisible'(0', s'(y)) → true'
divisible'(s'(x), s'(y)) → div'(s'(x), s'(y), s'(y))
div'(x, y, 0') → divisible'(x, y)
div'(0', y, s'(z)) → false'
div'(s'(x), y, s'(z)) → div'(x, y, z)
a' → b'
a' → c'
Types:
lcm' :: 0':s' → 0':s' → 0':s'
lcmIter' :: 0':s' → 0':s' → 0':s' → 0':s' → 0':s'
0' :: 0':s'
times' :: 0':s' → 0':s' → 0':s'
if' :: true':false' → 0':s' → 0':s' → 0':s' → 0':s' → 0':s'
or' :: true':false' → true':false' → true':false'
ge' :: 0':s' → 0':s' → true':false'
true' :: true':false'
false' :: true':false'
if2' :: true':false' → 0':s' → 0':s' → 0':s' → 0':s' → 0':s'
divisible' :: 0':s' → 0':s' → true':false'
plus' :: 0':s' → 0':s' → 0':s'
s' :: 0':s' → 0':s'
ifTimes' :: true':false' → 0':s' → 0':s' → 0':s'
p' :: 0':s' → 0':s'
div' :: 0':s' → 0':s' → 0':s' → true':false'
a' :: b':c'
b' :: b':c'
c' :: b':c'
_hole_0':s'1 :: 0':s'
_hole_true':false'2 :: true':false'
_hole_b':c'3 :: b':c'
_gen_0':s'4 :: Nat → 0':s'
Generator Equations:
_gen_0':s'4(0) ⇔ 0'
_gen_0':s'4(+(x, 1)) ⇔ s'(_gen_0':s'4(x))
The following defined symbols remain to be analysed:
ge', lcmIter', times', divisible', plus', div'
They will be analysed ascendingly in the following order:
ge' < lcmIter'
divisible' < lcmIter'
plus' < lcmIter'
ge' < times'
plus' < times'
divisible' = div'
Proved the following rewrite lemma:
ge'(_gen_0':s'4(_n6), _gen_0':s'4(_n6)) → true', rt ∈ Ω(1 + n6)
Induction Base:
ge'(_gen_0':s'4(0), _gen_0':s'4(0)) →RΩ(1)
true'
Induction Step:
ge'(_gen_0':s'4(+(_$n7, 1)), _gen_0':s'4(+(_$n7, 1))) →RΩ(1)
ge'(_gen_0':s'4(_$n7), _gen_0':s'4(_$n7)) →IH
true'
We have rt ∈ Ω(n) and sz ∈ O(n). Thus, we have ircR ∈ Ω(n).
Rules:
lcm'(x, y) → lcmIter'(x, y, 0', times'(x, y))
lcmIter'(x, y, z, u) → if'(or'(ge'(0', x), ge'(z, u)), x, y, z, u)
if'(true', x, y, z, u) → z
if'(false', x, y, z, u) → if2'(divisible'(z, y), x, y, z, u)
if2'(true', x, y, z, u) → z
if2'(false', x, y, z, u) → lcmIter'(x, y, plus'(x, z), u)
plus'(0', y) → y
plus'(s'(x), y) → s'(plus'(x, y))
times'(x, y) → ifTimes'(ge'(0', x), x, y)
ifTimes'(true', x, y) → 0'
ifTimes'(false', x, y) → plus'(y, times'(y, p'(x)))
p'(s'(x)) → x
p'(0') → s'(s'(0'))
ge'(x, 0') → true'
ge'(0', s'(y)) → false'
ge'(s'(x), s'(y)) → ge'(x, y)
or'(true', y) → true'
or'(false', y) → y
divisible'(0', s'(y)) → true'
divisible'(s'(x), s'(y)) → div'(s'(x), s'(y), s'(y))
div'(x, y, 0') → divisible'(x, y)
div'(0', y, s'(z)) → false'
div'(s'(x), y, s'(z)) → div'(x, y, z)
a' → b'
a' → c'
Types:
lcm' :: 0':s' → 0':s' → 0':s'
lcmIter' :: 0':s' → 0':s' → 0':s' → 0':s' → 0':s'
0' :: 0':s'
times' :: 0':s' → 0':s' → 0':s'
if' :: true':false' → 0':s' → 0':s' → 0':s' → 0':s' → 0':s'
or' :: true':false' → true':false' → true':false'
ge' :: 0':s' → 0':s' → true':false'
true' :: true':false'
false' :: true':false'
if2' :: true':false' → 0':s' → 0':s' → 0':s' → 0':s' → 0':s'
divisible' :: 0':s' → 0':s' → true':false'
plus' :: 0':s' → 0':s' → 0':s'
s' :: 0':s' → 0':s'
ifTimes' :: true':false' → 0':s' → 0':s' → 0':s'
p' :: 0':s' → 0':s'
div' :: 0':s' → 0':s' → 0':s' → true':false'
a' :: b':c'
b' :: b':c'
c' :: b':c'
_hole_0':s'1 :: 0':s'
_hole_true':false'2 :: true':false'
_hole_b':c'3 :: b':c'
_gen_0':s'4 :: Nat → 0':s'
Lemmas:
ge'(_gen_0':s'4(_n6), _gen_0':s'4(_n6)) → true', rt ∈ Ω(1 + n6)
Generator Equations:
_gen_0':s'4(0) ⇔ 0'
_gen_0':s'4(+(x, 1)) ⇔ s'(_gen_0':s'4(x))
The following defined symbols remain to be analysed:
plus', lcmIter', times', divisible', div'
They will be analysed ascendingly in the following order:
divisible' < lcmIter'
plus' < lcmIter'
plus' < times'
divisible' = div'
Proved the following rewrite lemma:
plus'(_gen_0':s'4(_n1353), _gen_0':s'4(b)) → _gen_0':s'4(+(_n1353, b)), rt ∈ Ω(1 + n1353)
Induction Base:
plus'(_gen_0':s'4(0), _gen_0':s'4(b)) →RΩ(1)
_gen_0':s'4(b)
Induction Step:
plus'(_gen_0':s'4(+(_$n1354, 1)), _gen_0':s'4(_b1486)) →RΩ(1)
s'(plus'(_gen_0':s'4(_$n1354), _gen_0':s'4(_b1486))) →IH
s'(_gen_0':s'4(+(_$n1354, _b1486)))
We have rt ∈ Ω(n) and sz ∈ O(n). Thus, we have ircR ∈ Ω(n).
Rules:
lcm'(x, y) → lcmIter'(x, y, 0', times'(x, y))
lcmIter'(x, y, z, u) → if'(or'(ge'(0', x), ge'(z, u)), x, y, z, u)
if'(true', x, y, z, u) → z
if'(false', x, y, z, u) → if2'(divisible'(z, y), x, y, z, u)
if2'(true', x, y, z, u) → z
if2'(false', x, y, z, u) → lcmIter'(x, y, plus'(x, z), u)
plus'(0', y) → y
plus'(s'(x), y) → s'(plus'(x, y))
times'(x, y) → ifTimes'(ge'(0', x), x, y)
ifTimes'(true', x, y) → 0'
ifTimes'(false', x, y) → plus'(y, times'(y, p'(x)))
p'(s'(x)) → x
p'(0') → s'(s'(0'))
ge'(x, 0') → true'
ge'(0', s'(y)) → false'
ge'(s'(x), s'(y)) → ge'(x, y)
or'(true', y) → true'
or'(false', y) → y
divisible'(0', s'(y)) → true'
divisible'(s'(x), s'(y)) → div'(s'(x), s'(y), s'(y))
div'(x, y, 0') → divisible'(x, y)
div'(0', y, s'(z)) → false'
div'(s'(x), y, s'(z)) → div'(x, y, z)
a' → b'
a' → c'
Types:
lcm' :: 0':s' → 0':s' → 0':s'
lcmIter' :: 0':s' → 0':s' → 0':s' → 0':s' → 0':s'
0' :: 0':s'
times' :: 0':s' → 0':s' → 0':s'
if' :: true':false' → 0':s' → 0':s' → 0':s' → 0':s' → 0':s'
or' :: true':false' → true':false' → true':false'
ge' :: 0':s' → 0':s' → true':false'
true' :: true':false'
false' :: true':false'
if2' :: true':false' → 0':s' → 0':s' → 0':s' → 0':s' → 0':s'
divisible' :: 0':s' → 0':s' → true':false'
plus' :: 0':s' → 0':s' → 0':s'
s' :: 0':s' → 0':s'
ifTimes' :: true':false' → 0':s' → 0':s' → 0':s'
p' :: 0':s' → 0':s'
div' :: 0':s' → 0':s' → 0':s' → true':false'
a' :: b':c'
b' :: b':c'
c' :: b':c'
_hole_0':s'1 :: 0':s'
_hole_true':false'2 :: true':false'
_hole_b':c'3 :: b':c'
_gen_0':s'4 :: Nat → 0':s'
Lemmas:
ge'(_gen_0':s'4(_n6), _gen_0':s'4(_n6)) → true', rt ∈ Ω(1 + n6)
plus'(_gen_0':s'4(_n1353), _gen_0':s'4(b)) → _gen_0':s'4(+(_n1353, b)), rt ∈ Ω(1 + n1353)
Generator Equations:
_gen_0':s'4(0) ⇔ 0'
_gen_0':s'4(+(x, 1)) ⇔ s'(_gen_0':s'4(x))
The following defined symbols remain to be analysed:
times', lcmIter', divisible', div'
They will be analysed ascendingly in the following order:
divisible' < lcmIter'
divisible' = div'
Could not prove a rewrite lemma for the defined symbol times'.
Rules:
lcm'(x, y) → lcmIter'(x, y, 0', times'(x, y))
lcmIter'(x, y, z, u) → if'(or'(ge'(0', x), ge'(z, u)), x, y, z, u)
if'(true', x, y, z, u) → z
if'(false', x, y, z, u) → if2'(divisible'(z, y), x, y, z, u)
if2'(true', x, y, z, u) → z
if2'(false', x, y, z, u) → lcmIter'(x, y, plus'(x, z), u)
plus'(0', y) → y
plus'(s'(x), y) → s'(plus'(x, y))
times'(x, y) → ifTimes'(ge'(0', x), x, y)
ifTimes'(true', x, y) → 0'
ifTimes'(false', x, y) → plus'(y, times'(y, p'(x)))
p'(s'(x)) → x
p'(0') → s'(s'(0'))
ge'(x, 0') → true'
ge'(0', s'(y)) → false'
ge'(s'(x), s'(y)) → ge'(x, y)
or'(true', y) → true'
or'(false', y) → y
divisible'(0', s'(y)) → true'
divisible'(s'(x), s'(y)) → div'(s'(x), s'(y), s'(y))
div'(x, y, 0') → divisible'(x, y)
div'(0', y, s'(z)) → false'
div'(s'(x), y, s'(z)) → div'(x, y, z)
a' → b'
a' → c'
Types:
lcm' :: 0':s' → 0':s' → 0':s'
lcmIter' :: 0':s' → 0':s' → 0':s' → 0':s' → 0':s'
0' :: 0':s'
times' :: 0':s' → 0':s' → 0':s'
if' :: true':false' → 0':s' → 0':s' → 0':s' → 0':s' → 0':s'
or' :: true':false' → true':false' → true':false'
ge' :: 0':s' → 0':s' → true':false'
true' :: true':false'
false' :: true':false'
if2' :: true':false' → 0':s' → 0':s' → 0':s' → 0':s' → 0':s'
divisible' :: 0':s' → 0':s' → true':false'
plus' :: 0':s' → 0':s' → 0':s'
s' :: 0':s' → 0':s'
ifTimes' :: true':false' → 0':s' → 0':s' → 0':s'
p' :: 0':s' → 0':s'
div' :: 0':s' → 0':s' → 0':s' → true':false'
a' :: b':c'
b' :: b':c'
c' :: b':c'
_hole_0':s'1 :: 0':s'
_hole_true':false'2 :: true':false'
_hole_b':c'3 :: b':c'
_gen_0':s'4 :: Nat → 0':s'
Lemmas:
ge'(_gen_0':s'4(_n6), _gen_0':s'4(_n6)) → true', rt ∈ Ω(1 + n6)
plus'(_gen_0':s'4(_n1353), _gen_0':s'4(b)) → _gen_0':s'4(+(_n1353, b)), rt ∈ Ω(1 + n1353)
Generator Equations:
_gen_0':s'4(0) ⇔ 0'
_gen_0':s'4(+(x, 1)) ⇔ s'(_gen_0':s'4(x))
The following defined symbols remain to be analysed:
div', lcmIter', divisible'
They will be analysed ascendingly in the following order:
divisible' < lcmIter'
divisible' = div'
Proved the following rewrite lemma:
div'(_gen_0':s'4(_n3064), _gen_0':s'4(b), _gen_0':s'4(+(1, _n3064))) → false', rt ∈ Ω(1 + n3064)
Induction Base:
div'(_gen_0':s'4(0), _gen_0':s'4(b), _gen_0':s'4(+(1, 0))) →RΩ(1)
false'
Induction Step:
div'(_gen_0':s'4(+(_$n3065, 1)), _gen_0':s'4(_b3376), _gen_0':s'4(+(1, +(_$n3065, 1)))) →RΩ(1)
div'(_gen_0':s'4(_$n3065), _gen_0':s'4(_b3376), _gen_0':s'4(+(1, _$n3065))) →IH
false'
We have rt ∈ Ω(n) and sz ∈ O(n). Thus, we have ircR ∈ Ω(n).
Rules:
lcm'(x, y) → lcmIter'(x, y, 0', times'(x, y))
lcmIter'(x, y, z, u) → if'(or'(ge'(0', x), ge'(z, u)), x, y, z, u)
if'(true', x, y, z, u) → z
if'(false', x, y, z, u) → if2'(divisible'(z, y), x, y, z, u)
if2'(true', x, y, z, u) → z
if2'(false', x, y, z, u) → lcmIter'(x, y, plus'(x, z), u)
plus'(0', y) → y
plus'(s'(x), y) → s'(plus'(x, y))
times'(x, y) → ifTimes'(ge'(0', x), x, y)
ifTimes'(true', x, y) → 0'
ifTimes'(false', x, y) → plus'(y, times'(y, p'(x)))
p'(s'(x)) → x
p'(0') → s'(s'(0'))
ge'(x, 0') → true'
ge'(0', s'(y)) → false'
ge'(s'(x), s'(y)) → ge'(x, y)
or'(true', y) → true'
or'(false', y) → y
divisible'(0', s'(y)) → true'
divisible'(s'(x), s'(y)) → div'(s'(x), s'(y), s'(y))
div'(x, y, 0') → divisible'(x, y)
div'(0', y, s'(z)) → false'
div'(s'(x), y, s'(z)) → div'(x, y, z)
a' → b'
a' → c'
Types:
lcm' :: 0':s' → 0':s' → 0':s'
lcmIter' :: 0':s' → 0':s' → 0':s' → 0':s' → 0':s'
0' :: 0':s'
times' :: 0':s' → 0':s' → 0':s'
if' :: true':false' → 0':s' → 0':s' → 0':s' → 0':s' → 0':s'
or' :: true':false' → true':false' → true':false'
ge' :: 0':s' → 0':s' → true':false'
true' :: true':false'
false' :: true':false'
if2' :: true':false' → 0':s' → 0':s' → 0':s' → 0':s' → 0':s'
divisible' :: 0':s' → 0':s' → true':false'
plus' :: 0':s' → 0':s' → 0':s'
s' :: 0':s' → 0':s'
ifTimes' :: true':false' → 0':s' → 0':s' → 0':s'
p' :: 0':s' → 0':s'
div' :: 0':s' → 0':s' → 0':s' → true':false'
a' :: b':c'
b' :: b':c'
c' :: b':c'
_hole_0':s'1 :: 0':s'
_hole_true':false'2 :: true':false'
_hole_b':c'3 :: b':c'
_gen_0':s'4 :: Nat → 0':s'
Lemmas:
ge'(_gen_0':s'4(_n6), _gen_0':s'4(_n6)) → true', rt ∈ Ω(1 + n6)
plus'(_gen_0':s'4(_n1353), _gen_0':s'4(b)) → _gen_0':s'4(+(_n1353, b)), rt ∈ Ω(1 + n1353)
div'(_gen_0':s'4(_n3064), _gen_0':s'4(b), _gen_0':s'4(+(1, _n3064))) → false', rt ∈ Ω(1 + n3064)
Generator Equations:
_gen_0':s'4(0) ⇔ 0'
_gen_0':s'4(+(x, 1)) ⇔ s'(_gen_0':s'4(x))
The following defined symbols remain to be analysed:
divisible', lcmIter'
They will be analysed ascendingly in the following order:
divisible' < lcmIter'
divisible' = div'
Could not prove a rewrite lemma for the defined symbol divisible'.
Rules:
lcm'(x, y) → lcmIter'(x, y, 0', times'(x, y))
lcmIter'(x, y, z, u) → if'(or'(ge'(0', x), ge'(z, u)), x, y, z, u)
if'(true', x, y, z, u) → z
if'(false', x, y, z, u) → if2'(divisible'(z, y), x, y, z, u)
if2'(true', x, y, z, u) → z
if2'(false', x, y, z, u) → lcmIter'(x, y, plus'(x, z), u)
plus'(0', y) → y
plus'(s'(x), y) → s'(plus'(x, y))
times'(x, y) → ifTimes'(ge'(0', x), x, y)
ifTimes'(true', x, y) → 0'
ifTimes'(false', x, y) → plus'(y, times'(y, p'(x)))
p'(s'(x)) → x
p'(0') → s'(s'(0'))
ge'(x, 0') → true'
ge'(0', s'(y)) → false'
ge'(s'(x), s'(y)) → ge'(x, y)
or'(true', y) → true'
or'(false', y) → y
divisible'(0', s'(y)) → true'
divisible'(s'(x), s'(y)) → div'(s'(x), s'(y), s'(y))
div'(x, y, 0') → divisible'(x, y)
div'(0', y, s'(z)) → false'
div'(s'(x), y, s'(z)) → div'(x, y, z)
a' → b'
a' → c'
Types:
lcm' :: 0':s' → 0':s' → 0':s'
lcmIter' :: 0':s' → 0':s' → 0':s' → 0':s' → 0':s'
0' :: 0':s'
times' :: 0':s' → 0':s' → 0':s'
if' :: true':false' → 0':s' → 0':s' → 0':s' → 0':s' → 0':s'
or' :: true':false' → true':false' → true':false'
ge' :: 0':s' → 0':s' → true':false'
true' :: true':false'
false' :: true':false'
if2' :: true':false' → 0':s' → 0':s' → 0':s' → 0':s' → 0':s'
divisible' :: 0':s' → 0':s' → true':false'
plus' :: 0':s' → 0':s' → 0':s'
s' :: 0':s' → 0':s'
ifTimes' :: true':false' → 0':s' → 0':s' → 0':s'
p' :: 0':s' → 0':s'
div' :: 0':s' → 0':s' → 0':s' → true':false'
a' :: b':c'
b' :: b':c'
c' :: b':c'
_hole_0':s'1 :: 0':s'
_hole_true':false'2 :: true':false'
_hole_b':c'3 :: b':c'
_gen_0':s'4 :: Nat → 0':s'
Lemmas:
ge'(_gen_0':s'4(_n6), _gen_0':s'4(_n6)) → true', rt ∈ Ω(1 + n6)
plus'(_gen_0':s'4(_n1353), _gen_0':s'4(b)) → _gen_0':s'4(+(_n1353, b)), rt ∈ Ω(1 + n1353)
div'(_gen_0':s'4(_n3064), _gen_0':s'4(b), _gen_0':s'4(+(1, _n3064))) → false', rt ∈ Ω(1 + n3064)
Generator Equations:
_gen_0':s'4(0) ⇔ 0'
_gen_0':s'4(+(x, 1)) ⇔ s'(_gen_0':s'4(x))
The following defined symbols remain to be analysed:
lcmIter'
Could not prove a rewrite lemma for the defined symbol lcmIter'.
Rules:
lcm'(x, y) → lcmIter'(x, y, 0', times'(x, y))
lcmIter'(x, y, z, u) → if'(or'(ge'(0', x), ge'(z, u)), x, y, z, u)
if'(true', x, y, z, u) → z
if'(false', x, y, z, u) → if2'(divisible'(z, y), x, y, z, u)
if2'(true', x, y, z, u) → z
if2'(false', x, y, z, u) → lcmIter'(x, y, plus'(x, z), u)
plus'(0', y) → y
plus'(s'(x), y) → s'(plus'(x, y))
times'(x, y) → ifTimes'(ge'(0', x), x, y)
ifTimes'(true', x, y) → 0'
ifTimes'(false', x, y) → plus'(y, times'(y, p'(x)))
p'(s'(x)) → x
p'(0') → s'(s'(0'))
ge'(x, 0') → true'
ge'(0', s'(y)) → false'
ge'(s'(x), s'(y)) → ge'(x, y)
or'(true', y) → true'
or'(false', y) → y
divisible'(0', s'(y)) → true'
divisible'(s'(x), s'(y)) → div'(s'(x), s'(y), s'(y))
div'(x, y, 0') → divisible'(x, y)
div'(0', y, s'(z)) → false'
div'(s'(x), y, s'(z)) → div'(x, y, z)
a' → b'
a' → c'
Types:
lcm' :: 0':s' → 0':s' → 0':s'
lcmIter' :: 0':s' → 0':s' → 0':s' → 0':s' → 0':s'
0' :: 0':s'
times' :: 0':s' → 0':s' → 0':s'
if' :: true':false' → 0':s' → 0':s' → 0':s' → 0':s' → 0':s'
or' :: true':false' → true':false' → true':false'
ge' :: 0':s' → 0':s' → true':false'
true' :: true':false'
false' :: true':false'
if2' :: true':false' → 0':s' → 0':s' → 0':s' → 0':s' → 0':s'
divisible' :: 0':s' → 0':s' → true':false'
plus' :: 0':s' → 0':s' → 0':s'
s' :: 0':s' → 0':s'
ifTimes' :: true':false' → 0':s' → 0':s' → 0':s'
p' :: 0':s' → 0':s'
div' :: 0':s' → 0':s' → 0':s' → true':false'
a' :: b':c'
b' :: b':c'
c' :: b':c'
_hole_0':s'1 :: 0':s'
_hole_true':false'2 :: true':false'
_hole_b':c'3 :: b':c'
_gen_0':s'4 :: Nat → 0':s'
Lemmas:
ge'(_gen_0':s'4(_n6), _gen_0':s'4(_n6)) → true', rt ∈ Ω(1 + n6)
plus'(_gen_0':s'4(_n1353), _gen_0':s'4(b)) → _gen_0':s'4(+(_n1353, b)), rt ∈ Ω(1 + n1353)
div'(_gen_0':s'4(_n3064), _gen_0':s'4(b), _gen_0':s'4(+(1, _n3064))) → false', rt ∈ Ω(1 + n3064)
Generator Equations:
_gen_0':s'4(0) ⇔ 0'
_gen_0':s'4(+(x, 1)) ⇔ s'(_gen_0':s'4(x))
No more defined symbols left to analyse.
The lowerbound Ω(n) was proven with the following lemma:
ge'(_gen_0':s'4(_n6), _gen_0':s'4(_n6)) → true', rt ∈ Ω(1 + n6)