Commit a5f94780 authored by Jacques-Henri Jourdan's avatar Jacques-Henri Jourdan

Correct the Inv-alloc rule.

parent 4485ef7d
Pipeline #2818 passed with stage
in 9 minutes and 25 seconds
......@@ -434,7 +434,7 @@ We can now derive the following rules (this involves unfolding the definition of
\begin{mathpar}
\axiomH{inv-persist}{\knowInv\namesp\prop \proves \always\knowInv\namesp\prop}
\axiomH{inv-alloc}{\later\prop \proves \pvs[\namesp] \knowInv\namesp\prop}
\axiomH{inv-alloc}{\later\prop \proves \pvs[\bot] \knowInv\namesp\prop}
\inferH{inv-open}
{\namesp \subseteq \mask}
......
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