lemma

draft/draft.tex

@@ -2207,14 +2207,11 @@ Now, we prove that the given order on the maybe functor is a liftable one.
 \end{proof}
 So, proven by Dubut, for every symmetric AM-simulation relation over a coalgebra $(X,\alpha)$ of the maybe functor, we have a witness $\sigma\c R\to R+1$ such that $\alpha\comp p_1=(p_1+1)\comp\sigma$.
 \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
+	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$ 
 	\begin{gather*}
-		\alpha(x_1),\alpha(x_2)\in X,
+		\alpha(x_1)\in X\Rightarrow \alpha(x_2)\in X\\
+		\alpha(x_1)=\bot \Rightarrow \alpha(x_2)=\bot
 	\end{gather*} 
-	or
-	\begin{gather*}
-		\alpha(x_1)=\alpha(x_2)=\bot.
-	\end{gather*}
 \end{lemma}
 \begin{proof}
 	By~\autoref{prop:alph-prod-dubut} and~\autoref{lem:maybe-lif} there exists $\sigma\c R\to R+1$ that is a witness for $R$ to be an AM-simulation, and $p_1+1\comp\sigma=\alpha\comp p_1$. Since $R$ is symmetric, for every $(x_1,x_2)\in $ we have the following:
@@ -2317,7 +2314,7 @@ So, we have the following:
 \begin{gather*}
 	R\iso R_{X^2}+R_{2\times X}+R_{1}
 \end{gather*}
-And now we can use $q_2+r_2+s_2\c R_{X^2}+R_{2\times X}+R_{1}\to X^2+(2\times X)+1$ instead of $\brks{\alpha\comp p_1,\alpha\comp p_2}$. To prove~\autoref{lem:maybe-func-set} abstractly is to prove that $q_2+r_2+s_2$ factors through $X^2+1$. To achieve this, we need to show that $R_{2\times X}\iso 0$. 
+And now we can use $q_2+r_2+s_2\c R_{X^2}+R_{2\times X}+R_{1}\to X^2+(2\times X)+1$ instead of $\brks{\alpha\comp p_1,\alpha\comp p_2}$. To prove~\autoref{lem:maybe-func-set} abstractly is to prove that $q_2+r_2+s_2$ factors through $X^2+1$. To achieve this, we need to show that $R_{2\times X}\iso 0$ that is indeed the abstraction of~\autoref{lem:maybe-func-set}. 
 \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: