We define the relation between states and
formulas (where
means: in state s formula
holds) inductively
on the structure of formulas as the least relation
satisfying:
The notation above means:
with u
substituted for the free occurrences of x .
If
, the whole formula
may be substituted for
, and since
, the ``recursion'' in the
definition of
is unbounded, whence the appeal
above to ``least relation''.
Note that the relation is not monotonic in its
left argument, i.e.,
when
,
does in general not imply
.