diff -r 57182b36ec01 -r 41a2a3b63853 thys2/Paper/document/root.tex
--- a/thys2/Paper/document/root.tex	Sun Feb 06 00:02:04 2022 +0000
+++ b/thys2/Paper/document/root.tex	Mon Feb 07 01:11:25 2022 +0000
@@ -49,7 +49,7 @@
 \def\S{\mathit{S}}
 \newcommand{\ZERO}{\mbox{\bf 0}}
 \newcommand{\ONE}{\mbox{\bf 1}}
-
+\def\rs{\mathit{rs}}
 
 \def\Brz{Brzozowski}
 \def\der{\backslash}
@@ -83,17 +83,19 @@
   of the regular expression.  The purpose of the bitcodes is to generate POSIX values incrementally while
   derivatives are calculated. They also help with designing
   an ``aggressive'' simplification function that keeps the size of
-  derivatives small. Without simplification the size derivatives can grow
-  exponentially resulting in an extremely slow lexing algorithm.  In this
+  derivatives finite. Without simplification the size derivatives can grow
+  arbitrarily big resulting in an extremely slow lexing algorithm.  In this
   paper we describe a variant of Sulzmann and Lu's algorithm: Our
   algorithm is a recursive functional program, whereas Sulzmann
   and Lu's version involves a fixpoint construction. We \textit{(i)}
   prove in Isabelle/HOL that our program is correct and generates
-  unique POSIX values; we also \textit{(ii)} establish a polynomial
-  bound for the size of the derivatives. The size can be seen as a
-  proxy measure for the efficiency of the lexing algorithm: because of
-  the polynomial bound our algorithm does not suffer from
-  the exponential blowup in earlier works.
+  unique POSIX values; we also \textit{(ii)} establish a finite
+  bound for the size of the derivatives.
+
+  %The size can be seen as a
+  %proxy measure for the efficiency of the lexing algorithm: because of
+  %the polynomial bound our algorithm does not suffer from
+  %the exponential blowup in earlier works.
   
   % Brzozowski introduced the notion of derivatives for regular
   % expressions. They can be used for a very simple regular expression