2190     apply(simp)

  2190     apply(simp)

  2191     done

  2191     done

  2192   hence eq_max: "Max ((\<lambda>th. preced th s) ` ({th1} \<union> dependants (wq s) th1)) =

  2192   hence eq_max: "Max ((\<lambda>th. preced th s) ` ({th1} \<union> dependants (wq s) th1)) =

  2193                  Max ((\<lambda>th. preced th s) ` ({th2} \<union> dependants (wq s) th2))"

  2193                  Max ((\<lambda>th. preced th s) ` ({th2} \<union> dependants (wq s) th2))"

  2194     (is "Max (?f ` ?A) = Max (?f ` ?B)")

  2194     (is "Max (?f ` ?A) = Max (?f ` ?B)")

  2196     unfolding cp_eq_cpreced 

  2195     unfolding cp_eq_cpreced 

  2197     unfolding cpreced_def .

  2196     unfolding cpreced_def .

  2198   obtain th1' where th1_in: "th1' \<in> ?A" and eq_f_th1: "?f th1' = Max (?f ` ?A)"

  2197   obtain th1' where th1_in: "th1' \<in> ?A" and eq_f_th1: "?f th1' = Max (?f ` ?A)"

  2200   proof -

  2198   proof -

  2201     have h1: "finite (?f ` ?A)"

  2199     have h1: "finite (?f ` ?A)"

  2202     proof -

  2200     proof -

  2203       have "finite ?A" 

  2201       have "finite ?A" 

  2204       proof -

  2202       proof -

  2229     moreover have h2: "(?f ` ?A) \<noteq> {}"

  2227     moreover have h2: "(?f ` ?A) \<noteq> {}"

  2230     proof -

  2228     proof -

  2231       have "?A \<noteq> {}" by simp

  2229       have "?A \<noteq> {}" by simp

  2232       thus ?thesis by simp

  2230       thus ?thesis by simp

  2233     qed

  2231     qed

  2235     from Max_in [OF h1 h2]

  2232     from Max_in [OF h1 h2]

  2236     have "Max (?f ` ?A) \<in> (?f ` ?A)" .

  2233     have "Max (?f ` ?A) \<in> (?f ` ?A)" .

  2237     thus ?thesis 

  2234     thus ?thesis 

  2238       thm cpreced_def

  2235       thm cpreced_def

  2239       unfolding cpreced_def[symmetric] 

  2236       unfolding cpreced_def[symmetric]