(STRATEGY
    INNERMOST)

(VAR
    l x)
(DATATYPES
    A = µX.< 0, s(X), true, false, cons(X, X), nil >)
(SIGNATURES
    half :: [A] -> A
    lastbit :: [A] -> A
    zero :: [A] -> A
    conv :: [A] -> A
    conviter :: [A x A] -> A
    if :: [A x A x A] -> A)
(RULES
    half(0()) -> 0()
    half(s(0())) -> 0()
    half(s(s(x))) -> s(half(x))
    lastbit(0()) -> 0()
    lastbit(s(0())) -> s(0())
    lastbit(s(s(x))) -> lastbit(x)
    zero(0()) -> true()
    zero(s(x)) -> false()
    conv(x) -> conviter(x
                       ,cons(0(),nil()))
    conviter(x,l) -> if(zero(x),x,l)
    if(true(),x,l) -> l
    if(false(),x,l) ->
      conviter(half(x)
              ,cons(lastbit(x),l)))