692 

   692 

   693   The following lemma summarises the above lemmas to give an overall

   693   The following lemma summarises the above lemmas to give an overall

   694   characterisationof the blocking thread @{text "th'"}:

   694   characterisationof the blocking thread @{text "th'"}:

   695 

   695 

   696 *}

   696 *}

   698 lemma runing_inversion: (* ddd, one of the main lemmas to present *)

   698 lemma runing_inversion: (* ddd, one of the main lemmas to present *)

   699   assumes runing': "th' \<in> runing (t@s)"

   699   assumes runing': "th' \<in> runing (t@s)"

   700   and neq_th: "th' \<noteq> th"

   700   and neq_th: "th' \<noteq> th"

   701   shows "th' \<in> threads s"

   701   shows "th' \<in> threads s"

   702   and    "\<not>detached s th'"

   702   and    "\<not>detached s th'"