diff options
Diffstat (limited to 'proof.tex')
| -rw-r--r-- | proof.tex | 2 |
1 files changed, 1 insertions, 1 deletions
@@ -33,7 +33,7 @@ As HTL is quite different to 3AC, this first translation is the most involved an \end{lemma} \begin{proof} - Follows by using a specification of the important properties $\yhfunction{tr\_htl}}$ which can be used as an assumption in the proof instead. The forward simulation is then proven by showing that the initial states and final states between the 3AC semantics and HTL semantics match, and then showing that the simulation diagram in Lemma~\ref{lemma:simulation_diagram} holds. + Follows by using a specification of the important properties $\yhfunction{tr\_htl}$ which can be used as an assumption in the proof instead. The forward simulation is then proven by showing that the initial states and final states between the 3AC semantics and HTL semantics match, and then showing that the simulation diagram in Lemma~\ref{lemma:simulation_diagram} holds. \end{proof} \subsubsection{Specification}\label{sec:proof:3ac_htl:specification} |