(*<*)

theory SlidesB

imports "~~/src/HOL/Library/LaTeXsugar" "../Nominal/Nominal2"

begin

notation (latex output)

  set ("_") and

  Cons  ("_::/_" [66,65] 65) 

(*>*)

text_raw {*

  %% was \begin{colormixin}{20!averagebackgroundcolor}

  %% 

  %% is \begin{colormixin}{50!averagebackgroundcolor}

  \renewcommand{\slidecaption}{Dagstuhl, 14 October 2013}

  %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

  \mode<presentation>{

  \begin{frame}

  \frametitle{%

  \begin{tabular}{@ {}c@ {}}

  \Huge Nominal Isabelle\\[0mm]

  \Large or, How Not to be Intimidated by\\[-3mm]

  \Large the Variable Convention\\[-5mm]

  \end{tabular}}

  \begin{center}

  Christian Urban\\[1mm]

  King's College London\\[-4mm]\mbox{}

  \end{center}

  \begin{center}

  \begin{block}{}

  \color{gray}

  \small

  {\bf\mbox{}\hspace{-1.5mm}Variable Convention:}\\[1mm] 

  If $M_1,\ldots,M_n$ occur in a certain mathematical context

  (e.g. definition, proof), then in these terms all bound variables 

  are chosen to be different from the free variables.\\[2mm]

  \footnotesize\hfill Henk Barendregt in ``The Lambda-Calculus: Its Syntax and Semantics''

  \end{block}

  \end{center}

  \end{frame}}

  %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%     

*}

text_raw {*

  %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

  \mode<presentation>{

  \begin{frame}<1->[c]

  \frametitle{}

  \begin{center}

  \begin{tabular}{@ {\hspace{-2mm}}c@ {}}

  \includegraphics[scale=0.36]{phd-2.jpg}\,

  \includegraphics[scale=0.36]{phd-1.jpg}\\

  \hfill\textcolor{gray}{\small dinner after my PhD examination}

  \end{tabular}

  \end{center}

  \end{frame}}

  %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%     

*}

text_raw {*

  %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

  \mode<presentation>{

  \begin{frame}<1->[c]

  \frametitle{}

  \begin{itemize}

  \item \normalsize Aim: develop Nominal Isabelle for reasoning formally about 

  programming languages\\[-10mm]\mbox{}

  \end{itemize}

  \begin{center}

  \begin{block}{}

  \color{gray}

  \footnotesize

  {\bf\mbox{}\hspace{-1.5mm}Variable Convention:}\\[0mm] 

  If $M_1,\ldots,M_n$ occur in a certain mathematical context

  (e.g. definition, proof), then in these terms all bound variables 

  are chosen to be different from the free variables.\hfill ---Henk Barendregt

  \end{block}

  \end{center}\pause

  \mbox{}\\[-19mm]\mbox{}

  \begin{itemize}

  \item found an error in an ACM journal paper by Bob Harper and Frank Pfenning 

  about LF (and fixed it in three ways)

  \item found also fixable errors in my Ph.D.-thesis about cut-elimination

  (examined by Henk Barendregt and Andy Pitts)

  \item found that the variable convention can in principle be used for proving false

  \end{itemize}

  \end{frame}}

  %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%     

*}

text_raw {*

  %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

  \mode<presentation>{

  \begin{frame}<1->[c]

  \frametitle{Nominal Techniques}

  \begin{itemize}

  \item Andy Pitts showed me that permutations\\ preserve $\alpha$-equivalence:

  \begin{center}

  \smath{t_1 \approx_{\alpha} t_2 \quad \Rightarrow\quad \pi \act t_1 \approx_{\alpha} \pi \act t_2} 

  \end{center}

  \item also permutations and substitutions commute, if you suspend permutations

  in front of variables

  \begin{center}

  \smath{\pi\act\sigma(t) = \sigma(\pi\act t)}

  \end{center}\medskip\medskip

  \item this allowed us to define as simple Nominal Unification algorithm\medskip

  \begin{center}

  \smath{\nabla \vdash t \approx^?_{\alpha} t'}\hspace{2cm}

  \smath{\nabla \vdash a \fresh^? t}

  \end{center}

  \end{itemize}

  %\begin{textblock}{3}(13.1,1.3)

  %\includegraphics[scale=0.26]{andrewpitts.jpg}

  %\end{textblock}

  \end{frame}}

  %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%     

*}

text_raw {*

  %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

  \mode<presentation>{

  \begin{frame}[c]

  \frametitle{Nominal Isabelle}

  \begin{itemize}

  \item a general theory about atoms and permutations\medskip

  \begin{itemize}

  \item sorted atoms and

  \item sort-respecting permutations\bigskip

  \end{itemize}

  \item support and freshness

  \begin{center}

  \begin{tabular}{l}

  \smath{\textit{supp}(x) \dn \{ a \mid \textit{infinite}\,\{ b \mid \swap{a}{b}\act x \not= x\}\}}\\[2mm]

  \smath{a \fresh x \dn a \notin \textit{supp}(x)}

  \end{tabular}

  \end{center}\bigskip\pause

  \item allow users to reason about alpha-equivalence classes as if they were 

  syntax trees

  %

  %\item $\alpha$-equivalence

  %\begin{center}

  %\begin{tabular}{l}

  %\smath{as.x \approx_\alpha bs.y \dn}\\[2mm]

  %\hspace{2cm}\smath{\exists \pi.\;\text{supp}(x) - as = \text{supp}(y) - bs}\\ 

  %\hspace{2cm}\smath{\;\wedge\; \text{supp}(x) - as \fresh \pi}\\

  %\hspace{2cm}\smath{\;\wedge\; \pi \act x = y}

  %\end{tabular}

  %\end{center}

  \end{itemize}

  \end{frame}}

  %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%     

*}

text_raw {*

  %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

  \mode<presentation>{

  \begin{frame}<1-7>

  \frametitle{New Types in HOL}

   \begin{center}

  \begin{tikzpicture}[scale=1.5]

  %%%\draw[step=2mm] (-4,-1) grid (4,1);

  \onslide<2-4,6->{\draw[very thick] (0.7,0.4) circle (4.25mm);}

  \onslide<1-4,6->{\draw[rounded corners=1mm, very thick] ( 0.0,-0.8) rectangle ( 1.8, 0.9);}

  \onslide<3-5,6->{\draw[rounded corners=1mm, very thick] (-1.95,0.85) rectangle (-2.85,-0.05);}

  \onslide<3-4,6->{\draw (-2.0, 0.845) --  (0.7,0.845);}

  \onslide<3-4,6->{\draw (-2.0,-0.045)  -- (0.7,-0.045);}

  \onslide<4-4,6->{\alert{\draw ( 0.7, 0.4) node {\footnotesize\begin{tabular}{@ {}c@ {}}$\alpha$-\\[-1mm]classes\end{tabular}};}}

  \onslide<4-5,6->{\alert{\draw (-2.4, 0.4) node {\footnotesize\begin{tabular}{@ {}c@ {}}$\alpha$-eq.\\[-1mm]terms\end{tabular}};}}

  \onslide<1-4,6->{\draw (1.8, 0.48) node[right=-0.1mm]

    {\footnotesize\begin{tabular}{@ {}l@ {}}existing\\[-1mm] type\\ \onslide<4-4,6->{\alert{(sets of raw terms)}}\end{tabular}};}

  \onslide<2-4,6->{\draw (0.9, -0.35) node {\footnotesize\begin{tabular}{@ {}l@ {}}non-empty\\[-1mm]subset\end{tabular}};}

  \onslide<3-5,6->{\draw (-3.25, 0.55) node {\footnotesize\begin{tabular}{@ {}l@ {}}new\\[-1mm]type\end{tabular}};}

  \onslide<3-4,6->{\draw[<->, very thick] (-1.8, 0.3) -- (-0.1,0.3);}

  \onslide<3-4,6->{\draw (-0.95, 0.3) node[above=0mm] {\footnotesize{}isomorphism};}

  \onslide<6->{\draw[->, line width=2mm, red] (-1.0,-0.4) -- (0.35,0.16);}

  \end{tikzpicture}

  \end{center}

  \begin{center}

  \textcolor{red}{\large\bf\onslide<6->{define \boldmath$\alpha$-equivalence}}

  \end{center}

  \begin{textblock}{9}(2.8,12.5)

  \only<7>{

  \begin{tikzpicture}

  \draw (0,0) node[fill=cream, text width=8.5cm, thick, draw=red, rounded corners=1mm] (nn)

  {The ``new types mechanism'' is the reason why there is no Nominal Coq.};

  \end{tikzpicture}}

  \end{textblock}

  \end{frame}}

  %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%     

*}

text_raw {*

  %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

  \mode<presentation>{

  \begin{frame}<1-3>[c]

  \frametitle{HOL vs.~Nominal}

  \begin{itemize}

  \item Nominal logic by Pitts is incompatible 

  with choice principles\medskip

  \item but HOL includes Hilbert's epsilon\pause\bigskip

  \item The solution: Do not require that everything has finite support\medskip

  \begin{center}

  \smath{\onslide<1-2>{\textit{finite}(\textit{supp}(x))  \quad\Rightarrow\quad} a \fresh a.x}

  \end{center}

  \end{itemize}

  \end{frame}}

  %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%     

*}

text_raw {*

  %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

  \mode<presentation>{

  \begin{frame}<1-5>

  \frametitle{\begin{tabular}{c}Our Work\end{tabular}}

  \mbox{}\\[-6mm]

    \begin{center}

  \begin{tikzpicture}[scale=1.5]

  %%%\draw[step=2mm] (-4,-1) grid (4,1);

  \onslide<1>{\draw[very thick] (0.7,0.4) circle (4.25mm);}

  \onslide<1>{\draw[rounded corners=1mm, very thick] ( 0.0,-0.8) rectangle ( 1.8, 0.9);}

  \onslide<1->{\draw[rounded corners=1mm, very thick] (-1.95,0.85) rectangle (-2.85,-0.05);}

  \onslide<1>{\draw (-2.0, 0.845) --  (0.7,0.845);}

  \onslide<1>{\draw (-2.0,-0.045)  -- (0.7,-0.045);}

  \onslide<1>{\alert{\draw ( 0.7, 0.4) node {\footnotesize\begin{tabular}{@ {}c@ {}}$\alpha$-\\[-1mm]classes\end{tabular}};}}

  \onslide<1->{\alert{\draw (-2.4, 0.4) node {\footnotesize\begin{tabular}{@ {}c@ {}}$\alpha$-eq.\\[-1mm]terms\end{tabular}};}}

  \onslide<1>{\draw (1.8, 0.48) node[right=-0.1mm]

    {\footnotesize\begin{tabular}{@ {}l@ {}}existing\\[-1mm] type\\ \onslide<1>{\alert{(sets of raw terms)}}\end{tabular}};}

  \onslide<1>{\draw (0.9, -0.35) node {\footnotesize\begin{tabular}{@ {}l@ {}}non-empty\\[-1mm]subset\end{tabular}};}

  \onslide<1->{\draw (-3.25, 0.55) node {\footnotesize\begin{tabular}{@ {}l@ {}}new\\[-1mm]type\end{tabular}};}

  \onslide<1>{\draw[<->, very thick] (-1.8, 0.3) -- (-0.1,0.3);}

  \onslide<1>{\draw (-0.95, 0.3) node[above=0mm] {\footnotesize{}isomorphism};}

  %%\onslide<1>{\draw[->, line width=2mm, red] (-1.0,-0.4) -- (0.35,0.16);}

  \end{tikzpicture}

  \end{center}

  \begin{textblock}{9.5}(6,3.5)

  \begin{itemize}

  \item<1-> define fv and $\alpha$

  \item<2-> build quotient / new type

  \item<3-> derive a reasoning infrastructure ($\fresh$, distinctness, injectivity, cases,\ldots) 

  \item<4-> derive a {\bf stronger} cases lemma

  \item<5-> from this, a {\bf stronger} induction principle (Barendregt variable convention built in)\\

  \begin{center}

  \textcolor{blue}{Foo ($\lambda x. \lambda y. t$) ($\lambda u. \lambda v. s$)} 

  \end{center}

  \end{itemize}

  \end{textblock}

  \end{frame}}

  %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%     

*}

text_raw {*

  %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

  \mode<presentation>{

  \begin{frame}

  \frametitle{Nominal Isabelle} 

  \begin{itemize}

  \item Users can for example define lambda-terms as:

  \end{itemize}

*}

 atom_decl name   text_raw {*\medskip\isanewline *}

	nominal_datatype lam =

	    Var name

	  | App lam lam 

	  | Lam x::name t::lam   binds x in t ("Lam _. _")

text_raw {*

  \mbox{}\bigskip

  \begin{itemize}

  \item These are \underline{\bf named} alpha-equivalence classes, for example

  \end{itemize}

  \begin{center}

  \gb{@{text "Lam a.(Var a)"}} \alert{$\,=\,$} \gb{@{text "Lam b.(Var b)"}}

  \end{center}

  \end{frame}}

  %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%     

*}

text_raw {*

  %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

  \mode<presentation>{

  \begin{frame}

  \frametitle{\Large (Weak) Induction Principles} 

  \begin{itemize}

  \item The usual induction principle for lambda-terms is as follows:

  \begin{center}

  \mbox{}\hspace{-1mm}\begin{beamercolorbox}[sep=1mm, wd=9cm]{boxcolor}

  \centering\smath{%

  \infer{P\,t}

  {\begin{array}{l}

  \forall x.\;P\,x\\[2mm]

  \forall t_1\,t_2.\;P\,t_1\wedge P\,t_2\Rightarrow P\,(t_1\;t_2)\\[2mm]

  \forall x\,t.\;P\,t\Rightarrow P\,(\lambda x.t)\\

  \end{array}

  }}

  \end{beamercolorbox}

  \end{center}

  \item It requires us in the lambda-case to show the property \smath{P} for

  all binders \smath{x}.\medskip\\ 

  (This nearly always requires renamings and they can be 

  tricky to automate.)

  \end{itemize}

  \end{frame}}

  %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%     

*}

text_raw {*

  %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

  \mode<presentation>{

  \begin{frame}

  \frametitle{\Large Strong Induction Principles} 

  \begin{itemize}

  \item Therefore we introduced the following strong induction principle:

  \begin{center}

  \mbox{}\hspace{-2mm}\begin{beamercolorbox}[sep=1mm, wd=11.5cm]{boxcolor}

  \centering\smath{%

  \infer{\tikz[remember picture] \node[inner sep=1mm] (n1a) {\alert<4>{$P$}};%

         \tikz[remember picture] \node[inner sep=1mm] (n2a) {\alert<3>{$c$}};%

         \tikz[remember picture] \node[inner sep=1mm] (n3a) {\alert<2>{$t$}};}

  {\begin{array}{l}

  \forall x\,c.\;P\,c\;x\\[2mm]

  \forall t_1\,t_2\,c.\;(\forall d.\,P d\,t_1)\wedge (\forall d. P\,d\,t_2)

  \Rightarrow P\,c\;(t_1\,t_2)\\[2mm]

  \forall x\,t\,c.\;\alert<1>{x\fresh \alert<3>{c}} 

  \wedge (\forall d. P\,d\,t)\Rightarrow P\,c\;(\lambda x.t)

  \end{array}

  }}

  \end{beamercolorbox}

  \end{center}

  \end{itemize}

  \begin{textblock}{11}(0.9,10.9)

  \only<2>{

  \begin{tikzpicture}[remember picture]

  \draw (0,0) node[fill=cream, text width=10.5cm, thick, draw=red, rounded corners=1mm] (n3b)

  { The variable over which the induction proceeds:\\[2mm]

    \hspace{3mm}``\ldots By induction over the structure of \smath{M}\ldots''};

  \path[overlay, ->, ultra thick, red] (n3b) edge[out=90, in=-110] (n3a);

  \end{tikzpicture}}

  \only<3>{

  \begin{tikzpicture}[remember picture]

  \draw (0,0) node[fill=cream, text width=11cm, thick, draw=red, rounded corners=1mm] (n2b)

  {The {\bf context} of the induction; i.e.~what the binder should be fresh for

   $\quad\Rightarrow$ \smath{(x,y,N,L)}:\\[2mm]

   ``\ldots By the variable convention we can assume \mbox{\smath{z\not\equiv x,y}} 

     and \smath{z} not free in \smath{N}$\!$,\,\smath{L}\ldots''};

  \path[overlay, ->, ultra thick, red] (n2b) edge[out=90, in=-100] (n2a);

  \end{tikzpicture}}

  \only<4>{

  \begin{tikzpicture}[remember picture]

  \draw (0,0) node[fill=cream, text width=11cm, thick, draw=red, rounded corners=1mm] (n1b)

  {The property to be proved by induction:\\[-3mm]

  \begin{center}\small

  \begin{tabular}{l}

  \smath{\!\!\lambda

  (x,\!y,\!N\!,\!L).\,\lambda M.\;\,x\not=y\,\wedge\,x\fresh L\,\Rightarrow}\\[1mm]

  \hspace{8mm}

  \smath{M[x\!:=\!N][y\!:=\!L] = M[y\!:=\!L][x\!:=\!N[y\!:=\!L]]}  

  \end{tabular}

  \end{center}};

  \path[overlay, ->, ultra thick, red] (n1b) edge[out=90, in=-70] (n1a);

  \end{tikzpicture}}

  \end{textblock}

  \end{frame}}

  %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%     

*}

text_raw {*

  %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

  \mode<presentation>{

  \begin{frame}<1-4>

  \frametitle{\begin{tabular}{c}Binding Sets of Names\end{tabular}}

  \mbox{}\\[-3mm]

  \begin{itemize}

  \item binding sets of names has some interesting properties:\medskip

  \begin{center}

  \begin{tabular}{l}

  \textcolor{blue}{$\forall\{x, y\}.\, x \rightarrow y \;\;\approx_\alpha\;\; \forall\{y, x\}.\, y \rightarrow x$}

  \bigskip\smallskip\\

  \onslide<2->{%

  \textcolor{blue}{$\forall\{x, y\}.\, x \rightarrow y \;\;\not\approx_\alpha\;\; \forall\{z\}.\, z \rightarrow z$}

  }\bigskip\smallskip\\

  \onslide<3->{%

  \textcolor{blue}{$\forall\{x\}.\, x \rightarrow y \;\;\approx_\alpha\;\; \forall\{x, \alert{z}\}.\, x \rightarrow y$}

  }\medskip\\

  \onslide<3->{\hspace{4cm}\small provided $z$ is fresh for the type}

  \end{tabular}

  \end{center}

  \end{itemize}

  \begin{textblock}{8}(2,14.5)

  \footnotesize $^*$ $x$, $y$, $z$ are assumed to be distinct

  \end{textblock}

  \only<4>{

  \begin{textblock}{6}(2.5,4)

  \begin{tikzpicture}

  \draw (0,0) node[inner sep=3mm,fill=cream, ultra thick, draw=red, rounded corners=2mm] 

  {\normalsize\color{darkgray}

  \begin{minipage}{8cm}\raggedright

  For type-schemes the order of bound names does not matter, and

  $\alpha$-equivalence is preserved under \alert{vacuous} binders.

  \end{minipage}};

  \end{tikzpicture}

  \end{textblock}}

  \end{frame}}

  %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%     

*}

text_raw {*

  %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

  \mode<presentation>{

  \begin{frame}<1-3>

  \frametitle{\begin{tabular}{c}Other Binding Modes\end{tabular}}

  \mbox{}\\[-3mm]

  \begin{itemize}

  \item alpha-equivalence being preserved under vacuous binders is \underline{not} always

  wanted:\bigskip\bigskip\normalsize

  \textcolor{blue}{\begin{tabular}{@ {\hspace{-8mm}}l}

  $\text{let}\;x = 3\;\text{and}\;y = 2\;\text{in}\;x - y\;\text{end}$\medskip\\

  \onslide<2->{$\;\;\;\only<2>{\approx_\alpha}\only<3>{\alert{\not\approx_\alpha}}

   \text{let}\;y = 2\;\text{and}\;x = 3\only<3->{\alert{\;\text{and}

    \;z = \text{loop}}}\;\text{in}\;x - y\;\text{end}$}

  \end{tabular}}

  \end{itemize}

  \end{frame}}

  %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%     

*}

text_raw {*

  %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

  \mode<presentation>{

  \begin{frame}<1>

  \frametitle{\begin{tabular}{c}\Large{}Even Another Binding Mode\end{tabular}}

  \mbox{}\\[-3mm]

  \begin{itemize}

  \item sometimes one wants to abstract more than one name, but the order \underline{does} matter\bigskip

  \begin{center}

  \textcolor{blue}{\begin{tabular}{@ {\hspace{-8mm}}l}

  $\text{let}\;(x, y) = (3, 2)\;\text{in}\;x - y\;\text{end}$\medskip\\

  $\;\;\;\not\approx_\alpha