(VAR x y )
(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)
        
)