2591   using assms

  2591   using assms

  2592   using cnp_cnv_cncs not_thread_cncs by auto

  2592   using cnp_cnv_cncs not_thread_cncs by auto

  2593 

  2593 

  2594 end

  2594 end

  2595 

  2595 

  2597 lemma eq_RAG: 

  2596 lemma eq_RAG: 

  2598   "RAG (wq s) = RAG s"

  2597   "RAG (wq s) = RAG s"

  2599 by (unfold cs_RAG_def s_RAG_def, auto)

  2598 by (unfold cs_RAG_def s_RAG_def, auto)

  2600 

  2599 

  2601 context valid_trace

  2600 context valid_trace