This commit is contained in:
partowp
2026-07-15 15:38:16 +01:00
parent 58c3a32e87
commit c47a548df7
+1 -1
View File
@@ -2314,7 +2314,7 @@ So, proven by Dubut, for every AM-simulation relation over a coalgebra $(X,\alph
\Rightarrow&\sigma(x_2,x_1)=\bot,\\
\Rightarrow&p_1+1\comp\sigma(x_2,x_1)=\bot,\\
\Rightarrow&\alpha(x_2)=\bot,&\eqref{eq:maybe-func-set-2}\\
\Rightarrow&\alpha(x_2)=p_1+1\comp\sigma(x_1,x_2)\bot.
\Rightarrow&\alpha(x_2)=p_1+1\comp\sigma(x_1,x_2).
\end{align*}
\end{itemize}\qed
\end{proof}