From 4ac3b6337f065fee93398757dfc3dc6b885eafce Mon Sep 17 00:00:00 2001
From: Ralf Jung <jung@mpi-sws.org>
Date: Tue, 16 Aug 2016 10:45:50 +0200
Subject: [PATCH] docs: fix typo in namespaces
---
docs/derived.tex | 2 +-
1 file changed, 1 insertion(+), 1 deletion(-)
diff --git a/docs/derived.tex b/docs/derived.tex
index 38674cb70..25cb02046 100644
--- a/docs/derived.tex
+++ b/docs/derived.tex
@@ -273,7 +273,7 @@ From~\ruleref{pvs-update}, \ruleref{vs-update} and the frame-preserving updates
\subsection{Invariant identifier namespaces}
-Let $\namesp \ni \textlog{InvNamesp} \eqdef \textlog{list}(\textlog{InvName})$ be the type of \emph{namespaces} for invariant names.
+Let $\namesp \in \textlog{InvNamesp} \eqdef \textlog{list}(\textlog{InvName})$ be the type of \emph{namespaces} for invariant names.
Notice that there is an injection $\textlog{namesp\_inj}: \textlog{InvNamesp} \ra \textlog{InvName}$.
Whenever needed (in particular, for masks at view shifts and Hoare triples), we coerce $\namesp$ to its suffix-closure: \[\namecl\namesp \eqdef \setComp{\iname}{\Exists \namesp'. \iname = \textlog{namesp\_inj}(\namesp' \dplus \namesp)}\]
We use the notation $\namesp.\iname$ for the namespace $[\iname] \dplus \namesp$.
--
GitLab