Skip to content
GitLab
Menu
Projects
Groups
Snippets
Help
Help
Support
Community forum
Keyboard shortcuts
?
Submit feedback
Contribute to GitLab
Sign in / Register
Toggle navigation
Menu
Open sidebar
Rice Wine
Iris
Commits
b2dce48b
Commit
b2dce48b
authored
Jun 29, 2018
by
Ralf Jung
Browse files
docs: Fix definition of validity for auth
Thanks to Siddharth for pointing this out
parent
403c9587
Changes
1
Hide whitespace changes
Inline
Side-by-side
docs/constructions.tex
View file @
b2dce48b
...
...
@@ -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.)
\begin{align*}
\authm
(M)
\eqdef
{}&
\maybe
{
\exm
(M)
}
\times
M
\\
\mval
( (x,
\meltB
) )
\eqdef
{}&
\setComp
{
n
}{
n
\in
\mval
(
\meltB
)
\l
and
(x =
\mnocore
\l
or
\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
...
...
Write
Preview
Supports
Markdown
0%
Try again
or
attach a new file
.
Attach a file
Cancel
You are about to add
0
people
to the discussion. Proceed with caution.
Finish editing this message first!
Cancel
Please
register
or
sign in
to comment