Runtime Complexity TRS:
The TRS R consists of the following rules:

eq(0, 0) → true
eq(0, s(y)) → false
eq(s(x), 0) → false
eq(s(x), s(y)) → eq(x, y)
lt(0, s(y)) → true
lt(x, 0) → false
lt(s(x), s(y)) → lt(x, y)
bin2s(nil) → 0
bin2s(cons(x, xs)) → bin2ss(x, xs)
bin2ss(x, nil) → x
bin2ss(x, cons(0, xs)) → bin2ss(double(x), xs)
bin2ss(x, cons(1, xs)) → bin2ss(s(double(x)), xs)
half(0) → 0
half(s(0)) → 0
half(s(s(x))) → s(half(x))
log(0) → 0
log(s(0)) → 0
log(s(s(x))) → s(log(half(s(s(x)))))
more(nil) → nil
more(cons(xs, ys)) → cons(cons(0, xs), cons(cons(1, xs), cons(xs, ys)))
s2bin(x) → s2bin1(x, 0, cons(nil, nil))
s2bin1(x, y, lists) → if1(lt(y, log(x)), x, y, lists)
if1(true, x, y, lists) → s2bin1(x, s(y), more(lists))
if1(false, x, y, lists) → s2bin2(x, lists)
s2bin2(x, nil) → bug_list_not
s2bin2(x, cons(xs, ys)) → if2(eq(x, bin2s(xs)), x, xs, ys)
if2(true, x, xs, ys) → xs
if2(false, x, xs, ys) → s2bin2(x, ys)

Rewrite Strategy: INNERMOST

Renamed function symbols to avoid clashes with predefined symbol.

Runtime Complexity TRS:
The TRS R consists of the following rules:


eq'(0', 0') → true'
eq'(0', s'(y)) → false'
eq'(s'(x), 0') → false'
eq'(s'(x), s'(y)) → eq'(x, y)
lt'(0', s'(y)) → true'
lt'(x, 0') → false'
lt'(s'(x), s'(y)) → lt'(x, y)
bin2s'(nil') → 0'
bin2s'(cons'(x, xs)) → bin2ss'(x, xs)
bin2ss'(x, nil') → x
bin2ss'(x, cons'(0', xs)) → bin2ss'(double'(x), xs)
bin2ss'(x, cons'(1', xs)) → bin2ss'(s'(double'(x)), xs)
half'(0') → 0'
half'(s'(0')) → 0'
half'(s'(s'(x))) → s'(half'(x))
log'(0') → 0'
log'(s'(0')) → 0'
log'(s'(s'(x))) → s'(log'(half'(s'(s'(x)))))
more'(nil') → nil'
more'(cons'(xs, ys)) → cons'(cons'(0', xs), cons'(cons'(1', xs), cons'(xs, ys)))
s2bin'(x) → s2bin1'(x, 0', cons'(nil', nil'))
s2bin1'(x, y, lists) → if1'(lt'(y, log'(x)), x, y, lists)
if1'(true', x, y, lists) → s2bin1'(x, s'(y), more'(lists))
if1'(false', x, y, lists) → s2bin2'(x, lists)
s2bin2'(x, nil') → bug_list_not'
s2bin2'(x, cons'(xs, ys)) → if2'(eq'(x, bin2s'(xs)), x, xs, ys)
if2'(true', x, xs, ys) → xs
if2'(false', x, xs, ys) → s2bin2'(x, ys)

Rewrite Strategy: INNERMOST

Sliced the following arguments:
double'/0

Runtime Complexity TRS:
The TRS R consists of the following rules:


eq'(0', 0') → true'
eq'(0', s'(y)) → false'
eq'(s'(x), 0') → false'
eq'(s'(x), s'(y)) → eq'(x, y)
lt'(0', s'(y)) → true'
lt'(x, 0') → false'
lt'(s'(x), s'(y)) → lt'(x, y)
bin2s'(nil') → 0'
bin2s'(cons'(x, xs)) → bin2ss'(x, xs)
bin2ss'(x, nil') → x
bin2ss'(x, cons'(0', xs)) → bin2ss'(double', xs)
bin2ss'(x, cons'(1', xs)) → bin2ss'(s'(double'), xs)
half'(0') → 0'
half'(s'(0')) → 0'
half'(s'(s'(x))) → s'(half'(x))
log'(0') → 0'
log'(s'(0')) → 0'
log'(s'(s'(x))) → s'(log'(half'(s'(s'(x)))))
more'(nil') → nil'
more'(cons'(xs, ys)) → cons'(cons'(0', xs), cons'(cons'(1', xs), cons'(xs, ys)))
s2bin'(x) → s2bin1'(x, 0', cons'(nil', nil'))
s2bin1'(x, y, lists) → if1'(lt'(y, log'(x)), x, y, lists)
if1'(true', x, y, lists) → s2bin1'(x, s'(y), more'(lists))
if1'(false', x, y, lists) → s2bin2'(x, lists)
s2bin2'(x, nil') → bug_list_not'
s2bin2'(x, cons'(xs, ys)) → if2'(eq'(x, bin2s'(xs)), x, xs, ys)
if2'(true', x, xs, ys) → xs
if2'(false', x, xs, ys) → s2bin2'(x, ys)

Rewrite Strategy: INNERMOST

Infered types.

Rules:
eq'(0', 0') → true'
eq'(0', s'(y)) → false'
eq'(s'(x), 0') → false'
eq'(s'(x), s'(y)) → eq'(x, y)
lt'(0', s'(y)) → true'
lt'(x, 0') → false'
lt'(s'(x), s'(y)) → lt'(x, y)
bin2s'(nil') → 0'
bin2s'(cons'(x, xs)) → bin2ss'(x, xs)
bin2ss'(x, nil') → x
bin2ss'(x, cons'(0', xs)) → bin2ss'(double', xs)
bin2ss'(x, cons'(1', xs)) → bin2ss'(s'(double'), xs)
half'(0') → 0'
half'(s'(0')) → 0'
half'(s'(s'(x))) → s'(half'(x))
log'(0') → 0'
log'(s'(0')) → 0'
log'(s'(s'(x))) → s'(log'(half'(s'(s'(x)))))
more'(nil') → nil'
more'(cons'(xs, ys)) → cons'(cons'(0', xs), cons'(cons'(1', xs), cons'(xs, ys)))
s2bin'(x) → s2bin1'(x, 0', cons'(nil', nil'))
s2bin1'(x, y, lists) → if1'(lt'(y, log'(x)), x, y, lists)
if1'(true', x, y, lists) → s2bin1'(x, s'(y), more'(lists))
if1'(false', x, y, lists) → s2bin2'(x, lists)
s2bin2'(x, nil') → bug_list_not'
s2bin2'(x, cons'(xs, ys)) → if2'(eq'(x, bin2s'(xs)), x, xs, ys)
if2'(true', x, xs, ys) → xs
if2'(false', x, xs, ys) → s2bin2'(x, ys)

