Changeset 2629

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

...

File:
1 edited

Legend:

Unmodified
 r2628 \begin{enumerate} \item if $b$ (the trace ends with a return) then there exists $s_{2_m},s_2'$ and a $\texttt{trace\_any\_label}~b~s_2~s_{2_m}$ called $tal_2$ and a and a trace $\texttt{trace\_any\_label}~b~s_2~s_{2_m}$ called $tal_2$ and a $\texttt{trace\_any\_any\_free}~s_{2_m}~s_2'$ called $taa_2$ s.t. $s_1' (\mathcal{S} \cap \mathcal{L}) s_2'$ and