# HG changeset patch
# User Eugen Sawin <sawine@me73.com>
# Date 1311370782 -7200
# Node ID 9938ea8ed067a08706ea6c78bf7490a8c861cebf
# Parent  271b2a5270c16a0766235fc5c52692c02cca0221
Final.

diff -r 271b2a5270c1 -r 9938ea8ed067 slides/final/slides.pdf
Binary file slides/final/slides.pdf has changed
diff -r 271b2a5270c1 -r 9938ea8ed067 slides/images/att.jpg
Binary file slides/images/att.jpg has changed
diff -r 271b2a5270c1 -r 9938ea8ed067 slides/images/fujitsu.jpg
Binary file slides/images/fujitsu.jpg has changed
diff -r 271b2a5270c1 -r 9938ea8ed067 slides/images/hp.jpg
Binary file slides/images/hp.jpg has changed
diff -r 271b2a5270c1 -r 9938ea8ed067 slides/images/ibm.jpg
Binary file slides/images/ibm.jpg has changed
diff -r 271b2a5270c1 -r 9938ea8ed067 slides/images/intel2.jpg
Binary file slides/images/intel2.jpg has changed
diff -r 271b2a5270c1 -r 9938ea8ed067 slides/images/motorola.jpg
Binary file slides/images/motorola.jpg has changed
diff -r 271b2a5270c1 -r 9938ea8ed067 slides/images/nec.jpg
Binary file slides/images/nec.jpg has changed
diff -r 271b2a5270c1 -r 9938ea8ed067 slides/images/sgi.jpg
Binary file slides/images/sgi.jpg has changed
diff -r 271b2a5270c1 -r 9938ea8ed067 slides/images/siemens.jpg
Binary file slides/images/siemens.jpg has changed
diff -r 271b2a5270c1 -r 9938ea8ed067 slides/images/sun.jpg
Binary file slides/images/sun.jpg has changed
diff -r 271b2a5270c1 -r 9938ea8ed067 slides/src/slides.tex
--- a/slides/src/slides.tex	Fri Jul 22 23:11:53 2011 +0200
+++ b/slides/src/slides.tex	Fri Jul 22 23:39:42 2011 +0200
@@ -46,6 +46,7 @@
 \newtheorem*{def:general automata}{Generalised automaton}
 \newtheorem*{def:general acceptance}{Acceptance}
 \newtheorem*{def:syntax}{Syntax}
+\newtheorem*{def:derived syntax}{Derived connectives}
 \newtheorem*{def:program}{Program}
 \newtheorem*{def:program automaton}{System automaton}
 
@@ -118,7 +119,16 @@
 \subfigure{\includegraphics[width=70pt,height=50pt]{images/atc.jpg}}
 }
 \only<2>{
-\subfigure{\includegraphics[width=20pt,height=10pt]{images/intel2.jpg}}
+\subfigure{\includegraphics[width=35pt,height=20pt]{images/sun.jpg}}
+\subfigure{\includegraphics[width=20pt,height=20pt]{images/hp.jpg}}
+\subfigure{\includegraphics[width=40pt,height=20pt]{images/siemens.jpg}}
+\subfigure{\includegraphics[width=15pt,height=20pt]{images/att.jpg}}
+%\subfigure{\includegraphics[width=20pt,height=20pt]{images/motorola.jpg}}
+\subfigure{\includegraphics[width=20pt,height=20pt]{images/sgi.jpg}}
+\subfigure{\includegraphics[width=25pt,height=20pt]{images/fujitsu.jpg}}
+\subfigure{\includegraphics[width=20pt,height=18pt]{images/nec.jpg}}
+\subfigure{\includegraphics[width=20pt,height=20pt]{images/intel2.jpg}}
+\subfigure{\includegraphics[width=25pt,height=20pt]{images/ibm.jpg}}
 }
 \end{figure}
 \end{frame}
@@ -166,6 +176,23 @@
 \item $\U$ reads \emph{until}.
 \end{itemize}
 \end{def:syntax}
+
+\visible<2>{
+\begin{def:derived syntax}
+Let $\varphi$ and $\psi$ be formulae:
+\begin{multicols}{2}
+\begin{itemize}
+\item $\top \equiv p \lor \neg p$ for $p \in \Prop$
+\item $\bot \equiv \neg \top$
+\item $\varphi \land \psi \equiv \neg (\neg \varphi \lor \neg \psi)$
+\item $\varphi \rightarrow \psi \equiv \neg \varphi \lor \psi$
+\item $\varphi \leftrightarrow \psi \equiv (\varphi \rightarrow \psi) \land (\psi \rightarrow \varphi)$
+\item $\Diamond \varphi \equiv \top \U \varphi$
+\item $\Box \varphi \equiv \neg \Diamond \neg \varphi$
+\end{itemize}
+\end{multicols}
+\end{def:derived syntax}
+}
 \end{frame}
 
 \begin{frame}
@@ -527,7 +554,7 @@
 $\Downarrow$\\
 Automaton $\A_\varphi$ for $\varphi$\\
 \vspace{20pt}
-\visible<2>{\textcolor{red}{On-the-fly methods} \`a la Gerth et al.}
+\visible<2>{\textcolor{red}{On-the-fly method} \`a la Gerth et al.}
 \end{center}
 \end{frame}