Types:
eq' :: 0':s':nil':cons':double':1':bug_list_not' → 0':s':nil':cons':double':1':bug_list_not' → true':false'
0' :: 0':s':nil':cons':double':1':bug_list_not'
true' :: true':false'
s' :: 0':s':nil':cons':double':1':bug_list_not' → 0':s':nil':cons':double':1':bug_list_not'
false' :: true':false'
lt' :: 0':s':nil':cons':double':1':bug_list_not' → 0':s':nil':cons':double':1':bug_list_not' → true':false'
bin2s' :: 0':s':nil':cons':double':1':bug_list_not' → 0':s':nil':cons':double':1':bug_list_not'
nil' :: 0':s':nil':cons':double':1':bug_list_not'
cons' :: 0':s':nil':cons':double':1':bug_list_not' → 0':s':nil':cons':double':1':bug_list_not' → 0':s':nil':cons':double':1':bug_list_not'
bin2ss' :: 0':s':nil':cons':double':1':bug_list_not' → 0':s':nil':cons':double':1':bug_list_not' → 0':s':nil':cons':double':1':bug_list_not'
double' :: 0':s':nil':cons':double':1':bug_list_not'
1' :: 0':s':nil':cons':double':1':bug_list_not'
half' :: 0':s':nil':cons':double':1':bug_list_not' → 0':s':nil':cons':double':1':bug_list_not'
log' :: 0':s':nil':cons':double':1':bug_list_not' → 0':s':nil':cons':double':1':bug_list_not'
more' :: 0':s':nil':cons':double':1':bug_list_not' → 0':s':nil':cons':double':1':bug_list_not'
s2bin' :: 0':s':nil':cons':double':1':bug_list_not' → 0':s':nil':cons':double':1':bug_list_not'
s2bin1' :: 0':s':nil':cons':double':1':bug_list_not' → 0':s':nil':cons':double':1':bug_list_not' → 0':s':nil':cons':double':1':bug_list_not' → 0':s':nil':cons':double':1':bug_list_not'
if1' :: true':false' → 0':s':nil':cons':double':1':bug_list_not' → 0':s':nil':cons':double':1':bug_list_not' → 0':s':nil':cons':double':1':bug_list_not' → 0':s':nil':cons':double':1':bug_list_not'
s2bin2' :: 0':s':nil':cons':double':1':bug_list_not' → 0':s':nil':cons':double':1':bug_list_not' → 0':s':nil':cons':double':1':bug_list_not'
bug_list_not' :: 0':s':nil':cons':double':1':bug_list_not'
if2' :: true':false' → 0':s':nil':cons':double':1':bug_list_not' → 0':s':nil':cons':double':1':bug_list_not' → 0':s':nil':cons':double':1':bug_list_not' → 0':s':nil':cons':double':1':bug_list_not'
_hole_true':false'1 :: true':false'
_hole_0':s':nil':cons':double':1':bug_list_not'2 :: 0':s':nil':cons':double':1':bug_list_not'
_gen_0':s':nil':cons':double':1':bug_list_not'3 :: Nat → 0':s':nil':cons':double':1':bug_list_not'

Heuristically decided to analyse the following defined symbols:
eq', lt', bin2ss', half', log', s2bin1', s2bin2'

They will be analysed ascendingly in the following order:
eq' < s2bin2'
lt' < s2bin1'
half' < log'
log' < s2bin1'
s2bin2' < s2bin1'

Rules:
eq'(0', 0') → true'
eq'(0', s'(y)) → false'
eq'(s'(x), 0') → false'
eq'(s'(x), s'(y)) → eq'(x, y)
lt'(0', s'(y)) → true'
lt'(x, 0') → false'
lt'(s'(x), s'(y)) → lt'(x, y)
bin2s'(nil') → 0'
bin2s'(cons'(x, xs)) → bin2ss'(x, xs)
bin2ss'(x, nil') → x
bin2ss'(x, cons'(0', xs)) → bin2ss'(double', xs)
bin2ss'(x, cons'(1', xs)) → bin2ss'(s'(double'), xs)
half'(0') → 0'
half'(s'(0')) → 0'
half'(s'(s'(x))) → s'(half'(x))
log'(0') → 0'
log'(s'(0')) → 0'
log'(s'(s'(x))) → s'(log'(half'(s'(s'(x)))))
more'(nil') → nil'
more'(cons'(xs, ys)) → cons'(cons'(0', xs), cons'(cons'(1', xs), cons'(xs, ys)))
s2bin'(x) → s2bin1'(x, 0', cons'(nil', nil'))
s2bin1'(x, y, lists) → if1'(lt'(y, log'(x)), x, y, lists)
if1'(true', x, y, lists) → s2bin1'(x, s'(y), more'(lists))
if1'(false', x, y, lists) → s2bin2'(x, lists)
s2bin2'(x, nil') → bug_list_not'
s2bin2'(x, cons'(xs, ys)) → if2'(eq'(x, bin2s'(xs)), x, xs, ys)
if2'(true', x, xs, ys) → xs
if2'(false', x, xs, ys) → s2bin2'(x, ys)

Types:
eq' :: 0':s':nil':cons':double':1':bug_list_not' → 0':s':nil':cons':double':1':bug_list_not' → true':false'
0' :: 0':s':nil':cons':double':1':bug_list_not'
true' :: true':false'
s' :: 0':s':nil':cons':double':1':bug_list_not' → 0':s':nil':cons':double':1':bug_list_not'
false' :: true':false'
lt' :: 0':s':nil':cons':double':1':bug_list_not' → 0':s':nil':cons':double':1':bug_list_not' → true':false'
bin2s' :: 0':s':nil':cons':double':1':bug_list_not' → 0':s':nil':cons':double':1':bug_list_not'
nil' :: 0':s':nil':cons':double':1':bug_list_not'
cons' :: 0':s':nil':cons':double':1':bug_list_not' → 0':s':nil':cons':double':1':bug_list_not' → 0':s':nil':cons':double':1':bug_list_not'
bin2ss' :: 0':s':nil':cons':double':1':bug_list_not' → 0':s':nil':cons':double':1':bug_list_not' → 0':s':nil':cons':double':1':bug_list_not'
double' :: 0':s':nil':cons':double':1':bug_list_not'
1' :: 0':s':nil':cons':double':1':bug_list_not'
half' :: 0':s':nil':cons':double':1':bug_list_not' → 0':s':nil':cons':double':1':bug_list_not'
log' :: 0':s':nil':cons':double':1':bug_list_not' → 0':s':nil':cons':double':1':bug_list_not'
more' :: 0':s':nil':cons':double':1':bug_list_not' → 0':s':nil':cons':double':1':bug_list_not'
s2bin' :: 0':s':nil':cons':double':1':bug_list_not' → 0':s':nil':cons':double':1':bug_list_not'
s2bin1' :: 0':s':nil':cons':double':1':bug_list_not' → 0':s':nil':cons':double':1':bug_list_not' → 0':s':nil':cons':double':1':bug_list_not' → 0':s':nil':cons':double':1':bug_list_not'
if1' :: true':false' → 0':s':nil':cons':double':1':bug_list_not' → 0':s':nil':cons':double':1':bug_list_not' → 0':s':nil':cons':double':1':bug_list_not' → 0':s':nil':cons':double':1':bug_list_not'
s2bin2' :: 0':s':nil':cons':double':1':bug_list_not' → 0':s':nil':cons':double':1':bug_list_not' → 0':s':nil':cons':double':1':bug_list_not'
bug_list_not' :: 0':s':nil':cons':double':1':bug_list_not'
if2' :: true':false' → 0':s':nil':cons':double':1':bug_list_not' → 0':s':nil':cons':double':1':bug_list_not' → 0':s':nil':cons':double':1':bug_list_not' → 0':s':nil':cons':double':1':bug_list_not'
_hole_true':false'1 :: true':false'
_hole_0':s':nil':cons':double':1':bug_list_not'2 :: 0':s':nil':cons':double':1':bug_list_not'
_gen_0':s':nil':cons':double':1':bug_list_not'3 :: Nat → 0':s':nil':cons':double':1':bug_list_not'

Generator Equations:
_gen_0':s':nil':cons':double':1':bug_list_not'3(0) ⇔ 0'
_gen_0':s':nil':cons':double':1':bug_list_not'3(+(x, 1)) ⇔ s'(_gen_0':s':nil':cons':double':1':bug_list_not'3(x))

The following defined symbols remain to be analysed:
eq', lt', bin2ss', half', log', s2bin1', s2bin2'

They will be analysed ascendingly in the following order:
eq' < s2bin2'
lt' < s2bin1'
half' < log'
log' < s2bin1'
s2bin2' < s2bin1'

Proved the following rewrite lemma:
eq'(_gen_0':s':nil':cons':double':1':bug_list_not'3(_n5), _gen_0':s':nil':cons':double':1':bug_list_not'3(_n5)) → true', rt ∈ Ω(1 + n5)

Induction Base:
eq'(_gen_0':s':nil':cons':double':1':bug_list_not'3(0), _gen_0':s':nil':cons':double':1':bug_list_not'3(0)) →RΩ(1)
true'

Induction Step:
eq'(_gen_0':s':nil':cons':double':1':bug_list_not'3(+(_$n6, 1)), _gen_0':s':nil':cons':double':1':bug_list_not'3(+(_$n6, 1))) →RΩ(1)
eq'(_gen_0':s':nil':cons':double':1':bug_list_not'3(_$n6), _gen_0':s':nil':cons':double':1':bug_list_not'3(_$n6)) →IH
true'

We have rt ∈ Ω(n) and sz ∈ O(n). Thus, we have ircR ∈ Ω(n).

Rules:
eq'(0', 0') → true'
eq'(0', s'(y)) → false'
eq'(s'(x), 0') → false'
eq'(s'(x), s'(y)) → eq'(x, y)
lt'(0', s'(y)) → true'
lt'(x, 0') → false'
lt'(s'(x), s'(y)) → lt'(x, y)
bin2s'(nil') → 0'
bin2s'(cons'(x, xs)) → bin2ss'(x, xs)
bin2ss'(x, nil') → x
bin2ss'(x, cons'(0', xs)) → bin2ss'(double', xs)
bin2ss'(x, cons'(1', xs)) → bin2ss'(s'(double'), xs)
half'(0') → 0'
half'(s'(0')) → 0'
half'(s'(s'(x))) → s'(half'(x))
log'(0') → 0'
log'(s'(0')) → 0'
log'(s'(s'(x))) → s'(log'(half'(s'(s'(x)))))
more'(nil') → nil'
more'(cons'(xs, ys)) → cons'(cons'(0', xs), cons'(cons'(1', xs), cons'(xs, ys)))
s2bin'(x) → s2bin1'(x, 0', cons'(nil', nil'))
s2bin1'(x, y, lists) → if1'(lt'(y, log'(x)), x, y, lists)
if1'(true', x, y, lists) → s2bin1'(x, s'(y), more'(lists))
if1'(false', x, y, lists) → s2bin2'(x, lists)
s2bin2'(x, nil') → bug_list_not'
s2bin2'(x, cons'(xs, ys)) → if2'(eq'(x, bin2s'(xs)), x, xs, ys)
if2'(true', x, xs, ys) → xs
if2'(false', x, xs, ys) → s2bin2'(x, ys)

Types:
eq' :: 0':s':nil':cons':double':1':bug_list_not' → 0':s':nil':cons':double':1':bug_list_not' → true':false'
0' :: 0':s':nil':cons':double':1':bug_list_not'
true' :: true':false'
s' :: 0':s':nil':cons':double':1':bug_list_not' → 0':s':nil':cons':double':1':bug_list_not'
false' :: true':false'
lt' :: 0':s':nil':cons':double':1':bug_list_not' → 0':s':nil':cons':double':1':bug_list_not' → true':false'
bin2s' :: 0':s':nil':cons':double':1':bug_list_not' → 0':s':nil':cons':double':1':bug_list_not'
nil' :: 0':s':nil':cons':double':1':bug_list_not'
cons' :: 0':s':nil':cons':double':1':bug_list_not' → 0':s':nil':cons':double':1':bug_list_not' → 0':s':nil':cons':double':1':bug_list_not'
bin2ss' :: 0':s':nil':cons':double':1':bug_list_not' → 0':s':nil':cons':double':1':bug_list_not' → 0':s':nil':cons':double':1':bug_list_not'
double' :: 0':s':nil':cons':double':1':bug_list_not'
1' :: 0':s':nil':cons':double':1':bug_list_not'
half' :: 0':s':nil':cons':double':1':bug_list_not' → 0':s':nil':cons':double':1':bug_list_not'
log' :: 0':s':nil':cons':double':1':bug_list_not' → 0':s':nil':cons':double':1':bug_list_not'
more' :: 0':s':nil':cons':double':1':bug_list_not' → 0':s':nil':cons':double':1':bug_list_not'
s2bin' :: 0':s':nil':cons':double':1':bug_list_not' → 0':s':nil':cons':double':1':bug_list_not'
s2bin1' :: 0':s':nil':cons':double':1':bug_list_not' → 0':s':nil':cons':double':1':bug_list_not' → 0':s':nil':cons':double':1':bug_list_not' → 0':s':nil':cons':double':1':bug_list_not'
if1' :: true':false' → 0':s':nil':cons':double':1':bug_list_not' → 0':s':nil':cons':double':1':bug_list_not' → 0':s':nil':cons':double':1':bug_list_not' → 0':s':nil':cons':double':1':bug_list_not'
s2bin2' :: 0':s':nil':cons':double':1':bug_list_not' → 0':s':nil':cons':double':1':bug_list_not' → 0':s':nil':cons':double':1':bug_list_not'
bug_list_not' :: 0':s':nil':cons':double':1':bug_list_not'
if2' :: true':false' → 0':s':nil':cons':double':1':bug_list_not' → 0':s':nil':cons':double':1':bug_list_not' → 0':s':nil':cons':double':1':bug_list_not' → 0':s':nil':cons':double':1':bug_list_not'
_hole_true':false'1 :: true':false'
_hole_0':s':nil':cons':double':1':bug_list_not'2 :: 0':s':nil':cons':double':1':bug_list_not'
_gen_0':s':nil':cons':double':1':bug_list_not'3 :: Nat → 0':s':nil':cons':double':1':bug_list_not'

Lemmas:
eq'(_gen_0':s':nil':cons':double':1':bug_list_not'3(_n5), _gen_0':s':nil':cons':double':1':bug_list_not'3(_n5)) → true', rt ∈ Ω(1 + n5)

Generator Equations:
_gen_0':s':nil':cons':double':1':bug_list_not'3(0) ⇔ 0'
_gen_0':s':nil':cons':double':1':bug_list_not'3(+(x, 1)) ⇔ s'(_gen_0':s':nil':cons':double':1':bug_list_not'3(x))

The following defined symbols remain to be analysed:
lt', bin2ss', half', log', s2bin1', s2bin2'

They will be analysed ascendingly in the following order:
lt' < s2bin1'
half' < log'
log' < s2bin1'
s2bin2' < s2bin1'

Proved the following rewrite lemma:
lt'(_gen_0':s':nil':cons':double':1':bug_list_not'3(_n1338), _gen_0':s':nil':cons':double':1':bug_list_not'3(+(1, _n1338))) → true', rt ∈ Ω(1 + n1338)

Induction Base:
lt'(_gen_0':s':nil':cons':double':1':bug_list_not'3(0), _gen_0':s':nil':cons':double':1':bug_list_not'3(+(1, 0))) →RΩ(1)
true'

Induction Step:
lt'(_gen_0':s':nil':cons':double':1':bug_list_not'3(+(_$n1339, 1)), _gen_0':s':nil':cons':double':1':bug_list_not'3(+(1, +(_$n1339, 1)))) →RΩ(1)
lt'(_gen_0':s':nil':cons':double':1':bug_list_not'3(_$n1339), _gen_0':s':nil':cons':double':1':bug_list_not'3(+(1, _$n1339))) →IH
true'

We have rt ∈ Ω(n) and sz ∈ O(n). Thus, we have ircR ∈ Ω(n).

Rules:
eq'(0', 0') → true'
eq'(0', s'(y)) → false'
eq'(s'(x), 0') → false'
eq'(s'(x), s'(y)) → eq'(x, y)
lt'(0', s'(y)) → true'
lt'(x, 0') → false'
lt'(s'(x), s'(y)) → lt'(x, y)
bin2s'(nil') → 0'
bin2s'(cons'(x, xs)) → bin2ss'(x, xs)
bin2ss'(x, nil') → x
bin2ss'(x, cons'(0', xs)) → bin2ss'(double', xs)
bin2ss'(x, cons'(1', xs)) → bin2ss'(s'(double'), xs)
half'(0') → 0'
half'(s'(0')) → 0'
half'(s'(s'(x))) → s'(half'(x))
log'(0') → 0'
log'(s'(0')) → 0'
log'(s'(s'(x))) → s'(log'(half'(s'(s'(x)))))
more'(nil') → nil'
more'(cons'(xs, ys)) → cons'(cons'(0', xs), cons'(cons'(1', xs), cons'(xs, ys)))
s2bin'(x) → s2bin1'(x, 0', cons'(nil', nil'))
s2bin1'(x, y, lists) → if1'(lt'(y, log'(x)), x, y, lists)
if1'(true', x, y, lists) → s2bin1'(x, s'(y), more'(lists))
if1'(false', x, y, lists) → s2bin2'(x, lists)
s2bin2'(x, nil') → bug_list_not'
s2bin2'(x, cons'(xs, ys)) → if2'(eq'(x, bin2s'(xs)), x, xs, ys)
if2'(true', x, xs, ys) → xs
if2'(false', x, xs, ys) → s2bin2'(x, ys)

Types:
eq' :: 0':s':nil':cons':double':1':bug_list_not' → 0':s':nil':cons':double':1':bug_list_not' → true':false'
0' :: 0':s':nil':cons':double':1':bug_list_not'
true' :: true':false'
s' :: 0':s':nil':cons':double':1':bug_list_not' → 0':s':nil':cons':double':1':bug_list_not'
false' :: true':false'
lt' :: 0':s':nil':cons':double':1':bug_list_not' → 0':s':nil':cons':double':1':bug_list_not' → true':false'
bin2s' :: 0':s':nil':cons':double':1':bug_list_not' → 0':s':nil':cons':double':1':bug_list_not'
nil' :: 0':s':nil':cons':double':1':bug_list_not'
cons' :: 0':s':nil':cons':double':1':bug_list_not' → 0':s':nil':cons':double':1':bug_list_not' → 0':s':nil':cons':double':1':bug_list_not'
bin2ss' :: 0':s':nil':cons':double':1':bug_list_not' → 0':s':nil':cons':double':1':bug_list_not' → 0':s':nil':cons':double':1':bug_list_not'
double' :: 0':s':nil':cons':double':1':bug_list_not'
1' :: 0':s':nil':cons':double':1':bug_list_not'
half' :: 0':s':nil':cons':double':1':bug_list_not' → 0':s':nil':cons':double':1':bug_list_not'
log' :: 0':s':nil':cons':double':1':bug_list_not' → 0':s':nil':cons':double':1':bug_list_not'
more' :: 0':s':nil':cons':double':1':bug_list_not' → 0':s':nil':cons':double':1':bug_list_not'
s2bin' :: 0':s':nil':cons':double':1':bug_list_not' → 0':s':nil':cons':double':1':bug_list_not'
s2bin1' :: 0':s':nil':cons':double':1':bug_list_not' → 0':s':nil':cons':double':1':bug_list_not' → 0':s':nil':cons':double':1':bug_list_not' → 0':s':nil':cons':double':1':bug_list_not'
if1' :: true':false' → 0':s':nil':cons':double':1':bug_list_not' → 0':s':nil':cons':double':1':bug_list_not' → 0':s':nil':cons':double':1':bug_list_not' → 0':s':nil':cons':double':1':bug_list_not'
s2bin2' :: 0':s':nil':cons':double':1':bug_list_not' → 0':s':nil':cons':double':1':bug_list_not' → 0':s':nil':cons':double':1':bug_list_not'
bug_list_not' :: 0':s':nil':cons':double':1':bug_list_not'
if2' :: true':false' → 0':s':nil':cons':double':1':bug_list_not' → 0':s':nil':cons':double':1':bug_list_not' → 0':s':nil':cons':double':1':bug_list_not' → 0':s':nil':cons':double':1':bug_list_not'
_hole_true':false'1 :: true':false'
_hole_0':s':nil':cons':double':1':bug_list_not'2 :: 0':s':nil':cons':double':1':bug_list_not'
_gen_0':s':nil':cons':double':1':bug_list_not'3 :: Nat → 0':s':nil':cons':double':1':bug_list_not'

Lemmas:
eq'(_gen_0':s':nil':cons':double':1':bug_list_not'3(_n5), _gen_0':s':nil':cons':double':1':bug_list_not'3(_n5)) → true', rt ∈ Ω(1 + n5)
lt'(_gen_0':s':nil':cons':double':1':bug_list_not'3(_n1338), _gen_0':s':nil':cons':double':1':bug_list_not'3(+(1, _n1338))) → true', rt ∈ Ω(1 + n1338)

Generator Equations:
_gen_0':s':nil':cons':double':1':bug_list_not'3(0) ⇔ 0'
_gen_0':s':nil':cons':double':1':bug_list_not'3(+(x, 1)) ⇔ s'(_gen_0':s':nil':cons':double':1':bug_list_not'3(x))

The following defined symbols remain to be analysed:
bin2ss', half', log', s2bin1', s2bin2'

They will be analysed ascendingly in the following order:
half' < log'
log' < s2bin1'
s2bin2' < s2bin1'

Could not prove a rewrite lemma for the defined symbol bin2ss'.

Rules:
eq'(0', 0') → true'
eq'(0', s'(y)) → false'
eq'(s'(x), 0') → false'
eq'(s'(x), s'(y)) → eq'(x, y)
lt'(0', s'(y)) → true'
lt'(x, 0') → false'
lt'(s'(x), s'(y)) → lt'(x, y)
bin2s'(nil') → 0'
bin2s'(cons'(x, xs)) → bin2ss'(x, xs)
bin2ss'(x, nil') → x
bin2ss'(x, cons'(0', xs)) → bin2ss'(double', xs)
bin2ss'(x, cons'(1', xs)) → bin2ss'(s'(double'), xs)
half'(0') → 0'
half'(s'(0')) → 0'
half'(s'(s'(x))) → s'(half'(x))
log'(0') → 0'
log'(s'(0')) → 0'
log'(s'(s'(x))) → s'(log'(half'(s'(s'(x)))))
more'(nil') → nil'
more'(cons'(xs, ys)) → cons'(cons'(0', xs), cons'(cons'(1', xs), cons'(xs, ys)))
s2bin'(x) → s2bin1'(x, 0', cons'(nil', nil'))
s2bin1'(x, y, lists) → if1'(lt'(y, log'(x)), x, y, lists)
if1'(true', x, y, lists) → s2bin1'(x, s'(y), more'(lists))
if1'(false', x, y, lists) → s2bin2'(x, lists)
s2bin2'(x, nil') → bug_list_not'
s2bin2'(x, cons'(xs, ys)) → if2'(eq'(x, bin2s'(xs)), x, xs, ys)
if2'(true', x, xs, ys) → xs
if2'(false', x, xs, ys) → s2bin2'(x, ys)

