Commit 670c101b authored by Ralf Jung's avatar Ralf Jung

Merge branch 'master' into gen_proofmode

parents 27914f87 241b6c7c
......@@ -145,7 +145,7 @@ Notice also that the core of an RA is a strict generalization of the unit that a
It is possible to do a \emph{frame-preserving update} from $\melt \in \monoid$ to $\meltsB \subseteq \monoid$, written $\melt \mupd \meltsB$, if
\[ \All \maybe{\melt_\f} \in \maybe\monoid. \melt \mtimes \mvalFull(\maybe{\melt_\f}) \Ra \Exists \meltB \in \meltsB. \meltB \mtimes \mvalFull(\maybe{\melt_\f}) \]
\[ \All \maybe{\melt_\f} \in \maybe\monoid. \mvalFull(\melt \mtimes \maybe{\melt_\f}) \Ra \Exists \meltB \in \meltsB. \mvalFull(\meltB \mtimes \maybe{\melt_\f}) \]
We further define $\melt \mupd \meltB \eqdef \melt \mupd \set\meltB$.
......@@ -254,7 +254,7 @@ We assume that $M$ has a unit $\munit$, and hence its core is total.
(If $M$ is an exclusive monoid, the construction is very similar to a half-ownership monoid with two asymmetric halves.)
\authm(M) \eqdef{}& \maybe{\exm(M)} \times M \\
\mval( (x, \meltB ) ) \eqdef{}& \setComp{ n }{ n \in \mval(\meltB) \land (x = \mnocore \lor \Exists \melt. x = \exinj(\melt) \land \meltB \mincl_n \melt) } \\
\mval( (x, \meltB ) ) \eqdef{}& \setComp{ n }{ (x = \mnocore \land n \in \mval(\meltB)) \lor (\Exists \melt. x = \exinj(\melt) \land \meltB \mincl_n \melt \land n \in \mval(\melt)) } \\
(x_1, \meltB_1) \mtimes (x_2, \meltB_2) \eqdef{}& (x_1 \mtimes x_2, \meltB_2 \mtimes \meltB_2) \\
\mcore{(x, \meltB)} \eqdef{}& (\mnocore, \mcore\meltB) \\
(x_1, \meltB_1) \nequiv{n} (x_2, \meltB_2) \eqdef{}& x_1 \nequiv{n} x_2 \land \meltB_1 \nequiv{n} \meltB_2
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