(STRATEGY
    INNERMOST)

(VAR
    L X Y)
(DATATYPES
    A = µX.< 0, true, s(X), false, cons(X, X), nil >)
(SIGNATURES
    eq :: [A x A] -> A
    inf :: [A] -> A
    take :: [A x A] -> A
    length :: [A] -> A)
(RULES
    eq(0(),0()) -> true()
    eq(s(X),s(Y)) -> eq(X,Y)
    eq(X,Y) -> false()
    inf(X) -> cons(X,inf(s(X)))
    take(0(),X) -> nil()
    take(s(X),cons(Y,L)) -> cons(Y
                                ,take(X,L))
    length(nil()) -> 0()
    length(cons(X,L)) ->
      s(length(L)))