1 theory CpsG

     1 theory CpsG

     2 imports PrioG 

     2 imports PrioG 

     3 begin

     3 begin

     4 

     5 

     5 lemma not_thread_holdents:

     6 lemma not_thread_holdents:

     6   fixes th s

     7   fixes th s

     7   assumes vt: "vt s"

     8   assumes vt: "vt s"

     8   and not_in: "th \<notin> threads s" 

     9   and not_in: "th \<notin> threads s"