From fe66881e02b7ff7f60c312f45e1c6231471f2aaf Mon Sep 17 00:00:00 2001
From: Ralf Jung <jung@mpi-sws.org>
Date: Tue, 23 Aug 2016 11:19:47 +0200
Subject: [PATCH] docs: fix V being about any CMRA; fix V's timeless axiom
---
docs/logic.tex | 4 ++--
docs/model.tex | 4 ++--
2 files changed, 4 insertions(+), 4 deletions(-)
diff --git a/docs/logic.tex b/docs/logic.tex
index a8e7552ad..d2d84550b 100644
--- a/docs/logic.tex
+++ b/docs/logic.tex
@@ -270,7 +270,7 @@ In writing $\vctx, x:\type$, we presuppose that $x$ is not already declared in $
\infer{\vctx \proves \wtt{\melt}{\textlog{M}}}
{\vctx \proves \wtt{\ownGGhost{\melt}}{\Prop}}
\and
- \infer{\vctx \proves \wtt{\melt}{\textlog{M}}}
+ \infer{\vctx \proves \wtt{\melt}{\type} \and \text{$\type$ is a CMRA}}
{\vctx \proves \wtt{\mval(\melt)}{\Prop}}
\and
\infer{\vctx \proves \wtt{\state}{\textlog{State}}}
@@ -464,7 +464,7 @@ A type $\type$ being \emph{inhabited} means that $ \proves \wtt{\term}{\type}$ i
{\timeless{\ownGGhost\melt}}
\infer
-{\text{$\melt$ is a discrete COFE element}}
+{\text{$\melt$ is an element of a discrete CMRA}}
{\timeless{\mval(\melt)}}
\infer{}
diff --git a/docs/model.tex b/docs/model.tex
index 31db77a01..9546c8d11 100644
--- a/docs/model.tex
+++ b/docs/model.tex
@@ -40,8 +40,8 @@ We introduce an additional logical connective $\ownM\melt$, which will later be
\Lam \melt. \setComp{n}{\begin{aligned}
\All m, \meltB.& m \leq n \land \melt\mtimes\meltB \in \mval_m \Ra {} \\
& m \in \Sem{\vctx \proves \prop : \Prop}_\gamma(\meltB) \Ra {}\\& m \in \Sem{\vctx \proves \propB : \Prop}_\gamma(\melt\mtimes\meltB)\end{aligned}} \\
- \Sem{\vctx \proves \ownM{\melt} : \Prop}_\gamma &\eqdef \Lam\meltB. \setComp{n}{\melt \mincl[n] \meltB} \\
- \Sem{\vctx \proves \mval(\melt) : \Prop}_\gamma &\eqdef \Lam\any. \setComp{n}{\melt \in \mval_n} \\
+ \Sem{\vctx \proves \ownM{\melt} : \Prop}_\gamma &\eqdef \Lam\meltB. \setComp{n}{\Sem{\vctx \proves \melt : \textlog{M}} \mincl[n] \meltB} \\
+ \Sem{\vctx \proves \mval(\melt) : \Prop}_\gamma &\eqdef \Lam\any. \setComp{n}{\Sem{\vctx \proves \melt : \type} \in \mval_n} \\
\end{align*}
For every definition, we have to show all the side-conditions: The maps have to be non-expansive and monotone.
--
GitLab