Types:
eq' :: 0':s':nil':cons':double':1':bug_list_not' → 0':s':nil':cons':double':1':bug_list_not' → true':false'
0' :: 0':s':nil':cons':double':1':bug_list_not'
true' :: true':false'
s' :: 0':s':nil':cons':double':1':bug_list_not' → 0':s':nil':cons':double':1':bug_list_not'
false' :: true':false'
lt' :: 0':s':nil':cons':double':1':bug_list_not' → 0':s':nil':cons':double':1':bug_list_not' → true':false'
bin2s' :: 0':s':nil':cons':double':1':bug_list_not' → 0':s':nil':cons':double':1':bug_list_not'
nil' :: 0':s':nil':cons':double':1':bug_list_not'
cons' :: 0':s':nil':cons':double':1':bug_list_not' → 0':s':nil':cons':double':1':bug_list_not' → 0':s':nil':cons':double':1':bug_list_not'
bin2ss' :: 0':s':nil':cons':double':1':bug_list_not' → 0':s':nil':cons':double':1':bug_list_not' → 0':s':nil':cons':double':1':bug_list_not'
double' :: 0':s':nil':cons':double':1':bug_list_not'
1' :: 0':s':nil':cons':double':1':bug_list_not'
half' :: 0':s':nil':cons':double':1':bug_list_not' → 0':s':nil':cons':double':1':bug_list_not'
log' :: 0':s':nil':cons':double':1':bug_list_not' → 0':s':nil':cons':double':1':bug_list_not'
more' :: 0':s':nil':cons':double':1':bug_list_not' → 0':s':nil':cons':double':1':bug_list_not'
s2bin' :: 0':s':nil':cons':double':1':bug_list_not' → 0':s':nil':cons':double':1':bug_list_not'
s2bin1' :: 0':s':nil':cons':double':1':bug_list_not' → 0':s':nil':cons':double':1':bug_list_not' → 0':s':nil':cons':double':1':bug_list_not' → 0':s':nil':cons':double':1':bug_list_not'
if1' :: true':false' → 0':s':nil':cons':double':1':bug_list_not' → 0':s':nil':cons':double':1':bug_list_not' → 0':s':nil':cons':double':1':bug_list_not' → 0':s':nil':cons':double':1':bug_list_not'
s2bin2' :: 0':s':nil':cons':double':1':bug_list_not' → 0':s':nil':cons':double':1':bug_list_not' → 0':s':nil':cons':double':1':bug_list_not'
bug_list_not' :: 0':s':nil':cons':double':1':bug_list_not'
if2' :: true':false' → 0':s':nil':cons':double':1':bug_list_not' → 0':s':nil':cons':double':1':bug_list_not' → 0':s':nil':cons':double':1':bug_list_not' → 0':s':nil':cons':double':1':bug_list_not'
_hole_true':false'1 :: true':false'
_hole_0':s':nil':cons':double':1':bug_list_not'2 :: 0':s':nil':cons':double':1':bug_list_not'
_gen_0':s':nil':cons':double':1':bug_list_not'3 :: Nat → 0':s':nil':cons':double':1':bug_list_not'

Lemmas:
eq'(_gen_0':s':nil':cons':double':1':bug_list_not'3(_n5), _gen_0':s':nil':cons':double':1':bug_list_not'3(_n5)) → true', rt ∈ Ω(1 + n5)
lt'(_gen_0':s':nil':cons':double':1':bug_list_not'3(_n1338), _gen_0':s':nil':cons':double':1':bug_list_not'3(+(1, _n1338))) → true', rt ∈ Ω(1 + n1338)

Generator Equations:
_gen_0':s':nil':cons':double':1':bug_list_not'3(0) ⇔ 0'
_gen_0':s':nil':cons':double':1':bug_list_not'3(+(x, 1)) ⇔ s'(_gen_0':s':nil':cons':double':1':bug_list_not'3(x))

The following defined symbols remain to be analysed:
half', log', s2bin1', s2bin2'

They will be analysed ascendingly in the following order:
half' < log'
log' < s2bin1'
s2bin2' < s2bin1'

Proved the following rewrite lemma:
half'(_gen_0':s':nil':cons':double':1':bug_list_not'3(*(2, _n2867))) → _gen_0':s':nil':cons':double':1':bug_list_not'3(_n2867), rt ∈ Ω(1 + n2867)

Induction Base:
half'(_gen_0':s':nil':cons':double':1':bug_list_not'3(*(2, 0))) →RΩ(1)
0'

Induction Step:
half'(_gen_0':s':nil':cons':double':1':bug_list_not'3(*(2, +(_$n2868, 1)))) →RΩ(1)
s'(half'(_gen_0':s':nil':cons':double':1':bug_list_not'3(*(2, _$n2868)))) →IH
s'(_gen_0':s':nil':cons':double':1':bug_list_not'3(_$n2868))

We have rt ∈ Ω(n) and sz ∈ O(n). Thus, we have ircR ∈ Ω(n).

Rules:
eq'(0', 0') → true'
eq'(0', s'(y)) → false'
eq'(s'(x), 0') → false'
eq'(s'(x), s'(y)) → eq'(x, y)
lt'(0', s'(y)) → true'
lt'(x, 0') → false'
lt'(s'(x), s'(y)) → lt'(x, y)
bin2s'(nil') → 0'
bin2s'(cons'(x, xs)) → bin2ss'(x, xs)
bin2ss'(x, nil') → x
bin2ss'(x, cons'(0', xs)) → bin2ss'(double', xs)
bin2ss'(x, cons'(1', xs)) → bin2ss'(s'(double'), xs)
half'(0') → 0'
half'(s'(0')) → 0'
half'(s'(s'(x))) → s'(half'(x))
log'(0') → 0'
log'(s'(0')) → 0'
log'(s'(s'(x))) → s'(log'(half'(s'(s'(x)))))
more'(nil') → nil'
more'(cons'(xs, ys)) → cons'(cons'(0', xs), cons'(cons'(1', xs), cons'(xs, ys)))
s2bin'(x) → s2bin1'(x, 0', cons'(nil', nil'))
s2bin1'(x, y, lists) → if1'(lt'(y, log'(x)), x, y, lists)
if1'(true', x, y, lists) → s2bin1'(x, s'(y), more'(lists))
if1'(false', x, y, lists) → s2bin2'(x, lists)
s2bin2'(x, nil') → bug_list_not'
s2bin2'(x, cons'(xs, ys)) → if2'(eq'(x, bin2s'(xs)), x, xs, ys)
if2'(true', x, xs, ys) → xs
if2'(false', x, xs, ys) → s2bin2'(x, ys)

