Correctness.thy
changeset 96 4805c6333fef
parent 95 8d2cc27f45f3
child 97 c7ba70dc49bd
equal deleted inserted replaced
95:8d2cc27f45f3 96:4805c6333fef
   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