Commit 7e15ce54 authored by Glen Mével's avatar Glen Mével
Browse files

ICFP21 paper: fix statement of theorem with existentials

parent d60bcda9
......@@ -10,7 +10,8 @@
We now turn to proving the following.
\begin{theorem}%
The implementation shown in \fref{fig:queue:impl} (\sref{sec:queue:impl})
There exist predicates $\ISQUEUE$ and $\QUEUEINV$ such that
the implementation shown in \fref{fig:queue:impl} (\sref{sec:queue:impl})
satisfies the functional specification appearing in \fref{fig:queue:spec:weak}
(\sref{sec:queue:spec:weak}).
\end{theorem}%
......
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