A good counter example!!!

draft/draft.tex

@@ -1203,7 +1203,7 @@ A big concern with this approach is that Comma Objects are defined in a 2-catego
 
 \subsection{Choosing a suitable order for our setting}
 Maybe we can first choose a suitable order on $T(\Sigma_\val\mS\times D(\mS,\mS))$ and then prove that if a relation and its inverse is a simulation then it is a bisimulation as well. Maybe $T$ being $\omega$-continuous can give the ordering. It can be something easier that relates to termination as well! That if a term has a big-step evaluation, then it is bigger than or equal to any other term, and if it does not, then it is less than or equal to any other term.
-\section{Symmetric Simulation is Bisimulation}
+\section{Symmetric Simulation is a Bisimulation}
 \begin{definition}[Graph]
 	In a category $\BC$ a graph is a tuple $(R,X)$ of the following form:
 	\begin{equation*}
@@ -2161,6 +2161,30 @@ We recall that in the above diagram $\sigma_3$ is a bisimulation, and the rest a
 %	\end{gather*}
 %	We have $(Fp_1)^\dagger\comp\sigma$.
 %\end{proof}
+\begin{example}
+And another counter-example!!! 
+Assuming that $F$ is the powerset endofunctor over the category of sets and injective maps. Then for every $X$, we define the order on $FX$ as $A\appr B$ whenever $|A|\leq |B|$, where $|A|$ and $|B|$ are just cardinalities of $|A|$ and $|B|$ respectively. This is a preorder.\\
+We take $R=\{(1,1),(1,2),(2,1),(2,2)\}$, and $X=\{1,2,3\}$. $\alpha$ is defined as below:
+\begin{gather*}
+	\alpha(x)=
+	\begin{cases} 
+		\{1,2\} & x=1  \\
+		\{2,3\} & x=2\\
+		\{3\} & x=3
+	\end{cases}
+\end{gather*}
+$\sigma$ is defined as below:
+\begin{gather*}
+	\sigma(w)=
+	\begin{cases} 
+		\{(1,2),(2,2)\} & w=(1,2)  \\
+		\{(2,1),(2,2)\} & w=(2,1)  \\
+		\{(1,2),(2,1)\} & w=(1,1)  \\
+		\{(2,2),(1,1)\} & w=(2,2)
+	\end{cases}
+\end{gather*}
+$R$ is symmetric, and $\sigma$ is a witness for $R$ to be an AM-simulation, but $R$ is not a bisimulation in the traditional sense because $(2,1)\in R$, and $2\to 3$, but $(3,1)$ or $(3,2)$ are not in $R$. It is easy to see that it is not an AM-bisimulation as well because we can not define a function that can serve as an evidence for it as $3$ does not appear in any pair in $R$, while it exists in $\alpha(2)$.
+\end{example}
 \subsection{The concrete proof}
 %\begin{lemma}\label{lem:sim-opsim-inc1}\ppnote{Actually, this lemma holds for every functor in an arbitrary category.}
 %	Assuming that $\sigma\c R\to\powf R$ is witness for a symmetric relation $R$ to be an AM simulation on $\powf$-coalgebra $(X,\alpha)$, then for all $(x_1,x_2)\in R$ we have: