theory Schedule_C

lemma chooseThread_ccorres:
  "ccorres dc xfdc all_invs_but_ct_idle_or_in_cur_domain' UNIV [] chooseThread (Call chooseThread_'proc)" proof - note prio_and_dom_limit_helpers [simp] note Collect_const_mem [simp] note Collect_const [simp del] 
  (* when numDomains = 1, array bounds checks would become _ = 0 rather than _ < 1, changing the
     shape of the proof compared to when numDomains > 1 *)
   include no_less_1_simps have invs_no_cicd'_max_CurDomain[intro]:
    "\<And>s. invs_no_cicd' s \<Longrightarrow> ksCurDomain s \<le> maxDomain" by (simp add: invs_no_cicd'_def) show ?thesis supply if_split[split del] apply (cinit) apply (simp add: numDomains_sge_1_simp) apply (rule_tac xf'=dom_' and r'="\<lambda>rv rv'. rv' = ucast rv" in ccorres_split_nothrow_novcg) apply (rule ccorres_from_vcg[where P=\<top> and P'=UNIV]) apply clarsimp apply (rule conseqPre, vcg) apply (rule Collect_mono) apply (clarsimp split: prod.split) apply (clarsimp simp: curDomain_def simpler_gets_def return_def rf_sr_ksCurDomain) apply ceqv apply clarsimp apply (rename_tac curdom) apply (rule_tac P="curdom \<le> maxDomain" in ccorres_cross_over_guard_no_st) apply (rule ccorres_Guard) apply (rule ccorres_pre_getReadyQueuesL1Bitmap) apply (rename_tac l1) apply (rule_tac R="\<lambda>s. l1 = ksReadyQueuesL1Bitmap s curdom \<and> curdom \<le> maxDomain"
                in ccorres_cond) subgoal by (fastforce dest!: rf_sr_cbitmap_L1_relation simp: cbitmap_L1_relation_def) prefer 2 \<comment> \<open>switchToIdleThread\<close> apply (ctac(no_vcg) add: switchToIdleThread_ccorres) apply clarsimp apply (rule ccorres_rhs_assoc)+ apply (rule ccorres_split_nothrow_novcg) apply (rule_tac xf'=prio_' in ccorres_call) apply (rule getHighestPrio_ccorres[simplified getHighestPrio_def']) apply simp+ apply ceqv apply clarsimp apply (rename_tac prio) apply (rule_tac P="curdom \<le> maxDomain" in ccorres_cross_over_guard_no_st) apply (rule_tac P="prio \<le> maxPriority" in ccorres_cross_over_guard_no_st) apply (rule ccorres_pre_getQueue) apply (rule_tac P="queue \<noteq> []" in ccorres_cross_over_guard_no_st) apply (rule ccorres_symb_exec_l) apply (rule ccorres_assert) apply (rule ccorres_symb_exec_r) apply (rule ccorres_Guard_Seq)+ apply (rule ccorres_symb_exec_r) apply (simp only: ccorres_seq_skip) apply (rule ccorres_call[OF switchToThread_ccorres']; simp) apply vcg apply (rule conseqPre, vcg) apply clarsimp apply clarsimp apply (rule conseqPre, vcg) apply (rule Collect_mono) apply clarsimp apply (strengthen queue_in_range) apply assumption apply clarsimp apply (rule conseqPre, vcg) apply clarsimp apply (wp isRunnable_wp)+ apply (clarsimp simp: Let_def guard_is_UNIV_def) apply (drule invs_no_cicd'_queues) apply (case_tac queue, simp) apply (clarsimp simp: tcb_queue_relation'_def cready_queues_index_to_C_def numPriorities_def) apply (clarsimp simp add: maxDom_to_H maxPrio_to_H
                                 queue_in_range[where qdom=0, simplified, simplified maxPrio_to_H]) apply (clarsimp simp: le_maxDomain_eq_less_numDomains unat_trans_ucast_helper ) apply wpsimp apply (clarsimp simp: guard_is_UNIV_def le_maxDomain_eq_less_numDomains word_less_nat_alt
                           numDomains_less_numeric_explicit) apply (frule invs_no_cicd'_queues) apply (frule invs_no_cicd'_max_CurDomain) apply (frule invs_no_cicd'_queues) apply (clarsimp simp: valid_queues_def lookupBitmapPriority_le_maxPriority) apply (intro conjI impI) apply (fastforce dest: bitmapQ_from_bitmap_lookup simp: valid_bitmapQ_bitmapQ_simp) apply (fastforce dest: lookupBitmapPriority_obj_at'
                       simp: pred_conj_def obj_at'_def st_tcb_at'_def) apply (fastforce dest: bitmapQ_from_bitmap_lookup simp: valid_bitmapQ_bitmapQ_simp) apply (clarsimp simp: pred_conj_def obj_at'_def st_tcb_at'_def) apply (clarsimp simp: not_less le_maxDomain_eq_less_numDomains) apply (prop_tac "ksCurDomain s = 0") using unsigned_eq_0_iff apply force apply (cut_tac s=s in lookupBitmapPriority_obj_at'; simp?) apply (clarsimp simp: pred_conj_def obj_at'_def st_tcb_at'_def) done qed

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. ccorres dc xfdc all_invs_but_ct_idle_or_in_cur_domain' UNIV [] chooseThread (Call chooseThread_'proc) proof (state)
goal (1 subgoal):
 1. ccorres dc xfdc all_invs_but_ct_idle_or_in_cur_domain' UNIV [] chooseThread (Call chooseThread_'proc) proof (state)
this:
UCAST(8 \<rightarrow> 32) ?p >> wordRadix < 8
UCAST(8 \<rightarrow> 32) ?p >> wordRadix \<le> 7
UCAST(8 \<rightarrow> 32) ?p >> wordRadix < 0x20
unat (?p >> wordRadix) \<le> 7
unat (UCAST(8 \<rightarrow> 32) ?d * 0x100 + UCAST(8 \<rightarrow> 32) ?p) = unat ?d * 256 + unat ?p
unat (UCAST(8 \<rightarrow> 32) ?p && 0x1F) = unat (?p && 0x1F)
?w && 0x1F < 0x20

goal (1 subgoal):
 1. ccorres dc xfdc all_invs_but_ct_idle_or_in_cur_domain' UNIV [] chooseThread (Call chooseThread_'proc) proof (state)
this:
(?x \<in> (if ?P then UNIV else {})) = ?P

goal (1 subgoal):
 1. ccorres dc xfdc all_invs_but_ct_idle_or_in_cur_domain' UNIV [] chooseThread (Call chooseThread_'proc) proof (state)
this:
\<lbrace>?P\<rbrace> = (if ?P then UNIV else {})

goal (1 subgoal):
 1. ccorres dc xfdc all_invs_but_ct_idle_or_in_cur_domain' UNIV [] chooseThread (Call chooseThread_'proc) proof (state)
this:
\<lbrace>?P\<rbrace> = (if ?P then UNIV else {})

goal (1 subgoal):
 1. ccorres dc xfdc all_invs_but_ct_idle_or_in_cur_domain' UNIV [] chooseThread (Call chooseThread_'proc) proof (state)
goal (1 subgoal):
 1. ccorres dc xfdc all_invs_but_ct_idle_or_in_cur_domain' UNIV [] chooseThread (Call chooseThread_'proc) proof (prove)
goal (1 subgoal):
 1. \<And>s. all_invs_but_ct_idle_or_in_cur_domain' s \<Longrightarrow> ksCurDomain s \<le> maxDomain proof (state)
this:
all_invs_but_ct_idle_or_in_cur_domain' ?s1 \<Longrightarrow> ksCurDomain ?s1 \<le> maxDomain

goal (1 subgoal):
 1. ccorres dc xfdc all_invs_but_ct_idle_or_in_cur_domain' UNIV [] chooseThread (Call chooseThread_'proc) proof (prove)
goal (1 subgoal):
 1. ccorres dc xfdc all_invs_but_ct_idle_or_in_cur_domain' UNIV [] chooseThread (Call chooseThread_'proc) proof (prove)
goal (1 subgoal):
 1. ccorres dc xfdc all_invs_but_ct_idle_or_in_cur_domain' UNIV [] chooseThread (Call chooseThread_'proc) proof (prove)
goal (2 subgoals):
 1. ccorres dc xfdc ?Q294 ?Q'294 [SKIP] (do curdom <- if Suc 0 < numDomains then curDomain else return 0;
l1 <- getReadyQueuesL1Bitmap curdom;
if l1 \<noteq> 0 then do prio <- getHighestPrio curdom;
queue <- getQueue curdom prio;
thread <- return (HaskellLib_H.head queue);
runnable <- isRunnable thread;
haskell_assert runnable [];
global.switchToThread thread
od else global.switchToIdleThread
od) (IF 1 <s Kernel_C.numDomains THEN
  \<acute>dom :== \<acute>ksCurDomain
ELSE
  \<acute>dom :== 0
FI;;
Guard ArrayBounds \<lbrace>\<acute>dom < 0x10\<rbrace> (IF \<acute>ksReadyQueuesL1Bitmap.[unat \<acute>dom] \<noteq> 0 THEN
  \<acute>prio :== CALL getHighestPrio_'proc(\<acute>dom);;
\<acute>ret__unsigned_long :== CALL ready_queues_index_'proc(\<acute>dom,\<acute>prio);;
Guard ArrayBounds \<lbrace>\<acute>ret__unsigned_long < 0x1000\<rbrace> (\<acute>thread :== head_C (\<acute>ksReadyQueues.[unat \<acute>ret__unsigned_long]));;
CALL switchToThread_'proc(\<acute>thread)
ELSE
  CALL switchToIdleThread_'proc()
FI))
 2. \<And>s s'. \<lbrakk>(s, s') \<in> rf_sr; all_invs_but_ct_idle_or_in_cur_domain' s; s' \<in> UNIV\<rbrakk> \<Longrightarrow> ?Q294 s \<and> s' \<in> ?Q'294 proof (prove)
goal (2 subgoals):
 1. ccorres dc xfdc ?Q294 ?Q'294 [SKIP] (do curdom <- if Suc 0 < numDomains then curDomain else return 0;
l1 <- getReadyQueuesL1Bitmap curdom;
if l1 \<noteq> 0 then do prio <- getHighestPrio curdom;
queue <- getQueue curdom prio;
thread <- return (HaskellLib_H.head queue);
runnable <- isRunnable thread;
haskell_assert runnable [];
global.switchToThread thread
od else global.switchToIdleThread
od) (IF Suc 0 < numDomains THEN
  \<acute>dom :== \<acute>ksCurDomain
ELSE
  \<acute>dom :== 0
FI;;
Guard ArrayBounds \<lbrace>\<acute>dom < 0x10\<rbrace> (IF \<acute>ksReadyQueuesL1Bitmap.[unat \<acute>dom] \<noteq> 0 THEN
  \<acute>prio :== CALL getHighestPrio_'proc();;
\<acute>ret__unsigned_long :== CALL ready_queues_index_'proc();;
Guard ArrayBounds \<lbrace>\<acute>ret__unsigned_long < 0x1000\<rbrace> (\<acute>thread :== head_C (\<acute>ksReadyQueues.[unat \<acute>ret__unsigned_long]));;
CALL switchToThread_'proc()
ELSE
  CALL switchToIdleThread_'proc()
FI))
 2. \<And>s s'. \<lbrakk>(s, s') \<in> rf_sr; all_invs_but_ct_idle_or_in_cur_domain' s; s' \<in> UNIV\<rbrakk> \<Longrightarrow> ?Q294 s \<and> s' \<in> ?Q'294 proof (prove)
goal (6 subgoals):
 1. ccorres (\<lambda>rv rv'. rv' = UCAST(8 \<rightarrow> 32) rv) dom_' ?P301 ?Q'294 [] (if Suc 0 < numDomains then curDomain else return 0) (IF Suc 0 < numDomains THEN
  \<acute>dom :== \<acute>ksCurDomain
ELSE
  \<acute>dom :== 0
FI)
 2. \<And>rv' t t'. ceqv \<Gamma> dom_' rv' t t' (Guard ArrayBounds \<lbrace>\<acute>dom < 0x10\<rbrace> (IF \<acute>ksReadyQueuesL1Bitmap.[unat \<acute>dom] \<noteq> 0 THEN
  \<acute>prio :== CALL getHighestPrio_'proc();;
\<acute>ret__unsigned_long :== CALL ready_queues_index_'proc();;
Guard ArrayBounds \<lbrace>\<acute>ret__unsigned_long < 0x1000\<rbrace> (\<acute>thread :== head_C (\<acute>ksReadyQueues.[unat \<acute>ret__unsigned_long]));;
CALL switchToThread_'proc()
ELSE
  CALL switchToIdleThread_'proc()
FI)) (?d'301 rv')
 3. \<And>rv rv'. rv' = UCAST(8 \<rightarrow> 32) rv \<Longrightarrow> ccorres dc xfdc (?Q301 rv) (?Q'301 rv rv') [SKIP] (do l1 <- getReadyQueuesL1Bitmap rv;
if l1 \<noteq> 0 then do prio <- getHighestPrio rv;
queue <- getQueue rv prio;
thread <- return (HaskellLib_H.head queue);
runnable <- isRunnable thread;
haskell_assert runnable [];
global.switchToThread thread
od else global.switchToIdleThread
od) (?d'301 rv')
 4. \<lbrace>?R301\<rbrace> if Suc 0 < numDomains then curDomain else return 0 \<lbrace>?Q301\<rbrace>
 5. guard_is_UNIV (\<lambda>rv rv'. rv' = UCAST(8 \<rightarrow> 32) rv) dom_' ?Q'301
 6. \<And>s s'. \<lbrakk>(s, s') \<in> rf_sr; all_invs_but_ct_idle_or_in_cur_domain' s; s' \<in> UNIV\<rbrakk> \<Longrightarrow> (?P301 and ?R301) s \<and> s' \<in> ?Q'294 proof (prove)
goal (6 subgoals):
 1. \<forall>\<sigma>. \<Gamma>\<turnstile> {s. True \<and> s \<in> UNIV \<and> (\<sigma>, s) \<in> rf_sr} IF Suc 0 < numDomains THEN
  \<acute>dom :== \<acute>ksCurDomain
ELSE
  \<acute>dom :== 0
FI {s. \<exists>(rv, \<sigma>')\<in>fst ((if Suc 0 < numDomains then curDomain else return 0) \<sigma>). (\<sigma>', s) \<in> rf_sr \<and> dom_' s = UCAST(8 \<rightarrow> 32) rv}
 2. \<And>rv' t t'. ceqv \<Gamma> dom_' rv' t t' (Guard ArrayBounds \<lbrace>\<acute>dom < 0x10\<rbrace> (IF \<acute>ksReadyQueuesL1Bitmap.[unat \<acute>dom] \<noteq> 0 THEN
  \<acute>prio :== CALL getHighestPrio_'proc();;
\<acute>ret__unsigned_long :== CALL ready_queues_index_'proc();;
Guard ArrayBounds \<lbrace>\<acute>ret__unsigned_long < 0x1000\<rbrace> (\<acute>thread :== head_C (\<acute>ksReadyQueues.[unat \<acute>ret__unsigned_long]));;
CALL switchToThread_'proc()
ELSE
  CALL switchToIdleThread_'proc()
FI)) (?d'301 rv')
 3. \<And>rv rv'. rv' = UCAST(8 \<rightarrow> 32) rv \<Longrightarrow> ccorres dc xfdc (?Q301 rv) (?Q'301 rv rv') [SKIP] (do l1 <- getReadyQueuesL1Bitmap rv;
if l1 \<noteq> 0 then do prio <- getHighestPrio rv;
queue <- getQueue rv prio;
thread <- return (HaskellLib_H.head queue);
runnable <- isRunnable thread;
haskell_assert runnable [];
global.switchToThread thread
od else global.switchToIdleThread
od) (?d'301 rv')
 4. \<lbrace>?R301\<rbrace> if Suc 0 < numDomains then curDomain else return 0 \<lbrace>?Q301\<rbrace>
 5. guard_is_UNIV (\<lambda>rv rv'. rv' = UCAST(8 \<rightarrow> 32) rv) dom_' ?Q'301
 6. \<And>s s'. \<lbrakk>(s, s') \<in> rf_sr; all_invs_but_ct_idle_or_in_cur_domain' s; s' \<in> UNIV\<rbrakk> \<Longrightarrow> ((\<lambda>_. True) and ?R301) s \<and> s' \<in> UNIV proof (prove)
goal (6 subgoals):
 1. \<And>\<sigma>. \<Gamma>\<turnstile> {s. (\<sigma>, s) \<in> rf_sr} IF Suc 0 < numDomains THEN
  \<acute>dom :== \<acute>ksCurDomain
ELSE
  \<acute>dom :== 0
FI {s. \<exists>x\<in>fst ((if Suc 0 < numDomains then curDomain else return 0) \<sigma>). case x of (rv, \<sigma>') \<Rightarrow> (\<sigma>', s) \<in> rf_sr \<and> dom_' s = UCAST(8 \<rightarrow> 32) rv}
 2. \<And>rv' t t'. ceqv \<Gamma> dom_' rv' t t' (Guard ArrayBounds \<lbrace>\<acute>dom < 0x10\<rbrace> (IF \<acute>ksReadyQueuesL1Bitmap.[unat \<acute>dom] \<noteq> 0 THEN
  \<acute>prio :== CALL getHighestPrio_'proc();;
\<acute>ret__unsigned_long :== CALL ready_queues_index_'proc();;
Guard ArrayBounds \<lbrace>\<acute>ret__unsigned_long < 0x1000\<rbrace> (\<acute>thread :== head_C (\<acute>ksReadyQueues.[unat \<acute>ret__unsigned_long]));;
CALL switchToThread_'proc()
ELSE
  CALL switchToIdleThread_'proc()
FI)) (?d'301 rv')
 3. \<And>rv rv'. rv' = UCAST(8 \<rightarrow> 32) rv \<Longrightarrow> ccorres dc xfdc (?Q301 rv) (?Q'301 rv rv') [SKIP] (do l1 <- getReadyQueuesL1Bitmap rv;
if l1 \<noteq> 0 then do prio <- getHighestPrio rv;
queue <- getQueue rv prio;
thread <- return (HaskellLib_H.head queue);
runnable <- isRunnable thread;
haskell_assert runnable [];
global.switchToThread thread
od else global.switchToIdleThread
od) (?d'301 rv')
 4. \<lbrace>?R301\<rbrace> if Suc 0 < numDomains then curDomain else return 0 \<lbrace>?Q301\<rbrace>
 5. guard_is_UNIV (\<lambda>rv rv'. rv' = UCAST(8 \<rightarrow> 32) rv) dom_' ?Q'301
 6. \<And>s s'. \<lbrakk>(s, s') \<in> rf_sr; all_invs_but_ct_idle_or_in_cur_domain' s; s' \<in> UNIV\<rbrakk> \<Longrightarrow> ((\<lambda>_. True) and ?R301) s \<and> s' \<in> UNIV proof (prove)
goal (6 subgoals):
 1. \<And>\<sigma>. {s. (\<sigma>, s) \<in> rf_sr} \<subseteq> {s. (Suc 0 < numDomains \<longrightarrow> (\<exists>(rv, \<sigma>')\<in>fst ((if Suc 0 < numDomains then curDomain else return 0) \<sigma>). (\<sigma>', dom_'_update (\<lambda>_. ksCurDomain_' (globals s)) s) \<in> rf_sr \<and> ksCurDomain_' (globals s) = UCAST(8 \<rightarrow> 32) rv)) \<and> (\<not> Suc 0 < numDomains \<longrightarrow> (\<exists>(rv, \<sigma>')\<in>fst ((if Suc 0 < numDomains then curDomain else return 0) \<sigma>). (\<sigma>', dom_'_update (\<lambda>_. 0) s) \<in> rf_sr \<and> 0 = UCAST(8 \<rightarrow> 32) rv))}
 2. \<And>rv' t t'. ceqv \<Gamma> dom_' rv' t t' (Guard ArrayBounds \<lbrace>\<acute>dom < 0x10\<rbrace> (IF \<acute>ksReadyQueuesL1Bitmap.[unat \<acute>dom] \<noteq> 0 THEN
  \<acute>prio :== CALL getHighestPrio_'proc();;
\<acute>ret__unsigned_long :== CALL ready_queues_index_'proc();;
Guard ArrayBounds \<lbrace>\<acute>ret__unsigned_long < 0x1000\<rbrace> (\<acute>thread :== head_C (\<acute>ksReadyQueues.[unat \<acute>ret__unsigned_long]));;
CALL switchToThread_'proc()
ELSE
  CALL switchToIdleThread_'proc()
FI)) (?d'301 rv')
 3. \<And>rv rv'. rv' = UCAST(8 \<rightarrow> 32) rv \<Longrightarrow> ccorres dc xfdc (?Q301 rv) (?Q'301 rv rv') [SKIP] (do l1 <- getReadyQueuesL1Bitmap rv;
if l1 \<noteq> 0 then do prio <- getHighestPrio rv;
queue <- getQueue rv prio;
thread <- return (HaskellLib_H.head queue);
runnable <- isRunnable thread;
haskell_assert runnable [];
global.switchToThread thread
od else global.switchToIdleThread
od) (?d'301 rv')
 4. \<lbrace>?R301\<rbrace> if Suc 0 < numDomains then curDomain else return 0 \<lbrace>?Q301\<rbrace>
 5. guard_is_UNIV (\<lambda>rv rv'. rv' = UCAST(8 \<rightarrow> 32) rv) dom_' ?Q'301
 6. \<And>s s'. \<lbrakk>(s, s') \<in> rf_sr; all_invs_but_ct_idle_or_in_cur_domain' s; s' \<in> UNIV\<rbrakk> \<Longrightarrow> ((\<lambda>_. True) and ?R301) s \<and> s' \<in> UNIV proof (prove)
goal (6 subgoals):
 1. \<And>\<sigma> x. (\<sigma>, x) \<in> rf_sr \<longrightarrow> (Suc 0 < numDomains \<longrightarrow> (\<exists>(rv, \<sigma>')\<in>fst ((if Suc 0 < numDomains then curDomain else return 0) \<sigma>). (\<sigma>', dom_'_update (\<lambda>_. ksCurDomain_' (globals x)) x) \<in> rf_sr \<and> ksCurDomain_' (globals x) = UCAST(8 \<rightarrow> 32) rv)) \<and> (\<not> Suc 0 < numDomains \<longrightarrow> (\<exists>(rv, \<sigma>')\<in>fst ((if Suc 0 < numDomains then curDomain else return 0) \<sigma>). (\<sigma>', dom_'_update (\<lambda>_. 0) x) \<in> rf_sr \<and> 0 = UCAST(8 \<rightarrow> 32) rv))
 2. \<And>rv' t t'. ceqv \<Gamma> dom_' rv' t t' (Guard ArrayBounds \<lbrace>\<acute>dom < 0x10\<rbrace> (IF \<acute>ksReadyQueuesL1Bitmap.[unat \<acute>dom] \<noteq> 0 THEN
  \<acute>prio :== CALL getHighestPrio_'proc();;
\<acute>ret__unsigned_long :== CALL ready_queues_index_'proc();;
Guard ArrayBounds \<lbrace>\<acute>ret__unsigned_long < 0x1000\<rbrace> (\<acute>thread :== head_C (\<acute>ksReadyQueues.[unat \<acute>ret__unsigned_long]));;
CALL switchToThread_'proc()
ELSE
  CALL switchToIdleThread_'proc()
FI)) (?d'301 rv')
 3. \<And>rv rv'. rv' = UCAST(8 \<rightarrow> 32) rv \<Longrightarrow> ccorres dc xfdc (?Q301 rv) (?Q'301 rv rv') [SKIP] (do l1 <- getReadyQueuesL1Bitmap rv;
if l1 \<noteq> 0 then do prio <- getHighestPrio rv;
queue <- getQueue rv prio;
thread <- return (HaskellLib_H.head queue);
runnable <- isRunnable thread;
haskell_assert runnable [];
global.switchToThread thread
od else global.switchToIdleThread
od) (?d'301 rv')
 4. \<lbrace>?R301\<rbrace> if Suc 0 < numDomains then curDomain else return 0 \<lbrace>?Q301\<rbrace>
 5. guard_is_UNIV (\<lambda>rv rv'. rv' = UCAST(8 \<rightarrow> 32) rv) dom_' ?Q'301
 6. \<And>s s'. \<lbrakk>(s, s') \<in> rf_sr; all_invs_but_ct_idle_or_in_cur_domain' s; s' \<in> UNIV\<rbrakk> \<Longrightarrow> ((\<lambda>_. True) and ?R301) s \<and> s' \<in> UNIV proof (prove)
goal (6 subgoals):
 1. \<And>\<sigma> x. (\<sigma>, x) \<in> rf_sr \<Longrightarrow> (Suc 0 < numDomains \<longrightarrow> (\<exists>xa\<in>fst (curDomain \<sigma>). \<forall>x1 x2. xa = (x1, x2) \<longrightarrow> (x2, x) \<in> rf_sr \<and> ksCurDomain_' (globals x) = UCAST(8 \<rightarrow> 32) x1)) \<and> (\<not> Suc 0 < numDomains \<longrightarrow> (\<exists>xa\<in>fst (return 0 \<sigma>). \<forall>x1 x2. xa = (x1, x2) \<longrightarrow> (x2, x) \<in> rf_sr \<and> UCAST(8 \<rightarrow> 32) x1 = 0))
 2. \<And>rv' t t'. ceqv \<Gamma> dom_' rv' t t' (Guard ArrayBounds \<lbrace>\<acute>dom < 0x10\<rbrace> (IF \<acute>ksReadyQueuesL1Bitmap.[unat \<acute>dom] \<noteq> 0 THEN
  \<acute>prio :== CALL getHighestPrio_'proc();;
\<acute>ret__unsigned_long :== CALL ready_queues_index_'proc();;
Guard ArrayBounds \<lbrace>\<acute>ret__unsigned_long < 0x1000\<rbrace> (\<acute>thread :== head_C (\<acute>ksReadyQueues.[unat \<acute>ret__unsigned_long]));;
CALL switchToThread_'proc()
ELSE
  CALL switchToIdleThread_'proc()
FI)) (?d'301 rv')
 3. \<And>rv rv'. rv' = UCAST(8 \<rightarrow> 32) rv \<Longrightarrow> ccorres dc xfdc (?Q301 rv) (?Q'301 rv rv') [SKIP] (do l1 <- getReadyQueuesL1Bitmap rv;
if l1 \<noteq> 0 then do prio <- getHighestPrio rv;
queue <- getQueue rv prio;
thread <- return (HaskellLib_H.head queue);
runnable <- isRunnable thread;
haskell_assert runnable [];
global.switchToThread thread
od else global.switchToIdleThread
od) (?d'301 rv')
 4. \<lbrace>?R301\<rbrace> if Suc 0 < numDomains then curDomain else return 0 \<lbrace>?Q301\<rbrace>
 5. guard_is_UNIV (\<lambda>rv rv'. rv' = UCAST(8 \<rightarrow> 32) rv) dom_' ?Q'301
 6. \<And>s s'. \<lbrakk>(s, s') \<in> rf_sr; all_invs_but_ct_idle_or_in_cur_domain' s; s' \<in> UNIV\<rbrakk> \<Longrightarrow> ((\<lambda>_. True) and ?R301) s \<and> s' \<in> UNIV proof (prove)
goal (5 subgoals):
 1. \<And>rv' t t'. ceqv \<Gamma> dom_' rv' t t' (Guard ArrayBounds \<lbrace>\<acute>dom < 0x10\<rbrace> (IF \<acute>ksReadyQueuesL1Bitmap.[unat \<acute>dom] \<noteq> 0 THEN
  \<acute>prio :== CALL getHighestPrio_'proc();;
\<acute>ret__unsigned_long :== CALL ready_queues_index_'proc();;
Guard ArrayBounds \<lbrace>\<acute>ret__unsigned_long < 0x1000\<rbrace> (\<acute>thread :== head_C (\<acute>ksReadyQueues.[unat \<acute>ret__unsigned_long]));;
CALL switchToThread_'proc()
ELSE
  CALL switchToIdleThread_'proc()
FI)) (?d'301 rv')
 2. \<And>rv rv'. rv' = UCAST(8 \<rightarrow> 32) rv \<Longrightarrow> ccorres dc xfdc (?Q301 rv) (?Q'301 rv rv') [SKIP] (do l1 <- getReadyQueuesL1Bitmap rv;
if l1 \<noteq> 0 then do prio <- getHighestPrio rv;
queue <- getQueue rv prio;
thread <- return (HaskellLib_H.head queue);
runnable <- isRunnable thread;
haskell_assert runnable [];
global.switchToThread thread
od else global.switchToIdleThread
od) (?d'301 rv')
 3. \<lbrace>?R301\<rbrace> if Suc 0 < numDomains then curDomain else return 0 \<lbrace>?Q301\<rbrace>
 4. guard_is_UNIV (\<lambda>rv rv'. rv' = UCAST(8 \<rightarrow> 32) rv) dom_' ?Q'301
 5. \<And>s s'. \<lbrakk>(s, s') \<in> rf_sr; all_invs_but_ct_idle_or_in_cur_domain' s; s' \<in> UNIV\<rbrakk> \<Longrightarrow> ((\<lambda>_. True) and ?R301) s \<and> s' \<in> UNIV proof (prove)
goal (4 subgoals):
 1. \<And>rv rv'. rv' = UCAST(8 \<rightarrow> 32) rv \<Longrightarrow> ccorres dc xfdc (?Q301 rv) (?Q'301 rv rv') [SKIP] (do l1 <- getReadyQueuesL1Bitmap rv;
if l1 \<noteq> 0 then do prio <- getHighestPrio rv;
queue <- getQueue rv prio;
thread <- return (HaskellLib_H.head queue);
runnable <- isRunnable thread;
haskell_assert runnable [];
global.switchToThread thread
od else global.switchToIdleThread
od) (Guard ArrayBounds \<lbrace>rv' < 0x10\<rbrace> (IF \<acute>ksReadyQueuesL1Bitmap.[unat rv'] \<noteq> 0 THEN
  \<acute>prio :== CALL getHighestPrio_'proc(rv');;
\<acute>ret__unsigned_long :== CALL ready_queues_index_'proc(rv',\<acute>prio);;
Guard ArrayBounds \<lbrace>\<acute>ret__unsigned_long < 0x1000\<rbrace> (\<acute>thread :== head_C (\<acute>ksReadyQueues.[unat \<acute>ret__unsigned_long]));;
CALL switchToThread_'proc(\<acute>thread)
ELSE
  CALL switchToIdleThread_'proc()
FI))
 2. \<lbrace>?R301\<rbrace> if Suc 0 < numDomains then curDomain else return 0 \<lbrace>?Q301\<rbrace>
 3. guard_is_UNIV (\<lambda>rv rv'. rv' = UCAST(8 \<rightarrow> 32) rv) dom_' ?Q'301
 4. \<And>s s'. \<lbrakk>(s, s') \<in> rf_sr; all_invs_but_ct_idle_or_in_cur_domain' s; s' \<in> UNIV\<rbrakk> \<Longrightarrow> ((\<lambda>_. True) and ?R301) s \<and> s' \<in> UNIV proof (prove)
goal (4 subgoals):
 1. \<And>rv. ccorres dc xfdc (?Q301 rv) (?Q'301 rv (UCAST(8 \<rightarrow> 32) rv)) [SKIP] (do l1 <- getReadyQueuesL1Bitmap rv;
if l1 \<noteq> 0 then do prio <- getHighestPrio rv;
queue <- getQueue rv prio;
thread <- return (HaskellLib_H.head queue);
runnable <- isRunnable thread;
haskell_assert runnable [];
global.switchToThread thread
od else global.switchToIdleThread
od) (Guard ArrayBounds \<lbrace>UCAST(8 \<rightarrow> 32) rv < 0x10\<rbrace> (IF \<acute>ksReadyQueuesL1Bitmap.[unat rv] \<noteq> 0 THEN
  \<acute>prio :== CALL getHighestPrio_'proc(UCAST(8 \<rightarrow> 32) rv);;
\<acute>ret__unsigned_long :== CALL ready_queues_index_'proc(UCAST(8 \<rightarrow> 32) rv);;
Guard ArrayBounds \<lbrace>\<acute>ret__unsigned_long < 0x1000\<rbrace> (\<acute>thread :== head_C (\<acute>ksReadyQueues.[unat \<acute>ret__unsigned_long]));;
CALL switchToThread_'proc()
ELSE
  CALL switchToIdleThread_'proc()
FI))
 2. \<lbrace>?R301\<rbrace> if Suc 0 < numDomains then curDomain else return 0 \<lbrace>?Q301\<rbrace>
 3. guard_is_UNIV (\<lambda>rv rv'. rv' = UCAST(8 \<rightarrow> 32) rv) dom_' ?Q'301
 4. \<And>s s'. \<lbrakk>(s, s') \<in> rf_sr; all_invs_but_ct_idle_or_in_cur_domain' s; s' \<in> UNIV\<rbrakk> \<Longrightarrow> ((\<lambda>_. True) and ?R301) s \<and> s' \<in> UNIV proof (prove)
