Changeset 2628 for Papers


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

...

File:
1 edited

Legend:

Unmodified
Added
Removed
  • Papers/itp-2013/ccexec.tex

    r2627 r2628  
    10141014\begin{theorem}[\texttt{status\_simulation\_produce\_tll}]
    10151015For 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 a
     1016there is a $\texttt{trace\_label\_label}~b~s_1~s_1'$ called $tll_1$ and a
    10171017$\texttt{trace\_any\_any}~s_{2_b}~s_2$ and $s_1 \mathcal{L} s_{2_b}$ and
    10181018$s_1 \mathcal{S} s_2$, there exists $s_{2_m},s_2'$ s.t.
     
    10311031\end{itemize}
    10321032\end{theorem}
    1033 
     1033\begin{theorem}[\texttt{status\_simulation\_produce\_tal}]
     1034For every $s_1,s_1',s_2$ s.t.
     1035there 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}
    10341055\begin{corollary}
    10351056For every $s_1,s_1',s_2$ s.t.
     
    10441065$s_1' \mathcal{R} s_{2_m}$.
    10451066\end{corollary}
     1067\end{comment}
    10461068
    10471069\begin{comment}
Note: See TracChangeset for help on using the changeset viewer.