MAYBE
Time: 0.026310
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))),
        s2bin1(x, y, lists) -> if1(lt(y, log x), x, y, lists),
                    s2bin x -> s2bin1(x, 0(), cons(nil(), nil())),
   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)}
 DP:
  DP:
   {             eq#(s x, s y) -> eq#(x, y),
                 lt#(s x, s y) -> lt#(x, y),
            bin2s# cons(x, xs) -> bin2ss#(x, xs),
     bin2ss#(x, cons(0(), xs)) -> bin2ss#(double x, xs),
     bin2ss#(x, cons(1(), xs)) -> bin2ss#(s double x, xs),
                   half# s s x -> half# x,
                    log# s s x -> half# s s x,
                    log# s s x -> log# half s s x,
          s2bin1#(x, y, lists) -> lt#(y, log x),
          s2bin1#(x, y, lists) -> log# x,
          s2bin1#(x, y, lists) -> if1#(lt(y, log x), x, y, lists),
                      s2bin# x -> s2bin1#(x, 0(), cons(nil(), nil())),
     if1#(true(), x, y, lists) -> more# lists,
     if1#(true(), x, y, lists) -> s2bin1#(x, s y, more lists),
    if1#(false(), x, y, lists) -> s2bin2#(x, lists),
      s2bin2#(x, cons(xs, ys)) -> eq#(x, bin2s xs),
      s2bin2#(x, cons(xs, ys)) -> bin2s# xs,
      s2bin2#(x, cons(xs, ys)) -> if2#(eq(x, bin2s xs), x, xs, ys),
      if2#(false(), x, xs, ys) -> s2bin2#(x, ys)}
  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))),
         s2bin1(x, y, lists) -> if1(lt(y, log x), x, y, lists),
                     s2bin x -> s2bin1(x, 0(), cons(nil(), nil())),
    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)}
  EDG:
   {(if1#(true(), x, y, lists) -> s2bin1#(x, s y, more lists), s2bin1#(x, y, lists) -> if1#(lt(y, log x), x, y, lists))
    (if1#(true(), x, y, lists) -> s2bin1#(x, s y, more lists), s2bin1#(x, y, lists) -> log# x)
    (if1#(true(), x, y, lists) -> s2bin1#(x, s y, more lists), s2bin1#(x, y, lists) -> lt#(y, log x))
    (lt#(s x, s y) -> lt#(x, y), lt#(s x, s y) -> lt#(x, y))
    (if1#(false(), x, y, lists) -> s2bin2#(x, lists), s2bin2#(x, cons(xs, ys)) -> if2#(eq(x, bin2s xs), x, xs, ys))
    (if1#(false(), x, y, lists) -> s2bin2#(x, lists), s2bin2#(x, cons(xs, ys)) -> bin2s# xs)
    (if1#(false(), x, y, lists) -> s2bin2#(x, lists), s2bin2#(x, cons(xs, ys)) -> eq#(x, bin2s xs))
    (s2bin2#(x, cons(xs, ys)) -> eq#(x, bin2s xs), eq#(s x, s y) -> eq#(x, y))
    (s2bin2#(x, cons(xs, ys)) -> bin2s# xs, bin2s# cons(x, xs) -> bin2ss#(x, xs))
    (s2bin2#(x, cons(xs, ys)) -> if2#(eq(x, bin2s xs), x, xs, ys), if2#(false(), x, xs, ys) -> s2bin2#(x, ys))
    (bin2ss#(x, cons(1(), xs)) -> bin2ss#(s double x, xs), bin2ss#(x, cons(1(), xs)) -> bin2ss#(s double x, xs))
    (bin2ss#(x, cons(1(), xs)) -> bin2ss#(s double x, xs), bin2ss#(x, cons(0(), xs)) -> bin2ss#(double x, xs))
    (log# s s x -> log# half s s x, log# s s x -> log# half s s x)
    (log# s s x -> log# half s s x, log# s s x -> half# s s x)
    (half# s s x -> half# x, half# s s x -> half# x)
    (s2bin1#(x, y, lists) -> log# x, log# s s x -> half# s s x)
    (s2bin1#(x, y, lists) -> log# x, log# s s x -> log# half s s x)
    (log# s s x -> half# s s x, half# s s x -> half# x)
    (if2#(false(), x, xs, ys) -> s2bin2#(x, ys), s2bin2#(x, cons(xs, ys)) -> eq#(x, bin2s xs))
    (if2#(false(), x, xs, ys) -> s2bin2#(x, ys), s2bin2#(x, cons(xs, ys)) -> bin2s# xs)
    (if2#(false(), x, xs, ys) -> s2bin2#(x, ys), s2bin2#(x, cons(xs, ys)) -> if2#(eq(x, bin2s xs), x, xs, ys))
    (bin2ss#(x, cons(0(), xs)) -> bin2ss#(double x, xs), bin2ss#(x, cons(0(), xs)) -> bin2ss#(double x, xs))
    (bin2ss#(x, cons(0(), xs)) -> bin2ss#(double x, xs), bin2ss#(x, cons(1(), xs)) -> bin2ss#(s double x, xs))
    (s2bin1#(x, y, lists) -> if1#(lt(y, log x), x, y, lists), if1#(true(), x, y, lists) -> more# lists)
    (s2bin1#(x, y, lists) -> if1#(lt(y, log x), x, y, lists), if1#(true(), x, y, lists) -> s2bin1#(x, s y, more lists))
    (s2bin1#(x, y, lists) -> if1#(lt(y, log x), x, y, lists), if1#(false(), x, y, lists) -> s2bin2#(x, lists))
    (s2bin1#(x, y, lists) -> lt#(y, log x), lt#(s x, s y) -> lt#(x, y))
    (bin2s# cons(x, xs) -> bin2ss#(x, xs), bin2ss#(x, cons(0(), xs)) -> bin2ss#(double x, xs))
    (bin2s# cons(x, xs) -> bin2ss#(x, xs), bin2ss#(x, cons(1(), xs)) -> bin2ss#(s double x, xs))
    (eq#(s x, s y) -> eq#(x, y), eq#(s x, s y) -> eq#(x, y))
    (s2bin# x -> s2bin1#(x, 0(), cons(nil(), nil())), s2bin1#(x, y, lists) -> lt#(y, log x))
    (s2bin# x -> s2bin1#(x, 0(), cons(nil(), nil())), s2bin1#(x, y, lists) -> log# x)
    (s2bin# x -> s2bin1#(x, 0(), cons(nil(), nil())), s2bin1#(x, y, lists) -> if1#(lt(y, log x), x, y, lists))}
   EDG:
    {(if1#(true(), x, y, lists) -> s2bin1#(x, s y, more lists), s2bin1#(x, y, lists) -> if1#(lt(y, log x), x, y, lists))
     (if1#(true(), x, y, lists) -> s2bin1#(x, s y, more lists), s2bin1#(x, y, lists) -> log# x)
     (if1#(true(), x, y, lists) -> s2bin1#(x, s y, more lists), s2bin1#(x, y, lists) -> lt#(y, log x))
     (lt#(s x, s y) -> lt#(x, y), lt#(s x, s y) -> lt#(x, y))
     (if1#(false(), x, y, lists) -> s2bin2#(x, lists), s2bin2#(x, cons(xs, ys)) -> if2#(eq(x, bin2s xs), x, xs, ys))
     (if1#(false(), x, y, lists) -> s2bin2#(x, lists), s2bin2#(x, cons(xs, ys)) -> bin2s# xs)
     (if1#(false(), x, y, lists) -> s2bin2#(x, lists), s2bin2#(x, cons(xs, ys)) -> eq#(x, bin2s xs))
     (s2bin2#(x, cons(xs, ys)) -> eq#(x, bin2s xs), eq#(s x, s y) -> eq#(x, y))
     (s2bin2#(x, cons(xs, ys)) -> bin2s# xs, bin2s# cons(x, xs) -> bin2ss#(x, xs))
     (s2bin2#(x, cons(xs, ys)) -> if2#(eq(x, bin2s xs), x, xs, ys), if2#(false(), x, xs, ys) -> s2bin2#(x, ys))
     (bin2ss#(x, cons(1(), xs)) -> bin2ss#(s double x, xs), bin2ss#(x, cons(1(), xs)) -> bin2ss#(s double x, xs))
     (bin2ss#(x, cons(1(), xs)) -> bin2ss#(s double x, xs), bin2ss#(x, cons(0(), xs)) -> bin2ss#(double x, xs))
     (log# s s x -> log# half s s x, log# s s x -> log# half s s x)
     (log# s s x -> log# half s s x, log# s s x -> half# s s x)
     (half# s s x -> half# x, half# s s x -> half# x)
     (s2bin1#(x, y, lists) -> log# x, log# s s x -> half# s s x)
     (s2bin1#(x, y, lists) -> log# x, log# s s x -> log# half s s x)
     (log# s s x -> half# s s x, half# s s x -> half# x)
     (if2#(false(), x, xs, ys) -> s2bin2#(x, ys), s2bin2#(x, cons(xs, ys)) -> eq#(x, bin2s xs))
     (if2#(false(), x, xs, ys) -> s2bin2#(x, ys), s2bin2#(x, cons(xs, ys)) -> bin2s# xs)
     (if2#(false(), x, xs, ys) -> s2bin2#(x, ys), s2bin2#(x, cons(xs, ys)) -> if2#(eq(x, bin2s xs), x, xs, ys))
     (bin2ss#(x, cons(0(), xs)) -> bin2ss#(double x, xs), bin2ss#(x, cons(0(), xs)) -> bin2ss#(double x, xs))
     (bin2ss#(x, cons(0(), xs)) -> bin2ss#(double x, xs), bin2ss#(x, cons(1(), xs)) -> bin2ss#(s double x, xs))
     (s2bin1#(x, y, lists) -> if1#(lt(y, log x), x, y, lists), if1#(true(), x, y, lists) -> more# lists)
     (s2bin1#(x, y, lists) -> if1#(lt(y, log x), x, y, lists), if1#(true(), x, y, lists) -> s2bin1#(x, s y, more lists))
     (s2bin1#(x, y, lists) -> if1#(lt(y, log x), x, y, lists), if1#(false(), x, y, lists) -> s2bin2#(x, lists))
     (s2bin1#(x, y, lists) -> lt#(y, log x), lt#(s x, s y) -> lt#(x, y))
     (bin2s# cons(x, xs) -> bin2ss#(x, xs), bin2ss#(x, cons(0(), xs)) -> bin2ss#(double x, xs))
     (bin2s# cons(x, xs) -> bin2ss#(x, xs), bin2ss#(x, cons(1(), xs)) -> bin2ss#(s double x, xs))
     (eq#(s x, s y) -> eq#(x, y), eq#(s x, s y) -> eq#(x, y))
     (s2bin# x -> s2bin1#(x, 0(), cons(nil(), nil())), s2bin1#(x, y, lists) -> lt#(y, log x))
     (s2bin# x -> s2bin1#(x, 0(), cons(nil(), nil())), s2bin1#(x, y, lists) -> log# x)
     (s2bin# x -> s2bin1#(x, 0(), cons(nil(), nil())), s2bin1#(x, y, lists) -> if1#(lt(y, log x), x, y, lists))}
    EDG:
     {(if1#(true(), x, y, lists) -> s2bin1#(x, s y, more lists), s2bin1#(x, y, lists) -> if1#(lt(y, log x), x, y, lists))
      (if1#(true(), x, y, lists) -> s2bin1#(x, s y, more lists), s2bin1#(x, y, lists) -> log# x)
      (if1#(true(), x, y, lists) -> s2bin1#(x, s y, more lists), s2bin1#(x, y, lists) -> lt#(y, log x))
      (lt#(s x, s y) -> lt#(x, y), lt#(s x, s y) -> lt#(x, y))
      (if1#(false(), x, y, lists) -> s2bin2#(x, lists), s2bin2#(x, cons(xs, ys)) -> if2#(eq(x, bin2s xs), x, xs, ys))
      (if1#(false(), x, y, lists) -> s2bin2#(x, lists), s2bin2#(x, cons(xs, ys)) -> bin2s# xs)
      (if1#(false(), x, y, lists) -> s2bin2#(x, lists), s2bin2#(x, cons(xs, ys)) -> eq#(x, bin2s xs))
      (s2bin2#(x, cons(xs, ys)) -> eq#(x, bin2s xs), eq#(s x, s y) -> eq#(x, y))
      (s2bin2#(x, cons(xs, ys)) -> bin2s# xs, bin2s# cons(x, xs) -> bin2ss#(x, xs))
      (s2bin2#(x, cons(xs, ys)) -> if2#(eq(x, bin2s xs), x, xs, ys), if2#(false(), x, xs, ys) -> s2bin2#(x, ys))
      (bin2ss#(x, cons(1(), xs)) -> bin2ss#(s double x, xs), bin2ss#(x, cons(1(), xs)) -> bin2ss#(s double x, xs))
      (bin2ss#(x, cons(1(), xs)) -> bin2ss#(s double x, xs), bin2ss#(x, cons(0(), xs)) -> bin2ss#(double x, xs))
      (log# s s x -> log# half s s x, log# s s x -> log# half s s x)
      (log# s s x -> log# half s s x, log# s s x -> half# s s x)
      (half# s s x -> half# x, half# s s x -> half# x)
      (s2bin1#(x, y, lists) -> log# x, log# s s x -> half# s s x)
      (s2bin1#(x, y, lists) -> log# x, log# s s x -> log# half s s x)
      (log# s s x -> half# s s x, half# s s x -> half# x)
      (if2#(false(), x, xs, ys) -> s2bin2#(x, ys), s2bin2#(x, cons(xs, ys)) -> eq#(x, bin2s xs))
      (if2#(false(), x, xs, ys) -> s2bin2#(x, ys), s2bin2#(x, cons(xs, ys)) -> bin2s# xs)
      (if2#(false(), x, xs, ys) -> s2bin2#(x, ys), s2bin2#(x, cons(xs, ys)) -> if2#(eq(x, bin2s xs), x, xs, ys))
      (bin2ss#(x, cons(0(), xs)) -> bin2ss#(double x, xs), bin2ss#(x, cons(0(), xs)) -> bin2ss#(double x, xs))
      (bin2ss#(x, cons(0(), xs)) -> bin2ss#(double x, xs), bin2ss#(x, cons(1(), xs)) -> bin2ss#(s double x, xs))
      (s2bin1#(x, y, lists) -> if1#(lt(y, log x), x, y, lists), if1#(true(), x, y, lists) -> more# lists)
      (s2bin1#(x, y, lists) -> if1#(lt(y, log x), x, y, lists), if1#(true(), x, y, lists) -> s2bin1#(x, s y, more lists))
      (s2bin1#(x, y, lists) -> if1#(lt(y, log x), x, y, lists), if1#(false(), x, y, lists) -> s2bin2#(x, lists))
      (s2bin1#(x, y, lists) -> lt#(y, log x), lt#(s x, s y) -> lt#(x, y))
      (bin2s# cons(x, xs) -> bin2ss#(x, xs), bin2ss#(x, cons(0(), xs)) -> bin2ss#(double x, xs))
      (bin2s# cons(x, xs) -> bin2ss#(x, xs), bin2ss#(x, cons(1(), xs)) -> bin2ss#(s double x, xs))
      (eq#(s x, s y) -> eq#(x, y), eq#(s x, s y) -> eq#(x, y))
      (s2bin# x -> s2bin1#(x, 0(), cons(nil(), nil())), s2bin1#(x, y, lists) -> lt#(y, log x))
      (s2bin# x -> s2bin1#(x, 0(), cons(nil(), nil())), s2bin1#(x, y, lists) -> log# x)
      (s2bin# x -> s2bin1#(x, 0(), cons(nil(), nil())), s2bin1#(x, y, lists) -> if1#(lt(y, log x), x, y, lists))}
     STATUS:
      arrows: 0.908587
      SCCS (7):
       Scc:
        {     s2bin1#(x, y, lists) -> if1#(lt(y, log x), x, y, lists),
         if1#(true(), x, y, lists) -> s2bin1#(x, s y, more lists)}
       Scc:
        {s2bin2#(x, cons(xs, ys)) -> if2#(eq(x, bin2s xs), x, xs, ys),
         if2#(false(), x, xs, ys) -> s2bin2#(x, ys)}
       Scc:
        {bin2ss#(x, cons(0(), xs)) -> bin2ss#(double x, xs),
         bin2ss#(x, cons(1(), xs)) -> bin2ss#(s double x, xs)}
       Scc:
        {eq#(s x, s y) -> eq#(x, y)}
       Scc:
        {log# s s x -> log# half s s x}
       Scc:
        {half# s s x -> half# x}
       Scc:
        {lt#(s x, s y) -> lt#(x, y)}
       
       
       SCC (2):
        Strict:
         {     s2bin1#(x, y, lists) -> if1#(lt(y, log x), x, y, lists),
          if1#(true(), x, y, lists) -> s2bin1#(x, s y, more lists)}
        Weak:
        {             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))),
               s2bin1(x, y, lists) -> if1(lt(y, log x), x, y, lists),
                           s2bin x -> s2bin1(x, 0(), cons(nil(), nil())),
          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)}
        Open
       
       SCC (2):
        Strict:
         {s2bin2#(x, cons(xs, ys)) -> if2#(eq(x, bin2s xs), x, xs, ys),
          if2#(false(), x, xs, ys) -> s2bin2#(x, ys)}
        Weak:
        {             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))),
               s2bin1(x, y, lists) -> if1(lt(y, log x), x, y, lists),
                           s2bin x -> s2bin1(x, 0(), cons(nil(), nil())),
          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)}
        Open
       
       
       SCC (2):
        Strict:
         {bin2ss#(x, cons(0(), xs)) -> bin2ss#(double x, xs),
          bin2ss#(x, cons(1(), xs)) -> bin2ss#(s double x, xs)}
        Weak:
        {             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))),
               s2bin1(x, y, lists) -> if1(lt(y, log x), x, y, lists),
                           s2bin x -> s2bin1(x, 0(), cons(nil(), nil())),
          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)}
        Open
       
       SCC (1):
        Strict:
         {eq#(s x, s y) -> eq#(x, y)}
        Weak:
        {             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))),
               s2bin1(x, y, lists) -> if1(lt(y, log x), x, y, lists),
                           s2bin x -> s2bin1(x, 0(), cons(nil(), nil())),
          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)}
        Open
       
       
       SCC (1):
        Strict:
         {log# s s x -> log# half s s x}
        Weak:
        {             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))),
               s2bin1(x, y, lists) -> if1(lt(y, log x), x, y, lists),
                           s2bin x -> s2bin1(x, 0(), cons(nil(), nil())),
          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)}
        Open
       
       SCC (1):
        Strict:
         {half# s s x -> half# x}
        Weak:
        {             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))),
               s2bin1(x, y, lists) -> if1(lt(y, log x), x, y, lists),
                           s2bin x -> s2bin1(x, 0(), cons(nil(), nil())),
          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)}
        Open
       
       SCC (1):
        Strict:
         {lt#(s x, s y) -> lt#(x, y)}
        Weak:
        {             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))),
               s2bin1(x, y, lists) -> if1(lt(y, log x), x, y, lists),
                           s2bin x -> s2bin1(x, 0(), cons(nil(), nil())),
          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)}
        Open