diff --git a/docs/constructions.tex b/docs/constructions.tex
index e7607889b4b425cf59597252ded7b15296ab9112..4333612536fd476c25cb8cf0830a61ade5bf7ad8 100644
--- a/docs/constructions.tex
+++ b/docs/constructions.tex
@@ -55,7 +55,7 @@ Frame-preserving updates on the $M_i$ lift to the product:
\begin{mathpar}
\inferH{prod-update}
{\melt \mupd_{M_i} \meltsB}
- {f[i \mapsto \melt] \mupd \setComp{ f[i \mapsto \meltB]}{\meltB \in \meltsB}}
+ {\mapinsert i \melt f \mupd \setComp{ \mapinsert i \meltB f}{\meltB \in \meltsB}}
\end{mathpar}
\subsection{Sum}
@@ -96,15 +96,15 @@ We obtain the following frame-preserving updates:
\begin{mathpar}
\inferH{fpfn-alloc-strong}
{\text{$G$ infinite} \and \melt \in \mval}
- {\emptyset \mupd \setComp{[\gname \mapsto \melt]}{\gname \in G}}
+ {\emptyset \mupd \setComp{\mapsingleton \gname \melt}{\gname \in G}}
\inferH{fpfn-alloc}
{\melt \in \mval}
- {\emptyset \mupd \setComp{[\gname \mapsto \melt]}{\gname \in K}}
+ {\emptyset \mupd \setComp{\mapsingleton \gname \melt}{\gname \in K}}
\inferH{fpfn-update}
{\melt \mupd_\monoid \meltsB}
- {f[i \mapsto \melt] \mupd \setComp{ f[i \mapsto \meltB]}{\meltB \in \meltsB}}
+ {\mapinsert i \melt f] \mupd \setComp{ \mapinsert i \meltB f}{\meltB \in \meltsB}}
\end{mathpar}
Above, $\mval$ refers to the validity of $\monoid$.
diff --git a/docs/ghost-state.tex b/docs/ghost-state.tex
index d5226a1ecf805fa487795e2ae31a3d77fe877cb4..0d7da30daef1c14a6c78408f68dc3bb427e67413 100644
--- a/docs/ghost-state.tex
+++ b/docs/ghost-state.tex
@@ -197,7 +197,7 @@ This is best demonstrated by giving some proof rules.
So let us first define the notion of ghost ownership that we use in this logic.
Assuming that the family of functors contains the functor $\Sigma_i$ at index $i$, and furthermore assuming that $\monoid_i = \Sigma_i(\iPreProp, \iPreProp)$, given some $\melt \in \monoid_i$ we define:
-\[ \ownGhost\gname{\melt:\monoid_i} \eqdef \ownM{(\ldots, \emptyset, i:\set{\gname \mapsto \melt}, \emptyset, \ldots)} \]
+\[ \ownGhost\gname{\melt:\monoid_i} \eqdef \ownM{(\ldots, \emptyset, i:\mapsingleton \gname \melt, \emptyset, \ldots)} \]
This is ownership of the pair (element of the product over all the functors) that has the empty finite partial function in all components \emph{except for} the component corresponding to index $i$, where we own the element $\melt$ at index $\gname$ in the finite partial function.
We can show the following properties for this form of ownership:
diff --git a/docs/iris.sty b/docs/iris.sty
index 656e4586166dd9066790b404ae4fc321aba80fad..4100a659228bee91365e5a93dbae85c52a94e970 100644
--- a/docs/iris.sty
+++ b/docs/iris.sty
@@ -85,6 +85,8 @@
\newcommand{\subst}[3]{{#1}[{#3} / {#2}]}
\newcommand{\mapinsert}[3]{#3[#1:=#2]}
+\newcommand{\mapsingleton}[2]{[#1:=#2]}
+\newcommand{\mapsingletonComp}[3]{\left[ #1 := #2 \spac\middle|\spac #3 \right]}
\newcommand{\nil}{\epsilon}
diff --git a/docs/model.tex b/docs/model.tex
index bb91207bb095ca84ae3b7bcc6e913c747dfaba2a..4a97f7a0aa9a8d3e9eb8bc36a7814373895c9532 100644
--- a/docs/model.tex
+++ b/docs/model.tex
@@ -42,10 +42,10 @@ We are thus going to define the assertions as mapping CMRA elements to sets of s
\Lam \melt. \setComp{n}{\begin{aligned}
\All m, \meltB.& m \leq n \land \melt \mincl \meltB \land \meltB \in \mval_m \Ra {} \\
& m \in \Sem{\vctx \proves \prop : \Prop}_\gamma(\meltB) \Ra {}\\& m \in \Sem{\vctx \proves \propB : \Prop}_\gamma(\meltB)\end{aligned}}\\
- \Sem{\vctx \proves \All x : \type. \prop : \Prop}_\gamma &\eqdef
- \Lam \melt. \setComp{n}{ \All v \in \Sem{\type}. n \in \Sem{\vctx, x : \type \proves \prop : \Prop}_{\gamma[x \mapsto v]}(\melt) } \\
- \Sem{\vctx \proves \Exists x : \type. \prop : \Prop}_\gamma &\eqdef
- \Lam \melt. \setComp{n}{ \Exists v \in \Sem{\type}. n \in \Sem{\vctx, x : \type \proves \prop : \Prop}_{\gamma[x \mapsto v]}(\melt) } \\
+ \Sem{\vctx \proves \All \var : \type. \prop : \Prop}_\gamma &\eqdef
+ \Lam \melt. \setComp{n}{ \All v \in \Sem{\type}. n \in \Sem{\vctx, \var : \type \proves \prop : \Prop}_{\mapinsert \var v \gamma}(\melt) } \\
+ \Sem{\vctx \proves \Exists \var : \type. \prop : \Prop}_\gamma &\eqdef
+ \Lam \melt. \setComp{n}{ \Exists v \in \Sem{\type}. n \in \Sem{\vctx, \var : \type \proves \prop : \Prop}_{\mapinsert \var v \gamma}(\melt) } \\
~\\
\Sem{\vctx \proves \prop * \propB : \Prop}_\gamma &\eqdef \Lam\melt. \setComp{n}{\begin{aligned}\Exists \meltB_1, \meltB_2. &\melt \nequiv{n} \meltB_1 \mtimes \meltB_2 \land {}\\& n \in \Sem{\vctx \proves \prop : \Prop}_\gamma(\meltB_1) \land n \in \Sem{\vctx \proves \propB : \Prop}_\gamma(\meltB_2)\end{aligned}}
\\
@@ -72,11 +72,11 @@ For every definition, we have to show all the side-conditions: The maps have to
\Sem{\vctx \proves x : \type}_\gamma &\eqdef \gamma(x) \\
\Sem{\vctx \proves \sigfn(\term_1, \dots, \term_n) : \type_{n+1}}_\gamma &\eqdef \Sem{\sigfn}(\Sem{\vctx \proves \term_1 : \type_1}_\gamma, \dots, \Sem{\vctx \proves \term_n : \type_n}_\gamma) \\
\Sem{\vctx \proves \Lam \var:\type. \term : \type \to \type'}_\gamma &\eqdef
- \Lam \termB : \Sem{\type}. \Sem{\vctx, \var : \type \proves \term : \type}_{\gamma[\var \mapsto \termB]} \\
+ \Lam \termB : \Sem{\type}. \Sem{\vctx, \var : \type \proves \term : \type}_{\mapinsert \var \termB \gamma]} \\
\Sem{\vctx \proves \term(\termB) : \type'}_\gamma &\eqdef
\Sem{\vctx \proves \term : \type \to \type'}_\gamma(\Sem{\vctx \proves \termB : \type}_\gamma) \\
\Sem{\vctx \proves \MU \var:\type. \term : \type}_\gamma &\eqdef
- \mathit{fix}(\Lam \termB : \Sem{\type}. \Sem{\vctx, x : \type \proves \term : \type}_{\gamma[x \mapsto \termB]}) \\
+ \mathit{fix}(\Lam \termB : \Sem{\type}. \Sem{\vctx, x : \type \proves \term : \type}_{\mapinsert \var \termB \gamma}) \\
~\\
\Sem{\vctx \proves () : 1}_\gamma &\eqdef () \\
\Sem{\vctx \proves (\term_1, \term_2) : \type_1 \times \type_2}_\gamma &\eqdef (\Sem{\vctx \proves \term_1 : \type_1}_\gamma, \Sem{\vctx \proves \term_2 : \type_2}_\gamma) \\
diff --git a/docs/program-logic.tex b/docs/program-logic.tex
index 77f010aea51e00b57c53b7b06e066feeb8debae4..c292b837af7286a706588eae0806fd8e587e55f9 100644
--- a/docs/program-logic.tex
+++ b/docs/program-logic.tex
@@ -85,12 +85,20 @@ Furthermore, we assume that instances named $\gname_{\textmon{State}}$, $\gname_
\paragraph{World Satisfaction.}
We can now define the assertion $W$ (\emph{world satisfaction}) which ensures that the enabled invariants are actually maintained:
\begin{align*}
- W \eqdef{}& \Exists I : \mathbb N \fpfn \Prop. \ownGhost{\gname_{\textmon{Inv}}}{\authfull \setComp{\iname \mapsto \aginj(\latertinj(\wIso(I(\iname))))}{\iname \in \dom(I)}} * \Sep_{\iname \in \dom(I)} \left( \later I(\iname) * \ownGhost{\gname_{\textmon{Dis}}}{\set{\iname}} \lor \ownGhost{\gname_{\textmon{En}}}{\set{\iname}} \right)
+ W \eqdef{}& \Exists I : \mathbb N \fpfn \Prop.
+ \begin{array}{@{} l}
+ \ownGhost{\gname_{\textmon{Inv}}}{\authfull
+ \mapsingletonComp {\iname}
+ {\aginj(\latertinj(\wIso(I(\iname))))}
+ {\iname \in \dom(I)}} * \\
+ \Sep_{\iname \in \dom(I)} \left( \later I(\iname) * \ownGhost{\gname_{\textmon{Dis}}}{\set{\iname}} \lor \ownGhost{\gname_{\textmon{En}}}{\set{\iname}} \right)
+ \end{array}
\end{align*}
\paragraph{Invariants.}
The following assertion states that an invariant with name $\iname$ exists and maintains assertion $\prop$:
-\[ \knowInv\iname\prop \eqdef \ownGhost{\gname_{\textmon{Inv}}}{\authfrag\set{\iname \mapsto \aginj(\latertinj(\wIso(\prop)))}} \]
+\[ \knowInv\iname\prop \eqdef \ownGhost{\gname_{\textmon{Inv}}}
+ {\authfrag \mapsingleton \iname {\aginj(\latertinj(\wIso(\prop)))}} \]
\paragraph{View Updates and View Shifts.}
Next, we define \emph{view updates}, which are essentially the same as the resource updates of the base logic ($\Sref{sec:base-logic}$), except that they also have access to world satisfaction and can enable and disable invariants: