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

Revising before class

Browse source
This commit is contained in:
Adam Chlipala 2020-05-05 19:26:59 -04:00
parent 1c91cf3d5c
commit 8a87c209f7
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

@ -5416,7 +5416,7 @@ Here is a sketch of the key lemmas.
\begin{lemma}\label{preserve_unused} \begin{lemma}\label{preserve_unused}
Assume that $\vec{\alpha}$ is a duplicate-free list of parties excluding both sender and receiver of channel $c$. Assume that $\vec{\alpha}$ is a duplicate-free list of parties excluding both sender and receiver of channel $c$.
If $\mptys{p}{\vec{\alpha}}{\; \send{c}{x : \sigma}{\tau(x)}}$, then for any $v : \sigma$, we have $\mptys{p'}{\vec{\alpha}}{\tau(v)}$. If $\mptys{p}{\vec{\alpha}}{\; \send{c}{x : \sigma}{\tau(x)}}$, then for any $v : \sigma$, we have $\mptys{p}{\vec{\alpha}}{\tau(v)}$.
In other words, when we have well-typed code for a set of parties that do not participate in the first step of a protocol, that code remains well-typed when we advance to the next protocol step. In other words, when we have well-typed code for a set of parties that do not participate in the first step of a protocol, that code remains well-typed when we advance to the next protocol step.
\end{lemma} \end{lemma}
\begin{proof} \begin{proof}