--- a/PIPDefs.thy	Fri Dec 09 15:18:19 2016 +0000
+++ b/PIPDefs.thy	Mon Dec 19 23:43:54 2016 +0000
@@ -232,6 +232,13 @@
   apply(rule_tac f="Max" in arg_cong)
   by (auto)
 
+lemma cpreced_def3:
+  "cpreced wq s th \<equiv> Max (preceds ({th} \<union> dependants_raw wq th) s)"
+  unfolding cpreced_def2 image_def
+  apply(rule eq_reflection)
+  apply(rule_tac f="Max" in arg_cong)
+  by (auto)
+  
 definition 
   cpreceds :: "(cs \<Rightarrow> thread list) \<Rightarrow> state \<Rightarrow> thread set \<Rightarrow> precedence set"
   where