added missing comma in LF invariant.

Author: MatteP1

presentation/presentation.pdf

@@ -1367,7 +1367,7 @@ \section{Proving that the Lock-Free Michael-Scott Queue Satisfies the HOCAP-styl
         \begin{align*}
           &\LFQueueInvariantHocap(\lochead, \loctail, \Qg) \eqdef\\
           &\Exists \absvalueList. \abstractstateauth{\Qg.\gabst}{\absvalueList} \star{}\\
-          &\Exists \xsc, \xsqueue, \nodehead, \nodetail \nodelast .\\
+          &\Exists \xsc, \xsqueue, \nodehead, \nodetail, \nodelast .\\
           &\xsc = \xsqueue \catenate [\nodehead] \star{}\\
           &\isLL(\xsc) \star{}\\
           &\isLast(\nodelast, \xsc) \star{}\\

presentation/presentation.tex

@@ -2419,7 +2419,7 @@ \section{HOCAP-style Queue Predicate}
   \begin{align*}
     &\LFQueueInvariantHocap(\lochead, \loctail, \Qg) \eqdef\\
     &\Exists \absvalueList. \abstractstateauth{\Qg.\gabst}{\absvalueList} \star{} &&\text{(abstract state)}\\
-    &\Exists \xsc, \xsqueue, \nodehead, \nodetail \nodelast . &&\text{(concrete state)}\\
+    &\Exists \xsc, \xsqueue, \nodehead, \nodetail, \nodelast . &&\text{(concrete state)}\\
     &\xsc = \xsqueue \catenate [\nodehead] \star{}\\
     &\isLL(\xsc) \star{}\\
     &\isLast(\nodelast, \xsc) \star{}\\