(STRATEGY
    INNERMOST)

(VAR
    x y)
(DATATYPES
    A = µX.< sent(X), nil, cons(X, X) >)
(SIGNATURES
    top :: [A] -> A
    rest :: [A] -> A
    check :: [A] -> A)
(RULES
    top(sent(x)) ->
      top(check(rest(x)))
    rest(nil()) -> sent(nil())
    rest(cons(x,y)) -> sent(y)
    check(sent(x)) -> sent(check(x))
    check(rest(x)) -> rest(check(x))
    check(cons(x,y)) ->
      cons(check(x),y)
    check(cons(x,y)) -> cons(x
                            ,check(y))
    check(cons(x,y)) -> cons(x,y))