Changeset 2630 for Papers/itp-2013


Ignore:
Timestamp:
Feb 6, 2013, 10:19:52 PM (7 years ago)
Author:
sacerdot
Message:

...

File:
1 edited

Legend:

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

    r2629 r2630  
    10351035there is a $\texttt{trace\_any\_label}~b~s_1~s_1'$ called $tal_1$ and
    10361036$s_1 \mathcal{S} s_2$
    1037 \begin{enumerate}
     1037\begin{itemize}
    10381038 \item if $b$ (the trace ends with a return) then there exists $s_{2_m},s_2'$
    10391039   and a trace $\texttt{trace\_any\_label}~b~s_2~s_{2_m}$ called $tal_2$ and a
     
    10491049   or $s_1' (\mathcal{S} \cap \mathcal{L}) s_2$ and
    10501050   $\texttt{tal\_collapsable}~tal_1$ and $\lnot (\texttt{as\_costed}~s_1)$
    1051 \end{enumerate}
     1051\end{itemize}
    10521052\end{theorem}
    10531053
Note: See TracChangeset for help on using the changeset viewer.