equal
deleted
inserted
replaced
1704 |
1704 |
1705 \noindent Assume you have an extension @{text t}, this essentially |
1705 \noindent Assume you have an extension @{text t}, this essentially |
1706 defines in out list representation of states all the postfixes of |
1706 defines in out list representation of states all the postfixes of |
1707 @{text t}. |
1707 @{text t}. |
1708 |
1708 |
|
1709 \begin{theorem} |
|
1710 Given our assumptions about bounds, we have that |
|
1711 |
|
1712 \[ |
|
1713 @{text "len"}\,[@{text "s'"} |
|
1714 \leftarrow @{text "s upto t"}.\;\; @{text "th"} \not\in @{text "running s'"}] \leq 1 + |
|
1715 \] |
|
1716 |
|
1717 \[@{thm bounded_extend_highest.priority_inversion_is_finite_upto}\] |
|
1718 \end{theorem} |
|
1719 |
|
1720 |
1709 Theorem: |
1721 Theorem: |
1710 |
1722 |
1711 \begin{isabelle}\ \ \ \ \ %%% |
1723 \begin{isabelle}\ \ \ \ \ %%% |
1712 @{text "len (filter (\<lambda>t'. th \<notin> running t') (s upto t)) \<le> |
1724 @{text "len (filter (\<lambda>t'. th \<notin> running t') (s upto t)) \<le> |
1713 1 + len (actions_of blockers t) + len (filter isCreate t)"} |
1725 1 + len (actions_of blockers t) + len (filter isCreate t)"} |