ACfull proof

draft/draft.tex

@@ -2038,6 +2038,7 @@ The above translation seems to be true in a more general case, where $\spa$ and
 \begin{remark}
 	If we want to have the previous corollary for two different coalgebras $\alpha\c X\to FX$ and $\beta\c X\to FX$, we need to assume that $r^\op$ is also a $\relar$-simulation from $\beta$ to $\alpha$. 
 \end{remark}
+
 \begin{prop}
 	$\hat{\relar}$ is a symmetric relator, i.e., every $\hat{\relar}$-simulation is actually a $\hat{\relar}$-bisimulation.
 \end{prop}
@@ -2053,6 +2054,16 @@ The above translation seems to be true in a more general case, where $\spa$ and
 	\end{align*}\qed
 \end{proof}
 
+\begin{prop}
+	Assuming that $\relar$ is a symmetric relator, and $r$ is a $\relar$-simulation from a coalgebra $(X,\alpha)$ to itself, then $r^\op_{s}$ is a $\relar$-simulation as well.
+\end{prop}
+\begin{proof}
+	It is easy to directly show that $r^\op$ is a $\relar$-simulation.\qed
+\end{proof}
+\begin{cor}
+		Assuming that $\relar$ is a symmetric relator, then the $\relar$-simularity from a coalgebra $(X,\alpha)$ to itself is a symmetric relation.
+\end{cor}
+
 \begin{prop}
 	Assuming that $\relar$ is a symmetric relator, then for every $r$ that is a $\relar$-simulation, $r^\op$ is also a $\relar$-simulation. 
 \end{prop}
@@ -2072,10 +2083,6 @@ The above translation seems to be true in a more general case, where $\spa$ and
 	For a relator $\relar$ the $\relar$-similarity from a coalgebra $(X,\alpha)$ to a coalgebra $(Y,\beta)$ is sound iff it is less than or equal to their behavioural equivalence, and it is complete iff it is greater than or equal to their behavioural equivalence.
 \end{definition}
 
-\begin{prop}
-	Assuming that $\relar$ preserves difunctional relations  
-\end{prop}
-
 \begin{thm}
 	Let $\relar$ be a relator for a functor $F$:
 	\begin{enumerate}
@@ -2097,13 +2104,6 @@ The above translation seems to be true in a more general case, where $\spa$ and
 	$\relar$-similarity being symmetric means that for the $f_1$, $f_2$, $g_1$ and $g_2$ in the proof of~\autoref{prop:difunc-preser}, we have $f_1=f_2$ and $g_1=g_2$.\qed
 \end{proof}
 
-\begin{prop}
-	Assuming that $\relar$-similarity is symmetric and complete, then $\hat{\relar}$-similarity from a coalgebra $\alpha\c X\to FX$ to itself is sound and complete.
-\end{prop}
-\begin{proof}
-	(Completeness): We show $\relar$-similarity with $r_s$ and $\hat{\relar}$-similarity with $r_{\hat{s}}$. Also, we show the behabioural equivalence with $r_b$. Since  
-\end{proof}
-
 Assuming that $\relar$-similarity is complete, does not guarantee that $\hat{\relar}$-similarity is sound and complete. We give a counter-example. Assuming that $\relar$ is a $\powf$-relator that takes $r\c X\rto Y$ to $\powf X\times \powf Y$, then $\hat{\relar} r= \powf X\times\powf Y$ as well. It means that for every coalgebras $(X,\alpha)$, $(Y,\beta)$, $\hat{\relar}$-similarity is equal to $X\times Y$, which is rare to be equal to behavioural equivalence. For example, if we take $X=\{x_1,x_2\}$ and $Y=\{y_1,y_2,y_3\}$, and we define $\alpha$ and $\beta$ as 
 \begin{gather*}
 	\alpha(x)=
@@ -2120,6 +2120,35 @@ Assuming that $\relar$-similarity is complete, does not guarantee that $\hat{\re
 	\end{cases}
 \end{gather*}
 then at least $(x_1,y_3)$ is not in the behavioural equivalence, while it is in $\hat{\relar}$-similarity.
+
+\begin{prop}
+	Assuming that $\relar$-similarity is symmetric and complete, then $\hat{\relar}$-similarity from a coalgebra $\alpha\c X\to FX$ to itself is sound and complete.
+\end{prop}
+\begin{proof}
+	(Completeness): We show $\relar$-similarity with $r_s$ and $\hat{\relar}$-similarity with $r_{\hat{s}}$. Also, we show the behabioural equivalence with $r_b$. Since  
+\end{proof}
+
+\begin{prop}
+	Assuming that $\relar$ is a $F$-relator ($F$ is a set functor), that for every functions $f\c X\to Z$ and $g\c Y\to Z$, we have $\relar(g^\op\comp f)\geq (Fg)^\op\comp Ff$, then $\hat{\relar}$-similarity is complete.
+\end{prop}
+\begin{proof}
+	We need to prove that for every functions $f\c X\to Z$ and $g\c Y\to Z$ we have $\hat{\relar}(g^\op\comp f)\geq (Fg)^\op\comp Ff$. By the assumption we have $\relar(g^\op\comp f)\geq(Fg)^\op\comp Ff$. Also, again from the assumption we have $\relar(f^\op\comp g)\geq(Ff)^\op\comp Fg$ that gives $(\relar(f^\op\comp g))^\op\geq(Fg)^\op\comp Ff$. So, we have $\hat{\relar}(g^\op\comp f)\geq F(g)^\op\comp Ff$.\qed
+\end{proof}
+\begin{prop}
+	Assuming that $\relar$ is a symmetric relator for a functor $F\c\Set\to\Set$, then the $\relar$-bisimilarity from a coalgebra $\alpha\c X\to FX$ to itself is sound, using the axiom of choice.
+\end{prop}
+\begin{proof}
+	We call the bisimilarity relation $r$, and we assume $x_1\;r\;x_2$, now we need to prove that $x_1$ and $x_2$ are behaviourally equivalent. We take $Z=X/r$, where $X/r=\{[x]\mid [x]=\{y\mid x\;r\;y\}\}$. Now, we define the coalgebra homomorphism $f\c X\to X/r$ as $f(x)=[x]$. So, assuming $x_1\;r\;x_2$ gives $f(x_1)=f(x_2)$. Now, assuming that exists a choice function $c\c X/r\to X$ that $c\comp f=\id_X$, we define $\gamma\c X/r\to F(X/r)$, as $\gamma([x])=Ff\comp\alpha\comp c([x])$. Now, we have
+	\begin{align*}
+		\gamma\comp f&\\
+		&=Ff\comp\alpha\comp c\comp f\\
+		&=Ff\comp\alpha.
+	\end{align*}
+	So, $x_1$ and $x_2$ are behaviourally equivalent. So, the $\relar$-bisimilarity is sound.\qed
+\end{proof}
+\begin{cor}
+	Assuming that a relator $\relar$ over a functor $F\c\Set\to\Set$ satisfies $\relar(g^\op\comp f)\geq (Fg)^\op\comp Ff$ for every functions $f\c X\to Z$ and $g\c Y\to Z$, then $\hat{\relar}$-bisimilarity from a coalgebra $\alpha\c X\to FX$ to itself is sound and complete, using the axiom of choice.
+\end{cor}
 \end{document}