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

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

(*>*)

text_raw {*
  \renewcommand{\slidecaption}{UNIF, Edinburgh, 14.~July 2010}

  \newcommand{\abst}[2]{#1.#2}% atom-abstraction
  \newcommand{\pair}[2]{\langle #1,#2\rangle} % pairing
  \newcommand{\susp}{{\boldsymbol{\cdot}}}% for suspensions
  \newcommand{\unit}{\langle\rangle}% unit
  \newcommand{\app}[2]{#1\,#2}% application
  \newcommand{\eqprob}{\mathrel{{\approx}?}}

  \pgfdeclareradialshading{smallbluesphere}{\pgfpoint{0.5mm}{0.5mm}}%
  {rgb(0mm)=(0,0,0.9);
  rgb(0.9mm)=(0,0,0.7);
  rgb(1.3mm)=(0,0,0.5);
  rgb(1.4mm)=(1,1,1)}

  %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
  \mode<presentation>{
  \begin{frame}<1>[c]
  \frametitle{Quiz}
  
  Assuming that \smath{a} and \smath{b} are distinct variables,\\
  is it possible to find $\lambda$-terms \smath{M_1} to \smath{M_7} 
  that make the following pairs \alert{$\alpha$-equivalent}?

  \begin{tabular}{@ {\hspace{14mm}}p{12cm}}
  \begin{itemize}
  \item \smath{\lambda a.\lambda b. (M_1\,b)\;} and 
        \smath{\lambda b.\lambda a. (a\,M_1)\;}

  \item \smath{\lambda a.\lambda b. (M_2\,b)\;} and 
        \smath{\lambda b.\lambda a. (a\,M_3)\;}

  \item \smath{\lambda a.\lambda b. (b\,M_4)\;} and 
        \smath{\lambda b.\lambda a. (a\,M_5)\;}

  \item \smath{\lambda a.\lambda b. (b\,M_6)\;} and 
        \smath{\lambda a.\lambda a. (a\,M_7)\;}
  \end{itemize}
  \end{tabular}

  If there is one solution for a pair, can you describe all its solutions?

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

text_raw {*
  %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
  \mode<presentation>{
  \begin{frame}<1>[t]
  \frametitle{%
  \begin{tabular}{@ {\hspace{-3mm}}c@ {}}
  \\
  \huge Nominal Unification\\[-2mm] 
  \Large Hitting a Sweet Spot\\[5mm]
  \end{tabular}}
  \begin{center}
  Christian Urban
  \end{center}
  \begin{center}
  \small initial work with Andy Pitts and Jamie Gabbay\\[0mm] 
  \end{center}
  \end{frame}}
  %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%     

*}
text_raw {*
  %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
  \mode<presentation>{
  \begin{frame}<1-4>[c]
  \frametitle{One Motivation}

  \onslide<2->{Typing implemented in Prolog \textcolor{darkgray}{(from a textbook)}}\bigskip\\

  \onslide<3->{
  \begin{tabular}{l}
  type (Gamma, var(X), T) :- member (X,T) Gamma.\smallskip\medskip\\
  
  type (Gamma, app(M, N), T') :-\\
  \hspace{3cm}type (Gamma, M, arrow(T, T')),\\ 
  \hspace{3cm}type (Gamma, N, T).\smallskip\medskip\\
  
  type (Gamma, lam(X, M), arrow(T, T')) :-\\
  \hspace{3cm}type ((X, T)::Gamma, M, T').\smallskip\medskip\\
  
  member X X::Tail.\\
  member X Y::Tail :- member X Tail.\\
  \end{tabular}}
 
  \only<4>{
  \begin{textblock}{6}(2.5,2)
  \begin{tikzpicture}
  \draw (0,0) node[inner sep=3mm,fill=cream, ultra thick, draw=red, rounded corners=2mm] 
  {\color{darkgray}
  \begin{minipage}{8cm}\raggedright
  The problem is that \smath{\lambda x.\lambda x. (x\;x)}
  gets the types
  \begin{center}
  \begin{tabular}{l}
  \smath{T\rightarrow (T\rightarrow S) \rightarrow S} and\\ 
  \smath{(T\rightarrow S)\rightarrow T \rightarrow S}\\
  \end{tabular}
  \end{center}
  \end{minipage}};
  \end{tikzpicture}
  \end{textblock}}
  
  \end{frame}}
  %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%     
*}

text_raw {*
  %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
  \mode<presentation>{
  \begin{frame}<1>[c]
  \frametitle{Higher-Order Unification}

  \begin{itemize}
  \item Lambda Prolog with full Higher-Order Unification\\ 
  \textcolor{darkgray}{(no mgus, undecidable, modulo $\alpha\beta$)}\bigskip
  \item Higher-Order Pattern Unification\\ 
  \textcolor{darkgray}{(has mgus, decidable, some restrictions, modulo $\alpha\beta_0$)}
  \end{itemize}
 
  \end{frame}}
  %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%     
*}

text_raw {*
  %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
  \mode<presentation>{
  \begin{frame}<1-10>[t]
  \frametitle{Underlying Ideas}

  \begin{itemize}
  \item<1-> Unification (\alert{only}) up to $\alpha$

  \item<2-> Swappings / Permutations

  \only<2-5>{
  \begin{center}
  \begin{tabular}{r@ {\hspace{1mm}}l@ {\hspace{12mm}}r@ {\hspace{1mm}}l}
  \only<2>{\smath{\textcolor{white}{[b\!:=\!a]}}}%
  \only<3>{\smath{[b\!:=\!a]}}%
  \only<4-5>{\smath{\alert{\swap{a}{b}\,\act}}} & 
  \onslide<2-5>{\smath{\lambda a.b}} &
  
  \only<2>{\smath{\textcolor{white}{[b\!:=\!a]}}}%
  \only<3>{\smath{[b\!:=\!a]}}%
  \only<4-5>{\smath{\alert{\swap{a}{b}\,\act}}} &
  \onslide<2-5>{\smath{\lambda c.b}}\\

  \onslide<3-5>{\smath{=}} & \only<3>{\smath{\lambda a.a}}\only<4-5>{\smath{\lambda b.a}} & 
  \onslide<3-5>{\smath{=}} & \only<3>{\smath{\lambda c.a}}\only<4-5>{\smath{\lambda c.a}}\\
  \end{tabular}
  \end{center}\bigskip

  \onslide<4-5>{
  \begin{center}
  \begin{tikzpicture}
  \draw (0,0) node[inner sep=0mm,fill=cream, ultra thick, draw=cream] 
  {\begin{minipage}{8cm}
  \begin{tabular}{r@ {\hspace{3mm}}l}
  \smath{\swap{a}{b}\act t} $\;\dn$ & \alert{swap} {\bf all} occurences of\\ 
                                  & \smath{b} and \smath{a} in \smath{t}
  \end{tabular}
  \end{minipage}};
  \end{tikzpicture}
  \end{center}}\bigskip

  \onslide<5>{
  Unlike for \smath{[b\!:=\!a]\act(-)}, for \smath{\swap{a}{b}\act (-)} we do
  have if \smath{t =_\alpha t'} then \smath{\pi \act t =_\alpha \pi \act t'.}}}

  \item<6-> Variables (or holes)\bigskip

  \begin{center}
  \onslide<7->{\mbox{}\hspace{-25mm}\smath{\lambda x\hspace{-0.5mm}s .}}
  \onslide<8-9>{\raisebox{-1.7mm}{\huge\smath{(}}}\raisebox{-4mm}{\begin{tikzpicture}
  \fill[blue] (0, 0) circle (5mm);
  \end{tikzpicture}}
  \onslide<8-9>{\smath{y\hspace{-0.5mm}s}{\raisebox{-1.7mm}{\huge\smath{)}}}}\bigskip
  \end{center}

  \only<8-9>{\smath{y\hspace{-0.5mm}s} are the parameters the hole can depend on\onslide<9->{, but 
  then you need $\beta_0$-reduction\medskip
  \begin{center}
  \smath{(\lambda x. t) y \longrightarrow_{\beta_0} t[x:=y]}
  \end{center}}}

  \only<10>{we will record the information about which parameters a hole 
  \alert{\bf cannot} depend on}

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

text_raw {*
  %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
  \mode<presentation>{
  \begin{frame}<1-4>[c]
  \frametitle{Terms}

  \begin{tabular}{lll @ {\hspace{10mm}}lll}

  \onslide<1->{\pgfuseshading{smallbluesphere}} & 
  \onslide<1->{\colorbox{cream}{\smath{\unit}}} &
  \onslide<1->{Units} &

  \onslide<2->{\pgfuseshading{smallbluesphere}} &
  \onslide<2->{\colorbox{cream}{\smath{a}}} &
  \onslide<2->{Atoms} \\[5mm]

  \onslide<1->{\pgfuseshading{smallbluesphere}} & 
  \onslide<1->{\colorbox{cream}{\smath{\pair{t}{t'}}}} &
  \onslide<1->{Pairs} &
  
  \onslide<3->{\pgfuseshading{smallbluesphere}} &
  \onslide<3->{\colorbox{cream}{\smath{\abst{a}{t}}}} &
  \onslide<3->{Abstractions}\\[5mm]

  \onslide<1->{\pgfuseshading{smallbluesphere}} & 
  \onslide<1->{\colorbox{cream}{\smath{\app{F}{t}}}} &
  \onslide<1->{Funct.} &

  \onslide<4->{\pgfuseshading{smallbluesphere}} &
  \onslide<4->{\colorbox{cream}{\smath{\pi\susp X}}} &
  \onslide<4->{Suspensions}
  \end{tabular}
 
  \only<2>{
  \begin{textblock}{13}(1.5,12)
  \small Atoms are constants \textcolor{darkgray}{(infinitely many of them)}
  \end{textblock}}

  \only<3>{
  \begin{textblock}{13}(1.5,12)
  \small \smath{\ulcorner \lambda\abst{a}{a}\urcorner \mapsto \text{fn\ }\abst{a}{a}}\\
  \small constructions like \smath{\text{fn\ }\abst{X}{X}} are not allowed
  \end{textblock}}

  \only<4>{
  \begin{textblock}{13}(1.5,12)
  \small \smath{X} is a variable standing for a term\\
  \small \smath{\pi} is an explicit permutation \smath{\swap{a_1}{b_1}\ldots\swap{a_n}{b_n}},
  waiting to be applied to the term that is substituted for \smath{X}
  \end{textblock}}

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

text_raw {*
  %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
  \mode<presentation>{
  \begin{frame}<1-3>[c]
  \frametitle{Permutations}

  a permutation applied to a term

  \begin{center}
  \begin{tabular}{lrcl}
  \pgfuseshading{smallbluesphere} &
  \smath{[]\act c} & \smath{\dn} & \smath{c} \\

  \pgfuseshading{smallbluesphere} &
  \smath{\swap{a}{b}\!::\!\pi\act c} & \smath{\dn} & 
  \smath{\begin{cases} 
  a & \text{if}\;\pi\act c = b\\
  b & \text{if}\;\pi\act c = a\\
  \pi\act c & \text{otherwise}
  \end{cases}}\\

  \onslide<2->{\pgfuseshading{smallbluesphere}} &
  \onslide<2->{\smath{\pi\act\abst{a}{t}}} & \onslide<2->{\smath{\dn}} & 
  \onslide<2->{\smath{\abst{\pi\act a}{\pi\act t}}}\\ 

  \onslide<3->{\pgfuseshading{smallbluesphere}} &
  \onslide<3->{\smath{\pi\act\pi'\act X}} & \onslide<3->{\smath{\dn}} & 
  \onslide<3->{\smath{(\pi @ \pi')\act X}}\\
  \end{tabular}
  \end{center}

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

text_raw {*
  %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
  \mode<presentation>{
  \begin{frame}<1-3>[c]
  \frametitle{Freshness Constraints}

  Recall \smath{\lambda a. \raisebox{-0.7mm}{\tikz \fill[blue] (0, 0) circle (2.5mm);}}
  \bigskip\pause

  We therefore will identify

  \begin{center}
  \smath{\mathtt{fn\ } a. X \;\approx\; \mathtt{fn\ } b. \alert<3->{\swap{a}{b}}\act X}
  \end{center}

  provided that `\smath{b} is fresh for \smath{X} --- (\smath{b\fresh X})',
  i.e., does not occur freely in any ground term that might be substituted for
  \smath{X}.\bigskip\pause 

  If we know more about \smath{X}, e.g., if we knew that \smath{a\fresh X} and
  \smath{b\fresh X}, then we can replace\\ \smath{\swap{a}{b}\act X} by
  \smath{X}.

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

text_raw {*
  %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
  \mode<presentation>{
  \begin{frame}<1-4>[c]
  \frametitle{Equivalence Judgements}

  \alt<1>{Our equality is {\bf not} just}{but judgements}

  \begin{center}
  \begin{tabular}{rl}
  \colorbox{cream}{\smath{\onslide<2->{\nabla \vdash} t \approx t'}} & \alert{$\alpha$-equivalence}\\[1mm]
  \onslide<4->{\colorbox{cream}{\smath{\onslide<2->{\nabla \vdash} a \fresh t}}} & 
  \onslide<4->{\alert{freshness}}
  \end{tabular}
  \end{center}

  \onslide<2->{
  where
  \begin{center}
  \smath{\nabla = \{a_1\fresh X_1,\ldots, a_n\fresh X_n\}}
  \end{center}
  is a finite set of \alert{freshness assumptions}.}

  \onslide<3->{
  \begin{center}
  \smath{\{a\fresh X,b\fresh X\} \vdash \text{fn\ } a. X \approx \text{fn\ } b. X}
  \end{center}}

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

text_raw {*
  %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
  \mode<presentation>{
  \begin{frame}<1>[c]
  \frametitle{Rules for Equivalence}

  \begin{center}
  \begin{tabular}{c}
  Excerpt\\
  (i.e.~only the interesting rules)
  \end{tabular}
  \end{center}  

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

text_raw {*
  %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
  \mode<presentation>{
  \begin{frame}<1>[c]
  \frametitle{Rules for Equivalence}

  \begin{center}
  \begin{tabular}{c}
  \colorbox{cream}{\smath{\infer{\nabla \vdash a \approx a}{}}}\\[8mm]

  \colorbox{cream}{%
  \smath{\infer{\nabla \vdash \abst{a}{t} \approx \abst{a}{t'}}
               {\nabla \vdash t \approx t'}}}\\[8mm]
 
  \colorbox{cream}{%
  \smath{\infer{\nabla \vdash \abst{a}{t} \approx \abst{b}{t'}}
  {a\not=b\;\; & \nabla \vdash t \approx \swap{a}{b}\act t'\;\;& \nabla \vdash a\fresh t'}}}
  \end{tabular}
  \end{center}

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

text_raw {*
  %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
  \mode<presentation>{
  \begin{frame}<1-3>[c]
  \frametitle{Rules for Equivalence}

  \begin{center}
  \colorbox{cream}{%
  \smath{%
  \infer{\nabla \vdash \pi\act X \approx \pi'\act X}
  {\begin{array}{c}
  (a\fresh X)\in\nabla\\
  \text{for all}\; a \;\text{with}\;\pi\act a \not= \pi'\act a 
  \end{array}
  }}}
  \end{center}

  \onslide<2->{
  for example\\[4mm]
  
  \alt<2>{%
  \begin{center}
  \smath{\{a\fresh\!X, b\fresh\!X\} \vdash X \approx \swap{a}{b}\act X}
  \end{center}}
  {%
  \begin{center}
  \smath{\{a\fresh\!X, c\fresh\!X\} \vdash \swap{a}{c}\swap{a}{b}\act X \approx \swap{b}{c}\act X}
  \end{center}}

  \onslide<3->{
  \begin{tabular}{@ {}lllll@ {}}
  because & 
  \smath{\swap{a}{c}\swap{a}{b}}: & 
  \smath{a\mapsto b} &
  \smath{\swap{b}{c}}: &
  \smath{a\mapsto a}\\
  & & \smath{b\mapsto c} & & \smath{b\mapsto c}\\
  & & \smath{c\mapsto a} & & \smath{c\mapsto b}\\
  \end{tabular}
  disagree at \smath{a} and \smath{c}.}
  }

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

text_raw {*
  %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
  \mode<presentation>{
  \begin{frame}<1>[c]
  \frametitle{Rules for Freshness}

  \begin{center}
  \begin{tabular}{c}
  Excerpt\\
  (i.e.~only the interesting rules)
  \end{tabular}
  \end{center}  

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

text_raw {*
  %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
  \mode<presentation>{
  \begin{frame}<1>[c]
  \frametitle{Rules for Freshness}

  \begin{center}
  \begin{tabular}{c}
  \colorbox{cream}{%
  \smath{\infer{\nabla \vdash a\fresh b}{a\not= b}}}\\[5mm]
  
  \colorbox{cream}{%
  \smath{\infer{\nabla \vdash a\fresh\abst{a}{t}}{}}}\hspace{7mm}
  \colorbox{cream}{%
  \smath{\infer{\nabla \vdash a\fresh\abst{b}{t}}
  {a\not= b\;\; & \nabla \vdash a\fresh t}}}\\[5mm]

  \colorbox{cream}{%
  \smath{\infer{\nabla \vdash a\fresh \pi\act X}
  {(\pi^{-1}\act a\fresh X)\in\nabla}}}
  \end{tabular}
  \end{center}

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

text_raw {*
  %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
  \mode<presentation>{
  \begin{frame}<1-4>[t]
  \frametitle{$\approx$ is an Equivalence}
  \mbox{}\\[5mm]

  \begin{center}
  \colorbox{cream}{\alert{Theorem:}
  $\approx$ is an equivalence relation.}
  \end{center}\bigskip

  \only<1>{%
  \begin{tabular}{ll}
  (Reflexivity)  & $\smath{\nabla\vdash t\approx t}$\\[2mm]
  (Symmetry)     & if $\smath{\nabla\vdash t_1\approx t_2}\;$ 
                   then $\;\smath{\nabla\vdash t_2\approx t_1}$\\[2mm]
  (Transitivity) & if $\smath{\nabla\vdash t_1\approx t_2}\;$ and 
                   $\;\smath{\nabla\vdash t_2\approx t_3}$\\
                 & then $\smath{\nabla\vdash t_1\approx t_3}$\\
  \end{tabular}}

  \only<2->{%
  \begin{itemize}
  \item<2-> \smath{\nabla \vdash t\approx t'} then \smath{\nabla \vdash \pi\act t\approx \pi\act t'}

  \item<2-> \smath{\nabla \vdash a\fresh t} then 
  \smath{\nabla \vdash \pi\act a\fresh \pi\act t}

  \item<3-> \smath{\nabla \vdash t\approx \pi\act t'} then 
  \smath{\nabla \vdash (\pi^{-1})\act t\approx t'}

  \item<3-> \smath{\nabla \vdash a\fresh \pi\act t} then 
  \smath{\nabla \vdash (\pi^{-1})\act a\fresh t}

  \item<4-> \smath{\nabla \vdash a\fresh t} and \smath{\nabla \vdash t\approx t'} then
      \smath{\nabla \vdash a\fresh t'}
  \end{itemize}
  }

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

text_raw {*
  %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
  \mode<presentation>{
  \begin{frame}<1-4>
  \frametitle{Comparison $=_\alpha$}

  Traditionally \smath{=_\alpha} is defined as

  \begin{center}
  \colorbox{cream}{%
  \begin{minipage}{9cm}
  \raggedright least congruence which identifies \smath{\abst{a}{t}} 
  with \smath{\abst{b}{[a:=b]t}} provided \smath{b} is not free  
  in \smath{t}
  \end{minipage}}
  \end{center}

  where \smath{[a:=b]t} replaces all free occurrences of\\
  \smath{a} by \smath{b} in \smath{t}.
  \bigskip 

  \only<2>{%
  \begin{textblock}{13}(1.2,10)
  For \alert{ground} terms:
  
  \begin{center}
  \colorbox{cream}{%
  \begin{minipage}{9.0cm}
  \begin{tabular}{@ {}rl}
  \underline{Theorem:}
  & \smath{t=_\alpha t'\;\;}  if\hspace{-0.5mm}f~\smath{\;\;\emptyset \vdash t\approx t'}\\[2mm]
  & \smath{a\not\in FA(t)\;\;} if\hspace{-0.5mm}f~\smath{\;\;\emptyset\vdash a\fresh t} 
  \end{tabular}
  \end{minipage}}
  \end{center}
  \end{textblock}}

  \only<3>{%
  \begin{textblock}{13}(1.2,10)
  In general \smath{=_\alpha} and \smath{\approx} are distinct!
  \begin{center}
  \colorbox{cream}{%
  \begin{minipage}{6.0cm}
  \smath{\abst{a}{X}=_\alpha \abst{b}{X}\;} but not\\[2mm]
  \smath{\emptyset \vdash \abst{a}{X} \approx \abst{b}{X}\;} (\smath{a\not=b})
  \end{minipage}}
  \end{center}
  \end{textblock}}

  \only<4>{
  \begin{textblock}{6}(1,2)
  \begin{tikzpicture}
  \draw (0,0) node[inner sep=3mm,fill=cream, ultra thick, draw=red, rounded corners=2mm] 
  {\color{darkgray}
  \begin{minipage}{10cm}\raggedright
  That is a crucial point: if we had\\[-2mm]
  \[\smath{\emptyset \vdash \abst{a}{X}\approx \abst{b}{X}}\mbox{,}\] 
  then applying $\smath{[X:=a]}$, $\smath{[X:=b]}$, $\ldots$\\
  give two terms that are {\bf not} $\alpha$-equivalent.\\[3mm] 
  The freshness constraints $\smath{a\fresh X}$ and $\smath{b\fresh X}$
  rule out the problematic substitutions. Therefore

  \[\smath{\{a\fresh X,b\fresh X\} \vdash \abst{a}{X}\approx \abst{b}{X}}\] 
  
  does hold.
  \end{minipage}};
  \end{tikzpicture}
  \end{textblock}}

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

text_raw {*
  %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
  \mode<presentation>{
  \begin{frame}<1-9>
  \frametitle{Substitution}

  \begin{tabular}{l@ {\hspace{8mm}}r@ {\hspace{1.5mm}}c@ {\hspace{1.5mm}}l@ {}}
  \pgfuseshading{smallbluesphere} & 
  \smath{\sigma(\abst{a}{t})} & \smath{\dn} & \smath{\abst{a}{\sigma(t)}}\\[2mm]

  \pgfuseshading{smallbluesphere} & 
  \smath{\sigma(\pi\act X)} & \smath{\dn} & 
  \smath{\begin{cases}% 
  \pi\;\act\;\sigma(X) & \!\!\text{if\ } \sigma(X)\not=X\\
  \pi\act X & \!\!\text{otherwise}% 
  \end{cases}}\\[6mm]
  \end{tabular}\bigskip\bigskip

  \pause
  \only<2-5>{
  \only<2->{for example}
  \def\arraystretch{1.3}
  \begin{tabular}{@ {\hspace{14mm}}l@ {\hspace{3mm}}l}
  \onslide<2->{\textcolor{white}{$\Rightarrow$}} &
  \onslide<2->{\alt<3>{\smath{\underline{\abst{a}{\swap{a}{b}\act X}\;\,[X:=\pair{b}{Y}]}}}
                      {\smath{\abst{a}{\swap{a}{b}\act X}\;\,[X:=\pair{b}{Y}]}}}\\
  \onslide<3->{\smath{\Rightarrow}} &
  \onslide<3->{\alt<3,4>{\smath{\abst{a}{\underline{\swap{a}{b}\act X[X:=\pair{b}{Y}]}}}}
                        {\smath{\abst{a}{\swap{a}{b}\act X}[X:=\pair{b}{Y}]}}}\\
  \onslide<4->{\smath{\Rightarrow}} &
  \onslide<4->{\alt<4>{\smath{\abst{a}{\swap{a}{b}\act \underline{\pair{b}{Y}}}}}
                      {\smath{\abst{a}{\underline{\swap{a}{b}}\act \pair{b}{Y}}}}}\\
  \onslide<5->{\smath{\Rightarrow}} &
  \onslide<5->{\smath{\abst{a}{\pair{a}{\swap{a}{b}\act Y}}}}
  \end{tabular}}

  \only<6->
  {\begin{tabular}{l@ {\hspace{8mm}}l@ {}}
  \pgfuseshading{smallbluesphere} &
  if \smath{\nabla\vdash t\approx t'} and\hspace{-2mm}\mbox{}
  \raisebox{-2.7mm}{
  \alt<7>{\begin{tikzpicture}
          \draw (0,0) node[inner sep=1mm,fill=cream, very thick, draw=red, rounded corners=3mm] 
          {\smath{\;\nabla'\vdash\sigma(\nabla)\;}};
          \end{tikzpicture}}
         {\begin{tikzpicture}
          \draw (0,0) node[inner sep=1mm,fill=white, very thick, draw=white, rounded corners=3mm] 
          {\smath{\;\nabla'\vdash\sigma(\nabla)\;}};
          \end{tikzpicture}}}\\
  & then \smath{\nabla'\vdash\sigma(t)\approx\sigma(t')}
  \end{tabular}}

  \only<9>
  {\begin{tabular}{l@ {\hspace{8mm}}l@ {}}
  \\[-4mm]
  \pgfuseshading{smallbluesphere} &
  \smath{\sigma(\pi\act t)=\pi\act\sigma(t)}
  \end{tabular}}


  \only<7>{
  \begin{textblock}{6}(10,10.5)
  \begin{tikzpicture}
  \draw (0,0) node[inner sep=1mm,fill=cream, very thick, draw=red, rounded corners=2mm] 
  {\color{darkgray}
   \begin{minipage}{3.8cm}\raggedright
   this means\\[1mm]
   \smath{\nabla'\vdash a\fresh\sigma(X)}\\[1mm]
   holds for all\\[1mm]
   \smath{(a\fresh X)\in\nabla}
  \end{minipage}};
  \end{tikzpicture}
  \end{textblock}}

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

text_raw {*
  %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
  \mode<presentation>{
  \begin{frame}<1->
  \frametitle{Equational Problems}

  An equational problem 
  \[
    \colorbox{cream}{\smath{t \eqprob t'}}
  \]
  is \alert{solved} by

  \begin{center}
  \begin{tabular}{ll}
  \pgfuseshading{smallbluesphere} & a substitution \smath{\sigma} (terms for variables)\\[3mm]
  \pgfuseshading{smallbluesphere} & {\bf and} a set of freshness assumptions \smath{\nabla}
  \end{tabular}
  \end{center}

  so that \smath{\nabla\vdash \sigma(t)\approx \sigma(t')}.


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

text_raw {*
  %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
  \mode<presentation>{
  \begin{frame}<1->
  \frametitle{Conclusion}

  \begin{itemize}
  \item the user does not see anything of the raw level\medskip
  \only<1>{\begin{center}
  Lam a (Var a) \alert{$=$} Lam b (Var b)
  \end{center}\bigskip}

  \item<2-> we have not yet done function definitions (will come soon and
  we hope to make improvements over the old way there too)\medskip
  \item<3-> it took quite some time to get here, but it seems worthwhile 
  (Barendregt's variable convention is unsound in general, 
  found bugs in two paper proofs, quotient package, POPL 2011 tutorial)\medskip
  \end{itemize}


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

(*<*)
end
(*>*)