--- a/PIPBasics.thy	Fri Oct 21 14:47:01 2016 +0100
+++ b/PIPBasics.thy	Fri Dec 09 12:51:29 2016 +0000
@@ -3784,14 +3784,14 @@
     unfolding threads_alt_def1 by simp
   also have "... = Max {Max (preceds (subtree (tG s) th) s) | th. th \<in> readys s}"
     apply(subst Max_Segments[symmetric])
-    prefer 5  
+    apply (simp add: finite_readys)
+    apply (simp add: fsbttGs.finite_subtree)
+    apply blast
+    using False apply blast
     apply(rule arg_cong)
     back
     apply(blast)
-    apply (simp add: finite_readys)
-    apply (simp add: fsbttGs.finite_subtree)
-    apply blast
-    using False by blast
+    done 
   also have "... = Max {cp s th | th. th \<in> readys s}"
     unfolding cp_alt_def3 ..
   finally show "Max (cp s ` readys s) = Max (preceds (threads s) s)"