 Timestamp:
 Feb 6, 2013, 10:19:52 PM (8 years ago)
 File:

 1 edited
Legend:
 Unmodified
 Added
 Removed

Papers/itp2013/ccexec.tex
r2629 r2630 1035 1035 there is a $\texttt{trace\_any\_label}~b~s_1~s_1'$ called $tal_1$ and 1036 1036 $s_1 \mathcal{S} s_2$ 1037 \begin{ enumerate}1037 \begin{itemize} 1038 1038 \item if $b$ (the trace ends with a return) then there exists $s_{2_m},s_2'$ 1039 1039 and a trace $\texttt{trace\_any\_label}~b~s_2~s_{2_m}$ called $tal_2$ and a … … 1049 1049 or $s_1' (\mathcal{S} \cap \mathcal{L}) s_2$ and 1050 1050 $\texttt{tal\_collapsable}~tal_1$ and $\lnot (\texttt{as\_costed}~s_1)$ 1051 \end{ enumerate}1051 \end{itemize} 1052 1052 \end{theorem} 1053 1053
Note: See TracChangeset
for help on using the changeset viewer.