goal (4 subgoals):
 1. \<And>curdom. ccorres dc xfdc (?Q301 curdom) (?Q'301 curdom (UCAST(8 \<rightarrow> 32) curdom)) [SKIP] (do l1 <- getReadyQueuesL1Bitmap curdom;
if l1 \<noteq> 0 then do prio <- getHighestPrio curdom;
queue <- getQueue curdom prio;
thread <- return (HaskellLib_H.head queue);
runnable <- isRunnable thread;
haskell_assert runnable [];
global.switchToThread thread
od else global.switchToIdleThread
od) (Guard ArrayBounds \<lbrace>UCAST(8 \<rightarrow> 32) curdom < 0x10\<rbrace> (IF \<acute>ksReadyQueuesL1Bitmap.[unat curdom] \<noteq> 0 THEN
  \<acute>prio :== CALL getHighestPrio_'proc(UCAST(8 \<rightarrow> 32) curdom);;
\<acute>ret__unsigned_long :== CALL ready_queues_index_'proc(UCAST(8 \<rightarrow> 32) curdom);;
Guard ArrayBounds \<lbrace>\<acute>ret__unsigned_long < 0x1000\<rbrace> (\<acute>thread :== head_C (\<acute>ksReadyQueues.[unat \<acute>ret__unsigned_long]));;
CALL switchToThread_'proc()
ELSE
  CALL switchToIdleThread_'proc()
FI))
 2. \<lbrace>?R301\<rbrace> if Suc 0 < numDomains then curDomain else return 0 \<lbrace>?Q301\<rbrace>
 3. guard_is_UNIV (\<lambda>rv rv'. rv' = UCAST(8 \<rightarrow> 32) rv) dom_' ?Q'301
 4. \<And>s s'. \<lbrakk>(s, s') \<in> rf_sr; all_invs_but_ct_idle_or_in_cur_domain' s; s' \<in> UNIV\<rbrakk> \<Longrightarrow> ((\<lambda>_. True) and ?R301) s \<and> s' \<in> UNIV proof (prove)
goal (4 subgoals):
 1. \<And>curdom. ccorres dc xfdc (?P'474 curdom) (?Q476 curdom (UCAST(8 \<rightarrow> 32) curdom)) [SKIP] (do l1 <- getReadyQueuesL1Bitmap curdom;
if l1 \<noteq> 0 then do prio <- getHighestPrio curdom;
queue <- getQueue curdom prio;
thread <- return (HaskellLib_H.head queue);
runnable <- isRunnable thread;
haskell_assert runnable [];
global.switchToThread thread
od else global.switchToIdleThread
od) (Guard ArrayBounds \<lbrace>UCAST(8 \<rightarrow> 32) curdom < 0x10\<rbrace> (IF \<acute>ksReadyQueuesL1Bitmap.[unat curdom] \<noteq> 0 THEN
  \<acute>prio :== CALL getHighestPrio_'proc(UCAST(8 \<rightarrow> 32) curdom);;
\<acute>ret__unsigned_long :== CALL ready_queues_index_'proc(UCAST(8 \<rightarrow> 32) curdom);;
Guard ArrayBounds \<lbrace>\<acute>ret__unsigned_long < 0x1000\<rbrace> (\<acute>thread :== head_C (\<acute>ksReadyQueues.[unat \<acute>ret__unsigned_long]));;
CALL switchToThread_'proc()
ELSE
  CALL switchToIdleThread_'proc()
FI))
 2. \<lbrace>?R301\<rbrace> if Suc 0 < numDomains then curDomain else return 0 \<lbrace>\<lambda>curdom. K (curdom \<le> maxDomain) and ?P'474 curdom\<rbrace>
 3. guard_is_UNIV (\<lambda>rv rv'. rv' = UCAST(8 \<rightarrow> 32) rv) dom_' (\<lambda>a b. {s'. a \<le> maxDomain \<longrightarrow> s' \<in> ?Q476 a b})
 4. \<And>s s'. \<lbrakk>(s, s') \<in> rf_sr; all_invs_but_ct_idle_or_in_cur_domain' s; s' \<in> UNIV\<rbrakk> \<Longrightarrow> ((\<lambda>_. True) and ?R301) s \<and> s' \<in> UNIV proof (prove)
goal (4 subgoals):
 1. \<And>curdom. ccorres dc xfdc (?P'474 curdom) (?C'478 curdom (UCAST(8 \<rightarrow> 32) curdom)) [SKIP] (do l1 <- getReadyQueuesL1Bitmap curdom;
if l1 \<noteq> 0 then do prio <- getHighestPrio curdom;
queue <- getQueue curdom prio;
thread <- return (HaskellLib_H.head queue);
runnable <- isRunnable thread;
haskell_assert runnable [];
global.switchToThread thread
od else global.switchToIdleThread
od) (IF \<acute>ksReadyQueuesL1Bitmap.[unat curdom] \<noteq> 0 THEN
  \<acute>prio :== CALL getHighestPrio_'proc(UCAST(8 \<rightarrow> 32) curdom);;
\<acute>ret__unsigned_long :== CALL ready_queues_index_'proc(UCAST(8 \<rightarrow> 32) curdom);;
Guard ArrayBounds \<lbrace>\<acute>ret__unsigned_long < 0x1000\<rbrace> (\<acute>thread :== head_C (\<acute>ksReadyQueues.[unat \<acute>ret__unsigned_long]));;
CALL switchToThread_'proc()
ELSE
  CALL switchToIdleThread_'proc()
FI)
 2. \<lbrace>?R301\<rbrace> if Suc 0 < numDomains then curDomain else return 0 \<lbrace>\<lambda>curdom. K (curdom \<le> maxDomain) and ?P'474 curdom\<rbrace>
 3. guard_is_UNIV (\<lambda>rv rv'. rv' = UCAST(8 \<rightarrow> 32) rv) dom_' (\<lambda>a b. {s'. a \<le> maxDomain \<longrightarrow> s' \<in> ?C'478 a b \<inter> \<lbrace>b < 0x10\<rbrace>})
 4. \<And>s s'. \<lbrakk>(s, s') \<in> rf_sr; all_invs_but_ct_idle_or_in_cur_domain' s; s' \<in> UNIV\<rbrakk> \<Longrightarrow> ((\<lambda>_. True) and ?R301) s \<and> s' \<in> UNIV proof (prove)
goal (4 subgoals):
 1. \<And>curdom rv. ccorres dc xfdc (?P480 curdom rv) (?P'482 curdom (UCAST(8 \<rightarrow> 32) curdom) rv) [SKIP] (if rv \<noteq> 0 then do prio <- getHighestPrio curdom;
queue <- getQueue curdom prio;
thread <- return (HaskellLib_H.head queue);
runnable <- isRunnable thread;
haskell_assert runnable [];
global.switchToThread thread
od else global.switchToIdleThread) (IF \<acute>ksReadyQueuesL1Bitmap.[unat curdom] \<noteq> 0 THEN
  \<acute>prio :== CALL getHighestPrio_'proc(UCAST(8 \<rightarrow> 32) curdom);;
\<acute>ret__unsigned_long :== CALL ready_queues_index_'proc(UCAST(8 \<rightarrow> 32) curdom);;
Guard ArrayBounds \<lbrace>\<acute>ret__unsigned_long < 0x1000\<rbrace> (\<acute>thread :== head_C (\<acute>ksReadyQueues.[unat \<acute>ret__unsigned_long]));;
CALL switchToThread_'proc()
ELSE
  CALL switchToIdleThread_'proc()
FI)
 2. \<lbrace>?R301\<rbrace> if Suc 0 < numDomains then curDomain else return 0 \<lbrace>\<lambda>curdom. K (curdom \<le> maxDomain) and (\<lambda>s. curdom \<le> maxDomain \<and> (\<forall>rv. ksReadyQueuesL1Bitmap s curdom = rv \<longrightarrow> ?P480 curdom rv s))\<rbrace>
 3. guard_is_UNIV (\<lambda>rv rv'. rv' = UCAST(8 \<rightarrow> 32) rv) dom_' (\<lambda>a b. {s'. a \<le> maxDomain \<longrightarrow> s' \<in> {s. \<forall>rv. ksReadyQueuesL1Bitmap_' (globals s).[unat a] = UCAST(32 \<rightarrow> 32) rv \<longrightarrow> s \<in> ?P'482 a b rv} \<inter> \<lbrace>b < 0x10\<rbrace>})
 4. \<And>s s'. \<lbrakk>(s, s') \<in> rf_sr; all_invs_but_ct_idle_or_in_cur_domain' s; s' \<in> UNIV\<rbrakk> \<Longrightarrow> ((\<lambda>_. True) and ?R301) s \<and> s' \<in> UNIV proof (prove)
goal (4 subgoals):
 1. \<And>curdom l1. ccorres dc xfdc (?P480 curdom l1) (?P'482 curdom (UCAST(8 \<rightarrow> 32) curdom) l1) [SKIP] (if l1 \<noteq> 0 then do prio <- getHighestPrio curdom;
queue <- getQueue curdom prio;
thread <- return (HaskellLib_H.head queue);
runnable <- isRunnable thread;
haskell_assert runnable [];
global.switchToThread thread
od else global.switchToIdleThread) (IF \<acute>ksReadyQueuesL1Bitmap.[unat curdom] \<noteq> 0 THEN
  \<acute>prio :== CALL getHighestPrio_'proc(UCAST(8 \<rightarrow> 32) curdom);;
\<acute>ret__unsigned_long :== CALL ready_queues_index_'proc(UCAST(8 \<rightarrow> 32) curdom);;
Guard ArrayBounds \<lbrace>\<acute>ret__unsigned_long < 0x1000\<rbrace> (\<acute>thread :== head_C (\<acute>ksReadyQueues.[unat \<acute>ret__unsigned_long]));;
CALL switchToThread_'proc()
ELSE
  CALL switchToIdleThread_'proc()
FI)
 2. \<lbrace>?R301\<rbrace> if Suc 0 < numDomains then curDomain else return 0 \<lbrace>\<lambda>curdom. K (curdom \<le> maxDomain) and (\<lambda>s. curdom \<le> maxDomain \<and> (\<forall>rv. ksReadyQueuesL1Bitmap s curdom = rv \<longrightarrow> ?P480 curdom rv s))\<rbrace>
 3. guard_is_UNIV (\<lambda>rv rv'. rv' = UCAST(8 \<rightarrow> 32) rv) dom_' (\<lambda>a b. {s'. a \<le> maxDomain \<longrightarrow> s' \<in> {s. \<forall>rv. ksReadyQueuesL1Bitmap_' (globals s).[unat a] = UCAST(32 \<rightarrow> 32) rv \<longrightarrow> s \<in> ?P'482 a b rv} \<inter> \<lbrace>b < 0x10\<rbrace>})
 4. \<And>s s'. \<lbrakk>(s, s') \<in> rf_sr; all_invs_but_ct_idle_or_in_cur_domain' s; s' \<in> UNIV\<rbrakk> \<Longrightarrow> ((\<lambda>_. True) and ?R301) s \<and> s' \<in> UNIV proof (prove)
goal (6 subgoals):
 1. \<And>curdom l1. \<forall>s s'. (s, s') \<in> rf_sr \<and> l1 = ksReadyQueuesL1Bitmap s curdom \<and> curdom \<le> maxDomain \<longrightarrow> (l1 \<noteq> 0) = (s' \<in> \<lbrace>\<acute>ksReadyQueuesL1Bitmap.[unat curdom] \<noteq> 0\<rbrace>)
 2. \<And>curdom l1. ccorres dc xfdc (?Pt484 curdom l1) (?Rt487 curdom (UCAST(8 \<rightarrow> 32) curdom) l1) [SKIP] (do prio <- getHighestPrio curdom;
queue <- getQueue curdom prio;
thread <- return (HaskellLib_H.head queue);
runnable <- isRunnable thread;
haskell_assert runnable [];
global.switchToThread thread
od) (\<acute>prio :== CALL getHighestPrio_'proc(UCAST(8 \<rightarrow> 32) curdom);;
\<acute>ret__unsigned_long :== CALL ready_queues_index_'proc(UCAST(8 \<rightarrow> 32) curdom);;
Guard ArrayBounds \<lbrace>\<acute>ret__unsigned_long < 0x1000\<rbrace> (\<acute>thread :== head_C (\<acute>ksReadyQueues.[unat \<acute>ret__unsigned_long]));;
CALL switchToThread_'proc())
 3. \<And>curdom l1. ccorres dc xfdc (?Pf484 curdom l1) (?Rf486 curdom (UCAST(8 \<rightarrow> 32) curdom) l1) [SKIP] global.switchToIdleThread (CALL switchToIdleThread_'proc())
 4. \<lbrace>?R301\<rbrace> if Suc 0 < numDomains then curDomain else return 0 \<lbrace>\<lambda>curdom. K (curdom \<le> maxDomain) and (\<lambda>s. curdom \<le> maxDomain \<and> (\<forall>rv. ksReadyQueuesL1Bitmap s curdom = rv \<longrightarrow> ((\<lambda>s. rv = ksReadyQueuesL1Bitmap s curdom \<and> curdom \<le> maxDomain) and (\<lambda>s. rv \<noteq> 0 \<longrightarrow> ?Pt484 curdom rv s) and (\<lambda>s. \<not> rv \<noteq> 0 \<longrightarrow> ?Pf484 curdom rv s)) s))\<rbrace>
 5. guard_is_UNIV (\<lambda>rv rv'. rv' = UCAST(8 \<rightarrow> 32) rv) dom_' (\<lambda>a b. {s'. a \<le> maxDomain \<longrightarrow> s' \<in> {s. \<forall>rv. ksReadyQueuesL1Bitmap_' (globals s).[unat a] = UCAST(32 \<rightarrow> 32) rv \<longrightarrow> s \<in> ?Rt487 a b rv \<inter> \<lbrace>\<acute>ksReadyQueuesL1Bitmap.[unat a] \<noteq> 0\<rbrace> \<union> ?Rf486 a b rv \<inter> - \<lbrace>\<acute>ksReadyQueuesL1Bitmap.[unat a] \<noteq> 0\<rbrace>} \<inter> \<lbrace>b < 0x10\<rbrace>})
 6. \<And>s s'. \<lbrakk>(s, s') \<in> rf_sr; all_invs_but_ct_idle_or_in_cur_domain' s; s' \<in> UNIV\<rbrakk> \<Longrightarrow> ((\<lambda>_. True) and ?R301) s \<and> s' \<in> UNIV proof (prove)
goal (1 subgoal):
 1. \<forall>s s'. (s, s') \<in> rf_sr \<and> l1_ = ksReadyQueuesL1Bitmap s curdom_ \<and> curdom_ \<le> maxDomain \<longrightarrow> (l1_ \<noteq> 0) = (s' \<in> \<lbrace>\<acute>ksReadyQueuesL1Bitmap.[unat curdom_] \<noteq> 0\<rbrace>) proof (prove)
goal (5 subgoals):
 1. \<And>curdom l1. ccorres dc xfdc (?Pt484 curdom l1) (?Rt487 curdom (UCAST(8 \<rightarrow> 32) curdom) l1) [SKIP] (do prio <- getHighestPrio curdom;
queue <- getQueue curdom prio;
thread <- return (HaskellLib_H.head queue);
runnable <- isRunnable thread;
haskell_assert runnable [];
global.switchToThread thread
od) (\<acute>prio :== CALL getHighestPrio_'proc(UCAST(8 \<rightarrow> 32) curdom);;
\<acute>ret__unsigned_long :== CALL ready_queues_index_'proc(UCAST(8 \<rightarrow> 32) curdom);;
Guard ArrayBounds \<lbrace>\<acute>ret__unsigned_long < 0x1000\<rbrace> (\<acute>thread :== head_C (\<acute>ksReadyQueues.[unat \<acute>ret__unsigned_long]));;
CALL switchToThread_'proc())
 2. \<And>curdom l1. ccorres dc xfdc (?Pf484 curdom l1) (?Rf486 curdom (UCAST(8 \<rightarrow> 32) curdom) l1) [SKIP] global.switchToIdleThread (CALL switchToIdleThread_'proc())
 3. \<lbrace>?R301\<rbrace> if Suc 0 < numDomains then curDomain else return 0 \<lbrace>\<lambda>curdom. K (curdom \<le> maxDomain) and (\<lambda>s. curdom \<le> maxDomain \<and> (\<forall>rv. ksReadyQueuesL1Bitmap s curdom = rv \<longrightarrow> ((\<lambda>s. rv = ksReadyQueuesL1Bitmap s curdom \<and> curdom \<le> maxDomain) and (\<lambda>s. rv \<noteq> 0 \<longrightarrow> ?Pt484 curdom rv s) and (\<lambda>s. \<not> rv \<noteq> 0 \<longrightarrow> ?Pf484 curdom rv s)) s))\<rbrace>
 4. guard_is_UNIV (\<lambda>rv rv'. rv' = UCAST(8 \<rightarrow> 32) rv) dom_' (\<lambda>a b. {s'. a \<le> maxDomain \<longrightarrow> s' \<in> {s. \<forall>rv. ksReadyQueuesL1Bitmap_' (globals s).[unat a] = UCAST(32 \<rightarrow> 32) rv \<longrightarrow> s \<in> ?Rt487 a b rv \<inter> \<lbrace>\<acute>ksReadyQueuesL1Bitmap.[unat a] \<noteq> 0\<rbrace> \<union> ?Rf486 a b rv \<inter> - \<lbrace>\<acute>ksReadyQueuesL1Bitmap.[unat a] \<noteq> 0\<rbrace>} \<inter> \<lbrace>b < 0x10\<rbrace>})
 5. \<And>s s'. \<lbrakk>(s, s') \<in> rf_sr; all_invs_but_ct_idle_or_in_cur_domain' s; s' \<in> UNIV\<rbrakk> \<Longrightarrow> ((\<lambda>_. True) and ?R301) s \<and> s' \<in> UNIV proof (prove)
goal (5 subgoals):
 1. \<And>curdom l1. ccorres dc xfdc (?Pf484 curdom l1) (?Rf486 curdom (UCAST(8 \<rightarrow> 32) curdom) l1) [SKIP] global.switchToIdleThread (CALL switchToIdleThread_'proc())
 2. \<And>curdom l1. ccorres dc xfdc (?Pt484 curdom l1) (?Rt487 curdom (UCAST(8 \<rightarrow> 32) curdom) l1) [SKIP] (do prio <- getHighestPrio curdom;
queue <- getQueue curdom prio;
thread <- return (HaskellLib_H.head queue);
runnable <- isRunnable thread;
haskell_assert runnable [];
global.switchToThread thread
od) (\<acute>prio :== CALL getHighestPrio_'proc(UCAST(8 \<rightarrow> 32) curdom);;
\<acute>ret__unsigned_long :== CALL ready_queues_index_'proc(UCAST(8 \<rightarrow> 32) curdom);;
Guard ArrayBounds \<lbrace>\<acute>ret__unsigned_long < 0x1000\<rbrace> (\<acute>thread :== head_C (\<acute>ksReadyQueues.[unat \<acute>ret__unsigned_long]));;
CALL switchToThread_'proc())
 3. \<lbrace>?R301\<rbrace> if Suc 0 < numDomains then curDomain else return 0 \<lbrace>\<lambda>curdom. K (curdom \<le> maxDomain) and (\<lambda>s. curdom \<le> maxDomain \<and> (\<forall>rv. ksReadyQueuesL1Bitmap s curdom = rv \<longrightarrow> ((\<lambda>s. rv = ksReadyQueuesL1Bitmap s curdom \<and> curdom \<le> maxDomain) and (\<lambda>s. rv \<noteq> 0 \<longrightarrow> ?Pt484 curdom rv s) and (\<lambda>s. \<not> rv \<noteq> 0 \<longrightarrow> ?Pf484 curdom rv s)) s))\<rbrace>
 4. guard_is_UNIV (\<lambda>rv rv'. rv' = UCAST(8 \<rightarrow> 32) rv) dom_' (\<lambda>a b. {s'. a \<le> maxDomain \<longrightarrow> s' \<in> {s. \<forall>rv. ksReadyQueuesL1Bitmap_' (globals s).[unat a] = UCAST(32 \<rightarrow> 32) rv \<longrightarrow> s \<in> ?Rt487 a b rv \<inter> \<lbrace>\<acute>ksReadyQueuesL1Bitmap.[unat a] \<noteq> 0\<rbrace> \<union> ?Rf486 a b rv \<inter> - \<lbrace>\<acute>ksReadyQueuesL1Bitmap.[unat a] \<noteq> 0\<rbrace>} \<inter> \<lbrace>b < 0x10\<rbrace>})
 5. \<And>s s'. \<lbrakk>(s, s') \<in> rf_sr; all_invs_but_ct_idle_or_in_cur_domain' s; s' \<in> UNIV\<rbrakk> \<Longrightarrow> ((\<lambda>_. True) and ?R301) s \<and> s' \<in> UNIV proof (prove)
