# Changeset 2628

Ignore:
Timestamp:
Feb 6, 2013, 10:18:25 PM (6 years ago)
Message:

...

File:
1 edited

### Legend:

Unmodified
 r2627 \begin{theorem}[\texttt{status\_simulation\_produce\_tll}] For every $s_1,s_1',s_{2_b},s_2$ s.t. there is a $\texttt{trace\_label\_label}~f~s_1~s_1'$ called $tll_1$ and a there is a $\texttt{trace\_label\_label}~b~s_1~s_1'$ called $tll_1$ and a $\texttt{trace\_any\_any}~s_{2_b}~s_2$ and $s_1 \mathcal{L} s_{2_b}$ and $s_1 \mathcal{S} s_2$, there exists $s_{2_m},s_2'$ s.t. \end{itemize} \end{theorem} \begin{theorem}[\texttt{status\_simulation\_produce\_tal}] For every $s_1,s_1',s_2$ s.t. there is a $\texttt{trace\_any\_label}~b~s_1~s_1'$ called $tal_1$ and $s_1 \mathcal{S} s_2$ \begin{enumerate} \item if $b$ (the trace ends with a return) then there exists $s_{2_m},s_2'$ and a $\texttt{trace\_any\_label}~b~s_2~s_{2_m}$ called $tal_2$ and a $\texttt{trace\_any\_any\_free}~s_{2_m}~s_2'$ called $taa_2$ s.t. $s_1' (\mathcal{S} \cap \mathcal{L}) s_2'$ and $s_1' \mathcal{R} s_{2_m}$ and $\texttt{tal\_rel}~tal_1~tal_2$ and if $taa_2$ is non empty then $\lnot (\texttt{as\_costed}~s_{2_m})$ \item else there exists $s_2'$ and a $\texttt{trace\_any\_label}~b~s_2~s_2'$ called $tal_2$ such that either $s_1' (\mathcal{S} \cap \mathcal{L}) s_2'$ and $\texttt{tal\_rel}~tal_1~tal_2$ or $s_1' (\mathcal{S} \cap \mathcal{L}) s_2$ and $\texttt{tal\_collapsable}~tal_1$ and $\lnot (\texttt{as\_costed}~s_1)$ \end{enumerate} \end{theorem} \begin{comment} \begin{corollary} For every $s_1,s_1',s_2$ s.t. $s_1' \mathcal{R} s_{2_m}$. \end{corollary} \end{comment} \begin{comment}