theory Invoke_C

lemma setDomain_ccorres:
  "ccorres dc xfdc
      (invs' and tcb_at' t and sch_act_simple
             and (\<lambda>s. d \<le> maxDomain))
      (UNIV \<inter> {s. tptr_' s = tcb_ptr_to_ctcb_ptr t} \<inter> {s. dom_' s = ucast d})
      [] (setDomain t d) (Call setDomain_'proc)" apply (rule ccorres_gen_asm) apply (cinit lift: tptr_' dom_') apply (rule ccorres_pre_getCurThread) apply (ctac(no_vcg) add: tcbSchedDequeue_ccorres) apply (rule ccorres_move_c_guard_tcb) apply (rule ccorres_split_nothrow_novcg_dc) apply (rule threadSet_ccorres_lemma2[where P=\<top>]) apply vcg apply clarsimp apply (erule(1) rf_sr_tcb_update_no_queue2,
              (simp add: typ_heap_simps')+, simp_all?)[1] apply (rule ball_tcb_cte_casesI, simp+) apply (simp add: ctcb_relation_def) apply (ctac(no_vcg) add: isRunnable_ccorres) apply (rule ccorres_split_nothrow_novcg_dc) apply (simp add: when_def to_bool_def del: Collect_const) apply (rule ccorres_cond2[where R=\<top>], simp add: Collect_const_mem) apply (ctac add: tcbSchedEnqueue_ccorres) apply (rule ccorres_return_Skip) apply (simp add: when_def) apply (rule_tac R="\<lambda>s. curThread = ksCurThread s"
                    in ccorres_cond2) apply (clarsimp simp: rf_sr_ksCurThread) apply (ctac add: rescheduleRequired_ccorres) apply (rule ccorres_return_Skip') apply simp apply (wp hoare_drop_imps weak_sch_act_wf_lift_linear) apply (simp add: guard_is_UNIV_def) apply simp apply wp apply (rule_tac Q="\<lambda>_. all_invs_but_sch_extra and tcb_at' t and sch_act_simple
                            and (\<lambda>s. curThread = ksCurThread s)"
              in hoare_strengthen_post) apply (wp threadSet_all_invs_but_sch_extra) apply (clarsimp simp: valid_pspace_valid_objs' st_tcb_at_def[symmetric]
                           sch_act_simple_def st_tcb_at'_def weak_sch_act_wf_def
                    split: if_splits) apply (simp add: guard_is_UNIV_def) apply (rule_tac Q="\<lambda>_. invs' and tcb_at' t and sch_act_simple
                          and (\<lambda>s. curThread = ksCurThread s \<and> (\<forall>p. t \<notin> set (ksReadyQueues s p)))"
            in hoare_strengthen_post) apply (wp weak_sch_act_wf_lift_linear tcbSchedDequeue_not_queued
              tcbSchedDequeue_not_in_queue hoare_vcg_imp_lift hoare_vcg_all_lift) apply (clarsimp simp: invs'_def valid_pspace'_def valid_state'_def) apply (fastforce simp: valid_tcb'_def tcb_cte_cases_def
                         invs'_def valid_state'_def valid_pspace'_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. ccorres dc xfdc (invs' and tcb_at' t and sch_act_simple and (\<lambda>s. d \<le> maxDomain)) (UNIV \<inter> \<lbrace>\<acute>tptr = tcb_ptr_to_ctcb_ptr t\<rbrace> \<inter> \<lbrace>\<acute>dom = UCAST(8 \<rightarrow> 32) d\<rbrace>) [] (setDomain t d) (Call setDomain_'proc) proof (prove)
goal (1 subgoal):
 1. d \<le> maxDomain \<Longrightarrow> ccorres dc xfdc (invs' and tcb_at' t and sch_act_simple) (UNIV \<inter> \<lbrace>\<acute>tptr = tcb_ptr_to_ctcb_ptr t\<rbrace> \<inter> \<lbrace>\<acute>dom = UCAST(8 \<rightarrow> 32) d\<rbrace>) [] (setDomain t d) (Call setDomain_'proc) proof (prove)
goal (2 subgoals):
 1. \<And>dom tptr. \<lbrakk>d \<le> maxDomain; dom = UCAST(8 \<rightarrow> 32) d; tptr = tcb_ptr_to_ctcb_ptr t\<rbrakk> \<Longrightarrow> ccorres dc xfdc (?Q333 dom tptr) (?Q'333 dom tptr) [SKIP] (do curThread <- getCurThread;
y <- tcbSchedDequeue t;
y <- threadSet (tcbDomain_update (\<lambda>_. d)) t;
runnable <- isRunnable t;
y <- when runnable (tcbSchedEnqueue t);
when (t = curThread) rescheduleRequired
od) (CALL tcbSchedDequeue_'proc(tptr);;
(Guard C_Guard {s. s \<Turnstile>\<^sub>c tptr} (\<acute>globals :== t_hrs_'_update (hrs_mem_update (heap_update (PTR(32 word) &(tptr\<rightarrow>[''tcbDomain_C''])) dom)));;
(\<acute>ret__unsigned_long :== CALL isRunnable_'proc(tptr);;
(IF \<acute>ret__unsigned_long \<noteq> 0 THEN
  CALL tcbSchedEnqueue_'proc(tptr)
FI;;
IF tptr = \<acute>ksCurThread THEN
  CALL rescheduleRequired_'proc()
FI))))
 2. \<And>dom tptr s s'. \<lbrakk>d \<le> maxDomain; dom = UCAST(8 \<rightarrow> 32) d; tptr = tcb_ptr_to_ctcb_ptr t; (s, s') \<in> rf_sr; (invs' and tcb_at' t and sch_act_simple) s; s' \<in> UNIV\<rbrakk> \<Longrightarrow> ?Q333 dom tptr s \<and> s' \<in> ?Q'333 dom tptr proof (prove)
goal (2 subgoals):
 1. \<And>dom tptr curThread. \<lbrakk>d \<le> maxDomain; dom = UCAST(8 \<rightarrow> 32) d; tptr = tcb_ptr_to_ctcb_ptr t\<rbrakk> \<Longrightarrow> ccorres dc xfdc (?P339 dom tptr curThread) (?P'339 dom tptr curThread) [SKIP] (do y <- tcbSchedDequeue t;
y <- threadSet (tcbDomain_update (\<lambda>_. d)) t;
runnable <- isRunnable t;
y <- when runnable (tcbSchedEnqueue t);
when (t = curThread) rescheduleRequired
od) (CALL tcbSchedDequeue_'proc(tptr);;
(Guard C_Guard {s. s \<Turnstile>\<^sub>c tptr} (\<acute>globals :== t_hrs_'_update (hrs_mem_update (heap_update (PTR(32 word) &(tptr\<rightarrow>[''tcbDomain_C''])) dom)));;
(\<acute>ret__unsigned_long :== CALL isRunnable_'proc(tptr);;
(IF \<acute>ret__unsigned_long \<noteq> 0 THEN
  CALL tcbSchedEnqueue_'proc(tptr)
FI;;
IF tptr = \<acute>ksCurThread THEN
  CALL rescheduleRequired_'proc()
FI))))
 2. \<And>dom tptr s s'. \<lbrakk>d \<le> maxDomain; dom = UCAST(8 \<rightarrow> 32) d; tptr = tcb_ptr_to_ctcb_ptr t; (s, s') \<in> rf_sr; (invs' and tcb_at' t and sch_act_simple) s; s' \<in> UNIV\<rbrakk> \<Longrightarrow> (\<forall>rv. ksCurThread s = rv \<longrightarrow> ?P339 dom tptr rv s) \<and> s' \<in> {s. \<forall>rv. ksCurThread_' (globals s) = tcb_ptr_to_ctcb_ptr rv \<longrightarrow> s \<in> ?P'339 dom tptr rv} proof (prove)
goal (3 subgoals):
 1. \<And>dom tptr curThread rv xfdca. \<lbrakk>d \<le> maxDomain; dom = UCAST(8 \<rightarrow> 32) d; tptr = tcb_ptr_to_ctcb_ptr t; dc rv xfdca\<rbrakk> \<Longrightarrow> ccorres dc xfdc (?Q343 dom tptr curThread rv) (?Q'343 dom tptr curThread rv xfdca) [SKIP] (do y <- threadSet (tcbDomain_update (\<lambda>_. d)) t;
runnable <- isRunnable t;
y <- when runnable (tcbSchedEnqueue t);
when (t = curThread) rescheduleRequired
od) (Guard C_Guard {s. s \<Turnstile>\<^sub>c tptr} (\<acute>globals :== t_hrs_'_update (hrs_mem_update (heap_update (PTR(32 word) &(tptr\<rightarrow>[''tcbDomain_C''])) dom)));;
(\<acute>ret__unsigned_long :== CALL isRunnable_'proc(tptr);;
(IF \<acute>ret__unsigned_long \<noteq> 0 THEN
  CALL tcbSchedEnqueue_'proc(tptr)
FI;;
IF tptr = \<acute>ksCurThread THEN
  CALL rescheduleRequired_'proc()
FI)))
 2. \<And>dom tptr curThread. \<lbrakk>d \<le> maxDomain; dom = UCAST(8 \<rightarrow> 32) d; tptr = tcb_ptr_to_ctcb_ptr t\<rbrakk> \<Longrightarrow> \<lbrace>?R343 dom tptr curThread\<rbrace> tcbSchedDequeue t \<lbrace>?Q343 dom tptr curThread\<rbrace>
 3. \<And>dom tptr s s'. \<lbrakk>d \<le> maxDomain; dom = UCAST(8 \<rightarrow> 32) d; tptr = tcb_ptr_to_ctcb_ptr t; (s, s') \<in> rf_sr; (invs' and tcb_at' t and sch_act_simple) s; s' \<in> UNIV\<rbrakk> \<Longrightarrow> (\<forall>rv. ksCurThread s = rv \<longrightarrow> (Invariants_H.valid_queues and valid_queues' and tcb_at' t and valid_objs' and ?R343 dom tptr rv) s) \<and> s' \<in> {s. \<forall>rv. ksCurThread_' (globals s) = tcb_ptr_to_ctcb_ptr rv \<longrightarrow> s \<in> {s. tcb_'_update (\<lambda>_. tptr) s \<in> UNIV \<inter> \<lbrace>\<acute>tcb = tcb_ptr_to_ctcb_ptr t\<rbrace>} \<inter> {s'. \<forall>t rva. dc rva (xfdc t) \<longrightarrow> s'\<lparr>globals := globals t\<rparr> \<in> ?Q'343 dom tptr rv rva (xfdc t)}} proof (prove)
goal (3 subgoals):
 1. \<And>dom tptr curThread rv xfdca. \<lbrakk>d \<le> maxDomain; dom = UCAST(8 \<rightarrow> 32) d; tptr = tcb_ptr_to_ctcb_ptr t; dc rv xfdca\<rbrakk> \<Longrightarrow> ccorres dc xfdc (?A367 dom tptr curThread rv) (?C'366 dom tptr curThread rv xfdca) [SKIP] (do y <- threadSet (tcbDomain_update (\<lambda>_. d)) t;
runnable <- isRunnable t;
y <- when runnable (tcbSchedEnqueue t);
when (t = curThread) rescheduleRequired
od) (\<acute>globals :== t_hrs_'_update (hrs_mem_update (heap_update (PTR(32 word) &(tptr\<rightarrow>[''tcbDomain_C''])) dom));;
(\<acute>ret__unsigned_long :== CALL isRunnable_'proc(tptr);;
(IF \<acute>ret__unsigned_long \<noteq> 0 THEN
  CALL tcbSchedEnqueue_'proc(tptr)
FI;;
IF tptr = \<acute>ksCurThread THEN
  CALL rescheduleRequired_'proc()
FI)))
 2. \<And>dom tptr curThread. \<lbrakk>d \<le> maxDomain; dom = UCAST(8 \<rightarrow> 32) d; tptr = tcb_ptr_to_ctcb_ptr t\<rbrakk> \<Longrightarrow> \<lbrace>?R343 dom tptr curThread\<rbrace> tcbSchedDequeue t \<lbrace>\<lambda>rv. ?A367 dom tptr curThread rv and tcb_at' (ctcb_ptr_to_tcb_ptr tptr)\<rbrace>
 3. \<And>dom tptr s s'. \<lbrakk>d \<le> maxDomain; dom = UCAST(8 \<rightarrow> 32) d; tptr = tcb_ptr_to_ctcb_ptr t; (s, s') \<in> rf_sr; (invs' and tcb_at' t and sch_act_simple) s; s' \<in> UNIV\<rbrakk> \<Longrightarrow> (\<forall>rv. ksCurThread s = rv \<longrightarrow> (Invariants_H.valid_queues and valid_queues' and tcb_at' t and valid_objs' and ?R343 dom tptr rv) s) \<and> s' \<in> {s. \<forall>rv. ksCurThread_' (globals s) = tcb_ptr_to_ctcb_ptr rv \<longrightarrow> s \<in> {s. tcb_'_update (\<lambda>_. tptr) s \<in> UNIV \<inter> \<lbrace>\<acute>tcb = tcb_ptr_to_ctcb_ptr t\<rbrace>} \<inter> {s'. \<forall>t rva. dc rva (xfdc t) \<longrightarrow> s'\<lparr>globals := globals t\<rparr> \<in> ?C'366 dom tptr rv rva (xfdc t) \<inter> \<lbrace>True\<rbrace>}} proof (prove)
goal (6 subgoals):
 1. \<And>dom tptr curThread rv xfdca. \<lbrakk>d \<le> maxDomain; dom = UCAST(8 \<rightarrow> 32) d; tptr = tcb_ptr_to_ctcb_ptr t; dc rv xfdca\<rbrakk> \<Longrightarrow> ccorres dc xfdc (?P371 dom tptr curThread rv) (?C'366 dom tptr curThread rv xfdca) [] (threadSet (tcbDomain_update (\<lambda>_. d)) t) (\<acute>globals :== t_hrs_'_update (hrs_mem_update (heap_update (PTR(32 word) &(tptr\<rightarrow>[''tcbDomain_C''])) dom)))
 2. \<And>dom tptr curThread rv xfdca y rv'. \<lbrakk>d \<le> maxDomain; dom = UCAST(8 \<rightarrow> 32) d; tptr = tcb_ptr_to_ctcb_ptr t; dc rv xfdca; dc y rv'\<rbrakk> \<Longrightarrow> ccorres dc xfdc (?Q370 dom tptr curThread rv xfdca y) (?Q'370 dom tptr curThread rv xfdca y rv') [SKIP] (do runnable <- isRunnable t;
y <- when runnable (tcbSchedEnqueue t);
when (t = curThread) rescheduleRequired
od) (\<acute>ret__unsigned_long :== CALL isRunnable_'proc(tptr);;
(IF \<acute>ret__unsigned_long \<noteq> 0 THEN
  CALL tcbSchedEnqueue_'proc(tptr)
FI;;
IF tptr = \<acute>ksCurThread THEN
  CALL rescheduleRequired_'proc()
FI))
 3. \<And>dom tptr curThread rv xfdc. \<lbrakk>d \<le> maxDomain; dom = UCAST(8 \<rightarrow> 32) d; tptr = tcb_ptr_to_ctcb_ptr t; dc rv xfdc\<rbrakk> \<Longrightarrow> \<lbrace>?R372 dom tptr curThread rv\<rbrace> threadSet (tcbDomain_update (\<lambda>_. d)) t \<lbrace>?Q370 dom tptr curThread rv xfdc\<rbrace>
 4. \<And>dom tptr curThread rv xfdca. \<lbrakk>d \<le> maxDomain; dom = UCAST(8 \<rightarrow> 32) d; tptr = tcb_ptr_to_ctcb_ptr t; dc rv xfdca\<rbrakk> \<Longrightarrow> guard_is_UNIV dc xfdc (?Q'370 dom tptr curThread rv xfdca)
 5. \<And>dom tptr curThread. \<lbrakk>d \<le> maxDomain; dom = UCAST(8 \<rightarrow> 32) d; tptr = tcb_ptr_to_ctcb_ptr t\<rbrakk> \<Longrightarrow> \<lbrace>?R343 dom tptr curThread\<rbrace> tcbSchedDequeue t \<lbrace>\<lambda>rv. ?P371 dom tptr curThread rv and ?R372 dom tptr curThread rv and tcb_at' (ctcb_ptr_to_tcb_ptr tptr)\<rbrace>
 6. \<And>dom tptr s s'. \<lbrakk>d \<le> maxDomain; dom = UCAST(8 \<rightarrow> 32) d; tptr = tcb_ptr_to_ctcb_ptr t; (s, s') \<in> rf_sr; (invs' and tcb_at' t and sch_act_simple) s; s' \<in> UNIV\<rbrakk> \<Longrightarrow> (\<forall>rv. ksCurThread s = rv \<longrightarrow> (Invariants_H.valid_queues and valid_queues' and tcb_at' t and valid_objs' and ?R343 dom tptr rv) s) \<and> s' \<in> {s. \<forall>rv. ksCurThread_' (globals s) = tcb_ptr_to_ctcb_ptr rv \<longrightarrow> s \<in> {s. tcb_'_update (\<lambda>_. tptr) s \<in> UNIV \<inter> \<lbrace>\<acute>tcb = tcb_ptr_to_ctcb_ptr t\<rbrace>} \<inter> {s'. \<forall>t rva. dc rva (xfdc t) \<longrightarrow> s'\<lparr>globals := globals t\<rparr> \<in> ?C'366 dom tptr rv rva (xfdc t) \<inter> \<lbrace>True\<rbrace>}} proof (prove)
