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