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