From a603fe3a4b9ee32da36184893af296652257aff4 Mon Sep 17 00:00:00 2001
From: Ralf Jung <jung@mpi-sws.org>
Date: Fri, 8 Dec 2017 19:03:01 +0100
Subject: [PATCH] fix typos; add comment
---
docs/algebra.tex | 4 +++-
1 file changed, 3 insertions(+), 1 deletion(-)
diff --git a/docs/algebra.tex b/docs/algebra.tex
index 357a9db8b..adf798b09 100644
--- a/docs/algebra.tex
+++ b/docs/algebra.tex
@@ -89,6 +89,8 @@ For once, every \emph{contractive function} $f : \ofe \to \cofeB$ where $\cofeB$
This also holds if $f^k$ is contractive for an arbitrary $k$.
Furthermore, by America and Rutten's theorem~\cite{America-Rutten:JCSS89,birkedal:metric-space}, every contractive (bi)functor from $\COFEs$ to $\COFEs$ has a unique\footnote{Uniqueness is not proven in Coq.} fixed-point.
+$\SProp$ as defined above is complete, \ie it is a COFE.
+
\subsection{RA}
@@ -208,7 +210,7 @@ This operation is needed to prove that $\later$ commutes with separating conjunc
\begin{defn}
It is possible to do a \emph{frame-preserving update} from $\melt \in \monoid$ to $\meltsB \subseteq \monoid$, written $\melt \mupd \meltsB$, if
- \[ \All n, \maybe{\melt_\f}. \melt \mtimes n \in \mval(\maybe{\melt_\f}) \Ra \Exists \meltB \in \meltsB. \meltB \mtimes n \in\mval(\maybe{\melt_\f}) \]
+ \[ \All n, \maybe{\melt_\f}. n \in \mval(\melt \mtimes \maybe{\melt_\f}) \Ra \Exists \meltB \in \meltsB. n \in\mval(\meltB \mtimes \maybe{\melt_\f}) \]
We further define $\melt \mupd \meltB \eqdef \melt \mupd \set\meltB$.
\end{defn}
--
GitLab