Types:
eq' :: 0':s':nil':cons':double':1':bug_list_not' → 0':s':nil':cons':double':1':bug_list_not' → true':false'
0' :: 0':s':nil':cons':double':1':bug_list_not'
true' :: true':false'
s' :: 0':s':nil':cons':double':1':bug_list_not' → 0':s':nil':cons':double':1':bug_list_not'
false' :: true':false'
lt' :: 0':s':nil':cons':double':1':bug_list_not' → 0':s':nil':cons':double':1':bug_list_not' → true':false'
bin2s' :: 0':s':nil':cons':double':1':bug_list_not' → 0':s':nil':cons':double':1':bug_list_not'
nil' :: 0':s':nil':cons':double':1':bug_list_not'
cons' :: 0':s':nil':cons':double':1':bug_list_not' → 0':s':nil':cons':double':1':bug_list_not' → 0':s':nil':cons':double':1':bug_list_not'
bin2ss' :: 0':s':nil':cons':double':1':bug_list_not' → 0':s':nil':cons':double':1':bug_list_not' → 0':s':nil':cons':double':1':bug_list_not'
double' :: 0':s':nil':cons':double':1':bug_list_not'
1' :: 0':s':nil':cons':double':1':bug_list_not'
half' :: 0':s':nil':cons':double':1':bug_list_not' → 0':s':nil':cons':double':1':bug_list_not'
log' :: 0':s':nil':cons':double':1':bug_list_not' → 0':s':nil':cons':double':1':bug_list_not'
more' :: 0':s':nil':cons':double':1':bug_list_not' → 0':s':nil':cons':double':1':bug_list_not'
s2bin' :: 0':s':nil':cons':double':1':bug_list_not' → 0':s':nil':cons':double':1':bug_list_not'
s2bin1' :: 0':s':nil':cons':double':1':bug_list_not' → 0':s':nil':cons':double':1':bug_list_not' → 0':s':nil':cons':double':1':bug_list_not' → 0':s':nil':cons':double':1':bug_list_not'
if1' :: true':false' → 0':s':nil':cons':double':1':bug_list_not' → 0':s':nil':cons':double':1':bug_list_not' → 0':s':nil':cons':double':1':bug_list_not' → 0':s':nil':cons':double':1':bug_list_not'
s2bin2' :: 0':s':nil':cons':double':1':bug_list_not' → 0':s':nil':cons':double':1':bug_list_not' → 0':s':nil':cons':double':1':bug_list_not'
bug_list_not' :: 0':s':nil':cons':double':1':bug_list_not'
if2' :: true':false' → 0':s':nil':cons':double':1':bug_list_not' → 0':s':nil':cons':double':1':bug_list_not' → 0':s':nil':cons':double':1':bug_list_not' → 0':s':nil':cons':double':1':bug_list_not'
_hole_true':false'1 :: true':false'
_hole_0':s':nil':cons':double':1':bug_list_not'2 :: 0':s':nil':cons':double':1':bug_list_not'
_gen_0':s':nil':cons':double':1':bug_list_not'3 :: Nat → 0':s':nil':cons':double':1':bug_list_not'

Lemmas:
eq'(_gen_0':s':nil':cons':double':1':bug_list_not'3(_n5), _gen_0':s':nil':cons':double':1':bug_list_not'3(_n5)) → true', rt ∈ Ω(1 + n5)
lt'(_gen_0':s':nil':cons':double':1':bug_list_not'3(_n1338), _gen_0':s':nil':cons':double':1':bug_list_not'3(+(1, _n1338))) → true', rt ∈ Ω(1 + n1338)
half'(_gen_0':s':nil':cons':double':1':bug_list_not'3(*(2, _n2867))) → _gen_0':s':nil':cons':double':1':bug_list_not'3(_n2867), rt ∈ Ω(1 + n2867)

Generator Equations:
_gen_0':s':nil':cons':double':1':bug_list_not'3(0) ⇔ 0'
_gen_0':s':nil':cons':double':1':bug_list_not'3(+(x, 1)) ⇔ s'(_gen_0':s':nil':cons':double':1':bug_list_not'3(x))

The following defined symbols remain to be analysed:
log', s2bin1', s2bin2'

They will be analysed ascendingly in the following order:
log' < s2bin1'
s2bin2' < s2bin1'

Could not prove a rewrite lemma for the defined symbol log'.

Rules:
eq'(0', 0') → true'
eq'(0', s'(y)) → false'
eq'(s'(x), 0') → false'
eq'(s'(x), s'(y)) → eq'(x, y)
lt'(0', s'(y)) → true'
lt'(x, 0') → false'
lt'(s'(x), s'(y)) → lt'(x, y)
bin2s'(nil') → 0'
bin2s'(cons'(x, xs)) → bin2ss'(x, xs)
bin2ss'(x, nil') → x
bin2ss'(x, cons'(0', xs)) → bin2ss'(double', xs)
bin2ss'(x, cons'(1', xs)) → bin2ss'(s'(double'), xs)
half'(0') → 0'
half'(s'(0')) → 0'
half'(s'(s'(x))) → s'(half'(x))
log'(0') → 0'
log'(s'(0')) → 0'
log'(s'(s'(x))) → s'(log'(half'(s'(s'(x)))))
more'(nil') → nil'
more'(cons'(xs, ys)) → cons'(cons'(0', xs), cons'(cons'(1', xs), cons'(xs, ys)))
s2bin'(x) → s2bin1'(x, 0', cons'(nil', nil'))
s2bin1'(x, y, lists) → if1'(lt'(y, log'(x)), x, y, lists)
if1'(true', x, y, lists) → s2bin1'(x, s'(y), more'(lists))
if1'(false', x, y, lists) → s2bin2'(x, lists)
s2bin2'(x, nil') → bug_list_not'
s2bin2'(x, cons'(xs, ys)) → if2'(eq'(x, bin2s'(xs)), x, xs, ys)
if2'(true', x, xs, ys) → xs
if2'(false', x, xs, ys) → s2bin2'(x, ys)

