Once the process specifications, constraints, and policies are coded
as logic expressions, we must determine when a case is in agreement
with these process specifications, constraints, and policies. A
workcase can be seen as a subsequence of a model. If the current time
is ,
then the workcase *wc* is a sequence
.
We will denote the state
*s*_{i} of the workcase *wc* as *wc*|*i*.

We will call a model *m* a **continuation** of a workcase *wc*,
after time ,
if for all
,
*m*|*i* = *wc*|*i*. A
continuation is a model that agrees with the workcase up to time
.

We will collect the logical formulas that state the policies,
constraints, and processes in a single formula *F*, which can be
thought as the conjunction of all the individual formulas.

A workcase *wc* is consistent with the set of procedures and policies
*F*, up to time ,
if there exists at least one model *m* that is
a continuation of *wc* after time ,
such that
.
That is the workcase is consistent with the set of policies
and procedures if there is at least one possible continuation of that
workcase that satisfy the formulas in *F* for all times.

We denote that a workcase *wc* is consistent up to time
with
the set *F* as

(18) |

For example, let us suppose that the case developed as below, where
the top row refer to states and the bottom row lists the
propositions that are *true* in each state.

The workcase, up to time