**syntax:** `(ws1s &optional (fnums *) (examples? t)
(automaton? nil) (traces? nil) (verbose? t) (defs !)
theories rewrites exclude)`

**effect: **This strategy implements a decision procedure for the Weak Second-order
monadic logic of 1 Successor (WS1S). The supported fragment of WS1S
includes boolean expression, arithmetic on the natural numbers restricted
to addition/subraction with/from a constant, and operations on finite sets
over the naturals like union, intersection, set difference, addition and
removal of a natural. Predicates include arithmetic comparisons
like `<`, `<=`, `>`, `>=`,
equality, disequality, the subset relation,
and membership in the form `P(i)`. There is quantification over the booleans,
the natural numbers, finite sets of naturals, and predicate subtypes of the
aforementioned types built from formulas in the set just described.
Furthermore, natural numbers, and finite sets of natural numbers may also
be described using the `the` operator; e.g. ripple-carry addition may be
defined as:

+(P, Q: finite_set[nat]): finite_set[nat] = the({R: finite_set[nat] | EXISTS (C: finite_set[nat]): NOT(C(0)) AND FORALL (t: nat): (C(t + 1) = ((P(t) AND Q(t)) OR (P(t) AND C(t)) OR (Q(t) AND C(t)))) AND (R(t) = P(t) = Q(t) = C(t))});Using this definition, lemmas such as

plus_assoc: LEMMA FORALL (X, Y, Z: finite_set[nat]): X + (Y + Z) = (X + Y) + Zare proven to be valid by simply calling

In a first step, the WS1S strategy rewrites the
formulas specifed by `FNUMS`. The resulting formulas are then translated,
using the rule `WS1S-SIMP`, to an automaton which recognizes the language
of their interpretations. Hereby, subformulas that do not appear
to be in the WS1S fragment are abstracted away by introducing
new parameters. If the final automaton recognizes the full set,
the `FNUMS` formulas are replaced by `TRUE`; otherwise, these formulas are
left unchanged.

The `DEFS`, `THEORIES`, `REWRITES`, and `EXCLUDE` arguments are used to
install rewrites. For a precise description of their meaning see
e.g. `AUTO-REWRITE-THEORY` or `INSTALL-REWRITES`.

In case where the formulae specified by `FNUMS` are neither valid nor unsatisfiable
both a witness and a counterexample are displayed if the
flag `EXAMPLES?` is set. Hereby, expressions are displayed for
both the free variables in the `FNUMS` formulas and the newly introduced
abstraction parameters. An alternative, trace-oriented view of the
examples are displayed if the `TRACES?` flag is on.

With the `AUTOMATON?` flag turned on, the constructed automaton is
displayed.

Translation messages are being displayed whenever the flag `VERBOSE?`
is set to `T`. Messages like "Abstracting..." indicate the introduction
of a new parameter, and "Not abstractable ..." indicates that there
is a free occurrences of a bound variables in the current subformula.
In this case, the translation process aborts. A second source of
failure in the translation process comes from quantifiers which
contain bindings not included in WS1S. In these cases, a message
like "Not in ws1s: ... in ..." is displayed and the translation process
aborts.

These messages may be helpful in detecting expressions that
are not known to be in WS1S by the translator. In these cases,
it might be useful to decorate these expressions with appropriate
type coercions (e.g. `{x: nat | x = 1 OR x = 2} :: finite_set[nat]`)
to support the translation process.

**usage:** `(ws1s 1 :examples? nil :verbose?? nil)`
Tries to reduce formula 1 to true; suppresses both translation
messages and the display of a witness and a counterexample in
case this formula is neither valid nor satisfiable.

**errors:** "Formula ... not in WS1S"

The translation process could not construct a DFA for
the formula ...

**notes:** The WS1S strategy uses the libraries of Mona to construct
DFAs. Mona was developed at BRICS -
see http://www.brics.dk/~mona for details.