Types:
eq' :: 0':s':nil':cons':double':1':bug_list_not' → 0':s':nil':cons':double':1':bug_list_not' → true':false'
0' :: 0':s':nil':cons':double':1':bug_list_not'
true' :: true':false'
s' :: 0':s':nil':cons':double':1':bug_list_not' → 0':s':nil':cons':double':1':bug_list_not'
false' :: true':false'
lt' :: 0':s':nil':cons':double':1':bug_list_not' → 0':s':nil':cons':double':1':bug_list_not' → true':false'
bin2s' :: 0':s':nil':cons':double':1':bug_list_not' → 0':s':nil':cons':double':1':bug_list_not'
nil' :: 0':s':nil':cons':double':1':bug_list_not'
cons' :: 0':s':nil':cons':double':1':bug_list_not' → 0':s':nil':cons':double':1':bug_list_not' → 0':s':nil':cons':double':1':bug_list_not'
bin2ss' :: 0':s':nil':cons':double':1':bug_list_not' → 0':s':nil':cons':double':1':bug_list_not' → 0':s':nil':cons':double':1':bug_list_not'
double' :: 0':s':nil':cons':double':1':bug_list_not'
1' :: 0':s':nil':cons':double':1':bug_list_not'
half' :: 0':s':nil':cons':double':1':bug_list_not' → 0':s':nil':cons':double':1':bug_list_not'
log' :: 0':s':nil':cons':double':1':bug_list_not' → 0':s':nil':cons':double':1':bug_list_not'
more' :: 0':s':nil':cons':double':1':bug_list_not' → 0':s':nil':cons':double':1':bug_list_not'
s2bin' :: 0':s':nil':cons':double':1':bug_list_not' → 0':s':nil':cons':double':1':bug_list_not'
s2bin1' :: 0':s':nil':cons':double':1':bug_list_not' → 0':s':nil':cons':double':1':bug_list_not' → 0':s':nil':cons':double':1':bug_list_not' → 0':s':nil':cons':double':1':bug_list_not'
if1' :: true':false' → 0':s':nil':cons':double':1':bug_list_not' → 0':s':nil':cons':double':1':bug_list_not' → 0':s':nil':cons':double':1':bug_list_not' → 0':s':nil':cons':double':1':bug_list_not'
s2bin2' :: 0':s':nil':cons':double':1':bug_list_not' → 0':s':nil':cons':double':1':bug_list_not' → 0':s':nil':cons':double':1':bug_list_not'
bug_list_not' :: 0':s':nil':cons':double':1':bug_list_not'
if2' :: true':false' → 0':s':nil':cons':double':1':bug_list_not' → 0':s':nil':cons':double':1':bug_list_not' → 0':s':nil':cons':double':1':bug_list_not' → 0':s':nil':cons':double':1':bug_list_not'
_hole_true':false'1 :: true':false'
_hole_0':s':nil':cons':double':1':bug_list_not'2 :: 0':s':nil':cons':double':1':bug_list_not'
_gen_0':s':nil':cons':double':1':bug_list_not'3 :: Nat → 0':s':nil':cons':double':1':bug_list_not'

Lemmas:
eq'(_gen_0':s':nil':cons':double':1':bug_list_not'3(_n5), _gen_0':s':nil':cons':double':1':bug_list_not'3(_n5)) → true', rt ∈ Ω(1 + n5)
lt'(_gen_0':s':nil':cons':double':1':bug_list_not'3(_n1338), _gen_0':s':nil':cons':double':1':bug_list_not'3(+(1, _n1338))) → true', rt ∈ Ω(1 + n1338)
half'(_gen_0':s':nil':cons':double':1':bug_list_not'3(*(2, _n2867))) → _gen_0':s':nil':cons':double':1':bug_list_not'3(_n2867), rt ∈ Ω(1 + n2867)

Generator Equations:
_gen_0':s':nil':cons':double':1':bug_list_not'3(0) ⇔ 0'
_gen_0':s':nil':cons':double':1':bug_list_not'3(+(x, 1)) ⇔ s'(_gen_0':s':nil':cons':double':1':bug_list_not'3(x))

The following defined symbols remain to be analysed:
s2bin2', s2bin1'

They will be analysed ascendingly in the following order:
s2bin2' < s2bin1'

Could not prove a rewrite lemma for the defined symbol s2bin2'.

Rules:
eq'(0', 0') → true'
eq'(0', s'(y)) → false'
eq'(s'(x), 0') → false'
eq'(s'(x), s'(y)) → eq'(x, y)
lt'(0', s'(y)) → true'
lt'(x, 0') → false'
lt'(s'(x), s'(y)) → lt'(x, y)
bin2s'(nil') → 0'
bin2s'(cons'(x, xs)) → bin2ss'(x, xs)
bin2ss'(x, nil') → x
bin2ss'(x, cons'(0', xs)) → bin2ss'(double', xs)
bin2ss'(x, cons'(1', xs)) → bin2ss'(s'(double'), xs)
half'(0') → 0'
half'(s'(0')) → 0'
half'(s'(s'(x))) → s'(half'(x))
log'(0') → 0'
log'(s'(0')) → 0'
log'(s'(s'(x))) → s'(log'(half'(s'(s'(x)))))
more'(nil') → nil'
more'(cons'(xs, ys)) → cons'(cons'(0', xs), cons'(cons'(1', xs), cons'(xs, ys)))
s2bin'(x) → s2bin1'(x, 0', cons'(nil', nil'))
s2bin1'(x, y, lists) → if1'(lt'(y, log'(x)), x, y, lists)
if1'(true', x, y, lists) → s2bin1'(x, s'(y), more'(lists))
if1'(false', x, y, lists) → s2bin2'(x, lists)
s2bin2'(x, nil') → bug_list_not'
s2bin2'(x, cons'(xs, ys)) → if2'(eq'(x, bin2s'(xs)), x, xs, ys)
if2'(true', x, xs, ys) → xs
if2'(false', x, xs, ys) → s2bin2'(x, ys)

Types:
eq' :: 0':s':nil':cons':double':1':bug_list_not' → 0':s':nil':cons':double':1':bug_list_not' → true':false'
0' :: 0':s':nil':cons':double':1':bug_list_not'
true' :: true':false'
s' :: 0':s':nil':cons':double':1':bug_list_not' → 0':s':nil':cons':double':1':bug_list_not'
false' :: true':false'
lt' :: 0':s':nil':cons':double':1':bug_list_not' → 0':s':nil':cons':double':1':bug_list_not' → true':false'
bin2s' :: 0':s':nil':cons':double':1':bug_list_not' → 0':s':nil':cons':double':1':bug_list_not'
nil' :: 0':s':nil':cons':double':1':bug_list_not'
cons' :: 0':s':nil':cons':double':1':bug_list_not' → 0':s':nil':cons':double':1':bug_list_not' → 0':s':nil':cons':double':1':bug_list_not'
bin2ss' :: 0':s':nil':cons':double':1':bug_list_not' → 0':s':nil':cons':double':1':bug_list_not' → 0':s':nil':cons':double':1':bug_list_not'
double' :: 0':s':nil':cons':double':1':bug_list_not'
1' :: 0':s':nil':cons':double':1':bug_list_not'
half' :: 0':s':nil':cons':double':1':bug_list_not' → 0':s':nil':cons':double':1':bug_list_not'
log' :: 0':s':nil':cons':double':1':bug_list_not' → 0':s':nil':cons':double':1':bug_list_not'
more' :: 0':s':nil':cons':double':1':bug_list_not' → 0':s':nil':cons':double':1':bug_list_not'
s2bin' :: 0':s':nil':cons':double':1':bug_list_not' → 0':s':nil':cons':double':1':bug_list_not'
s2bin1' :: 0':s':nil':cons':double':1':bug_list_not' → 0':s':nil':cons':double':1':bug_list_not' → 0':s':nil':cons':double':1':bug_list_not' → 0':s':nil':cons':double':1':bug_list_not'
if1' :: true':false' → 0':s':nil':cons':double':1':bug_list_not' → 0':s':nil':cons':double':1':bug_list_not' → 0':s':nil':cons':double':1':bug_list_not' → 0':s':nil':cons':double':1':bug_list_not'
s2bin2' :: 0':s':nil':cons':double':1':bug_list_not' → 0':s':nil':cons':double':1':bug_list_not' → 0':s':nil':cons':double':1':bug_list_not'
bug_list_not' :: 0':s':nil':cons':double':1':bug_list_not'
if2' :: true':false' → 0':s':nil':cons':double':1':bug_list_not' → 0':s':nil':cons':double':1':bug_list_not' → 0':s':nil':cons':double':1':bug_list_not' → 0':s':nil':cons':double':1':bug_list_not'
_hole_true':false'1 :: true':false'
_hole_0':s':nil':cons':double':1':bug_list_not'2 :: 0':s':nil':cons':double':1':bug_list_not'
_gen_0':s':nil':cons':double':1':bug_list_not'3 :: Nat → 0':s':nil':cons':double':1':bug_list_not'

