For each rule R and each state S appropriate for
R, we define a family
=
NUpdates(R,S)
of update sets over S . To fire R at S ,
choose any
and fire
at S .
We stipulate that an arbitrary rule R is equivalent, over the given S ,
to an S -perspicuous rule R' obtained from R by renaming the bound
variables. The equivalence means here that
NUpdates(R,S) = NUpdates(R',S)
.
It remains to define
=
NUpdates(R,S)
when S is
S -perspicuous.