MAYBE

We are left with following problem, upon which TcT provides the
certificate MAYBE.

Strict Trs:
  { eq(0(), 0()) -> true()
  , eq(0(), s(y)) -> false()
  , eq(s(x), 0()) -> false()
  , eq(s(x), s(y)) -> eq(x, y)
  , lt(x, 0()) -> false()
  , lt(0(), s(y)) -> true()
  , 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) }
Obligation:
  innermost runtime complexity
Answer:
  MAYBE

We add following dependency tuples:

Strict DPs:
  { eq^#(0(), 0()) -> c_1()
  , eq^#(0(), s(y)) -> c_2()
  , eq^#(s(x), 0()) -> c_3()
  , eq^#(s(x), s(y)) -> c_4(eq^#(x, y))
  , lt^#(x, 0()) -> c_5()
  , lt^#(0(), s(y)) -> c_6()
  , lt^#(s(x), s(y)) -> c_7(lt^#(x, y))
  , bin2s^#(nil()) -> c_8()
  , bin2s^#(cons(x, xs)) -> c_9(bin2ss^#(x, xs))
  , bin2ss^#(x, nil()) -> c_10()
  , bin2ss^#(x, cons(0(), xs)) -> c_11(bin2ss^#(double(x), xs))
  , bin2ss^#(x, cons(1(), xs)) -> c_12(bin2ss^#(s(double(x)), xs))
  , half^#(0()) -> c_13()
  , half^#(s(0())) -> c_14()
  , half^#(s(s(x))) -> c_15(half^#(x))
  , log^#(0()) -> c_16()
  , log^#(s(0())) -> c_17()
  , log^#(s(s(x))) -> c_18(log^#(half(s(s(x)))), half^#(s(s(x))))
  , more^#(nil()) -> c_19()
  , more^#(cons(xs, ys)) -> c_20()
  , s2bin^#(x) -> c_21(s2bin1^#(x, 0(), cons(nil(), nil())))
  , s2bin1^#(x, y, lists) ->
    c_22(if1^#(lt(y, log(x)), x, y, lists), lt^#(y, log(x)), log^#(x))
  , if1^#(true(), x, y, lists) ->
    c_23(s2bin1^#(x, s(y), more(lists)), more^#(lists))
  , if1^#(false(), x, y, lists) -> c_24(s2bin2^#(x, lists))
  , s2bin2^#(x, nil()) -> c_25()
  , s2bin2^#(x, cons(xs, ys)) ->
    c_26(if2^#(eq(x, bin2s(xs)), x, xs, ys),
         eq^#(x, bin2s(xs)),
         bin2s^#(xs))
  , if2^#(true(), x, xs, ys) -> c_27()
  , if2^#(false(), x, xs, ys) -> c_28(s2bin2^#(x, ys)) }

and mark the set of starting terms.

We are left with following problem, upon which TcT provides the
certificate MAYBE.

Strict DPs:
  { eq^#(0(), 0()) -> c_1()
  , eq^#(0(), s(y)) -> c_2()
  , eq^#(s(x), 0()) -> c_3()
  , eq^#(s(x), s(y)) -> c_4(eq^#(x, y))
  , lt^#(x, 0()) -> c_5()
  , lt^#(0(), s(y)) -> c_6()
  , lt^#(s(x), s(y)) -> c_7(lt^#(x, y))
  , bin2s^#(nil()) -> c_8()
  , bin2s^#(cons(x, xs)) -> c_9(bin2ss^#(x, xs))
  , bin2ss^#(x, nil()) -> c_10()
  , bin2ss^#(x, cons(0(), xs)) -> c_11(bin2ss^#(double(x), xs))
  , bin2ss^#(x, cons(1(), xs)) -> c_12(bin2ss^#(s(double(x)), xs))
  , half^#(0()) -> c_13()
  , half^#(s(0())) -> c_14()
  , half^#(s(s(x))) -> c_15(half^#(x))
  , log^#(0()) -> c_16()
  , log^#(s(0())) -> c_17()
  , log^#(s(s(x))) -> c_18(log^#(half(s(s(x)))), half^#(s(s(x))))
  , more^#(nil()) -> c_19()
  , more^#(cons(xs, ys)) -> c_20()
  , s2bin^#(x) -> c_21(s2bin1^#(x, 0(), cons(nil(), nil())))
  , s2bin1^#(x, y, lists) ->
    c_22(if1^#(lt(y, log(x)), x, y, lists), lt^#(y, log(x)), log^#(x))
  , if1^#(true(), x, y, lists) ->
    c_23(s2bin1^#(x, s(y), more(lists)), more^#(lists))
  , if1^#(false(), x, y, lists) -> c_24(s2bin2^#(x, lists))
  , s2bin2^#(x, nil()) -> c_25()
  , s2bin2^#(x, cons(xs, ys)) ->
    c_26(if2^#(eq(x, bin2s(xs)), x, xs, ys),
         eq^#(x, bin2s(xs)),
         bin2s^#(xs))
  , if2^#(true(), x, xs, ys) -> c_27()
  , if2^#(false(), x, xs, ys) -> c_28(s2bin2^#(x, ys)) }
Weak Trs:
  { eq(0(), 0()) -> true()
  , eq(0(), s(y)) -> false()
  , eq(s(x), 0()) -> false()
  , eq(s(x), s(y)) -> eq(x, y)
  , lt(x, 0()) -> false()
  , lt(0(), s(y)) -> true()
  , 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) }
Obligation:
  innermost runtime complexity
Answer:
  MAYBE

We estimate the number of application of
{1,2,3,5,6,8,10,13,14,16,17,19,20,25,27} by applications of
Pre({1,2,3,5,6,8,10,13,14,16,17,19,20,25,27}) =
{4,7,9,11,12,15,18,22,23,24,26,28}. Here rules are labeled as
follows:

  DPs:
    { 1: eq^#(0(), 0()) -> c_1()
    , 2: eq^#(0(), s(y)) -> c_2()
    , 3: eq^#(s(x), 0()) -> c_3()
    , 4: eq^#(s(x), s(y)) -> c_4(eq^#(x, y))
    , 5: lt^#(x, 0()) -> c_5()
    , 6: lt^#(0(), s(y)) -> c_6()
    , 7: lt^#(s(x), s(y)) -> c_7(lt^#(x, y))
    , 8: bin2s^#(nil()) -> c_8()
    , 9: bin2s^#(cons(x, xs)) -> c_9(bin2ss^#(x, xs))
    , 10: bin2ss^#(x, nil()) -> c_10()
    , 11: bin2ss^#(x, cons(0(), xs)) -> c_11(bin2ss^#(double(x), xs))
    , 12: bin2ss^#(x, cons(1(), xs)) ->
          c_12(bin2ss^#(s(double(x)), xs))
    , 13: half^#(0()) -> c_13()
    , 14: half^#(s(0())) -> c_14()
    , 15: half^#(s(s(x))) -> c_15(half^#(x))
    , 16: log^#(0()) -> c_16()
    , 17: log^#(s(0())) -> c_17()
    , 18: log^#(s(s(x))) -> c_18(log^#(half(s(s(x)))), half^#(s(s(x))))
    , 19: more^#(nil()) -> c_19()
    , 20: more^#(cons(xs, ys)) -> c_20()
    , 21: s2bin^#(x) -> c_21(s2bin1^#(x, 0(), cons(nil(), nil())))
    , 22: s2bin1^#(x, y, lists) ->
          c_22(if1^#(lt(y, log(x)), x, y, lists), lt^#(y, log(x)), log^#(x))
    , 23: if1^#(true(), x, y, lists) ->
          c_23(s2bin1^#(x, s(y), more(lists)), more^#(lists))
    , 24: if1^#(false(), x, y, lists) -> c_24(s2bin2^#(x, lists))
    , 25: s2bin2^#(x, nil()) -> c_25()
    , 26: s2bin2^#(x, cons(xs, ys)) ->
          c_26(if2^#(eq(x, bin2s(xs)), x, xs, ys),
               eq^#(x, bin2s(xs)),
               bin2s^#(xs))
    , 27: if2^#(true(), x, xs, ys) -> c_27()
    , 28: if2^#(false(), x, xs, ys) -> c_28(s2bin2^#(x, ys)) }

We are left with following problem, upon which TcT provides the
certificate MAYBE.

Strict DPs:
  { eq^#(s(x), s(y)) -> c_4(eq^#(x, y))
  , lt^#(s(x), s(y)) -> c_7(lt^#(x, y))
  , bin2s^#(cons(x, xs)) -> c_9(bin2ss^#(x, xs))
  , bin2ss^#(x, cons(0(), xs)) -> c_11(bin2ss^#(double(x), xs))
  , bin2ss^#(x, cons(1(), xs)) -> c_12(bin2ss^#(s(double(x)), xs))
  , half^#(s(s(x))) -> c_15(half^#(x))
  , log^#(s(s(x))) -> c_18(log^#(half(s(s(x)))), half^#(s(s(x))))
  , s2bin^#(x) -> c_21(s2bin1^#(x, 0(), cons(nil(), nil())))
  , s2bin1^#(x, y, lists) ->
    c_22(if1^#(lt(y, log(x)), x, y, lists), lt^#(y, log(x)), log^#(x))
  , if1^#(true(), x, y, lists) ->
    c_23(s2bin1^#(x, s(y), more(lists)), more^#(lists))
  , if1^#(false(), x, y, lists) -> c_24(s2bin2^#(x, lists))
  , s2bin2^#(x, cons(xs, ys)) ->
    c_26(if2^#(eq(x, bin2s(xs)), x, xs, ys),
         eq^#(x, bin2s(xs)),
         bin2s^#(xs))
  , if2^#(false(), x, xs, ys) -> c_28(s2bin2^#(x, ys)) }
Weak DPs:
  { eq^#(0(), 0()) -> c_1()
  , eq^#(0(), s(y)) -> c_2()
  , eq^#(s(x), 0()) -> c_3()
  , lt^#(x, 0()) -> c_5()
  , lt^#(0(), s(y)) -> c_6()
  , bin2s^#(nil()) -> c_8()
  , bin2ss^#(x, nil()) -> c_10()
  , half^#(0()) -> c_13()
  , half^#(s(0())) -> c_14()
  , log^#(0()) -> c_16()
  , log^#(s(0())) -> c_17()
  , more^#(nil()) -> c_19()
  , more^#(cons(xs, ys)) -> c_20()
  , s2bin2^#(x, nil()) -> c_25()
  , if2^#(true(), x, xs, ys) -> c_27() }
Weak Trs:
  { eq(0(), 0()) -> true()
  , eq(0(), s(y)) -> false()
  , eq(s(x), 0()) -> false()
  , eq(s(x), s(y)) -> eq(x, y)
  , lt(x, 0()) -> false()
  , lt(0(), s(y)) -> true()
  , 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) }
Obligation:
  innermost runtime complexity
Answer:
  MAYBE

The following weak DPs constitute a sub-graph of the DG that is
closed under successors. The DPs are removed.

{ eq^#(0(), 0()) -> c_1()
, eq^#(0(), s(y)) -> c_2()
, eq^#(s(x), 0()) -> c_3()
, lt^#(x, 0()) -> c_5()
, lt^#(0(), s(y)) -> c_6()
, bin2s^#(nil()) -> c_8()
, bin2ss^#(x, nil()) -> c_10()
, half^#(0()) -> c_13()
, half^#(s(0())) -> c_14()
, log^#(0()) -> c_16()
, log^#(s(0())) -> c_17()
, more^#(nil()) -> c_19()
, more^#(cons(xs, ys)) -> c_20()
, s2bin2^#(x, nil()) -> c_25()
, if2^#(true(), x, xs, ys) -> c_27() }

We are left with following problem, upon which TcT provides the
certificate MAYBE.

Strict DPs:
  { eq^#(s(x), s(y)) -> c_4(eq^#(x, y))
  , lt^#(s(x), s(y)) -> c_7(lt^#(x, y))
  , bin2s^#(cons(x, xs)) -> c_9(bin2ss^#(x, xs))
  , bin2ss^#(x, cons(0(), xs)) -> c_11(bin2ss^#(double(x), xs))
  , bin2ss^#(x, cons(1(), xs)) -> c_12(bin2ss^#(s(double(x)), xs))
  , half^#(s(s(x))) -> c_15(half^#(x))
  , log^#(s(s(x))) -> c_18(log^#(half(s(s(x)))), half^#(s(s(x))))
  , s2bin^#(x) -> c_21(s2bin1^#(x, 0(), cons(nil(), nil())))
  , s2bin1^#(x, y, lists) ->
    c_22(if1^#(lt(y, log(x)), x, y, lists), lt^#(y, log(x)), log^#(x))
  , if1^#(true(), x, y, lists) ->
    c_23(s2bin1^#(x, s(y), more(lists)), more^#(lists))
  , if1^#(false(), x, y, lists) -> c_24(s2bin2^#(x, lists))
  , s2bin2^#(x, cons(xs, ys)) ->
    c_26(if2^#(eq(x, bin2s(xs)), x, xs, ys),
         eq^#(x, bin2s(xs)),
         bin2s^#(xs))
  , if2^#(false(), x, xs, ys) -> c_28(s2bin2^#(x, ys)) }
Weak Trs:
  { eq(0(), 0()) -> true()
  , eq(0(), s(y)) -> false()
  , eq(s(x), 0()) -> false()
  , eq(s(x), s(y)) -> eq(x, y)
  , lt(x, 0()) -> false()
  , lt(0(), s(y)) -> true()
  , 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) }
Obligation:
  innermost runtime complexity
Answer:
  MAYBE

Due to missing edges in the dependency-graph, the right-hand sides
of following rules could be simplified:

  { if1^#(true(), x, y, lists) ->
    c_23(s2bin1^#(x, s(y), more(lists)), more^#(lists)) }

We are left with following problem, upon which TcT provides the
certificate MAYBE.

Strict DPs:
  { eq^#(s(x), s(y)) -> c_1(eq^#(x, y))
  , lt^#(s(x), s(y)) -> c_2(lt^#(x, y))
  , bin2s^#(cons(x, xs)) -> c_3(bin2ss^#(x, xs))
  , bin2ss^#(x, cons(0(), xs)) -> c_4(bin2ss^#(double(x), xs))
  , bin2ss^#(x, cons(1(), xs)) -> c_5(bin2ss^#(s(double(x)), xs))
  , half^#(s(s(x))) -> c_6(half^#(x))
  , log^#(s(s(x))) -> c_7(log^#(half(s(s(x)))), half^#(s(s(x))))
  , s2bin^#(x) -> c_8(s2bin1^#(x, 0(), cons(nil(), nil())))
  , s2bin1^#(x, y, lists) ->
    c_9(if1^#(lt(y, log(x)), x, y, lists), lt^#(y, log(x)), log^#(x))
  , if1^#(true(), x, y, lists) ->
    c_10(s2bin1^#(x, s(y), more(lists)))
  , if1^#(false(), x, y, lists) -> c_11(s2bin2^#(x, lists))
  , s2bin2^#(x, cons(xs, ys)) ->
    c_12(if2^#(eq(x, bin2s(xs)), x, xs, ys),
         eq^#(x, bin2s(xs)),
         bin2s^#(xs))
  , if2^#(false(), x, xs, ys) -> c_13(s2bin2^#(x, ys)) }
Weak Trs:
  { eq(0(), 0()) -> true()
  , eq(0(), s(y)) -> false()
  , eq(s(x), 0()) -> false()
  , eq(s(x), s(y)) -> eq(x, y)
  , lt(x, 0()) -> false()
  , lt(0(), s(y)) -> true()
  , 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) }
Obligation:
  innermost runtime complexity
Answer:
  MAYBE

We replace rewrite rules by usable rules:

  Weak Usable Rules:
    { eq(0(), 0()) -> true()
    , eq(0(), s(y)) -> false()
    , eq(s(x), 0()) -> false()
    , eq(s(x), s(y)) -> eq(x, y)
    , lt(x, 0()) -> false()
    , lt(0(), s(y)) -> true()
    , 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))) }

We are left with following problem, upon which TcT provides the
certificate MAYBE.

Strict DPs:
  { eq^#(s(x), s(y)) -> c_1(eq^#(x, y))
  , lt^#(s(x), s(y)) -> c_2(lt^#(x, y))
  , bin2s^#(cons(x, xs)) -> c_3(bin2ss^#(x, xs))
  , bin2ss^#(x, cons(0(), xs)) -> c_4(bin2ss^#(double(x), xs))
  , bin2ss^#(x, cons(1(), xs)) -> c_5(bin2ss^#(s(double(x)), xs))
  , half^#(s(s(x))) -> c_6(half^#(x))
  , log^#(s(s(x))) -> c_7(log^#(half(s(s(x)))), half^#(s(s(x))))
  , s2bin^#(x) -> c_8(s2bin1^#(x, 0(), cons(nil(), nil())))
  , s2bin1^#(x, y, lists) ->
    c_9(if1^#(lt(y, log(x)), x, y, lists), lt^#(y, log(x)), log^#(x))
  , if1^#(true(), x, y, lists) ->
    c_10(s2bin1^#(x, s(y), more(lists)))
  , if1^#(false(), x, y, lists) -> c_11(s2bin2^#(x, lists))
  , s2bin2^#(x, cons(xs, ys)) ->
    c_12(if2^#(eq(x, bin2s(xs)), x, xs, ys),
         eq^#(x, bin2s(xs)),
         bin2s^#(xs))
  , if2^#(false(), x, xs, ys) -> c_13(s2bin2^#(x, ys)) }
Weak Trs:
  { eq(0(), 0()) -> true()
  , eq(0(), s(y)) -> false()
  , eq(s(x), 0()) -> false()
  , eq(s(x), s(y)) -> eq(x, y)
  , lt(x, 0()) -> false()
  , lt(0(), s(y)) -> true()
  , 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))) }
Obligation:
  innermost runtime complexity
Answer:
  MAYBE

Consider the dependency graph

  1: eq^#(s(x), s(y)) -> c_1(eq^#(x, y))
     -->_1 eq^#(s(x), s(y)) -> c_1(eq^#(x, y)) :1
  
  2: lt^#(s(x), s(y)) -> c_2(lt^#(x, y))
     -->_1 lt^#(s(x), s(y)) -> c_2(lt^#(x, y)) :2
  
  3: bin2s^#(cons(x, xs)) -> c_3(bin2ss^#(x, xs))
     -->_1 bin2ss^#(x, cons(1(), xs)) ->
           c_5(bin2ss^#(s(double(x)), xs)) :5
     -->_1 bin2ss^#(x, cons(0(), xs)) -> c_4(bin2ss^#(double(x), xs)) :4
  
  4: bin2ss^#(x, cons(0(), xs)) -> c_4(bin2ss^#(double(x), xs))
     -->_1 bin2ss^#(x, cons(1(), xs)) ->
           c_5(bin2ss^#(s(double(x)), xs)) :5
     -->_1 bin2ss^#(x, cons(0(), xs)) -> c_4(bin2ss^#(double(x), xs)) :4
  
  5: bin2ss^#(x, cons(1(), xs)) -> c_5(bin2ss^#(s(double(x)), xs))
     -->_1 bin2ss^#(x, cons(1(), xs)) ->
           c_5(bin2ss^#(s(double(x)), xs)) :5
     -->_1 bin2ss^#(x, cons(0(), xs)) -> c_4(bin2ss^#(double(x), xs)) :4
  
  6: half^#(s(s(x))) -> c_6(half^#(x))
     -->_1 half^#(s(s(x))) -> c_6(half^#(x)) :6
  
  7: log^#(s(s(x))) -> c_7(log^#(half(s(s(x)))), half^#(s(s(x))))
     -->_1 log^#(s(s(x))) ->
           c_7(log^#(half(s(s(x)))), half^#(s(s(x)))) :7
     -->_2 half^#(s(s(x))) -> c_6(half^#(x)) :6
  
  8: s2bin^#(x) -> c_8(s2bin1^#(x, 0(), cons(nil(), nil())))
     -->_1 s2bin1^#(x, y, lists) ->
           c_9(if1^#(lt(y, log(x)), x, y, lists),
               lt^#(y, log(x)),
               log^#(x)) :9
  
  9: s2bin1^#(x, y, lists) ->
     c_9(if1^#(lt(y, log(x)), x, y, lists), lt^#(y, log(x)), log^#(x))
     -->_1 if1^#(false(), x, y, lists) -> c_11(s2bin2^#(x, lists)) :11
     -->_1 if1^#(true(), x, y, lists) ->
           c_10(s2bin1^#(x, s(y), more(lists))) :10
     -->_3 log^#(s(s(x))) ->
           c_7(log^#(half(s(s(x)))), half^#(s(s(x)))) :7
     -->_2 lt^#(s(x), s(y)) -> c_2(lt^#(x, y)) :2
  
  10: if1^#(true(), x, y, lists) ->
      c_10(s2bin1^#(x, s(y), more(lists)))
     -->_1 s2bin1^#(x, y, lists) ->
           c_9(if1^#(lt(y, log(x)), x, y, lists),
               lt^#(y, log(x)),
               log^#(x)) :9
  
  11: if1^#(false(), x, y, lists) -> c_11(s2bin2^#(x, lists))
     -->_1 s2bin2^#(x, cons(xs, ys)) ->
           c_12(if2^#(eq(x, bin2s(xs)), x, xs, ys),
                eq^#(x, bin2s(xs)),
                bin2s^#(xs)) :12
  
  12: s2bin2^#(x, cons(xs, ys)) ->
      c_12(if2^#(eq(x, bin2s(xs)), x, xs, ys),
           eq^#(x, bin2s(xs)),
           bin2s^#(xs))
     -->_1 if2^#(false(), x, xs, ys) -> c_13(s2bin2^#(x, ys)) :13
     -->_3 bin2s^#(cons(x, xs)) -> c_3(bin2ss^#(x, xs)) :3
     -->_2 eq^#(s(x), s(y)) -> c_1(eq^#(x, y)) :1
  
  13: if2^#(false(), x, xs, ys) -> c_13(s2bin2^#(x, ys))
     -->_1 s2bin2^#(x, cons(xs, ys)) ->
           c_12(if2^#(eq(x, bin2s(xs)), x, xs, ys),
                eq^#(x, bin2s(xs)),
                bin2s^#(xs)) :12
  

Following roots of the dependency graph are removed, as the
considered set of starting terms is closed under reduction with
respect to these rules (modulo compound contexts).

  { s2bin^#(x) -> c_8(s2bin1^#(x, 0(), cons(nil(), nil()))) }


We are left with following problem, upon which TcT provides the
certificate MAYBE.

Strict DPs:
  { eq^#(s(x), s(y)) -> c_1(eq^#(x, y))
  , lt^#(s(x), s(y)) -> c_2(lt^#(x, y))
  , bin2s^#(cons(x, xs)) -> c_3(bin2ss^#(x, xs))
  , bin2ss^#(x, cons(0(), xs)) -> c_4(bin2ss^#(double(x), xs))
  , bin2ss^#(x, cons(1(), xs)) -> c_5(bin2ss^#(s(double(x)), xs))
  , half^#(s(s(x))) -> c_6(half^#(x))
  , log^#(s(s(x))) -> c_7(log^#(half(s(s(x)))), half^#(s(s(x))))
  , s2bin1^#(x, y, lists) ->
    c_9(if1^#(lt(y, log(x)), x, y, lists), lt^#(y, log(x)), log^#(x))
  , if1^#(true(), x, y, lists) ->
    c_10(s2bin1^#(x, s(y), more(lists)))
  , if1^#(false(), x, y, lists) -> c_11(s2bin2^#(x, lists))
  , s2bin2^#(x, cons(xs, ys)) ->
    c_12(if2^#(eq(x, bin2s(xs)), x, xs, ys),
         eq^#(x, bin2s(xs)),
         bin2s^#(xs))
  , if2^#(false(), x, xs, ys) -> c_13(s2bin2^#(x, ys)) }
Weak Trs:
  { eq(0(), 0()) -> true()
  , eq(0(), s(y)) -> false()
  , eq(s(x), 0()) -> false()
  , eq(s(x), s(y)) -> eq(x, y)
  , lt(x, 0()) -> false()
  , lt(0(), s(y)) -> true()
  , 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))) }
Obligation:
  innermost runtime complexity
Answer:
  MAYBE

None of the processors succeeded.

Details of failed attempt(s):
-----------------------------
1) 'matrices' failed due to the following reason:
   
   None of the processors succeeded.
   
   Details of failed attempt(s):
   -----------------------------
   1) 'matrix interpretation of dimension 4' failed due to the
      following reason:
      
      Following exception was raised:
        stack overflow
   
   2) 'matrix interpretation of dimension 3' failed due to the
      following reason:
      
      The input cannot be shown compatible
   
   3) 'matrix interpretation of dimension 3' failed due to the
      following reason:
      
      The input cannot be shown compatible
   
   4) 'matrix interpretation of dimension 2' failed due to the
      following reason:
      
      The input cannot be shown compatible
   
   5) 'matrix interpretation of dimension 2' failed due to the
      following reason:
      
      The input cannot be shown compatible
   
   6) 'matrix interpretation of dimension 1' failed due to the
      following reason:
      
      The input cannot be shown compatible
   

2) 'empty' failed due to the following reason:
   
   Empty strict component of the problem is NOT empty.


Arrrr..