(*<*)
theory Slides1
imports "LaTeXsugar" "Nominal"
begin

notation (latex output)
  set ("_") and
  Cons  ("_::/_" [66,65] 65) 

(*>*)


text_raw {*
  \renewcommand{\slidecaption}{TU Munich, 28.~May 2010}
  %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
  \mode<presentation>{
  \begin{frame}<1>[t]
  \frametitle{%
  \begin{tabular}{@ {\hspace{-3mm}}c@ {}}
  \\
  \huge Nominal 2\\[-2mm] 
  \large Or, How to Reason Conveniently with\\[-5mm]
  \large General Bindings\\[15mm]
  \end{tabular}}
  \begin{center}
  joint work with {\bf Cezary} and Brian Huf\!fman\\[0mm] 
  \end{center}
  \end{frame}}
  %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%     

*}

text_raw {*
  %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
  \mode<presentation>{
  \begin{frame}<1-2>
  \frametitle{\begin{tabular}{c}Part I: Nominal Theory\end{tabular}}
  \mbox{}\\[-3mm]

  \begin{itemize}
  \item sorted atoms and sort-respecting permutations\medskip

  \onslide<2->{
  \item[] in old Nominal: atoms have dif\!ferent type

  \begin{center}
  \begin{tabular}{c@ {\hspace{7mm}}c}
  $[] \act c \dn c$ &
  @{text "(a b)::\<pi> \<bullet> c \<equiv>"} 
  $\begin{cases}
  \mbox{@{text "b"}} & \text{if} \mbox{@{text "\<pi> \<bullet> c = a"}}\\
  \mbox{@{text "a"}} & \text{if} \mbox{@{text "\<pi> \<bullet> c = b"}}\\
  \mbox{@{text "\<pi> \<bullet> c"}} & \text{otherwise}
  \end{cases}$
  \end{tabular}
  \end{center}}
  \end{itemize}

  \end{frame}}
  %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%     
*}

text_raw {*
  %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
  \mode<presentation>{
  \begin{frame}<1>
  \frametitle{\begin{tabular}{c}Problems\end{tabular}}
  \mbox{}\\[-3mm]

  \begin{itemize}
  \item $\_ \act \_ :: \alpha perm \Rightarrow \beta \Rightarrow \beta$

  \item $supp \_ :: \beta \Rightarrow \alpha set$

  \begin{center}
  $finite (supp x)_{\alpha_1} \ldots finite (supp x)_{\alpha_n}$
  \end{center}
  
  \item $\forall \pi_{\alpha_1} \ldots \pi_{\alpha_n}\;.\; P$
  \end{itemize}

  \end{frame}}
  %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%     
*}


text_raw {*
  %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
  \mode<presentation>{
  \begin{frame}<1>[c]
  \frametitle{\begin{tabular}{c}Part II: General Bindings\end{tabular}}
  \mbox{}\\[-3mm]

  
  \end{frame}}
  %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%     
*}



(*<*)
end
(*>*)