From 92c7ba03c35a8bfc6ac709c94641490fa35beebe Mon Sep 17 00:00:00 2001 From: partowp Date: Sun, 14 Jun 2026 19:20:03 +0100 Subject: [PATCH] minor --- draft/draft.tex | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/draft/draft.tex b/draft/draft.tex index dda38ba..6b8c8c1 100644 --- a/draft/draft.tex +++ b/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)\\