car(cons(x, l)) → x
cddr(nil) → nil
cddr(cons(x, nil)) → nil
cddr(cons(x, cons(y, l))) → l
cadr(cons(x, cons(y, l))) → y
isZero(0) → true
isZero(s(x)) → false
plus(x, y) → ifplus(isZero(x), x, y)
ifplus(true, x, y) → y
ifplus(false, x, y) → s(plus(p(x), y))
times(x, y) → iftimes(isZero(x), x, y)
iftimes(true, x, y) → 0
iftimes(false, x, y) → plus(y, times(p(x), y))
p(s(x)) → x
p(0) → 0
shorter(nil, y) → true
shorter(cons(x, l), 0) → false
shorter(cons(x, l), s(y)) → shorter(l, y)
prod(l) → if(shorter(l, 0), shorter(l, s(0)), l)
if(true, b, l) → s(0)
if(false, b, l) → if2(b, l)
if2(true, l) → car(l)
if2(false, l) → prod(cons(times(car(l), cadr(l)), cddr(l)))
Renamed function symbols to avoid clashes with predefined symbol.
Runtime Complexity TRS:
The TRS R consists of the following rules:
car'(cons'(x, l)) → x
cddr'(nil') → nil'
cddr'(cons'(x, nil')) → nil'
cddr'(cons'(x, cons'(y, l))) → l
cadr'(cons'(x, cons'(y, l))) → y
isZero'(0') → true'
isZero'(s'(x)) → false'
plus'(x, y) → ifplus'(isZero'(x), x, y)
ifplus'(true', x, y) → y
ifplus'(false', x, y) → s'(plus'(p'(x), y))
times'(x, y) → iftimes'(isZero'(x), x, y)
iftimes'(true', x, y) → 0'
iftimes'(false', x, y) → plus'(y, times'(p'(x), y))
p'(s'(x)) → x
p'(0') → 0'
shorter'(nil', y) → true'
shorter'(cons'(x, l), 0') → false'
shorter'(cons'(x, l), s'(y)) → shorter'(l, y)
prod'(l) → if'(shorter'(l, 0'), shorter'(l, s'(0')), l)
if'(true', b, l) → s'(0')
if'(false', b, l) → if2'(b, l)
if2'(true', l) → car'(l)
if2'(false', l) → prod'(cons'(times'(car'(l), cadr'(l)), cddr'(l)))
Infered types.
Rules:
car'(cons'(x, l)) → x
cddr'(nil') → nil'
cddr'(cons'(x, nil')) → nil'
cddr'(cons'(x, cons'(y, l))) → l
cadr'(cons'(x, cons'(y, l))) → y
isZero'(0') → true'
isZero'(s'(x)) → false'
plus'(x, y) → ifplus'(isZero'(x), x, y)
ifplus'(true', x, y) → y
ifplus'(false', x, y) → s'(plus'(p'(x), y))
times'(x, y) → iftimes'(isZero'(x), x, y)
iftimes'(true', x, y) → 0'
iftimes'(false', x, y) → plus'(y, times'(p'(x), y))
p'(s'(x)) → x
p'(0') → 0'
shorter'(nil', y) → true'
shorter'(cons'(x, l), 0') → false'
shorter'(cons'(x, l), s'(y)) → shorter'(l, y)
prod'(l) → if'(shorter'(l, 0'), shorter'(l, s'(0')), l)
if'(true', b, l) → s'(0')
if'(false', b, l) → if2'(b, l)
if2'(true', l) → car'(l)
if2'(false', l) → prod'(cons'(times'(car'(l), cadr'(l)), cddr'(l)))
Types:
car' :: cons':nil' → 0':s'
cons' :: 0':s' → cons':nil' → cons':nil'
cddr' :: cons':nil' → cons':nil'
nil' :: cons':nil'
cadr' :: cons':nil' → 0':s'
isZero' :: 0':s' → true':false'
0' :: 0':s'
true' :: true':false'
s' :: 0':s' → 0':s'
false' :: true':false'
plus' :: 0':s' → 0':s' → 0':s'
ifplus' :: true':false' → 0':s' → 0':s' → 0':s'
p' :: 0':s' → 0':s'
times' :: 0':s' → 0':s' → 0':s'
iftimes' :: true':false' → 0':s' → 0':s' → 0':s'
shorter' :: cons':nil' → 0':s' → true':false'
prod' :: cons':nil' → 0':s'
if' :: true':false' → true':false' → cons':nil' → 0':s'
if2' :: true':false' → cons':nil' → 0':s'
_hole_0':s'1 :: 0':s'
_hole_cons':nil'2 :: cons':nil'
_hole_true':false'3 :: true':false'
_gen_0':s'4 :: Nat → 0':s'
_gen_cons':nil'5 :: Nat → cons':nil'
Heuristically decided to analyse the following defined symbols:
plus', times', shorter', prod'
They will be analysed ascendingly in the following order:
plus' < times'
times' < prod'
shorter' < prod'
Rules:
car'(cons'(x, l)) → x
cddr'(nil') → nil'
cddr'(cons'(x, nil')) → nil'
cddr'(cons'(x, cons'(y, l))) → l
cadr'(cons'(x, cons'(y, l))) → y
isZero'(0') → true'
isZero'(s'(x)) → false'
plus'(x, y) → ifplus'(isZero'(x), x, y)
ifplus'(true', x, y) → y
ifplus'(false', x, y) → s'(plus'(p'(x), y))
times'(x, y) → iftimes'(isZero'(x), x, y)
iftimes'(true', x, y) → 0'
iftimes'(false', x, y) → plus'(y, times'(p'(x), y))
p'(s'(x)) → x
p'(0') → 0'
shorter'(nil', y) → true'
shorter'(cons'(x, l), 0') → false'
shorter'(cons'(x, l), s'(y)) → shorter'(l, y)
prod'(l) → if'(shorter'(l, 0'), shorter'(l, s'(0')), l)
if'(true', b, l) → s'(0')
if'(false', b, l) → if2'(b, l)
if2'(true', l) → car'(l)
if2'(false', l) → prod'(cons'(times'(car'(l), cadr'(l)), cddr'(l)))
Types:
car' :: cons':nil' → 0':s'
cons' :: 0':s' → cons':nil' → cons':nil'
cddr' :: cons':nil' → cons':nil'
nil' :: cons':nil'
cadr' :: cons':nil' → 0':s'
isZero' :: 0':s' → true':false'
0' :: 0':s'
true' :: true':false'
s' :: 0':s' → 0':s'
false' :: true':false'
plus' :: 0':s' → 0':s' → 0':s'
ifplus' :: true':false' → 0':s' → 0':s' → 0':s'
p' :: 0':s' → 0':s'
times' :: 0':s' → 0':s' → 0':s'
iftimes' :: true':false' → 0':s' → 0':s' → 0':s'
shorter' :: cons':nil' → 0':s' → true':false'
prod' :: cons':nil' → 0':s'
if' :: true':false' → true':false' → cons':nil' → 0':s'
if2' :: true':false' → cons':nil' → 0':s'
_hole_0':s'1 :: 0':s'
_hole_cons':nil'2 :: cons':nil'
_hole_true':false'3 :: true':false'
_gen_0':s'4 :: Nat → 0':s'
_gen_cons':nil'5 :: Nat → cons':nil'
Generator Equations:
_gen_0':s'4(0) ⇔ 0'
_gen_0':s'4(+(x, 1)) ⇔ s'(_gen_0':s'4(x))
_gen_cons':nil'5(0) ⇔ nil'
_gen_cons':nil'5(+(x, 1)) ⇔ cons'(0', _gen_cons':nil'5(x))
The following defined symbols remain to be analysed:
plus', times', shorter', prod'
They will be analysed ascendingly in the following order:
plus' < times'
times' < prod'
shorter' < prod'
Proved the following rewrite lemma:
plus'(_gen_0':s'4(_n7), _gen_0':s'4(b)) → _gen_0':s'4(+(_n7, b)), rt ∈ Ω(1 + n7)
Induction Base:
plus'(_gen_0':s'4(0), _gen_0':s'4(b)) →RΩ(1)
ifplus'(isZero'(_gen_0':s'4(0)), _gen_0':s'4(0), _gen_0':s'4(b)) →RΩ(1)
ifplus'(true', _gen_0':s'4(0), _gen_0':s'4(b)) →RΩ(1)
_gen_0':s'4(b)
Induction Step:
plus'(_gen_0':s'4(+(_$n8, 1)), _gen_0':s'4(_b372)) →RΩ(1)
ifplus'(isZero'(_gen_0':s'4(+(_$n8, 1))), _gen_0':s'4(+(_$n8, 1)), _gen_0':s'4(_b372)) →RΩ(1)
ifplus'(false', _gen_0':s'4(+(1, _$n8)), _gen_0':s'4(_b372)) →RΩ(1)
s'(plus'(p'(_gen_0':s'4(+(1, _$n8))), _gen_0':s'4(_b372))) →RΩ(1)
s'(plus'(_gen_0':s'4(_$n8), _gen_0':s'4(_b372))) →IH
s'(_gen_0':s'4(+(_$n8, _b372)))
We have rt ∈ Ω(n) and sz ∈ O(n). Thus, we have ircR ∈ Ω(n).
Rules:
car'(cons'(x, l)) → x
cddr'(nil') → nil'
cddr'(cons'(x, nil')) → nil'
cddr'(cons'(x, cons'(y, l))) → l
cadr'(cons'(x, cons'(y, l))) → y
isZero'(0') → true'
isZero'(s'(x)) → false'
plus'(x, y) → ifplus'(isZero'(x), x, y)
ifplus'(true', x, y) → y
ifplus'(false', x, y) → s'(plus'(p'(x), y))
times'(x, y) → iftimes'(isZero'(x), x, y)
iftimes'(true', x, y) → 0'
iftimes'(false', x, y) → plus'(y, times'(p'(x), y))
p'(s'(x)) → x
p'(0') → 0'
shorter'(nil', y) → true'
shorter'(cons'(x, l), 0') → false'
shorter'(cons'(x, l), s'(y)) → shorter'(l, y)
prod'(l) → if'(shorter'(l, 0'), shorter'(l, s'(0')), l)
if'(true', b, l) → s'(0')
if'(false', b, l) → if2'(b, l)
if2'(true', l) → car'(l)
if2'(false', l) → prod'(cons'(times'(car'(l), cadr'(l)), cddr'(l)))
Types:
car' :: cons':nil' → 0':s'
cons' :: 0':s' → cons':nil' → cons':nil'
cddr' :: cons':nil' → cons':nil'
nil' :: cons':nil'
cadr' :: cons':nil' → 0':s'
isZero' :: 0':s' → true':false'
0' :: 0':s'
true' :: true':false'
s' :: 0':s' → 0':s'
false' :: true':false'
plus' :: 0':s' → 0':s' → 0':s'
ifplus' :: true':false' → 0':s' → 0':s' → 0':s'
p' :: 0':s' → 0':s'
times' :: 0':s' → 0':s' → 0':s'
iftimes' :: true':false' → 0':s' → 0':s' → 0':s'
shorter' :: cons':nil' → 0':s' → true':false'
prod' :: cons':nil' → 0':s'
if' :: true':false' → true':false' → cons':nil' → 0':s'
if2' :: true':false' → cons':nil' → 0':s'
_hole_0':s'1 :: 0':s'
_hole_cons':nil'2 :: cons':nil'
_hole_true':false'3 :: true':false'
_gen_0':s'4 :: Nat → 0':s'
_gen_cons':nil'5 :: Nat → cons':nil'
Lemmas:
plus'(_gen_0':s'4(_n7), _gen_0':s'4(b)) → _gen_0':s'4(+(_n7, b)), rt ∈ Ω(1 + n7)
Generator Equations:
_gen_0':s'4(0) ⇔ 0'
_gen_0':s'4(+(x, 1)) ⇔ s'(_gen_0':s'4(x))
_gen_cons':nil'5(0) ⇔ nil'
_gen_cons':nil'5(+(x, 1)) ⇔ cons'(0', _gen_cons':nil'5(x))
The following defined symbols remain to be analysed:
times', shorter', prod'
They will be analysed ascendingly in the following order:
times' < prod'
shorter' < prod'
Proved the following rewrite lemma:
times'(_gen_0':s'4(_n3005), _gen_0':s'4(b)) → _gen_0':s'4(*(_n3005, b)), rt ∈ Ω(1 + b3630·n3005 + n3005)
Induction Base:
times'(_gen_0':s'4(0), _gen_0':s'4(b)) →RΩ(1)
iftimes'(isZero'(_gen_0':s'4(0)), _gen_0':s'4(0), _gen_0':s'4(b)) →RΩ(1)
iftimes'(true', _gen_0':s'4(0), _gen_0':s'4(b)) →RΩ(1)
0'
Induction Step:
times'(_gen_0':s'4(+(_$n3006, 1)), _gen_0':s'4(_b3630)) →RΩ(1)
iftimes'(isZero'(_gen_0':s'4(+(_$n3006, 1))), _gen_0':s'4(+(_$n3006, 1)), _gen_0':s'4(_b3630)) →RΩ(1)
iftimes'(false', _gen_0':s'4(+(1, _$n3006)), _gen_0':s'4(_b3630)) →RΩ(1)
plus'(_gen_0':s'4(_b3630), times'(p'(_gen_0':s'4(+(1, _$n3006))), _gen_0':s'4(_b3630))) →RΩ(1)
plus'(_gen_0':s'4(_b3630), times'(_gen_0':s'4(_$n3006), _gen_0':s'4(_b3630))) →IH
plus'(_gen_0':s'4(_b3630), _gen_0':s'4(*(_$n3006, _b3630))) →LΩ(1 + b3630)
_gen_0':s'4(+(_b3630, *(_$n3006, _b3630)))
We have rt ∈ Ω(n2) and sz ∈ O(n). Thus, we have ircR ∈ Ω(n2).
Rules:
car'(cons'(x, l)) → x
cddr'(nil') → nil'
cddr'(cons'(x, nil')) → nil'
cddr'(cons'(x, cons'(y, l))) → l
cadr'(cons'(x, cons'(y, l))) → y
isZero'(0') → true'
isZero'(s'(x)) → false'
plus'(x, y) → ifplus'(isZero'(x), x, y)
ifplus'(true', x, y) → y
ifplus'(false', x, y) → s'(plus'(p'(x), y))
times'(x, y) → iftimes'(isZero'(x), x, y)
iftimes'(true', x, y) → 0'
iftimes'(false', x, y) → plus'(y, times'(p'(x), y))
p'(s'(x)) → x
p'(0') → 0'
shorter'(nil', y) → true'
shorter'(cons'(x, l), 0') → false'
shorter'(cons'(x, l), s'(y)) → shorter'(l, y)
prod'(l) → if'(shorter'(l, 0'), shorter'(l, s'(0')), l)
if'(true', b, l) → s'(0')
if'(false', b, l) → if2'(b, l)
if2'(true', l) → car'(l)
if2'(false', l) → prod'(cons'(times'(car'(l), cadr'(l)), cddr'(l)))
Types:
car' :: cons':nil' → 0':s'
cons' :: 0':s' → cons':nil' → cons':nil'
cddr' :: cons':nil' → cons':nil'
nil' :: cons':nil'
cadr' :: cons':nil' → 0':s'
isZero' :: 0':s' → true':false'
0' :: 0':s'
true' :: true':false'
s' :: 0':s' → 0':s'
false' :: true':false'
plus' :: 0':s' → 0':s' → 0':s'
ifplus' :: true':false' → 0':s' → 0':s' → 0':s'
p' :: 0':s' → 0':s'
times' :: 0':s' → 0':s' → 0':s'
iftimes' :: true':false' → 0':s' → 0':s' → 0':s'
shorter' :: cons':nil' → 0':s' → true':false'
prod' :: cons':nil' → 0':s'
if' :: true':false' → true':false' → cons':nil' → 0':s'
if2' :: true':false' → cons':nil' → 0':s'
_hole_0':s'1 :: 0':s'
_hole_cons':nil'2 :: cons':nil'
_hole_true':false'3 :: true':false'
_gen_0':s'4 :: Nat → 0':s'
_gen_cons':nil'5 :: Nat → cons':nil'
Lemmas:
plus'(_gen_0':s'4(_n7), _gen_0':s'4(b)) → _gen_0':s'4(+(_n7, b)), rt ∈ Ω(1 + n7)
times'(_gen_0':s'4(_n3005), _gen_0':s'4(b)) → _gen_0':s'4(*(_n3005, b)), rt ∈ Ω(1 + b3630·n3005 + n3005)
Generator Equations:
_gen_0':s'4(0) ⇔ 0'
_gen_0':s'4(+(x, 1)) ⇔ s'(_gen_0':s'4(x))
_gen_cons':nil'5(0) ⇔ nil'
_gen_cons':nil'5(+(x, 1)) ⇔ cons'(0', _gen_cons':nil'5(x))
The following defined symbols remain to be analysed:
shorter', prod'
They will be analysed ascendingly in the following order:
shorter' < prod'
Proved the following rewrite lemma:
shorter'(_gen_cons':nil'5(_n7220), _gen_0':s'4(_n7220)) → true', rt ∈ Ω(1 + n7220)
Induction Base:
shorter'(_gen_cons':nil'5(0), _gen_0':s'4(0)) →RΩ(1)
true'
Induction Step:
shorter'(_gen_cons':nil'5(+(_$n7221, 1)), _gen_0':s'4(+(_$n7221, 1))) →RΩ(1)
shorter'(_gen_cons':nil'5(_$n7221), _gen_0':s'4(_$n7221)) →IH
true'
We have rt ∈ Ω(n) and sz ∈ O(n). Thus, we have ircR ∈ Ω(n).
Rules:
car'(cons'(x, l)) → x
cddr'(nil') → nil'
cddr'(cons'(x, nil')) → nil'
cddr'(cons'(x, cons'(y, l))) → l
cadr'(cons'(x, cons'(y, l))) → y
isZero'(0') → true'
isZero'(s'(x)) → false'
plus'(x, y) → ifplus'(isZero'(x), x, y)
ifplus'(true', x, y) → y
ifplus'(false', x, y) → s'(plus'(p'(x), y))
times'(x, y) → iftimes'(isZero'(x), x, y)
iftimes'(true', x, y) → 0'
iftimes'(false', x, y) → plus'(y, times'(p'(x), y))
p'(s'(x)) → x
p'(0') → 0'
shorter'(nil', y) → true'
shorter'(cons'(x, l), 0') → false'
shorter'(cons'(x, l), s'(y)) → shorter'(l, y)
prod'(l) → if'(shorter'(l, 0'), shorter'(l, s'(0')), l)
if'(true', b, l) → s'(0')
if'(false', b, l) → if2'(b, l)
if2'(true', l) → car'(l)
if2'(false', l) → prod'(cons'(times'(car'(l), cadr'(l)), cddr'(l)))
Types:
car' :: cons':nil' → 0':s'
cons' :: 0':s' → cons':nil' → cons':nil'
cddr' :: cons':nil' → cons':nil'
nil' :: cons':nil'
cadr' :: cons':nil' → 0':s'
isZero' :: 0':s' → true':false'
0' :: 0':s'
true' :: true':false'
s' :: 0':s' → 0':s'
false' :: true':false'
plus' :: 0':s' → 0':s' → 0':s'
ifplus' :: true':false' → 0':s' → 0':s' → 0':s'
p' :: 0':s' → 0':s'
times' :: 0':s' → 0':s' → 0':s'
iftimes' :: true':false' → 0':s' → 0':s' → 0':s'
shorter' :: cons':nil' → 0':s' → true':false'
prod' :: cons':nil' → 0':s'
if' :: true':false' → true':false' → cons':nil' → 0':s'
if2' :: true':false' → cons':nil' → 0':s'
_hole_0':s'1 :: 0':s'
_hole_cons':nil'2 :: cons':nil'
_hole_true':false'3 :: true':false'
_gen_0':s'4 :: Nat → 0':s'
_gen_cons':nil'5 :: Nat → cons':nil'
Lemmas:
plus'(_gen_0':s'4(_n7), _gen_0':s'4(b)) → _gen_0':s'4(+(_n7, b)), rt ∈ Ω(1 + n7)
times'(_gen_0':s'4(_n3005), _gen_0':s'4(b)) → _gen_0':s'4(*(_n3005, b)), rt ∈ Ω(1 + b3630·n3005 + n3005)
shorter'(_gen_cons':nil'5(_n7220), _gen_0':s'4(_n7220)) → true', rt ∈ Ω(1 + n7220)
Generator Equations:
_gen_0':s'4(0) ⇔ 0'
_gen_0':s'4(+(x, 1)) ⇔ s'(_gen_0':s'4(x))
_gen_cons':nil'5(0) ⇔ nil'
_gen_cons':nil'5(+(x, 1)) ⇔ cons'(0', _gen_cons':nil'5(x))
The following defined symbols remain to be analysed:
prod'
Could not prove a rewrite lemma for the defined symbol prod'.
Rules:
car'(cons'(x, l)) → x
cddr'(nil') → nil'
cddr'(cons'(x, nil')) → nil'
cddr'(cons'(x, cons'(y, l))) → l
cadr'(cons'(x, cons'(y, l))) → y
isZero'(0') → true'
isZero'(s'(x)) → false'
plus'(x, y) → ifplus'(isZero'(x), x, y)
ifplus'(true', x, y) → y
ifplus'(false', x, y) → s'(plus'(p'(x), y))
times'(x, y) → iftimes'(isZero'(x), x, y)
iftimes'(true', x, y) → 0'
iftimes'(false', x, y) → plus'(y, times'(p'(x), y))
p'(s'(x)) → x
p'(0') → 0'
shorter'(nil', y) → true'
shorter'(cons'(x, l), 0') → false'
shorter'(cons'(x, l), s'(y)) → shorter'(l, y)
prod'(l) → if'(shorter'(l, 0'), shorter'(l, s'(0')), l)
if'(true', b, l) → s'(0')
if'(false', b, l) → if2'(b, l)
if2'(true', l) → car'(l)
if2'(false', l) → prod'(cons'(times'(car'(l), cadr'(l)), cddr'(l)))
Types:
car' :: cons':nil' → 0':s'
cons' :: 0':s' → cons':nil' → cons':nil'
cddr' :: cons':nil' → cons':nil'
nil' :: cons':nil'
cadr' :: cons':nil' → 0':s'
isZero' :: 0':s' → true':false'
0' :: 0':s'
true' :: true':false'
s' :: 0':s' → 0':s'
false' :: true':false'
plus' :: 0':s' → 0':s' → 0':s'
ifplus' :: true':false' → 0':s' → 0':s' → 0':s'
p' :: 0':s' → 0':s'
times' :: 0':s' → 0':s' → 0':s'
iftimes' :: true':false' → 0':s' → 0':s' → 0':s'
shorter' :: cons':nil' → 0':s' → true':false'
prod' :: cons':nil' → 0':s'
if' :: true':false' → true':false' → cons':nil' → 0':s'
if2' :: true':false' → cons':nil' → 0':s'
_hole_0':s'1 :: 0':s'
_hole_cons':nil'2 :: cons':nil'
_hole_true':false'3 :: true':false'
_gen_0':s'4 :: Nat → 0':s'
_gen_cons':nil'5 :: Nat → cons':nil'
Lemmas:
plus'(_gen_0':s'4(_n7), _gen_0':s'4(b)) → _gen_0':s'4(+(_n7, b)), rt ∈ Ω(1 + n7)
times'(_gen_0':s'4(_n3005), _gen_0':s'4(b)) → _gen_0':s'4(*(_n3005, b)), rt ∈ Ω(1 + b3630·n3005 + n3005)
shorter'(_gen_cons':nil'5(_n7220), _gen_0':s'4(_n7220)) → true', rt ∈ Ω(1 + n7220)
Generator Equations:
_gen_0':s'4(0) ⇔ 0'
_gen_0':s'4(+(x, 1)) ⇔ s'(_gen_0':s'4(x))
_gen_cons':nil'5(0) ⇔ nil'
_gen_cons':nil'5(+(x, 1)) ⇔ cons'(0', _gen_cons':nil'5(x))
No more defined symbols left to analyse.
The lowerbound Ω(n2) was proven with the following lemma:
times'(_gen_0':s'4(_n3005), _gen_0':s'4(b)) → _gen_0':s'4(*(_n3005, b)), rt ∈ Ω(1 + b3630·n3005 + n3005)