From 61ff48e3838f57083e5aa3d8fde621dff86b84f1 Mon Sep 17 00:00:00 2001
From: Dan Frumin <dfrumin@cs.ru.nl>
Date: Sun, 11 Dec 2016 22:31:06 +0100
Subject: [PATCH] Fix a typo in constructions.tex
---
docs/constructions.tex | 2 +-
1 file changed, 1 insertion(+), 1 deletion(-)
diff --git a/docs/constructions.tex b/docs/constructions.tex
index 225016c84..6a62fa47c 100644
--- a/docs/constructions.tex
+++ b/docs/constructions.tex
@@ -295,7 +295,7 @@ The frame-preserving update involves the notion of a \emph{local update}:
\newcommand\lupd{\stackrel{\mathrm l}{\mupd}}
\begin{defn}
It is possible to do a \emph{local update} from $\melt_1$ and $\meltB_1$ to $\melt_2$ and $\meltB_2$, written $(\melt_1, \meltB_1) \lupd (\melt_2, \meltB_2)$, if
- \[ \All n, \maybe{\melt_\f}. x_1 \in \mval_n \land \melt_1 \nequiv{n} \meltB_1 \mtimes \maybe{\melt_\f} \Ra \melt_2 \in \mval_n \land \melt_2 \nequiv{n} \meltB_2 \mtimes \maybe{\melt_\f} \]
+ \[ \All n, \maybe{\melt_\f}. \melt_1 \in \mval_n \land \melt_1 \nequiv{n} \meltB_1 \mtimes \maybe{\melt_\f} \Ra \melt_2 \in \mval_n \land \melt_2 \nequiv{n} \meltB_2 \mtimes \maybe{\melt_\f} \]
\end{defn}
In other words, the idea is that for every possible frame $\maybe{\melt_\f}$ completing $\meltB_1$ to $\melt_1$, the same frame also completes $\meltB_2$ to $\melt_2$.
--
GitLab