diff --git a/draft/draft.tex b/draft/draft.tex index dda38ba..840297e 100644 --- a/draft/draft.tex +++ b/draft/draft.tex @@ -1943,6 +1943,9 @@ Since $\subseteq$ is a liftable order, we have the following lemma. The liftabil \end{gather*} Since $\powf p_1\comp\sigma=\alpha\comp p_1$ by precomposing $s$ to the both sides of the equation we get $\powf p_2\comp(\powf s\comp\sigma\comp s)=\alpha\comp p_2$. So, $\sigma\join(\powf s\comp\sigma\comp s)$ is a witness for $R$ to be a bisimulation.\qed \end{proof} +\begin{cor} + Considering~\autoref{lem:alph-prod}, assuming that $R$ is a symmetric relation and it is an AM simulation, then $R$ is an AM bisimulation as well. +\end{cor} \section{Relators} \subsection{Two-way similarity in Hughes-Jacobs}