**Abstract**

In this note, we describe how a fragment of arithmetic can be decided in practice. We follow essentially the ideas of [Thatcher & Wright], which we have embedded in the Mona tool.

Mona is an implementation of *Monadic Second-order Logic*
on finite strings (and trees).
The previous semantics used in Mona is the one provided in current
literature [Straubing, Thomas], where the
meaning of first-order terms is restricted to being a position in the
string over which the formula is interpreted.

In this note, we describe our new semantics, where terms are
interpreted relative to *all* natural numbers. With this semantics
Mona becomes a decision procedure for the calculus called WS1S, the
Weak Second-order theory of 1 Successor.

We also show how the Mona representation of automata subsumes a recent proposal for representing queues. We exploit the natural semantics to carry out automated reasoning about queue operations.