goal (7 subgoals):
 1. \<And>dom tptr curThread rv xfdc s tcb. \<lbrakk>d \<le> maxDomain; dom = UCAST(8 \<rightarrow> 32) d; tptr = tcb_ptr_to_ctcb_ptr t; dc rv xfdc\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile> (?Q377 dom tptr curThread rv xfdc s tcb) \<acute>globals :== t_hrs_'_update (hrs_mem_update (heap_update (PTR(32 word) &(tptr\<rightarrow>[''tcbDomain_C''])) dom)) {s'. (s\<lparr>ksPSpace := (ksPSpace s)(t \<mapsto> injectKOS (tcbDomain_update (\<lambda>_. d) tcb))\<rparr>, s') \<in> rf_sr}
 2. \<And>dom tptr curThread rv xfdc s s' tcb tcb'. \<lbrakk>d \<le> maxDomain; dom = UCAST(8 \<rightarrow> 32) d; tptr = tcb_ptr_to_ctcb_ptr t; dc rv xfdc; (s, s') \<in> rf_sr; True; ko_at' tcb t s; cslift s' (tcb_ptr_to_ctcb_ptr t) = Some tcb'; ctcb_relation tcb tcb'; True; s' \<in> UNIV\<rbrakk> \<Longrightarrow> s' \<in> ?Q377 dom tptr curThread rv xfdc s tcb
 3. \<And>dom tptr curThread rv xfdca y rv'. \<lbrakk>d \<le> maxDomain; dom = UCAST(8 \<rightarrow> 32) d; tptr = tcb_ptr_to_ctcb_ptr t; dc rv xfdca; dc y rv'\<rbrakk> \<Longrightarrow> ccorres dc xfdc (?Q370 dom tptr curThread rv xfdca y) (?Q'370 dom tptr curThread rv xfdca y rv') [SKIP] (do runnable <- isRunnable t;
y <- when runnable (tcbSchedEnqueue t);
when (t = curThread) rescheduleRequired
od) (\<acute>ret__unsigned_long :== CALL isRunnable_'proc(tptr);;
(IF \<acute>ret__unsigned_long \<noteq> 0 THEN
  CALL tcbSchedEnqueue_'proc(tptr)
FI;;
IF tptr = \<acute>ksCurThread THEN
  CALL rescheduleRequired_'proc()
FI))
 4. \<And>dom tptr curThread rv xfdc. \<lbrakk>d \<le> maxDomain; dom = UCAST(8 \<rightarrow> 32) d; tptr = tcb_ptr_to_ctcb_ptr t; dc rv xfdc\<rbrakk> \<Longrightarrow> \<lbrace>?R372 dom tptr curThread rv\<rbrace> threadSet (tcbDomain_update (\<lambda>_. d)) t \<lbrace>?Q370 dom tptr curThread rv xfdc\<rbrace>
 5. \<And>dom tptr curThread rv xfdca. \<lbrakk>d \<le> maxDomain; dom = UCAST(8 \<rightarrow> 32) d; tptr = tcb_ptr_to_ctcb_ptr t; dc rv xfdca\<rbrakk> \<Longrightarrow> guard_is_UNIV dc xfdc (?Q'370 dom tptr curThread rv xfdca)
 6. \<And>dom tptr curThread. \<lbrakk>d \<le> maxDomain; dom = UCAST(8 \<rightarrow> 32) d; tptr = tcb_ptr_to_ctcb_ptr t\<rbrakk> \<Longrightarrow> \<lbrace>?R343 dom tptr curThread\<rbrace> tcbSchedDequeue t \<lbrace>\<lambda>rv. tcb_at' t and (\<lambda>_. True) and ?R372 dom tptr curThread rv and tcb_at' (ctcb_ptr_to_tcb_ptr tptr)\<rbrace>
 7. \<And>dom tptr s s'. \<lbrakk>d \<le> maxDomain; dom = UCAST(8 \<rightarrow> 32) d; tptr = tcb_ptr_to_ctcb_ptr t; (s, s') \<in> rf_sr; (invs' and tcb_at' t and sch_act_simple) s; s' \<in> UNIV\<rbrakk> \<Longrightarrow> (\<forall>rv. ksCurThread s = rv \<longrightarrow> (Invariants_H.valid_queues and valid_queues' and tcb_at' t and valid_objs' and ?R343 dom tptr rv) s) \<and> s' \<in> {s. \<forall>rv. ksCurThread_' (globals s) = tcb_ptr_to_ctcb_ptr rv \<longrightarrow> s \<in> {s. tcb_'_update (\<lambda>_. tptr) s \<in> UNIV \<inter> \<lbrace>\<acute>tcb = tcb_ptr_to_ctcb_ptr t\<rbrace>} \<inter> {s'. \<forall>t rv. dc rv (xfdc t) \<longrightarrow> s'\<lparr>globals := globals t\<rparr> \<in> UNIV \<inter> \<lbrace>True\<rbrace>}} proof (prove)
goal (6 subgoals):
 1. \<And>dom tptr curThread rv xfdc s s' tcb tcb'. \<lbrakk>d \<le> maxDomain; dom = UCAST(8 \<rightarrow> 32) d; tptr = tcb_ptr_to_ctcb_ptr t; dc rv xfdc; (s, s') \<in> rf_sr; True; ko_at' tcb t s; cslift s' (tcb_ptr_to_ctcb_ptr t) = Some tcb'; ctcb_relation tcb tcb'; True; s' \<in> UNIV\<rbrakk> \<Longrightarrow> s' \<in> {sa. (s\<lparr>ksPSpace := (ksPSpace s)(t \<mapsto> injectKOS (tcbDomain_update (\<lambda>_. d) tcb))\<rparr>, globals_update (t_hrs_'_update (hrs_mem_update (heap_update (PTR(32 word) &(tptr\<rightarrow>[''tcbDomain_C''])) dom))) sa) \<in> rf_sr}
 2. \<And>dom tptr curThread rv xfdca y rv'. \<lbrakk>d \<le> maxDomain; dom = UCAST(8 \<rightarrow> 32) d; tptr = tcb_ptr_to_ctcb_ptr t; dc rv xfdca; dc y rv'\<rbrakk> \<Longrightarrow> ccorres dc xfdc (?Q370 dom tptr curThread rv xfdca y) (?Q'370 dom tptr curThread rv xfdca y rv') [SKIP] (do runnable <- isRunnable t;
y <- when runnable (tcbSchedEnqueue t);
when (t = curThread) rescheduleRequired
od) (\<acute>ret__unsigned_long :== CALL isRunnable_'proc(tptr);;
(IF \<acute>ret__unsigned_long \<noteq> 0 THEN
  CALL tcbSchedEnqueue_'proc(tptr)
FI;;
IF tptr = \<acute>ksCurThread THEN
  CALL rescheduleRequired_'proc()
FI))
 3. \<And>dom tptr curThread rv xfdc. \<lbrakk>d \<le> maxDomain; dom = UCAST(8 \<rightarrow> 32) d; tptr = tcb_ptr_to_ctcb_ptr t; dc rv xfdc\<rbrakk> \<Longrightarrow> \<lbrace>?R372 dom tptr curThread rv\<rbrace> threadSet (tcbDomain_update (\<lambda>_. d)) t \<lbrace>?Q370 dom tptr curThread rv xfdc\<rbrace>
 4. \<And>dom tptr curThread rv xfdca. \<lbrakk>d \<le> maxDomain; dom = UCAST(8 \<rightarrow> 32) d; tptr = tcb_ptr_to_ctcb_ptr t; dc rv xfdca\<rbrakk> \<Longrightarrow> guard_is_UNIV dc xfdc (?Q'370 dom tptr curThread rv xfdca)
 5. \<And>dom tptr curThread. \<lbrakk>d \<le> maxDomain; dom = UCAST(8 \<rightarrow> 32) d; tptr = tcb_ptr_to_ctcb_ptr t\<rbrakk> \<Longrightarrow> \<lbrace>?R343 dom tptr curThread\<rbrace> tcbSchedDequeue t \<lbrace>\<lambda>rv. tcb_at' t and (\<lambda>_. True) and ?R372 dom tptr curThread rv and tcb_at' (ctcb_ptr_to_tcb_ptr tptr)\<rbrace>
 6. \<And>dom tptr s s'. \<lbrakk>d \<le> maxDomain; dom = UCAST(8 \<rightarrow> 32) d; tptr = tcb_ptr_to_ctcb_ptr t; (s, s') \<in> rf_sr; (invs' and tcb_at' t and sch_act_simple) s; s' \<in> UNIV\<rbrakk> \<Longrightarrow> (\<forall>rv. ksCurThread s = rv \<longrightarrow> (Invariants_H.valid_queues and valid_queues' and tcb_at' t and valid_objs' and ?R343 dom tptr rv) s) \<and> s' \<in> {s. \<forall>rv. ksCurThread_' (globals s) = tcb_ptr_to_ctcb_ptr rv \<longrightarrow> s \<in> {s. tcb_'_update (\<lambda>_. tptr) s \<in> UNIV \<inter> \<lbrace>\<acute>tcb = tcb_ptr_to_ctcb_ptr t\<rbrace>} \<inter> {s'. \<forall>t rv. dc rv (xfdc t) \<longrightarrow> s'\<lparr>globals := globals t\<rparr> \<in> UNIV \<inter> \<lbrace>True\<rbrace>}} proof (prove)
goal (6 subgoals):
 1. \<And>s s' tcb tcb'. \<lbrakk>d \<le> maxDomain; (s, s') \<in> rf_sr; ko_at' tcb t s; cslift s' (tcb_ptr_to_ctcb_ptr t) = Some tcb'; ctcb_relation tcb tcb'\<rbrakk> \<Longrightarrow> (s\<lparr>ksPSpace := (ksPSpace s)(t \<mapsto> KOTCB (tcbDomain_update (\<lambda>_. d) tcb))\<rparr>, globals_update (t_hrs_'_update (hrs_mem_update (heap_update (PTR(32 word) &(tcb_ptr_to_ctcb_ptr t\<rightarrow>[''tcbDomain_C''])) (UCAST(8 \<rightarrow> 32) d)))) s') \<in> rf_sr
 2. \<And>dom tptr curThread rv xfdca y rv'. \<lbrakk>d \<le> maxDomain; dom = UCAST(8 \<rightarrow> 32) d; tptr = tcb_ptr_to_ctcb_ptr t; dc rv xfdca; dc y rv'\<rbrakk> \<Longrightarrow> ccorres dc xfdc (?Q370 dom tptr curThread rv xfdca y) (?Q'370 dom tptr curThread rv xfdca y rv') [SKIP] (do runnable <- isRunnable t;
y <- when runnable (tcbSchedEnqueue t);
when (t = curThread) rescheduleRequired
od) (\<acute>ret__unsigned_long :== CALL isRunnable_'proc(tptr);;
(IF \<acute>ret__unsigned_long \<noteq> 0 THEN
  CALL tcbSchedEnqueue_'proc(tptr)
FI;;
IF tptr = \<acute>ksCurThread THEN
  CALL rescheduleRequired_'proc()
FI))
 3. \<And>dom tptr curThread rv xfdc. \<lbrakk>d \<le> maxDomain; dom = UCAST(8 \<rightarrow> 32) d; tptr = tcb_ptr_to_ctcb_ptr t; dc rv xfdc\<rbrakk> \<Longrightarrow> \<lbrace>?R372 dom tptr curThread rv\<rbrace> threadSet (tcbDomain_update (\<lambda>_. d)) t \<lbrace>?Q370 dom tptr curThread rv xfdc\<rbrace>
 4. \<And>dom tptr curThread rv xfdca. \<lbrakk>d \<le> maxDomain; dom = UCAST(8 \<rightarrow> 32) d; tptr = tcb_ptr_to_ctcb_ptr t; dc rv xfdca\<rbrakk> \<Longrightarrow> guard_is_UNIV dc xfdc (?Q'370 dom tptr curThread rv xfdca)
 5. \<And>dom tptr curThread. \<lbrakk>d \<le> maxDomain; dom = UCAST(8 \<rightarrow> 32) d; tptr = tcb_ptr_to_ctcb_ptr t\<rbrakk> \<Longrightarrow> \<lbrace>?R343 dom tptr curThread\<rbrace> tcbSchedDequeue t \<lbrace>\<lambda>rv. tcb_at' t and (\<lambda>_. True) and ?R372 dom tptr curThread rv and tcb_at' (ctcb_ptr_to_tcb_ptr tptr)\<rbrace>
 6. \<And>dom tptr s s'. \<lbrakk>d \<le> maxDomain; dom = UCAST(8 \<rightarrow> 32) d; tptr = tcb_ptr_to_ctcb_ptr t; (s, s') \<in> rf_sr; (invs' and tcb_at' t and sch_act_simple) s; s' \<in> UNIV\<rbrakk> \<Longrightarrow> (\<forall>rv. ksCurThread s = rv \<longrightarrow> (Invariants_H.valid_queues and valid_queues' and tcb_at' t and valid_objs' and ?R343 dom tptr rv) s) \<and> s' \<in> {s. \<forall>rv. ksCurThread_' (globals s) = tcb_ptr_to_ctcb_ptr rv \<longrightarrow> s \<in> {s. tcb_'_update (\<lambda>_. tptr) s \<in> UNIV \<inter> \<lbrace>\<acute>tcb = tcb_ptr_to_ctcb_ptr t\<rbrace>} \<inter> {s'. \<forall>t rv. dc rv (xfdc t) \<longrightarrow> s'\<lparr>globals := globals t\<rparr> \<in> UNIV \<inter> \<lbrace>True\<rbrace>}} proof (prove)
goal (7 subgoals):
 1. \<And>s s' tcb tcb'. \<lbrakk>d \<le> maxDomain; ko_at' tcb t s; cslift s' (tcb_ptr_to_ctcb_ptr t) = Some tcb'; ctcb_relation tcb tcb'\<rbrakk> \<Longrightarrow> \<forall>x\<in>ran tcb_cte_cases. case x of (getF, setF) \<Rightarrow> getF (tcbDomain_update (\<lambda>_. d) tcb) = getF tcb
 2. \<And>s s' tcb tcb'. \<lbrakk>d \<le> maxDomain; ko_at' tcb t s; cslift s' (tcb_ptr_to_ctcb_ptr t) = Some tcb'; ctcb_relation tcb tcb'\<rbrakk> \<Longrightarrow> ctcb_relation (tcbDomain_update (\<lambda>_. d) tcb) (tcbDomain_C_update (\<lambda>_. UCAST(8 \<rightarrow> 32) d) tcb')
 3. \<And>dom tptr curThread rv xfdca y rv'. \<lbrakk>d \<le> maxDomain; dom = UCAST(8 \<rightarrow> 32) d; tptr = tcb_ptr_to_ctcb_ptr t; dc rv xfdca; dc y rv'\<rbrakk> \<Longrightarrow> ccorres dc xfdc (?Q370 dom tptr curThread rv xfdca y) (?Q'370 dom tptr curThread rv xfdca y rv') [SKIP] (do runnable <- isRunnable t;
y <- when runnable (tcbSchedEnqueue t);
when (t = curThread) rescheduleRequired
od) (\<acute>ret__unsigned_long :== CALL isRunnable_'proc(tptr);;
(IF \<acute>ret__unsigned_long \<noteq> 0 THEN
  CALL tcbSchedEnqueue_'proc(tptr)
FI;;
IF tptr = \<acute>ksCurThread THEN
  CALL rescheduleRequired_'proc()
FI))
 4. \<And>dom tptr curThread rv xfdc. \<lbrakk>d \<le> maxDomain; dom = UCAST(8 \<rightarrow> 32) d; tptr = tcb_ptr_to_ctcb_ptr t; dc rv xfdc\<rbrakk> \<Longrightarrow> \<lbrace>?R372 dom tptr curThread rv\<rbrace> threadSet (tcbDomain_update (\<lambda>_. d)) t \<lbrace>?Q370 dom tptr curThread rv xfdc\<rbrace>
 5. \<And>dom tptr curThread rv xfdca. \<lbrakk>d \<le> maxDomain; dom = UCAST(8 \<rightarrow> 32) d; tptr = tcb_ptr_to_ctcb_ptr t; dc rv xfdca\<rbrakk> \<Longrightarrow> guard_is_UNIV dc xfdc (?Q'370 dom tptr curThread rv xfdca)
 6. \<And>dom tptr curThread. \<lbrakk>d \<le> maxDomain; dom = UCAST(8 \<rightarrow> 32) d; tptr = tcb_ptr_to_ctcb_ptr t\<rbrakk> \<Longrightarrow> \<lbrace>?R343 dom tptr curThread\<rbrace> tcbSchedDequeue t \<lbrace>\<lambda>rv. tcb_at' t and (\<lambda>_. True) and ?R372 dom tptr curThread rv and tcb_at' (ctcb_ptr_to_tcb_ptr tptr)\<rbrace>
 7. \<And>dom tptr s s'. \<lbrakk>d \<le> maxDomain; dom = UCAST(8 \<rightarrow> 32) d; tptr = tcb_ptr_to_ctcb_ptr t; (s, s') \<in> rf_sr; (invs' and tcb_at' t and sch_act_simple) s; s' \<in> UNIV\<rbrakk> \<Longrightarrow> (\<forall>rv. ksCurThread s = rv \<longrightarrow> (Invariants_H.valid_queues and valid_queues' and tcb_at' t and valid_objs' and ?R343 dom tptr rv) s) \<and> s' \<in> {s. \<forall>rv. ksCurThread_' (globals s) = tcb_ptr_to_ctcb_ptr rv \<longrightarrow> s \<in> {s. tcb_'_update (\<lambda>_. tptr) s \<in> UNIV \<inter> \<lbrace>\<acute>tcb = tcb_ptr_to_ctcb_ptr t\<rbrace>} \<inter> {s'. \<forall>t rv. dc rv (xfdc t) \<longrightarrow> s'\<lparr>globals := globals t\<rparr> \<in> UNIV \<inter> \<lbrace>True\<rbrace>}} proof (prove)
goal (6 subgoals):
 1. \<And>s s' tcb tcb'. \<lbrakk>d \<le> maxDomain; ko_at' tcb t s; cslift s' (tcb_ptr_to_ctcb_ptr t) = Some tcb'; ctcb_relation tcb tcb'\<rbrakk> \<Longrightarrow> ctcb_relation (tcbDomain_update (\<lambda>_. d) tcb) (tcbDomain_C_update (\<lambda>_. UCAST(8 \<rightarrow> 32) d) tcb')
 2. \<And>dom tptr curThread rv xfdca y rv'. \<lbrakk>d \<le> maxDomain; dom = UCAST(8 \<rightarrow> 32) d; tptr = tcb_ptr_to_ctcb_ptr t; dc rv xfdca; dc y rv'\<rbrakk> \<Longrightarrow> ccorres dc xfdc (?Q370 dom tptr curThread rv xfdca y) (?Q'370 dom tptr curThread rv xfdca y rv') [SKIP] (do runnable <- isRunnable t;
y <- when runnable (tcbSchedEnqueue t);
when (t = curThread) rescheduleRequired
od) (\<acute>ret__unsigned_long :== CALL isRunnable_'proc(tptr);;
(IF \<acute>ret__unsigned_long \<noteq> 0 THEN
  CALL tcbSchedEnqueue_'proc(tptr)
FI;;
IF tptr = \<acute>ksCurThread THEN
  CALL rescheduleRequired_'proc()
FI))
 3. \<And>dom tptr curThread rv xfdc. \<lbrakk>d \<le> maxDomain; dom = UCAST(8 \<rightarrow> 32) d; tptr = tcb_ptr_to_ctcb_ptr t; dc rv xfdc\<rbrakk> \<Longrightarrow> \<lbrace>?R372 dom tptr curThread rv\<rbrace> threadSet (tcbDomain_update (\<lambda>_. d)) t \<lbrace>?Q370 dom tptr curThread rv xfdc\<rbrace>
 4. \<And>dom tptr curThread rv xfdca. \<lbrakk>d \<le> maxDomain; dom = UCAST(8 \<rightarrow> 32) d; tptr = tcb_ptr_to_ctcb_ptr t; dc rv xfdca\<rbrakk> \<Longrightarrow> guard_is_UNIV dc xfdc (?Q'370 dom tptr curThread rv xfdca)
 5. \<And>dom tptr curThread. \<lbrakk>d \<le> maxDomain; dom = UCAST(8 \<rightarrow> 32) d; tptr = tcb_ptr_to_ctcb_ptr t\<rbrakk> \<Longrightarrow> \<lbrace>?R343 dom tptr curThread\<rbrace> tcbSchedDequeue t \<lbrace>\<lambda>rv. tcb_at' t and (\<lambda>_. True) and ?R372 dom tptr curThread rv and tcb_at' (ctcb_ptr_to_tcb_ptr tptr)\<rbrace>
 6. \<And>dom tptr s s'. \<lbrakk>d \<le> maxDomain; dom = UCAST(8 \<rightarrow> 32) d; tptr = tcb_ptr_to_ctcb_ptr t; (s, s') \<in> rf_sr; (invs' and tcb_at' t and sch_act_simple) s; s' \<in> UNIV\<rbrakk> \<Longrightarrow> (\<forall>rv. ksCurThread s = rv \<longrightarrow> (Invariants_H.valid_queues and valid_queues' and tcb_at' t and valid_objs' and ?R343 dom tptr rv) s) \<and> s' \<in> {s. \<forall>rv. ksCurThread_' (globals s) = tcb_ptr_to_ctcb_ptr rv \<longrightarrow> s \<in> {s. tcb_'_update (\<lambda>_. tptr) s \<in> UNIV \<inter> \<lbrace>\<acute>tcb = tcb_ptr_to_ctcb_ptr t\<rbrace>} \<inter> {s'. \<forall>t rv. dc rv (xfdc t) \<longrightarrow> s'\<lparr>globals := globals t\<rparr> \<in> UNIV \<inter> \<lbrace>True\<rbrace>}} proof (prove)
goal (5 subgoals):
 1. \<And>dom tptr curThread rv xfdca y rv'. \<lbrakk>d \<le> maxDomain; dom = UCAST(8 \<rightarrow> 32) d; tptr = tcb_ptr_to_ctcb_ptr t; dc rv xfdca; dc y rv'\<rbrakk> \<Longrightarrow> ccorres dc xfdc (?Q370 dom tptr curThread rv xfdca y) (?Q'370 dom tptr curThread rv xfdca y rv') [SKIP] (do runnable <- isRunnable t;
y <- when runnable (tcbSchedEnqueue t);
when (t = curThread) rescheduleRequired
od) (\<acute>ret__unsigned_long :== CALL isRunnable_'proc(tptr);;
(IF \<acute>ret__unsigned_long \<noteq> 0 THEN
  CALL tcbSchedEnqueue_'proc(tptr)
FI;;
IF tptr = \<acute>ksCurThread THEN
  CALL rescheduleRequired_'proc()
FI))
 2. \<And>dom tptr curThread rv xfdc. \<lbrakk>d \<le> maxDomain; dom = UCAST(8 \<rightarrow> 32) d; tptr = tcb_ptr_to_ctcb_ptr t; dc rv xfdc\<rbrakk> \<Longrightarrow> \<lbrace>?R372 dom tptr curThread rv\<rbrace> threadSet (tcbDomain_update (\<lambda>_. d)) t \<lbrace>?Q370 dom tptr curThread rv xfdc\<rbrace>
 3. \<And>dom tptr curThread rv xfdca. \<lbrakk>d \<le> maxDomain; dom = UCAST(8 \<rightarrow> 32) d; tptr = tcb_ptr_to_ctcb_ptr t; dc rv xfdca\<rbrakk> \<Longrightarrow> guard_is_UNIV dc xfdc (?Q'370 dom tptr curThread rv xfdca)
 4. \<And>dom tptr curThread. \<lbrakk>d \<le> maxDomain; dom = UCAST(8 \<rightarrow> 32) d; tptr = tcb_ptr_to_ctcb_ptr t\<rbrakk> \<Longrightarrow> \<lbrace>?R343 dom tptr curThread\<rbrace> tcbSchedDequeue t \<lbrace>\<lambda>rv. tcb_at' t and (\<lambda>_. True) and ?R372 dom tptr curThread rv and tcb_at' (ctcb_ptr_to_tcb_ptr tptr)\<rbrace>
 5. \<And>dom tptr s s'. \<lbrakk>d \<le> maxDomain; dom = UCAST(8 \<rightarrow> 32) d; tptr = tcb_ptr_to_ctcb_ptr t; (s, s') \<in> rf_sr; (invs' and tcb_at' t and sch_act_simple) s; s' \<in> UNIV\<rbrakk> \<Longrightarrow> (\<forall>rv. ksCurThread s = rv \<longrightarrow> (Invariants_H.valid_queues and valid_queues' and tcb_at' t and valid_objs' and ?R343 dom tptr rv) s) \<and> s' \<in> {s. \<forall>rv. ksCurThread_' (globals s) = tcb_ptr_to_ctcb_ptr rv \<longrightarrow> s \<in> {s. tcb_'_update (\<lambda>_. tptr) s \<in> UNIV \<inter> \<lbrace>\<acute>tcb = tcb_ptr_to_ctcb_ptr t\<rbrace>} \<inter> {s'. \<forall>t rv. dc rv (xfdc t) \<longrightarrow> s'\<lparr>globals := globals t\<rparr> \<in> UNIV \<inter> \<lbrace>True\<rbrace>}} proof (prove)
goal (6 subgoals):
 1. \<And>dom tptr curThread rv xfdca y rv' rva ret__unsigned_long. \<lbrakk>d \<le> maxDomain; dom = UCAST(8 \<rightarrow> 32) d; tptr = tcb_ptr_to_ctcb_ptr t; dc rv xfdca; dc y rv'; rva = to_bool ret__unsigned_long\<rbrakk> \<Longrightarrow> ccorres dc xfdc (?Q409 dom tptr curThread rv xfdca y rv' rva) (?Q'409 dom tptr curThread rv xfdca y rv' rva ret__unsigned_long) [SKIP] (do y <- when rva (tcbSchedEnqueue t);
when (t = curThread) rescheduleRequired
od) (IF ret__unsigned_long \<noteq> 0 THEN
  CALL tcbSchedEnqueue_'proc(tptr)
FI;;
IF tptr = \<acute>ksCurThread THEN
  CALL rescheduleRequired_'proc()
FI)
 2. \<And>dom tptr curThread rv xfdc y rv'. \<lbrakk>d \<le> maxDomain; dom = UCAST(8 \<rightarrow> 32) d; tptr = tcb_ptr_to_ctcb_ptr t; dc rv xfdc; dc y rv'\<rbrakk> \<Longrightarrow> \<lbrace>?R411 dom tptr curThread rv xfdc y\<rbrace> isRunnable t \<lbrace>?Q409 dom tptr curThread rv xfdc y rv'\<rbrace>
 3. \<And>dom tptr curThread rv xfdc. \<lbrakk>d \<le> maxDomain; dom = UCAST(8 \<rightarrow> 32) d; tptr = tcb_ptr_to_ctcb_ptr t; dc rv xfdc\<rbrakk> \<Longrightarrow> \<lbrace>?R372 dom tptr curThread rv\<rbrace> threadSet (tcbDomain_update (\<lambda>_. d)) t \<lbrace>\<lambda>y. tcb_at' t and ?R411 dom tptr curThread rv xfdc y\<rbrace>
 4. \<And>dom tptr curThread rv xfdca. \<lbrakk>d \<le> maxDomain; dom = UCAST(8 \<rightarrow> 32) d; tptr = tcb_ptr_to_ctcb_ptr t; dc rv xfdca\<rbrakk> \<Longrightarrow> guard_is_UNIV dc xfdc (\<lambda>y rv'. {s. thread_'_update (\<lambda>_. tptr) s \<in> UNIV \<inter> \<lbrace>\<acute>thread = tcb_ptr_to_ctcb_ptr t\<rbrace>} \<inter> {s'. \<forall>t rva. rva = to_bool (ret__unsigned_long_' t) \<longrightarrow> s'\<lparr>globals := globals t, ret__unsigned_long_' := ret__unsigned_long_' t\<rparr> \<in> ?Q'409 dom tptr curThread rv xfdca y rv' rva (ret__unsigned_long_' t)})
 5. \<And>dom tptr curThread. \<lbrakk>d \<le> maxDomain; dom = UCAST(8 \<rightarrow> 32) d; tptr = tcb_ptr_to_ctcb_ptr t\<rbrakk> \<Longrightarrow> \<lbrace>?R343 dom tptr curThread\<rbrace> tcbSchedDequeue t \<lbrace>\<lambda>rv. tcb_at' t and (\<lambda>_. True) and ?R372 dom tptr curThread rv and tcb_at' (ctcb_ptr_to_tcb_ptr tptr)\<rbrace>
 6. \<And>dom tptr s s'. \<lbrakk>d \<le> maxDomain; dom = UCAST(8 \<rightarrow> 32) d; tptr = tcb_ptr_to_ctcb_ptr t; (s, s') \<in> rf_sr; (invs' and tcb_at' t and sch_act_simple) s; s' \<in> UNIV\<rbrakk> \<Longrightarrow> (\<forall>rv. ksCurThread s = rv \<longrightarrow> (Invariants_H.valid_queues and valid_queues' and tcb_at' t and valid_objs' and ?R343 dom tptr rv) s) \<and> s' \<in> {s. \<forall>rv. ksCurThread_' (globals s) = tcb_ptr_to_ctcb_ptr rv \<longrightarrow> s \<in> {s. tcb_'_update (\<lambda>_. tptr) s \<in> UNIV \<inter> \<lbrace>\<acute>tcb = tcb_ptr_to_ctcb_ptr t\<rbrace>} \<inter> {s'. \<forall>t rv. dc rv (xfdc t) \<longrightarrow> s'\<lparr>globals := globals t\<rparr> \<in> UNIV \<inter> \<lbrace>True\<rbrace>}} proof (prove)
goal (9 subgoals):
 1. \<And>dom tptr curThread rv xfdca y rv' rva ret__unsigned_long. \<lbrakk>d \<le> maxDomain; dom = UCAST(8 \<rightarrow> 32) d; tptr = tcb_ptr_to_ctcb_ptr t; dc rv xfdca; dc y rv'; rva = to_bool ret__unsigned_long\<rbrakk> \<Longrightarrow> ccorres dc xfdc (?P512 dom tptr curThread rv xfdca y rv' rva) (?Q'409 dom tptr curThread rv xfdca y rv' rva ret__unsigned_long) [] (when rva (tcbSchedEnqueue t)) (IF ret__unsigned_long \<noteq> 0 THEN
  CALL tcbSchedEnqueue_'proc(tptr)
FI)
 2. \<And>dom tptr curThread rv xfdca y rv' rva ret__unsigned_long ya rv'a. \<lbrakk>d \<le> maxDomain; dom = UCAST(8 \<rightarrow> 32) d; tptr = tcb_ptr_to_ctcb_ptr t; dc rv xfdca; dc y rv'; rva = to_bool ret__unsigned_long; dc ya rv'a\<rbrakk> \<Longrightarrow> ccorres dc xfdc (?Q511 dom tptr curThread rv xfdca y rv' rva ret__unsigned_long ya) (?Q'511 dom tptr curThread rv xfdca y rv' rva ret__unsigned_long ya rv'a) [SKIP] (when (t = curThread) rescheduleRequired) (IF tptr = \<acute>ksCurThread THEN
  CALL rescheduleRequired_'proc()
FI)
 3. \<And>dom tptr curThread rv xfdc y rv' rva ret__unsigned_long. \<lbrakk>d \<le> maxDomain; dom = UCAST(8 \<rightarrow> 32) d; tptr = tcb_ptr_to_ctcb_ptr t; dc rv xfdc; dc y rv'; rva = to_bool ret__unsigned_long\<rbrakk> \<Longrightarrow> \<lbrace>?R513 dom tptr curThread rv xfdc y rv' rva\<rbrace> when rva (tcbSchedEnqueue t) \<lbrace>?Q511 dom tptr curThread rv xfdc y rv' rva ret__unsigned_long\<rbrace>
 4. \<And>dom tptr curThread rv xfdca y rv' rva ret__unsigned_long. \<lbrakk>d \<le> maxDomain; dom = UCAST(8 \<rightarrow> 32) d; tptr = tcb_ptr_to_ctcb_ptr t; dc rv xfdca; dc y rv'; rva = to_bool ret__unsigned_long\<rbrakk> \<Longrightarrow> guard_is_UNIV dc xfdc (?Q'511 dom tptr curThread rv xfdca y rv' rva ret__unsigned_long)
 5. \<And>dom tptr curThread rv xfdc y rv'. \<lbrakk>d \<le> maxDomain; dom = UCAST(8 \<rightarrow> 32) d; tptr = tcb_ptr_to_ctcb_ptr t; dc rv xfdc; dc y rv'\<rbrakk> \<Longrightarrow> \<lbrace>?R411 dom tptr curThread rv xfdc y\<rbrace> isRunnable t \<lbrace>\<lambda>rva. ?P512 dom tptr curThread rv xfdc y rv' rva and ?R513 dom tptr curThread rv xfdc y rv' rva\<rbrace>
 6. \<And>dom tptr curThread rv xfdc. \<lbrakk>d \<le> maxDomain; dom = UCAST(8 \<rightarrow> 32) d; tptr = tcb_ptr_to_ctcb_ptr t; dc rv xfdc\<rbrakk> \<Longrightarrow> \<lbrace>?R372 dom tptr curThread rv\<rbrace> threadSet (tcbDomain_update (\<lambda>_. d)) t \<lbrace>\<lambda>y. tcb_at' t and ?R411 dom tptr curThread rv xfdc y\<rbrace>
 7. \<And>dom tptr curThread rv xfdca. \<lbrakk>d \<le> maxDomain; dom = UCAST(8 \<rightarrow> 32) d; tptr = tcb_ptr_to_ctcb_ptr t; dc rv xfdca\<rbrakk> \<Longrightarrow> guard_is_UNIV dc xfdc (\<lambda>y rv'. {s. thread_'_update (\<lambda>_. tptr) s \<in> UNIV \<inter> \<lbrace>\<acute>thread = tcb_ptr_to_ctcb_ptr t\<rbrace>} \<inter> {s'. \<forall>t rva. rva = to_bool (ret__unsigned_long_' t) \<longrightarrow> s'\<lparr>globals := globals t, ret__unsigned_long_' := ret__unsigned_long_' t\<rparr> \<in> ?Q'409 dom tptr curThread rv xfdca y rv' rva (ret__unsigned_long_' t)})
 8. \<And>dom tptr curThread. \<lbrakk>d \<le> maxDomain; dom = UCAST(8 \<rightarrow> 32) d; tptr = tcb_ptr_to_ctcb_ptr t\<rbrakk> \<Longrightarrow> \<lbrace>?R343 dom tptr curThread\<rbrace> tcbSchedDequeue t \<lbrace>\<lambda>rv. tcb_at' t and (\<lambda>_. True) and ?R372 dom tptr curThread rv and tcb_at' (ctcb_ptr_to_tcb_ptr tptr)\<rbrace>
 9. \<And>dom tptr s s'. \<lbrakk>d \<le> maxDomain; dom = UCAST(8 \<rightarrow> 32) d; tptr = tcb_ptr_to_ctcb_ptr t; (s, s') \<in> rf_sr; (invs' and tcb_at' t and sch_act_simple) s; s' \<in> UNIV\<rbrakk> \<Longrightarrow> (\<forall>rv. ksCurThread s = rv \<longrightarrow> (Invariants_H.valid_queues and valid_queues' and tcb_at' t and valid_objs' and ?R343 dom tptr rv) s) \<and> s' \<in> {s. \<forall>rv. ksCurThread_' (globals s) = tcb_ptr_to_ctcb_ptr rv \<longrightarrow> s \<in> {s. tcb_'_update (\<lambda>_. tptr) s \<in> UNIV \<inter> \<lbrace>\<acute>tcb = tcb_ptr_to_ctcb_ptr t\<rbrace>} \<inter> {s'. \<forall>t rv. dc rv (xfdc t) \<longrightarrow> s'\<lparr>globals := globals t\<rparr> \<in> UNIV \<inter> \<lbrace>True\<rbrace>}} proof (prove)
goal (9 subgoals):
 1. \<And>dom tptr curThread xfdca rv' rva ret__unsigned_long. \<lbrakk>d \<le> maxDomain; dom = UCAST(8 \<rightarrow> 32) d; tptr = tcb_ptr_to_ctcb_ptr t; rva = (ret__unsigned_long \<noteq> 0)\<rbrakk> \<Longrightarrow> ccorres dc xfdc (?P512 (UCAST(8 \<rightarrow> 32) d) (tcb_ptr_to_ctcb_ptr t) curThread () xfdca () rv' (ret__unsigned_long \<noteq> 0)) (?Q'409 (UCAST(8 \<rightarrow> 32) d) (tcb_ptr_to_ctcb_ptr t) curThread () xfdca () rv' (ret__unsigned_long \<noteq> 0) ret__unsigned_long) [] (if ret__unsigned_long \<noteq> 0 then tcbSchedEnqueue t else return ()) (IF ret__unsigned_long \<noteq> 0 THEN
  CALL tcbSchedEnqueue_'proc(tcb_ptr_to_ctcb_ptr t)
FI)
 2. \<And>dom tptr curThread rv xfdca y rv' rva ret__unsigned_long ya rv'a. \<lbrakk>d \<le> maxDomain; dom = UCAST(8 \<rightarrow> 32) d; tptr = tcb_ptr_to_ctcb_ptr t; dc rv xfdca; dc y rv'; rva = to_bool ret__unsigned_long; dc ya rv'a\<rbrakk> \<Longrightarrow> ccorres dc xfdc (?Q511 dom tptr curThread rv xfdca y rv' rva ret__unsigned_long ya) (?Q'511 dom tptr curThread rv xfdca y rv' rva ret__unsigned_long ya rv'a) [SKIP] (when (t = curThread) rescheduleRequired) (IF tptr = \<acute>ksCurThread THEN
  CALL rescheduleRequired_'proc()
FI)
 3. \<And>dom tptr curThread rv xfdc y rv' rva ret__unsigned_long. \<lbrakk>d \<le> maxDomain; dom = UCAST(8 \<rightarrow> 32) d; tptr = tcb_ptr_to_ctcb_ptr t; dc rv xfdc; dc y rv'; rva = to_bool ret__unsigned_long\<rbrakk> \<Longrightarrow> \<lbrace>?R513 dom tptr curThread rv xfdc y rv' rva\<rbrace> when rva (tcbSchedEnqueue t) \<lbrace>?Q511 dom tptr curThread rv xfdc y rv' rva ret__unsigned_long\<rbrace>
 4. \<And>dom tptr curThread rv xfdca y rv' rva ret__unsigned_long. \<lbrakk>d \<le> maxDomain; dom = UCAST(8 \<rightarrow> 32) d; tptr = tcb_ptr_to_ctcb_ptr t; dc rv xfdca; dc y rv'; rva = to_bool ret__unsigned_long\<rbrakk> \<Longrightarrow> guard_is_UNIV dc xfdc (?Q'511 dom tptr curThread rv xfdca y rv' rva ret__unsigned_long)
 5. \<And>dom tptr curThread rv xfdc y rv'. \<lbrakk>d \<le> maxDomain; dom = UCAST(8 \<rightarrow> 32) d; tptr = tcb_ptr_to_ctcb_ptr t; dc rv xfdc; dc y rv'\<rbrakk> \<Longrightarrow> \<lbrace>?R411 dom tptr curThread rv xfdc y\<rbrace> isRunnable t \<lbrace>\<lambda>rva. ?P512 dom tptr curThread rv xfdc y rv' rva and ?R513 dom tptr curThread rv xfdc y rv' rva\<rbrace>
 6. \<And>dom tptr curThread rv xfdc. \<lbrakk>d \<le> maxDomain; dom = UCAST(8 \<rightarrow> 32) d; tptr = tcb_ptr_to_ctcb_ptr t; dc rv xfdc\<rbrakk> \<Longrightarrow> \<lbrace>?R372 dom tptr curThread rv\<rbrace> threadSet (tcbDomain_update (\<lambda>_. d)) t \<lbrace>\<lambda>y. tcb_at' t and ?R411 dom tptr curThread rv xfdc y\<rbrace>
 7. \<And>dom tptr curThread rv xfdca. \<lbrakk>d \<le> maxDomain; dom = UCAST(8 \<rightarrow> 32) d; tptr = tcb_ptr_to_ctcb_ptr t; dc rv xfdca\<rbrakk> \<Longrightarrow> guard_is_UNIV dc xfdc (\<lambda>y rv'. {s. thread_'_update (\<lambda>_. tptr) s \<in> UNIV \<inter> \<lbrace>\<acute>thread = tcb_ptr_to_ctcb_ptr t\<rbrace>} \<inter> {s'. \<forall>t rva. rva = to_bool (ret__unsigned_long_' t) \<longrightarrow> s'\<lparr>globals := globals t, ret__unsigned_long_' := ret__unsigned_long_' t\<rparr> \<in> ?Q'409 dom tptr curThread rv xfdca y rv' rva (ret__unsigned_long_' t)})
 8. \<And>dom tptr curThread. \<lbrakk>d \<le> maxDomain; dom = UCAST(8 \<rightarrow> 32) d; tptr = tcb_ptr_to_ctcb_ptr t\<rbrakk> \<Longrightarrow> \<lbrace>?R343 dom tptr curThread\<rbrace> tcbSchedDequeue t \<lbrace>\<lambda>rv. tcb_at' t and (\<lambda>_. True) and ?R372 dom tptr curThread rv and tcb_at' (ctcb_ptr_to_tcb_ptr tptr)\<rbrace>
 9. \<And>dom tptr s s'. \<lbrakk>d \<le> maxDomain; dom = UCAST(8 \<rightarrow> 32) d; tptr = tcb_ptr_to_ctcb_ptr t; (s, s') \<in> rf_sr; (invs' and tcb_at' t and sch_act_simple) s; s' \<in> UNIV\<rbrakk> \<Longrightarrow> (\<forall>rv. ksCurThread s = rv \<longrightarrow> (Invariants_H.valid_queues and valid_queues' and tcb_at' t and valid_objs' and ?R343 dom tptr rv) s) \<and> s' \<in> {s. \<forall>rv. ksCurThread_' (globals s) = tcb_ptr_to_ctcb_ptr rv \<longrightarrow> s \<in> {s. tcb_'_update (\<lambda>_. tptr) s \<in> UNIV \<inter> \<lbrace>\<acute>tcb = tcb_ptr_to_ctcb_ptr t\<rbrace>} \<inter> {s'. \<forall>t rv. dc rv (xfdc t) \<longrightarrow> s'\<lparr>globals := globals t\<rparr> \<in> UNIV \<inter> \<lbrace>True\<rbrace>}} proof (prove)
goal (10 subgoals):
 1. \<And>dom tptr curThread xfdca rv' rva ret__unsigned_long. \<lbrakk>d \<le> maxDomain; dom = UCAST(8 \<rightarrow> 32) d; tptr = tcb_ptr_to_ctcb_ptr t; rva = (ret__unsigned_long \<noteq> 0)\<rbrakk> \<Longrightarrow> ccorres dc xfdc (?Pt540 (UCAST(8 \<rightarrow> 32) d) (tcb_ptr_to_ctcb_ptr t) curThread () xfdca () rv' (ret__unsigned_long \<noteq> 0)) (?Rt536 (UCAST(8 \<rightarrow> 32) d) (tcb_ptr_to_ctcb_ptr t) curThread () xfdca () rv' (ret__unsigned_long \<noteq> 0) ret__unsigned_long) [] (tcbSchedEnqueue t) (CALL tcbSchedEnqueue_'proc(tcb_ptr_to_ctcb_ptr t))
 2. \<And>dom tptr curThread xfdca rv' rva ret__unsigned_long. \<lbrakk>d \<le> maxDomain; dom = UCAST(8 \<rightarrow> 32) d; tptr = tcb_ptr_to_ctcb_ptr t; rva = (ret__unsigned_long \<noteq> 0)\<rbrakk> \<Longrightarrow> ccorres dc xfdc (?Pf538 (UCAST(8 \<rightarrow> 32) d) (tcb_ptr_to_ctcb_ptr t) curThread () xfdca () rv' (ret__unsigned_long \<noteq> 0)) (?Rf534 (UCAST(8 \<rightarrow> 32) d) (tcb_ptr_to_ctcb_ptr t) curThread () xfdca () rv' (ret__unsigned_long \<noteq> 0) ret__unsigned_long) [] (return ()) SKIP
 3. \<And>dom tptr curThread rv xfdca y rv' rva ret__unsigned_long ya rv'a. \<lbrakk>d \<le> maxDomain; dom = UCAST(8 \<rightarrow> 32) d; tptr = tcb_ptr_to_ctcb_ptr t; dc rv xfdca; dc y rv'; rva = to_bool ret__unsigned_long; dc ya rv'a\<rbrakk> \<Longrightarrow> ccorres dc xfdc (?Q511 dom tptr curThread rv xfdca y rv' rva ret__unsigned_long ya) (?Q'511 dom tptr curThread rv xfdca y rv' rva ret__unsigned_long ya rv'a) [SKIP] (when (t = curThread) rescheduleRequired) (IF tptr = \<acute>ksCurThread THEN
  CALL rescheduleRequired_'proc()
FI)
 4. \<And>dom tptr curThread rv xfdc y rv' rva ret__unsigned_long. \<lbrakk>d \<le> maxDomain; dom = UCAST(8 \<rightarrow> 32) d; tptr = tcb_ptr_to_ctcb_ptr t; dc rv xfdc; dc y rv'; rva = to_bool ret__unsigned_long\<rbrakk> \<Longrightarrow> \<lbrace>?R513 dom tptr curThread rv xfdc y rv' rva\<rbrace> when rva (tcbSchedEnqueue t) \<lbrace>?Q511 dom tptr curThread rv xfdc y rv' rva ret__unsigned_long\<rbrace>
 5. \<And>dom tptr curThread rv xfdca y rv' rva ret__unsigned_long. \<lbrakk>d \<le> maxDomain; dom = UCAST(8 \<rightarrow> 32) d; tptr = tcb_ptr_to_ctcb_ptr t; dc rv xfdca; dc y rv'; rva = to_bool ret__unsigned_long\<rbrakk> \<Longrightarrow> guard_is_UNIV dc xfdc (?Q'511 dom tptr curThread rv xfdca y rv' rva ret__unsigned_long)
 6. \<And>dom tptr curThread rv xfdc y rv'. \<lbrakk>d \<le> maxDomain; dom = UCAST(8 \<rightarrow> 32) d; tptr = tcb_ptr_to_ctcb_ptr t; dc rv xfdc; dc y rv'\<rbrakk> \<Longrightarrow> \<lbrace>?R411 dom tptr curThread rv xfdc y\<rbrace> isRunnable t \<lbrace>\<lambda>rva. (\<lambda>_. True) and (\<lambda>s. rva \<longrightarrow> ?Pt540 dom tptr curThread rv xfdc y rv' rva s) and (\<lambda>s. \<not> rva \<longrightarrow> ?Pf538 dom tptr curThread rv xfdc y rv' rva s) and ?R513 dom tptr curThread rv xfdc y rv' rva\<rbrace>
 7. \<And>dom tptr curThread rv xfdc. \<lbrakk>d \<le> maxDomain; dom = UCAST(8 \<rightarrow> 32) d; tptr = tcb_ptr_to_ctcb_ptr t; dc rv xfdc\<rbrakk> \<Longrightarrow> \<lbrace>?R372 dom tptr curThread rv\<rbrace> threadSet (tcbDomain_update (\<lambda>_. d)) t \<lbrace>\<lambda>y. tcb_at' t and ?R411 dom tptr curThread rv xfdc y\<rbrace>
 8. \<And>dom tptr curThread rv xfdca. \<lbrakk>d \<le> maxDomain; dom = UCAST(8 \<rightarrow> 32) d; tptr = tcb_ptr_to_ctcb_ptr t; dc rv xfdca\<rbrakk> \<Longrightarrow> guard_is_UNIV dc xfdc (\<lambda>y rv'. {s. thread_'_update (\<lambda>_. tptr) s \<in> UNIV \<inter> \<lbrace>\<acute>thread = tcb_ptr_to_ctcb_ptr t\<rbrace>} \<inter> {s'. \<forall>t rva. rva = to_bool (ret__unsigned_long_' t) \<longrightarrow> s'\<lparr>globals := globals t, ret__unsigned_long_' := ret__unsigned_long_' t\<rparr> \<in> {s. (s \<in> \<lbrace>rva\<rbrace> \<longrightarrow> s \<in> ?Rt536 dom tptr curThread rv xfdca y rv' rva (ret__unsigned_long_' t)) \<and> (s \<notin> \<lbrace>rva\<rbrace> \<longrightarrow> s \<in> ?Rf534 dom tptr curThread rv xfdca y rv' rva (ret__unsigned_long_' t))}})
 9. \<And>dom tptr curThread. \<lbrakk>d \<le> maxDomain; dom = UCAST(8 \<rightarrow> 32) d; tptr = tcb_ptr_to_ctcb_ptr t\<rbrakk> \<Longrightarrow> \<lbrace>?R343 dom tptr curThread\<rbrace> tcbSchedDequeue t \<lbrace>\<lambda>rv. tcb_at' t and (\<lambda>_. True) and ?R372 dom tptr curThread rv and tcb_at' (ctcb_ptr_to_tcb_ptr tptr)\<rbrace>
 10. \<And>dom tptr s s'. \<lbrakk>d \<le> maxDomain; dom = UCAST(8 \<rightarrow> 32) d; tptr = tcb_ptr_to_ctcb_ptr t; (s, s') \<in> rf_sr; (invs' and tcb_at' t and sch_act_simple) s; s' \<in> UNIV\<rbrakk> \<Longrightarrow> (\<forall>rv. ksCurThread s = rv \<longrightarrow> (Invariants_H.valid_queues and valid_queues' and tcb_at' t and valid_objs' and ?R343 dom tptr rv) s) \<and> s' \<in> {s. \<forall>rv. ksCurThread_' (globals s) = tcb_ptr_to_ctcb_ptr rv \<longrightarrow> s \<in> {s. tcb_'_update (\<lambda>_. tptr) s \<in> UNIV \<inter> \<lbrace>\<acute>tcb = tcb_ptr_to_ctcb_ptr t\<rbrace>} \<inter> {s'. \<forall>t rv. dc rv (xfdc t) \<longrightarrow> s'\<lparr>globals := globals t\<rparr> \<in> UNIV \<inter> \<lbrace>True\<rbrace>}} proof (prove)
goal (9 subgoals):
 1. \<And>dom tptr curThread xfdca rv' rva ret__unsigned_long. \<lbrakk>d \<le> maxDomain; dom = UCAST(8 \<rightarrow> 32) d; tptr = tcb_ptr_to_ctcb_ptr t; rva = (ret__unsigned_long \<noteq> 0)\<rbrakk> \<Longrightarrow> ccorres dc xfdc (?Pf538 (UCAST(8 \<rightarrow> 32) d) (tcb_ptr_to_ctcb_ptr t) curThread () xfdca () rv' (ret__unsigned_long \<noteq> 0)) (?Rf534 (UCAST(8 \<rightarrow> 32) d) (tcb_ptr_to_ctcb_ptr t) curThread () xfdca () rv' (ret__unsigned_long \<noteq> 0) ret__unsigned_long) [] (return ()) SKIP
 2. \<And>dom tptr curThread rv xfdca y rv' rva ret__unsigned_long ya rv'a. \<lbrakk>d \<le> maxDomain; dom = UCAST(8 \<rightarrow> 32) d; tptr = tcb_ptr_to_ctcb_ptr t; dc rv xfdca; dc y rv'; rva = to_bool ret__unsigned_long; dc ya rv'a\<rbrakk> \<Longrightarrow> ccorres dc xfdc (?Q511 dom tptr curThread rv xfdca y rv' rva ret__unsigned_long ya) (?Q'511 dom tptr curThread rv xfdca y rv' rva ret__unsigned_long ya rv'a) [SKIP] (when (t = curThread) rescheduleRequired) (IF tptr = \<acute>ksCurThread THEN
  CALL rescheduleRequired_'proc()
FI)
 3. \<And>dom tptr curThread rv xfdc y rv' rva ret__unsigned_long. \<lbrakk>d \<le> maxDomain; dom = UCAST(8 \<rightarrow> 32) d; tptr = tcb_ptr_to_ctcb_ptr t; dc rv xfdc; dc y rv'; rva = to_bool ret__unsigned_long\<rbrakk> \<Longrightarrow> \<lbrace>?R513 dom tptr curThread rv xfdc y rv' rva\<rbrace> when rva (tcbSchedEnqueue t) \<lbrace>?Q511 dom tptr curThread rv xfdc y rv' rva ret__unsigned_long\<rbrace>
 4. \<And>dom tptr curThread rv xfdca y rv' rva ret__unsigned_long. \<lbrakk>d \<le> maxDomain; dom = UCAST(8 \<rightarrow> 32) d; tptr = tcb_ptr_to_ctcb_ptr t; dc rv xfdca; dc y rv'; rva = to_bool ret__unsigned_long\<rbrakk> \<Longrightarrow> guard_is_UNIV dc xfdc (?Q'511 dom tptr curThread rv xfdca y rv' rva ret__unsigned_long)
 5. \<And>dom tptr curThread rv xfdc y rv'. \<lbrakk>d \<le> maxDomain; dom = UCAST(8 \<rightarrow> 32) d; tptr = tcb_ptr_to_ctcb_ptr t; dc rv xfdc; dc y rv'\<rbrakk> \<Longrightarrow> \<lbrace>?R411 dom tptr curThread rv xfdc y\<rbrace> isRunnable t \<lbrace>\<lambda>rva. (\<lambda>_. True) and (\<lambda>s. rva \<longrightarrow> (Invariants_H.valid_queues and tcb_at' t and valid_objs') s) and (\<lambda>s. \<not> rva \<longrightarrow> ?Pf538 dom tptr curThread rv xfdc y rv' rva s) and ?R513 dom tptr curThread rv xfdc y rv' rva\<rbrace>
 6. \<And>dom tptr curThread rv xfdc. \<lbrakk>d \<le> maxDomain; dom = UCAST(8 \<rightarrow> 32) d; tptr = tcb_ptr_to_ctcb_ptr t; dc rv xfdc\<rbrakk> \<Longrightarrow> \<lbrace>?R372 dom tptr curThread rv\<rbrace> threadSet (tcbDomain_update (\<lambda>_. d)) t \<lbrace>\<lambda>y. tcb_at' t and ?R411 dom tptr curThread rv xfdc y\<rbrace>
 7. \<And>dom tptr curThread rv xfdca. \<lbrakk>d \<le> maxDomain; dom = UCAST(8 \<rightarrow> 32) d; tptr = tcb_ptr_to_ctcb_ptr t; dc rv xfdca\<rbrakk> \<Longrightarrow> guard_is_UNIV dc xfdc (\<lambda>y rv'. {s. thread_'_update (\<lambda>_. tptr) s \<in> UNIV \<inter> \<lbrace>\<acute>thread = tcb_ptr_to_ctcb_ptr t\<rbrace>} \<inter> {s'. \<forall>t rva. rva = to_bool (ret__unsigned_long_' t) \<longrightarrow> s'\<lparr>globals := globals t, ret__unsigned_long_' := ret__unsigned_long_' t\<rparr> \<in> {s. (s \<in> \<lbrace>rva\<rbrace> \<longrightarrow> s \<in> {s. tcb_'_update (\<lambda>_. tptr) s \<in> UNIV \<inter> \<lbrace>\<acute>tcb = tptr\<rbrace>}) \<and> (s \<notin> \<lbrace>rva\<rbrace> \<longrightarrow> s \<in> ?Rf534 dom tptr curThread rv xfdca y rv' rva (ret__unsigned_long_' t))}})
 8. \<And>dom tptr curThread. \<lbrakk>d \<le> maxDomain; dom = UCAST(8 \<rightarrow> 32) d; tptr = tcb_ptr_to_ctcb_ptr t\<rbrakk> \<Longrightarrow> \<lbrace>?R343 dom tptr curThread\<rbrace> tcbSchedDequeue t \<lbrace>\<lambda>rv. tcb_at' t and (\<lambda>_. True) and ?R372 dom tptr curThread rv and tcb_at' (ctcb_ptr_to_tcb_ptr tptr)\<rbrace>
 9. \<And>dom tptr s s'. \<lbrakk>d \<le> maxDomain; dom = UCAST(8 \<rightarrow> 32) d; tptr = tcb_ptr_to_ctcb_ptr t; (s, s') \<in> rf_sr; (invs' and tcb_at' t and sch_act_simple) s; s' \<in> UNIV\<rbrakk> \<Longrightarrow> (\<forall>rv. ksCurThread s = rv \<longrightarrow> (Invariants_H.valid_queues and valid_queues' and tcb_at' t and valid_objs' and ?R343 dom tptr rv) s) \<and> s' \<in> {s. \<forall>rv. ksCurThread_' (globals s) = tcb_ptr_to_ctcb_ptr rv \<longrightarrow> s \<in> {s. tcb_'_update (\<lambda>_. tptr) s \<in> UNIV \<inter> \<lbrace>\<acute>tcb = tcb_ptr_to_ctcb_ptr t\<rbrace>} \<inter> {s'. \<forall>t rv. dc rv (xfdc t) \<longrightarrow> s'\<lparr>globals := globals t\<rparr> \<in> UNIV \<inter> \<lbrace>True\<rbrace>}} proof (prove)
goal (8 subgoals):
 1. \<And>dom tptr curThread rv xfdca y rv' rva ret__unsigned_long ya rv'a. \<lbrakk>d \<le> maxDomain; dom = UCAST(8 \<rightarrow> 32) d; tptr = tcb_ptr_to_ctcb_ptr t; dc rv xfdca; dc y rv'; rva = to_bool ret__unsigned_long; dc ya rv'a\<rbrakk> \<Longrightarrow> ccorres dc xfdc (?Q511 dom tptr curThread rv xfdca y rv' rva ret__unsigned_long ya) (?Q'511 dom tptr curThread rv xfdca y rv' rva ret__unsigned_long ya rv'a) [SKIP] (when (t = curThread) rescheduleRequired) (IF tptr = \<acute>ksCurThread THEN
  CALL rescheduleRequired_'proc()
FI)
 2. \<And>dom tptr curThread rv xfdc y rv' rva ret__unsigned_long. \<lbrakk>d \<le> maxDomain; dom = UCAST(8 \<rightarrow> 32) d; tptr = tcb_ptr_to_ctcb_ptr t; dc rv xfdc; dc y rv'; rva = to_bool ret__unsigned_long\<rbrakk> \<Longrightarrow> \<lbrace>?R513 dom tptr curThread rv xfdc y rv' rva\<rbrace> when rva (tcbSchedEnqueue t) \<lbrace>?Q511 dom tptr curThread rv xfdc y rv' rva ret__unsigned_long\<rbrace>
 3. \<And>dom tptr curThread rv xfdca y rv' rva ret__unsigned_long. \<lbrakk>d \<le> maxDomain; dom = UCAST(8 \<rightarrow> 32) d; tptr = tcb_ptr_to_ctcb_ptr t; dc rv xfdca; dc y rv'; rva = to_bool ret__unsigned_long\<rbrakk> \<Longrightarrow> guard_is_UNIV dc xfdc (?Q'511 dom tptr curThread rv xfdca y rv' rva ret__unsigned_long)
 4. \<And>dom tptr curThread rv xfdc y rv'. \<lbrakk>d \<le> maxDomain; dom = UCAST(8 \<rightarrow> 32) d; tptr = tcb_ptr_to_ctcb_ptr t; dc rv xfdc; dc y rv'\<rbrakk> \<Longrightarrow> \<lbrace>?R411 dom tptr curThread rv xfdc y\<rbrace> isRunnable t \<lbrace>\<lambda>rva. (\<lambda>_. True) and (\<lambda>s. rva \<longrightarrow> (Invariants_H.valid_queues and tcb_at' t and valid_objs') s) and (\<lambda>s. \<not> rva \<longrightarrow> True) and ?R513 dom tptr curThread rv xfdc y rv' rva\<rbrace>
 5. \<And>dom tptr curThread rv xfdc. \<lbrakk>d \<le> maxDomain; dom = UCAST(8 \<rightarrow> 32) d; tptr = tcb_ptr_to_ctcb_ptr t; dc rv xfdc\<rbrakk> \<Longrightarrow> \<lbrace>?R372 dom tptr curThread rv\<rbrace> threadSet (tcbDomain_update (\<lambda>_. d)) t \<lbrace>\<lambda>y. tcb_at' t and ?R411 dom tptr curThread rv xfdc y\<rbrace>
 6. \<And>dom tptr curThread rv xfdca. \<lbrakk>d \<le> maxDomain; dom = UCAST(8 \<rightarrow> 32) d; tptr = tcb_ptr_to_ctcb_ptr t; dc rv xfdca\<rbrakk> \<Longrightarrow> guard_is_UNIV dc xfdc (\<lambda>y rv'. {s. thread_'_update (\<lambda>_. tptr) s \<in> UNIV \<inter> \<lbrace>\<acute>thread = tcb_ptr_to_ctcb_ptr t\<rbrace>} \<inter> {s'. \<forall>t rv. rv = to_bool (ret__unsigned_long_' t) \<longrightarrow> s'\<lparr>globals := globals t, ret__unsigned_long_' := ret__unsigned_long_' t\<rparr> \<in> {s. (s \<in> \<lbrace>rv\<rbrace> \<longrightarrow> s \<in> {s. tcb_'_update (\<lambda>_. tptr) s \<in> UNIV \<inter> \<lbrace>\<acute>tcb = tptr\<rbrace>}) \<and> (s \<notin> \<lbrace>rv\<rbrace> \<longrightarrow> s \<in> UNIV)}})
 7. \<And>dom tptr curThread. \<lbrakk>d \<le> maxDomain; dom = UCAST(8 \<rightarrow> 32) d; tptr = tcb_ptr_to_ctcb_ptr t\<rbrakk> \<Longrightarrow> \<lbrace>?R343 dom tptr curThread\<rbrace> tcbSchedDequeue t \<lbrace>\<lambda>rv. tcb_at' t and (\<lambda>_. True) and ?R372 dom tptr curThread rv and tcb_at' (ctcb_ptr_to_tcb_ptr tptr)\<rbrace>
 8. \<And>dom tptr s s'. \<lbrakk>d \<le> maxDomain; dom = UCAST(8 \<rightarrow> 32) d; tptr = tcb_ptr_to_ctcb_ptr t; (s, s') \<in> rf_sr; (invs' and tcb_at' t and sch_act_simple) s; s' \<in> UNIV\<rbrakk> \<Longrightarrow> (\<forall>rv. ksCurThread s = rv \<longrightarrow> (Invariants_H.valid_queues and valid_queues' and tcb_at' t and valid_objs' and ?R343 dom tptr rv) s) \<and> s' \<in> {s. \<forall>rv. ksCurThread_' (globals s) = tcb_ptr_to_ctcb_ptr rv \<longrightarrow> s \<in> {s. tcb_'_update (\<lambda>_. tptr) s \<in> UNIV \<inter> \<lbrace>\<acute>tcb = tcb_ptr_to_ctcb_ptr t\<rbrace>} \<inter> {s'. \<forall>t rv. dc rv (xfdc t) \<longrightarrow> s'\<lparr>globals := globals t\<rparr> \<in> UNIV \<inter> \<lbrace>True\<rbrace>}} proof (prove)
goal (8 subgoals):
 1. \<And>dom tptr curThread xfdca rv' rva ret__unsigned_long rv'a. \<lbrakk>d \<le> maxDomain; dom = UCAST(8 \<rightarrow> 32) d; tptr = tcb_ptr_to_ctcb_ptr t; rva = to_bool ret__unsigned_long\<rbrakk> \<Longrightarrow> ccorres dc xfdc (?Q511 (UCAST(8 \<rightarrow> 32) d) (tcb_ptr_to_ctcb_ptr t) curThread () xfdca () rv' (to_bool ret__unsigned_long) ret__unsigned_long ()) (?Q'511 (UCAST(8 \<rightarrow> 32) d) (tcb_ptr_to_ctcb_ptr t) curThread () xfdca () rv' (to_bool ret__unsigned_long) ret__unsigned_long () rv'a) [SKIP] (if t = curThread then rescheduleRequired else return ()) (IF tcb_ptr_to_ctcb_ptr t = \<acute>ksCurThread THEN
  CALL rescheduleRequired_'proc()
FI)
 2. \<And>dom tptr curThread rv xfdc y rv' rva ret__unsigned_long. \<lbrakk>d \<le> maxDomain; dom = UCAST(8 \<rightarrow> 32) d; tptr = tcb_ptr_to_ctcb_ptr t; dc rv xfdc; dc y rv'; rva = to_bool ret__unsigned_long\<rbrakk> \<Longrightarrow> \<lbrace>?R513 dom tptr curThread rv xfdc y rv' rva\<rbrace> when rva (tcbSchedEnqueue t) \<lbrace>?Q511 dom tptr curThread rv xfdc y rv' rva ret__unsigned_long\<rbrace>
 3. \<And>dom tptr curThread rv xfdca y rv' rva ret__unsigned_long. \<lbrakk>d \<le> maxDomain; dom = UCAST(8 \<rightarrow> 32) d; tptr = tcb_ptr_to_ctcb_ptr t; dc rv xfdca; dc y rv'; rva = to_bool ret__unsigned_long\<rbrakk> \<Longrightarrow> guard_is_UNIV dc xfdc (?Q'511 dom tptr curThread rv xfdca y rv' rva ret__unsigned_long)
 4. \<And>dom tptr curThread rv xfdc y rv'. \<lbrakk>d \<le> maxDomain; dom = UCAST(8 \<rightarrow> 32) d; tptr = tcb_ptr_to_ctcb_ptr t; dc rv xfdc; dc y rv'\<rbrakk> \<Longrightarrow> \<lbrace>?R411 dom tptr curThread rv xfdc y\<rbrace> isRunnable t \<lbrace>\<lambda>rva. (\<lambda>_. True) and (\<lambda>s. rva \<longrightarrow> (Invariants_H.valid_queues and tcb_at' t and valid_objs') s) and (\<lambda>s. \<not> rva \<longrightarrow> True) and ?R513 dom tptr curThread rv xfdc y rv' rva\<rbrace>
 5. \<And>dom tptr curThread rv xfdc. \<lbrakk>d \<le> maxDomain; dom = UCAST(8 \<rightarrow> 32) d; tptr = tcb_ptr_to_ctcb_ptr t; dc rv xfdc\<rbrakk> \<Longrightarrow> \<lbrace>?R372 dom tptr curThread rv\<rbrace> threadSet (tcbDomain_update (\<lambda>_. d)) t \<lbrace>\<lambda>y. tcb_at' t and ?R411 dom tptr curThread rv xfdc y\<rbrace>
 6. \<And>dom tptr curThread rv xfdca. \<lbrakk>d \<le> maxDomain; dom = UCAST(8 \<rightarrow> 32) d; tptr = tcb_ptr_to_ctcb_ptr t; dc rv xfdca\<rbrakk> \<Longrightarrow> guard_is_UNIV dc xfdc (\<lambda>y rv'. {s. thread_'_update (\<lambda>_. tptr) s \<in> UNIV \<inter> \<lbrace>\<acute>thread = tcb_ptr_to_ctcb_ptr t\<rbrace>} \<inter> {s'. \<forall>t rv. rv = to_bool (ret__unsigned_long_' t) \<longrightarrow> s'\<lparr>globals := globals t, ret__unsigned_long_' := ret__unsigned_long_' t\<rparr> \<in> {s. (s \<in> \<lbrace>rv\<rbrace> \<longrightarrow> s \<in> {s. tcb_'_update (\<lambda>_. tptr) s \<in> UNIV \<inter> \<lbrace>\<acute>tcb = tptr\<rbrace>}) \<and> (s \<notin> \<lbrace>rv\<rbrace> \<longrightarrow> s \<in> UNIV)}})
 7. \<And>dom tptr curThread. \<lbrakk>d \<le> maxDomain; dom = UCAST(8 \<rightarrow> 32) d; tptr = tcb_ptr_to_ctcb_ptr t\<rbrakk> \<Longrightarrow> \<lbrace>?R343 dom tptr curThread\<rbrace> tcbSchedDequeue t \<lbrace>\<lambda>rv. tcb_at' t and (\<lambda>_. True) and ?R372 dom tptr curThread rv and tcb_at' (ctcb_ptr_to_tcb_ptr tptr)\<rbrace>
 8. \<And>dom tptr s s'. \<lbrakk>d \<le> maxDomain; dom = UCAST(8 \<rightarrow> 32) d; tptr = tcb_ptr_to_ctcb_ptr t; (s, s') \<in> rf_sr; (invs' and tcb_at' t and sch_act_simple) s; s' \<in> UNIV\<rbrakk> \<Longrightarrow> (\<forall>rv. ksCurThread s = rv \<longrightarrow> (Invariants_H.valid_queues and valid_queues' and tcb_at' t and valid_objs' and ?R343 dom tptr rv) s) \<and> s' \<in> {s. \<forall>rv. ksCurThread_' (globals s) = tcb_ptr_to_ctcb_ptr rv \<longrightarrow> s \<in> {s. tcb_'_update (\<lambda>_. tptr) s \<in> UNIV \<inter> \<lbrace>\<acute>tcb = tcb_ptr_to_ctcb_ptr t\<rbrace>} \<inter> {s'. \<forall>t rv. dc rv (xfdc t) \<longrightarrow> s'\<lparr>globals := globals t\<rparr> \<in> UNIV \<inter> \<lbrace>True\<rbrace>}} proof (prove)
goal (10 subgoals):
 1. \<And>dom tptr curThread xfdc rv' rva ret__unsigned_long rv'a. \<lbrakk>d \<le> maxDomain; dom = UCAST(8 \<rightarrow> 32) d; tptr = tcb_ptr_to_ctcb_ptr t; rva = to_bool ret__unsigned_long\<rbrakk> \<Longrightarrow> \<forall>s s'. (s, s') \<in> rf_sr \<and> curThread = ksCurThread s \<longrightarrow> (t = curThread) = (s' \<in> \<lbrace>tcb_ptr_to_ctcb_ptr t = \<acute>ksCurThread\<rbrace>)
 2. \<And>dom tptr curThread xfdca rv' rva ret__unsigned_long rv'a. \<lbrakk>d \<le> maxDomain; dom = UCAST(8 \<rightarrow> 32) d; tptr = tcb_ptr_to_ctcb_ptr t; rva = to_bool ret__unsigned_long\<rbrakk> \<Longrightarrow> ccorres dc xfdc (?Pt571 (UCAST(8 \<rightarrow> 32) d) (tcb_ptr_to_ctcb_ptr t) curThread () xfdca () rv' (to_bool ret__unsigned_long) ret__unsigned_long ()) (?Rt567 (UCAST(8 \<rightarrow> 32) d) (tcb_ptr_to_ctcb_ptr t) curThread () xfdca () rv' (to_bool ret__unsigned_long) ret__unsigned_long () rv'a) [SKIP] rescheduleRequired (CALL rescheduleRequired_'proc())
 3. \<And>dom tptr curThread xfdca rv' rva ret__unsigned_long rv'a. \<lbrakk>d \<le> maxDomain; dom = UCAST(8 \<rightarrow> 32) d; tptr = tcb_ptr_to_ctcb_ptr t; rva = to_bool ret__unsigned_long\<rbrakk> \<Longrightarrow> ccorres dc xfdc (?Pf569 (UCAST(8 \<rightarrow> 32) d) (tcb_ptr_to_ctcb_ptr t) curThread () xfdca () rv' (to_bool ret__unsigned_long) ret__unsigned_long ()) (?Rf565 (UCAST(8 \<rightarrow> 32) d) (tcb_ptr_to_ctcb_ptr t) curThread () xfdca () rv' (to_bool ret__unsigned_long) ret__unsigned_long () rv'a) [SKIP] (return ()) SKIP
 4. \<And>dom tptr curThread rv xfdc y rv' rva ret__unsigned_long. \<lbrakk>d \<le> maxDomain; dom = UCAST(8 \<rightarrow> 32) d; tptr = tcb_ptr_to_ctcb_ptr t; dc rv xfdc; dc y rv'; rva = to_bool ret__unsigned_long\<rbrakk> \<Longrightarrow> \<lbrace>?R513 dom tptr curThread rv xfdc y rv' rva\<rbrace> when rva (tcbSchedEnqueue t) \<lbrace>\<lambda>a. (\<lambda>s. curThread = ksCurThread s) and (\<lambda>s. t = curThread \<longrightarrow> ?Pt571 dom tptr curThread rv xfdc y rv' rva ret__unsigned_long a s) and (\<lambda>s. t \<noteq> curThread \<longrightarrow> ?Pf569 dom tptr curThread rv xfdc y rv' rva ret__unsigned_long a s)\<rbrace>
 5. \<And>dom tptr curThread rv xfdca y rv' rva ret__unsigned_long. \<lbrakk>d \<le> maxDomain; dom = UCAST(8 \<rightarrow> 32) d; tptr = tcb_ptr_to_ctcb_ptr t; dc rv xfdca; dc y rv'; rva = to_bool ret__unsigned_long\<rbrakk> \<Longrightarrow> guard_is_UNIV dc xfdc (\<lambda>a b. {s. (s \<in> \<lbrace>tptr = \<acute>ksCurThread\<rbrace> \<longrightarrow> s \<in> ?Rt567 dom tptr curThread rv xfdca y rv' rva ret__unsigned_long a b) \<and> (s \<notin> \<lbrace>tptr = \<acute>ksCurThread\<rbrace> \<longrightarrow> s \<in> ?Rf565 dom tptr curThread rv xfdca y rv' rva ret__unsigned_long a b)})
 6. \<And>dom tptr curThread rv xfdc y rv'. \<lbrakk>d \<le> maxDomain; dom = UCAST(8 \<rightarrow> 32) d; tptr = tcb_ptr_to_ctcb_ptr t; dc rv xfdc; dc y rv'\<rbrakk> \<Longrightarrow> \<lbrace>?R411 dom tptr curThread rv xfdc y\<rbrace> isRunnable t \<lbrace>\<lambda>rva. (\<lambda>_. True) and (\<lambda>s. rva \<longrightarrow> (Invariants_H.valid_queues and tcb_at' t and valid_objs') s) and (\<lambda>s. \<not> rva \<longrightarrow> True) and ?R513 dom tptr curThread rv xfdc y rv' rva\<rbrace>
 7. \<And>dom tptr curThread rv xfdc. \<lbrakk>d \<le> maxDomain; dom = UCAST(8 \<rightarrow> 32) d; tptr = tcb_ptr_to_ctcb_ptr t; dc rv xfdc\<rbrakk> \<Longrightarrow> \<lbrace>?R372 dom tptr curThread rv\<rbrace> threadSet (tcbDomain_update (\<lambda>_. d)) t \<lbrace>\<lambda>y. tcb_at' t and ?R411 dom tptr curThread rv xfdc y\<rbrace>
 8. \<And>dom tptr curThread rv xfdca. \<lbrakk>d \<le> maxDomain; dom = UCAST(8 \<rightarrow> 32) d; tptr = tcb_ptr_to_ctcb_ptr t; dc rv xfdca\<rbrakk> \<Longrightarrow> guard_is_UNIV dc xfdc (\<lambda>y rv'. {s. thread_'_update (\<lambda>_. tptr) s \<in> UNIV \<inter> \<lbrace>\<acute>thread = tcb_ptr_to_ctcb_ptr t\<rbrace>} \<inter> {s'. \<forall>t rv. rv = to_bool (ret__unsigned_long_' t) \<longrightarrow> s'\<lparr>globals := globals t, ret__unsigned_long_' := ret__unsigned_long_' t\<rparr> \<in> {s. (s \<in> \<lbrace>rv\<rbrace> \<longrightarrow> s \<in> {s. tcb_'_update (\<lambda>_. tptr) s \<in> UNIV \<inter> \<lbrace>\<acute>tcb = tptr\<rbrace>}) \<and> (s \<notin> \<lbrace>rv\<rbrace> \<longrightarrow> s \<in> UNIV)}})
 9. \<And>dom tptr curThread. \<lbrakk>d \<le> maxDomain; dom = UCAST(8 \<rightarrow> 32) d; tptr = tcb_ptr_to_ctcb_ptr t\<rbrakk> \<Longrightarrow> \<lbrace>?R343 dom tptr curThread\<rbrace> tcbSchedDequeue t \<lbrace>\<lambda>rv. tcb_at' t and (\<lambda>_. True) and ?R372 dom tptr curThread rv and tcb_at' (ctcb_ptr_to_tcb_ptr tptr)\<rbrace>
 10. \<And>dom tptr s s'. \<lbrakk>d \<le> maxDomain; dom = UCAST(8 \<rightarrow> 32) d; tptr = tcb_ptr_to_ctcb_ptr t; (s, s') \<in> rf_sr; (invs' and tcb_at' t and sch_act_simple) s; s' \<in> UNIV\<rbrakk> \<Longrightarrow> (\<forall>rv. ksCurThread s = rv \<longrightarrow> (Invariants_H.valid_queues and valid_queues' and tcb_at' t and valid_objs' and ?R343 dom tptr rv) s) \<and> s' \<in> {s. \<forall>rv. ksCurThread_' (globals s) = tcb_ptr_to_ctcb_ptr rv \<longrightarrow> s \<in> {s. tcb_'_update (\<lambda>_. tptr) s \<in> UNIV \<inter> \<lbrace>\<acute>tcb = tcb_ptr_to_ctcb_ptr t\<rbrace>} \<inter> {s'. \<forall>t rv. dc rv (xfdc t) \<longrightarrow> s'\<lparr>globals := globals t\<rparr> \<in> UNIV \<inter> \<lbrace>True\<rbrace>}} proof (prove)
goal (9 subgoals):
 1. \<And>dom tptr curThread xfdca rv' rva ret__unsigned_long rv'a. \<lbrakk>d \<le> maxDomain; dom = UCAST(8 \<rightarrow> 32) d; tptr = tcb_ptr_to_ctcb_ptr t; rva = to_bool ret__unsigned_long\<rbrakk> \<Longrightarrow> ccorres dc xfdc (?Pt571 (UCAST(8 \<rightarrow> 32) d) (tcb_ptr_to_ctcb_ptr t) curThread () xfdca () rv' (to_bool ret__unsigned_long) ret__unsigned_long ()) (?Rt567 (UCAST(8 \<rightarrow> 32) d) (tcb_ptr_to_ctcb_ptr t) curThread () xfdca () rv' (to_bool ret__unsigned_long) ret__unsigned_long () rv'a) [SKIP] rescheduleRequired (CALL rescheduleRequired_'proc())
 2. \<And>dom tptr curThread xfdca rv' rva ret__unsigned_long rv'a. \<lbrakk>d \<le> maxDomain; dom = UCAST(8 \<rightarrow> 32) d; tptr = tcb_ptr_to_ctcb_ptr t; rva = to_bool ret__unsigned_long\<rbrakk> \<Longrightarrow> ccorres dc xfdc (?Pf569 (UCAST(8 \<rightarrow> 32) d) (tcb_ptr_to_ctcb_ptr t) curThread () xfdca () rv' (to_bool ret__unsigned_long) ret__unsigned_long ()) (?Rf565 (UCAST(8 \<rightarrow> 32) d) (tcb_ptr_to_ctcb_ptr t) curThread () xfdca () rv' (to_bool ret__unsigned_long) ret__unsigned_long () rv'a) [SKIP] (return ()) SKIP
 3. \<And>dom tptr curThread rv xfdc y rv' rva ret__unsigned_long. \<lbrakk>d \<le> maxDomain; dom = UCAST(8 \<rightarrow> 32) d; tptr = tcb_ptr_to_ctcb_ptr t; dc rv xfdc; dc y rv'; rva = to_bool ret__unsigned_long\<rbrakk> \<Longrightarrow> \<lbrace>?R513 dom tptr curThread rv xfdc y rv' rva\<rbrace> when rva (tcbSchedEnqueue t) \<lbrace>\<lambda>a. (\<lambda>s. curThread = ksCurThread s) and (\<lambda>s. t = curThread \<longrightarrow> ?Pt571 dom tptr curThread rv xfdc y rv' rva ret__unsigned_long a s) and (\<lambda>s. t \<noteq> curThread \<longrightarrow> ?Pf569 dom tptr curThread rv xfdc y rv' rva ret__unsigned_long a s)\<rbrace>
 4. \<And>dom tptr curThread rv xfdca y rv' rva ret__unsigned_long. \<lbrakk>d \<le> maxDomain; dom = UCAST(8 \<rightarrow> 32) d; tptr = tcb_ptr_to_ctcb_ptr t; dc rv xfdca; dc y rv'; rva = to_bool ret__unsigned_long\<rbrakk> \<Longrightarrow> guard_is_UNIV dc xfdc (\<lambda>a b. {s. (s \<in> \<lbrace>tptr = \<acute>ksCurThread\<rbrace> \<longrightarrow> s \<in> ?Rt567 dom tptr curThread rv xfdca y rv' rva ret__unsigned_long a b) \<and> (s \<notin> \<lbrace>tptr = \<acute>ksCurThread\<rbrace> \<longrightarrow> s \<in> ?Rf565 dom tptr curThread rv xfdca y rv' rva ret__unsigned_long a b)})
 5. \<And>dom tptr curThread rv xfdc y rv'. \<lbrakk>d \<le> maxDomain; dom = UCAST(8 \<rightarrow> 32) d; tptr = tcb_ptr_to_ctcb_ptr t; dc rv xfdc; dc y rv'\<rbrakk> \<Longrightarrow> \<lbrace>?R411 dom tptr curThread rv xfdc y\<rbrace> isRunnable t \<lbrace>\<lambda>rva. (\<lambda>_. True) and (\<lambda>s. rva \<longrightarrow> (Invariants_H.valid_queues and tcb_at' t and valid_objs') s) and (\<lambda>s. \<not> rva \<longrightarrow> True) and ?R513 dom tptr curThread rv xfdc y rv' rva\<rbrace>
 6. \<And>dom tptr curThread rv xfdc. \<lbrakk>d \<le> maxDomain; dom = UCAST(8 \<rightarrow> 32) d; tptr = tcb_ptr_to_ctcb_ptr t; dc rv xfdc\<rbrakk> \<Longrightarrow> \<lbrace>?R372 dom tptr curThread rv\<rbrace> threadSet (tcbDomain_update (\<lambda>_. d)) t \<lbrace>\<lambda>y. tcb_at' t and ?R411 dom tptr curThread rv xfdc y\<rbrace>
 7. \<And>dom tptr curThread rv xfdca. \<lbrakk>d \<le> maxDomain; dom = UCAST(8 \<rightarrow> 32) d; tptr = tcb_ptr_to_ctcb_ptr t; dc rv xfdca\<rbrakk> \<Longrightarrow> guard_is_UNIV dc xfdc (\<lambda>y rv'. {s. thread_'_update (\<lambda>_. tptr) s \<in> UNIV \<inter> \<lbrace>\<acute>thread = tcb_ptr_to_ctcb_ptr t\<rbrace>} \<inter> {s'. \<forall>t rv. rv = to_bool (ret__unsigned_long_' t) \<longrightarrow> s'\<lparr>globals := globals t, ret__unsigned_long_' := ret__unsigned_long_' t\<rparr> \<in> {s. (s \<in> \<lbrace>rv\<rbrace> \<longrightarrow> s \<in> {s. tcb_'_update (\<lambda>_. tptr) s \<in> UNIV \<inter> \<lbrace>\<acute>tcb = tptr\<rbrace>}) \<and> (s \<notin> \<lbrace>rv\<rbrace> \<longrightarrow> s \<in> UNIV)}})
 8. \<And>dom tptr curThread. \<lbrakk>d \<le> maxDomain; dom = UCAST(8 \<rightarrow> 32) d; tptr = tcb_ptr_to_ctcb_ptr t\<rbrakk> \<Longrightarrow> \<lbrace>?R343 dom tptr curThread\<rbrace> tcbSchedDequeue t \<lbrace>\<lambda>rv. tcb_at' t and (\<lambda>_. True) and ?R372 dom tptr curThread rv and tcb_at' (ctcb_ptr_to_tcb_ptr tptr)\<rbrace>
 9. \<And>dom tptr s s'. \<lbrakk>d \<le> maxDomain; dom = UCAST(8 \<rightarrow> 32) d; tptr = tcb_ptr_to_ctcb_ptr t; (s, s') \<in> rf_sr; (invs' and tcb_at' t and sch_act_simple) s; s' \<in> UNIV\<rbrakk> \<Longrightarrow> (\<forall>rv. ksCurThread s = rv \<longrightarrow> (Invariants_H.valid_queues and valid_queues' and tcb_at' t and valid_objs' and ?R343 dom tptr rv) s) \<and> s' \<in> {s. \<forall>rv. ksCurThread_' (globals s) = tcb_ptr_to_ctcb_ptr rv \<longrightarrow> s \<in> {s. tcb_'_update (\<lambda>_. tptr) s \<in> UNIV \<inter> \<lbrace>\<acute>tcb = tcb_ptr_to_ctcb_ptr t\<rbrace>} \<inter> {s'. \<forall>t rv. dc rv (xfdc t) \<longrightarrow> s'\<lparr>globals := globals t\<rparr> \<in> UNIV \<inter> \<lbrace>True\<rbrace>}} proof (prove)
goal (8 subgoals):
 1. \<And>dom tptr curThread xfdca rv' rva ret__unsigned_long rv'a. \<lbrakk>d \<le> maxDomain; dom = UCAST(8 \<rightarrow> 32) d; tptr = tcb_ptr_to_ctcb_ptr t; rva = to_bool ret__unsigned_long\<rbrakk> \<Longrightarrow> ccorres dc xfdc (?Pf569 (UCAST(8 \<rightarrow> 32) d) (tcb_ptr_to_ctcb_ptr t) curThread () xfdca () rv' (to_bool ret__unsigned_long) ret__unsigned_long ()) (?Rf565 (UCAST(8 \<rightarrow> 32) d) (tcb_ptr_to_ctcb_ptr t) curThread () xfdca () rv' (to_bool ret__unsigned_long) ret__unsigned_long () rv'a) [SKIP] (return ()) SKIP
 2. \<And>dom tptr curThread rv xfdc y rv' rva ret__unsigned_long. \<lbrakk>d \<le> maxDomain; dom = UCAST(8 \<rightarrow> 32) d; tptr = tcb_ptr_to_ctcb_ptr t; dc rv xfdc; dc y rv'; rva = to_bool ret__unsigned_long\<rbrakk> \<Longrightarrow> \<lbrace>?R513 dom tptr curThread rv xfdc y rv' rva\<rbrace> when rva (tcbSchedEnqueue t) \<lbrace>\<lambda>a. (\<lambda>s. curThread = ksCurThread s) and (\<lambda>s. t = curThread \<longrightarrow> (Invariants_H.valid_queues and (\<lambda>s. weak_sch_act_wf (ksSchedulerAction s) s) and valid_objs') s) and (\<lambda>s. t \<noteq> curThread \<longrightarrow> ?Pf569 dom tptr curThread rv xfdc y rv' rva ret__unsigned_long a s)\<rbrace>
 3. \<And>dom tptr curThread rv xfdca y rv' rva ret__unsigned_long. \<lbrakk>d \<le> maxDomain; dom = UCAST(8 \<rightarrow> 32) d; tptr = tcb_ptr_to_ctcb_ptr t; dc rv xfdca; dc y rv'; rva = to_bool ret__unsigned_long\<rbrakk> \<Longrightarrow> guard_is_UNIV dc xfdc (\<lambda>a b. {s. (s \<in> \<lbrace>tptr = \<acute>ksCurThread\<rbrace> \<longrightarrow> s \<in> {s. s \<in> UNIV}) \<and> (s \<notin> \<lbrace>tptr = \<acute>ksCurThread\<rbrace> \<longrightarrow> s \<in> ?Rf565 dom tptr curThread rv xfdca y rv' rva ret__unsigned_long a b)})
 4. \<And>dom tptr curThread rv xfdc y rv'. \<lbrakk>d \<le> maxDomain; dom = UCAST(8 \<rightarrow> 32) d; tptr = tcb_ptr_to_ctcb_ptr t; dc rv xfdc; dc y rv'\<rbrakk> \<Longrightarrow> \<lbrace>?R411 dom tptr curThread rv xfdc y\<rbrace> isRunnable t \<lbrace>\<lambda>rva. (\<lambda>_. True) and (\<lambda>s. rva \<longrightarrow> (Invariants_H.valid_queues and tcb_at' t and valid_objs') s) and (\<lambda>s. \<not> rva \<longrightarrow> True) and ?R513 dom tptr curThread rv xfdc y rv' rva\<rbrace>
 5. \<And>dom tptr curThread rv xfdc. \<lbrakk>d \<le> maxDomain; dom = UCAST(8 \<rightarrow> 32) d; tptr = tcb_ptr_to_ctcb_ptr t; dc rv xfdc\<rbrakk> \<Longrightarrow> \<lbrace>?R372 dom tptr curThread rv\<rbrace> threadSet (tcbDomain_update (\<lambda>_. d)) t \<lbrace>\<lambda>y. tcb_at' t and ?R411 dom tptr curThread rv xfdc y\<rbrace>
 6. \<And>dom tptr curThread rv xfdca. \<lbrakk>d \<le> maxDomain; dom = UCAST(8 \<rightarrow> 32) d; tptr = tcb_ptr_to_ctcb_ptr t; dc rv xfdca\<rbrakk> \<Longrightarrow> guard_is_UNIV dc xfdc (\<lambda>y rv'. {s. thread_'_update (\<lambda>_. tptr) s \<in> UNIV \<inter> \<lbrace>\<acute>thread = tcb_ptr_to_ctcb_ptr t\<rbrace>} \<inter> {s'. \<forall>t rv. rv = to_bool (ret__unsigned_long_' t) \<longrightarrow> s'\<lparr>globals := globals t, ret__unsigned_long_' := ret__unsigned_long_' t\<rparr> \<in> {s. (s \<in> \<lbrace>rv\<rbrace> \<longrightarrow> s \<in> {s. tcb_'_update (\<lambda>_. tptr) s \<in> UNIV \<inter> \<lbrace>\<acute>tcb = tptr\<rbrace>}) \<and> (s \<notin> \<lbrace>rv\<rbrace> \<longrightarrow> s \<in> UNIV)}})
 7. \<And>dom tptr curThread. \<lbrakk>d \<le> maxDomain; dom = UCAST(8 \<rightarrow> 32) d; tptr = tcb_ptr_to_ctcb_ptr t\<rbrakk> \<Longrightarrow> \<lbrace>?R343 dom tptr curThread\<rbrace> tcbSchedDequeue t \<lbrace>\<lambda>rv. tcb_at' t and (\<lambda>_. True) and ?R372 dom tptr curThread rv and tcb_at' (ctcb_ptr_to_tcb_ptr tptr)\<rbrace>
 8. \<And>dom tptr s s'. \<lbrakk>d \<le> maxDomain; dom = UCAST(8 \<rightarrow> 32) d; tptr = tcb_ptr_to_ctcb_ptr t; (s, s') \<in> rf_sr; (invs' and tcb_at' t and sch_act_simple) s; s' \<in> UNIV\<rbrakk> \<Longrightarrow> (\<forall>rv. ksCurThread s = rv \<longrightarrow> (Invariants_H.valid_queues and valid_queues' and tcb_at' t and valid_objs' and ?R343 dom tptr rv) s) \<and> s' \<in> {s. \<forall>rv. ksCurThread_' (globals s) = tcb_ptr_to_ctcb_ptr rv \<longrightarrow> s \<in> {s. tcb_'_update (\<lambda>_. tptr) s \<in> UNIV \<inter> \<lbrace>\<acute>tcb = tcb_ptr_to_ctcb_ptr t\<rbrace>} \<inter> {s'. \<forall>t rv. dc rv (xfdc t) \<longrightarrow> s'\<lparr>globals := globals t\<rparr> \<in> UNIV \<inter> \<lbrace>True\<rbrace>}} proof (prove)
goal (7 subgoals):
 1. \<And>dom tptr curThread rv xfdc y rv' rva ret__unsigned_long. \<lbrakk>d \<le> maxDomain; dom = UCAST(8 \<rightarrow> 32) d; tptr = tcb_ptr_to_ctcb_ptr t; dc rv xfdc; dc y rv'; rva = to_bool ret__unsigned_long\<rbrakk> \<Longrightarrow> \<lbrace>?R513 dom tptr curThread rv xfdc y rv' rva\<rbrace> when rva (tcbSchedEnqueue t) \<lbrace>\<lambda>a. (\<lambda>s. curThread = ksCurThread s) and (\<lambda>s. t = curThread \<longrightarrow> (Invariants_H.valid_queues and (\<lambda>s. weak_sch_act_wf (ksSchedulerAction s) s) and valid_objs') s) and (\<lambda>s. t \<noteq> curThread \<longrightarrow> True)\<rbrace>
 2. \<And>dom tptr curThread rv xfdca y rv' rva ret__unsigned_long. \<lbrakk>d \<le> maxDomain; dom = UCAST(8 \<rightarrow> 32) d; tptr = tcb_ptr_to_ctcb_ptr t; dc rv xfdca; dc y rv'; rva = to_bool ret__unsigned_long\<rbrakk> \<Longrightarrow> guard_is_UNIV dc xfdc (\<lambda>a b. {s. (s \<in> \<lbrace>tptr = \<acute>ksCurThread\<rbrace> \<longrightarrow> s \<in> {s. s \<in> UNIV}) \<and> (s \<notin> \<lbrace>tptr = \<acute>ksCurThread\<rbrace> \<longrightarrow> s \<in> UNIV \<inter> {s. dc a (xfdc s)})})
 3. \<And>dom tptr curThread rv xfdc y rv'. \<lbrakk>d \<le> maxDomain; dom = UCAST(8 \<rightarrow> 32) d; tptr = tcb_ptr_to_ctcb_ptr t; dc rv xfdc; dc y rv'\<rbrakk> \<Longrightarrow> \<lbrace>?R411 dom tptr curThread rv xfdc y\<rbrace> isRunnable t \<lbrace>\<lambda>rva. (\<lambda>_. True) and (\<lambda>s. rva \<longrightarrow> (Invariants_H.valid_queues and tcb_at' t and valid_objs') s) and (\<lambda>s. \<not> rva \<longrightarrow> True) and ?R513 dom tptr curThread rv xfdc y rv' rva\<rbrace>
 4. \<And>dom tptr curThread rv xfdc. \<lbrakk>d \<le> maxDomain; dom = UCAST(8 \<rightarrow> 32) d; tptr = tcb_ptr_to_ctcb_ptr t; dc rv xfdc\<rbrakk> \<Longrightarrow> \<lbrace>?R372 dom tptr curThread rv\<rbrace> threadSet (tcbDomain_update (\<lambda>_. d)) t \<lbrace>\<lambda>y. tcb_at' t and ?R411 dom tptr curThread rv xfdc y\<rbrace>
 5. \<And>dom tptr curThread rv xfdca. \<lbrakk>d \<le> maxDomain; dom = UCAST(8 \<rightarrow> 32) d; tptr = tcb_ptr_to_ctcb_ptr t; dc rv xfdca\<rbrakk> \<Longrightarrow> guard_is_UNIV dc xfdc (\<lambda>y rv'. {s. thread_'_update (\<lambda>_. tptr) s \<in> UNIV \<inter> \<lbrace>\<acute>thread = tcb_ptr_to_ctcb_ptr t\<rbrace>} \<inter> {s'. \<forall>t rv. rv = to_bool (ret__unsigned_long_' t) \<longrightarrow> s'\<lparr>globals := globals t, ret__unsigned_long_' := ret__unsigned_long_' t\<rparr> \<in> {s. (s \<in> \<lbrace>rv\<rbrace> \<longrightarrow> s \<in> {s. tcb_'_update (\<lambda>_. tptr) s \<in> UNIV \<inter> \<lbrace>\<acute>tcb = tptr\<rbrace>}) \<and> (s \<notin> \<lbrace>rv\<rbrace> \<longrightarrow> s \<in> UNIV)}})
 6. \<And>dom tptr curThread. \<lbrakk>d \<le> maxDomain; dom = UCAST(8 \<rightarrow> 32) d; tptr = tcb_ptr_to_ctcb_ptr t\<rbrakk> \<Longrightarrow> \<lbrace>?R343 dom tptr curThread\<rbrace> tcbSchedDequeue t \<lbrace>\<lambda>rv. tcb_at' t and (\<lambda>_. True) and ?R372 dom tptr curThread rv and tcb_at' (ctcb_ptr_to_tcb_ptr tptr)\<rbrace>
 7. \<And>dom tptr s s'. \<lbrakk>d \<le> maxDomain; dom = UCAST(8 \<rightarrow> 32) d; tptr = tcb_ptr_to_ctcb_ptr t; (s, s') \<in> rf_sr; (invs' and tcb_at' t and sch_act_simple) s; s' \<in> UNIV\<rbrakk> \<Longrightarrow> (\<forall>rv. ksCurThread s = rv \<longrightarrow> (Invariants_H.valid_queues and valid_queues' and tcb_at' t and valid_objs' and ?R343 dom tptr rv) s) \<and> s' \<in> {s. \<forall>rv. ksCurThread_' (globals s) = tcb_ptr_to_ctcb_ptr rv \<longrightarrow> s \<in> {s. tcb_'_update (\<lambda>_. tptr) s \<in> UNIV \<inter> \<lbrace>\<acute>tcb = tcb_ptr_to_ctcb_ptr t\<rbrace>} \<inter> {s'. \<forall>t rv. dc rv (xfdc t) \<longrightarrow> s'\<lparr>globals := globals t\<rparr> \<in> UNIV \<inter> \<lbrace>True\<rbrace>}} proof (prove)
goal (7 subgoals):
 1. \<And>dom tptr curThread xfdc rv' rva ret__unsigned_long. \<lbrakk>d \<le> maxDomain; dom = UCAST(8 \<rightarrow> 32) d; tptr = tcb_ptr_to_ctcb_ptr t; rva = to_bool ret__unsigned_long\<rbrakk> \<Longrightarrow> \<lbrace>?R513 (UCAST(8 \<rightarrow> 32) d) (tcb_ptr_to_ctcb_ptr t) curThread () xfdc () rv' (to_bool ret__unsigned_long)\<rbrace> when (to_bool ret__unsigned_long) (tcbSchedEnqueue t) \<lbrace>\<lambda>a b. curThread = ksCurThread b \<and> (t = curThread \<longrightarrow> Invariants_H.valid_queues b \<and> weak_sch_act_wf (ksSchedulerAction b) b \<and> valid_objs' b)\<rbrace>
 2. \<And>dom tptr curThread rv xfdca y rv' rva ret__unsigned_long. \<lbrakk>d \<le> maxDomain; dom = UCAST(8 \<rightarrow> 32) d; tptr = tcb_ptr_to_ctcb_ptr t; dc rv xfdca; dc y rv'; rva = to_bool ret__unsigned_long\<rbrakk> \<Longrightarrow> guard_is_UNIV dc xfdc (\<lambda>a b. {s. (s \<in> \<lbrace>tptr = \<acute>ksCurThread\<rbrace> \<longrightarrow> s \<in> {s. s \<in> UNIV}) \<and> (s \<notin> \<lbrace>tptr = \<acute>ksCurThread\<rbrace> \<longrightarrow> s \<in> UNIV \<inter> {s. dc a (xfdc s)})})
 3. \<And>dom tptr curThread rv xfdc y rv'. \<lbrakk>d \<le> maxDomain; dom = UCAST(8 \<rightarrow> 32) d; tptr = tcb_ptr_to_ctcb_ptr t; dc rv xfdc; dc y rv'\<rbrakk> \<Longrightarrow> \<lbrace>?R411 dom tptr curThread rv xfdc y\<rbrace> isRunnable t \<lbrace>\<lambda>rva. (\<lambda>_. True) and (\<lambda>s. rva \<longrightarrow> (Invariants_H.valid_queues and tcb_at' t and valid_objs') s) and (\<lambda>s. \<not> rva \<longrightarrow> True) and ?R513 dom tptr curThread rv xfdc y rv' rva\<rbrace>
 4. \<And>dom tptr curThread rv xfdc. \<lbrakk>d \<le> maxDomain; dom = UCAST(8 \<rightarrow> 32) d; tptr = tcb_ptr_to_ctcb_ptr t; dc rv xfdc\<rbrakk> \<Longrightarrow> \<lbrace>?R372 dom tptr curThread rv\<rbrace> threadSet (tcbDomain_update (\<lambda>_. d)) t \<lbrace>\<lambda>y. tcb_at' t and ?R411 dom tptr curThread rv xfdc y\<rbrace>
 5. \<And>dom tptr curThread rv xfdca. \<lbrakk>d \<le> maxDomain; dom = UCAST(8 \<rightarrow> 32) d; tptr = tcb_ptr_to_ctcb_ptr t; dc rv xfdca\<rbrakk> \<Longrightarrow> guard_is_UNIV dc xfdc (\<lambda>y rv'. {s. thread_'_update (\<lambda>_. tptr) s \<in> UNIV \<inter> \<lbrace>\<acute>thread = tcb_ptr_to_ctcb_ptr t\<rbrace>} \<inter> {s'. \<forall>t rv. rv = to_bool (ret__unsigned_long_' t) \<longrightarrow> s'\<lparr>globals := globals t, ret__unsigned_long_' := ret__unsigned_long_' t\<rparr> \<in> {s. (s \<in> \<lbrace>rv\<rbrace> \<longrightarrow> s \<in> {s. tcb_'_update (\<lambda>_. tptr) s \<in> UNIV \<inter> \<lbrace>\<acute>tcb = tptr\<rbrace>}) \<and> (s \<notin> \<lbrace>rv\<rbrace> \<longrightarrow> s \<in> UNIV)}})
 6. \<And>dom tptr curThread. \<lbrakk>d \<le> maxDomain; dom = UCAST(8 \<rightarrow> 32) d; tptr = tcb_ptr_to_ctcb_ptr t\<rbrakk> \<Longrightarrow> \<lbrace>?R343 dom tptr curThread\<rbrace> tcbSchedDequeue t \<lbrace>\<lambda>rv. tcb_at' t and (\<lambda>_. True) and ?R372 dom tptr curThread rv and tcb_at' (ctcb_ptr_to_tcb_ptr tptr)\<rbrace>
 7. \<And>dom tptr s s'. \<lbrakk>d \<le> maxDomain; dom = UCAST(8 \<rightarrow> 32) d; tptr = tcb_ptr_to_ctcb_ptr t; (s, s') \<in> rf_sr; (invs' and tcb_at' t and sch_act_simple) s; s' \<in> UNIV\<rbrakk> \<Longrightarrow> (\<forall>rv. ksCurThread s = rv \<longrightarrow> (Invariants_H.valid_queues and valid_queues' and tcb_at' t and valid_objs' and ?R343 dom tptr rv) s) \<and> s' \<in> {s. \<forall>rv. ksCurThread_' (globals s) = tcb_ptr_to_ctcb_ptr rv \<longrightarrow> s \<in> {s. tcb_'_update (\<lambda>_. tptr) s \<in> UNIV \<inter> \<lbrace>\<acute>tcb = tcb_ptr_to_ctcb_ptr t\<rbrace>} \<inter> {s'. \<forall>t rv. dc rv (xfdc t) \<longrightarrow> s'\<lparr>globals := globals t\<rparr> \<in> UNIV \<inter> \<lbrace>True\<rbrace>}} proof (prove)
goal (6 subgoals):
 1. \<And>dom tptr curThread rv xfdca y rv' rva ret__unsigned_long. \<lbrakk>d \<le> maxDomain; dom = UCAST(8 \<rightarrow> 32) d; tptr = tcb_ptr_to_ctcb_ptr t; dc rv xfdca; dc y rv'; rva = to_bool ret__unsigned_long\<rbrakk> \<Longrightarrow> guard_is_UNIV dc xfdc (\<lambda>a b. {s. (s \<in> \<lbrace>tptr = \<acute>ksCurThread\<rbrace> \<longrightarrow> s \<in> {s. s \<in> UNIV}) \<and> (s \<notin> \<lbrace>tptr = \<acute>ksCurThread\<rbrace> \<longrightarrow> s \<in> UNIV \<inter> {s. dc a (xfdc s)})})
 2. \<And>dom tptr curThread rv xfdc y rv'. \<lbrakk>d \<le> maxDomain; dom = UCAST(8 \<rightarrow> 32) d; tptr = tcb_ptr_to_ctcb_ptr t; dc rv xfdc; dc y rv'\<rbrakk> \<Longrightarrow> \<lbrace>?R411 dom tptr curThread rv xfdc y\<rbrace> isRunnable t \<lbrace>\<lambda>rva. (\<lambda>_. True) and (\<lambda>s. rva \<longrightarrow> (Invariants_H.valid_queues and tcb_at' t and valid_objs') s) and (\<lambda>s. \<not> rva \<longrightarrow> True) and (if rva then \<lambda>a. curThread = ksCurThread a \<and> (Invariants_H.valid_queues and st_tcb_at' runnable' t and valid_objs') a \<and> weak_sch_act_wf (ksSchedulerAction a) a \<and> valid_objs' a else (\<lambda>a. curThread = ksCurThread a \<and> (t = curThread \<longrightarrow> Invariants_H.valid_queues a \<and> weak_sch_act_wf (ksSchedulerAction a) a \<and> valid_objs' a)))\<rbrace>
 3. \<And>dom tptr curThread rv xfdc. \<lbrakk>d \<le> maxDomain; dom = UCAST(8 \<rightarrow> 32) d; tptr = tcb_ptr_to_ctcb_ptr t; dc rv xfdc\<rbrakk> \<Longrightarrow> \<lbrace>?R372 dom tptr curThread rv\<rbrace> threadSet (tcbDomain_update (\<lambda>_. d)) t \<lbrace>\<lambda>y. tcb_at' t and ?R411 dom tptr curThread rv xfdc y\<rbrace>
 4. \<And>dom tptr curThread rv xfdca. \<lbrakk>d \<le> maxDomain; dom = UCAST(8 \<rightarrow> 32) d; tptr = tcb_ptr_to_ctcb_ptr t; dc rv xfdca\<rbrakk> \<Longrightarrow> guard_is_UNIV dc xfdc (\<lambda>y rv'. {s. thread_'_update (\<lambda>_. tptr) s \<in> UNIV \<inter> \<lbrace>\<acute>thread = tcb_ptr_to_ctcb_ptr t\<rbrace>} \<inter> {s'. \<forall>t rv. rv = to_bool (ret__unsigned_long_' t) \<longrightarrow> s'\<lparr>globals := globals t, ret__unsigned_long_' := ret__unsigned_long_' t\<rparr> \<in> {s. (s \<in> \<lbrace>rv\<rbrace> \<longrightarrow> s \<in> {s. tcb_'_update (\<lambda>_. tptr) s \<in> UNIV \<inter> \<lbrace>\<acute>tcb = tptr\<rbrace>}) \<and> (s \<notin> \<lbrace>rv\<rbrace> \<longrightarrow> s \<in> UNIV)}})
 5. \<And>dom tptr curThread. \<lbrakk>d \<le> maxDomain; dom = UCAST(8 \<rightarrow> 32) d; tptr = tcb_ptr_to_ctcb_ptr t\<rbrakk> \<Longrightarrow> \<lbrace>?R343 dom tptr curThread\<rbrace> tcbSchedDequeue t \<lbrace>\<lambda>rv. tcb_at' t and (\<lambda>_. True) and ?R372 dom tptr curThread rv and tcb_at' (ctcb_ptr_to_tcb_ptr tptr)\<rbrace>
 6. \<And>dom tptr s s'. \<lbrakk>d \<le> maxDomain; dom = UCAST(8 \<rightarrow> 32) d; tptr = tcb_ptr_to_ctcb_ptr t; (s, s') \<in> rf_sr; (invs' and tcb_at' t and sch_act_simple) s; s' \<in> UNIV\<rbrakk> \<Longrightarrow> (\<forall>rv. ksCurThread s = rv \<longrightarrow> (Invariants_H.valid_queues and valid_queues' and tcb_at' t and valid_objs' and ?R343 dom tptr rv) s) \<and> s' \<in> {s. \<forall>rv. ksCurThread_' (globals s) = tcb_ptr_to_ctcb_ptr rv \<longrightarrow> s \<in> {s. tcb_'_update (\<lambda>_. tptr) s \<in> UNIV \<inter> \<lbrace>\<acute>tcb = tcb_ptr_to_ctcb_ptr t\<rbrace>} \<inter> {s'. \<forall>t rv. dc rv (xfdc t) \<longrightarrow> s'\<lparr>globals := globals t\<rparr> \<in> UNIV \<inter> \<lbrace>True\<rbrace>}} proof (prove)
goal (5 subgoals):
 1. \<And>dom tptr curThread rv xfdc y rv'. \<lbrakk>d \<le> maxDomain; dom = UCAST(8 \<rightarrow> 32) d; tptr = tcb_ptr_to_ctcb_ptr t; dc rv xfdc; dc y rv'\<rbrakk> \<Longrightarrow> \<lbrace>?R411 dom tptr curThread rv xfdc y\<rbrace> isRunnable t \<lbrace>\<lambda>rva. (\<lambda>_. True) and (\<lambda>s. rva \<longrightarrow> (Invariants_H.valid_queues and tcb_at' t and valid_objs') s) and (\<lambda>s. \<not> rva \<longrightarrow> True) and (if rva then \<lambda>a. curThread = ksCurThread a \<and> (Invariants_H.valid_queues and st_tcb_at' runnable' t and valid_objs') a \<and> weak_sch_act_wf (ksSchedulerAction a) a \<and> valid_objs' a else (\<lambda>a. curThread = ksCurThread a \<and> (t = curThread \<longrightarrow> Invariants_H.valid_queues a \<and> weak_sch_act_wf (ksSchedulerAction a) a \<and> valid_objs' a)))\<rbrace>
 2. \<And>dom tptr curThread rv xfdc. \<lbrakk>d \<le> maxDomain; dom = UCAST(8 \<rightarrow> 32) d; tptr = tcb_ptr_to_ctcb_ptr t; dc rv xfdc\<rbrakk> \<Longrightarrow> \<lbrace>?R372 dom tptr curThread rv\<rbrace> threadSet (tcbDomain_update (\<lambda>_. d)) t \<lbrace>\<lambda>y. tcb_at' t and ?R411 dom tptr curThread rv xfdc y\<rbrace>
 3. \<And>dom tptr curThread rv xfdca. \<lbrakk>d \<le> maxDomain; dom = UCAST(8 \<rightarrow> 32) d; tptr = tcb_ptr_to_ctcb_ptr t; dc rv xfdca\<rbrakk> \<Longrightarrow> guard_is_UNIV dc xfdc (\<lambda>y rv'. {s. thread_'_update (\<lambda>_. tptr) s \<in> UNIV \<inter> \<lbrace>\<acute>thread = tcb_ptr_to_ctcb_ptr t\<rbrace>} \<inter> {s'. \<forall>t rv. rv = to_bool (ret__unsigned_long_' t) \<longrightarrow> s'\<lparr>globals := globals t, ret__unsigned_long_' := ret__unsigned_long_' t\<rparr> \<in> {s. (s \<in> \<lbrace>rv\<rbrace> \<longrightarrow> s \<in> {s. tcb_'_update (\<lambda>_. tptr) s \<in> UNIV \<inter> \<lbrace>\<acute>tcb = tptr\<rbrace>}) \<and> (s \<notin> \<lbrace>rv\<rbrace> \<longrightarrow> s \<in> UNIV)}})
 4. \<And>dom tptr curThread. \<lbrakk>d \<le> maxDomain; dom = UCAST(8 \<rightarrow> 32) d; tptr = tcb_ptr_to_ctcb_ptr t\<rbrakk> \<Longrightarrow> \<lbrace>?R343 dom tptr curThread\<rbrace> tcbSchedDequeue t \<lbrace>\<lambda>rv. tcb_at' t and (\<lambda>_. True) and ?R372 dom tptr curThread rv and tcb_at' (ctcb_ptr_to_tcb_ptr tptr)\<rbrace>
 5. \<And>dom tptr s s'. \<lbrakk>d \<le> maxDomain; dom = UCAST(8 \<rightarrow> 32) d; tptr = tcb_ptr_to_ctcb_ptr t; (s, s') \<in> rf_sr; (invs' and tcb_at' t and sch_act_simple) s; s' \<in> UNIV\<rbrakk> \<Longrightarrow> (\<forall>rv. ksCurThread s = rv \<longrightarrow> (Invariants_H.valid_queues and valid_queues' and tcb_at' t and valid_objs' and ?R343 dom tptr rv) s) \<and> s' \<in> {s. \<forall>rv. ksCurThread_' (globals s) = tcb_ptr_to_ctcb_ptr rv \<longrightarrow> s \<in> {s. tcb_'_update (\<lambda>_. tptr) s \<in> UNIV \<inter> \<lbrace>\<acute>tcb = tcb_ptr_to_ctcb_ptr t\<rbrace>} \<inter> {s'. \<forall>t rv. dc rv (xfdc t) \<longrightarrow> s'\<lparr>globals := globals t\<rparr> \<in> UNIV \<inter> \<lbrace>True\<rbrace>}} proof (prove)
goal (5 subgoals):
 1. \<And>dom tptr curThread xfdc. \<lbrakk>d \<le> maxDomain; dom = UCAST(8 \<rightarrow> 32) d; tptr = tcb_ptr_to_ctcb_ptr t\<rbrakk> \<Longrightarrow> \<lbrace>?R411 (UCAST(8 \<rightarrow> 32) d) (tcb_ptr_to_ctcb_ptr t) curThread () xfdc ()\<rbrace> isRunnable t \<lbrace>\<lambda>rva. (\<lambda>a. rva \<longrightarrow> Invariants_H.valid_queues a \<and> tcb_at' t a \<and> valid_objs' a) and (if rva then \<lambda>a. curThread = ksCurThread a \<and> (Invariants_H.valid_queues and st_tcb_at' runnable' t and valid_objs') a \<and> weak_sch_act_wf (ksSchedulerAction a) a \<and> valid_objs' a else (\<lambda>a. curThread = ksCurThread a \<and> (t = curThread \<longrightarrow> Invariants_H.valid_queues a \<and> weak_sch_act_wf (ksSchedulerAction a) a \<and> valid_objs' a)))\<rbrace>
 2. \<And>dom tptr curThread rv xfdc. \<lbrakk>d \<le> maxDomain; dom = UCAST(8 \<rightarrow> 32) d; tptr = tcb_ptr_to_ctcb_ptr t; dc rv xfdc\<rbrakk> \<Longrightarrow> \<lbrace>?R372 dom tptr curThread rv\<rbrace> threadSet (tcbDomain_update (\<lambda>_. d)) t \<lbrace>\<lambda>y. tcb_at' t and ?R411 dom tptr curThread rv xfdc y\<rbrace>
 3. \<And>dom tptr curThread rv xfdca. \<lbrakk>d \<le> maxDomain; dom = UCAST(8 \<rightarrow> 32) d; tptr = tcb_ptr_to_ctcb_ptr t; dc rv xfdca\<rbrakk> \<Longrightarrow> guard_is_UNIV dc xfdc (\<lambda>y rv'. {s. thread_'_update (\<lambda>_. tptr) s \<in> UNIV \<inter> \<lbrace>\<acute>thread = tcb_ptr_to_ctcb_ptr t\<rbrace>} \<inter> {s'. \<forall>t rv. rv = to_bool (ret__unsigned_long_' t) \<longrightarrow> s'\<lparr>globals := globals t, ret__unsigned_long_' := ret__unsigned_long_' t\<rparr> \<in> {s. (s \<in> \<lbrace>rv\<rbrace> \<longrightarrow> s \<in> {s. tcb_'_update (\<lambda>_. tptr) s \<in> UNIV \<inter> \<lbrace>\<acute>tcb = tptr\<rbrace>}) \<and> (s \<notin> \<lbrace>rv\<rbrace> \<longrightarrow> s \<in> UNIV)}})
 4. \<And>dom tptr curThread. \<lbrakk>d \<le> maxDomain; dom = UCAST(8 \<rightarrow> 32) d; tptr = tcb_ptr_to_ctcb_ptr t\<rbrakk> \<Longrightarrow> \<lbrace>?R343 dom tptr curThread\<rbrace> tcbSchedDequeue t \<lbrace>\<lambda>rv. tcb_at' t and (\<lambda>_. True) and ?R372 dom tptr curThread rv and tcb_at' (ctcb_ptr_to_tcb_ptr tptr)\<rbrace>
 5. \<And>dom tptr s s'. \<lbrakk>d \<le> maxDomain; dom = UCAST(8 \<rightarrow> 32) d; tptr = tcb_ptr_to_ctcb_ptr t; (s, s') \<in> rf_sr; (invs' and tcb_at' t and sch_act_simple) s; s' \<in> UNIV\<rbrakk> \<Longrightarrow> (\<forall>rv. ksCurThread s = rv \<longrightarrow> (Invariants_H.valid_queues and valid_queues' and tcb_at' t and valid_objs' and ?R343 dom tptr rv) s) \<and> s' \<in> {s. \<forall>rv. ksCurThread_' (globals s) = tcb_ptr_to_ctcb_ptr rv \<longrightarrow> s \<in> {s. tcb_'_update (\<lambda>_. tptr) s \<in> UNIV \<inter> \<lbrace>\<acute>tcb = tcb_ptr_to_ctcb_ptr t\<rbrace>} \<inter> {s'. \<forall>t rv. dc rv (xfdc t) \<longrightarrow> s'\<lparr>globals := globals t\<rparr> \<in> UNIV \<inter> \<lbrace>True\<rbrace>}} proof (prove)
goal (4 subgoals):
 1. \<And>dom tptr curThread rv xfdc. \<lbrakk>d \<le> maxDomain; dom = UCAST(8 \<rightarrow> 32) d; tptr = tcb_ptr_to_ctcb_ptr t; dc rv xfdc\<rbrakk> \<Longrightarrow> \<lbrace>?R372 dom tptr curThread rv\<rbrace> threadSet (tcbDomain_update (\<lambda>_. d)) t \<lbrace>\<lambda>y. tcb_at' t and (\<lambda>a. ((\<lambda>b. st_tcb_at' runnable' t a \<longrightarrow> Invariants_H.valid_queues b \<and> tcb_at' t b \<and> valid_objs' b) and (if st_tcb_at' runnable' t a then \<lambda>a. curThread = ksCurThread a \<and> (Invariants_H.valid_queues and st_tcb_at' runnable' t and valid_objs') a \<and> weak_sch_act_wf (ksSchedulerAction a) a \<and> valid_objs' a else (\<lambda>a. curThread = ksCurThread a \<and> (t = curThread \<longrightarrow> Invariants_H.valid_queues a \<and> weak_sch_act_wf (ksSchedulerAction a) a \<and> valid_objs' a)))) a)\<rbrace>
 2. \<And>dom tptr curThread rv xfdca. \<lbrakk>d \<le> maxDomain; dom = UCAST(8 \<rightarrow> 32) d; tptr = tcb_ptr_to_ctcb_ptr t; dc rv xfdca\<rbrakk> \<Longrightarrow> guard_is_UNIV dc xfdc (\<lambda>y rv'. {s. thread_'_update (\<lambda>_. tptr) s \<in> UNIV \<inter> \<lbrace>\<acute>thread = tcb_ptr_to_ctcb_ptr t\<rbrace>} \<inter> {s'. \<forall>t rv. rv = to_bool (ret__unsigned_long_' t) \<longrightarrow> s'\<lparr>globals := globals t, ret__unsigned_long_' := ret__unsigned_long_' t\<rparr> \<in> {s. (s \<in> \<lbrace>rv\<rbrace> \<longrightarrow> s \<in> {s. tcb_'_update (\<lambda>_. tptr) s \<in> UNIV \<inter> \<lbrace>\<acute>tcb = tptr\<rbrace>}) \<and> (s \<notin> \<lbrace>rv\<rbrace> \<longrightarrow> s \<in> UNIV)}})
 3. \<And>dom tptr curThread. \<lbrakk>d \<le> maxDomain; dom = UCAST(8 \<rightarrow> 32) d; tptr = tcb_ptr_to_ctcb_ptr t\<rbrakk> \<Longrightarrow> \<lbrace>?R343 dom tptr curThread\<rbrace> tcbSchedDequeue t \<lbrace>\<lambda>rv. tcb_at' t and (\<lambda>_. True) and ?R372 dom tptr curThread rv and tcb_at' (ctcb_ptr_to_tcb_ptr tptr)\<rbrace>
 4. \<And>dom tptr s s'. \<lbrakk>d \<le> maxDomain; dom = UCAST(8 \<rightarrow> 32) d; tptr = tcb_ptr_to_ctcb_ptr t; (s, s') \<in> rf_sr; (invs' and tcb_at' t and sch_act_simple) s; s' \<in> UNIV\<rbrakk> \<Longrightarrow> (\<forall>rv. ksCurThread s = rv \<longrightarrow> (Invariants_H.valid_queues and valid_queues' and tcb_at' t and valid_objs' and ?R343 dom tptr rv) s) \<and> s' \<in> {s. \<forall>rv. ksCurThread_' (globals s) = tcb_ptr_to_ctcb_ptr rv \<longrightarrow> s \<in> {s. tcb_'_update (\<lambda>_. tptr) s \<in> UNIV \<inter> \<lbrace>\<acute>tcb = tcb_ptr_to_ctcb_ptr t\<rbrace>} \<inter> {s'. \<forall>t rv. dc rv (xfdc t) \<longrightarrow> s'\<lparr>globals := globals t\<rparr> \<in> UNIV \<inter> \<lbrace>True\<rbrace>}} proof (prove)
goal (5 subgoals):
 1. \<And>dom tptr curThread rv xfdc. \<lbrakk>d \<le> maxDomain; dom = UCAST(8 \<rightarrow> 32) d; tptr = tcb_ptr_to_ctcb_ptr t; dc rv xfdc\<rbrakk> \<Longrightarrow> \<lbrace>?R372 dom tptr curThread rv\<rbrace> threadSet (tcbDomain_update (\<lambda>_. d)) t \<lbrace>\<lambda>_. (\<lambda>s. valid_pspace' s \<and> Invariants_H.valid_queues s \<and> sym_refs (state_refs_of' s) \<and> if_live_then_nonz_cap' s \<and> if_unsafe_then_cap' s \<and> valid_idle' s \<and> valid_global_refs' s \<and> valid_arch_state' s \<and> valid_irq_node' (irq_node' s) s \<and> valid_irq_handlers' s \<and> valid_irq_states' s \<and> irqs_masked' s \<and> valid_machine_state' s \<and> cur_tcb' s \<and> untyped_ranges_zero' s \<and> valid_queues' s \<and> valid_pde_mappings' s \<and> pspace_domain_valid s \<and> ksCurDomain s \<le> maxDomain \<and> valid_dom_schedule' s \<and> (\<forall>x. ksSchedulerAction s = SwitchToThread x \<longrightarrow> st_tcb_at' runnable' x s)) and tcb_at' t and sch_act_simple and (\<lambda>s. curThread = ksCurThread s)\<rbrace>
 2. \<And>dom tptr curThread rv xfdc rva s. \<lbrakk>d \<le> maxDomain; dom = UCAST(8 \<rightarrow> 32) d; tptr = tcb_ptr_to_ctcb_ptr t; dc rv xfdc; ((\<lambda>s. valid_pspace' s \<and> Invariants_H.valid_queues s \<and> sym_refs (state_refs_of' s) \<and> if_live_then_nonz_cap' s \<and> if_unsafe_then_cap' s \<and> valid_idle' s \<and> valid_global_refs' s \<and> valid_arch_state' s \<and> valid_irq_node' (irq_node' s) s \<and> valid_irq_handlers' s \<and> valid_irq_states' s \<and> irqs_masked' s \<and> valid_machine_state' s \<and> cur_tcb' s \<and> untyped_ranges_zero' s \<and> valid_queues' s \<and> valid_pde_mappings' s \<and> pspace_domain_valid s \<and> ksCurDomain s \<le> maxDomain \<and> valid_dom_schedule' s \<and> (\<forall>x. ksSchedulerAction s = SwitchToThread x \<longrightarrow> st_tcb_at' runnable' x s)) and tcb_at' t and sch_act_simple and (\<lambda>s. curThread = ksCurThread s)) s\<rbrakk> \<Longrightarrow> (tcb_at' t and (\<lambda>a. ((\<lambda>b. st_tcb_at' runnable' t a \<longrightarrow> Invariants_H.valid_queues b \<and> tcb_at' t b \<and> valid_objs' b) and (if st_tcb_at' runnable' t a then \<lambda>a. curThread = ksCurThread a \<and> (Invariants_H.valid_queues and st_tcb_at' runnable' t and valid_objs') a \<and> weak_sch_act_wf (ksSchedulerAction a) a \<and> valid_objs' a else (\<lambda>a. curThread = ksCurThread a \<and> (t = curThread \<longrightarrow> Invariants_H.valid_queues a \<and> weak_sch_act_wf (ksSchedulerAction a) a \<and> valid_objs' a)))) a)) s
 3. \<And>dom tptr curThread rv xfdca. \<lbrakk>d \<le> maxDomain; dom = UCAST(8 \<rightarrow> 32) d; tptr = tcb_ptr_to_ctcb_ptr t; dc rv xfdca\<rbrakk> \<Longrightarrow> guard_is_UNIV dc xfdc (\<lambda>y rv'. {s. thread_'_update (\<lambda>_. tptr) s \<in> UNIV \<inter> \<lbrace>\<acute>thread = tcb_ptr_to_ctcb_ptr t\<rbrace>} \<inter> {s'. \<forall>t rv. rv = to_bool (ret__unsigned_long_' t) \<longrightarrow> s'\<lparr>globals := globals t, ret__unsigned_long_' := ret__unsigned_long_' t\<rparr> \<in> {s. (s \<in> \<lbrace>rv\<rbrace> \<longrightarrow> s \<in> {s. tcb_'_update (\<lambda>_. tptr) s \<in> UNIV \<inter> \<lbrace>\<acute>tcb = tptr\<rbrace>}) \<and> (s \<notin> \<lbrace>rv\<rbrace> \<longrightarrow> s \<in> UNIV)}})
 4. \<And>dom tptr curThread. \<lbrakk>d \<le> maxDomain; dom = UCAST(8 \<rightarrow> 32) d; tptr = tcb_ptr_to_ctcb_ptr t\<rbrakk> \<Longrightarrow> \<lbrace>?R343 dom tptr curThread\<rbrace> tcbSchedDequeue t \<lbrace>\<lambda>rv. tcb_at' t and (\<lambda>_. True) and ?R372 dom tptr curThread rv and tcb_at' (ctcb_ptr_to_tcb_ptr tptr)\<rbrace>
 5. \<And>dom tptr s s'. \<lbrakk>d \<le> maxDomain; dom = UCAST(8 \<rightarrow> 32) d; tptr = tcb_ptr_to_ctcb_ptr t; (s, s') \<in> rf_sr; (invs' and tcb_at' t and sch_act_simple) s; s' \<in> UNIV\<rbrakk> \<Longrightarrow> (\<forall>rv. ksCurThread s = rv \<longrightarrow> (Invariants_H.valid_queues and valid_queues' and tcb_at' t and valid_objs' and ?R343 dom tptr rv) s) \<and> s' \<in> {s. \<forall>rv. ksCurThread_' (globals s) = tcb_ptr_to_ctcb_ptr rv \<longrightarrow> s \<in> {s. tcb_'_update (\<lambda>_. tptr) s \<in> UNIV \<inter> \<lbrace>\<acute>tcb = tcb_ptr_to_ctcb_ptr t\<rbrace>} \<inter> {s'. \<forall>t rv. dc rv (xfdc t) \<longrightarrow> s'\<lparr>globals := globals t\<rparr> \<in> UNIV \<inter> \<lbrace>True\<rbrace>}} proof (prove)
goal (4 subgoals):
 1. \<And>dom tptr curThread rv xfdc rva s. \<lbrakk>d \<le> maxDomain; dom = UCAST(8 \<rightarrow> 32) d; tptr = tcb_ptr_to_ctcb_ptr t; dc rv xfdc; ((\<lambda>s. valid_pspace' s \<and> Invariants_H.valid_queues s \<and> sym_refs (state_refs_of' s) \<and> if_live_then_nonz_cap' s \<and> if_unsafe_then_cap' s \<and> valid_idle' s \<and> valid_global_refs' s \<and> valid_arch_state' s \<and> valid_irq_node' (irq_node' s) s \<and> valid_irq_handlers' s \<and> valid_irq_states' s \<and> irqs_masked' s \<and> valid_machine_state' s \<and> cur_tcb' s \<and> untyped_ranges_zero' s \<and> valid_queues' s \<and> valid_pde_mappings' s \<and> pspace_domain_valid s \<and> ksCurDomain s \<le> maxDomain \<and> valid_dom_schedule' s \<and> (\<forall>x. ksSchedulerAction s = SwitchToThread x \<longrightarrow> st_tcb_at' runnable' x s)) and tcb_at' t and sch_act_simple and (\<lambda>s. curThread = ksCurThread s)) s\<rbrakk> \<Longrightarrow> (tcb_at' t and (\<lambda>a. ((\<lambda>b. st_tcb_at' runnable' t a \<longrightarrow> Invariants_H.valid_queues b \<and> tcb_at' t b \<and> valid_objs' b) and (if st_tcb_at' runnable' t a then \<lambda>a. curThread = ksCurThread a \<and> (Invariants_H.valid_queues and st_tcb_at' runnable' t and valid_objs') a \<and> weak_sch_act_wf (ksSchedulerAction a) a \<and> valid_objs' a else (\<lambda>a. curThread = ksCurThread a \<and> (t = curThread \<longrightarrow> Invariants_H.valid_queues a \<and> weak_sch_act_wf (ksSchedulerAction a) a \<and> valid_objs' a)))) a)) s
 2. \<And>dom tptr curThread rv xfdca. \<lbrakk>d \<le> maxDomain; dom = UCAST(8 \<rightarrow> 32) d; tptr = tcb_ptr_to_ctcb_ptr t; dc rv xfdca\<rbrakk> \<Longrightarrow> guard_is_UNIV dc xfdc (\<lambda>y rv'. {s. thread_'_update (\<lambda>_. tptr) s \<in> UNIV \<inter> \<lbrace>\<acute>thread = tcb_ptr_to_ctcb_ptr t\<rbrace>} \<inter> {s'. \<forall>t rv. rv = to_bool (ret__unsigned_long_' t) \<longrightarrow> s'\<lparr>globals := globals t, ret__unsigned_long_' := ret__unsigned_long_' t\<rparr> \<in> {s. (s \<in> \<lbrace>rv\<rbrace> \<longrightarrow> s \<in> {s. tcb_'_update (\<lambda>_. tptr) s \<in> UNIV \<inter> \<lbrace>\<acute>tcb = tptr\<rbrace>}) \<and> (s \<notin> \<lbrace>rv\<rbrace> \<longrightarrow> s \<in> UNIV)}})
 3. \<And>dom tptr curThread. \<lbrakk>d \<le> maxDomain; dom = UCAST(8 \<rightarrow> 32) d; tptr = tcb_ptr_to_ctcb_ptr t\<rbrakk> \<Longrightarrow> \<lbrace>?R343 dom tptr curThread\<rbrace> tcbSchedDequeue t \<lbrace>\<lambda>rv. tcb_at' t and (\<lambda>_. True) and (\<lambda>s. (tcb_at' t and (\<lambda>s. \<forall>p. t \<notin> set (ksReadyQueues s p)) and (\<lambda>s. valid_pspace' s \<and> Invariants_H.valid_queues s \<and> sym_refs (state_refs_of' s) \<and> if_live_then_nonz_cap' s \<and> if_unsafe_then_cap' s \<and> valid_idle' s \<and> valid_global_refs' s \<and> valid_arch_state' s \<and> valid_irq_node' (irq_node' s) s \<and> valid_irq_handlers' s \<and> valid_irq_states' s \<and> irqs_masked' s \<and> valid_machine_state' s \<and> cur_tcb' s \<and> untyped_ranges_zero' s \<and> valid_queues' s \<and> valid_pde_mappings' s \<and> pspace_domain_valid s \<and> ksCurDomain s \<le> maxDomain \<and> valid_dom_schedule' s \<and> (\<forall>x. ksSchedulerAction s = SwitchToThread x \<longrightarrow> st_tcb_at' runnable' x s)) and sch_act_simple and K (d \<le> maxDomain)) s \<and> obj_at' (\<lambda>obj. if t = t then True else True) t s \<and> sch_act_simple s \<and> curThread = ksCurThread s) and tcb_at' (ctcb_ptr_to_tcb_ptr tptr)\<rbrace>
 4. \<And>dom tptr s s'. \<lbrakk>d \<le> maxDomain; dom = UCAST(8 \<rightarrow> 32) d; tptr = tcb_ptr_to_ctcb_ptr t; (s, s') \<in> rf_sr; (invs' and tcb_at' t and sch_act_simple) s; s' \<in> UNIV\<rbrakk> \<Longrightarrow> (\<forall>rv. ksCurThread s = rv \<longrightarrow> (Invariants_H.valid_queues and valid_queues' and tcb_at' t and valid_objs' and ?R343 dom tptr rv) s) \<and> s' \<in> {s. \<forall>rv. ksCurThread_' (globals s) = tcb_ptr_to_ctcb_ptr rv \<longrightarrow> s \<in> {s. tcb_'_update (\<lambda>_. tptr) s \<in> UNIV \<inter> \<lbrace>\<acute>tcb = tcb_ptr_to_ctcb_ptr t\<rbrace>} \<inter> {s'. \<forall>t rv. dc rv (xfdc t) \<longrightarrow> s'\<lparr>globals := globals t\<rparr> \<in> UNIV \<inter> \<lbrace>True\<rbrace>}} proof (prove)
goal (3 subgoals):
 1. \<And>dom tptr curThread rv xfdca. \<lbrakk>d \<le> maxDomain; dom = UCAST(8 \<rightarrow> 32) d; tptr = tcb_ptr_to_ctcb_ptr t; dc rv xfdca\<rbrakk> \<Longrightarrow> guard_is_UNIV dc xfdc (\<lambda>y rv'. {s. thread_'_update (\<lambda>_. tptr) s \<in> UNIV \<inter> \<lbrace>\<acute>thread = tcb_ptr_to_ctcb_ptr t\<rbrace>} \<inter> {s'. \<forall>t rv. rv = to_bool (ret__unsigned_long_' t) \<longrightarrow> s'\<lparr>globals := globals t, ret__unsigned_long_' := ret__unsigned_long_' t\<rparr> \<in> {s. (s \<in> \<lbrace>rv\<rbrace> \<longrightarrow> s \<in> {s. tcb_'_update (\<lambda>_. tptr) s \<in> UNIV \<inter> \<lbrace>\<acute>tcb = tptr\<rbrace>}) \<and> (s \<notin> \<lbrace>rv\<rbrace> \<longrightarrow> s \<in> UNIV)}})
 2. \<And>dom tptr curThread. \<lbrakk>d \<le> maxDomain; dom = UCAST(8 \<rightarrow> 32) d; tptr = tcb_ptr_to_ctcb_ptr t\<rbrakk> \<Longrightarrow> \<lbrace>?R343 dom tptr curThread\<rbrace> tcbSchedDequeue t \<lbrace>\<lambda>rv. tcb_at' t and (\<lambda>_. True) and (\<lambda>s. (tcb_at' t and (\<lambda>s. \<forall>p. t \<notin> set (ksReadyQueues s p)) and (\<lambda>s. valid_pspace' s \<and> Invariants_H.valid_queues s \<and> sym_refs (state_refs_of' s) \<and> if_live_then_nonz_cap' s \<and> if_unsafe_then_cap' s \<and> valid_idle' s \<and> valid_global_refs' s \<and> valid_arch_state' s \<and> valid_irq_node' (irq_node' s) s \<and> valid_irq_handlers' s \<and> valid_irq_states' s \<and> irqs_masked' s \<and> valid_machine_state' s \<and> cur_tcb' s \<and> untyped_ranges_zero' s \<and> valid_queues' s \<and> valid_pde_mappings' s \<and> pspace_domain_valid s \<and> ksCurDomain s \<le> maxDomain \<and> valid_dom_schedule' s \<and> (\<forall>x. ksSchedulerAction s = SwitchToThread x \<longrightarrow> st_tcb_at' runnable' x s)) and sch_act_simple and K (d \<le> maxDomain)) s \<and> obj_at' (\<lambda>obj. if t = t then True else True) t s \<and> sch_act_simple s \<and> curThread = ksCurThread s) and tcb_at' (ctcb_ptr_to_tcb_ptr tptr)\<rbrace>
 3. \<And>dom tptr s s'. \<lbrakk>d \<le> maxDomain; dom = UCAST(8 \<rightarrow> 32) d; tptr = tcb_ptr_to_ctcb_ptr t; (s, s') \<in> rf_sr; (invs' and tcb_at' t and sch_act_simple) s; s' \<in> UNIV\<rbrakk> \<Longrightarrow> (\<forall>rv. ksCurThread s = rv \<longrightarrow> (Invariants_H.valid_queues and valid_queues' and tcb_at' t and valid_objs' and ?R343 dom tptr rv) s) \<and> s' \<in> {s. \<forall>rv. ksCurThread_' (globals s) = tcb_ptr_to_ctcb_ptr rv \<longrightarrow> s \<in> {s. tcb_'_update (\<lambda>_. tptr) s \<in> UNIV \<inter> \<lbrace>\<acute>tcb = tcb_ptr_to_ctcb_ptr t\<rbrace>} \<inter> {s'. \<forall>t rv. dc rv (xfdc t) \<longrightarrow> s'\<lparr>globals := globals t\<rparr> \<in> UNIV \<inter> \<lbrace>True\<rbrace>}} proof (prove)
goal (2 subgoals):
 1. \<And>dom tptr curThread. \<lbrakk>d \<le> maxDomain; dom = UCAST(8 \<rightarrow> 32) d; tptr = tcb_ptr_to_ctcb_ptr t\<rbrakk> \<Longrightarrow> \<lbrace>?R343 dom tptr curThread\<rbrace> tcbSchedDequeue t \<lbrace>\<lambda>rv. tcb_at' t and (\<lambda>_. True) and (\<lambda>s. (tcb_at' t and (\<lambda>s. \<forall>p. t \<notin> set (ksReadyQueues s p)) and (\<lambda>s. valid_pspace' s \<and> Invariants_H.valid_queues s \<and> sym_refs (state_refs_of' s) \<and> if_live_then_nonz_cap' s \<and> if_unsafe_then_cap' s \<and> valid_idle' s \<and> valid_global_refs' s \<and> valid_arch_state' s \<and> valid_irq_node' (irq_node' s) s \<and> valid_irq_handlers' s \<and> valid_irq_states' s \<and> irqs_masked' s \<and> valid_machine_state' s \<and> cur_tcb' s \<and> untyped_ranges_zero' s \<and> valid_queues' s \<and> valid_pde_mappings' s \<and> pspace_domain_valid s \<and> ksCurDomain s \<le> maxDomain \<and> valid_dom_schedule' s \<and> (\<forall>x. ksSchedulerAction s = SwitchToThread x \<longrightarrow> st_tcb_at' runnable' x s)) and sch_act_simple and K (d \<le> maxDomain)) s \<and> obj_at' (\<lambda>obj. if t = t then True else True) t s \<and> sch_act_simple s \<and> curThread = ksCurThread s) and tcb_at' (ctcb_ptr_to_tcb_ptr tptr)\<rbrace>
 2. \<And>dom tptr s s'. \<lbrakk>d \<le> maxDomain; dom = UCAST(8 \<rightarrow> 32) d; tptr = tcb_ptr_to_ctcb_ptr t; (s, s') \<in> rf_sr; (invs' and tcb_at' t and sch_act_simple) s; s' \<in> UNIV\<rbrakk> \<Longrightarrow> (\<forall>rv. ksCurThread s = rv \<longrightarrow> (Invariants_H.valid_queues and valid_queues' and tcb_at' t and valid_objs' and ?R343 dom tptr rv) s) \<and> s' \<in> {s. \<forall>rv. ksCurThread_' (globals s) = tcb_ptr_to_ctcb_ptr rv \<longrightarrow> s \<in> {s. tcb_'_update (\<lambda>_. tptr) s \<in> UNIV \<inter> \<lbrace>\<acute>tcb = tcb_ptr_to_ctcb_ptr t\<rbrace>} \<inter> {s'. \<forall>t rv. dc rv (xfdc t) \<longrightarrow> s'\<lparr>globals := globals t\<rparr> \<in> UNIV \<inter> \<lbrace>True\<rbrace>}} proof (prove)
goal (3 subgoals):
 1. \<And>dom tptr curThread. \<lbrakk>d \<le> maxDomain; dom = UCAST(8 \<rightarrow> 32) d; tptr = tcb_ptr_to_ctcb_ptr t\<rbrakk> \<Longrightarrow> \<lbrace>?R343 dom tptr curThread\<rbrace> tcbSchedDequeue t \<lbrace>\<lambda>_. invs' and tcb_at' t and sch_act_simple and (\<lambda>s. curThread = ksCurThread s \<and> (\<forall>p. t \<notin> set (ksReadyQueues s p)))\<rbrace>
 2. \<And>dom tptr curThread rv s. \<lbrakk>d \<le> maxDomain; dom = UCAST(8 \<rightarrow> 32) d; tptr = tcb_ptr_to_ctcb_ptr t; (invs' and tcb_at' t and sch_act_simple and (\<lambda>s. curThread = ksCurThread s \<and> (\<forall>p. t \<notin> set (ksReadyQueues s p)))) s\<rbrakk> \<Longrightarrow> (tcb_at' t and (\<lambda>_. True) and (\<lambda>s. (tcb_at' t and (\<lambda>s. \<forall>p. t \<notin> set (ksReadyQueues s p)) and (\<lambda>s. valid_pspace' s \<and> Invariants_H.valid_queues s \<and> sym_refs (state_refs_of' s) \<and> if_live_then_nonz_cap' s \<and> if_unsafe_then_cap' s \<and> valid_idle' s \<and> valid_global_refs' s \<and> valid_arch_state' s \<and> valid_irq_node' (irq_node' s) s \<and> valid_irq_handlers' s \<and> valid_irq_states' s \<and> irqs_masked' s \<and> valid_machine_state' s \<and> cur_tcb' s \<and> untyped_ranges_zero' s \<and> valid_queues' s \<and> valid_pde_mappings' s \<and> pspace_domain_valid s \<and> ksCurDomain s \<le> maxDomain \<and> valid_dom_schedule' s \<and> (\<forall>x. ksSchedulerAction s = SwitchToThread x \<longrightarrow> st_tcb_at' runnable' x s)) and sch_act_simple and K (d \<le> maxDomain)) s \<and> obj_at' (\<lambda>obj. if t = t then True else True) t s \<and> sch_act_simple s \<and> curThread = ksCurThread s) and tcb_at' (ctcb_ptr_to_tcb_ptr tptr)) s
 3. \<And>dom tptr s s'. \<lbrakk>d \<le> maxDomain; dom = UCAST(8 \<rightarrow> 32) d; tptr = tcb_ptr_to_ctcb_ptr t; (s, s') \<in> rf_sr; (invs' and tcb_at' t and sch_act_simple) s; s' \<in> UNIV\<rbrakk> \<Longrightarrow> (\<forall>rv. ksCurThread s = rv \<longrightarrow> (Invariants_H.valid_queues and valid_queues' and tcb_at' t and valid_objs' and ?R343 dom tptr rv) s) \<and> s' \<in> {s. \<forall>rv. ksCurThread_' (globals s) = tcb_ptr_to_ctcb_ptr rv \<longrightarrow> s \<in> {s. tcb_'_update (\<lambda>_. tptr) s \<in> UNIV \<inter> \<lbrace>\<acute>tcb = tcb_ptr_to_ctcb_ptr t\<rbrace>} \<inter> {s'. \<forall>t rv. dc rv (xfdc t) \<longrightarrow> s'\<lparr>globals := globals t\<rparr> \<in> UNIV \<inter> \<lbrace>True\<rbrace>}} proof (prove)
goal (2 subgoals):
 1. \<And>dom tptr curThread rv s. \<lbrakk>d \<le> maxDomain; dom = UCAST(8 \<rightarrow> 32) d; tptr = tcb_ptr_to_ctcb_ptr t; (invs' and tcb_at' t and sch_act_simple and (\<lambda>s. curThread = ksCurThread s \<and> (\<forall>p. t \<notin> set (ksReadyQueues s p)))) s\<rbrakk> \<Longrightarrow> (tcb_at' t and (\<lambda>_. True) and (\<lambda>s. (tcb_at' t and (\<lambda>s. \<forall>p. t \<notin> set (ksReadyQueues s p)) and (\<lambda>s. valid_pspace' s \<and> Invariants_H.valid_queues s \<and> sym_refs (state_refs_of' s) \<and> if_live_then_nonz_cap' s \<and> if_unsafe_then_cap' s \<and> valid_idle' s \<and> valid_global_refs' s \<and> valid_arch_state' s \<and> valid_irq_node' (irq_node' s) s \<and> valid_irq_handlers' s \<and> valid_irq_states' s \<and> irqs_masked' s \<and> valid_machine_state' s \<and> cur_tcb' s \<and> untyped_ranges_zero' s \<and> valid_queues' s \<and> valid_pde_mappings' s \<and> pspace_domain_valid s \<and> ksCurDomain s \<le> maxDomain \<and> valid_dom_schedule' s \<and> (\<forall>x. ksSchedulerAction s = SwitchToThread x \<longrightarrow> st_tcb_at' runnable' x s)) and sch_act_simple and K (d \<le> maxDomain)) s \<and> obj_at' (\<lambda>obj. if t = t then True else True) t s \<and> sch_act_simple s \<and> curThread = ksCurThread s) and tcb_at' (ctcb_ptr_to_tcb_ptr tptr)) s
 2. \<And>dom tptr s s'. \<lbrakk>d \<le> maxDomain; dom = UCAST(8 \<rightarrow> 32) d; tptr = tcb_ptr_to_ctcb_ptr t; (s, s') \<in> rf_sr; (invs' and tcb_at' t and sch_act_simple) s; s' \<in> UNIV\<rbrakk> \<Longrightarrow> (\<forall>rv. ksCurThread s = rv \<longrightarrow> (Invariants_H.valid_queues and valid_queues' and tcb_at' t and valid_objs' and (\<lambda>s. (invs' and tcb_at' t) s \<and> tcb_at' t s \<and> sch_act_simple s \<and> rv = ksCurThread s \<and> (\<forall>x. (Invariants_H.valid_queues and tcb_at' t and valid_objs') s))) s) \<and> s' \<in> {s. \<forall>rv. ksCurThread_' (globals s) = tcb_ptr_to_ctcb_ptr rv \<longrightarrow> s \<in> {s. tcb_'_update (\<lambda>_. tptr) s \<in> UNIV \<inter> \<lbrace>\<acute>tcb = tcb_ptr_to_ctcb_ptr t\<rbrace>} \<inter> {s'. \<forall>t rv. dc rv (xfdc t) \<longrightarrow> s'\<lparr>globals := globals t\<rparr> \<in> UNIV \<inter> \<lbrace>True\<rbrace>}} proof (prove)
