502 *}

   502 *}

   503 lemma running_preced_inversion:

   503 lemma running_preced_inversion:

   504   assumes running': "th' \<in> running (t @ s)"

   504   assumes running': "th' \<in> running (t @ s)"

   505   shows "cp (t @ s) th' = preced th s"

   505   shows "cp (t @ s) th' = preced th s"

   506 proof -

   506 proof -

   507   have "cp (t @ s) th' = Max (cp (t @ s) ` readys (t @ s))" using assms

   510   have "cp (t @ s) th' = Max (cp (t @ s) ` readys (t @ s))" using assms

   508       unfolding running_def by simp

   511       unfolding running_def by simp

   509   also have "... =  Max (cp (t @ s) ` threads (t @ s))"

   512   also have "... =  Max (cp (t @ s) ` threads (t @ s))"

   510       using vat_t.max_cp_readys_threads .

   513       using vat_t.max_cp_readys_threads .

   511   also have "... = cp (t @ s) th"

   514   also have "... = cp (t @ s) th"