# HG changeset patch
# User Chengsong
# Date 1583185524 0
# Node ID c8af86f7558ed5f4431db59d7f2b6ef36933e717
# Parent  31711ca3168513be5dc8ca8b4ced9850030dc5f0
ders2

diff -r 31711ca31685 -r c8af86f7558e etnms/etnms.tex
--- a/etnms/etnms.tex	Mon Mar 02 18:08:12 2020 +0000
+++ b/etnms/etnms.tex	Mon Mar 02 21:45:24 2020 +0000
@@ -1708,18 +1708,36 @@
 where $s_1$ is a substring of $s$.
 For this we introduce the $\textit{ders2}$ function,
 which does a "convolution" on $r_1$ and $r_2$ using the string
-$s$.
+$s$. We omit the bits here as they are not affecting the 
+structure of the regular expression, and we are mainly 
+focusing on structure here.
 It is based on the observation that the derivative of $r_1 \cdot r_2$
 with respect to a string $s$ can actually be written in an "explicit form"
-composed of $r_1$'s derivative of $s$ and $r_2$'s derivative of $s$.
-This can be illustrated in the following procedure execution 
+composed of $r_1$ and $r_2$'s derivatives.
+For example, we can look at how $r1\cdot r2$ expands
+when being derived with a two-character string:
 \begin{center}
-	$ (r_1 \cdot r_2) \backslash [c_1c_2] =  (\textit{if} \; \nullable(r_1)\;  \textit{then} \; ((r_1 \backslash c_1) \cdot r_2 + r_2 \backslash c_1) \; \textit{else} \; (r_1\backslash c_1) \cdot r_2) \backslash c_2$
+\begin{tabular}{lcl}
+	$ (r_1 \cdot r_2) \backslash [c_1c_2]$ & $=$ & $ (\textit{if} \; \nullable(r_1)\;  \textit{then} \; ((r_1 \backslash c_1) \cdot r_2 + r_2 \backslash c_1) \; \textit{else} \; (r_1\backslash c_1) \cdot r_2) \backslash c_2$\\
+	& $=$ & $\textit{if} \; \textit{nullable}(r_1) \;\textit{and} \; \nullable(r_1\backslash c_1) \; \textit{then} \;
+	(((r_1\backslash c_1c_2)\cdot r_2 +( r_1 \backslash c_1 )\cdot r_2\backslash c_2 )+ r_2 \backslash c_1c_2)$\\
+	&& $\textit{else if} \; \nullable(r_1) \textit{and} \;\textit{not} \; \nullable(r_1 \backslash c_1)\; \textit{then} \;
+	((r_1\backslash c_1c_2)\cdot r_2 + r_2 \backslash c_1c_2)$\\
+	&& $\textit{else} \;(r_1\backslash c_1c_2) \cdot r_2$
+\end{tabular}
 \end{center}
 which can also be written in a "convoluted sum"
-format:
+format if we omit the order in which the alternatives
+are being nested:
 \begin{center}
-	$ (r_1 \cdot r_2) \backslash [c_1c_2] =  \sum{r_1 \backslash s_i \cdot r_2 \backslash s_j}$
+\begin{tabular}{lcl}
+	$(r_1 \cdot r_2) \backslash [c_1c_2] $ & $=$ & $\textit{if} \; \textit{nullable}(r_1) \;\textit{and} \; \nullable(r_1\backslash c_1) \; \textit{then} \;
+	(r_1 \backslash c_1c_2) \cdot r_2 + (r_1 \backslash c_1)\cdot (r_2 \backslash c_2) + r_2 \backslash c_1c_2$\\
+	&& $\textit{else if} \; \nullable(r_1) \textit{and} \;\textit{not} \; \nullable(r_1 \backslash c_1)\; \textit{then} \;
+	((r_1\backslash c_1c_2)\cdot r_2 + r_2 \backslash c_1c_2)$\\
+	&& $\textit{else} \;(r_1\backslash c_1c_2) \cdot r_2$\\
+	& $=$ & $\sum\limits{s_i }{r_1 \backslash s_i \cdot r_2 \backslash s_j} \; \text{where} \; s_i \; \text{is} \; \text{true prefix}\;  \text{of} \; s \;\text{and} \; s_i @s_j = s \; \text{and} \;\nullable(r_1\backslash s_i)$
+\end{tabular}
 \end{center}
 In a more serious manner, we should write
 \begin{center}