3134   } thus ?thesis by (unfold single_valued_def, auto)

  3134   } thus ?thesis by (unfold single_valued_def, auto)

  3135 qed

  3135 qed

  3136 

  3136 

  3137 end

  3137 end

  3138 

  3138 

  3139 text {*

  3141 text {*

  3140   It can be shown that @{term tRAG} is also a 

  3142   It can be shown that @{term tRAG} is also a 

  3141   finite-branch relational tree (or forest):  

  3143   finite-branch relational tree (or forest):  

  3142 *}

  3144 *}

  3143 

  3145 

  5461     show False

  5463     show False

  5462     using assms children_def holdents_alt_def by fastforce

  5464     using assms children_def holdents_alt_def by fastforce

  5463   qed

  5465   qed

  5464 qed

  5466 qed

  5465 

  5467 

  5466 lemma readys_RAG:

  5469 lemma readys_RAG:

  5467   assumes "th \<in> readys s"

  5470   assumes "th \<in> readys s"

  5468   shows "Th th \<notin> Domain (RAG s)"

  5471   shows "Th th \<notin> Domain (RAG s)"

  5469 proof

  5472 proof

  5470   assume "Th th \<in> Domain (RAG s)"

  5473   assume "Th th \<in> Domain (RAG s)"

  5474     assume "(Th th, b) \<in> RAG s"

  5477     assume "(Th th, b) \<in> RAG s"

  5475     with assms[unfolded readys_def s_waiting_def]

  5478     with assms[unfolded readys_def s_waiting_def]

  5476     show False

  5479     show False

  5477       using Collect_disj_eq s_RAG_def s_waiting_abv s_waiting_def wq_def by fastforce

  5480       using Collect_disj_eq s_RAG_def s_waiting_abv s_waiting_def wq_def by fastforce

  5478   qed

  5481   qed

  5479 qed

  5512 qed

  5480 

  5513 

  5481 lemma readys_holdents_detached:

  5514 lemma readys_holdents_detached:

  5482   assumes "th \<in> readys s"

  5515   assumes "th \<in> readys s"

  5483   and "holdents s th = {}"

  5516   and "holdents s th = {}"