bluh bluh

draft/draft.tex

@@ -2221,7 +2221,41 @@ We prove that symmetric simulation is a bisimulation for the case that $FX=X+1$.
 	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}
 
+Now, we give another proof for this functor. This proof is similar to the proof that we have given for the powerset functor.
 
+\begin{lemma}
+	The order structure on the set-functor $FX=X+1$ is a liftable order.
+\end{lemma}
+\begin{proof}
+	By~\autoref{lem:set-ord-str}, assuming $h\in\Hom(1,Y+1)$, $k\in\Hom(1,X+1)$, $g\c X\to Y$, and $h\appr (g+1)(k)$, we need to prove that exists $k'\in\Hom(1,X+1)$ such that $(g+1)(k')=h$. Since $h\in\Hom(1,Y+1)$ we have two cases:
+	\begin{itemize}
+		\item $h=\bot$: In this case we take $k'=\bot$, then we have $g+1(k')=\bot=h$.  
+		
+		\item $g+1(k)=h$: In this case we take $k'=k$, then we have $g+1(k')=h$, and they are both an element of $Y$.\qed
+	\end{itemize}
+\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{prop}\label{prop:sym-rel-bisim-may}
+	Assuming that $R$ is a symmetric relation, and $\sigma\c R\to R+1$ is a witness for $R$ to be a simulation, for which $(p_1+1)\comp\sigma=\alpha\comp p_1$, then the following morphism is a witness for $R$ to be a bisimulation:
+	\begin{gather*}
+		\sigma\join((s+1)\comp\sigma\comp s)
+	\end{gather*}
+\end{prop}
+\begin{proof}
+	For every $(x_1,x_2)\in R$ by~\autoref{lem:proj-dist-set} and~\autoref{lem:sim-opsim-inc}.\ref{item:sim-opsim-inc:I} we have 
+	\begin{gather*}
+		\powf p_1\comp(\sigma\join(\powf s\comp\sigma\comp s))(x_1,x_2)=
+		\powf p_1\comp\sigma(x_1,x_2).
+	\end{gather*}
+	%	and by~\autoref{lem:alph-prod}, 
+	Recall that $\powf p_1\comp\sigma(x_1,x_2)=\alpha(x_1)$. By~\autoref{lem:proj-dist-set} and~\autoref{lem:sim-opsim-inc}.\ref{item:sim-opsim-inc:II} we have
+	\begin{gather*}
+		\powf p_2\comp(\sigma\join(\powf s\comp\sigma\comp s))(x_1,x_2)=
+		\powf p_2\comp(\powf s\comp\sigma\comp s)(x_1,x_2).
+	\end{gather*}
+	Since $\powf p_1\comp\sigma=\alpha\comp p_1$ by precomposing $s$ to the both sides of the equation we get $\powf p_2\comp(\powf s\comp\sigma\comp s)=\alpha\comp p_2$. So, $\sigma\join(\powf s\comp\sigma\comp s)$ is a witness for $R$ to be an AM bisimulation.\qed
+\end{proof}
 
 \section{Relators}
 \subsection{Two-way similarity in Hughes-Jacobs}