empty(nil) → true
empty(cons(x, y)) → false
tail(nil) → nil
tail(cons(x, y)) → y
head(cons(x, y)) → x
zero(0) → true
zero(s(x)) → false
p(0) → 0
p(s(0)) → 0
p(s(s(x))) → s(p(s(x)))
intlist(x) → if_intlist(empty(x), x)
if_intlist(true, x) → nil
if_intlist(false, x) → cons(s(head(x)), intlist(tail(x)))
int(x, y) → if_int(zero(x), zero(y), x, y)
if_int(true, b, x, y) → if1(b, x, y)
if_int(false, b, x, y) → if2(b, x, y)
if1(true, x, y) → cons(0, nil)
if1(false, x, y) → cons(0, int(s(0), y))
if2(true, x, y) → nil
if2(false, x, y) → intlist(int(p(x), p(y)))
Renamed function symbols to avoid clashes with predefined symbol.
Runtime Complexity TRS:
The TRS R consists of the following rules:
empty'(nil') → true'
empty'(cons'(x, y)) → false'
tail'(nil') → nil'
tail'(cons'(x, y)) → y
head'(cons'(x, y)) → x
zero'(0') → true'
zero'(s'(x)) → false'
p'(0') → 0'
p'(s'(0')) → 0'
p'(s'(s'(x))) → s'(p'(s'(x)))
intlist'(x) → if_intlist'(empty'(x), x)
if_intlist'(true', x) → nil'
if_intlist'(false', x) → cons'(s'(head'(x)), intlist'(tail'(x)))
int'(x, y) → if_int'(zero'(x), zero'(y), x, y)
if_int'(true', b, x, y) → if1'(b, x, y)
if_int'(false', b, x, y) → if2'(b, x, y)
if1'(true', x, y) → cons'(0', nil')
if1'(false', x, y) → cons'(0', int'(s'(0'), y))
if2'(true', x, y) → nil'
if2'(false', x, y) → intlist'(int'(p'(x), p'(y)))
Sliced the following arguments:
if1'/1
Runtime Complexity TRS:
The TRS R consists of the following rules:
empty'(nil') → true'
empty'(cons'(x, y)) → false'
tail'(nil') → nil'
tail'(cons'(x, y)) → y
head'(cons'(x, y)) → x
zero'(0') → true'
zero'(s'(x)) → false'
p'(0') → 0'
p'(s'(0')) → 0'
p'(s'(s'(x))) → s'(p'(s'(x)))
intlist'(x) → if_intlist'(empty'(x), x)
if_intlist'(true', x) → nil'
if_intlist'(false', x) → cons'(s'(head'(x)), intlist'(tail'(x)))
int'(x, y) → if_int'(zero'(x), zero'(y), x, y)
if_int'(true', b, x, y) → if1'(b, y)
if_int'(false', b, x, y) → if2'(b, x, y)
if1'(true', y) → cons'(0', nil')
if1'(false', y) → cons'(0', int'(s'(0'), y))
if2'(true', x, y) → nil'
if2'(false', x, y) → intlist'(int'(p'(x), p'(y)))
Infered types.
Rules:
empty'(nil') → true'
empty'(cons'(x, y)) → false'
tail'(nil') → nil'
tail'(cons'(x, y)) → y
head'(cons'(x, y)) → x
zero'(0') → true'
zero'(s'(x)) → false'
p'(0') → 0'
p'(s'(0')) → 0'
p'(s'(s'(x))) → s'(p'(s'(x)))
intlist'(x) → if_intlist'(empty'(x), x)
if_intlist'(true', x) → nil'
if_intlist'(false', x) → cons'(s'(head'(x)), intlist'(tail'(x)))
int'(x, y) → if_int'(zero'(x), zero'(y), x, y)
if_int'(true', b, x, y) → if1'(b, y)
if_int'(false', b, x, y) → if2'(b, x, y)
if1'(true', y) → cons'(0', nil')
if1'(false', y) → cons'(0', int'(s'(0'), y))
if2'(true', x, y) → nil'
if2'(false', x, y) → intlist'(int'(p'(x), p'(y)))
Types:
empty' :: nil':cons' → true':false'
nil' :: nil':cons'
true' :: true':false'
cons' :: 0':s' → nil':cons' → nil':cons'
false' :: true':false'
tail' :: nil':cons' → nil':cons'
head' :: nil':cons' → 0':s'
zero' :: 0':s' → true':false'
0' :: 0':s'
s' :: 0':s' → 0':s'
p' :: 0':s' → 0':s'
intlist' :: nil':cons' → nil':cons'
if_intlist' :: true':false' → nil':cons' → nil':cons'
int' :: 0':s' → 0':s' → nil':cons'
if_int' :: true':false' → true':false' → 0':s' → 0':s' → nil':cons'
if1' :: true':false' → 0':s' → nil':cons'
if2' :: true':false' → 0':s' → 0':s' → nil':cons'
_hole_true':false'1 :: true':false'
_hole_nil':cons'2 :: nil':cons'
_hole_0':s'3 :: 0':s'
_gen_nil':cons'4 :: Nat → nil':cons'
_gen_0':s'5 :: Nat → 0':s'
Heuristically decided to analyse the following defined symbols:
p', intlist', int', if1'
They will be analysed ascendingly in the following order:
p' < int'
intlist' < int'
int' = if1'
Rules:
empty'(nil') → true'
empty'(cons'(x, y)) → false'
tail'(nil') → nil'
tail'(cons'(x, y)) → y
head'(cons'(x, y)) → x
zero'(0') → true'
zero'(s'(x)) → false'
p'(0') → 0'
p'(s'(0')) → 0'
p'(s'(s'(x))) → s'(p'(s'(x)))
intlist'(x) → if_intlist'(empty'(x), x)
if_intlist'(true', x) → nil'
if_intlist'(false', x) → cons'(s'(head'(x)), intlist'(tail'(x)))
int'(x, y) → if_int'(zero'(x), zero'(y), x, y)
if_int'(true', b, x, y) → if1'(b, y)
if_int'(false', b, x, y) → if2'(b, x, y)
if1'(true', y) → cons'(0', nil')
if1'(false', y) → cons'(0', int'(s'(0'), y))
if2'(true', x, y) → nil'
if2'(false', x, y) → intlist'(int'(p'(x), p'(y)))
Types:
empty' :: nil':cons' → true':false'
nil' :: nil':cons'
true' :: true':false'
cons' :: 0':s' → nil':cons' → nil':cons'
false' :: true':false'
tail' :: nil':cons' → nil':cons'
head' :: nil':cons' → 0':s'
zero' :: 0':s' → true':false'
0' :: 0':s'
s' :: 0':s' → 0':s'
p' :: 0':s' → 0':s'
intlist' :: nil':cons' → nil':cons'
if_intlist' :: true':false' → nil':cons' → nil':cons'
int' :: 0':s' → 0':s' → nil':cons'
if_int' :: true':false' → true':false' → 0':s' → 0':s' → nil':cons'
if1' :: true':false' → 0':s' → nil':cons'
if2' :: true':false' → 0':s' → 0':s' → nil':cons'
_hole_true':false'1 :: true':false'
_hole_nil':cons'2 :: nil':cons'
_hole_0':s'3 :: 0':s'
_gen_nil':cons'4 :: Nat → nil':cons'
_gen_0':s'5 :: Nat → 0':s'
Generator Equations:
_gen_nil':cons'4(0) ⇔ nil'
_gen_nil':cons'4(+(x, 1)) ⇔ cons'(0', _gen_nil':cons'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', intlist', int', if1'
They will be analysed ascendingly in the following order:
p' < int'
intlist' < int'
int' = if1'
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:
empty'(nil') → true'
empty'(cons'(x, y)) → false'
tail'(nil') → nil'
tail'(cons'(x, y)) → y
head'(cons'(x, y)) → x
zero'(0') → true'
zero'(s'(x)) → false'
p'(0') → 0'
p'(s'(0')) → 0'
p'(s'(s'(x))) → s'(p'(s'(x)))
intlist'(x) → if_intlist'(empty'(x), x)
if_intlist'(true', x) → nil'
if_intlist'(false', x) → cons'(s'(head'(x)), intlist'(tail'(x)))
int'(x, y) → if_int'(zero'(x), zero'(y), x, y)
if_int'(true', b, x, y) → if1'(b, y)
if_int'(false', b, x, y) → if2'(b, x, y)
if1'(true', y) → cons'(0', nil')
if1'(false', y) → cons'(0', int'(s'(0'), y))
if2'(true', x, y) → nil'
if2'(false', x, y) → intlist'(int'(p'(x), p'(y)))
Types:
empty' :: nil':cons' → true':false'
nil' :: nil':cons'
true' :: true':false'
cons' :: 0':s' → nil':cons' → nil':cons'
false' :: true':false'
tail' :: nil':cons' → nil':cons'
head' :: nil':cons' → 0':s'
zero' :: 0':s' → true':false'
0' :: 0':s'
s' :: 0':s' → 0':s'
p' :: 0':s' → 0':s'
intlist' :: nil':cons' → nil':cons'
if_intlist' :: true':false' → nil':cons' → nil':cons'
int' :: 0':s' → 0':s' → nil':cons'
if_int' :: true':false' → true':false' → 0':s' → 0':s' → nil':cons'
if1' :: true':false' → 0':s' → nil':cons'
if2' :: true':false' → 0':s' → 0':s' → nil':cons'
_hole_true':false'1 :: true':false'
_hole_nil':cons'2 :: nil':cons'
_hole_0':s'3 :: 0':s'
_gen_nil':cons'4 :: Nat → nil':cons'
_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_nil':cons'4(0) ⇔ nil'
_gen_nil':cons'4(+(x, 1)) ⇔ cons'(0', _gen_nil':cons'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:
intlist', int', if1'
They will be analysed ascendingly in the following order:
intlist' < int'
int' = if1'
Proved the following rewrite lemma:
intlist'(_gen_nil':cons'4(_n734)) → _*6, rt ∈ Ω(n734)
Induction Base:
intlist'(_gen_nil':cons'4(0))
Induction Step:
intlist'(_gen_nil':cons'4(+(_$n735, 1))) →RΩ(1)
if_intlist'(empty'(_gen_nil':cons'4(+(_$n735, 1))), _gen_nil':cons'4(+(_$n735, 1))) →RΩ(1)
if_intlist'(false', _gen_nil':cons'4(+(1, _$n735))) →RΩ(1)
cons'(s'(head'(_gen_nil':cons'4(+(1, _$n735)))), intlist'(tail'(_gen_nil':cons'4(+(1, _$n735))))) →RΩ(1)
cons'(s'(0'), intlist'(tail'(_gen_nil':cons'4(+(1, _$n735))))) →RΩ(1)
cons'(s'(0'), intlist'(_gen_nil':cons'4(_$n735))) →IH
cons'(s'(0'), _*6)
We have rt ∈ Ω(n) and sz ∈ O(n). Thus, we have ircR ∈ Ω(n).
Rules:
empty'(nil') → true'
empty'(cons'(x, y)) → false'
tail'(nil') → nil'
tail'(cons'(x, y)) → y
head'(cons'(x, y)) → x
zero'(0') → true'
zero'(s'(x)) → false'
p'(0') → 0'
p'(s'(0')) → 0'
p'(s'(s'(x))) → s'(p'(s'(x)))
intlist'(x) → if_intlist'(empty'(x), x)
if_intlist'(true', x) → nil'
if_intlist'(false', x) → cons'(s'(head'(x)), intlist'(tail'(x)))
int'(x, y) → if_int'(zero'(x), zero'(y), x, y)
if_int'(true', b, x, y) → if1'(b, y)
if_int'(false', b, x, y) → if2'(b, x, y)
if1'(true', y) → cons'(0', nil')
if1'(false', y) → cons'(0', int'(s'(0'), y))
if2'(true', x, y) → nil'
if2'(false', x, y) → intlist'(int'(p'(x), p'(y)))
Types:
empty' :: nil':cons' → true':false'
nil' :: nil':cons'
true' :: true':false'
cons' :: 0':s' → nil':cons' → nil':cons'
false' :: true':false'
tail' :: nil':cons' → nil':cons'
head' :: nil':cons' → 0':s'
zero' :: 0':s' → true':false'
0' :: 0':s'
s' :: 0':s' → 0':s'
p' :: 0':s' → 0':s'
intlist' :: nil':cons' → nil':cons'
if_intlist' :: true':false' → nil':cons' → nil':cons'
int' :: 0':s' → 0':s' → nil':cons'
if_int' :: true':false' → true':false' → 0':s' → 0':s' → nil':cons'
if1' :: true':false' → 0':s' → nil':cons'
if2' :: true':false' → 0':s' → 0':s' → nil':cons'
_hole_true':false'1 :: true':false'
_hole_nil':cons'2 :: nil':cons'
_hole_0':s'3 :: 0':s'
_gen_nil':cons'4 :: Nat → nil':cons'
_gen_0':s'5 :: Nat → 0':s'
Lemmas:
p'(_gen_0':s'5(+(1, _n7))) → _gen_0':s'5(_n7), rt ∈ Ω(1 + n7)
intlist'(_gen_nil':cons'4(_n734)) → _*6, rt ∈ Ω(n734)
Generator Equations:
_gen_nil':cons'4(0) ⇔ nil'
_gen_nil':cons'4(+(x, 1)) ⇔ cons'(0', _gen_nil':cons'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:
if1', int'
They will be analysed ascendingly in the following order:
int' = if1'
Could not prove a rewrite lemma for the defined symbol if1'.
Rules:
empty'(nil') → true'
empty'(cons'(x, y)) → false'
tail'(nil') → nil'
tail'(cons'(x, y)) → y
head'(cons'(x, y)) → x
zero'(0') → true'
zero'(s'(x)) → false'
p'(0') → 0'
p'(s'(0')) → 0'
p'(s'(s'(x))) → s'(p'(s'(x)))
intlist'(x) → if_intlist'(empty'(x), x)
if_intlist'(true', x) → nil'
if_intlist'(false', x) → cons'(s'(head'(x)), intlist'(tail'(x)))
int'(x, y) → if_int'(zero'(x), zero'(y), x, y)
if_int'(true', b, x, y) → if1'(b, y)
if_int'(false', b, x, y) → if2'(b, x, y)
if1'(true', y) → cons'(0', nil')
if1'(false', y) → cons'(0', int'(s'(0'), y))
if2'(true', x, y) → nil'
if2'(false', x, y) → intlist'(int'(p'(x), p'(y)))
Types:
empty' :: nil':cons' → true':false'
nil' :: nil':cons'
true' :: true':false'
cons' :: 0':s' → nil':cons' → nil':cons'
false' :: true':false'
tail' :: nil':cons' → nil':cons'
head' :: nil':cons' → 0':s'
zero' :: 0':s' → true':false'
0' :: 0':s'
s' :: 0':s' → 0':s'
p' :: 0':s' → 0':s'
intlist' :: nil':cons' → nil':cons'
if_intlist' :: true':false' → nil':cons' → nil':cons'
int' :: 0':s' → 0':s' → nil':cons'
if_int' :: true':false' → true':false' → 0':s' → 0':s' → nil':cons'
if1' :: true':false' → 0':s' → nil':cons'
if2' :: true':false' → 0':s' → 0':s' → nil':cons'
_hole_true':false'1 :: true':false'
_hole_nil':cons'2 :: nil':cons'
_hole_0':s'3 :: 0':s'
_gen_nil':cons'4 :: Nat → nil':cons'
_gen_0':s'5 :: Nat → 0':s'
Lemmas:
p'(_gen_0':s'5(+(1, _n7))) → _gen_0':s'5(_n7), rt ∈ Ω(1 + n7)
intlist'(_gen_nil':cons'4(_n734)) → _*6, rt ∈ Ω(n734)
Generator Equations:
_gen_nil':cons'4(0) ⇔ nil'
_gen_nil':cons'4(+(x, 1)) ⇔ cons'(0', _gen_nil':cons'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:
int'
They will be analysed ascendingly in the following order:
int' = if1'
Proved the following rewrite lemma:
int'(_gen_0':s'5(+(1, _n204008)), _gen_0':s'5(_n204008)) → _gen_nil':cons'4(0), rt ∈ Ω(1 + n204008 + n2040082)
Induction Base:
int'(_gen_0':s'5(+(1, 0)), _gen_0':s'5(0)) →RΩ(1)
if_int'(zero'(_gen_0':s'5(+(1, 0))), zero'(_gen_0':s'5(0)), _gen_0':s'5(+(1, 0)), _gen_0':s'5(0)) →RΩ(1)
if_int'(false', zero'(_gen_0':s'5(0)), _gen_0':s'5(1), _gen_0':s'5(0)) →RΩ(1)
if_int'(false', true', _gen_0':s'5(1), _gen_0':s'5(0)) →RΩ(1)
if2'(true', _gen_0':s'5(1), _gen_0':s'5(0)) →RΩ(1)
nil'
Induction Step:
int'(_gen_0':s'5(+(1, +(_$n204009, 1))), _gen_0':s'5(+(_$n204009, 1))) →RΩ(1)
if_int'(zero'(_gen_0':s'5(+(1, +(_$n204009, 1)))), zero'(_gen_0':s'5(+(_$n204009, 1))), _gen_0':s'5(+(1, +(_$n204009, 1))), _gen_0':s'5(+(_$n204009, 1))) →RΩ(1)
if_int'(false', zero'(_gen_0':s'5(+(1, _$n204009))), _gen_0':s'5(+(2, _$n204009)), _gen_0':s'5(+(1, _$n204009))) →RΩ(1)
if_int'(false', false', _gen_0':s'5(+(2, _$n204009)), _gen_0':s'5(+(1, _$n204009))) →RΩ(1)
if2'(false', _gen_0':s'5(+(2, _$n204009)), _gen_0':s'5(+(1, _$n204009))) →RΩ(1)
intlist'(int'(p'(_gen_0':s'5(+(2, _$n204009))), p'(_gen_0':s'5(+(1, _$n204009))))) →LΩ(2 + $n204009)
intlist'(int'(_gen_0':s'5(+(1, _$n204009)), p'(_gen_0':s'5(+(1, _$n204009))))) →LΩ(1 + $n204009)
intlist'(int'(_gen_0':s'5(+(1, _$n204009)), _gen_0':s'5(_$n204009))) →IH
intlist'(_gen_nil':cons'4(0)) →RΩ(1)
if_intlist'(empty'(_gen_nil':cons'4(0)), _gen_nil':cons'4(0)) →RΩ(1)
if_intlist'(true', _gen_nil':cons'4(0)) →RΩ(1)
nil'
We have rt ∈ Ω(n2) and sz ∈ O(n). Thus, we have ircR ∈ Ω(n2).
Rules:
empty'(nil') → true'
empty'(cons'(x, y)) → false'
tail'(nil') → nil'
tail'(cons'(x, y)) → y
head'(cons'(x, y)) → x
zero'(0') → true'
zero'(s'(x)) → false'
p'(0') → 0'
p'(s'(0')) → 0'
p'(s'(s'(x))) → s'(p'(s'(x)))
intlist'(x) → if_intlist'(empty'(x), x)
if_intlist'(true', x) → nil'
if_intlist'(false', x) → cons'(s'(head'(x)), intlist'(tail'(x)))
int'(x, y) → if_int'(zero'(x), zero'(y), x, y)
if_int'(true', b, x, y) → if1'(b, y)
if_int'(false', b, x, y) → if2'(b, x, y)
if1'(true', y) → cons'(0', nil')
if1'(false', y) → cons'(0', int'(s'(0'), y))
if2'(true', x, y) → nil'
if2'(false', x, y) → intlist'(int'(p'(x), p'(y)))
Types:
empty' :: nil':cons' → true':false'
nil' :: nil':cons'
true' :: true':false'
cons' :: 0':s' → nil':cons' → nil':cons'
false' :: true':false'
tail' :: nil':cons' → nil':cons'
head' :: nil':cons' → 0':s'
zero' :: 0':s' → true':false'
0' :: 0':s'
s' :: 0':s' → 0':s'
p' :: 0':s' → 0':s'
intlist' :: nil':cons' → nil':cons'
if_intlist' :: true':false' → nil':cons' → nil':cons'
int' :: 0':s' → 0':s' → nil':cons'
if_int' :: true':false' → true':false' → 0':s' → 0':s' → nil':cons'
if1' :: true':false' → 0':s' → nil':cons'
if2' :: true':false' → 0':s' → 0':s' → nil':cons'
_hole_true':false'1 :: true':false'
_hole_nil':cons'2 :: nil':cons'
_hole_0':s'3 :: 0':s'
_gen_nil':cons'4 :: Nat → nil':cons'
_gen_0':s'5 :: Nat → 0':s'
Lemmas:
p'(_gen_0':s'5(+(1, _n7))) → _gen_0':s'5(_n7), rt ∈ Ω(1 + n7)
intlist'(_gen_nil':cons'4(_n734)) → _*6, rt ∈ Ω(n734)
int'(_gen_0':s'5(+(1, _n204008)), _gen_0':s'5(_n204008)) → _gen_nil':cons'4(0), rt ∈ Ω(1 + n204008 + n2040082)
Generator Equations:
_gen_nil':cons'4(0) ⇔ nil'
_gen_nil':cons'4(+(x, 1)) ⇔ cons'(0', _gen_nil':cons'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:
if1'
They will be analysed ascendingly in the following order:
int' = if1'
Could not prove a rewrite lemma for the defined symbol if1'.
Rules:
empty'(nil') → true'
empty'(cons'(x, y)) → false'
tail'(nil') → nil'
tail'(cons'(x, y)) → y
head'(cons'(x, y)) → x
zero'(0') → true'
zero'(s'(x)) → false'
p'(0') → 0'
p'(s'(0')) → 0'
p'(s'(s'(x))) → s'(p'(s'(x)))
intlist'(x) → if_intlist'(empty'(x), x)
if_intlist'(true', x) → nil'
if_intlist'(false', x) → cons'(s'(head'(x)), intlist'(tail'(x)))
int'(x, y) → if_int'(zero'(x), zero'(y), x, y)
if_int'(true', b, x, y) → if1'(b, y)
if_int'(false', b, x, y) → if2'(b, x, y)
if1'(true', y) → cons'(0', nil')
if1'(false', y) → cons'(0', int'(s'(0'), y))
if2'(true', x, y) → nil'
if2'(false', x, y) → intlist'(int'(p'(x), p'(y)))
Types:
empty' :: nil':cons' → true':false'
nil' :: nil':cons'
true' :: true':false'
cons' :: 0':s' → nil':cons' → nil':cons'
false' :: true':false'
tail' :: nil':cons' → nil':cons'
head' :: nil':cons' → 0':s'
zero' :: 0':s' → true':false'
0' :: 0':s'
s' :: 0':s' → 0':s'
p' :: 0':s' → 0':s'
intlist' :: nil':cons' → nil':cons'
if_intlist' :: true':false' → nil':cons' → nil':cons'
int' :: 0':s' → 0':s' → nil':cons'
if_int' :: true':false' → true':false' → 0':s' → 0':s' → nil':cons'
if1' :: true':false' → 0':s' → nil':cons'
if2' :: true':false' → 0':s' → 0':s' → nil':cons'
_hole_true':false'1 :: true':false'
_hole_nil':cons'2 :: nil':cons'
_hole_0':s'3 :: 0':s'
_gen_nil':cons'4 :: Nat → nil':cons'
_gen_0':s'5 :: Nat → 0':s'
Lemmas:
p'(_gen_0':s'5(+(1, _n7))) → _gen_0':s'5(_n7), rt ∈ Ω(1 + n7)
intlist'(_gen_nil':cons'4(_n734)) → _*6, rt ∈ Ω(n734)
int'(_gen_0':s'5(+(1, _n204008)), _gen_0':s'5(_n204008)) → _gen_nil':cons'4(0), rt ∈ Ω(1 + n204008 + n2040082)
Generator Equations:
_gen_nil':cons'4(0) ⇔ nil'
_gen_nil':cons'4(+(x, 1)) ⇔ cons'(0', _gen_nil':cons'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:
int'(_gen_0':s'5(+(1, _n204008)), _gen_0':s'5(_n204008)) → _gen_nil':cons'4(0), rt ∈ Ω(1 + n204008 + n2040082)