1775 

  1775 

  1776   \noindent With this in place we can conclude our theorem.\hfill\qed

  1776   \noindent With this in place we can conclude our theorem.\hfill\qed

  1777   \end{proof}

  1777   \end{proof}

  1778 

  1778 

  1779   \noindent This theorem is the main conclusion we obtain for the

  1779   \noindent This theorem is the main conclusion we obtain for the

  1781   is fixed at state @{text s} when @{text th} becomes the thread with

  1781   is fixed at state @{text s} when @{text th} becomes the thread with

  1782   highest priority. Then no additional blocker of @{text th} can

  1782   highest priority. Then no additional blocker of @{text th} can

  1783   appear after the state @{text s}. And in this way we can bound the

  1783   appear after the state @{text s}. And in this way we can bound the

  1784   number of states where the thread @{text th} with the highest

  1784   number of states where the thread @{text th} with the highest

  1785   priority is prevented from running.

  1785   priority is prevented from running.