Add simulation diagram

1 files changed, 2 insertions, 2 deletions

diff --git a/proof.tex b/proof.tex
index a5ccb44..4c0359e 100644
--- a/proof.tex
+++ b/proof.tex
@@ -71,11 +71,11 @@ Using the \texttt{match\_states}, we can then define the correctness theorem for
       \node[circle] (r1) at (6,1.5) {$\Gamma_{r}, \Gamma_{a}, \Gamma_{r}!\sigma$};
       \node[circle] (s2) at (0,0) {$R', M', \textit{pc}'$};
       \node[circle] (r2) at (6,0) {$\Gamma_{r}', \Gamma_{a}', \Gamma_{r}'!\sigma$};
-      \node at (6.3,3) {+};
+      \node at (6.3,0.75) {+};
       \draw (s1) -- node[above] {$R \le \Gamma_{r} \land M \le \Gamma_{a} \land \textit{pc} = \Gamma_{r}!\sigma$} ++ (r1);
       \draw[-{Latex}] ($(s1.south) + (0,0.3)$) -- ($(s2.north) - (0,0.3)$);
       \draw[-{Latex},dashed] ($(r1.south) + (0,0.4)$) -- ($(r2.north) - (0,0.4)$);
-      \draw[dashed] (s2) -- node[above] {\textasciitilde{}} node[below] {\small\texttt{match\_states}} ++ (r2);
+      \draw[dashed] (s2) -- node[above] {$R' \le \Gamma_{r}' \land M' \le \Gamma_{a}' \land \textit{pc}' = \Gamma_{r}'!\sigma$} ++ (r2);
     \end{scope}
   \end{tikzpicture}
 \end{center}