diff --git a/docs/constructions.tex b/docs/constructions.tex
index a45a30b799857e34ac00b0cb26db95aeb67368ef..c8381082f26137c2e936a04c8751851706a9f878 100644
--- a/docs/constructions.tex
+++ b/docs/constructions.tex
@@ -387,20 +387,20 @@ The construction follows the idea of STSs as described in CaReSL \cite{caresl}.
We first lift the transition relation to $\STSS \times \wp(\STST)$ (implementing a \emph{law of token conservation}) and define a stepping relation for the \emph{frame} of a given token set:
\begin{align*}
(s, T) \stsstep (s', T') \eqdef{}& s \stsstep s' \land \STSL(s) \uplus T = \STSL(s') \uplus T' \\
- s \stsfstep{T} s' \eqdef{}& \Exists T_1, T_2. T_1 \sep \STSL(s) \cup T \l+and (s, T_1) \stsstep (s', T_2)
+ s \stsfstep{T} s' \eqdef{}& \Exists T_1, T_2. T_1 \disj \STSL(s) \cup T \l+and (s, T_1) \stsstep (s', T_2)
\end{align*}
We further define \emph{closed} sets of states (given a particular set of tokens) as well as the \emph{closure} of a set:
\begin{align*}
-\STSclsd(S, T) \eqdef{}& \All s \in S. \STSL(s) \sep T \land \All s'. s \stsfstep{T} s' \Ra s' \in S \\
+\STSclsd(S, T) \eqdef{}& \All s \in S. \STSL(s) \disj T \land \All s'. s \stsfstep{T} s' \Ra s' \in S \\
\upclose(S, T) \eqdef{}& \setComp{ s' \in \STSS}{\Exists s \in S. s \stsftrans{T} s' }
\end{align*}
The STS RA is defined as follows
\begin{align*}
- \monoid \eqdef{}& \setComp{\STSauth((s, T) \in \STSS \times \wp(\STST))}{\STSL(s) \sep T} +{}\\& \setComp{\STSfrag((S, T) \in \wp(\STSS) \times \wp(\STST))}{\STSclsd(S, T) \land S \neq \emptyset} + \bot \\
- \STSfrag(S_1, T_1) \mtimes \STSfrag(S_2, T_2) \eqdef{}& \STSfrag(S_1 \cap S_2, T_1 \cup T_2) \qquad\qquad\qquad \text{if $T_1 \sep T_2$ and $S_1 \cap S_2 \neq \emptyset$} \\
- \STSfrag(S, T) \mtimes \STSauth(s, T') \eqdef{}& \STSauth(s, T') \mtimes \STSfrag(S, T) \eqdef \STSauth(s, T \cup T') \qquad \text{if $T \sep T'$ and $s \in S$} \\
+ \monoid \eqdef{}& \setComp{\STSauth((s, T) \in \STSS \times \wp(\STST))}{\STSL(s) \disj T} +{}\\& \setComp{\STSfrag((S, T) \in \wp(\STSS) \times \wp(\STST))}{\STSclsd(S, T) \land S \neq \emptyset} + \bot \\
+ \STSfrag(S_1, T_1) \mtimes \STSfrag(S_2, T_2) \eqdef{}& \STSfrag(S_1 \cap S_2, T_1 \cup T_2) \qquad\qquad\qquad \text{if $T_1 \disj T_2$ and $S_1 \cap S_2 \neq \emptyset$} \\
+ \STSfrag(S, T) \mtimes \STSauth(s, T') \eqdef{}& \STSauth(s, T') \mtimes \STSfrag(S, T) \eqdef \STSauth(s, T \cup T') \qquad \text{if $T \disj T'$ and $s \in S$} \\
\mcore{\STSfrag(S, T)} \eqdef{}& \STSfrag(\upclose(S, \emptyset), \emptyset) \\
\mcore{\STSauth(s, T)} \eqdef{}& \STSfrag(\upclose(\set{s}, \emptyset), \emptyset)
\end{align*}
diff --git a/docs/derived.tex b/docs/derived.tex
index df80640344bc8282f48d1f01beed61dc50a2fa45..696be132bc318fb8d6f73ab3350b1ba92bd16c28 100644
--- a/docs/derived.tex
+++ b/docs/derived.tex
@@ -319,8 +319,8 @@ We use the notation $\namesp.\iname$ for the namespace $[\iname] \dplus \namesp$
We define the inclusion relation on namespaces as $\namesp_1 \sqsubseteq \namesp_2 \Lra \Exists \namesp_3. \namesp_2 = \namesp_3 \dplus \namesp_1$, \ie $\namesp_1$ is a suffix of $\namesp_2$.
We have that $\namesp_1 \sqsubseteq \namesp_2 \Ra \namecl{\namesp_2} \subseteq \namecl{\namesp_1}$.
-Similarly, we define $\namesp_1 \sep \namesp_2 \eqdef \Exists \namesp_1', \namesp_2'. \namesp_1' \sqsubseteq \namesp_1 \land \namesp_2' \sqsubseteq \namesp_2 \land |\namesp_1'| = |\namesp_2'| \land \namesp_1' \neq \namesp_2'$, \ie there exists a distinguishing suffix.
-We have that $\namesp_1 \sep \namesp_2 \Ra \namecl{\namesp_2} \sep \namecl{\namesp_1}$, and furthermore $\iname_1 \neq \iname_2 \Ra \namesp.\iname_1 \sep \namesp.\iname_2$.
+Similarly, we define $\namesp_1 \disj \namesp_2 \eqdef \Exists \namesp_1', \namesp_2'. \namesp_1' \sqsubseteq \namesp_1 \land \namesp_2' \sqsubseteq \namesp_2 \land |\namesp_1'| = |\namesp_2'| \land \namesp_1' \neq \namesp_2'$, \ie there exists a distinguishing suffix.
+We have that $\namesp_1 \disj \namesp_2 \Ra \namecl{\namesp_2} \disj \namecl{\namesp_1}$, and furthermore $\iname_1 \neq \iname_2 \Ra \namesp.\iname_1 \disj \namesp.\iname_2$.
We will overload the usual Iris notation for invariant assertions in the following:
\[ \knowInv\namesp\prop \eqdef \Exists \iname \in \namecl\namesp. \knowInv\iname{\prop} \]
diff --git a/docs/iris.sty b/docs/iris.sty
index c5692f9060e557200b0348e1580e8d605ec0a890..8d893c58bec2787c3963d99ff92609d09e7b6c7c 100644
--- a/docs/iris.sty
+++ b/docs/iris.sty
@@ -29,9 +29,8 @@
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\DeclareMathOperator*{\Sep}{\scalerel*{\ast}{\sum}}
-\newcommand{\bigast}{\Sep}
-
-\newcommand*{\sep}[1][]{\mathrel{\#_{#1}}} % bad name; it's a different "sep"
+\newcommand*{\disj}[1][]{\mathrel{\#_{#1}}}
+\newcommand\pord{\sqsubseteq}
\newcommand\dplus{\mathbin{+\kern-1.0ex+}}
\newcommand{\upclose}{\mathord{\uparrow}}
\newcommand{\ALT}{\ |\ }
@@ -44,10 +43,11 @@
\newcommand{\any}{{\rule[-.2ex]{1ex}{.4pt}}}%
-\newcommand{\judgment}[2]{\paragraph{#1}\hspace{\stretch{1}}\fbox{$#2$}}
+\newcommand{\judgment}[2][]{\paragraph{#1}\hspace{\stretch{1}}\fbox{$#2$}}
\newcommand{\pfn}{\rightharpoonup}
\newcommand\fpfn{\xrightharpoonup{\kern-0.25ex\textrm{fin}\kern-0.25ex}}
+\newcommand{\la}{\leftarrow}
\newcommand{\ra}{\rightarrow}
\newcommand{\Ra}{\Rightarrow}
\newcommand{\Lra}{\Leftrightarrow}
diff --git a/docs/logic.tex b/docs/logic.tex
index 6b3c37119d6f9e2780cca18bd9b40338aaa7c0a9..0cd2a4df83876e4b1008a869dcf659f2d49fc103 100644
--- a/docs/logic.tex
+++ b/docs/logic.tex
@@ -50,7 +50,7 @@ For any language $\Lang$, we define the corresponding thread-pool semantics.
\tpool \in \textdom{ThreadPool} \eqdef \bigcup_n \textdom{Exp}^n
\]
-\judgment{Machine reduction} {\cfg{\tpool}{\state} \step
+\judgment[Machine reduction]{\cfg{\tpool}{\state} \step
\cfg{\tpool'}{\state'}}
\begin{mathpar}
\infer
@@ -181,7 +181,7 @@ The judgment $\vctx \proves \wtt{\term}{\type}$ expresses that, in variable cont
A variable context, $\vctx = x_1:\type_1, \dots, x_n:\type_n$, declares a list of variables and their types.
In writing $\vctx, x:\type$, we presuppose that $x$ is not already declared in $\vctx$.
-\judgment{Well-typed terms}{\vctx \proves_\Sig \wtt{\term}{\type}}
+\judgment[Well-typed terms]{\vctx \proves_\Sig \wtt{\term}{\type}}
\begin{mathparpagebreakable}
%%% variables and function symbols
\axiom{x : \type \proves \wtt{x}{\type}}
@@ -312,7 +312,7 @@ We implicitly assume that an arbitrary variable context, $\vctx$, is added to ev
Furthermore, an arbitrary \emph{boxed} assertion context $\always\pfctx$ may be added to every constituent.
Axioms $\vctx \mid \prop \provesIff \propB$ indicate that both $\vctx \mid \prop \proves \propB$ and $\vctx \mid \propB \proves \prop$ can be derived.
-\judgment{}{\vctx \mid \pfctx \proves \prop}
+\judgment{\vctx \mid \pfctx \proves \prop}
\paragraph{Laws of intuitionistic higher-order logic with equality.}
This is entirely standard.
\begin{mathparpagebreakable}
diff --git a/docs/model.tex b/docs/model.tex
index aff36d7ae2aaf886ab3591b884e7cb4818d4893d..cd8565605419bf22fd5b2cfe2533d13e238d62b7 100644
--- a/docs/model.tex
+++ b/docs/model.tex
@@ -95,7 +95,7 @@ We only have to define the missing connectives, the most interesting bits being
\typedsection{Primitive view-shift}{\mathit{pvs}_{-}^{-}(-) : \Delta(\pset{\mathbb{N}}) \times \Delta(\pset{\mathbb{N}}) \times \iProp \nfn \iProp}
\begin{align*}
\mathit{pvs}_{\mask_1}^{\mask_2}(\prop) &= \Lam \rs. \setComp{n}{\begin{aligned}
- \All \rs_\f, m, \mask_\f, \state.& 0 < m \leq n \land (\mask_1 \cup \mask_2) \sep \mask_\f \land k \in \wsat\state{\mask_1 \cup \mask_\f}{\rs \mtimes \rs_\f} \Ra {}\\&
+ \All \rs_\f, m, \mask_\f, \state.& 0 < m \leq n \land (\mask_1 \cup \mask_2) \disj \mask_\f \land k \in \wsat\state{\mask_1 \cup \mask_\f}{\rs \mtimes \rs_\f} \Ra {}\\&
\Exists \rsB. k \in \prop(\rsB) \land k \in \wsat\state{\mask_2 \cup \mask_\f}{\rsB \mtimes \rs_\f}
\end{aligned}}
\end{align*}
@@ -105,7 +105,7 @@ We only have to define the missing connectives, the most interesting bits being
$\textdom{wp}$ is defined as the fixed-point of a contractive function.
\begin{align*}
\textdom{pre-wp}(\textdom{wp})(\mask, \expr, \pred) &\eqdef \Lam\rs. \setComp{n}{\begin{aligned}
- \All &\rs_\f, m, \mask_\f, \state. 0 \leq m < n \land \mask \sep \mask_\f \land m+1 \in \wsat\state{\mask \cup \mask_\f}{\rs \mtimes \rs_\f} \Ra {}\\
+ \All &\rs_\f, m, \mask_\f, \state. 0 \leq m < n \land \mask \disj \mask_\f \land m+1 \in \wsat\state{\mask \cup \mask_\f}{\rs \mtimes \rs_\f} \Ra {}\\
&(\All\val. \toval(\expr) = \val \Ra \Exists \rsB. m+1 \in \prop(\rs') \land m+1 \in \wsat\state{\mask \cup \mask_\f}{\rs' \mtimes \rs_\f}) \land {}\\
&(\toval(\expr) = \bot \land 0 < m \Ra \red(\expr, \state) \land \All \expr_2, \state_2, \expr_\f. \expr,\state \step \expr_2,\state_2,\expr_\f \Ra {}\\
&\qquad \Exists \rsB_1, \rsB_2. m \in \wsat\state{\mask \cup \mask_\f}{\rs' \mtimes \rs_\f} \land m \in \textdom{wp}(\mask, \expr_2, \pred)(\rsB_1) \land {}&\\