3782 case False |
3782 case False |
3783 have "Max (preceds (threads s) s) = Max (preceds (\<Union>th\<in>readys s. subtree (tG s) th) s)" |
3783 have "Max (preceds (threads s) s) = Max (preceds (\<Union>th\<in>readys s. subtree (tG s) th) s)" |
3784 unfolding threads_alt_def1 by simp |
3784 unfolding threads_alt_def1 by simp |
3785 also have "... = Max {Max (preceds (subtree (tG s) th) s) | th. th \<in> readys s}" |
3785 also have "... = Max {Max (preceds (subtree (tG s) th) s) | th. th \<in> readys s}" |
3786 apply(subst Max_Segments[symmetric]) |
3786 apply(subst Max_Segments[symmetric]) |
3787 prefer 5 |
3787 apply (simp add: finite_readys) |
|
3788 apply (simp add: fsbttGs.finite_subtree) |
|
3789 apply blast |
|
3790 using False apply blast |
3788 apply(rule arg_cong) |
3791 apply(rule arg_cong) |
3789 back |
3792 back |
3790 apply(blast) |
3793 apply(blast) |
3791 apply (simp add: finite_readys) |
3794 done |
3792 apply (simp add: fsbttGs.finite_subtree) |
|
3793 apply blast |
|
3794 using False by blast |
|
3795 also have "... = Max {cp s th | th. th \<in> readys s}" |
3795 also have "... = Max {cp s th | th. th \<in> readys s}" |
3796 unfolding cp_alt_def3 .. |
3796 unfolding cp_alt_def3 .. |
3797 finally show "Max (cp s ` readys s) = Max (preceds (threads s) s)" |
3797 finally show "Max (cp s ` readys s) = Max (preceds (threads s) s)" |
3798 by (simp add: Setcompr_eq_image image_def) |
3798 by (simp add: Setcompr_eq_image image_def) |
3799 qed (auto simp:threads_alt_def) |
3799 qed (auto simp:threads_alt_def) |