Commit 01e5e3f8 authored by Ralf Jung's avatar Ralf Jung

Merge branch 'master' into 'master'

docs: fix bug in ghost resource laws

I think the current rule if buggy; the validity of a ghost resource `a` should not imply its ownership.

Please advise me if I understand incorrectly :-)  Thank you!
Jeehoon

See merge request !5
parents 5067c640 42624c94
......@@ -417,7 +417,7 @@ Furthermore, we have the usual $\eta$ and $\beta$ laws for projections, $\lambda
\begin{mathpar}
\begin{array}{rMcMl}
\ownGGhost{\melt} * \ownGGhost{\meltB} &\provesIff& \ownGGhost{\melt \mtimes \meltB} \\
\ownGGhost{\melt} &\provesIff& \mval(\melt) \\
\ownGGhost{\melt} &\proves& \mval(\melt) \\
\TRUE &\proves& \ownGGhost{\munit}
\end{array}
\and
......
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