WORST_CASE(Omega(n^1),?)
proof of input_7cJ0rVaOJ6.trs
# AProVE Commit ID: aff8ecad908e01718a4c36e68d2e55d5e0f16e15 fuhs 20220216 unpublished


The Runtime Complexity (parallel-innermost) of the given CpxTRS could be proven to be BOUNDS(n^1, INF).

(0) CpxTRS
(1) CpxTrsToCdtProof [BOTH BOUNDS(ID, ID), 0 ms]
(2) CdtProblem
(3) CdtToCpxRelTrsProof [BOTH BOUNDS(ID, ID), 0 ms]
(4) CpxRelTRS
(5) RenamingProof [BOTH BOUNDS(ID, ID), 0 ms]
(6) CpxRelTRS
(7) TypeInferenceProof [BOTH BOUNDS(ID, ID), 0 ms]
(8) typed CpxTrs
(9) OrderProof [LOWER BOUND(ID), 37 ms]
(10) typed CpxTrs
(11) RewriteLemmaProof [LOWER BOUND(ID), 370 ms]
(12) BEST
    (13) proven lower bound
        (14) LowerBoundPropagationProof [FINISHED, 0 ms]
        (15) BOUNDS(n^1, INF)
    (16) typed CpxTrs
        (17) RewriteLemmaProof [LOWER BOUND(ID), 153 ms]
        (18) typed CpxTrs
        (19) RewriteLemmaProof [LOWER BOUND(ID), 67 ms]
        (20) typed CpxTrs
        (21) RewriteLemmaProof [LOWER BOUND(ID), 26 ms]
        (22) typed CpxTrs
        (23) RewriteLemmaProof [LOWER BOUND(ID), 46 ms]
        (24) typed CpxTrs
        (25) RewriteLemmaProof [LOWER BOUND(ID), 32 ms]
        (26) typed CpxTrs


----------------------------------------

(0)
Obligation:
The Runtime Complexity (parallel-innermost) of the given CpxTRS could be proven to be BOUNDS(n^1, INF).


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)

S is empty.
Rewrite Strategy: PARALLEL_INNERMOST
----------------------------------------

(1) CpxTrsToCdtProof (BOTH BOUNDS(ID, ID))
Converted Cpx (relative) TRS with rewrite strategy PARALLEL_INNERMOST to CDT
----------------------------------------

(2)
Obligation:
Complexity Dependency Tuples Problem

Rules:
   eq(0, 0) -> true
   eq(0, s(z0)) -> false
   eq(s(z0), 0) -> false
   eq(s(z0), s(z1)) -> eq(z0, z1)
   lt(0, s(z0)) -> true
   lt(z0, 0) -> false
   lt(s(z0), s(z1)) -> lt(z0, z1)
   bin2s(nil) -> 0
   bin2s(cons(z0, z1)) -> bin2ss(z0, z1)
   bin2ss(z0, nil) -> z0
   bin2ss(z0, cons(0, z1)) -> bin2ss(double(z0), z1)
   bin2ss(z0, cons(1, z1)) -> bin2ss(s(double(z0)), z1)
   half(0) -> 0
   half(s(0)) -> 0
   half(s(s(z0))) -> s(half(z0))
   log(0) -> 0
   log(s(0)) -> 0
   log(s(s(z0))) -> s(log(half(s(s(z0)))))
   more(nil) -> nil
   more(cons(z0, z1)) -> cons(cons(0, z0), cons(cons(1, z0), cons(z0, z1)))
   s2bin(z0) -> s2bin1(z0, 0, cons(nil, nil))
   s2bin1(z0, z1, z2) -> if1(lt(z1, log(z0)), z0, z1, z2)
   if1(true, z0, z1, z2) -> s2bin1(z0, s(z1), more(z2))
   if1(false, z0, z1, z2) -> s2bin2(z0, z2)
   s2bin2(z0, nil) -> bug_list_not
   s2bin2(z0, cons(z1, z2)) -> if2(eq(z0, bin2s(z1)), z0, z1, z2)
   if2(true, z0, z1, z2) -> z1
   if2(false, z0, z1, z2) -> s2bin2(z0, z2)
Tuples:
   EQ(0, 0) -> c
   EQ(0, s(z0)) -> c1
   EQ(s(z0), 0) -> c2
   EQ(s(z0), s(z1)) -> c3(EQ(z0, z1))
   LT(0, s(z0)) -> c4
   LT(z0, 0) -> c5
   LT(s(z0), s(z1)) -> c6(LT(z0, z1))
   BIN2S(nil) -> c7
   BIN2S(cons(z0, z1)) -> c8(BIN2SS(z0, z1))
   BIN2SS(z0, nil) -> c9
   BIN2SS(z0, cons(0, z1)) -> c10(BIN2SS(double(z0), z1))
   BIN2SS(z0, cons(1, z1)) -> c11(BIN2SS(s(double(z0)), z1))
   HALF(0) -> c12
   HALF(s(0)) -> c13
   HALF(s(s(z0))) -> c14(HALF(z0))
   LOG(0) -> c15
   LOG(s(0)) -> c16
   LOG(s(s(z0))) -> c17(LOG(half(s(s(z0)))), HALF(s(s(z0))))
   MORE(nil) -> c18
   MORE(cons(z0, z1)) -> c19
   S2BIN(z0) -> c20(S2BIN1(z0, 0, cons(nil, nil)))
   S2BIN1(z0, z1, z2) -> c21(IF1(lt(z1, log(z0)), z0, z1, z2), LT(z1, log(z0)), LOG(z0))
   IF1(true, z0, z1, z2) -> c22(S2BIN1(z0, s(z1), more(z2)), MORE(z2))
   IF1(false, z0, z1, z2) -> c23(S2BIN2(z0, z2))
   S2BIN2(z0, nil) -> c24
   S2BIN2(z0, cons(z1, z2)) -> c25(IF2(eq(z0, bin2s(z1)), z0, z1, z2), EQ(z0, bin2s(z1)), BIN2S(z1))
   IF2(true, z0, z1, z2) -> c26
   IF2(false, z0, z1, z2) -> c27(S2BIN2(z0, z2))
S tuples:
   EQ(0, 0) -> c
   EQ(0, s(z0)) -> c1
   EQ(s(z0), 0) -> c2
   EQ(s(z0), s(z1)) -> c3(EQ(z0, z1))
   LT(0, s(z0)) -> c4
   LT(z0, 0) -> c5
   LT(s(z0), s(z1)) -> c6(LT(z0, z1))
   BIN2S(nil) -> c7
   BIN2S(cons(z0, z1)) -> c8(BIN2SS(z0, z1))
   BIN2SS(z0, nil) -> c9
   BIN2SS(z0, cons(0, z1)) -> c10(BIN2SS(double(z0), z1))
   BIN2SS(z0, cons(1, z1)) -> c11(BIN2SS(s(double(z0)), z1))
   HALF(0) -> c12
   HALF(s(0)) -> c13
   HALF(s(s(z0))) -> c14(HALF(z0))
   LOG(0) -> c15
   LOG(s(0)) -> c16
   LOG(s(s(z0))) -> c17(LOG(half(s(s(z0)))), HALF(s(s(z0))))
   MORE(nil) -> c18
   MORE(cons(z0, z1)) -> c19
   S2BIN(z0) -> c20(S2BIN1(z0, 0, cons(nil, nil)))
   S2BIN1(z0, z1, z2) -> c21(IF1(lt(z1, log(z0)), z0, z1, z2), LT(z1, log(z0)), LOG(z0))
   IF1(true, z0, z1, z2) -> c22(S2BIN1(z0, s(z1), more(z2)), MORE(z2))
   IF1(false, z0, z1, z2) -> c23(S2BIN2(z0, z2))
   S2BIN2(z0, nil) -> c24
   S2BIN2(z0, cons(z1, z2)) -> c25(IF2(eq(z0, bin2s(z1)), z0, z1, z2), EQ(z0, bin2s(z1)), BIN2S(z1))
   IF2(true, z0, z1, z2) -> c26
   IF2(false, z0, z1, z2) -> c27(S2BIN2(z0, z2))
K tuples:none
Defined Rule Symbols:   eq_2, lt_2, bin2s_1, bin2ss_2, half_1, log_1, more_1, s2bin_1, s2bin1_3, if1_4, s2bin2_2, if2_4

Defined Pair Symbols:   EQ_2, LT_2, BIN2S_1, BIN2SS_2, HALF_1, LOG_1, MORE_1, S2BIN_1, S2BIN1_3, IF1_4, S2BIN2_2, IF2_4

Compound Symbols:   c, c1, c2, c3_1, c4, c5, c6_1, c7, c8_1, c9, c10_1, c11_1, c12, c13, c14_1, c15, c16, c17_2, c18, c19, c20_1, c21_3, c22_2, c23_1, c24, c25_3, c26, c27_1


----------------------------------------

(3) CdtToCpxRelTrsProof (BOTH BOUNDS(ID, ID))
Converted S to standard rules, and D \ S as well as R to relative rules.
----------------------------------------

(4)
Obligation:
The Runtime Complexity (innermost) of the given CpxRelTRS could be proven to be BOUNDS(n^1, INF).


The TRS R consists of the following rules:

   EQ(0, 0) -> c
   EQ(0, s(z0)) -> c1
   EQ(s(z0), 0) -> c2
   EQ(s(z0), s(z1)) -> c3(EQ(z0, z1))
   LT(0, s(z0)) -> c4
   LT(z0, 0) -> c5
   LT(s(z0), s(z1)) -> c6(LT(z0, z1))
   BIN2S(nil) -> c7
   BIN2S(cons(z0, z1)) -> c8(BIN2SS(z0, z1))
   BIN2SS(z0, nil) -> c9
   BIN2SS(z0, cons(0, z1)) -> c10(BIN2SS(double(z0), z1))
   BIN2SS(z0, cons(1, z1)) -> c11(BIN2SS(s(double(z0)), z1))
   HALF(0) -> c12
   HALF(s(0)) -> c13
   HALF(s(s(z0))) -> c14(HALF(z0))
   LOG(0) -> c15
   LOG(s(0)) -> c16
   LOG(s(s(z0))) -> c17(LOG(half(s(s(z0)))), HALF(s(s(z0))))
   MORE(nil) -> c18
   MORE(cons(z0, z1)) -> c19
   S2BIN(z0) -> c20(S2BIN1(z0, 0, cons(nil, nil)))
   S2BIN1(z0, z1, z2) -> c21(IF1(lt(z1, log(z0)), z0, z1, z2), LT(z1, log(z0)), LOG(z0))
   IF1(true, z0, z1, z2) -> c22(S2BIN1(z0, s(z1), more(z2)), MORE(z2))
   IF1(false, z0, z1, z2) -> c23(S2BIN2(z0, z2))
   S2BIN2(z0, nil) -> c24
   S2BIN2(z0, cons(z1, z2)) -> c25(IF2(eq(z0, bin2s(z1)), z0, z1, z2), EQ(z0, bin2s(z1)), BIN2S(z1))
   IF2(true, z0, z1, z2) -> c26
   IF2(false, z0, z1, z2) -> c27(S2BIN2(z0, z2))

The (relative) TRS S consists of the following rules:

   eq(0, 0) -> true
   eq(0, s(z0)) -> false
   eq(s(z0), 0) -> false
   eq(s(z0), s(z1)) -> eq(z0, z1)
   lt(0, s(z0)) -> true
   lt(z0, 0) -> false
   lt(s(z0), s(z1)) -> lt(z0, z1)
   bin2s(nil) -> 0
   bin2s(cons(z0, z1)) -> bin2ss(z0, z1)
   bin2ss(z0, nil) -> z0
   bin2ss(z0, cons(0, z1)) -> bin2ss(double(z0), z1)
   bin2ss(z0, cons(1, z1)) -> bin2ss(s(double(z0)), z1)
   half(0) -> 0
   half(s(0)) -> 0
   half(s(s(z0))) -> s(half(z0))
   log(0) -> 0
   log(s(0)) -> 0
   log(s(s(z0))) -> s(log(half(s(s(z0)))))
   more(nil) -> nil
   more(cons(z0, z1)) -> cons(cons(0, z0), cons(cons(1, z0), cons(z0, z1)))
   s2bin(z0) -> s2bin1(z0, 0, cons(nil, nil))
   s2bin1(z0, z1, z2) -> if1(lt(z1, log(z0)), z0, z1, z2)
   if1(true, z0, z1, z2) -> s2bin1(z0, s(z1), more(z2))
   if1(false, z0, z1, z2) -> s2bin2(z0, z2)
   s2bin2(z0, nil) -> bug_list_not
   s2bin2(z0, cons(z1, z2)) -> if2(eq(z0, bin2s(z1)), z0, z1, z2)
   if2(true, z0, z1, z2) -> z1
   if2(false, z0, z1, z2) -> s2bin2(z0, z2)

Rewrite Strategy: INNERMOST
----------------------------------------

(5) RenamingProof (BOTH BOUNDS(ID, ID))
Renamed function symbols to avoid clashes with predefined symbol.
----------------------------------------

(6)
Obligation:
The Runtime Complexity (innermost) of the given CpxRelTRS could be proven to be BOUNDS(n^1, INF).


