Commit 0a151fd4 authored by Derek Dreyer's avatar Derek Dreyer

fixed some proof formatting errors

parent b958d569
......@@ -67,7 +67,7 @@ Unsurprisingly, that leads to a contradiction, as is shown in the following lemm
With this lemma in hand, the proof of \thmref{thm:counterexample-1} is simple.
\begin{proof}[Proof of \thmref{thm:counterexample-1}]
Using the previous lemmas we have
\proves \All \gname. \lnot (\gname \Mapsto A(\gname)).
......@@ -176,7 +176,7 @@ We have
Thus for any $\prop$ we have ${\upd}_1\left(\ownGhost{\gname}{\starttoken} \lor \ownGhost \gname \finishtoken * \prop\right)$.
Again since our goal is still of the form ${\upd}_1$ we may assume $\ownGhost{\gname}{\starttoken} \lor \ownGhost \gname \finishtoken * \always \prop$.
The rule \ruleref{eq:inv-alloc} then gives us precisely what we need.
\qed \end{proof}
......@@ -191,7 +191,7 @@ and thus
\item We first show
\[\gname \Mapsto \prop * \gname \Mapsto \propB * \always \prop \proves {\upd}_1 \always \propB.\]
......@@ -218,7 +218,7 @@ and thus
\item By applying the above twice, we easily obtain
\[ \gname \Mapsto \prop * \gname \Mapsto \propB \proves ({\upd}_1 \always \prop) \Lra ({\upd}_1 \always \propB) \]
\qed \end{proof}
% When allocating $\gname \Mapsto \prop(\gname)$ in \lemref{lem:counterexample-invariants-saved-prop-alloc}, we will start off in ``state'' $\ownGhost \gname \starttoken$, and once we have $P$ in \lemref{lem:counterexample-invariants-saved-prop-agree} we use \ruleref{eq:start-finish} to transition to $\ownGhost\gname \finishtoken$, obtaining ourselves a copy of said token.
% Finally, we use this token with $\gname \Mapsto \propB$ to obtain a proof of $\propB$.
Intuitively, \lemref{lem:counterexample-invariants-saved-prop-agree} shows that we can ``convert'' a proof from $\prop$ to $\propB$.
Markdown is supported
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment