cst_tests: comparison etnms/etnms.tex

equal deleted inserted replaced

-:b6984212cf87
+:69292c2b54d8
 \begin{center}
 \begin{tabular}{lcl}
 $\textit{a}$ & $::=$  & $\ZERO$\\
 & $\mid$ & $_{bs}\ONE$\\
 & $\mid$ & $_{bs}{\bf c}$\\
-& $\mid$ & $_{bs}\oplus\,as$\\
+& $\mid$ & $_{bs}\sum\,as$\\
 & $\mid$ & $_{bs}a_1\cdot a_2$\\
 & $\mid$ & $_{bs}a^*$
 \end{tabular}
 \end{center}
 %(in \textit{ALTS})
 \noindent
 where $bs$ stands for bitcodes, $a$  for $\bold{a}$nnotated regular
 expressions and $as$ for a list of annotated regular expressions.
-The alternative constructor($\oplus$) has been generalized to
+The alternative constructor($\sum$) has been generalized to
 accept a list of annotated regular expressions rather than just 2.
 We will show that these bitcodes encode information about
 the (POSIX) value that should be generated by the Sulzmann and Lu
 algorithm.
 \begin{tabular}{lcl}
 $(\ZERO)^\uparrow$ & $\dn$ & $\ZERO$\\
 $(\ONE)^\uparrow$ & $\dn$ & $_{[]}\ONE$\\
 $(c)^\uparrow$ & $\dn$ & $_{[]}{\bf c}$\\
 $(r_1 + r_2)^\uparrow$ & $\dn$ &
