1079   \begin{lemma}\label{runningpreced}

  1079   \begin{lemma}\label{runningpreced}

  1080   @{thm [mode=IfThen] running_preced_inversion}

  1080   @{thm [mode=IfThen] running_preced_inversion}

  1081   \end{lemma}

  1081   \end{lemma}

  1082 

  1082 

  1083   \begin{proof}

  1083   \begin{proof}

  1085   all ready threads, that is

  1085   all ready threads, that is

  1086 

  1086 

  1087   \begin{center}

  1087   \begin{center}

  1088   @{term "cp (t @ s) th' = Max (cp (t @ s) ` readys (t @ s))"}

  1088   @{term "cp (t @ s) th' = Max (cp (t @ s) ` readys (t @ s))"}

  1089   \end{center}

  1089   \end{center}