Commit a1fbc5c9 authored by Ralf Jung's avatar Ralf Jung


parent c3585db7
Pipeline #5867 passed with stages
in 30 minutes and 42 seconds
...@@ -16,7 +16,7 @@ Now we define: ...@@ -16,7 +16,7 @@ Now we define:
\CInv{\gname}{\namesp}{\prop} \eqdef{}& \knowInv\namesp{\prop \lor \ownGhost\gname{1}} \CInv{\gname}{\namesp}{\prop} \eqdef{}& \knowInv\namesp{\prop \lor \ownGhost\gname{1}}
\end{align*} \end{align*}
It is then straight forward to prove: It is then straightforward to prove:
\begin{mathpar} \begin{mathpar}
\inferH{CInv-new}{} \inferH{CInv-new}{}
{\later\prop \vs[\bot] \Exists \gname. \CInvTok\gname{1} * \always\CInv\gname\namesp\prop} {\later\prop \vs[\bot] \Exists \gname. \CInvTok\gname{1} * \always\CInv\gname\namesp\prop}
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