pouya/coalgebraic-simulation
1
0
Fork 0
Code Issues Pull Requests Releases Wiki Activity

cor

Browse Source
This commit is contained in:
Pouya
2026-06-14 00:11:10 +01:00
parent 720a02a87f
commit c5e0e21128
1 changed files with 3 additions and 0 deletions
Download Patch File Download Diff File Expand all files Collapse all files
draft/draft.tex
+3
View File
@@ -1943,6 +1943,9 @@ Since $\subseteq$ is a liftable order, we have the following lemma. The liftabil
\end{gather*} \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 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} \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} \section{Relators}
\subsection{Two-way similarity in Hughes-Jacobs} \subsection{Two-way similarity in Hughes-Jacobs}