equal
deleted
inserted
replaced
567 from h have "(Th th, Th th') \<in> (RAG s')\<^sup>+" |
567 from h have "(Th th, Th th') \<in> (RAG s')\<^sup>+" |
568 by (unfold s_dependants_def, unfold eq_RAG, unfold eq_dep, auto) |
568 by (unfold s_dependants_def, unfold eq_RAG, unfold eq_dep, auto) |
569 from tranclD[OF this] |
569 from tranclD[OF this] |
570 obtain z where "(Th th, z) \<in> RAG s'" by auto |
570 obtain z where "(Th th, z) \<in> RAG s'" by auto |
571 with rd_th show "False" |
571 with rd_th show "False" |
572 apply (case_tac z, auto simp:readys_def s_waiting_def s_RAG_def s_waiting_def cs_waiting_def) |
572 apply (case_tac z, auto simp:readys_def s_RAG_def s_waiting_def cs_waiting_def) |
573 by (fold wq_def, blast) |
573 by (fold wq_def, blast) |
574 qed |
574 qed |
575 |
575 |
576 (* Result improved *) |
576 (* Result improved *) |
577 lemma eq_cp: |
577 lemma eq_cp: |