First two separation rules

1 files changed, 24 insertions, 1 deletions

diff --git a/Assignment1/conversion.tex b/Assignment1/conversion.tex
index 9e39283..2ed3e47 100644
--- a/Assignment1/conversion.tex
+++ b/Assignment1/conversion.tex
@@ -33,7 +33,30 @@ This rewrite system is given in Figure~\ref{fig:rewrite}.
 	\caption{The rewrite rules for writing any PLTL formula as a formula containing only $\Sop$ and $\Uop$.}
 	\label{fig:rewrite}
 \end{figure}
-This full expressiveness of $\Uop$ and $\Sop$ is proven in theorem 2.3 of the paper by Gabbay~\cite{Gabbay1989}.
+This full expressiveness of $\Uop$ and $\Sop$ is proven in the PhD. thesis of J. Kamp~\cite{Kamp1968},
+and again by Gabbay using a different method~\cite{Gabbay1989}.
+
+Step 2 of the algorithm entails rewriting the formula containing only $\Uop$ and $\Sop$ to a form where there is no $\Sop$ in the scope of a $\Uop$,
+and there exists on $\Uop$ in the scope of a $\Sop$.
+Gabby proofs that this can by done in Theorem 2.4 of his paper,
+the rewrite rules are given in the Appendix of the same paper.
+In this book, we will not proof that these rewrite rules hold, but they are given below.
+First, however, note that there are 8 possible cases where there is a $\Uop$ in the scope of a $\Sop$.
+\begin{itemize}
+	\item Suppose $E = q \Sop a \wedge (\alpha \Uop \beta))$ then it holds that $E = E_1 \vee E_2 \vee E_3$ if:
+	\begin{align*}
+		E_1 &= (q \Sop a) \wedge (\alpha \Sop a) \wedge \alpha (\alpha \Uop \beta)\\
+		E_2 &= \beta \wedge (\alpha \Sop a) \wedge (q \Sop a)\\
+		E_3 &= q \Sop \beta \wedge q \wedge (\alpha \Sop a) \wedge (q \Sop a)
+	\end{align*}
+
+	\item Suppose $E = q \Sop a \wedge \neg (a \Uop \beta)$ then it holds that $E = E_1 \vee E_2 \vee E_3$ if:
+		\begin{align*}
+			E_1 &= (a \wedge \neg \beta \Sop a) \wedge \neg \beta \wedge \neg (\alpha \Uop \beta)\\
+			E_2 &= \neg \beta \wedge \neg \alpha \wedge (\neg \beta \wedge q \Sop a)\\
+		E_3 &= a\Sop\neg\beta \wedge \neg \alpha \wedge q \wedge (q \wedge \neg\beta \Sop a)
+		\end{align*}
+\end{itemize}
 
 \paragraph{Automata-based Algorithm}