equal
deleted
inserted
replaced
702 \begin{tabular}{@{}ll@{}} |
702 \begin{tabular}{@{}ll@{}} |
703 \bl{$P\;\text{says}\;F_1 \wedge Q\;\text{says}\;F_2 \vdash Q\;\text{says}\;F_2 \wedge P\;\text{says}\;F_1$} |
703 \bl{$P\;\text{says}\;F_1 \wedge Q\;\text{says}\;F_2 \vdash Q\;\text{says}\;F_2 \wedge P\;\text{says}\;F_1$} |
704 \end{tabular} |
704 \end{tabular} |
705 \end{center} |
705 \end{center} |
706 |
706 |
707 We are better be able to prove: |
707 We better be able to prove: |
708 |
708 |
709 \begin{center} |
709 \begin{center} |
710 \begin{tabular}{@{}ll@{}} |
710 \begin{tabular}{@{}ll@{}} |
711 (1) & \bl{$P\;\text{says}\;F_1 \wedge Q\;\text{says}\;F_2 \vdash P\;\text{says}\;F_1$}\\ |
711 (1) & \bl{$P\;\text{says}\;F_1 \wedge Q\;\text{says}\;F_2 \vdash Q\;\text{says}\;F_2$}\\ |
712 (2) & \bl{$P\;\text{says}\;F_1 \wedge Q\;\text{says}\;F_2 \vdash Q\;\text{says}\;F_2$}\\ |
712 (2) & \bl{$P\;\text{says}\;F_1 \wedge Q\;\text{says}\;F_2 \vdash P\;\text{says}\;F_1$}\\ |
713 \end{tabular} |
713 \end{tabular} |
714 \end{center} |
714 \end{center} |
715 |
715 |
716 For (1): If we can prove |
716 For (1): If we can prove |
717 |
717 |
725 \end{minipage} |
725 \end{minipage} |
726 \end{tabular} |
726 \end{tabular} |
727 |
727 |
728 \end{frame}} |
728 \end{frame}} |
729 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
729 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
|
730 |
|
731 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
|
732 \mode<presentation>{ |
|
733 \begin{frame}[t] |
|
734 |
|
735 I want to prove |
|
736 |
|
737 \begin{center} |
|
738 \bl{$\Gamma \vdash \text{del\_file}$} |
|
739 \end{center}\pause |
|
740 |
|
741 There is an inference rule |
|
742 |
|
743 \begin{center} |
|
744 \bl{\infer{\Gamma \vdash P \,\text{says}\, F}{\Gamma \vdash F}} |
|
745 \end{center}\pause |
|
746 |
|
747 So I can derive \bl{$\Gamma \vdash \text{Alice} \,\text{says}\,\text{del\_file}$}.\bigskip\pause |
|
748 |
|
749 \bl{$\Gamma$} contains already \bl{$\text{Alice} \,\text{says}\,\text{del\_file}$}. \\ |
|
750 So I can use the rule |
|
751 |
|
752 \begin{center} |
|
753 \bl{\infer{\Gamma, F \vdash F}{}} |
|
754 \end{center} |
|
755 |
|
756 \onslide<5>{\bf\alert{What is wrong with this?}} |
|
757 \hfill{\bf Done. Qed.} |
|
758 |
|
759 \end{frame}} |
|
760 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
|
761 |
730 |
762 |
731 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
763 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
732 \mode<presentation>{ |
764 \mode<presentation>{ |
733 \begin{frame}[c] |
765 \begin{frame}[c] |
734 \frametitle{} |
766 \frametitle{} |