counter-example edited

draft/draft.tex

@@ -1144,17 +1144,15 @@ 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.
 
-\begin{example}
-	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*}
-		\sigma(w)=
-		\begin{cases} 
-			R & w\neq (1,3)  \\
-			R\setminus\{(1,2)\} & w=(1,3)
-		\end{cases}
-	\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 $(\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}
+(But still!)We have a counter-example for a symmetric relation $R$ that has a witness to be a simulation, but that morphism does not serve as a witness for $R$ to be a bisimulation. In the category of sets we 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:
+\begin{gather*}
+	\sigma(w)=
+	\begin{cases} 
+		(X,X) & w\neq (1,3)  \\
+		(X,X\setminus\{2\}) & w=(1,3)
+	\end{cases}
+\end{gather*}
+In this scenario, $\sigma$ is a witness for $R$ to be a simulation, but it is not a witness for $R$ to be a bisimulation. $\sigma$ is a witness for $R$ to be a simulation since for every $w\in R$ we have $\alpha(p_1(w))\subseteq((\mathcal{P}p_1)^\ddagger(\sigma(w)))=X$. Also, for every $w\in R$, $((\mathcal{P}p_2)^\ddagger(\sigma(w)))\subseteq\alpha(p_2(w))=X$. But it is not a bisimulation, since $\alpha(p_2(1,3))=\alpha(3)=X\neq(\mathcal{P}p_2)^\ddagger(\sigma(1,3))=X\setminus\{2\}$.
 %
 \begin{example}
 	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:
@@ -1787,7 +1785,7 @@ We define $\join$ and $\meet$ on morphisms as follows:
 \begin{lemma}
 	For every $S\in \powf R$,
 	\begin{gather*}
-		((\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)
+		((\powf p_1)(S),(\powf p_2)(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{lemma}
 \begin{lemma}\label{lem:alph-prod}