Commit 7f79f2c1 authored by Glen Mével's avatar Glen Mével
Browse files

ICFP21 paper: fix spacing around logical connectives

parent e2e75b32
......@@ -104,7 +104,7 @@
\displaystyle\Sep_{\head-\capacity \leq \idx < \tail}&
% cell bearing no value, available for next round:
\emptyCell \idx {\nthStatusView{\modcap\idx}}
&\lor&
&{}\LOR{}&
% cell being emptied by a dequeuer:
\status_{\modcap\idx} = 2\idx + 1
% NOTE: here we can add 0 ≤ i to the invariant, but it is unneeded
......@@ -113,7 +113,7 @@
% cell bearing a value:
%\fullCell \idx {\nthStatusView{\modcap\idx}} {\nthElemView{\idx-\tail}}
\fullCell \idx {\nthStatusView{\modcap\idx}} {\nthElemView\idx}
&\lor&
&{}\LOR{}&
% cell being filled with a value by an enqueuer:
\status_{\modcap\idx} = 2\idx
\end{array}% end of array used to align the two big-stars
......
......@@ -63,9 +63,9 @@ Formally, the two assertions satisfy the following properties:
\ISEP \isQueue {\tview'} {\hview'} \elemViewListB
}{%
\tview = \tview'
\land \hview = \hview'
\land \Forall i. \elem = \elem'_i
\land \eview_i = \eview'_i
\LAND \hview = \hview'
\mathlop{\mathord\land \Forall i.} \elem = \elem'_i
\LAND \eview_i = \eview'_i
}
\infer{%
......@@ -515,7 +515,6 @@ capture the essence of logical atomicity, and to understand our proof, is:
\[\begin{array}{rcl}%
\lahoare<x>{P}{e}{\pred}
&\eqdef&
\delimiterfactor = 1200
\Forall \predB,
\left[ \pvs[\top][\emptyset] \Exists x.
P \ISEP \left(\Forall v. \pred\;v \WAND\pvs[\emptyset][\top] \predB\;v\right)
......@@ -641,7 +640,7 @@ for slot~$\modcap{\idx-\capacity}$:
%
\[%
\fullCell {(\idx-\capacity)} {\nthStatusView{\modcap{\idx-\capacity}}} {\nthElemView{\idx-\capacity}}
\;\lor\;
\LOR
\status_{\modcap{\idx-\capacity}} = 2(\idx-\capacity)
\]%
%
......@@ -649,7 +648,7 @@ Because $\modcap{\idx-\capacity} = \modcap\idx$, this implies:
%
\[%
\status_{\modcap\idx} = 2(\idx-\capacity) + 1
\;\lor\;
\LOR
\status_{\modcap\idx} = 2(\idx-\capacity)
\]%
%
......@@ -667,7 +666,7 @@ that the invariant gives us:
%
\[%
\emptyCell {(\idx-\capacity)} {\nthStatusView{\modcap{\idx-\capacity}}}
\;\lor\;
\LOR
\status_{\modcap{\idx-\capacity}} = 2(\idx-\capacity)+1
\]%
%
......@@ -722,7 +721,7 @@ The invariant then gives us for slot~$\modcap\idx$:
%
\[%
\fullCell \idx {\nthStatusView{\modcap\idx}} {\nthElemView\idx}
\;\lor\;
\LOR
\status_{\modcap\idx} = 2\idx
\]%
%
......@@ -737,7 +736,7 @@ We then switch to the left disjunct, by constituting the assertion:
%
\[%
\fullCell \idx {\pair{\status^2}{\sview^2}} {\pair\elem\eview}
\iequiv
\;\iequiv\;
\isepV{%
\status^2 = 2\idx + 1
\cr (\nthpointstoNA\refelements{\modcap\idx}{\elem}) \opat \sview^2
......
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment