From 1900da7ed75215e49df5245b85c7fc32bae7bf0c Mon Sep 17 00:00:00 2001 From: partowp Date: Tue, 4 Aug 2026 20:30:40 +0100 Subject: [PATCH] PF --- draft/draft.tex | 14 +++++++++++++- 1 file changed, 13 insertions(+), 1 deletion(-) diff --git a/draft/draft.tex b/draft/draft.tex index 719546c..36a2a03 100644 --- a/draft/draft.tex +++ b/draft/draft.tex @@ -2340,7 +2340,7 @@ Indeed, $\sigma^\dagger$ is a witness for $R$ to be an HJ-simulation, but it is \end{gather*} \end{example} -\subsection{The concrete proof} +\subsection{From Symmetric Simulation To Bisimulation (Span-based)} %\begin{lemma}\label{lem:sim-opsim-inc1}\ppnote{Actually, this lemma holds for every functor in an arbitrary category.} % Assuming that $\sigma\c R\to\powf R$ is witness for a 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*)] @@ -2416,6 +2416,7 @@ We define $\join$ on each $\Hom(X,\powf Y)$ for every sets $X$ and $Y$: %\begin{proof} % \todo{Finish.} %\end{proof} +\subsection{Powerset Functor} \begin{lemma}\label{lem:proj-dist-set} For relations $R_1$ and $R_2$ the following equation holds: \begin{gather*} @@ -2482,6 +2483,17 @@ Now, we prove our main statement. Considering~\autoref{prop:alph-prod}, assuming that $R$ is a symmetric relation and it is an AM simulation, then $R$ is an AM bisimulation as well. \end{cor} Now, we make the proof more abstract. We prove the statement for set-functors of the form $\powf F$, where $F$ is an arbitrary set-functor, and $\powf$ is the powerset functor. + +\subsection{PF} +\begin{lemma}\label{lem:proj-dist-set-abs} + For sets $X$ and $Y$ in $\powf A$, and a function $f\c A\to B$ the following equation holds: + \begin{gather*} + %(\powf p_i)^\dagger(R_1\cup R_2)=(\powf p_i)^\dagger(R_1)\cup(\powf p_i)^\dagger(R_2) + \powf f(X\cup Y)=\powf f(X)\cup(\powf f)(Y) + \end{gather*} +\end{lemma} +\todo{Finish this proof. With this, you can give the proof for $\powf F$. After you finished this, you can remove the previous sections.} + \subsection{Maybe Functor} We prove that symmetric simulation is a bisimulation for the case that $FX=X+1$. First, we prove it for $\Set$.\\ Proven by Dubut, for every AM-simulation relation over a coalgebra $(X,\alpha)$ of a functor with a liftable order, we have a witness $\sigma\c R\to R+1$ such that $\alpha\comp p_1=Fp_1\comp\sigma$. We have shown that the ordering on the maybe functor is liftable and coliftalbe in~\autoref{prop:maybe-lif} and~\autoref{prop:maybe-colif}