1 files changed, 6 insertions, 2 deletions
diff --git a/Assignment1/conversion.tex b/Assignment1/conversion.tex
index 24be26d..3a08292 100644
--- a/Assignment1/conversion.tex
+++ b/Assignment1/conversion.tex
@@ -8,7 +8,7 @@ We will explain more about this algorithm once we get to it.
 
 \erin
 \paragraph{Syntactic Algorithm}
-The syntactic algorithm as proposed by Gabby has its foundation in the following three facts:
+The syntactic algorithm as proposed by Gabby has its foundation in the following three facts\footnote{Note that Gabbay used a slightly different definition for the $\Uop$ and $\Sop$ operators. For this paragraph of the book we will assume $\phi \Uop \psi := \Xop (\phi \Uop \psi)$ and $\phi \Sop \psi := \Xop^{-1} (\phi \Sop \psi)$. For a given formula, it is not hard to convert it to this form.}:
 \begin{enumerate}
 	\item Every PLTL formula can be written using only the $\Sop$ and $\Uop$ operators.
 	\item Every formula containing only the $\Sop$ and $\Uop$ operators can be written in the following form: $F \cup P \cup A$ where $F$ are the future modalities ($\Uop$), $P$ are the past modalities ($\Sop$), and $A$ are the atomic expressions.
@@ -41,7 +41,6 @@ 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{enumerate}
 	\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*}
@@ -96,6 +95,11 @@ First, however, note that there are 8 possible cases where there is a $\Uop$ in
 		After elimination of $\Gop^{-1}$, this formula can be further eliminated.
 		In particular by using elimination 5.
 \end{enumerate}
+When considering these rules, it might be noted that they can only be applied when a $\Uop$ is within the scope of a $\Sop$.
+In order to move the $\Sop$ out of the scope of the $\Uop$ we need to consider that these formulas also hold when the path is reversed.
+I.e. we can also apply these eliminations when a $\Sop$ is within the scope of a $\Uop$.
+
+The final step of the algorithm entails removing the part of the formula that contains the $\Sop$-operators.
 
 \paragraph{Automata-based Algorithm}