# Changeset 973 for src/ASM/CPP2011/cpp-2011.tex

Ignore:
Timestamp:
Jun 16, 2011, 10:05:46 AM (9 years ago)
Message:

work from yesterday that could not be committed

File:
1 edited

### Legend:

Unmodified
 r970 This is done with the following function: \begin{lstlisting} definition next_internal_pseudo_address_map0: definition next_internal_pseudo_address_map: internal_pseudo_address_map $\rightarrow$ PseudoStatus $\rightarrow$ option internal_pseudo_address_map \end{lstlisting} \end{lstlisting} The statement can be given an intuitive reading as follows. Suppose our \texttt{PseudoStatus} $ps$ can be successfully converted into a \texttt{Status} $s$. Suppose further that, after executing a single assembly instruction and converting the resulting \texttt{PseudoStatus} into a \texttt{Status}, we obtain $s''$, being careful to track the number of ticks executed. Then, there exists some number $n$, so that executing $n$ machine code instructions in \texttt{Status} $s$ gives us \texttt{Status} $s''$. % ---------------------------------------------------------------------------- %