(VAR L X )
(RULES 
        tail(cons(X)) -> L
        incr(nil) -> nil
        incr(cons(X)) -> cons(s(X))
        adx(nil) -> nil
        adx(cons(X)) -> incr(cons(X))
        nats -> adx(zeros)
        zeros -> cons(0)
        head(cons(X)) -> X
        
)