equal
deleted
inserted
replaced
887 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
887 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
888 \mode<presentation>{ |
888 \mode<presentation>{ |
889 \begin{frame}[c] |
889 \begin{frame}[c] |
890 |
890 |
891 \begin{itemize} |
891 \begin{itemize} |
|
892 \item \bl{$P \,\text{says}\, F$} means \bl{$P$} can send a ``signal'' \bl{$F$} through a wire, or |
|
893 can make a statement \bl{$F$}\bigskip |
|
894 |
892 \item \bl{$P$} is entitled to do \bl{$F$}\smallskip\\ |
895 \item \bl{$P$} is entitled to do \bl{$F$}\smallskip\\ |
893 \bl{$P \,\text{controls}\, F \,\dn\, (P\,\text{says}\, F) \Rightarrow F$}\medskip |
896 \bl{$P \,\text{controls}\, F \,\dn\, (P\,\text{says}\, F) \Rightarrow F$}\medskip |
894 |
897 |
895 \begin{center} |
898 \begin{center} |
896 \bl{\infer{\Gamma \vdash F}{\Gamma \vdash P\,\text{controls}\, F & \Gamma \vdash P\,\text{says}\,F}} |
899 \bl{\infer{\Gamma \vdash F}{\Gamma \vdash P\,\text{controls}\, F & \Gamma \vdash P\,\text{says}\,F}} |