\begin{tabbing}
val{-}axiom(\=$E$;$V$;$M$;${\it info}$;${\it pred?}$;\+
\\[0ex]${\it init}$;${\it Trans}$;${\it Choose}$;
\\[0ex]${\it Send}$;${\it val}$)
\-\\[0ex]$\,\equiv$$_{\mbox{\scriptsize def}}$$\;\;$\=(\=$\forall$$e$:$E$.\+\+
\\[0ex]islocal(kind($e$))
\\[0ex]$\Rightarrow$ \=isl(${\it Choose}$(loc($e$),act(kind($e$)),state\_when($e$)))\+
\\[0ex]\& ${\it val}$($e$) $=$ outl(${\it Choose}$(loc($e$),act(kind($e$)),state\_when($e$))))
\-\-\\[0ex]\& (\=$\forall$$e$:$E$.\+
\\[0ex]isrcv(kind($e$))
\\[0ex]$\Rightarrow$ ($\langle$lnk(kind($e$))$,\,$tag(kind($e$))$,\,$(${\it val}$($e$))$\rangle$ $\in$ \=${\it Send}$\+
\\[0ex](loc(sender($e$))
\\[0ex],kind(sender($e$))
\\[0ex],${\it val}$(sender($e$))
\\[0ex],state\_when(sender($e$)))))
\-\-\-
\end{tabbing}