--- a/Correctness.thy	Thu Jan 28 13:46:45 2016 +0000
+++ b/Correctness.thy	Thu Jan 28 14:26:10 2016 +0000
@@ -2,6 +2,8 @@
 imports PIPBasics
 begin
 
+lemma Setcompr_eq_image: "{f x | x. x \<in> A} = f ` A"
+  by blast
 
 text {* 
   The following two auxiliary lemmas are used to reason about @{term Max}.
@@ -799,7 +801,7 @@
 
 *}
 
-lemma live: "runing (t@s) \<noteq> {}"
+lemma live: "runing (t @ s) \<noteq> {}"
 proof(cases "th \<in> runing (t@s)") 
   case True thus ?thesis by auto
 next