equal
deleted
inserted
replaced
800 @{thm th_blockedE}. |
800 @{thm th_blockedE}. |
801 |
801 |
802 *} |
802 *} |
803 |
803 |
804 lemma live: "runing (t @ s) \<noteq> {}" |
804 lemma live: "runing (t @ s) \<noteq> {}" |
805 proof(cases "th \<in> runing (t@s)") |
805 proof(cases "th \<in> runing (t @ s)") |
806 case True thus ?thesis by auto |
806 case True thus ?thesis by auto |
807 next |
807 next |
808 case False |
808 case False |
809 thus ?thesis using th_blockedE by auto |
809 thus ?thesis using th_blockedE by auto |
810 qed |
810 qed |