theory Syscall_R

lemma setDomain_corres:
  "corres dc
     (valid_etcbs and valid_sched and tcb_at tptr)
     (invs'  and sch_act_simple
             and tcb_at' tptr and (\<lambda>s. new_dom \<le> maxDomain))
     (set_domain tptr new_dom)
     (setDomain tptr new_dom)" apply (rule corres_gen_asm2) apply (simp add: set_domain_def setDomain_def thread_set_domain_def) apply (rule corres_guard_imp) apply (rule corres_split[OF getCurThread_corres]) apply (rule corres_split[OF tcbSchedDequeue_corres]) apply (rule corres_split) apply (rule ethread_set_corres; simp) apply (clarsimp simp: etcb_relation_def) apply (rule corres_split[OF isRunnable_corres]) apply simp apply (rule corres_split) apply clarsimp apply (rule corres_when[OF refl]) apply (rule tcbSchedEnqueue_corres) apply (rule corres_when[OF refl]) apply (rule rescheduleRequired_corres) apply ((wp hoare_drop_imps hoare_vcg_conj_lift | clarsimp| assumption)+)[5] apply clarsimp apply (rule_tac Q="\<lambda>_. valid_objs' and valid_queues' and valid_queues and
          (\<lambda>s. sch_act_wf (ksSchedulerAction s) s) and tcb_at' tptr"
          in hoare_strengthen_post[rotated]) apply (auto simp: invs'_def valid_state'_def sch_act_wf_weak st_tcb_at'_def o_def)[1] apply (wp threadSet_valid_objs' threadSet_valid_queues'_no_state
          threadSet_valid_queues_no_state
          threadSet_pred_tcb_no_state | simp)+ apply (rule_tac Q = "\<lambda>r s. invs' s \<and> (\<forall>p. tptr \<notin> set (ksReadyQueues s p)) \<and> sch_act_simple s
        \<and>  tcb_at' tptr s" in hoare_strengthen_post[rotated]) apply (clarsimp simp:invs'_def valid_state'_def valid_pspace'_def sch_act_simple_def) apply (clarsimp simp:valid_tcb'_def) apply (drule(1) bspec) apply (clarsimp simp:tcb_cte_cases_def) apply fastforce apply (wp hoare_vcg_all_lift Tcb_R.tcbSchedDequeue_not_in_queue)+ apply clarsimp apply (frule tcb_at_is_etcb_at) apply simp+ apply (auto elim: tcb_at_is_etcb_at valid_objs'_maxDomain valid_objs'_maxPriority pred_tcb'_weakenE
               simp: valid_sched_def valid_sched_action_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. corres dc (valid_etcbs and valid_sched and tcb_at tptr) (invs' and sch_act_simple and tcb_at' tptr and (\<lambda>s. new_dom \<le> maxDomain)) (set_domain tptr new_dom) (setDomain tptr new_dom) proof (prove)
goal (1 subgoal):
 1. new_dom \<le> maxDomain \<Longrightarrow> corres dc (valid_etcbs and valid_sched and tcb_at tptr) (invs' and sch_act_simple and tcb_at' tptr) (set_domain tptr new_dom) (setDomain tptr new_dom) proof (prove)
goal (1 subgoal):
 1. new_dom \<le> maxDomain \<Longrightarrow> corres dc (valid_etcbs and valid_sched and tcb_at tptr) (invs' and sch_act_simple and tcb_at' tptr) (do cur <- gets cur_thread;
y <- tcb_sched_action tcb_sched_dequeue tptr;
y <- ethread_set (tcb_domain_update (\<lambda>_. new_dom)) tptr;
ts <- get_thread_state tptr;
y <- when (runnable ts) (tcb_sched_action tcb_sched_enqueue tptr);
when (tptr = cur) reschedule_required
od) (do curThread <- getCurThread;
y <- tcbSchedDequeue tptr;
y <- threadSet (tcbDomain_update (\<lambda>_. new_dom)) tptr;
runnable <- isRunnable tptr;
y <- when runnable (tcbSchedEnqueue tptr);
when (tptr = curThread) rescheduleRequired
od) proof (prove)
goal (3 subgoals):
 1. new_dom \<le> maxDomain \<Longrightarrow> corres dc ?Q2 ?Q'2 (do cur <- gets cur_thread;
y <- tcb_sched_action tcb_sched_dequeue tptr;
y <- ethread_set (tcb_domain_update (\<lambda>_. new_dom)) tptr;
ts <- get_thread_state tptr;
y <- when (runnable ts) (tcb_sched_action tcb_sched_enqueue tptr);
when (tptr = cur) reschedule_required
od) (do curThread <- getCurThread;
y <- tcbSchedDequeue tptr;
y <- threadSet (tcbDomain_update (\<lambda>_. new_dom)) tptr;
runnable <- isRunnable tptr;
y <- when runnable (tcbSchedEnqueue tptr);
when (tptr = curThread) rescheduleRequired
od)
 2. \<And>s. \<lbrakk>new_dom \<le> maxDomain; (valid_etcbs and valid_sched and tcb_at tptr) s\<rbrakk> \<Longrightarrow> ?Q2 s
 3. \<And>s. \<lbrakk>new_dom \<le> maxDomain; (invs' and sch_act_simple and tcb_at' tptr) s\<rbrakk> \<Longrightarrow> ?Q'2 s proof (prove)
