Mercurial Mercurial > hg > nominal2 / comparison
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | file | latest | revisions | annotate | diff | comparison | raw | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Slides/Slides7.thy
changeset 2780 2c6851248b3f
parent 2775 5f3387b7474f
equal deleted inserted replaced
2779:3c769bf10e63 2780:2c6851248b3f 
    10   Cons  ("_::/_" [66,65] 65) 
    10   Cons  ("_::/_" [66,65] 65) 
    11 
    11 
    12 (*>*)
 
    12 (*>*)
 
    13 
    13 
    14 text_raw {*
 
    14 text_raw {*
 
    15   \renewcommand{\slidecaption}{Hefei, 15.~April 2011}
 
    15   \renewcommand{\slidecaption}{Beijing, 29.~April 2011}
 
    16 
    16 
    17   \newcommand{\abst}[2]{#1.#2}% atom-abstraction
 
    17   \newcommand{\abst}[2]{#1.#2}% atom-abstraction
 
    18   \newcommand{\pair}[2]{\langle #1,#2\rangle} % pairing
 
    18   \newcommand{\pair}[2]{\langle #1,#2\rangle} % pairing
 
    19   \newcommand{\susp}{{\boldsymbol{\cdot}}}% for suspensions
 
    19   \newcommand{\susp}{{\boldsymbol{\cdot}}}% for suspensions
 
    20   \newcommand{\unit}{\langle\rangle}% unit
 
    20   \newcommand{\unit}{\langle\rangle}% unit
 
    88   \begin{itemize}
 
    88   \begin{itemize}
 
    89   \item It is easy to make mistakes.\bigskip
 
    89   \item It is easy to make mistakes.\bigskip
 
    90   \item Theorem provers can prevent mistakes, {\bf if} the problem
 
    90   \item Theorem provers can prevent mistakes, {\bf if} the problem
 
    91   is formulated so that it is suitable for theorem provers.\bigskip
 
    91   is formulated so that it is suitable for theorem provers.\bigskip
 
    92   \item This re-formulation can be done, even in domains where
 
    92   \item This re-formulation can be done, even in domains where
 
    93   we do not expect it.
 
    93   we least expect it.
 
    94   \end{itemize}
 
    94   \end{itemize}
 
    95 
    95 
    96   \end{frame}}
 
    96   \end{frame}}
 
    97   %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%     
    97   %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%     
    98 *}
 
    98 *}
 
   235   \onslide<2->{\bl{matches$_1$ x$\cdot$(0$|$1)$^*\;$ x3}  & \bl{$\mapsto$} & \bl{false}}
 
   235   \onslide<2->{\bl{matches$_1$ x$\cdot$(0$|$1)$^*\;$ x3}  & \bl{$\mapsto$} & \bl{false}}
 
   236   \end{tabular}
 
   236   \end{tabular}
 
   237   \end{center}
 
   237   \end{center}
 
   238  
   238  
   239   \onslide<3->
 
   239   \onslide<3->
 
   240   {looks OK \ldots let's ship it to customers\hspace{5mm} 
   240   {Looks OK \ldots let's ship it to customers\hspace{5mm} 
   241    \raisebox{-5mm}{\includegraphics[scale=0.05]{sun.png}}}
 
   241    \raisebox{-5mm}{\includegraphics[scale=0.05]{sun.png}}}
 
   242   
   242   
   243   \end{frame}}
 
   243   \end{frame}}
 
   244   %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%     
   244   %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%     
   245 *}
 
   245 *}
 
   327   \bl{der c ($\varnothing$)}       & \bl{$=$} & \bl{$\varnothing$} & \\
 
   327   \bl{der c ($\varnothing$)}       & \bl{$=$} & \bl{$\varnothing$} & \\
 
   328   \bl{der c ([])}                  & \bl{$=$} & \bl{$\varnothing$} & \\
 
   328   \bl{der c ([])}                  & \bl{$=$} & \bl{$\varnothing$} & \\
 
   329   \bl{der c (d)}                   & \bl{$=$} & \bl{if c = d then [] else $\varnothing$} & \\
 
   329   \bl{der c (d)}                   & \bl{$=$} & \bl{if c = d then [] else $\varnothing$} & \\
 
   330   \bl{der c (r$_1$ + r$_2$)}       & \bl{$=$} & \bl{(der c r$_1$) + (der c r$_2$)} & \\
 
   330   \bl{der c (r$_1$ + r$_2$)}       & \bl{$=$} & \bl{(der c r$_1$) + (der c r$_2$)} & \\
 
   331   \bl{der c (r$_1$ $\cdot$ r$_2$)} & \bl{$=$} & \bl{((der c r$_1$) $\cdot$ r$_2$)} & \\
 
   331   \bl{der c (r$_1$ $\cdot$ r$_2$)} & \bl{$=$} & \bl{((der c r$_1$) $\cdot$ r$_2$)} & \\
 
   332        &          & \bl{\;\;+ (if nullable r$_1$ then der c r$_2$ else $\varnothing$)}\\
 
   332        &          & \bl{\;\;\;\;+ (if nullable r$_1$ then der c r$_2$ else $\varnothing$)}\\
 
   333   \bl{der c (r$^*$)}          & \bl{$=$} & \bl{(der c r) $\cdot$ r$^*$} &\smallskip\\
 
   333   \bl{der c (r$^*$)}          & \bl{$=$} & \bl{(der c r) $\cdot$ r$^*$} &\smallskip\\
 
   334 
   334 
   335   \bl{derivative r []}     & \bl{$=$} & \bl{r} & \\
 
   335   \bl{derivative r []}     & \bl{$=$} & \bl{r} & \\
 
   336   \bl{derivative r (c::s)} & \bl{$=$} & \bl{derivative (der c r) s} & \\
 
   336   \bl{derivative r (c::s)} & \bl{$=$} & \bl{derivative (der c r) s} & \\
 
   337   \end{tabular}\medskip
 
   337   \end{tabular}\medskip
 
   381   \bl{matches$_2$ r s = false} & \only<1>{\rd{$\Longrightarrow\,\,$}}\only<2>{\rd{$\Longleftarrow\,\,$}}%
 
   381   \bl{matches$_2$ r s = false} & \only<1>{\rd{$\Longrightarrow\,\,$}}\only<2>{\rd{$\Longleftarrow\,\,$}}%
 
   382   \only<3->{\rd{$\Longleftrightarrow$}} & \bl{s $\notin$ \LL(r)}\\
 
   382   \only<3->{\rd{$\Longleftrightarrow$}} & \bl{s $\notin$ \LL(r)}\\
 
   383   \end{tabular}
 
   383   \end{tabular}
 
   384   \end{center}
 
   384   \end{center}
 
   385   \pause\pause\bigskip
 
   385   \pause\pause\bigskip
 
   386   ??? By \alert<4->{induction}, we can {\bf prove} these properties.\bigskip
 
   386   By \alert<4->{induction}, we can {\bf prove} these properties.\bigskip
 
   387 
   387 
   388   \begin{tabular}{lrcl}
 
   388   \begin{tabular}{lrcl}
 
   389   Lemmas:  & \bl{nullable (r)}          & \bl{$\Longleftrightarrow$} & \bl{[] $\in$ \LL (r)}\\
 
   389   Lemmas:  & \bl{nullable (r)}          & \bl{$\Longleftrightarrow$} & \bl{[] $\in$ \LL (r)}\\
 
   390            & \bl{s $\in$ \LL (der c r)} & \bl{$\Longleftrightarrow$} & \bl{(c::s) $\in$ \LL (r)}\\
 
   390            & \bl{s $\in$ \LL (der c r)} & \bl{$\Longleftrightarrow$} & \bl{(c::s) $\in$ \LL (r)}\\
 
   391   \end{tabular}
 
   391   \end{tabular}
 
   522   \begin{center}
 
   522   \begin{center}
 
   523   \begin{tabular}{p{9cm}}
 
   523   \begin{tabular}{p{9cm}}
 
   524   My point:\bigskip\\
 
   524   My point:\bigskip\\
 
   525 
   525 
   526   The theory about regular languages can be reformulated 
   526   The theory about regular languages can be reformulated 
   527   to be more suitable for theorem proving.
 
   527   to be more\\ suitable for theorem proving.
 
   528   \end{tabular}
 
   528   \end{tabular}
 
   529   \end{center}
 
   529   \end{center}
 
   530   \end{frame}}
 
   530   \end{frame}}
 
   531   %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%     
   531   %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%     
   532 *}
 
   532 *}
 
   612   \item Myhill-Nerode:
 
   612   \item Myhill-Nerode:
 
   613 
   613 
   614   \begin{center}
 
   614   \begin{center}
 
   615   \begin{tabular}{l}
 
   615   \begin{tabular}{l}
 
   616   finite $\Rightarrow$ regular\\
 
   616   finite $\Rightarrow$ regular\\
 
   617   \;\;\;\smath{\text{finite}\,(U\!N\!IV /\!/ \approx_L) \Rightarrow \exists r. L = \mathbb{L}(r)}\\[3mm]
 
   617   \;\;\;\smath{\text{finite}\,(U\!N\!IV /\!/ \approx_L) \Rightarrow \exists r.\; L = \mathbb{L}(r)}\\[3mm]
 
   618   regular $\Rightarrow$ finite\\
 
   618   regular $\Rightarrow$ finite\\
 
   619   \;\;\;\smath{\text{finite}\, (U\!N\!IV /\!/ \approx_{\mathbb{L}(r)})}
 
   619   \;\;\;\smath{\text{finite}\, (U\!N\!IV /\!/ \approx_{\mathbb{L}(r)})}
 
   620   \end{tabular}
 
   620   \end{tabular}
 
   621   \end{center}
 
   621   \end{center}
 
   622 
   622 
   629 
   629 
   630 text_raw {*
 
   630 text_raw {*
 
   631   %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
 
   631   %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
 
   632   \mode<presentation>{
 
   632   \mode<presentation>{
 
   633   \begin{frame}[c]
 
   633   \begin{frame}[c]
 
   634   \frametitle{\LARGE Final States}
 
   634   \frametitle{\LARGE Final Equiv.~Classes}
 
   635 
   635 
   636   \mbox{}\\[3cm]
 
   636   \mbox{}\\[3cm]
 
   637 
   637 
   638   \begin{itemize}
 
   638   \begin{itemize}
 
   639   \item ??? \smath{\text{final}_L\,X \dn \{[|s|]_\approx\;|\; s \in X\}}\\
 
   639   \item \smath{\text{finals}\,L \dn 
       
   640      \{{\lbrack\mkern-2mu\lbrack{s}\rbrack\mkern-2mu\rbrack}_\approx\;|\; s \in L\}}\\
 
   640   \medskip
 
   641   \medskip
 
   641 
   642 
   642   \item we can prove: \smath{L = \bigcup \{X\;|\;\text{final}_L\,X\}}
 
   643   \item we can prove: \smath{L = \bigcup (\text{finals}\,L)}
 
   643 
   644 
   644   \end{itemize}
 
   645   \end{itemize}
 
   645 
   646 
   646   \end{frame}}
 
   647   \end{frame}}
 
   647   %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%     
   648   %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%     
   648 *}
 
   649 *}
 
   649 
   650 
   650 text_raw {*
 
   651 text_raw {*
 
   651   %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
 
   652   %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
 
   652   \mode<presentation>{
 
   653   \mode<presentation>{
 
   653   \begin{frame}[c]
 
   654   \begin{frame}[c]
 
   654   \frametitle{\LARGE Transitions between\\[-3mm] Equivalence Classes}
 
   655   \frametitle{\LARGE Transitions between ECs}
 
   655 
   656 
   656   \smath{L = \{[c]\}}
 
   657   \smath{L = \{[c]\}}
 
   657 
   658 
   658   \begin{tabular}{@ {\hspace{-7mm}}cc}
 
   659   \begin{tabular}{@ {\hspace{-7mm}}cc}
 
   659   \begin{tabular}{c}
 
   660   \begin{tabular}{c}
 
   723   \begin{tabular}{@ {\hspace{-6mm}}ll@ {\hspace{1mm}}c@ {\hspace{1mm}}l}
 
   724   \begin{tabular}{@ {\hspace{-6mm}}ll@ {\hspace{1mm}}c@ {\hspace{1mm}}l}
 
   724   & \smath{R_1} & \smath{\equiv} & \smath{R_1;b + R_2;b \onslide<2->{\alert<2>{+ \lambda;[]}}}\\
 
   725   & \smath{R_1} & \smath{\equiv} & \smath{R_1;b + R_2;b \onslide<2->{\alert<2>{+ \lambda;[]}}}\\
 
   725   & \smath{R_2} & \smath{\equiv} & \smath{R_1;a + R_2;a}\medskip\\
 
   726   & \smath{R_2} & \smath{\equiv} & \smath{R_1;a + R_2;a}\medskip\\
 
   726   \onslide<3->{we can prove} 
   727   \onslide<3->{we can prove} 
   727   & \onslide<3->{\smath{R_1}} & \onslide<3->{\smath{=}} 
   728   & \onslide<3->{\smath{R_1}} & \onslide<3->{\smath{=}} 
   728       & \onslide<3->{\smath{R_1; \mathbb{L}(b) \,\cup\, R_2;\mathbb{L}(b) \,\cup\, \{[]\};\{[]\}}}\\
 
   729       & \onslide<3->{\smath{R_1;; \mathbb{L}(b) \,\cup\, R_2;;\mathbb{L}(b) \,\cup\, \{[]\}}}\\
 
   729   & \onslide<3->{\smath{R_2}} & \onslide<3->{\smath{=}}    
   730   & \onslide<3->{\smath{R_2}} & \onslide<3->{\smath{=}}    
   730       & \onslide<3->{\smath{R_1; \mathbb{L}(a) \,\cup\, R_2;\mathbb{L}(a)}}\\
 
   731       & \onslide<3->{\smath{R_1;; \mathbb{L}(a) \,\cup\, R_2;;\mathbb{L}(a)}}\\
 
   731   \end{tabular}
 
   732   \end{tabular}
 
   732   \end{center}
 
   733   \end{center}
 
   733 
   734 
   734   \end{frame}}
 
   735   \end{frame}}
 
   735   %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%     
   736   %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%     
   926   \end{frame}}
 
   927   \end{frame}}
 
   927   %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%     
   928   %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%     
   928 *}
 
   929 *}
 
   929 
   930 
   930 
   931 
   931 text_raw {*
 
   932 
   932   %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
 
   933 text_raw {*
 
   933   \mode<presentation>{
 
   934   %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
 
   934   \begin{frame}[c]
 
   935   \mode<presentation>{
 
   935   \frametitle{\LARGE Other Direction}
 
   936   \begin{frame}[c]
 
   936 
   937   \frametitle{\LARGE The Other Direction}
 
       
   938   
   937   One has to prove
 
   939   One has to prove
 
   938 
   940 
   939   \begin{center}
 
   941   \begin{center}
 
   940   \smath{\text{finite} (U\!N\!IV /\!/ \approx_{\mathbb{L}(r)})}
 
   942   \smath{\text{finite} (U\!N\!IV /\!/ \approx_{\mathbb{L}(r)})}
 
   941   \end{center}
 
   943   \end{center}
 
   942 
   944 
   943   by induction on \smath{r}. Not trivial, but after a bit 
   945   by induction on \smath{r}. This is straightforward for \\the base cases:\small
 
   944   of thinking, one can prove that if
 
   946 
   945 
   947   \begin{center}
 
   946   \begin{center}
 
   948   \begin{tabular}{l@ {\hspace{1mm}}l}
 
   947   \smath{\text{finite} (U\!N\!IV /\!/ \approx_{\mathbb{L}(r_1)})}\hspace{5mm}
 
   949   \smath{U\!N\!IV /\!/ \!\approx_{\emptyset}} & \smath{= \{U\!N\!IV\}}\smallskip\\
 
       
   950   \smath{U\!N\!IV /\!/ \!\approx_{\{[]\}}} & \smath{\subseteq \{\{[]\}, U\!N\!IV - \{[]\}\}}\smallskip\\
 
       
   951   \smath{U\!N\!IV /\!/ \!\approx_{\{[c]\}}} & \smath{\subseteq \{\{[]\}, \{[c]\}, U\!N\!IV - \{[], [c]\}\}}
 
       
   952   \end{tabular}
 
       
   953   \end{center}
 
       
   954 
       
   955   
       
   956   \end{frame}}
 
       
   957   %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%     
       
   958 *}
 
       
   959 
       
   960 
       
   961 text_raw {*
 
       
   962   %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
 
       
   963   \mode<presentation>{
 
       
   964   \begin{frame}[t]
 
       
   965   \frametitle{\LARGE The Other Direction}
 
       
   966 
       
   967   More complicated are the inductive cases:\\ one needs to prove that if
 
       
   968 
       
   969   \begin{center}
 
       
   970   \smath{\text{finite} (U\!N\!IV /\!/ \approx_{\mathbb{L}(r_1)})}\hspace{3mm}
 
   948   \smath{\text{finite} (U\!N\!IV /\!/ \approx_{\mathbb{L}(r_2)})}
 
   971   \smath{\text{finite} (U\!N\!IV /\!/ \approx_{\mathbb{L}(r_2)})}
 
   949   \end{center}
 
   972   \end{center}
 
   950 
   973 
   951   then
 
   974   then
 
   952 
   975 
   953   \begin{center}
 
   976   \begin{center}
 
   954   \smath{\text{finite} (U\!N\!IV /\!/ \approx_{\mathbb{L}(r_1) \,\cup\, \mathbb{L}(r_2)})}
 
   977   \smath{\text{finite} (U\!N\!IV /\!/ \approx_{\mathbb{L}(r_1) \,\cup\, \mathbb{L}(r_2)})}
 
   955   \end{center}
 
   978   \end{center}
 
   956   
   979   
   957   
   980   \end{frame}}
 
   958 
   981   %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%     
       
   982 *}
 
       
   983 
       
   984 
       
   985 text_raw {*
 
       
   986   %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
 
       
   987   \mode<presentation>{
 
       
   988   \begin{frame}[t]
 
       
   989   \frametitle{\LARGE Helper Lemma}
 
       
   990 
       
   991   \begin{center}
 
       
   992   \begin{tabular}{p{10cm}}
 
       
   993   %If \smath{\text{finite} (f\;' A)} and \smath{f} is injective 
       
   994   %(on \smath{A}),\\ then \smath{\text{finite}\,A}.
 
       
   995   Given two equivalence relations \smath{R_1} and \smath{R_2} with
 
       
   996   \smath{R_1} refining \smath{R_2} (\smath{R_1 \subseteq R_2}).\\ 
       
   997   Then\medskip\\
 
       
   998   \smath{\;\;\text{finite} (U\!N\!IV /\!/ R_1) \Rightarrow \text{finite} (U\!N\!IV /\!/ R_2)}
 
       
   999   \end{tabular}
 
       
  1000   \end{center}
 
       
  1001   
       
  1002   \end{frame}}
 
       
  1003   %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%     
       
  1004 *}
 
       
  1005 
       
  1006 text_raw {*
 
       
  1007   %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
 
       
  1008   \mode<presentation>{
 
       
  1009   \begin{frame}[c]
 
       
  1010   \frametitle{\Large Derivatives and Left-Quotients}
 
       
  1011   \small
 
       
  1012   Work by Brozowski ('64) and Antimirov ('96):\pause\smallskip
 
       
  1013 
       
  1014 
       
  1015   \begin{tabular}{@ {}l@ {\hspace{2mm}}c@ {\hspace{2mm}}l@ {\hspace{-10mm}}l@ {}}
 
       
  1016   \multicolumn{4}{@ {}l}{Left-Quotient:}\\
 
       
  1017   \multicolumn{4}{@ {}l}{\bl{$\text{Ders}\;\text{s}\,A \dn \{\text{s'} \;|\; \text{s @ s'} \in A\}$}}\bigskip\\
 
       
  1018 
       
  1019   \multicolumn{4}{@ {}l}{Derivative:}\\
 
       
  1020   \bl{der c ($\varnothing$)}       & \bl{$=$} & \bl{$\varnothing$} & \\
 
       
  1021   \bl{der c ([])}                  & \bl{$=$} & \bl{$\varnothing$} & \\
 
       
  1022   \bl{der c (d)}                   & \bl{$=$} & \bl{if c = d then [] else $\varnothing$} & \\
 
       
  1023   \bl{der c (r$_1$ + r$_2$)}       & \bl{$=$} & \bl{(der c r$_1$) + (der c r$_2$)} & \\
 
       
  1024   \bl{der c (r$_1$ $\cdot$ r$_2$)} & \bl{$=$} & \bl{((der c r$_1$) $\cdot$ r$_2$)} & \\
 
       
  1025        &          & \bl{\;\;\;\;+ (if nullable r$_1$ then der c r$_2$ else $\varnothing$)}\\
 
       
  1026   \bl{der c (r$^*$)}          & \bl{$=$} & \bl{(der c r) $\cdot$ r$^*$} &\smallskip\\
 
       
  1027 
       
  1028   \bl{ders [] r}     & \bl{$=$} & \bl{r} & \\
 
       
  1029   \bl{ders (s @ [c]) r} & \bl{$=$} & \bl{der c (ders s r)} & \\
 
       
  1030   \end{tabular}\pause
 
       
  1031 
       
  1032   \begin{center}
 
       
  1033   \alert{$\Rightarrow$}\smath{\;\;\text{Ders}\,\text{s}\,(\mathbb{L}(\text{r})) = \mathbb{L} (\text{ders s r})}
 
       
  1034   \end{center}
 
       
  1035   
       
  1036   \end{frame}}
 
       
  1037   %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%     
       
  1038 *}
 
       
  1039 
       
  1040 text_raw {*
 
       
  1041   %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
 
       
  1042   \mode<presentation>{
 
       
  1043   \begin{frame}[c]
 
       
  1044   \frametitle{\LARGE Left-Quotients and MN-Rels}
 
       
  1045 
       
  1046   \begin{itemize}
 
       
  1047   \item \smath{x \approx_{A} y \,\dn\, \forall z.\; x @ z \in A \Leftrightarrow y @ z \in A}\medskip
 
       
  1048   \item \bl{$\text{Ders}\;s\,A \dn \{s' \;|\; s @ s' \in A\}$}
 
       
  1049   \end{itemize}\bigskip
 
       
  1050 
       
  1051   \begin{center}
 
       
  1052   \smath{x \approx_A y  \Longleftrightarrow \text{Ders}\;x\;A = \text{Ders}\;y\;A}
 
       
  1053   \end{center}\bigskip\pause\small
 
       
  1054 
       
  1055   which means
 
       
  1056 
       
  1057   \begin{center}
 
       
  1058   \smath{x \approx_{\mathbb{L}(r)} y  \Longleftrightarrow 
       
  1059   \mathbb{L}(\text{ders}\;x\;r) = \mathbb{L}(\text{ders}\;y\;r)}
 
       
  1060   \end{center}\pause
 
       
  1061 
       
  1062   \hspace{8.8mm}or
 
       
  1063   \smath{\;x \approx_{\mathbb{L}(r)} y  \Longleftarrow 
       
  1064   \text{ders}\;x\;r = \text{ders}\;y\;r}
 
       
  1065 
       
  1066   
       
  1067 
       
  1068   \end{frame}}
 
       
  1069   %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%     
       
  1070 *}
 
       
  1071 
       
  1072 text_raw {*
 
       
  1073   %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
 
       
  1074   \mode<presentation>{
 
       
  1075   \begin{frame}[c]
 
       
  1076   \frametitle{\LARGE Partial Derivatives}
 
       
  1077 
       
  1078   Antimirov: \bl{pder : rexp $\Rightarrow$ rexp set}\bigskip
 
       
  1079 
       
  1080   \begin{tabular}{@ {}l@ {\hspace{2mm}}c@ {\hspace{2mm}}l@ {\hspace{-10mm}}l@ {}}
 
       
  1081   \bl{pder c ($\varnothing$)}       & \bl{$=$} & \bl{\{$\varnothing$\}} & \\
 
       
  1082   \bl{pder c ([])}                  & \bl{$=$} & \bl{\{$\varnothing$\}} & \\
 
       
  1083   \bl{pder c (d)}                   & \bl{$=$} & \bl{if c = d then \{[]\} else \{$\varnothing$\}} & \\
 
       
  1084   \bl{pder c (r$_1$ + r$_2$)}       & \bl{$=$} & \bl{(pder c r$_1$) $\cup$ (pder c r$_2$)} & \\
 
       
  1085   \bl{pder c (r$_1$ $\cdot$ r$_2$)} & \bl{$=$} & \bl{(pder c r$_1$) $\odot$ r$_2$} & \\
 
       
  1086        &          & \bl{\hspace{-10mm}$\cup$ (if nullable r$_1$ then pder c r$_2$ else $\varnothing$)}\\
 
       
  1087   \bl{pder c (r$^*$)}          & \bl{$=$} & \bl{(pder c r) $\odot$ r$^*$} &\smallskip\\
 
       
  1088   \end{tabular}
 
       
  1089 
       
  1090   \begin{tabular}{@ {}l@ {\hspace{2mm}}c@ {\hspace{2mm}}l@ {\hspace{-10mm}}l@ {}}
 
       
  1091   \bl{pders [] r}     & \bl{$=$} & \bl{r} & \\
 
       
  1092   \bl{pders (s @ [c]) r} & \bl{$=$} & \bl{pder c (pders s r)} & \\
 
       
  1093   \end{tabular}\pause
 
       
  1094 
       
  1095   \begin{center}
 
       
  1096   \alert{$\Rightarrow$}\smath{\;\;\text{Ders}\,\text{s}\,(\mathbb{L}(\text{r})) = \bigcup (\mathbb{L}\;`\; (\text{pders s r}))}
 
       
  1097   \end{center}
 
       
  1098 
       
  1099   \end{frame}}
 
       
  1100   %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%     
       
  1101 *}
 
       
  1102 
       
  1103 text_raw {*
 
       
  1104   %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
 
       
  1105   \mode<presentation>{
 
       
  1106   \begin{frame}[t]
 
       
  1107   \frametitle{\LARGE Final Result}
 
       
  1108   
       
  1109   \mbox{}\\[7mm]
 
       
  1110 
       
  1111   \begin{itemize}
 
       
  1112   \item \alt<1>{\smath{\text{pders x r \mbox{$=$} pders y r}}}
 
       
  1113             {\smath{\underbrace{\text{pders x r \mbox{$=$} pders y r}}_{R_1}}} 
       
  1114         refines \bl{x $\approx_{\mathbb{L}(\text{r})}$ y}\pause
 
       
  1115   \item \smath{\text{finite} (U\!N\!IV /\!/ R_1)} \bigskip\pause
 
       
  1116   \item Therefore \smath{\text{finite} (U\!N\!IV /\!/ \approx_{\mathbb{L}(r)})}. Qed.
 
       
  1117   \end{itemize}
 
       
  1118   
   959   \end{frame}}
 
  1119   \end{frame}}
 
   960   %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%     
  1120   %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%     
   961 *}
 
  1121 *}
 
   962 
  1122 
   963 
  1123
nominal2