(STRATEGY
    INNERMOST)

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