Commit 10186bd8 by Ralf Jung

### Merge branch 'patch-1' into 'master'

Fix a typo in constructions.tex

x_1 should be a_1

See merge request !35
parents 7cbcc410 61ff48e3
 ... @@ -295,7 +295,7 @@ The frame-preserving update involves the notion of a \emph{local update}: ... @@ -295,7 +295,7 @@ The frame-preserving update involves the notion of a \emph{local update}: \newcommand\lupd{\stackrel{\mathrm l}{\mupd}} \newcommand\lupd{\stackrel{\mathrm l}{\mupd}} \begin{defn} \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 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} \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$. 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$. ... ...
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!