The TRS R consists of the following rules:

   EQ(0', 0') -> c
   EQ(0', s(z0)) -> c1
   EQ(s(z0), 0') -> c2
   EQ(s(z0), s(z1)) -> c3(EQ(z0, z1))
   LT(0', s(z0)) -> c4
   LT(z0, 0') -> c5
   LT(s(z0), s(z1)) -> c6(LT(z0, z1))
   BIN2S(nil) -> c7
   BIN2S(cons(z0, z1)) -> c8(BIN2SS(z0, z1))
   BIN2SS(z0, nil) -> c9
   BIN2SS(z0, cons(0', z1)) -> c10(BIN2SS(double(z0), z1))
   BIN2SS(z0, cons(1', z1)) -> c11(BIN2SS(s(double(z0)), z1))
   HALF(0') -> c12
   HALF(s(0')) -> c13
   HALF(s(s(z0))) -> c14(HALF(z0))
   LOG(0') -> c15
   LOG(s(0')) -> c16
   LOG(s(s(z0))) -> c17(LOG(half(s(s(z0)))), HALF(s(s(z0))))
   MORE(nil) -> c18
   MORE(cons(z0, z1)) -> c19
   S2BIN(z0) -> c20(S2BIN1(z0, 0', cons(nil, nil)))
   S2BIN1(z0, z1, z2) -> c21(IF1(lt(z1, log(z0)), z0, z1, z2), LT(z1, log(z0)), LOG(z0))
   IF1(true, z0, z1, z2) -> c22(S2BIN1(z0, s(z1), more(z2)), MORE(z2))
   IF1(false, z0, z1, z2) -> c23(S2BIN2(z0, z2))
   S2BIN2(z0, nil) -> c24
   S2BIN2(z0, cons(z1, z2)) -> c25(IF2(eq(z0, bin2s(z1)), z0, z1, z2), EQ(z0, bin2s(z1)), BIN2S(z1))
   IF2(true, z0, z1, z2) -> c26
   IF2(false, z0, z1, z2) -> c27(S2BIN2(z0, z2))

The (relative) TRS S consists of the following rules:

   eq(0', 0') -> true
   eq(0', s(z0)) -> false
   eq(s(z0), 0') -> false
   eq(s(z0), s(z1)) -> eq(z0, z1)
   lt(0', s(z0)) -> true
   lt(z0, 0') -> false
   lt(s(z0), s(z1)) -> lt(z0, z1)
   bin2s(nil) -> 0'
   bin2s(cons(z0, z1)) -> bin2ss(z0, z1)
   bin2ss(z0, nil) -> z0
   bin2ss(z0, cons(0', z1)) -> bin2ss(double(z0), z1)
   bin2ss(z0, cons(1', z1)) -> bin2ss(s(double(z0)), z1)
   half(0') -> 0'
   half(s(0')) -> 0'
   half(s(s(z0))) -> s(half(z0))
   log(0') -> 0'
   log(s(0')) -> 0'
   log(s(s(z0))) -> s(log(half(s(s(z0)))))
   more(nil) -> nil
   more(cons(z0, z1)) -> cons(cons(0', z0), cons(cons(1', z0), cons(z0, z1)))
   s2bin(z0) -> s2bin1(z0, 0', cons(nil, nil))
   s2bin1(z0, z1, z2) -> if1(lt(z1, log(z0)), z0, z1, z2)
   if1(true, z0, z1, z2) -> s2bin1(z0, s(z1), more(z2))
   if1(false, z0, z1, z2) -> s2bin2(z0, z2)
   s2bin2(z0, nil) -> bug_list_not
   s2bin2(z0, cons(z1, z2)) -> if2(eq(z0, bin2s(z1)), z0, z1, z2)
   if2(true, z0, z1, z2) -> z1
   if2(false, z0, z1, z2) -> s2bin2(z0, z2)

Rewrite Strategy: INNERMOST
----------------------------------------

(7) TypeInferenceProof (BOTH BOUNDS(ID, ID))
Inferred types.
----------------------------------------

(8)
Obligation:
Innermost TRS:
Rules:
EQ(0', 0') -> c
EQ(0', s(z0)) -> c1
EQ(s(z0), 0') -> c2
EQ(s(z0), s(z1)) -> c3(EQ(z0, z1))
LT(0', s(z0)) -> c4
LT(z0, 0') -> c5
LT(s(z0), s(z1)) -> c6(LT(z0, z1))
BIN2S(nil) -> c7
BIN2S(cons(z0, z1)) -> c8(BIN2SS(z0, z1))
BIN2SS(z0, nil) -> c9
BIN2SS(z0, cons(0', z1)) -> c10(BIN2SS(double(z0), z1))
BIN2SS(z0, cons(1', z1)) -> c11(BIN2SS(s(double(z0)), z1))
HALF(0') -> c12
HALF(s(0')) -> c13
HALF(s(s(z0))) -> c14(HALF(z0))
LOG(0') -> c15
LOG(s(0')) -> c16
LOG(s(s(z0))) -> c17(LOG(half(s(s(z0)))), HALF(s(s(z0))))
MORE(nil) -> c18
MORE(cons(z0, z1)) -> c19
S2BIN(z0) -> c20(S2BIN1(z0, 0', cons(nil, nil)))
S2BIN1(z0, z1, z2) -> c21(IF1(lt(z1, log(z0)), z0, z1, z2), LT(z1, log(z0)), LOG(z0))
IF1(true, z0, z1, z2) -> c22(S2BIN1(z0, s(z1), more(z2)), MORE(z2))
IF1(false, z0, z1, z2) -> c23(S2BIN2(z0, z2))
S2BIN2(z0, nil) -> c24
S2BIN2(z0, cons(z1, z2)) -> c25(IF2(eq(z0, bin2s(z1)), z0, z1, z2), EQ(z0, bin2s(z1)), BIN2S(z1))
IF2(true, z0, z1, z2) -> c26
IF2(false, z0, z1, z2) -> c27(S2BIN2(z0, z2))
eq(0', 0') -> true
eq(0', s(z0)) -> false
eq(s(z0), 0') -> false
eq(s(z0), s(z1)) -> eq(z0, z1)
lt(0', s(z0)) -> true
lt(z0, 0') -> false
lt(s(z0), s(z1)) -> lt(z0, z1)
bin2s(nil) -> 0'
bin2s(cons(z0, z1)) -> bin2ss(z0, z1)
bin2ss(z0, nil) -> z0
bin2ss(z0, cons(0', z1)) -> bin2ss(double(z0), z1)
bin2ss(z0, cons(1', z1)) -> bin2ss(s(double(z0)), z1)
half(0') -> 0'
half(s(0')) -> 0'
half(s(s(z0))) -> s(half(z0))
log(0') -> 0'
log(s(0')) -> 0'
log(s(s(z0))) -> s(log(half(s(s(z0)))))
more(nil) -> nil
more(cons(z0, z1)) -> cons(cons(0', z0), cons(cons(1', z0), cons(z0, z1)))
s2bin(z0) -> s2bin1(z0, 0', cons(nil, nil))
s2bin1(z0, z1, z2) -> if1(lt(z1, log(z0)), z0, z1, z2)
if1(true, z0, z1, z2) -> s2bin1(z0, s(z1), more(z2))
if1(false, z0, z1, z2) -> s2bin2(z0, z2)
s2bin2(z0, nil) -> bug_list_not
s2bin2(z0, cons(z1, z2)) -> if2(eq(z0, bin2s(z1)), z0, z1, z2)
if2(true, z0, z1, z2) -> z1
if2(false, z0, z1, z2) -> s2bin2(z0, z2)

Types:
EQ :: 0':s:nil:cons:double:1':bug_list_not -> 0':s:nil:cons:double:1':bug_list_not -> c:c1:c2:c3
0' :: 0':s:nil:cons:double:1':bug_list_not
c :: c:c1:c2:c3
s :: 0':s:nil:cons:double:1':bug_list_not -> 0':s:nil:cons:double:1':bug_list_not
c1 :: c:c1:c2:c3
c2 :: c:c1:c2:c3
c3 :: c:c1:c2:c3 -> c:c1:c2:c3
LT :: 0':s:nil:cons:double:1':bug_list_not -> 0':s:nil:cons:double:1':bug_list_not -> c4:c5:c6
c4 :: c4:c5:c6
c5 :: c4:c5:c6
c6 :: c4:c5:c6 -> c4:c5:c6
BIN2S :: 0':s:nil:cons:double:1':bug_list_not -> c7:c8
nil :: 0':s:nil:cons:double:1':bug_list_not
c7 :: c7:c8
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
c8 :: c9:c10:c11 -> c7:c8
BIN2SS :: 0':s:nil:cons:double:1':bug_list_not -> 0':s:nil:cons:double:1':bug_list_not -> c9:c10:c11
c9 :: c9:c10:c11
c10 :: c9:c10:c11 -> c9:c10:c11
double :: 0':s:nil:cons:double:1':bug_list_not -> 0':s:nil:cons:double:1':bug_list_not
1' :: 0':s:nil:cons:double:1':bug_list_not
c11 :: c9:c10:c11 -> c9:c10:c11
HALF :: 0':s:nil:cons:double:1':bug_list_not -> c12:c13:c14
c12 :: c12:c13:c14
c13 :: c12:c13:c14
c14 :: c12:c13:c14 -> c12:c13:c14
LOG :: 0':s:nil:cons:double:1':bug_list_not -> c15:c16:c17
c15 :: c15:c16:c17
c16 :: c15:c16:c17
c17 :: c15:c16:c17 -> c12:c13:c14 -> c15:c16:c17
half :: 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 -> c18:c19
c18 :: c18:c19
c19 :: c18:c19
S2BIN :: 0':s:nil:cons:double:1':bug_list_not -> c20
c20 :: c21 -> c20
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 -> c21
c21 :: c22:c23 -> c4:c5:c6 -> c15:c16:c17 -> c21
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 -> c22:c23
lt :: 0':s:nil:cons:double:1':bug_list_not -> 0':s:nil:cons:double:1':bug_list_not -> true:false
log :: 0':s:nil:cons:double:1':bug_list_not -> 0':s:nil:cons:double:1':bug_list_not
true :: true:false
c22 :: c21 -> c18:c19 -> c22:c23
more :: 0':s:nil:cons:double:1':bug_list_not -> 0':s:nil:cons:double:1':bug_list_not
false :: true:false
c23 :: c24:c25 -> c22:c23
S2BIN2 :: 0':s:nil:cons:double:1':bug_list_not -> 0':s:nil:cons:double:1':bug_list_not -> c24:c25
c24 :: c24:c25
c25 :: c26:c27 -> c:c1:c2:c3 -> c7:c8 -> c24:c25
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 -> c26:c27
eq :: 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
c26 :: c26:c27
c27 :: c24:c25 -> c26:c27
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
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_c:c1:c2:c31_28 :: c:c1:c2:c3
hole_0':s:nil:cons:double:1':bug_list_not2_28 :: 0':s:nil:cons:double:1':bug_list_not
hole_c4:c5:c63_28 :: c4:c5:c6
hole_c7:c84_28 :: c7:c8
hole_c9:c10:c115_28 :: c9:c10:c11
hole_c12:c13:c146_28 :: c12:c13:c14
hole_c15:c16:c177_28 :: c15:c16:c17
hole_c18:c198_28 :: c18:c19
hole_c209_28 :: c20
hole_c2110_28 :: c21
hole_c22:c2311_28 :: c22:c23
hole_true:false12_28 :: true:false
hole_c24:c2513_28 :: c24:c25
hole_c26:c2714_28 :: c26:c27
gen_c:c1:c2:c315_28 :: Nat -> c:c1:c2:c3
gen_0':s:nil:cons:double:1':bug_list_not16_28 :: Nat -> 0':s:nil:cons:double:1':bug_list_not
gen_c4:c5:c617_28 :: Nat -> c4:c5:c6
gen_c9:c10:c1118_28 :: Nat -> c9:c10:c11
gen_c12:c13:c1419_28 :: Nat -> c12:c13:c14
gen_c15:c16:c1720_28 :: Nat -> c15:c16:c17

----------------------------------------

(9) OrderProof (LOWER BOUND(ID))
Heuristically decided to analyse the following defined symbols:
EQ, LT, BIN2SS, HALF, LOG, half, S2BIN1, lt, log, S2BIN2, eq, bin2ss, s2bin1, s2bin2

They will be analysed ascendingly in the following order:
EQ < S2BIN2
LT < S2BIN1
HALF < LOG
half < LOG
LOG < S2BIN1
half < log
lt < S2BIN1
log < S2BIN1
S2BIN2 < S2BIN1
lt < s2bin1
log < s2bin1
eq < S2BIN2
eq < s2bin2
s2bin2 < s2bin1

----------------------------------------

(10)
Obligation:
Innermost TRS:
Rules:
EQ(0', 0') -> c
EQ(0', s(z0)) -> c1
EQ(s(z0), 0') -> c2
EQ(s(z0), s(z1)) -> c3(EQ(z0, z1))
LT(0', s(z0)) -> c4
LT(z0, 0') -> c5
LT(s(z0), s(z1)) -> c6(LT(z0, z1))
BIN2S(nil) -> c7
BIN2S(cons(z0, z1)) -> c8(BIN2SS(z0, z1))
BIN2SS(z0, nil) -> c9
BIN2SS(z0, cons(0', z1)) -> c10(BIN2SS(double(z0), z1))
BIN2SS(z0, cons(1', z1)) -> c11(BIN2SS(s(double(z0)), z1))
HALF(0') -> c12
HALF(s(0')) -> c13
HALF(s(s(z0))) -> c14(HALF(z0))
LOG(0') -> c15
LOG(s(0')) -> c16
LOG(s(s(z0))) -> c17(LOG(half(s(s(z0)))), HALF(s(s(z0))))
MORE(nil) -> c18
MORE(cons(z0, z1)) -> c19
S2BIN(z0) -> c20(S2BIN1(z0, 0', cons(nil, nil)))
S2BIN1(z0, z1, z2) -> c21(IF1(lt(z1, log(z0)), z0, z1, z2), LT(z1, log(z0)), LOG(z0))
IF1(true, z0, z1, z2) -> c22(S2BIN1(z0, s(z1), more(z2)), MORE(z2))
IF1(false, z0, z1, z2) -> c23(S2BIN2(z0, z2))
S2BIN2(z0, nil) -> c24
S2BIN2(z0, cons(z1, z2)) -> c25(IF2(eq(z0, bin2s(z1)), z0, z1, z2), EQ(z0, bin2s(z1)), BIN2S(z1))
IF2(true, z0, z1, z2) -> c26
IF2(false, z0, z1, z2) -> c27(S2BIN2(z0, z2))
eq(0', 0') -> true
eq(0', s(z0)) -> false
eq(s(z0), 0') -> false
eq(s(z0), s(z1)) -> eq(z0, z1)
lt(0', s(z0)) -> true
lt(z0, 0') -> false
lt(s(z0), s(z1)) -> lt(z0, z1)
bin2s(nil) -> 0'
bin2s(cons(z0, z1)) -> bin2ss(z0, z1)
bin2ss(z0, nil) -> z0
bin2ss(z0, cons(0', z1)) -> bin2ss(double(z0), z1)
bin2ss(z0, cons(1', z1)) -> bin2ss(s(double(z0)), z1)
half(0') -> 0'
half(s(0')) -> 0'
half(s(s(z0))) -> s(half(z0))
log(0') -> 0'
log(s(0')) -> 0'
log(s(s(z0))) -> s(log(half(s(s(z0)))))
more(nil) -> nil
more(cons(z0, z1)) -> cons(cons(0', z0), cons(cons(1', z0), cons(z0, z1)))
s2bin(z0) -> s2bin1(z0, 0', cons(nil, nil))
s2bin1(z0, z1, z2) -> if1(lt(z1, log(z0)), z0, z1, z2)
if1(true, z0, z1, z2) -> s2bin1(z0, s(z1), more(z2))
if1(false, z0, z1, z2) -> s2bin2(z0, z2)
s2bin2(z0, nil) -> bug_list_not
s2bin2(z0, cons(z1, z2)) -> if2(eq(z0, bin2s(z1)), z0, z1, z2)
if2(true, z0, z1, z2) -> z1
if2(false, z0, z1, z2) -> s2bin2(z0, z2)

Types:
EQ :: 0':s:nil:cons:double:1':bug_list_not -> 0':s:nil:cons:double:1':bug_list_not -> c:c1:c2:c3
0' :: 0':s:nil:cons:double:1':bug_list_not
c :: c:c1:c2:c3
s :: 0':s:nil:cons:double:1':bug_list_not -> 0':s:nil:cons:double:1':bug_list_not
c1 :: c:c1:c2:c3
c2 :: c:c1:c2:c3
c3 :: c:c1:c2:c3 -> c:c1:c2:c3
LT :: 0':s:nil:cons:double:1':bug_list_not -> 0':s:nil:cons:double:1':bug_list_not -> c4:c5:c6
c4 :: c4:c5:c6
c5 :: c4:c5:c6
c6 :: c4:c5:c6 -> c4:c5:c6
BIN2S :: 0':s:nil:cons:double:1':bug_list_not -> c7:c8
nil :: 0':s:nil:cons:double:1':bug_list_not
c7 :: c7:c8
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
c8 :: c9:c10:c11 -> c7:c8
BIN2SS :: 0':s:nil:cons:double:1':bug_list_not -> 0':s:nil:cons:double:1':bug_list_not -> c9:c10:c11
c9 :: c9:c10:c11
c10 :: c9:c10:c11 -> c9:c10:c11
double :: 0':s:nil:cons:double:1':bug_list_not -> 0':s:nil:cons:double:1':bug_list_not
1' :: 0':s:nil:cons:double:1':bug_list_not
c11 :: c9:c10:c11 -> c9:c10:c11
HALF :: 0':s:nil:cons:double:1':bug_list_not -> c12:c13:c14
c12 :: c12:c13:c14
c13 :: c12:c13:c14
c14 :: c12:c13:c14 -> c12:c13:c14
LOG :: 0':s:nil:cons:double:1':bug_list_not -> c15:c16:c17
c15 :: c15:c16:c17
c16 :: c15:c16:c17
c17 :: c15:c16:c17 -> c12:c13:c14 -> c15:c16:c17
half :: 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 -> c18:c19
c18 :: c18:c19
c19 :: c18:c19
S2BIN :: 0':s:nil:cons:double:1':bug_list_not -> c20
c20 :: c21 -> c20
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 -> c21
c21 :: c22:c23 -> c4:c5:c6 -> c15:c16:c17 -> c21
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 -> c22:c23
lt :: 0':s:nil:cons:double:1':bug_list_not -> 0':s:nil:cons:double:1':bug_list_not -> true:false
log :: 0':s:nil:cons:double:1':bug_list_not -> 0':s:nil:cons:double:1':bug_list_not
true :: true:false
c22 :: c21 -> c18:c19 -> c22:c23
more :: 0':s:nil:cons:double:1':bug_list_not -> 0':s:nil:cons:double:1':bug_list_not
false :: true:false
c23 :: c24:c25 -> c22:c23
S2BIN2 :: 0':s:nil:cons:double:1':bug_list_not -> 0':s:nil:cons:double:1':bug_list_not -> c24:c25
c24 :: c24:c25
c25 :: c26:c27 -> c:c1:c2:c3 -> c7:c8 -> c24:c25
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 -> c26:c27
eq :: 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
c26 :: c26:c27
c27 :: c24:c25 -> c26:c27
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
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_c:c1:c2:c31_28 :: c:c1:c2:c3
hole_0':s:nil:cons:double:1':bug_list_not2_28 :: 0':s:nil:cons:double:1':bug_list_not
hole_c4:c5:c63_28 :: c4:c5:c6
hole_c7:c84_28 :: c7:c8
hole_c9:c10:c115_28 :: c9:c10:c11
hole_c12:c13:c146_28 :: c12:c13:c14
hole_c15:c16:c177_28 :: c15:c16:c17
hole_c18:c198_28 :: c18:c19
hole_c209_28 :: c20
hole_c2110_28 :: c21
hole_c22:c2311_28 :: c22:c23
hole_true:false12_28 :: true:false
hole_c24:c2513_28 :: c24:c25
hole_c26:c2714_28 :: c26:c27
gen_c:c1:c2:c315_28 :: Nat -> c:c1:c2:c3
gen_0':s:nil:cons:double:1':bug_list_not16_28 :: Nat -> 0':s:nil:cons:double:1':bug_list_not
gen_c4:c5:c617_28 :: Nat -> c4:c5:c6
gen_c9:c10:c1118_28 :: Nat -> c9:c10:c11
gen_c12:c13:c1419_28 :: Nat -> c12:c13:c14
gen_c15:c16:c1720_28 :: Nat -> c15:c16:c17


Generator Equations:
gen_c:c1:c2:c315_28(0) <=> c
gen_c:c1:c2:c315_28(+(x, 1)) <=> c3(gen_c:c1:c2:c315_28(x))
gen_0':s:nil:cons:double:1':bug_list_not16_28(0) <=> 0'
gen_0':s:nil:cons:double:1':bug_list_not16_28(+(x, 1)) <=> s(gen_0':s:nil:cons:double:1':bug_list_not16_28(x))
gen_c4:c5:c617_28(0) <=> c4
gen_c4:c5:c617_28(+(x, 1)) <=> c6(gen_c4:c5:c617_28(x))
gen_c9:c10:c1118_28(0) <=> c9
gen_c9:c10:c1118_28(+(x, 1)) <=> c10(gen_c9:c10:c1118_28(x))
gen_c12:c13:c1419_28(0) <=> c12
gen_c12:c13:c1419_28(+(x, 1)) <=> c14(gen_c12:c13:c1419_28(x))
gen_c15:c16:c1720_28(0) <=> c15
gen_c15:c16:c1720_28(+(x, 1)) <=> c17(gen_c15:c16:c1720_28(x), c12)


The following defined symbols remain to be analysed:
EQ, LT, BIN2SS, HALF, LOG, half, S2BIN1, lt, log, S2BIN2, eq, bin2ss, s2bin1, s2bin2

They will be analysed ascendingly in the following order:
EQ < S2BIN2
LT < S2BIN1
HALF < LOG
half < LOG
LOG < S2BIN1
half < log
lt < S2BIN1
log < S2BIN1
S2BIN2 < S2BIN1
lt < s2bin1
log < s2bin1
eq < S2BIN2
eq < s2bin2
s2bin2 < s2bin1

----------------------------------------

(11) RewriteLemmaProof (LOWER BOUND(ID))
Proved the following rewrite lemma:
EQ(gen_0':s:nil:cons:double:1':bug_list_not16_28(n22_28), gen_0':s:nil:cons:double:1':bug_list_not16_28(n22_28)) -> gen_c:c1:c2:c315_28(n22_28), rt in Omega(1 + n22_28)

Induction Base:
EQ(gen_0':s:nil:cons:double:1':bug_list_not16_28(0), gen_0':s:nil:cons:double:1':bug_list_not16_28(0)) ->_R^Omega(1)
c

Induction Step:
EQ(gen_0':s:nil:cons:double:1':bug_list_not16_28(+(n22_28, 1)), gen_0':s:nil:cons:double:1':bug_list_not16_28(+(n22_28, 1))) ->_R^Omega(1)
c3(EQ(gen_0':s:nil:cons:double:1':bug_list_not16_28(n22_28), gen_0':s:nil:cons:double:1':bug_list_not16_28(n22_28))) ->_IH
c3(gen_c:c1:c2:c315_28(c23_28))

We have rt in Omega(n^1) and sz in O(n). Thus, we have irc_R in Omega(n).
----------------------------------------

(12)
Complex Obligation (BEST)

----------------------------------------

(13)
Obligation:
Proved the lower bound n^1 for the following obligation:

Innermost TRS:
Rules:
EQ(0', 0') -> c
EQ(0', s(z0)) -> c1
EQ(s(z0), 0') -> c2
EQ(s(z0), s(z1)) -> c3(EQ(z0, z1))
LT(0', s(z0)) -> c4
LT(z0, 0') -> c5
LT(s(z0), s(z1)) -> c6(LT(z0, z1))
BIN2S(nil) -> c7
BIN2S(cons(z0, z1)) -> c8(BIN2SS(z0, z1))
BIN2SS(z0, nil) -> c9
BIN2SS(z0, cons(0', z1)) -> c10(BIN2SS(double(z0), z1))
BIN2SS(z0, cons(1', z1)) -> c11(BIN2SS(s(double(z0)), z1))
HALF(0') -> c12
HALF(s(0')) -> c13
HALF(s(s(z0))) -> c14(HALF(z0))
LOG(0') -> c15
LOG(s(0')) -> c16
LOG(s(s(z0))) -> c17(LOG(half(s(s(z0)))), HALF(s(s(z0))))
MORE(nil) -> c18
MORE(cons(z0, z1)) -> c19
S2BIN(z0) -> c20(S2BIN1(z0, 0', cons(nil, nil)))
S2BIN1(z0, z1, z2) -> c21(IF1(lt(z1, log(z0)), z0, z1, z2), LT(z1, log(z0)), LOG(z0))
IF1(true, z0, z1, z2) -> c22(S2BIN1(z0, s(z1), more(z2)), MORE(z2))
IF1(false, z0, z1, z2) -> c23(S2BIN2(z0, z2))
S2BIN2(z0, nil) -> c24
S2BIN2(z0, cons(z1, z2)) -> c25(IF2(eq(z0, bin2s(z1)), z0, z1, z2), EQ(z0, bin2s(z1)), BIN2S(z1))
IF2(true, z0, z1, z2) -> c26
IF2(false, z0, z1, z2) -> c27(S2BIN2(z0, z2))
eq(0', 0') -> true
eq(0', s(z0)) -> false
eq(s(z0), 0') -> false
eq(s(z0), s(z1)) -> eq(z0, z1)
lt(0', s(z0)) -> true
lt(z0, 0') -> false
lt(s(z0), s(z1)) -> lt(z0, z1)
bin2s(nil) -> 0'
bin2s(cons(z0, z1)) -> bin2ss(z0, z1)
bin2ss(z0, nil) -> z0
bin2ss(z0, cons(0', z1)) -> bin2ss(double(z0), z1)
bin2ss(z0, cons(1', z1)) -> bin2ss(s(double(z0)), z1)
half(0') -> 0'
half(s(0')) -> 0'
half(s(s(z0))) -> s(half(z0))
log(0') -> 0'
log(s(0')) -> 0'
log(s(s(z0))) -> s(log(half(s(s(z0)))))
more(nil) -> nil
more(cons(z0, z1)) -> cons(cons(0', z0), cons(cons(1', z0), cons(z0, z1)))
s2bin(z0) -> s2bin1(z0, 0', cons(nil, nil))
s2bin1(z0, z1, z2) -> if1(lt(z1, log(z0)), z0, z1, z2)
if1(true, z0, z1, z2) -> s2bin1(z0, s(z1), more(z2))
if1(false, z0, z1, z2) -> s2bin2(z0, z2)
s2bin2(z0, nil) -> bug_list_not
s2bin2(z0, cons(z1, z2)) -> if2(eq(z0, bin2s(z1)), z0, z1, z2)
if2(true, z0, z1, z2) -> z1
if2(false, z0, z1, z2) -> s2bin2(z0, z2)

Types:
EQ :: 0':s:nil:cons:double:1':bug_list_not -> 0':s:nil:cons:double:1':bug_list_not -> c:c1:c2:c3
0' :: 0':s:nil:cons:double:1':bug_list_not
c :: c:c1:c2:c3
s :: 0':s:nil:cons:double:1':bug_list_not -> 0':s:nil:cons:double:1':bug_list_not
c1 :: c:c1:c2:c3
c2 :: c:c1:c2:c3
c3 :: c:c1:c2:c3 -> c:c1:c2:c3
LT :: 0':s:nil:cons:double:1':bug_list_not -> 0':s:nil:cons:double:1':bug_list_not -> c4:c5:c6
c4 :: c4:c5:c6
c5 :: c4:c5:c6
c6 :: c4:c5:c6 -> c4:c5:c6
BIN2S :: 0':s:nil:cons:double:1':bug_list_not -> c7:c8
nil :: 0':s:nil:cons:double:1':bug_list_not
c7 :: c7:c8
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
c8 :: c9:c10:c11 -> c7:c8
BIN2SS :: 0':s:nil:cons:double:1':bug_list_not -> 0':s:nil:cons:double:1':bug_list_not -> c9:c10:c11
c9 :: c9:c10:c11
c10 :: c9:c10:c11 -> c9:c10:c11
double :: 0':s:nil:cons:double:1':bug_list_not -> 0':s:nil:cons:double:1':bug_list_not
1' :: 0':s:nil:cons:double:1':bug_list_not
c11 :: c9:c10:c11 -> c9:c10:c11
HALF :: 0':s:nil:cons:double:1':bug_list_not -> c12:c13:c14
c12 :: c12:c13:c14
c13 :: c12:c13:c14
c14 :: c12:c13:c14 -> c12:c13:c14
LOG :: 0':s:nil:cons:double:1':bug_list_not -> c15:c16:c17
c15 :: c15:c16:c17
c16 :: c15:c16:c17
c17 :: c15:c16:c17 -> c12:c13:c14 -> c15:c16:c17
half :: 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 -> c18:c19
c18 :: c18:c19
c19 :: c18:c19
S2BIN :: 0':s:nil:cons:double:1':bug_list_not -> c20
c20 :: c21 -> c20
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 -> c21
c21 :: c22:c23 -> c4:c5:c6 -> c15:c16:c17 -> c21
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 -> c22:c23
lt :: 0':s:nil:cons:double:1':bug_list_not -> 0':s:nil:cons:double:1':bug_list_not -> true:false
log :: 0':s:nil:cons:double:1':bug_list_not -> 0':s:nil:cons:double:1':bug_list_not
true :: true:false
c22 :: c21 -> c18:c19 -> c22:c23
more :: 0':s:nil:cons:double:1':bug_list_not -> 0':s:nil:cons:double:1':bug_list_not
false :: true:false
c23 :: c24:c25 -> c22:c23
S2BIN2 :: 0':s:nil:cons:double:1':bug_list_not -> 0':s:nil:cons:double:1':bug_list_not -> c24:c25
c24 :: c24:c25
c25 :: c26:c27 -> c:c1:c2:c3 -> c7:c8 -> c24:c25
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 -> c26:c27
eq :: 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
c26 :: c26:c27
c27 :: c24:c25 -> c26:c27
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
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_c:c1:c2:c31_28 :: c:c1:c2:c3
hole_0':s:nil:cons:double:1':bug_list_not2_28 :: 0':s:nil:cons:double:1':bug_list_not
hole_c4:c5:c63_28 :: c4:c5:c6
hole_c7:c84_28 :: c7:c8
hole_c9:c10:c115_28 :: c9:c10:c11
hole_c12:c13:c146_28 :: c12:c13:c14
hole_c15:c16:c177_28 :: c15:c16:c17
hole_c18:c198_28 :: c18:c19
hole_c209_28 :: c20
hole_c2110_28 :: c21
hole_c22:c2311_28 :: c22:c23
hole_true:false12_28 :: true:false
hole_c24:c2513_28 :: c24:c25
hole_c26:c2714_28 :: c26:c27
gen_c:c1:c2:c315_28 :: Nat -> c:c1:c2:c3
gen_0':s:nil:cons:double:1':bug_list_not16_28 :: Nat -> 0':s:nil:cons:double:1':bug_list_not
gen_c4:c5:c617_28 :: Nat -> c4:c5:c6
gen_c9:c10:c1118_28 :: Nat -> c9:c10:c11
gen_c12:c13:c1419_28 :: Nat -> c12:c13:c14
gen_c15:c16:c1720_28 :: Nat -> c15:c16:c17


Generator Equations:
gen_c:c1:c2:c315_28(0) <=> c
gen_c:c1:c2:c315_28(+(x, 1)) <=> c3(gen_c:c1:c2:c315_28(x))
gen_0':s:nil:cons:double:1':bug_list_not16_28(0) <=> 0'
gen_0':s:nil:cons:double:1':bug_list_not16_28(+(x, 1)) <=> s(gen_0':s:nil:cons:double:1':bug_list_not16_28(x))
gen_c4:c5:c617_28(0) <=> c4
gen_c4:c5:c617_28(+(x, 1)) <=> c6(gen_c4:c5:c617_28(x))
gen_c9:c10:c1118_28(0) <=> c9
gen_c9:c10:c1118_28(+(x, 1)) <=> c10(gen_c9:c10:c1118_28(x))
gen_c12:c13:c1419_28(0) <=> c12
gen_c12:c13:c1419_28(+(x, 1)) <=> c14(gen_c12:c13:c1419_28(x))
gen_c15:c16:c1720_28(0) <=> c15
gen_c15:c16:c1720_28(+(x, 1)) <=> c17(gen_c15:c16:c1720_28(x), c12)


The following defined symbols remain to be analysed:
EQ, LT, BIN2SS, HALF, LOG, half, S2BIN1, lt, log, S2BIN2, eq, bin2ss, s2bin1, s2bin2

They will be analysed ascendingly in the following order:
EQ < S2BIN2
LT < S2BIN1
HALF < LOG
half < LOG
LOG < S2BIN1
half < log
lt < S2BIN1
log < S2BIN1
S2BIN2 < S2BIN1
lt < s2bin1
log < s2bin1
eq < S2BIN2
eq < s2bin2
s2bin2 < s2bin1

----------------------------------------

(14) LowerBoundPropagationProof (FINISHED)
Propagated lower bound.
----------------------------------------

(15)
BOUNDS(n^1, INF)

----------------------------------------

(16)
Obligation:
Innermost TRS:
Rules:
EQ(0', 0') -> c
EQ(0', s(z0)) -> c1
EQ(s(z0), 0') -> c2
EQ(s(z0), s(z1)) -> c3(EQ(z0, z1))
LT(0', s(z0)) -> c4
LT(z0, 0') -> c5
LT(s(z0), s(z1)) -> c6(LT(z0, z1))
BIN2S(nil) -> c7
BIN2S(cons(z0, z1)) -> c8(BIN2SS(z0, z1))
BIN2SS(z0, nil) -> c9
BIN2SS(z0, cons(0', z1)) -> c10(BIN2SS(double(z0), z1))
BIN2SS(z0, cons(1', z1)) -> c11(BIN2SS(s(double(z0)), z1))
HALF(0') -> c12
HALF(s(0')) -> c13
HALF(s(s(z0))) -> c14(HALF(z0))
LOG(0') -> c15
LOG(s(0')) -> c16
LOG(s(s(z0))) -> c17(LOG(half(s(s(z0)))), HALF(s(s(z0))))
MORE(nil) -> c18
MORE(cons(z0, z1)) -> c19
S2BIN(z0) -> c20(S2BIN1(z0, 0', cons(nil, nil)))
S2BIN1(z0, z1, z2) -> c21(IF1(lt(z1, log(z0)), z0, z1, z2), LT(z1, log(z0)), LOG(z0))
IF1(true, z0, z1, z2) -> c22(S2BIN1(z0, s(z1), more(z2)), MORE(z2))
IF1(false, z0, z1, z2) -> c23(S2BIN2(z0, z2))
S2BIN2(z0, nil) -> c24
S2BIN2(z0, cons(z1, z2)) -> c25(IF2(eq(z0, bin2s(z1)), z0, z1, z2), EQ(z0, bin2s(z1)), BIN2S(z1))
IF2(true, z0, z1, z2) -> c26
IF2(false, z0, z1, z2) -> c27(S2BIN2(z0, z2))
eq(0', 0') -> true
eq(0', s(z0)) -> false
eq(s(z0), 0') -> false
eq(s(z0), s(z1)) -> eq(z0, z1)
lt(0', s(z0)) -> true
lt(z0, 0') -> false
lt(s(z0), s(z1)) -> lt(z0, z1)
bin2s(nil) -> 0'
bin2s(cons(z0, z1)) -> bin2ss(z0, z1)
bin2ss(z0, nil) -> z0
bin2ss(z0, cons(0', z1)) -> bin2ss(double(z0), z1)
bin2ss(z0, cons(1', z1)) -> bin2ss(s(double(z0)), z1)
half(0') -> 0'
half(s(0')) -> 0'
half(s(s(z0))) -> s(half(z0))
log(0') -> 0'
log(s(0')) -> 0'
log(s(s(z0))) -> s(log(half(s(s(z0)))))
more(nil) -> nil
more(cons(z0, z1)) -> cons(cons(0', z0), cons(cons(1', z0), cons(z0, z1)))
s2bin(z0) -> s2bin1(z0, 0', cons(nil, nil))
s2bin1(z0, z1, z2) -> if1(lt(z1, log(z0)), z0, z1, z2)
if1(true, z0, z1, z2) -> s2bin1(z0, s(z1), more(z2))
if1(false, z0, z1, z2) -> s2bin2(z0, z2)
s2bin2(z0, nil) -> bug_list_not
s2bin2(z0, cons(z1, z2)) -> if2(eq(z0, bin2s(z1)), z0, z1, z2)
if2(true, z0, z1, z2) -> z1
if2(false, z0, z1, z2) -> s2bin2(z0, z2)

Types:
EQ :: 0':s:nil:cons:double:1':bug_list_not -> 0':s:nil:cons:double:1':bug_list_not -> c:c1:c2:c3
0' :: 0':s:nil:cons:double:1':bug_list_not
c :: c:c1:c2:c3
s :: 0':s:nil:cons:double:1':bug_list_not -> 0':s:nil:cons:double:1':bug_list_not
c1 :: c:c1:c2:c3
c2 :: c:c1:c2:c3
c3 :: c:c1:c2:c3 -> c:c1:c2:c3
LT :: 0':s:nil:cons:double:1':bug_list_not -> 0':s:nil:cons:double:1':bug_list_not -> c4:c5:c6
c4 :: c4:c5:c6
c5 :: c4:c5:c6
c6 :: c4:c5:c6 -> c4:c5:c6
BIN2S :: 0':s:nil:cons:double:1':bug_list_not -> c7:c8
nil :: 0':s:nil:cons:double:1':bug_list_not
c7 :: c7:c8
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
c8 :: c9:c10:c11 -> c7:c8
BIN2SS :: 0':s:nil:cons:double:1':bug_list_not -> 0':s:nil:cons:double:1':bug_list_not -> c9:c10:c11
c9 :: c9:c10:c11
c10 :: c9:c10:c11 -> c9:c10:c11
double :: 0':s:nil:cons:double:1':bug_list_not -> 0':s:nil:cons:double:1':bug_list_not
1' :: 0':s:nil:cons:double:1':bug_list_not
c11 :: c9:c10:c11 -> c9:c10:c11
HALF :: 0':s:nil:cons:double:1':bug_list_not -> c12:c13:c14
c12 :: c12:c13:c14
c13 :: c12:c13:c14
c14 :: c12:c13:c14 -> c12:c13:c14
LOG :: 0':s:nil:cons:double:1':bug_list_not -> c15:c16:c17
c15 :: c15:c16:c17
c16 :: c15:c16:c17
c17 :: c15:c16:c17 -> c12:c13:c14 -> c15:c16:c17
half :: 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 -> c18:c19
c18 :: c18:c19
c19 :: c18:c19
S2BIN :: 0':s:nil:cons:double:1':bug_list_not -> c20
c20 :: c21 -> c20
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 -> c21
c21 :: c22:c23 -> c4:c5:c6 -> c15:c16:c17 -> c21
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 -> c22:c23
lt :: 0':s:nil:cons:double:1':bug_list_not -> 0':s:nil:cons:double:1':bug_list_not -> true:false
log :: 0':s:nil:cons:double:1':bug_list_not -> 0':s:nil:cons:double:1':bug_list_not
true :: true:false
c22 :: c21 -> c18:c19 -> c22:c23
more :: 0':s:nil:cons:double:1':bug_list_not -> 0':s:nil:cons:double:1':bug_list_not
false :: true:false
c23 :: c24:c25 -> c22:c23
S2BIN2 :: 0':s:nil:cons:double:1':bug_list_not -> 0':s:nil:cons:double:1':bug_list_not -> c24:c25
c24 :: c24:c25
c25 :: c26:c27 -> c:c1:c2:c3 -> c7:c8 -> c24:c25
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 -> c26:c27
eq :: 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
c26 :: c26:c27
c27 :: c24:c25 -> c26:c27
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
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_c:c1:c2:c31_28 :: c:c1:c2:c3
hole_0':s:nil:cons:double:1':bug_list_not2_28 :: 0':s:nil:cons:double:1':bug_list_not
hole_c4:c5:c63_28 :: c4:c5:c6
hole_c7:c84_28 :: c7:c8
hole_c9:c10:c115_28 :: c9:c10:c11
hole_c12:c13:c146_28 :: c12:c13:c14
hole_c15:c16:c177_28 :: c15:c16:c17
hole_c18:c198_28 :: c18:c19
hole_c209_28 :: c20
hole_c2110_28 :: c21
hole_c22:c2311_28 :: c22:c23
hole_true:false12_28 :: true:false
hole_c24:c2513_28 :: c24:c25
hole_c26:c2714_28 :: c26:c27
gen_c:c1:c2:c315_28 :: Nat -> c:c1:c2:c3
gen_0':s:nil:cons:double:1':bug_list_not16_28 :: Nat -> 0':s:nil:cons:double:1':bug_list_not
gen_c4:c5:c617_28 :: Nat -> c4:c5:c6
gen_c9:c10:c1118_28 :: Nat -> c9:c10:c11
gen_c12:c13:c1419_28 :: Nat -> c12:c13:c14
gen_c15:c16:c1720_28 :: Nat -> c15:c16:c17


Lemmas:
EQ(gen_0':s:nil:cons:double:1':bug_list_not16_28(n22_28), gen_0':s:nil:cons:double:1':bug_list_not16_28(n22_28)) -> gen_c:c1:c2:c315_28(n22_28), rt in Omega(1 + n22_28)


Generator Equations:
gen_c:c1:c2:c315_28(0) <=> c
gen_c:c1:c2:c315_28(+(x, 1)) <=> c3(gen_c:c1:c2:c315_28(x))
gen_0':s:nil:cons:double:1':bug_list_not16_28(0) <=> 0'
gen_0':s:nil:cons:double:1':bug_list_not16_28(+(x, 1)) <=> s(gen_0':s:nil:cons:double:1':bug_list_not16_28(x))
gen_c4:c5:c617_28(0) <=> c4
gen_c4:c5:c617_28(+(x, 1)) <=> c6(gen_c4:c5:c617_28(x))
gen_c9:c10:c1118_28(0) <=> c9
gen_c9:c10:c1118_28(+(x, 1)) <=> c10(gen_c9:c10:c1118_28(x))
gen_c12:c13:c1419_28(0) <=> c12
gen_c12:c13:c1419_28(+(x, 1)) <=> c14(gen_c12:c13:c1419_28(x))
gen_c15:c16:c1720_28(0) <=> c15
gen_c15:c16:c1720_28(+(x, 1)) <=> c17(gen_c15:c16:c1720_28(x), c12)


The following defined symbols remain to be analysed:
LT, BIN2SS, HALF, LOG, half, S2BIN1, lt, log, S2BIN2, eq, bin2ss, s2bin1, s2bin2

They will be analysed ascendingly in the following order:
LT < S2BIN1
HALF < LOG
half < LOG
LOG < S2BIN1
half < log
lt < S2BIN1
log < S2BIN1
S2BIN2 < S2BIN1
lt < s2bin1
log < s2bin1
eq < S2BIN2
eq < s2bin2
s2bin2 < s2bin1

----------------------------------------

(17) RewriteLemmaProof (LOWER BOUND(ID))
Proved the following rewrite lemma:
LT(gen_0':s:nil:cons:double:1':bug_list_not16_28(n1267_28), gen_0':s:nil:cons:double:1':bug_list_not16_28(+(1, n1267_28))) -> gen_c4:c5:c617_28(n1267_28), rt in Omega(1 + n1267_28)

Induction Base:
LT(gen_0':s:nil:cons:double:1':bug_list_not16_28(0), gen_0':s:nil:cons:double:1':bug_list_not16_28(+(1, 0))) ->_R^Omega(1)
c4

Induction Step:
LT(gen_0':s:nil:cons:double:1':bug_list_not16_28(+(n1267_28, 1)), gen_0':s:nil:cons:double:1':bug_list_not16_28(+(1, +(n1267_28, 1)))) ->_R^Omega(1)
c6(LT(gen_0':s:nil:cons:double:1':bug_list_not16_28(n1267_28), gen_0':s:nil:cons:double:1':bug_list_not16_28(+(1, n1267_28)))) ->_IH
c6(gen_c4:c5:c617_28(c1268_28))

We have rt in Omega(n^1) and sz in O(n). Thus, we have irc_R in Omega(n).
----------------------------------------

(18)
Obligation:
Innermost TRS:
Rules:
EQ(0', 0') -> c
EQ(0', s(z0)) -> c1
EQ(s(z0), 0') -> c2
EQ(s(z0), s(z1)) -> c3(EQ(z0, z1))
LT(0', s(z0)) -> c4
LT(z0, 0') -> c5
LT(s(z0), s(z1)) -> c6(LT(z0, z1))
BIN2S(nil) -> c7
BIN2S(cons(z0, z1)) -> c8(BIN2SS(z0, z1))
BIN2SS(z0, nil) -> c9
BIN2SS(z0, cons(0', z1)) -> c10(BIN2SS(double(z0), z1))
BIN2SS(z0, cons(1', z1)) -> c11(BIN2SS(s(double(z0)), z1))
HALF(0') -> c12
HALF(s(0')) -> c13
HALF(s(s(z0))) -> c14(HALF(z0))
LOG(0') -> c15
LOG(s(0')) -> c16
LOG(s(s(z0))) -> c17(LOG(half(s(s(z0)))), HALF(s(s(z0))))
MORE(nil) -> c18
MORE(cons(z0, z1)) -> c19
S2BIN(z0) -> c20(S2BIN1(z0, 0', cons(nil, nil)))
S2BIN1(z0, z1, z2) -> c21(IF1(lt(z1, log(z0)), z0, z1, z2), LT(z1, log(z0)), LOG(z0))
IF1(true, z0, z1, z2) -> c22(S2BIN1(z0, s(z1), more(z2)), MORE(z2))
IF1(false, z0, z1, z2) -> c23(S2BIN2(z0, z2))
S2BIN2(z0, nil) -> c24
S2BIN2(z0, cons(z1, z2)) -> c25(IF2(eq(z0, bin2s(z1)), z0, z1, z2), EQ(z0, bin2s(z1)), BIN2S(z1))
IF2(true, z0, z1, z2) -> c26
IF2(false, z0, z1, z2) -> c27(S2BIN2(z0, z2))
eq(0', 0') -> true
eq(0', s(z0)) -> false
eq(s(z0), 0') -> false
eq(s(z0), s(z1)) -> eq(z0, z1)
lt(0', s(z0)) -> true
lt(z0, 0') -> false
lt(s(z0), s(z1)) -> lt(z0, z1)
bin2s(nil) -> 0'
bin2s(cons(z0, z1)) -> bin2ss(z0, z1)
bin2ss(z0, nil) -> z0
bin2ss(z0, cons(0', z1)) -> bin2ss(double(z0), z1)
bin2ss(z0, cons(1', z1)) -> bin2ss(s(double(z0)), z1)
half(0') -> 0'
half(s(0')) -> 0'
half(s(s(z0))) -> s(half(z0))
log(0') -> 0'
log(s(0')) -> 0'
log(s(s(z0))) -> s(log(half(s(s(z0)))))
more(nil) -> nil
more(cons(z0, z1)) -> cons(cons(0', z0), cons(cons(1', z0), cons(z0, z1)))
s2bin(z0) -> s2bin1(z0, 0', cons(nil, nil))
s2bin1(z0, z1, z2) -> if1(lt(z1, log(z0)), z0, z1, z2)
if1(true, z0, z1, z2) -> s2bin1(z0, s(z1), more(z2))
if1(false, z0, z1, z2) -> s2bin2(z0, z2)
s2bin2(z0, nil) -> bug_list_not
s2bin2(z0, cons(z1, z2)) -> if2(eq(z0, bin2s(z1)), z0, z1, z2)
if2(true, z0, z1, z2) -> z1
if2(false, z0, z1, z2) -> s2bin2(z0, z2)

Types:
EQ :: 0':s:nil:cons:double:1':bug_list_not -> 0':s:nil:cons:double:1':bug_list_not -> c:c1:c2:c3
0' :: 0':s:nil:cons:double:1':bug_list_not
c :: c:c1:c2:c3
s :: 0':s:nil:cons:double:1':bug_list_not -> 0':s:nil:cons:double:1':bug_list_not
c1 :: c:c1:c2:c3
c2 :: c:c1:c2:c3
c3 :: c:c1:c2:c3 -> c:c1:c2:c3
LT :: 0':s:nil:cons:double:1':bug_list_not -> 0':s:nil:cons:double:1':bug_list_not -> c4:c5:c6
c4 :: c4:c5:c6
c5 :: c4:c5:c6
c6 :: c4:c5:c6 -> c4:c5:c6
BIN2S :: 0':s:nil:cons:double:1':bug_list_not -> c7:c8
nil :: 0':s:nil:cons:double:1':bug_list_not
c7 :: c7:c8
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
c8 :: c9:c10:c11 -> c7:c8
BIN2SS :: 0':s:nil:cons:double:1':bug_list_not -> 0':s:nil:cons:double:1':bug_list_not -> c9:c10:c11
c9 :: c9:c10:c11
c10 :: c9:c10:c11 -> c9:c10:c11
double :: 0':s:nil:cons:double:1':bug_list_not -> 0':s:nil:cons:double:1':bug_list_not
1' :: 0':s:nil:cons:double:1':bug_list_not
c11 :: c9:c10:c11 -> c9:c10:c11
HALF :: 0':s:nil:cons:double:1':bug_list_not -> c12:c13:c14
c12 :: c12:c13:c14
c13 :: c12:c13:c14
c14 :: c12:c13:c14 -> c12:c13:c14
LOG :: 0':s:nil:cons:double:1':bug_list_not -> c15:c16:c17
c15 :: c15:c16:c17
c16 :: c15:c16:c17
c17 :: c15:c16:c17 -> c12:c13:c14 -> c15:c16:c17
half :: 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 -> c18:c19
c18 :: c18:c19
c19 :: c18:c19
S2BIN :: 0':s:nil:cons:double:1':bug_list_not -> c20
c20 :: c21 -> c20
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 -> c21
c21 :: c22:c23 -> c4:c5:c6 -> c15:c16:c17 -> c21
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 -> c22:c23
lt :: 0':s:nil:cons:double:1':bug_list_not -> 0':s:nil:cons:double:1':bug_list_not -> true:false
log :: 0':s:nil:cons:double:1':bug_list_not -> 0':s:nil:cons:double:1':bug_list_not
true :: true:false
c22 :: c21 -> c18:c19 -> c22:c23
more :: 0':s:nil:cons:double:1':bug_list_not -> 0':s:nil:cons:double:1':bug_list_not
false :: true:false
c23 :: c24:c25 -> c22:c23
S2BIN2 :: 0':s:nil:cons:double:1':bug_list_not -> 0':s:nil:cons:double:1':bug_list_not -> c24:c25
c24 :: c24:c25
c25 :: c26:c27 -> c:c1:c2:c3 -> c7:c8 -> c24:c25
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 -> c26:c27
eq :: 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
c26 :: c26:c27
c27 :: c24:c25 -> c26:c27
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
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_c:c1:c2:c31_28 :: c:c1:c2:c3
hole_0':s:nil:cons:double:1':bug_list_not2_28 :: 0':s:nil:cons:double:1':bug_list_not
hole_c4:c5:c63_28 :: c4:c5:c6
hole_c7:c84_28 :: c7:c8
hole_c9:c10:c115_28 :: c9:c10:c11
hole_c12:c13:c146_28 :: c12:c13:c14
hole_c15:c16:c177_28 :: c15:c16:c17
hole_c18:c198_28 :: c18:c19
hole_c209_28 :: c20
hole_c2110_28 :: c21
hole_c22:c2311_28 :: c22:c23
hole_true:false12_28 :: true:false
hole_c24:c2513_28 :: c24:c25
hole_c26:c2714_28 :: c26:c27
gen_c:c1:c2:c315_28 :: Nat -> c:c1:c2:c3
gen_0':s:nil:cons:double:1':bug_list_not16_28 :: Nat -> 0':s:nil:cons:double:1':bug_list_not
gen_c4:c5:c617_28 :: Nat -> c4:c5:c6
gen_c9:c10:c1118_28 :: Nat -> c9:c10:c11
gen_c12:c13:c1419_28 :: Nat -> c12:c13:c14
gen_c15:c16:c1720_28 :: Nat -> c15:c16:c17


Lemmas:
EQ(gen_0':s:nil:cons:double:1':bug_list_not16_28(n22_28), gen_0':s:nil:cons:double:1':bug_list_not16_28(n22_28)) -> gen_c:c1:c2:c315_28(n22_28), rt in Omega(1 + n22_28)
LT(gen_0':s:nil:cons:double:1':bug_list_not16_28(n1267_28), gen_0':s:nil:cons:double:1':bug_list_not16_28(+(1, n1267_28))) -> gen_c4:c5:c617_28(n1267_28), rt in Omega(1 + n1267_28)


Generator Equations:
gen_c:c1:c2:c315_28(0) <=> c
gen_c:c1:c2:c315_28(+(x, 1)) <=> c3(gen_c:c1:c2:c315_28(x))
gen_0':s:nil:cons:double:1':bug_list_not16_28(0) <=> 0'
gen_0':s:nil:cons:double:1':bug_list_not16_28(+(x, 1)) <=> s(gen_0':s:nil:cons:double:1':bug_list_not16_28(x))
gen_c4:c5:c617_28(0) <=> c4
gen_c4:c5:c617_28(+(x, 1)) <=> c6(gen_c4:c5:c617_28(x))
gen_c9:c10:c1118_28(0) <=> c9
gen_c9:c10:c1118_28(+(x, 1)) <=> c10(gen_c9:c10:c1118_28(x))
gen_c12:c13:c1419_28(0) <=> c12
gen_c12:c13:c1419_28(+(x, 1)) <=> c14(gen_c12:c13:c1419_28(x))
gen_c15:c16:c1720_28(0) <=> c15
gen_c15:c16:c1720_28(+(x, 1)) <=> c17(gen_c15:c16:c1720_28(x), c12)


The following defined symbols remain to be analysed:
BIN2SS, HALF, LOG, half, S2BIN1, lt, log, S2BIN2, eq, bin2ss, s2bin1, s2bin2

They will be analysed ascendingly in the following order:
HALF < LOG
half < LOG
LOG < S2BIN1
half < log
lt < S2BIN1
log < S2BIN1
S2BIN2 < S2BIN1
lt < s2bin1
log < s2bin1
eq < S2BIN2
eq < s2bin2
s2bin2 < s2bin1

----------------------------------------

(19) RewriteLemmaProof (LOWER BOUND(ID))
Proved the following rewrite lemma:
HALF(gen_0':s:nil:cons:double:1':bug_list_not16_28(*(2, n2297_28))) -> gen_c12:c13:c1419_28(n2297_28), rt in Omega(1 + n2297_28)

Induction Base:
HALF(gen_0':s:nil:cons:double:1':bug_list_not16_28(*(2, 0))) ->_R^Omega(1)
c12

Induction Step:
HALF(gen_0':s:nil:cons:double:1':bug_list_not16_28(*(2, +(n2297_28, 1)))) ->_R^Omega(1)
c14(HALF(gen_0':s:nil:cons:double:1':bug_list_not16_28(*(2, n2297_28)))) ->_IH
c14(gen_c12:c13:c1419_28(c2298_28))

We have rt in Omega(n^1) and sz in O(n). Thus, we have irc_R in Omega(n).
----------------------------------------

(20)
Obligation:
Innermost TRS:
Rules:
EQ(0', 0') -> c
EQ(0', s(z0)) -> c1
EQ(s(z0), 0') -> c2
EQ(s(z0), s(z1)) -> c3(EQ(z0, z1))
LT(0', s(z0)) -> c4
LT(z0, 0') -> c5
LT(s(z0), s(z1)) -> c6(LT(z0, z1))
BIN2S(nil) -> c7
BIN2S(cons(z0, z1)) -> c8(BIN2SS(z0, z1))
BIN2SS(z0, nil) -> c9
BIN2SS(z0, cons(0', z1)) -> c10(BIN2SS(double(z0), z1))
BIN2SS(z0, cons(1', z1)) -> c11(BIN2SS(s(double(z0)), z1))
HALF(0') -> c12
HALF(s(0')) -> c13
HALF(s(s(z0))) -> c14(HALF(z0))
LOG(0') -> c15
LOG(s(0')) -> c16
LOG(s(s(z0))) -> c17(LOG(half(s(s(z0)))), HALF(s(s(z0))))
MORE(nil) -> c18
MORE(cons(z0, z1)) -> c19
S2BIN(z0) -> c20(S2BIN1(z0, 0', cons(nil, nil)))
S2BIN1(z0, z1, z2) -> c21(IF1(lt(z1, log(z0)), z0, z1, z2), LT(z1, log(z0)), LOG(z0))
IF1(true, z0, z1, z2) -> c22(S2BIN1(z0, s(z1), more(z2)), MORE(z2))
IF1(false, z0, z1, z2) -> c23(S2BIN2(z0, z2))
S2BIN2(z0, nil) -> c24
S2BIN2(z0, cons(z1, z2)) -> c25(IF2(eq(z0, bin2s(z1)), z0, z1, z2), EQ(z0, bin2s(z1)), BIN2S(z1))
IF2(true, z0, z1, z2) -> c26
IF2(false, z0, z1, z2) -> c27(S2BIN2(z0, z2))
eq(0', 0') -> true
eq(0', s(z0)) -> false
eq(s(z0), 0') -> false
eq(s(z0), s(z1)) -> eq(z0, z1)
lt(0', s(z0)) -> true
lt(z0, 0') -> false
lt(s(z0), s(z1)) -> lt(z0, z1)
bin2s(nil) -> 0'
bin2s(cons(z0, z1)) -> bin2ss(z0, z1)
bin2ss(z0, nil) -> z0
bin2ss(z0, cons(0', z1)) -> bin2ss(double(z0), z1)
bin2ss(z0, cons(1', z1)) -> bin2ss(s(double(z0)), z1)
half(0') -> 0'
half(s(0')) -> 0'
half(s(s(z0))) -> s(half(z0))
log(0') -> 0'
log(s(0')) -> 0'
log(s(s(z0))) -> s(log(half(s(s(z0)))))
more(nil) -> nil
more(cons(z0, z1)) -> cons(cons(0', z0), cons(cons(1', z0), cons(z0, z1)))
s2bin(z0) -> s2bin1(z0, 0', cons(nil, nil))
s2bin1(z0, z1, z2) -> if1(lt(z1, log(z0)), z0, z1, z2)
if1(true, z0, z1, z2) -> s2bin1(z0, s(z1), more(z2))
if1(false, z0, z1, z2) -> s2bin2(z0, z2)
s2bin2(z0, nil) -> bug_list_not
s2bin2(z0, cons(z1, z2)) -> if2(eq(z0, bin2s(z1)), z0, z1, z2)
if2(true, z0, z1, z2) -> z1
if2(false, z0, z1, z2) -> s2bin2(z0, z2)

Types:
EQ :: 0':s:nil:cons:double:1':bug_list_not -> 0':s:nil:cons:double:1':bug_list_not -> c:c1:c2:c3
0' :: 0':s:nil:cons:double:1':bug_list_not
c :: c:c1:c2:c3
s :: 0':s:nil:cons:double:1':bug_list_not -> 0':s:nil:cons:double:1':bug_list_not
c1 :: c:c1:c2:c3
c2 :: c:c1:c2:c3
c3 :: c:c1:c2:c3 -> c:c1:c2:c3
LT :: 0':s:nil:cons:double:1':bug_list_not -> 0':s:nil:cons:double:1':bug_list_not -> c4:c5:c6
c4 :: c4:c5:c6
c5 :: c4:c5:c6
c6 :: c4:c5:c6 -> c4:c5:c6
BIN2S :: 0':s:nil:cons:double:1':bug_list_not -> c7:c8
nil :: 0':s:nil:cons:double:1':bug_list_not
c7 :: c7:c8
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
c8 :: c9:c10:c11 -> c7:c8
BIN2SS :: 0':s:nil:cons:double:1':bug_list_not -> 0':s:nil:cons:double:1':bug_list_not -> c9:c10:c11
c9 :: c9:c10:c11
c10 :: c9:c10:c11 -> c9:c10:c11
double :: 0':s:nil:cons:double:1':bug_list_not -> 0':s:nil:cons:double:1':bug_list_not
1' :: 0':s:nil:cons:double:1':bug_list_not
c11 :: c9:c10:c11 -> c9:c10:c11
HALF :: 0':s:nil:cons:double:1':bug_list_not -> c12:c13:c14
c12 :: c12:c13:c14
c13 :: c12:c13:c14
c14 :: c12:c13:c14 -> c12:c13:c14
LOG :: 0':s:nil:cons:double:1':bug_list_not -> c15:c16:c17
c15 :: c15:c16:c17
c16 :: c15:c16:c17
c17 :: c15:c16:c17 -> c12:c13:c14 -> c15:c16:c17
half :: 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 -> c18:c19
c18 :: c18:c19
c19 :: c18:c19
S2BIN :: 0':s:nil:cons:double:1':bug_list_not -> c20
c20 :: c21 -> c20
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 -> c21
c21 :: c22:c23 -> c4:c5:c6 -> c15:c16:c17 -> c21
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 -> c22:c23
lt :: 0':s:nil:cons:double:1':bug_list_not -> 0':s:nil:cons:double:1':bug_list_not -> true:false
log :: 0':s:nil:cons:double:1':bug_list_not -> 0':s:nil:cons:double:1':bug_list_not
true :: true:false
c22 :: c21 -> c18:c19 -> c22:c23
more :: 0':s:nil:cons:double:1':bug_list_not -> 0':s:nil:cons:double:1':bug_list_not
false :: true:false
c23 :: c24:c25 -> c22:c23
S2BIN2 :: 0':s:nil:cons:double:1':bug_list_not -> 0':s:nil:cons:double:1':bug_list_not -> c24:c25
c24 :: c24:c25
c25 :: c26:c27 -> c:c1:c2:c3 -> c7:c8 -> c24:c25
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 -> c26:c27
eq :: 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
c26 :: c26:c27
c27 :: c24:c25 -> c26:c27
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
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_c:c1:c2:c31_28 :: c:c1:c2:c3
hole_0':s:nil:cons:double:1':bug_list_not2_28 :: 0':s:nil:cons:double:1':bug_list_not
hole_c4:c5:c63_28 :: c4:c5:c6
hole_c7:c84_28 :: c7:c8
hole_c9:c10:c115_28 :: c9:c10:c11
hole_c12:c13:c146_28 :: c12:c13:c14
hole_c15:c16:c177_28 :: c15:c16:c17
hole_c18:c198_28 :: c18:c19
hole_c209_28 :: c20
hole_c2110_28 :: c21
hole_c22:c2311_28 :: c22:c23
hole_true:false12_28 :: true:false
hole_c24:c2513_28 :: c24:c25
hole_c26:c2714_28 :: c26:c27
gen_c:c1:c2:c315_28 :: Nat -> c:c1:c2:c3
gen_0':s:nil:cons:double:1':bug_list_not16_28 :: Nat -> 0':s:nil:cons:double:1':bug_list_not
gen_c4:c5:c617_28 :: Nat -> c4:c5:c6
gen_c9:c10:c1118_28 :: Nat -> c9:c10:c11
gen_c12:c13:c1419_28 :: Nat -> c12:c13:c14
gen_c15:c16:c1720_28 :: Nat -> c15:c16:c17


Lemmas:
EQ(gen_0':s:nil:cons:double:1':bug_list_not16_28(n22_28), gen_0':s:nil:cons:double:1':bug_list_not16_28(n22_28)) -> gen_c:c1:c2:c315_28(n22_28), rt in Omega(1 + n22_28)
LT(gen_0':s:nil:cons:double:1':bug_list_not16_28(n1267_28), gen_0':s:nil:cons:double:1':bug_list_not16_28(+(1, n1267_28))) -> gen_c4:c5:c617_28(n1267_28), rt in Omega(1 + n1267_28)
HALF(gen_0':s:nil:cons:double:1':bug_list_not16_28(*(2, n2297_28))) -> gen_c12:c13:c1419_28(n2297_28), rt in Omega(1 + n2297_28)


Generator Equations:
gen_c:c1:c2:c315_28(0) <=> c
gen_c:c1:c2:c315_28(+(x, 1)) <=> c3(gen_c:c1:c2:c315_28(x))
gen_0':s:nil:cons:double:1':bug_list_not16_28(0) <=> 0'
gen_0':s:nil:cons:double:1':bug_list_not16_28(+(x, 1)) <=> s(gen_0':s:nil:cons:double:1':bug_list_not16_28(x))
gen_c4:c5:c617_28(0) <=> c4
gen_c4:c5:c617_28(+(x, 1)) <=> c6(gen_c4:c5:c617_28(x))
gen_c9:c10:c1118_28(0) <=> c9
gen_c9:c10:c1118_28(+(x, 1)) <=> c10(gen_c9:c10:c1118_28(x))
gen_c12:c13:c1419_28(0) <=> c12
gen_c12:c13:c1419_28(+(x, 1)) <=> c14(gen_c12:c13:c1419_28(x))
gen_c15:c16:c1720_28(0) <=> c15
gen_c15:c16:c1720_28(+(x, 1)) <=> c17(gen_c15:c16:c1720_28(x), c12)


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

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

----------------------------------------

(21) RewriteLemmaProof (LOWER BOUND(ID))
Proved the following rewrite lemma:
half(gen_0':s:nil:cons:double:1':bug_list_not16_28(*(2, n3068_28))) -> gen_0':s:nil:cons:double:1':bug_list_not16_28(n3068_28), rt in Omega(0)

Induction Base:
half(gen_0':s:nil:cons:double:1':bug_list_not16_28(*(2, 0))) ->_R^Omega(0)
0'

Induction Step:
half(gen_0':s:nil:cons:double:1':bug_list_not16_28(*(2, +(n3068_28, 1)))) ->_R^Omega(0)
s(half(gen_0':s:nil:cons:double:1':bug_list_not16_28(*(2, n3068_28)))) ->_IH
s(gen_0':s:nil:cons:double:1':bug_list_not16_28(c3069_28))

We have rt in Omega(1) and sz in O(n). Thus, we have irc_R in Omega(n^0).
----------------------------------------

(22)
Obligation:
Innermost TRS:
Rules:
EQ(0', 0') -> c
EQ(0', s(z0)) -> c1
EQ(s(z0), 0') -> c2
EQ(s(z0), s(z1)) -> c3(EQ(z0, z1))
LT(0', s(z0)) -> c4
LT(z0, 0') -> c5
LT(s(z0), s(z1)) -> c6(LT(z0, z1))
BIN2S(nil) -> c7
BIN2S(cons(z0, z1)) -> c8(BIN2SS(z0, z1))
BIN2SS(z0, nil) -> c9
BIN2SS(z0, cons(0', z1)) -> c10(BIN2SS(double(z0), z1))
BIN2SS(z0, cons(1', z1)) -> c11(BIN2SS(s(double(z0)), z1))
HALF(0') -> c12
HALF(s(0')) -> c13
HALF(s(s(z0))) -> c14(HALF(z0))
LOG(0') -> c15
LOG(s(0')) -> c16
LOG(s(s(z0))) -> c17(LOG(half(s(s(z0)))), HALF(s(s(z0))))
MORE(nil) -> c18
MORE(cons(z0, z1)) -> c19
S2BIN(z0) -> c20(S2BIN1(z0, 0', cons(nil, nil)))
S2BIN1(z0, z1, z2) -> c21(IF1(lt(z1, log(z0)), z0, z1, z2), LT(z1, log(z0)), LOG(z0))
IF1(true, z0, z1, z2) -> c22(S2BIN1(z0, s(z1), more(z2)), MORE(z2))
IF1(false, z0, z1, z2) -> c23(S2BIN2(z0, z2))
S2BIN2(z0, nil) -> c24
S2BIN2(z0, cons(z1, z2)) -> c25(IF2(eq(z0, bin2s(z1)), z0, z1, z2), EQ(z0, bin2s(z1)), BIN2S(z1))
IF2(true, z0, z1, z2) -> c26
IF2(false, z0, z1, z2) -> c27(S2BIN2(z0, z2))
eq(0', 0') -> true
eq(0', s(z0)) -> false
eq(s(z0), 0') -> false
eq(s(z0), s(z1)) -> eq(z0, z1)
lt(0', s(z0)) -> true
lt(z0, 0') -> false
lt(s(z0), s(z1)) -> lt(z0, z1)
bin2s(nil) -> 0'
bin2s(cons(z0, z1)) -> bin2ss(z0, z1)
bin2ss(z0, nil) -> z0
bin2ss(z0, cons(0', z1)) -> bin2ss(double(z0), z1)
bin2ss(z0, cons(1', z1)) -> bin2ss(s(double(z0)), z1)
half(0') -> 0'
half(s(0')) -> 0'
half(s(s(z0))) -> s(half(z0))
log(0') -> 0'
log(s(0')) -> 0'
log(s(s(z0))) -> s(log(half(s(s(z0)))))
more(nil) -> nil
more(cons(z0, z1)) -> cons(cons(0', z0), cons(cons(1', z0), cons(z0, z1)))
s2bin(z0) -> s2bin1(z0, 0', cons(nil, nil))
s2bin1(z0, z1, z2) -> if1(lt(z1, log(z0)), z0, z1, z2)
if1(true, z0, z1, z2) -> s2bin1(z0, s(z1), more(z2))
if1(false, z0, z1, z2) -> s2bin2(z0, z2)
s2bin2(z0, nil) -> bug_list_not
s2bin2(z0, cons(z1, z2)) -> if2(eq(z0, bin2s(z1)), z0, z1, z2)
if2(true, z0, z1, z2) -> z1
if2(false, z0, z1, z2) -> s2bin2(z0, z2)

Types:
EQ :: 0':s:nil:cons:double:1':bug_list_not -> 0':s:nil:cons:double:1':bug_list_not -> c:c1:c2:c3
0' :: 0':s:nil:cons:double:1':bug_list_not
c :: c:c1:c2:c3
s :: 0':s:nil:cons:double:1':bug_list_not -> 0':s:nil:cons:double:1':bug_list_not
c1 :: c:c1:c2:c3
c2 :: c:c1:c2:c3
c3 :: c:c1:c2:c3 -> c:c1:c2:c3
LT :: 0':s:nil:cons:double:1':bug_list_not -> 0':s:nil:cons:double:1':bug_list_not -> c4:c5:c6
c4 :: c4:c5:c6
c5 :: c4:c5:c6
c6 :: c4:c5:c6 -> c4:c5:c6
BIN2S :: 0':s:nil:cons:double:1':bug_list_not -> c7:c8
nil :: 0':s:nil:cons:double:1':bug_list_not
c7 :: c7:c8
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
c8 :: c9:c10:c11 -> c7:c8
BIN2SS :: 0':s:nil:cons:double:1':bug_list_not -> 0':s:nil:cons:double:1':bug_list_not -> c9:c10:c11
c9 :: c9:c10:c11
c10 :: c9:c10:c11 -> c9:c10:c11
double :: 0':s:nil:cons:double:1':bug_list_not -> 0':s:nil:cons:double:1':bug_list_not
1' :: 0':s:nil:cons:double:1':bug_list_not
c11 :: c9:c10:c11 -> c9:c10:c11
HALF :: 0':s:nil:cons:double:1':bug_list_not -> c12:c13:c14
c12 :: c12:c13:c14
c13 :: c12:c13:c14
c14 :: c12:c13:c14 -> c12:c13:c14
LOG :: 0':s:nil:cons:double:1':bug_list_not -> c15:c16:c17
c15 :: c15:c16:c17
c16 :: c15:c16:c17
c17 :: c15:c16:c17 -> c12:c13:c14 -> c15:c16:c17
half :: 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 -> c18:c19
c18 :: c18:c19
c19 :: c18:c19
S2BIN :: 0':s:nil:cons:double:1':bug_list_not -> c20
c20 :: c21 -> c20
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 -> c21
c21 :: c22:c23 -> c4:c5:c6 -> c15:c16:c17 -> c21
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 -> c22:c23
lt :: 0':s:nil:cons:double:1':bug_list_not -> 0':s:nil:cons:double:1':bug_list_not -> true:false
log :: 0':s:nil:cons:double:1':bug_list_not -> 0':s:nil:cons:double:1':bug_list_not
true :: true:false
c22 :: c21 -> c18:c19 -> c22:c23
more :: 0':s:nil:cons:double:1':bug_list_not -> 0':s:nil:cons:double:1':bug_list_not
false :: true:false
c23 :: c24:c25 -> c22:c23
S2BIN2 :: 0':s:nil:cons:double:1':bug_list_not -> 0':s:nil:cons:double:1':bug_list_not -> c24:c25
c24 :: c24:c25
c25 :: c26:c27 -> c:c1:c2:c3 -> c7:c8 -> c24:c25
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 -> c26:c27
eq :: 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
c26 :: c26:c27
c27 :: c24:c25 -> c26:c27
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
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_c:c1:c2:c31_28 :: c:c1:c2:c3
hole_0':s:nil:cons:double:1':bug_list_not2_28 :: 0':s:nil:cons:double:1':bug_list_not
hole_c4:c5:c63_28 :: c4:c5:c6
hole_c7:c84_28 :: c7:c8
hole_c9:c10:c115_28 :: c9:c10:c11
hole_c12:c13:c146_28 :: c12:c13:c14
hole_c15:c16:c177_28 :: c15:c16:c17
hole_c18:c198_28 :: c18:c19
hole_c209_28 :: c20
hole_c2110_28 :: c21
hole_c22:c2311_28 :: c22:c23
hole_true:false12_28 :: true:false
hole_c24:c2513_28 :: c24:c25
hole_c26:c2714_28 :: c26:c27
gen_c:c1:c2:c315_28 :: Nat -> c:c1:c2:c3
gen_0':s:nil:cons:double:1':bug_list_not16_28 :: Nat -> 0':s:nil:cons:double:1':bug_list_not
gen_c4:c5:c617_28 :: Nat -> c4:c5:c6
gen_c9:c10:c1118_28 :: Nat -> c9:c10:c11
gen_c12:c13:c1419_28 :: Nat -> c12:c13:c14
gen_c15:c16:c1720_28 :: Nat -> c15:c16:c17


Lemmas:
EQ(gen_0':s:nil:cons:double:1':bug_list_not16_28(n22_28), gen_0':s:nil:cons:double:1':bug_list_not16_28(n22_28)) -> gen_c:c1:c2:c315_28(n22_28), rt in Omega(1 + n22_28)
LT(gen_0':s:nil:cons:double:1':bug_list_not16_28(n1267_28), gen_0':s:nil:cons:double:1':bug_list_not16_28(+(1, n1267_28))) -> gen_c4:c5:c617_28(n1267_28), rt in Omega(1 + n1267_28)
HALF(gen_0':s:nil:cons:double:1':bug_list_not16_28(*(2, n2297_28))) -> gen_c12:c13:c1419_28(n2297_28), rt in Omega(1 + n2297_28)
half(gen_0':s:nil:cons:double:1':bug_list_not16_28(*(2, n3068_28))) -> gen_0':s:nil:cons:double:1':bug_list_not16_28(n3068_28), rt in Omega(0)


Generator Equations:
gen_c:c1:c2:c315_28(0) <=> c
gen_c:c1:c2:c315_28(+(x, 1)) <=> c3(gen_c:c1:c2:c315_28(x))
gen_0':s:nil:cons:double:1':bug_list_not16_28(0) <=> 0'
gen_0':s:nil:cons:double:1':bug_list_not16_28(+(x, 1)) <=> s(gen_0':s:nil:cons:double:1':bug_list_not16_28(x))
gen_c4:c5:c617_28(0) <=> c4
gen_c4:c5:c617_28(+(x, 1)) <=> c6(gen_c4:c5:c617_28(x))
gen_c9:c10:c1118_28(0) <=> c9
gen_c9:c10:c1118_28(+(x, 1)) <=> c10(gen_c9:c10:c1118_28(x))
gen_c12:c13:c1419_28(0) <=> c12
gen_c12:c13:c1419_28(+(x, 1)) <=> c14(gen_c12:c13:c1419_28(x))
gen_c15:c16:c1720_28(0) <=> c15
gen_c15:c16:c1720_28(+(x, 1)) <=> c17(gen_c15:c16:c1720_28(x), c12)


The following defined symbols remain to be analysed:
LOG, S2BIN1, lt, log, S2BIN2, eq, bin2ss, s2bin1, s2bin2

They will be analysed ascendingly in the following order:
LOG < S2BIN1
lt < S2BIN1
log < S2BIN1
S2BIN2 < S2BIN1
lt < s2bin1
log < s2bin1
eq < S2BIN2
eq < s2bin2
s2bin2 < s2bin1

----------------------------------------

(23) RewriteLemmaProof (LOWER BOUND(ID))
Proved the following rewrite lemma:
lt(gen_0':s:nil:cons:double:1':bug_list_not16_28(n4023_28), gen_0':s:nil:cons:double:1':bug_list_not16_28(+(1, n4023_28))) -> true, rt in Omega(0)

Induction Base:
lt(gen_0':s:nil:cons:double:1':bug_list_not16_28(0), gen_0':s:nil:cons:double:1':bug_list_not16_28(+(1, 0))) ->_R^Omega(0)
true

Induction Step:
lt(gen_0':s:nil:cons:double:1':bug_list_not16_28(+(n4023_28, 1)), gen_0':s:nil:cons:double:1':bug_list_not16_28(+(1, +(n4023_28, 1)))) ->_R^Omega(0)
lt(gen_0':s:nil:cons:double:1':bug_list_not16_28(n4023_28), gen_0':s:nil:cons:double:1':bug_list_not16_28(+(1, n4023_28))) ->_IH
true

We have rt in Omega(1) and sz in O(n). Thus, we have irc_R in Omega(n^0).
----------------------------------------

(24)
Obligation:
Innermost TRS:
Rules:
EQ(0', 0') -> c
EQ(0', s(z0)) -> c1
EQ(s(z0), 0') -> c2
EQ(s(z0), s(z1)) -> c3(EQ(z0, z1))
LT(0', s(z0)) -> c4
LT(z0, 0') -> c5
LT(s(z0), s(z1)) -> c6(LT(z0, z1))
BIN2S(nil) -> c7
BIN2S(cons(z0, z1)) -> c8(BIN2SS(z0, z1))
BIN2SS(z0, nil) -> c9
BIN2SS(z0, cons(0', z1)) -> c10(BIN2SS(double(z0), z1))
BIN2SS(z0, cons(1', z1)) -> c11(BIN2SS(s(double(z0)), z1))
HALF(0') -> c12
HALF(s(0')) -> c13
HALF(s(s(z0))) -> c14(HALF(z0))
LOG(0') -> c15
LOG(s(0')) -> c16
LOG(s(s(z0))) -> c17(LOG(half(s(s(z0)))), HALF(s(s(z0))))
MORE(nil) -> c18
MORE(cons(z0, z1)) -> c19
S2BIN(z0) -> c20(S2BIN1(z0, 0', cons(nil, nil)))
S2BIN1(z0, z1, z2) -> c21(IF1(lt(z1, log(z0)), z0, z1, z2), LT(z1, log(z0)), LOG(z0))
IF1(true, z0, z1, z2) -> c22(S2BIN1(z0, s(z1), more(z2)), MORE(z2))
IF1(false, z0, z1, z2) -> c23(S2BIN2(z0, z2))
S2BIN2(z0, nil) -> c24
S2BIN2(z0, cons(z1, z2)) -> c25(IF2(eq(z0, bin2s(z1)), z0, z1, z2), EQ(z0, bin2s(z1)), BIN2S(z1))
IF2(true, z0, z1, z2) -> c26
IF2(false, z0, z1, z2) -> c27(S2BIN2(z0, z2))
eq(0', 0') -> true
eq(0', s(z0)) -> false
eq(s(z0), 0') -> false
eq(s(z0), s(z1)) -> eq(z0, z1)
lt(0', s(z0)) -> true
lt(z0, 0') -> false
lt(s(z0), s(z1)) -> lt(z0, z1)
bin2s(nil) -> 0'
bin2s(cons(z0, z1)) -> bin2ss(z0, z1)
bin2ss(z0, nil) -> z0
bin2ss(z0, cons(0', z1)) -> bin2ss(double(z0), z1)
bin2ss(z0, cons(1', z1)) -> bin2ss(s(double(z0)), z1)
half(0') -> 0'
half(s(0')) -> 0'
half(s(s(z0))) -> s(half(z0))
log(0') -> 0'
log(s(0')) -> 0'
log(s(s(z0))) -> s(log(half(s(s(z0)))))
more(nil) -> nil
more(cons(z0, z1)) -> cons(cons(0', z0), cons(cons(1', z0), cons(z0, z1)))
s2bin(z0) -> s2bin1(z0, 0', cons(nil, nil))
s2bin1(z0, z1, z2) -> if1(lt(z1, log(z0)), z0, z1, z2)
if1(true, z0, z1, z2) -> s2bin1(z0, s(z1), more(z2))
if1(false, z0, z1, z2) -> s2bin2(z0, z2)
s2bin2(z0, nil) -> bug_list_not
s2bin2(z0, cons(z1, z2)) -> if2(eq(z0, bin2s(z1)), z0, z1, z2)
if2(true, z0, z1, z2) -> z1
if2(false, z0, z1, z2) -> s2bin2(z0, z2)

Types:
EQ :: 0':s:nil:cons:double:1':bug_list_not -> 0':s:nil:cons:double:1':bug_list_not -> c:c1:c2:c3
0' :: 0':s:nil:cons:double:1':bug_list_not
c :: c:c1:c2:c3
s :: 0':s:nil:cons:double:1':bug_list_not -> 0':s:nil:cons:double:1':bug_list_not
c1 :: c:c1:c2:c3
c2 :: c:c1:c2:c3
c3 :: c:c1:c2:c3 -> c:c1:c2:c3
LT :: 0':s:nil:cons:double:1':bug_list_not -> 0':s:nil:cons:double:1':bug_list_not -> c4:c5:c6
c4 :: c4:c5:c6
c5 :: c4:c5:c6
c6 :: c4:c5:c6 -> c4:c5:c6
BIN2S :: 0':s:nil:cons:double:1':bug_list_not -> c7:c8
nil :: 0':s:nil:cons:double:1':bug_list_not
c7 :: c7:c8
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
c8 :: c9:c10:c11 -> c7:c8
BIN2SS :: 0':s:nil:cons:double:1':bug_list_not -> 0':s:nil:cons:double:1':bug_list_not -> c9:c10:c11
c9 :: c9:c10:c11
c10 :: c9:c10:c11 -> c9:c10:c11
double :: 0':s:nil:cons:double:1':bug_list_not -> 0':s:nil:cons:double:1':bug_list_not
1' :: 0':s:nil:cons:double:1':bug_list_not
c11 :: c9:c10:c11 -> c9:c10:c11
HALF :: 0':s:nil:cons:double:1':bug_list_not -> c12:c13:c14
c12 :: c12:c13:c14
c13 :: c12:c13:c14
c14 :: c12:c13:c14 -> c12:c13:c14
LOG :: 0':s:nil:cons:double:1':bug_list_not -> c15:c16:c17
c15 :: c15:c16:c17
c16 :: c15:c16:c17
c17 :: c15:c16:c17 -> c12:c13:c14 -> c15:c16:c17
half :: 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 -> c18:c19
c18 :: c18:c19
c19 :: c18:c19
S2BIN :: 0':s:nil:cons:double:1':bug_list_not -> c20
c20 :: c21 -> c20
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 -> c21
c21 :: c22:c23 -> c4:c5:c6 -> c15:c16:c17 -> c21
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 -> c22:c23
lt :: 0':s:nil:cons:double:1':bug_list_not -> 0':s:nil:cons:double:1':bug_list_not -> true:false
log :: 0':s:nil:cons:double:1':bug_list_not -> 0':s:nil:cons:double:1':bug_list_not
true :: true:false
c22 :: c21 -> c18:c19 -> c22:c23
more :: 0':s:nil:cons:double:1':bug_list_not -> 0':s:nil:cons:double:1':bug_list_not
false :: true:false
c23 :: c24:c25 -> c22:c23
S2BIN2 :: 0':s:nil:cons:double:1':bug_list_not -> 0':s:nil:cons:double:1':bug_list_not -> c24:c25
c24 :: c24:c25
c25 :: c26:c27 -> c:c1:c2:c3 -> c7:c8 -> c24:c25
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 -> c26:c27
eq :: 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
c26 :: c26:c27
c27 :: c24:c25 -> c26:c27
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
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_c:c1:c2:c31_28 :: c:c1:c2:c3
hole_0':s:nil:cons:double:1':bug_list_not2_28 :: 0':s:nil:cons:double:1':bug_list_not
hole_c4:c5:c63_28 :: c4:c5:c6
hole_c7:c84_28 :: c7:c8
hole_c9:c10:c115_28 :: c9:c10:c11
hole_c12:c13:c146_28 :: c12:c13:c14
hole_c15:c16:c177_28 :: c15:c16:c17
hole_c18:c198_28 :: c18:c19
hole_c209_28 :: c20
hole_c2110_28 :: c21
hole_c22:c2311_28 :: c22:c23
hole_true:false12_28 :: true:false
hole_c24:c2513_28 :: c24:c25
hole_c26:c2714_28 :: c26:c27
gen_c:c1:c2:c315_28 :: Nat -> c:c1:c2:c3
gen_0':s:nil:cons:double:1':bug_list_not16_28 :: Nat -> 0':s:nil:cons:double:1':bug_list_not
gen_c4:c5:c617_28 :: Nat -> c4:c5:c6
gen_c9:c10:c1118_28 :: Nat -> c9:c10:c11
gen_c12:c13:c1419_28 :: Nat -> c12:c13:c14
gen_c15:c16:c1720_28 :: Nat -> c15:c16:c17


Lemmas:
EQ(gen_0':s:nil:cons:double:1':bug_list_not16_28(n22_28), gen_0':s:nil:cons:double:1':bug_list_not16_28(n22_28)) -> gen_c:c1:c2:c315_28(n22_28), rt in Omega(1 + n22_28)
LT(gen_0':s:nil:cons:double:1':bug_list_not16_28(n1267_28), gen_0':s:nil:cons:double:1':bug_list_not16_28(+(1, n1267_28))) -> gen_c4:c5:c617_28(n1267_28), rt in Omega(1 + n1267_28)
HALF(gen_0':s:nil:cons:double:1':bug_list_not16_28(*(2, n2297_28))) -> gen_c12:c13:c1419_28(n2297_28), rt in Omega(1 + n2297_28)
half(gen_0':s:nil:cons:double:1':bug_list_not16_28(*(2, n3068_28))) -> gen_0':s:nil:cons:double:1':bug_list_not16_28(n3068_28), rt in Omega(0)
lt(gen_0':s:nil:cons:double:1':bug_list_not16_28(n4023_28), gen_0':s:nil:cons:double:1':bug_list_not16_28(+(1, n4023_28))) -> true, rt in Omega(0)


Generator Equations:
gen_c:c1:c2:c315_28(0) <=> c
gen_c:c1:c2:c315_28(+(x, 1)) <=> c3(gen_c:c1:c2:c315_28(x))
gen_0':s:nil:cons:double:1':bug_list_not16_28(0) <=> 0'
gen_0':s:nil:cons:double:1':bug_list_not16_28(+(x, 1)) <=> s(gen_0':s:nil:cons:double:1':bug_list_not16_28(x))
gen_c4:c5:c617_28(0) <=> c4
gen_c4:c5:c617_28(+(x, 1)) <=> c6(gen_c4:c5:c617_28(x))
gen_c9:c10:c1118_28(0) <=> c9
gen_c9:c10:c1118_28(+(x, 1)) <=> c10(gen_c9:c10:c1118_28(x))
gen_c12:c13:c1419_28(0) <=> c12
gen_c12:c13:c1419_28(+(x, 1)) <=> c14(gen_c12:c13:c1419_28(x))
gen_c15:c16:c1720_28(0) <=> c15
gen_c15:c16:c1720_28(+(x, 1)) <=> c17(gen_c15:c16:c1720_28(x), c12)


The following defined symbols remain to be analysed:
log, S2BIN1, S2BIN2, eq, bin2ss, s2bin1, s2bin2

They will be analysed ascendingly in the following order:
log < S2BIN1
S2BIN2 < S2BIN1
log < s2bin1
eq < S2BIN2
eq < s2bin2
s2bin2 < s2bin1

----------------------------------------

(25) RewriteLemmaProof (LOWER BOUND(ID))
Proved the following rewrite lemma:
eq(gen_0':s:nil:cons:double:1':bug_list_not16_28(n4858_28), gen_0':s:nil:cons:double:1':bug_list_not16_28(n4858_28)) -> true, rt in Omega(0)

Induction Base:
eq(gen_0':s:nil:cons:double:1':bug_list_not16_28(0), gen_0':s:nil:cons:double:1':bug_list_not16_28(0)) ->_R^Omega(0)
true

Induction Step:
eq(gen_0':s:nil:cons:double:1':bug_list_not16_28(+(n4858_28, 1)), gen_0':s:nil:cons:double:1':bug_list_not16_28(+(n4858_28, 1))) ->_R^Omega(0)
eq(gen_0':s:nil:cons:double:1':bug_list_not16_28(n4858_28), gen_0':s:nil:cons:double:1':bug_list_not16_28(n4858_28)) ->_IH
true

We have rt in Omega(1) and sz in O(n). Thus, we have irc_R in Omega(n^0).
----------------------------------------

(26)
Obligation:
Innermost TRS:
Rules:
EQ(0', 0') -> c
EQ(0', s(z0)) -> c1
EQ(s(z0), 0') -> c2
EQ(s(z0), s(z1)) -> c3(EQ(z0, z1))
LT(0', s(z0)) -> c4
LT(z0, 0') -> c5
LT(s(z0), s(z1)) -> c6(LT(z0, z1))
BIN2S(nil) -> c7
BIN2S(cons(z0, z1)) -> c8(BIN2SS(z0, z1))
BIN2SS(z0, nil) -> c9
BIN2SS(z0, cons(0', z1)) -> c10(BIN2SS(double(z0), z1))
BIN2SS(z0, cons(1', z1)) -> c11(BIN2SS(s(double(z0)), z1))
HALF(0') -> c12
HALF(s(0')) -> c13
HALF(s(s(z0))) -> c14(HALF(z0))
LOG(0') -> c15
LOG(s(0')) -> c16
LOG(s(s(z0))) -> c17(LOG(half(s(s(z0)))), HALF(s(s(z0))))
MORE(nil) -> c18
MORE(cons(z0, z1)) -> c19
S2BIN(z0) -> c20(S2BIN1(z0, 0', cons(nil, nil)))
S2BIN1(z0, z1, z2) -> c21(IF1(lt(z1, log(z0)), z0, z1, z2), LT(z1, log(z0)), LOG(z0))
IF1(true, z0, z1, z2) -> c22(S2BIN1(z0, s(z1), more(z2)), MORE(z2))
IF1(false, z0, z1, z2) -> c23(S2BIN2(z0, z2))
S2BIN2(z0, nil) -> c24
S2BIN2(z0, cons(z1, z2)) -> c25(IF2(eq(z0, bin2s(z1)), z0, z1, z2), EQ(z0, bin2s(z1)), BIN2S(z1))
IF2(true, z0, z1, z2) -> c26
IF2(false, z0, z1, z2) -> c27(S2BIN2(z0, z2))
eq(0', 0') -> true
eq(0', s(z0)) -> false
eq(s(z0), 0') -> false
eq(s(z0), s(z1)) -> eq(z0, z1)
lt(0', s(z0)) -> true
lt(z0, 0') -> false
lt(s(z0), s(z1)) -> lt(z0, z1)
bin2s(nil) -> 0'
bin2s(cons(z0, z1)) -> bin2ss(z0, z1)
bin2ss(z0, nil) -> z0
bin2ss(z0, cons(0', z1)) -> bin2ss(double(z0), z1)
bin2ss(z0, cons(1', z1)) -> bin2ss(s(double(z0)), z1)
half(0') -> 0'
half(s(0')) -> 0'
half(s(s(z0))) -> s(half(z0))
log(0') -> 0'
log(s(0')) -> 0'
log(s(s(z0))) -> s(log(half(s(s(z0)))))
more(nil) -> nil
more(cons(z0, z1)) -> cons(cons(0', z0), cons(cons(1', z0), cons(z0, z1)))
s2bin(z0) -> s2bin1(z0, 0', cons(nil, nil))
s2bin1(z0, z1, z2) -> if1(lt(z1, log(z0)), z0, z1, z2)
if1(true, z0, z1, z2) -> s2bin1(z0, s(z1), more(z2))
if1(false, z0, z1, z2) -> s2bin2(z0, z2)
s2bin2(z0, nil) -> bug_list_not
s2bin2(z0, cons(z1, z2)) -> if2(eq(z0, bin2s(z1)), z0, z1, z2)
if2(true, z0, z1, z2) -> z1
if2(false, z0, z1, z2) -> s2bin2(z0, z2)

Types:
EQ :: 0':s:nil:cons:double:1':bug_list_not -> 0':s:nil:cons:double:1':bug_list_not -> c:c1:c2:c3
0' :: 0':s:nil:cons:double:1':bug_list_not
c :: c:c1:c2:c3
s :: 0':s:nil:cons:double:1':bug_list_not -> 0':s:nil:cons:double:1':bug_list_not
c1 :: c:c1:c2:c3
c2 :: c:c1:c2:c3
c3 :: c:c1:c2:c3 -> c:c1:c2:c3
LT :: 0':s:nil:cons:double:1':bug_list_not -> 0':s:nil:cons:double:1':bug_list_not -> c4:c5:c6
c4 :: c4:c5:c6
c5 :: c4:c5:c6
c6 :: c4:c5:c6 -> c4:c5:c6
BIN2S :: 0':s:nil:cons:double:1':bug_list_not -> c7:c8
nil :: 0':s:nil:cons:double:1':bug_list_not
c7 :: c7:c8
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
c8 :: c9:c10:c11 -> c7:c8
BIN2SS :: 0':s:nil:cons:double:1':bug_list_not -> 0':s:nil:cons:double:1':bug_list_not -> c9:c10:c11
c9 :: c9:c10:c11
c10 :: c9:c10:c11 -> c9:c10:c11
double :: 0':s:nil:cons:double:1':bug_list_not -> 0':s:nil:cons:double:1':bug_list_not
1' :: 0':s:nil:cons:double:1':bug_list_not
c11 :: c9:c10:c11 -> c9:c10:c11
HALF :: 0':s:nil:cons:double:1':bug_list_not -> c12:c13:c14
c12 :: c12:c13:c14
c13 :: c12:c13:c14
c14 :: c12:c13:c14 -> c12:c13:c14
LOG :: 0':s:nil:cons:double:1':bug_list_not -> c15:c16:c17
c15 :: c15:c16:c17
c16 :: c15:c16:c17
c17 :: c15:c16:c17 -> c12:c13:c14 -> c15:c16:c17
half :: 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 -> c18:c19
c18 :: c18:c19
c19 :: c18:c19
S2BIN :: 0':s:nil:cons:double:1':bug_list_not -> c20
c20 :: c21 -> c20
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 -> c21
c21 :: c22:c23 -> c4:c5:c6 -> c15:c16:c17 -> c21
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 -> c22:c23
lt :: 0':s:nil:cons:double:1':bug_list_not -> 0':s:nil:cons:double:1':bug_list_not -> true:false
log :: 0':s:nil:cons:double:1':bug_list_not -> 0':s:nil:cons:double:1':bug_list_not
true :: true:false
c22 :: c21 -> c18:c19 -> c22:c23
more :: 0':s:nil:cons:double:1':bug_list_not -> 0':s:nil:cons:double:1':bug_list_not
false :: true:false
c23 :: c24:c25 -> c22:c23
S2BIN2 :: 0':s:nil:cons:double:1':bug_list_not -> 0':s:nil:cons:double:1':bug_list_not -> c24:c25
c24 :: c24:c25
c25 :: c26:c27 -> c:c1:c2:c3 -> c7:c8 -> c24:c25
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 -> c26:c27
eq :: 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
c26 :: c26:c27
c27 :: c24:c25 -> c26:c27
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
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_c:c1:c2:c31_28 :: c:c1:c2:c3
hole_0':s:nil:cons:double:1':bug_list_not2_28 :: 0':s:nil:cons:double:1':bug_list_not
hole_c4:c5:c63_28 :: c4:c5:c6
hole_c7:c84_28 :: c7:c8
hole_c9:c10:c115_28 :: c9:c10:c11
hole_c12:c13:c146_28 :: c12:c13:c14
hole_c15:c16:c177_28 :: c15:c16:c17
hole_c18:c198_28 :: c18:c19
hole_c209_28 :: c20
hole_c2110_28 :: c21
hole_c22:c2311_28 :: c22:c23
hole_true:false12_28 :: true:false
hole_c24:c2513_28 :: c24:c25
hole_c26:c2714_28 :: c26:c27
gen_c:c1:c2:c315_28 :: Nat -> c:c1:c2:c3
gen_0':s:nil:cons:double:1':bug_list_not16_28 :: Nat -> 0':s:nil:cons:double:1':bug_list_not
gen_c4:c5:c617_28 :: Nat -> c4:c5:c6
gen_c9:c10:c1118_28 :: Nat -> c9:c10:c11
gen_c12:c13:c1419_28 :: Nat -> c12:c13:c14
gen_c15:c16:c1720_28 :: Nat -> c15:c16:c17


Lemmas:
EQ(gen_0':s:nil:cons:double:1':bug_list_not16_28(n22_28), gen_0':s:nil:cons:double:1':bug_list_not16_28(n22_28)) -> gen_c:c1:c2:c315_28(n22_28), rt in Omega(1 + n22_28)
LT(gen_0':s:nil:cons:double:1':bug_list_not16_28(n1267_28), gen_0':s:nil:cons:double:1':bug_list_not16_28(+(1, n1267_28))) -> gen_c4:c5:c617_28(n1267_28), rt in Omega(1 + n1267_28)
HALF(gen_0':s:nil:cons:double:1':bug_list_not16_28(*(2, n2297_28))) -> gen_c12:c13:c1419_28(n2297_28), rt in Omega(1 + n2297_28)
half(gen_0':s:nil:cons:double:1':bug_list_not16_28(*(2, n3068_28))) -> gen_0':s:nil:cons:double:1':bug_list_not16_28(n3068_28), rt in Omega(0)
lt(gen_0':s:nil:cons:double:1':bug_list_not16_28(n4023_28), gen_0':s:nil:cons:double:1':bug_list_not16_28(+(1, n4023_28))) -> true, rt in Omega(0)
eq(gen_0':s:nil:cons:double:1':bug_list_not16_28(n4858_28), gen_0':s:nil:cons:double:1':bug_list_not16_28(n4858_28)) -> true, rt in Omega(0)


Generator Equations:
gen_c:c1:c2:c315_28(0) <=> c
gen_c:c1:c2:c315_28(+(x, 1)) <=> c3(gen_c:c1:c2:c315_28(x))
gen_0':s:nil:cons:double:1':bug_list_not16_28(0) <=> 0'
gen_0':s:nil:cons:double:1':bug_list_not16_28(+(x, 1)) <=> s(gen_0':s:nil:cons:double:1':bug_list_not16_28(x))
gen_c4:c5:c617_28(0) <=> c4
gen_c4:c5:c617_28(+(x, 1)) <=> c6(gen_c4:c5:c617_28(x))
gen_c9:c10:c1118_28(0) <=> c9
gen_c9:c10:c1118_28(+(x, 1)) <=> c10(gen_c9:c10:c1118_28(x))
gen_c12:c13:c1419_28(0) <=> c12
gen_c12:c13:c1419_28(+(x, 1)) <=> c14(gen_c12:c13:c1419_28(x))
gen_c15:c16:c1720_28(0) <=> c15
gen_c15:c16:c1720_28(+(x, 1)) <=> c17(gen_c15:c16:c1720_28(x), c12)


The following defined symbols remain to be analysed:
S2BIN2, S2BIN1, bin2ss, s2bin1, s2bin2

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