Changeset 2628
 Timestamp:
 Feb 6, 2013, 10:18:25 PM (6 years ago)
 File:

 1 edited
Legend:
 Unmodified
 Added
 Removed

Papers/itp2013/ccexec.tex
r2627 r2628 1014 1014 \begin{theorem}[\texttt{status\_simulation\_produce\_tll}] 1015 1015 For every $s_1,s_1',s_{2_b},s_2$ s.t. 1016 there is a $\texttt{trace\_label\_label}~ f~s_1~s_1'$ called $tll_1$ and a1016 there is a $\texttt{trace\_label\_label}~b~s_1~s_1'$ called $tll_1$ and a 1017 1017 $\texttt{trace\_any\_any}~s_{2_b}~s_2$ and $s_1 \mathcal{L} s_{2_b}$ and 1018 1018 $s_1 \mathcal{S} s_2$, there exists $s_{2_m},s_2'$ s.t. … … 1031 1031 \end{itemize} 1032 1032 \end{theorem} 1033 1033 \begin{theorem}[\texttt{status\_simulation\_produce\_tal}] 1034 For every $s_1,s_1',s_2$ s.t. 1035 there is a $\texttt{trace\_any\_label}~b~s_1~s_1'$ called $tal_1$ and 1036 $s_1 \mathcal{S} s_2$ 1037 \begin{enumerate} 1038 \item if $b$ (the trace ends with a return) then there exists $s_{2_m},s_2'$ 1039 and a $\texttt{trace\_any\_label}~b~s_2~s_{2_m}$ called $tal_2$ and a 1040 $\texttt{trace\_any\_any\_free}~s_{2_m}~s_2'$ called $taa_2$ s.t. 1041 $s_1' (\mathcal{S} \cap \mathcal{L}) s_2'$ and 1042 $s_1' \mathcal{R} s_{2_m}$ and 1043 $\texttt{tal\_rel}~tal_1~tal_2$ and 1044 if $taa_2$ is non empty then $\lnot (\texttt{as\_costed}~s_{2_m})$ 1045 \item else there exists $s_2'$ and a 1046 $\texttt{trace\_any\_label}~b~s_2~s_2'$ called $tal_2$ such that 1047 either $s_1' (\mathcal{S} \cap \mathcal{L}) s_2'$ and 1048 $\texttt{tal\_rel}~tal_1~tal_2$ 1049 or $s_1' (\mathcal{S} \cap \mathcal{L}) s_2$ and 1050 $\texttt{tal\_collapsable}~tal_1$ and $\lnot (\texttt{as\_costed}~s_1)$ 1051 \end{enumerate} 1052 \end{theorem} 1053 1054 \begin{comment} 1034 1055 \begin{corollary} 1035 1056 For every $s_1,s_1',s_2$ s.t. … … 1044 1065 $s_1' \mathcal{R} s_{2_m}$. 1045 1066 \end{corollary} 1067 \end{comment} 1046 1068 1047 1069 \begin{comment}
Note: See TracChangeset
for help on using the changeset viewer.