--- a/Journal/Paper.thy	Thu May 18 14:30:08 2017 +0100
+++ b/Journal/Paper.thy	Thu May 18 15:11:49 2017 +0100
@@ -1706,6 +1706,18 @@
   defines in out list representation of states all the postfixes of 
   @{text t}.
 
+  \begin{theorem}
+  Given our assumptions about bounds, we have that 
+
+  \[
+  @{text "len"}\,[@{text "s'"} 
+  \leftarrow @{text "s upto t"}.\;\; @{text "th"} \not\in @{text "running s'"}] \leq 1 + 
+  \]
+
+  \[@{thm bounded_extend_highest.priority_inversion_is_finite_upto}\]
+  \end{theorem}
+
+
   Theorem: 
 
   \begin{isabelle}\ \ \ \ \ %%%