\documentclass[dvipsnames,14pt,t]{beamer}

\usepackage{../slides}

\usepackage{../graphics}

\usepackage{../langs}

\usepackage{../data}

\hfuzz=220pt 

\lstset{language=Scala,

        style=mystyle,

        numbersep=0pt,

        numbers=none,

        xleftmargin=0mm}

\newcommand{\bl}[1]{\textcolor{blue}{#1}}     

% beamer stuff 

\renewcommand{\slidecaption}{AFL 02, King's College London}

\begin{document}

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

\frametitle{%

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

  \\[-3mm]

  \LARGE Automata and \\[-2mm] 

  \LARGE Formal Languages (2)\\[3mm] 

  \end{tabular}}

  \begin{center}

  \begin{tabular}{ll}

  Email:  & christian.urban at kcl.ac.uk\\

  Office: & S1.27 (1st floor Strand Building)\\

  Slides: & KEATS 

  \end{tabular}

  \end{center}

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

\begin{frame}[c]

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

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

\mode<presentation>{

\begin{frame}[t]

\frametitle{\begin{tabular}{c}Strings\end{tabular}}

Different ways of writing strings:

\begin{center}

\begin{tabular}{ccc}

\bl{\consolas"$hello$"}\quad{} &  \bl{$[h, e, l, l, o]$} & \quad\bl{$h\!::\!e\!::\!l\!::\!l\!::\!o\!::\!N\!il$}\bigskip\\

\bl{\consolas ""}       &       \bl{$[]$}                & \bl{$N$\!$il$}

\end{tabular}

\end{center}\pause

The concatenation operation on strings and sets of strings:

\begin{center}

\begin{tabular}{l}

\bl{{\consolas"$f\!oo$"}$\;@\;${\consolas"$bar$"}$\;=\;${\consolas"$f\!oobar$"}}\medskip\\

\bl{$A \;@\; B \dn \{ s_1 @ s_2 \mid s_1 \in A \wedge s_2 \in B\}$}

\end{tabular}

\end{center}

\end{frame}}

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

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

\mode<presentation>{

\begin{frame}[t]

\frametitle{\begin{tabular}{c}Regular Expressions\end{tabular}}

Their inductive definition:

\begin{textblock}{6}(2,6.5)

  \begin{tabular}{@ {}rrl@ {\hspace{13mm}}l}

  \bl{$r$} & \bl{$::=$}  & \bl{$\varnothing$}  & null\\

         & \bl{$\mid$} & \bl{$\epsilon$}        & empty string / {\consolas""} / $[]$\\

         & \bl{$\mid$} & \bl{$c$}                         & character\\

         & \bl{$\mid$} & \bl{$r_1 \cdot r_2$} & sequence\\

         & \bl{$\mid$} & \bl{$r_1 + r_2$}  & alternative / choice\\

         & \bl{$\mid$} & \bl{$r^*$}                   & star (zero or more)\\

  \end{tabular}

  \end{textblock}

\only<2->{

\begin{textblock}{9}(4,0.5)

\begin{tikzpicture}

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

{\normalsize\color{darkgray}

\begin{minipage}{9cm}

\hspace{5mm}\mbox{{\lstset{language=Scala}\fontsize{8}{10}\selectfont

\texttt{\lstinputlisting{../progs/app51.scala}}}}

\end{minipage}};

\end{tikzpicture}

\end{textblock}}

\end{frame}}

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

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

\mode<presentation>{

\begin{frame}[c]

\frametitle{\begin{tabular}{c}The Meaning of a\\[-2mm] Regular Expression\end{tabular}}

\begin{textblock}{15}(1,4)

 \begin{tabular}{@ {}rcl}

 \bl{$L(\varnothing)$}     & \bl{$\dn$} & \bl{$\varnothing$}\\

 \bl{$L(\epsilon)$}          & \bl{$\dn$} & \bl{$\{$""$\}$}\\

 \bl{$L(c)$}                     & \bl{$\dn$} & \bl{$\{"c"\}$}\\

 \bl{$L(r_1 + r_2)$}        & \bl{$\dn$} & \bl{$L(r_1) \cup L(r_2)$}\\

 \bl{$L(r_1 \cdot r_2)$}  & \bl{$\dn$} & \bl{$L(r_1) \,@\, L(r_2)$}\\

 \bl{$L(r^*)$}                   & \bl{$\dn$} & \bl{$\bigcup_{n \ge 0} L(r)^n$}\\

  \end{tabular}\bigskip

\only<2->{  

\hspace{5mm}\textcolor{blue}{$L(r)^0 \;\dn\; \{""\}$}\\

\textcolor{blue}{$L(r)^{n+1} \;\dn\; L(r) \,@\, L(r)^n$}}  

\end{textblock}

\only<1->{

\begin{textblock}{6}(9,12)\small

\bl{$L$} is a function from regular expressions to sets of strings\\

\bl{$L$ : Rexp $\Rightarrow$ Set$[$String$]$}

\end{textblock}}

\end{frame}}

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

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

\mode<presentation>{

\begin{frame}[c]

\large

\begin{center}

What is \bl{$L(a^*)$}?

\end{center}  

\end{frame}}

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

\newcommand{\YES}{\textcolor{gray}{yes}}

\newcommand{\NO}{\textcolor{gray}{no}}

\newcommand{\FORALLR}{\textcolor{gray}{$\forall$ r.}}

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

\mode<presentation>{

\begin{frame}[c]

\frametitle{\begin{tabular}{c}Reg Exp Equivalences\end{tabular}}

\begin{center}

\begin{tabular}{l@ {\hspace{7mm}}rcl@ {\hspace{7mm}}l}

&\bl{$(a + b)  + c$} & \bl{$\equiv^?$} & \bl{$a + (b + c)$} & \onslide<2->{\YES}\\

&\bl{$a + a$} & \bl{$\equiv^?$} & \bl{$a$} & \onslide<3->{\YES}\\

&\bl{$(a \cdot b)  \cdot c$} & \bl{$\equiv^?$} & \bl{$a \cdot (b \cdot c)$} & \onslide<4->{\YES}\\

&\bl{$a \cdot a$} & \bl{$\equiv^?$} & \bl{$a$} & \onslide<5->{\NO}\\

&\bl{$\epsilon^*$} & \bl{$\equiv^?$} & \bl{$\epsilon$} & \onslide<6->{\YES}\\

&\bl{$\varnothing^*$} & \bl{$\equiv^?$} & \bl{$\varnothing$} & \onslide<7->{\NO}\\

\FORALLR &\bl{$r \cdot \epsilon$} & \bl{$\equiv^?$} & \bl{$r$} & \onslide<8->{\YES}\\

\FORALLR &\bl{$r + \epsilon$} & \bl{$\equiv^?$} & \bl{$r$} & \onslide<9->{\NO}\\

\FORALLR &\bl{$r + \varnothing$} & \bl{$\equiv^?$} & \bl{$r$} & \onslide<10->{\YES}\\

\FORALLR &\bl{$r \cdot \varnothing$} & \bl{$\equiv^?$} & \bl{$r$} & \onslide<11->{\NO}\\

&\bl{$c \cdot (a + b)$} & \bl{$\equiv^?$} & \bl{$(c \cdot a) + (c \cdot b)$} & \onslide<12->{\YES}\\

&\bl{$a^*$} & \bl{$\equiv^?$} & \bl{$\epsilon + (a \cdot a^*)$} & \onslide<13->{\YES}

\end{tabular}

\end{center}

\end{frame}}

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

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

\mode<presentation>{

\begin{frame}[c]

\frametitle{\begin{tabular}{c}The Specification\\[-1mm] for Matching\end{tabular}}

\large

a regular expression \bl{$r$} matches a string \bl{$s$}\\ if and only if

\begin{center}

\bl{$s \in L(r)$}\\ 

\end{center}\bigskip\bigskip\pause

\end{frame}}

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

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

\mode<presentation>{

\begin{frame}[t]

\frametitle{\begin{tabular}{c}\bl{$(a?\{n\}) \cdot a\{n\}$}\end{tabular}}

\mbox{}\\[-13mm]

\begin{tikzpicture}[y=.2cm, x=.3cm]

 	%axis

	\draw (0,0) -- coordinate (x axis mid) (30,0);

    	\draw (0,0) -- coordinate (y axis mid) (0,30);

    	%ticks

    	\foreach \x in {0,5,...,30}

     		\draw (\x,1pt) -- (\x,-3pt)

			node[anchor=north] {\x};

    	\foreach \y in {0,5,...,30}

     		\draw (1pt,\y) -- (-3pt,\y) 

     			node[anchor=east] {\y}; 

	%labels      

	\node[below=0.6cm] at (x axis mid) {\bl{a}s};

	\node[rotate=90, left=1.2cm] at (y axis mid) {secs};

	%plots

	\draw[color=blue] plot[mark=*, mark options={fill=white}] 

		file {re-python.data};

	\draw[color=brown] plot[mark=pentagon*, mark options={fill=white} ] 

		file {re-ruby.data};

	%legend

	\begin{scope}[shift={(4,20)}] 

	\draw[color=blue] (0,0) -- 

		plot[mark=*, mark options={fill=white}] (0.25,0) -- (0.5,0) 

		node[right]{\small Python};

	\draw[yshift=-\baselineskip, color=brown] (0,0) -- 

		plot[mark=pentagon*, mark options={fill=white}] (0.25,0) -- (0.5,0)

		node[right]{\small Ruby};

	\end{scope}

\end{tikzpicture}

\end{frame}}

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

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

\mode<presentation>{

\begin{frame}[c]

\frametitle{\begin{tabular}{c}Evil Regular Expressions\end{tabular}}

\begin{itemize}

\item \alert{R}egular \alert{e}xpression \alert{D}enial \alert{o}f \alert{S}ervice (ReDoS)\bigskip

\item Evil regular expressions\medskip

\begin{itemize}

\item \bl{$(a?\{n\}) \cdot a\{n\}$}

\item \bl{$(a^+)^+$}

\item \bl{$([a$\,-\,$z]^+)^*$}

\item \bl{$(a + a \cdot a)^+$}

\item \bl{$(a + a?)^+$}

\end{itemize}

\end{itemize}

\end{frame}}

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

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

\mode<presentation>{

\begin{frame}[t]

\frametitle{\begin{tabular}{c}A Matching Algorithm\end{tabular}}

\small

\ldots{}whether a regular expression can match the empty string:

\begin{center}

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

\bl{$nullable(\varnothing)$}      & \bl{$\dn$} & \bl{$f\!\/alse$}\\

\bl{$nullable(\epsilon)$}           & \bl{$\dn$} &  \bl{$true$}\\

\bl{$nullable (c)$}                    & \bl{$\dn$} &  \bl{$f\!alse$}\\

\bl{$nullable (r_1 + r_2)$}       & \bl{$\dn$} &  \bl{$nullable(r_1) \vee nullable(r_2)$} \\ 

\bl{$nullable (r_1 \cdot r_2)$} & \bl{$\dn$} &  \bl{$nullable(r_1) \wedge nullable(r_2)$} \\

\bl{$nullable (r^*)$}                 & \bl{$\dn$} & \bl{$true$} \\

\end{tabular}

\end{center}

\only<2->{

\begin{textblock}{9}(3.4,10)

\begin{tikzpicture}

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

{\normalsize\color{darkgray}

\begin{minipage}{9cm}

\hspace{5mm}\mbox{{\lstset{language=Scala}\fontsize{8}{10}\selectfont

\texttt{\lstinputlisting{../progs/app5.scala}}}}

\end{minipage}};

\end{tikzpicture}

\end{textblock}}

\end{frame}}

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

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

\mode<presentation>{

\begin{frame}[c]

\frametitle{\begin{tabular}{c}The Derivative of a Rexp\end{tabular}}

\large

If \bl{$r$} matches the string \bl{$c\!::\!s$}, what is a regular expression that matches \bl{$s$}?\bigskip\bigskip\bigskip\bigskip

\small

\bl{$der\,c\,r$} gives the answer

\end{frame}}

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

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

\mode<presentation>{

\begin{frame}[c]

\frametitle{\begin{tabular}{c}The Derivative of a Rexp (2)\end{tabular}}

\begin{center}

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

  \bl{$der\, c\, (\varnothing)$}      & \bl{$\dn$} & \bl{$\varnothing$} & \\

  \bl{$der\, c\, (\epsilon)$}           & \bl{$\dn$} & \bl{$\varnothing$} & \\

  \bl{$der\, c\, (d)$}                     & \bl{$\dn$} & \bl{if $c = d$ then $\epsilon$ else $\varnothing$} & \\

  \bl{$der\, c\, (r_1 + r_2)$}        & \bl{$\dn$} & \bl{$der\, c\, r_1 + der\, c\, r_2$} & \\

  \bl{$der\, c\, (r_1 \cdot r_2)$}  & \bl{$\dn$}  & \bl{if $nullable (r_1)$}\\

  & & \bl{then $(der\,c\,r_1) \cdot r_2 + der\, c\, r_2$}\\ 

  & & \bl{else $(der\, c\, r_1) \cdot r_2$}\\

  \bl{$der\, c\, (r^*)$}          & \bl{$\dn$} & \bl{$(der\,c\,r) \cdot (r^*)$} &\smallskip\\\pause

  \bl{$der\!s\, []\, r$}     & \bl{$\dn$} & \bl{$r$} & \\

  \bl{$der\!s\, (c\!::\!s)\, r$} & \bl{$\dn$} & \bl{$der\!s\,s\,(der\,c\,r)$} & \\

  \end{tabular}

\end{center}

\only<3->{

\begin{textblock}{10.5}(2,5)

\begin{tikzpicture}

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

{\normalsize\color{darkgray}

\begin{minipage}{10.5cm}

\hspace{5mm}\mbox{{\lstset{language=Scala}\fontsize{8}{10}\selectfont

\texttt{\lstinputlisting{../progs/app6.scala}}}}

\end{minipage}};

\end{tikzpicture}

\end{textblock}}

\end{frame}}

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

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

\mode<presentation>{

\begin{frame}[c]

\frametitle{\begin{tabular}{c}Examples\end{tabular}}

Given \bl{$r \dn ((a \cdot b) + b)^*$} what is

\begin{center}

\begin{tabular}{l}

\bl{$der\,a\,r$}\\

\bl{$der\,b\,r$}

\end{tabular}

\end{center}

\end{frame}}

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

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

\mode<presentation>{

\begin{frame}[t]

\frametitle{\begin{tabular}{c}\bl{$(a?\{n\}) \cdot a\{n\}$}\end{tabular}}

\mbox{}\\[-13mm]

\begin{tikzpicture}[y=.2cm, x=.3cm]

 	%axis

	\draw (0,0) -- coordinate (x axis mid) (30,0);

    	\draw (0,0) -- coordinate (y axis mid) (0,30);

    	%ticks

    	\foreach \x in {0,5,...,30}

     		\draw (\x,1pt) -- (\x,-3pt)

			node[anchor=north] {\x};

    	\foreach \y in {0,5,...,30}

     		\draw (1pt,\y) -- (-3pt,\y) 

     			node[anchor=east] {\y}; 

	%labels      

	\node[below=0.6cm] at (x axis mid) {\bl{a}s};

	\node[rotate=90, left=1.2cm] at (y axis mid) {secs};

	%plots

	\draw[color=blue] plot[mark=*, mark options={fill=white}] 

		file {re-python.data};

	\draw[color=red] plot[mark=triangle*, mark options={fill=white} ] 

		file {re1.data};

         \draw[color=brown] plot[mark=pentagon*, mark options={fill=white} ] 

		file {re-ruby.data};

	%legend

	\begin{scope}[shift={(4,20)}] 

	\draw[color=blue] (0,0) -- 

		plot[mark=*, mark options={fill=white}] (0.25,0) -- (0.5,0) 

		node[right]{\small Python};

	\draw[yshift=-\baselineskip, color=brown] (0,0) -- 

		plot[mark=pentagon*, mark options={fill=white}] (0.25,0) -- (0.5,0)

		node[right]{\small Ruby};

        \draw[yshift=\baselineskip, color=red] (0,0) -- 

		plot[mark=triangle*, mark options={fill=white}] (0.25,0) -- (0.5,0)

		node[right]{\small Scala V1};	

	\end{scope}

\end{tikzpicture}

\end{frame}}

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

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

\mode<presentation>{

\begin{frame}[t]

\frametitle{\begin{tabular}{c}Proofs about Rexps\end{tabular}}

Remember their inductive definition:\\[5cm]

\begin{textblock}{6}(5,5)

  \begin{tabular}{@ {}rrl}

  \bl{$r$} & \bl{$::=$}  & \bl{$\varnothing$}\\

         & \bl{$\mid$} & \bl{$\epsilon$}       \\

         & \bl{$\mid$} & \bl{$c$}                        \\

         & \bl{$\mid$} & \bl{$r_1 \cdot r_2$}\\

         & \bl{$\mid$} & \bl{$r_1 + r_2$}  \\

         & \bl{$\mid$} & \bl{$r^*$}                  \\

  \end{tabular}

  \end{textblock}

If we want to prove something, say a property \bl{$P(r)$}, for all regular expressions \bl{$r$} then \ldots

\end{frame}}

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

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

\mode<presentation>{

\begin{frame}[c]

\frametitle{\begin{tabular}{c}Proofs about Rexp (2)\end{tabular}}

\begin{itemize}

\item \bl{$P$} holds for \bl{$\varnothing$}, \bl{$\epsilon$} and \bl{c}\bigskip

\item \bl{$P$} holds for \bl{$r_1 + r_2$} under the assumption that \bl{$P$} already

holds for \bl{$r_1$} and \bl{$r_2$}.\bigskip

\item \bl{$P$} holds for \bl{$r_1 \cdot r_2$} under the assumption that \bl{$P$} already

holds for \bl{$r_1$} and \bl{$r_2$}.\bigskip

\item \bl{$P$} holds for \bl{$r^*$} under the assumption that \bl{$P$} already

holds for \bl{$r$}.

\end{itemize}

\end{frame}}

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

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

\mode<presentation>{

\begin{frame}[c]

\frametitle{\begin{tabular}{c}Proofs about Rexp (3)\end{tabular}}

Assume \bl{$P(r)$} is the property:

\begin{center}

\bl{$nullable(r)$} if and only if \bl{$"" \in L(r)$}

\end{center}

\end{frame}}

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

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

\mode<presentation>{

\begin{frame}[c]

\frametitle{\begin{tabular}{c}Proofs about Rexp (4)\end{tabular}}

Let \bl{$Der\,c\,A$} be the set defined as

\begin{center}

\bl{$Der\,c\,A \dn \{ s \;|\;  c\!::\!s \in A\}$ } 

\end{center}

We can prove

\begin{center}