* Step 1: Sum WORST_CASE(Omega(n^1),?)
    + Considered Problem:
        - Strict TRS:
            bin2s(cons(x,xs)) -> bin2ss(x,xs)
            bin2s(nil()) -> 0()
            bin2ss(x,cons(0(),xs)) -> bin2ss(double(x),xs)
            bin2ss(x,cons(1(),xs)) -> bin2ss(s(double(x)),xs)
            bin2ss(x,nil()) -> x
            eq(0(),0()) -> true()
            eq(0(),s(y)) -> false()
            eq(s(x),0()) -> false()
            eq(s(x),s(y)) -> eq(x,y)
            half(0()) -> 0()
            half(s(0())) -> 0()
            half(s(s(x))) -> s(half(x))
            if1(false(),x,y,lists) -> s2bin2(x,lists)
            if1(true(),x,y,lists) -> s2bin1(x,s(y),more(lists))
            if2(false(),x,xs,ys) -> s2bin2(x,ys)
            if2(true(),x,xs,ys) -> xs
            log(0()) -> 0()
            log(s(0())) -> 0()
            log(s(s(x))) -> s(log(half(s(s(x)))))
            lt(x,0()) -> false()
            lt(0(),s(y)) -> true()
            lt(s(x),s(y)) -> lt(x,y)
            more(cons(xs,ys)) -> cons(cons(0(),xs),cons(cons(1(),xs),cons(xs,ys)))
            more(nil()) -> nil()
            s2bin(x) -> s2bin1(x,0(),cons(nil(),nil()))
            s2bin1(x,y,lists) -> if1(lt(y,log(x)),x,y,lists)
            s2bin2(x,cons(xs,ys)) -> if2(eq(x,bin2s(xs)),x,xs,ys)
            s2bin2(x,nil()) -> bug_list_not()
        - Signature:
            {bin2s/1,bin2ss/2,eq/2,half/1,if1/4,if2/4,log/1,lt/2,more/1,s2bin/1,s2bin1/3,s2bin2/2} / {0/0,1/0
            ,bug_list_not/0,cons/2,double/1,false/0,nil/0,s/1,true/0}
        - Obligation:
            innermost runtime complexity wrt. defined symbols {bin2s,bin2ss,eq,half,if1,if2,log,lt,more,s2bin,s2bin1
            ,s2bin2} and constructors {0,1,bug_list_not,cons,double,false,nil,s,true}
    + Applied Processor:
        Sum {left = someStrategy, right = someStrategy}
    + Details:
        ()
* Step 2: DecreasingLoops WORST_CASE(Omega(n^1),?)
    + Considered Problem:
        - Strict TRS:
            bin2s(cons(x,xs)) -> bin2ss(x,xs)
            bin2s(nil()) -> 0()
            bin2ss(x,cons(0(),xs)) -> bin2ss(double(x),xs)
            bin2ss(x,cons(1(),xs)) -> bin2ss(s(double(x)),xs)
            bin2ss(x,nil()) -> x
            eq(0(),0()) -> true()
            eq(0(),s(y)) -> false()
            eq(s(x),0()) -> false()
            eq(s(x),s(y)) -> eq(x,y)
            half(0()) -> 0()
            half(s(0())) -> 0()
            half(s(s(x))) -> s(half(x))
            if1(false(),x,y,lists) -> s2bin2(x,lists)
            if1(true(),x,y,lists) -> s2bin1(x,s(y),more(lists))
            if2(false(),x,xs,ys) -> s2bin2(x,ys)
            if2(true(),x,xs,ys) -> xs
            log(0()) -> 0()
            log(s(0())) -> 0()
            log(s(s(x))) -> s(log(half(s(s(x)))))
            lt(x,0()) -> false()
            lt(0(),s(y)) -> true()
            lt(s(x),s(y)) -> lt(x,y)
            more(cons(xs,ys)) -> cons(cons(0(),xs),cons(cons(1(),xs),cons(xs,ys)))
            more(nil()) -> nil()
            s2bin(x) -> s2bin1(x,0(),cons(nil(),nil()))
            s2bin1(x,y,lists) -> if1(lt(y,log(x)),x,y,lists)
            s2bin2(x,cons(xs,ys)) -> if2(eq(x,bin2s(xs)),x,xs,ys)
            s2bin2(x,nil()) -> bug_list_not()
        - Signature:
            {bin2s/1,bin2ss/2,eq/2,half/1,if1/4,if2/4,log/1,lt/2,more/1,s2bin/1,s2bin1/3,s2bin2/2} / {0/0,1/0
            ,bug_list_not/0,cons/2,double/1,false/0,nil/0,s/1,true/0}
        - Obligation:
            innermost runtime complexity wrt. defined symbols {bin2s,bin2ss,eq,half,if1,if2,log,lt,more,s2bin,s2bin1
            ,s2bin2} and constructors {0,1,bug_list_not,cons,double,false,nil,s,true}
    + Applied Processor:
        DecreasingLoops {bound = AnyLoop, narrow = 10}
    + Details:
        The system has following decreasing Loops:
          bin2ss(x,y){y -> cons(0(),y)} =
            bin2ss(x,cons(0(),y)) ->^+ bin2ss(double(x),y)
              = C[bin2ss(double(x),y) = bin2ss(x,y){x -> double(x)}]

WORST_CASE(Omega(n^1),?)