isEmpty(cons(x, xs)) → false
isEmpty(nil) → true
isZero(0) → true
isZero(s(x)) → false
head(cons(x, xs)) → x
tail(cons(x, xs)) → xs
tail(nil) → nil
p(s(s(x))) → s(p(s(x)))
p(s(0)) → 0
p(0) → 0
inc(s(x)) → s(inc(x))
inc(0) → s(0)
sumList(xs, y) → if(isEmpty(xs), isZero(head(xs)), y, tail(xs), cons(p(head(xs)), tail(xs)), inc(y))
if(true, b, y, xs, ys, x) → y
if(false, true, y, xs, ys, x) → sumList(xs, y)
if(false, false, y, xs, ys, x) → sumList(ys, x)
sum(xs) → sumList(xs, 0)
Renamed function symbols to avoid clashes with predefined symbol.
Runtime Complexity TRS:
The TRS R consists of the following rules:
isEmpty'(cons'(x, xs)) → false'
isEmpty'(nil') → true'
isZero'(0') → true'
isZero'(s'(x)) → false'
head'(cons'(x, xs)) → x
tail'(cons'(x, xs)) → xs
tail'(nil') → nil'
p'(s'(s'(x))) → s'(p'(s'(x)))
p'(s'(0')) → 0'
p'(0') → 0'
inc'(s'(x)) → s'(inc'(x))
inc'(0') → s'(0')
sumList'(xs, y) → if'(isEmpty'(xs), isZero'(head'(xs)), y, tail'(xs), cons'(p'(head'(xs)), tail'(xs)), inc'(y))
if'(true', b, y, xs, ys, x) → y
if'(false', true', y, xs, ys, x) → sumList'(xs, y)
if'(false', false', y, xs, ys, x) → sumList'(ys, x)
sum'(xs) → sumList'(xs, 0')
Infered types.
Rules:
isEmpty'(cons'(x, xs)) → false'
isEmpty'(nil') → true'
isZero'(0') → true'
isZero'(s'(x)) → false'
head'(cons'(x, xs)) → x
tail'(cons'(x, xs)) → xs
tail'(nil') → nil'
p'(s'(s'(x))) → s'(p'(s'(x)))
p'(s'(0')) → 0'
p'(0') → 0'
inc'(s'(x)) → s'(inc'(x))
inc'(0') → s'(0')
sumList'(xs, y) → if'(isEmpty'(xs), isZero'(head'(xs)), y, tail'(xs), cons'(p'(head'(xs)), tail'(xs)), inc'(y))
if'(true', b, y, xs, ys, x) → y
if'(false', true', y, xs, ys, x) → sumList'(xs, y)
if'(false', false', y, xs, ys, x) → sumList'(ys, x)
sum'(xs) → sumList'(xs, 0')
Types:
isEmpty' :: cons':nil' → false':true'
cons' :: 0':s' → cons':nil' → cons':nil'
false' :: false':true'
nil' :: cons':nil'
true' :: false':true'
isZero' :: 0':s' → false':true'
0' :: 0':s'
s' :: 0':s' → 0':s'
head' :: cons':nil' → 0':s'
tail' :: cons':nil' → cons':nil'
p' :: 0':s' → 0':s'
inc' :: 0':s' → 0':s'
sumList' :: cons':nil' → 0':s' → 0':s'
if' :: false':true' → false':true' → 0':s' → cons':nil' → cons':nil' → 0':s' → 0':s'
sum' :: cons':nil' → 0':s'
_hole_false':true'1 :: false':true'
_hole_cons':nil'2 :: cons':nil'
_hole_0':s'3 :: 0':s'
_gen_cons':nil'4 :: Nat → cons':nil'
_gen_0':s'5 :: Nat → 0':s'
Heuristically decided to analyse the following defined symbols:
p', inc', sumList'
They will be analysed ascendingly in the following order:
p' < sumList'
inc' < sumList'
Rules:
isEmpty'(cons'(x, xs)) → false'
isEmpty'(nil') → true'
isZero'(0') → true'
isZero'(s'(x)) → false'
head'(cons'(x, xs)) → x
tail'(cons'(x, xs)) → xs
tail'(nil') → nil'
p'(s'(s'(x))) → s'(p'(s'(x)))
p'(s'(0')) → 0'
p'(0') → 0'
inc'(s'(x)) → s'(inc'(x))
inc'(0') → s'(0')
sumList'(xs, y) → if'(isEmpty'(xs), isZero'(head'(xs)), y, tail'(xs), cons'(p'(head'(xs)), tail'(xs)), inc'(y))
if'(true', b, y, xs, ys, x) → y
if'(false', true', y, xs, ys, x) → sumList'(xs, y)
if'(false', false', y, xs, ys, x) → sumList'(ys, x)
sum'(xs) → sumList'(xs, 0')
Types:
isEmpty' :: cons':nil' → false':true'
cons' :: 0':s' → cons':nil' → cons':nil'
false' :: false':true'
nil' :: cons':nil'
true' :: false':true'
isZero' :: 0':s' → false':true'
0' :: 0':s'
s' :: 0':s' → 0':s'
head' :: cons':nil' → 0':s'
tail' :: cons':nil' → cons':nil'
p' :: 0':s' → 0':s'
inc' :: 0':s' → 0':s'
sumList' :: cons':nil' → 0':s' → 0':s'
if' :: false':true' → false':true' → 0':s' → cons':nil' → cons':nil' → 0':s' → 0':s'
sum' :: cons':nil' → 0':s'
_hole_false':true'1 :: false':true'
_hole_cons':nil'2 :: cons':nil'
_hole_0':s'3 :: 0':s'
_gen_cons':nil'4 :: Nat → cons':nil'
_gen_0':s'5 :: Nat → 0':s'
Generator Equations:
_gen_cons':nil'4(0) ⇔ nil'
_gen_cons':nil'4(+(x, 1)) ⇔ cons'(0', _gen_cons':nil'4(x))
_gen_0':s'5(0) ⇔ 0'
_gen_0':s'5(+(x, 1)) ⇔ s'(_gen_0':s'5(x))
The following defined symbols remain to be analysed:
p', inc', sumList'
They will be analysed ascendingly in the following order:
p' < sumList'
inc' < sumList'
Proved the following rewrite lemma:
p'(_gen_0':s'5(+(1, _n7))) → _gen_0':s'5(_n7), rt ∈ Ω(1 + n7)
Induction Base:
p'(_gen_0':s'5(+(1, 0))) →RΩ(1)
0'
Induction Step:
p'(_gen_0':s'5(+(1, +(_$n8, 1)))) →RΩ(1)
s'(p'(s'(_gen_0':s'5(_$n8)))) →IH
s'(_gen_0':s'5(_$n8))
We have rt ∈ Ω(n) and sz ∈ O(n). Thus, we have ircR ∈ Ω(n).
Rules:
isEmpty'(cons'(x, xs)) → false'
isEmpty'(nil') → true'
isZero'(0') → true'
isZero'(s'(x)) → false'
head'(cons'(x, xs)) → x
tail'(cons'(x, xs)) → xs
tail'(nil') → nil'
p'(s'(s'(x))) → s'(p'(s'(x)))
p'(s'(0')) → 0'
p'(0') → 0'
inc'(s'(x)) → s'(inc'(x))
inc'(0') → s'(0')
sumList'(xs, y) → if'(isEmpty'(xs), isZero'(head'(xs)), y, tail'(xs), cons'(p'(head'(xs)), tail'(xs)), inc'(y))
if'(true', b, y, xs, ys, x) → y
if'(false', true', y, xs, ys, x) → sumList'(xs, y)
if'(false', false', y, xs, ys, x) → sumList'(ys, x)
sum'(xs) → sumList'(xs, 0')
Types:
isEmpty' :: cons':nil' → false':true'
cons' :: 0':s' → cons':nil' → cons':nil'
false' :: false':true'
nil' :: cons':nil'
true' :: false':true'
isZero' :: 0':s' → false':true'
0' :: 0':s'
s' :: 0':s' → 0':s'
head' :: cons':nil' → 0':s'
tail' :: cons':nil' → cons':nil'
p' :: 0':s' → 0':s'
inc' :: 0':s' → 0':s'
sumList' :: cons':nil' → 0':s' → 0':s'
if' :: false':true' → false':true' → 0':s' → cons':nil' → cons':nil' → 0':s' → 0':s'
sum' :: cons':nil' → 0':s'
_hole_false':true'1 :: false':true'
_hole_cons':nil'2 :: cons':nil'
_hole_0':s'3 :: 0':s'
_gen_cons':nil'4 :: Nat → cons':nil'
_gen_0':s'5 :: Nat → 0':s'
Lemmas:
p'(_gen_0':s'5(+(1, _n7))) → _gen_0':s'5(_n7), rt ∈ Ω(1 + n7)
Generator Equations:
_gen_cons':nil'4(0) ⇔ nil'
_gen_cons':nil'4(+(x, 1)) ⇔ cons'(0', _gen_cons':nil'4(x))
_gen_0':s'5(0) ⇔ 0'
_gen_0':s'5(+(x, 1)) ⇔ s'(_gen_0':s'5(x))
The following defined symbols remain to be analysed:
inc', sumList'
They will be analysed ascendingly in the following order:
inc' < sumList'
Proved the following rewrite lemma:
inc'(_gen_0':s'5(_n737)) → _gen_0':s'5(+(1, _n737)), rt ∈ Ω(1 + n737)
Induction Base:
inc'(_gen_0':s'5(0)) →RΩ(1)
s'(0')
Induction Step:
inc'(_gen_0':s'5(+(_$n738, 1))) →RΩ(1)
s'(inc'(_gen_0':s'5(_$n738))) →IH
s'(_gen_0':s'5(+(1, _$n738)))
We have rt ∈ Ω(n) and sz ∈ O(n). Thus, we have ircR ∈ Ω(n).
Rules:
isEmpty'(cons'(x, xs)) → false'
isEmpty'(nil') → true'
isZero'(0') → true'
isZero'(s'(x)) → false'
head'(cons'(x, xs)) → x
tail'(cons'(x, xs)) → xs
tail'(nil') → nil'
p'(s'(s'(x))) → s'(p'(s'(x)))
p'(s'(0')) → 0'
p'(0') → 0'
inc'(s'(x)) → s'(inc'(x))
inc'(0') → s'(0')
sumList'(xs, y) → if'(isEmpty'(xs), isZero'(head'(xs)), y, tail'(xs), cons'(p'(head'(xs)), tail'(xs)), inc'(y))
if'(true', b, y, xs, ys, x) → y
if'(false', true', y, xs, ys, x) → sumList'(xs, y)
if'(false', false', y, xs, ys, x) → sumList'(ys, x)
sum'(xs) → sumList'(xs, 0')
Types:
isEmpty' :: cons':nil' → false':true'
cons' :: 0':s' → cons':nil' → cons':nil'
false' :: false':true'
nil' :: cons':nil'
true' :: false':true'
isZero' :: 0':s' → false':true'
0' :: 0':s'
s' :: 0':s' → 0':s'
head' :: cons':nil' → 0':s'
tail' :: cons':nil' → cons':nil'
p' :: 0':s' → 0':s'
inc' :: 0':s' → 0':s'
sumList' :: cons':nil' → 0':s' → 0':s'
if' :: false':true' → false':true' → 0':s' → cons':nil' → cons':nil' → 0':s' → 0':s'
sum' :: cons':nil' → 0':s'
_hole_false':true'1 :: false':true'
_hole_cons':nil'2 :: cons':nil'
_hole_0':s'3 :: 0':s'
_gen_cons':nil'4 :: Nat → cons':nil'
_gen_0':s'5 :: Nat → 0':s'
Lemmas:
p'(_gen_0':s'5(+(1, _n7))) → _gen_0':s'5(_n7), rt ∈ Ω(1 + n7)
inc'(_gen_0':s'5(_n737)) → _gen_0':s'5(+(1, _n737)), rt ∈ Ω(1 + n737)
Generator Equations:
_gen_cons':nil'4(0) ⇔ nil'
_gen_cons':nil'4(+(x, 1)) ⇔ cons'(0', _gen_cons':nil'4(x))
_gen_0':s'5(0) ⇔ 0'
_gen_0':s'5(+(x, 1)) ⇔ s'(_gen_0':s'5(x))
The following defined symbols remain to be analysed:
sumList'
Proved the following rewrite lemma:
sumList'(_gen_cons':nil'4(_n1439), _gen_0':s'5(b)) → _gen_0':s'5(b), rt ∈ Ω(1 + b2188·n1439 + n1439 + b)
Induction Base:
sumList'(_gen_cons':nil'4(0), _gen_0':s'5(b)) →RΩ(1)
if'(isEmpty'(_gen_cons':nil'4(0)), isZero'(head'(_gen_cons':nil'4(0))), _gen_0':s'5(b), tail'(_gen_cons':nil'4(0)), cons'(p'(head'(_gen_cons':nil'4(0))), tail'(_gen_cons':nil'4(0))), inc'(_gen_0':s'5(b))) →RΩ(1)
if'(true', isZero'(head'(_gen_cons':nil'4(0))), _gen_0':s'5(b), tail'(_gen_cons':nil'4(0)), cons'(p'(head'(_gen_cons':nil'4(0))), tail'(_gen_cons':nil'4(0))), inc'(_gen_0':s'5(b))) →RΩ(1)
if'(true', isZero'(head'(_gen_cons':nil'4(0))), _gen_0':s'5(b), nil', cons'(p'(head'(_gen_cons':nil'4(0))), tail'(_gen_cons':nil'4(0))), inc'(_gen_0':s'5(b))) →RΩ(1)
if'(true', isZero'(head'(_gen_cons':nil'4(0))), _gen_0':s'5(b), nil', cons'(p'(head'(_gen_cons':nil'4(0))), nil'), inc'(_gen_0':s'5(b))) →LΩ(1 + b)
if'(true', isZero'(head'(_gen_cons':nil'4(0))), _gen_0':s'5(b), nil', cons'(p'(head'(_gen_cons':nil'4(0))), nil'), _gen_0':s'5(+(1, b))) →RΩ(1)
_gen_0':s'5(b)
Induction Step:
sumList'(_gen_cons':nil'4(+(_$n1440, 1)), _gen_0':s'5(_b2188)) →RΩ(1)
if'(isEmpty'(_gen_cons':nil'4(+(_$n1440, 1))), isZero'(head'(_gen_cons':nil'4(+(_$n1440, 1)))), _gen_0':s'5(_b2188), tail'(_gen_cons':nil'4(+(_$n1440, 1))), cons'(p'(head'(_gen_cons':nil'4(+(_$n1440, 1)))), tail'(_gen_cons':nil'4(+(_$n1440, 1)))), inc'(_gen_0':s'5(_b2188))) →RΩ(1)
if'(false', isZero'(head'(_gen_cons':nil'4(+(1, _$n1440)))), _gen_0':s'5(_b2188), tail'(_gen_cons':nil'4(+(1, _$n1440))), cons'(p'(head'(_gen_cons':nil'4(+(1, _$n1440)))), tail'(_gen_cons':nil'4(+(1, _$n1440)))), inc'(_gen_0':s'5(_b2188))) →RΩ(1)
if'(false', isZero'(0'), _gen_0':s'5(_b2188), tail'(_gen_cons':nil'4(+(1, _$n1440))), cons'(p'(head'(_gen_cons':nil'4(+(1, _$n1440)))), tail'(_gen_cons':nil'4(+(1, _$n1440)))), inc'(_gen_0':s'5(_b2188))) →RΩ(1)
if'(false', true', _gen_0':s'5(_b2188), tail'(_gen_cons':nil'4(+(1, _$n1440))), cons'(p'(head'(_gen_cons':nil'4(+(1, _$n1440)))), tail'(_gen_cons':nil'4(+(1, _$n1440)))), inc'(_gen_0':s'5(_b2188))) →RΩ(1)
if'(false', true', _gen_0':s'5(_b2188), _gen_cons':nil'4(_$n1440), cons'(p'(head'(_gen_cons':nil'4(+(1, _$n1440)))), tail'(_gen_cons':nil'4(+(1, _$n1440)))), inc'(_gen_0':s'5(_b2188))) →RΩ(1)
if'(false', true', _gen_0':s'5(_b2188), _gen_cons':nil'4(_$n1440), cons'(p'(0'), tail'(_gen_cons':nil'4(+(1, _$n1440)))), inc'(_gen_0':s'5(_b2188))) →RΩ(1)
if'(false', true', _gen_0':s'5(_b2188), _gen_cons':nil'4(_$n1440), cons'(0', tail'(_gen_cons':nil'4(+(1, _$n1440)))), inc'(_gen_0':s'5(_b2188))) →RΩ(1)
if'(false', true', _gen_0':s'5(_b2188), _gen_cons':nil'4(_$n1440), cons'(0', _gen_cons':nil'4(_$n1440)), inc'(_gen_0':s'5(_b2188))) →LΩ(1 + b2188)
if'(false', true', _gen_0':s'5(_b2188), _gen_cons':nil'4(_$n1440), cons'(0', _gen_cons':nil'4(_$n1440)), _gen_0':s'5(+(1, _b2188))) →RΩ(1)
sumList'(_gen_cons':nil'4(_$n1440), _gen_0':s'5(_b2188)) →IH
_gen_0':s'5(_b2188)
We have rt ∈ Ω(n2) and sz ∈ O(n). Thus, we have ircR ∈ Ω(n2).
Rules:
isEmpty'(cons'(x, xs)) → false'
isEmpty'(nil') → true'
isZero'(0') → true'
isZero'(s'(x)) → false'
head'(cons'(x, xs)) → x
tail'(cons'(x, xs)) → xs
tail'(nil') → nil'
p'(s'(s'(x))) → s'(p'(s'(x)))
p'(s'(0')) → 0'
p'(0') → 0'
inc'(s'(x)) → s'(inc'(x))
inc'(0') → s'(0')
sumList'(xs, y) → if'(isEmpty'(xs), isZero'(head'(xs)), y, tail'(xs), cons'(p'(head'(xs)), tail'(xs)), inc'(y))
if'(true', b, y, xs, ys, x) → y
if'(false', true', y, xs, ys, x) → sumList'(xs, y)
if'(false', false', y, xs, ys, x) → sumList'(ys, x)
sum'(xs) → sumList'(xs, 0')
Types:
isEmpty' :: cons':nil' → false':true'
cons' :: 0':s' → cons':nil' → cons':nil'
false' :: false':true'
nil' :: cons':nil'
true' :: false':true'
isZero' :: 0':s' → false':true'
0' :: 0':s'
s' :: 0':s' → 0':s'
head' :: cons':nil' → 0':s'
tail' :: cons':nil' → cons':nil'
p' :: 0':s' → 0':s'
inc' :: 0':s' → 0':s'
sumList' :: cons':nil' → 0':s' → 0':s'
if' :: false':true' → false':true' → 0':s' → cons':nil' → cons':nil' → 0':s' → 0':s'
sum' :: cons':nil' → 0':s'
_hole_false':true'1 :: false':true'
_hole_cons':nil'2 :: cons':nil'
_hole_0':s'3 :: 0':s'
_gen_cons':nil'4 :: Nat → cons':nil'
_gen_0':s'5 :: Nat → 0':s'
Lemmas:
p'(_gen_0':s'5(+(1, _n7))) → _gen_0':s'5(_n7), rt ∈ Ω(1 + n7)
inc'(_gen_0':s'5(_n737)) → _gen_0':s'5(+(1, _n737)), rt ∈ Ω(1 + n737)
sumList'(_gen_cons':nil'4(_n1439), _gen_0':s'5(b)) → _gen_0':s'5(b), rt ∈ Ω(1 + b2188·n1439 + n1439 + b)
Generator Equations:
_gen_cons':nil'4(0) ⇔ nil'
_gen_cons':nil'4(+(x, 1)) ⇔ cons'(0', _gen_cons':nil'4(x))
_gen_0':s'5(0) ⇔ 0'
_gen_0':s'5(+(x, 1)) ⇔ s'(_gen_0':s'5(x))
No more defined symbols left to analyse.
The lowerbound Ω(n2) was proven with the following lemma:
sumList'(_gen_cons':nil'4(_n1439), _gen_0':s'5(b)) → _gen_0':s'5(b), rt ∈ Ω(1 + b2188·n1439 + n1439 + b)