Hackfixes to get changebar right

1 files changed, 9 insertions, 7 deletions

diff --git a/Assignment1/conversion.tex b/Assignment1/conversion.tex
index 1138e11..fe9b136 100644
--- a/Assignment1/conversion.tex
+++ b/Assignment1/conversion.tex
@@ -10,7 +10,7 @@ This algorithm is described in more detail below.
 \label{pltl:to-ltl:syntactic}
 The syntactic algorithm as proposed by Gabbay has its foundation in the following three facts:%
 	\footnote{%
-		Note that Gabbay used a slightly different, \enquote{non-strict} definition for the $\Uop$ and $\Sop$ operators.
+		Gabbay used a slightly different, \enquote{non-strict} definition for the $\Uop$ and $\Sop$ operators.
 		\camil
 		We then get $\sigma \vDash_i \phi_1 \Uop \phi_2 \Leftrightarrow \exists_{j > i}[\sigma \vDash_j \phi_2]$ and $\sigma \vDash_k \phi_1$ for all $i < k < j$ (rather than $i \le k < j$), and similarly for $\Sop$.
 		Thus, our $\phi \Uop \psi$ is equivalent to Gabbay's $\psi \lor \phi \land \phi \Uop \psi$.
@@ -92,9 +92,10 @@ For the proofs of the equivalences, we refer the reader to the appendix of \cite
 	\end{align*}
 	The reasoning behind the other elimination rules is similar and will not be discussed in detail.
 \end{remark}
+\cbend
 
-\erin
 \begin{enumerate}[resume]
+	\erin
 	\item Suppose $E = (q \lor \alpha\Uop\beta) \Sop a$, then $E \equiv E_1 \vee E_2 \vee E_3$ where:
 		\begin{align*}
 			E_1 &= \bot \Sop a\\
@@ -142,16 +143,17 @@ For the proofs of the equivalences, we refer the reader to the appendix of \cite
 			E_2 &= (\neg a \vee \alpha \Uop \beta) \Sop (\neg q \wedge \alpha \Uop \beta \wedge \neg a)\\
 			E_3 &= (\neg a \vee \alpha \Uop \beta) \Sop (\neg q \wedge \alpha \Uop \beta)
 		\end{align*}
+
 		\camil
-		Since $\sigma \vDash_i E_2$ entails $\sigma \vDash_i E_3$ for all $i\in\mathbb N$, we also have $E \equiv \neg(E_1 \lor E_3)$.\cbend%
-			\footnote{\cbcolor{red}\cbstart
+		Since $\sigma \vDash_i E_2$ entails $\sigma \vDash_i E_3$ for all $i\in\mathbb N$, we also have $E \equiv \neg(E_1 \lor E_3)$.%
+			\footnote{%
 				According to \citet[p.~439]{Gabbay1989}, $E_3$ is \enquote{subsumed by} $E_2$.
-				Assuming the straightforward understanding of subsumption ($\phi$ subsumes $\psi$ if and only if $\textsl{Words}(\phi) \supseteq \textsl{Words}(\psi)$), this is incorrect and $E_2$ is subsumed by $E_3$ instead.\cbend}
+				Assuming the straightforward understanding of subsumption ($\phi$ subsumes $\psi$ if and only if $\textsl{Words}(\phi) \supseteq \textsl{Words}(\psi)$), this is incorrect and $E_2$ is subsumed by $E_3$ instead.}
 		The term\erin\ $E_3$ (and $E_2$) can be further eliminated, in particular using elimination 5.
-		\cbend{}
+		\cbend
 \end{enumerate}
-\erin
 
+\erin
 Note that these rules can only be applied when a $\Uop$ is within the scope of a $\Sop$.
 In order to move an $\Sop$ out of the scope of a $\Uop$, consider that $\Sop$ and $\Uop$ are symmetrical.
 The above equivalences also hold when the path is reversed, so similar elimination rules exist for the case that $\Sop$ occurs within the scope of $\Uop$.