747   then show "False" using a(1) by auto

   747   then show "False" using a(1) by auto

   748 qed

   748 qed

   749 

   749 

   750 

   750 

   751 

   751 

   756   (*

   752   (*

   757   obtain th0 where th0_in: "th0 \<in> S1 \<and> th0 \<in> S2" 

   753   obtain th0 where th0_in: "th0 \<in> S1 \<and> th0 \<in> S2" 

   758     and eq_f_th0: "preced th0 s = Max ((\<lambda>th. preced th s) ` (S1 \<inter> S2))"

   754     and eq_f_th0: "preced th0 s = Max ((\<lambda>th. preced th s) ` (S1 \<inter> S2))"

   759   proof -

   755   proof -

   760     from fin have h1: "finite ((\<lambda>th. preced th s) ` (S1 \<inter> S2))"

   756     from fin have h1: "finite ((\<lambda>th. preced th s) ` (S1 \<inter> S2))"

   782       apply(erule_tac preced_unique)

   778       apply(erule_tac preced_unique)

   783       done

   779       done

   784   qed

   780   qed

   785   *)

   781   *)

   786 

   782 

   787 end

   785 end