From f97d8e588fb43d24258b8b9c07439eeb05486eaa Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Ale=C5=A1=20Bizjak?= <abizjak@cs.au.dk>
Date: Sun, 9 Oct 2016 14:08:29 +0200
Subject: [PATCH] Fixed typos in the definition of the interpretation of pvs.
---
docs/model.tex | 2 +-
1 file changed, 1 insertion(+), 1 deletion(-)
diff --git a/docs/model.tex b/docs/model.tex
index 41b545ca2..bb91207bb 100644
--- a/docs/model.tex
+++ b/docs/model.tex
@@ -58,7 +58,7 @@ We are thus going to define the assertions as mapping CMRA elements to sets of s
\Sem{\vctx \proves \ownM{\melt} : \Prop}_\gamma &\eqdef \Lam\meltB. \setComp{n}{\Sem{\vctx \proves \melt : \textlog{M}}_\gamma \mincl[n] \meltB} \\
\Sem{\vctx \proves \mval(\melt) : \Prop}_\gamma &\eqdef \Lam\any. \setComp{n}{\Sem{\vctx \proves \melt : \type}_\gamma \in \mval_n} \\
\Sem{\vctx \proves \upd\prop : \Prop}_\gamma &\eqdef \Lam\melt. \setComp{n}{\begin{aligned}
- \All m, \melt'. & m \leq n \land (\melt \mtimes \melt') \in \mval_m \Ra {}\\& \Exists \meltB. (\meltB \mtimes \melt') \in \mval_k \land m \in \Sem{\vctx \proves \prop :\Prop}_\gamma(\melt')
+ \All m, \melt'. & m \leq n \land (\melt \mtimes \melt') \in \mval_m \Ra {}\\& \Exists \meltB. (\meltB \mtimes \melt') \in \mval_m \land m \in \Sem{\vctx \proves \prop :\Prop}_\gamma(\meltB)
\end{aligned}
}
\end{align*}
--
GitLab