-$_{[]}\oplus[\textit{fuse}\,[0]\,r_1^\uparrow,\,
+$_{[]}\sum[\textit{fuse}\,[0]\,r_1^\uparrow,\,
 \textit{fuse}\,[1]\,r_2^\uparrow]$\\
 $(r_1\cdot r_2)^\uparrow$ & $\dn$ &
 $_{[]}r_1^\uparrow \cdot r_2^\uparrow$\\
 $(r^*)^\uparrow$ & $\dn$ &
 $_{[]}(r^\uparrow)^*$\\
 $\textit{fuse}\;bs \; \ZERO$ & $\dn$ & $\ZERO$\\
 $\textit{fuse}\;bs\; _{bs'}\ONE$ & $\dn$ &
 $_{bs @ bs'}\ONE$\\
 $\textit{fuse}\;bs\;_{bs'}{\bf c}$ & $\dn$ &
 $_{bs@bs'}{\bf c}$\\
-$\textit{fuse}\;bs\,_{bs'}\oplus\textit{as}$ & $\dn$ &
+$\textit{fuse}\;bs\,_{bs'}\sum\textit{as}$ & $\dn$ &
-$_{bs@bs'}\oplus\textit{as}$\\
+$_{bs@bs'}\sum\textit{as}$\\
 $\textit{fuse}\;bs\; _{bs'}a_1\cdot a_2$ & $\dn$ &
 $_{bs@bs'}a_1 \cdot a_2$\\
 $\textit{fuse}\;bs\,_{bs'}a^*$ & $\dn$ &
 $_{bs @ bs'}a^*$
 \end{tabular}
 $(\ZERO)\,\backslash c$ & $\dn$ & $\ZERO$\\
 $(_{bs}\ONE)\,\backslash c$ & $\dn$ & $\ZERO$\\
 $(_{bs}{\bf d})\,\backslash c$ & $\dn$ &
 $\textit{if}\;c=d\; \;\textit{then}\;
 _{bs}\ONE\;\textit{else}\;\ZERO$\\
-$(_{bs}\oplus \;\textit{as})\,\backslash c$ & $\dn$ &
+$(_{bs}\sum \;\textit{as})\,\backslash c$ & $\dn$ &
-$_{bs}\oplus\;(\textit{as.map}(\backslash c))$\\
+$_{bs}\sum\;(\textit{as.map}(\backslash c))$\\
 $(_{bs}\;a_1\cdot a_2)\,\backslash c$ & $\dn$ &
 $\textit{if}\;\textit{bnullable}\,a_1$\\
-					       & &$\textit{then}\;_{bs}\oplus\,[(_{[]}\,(a_1\,\backslash c)\cdot\,a_2),$\\
+					       & &$\textit{then}\;_{bs}\sum\,[(_{[]}\,(a_1\,\backslash c)\cdot\,a_2),$\\
-					       & &$\phantom{\textit{then},\;_{bs}\oplus\,}(\textit{fuse}\,(\textit{bmkeps}\,a_1)\,(a_2\,\backslash c))]$\\
+					       & &$\phantom{\textit{then},\;_{bs}\sum\,}(\textit{fuse}\,(\textit{bmkeps}\,a_1)\,(a_2\,\backslash c))]$\\
 & &$\textit{else}\;_{bs}\,(a_1\,\backslash c)\cdot a_2$\\
 $(_{bs}a^*)\,\backslash c$ & $\dn$ &
 $_{bs}(\textit{fuse}\, [0] \; r\,\backslash c)\cdot
 (_{[]}r^*))$
 \end{tabular}
 \backslash c)$ will collapse the regular expression $a_1$(as it has
 already been fully matched) and store the parsing information at the
 head of the regular expression $a_2 \backslash c$ by fusing to it. The
 bitsequence $\textit{bs}$, which was initially attached to the
 first element of the sequence $a_1 \cdot a_2$, has
-now been elevated to the top-level of $\oplus$, as this information will be
+now been elevated to the top-level of $\sum$, as this information will be
 needed whichever way the sequence is matched---no matter whether $c$ belongs
 to $a_1$ or $ a_2$. After building these derivatives and maintaining all
 the lexing information, we complete the lexing by collecting the
 bitcodes using a generalised version of the $\textit{mkeps}$ function
 for annotated regular expressions, called $\textit{bmkeps}$:
 %\begin{definition}[\textit{bmkeps}]\mbox{}
 \begin{center}
 \begin{tabular}{lcl}
 $\textit{bmkeps}\,(_{bs}\ONE)$ & $\dn$ & $bs$\\
-$\textit{bmkeps}\,(_{bs}\oplus a::\textit{as})$ & $\dn$ &
+$\textit{bmkeps}\,(_{bs}\sum a::\textit{as})$ & $\dn$ &
 $\textit{if}\;\textit{bnullable}\,a$\\
 & &$\textit{then}\;bs\,@\,\textit{bmkeps}\,a$\\
-& &$\textit{else}\;bs\,@\,\textit{bmkeps}\,(_{bs}\oplus \textit{as})$\\
+& &$\textit{else}\;bs\,@\,\textit{bmkeps}\,(_{bs}\sum \textit{as})$\\
 $\textit{bmkeps}\,(_{bs} a_1 \cdot a_2)$ & $\dn$ &
 $bs \,@\,\textit{bmkeps}\,a_1\,@\, \textit{bmkeps}\,a_2$\\
 $\textit{bmkeps}\,(_{bs}a^*)$ & $\dn$ &
 $bs \,@\, [0]$
 \end{tabular}
 that the expected bound can be achieved. Obviously we could only
 partially cover  the search space as there are infinitely many regular
 expressions and strings.
 One modification we introduced is to allow a list of annotated regular
-expressions in the $\oplus$ constructor. This allows us to not just
+expressions in the $\sum$ constructor. This allows us to not just
 delete unnecessary $\ZERO$s and $\ONE$s from regular expressions, but
 also unnecessary ``copies'' of regular expressions (very similar to
 simplifying $r + r$ to just $r$, but in a more general setting). Another
 modification is that we use simplification rules inspired by Antimirov's
 work on partial derivatives. They maintain the idea that only the first
 &&$\quad\textit{case} \; (\_, \ZERO) \Rightarrow  \ZERO$ \\
 &&$\quad\textit{case} \;  (\ONE, a_2') \Rightarrow  \textit{fuse} \; bs \;  a_2'$ \\
 &&$\quad\textit{case} \; (a_1', \ONE) \Rightarrow  \textit{fuse} \; bs \;  a_1'$ \\
 &&$\quad\textit{case} \; (a_1', a_2') \Rightarrow   _{bs}a_1' \cdot a_2'$ \\
-$\textit{simp} \; (_{bs}\oplus \textit{as})$ & $\dn$ & $\textit{distinct}( \textit{flatten} ( \textit{map simp as})) \; \textit{match} $ \\
+$\textit{simp} \; (_{bs}\sum \textit{as})$ & $\dn$ & $\textit{distinct}( \textit{flatten} ( \textit{map simp as})) \; \textit{match} $ \\
 &&$\quad\textit{case} \; [] \Rightarrow  \ZERO$ \\
 &&$\quad\textit{case} \; a :: [] \Rightarrow  \textit{fuse bs a}$ \\
-&&$\quad\textit{case} \;  as' \Rightarrow _{bs}\oplus \textit{as'}$\\
+&&$\quad\textit{case} \;  as' \Rightarrow _{bs}\sum \textit{as'}$\\
 $\textit{simp} \; a$ & $\dn$ & $\textit{a} \qquad \textit{otherwise}$
 \end{tabular}
 \end{center}
 The simplification does a pattern matching on the regular expression.
 When it detected that the regular expression is an alternative or
 sequence, it will try to simplify its children regular expressions
 recursively and then see if one of the children turn into $\ZERO$ or
 $\ONE$, which might trigger further simplification at the current level.
-The most involved part is the $\oplus$ clause, where we use two
+The most involved part is the $\sum$ clause, where we use two
 auxiliary functions $\textit{flatten}$ and $\textit{distinct}$ to open up nested
 alternatives and reduce as many duplicates as possible. Function
 $\textit{distinct}$  keeps the first occurring copy only and remove all later ones
-when detected duplicates. Function $\textit{flatten}$ opens up nested $\oplus$s.
+when detected duplicates. Function $\textit{flatten}$ opens up nested $\sum$s.
 Its recursive definition is given below:
 \begin{center}
 \begin{tabular}{@{}lcl@{}}
-$\textit{flatten} \; (_{bs}\oplus \textit{as}) :: \textit{as'}$ & $\dn$ & $(\textit{map} \;
+$\textit{flatten} \; (_{bs}\sum \textit{as}) :: \textit{as'}$ & $\dn$ & $(\textit{map} \;
 (\textit{fuse}\;bs)\; \textit{as}) \; @ \; \textit{flatten} \; as' $ \\
 $\textit{flatten} \; \ZERO :: as'$ & $\dn$ & $ \textit{flatten} \;  \textit{as'} $ \\
 $\textit{flatten} \; a :: as'$ & $\dn$ & $a :: \textit{flatten} \; \textit{as'}$ \quad(otherwise)
 \end{tabular}
 \end{center}
 we use the helper function retrieve described by Sulzmann and Lu:
 \begin{center}
 \begin{tabular}{@{}l@{\hspace{2mm}}c@{\hspace{2mm}}l@{}}
 $\textit{retrieve}\,(_{bs}\ONE)\,\Empty$ & $\dn$ & $bs$\\
 $\textit{retrieve}\,(_{bs}{\bf c})\,(\Char\,d)$ & $\dn$ & $bs$\\
-$\textit{retrieve}\,(_{bs}\oplus a::as)\,(\Left\,v)$ & $\dn$ &
+$\textit{retrieve}\,(_{bs}\sum a::as)\,(\Left\,v)$ & $\dn$ &
 $bs \,@\, \textit{retrieve}\,a\,v$\\
-$\textit{retrieve}\,(_{bs}\oplus a::as)\,(\Right\,v)$ & $\dn$ &
+$\textit{retrieve}\,(_{bs}\sum a::as)\,(\Right\,v)$ & $\dn$ &
-$\textit{bs} \,@\, \textit{retrieve}\,(_{[]}\oplus as)\,v$\\
+$\textit{bs} \,@\, \textit{retrieve}\,(_{[]}\sum as)\,v$\\
 $\textit{retrieve}\,(_{bs}a_1\cdot a_2)\,(\Seq\,v_1\,v_2)$ & $\dn$ &
 $bs \,@\,\textit{retrieve}\,a_1\,v_1\,@\, \textit{retrieve}\,a_2\,v_2$\\
 $\textit{retrieve}\,(_{bs}a^*)\,(\Stars\,[])$ & $\dn$ &
 $bs \,@\, [0]$\\
 $\textit{retrieve}\,(_{bs}a^*)\,(\Stars\,(v\!::\!vs))$ & $\dn$ &\\
 \end{tabular}
 \end{center}
 \noindent
-and the difinition of $\flatten$:
+and the definition of $\flatten$:
 \begin{center}
 \begin{tabular}{c c c}
 $\flatten \; []$ & $\dn$ & $[]$\\
 $\flatten \; \ZERO::rs$ & $\dn$ & $rs$\\
-$\flatten \;(_{\textit{bs}_1}\oplus \textit{rs}_1 ::rs)$ & $\dn$ & $(\map \, (\fuse \, \textit{bs}_1) \,\textit{rs}_1) ::: \flatten(rs)$\\
+$\flatten \;(_{\textit{bs}_1}\sum \textit{rs}_1 ::rs)$ & $\dn$ & $(\map \, (\fuse \, \textit{bs}_1) \,\textit{rs}_1) ::: \flatten(rs)$\\
 $\flatten \; r :: rs$ & $\dn$ & $r::\flatten(rs)$
 \end{tabular}
 \end{center}
 \noindent
 If we call $\simp$ on $\rup\backslash a$, just as $\backslash_{simp}$
-requires, then we would go throught the third clause of
+requires, then we would go through the third clause of
 the sequence case:$\quad\textit{case} \;  (\ONE, a_2') \Rightarrow  \textit{fuse} \; bs \;  a_2'$.
 The $\ZERO$ of $(_0\ONE  + \ZERO)$ is thrown away
 by $\flatten$ and
 $_0\ONE$ merged into $(_0a  +  _1a^*)$ by simply
 putting its bits($_0$) to the front of the second component:
 namely, $(_0(_0a  +  _1a^*))\backslash a$, we get
 $
 _0(_0 \ONE  +  _1(_1\ONE \cdot a^*))
 $, and this simplifies to $_0(_0 \ONE  +  _{11} a^*)$
 by the third clause of the alternative case:
-$\quad\textit{case} \;  as' \Rightarrow  \textit{ALTS}\;bs\;as'$.
+\begin{center}
+$\quad\textit{case} \;  as' \Rightarrow  _{bs}\sum{as'}$.
+\end{center}
+\noindent
 The outmost bit $_0$ stays with
 the outmost regular expression, rather than being fused to
 its child regular expressions, as what we will later see happens
 to $\simp(\rup\backslash \, s)$.
 If we choose to not simplify in the midst of derivative operations,
 $\rup\backslash_{simp} \, s$
 and  $\simp(\rup\backslash s)$:
 \begin{center}
 \begin{tabular}{lcl}
 $D =\{ (r_1 \cdot r_2,\; [c_1c_2]) \mid $ & $\simp(r_2) = r_2, \simp(r_1 \backslash c_1) = \ONE,$\\
-$r_1 \; not \; \nullable, c_2 \in L(r_2),$ & $\exists \textit{rs},\textit{bs}.\;  r_2 \backslash c_2 = _{bs}{\oplus rs}$\\
+$r_1 \; not \; \nullable, c_2 \in L(r_2),$ & $\exists \textit{rs},\textit{bs}.\;  r_2 \backslash c_2 = _{bs}{\sum rs}$\\
-$\exists \textit{rs}_1. \; \simp(r_2 \backslash c_2) = _{bs}{\oplus \textit{rs}_1}$ &  $and \;\simp(r_1 \backslash [c_1c_2]) = \ZERO\}$\\
+$\exists \textit{rs}_1. \; \simp(r_2 \backslash c_2) = _{bs}{\sum \textit{rs}_1}$ &  $and \;\simp(r_1 \backslash [c_1c_2]) = \ZERO\}$\\
 \end{tabular}
 \end{center}
 We take a pair $(r, \;s)$ from the set $D$.
 Now we compute ${\bf \rup \backslash_{simp} s}$, we get:
 \begin{center}
 $ \simp \left[  \fuse \; \textit{bs}_2\; r_2  \backslash c_2 \right]$,
 \end{center}
 which is equal to
 \begin{center}
-$\simp \left[ \fuse \; \textit{bs}_2 \; _{bs}{\oplus rs} \right]$\\
+$\simp \left[ \fuse \; \textit{bs}_2 \; _{bs}{\sum rs} \right]$\\
-$=\simp \left[  \; _{bs_2++bs}{\oplus rs} \right]$\\
+$=\simp \left[  \; _{bs_2++bs}{\sum rs} \right]$\\
-$=  \; _{bs_2++bs}{\oplus \textit{rs}_1} $
+$=  \; _{bs_2++bs}{\sum \textit{rs}_1} $
 \end{center}
 \noindent
 by using the properties from the set $D$ again
 and again(The reason why we set so many conditions
 that the pair $(r,s)$ need to satisfy is because we can
 \noindent
 Again, using the properties above, we obtain
 the following chain of equalities:
 \begin{center}
 $\simp(\rup \backslash s)= \simp \left[ ((r_1 \cdot r_2 )\backslash c_1) \backslash c_2 \right]= \simp\left[    \left(r_1 \backslash c_1\right) \cdot r_2  \big) \backslash c_2 \right]$\\
-$= \simp \left[ \oplus[\big( \left(r_1 \backslash c_1\right) \backslash c_2 \big) \cdot r_2 \; , \; \fuse \; (\bmkeps \;r_1\backslash c_1) \; r_2 \backslash c_2 ] \right]$,
+$= \simp \left[ \sum[\big( \left(r_1 \backslash c_1\right) \backslash c_2 \big) \cdot r_2 \; , \; \fuse \; (\bmkeps \;r_1\backslash c_1) \; r_2 \backslash c_2 ] \right]$,
 \end{center}
 \noindent
 as before, we call the bitcode returned by
 $\bmkeps(r_1\backslash c_1)$ as
 $\textit{bs}_2$.
 Also, $\simp(r_2 \backslash c_2)$ is
-$_{bs}\oplus \textit{rs}_1$,
+$_{bs}\sum \textit{rs}_1$,
 and $( \left(r_1 \backslash c_1\right) \backslash c_2  \cdot r_2)$
 simplifies to $\ZERO$,
 so the above term can be expanded as
 \begin{center}
 \begin{tabular}{l}
-$\textit{distinct}(\flatten[\ZERO\;, \; _{\textit{bs}_2++\textit{bs}}\oplus \textit{rs}_1] ) \; \textit{match} $ \\
+$\textit{distinct}(\flatten[\ZERO\;, \; _{\textit{bs}_2++\textit{bs}}\sum \textit{rs}_1] ) \; \textit{match} $ \\
 $\textit{case} \; [] \Rightarrow  \ZERO$ \\
 $\textit{case} \; a :: [] \Rightarrow  \textit{\fuse \; \textit{bs} a}$ \\
-$\textit{case} \;  as' \Rightarrow  _{[]}\oplus as'$\\
+$\textit{case} \;  as' \Rightarrow  _{[]}\sum as'$\\
 \end{tabular}
 \end{center}
 \noindent
 Applying the definition of $\flatten$, we get
 \begin{center}
-$_{[]}\oplus (\textit{map} \; \fuse (\textit{bs}_2 ++ bs) rs_1)$
+$_{[]}\sum (\textit{map} \; \fuse (\textit{bs}_2 ++ bs) rs_1)$
 \end{center}
 \noindent
 compared to the result
 \begin{center}
-$ \; _{bs_2++bs}{\oplus \textit{rs}_1} $
+$ \; _{bs_2++bs}{\sum \textit{rs}_1} $
 \end{center}
 \noindent
 Note how these two regular expressions only
 differ in terms of the position of the bits
 $\textit{bs}_2++\textit{bs}$. They are the same otherwise.
 there exists an outer alternative.
 Note how the absence of simplification
 caused $\simp(\rup \backslash s)$ to
 generate the nested alternatives structure:
 \begin{center}
-$  \oplus[\ZERO \;, \; _{bs}\oplus \textit{rs} ]$
+$  \sum[\ZERO \;, \; _{bs}\sum \textit{rs} ]$
 \end{center}
 and this will always trigger the $\flatten$ to
 spill out the inner alternative's bitcode $\textit{bs}$,
 whereas when
 simplification is done along the way,
 How about we do not allow the function $\simp$
 to fuse out the bits when it is unnecessary?
 Like, for the above regular expression, we might
 just delete the outer layer of alternative
 \begin{center}
-\st{$ {\oplus[\ZERO \;,}$} $_{bs}\oplus \textit{rs}$ \st{$]$}
+\st{$ {\sum[\ZERO \;,}$} $_{bs}\sum \textit{rs}$ \st{$]$}
 \end{center}
-and get $_{bs}\oplus \textit{rs}$ instead, without
+and get $_{bs}\sum \textit{rs}$ instead, without
 fusing the bits $\textit{bs}$ inside to every element
 of $\textit{rs}$.
 This idea can be realized by making the following
 changes to the $\simp$-function:
 \begin{center}
 \begin{tabular}{@{}lcl@{}}
 $\textit{simp}' \; (_{\textit{bs}}(a_1 \cdot a_2))$ & $\dn$ & $\textit{as} \; \simp \; \textit{was} \; \textit{before} $ \\
-$\textit{simp}' \; (_{bs}\oplus as)$ & $\dn$ & \st{$\textit{distinct}( \textit{flatten} ( \textit{map simp as})) \; \textit{match} $} \\
+$\textit{simp}' \; (_{bs}\sum as)$ & $\dn$ & \st{$\textit{distinct}( \textit{flatten} ( \textit{map simp as})) \; \textit{match} $} \\
 &&\st{$\quad\textit{case} \; [] \Rightarrow  \ZERO$} \\
 &&\st{$\quad\textit{case} \; a :: [] \Rightarrow  \textit{fuse bs a}$} \\
 &&\st{$\quad\textit{case} \;  as' \Rightarrow  \textit{ALTS}\;bs\;as'$}\\
 &&$\textit{if}(\textit{hollowAlternatives}( \textit{map \; simp \; as}))$\\
 &&$\textit{then} \; \fuse  \; \textit{bs}\; \textit{extractAlt}(\textit{map} \; \simp \; \textit{as} )$\\
-&&$\textit{else} \; \simp(_{bs} \oplus \textit{as})$\\
+&&$\textit{else} \; \simp(_{bs} \sum \textit{as})$\\
 $\textit{simp}' \; a$ & $\dn$ & $\textit{a} \qquad \textit{otherwise}$
 \end{tabular}
 \end{center}
 \noindent
 given the definition of $\textit{hollowAlternatives}$ and  $\textit{extractAlt}$ :
 \begin{center}
 $\textit{hollowAlternatives}( \textit{rs}) \dn
-\exists r = (_{\textit{bs}_1}\oplus \textit{rs}_1)  \in \textit{rs}.  \forall r' \in \textit{rs}, \;
+\exists r = (_{\textit{bs}_1}\sum \textit{rs}_1)  \in \textit{rs}.  \forall r' \in \textit{rs}, \;
 \textit{either} \; r' = \ZERO \; \textit{or} \; r' = r $
 $\textit{extractAlt}( \textit{rs}) \dn \textit{if}\big(
-\exists r = (_{\textit{bs}_1}\oplus \textit{rs}_1)  \in \textit{rs}.  \forall r' \in \textit{rs}, \;
+\exists r = (_{\textit{bs}_1}\sum \textit{rs}_1)  \in \textit{rs}.  \forall r' \in \textit{rs}, \;
 \textit{either} \; r' = \ZERO \; \textit{or} \; r' = r \big)\; \textit{then} \; \textit{return} \; r$
 \end{center}
 \noindent
 Basically, $\textit{hollowAlternatives}$ captures the feature of
 a list of regular expression of the shape
 \begin{center}
-$  \oplus[\ZERO \;, \; _{bs}\oplus \textit{rs} ]$
+$  \sum[\ZERO \;, \; _{bs}\sum \textit{rs} ]$
 \end{center}
 and this means we can simply elevate the
-inner regular expression $_{bs}\oplus \textit{rs}$
+inner regular expression $_{bs}\sum \textit{rs}$
 to the outmost
 and throw away the useless $\ZERO$s and
-the outer $\oplus$ wrapper.
+the outer $\sum$ wrapper.
 Using this new definition of simp,
 under the example where  $r$ is the regular expression
 $(a+b)(a+a*)$ and $s$  is the string $aa$
 the problem of $\rup\backslash_{simp} \, s \neq \simp(\rup\backslash s)$
 is resolved.
 $\textit{sub}(\ONE) \dn \{\ONE\}$\\
 $\textit{sub}(r_1 \cdot r_2) \dn \textit{sub}(r_1) \cup \textit{sub}(r_2) \cup \{r_1 \cdot r_2\}$\\
 $\textit{sub}(r_1 + r_2) \dn \textit{sub}(r_1) \cup \textit{sub}(r_2) \cup \{r_1+r_2\}$\\
 \end{center}
 $\textit{good}(r) \dn r \neq \ZERO \land \\
-\forall r' \in \textit{sub}(r), \textit{if} \; r' = _{bs_1}\oplus(rs_1), \;
+\forall r' \in \textit{sub}(r), \textit{if} \; r' = _{bs_1}\sum(rs_1), \;
 \textit{then} \nexists r'' \in \textit{rs}_1 \; s.t.\;
-r'' = _{bs_2}\oplus \textit{rs}_2 $
+r'' = _{bs_2}\sum \textit{rs}_2 $
 The properties are mainly the ones below:
 \begin{itemize}
 \item
 \begin{center}
 $_{bs}{r_1 \cdot r_2}$ &
 $\gg$ &
 $\textit{bs} @ \textit{bs}_1 @ \textit{bs}_2$\\
 $\textit{if} \; r \gg \textit{bs}_1$ &  & $\textit{then}$  &
-$_{bs}{\oplus(r :: \textit{rs}})$ &
+$_{bs}{\sum(r :: \textit{rs}})$ &
 $\gg$ &
 $\textit{bs} @ \textit{bs}_1 $\\
-$\textit{if} \; _{bs}(\oplus \textit{rs}) \gg \textit{bs} @ \textit{bs}_1$ &  & $\textit{then}$  &
+$\textit{if} \; _{bs}(\sum \textit{rs}) \gg \textit{bs} @ \textit{bs}_1$ &  & $\textit{then}$  &
-$_{bs}{\oplus(r :: \textit{rs}})$ &
+$_{bs}{\sum(r :: \textit{rs}})$ &
 $\gg$ &
 $\textit{bs} @ \textit{bs}_1 $\\
 $\textit{if} \; r \gg \textit{bs}_1\; \textit{and}$ &  $_{bs}r^* \gg \textit{bs} @ \textit{bs}_2$ & $\textit{then}$  &
 $_{bs}r^* $ &

changeset 132	69292c2b54d8
parent 131	b6984212cf87
child 133	0172d422e93e