# Changeset 2630

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

...

File:
1 edited

### Legend:

Unmodified
 r2629 there is a $\texttt{trace\_any\_label}~b~s_1~s_1'$ called $tal_1$ and $s_1 \mathcal{S} s_2$ \begin{enumerate} \begin{itemize} \item if $b$ (the trace ends with a return) then there exists $s_{2_m},s_2'$ and a trace $\texttt{trace\_any\_label}~b~s_2~s_{2_m}$ called $tal_2$ and a 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{itemize} \end{theorem}