Commit 5515b8f0 authored by Jacques-Henri Jourdan's avatar Jacques-Henri Jourdan
Browse files

Get rid of existential quantifier in invariant-opening rule of logically...

Get rid of existential quantifier in invariant-opening rule of logically atomic triples. This matches what is stated in the Iris 1 paper, and is actually not less expressive.
parent 970b8a01
......@@ -76,7 +76,7 @@ This linearization point being atomic, it allows the opening of invariants just
\infer{%
\lahoare <x> {\later I \isep P} {e} {\later I \isep Q}
}{%
\knowInv{}{\Exists x. I} \vdash \lahoare <x> {P} {e} {Q}
\knowInv{}{I} \vdash \lahoare <x> {P} {e} {Q}
}
%
\end{mathpar}
......
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