1 theory CpsG

     1 theory CpsG

     2 imports PrioG 

     2 imports PrioG 

     3 begin

     3 begin

     5 

     4 

     6 lemma not_thread_holdents:

     5 lemma not_thread_holdents:

     7   fixes th s

     6   fixes th s

     8   assumes vt: "vt s"

     7   assumes vt: "vt s"

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

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