diff -r 12e9aa68d5db -r 4190df6f4488 prio/CpsG.thy
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/prio/CpsG.thy	Tue Jan 24 00:20:09 2012 +0000
@@ -0,0 +1,1826 @@
+theory CpsG
+imports PrioG 
+begin
+
+lemma not_thread_holdents:
+  fixes th s
+  assumes vt: "vt step s"
+  and not_in: "th \<notin> threads s" 
+  shows "holdents s th = {}"
+proof -
+  from vt not_in show ?thesis
+  proof(induct arbitrary:th)
+    case (vt_cons s e th)
+    assume vt: "vt step s"
+      and ih: "\<And>th. th \<notin> threads s \<Longrightarrow> holdents s th = {}"
+      and stp: "step s e"
+      and not_in: "th \<notin> threads (e # s)"
+    from stp show ?case
+    proof(cases)
+      case (thread_create thread prio)
+      assume eq_e: "e = Create thread prio"
+        and not_in': "thread \<notin> threads s"
+      have "holdents (e # s) th = holdents s th"
+        apply (unfold eq_e holdents_def)
+        by (simp add:depend_create_unchanged)
+      moreover have "th \<notin> threads s" 
+      proof -
+        from not_in eq_e show ?thesis by simp
+      qed
+      moreover note ih ultimately show ?thesis by auto
+    next
+      case (thread_exit thread)
+      assume eq_e: "e = Exit thread"
+      and nh: "holdents s thread = {}"
+      show ?thesis
+      proof(cases "th = thread")
+        case True
+        with nh eq_e
+        show ?thesis 
+          by (auto simp:holdents_def depend_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_def depend_exit_unchanged)
+      qed
+    next
+      case (thread_P thread cs)
+      assume eq_e: "e = P thread cs"
+      and is_runing: "thread \<in> runing s"
+      from prems have vtp: "vt step (P thread cs#s)" by auto
+      have neq_th: "th \<noteq> thread" 
+      proof -
+        from not_in eq_e have "th \<notin> threads s" by simp
+        moreover from is_runing have "thread \<in> threads s"
+          by (simp add:runing_def readys_def)
+        ultimately show ?thesis by auto
+      qed
+      hence "holdents (e # s) th  = holdents s th "
+        apply (unfold cntCS_def holdents_def eq_e)
+        by (unfold step_depend_p[OF vtp], auto)
+      moreover have "holdents s th = {}"
+      proof(rule ih)
+        from not_in eq_e show "th \<notin> threads s" by simp
+      qed
+      ultimately show ?thesis by simp
+    next
+      case (thread_V thread cs)
+      assume eq_e: "e = V thread cs"
+        and is_runing: "thread \<in> runing s"
+        and hold: "holding s thread cs"
+      have neq_th: "th \<noteq> thread" 
+      proof -
+        from not_in eq_e have "th \<notin> threads s" by simp
+        moreover from is_runing have "thread \<in> threads s"
+          by (simp add:runing_def readys_def)
+        ultimately show ?thesis by auto
+      qed
+      from prems have vtv: "vt step (V thread cs#s)" by auto
+      from hold obtain rest 
+        where eq_wq: "wq s cs = thread # rest"
+        by (case_tac "wq s cs", auto simp:s_holding_def)
+      from not_in eq_e eq_wq
+      have "\<not> next_th s thread cs th"
+        apply (auto simp:next_th_def)
+      proof -
+        assume ne: "rest \<noteq> []"
+          and ni: "hd (SOME q. distinct q \<and> set q = set rest) \<notin> threads s" (is "?t \<notin> threads s")
+        have "?t \<in> set rest"
+        proof(rule someI2)
+          from wq_distinct[OF step_back_vt[OF vtv], of cs] and eq_wq
+          show "distinct rest \<and> set rest = set rest" by auto
+        next
+          fix x assume "distinct x \<and> set x = set rest" with ne
+          show "hd x \<in> set rest" by (cases x, auto)
+        qed
+        with eq_wq have "?t \<in> set (wq s cs)" by simp
+        from wq_threads[OF step_back_vt[OF vtv], OF this] and ni
+        show False by auto
+      qed
+      moreover note neq_th eq_wq
+      ultimately have "holdents (e # s) th  = holdents s th"
+        by (unfold eq_e cntCS_def holdents_def step_depend_v[OF vtv], auto)
+      moreover have "holdents s th = {}"
+      proof(rule ih)
+        from not_in eq_e show "th \<notin> threads s" by simp
+      qed
+      ultimately show ?thesis by simp
+    next
+      case (thread_set thread prio)
+      print_facts
+      assume eq_e: "e = Set thread prio"
+        and is_runing: "thread \<in> runing s"
+      from not_in and eq_e have "th \<notin> threads s" by auto
+      from ih [OF this] and eq_e
+      show ?thesis 
+        apply (unfold eq_e cntCS_def holdents_def)
+        by (simp add:depend_set_unchanged)
+    qed
+    next
+      case vt_nil
+      show ?case
+      by (auto simp:count_def holdents_def s_depend_def wq_def cs_holding_def)
+  qed
+qed
+
+
+
+lemma next_th_neq: 
+  assumes vt: "vt step s"
+  and nt: "next_th s th cs th'"
+  shows "th' \<noteq> th"
+proof -
+  from nt show ?thesis
+    apply (auto simp:next_th_def)
+  proof -
+    fix rest
+    assume eq_wq: "wq s cs = hd (SOME q. distinct q \<and> set q = set rest) # rest"
+      and ne: "rest \<noteq> []"
+    have "hd (SOME q. distinct q \<and> set q = set rest) \<in> set rest" 
+    proof(rule someI2)
+      from wq_distinct[OF vt, of cs] eq_wq
+      show "distinct rest \<and> set rest = set rest" by auto
+    next
+      fix x
+      assume "distinct x \<and> set x = set rest"
+      hence eq_set: "set x = set rest" by auto
+      with ne have "x \<noteq> []" by auto
+      hence "hd x \<in> set x" by auto
+      with eq_set show "hd x \<in> set rest" by auto
+    qed
+    with wq_distinct[OF vt, of cs] eq_wq show False by auto
+  qed
+qed
+
+lemma next_th_unique: 
+  assumes nt1: "next_th s th cs th1"
+  and nt2: "next_th s th cs th2"
+  shows "th1 = th2"
+proof -
+  from assms show ?thesis
+    by (unfold next_th_def, auto)
+qed
+
+lemma pp_sub: "(r^+)^+ \<subseteq> r^+"
+  by auto
+
+lemma wf_depend:
+  assumes vt: "vt step s"
+  shows "wf (depend s)"
+proof(rule finite_acyclic_wf)
+  from finite_depend[OF vt] show "finite (depend s)" .
+next
+  from acyclic_depend[OF vt] show "acyclic (depend 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 =
+            {(Th th', Th th) | th th'. \<exists> cs. (Th th', Cs cs) \<in> depend s \<and> (Cs cs, Th th) \<in> depend s}"
+
+definition children :: "state \<Rightarrow> thread \<Rightarrow> thread set"
+  where "children s th = {th'. (Th th', Th th) \<in> child s}"
+
+
+lemma children_dependents: "children s th \<subseteq> dependents (wq s) th"
+  by (unfold children_def child_def cs_dependents_def, auto simp:eq_depend)
+
+lemma child_unique:
+  assumes vt: "vt step s"
+  and ch1: "(Th th, Th th1) \<in> child s"
+  and ch2: "(Th th, Th th2) \<in> child s"
+  shows "th1 = th2"
+proof -
+  from ch1 ch2 show ?thesis
+  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]
+    show "th1 = th2" by simp
+  qed 
+qed
+
+
+lemma cp_eq_cpreced_f: "cp s = cpreced s (wq s)"
+proof -
+  from fun_eq_iff 
+  have h:"\<And>f g. (\<forall> x. f x = g x) \<Longrightarrow> f = g" by auto
+  show ?thesis
+  proof(rule h)
+    from cp_eq_cpreced show "\<forall>x. cp s x = cpreced s (wq s) x" by auto
+  qed
+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)^+)"
+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"
+    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>+)"
+    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>+)"
+      proof -
+        from eq_c and h4 obtain th3 where eq_ca: "ca = Th th3"
+          by (case_tac ca, auto simp:s_depend_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
+        ultimately show ?thesis by auto
+      qed
+    next
+      assume "(Th th1, c) \<in> depend 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"
+    thus ?thesis
+      by (auto simp:s_depend_def)
+  qed
+qed
+
+lemma sub_child: "child s \<subseteq> (depend s)^+"
+  by (unfold child_def, auto)
+
+lemma wf_child: 
+  assumes vt: "vt step s"
+  shows "wf (child s)"
+proof(rule wf_subset)
+  from wf_trancl[OF wf_depend[OF vt]]
+  show "wf ((depend s)\<^sup>+)" .
+next
+  from sub_child show "child s \<subseteq> (depend s)\<^sup>+" .
+qed
+
+lemma depend_child_pre:
+  assumes vt: "vt step 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")
+proof -
+  from wf_trancl[OF wf_depend[OF vt]]
+  have wf: "wf ((depend 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>+"
+    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>+)" .
+      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>+"
+        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)
+        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
+    qed
+  qed
+qed
+
+lemma depend_child: "\<lbrakk>vt step s; (Th th, Th th') \<in> (depend s)^+\<rbrakk> \<Longrightarrow> (Th th, Th th') \<in> (child s)^+"
+  by (insert depend_child_pre, auto)
+
+lemma child_depend_p:
+  assumes "(n1, n2) \<in> (child s)^+"
+  shows "(n1, n2) \<in> (depend s)^+"
+proof -
+  from assms show ?thesis
+  proof(induct)
+    case (base y)
+    with sub_child show ?case by auto
+  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
+    ultimately show ?case by auto
+  qed
+qed
+
+lemma child_depend_eq: 
+  assumes vt: "vt step s"
+  shows 
+  "((Th th1, Th th2) \<in> (child s)^+) = 
+   ((Th th1, Th th2) \<in> (depend s)^+)"
+  by (auto intro: depend_child[OF vt] child_depend_p)
+
+lemma children_no_dep:
+  fixes s th th1 th2 th3
+  assumes vt: "vt step 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)^+"
+  shows "False"
+proof -
+  from depend_child[OF vt ch3]
+  have "(Th th1, Th th2) \<in> (child s)\<^sup>+" .
+  thus ?thesis
+  proof(rule converse_tranclE)
+    thm tranclD
+    assume "(Th th1, Th th2) \<in> child s"
+    from child_unique[OF vt ch1 this] have "th = th2" by simp
+    with ch2 have "(Th th2, Th th2) \<in> child s" by simp
+    with wf_child[OF vt] show ?thesis by auto
+  next
+    fix c
+    assume h1: "(Th th1, c) \<in> child s"
+      and h2: "(c, Th th2) \<in> (child s)\<^sup>+"
+    from h1 obtain th3 where eq_c: "c = Th th3" by (unfold child_def, auto)
+    with h1 have "(Th th1, Th th3) \<in> child s" by simp
+    from child_unique[OF vt ch1 this] have eq_th3: "th3 = th" by simp
+    with eq_c and h2 have "(Th th, Th th2) \<in> (child s)\<^sup>+" by simp
+    with ch2 have "(Th th, Th th) \<in> (child s)\<^sup>+" by auto
+    moreover have "wf ((child s)\<^sup>+)"
+    proof(rule wf_trancl)
+      from wf_child[OF vt] show "wf (child s)" .
+    qed
+    ultimately show False by auto
+  qed
+qed
+
+lemma unique_depend_p:
+  assumes vt: "vt step s"
+  and dp1: "(n, n1) \<in> (depend s)^+"
+  and dp2: "(n, n2) \<in> (depend s)^+"
+  and neq: "n1 \<noteq> n2"
+  shows "(n1, n2) \<in> (depend s)^+ \<or> (n2, n1) \<in> (depend 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
+qed
+
+lemma dependents_child_unique:
+  fixes s th th1 th2 th3
+  assumes vt: "vt step s"
+  and ch1: "(Th th1, Th th) \<in> child s"
+  and ch2: "(Th th2, Th th) \<in> child s"
+  and dp1: "th3 \<in> dependents s th1"
+  and dp2: "th3 \<in> dependents s th2"
+shows "th1 = th2"
+proof -
+  { assume neq: "th1 \<noteq> th2"
+    from dp1 have dp1: "(Th th3, Th th1) \<in> (depend s)^+" 
+      by (simp add:s_dependents_def eq_depend)
+    from dp2 have dp2: "(Th th3, Th th2) \<in> (depend s)^+" 
+      by (simp add:s_dependents_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
+    hence False
+    proof
+      assume "(Th th1, Th th2) \<in> (depend s)\<^sup>+ "
+      from children_no_dep[OF vt ch1 ch2 this] show ?thesis .
+    next
+      assume " (Th th2, Th th1) \<in> (depend s)\<^sup>+"
+      from children_no_dep[OF vt ch2 ch1 this] show ?thesis .
+    qed
+  } thus ?thesis by auto
+qed
+
+lemma cp_rec:
+  fixes s th
+  assumes vt: "vt step s"
+  shows "cp s th = Max ({preced th s} \<union> (cp s ` children s th))"
+proof(unfold cp_eq_cpreced_f cpreced_def)
+  let ?f = "(\<lambda>th. preced th s)"
+  show "Max ((\<lambda>th. preced th s) ` ({th} \<union> dependents (wq s) th)) =
+        Max ({preced th s} \<union> (\<lambda>th. Max ((\<lambda>th. preced th s) ` ({th} \<union> dependents (wq s) th))) ` children s th)"
+  proof(cases " children s th = {}")
+    case False
+    have "(\<lambda>th. Max ((\<lambda>th. preced th s) ` ({th} \<union> dependents (wq s) th))) ` children s th = 
+          {Max ((\<lambda>th. preced th s) ` ({th'} \<union> dependents (wq s) th')) | th' . th' \<in> children s th}"
+      (is "?L = ?R")
+      by auto
+    also have "\<dots> = 
+      Max ` {((\<lambda>th. preced th s) ` ({th'} \<union> dependents (wq s) th')) | th' . th' \<in> children s th}"
+      (is "_ = Max ` ?C")
+      by auto
+    finally have "Max ?L = Max (Max ` ?C)" by auto
+    also have "\<dots> = Max (\<Union> ?C)"
+    proof(rule Max_Union[symmetric])
+      from children_dependents[of s th] finite_threads[OF vt] and dependents_threads[OF vt, of th]
+      show "finite {(\<lambda>th. preced th s) ` ({th'} \<union> dependents (wq s) th') |th'. th' \<in> children s th}"
+        by (auto simp:finite_subset)
+    next
+      from False
+      show "{(\<lambda>th. preced th s) ` ({th'} \<union> dependents (wq s) th') |th'. th' \<in> children s th} \<noteq> {}"
+        by simp
+    next
+      show "\<And>A. A \<in> {(\<lambda>th. preced th s) ` ({th'} \<union> dependents (wq s) th') |th'. th' \<in> children s th} \<Longrightarrow>
+        finite A \<and> A \<noteq> {}"
+        apply (auto simp:finite_subset)
+      proof -
+        fix th'
+        from finite_threads[OF vt] and dependents_threads[OF vt, of th']
+        show "finite ((\<lambda>th. preced th s) ` dependents (wq s) th')" by (auto simp:finite_subset)
+      qed
+    qed
+    also have "\<dots> = Max ((\<lambda>th. preced th s) ` dependents (wq s) th)"
+      (is "Max ?A = Max ?B")
+    proof -
+      have "?A = ?B"
+      proof
+        show "\<Union>{(\<lambda>th. preced th s) ` ({th'} \<union> dependents (wq s) th') |th'. th' \<in> children s th}
+                    \<subseteq> (\<lambda>th. preced th s) ` dependents (wq s) th"
+        proof
+          fix x 
+          assume "x \<in> \<Union>{(\<lambda>th. preced th s) ` ({th'} \<union> dependents (wq s) th') |th'. th' \<in> children s th}"
+          then obtain th' where 
+             th'_in: "th' \<in> children s th"
+            and x_in: "x \<in> ?f ` ({th'} \<union> dependents (wq s) th')" by auto
+          hence "x = ?f th' \<or> x \<in> (?f ` dependents (wq s) th')" by auto
+          thus "x \<in> ?f ` dependents (wq s) th"
+          proof
+            assume "x = preced th' s"
+            with th'_in and children_dependents
+            show "x \<in> (\<lambda>th. preced th s) ` dependents (wq s) th" by auto
+          next
+            assume "x \<in> (\<lambda>th. preced th s) ` dependents (wq s) th'"
+            moreover note th'_in
+            ultimately show " x \<in> (\<lambda>th. preced th s) ` dependents (wq s) th"
+              by (unfold cs_dependents_def children_def child_def, auto simp:eq_depend)
+          qed
+        qed
+      next
+        show "?f ` dependents (wq s) th
+           \<subseteq> \<Union>{?f ` ({th'} \<union> dependents (wq s) th') |th'. th' \<in> children s th}"
+        proof
+          fix x 
+          assume x_in: "x \<in> (\<lambda>th. preced th s) ` dependents (wq s) th"
+          then obtain th' where
+            eq_x: "x = ?f th'" and dp: "(Th th', Th th) \<in> (depend s)^+" 
+            by (auto simp:cs_dependents_def eq_depend)
+          from depend_children[OF dp]
+          have "th' \<in> children s th \<or> (\<exists>th3. th3 \<in> children s th \<and> (Th th', Th th3) \<in> (depend s)\<^sup>+)" .
+          thus "x \<in> \<Union>{(\<lambda>th. preced th s) ` ({th'} \<union> dependents (wq s) th') |th'. th' \<in> children s th}"
+          proof
+            assume "th' \<in> children s th"
+            with eq_x
+            show "x \<in> \<Union>{(\<lambda>th. preced th s) ` ({th'} \<union> dependents (wq s) th') |th'. th' \<in> children s th}"
+              by auto
+          next
+            assume "\<exists>th3. th3 \<in> children s th \<and> (Th th', Th th3) \<in> (depend s)\<^sup>+"
+            then obtain th3 where th3_in: "th3 \<in> children s th"
+              and dp3: "(Th th', Th th3) \<in> (depend s)\<^sup>+" by auto
+            show "x \<in> \<Union>{(\<lambda>th. preced th s) ` ({th'} \<union> dependents (wq s) th') |th'. th' \<in> children s th}"
+            proof -
+              from dp3
+              have "th' \<in> dependents (wq s) th3"
+                by (auto simp:cs_dependents_def eq_depend)
+              with eq_x th3_in show ?thesis by auto
+            qed
+          qed          
+        qed
+      qed
+      thus ?thesis by simp
+    qed
+    finally have "Max ((\<lambda>th. preced th s) ` dependents (wq s) th) = Max (?L)" 
+      (is "?X = ?Y") by auto
+    moreover have "Max ((\<lambda>th. preced th s) ` ({th} \<union> dependents (wq s) th)) = 
+                   max (?f th) ?X" 
+    proof -
+      have "Max ((\<lambda>th. preced th s) ` ({th} \<union> dependents (wq s) th)) = 
+            Max ({?f th} \<union> ?f ` (dependents (wq s) th))" by simp
+      also have "\<dots> = max (Max {?f th}) (Max (?f ` (dependents (wq s) th)))"
+      proof(rule Max_Un, auto)
+        from finite_threads[OF vt] and dependents_threads[OF vt, of th]
+        show "finite ((\<lambda>th. preced th s) ` dependents (wq s) th)" by (auto simp:finite_subset)
+      next
+        assume "dependents (wq s) th = {}"
+        with False and children_dependents show False by auto
+      qed
+      also have "\<dots> = max (?f th) ?X" by simp
+      finally show ?thesis .
+    qed
+    moreover have "Max ({preced th s} \<union> 
+                     (\<lambda>th. Max ((\<lambda>th. preced th s) ` ({th} \<union> dependents (wq s) th))) ` children s th) = 
+                   max (?f th) ?Y"
+    proof -
+      have "Max ({preced th s} \<union> 
+                     (\<lambda>th. Max ((\<lambda>th. preced th s) ` ({th} \<union> dependents (wq s) th))) ` children s th) = 
+            max (Max {preced th s}) ?Y"
+      proof(rule Max_Un, auto)
+        from finite_threads[OF vt] dependents_threads[OF vt, of th] children_dependents [of s th]
+        show "finite ((\<lambda>th. Max (insert (preced th s) ((\<lambda>th. preced th s) ` dependents (wq s) th))) ` 
+                       children s th)" 
+          by (auto simp:finite_subset)
+      next
+        assume "children s th = {}"
+        with False show False by auto
+      qed
+      thus ?thesis by simp
+    qed
+    ultimately show ?thesis by auto
+  next
+    case True
+    moreover have "dependents (wq s) th = {}"
+    proof -
+      { fix th'
+        assume "th' \<in> dependents (wq s) th"
+        hence " (Th th', Th th) \<in> (depend s)\<^sup>+" by (simp add:cs_dependents_def eq_depend)
+        from depend_children[OF this] and True
+        have "False" by auto
+      } thus ?thesis by auto
+    qed
+    ultimately show ?thesis by auto
+  qed
+qed
+
+definition cps:: "state \<Rightarrow> (thread \<times> precedence) set"
+where "cps s = {(th, cp s th) | th . th \<in> threads s}"
+
+locale step_set_cps =
+  fixes s' th prio s 
+  defines s_def : "s \<equiv> (Set th prio#s')"
+  assumes vt_s: "vt step s"
+
+context step_set_cps 
+begin
+
+lemma eq_preced:
+  fixes th'
+  assumes "th' \<noteq> th"
+  shows "preced th' s = preced th' s'"
+proof -
+  from assms show ?thesis 
+    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_cp:
+  fixes th' 
+  assumes neq_th: "th' \<noteq> th"
+  and nd: "th \<notin> dependents s th'"
+  shows "cp s th' = cp s' th'"
+  apply (unfold cp_eq_cpreced cpreced_def)
+proof -
+  have eq_dp: "\<And> th. dependents (wq s) th = dependents (wq s') th"
+    by (unfold cs_dependents_def, auto simp:eq_dep eq_depend)
+  moreover {
+    fix th1 
+    assume "th1 \<in> {th'} \<union> dependents (wq s') th'"
+    hence "th1 = th' \<or> th1 \<in> dependents (wq s') th'" by auto
+    hence "preced th1 s = preced th1 s'"
+    proof
+      assume "th1 = th'"
+      with eq_preced[OF neq_th]
+      show "preced th1 s = preced th1 s'" by simp
+    next
+      assume "th1 \<in> dependents (wq s') th'"
+      with nd and eq_dp have "th1 \<noteq> th"
+        by (auto simp:eq_depend cs_dependents_def s_dependents_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> dependents (wq s) th')) = 
+                     ((\<lambda>th. preced th s') ` ({th'} \<union> dependents (wq s') th'))" 
+    by (auto simp:image_def)
+  thus "Max ((\<lambda>th. preced th s) ` ({th'} \<union> dependents (wq s) th')) =
+        Max ((\<lambda>th. preced th s') ` ({th'} \<union> dependents (wq s') th'))" by simp
+qed
+
+lemma eq_up:
+  fixes th' th''
+  assumes dp1: "th \<in> dependents s th'"
+  and dp2: "th' \<in> dependents s th''"
+  and eq_cps: "cp s th' = cp s' th'"
+  shows "cp s th'' = cp s' th''"
+proof -
+  from dp2
+  have "(Th th', Th th'') \<in> (depend (wq s))\<^sup>+" by (simp add:s_dependents_def)
+  from depend_child[OF vt_s this[unfolded eq_depend]]
+  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>
+                   (\<forall> th'' . n = Th th'' \<longrightarrow> cp s th'' = cp s' th'')"
+    proof(erule trancl_induct, auto)
+      fix y th''
+      assume y_ch: "(y, Th th'') \<in> child s"
+        and ih: "\<forall>th''. y = Th th'' \<longrightarrow> cp s th'' = cp s' th''"
+        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_dependents_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
+      show "cp s th'' = cp s' th''"
+        apply (subst cp_rec[OF vt_s])
+      proof -
+        have "preced th'' s = preced th'' s'"
+        proof(rule eq_preced)
+          show "th'' \<noteq> th"
+          proof
+            assume "th'' = th"
+            with dp_thy y_ch[unfolded eq_y] 
+            have "(Th th, Th th) \<in> (depend s)^+"
+              by (auto simp:child_def)
+            with wf_trancl[OF wf_depend[OF vt_s]] 
+            show False by auto
+          qed
+        qed
+        moreover { 
+          fix th1
+          assume th1_in: "th1 \<in> children s th''"
+          have "cp s th1 = cp s' th1"
+          proof(cases "th1 = thy")
+            case True
+            with eq_cpy show ?thesis by simp
+          next
+            case False
+            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
+              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> dependents s th1"
+            proof
+              assume h:"th \<in> dependents s th1"
+              from eq_y dp_thy have "th \<in> dependents s thy" by (auto simp:s_dependents_def eq_depend)
+              from dependents_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
+            qed
+            from eq_cp[OF neq_th1 this]
+            show ?thesis .
+          qed
+        }
+        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)
+        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
+    next
+      fix th''
+      assume dp': "(Th th', Th th'') \<in> child s"
+      show "cp s th'' = cp s' th''"
+        apply (subst cp_rec[OF vt_s])
+      proof -
+        have "preced th'' s = preced th'' s'"
+        proof(rule eq_preced)
+          show "th'' \<noteq> th"
+          proof
+            assume "th'' = th"
+            with dp1 dp'
+            have "(Th th, Th th) \<in> (depend s)^+"
+              by (auto simp:child_def s_dependents_def eq_depend)
+            with wf_trancl[OF wf_depend[OF vt_s]] 
+            show False by auto
+          qed
+        qed
+        moreover { 
+          fix th1
+          assume th1_in: "th1 \<in> children s th''"
+          have "cp s th1 = cp s' th1"
+          proof(cases "th1 = th'")
+            case True
+            with eq_cps show ?thesis by simp
+          next
+            case False
+            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_dependents_def eq_depend)
+              from children_no_dep[OF vt_s _ _ this]
+              th1_in dp'
+              show False by (auto simp:children_def)
+            qed
+            thus ?thesis
+            proof(rule eq_cp)
+              show "th \<notin> dependents s th1"
+              proof
+                assume "th \<in> dependents s th1"
+                from dependents_child_unique[OF vt_s _ _ this dp1]
+                th1_in dp' have "th1 = th'"
+                  by (auto simp:children_def)
+                with False show False by auto
+              qed
+            qed
+          qed
+        }
+        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)
+        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     
+    qed
+  }
+  ultimately show ?thesis by auto
+qed
+
+lemma eq_up_self:
+  fixes th' th''
+  assumes dp: "th \<in> dependents s th''"
+  and eq_cps: "cp s th = cp s' th"
+  shows "cp s th'' = cp s' th''"
+proof -
+  from dp
+  have "(Th th, Th th'') \<in> (depend (wq s))\<^sup>+" by (simp add:s_dependents_def)
+  from depend_child[OF vt_s this[unfolded eq_depend]]
+  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>
+                   (\<forall> th'' . n = Th th'' \<longrightarrow> cp s th'' = cp s' th'')"
+    proof(erule trancl_induct, auto)
+      fix y th''
+      assume y_ch: "(y, Th th'') \<in> child s"
+        and ih: "\<forall>th''. y = Th th'' \<longrightarrow> cp s th'' = cp s' th''"
+        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
+      show "cp s th'' = cp s' th''"
+        apply (subst cp_rec[OF vt_s])
+      proof -
+        have "preced th'' s = preced th'' s'"
+        proof(rule eq_preced)
+          show "th'' \<noteq> th"
+          proof
+            assume "th'' = th"
+            with dp_thy y_ch[unfolded eq_y] 
+            have "(Th th, Th th) \<in> (depend s)^+"
+              by (auto simp:child_def)
+            with wf_trancl[OF wf_depend[OF vt_s]] 
+            show False by auto
+          qed
+        qed
+        moreover { 
+          fix th1
+          assume th1_in: "th1 \<in> children s th''"
+          have "cp s th1 = cp s' th1"
+          proof(cases "th1 = thy")
+            case True
+            with eq_cpy show ?thesis by simp
+          next
+            case False
+            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
+              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> dependents s th1"
+            proof
+              assume h:"th \<in> dependents s th1"
+              from eq_y dp_thy have "th \<in> dependents s thy" by (auto simp:s_dependents_def eq_depend)
+              from dependents_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
+            qed
+            from eq_cp[OF neq_th1 this]
+            show ?thesis .
+          qed
+        }
+        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)
+        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
+    next
+      fix th''
+      assume dp': "(Th th, Th th'') \<in> child s"
+      show "cp s th'' = cp s' th''"
+        apply (subst cp_rec[OF vt_s])
+      proof -
+        have "preced th'' s = preced th'' s'"
+        proof(rule eq_preced)
+          show "th'' \<noteq> th"
+          proof
+            assume "th'' = th"
+            with dp dp'
+            have "(Th th, Th th) \<in> (depend s)^+"
+              by (auto simp:child_def s_dependents_def eq_depend)
+            with wf_trancl[OF wf_depend[OF vt_s]] 
+            show False by auto
+          qed
+        qed
+        moreover { 
+          fix th1
+          assume th1_in: "th1 \<in> children s th''"
+          have "cp s th1 = cp s' th1"
+          proof(cases "th1 = th")
+            case True
+            with eq_cps show ?thesis by simp
+          next
+            case False
+            assume neq_th1: "th1 \<noteq> th"
+            thus ?thesis
+            proof(rule eq_cp)
+              show "th \<notin> dependents s th1"
+              proof
+                assume "th \<in> dependents s th1"
+                hence "(Th th, Th th1) \<in> (depend s)^+" by (auto simp:s_dependents_def eq_depend)
+                from children_no_dep[OF vt_s _ _ this]
+                and th1_in dp' show False
+                  by (auto simp:children_def)
+              qed
+            qed
+          qed
+        }
+        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)
+        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     
+    qed
+  }
+  ultimately show ?thesis by auto
+qed
+end
+
+lemma next_waiting:
+  assumes vt: "vt step s"
+  and nxt: "next_th s th cs th'"
+  shows "waiting s th' cs"
+proof -
+  from assms show ?thesis
+    apply (auto simp:next_th_def s_waiting_def)
+  proof -
+    fix rest
+    assume ni: "hd (SOME q. distinct q \<and> set q = set rest) \<notin> set rest"
+      and eq_wq: "wq s cs = th # rest"
+      and ne: "rest \<noteq> []"
+    have "set (SOME q. distinct q \<and> set q = set rest) = set rest" 
+    proof(rule someI2)
+      from wq_distinct[OF vt, of cs] eq_wq
+      show "distinct rest \<and> set rest = set rest" by auto
+    next
+      show "\<And>x. distinct x \<and> set x = set rest \<Longrightarrow> set x = set rest" by auto
+    qed
+    with ni
+    have "hd (SOME q. distinct q \<and> set q = set rest) \<notin>  set (SOME q. distinct q \<and> set q = set rest)"
+      by simp
+    moreover have "(SOME q. distinct q \<and> set q = set rest) \<noteq> []"
+    proof(rule someI2)
+      from wq_distinct[OF vt, of cs] eq_wq
+      show "distinct rest \<and> set rest = set rest" by auto
+    next
+      from ne show "\<And>x. distinct x \<and> set x = set rest \<Longrightarrow> x \<noteq> []" by auto
+    qed
+    ultimately show "hd (SOME q. distinct q \<and> set q = set rest) = th" by auto
+  next
+    fix rest
+    assume eq_wq: "wq s cs = hd (SOME q. distinct q \<and> set q = set rest) # rest"
+      and ne: "rest \<noteq> []"
+    have "(SOME q. distinct q \<and> set q = set rest) \<noteq> []"
+    proof(rule someI2)
+      from wq_distinct[OF vt, of cs] eq_wq
+      show "distinct rest \<and> set rest = set rest" by auto
+    next
+      from ne show "\<And>x. distinct x \<and> set x = set rest \<Longrightarrow> x \<noteq> []" by auto
+    qed
+    hence "hd (SOME q. distinct q \<and> set q = set rest) \<in> set (SOME q. distinct q \<and> set q = set rest)"
+      by auto
+    moreover have "set (SOME q. distinct q \<and> set q = set rest) = set rest" 
+    proof(rule someI2)
+      from wq_distinct[OF vt, of cs] eq_wq
+      show "distinct rest \<and> set rest = set rest" by auto
+    next
+      show "\<And>x. distinct x \<and> set x = set rest \<Longrightarrow> set x = set rest" by auto
+    qed
+    ultimately have "hd (SOME q. distinct q \<and> set q = set rest) \<in> set rest" by simp
+    with eq_wq and wq_distinct[OF vt, of cs]
+    show False by auto
+  qed
+qed
+
+locale step_v_cps =
+  fixes s' th cs s 
+  defines s_def : "s \<equiv> (V th cs#s')"
+  assumes vt_s: "vt step s"
+
+locale step_v_cps_nt = step_v_cps +
+  fixes th'
+  assumes nt: "next_th s' th cs th'"
+
+context step_v_cps_nt
+begin
+
+lemma depend_s:
+  "depend s = (depend 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]
+    and nt show ?thesis  by (auto intro:next_th_unique)
+qed
+
+lemma dependents_kept:
+  fixes th''
+  assumes neq1: "th'' \<noteq> th"
+  and neq2: "th'' \<noteq> th'"
+  shows "dependents (wq s) th'' = dependents (wq s') th''"
+proof(auto)
+  fix x
+  assume "x \<in> dependents (wq s) th''"
+  hence dp: "(Th x, Th th'') \<in> (depend s)^+"
+    by (auto simp:cs_dependents_def eq_depend)
+  { fix n
+    have "(n, Th th'') \<in> (depend s)^+ \<Longrightarrow>  (n, Th th'') \<in> (depend 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
+    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>+"
+      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] 
+          have eq_z: "z = Th th'" by simp
+          with ztp have "(Th th', Th th'') \<in> (depend 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
+          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 s_depend_def cs_waiting_def)
+            from unique_depend[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 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
+          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 s_depend_def cs_waiting_def)
+            from unique_depend[OF step_back_vt[OF vt_s[unfolded s_def]] dps' this]
+            show ?thesis .
+          qed
+          with dps depend_s show False by auto
+        qed
+      qed
+      with depend_s yz have "(y, z) \<in> depend s'" by auto
+      with ztp'
+      show "(y, Th th'') \<in> (depend s')\<^sup>+" by auto
+    qed    
+  }
+  from this[OF dp]
+  show "x \<in> dependents (wq s') th''" 
+    by (auto simp:cs_dependents_def eq_depend)
+next
+  fix x
+  assume "x \<in> dependents (wq s') th''"
+  hence dp: "(Th x, Th th'') \<in> (depend s')^+"
+    by (auto simp:cs_dependents_def eq_depend)
+  { fix n
+    have "(n, Th th'') \<in> (depend s')^+ \<Longrightarrow>  (n, Th th'') \<in> (depend 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
+    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>+"
+      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 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: 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]
+            show ?thesis by simp
+          qed
+          from converse_tranclE[OF ztp]
+          obtain u where "(z, u) \<in> depend 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 s_depend_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
+          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 s_depend_def cs_waiting_def)
+            from unique_depend[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
+          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 cs_holding_def s_holding_def)
+          have "(Cs cs, Th th'') \<notin>  depend 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]
+            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
+          have "u = Th th"
+          proof -
+            from unique_depend[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
+          from converse_tranclE[OF this]
+          obtain v where "(Th th, v) \<in> (depend 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 s_depend_def s_waiting_def cs_waiting_def)
+        qed
+      qed
+      with depend_s yz have "(y, z) \<in> depend s" by auto
+      with ztp'
+      show "(y, Th th'') \<in> (depend s)\<^sup>+" by auto
+    qed    
+  }
+  from this[OF dp]
+  show "x \<in> dependents (wq s) th''"
+    by (auto simp:cs_dependents_def eq_depend)
+qed
+
+lemma cp_kept:
+  fixes th''
+  assumes neq1: "th'' \<noteq> th"
+  and neq2: "th'' \<noteq> th'"
+  shows "cp s th'' = cp s' th''"
+proof -
+  from dependents_kept[OF neq1 neq2]
+  have "dependents (wq s) th'' = dependents (wq s') th''" .
+  moreover {
+    fix th1
+    assume "th1 \<in> dependents (wq s) th''"
+    have "preced th1 s = preced th1 s'" 
+      by (unfold s_def, auto simp:preced_def)
+  }
+  moreover have "preced th'' s = preced th'' s'" 
+    by (unfold s_def, auto simp:preced_def)
+  ultimately have "((\<lambda>th. preced th s) ` ({th''} \<union> dependents (wq s) th'')) = 
+    ((\<lambda>th. preced th s') ` ({th''} \<union> dependents (wq s') th''))"
+    by (auto simp:image_def)
+  thus ?thesis
+    by (unfold cp_eq_cpreced cpreced_def, simp)
+qed
+
+end
+
+locale step_v_cps_nnt = step_v_cps +
+  assumes nnt: "\<And> th'. (\<not> next_th s' th cs th')"
+
+context step_v_cps_nnt
+begin
+
+lemma nw_cs: "(Th th1, Cs cs) \<notin> depend s'"
+proof
+  assume "(Th th1, Cs cs) \<in> depend s'"
+  thus "False"
+    apply (auto simp:s_depend_def cs_waiting_def)
+  proof -
+    assume h1: "th1 \<in> set (wq s' cs)"
+      and h2: "th1 \<noteq> hd (wq s' cs)"
+    from step_back_step[OF vt_s[unfolded s_def]]
+    show "False"
+    proof(cases)
+      assume "holding s' th cs" 
+      then obtain rest where
+        eq_wq: "wq s' cs = th#rest"
+        apply (unfold s_holding_def)
+        by (case_tac "(wq s' cs)", auto)
+      with h1 h2 have ne: "rest \<noteq> []" by auto
+      with eq_wq
+      have "next_th s' th cs (hd (SOME q. distinct q \<and> set q = set rest))"
+        by(unfold next_th_def, rule_tac x = "rest" in exI, auto)
+      with nnt show ?thesis by auto
+    qed
+  qed
+qed
+
+lemma depend_s: "depend s = depend s' - {(Cs cs, Th th)}"
+proof -
+  from nnt and  step_depend_v[OF vt_s[unfolded s_def], folded s_def]
+  show ?thesis by auto
+qed
+
+lemma child_kept_left:
+  assumes 
+  "(n1, n2) \<in> (child s')^+"
+  shows "(n1, n2) \<in> (child s)^+"
+proof -
+  from assms show ?thesis 
+  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'"
+      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 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
+    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
+  next
+    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'"
+      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 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
+    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
+    ultimately show ?case by auto
+  qed
+qed
+
+lemma  child_kept_right:
+  assumes
+  "(n1, n2) \<in> (child s)^+"
+  shows "(n1, n2) \<in> (child s')^+"
+proof -
+  from assms show ?thesis
+  proof(induct)
+    case (base y)
+    from base and depend_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'"
+      by (auto simp:child_def)
+    moreover have "(n1, y) \<in> (child s')\<^sup>+" by fact
+    ultimately show ?case by auto
+  qed
+qed
+
+lemma eq_child: "(child s)^+ = (child s')^+"
+  by (insert child_kept_left child_kept_right, auto)
+
+lemma eq_cp:
+  fixes th' 
+  shows "cp s th' = cp s' th'"
+  apply (unfold cp_eq_cpreced cpreced_def)
+proof -
+  have eq_dp: "\<And> th. dependents (wq s) th = dependents (wq s') th"
+    apply (unfold cs_dependents_def, unfold eq_depend)
+  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>+}"
+      by simp
+  qed
+  moreover {
+    fix th1 
+    assume "th1 \<in> {th'} \<union> dependents (wq s') th'"
+    hence "th1 = th' \<or> th1 \<in> dependents (wq s') th'" by auto
+    hence "preced th1 s = preced th1 s'"
+    proof
+      assume "th1 = th'"
+      show "preced th1 s = preced th1 s'" by (simp add:s_def preced_def)
+    next
+      assume "th1 \<in> dependents (wq s') th'"
+      show "preced th1 s = preced th1 s'" by (simp add:s_def preced_def)
+    qed
+  } ultimately have "((\<lambda>th. preced th s) ` ({th'} \<union> dependents (wq s) th')) = 
+                     ((\<lambda>th. preced th s') ` ({th'} \<union> dependents (wq s') th'))" 
+    by (auto simp:image_def)
+  thus "Max ((\<lambda>th. preced th s) ` ({th'} \<union> dependents (wq s) th')) =
+        Max ((\<lambda>th. preced th s') ` ({th'} \<union> dependents (wq s') th'))" by simp
+qed
+
+end
+
+locale step_P_cps =
+  fixes s' th cs s 
+  defines s_def : "s \<equiv> (P th cs#s')"
+  assumes vt_s: "vt step s"
+
+locale step_P_cps_ne =step_P_cps +
+  assumes ne: "wq s' cs \<noteq> []"
+
+context step_P_cps_ne
+begin
+
+lemma depend_s: "depend s = depend s' \<union> {(Th th, Cs cs)}"
+proof -
+  from step_depend_p[OF vt_s[unfolded s_def]] and ne
+  show ?thesis by (simp add:s_def)
+qed
+
+lemma eq_child_left:
+  assumes nd: "(Th th, Th th') \<notin> (child s)^+"
+  shows "(n1, Th th') \<in> (child s)^+ \<Longrightarrow> (n1, Th th') \<in> (child s')^+"
+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"
+    and eq_y: "y = Th th1"   by (auto simp:child_def)
+  have "th1 \<noteq> th"
+  proof
+    assume "th1 = th"
+    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 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"
+    and eq_y: "y = Th th1" and eq_z: "z = Th th2"  by (auto simp:child_def)
+  have "th1 \<noteq> th"
+  proof
+    assume "th1 = th"
+    with yz eq_y have "(Th th, z) \<in> child s" by simp
+    moreover have "(z, Th th') \<in> (child s)^+" by fact
+    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 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
+qed
+
+lemma eq_child_right:
+  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)
+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)
+  moreover have "(z, Th th') \<in> (child s)^+" by fact
+  ultimately show ?case by auto
+qed
+
+lemma eq_child:
+  assumes nd: "(Th th, Th th') \<notin> (child s)^+"
+  shows "((n1, Th th') \<in> (child s)^+) = ((n1, Th th') \<in> (child s')^+)"
+  by (insert eq_child_left[OF nd] eq_child_right, auto)
+
+lemma eq_cp:
+  fixes th' 
+  assumes nd: "th \<notin> dependents s th'"
+  shows "cp s th' = cp s' th'"
+  apply (unfold cp_eq_cpreced cpreced_def)
+proof -
+  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 nd show False 
+      by (simp add:s_dependents_def eq_depend)
+  qed
+  have eq_dp: "dependents (wq s) th' = dependents (wq s') th'"
+  proof(auto)
+    fix x assume " x \<in> dependents (wq s) th'"
+    thus "x \<in> dependents (wq s') th'"
+      apply (auto simp:cs_dependents_def eq_depend)
+    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
+      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
+    qed
+  next
+    fix x assume "x \<in> dependents (wq s') th'"
+    thus "x \<in> dependents (wq s) th'"
+      apply (auto simp:cs_dependents_def eq_depend)
+    proof -
+      assume "(Th x, Th th') \<in> (depend s')\<^sup>+"
+      with child_depend_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
+    qed
+  qed
+  moreover {
+    fix th1 have "preced th1 s = preced th1 s'" by (simp add:s_def preced_def)
+  } ultimately have "((\<lambda>th. preced th s) ` ({th'} \<union> dependents (wq s) th')) = 
+                     ((\<lambda>th. preced th s') ` ({th'} \<union> dependents (wq s') th'))" 
+    by (auto simp:image_def)
+  thus "Max ((\<lambda>th. preced th s) ` ({th'} \<union> dependents (wq s) th')) =
+        Max ((\<lambda>th. preced th s') ` ({th'} \<union> dependents (wq s') th'))" by simp
+qed
+
+lemma eq_up:
+  fixes th' th''
+  assumes dp1: "th \<in> dependents s th'"
+  and dp2: "th' \<in> dependents s th''"
+  and eq_cps: "cp s th' = cp s' th'"
+  shows "cp s th'' = cp s' th''"
+proof -
+  from dp2
+  have "(Th th', Th th'') \<in> (depend (wq s))\<^sup>+" by (simp add:s_dependents_def)
+  from depend_child[OF vt_s this[unfolded eq_depend]]
+  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>
+                   (\<forall> th'' . n = Th th'' \<longrightarrow> cp s th'' = cp s' th'')"
+    proof(erule trancl_induct, auto)
+      fix y th''
+      assume y_ch: "(y, Th th'') \<in> child s"
+        and ih: "\<forall>th''. y = Th th'' \<longrightarrow> cp s th'' = cp s' th''"
+        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_dependents_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
+      show "cp s th'' = cp s' th''"
+        apply (subst cp_rec[OF vt_s])
+      proof -
+        have "preced th'' s = preced th'' s'"
+          by (simp add:s_def preced_def)
+        moreover { 
+          fix th1
+          assume th1_in: "th1 \<in> children s th''"
+          have "cp s th1 = cp s' th1"
+          proof(cases "th1 = thy")
+            case True
+            with eq_cpy show ?thesis by simp
+          next
+            case False
+            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
+              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> dependents s th1"
+            proof
+              assume h:"th \<in> dependents s th1"
+              from eq_y dp_thy have "th \<in> dependents s thy" by (auto simp:s_dependents_def eq_depend)
+              from dependents_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
+            qed
+            from eq_cp[OF this]
+            show ?thesis .
+          qed
+        }
+        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)
+          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_dependents_def eq_depend)
+            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)
+            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]
+              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']
+              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']
+              have "y = Th th''" .
+              with ytd have "(Th th'', Th th') \<in> (depend s)^+" by simp
+              from depend_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
+          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]]])
+      qed
+    next
+      fix th''
+      assume dp': "(Th th', Th th'') \<in> child s"
+      show "cp s th'' = cp s' th''"
+        apply (subst cp_rec[OF vt_s])
+      proof -
+        have "preced th'' s = preced th'' s'"
+          by (simp add:s_def preced_def)
+        moreover { 
+          fix th1
+          assume th1_in: "th1 \<in> children s th''"
+          have "cp s th1 = cp s' th1"
+          proof(cases "th1 = th'")
+            case True
+            with eq_cps show ?thesis by simp
+          next
+            case False
+            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_dependents_def eq_depend)
+              from children_no_dep[OF vt_s _ _ this]
+              th1_in dp'
+              show False by (auto simp:children_def)
+            qed
+            show ?thesis
+            proof(rule eq_cp)
+              show "th \<notin> dependents s th1"
+              proof
+                assume "th \<in> dependents s th1"
+                from dependents_child_unique[OF vt_s _ _ this dp1]
+                th1_in dp' have "th1 = th'"
+                  by (auto simp:children_def)
+                with False show False by auto
+              qed
+            qed
+          qed
+        }
+        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)
+          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_dependents_def eq_depend)
+            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)
+            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]
+              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']
+              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']
+              have "y = Th th''" .
+              with ytd have "(Th th'', Th th') \<in> (depend s)^+" by simp
+              from depend_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
+          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]]])
+      qed     
+    qed
+  }
+  ultimately show ?thesis by auto
+qed
+
+end
+
+locale step_create_cps =
+  fixes s' th prio s 
+  defines s_def : "s \<equiv> (Create th prio#s')"
+  assumes vt_s: "vt step s"
+
+context step_create_cps
+begin
+
+lemma eq_dep: "depend s = depend s'"
+  by (unfold s_def depend_create_unchanged, auto)
+
+lemma eq_cp:
+  fixes th' 
+  assumes neq_th: "th' \<noteq> th"
+  shows "cp s th' = cp s' th'"
+  apply (unfold cp_eq_cpreced cpreced_def)
+proof -
+  have nd: "th \<notin> dependents s th'"
+  proof
+    assume "th \<in> dependents s th'"
+    hence "(Th th, Th th') \<in> (depend s)^+" by (simp add:s_dependents_def eq_depend)
+    with eq_dep have "(Th th, Th th') \<in> (depend 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]]]
+    have in_th: "th \<in> threads s'" by auto
+    from step_back_step[OF vt_s[unfolded s_def]]
+    show False
+    proof(cases)
+      assume "th \<notin> threads s'" 
+      with in_th show ?thesis by simp
+    qed
+  qed
+  have eq_dp: "\<And> th. dependents (wq s) th = dependents (wq s') th"
+    by (unfold cs_dependents_def, auto simp:eq_dep eq_depend)
+  moreover {
+    fix th1 
+    assume "th1 \<in> {th'} \<union> dependents (wq s') th'"
+    hence "th1 = th' \<or> th1 \<in> dependents (wq s') th'" by auto
+    hence "preced th1 s = preced th1 s'"
+    proof
+      assume "th1 = th'"
+      with neq_th
+      show "preced th1 s = preced th1 s'" by (auto simp:s_def preced_def)
+    next
+      assume "th1 \<in> dependents (wq s') th'"
+      with nd and eq_dp have "th1 \<noteq> th"
+        by (auto simp:eq_depend cs_dependents_def s_dependents_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> dependents (wq s) th')) = 
+                     ((\<lambda>th. preced th s') ` ({th'} \<union> dependents (wq s') th'))" 
+    by (auto simp:image_def)
+  thus "Max ((\<lambda>th. preced th s) ` ({th'} \<union> dependents (wq s) th')) =
+        Max ((\<lambda>th. preced th s') ` ({th'} \<union> dependents (wq s') th'))" by simp
+qed
+
+lemma nil_dependents: "dependents s th = {}"
+proof -
+  from step_back_step[OF vt_s[unfolded s_def]]
+  show ?thesis
+  proof(cases)
+    assume "th \<notin> threads s'"
+    from not_thread_holdents[OF step_back_vt[OF vt_s[unfolded s_def]] this]
+    have hdn: " holdents s' th = {}" .
+    have "dependents s' th = {}"
+    proof -
+      { assume "dependents s' th \<noteq> {}"
+        then obtain th' where dp: "(Th th', Th th) \<in> (depend s')^+"
+          by (auto simp:s_dependents_def eq_depend)
+        from tranclE[OF this] obtain cs' where 
+          "(Cs cs', Th th) \<in> depend s'" by (auto simp:s_depend_def)
+        with hdn
+        have False by (auto simp:holdents_def)
+      } thus ?thesis by auto
+    qed
+    thus ?thesis 
+      by (unfold s_def s_dependents_def eq_depend depend_create_unchanged, simp)
+  qed
+qed
+
+lemma eq_cp_th: "cp s th = preced th s"
+  apply (unfold cp_eq_cpreced cpreced_def)
+  by (insert nil_dependents, unfold s_dependents_def cs_dependents_def, auto)
+
+end
+
+
+locale step_exit_cps =
+  fixes s' th prio s 
+  defines s_def : "s \<equiv> (Exit th#s')"
+  assumes vt_s: "vt step s"
+
+context step_exit_cps
+begin
+
+lemma eq_dep: "depend s = depend s'"
+  by (unfold s_def depend_exit_unchanged, auto)
+
+lemma eq_cp:
+  fixes th' 
+  assumes neq_th: "th' \<noteq> th"
+  shows "cp s th' = cp s' th'"
+  apply (unfold cp_eq_cpreced cpreced_def)
+proof -
+  have nd: "th \<notin> dependents s th'"
+  proof
+    assume "th \<in> dependents s th'"
+    hence "(Th th, Th th') \<in> (depend s)^+" by (simp add:s_dependents_def eq_depend)
+    with eq_dep have "(Th th, Th th') \<in> (depend 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)
+    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)
+        by (auto simp:cs_waiting_def)
+    qed
+  qed
+  have eq_dp: "\<And> th. dependents (wq s) th = dependents (wq s') th"
+    by (unfold cs_dependents_def, auto simp:eq_dep eq_depend)
+  moreover {
+    fix th1 
+    assume "th1 \<in> {th'} \<union> dependents (wq s') th'"
+    hence "th1 = th' \<or> th1 \<in> dependents (wq s') th'" by auto
+    hence "preced th1 s = preced th1 s'"
+    proof
+      assume "th1 = th'"
+      with neq_th
+      show "preced th1 s = preced th1 s'" by (auto simp:s_def preced_def)
+    next
+      assume "th1 \<in> dependents (wq s') th'"
+      with nd and eq_dp have "th1 \<noteq> th"
+        by (auto simp:eq_depend cs_dependents_def s_dependents_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> dependents (wq s) th')) = 
+                     ((\<lambda>th. preced th s') ` ({th'} \<union> dependents (wq s') th'))" 
+    by (auto simp:image_def)
+  thus "Max ((\<lambda>th. preced th s) ` ({th'} \<union> dependents (wq s) th')) =
+        Max ((\<lambda>th. preced th s') ` ({th'} \<union> dependents (wq s') th'))" by simp
+qed
+
+end
+end
+