goal (1 subgoal):
 1. \<And>dom tptr s s'. \<lbrakk>d \<le> maxDomain; dom = UCAST(8 \<rightarrow> 32) d; tptr = tcb_ptr_to_ctcb_ptr t; (s, s') \<in> rf_sr; (invs' and tcb_at' t and sch_act_simple) s; s' \<in> UNIV\<rbrakk> \<Longrightarrow> (\<forall>rv. ksCurThread s = rv \<longrightarrow> (Invariants_H.valid_queues and valid_queues' and tcb_at' t and valid_objs' and (\<lambda>s. (invs' and tcb_at' t) s \<and> tcb_at' t s \<and> sch_act_simple s \<and> rv = ksCurThread s \<and> (\<forall>x. (Invariants_H.valid_queues and tcb_at' t and valid_objs') s))) s) \<and> s' \<in> {s. \<forall>rv. ksCurThread_' (globals s) = tcb_ptr_to_ctcb_ptr rv \<longrightarrow> s \<in> {s. tcb_'_update (\<lambda>_. tptr) s \<in> UNIV \<inter> \<lbrace>\<acute>tcb = tcb_ptr_to_ctcb_ptr t\<rbrace>} \<inter> {s'. \<forall>t rv. dc rv (xfdc t) \<longrightarrow> s'\<lparr>globals := globals t\<rparr> \<in> UNIV \<inter> \<lbrace>True\<rbrace>}} proof (prove)
goal:
No subgoals!