Change the pipeline invariant according to its Coq proof.

papers/icfp2021/figure-pipeline-inv.tex

@@ -35,12 +35,12 @@
 %\multicolumn{3}{r}{%
 
       \left\{\begin{array}{l}
-          \Exists \curf, \curg, \yElemViewListInv<\curg><\curf>*[].
+          \Exists \curf, \curg, \tview, \hview, \yElemViewListInv<\curg><\curf>*[].
       \\  \quad \ISep{%
                   \curg \leq \curf
             \isep \ownGhost \gcurf {\authfull \curf}
             \isep \ownGhost \gcurg {\authfull \curg}
-            \cr   \isQueue \emptyview \emptyview {\yElemViewListInv<\curg><\curf>}
+            \cr   \isQueue \tview \hview {\yElemViewListInv<\curg><\curf>}
             \cr   \displaystyle\Sep_{\curg \leq \idx < \curf}
                     \left(\wpre {g\;\yElem_\idx} {\Lam z. R\;\idx\;z}\right) \opat \view_\idx
           }%end of the main \ISep of the invariant