# HG changeset patch
# User Christian Urban <urbanc@in.tum.de>
# Date 1495116709 -3600
# Node ID c1028969401a04f1e13559a727e131db16718ffe
# Parent  39d4d1a2b1acbd5c92d6dca46e3bf4a30495cab0
updated

diff -r 39d4d1a2b1ac -r c1028969401a Journal/Paper.thy
--- 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}\ \ \ \ \ %%%
diff -r 39d4d1a2b1ac -r c1028969401a journal.pdf
Binary file journal.pdf has changed