Commit fe66881e authored by Ralf Jung's avatar Ralf Jung
Browse files

docs: fix V being about any CMRA; fix V's timeless axiom

parent 62299a95
......@@ -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}}
\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}}
\infer{\vctx \proves \wtt{\state}{\textlog{State}}}
......@@ -464,7 +464,7 @@ A type $\type$ being \emph{inhabited} means that $ \proves \wtt{\term}{\type}$ i
{\text{$\melt$ is a discrete COFE element}}
{\text{$\melt$ is an element of a discrete CMRA}}
......@@ -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} \\
For every definition, we have to show all the side-conditions: The maps have to be non-expansive and monotone.
Supports Markdown
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment