--- a/PIPDefs.thy	Mon Feb 01 20:56:39 2016 +0800
+++ b/PIPDefs.thy	Wed Feb 03 12:04:03 2016 +0800
@@ -665,6 +665,11 @@
 definition "cp_gen s x =
                   Max ((the_preced s \<circ> the_thread) ` subtree (tRAG s) x)"
 
+lemma cp_gen_alt_def:
+  "cp_gen s = (Max \<circ> (\<lambda>x. (the_preced s \<circ> the_thread) ` subtree (tRAG s) x))"
+    by (auto simp:cp_gen_def)
+
+
 (*<*)
 
 end