Lemmas:
eq'(_gen_0':s':nil':cons':double':1':bug_list_not'3(_n5), _gen_0':s':nil':cons':double':1':bug_list_not'3(_n5)) → true', rt ∈ Ω(1 + n5)
lt'(_gen_0':s':nil':cons':double':1':bug_list_not'3(_n1338), _gen_0':s':nil':cons':double':1':bug_list_not'3(+(1, _n1338))) → true', rt ∈ Ω(1 + n1338)
half'(_gen_0':s':nil':cons':double':1':bug_list_not'3(*(2, _n2867))) → _gen_0':s':nil':cons':double':1':bug_list_not'3(_n2867), rt ∈ Ω(1 + n2867)

Generator Equations:
_gen_0':s':nil':cons':double':1':bug_list_not'3(0) ⇔ 0'
_gen_0':s':nil':cons':double':1':bug_list_not'3(+(x, 1)) ⇔ s'(_gen_0':s':nil':cons':double':1':bug_list_not'3(x))

The following defined symbols remain to be analysed:
s2bin1'

Could not prove a rewrite lemma for the defined symbol s2bin1'.

Rules:
eq'(0', 0') → true'
eq'(0', s'(y)) → false'
eq'(s'(x), 0') → false'
eq'(s'(x), s'(y)) → eq'(x, y)
lt'(0', s'(y)) → true'
lt'(x, 0') → false'
lt'(s'(x), s'(y)) → lt'(x, y)
bin2s'(nil') → 0'
bin2s'(cons'(x, xs)) → bin2ss'(x, xs)
bin2ss'(x, nil') → x
bin2ss'(x, cons'(0', xs)) → bin2ss'(double', xs)
bin2ss'(x, cons'(1', xs)) → bin2ss'(s'(double'), xs)
half'(0') → 0'
half'(s'(0')) → 0'
half'(s'(s'(x))) → s'(half'(x))
log'(0') → 0'
log'(s'(0')) → 0'
log'(s'(s'(x))) → s'(log'(half'(s'(s'(x)))))
more'(nil') → nil'
more'(cons'(xs, ys)) → cons'(cons'(0', xs), cons'(cons'(1', xs), cons'(xs, ys)))
s2bin'(x) → s2bin1'(x, 0', cons'(nil', nil'))
s2bin1'(x, y, lists) → if1'(lt'(y, log'(x)), x, y, lists)
if1'(true', x, y, lists) → s2bin1'(x, s'(y), more'(lists))
if1'(false', x, y, lists) → s2bin2'(x, lists)
s2bin2'(x, nil') → bug_list_not'
s2bin2'(x, cons'(xs, ys)) → if2'(eq'(x, bin2s'(xs)), x, xs, ys)
if2'(true', x, xs, ys) → xs
if2'(false', x, xs, ys) → s2bin2'(x, ys)

Types:
eq' :: 0':s':nil':cons':double':1':bug_list_not' → 0':s':nil':cons':double':1':bug_list_not' → true':false'
0' :: 0':s':nil':cons':double':1':bug_list_not'
true' :: true':false'
s' :: 0':s':nil':cons':double':1':bug_list_not' → 0':s':nil':cons':double':1':bug_list_not'
false' :: true':false'
lt' :: 0':s':nil':cons':double':1':bug_list_not' → 0':s':nil':cons':double':1':bug_list_not' → true':false'
bin2s' :: 0':s':nil':cons':double':1':bug_list_not' → 0':s':nil':cons':double':1':bug_list_not'
nil' :: 0':s':nil':cons':double':1':bug_list_not'
cons' :: 0':s':nil':cons':double':1':bug_list_not' → 0':s':nil':cons':double':1':bug_list_not' → 0':s':nil':cons':double':1':bug_list_not'
bin2ss' :: 0':s':nil':cons':double':1':bug_list_not' → 0':s':nil':cons':double':1':bug_list_not' → 0':s':nil':cons':double':1':bug_list_not'
double' :: 0':s':nil':cons':double':1':bug_list_not'
1' :: 0':s':nil':cons':double':1':bug_list_not'
half' :: 0':s':nil':cons':double':1':bug_list_not' → 0':s':nil':cons':double':1':bug_list_not'
log' :: 0':s':nil':cons':double':1':bug_list_not' → 0':s':nil':cons':double':1':bug_list_not'
more' :: 0':s':nil':cons':double':1':bug_list_not' → 0':s':nil':cons':double':1':bug_list_not'
s2bin' :: 0':s':nil':cons':double':1':bug_list_not' → 0':s':nil':cons':double':1':bug_list_not'
s2bin1' :: 0':s':nil':cons':double':1':bug_list_not' → 0':s':nil':cons':double':1':bug_list_not' → 0':s':nil':cons':double':1':bug_list_not' → 0':s':nil':cons':double':1':bug_list_not'
if1' :: true':false' → 0':s':nil':cons':double':1':bug_list_not' → 0':s':nil':cons':double':1':bug_list_not' → 0':s':nil':cons':double':1':bug_list_not' → 0':s':nil':cons':double':1':bug_list_not'
s2bin2' :: 0':s':nil':cons':double':1':bug_list_not' → 0':s':nil':cons':double':1':bug_list_not' → 0':s':nil':cons':double':1':bug_list_not'
bug_list_not' :: 0':s':nil':cons':double':1':bug_list_not'
if2' :: true':false' → 0':s':nil':cons':double':1':bug_list_not' → 0':s':nil':cons':double':1':bug_list_not' → 0':s':nil':cons':double':1':bug_list_not' → 0':s':nil':cons':double':1':bug_list_not'
_hole_true':false'1 :: true':false'
_hole_0':s':nil':cons':double':1':bug_list_not'2 :: 0':s':nil':cons':double':1':bug_list_not'
_gen_0':s':nil':cons':double':1':bug_list_not'3 :: Nat → 0':s':nil':cons':double':1':bug_list_not'

Lemmas:
eq'(_gen_0':s':nil':cons':double':1':bug_list_not'3(_n5), _gen_0':s':nil':cons':double':1':bug_list_not'3(_n5)) → true', rt ∈ Ω(1 + n5)
lt'(_gen_0':s':nil':cons':double':1':bug_list_not'3(_n1338), _gen_0':s':nil':cons':double':1':bug_list_not'3(+(1, _n1338))) → true', rt ∈ Ω(1 + n1338)
half'(_gen_0':s':nil':cons':double':1':bug_list_not'3(*(2, _n2867))) → _gen_0':s':nil':cons':double':1':bug_list_not'3(_n2867), rt ∈ Ω(1 + n2867)

Generator Equations:
_gen_0':s':nil':cons':double':1':bug_list_not'3(0) ⇔ 0'
_gen_0':s':nil':cons':double':1':bug_list_not'3(+(x, 1)) ⇔ s'(_gen_0':s':nil':cons':double':1':bug_list_not'3(x))

No more defined symbols left to analyse.

The lowerbound Ω(n) was proven with the following lemma:
eq'(_gen_0':s':nil':cons':double':1':bug_list_not'3(_n5), _gen_0':s':nil':cons':double':1':bug_list_not'3(_n5)) → true', rt ∈ Ω(1 + n5)