(STRATEGY
    INNERMOST)

(VAR
    lists x xs y ys)
(DATATYPES
    A = µX.< 0, true, s(X), false, nil, cons(X, X), double(X), 1, bug_list_not >)
(SIGNATURES
    eq :: [A x A] -> A
    lt :: [A x A] -> A
    bin2s :: [A] -> A
    bin2ss :: [A x A] -> A
    half :: [A] -> A
    log :: [A] -> A
    more :: [A] -> A
    s2bin :: [A] -> A
    s2bin1 :: [A x A x A] -> A
    if1 :: [A x A x A x A] -> A
    s2bin2 :: [A x A] -> A
    if2 :: [A x A x A x A] -> A)
(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))