(VAR X N M)
(RULES 
and(tt) -> X
plus(N,0) -> N
plus(N,s(M)) -> s(plus(N,M))
)