minor

draft/draft.tex

@@ -1848,7 +1848,7 @@ We recall that in the above diagram $\sigma_3$ is a bisimulation, and the rest a
 %\end{proof}
 \subsection{The concrete proof}
 \begin{lemma}\label{lem:sim-opsim-inc}
-	Assuming that $\sigma\c R\to\powf R$ is a simulation structure, and $R$ is symmetric, then for all $(x_1,x_2)\in R$ we have:
+	Assuming that $\sigma\c R\to\powf R$ is witness for the symmetric relation $R$ to be an AM simulation on $\powf$-coalgebra $(X,\alpha)$, then for all $(x_1,x_2)\in R$ we have:
 	\begin{enumerate}[label=(\Roman*), ref=(\Roman*)]
 		\item $\powf p_1\comp\powf s\comp\sigma\comp s(x_1,x_2)\subseteq \powf p_1\comp\sigma(x_1,x_2)$\label{item:sim-opsim-inc:I}
 		\item $\powf p_2\comp\sigma(x_1,x_2)\subseteq \powf p_2\comp\powf s\comp\sigma\comp s(x_1,x_2)$\label{item:sim-opsim-inc:II}
@@ -1868,7 +1868,7 @@ We recall that in the above diagram $\sigma_3$ is a bisimulation, and the rest a
 	\end{align*}
 	So, from $\alpha(x_1)\subseteq\powf p_1\comp\sigma(x_1,x_2)$ we have $\powf p_1\comp\powf s\comp\sigma\comp s(x_1,x_2)\subseteq \powf p_1\comp\sigma(x_1,x_2)$.
 	
-	Furthermore, from $\alpha(x_1)\subseteq\powf p_1\comp\sigma(x_1,x_2)$ we get $\alpha(x_2)\subseteq\powf p_1\comp\sigma(x_2,x_1)$, where 
+	Furthermore, from $\alpha(x_1)\subseteq\powf p_1\comp\sigma(x_1,x_2)$ by the symmetry of $R$ we have $(x_2,x_1)\in R$, so we get $\alpha(x_2)\subseteq\powf p_1\comp\sigma(x_2,x_1)$, where 
 	\begin{align*}
 		\powf p_1\comp\sigma(x_2,x_1)&\\
 		&=\powf p_1\comp\sigma\comp s(x_1,x_2)\\