lem

draft/draft.tex

@@ -1781,13 +1781,19 @@ We define $\join$ and $\meet$ on morphisms as follows:
 	\end{gather*}
 \end{cor}
 
+\begin{lemma}
+	For every $S\in \mathcal{P}R$,
+	\begin{gather*}
+		((\mathcal{P}p_1)^\dagger(S),(\mathcal{P}p_2)^\dagger(S))\in(\mathcal{P}R)^\dagger\Leftrightarrow(\mathcal{P}p_1)(S)\subseteq(\mathcal{P}p_1)(R),(\mathcal{P}p_2)(S)\subseteq(\mathcal{P}p_2)(R)
+	\end{gather*}
+\end{lemma}
 \begin{lemma}\label{lem:alph-prod}
 	Assuming that $R$ is a symmetric relation, and $S\neq\emptyset$ is the set of all simulation structures of the type $R\to (\mathcal{P}R)^\dagger$, then there there exists a simulation structure $\sigma\in S$ that for every $(x_1,x_2)$,  $(\mathcal{P}p_1)^\dagger\comp\sigma(x_1,x_2)=\alpha(x_1)$. 
 \end{lemma}
 \begin{proof}
 	Since $S\neq\emptyset$ there exists $\delta\in S$. We define $\sigma$ for every $(x_1,x_2)$ as the following:
 	\begin{gather*}
-		\sigma(x_1,x_2)=\alpha(x_1)\times (\mathcal{P}p_2)^\dagger\comp\delta(x_1,x_2)
+		\sigma(x_1,x_2)=(\alpha(x_1), (\mathcal{P}p_2)^\dagger\comp\delta(x_1,x_2))
 	\end{gather*}
 	We have $\sigma(x_1,x_2)\in(\mathcal{P}R)^\dagger$, as $\alpha(x_1)\subseteq\mathcal{P}p_1(R)$ and $(\mathcal{P}p_2)^\dagger\comp\delta(x_1,x_2)\subseteq\mathcal{P}p_2(R)$ are inherited from $\delta$ being a simulation structure.
 	Also, it obviously is a simulation as $(\mathcal{P}p_1)^\dagger\comp\sigma(x_1,x_2)=\alpha(x_1)$ and $(\mathcal{P}p_2)^\dagger\comp\sigma(x_1,x_2)\subseteq\alpha(x_2)$ as $(\mathcal{P}p_2)^\dagger\comp\delta(x_1,x_2)\subseteq\alpha(x_2)$. 
@@ -2012,6 +2018,12 @@ The above translation seems to be true in a more general case, where $\spa$ and
 		\hat{\relar}r=\relar r\cap (\relar(r^\op))^\op
 	\end{gather*}
 \end{definition}
+\begin{prop}
+	For every relator $\relar$, $\hat{\relar}$ is a relator.
+\end{prop}
+\begin{proof}
+	Almost obvious!\qed  
+\end{proof}
 \begin{prop}
 	Assuming that $\relar$ is a relator, and $r$ and $r^\op$ are both $\relar$-simulations from a coalgebra $\alpha\c X\to FX$ to a coalgebra $\beta\c Y\to FY$ and vice-versa respectively, then $r$ is also a $\hat{\relar}$-simulation.
 \end{prop}
@@ -2039,6 +2051,14 @@ The above translation seems to be true in a more general case, where $\spa$ and
 		&=(\hat{\relar}r)^\op
 	\end{align*}\qed
 \end{proof}
+
+\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}
+\begin{proof}
+	Assuming $y\; r^\op x$ we have $x\; r\; y$. Since $r$ is $\relar$-simulation we have $\alpha(x)\;\relar r\;\beta (y)$. So, we have $\beta(y)\;(\relar r)^\op\;\alpha(x)$, and since $\relar$ is symmetric we have $\beta(y)\;\relar r^\op\;\alpha(x)$.\qed
+\end{proof}
+
 \begin{definition}[Behavioural Equivalence]
 	Two states $x$ and $y$ of two coalgebras $(X,\alpha)$ and $(Y,\beta)$ are behaviourally equivalent iff there exist a coalgebra $(Z,\gamma)$ and coalgebra morphisms $f\c(X,\alpha)\to(Z,\gamma)$ and $g\c(Y,\beta)\to(Z,\gamma)$ such that $f(x)=g(y)$. The relation $r$ consisting of all behaviourally equivalent states of these two coalgebras is called behavioural equivalence.
 \end{definition}
@@ -2047,10 +2067,14 @@ The above translation seems to be true in a more general case, where $\spa$ and
 	A relation $r\c X\rto Y$ is difunctional iff there are functions $f\c X\to Z$ and $g\c Y\to Z$ such that for every $(x,y)\in R$ we have $f(x)=g(y)$.
 \end{definition}
 
-\begin{definition}[Soundness and Completeness of Relators]
+\begin{definition}[Soundness and Completeness of $\relar$-similarity]
-	A relator $\relar$ is sound iff the $\relar$-similarity from a coalgebra $(X,\alpha)$ to a coalgebra $(Y,\beta)$ is less than or equal to their behavioural equivalence, and it is complete iff it is greater than or equal to their behavioural equivalence.
+	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}
@@ -2059,9 +2083,25 @@ The above translation seems to be true in a more general case, where $\spa$ and
 	\end{enumerate}\qed
 \end{thm}
 
-\begin{prop}
+\begin{prop}\label{prop:difunc-preser}
-	$\hat{\relar}$ is sound and complete.
+	Assuming that $\relar$ is a $F$-relator that preserves difunctional relations, then $\hat{\relar}$ does the same.
 \end{prop}
+\begin{proof}
+	Assuming $r$ is difunctional, then there exist $f_1,f_2\c FX\to FZ$ and $g_1,g_2\c FY\to FZ$ such that $p\;\relar r\;q$ iff $f_1(p)=g_1(q)$ and $q \;\relar r^\op \;p$ iff $f_2(p)=g_2(q)$. By the definition of $\hat{\relar}$ we have $p\;\hat{\relar}r\;q$ iff $p\;\relar r\;q$ and $p\;(\relar r^\op)^\op\;q$ that is equivalent to say that $\brks{f_1,f_2}(p)=\brks{g_1,g_2}(q)$.\qed
+\end{proof}
+\begin{cor}
+	Assuming that $\relar$ is a $F$-relator that preserves difunctional relations, for every symmetric relation $r$ we have $\hat{\relar}r=\relar r$.
+\end{cor}
+\begin{proof}
+	$\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}
 \end{document}