From a5f94780633073536a6934f9e53d6c2acdbb7503 Mon Sep 17 00:00:00 2001
From: Jacques-Henri Jourdan <jacques-henri.jourdan@normalesup.org>
Date: Wed, 12 Oct 2016 14:43:48 +0200
Subject: [PATCH] Correct the Inv-alloc rule.
---
docs/program-logic.tex | 2 +-
1 file changed, 1 insertion(+), 1 deletion(-)
diff --git a/docs/program-logic.tex b/docs/program-logic.tex
index d6d711649..354d342f7 100644
--- a/docs/program-logic.tex
+++ b/docs/program-logic.tex
@@ -434,7 +434,7 @@ We can now derive the following rules (this involves unfolding the definition of
\begin{mathpar}
\axiomH{inv-persist}{\knowInv\namesp\prop \proves \always\knowInv\namesp\prop}
- \axiomH{inv-alloc}{\later\prop \proves \pvs[\namesp] \knowInv\namesp\prop}
+ \axiomH{inv-alloc}{\later\prop \proves \pvs[\bot] \knowInv\namesp\prop}
\inferH{inv-open}
{\namesp \subseteq \mask}
--
GitLab