--- 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 "\<beta>"} is a generic type for @{text x}. The definition of this operation will be
+ whereby @{text "\<beta>"} 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 "\<pi> \<bullet> (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 \<Rightarrow> (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 \<pi>}. 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 "\<and>"}, @{text "\<or>"}, @{text
- "\<not>"} and @{text "\<longrightarrow>"}, 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 "\<and>"},
+ @{text "\<or>"}, @{text "\<longrightarrow>"} and @{text "\<not>"} are equivariant too:
\begin{isabelle}\ \ \ \ \ \ \ \ \ \ %%%
\begin{tabular}{@ {}lcl}
@{text "\<pi> \<bullet> (A \<and> B) = (\<pi> \<bullet> A) \<and> (\<pi> \<bullet> B)"}\\
+ @{text "\<pi> \<bullet> (A \<or> B) = (\<pi> \<bullet> A) \<or> (\<pi> \<bullet> B)"}\\
@{text "\<pi> \<bullet> (A \<longrightarrow> B) = (\<pi> \<bullet> A) \<longrightarrow> (\<pi> \<bullet> B)"}\\
+ @{text "\<pi> \<bullet> (\<not>A) = \<not>(\<pi> \<bullet> 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 "\<pi>"} inside a term and the only remaining
- instances of @{text "\<pi>"} 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 \<pi>}, let @{text t'} be the HOL-term @{text t} except every
+ free variable @{text x} in @{term t} is replaced by @{text "\<pi> \<bullet> x"}, then
+ @{text "\<pi> \<bullet> 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 "\<forall>"}, is
+ of type @{text "(\<alpha> \<Rightarrow> bool) \<Rightarrow> 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 "\<pi> \<bullet> (All P) \<equiv> \<pi> \<bullet> (P = (\<lambda>x. True)) = ((\<pi> \<bullet> P) = (\<lambda>x. True)) \<equiv> All (\<pi> \<bullet> 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 \<pi>} 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 "\<exists>"}, 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 "\<forall>"} and @{text "\<longrightarrow>"}). 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 "\<pi> \<cdot> t = ... = t'"}
+ \end{isabelle}
+
+ \noindent
+ that establish the equality between @{term "\<pi> \<bullet> 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 "\<pi>"} inside a
+ term and the only remaining instances of @{text "\<pi>"} 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 \<pi>} 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 \<pi>}, let @{text t'}
- be the HOL-term @{text t} except every free variable @{text x} in @{term t} is
- replaced by @{text "\<pi> \<bullet> x"}, then @{text "\<pi> \<bullet> t = t'"}.
- \end{theorem}
--- 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}
--- 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<presentation>{
\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<presentation>{
\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<presentation>{
\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<presentation>{
+ \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<presentation>{
+ \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<presentation>{
+ \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<presentation>{
+ \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<presentation>{
+ \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<presentation>{
+ \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 {*
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%