slides/slides06.tex
changeset 129 10526c967679
parent 128 4e108563716c
child 130 4e8482e50590
--- a/slides/slides06.tex	Tue Nov 12 08:03:16 2013 +0000
+++ b/slides/slides06.tex	Tue Nov 12 09:57:22 2013 +0000
@@ -704,12 +704,12 @@
 \end{tabular}
 \end{center}
 
-We are better be able to prove:
+We better be able to prove:
 
 \begin{center}
 \begin{tabular}{@{}ll@{}}
-(1) & \bl{$P\;\text{says}\;F_1 \wedge Q\;\text{says}\;F_2 \vdash P\;\text{says}\;F_1$}\\
-(2) & \bl{$P\;\text{says}\;F_1 \wedge Q\;\text{says}\;F_2 \vdash Q\;\text{says}\;F_2$}\\
+(1) & \bl{$P\;\text{says}\;F_1 \wedge Q\;\text{says}\;F_2 \vdash Q\;\text{says}\;F_2$}\\
+(2) & \bl{$P\;\text{says}\;F_1 \wedge Q\;\text{says}\;F_2 \vdash P\;\text{says}\;F_1$}\\
 \end{tabular}
 \end{center}
 
@@ -729,6 +729,38 @@
 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%      
      
 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+\mode<presentation>{
+\begin{frame}[t]
+
+I want to prove
+
+\begin{center}
+\bl{$\Gamma \vdash \text{del\_file}$}
+\end{center}\pause
+
+There is an inference rule
+
+\begin{center}
+\bl{\infer{\Gamma \vdash P \,\text{says}\, F}{\Gamma \vdash F}}
+\end{center}\pause
+
+So I can derive \bl{$\Gamma \vdash \text{Alice} \,\text{says}\,\text{del\_file}$}.\bigskip\pause
+
+\bl{$\Gamma$} contains already \bl{$\text{Alice} \,\text{says}\,\text{del\_file}$}. \\
+So I can use the rule
+
+\begin{center}
+\bl{\infer{\Gamma, F \vdash F}{}}
+\end{center}
+
+\onslide<5>{\bf\alert{What is wrong with this?}}
+\hfill{\bf Done. Qed.}
+
+\end{frame}}
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%        
+     
+     
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
   \mode<presentation>{
   \begin{frame}[c]
   \frametitle{}