diff options
Diffstat (limited to 'Assignment1')
| -rw-r--r-- | Assignment1/conversion.tex | 12 |
1 files changed, 6 insertions, 6 deletions
diff --git a/Assignment1/conversion.tex b/Assignment1/conversion.tex index e42d967..9e39283 100644 --- a/Assignment1/conversion.tex +++ b/Assignment1/conversion.tex @@ -23,12 +23,12 @@ This rewrite system is given in Figure~\ref{fig:rewrite}. \begin{figure} \centering \begin{alignat*}{2} - &\Pop\phi &&\leftrightarrow \phi \Sop \bot\\ - &\Xop\phi &&\leftrightarrow \phi \Uop \bot\\ - &\Gop\phi &&\leftrightarrow \neg (\neg \phi \Uop \top)\\ - &\Fop\phi &&\leftrightarrow \phi \Uop \top\\ - &\Gop^{--1}\phi &&\leftrightarrow \neg (\neg \phi \Sop \top)\\ - &\Fop^{--1}\phi &&\leftrightarrow \phi \Sop \top + &\Pop\phi &&\leftrightarrow \bot \Sop \phi\\ + &\Xop\phi &&\leftrightarrow \bot \Uop \phi\\ + &\Gop\phi &&\leftrightarrow \neg (\top \Uop \neg \phi)\\ + &\Fop\phi &&\leftrightarrow \top \Uop \phi\\ + &\Gop^{--1}\phi &&\leftrightarrow \neg (\top \Sop \neg \phi)\\ + &\Fop^{--1}\phi &&\leftrightarrow \top \Sop \neg \end{alignat*} \caption{The rewrite rules for writing any PLTL formula as a formula containing only $\Sop$ and $\Uop$.} \label{fig:rewrite} |