equal
deleted
inserted
replaced
663 by (auto simp:tRAG_def RAG_split wRAG_def hRAG_def) |
663 by (auto simp:tRAG_def RAG_split wRAG_def hRAG_def) |
664 |
664 |
665 definition "cp_gen s x = |
665 definition "cp_gen s x = |
666 Max ((the_preced s \<circ> the_thread) ` subtree (tRAG s) x)" |
666 Max ((the_preced s \<circ> the_thread) ` subtree (tRAG s) x)" |
667 |
667 |
|
668 lemma cp_gen_alt_def: |
|
669 "cp_gen s = (Max \<circ> (\<lambda>x. (the_preced s \<circ> the_thread) ` subtree (tRAG s) x))" |
|
670 by (auto simp:cp_gen_def) |
|
671 |
|
672 |
668 (*<*) |
673 (*<*) |
669 |
674 |
670 end |
675 end |
671 (*>*) |
676 (*>*) |
672 |
677 |