From fa4cfb928d507fb0d596cf4c70b0ec24f35e2dc8 Mon Sep 17 00:00:00 2001
From: Jacques-Henri Jourdan <jacques-henri.jourdan@normalesup.org>
Date: Wed, 3 Mar 2021 08:09:20 +0100
Subject: [PATCH] Change the pipeline invariant according to its Coq proof.
---
papers/icfp2021/figure-pipeline-inv.tex | 4 ++--
1 file changed, 2 insertions(+), 2 deletions(-)
diff --git a/papers/icfp2021/figure-pipeline-inv.tex b/papers/icfp2021/figure-pipeline-inv.tex
index e425ff4..f44c5d7 100644
--- a/papers/icfp2021/figure-pipeline-inv.tex
+++ b/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
--
GitLab