maybe

draft/draft.tex

@@ -2104,6 +2104,55 @@ Since $\subseteq$ is a liftable order (\autoref{def:liftable-ord}), we have the
 	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}
 
+\subsection{Maybe Functor}
+We prove that symmetric simulation is a bisimulation for the case that $FX=X+1$. First, we prove it for $\Set$.
+\begin{lemma}\label{lem:maybe-func-set}
+	Assuming that $R$ is a symmetric AM simulation over an $F$-coalgebra $(X,\alpha)$ that $FX=X+1$, then for every $(x_1,x_2)\in R$ either
+	\begin{gather*}
+		\alpha(x_1),\alpha(x_2)\in X,
+	\end{gather*} 
+	or
+	\begin{gather*}
+		\alpha(x_1)=\alpha(x_2)=\bot.
+	\end{gather*}
+\end{lemma}
+\begin{proof}
+	We assume that $\sigma\c R\to R+1$ is the witness that we have for $R$ to be an AM-simulation. We prove the statement by contradiction. If the statement is false, then we either have 
+	\begin{gather*}
+		\alpha(x_1)\in X\quad\&\quad \alpha(x_2)=\bot,
+	\end{gather*}
+	or
+	\begin{gather*}
+		\alpha(x_1)=\bot\quad\&\quad \alpha(x_2)\in X.
+	\end{gather*}
+	Assuming $\alpha(x_1)\in X\;\&\; \alpha(x_2)=\bot$, then since $R$ is an AM-simulation, by~\eqref{eq:diag-lax-sim}$(p_2+1)\comp \sigma(x_1,x_2)\appr\alpha(x_2)$, we have $(p_2+1)\comp \sigma(x_1,x_2)=\bot$ that entails $\sigma(x_1,x_2)=\bot$. So, we have $(p_1+1)\comp \sigma(x_1,x_2)=\bot$, while $\alpha(x_1)\not\sqsubseteq\bot$ that means that $\sigma$ is not a witness for $R$ to be an AM-simulation.\textreferencemark
+	
+	Assuming $\alpha(x_1)=\bot\;\&\; \alpha(x_2)\in X$, since $R$ is reflexive, then we have $(x_2,x_1)\in R$ as well. So, by~\eqref{eq:diag-lax-sim} we have $(p_2+1)\comp \sigma(x_2,x_1)\appr\alpha(x_1)$ that entails $\sigma(x_2,x_1)=\bot$. So, we have $(p_1+1)\comp\sigma(x_2,x_1)=\bot$, while  $\alpha(x_2)\not\sqsubseteq\bot$ that means that $\sigma$ is not a witness for $R$ to be an AM-simulation.\textreferencemark\qed
+\end{proof}
+
+\begin{prop}
+	For a $F$-coalgebra $(X,\alpha)$ in $\Set$, such that $FX=X+1$, a symmetric AM-simulation relation $R$ on $X$ is an AM-bisimulation.
+\end{prop}
+\begin{proof}
+	By~\autoref{lem:maybe-func-set} for every $(x_1,x_2)\in R$, we either have 
+	\begin{gather*}
+		\alpha(x_1)=\bot\quad\&\quad \alpha(x_2)=\bot,
+	\end{gather*}
+	or
+	\begin{gather*}
+		\alpha(x_1)\in X\quad\&\quad \alpha(x_2)\in X.
+	\end{gather*}
+	We define $\beta$ as a witness for $R$ to be an AM-bisimulation as follows:
+	\begin{gather*}
+		\beta(x_1,x_2)=
+		\begin{cases} 
+			\bot & \alpha(x_1)=\bot\;\&\; \alpha(x_2)=\bot  \\
+			(\alpha(x_1),\alpha(x_2)) & \alpha(x_1)\in X\;\&\;\alpha(x_2)\in X
+		\end{cases}
+	\end{gather*}
+	Assuming $\alpha(x_1)=\bot\;\&\; \alpha(x_2)=\bot$ we have $(p_i+1)\comp\beta(x_1,x_2)=\bot=\alpha(x_i)$, and assuming $\alpha(x_1)\in X\;\&\;\alpha(x_2)\in X$ we have $(p_i+1)\comp\beta(x_1,x_2)=\alpha(x_i)\in X$.\qed
+\end{proof}
+
 \section{Relators}
 \subsection{Two-way similarity in Hughes-Jacobs}
 Hughes and Jacobs define two-way similarity as $\leq\cap\leq^\op$. They give a sufficient condition for the two-way similarity to be the bisimilarity. We discuss that this condition does not allow us to say that a symmetric simularity is a bisimilarity. The condition is: