diff -r 313acffe63b6 -r 92f61f6a0fe7 CpsG.thy
--- a/CpsG.thy	Tue May 20 12:49:21 2014 +0100
+++ b/CpsG.thy	Thu May 22 17:40:39 2014 +0100
@@ -1,6 +1,6 @@
 
 theory CpsG
-imports PrioG 
+imports PrioG Max
 begin
 
 lemma not_thread_holdents:
@@ -23,7 +23,7 @@
         and not_in': "thread \<notin> threads s"
       have "holdents (e # s) th = holdents s th"
         apply (unfold eq_e holdents_test)
-        by (simp add:depend_create_unchanged)
+        by (simp add:RAG_create_unchanged)
       moreover have "th \<notin> threads s" 
       proof -
         from not_in eq_e show ?thesis by simp
@@ -38,13 +38,13 @@
         case True
         with nh eq_e
         show ?thesis 
-          by (auto simp:holdents_test depend_exit_unchanged)
+          by (auto simp:holdents_test RAG_exit_unchanged)
       next
         case False
         with not_in and eq_e
         have "th \<notin> threads s" by simp
         from ih[OF this] False eq_e show ?thesis 
-          by (auto simp:holdents_test depend_exit_unchanged)
+          by (auto simp:holdents_test RAG_exit_unchanged)
       qed
     next
       case (thread_P thread cs)
@@ -60,7 +60,7 @@
       qed
       hence "holdents (e # s) th  = holdents s th "
         apply (unfold cntCS_def holdents_test eq_e)
-        by (unfold step_depend_p[OF vtp], auto)
+        by (unfold step_RAG_p[OF vtp], auto)
       moreover have "holdents s th = {}"
       proof(rule ih)
         from not_in eq_e show "th \<notin> threads s" by simp
@@ -102,7 +102,7 @@
       qed
       moreover note neq_th eq_wq
       ultimately have "holdents (e # s) th  = holdents s th"
-        by (unfold eq_e cntCS_def holdents_test step_depend_v[OF vtv], auto)
+        by (unfold eq_e cntCS_def holdents_test step_RAG_v[OF vtv], auto)
       moreover have "holdents s th = {}"
       proof(rule ih)
         from not_in eq_e show "th \<notin> threads s" by simp
@@ -117,12 +117,12 @@
       from ih [OF this] and eq_e
       show ?thesis 
         apply (unfold eq_e cntCS_def holdents_test)
-        by (simp add:depend_set_unchanged)
+        by (simp add:RAG_set_unchanged)
     qed
     next
       case vt_nil
       show ?case
-      by (auto simp:count_def holdents_test s_depend_def wq_def cs_holding_def)
+      by (auto simp:count_def holdents_test s_RAG_def wq_def cs_holding_def)
   qed
 qed
 
@@ -161,97 +161,33 @@
   shows "th1 = th2"
 using assms by (unfold next_th_def, auto)
 
-lemma wf_depend:
+lemma wf_RAG:
   assumes vt: "vt s"
-  shows "wf (depend s)"
+  shows "wf (RAG s)"
 proof(rule finite_acyclic_wf)
-  from finite_depend[OF vt] show "finite (depend s)" .
+  from finite_RAG[OF vt] show "finite (RAG s)" .
 next
-  from acyclic_depend[OF vt] show "acyclic (depend s)" .
+  from acyclic_RAG[OF vt] show "acyclic (RAG s)" .
 qed
 
-lemma Max_Union:
-  assumes fc: "finite C"
-  and ne: "C \<noteq> {}"
-  and fa: "\<And> A. A \<in> C \<Longrightarrow> finite A \<and> A \<noteq> {}"
-  shows "Max (\<Union> C) = Max (Max ` C)"
-proof -
-  from fc ne fa show ?thesis
-  proof(induct)
-    case (insert x F)
-    assume ih: "\<lbrakk>F \<noteq> {}; \<And>A. A \<in> F \<Longrightarrow> finite A \<and> A \<noteq> {}\<rbrakk> \<Longrightarrow> Max (\<Union>F) = Max (Max ` F)"
-    and h: "\<And> A. A \<in> insert x F \<Longrightarrow> finite A \<and> A \<noteq> {}"
-    show ?case (is "?L = ?R")
-    proof(cases "F = {}")
-      case False
-      from Union_insert have "?L = Max (x \<union> (\<Union> F))" by simp
-      also have "\<dots> = max (Max x) (Max(\<Union> F))"
-      proof(rule Max_Un)
-        from h[of x] show "finite x" by auto
-      next
-        from h[of x] show "x \<noteq> {}" by auto
-      next
-        show "finite (\<Union>F)"
-        proof(rule finite_Union)
-          show "finite F" by fact
-        next
-          from h show "\<And>M. M \<in> F \<Longrightarrow> finite M" by auto
-        qed
-      next
-        from False and h show "\<Union>F \<noteq> {}" by auto
-      qed
-      also have "\<dots> = ?R"
-      proof -
-        have "?R = Max (Max ` ({x} \<union> F))" by simp
-        also have "\<dots> = Max ({Max x} \<union> (Max ` F))" by simp
-        also have "\<dots> = max (Max x) (Max (\<Union>F))"
-        proof -
-          have "Max ({Max x} \<union> Max ` F) = max (Max {Max x}) (Max (Max ` F))"
-          proof(rule Max_Un)
-            show "finite {Max x}" by simp
-          next
-            show "{Max x} \<noteq> {}" by simp
-          next
-            from insert show "finite (Max ` F)" by auto
-          next
-            from False show "Max ` F \<noteq> {}" by auto
-          qed
-          moreover have "Max {Max x} = Max x" by simp
-          moreover have "Max (\<Union>F) = Max (Max ` F)"
-          proof(rule ih)
-            show "F \<noteq> {}" by fact
-          next
-            from h show "\<And>A. A \<in> F \<Longrightarrow> finite A \<and> A \<noteq> {}"
-              by auto
-          qed
-          ultimately show ?thesis by auto
-        qed
-        finally show ?thesis by simp
-      qed
-      finally show ?thesis by simp
-    next
-      case True
-      thus ?thesis by auto
-    qed
-  next
-    case empty
-    assume "{} \<noteq> {}" show ?case by auto
-  qed
-qed
+
 
 definition child :: "state \<Rightarrow> (node \<times> node) set"
   where "child s \<equiv>
-            {(Th th', Th th) | th th'. \<exists>cs. (Th th', Cs cs) \<in> depend s \<and> (Cs cs, Th th) \<in> depend s}"
+            {(Th th', Th th) | th th'. \<exists>cs. (Th th', Cs cs) \<in> RAG s \<and> (Cs cs, Th th) \<in> RAG s}"
 
 definition children :: "state \<Rightarrow> thread \<Rightarrow> thread set"
   where "children s th \<equiv> {th'. (Th th', Th th) \<in> child s}"
 
 lemma children_def2:
-  "children s th \<equiv> {th'. \<exists> cs. (Th th', Cs cs) \<in> depend s \<and> (Cs cs, Th th) \<in> depend s}"
+  "children s th \<equiv> {th'. \<exists> cs. (Th th', Cs cs) \<in> RAG s \<and> (Cs cs, Th th) \<in> RAG s}"
 unfolding child_def children_def by simp
 
-lemma children_dependants: "children s th \<subseteq> dependants (wq s) th"
-  by (unfold children_def child_def cs_dependants_def, auto simp:eq_depend)
+lemma children_dependants: 
+  "children s th \<subseteq> dependants (wq s) th"
+  unfolding children_def2
+  unfolding cs_dependants_def
+  by (auto simp add: eq_RAG)
 
 lemma child_unique:
   assumes vt: "vt s"
@@ -261,92 +197,92 @@
 using ch1 ch2 
 proof(unfold child_def, clarsimp)
   fix cs csa
-  assume h1: "(Th th, Cs cs) \<in> depend s"
-    and h2: "(Cs cs, Th th1) \<in> depend s"
-    and h3: "(Th th, Cs csa) \<in> depend s"
-    and h4: "(Cs csa, Th th2) \<in> depend s"
-  from unique_depend[OF vt h1 h3] have "cs = csa" by simp
-  with h4 have "(Cs cs, Th th2) \<in> depend s" by simp
-  from unique_depend[OF vt h2 this]
+  assume h1: "(Th th, Cs cs) \<in> RAG s"
+    and h2: "(Cs cs, Th th1) \<in> RAG s"
+    and h3: "(Th th, Cs csa) \<in> RAG s"
+    and h4: "(Cs csa, Th th2) \<in> RAG s"
+  from unique_RAG[OF vt h1 h3] have "cs = csa" by simp
+  with h4 have "(Cs cs, Th th2) \<in> RAG s" by simp
+  from unique_RAG[OF vt h2 this]
   show "th1 = th2" by simp
 qed 
 
-lemma depend_children:
-  assumes h: "(Th th1, Th th2) \<in> (depend s)^+"
-  shows "th1 \<in> children s th2 \<or> (\<exists> th3. th3 \<in> children s th2 \<and> (Th th1, Th th3) \<in> (depend s)^+)"
+lemma RAG_children:
+  assumes h: "(Th th1, Th th2) \<in> (RAG s)^+"
+  shows "th1 \<in> children s th2 \<or> (\<exists> th3. th3 \<in> children s th2 \<and> (Th th1, Th th3) \<in> (RAG s)^+)"
 proof -
   from h show ?thesis
   proof(induct rule: tranclE)
     fix c th2
-    assume h1: "(Th th1, c) \<in> (depend s)\<^sup>+"
-    and h2: "(c, Th th2) \<in> depend s"
+    assume h1: "(Th th1, c) \<in> (RAG s)\<^sup>+"
+    and h2: "(c, Th th2) \<in> RAG s"
     from h2 obtain cs where eq_c: "c = Cs cs"
-      by (case_tac c, auto simp:s_depend_def)
-    show "th1 \<in> children s th2 \<or> (\<exists>th3. th3 \<in> children s th2 \<and> (Th th1, Th th3) \<in> (depend s)\<^sup>+)"
+      by (case_tac c, auto simp:s_RAG_def)
+    show "th1 \<in> children s th2 \<or> (\<exists>th3. th3 \<in> children s th2 \<and> (Th th1, Th th3) \<in> (RAG s)\<^sup>+)"
     proof(rule tranclE[OF h1])
       fix ca
-      assume h3: "(Th th1, ca) \<in> (depend s)\<^sup>+"
-        and h4: "(ca, c) \<in> depend s"
-      show "th1 \<in> children s th2 \<or> (\<exists>th3. th3 \<in> children s th2 \<and> (Th th1, Th th3) \<in> (depend s)\<^sup>+)"
+      assume h3: "(Th th1, ca) \<in> (RAG s)\<^sup>+"
+        and h4: "(ca, c) \<in> RAG s"
+      show "th1 \<in> children s th2 \<or> (\<exists>th3. th3 \<in> children s th2 \<and> (Th th1, Th th3) \<in> (RAG s)\<^sup>+)"
       proof -
         from eq_c and h4 obtain th3 where eq_ca: "ca = Th th3"
-          by (case_tac ca, auto simp:s_depend_def)
+          by (case_tac ca, auto simp:s_RAG_def)
         from eq_ca h4 h2 eq_c
         have "th3 \<in> children s th2" by (auto simp:children_def child_def)
-        moreover from h3 eq_ca have "(Th th1, Th th3) \<in> (depend s)\<^sup>+" by simp
+        moreover from h3 eq_ca have "(Th th1, Th th3) \<in> (RAG s)\<^sup>+" by simp
         ultimately show ?thesis by auto
       qed
     next
-      assume "(Th th1, c) \<in> depend s"
+      assume "(Th th1, c) \<in> RAG s"
       with h2 eq_c
       have "th1 \<in> children s th2"
         by (auto simp:children_def child_def)
       thus ?thesis by auto
     qed
   next
-    assume "(Th th1, Th th2) \<in> depend s"
+    assume "(Th th1, Th th2) \<in> RAG s"
     thus ?thesis
-      by (auto simp:s_depend_def)
+      by (auto simp:s_RAG_def)
   qed
 qed
 
-lemma sub_child: "child s \<subseteq> (depend s)^+"
+lemma sub_child: "child s \<subseteq> (RAG s)^+"
   by (unfold child_def, auto)
 
 lemma wf_child: 
   assumes vt: "vt s"
   shows "wf (child s)"
 apply(rule wf_subset)
-apply(rule wf_trancl[OF wf_depend[OF vt]])
+apply(rule wf_trancl[OF wf_RAG[OF vt]])
 apply(rule sub_child)
 done
 
-lemma depend_child_pre:
+lemma RAG_child_pre:
   assumes vt: "vt s"
   shows
-  "(Th th, n) \<in> (depend s)^+ \<longrightarrow> (\<forall> th'. n = (Th th') \<longrightarrow> (Th th, Th th') \<in> (child s)^+)" (is "?P n")
+  "(Th th, n) \<in> (RAG s)^+ \<longrightarrow> (\<forall> th'. n = (Th th') \<longrightarrow> (Th th, Th th') \<in> (child s)^+)" (is "?P n")
 proof -
-  from wf_trancl[OF wf_depend[OF vt]]
-  have wf: "wf ((depend s)^+)" .
+  from wf_trancl[OF wf_RAG[OF vt]]
+  have wf: "wf ((RAG s)^+)" .
   show ?thesis
   proof(rule wf_induct[OF wf, of ?P], clarsimp)
     fix th'
-    assume ih[rule_format]: "\<forall>y. (y, Th th') \<in> (depend s)\<^sup>+ \<longrightarrow>
-               (Th th, y) \<in> (depend s)\<^sup>+ \<longrightarrow> (\<forall>th'. y = Th th' \<longrightarrow> (Th th, Th th') \<in> (child s)\<^sup>+)"
-    and h: "(Th th, Th th') \<in> (depend s)\<^sup>+"
+    assume ih[rule_format]: "\<forall>y. (y, Th th') \<in> (RAG s)\<^sup>+ \<longrightarrow>
+               (Th th, y) \<in> (RAG s)\<^sup>+ \<longrightarrow> (\<forall>th'. y = Th th' \<longrightarrow> (Th th, Th th') \<in> (child s)\<^sup>+)"
+    and h: "(Th th, Th th') \<in> (RAG s)\<^sup>+"
     show "(Th th, Th th') \<in> (child s)\<^sup>+"
     proof -
-      from depend_children[OF h]
-      have "th \<in> children s th' \<or> (\<exists>th3. th3 \<in> children s th' \<and> (Th th, Th th3) \<in> (depend s)\<^sup>+)" .
+      from RAG_children[OF h]
+      have "th \<in> children s th' \<or> (\<exists>th3. th3 \<in> children s th' \<and> (Th th, Th th3) \<in> (RAG s)\<^sup>+)" .
       thus ?thesis
       proof
         assume "th \<in> children s th'"
         thus "(Th th, Th th') \<in> (child s)\<^sup>+" by (auto simp:children_def)
       next
-        assume "\<exists>th3. th3 \<in> children s th' \<and> (Th th, Th th3) \<in> (depend s)\<^sup>+"
+        assume "\<exists>th3. th3 \<in> children s th' \<and> (Th th, Th th3) \<in> (RAG s)\<^sup>+"
         then obtain th3 where th3_in: "th3 \<in> children s th'" 
-          and th_dp: "(Th th, Th th3) \<in> (depend s)\<^sup>+" by auto
-        from th3_in have "(Th th3, Th th') \<in> (depend s)^+" by (auto simp:children_def child_def)
+          and th_dp: "(Th th, Th th3) \<in> (RAG s)\<^sup>+" by auto
+        from th3_in have "(Th th3, Th th') \<in> (RAG s)^+" by (auto simp:children_def child_def)
         from ih[OF this th_dp, of th3] have "(Th th, Th th3) \<in> (child s)\<^sup>+" by simp
         with th3_in show "(Th th, Th th') \<in> (child s)\<^sup>+" by (auto simp:children_def)
       qed
@@ -354,12 +290,12 @@
   qed
 qed
 
-lemma depend_child: "\<lbrakk>vt s; (Th th, Th th') \<in> (depend s)^+\<rbrakk> \<Longrightarrow> (Th th, Th th') \<in> (child s)^+"
-  by (insert depend_child_pre, auto)
+lemma RAG_child: "\<lbrakk>vt s; (Th th, Th th') \<in> (RAG s)^+\<rbrakk> \<Longrightarrow> (Th th, Th th') \<in> (child s)^+"
+  by (insert RAG_child_pre, auto)
 
-lemma child_depend_p:
+lemma child_RAG_p:
   assumes "(n1, n2) \<in> (child s)^+"
-  shows "(n1, n2) \<in> (depend s)^+"
+  shows "(n1, n2) \<in> (RAG s)^+"
 proof -
   from assms show ?thesis
   proof(induct)
@@ -368,26 +304,26 @@
   next
     case (step y z)
     assume "(y, z) \<in> child s"
-    with sub_child have "(y, z) \<in> (depend s)^+" by auto
-    moreover have "(n1, y) \<in> (depend s)^+" by fact
+    with sub_child have "(y, z) \<in> (RAG s)^+" by auto
+    moreover have "(n1, y) \<in> (RAG s)^+" by fact
     ultimately show ?case by auto
   qed
 qed
 
-lemma child_depend_eq: 
+lemma child_RAG_eq: 
   assumes vt: "vt s"
-  shows "(Th th1, Th th2) \<in> (child s)^+  \<longleftrightarrow> (Th th1, Th th2) \<in> (depend s)^+"
-  by (auto intro: depend_child[OF vt] child_depend_p)
+  shows "(Th th1, Th th2) \<in> (child s)^+  \<longleftrightarrow> (Th th1, Th th2) \<in> (RAG s)^+"
+  by (auto intro: RAG_child[OF vt] child_RAG_p)
 
 lemma children_no_dep:
   fixes s th th1 th2 th3
   assumes vt: "vt s"
   and ch1: "(Th th1, Th th) \<in> child s"
   and ch2: "(Th th2, Th th) \<in> child s"
-  and ch3: "(Th th1, Th th2) \<in> (depend s)^+"
+  and ch3: "(Th th1, Th th2) \<in> (RAG s)^+"
   shows "False"
 proof -
-  from depend_child[OF vt ch3]
+  from RAG_child[OF vt ch3]
   have "(Th th1, Th th2) \<in> (child s)\<^sup>+" .
   thus ?thesis
   proof(rule converse_tranclE)
@@ -412,15 +348,15 @@
   qed
 qed
 
-lemma unique_depend_p:
+lemma unique_RAG_p:
   assumes vt: "vt s"
-  and dp1: "(n, n1) \<in> (depend s)^+"
-  and dp2: "(n, n2) \<in> (depend s)^+"
+  and dp1: "(n, n1) \<in> (RAG s)^+"
+  and dp2: "(n, n2) \<in> (RAG s)^+"
   and neq: "n1 \<noteq> n2"
-  shows "(n1, n2) \<in> (depend s)^+ \<or> (n2, n1) \<in> (depend s)^+"
+  shows "(n1, n2) \<in> (RAG s)^+ \<or> (n2, n1) \<in> (RAG s)^+"
 proof(rule unique_chain [OF _ dp1 dp2 neq])
-  from unique_depend[OF vt]
-  show "\<And>a b c. \<lbrakk>(a, b) \<in> depend s; (a, c) \<in> depend s\<rbrakk> \<Longrightarrow> b = c" by auto
+  from unique_RAG[OF vt]
+  show "\<And>a b c. \<lbrakk>(a, b) \<in> RAG s; (a, c) \<in> RAG s\<rbrakk> \<Longrightarrow> b = c" by auto
 qed
 
 lemma dependants_child_unique:
@@ -433,47 +369,41 @@
 shows "th1 = th2"
 proof -
   { assume neq: "th1 \<noteq> th2"
-    from dp1 have dp1: "(Th th3, Th th1) \<in> (depend s)^+" 
-      by (simp add:s_dependants_def eq_depend)
-    from dp2 have dp2: "(Th th3, Th th2) \<in> (depend s)^+" 
-      by (simp add:s_dependants_def eq_depend)
-    from unique_depend_p[OF vt dp1 dp2] and neq
-    have "(Th th1, Th th2) \<in> (depend s)\<^sup>+ \<or> (Th th2, Th th1) \<in> (depend s)\<^sup>+" by auto
+    from dp1 have dp1: "(Th th3, Th th1) \<in> (RAG s)^+" 
+      by (simp add:s_dependants_def eq_RAG)
+    from dp2 have dp2: "(Th th3, Th th2) \<in> (RAG s)^+" 
+      by (simp add:s_dependants_def eq_RAG)
+    from unique_RAG_p[OF vt dp1 dp2] and neq
+    have "(Th th1, Th th2) \<in> (RAG s)\<^sup>+ \<or> (Th th2, Th th1) \<in> (RAG s)\<^sup>+" by auto
     hence False
     proof
-      assume "(Th th1, Th th2) \<in> (depend s)\<^sup>+ "
+      assume "(Th th1, Th th2) \<in> (RAG s)\<^sup>+ "
       from children_no_dep[OF vt ch1 ch2 this] show ?thesis .
     next
-      assume " (Th th2, Th th1) \<in> (depend s)\<^sup>+"
+      assume " (Th th2, Th th1) \<in> (RAG s)\<^sup>+"
       from children_no_dep[OF vt ch2 ch1 this] show ?thesis .
     qed
   } thus ?thesis by auto
 qed
 
-lemma depend_plus_elim:
+lemma RAG_plus_elim:
   assumes "vt s"
   fixes x
-  assumes "(Th x, Th th) \<in> (depend (wq s))\<^sup>+"
-  shows "\<exists>th'\<in>children s th. x = th' \<or> (Th x, Th th') \<in> (depend (wq s))\<^sup>+"
-  using assms(2)[unfolded eq_depend, folded child_depend_eq[OF `vt s`]]
+  assumes "(Th x, Th th) \<in> (RAG (wq s))\<^sup>+"
+  shows "\<exists>th'\<in>children s th. x = th' \<or> (Th x, Th th') \<in> (RAG (wq s))\<^sup>+"
+  using assms(2)[unfolded eq_RAG, folded child_RAG_eq[OF `vt s`]]
   apply (unfold children_def)
-  by (metis assms(2) children_def depend_children eq_depend)
-
-lemma dependants_expand_pre: 
-  assumes "vt s"
-  shows "dependants (wq s) th = (\<Union> th' \<in> children s th. {th'} \<union> dependants (wq s) th')"
-  apply (unfold cs_dependants_def)
-  apply (auto elim!:depend_plus_elim[OF assms])
-  apply (metis children_def eq_depend mem_Collect_eq set_mp sub_child)
-  apply (unfold children_def, auto)
-  apply (unfold eq_depend, fold  child_depend_eq[OF `vt s`])
-  by (metis trancl.simps)
+  by (metis assms(2) children_def RAG_children eq_RAG)
 
 lemma dependants_expand:
   assumes "vt s"
-  shows "dependants (wq s) th = (\<Union> ((\<lambda> th. {th} \<union> dependants (wq s) th) ` (children s th)))"
-  apply (subst dependants_expand_pre[OF assms])
-  by simp
+  shows "dependants (wq s) th = (children s th) \<union> (\<Union>((dependants (wq s)) ` children s th))"
+apply(simp add: image_def)
+unfolding cs_dependants_def
+apply(auto)
+apply (metis assms RAG_plus_elim mem_Collect_eq)
+apply (metis child_RAG_p children_def eq_RAG mem_Collect_eq r_into_trancl')
+by (metis assms child_RAG_eq children_def eq_RAG mem_Collect_eq trancl.trancl_into_trancl)
 
 lemma finite_children:
   assumes "vt s"
@@ -487,23 +417,11 @@
   using dependants_threads[OF assms] finite_threads[OF assms]
   by (metis rev_finite_subset)
 
-lemma Max_insert:
-  assumes "finite B"
-  and  "B \<noteq> {}"
-  shows "Max ({x} \<union> B) = max x (Max B)"
-  by (metis Max_insert assms insert_is_Un)
-
-lemma dependands_expand2:
-  assumes "vt s"
-  shows "dependants (wq s) th = (children s th) \<union> (\<Union>((dependants (wq s)) ` children s th))"
-  by (subst dependants_expand[OF assms]) (auto)
+abbreviation
+  "preceds s ths \<equiv> {preced th s| th. th \<in> ths}"
 
 abbreviation
-  "preceds s Ths \<equiv> {preced th s| th. th \<in> Ths}"
-
-lemma image_compr:
-  "f ` A = {f x | x. x \<in> A}"
-by auto
+  "cpreceds s ths \<equiv> (cp s) ` ths"
 
 lemma Un_compr:
   "{f th | th. R th \<or> Q th} = ({f th | th. R th} \<union> {f th' | th'. Q th'})"
@@ -531,11 +449,11 @@
   show ?thesis (is "?LHS = ?RHS")
   proof -
     have eq_cp: "cp s = (\<lambda>th. Max (preceds s ({th} \<union> dependants (wq s) th)))"
-      by (simp add: fun_eq_iff cp_eq_cpreced cpreced_def Un_compr image_compr[symmetric])
+      by (simp add: fun_eq_iff cp_eq_cpreced cpreced_def Un_compr image_Collect[symmetric])
   
     have not_emptyness_facts[simp]: 
       "dependants (wq s) th \<noteq> {}" "children s th \<noteq> {}"
-      using False dependands_expand2[OF assms] by(auto simp only: Un_empty)
+      using False dependants_expand[OF assms] by(auto simp only: Un_empty)
 
     have finiteness_facts[simp]:
       "\<And>th. finite (dependants (wq s) th)" "\<And>th. finite (children s th)"
@@ -552,7 +470,7 @@
     (* expanding dependants *)
     also have "\<dots> = max (Max {preced th s}) 
       (Max (preceds s (children s th \<union> \<Union>(dependants (wq s) ` children s th))))"
-      by (subst dependands_expand2[OF `vt s`]) (simp)
+      by (subst dependants_expand[OF `vt s`]) (simp)
 
     (* moving out big Union *)
     also have "\<dots> = max (Max {preced th s})
@@ -602,8 +520,8 @@
     by (unfold s_def, auto simp:preced_def)
 qed
 
-lemma eq_dep: "depend s = depend s'"
-  by (unfold s_def depend_set_unchanged, auto)
+lemma eq_dep: "RAG s = RAG s'"
+  by (unfold s_def RAG_set_unchanged, auto)
 
 lemma eq_cp_pre:
   fixes th' 
@@ -613,7 +531,7 @@
   apply (unfold cp_eq_cpreced cpreced_def)
 proof -
   have eq_dp: "\<And> th. dependants (wq s) th = dependants (wq s') th"
-    by (unfold cs_dependants_def, auto simp:eq_dep eq_depend)
+    by (unfold cs_dependants_def, auto simp:eq_dep eq_RAG)
   moreover {
     fix th1 
     assume "th1 \<in> {th'} \<union> dependants (wq s') th'"
@@ -626,7 +544,7 @@
     next
       assume "th1 \<in> dependants (wq s') th'"
       with nd and eq_dp have "th1 \<noteq> th"
-        by (auto simp:eq_depend cs_dependants_def s_dependants_def eq_dep)
+        by (auto simp:eq_RAG cs_dependants_def s_dependants_def eq_dep)
       from eq_preced[OF this] show "preced th1 s = preced th1 s'" by simp
     qed
   } ultimately have "((\<lambda>th. preced th s) ` ({th'} \<union> dependants (wq s) th')) = 
@@ -646,12 +564,12 @@
   hence "th \<in> runing s'" by (cases, simp)
   hence rd_th: "th \<in> readys s'" 
     by (simp add:readys_def runing_def)
-  from h have "(Th th, Th th') \<in> (depend s')\<^sup>+"
-    by (unfold s_dependants_def, unfold eq_depend, unfold eq_dep, auto)
+  from h have "(Th th, Th th') \<in> (RAG s')\<^sup>+"
+    by (unfold s_dependants_def, unfold eq_RAG, unfold eq_dep, auto)
   from tranclD[OF this]
-  obtain z where "(Th th, z) \<in> depend s'" by auto
+  obtain z where "(Th th, z) \<in> RAG s'" by auto
   with rd_th show "False"
-    apply (case_tac z, auto simp:readys_def s_waiting_def s_depend_def s_waiting_def cs_waiting_def)
+    apply (case_tac z, auto simp:readys_def s_waiting_def s_RAG_def s_waiting_def cs_waiting_def)
     by (fold wq_def, blast)
 qed
 
@@ -673,8 +591,8 @@
   shows "cp s th'' = cp s' th''"
 proof -
   from dp2
-  have "(Th th', Th th'') \<in> (depend (wq s))\<^sup>+" by (simp add:s_dependants_def)
-  from depend_child[OF vt_s this[unfolded eq_depend]]
+  have "(Th th', Th th'') \<in> (RAG (wq s))\<^sup>+" by (simp add:s_dependants_def)
+  from RAG_child[OF vt_s this[unfolded eq_RAG]]
   have ch_th': "(Th th', Th th'') \<in> (child s)\<^sup>+" .
   moreover { fix n th''
     have "\<lbrakk>(Th th', n) \<in> (child s)^+\<rbrakk> \<Longrightarrow>
@@ -686,10 +604,10 @@
         and ch': "(Th th', y) \<in> (child s)\<^sup>+"
       from y_ch obtain thy where eq_y: "y = Th thy" by (auto simp:child_def)
       with ih have eq_cpy:"cp s thy = cp s' thy" by blast
-      from dp1 have "(Th th, Th th') \<in> (depend s)^+" by (auto simp:s_dependants_def eq_depend)
-      moreover from child_depend_p[OF ch'] and eq_y
-      have "(Th th', Th thy) \<in> (depend s)^+" by simp
-      ultimately have dp_thy: "(Th th, Th thy) \<in> (depend s)^+" by auto
+      from dp1 have "(Th th, Th th') \<in> (RAG s)^+" by (auto simp:s_dependants_def eq_RAG)
+      moreover from child_RAG_p[OF ch'] and eq_y
+      have "(Th th', Th thy) \<in> (RAG s)^+" by simp
+      ultimately have dp_thy: "(Th th, Th thy) \<in> (RAG s)^+" by auto
       show "cp s th'' = cp s' th''"
         apply (subst cp_rec[OF vt_s])
       proof -
@@ -699,9 +617,9 @@
           proof
             assume "th'' = th"
             with dp_thy y_ch[unfolded eq_y] 
-            have "(Th th, Th th) \<in> (depend s)^+"
+            have "(Th th, Th th) \<in> (RAG s)^+"
               by (auto simp:child_def)
-            with wf_trancl[OF wf_depend[OF vt_s]] 
+            with wf_trancl[OF wf_RAG[OF vt_s]] 
             show False by auto
           qed
         qed
@@ -717,14 +635,14 @@
             have neq_th1: "th1 \<noteq> th"
             proof
               assume eq_th1: "th1 = th"
-              with dp_thy have "(Th th1, Th thy) \<in> (depend s)^+" by simp
+              with dp_thy have "(Th th1, Th thy) \<in> (RAG s)^+" by simp
               from children_no_dep[OF vt_s _ _ this] and 
               th1_in y_ch eq_y show False by (auto simp:children_def)
             qed
             have "th \<notin> dependants s th1"
             proof
               assume h:"th \<in> dependants s th1"
-              from eq_y dp_thy have "th \<in> dependants s thy" by (auto simp:s_dependants_def eq_depend)
+              from eq_y dp_thy have "th \<in> dependants s thy" by (auto simp:s_dependants_def eq_RAG)
               from dependants_child_unique[OF vt_s _ _ h this]
               th1_in y_ch eq_y have "th1 = thy" by (auto simp:children_def child_def)
               with False show False by auto
@@ -736,7 +654,7 @@
         ultimately have "{preced th'' s} \<union> (cp s ` children s th'') = 
           {preced th'' s'} \<union> (cp s' ` children s th'')" by (auto simp:image_def)
         moreover have "children s th'' = children s' th''"
-          by (unfold children_def child_def s_def depend_set_unchanged, simp)
+          by (unfold children_def child_def s_def RAG_set_unchanged, simp)
         ultimately show "Max ({preced th'' s} \<union> cp s ` children s th'') = cp s' th''"
           by (simp add:cp_rec[OF step_back_vt[OF vt_s[unfolded s_def]]])
       qed
@@ -752,9 +670,9 @@
           proof
             assume "th'' = th"
             with dp1 dp'
-            have "(Th th, Th th) \<in> (depend s)^+"
-              by (auto simp:child_def s_dependants_def eq_depend)
-            with wf_trancl[OF wf_depend[OF vt_s]] 
+            have "(Th th, Th th) \<in> (RAG s)^+"
+              by (auto simp:child_def s_dependants_def eq_RAG)
+            with wf_trancl[OF wf_RAG[OF vt_s]] 
             show False by auto
           qed
         qed
@@ -770,8 +688,8 @@
             have neq_th1: "th1 \<noteq> th"
             proof
               assume eq_th1: "th1 = th"
-              with dp1 have "(Th th1, Th th') \<in> (depend s)^+" 
-                by (auto simp:s_dependants_def eq_depend)
+              with dp1 have "(Th th1, Th th') \<in> (RAG s)^+" 
+                by (auto simp:s_dependants_def eq_RAG)
               from children_no_dep[OF vt_s _ _ this]
               th1_in dp'
               show False by (auto simp:children_def)
@@ -792,7 +710,7 @@
         ultimately have "{preced th'' s} \<union> (cp s ` children s th'') = 
           {preced th'' s'} \<union> (cp s' ` children s th'')" by (auto simp:image_def)
         moreover have "children s th'' = children s' th''"
-          by (unfold children_def child_def s_def depend_set_unchanged, simp)
+          by (unfold children_def child_def s_def RAG_set_unchanged, simp)
         ultimately show "Max ({preced th'' s} \<union> cp s ` children s th'') = cp s' th''"
           by (simp add:cp_rec[OF step_back_vt[OF vt_s[unfolded s_def]]])
       qed     
@@ -808,8 +726,8 @@
   shows "cp s th'' = cp s' th''"
 proof -
   from dp
-  have "(Th th, Th th'') \<in> (depend (wq s))\<^sup>+" by (simp add:s_dependants_def)
-  from depend_child[OF vt_s this[unfolded eq_depend]]
+  have "(Th th, Th th'') \<in> (RAG (wq s))\<^sup>+" by (simp add:s_dependants_def)
+  from RAG_child[OF vt_s this[unfolded eq_RAG]]
   have ch_th': "(Th th, Th th'') \<in> (child s)\<^sup>+" .
   moreover { fix n th''
     have "\<lbrakk>(Th th, n) \<in> (child s)^+\<rbrakk> \<Longrightarrow>
@@ -821,8 +739,8 @@
         and ch': "(Th th, y) \<in> (child s)\<^sup>+"
       from y_ch obtain thy where eq_y: "y = Th thy" by (auto simp:child_def)
       with ih have eq_cpy:"cp s thy = cp s' thy" by blast
-      from child_depend_p[OF ch'] and eq_y
-      have dp_thy: "(Th th, Th thy) \<in> (depend s)^+" by simp
+      from child_RAG_p[OF ch'] and eq_y
+      have dp_thy: "(Th th, Th thy) \<in> (RAG s)^+" by simp
       show "cp s th'' = cp s' th''"
         apply (subst cp_rec[OF vt_s])
       proof -
@@ -832,9 +750,9 @@
           proof
             assume "th'' = th"
             with dp_thy y_ch[unfolded eq_y] 
-            have "(Th th, Th th) \<in> (depend s)^+"
+            have "(Th th, Th th) \<in> (RAG s)^+"
               by (auto simp:child_def)
-            with wf_trancl[OF wf_depend[OF vt_s]] 
+            with wf_trancl[OF wf_RAG[OF vt_s]] 
             show False by auto
           qed
         qed
@@ -850,14 +768,14 @@
             have neq_th1: "th1 \<noteq> th"
             proof
               assume eq_th1: "th1 = th"
-              with dp_thy have "(Th th1, Th thy) \<in> (depend s)^+" by simp
+              with dp_thy have "(Th th1, Th thy) \<in> (RAG s)^+" by simp
               from children_no_dep[OF vt_s _ _ this] and 
               th1_in y_ch eq_y show False by (auto simp:children_def)
             qed
             have "th \<notin> dependants s th1"
             proof
               assume h:"th \<in> dependants s th1"
-              from eq_y dp_thy have "th \<in> dependants s thy" by (auto simp:s_dependants_def eq_depend)
+              from eq_y dp_thy have "th \<in> dependants s thy" by (auto simp:s_dependants_def eq_RAG)
               from dependants_child_unique[OF vt_s _ _ h this]
               th1_in y_ch eq_y have "th1 = thy" by (auto simp:children_def child_def)
               with False show False by auto
@@ -869,7 +787,7 @@
         ultimately have "{preced th'' s} \<union> (cp s ` children s th'') = 
           {preced th'' s'} \<union> (cp s' ` children s th'')" by (auto simp:image_def)
         moreover have "children s th'' = children s' th''"
-          by (unfold children_def child_def s_def depend_set_unchanged, simp)
+          by (unfold children_def child_def s_def RAG_set_unchanged, simp)
         ultimately show "Max ({preced th'' s} \<union> cp s ` children s th'') = cp s' th''"
           by (simp add:cp_rec[OF step_back_vt[OF vt_s[unfolded s_def]]])
       qed
@@ -885,9 +803,9 @@
           proof
             assume "th'' = th"
             with dp dp'
-            have "(Th th, Th th) \<in> (depend s)^+"
-              by (auto simp:child_def s_dependants_def eq_depend)
-            with wf_trancl[OF wf_depend[OF vt_s]] 
+            have "(Th th, Th th) \<in> (RAG s)^+"
+              by (auto simp:child_def s_dependants_def eq_RAG)
+            with wf_trancl[OF wf_RAG[OF vt_s]] 
             show False by auto
           qed
         qed
@@ -906,7 +824,7 @@
               show "th \<notin> dependants s th1"
               proof
                 assume "th \<in> dependants s th1"
-                hence "(Th th, Th th1) \<in> (depend s)^+" by (auto simp:s_dependants_def eq_depend)
+                hence "(Th th, Th th1) \<in> (RAG s)^+" by (auto simp:s_dependants_def eq_RAG)
                 from children_no_dep[OF vt_s _ _ this]
                 and th1_in dp' show False
                   by (auto simp:children_def)
@@ -917,7 +835,7 @@
         ultimately have "{preced th'' s} \<union> (cp s ` children s th'') = 
           {preced th'' s'} \<union> (cp s' ` children s th'')" by (auto simp:image_def)
         moreover have "children s th'' = children s' th''"
-          by (unfold children_def child_def s_def depend_set_unchanged, simp)
+          by (unfold children_def child_def s_def RAG_set_unchanged, simp)
         ultimately show "Max ({preced th'' s} \<union> cp s ` children s th'') = cp s' th''"
           by (simp add:cp_rec[OF step_back_vt[OF vt_s[unfolded s_def]]])
       qed     
@@ -998,11 +916,11 @@
 context step_v_cps_nt
 begin
 
-lemma depend_s:
-  "depend s = (depend s' - {(Cs cs, Th th), (Th th', Cs cs)}) \<union>
+lemma RAG_s:
+  "RAG s = (RAG s' - {(Cs cs, Th th), (Th th', Cs cs)}) \<union>
                                          {(Cs cs, Th th')}"
 proof -
-  from step_depend_v[OF vt_s[unfolded s_def], folded s_def]
+  from step_RAG_v[OF vt_s[unfolded s_def], folded s_def]
     and nt show ?thesis  by (auto intro:next_th_unique)
 qed
 
@@ -1014,163 +932,163 @@
 proof(auto)
   fix x
   assume "x \<in> dependants (wq s) th''"
-  hence dp: "(Th x, Th th'') \<in> (depend s)^+"
-    by (auto simp:cs_dependants_def eq_depend)
+  hence dp: "(Th x, Th th'') \<in> (RAG s)^+"
+    by (auto simp:cs_dependants_def eq_RAG)
   { fix n
-    have "(n, Th th'') \<in> (depend s)^+ \<Longrightarrow>  (n, Th th'') \<in> (depend s')^+"
+    have "(n, Th th'') \<in> (RAG s)^+ \<Longrightarrow>  (n, Th th'') \<in> (RAG s')^+"
     proof(induct rule:converse_trancl_induct)
       fix y 
-      assume "(y, Th th'') \<in> depend s"
-      with depend_s neq1 neq2
-      have "(y, Th th'') \<in> depend s'" by auto
-      thus "(y, Th th'') \<in> (depend s')\<^sup>+" by auto
+      assume "(y, Th th'') \<in> RAG s"
+      with RAG_s neq1 neq2
+      have "(y, Th th'') \<in> RAG s'" by auto
+      thus "(y, Th th'') \<in> (RAG s')\<^sup>+" by auto
     next
       fix y z 
-      assume yz: "(y, z) \<in> depend s"
-        and ztp: "(z, Th th'') \<in> (depend s)\<^sup>+"
-        and ztp': "(z, Th th'') \<in> (depend s')\<^sup>+"
+      assume yz: "(y, z) \<in> RAG s"
+        and ztp: "(z, Th th'') \<in> (RAG s)\<^sup>+"
+        and ztp': "(z, Th th'') \<in> (RAG s')\<^sup>+"
       have "y \<noteq> Cs cs \<and> y \<noteq> Th th'"
       proof
         show "y \<noteq> Cs cs"
         proof
           assume eq_y: "y = Cs cs"
-          with yz have dp_yz: "(Cs cs, z) \<in> depend s" by simp
-          from depend_s
-          have cst': "(Cs cs, Th th') \<in> depend s" by simp
-          from unique_depend[OF vt_s this dp_yz] 
+          with yz have dp_yz: "(Cs cs, z) \<in> RAG s" by simp
+          from RAG_s
+          have cst': "(Cs cs, Th th') \<in> RAG s" by simp
+          from unique_RAG[OF vt_s this dp_yz] 
           have eq_z: "z = Th th'" by simp
-          with ztp have "(Th th', Th th'') \<in> (depend s)^+" by simp
+          with ztp have "(Th th', Th th'') \<in> (RAG s)^+" by simp
           from converse_tranclE[OF this]
-          obtain cs' where dp'': "(Th th', Cs cs') \<in> depend s"
-            by (auto simp:s_depend_def)
-          with depend_s have dp': "(Th th', Cs cs') \<in> depend s'" by auto
-          from dp'' eq_y yz eq_z have "(Cs cs, Cs cs') \<in> (depend s)^+" by auto
+          obtain cs' where dp'': "(Th th', Cs cs') \<in> RAG s"
+            by (auto simp:s_RAG_def)
+          with RAG_s have dp': "(Th th', Cs cs') \<in> RAG s'" by auto
+          from dp'' eq_y yz eq_z have "(Cs cs, Cs cs') \<in> (RAG s)^+" by auto
           moreover have "cs' = cs"
           proof -
             from next_waiting[OF step_back_vt[OF vt_s[unfolded s_def]] nt]
-            have "(Th th', Cs cs) \<in> depend s'"
-              by (auto simp:s_waiting_def wq_def s_depend_def cs_waiting_def)
-            from unique_depend[OF step_back_vt[OF vt_s[unfolded s_def]] this dp']
+            have "(Th th', Cs cs) \<in> RAG s'"
+              by (auto simp:s_waiting_def wq_def s_RAG_def cs_waiting_def)
+            from unique_RAG[OF step_back_vt[OF vt_s[unfolded s_def]] this dp']
             show ?thesis by simp
           qed
-          ultimately have "(Cs cs, Cs cs) \<in> (depend s)^+" by simp
-          moreover note wf_trancl[OF wf_depend[OF vt_s]]
+          ultimately have "(Cs cs, Cs cs) \<in> (RAG s)^+" by simp
+          moreover note wf_trancl[OF wf_RAG[OF vt_s]]
           ultimately show False by auto
         qed
       next
         show "y \<noteq> Th th'"
         proof
           assume eq_y: "y = Th th'"
-          with yz have dps: "(Th th', z) \<in> depend s" by simp
-          with depend_s have dps': "(Th th', z) \<in> depend s'" by auto
+          with yz have dps: "(Th th', z) \<in> RAG s" by simp
+          with RAG_s have dps': "(Th th', z) \<in> RAG s'" by auto
           have "z = Cs cs"
           proof -
             from next_waiting[OF step_back_vt[OF vt_s[unfolded s_def]] nt]
-            have "(Th th', Cs cs) \<in> depend s'"
-              by (auto simp:s_waiting_def wq_def s_depend_def cs_waiting_def)
-            from unique_depend[OF step_back_vt[OF vt_s[unfolded s_def]] dps' this]
+            have "(Th th', Cs cs) \<in> RAG s'"
+              by (auto simp:s_waiting_def wq_def s_RAG_def cs_waiting_def)
+            from unique_RAG[OF step_back_vt[OF vt_s[unfolded s_def]] dps' this]
             show ?thesis .
           qed
-          with dps depend_s show False by auto
+          with dps RAG_s show False by auto
         qed
       qed
-      with depend_s yz have "(y, z) \<in> depend s'" by auto
+      with RAG_s yz have "(y, z) \<in> RAG s'" by auto
       with ztp'
-      show "(y, Th th'') \<in> (depend s')\<^sup>+" by auto
+      show "(y, Th th'') \<in> (RAG s')\<^sup>+" by auto
     qed    
   }
   from this[OF dp]
   show "x \<in> dependants (wq s') th''" 
-    by (auto simp:cs_dependants_def eq_depend)
+    by (auto simp:cs_dependants_def eq_RAG)
 next
   fix x
   assume "x \<in> dependants (wq s') th''"
-  hence dp: "(Th x, Th th'') \<in> (depend s')^+"
-    by (auto simp:cs_dependants_def eq_depend)
+  hence dp: "(Th x, Th th'') \<in> (RAG s')^+"
+    by (auto simp:cs_dependants_def eq_RAG)
   { fix n
-    have "(n, Th th'') \<in> (depend s')^+ \<Longrightarrow>  (n, Th th'') \<in> (depend s)^+"
+    have "(n, Th th'') \<in> (RAG s')^+ \<Longrightarrow>  (n, Th th'') \<in> (RAG s)^+"
     proof(induct rule:converse_trancl_induct)
       fix y 
-      assume "(y, Th th'') \<in> depend s'"
-      with depend_s neq1 neq2
-      have "(y, Th th'') \<in> depend s" by auto
-      thus "(y, Th th'') \<in> (depend s)\<^sup>+" by auto
+      assume "(y, Th th'') \<in> RAG s'"
+      with RAG_s neq1 neq2
+      have "(y, Th th'') \<in> RAG s" by auto
+      thus "(y, Th th'') \<in> (RAG s)\<^sup>+" by auto
     next
       fix y z 
-      assume yz: "(y, z) \<in> depend s'"
-        and ztp: "(z, Th th'') \<in> (depend s')\<^sup>+"
-        and ztp': "(z, Th th'') \<in> (depend s)\<^sup>+"
+      assume yz: "(y, z) \<in> RAG s'"
+        and ztp: "(z, Th th'') \<in> (RAG s')\<^sup>+"
+        and ztp': "(z, Th th'') \<in> (RAG s)\<^sup>+"
       have "y \<noteq> Cs cs \<and> y \<noteq> Th th'"
       proof
         show "y \<noteq> Cs cs"
         proof
           assume eq_y: "y = Cs cs"
-          with yz have dp_yz: "(Cs cs, z) \<in> depend s'" by simp
+          with yz have dp_yz: "(Cs cs, z) \<in> RAG s'" by simp
           from this have eq_z: "z = Th th"
           proof -
             from step_back_step[OF vt_s[unfolded s_def]]
-            have "(Cs cs, Th th) \<in> depend s'"
-              by(cases, auto simp: wq_def s_depend_def cs_holding_def s_holding_def)
-            from unique_depend[OF step_back_vt[OF vt_s[unfolded s_def]] this dp_yz]
+            have "(Cs cs, Th th) \<in> RAG s'"
+              by(cases, auto simp: wq_def s_RAG_def cs_holding_def s_holding_def)
+            from unique_RAG[OF step_back_vt[OF vt_s[unfolded s_def]] this dp_yz]
             show ?thesis by simp
           qed
           from converse_tranclE[OF ztp]
-          obtain u where "(z, u) \<in> depend s'" by auto
+          obtain u where "(z, u) \<in> RAG s'" by auto
           moreover 
           from step_back_step[OF vt_s[unfolded s_def]]
           have "th \<in> readys s'" by (cases, simp add:runing_def)
           moreover note eq_z
           ultimately show False 
-            by (auto simp:readys_def wq_def s_depend_def s_waiting_def cs_waiting_def)
+            by (auto simp:readys_def wq_def s_RAG_def s_waiting_def cs_waiting_def)
         qed
       next
         show "y \<noteq> Th th'"
         proof
           assume eq_y: "y = Th th'"
-          with yz have dps: "(Th th', z) \<in> depend s'" by simp
+          with yz have dps: "(Th th', z) \<in> RAG s'" by simp
           have "z = Cs cs"
           proof -
             from next_waiting[OF step_back_vt[OF vt_s[unfolded s_def]] nt]
-            have "(Th th', Cs cs) \<in> depend s'"
-              by (auto simp:s_waiting_def wq_def s_depend_def cs_waiting_def)
-            from unique_depend[OF step_back_vt[OF vt_s[unfolded s_def]] dps this]
+            have "(Th th', Cs cs) \<in> RAG s'"
+              by (auto simp:s_waiting_def wq_def s_RAG_def cs_waiting_def)
+            from unique_RAG[OF step_back_vt[OF vt_s[unfolded s_def]] dps this]
             show ?thesis .
           qed
-          with ztp have cs_i: "(Cs cs, Th th'') \<in>  (depend s')\<^sup>+" by simp
+          with ztp have cs_i: "(Cs cs, Th th'') \<in>  (RAG s')\<^sup>+" by simp
           from step_back_step[OF vt_s[unfolded s_def]]
-          have cs_th: "(Cs cs, Th th) \<in> depend s'"
-            by(cases, auto simp: s_depend_def wq_def cs_holding_def s_holding_def)
-          have "(Cs cs, Th th'') \<notin>  depend s'"
+          have cs_th: "(Cs cs, Th th) \<in> RAG s'"
+            by(cases, auto simp: s_RAG_def wq_def cs_holding_def s_holding_def)
+          have "(Cs cs, Th th'') \<notin>  RAG s'"
           proof
-            assume "(Cs cs, Th th'') \<in> depend s'"
-            from unique_depend[OF step_back_vt[OF vt_s[unfolded s_def]] this cs_th]
+            assume "(Cs cs, Th th'') \<in> RAG s'"
+            from unique_RAG[OF step_back_vt[OF vt_s[unfolded s_def]] this cs_th]
             and neq1 show "False" by simp
           qed
           with converse_tranclE[OF cs_i]
-          obtain u where cu: "(Cs cs, u) \<in> depend s'"  
-            and u_t: "(u, Th th'') \<in> (depend s')\<^sup>+" by auto
+          obtain u where cu: "(Cs cs, u) \<in> RAG s'"  
+            and u_t: "(u, Th th'') \<in> (RAG s')\<^sup>+" by auto
           have "u = Th th"
           proof -
-            from unique_depend[OF step_back_vt[OF vt_s[unfolded s_def]] cu cs_th]
+            from unique_RAG[OF step_back_vt[OF vt_s[unfolded s_def]] cu cs_th]
             show ?thesis .
           qed
-          with u_t have "(Th th, Th th'') \<in> (depend s')\<^sup>+" by simp
+          with u_t have "(Th th, Th th'') \<in> (RAG s')\<^sup>+" by simp
           from converse_tranclE[OF this]
-          obtain v where "(Th th, v) \<in> (depend s')" by auto
+          obtain v where "(Th th, v) \<in> (RAG s')" by auto
           moreover from step_back_step[OF vt_s[unfolded s_def]]
           have "th \<in> readys s'" by (cases, simp add:runing_def)
           ultimately show False 
-            by (auto simp:readys_def wq_def s_depend_def s_waiting_def cs_waiting_def)
+            by (auto simp:readys_def wq_def s_RAG_def s_waiting_def cs_waiting_def)
         qed
       qed
-      with depend_s yz have "(y, z) \<in> depend s" by auto
+      with RAG_s yz have "(y, z) \<in> RAG s" by auto
       with ztp'
-      show "(y, Th th'') \<in> (depend s)\<^sup>+" by auto
+      show "(y, Th th'') \<in> (RAG s)\<^sup>+" by auto
     qed    
   }
   from this[OF dp]
   show "x \<in> dependants (wq s) th''"
-    by (auto simp:cs_dependants_def eq_depend)
+    by (auto simp:cs_dependants_def eq_RAG)
 qed
 
 lemma cp_kept:
@@ -1204,11 +1122,11 @@
 context step_v_cps_nnt
 begin
 
-lemma nw_cs: "(Th th1, Cs cs) \<notin> depend s'"
+lemma nw_cs: "(Th th1, Cs cs) \<notin> RAG s'"
 proof
-  assume "(Th th1, Cs cs) \<in> depend s'"
+  assume "(Th th1, Cs cs) \<in> RAG s'"
   thus "False"
-    apply (auto simp:s_depend_def cs_waiting_def)
+    apply (auto simp:s_RAG_def cs_waiting_def)
   proof -
     assume h1: "th1 \<in> set (wq s' cs)"
       and h2: "th1 \<noteq> hd (wq s' cs)"
@@ -1229,9 +1147,9 @@
   qed
 qed
 
-lemma depend_s: "depend s = depend s' - {(Cs cs, Th th)}"
+lemma RAG_s: "RAG s = RAG s' - {(Cs cs, Th th)}"
 proof -
-  from nnt and  step_depend_v[OF vt_s[unfolded s_def], folded s_def]
+  from nnt and  step_RAG_v[OF vt_s[unfolded s_def], folded s_def]
   show ?thesis by auto
 qed
 
@@ -1244,18 +1162,18 @@
   proof(induct rule: converse_trancl_induct)
     case (base y)
     from base obtain th1 cs1 th2
-      where h1: "(Th th1, Cs cs1) \<in> depend s'"
-      and h2: "(Cs cs1, Th th2) \<in> depend s'"
+      where h1: "(Th th1, Cs cs1) \<in> RAG s'"
+      and h2: "(Cs cs1, Th th2) \<in> RAG s'"
       and eq_y: "y = Th th1" and eq_n2: "n2 = Th th2"  by (auto simp:child_def)
     have "cs1 \<noteq> cs"
     proof
       assume eq_cs: "cs1 = cs"
-      with h1 have "(Th th1, Cs cs1) \<in> depend s'" by simp
+      with h1 have "(Th th1, Cs cs1) \<in> RAG s'" by simp
       with nw_cs eq_cs show False by auto
     qed
-    with h1 h2 depend_s have 
-      h1': "(Th th1, Cs cs1) \<in> depend s" and
-      h2': "(Cs cs1, Th th2) \<in> depend s" by auto
+    with h1 h2 RAG_s have 
+      h1': "(Th th1, Cs cs1) \<in> RAG s" and
+      h2': "(Cs cs1, Th th2) \<in> RAG s" by auto
     hence "(Th th1, Th th2) \<in> child s" by (auto simp:child_def)
     with eq_y eq_n2 have "(y, n2) \<in> child s" by simp
     thus ?case by auto
@@ -1263,18 +1181,18 @@
     case (step y z)
     have "(y, z) \<in> child s'" by fact
     then obtain th1 cs1 th2
-      where h1: "(Th th1, Cs cs1) \<in> depend s'"
-      and h2: "(Cs cs1, Th th2) \<in> depend s'"
+      where h1: "(Th th1, Cs cs1) \<in> RAG s'"
+      and h2: "(Cs cs1, Th th2) \<in> RAG s'"
       and eq_y: "y = Th th1" and eq_z: "z = Th th2"  by (auto simp:child_def)
     have "cs1 \<noteq> cs"
     proof
       assume eq_cs: "cs1 = cs"
-      with h1 have "(Th th1, Cs cs1) \<in> depend s'" by simp
+      with h1 have "(Th th1, Cs cs1) \<in> RAG s'" by simp
       with nw_cs eq_cs show False by auto
     qed
-    with h1 h2 depend_s have 
-      h1': "(Th th1, Cs cs1) \<in> depend s" and
-      h2': "(Cs cs1, Th th2) \<in> depend s" by auto
+    with h1 h2 RAG_s have 
+      h1': "(Th th1, Cs cs1) \<in> RAG s" and
+      h2': "(Cs cs1, Th th2) \<in> RAG s" by auto
     hence "(Th th1, Th th2) \<in> child s" by (auto simp:child_def)
     with eq_y eq_z have "(y, z) \<in> child s" by simp
     moreover have "(z, n2) \<in> (child s)^+" by fact
@@ -1290,14 +1208,14 @@
   from assms show ?thesis
   proof(induct)
     case (base y)
-    from base and depend_s 
+    from base and RAG_s 
     have "(n1, y) \<in> child s'"
       by (auto simp:child_def)
     thus ?case by auto
   next
     case (step y z)
     have "(y, z) \<in> child s" by fact
-    with depend_s have "(y, z) \<in> child s'"
+    with RAG_s have "(y, z) \<in> child s'"
       by (auto simp:child_def)
     moreover have "(n1, y) \<in> (child s')\<^sup>+" by fact
     ultimately show ?case by auto
@@ -1313,13 +1231,13 @@
   apply (unfold cp_eq_cpreced cpreced_def)
 proof -
   have eq_dp: "\<And> th. dependants (wq s) th = dependants (wq s') th"
-    apply (unfold cs_dependants_def, unfold eq_depend)
+    apply (unfold cs_dependants_def, unfold eq_RAG)
   proof -
     from eq_child
     have "\<And>th. {th'. (Th th', Th th) \<in> (child s)\<^sup>+} = {th'. (Th th', Th th) \<in> (child s')\<^sup>+}"
       by simp
-    with child_depend_eq[OF vt_s] child_depend_eq[OF step_back_vt[OF vt_s[unfolded s_def]]]
-    show "\<And>th. {th'. (Th th', Th th) \<in> (depend s)\<^sup>+} = {th'. (Th th', Th th) \<in> (depend s')\<^sup>+}"
+    with child_RAG_eq[OF vt_s] child_RAG_eq[OF step_back_vt[OF vt_s[unfolded s_def]]]
+    show "\<And>th. {th'. (Th th', Th th) \<in> (RAG s)\<^sup>+} = {th'. (Th th', Th th) \<in> (RAG s')\<^sup>+}"
       by simp
   qed
   moreover {
@@ -1357,9 +1275,9 @@
 context step_P_cps_e
 begin
 
-lemma depend_s: "depend s = depend s' \<union> {(Cs cs, Th th)}"
+lemma RAG_s: "RAG s = RAG s' \<union> {(Cs cs, Th th)}"
 proof -
-  from ee and  step_depend_p[OF vt_s[unfolded s_def], folded s_def]
+  from ee and  step_RAG_p[OF vt_s[unfolded s_def], folded s_def]
   show ?thesis by auto
 qed
 
@@ -1372,19 +1290,19 @@
   proof(induct rule: converse_trancl_induct)
     case (base y)
     from base obtain th1 cs1 th2
-      where h1: "(Th th1, Cs cs1) \<in> depend s'"
-      and h2: "(Cs cs1, Th th2) \<in> depend s'"
+      where h1: "(Th th1, Cs cs1) \<in> RAG s'"
+      and h2: "(Cs cs1, Th th2) \<in> RAG s'"
       and eq_y: "y = Th th1" and eq_n2: "n2 = Th th2"  by (auto simp:child_def)
     have "cs1 \<noteq> cs"
     proof
       assume eq_cs: "cs1 = cs"
-      with h1 have "(Th th1, Cs cs) \<in> depend s'" by simp
+      with h1 have "(Th th1, Cs cs) \<in> RAG s'" by simp
       with ee show False
-        by (auto simp:s_depend_def cs_waiting_def)
+        by (auto simp:s_RAG_def cs_waiting_def)
     qed
-    with h1 h2 depend_s have 
-      h1': "(Th th1, Cs cs1) \<in> depend s" and
-      h2': "(Cs cs1, Th th2) \<in> depend s" by auto
+    with h1 h2 RAG_s have 
+      h1': "(Th th1, Cs cs1) \<in> RAG s" and
+      h2': "(Cs cs1, Th th2) \<in> RAG s" by auto
     hence "(Th th1, Th th2) \<in> child s" by (auto simp:child_def)
     with eq_y eq_n2 have "(y, n2) \<in> child s" by simp
     thus ?case by auto
@@ -1392,19 +1310,19 @@
     case (step y z)
     have "(y, z) \<in> child s'" by fact
     then obtain th1 cs1 th2
-      where h1: "(Th th1, Cs cs1) \<in> depend s'"
-      and h2: "(Cs cs1, Th th2) \<in> depend s'"
+      where h1: "(Th th1, Cs cs1) \<in> RAG s'"
+      and h2: "(Cs cs1, Th th2) \<in> RAG s'"
       and eq_y: "y = Th th1" and eq_z: "z = Th th2"  by (auto simp:child_def)
     have "cs1 \<noteq> cs"
     proof
       assume eq_cs: "cs1 = cs"
-      with h1 have "(Th th1, Cs cs) \<in> depend s'" by simp
+      with h1 have "(Th th1, Cs cs) \<in> RAG s'" by simp
       with ee show False 
-        by (auto simp:s_depend_def cs_waiting_def)
+        by (auto simp:s_RAG_def cs_waiting_def)
     qed
-    with h1 h2 depend_s have 
-      h1': "(Th th1, Cs cs1) \<in> depend s" and
-      h2': "(Cs cs1, Th th2) \<in> depend s" by auto
+    with h1 h2 RAG_s have 
+      h1': "(Th th1, Cs cs1) \<in> RAG s" and
+      h2': "(Cs cs1, Th th2) \<in> RAG s" by auto
     hence "(Th th1, Th th2) \<in> child s" by (auto simp:child_def)
     with eq_y eq_z have "(y, z) \<in> child s" by simp
     moreover have "(z, n2) \<in> (child s)^+" by fact
@@ -1420,28 +1338,28 @@
   from assms show ?thesis
   proof(induct)
     case (base y)
-    from base and depend_s
+    from base and RAG_s
     have "(n1, y) \<in> child s'"
       apply (auto simp:child_def)
       proof -
         fix th'
-        assume "(Th th', Cs cs) \<in> depend s'"
+        assume "(Th th', Cs cs) \<in> RAG s'"
         with ee have "False"
-          by (auto simp:s_depend_def cs_waiting_def)
-        thus "\<exists>cs. (Th th', Cs cs) \<in> depend s' \<and> (Cs cs, Th th) \<in> depend s'" by auto 
+          by (auto simp:s_RAG_def cs_waiting_def)
+        thus "\<exists>cs. (Th th', Cs cs) \<in> RAG s' \<and> (Cs cs, Th th) \<in> RAG s'" by auto 
       qed
     thus ?case by auto
   next
     case (step y z)
     have "(y, z) \<in> child s" by fact
-    with depend_s have "(y, z) \<in> child s'"
+    with RAG_s have "(y, z) \<in> child s'"
       apply (auto simp:child_def)
       proof -
         fix th'
-        assume "(Th th', Cs cs) \<in> depend s'"
+        assume "(Th th', Cs cs) \<in> RAG s'"
         with ee have "False"
-          by (auto simp:s_depend_def cs_waiting_def)
-        thus "\<exists>cs. (Th th', Cs cs) \<in> depend s' \<and> (Cs cs, Th th) \<in> depend s'" by auto 
+          by (auto simp:s_RAG_def cs_waiting_def)
+        thus "\<exists>cs. (Th th', Cs cs) \<in> RAG s' \<and> (Cs cs, Th th) \<in> RAG s'" by auto 
       qed
     moreover have "(n1, y) \<in> (child s')\<^sup>+" by fact
     ultimately show ?case by auto
@@ -1457,13 +1375,13 @@
   apply (unfold cp_eq_cpreced cpreced_def)
 proof -
   have eq_dp: "\<And> th. dependants (wq s) th = dependants (wq s') th"
-    apply (unfold cs_dependants_def, unfold eq_depend)
+    apply (unfold cs_dependants_def, unfold eq_RAG)
   proof -
     from eq_child
     have "\<And>th. {th'. (Th th', Th th) \<in> (child s)\<^sup>+} = {th'. (Th th', Th th) \<in> (child s')\<^sup>+}"
       by auto
-    with child_depend_eq[OF vt_s] child_depend_eq[OF step_back_vt[OF vt_s[unfolded s_def]]]
-    show "\<And>th. {th'. (Th th', Th th) \<in> (depend s)\<^sup>+} = {th'. (Th th', Th th) \<in> (depend s')\<^sup>+}"
+    with child_RAG_eq[OF vt_s] child_RAG_eq[OF step_back_vt[OF vt_s[unfolded s_def]]]
+    show "\<And>th. {th'. (Th th', Th th) \<in> (RAG s)\<^sup>+} = {th'. (Th th', Th th) \<in> (RAG s')\<^sup>+}"
       by simp
   qed
   moreover {
@@ -1490,9 +1408,9 @@
 context step_P_cps_ne
 begin
 
-lemma depend_s: "depend s = depend s' \<union> {(Th th, Cs cs)}"
+lemma RAG_s: "RAG s = RAG s' \<union> {(Th th, Cs cs)}"
 proof -
-  from step_depend_p[OF vt_s[unfolded s_def]] and ne
+  from step_RAG_p[OF vt_s[unfolded s_def]] and ne
   show ?thesis by (simp add:s_def)
 qed
 
@@ -1502,8 +1420,8 @@
 proof(induct rule:converse_trancl_induct)
   case (base y)
   from base obtain th1 cs1
-    where h1: "(Th th1, Cs cs1) \<in> depend s"
-    and h2: "(Cs cs1, Th th') \<in> depend s"
+    where h1: "(Th th1, Cs cs1) \<in> RAG s"
+    and h2: "(Cs cs1, Th th') \<in> RAG s"
     and eq_y: "y = Th th1"   by (auto simp:child_def)
   have "th1 \<noteq> th"
   proof
@@ -1511,16 +1429,16 @@
     with base eq_y have "(Th th, Th th') \<in> child s" by simp
     with nd show False by auto
   qed
-  with h1 h2 depend_s 
-  have h1': "(Th th1, Cs cs1) \<in> depend s'" and 
-       h2': "(Cs cs1, Th th') \<in> depend s'" by auto
+  with h1 h2 RAG_s 
+  have h1': "(Th th1, Cs cs1) \<in> RAG s'" and 
+       h2': "(Cs cs1, Th th') \<in> RAG s'" by auto
   with eq_y show ?case by (auto simp:child_def)
 next
   case (step y z)
   have yz: "(y, z) \<in> child s" by fact
   then obtain th1 cs1 th2
-    where h1: "(Th th1, Cs cs1) \<in> depend s"
-    and h2: "(Cs cs1, Th th2) \<in> depend s"
+    where h1: "(Th th1, Cs cs1) \<in> RAG s"
+    and h2: "(Cs cs1, Th th2) \<in> RAG s"
     and eq_y: "y = Th th1" and eq_z: "z = Th th2"  by (auto simp:child_def)
   have "th1 \<noteq> th"
   proof
@@ -1530,8 +1448,8 @@
     ultimately have "(Th th, Th th') \<in> (child s)^+" by auto
     with nd show False by auto
   qed
-  with h1 h2 depend_s have h1': "(Th th1, Cs cs1) \<in> depend s'"
-                       and h2': "(Cs cs1, Th th2) \<in> depend s'" by auto
+  with h1 h2 RAG_s have h1': "(Th th1, Cs cs1) \<in> RAG s'"
+                       and h2': "(Cs cs1, Th th2) \<in> RAG s'" by auto
   with eq_y eq_z have "(y, z) \<in> child s'" by (auto simp:child_def)
   moreover have "(z, Th th') \<in> (child s')^+" by fact
   ultimately show ?case by auto
@@ -1541,11 +1459,11 @@
   shows "(n1, Th th') \<in> (child s')^+ \<Longrightarrow> (n1, Th th') \<in> (child s)^+"
 proof(induct rule:converse_trancl_induct)
   case (base y)
-  with depend_s show ?case by (auto simp:child_def)
+  with RAG_s show ?case by (auto simp:child_def)
 next
   case (step y z)
   have "(y, z) \<in> child s'" by fact
-  with depend_s have "(y, z) \<in> child s" by (auto simp:child_def)
+  with RAG_s have "(y, z) \<in> child s" by (auto simp:child_def)
   moreover have "(z, Th th') \<in> (child s)^+" by fact
   ultimately show ?case by auto
 qed
@@ -1564,34 +1482,34 @@
   have nd': "(Th th, Th th') \<notin> (child s)^+"
   proof
     assume "(Th th, Th th') \<in> (child s)\<^sup>+"
-    with child_depend_eq[OF vt_s]
-    have "(Th th, Th th') \<in> (depend s)\<^sup>+" by simp
+    with child_RAG_eq[OF vt_s]
+    have "(Th th, Th th') \<in> (RAG s)\<^sup>+" by simp
     with nd show False 
-      by (simp add:s_dependants_def eq_depend)
+      by (simp add:s_dependants_def eq_RAG)
   qed
   have eq_dp: "dependants (wq s) th' = dependants (wq s') th'"
   proof(auto)
     fix x assume " x \<in> dependants (wq s) th'"
     thus "x \<in> dependants (wq s') th'"
-      apply (auto simp:cs_dependants_def eq_depend)
+      apply (auto simp:cs_dependants_def eq_RAG)
     proof -
-      assume "(Th x, Th th') \<in> (depend s)\<^sup>+"
-      with  child_depend_eq[OF vt_s] have "(Th x, Th th') \<in> (child s)\<^sup>+" by simp
+      assume "(Th x, Th th') \<in> (RAG s)\<^sup>+"
+      with  child_RAG_eq[OF vt_s] have "(Th x, Th th') \<in> (child s)\<^sup>+" by simp
       with eq_child[OF nd'] have "(Th x, Th th') \<in> (child s')^+" by simp
-      with child_depend_eq[OF step_back_vt[OF vt_s[unfolded s_def]]]
-      show "(Th x, Th th') \<in> (depend s')\<^sup>+" by simp
+      with child_RAG_eq[OF step_back_vt[OF vt_s[unfolded s_def]]]
+      show "(Th x, Th th') \<in> (RAG s')\<^sup>+" by simp
     qed
   next
     fix x assume "x \<in> dependants (wq s') th'"
     thus "x \<in> dependants (wq s) th'"
-      apply (auto simp:cs_dependants_def eq_depend)
+      apply (auto simp:cs_dependants_def eq_RAG)
     proof -
-      assume "(Th x, Th th') \<in> (depend s')\<^sup>+"
-      with child_depend_eq[OF step_back_vt[OF vt_s[unfolded s_def]]] 
+      assume "(Th x, Th th') \<in> (RAG s')\<^sup>+"
+      with child_RAG_eq[OF step_back_vt[OF vt_s[unfolded s_def]]] 
       have "(Th x, Th th') \<in> (child s')\<^sup>+" by simp
       with eq_child[OF nd'] have "(Th x, Th th') \<in> (child s)^+" by simp
-      with  child_depend_eq[OF vt_s]
-      show "(Th x, Th th') \<in> (depend s)\<^sup>+" by simp
+      with  child_RAG_eq[OF vt_s]
+      show "(Th x, Th th') \<in> (RAG s)\<^sup>+" by simp
     qed
   qed
   moreover {
@@ -1611,8 +1529,8 @@
   shows "cp s th'' = cp s' th''"
 proof -
   from dp2
-  have "(Th th', Th th'') \<in> (depend (wq s))\<^sup>+" by (simp add:s_dependants_def)
-  from depend_child[OF vt_s this[unfolded eq_depend]]
+  have "(Th th', Th th'') \<in> (RAG (wq s))\<^sup>+" by (simp add:s_dependants_def)
+  from RAG_child[OF vt_s this[unfolded eq_RAG]]
   have ch_th': "(Th th', Th th'') \<in> (child s)\<^sup>+" .
   moreover {
     fix n th''
@@ -1625,10 +1543,10 @@
         and ch': "(Th th', y) \<in> (child s)\<^sup>+"
       from y_ch obtain thy where eq_y: "y = Th thy" by (auto simp:child_def)
       with ih have eq_cpy:"cp s thy = cp s' thy" by blast
-      from dp1 have "(Th th, Th th') \<in> (depend s)^+" by (auto simp:s_dependants_def eq_depend)
-      moreover from child_depend_p[OF ch'] and eq_y
-      have "(Th th', Th thy) \<in> (depend s)^+" by simp
-      ultimately have dp_thy: "(Th th, Th thy) \<in> (depend s)^+" by auto
+      from dp1 have "(Th th, Th th') \<in> (RAG s)^+" by (auto simp:s_dependants_def eq_RAG)
+      moreover from child_RAG_p[OF ch'] and eq_y
+      have "(Th th', Th thy) \<in> (RAG s)^+" by simp
+      ultimately have dp_thy: "(Th th, Th thy) \<in> (RAG s)^+" by auto
       show "cp s th'' = cp s' th''"
         apply (subst cp_rec[OF vt_s])
       proof -
@@ -1646,14 +1564,14 @@
             have neq_th1: "th1 \<noteq> th"
             proof
               assume eq_th1: "th1 = th"
-              with dp_thy have "(Th th1, Th thy) \<in> (depend s)^+" by simp
+              with dp_thy have "(Th th1, Th thy) \<in> (RAG s)^+" by simp
               from children_no_dep[OF vt_s _ _ this] and 
               th1_in y_ch eq_y show False by (auto simp:children_def)
             qed
             have "th \<notin> dependants s th1"
             proof
               assume h:"th \<in> dependants s th1"
-              from eq_y dp_thy have "th \<in> dependants s thy" by (auto simp:s_dependants_def eq_depend)
+              from eq_y dp_thy have "th \<in> dependants s thy" by (auto simp:s_dependants_def eq_RAG)
               from dependants_child_unique[OF vt_s _ _ h this]
               th1_in y_ch eq_y have "th1 = thy" by (auto simp:children_def child_def)
               with False show False by auto
@@ -1665,48 +1583,48 @@
         ultimately have "{preced th'' s} \<union> (cp s ` children s th'') = 
           {preced th'' s'} \<union> (cp s' ` children s th'')" by (auto simp:image_def)
         moreover have "children s th'' = children s' th''"
-          apply (unfold children_def child_def s_def depend_set_unchanged, simp)
-          apply (fold s_def, auto simp:depend_s)
+          apply (unfold children_def child_def s_def RAG_set_unchanged, simp)
+          apply (fold s_def, auto simp:RAG_s)
           proof -
-            assume "(Cs cs, Th th'') \<in> depend s'"
-            with depend_s have cs_th': "(Cs cs, Th th'') \<in> depend s" by auto
-            from dp1 have "(Th th, Th th') \<in> (depend s)^+"
-              by (auto simp:s_dependants_def eq_depend)
+            assume "(Cs cs, Th th'') \<in> RAG s'"
+            with RAG_s have cs_th': "(Cs cs, Th th'') \<in> RAG s" by auto
+            from dp1 have "(Th th, Th th') \<in> (RAG s)^+"
+              by (auto simp:s_dependants_def eq_RAG)
             from converse_tranclE[OF this]
-            obtain cs1 where h1: "(Th th, Cs cs1) \<in> depend s"
-              and h2: "(Cs cs1 , Th th') \<in> (depend s)\<^sup>+"
-              by (auto simp:s_depend_def)
+            obtain cs1 where h1: "(Th th, Cs cs1) \<in> RAG s"
+              and h2: "(Cs cs1 , Th th') \<in> (RAG s)\<^sup>+"
+              by (auto simp:s_RAG_def)
             have eq_cs: "cs1 = cs" 
             proof -
-              from depend_s have "(Th th, Cs cs) \<in> depend s" by simp
-              from unique_depend[OF vt_s this h1]
+              from RAG_s have "(Th th, Cs cs) \<in> RAG s" by simp
+              from unique_RAG[OF vt_s this h1]
               show ?thesis by simp
             qed
             have False
             proof(rule converse_tranclE[OF h2])
-              assume "(Cs cs1, Th th') \<in> depend s"
-              with eq_cs have "(Cs cs, Th th') \<in> depend s" by simp
-              from unique_depend[OF vt_s this cs_th']
+              assume "(Cs cs1, Th th') \<in> RAG s"
+              with eq_cs have "(Cs cs, Th th') \<in> RAG s" by simp
+              from unique_RAG[OF vt_s this cs_th']
               have "th' = th''" by simp
               with ch' y_ch have "(Th th'', Th th'') \<in> (child s)^+" by auto
               with wf_trancl[OF wf_child[OF vt_s]] 
               show False by auto
             next
               fix y
-              assume "(Cs cs1, y) \<in> depend s"
-                and ytd: " (y, Th th') \<in> (depend s)\<^sup>+"
-              with eq_cs have csy: "(Cs cs, y) \<in> depend s" by simp
-              from unique_depend[OF vt_s this cs_th']
+              assume "(Cs cs1, y) \<in> RAG s"
+                and ytd: " (y, Th th') \<in> (RAG s)\<^sup>+"
+              with eq_cs have csy: "(Cs cs, y) \<in> RAG s" by simp
+              from unique_RAG[OF vt_s this cs_th']
               have "y = Th th''" .
-              with ytd have "(Th th'', Th th') \<in> (depend s)^+" by simp
-              from depend_child[OF vt_s this]
+              with ytd have "(Th th'', Th th') \<in> (RAG s)^+" by simp
+              from RAG_child[OF vt_s this]
               have "(Th th'', Th th') \<in> (child s)\<^sup>+" .
               moreover from ch' y_ch have ch'': "(Th th', Th th'') \<in> (child s)^+" by auto
               ultimately have "(Th th'', Th th'') \<in> (child s)^+" by auto 
               with wf_trancl[OF wf_child[OF vt_s]] 
               show False by auto
             qed
-            thus "\<exists>cs. (Th th, Cs cs) \<in> depend s' \<and> (Cs cs, Th th'') \<in> depend s'" by auto
+            thus "\<exists>cs. (Th th, Cs cs) \<in> RAG s' \<and> (Cs cs, Th th'') \<in> RAG s'" by auto
           qed
           ultimately show "Max ({preced th'' s} \<union> cp s ` children s th'') = cp s' th''"
           by (simp add:cp_rec[OF step_back_vt[OF vt_s[unfolded s_def]]])
@@ -1731,8 +1649,8 @@
             have neq_th1: "th1 \<noteq> th"
             proof
               assume eq_th1: "th1 = th"
-              with dp1 have "(Th th1, Th th') \<in> (depend s)^+" 
-                by (auto simp:s_dependants_def eq_depend)
+              with dp1 have "(Th th1, Th th') \<in> (RAG s)^+" 
+                by (auto simp:s_dependants_def eq_RAG)
               from children_no_dep[OF vt_s _ _ this]
               th1_in dp'
               show False by (auto simp:children_def)
@@ -1753,48 +1671,48 @@
         ultimately have "{preced th'' s} \<union> (cp s ` children s th'') = 
           {preced th'' s'} \<union> (cp s' ` children s th'')" by (auto simp:image_def)
         moreover have "children s th'' = children s' th''"
-          apply (unfold children_def child_def s_def depend_set_unchanged, simp)
-          apply (fold s_def, auto simp:depend_s)
+          apply (unfold children_def child_def s_def RAG_set_unchanged, simp)
+          apply (fold s_def, auto simp:RAG_s)
           proof -
-            assume "(Cs cs, Th th'') \<in> depend s'"
-            with depend_s have cs_th': "(Cs cs, Th th'') \<in> depend s" by auto
-            from dp1 have "(Th th, Th th') \<in> (depend s)^+"
-              by (auto simp:s_dependants_def eq_depend)
+            assume "(Cs cs, Th th'') \<in> RAG s'"
+            with RAG_s have cs_th': "(Cs cs, Th th'') \<in> RAG s" by auto
+            from dp1 have "(Th th, Th th') \<in> (RAG s)^+"
+              by (auto simp:s_dependants_def eq_RAG)
             from converse_tranclE[OF this]
-            obtain cs1 where h1: "(Th th, Cs cs1) \<in> depend s"
-              and h2: "(Cs cs1 , Th th') \<in> (depend s)\<^sup>+"
-              by (auto simp:s_depend_def)
+            obtain cs1 where h1: "(Th th, Cs cs1) \<in> RAG s"
+              and h2: "(Cs cs1 , Th th') \<in> (RAG s)\<^sup>+"
+              by (auto simp:s_RAG_def)
             have eq_cs: "cs1 = cs" 
             proof -
-              from depend_s have "(Th th, Cs cs) \<in> depend s" by simp
-              from unique_depend[OF vt_s this h1]
+              from RAG_s have "(Th th, Cs cs) \<in> RAG s" by simp
+              from unique_RAG[OF vt_s this h1]
               show ?thesis by simp
             qed
             have False
             proof(rule converse_tranclE[OF h2])
-              assume "(Cs cs1, Th th') \<in> depend s"
-              with eq_cs have "(Cs cs, Th th') \<in> depend s" by simp
-              from unique_depend[OF vt_s this cs_th']
+              assume "(Cs cs1, Th th') \<in> RAG s"
+              with eq_cs have "(Cs cs, Th th') \<in> RAG s" by simp
+              from unique_RAG[OF vt_s this cs_th']
               have "th' = th''" by simp
               with dp' have "(Th th'', Th th'') \<in> (child s)^+" by auto
               with wf_trancl[OF wf_child[OF vt_s]] 
               show False by auto
             next
               fix y
-              assume "(Cs cs1, y) \<in> depend s"
-                and ytd: " (y, Th th') \<in> (depend s)\<^sup>+"
-              with eq_cs have csy: "(Cs cs, y) \<in> depend s" by simp
-              from unique_depend[OF vt_s this cs_th']
+              assume "(Cs cs1, y) \<in> RAG s"
+                and ytd: " (y, Th th') \<in> (RAG s)\<^sup>+"
+              with eq_cs have csy: "(Cs cs, y) \<in> RAG s" by simp
+              from unique_RAG[OF vt_s this cs_th']
               have "y = Th th''" .
-              with ytd have "(Th th'', Th th') \<in> (depend s)^+" by simp
-              from depend_child[OF vt_s this]
+              with ytd have "(Th th'', Th th') \<in> (RAG s)^+" by simp
+              from RAG_child[OF vt_s this]
               have "(Th th'', Th th') \<in> (child s)\<^sup>+" .
               moreover from dp' have ch'': "(Th th', Th th'') \<in> (child s)^+" by auto
               ultimately have "(Th th'', Th th'') \<in> (child s)^+" by auto 
               with wf_trancl[OF wf_child[OF vt_s]] 
               show False by auto
             qed
-            thus "\<exists>cs. (Th th, Cs cs) \<in> depend s' \<and> (Cs cs, Th th'') \<in> depend s'" by auto
+            thus "\<exists>cs. (Th th, Cs cs) \<in> RAG s' \<and> (Cs cs, Th th'') \<in> RAG s'" by auto
           qed
         ultimately show "Max ({preced th'' s} \<union> cp s ` children s th'') = cp s' th''"
           by (simp add:cp_rec[OF step_back_vt[OF vt_s[unfolded s_def]]])
@@ -1814,8 +1732,8 @@
 context step_create_cps
 begin
 
-lemma eq_dep: "depend s = depend s'"
-  by (unfold s_def depend_create_unchanged, auto)
+lemma eq_dep: "RAG s = RAG s'"
+  by (unfold s_def RAG_create_unchanged, auto)
 
 lemma eq_cp:
   fixes th' 
@@ -1826,11 +1744,11 @@
   have nd: "th \<notin> dependants s th'"
   proof
     assume "th \<in> dependants s th'"
-    hence "(Th th, Th th') \<in> (depend s)^+" by (simp add:s_dependants_def eq_depend)
-    with eq_dep have "(Th th, Th th') \<in> (depend s')^+" by simp
+    hence "(Th th, Th th') \<in> (RAG s)^+" by (simp add:s_dependants_def eq_RAG)
+    with eq_dep have "(Th th, Th th') \<in> (RAG s')^+" by simp
     from converse_tranclE[OF this]
-    obtain y where "(Th th, y) \<in> depend s'" by auto
-    with dm_depend_threads[OF step_back_vt[OF vt_s[unfolded s_def]]]
+    obtain y where "(Th th, y) \<in> RAG s'" by auto
+    with dm_RAG_threads[OF step_back_vt[OF vt_s[unfolded s_def]]]
     have in_th: "th \<in> threads s'" by auto
     from step_back_step[OF vt_s[unfolded s_def]]
     show False
@@ -1840,7 +1758,7 @@
     qed
   qed
   have eq_dp: "\<And> th. dependants (wq s) th = dependants (wq s') th"
-    by (unfold cs_dependants_def, auto simp:eq_dep eq_depend)
+    by (unfold cs_dependants_def, auto simp:eq_dep eq_RAG)
   moreover {
     fix th1 
     assume "th1 \<in> {th'} \<union> dependants (wq s') th'"
@@ -1853,7 +1771,7 @@
     next
       assume "th1 \<in> dependants (wq s') th'"
       with nd and eq_dp have "th1 \<noteq> th"
-        by (auto simp:eq_depend cs_dependants_def s_dependants_def eq_dep)
+        by (auto simp:eq_RAG cs_dependants_def s_dependants_def eq_dep)
       thus "preced th1 s = preced th1 s'" by (auto simp:s_def preced_def)
     qed
   } ultimately have "((\<lambda>th. preced th s) ` ({th'} \<union> dependants (wq s) th')) = 
@@ -1874,16 +1792,16 @@
     have "dependants s' th = {}"
     proof -
       { assume "dependants s' th \<noteq> {}"
-        then obtain th' where dp: "(Th th', Th th) \<in> (depend s')^+"
-          by (auto simp:s_dependants_def eq_depend)
+        then obtain th' where dp: "(Th th', Th th) \<in> (RAG s')^+"
+          by (auto simp:s_dependants_def eq_RAG)
         from tranclE[OF this] obtain cs' where 
-          "(Cs cs', Th th) \<in> depend s'" by (auto simp:s_depend_def)
+          "(Cs cs', Th th) \<in> RAG s'" by (auto simp:s_RAG_def)
         with hdn
         have False by (auto simp:holdents_test)
       } thus ?thesis by auto
     qed
     thus ?thesis 
-      by (unfold s_def s_dependants_def eq_depend depend_create_unchanged, simp)
+      by (unfold s_def s_dependants_def eq_RAG RAG_create_unchanged, simp)
   qed
 qed
 
@@ -1902,8 +1820,8 @@
 context step_exit_cps
 begin
 
-lemma eq_dep: "depend s = depend s'"
-  by (unfold s_def depend_exit_unchanged, auto)
+lemma eq_dep: "RAG s = RAG s'"
+  by (unfold s_def RAG_exit_unchanged, auto)
 
 lemma eq_cp:
   fixes th' 
@@ -1914,22 +1832,22 @@
   have nd: "th \<notin> dependants s th'"
   proof
     assume "th \<in> dependants s th'"
-    hence "(Th th, Th th') \<in> (depend s)^+" by (simp add:s_dependants_def eq_depend)
-    with eq_dep have "(Th th, Th th') \<in> (depend s')^+" by simp
+    hence "(Th th, Th th') \<in> (RAG s)^+" by (simp add:s_dependants_def eq_RAG)
+    with eq_dep have "(Th th, Th th') \<in> (RAG s')^+" by simp
     from converse_tranclE[OF this]
-    obtain cs' where bk: "(Th th, Cs cs') \<in> depend s'"
-      by (auto simp:s_depend_def)
+    obtain cs' where bk: "(Th th, Cs cs') \<in> RAG s'"
+      by (auto simp:s_RAG_def)
     from step_back_step[OF vt_s[unfolded s_def]]
     show False
     proof(cases)
       assume "th \<in> runing s'"
       with bk show ?thesis
-        apply (unfold runing_def readys_def s_waiting_def s_depend_def)
+        apply (unfold runing_def readys_def s_waiting_def s_RAG_def)
         by (auto simp:cs_waiting_def wq_def)
     qed
   qed
   have eq_dp: "\<And> th. dependants (wq s) th = dependants (wq s') th"
-    by (unfold cs_dependants_def, auto simp:eq_dep eq_depend)
+    by (unfold cs_dependants_def, auto simp:eq_dep eq_RAG)
   moreover {
     fix th1 
     assume "th1 \<in> {th'} \<union> dependants (wq s') th'"
@@ -1942,7 +1860,7 @@
     next
       assume "th1 \<in> dependants (wq s') th'"
       with nd and eq_dp have "th1 \<noteq> th"
-        by (auto simp:eq_depend cs_dependants_def s_dependants_def eq_dep)
+        by (auto simp:eq_RAG cs_dependants_def s_dependants_def eq_dep)
       thus "preced th1 s = preced th1 s'" by (auto simp:s_def preced_def)
     qed
   } ultimately have "((\<lambda>th. preced th s) ` ({th'} \<union> dependants (wq s) th')) =