\documentclass[pdf]{prosper}
\usepackage{alltt}
%\usepackage{proof}
\usepackage{amssymb}
\usepackage{pstricks}
\usepackage{pst-node}
\usepackage{fancyvrb}

\newrgbcolor{nictablue}{0.0 0.310 0.490}

\newrgbcolor{purple}{0.63 0.13 0.94}
\newrgbcolor{redbrown}{0.698 0.133 0.133}
\newrgbcolor{brown}{0.647 0.165 0.165}
\newrgbcolor{darkviolet}{0.4 0.2 0.6}
\newrgbcolor{lightazure}{0.2 0.6 1.0}
\newrgbcolor{darkazure}{0.0 0.4 0.8}
\newrgbcolor{dkdullazure}{0.2 0.4 0.6}
\newrgbcolor{obsdullazure}{0.0 0.2 0.4}
\newrgbcolor{dkazureblue}{0.0 0.2 0.6}
\newrgbcolor{dkazurecyan}{0.0 0.4 0.6}
\newrgbcolor{dkblueazure}{0.0 0.2 0.8}
\newrgbcolor{obsdullcyan}{0.0 0.4 0.4}

\newrgbcolor{varcolor}{0.2 0.4 0.0}
\newrgbcolor{tycolor}{0.6 0.2 0.2}

\newcommand{\constcolor}{\nictablue}  % have used nictablue, darkviolet

\newcommand{\mytt}{\usefont{OT1}{ppl}{m}{n}}

\newcommand{\fld}[1]{{\nictablue\textsf{#1}}}
\newcommand{\var}[1]{{\varcolor\ensuremath{\mathit{#1}}}}
\newcommand{\tyname}[1]{\textrm{\usefont{OT1}{put}{m}{it}\tycolor #1}}
\newcommand{\constname}[1]{\textrm{\constcolor\mytt #1}}

\newcommand{\ints}{\ensuremath{\mathbb{Z}}}
\newcommand{\nats}{\ensuremath{\mathbb{N}}}
\newcommand{\reals}{\ensuremath{\mathbb{R}}}
\newcommand{\rats}{\ensuremath{\mathbb{Q}}}
\newcommand{\bools}{\ensuremath{\mathbb{B}}}



\title{Title is here
}
\author{Author Name etc.
}
\email{email or website etc
}
\institution{{\includegraphics{nicta-colour-on-pale.eps}}
}
\date{23rd October 2003
}
\slideCaption{This message appears at the bottom of each page.
}
\Logo(-1,-1.3){\includegraphics[width=1.7cm]{nicta-colour-on-pale.eps}}

\begin{document}

\maketitle

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%%%%%%%%%% Slide 1
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\begin{slide}{Introduction}

  \begin{itemize}
  \item Item 1
  \item Item 2 is longer
  \item Item 3 is also ...
    \begin{itemize}
    \item also what?
    \end{itemize}
  \item Another item of interest
  \item Last comments
  \end{itemize}

\end{slide}

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%%%%%%%%%% Slide 2
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\begin{slide}{A descriptive look}

\begin{description}
\item[{{\large\nictablue Theorems taste great:}}] The proof of
  the technique's ``main theorem'' is played out for each problem
  instance. (Used to implement Cooper's algorithm; see paper.)

\item[{{\large\nictablue Theorems stay crunchy:}}] The ``main
  theorem'' is proved once and for all, and is instantiated with each
  problem.

\item[{{\large\nictablue Theorems are good for you:}}] An external tool
  finds a proof that can then be replayed in HOL.  If proof search
  dominates this can be very effective.
\end{description}

\end{slide}

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%%%%%%%%%% Slide 3
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%two slides rolled into one - a slide with special effects
\overlays{2}{
\begin{slide}{I want slides like Michael's}
\newcommand\form{\textsl{formula}}
\newcommand\term{\textsl{term}}
\renewcommand\var{\textsl{var}}
\newcommand\lit{\textsl{numeral}}
\newcommand\sep{\texttt{  |  }}
\newcommand\bnfeq{\texttt{::=}}
\newcommand\relop{\textsl{relop}}
\[\begin{array}{lcl}
   \form & \bnfeq & \form \land \form \sep \form \lor \form \sep\\
         &        & \neg\form \sep \exists \var.\, \form \sep
                    \forall \var.\, \form \sep \\
         &        &
\onlySlide*{1}{\psframebox[linecolor=white]{\lit \,|\, \term}}
\onlySlide*{2}{\rnode{A}{\rput(-2.1,.8){%
      \rnode{B}{\mbox{\tiny\red\term{} ``is divisible by'' \lit}}}%
    \psframebox[linecolor=red,linestyle=dotted]{\lit \,|\, \term}}}
         \sep  \term \;\relop\; \term\\
   \term & \bnfeq & \lit \sep \term + \term \sep
                    - \term \sep\\
         &        & \lit * \term \sep \var\\
   \relop& \bnfeq & < \sep \leq \sep = \sep \geq \sep > \\
   \var  & \bnfeq & x \sep y \sep z\dots\\
   \lit  & \bnfeq & 0 \sep 1 \sep 2\dots
\end{array}\]
\FromSlide{2}
\nccurve[angleA=270,angleB=180,linestyle=dotted,linecolor=red]{->}{B}{A}
\end{slide}}

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%%%%%%%%%% Slide 4
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\overlays{8}{
\begin{slide}{Doing it bit by bit 101}

\begin{itemize}
  \item In the beginning ...
 \FromSlide{2} there was dirt and sticks
 \FromSlide{3} \item Then came
 \FromSlide{4} 
  \begin{itemize}
  \item Clay tablets
  \FromSlide{5} \item Blackboards
  \FromSlide{6} \item Whiteboards
 \end{itemize}
\FromSlide{7} \item Then came \texttt{powerpoint, slitex, foiltex etc.}
\FromSlide{8} \item Then came \Large{\texttt{prosper}}

\end{itemize}

\end{slide}
}

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%%%%%%%%%% Slide 5
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\overlays{5}{
\begin{slide}{\small{Doing it bit by bit - Real World Applications from Michael}}
\[
\begin{array}{ll}
  & (\exists x.\; 3x + y \leq 10 \land 20 \leq x - y)\\
& \FromSlide{2} \quad\mbox{\textit{(re-arrange)}}\\
\FromSlide{2} \equiv &
\FromSlide{2} (\exists x.\; 3x \leq 10 - y \land 20 + y \leq x)\\
& \FromSlide{3} \quad \mbox{\textit{(re-express with \texttt{evalupper} \& \texttt{evallower})}}\\
\FromSlide{3}\equiv &
\FromSlide{3}(\exists x. \;\texttt{evalupper}\; x\; [(3,10-y)] \land
                     \texttt{evallower}\; x\; [(1,20+y)])\\
& \FromSlide{4} \quad\mbox{\textit{(apply theorem)}}\\
\FromSlide{4}
\equiv & \FromSlide{4} \texttt{real\_shadow} \;[(3,10-y)]\;[(1,20 + y)]\\
& \FromSlide{5} \quad\mbox{\textit{(unfold def'n of \texttt{real\_shadow})}}\\
\FromSlide{5}
\equiv & \FromSlide{5} 3 (20 + y) \leq (10 - y)\\
\FromSlide{5}\equiv & \FromSlide{5}4y \leq -50\\
\FromSlide{5}\equiv & \FromSlide{5}y \leq -13\\
\end{array}
\]
\end{slide}
}


\end{document}
%%% Local Variables:
%%% mode: latex
%%% TeX-master: t
%%% End: