diff --git a/thys/Posix-Lexing/document/root.bib b/thys/Posix-Lexing/document/root.bib
--- a/thys/Posix-Lexing/document/root.bib
+++ b/thys/Posix-Lexing/document/root.bib
@@ -1,10 +1,22 @@
 
 @inproceedings{Sulzmann2014,
   author    = {M.~Sulzmann and K.~Lu},
   title     = {{POSIX} {R}egular {E}xpression {P}arsing with {D}erivatives},
   booktitle = {Proc.~of the 12th International Conference on Functional and Logic Programming (FLOPS)},
   pages     = {203--220},
   year      = {2014},
   volume =    {8475},
   series =    {LNCS}
-}
\ No newline at end of file
+}
+
+@InProceedings{OkuiSuzuki2010,
+  author =       {S.~Okui and T.~Suzuki},
+  title =        {{D}isambiguation in {R}egular {E}xpression {M}atching via
+                  {P}osition {A}utomata with {A}ugmented {T}ransitions},
+  booktitle = {Proc.~of the 15th International Conference on Implementation
+                  and Application of Automata (CIAA)},
+  year =      {2010},
+  volume =    {6482},
+  series =    {LNCS},
+  pages =     {231--240}
+}
diff --git a/thys/Posix-Lexing/document/root.tex b/thys/Posix-Lexing/document/root.tex
--- a/thys/Posix-Lexing/document/root.tex
+++ b/thys/Posix-Lexing/document/root.tex
@@ -1,44 +1,49 @@
 \documentclass[11pt,a4paper]{article}
 \usepackage[T1]{fontenc}
 \usepackage{isabelle,isabellesym}
 \usepackage{amsmath}
 \usepackage{amssymb}
 \usepackage{eufrak}
 % this should be the last package used
 \usepackage{pdfsetup}
 
 % urls in roman style, theory text in math-similar italics
 \urlstyle{rm}
 \isabellestyle{it}
 
 
 \begin{document}
 
 \title{POSIX Lexing with Derivatives of Regular Expressions}
 \author{Fahad Ausaf \and Roy Dyckhoff \and Christian Urban}
 \maketitle
 
 \begin{abstract}
   Brzozowski introduced the notion of derivatives for regular
   expressions. They can be used for a very simple regular expression
   matching algorithm. Sulzmann and Lu \cite{Sulzmann2014} cleverly extended this algorithm
   in order to deal with POSIX matching, which is the underlying
   disambiguation strategy for regular expressions needed in
   lexers. In this entry we give our inductive definition
   of what a POSIX value is and show (i) that such a value is unique (for
   given regular expression and string being matched) and (ii) that
   Sulzmann and Lu's algorithm always generates such a value (provided
   that the regular expression matches the string). We also prove the
   correctness of an optimised version of the POSIX matching
-  algorithm. 
+  algorithm. Finally we show that
+  (iii) our inductive definition of a POSIX value is equivalent
+  to an alternative definition by Okui and Suzuki \cite{OkuiSuzuki2010} which
+  identifies POSIX values as least elements according to an
+  ordering of values. All results are given also for the bounded
+  regular expressions ($r^{n}$ and $r^{..n}$).
 \end{abstract}
 
 \tableofcontents
 
 % include generated text of all theories
 \input{session}
 
 \bibliographystyle{abbrv}
 \bibliography{root}
 
 \end{document}