--- 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{}