Commit 7905c004 authored by Ralf Jung's avatar Ralf Jung

LaTeX: change \set macros

parent d7d3cacf
......@@ -249,7 +249,7 @@ Given a monoid $M$, we construct a monoid modeling someone owning an \emph{autho
(If $M$ is an exclusive monoid, the construction is very similar to a half-ownership monoid with two asymmetric halves.)
Let $\auth{M}$ be the monoid with carrier
\[
\SET{ (x, \melt) }{ x \in \mcarp{\exm{\mcarp{M}}} \land \melt \in \mcarp{M} \land (x = \munit_{\exm{\mcarp{M}}} \lor \melt \leq_M x) }
\setComp{ (x, \melt) }{ x \in \mcarp{\exm{\mcarp{M}}} \land \melt \in \mcarp{M} \land (x = \munit_{\exm{\mcarp{M}}} \lor \melt \leq_M x) }
\]
and multiplication
\[
......@@ -341,7 +341,7 @@ We first lift the transition relation to $\STSS \times \mathcal{P}(\STST)$ (impl
\begin{align*}
(s, T) \ra (s', T') \eqdef&\, s \ra s' \land \STSL(s) \uplus T = \STSL(s') \uplus T' \\
\textsf{frame}(s, T) \eqdef&\, (s, \STST \setminus (\STSL(s) \uplus T)) \\
\upclose(S, T) \eqdef&\, \SET{ s' \in \STSS}{\exists s \in S.\; \textsf{frame}(s, T) \ststrans \textsf{frame}(s', T) }
\upclose(S, T) \eqdef&\, \setComp{ s' \in \STSS}{\exists s \in S.\; \textsf{frame}(s, T) \ststrans \textsf{frame}(s', T) }
\end{align*}
\noindent
......@@ -358,7 +358,7 @@ This is exactly what we have to show, since we know $\STSL(s) \uplus T = \STSL(s
Let $\STSMon{\STSS}$ be the monoid with carrier
\[
\SET{ (s, S, T) \in \exm{\STSS} \times \mathcal{P}(\STSS) \times \mathcal{P}(\STST) }{ \begin{aligned} &(s = \munit \lor s \in S) \land \upclose(S, T) = S \land{} \\& S \neq \emptyset \land \All s \in S. \STSL(s) \sep T \end{aligned} }
\setComp{ (s, S, T) \in \exm{\STSS} \times \mathcal{P}(\STSS) \times \mathcal{P}(\STST) }{ \begin{aligned} &(s = \munit \lor s \in S) \land \upclose(S, T) = S \land{} \\& S \neq \emptyset \land \All s \in S. \STSL(s) \sep T \end{aligned} }
\]
and multiplication
\[
......
......@@ -152,9 +152,11 @@
\newcommand{\upclose}{\mathord{\uparrow}}
\def\All #1.{\forall #1.\;}%
\def\Exists #1.{\exists #1.\;}%
\def\Ret #1.{#1.\;}%
\newcommand{\spac}{\;} % a space
\def\All #1.{\forall #1.\spac}%
\def\Exists #1.{\exists #1.\spac}%
\def\Ret #1.{#1.\spac}%
\newcommand{\any}{{\rule[-.2ex]{1ex}{.4pt}}}%
\newcommand{\unitval}{()}%
......@@ -182,21 +184,8 @@
\newcommand{\IF}{\mathrel{\text{if}}}
\newcommand{\WHEN}{\textrm{when }}
\newcommand{\SET}[2]{
\left\{%
#1%
\;\middle|\;%
#2%
\right\}
}
\newcommand{\SETB}[1]{
\left\{%
#1%
\right\}
}
\newcommand{\SETC}[2]{#1 & #2}
\newcommand*\setComp[2]{\left\{#1\spac\middle|\spac#2\right\}}
\newcommand*\set[1]{\left\{#1\right\}}
\newenvironment{inbox}[1][]{
\begin{array}[#1]{@{}l@{}}
......@@ -317,8 +306,8 @@
%% various pieces of Syntax
\newcommand{\unitsort}{1}% \unit is bold.
\def\MU #1.{\mu #1.\;}%
\def\Lam #1.{\lambda #1.\;}%
\def\MU #1.{\mu #1.\spac}%
\def\Lam #1.{\lambda #1.\spac}%
\newcommand{\proves}{\vdash}
\newcommand{\provesalways}{\vdash_{\!\!\boxempty}}
......
Markdown is supported
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