# HG changeset patch # User Christian Urban # Date 1304494024 -28800 # Node ID 5f3387b7474f6d44b42622e8308dca8d8af684b4 # Parent d19bfc6e76313bdf6e7b9123de857c42a8fa6448 more on pearl-paper diff -r d19bfc6e7631 -r 5f3387b7474f Pearl-jv/Paper.thy --- a/Pearl-jv/Paper.thy Mon May 02 13:01:02 2011 +0800 +++ b/Pearl-jv/Paper.thy Wed May 04 15:27:04 2011 +0800 @@ -290,7 +290,7 @@ a function in @{typ perm}. One advantage of using functions as a representation for - permutations is that it is unique. For example the swappings + permutations is that it is a unique representation. For example the swappings \begin{isabelle}\ \ \ \ \ \ \ \ \ \ %%% \begin{tabular}{@ {}l} @@ -352,7 +352,7 @@ \end{isabelle} \noindent - whereby @{text "\"} is a generic type for @{text x}. The definition of this operation will be + whereby @{text "\"} is a generic type for the object @{text x}. The definition of this operation will be given by in terms of `induction' over this generic type. The type-class mechanism of Isabelle/HOL \cite{Wenzel04} allows us to give a definition for `base' types, such as atoms, permutations, booleans and natural numbers: @@ -435,7 +435,7 @@ \noindent Note that the permutation operation for functions is defined so that - we have for applications the property + we have for applications the equation \begin{isabelle}\ \ \ \ \ \ \ \ \ \ %%% @{text "\ \ (f x) ="} @@ -444,7 +444,7 @@ \end{isabelle} \noindent - whenever the permutation properties hold for @{text x}. This property can + whenever the permutation properties hold for @{text x}. This equation can be easily shown by unfolding the permutation operation for functions on the right-hand side, simplifying the beta-redex and eliminating the permutations in front of @{text x} using \eqref{cancel}. @@ -454,7 +454,7 @@ are satisfied to Isabelle/HOL's type system: we only have to establish that base types satisfy them and that type-constructors preserve them. Isabelle/HOL will use this information and determine - whether an object @{text x} with a compound type satisfies the + whether an object @{text x} with a compound type, like @{typ "atom \ (atom set * nat)"}, satisfies the permutation properties. For this we define the notion of a \emph{permutation type}: @@ -506,13 +506,13 @@ \end{isabelle} \noindent - where @{text c} stands for constants and @{text x} for - variables. - We assume HOL-terms are fully typed, but for the sake of - greater legibility we leave the typing information implicit. We - also assume the usual notions for free and bound variables of a - HOL-term. Furthermore, it is custom in HOL to regard terms as equal - modulo alpha-, beta- and eta-equivalence. + where @{text c} stands for constants and @{text x} for variables. + We assume HOL-terms are fully typed, but for the sake of greater + legibility we leave the typing information implicit. We also assume + the usual notions for free and bound variables of a HOL-term. + Furthermore, HOL-terms are regarded as equal modulo alpha-, beta- + and eta-equivalence. Statements in HOL are HOL-terms of type @{text + "bool"}. An \emph{equivariant} HOL-term is one that is invariant under the permutation operation. This can be defined in Isabelle/HOL @@ -546,11 +546,11 @@ \eqref{cancel}. To see the other direction, we use \eqref{permutefunapp}. Similarly for HOL-terms that take more than one argument. The point to note is that equivariance and equivariance in fully - applied form are (for permutation types) always interderivable. + applied form are always interderivable (for permutation types). Both formulations of equivariance have their advantages and disadvantages: \eqref{altequivariance} is usually more convenient to - establish, since statements in Isabelle/HOL are commonly given in a + establish, since statements in HOL are commonly given in a form where functions are fully applied. For example we can easily show that equality is equivariant @@ -579,41 +579,91 @@ \noindent for all @{text a}, @{text b} and @{text \}. Also the booleans @{const True} and @{const False} are equivariant by the definition - of the permutation operation for booleans. It is easy to see - that the boolean operators, like @{text "\"}, @{text "\"}, @{text - "\"} and @{text "\"}, are equivariant too; for example we have + of the permutation operation for booleans. Given this definition, it + is also easy to see that the boolean operators, like @{text "\"}, + @{text "\"}, @{text "\"} and @{text "\"} are equivariant too: \begin{isabelle}\ \ \ \ \ \ \ \ \ \ %%% \begin{tabular}{@ {}lcl} @{text "\ \ (A \ B) = (\ \ A) \ (\ \ B)"}\\ + @{text "\ \ (A \ B) = (\ \ A) \ (\ \ B)"}\\ @{text "\ \ (A \ B) = (\ \ A) \ (\ \ B)"}\\ + @{text "\ \ (\A) = \(\ \ A)"}\\ \end{tabular} \end{isabelle} - - \noindent - by the definition of the permutation operation acting on booleans. In contrast, the advantage of Definition \ref{equivariance} is that - it leads to a relatively simple rewrite system that allows us to `push' a permutation - towards the leaves of a HOL-term (i.e.~constants and - variables). Then the permutation disappears in cases where the - constants are equivariant. We have implemented this rewrite system - as a simplification tactic on the ML-level of Isabelle/HOL. Having this tactic - at our disposal, together with a collection of constants for which - equivariance is already established, we can automatically establish - equivariance of a constant for which equivariance is not yet known. For this we only have to - make sure that the definiens of this constant - is a HOL-term whose constants are all equivariant. In what follows - we shall specify this tactic and argue that it terminates and - is correct (in the sense of pushing a - permutation @{text "\"} inside a term and the only remaining - instances of @{text "\"} are in front of the term's free variables). + it leads to rewrite system that allows us to + `push' a permutation towards the leaves of a HOL-term + (i.e.~constants and variables). Then the permutation disappears in + cases where the constants are equivariant. This can be stated more + formally as the following \emph{equivariance principle}: + + \begin{theorem}[Equivariance Principle]\label{eqvtprin} + Suppose a HOL-term @{text t} whose constants are all equivariant. For any + permutation @{text \}, let @{text t'} be the HOL-term @{text t} except every + free variable @{text x} in @{term t} is replaced by @{text "\ \ x"}, then + @{text "\ \ t = t'"}. + \end{theorem} + + \noindent + The significance of this principle is that we can automatically establish + the equivariance of a constant for which equivariance is not yet + known. For this we only have to make sure that the definiens of this + constant is a HOL-term whose constants are all equivariant. For example + the universal quantifier @{text "All"}, also written @{text "\"}, is + of type @{text "(\ \ bool) \ bool"} and in HOL is definied as + + \begin{isabelle}\ \ \ \ \ \ \ \ \ \ %%% + @{thm All_def[no_vars]} + \end{isabelle} + + \noindent + Now @{text All} must be equivariant, because by the equivariance + principle we only have to test whether the contants in the HOL-term + @{thm (rhs) All_def[no_vars]}, namely @{text "="} and @{text + "True"}, are equivariant. We shown this above. Taking all equations + together, we can establish + + \begin{isabelle}\ \ \ \ \ \ \ \ \ \ %%% + @{text "\ \ (All P) \ \ \ (P = (\x. True)) = ((\ \ P) = (\x. True)) \ All (\ \ P)"} + \end{isabelle} - The simplifiaction tactic is a rewrite systems consisting of four `oriented' - equations. We will first give a naive version of this tactic, which however - is in some cornercases incorrect and does not terminate, and then modify - it in order to obtain the desired properties. A permutation @{text \} can - be pushed into applications and abstractions as follows + \noindent + where the equation in the `middle' is given by Theorem~\ref{eqvtprin}. + As a consequence, the constant @{text "All"} is equivariant. Given this + fact we can further show that the existential quantifier @{text Ex}, + written also as @{text "\"}, is equivariant, since it is defined as + + \begin{isabelle}\ \ \ \ \ \ \ \ \ \ %%% + @{thm Ex_def[no_vars]} + \end{isabelle} + + \noindent + and the HOL-term on the right-hand side contains equivariant constants only + (namely @{text "\"} and @{text "\"}). In this way we can establish step by step + equivariance for constants in HOL. + + In order to establish Theorem~\ref{eqvtprin}, we use a rewrite system + consisting of a series of equalities + + \begin{isabelle}\ \ \ \ \ \ \ \ \ \ %%% + @{text "\ \ t = ... = t'"} + \end{isabelle} + + \noindent + that establish the equality between @{term "\ \ t"} and @{text + "t'"}. We have implemented this rewrite system as a conversion + tactic on the ML-level of Isabelle/HOL. + We shall next specify this tactic and show that it terminates and is + correct (in the sense of pushing a permutation @{text "\"} inside a + term and the only remaining instances of @{text "\"} are in front of + the term's free variables). The tactic applies four `oriented' + equations. We will first give a naive version of this tactic, which + however in some cornercases produces incorrect resolts or does not + terminate. We then give a modification it in order to obtain the + desired properties. A permutation @{text \} can be pushed into + applications and abstractions as follows \begin{isabelle}\ \ \ \ \ \ \ \ \ \ %%% \begin{tabular}{@ {}lr@ {\hspace{3mm}}c@ {\hspace{3mm}}l} @@ -732,12 +782,6 @@ involved because of the fact that @{text unpermutes} needs to be treated specially. - \begin{theorem}[Equivariance Principle] - Suppose a HOL-term @{text t} does not contain any @{text unpermutes} and all - its constants are equivariant. For any permutation @{text \}, let @{text t'} - be the HOL-term @{text t} except every free variable @{text x} in @{term t} is - replaced by @{text "\ \ x"}, then @{text "\ \ t = t'"}. - \end{theorem} diff -r d19bfc6e7631 -r 5f3387b7474f Pearl-jv/document/root.tex --- a/Pearl-jv/document/root.tex Mon May 02 13:01:02 2011 +0800 +++ b/Pearl-jv/document/root.tex Wed May 04 15:27:04 2011 +0800 @@ -47,7 +47,8 @@ to have finite support. We present a formalisation that is based on a unified atom type and that represents permutations by bijective functions from atoms to atoms. Interestingly, we allow swappings, which are permutations -build from two atoms, to be ill-sorted. We also describe a formalisation of +build from two atoms, to be ill-sorted. We also describe a reasoning infrastructure +that automates properties about equivariance, and present a formalisation of two abstraction operators that bind sets of names. \end{abstract} diff -r d19bfc6e7631 -r 5f3387b7474f Slides/Slides7.thy --- a/Slides/Slides7.thy Mon May 02 13:01:02 2011 +0800 +++ b/Slides/Slides7.thy Wed May 04 15:27:04 2011 +0800 @@ -12,7 +12,7 @@ (*>*) text_raw {* - \renewcommand{\slidecaption}{Hefei, 15.~April 2011} + \renewcommand{\slidecaption}{Beijing, 29.~April 2011} \newcommand{\abst}[2]{#1.#2}% atom-abstraction \newcommand{\pair}[2]{\langle #1,#2\rangle} % pairing @@ -90,7 +90,7 @@ \item Theorem provers can prevent mistakes, {\bf if} the problem is formulated so that it is suitable for theorem provers.\bigskip \item This re-formulation can be done, even in domains where - we do not expect it. + we least expect it. \end{itemize} \end{frame}} @@ -237,7 +237,7 @@ \end{center} \onslide<3-> - {looks OK \ldots let's ship it to customers\hspace{5mm} + {Looks OK \ldots let's ship it to customers\hspace{5mm} \raisebox{-5mm}{\includegraphics[scale=0.05]{sun.png}}} \end{frame}} @@ -329,7 +329,7 @@ \bl{der c (d)} & \bl{$=$} & \bl{if c = d then [] else $\varnothing$} & \\ \bl{der c (r$_1$ + r$_2$)} & \bl{$=$} & \bl{(der c r$_1$) + (der c r$_2$)} & \\ \bl{der c (r$_1$ $\cdot$ r$_2$)} & \bl{$=$} & \bl{((der c r$_1$) $\cdot$ r$_2$)} & \\ - & & \bl{\;\;+ (if nullable r$_1$ then der c r$_2$ else $\varnothing$)}\\ + & & \bl{\;\;\;\;+ (if nullable r$_1$ then der c r$_2$ else $\varnothing$)}\\ \bl{der c (r$^*$)} & \bl{$=$} & \bl{(der c r) $\cdot$ r$^*$} &\smallskip\\ \bl{derivative r []} & \bl{$=$} & \bl{r} & \\ @@ -383,7 +383,7 @@ \end{tabular} \end{center} \pause\pause\bigskip - ??? By \alert<4->{induction}, we can {\bf prove} these properties.\bigskip + By \alert<4->{induction}, we can {\bf prove} these properties.\bigskip \begin{tabular}{lrcl} Lemmas: & \bl{nullable (r)} & \bl{$\Longleftrightarrow$} & \bl{[] $\in$ \LL (r)}\\ @@ -524,7 +524,7 @@ My point:\bigskip\\ The theory about regular languages can be reformulated - to be more suitable for theorem proving. + to be more\\ suitable for theorem proving. \end{tabular} \end{center} \end{frame}} @@ -614,7 +614,7 @@ \begin{center} \begin{tabular}{l} finite $\Rightarrow$ regular\\ - \;\;\;\smath{\text{finite}\,(U\!N\!IV /\!/ \approx_L) \Rightarrow \exists r. L = \mathbb{L}(r)}\\[3mm] + \;\;\;\smath{\text{finite}\,(U\!N\!IV /\!/ \approx_L) \Rightarrow \exists r.\; L = \mathbb{L}(r)}\\[3mm] regular $\Rightarrow$ finite\\ \;\;\;\smath{\text{finite}\, (U\!N\!IV /\!/ \approx_{\mathbb{L}(r)})} \end{tabular} @@ -631,15 +631,16 @@ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% \mode{ \begin{frame}[c] - \frametitle{\LARGE Final States} + \frametitle{\LARGE Final Equiv.~Classes} \mbox{}\\[3cm] \begin{itemize} - \item ??? \smath{\text{final}_L\,X \dn \{[|s|]_\approx\;|\; s \in X\}}\\ + \item \smath{\text{finals}\,L \dn + \{{\lbrack\mkern-2mu\lbrack{s}\rbrack\mkern-2mu\rbrack}_\approx\;|\; s \in L\}}\\ \medskip - \item we can prove: \smath{L = \bigcup \{X\;|\;\text{final}_L\,X\}} + \item we can prove: \smath{L = \bigcup (\text{finals}\,L)} \end{itemize} @@ -651,7 +652,7 @@ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% \mode{ \begin{frame}[c] - \frametitle{\LARGE Transitions between\\[-3mm] Equivalence Classes} + \frametitle{\LARGE Transitions between ECs} \smath{L = \{[c]\}} @@ -725,9 +726,9 @@ & \smath{R_2} & \smath{\equiv} & \smath{R_1;a + R_2;a}\medskip\\ \onslide<3->{we can prove} & \onslide<3->{\smath{R_1}} & \onslide<3->{\smath{=}} - & \onslide<3->{\smath{R_1; \mathbb{L}(b) \,\cup\, R_2;\mathbb{L}(b) \,\cup\, \{[]\};\{[]\}}}\\ + & \onslide<3->{\smath{R_1;; \mathbb{L}(b) \,\cup\, R_2;;\mathbb{L}(b) \,\cup\, \{[]\}}}\\ & \onslide<3->{\smath{R_2}} & \onslide<3->{\smath{=}} - & \onslide<3->{\smath{R_1; \mathbb{L}(a) \,\cup\, R_2;\mathbb{L}(a)}}\\ + & \onslide<3->{\smath{R_1;; \mathbb{L}(a) \,\cup\, R_2;;\mathbb{L}(a)}}\\ \end{tabular} \end{center} @@ -928,23 +929,45 @@ *} + text_raw {* %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% \mode{ \begin{frame}[c] - \frametitle{\LARGE Other Direction} - + \frametitle{\LARGE The Other Direction} + One has to prove \begin{center} \smath{\text{finite} (U\!N\!IV /\!/ \approx_{\mathbb{L}(r)})} \end{center} - by induction on \smath{r}. Not trivial, but after a bit - of thinking, one can prove that if + by induction on \smath{r}. This is straightforward for \\the base cases:\small \begin{center} - \smath{\text{finite} (U\!N\!IV /\!/ \approx_{\mathbb{L}(r_1)})}\hspace{5mm} + \begin{tabular}{l@ {\hspace{1mm}}l} + \smath{U\!N\!IV /\!/ \!\approx_{\emptyset}} & \smath{= \{U\!N\!IV\}}\smallskip\\ + \smath{U\!N\!IV /\!/ \!\approx_{\{[]\}}} & \smath{\subseteq \{\{[]\}, U\!N\!IV - \{[]\}\}}\smallskip\\ + \smath{U\!N\!IV /\!/ \!\approx_{\{[c]\}}} & \smath{\subseteq \{\{[]\}, \{[c]\}, U\!N\!IV - \{[], [c]\}\}} + \end{tabular} + \end{center} + + + \end{frame}} + %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% +*} + + +text_raw {* + %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% + \mode{ + \begin{frame}[t] + \frametitle{\LARGE The Other Direction} + + More complicated are the inductive cases:\\ one needs to prove that if + + \begin{center} + \smath{\text{finite} (U\!N\!IV /\!/ \approx_{\mathbb{L}(r_1)})}\hspace{3mm} \smath{\text{finite} (U\!N\!IV /\!/ \approx_{\mathbb{L}(r_2)})} \end{center} @@ -954,12 +977,149 @@ \smath{\text{finite} (U\!N\!IV /\!/ \approx_{\mathbb{L}(r_1) \,\cup\, \mathbb{L}(r_2)})} \end{center} + \end{frame}} + %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% +*} + + +text_raw {* + %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% + \mode{ + \begin{frame}[t] + \frametitle{\LARGE Helper Lemma} + + \begin{center} + \begin{tabular}{p{10cm}} + %If \smath{\text{finite} (f\;' A)} and \smath{f} is injective + %(on \smath{A}),\\ then \smath{\text{finite}\,A}. + Given two equivalence relations \smath{R_1} and \smath{R_2} with + \smath{R_1} refining \smath{R_2} (\smath{R_1 \subseteq R_2}).\\ + Then\medskip\\ + \smath{\;\;\text{finite} (U\!N\!IV /\!/ R_1) \Rightarrow \text{finite} (U\!N\!IV /\!/ R_2)} + \end{tabular} + \end{center} + + \end{frame}} + %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% +*} + +text_raw {* + %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% + \mode{ + \begin{frame}[c] + \frametitle{\Large Derivatives and Left-Quotients} + \small + Work by Brozowski ('64) and Antimirov ('96):\pause\smallskip + + + \begin{tabular}{@ {}l@ {\hspace{2mm}}c@ {\hspace{2mm}}l@ {\hspace{-10mm}}l@ {}} + \multicolumn{4}{@ {}l}{Left-Quotient:}\\ + \multicolumn{4}{@ {}l}{\bl{$\text{Ders}\;\text{s}\,A \dn \{\text{s'} \;|\; \text{s @ s'} \in A\}$}}\bigskip\\ + + \multicolumn{4}{@ {}l}{Derivative:}\\ + \bl{der c ($\varnothing$)} & \bl{$=$} & \bl{$\varnothing$} & \\ + \bl{der c ([])} & \bl{$=$} & \bl{$\varnothing$} & \\ + \bl{der c (d)} & \bl{$=$} & \bl{if c = d then [] else $\varnothing$} & \\ + \bl{der c (r$_1$ + r$_2$)} & \bl{$=$} & \bl{(der c r$_1$) + (der c r$_2$)} & \\ + \bl{der c (r$_1$ $\cdot$ r$_2$)} & \bl{$=$} & \bl{((der c r$_1$) $\cdot$ r$_2$)} & \\ + & & \bl{\;\;\;\;+ (if nullable r$_1$ then der c r$_2$ else $\varnothing$)}\\ + \bl{der c (r$^*$)} & \bl{$=$} & \bl{(der c r) $\cdot$ r$^*$} &\smallskip\\ + + \bl{ders [] r} & \bl{$=$} & \bl{r} & \\ + \bl{ders (s @ [c]) r} & \bl{$=$} & \bl{der c (ders s r)} & \\ + \end{tabular}\pause + + \begin{center} + \alert{$\Rightarrow$}\smath{\;\;\text{Ders}\,\text{s}\,(\mathbb{L}(\text{r})) = \mathbb{L} (\text{ders s r})} + \end{center} + + \end{frame}} + %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% +*} + +text_raw {* + %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% + \mode{ + \begin{frame}[c] + \frametitle{\LARGE Left-Quotients and MN-Rels} + + \begin{itemize} + \item \smath{x \approx_{A} y \,\dn\, \forall z.\; x @ z \in A \Leftrightarrow y @ z \in A}\medskip + \item \bl{$\text{Ders}\;s\,A \dn \{s' \;|\; s @ s' \in A\}$} + \end{itemize}\bigskip + + \begin{center} + \smath{x \approx_A y \Longleftrightarrow \text{Ders}\;x\;A = \text{Ders}\;y\;A} + \end{center}\bigskip\pause\small + + which means + + \begin{center} + \smath{x \approx_{\mathbb{L}(r)} y \Longleftrightarrow + \mathbb{L}(\text{ders}\;x\;r) = \mathbb{L}(\text{ders}\;y\;r)} + \end{center}\pause + + \hspace{8.8mm}or + \smath{\;x \approx_{\mathbb{L}(r)} y \Longleftarrow + \text{ders}\;x\;r = \text{ders}\;y\;r} + \end{frame}} %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% *} +text_raw {* + %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% + \mode{ + \begin{frame}[c] + \frametitle{\LARGE Partial Derivatives} + + Antimirov: \bl{pder : rexp $\Rightarrow$ rexp set}\bigskip + + \begin{tabular}{@ {}l@ {\hspace{2mm}}c@ {\hspace{2mm}}l@ {\hspace{-10mm}}l@ {}} + \bl{pder c ($\varnothing$)} & \bl{$=$} & \bl{\{$\varnothing$\}} & \\ + \bl{pder c ([])} & \bl{$=$} & \bl{\{$\varnothing$\}} & \\ + \bl{pder c (d)} & \bl{$=$} & \bl{if c = d then \{[]\} else \{$\varnothing$\}} & \\ + \bl{pder c (r$_1$ + r$_2$)} & \bl{$=$} & \bl{(pder c r$_1$) $\cup$ (pder c r$_2$)} & \\ + \bl{pder c (r$_1$ $\cdot$ r$_2$)} & \bl{$=$} & \bl{(pder c r$_1$) $\odot$ r$_2$} & \\ + & & \bl{\hspace{-10mm}$\cup$ (if nullable r$_1$ then pder c r$_2$ else $\varnothing$)}\\ + \bl{pder c (r$^*$)} & \bl{$=$} & \bl{(pder c r) $\odot$ r$^*$} &\smallskip\\ + \end{tabular} + + \begin{tabular}{@ {}l@ {\hspace{2mm}}c@ {\hspace{2mm}}l@ {\hspace{-10mm}}l@ {}} + \bl{pders [] r} & \bl{$=$} & \bl{r} & \\ + \bl{pders (s @ [c]) r} & \bl{$=$} & \bl{pder c (pders s r)} & \\ + \end{tabular}\pause + + \begin{center} + \alert{$\Rightarrow$}\smath{\;\;\text{Ders}\,\text{s}\,(\mathbb{L}(\text{r})) = \bigcup (\mathbb{L}\;`\; (\text{pders s r}))} + \end{center} + + \end{frame}} + %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% +*} + +text_raw {* + %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% + \mode{ + \begin{frame}[t] + \frametitle{\LARGE Final Result} + + \mbox{}\\[7mm] + + \begin{itemize} + \item \alt<1>{\smath{\text{pders x r \mbox{$=$} pders y r}}} + {\smath{\underbrace{\text{pders x r \mbox{$=$} pders y r}}_{R_1}}} + refines \bl{x $\approx_{\mathbb{L}(\text{r})}$ y}\pause + \item \smath{\text{finite} (U\!N\!IV /\!/ R_1)} \bigskip\pause + \item Therefore \smath{\text{finite} (U\!N\!IV /\!/ \approx_{\mathbb{L}(r)})}. Qed. + \end{itemize} + + \end{frame}} + %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% +*} + text_raw {* %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%