pl/frap
1
0
Fork 0
mirror of https://github.com/achlipala/frap.git synced 2024-11-10 00:07:51 +00:00
Code Issues Projects Releases Packages Wiki Activity Actions

Typo fix (issue #14)

Browse source
This commit is contained in:
Adam Chlipala 2016-10-12 13:24:52 -04:00
parent ee4aec520b
commit 84791f343f
1 changed files with 1 additions and 1 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

2
frap_book.tex
View file

@ -2779,7 +2779,7 @@ These rules together are \emph{complete}\index{completeness of Hoare logic}, in
Here we only go into detail on a proof of the dual property, \emph{soundness}\index{soundness of Hoare logic}. Here we only go into detail on a proof of the dual property, \emph{soundness}\index{soundness of Hoare logic}.
\begin{lemma}\label{hoare_while} \begin{lemma}\label{hoare_while}
Assume the following fact: Together, $\bigstep{(h, v, c)}{(h', v')}$, $I(h, v)$, and $\denote{b}(h, s)$ imply $I(h', v')$. Assume the following fact: Together, $\bigstep{(h, v, c)}{(h', v')}$, $I(h, v)$, and $\denote{b}(h, v)$ imply $I(h', v')$.
Then, given $\bigstep{(h, v, \{I\} \while{b}{c})}{(h', v')}$, it follows that $I(h', v')$ and $\neg \denote{b}(h', v')$. Then, given $\bigstep{(h, v, \{I\} \while{b}{c})}{(h', v')}$, it follows that $I(h', v')$ and $\neg \denote{b}(h', v')$.
\end{lemma} \end{lemma}
\begin{proof} \begin{proof}