diff options
Diffstat (limited to 'Assignment1/syntax.tex')
| -rw-r--r-- | Assignment1/syntax.tex | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/Assignment1/syntax.tex b/Assignment1/syntax.tex index 6d86281..ac2e13c 100644 --- a/Assignment1/syntax.tex +++ b/Assignment1/syntax.tex @@ -167,7 +167,7 @@ Before turning to the formal semantics in the next subsection, we provide some e However, the requirement \enquote{once red, the light cannot become green immediately} \emph{can} be expressed with past modalities. To rewrite it, consider that this requirements is equivalent to \enquote{if green, the light cannot have been red previously}. This yields the formula: - \[\square\left(\textsl{green} \rightarrow \lnot \Pop\textsl{red}\right) \qedhere\] + \[\square(\textsl{green} \rightarrow \lnot \Pop\textsl{red}) \qedhere\] \end{example} \begin{example}[A property for an Authentication System] |