equal
deleted
inserted
replaced
893 qed |
893 qed |
894 |
894 |
895 lemma runing_inversion_3: |
895 lemma runing_inversion_3: |
896 assumes runing': "th' \<in> runing (t@s)" |
896 assumes runing': "th' \<in> runing (t@s)" |
897 and neq_th: "th' \<noteq> th" |
897 and neq_th: "th' \<noteq> th" |
898 shows "(th' \<noteq> th \<and> th' \<in> threads s \<and> cntV s th' < cntP s th')" |
898 shows "th' \<in> threads s \<and> cntV s th' < cntP s th'" |
899 proof - |
899 proof - |
900 from runing_inversion_2 [OF runing'] and neq_th |
900 from runing_inversion_2 [OF runing'] and neq_th |
901 show ?thesis by auto |
901 show ?thesis by auto |
902 qed |
902 qed |
903 |
903 |