\begin{tabbing}
val{-}axiom($E$;$V$;$M$;${\it info}$;${\it pred?}$;
\\[0ex]${\it init}$;${\it Trans}$;
\\[0ex]${\it Choose}$;${\it Send}$;${\it val}$;${\it time}$)
\\[0ex]$\,\equiv$$_{\mbox{\scriptsize def}}$$\;\;$\=($\forall$$e$:$E$. \+
\\[0ex]($\uparrow$islocal(kind($e$)))
\\[0ex]$\Rightarrow$ ($\exists$\=$x$:$\mathbb{N}$\+
\\[0ex](($\uparrow$isl(${\it Choose}$(loc($e$),act(kind($e$)),$x$,$\lambda$$x$.state\_when($e$)($x$,0))))
\\[0ex]c$\wedge$ (${\it val}$($e$) = outl(${\it Choose}$(loc($e$),act(kind($e$)),$x$,$\lambda$$x$.state\_when($e$)($x$,0)))))))
\-\\[0ex]$\wedge$ \=($\forall$$e$:$E$. \+
\\[0ex]($\uparrow$isrcv(kind($e$)))
\\[0ex]$\Rightarrow$ ($<$lnk(kind($e$)), tag(kind($e$)), ${\it val}$($e$)$>$ $\in$ \=${\it Send}$\+
\\[0ex](loc(sender($e$))
\\[0ex],kind(sender($e$))
\\[0ex],${\it val}$(sender($e$))
\\[0ex],$\lambda$$x$.state\_when(sender($e$))($x$,0))))
\-\-\-
\end{tabbing}