Merge branch 'master' of git.wlog.site:pouya/coalgebraic-simulation

draft/draft.tex

@@ -2205,15 +2205,15 @@ Now, we prove that the given order on the maybe functor is a liftable one.
 		\item $h\in Y$: Since $h\appr Fg(k)$ and $h\neq\bot$, we have $h=Fg(k)$. In this case we take $k'=k$, so $k'\appr k$ and $Fg(k')=h$.\qed
 	\end{itemize}
 \end{proof}
+\begin{remark}
+	The mentioned order on the maybe functor is not coliftable.
+\end{remark}
 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=Fp_1\comp\sigma$.
 \begin{lemma}\label{lem:maybe-func-set}
-	Assuming that $R$ is a symmetric AM-simulation over an $F$-coalgebra $(X,\alpha)$ such 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,
-	\end{gather*} 
-	or
-	\begin{gather*}
-		\alpha(x_1)=\alpha(x_2)=\bot.
+		\alpha(x_1)\in X\Rightarrow \alpha(x_2)\in X\\
+		\alpha(x_1)=\bot \Rightarrow \alpha(x_2)=\bot
 	\end{gather*} 
 \end{lemma}
 \begin{proof}