plus(x, y) → ifPlus(isZero(x), x, inc(y))
ifPlus(true, x, y) → p(y)
ifPlus(false, x, y) → plus(p(x), y)
times(x, y) → timesIter(0, x, y, 0)
timesIter(i, x, y, z) → ifTimes(ge(i, x), i, x, y, z)
ifTimes(true, i, x, y, z) → z
ifTimes(false, i, x, y, z) → timesIter(inc(i), x, y, plus(z, y))
isZero(0) → true
isZero(s(0)) → false
isZero(s(s(x))) → isZero(s(x))
inc(0) → s(0)
inc(s(x)) → s(inc(x))
inc(x) → s(x)
p(0) → 0
p(s(x)) → x
p(s(s(x))) → s(p(s(x)))
ge(x, 0) → true
ge(0, s(y)) → false
ge(s(x), s(y)) → ge(x, y)
f0(0, y, x) → f1(x, y, x)
f1(x, y, z) → f2(x, y, z)
f2(x, 1, z) → f0(x, z, z)
f0(x, y, z) → d
f1(x, y, z) → c
Renamed function symbols to avoid clashes with predefined symbol.
Runtime Complexity TRS:
The TRS R consists of the following rules:
plus'(x, y) → ifPlus'(isZero'(x), x, inc'(y))
ifPlus'(true', x, y) → p'(y)
ifPlus'(false', x, y) → plus'(p'(x), y)
times'(x, y) → timesIter'(0', x, y, 0')
timesIter'(i, x, y, z) → ifTimes'(ge'(i, x), i, x, y, z)
ifTimes'(true', i, x, y, z) → z
ifTimes'(false', i, x, y, z) → timesIter'(inc'(i), x, y, plus'(z, y))
isZero'(0') → true'
isZero'(s'(0')) → false'
isZero'(s'(s'(x))) → isZero'(s'(x))
inc'(0') → s'(0')
inc'(s'(x)) → s'(inc'(x))
inc'(x) → s'(x)
p'(0') → 0'
p'(s'(x)) → x
p'(s'(s'(x))) → s'(p'(s'(x)))
ge'(x, 0') → true'
ge'(0', s'(y)) → false'
ge'(s'(x), s'(y)) → ge'(x, y)
f0'(0', y, x) → f1'(x, y, x)
f1'(x, y, z) → f2'(x, y, z)
f2'(x, 1', z) → f0'(x, z, z)
f0'(x, y, z) → d'
f1'(x, y, z) → c'
Infered types.
Rules:
plus'(x, y) → ifPlus'(isZero'(x), x, inc'(y))
ifPlus'(true', x, y) → p'(y)
ifPlus'(false', x, y) → plus'(p'(x), y)
times'(x, y) → timesIter'(0', x, y, 0')
timesIter'(i, x, y, z) → ifTimes'(ge'(i, x), i, x, y, z)
ifTimes'(true', i, x, y, z) → z
ifTimes'(false', i, x, y, z) → timesIter'(inc'(i), x, y, plus'(z, y))
isZero'(0') → true'
isZero'(s'(0')) → false'
isZero'(s'(s'(x))) → isZero'(s'(x))
inc'(0') → s'(0')
inc'(s'(x)) → s'(inc'(x))
inc'(x) → s'(x)
p'(0') → 0'
p'(s'(x)) → x
p'(s'(s'(x))) → s'(p'(s'(x)))
ge'(x, 0') → true'
ge'(0', s'(y)) → false'
ge'(s'(x), s'(y)) → ge'(x, y)
f0'(0', y, x) → f1'(x, y, x)
f1'(x, y, z) → f2'(x, y, z)
f2'(x, 1', z) → f0'(x, z, z)
f0'(x, y, z) → d'
f1'(x, y, z) → c'
Types:
plus' :: 0':s':1' → 0':s':1' → 0':s':1'
ifPlus' :: true':false' → 0':s':1' → 0':s':1' → 0':s':1'
isZero' :: 0':s':1' → true':false'
inc' :: 0':s':1' → 0':s':1'
true' :: true':false'
p' :: 0':s':1' → 0':s':1'
false' :: true':false'
times' :: 0':s':1' → 0':s':1' → 0':s':1'
timesIter' :: 0':s':1' → 0':s':1' → 0':s':1' → 0':s':1' → 0':s':1'
0' :: 0':s':1'
ifTimes' :: true':false' → 0':s':1' → 0':s':1' → 0':s':1' → 0':s':1' → 0':s':1'
ge' :: 0':s':1' → 0':s':1' → true':false'
s' :: 0':s':1' → 0':s':1'
f0' :: 0':s':1' → 0':s':1' → 0':s':1' → d':c'
f1' :: 0':s':1' → 0':s':1' → 0':s':1' → d':c'
f2' :: 0':s':1' → 0':s':1' → 0':s':1' → d':c'
1' :: 0':s':1'
d' :: d':c'
c' :: d':c'
_hole_0':s':1'1 :: 0':s':1'
_hole_true':false'2 :: true':false'
_hole_d':c'3 :: d':c'
_gen_0':s':1'4 :: Nat → 0':s':1'
Heuristically decided to analyse the following defined symbols:
plus', isZero', inc', p', timesIter', ge', f0', f1', f2'
They will be analysed ascendingly in the following order:
isZero' < plus'
inc' < plus'
p' < plus'
plus' < timesIter'
inc' < timesIter'
ge' < timesIter'
f0' = f1'
f0' = f2'
f1' = f2'
Rules:
plus'(x, y) → ifPlus'(isZero'(x), x, inc'(y))
ifPlus'(true', x, y) → p'(y)
ifPlus'(false', x, y) → plus'(p'(x), y)
times'(x, y) → timesIter'(0', x, y, 0')
timesIter'(i, x, y, z) → ifTimes'(ge'(i, x), i, x, y, z)
ifTimes'(true', i, x, y, z) → z
ifTimes'(false', i, x, y, z) → timesIter'(inc'(i), x, y, plus'(z, y))
isZero'(0') → true'
isZero'(s'(0')) → false'
isZero'(s'(s'(x))) → isZero'(s'(x))
inc'(0') → s'(0')
inc'(s'(x)) → s'(inc'(x))
inc'(x) → s'(x)
p'(0') → 0'
p'(s'(x)) → x
p'(s'(s'(x))) → s'(p'(s'(x)))
ge'(x, 0') → true'
ge'(0', s'(y)) → false'
ge'(s'(x), s'(y)) → ge'(x, y)
f0'(0', y, x) → f1'(x, y, x)
f1'(x, y, z) → f2'(x, y, z)
f2'(x, 1', z) → f0'(x, z, z)
f0'(x, y, z) → d'
f1'(x, y, z) → c'
Types:
plus' :: 0':s':1' → 0':s':1' → 0':s':1'
ifPlus' :: true':false' → 0':s':1' → 0':s':1' → 0':s':1'
isZero' :: 0':s':1' → true':false'
inc' :: 0':s':1' → 0':s':1'
true' :: true':false'
p' :: 0':s':1' → 0':s':1'
false' :: true':false'
times' :: 0':s':1' → 0':s':1' → 0':s':1'
timesIter' :: 0':s':1' → 0':s':1' → 0':s':1' → 0':s':1' → 0':s':1'
0' :: 0':s':1'
ifTimes' :: true':false' → 0':s':1' → 0':s':1' → 0':s':1' → 0':s':1' → 0':s':1'
ge' :: 0':s':1' → 0':s':1' → true':false'
s' :: 0':s':1' → 0':s':1'
f0' :: 0':s':1' → 0':s':1' → 0':s':1' → d':c'
f1' :: 0':s':1' → 0':s':1' → 0':s':1' → d':c'
f2' :: 0':s':1' → 0':s':1' → 0':s':1' → d':c'
1' :: 0':s':1'
d' :: d':c'
c' :: d':c'
_hole_0':s':1'1 :: 0':s':1'
_hole_true':false'2 :: true':false'
_hole_d':c'3 :: d':c'
_gen_0':s':1'4 :: Nat → 0':s':1'
Generator Equations:
_gen_0':s':1'4(0) ⇔ 0'
_gen_0':s':1'4(+(x, 1)) ⇔ s'(_gen_0':s':1'4(x))
The following defined symbols remain to be analysed:
isZero', plus', inc', p', timesIter', ge', f0', f1', f2'
They will be analysed ascendingly in the following order:
isZero' < plus'
inc' < plus'
p' < plus'
plus' < timesIter'
inc' < timesIter'
ge' < timesIter'
f0' = f1'
f0' = f2'
f1' = f2'
Proved the following rewrite lemma:
isZero'(_gen_0':s':1'4(+(1, _n6))) → false', rt ∈ Ω(1 + n6)
Induction Base:
isZero'(_gen_0':s':1'4(+(1, 0))) →RΩ(1)
false'
Induction Step:
isZero'(_gen_0':s':1'4(+(1, +(_$n7, 1)))) →RΩ(1)
isZero'(s'(_gen_0':s':1'4(_$n7))) →IH
false'
We have rt ∈ Ω(n) and sz ∈ O(n). Thus, we have ircR ∈ Ω(n).
Rules:
plus'(x, y) → ifPlus'(isZero'(x), x, inc'(y))
ifPlus'(true', x, y) → p'(y)
ifPlus'(false', x, y) → plus'(p'(x), y)
times'(x, y) → timesIter'(0', x, y, 0')
timesIter'(i, x, y, z) → ifTimes'(ge'(i, x), i, x, y, z)
ifTimes'(true', i, x, y, z) → z
ifTimes'(false', i, x, y, z) → timesIter'(inc'(i), x, y, plus'(z, y))
isZero'(0') → true'
isZero'(s'(0')) → false'
isZero'(s'(s'(x))) → isZero'(s'(x))
inc'(0') → s'(0')
inc'(s'(x)) → s'(inc'(x))
inc'(x) → s'(x)
p'(0') → 0'
p'(s'(x)) → x
p'(s'(s'(x))) → s'(p'(s'(x)))
ge'(x, 0') → true'
ge'(0', s'(y)) → false'
ge'(s'(x), s'(y)) → ge'(x, y)
f0'(0', y, x) → f1'(x, y, x)
f1'(x, y, z) → f2'(x, y, z)
f2'(x, 1', z) → f0'(x, z, z)
f0'(x, y, z) → d'
f1'(x, y, z) → c'
Types:
plus' :: 0':s':1' → 0':s':1' → 0':s':1'
ifPlus' :: true':false' → 0':s':1' → 0':s':1' → 0':s':1'
isZero' :: 0':s':1' → true':false'
inc' :: 0':s':1' → 0':s':1'
true' :: true':false'
p' :: 0':s':1' → 0':s':1'
false' :: true':false'
times' :: 0':s':1' → 0':s':1' → 0':s':1'
timesIter' :: 0':s':1' → 0':s':1' → 0':s':1' → 0':s':1' → 0':s':1'
0' :: 0':s':1'
ifTimes' :: true':false' → 0':s':1' → 0':s':1' → 0':s':1' → 0':s':1' → 0':s':1'
ge' :: 0':s':1' → 0':s':1' → true':false'
s' :: 0':s':1' → 0':s':1'
f0' :: 0':s':1' → 0':s':1' → 0':s':1' → d':c'
f1' :: 0':s':1' → 0':s':1' → 0':s':1' → d':c'
f2' :: 0':s':1' → 0':s':1' → 0':s':1' → d':c'
1' :: 0':s':1'
d' :: d':c'
c' :: d':c'
_hole_0':s':1'1 :: 0':s':1'
_hole_true':false'2 :: true':false'
_hole_d':c'3 :: d':c'
_gen_0':s':1'4 :: Nat → 0':s':1'
Lemmas:
isZero'(_gen_0':s':1'4(+(1, _n6))) → false', rt ∈ Ω(1 + n6)
Generator Equations:
_gen_0':s':1'4(0) ⇔ 0'
_gen_0':s':1'4(+(x, 1)) ⇔ s'(_gen_0':s':1'4(x))
The following defined symbols remain to be analysed:
inc', plus', p', timesIter', ge', f0', f1', f2'
They will be analysed ascendingly in the following order:
inc' < plus'
p' < plus'
plus' < timesIter'
inc' < timesIter'
ge' < timesIter'
f0' = f1'
f0' = f2'
f1' = f2'
Proved the following rewrite lemma:
inc'(_gen_0':s':1'4(_n923)) → _gen_0':s':1'4(+(1, _n923)), rt ∈ Ω(1 + n923)
Induction Base:
inc'(_gen_0':s':1'4(0)) →RΩ(1)
s'(0')
Induction Step:
inc'(_gen_0':s':1'4(+(_$n924, 1))) →RΩ(1)
s'(inc'(_gen_0':s':1'4(_$n924))) →IH
s'(_gen_0':s':1'4(+(1, _$n924)))
We have rt ∈ Ω(n) and sz ∈ O(n). Thus, we have ircR ∈ Ω(n).
Rules:
plus'(x, y) → ifPlus'(isZero'(x), x, inc'(y))
ifPlus'(true', x, y) → p'(y)
ifPlus'(false', x, y) → plus'(p'(x), y)
times'(x, y) → timesIter'(0', x, y, 0')
timesIter'(i, x, y, z) → ifTimes'(ge'(i, x), i, x, y, z)
ifTimes'(true', i, x, y, z) → z
ifTimes'(false', i, x, y, z) → timesIter'(inc'(i), x, y, plus'(z, y))
isZero'(0') → true'
isZero'(s'(0')) → false'
isZero'(s'(s'(x))) → isZero'(s'(x))
inc'(0') → s'(0')
inc'(s'(x)) → s'(inc'(x))
inc'(x) → s'(x)
p'(0') → 0'
p'(s'(x)) → x
p'(s'(s'(x))) → s'(p'(s'(x)))
ge'(x, 0') → true'
ge'(0', s'(y)) → false'
ge'(s'(x), s'(y)) → ge'(x, y)
f0'(0', y, x) → f1'(x, y, x)
f1'(x, y, z) → f2'(x, y, z)
f2'(x, 1', z) → f0'(x, z, z)
f0'(x, y, z) → d'
f1'(x, y, z) → c'
Types:
plus' :: 0':s':1' → 0':s':1' → 0':s':1'
ifPlus' :: true':false' → 0':s':1' → 0':s':1' → 0':s':1'
isZero' :: 0':s':1' → true':false'
inc' :: 0':s':1' → 0':s':1'
true' :: true':false'
p' :: 0':s':1' → 0':s':1'
false' :: true':false'
times' :: 0':s':1' → 0':s':1' → 0':s':1'
timesIter' :: 0':s':1' → 0':s':1' → 0':s':1' → 0':s':1' → 0':s':1'
0' :: 0':s':1'
ifTimes' :: true':false' → 0':s':1' → 0':s':1' → 0':s':1' → 0':s':1' → 0':s':1'
ge' :: 0':s':1' → 0':s':1' → true':false'
s' :: 0':s':1' → 0':s':1'
f0' :: 0':s':1' → 0':s':1' → 0':s':1' → d':c'
f1' :: 0':s':1' → 0':s':1' → 0':s':1' → d':c'
f2' :: 0':s':1' → 0':s':1' → 0':s':1' → d':c'
1' :: 0':s':1'
d' :: d':c'
c' :: d':c'
_hole_0':s':1'1 :: 0':s':1'
_hole_true':false'2 :: true':false'
_hole_d':c'3 :: d':c'
_gen_0':s':1'4 :: Nat → 0':s':1'
Lemmas:
isZero'(_gen_0':s':1'4(+(1, _n6))) → false', rt ∈ Ω(1 + n6)
inc'(_gen_0':s':1'4(_n923)) → _gen_0':s':1'4(+(1, _n923)), rt ∈ Ω(1 + n923)
Generator Equations:
_gen_0':s':1'4(0) ⇔ 0'
_gen_0':s':1'4(+(x, 1)) ⇔ s'(_gen_0':s':1'4(x))
The following defined symbols remain to be analysed:
p', plus', timesIter', ge', f0', f1', f2'
They will be analysed ascendingly in the following order:
p' < plus'
plus' < timesIter'
ge' < timesIter'
f0' = f1'
f0' = f2'
f1' = f2'
Proved the following rewrite lemma:
p'(_gen_0':s':1'4(+(2, _n3445))) → _*5, rt ∈ Ω(n3445)
Induction Base:
p'(_gen_0':s':1'4(+(2, 0)))
Induction Step:
p'(_gen_0':s':1'4(+(2, +(_$n3446, 1)))) →RΩ(1)
s'(p'(s'(_gen_0':s':1'4(+(1, _$n3446))))) →IH
s'(_*5)
We have rt ∈ Ω(n) and sz ∈ O(n). Thus, we have ircR ∈ Ω(n).
Rules:
plus'(x, y) → ifPlus'(isZero'(x), x, inc'(y))
ifPlus'(true', x, y) → p'(y)
ifPlus'(false', x, y) → plus'(p'(x), y)
times'(x, y) → timesIter'(0', x, y, 0')
timesIter'(i, x, y, z) → ifTimes'(ge'(i, x), i, x, y, z)
ifTimes'(true', i, x, y, z) → z
ifTimes'(false', i, x, y, z) → timesIter'(inc'(i), x, y, plus'(z, y))
isZero'(0') → true'
isZero'(s'(0')) → false'
isZero'(s'(s'(x))) → isZero'(s'(x))
inc'(0') → s'(0')
inc'(s'(x)) → s'(inc'(x))
inc'(x) → s'(x)
p'(0') → 0'
p'(s'(x)) → x
p'(s'(s'(x))) → s'(p'(s'(x)))
ge'(x, 0') → true'
ge'(0', s'(y)) → false'
ge'(s'(x), s'(y)) → ge'(x, y)
f0'(0', y, x) → f1'(x, y, x)
f1'(x, y, z) → f2'(x, y, z)
f2'(x, 1', z) → f0'(x, z, z)
f0'(x, y, z) → d'
f1'(x, y, z) → c'
Types:
plus' :: 0':s':1' → 0':s':1' → 0':s':1'
ifPlus' :: true':false' → 0':s':1' → 0':s':1' → 0':s':1'
isZero' :: 0':s':1' → true':false'
inc' :: 0':s':1' → 0':s':1'
true' :: true':false'
p' :: 0':s':1' → 0':s':1'
false' :: true':false'
times' :: 0':s':1' → 0':s':1' → 0':s':1'
timesIter' :: 0':s':1' → 0':s':1' → 0':s':1' → 0':s':1' → 0':s':1'
0' :: 0':s':1'
ifTimes' :: true':false' → 0':s':1' → 0':s':1' → 0':s':1' → 0':s':1' → 0':s':1'
ge' :: 0':s':1' → 0':s':1' → true':false'
s' :: 0':s':1' → 0':s':1'
f0' :: 0':s':1' → 0':s':1' → 0':s':1' → d':c'
f1' :: 0':s':1' → 0':s':1' → 0':s':1' → d':c'
f2' :: 0':s':1' → 0':s':1' → 0':s':1' → d':c'
1' :: 0':s':1'
d' :: d':c'
c' :: d':c'
_hole_0':s':1'1 :: 0':s':1'
_hole_true':false'2 :: true':false'
_hole_d':c'3 :: d':c'
_gen_0':s':1'4 :: Nat → 0':s':1'
Lemmas:
isZero'(_gen_0':s':1'4(+(1, _n6))) → false', rt ∈ Ω(1 + n6)
inc'(_gen_0':s':1'4(_n923)) → _gen_0':s':1'4(+(1, _n923)), rt ∈ Ω(1 + n923)
p'(_gen_0':s':1'4(+(2, _n3445))) → _*5, rt ∈ Ω(n3445)
Generator Equations:
_gen_0':s':1'4(0) ⇔ 0'
_gen_0':s':1'4(+(x, 1)) ⇔ s'(_gen_0':s':1'4(x))
The following defined symbols remain to be analysed:
plus', timesIter', ge', f0', f1', f2'
They will be analysed ascendingly in the following order:
plus' < timesIter'
ge' < timesIter'
f0' = f1'
f0' = f2'
f1' = f2'
Could not prove a rewrite lemma for the defined symbol plus'.
Rules:
plus'(x, y) → ifPlus'(isZero'(x), x, inc'(y))
ifPlus'(true', x, y) → p'(y)
ifPlus'(false', x, y) → plus'(p'(x), y)
times'(x, y) → timesIter'(0', x, y, 0')
timesIter'(i, x, y, z) → ifTimes'(ge'(i, x), i, x, y, z)
ifTimes'(true', i, x, y, z) → z
ifTimes'(false', i, x, y, z) → timesIter'(inc'(i), x, y, plus'(z, y))
isZero'(0') → true'
isZero'(s'(0')) → false'
isZero'(s'(s'(x))) → isZero'(s'(x))
inc'(0') → s'(0')
inc'(s'(x)) → s'(inc'(x))
inc'(x) → s'(x)
p'(0') → 0'
p'(s'(x)) → x
p'(s'(s'(x))) → s'(p'(s'(x)))
ge'(x, 0') → true'
ge'(0', s'(y)) → false'
ge'(s'(x), s'(y)) → ge'(x, y)
f0'(0', y, x) → f1'(x, y, x)
f1'(x, y, z) → f2'(x, y, z)
f2'(x, 1', z) → f0'(x, z, z)
f0'(x, y, z) → d'
f1'(x, y, z) → c'
Types:
plus' :: 0':s':1' → 0':s':1' → 0':s':1'
ifPlus' :: true':false' → 0':s':1' → 0':s':1' → 0':s':1'
isZero' :: 0':s':1' → true':false'
inc' :: 0':s':1' → 0':s':1'
true' :: true':false'
p' :: 0':s':1' → 0':s':1'
false' :: true':false'
times' :: 0':s':1' → 0':s':1' → 0':s':1'
timesIter' :: 0':s':1' → 0':s':1' → 0':s':1' → 0':s':1' → 0':s':1'
0' :: 0':s':1'
ifTimes' :: true':false' → 0':s':1' → 0':s':1' → 0':s':1' → 0':s':1' → 0':s':1'
ge' :: 0':s':1' → 0':s':1' → true':false'
s' :: 0':s':1' → 0':s':1'
f0' :: 0':s':1' → 0':s':1' → 0':s':1' → d':c'
f1' :: 0':s':1' → 0':s':1' → 0':s':1' → d':c'
f2' :: 0':s':1' → 0':s':1' → 0':s':1' → d':c'
1' :: 0':s':1'
d' :: d':c'
c' :: d':c'
_hole_0':s':1'1 :: 0':s':1'
_hole_true':false'2 :: true':false'
_hole_d':c'3 :: d':c'
_gen_0':s':1'4 :: Nat → 0':s':1'
Lemmas:
isZero'(_gen_0':s':1'4(+(1, _n6))) → false', rt ∈ Ω(1 + n6)
inc'(_gen_0':s':1'4(_n923)) → _gen_0':s':1'4(+(1, _n923)), rt ∈ Ω(1 + n923)
p'(_gen_0':s':1'4(+(2, _n3445))) → _*5, rt ∈ Ω(n3445)
Generator Equations:
_gen_0':s':1'4(0) ⇔ 0'
_gen_0':s':1'4(+(x, 1)) ⇔ s'(_gen_0':s':1'4(x))
The following defined symbols remain to be analysed:
ge', timesIter', f0', f1', f2'
They will be analysed ascendingly in the following order:
ge' < timesIter'
f0' = f1'
f0' = f2'
f1' = f2'
Proved the following rewrite lemma:
ge'(_gen_0':s':1'4(_n6479), _gen_0':s':1'4(_n6479)) → true', rt ∈ Ω(1 + n6479)
Induction Base:
ge'(_gen_0':s':1'4(0), _gen_0':s':1'4(0)) →RΩ(1)
true'
Induction Step:
ge'(_gen_0':s':1'4(+(_$n6480, 1)), _gen_0':s':1'4(+(_$n6480, 1))) →RΩ(1)
ge'(_gen_0':s':1'4(_$n6480), _gen_0':s':1'4(_$n6480)) →IH
true'
We have rt ∈ Ω(n) and sz ∈ O(n). Thus, we have ircR ∈ Ω(n).
Rules:
plus'(x, y) → ifPlus'(isZero'(x), x, inc'(y))
ifPlus'(true', x, y) → p'(y)
ifPlus'(false', x, y) → plus'(p'(x), y)
times'(x, y) → timesIter'(0', x, y, 0')
timesIter'(i, x, y, z) → ifTimes'(ge'(i, x), i, x, y, z)
ifTimes'(true', i, x, y, z) → z
ifTimes'(false', i, x, y, z) → timesIter'(inc'(i), x, y, plus'(z, y))
isZero'(0') → true'
isZero'(s'(0')) → false'
isZero'(s'(s'(x))) → isZero'(s'(x))
inc'(0') → s'(0')
inc'(s'(x)) → s'(inc'(x))
inc'(x) → s'(x)
p'(0') → 0'
p'(s'(x)) → x
p'(s'(s'(x))) → s'(p'(s'(x)))
ge'(x, 0') → true'
ge'(0', s'(y)) → false'
ge'(s'(x), s'(y)) → ge'(x, y)
f0'(0', y, x) → f1'(x, y, x)
f1'(x, y, z) → f2'(x, y, z)
f2'(x, 1', z) → f0'(x, z, z)
f0'(x, y, z) → d'
f1'(x, y, z) → c'
Types:
plus' :: 0':s':1' → 0':s':1' → 0':s':1'
ifPlus' :: true':false' → 0':s':1' → 0':s':1' → 0':s':1'
isZero' :: 0':s':1' → true':false'
inc' :: 0':s':1' → 0':s':1'
true' :: true':false'
p' :: 0':s':1' → 0':s':1'
false' :: true':false'
times' :: 0':s':1' → 0':s':1' → 0':s':1'
timesIter' :: 0':s':1' → 0':s':1' → 0':s':1' → 0':s':1' → 0':s':1'
0' :: 0':s':1'
ifTimes' :: true':false' → 0':s':1' → 0':s':1' → 0':s':1' → 0':s':1' → 0':s':1'
ge' :: 0':s':1' → 0':s':1' → true':false'
s' :: 0':s':1' → 0':s':1'
f0' :: 0':s':1' → 0':s':1' → 0':s':1' → d':c'
f1' :: 0':s':1' → 0':s':1' → 0':s':1' → d':c'
f2' :: 0':s':1' → 0':s':1' → 0':s':1' → d':c'
1' :: 0':s':1'
d' :: d':c'
c' :: d':c'
_hole_0':s':1'1 :: 0':s':1'
_hole_true':false'2 :: true':false'
_hole_d':c'3 :: d':c'
_gen_0':s':1'4 :: Nat → 0':s':1'
Lemmas:
isZero'(_gen_0':s':1'4(+(1, _n6))) → false', rt ∈ Ω(1 + n6)
inc'(_gen_0':s':1'4(_n923)) → _gen_0':s':1'4(+(1, _n923)), rt ∈ Ω(1 + n923)
p'(_gen_0':s':1'4(+(2, _n3445))) → _*5, rt ∈ Ω(n3445)
ge'(_gen_0':s':1'4(_n6479), _gen_0':s':1'4(_n6479)) → true', rt ∈ Ω(1 + n6479)
Generator Equations:
_gen_0':s':1'4(0) ⇔ 0'
_gen_0':s':1'4(+(x, 1)) ⇔ s'(_gen_0':s':1'4(x))
The following defined symbols remain to be analysed:
timesIter', f0', f1', f2'
They will be analysed ascendingly in the following order:
f0' = f1'
f0' = f2'
f1' = f2'
Could not prove a rewrite lemma for the defined symbol timesIter'.
Rules:
plus'(x, y) → ifPlus'(isZero'(x), x, inc'(y))
ifPlus'(true', x, y) → p'(y)
ifPlus'(false', x, y) → plus'(p'(x), y)
times'(x, y) → timesIter'(0', x, y, 0')
timesIter'(i, x, y, z) → ifTimes'(ge'(i, x), i, x, y, z)
ifTimes'(true', i, x, y, z) → z
ifTimes'(false', i, x, y, z) → timesIter'(inc'(i), x, y, plus'(z, y))
isZero'(0') → true'
isZero'(s'(0')) → false'
isZero'(s'(s'(x))) → isZero'(s'(x))
inc'(0') → s'(0')
inc'(s'(x)) → s'(inc'(x))
inc'(x) → s'(x)
p'(0') → 0'
p'(s'(x)) → x
p'(s'(s'(x))) → s'(p'(s'(x)))
ge'(x, 0') → true'
ge'(0', s'(y)) → false'
ge'(s'(x), s'(y)) → ge'(x, y)
f0'(0', y, x) → f1'(x, y, x)
f1'(x, y, z) → f2'(x, y, z)
f2'(x, 1', z) → f0'(x, z, z)
f0'(x, y, z) → d'
f1'(x, y, z) → c'
Types:
plus' :: 0':s':1' → 0':s':1' → 0':s':1'
ifPlus' :: true':false' → 0':s':1' → 0':s':1' → 0':s':1'
isZero' :: 0':s':1' → true':false'
inc' :: 0':s':1' → 0':s':1'
true' :: true':false'
p' :: 0':s':1' → 0':s':1'
false' :: true':false'
times' :: 0':s':1' → 0':s':1' → 0':s':1'
timesIter' :: 0':s':1' → 0':s':1' → 0':s':1' → 0':s':1' → 0':s':1'
0' :: 0':s':1'
ifTimes' :: true':false' → 0':s':1' → 0':s':1' → 0':s':1' → 0':s':1' → 0':s':1'
ge' :: 0':s':1' → 0':s':1' → true':false'
s' :: 0':s':1' → 0':s':1'
f0' :: 0':s':1' → 0':s':1' → 0':s':1' → d':c'
f1' :: 0':s':1' → 0':s':1' → 0':s':1' → d':c'
f2' :: 0':s':1' → 0':s':1' → 0':s':1' → d':c'
1' :: 0':s':1'
d' :: d':c'
c' :: d':c'
_hole_0':s':1'1 :: 0':s':1'
_hole_true':false'2 :: true':false'
_hole_d':c'3 :: d':c'
_gen_0':s':1'4 :: Nat → 0':s':1'
Lemmas:
isZero'(_gen_0':s':1'4(+(1, _n6))) → false', rt ∈ Ω(1 + n6)
inc'(_gen_0':s':1'4(_n923)) → _gen_0':s':1'4(+(1, _n923)), rt ∈ Ω(1 + n923)
p'(_gen_0':s':1'4(+(2, _n3445))) → _*5, rt ∈ Ω(n3445)
ge'(_gen_0':s':1'4(_n6479), _gen_0':s':1'4(_n6479)) → true', rt ∈ Ω(1 + n6479)
Generator Equations:
_gen_0':s':1'4(0) ⇔ 0'
_gen_0':s':1'4(+(x, 1)) ⇔ s'(_gen_0':s':1'4(x))
The following defined symbols remain to be analysed:
f1', f0', f2'
They will be analysed ascendingly in the following order:
f0' = f1'
f0' = f2'
f1' = f2'
Could not prove a rewrite lemma for the defined symbol f1'.
Rules:
plus'(x, y) → ifPlus'(isZero'(x), x, inc'(y))
ifPlus'(true', x, y) → p'(y)
ifPlus'(false', x, y) → plus'(p'(x), y)
times'(x, y) → timesIter'(0', x, y, 0')
timesIter'(i, x, y, z) → ifTimes'(ge'(i, x), i, x, y, z)
ifTimes'(true', i, x, y, z) → z
ifTimes'(false', i, x, y, z) → timesIter'(inc'(i), x, y, plus'(z, y))
isZero'(0') → true'
isZero'(s'(0')) → false'
isZero'(s'(s'(x))) → isZero'(s'(x))
inc'(0') → s'(0')
inc'(s'(x)) → s'(inc'(x))
inc'(x) → s'(x)
p'(0') → 0'
p'(s'(x)) → x
p'(s'(s'(x))) → s'(p'(s'(x)))
ge'(x, 0') → true'
ge'(0', s'(y)) → false'
ge'(s'(x), s'(y)) → ge'(x, y)
f0'(0', y, x) → f1'(x, y, x)
f1'(x, y, z) → f2'(x, y, z)
f2'(x, 1', z) → f0'(x, z, z)
f0'(x, y, z) → d'
f1'(x, y, z) → c'
Types:
plus' :: 0':s':1' → 0':s':1' → 0':s':1'
ifPlus' :: true':false' → 0':s':1' → 0':s':1' → 0':s':1'
isZero' :: 0':s':1' → true':false'
inc' :: 0':s':1' → 0':s':1'
true' :: true':false'
p' :: 0':s':1' → 0':s':1'
false' :: true':false'
times' :: 0':s':1' → 0':s':1' → 0':s':1'
timesIter' :: 0':s':1' → 0':s':1' → 0':s':1' → 0':s':1' → 0':s':1'
0' :: 0':s':1'
ifTimes' :: true':false' → 0':s':1' → 0':s':1' → 0':s':1' → 0':s':1' → 0':s':1'
ge' :: 0':s':1' → 0':s':1' → true':false'
s' :: 0':s':1' → 0':s':1'
f0' :: 0':s':1' → 0':s':1' → 0':s':1' → d':c'
f1' :: 0':s':1' → 0':s':1' → 0':s':1' → d':c'
f2' :: 0':s':1' → 0':s':1' → 0':s':1' → d':c'
1' :: 0':s':1'
d' :: d':c'
c' :: d':c'
_hole_0':s':1'1 :: 0':s':1'
_hole_true':false'2 :: true':false'
_hole_d':c'3 :: d':c'
_gen_0':s':1'4 :: Nat → 0':s':1'
Lemmas:
isZero'(_gen_0':s':1'4(+(1, _n6))) → false', rt ∈ Ω(1 + n6)
inc'(_gen_0':s':1'4(_n923)) → _gen_0':s':1'4(+(1, _n923)), rt ∈ Ω(1 + n923)
p'(_gen_0':s':1'4(+(2, _n3445))) → _*5, rt ∈ Ω(n3445)
ge'(_gen_0':s':1'4(_n6479), _gen_0':s':1'4(_n6479)) → true', rt ∈ Ω(1 + n6479)
Generator Equations:
_gen_0':s':1'4(0) ⇔ 0'
_gen_0':s':1'4(+(x, 1)) ⇔ s'(_gen_0':s':1'4(x))
The following defined symbols remain to be analysed:
f2', f0'
They will be analysed ascendingly in the following order:
f0' = f1'
f0' = f2'
f1' = f2'
Could not prove a rewrite lemma for the defined symbol f2'.
Rules:
plus'(x, y) → ifPlus'(isZero'(x), x, inc'(y))
ifPlus'(true', x, y) → p'(y)
ifPlus'(false', x, y) → plus'(p'(x), y)
times'(x, y) → timesIter'(0', x, y, 0')
timesIter'(i, x, y, z) → ifTimes'(ge'(i, x), i, x, y, z)
ifTimes'(true', i, x, y, z) → z
ifTimes'(false', i, x, y, z) → timesIter'(inc'(i), x, y, plus'(z, y))
isZero'(0') → true'
isZero'(s'(0')) → false'
isZero'(s'(s'(x))) → isZero'(s'(x))
inc'(0') → s'(0')
inc'(s'(x)) → s'(inc'(x))
inc'(x) → s'(x)
p'(0') → 0'
p'(s'(x)) → x
p'(s'(s'(x))) → s'(p'(s'(x)))
ge'(x, 0') → true'
ge'(0', s'(y)) → false'
ge'(s'(x), s'(y)) → ge'(x, y)
f0'(0', y, x) → f1'(x, y, x)
f1'(x, y, z) → f2'(x, y, z)
f2'(x, 1', z) → f0'(x, z, z)
f0'(x, y, z) → d'
f1'(x, y, z) → c'
Types:
plus' :: 0':s':1' → 0':s':1' → 0':s':1'
ifPlus' :: true':false' → 0':s':1' → 0':s':1' → 0':s':1'
isZero' :: 0':s':1' → true':false'
inc' :: 0':s':1' → 0':s':1'
true' :: true':false'
p' :: 0':s':1' → 0':s':1'
false' :: true':false'
times' :: 0':s':1' → 0':s':1' → 0':s':1'
timesIter' :: 0':s':1' → 0':s':1' → 0':s':1' → 0':s':1' → 0':s':1'
0' :: 0':s':1'
ifTimes' :: true':false' → 0':s':1' → 0':s':1' → 0':s':1' → 0':s':1' → 0':s':1'
ge' :: 0':s':1' → 0':s':1' → true':false'
s' :: 0':s':1' → 0':s':1'
f0' :: 0':s':1' → 0':s':1' → 0':s':1' → d':c'
f1' :: 0':s':1' → 0':s':1' → 0':s':1' → d':c'
f2' :: 0':s':1' → 0':s':1' → 0':s':1' → d':c'
1' :: 0':s':1'
d' :: d':c'
c' :: d':c'
_hole_0':s':1'1 :: 0':s':1'
_hole_true':false'2 :: true':false'
_hole_d':c'3 :: d':c'
_gen_0':s':1'4 :: Nat → 0':s':1'
Lemmas:
isZero'(_gen_0':s':1'4(+(1, _n6))) → false', rt ∈ Ω(1 + n6)
inc'(_gen_0':s':1'4(_n923)) → _gen_0':s':1'4(+(1, _n923)), rt ∈ Ω(1 + n923)
p'(_gen_0':s':1'4(+(2, _n3445))) → _*5, rt ∈ Ω(n3445)
ge'(_gen_0':s':1'4(_n6479), _gen_0':s':1'4(_n6479)) → true', rt ∈ Ω(1 + n6479)
Generator Equations:
_gen_0':s':1'4(0) ⇔ 0'
_gen_0':s':1'4(+(x, 1)) ⇔ s'(_gen_0':s':1'4(x))
The following defined symbols remain to be analysed:
f0'
They will be analysed ascendingly in the following order:
f0' = f1'
f0' = f2'
f1' = f2'
Could not prove a rewrite lemma for the defined symbol f0'.
Rules:
plus'(x, y) → ifPlus'(isZero'(x), x, inc'(y))
ifPlus'(true', x, y) → p'(y)
ifPlus'(false', x, y) → plus'(p'(x), y)
times'(x, y) → timesIter'(0', x, y, 0')
timesIter'(i, x, y, z) → ifTimes'(ge'(i, x), i, x, y, z)
ifTimes'(true', i, x, y, z) → z
ifTimes'(false', i, x, y, z) → timesIter'(inc'(i), x, y, plus'(z, y))
isZero'(0') → true'
isZero'(s'(0')) → false'
isZero'(s'(s'(x))) → isZero'(s'(x))
inc'(0') → s'(0')
inc'(s'(x)) → s'(inc'(x))
inc'(x) → s'(x)
p'(0') → 0'
p'(s'(x)) → x
p'(s'(s'(x))) → s'(p'(s'(x)))
ge'(x, 0') → true'
ge'(0', s'(y)) → false'
ge'(s'(x), s'(y)) → ge'(x, y)
f0'(0', y, x) → f1'(x, y, x)
f1'(x, y, z) → f2'(x, y, z)
f2'(x, 1', z) → f0'(x, z, z)
f0'(x, y, z) → d'
f1'(x, y, z) → c'
Types:
plus' :: 0':s':1' → 0':s':1' → 0':s':1'
ifPlus' :: true':false' → 0':s':1' → 0':s':1' → 0':s':1'
isZero' :: 0':s':1' → true':false'
inc' :: 0':s':1' → 0':s':1'
true' :: true':false'
p' :: 0':s':1' → 0':s':1'
false' :: true':false'
times' :: 0':s':1' → 0':s':1' → 0':s':1'
timesIter' :: 0':s':1' → 0':s':1' → 0':s':1' → 0':s':1' → 0':s':1'
0' :: 0':s':1'
ifTimes' :: true':false' → 0':s':1' → 0':s':1' → 0':s':1' → 0':s':1' → 0':s':1'
ge' :: 0':s':1' → 0':s':1' → true':false'
s' :: 0':s':1' → 0':s':1'
f0' :: 0':s':1' → 0':s':1' → 0':s':1' → d':c'
f1' :: 0':s':1' → 0':s':1' → 0':s':1' → d':c'
f2' :: 0':s':1' → 0':s':1' → 0':s':1' → d':c'
1' :: 0':s':1'
d' :: d':c'
c' :: d':c'
_hole_0':s':1'1 :: 0':s':1'
_hole_true':false'2 :: true':false'
_hole_d':c'3 :: d':c'
_gen_0':s':1'4 :: Nat → 0':s':1'
Lemmas:
isZero'(_gen_0':s':1'4(+(1, _n6))) → false', rt ∈ Ω(1 + n6)
inc'(_gen_0':s':1'4(_n923)) → _gen_0':s':1'4(+(1, _n923)), rt ∈ Ω(1 + n923)
p'(_gen_0':s':1'4(+(2, _n3445))) → _*5, rt ∈ Ω(n3445)
ge'(_gen_0':s':1'4(_n6479), _gen_0':s':1'4(_n6479)) → true', rt ∈ Ω(1 + n6479)
Generator Equations:
_gen_0':s':1'4(0) ⇔ 0'
_gen_0':s':1'4(+(x, 1)) ⇔ s'(_gen_0':s':1'4(x))
No more defined symbols left to analyse.
The lowerbound Ω(n) was proven with the following lemma:
isZero'(_gen_0':s':1'4(+(1, _n6))) → false', rt ∈ Ω(1 + n6)