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

counter-example

Browse Source
This commit is contained in:
partowp 2026-05-03 19:47:03 +01:00
parent d572b575d3
commit ed01ebf5bf
1 changed files with 134 additions and 116 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

250
draft/draft.tex
View File

@ -289,6 +289,7 @@
\newcommand{\obj}{\mathbf{Obj}} \newcommand{\obj}{\mathbf{Obj}}
\newcommand{\relar}{\mathbf{R}} \newcommand{\relar}{\mathbf{R}}
\newcommand{\rto}{\mathrel{\tikz{\draw[-{Stealth}] (0,0) -- (0.4,0); \draw (0.17,0.07) -- (0.17,-0.07);}}} \newcommand{\rto}{\mathrel{\tikz{\draw[-{Stealth}] (0,0) -- (0.4,0); \draw (0.17,0.07) -- (0.17,-0.07);}}}
\newcommand{\powf}{\mathcal{P}}
\newcommand{\simeet}{% \newcommand{\simeet}{%
\mathbin{% \mathbin{%
@ -939,7 +940,7 @@ Lifting from $\BC$ to $\gra(\BC)$ is easy. For $F\c\BC\to\BC$ we define $F_\gra\
\arrow["{Fp_2}", from=1-2, to=2-3] \arrow["{Fp_2}", from=1-2, to=2-3]
\end{tikzcd} \end{tikzcd}
\end{equation*} \end{equation*}
This lifting does not work for $\rel$. As an example, if we set $F$ to be the powerset functor $\mathcal{P}$, then $(\mathcal{P}R,\mathcal{P}X)$ is not necessarily a relation anymore. For example, if we take $R=\{(1,0),(0,1),(0,0),(1,1)\}$, then taking $\{\{(1,0),(0,1),(0,0),(1,1)\}\}$ and $\{\{(1,0),(0,1),(0,0)\}\}$ as elements of $\mathcal{P}R$, the morphism $\brks{\mathcal{P}p_1,\mathcal{P}p_2}$ maps them both to $(\{0,1\},\{0,1\})$ so it is not monic. This lifting does not work for $\rel$. As an example, if we set $F$ to be the powerset functor $\powf$, then $(\powf R,\powf X)$ is not necessarily a relation anymore. For example, if we take $R=\{(1,0),(0,1),(0,0),(1,1)\}$, then taking $\{\{(1,0),(0,1),(0,0),(1,1)\}\}$ and $\{\{(1,0),(0,1),(0,0)\}\}$ as elements of $\powf R$, the morphism $\brks{\powf p_1,\powf p_2}$ maps them both to $(\{0,1\},\{0,1\})$ so it is not monic.
To cope with this, we assume the following epi-mono decomposition for $(R,X)\in\rel(\BC)$: To cope with this, we assume the following epi-mono decomposition for $(R,X)\in\rel(\BC)$:
\begin{equation*} \begin{equation*}
@ -1142,7 +1143,7 @@ Another avenue would be to give another definition for simulation that does not
Well! This counter example does not work! Because the described order $\appr$ does not satisfy the condition mentioned in Jacobs's paper. The condition is that the order on $FX$ should satisfy the property that for a morphism $f\c X\to Y$ the morphism $Ff\c FX\to FY$ preserves $\appr$. Probably, the only poset that has this property for $\mathbf{Id}$ is $\Delta$. If there is a counter-example, it is true for another functor. Well! This counter example does not work! Because the described order $\appr$ does not satisfy the condition mentioned in Jacobs's paper. The condition is that the order on $FX$ should satisfy the property that for a morphism $f\c X\to Y$ the morphism $Ff\c FX\to FY$ preserves $\appr$. Probably, the only poset that has this property for $\mathbf{Id}$ is $\Delta$. If there is a counter-example, it is true for another functor.
\begin{example} \begin{example}
Another counter-example! Assume that $F=\mathcal{P}$, and take $R=\{(1,2),(2,1),(1,3),(3,1)\}$, and $X=\{1,2,3\}$. $\alpha(x)=X$ for every $x\in X$, and $\sigma$ is defined as below: Another counter-example! Assume that $F=\powf $, and take $R=\{(1,2),(2,1),(1,3),(3,1)\}$, and $X=\{1,2,3\}$. $\alpha(x)=X$ for every $x\in X$, and $\sigma$ is defined as below:
\begin{gather*} \begin{gather*}
\sigma(w)= \sigma(w)=
\begin{cases} \begin{cases}
@ -1150,11 +1151,11 @@ Well! This counter example does not work! Because the described order $\appr$ do
R\setminus\{(1,2)\} & w=(1,3) R\setminus\{(1,2)\} & w=(1,3)
\end{cases} \end{cases}
\end{gather*} \end{gather*}
In this scenario, $\sigma$ is a simulation, but it is not a bisimulation. It is a simulation since for every $w\in R$ we have $(\mathcal{P}p_1(\sigma(w)))=X$, thus for every $x\in X$, $\alpha(x)=X\subseteq X$. Also, $\mathcal{P}p_2(\sigma(w))\subseteq \alpha(p_2(w))$ as $\alpha(p_2(w))=X$ for every $w\in R$. But it is not a bisimulation, since $\alpha\comp p_2(1,3)=\alpha(3)=X\neq(\mathcal{P}p_2)^\dagger(\sigma(1,3))=\{1,3\}$. In this scenario, $\sigma$ is a simulation, but it is not a bisimulation. It is a simulation since for every $w\in R$ we have $(\powf p_1(\sigma(w)))=X$, thus for every $x\in X$, $\alpha(x)=X\subseteq X$. Also, $\powf p_2(\sigma(w))\subseteq \alpha(p_2(w))$ as $\alpha(p_2(w))=X$ for every $w\in R$. But it is not a bisimulation, since $\alpha\comp p_2(1,3)=\alpha(3)=X\neq(\powf p_2)^\dagger(\sigma(1,3))=\{1,3\}$.
\end{example} \end{example}
% %
\begin{example} \begin{example}
And another counter-example!!! Assume that $F=\mathcal{P}$, and take $R=X\times X\setminus\{(1,3),(3,1)\}$, and $X=\{1,2,3\}$. $\alpha$ is defined as below: And another counter-example!!! Assume that $F=\powf $, and take $R=X\times X\setminus\{(1,3),(3,1)\}$, and $X=\{1,2,3\}$. $\alpha$ is defined as below:
\begin{gather*} \begin{gather*}
\alpha(x)= \alpha(x)=
\begin{cases} \begin{cases}
@ -1176,7 +1177,7 @@ Well! This counter example does not work! Because the described order $\appr$ do
\end{cases} \end{cases}
\end{gather*} \end{gather*}
\begin{gather*} \begin{gather*}
(\mathcal{P}p_1)^\dagger\comp\sigma_1(w)= (\powf p_1)^\dagger\comp\sigma_1(w)=
\begin{cases} \begin{cases}
\{1,2\} & w=(1,2) \\ \{1,2\} & w=(1,2) \\
\{2,3\} & w=(2,1) \\ \{2,3\} & w=(2,1) \\
@ -1185,7 +1186,7 @@ Well! This counter example does not work! Because the described order $\appr$ do
\{2,3\} & w=(2,3) \\ \{2,3\} & w=(2,3) \\
\{3\} & w=(3,3) \{3\} & w=(3,3)
\end{cases} \end{cases}
(\mathcal{P}p_2)^\dagger\comp\sigma_1(w)= (\powf p_2)^\dagger\comp\sigma_1(w)=
\begin{cases} \begin{cases}
\{2\} & w=(1,2) \\ \{2\} & w=(1,2) \\
\{1,2\} & w=(2,1) \\ \{1,2\} & w=(2,1) \\
@ -1208,7 +1209,7 @@ Well! This counter example does not work! Because the described order $\appr$ do
\end{cases} \end{cases}
\end{gather*} \end{gather*}
\begin{gather*} \begin{gather*}
(\mathcal{P}p_1)^\dagger\comp\sigma'_1(w)= (\powf p_1)^\dagger\comp\sigma'_1(w)=
\begin{cases} \begin{cases}
\{1,2\} & w=(1,2) \\ \{1,2\} & w=(1,2) \\
\{2,3\} & w=(2,1) \\ \{2,3\} & w=(2,1) \\
@ -1218,7 +1219,7 @@ Well! This counter example does not work! Because the described order $\appr$ do
\{2,3\} & w=(2,3) \\ \{2,3\} & w=(2,3) \\
\{3\} & w=(3,3) \{3\} & w=(3,3)
\end{cases} \end{cases}
(\mathcal{P}p_2)^\dagger\comp\sigma'_1(w)= (\powf p_2)^\dagger\comp\sigma'_1(w)=
\begin{cases} \begin{cases}
\{2,3\} & w=(1,2) \\ \{2,3\} & w=(1,2) \\
\{1,2\} & w=(2,1) \\ \{1,2\} & w=(2,1) \\
@ -1249,7 +1250,7 @@ Well! This counter example does not work! Because the described order $\appr$ do
\beta=\sigma'_1 \beta=\sigma'_1
\end{gather*} \end{gather*}
\begin{gather*} \begin{gather*}
(\mathcal{P}s)^\dagger\comp\sigma_1\comp s(w)= (\powf s)^\dagger\comp\sigma_1\comp s(w)=
\begin{cases} \begin{cases}
\{(1,2),(2,3)\} & w=(1,2) \\ \{(1,2),(2,3)\} & w=(1,2) \\
\{(2,1),(2,2)\} & w=(2,1) \\ \{(2,1),(2,2)\} & w=(2,1) \\
@ -1261,7 +1262,7 @@ Well! This counter example does not work! Because the described order $\appr$ do
\end{cases} \end{cases}
\end{gather*} \end{gather*}
\begin{gather*} \begin{gather*}
(\mathcal{P}p_1)^\dagger\comp(\mathcal{P}s)^\dagger\comp\sigma_1\comp s(w)= (\powf p_1)^\dagger\comp(\powf s)^\dagger\comp\sigma_1\comp s(w)=
\begin{cases} \begin{cases}
\{1,2\} & w=(1,2) \\ \{1,2\} & w=(1,2) \\
\{2\} & w=(2,1) \\ \{2\} & w=(2,1) \\
@ -1271,7 +1272,7 @@ Well! This counter example does not work! Because the described order $\appr$ do
\{2,3\} & w=(2,3) \\ \{2,3\} & w=(2,3) \\
\{3\} & w=(3,3) \{3\} & w=(3,3)
\end{cases} \end{cases}
(\mathcal{P}p_2)^\dagger\comp(\mathcal{P}s)^\dagger\comp\sigma_1\comp s(w)= (\powf p_2)^\dagger\comp(\powf s)^\dagger\comp\sigma_1\comp s(w)=
\begin{cases} \begin{cases}
\{2,3\} & w=(1,2) \\ \{2,3\} & w=(1,2) \\
\{1,2\} & w=(2,1) \\ \{1,2\} & w=(2,1) \\
@ -1282,7 +1283,7 @@ Well! This counter example does not work! Because the described order $\appr$ do
\{3\} & w=(3,3) \{3\} & w=(3,3)
\end{cases} \end{cases}
\end{gather*} \end{gather*}
In this scenario, $\sigma_1$ is a simulation, but it is not a bisimulation. $\sigma'_1$, $\sigma''_1$ and $(\mathcal{P}s)^\dagger\comp\sigma_1\comp s$ are neither. We can not make $\sigma_1$ bigger here to make it a bisimulation as $\alpha\comp p_1(3,2)=\{3\}\subsetneq\{2,3\}=(\mathcal{P}p_1)^\dagger\comp\sigma_1(3,2)$. In this scenario, $\sigma_1$ is a simulation, but it is not a bisimulation. $\sigma'_1$, $\sigma''_1$ and $(\powf s)^\dagger\comp\sigma_1\comp s$ are neither. We can not make $\sigma_1$ bigger here to make it a bisimulation as $\alpha\comp p_1(3,2)=\{3\}\subsetneq\{2,3\}=(\powf p_1)^\dagger\comp\sigma_1(3,2)$.
The following is also a simulation and not a bisimulation: The following is also a simulation and not a bisimulation:
\begin{gather*} \begin{gather*}
@ -1297,7 +1298,7 @@ Well! This counter example does not work! Because the described order $\appr$ do
\end{cases} \end{cases}
\end{gather*} \end{gather*}
\begin{gather*} \begin{gather*}
(\mathcal{P}p_1)^\dagger\comp\sigma_2(w)= (\powf p_1)^\dagger\comp\sigma_2(w)=
\begin{cases} \begin{cases}
\{1,2\} & w=(1,2) \\ \{1,2\} & w=(1,2) \\
\{2,3\} & w=(2,1) \\ \{2,3\} & w=(2,1) \\
@ -1306,7 +1307,7 @@ Well! This counter example does not work! Because the described order $\appr$ do
\{2,3\} & w=(2,3) \\ \{2,3\} & w=(2,3) \\
\{3\} & w\in\{(3,2),(3,3)\} \{3\} & w\in\{(3,2),(3,3)\}
\end{cases} \end{cases}
(\mathcal{P}p_2)^\dagger\comp\sigma_2(w)= (\powf p_2)^\dagger\comp\sigma_2(w)=
\begin{cases} \begin{cases}
\{2\} & w=(1,2) \\ \{2\} & w=(1,2) \\
\{1,2\} & w=(2,1) \\ \{1,2\} & w=(2,1) \\
@ -1329,7 +1330,7 @@ Well! This counter example does not work! Because the described order $\appr$ do
\end{cases} \end{cases}
\end{gather*} \end{gather*}
\begin{gather*} \begin{gather*}
(\mathcal{P}p_1)^\dagger\comp\sigma'_2(w)= (\powf p_1)^\dagger\comp\sigma'_2(w)=
\begin{cases} \begin{cases}
\{1,2\} & w=(1,2) \\ \{1,2\} & w=(1,2) \\
\{2,3\} & w=(2,1) \\ \{2,3\} & w=(2,1) \\
@ -1339,7 +1340,7 @@ Well! This counter example does not work! Because the described order $\appr$ do
\{2,3\} & w=(2,3) \\ \{2,3\} & w=(2,3) \\
\{3\} & w=(3,3) \{3\} & w=(3,3)
\end{cases} \end{cases}
(\mathcal{P}p_2)^\dagger\comp\sigma'_2(w)= (\powf p_2)^\dagger\comp\sigma'_2(w)=
\begin{cases} \begin{cases}
\{2,3\} & w=(1,2) \\ \{2,3\} & w=(1,2) \\
\{1,2\} & w=(2,1) \\ \{1,2\} & w=(2,1) \\
@ -1351,7 +1352,7 @@ Well! This counter example does not work! Because the described order $\appr$ do
\end{cases} \end{cases}
\end{gather*} \end{gather*}
\begin{gather*} \begin{gather*}
(\mathcal{P}s)^\dagger\comp\sigma_2\comp s(w)= (\powf s)^\dagger\comp\sigma_2\comp s(w)=
\begin{cases} \begin{cases}
\{(1,2),(2,3)\} & w=(1,2) \\ \{(1,2),(2,3)\} & w=(1,2) \\
\{(2,1),(2,2)\} & w=(2,1) \\ \{(2,1),(2,2)\} & w=(2,1) \\
@ -1363,7 +1364,7 @@ Well! This counter example does not work! Because the described order $\appr$ do
\end{cases} \end{cases}
\end{gather*} \end{gather*}
\begin{gather*} \begin{gather*}
(\mathcal{P}p_1)^\dagger\comp(\mathcal{P}s)^\dagger\comp\sigma_2\comp s(w)= (\powf p_1)^\dagger\comp(\powf s)^\dagger\comp\sigma_2\comp s(w)=
\begin{cases} \begin{cases}
\{1,2\} & w=(1,2) \\ \{1,2\} & w=(1,2) \\
\{2\} & w=(2,1) \\ \{2\} & w=(2,1) \\
@ -1373,7 +1374,7 @@ Well! This counter example does not work! Because the described order $\appr$ do
\{2\} & w=(2,3) \\ \{2\} & w=(2,3) \\
\{3\} & w=(3,3) \{3\} & w=(3,3)
\end{cases} \end{cases}
(\mathcal{P}p_2)^\dagger\comp(\mathcal{P}s)^\dagger\comp\sigma_2\comp s(w)= (\powf p_2)^\dagger\comp(\powf s)^\dagger\comp\sigma_2\comp s(w)=
\begin{cases} \begin{cases}
\{2,3\} & w=(1,2) \\ \{2,3\} & w=(1,2) \\
\{1,2\} & w=(2,1) \\ \{1,2\} & w=(2,1) \\
@ -1384,7 +1385,7 @@ Well! This counter example does not work! Because the described order $\appr$ do
\{3\} & w=(3,3) \{3\} & w=(3,3)
\end{cases} \end{cases}
\end{gather*} \end{gather*}
$\sigma_2$ is a simulation, $\sigma'_2$ is a bisimulation, and $(\mathcal{P}s)^\dagger\comp\sigma_2\comp s$ is neither. $\sigma_2$ is a simulation, $\sigma'_2$ is a bisimulation, and $(\powf s)^\dagger\comp\sigma_2\comp s$ is neither.
The following is both a simulation and a bisimulation: The following is both a simulation and a bisimulation:
\begin{gather*} \begin{gather*}
\sigma_3(w)= \sigma_3(w)=
@ -1399,7 +1400,7 @@ Well! This counter example does not work! Because the described order $\appr$ do
\end{cases} \end{cases}
\end{gather*} \end{gather*}
\begin{gather*} \begin{gather*}
(\mathcal{P}p_1)^\dagger\comp\sigma_3(w)= (\powf p_1)^\dagger\comp\sigma_3(w)=
\begin{cases} \begin{cases}
\{1,2\} & w=(1,2) \\ \{1,2\} & w=(1,2) \\
\{2,3\} & w=(2,1) \\ \{2,3\} & w=(2,1) \\
@ -1409,7 +1410,7 @@ Well! This counter example does not work! Because the described order $\appr$ do
\{3\} & w=(3,2) \\ \{3\} & w=(3,2) \\
\{3\} & w=(3,3) \{3\} & w=(3,3)
\end{cases} \end{cases}
(\mathcal{P}p_2)^\dagger\comp\sigma_3(w)= (\powf p_2)^\dagger\comp\sigma_3(w)=
\begin{cases} \begin{cases}
\{2,3\} & w=(1,2) \\ \{2,3\} & w=(1,2) \\
\{1,2\} & w=(2,1) \\ \{1,2\} & w=(2,1) \\
@ -1434,7 +1435,7 @@ Well! This counter example does not work! Because the described order $\appr$ do
\end{cases} \end{cases}
\end{gather*} \end{gather*}
\begin{gather*} \begin{gather*}
(\mathcal{P}p_1)^\dagger\comp\sigma_4(w)= (\powf p_1)^\dagger\comp\sigma_4(w)=
\begin{cases} \begin{cases}
\{1,2,3\} & w=(1,2) \\ \{1,2,3\} & w=(1,2) \\
\{1,2,3\} & w=(2,1) \\ \{1,2,3\} & w=(2,1) \\
@ -1444,7 +1445,7 @@ Well! This counter example does not work! Because the described order $\appr$ do
\{1,2,3\} & w=(3,2) \\ \{1,2,3\} & w=(3,2) \\
\{3\} & w=(3,3) \{3\} & w=(3,3)
\end{cases} \end{cases}
(\mathcal{P}p_2)^\dagger\comp\sigma_4(w)= (\powf p_2)^\dagger\comp\sigma_4(w)=
\begin{cases} \begin{cases}
\{2,3\} & w=(1,2) \\ \{2,3\} & w=(1,2) \\
\{1,2\} & w=(2,1) \\ \{1,2\} & w=(2,1) \\
@ -1468,7 +1469,7 @@ Well! This counter example does not work! Because the described order $\appr$ do
\end{cases} \end{cases}
\end{gather*} \end{gather*}
\begin{gather*} \begin{gather*}
(\mathcal{P}p_1)^\dagger\comp\sigma''_4(w)= (\powf p_1)^\dagger\comp\sigma''_4(w)=
\begin{cases} \begin{cases}
\{1,2\} & w=(1,2) \\ \{1,2\} & w=(1,2) \\
\{2,3\} & w=(2,1) \\ \{2,3\} & w=(2,1) \\
@ -1478,7 +1479,7 @@ Well! This counter example does not work! Because the described order $\appr$ do
\{3\} & w=(3,2) \\ \{3\} & w=(3,2) \\
\{3\} & w=(3,3) \{3\} & w=(3,3)
\end{cases} \end{cases}
(\mathcal{P}p_2)^\dagger\comp\sigma''_4(w)= (\powf p_2)^\dagger\comp\sigma''_4(w)=
\begin{cases} \begin{cases}
\{2,3\} & w=(1,2) \\ \{2,3\} & w=(1,2) \\
\{1,2\} & w=(2,1) \\ \{1,2\} & w=(2,1) \\
@ -1490,7 +1491,7 @@ Well! This counter example does not work! Because the described order $\appr$ do
\end{cases} \end{cases}
\end{gather*} \end{gather*}
\begin{gather*} \begin{gather*}
(\mathcal{P}s)^\dagger\comp\sigma_4\comp s(w)= (\powf s)^\dagger\comp\sigma_4\comp s(w)=
\begin{cases} \begin{cases}
\{(1,1),(1,2),(2,1),(2,2),(2,3)\} & w=(1,2) \\ \{(1,1),(1,2),(2,1),(2,2),(2,3)\} & w=(1,2) \\
\{(2,1),(2,2),(2,3),(3,2),(3,3)\} & w=(2,1) \\ \{(2,1),(2,2),(2,3),(3,2),(3,3)\} & w=(2,1) \\
@ -1502,7 +1503,7 @@ Well! This counter example does not work! Because the described order $\appr$ do
\end{cases} \end{cases}
\end{gather*} \end{gather*}
\begin{gather*} \begin{gather*}
(\mathcal{P}p_1)^\dagger\comp(\mathcal{P}s)^\dagger\comp\sigma_4\comp s(w)= (\powf p_1)^\dagger\comp(\powf s)^\dagger\comp\sigma_4\comp s(w)=
\begin{cases} \begin{cases}
\{1,2\} & w=(1,2) \\ \{1,2\} & w=(1,2) \\
\{2,3\} & w=(2,1) \\ \{2,3\} & w=(2,1) \\
@ -1512,7 +1513,7 @@ Well! This counter example does not work! Because the described order $\appr$ do
\{3\} & w=(3,2) \\ \{3\} & w=(3,2) \\
\{3\} & w=(3,3) \{3\} & w=(3,3)
\end{cases} \end{cases}
(\mathcal{P}p_2)^\dagger\comp(\mathcal{P}s)^\dagger\comp\sigma_4\comp s(w)= (\powf p_2)^\dagger\comp(\powf s)^\dagger\comp\sigma_4\comp s(w)=
\begin{cases} \begin{cases}
\{1,2,3\} & w=(1,2) \\ \{1,2,3\} & w=(1,2) \\
\{1,2,3\} & w=(2,1) \\ \{1,2,3\} & w=(2,1) \\
@ -1523,7 +1524,7 @@ Well! This counter example does not work! Because the described order $\appr$ do
\{3\} & w=(3,3) \{3\} & w=(3,3)
\end{cases} \end{cases}
\end{gather*} \end{gather*}
$\sigma_4$ is a simulation, $\sigma''_4$ is a bisimulation, and $(\mathcal{P}s)^\dagger\comp\sigma_4\comp s$ is neither. $\sigma_4$ is a simulation, $\sigma''_4$ is a bisimulation, and $(\powf s)^\dagger\comp\sigma_4\comp s$ is neither.
The following is also a simulation and not a bisimulation: The following is also a simulation and not a bisimulation:
\begin{gather*} \begin{gather*}
@ -1539,7 +1540,7 @@ Well! This counter example does not work! Because the described order $\appr$ do
\end{cases} \end{cases}
\end{gather*} \end{gather*}
\begin{gather*} \begin{gather*}
(\mathcal{P}p_1)^\dagger\comp\sigma_5(w)= (\powf p_1)^\dagger\comp\sigma_5(w)=
\begin{cases} \begin{cases}
\{1,2\} & w=(1,2) \\ \{1,2\} & w=(1,2) \\
\{2,3\} & w=(2,1) \\ \{2,3\} & w=(2,1) \\
@ -1549,7 +1550,7 @@ Well! This counter example does not work! Because the described order $\appr$ do
\{3\} & w=(3,2) \\ \{3\} & w=(3,2) \\
\{3\} & w=(3,3) \{3\} & w=(3,3)
\end{cases} \end{cases}
(\mathcal{P}p_2)^\dagger\comp\sigma_5(w)= (\powf p_2)^\dagger\comp\sigma_5(w)=
\begin{cases} \begin{cases}
\{2\} & w=(1,2) \\ \{2\} & w=(1,2) \\
\{2\} & w=(2,1) \\ \{2\} & w=(2,1) \\
@ -1574,7 +1575,7 @@ Well! This counter example does not work! Because the described order $\appr$ do
\end{cases} \end{cases}
\end{gather*} \end{gather*}
\begin{gather*} \begin{gather*}
(\mathcal{P}p_1)^\dagger\comp\sigma_6(w)= (\powf p_1)^\dagger\comp\sigma_6(w)=
\begin{cases} \begin{cases}
\{1,2\} & w=(1,2) \\ \{1,2\} & w=(1,2) \\
\{2,3\} & w=(2,1) \\ \{2,3\} & w=(2,1) \\
@ -1584,7 +1585,7 @@ Well! This counter example does not work! Because the described order $\appr$ do
\{3\} & w=(3,2) \\ \{3\} & w=(3,2) \\
\{3\} & w=(3,3) \{3\} & w=(3,3)
\end{cases} \end{cases}
(\mathcal{P}p_2)^\dagger\comp\sigma_6(w)= (\powf p_2)^\dagger\comp\sigma_6(w)=
\begin{cases} \begin{cases}
\{2\} & w=(1,2) \\ \{2\} & w=(1,2) \\
\{1\} & w=(2,1) \\ \{1\} & w=(2,1) \\
@ -1602,10 +1603,10 @@ Well! This counter example does not work! Because the described order $\appr$ do
% %
If we define $\appr$ on simulations as If we define $\appr$ on simulations as
\begin{gather*} \begin{gather*}
\sigma_1\appr\sigma_2\iff \forall x_1,x_2\in X, (\mathcal{P}p_i)^\dagger\comp\sigma_1(x_1,x_2)\subseteq(\mathcal{P}p_i)^\dagger\comp\sigma_2(x_1,x_2) \sigma_1\appr\sigma_2\iff \forall x_1,x_2\in X, (\powf p_i)^\dagger\comp\sigma_1(x_1,x_2)\subseteq(\powf p_i)^\dagger\comp\sigma_2(x_1,x_2)
\end{gather*} \end{gather*}
\begin{lemma} \begin{lemma}
$(Hom(R,(\mathcal{P}R)^\dagger),\appr)$ is a poset. $(Hom(R,(\powf R)^\dagger),\appr)$ is a poset.
\end{lemma} \end{lemma}
\begin{proof} \begin{proof}
Reflexivity and transitivity are obvious. We need to prove anti-symmetry.\\ Reflexivity and transitivity are obvious. We need to prove anti-symmetry.\\
@ -1630,192 +1631,192 @@ We define $\join$ and $\meet$ on morphisms as follows:
\begin{gather*} \begin{gather*}
\forall x_1,x_2\in X,\\ \forall x_1,x_2\in X,\\
\sigma_1 \join \sigma_2 (x_1,x_2)= \sigma_1(x_1,x_2) \cup \sigma_2(x_1,x_2),\\ \sigma_1 \join \sigma_2 (x_1,x_2)= \sigma_1(x_1,x_2) \cup \sigma_2(x_1,x_2),\\
\sigma_1 \meet \sigma_2 (x_1,x_2)= (\mathcal{P}p_1)^\dagger\comp\sigma_1(x_1,x_2) \cap (\mathcal{P}p_1)^\dagger\comp\sigma_2(x_1,x_2)\times(\mathcal{P}p_2)^\dagger\comp\sigma_1(x_1,x_2) \cap (\mathcal{P}p_2)^\dagger\comp\sigma_2(x_1,x_2). \sigma_1 \meet \sigma_2 (x_1,x_2)= (\powf p_1)^\dagger\comp\sigma_1(x_1,x_2) \cap (\powf p_1)^\dagger\comp\sigma_2(x_1,x_2)\times(\powf p_2)^\dagger\comp\sigma_1(x_1,x_2) \cap (\powf p_2)^\dagger\comp\sigma_2(x_1,x_2).
\end{gather*} \end{gather*}
\end{definition} \end{definition}
\begin{lemma}\label{lem:proj-dist-set} \begin{lemma}\label{lem:proj-dist-set}
For relations $R_1$ and $R_2$ the following equation holds: For relations $R_1$ and $R_2$ the following equation holds:
\begin{gather*} \begin{gather*}
%(\mathcal{P}p_i)^\dagger(R_1\cup R_2)=(\mathcal{P}p_i)^\dagger(R_1)\cup(\mathcal{P}p_i)^\dagger(R_2) %(\powf p_i)^\dagger(R_1\cup R_2)=(\powf p_i)^\dagger(R_1)\cup(\powf p_i)^\dagger(R_2)
(\mathcal{P}p_i)(R_1\cup R_2)=(\mathcal{P}p_i)(R_1)\cup(\mathcal{P}p_i)(R_2) (\powf p_i)(R_1\cup R_2)=(\powf p_i)(R_1)\cup(\powf p_i)(R_2)
\end{gather*} \end{gather*}
\end{lemma} \end{lemma}
\begin{proof} \begin{proof}
We prove the lemma for the case that $i=1$. The proof is the same for $i=2$. We prove the lemma for the case that $i=1$. The proof is the same for $i=2$.
Assuming $x_1\in(\mathcal{P}p_1)^\dagger(R_1\cup R_2)$ then exists $x_2$ that $(x_1,x_2)\in R_1\cup R_2$, thus either $(x_1,x_2)\in R_1$ or $(x_1,x_2)\in R_2$, so we have $x_1\in(\mathcal{P}p_1)^\dagger(R_1)$ or $x_1\in(\mathcal{P}p_1)^\dagger(R_2)$, respectively. So, we have $x_1\in (\mathcal{P}p_1)^\dagger(R_1)\cup(\mathcal{P}p_1)^\dagger(R_2)$. Assuming $x_1\in(\powf p_1)^\dagger(R_1\cup R_2)$ then exists $x_2$ that $(x_1,x_2)\in R_1\cup R_2$, thus either $(x_1,x_2)\in R_1$ or $(x_1,x_2)\in R_2$, so we have $x_1\in(\powf p_1)^\dagger(R_1)$ or $x_1\in(\powf p_1)^\dagger(R_2)$, respectively. So, we have $x_1\in (\powf p_1)^\dagger(R_1)\cup(\powf p_1)^\dagger(R_2)$.
Now, assuming that $x_1\in(\mathcal{P}p_1)^\dagger(R_1)\cup(\mathcal{P}p_1)^\dagger(R_2)$ either $x_1\in(\mathcal{P}p_1)^\dagger(R_1)$ or $x_1\in(\mathcal{P}p_1)^\dagger(R_2)$. Without loss of generality, we can assume $x_1\in(\mathcal{P}p_1)^\dagger(R_j)$, where $j\in\{1,2\}$. Now, assuming that $x_1\in(\powf p_1)^\dagger(R_1)\cup(\powf p_1)^\dagger(R_2)$ either $x_1\in(\powf p_1)^\dagger(R_1)$ or $x_1\in(\powf p_1)^\dagger(R_2)$. Without loss of generality, we can assume $x_1\in(\powf p_1)^\dagger(R_j)$, where $j\in\{1,2\}$.
Then there exists $x_2$ that $(x_1,x_2)\in R_j$, then we have $(x_1,x_2)\in R_1\cup R_2$ that gives $x_1\in(\mathcal{P}p_1)^\dagger(R_1\cup R_2)$. Then there exists $x_2$ that $(x_1,x_2)\in R_j$, then we have $(x_1,x_2)\in R_1\cup R_2$ that gives $x_1\in(\powf p_1)^\dagger(R_1\cup R_2)$.
% We prove the lemma for the case that $i=1$. The proof is the same for $i=2$. % We prove the lemma for the case that $i=1$. The proof is the same for $i=2$.
% %
% First, we prove $(\mathcal{P}p_1)^\dagger\comp((\mathcal{P}s)^\dagger\comp\sigma\comp s\join\sigma)(x_1,x_2)\subseteq(\mathcal{P}p_1)^\dagger\comp(\mathcal{P}s)^\dagger\comp\sigma\comp s\join(\mathcal{P}p_1)^\dagger\comp\sigma(x_1,x_2)$. % First, we prove $(\powf p_1)^\dagger\comp((\powf s)^\dagger\comp\sigma\comp s\join\sigma)(x_1,x_2)\subseteq(\powf p_1)^\dagger\comp(\powf s)^\dagger\comp\sigma\comp s\join(\powf p_1)^\dagger\comp\sigma(x_1,x_2)$.
% Assuming $y_1\in(\mathcal{P}p_1)^\dagger\comp((\mathcal{P}s)^\dagger\comp\sigma\comp s\join\sigma)(x_1,x_2)$ then exists $y_2$ that we have either $(y_1,y_2)\in(\mathcal{P}s)^\dagger\comp\sigma\comp s(x_1,x_2)$ or $(y_1,y_2)\in\sigma(x_1,x_2)$. So, we have either $y_1\in(\mathcal{P}p_1)^\dagger\comp(\mathcal{P}s)^\dagger\comp\sigma\comp s(x_1,x_2)$ or $y_1\in(\mathcal{P}p_1)^\dagger\comp\sigma(x_1,x_2)$ that means that we have $y_1\in(\mathcal{P}p_1)^\dagger\comp(\mathcal{P}s)^\dagger\comp\sigma\comp s\join(\mathcal{P}p_1)^\dagger\comp\sigma(x_1,x_2)$. % Assuming $y_1\in(\powf p_1)^\dagger\comp((\powf s)^\dagger\comp\sigma\comp s\join\sigma)(x_1,x_2)$ then exists $y_2$ that we have either $(y_1,y_2)\in(\powf s)^\dagger\comp\sigma\comp s(x_1,x_2)$ or $(y_1,y_2)\in\sigma(x_1,x_2)$. So, we have either $y_1\in(\powf p_1)^\dagger\comp(\powf s)^\dagger\comp\sigma\comp s(x_1,x_2)$ or $y_1\in(\powf p_1)^\dagger\comp\sigma(x_1,x_2)$ that means that we have $y_1\in(\powf p_1)^\dagger\comp(\powf s)^\dagger\comp\sigma\comp s\join(\powf p_1)^\dagger\comp\sigma(x_1,x_2)$.
% %
% Now, we prove $(\mathcal{P}p_1)^\dagger\comp(\mathcal{P}s)^\dagger\comp\sigma\comp s\join(\mathcal{P}p_1)^\dagger\comp\sigma(x_1,x_2)\subseteq(\mathcal{P}p_1)^\dagger\comp((\mathcal{P}s)^\dagger\comp\sigma\comp s\join\sigma)(x_1,x_2)$. Assuming $y_1\in(\mathcal{P}p_1)^\dagger\comp(\mathcal{P}s)^\dagger\comp\sigma\comp s\join(\mathcal{P}p_1)^\dagger\comp\sigma(x_1,x_2)$ then we have: % Now, we prove $(\powf p_1)^\dagger\comp(\powf s)^\dagger\comp\sigma\comp s\join(\powf p_1)^\dagger\comp\sigma(x_1,x_2)\subseteq(\powf p_1)^\dagger\comp((\powf s)^\dagger\comp\sigma\comp s\join\sigma)(x_1,x_2)$. Assuming $y_1\in(\powf p_1)^\dagger\comp(\powf s)^\dagger\comp\sigma\comp s\join(\powf p_1)^\dagger\comp\sigma(x_1,x_2)$ then we have:
% \begin{itemize} % \begin{itemize}
% \item $y_1\in(\mathcal{P}p_1)^\dagger\comp(\mathcal{P}s)^\dagger\comp\sigma\comp s(x_1,x_2)$: Then there exists $y_2$ such that $(y_1,y_2)\in(\mathcal{P}s)^\dagger\comp\sigma\comp s(x_1,x_2)$. So, $(y_1,y_2)\in(\mathcal{P}s)^\dagger\comp\sigma\comp s\join\sigma(x_1,x_2)$, thus $y_1\in(\mathcal{P}p_1)^\dagger\comp((\mathcal{P}s)^\dagger\comp\sigma\comp s\join\sigma)(x_1,x_2)$. % \item $y_1\in(\powf p_1)^\dagger\comp(\powf s)^\dagger\comp\sigma\comp s(x_1,x_2)$: Then there exists $y_2$ such that $(y_1,y_2)\in(\powf s)^\dagger\comp\sigma\comp s(x_1,x_2)$. So, $(y_1,y_2)\in(\powf s)^\dagger\comp\sigma\comp s\join\sigma(x_1,x_2)$, thus $y_1\in(\powf p_1)^\dagger\comp((\powf s)^\dagger\comp\sigma\comp s\join\sigma)(x_1,x_2)$.
% \item $y_1\in(\mathcal{P}p_1)^\dagger\comp\sigma(x_1,x_2)$: Then there exists $y_2$ such that $(y_1,y_2)\in\sigma(x_1,x_2)$. So, $(y_1,y_2)\in(\mathcal{P}s)^\dagger\comp\sigma\comp s\join\sigma(x_1,x_2)$, thus $y_1\in(\mathcal{P}p_1)^\dagger\comp((\mathcal{P}s)^\dagger\comp\sigma\comp s\join\sigma)(x_1,x_2)$. % \item $y_1\in(\powf p_1)^\dagger\comp\sigma(x_1,x_2)$: Then there exists $y_2$ such that $(y_1,y_2)\in\sigma(x_1,x_2)$. So, $(y_1,y_2)\in(\powf s)^\dagger\comp\sigma\comp s\join\sigma(x_1,x_2)$, thus $y_1\in(\powf p_1)^\dagger\comp((\powf s)^\dagger\comp\sigma\comp s\join\sigma)(x_1,x_2)$.
% \end{itemize} \qed % \end{itemize} \qed
% \todo{Rewrite the proof according to the statement!} % \todo{Rewrite the proof according to the statement!}
\end{proof} \end{proof}
\begin{lemma} \begin{lemma}
Assuming that $\sigma_1$ and $\sigma_2$ are simulation structures of type $R\to(\mathcal{P}R)^\dagger$, then $\sigma_1 \join \sigma_2$ and $\sigma_1 \meet \sigma_2$ are also simulation structures of the same type. Assuming that $\sigma_1$ and $\sigma_2$ are simulation structures of type $R\to(\powf R)^\dagger$, then $\sigma_1 \join \sigma_2$ and $\sigma_1 \meet \sigma_2$ are also simulation structures of the same type.
\end{lemma} \end{lemma}
\begin{proof} \begin{proof}
Since $\sigma_1$ and $\sigma_2$ are simulation structures, for every $(x_1,x_2)\in R$, for $i\in\{1,2\}$ we have: Since $\sigma_1$ and $\sigma_2$ are simulation structures, for every $(x_1,x_2)\in R$, for $i\in\{1,2\}$ we have:
\begin{gather} \begin{gather}
\alpha(x_1)\subseteq(\mathcal{P}p_1)^\dagger\comp\sigma_i(x_1,x_2),\\ \alpha(x_1)\subseteq(\powf p_1)^\dagger\comp\sigma_i(x_1,x_2),\\
(\mathcal{P}p_2)^\dagger\comp\sigma_i(x_1,x_2)\subseteq\alpha(x_2). (\powf p_2)^\dagger\comp\sigma_i(x_1,x_2)\subseteq\alpha(x_2).
\end{gather} \end{gather}
First, we prove the case for $\join$. Since $\alpha(x_1)\subseteq(\mathcal{P}p_1)^\dagger\comp\sigma_i(x_1,x_2)$ we have the following: First, we prove the case for $\join$. Since $\alpha(x_1)\subseteq(\powf p_1)^\dagger\comp\sigma_i(x_1,x_2)$ we have the following:
\begin{gather*} \begin{gather*}
\alpha(x_1)\subseteq(\mathcal{P}p_1)^\dagger\comp\sigma_1(x_1,x_2)\cup (\mathcal{P}p_1)^\dagger\comp\sigma_2(x_1,x_2) \alpha(x_1)\subseteq(\powf p_1)^\dagger\comp\sigma_1(x_1,x_2)\cup (\powf p_1)^\dagger\comp\sigma_2(x_1,x_2)
\end{gather*} \end{gather*}
So, by~\autoref{lem:proj-dist-set} we have $\alpha(x_1)\subseteq(\mathcal{P}p_1)^\dagger(\sigma_1(x_1,x_2)\cup \sigma_2(x_1,x_2))$. So, by~\autoref{lem:proj-dist-set} we have $\alpha(x_1)\subseteq(\powf p_1)^\dagger(\sigma_1(x_1,x_2)\cup \sigma_2(x_1,x_2))$.
Similarly, we have $(\mathcal{P}p_2)^\dagger\comp\sigma_i(x_1,x_2)\subseteq\alpha(x_2)$ that gives the following: Similarly, we have $(\powf p_2)^\dagger\comp\sigma_i(x_1,x_2)\subseteq\alpha(x_2)$ that gives the following:
\begin{gather*} \begin{gather*}
(\mathcal{P}p_2)^\dagger\comp\sigma_1(x_1,x_2)\cup (\mathcal{P}p_2)^\dagger\comp\sigma_2(x_1,x_2)\subseteq\alpha(x_2) (\powf p_2)^\dagger\comp\sigma_1(x_1,x_2)\cup (\powf p_2)^\dagger\comp\sigma_2(x_1,x_2)\subseteq\alpha(x_2)
\end{gather*} \end{gather*}
So, by~\autoref{lem:proj-dist-set} we have $(\mathcal{P}p_2)^\dagger(\sigma_1(x_1,x_2)\cup \sigma_2(x_1,x_2))\subseteq\alpha(x_2)$. So, by~\autoref{lem:proj-dist-set} we have $(\powf p_2)^\dagger(\sigma_1(x_1,x_2)\cup \sigma_2(x_1,x_2))\subseteq\alpha(x_2)$.
Now, we prove the case for $\meet$. For $\meet$ unlike $\join$ we need to prove that $\sigma_1\meet\sigma_2(x_1,x_2)\in(\mathcal{P}R)^\dagger$. To achieve this, we need to show that assuming $\pi_1$, $\pi_2$ are projections of $\sigma_1\meet\sigma_2(x_1,x_2)$, then for $j\in\{1,2\}$ we have $\pi_j\comp(\sigma_1\meet\sigma_2)(x_1,x_2)\subseteq\mathcal{P}p_j(R)$. Since $(\mathcal{P}p_j)^\dagger\comp\sigma_i(x_1,x_2)\subseteq\mathcal{P}p_j(R)$, we have $\pi_j\comp(\sigma_1 \meet \sigma_2) (x_1,x_2)\subseteq\mathcal{P}p_j(R)$, so we have $\sigma_1\meet\sigma_2(x_1,x_2)\in(\mathcal{P}R)^\dagger$, meaning that $\pi_j\comp(\sigma_1\meet\sigma_2)(x_1,x_2)=(\mathcal{P}p_j)^\dagger\comp(\sigma_1\meet\sigma_2)(x_1,x_2)$.\ppnote{The last part of the proof is necessary because the type of the codomain of the definition of $\meet$ is not $(\mathcal{P}R)^\dagger$, but it is $\mathcal{P}X\times\mathcal{P}X$. Perhaps the epi-mono factorization must be used to cope with this in the abstract case.} Now, we prove the case for $\meet$. For $\meet$ unlike $\join$ we need to prove that $\sigma_1\meet\sigma_2(x_1,x_2)\in(\powf R)^\dagger$. To achieve this, we need to show that assuming $\pi_1$, $\pi_2$ are projections of $\sigma_1\meet\sigma_2(x_1,x_2)$, then for $j\in\{1,2\}$ we have $\pi_j\comp(\sigma_1\meet\sigma_2)(x_1,x_2)\subseteq\powf p_j(R)$. Since $(\powf p_j)^\dagger\comp\sigma_i(x_1,x_2)\subseteq\powf p_j(R)$, we have $\pi_j\comp(\sigma_1 \meet \sigma_2) (x_1,x_2)\subseteq\powf p_j(R)$, so we have $\sigma_1\meet\sigma_2(x_1,x_2)\in(\powf R)^\dagger$, meaning that $\pi_j\comp(\sigma_1\meet\sigma_2)(x_1,x_2)=(\powf p_j)^\dagger\comp(\sigma_1\meet\sigma_2)(x_1,x_2)$.\ppnote{The last part of the proof is necessary because the type of the codomain of the definition of $\meet$ is not $(\powf R)^\dagger$, but it is $\powf X\times\powf X$. Perhaps the epi-mono factorization must be used to cope with this in the abstract case.}
For $j\in\{1,2\}$ we have For $j\in\{1,2\}$ we have
\begin{gather}\label{eq:proj-meet} \begin{gather}\label{eq:proj-meet}
(\mathcal{P}p_j)^\dagger\comp(\sigma_1 \meet \sigma_2 (x_1,x_2))=(\mathcal{P}p_j)^\dagger\comp\sigma_1(x_1,x_2) \cap (\mathcal{P}p_j)^\dagger\comp\sigma_2(x_1,x_2). (\powf p_j)^\dagger\comp(\sigma_1 \meet \sigma_2 (x_1,x_2))=(\powf p_j)^\dagger\comp\sigma_1(x_1,x_2) \cap (\powf p_j)^\dagger\comp\sigma_2(x_1,x_2).
\end{gather} \end{gather}
Since $\alpha(x_1)\subseteq(\mathcal{P}p_1)^\dagger\comp\sigma_i(x_1,x_2)$, we have Since $\alpha(x_1)\subseteq(\powf p_1)^\dagger\comp\sigma_i(x_1,x_2)$, we have
\begin{gather*} \begin{gather*}
\alpha(x_1)\subseteq(\mathcal{P}p_1)^\dagger\comp\sigma_1(x_1,x_2)\cap (\mathcal{P}p_1)^\dagger\comp\sigma_2(x_1,x_2), \alpha(x_1)\subseteq(\powf p_1)^\dagger\comp\sigma_1(x_1,x_2)\cap (\powf p_1)^\dagger\comp\sigma_2(x_1,x_2),
\end{gather*} \end{gather*}
so by~\eqref{eq:proj-meet} we have $\alpha(x_1)\subseteq(\mathcal{P}p_1)^\dagger\comp(\sigma_1 \meet \sigma_2 (x_1,x_2))$. Similarly, since $(\mathcal{P}p_2)^\dagger\comp\sigma_i(x_1,x_2)\subseteq\alpha(x_2)$, we have so by~\eqref{eq:proj-meet} we have $\alpha(x_1)\subseteq(\powf p_1)^\dagger\comp(\sigma_1 \meet \sigma_2 (x_1,x_2))$. Similarly, since $(\powf p_2)^\dagger\comp\sigma_i(x_1,x_2)\subseteq\alpha(x_2)$, we have
\begin{gather*} \begin{gather*}
(\mathcal{P}p_2)^\dagger\comp\sigma_1(x_1,x_2)\cap (\mathcal{P}p_2)^\dagger\comp\sigma_2(x_1,x_2)\subseteq\alpha(x_2), (\powf p_2)^\dagger\comp\sigma_1(x_1,x_2)\cap (\powf p_2)^\dagger\comp\sigma_2(x_1,x_2)\subseteq\alpha(x_2),
\end{gather*} \end{gather*}
so by~\eqref{eq:proj-meet} we have $(\mathcal{P}p_2)^\dagger\comp(\sigma_1 \meet \sigma_2 (x_1,x_2))\subseteq\alpha(x_2)$.\qed so by~\eqref{eq:proj-meet} we have $(\powf p_2)^\dagger\comp(\sigma_1 \meet \sigma_2 (x_1,x_2))\subseteq\alpha(x_2)$.\qed
\end{proof} \end{proof}
\begin{lemma}\label{lem:sim-opsim-inc} \begin{lemma}\label{lem:sim-opsim-inc}
Assuming that $\sigma\c R\to(\mathcal{P}R)^\dagger$ is a simulation structure, and $R$ is symmetric, then for all $(x_1,x_2)\in R$ we have: Assuming that $\sigma\c R\to(\powf R)^\dagger$ is a simulation structure, and $R$ is symmetric, then for all $(x_1,x_2)\in R$ we have:
\begin{enumerate} \begin{enumerate}
\item $(\mathcal{P}p_1)^\dagger\comp(\mathcal{P}s)^\dagger\comp\sigma\comp s(x_1,x_2)\subseteq (\mathcal{P}p_1)^\dagger\comp\sigma(x_1,x_2)$ \item $(\powf p_1)^\dagger\comp(\powf s)^\dagger\comp\sigma\comp s(x_1,x_2)\subseteq (\powf p_1)^\dagger\comp\sigma(x_1,x_2)$
\item $(\mathcal{P}p_2)^\dagger\comp\sigma(x_1,x_2)\subseteq (\mathcal{P}p_2)^\dagger\comp(\mathcal{P}s)^\dagger\comp\sigma\comp s(x_1,x_2)$ \item $(\powf p_2)^\dagger\comp\sigma(x_1,x_2)\subseteq (\powf p_2)^\dagger\comp(\powf s)^\dagger\comp\sigma\comp s(x_1,x_2)$
\end{enumerate} \end{enumerate}
\end{lemma} \end{lemma}
\begin{proof} \begin{proof}
We prove the second clause. We prove the second clause.
By~\eqref{eq:diag-lax-sim} for every $(x_1,x_2)\in R$ we have By~\eqref{eq:diag-lax-sim} for every $(x_1,x_2)\in R$ we have
\begin{gather*} \begin{gather*}
\alpha(x_1)\subseteq(\mathcal{P}p_1)^\dagger\comp\sigma(x_1,x_2),\\ \alpha(x_1)\subseteq(\powf p_1)^\dagger\comp\sigma(x_1,x_2),\\
(\mathcal{P}p_2)^\dagger\comp\sigma(x_1,x_2)\subseteq\alpha(x_2). (\powf p_2)^\dagger\comp\sigma(x_1,x_2)\subseteq\alpha(x_2).
\end{gather*} \end{gather*}
From $\alpha(x_1)\subseteq(\mathcal{P}p_1)^\dagger\comp\sigma(x_1,x_2)$ since $R$ is symmetric we get $\alpha(x_2)\subseteq(\mathcal{P}p_1)^\dagger\comp\sigma(x_2,x_1)$, where From $\alpha(x_1)\subseteq(\powf p_1)^\dagger\comp\sigma(x_1,x_2)$ since $R$ is symmetric we get $\alpha(x_2)\subseteq(\powf p_1)^\dagger\comp\sigma(x_2,x_1)$, where
\begin{gather*} \begin{gather*}
(\mathcal{P}p_1)^\dagger\comp\sigma(x_2,x_1)=(\mathcal{P}p_2)^\dagger\comp(\mathcal{P}s)^\dagger\comp\sigma\comp s(x_1,x_2). (\powf p_1)^\dagger\comp\sigma(x_2,x_1)=(\powf p_2)^\dagger\comp(\powf s)^\dagger\comp\sigma\comp s(x_1,x_2).
\end{gather*} \end{gather*}
So, from $(\mathcal{P}p_2)^\dagger\comp\sigma(x_1,x_2)\subseteq\alpha(x_2)$ we have $(\mathcal{P}p_2)^\dagger\comp\sigma(x_1,x_2)\subseteq (\mathcal{P}p_2)^\dagger\comp(\mathcal{P}s)^\dagger\comp\sigma\comp s(x_1,x_2)$. Similarly, we can get the other inequation.\qed So, from $(\powf p_2)^\dagger\comp\sigma(x_1,x_2)\subseteq\alpha(x_2)$ we have $(\powf p_2)^\dagger\comp\sigma(x_1,x_2)\subseteq (\powf p_2)^\dagger\comp(\powf s)^\dagger\comp\sigma\comp s(x_1,x_2)$. Similarly, we can get the other inequation.\qed
\end{proof} \end{proof}
\begin{lemma}\label{lem:sim-bisim-inc} \begin{lemma}\label{lem:sim-bisim-inc}
Assuming that $\sigma\c R\to(\mathcal{P}R)^\dagger$ is a simulation structure, and $\beta\c R\to(\mathcal{P}R)^\dagger$ is a bisimulation structure, Assuming that $\sigma\c R\to(\powf R)^\dagger$ is a simulation structure, and $\beta\c R\to(\powf R)^\dagger$ is a bisimulation structure,
\begin{enumerate} \begin{enumerate}
\item if $\sigma\appr\beta$ then we have: \item if $\sigma\appr\beta$ then we have:
\begin{gather*} \begin{gather*}
\alpha(x_1)=(\mathcal{P}p_1)^\dagger\comp\sigma(x_1,x_2), \alpha(x_1)=(\powf p_1)^\dagger\comp\sigma(x_1,x_2),
\end{gather*} \end{gather*}
and if $R$ is symmetric we have and if $R$ is symmetric we have
\begin{gather*} \begin{gather*}
(\mathcal{P}p_2)^\dagger\comp(\mathcal{P}s)^\dagger\comp\sigma\comp s(x_1,x_2)=\alpha(x_2). (\powf p_2)^\dagger\comp(\powf s)^\dagger\comp\sigma\comp s(x_1,x_2)=\alpha(x_2).
\end{gather*} \end{gather*}
\item if $\beta\appr\sigma$ then we have: \item if $\beta\appr\sigma$ then we have:
\begin{gather*} \begin{gather*}
(\mathcal{P}p_2)^\dagger\comp\sigma(x_1,x_2)=\alpha(x_2) (\powf p_2)^\dagger\comp\sigma(x_1,x_2)=\alpha(x_2)
\end{gather*} \end{gather*}
and if $R$ is symmetric we have and if $R$ is symmetric we have
\begin{gather*} \begin{gather*}
\alpha(x_1)=(\mathcal{P}p_1)^\dagger\comp(\mathcal{P}s)^\dagger\comp\sigma\comp s(x_1,x_2). \alpha(x_1)=(\powf p_1)^\dagger\comp(\powf s)^\dagger\comp\sigma\comp s(x_1,x_2).
\end{gather*} \end{gather*}
\end{enumerate} \end{enumerate}
\end{lemma} \end{lemma}
\begin{proof} \begin{proof}
\begin{enumerate} \begin{enumerate}
\item Since $\sigma$ is a simulation structure for an arbitrary $(x_1,x_2)\in R$ we have $\alpha(x_1)\subseteq(\mathcal{P}p_1)^\dagger\comp\sigma(x_1,x_2)$. Since $\sigma\appr\beta$ we have $(\mathcal{P}p_1)\comp\sigma(x_1,x_2)\subseteq(\mathcal{P}p_1)\comp\beta(x_1,x_2)$, while $(\mathcal{P}p_1)\comp\beta(x_1,x_2)=\alpha(x_1)$ by definition of bisimulation. So we have $\alpha(x_1)=(\mathcal{P}p_1)^\dagger\comp\sigma(x_1,x_2)$. Then because of the symmetry of $R$ the second clause is easily achievable by using the equations in~\eqref{eq:diag-sym-rel}. \item Since $\sigma$ is a simulation structure for an arbitrary $(x_1,x_2)\in R$ we have $\alpha(x_1)\subseteq(\powf p_1)^\dagger\comp\sigma(x_1,x_2)$. Since $\sigma\appr\beta$ we have $(\powf p_1)\comp\sigma(x_1,x_2)\subseteq(\powf p_1)\comp\beta(x_1,x_2)$, while $(\powf p_1)\comp\beta(x_1,x_2)=\alpha(x_1)$ by definition of bisimulation. So we have $\alpha(x_1)=(\powf p_1)^\dagger\comp\sigma(x_1,x_2)$. Then because of the symmetry of $R$ the second clause is easily achievable by using the equations in~\eqref{eq:diag-sym-rel}.
\item This clause can be proven similar to (1). \item This clause can be proven similar to (1).
\end{enumerate}\qed \end{enumerate}\qed
\end{proof} \end{proof}
\begin{prop} \begin{prop}
Assuming that $\sigma\c R\to(\mathcal{P}R)^\dagger$ is a simulation structure, and $\beta\c R\to(\mathcal{P}R)^\dagger$ is a bisimulation structure, Assuming that $\sigma\c R\to(\powf R)^\dagger$ is a simulation structure, and $\beta\c R\to(\powf R)^\dagger$ is a bisimulation structure,
\begin{enumerate} \begin{enumerate}
\item if $\sigma\appr\beta$ then we have: \item if $\sigma\appr\beta$ then we have:
\begin{gather*} \begin{gather*}
\beta=\sigma\join ((\mathcal{P}s)^\dagger\comp\sigma\comp s) \beta=\sigma\join ((\powf s)^\dagger\comp\sigma\comp s)
\end{gather*} \end{gather*}
\item if $\beta\appr\sigma$ then we have: \item if $\beta\appr\sigma$ then we have:
\begin{gather*} \begin{gather*}
\beta=\sigma\meet((\mathcal{P}s)^\dagger\comp\sigma\comp s) \beta=\sigma\meet((\powf s)^\dagger\comp\sigma\comp s)
\end{gather*} \end{gather*}
\end{enumerate} \end{enumerate}
\end{prop} \end{prop}
\begin{proof} \begin{proof}
1. We need to prove that $\sigma\join((\mathcal{P}s)^\dagger\comp\sigma\comp s)$ is the bisimulation structure. 1. We need to prove that $\sigma\join((\powf s)^\dagger\comp\sigma\comp s)$ is the bisimulation structure.
By~\autoref{lem:sim-opsim-inc}.(1), for every $(x_1,x_2)\in R$, we have $(\mathcal{P}p_1)^\dagger\comp(\mathcal{P}s)^\dagger\comp\sigma\comp s(x_1,x_2)\subseteq(\mathcal{P}p_1)^\dagger\comp\sigma(x_1,x_2)$, and by~\autoref{lem:sim-bisim-inc}.(1), we have $(\mathcal{P}p_1)^\dagger\comp\sigma(x_1,x_2)=\alpha(x_1)$. So, we have $(\mathcal{P}p_1)^\dagger\comp\sigma\join(\mathcal{P}p_1)^\dagger\comp(\mathcal{P}s)^\dagger\comp\sigma\comp s(x_1,x_2)=\alpha(x_1)$, then by~\autoref{lem:proj-dist-set} we have $(\mathcal{P}p_1)^\dagger\comp(\sigma\join((\mathcal{P}s)^\dagger\comp\sigma\comp s))(x_1,x_2)=\alpha(x_1)$. By~\autoref{lem:sim-opsim-inc}.(1), for every $(x_1,x_2)\in R$, we have $(\powf p_1)^\dagger\comp(\powf s)^\dagger\comp\sigma\comp s(x_1,x_2)\subseteq(\powf p_1)^\dagger\comp\sigma(x_1,x_2)$, and by~\autoref{lem:sim-bisim-inc}.(1), we have $(\powf p_1)^\dagger\comp\sigma(x_1,x_2)=\alpha(x_1)$. So, we have $(\powf p_1)^\dagger\comp\sigma\join(\powf p_1)^\dagger\comp(\powf s)^\dagger\comp\sigma\comp s(x_1,x_2)=\alpha(x_1)$, then by~\autoref{lem:proj-dist-set} we have $(\powf p_1)^\dagger\comp(\sigma\join((\powf s)^\dagger\comp\sigma\comp s))(x_1,x_2)=\alpha(x_1)$.
Also, by~\autoref{lem:sim-bisim-inc}.(1) we have $(\mathcal{P}p_2)^\dagger\comp(\mathcal{P}s)^\dagger\comp\sigma(x_1,x_2)=\alpha(x_2)$. So, since we already have $(\mathcal{P}p_2)^\dagger\comp\sigma(x_1,x_2)\subseteq\alpha(x_2)$ then by~\autoref{lem:proj-dist-set} we have $(\mathcal{P}p_2)^\dagger\comp(\sigma\join((\mathcal{P}s)^\dagger\comp\sigma\comp s))(x_1,x_2)=\alpha(x_2)$. Also, by~\autoref{lem:sim-bisim-inc}.(1) we have $(\powf p_2)^\dagger\comp(\powf s)^\dagger\comp\sigma(x_1,x_2)=\alpha(x_2)$. So, since we already have $(\powf p_2)^\dagger\comp\sigma(x_1,x_2)\subseteq\alpha(x_2)$ then by~\autoref{lem:proj-dist-set} we have $(\powf p_2)^\dagger\comp(\sigma\join((\powf s)^\dagger\comp\sigma\comp s))(x_1,x_2)=\alpha(x_2)$.
2. We need to prove that $\sigma\meet((\mathcal{P}s)^\dagger\comp\sigma\comp s)$ is the bisimulation structure. 2. We need to prove that $\sigma\meet((\powf s)^\dagger\comp\sigma\comp s)$ is the bisimulation structure.
For $i\in\{1,2\}$, for every $(x_1,x_2)\in R$, we have: For $i\in\{1,2\}$, for every $(x_1,x_2)\in R$, we have:
{\small {\small
\begin{align*} \begin{align*}
&(\mathcal{P}p_i)^\dagger\comp(\sigma\meet((\mathcal{P}s)^\dagger\comp\sigma\comp s))(x_1,x_2)\\ &(\powf p_i)^\dagger\comp(\sigma\meet((\powf s)^\dagger\comp\sigma\comp s))(x_1,x_2)\\
&=(\mathcal{P}p_i)^\dagger\comp(((\mathcal{P}p_1)^\dagger\comp\sigma(x_1,x_2) \cap (\mathcal{P}p_1)^\dagger\comp((\mathcal{P}s)^\dagger\comp\sigma\comp s)(x_1,x_2))\times((\mathcal{P}p_2)^\dagger\comp\sigma(x_1,x_2) \cap (\mathcal{P}p_2)^\dagger\comp((\mathcal{P}s)^\dagger\comp\sigma\comp s)(x_1,x_2)))\\ &=(\powf p_i)^\dagger\comp(((\powf p_1)^\dagger\comp\sigma(x_1,x_2) \cap (\powf p_1)^\dagger\comp((\powf s)^\dagger\comp\sigma\comp s)(x_1,x_2))\times((\powf p_2)^\dagger\comp\sigma(x_1,x_2) \cap (\powf p_2)^\dagger\comp((\powf s)^\dagger\comp\sigma\comp s)(x_1,x_2)))\\
&=(\mathcal{P}p_i)^\dagger\comp\sigma(x_1,x_2) \cap (\mathcal{P}p_i)^\dagger\comp((\mathcal{P}s)^\dagger\comp\sigma\comp s)(x_1,x_2) &=(\powf p_i)^\dagger\comp\sigma(x_1,x_2) \cap (\powf p_i)^\dagger\comp((\powf s)^\dagger\comp\sigma\comp s)(x_1,x_2)
\end{align*} \end{align*}
} }
By~\autoref{lem:sim-opsim-inc}.(1), $(\mathcal{P}p_1)^\dagger\comp((\mathcal{P}s)^\dagger\comp\sigma\comp s)(x_1,x_2)\subseteq (\mathcal{P}p_1)^\dagger\comp\sigma(x_1,x_2)$, and by~\autoref{lem:sim-bisim-inc}.(2) we have $(\mathcal{P}p_1)^\dagger\comp((\mathcal{P}s)^\dagger\comp\sigma\comp s)(x_1,x_2)=\alpha(x_1)$, so we have $(\mathcal{P}p_1)^\dagger\comp(\sigma\meet((\mathcal{P}s)^\dagger\comp\sigma\comp s))(x_1,x_2)=\alpha(x_1)$. By~\autoref{lem:sim-opsim-inc}.(1), $(\powf p_1)^\dagger\comp((\powf s)^\dagger\comp\sigma\comp s)(x_1,x_2)\subseteq (\powf p_1)^\dagger\comp\sigma(x_1,x_2)$, and by~\autoref{lem:sim-bisim-inc}.(2) we have $(\powf p_1)^\dagger\comp((\powf s)^\dagger\comp\sigma\comp s)(x_1,x_2)=\alpha(x_1)$, so we have $(\powf p_1)^\dagger\comp(\sigma\meet((\powf s)^\dagger\comp\sigma\comp s))(x_1,x_2)=\alpha(x_1)$.
Also, by~\autoref{lem:sim-bisim-inc}.(2) we have $(\mathcal{P}p_2)^\dagger\comp\sigma(x_1,x_2)=\alpha(x_2)$, so, since by~\autoref{lem:sim-opsim-inc}.(2), we have $(\mathcal{P}p_2)^\dagger\comp\sigma(x_1,x_2)\subseteq (\mathcal{P}p_2)^\dagger\comp(\mathcal{P}s)^\dagger\comp\sigma\comp s(x_1,x_2)$, so we have $(\mathcal{P}p_2)^\dagger\comp(\sigma\meet((\mathcal{P}s)^\dagger\comp\sigma\comp s)(x_1,x_2))=\alpha(x_2)$.\qed Also, by~\autoref{lem:sim-bisim-inc}.(2) we have $(\powf p_2)^\dagger\comp\sigma(x_1,x_2)=\alpha(x_2)$, so, since by~\autoref{lem:sim-opsim-inc}.(2), we have $(\powf p_2)^\dagger\comp\sigma(x_1,x_2)\subseteq (\powf p_2)^\dagger\comp(\powf s)^\dagger\comp\sigma\comp s(x_1,x_2)$, so we have $(\powf p_2)^\dagger\comp(\sigma\meet((\powf s)^\dagger\comp\sigma\comp s)(x_1,x_2))=\alpha(x_2)$.\qed
\end{proof} \end{proof}
\begin{cor} \begin{cor}
Assuming that $R$ is a symmetric relation, and $S\neq\emptyset$ is the set of all simulation structures of the type $R\to (\mathcal{P}R)^\dagger$, then if the bisimulation morphism exists, it is equal with the following morphism: Assuming that $R$ is a symmetric relation, and $S\neq\emptyset$ is the set of all simulation structures of the type $R\to (\powf R)^\dagger$, then if the bisimulation morphism exists, it is equal with the following morphism:
\begin{gather*} \begin{gather*}
(\bigjoin_{\sigma\in S}\sigma)\meet(\mathcal{P}s)^\dagger\comp(\bigjoin_{\sigma\in S}\sigma)\comp s (\bigjoin_{\sigma\in S}\sigma)\meet(\powf s)^\dagger\comp(\bigjoin_{\sigma\in S}\sigma)\comp s
\end{gather*} \end{gather*}
\end{cor} \end{cor}
\begin{lemma} \begin{lemma}
For every $S\in \mathcal{P}R$, For every $S\in \powf R$,
\begin{gather*} \begin{gather*}
((\mathcal{P}p_1)^\dagger(S),(\mathcal{P}p_2)^\dagger(S))\in(\mathcal{P}R)^\dagger\Leftrightarrow(\mathcal{P}p_1)(S)\subseteq(\mathcal{P}p_1)(R),(\mathcal{P}p_2)(S)\subseteq(\mathcal{P}p_2)(R) ((\powf p_1)^\dagger(S),(\powf p_2)^\dagger(S))\in(\powf R)^\dagger\Leftrightarrow(\powf p_1)(S)\subseteq(\powf p_1)(R),(\powf p_2)(S)\subseteq(\powf p_2)(R)
\end{gather*} \end{gather*}
\end{lemma} \end{lemma}
\begin{lemma}\label{lem:alph-prod} \begin{lemma}\label{lem:alph-prod}
Assuming that $R$ is a symmetric relation, and $S\neq\emptyset$ is the set of all simulation structures of the type $R\to (\mathcal{P}R)^\dagger$, then there there exists a simulation structure $\sigma\in S$ that for every $(x_1,x_2)$, $(\mathcal{P}p_1)^\dagger\comp\sigma(x_1,x_2)=\alpha(x_1)$. Assuming that $R$ is a symmetric relation, and $S\neq\emptyset$ is the set of all simulation structures of the type $R\to (\powf R)^\dagger$, then there there exists a simulation structure $\sigma\in S$ that for every $(x_1,x_2)$, $(\powf p_1)^\dagger\comp\sigma(x_1,x_2)=\alpha(x_1)$.
\end{lemma} \end{lemma}
\begin{proof} \begin{proof}
Since $S\neq\emptyset$ there exists $\delta\in S$. We define $\sigma$ for every $(x_1,x_2)$ as the following: Since $S\neq\emptyset$ there exists $\delta\in S$. We define $\sigma$ for every $(x_1,x_2)$ as the following:
\begin{gather*} \begin{gather*}
\sigma(x_1,x_2)=(\alpha(x_1), (\mathcal{P}p_2)^\dagger\comp\delta(x_1,x_2)) \sigma(x_1,x_2)=(\alpha(x_1), (\powf p_2)^\dagger\comp\delta(x_1,x_2))
\end{gather*} \end{gather*}
We have $\sigma(x_1,x_2)\in(\mathcal{P}R)^\dagger$, as $\alpha(x_1)\subseteq\mathcal{P}p_1(R)$ and $(\mathcal{P}p_2)^\dagger\comp\delta(x_1,x_2)\subseteq\mathcal{P}p_2(R)$ are inherited from $\delta$ being a simulation structure. We have $\sigma(x_1,x_2)\in(\powf R)^\dagger$, as $\alpha(x_1)\subseteq\powf p_1(R)$ and $(\powf p_2)^\dagger\comp\delta(x_1,x_2)\subseteq\powf p_2(R)$ are inherited from $\delta$ being a simulation structure.
Also, it obviously is a simulation as $(\mathcal{P}p_1)^\dagger\comp\sigma(x_1,x_2)=\alpha(x_1)$ and $(\mathcal{P}p_2)^\dagger\comp\sigma(x_1,x_2)\subseteq\alpha(x_2)$ as $(\mathcal{P}p_2)^\dagger\comp\delta(x_1,x_2)\subseteq\alpha(x_2)$. Also, it obviously is a simulation as $(\powf p_1)^\dagger\comp\sigma(x_1,x_2)=\alpha(x_1)$ and $(\powf p_2)^\dagger\comp\sigma(x_1,x_2)\subseteq\alpha(x_2)$ as $(\powf p_2)^\dagger\comp\delta(x_1,x_2)\subseteq\alpha(x_2)$.
\end{proof} \end{proof}
\begin{prop}\label{prop:sym-rel-bisim} \begin{prop}\label{prop:sym-rel-bisim}
Assuming that $R$ is a symmetric relation, and $S\neq\emptyset$ is the set of all simulation structures of the type $R\to (\mathcal{P}R)^\dagger$, then the following morphism is the bisimulation structure: Assuming that $R$ is a symmetric relation, and $S\neq\emptyset$ is the set of all simulation structures of the type $R\to (\powf R)^\dagger$, then the following morphism is the bisimulation structure:
\begin{gather*} \begin{gather*}
(\bigmeet_{\sigma\in S}\sigma)\join(\mathcal{P}s)^\dagger\comp(\bigmeet_{\sigma\in S}\sigma)\comp s (\bigmeet_{\sigma\in S}\sigma)\join(\powf s)^\dagger\comp(\bigmeet_{\sigma\in S}\sigma)\comp s
\end{gather*} \end{gather*}
\end{prop} \end{prop}
\begin{proof} \begin{proof}
For every $(x_1,x_2)\in R$ we have For every $(x_1,x_2)\in R$ we have
\begin{gather*} \begin{gather*}
(\mathcal{P}p_1)^\dagger\comp((\bigmeet_{\sigma\in S}\sigma)\join(\mathcal{P}s)^\dagger\comp(\bigmeet_{\sigma\in S}\sigma)\comp s)(x_1,x_2)= (\powf p_1)^\dagger\comp((\bigmeet_{\sigma\in S}\sigma)\join(\powf s)^\dagger\comp(\bigmeet_{\sigma\in S}\sigma)\comp s)(x_1,x_2)=
(\mathcal{P}p_1)^\dagger\comp(\bigmeet_{\sigma\in S}\sigma)(x_1,x_2), (\powf p_1)^\dagger\comp(\bigmeet_{\sigma\in S}\sigma)(x_1,x_2),
\end{gather*} \end{gather*}
and and
\begin{gather*} \begin{gather*}
(\mathcal{P}p_2)^\dagger\comp((\bigmeet_{\sigma\in S}\sigma)\join(\mathcal{P}s)^\dagger\comp(\bigmeet_{\sigma\in S}\sigma)\comp s)(x_1,x_2)= (\powf p_2)^\dagger\comp((\bigmeet_{\sigma\in S}\sigma)\join(\powf s)^\dagger\comp(\bigmeet_{\sigma\in S}\sigma)\comp s)(x_1,x_2)=
(\mathcal{P}p_2)^\dagger\comp((\mathcal{P}s)^\dagger\comp(\bigmeet_{\sigma\in S}\sigma)\comp s)(x_1,x_2). (\powf p_2)^\dagger\comp((\powf s)^\dagger\comp(\bigmeet_{\sigma\in S}\sigma)\comp s)(x_1,x_2).
\end{gather*} \end{gather*}
By~\autoref{lem:alph-prod} there exists a simulation $\delta\in S$ for which we have $(\mathcal{P}p_1)^\dagger\comp\delta(x_1,x_2)=\alpha(x_1)$. So, $(\mathcal{P}p_1)^\dagger\comp(\bigmeet_{\sigma\in S}\sigma)(x_1,x_2)=\alpha(x_1)$. Then by the equations in~\eqref{eq:diag-sym-rel} we also get $(\mathcal{P}p_2)^\dagger\comp((\mathcal{P}s)^\dagger\comp(\bigmeet_{\sigma\in S}\sigma)\comp s)(x_1,x_2)=\alpha(x_2)$.\qed By~\autoref{lem:alph-prod} there exists a simulation $\delta\in S$ for which we have $(\powf p_1)^\dagger\comp\delta(x_1,x_2)=\alpha(x_1)$. So, $(\powf p_1)^\dagger\comp(\bigmeet_{\sigma\in S}\sigma)(x_1,x_2)=\alpha(x_1)$. Then by the equations in~\eqref{eq:diag-sym-rel} we also get $(\powf p_2)^\dagger\comp((\powf s)^\dagger\comp(\bigmeet_{\sigma\in S}\sigma)\comp s)(x_1,x_2)=\alpha(x_2)$.\qed
\end{proof} \end{proof}
\section{Symmetric Simulation in Quantaloids} \section{Symmetric Simulation in Quantaloids}
We generalize~\autoref{prop:sym-rel-bisim} in regular quantaloids. A quantaloid is a category enriched with suplattices. We generalize~\autoref{prop:sym-rel-bisim} in regular quantaloids. A quantaloid is a category enriched with suplattices.
@ -1886,14 +1887,14 @@ At the moment we have limited the discussion to the category of sets and we are
\begin{equation*} \begin{equation*}
\begin{tikzcd}[ampersand replacement=\&] \begin{tikzcd}[ampersand replacement=\&]
X \& R \& Y\\ X \& R \& Y\\
{\mathcal{P}X} \& {\subseteq;(\mathcal{P}R)^\dagger;\subseteq} \& {\mathcal{P}Y} {\powf X} \& {\subseteq;(\powf R)^\dagger;\subseteq} \& {\powf Y}
\arrow["\alpha"', from=1-1, to=2-1] \arrow["\alpha"', from=1-1, to=2-1]
\arrow["{p_1}"', from=1-2, to=1-1] \arrow["{p_1}"', from=1-2, to=1-1]
\arrow["{p_2}", from=1-2, to=1-3] \arrow["{p_2}", from=1-2, to=1-3]
\arrow["\sigma", dashed, from=1-2, to=2-2] \arrow["\sigma", dashed, from=1-2, to=2-2]
\arrow["\beta", from=1-3, to=2-3] \arrow["\beta", from=1-3, to=2-3]
\arrow["{{\mathcal{P}p_1}_\subseteq}", from=2-2, to=2-1] \arrow["{{\powf p_1}_\subseteq}", from=2-2, to=2-1]
\arrow["{{\mathcal{P}p_2}_\subseteq}"', from=2-2, to=2-3] \arrow["{{\powf p_2}_\subseteq}"', from=2-2, to=2-3]
\end{tikzcd} \end{tikzcd}
\end{equation*} \end{equation*}
It is defined as $\sigma(x_1,x_2)=(\alpha(x_1),\beta(x_2))$. It is defined as $\sigma(x_1,x_2)=(\alpha(x_1),\beta(x_2))$.
@ -1901,7 +1902,7 @@ But $\sigma'$ in the following diagram is not unique:
\begin{equation*} \begin{equation*}
\begin{tikzcd}[ampersand replacement=\&] \begin{tikzcd}[ampersand replacement=\&]
X \& R \& Y \\ X \& R \& Y \\
{\mathcal{P}X} \& {(\mathcal{P}R)^\dagger} \& {\mathcal{P}Y} {\powf X} \& {(\powf R)^\dagger} \& {\powf Y}
\arrow["\alpha"', from=1-1, to=2-1] \arrow["\alpha"', from=1-1, to=2-1]
\arrow["\subseteq"{marking, allow upside down}, draw=none, from=1-1, to=2-2] \arrow["\subseteq"{marking, allow upside down}, draw=none, from=1-1, to=2-2]
\arrow["{p_1}"', from=1-2, to=1-1] \arrow["{p_1}"', from=1-2, to=1-1]
@ -1909,16 +1910,16 @@ But $\sigma'$ in the following diagram is not unique:
\arrow["{\sigma'}", from=1-2, to=2-2] \arrow["{\sigma'}", from=1-2, to=2-2]
\arrow["\beta", from=1-3, to=2-3] \arrow["\beta", from=1-3, to=2-3]
\arrow["\subseteq"{marking, allow upside down}, draw=none, from=2-2, to=1-3] \arrow["\subseteq"{marking, allow upside down}, draw=none, from=2-2, to=1-3]
\arrow["{{\mathcal{P}p_1^\dagger}}", from=2-2, to=2-1] \arrow["{{\powf p_1^\dagger}}", from=2-2, to=2-1]
\arrow["{{\mathcal{P}p_2^\dagger}}"', from=2-2, to=2-3] \arrow["{{\powf p_2^\dagger}}"', from=2-2, to=2-3]
\end{tikzcd} \end{tikzcd}
\end{equation*} \end{equation*}
Because assuming we have $\sigma$, for every given $\sigma'$ we can define a $\delta\c(\mathcal{P}R)^\dagger\to\subseteq;(\mathcal{P}R)^\dagger;\subseteq$ that $\sigma=\delta\comp\sigma'$, i.e., the following diagram commutes: Because assuming we have $\sigma$, for every given $\sigma'$ we can define a $\delta\c(\powf R)^\dagger\to\subseteq;(\powf R)^\dagger;\subseteq$ that $\sigma=\delta\comp\sigma'$, i.e., the following diagram commutes:
\begin{equation*} \begin{equation*}
\begin{tikzcd}[ampersand replacement=\&] \begin{tikzcd}[ampersand replacement=\&]
X \& R \& Y \\ X \& R \& Y \\
{\mathcal{P}X} \& {(\mathcal{P}R)^\dagger} \& {\mathcal{P}Y} \\ {\powf X} \& {(\powf R)^\dagger} \& {\powf Y} \\
{\mathcal{P}X} \& {\subseteq;(\mathcal{P}R)^\dagger;\subseteq} \& {\mathcal{P}Y} {\powf X} \& {\subseteq;(\powf R)^\dagger;\subseteq} \& {\powf Y}
\arrow["\alpha"', from=1-1, to=2-1] \arrow["\alpha"', from=1-1, to=2-1]
\arrow["{p_1}"', from=1-2, to=1-1] \arrow["{p_1}"', from=1-2, to=1-1]
\arrow["{p_2}", from=1-2, to=1-3] \arrow["{p_2}", from=1-2, to=1-3]
@ -1927,11 +1928,11 @@ Because assuming we have $\sigma$, for every given $\sigma'$ we can define a $\d
\arrow["id"', from=2-1, to=3-1] \arrow["id"', from=2-1, to=3-1]
\arrow["\delta", from=2-2, to=3-2] \arrow["\delta", from=2-2, to=3-2]
\arrow["id", from=2-3, to=3-3] \arrow["id", from=2-3, to=3-3]
\arrow["{{\mathcal{P}p_1}_\subseteq}", from=3-2, to=3-1] \arrow["{{\powf p_1}_\subseteq}", from=3-2, to=3-1]
\arrow["{{\mathcal{P}p_2}_\subseteq}"', from=3-2, to=3-3] \arrow["{{\powf p_2}_\subseteq}"', from=3-2, to=3-3]
\end{tikzcd} \end{tikzcd}
\end{equation*} \end{equation*}
To define $\delta$, we define $c\c(\mathcal{P}R^\dagger)\to((\mathcal{P}R^\dagger)\times R)+(\mathcal{P}R)^\dagger$ and $u\c((\mathcal{P}R^\dagger)\times R)+(\mathcal{P}R)^\dagger\to\subseteq;(\mathcal{P}R)^\dagger;\subseteq$ and then we define $\delta=u\comp c$. Here are the definitions for $c$ and $u$: To define $\delta$, we define $c\c(\powf R^\dagger)\to((\powf R^\dagger)\times R)+(\powf R)^\dagger$ and $u\c((\powf R^\dagger)\times R)+(\powf R)^\dagger\to\subseteq;(\powf R)^\dagger;\subseteq$ and then we define $\delta=u\comp c$. Here are the definitions for $c$ and $u$:
\begin{gather*} \begin{gather*}
c(w)= c(w)=
\begin{cases} \begin{cases}
@ -2102,6 +2103,23 @@ The above translation seems to be true in a more general case, where $\spa$ and
\begin{proof} \begin{proof}
(Completeness): We show $\relar$-similarity with $r_s$ and $\hat{\relar}$-similarity with $r_{\hat{s}}$. Also, we show the behabioural equivalence with $r_b$. Since (Completeness): We show $\relar$-similarity with $r_s$ and $\hat{\relar}$-similarity with $r_{\hat{s}}$. Also, we show the behabioural equivalence with $r_b$. Since
\end{proof} \end{proof}
Assuming that $\relar$-similarity is complete, does not guarantee that $\hat{\relar}$-similarity is sound and complete. We give a counter-example. Assuming that $\relar$ is a $\powf$-relator that takes $r\c X\rto Y$ to $\powf X\times \powf Y$, then $\hat{\relar} r= \powf X\times\powf Y$ as well. It means that for every coalgebras $(X,\alpha)$, $(Y,\beta)$, $\hat{\relar}$-similarity is equal to $X\times Y$, which is rare to be equal to behavioural equivalence. For example, if we take $X=\{x_1,x_2\}$ and $Y=\{y_1,y_2,y_3\}$, and we define $\alpha$ and $\beta$ as
\begin{gather*}
\alpha(x)=
\begin{cases}
\{x_1,x_2\} & x=x_1 \\
\{x_2\} & x=x_2
\end{cases}
\intertext{and}
\beta(y)=
\begin{cases}
\{y_3\} & y=y_1 \\
Y & y=y_2\\
\emptyset & y=y_3
\end{cases}
\end{gather*}
then at least $(x_1,y_3)$ is not in the behavioural equivalence, while it is in $\hat{\relar}$-similarity.
\end{document} \end{document}