plus(x, y) → plusIter(x, y, 0)
plusIter(x, y, z) → ifPlus(le(x, z), x, y, z)
ifPlus(true, x, y, z) → y
ifPlus(false, x, y, z) → plusIter(x, s(y), s(z))
le(s(x), 0) → false
le(0, y) → true
le(s(x), s(y)) → le(x, y)
sum(xs) → sumIter(xs, 0)
sumIter(xs, x) → ifSum(isempty(xs), xs, x, plus(x, head(xs)))
ifSum(true, xs, x, y) → x
ifSum(false, xs, x, y) → sumIter(tail(xs), y)
isempty(nil) → true
isempty(cons(x, xs)) → false
head(nil) → error
head(cons(x, xs)) → x
tail(nil) → nil
tail(cons(x, xs)) → xs
a → b
a → c
Renamed function symbols to avoid clashes with predefined symbol.
Runtime Complexity TRS:
The TRS R consists of the following rules:
plus'(x, y) → plusIter'(x, y, 0')
plusIter'(x, y, z) → ifPlus'(le'(x, z), x, y, z)
ifPlus'(true', x, y, z) → y
ifPlus'(false', x, y, z) → plusIter'(x, s'(y), s'(z))
le'(s'(x), 0') → false'
le'(0', y) → true'
le'(s'(x), s'(y)) → le'(x, y)
sum'(xs) → sumIter'(xs, 0')
sumIter'(xs, x) → ifSum'(isempty'(xs), xs, x, plus'(x, head'(xs)))
ifSum'(true', xs, x, y) → x
ifSum'(false', xs, x, y) → sumIter'(tail'(xs), y)
isempty'(nil') → true'
isempty'(cons'(x, xs)) → false'
head'(nil') → error'
head'(cons'(x, xs)) → x
tail'(nil') → nil'
tail'(cons'(x, xs)) → xs
a' → b'
a' → c'
Infered types.
Rules:
plus'(x, y) → plusIter'(x, y, 0')
plusIter'(x, y, z) → ifPlus'(le'(x, z), x, y, z)
ifPlus'(true', x, y, z) → y
ifPlus'(false', x, y, z) → plusIter'(x, s'(y), s'(z))
le'(s'(x), 0') → false'
le'(0', y) → true'
le'(s'(x), s'(y)) → le'(x, y)
sum'(xs) → sumIter'(xs, 0')
sumIter'(xs, x) → ifSum'(isempty'(xs), xs, x, plus'(x, head'(xs)))
ifSum'(true', xs, x, y) → x
ifSum'(false', xs, x, y) → sumIter'(tail'(xs), y)
isempty'(nil') → true'
isempty'(cons'(x, xs)) → false'
head'(nil') → error'
head'(cons'(x, xs)) → x
tail'(nil') → nil'
tail'(cons'(x, xs)) → xs
a' → b'
a' → c'
Types:
plus' :: 0':s':error' → 0':s':error' → 0':s':error'
plusIter' :: 0':s':error' → 0':s':error' → 0':s':error' → 0':s':error'
0' :: 0':s':error'
ifPlus' :: true':false' → 0':s':error' → 0':s':error' → 0':s':error' → 0':s':error'
le' :: 0':s':error' → 0':s':error' → true':false'
true' :: true':false'
false' :: true':false'
s' :: 0':s':error' → 0':s':error'
sum' :: nil':cons' → 0':s':error'
sumIter' :: nil':cons' → 0':s':error' → 0':s':error'
ifSum' :: true':false' → nil':cons' → 0':s':error' → 0':s':error' → 0':s':error'
isempty' :: nil':cons' → true':false'
head' :: nil':cons' → 0':s':error'
tail' :: nil':cons' → nil':cons'
nil' :: nil':cons'
cons' :: 0':s':error' → nil':cons' → nil':cons'
error' :: 0':s':error'
a' :: b':c'
b' :: b':c'
c' :: b':c'
_hole_0':s':error'1 :: 0':s':error'
_hole_true':false'2 :: true':false'
_hole_nil':cons'3 :: nil':cons'
_hole_b':c'4 :: b':c'
_gen_0':s':error'5 :: Nat → 0':s':error'
_gen_nil':cons'6 :: Nat → nil':cons'
Heuristically decided to analyse the following defined symbols:
plusIter', le', sumIter'
They will be analysed ascendingly in the following order:
le' < plusIter'
Rules:
plus'(x, y) → plusIter'(x, y, 0')
plusIter'(x, y, z) → ifPlus'(le'(x, z), x, y, z)
ifPlus'(true', x, y, z) → y
ifPlus'(false', x, y, z) → plusIter'(x, s'(y), s'(z))
le'(s'(x), 0') → false'
le'(0', y) → true'
le'(s'(x), s'(y)) → le'(x, y)
sum'(xs) → sumIter'(xs, 0')
sumIter'(xs, x) → ifSum'(isempty'(xs), xs, x, plus'(x, head'(xs)))
ifSum'(true', xs, x, y) → x
ifSum'(false', xs, x, y) → sumIter'(tail'(xs), y)
isempty'(nil') → true'
isempty'(cons'(x, xs)) → false'
head'(nil') → error'
head'(cons'(x, xs)) → x
tail'(nil') → nil'
tail'(cons'(x, xs)) → xs
a' → b'
a' → c'
Types:
plus' :: 0':s':error' → 0':s':error' → 0':s':error'
plusIter' :: 0':s':error' → 0':s':error' → 0':s':error' → 0':s':error'
0' :: 0':s':error'
ifPlus' :: true':false' → 0':s':error' → 0':s':error' → 0':s':error' → 0':s':error'
le' :: 0':s':error' → 0':s':error' → true':false'
true' :: true':false'
false' :: true':false'
s' :: 0':s':error' → 0':s':error'
sum' :: nil':cons' → 0':s':error'
sumIter' :: nil':cons' → 0':s':error' → 0':s':error'
ifSum' :: true':false' → nil':cons' → 0':s':error' → 0':s':error' → 0':s':error'
isempty' :: nil':cons' → true':false'
head' :: nil':cons' → 0':s':error'
tail' :: nil':cons' → nil':cons'
nil' :: nil':cons'
cons' :: 0':s':error' → nil':cons' → nil':cons'
error' :: 0':s':error'
a' :: b':c'
b' :: b':c'
c' :: b':c'
_hole_0':s':error'1 :: 0':s':error'
_hole_true':false'2 :: true':false'
_hole_nil':cons'3 :: nil':cons'
_hole_b':c'4 :: b':c'
_gen_0':s':error'5 :: Nat → 0':s':error'
_gen_nil':cons'6 :: Nat → nil':cons'
Generator Equations:
_gen_0':s':error'5(0) ⇔ 0'
_gen_0':s':error'5(+(x, 1)) ⇔ s'(_gen_0':s':error'5(x))
_gen_nil':cons'6(0) ⇔ nil'
_gen_nil':cons'6(+(x, 1)) ⇔ cons'(0', _gen_nil':cons'6(x))
The following defined symbols remain to be analysed:
le', plusIter', sumIter'
They will be analysed ascendingly in the following order:
le' < plusIter'
Proved the following rewrite lemma:
le'(_gen_0':s':error'5(+(1, _n8)), _gen_0':s':error'5(_n8)) → false', rt ∈ Ω(1 + n8)
Induction Base:
le'(_gen_0':s':error'5(+(1, 0)), _gen_0':s':error'5(0)) →RΩ(1)
false'
Induction Step:
le'(_gen_0':s':error'5(+(1, +(_$n9, 1))), _gen_0':s':error'5(+(_$n9, 1))) →RΩ(1)
le'(_gen_0':s':error'5(+(1, _$n9)), _gen_0':s':error'5(_$n9)) →IH
false'
We have rt ∈ Ω(n) and sz ∈ O(n). Thus, we have ircR ∈ Ω(n).
Rules:
plus'(x, y) → plusIter'(x, y, 0')
plusIter'(x, y, z) → ifPlus'(le'(x, z), x, y, z)
ifPlus'(true', x, y, z) → y
ifPlus'(false', x, y, z) → plusIter'(x, s'(y), s'(z))
le'(s'(x), 0') → false'
le'(0', y) → true'
le'(s'(x), s'(y)) → le'(x, y)
sum'(xs) → sumIter'(xs, 0')
sumIter'(xs, x) → ifSum'(isempty'(xs), xs, x, plus'(x, head'(xs)))
ifSum'(true', xs, x, y) → x
ifSum'(false', xs, x, y) → sumIter'(tail'(xs), y)
isempty'(nil') → true'
isempty'(cons'(x, xs)) → false'
head'(nil') → error'
head'(cons'(x, xs)) → x
tail'(nil') → nil'
tail'(cons'(x, xs)) → xs
a' → b'
a' → c'
Types:
plus' :: 0':s':error' → 0':s':error' → 0':s':error'
plusIter' :: 0':s':error' → 0':s':error' → 0':s':error' → 0':s':error'
0' :: 0':s':error'
ifPlus' :: true':false' → 0':s':error' → 0':s':error' → 0':s':error' → 0':s':error'
le' :: 0':s':error' → 0':s':error' → true':false'
true' :: true':false'
false' :: true':false'
s' :: 0':s':error' → 0':s':error'
sum' :: nil':cons' → 0':s':error'
sumIter' :: nil':cons' → 0':s':error' → 0':s':error'
ifSum' :: true':false' → nil':cons' → 0':s':error' → 0':s':error' → 0':s':error'
isempty' :: nil':cons' → true':false'
head' :: nil':cons' → 0':s':error'
tail' :: nil':cons' → nil':cons'
nil' :: nil':cons'
cons' :: 0':s':error' → nil':cons' → nil':cons'
error' :: 0':s':error'
a' :: b':c'
b' :: b':c'
c' :: b':c'
_hole_0':s':error'1 :: 0':s':error'
_hole_true':false'2 :: true':false'
_hole_nil':cons'3 :: nil':cons'
_hole_b':c'4 :: b':c'
_gen_0':s':error'5 :: Nat → 0':s':error'
_gen_nil':cons'6 :: Nat → nil':cons'
Lemmas:
le'(_gen_0':s':error'5(+(1, _n8)), _gen_0':s':error'5(_n8)) → false', rt ∈ Ω(1 + n8)
Generator Equations:
_gen_0':s':error'5(0) ⇔ 0'
_gen_0':s':error'5(+(x, 1)) ⇔ s'(_gen_0':s':error'5(x))
_gen_nil':cons'6(0) ⇔ nil'
_gen_nil':cons'6(+(x, 1)) ⇔ cons'(0', _gen_nil':cons'6(x))
The following defined symbols remain to be analysed:
plusIter', sumIter'
Could not prove a rewrite lemma for the defined symbol plusIter'.
Rules:
plus'(x, y) → plusIter'(x, y, 0')
plusIter'(x, y, z) → ifPlus'(le'(x, z), x, y, z)
ifPlus'(true', x, y, z) → y
ifPlus'(false', x, y, z) → plusIter'(x, s'(y), s'(z))
le'(s'(x), 0') → false'
le'(0', y) → true'
le'(s'(x), s'(y)) → le'(x, y)
sum'(xs) → sumIter'(xs, 0')
sumIter'(xs, x) → ifSum'(isempty'(xs), xs, x, plus'(x, head'(xs)))
ifSum'(true', xs, x, y) → x
ifSum'(false', xs, x, y) → sumIter'(tail'(xs), y)
isempty'(nil') → true'
isempty'(cons'(x, xs)) → false'
head'(nil') → error'
head'(cons'(x, xs)) → x
tail'(nil') → nil'
tail'(cons'(x, xs)) → xs
a' → b'
a' → c'
Types:
plus' :: 0':s':error' → 0':s':error' → 0':s':error'
plusIter' :: 0':s':error' → 0':s':error' → 0':s':error' → 0':s':error'
0' :: 0':s':error'
ifPlus' :: true':false' → 0':s':error' → 0':s':error' → 0':s':error' → 0':s':error'
le' :: 0':s':error' → 0':s':error' → true':false'
true' :: true':false'
false' :: true':false'
s' :: 0':s':error' → 0':s':error'
sum' :: nil':cons' → 0':s':error'
sumIter' :: nil':cons' → 0':s':error' → 0':s':error'
ifSum' :: true':false' → nil':cons' → 0':s':error' → 0':s':error' → 0':s':error'
isempty' :: nil':cons' → true':false'
head' :: nil':cons' → 0':s':error'
tail' :: nil':cons' → nil':cons'
nil' :: nil':cons'
cons' :: 0':s':error' → nil':cons' → nil':cons'
error' :: 0':s':error'
a' :: b':c'
b' :: b':c'
c' :: b':c'
_hole_0':s':error'1 :: 0':s':error'
_hole_true':false'2 :: true':false'
_hole_nil':cons'3 :: nil':cons'
_hole_b':c'4 :: b':c'
_gen_0':s':error'5 :: Nat → 0':s':error'
_gen_nil':cons'6 :: Nat → nil':cons'
Lemmas:
le'(_gen_0':s':error'5(+(1, _n8)), _gen_0':s':error'5(_n8)) → false', rt ∈ Ω(1 + n8)
Generator Equations:
_gen_0':s':error'5(0) ⇔ 0'
_gen_0':s':error'5(+(x, 1)) ⇔ s'(_gen_0':s':error'5(x))
_gen_nil':cons'6(0) ⇔ nil'
_gen_nil':cons'6(+(x, 1)) ⇔ cons'(0', _gen_nil':cons'6(x))
The following defined symbols remain to be analysed:
sumIter'
Proved the following rewrite lemma:
sumIter'(_gen_nil':cons'6(_n2748), _gen_0':s':error'5(1)) → _*7, rt ∈ Ω(n2748)
Induction Base:
sumIter'(_gen_nil':cons'6(0), _gen_0':s':error'5(1))
Induction Step:
sumIter'(_gen_nil':cons'6(+(_$n2749, 1)), _gen_0':s':error'5(1)) →RΩ(1)
ifSum'(isempty'(_gen_nil':cons'6(+(_$n2749, 1))), _gen_nil':cons'6(+(_$n2749, 1)), _gen_0':s':error'5(1), plus'(_gen_0':s':error'5(1), head'(_gen_nil':cons'6(+(_$n2749, 1))))) →RΩ(1)
ifSum'(false', _gen_nil':cons'6(+(1, _$n2749)), _gen_0':s':error'5(1), plus'(_gen_0':s':error'5(1), head'(_gen_nil':cons'6(+(1, _$n2749))))) →RΩ(1)
ifSum'(false', _gen_nil':cons'6(+(1, _$n2749)), _gen_0':s':error'5(1), plus'(_gen_0':s':error'5(1), 0')) →RΩ(1)
ifSum'(false', _gen_nil':cons'6(+(1, _$n2749)), _gen_0':s':error'5(1), plusIter'(_gen_0':s':error'5(1), 0', 0')) →RΩ(1)
ifSum'(false', _gen_nil':cons'6(+(1, _$n2749)), _gen_0':s':error'5(1), ifPlus'(le'(_gen_0':s':error'5(1), 0'), _gen_0':s':error'5(1), 0', 0')) →LΩ(1)
ifSum'(false', _gen_nil':cons'6(+(1, _$n2749)), _gen_0':s':error'5(1), ifPlus'(false', _gen_0':s':error'5(1), 0', 0')) →RΩ(1)
ifSum'(false', _gen_nil':cons'6(+(1, _$n2749)), _gen_0':s':error'5(1), plusIter'(_gen_0':s':error'5(1), s'(0'), s'(0'))) →RΩ(1)
ifSum'(false', _gen_nil':cons'6(+(1, _$n2749)), _gen_0':s':error'5(1), ifPlus'(le'(_gen_0':s':error'5(1), s'(0')), _gen_0':s':error'5(1), s'(0'), s'(0'))) →RΩ(1)
ifSum'(false', _gen_nil':cons'6(+(1, _$n2749)), _gen_0':s':error'5(1), ifPlus'(le'(_gen_0':s':error'5(0), 0'), _gen_0':s':error'5(1), s'(0'), s'(0'))) →RΩ(1)
ifSum'(false', _gen_nil':cons'6(+(1, _$n2749)), _gen_0':s':error'5(1), ifPlus'(true', _gen_0':s':error'5(1), s'(0'), s'(0'))) →RΩ(1)
ifSum'(false', _gen_nil':cons'6(+(1, _$n2749)), _gen_0':s':error'5(1), s'(0')) →RΩ(1)
sumIter'(tail'(_gen_nil':cons'6(+(1, _$n2749))), s'(0')) →RΩ(1)
sumIter'(_gen_nil':cons'6(_$n2749), s'(0')) →IH
_*7
We have rt ∈ Ω(n) and sz ∈ O(n). Thus, we have ircR ∈ Ω(n).
Rules:
plus'(x, y) → plusIter'(x, y, 0')
plusIter'(x, y, z) → ifPlus'(le'(x, z), x, y, z)
ifPlus'(true', x, y, z) → y
ifPlus'(false', x, y, z) → plusIter'(x, s'(y), s'(z))
le'(s'(x), 0') → false'
le'(0', y) → true'
le'(s'(x), s'(y)) → le'(x, y)
sum'(xs) → sumIter'(xs, 0')
sumIter'(xs, x) → ifSum'(isempty'(xs), xs, x, plus'(x, head'(xs)))
ifSum'(true', xs, x, y) → x
ifSum'(false', xs, x, y) → sumIter'(tail'(xs), y)
isempty'(nil') → true'
isempty'(cons'(x, xs)) → false'
head'(nil') → error'
head'(cons'(x, xs)) → x
tail'(nil') → nil'
tail'(cons'(x, xs)) → xs
a' → b'
a' → c'
Types:
plus' :: 0':s':error' → 0':s':error' → 0':s':error'
plusIter' :: 0':s':error' → 0':s':error' → 0':s':error' → 0':s':error'
0' :: 0':s':error'
ifPlus' :: true':false' → 0':s':error' → 0':s':error' → 0':s':error' → 0':s':error'
le' :: 0':s':error' → 0':s':error' → true':false'
true' :: true':false'
false' :: true':false'
s' :: 0':s':error' → 0':s':error'
sum' :: nil':cons' → 0':s':error'
sumIter' :: nil':cons' → 0':s':error' → 0':s':error'
ifSum' :: true':false' → nil':cons' → 0':s':error' → 0':s':error' → 0':s':error'
isempty' :: nil':cons' → true':false'
head' :: nil':cons' → 0':s':error'
tail' :: nil':cons' → nil':cons'
nil' :: nil':cons'
cons' :: 0':s':error' → nil':cons' → nil':cons'
error' :: 0':s':error'
a' :: b':c'
b' :: b':c'
c' :: b':c'
_hole_0':s':error'1 :: 0':s':error'
_hole_true':false'2 :: true':false'
_hole_nil':cons'3 :: nil':cons'
_hole_b':c'4 :: b':c'
_gen_0':s':error'5 :: Nat → 0':s':error'
_gen_nil':cons'6 :: Nat → nil':cons'
Lemmas:
le'(_gen_0':s':error'5(+(1, _n8)), _gen_0':s':error'5(_n8)) → false', rt ∈ Ω(1 + n8)
sumIter'(_gen_nil':cons'6(_n2748), _gen_0':s':error'5(1)) → _*7, rt ∈ Ω(n2748)
Generator Equations:
_gen_0':s':error'5(0) ⇔ 0'
_gen_0':s':error'5(+(x, 1)) ⇔ s'(_gen_0':s':error'5(x))
_gen_nil':cons'6(0) ⇔ nil'
_gen_nil':cons'6(+(x, 1)) ⇔ cons'(0', _gen_nil':cons'6(x))
No more defined symbols left to analyse.
The lowerbound Ω(n) was proven with the following lemma:
le'(_gen_0':s':error'5(+(1, _n8)), _gen_0':s':error'5(_n8)) → false', rt ∈ Ω(1 + n8)