m2_m0-enter.tex

\noindent \ref{m0:enter} [t] \textbf{event}
\begin{block}
\item \textbf{during}
\begin{block}
\item[ \eqref{default} ]$\false$ %
\end{block}
\item \textbf{when}
\begin{block}
\item[ \eqref{ent:grd1} ]$\neg t \in in $ %
\item[ \eqref{et:g1} ]$\neg ent \in \ran.loc $ %
\end{block}
\item \textbf{begin}
\begin{block}
\item[ \eqref{a1} ]$in' = in \bunion \{ t \} $ %
\item[ \eqref{a3} ]$loc' = loc \1| t \fun ent $ %
\end{block}
\item \textbf{end} \\
\end{block}