PF

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}