goal (4 subgoals):
 1. \<And>curdom l1. ccorres dc xfdc (?Pt484 curdom l1) (?Rt487 curdom (UCAST(8 \<rightarrow> 32) curdom) l1) [SKIP] (do prio <- getHighestPrio curdom;
queue <- getQueue curdom prio;
thread <- return (HaskellLib_H.head queue);
runnable <- isRunnable thread;
haskell_assert runnable [];
global.switchToThread thread
od) (\<acute>prio :== CALL getHighestPrio_'proc(UCAST(8 \<rightarrow> 32) curdom);;
\<acute>ret__unsigned_long :== CALL ready_queues_index_'proc(UCAST(8 \<rightarrow> 32) curdom);;
Guard ArrayBounds \<lbrace>\<acute>ret__unsigned_long < 0x1000\<rbrace> (\<acute>thread :== head_C (\<acute>ksReadyQueues.[unat \<acute>ret__unsigned_long]));;
CALL switchToThread_'proc())
 2. \<lbrace>?R301\<rbrace> if Suc 0 < numDomains then curDomain else return 0 \<lbrace>\<lambda>curdom. K (curdom \<le> maxDomain) and (\<lambda>s. curdom \<le> maxDomain \<and> (\<forall>rv. ksReadyQueuesL1Bitmap s curdom = rv \<longrightarrow> ((\<lambda>s. rv = ksReadyQueuesL1Bitmap s curdom \<and> curdom \<le> maxDomain) and (\<lambda>s. rv \<noteq> 0 \<longrightarrow> ?Pt484 curdom rv s) and (\<lambda>s. \<not> rv \<noteq> 0 \<longrightarrow> all_invs_but_ct_idle_or_in_cur_domain' s)) s))\<rbrace>
 3. guard_is_UNIV (\<lambda>rv rv'. rv' = UCAST(8 \<rightarrow> 32) rv) dom_' (\<lambda>a b. {s'. a \<le> maxDomain \<longrightarrow> s' \<in> {s. \<forall>rv. ksReadyQueuesL1Bitmap_' (globals s).[unat a] = UCAST(32 \<rightarrow> 32) rv \<longrightarrow> s \<in> ?Rt487 a b rv \<inter> \<lbrace>\<acute>ksReadyQueuesL1Bitmap.[unat a] \<noteq> 0\<rbrace> \<union> {s. s \<in> UNIV} \<inter> - \<lbrace>\<acute>ksReadyQueuesL1Bitmap.[unat a] \<noteq> 0\<rbrace>} \<inter> \<lbrace>b < 0x10\<rbrace>})
 4. \<And>s s'. \<lbrakk>(s, s') \<in> rf_sr; all_invs_but_ct_idle_or_in_cur_domain' s; s' \<in> UNIV\<rbrakk> \<Longrightarrow> ((\<lambda>_. True) and ?R301) s \<and> s' \<in> UNIV proof (prove)
goal (4 subgoals):
 1. \<And>curdom l1. ccorres dc xfdc (?Pt484 curdom l1) (?Rt487 curdom (UCAST(8 \<rightarrow> 32) curdom) l1) [SKIP] (do prio <- gets (lookupBitmapPriority curdom);
queue <- getQueue curdom prio;
runnable <- isRunnable (hd queue);
a <- assert runnable;
global.switchToThread (hd queue)
od) (\<acute>prio :== CALL getHighestPrio_'proc(UCAST(8 \<rightarrow> 32) curdom);;
\<acute>ret__unsigned_long :== CALL ready_queues_index_'proc(UCAST(8 \<rightarrow> 32) curdom);;
Guard ArrayBounds \<lbrace>\<acute>ret__unsigned_long < 0x1000\<rbrace> (\<acute>thread :== head_C (\<acute>ksReadyQueues.[unat \<acute>ret__unsigned_long]));;
CALL switchToThread_'proc())
 2. \<lbrace>?R301\<rbrace> if Suc 0 < numDomains then curDomain else return 0 \<lbrace>\<lambda>curdom. K (curdom \<le> maxDomain) and (\<lambda>s. curdom \<le> maxDomain \<and> (\<forall>rv. ksReadyQueuesL1Bitmap s curdom = rv \<longrightarrow> ((\<lambda>s. rv = ksReadyQueuesL1Bitmap s curdom \<and> curdom \<le> maxDomain) and (\<lambda>s. rv \<noteq> 0 \<longrightarrow> ?Pt484 curdom rv s) and (\<lambda>s. \<not> rv \<noteq> 0 \<longrightarrow> all_invs_but_ct_idle_or_in_cur_domain' s)) s))\<rbrace>
 3. guard_is_UNIV (\<lambda>rv rv'. rv' = UCAST(8 \<rightarrow> 32) rv) dom_' (\<lambda>a b. {s'. a \<le> maxDomain \<longrightarrow> s' \<in> {s. \<forall>rv. ksReadyQueuesL1Bitmap_' (globals s).[unat a] = UCAST(32 \<rightarrow> 32) rv \<longrightarrow> s \<in> ?Rt487 a b rv \<inter> \<lbrace>\<acute>ksReadyQueuesL1Bitmap.[unat a] \<noteq> 0\<rbrace> \<union> {s. s \<in> UNIV} \<inter> - \<lbrace>\<acute>ksReadyQueuesL1Bitmap.[unat a] \<noteq> 0\<rbrace>} \<inter> \<lbrace>b < 0x10\<rbrace>})
 4. \<And>s s'. \<lbrakk>(s, s') \<in> rf_sr; all_invs_but_ct_idle_or_in_cur_domain' s; s' \<in> UNIV\<rbrakk> \<Longrightarrow> ((\<lambda>_. True) and ?R301) s \<and> s' \<in> UNIV proof (prove)
goal (4 subgoals):
 1. \<And>curdom l1. ccorres dc xfdc (?Pt484 curdom l1) (?Rt487 curdom (UCAST(8 \<rightarrow> 32) curdom) l1) [SKIP] (do prio <- gets (lookupBitmapPriority curdom);
queue <- getQueue curdom prio;
runnable <- isRunnable (hd queue);
a <- assert runnable;
global.switchToThread (hd queue)
od) (\<acute>prio :== CALL getHighestPrio_'proc(UCAST(8 \<rightarrow> 32) curdom);;
(\<acute>ret__unsigned_long :== CALL ready_queues_index_'proc(UCAST(8 \<rightarrow> 32) curdom);;
(Guard ArrayBounds \<lbrace>\<acute>ret__unsigned_long < 0x1000\<rbrace> (\<acute>thread :== head_C (\<acute>ksReadyQueues.[unat \<acute>ret__unsigned_long]));;
CALL switchToThread_'proc())))
 2. \<lbrace>?R301\<rbrace> if Suc 0 < numDomains then curDomain else return 0 \<lbrace>\<lambda>curdom. K (curdom \<le> maxDomain) and (\<lambda>s. curdom \<le> maxDomain \<and> (\<forall>rv. ksReadyQueuesL1Bitmap s curdom = rv \<longrightarrow> ((\<lambda>s. rv = ksReadyQueuesL1Bitmap s curdom \<and> curdom \<le> maxDomain) and (\<lambda>s. rv \<noteq> 0 \<longrightarrow> ?Pt484 curdom rv s) and (\<lambda>s. \<not> rv \<noteq> 0 \<longrightarrow> all_invs_but_ct_idle_or_in_cur_domain' s)) s))\<rbrace>
 3. guard_is_UNIV (\<lambda>rv rv'. rv' = UCAST(8 \<rightarrow> 32) rv) dom_' (\<lambda>a b. {s'. a \<le> maxDomain \<longrightarrow> s' \<in> {s. \<forall>rv. ksReadyQueuesL1Bitmap_' (globals s).[unat a] = UCAST(32 \<rightarrow> 32) rv \<longrightarrow> s \<in> ?Rt487 a b rv \<inter> \<lbrace>\<acute>ksReadyQueuesL1Bitmap.[unat a] \<noteq> 0\<rbrace> \<union> {s. s \<in> UNIV} \<inter> - \<lbrace>\<acute>ksReadyQueuesL1Bitmap.[unat a] \<noteq> 0\<rbrace>} \<inter> \<lbrace>b < 0x10\<rbrace>})
 4. \<And>s s'. \<lbrakk>(s, s') \<in> rf_sr; all_invs_but_ct_idle_or_in_cur_domain' s; s' \<in> UNIV\<rbrakk> \<Longrightarrow> ((\<lambda>_. True) and ?R301) s \<and> s' \<in> UNIV proof (prove)
goal (8 subgoals):
 1. \<And>curdom l1. ccorres (?r'503 curdom l1) (?xf'503 curdom l1) (?P503 curdom l1) (?Rt487 curdom (UCAST(8 \<rightarrow> 32) curdom) l1) [] (gets (lookupBitmapPriority curdom)) (\<acute>prio :== CALL getHighestPrio_'proc(UCAST(8 \<rightarrow> 32) curdom))
 2. \<And>curdom l1 rv' t t'. ceqv \<Gamma> (?xf'503 curdom l1) rv' t t' (\<acute>ret__unsigned_long :== CALL ready_queues_index_'proc(UCAST(8 \<rightarrow> 32) curdom);;
(Guard ArrayBounds \<lbrace>\<acute>ret__unsigned_long < 0x1000\<rbrace> (\<acute>thread :== head_C (\<acute>ksReadyQueues.[unat \<acute>ret__unsigned_long]));;
CALL switchToThread_'proc())) (?d'503 curdom l1 rv')
 3. \<And>curdom l1 rv rv'. ?r'503 curdom l1 rv rv' \<Longrightarrow> ccorres dc xfdc (?Q503 curdom l1 rv) (?Q'503 curdom l1 rv rv') [SKIP] (do queue <- getQueue curdom rv;
runnable <- isRunnable (hd queue);
a <- assert runnable;
global.switchToThread (hd queue)
od) (?d'503 curdom l1 rv')
 4. \<And>curdom l1. \<lbrace>?R503 curdom l1\<rbrace> gets (lookupBitmapPriority curdom) \<lbrace>?Q503 curdom l1\<rbrace>
 5. \<And>curdom l1. guard_is_UNIV (?r'503 curdom l1) (?xf'503 curdom l1) (?Q'503 curdom l1)
 6. \<lbrace>?R301\<rbrace> if Suc 0 < numDomains then curDomain else return 0 \<lbrace>\<lambda>curdom. K (curdom \<le> maxDomain) and (\<lambda>s. curdom \<le> maxDomain \<and> (\<forall>rv. ksReadyQueuesL1Bitmap s curdom = rv \<longrightarrow> ((\<lambda>s. rv = ksReadyQueuesL1Bitmap s curdom \<and> curdom \<le> maxDomain) and (\<lambda>s. rv \<noteq> 0 \<longrightarrow> (?P503 curdom rv and ?R503 curdom rv) s) and (\<lambda>s. \<not> rv \<noteq> 0 \<longrightarrow> all_invs_but_ct_idle_or_in_cur_domain' s)) s))\<rbrace>
 7. guard_is_UNIV (\<lambda>rv rv'. rv' = UCAST(8 \<rightarrow> 32) rv) dom_' (\<lambda>a b. {s'. a \<le> maxDomain \<longrightarrow> s' \<in> {s. \<forall>rv. ksReadyQueuesL1Bitmap_' (globals s).[unat a] = UCAST(32 \<rightarrow> 32) rv \<longrightarrow> s \<in> ?Rt487 a b rv \<inter> \<lbrace>\<acute>ksReadyQueuesL1Bitmap.[unat a] \<noteq> 0\<rbrace> \<union> {s. s \<in> UNIV} \<inter> - \<lbrace>\<acute>ksReadyQueuesL1Bitmap.[unat a] \<noteq> 0\<rbrace>} \<inter> \<lbrace>b < 0x10\<rbrace>})
 8. \<And>s s'. \<lbrakk>(s, s') \<in> rf_sr; all_invs_but_ct_idle_or_in_cur_domain' s; s' \<in> UNIV\<rbrakk> \<Longrightarrow> ((\<lambda>_. True) and ?R301) s \<and> s' \<in> UNIV proof (prove)
goal (11 subgoals):
 1. \<And>curdom l1. ccorres (?r'503 curdom l1) (?xf''509 curdom l1) (?P503 curdom l1) (?C'511 curdom (UCAST(8 \<rightarrow> 32) curdom) l1) [] (gets (lookupBitmapPriority curdom)) (Call getHighestPrio_'proc)
 2. \<And>curdom l1 x y s. globals (prio_'_update (\<lambda>_. ret__unsigned_long_' y) s) = globals s
 3. \<And>curdom l1 a s t. prio_' (prio_'_update (\<lambda>_. ret__unsigned_long_' t) (s\<lparr>globals := globals t\<rparr>)) = ?xf''509 curdom l1 t
 4. \<And>curdom l1 s. globals (dom_'_update (\<lambda>x. UCAST(8 \<rightarrow> 32) curdom) s) = globals s
 5. \<And>curdom l1 rv' t t'. ceqv \<Gamma> prio_' rv' t t' (\<acute>ret__unsigned_long :== CALL ready_queues_index_'proc(UCAST(8 \<rightarrow> 32) curdom);;
(Guard ArrayBounds \<lbrace>\<acute>ret__unsigned_long < 0x1000\<rbrace> (\<acute>thread :== head_C (\<acute>ksReadyQueues.[unat \<acute>ret__unsigned_long]));;
CALL switchToThread_'proc())) (?d'503 curdom l1 rv')
 6. \<And>curdom l1 rv rv'. ?r'503 curdom l1 rv rv' \<Longrightarrow> ccorres dc xfdc (?Q503 curdom l1 rv) (?Q'503 curdom l1 rv rv') [SKIP] (do queue <- getQueue curdom rv;
runnable <- isRunnable (hd queue);
a <- assert runnable;
global.switchToThread (hd queue)
od) (?d'503 curdom l1 rv')
 7. \<And>curdom l1. \<lbrace>?R503 curdom l1\<rbrace> gets (lookupBitmapPriority curdom) \<lbrace>?Q503 curdom l1\<rbrace>
 8. \<And>curdom l1. guard_is_UNIV (?r'503 curdom l1) prio_' (?Q'503 curdom l1)
 9. \<lbrace>?R301\<rbrace> if Suc 0 < numDomains then curDomain else return 0 \<lbrace>\<lambda>curdom. K (curdom \<le> maxDomain) and (\<lambda>s. curdom \<le> maxDomain \<and> (\<forall>rv. ksReadyQueuesL1Bitmap s curdom = rv \<longrightarrow> ((\<lambda>s. rv = ksReadyQueuesL1Bitmap s curdom \<and> curdom \<le> maxDomain) and (\<lambda>s. rv \<noteq> 0 \<longrightarrow> (?P503 curdom rv and ?R503 curdom rv) s) and (\<lambda>s. \<not> rv \<noteq> 0 \<longrightarrow> all_invs_but_ct_idle_or_in_cur_domain' s)) s))\<rbrace>
 10. guard_is_UNIV (\<lambda>rv rv'. rv' = UCAST(8 \<rightarrow> 32) rv) dom_' (\<lambda>a b. {s'. a \<le> maxDomain \<longrightarrow> s' \<in> {s. \<forall>rv. ksReadyQueuesL1Bitmap_' (globals s).[unat a] = UCAST(32 \<rightarrow> 32) rv \<longrightarrow> s \<in> {s. dom_'_update (\<lambda>x. b) s \<in> ?C'511 a b rv} \<inter> \<lbrace>\<acute>ksReadyQueuesL1Bitmap.[unat a] \<noteq> 0\<rbrace> \<union> {s. s \<in> UNIV} \<inter> - \<lbrace>\<acute>ksReadyQueuesL1Bitmap.[unat a] \<noteq> 0\<rbrace>} \<inter> \<lbrace>b < 0x10\<rbrace>})
A total of 11 subgoals... proof (prove)
goal (10 subgoals):
 1. \<And>curdom l1 x y s. globals (prio_'_update (\<lambda>_. ret__unsigned_long_' y) s) = globals s
 2. \<And>curdom l1 a s t. prio_' (prio_'_update (\<lambda>_. ret__unsigned_long_' t) (s\<lparr>globals := globals t\<rparr>)) = ret__unsigned_long_' t
 3. \<And>curdom l1 s. globals (dom_'_update (\<lambda>x. UCAST(8 \<rightarrow> 32) curdom) s) = globals s
 4. \<And>curdom l1 rv' t t'. ceqv \<Gamma> prio_' rv' t t' (\<acute>ret__unsigned_long :== CALL ready_queues_index_'proc(UCAST(8 \<rightarrow> 32) curdom);;
(Guard ArrayBounds \<lbrace>\<acute>ret__unsigned_long < 0x1000\<rbrace> (\<acute>thread :== head_C (\<acute>ksReadyQueues.[unat \<acute>ret__unsigned_long]));;
CALL switchToThread_'proc())) (?d'503 curdom l1 rv')
 5. \<And>curdom l1 rv rv'. rv' = UCAST(8 \<rightarrow> 32) rv \<Longrightarrow> ccorres dc xfdc (?Q503 curdom l1 rv) (?Q'503 curdom l1 rv rv') [SKIP] (do queue <- getQueue curdom rv;
runnable <- isRunnable (hd queue);
a <- assert runnable;
global.switchToThread (hd queue)
od) (?d'503 curdom l1 rv')
 6. \<And>curdom l1. \<lbrace>?R503 curdom l1\<rbrace> gets (lookupBitmapPriority curdom) \<lbrace>?Q503 curdom l1\<rbrace>
 7. \<And>curdom l1. guard_is_UNIV (\<lambda>rv rv'. rv' = UCAST(8 \<rightarrow> 32) rv) prio_' (?Q'503 curdom l1)
 8. \<lbrace>?R301\<rbrace> if Suc 0 < numDomains then curDomain else return 0 \<lbrace>\<lambda>curdom. K (curdom \<le> maxDomain) and (\<lambda>s. curdom \<le> maxDomain \<and> (\<forall>rv. ksReadyQueuesL1Bitmap s curdom = rv \<longrightarrow> ((\<lambda>s. rv = ksReadyQueuesL1Bitmap s curdom \<and> curdom \<le> maxDomain) and (\<lambda>s. rv \<noteq> 0 \<longrightarrow> ((\<lambda>s. curdom \<le> maxDomain \<and> ksReadyQueuesL1Bitmap s curdom \<noteq> 0 \<and> bitmapQ_no_L1_orphans s) and ?R503 curdom rv) s) and (\<lambda>s. \<not> rv \<noteq> 0 \<longrightarrow> all_invs_but_ct_idle_or_in_cur_domain' s)) s))\<rbrace>
 9. guard_is_UNIV (\<lambda>rv rv'. rv' = UCAST(8 \<rightarrow> 32) rv) dom_' (\<lambda>a b. {s'. a \<le> maxDomain \<longrightarrow> s' \<in> {s. \<forall>rv. ksReadyQueuesL1Bitmap_' (globals s).[unat a] = UCAST(32 \<rightarrow> 32) rv \<longrightarrow> s \<in> {s. dom_'_update (\<lambda>x. b) s \<in> UNIV \<inter> \<lbrace>\<acute>dom = b\<rbrace>} \<inter> \<lbrace>\<acute>ksReadyQueuesL1Bitmap.[unat a] \<noteq> 0\<rbrace> \<union> {s. s \<in> UNIV} \<inter> - \<lbrace>\<acute>ksReadyQueuesL1Bitmap.[unat a] \<noteq> 0\<rbrace>} \<inter> \<lbrace>b < 0x10\<rbrace>})
 10. \<And>s s'. \<lbrakk>(s, s') \<in> rf_sr; all_invs_but_ct_idle_or_in_cur_domain' s; s' \<in> UNIV\<rbrakk> \<Longrightarrow> ((\<lambda>_. True) and ?R301) s \<and> s' \<in> UNIV proof (prove)
goal (7 subgoals):
 1. \<And>curdom l1 rv' t t'. ceqv \<Gamma> prio_' rv' t t' (\<acute>ret__unsigned_long :== CALL ready_queues_index_'proc(UCAST(8 \<rightarrow> 32) curdom);;
(Guard ArrayBounds \<lbrace>\<acute>ret__unsigned_long < 0x1000\<rbrace> (\<acute>thread :== head_C (\<acute>ksReadyQueues.[unat \<acute>ret__unsigned_long]));;
CALL switchToThread_'proc())) (?d'503 curdom l1 rv')
 2. \<And>curdom l1 rv rv'. rv' = UCAST(8 \<rightarrow> 32) rv \<Longrightarrow> ccorres dc xfdc (?Q503 curdom l1 rv) (?Q'503 curdom l1 rv rv') [SKIP] (do queue <- getQueue curdom rv;
runnable <- isRunnable (hd queue);
a <- assert runnable;
global.switchToThread (hd queue)
od) (?d'503 curdom l1 rv')
 3. \<And>curdom l1. \<lbrace>?R503 curdom l1\<rbrace> gets (lookupBitmapPriority curdom) \<lbrace>?Q503 curdom l1\<rbrace>
 4. \<And>curdom l1. guard_is_UNIV (\<lambda>rv rv'. rv' = UCAST(8 \<rightarrow> 32) rv) prio_' (?Q'503 curdom l1)
 5. \<lbrace>?R301\<rbrace> if Suc 0 < numDomains then curDomain else return 0 \<lbrace>\<lambda>curdom. K (curdom \<le> maxDomain) and (\<lambda>s. curdom \<le> maxDomain \<and> (\<forall>rv. ksReadyQueuesL1Bitmap s curdom = rv \<longrightarrow> ((\<lambda>s. rv = ksReadyQueuesL1Bitmap s curdom \<and> curdom \<le> maxDomain) and (\<lambda>s. rv \<noteq> 0 \<longrightarrow> ((\<lambda>s. curdom \<le> maxDomain \<and> ksReadyQueuesL1Bitmap s curdom \<noteq> 0 \<and> bitmapQ_no_L1_orphans s) and ?R503 curdom rv) s) and (\<lambda>s. \<not> rv \<noteq> 0 \<longrightarrow> all_invs_but_ct_idle_or_in_cur_domain' s)) s))\<rbrace>
 6. guard_is_UNIV (\<lambda>rv rv'. rv' = UCAST(8 \<rightarrow> 32) rv) dom_' (\<lambda>a b. {s'. a \<le> maxDomain \<longrightarrow> s' \<in> {s. \<forall>rv. ksReadyQueuesL1Bitmap_' (globals s).[unat a] = UCAST(32 \<rightarrow> 32) rv \<longrightarrow> s \<in> {s. dom_'_update (\<lambda>x. b) s \<in> UNIV \<inter> \<lbrace>\<acute>dom = b\<rbrace>} \<inter> \<lbrace>\<acute>ksReadyQueuesL1Bitmap.[unat a] \<noteq> 0\<rbrace> \<union> {s. s \<in> UNIV} \<inter> - \<lbrace>\<acute>ksReadyQueuesL1Bitmap.[unat a] \<noteq> 0\<rbrace>} \<inter> \<lbrace>b < 0x10\<rbrace>})
 7. \<And>s s'. \<lbrakk>(s, s') \<in> rf_sr; all_invs_but_ct_idle_or_in_cur_domain' s; s' \<in> UNIV\<rbrakk> \<Longrightarrow> ((\<lambda>_. True) and ?R301) s \<and> s' \<in> UNIV proof (prove)
goal (6 subgoals):
 1. \<And>curdom l1 rv rv'. rv' = UCAST(8 \<rightarrow> 32) rv \<Longrightarrow> ccorres dc xfdc (?Q503 curdom l1 rv) (?Q'503 curdom l1 rv rv') [SKIP] (do queue <- getQueue curdom rv;
runnable <- isRunnable (hd queue);
a <- assert runnable;
global.switchToThread (hd queue)
od) (\<acute>ret__unsigned_long :== CALL ready_queues_index_'proc(UCAST(8 \<rightarrow> 32) curdom,rv');;
(Guard ArrayBounds \<lbrace>\<acute>ret__unsigned_long < 0x1000\<rbrace> (\<acute>thread :== head_C (\<acute>ksReadyQueues.[unat \<acute>ret__unsigned_long]));;
CALL switchToThread_'proc(\<acute>thread)))
 2. \<And>curdom l1. \<lbrace>?R503 curdom l1\<rbrace> gets (lookupBitmapPriority curdom) \<lbrace>?Q503 curdom l1\<rbrace>
 3. \<And>curdom l1. guard_is_UNIV (\<lambda>rv rv'. rv' = UCAST(8 \<rightarrow> 32) rv) prio_' (?Q'503 curdom l1)
 4. \<lbrace>?R301\<rbrace> if Suc 0 < numDomains then curDomain else return 0 \<lbrace>\<lambda>curdom. K (curdom \<le> maxDomain) and (\<lambda>s. curdom \<le> maxDomain \<and> (\<forall>rv. ksReadyQueuesL1Bitmap s curdom = rv \<longrightarrow> ((\<lambda>s. rv = ksReadyQueuesL1Bitmap s curdom \<and> curdom \<le> maxDomain) and (\<lambda>s. rv \<noteq> 0 \<longrightarrow> ((\<lambda>s. curdom \<le> maxDomain \<and> ksReadyQueuesL1Bitmap s curdom \<noteq> 0 \<and> bitmapQ_no_L1_orphans s) and ?R503 curdom rv) s) and (\<lambda>s. \<not> rv \<noteq> 0 \<longrightarrow> all_invs_but_ct_idle_or_in_cur_domain' s)) s))\<rbrace>
 5. guard_is_UNIV (\<lambda>rv rv'. rv' = UCAST(8 \<rightarrow> 32) rv) dom_' (\<lambda>a b. {s'. a \<le> maxDomain \<longrightarrow> s' \<in> {s. \<forall>rv. ksReadyQueuesL1Bitmap_' (globals s).[unat a] = UCAST(32 \<rightarrow> 32) rv \<longrightarrow> s \<in> {s. dom_'_update (\<lambda>x. b) s \<in> UNIV \<inter> \<lbrace>\<acute>dom = b\<rbrace>} \<inter> \<lbrace>\<acute>ksReadyQueuesL1Bitmap.[unat a] \<noteq> 0\<rbrace> \<union> {s. s \<in> UNIV} \<inter> - \<lbrace>\<acute>ksReadyQueuesL1Bitmap.[unat a] \<noteq> 0\<rbrace>} \<inter> \<lbrace>b < 0x10\<rbrace>})
 6. \<And>s s'. \<lbrakk>(s, s') \<in> rf_sr; all_invs_but_ct_idle_or_in_cur_domain' s; s' \<in> UNIV\<rbrakk> \<Longrightarrow> ((\<lambda>_. True) and ?R301) s \<and> s' \<in> UNIV proof (prove)
goal (6 subgoals):
 1. \<And>curdom l1 rv. ccorres dc xfdc (?Q503 curdom l1 rv) (?Q'503 curdom l1 rv (UCAST(8 \<rightarrow> 32) rv)) [SKIP] (do queue <- getQueue curdom rv;
runnable <- isRunnable (hd queue);
a <- assert runnable;
global.switchToThread (hd queue)
od) (\<acute>ret__unsigned_long :== CALL ready_queues_index_'proc(UCAST(8 \<rightarrow> 32) curdom,UCAST(8 \<rightarrow> 32) rv);;
(Guard ArrayBounds \<lbrace>\<acute>ret__unsigned_long < 0x1000\<rbrace> (\<acute>thread :== head_C (\<acute>ksReadyQueues.[unat \<acute>ret__unsigned_long]));;
CALL switchToThread_'proc()))
 2. \<And>curdom l1. \<lbrace>?R503 curdom l1\<rbrace> gets (lookupBitmapPriority curdom) \<lbrace>?Q503 curdom l1\<rbrace>
 3. \<And>curdom l1. guard_is_UNIV (\<lambda>rv rv'. rv' = UCAST(8 \<rightarrow> 32) rv) prio_' (?Q'503 curdom l1)
 4. \<lbrace>?R301\<rbrace> if Suc 0 < numDomains then curDomain else return 0 \<lbrace>\<lambda>curdom. K (curdom \<le> maxDomain) and (\<lambda>s. curdom \<le> maxDomain \<and> (\<forall>rv. ksReadyQueuesL1Bitmap s curdom = rv \<longrightarrow> ((\<lambda>s. rv = ksReadyQueuesL1Bitmap s curdom \<and> curdom \<le> maxDomain) and (\<lambda>s. rv \<noteq> 0 \<longrightarrow> ((\<lambda>s. curdom \<le> maxDomain \<and> ksReadyQueuesL1Bitmap s curdom \<noteq> 0 \<and> bitmapQ_no_L1_orphans s) and ?R503 curdom rv) s) and (\<lambda>s. \<not> rv \<noteq> 0 \<longrightarrow> all_invs_but_ct_idle_or_in_cur_domain' s)) s))\<rbrace>
 5. guard_is_UNIV (\<lambda>rv rv'. rv' = UCAST(8 \<rightarrow> 32) rv) dom_' (\<lambda>a b. {s'. a \<le> maxDomain \<longrightarrow> s' \<in> {s. \<forall>rv. ksReadyQueuesL1Bitmap_' (globals s).[unat a] = UCAST(32 \<rightarrow> 32) rv \<longrightarrow> s \<in> {s. dom_'_update (\<lambda>x. b) s \<in> UNIV \<inter> \<lbrace>\<acute>dom = b\<rbrace>} \<inter> \<lbrace>\<acute>ksReadyQueuesL1Bitmap.[unat a] \<noteq> 0\<rbrace> \<union> {s. s \<in> UNIV} \<inter> - \<lbrace>\<acute>ksReadyQueuesL1Bitmap.[unat a] \<noteq> 0\<rbrace>} \<inter> \<lbrace>b < 0x10\<rbrace>})
 6. \<And>s s'. \<lbrakk>(s, s') \<in> rf_sr; all_invs_but_ct_idle_or_in_cur_domain' s; s' \<in> UNIV\<rbrakk> \<Longrightarrow> ((\<lambda>_. True) and ?R301) s \<and> s' \<in> UNIV proof (prove)
goal (6 subgoals):
 1. \<And>curdom l1 prio. ccorres dc xfdc (?Q503 curdom l1 prio) (?Q'503 curdom l1 prio (UCAST(8 \<rightarrow> 32) prio)) [SKIP] (do queue <- getQueue curdom prio;
runnable <- isRunnable (hd queue);
a <- assert runnable;
global.switchToThread (hd queue)
od) (\<acute>ret__unsigned_long :== CALL ready_queues_index_'proc(UCAST(8 \<rightarrow> 32) curdom,UCAST(8 \<rightarrow> 32) prio);;
(Guard ArrayBounds \<lbrace>\<acute>ret__unsigned_long < 0x1000\<rbrace> (\<acute>thread :== head_C (\<acute>ksReadyQueues.[unat \<acute>ret__unsigned_long]));;
CALL switchToThread_'proc()))
 2. \<And>curdom l1. \<lbrace>?R503 curdom l1\<rbrace> gets (lookupBitmapPriority curdom) \<lbrace>?Q503 curdom l1\<rbrace>
 3. \<And>curdom l1. guard_is_UNIV (\<lambda>rv rv'. rv' = UCAST(8 \<rightarrow> 32) rv) prio_' (?Q'503 curdom l1)
 4. \<lbrace>?R301\<rbrace> if Suc 0 < numDomains then curDomain else return 0 \<lbrace>\<lambda>curdom. K (curdom \<le> maxDomain) and (\<lambda>s. curdom \<le> maxDomain \<and> (\<forall>rv. ksReadyQueuesL1Bitmap s curdom = rv \<longrightarrow> ((\<lambda>s. rv = ksReadyQueuesL1Bitmap s curdom \<and> curdom \<le> maxDomain) and (\<lambda>s. rv \<noteq> 0 \<longrightarrow> ((\<lambda>s. curdom \<le> maxDomain \<and> ksReadyQueuesL1Bitmap s curdom \<noteq> 0 \<and> bitmapQ_no_L1_orphans s) and ?R503 curdom rv) s) and (\<lambda>s. \<not> rv \<noteq> 0 \<longrightarrow> all_invs_but_ct_idle_or_in_cur_domain' s)) s))\<rbrace>
 5. guard_is_UNIV (\<lambda>rv rv'. rv' = UCAST(8 \<rightarrow> 32) rv) dom_' (\<lambda>a b. {s'. a \<le> maxDomain \<longrightarrow> s' \<in> {s. \<forall>rv. ksReadyQueuesL1Bitmap_' (globals s).[unat a] = UCAST(32 \<rightarrow> 32) rv \<longrightarrow> s \<in> {s. dom_'_update (\<lambda>x. b) s \<in> UNIV \<inter> \<lbrace>\<acute>dom = b\<rbrace>} \<inter> \<lbrace>\<acute>ksReadyQueuesL1Bitmap.[unat a] \<noteq> 0\<rbrace> \<union> {s. s \<in> UNIV} \<inter> - \<lbrace>\<acute>ksReadyQueuesL1Bitmap.[unat a] \<noteq> 0\<rbrace>} \<inter> \<lbrace>b < 0x10\<rbrace>})
 6. \<And>s s'. \<lbrakk>(s, s') \<in> rf_sr; all_invs_but_ct_idle_or_in_cur_domain' s; s' \<in> UNIV\<rbrakk> \<Longrightarrow> ((\<lambda>_. True) and ?R301) s \<and> s' \<in> UNIV proof (prove)
goal (6 subgoals):
 1. \<And>curdom l1 prio. ccorres dc xfdc (?P'583 curdom l1 prio) (?Q585 curdom l1 prio (UCAST(8 \<rightarrow> 32) prio)) [SKIP] (do queue <- getQueue curdom prio;
runnable <- isRunnable (hd queue);
a <- assert runnable;
global.switchToThread (hd queue)
od) (\<acute>ret__unsigned_long :== CALL ready_queues_index_'proc(UCAST(8 \<rightarrow> 32) curdom,UCAST(8 \<rightarrow> 32) prio);;
(Guard ArrayBounds \<lbrace>\<acute>ret__unsigned_long < 0x1000\<rbrace> (\<acute>thread :== head_C (\<acute>ksReadyQueues.[unat \<acute>ret__unsigned_long]));;
CALL switchToThread_'proc()))
 2. \<And>curdom l1. \<lbrace>?R503 curdom l1\<rbrace> gets (lookupBitmapPriority curdom) \<lbrace>\<lambda>prio. K (curdom \<le> maxDomain) and ?P'583 curdom l1 prio\<rbrace>
 3. \<And>curdom l1. guard_is_UNIV (\<lambda>rv rv'. rv' = UCAST(8 \<rightarrow> 32) rv) prio_' (\<lambda>a b. {s'. curdom \<le> maxDomain \<longrightarrow> s' \<in> ?Q585 curdom l1 a b})
 4. \<lbrace>?R301\<rbrace> if Suc 0 < numDomains then curDomain else return 0 \<lbrace>\<lambda>curdom. K (curdom \<le> maxDomain) and (\<lambda>s. curdom \<le> maxDomain \<and> (\<forall>rv. ksReadyQueuesL1Bitmap s curdom = rv \<longrightarrow> ((\<lambda>s. rv = ksReadyQueuesL1Bitmap s curdom \<and> curdom \<le> maxDomain) and (\<lambda>s. rv \<noteq> 0 \<longrightarrow> ((\<lambda>s. curdom \<le> maxDomain \<and> ksReadyQueuesL1Bitmap s curdom \<noteq> 0 \<and> bitmapQ_no_L1_orphans s) and ?R503 curdom rv) s) and (\<lambda>s. \<not> rv \<noteq> 0 \<longrightarrow> all_invs_but_ct_idle_or_in_cur_domain' s)) s))\<rbrace>
 5. guard_is_UNIV (\<lambda>rv rv'. rv' = UCAST(8 \<rightarrow> 32) rv) dom_' (\<lambda>a b. {s'. a \<le> maxDomain \<longrightarrow> s' \<in> {s. \<forall>rv. ksReadyQueuesL1Bitmap_' (globals s).[unat a] = UCAST(32 \<rightarrow> 32) rv \<longrightarrow> s \<in> {s. dom_'_update (\<lambda>x. b) s \<in> UNIV \<inter> \<lbrace>\<acute>dom = b\<rbrace>} \<inter> \<lbrace>\<acute>ksReadyQueuesL1Bitmap.[unat a] \<noteq> 0\<rbrace> \<union> {s. s \<in> UNIV} \<inter> - \<lbrace>\<acute>ksReadyQueuesL1Bitmap.[unat a] \<noteq> 0\<rbrace>} \<inter> \<lbrace>b < 0x10\<rbrace>})
 6. \<And>s s'. \<lbrakk>(s, s') \<in> rf_sr; all_invs_but_ct_idle_or_in_cur_domain' s; s' \<in> UNIV\<rbrakk> \<Longrightarrow> ((\<lambda>_. True) and ?R301) s \<and> s' \<in> UNIV proof (prove)
goal (6 subgoals):
 1. \<And>curdom l1 prio. ccorres dc xfdc (?P'586 curdom l1 prio) (?Q588 curdom l1 prio (UCAST(8 \<rightarrow> 32) prio)) [SKIP] (do queue <- getQueue curdom prio;
runnable <- isRunnable (hd queue);
a <- assert runnable;
global.switchToThread (hd queue)
od) (\<acute>ret__unsigned_long :== CALL ready_queues_index_'proc(UCAST(8 \<rightarrow> 32) curdom,UCAST(8 \<rightarrow> 32) prio);;
(Guard ArrayBounds \<lbrace>\<acute>ret__unsigned_long < 0x1000\<rbrace> (\<acute>thread :== head_C (\<acute>ksReadyQueues.[unat \<acute>ret__unsigned_long]));;
CALL switchToThread_'proc()))
 2. \<And>curdom l1. \<lbrace>?R503 curdom l1\<rbrace> gets (lookupBitmapPriority curdom) \<lbrace>\<lambda>prio. K (curdom \<le> maxDomain) and (K (prio \<le> maxPriority) and ?P'586 curdom l1 prio)\<rbrace>
 3. \<And>curdom l1. guard_is_UNIV (\<lambda>rv rv'. rv' = UCAST(8 \<rightarrow> 32) rv) prio_' (\<lambda>a b. {s'. curdom \<le> maxDomain \<longrightarrow> s' \<in> {s'. a \<le> maxPriority \<longrightarrow> s' \<in> ?Q588 curdom l1 a b}})
 4. \<lbrace>?R301\<rbrace> if Suc 0 < numDomains then curDomain else return 0 \<lbrace>\<lambda>curdom. K (curdom \<le> maxDomain) and (\<lambda>s. curdom \<le> maxDomain \<and> (\<forall>rv. ksReadyQueuesL1Bitmap s curdom = rv \<longrightarrow> ((\<lambda>s. rv = ksReadyQueuesL1Bitmap s curdom \<and> curdom \<le> maxDomain) and (\<lambda>s. rv \<noteq> 0 \<longrightarrow> ((\<lambda>s. curdom \<le> maxDomain \<and> ksReadyQueuesL1Bitmap s curdom \<noteq> 0 \<and> bitmapQ_no_L1_orphans s) and ?R503 curdom rv) s) and (\<lambda>s. \<not> rv \<noteq> 0 \<longrightarrow> all_invs_but_ct_idle_or_in_cur_domain' s)) s))\<rbrace>
 5. guard_is_UNIV (\<lambda>rv rv'. rv' = UCAST(8 \<rightarrow> 32) rv) dom_' (\<lambda>a b. {s'. a \<le> maxDomain \<longrightarrow> s' \<in> {s. \<forall>rv. ksReadyQueuesL1Bitmap_' (globals s).[unat a] = UCAST(32 \<rightarrow> 32) rv \<longrightarrow> s \<in> {s. dom_'_update (\<lambda>x. b) s \<in> UNIV \<inter> \<lbrace>\<acute>dom = b\<rbrace>} \<inter> \<lbrace>\<acute>ksReadyQueuesL1Bitmap.[unat a] \<noteq> 0\<rbrace> \<union> {s. s \<in> UNIV} \<inter> - \<lbrace>\<acute>ksReadyQueuesL1Bitmap.[unat a] \<noteq> 0\<rbrace>} \<inter> \<lbrace>b < 0x10\<rbrace>})
 6. \<And>s s'. \<lbrakk>(s, s') \<in> rf_sr; all_invs_but_ct_idle_or_in_cur_domain' s; s' \<in> UNIV\<rbrakk> \<Longrightarrow> ((\<lambda>_. True) and ?R301) s \<and> s' \<in> UNIV proof (prove)
goal (6 subgoals):
 1. \<And>curdom l1 prio queue. ccorres dc xfdc (?P589 curdom l1 prio queue) (?P'591 curdom l1 prio (UCAST(8 \<rightarrow> 32) prio) queue) [SKIP] (do runnable <- isRunnable (hd queue);
a <- assert runnable;
global.switchToThread (hd queue)
od) (\<acute>ret__unsigned_long :== CALL ready_queues_index_'proc(UCAST(8 \<rightarrow> 32) curdom,UCAST(8 \<rightarrow> 32) prio);;
(Guard ArrayBounds \<lbrace>\<acute>ret__unsigned_long < 0x1000\<rbrace> (\<acute>thread :== head_C (\<acute>ksReadyQueues.[unat \<acute>ret__unsigned_long]));;
CALL switchToThread_'proc()))
 2. \<And>curdom l1. \<lbrace>?R503 curdom l1\<rbrace> gets (lookupBitmapPriority curdom) \<lbrace>\<lambda>prio. K (curdom \<le> maxDomain) and (K (prio \<le> maxPriority) and (\<lambda>s. ?P589 curdom l1 prio (ksReadyQueues s (curdom, prio)) s \<and> curdom \<le> maxDomain \<and> prio \<le> maxPriority))\<rbrace>
 3. \<And>curdom l1. guard_is_UNIV (\<lambda>rv rv'. rv' = UCAST(8 \<rightarrow> 32) rv) prio_' (\<lambda>a b. {s'. curdom \<le> maxDomain \<longrightarrow> s' \<in> {s'. a \<le> maxPriority \<longrightarrow> s' \<in> {s'. \<forall>queue. (let cqueue = ksReadyQueues_' (globals s').[cready_queues_index_to_C curdom a] in sched_queue_relation' (cslift s') queue (head_C cqueue) (StateRelation_C.end_C cqueue)) \<longrightarrow> s' \<in> ?P'591 curdom l1 a b queue}}})
 4. \<lbrace>?R301\<rbrace> if Suc 0 < numDomains then curDomain else return 0 \<lbrace>\<lambda>curdom. K (curdom \<le> maxDomain) and (\<lambda>s. curdom \<le> maxDomain \<and> (\<forall>rv. ksReadyQueuesL1Bitmap s curdom = rv \<longrightarrow> ((\<lambda>s. rv = ksReadyQueuesL1Bitmap s curdom \<and> curdom \<le> maxDomain) and (\<lambda>s. rv \<noteq> 0 \<longrightarrow> ((\<lambda>s. curdom \<le> maxDomain \<and> ksReadyQueuesL1Bitmap s curdom \<noteq> 0 \<and> bitmapQ_no_L1_orphans s) and ?R503 curdom rv) s) and (\<lambda>s. \<not> rv \<noteq> 0 \<longrightarrow> all_invs_but_ct_idle_or_in_cur_domain' s)) s))\<rbrace>
 5. guard_is_UNIV (\<lambda>rv rv'. rv' = UCAST(8 \<rightarrow> 32) rv) dom_' (\<lambda>a b. {s'. a \<le> maxDomain \<longrightarrow> s' \<in> {s. \<forall>rv. ksReadyQueuesL1Bitmap_' (globals s).[unat a] = UCAST(32 \<rightarrow> 32) rv \<longrightarrow> s \<in> {s. dom_'_update (\<lambda>x. b) s \<in> UNIV \<inter> \<lbrace>\<acute>dom = b\<rbrace>} \<inter> \<lbrace>\<acute>ksReadyQueuesL1Bitmap.[unat a] \<noteq> 0\<rbrace> \<union> {s. s \<in> UNIV} \<inter> - \<lbrace>\<acute>ksReadyQueuesL1Bitmap.[unat a] \<noteq> 0\<rbrace>} \<inter> \<lbrace>b < 0x10\<rbrace>})
 6. \<And>s s'. \<lbrakk>(s, s') \<in> rf_sr; all_invs_but_ct_idle_or_in_cur_domain' s; s' \<in> UNIV\<rbrakk> \<Longrightarrow> ((\<lambda>_. True) and ?R301) s \<and> s' \<in> UNIV proof (prove)
goal (6 subgoals):
 1. \<And>curdom l1 prio queue. ccorres dc xfdc (?P'593 curdom l1 prio queue) (?Q595 curdom l1 prio (UCAST(8 \<rightarrow> 32) prio) queue) [SKIP] (do runnable <- isRunnable (hd queue);
a <- assert runnable;
global.switchToThread (hd queue)
od) (\<acute>ret__unsigned_long :== CALL ready_queues_index_'proc(UCAST(8 \<rightarrow> 32) curdom,UCAST(8 \<rightarrow> 32) prio);;
(Guard ArrayBounds \<lbrace>\<acute>ret__unsigned_long < 0x1000\<rbrace> (\<acute>thread :== head_C (\<acute>ksReadyQueues.[unat \<acute>ret__unsigned_long]));;
CALL switchToThread_'proc()))
 2. \<And>curdom l1. \<lbrace>?R503 curdom l1\<rbrace> gets (lookupBitmapPriority curdom) \<lbrace>\<lambda>prio. K (curdom \<le> maxDomain) and (K (prio \<le> maxPriority) and (\<lambda>s. (K (ksReadyQueues s (curdom, prio) \<noteq> []) and ?P'593 curdom l1 prio (ksReadyQueues s (curdom, prio))) s \<and> curdom \<le> maxDomain \<and> prio \<le> maxPriority))\<rbrace>
 3. \<And>curdom l1. guard_is_UNIV (\<lambda>rv rv'. rv' = UCAST(8 \<rightarrow> 32) rv) prio_' (\<lambda>a b. {s'. curdom \<le> maxDomain \<longrightarrow> s' \<in> {s'. a \<le> maxPriority \<longrightarrow> s' \<in> {s'. \<forall>queue. (let cqueue = ksReadyQueues_' (globals s').[cready_queues_index_to_C curdom a] in sched_queue_relation' (cslift s') queue (head_C cqueue) (StateRelation_C.end_C cqueue)) \<longrightarrow> s' \<in> {s'. queue \<noteq> [] \<longrightarrow> s' \<in> ?Q595 curdom l1 a b queue}}}})
 4. \<lbrace>?R301\<rbrace> if Suc 0 < numDomains then curDomain else return 0 \<lbrace>\<lambda>curdom. K (curdom \<le> maxDomain) and (\<lambda>s. curdom \<le> maxDomain \<and> (\<forall>rv. ksReadyQueuesL1Bitmap s curdom = rv \<longrightarrow> ((\<lambda>s. rv = ksReadyQueuesL1Bitmap s curdom \<and> curdom \<le> maxDomain) and (\<lambda>s. rv \<noteq> 0 \<longrightarrow> ((\<lambda>s. curdom \<le> maxDomain \<and> ksReadyQueuesL1Bitmap s curdom \<noteq> 0 \<and> bitmapQ_no_L1_orphans s) and ?R503 curdom rv) s) and (\<lambda>s. \<not> rv \<noteq> 0 \<longrightarrow> all_invs_but_ct_idle_or_in_cur_domain' s)) s))\<rbrace>
 5. guard_is_UNIV (\<lambda>rv rv'. rv' = UCAST(8 \<rightarrow> 32) rv) dom_' (\<lambda>a b. {s'. a \<le> maxDomain \<longrightarrow> s' \<in> {s. \<forall>rv. ksReadyQueuesL1Bitmap_' (globals s).[unat a] = UCAST(32 \<rightarrow> 32) rv \<longrightarrow> s \<in> {s. dom_'_update (\<lambda>x. b) s \<in> UNIV \<inter> \<lbrace>\<acute>dom = b\<rbrace>} \<inter> \<lbrace>\<acute>ksReadyQueuesL1Bitmap.[unat a] \<noteq> 0\<rbrace> \<union> {s. s \<in> UNIV} \<inter> - \<lbrace>\<acute>ksReadyQueuesL1Bitmap.[unat a] \<noteq> 0\<rbrace>} \<inter> \<lbrace>b < 0x10\<rbrace>})
 6. \<And>s s'. \<lbrakk>(s, s') \<in> rf_sr; all_invs_but_ct_idle_or_in_cur_domain' s; s' \<in> UNIV\<rbrakk> \<Longrightarrow> ((\<lambda>_. True) and ?R301) s \<and> s' \<in> UNIV proof (prove)
goal (9 subgoals):
 1. \<And>curdom l1 prio queue rv. ccorres dc xfdc (?Q600 curdom l1 prio (UCAST(8 \<rightarrow> 32) prio) queue rv) (?Q'599 curdom l1 prio (UCAST(8 \<rightarrow> 32) prio) queue rv) [SKIP] (do a <- assert rv;
global.switchToThread (hd queue)
od) (\<acute>ret__unsigned_long :== CALL ready_queues_index_'proc(UCAST(8 \<rightarrow> 32) curdom,UCAST(8 \<rightarrow> 32) prio);;
(Guard ArrayBounds \<lbrace>\<acute>ret__unsigned_long < 0x1000\<rbrace> (\<acute>thread :== head_C (\<acute>ksReadyQueues.[unat \<acute>ret__unsigned_long]));;
CALL switchToThread_'proc()))
 2. \<And>curdom l1 prio queue s. \<lbrace>(=) s\<rbrace> isRunnable (hd queue) \<lbrace>\<lambda>r. (=) s\<rbrace>
 3. \<And>curdom l1 prio queue. \<lbrace>?P'593 curdom l1 prio queue\<rbrace> isRunnable (hd queue) \<lbrace>?Q600 curdom l1 prio (UCAST(8 \<rightarrow> 32) prio) queue\<rbrace>
 4. \<And>curdom l1 prio queue. empty_fail (isRunnable (hd queue))
 5. \<And>curdom l1. \<lbrace>?R503 curdom l1\<rbrace> gets (lookupBitmapPriority curdom) \<lbrace>\<lambda>prio. K (curdom \<le> maxDomain) and (K (prio \<le> maxPriority) and (\<lambda>s. (K (ksReadyQueues s (curdom, prio) \<noteq> []) and ?P'593 curdom l1 prio (ksReadyQueues s (curdom, prio))) s \<and> curdom \<le> maxDomain \<and> prio \<le> maxPriority))\<rbrace>
 6. \<And>curdom l1. guard_is_UNIV (\<lambda>rv rv'. rv' = UCAST(8 \<rightarrow> 32) rv) prio_' (\<lambda>a b. {s'. curdom \<le> maxDomain \<longrightarrow> s' \<in> {s'. a \<le> maxPriority \<longrightarrow> s' \<in> {s'. \<forall>queue. (let cqueue = ksReadyQueues_' (globals s').[cready_queues_index_to_C curdom a] in sched_queue_relation' (cslift s') queue (head_C cqueue) (StateRelation_C.end_C cqueue)) \<longrightarrow> s' \<in> {s'. queue \<noteq> [] \<longrightarrow> s' \<in> {s'. \<forall>rv s. (s, s') \<in> rf_sr \<and> ?Q600 curdom l1 a b queue rv s \<longrightarrow> s' \<in> ?Q'599 curdom l1 a b queue rv}}}}})
 7. \<lbrace>?R301\<rbrace> if Suc 0 < numDomains then curDomain else return 0 \<lbrace>\<lambda>curdom. K (curdom \<le> maxDomain) and (\<lambda>s. curdom \<le> maxDomain \<and> (\<forall>rv. ksReadyQueuesL1Bitmap s curdom = rv \<longrightarrow> ((\<lambda>s. rv = ksReadyQueuesL1Bitmap s curdom \<and> curdom \<le> maxDomain) and (\<lambda>s. rv \<noteq> 0 \<longrightarrow> ((\<lambda>s. curdom \<le> maxDomain \<and> ksReadyQueuesL1Bitmap s curdom \<noteq> 0 \<and> bitmapQ_no_L1_orphans s) and ?R503 curdom rv) s) and (\<lambda>s. \<not> rv \<noteq> 0 \<longrightarrow> all_invs_but_ct_idle_or_in_cur_domain' s)) s))\<rbrace>
 8. guard_is_UNIV (\<lambda>rv rv'. rv' = UCAST(8 \<rightarrow> 32) rv) dom_' (\<lambda>a b. {s'. a \<le> maxDomain \<longrightarrow> s' \<in> {s. \<forall>rv. ksReadyQueuesL1Bitmap_' (globals s).[unat a] = UCAST(32 \<rightarrow> 32) rv \<longrightarrow> s \<in> {s. dom_'_update (\<lambda>x. b) s \<in> UNIV \<inter> \<lbrace>\<acute>dom = b\<rbrace>} \<inter> \<lbrace>\<acute>ksReadyQueuesL1Bitmap.[unat a] \<noteq> 0\<rbrace> \<union> {s. s \<in> UNIV} \<inter> - \<lbrace>\<acute>ksReadyQueuesL1Bitmap.[unat a] \<noteq> 0\<rbrace>} \<inter> \<lbrace>b < 0x10\<rbrace>})
 9. \<And>s s'. \<lbrakk>(s, s') \<in> rf_sr; all_invs_but_ct_idle_or_in_cur_domain' s; s' \<in> UNIV\<rbrakk> \<Longrightarrow> ((\<lambda>_. True) and ?R301) s \<and> s' \<in> UNIV proof (prove)
goal (9 subgoals):
 1. \<And>curdom l1 prio queue rv. rv \<Longrightarrow> ccorres dc xfdc (?Q600 curdom l1 prio (UCAST(8 \<rightarrow> 32) prio) queue rv) (?Q'599 curdom l1 prio (UCAST(8 \<rightarrow> 32) prio) queue rv) [SKIP] (global.switchToThread (hd queue)) (\<acute>ret__unsigned_long :== CALL ready_queues_index_'proc(UCAST(8 \<rightarrow> 32) curdom,UCAST(8 \<rightarrow> 32) prio);;
(Guard ArrayBounds \<lbrace>\<acute>ret__unsigned_long < 0x1000\<rbrace> (\<acute>thread :== head_C (\<acute>ksReadyQueues.[unat \<acute>ret__unsigned_long]));;
CALL switchToThread_'proc()))
 2. \<And>curdom l1 prio queue s. \<lbrace>(=) s\<rbrace> isRunnable (hd queue) \<lbrace>\<lambda>r. (=) s\<rbrace>
 3. \<And>curdom l1 prio queue. \<lbrace>?P'593 curdom l1 prio queue\<rbrace> isRunnable (hd queue) \<lbrace>?Q600 curdom l1 prio (UCAST(8 \<rightarrow> 32) prio) queue\<rbrace>
 4. \<And>curdom l1 prio queue. empty_fail (isRunnable (hd queue))
 5. \<And>curdom l1. \<lbrace>?R503 curdom l1\<rbrace> gets (lookupBitmapPriority curdom) \<lbrace>\<lambda>prio. K (curdom \<le> maxDomain) and (K (prio \<le> maxPriority) and (\<lambda>s. (K (ksReadyQueues s (curdom, prio) \<noteq> []) and ?P'593 curdom l1 prio (ksReadyQueues s (curdom, prio))) s \<and> curdom \<le> maxDomain \<and> prio \<le> maxPriority))\<rbrace>
 6. \<And>curdom l1. guard_is_UNIV (\<lambda>rv rv'. rv' = UCAST(8 \<rightarrow> 32) rv) prio_' (\<lambda>a b. {s'. curdom \<le> maxDomain \<longrightarrow> s' \<in> {s'. a \<le> maxPriority \<longrightarrow> s' \<in> {s'. \<forall>queue. (let cqueue = ksReadyQueues_' (globals s').[cready_queues_index_to_C curdom a] in sched_queue_relation' (cslift s') queue (head_C cqueue) (StateRelation_C.end_C cqueue)) \<longrightarrow> s' \<in> {s'. queue \<noteq> [] \<longrightarrow> s' \<in> {s'. \<forall>rv s. (s, s') \<in> rf_sr \<and> ?Q600 curdom l1 a b queue rv s \<longrightarrow> s' \<in> ?Q'599 curdom l1 a b queue rv}}}}})
 7. \<lbrace>?R301\<rbrace> if Suc 0 < numDomains then curDomain else return 0 \<lbrace>\<lambda>curdom. K (curdom \<le> maxDomain) and (\<lambda>s. curdom \<le> maxDomain \<and> (\<forall>rv. ksReadyQueuesL1Bitmap s curdom = rv \<longrightarrow> ((\<lambda>s. rv = ksReadyQueuesL1Bitmap s curdom \<and> curdom \<le> maxDomain) and (\<lambda>s. rv \<noteq> 0 \<longrightarrow> ((\<lambda>s. curdom \<le> maxDomain \<and> ksReadyQueuesL1Bitmap s curdom \<noteq> 0 \<and> bitmapQ_no_L1_orphans s) and ?R503 curdom rv) s) and (\<lambda>s. \<not> rv \<noteq> 0 \<longrightarrow> all_invs_but_ct_idle_or_in_cur_domain' s)) s))\<rbrace>
 8. guard_is_UNIV (\<lambda>rv rv'. rv' = UCAST(8 \<rightarrow> 32) rv) dom_' (\<lambda>a b. {s'. a \<le> maxDomain \<longrightarrow> s' \<in> {s. \<forall>rv. ksReadyQueuesL1Bitmap_' (globals s).[unat a] = UCAST(32 \<rightarrow> 32) rv \<longrightarrow> s \<in> {s. dom_'_update (\<lambda>x. b) s \<in> UNIV \<inter> \<lbrace>\<acute>dom = b\<rbrace>} \<inter> \<lbrace>\<acute>ksReadyQueuesL1Bitmap.[unat a] \<noteq> 0\<rbrace> \<union> {s. s \<in> UNIV} \<inter> - \<lbrace>\<acute>ksReadyQueuesL1Bitmap.[unat a] \<noteq> 0\<rbrace>} \<inter> \<lbrace>b < 0x10\<rbrace>})
 9. \<And>s s'. \<lbrakk>(s, s') \<in> rf_sr; all_invs_but_ct_idle_or_in_cur_domain' s; s' \<in> UNIV\<rbrakk> \<Longrightarrow> ((\<lambda>_. True) and ?R301) s \<and> s' \<in> UNIV proof (prove)
goal (11 subgoals):
 1. \<And>curdom l1 prio queue rv. rv \<Longrightarrow> ccorres dc xfdc (?Q600 curdom l1 prio (UCAST(8 \<rightarrow> 32) prio) queue rv) (?Q'607 curdom l1 prio queue rv) [SKIP] (global.switchToThread (hd queue)) (Guard ArrayBounds \<lbrace>\<acute>ret__unsigned_long < 0x1000\<rbrace> (\<acute>thread :== head_C (\<acute>ksReadyQueues.[unat \<acute>ret__unsigned_long]));;
CALL switchToThread_'proc())
 2. \<And>curdom l1 prio queue rv. rv \<Longrightarrow> \<Gamma>\<turnstile> (?Q'599 curdom l1 prio (UCAST(8 \<rightarrow> 32) prio) queue rv) \<acute>ret__unsigned_long :== CALL ready_queues_index_'proc(UCAST(8 \<rightarrow> 32) curdom,UCAST(8 \<rightarrow> 32) prio) (?Q'607 curdom l1 prio queue rv)
 3. \<And>curdom l1 prio queue rv s. \<lbrakk>rv; ?Q600 curdom l1 prio (UCAST(8 \<rightarrow> 32) prio) queue rv s\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile> (?Q'599 curdom l1 prio (UCAST(8 \<rightarrow> 32) prio) queue rv \<inter> {s'. (s, s') \<in> rf_sr}) \<acute>ret__unsigned_long :== CALL ready_queues_index_'proc(UCAST(8 \<rightarrow> 32) curdom,UCAST(8 \<rightarrow> 32) prio) {s'. (s, s') \<in> rf_sr}
 4. \<And>curdom l1 prio queue s. \<lbrace>(=) s\<rbrace> isRunnable (hd queue) \<lbrace>\<lambda>r. (=) s\<rbrace>
 5. \<And>curdom l1 prio queue. \<lbrace>?P'593 curdom l1 prio queue\<rbrace> isRunnable (hd queue) \<lbrace>?Q600 curdom l1 prio (UCAST(8 \<rightarrow> 32) prio) queue\<rbrace>
 6. \<And>curdom l1 prio queue. empty_fail (isRunnable (hd queue))
 7. \<And>curdom l1. \<lbrace>?R503 curdom l1\<rbrace> gets (lookupBitmapPriority curdom) \<lbrace>\<lambda>prio. K (curdom \<le> maxDomain) and (K (prio \<le> maxPriority) and (\<lambda>s. (K (ksReadyQueues s (curdom, prio) \<noteq> []) and ?P'593 curdom l1 prio (ksReadyQueues s (curdom, prio))) s \<and> curdom \<le> maxDomain \<and> prio \<le> maxPriority))\<rbrace>
 8. \<And>curdom l1. guard_is_UNIV (\<lambda>rv rv'. rv' = UCAST(8 \<rightarrow> 32) rv) prio_' (\<lambda>a b. {s'. curdom \<le> maxDomain \<longrightarrow> s' \<in> {s'. a \<le> maxPriority \<longrightarrow> s' \<in> {s'. \<forall>queue. (let cqueue = ksReadyQueues_' (globals s').[cready_queues_index_to_C curdom a] in sched_queue_relation' (cslift s') queue (head_C cqueue) (StateRelation_C.end_C cqueue)) \<longrightarrow> s' \<in> {s'. queue \<noteq> [] \<longrightarrow> s' \<in> {s'. \<forall>rv s. (s, s') \<in> rf_sr \<and> ?Q600 curdom l1 a b queue rv s \<longrightarrow> s' \<in> ?Q'599 curdom l1 a b queue rv}}}}})
 9. \<lbrace>?R301\<rbrace> if Suc 0 < numDomains then curDomain else return 0 \<lbrace>\<lambda>curdom. K (curdom \<le> maxDomain) and (\<lambda>s. curdom \<le> maxDomain \<and> (\<forall>rv. ksReadyQueuesL1Bitmap s curdom = rv \<longrightarrow> ((\<lambda>s. rv = ksReadyQueuesL1Bitmap s curdom \<and> curdom \<le> maxDomain) and (\<lambda>s. rv \<noteq> 0 \<longrightarrow> ((\<lambda>s. curdom \<le> maxDomain \<and> ksReadyQueuesL1Bitmap s curdom \<noteq> 0 \<and> bitmapQ_no_L1_orphans s) and ?R503 curdom rv) s) and (\<lambda>s. \<not> rv \<noteq> 0 \<longrightarrow> all_invs_but_ct_idle_or_in_cur_domain' s)) s))\<rbrace>
 10. guard_is_UNIV (\<lambda>rv rv'. rv' = UCAST(8 \<rightarrow> 32) rv) dom_' (\<lambda>a b. {s'. a \<le> maxDomain \<longrightarrow> s' \<in> {s. \<forall>rv. ksReadyQueuesL1Bitmap_' (globals s).[unat a] = UCAST(32 \<rightarrow> 32) rv \<longrightarrow> s \<in> {s. dom_'_update (\<lambda>x. b) s \<in> UNIV \<inter> \<lbrace>\<acute>dom = b\<rbrace>} \<inter> \<lbrace>\<acute>ksReadyQueuesL1Bitmap.[unat a] \<noteq> 0\<rbrace> \<union> {s. s \<in> UNIV} \<inter> - \<lbrace>\<acute>ksReadyQueuesL1Bitmap.[unat a] \<noteq> 0\<rbrace>} \<inter> \<lbrace>b < 0x10\<rbrace>})
A total of 11 subgoals... proof (prove)
goal (11 subgoals):
 1. \<And>curdom l1 prio queue rv. rv \<Longrightarrow> ccorres dc xfdc (?Q600 curdom l1 prio (UCAST(8 \<rightarrow> 32) prio) queue rv) (?C'611 curdom l1 prio queue rv) [SKIP] (global.switchToThread (hd queue)) (\<acute>thread :== head_C (\<acute>ksReadyQueues.[unat \<acute>ret__unsigned_long]);;
CALL switchToThread_'proc())
 2. \<And>curdom l1 prio queue rv. rv \<Longrightarrow> \<Gamma>\<turnstile> (?Q'599 curdom l1 prio (UCAST(8 \<rightarrow> 32) prio) queue rv) \<acute>ret__unsigned_long :== CALL ready_queues_index_'proc(UCAST(8 \<rightarrow> 32) curdom,UCAST(8 \<rightarrow> 32) prio) (?C'611 curdom l1 prio queue rv \<inter> \<lbrace>\<acute>ret__unsigned_long < 0x1000\<rbrace>)
 3. \<And>curdom l1 prio queue rv s. \<lbrakk>rv; ?Q600 curdom l1 prio (UCAST(8 \<rightarrow> 32) prio) queue rv s\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile> (?Q'599 curdom l1 prio (UCAST(8 \<rightarrow> 32) prio) queue rv \<inter> {s'. (s, s') \<in> rf_sr}) \<acute>ret__unsigned_long :== CALL ready_queues_index_'proc(UCAST(8 \<rightarrow> 32) curdom,UCAST(8 \<rightarrow> 32) prio) {s'. (s, s') \<in> rf_sr}
 4. \<And>curdom l1 prio queue s. \<lbrace>(=) s\<rbrace> isRunnable (hd queue) \<lbrace>\<lambda>r. (=) s\<rbrace>
 5. \<And>curdom l1 prio queue. \<lbrace>?P'593 curdom l1 prio queue\<rbrace> isRunnable (hd queue) \<lbrace>?Q600 curdom l1 prio (UCAST(8 \<rightarrow> 32) prio) queue\<rbrace>
 6. \<And>curdom l1 prio queue. empty_fail (isRunnable (hd queue))
 7. \<And>curdom l1. \<lbrace>?R503 curdom l1\<rbrace> gets (lookupBitmapPriority curdom) \<lbrace>\<lambda>prio. K (curdom \<le> maxDomain) and (K (prio \<le> maxPriority) and (\<lambda>s. (K (ksReadyQueues s (curdom, prio) \<noteq> []) and ?P'593 curdom l1 prio (ksReadyQueues s (curdom, prio))) s \<and> curdom \<le> maxDomain \<and> prio \<le> maxPriority))\<rbrace>
 8. \<And>curdom l1. guard_is_UNIV (\<lambda>rv rv'. rv' = UCAST(8 \<rightarrow> 32) rv) prio_' (\<lambda>a b. {s'. curdom \<le> maxDomain \<longrightarrow> s' \<in> {s'. a \<le> maxPriority \<longrightarrow> s' \<in> {s'. \<forall>queue. (let cqueue = ksReadyQueues_' (globals s').[cready_queues_index_to_C curdom a] in sched_queue_relation' (cslift s') queue (head_C cqueue) (StateRelation_C.end_C cqueue)) \<longrightarrow> s' \<in> {s'. queue \<noteq> [] \<longrightarrow> s' \<in> {s'. \<forall>rv s. (s, s') \<in> rf_sr \<and> ?Q600 curdom l1 a b queue rv s \<longrightarrow> s' \<in> ?Q'599 curdom l1 a b queue rv}}}}})
 9. \<lbrace>?R301\<rbrace> if Suc 0 < numDomains then curDomain else return 0 \<lbrace>\<lambda>curdom. K (curdom \<le> maxDomain) and (\<lambda>s. curdom \<le> maxDomain \<and> (\<forall>rv. ksReadyQueuesL1Bitmap s curdom = rv \<longrightarrow> ((\<lambda>s. rv = ksReadyQueuesL1Bitmap s curdom \<and> curdom \<le> maxDomain) and (\<lambda>s. rv \<noteq> 0 \<longrightarrow> ((\<lambda>s. curdom \<le> maxDomain \<and> ksReadyQueuesL1Bitmap s curdom \<noteq> 0 \<and> bitmapQ_no_L1_orphans s) and ?R503 curdom rv) s) and (\<lambda>s. \<not> rv \<noteq> 0 \<longrightarrow> all_invs_but_ct_idle_or_in_cur_domain' s)) s))\<rbrace>
 10. guard_is_UNIV (\<lambda>rv rv'. rv' = UCAST(8 \<rightarrow> 32) rv) dom_' (\<lambda>a b. {s'. a \<le> maxDomain \<longrightarrow> s' \<in> {s. \<forall>rv. ksReadyQueuesL1Bitmap_' (globals s).[unat a] = UCAST(32 \<rightarrow> 32) rv \<longrightarrow> s \<in> {s. dom_'_update (\<lambda>x. b) s \<in> UNIV \<inter> \<lbrace>\<acute>dom = b\<rbrace>} \<inter> \<lbrace>\<acute>ksReadyQueuesL1Bitmap.[unat a] \<noteq> 0\<rbrace> \<union> {s. s \<in> UNIV} \<inter> - \<lbrace>\<acute>ksReadyQueuesL1Bitmap.[unat a] \<noteq> 0\<rbrace>} \<inter> \<lbrace>b < 0x10\<rbrace>})
A total of 11 subgoals... proof (prove)
goal (13 subgoals):
 1. \<And>curdom l1 prio queue rv. rv \<Longrightarrow> ccorres dc xfdc (?Q600 curdom l1 prio (UCAST(8 \<rightarrow> 32) prio) queue rv) (?Q'613 curdom l1 prio queue rv) [SKIP] (global.switchToThread (hd queue)) (CALL switchToThread_'proc())
 2. \<And>curdom l1 prio queue rv. rv \<Longrightarrow> \<Gamma>\<turnstile> (?C'611 curdom l1 prio queue rv) \<acute>thread :== head_C (\<acute>ksReadyQueues.[unat \<acute>ret__unsigned_long]) (?Q'613 curdom l1 prio queue rv)
 3. \<And>curdom l1 prio queue rv s. \<lbrakk>rv; ?Q600 curdom l1 prio (UCAST(8 \<rightarrow> 32) prio) queue rv s\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile> (?C'611 curdom l1 prio queue rv \<inter> {s'. (s, s') \<in> rf_sr}) \<acute>thread :== head_C (\<acute>ksReadyQueues.[unat \<acute>ret__unsigned_long]) {s'. (s, s') \<in> rf_sr}
 4. \<And>curdom l1 prio queue rv. rv \<Longrightarrow> \<Gamma>\<turnstile> (?Q'599 curdom l1 prio (UCAST(8 \<rightarrow> 32) prio) queue rv) \<acute>ret__unsigned_long :== CALL ready_queues_index_'proc(UCAST(8 \<rightarrow> 32) curdom,UCAST(8 \<rightarrow> 32) prio) (?C'611 curdom l1 prio queue rv \<inter> \<lbrace>\<acute>ret__unsigned_long < 0x1000\<rbrace>)
 5. \<And>curdom l1 prio queue rv s. \<lbrakk>rv; ?Q600 curdom l1 prio (UCAST(8 \<rightarrow> 32) prio) queue rv s\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile> (?Q'599 curdom l1 prio (UCAST(8 \<rightarrow> 32) prio) queue rv \<inter> {s'. (s, s') \<in> rf_sr}) \<acute>ret__unsigned_long :== CALL ready_queues_index_'proc(UCAST(8 \<rightarrow> 32) curdom,UCAST(8 \<rightarrow> 32) prio) {s'. (s, s') \<in> rf_sr}
 6. \<And>curdom l1 prio queue s. \<lbrace>(=) s\<rbrace> isRunnable (hd queue) \<lbrace>\<lambda>r. (=) s\<rbrace>
 7. \<And>curdom l1 prio queue. \<lbrace>?P'593 curdom l1 prio queue\<rbrace> isRunnable (hd queue) \<lbrace>?Q600 curdom l1 prio (UCAST(8 \<rightarrow> 32) prio) queue\<rbrace>
 8. \<And>curdom l1 prio queue. empty_fail (isRunnable (hd queue))
 9. \<And>curdom l1. \<lbrace>?R503 curdom l1\<rbrace> gets (lookupBitmapPriority curdom) \<lbrace>\<lambda>prio. K (curdom \<le> maxDomain) and (K (prio \<le> maxPriority) and (\<lambda>s. (K (ksReadyQueues s (curdom, prio) \<noteq> []) and ?P'593 curdom l1 prio (ksReadyQueues s (curdom, prio))) s \<and> curdom \<le> maxDomain \<and> prio \<le> maxPriority))\<rbrace>
 10. \<And>curdom l1. guard_is_UNIV (\<lambda>rv rv'. rv' = UCAST(8 \<rightarrow> 32) rv) prio_' (\<lambda>a b. {s'. curdom \<le> maxDomain \<longrightarrow> s' \<in> {s'. a \<le> maxPriority \<longrightarrow> s' \<in> {s'. \<forall>queue. (let cqueue = ksReadyQueues_' (globals s').[cready_queues_index_to_C curdom a] in sched_queue_relation' (cslift s') queue (head_C cqueue) (StateRelation_C.end_C cqueue)) \<longrightarrow> s' \<in> {s'. queue \<noteq> [] \<longrightarrow> s' \<in> {s'. \<forall>rv s. (s, s') \<in> rf_sr \<and> ?Q600 curdom l1 a b queue rv s \<longrightarrow> s' \<in> ?Q'599 curdom l1 a b queue rv}}}}})
A total of 13 subgoals... proof (prove)
goal (13 subgoals):
 1. \<And>curdom l1 prio queue rv. rv \<Longrightarrow> ccorres dc xfdc (?Q600 curdom l1 prio (UCAST(8 \<rightarrow> 32) prio) queue True) (?Q'613 curdom l1 prio queue True) [SKIP] (global.switchToThread (hd queue)) (CALL switchToThread_'proc())
 2. \<And>curdom l1 prio queue rv. rv \<Longrightarrow> \<Gamma>\<turnstile> (?C'611 curdom l1 prio queue rv) \<acute>thread :== head_C (\<acute>ksReadyQueues.[unat \<acute>ret__unsigned_long]) (?Q'613 curdom l1 prio queue rv)
 3. \<And>curdom l1 prio queue rv s. \<lbrakk>rv; ?Q600 curdom l1 prio (UCAST(8 \<rightarrow> 32) prio) queue rv s\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile> (?C'611 curdom l1 prio queue rv \<inter> {s'. (s, s') \<in> rf_sr}) \<acute>thread :== head_C (\<acute>ksReadyQueues.[unat \<acute>ret__unsigned_long]) {s'. (s, s') \<in> rf_sr}
 4. \<And>curdom l1 prio queue rv. rv \<Longrightarrow> \<Gamma>\<turnstile> (?Q'599 curdom l1 prio (UCAST(8 \<rightarrow> 32) prio) queue rv) \<acute>ret__unsigned_long :== CALL ready_queues_index_'proc(UCAST(8 \<rightarrow> 32) curdom,UCAST(8 \<rightarrow> 32) prio) (?C'611 curdom l1 prio queue rv \<inter> \<lbrace>\<acute>ret__unsigned_long < 0x1000\<rbrace>)
 5. \<And>curdom l1 prio queue rv s. \<lbrakk>rv; ?Q600 curdom l1 prio (UCAST(8 \<rightarrow> 32) prio) queue rv s\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile> (?Q'599 curdom l1 prio (UCAST(8 \<rightarrow> 32) prio) queue rv \<inter> {s'. (s, s') \<in> rf_sr}) \<acute>ret__unsigned_long :== CALL ready_queues_index_'proc(UCAST(8 \<rightarrow> 32) curdom,UCAST(8 \<rightarrow> 32) prio) {s'. (s, s') \<in> rf_sr}
 6. \<And>curdom l1 prio queue s. \<lbrace>(=) s\<rbrace> isRunnable (hd queue) \<lbrace>\<lambda>r. (=) s\<rbrace>
 7. \<And>curdom l1 prio queue. \<lbrace>?P'593 curdom l1 prio queue\<rbrace> isRunnable (hd queue) \<lbrace>?Q600 curdom l1 prio (UCAST(8 \<rightarrow> 32) prio) queue\<rbrace>
 8. \<And>curdom l1 prio queue. empty_fail (isRunnable (hd queue))
 9. \<And>curdom l1. \<lbrace>?R503 curdom l1\<rbrace> gets (lookupBitmapPriority curdom) \<lbrace>\<lambda>prio. K (curdom \<le> maxDomain) and (K (prio \<le> maxPriority) and (\<lambda>s. (K (ksReadyQueues s (curdom, prio) \<noteq> []) and ?P'593 curdom l1 prio (ksReadyQueues s (curdom, prio))) s \<and> curdom \<le> maxDomain \<and> prio \<le> maxPriority))\<rbrace>
 10. \<And>curdom l1. guard_is_UNIV (\<lambda>rv rv'. rv' = UCAST(8 \<rightarrow> 32) rv) prio_' (\<lambda>a b. {s'. curdom \<le> maxDomain \<longrightarrow> s' \<in> {s'. a \<le> maxPriority \<longrightarrow> s' \<in> {s'. \<forall>queue. (let cqueue = ksReadyQueues_' (globals s').[cready_queues_index_to_C curdom a] in sched_queue_relation' (cslift s') queue (head_C cqueue) (StateRelation_C.end_C cqueue)) \<longrightarrow> s' \<in> {s'. queue \<noteq> [] \<longrightarrow> s' \<in> {s'. \<forall>rv s. (s, s') \<in> rf_sr \<and> ?Q600 curdom l1 a b queue rv s \<longrightarrow> s' \<in> ?Q'599 curdom l1 a b queue rv}}}}})
A total of 13 subgoals... proof (prove)
goal (12 subgoals):
 1. \<And>curdom l1 prio queue rv. rv \<Longrightarrow> \<Gamma>\<turnstile> (?C'611 curdom l1 prio queue rv) \<acute>thread :== head_C (\<acute>ksReadyQueues.[unat \<acute>ret__unsigned_long]) {s. s \<in> UNIV \<inter> \<lbrace>\<acute>thread = tcb_ptr_to_ctcb_ptr (hd queue)\<rbrace>}
 2. \<And>curdom l1 prio queue rv s. \<lbrakk>rv; (all_invs_but_ct_idle_or_in_cur_domain' and obj_at' (\<lambda>x. rv) (hd queue)) s\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile> (?C'611 curdom l1 prio queue rv \<inter> {s'. (s, s') \<in> rf_sr}) \<acute>thread :== head_C (\<acute>ksReadyQueues.[unat \<acute>ret__unsigned_long]) {s'. (s, s') \<in> rf_sr}
 3. \<And>curdom l1 prio queue rv. rv \<Longrightarrow> \<Gamma>\<turnstile> (?Q'599 curdom l1 prio (UCAST(8 \<rightarrow> 32) prio) queue rv) \<acute>ret__unsigned_long :== CALL ready_queues_index_'proc(UCAST(8 \<rightarrow> 32) curdom,UCAST(8 \<rightarrow> 32) prio) (?C'611 curdom l1 prio queue rv \<inter> \<lbrace>\<acute>ret__unsigned_long < 0x1000\<rbrace>)
 4. \<And>curdom l1 prio queue rv s. \<lbrakk>rv; (all_invs_but_ct_idle_or_in_cur_domain' and obj_at' (\<lambda>x. rv) (hd queue)) s\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile> (?Q'599 curdom l1 prio (UCAST(8 \<rightarrow> 32) prio) queue rv \<inter> {s'. (s, s') \<in> rf_sr}) \<acute>ret__unsigned_long :== CALL ready_queues_index_'proc(UCAST(8 \<rightarrow> 32) curdom,UCAST(8 \<rightarrow> 32) prio) {s'. (s, s') \<in> rf_sr}
 5. \<And>curdom l1 prio queue s. \<lbrace>(=) s\<rbrace> isRunnable (hd queue) \<lbrace>\<lambda>r. (=) s\<rbrace>
 6. \<And>curdom l1 prio queue. \<lbrace>?P'593 curdom l1 prio queue\<rbrace> isRunnable (hd queue) \<lbrace>\<lambda>rv. all_invs_but_ct_idle_or_in_cur_domain' and obj_at' (\<lambda>x. rv) (hd queue)\<rbrace>
 7. \<And>curdom l1 prio queue. empty_fail (isRunnable (hd queue))
 8. \<And>curdom l1. \<lbrace>?R503 curdom l1\<rbrace> gets (lookupBitmapPriority curdom) \<lbrace>\<lambda>prio. K (curdom \<le> maxDomain) and (K (prio \<le> maxPriority) and (\<lambda>s. (K (ksReadyQueues s (curdom, prio) \<noteq> []) and ?P'593 curdom l1 prio (ksReadyQueues s (curdom, prio))) s \<and> curdom \<le> maxDomain \<and> prio \<le> maxPriority))\<rbrace>
 9. \<And>curdom l1. guard_is_UNIV (\<lambda>rv rv'. rv' = UCAST(8 \<rightarrow> 32) rv) prio_' (\<lambda>a b. {s'. curdom \<le> maxDomain \<longrightarrow> s' \<in> {s'. a \<le> maxPriority \<longrightarrow> s' \<in> {s'. \<forall>queue. (let cqueue = ksReadyQueues_' (globals s').[cready_queues_index_to_C curdom a] in sched_queue_relation' (cslift s') queue (head_C cqueue) (StateRelation_C.end_C cqueue)) \<longrightarrow> s' \<in> {s'. queue \<noteq> [] \<longrightarrow> s' \<in> {s'. \<forall>rv s. (s, s') \<in> rf_sr \<and> (all_invs_but_ct_idle_or_in_cur_domain' and obj_at' (\<lambda>x. rv) (hd queue)) s \<longrightarrow> s' \<in> ?Q'599 curdom l1 a b queue rv}}}}})
 10. \<lbrace>?R301\<rbrace> if Suc 0 < numDomains then curDomain else return 0 \<lbrace>\<lambda>curdom. K (curdom \<le> maxDomain) and (\<lambda>s. curdom \<le> maxDomain \<and> (\<forall>rv. ksReadyQueuesL1Bitmap s curdom = rv \<longrightarrow> ((\<lambda>s. rv = ksReadyQueuesL1Bitmap s curdom \<and> curdom \<le> maxDomain) and (\<lambda>s. rv \<noteq> 0 \<longrightarrow> ((\<lambda>s. curdom \<le> maxDomain \<and> ksReadyQueuesL1Bitmap s curdom \<noteq> 0 \<and> bitmapQ_no_L1_orphans s) and ?R503 curdom rv) s) and (\<lambda>s. \<not> rv \<noteq> 0 \<longrightarrow> all_invs_but_ct_idle_or_in_cur_domain' s)) s))\<rbrace>
A total of 12 subgoals... proof (prove)
goal (11 subgoals):
 1. \<And>curdom l1 prio queue rv s. \<lbrakk>rv; (all_invs_but_ct_idle_or_in_cur_domain' and obj_at' (\<lambda>x. rv) (hd queue)) s\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile> (\<lbrace>True \<and> head_C (\<acute>ksReadyQueues.[unat \<acute>ret__unsigned_long]) = tcb_ptr_to_ctcb_ptr (hd queue)\<rbrace> \<inter> {s'. (s, s') \<in> rf_sr}) \<acute>thread :== head_C (\<acute>ksReadyQueues.[unat \<acute>ret__unsigned_long]) {s'. (s, s') \<in> rf_sr}
 2. \<And>curdom l1 prio queue rv. rv \<Longrightarrow> \<Gamma>\<turnstile> (?Q'599 curdom l1 prio (UCAST(8 \<rightarrow> 32) prio) queue rv) \<acute>ret__unsigned_long :== CALL ready_queues_index_'proc(UCAST(8 \<rightarrow> 32) curdom,UCAST(8 \<rightarrow> 32) prio) (\<lbrace>True \<and> head_C (\<acute>ksReadyQueues.[unat \<acute>ret__unsigned_long]) = tcb_ptr_to_ctcb_ptr (hd queue)\<rbrace> \<inter> \<lbrace>\<acute>ret__unsigned_long < 0x1000\<rbrace>)
 3. \<And>curdom l1 prio queue rv s. \<lbrakk>rv; (all_invs_but_ct_idle_or_in_cur_domain' and obj_at' (\<lambda>x. rv) (hd queue)) s\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile> (?Q'599 curdom l1 prio (UCAST(8 \<rightarrow> 32) prio) queue rv \<inter> {s'. (s, s') \<in> rf_sr}) \<acute>ret__unsigned_long :== CALL ready_queues_index_'proc(UCAST(8 \<rightarrow> 32) curdom,UCAST(8 \<rightarrow> 32) prio) {s'. (s, s') \<in> rf_sr}
 4. \<And>curdom l1 prio queue s. \<lbrace>(=) s\<rbrace> isRunnable (hd queue) \<lbrace>\<lambda>r. (=) s\<rbrace>
 5. \<And>curdom l1 prio queue. \<lbrace>?P'593 curdom l1 prio queue\<rbrace> isRunnable (hd queue) \<lbrace>\<lambda>rv. all_invs_but_ct_idle_or_in_cur_domain' and obj_at' (\<lambda>x. rv) (hd queue)\<rbrace>
 6. \<And>curdom l1 prio queue. empty_fail (isRunnable (hd queue))
 7. \<And>curdom l1. \<lbrace>?R503 curdom l1\<rbrace> gets (lookupBitmapPriority curdom) \<lbrace>\<lambda>prio. K (curdom \<le> maxDomain) and (K (prio \<le> maxPriority) and (\<lambda>s. (K (ksReadyQueues s (curdom, prio) \<noteq> []) and ?P'593 curdom l1 prio (ksReadyQueues s (curdom, prio))) s \<and> curdom \<le> maxDomain \<and> prio \<le> maxPriority))\<rbrace>
 8. \<And>curdom l1. guard_is_UNIV (\<lambda>rv rv'. rv' = UCAST(8 \<rightarrow> 32) rv) prio_' (\<lambda>a b. {s'. curdom \<le> maxDomain \<longrightarrow> s' \<in> {s'. a \<le> maxPriority \<longrightarrow> s' \<in> {s'. \<forall>queue. (let cqueue = ksReadyQueues_' (globals s').[cready_queues_index_to_C curdom a] in sched_queue_relation' (cslift s') queue (head_C cqueue) (StateRelation_C.end_C cqueue)) \<longrightarrow> s' \<in> {s'. queue \<noteq> [] \<longrightarrow> s' \<in> {s'. \<forall>rv s. (s, s') \<in> rf_sr \<and> (all_invs_but_ct_idle_or_in_cur_domain' and obj_at' (\<lambda>x. rv) (hd queue)) s \<longrightarrow> s' \<in> ?Q'599 curdom l1 a b queue rv}}}}})
 9. \<lbrace>?R301\<rbrace> if Suc 0 < numDomains then curDomain else return 0 \<lbrace>\<lambda>curdom. K (curdom \<le> maxDomain) and (\<lambda>s. curdom \<le> maxDomain \<and> (\<forall>rv. ksReadyQueuesL1Bitmap s curdom = rv \<longrightarrow> ((\<lambda>s. rv = ksReadyQueuesL1Bitmap s curdom \<and> curdom \<le> maxDomain) and (\<lambda>s. rv \<noteq> 0 \<longrightarrow> ((\<lambda>s. curdom \<le> maxDomain \<and> ksReadyQueuesL1Bitmap s curdom \<noteq> 0 \<and> bitmapQ_no_L1_orphans s) and ?R503 curdom rv) s) and (\<lambda>s. \<not> rv \<noteq> 0 \<longrightarrow> all_invs_but_ct_idle_or_in_cur_domain' s)) s))\<rbrace>
 10. guard_is_UNIV (\<lambda>rv rv'. rv' = UCAST(8 \<rightarrow> 32) rv) dom_' (\<lambda>a b. {s'. a \<le> maxDomain \<longrightarrow> s' \<in> {s. \<forall>rv. ksReadyQueuesL1Bitmap_' (globals s).[unat a] = UCAST(32 \<rightarrow> 32) rv \<longrightarrow> s \<in> {s. dom_'_update (\<lambda>x. b) s \<in> UNIV \<inter> \<lbrace>\<acute>dom = b\<rbrace>} \<inter> \<lbrace>\<acute>ksReadyQueuesL1Bitmap.[unat a] \<noteq> 0\<rbrace> \<union> {s. s \<in> UNIV} \<inter> - \<lbrace>\<acute>ksReadyQueuesL1Bitmap.[unat a] \<noteq> 0\<rbrace>} \<inter> \<lbrace>b < 0x10\<rbrace>})
A total of 11 subgoals... proof (prove)
goal (11 subgoals):
 1. \<And>curdom l1 prio queue rv s. \<lbrakk>rv; (all_invs_but_ct_idle_or_in_cur_domain' and obj_at' (\<lambda>x. rv) (hd queue)) s\<rbrakk> \<Longrightarrow> \<lbrace>True \<and> head_C (\<acute>ksReadyQueues.[unat \<acute>ret__unsigned_long]) = tcb_ptr_to_ctcb_ptr (hd queue)\<rbrace> \<inter> {s'. (s, s') \<in> rf_sr} \<subseteq> {sa. (s, thread_'_update (\<lambda>_. head_C (ksReadyQueues_' (globals sa).[unat (ret__unsigned_long_' sa)])) sa) \<in> rf_sr}
 2. \<And>curdom l1 prio queue rv. rv \<Longrightarrow> \<Gamma>\<turnstile> (?Q'599 curdom l1 prio (UCAST(8 \<rightarrow> 32) prio) queue rv) \<acute>ret__unsigned_long :== CALL ready_queues_index_'proc(UCAST(8 \<rightarrow> 32) curdom,UCAST(8 \<rightarrow> 32) prio) (\<lbrace>True \<and> head_C (\<acute>ksReadyQueues.[unat \<acute>ret__unsigned_long]) = tcb_ptr_to_ctcb_ptr (hd queue)\<rbrace> \<inter> \<lbrace>\<acute>ret__unsigned_long < 0x1000\<rbrace>)
 3. \<And>curdom l1 prio queue rv s. \<lbrakk>rv; (all_invs_but_ct_idle_or_in_cur_domain' and obj_at' (\<lambda>x. rv) (hd queue)) s\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile> (?Q'599 curdom l1 prio (UCAST(8 \<rightarrow> 32) prio) queue rv \<inter> {s'. (s, s') \<in> rf_sr}) \<acute>ret__unsigned_long :== CALL ready_queues_index_'proc(UCAST(8 \<rightarrow> 32) curdom,UCAST(8 \<rightarrow> 32) prio) {s'. (s, s') \<in> rf_sr}
 4. \<And>curdom l1 prio queue s. \<lbrace>(=) s\<rbrace> isRunnable (hd queue) \<lbrace>\<lambda>r. (=) s\<rbrace>
 5. \<And>curdom l1 prio queue. \<lbrace>?P'593 curdom l1 prio queue\<rbrace> isRunnable (hd queue) \<lbrace>\<lambda>rv. all_invs_but_ct_idle_or_in_cur_domain' and obj_at' (\<lambda>x. rv) (hd queue)\<rbrace>
 6. \<And>curdom l1 prio queue. empty_fail (isRunnable (hd queue))
 7. \<And>curdom l1. \<lbrace>?R503 curdom l1\<rbrace> gets (lookupBitmapPriority curdom) \<lbrace>\<lambda>prio. K (curdom \<le> maxDomain) and (K (prio \<le> maxPriority) and (\<lambda>s. (K (ksReadyQueues s (curdom, prio) \<noteq> []) and ?P'593 curdom l1 prio (ksReadyQueues s (curdom, prio))) s \<and> curdom \<le> maxDomain \<and> prio \<le> maxPriority))\<rbrace>
 8. \<And>curdom l1. guard_is_UNIV (\<lambda>rv rv'. rv' = UCAST(8 \<rightarrow> 32) rv) prio_' (\<lambda>a b. {s'. curdom \<le> maxDomain \<longrightarrow> s' \<in> {s'. a \<le> maxPriority \<longrightarrow> s' \<in> {s'. \<forall>queue. (let cqueue = ksReadyQueues_' (globals s').[cready_queues_index_to_C curdom a] in sched_queue_relation' (cslift s') queue (head_C cqueue) (StateRelation_C.end_C cqueue)) \<longrightarrow> s' \<in> {s'. queue \<noteq> [] \<longrightarrow> s' \<in> {s'. \<forall>rv s. (s, s') \<in> rf_sr \<and> (all_invs_but_ct_idle_or_in_cur_domain' and obj_at' (\<lambda>x. rv) (hd queue)) s \<longrightarrow> s' \<in> ?Q'599 curdom l1 a b queue rv}}}}})
 9. \<lbrace>?R301\<rbrace> if Suc 0 < numDomains then curDomain else return 0 \<lbrace>\<lambda>curdom. K (curdom \<le> maxDomain) and (\<lambda>s. curdom \<le> maxDomain \<and> (\<forall>rv. ksReadyQueuesL1Bitmap s curdom = rv \<longrightarrow> ((\<lambda>s. rv = ksReadyQueuesL1Bitmap s curdom \<and> curdom \<le> maxDomain) and (\<lambda>s. rv \<noteq> 0 \<longrightarrow> ((\<lambda>s. curdom \<le> maxDomain \<and> ksReadyQueuesL1Bitmap s curdom \<noteq> 0 \<and> bitmapQ_no_L1_orphans s) and ?R503 curdom rv) s) and (\<lambda>s. \<not> rv \<noteq> 0 \<longrightarrow> all_invs_but_ct_idle_or_in_cur_domain' s)) s))\<rbrace>
 10. guard_is_UNIV (\<lambda>rv rv'. rv' = UCAST(8 \<rightarrow> 32) rv) dom_' (\<lambda>a b. {s'. a \<le> maxDomain \<longrightarrow> s' \<in> {s. \<forall>rv. ksReadyQueuesL1Bitmap_' (globals s).[unat a] = UCAST(32 \<rightarrow> 32) rv \<longrightarrow> s \<in> {s. dom_'_update (\<lambda>x. b) s \<in> UNIV \<inter> \<lbrace>\<acute>dom = b\<rbrace>} \<inter> \<lbrace>\<acute>ksReadyQueuesL1Bitmap.[unat a] \<noteq> 0\<rbrace> \<union> {s. s \<in> UNIV} \<inter> - \<lbrace>\<acute>ksReadyQueuesL1Bitmap.[unat a] \<noteq> 0\<rbrace>} \<inter> \<lbrace>b < 0x10\<rbrace>})
A total of 11 subgoals... proof (prove)
goal (10 subgoals):
 1. \<And>curdom l1 prio queue rv. rv \<Longrightarrow> \<Gamma>\<turnstile> (?Q'599 curdom l1 prio (UCAST(8 \<rightarrow> 32) prio) queue rv) \<acute>ret__unsigned_long :== CALL ready_queues_index_'proc(UCAST(8 \<rightarrow> 32) curdom,UCAST(8 \<rightarrow> 32) prio) (\<lbrace>True \<and> head_C (\<acute>ksReadyQueues.[unat \<acute>ret__unsigned_long]) = tcb_ptr_to_ctcb_ptr (hd queue)\<rbrace> \<inter> \<lbrace>\<acute>ret__unsigned_long < 0x1000\<rbrace>)
 2. \<And>curdom l1 prio queue rv s. \<lbrakk>rv; (all_invs_but_ct_idle_or_in_cur_domain' and obj_at' (\<lambda>x. rv) (hd queue)) s\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile> (?Q'599 curdom l1 prio (UCAST(8 \<rightarrow> 32) prio) queue rv \<inter> {s'. (s, s') \<in> rf_sr}) \<acute>ret__unsigned_long :== CALL ready_queues_index_'proc(UCAST(8 \<rightarrow> 32) curdom,UCAST(8 \<rightarrow> 32) prio) {s'. (s, s') \<in> rf_sr}
 3. \<And>curdom l1 prio queue s. \<lbrace>(=) s\<rbrace> isRunnable (hd queue) \<lbrace>\<lambda>r. (=) s\<rbrace>
 4. \<And>curdom l1 prio queue. \<lbrace>?P'593 curdom l1 prio queue\<rbrace> isRunnable (hd queue) \<lbrace>\<lambda>rv. all_invs_but_ct_idle_or_in_cur_domain' and obj_at' (\<lambda>x. rv) (hd queue)\<rbrace>
 5. \<And>curdom l1 prio queue. empty_fail (isRunnable (hd queue))
 6. \<And>curdom l1. \<lbrace>?R503 curdom l1\<rbrace> gets (lookupBitmapPriority curdom) \<lbrace>\<lambda>prio. K (curdom \<le> maxDomain) and (K (prio \<le> maxPriority) and (\<lambda>s. (K (ksReadyQueues s (curdom, prio) \<noteq> []) and ?P'593 curdom l1 prio (ksReadyQueues s (curdom, prio))) s \<and> curdom \<le> maxDomain \<and> prio \<le> maxPriority))\<rbrace>
 7. \<And>curdom l1. guard_is_UNIV (\<lambda>rv rv'. rv' = UCAST(8 \<rightarrow> 32) rv) prio_' (\<lambda>a b. {s'. curdom \<le> maxDomain \<longrightarrow> s' \<in> {s'. a \<le> maxPriority \<longrightarrow> s' \<in> {s'. \<forall>queue. (let cqueue = ksReadyQueues_' (globals s').[cready_queues_index_to_C curdom a] in sched_queue_relation' (cslift s') queue (head_C cqueue) (StateRelation_C.end_C cqueue)) \<longrightarrow> s' \<in> {s'. queue \<noteq> [] \<longrightarrow> s' \<in> {s'. \<forall>rv s. (s, s') \<in> rf_sr \<and> (all_invs_but_ct_idle_or_in_cur_domain' and obj_at' (\<lambda>x. rv) (hd queue)) s \<longrightarrow> s' \<in> ?Q'599 curdom l1 a b queue rv}}}}})
 8. \<lbrace>?R301\<rbrace> if Suc 0 < numDomains then curDomain else return 0 \<lbrace>\<lambda>curdom. K (curdom \<le> maxDomain) and (\<lambda>s. curdom \<le> maxDomain \<and> (\<forall>rv. ksReadyQueuesL1Bitmap s curdom = rv \<longrightarrow> ((\<lambda>s. rv = ksReadyQueuesL1Bitmap s curdom \<and> curdom \<le> maxDomain) and (\<lambda>s. rv \<noteq> 0 \<longrightarrow> ((\<lambda>s. curdom \<le> maxDomain \<and> ksReadyQueuesL1Bitmap s curdom \<noteq> 0 \<and> bitmapQ_no_L1_orphans s) and ?R503 curdom rv) s) and (\<lambda>s. \<not> rv \<noteq> 0 \<longrightarrow> all_invs_but_ct_idle_or_in_cur_domain' s)) s))\<rbrace>
 9. guard_is_UNIV (\<lambda>rv rv'. rv' = UCAST(8 \<rightarrow> 32) rv) dom_' (\<lambda>a b. {s'. a \<le> maxDomain \<longrightarrow> s' \<in> {s. \<forall>rv. ksReadyQueuesL1Bitmap_' (globals s).[unat a] = UCAST(32 \<rightarrow> 32) rv \<longrightarrow> s \<in> {s. dom_'_update (\<lambda>x. b) s \<in> UNIV \<inter> \<lbrace>\<acute>dom = b\<rbrace>} \<inter> \<lbrace>\<acute>ksReadyQueuesL1Bitmap.[unat a] \<noteq> 0\<rbrace> \<union> {s. s \<in> UNIV} \<inter> - \<lbrace>\<acute>ksReadyQueuesL1Bitmap.[unat a] \<noteq> 0\<rbrace>} \<inter> \<lbrace>b < 0x10\<rbrace>})
 10. \<And>s s'. \<lbrakk>(s, s') \<in> rf_sr; all_invs_but_ct_idle_or_in_cur_domain' s; s' \<in> UNIV\<rbrakk> \<Longrightarrow> ((\<lambda>_. True) and ?R301) s \<and> s' \<in> UNIV proof (prove)
goal (10 subgoals):
 1. \<And>curdom l1 prio queue rv. rv \<Longrightarrow> \<Gamma>\<turnstile> (?Q'599 curdom l1 prio (UCAST(8 \<rightarrow> 32) prio) queue True) \<acute>ret__unsigned_long :== CALL ready_queues_index_'proc(UCAST(8 \<rightarrow> 32) curdom,UCAST(8 \<rightarrow> 32) prio) (\<lbrace>head_C (\<acute>ksReadyQueues.[unat \<acute>ret__unsigned_long]) = tcb_ptr_to_ctcb_ptr (hd queue)\<rbrace> \<inter> \<lbrace>\<acute>ret__unsigned_long < 0x1000\<rbrace>)
 2. \<And>curdom l1 prio queue rv s. \<lbrakk>rv; (all_invs_but_ct_idle_or_in_cur_domain' and obj_at' (\<lambda>x. rv) (hd queue)) s\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile> (?Q'599 curdom l1 prio (UCAST(8 \<rightarrow> 32) prio) queue rv \<inter> {s'. (s, s') \<in> rf_sr}) \<acute>ret__unsigned_long :== CALL ready_queues_index_'proc(UCAST(8 \<rightarrow> 32) curdom,UCAST(8 \<rightarrow> 32) prio) {s'. (s, s') \<in> rf_sr}
 3. \<And>curdom l1 prio queue s. \<lbrace>(=) s\<rbrace> isRunnable (hd queue) \<lbrace>\<lambda>r. (=) s\<rbrace>
 4. \<And>curdom l1 prio queue. \<lbrace>?P'593 curdom l1 prio queue\<rbrace> isRunnable (hd queue) \<lbrace>\<lambda>rv. all_invs_but_ct_idle_or_in_cur_domain' and obj_at' (\<lambda>x. rv) (hd queue)\<rbrace>
 5. \<And>curdom l1 prio queue. empty_fail (isRunnable (hd queue))
 6. \<And>curdom l1. \<lbrace>?R503 curdom l1\<rbrace> gets (lookupBitmapPriority curdom) \<lbrace>\<lambda>prio. K (curdom \<le> maxDomain) and (K (prio \<le> maxPriority) and (\<lambda>s. (K (ksReadyQueues s (curdom, prio) \<noteq> []) and ?P'593 curdom l1 prio (ksReadyQueues s (curdom, prio))) s \<and> curdom \<le> maxDomain \<and> prio \<le> maxPriority))\<rbrace>
 7. \<And>curdom l1. guard_is_UNIV (\<lambda>rv rv'. rv' = UCAST(8 \<rightarrow> 32) rv) prio_' (\<lambda>a b. {s'. curdom \<le> maxDomain \<longrightarrow> s' \<in> {s'. a \<le> maxPriority \<longrightarrow> s' \<in> {s'. \<forall>queue. (let cqueue = ksReadyQueues_' (globals s').[cready_queues_index_to_C curdom a] in sched_queue_relation' (cslift s') queue (head_C cqueue) (StateRelation_C.end_C cqueue)) \<longrightarrow> s' \<in> {s'. queue \<noteq> [] \<longrightarrow> s' \<in> {s'. \<forall>rv s. (s, s') \<in> rf_sr \<and> (all_invs_but_ct_idle_or_in_cur_domain' and obj_at' (\<lambda>x. rv) (hd queue)) s \<longrightarrow> s' \<in> ?Q'599 curdom l1 a b queue rv}}}}})
 8. \<lbrace>?R301\<rbrace> if Suc 0 < numDomains then curDomain else return 0 \<lbrace>\<lambda>curdom. K (curdom \<le> maxDomain) and (\<lambda>s. curdom \<le> maxDomain \<and> (\<forall>rv. ksReadyQueuesL1Bitmap s curdom = rv \<longrightarrow> ((\<lambda>s. rv = ksReadyQueuesL1Bitmap s curdom \<and> curdom \<le> maxDomain) and (\<lambda>s. rv \<noteq> 0 \<longrightarrow> ((\<lambda>s. curdom \<le> maxDomain \<and> ksReadyQueuesL1Bitmap s curdom \<noteq> 0 \<and> bitmapQ_no_L1_orphans s) and ?R503 curdom rv) s) and (\<lambda>s. \<not> rv \<noteq> 0 \<longrightarrow> all_invs_but_ct_idle_or_in_cur_domain' s)) s))\<rbrace>
 9. guard_is_UNIV (\<lambda>rv rv'. rv' = UCAST(8 \<rightarrow> 32) rv) dom_' (\<lambda>a b. {s'. a \<le> maxDomain \<longrightarrow> s' \<in> {s. \<forall>rv. ksReadyQueuesL1Bitmap_' (globals s).[unat a] = UCAST(32 \<rightarrow> 32) rv \<longrightarrow> s \<in> {s. dom_'_update (\<lambda>x. b) s \<in> UNIV \<inter> \<lbrace>\<acute>dom = b\<rbrace>} \<inter> \<lbrace>\<acute>ksReadyQueuesL1Bitmap.[unat a] \<noteq> 0\<rbrace> \<union> {s. s \<in> UNIV} \<inter> - \<lbrace>\<acute>ksReadyQueuesL1Bitmap.[unat a] \<noteq> 0\<rbrace>} \<inter> \<lbrace>b < 0x10\<rbrace>})
 10. \<And>s s'. \<lbrakk>(s, s') \<in> rf_sr; all_invs_but_ct_idle_or_in_cur_domain' s; s' \<in> UNIV\<rbrakk> \<Longrightarrow> ((\<lambda>_. True) and ?R301) s \<and> s' \<in> UNIV proof (prove)
goal (10 subgoals):
 1. \<And>curdom l1 prio queue rv. rv \<Longrightarrow> ?Q'599 curdom l1 prio (UCAST(8 \<rightarrow> 32) prio) queue True \<subseteq> \<lbrace>(numDomains \<le> 1 \<longrightarrow> UCAST(8 \<rightarrow> 32) curdom = 0) \<and> (\<forall>t. \<^bsup>t\<^esup>ret__unsigned_long = UCAST(8 \<rightarrow> 32) curdom * 0x100 + UCAST(8 \<rightarrow> 32) prio \<longrightarrow> head_C (\<acute>ksReadyQueues.[unat (UCAST(8 \<rightarrow> 32) curdom * 0x100 + UCAST(8 \<rightarrow> 32) prio)]) = tcb_ptr_to_ctcb_ptr (hd queue) \<and> UCAST(8 \<rightarrow> 32) curdom * 0x100 + UCAST(8 \<rightarrow> 32) prio < 0x1000)\<rbrace>
 2. \<And>curdom l1 prio queue rv s. \<lbrakk>rv; (all_invs_but_ct_idle_or_in_cur_domain' and obj_at' (\<lambda>x. rv) (hd queue)) s\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile> (?Q'599 curdom l1 prio (UCAST(8 \<rightarrow> 32) prio) queue rv \<inter> {s'. (s, s') \<in> rf_sr}) \<acute>ret__unsigned_long :== CALL ready_queues_index_'proc(UCAST(8 \<rightarrow> 32) curdom,UCAST(8 \<rightarrow> 32) prio) {s'. (s, s') \<in> rf_sr}
 3. \<And>curdom l1 prio queue s. \<lbrace>(=) s\<rbrace> isRunnable (hd queue) \<lbrace>\<lambda>r. (=) s\<rbrace>
 4. \<And>curdom l1 prio queue. \<lbrace>?P'593 curdom l1 prio queue\<rbrace> isRunnable (hd queue) \<lbrace>\<lambda>rv. all_invs_but_ct_idle_or_in_cur_domain' and obj_at' (\<lambda>x. rv) (hd queue)\<rbrace>
 5. \<And>curdom l1 prio queue. empty_fail (isRunnable (hd queue))
 6. \<And>curdom l1. \<lbrace>?R503 curdom l1\<rbrace> gets (lookupBitmapPriority curdom) \<lbrace>\<lambda>prio. K (curdom \<le> maxDomain) and (K (prio \<le> maxPriority) and (\<lambda>s. (K (ksReadyQueues s (curdom, prio) \<noteq> []) and ?P'593 curdom l1 prio (ksReadyQueues s (curdom, prio))) s \<and> curdom \<le> maxDomain \<and> prio \<le> maxPriority))\<rbrace>
 7. \<And>curdom l1. guard_is_UNIV (\<lambda>rv rv'. rv' = UCAST(8 \<rightarrow> 32) rv) prio_' (\<lambda>a b. {s'. curdom \<le> maxDomain \<longrightarrow> s' \<in> {s'. a \<le> maxPriority \<longrightarrow> s' \<in> {s'. \<forall>queue. (let cqueue = ksReadyQueues_' (globals s').[cready_queues_index_to_C curdom a] in sched_queue_relation' (cslift s') queue (head_C cqueue) (StateRelation_C.end_C cqueue)) \<longrightarrow> s' \<in> {s'. queue \<noteq> [] \<longrightarrow> s' \<in> {s'. \<forall>rv s. (s, s') \<in> rf_sr \<and> (all_invs_but_ct_idle_or_in_cur_domain' and obj_at' (\<lambda>x. rv) (hd queue)) s \<longrightarrow> s' \<in> ?Q'599 curdom l1 a b queue rv}}}}})
 8. \<lbrace>?R301\<rbrace> if Suc 0 < numDomains then curDomain else return 0 \<lbrace>\<lambda>curdom. K (curdom \<le> maxDomain) and (\<lambda>s. curdom \<le> maxDomain \<and> (\<forall>rv. ksReadyQueuesL1Bitmap s curdom = rv \<longrightarrow> ((\<lambda>s. rv = ksReadyQueuesL1Bitmap s curdom \<and> curdom \<le> maxDomain) and (\<lambda>s. rv \<noteq> 0 \<longrightarrow> ((\<lambda>s. curdom \<le> maxDomain \<and> ksReadyQueuesL1Bitmap s curdom \<noteq> 0 \<and> bitmapQ_no_L1_orphans s) and ?R503 curdom rv) s) and (\<lambda>s. \<not> rv \<noteq> 0 \<longrightarrow> all_invs_but_ct_idle_or_in_cur_domain' s)) s))\<rbrace>
 9. guard_is_UNIV (\<lambda>rv rv'. rv' = UCAST(8 \<rightarrow> 32) rv) dom_' (\<lambda>a b. {s'. a \<le> maxDomain \<longrightarrow> s' \<in> {s. \<forall>rv. ksReadyQueuesL1Bitmap_' (globals s).[unat a] = UCAST(32 \<rightarrow> 32) rv \<longrightarrow> s \<in> {s. dom_'_update (\<lambda>x. b) s \<in> UNIV \<inter> \<lbrace>\<acute>dom = b\<rbrace>} \<inter> \<lbrace>\<acute>ksReadyQueuesL1Bitmap.[unat a] \<noteq> 0\<rbrace> \<union> {s. s \<in> UNIV} \<inter> - \<lbrace>\<acute>ksReadyQueuesL1Bitmap.[unat a] \<noteq> 0\<rbrace>} \<inter> \<lbrace>b < 0x10\<rbrace>})
 10. \<And>s s'. \<lbrakk>(s, s') \<in> rf_sr; all_invs_but_ct_idle_or_in_cur_domain' s; s' \<in> UNIV\<rbrakk> \<Longrightarrow> ((\<lambda>_. True) and ?R301) s \<and> s' \<in> UNIV proof (prove)
goal (10 subgoals):
 1. \<And>curdom l1 prio queue rv x. rv \<Longrightarrow> ?P662 curdom l1 prio (UCAST(8 \<rightarrow> 32) prio) queue True x \<longrightarrow> (numDomains \<le> 1 \<longrightarrow> UCAST(8 \<rightarrow> 32) curdom = 0) \<and> (\<forall>t. ret__unsigned_long_' t = UCAST(8 \<rightarrow> 32) curdom * 0x100 + UCAST(8 \<rightarrow> 32) prio \<longrightarrow> head_C (ksReadyQueues_' (globals x).[unat (UCAST(8 \<rightarrow> 32) curdom * 0x100 + UCAST(8 \<rightarrow> 32) prio)]) = tcb_ptr_to_ctcb_ptr (hd queue) \<and> UCAST(8 \<rightarrow> 32) curdom * 0x100 + UCAST(8 \<rightarrow> 32) prio < 0x1000)
 2. \<And>curdom l1 prio queue rv s. \<lbrakk>rv; (all_invs_but_ct_idle_or_in_cur_domain' and obj_at' (\<lambda>x. rv) (hd queue)) s\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile> ({a. ?P662 curdom l1 prio (UCAST(8 \<rightarrow> 32) prio) queue rv a} \<inter> {s'. (s, s') \<in> rf_sr}) \<acute>ret__unsigned_long :== CALL ready_queues_index_'proc(UCAST(8 \<rightarrow> 32) curdom,UCAST(8 \<rightarrow> 32) prio) {s'. (s, s') \<in> rf_sr}
 3. \<And>curdom l1 prio queue s. \<lbrace>(=) s\<rbrace> isRunnable (hd queue) \<lbrace>\<lambda>r. (=) s\<rbrace>
 4. \<And>curdom l1 prio queue. \<lbrace>?P'593 curdom l1 prio queue\<rbrace> isRunnable (hd queue) \<lbrace>\<lambda>rv. all_invs_but_ct_idle_or_in_cur_domain' and obj_at' (\<lambda>x. rv) (hd queue)\<rbrace>
 5. \<And>curdom l1 prio queue. empty_fail (isRunnable (hd queue))
 6. \<And>curdom l1. \<lbrace>?R503 curdom l1\<rbrace> gets (lookupBitmapPriority curdom) \<lbrace>\<lambda>prio. K (curdom \<le> maxDomain) and (K (prio \<le> maxPriority) and (\<lambda>s. (K (ksReadyQueues s (curdom, prio) \<noteq> []) and ?P'593 curdom l1 prio (ksReadyQueues s (curdom, prio))) s \<and> curdom \<le> maxDomain \<and> prio \<le> maxPriority))\<rbrace>
 7. \<And>curdom l1. guard_is_UNIV (\<lambda>rv rv'. rv' = UCAST(8 \<rightarrow> 32) rv) prio_' (\<lambda>a b. {s'. curdom \<le> maxDomain \<longrightarrow> s' \<in> {s'. a \<le> maxPriority \<longrightarrow> s' \<in> {s'. \<forall>queue. (let cqueue = ksReadyQueues_' (globals s').[cready_queues_index_to_C curdom a] in sched_queue_relation' (cslift s') queue (head_C cqueue) (StateRelation_C.end_C cqueue)) \<longrightarrow> s' \<in> {s'. queue \<noteq> [] \<longrightarrow> s' \<in> {s'. \<forall>rv s. (s, s') \<in> rf_sr \<and> (all_invs_but_ct_idle_or_in_cur_domain' and obj_at' (\<lambda>x. rv) (hd queue)) s \<longrightarrow> s' \<in> {c. ?P662 curdom l1 a b queue rv c}}}}}})
 8. \<lbrace>?R301\<rbrace> if Suc 0 < numDomains then curDomain else return 0 \<lbrace>\<lambda>curdom. K (curdom \<le> maxDomain) and (\<lambda>s. curdom \<le> maxDomain \<and> (\<forall>rv. ksReadyQueuesL1Bitmap s curdom = rv \<longrightarrow> ((\<lambda>s. rv = ksReadyQueuesL1Bitmap s curdom \<and> curdom \<le> maxDomain) and (\<lambda>s. rv \<noteq> 0 \<longrightarrow> ((\<lambda>s. curdom \<le> maxDomain \<and> ksReadyQueuesL1Bitmap s curdom \<noteq> 0 \<and> bitmapQ_no_L1_orphans s) and ?R503 curdom rv) s) and (\<lambda>s. \<not> rv \<noteq> 0 \<longrightarrow> all_invs_but_ct_idle_or_in_cur_domain' s)) s))\<rbrace>
 9. guard_is_UNIV (\<lambda>rv rv'. rv' = UCAST(8 \<rightarrow> 32) rv) dom_' (\<lambda>a b. {s'. a \<le> maxDomain \<longrightarrow> s' \<in> {s. \<forall>rv. ksReadyQueuesL1Bitmap_' (globals s).[unat a] = UCAST(32 \<rightarrow> 32) rv \<longrightarrow> s \<in> {s. dom_'_update (\<lambda>x. b) s \<in> UNIV \<inter> \<lbrace>\<acute>dom = b\<rbrace>} \<inter> \<lbrace>\<acute>ksReadyQueuesL1Bitmap.[unat a] \<noteq> 0\<rbrace> \<union> {s. s \<in> UNIV} \<inter> - \<lbrace>\<acute>ksReadyQueuesL1Bitmap.[unat a] \<noteq> 0\<rbrace>} \<inter> \<lbrace>b < 0x10\<rbrace>})
 10. \<And>s s'. \<lbrakk>(s, s') \<in> rf_sr; all_invs_but_ct_idle_or_in_cur_domain' s; s' \<in> UNIV\<rbrakk> \<Longrightarrow> ((\<lambda>_. True) and ?R301) s \<and> s' \<in> UNIV proof (prove)
goal (10 subgoals):
 1. \<And>curdom l1 prio queue rv x. \<lbrakk>rv; ?P662 curdom l1 prio (UCAST(8 \<rightarrow> 32) prio) queue True x\<rbrakk> \<Longrightarrow> (numDomains \<le> Suc 0 \<longrightarrow> UCAST(8 \<rightarrow> 32) curdom = 0) \<and> ((\<exists>t. ret__unsigned_long_' t = UCAST(8 \<rightarrow> 32) curdom * 0x100 + UCAST(8 \<rightarrow> 32) prio) \<longrightarrow> head_C (ksReadyQueues_' (globals x).[unat curdom * 256 + unat prio]) = tcb_ptr_to_ctcb_ptr (hd queue) \<and> UCAST(8 \<rightarrow> 32) curdom * 0x100 + UCAST(8 \<rightarrow> 32) prio < 0x1000)
 2. \<And>curdom l1 prio queue rv s. \<lbrakk>rv; (all_invs_but_ct_idle_or_in_cur_domain' and obj_at' (\<lambda>x. rv) (hd queue)) s\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile> ({a. ?P662 curdom l1 prio (UCAST(8 \<rightarrow> 32) prio) queue rv a} \<inter> {s'. (s, s') \<in> rf_sr}) \<acute>ret__unsigned_long :== CALL ready_queues_index_'proc(UCAST(8 \<rightarrow> 32) curdom,UCAST(8 \<rightarrow> 32) prio) {s'. (s, s') \<in> rf_sr}
 3. \<And>curdom l1 prio queue s. \<lbrace>(=) s\<rbrace> isRunnable (hd queue) \<lbrace>\<lambda>r. (=) s\<rbrace>
 4. \<And>curdom l1 prio queue. \<lbrace>?P'593 curdom l1 prio queue\<rbrace> isRunnable (hd queue) \<lbrace>\<lambda>rv. all_invs_but_ct_idle_or_in_cur_domain' and obj_at' (\<lambda>x. rv) (hd queue)\<rbrace>
 5. \<And>curdom l1 prio queue. empty_fail (isRunnable (hd queue))
 6. \<And>curdom l1. \<lbrace>?R503 curdom l1\<rbrace> gets (lookupBitmapPriority curdom) \<lbrace>\<lambda>prio. K (curdom \<le> maxDomain) and (K (prio \<le> maxPriority) and (\<lambda>s. (K (ksReadyQueues s (curdom, prio) \<noteq> []) and ?P'593 curdom l1 prio (ksReadyQueues s (curdom, prio))) s \<and> curdom \<le> maxDomain \<and> prio \<le> maxPriority))\<rbrace>
 7. \<And>curdom l1. guard_is_UNIV (\<lambda>rv rv'. rv' = UCAST(8 \<rightarrow> 32) rv) prio_' (\<lambda>a b. {s'. curdom \<le> maxDomain \<longrightarrow> s' \<in> {s'. a \<le> maxPriority \<longrightarrow> s' \<in> {s'. \<forall>queue. (let cqueue = ksReadyQueues_' (globals s').[cready_queues_index_to_C curdom a] in sched_queue_relation' (cslift s') queue (head_C cqueue) (StateRelation_C.end_C cqueue)) \<longrightarrow> s' \<in> {s'. queue \<noteq> [] \<longrightarrow> s' \<in> {s'. \<forall>rv s. (s, s') \<in> rf_sr \<and> (all_invs_but_ct_idle_or_in_cur_domain' and obj_at' (\<lambda>x. rv) (hd queue)) s \<longrightarrow> s' \<in> {c. ?P662 curdom l1 a b queue rv c}}}}}})
 8. \<lbrace>?R301\<rbrace> if Suc 0 < numDomains then curDomain else return 0 \<lbrace>\<lambda>curdom. K (curdom \<le> maxDomain) and (\<lambda>s. curdom \<le> maxDomain \<and> (\<forall>rv. ksReadyQueuesL1Bitmap s curdom = rv \<longrightarrow> ((\<lambda>s. rv = ksReadyQueuesL1Bitmap s curdom \<and> curdom \<le> maxDomain) and (\<lambda>s. rv \<noteq> 0 \<longrightarrow> ((\<lambda>s. curdom \<le> maxDomain \<and> ksReadyQueuesL1Bitmap s curdom \<noteq> 0 \<and> bitmapQ_no_L1_orphans s) and ?R503 curdom rv) s) and (\<lambda>s. \<not> rv \<noteq> 0 \<longrightarrow> all_invs_but_ct_idle_or_in_cur_domain' s)) s))\<rbrace>
 9. guard_is_UNIV (\<lambda>rv rv'. rv' = UCAST(8 \<rightarrow> 32) rv) dom_' (\<lambda>a b. {s'. a \<le> maxDomain \<longrightarrow> s' \<in> {s. \<forall>rv. ksReadyQueuesL1Bitmap_' (globals s).[unat a] = UCAST(32 \<rightarrow> 32) rv \<longrightarrow> s \<in> {s. dom_'_update (\<lambda>x. b) s \<in> UNIV \<inter> \<lbrace>\<acute>dom = b\<rbrace>} \<inter> \<lbrace>\<acute>ksReadyQueuesL1Bitmap.[unat a] \<noteq> 0\<rbrace> \<union> {s. s \<in> UNIV} \<inter> - \<lbrace>\<acute>ksReadyQueuesL1Bitmap.[unat a] \<noteq> 0\<rbrace>} \<inter> \<lbrace>b < 0x10\<rbrace>})
 10. \<And>s s'. \<lbrakk>(s, s') \<in> rf_sr; all_invs_but_ct_idle_or_in_cur_domain' s; s' \<in> UNIV\<rbrakk> \<Longrightarrow> ((\<lambda>_. True) and ?R301) s \<and> s' \<in> UNIV proof (prove)
goal (10 subgoals):
 1. \<And>curdom l1 prio queue rv x. \<lbrakk>rv; ?P662 curdom l1 prio (UCAST(8 \<rightarrow> 32) prio) queue True x\<rbrakk> \<Longrightarrow> (numDomains \<le> Suc 0 \<longrightarrow> UCAST(8 \<rightarrow> 32) curdom = 0) \<and> ((\<exists>t. ret__unsigned_long_' t = UCAST(8 \<rightarrow> 32) curdom * 0x100 + UCAST(8 \<rightarrow> 32) prio) \<longrightarrow> head_C (ksReadyQueues_' (globals x).[unat curdom * 256 + unat prio]) = tcb_ptr_to_ctcb_ptr (hd queue) \<and> curdom \<le> UCAST(32 signed \<rightarrow> 8) maxDom \<and> prio \<le> UCAST(32 signed \<rightarrow> 8) seL4_MaxPrio)
 2. \<And>curdom l1 prio queue rv s. \<lbrakk>rv; (all_invs_but_ct_idle_or_in_cur_domain' and obj_at' (\<lambda>x. rv) (hd queue)) s\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile> ({a. ?P662 curdom l1 prio (UCAST(8 \<rightarrow> 32) prio) queue rv a} \<inter> {s'. (s, s') \<in> rf_sr}) \<acute>ret__unsigned_long :== CALL ready_queues_index_'proc(UCAST(8 \<rightarrow> 32) curdom,UCAST(8 \<rightarrow> 32) prio) {s'. (s, s') \<in> rf_sr}
 3. \<And>curdom l1 prio queue s. \<lbrace>(=) s\<rbrace> isRunnable (hd queue) \<lbrace>\<lambda>r. (=) s\<rbrace>
 4. \<And>curdom l1 prio queue. \<lbrace>?P'593 curdom l1 prio queue\<rbrace> isRunnable (hd queue) \<lbrace>\<lambda>rv. all_invs_but_ct_idle_or_in_cur_domain' and obj_at' (\<lambda>x. rv) (hd queue)\<rbrace>
 5. \<And>curdom l1 prio queue. empty_fail (isRunnable (hd queue))
 6. \<And>curdom l1. \<lbrace>?R503 curdom l1\<rbrace> gets (lookupBitmapPriority curdom) \<lbrace>\<lambda>prio. K (curdom \<le> maxDomain) and (K (prio \<le> maxPriority) and (\<lambda>s. (K (ksReadyQueues s (curdom, prio) \<noteq> []) and ?P'593 curdom l1 prio (ksReadyQueues s (curdom, prio))) s \<and> curdom \<le> maxDomain \<and> prio \<le> maxPriority))\<rbrace>
 7. \<And>curdom l1. guard_is_UNIV (\<lambda>rv rv'. rv' = UCAST(8 \<rightarrow> 32) rv) prio_' (\<lambda>a b. {s'. curdom \<le> maxDomain \<longrightarrow> s' \<in> {s'. a \<le> maxPriority \<longrightarrow> s' \<in> {s'. \<forall>queue. (let cqueue = ksReadyQueues_' (globals s').[cready_queues_index_to_C curdom a] in sched_queue_relation' (cslift s') queue (head_C cqueue) (StateRelation_C.end_C cqueue)) \<longrightarrow> s' \<in> {s'. queue \<noteq> [] \<longrightarrow> s' \<in> {s'. \<forall>rv s. (s, s') \<in> rf_sr \<and> (all_invs_but_ct_idle_or_in_cur_domain' and obj_at' (\<lambda>x. rv) (hd queue)) s \<longrightarrow> s' \<in> {c. ?P662 curdom l1 a b queue rv c}}}}}})
 8. \<lbrace>?R301\<rbrace> if Suc 0 < numDomains then curDomain else return 0 \<lbrace>\<lambda>curdom. K (curdom \<le> maxDomain) and (\<lambda>s. curdom \<le> maxDomain \<and> (\<forall>rv. ksReadyQueuesL1Bitmap s curdom = rv \<longrightarrow> ((\<lambda>s. rv = ksReadyQueuesL1Bitmap s curdom \<and> curdom \<le> maxDomain) and (\<lambda>s. rv \<noteq> 0 \<longrightarrow> ((\<lambda>s. curdom \<le> maxDomain \<and> ksReadyQueuesL1Bitmap s curdom \<noteq> 0 \<and> bitmapQ_no_L1_orphans s) and ?R503 curdom rv) s) and (\<lambda>s. \<not> rv \<noteq> 0 \<longrightarrow> all_invs_but_ct_idle_or_in_cur_domain' s)) s))\<rbrace>
 9. guard_is_UNIV (\<lambda>rv rv'. rv' = UCAST(8 \<rightarrow> 32) rv) dom_' (\<lambda>a b. {s'. a \<le> maxDomain \<longrightarrow> s' \<in> {s. \<forall>rv. ksReadyQueuesL1Bitmap_' (globals s).[unat a] = UCAST(32 \<rightarrow> 32) rv \<longrightarrow> s \<in> {s. dom_'_update (\<lambda>x. b) s \<in> UNIV \<inter> \<lbrace>\<acute>dom = b\<rbrace>} \<inter> \<lbrace>\<acute>ksReadyQueuesL1Bitmap.[unat a] \<noteq> 0\<rbrace> \<union> {s. s \<in> UNIV} \<inter> - \<lbrace>\<acute>ksReadyQueuesL1Bitmap.[unat a] \<noteq> 0\<rbrace>} \<inter> \<lbrace>b < 0x10\<rbrace>})
 10. \<And>s s'. \<lbrakk>(s, s') \<in> rf_sr; all_invs_but_ct_idle_or_in_cur_domain' s; s' \<in> UNIV\<rbrakk> \<Longrightarrow> ((\<lambda>_. True) and ?R301) s \<and> s' \<in> UNIV proof (prove)
goal (9 subgoals):
 1. \<And>curdom l1 prio queue rv s. \<lbrakk>rv; (all_invs_but_ct_idle_or_in_cur_domain' and obj_at' (\<lambda>x. rv) (hd queue)) s\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile> (\<lbrace>(numDomains \<le> Suc 0 \<longrightarrow> UCAST(8 \<rightarrow> 32) curdom = 0) \<and> ((\<exists>t. \<^bsup>t\<^esup>ret__unsigned_long = UCAST(8 \<rightarrow> 32) curdom * 0x100 + UCAST(8 \<rightarrow> 32) prio) \<longrightarrow> head_C (\<acute>ksReadyQueues.[unat curdom * 256 + unat prio]) = tcb_ptr_to_ctcb_ptr (hd queue) \<and> curdom \<le> UCAST(32 signed \<rightarrow> 8) maxDom \<and> prio \<le> UCAST(32 signed \<rightarrow> 8) seL4_MaxPrio)\<rbrace> \<inter> {s'. (s, s') \<in> rf_sr}) \<acute>ret__unsigned_long :== CALL ready_queues_index_'proc(UCAST(8 \<rightarrow> 32) curdom,UCAST(8 \<rightarrow> 32) prio) {s'. (s, s') \<in> rf_sr}
 2. \<And>curdom l1 prio queue s. \<lbrace>(=) s\<rbrace> isRunnable (hd queue) \<lbrace>\<lambda>r. (=) s\<rbrace>
 3. \<And>curdom l1 prio queue. \<lbrace>?P'593 curdom l1 prio queue\<rbrace> isRunnable (hd queue) \<lbrace>\<lambda>rv. all_invs_but_ct_idle_or_in_cur_domain' and obj_at' (\<lambda>x. rv) (hd queue)\<rbrace>
 4. \<And>curdom l1 prio queue. empty_fail (isRunnable (hd queue))
 5. \<And>curdom l1. \<lbrace>?R503 curdom l1\<rbrace> gets (lookupBitmapPriority curdom) \<lbrace>\<lambda>prio. K (curdom \<le> maxDomain) and (K (prio \<le> maxPriority) and (\<lambda>s. (K (ksReadyQueues s (curdom, prio) \<noteq> []) and ?P'593 curdom l1 prio (ksReadyQueues s (curdom, prio))) s \<and> curdom \<le> maxDomain \<and> prio \<le> maxPriority))\<rbrace>
 6. \<And>curdom l1. guard_is_UNIV (\<lambda>rv rv'. rv' = UCAST(8 \<rightarrow> 32) rv) prio_' (\<lambda>a b. {s'. curdom \<le> maxDomain \<longrightarrow> s' \<in> {s'. a \<le> maxPriority \<longrightarrow> s' \<in> {s'. \<forall>queue. (let cqueue = ksReadyQueues_' (globals s').[cready_queues_index_to_C curdom a] in sched_queue_relation' (cslift s') queue (head_C cqueue) (StateRelation_C.end_C cqueue)) \<longrightarrow> s' \<in> {s'. queue \<noteq> [] \<longrightarrow> s' \<in> {s'. \<forall>rv s. (s, s') \<in> rf_sr \<and> (all_invs_but_ct_idle_or_in_cur_domain' and obj_at' (\<lambda>x. rv) (hd queue)) s \<longrightarrow> s' \<in> \<lbrace>(numDomains \<le> Suc 0 \<longrightarrow> UCAST(8 \<rightarrow> 32) curdom = 0) \<and> ((\<exists>t. \<^bsup>t\<^esup>ret__unsigned_long = UCAST(8 \<rightarrow> 32) curdom * 0x100 + b) \<longrightarrow> head_C (\<acute>ksReadyQueues.[unat curdom * 256 + unat a]) = tcb_ptr_to_ctcb_ptr (hd queue) \<and> curdom \<le> UCAST(32 signed \<rightarrow> 8) maxDom \<and> a \<le> UCAST(32 signed \<rightarrow> 8) seL4_MaxPrio)\<rbrace>}}}}})
 7. \<lbrace>?R301\<rbrace> if Suc 0 < numDomains then curDomain else return 0 \<lbrace>\<lambda>curdom. K (curdom \<le> maxDomain) and (\<lambda>s. curdom \<le> maxDomain \<and> (\<forall>rv. ksReadyQueuesL1Bitmap s curdom = rv \<longrightarrow> ((\<lambda>s. rv = ksReadyQueuesL1Bitmap s curdom \<and> curdom \<le> maxDomain) and (\<lambda>s. rv \<noteq> 0 \<longrightarrow> ((\<lambda>s. curdom \<le> maxDomain \<and> ksReadyQueuesL1Bitmap s curdom \<noteq> 0 \<and> bitmapQ_no_L1_orphans s) and ?R503 curdom rv) s) and (\<lambda>s. \<not> rv \<noteq> 0 \<longrightarrow> all_invs_but_ct_idle_or_in_cur_domain' s)) s))\<rbrace>
 8. guard_is_UNIV (\<lambda>rv rv'. rv' = UCAST(8 \<rightarrow> 32) rv) dom_' (\<lambda>a b. {s'. a \<le> maxDomain \<longrightarrow> s' \<in> {s. \<forall>rv. ksReadyQueuesL1Bitmap_' (globals s).[unat a] = UCAST(32 \<rightarrow> 32) rv \<longrightarrow> s \<in> {s. dom_'_update (\<lambda>x. b) s \<in> UNIV \<inter> \<lbrace>\<acute>dom = b\<rbrace>} \<inter> \<lbrace>\<acute>ksReadyQueuesL1Bitmap.[unat a] \<noteq> 0\<rbrace> \<union> {s. s \<in> UNIV} \<inter> - \<lbrace>\<acute>ksReadyQueuesL1Bitmap.[unat a] \<noteq> 0\<rbrace>} \<inter> \<lbrace>b < 0x10\<rbrace>})
 9. \<And>s s'. \<lbrakk>(s, s') \<in> rf_sr; all_invs_but_ct_idle_or_in_cur_domain' s; s' \<in> UNIV\<rbrakk> \<Longrightarrow> ((\<lambda>_. True) and ?R301) s \<and> s' \<in> UNIV proof (prove)
goal (9 subgoals):
 1. \<And>curdom prio queue rv s. \<lbrakk>rv; all_invs_but_ct_idle_or_in_cur_domain' s; tcb_at' (hd queue) s\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile> (\<lbrace>(numDomains \<le> Suc 0 \<longrightarrow> UCAST(8 \<rightarrow> 32) curdom = 0) \<and> ((\<exists>t. \<^bsup>t\<^esup>ret__unsigned_long = UCAST(8 \<rightarrow> 32) curdom * 0x100 + UCAST(8 \<rightarrow> 32) prio) \<longrightarrow> head_C (\<acute>ksReadyQueues.[unat curdom * 256 + unat prio]) = tcb_ptr_to_ctcb_ptr (hd queue) \<and> curdom \<le> UCAST(32 signed \<rightarrow> 8) maxDom \<and> prio \<le> UCAST(32 signed \<rightarrow> 8) seL4_MaxPrio)\<rbrace> \<inter> {s'. (s, s') \<in> rf_sr}) \<acute>ret__unsigned_long :== CALL ready_queues_index_'proc(UCAST(8 \<rightarrow> 32) curdom,UCAST(8 \<rightarrow> 32) prio) {s'. (s, s') \<in> rf_sr}
 2. \<And>curdom l1 prio queue s. \<lbrace>(=) s\<rbrace> isRunnable (hd queue) \<lbrace>\<lambda>r. (=) s\<rbrace>
 3. \<And>curdom l1 prio queue. \<lbrace>?P'593 curdom l1 prio queue\<rbrace> isRunnable (hd queue) \<lbrace>\<lambda>rv. all_invs_but_ct_idle_or_in_cur_domain' and obj_at' (\<lambda>x. rv) (hd queue)\<rbrace>
 4. \<And>curdom l1 prio queue. empty_fail (isRunnable (hd queue))
 5. \<And>curdom l1. \<lbrace>?R503 curdom l1\<rbrace> gets (lookupBitmapPriority curdom) \<lbrace>\<lambda>prio. K (curdom \<le> maxDomain) and (K (prio \<le> maxPriority) and (\<lambda>s. (K (ksReadyQueues s (curdom, prio) \<noteq> []) and ?P'593 curdom l1 prio (ksReadyQueues s (curdom, prio))) s \<and> curdom \<le> maxDomain \<and> prio \<le> maxPriority))\<rbrace>
 6. \<And>curdom l1. guard_is_UNIV (\<lambda>rv rv'. rv' = UCAST(8 \<rightarrow> 32) rv) prio_' (\<lambda>a b. {s'. curdom \<le> maxDomain \<longrightarrow> s' \<in> {s'. a \<le> maxPriority \<longrightarrow> s' \<in> {s'. \<forall>queue. (let cqueue = ksReadyQueues_' (globals s').[cready_queues_index_to_C curdom a] in sched_queue_relation' (cslift s') queue (head_C cqueue) (StateRelation_C.end_C cqueue)) \<longrightarrow> s' \<in> {s'. queue \<noteq> [] \<longrightarrow> s' \<in> {s'. \<forall>rv s. (s, s') \<in> rf_sr \<and> (all_invs_but_ct_idle_or_in_cur_domain' and obj_at' (\<lambda>x. rv) (hd queue)) s \<longrightarrow> s' \<in> \<lbrace>(numDomains \<le> Suc 0 \<longrightarrow> UCAST(8 \<rightarrow> 32) curdom = 0) \<and> ((\<exists>t. \<^bsup>t\<^esup>ret__unsigned_long = UCAST(8 \<rightarrow> 32) curdom * 0x100 + b) \<longrightarrow> head_C (\<acute>ksReadyQueues.[unat curdom * 256 + unat a]) = tcb_ptr_to_ctcb_ptr (hd queue) \<and> curdom \<le> UCAST(32 signed \<rightarrow> 8) maxDom \<and> a \<le> UCAST(32 signed \<rightarrow> 8) seL4_MaxPrio)\<rbrace>}}}}})
 7. \<lbrace>?R301\<rbrace> if Suc 0 < numDomains then curDomain else return 0 \<lbrace>\<lambda>curdom. K (curdom \<le> maxDomain) and (\<lambda>s. curdom \<le> maxDomain \<and> (\<forall>rv. ksReadyQueuesL1Bitmap s curdom = rv \<longrightarrow> ((\<lambda>s. rv = ksReadyQueuesL1Bitmap s curdom \<and> curdom \<le> maxDomain) and (\<lambda>s. rv \<noteq> 0 \<longrightarrow> ((\<lambda>s. curdom \<le> maxDomain \<and> ksReadyQueuesL1Bitmap s curdom \<noteq> 0 \<and> bitmapQ_no_L1_orphans s) and ?R503 curdom rv) s) and (\<lambda>s. \<not> rv \<noteq> 0 \<longrightarrow> all_invs_but_ct_idle_or_in_cur_domain' s)) s))\<rbrace>
 8. guard_is_UNIV (\<lambda>rv rv'. rv' = UCAST(8 \<rightarrow> 32) rv) dom_' (\<lambda>a b. {s'. a \<le> maxDomain \<longrightarrow> s' \<in> {s. \<forall>rv. ksReadyQueuesL1Bitmap_' (globals s).[unat a] = UCAST(32 \<rightarrow> 32) rv \<longrightarrow> s \<in> {s. dom_'_update (\<lambda>x. b) s \<in> UNIV \<inter> \<lbrace>\<acute>dom = b\<rbrace>} \<inter> \<lbrace>\<acute>ksReadyQueuesL1Bitmap.[unat a] \<noteq> 0\<rbrace> \<union> {s. s \<in> UNIV} \<inter> - \<lbrace>\<acute>ksReadyQueuesL1Bitmap.[unat a] \<noteq> 0\<rbrace>} \<inter> \<lbrace>b < 0x10\<rbrace>})
 9. \<And>s s'. \<lbrakk>(s, s') \<in> rf_sr; all_invs_but_ct_idle_or_in_cur_domain' s; s' \<in> UNIV\<rbrakk> \<Longrightarrow> ((\<lambda>_. True) and ?R301) s \<and> s' \<in> UNIV proof (prove)
goal (9 subgoals):
 1. \<And>curdom prio queue rv s. \<lbrakk>rv; all_invs_but_ct_idle_or_in_cur_domain' s; tcb_at' (hd queue) s\<rbrakk> \<Longrightarrow> \<lbrace>(numDomains \<le> Suc 0 \<longrightarrow> UCAST(8 \<rightarrow> 32) curdom = 0) \<and> ((\<exists>t. \<^bsup>t\<^esup>ret__unsigned_long = UCAST(8 \<rightarrow> 32) curdom * 0x100 + UCAST(8 \<rightarrow> 32) prio) \<longrightarrow> head_C (\<acute>ksReadyQueues.[unat curdom * 256 + unat prio]) = tcb_ptr_to_ctcb_ptr (hd queue) \<and> curdom \<le> UCAST(32 signed \<rightarrow> 8) maxDom \<and> prio \<le> UCAST(32 signed \<rightarrow> 8) seL4_MaxPrio)\<rbrace> \<inter> {s'. (s, s') \<in> rf_sr} \<subseteq> {sa. (numDomains \<le> 1 \<longrightarrow> UCAST(8 \<rightarrow> 32) curdom = 0) \<and> (\<forall>t. ret__unsigned_long_' t = UCAST(8 \<rightarrow> 32) curdom * 0x100 + UCAST(8 \<rightarrow> 32) prio \<longrightarrow> (s, sa\<lparr>ret__unsigned_long_' := UCAST(8 \<rightarrow> 32) curdom * 0x100 + UCAST(8 \<rightarrow> 32) prio\<rparr>) \<in> rf_sr)}
 2. \<And>curdom l1 prio queue s. \<lbrace>(=) s\<rbrace> isRunnable (hd queue) \<lbrace>\<lambda>r. (=) s\<rbrace>
 3. \<And>curdom l1 prio queue. \<lbrace>?P'593 curdom l1 prio queue\<rbrace> isRunnable (hd queue) \<lbrace>\<lambda>rv. all_invs_but_ct_idle_or_in_cur_domain' and obj_at' (\<lambda>x. rv) (hd queue)\<rbrace>
 4. \<And>curdom l1 prio queue. empty_fail (isRunnable (hd queue))
 5. \<And>curdom l1. \<lbrace>?R503 curdom l1\<rbrace> gets (lookupBitmapPriority curdom) \<lbrace>\<lambda>prio. K (curdom \<le> maxDomain) and (K (prio \<le> maxPriority) and (\<lambda>s. (K (ksReadyQueues s (curdom, prio) \<noteq> []) and ?P'593 curdom l1 prio (ksReadyQueues s (curdom, prio))) s \<and> curdom \<le> maxDomain \<and> prio \<le> maxPriority))\<rbrace>
 6. \<And>curdom l1. guard_is_UNIV (\<lambda>rv rv'. rv' = UCAST(8 \<rightarrow> 32) rv) prio_' (\<lambda>a b. {s'. curdom \<le> maxDomain \<longrightarrow> s' \<in> {s'. a \<le> maxPriority \<longrightarrow> s' \<in> {s'. \<forall>queue. (let cqueue = ksReadyQueues_' (globals s').[cready_queues_index_to_C curdom a] in sched_queue_relation' (cslift s') queue (head_C cqueue) (StateRelation_C.end_C cqueue)) \<longrightarrow> s' \<in> {s'. queue \<noteq> [] \<longrightarrow> s' \<in> {s'. \<forall>rv s. (s, s') \<in> rf_sr \<and> (all_invs_but_ct_idle_or_in_cur_domain' and obj_at' (\<lambda>x. rv) (hd queue)) s \<longrightarrow> s' \<in> \<lbrace>(numDomains \<le> Suc 0 \<longrightarrow> UCAST(8 \<rightarrow> 32) curdom = 0) \<and> ((\<exists>t. \<^bsup>t\<^esup>ret__unsigned_long = UCAST(8 \<rightarrow> 32) curdom * 0x100 + b) \<longrightarrow> head_C (\<acute>ksReadyQueues.[unat curdom * 256 + unat a]) = tcb_ptr_to_ctcb_ptr (hd queue) \<and> curdom \<le> UCAST(32 signed \<rightarrow> 8) maxDom \<and> a \<le> UCAST(32 signed \<rightarrow> 8) seL4_MaxPrio)\<rbrace>}}}}})
 7. \<lbrace>?R301\<rbrace> if Suc 0 < numDomains then curDomain else return 0 \<lbrace>\<lambda>curdom. K (curdom \<le> maxDomain) and (\<lambda>s. curdom \<le> maxDomain \<and> (\<forall>rv. ksReadyQueuesL1Bitmap s curdom = rv \<longrightarrow> ((\<lambda>s. rv = ksReadyQueuesL1Bitmap s curdom \<and> curdom \<le> maxDomain) and (\<lambda>s. rv \<noteq> 0 \<longrightarrow> ((\<lambda>s. curdom \<le> maxDomain \<and> ksReadyQueuesL1Bitmap s curdom \<noteq> 0 \<and> bitmapQ_no_L1_orphans s) and ?R503 curdom rv) s) and (\<lambda>s. \<not> rv \<noteq> 0 \<longrightarrow> all_invs_but_ct_idle_or_in_cur_domain' s)) s))\<rbrace>
 8. guard_is_UNIV (\<lambda>rv rv'. rv' = UCAST(8 \<rightarrow> 32) rv) dom_' (\<lambda>a b. {s'. a \<le> maxDomain \<longrightarrow> s' \<in> {s. \<forall>rv. ksReadyQueuesL1Bitmap_' (globals s).[unat a] = UCAST(32 \<rightarrow> 32) rv \<longrightarrow> s \<in> {s. dom_'_update (\<lambda>x. b) s \<in> UNIV \<inter> \<lbrace>\<acute>dom = b\<rbrace>} \<inter> \<lbrace>\<acute>ksReadyQueuesL1Bitmap.[unat a] \<noteq> 0\<rbrace> \<union> {s. s \<in> UNIV} \<inter> - \<lbrace>\<acute>ksReadyQueuesL1Bitmap.[unat a] \<noteq> 0\<rbrace>} \<inter> \<lbrace>b < 0x10\<rbrace>})
 9. \<And>s s'. \<lbrakk>(s, s') \<in> rf_sr; all_invs_but_ct_idle_or_in_cur_domain' s; s' \<in> UNIV\<rbrakk> \<Longrightarrow> ((\<lambda>_. True) and ?R301) s \<and> s' \<in> UNIV proof (prove)
goal (8 subgoals):
 1. \<And>curdom l1 prio queue s. \<lbrace>(=) s\<rbrace> isRunnable (hd queue) \<lbrace>\<lambda>r. (=) s\<rbrace>
 2. \<And>curdom l1 prio queue. \<lbrace>?P'593 curdom l1 prio queue\<rbrace> isRunnable (hd queue) \<lbrace>\<lambda>rv. all_invs_but_ct_idle_or_in_cur_domain' and obj_at' (\<lambda>x. rv) (hd queue)\<rbrace>
 3. \<And>curdom l1 prio queue. empty_fail (isRunnable (hd queue))
 4. \<And>curdom l1. \<lbrace>?R503 curdom l1\<rbrace> gets (lookupBitmapPriority curdom) \<lbrace>\<lambda>prio. K (curdom \<le> maxDomain) and (K (prio \<le> maxPriority) and (\<lambda>s. (K (ksReadyQueues s (curdom, prio) \<noteq> []) and ?P'593 curdom l1 prio (ksReadyQueues s (curdom, prio))) s \<and> curdom \<le> maxDomain \<and> prio \<le> maxPriority))\<rbrace>
 5. \<And>curdom l1. guard_is_UNIV (\<lambda>rv rv'. rv' = UCAST(8 \<rightarrow> 32) rv) prio_' (\<lambda>a b. {s'. curdom \<le> maxDomain \<longrightarrow> s' \<in> {s'. a \<le> maxPriority \<longrightarrow> s' \<in> {s'. \<forall>queue. (let cqueue = ksReadyQueues_' (globals s').[cready_queues_index_to_C curdom a] in sched_queue_relation' (cslift s') queue (head_C cqueue) (StateRelation_C.end_C cqueue)) \<longrightarrow> s' \<in> {s'. queue \<noteq> [] \<longrightarrow> s' \<in> {s'. \<forall>rv s. (s, s') \<in> rf_sr \<and> (all_invs_but_ct_idle_or_in_cur_domain' and obj_at' (\<lambda>x. rv) (hd queue)) s \<longrightarrow> s' \<in> \<lbrace>(numDomains \<le> Suc 0 \<longrightarrow> UCAST(8 \<rightarrow> 32) curdom = 0) \<and> ((\<exists>t. \<^bsup>t\<^esup>ret__unsigned_long = UCAST(8 \<rightarrow> 32) curdom * 0x100 + b) \<longrightarrow> head_C (\<acute>ksReadyQueues.[unat curdom * 256 + unat a]) = tcb_ptr_to_ctcb_ptr (hd queue) \<and> curdom \<le> UCAST(32 signed \<rightarrow> 8) maxDom \<and> a \<le> UCAST(32 signed \<rightarrow> 8) seL4_MaxPrio)\<rbrace>}}}}})
 6. \<lbrace>?R301\<rbrace> if Suc 0 < numDomains then curDomain else return 0 \<lbrace>\<lambda>curdom. K (curdom \<le> maxDomain) and (\<lambda>s. curdom \<le> maxDomain \<and> (\<forall>rv. ksReadyQueuesL1Bitmap s curdom = rv \<longrightarrow> ((\<lambda>s. rv = ksReadyQueuesL1Bitmap s curdom \<and> curdom \<le> maxDomain) and (\<lambda>s. rv \<noteq> 0 \<longrightarrow> ((\<lambda>s. curdom \<le> maxDomain \<and> ksReadyQueuesL1Bitmap s curdom \<noteq> 0 \<and> bitmapQ_no_L1_orphans s) and ?R503 curdom rv) s) and (\<lambda>s. \<not> rv \<noteq> 0 \<longrightarrow> all_invs_but_ct_idle_or_in_cur_domain' s)) s))\<rbrace>
 7. guard_is_UNIV (\<lambda>rv rv'. rv' = UCAST(8 \<rightarrow> 32) rv) dom_' (\<lambda>a b. {s'. a \<le> maxDomain \<longrightarrow> s' \<in> {s. \<forall>rv. ksReadyQueuesL1Bitmap_' (globals s).[unat a] = UCAST(32 \<rightarrow> 32) rv \<longrightarrow> s \<in> {s. dom_'_update (\<lambda>x. b) s \<in> UNIV \<inter> \<lbrace>\<acute>dom = b\<rbrace>} \<inter> \<lbrace>\<acute>ksReadyQueuesL1Bitmap.[unat a] \<noteq> 0\<rbrace> \<union> {s. s \<in> UNIV} \<inter> - \<lbrace>\<acute>ksReadyQueuesL1Bitmap.[unat a] \<noteq> 0\<rbrace>} \<inter> \<lbrace>b < 0x10\<rbrace>})
 8. \<And>s s'. \<lbrakk>(s, s') \<in> rf_sr; all_invs_but_ct_idle_or_in_cur_domain' s; s' \<in> UNIV\<rbrakk> \<Longrightarrow> ((\<lambda>_. True) and ?R301) s \<and> s' \<in> UNIV proof (prove)
goal (4 subgoals):
 1. \<And>curdom l1. guard_is_UNIV (\<lambda>rv rv'. rv' = UCAST(8 \<rightarrow> 32) rv) prio_' (\<lambda>a b. {s'. curdom \<le> maxDomain \<longrightarrow> s' \<in> {s'. a \<le> maxPriority \<longrightarrow> s' \<in> {s'. \<forall>queue. (let cqueue = ksReadyQueues_' (globals s').[cready_queues_index_to_C curdom a] in sched_queue_relation' (cslift s') queue (head_C cqueue) (StateRelation_C.end_C cqueue)) \<longrightarrow> s' \<in> {s'. queue \<noteq> [] \<longrightarrow> s' \<in> {s'. \<forall>rv s. (s, s') \<in> rf_sr \<and> (all_invs_but_ct_idle_or_in_cur_domain' and obj_at' (\<lambda>x. rv) (hd queue)) s \<longrightarrow> s' \<in> \<lbrace>(numDomains \<le> Suc 0 \<longrightarrow> UCAST(8 \<rightarrow> 32) curdom = 0) \<and> ((\<exists>t. \<^bsup>t\<^esup>ret__unsigned_long = UCAST(8 \<rightarrow> 32) curdom * 0x100 + b) \<longrightarrow> head_C (\<acute>ksReadyQueues.[unat curdom * 256 + unat a]) = tcb_ptr_to_ctcb_ptr (hd queue) \<and> curdom \<le> UCAST(32 signed \<rightarrow> 8) maxDom \<and> a \<le> UCAST(32 signed \<rightarrow> 8) seL4_MaxPrio)\<rbrace>}}}}})
 2. \<lbrace>?R301\<rbrace> if Suc 0 < numDomains then curDomain else return 0 \<lbrace>\<lambda>curdom. K (curdom \<le> maxDomain) and (\<lambda>s. curdom \<le> maxDomain \<and> (\<forall>rv. ksReadyQueuesL1Bitmap s curdom = rv \<longrightarrow> ((\<lambda>s. rv = ksReadyQueuesL1Bitmap s curdom \<and> curdom \<le> maxDomain) and (\<lambda>s. rv \<noteq> 0 \<longrightarrow> ((\<lambda>s. curdom \<le> maxDomain \<and> ksReadyQueuesL1Bitmap s curdom \<noteq> 0 \<and> bitmapQ_no_L1_orphans s) and (\<lambda>s. (K (curdom \<le> maxDomain) and (K (lookupBitmapPriority curdom s \<le> maxPriority) and (\<lambda>sa. (K (ksReadyQueues sa (curdom, lookupBitmapPriority curdom s) \<noteq> []) and (\<lambda>sb. (all_invs_but_ct_idle_or_in_cur_domain' and obj_at' (\<lambda>x. st_tcb_at' runnable' (hd (ksReadyQueues sa (curdom, lookupBitmapPriority curdom s))) sb) (hd (ksReadyQueues sa (curdom, lookupBitmapPriority curdom s)))) sb)) sa \<and> curdom \<le> maxDomain \<and> lookupBitmapPriority curdom s \<le> maxPriority))) s)) s) and (\<lambda>s. \<not> rv \<noteq> 0 \<longrightarrow> all_invs_but_ct_idle_or_in_cur_domain' s)) s))\<rbrace>
 3. guard_is_UNIV (\<lambda>rv rv'. rv' = UCAST(8 \<rightarrow> 32) rv) dom_' (\<lambda>a b. {s'. a \<le> maxDomain \<longrightarrow> s' \<in> {s. \<forall>rv. ksReadyQueuesL1Bitmap_' (globals s).[unat a] = UCAST(32 \<rightarrow> 32) rv \<longrightarrow> s \<in> {s. dom_'_update (\<lambda>x. b) s \<in> UNIV \<inter> \<lbrace>\<acute>dom = b\<rbrace>} \<inter> \<lbrace>\<acute>ksReadyQueuesL1Bitmap.[unat a] \<noteq> 0\<rbrace> \<union> {s. s \<in> UNIV} \<inter> - \<lbrace>\<acute>ksReadyQueuesL1Bitmap.[unat a] \<noteq> 0\<rbrace>} \<inter> \<lbrace>b < 0x10\<rbrace>})
 4. \<And>s s'. \<lbrakk>(s, s') \<in> rf_sr; all_invs_but_ct_idle_or_in_cur_domain' s; s' \<in> UNIV\<rbrakk> \<Longrightarrow> ((\<lambda>_. True) and ?R301) s \<and> s' \<in> UNIV proof (prove)
goal (4 subgoals):
 1. \<And>curdom s rv queue rva sa. \<lbrakk>prio_' s = UCAST(8 \<rightarrow> 32) rv; curdom \<le> maxDomain; rv \<le> maxPriority; sched_queue_relation' (cslift s) queue (head_C (ksReadyQueues_' (globals s).[cready_queues_index_to_C curdom rv])) (StateRelation_C.end_C (ksReadyQueues_' (globals s).[cready_queues_index_to_C curdom rv])); queue \<noteq> []; (sa, s) \<in> rf_sr; all_invs_but_ct_idle_or_in_cur_domain' sa; obj_at' (\<lambda>x. rva) (hd queue) sa\<rbrakk> \<Longrightarrow> (numDomains \<le> Suc 0 \<longrightarrow> UCAST(8 \<rightarrow> 32) curdom = 0) \<and> ((\<exists>t. ret__unsigned_long_' t = UCAST(8 \<rightarrow> 32) curdom * 0x100 + UCAST(8 \<rightarrow> 32) rv) \<longrightarrow> head_C (ksReadyQueues_' (globals s).[unat curdom * 256 + unat rv]) = tcb_ptr_to_ctcb_ptr (hd queue) \<and> curdom \<le> UCAST(32 signed \<rightarrow> 8) maxDom \<and> rv \<le> UCAST(32 signed \<rightarrow> 8) seL4_MaxPrio)
 2. \<lbrace>?R301\<rbrace> if Suc 0 < numDomains then curDomain else return 0 \<lbrace>\<lambda>curdom. K (curdom \<le> maxDomain) and (\<lambda>s. curdom \<le> maxDomain \<and> (\<forall>rv. ksReadyQueuesL1Bitmap s curdom = rv \<longrightarrow> ((\<lambda>s. rv = ksReadyQueuesL1Bitmap s curdom \<and> curdom \<le> maxDomain) and (\<lambda>s. rv \<noteq> 0 \<longrightarrow> ((\<lambda>s. curdom \<le> maxDomain \<and> ksReadyQueuesL1Bitmap s curdom \<noteq> 0 \<and> bitmapQ_no_L1_orphans s) and (\<lambda>s. (K (curdom \<le> maxDomain) and (K (lookupBitmapPriority curdom s \<le> maxPriority) and (\<lambda>sa. (K (ksReadyQueues sa (curdom, lookupBitmapPriority curdom s) \<noteq> []) and (\<lambda>sb. (all_invs_but_ct_idle_or_in_cur_domain' and obj_at' (\<lambda>x. st_tcb_at' runnable' (hd (ksReadyQueues sa (curdom, lookupBitmapPriority curdom s))) sb) (hd (ksReadyQueues sa (curdom, lookupBitmapPriority curdom s)))) sb)) sa \<and> curdom \<le> maxDomain \<and> lookupBitmapPriority curdom s \<le> maxPriority))) s)) s) and (\<lambda>s. \<not> rv \<noteq> 0 \<longrightarrow> all_invs_but_ct_idle_or_in_cur_domain' s)) s))\<rbrace>
 3. guard_is_UNIV (\<lambda>rv rv'. rv' = UCAST(8 \<rightarrow> 32) rv) dom_' (\<lambda>a b. {s'. a \<le> maxDomain \<longrightarrow> s' \<in> {s. \<forall>rv. ksReadyQueuesL1Bitmap_' (globals s).[unat a] = UCAST(32 \<rightarrow> 32) rv \<longrightarrow> s \<in> {s. dom_'_update (\<lambda>x. b) s \<in> UNIV \<inter> \<lbrace>\<acute>dom = b\<rbrace>} \<inter> \<lbrace>\<acute>ksReadyQueuesL1Bitmap.[unat a] \<noteq> 0\<rbrace> \<union> {s. s \<in> UNIV} \<inter> - \<lbrace>\<acute>ksReadyQueuesL1Bitmap.[unat a] \<noteq> 0\<rbrace>} \<inter> \<lbrace>b < 0x10\<rbrace>})
 4. \<And>s s'. \<lbrakk>(s, s') \<in> rf_sr; all_invs_but_ct_idle_or_in_cur_domain' s; s' \<in> UNIV\<rbrakk> \<Longrightarrow> ((\<lambda>_. True) and ?R301) s \<and> s' \<in> UNIV proof (prove)
goal (4 subgoals):
 1. \<And>curdom s rv queue rva sa. \<lbrakk>prio_' s = UCAST(8 \<rightarrow> 32) rv; curdom \<le> maxDomain; rv \<le> maxPriority; sched_queue_relation' (cslift s) queue (head_C (ksReadyQueues_' (globals s).[cready_queues_index_to_C curdom rv])) (StateRelation_C.end_C (ksReadyQueues_' (globals s).[cready_queues_index_to_C curdom rv])); queue \<noteq> []; (sa, s) \<in> rf_sr; obj_at' (\<lambda>x. rva) (hd queue) sa; Invariants_H.valid_queues sa\<rbrakk> \<Longrightarrow> (numDomains \<le> Suc 0 \<longrightarrow> UCAST(8 \<rightarrow> 32) curdom = 0) \<and> ((\<exists>t. ret__unsigned_long_' t = UCAST(8 \<rightarrow> 32) curdom * 0x100 + UCAST(8 \<rightarrow> 32) rv) \<longrightarrow> head_C (ksReadyQueues_' (globals s).[unat curdom * 256 + unat rv]) = tcb_ptr_to_ctcb_ptr (hd queue) \<and> curdom \<le> UCAST(32 signed \<rightarrow> 8) maxDom \<and> rv \<le> UCAST(32 signed \<rightarrow> 8) seL4_MaxPrio)
 2. \<lbrace>?R301\<rbrace> if Suc 0 < numDomains then curDomain else return 0 \<lbrace>\<lambda>curdom. K (curdom \<le> maxDomain) and (\<lambda>s. curdom \<le> maxDomain \<and> (\<forall>rv. ksReadyQueuesL1Bitmap s curdom = rv \<longrightarrow> ((\<lambda>s. rv = ksReadyQueuesL1Bitmap s curdom \<and> curdom \<le> maxDomain) and (\<lambda>s. rv \<noteq> 0 \<longrightarrow> ((\<lambda>s. curdom \<le> maxDomain \<and> ksReadyQueuesL1Bitmap s curdom \<noteq> 0 \<and> bitmapQ_no_L1_orphans s) and (\<lambda>s. (K (curdom \<le> maxDomain) and (K (lookupBitmapPriority curdom s \<le> maxPriority) and (\<lambda>sa. (K (ksReadyQueues sa (curdom, lookupBitmapPriority curdom s) \<noteq> []) and (\<lambda>sb. (all_invs_but_ct_idle_or_in_cur_domain' and obj_at' (\<lambda>x. st_tcb_at' runnable' (hd (ksReadyQueues sa (curdom, lookupBitmapPriority curdom s))) sb) (hd (ksReadyQueues sa (curdom, lookupBitmapPriority curdom s)))) sb)) sa \<and> curdom \<le> maxDomain \<and> lookupBitmapPriority curdom s \<le> maxPriority))) s)) s) and (\<lambda>s. \<not> rv \<noteq> 0 \<longrightarrow> all_invs_but_ct_idle_or_in_cur_domain' s)) s))\<rbrace>
 3. guard_is_UNIV (\<lambda>rv rv'. rv' = UCAST(8 \<rightarrow> 32) rv) dom_' (\<lambda>a b. {s'. a \<le> maxDomain \<longrightarrow> s' \<in> {s. \<forall>rv. ksReadyQueuesL1Bitmap_' (globals s).[unat a] = UCAST(32 \<rightarrow> 32) rv \<longrightarrow> s \<in> {s. dom_'_update (\<lambda>x. b) s \<in> UNIV \<inter> \<lbrace>\<acute>dom = b\<rbrace>} \<inter> \<lbrace>\<acute>ksReadyQueuesL1Bitmap.[unat a] \<noteq> 0\<rbrace> \<union> {s. s \<in> UNIV} \<inter> - \<lbrace>\<acute>ksReadyQueuesL1Bitmap.[unat a] \<noteq> 0\<rbrace>} \<inter> \<lbrace>b < 0x10\<rbrace>})
 4. \<And>s s'. \<lbrakk>(s, s') \<in> rf_sr; all_invs_but_ct_idle_or_in_cur_domain' s; s' \<in> UNIV\<rbrakk> \<Longrightarrow> ((\<lambda>_. True) and ?R301) s \<and> s' \<in> UNIV proof (prove)
goal (4 subgoals):
 1. \<And>curdom s rv queue rva sa a list. \<lbrakk>prio_' s = UCAST(8 \<rightarrow> 32) rv; curdom \<le> maxDomain; rv \<le> maxPriority; sched_queue_relation' (cslift s) queue (head_C (ksReadyQueues_' (globals s).[cready_queues_index_to_C curdom rv])) (StateRelation_C.end_C (ksReadyQueues_' (globals s).[cready_queues_index_to_C curdom rv])); queue \<noteq> []; (sa, s) \<in> rf_sr; obj_at' (\<lambda>x. rva) (hd queue) sa; Invariants_H.valid_queues sa; queue = a # list\<rbrakk> \<Longrightarrow> (numDomains \<le> Suc 0 \<longrightarrow> UCAST(8 \<rightarrow> 32) curdom = 0) \<and> ((\<exists>t. ret__unsigned_long_' t = UCAST(8 \<rightarrow> 32) curdom * 0x100 + UCAST(8 \<rightarrow> 32) rv) \<longrightarrow> head_C (ksReadyQueues_' (globals s).[unat curdom * 256 + unat rv]) = tcb_ptr_to_ctcb_ptr (hd queue) \<and> curdom \<le> UCAST(32 signed \<rightarrow> 8) maxDom \<and> rv \<le> UCAST(32 signed \<rightarrow> 8) seL4_MaxPrio)
 2. \<lbrace>?R301\<rbrace> if Suc 0 < numDomains then curDomain else return 0 \<lbrace>\<lambda>curdom. K (curdom \<le> maxDomain) and (\<lambda>s. curdom \<le> maxDomain \<and> (\<forall>rv. ksReadyQueuesL1Bitmap s curdom = rv \<longrightarrow> ((\<lambda>s. rv = ksReadyQueuesL1Bitmap s curdom \<and> curdom \<le> maxDomain) and (\<lambda>s. rv \<noteq> 0 \<longrightarrow> ((\<lambda>s. curdom \<le> maxDomain \<and> ksReadyQueuesL1Bitmap s curdom \<noteq> 0 \<and> bitmapQ_no_L1_orphans s) and (\<lambda>s. (K (curdom \<le> maxDomain) and (K (lookupBitmapPriority curdom s \<le> maxPriority) and (\<lambda>sa. (K (ksReadyQueues sa (curdom, lookupBitmapPriority curdom s) \<noteq> []) and (\<lambda>sb. (all_invs_but_ct_idle_or_in_cur_domain' and obj_at' (\<lambda>x. st_tcb_at' runnable' (hd (ksReadyQueues sa (curdom, lookupBitmapPriority curdom s))) sb) (hd (ksReadyQueues sa (curdom, lookupBitmapPriority curdom s)))) sb)) sa \<and> curdom \<le> maxDomain \<and> lookupBitmapPriority curdom s \<le> maxPriority))) s)) s) and (\<lambda>s. \<not> rv \<noteq> 0 \<longrightarrow> all_invs_but_ct_idle_or_in_cur_domain' s)) s))\<rbrace>
 3. guard_is_UNIV (\<lambda>rv rv'. rv' = UCAST(8 \<rightarrow> 32) rv) dom_' (\<lambda>a b. {s'. a \<le> maxDomain \<longrightarrow> s' \<in> {s. \<forall>rv. ksReadyQueuesL1Bitmap_' (globals s).[unat a] = UCAST(32 \<rightarrow> 32) rv \<longrightarrow> s \<in> {s. dom_'_update (\<lambda>x. b) s \<in> UNIV \<inter> \<lbrace>\<acute>dom = b\<rbrace>} \<inter> \<lbrace>\<acute>ksReadyQueuesL1Bitmap.[unat a] \<noteq> 0\<rbrace> \<union> {s. s \<in> UNIV} \<inter> - \<lbrace>\<acute>ksReadyQueuesL1Bitmap.[unat a] \<noteq> 0\<rbrace>} \<inter> \<lbrace>b < 0x10\<rbrace>})
 4. \<And>s s'. \<lbrakk>(s, s') \<in> rf_sr; all_invs_but_ct_idle_or_in_cur_domain' s; s' \<in> UNIV\<rbrakk> \<Longrightarrow> ((\<lambda>_. True) and ?R301) s \<and> s' \<in> UNIV proof (prove)
goal (4 subgoals):
 1. \<And>curdom s rv rva sa a list tcb. \<lbrakk>prio_' s = UCAST(8 \<rightarrow> 32) rv; curdom \<le> maxDomain; rv \<le> maxPriority; (sa, s) \<in> rf_sr; obj_at' (\<lambda>x. rva) a sa; Invariants_H.valid_queues sa; StateRelation_C.end_C (ksReadyQueues_' (globals s).[unat curdom * 256 + unat rv]) = tcb_ptr_to_ctcb_ptr (if list = [] then a else last list); head_C (ksReadyQueues_' (globals s).[unat curdom * 256 + unat rv]) = tcb_ptr_to_ctcb_ptr a; cslift s (tcb_ptr_to_ctcb_ptr a) = Some tcb; tcbSchedPrev_C tcb = NULL; sched_queue_relation (cslift s) list (tcb_ptr_to_ctcb_ptr a) (tcbSchedNext_C tcb)\<rbrakk> \<Longrightarrow> (numDomains \<le> Suc 0 \<longrightarrow> UCAST(8 \<rightarrow> 32) curdom = 0) \<and> ((\<exists>t. ret__unsigned_long_' t = UCAST(8 \<rightarrow> 32) curdom * 0x100 + UCAST(8 \<rightarrow> 32) rv) \<longrightarrow> curdom \<le> UCAST(32 signed \<rightarrow> 8) maxDom \<and> rv \<le> UCAST(32 signed \<rightarrow> 8) seL4_MaxPrio)
 2. \<lbrace>?R301\<rbrace> if Suc 0 < numDomains then curDomain else return 0 \<lbrace>\<lambda>curdom. K (curdom \<le> maxDomain) and (\<lambda>s. curdom \<le> maxDomain \<and> (\<forall>rv. ksReadyQueuesL1Bitmap s curdom = rv \<longrightarrow> ((\<lambda>s. rv = ksReadyQueuesL1Bitmap s curdom \<and> curdom \<le> maxDomain) and (\<lambda>s. rv \<noteq> 0 \<longrightarrow> ((\<lambda>s. curdom \<le> maxDomain \<and> ksReadyQueuesL1Bitmap s curdom \<noteq> 0 \<and> bitmapQ_no_L1_orphans s) and (\<lambda>s. (K (curdom \<le> maxDomain) and (K (lookupBitmapPriority curdom s \<le> maxPriority) and (\<lambda>sa. (K (ksReadyQueues sa (curdom, lookupBitmapPriority curdom s) \<noteq> []) and (\<lambda>sb. (all_invs_but_ct_idle_or_in_cur_domain' and obj_at' (\<lambda>x. st_tcb_at' runnable' (hd (ksReadyQueues sa (curdom, lookupBitmapPriority curdom s))) sb) (hd (ksReadyQueues sa (curdom, lookupBitmapPriority curdom s)))) sb)) sa \<and> curdom \<le> maxDomain \<and> lookupBitmapPriority curdom s \<le> maxPriority))) s)) s) and (\<lambda>s. \<not> rv \<noteq> 0 \<longrightarrow> all_invs_but_ct_idle_or_in_cur_domain' s)) s))\<rbrace>
 3. guard_is_UNIV (\<lambda>rv rv'. rv' = UCAST(8 \<rightarrow> 32) rv) dom_' (\<lambda>a b. {s'. a \<le> maxDomain \<longrightarrow> s' \<in> {s. \<forall>rv. ksReadyQueuesL1Bitmap_' (globals s).[unat a] = UCAST(32 \<rightarrow> 32) rv \<longrightarrow> s \<in> {s. dom_'_update (\<lambda>x. b) s \<in> UNIV \<inter> \<lbrace>\<acute>dom = b\<rbrace>} \<inter> \<lbrace>\<acute>ksReadyQueuesL1Bitmap.[unat a] \<noteq> 0\<rbrace> \<union> {s. s \<in> UNIV} \<inter> - \<lbrace>\<acute>ksReadyQueuesL1Bitmap.[unat a] \<noteq> 0\<rbrace>} \<inter> \<lbrace>b < 0x10\<rbrace>})
 4. \<And>s s'. \<lbrakk>(s, s') \<in> rf_sr; all_invs_but_ct_idle_or_in_cur_domain' s; s' \<in> UNIV\<rbrakk> \<Longrightarrow> ((\<lambda>_. True) and ?R301) s \<and> s' \<in> UNIV proof (prove)
goal (4 subgoals):
 1. \<And>curdom s rv rva sa a list tcb. \<lbrakk>prio_' s = UCAST(8 \<rightarrow> 32) rv; curdom \<le> maxDomain; rv \<le> maxPriority; (sa, s) \<in> rf_sr; obj_at' (\<lambda>x. rva) a sa; Invariants_H.valid_queues sa; StateRelation_C.end_C (ksReadyQueues_' (globals s).[unat curdom * 256 + unat rv]) = tcb_ptr_to_ctcb_ptr (if list = [] then a else last list); head_C (ksReadyQueues_' (globals s).[unat curdom * 256 + unat rv]) = tcb_ptr_to_ctcb_ptr a; cslift s (tcb_ptr_to_ctcb_ptr a) = Some tcb; tcbSchedPrev_C tcb = NULL; sched_queue_relation (cslift s) list (tcb_ptr_to_ctcb_ptr a) (tcbSchedNext_C tcb); numDomains \<le> Suc 0\<rbrakk> \<Longrightarrow> UCAST(8 \<rightarrow> 32) curdom = 0
 2. \<lbrace>?R301\<rbrace> if Suc 0 < numDomains then curDomain else return 0 \<lbrace>\<lambda>curdom. K (curdom \<le> maxDomain) and (\<lambda>s. curdom \<le> maxDomain \<and> (\<forall>rv. ksReadyQueuesL1Bitmap s curdom = rv \<longrightarrow> ((\<lambda>s. rv = ksReadyQueuesL1Bitmap s curdom \<and> curdom \<le> maxDomain) and (\<lambda>s. rv \<noteq> 0 \<longrightarrow> ((\<lambda>s. curdom \<le> maxDomain \<and> ksReadyQueuesL1Bitmap s curdom \<noteq> 0 \<and> bitmapQ_no_L1_orphans s) and (\<lambda>s. (K (curdom \<le> maxDomain) and (K (lookupBitmapPriority curdom s \<le> maxPriority) and (\<lambda>sa. (K (ksReadyQueues sa (curdom, lookupBitmapPriority curdom s) \<noteq> []) and (\<lambda>sb. (all_invs_but_ct_idle_or_in_cur_domain' and obj_at' (\<lambda>x. st_tcb_at' runnable' (hd (ksReadyQueues sa (curdom, lookupBitmapPriority curdom s))) sb) (hd (ksReadyQueues sa (curdom, lookupBitmapPriority curdom s)))) sb)) sa \<and> curdom \<le> maxDomain \<and> lookupBitmapPriority curdom s \<le> maxPriority))) s)) s) and (\<lambda>s. \<not> rv \<noteq> 0 \<longrightarrow> all_invs_but_ct_idle_or_in_cur_domain' s)) s))\<rbrace>
 3. guard_is_UNIV (\<lambda>rv rv'. rv' = UCAST(8 \<rightarrow> 32) rv) dom_' (\<lambda>a b. {s'. a \<le> maxDomain \<longrightarrow> s' \<in> {s. \<forall>rv. ksReadyQueuesL1Bitmap_' (globals s).[unat a] = UCAST(32 \<rightarrow> 32) rv \<longrightarrow> s \<in> {s. dom_'_update (\<lambda>x. b) s \<in> UNIV \<inter> \<lbrace>\<acute>dom = b\<rbrace>} \<inter> \<lbrace>\<acute>ksReadyQueuesL1Bitmap.[unat a] \<noteq> 0\<rbrace> \<union> {s. s \<in> UNIV} \<inter> - \<lbrace>\<acute>ksReadyQueuesL1Bitmap.[unat a] \<noteq> 0\<rbrace>} \<inter> \<lbrace>b < 0x10\<rbrace>})
 4. \<And>s s'. \<lbrakk>(s, s') \<in> rf_sr; all_invs_but_ct_idle_or_in_cur_domain' s; s' \<in> UNIV\<rbrakk> \<Longrightarrow> ((\<lambda>_. True) and ?R301) s \<and> s' \<in> UNIV proof (prove)
goal (3 subgoals):
 1. \<lbrace>?R301\<rbrace> if Suc 0 < numDomains then curDomain else return 0 \<lbrace>\<lambda>curdom. K (curdom \<le> maxDomain) and (\<lambda>s. curdom \<le> maxDomain \<and> (\<forall>rv. ksReadyQueuesL1Bitmap s curdom = rv \<longrightarrow> ((\<lambda>s. rv = ksReadyQueuesL1Bitmap s curdom \<and> curdom \<le> maxDomain) and (\<lambda>s. rv \<noteq> 0 \<longrightarrow> ((\<lambda>s. curdom \<le> maxDomain \<and> ksReadyQueuesL1Bitmap s curdom \<noteq> 0 \<and> bitmapQ_no_L1_orphans s) and (\<lambda>s. (K (curdom \<le> maxDomain) and (K (lookupBitmapPriority curdom s \<le> maxPriority) and (\<lambda>sa. (K (ksReadyQueues sa (curdom, lookupBitmapPriority curdom s) \<noteq> []) and (\<lambda>sb. (all_invs_but_ct_idle_or_in_cur_domain' and obj_at' (\<lambda>x. st_tcb_at' runnable' (hd (ksReadyQueues sa (curdom, lookupBitmapPriority curdom s))) sb) (hd (ksReadyQueues sa (curdom, lookupBitmapPriority curdom s)))) sb)) sa \<and> curdom \<le> maxDomain \<and> lookupBitmapPriority curdom s \<le> maxPriority))) s)) s) and (\<lambda>s. \<not> rv \<noteq> 0 \<longrightarrow> all_invs_but_ct_idle_or_in_cur_domain' s)) s))\<rbrace>
 2. guard_is_UNIV (\<lambda>rv rv'. rv' = UCAST(8 \<rightarrow> 32) rv) dom_' (\<lambda>a b. {s'. a \<le> maxDomain \<longrightarrow> s' \<in> {s. \<forall>rv. ksReadyQueuesL1Bitmap_' (globals s).[unat a] = UCAST(32 \<rightarrow> 32) rv \<longrightarrow> s \<in> {s. dom_'_update (\<lambda>x. b) s \<in> UNIV \<inter> \<lbrace>\<acute>dom = b\<rbrace>} \<inter> \<lbrace>\<acute>ksReadyQueuesL1Bitmap.[unat a] \<noteq> 0\<rbrace> \<union> {s. s \<in> UNIV} \<inter> - \<lbrace>\<acute>ksReadyQueuesL1Bitmap.[unat a] \<noteq> 0\<rbrace>} \<inter> \<lbrace>b < 0x10\<rbrace>})
 3. \<And>s s'. \<lbrakk>(s, s') \<in> rf_sr; all_invs_but_ct_idle_or_in_cur_domain' s; s' \<in> UNIV\<rbrakk> \<Longrightarrow> ((\<lambda>_. True) and ?R301) s \<and> s' \<in> UNIV proof (prove)
goal (2 subgoals):
 1. guard_is_UNIV (\<lambda>rv rv'. rv' = UCAST(8 \<rightarrow> 32) rv) dom_' (\<lambda>a b. {s'. a \<le> maxDomain \<longrightarrow> s' \<in> {s. \<forall>rv. ksReadyQueuesL1Bitmap_' (globals s).[unat a] = UCAST(32 \<rightarrow> 32) rv \<longrightarrow> s \<in> {s. dom_'_update (\<lambda>x. b) s \<in> UNIV \<inter> \<lbrace>\<acute>dom = b\<rbrace>} \<inter> \<lbrace>\<acute>ksReadyQueuesL1Bitmap.[unat a] \<noteq> 0\<rbrace> \<union> {s. s \<in> UNIV} \<inter> - \<lbrace>\<acute>ksReadyQueuesL1Bitmap.[unat a] \<noteq> 0\<rbrace>} \<inter> \<lbrace>b < 0x10\<rbrace>})
 2. \<And>s s'. \<lbrakk>(s, s') \<in> rf_sr; all_invs_but_ct_idle_or_in_cur_domain' s; s' \<in> UNIV\<rbrakk> \<Longrightarrow> ((\<lambda>_. True) and (\<lambda>s. (Suc 0 < numDomains \<longrightarrow> K (ksCurDomain s \<le> maxDomain) s \<and> ksCurDomain s \<le> maxDomain \<and> (\<forall>rv. ksReadyQueuesL1Bitmap s (ksCurDomain s) = rv \<longrightarrow> ((\<lambda>sa. rv = ksReadyQueuesL1Bitmap sa (ksCurDomain s) \<and> ksCurDomain s \<le> maxDomain) and (\<lambda>sa. rv \<noteq> 0 \<longrightarrow> ((\<lambda>sa. ksCurDomain s \<le> maxDomain \<and> ksReadyQueuesL1Bitmap sa (ksCurDomain s) \<noteq> 0 \<and> bitmapQ_no_L1_orphans sa) and (\<lambda>sa. (K (ksCurDomain s \<le> maxDomain) and (K (lookupBitmapPriority (ksCurDomain s) sa \<le> maxPriority) and (\<lambda>sb. (K (ksReadyQueues sb (ksCurDomain s, lookupBitmapPriority (ksCurDomain s) sa) \<noteq> []) and (\<lambda>sc. (all_invs_but_ct_idle_or_in_cur_domain' and obj_at' (\<lambda>x. st_tcb_at' runnable' (hd (ksReadyQueues sb (ksCurDomain s, lookupBitmapPriority (ksCurDomain s) sa))) sc) (hd (ksReadyQueues sb (ksCurDomain s, lookupBitmapPriority (ksCurDomain s) sa)))) sc)) sb \<and> ksCurDomain s \<le> maxDomain \<and> lookupBitmapPriority (ksCurDomain s) sa \<le> maxPriority))) sa)) sa) and (\<lambda>s. \<not> rv \<noteq> 0 \<longrightarrow> all_invs_but_ct_idle_or_in_cur_domain' s)) s)) \<and> (\<not> Suc 0 < numDomains \<longrightarrow> K (0 \<le> maxDomain) s \<and> 0 \<le> maxDomain \<and> (\<forall>rv. ksReadyQueuesL1Bitmap s 0 = rv \<longrightarrow> ((\<lambda>s. rv = ksReadyQueuesL1Bitmap s 0 \<and> 0 \<le> maxDomain) and (\<lambda>s. rv \<noteq> 0 \<longrightarrow> ((\<lambda>s. 0 \<le> maxDomain \<and> ksReadyQueuesL1Bitmap s 0 \<noteq> 0 \<and> bitmapQ_no_L1_orphans s) and (\<lambda>s. (K (0 \<le> maxDomain) and (K (lookupBitmapPriority 0 s \<le> maxPriority) and (\<lambda>sa. (K (ksReadyQueues sa (0, lookupBitmapPriority 0 s) \<noteq> []) and (\<lambda>sb. (all_invs_but_ct_idle_or_in_cur_domain' and obj_at' (\<lambda>x. st_tcb_at' runnable' (hd (ksReadyQueues sa (0, lookupBitmapPriority 0 s))) sb) (hd (ksReadyQueues sa (0, lookupBitmapPriority 0 s)))) sb)) sa \<and> 0 \<le> maxDomain \<and> lookupBitmapPriority 0 s \<le> maxPriority))) s)) s) and (\<lambda>s. \<not> rv \<noteq> 0 \<longrightarrow> all_invs_but_ct_idle_or_in_cur_domain' s)) s)))) s \<and> s' \<in> UNIV proof (prove)
goal (1 subgoal):
 1. \<And>s s'. \<lbrakk>(s, s') \<in> rf_sr; all_invs_but_ct_idle_or_in_cur_domain' s; s' \<in> UNIV\<rbrakk> \<Longrightarrow> ((\<lambda>_. True) and (\<lambda>s. (Suc 0 < numDomains \<longrightarrow> K (ksCurDomain s \<le> maxDomain) s \<and> ksCurDomain s \<le> maxDomain \<and> (\<forall>rv. ksReadyQueuesL1Bitmap s (ksCurDomain s) = rv \<longrightarrow> ((\<lambda>sa. rv = ksReadyQueuesL1Bitmap sa (ksCurDomain s) \<and> ksCurDomain s \<le> maxDomain) and (\<lambda>sa. rv \<noteq> 0 \<longrightarrow> ((\<lambda>sa. ksCurDomain s \<le> maxDomain \<and> ksReadyQueuesL1Bitmap sa (ksCurDomain s) \<noteq> 0 \<and> bitmapQ_no_L1_orphans sa) and (\<lambda>sa. (K (ksCurDomain s \<le> maxDomain) and (K (lookupBitmapPriority (ksCurDomain s) sa \<le> maxPriority) and (\<lambda>sb. (K (ksReadyQueues sb (ksCurDomain s, lookupBitmapPriority (ksCurDomain s) sa) \<noteq> []) and (\<lambda>sc. (all_invs_but_ct_idle_or_in_cur_domain' and obj_at' (\<lambda>x. st_tcb_at' runnable' (hd (ksReadyQueues sb (ksCurDomain s, lookupBitmapPriority (ksCurDomain s) sa))) sc) (hd (ksReadyQueues sb (ksCurDomain s, lookupBitmapPriority (ksCurDomain s) sa)))) sc)) sb \<and> ksCurDomain s \<le> maxDomain \<and> lookupBitmapPriority (ksCurDomain s) sa \<le> maxPriority))) sa)) sa) and (\<lambda>s. \<not> rv \<noteq> 0 \<longrightarrow> all_invs_but_ct_idle_or_in_cur_domain' s)) s)) \<and> (\<not> Suc 0 < numDomains \<longrightarrow> K (0 \<le> maxDomain) s \<and> 0 \<le> maxDomain \<and> (\<forall>rv. ksReadyQueuesL1Bitmap s 0 = rv \<longrightarrow> ((\<lambda>s. rv = ksReadyQueuesL1Bitmap s 0 \<and> 0 \<le> maxDomain) and (\<lambda>s. rv \<noteq> 0 \<longrightarrow> ((\<lambda>s. 0 \<le> maxDomain \<and> ksReadyQueuesL1Bitmap s 0 \<noteq> 0 \<and> bitmapQ_no_L1_orphans s) and (\<lambda>s. (K (0 \<le> maxDomain) and (K (lookupBitmapPriority 0 s \<le> maxPriority) and (\<lambda>sa. (K (ksReadyQueues sa (0, lookupBitmapPriority 0 s) \<noteq> []) and (\<lambda>sb. (all_invs_but_ct_idle_or_in_cur_domain' and obj_at' (\<lambda>x. st_tcb_at' runnable' (hd (ksReadyQueues sa (0, lookupBitmapPriority 0 s))) sb) (hd (ksReadyQueues sa (0, lookupBitmapPriority 0 s)))) sb)) sa \<and> 0 \<le> maxDomain \<and> lookupBitmapPriority 0 s \<le> maxPriority))) s)) s) and (\<lambda>s. \<not> rv \<noteq> 0 \<longrightarrow> all_invs_but_ct_idle_or_in_cur_domain' s)) s)))) s \<and> s' \<in> UNIV proof (prove)
goal (1 subgoal):
 1. \<And>s s'. \<lbrakk>(s, s') \<in> rf_sr; all_invs_but_ct_idle_or_in_cur_domain' s; s' \<in> UNIV; Invariants_H.valid_queues s\<rbrakk> \<Longrightarrow> ((\<lambda>_. True) and (\<lambda>s. (Suc 0 < numDomains \<longrightarrow> K (ksCurDomain s \<le> maxDomain) s \<and> ksCurDomain s \<le> maxDomain \<and> (\<forall>rv. ksReadyQueuesL1Bitmap s (ksCurDomain s) = rv \<longrightarrow> ((\<lambda>sa. rv = ksReadyQueuesL1Bitmap sa (ksCurDomain s) \<and> ksCurDomain s \<le> maxDomain) and (\<lambda>sa. rv \<noteq> 0 \<longrightarrow> ((\<lambda>sa. ksCurDomain s \<le> maxDomain \<and> ksReadyQueuesL1Bitmap sa (ksCurDomain s) \<noteq> 0 \<and> bitmapQ_no_L1_orphans sa) and (\<lambda>sa. (K (ksCurDomain s \<le> maxDomain) and (K (lookupBitmapPriority (ksCurDomain s) sa \<le> maxPriority) and (\<lambda>sb. (K (ksReadyQueues sb (ksCurDomain s, lookupBitmapPriority (ksCurDomain s) sa) \<noteq> []) and (\<lambda>sc. (all_invs_but_ct_idle_or_in_cur_domain' and obj_at' (\<lambda>x. st_tcb_at' runnable' (hd (ksReadyQueues sb (ksCurDomain s, lookupBitmapPriority (ksCurDomain s) sa))) sc) (hd (ksReadyQueues sb (ksCurDomain s, lookupBitmapPriority (ksCurDomain s) sa)))) sc)) sb \<and> ksCurDomain s \<le> maxDomain \<and> lookupBitmapPriority (ksCurDomain s) sa \<le> maxPriority))) sa)) sa) and (\<lambda>s. \<not> rv \<noteq> 0 \<longrightarrow> all_invs_but_ct_idle_or_in_cur_domain' s)) s)) \<and> (\<not> Suc 0 < numDomains \<longrightarrow> K (0 \<le> maxDomain) s \<and> 0 \<le> maxDomain \<and> (\<forall>rv. ksReadyQueuesL1Bitmap s 0 = rv \<longrightarrow> ((\<lambda>s. rv = ksReadyQueuesL1Bitmap s 0 \<and> 0 \<le> maxDomain) and (\<lambda>s. rv \<noteq> 0 \<longrightarrow> ((\<lambda>s. 0 \<le> maxDomain \<and> ksReadyQueuesL1Bitmap s 0 \<noteq> 0 \<and> bitmapQ_no_L1_orphans s) and (\<lambda>s. (K (0 \<le> maxDomain) and (K (lookupBitmapPriority 0 s \<le> maxPriority) and (\<lambda>sa. (K (ksReadyQueues sa (0, lookupBitmapPriority 0 s) \<noteq> []) and (\<lambda>sb. (all_invs_but_ct_idle_or_in_cur_domain' and obj_at' (\<lambda>x. st_tcb_at' runnable' (hd (ksReadyQueues sa (0, lookupBitmapPriority 0 s))) sb) (hd (ksReadyQueues sa (0, lookupBitmapPriority 0 s)))) sb)) sa \<and> 0 \<le> maxDomain \<and> lookupBitmapPriority 0 s \<le> maxPriority))) s)) s) and (\<lambda>s. \<not> rv \<noteq> 0 \<longrightarrow> all_invs_but_ct_idle_or_in_cur_domain' s)) s)))) s \<and> s' \<in> UNIV proof (prove)
goal (1 subgoal):
 1. \<And>s s'. \<lbrakk>(s, s') \<in> rf_sr; all_invs_but_ct_idle_or_in_cur_domain' s; s' \<in> UNIV; Invariants_H.valid_queues s; ksCurDomain s \<le> maxDomain\<rbrakk> \<Longrightarrow> ((\<lambda>_. True) and (\<lambda>s. (Suc 0 < numDomains \<longrightarrow> K (ksCurDomain s \<le> maxDomain) s \<and> ksCurDomain s \<le> maxDomain \<and> (\<forall>rv. ksReadyQueuesL1Bitmap s (ksCurDomain s) = rv \<longrightarrow> ((\<lambda>sa. rv = ksReadyQueuesL1Bitmap sa (ksCurDomain s) \<and> ksCurDomain s \<le> maxDomain) and (\<lambda>sa. rv \<noteq> 0 \<longrightarrow> ((\<lambda>sa. ksCurDomain s \<le> maxDomain \<and> ksReadyQueuesL1Bitmap sa (ksCurDomain s) \<noteq> 0 \<and> bitmapQ_no_L1_orphans sa) and (\<lambda>sa. (K (ksCurDomain s \<le> maxDomain) and (K (lookupBitmapPriority (ksCurDomain s) sa \<le> maxPriority) and (\<lambda>sb. (K (ksReadyQueues sb (ksCurDomain s, lookupBitmapPriority (ksCurDomain s) sa) \<noteq> []) and (\<lambda>sc. (all_invs_but_ct_idle_or_in_cur_domain' and obj_at' (\<lambda>x. st_tcb_at' runnable' (hd (ksReadyQueues sb (ksCurDomain s, lookupBitmapPriority (ksCurDomain s) sa))) sc) (hd (ksReadyQueues sb (ksCurDomain s, lookupBitmapPriority (ksCurDomain s) sa)))) sc)) sb \<and> ksCurDomain s \<le> maxDomain \<and> lookupBitmapPriority (ksCurDomain s) sa \<le> maxPriority))) sa)) sa) and (\<lambda>s. \<not> rv \<noteq> 0 \<longrightarrow> all_invs_but_ct_idle_or_in_cur_domain' s)) s)) \<and> (\<not> Suc 0 < numDomains \<longrightarrow> K (0 \<le> maxDomain) s \<and> 0 \<le> maxDomain \<and> (\<forall>rv. ksReadyQueuesL1Bitmap s 0 = rv \<longrightarrow> ((\<lambda>s. rv = ksReadyQueuesL1Bitmap s 0 \<and> 0 \<le> maxDomain) and (\<lambda>s. rv \<noteq> 0 \<longrightarrow> ((\<lambda>s. 0 \<le> maxDomain \<and> ksReadyQueuesL1Bitmap s 0 \<noteq> 0 \<and> bitmapQ_no_L1_orphans s) and (\<lambda>s. (K (0 \<le> maxDomain) and (K (lookupBitmapPriority 0 s \<le> maxPriority) and (\<lambda>sa. (K (ksReadyQueues sa (0, lookupBitmapPriority 0 s) \<noteq> []) and (\<lambda>sb. (all_invs_but_ct_idle_or_in_cur_domain' and obj_at' (\<lambda>x. st_tcb_at' runnable' (hd (ksReadyQueues sa (0, lookupBitmapPriority 0 s))) sb) (hd (ksReadyQueues sa (0, lookupBitmapPriority 0 s)))) sb)) sa \<and> 0 \<le> maxDomain \<and> lookupBitmapPriority 0 s \<le> maxPriority))) s)) s) and (\<lambda>s. \<not> rv \<noteq> 0 \<longrightarrow> all_invs_but_ct_idle_or_in_cur_domain' s)) s)))) s \<and> s' \<in> UNIV proof (prove)
goal (1 subgoal):
 1. \<And>s s'. \<lbrakk>(s, s') \<in> rf_sr; all_invs_but_ct_idle_or_in_cur_domain' s; s' \<in> UNIV; Invariants_H.valid_queues s; ksCurDomain s \<le> maxDomain; Invariants_H.valid_queues s\<rbrakk> \<Longrightarrow> ((\<lambda>_. True) and (\<lambda>s. (Suc 0 < numDomains \<longrightarrow> K (ksCurDomain s \<le> maxDomain) s \<and> ksCurDomain s \<le> maxDomain \<and> (\<forall>rv. ksReadyQueuesL1Bitmap s (ksCurDomain s) = rv \<longrightarrow> ((\<lambda>sa. rv = ksReadyQueuesL1Bitmap sa (ksCurDomain s) \<and> ksCurDomain s \<le> maxDomain) and (\<lambda>sa. rv \<noteq> 0 \<longrightarrow> ((\<lambda>sa. ksCurDomain s \<le> maxDomain \<and> ksReadyQueuesL1Bitmap sa (ksCurDomain s) \<noteq> 0 \<and> bitmapQ_no_L1_orphans sa) and (\<lambda>sa. (K (ksCurDomain s \<le> maxDomain) and (K (lookupBitmapPriority (ksCurDomain s) sa \<le> maxPriority) and (\<lambda>sb. (K (ksReadyQueues sb (ksCurDomain s, lookupBitmapPriority (ksCurDomain s) sa) \<noteq> []) and (\<lambda>sc. (all_invs_but_ct_idle_or_in_cur_domain' and obj_at' (\<lambda>x. st_tcb_at' runnable' (hd (ksReadyQueues sb (ksCurDomain s, lookupBitmapPriority (ksCurDomain s) sa))) sc) (hd (ksReadyQueues sb (ksCurDomain s, lookupBitmapPriority (ksCurDomain s) sa)))) sc)) sb \<and> ksCurDomain s \<le> maxDomain \<and> lookupBitmapPriority (ksCurDomain s) sa \<le> maxPriority))) sa)) sa) and (\<lambda>s. \<not> rv \<noteq> 0 \<longrightarrow> all_invs_but_ct_idle_or_in_cur_domain' s)) s)) \<and> (\<not> Suc 0 < numDomains \<longrightarrow> K (0 \<le> maxDomain) s \<and> 0 \<le> maxDomain \<and> (\<forall>rv. ksReadyQueuesL1Bitmap s 0 = rv \<longrightarrow> ((\<lambda>s. rv = ksReadyQueuesL1Bitmap s 0 \<and> 0 \<le> maxDomain) and (\<lambda>s. rv \<noteq> 0 \<longrightarrow> ((\<lambda>s. 0 \<le> maxDomain \<and> ksReadyQueuesL1Bitmap s 0 \<noteq> 0 \<and> bitmapQ_no_L1_orphans s) and (\<lambda>s. (K (0 \<le> maxDomain) and (K (lookupBitmapPriority 0 s \<le> maxPriority) and (\<lambda>sa. (K (ksReadyQueues sa (0, lookupBitmapPriority 0 s) \<noteq> []) and (\<lambda>sb. (all_invs_but_ct_idle_or_in_cur_domain' and obj_at' (\<lambda>x. st_tcb_at' runnable' (hd (ksReadyQueues sa (0, lookupBitmapPriority 0 s))) sb) (hd (ksReadyQueues sa (0, lookupBitmapPriority 0 s)))) sb)) sa \<and> 0 \<le> maxDomain \<and> lookupBitmapPriority 0 s \<le> maxPriority))) s)) s) and (\<lambda>s. \<not> rv \<noteq> 0 \<longrightarrow> all_invs_but_ct_idle_or_in_cur_domain' s)) s)))) s \<and> s' \<in> UNIV proof (prove)
goal (1 subgoal):
 1. \<And>s s'. \<lbrakk>(s, s') \<in> rf_sr; all_invs_but_ct_idle_or_in_cur_domain' s; ksCurDomain s \<le> maxDomain; valid_queues_no_bitmap s; valid_bitmapQ s; bitmapQ_no_L2_orphans s; bitmapQ_no_L1_orphans s\<rbrakk> \<Longrightarrow> (Suc 0 < numDomains \<longrightarrow> ksReadyQueuesL1Bitmap s (ksCurDomain s) \<noteq> 0 \<longrightarrow> ksReadyQueues s (ksCurDomain s, lookupBitmapPriority (ksCurDomain s) s) \<noteq> [] \<and> obj_at' (\<lambda>x. st_tcb_at' runnable' (hd (ksReadyQueues s (ksCurDomain s, lookupBitmapPriority (ksCurDomain s) s))) s) (hd (ksReadyQueues s (ksCurDomain s, lookupBitmapPriority (ksCurDomain s) s))) s) \<and> (\<not> Suc 0 < numDomains \<longrightarrow> ksReadyQueuesL1Bitmap s 0 \<noteq> 0 \<longrightarrow> ksReadyQueues s (0, lookupBitmapPriority 0 s) \<noteq> [] \<and> obj_at' (\<lambda>x. st_tcb_at' runnable' (hd (ksReadyQueues s (0, lookupBitmapPriority 0 s))) s) (hd (ksReadyQueues s (0, lookupBitmapPriority 0 s))) s) proof (prove)
goal (4 subgoals):
 1. \<And>s s'. \<lbrakk>(s, s') \<in> rf_sr; all_invs_but_ct_idle_or_in_cur_domain' s; ksCurDomain s \<le> maxDomain; valid_queues_no_bitmap s; valid_bitmapQ s; bitmapQ_no_L2_orphans s; bitmapQ_no_L1_orphans s; Suc 0 < numDomains; ksReadyQueuesL1Bitmap s (ksCurDomain s) \<noteq> 0\<rbrakk> \<Longrightarrow> ksReadyQueues s (ksCurDomain s, lookupBitmapPriority (ksCurDomain s) s) \<noteq> []
 2. \<And>s s'. \<lbrakk>(s, s') \<in> rf_sr; all_invs_but_ct_idle_or_in_cur_domain' s; ksCurDomain s \<le> maxDomain; valid_queues_no_bitmap s; valid_bitmapQ s; bitmapQ_no_L2_orphans s; bitmapQ_no_L1_orphans s; Suc 0 < numDomains; ksReadyQueuesL1Bitmap s (ksCurDomain s) \<noteq> 0\<rbrakk> \<Longrightarrow> obj_at' (\<lambda>x. st_tcb_at' runnable' (hd (ksReadyQueues s (ksCurDomain s, lookupBitmapPriority (ksCurDomain s) s))) s) (hd (ksReadyQueues s (ksCurDomain s, lookupBitmapPriority (ksCurDomain s) s))) s
 3. \<And>s s'. \<lbrakk>(s, s') \<in> rf_sr; all_invs_but_ct_idle_or_in_cur_domain' s; ksCurDomain s \<le> maxDomain; valid_queues_no_bitmap s; valid_bitmapQ s; bitmapQ_no_L2_orphans s; bitmapQ_no_L1_orphans s; \<not> Suc 0 < numDomains; ksReadyQueuesL1Bitmap s 0 \<noteq> 0\<rbrakk> \<Longrightarrow> ksReadyQueues s (0, lookupBitmapPriority 0 s) \<noteq> []
 4. \<And>s s'. \<lbrakk>(s, s') \<in> rf_sr; all_invs_but_ct_idle_or_in_cur_domain' s; ksCurDomain s \<le> maxDomain; valid_queues_no_bitmap s; valid_bitmapQ s; bitmapQ_no_L2_orphans s; bitmapQ_no_L1_orphans s; \<not> Suc 0 < numDomains; ksReadyQueuesL1Bitmap s 0 \<noteq> 0\<rbrakk> \<Longrightarrow> obj_at' (\<lambda>x. st_tcb_at' runnable' (hd (ksReadyQueues s (0, lookupBitmapPriority 0 s))) s) (hd (ksReadyQueues s (0, lookupBitmapPriority 0 s))) s proof (prove)
goal (3 subgoals):
 1. \<And>s s'. \<lbrakk>(s, s') \<in> rf_sr; all_invs_but_ct_idle_or_in_cur_domain' s; ksCurDomain s \<le> maxDomain; valid_queues_no_bitmap s; valid_bitmapQ s; bitmapQ_no_L2_orphans s; bitmapQ_no_L1_orphans s; Suc 0 < numDomains; ksReadyQueuesL1Bitmap s (ksCurDomain s) \<noteq> 0\<rbrakk> \<Longrightarrow> obj_at' (\<lambda>x. st_tcb_at' runnable' (hd (ksReadyQueues s (ksCurDomain s, lookupBitmapPriority (ksCurDomain s) s))) s) (hd (ksReadyQueues s (ksCurDomain s, lookupBitmapPriority (ksCurDomain s) s))) s
 2. \<And>s s'. \<lbrakk>(s, s') \<in> rf_sr; all_invs_but_ct_idle_or_in_cur_domain' s; ksCurDomain s \<le> maxDomain; valid_queues_no_bitmap s; valid_bitmapQ s; bitmapQ_no_L2_orphans s; bitmapQ_no_L1_orphans s; \<not> Suc 0 < numDomains; ksReadyQueuesL1Bitmap s 0 \<noteq> 0\<rbrakk> \<Longrightarrow> ksReadyQueues s (0, lookupBitmapPriority 0 s) \<noteq> []
 3. \<And>s s'. \<lbrakk>(s, s') \<in> rf_sr; all_invs_but_ct_idle_or_in_cur_domain' s; ksCurDomain s \<le> maxDomain; valid_queues_no_bitmap s; valid_bitmapQ s; bitmapQ_no_L2_orphans s; bitmapQ_no_L1_orphans s; \<not> Suc 0 < numDomains; ksReadyQueuesL1Bitmap s 0 \<noteq> 0\<rbrakk> \<Longrightarrow> obj_at' (\<lambda>x. st_tcb_at' runnable' (hd (ksReadyQueues s (0, lookupBitmapPriority 0 s))) s) (hd (ksReadyQueues s (0, lookupBitmapPriority 0 s))) s proof (prove)
goal (2 subgoals):
 1. \<And>s s'. \<lbrakk>(s, s') \<in> rf_sr; all_invs_but_ct_idle_or_in_cur_domain' s; ksCurDomain s \<le> maxDomain; valid_queues_no_bitmap s; valid_bitmapQ s; bitmapQ_no_L2_orphans s; bitmapQ_no_L1_orphans s; \<not> Suc 0 < numDomains; ksReadyQueuesL1Bitmap s 0 \<noteq> 0\<rbrakk> \<Longrightarrow> ksReadyQueues s (0, lookupBitmapPriority 0 s) \<noteq> []
 2. \<And>s s'. \<lbrakk>(s, s') \<in> rf_sr; all_invs_but_ct_idle_or_in_cur_domain' s; ksCurDomain s \<le> maxDomain; valid_queues_no_bitmap s; valid_bitmapQ s; bitmapQ_no_L2_orphans s; bitmapQ_no_L1_orphans s; \<not> Suc 0 < numDomains; ksReadyQueuesL1Bitmap s 0 \<noteq> 0\<rbrakk> \<Longrightarrow> obj_at' (\<lambda>x. st_tcb_at' runnable' (hd (ksReadyQueues s (0, lookupBitmapPriority 0 s))) s) (hd (ksReadyQueues s (0, lookupBitmapPriority 0 s))) s proof (prove)
goal (1 subgoal):
 1. \<And>s s'. \<lbrakk>(s, s') \<in> rf_sr; all_invs_but_ct_idle_or_in_cur_domain' s; ksCurDomain s \<le> maxDomain; valid_queues_no_bitmap s; valid_bitmapQ s; bitmapQ_no_L2_orphans s; bitmapQ_no_L1_orphans s; \<not> Suc 0 < numDomains; ksReadyQueuesL1Bitmap s 0 \<noteq> 0\<rbrakk> \<Longrightarrow> obj_at' (\<lambda>x. st_tcb_at' runnable' (hd (ksReadyQueues s (0, lookupBitmapPriority 0 s))) s) (hd (ksReadyQueues s (0, lookupBitmapPriority 0 s))) s proof (prove)
goal (1 subgoal):
 1. \<And>s s'. \<lbrakk>(s, s') \<in> rf_sr; all_invs_but_ct_idle_or_in_cur_domain' s; ksCurDomain s \<le> maxDomain; valid_queues_no_bitmap s; valid_bitmapQ s; bitmapQ_no_L2_orphans s; bitmapQ_no_L1_orphans s; \<not> Suc 0 < numDomains; ksReadyQueuesL1Bitmap s 0 \<noteq> 0\<rbrakk> \<Longrightarrow> \<exists>ko. ksPSpace s (hd (ksReadyQueues s (0, lookupBitmapPriority 0 s))) = Some ko \<and> is_aligned (hd (ksReadyQueues s (0, lookupBitmapPriority 0 s))) (objBitsKO ko) \<and> (\<exists>obj. fst (projectKO ko s) = {(obj, s)}) \<and> (\<exists>ko. ksPSpace s (hd (ksReadyQueues s (0, lookupBitmapPriority 0 s))) = Some ko \<and> is_aligned (hd (ksReadyQueues s (0, lookupBitmapPriority 0 s))) (objBitsKO ko) \<and> (\<exists>obj. fst (projectKO ko s) = {(obj, s)} \<and> runnable' (tcbState obj) \<and> ps_clear (hd (ksReadyQueues s (0, lookupBitmapPriority 0 s))) (objBitsKO ko) s)) \<and> ps_clear (hd (ksReadyQueues s (0, lookupBitmapPriority 0 s))) (objBitsKO ko) s proof (prove)
goal (1 subgoal):
 1. \<And>s s'. \<lbrakk>(s, s') \<in> rf_sr; all_invs_but_ct_idle_or_in_cur_domain' s; unat (ksCurDomain s) < numDomains; valid_queues_no_bitmap s; valid_bitmapQ s; bitmapQ_no_L2_orphans s; bitmapQ_no_L1_orphans s; numDomains \<le> Suc 0; ksReadyQueuesL1Bitmap s 0 \<noteq> 0\<rbrakk> \<Longrightarrow> \<exists>ko. ksPSpace s (hd (ksReadyQueues s (0, lookupBitmapPriority 0 s))) = Some ko \<and> is_aligned (hd (ksReadyQueues s (0, lookupBitmapPriority 0 s))) (objBitsKO ko) \<and> (\<exists>obj. fst (projectKO ko s) = {(obj, s)}) \<and> (\<exists>ko. ksPSpace s (hd (ksReadyQueues s (0, lookupBitmapPriority 0 s))) = Some ko \<and> is_aligned (hd (ksReadyQueues s (0, lookupBitmapPriority 0 s))) (objBitsKO ko) \<and> (\<exists>obj. fst (projectKO ko s) = {(obj, s)} \<and> runnable' (tcbState obj) \<and> ps_clear (hd (ksReadyQueues s (0, lookupBitmapPriority 0 s))) (objBitsKO ko) s)) \<and> ps_clear (hd (ksReadyQueues s (0, lookupBitmapPriority 0 s))) (objBitsKO ko) s proof (prove)
goal (2 subgoals):
 1. \<And>s s'. \<lbrakk>(s, s') \<in> rf_sr; all_invs_but_ct_idle_or_in_cur_domain' s; unat (ksCurDomain s) < numDomains; valid_queues_no_bitmap s; valid_bitmapQ s; bitmapQ_no_L2_orphans s; bitmapQ_no_L1_orphans s; numDomains \<le> Suc 0; ksReadyQueuesL1Bitmap s 0 \<noteq> 0\<rbrakk> \<Longrightarrow> ksCurDomain s = 0
 2. \<And>s s'. \<lbrakk>(s, s') \<in> rf_sr; all_invs_but_ct_idle_or_in_cur_domain' s; unat (ksCurDomain s) < numDomains; valid_queues_no_bitmap s; valid_bitmapQ s; bitmapQ_no_L2_orphans s; bitmapQ_no_L1_orphans s; numDomains \<le> Suc 0; ksReadyQueuesL1Bitmap s 0 \<noteq> 0; ksCurDomain s = 0\<rbrakk> \<Longrightarrow> \<exists>ko. ksPSpace s (hd (ksReadyQueues s (0, lookupBitmapPriority 0 s))) = Some ko \<and> is_aligned (hd (ksReadyQueues s (0, lookupBitmapPriority 0 s))) (objBitsKO ko) \<and> (\<exists>obj. fst (projectKO ko s) = {(obj, s)}) \<and> (\<exists>ko. ksPSpace s (hd (ksReadyQueues s (0, lookupBitmapPriority 0 s))) = Some ko \<and> is_aligned (hd (ksReadyQueues s (0, lookupBitmapPriority 0 s))) (objBitsKO ko) \<and> (\<exists>obj. fst (projectKO ko s) = {(obj, s)} \<and> runnable' (tcbState obj) \<and> ps_clear (hd (ksReadyQueues s (0, lookupBitmapPriority 0 s))) (objBitsKO ko) s)) \<and> ps_clear (hd (ksReadyQueues s (0, lookupBitmapPriority 0 s))) (objBitsKO ko) s proof (prove)
using this:
(unsigned ?w = (0::?'a)) = (?w = 0)

goal (2 subgoals):
 1. \<And>s s'. \<lbrakk>(s, s') \<in> rf_sr; all_invs_but_ct_idle_or_in_cur_domain' s; unat (ksCurDomain s) < numDomains; valid_queues_no_bitmap s; valid_bitmapQ s; bitmapQ_no_L2_orphans s; bitmapQ_no_L1_orphans s; numDomains \<le> Suc 0; ksReadyQueuesL1Bitmap s 0 \<noteq> 0\<rbrakk> \<Longrightarrow> ksCurDomain s = 0
 2. \<And>s s'. \<lbrakk>(s, s') \<in> rf_sr; all_invs_but_ct_idle_or_in_cur_domain' s; unat (ksCurDomain s) < numDomains; valid_queues_no_bitmap s; valid_bitmapQ s; bitmapQ_no_L2_orphans s; bitmapQ_no_L1_orphans s; numDomains \<le> Suc 0; ksReadyQueuesL1Bitmap s 0 \<noteq> 0; ksCurDomain s = 0\<rbrakk> \<Longrightarrow> \<exists>ko. ksPSpace s (hd (ksReadyQueues s (0, lookupBitmapPriority 0 s))) = Some ko \<and> is_aligned (hd (ksReadyQueues s (0, lookupBitmapPriority 0 s))) (objBitsKO ko) \<and> (\<exists>obj. fst (projectKO ko s) = {(obj, s)}) \<and> (\<exists>ko. ksPSpace s (hd (ksReadyQueues s (0, lookupBitmapPriority 0 s))) = Some ko \<and> is_aligned (hd (ksReadyQueues s (0, lookupBitmapPriority 0 s))) (objBitsKO ko) \<and> (\<exists>obj. fst (projectKO ko s) = {(obj, s)} \<and> runnable' (tcbState obj) \<and> ps_clear (hd (ksReadyQueues s (0, lookupBitmapPriority 0 s))) (objBitsKO ko) s)) \<and> ps_clear (hd (ksReadyQueues s (0, lookupBitmapPriority 0 s))) (objBitsKO ko) s proof (prove)
goal (1 subgoal):
 1. \<And>s s'. \<lbrakk>(s, s') \<in> rf_sr; all_invs_but_ct_idle_or_in_cur_domain' s; unat (ksCurDomain s) < numDomains; valid_queues_no_bitmap s; valid_bitmapQ s; bitmapQ_no_L2_orphans s; bitmapQ_no_L1_orphans s; numDomains \<le> Suc 0; ksReadyQueuesL1Bitmap s 0 \<noteq> 0; ksCurDomain s = 0\<rbrakk> \<Longrightarrow> \<exists>ko. ksPSpace s (hd (ksReadyQueues s (0, lookupBitmapPriority 0 s))) = Some ko \<and> is_aligned (hd (ksReadyQueues s (0, lookupBitmapPriority 0 s))) (objBitsKO ko) \<and> (\<exists>obj. fst (projectKO ko s) = {(obj, s)}) \<and> (\<exists>ko. ksPSpace s (hd (ksReadyQueues s (0, lookupBitmapPriority 0 s))) = Some ko \<and> is_aligned (hd (ksReadyQueues s (0, lookupBitmapPriority 0 s))) (objBitsKO ko) \<and> (\<exists>obj. fst (projectKO ko s) = {(obj, s)} \<and> runnable' (tcbState obj) \<and> ps_clear (hd (ksReadyQueues s (0, lookupBitmapPriority 0 s))) (objBitsKO ko) s)) \<and> ps_clear (hd (ksReadyQueues s (0, lookupBitmapPriority 0 s))) (objBitsKO ko) s proof (prove)
goal (1 subgoal):
 1. \<And>s s'. \<lbrakk>(s, s') \<in> rf_sr; all_invs_but_ct_idle_or_in_cur_domain' s; 0 < numDomains; valid_queues_no_bitmap s; valid_bitmapQ s; bitmapQ_no_L2_orphans s; bitmapQ_no_L1_orphans s; numDomains \<le> Suc 0; ksReadyQueuesL1Bitmap s 0 \<noteq> 0; ksCurDomain s = 0; obj_at' (inQ 0 (lookupBitmapPriority 0 s) and runnable' \<circ> tcbState) (hd (ksReadyQueues s (0, lookupBitmapPriority 0 s))) s\<rbrakk> \<Longrightarrow> \<exists>ko. ksPSpace s (hd (ksReadyQueues s (0, lookupBitmapPriority 0 s))) = Some ko \<and> is_aligned (hd (ksReadyQueues s (0, lookupBitmapPriority 0 s))) (objBitsKO ko) \<and> (\<exists>obj. fst (projectKO ko s) = {(obj, s)}) \<and> (\<exists>ko. ksPSpace s (hd (ksReadyQueues s (0, lookupBitmapPriority 0 s))) = Some ko \<and> is_aligned (hd (ksReadyQueues s (0, lookupBitmapPriority 0 s))) (objBitsKO ko) \<and> (\<exists>obj. fst (projectKO ko s) = {(obj, s)} \<and> runnable' (tcbState obj) \<and> ps_clear (hd (ksReadyQueues s (0, lookupBitmapPriority 0 s))) (objBitsKO ko) s)) \<and> ps_clear (hd (ksReadyQueues s (0, lookupBitmapPriority 0 s))) (objBitsKO ko) s proof (prove)
goal:
No subgoals! proof (state)
this:
ccorres dc xfdc all_invs_but_ct_idle_or_in_cur_domain' UNIV [] chooseThread (Call chooseThread_'proc)

goal:
No subgoals!