goal (5 subgoals):
 1. \<And>cur curThread. \<lbrakk>new_dom \<le> maxDomain; cur = curThread\<rbrakk> \<Longrightarrow> corres dc (?R6 cur) (?R'6 curThread) (do y <- tcb_sched_action tcb_sched_dequeue tptr;
y <- ethread_set (tcb_domain_update (\<lambda>_. new_dom)) tptr;
ts <- get_thread_state tptr;
y <- when (runnable ts) (tcb_sched_action tcb_sched_enqueue tptr);
when (tptr = cur) reschedule_required
od) (do y <- tcbSchedDequeue tptr;
y <- threadSet (tcbDomain_update (\<lambda>_. new_dom)) tptr;
runnable <- isRunnable tptr;
y <- when runnable (tcbSchedEnqueue tptr);
when (tptr = curThread) rescheduleRequired
od)
 2. new_dom \<le> maxDomain \<Longrightarrow> \<lbrace>?Q6\<rbrace> gets cur_thread \<lbrace>?R6\<rbrace>
 3. new_dom \<le> maxDomain \<Longrightarrow> \<lbrace>?Q'6\<rbrace> getCurThread \<lbrace>?R'6\<rbrace>
 4. \<And>s. \<lbrakk>new_dom \<le> maxDomain; (valid_etcbs and valid_sched and tcb_at tptr) s\<rbrakk> \<Longrightarrow> ((\<lambda>_. True) and ?Q6) s
 5. \<And>s. \<lbrakk>new_dom \<le> maxDomain; (invs' and sch_act_simple and tcb_at' tptr) s\<rbrakk> \<Longrightarrow> ((\<lambda>_. True) and ?Q'6) s proof (prove)
goal (7 subgoals):
 1. \<And>cur curThread y ya. \<lbrakk>new_dom \<le> maxDomain; cur = curThread; dc y ya\<rbrakk> \<Longrightarrow> corres dc (?R10 cur curThread y) (?R'10 cur curThread ya) (do y <- ethread_set (tcb_domain_update (\<lambda>_. new_dom)) tptr;
ts <- get_thread_state tptr;
y <- when (runnable ts) (tcb_sched_action tcb_sched_enqueue tptr);
when (tptr = cur) reschedule_required
od) (do y <- threadSet (tcbDomain_update (\<lambda>_. new_dom)) tptr;
runnable <- isRunnable tptr;
y <- when runnable (tcbSchedEnqueue tptr);
when (tptr = curThread) rescheduleRequired
od)
 2. \<And>cur curThread. \<lbrakk>new_dom \<le> maxDomain; cur = curThread\<rbrakk> \<Longrightarrow> \<lbrace>?Q13 cur\<rbrace> tcb_sched_action tcb_sched_dequeue tptr \<lbrace>?R10 cur curThread\<rbrace>
 3. \<And>cur curThread. \<lbrakk>new_dom \<le> maxDomain; cur = curThread\<rbrakk> \<Longrightarrow> \<lbrace>?Q'15 curThread\<rbrace> tcbSchedDequeue tptr \<lbrace>?R'10 cur curThread\<rbrace>
 4. new_dom \<le> maxDomain \<Longrightarrow> \<lbrace>?Q6\<rbrace> gets cur_thread \<lbrace>\<lambda>cur. is_etcb_at tptr and ?Q13 cur\<rbrace>
 5. new_dom \<le> maxDomain \<Longrightarrow> \<lbrace>?Q'6\<rbrace> getCurThread \<lbrace>\<lambda>curThread. tcb_at' tptr and Invariants_H.valid_queues and ?Q'15 curThread\<rbrace>
 6. \<And>s. \<lbrakk>new_dom \<le> maxDomain; (valid_etcbs and valid_sched and tcb_at tptr) s\<rbrakk> \<Longrightarrow> ((\<lambda>_. True) and ?Q6) s
 7. \<And>s. \<lbrakk>new_dom \<le> maxDomain; (invs' and sch_act_simple and tcb_at' tptr) s\<rbrakk> \<Longrightarrow> ((\<lambda>_. True) and ?Q'6) s proof (prove)
goal (10 subgoals):
 1. \<And>cur curThread y ya. \<lbrakk>new_dom \<le> maxDomain; cur = curThread; dc y ya\<rbrakk> \<Longrightarrow> corres (?r'19 cur curThread y ya) (?P20 cur curThread y) (?P'22 cur curThread ya) (ethread_set (tcb_domain_update (\<lambda>_. new_dom)) tptr) (threadSet (tcbDomain_update (\<lambda>_. new_dom)) tptr)
 2. \<And>cur curThread y ya yb yc. \<lbrakk>new_dom \<le> maxDomain; cur = curThread; dc y ya; ?r'19 cur curThread y ya yb yc\<rbrakk> \<Longrightarrow> corres dc (?R19 cur curThread y ya yb) (?R'19 cur curThread y ya yc) (do ts <- get_thread_state tptr;
y <- when (runnable ts) (tcb_sched_action tcb_sched_enqueue tptr);
when (tptr = cur) reschedule_required
od) (do runnable <- isRunnable tptr;
y <- when runnable (tcbSchedEnqueue tptr);
when (tptr = curThread) rescheduleRequired
od)
 3. \<And>cur curThread y ya. \<lbrakk>new_dom \<le> maxDomain; cur = curThread; dc y ya\<rbrakk> \<Longrightarrow> \<lbrace>?Q21 cur curThread y\<rbrace> ethread_set (tcb_domain_update (\<lambda>_. new_dom)) tptr \<lbrace>?R19 cur curThread y ya\<rbrace>
 4. \<And>cur curThread y ya. \<lbrakk>new_dom \<le> maxDomain; cur = curThread; dc y ya\<rbrakk> \<Longrightarrow> \<lbrace>?Q'23 cur curThread ya\<rbrace> threadSet (tcbDomain_update (\<lambda>_. new_dom)) tptr \<lbrace>?R'19 cur curThread y ya\<rbrace>
 5. \<And>cur curThread. \<lbrakk>new_dom \<le> maxDomain; cur = curThread\<rbrakk> \<Longrightarrow> \<lbrace>?Q13 cur\<rbrace> tcb_sched_action tcb_sched_dequeue tptr \<lbrace>\<lambda>y. ?P20 cur curThread y and ?Q21 cur curThread y\<rbrace>
 6. \<And>cur curThread. \<lbrakk>new_dom \<le> maxDomain; cur = curThread\<rbrakk> \<Longrightarrow> \<lbrace>?Q'15 curThread\<rbrace> tcbSchedDequeue tptr \<lbrace>\<lambda>ya. ?P'22 cur curThread ya and ?Q'23 cur curThread ya\<rbrace>
 7. new_dom \<le> maxDomain \<Longrightarrow> \<lbrace>?Q6\<rbrace> gets cur_thread \<lbrace>\<lambda>cur. is_etcb_at tptr and ?Q13 cur\<rbrace>
 8. new_dom \<le> maxDomain \<Longrightarrow> \<lbrace>?Q'6\<rbrace> getCurThread \<lbrace>\<lambda>curThread. tcb_at' tptr and Invariants_H.valid_queues and ?Q'15 curThread\<rbrace>
 9. \<And>s. \<lbrakk>new_dom \<le> maxDomain; (valid_etcbs and valid_sched and tcb_at tptr) s\<rbrakk> \<Longrightarrow> ((\<lambda>_. True) and ?Q6) s
 10. \<And>s. \<lbrakk>new_dom \<le> maxDomain; (invs' and sch_act_simple and tcb_at' tptr) s\<rbrakk> \<Longrightarrow> ((\<lambda>_. True) and ?Q'6) s proof (prove)
goal (10 subgoals):
 1. \<And>cur curThread etcb tcb'. \<lbrakk>new_dom \<le> maxDomain; cur = curThread; etcb_relation etcb tcb'\<rbrakk> \<Longrightarrow> etcb_relation (etcb\<lparr>tcb_domain := new_dom\<rparr>) (tcbDomain_update (\<lambda>_. new_dom) tcb')
 2. \<And>cur curThread y ya yb yc. \<lbrakk>new_dom \<le> maxDomain; cur = curThread; dc y ya; dc yb yc\<rbrakk> \<Longrightarrow> corres dc (?R19 cur curThread y ya yb) (?R'19 cur curThread y ya yc) (do ts <- get_thread_state tptr;
y <- when (runnable ts) (tcb_sched_action tcb_sched_enqueue tptr);
when (tptr = cur) reschedule_required
od) (do runnable <- isRunnable tptr;
y <- when runnable (tcbSchedEnqueue tptr);
when (tptr = curThread) rescheduleRequired
od)
 3. \<And>cur curThread y ya. \<lbrakk>new_dom \<le> maxDomain; cur = curThread; dc y ya\<rbrakk> \<Longrightarrow> \<lbrace>?Q21 cur curThread y\<rbrace> ethread_set (tcb_domain_update (\<lambda>_. new_dom)) tptr \<lbrace>?R19 cur curThread y ya\<rbrace>
 4. \<And>cur curThread y ya. \<lbrakk>new_dom \<le> maxDomain; cur = curThread; dc y ya\<rbrakk> \<Longrightarrow> \<lbrace>?Q'23 cur curThread ya\<rbrace> threadSet (tcbDomain_update (\<lambda>_. new_dom)) tptr \<lbrace>?R'19 cur curThread y ya\<rbrace>
 5. \<And>cur curThread. \<lbrakk>new_dom \<le> maxDomain; cur = curThread\<rbrakk> \<Longrightarrow> \<lbrace>?Q13 cur\<rbrace> tcb_sched_action tcb_sched_dequeue tptr \<lbrace>\<lambda>y. tcb_at tptr and valid_etcbs and ?Q21 cur curThread y\<rbrace>
 6. \<And>cur curThread. \<lbrakk>new_dom \<le> maxDomain; cur = curThread\<rbrakk> \<Longrightarrow> \<lbrace>?Q'15 curThread\<rbrace> tcbSchedDequeue tptr \<lbrace>\<lambda>ya. tcb_at' tptr and ?Q'23 cur curThread ya\<rbrace>
 7. new_dom \<le> maxDomain \<Longrightarrow> \<lbrace>?Q6\<rbrace> gets cur_thread \<lbrace>\<lambda>cur. is_etcb_at tptr and ?Q13 cur\<rbrace>
 8. new_dom \<le> maxDomain \<Longrightarrow> \<lbrace>?Q'6\<rbrace> getCurThread \<lbrace>\<lambda>curThread. tcb_at' tptr and Invariants_H.valid_queues and ?Q'15 curThread\<rbrace>
 9. \<And>s. \<lbrakk>new_dom \<le> maxDomain; (valid_etcbs and valid_sched and tcb_at tptr) s\<rbrakk> \<Longrightarrow> ((\<lambda>_. True) and ?Q6) s
 10. \<And>s. \<lbrakk>new_dom \<le> maxDomain; (invs' and sch_act_simple and tcb_at' tptr) s\<rbrakk> \<Longrightarrow> ((\<lambda>_. True) and ?Q'6) s proof (prove)
goal (9 subgoals):
 1. \<And>cur curThread y ya yb yc. \<lbrakk>new_dom \<le> maxDomain; cur = curThread; dc y ya; dc yb yc\<rbrakk> \<Longrightarrow> corres dc (?R19 cur curThread y ya yb) (?R'19 cur curThread y ya yc) (do ts <- get_thread_state tptr;
y <- when (runnable ts) (tcb_sched_action tcb_sched_enqueue tptr);
when (tptr = cur) reschedule_required
od) (do runnable <- isRunnable tptr;
y <- when runnable (tcbSchedEnqueue tptr);
when (tptr = curThread) rescheduleRequired
od)
 2. \<And>cur curThread y ya. \<lbrakk>new_dom \<le> maxDomain; cur = curThread; dc y ya\<rbrakk> \<Longrightarrow> \<lbrace>?Q21 cur curThread y\<rbrace> ethread_set (tcb_domain_update (\<lambda>_. new_dom)) tptr \<lbrace>?R19 cur curThread y ya\<rbrace>
 3. \<And>cur curThread y ya. \<lbrakk>new_dom \<le> maxDomain; cur = curThread; dc y ya\<rbrakk> \<Longrightarrow> \<lbrace>?Q'23 cur curThread ya\<rbrace> threadSet (tcbDomain_update (\<lambda>_. new_dom)) tptr \<lbrace>?R'19 cur curThread y ya\<rbrace>
 4. \<And>cur curThread. \<lbrakk>new_dom \<le> maxDomain; cur = curThread\<rbrakk> \<Longrightarrow> \<lbrace>?Q13 cur\<rbrace> tcb_sched_action tcb_sched_dequeue tptr \<lbrace>\<lambda>y. tcb_at tptr and valid_etcbs and ?Q21 cur curThread y\<rbrace>
 5. \<And>cur curThread. \<lbrakk>new_dom \<le> maxDomain; cur = curThread\<rbrakk> \<Longrightarrow> \<lbrace>?Q'15 curThread\<rbrace> tcbSchedDequeue tptr \<lbrace>\<lambda>ya. tcb_at' tptr and ?Q'23 cur curThread ya\<rbrace>
 6. new_dom \<le> maxDomain \<Longrightarrow> \<lbrace>?Q6\<rbrace> gets cur_thread \<lbrace>\<lambda>cur. is_etcb_at tptr and ?Q13 cur\<rbrace>
 7. new_dom \<le> maxDomain \<Longrightarrow> \<lbrace>?Q'6\<rbrace> getCurThread \<lbrace>\<lambda>curThread. tcb_at' tptr and Invariants_H.valid_queues and ?Q'15 curThread\<rbrace>
 8. \<And>s. \<lbrakk>new_dom \<le> maxDomain; (valid_etcbs and valid_sched and tcb_at tptr) s\<rbrakk> \<Longrightarrow> ((\<lambda>_. True) and ?Q6) s
 9. \<And>s. \<lbrakk>new_dom \<le> maxDomain; (invs' and sch_act_simple and tcb_at' tptr) s\<rbrakk> \<Longrightarrow> ((\<lambda>_. True) and ?Q'6) s proof (prove)
goal (11 subgoals):
 1. \<And>cur curThread y ya yb yc ts runnablea. \<lbrakk>new_dom \<le> maxDomain; cur = curThread; dc y ya; dc yb yc; runnable ts = runnablea\<rbrakk> \<Longrightarrow> corres dc (?R54 cur curThread y ya yb yc ts) (?R'54 cur curThread y ya yb yc runnablea) (do y <- when (runnable ts) (tcb_sched_action tcb_sched_enqueue tptr);
when (tptr = cur) reschedule_required
od) (do y <- when runnablea (tcbSchedEnqueue tptr);
when (tptr = curThread) rescheduleRequired
od)
 2. \<And>cur curThread y ya yb yc. \<lbrakk>new_dom \<le> maxDomain; cur = curThread; dc y ya; dc yb yc\<rbrakk> \<Longrightarrow> \<lbrace>?Q57 cur curThread y ya yb\<rbrace> get_thread_state tptr \<lbrace>?R54 cur curThread y ya yb yc\<rbrace>
 3. \<And>cur curThread y ya yb yc. \<lbrakk>new_dom \<le> maxDomain; cur = curThread; dc y ya; dc yb yc\<rbrakk> \<Longrightarrow> \<lbrace>?Q'59 cur curThread y ya yc\<rbrace> isRunnable tptr \<lbrace>?R'54 cur curThread y ya yb yc\<rbrace>
 4. \<And>cur curThread y ya. \<lbrakk>new_dom \<le> maxDomain; cur = curThread; dc y ya\<rbrakk> \<Longrightarrow> \<lbrace>?Q21 cur curThread y\<rbrace> ethread_set (tcb_domain_update (\<lambda>_. new_dom)) tptr \<lbrace>\<lambda>yb. tcb_at tptr and ?Q57 cur curThread y ya yb\<rbrace>
 5. \<And>cur curThread y ya. \<lbrakk>new_dom \<le> maxDomain; cur = curThread; dc y ya\<rbrakk> \<Longrightarrow> \<lbrace>?Q'23 cur curThread ya\<rbrace> threadSet (tcbDomain_update (\<lambda>_. new_dom)) tptr \<lbrace>\<lambda>yc. tcb_at' tptr and ?Q'59 cur curThread y ya yc\<rbrace>
 6. \<And>cur curThread. \<lbrakk>new_dom \<le> maxDomain; cur = curThread\<rbrakk> \<Longrightarrow> \<lbrace>?Q13 cur\<rbrace> tcb_sched_action tcb_sched_dequeue tptr \<lbrace>\<lambda>y. tcb_at tptr and valid_etcbs and ?Q21 cur curThread y\<rbrace>
 7. \<And>cur curThread. \<lbrakk>new_dom \<le> maxDomain; cur = curThread\<rbrakk> \<Longrightarrow> \<lbrace>?Q'15 curThread\<rbrace> tcbSchedDequeue tptr \<lbrace>\<lambda>ya. tcb_at' tptr and ?Q'23 cur curThread ya\<rbrace>
 8. new_dom \<le> maxDomain \<Longrightarrow> \<lbrace>?Q6\<rbrace> gets cur_thread \<lbrace>\<lambda>cur. is_etcb_at tptr and ?Q13 cur\<rbrace>
 9. new_dom \<le> maxDomain \<Longrightarrow> \<lbrace>?Q'6\<rbrace> getCurThread \<lbrace>\<lambda>curThread. tcb_at' tptr and Invariants_H.valid_queues and ?Q'15 curThread\<rbrace>
 10. \<And>s. \<lbrakk>new_dom \<le> maxDomain; (valid_etcbs and valid_sched and tcb_at tptr) s\<rbrakk> \<Longrightarrow> ((\<lambda>_. True) and ?Q6) s
A total of 11 subgoals... proof (prove)
goal (11 subgoals):
 1. \<And>cur curThread ts runnablea. \<lbrakk>new_dom \<le> maxDomain; cur = curThread; runnable ts = runnablea\<rbrakk> \<Longrightarrow> corres dc (?R54 curThread curThread () () () () ts) (?R'54 curThread curThread () () () () runnablea) (do y <- when runnablea (tcb_sched_action tcb_sched_enqueue tptr);
when (tptr = curThread) reschedule_required
od) (do y <- when runnablea (tcbSchedEnqueue tptr);
when (tptr = curThread) rescheduleRequired
od)
 2. \<And>cur curThread y ya yb yc. \<lbrakk>new_dom \<le> maxDomain; cur = curThread; dc y ya; dc yb yc\<rbrakk> \<Longrightarrow> \<lbrace>?Q57 cur curThread y ya yb\<rbrace> get_thread_state tptr \<lbrace>?R54 cur curThread y ya yb yc\<rbrace>
 3. \<And>cur curThread y ya yb yc. \<lbrakk>new_dom \<le> maxDomain; cur = curThread; dc y ya; dc yb yc\<rbrakk> \<Longrightarrow> \<lbrace>?Q'59 cur curThread y ya yc\<rbrace> isRunnable tptr \<lbrace>?R'54 cur curThread y ya yb yc\<rbrace>
 4. \<And>cur curThread y ya. \<lbrakk>new_dom \<le> maxDomain; cur = curThread; dc y ya\<rbrakk> \<Longrightarrow> \<lbrace>?Q21 cur curThread y\<rbrace> ethread_set (tcb_domain_update (\<lambda>_. new_dom)) tptr \<lbrace>\<lambda>yb. tcb_at tptr and ?Q57 cur curThread y ya yb\<rbrace>
 5. \<And>cur curThread y ya. \<lbrakk>new_dom \<le> maxDomain; cur = curThread; dc y ya\<rbrakk> \<Longrightarrow> \<lbrace>?Q'23 cur curThread ya\<rbrace> threadSet (tcbDomain_update (\<lambda>_. new_dom)) tptr \<lbrace>\<lambda>yc. tcb_at' tptr and ?Q'59 cur curThread y ya yc\<rbrace>
 6. \<And>cur curThread. \<lbrakk>new_dom \<le> maxDomain; cur = curThread\<rbrakk> \<Longrightarrow> \<lbrace>?Q13 cur\<rbrace> tcb_sched_action tcb_sched_dequeue tptr \<lbrace>\<lambda>y. tcb_at tptr and valid_etcbs and ?Q21 cur curThread y\<rbrace>
 7. \<And>cur curThread. \<lbrakk>new_dom \<le> maxDomain; cur = curThread\<rbrakk> \<Longrightarrow> \<lbrace>?Q'15 curThread\<rbrace> tcbSchedDequeue tptr \<lbrace>\<lambda>ya. tcb_at' tptr and ?Q'23 cur curThread ya\<rbrace>
 8. new_dom \<le> maxDomain \<Longrightarrow> \<lbrace>?Q6\<rbrace> gets cur_thread \<lbrace>\<lambda>cur. is_etcb_at tptr and ?Q13 cur\<rbrace>
 9. new_dom \<le> maxDomain \<Longrightarrow> \<lbrace>?Q'6\<rbrace> getCurThread \<lbrace>\<lambda>curThread. tcb_at' tptr and Invariants_H.valid_queues and ?Q'15 curThread\<rbrace>
 10. \<And>s. \<lbrakk>new_dom \<le> maxDomain; (valid_etcbs and valid_sched and tcb_at tptr) s\<rbrakk> \<Longrightarrow> ((\<lambda>_. True) and ?Q6) s
A total of 11 subgoals... proof (prove)
goal (14 subgoals):
 1. \<And>cur curThread ts runnablea. \<lbrakk>new_dom \<le> maxDomain; cur = curThread; runnable ts = runnablea\<rbrakk> \<Longrightarrow> corres (?r'63 cur curThread ts runnablea) (?P74 curThread curThread () () () () ts) (?P'70 curThread curThread () () () () runnablea) (when runnablea (tcb_sched_action tcb_sched_enqueue tptr)) (when runnablea (tcbSchedEnqueue tptr))
 2. \<And>cur curThread ts runnablea y ya. \<lbrakk>new_dom \<le> maxDomain; cur = curThread; runnable ts = runnablea; ?r'63 cur curThread ts runnablea y ya\<rbrakk> \<Longrightarrow> corres dc (?R63 cur curThread ts runnablea y) (?R'63 cur curThread ts runnablea ya) (when (tptr = curThread) reschedule_required) (when (tptr = curThread) rescheduleRequired)
 3. \<And>cur curThread ts runnablea. \<lbrakk>new_dom \<le> maxDomain; cur = curThread; runnable ts = runnablea\<rbrakk> \<Longrightarrow> \<lbrace>?Q72 curThread curThread () () () () ts\<rbrace> when runnablea (tcb_sched_action tcb_sched_enqueue tptr) \<lbrace>?R63 cur curThread ts runnablea\<rbrace>
 4. \<And>cur curThread ts runnablea. \<lbrakk>new_dom \<le> maxDomain; cur = curThread; runnable ts = runnablea\<rbrakk> \<Longrightarrow> \<lbrace>?Q'68 curThread curThread () () () () runnablea\<rbrace> when runnablea (tcbSchedEnqueue tptr) \<lbrace>?R'63 cur curThread ts runnablea\<rbrace>
 5. \<And>cur curThread y ya yb yc. \<lbrakk>new_dom \<le> maxDomain; cur = curThread; dc y ya; dc yb yc\<rbrakk> \<Longrightarrow> \<lbrace>?Q57 cur curThread y ya yb\<rbrace> get_thread_state tptr \<lbrace>\<lambda>a. ?P74 cur curThread y ya yb yc a and ?Q72 cur curThread y ya yb yc a\<rbrace>
 6. \<And>cur curThread y ya yb yc. \<lbrakk>new_dom \<le> maxDomain; cur = curThread; dc y ya; dc yb yc\<rbrakk> \<Longrightarrow> \<lbrace>?Q'59 cur curThread y ya yc\<rbrace> isRunnable tptr \<lbrace>\<lambda>a. ?P'70 cur curThread y ya yb yc a and ?Q'68 cur curThread y ya yb yc a\<rbrace>
 7. \<And>cur curThread y ya. \<lbrakk>new_dom \<le> maxDomain; cur = curThread; dc y ya\<rbrakk> \<Longrightarrow> \<lbrace>?Q21 cur curThread y\<rbrace> ethread_set (tcb_domain_update (\<lambda>_. new_dom)) tptr \<lbrace>\<lambda>yb. tcb_at tptr and ?Q57 cur curThread y ya yb\<rbrace>
 8. \<And>cur curThread y ya. \<lbrakk>new_dom \<le> maxDomain; cur = curThread; dc y ya\<rbrakk> \<Longrightarrow> \<lbrace>?Q'23 cur curThread ya\<rbrace> threadSet (tcbDomain_update (\<lambda>_. new_dom)) tptr \<lbrace>\<lambda>yc. tcb_at' tptr and ?Q'59 cur curThread y ya yc\<rbrace>
 9. \<And>cur curThread. \<lbrakk>new_dom \<le> maxDomain; cur = curThread\<rbrakk> \<Longrightarrow> \<lbrace>?Q13 cur\<rbrace> tcb_sched_action tcb_sched_dequeue tptr \<lbrace>\<lambda>y. tcb_at tptr and valid_etcbs and ?Q21 cur curThread y\<rbrace>
 10. \<And>cur curThread. \<lbrakk>new_dom \<le> maxDomain; cur = curThread\<rbrakk> \<Longrightarrow> \<lbrace>?Q'15 curThread\<rbrace> tcbSchedDequeue tptr \<lbrace>\<lambda>ya. tcb_at' tptr and ?Q'23 cur curThread ya\<rbrace>
A total of 14 subgoals... proof (prove)
goal (14 subgoals):
 1. \<And>curThread ts. new_dom \<le> maxDomain \<Longrightarrow> corres (?r'63 curThread curThread ts (runnable ts)) (?P74 curThread curThread () () () () ts) (?P'70 curThread curThread () () () () (runnable ts)) (when (runnable ts) (tcb_sched_action tcb_sched_enqueue tptr)) (when (runnable ts) (tcbSchedEnqueue tptr))
 2. \<And>cur curThread ts runnablea y ya. \<lbrakk>new_dom \<le> maxDomain; cur = curThread; runnable ts = runnablea; ?r'63 cur curThread ts runnablea y ya\<rbrakk> \<Longrightarrow> corres dc (?R63 cur curThread ts runnablea y) (?R'63 cur curThread ts runnablea ya) (when (tptr = curThread) reschedule_required) (when (tptr = curThread) rescheduleRequired)
 3. \<And>cur curThread ts runnablea. \<lbrakk>new_dom \<le> maxDomain; cur = curThread; runnable ts = runnablea\<rbrakk> \<Longrightarrow> \<lbrace>?Q72 curThread curThread () () () () ts\<rbrace> when runnablea (tcb_sched_action tcb_sched_enqueue tptr) \<lbrace>?R63 cur curThread ts runnablea\<rbrace>
 4. \<And>cur curThread ts runnablea. \<lbrakk>new_dom \<le> maxDomain; cur = curThread; runnable ts = runnablea\<rbrakk> \<Longrightarrow> \<lbrace>?Q'68 curThread curThread () () () () runnablea\<rbrace> when runnablea (tcbSchedEnqueue tptr) \<lbrace>?R'63 cur curThread ts runnablea\<rbrace>
 5. \<And>cur curThread y ya yb yc. \<lbrakk>new_dom \<le> maxDomain; cur = curThread; dc y ya; dc yb yc\<rbrakk> \<Longrightarrow> \<lbrace>?Q57 cur curThread y ya yb\<rbrace> get_thread_state tptr \<lbrace>\<lambda>a. ?P74 cur curThread y ya yb yc a and ?Q72 cur curThread y ya yb yc a\<rbrace>
 6. \<And>cur curThread y ya yb yc. \<lbrakk>new_dom \<le> maxDomain; cur = curThread; dc y ya; dc yb yc\<rbrakk> \<Longrightarrow> \<lbrace>?Q'59 cur curThread y ya yc\<rbrace> isRunnable tptr \<lbrace>\<lambda>a. ?P'70 cur curThread y ya yb yc a and ?Q'68 cur curThread y ya yb yc a\<rbrace>
 7. \<And>cur curThread y ya. \<lbrakk>new_dom \<le> maxDomain; cur = curThread; dc y ya\<rbrakk> \<Longrightarrow> \<lbrace>?Q21 cur curThread y\<rbrace> ethread_set (tcb_domain_update (\<lambda>_. new_dom)) tptr \<lbrace>\<lambda>yb. tcb_at tptr and ?Q57 cur curThread y ya yb\<rbrace>
 8. \<And>cur curThread y ya. \<lbrakk>new_dom \<le> maxDomain; cur = curThread; dc y ya\<rbrakk> \<Longrightarrow> \<lbrace>?Q'23 cur curThread ya\<rbrace> threadSet (tcbDomain_update (\<lambda>_. new_dom)) tptr \<lbrace>\<lambda>yc. tcb_at' tptr and ?Q'59 cur curThread y ya yc\<rbrace>
 9. \<And>cur curThread. \<lbrakk>new_dom \<le> maxDomain; cur = curThread\<rbrakk> \<Longrightarrow> \<lbrace>?Q13 cur\<rbrace> tcb_sched_action tcb_sched_dequeue tptr \<lbrace>\<lambda>y. tcb_at tptr and valid_etcbs and ?Q21 cur curThread y\<rbrace>
 10. \<And>cur curThread. \<lbrakk>new_dom \<le> maxDomain; cur = curThread\<rbrakk> \<Longrightarrow> \<lbrace>?Q'15 curThread\<rbrace> tcbSchedDequeue tptr \<lbrace>\<lambda>ya. tcb_at' tptr and ?Q'23 cur curThread ya\<rbrace>
A total of 14 subgoals... proof (prove)
goal (14 subgoals):
 1. \<And>curThread ts. new_dom \<le> maxDomain \<Longrightarrow> corres dc (?P87 curThread curThread () () () () ts) (?P'86 curThread curThread () () () () (runnable ts)) (tcb_sched_action tcb_sched_enqueue tptr) (tcbSchedEnqueue tptr)
 2. \<And>cur curThread ts runnablea y ya. \<lbrakk>new_dom \<le> maxDomain; cur = curThread; runnable ts = runnablea; dc y ya\<rbrakk> \<Longrightarrow> corres dc (?R63 cur curThread ts runnablea y) (?R'63 cur curThread ts runnablea ya) (when (tptr = curThread) reschedule_required) (when (tptr = curThread) rescheduleRequired)
 3. \<And>cur curThread ts runnablea. \<lbrakk>new_dom \<le> maxDomain; cur = curThread; runnable ts = runnablea\<rbrakk> \<Longrightarrow> \<lbrace>?Q72 curThread curThread () () () () ts\<rbrace> when runnablea (tcb_sched_action tcb_sched_enqueue tptr) \<lbrace>?R63 cur curThread ts runnablea\<rbrace>
 4. \<And>cur curThread ts runnablea. \<lbrakk>new_dom \<le> maxDomain; cur = curThread; runnable ts = runnablea\<rbrakk> \<Longrightarrow> \<lbrace>?Q'68 curThread curThread () () () () runnablea\<rbrace> when runnablea (tcbSchedEnqueue tptr) \<lbrace>?R'63 cur curThread ts runnablea\<rbrace>
 5. \<And>cur curThread y ya yb yc. \<lbrakk>new_dom \<le> maxDomain; cur = curThread; dc y ya; dc yb yc\<rbrakk> \<Longrightarrow> \<lbrace>?Q57 cur curThread y ya yb\<rbrace> get_thread_state tptr \<lbrace>\<lambda>a. (\<lambda>b. runnable a \<longrightarrow> ?P87 cur curThread y ya yb yc a b) and ?Q72 cur curThread y ya yb yc a\<rbrace>
 6. \<And>cur curThread y ya yb yc. \<lbrakk>new_dom \<le> maxDomain; cur = curThread; dc y ya; dc yb yc\<rbrakk> \<Longrightarrow> \<lbrace>?Q'59 cur curThread y ya yc\<rbrace> isRunnable tptr \<lbrace>\<lambda>a. (\<lambda>b. a \<longrightarrow> ?P'86 cur curThread y ya yb yc a b) and ?Q'68 cur curThread y ya yb yc a\<rbrace>
 7. \<And>cur curThread y ya. \<lbrakk>new_dom \<le> maxDomain; cur = curThread; dc y ya\<rbrakk> \<Longrightarrow> \<lbrace>?Q21 cur curThread y\<rbrace> ethread_set (tcb_domain_update (\<lambda>_. new_dom)) tptr \<lbrace>\<lambda>yb. tcb_at tptr and ?Q57 cur curThread y ya yb\<rbrace>
 8. \<And>cur curThread y ya. \<lbrakk>new_dom \<le> maxDomain; cur = curThread; dc y ya\<rbrakk> \<Longrightarrow> \<lbrace>?Q'23 cur curThread ya\<rbrace> threadSet (tcbDomain_update (\<lambda>_. new_dom)) tptr \<lbrace>\<lambda>yc. tcb_at' tptr and ?Q'59 cur curThread y ya yc\<rbrace>
 9. \<And>cur curThread. \<lbrakk>new_dom \<le> maxDomain; cur = curThread\<rbrakk> \<Longrightarrow> \<lbrace>?Q13 cur\<rbrace> tcb_sched_action tcb_sched_dequeue tptr \<lbrace>\<lambda>y. tcb_at tptr and valid_etcbs and ?Q21 cur curThread y\<rbrace>
 10. \<And>cur curThread. \<lbrakk>new_dom \<le> maxDomain; cur = curThread\<rbrakk> \<Longrightarrow> \<lbrace>?Q'15 curThread\<rbrace> tcbSchedDequeue tptr \<lbrace>\<lambda>ya. tcb_at' tptr and ?Q'23 cur curThread ya\<rbrace>
A total of 14 subgoals... proof (prove)
goal (13 subgoals):
 1. \<And>cur curThread ts runnablea y ya. \<lbrakk>new_dom \<le> maxDomain; cur = curThread; runnable ts = runnablea; dc y ya\<rbrakk> \<Longrightarrow> corres dc (?R63 cur curThread ts runnablea y) (?R'63 cur curThread ts runnablea ya) (when (tptr = curThread) reschedule_required) (when (tptr = curThread) rescheduleRequired)
 2. \<And>cur curThread ts runnablea. \<lbrakk>new_dom \<le> maxDomain; cur = curThread; runnable ts = runnablea\<rbrakk> \<Longrightarrow> \<lbrace>?Q72 curThread curThread () () () () ts\<rbrace> when runnablea (tcb_sched_action tcb_sched_enqueue tptr) \<lbrace>?R63 cur curThread ts runnablea\<rbrace>
 3. \<And>cur curThread ts runnablea. \<lbrakk>new_dom \<le> maxDomain; cur = curThread; runnable ts = runnablea\<rbrakk> \<Longrightarrow> \<lbrace>?Q'68 curThread curThread () () () () runnablea\<rbrace> when runnablea (tcbSchedEnqueue tptr) \<lbrace>?R'63 cur curThread ts runnablea\<rbrace>
 4. \<And>cur curThread y ya yb yc. \<lbrakk>new_dom \<le> maxDomain; cur = curThread; dc y ya; dc yb yc\<rbrakk> \<Longrightarrow> \<lbrace>?Q57 cur curThread y ya yb\<rbrace> get_thread_state tptr \<lbrace>\<lambda>a. (\<lambda>b. runnable a \<longrightarrow> is_etcb_at tptr b) and ?Q72 cur curThread y ya yb yc a\<rbrace>
 5. \<And>cur curThread y ya yb yc. \<lbrakk>new_dom \<le> maxDomain; cur = curThread; dc y ya; dc yb yc\<rbrakk> \<Longrightarrow> \<lbrace>?Q'59 cur curThread y ya yc\<rbrace> isRunnable tptr \<lbrace>\<lambda>a. (\<lambda>b. a \<longrightarrow> (tcb_at' tptr and Invariants_H.valid_queues and valid_queues') b) and ?Q'68 cur curThread y ya yb yc a\<rbrace>
 6. \<And>cur curThread y ya. \<lbrakk>new_dom \<le> maxDomain; cur = curThread; dc y ya\<rbrakk> \<Longrightarrow> \<lbrace>?Q21 cur curThread y\<rbrace> ethread_set (tcb_domain_update (\<lambda>_. new_dom)) tptr \<lbrace>\<lambda>yb. tcb_at tptr and ?Q57 cur curThread y ya yb\<rbrace>
 7. \<And>cur curThread y ya. \<lbrakk>new_dom \<le> maxDomain; cur = curThread; dc y ya\<rbrakk> \<Longrightarrow> \<lbrace>?Q'23 cur curThread ya\<rbrace> threadSet (tcbDomain_update (\<lambda>_. new_dom)) tptr \<lbrace>\<lambda>yc. tcb_at' tptr and ?Q'59 cur curThread y ya yc\<rbrace>
 8. \<And>cur curThread. \<lbrakk>new_dom \<le> maxDomain; cur = curThread\<rbrakk> \<Longrightarrow> \<lbrace>?Q13 cur\<rbrace> tcb_sched_action tcb_sched_dequeue tptr \<lbrace>\<lambda>y. tcb_at tptr and valid_etcbs and ?Q21 cur curThread y\<rbrace>
 9. \<And>cur curThread. \<lbrakk>new_dom \<le> maxDomain; cur = curThread\<rbrakk> \<Longrightarrow> \<lbrace>?Q'15 curThread\<rbrace> tcbSchedDequeue tptr \<lbrace>\<lambda>ya. tcb_at' tptr and ?Q'23 cur curThread ya\<rbrace>
 10. new_dom \<le> maxDomain \<Longrightarrow> \<lbrace>?Q6\<rbrace> gets cur_thread \<lbrace>\<lambda>cur. is_etcb_at tptr and ?Q13 cur\<rbrace>
A total of 13 subgoals... proof (prove)
goal (13 subgoals):
 1. \<And>cur curThread ts runnablea y ya. \<lbrakk>new_dom \<le> maxDomain; cur = curThread; runnable ts = runnablea; dc y ya\<rbrakk> \<Longrightarrow> corres dc (?P93 cur curThread ts runnablea y) (?P'95 cur curThread ts runnablea ya) reschedule_required rescheduleRequired
 2. \<And>cur curThread ts runnablea. \<lbrakk>new_dom \<le> maxDomain; cur = curThread; runnable ts = runnablea\<rbrakk> \<Longrightarrow> \<lbrace>?Q72 curThread curThread () () () () ts\<rbrace> when runnablea (tcb_sched_action tcb_sched_enqueue tptr) \<lbrace>\<lambda>y x. tptr = curThread \<longrightarrow> ?P93 cur curThread ts runnablea y x\<rbrace>
 3. \<And>cur curThread ts runnablea. \<lbrakk>new_dom \<le> maxDomain; cur = curThread; runnable ts = runnablea\<rbrakk> \<Longrightarrow> \<lbrace>?Q'68 curThread curThread () () () () runnablea\<rbrace> when runnablea (tcbSchedEnqueue tptr) \<lbrace>\<lambda>ya x. tptr = curThread \<longrightarrow> ?P'95 cur curThread ts runnablea ya x\<rbrace>
 4. \<And>cur curThread y ya yb yc. \<lbrakk>new_dom \<le> maxDomain; cur = curThread; dc y ya; dc yb yc\<rbrakk> \<Longrightarrow> \<lbrace>?Q57 cur curThread y ya yb\<rbrace> get_thread_state tptr \<lbrace>\<lambda>a. (\<lambda>b. runnable a \<longrightarrow> is_etcb_at tptr b) and ?Q72 cur curThread y ya yb yc a\<rbrace>
 5. \<And>cur curThread y ya yb yc. \<lbrakk>new_dom \<le> maxDomain; cur = curThread; dc y ya; dc yb yc\<rbrakk> \<Longrightarrow> \<lbrace>?Q'59 cur curThread y ya yc\<rbrace> isRunnable tptr \<lbrace>\<lambda>a. (\<lambda>b. a \<longrightarrow> (tcb_at' tptr and Invariants_H.valid_queues and valid_queues') b) and ?Q'68 cur curThread y ya yb yc a\<rbrace>
 6. \<And>cur curThread y ya. \<lbrakk>new_dom \<le> maxDomain; cur = curThread; dc y ya\<rbrakk> \<Longrightarrow> \<lbrace>?Q21 cur curThread y\<rbrace> ethread_set (tcb_domain_update (\<lambda>_. new_dom)) tptr \<lbrace>\<lambda>yb. tcb_at tptr and ?Q57 cur curThread y ya yb\<rbrace>
 7. \<And>cur curThread y ya. \<lbrakk>new_dom \<le> maxDomain; cur = curThread; dc y ya\<rbrakk> \<Longrightarrow> \<lbrace>?Q'23 cur curThread ya\<rbrace> threadSet (tcbDomain_update (\<lambda>_. new_dom)) tptr \<lbrace>\<lambda>yc. tcb_at' tptr and ?Q'59 cur curThread y ya yc\<rbrace>
 8. \<And>cur curThread. \<lbrakk>new_dom \<le> maxDomain; cur = curThread\<rbrakk> \<Longrightarrow> \<lbrace>?Q13 cur\<rbrace> tcb_sched_action tcb_sched_dequeue tptr \<lbrace>\<lambda>y. tcb_at tptr and valid_etcbs and ?Q21 cur curThread y\<rbrace>
 9. \<And>cur curThread. \<lbrakk>new_dom \<le> maxDomain; cur = curThread\<rbrakk> \<Longrightarrow> \<lbrace>?Q'15 curThread\<rbrace> tcbSchedDequeue tptr \<lbrace>\<lambda>ya. tcb_at' tptr and ?Q'23 cur curThread ya\<rbrace>
 10. new_dom \<le> maxDomain \<Longrightarrow> \<lbrace>?Q6\<rbrace> gets cur_thread \<lbrace>\<lambda>cur. is_etcb_at tptr and ?Q13 cur\<rbrace>
A total of 13 subgoals... proof (prove)
goal (12 subgoals):
 1. \<And>cur curThread ts runnablea. \<lbrakk>new_dom \<le> maxDomain; cur = curThread; runnable ts = runnablea\<rbrakk> \<Longrightarrow> \<lbrace>?Q72 curThread curThread () () () () ts\<rbrace> when runnablea (tcb_sched_action tcb_sched_enqueue tptr) \<lbrace>\<lambda>y x. tptr = curThread \<longrightarrow> (weak_valid_sched_action and valid_etcbs) x\<rbrace>
 2. \<And>cur curThread ts runnablea. \<lbrakk>new_dom \<le> maxDomain; cur = curThread; runnable ts = runnablea\<rbrakk> \<Longrightarrow> \<lbrace>?Q'68 curThread curThread () () () () runnablea\<rbrace> when runnablea (tcbSchedEnqueue tptr) \<lbrace>\<lambda>ya x. tptr = curThread \<longrightarrow> (Invariants_H.valid_queues and valid_queues' and (\<lambda>s. weak_sch_act_wf (ksSchedulerAction s) s)) x\<rbrace>
 3. \<And>cur curThread y ya yb yc. \<lbrakk>new_dom \<le> maxDomain; cur = curThread; dc y ya; dc yb yc\<rbrakk> \<Longrightarrow> \<lbrace>?Q57 cur curThread y ya yb\<rbrace> get_thread_state tptr \<lbrace>\<lambda>a. (\<lambda>b. runnable a \<longrightarrow> is_etcb_at tptr b) and ?Q72 cur curThread y ya yb yc a\<rbrace>
 4. \<And>cur curThread y ya yb yc. \<lbrakk>new_dom \<le> maxDomain; cur = curThread; dc y ya; dc yb yc\<rbrakk> \<Longrightarrow> \<lbrace>?Q'59 cur curThread y ya yc\<rbrace> isRunnable tptr \<lbrace>\<lambda>a. (\<lambda>b. a \<longrightarrow> (tcb_at' tptr and Invariants_H.valid_queues and valid_queues') b) and ?Q'68 cur curThread y ya yb yc a\<rbrace>
 5. \<And>cur curThread y ya. \<lbrakk>new_dom \<le> maxDomain; cur = curThread; dc y ya\<rbrakk> \<Longrightarrow> \<lbrace>?Q21 cur curThread y\<rbrace> ethread_set (tcb_domain_update (\<lambda>_. new_dom)) tptr \<lbrace>\<lambda>yb. tcb_at tptr and ?Q57 cur curThread y ya yb\<rbrace>
 6. \<And>cur curThread y ya. \<lbrakk>new_dom \<le> maxDomain; cur = curThread; dc y ya\<rbrakk> \<Longrightarrow> \<lbrace>?Q'23 cur curThread ya\<rbrace> threadSet (tcbDomain_update (\<lambda>_. new_dom)) tptr \<lbrace>\<lambda>yc. tcb_at' tptr and ?Q'59 cur curThread y ya yc\<rbrace>
 7. \<And>cur curThread. \<lbrakk>new_dom \<le> maxDomain; cur = curThread\<rbrakk> \<Longrightarrow> \<lbrace>?Q13 cur\<rbrace> tcb_sched_action tcb_sched_dequeue tptr \<lbrace>\<lambda>y. tcb_at tptr and valid_etcbs and ?Q21 cur curThread y\<rbrace>
 8. \<And>cur curThread. \<lbrakk>new_dom \<le> maxDomain; cur = curThread\<rbrakk> \<Longrightarrow> \<lbrace>?Q'15 curThread\<rbrace> tcbSchedDequeue tptr \<lbrace>\<lambda>ya. tcb_at' tptr and ?Q'23 cur curThread ya\<rbrace>
 9. new_dom \<le> maxDomain \<Longrightarrow> \<lbrace>?Q6\<rbrace> gets cur_thread \<lbrace>\<lambda>cur. is_etcb_at tptr and ?Q13 cur\<rbrace>
 10. new_dom \<le> maxDomain \<Longrightarrow> \<lbrace>?Q'6\<rbrace> getCurThread \<lbrace>\<lambda>curThread. tcb_at' tptr and Invariants_H.valid_queues and ?Q'15 curThread\<rbrace>
A total of 12 subgoals... proof (prove)
goal (7 subgoals):
 1. \<And>cur curThread y ya. \<lbrakk>new_dom \<le> maxDomain; cur = curThread; dc y ya\<rbrakk> \<Longrightarrow> \<lbrace>?Q'23 cur curThread ya\<rbrace> threadSet (tcbDomain_update (\<lambda>_. new_dom)) tptr \<lbrace>\<lambda>yc. tcb_at' tptr and (\<lambda>a. ((\<lambda>b. st_tcb_at' runnable' tptr a \<longrightarrow> (tcb_at' tptr and Invariants_H.valid_queues and valid_queues') b) and (\<lambda>b. ((if st_tcb_at' runnable' tptr a then Invariants_H.valid_queues and st_tcb_at' runnable' tptr and valid_objs' else Invariants_H.valid_queues) b \<and> (if st_tcb_at' runnable' tptr a then valid_queues' and st_tcb_at' runnable' tptr else valid_queues') b) \<and> (if st_tcb_at' runnable' tptr a then \<lambda>a. weak_sch_act_wf (ksSchedulerAction a) a else (\<lambda>s. weak_sch_act_wf (ksSchedulerAction s) s)) b)) a)\<rbrace>
 2. \<And>cur curThread. \<lbrakk>new_dom \<le> maxDomain; cur = curThread\<rbrakk> \<Longrightarrow> \<lbrace>?Q13 cur\<rbrace> tcb_sched_action tcb_sched_dequeue tptr \<lbrace>\<lambda>y. tcb_at tptr and valid_etcbs and (\<lambda>s. tcb_at tptr s \<and> is_etcb_at tptr s \<and> weak_valid_sched_action s \<and> valid_etcbs s)\<rbrace>
 3. \<And>cur curThread. \<lbrakk>new_dom \<le> maxDomain; cur = curThread\<rbrakk> \<Longrightarrow> \<lbrace>?Q'15 curThread\<rbrace> tcbSchedDequeue tptr \<lbrace>\<lambda>ya. tcb_at' tptr and ?Q'23 cur curThread ya\<rbrace>
 4. new_dom \<le> maxDomain \<Longrightarrow> \<lbrace>?Q6\<rbrace> gets cur_thread \<lbrace>\<lambda>cur. is_etcb_at tptr and ?Q13 cur\<rbrace>
 5. new_dom \<le> maxDomain \<Longrightarrow> \<lbrace>?Q'6\<rbrace> getCurThread \<lbrace>\<lambda>curThread. tcb_at' tptr and Invariants_H.valid_queues and ?Q'15 curThread\<rbrace>
 6. \<And>s. \<lbrakk>new_dom \<le> maxDomain; (valid_etcbs and valid_sched and tcb_at tptr) s\<rbrakk> \<Longrightarrow> ((\<lambda>_. True) and ?Q6) s
 7. \<And>s. \<lbrakk>new_dom \<le> maxDomain; (invs' and sch_act_simple and tcb_at' tptr) s\<rbrakk> \<Longrightarrow> ((\<lambda>_. True) and ?Q'6) s proof (prove)
goal (7 subgoals):
 1. \<And>curThread. new_dom \<le> maxDomain \<Longrightarrow> \<lbrace>?Q'23 curThread curThread ()\<rbrace> threadSet (tcbDomain_update (\<lambda>_. new_dom)) tptr \<lbrace>\<lambda>yc x. tcb_at' tptr x \<and> (st_tcb_at' runnable' tptr x \<longrightarrow> tcb_at' tptr x \<and> Invariants_H.valid_queues x \<and> valid_queues' x \<and> Invariants_H.valid_queues x \<and> valid_objs' x \<and> valid_queues' x \<and> weak_sch_act_wf (ksSchedulerAction x) x) \<and> (\<not> st_tcb_at' runnable' tptr x \<longrightarrow> Invariants_H.valid_queues x \<and> valid_queues' x \<and> weak_sch_act_wf (ksSchedulerAction x) x)\<rbrace>
 2. \<And>cur curThread. \<lbrakk>new_dom \<le> maxDomain; cur = curThread\<rbrakk> \<Longrightarrow> \<lbrace>?Q13 cur\<rbrace> tcb_sched_action tcb_sched_dequeue tptr \<lbrace>\<lambda>y. tcb_at tptr and valid_etcbs and (\<lambda>s. tcb_at tptr s \<and> is_etcb_at tptr s \<and> weak_valid_sched_action s \<and> valid_etcbs s)\<rbrace>
 3. \<And>cur curThread. \<lbrakk>new_dom \<le> maxDomain; cur = curThread\<rbrakk> \<Longrightarrow> \<lbrace>?Q'15 curThread\<rbrace> tcbSchedDequeue tptr \<lbrace>\<lambda>ya. tcb_at' tptr and ?Q'23 cur curThread ya\<rbrace>
 4. new_dom \<le> maxDomain \<Longrightarrow> \<lbrace>?Q6\<rbrace> gets cur_thread \<lbrace>\<lambda>cur. is_etcb_at tptr and ?Q13 cur\<rbrace>
 5. new_dom \<le> maxDomain \<Longrightarrow> \<lbrace>?Q'6\<rbrace> getCurThread \<lbrace>\<lambda>curThread. tcb_at' tptr and Invariants_H.valid_queues and ?Q'15 curThread\<rbrace>
 6. \<And>s. \<lbrakk>new_dom \<le> maxDomain; (valid_etcbs and valid_sched and tcb_at tptr) s\<rbrakk> \<Longrightarrow> ((\<lambda>_. True) and ?Q6) s
 7. \<And>s. \<lbrakk>new_dom \<le> maxDomain; (invs' and sch_act_simple and tcb_at' tptr) s\<rbrakk> \<Longrightarrow> ((\<lambda>_. True) and ?Q'6) s proof (prove)
goal (8 subgoals):
 1. \<And>curThread rv s. \<lbrakk>new_dom \<le> maxDomain; (valid_objs' and valid_queues' and Invariants_H.valid_queues and (\<lambda>s. sch_act_wf (ksSchedulerAction s) s) and tcb_at' tptr) s\<rbrakk> \<Longrightarrow> tcb_at' tptr s \<and> (st_tcb_at' runnable' tptr s \<longrightarrow> tcb_at' tptr s \<and> Invariants_H.valid_queues s \<and> valid_queues' s \<and> Invariants_H.valid_queues s \<and> valid_objs' s \<and> valid_queues' s \<and> weak_sch_act_wf (ksSchedulerAction s) s) \<and> (\<not> st_tcb_at' runnable' tptr s \<longrightarrow> Invariants_H.valid_queues s \<and> valid_queues' s \<and> weak_sch_act_wf (ksSchedulerAction s) s)
 2. \<And>curThread. new_dom \<le> maxDomain \<Longrightarrow> \<lbrace>?Q'23 curThread curThread ()\<rbrace> threadSet (tcbDomain_update (\<lambda>_. new_dom)) tptr \<lbrace>\<lambda>_. valid_objs' and valid_queues' and Invariants_H.valid_queues and (\<lambda>s. sch_act_wf (ksSchedulerAction s) s) and tcb_at' tptr\<rbrace>
 3. \<And>cur curThread. \<lbrakk>new_dom \<le> maxDomain; cur = curThread\<rbrakk> \<Longrightarrow> \<lbrace>?Q13 cur\<rbrace> tcb_sched_action tcb_sched_dequeue tptr \<lbrace>\<lambda>y. tcb_at tptr and valid_etcbs and (\<lambda>s. tcb_at tptr s \<and> is_etcb_at tptr s \<and> weak_valid_sched_action s \<and> valid_etcbs s)\<rbrace>
 4. \<And>cur curThread. \<lbrakk>new_dom \<le> maxDomain; cur = curThread\<rbrakk> \<Longrightarrow> \<lbrace>?Q'15 curThread\<rbrace> tcbSchedDequeue tptr \<lbrace>\<lambda>ya. tcb_at' tptr and ?Q'23 cur curThread ya\<rbrace>
 5. new_dom \<le> maxDomain \<Longrightarrow> \<lbrace>?Q6\<rbrace> gets cur_thread \<lbrace>\<lambda>cur. is_etcb_at tptr and ?Q13 cur\<rbrace>
 6. new_dom \<le> maxDomain \<Longrightarrow> \<lbrace>?Q'6\<rbrace> getCurThread \<lbrace>\<lambda>curThread. tcb_at' tptr and Invariants_H.valid_queues and ?Q'15 curThread\<rbrace>
 7. \<And>s. \<lbrakk>new_dom \<le> maxDomain; (valid_etcbs and valid_sched and tcb_at tptr) s\<rbrakk> \<Longrightarrow> ((\<lambda>_. True) and ?Q6) s
 8. \<And>s. \<lbrakk>new_dom \<le> maxDomain; (invs' and sch_act_simple and tcb_at' tptr) s\<rbrakk> \<Longrightarrow> ((\<lambda>_. True) and ?Q'6) s proof (prove)
goal (7 subgoals):
 1. \<And>curThread. new_dom \<le> maxDomain \<Longrightarrow> \<lbrace>?Q'23 curThread curThread ()\<rbrace> threadSet (tcbDomain_update (\<lambda>_. new_dom)) tptr \<lbrace>\<lambda>_. valid_objs' and valid_queues' and Invariants_H.valid_queues and (\<lambda>s. sch_act_wf (ksSchedulerAction s) s) and tcb_at' tptr\<rbrace>
 2. \<And>cur curThread. \<lbrakk>new_dom \<le> maxDomain; cur = curThread\<rbrakk> \<Longrightarrow> \<lbrace>?Q13 cur\<rbrace> tcb_sched_action tcb_sched_dequeue tptr \<lbrace>\<lambda>y. tcb_at tptr and valid_etcbs and (\<lambda>s. tcb_at tptr s \<and> is_etcb_at tptr s \<and> weak_valid_sched_action s \<and> valid_etcbs s)\<rbrace>
 3. \<And>cur curThread. \<lbrakk>new_dom \<le> maxDomain; cur = curThread\<rbrakk> \<Longrightarrow> \<lbrace>?Q'15 curThread\<rbrace> tcbSchedDequeue tptr \<lbrace>\<lambda>ya. tcb_at' tptr and ?Q'23 cur curThread ya\<rbrace>
 4. new_dom \<le> maxDomain \<Longrightarrow> \<lbrace>?Q6\<rbrace> gets cur_thread \<lbrace>\<lambda>cur. is_etcb_at tptr and ?Q13 cur\<rbrace>
 5. new_dom \<le> maxDomain \<Longrightarrow> \<lbrace>?Q'6\<rbrace> getCurThread \<lbrace>\<lambda>curThread. tcb_at' tptr and Invariants_H.valid_queues and ?Q'15 curThread\<rbrace>
 6. \<And>s. \<lbrakk>new_dom \<le> maxDomain; (valid_etcbs and valid_sched and tcb_at tptr) s\<rbrakk> \<Longrightarrow> ((\<lambda>_. True) and ?Q6) s
 7. \<And>s. \<lbrakk>new_dom \<le> maxDomain; (invs' and sch_act_simple and tcb_at' tptr) s\<rbrakk> \<Longrightarrow> ((\<lambda>_. True) and ?Q'6) s proof (prove)
goal (5 subgoals):
 1. \<And>cur curThread. \<lbrakk>new_dom \<le> maxDomain; cur = curThread\<rbrakk> \<Longrightarrow> \<lbrace>?P'287 curThread\<rbrace> tcbSchedDequeue tptr \<lbrace>\<lambda>rv s. (\<forall>tcb. valid_tcb' tcb s \<longrightarrow> valid_tcb' (tcbDomain_update (\<lambda>_. new_dom) tcb) s) \<and> valid_queues' s \<and> (\<forall>a b. tptr \<notin> set (ksReadyQueues s (a, b))) \<and> Invariants_H.valid_queues s \<and> (\<forall>a b. tptr \<notin> set (ksReadyQueues s (a, b))) \<and> sch_act_wf (ksSchedulerAction s) s \<and> sch_act_not tptr s \<and> tcb_at' tptr s\<rbrace>
 2. new_dom \<le> maxDomain \<Longrightarrow> \<lbrace>?Q6\<rbrace> gets cur_thread \<lbrace>\<lambda>cur. is_etcb_at tptr and (\<lambda>s. tcb_at tptr s \<and> valid_etcbs s \<and> tcb_at tptr s \<and> is_etcb_at tptr s \<and> weak_valid_sched_action s \<and> valid_etcbs s)\<rbrace>
 3. new_dom \<le> maxDomain \<Longrightarrow> \<lbrace>?Q'6\<rbrace> getCurThread \<lbrace>\<lambda>curThread. tcb_at' tptr and Invariants_H.valid_queues and (\<lambda>s. tcb_at' tptr s \<and> valid_objs' s \<and> ?P'287 curThread s)\<rbrace>
 4. \<And>s. \<lbrakk>new_dom \<le> maxDomain; (valid_etcbs and valid_sched and tcb_at tptr) s\<rbrakk> \<Longrightarrow> ((\<lambda>_. True) and ?Q6) s
 5. \<And>s. \<lbrakk>new_dom \<le> maxDomain; (invs' and sch_act_simple and tcb_at' tptr) s\<rbrakk> \<Longrightarrow> ((\<lambda>_. True) and ?Q'6) s proof (prove)
goal (6 subgoals):
 1. \<And>cur curThread rv s. \<lbrakk>new_dom \<le> maxDomain; cur = curThread; invs' s \<and> (\<forall>p. tptr \<notin> set (ksReadyQueues s p)) \<and> sch_act_simple s \<and> tcb_at' tptr s\<rbrakk> \<Longrightarrow> (\<forall>tcb. valid_tcb' tcb s \<longrightarrow> valid_tcb' (tcbDomain_update (\<lambda>_. new_dom) tcb) s) \<and> valid_queues' s \<and> (\<forall>a b. tptr \<notin> set (ksReadyQueues s (a, b))) \<and> Invariants_H.valid_queues s \<and> (\<forall>a b. tptr \<notin> set (ksReadyQueues s (a, b))) \<and> sch_act_wf (ksSchedulerAction s) s \<and> sch_act_not tptr s \<and> tcb_at' tptr s
 2. \<And>cur curThread. \<lbrakk>new_dom \<le> maxDomain; cur = curThread\<rbrakk> \<Longrightarrow> \<lbrace>?P'287 curThread\<rbrace> tcbSchedDequeue tptr \<lbrace>\<lambda>r s. invs' s \<and> (\<forall>p. tptr \<notin> set (ksReadyQueues s p)) \<and> sch_act_simple s \<and> tcb_at' tptr s\<rbrace>
 3. new_dom \<le> maxDomain \<Longrightarrow> \<lbrace>?Q6\<rbrace> gets cur_thread \<lbrace>\<lambda>cur. is_etcb_at tptr and (\<lambda>s. tcb_at tptr s \<and> valid_etcbs s \<and> tcb_at tptr s \<and> is_etcb_at tptr s \<and> weak_valid_sched_action s \<and> valid_etcbs s)\<rbrace>
 4. new_dom \<le> maxDomain \<Longrightarrow> \<lbrace>?Q'6\<rbrace> getCurThread \<lbrace>\<lambda>curThread. tcb_at' tptr and Invariants_H.valid_queues and (\<lambda>s. tcb_at' tptr s \<and> valid_objs' s \<and> ?P'287 curThread s)\<rbrace>
 5. \<And>s. \<lbrakk>new_dom \<le> maxDomain; (valid_etcbs and valid_sched and tcb_at tptr) s\<rbrakk> \<Longrightarrow> ((\<lambda>_. True) and ?Q6) s
 6. \<And>s. \<lbrakk>new_dom \<le> maxDomain; (invs' and sch_act_simple and tcb_at' tptr) s\<rbrakk> \<Longrightarrow> ((\<lambda>_. True) and ?Q'6) s proof (prove)
goal (6 subgoals):
 1. \<And>s tcb. \<lbrakk>new_dom \<le> maxDomain; valid_objs' s; pspace_aligned' s; pspace_distinct' s; no_0_obj' s; valid_mdb' s; sch_act_wf (ksSchedulerAction s) s; Invariants_H.valid_queues s; sym_refs (state_refs_of' s); if_live_then_nonz_cap' s; if_unsafe_then_cap' s; valid_idle' s; valid_global_refs' s; valid_arch_state' s; valid_irq_node' (irq_node' s) s; valid_irq_handlers' s; valid_irq_states' s; valid_machine_state' s; irqs_masked' s; valid_queues' s; ct_not_inQ s; ct_idle_or_in_cur_domain' s; valid_pde_mappings' s; pspace_domain_valid s; ksCurDomain s \<le> maxDomain; ksDomSchedule (KernelInit_H.newKernelState undefined) \<noteq> []; \<forall>x\<in>set (ksDomSchedule (KernelInit_H.newKernelState undefined)). dschDomain x \<le> maxDomain \<and> 0 < dschLength x; ksDomSchedule s = ksDomSchedule (KernelInit_H.newKernelState undefined); ksDomScheduleIdx s < length (ksDomSchedule (KernelInit_H.newKernelState undefined)); untyped_ranges_zero' s; cur_tcb' s; \<forall>a b. tptr \<notin> set (ksReadyQueues s (a, b)); ksSchedulerAction s = ResumeCurrentThread \<or> ksSchedulerAction s = ChooseNewThread; tcb_at' tptr s; valid_tcb' tcb s\<rbrakk> \<Longrightarrow> valid_tcb' (tcbDomain_update (\<lambda>_. new_dom) tcb) s
 2. \<And>cur curThread. \<lbrakk>new_dom \<le> maxDomain; cur = curThread\<rbrakk> \<Longrightarrow> \<lbrace>?P'287 curThread\<rbrace> tcbSchedDequeue tptr \<lbrace>\<lambda>r s. invs' s \<and> (\<forall>p. tptr \<notin> set (ksReadyQueues s p)) \<and> sch_act_simple s \<and> tcb_at' tptr s\<rbrace>
 3. new_dom \<le> maxDomain \<Longrightarrow> \<lbrace>?Q6\<rbrace> gets cur_thread \<lbrace>\<lambda>cur. is_etcb_at tptr and (\<lambda>s. tcb_at tptr s \<and> valid_etcbs s \<and> tcb_at tptr s \<and> is_etcb_at tptr s \<and> weak_valid_sched_action s \<and> valid_etcbs s)\<rbrace>
 4. new_dom \<le> maxDomain \<Longrightarrow> \<lbrace>?Q'6\<rbrace> getCurThread \<lbrace>\<lambda>curThread. tcb_at' tptr and Invariants_H.valid_queues and (\<lambda>s. tcb_at' tptr s \<and> valid_objs' s \<and> ?P'287 curThread s)\<rbrace>
 5. \<And>s. \<lbrakk>new_dom \<le> maxDomain; (valid_etcbs and valid_sched and tcb_at tptr) s\<rbrakk> \<Longrightarrow> ((\<lambda>_. True) and ?Q6) s
 6. \<And>s. \<lbrakk>new_dom \<le> maxDomain; (invs' and sch_act_simple and tcb_at' tptr) s\<rbrakk> \<Longrightarrow> ((\<lambda>_. True) and ?Q'6) s proof (prove)
goal (6 subgoals):
 1. \<And>s tcb a b. \<lbrakk>new_dom \<le> maxDomain; valid_objs' s; pspace_aligned' s; pspace_distinct' s; no_0_obj' s; valid_mdb' s; sch_act_wf (ksSchedulerAction s) s; Invariants_H.valid_queues s; sym_refs (state_refs_of' s); if_live_then_nonz_cap' s; if_unsafe_then_cap' s; valid_idle' s; valid_global_refs' s; valid_arch_state' s; valid_irq_node' (irq_node' s) s; valid_irq_handlers' s; valid_irq_states' s; valid_machine_state' s; irqs_masked' s; valid_queues' s; ct_not_inQ s; ct_idle_or_in_cur_domain' s; valid_pde_mappings' s; pspace_domain_valid s; ksCurDomain s \<le> maxDomain; ksDomSchedule (KernelInit_H.newKernelState undefined) \<noteq> []; \<forall>x\<in>set (ksDomSchedule (KernelInit_H.newKernelState undefined)). dschDomain x \<le> maxDomain \<and> 0 < dschLength x; ksDomSchedule s = ksDomSchedule (KernelInit_H.newKernelState undefined); ksDomScheduleIdx s < length (ksDomSchedule (KernelInit_H.newKernelState undefined)); untyped_ranges_zero' s; cur_tcb' s; \<forall>a b. tptr \<notin> set (ksReadyQueues s (a, b)); ksSchedulerAction s = ResumeCurrentThread \<or> ksSchedulerAction s = ChooseNewThread; tcb_at' tptr s; (a, b) \<in> ran tcb_cte_cases; \<forall>x\<in>ran tcb_cte_cases. case x of (getF, setF) \<Rightarrow> valid_cap' (cteCap (getF tcb)) s; valid_tcb_state' (tcbState tcb) s; is_aligned (tcbIPCBuffer tcb) msg_align_bits; valid_bound_ntfn' (tcbBoundNotification tcb) s; tcbDomain tcb \<le> maxDomain; tcbPriority tcb \<le> maxPriority; tcbMCP tcb \<le> maxPriority\<rbrakk> \<Longrightarrow> valid_cap' (cteCap (a (tcbDomain_update (\<lambda>_. new_dom) tcb))) s
 2. \<And>cur curThread. \<lbrakk>new_dom \<le> maxDomain; cur = curThread\<rbrakk> \<Longrightarrow> \<lbrace>?P'287 curThread\<rbrace> tcbSchedDequeue tptr \<lbrace>\<lambda>r s. invs' s \<and> (\<forall>p. tptr \<notin> set (ksReadyQueues s p)) \<and> sch_act_simple s \<and> tcb_at' tptr s\<rbrace>
 3. new_dom \<le> maxDomain \<Longrightarrow> \<lbrace>?Q6\<rbrace> gets cur_thread \<lbrace>\<lambda>cur. is_etcb_at tptr and (\<lambda>s. tcb_at tptr s \<and> valid_etcbs s \<and> tcb_at tptr s \<and> is_etcb_at tptr s \<and> weak_valid_sched_action s \<and> valid_etcbs s)\<rbrace>
 4. new_dom \<le> maxDomain \<Longrightarrow> \<lbrace>?Q'6\<rbrace> getCurThread \<lbrace>\<lambda>curThread. tcb_at' tptr and Invariants_H.valid_queues and (\<lambda>s. tcb_at' tptr s \<and> valid_objs' s \<and> ?P'287 curThread s)\<rbrace>
 5. \<And>s. \<lbrakk>new_dom \<le> maxDomain; (valid_etcbs and valid_sched and tcb_at tptr) s\<rbrakk> \<Longrightarrow> ((\<lambda>_. True) and ?Q6) s
 6. \<And>s. \<lbrakk>new_dom \<le> maxDomain; (invs' and sch_act_simple and tcb_at' tptr) s\<rbrakk> \<Longrightarrow> ((\<lambda>_. True) and ?Q'6) s proof (prove)
goal (6 subgoals):
 1. \<And>s tcb a b. \<lbrakk>new_dom \<le> maxDomain; valid_objs' s; pspace_aligned' s; pspace_distinct' s; no_0_obj' s; valid_mdb' s; sch_act_wf (ksSchedulerAction s) s; Invariants_H.valid_queues s; sym_refs (state_refs_of' s); if_live_then_nonz_cap' s; if_unsafe_then_cap' s; valid_idle' s; valid_global_refs' s; valid_arch_state' s; valid_irq_node' (irq_node' s) s; valid_irq_handlers' s; valid_irq_states' s; valid_machine_state' s; irqs_masked' s; valid_queues' s; ct_not_inQ s; ct_idle_or_in_cur_domain' s; valid_pde_mappings' s; pspace_domain_valid s; ksCurDomain s \<le> maxDomain; ksDomSchedule (KernelInit_H.newKernelState undefined) \<noteq> []; \<forall>x\<in>set (ksDomSchedule (KernelInit_H.newKernelState undefined)). dschDomain x \<le> maxDomain \<and> 0 < dschLength x; ksDomSchedule s = ksDomSchedule (KernelInit_H.newKernelState undefined); ksDomScheduleIdx s < length (ksDomSchedule (KernelInit_H.newKernelState undefined)); untyped_ranges_zero' s; cur_tcb' s; \<forall>a b. tptr \<notin> set (ksReadyQueues s (a, b)); ksSchedulerAction s = ResumeCurrentThread \<or> ksSchedulerAction s = ChooseNewThread; tcb_at' tptr s; (a, b) \<in> ran tcb_cte_cases; valid_tcb_state' (tcbState tcb) s; is_aligned (tcbIPCBuffer tcb) msg_align_bits; valid_bound_ntfn' (tcbBoundNotification tcb) s; tcbDomain tcb \<le> maxDomain; tcbPriority tcb \<le> maxPriority; tcbMCP tcb \<le> maxPriority; case (a, b) of (getF, setF) \<Rightarrow> valid_cap' (cteCap (getF tcb)) s\<rbrakk> \<Longrightarrow> valid_cap' (cteCap (a (tcbDomain_update (\<lambda>_. new_dom) tcb))) s
 2. \<And>cur curThread. \<lbrakk>new_dom \<le> maxDomain; cur = curThread\<rbrakk> \<Longrightarrow> \<lbrace>?P'287 curThread\<rbrace> tcbSchedDequeue tptr \<lbrace>\<lambda>r s. invs' s \<and> (\<forall>p. tptr \<notin> set (ksReadyQueues s p)) \<and> sch_act_simple s \<and> tcb_at' tptr s\<rbrace>
 3. new_dom \<le> maxDomain \<Longrightarrow> \<lbrace>?Q6\<rbrace> gets cur_thread \<lbrace>\<lambda>cur. is_etcb_at tptr and (\<lambda>s. tcb_at tptr s \<and> valid_etcbs s \<and> tcb_at tptr s \<and> is_etcb_at tptr s \<and> weak_valid_sched_action s \<and> valid_etcbs s)\<rbrace>
 4. new_dom \<le> maxDomain \<Longrightarrow> \<lbrace>?Q'6\<rbrace> getCurThread \<lbrace>\<lambda>curThread. tcb_at' tptr and Invariants_H.valid_queues and (\<lambda>s. tcb_at' tptr s \<and> valid_objs' s \<and> ?P'287 curThread s)\<rbrace>
 5. \<And>s. \<lbrakk>new_dom \<le> maxDomain; (valid_etcbs and valid_sched and tcb_at tptr) s\<rbrakk> \<Longrightarrow> ((\<lambda>_. True) and ?Q6) s
 6. \<And>s. \<lbrakk>new_dom \<le> maxDomain; (invs' and sch_act_simple and tcb_at' tptr) s\<rbrakk> \<Longrightarrow> ((\<lambda>_. True) and ?Q'6) s proof (prove)
goal (6 subgoals):
 1. \<And>s tcb a b. \<lbrakk>new_dom \<le> maxDomain; valid_objs' s; pspace_aligned' s; pspace_distinct' s; no_0_obj' s; valid_mdb' s; sch_act_wf (ksSchedulerAction s) s; Invariants_H.valid_queues s; sym_refs (state_refs_of' s); if_live_then_nonz_cap' s; if_unsafe_then_cap' s; valid_idle' s; valid_global_refs' s; valid_arch_state' s; valid_irq_node' (irq_node' s) s; valid_irq_handlers' s; valid_irq_states' s; valid_machine_state' s; irqs_masked' s; valid_queues' s; ct_not_inQ s; ct_idle_or_in_cur_domain' s; valid_pde_mappings' s; pspace_domain_valid s; ksCurDomain s \<le> maxDomain; ksDomSchedule (KernelInit_H.newKernelState undefined) \<noteq> []; \<forall>x\<in>set (ksDomSchedule (KernelInit_H.newKernelState undefined)). dschDomain x \<le> maxDomain \<and> 0 < dschLength x; ksDomSchedule s = ksDomSchedule (KernelInit_H.newKernelState undefined); ksDomScheduleIdx s < length (ksDomSchedule (KernelInit_H.newKernelState undefined)); untyped_ranges_zero' s; cur_tcb' s; \<forall>a b. tptr \<notin> set (ksReadyQueues s (a, b)); ksSchedulerAction s = ResumeCurrentThread \<or> ksSchedulerAction s = ChooseNewThread; tcb_at' tptr s; a = tcbIPCBufferFrame \<and> b = tcbIPCBufferFrame_update \<or> a = tcbCaller \<and> b = tcbCaller_update \<or> a = tcbReply \<and> b = tcbReply_update \<or> a = tcbVTable \<and> b = tcbVTable_update \<or> a = tcbCTable \<and> b = tcbCTable_update; valid_tcb_state' (tcbState tcb) s; is_aligned (tcbIPCBuffer tcb) msg_align_bits; valid_bound_ntfn' (tcbBoundNotification tcb) s; tcbDomain tcb \<le> maxDomain; tcbPriority tcb \<le> maxPriority; tcbMCP tcb \<le> maxPriority; valid_cap' (cteCap (a tcb)) s\<rbrakk> \<Longrightarrow> valid_cap' (cteCap (a (tcbDomain_update (\<lambda>_. new_dom) tcb))) s
 2. \<And>cur curThread. \<lbrakk>new_dom \<le> maxDomain; cur = curThread\<rbrakk> \<Longrightarrow> \<lbrace>?P'287 curThread\<rbrace> tcbSchedDequeue tptr \<lbrace>\<lambda>r s. invs' s \<and> (\<forall>p. tptr \<notin> set (ksReadyQueues s p)) \<and> sch_act_simple s \<and> tcb_at' tptr s\<rbrace>
 3. new_dom \<le> maxDomain \<Longrightarrow> \<lbrace>?Q6\<rbrace> gets cur_thread \<lbrace>\<lambda>cur. is_etcb_at tptr and (\<lambda>s. tcb_at tptr s \<and> valid_etcbs s \<and> tcb_at tptr s \<and> is_etcb_at tptr s \<and> weak_valid_sched_action s \<and> valid_etcbs s)\<rbrace>
 4. new_dom \<le> maxDomain \<Longrightarrow> \<lbrace>?Q'6\<rbrace> getCurThread \<lbrace>\<lambda>curThread. tcb_at' tptr and Invariants_H.valid_queues and (\<lambda>s. tcb_at' tptr s \<and> valid_objs' s \<and> ?P'287 curThread s)\<rbrace>
 5. \<And>s. \<lbrakk>new_dom \<le> maxDomain; (valid_etcbs and valid_sched and tcb_at tptr) s\<rbrakk> \<Longrightarrow> ((\<lambda>_. True) and ?Q6) s
 6. \<And>s. \<lbrakk>new_dom \<le> maxDomain; (invs' and sch_act_simple and tcb_at' tptr) s\<rbrakk> \<Longrightarrow> ((\<lambda>_. True) and ?Q'6) s proof (prove)
goal (5 subgoals):
 1. \<And>cur curThread. \<lbrakk>new_dom \<le> maxDomain; cur = curThread\<rbrakk> \<Longrightarrow> \<lbrace>?P'287 curThread\<rbrace> tcbSchedDequeue tptr \<lbrace>\<lambda>r s. invs' s \<and> (\<forall>p. tptr \<notin> set (ksReadyQueues s p)) \<and> sch_act_simple s \<and> tcb_at' tptr s\<rbrace>
 2. new_dom \<le> maxDomain \<Longrightarrow> \<lbrace>?Q6\<rbrace> gets cur_thread \<lbrace>\<lambda>cur. is_etcb_at tptr and (\<lambda>s. tcb_at tptr s \<and> valid_etcbs s \<and> tcb_at tptr s \<and> is_etcb_at tptr s \<and> weak_valid_sched_action s \<and> valid_etcbs s)\<rbrace>
 3. new_dom \<le> maxDomain \<Longrightarrow> \<lbrace>?Q'6\<rbrace> getCurThread \<lbrace>\<lambda>curThread. tcb_at' tptr and Invariants_H.valid_queues and (\<lambda>s. tcb_at' tptr s \<and> valid_objs' s \<and> ?P'287 curThread s)\<rbrace>
 4. \<And>s. \<lbrakk>new_dom \<le> maxDomain; (valid_etcbs and valid_sched and tcb_at tptr) s\<rbrakk> \<Longrightarrow> ((\<lambda>_. True) and ?Q6) s
 5. \<And>s. \<lbrakk>new_dom \<le> maxDomain; (invs' and sch_act_simple and tcb_at' tptr) s\<rbrakk> \<Longrightarrow> ((\<lambda>_. True) and ?Q'6) s proof (prove)
goal (2 subgoals):
 1. \<And>s. \<lbrakk>new_dom \<le> maxDomain; (valid_etcbs and valid_sched and tcb_at tptr) s\<rbrakk> \<Longrightarrow> ((\<lambda>_. True) and (is_etcb_at tptr and (\<lambda>s. tcb_at tptr s \<and> valid_etcbs s \<and> tcb_at tptr s \<and> is_etcb_at tptr s \<and> weak_valid_sched_action s \<and> valid_etcbs s))) s
 2. \<And>s. \<lbrakk>new_dom \<le> maxDomain; (invs' and sch_act_simple and tcb_at' tptr) s\<rbrakk> \<Longrightarrow> ((\<lambda>_. True) and (tcb_at' tptr and Invariants_H.valid_queues and (\<lambda>s. tcb_at' tptr s \<and> valid_objs' s \<and> (invs' and tcb_at' tptr) s \<and> (\<forall>x. (Invariants_H.valid_queues and tcb_at' tptr and valid_objs') s) \<and> sch_act_simple s \<and> tcb_at' tptr s))) s proof (prove)
goal (2 subgoals):
 1. \<And>s. \<lbrakk>new_dom \<le> maxDomain; valid_etcbs s; valid_sched s; tcb_at tptr s\<rbrakk> \<Longrightarrow> is_etcb_at tptr s \<and> weak_valid_sched_action s
 2. \<And>s. \<lbrakk>new_dom \<le> maxDomain; (invs' and sch_act_simple and tcb_at' tptr) s\<rbrakk> \<Longrightarrow> ((\<lambda>_. True) and (tcb_at' tptr and Invariants_H.valid_queues and (\<lambda>s. tcb_at' tptr s \<and> valid_objs' s \<and> (invs' and tcb_at' tptr) s \<and> (\<forall>x. (Invariants_H.valid_queues and tcb_at' tptr and valid_objs') s) \<and> sch_act_simple s \<and> tcb_at' tptr s))) s proof (prove)
goal (3 subgoals):
 1. \<And>s. \<lbrakk>new_dom \<le> maxDomain; valid_etcbs s; valid_sched s; tcb_at tptr s\<rbrakk> \<Longrightarrow> valid_etcbs s
 2. \<And>s. \<lbrakk>new_dom \<le> maxDomain; valid_etcbs s; valid_sched s; tcb_at tptr s; is_etcb_at tptr s\<rbrakk> \<Longrightarrow> is_etcb_at tptr s \<and> weak_valid_sched_action s
 3. \<And>s. \<lbrakk>new_dom \<le> maxDomain; (invs' and sch_act_simple and tcb_at' tptr) s\<rbrakk> \<Longrightarrow> ((\<lambda>_. True) and (tcb_at' tptr and Invariants_H.valid_queues and (\<lambda>s. tcb_at' tptr s \<and> valid_objs' s \<and> (invs' and tcb_at' tptr) s \<and> (\<forall>x. (Invariants_H.valid_queues and tcb_at' tptr and valid_objs') s) \<and> sch_act_simple s \<and> tcb_at' tptr s))) s proof (prove)
goal (2 subgoals):
 1. \<And>s. \<lbrakk>new_dom \<le> maxDomain; valid_etcbs s; valid_sched s; tcb_at tptr s; is_etcb_at tptr s\<rbrakk> \<Longrightarrow> weak_valid_sched_action s
 2. \<And>s. \<lbrakk>new_dom \<le> maxDomain; (invs' and sch_act_simple and tcb_at' tptr) s\<rbrakk> \<Longrightarrow> ((\<lambda>_. True) and (tcb_at' tptr and Invariants_H.valid_queues and (\<lambda>s. tcb_at' tptr s \<and> valid_objs' s \<and> (invs' and tcb_at' tptr) s \<and> (\<forall>x. (Invariants_H.valid_queues and tcb_at' tptr and valid_objs') s) \<and> sch_act_simple s \<and> tcb_at' tptr s))) s proof (prove)
goal:
No subgoals!