(VAR x y z)
(RULES
q(q(x,y),z) -> q(x,q(y,z))
q(x,q(y,z)) -> q(q(x,y),z)
q(e,x) -> x
q(x,e) -> x

plus(x,plus(y,z)) -> plus(plus(x,y),z)
plus(x,y) -> plus(y,x)
plus(0,x) -> x
plus(s(x),y) -> s(plus(x,y))

len(e) -> 0
len(a) -> s(0)
len(q(a,y)) -> plus(len(a),len(y))
)
(COMMENT
the length function for queues.
)