theory IpcCancel_C

lemma possibleSwitchTo_ccorres:
  shows
  "ccorres dc xfdc
         (valid_queues and (\<lambda>s. weak_sch_act_wf (ksSchedulerAction s) s)
            and st_tcb_at' runnable' t and (\<lambda>s. ksCurDomain s \<le> maxDomain)
            and valid_objs')
         ({s. target_' s = tcb_ptr_to_ctcb_ptr t}
          \<inter> UNIV) []
     (possibleSwitchTo t )
     (Call possibleSwitchTo_'proc)" supply if_split [split del] supply Collect_const [simp del] supply prio_and_dom_limit_helpers[simp] 
  (* FIXME: these should likely be in simpset for CRefine, or even in general *)
   supply from_bool_eq_if[simp] from_bool_eq_if'[simp] from_bool_0[simp]
         ccorres_IF_True[simp] if_cong[cong] apply (cinit lift: target_') apply (rule ccorres_move_c_guard_tcb) apply (rule ccorres_pre_curDomain, rename_tac curDom) apply (rule ccorres_symb_exec_l3[OF _ threadGet_inv _ empty_fail_threadGet], rename_tac targetDom) apply (rule ccorres_symb_exec_l3[OF _ gsa_wp _ empty_fail_getSchedulerAction], rename_tac sact) apply (rule_tac C'="{s. targetDom \<noteq> curDom}"
              and Q="\<lambda>s. curDom = ksCurDomain s \<and> obj_at' (\<lambda>tcb. targetDom = tcbDomain tcb) t s"
              and Q'=UNIV in ccorres_rewrite_cond_sr) subgoal apply clarsimp apply (drule obj_at_ko_at', clarsimp  simp: rf_sr_ksCurDomain) apply (frule (1) obj_at_cslift_tcb, clarsimp simp: typ_heap_simps') apply (drule ctcb_relation_unat_tcbDomain_C) apply unat_arith apply fastforce done apply (rule ccorres_cond2[where R=\<top>], simp) apply (ctac add: tcbSchedEnqueue_ccorres) apply (rule_tac R="\<lambda>s. sact = ksSchedulerAction s \<and> weak_sch_act_wf (ksSchedulerAction s) s"
                     in ccorres_cond) apply (fastforce dest!: rf_sr_sched_action_relation pred_tcb_at' tcb_at_not_NULL
                        simp: cscheduler_action_relation_def weak_sch_act_wf_def
                        split: scheduler_action.splits) apply (ctac add: rescheduleRequired_ccorres) apply (ctac add: tcbSchedEnqueue_ccorres) apply wp apply (vcg exspec=rescheduleRequired_modifies) apply (rule ccorres_setSchedulerAction, simp add: cscheduler_action_relation_def) apply clarsimp apply wp apply clarsimp apply (wp hoare_drop_imps threadGet_get_obj_at'_has_domain) apply (clarsimp simp: pred_tcb_at') done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. ccorres dc xfdc (Invariants_H.valid_queues and (\<lambda>s. weak_sch_act_wf (ksSchedulerAction s) s) and st_tcb_at' runnable' t and (\<lambda>s. ksCurDomain s \<le> maxDomain) and valid_objs') (\<lbrace>\<acute>target = tcb_ptr_to_ctcb_ptr t\<rbrace> \<inter> UNIV) [] (possibleSwitchTo t) (Call possibleSwitchTo_'proc) proof (prove)
goal (1 subgoal):
 1. ccorres dc xfdc (Invariants_H.valid_queues and (\<lambda>s. weak_sch_act_wf (ksSchedulerAction s) s) and st_tcb_at' runnable' t and (\<lambda>s. ksCurDomain s \<le> maxDomain) and valid_objs') (\<lbrace>\<acute>target = tcb_ptr_to_ctcb_ptr t\<rbrace> \<inter> UNIV) [] (possibleSwitchTo t) (Call possibleSwitchTo_'proc) proof (prove)
goal (1 subgoal):
 1. ccorres dc xfdc (Invariants_H.valid_queues and (\<lambda>s. weak_sch_act_wf (ksSchedulerAction s) s) and st_tcb_at' runnable' t and (\<lambda>s. ksCurDomain s \<le> maxDomain) and valid_objs') (\<lbrace>\<acute>target = tcb_ptr_to_ctcb_ptr t\<rbrace> \<inter> UNIV) [] (possibleSwitchTo t) (Call possibleSwitchTo_'proc) proof (prove)
goal (1 subgoal):
 1. ccorres dc xfdc (Invariants_H.valid_queues and (\<lambda>s. weak_sch_act_wf (ksSchedulerAction s) s) and st_tcb_at' runnable' t and (\<lambda>s. ksCurDomain s \<le> maxDomain) and valid_objs') (\<lbrace>\<acute>target = tcb_ptr_to_ctcb_ptr t\<rbrace> \<inter> UNIV) [] (possibleSwitchTo t) (Call possibleSwitchTo_'proc) proof (prove)
goal (1 subgoal):
 1. ccorres dc xfdc (Invariants_H.valid_queues and (\<lambda>s. weak_sch_act_wf (ksSchedulerAction s) s) and st_tcb_at' runnable' t and (\<lambda>s. ksCurDomain s \<le> maxDomain) and valid_objs') (\<lbrace>\<acute>target = tcb_ptr_to_ctcb_ptr t\<rbrace> \<inter> UNIV) [] (possibleSwitchTo t) (Call possibleSwitchTo_'proc) proof (prove)
goal (1 subgoal):
 1. ccorres dc xfdc (Invariants_H.valid_queues and (\<lambda>s. weak_sch_act_wf (ksSchedulerAction s) s) and st_tcb_at' runnable' t and (\<lambda>s. ksCurDomain s \<le> maxDomain) and valid_objs') (\<lbrace>\<acute>target = tcb_ptr_to_ctcb_ptr t\<rbrace> \<inter> UNIV) [] (possibleSwitchTo t) (Call possibleSwitchTo_'proc) proof (prove)
goal (2 subgoals):
 1. \<And>target. target = tcb_ptr_to_ctcb_ptr t \<Longrightarrow> ccorres dc xfdc (?Q124 target) (?Q'124 target) [SKIP] (do curDom <- curDomain;
targetDom <- threadGet tcbDomain t;
action <- getSchedulerAction;
if targetDom \<noteq> curDom then tcbSchedEnqueue t else if action \<noteq> ResumeCurrentThread then do y <- rescheduleRequired;
tcbSchedEnqueue t
od else setSchedulerAction (SwitchToThread t)
od) (Guard C_Guard {s. s \<Turnstile>\<^sub>c target} (IF \<acute>ksCurDomain \<noteq> h_val (hrs_mem \<acute>t_hrs) (PTR(32 word) &(target\<rightarrow>[''tcbDomain_C''])) THEN
  CALL tcbSchedEnqueue_'proc(target)
ELSE
  IF \<acute>ksSchedulerAction \<noteq> NULL THEN
  CALL rescheduleRequired_'proc();;
CALL tcbSchedEnqueue_'proc(target)
ELSE
  \<acute>ksSchedulerAction :== target
FI
FI))
 2. \<And>target s s'. \<lbrakk>target = tcb_ptr_to_ctcb_ptr t; (s, s') \<in> rf_sr; (Invariants_H.valid_queues and (\<lambda>s. weak_sch_act_wf (ksSchedulerAction s) s) and st_tcb_at' runnable' t and (\<lambda>s. ksCurDomain s \<le> maxDomain) and valid_objs') s; s' \<in> UNIV\<rbrakk> \<Longrightarrow> ?Q124 target s \<and> s' \<in> ?Q'124 target proof (prove)
goal (2 subgoals):
 1. \<And>target. target = tcb_ptr_to_ctcb_ptr t \<Longrightarrow> ccorres dc xfdc (?A130 target) (?C'130 target) [SKIP] (do curDom <- curDomain;
targetDom <- threadGet tcbDomain t;
action <- getSchedulerAction;
if targetDom \<noteq> curDom then tcbSchedEnqueue t else if action \<noteq> ResumeCurrentThread then do y <- rescheduleRequired;
tcbSchedEnqueue t
od else setSchedulerAction (SwitchToThread t)
od) (IF \<acute>ksCurDomain \<noteq> h_val (hrs_mem \<acute>t_hrs) (PTR(32 word) &(target\<rightarrow>[''tcbDomain_C''])) THEN
  CALL tcbSchedEnqueue_'proc(target)
ELSE
  IF \<acute>ksSchedulerAction \<noteq> NULL THEN
  CALL rescheduleRequired_'proc();;
CALL tcbSchedEnqueue_'proc(target)
ELSE
  \<acute>ksSchedulerAction :== target
FI
FI)
 2. \<And>target s s'. \<lbrakk>target = tcb_ptr_to_ctcb_ptr t; (s, s') \<in> rf_sr; (Invariants_H.valid_queues and (\<lambda>s. weak_sch_act_wf (ksSchedulerAction s) s) and st_tcb_at' runnable' t and (\<lambda>s. ksCurDomain s \<le> maxDomain) and valid_objs') s; s' \<in> UNIV\<rbrakk> \<Longrightarrow> (?A130 target and tcb_at' (ctcb_ptr_to_tcb_ptr target)) s \<and> s' \<in> ?C'130 target \<inter> \<lbrace>True\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<And>target curDom. target = tcb_ptr_to_ctcb_ptr t \<Longrightarrow> ccorres dc xfdc (?P132 target curDom) (?P'132 target curDom) [SKIP] (do targetDom <- threadGet tcbDomain t;
action <- getSchedulerAction;
if targetDom \<noteq> curDom then tcbSchedEnqueue t else if action \<noteq> ResumeCurrentThread then do y <- rescheduleRequired;
tcbSchedEnqueue t
od else setSchedulerAction (SwitchToThread t)
od) (IF \<acute>ksCurDomain \<noteq> h_val (hrs_mem \<acute>t_hrs) (PTR(32 word) &(target\<rightarrow>[''tcbDomain_C''])) THEN
  CALL tcbSchedEnqueue_'proc(target)
ELSE
  IF \<acute>ksSchedulerAction \<noteq> NULL THEN
  CALL rescheduleRequired_'proc();;
CALL tcbSchedEnqueue_'proc(target)
ELSE
  \<acute>ksSchedulerAction :== target
FI
FI)
 2. \<And>target s s'. \<lbrakk>target = tcb_ptr_to_ctcb_ptr t; (s, s') \<in> rf_sr; (Invariants_H.valid_queues and (\<lambda>s. weak_sch_act_wf (ksSchedulerAction s) s) and st_tcb_at' runnable' t and (\<lambda>s. ksCurDomain s \<le> maxDomain) and valid_objs') s; s' \<in> UNIV\<rbrakk> \<Longrightarrow> ((\<lambda>s. \<forall>rv. ksCurDomain s = rv \<longrightarrow> ?P132 target rv s) and tcb_at' (ctcb_ptr_to_tcb_ptr target)) s \<and> s' \<in> {s. \<forall>rv. ksCurDomain_' (globals s) = UCAST(8 \<rightarrow> 32) rv \<longrightarrow> s \<in> ?P'132 target rv} \<inter> \<lbrace>True\<rbrace> proof (prove)
goal (3 subgoals):
 1. \<And>target curDom targetDom. target = tcb_ptr_to_ctcb_ptr t \<Longrightarrow> ccorres dc xfdc (?Q134 target curDom targetDom) (?Q'134 target curDom targetDom) [SKIP] (do action <- getSchedulerAction;
if targetDom \<noteq> curDom then tcbSchedEnqueue t else if action \<noteq> ResumeCurrentThread then do y <- rescheduleRequired;
tcbSchedEnqueue t
od else setSchedulerAction (SwitchToThread t)
od) (IF \<acute>ksCurDomain \<noteq> h_val (hrs_mem \<acute>t_hrs) (PTR(32 word) &(target\<rightarrow>[''tcbDomain_C''])) THEN
  CALL tcbSchedEnqueue_'proc(target)
ELSE
  IF \<acute>ksSchedulerAction \<noteq> NULL THEN
  CALL rescheduleRequired_'proc();;
CALL tcbSchedEnqueue_'proc(target)
ELSE
  \<acute>ksSchedulerAction :== target
FI
FI)
 2. \<And>target curDom. target = tcb_ptr_to_ctcb_ptr t \<Longrightarrow> \<lbrace>?P132 target curDom\<rbrace> threadGet tcbDomain t \<lbrace>?Q134 target curDom\<rbrace>
 3. \<And>target s s'. \<lbrakk>target = tcb_ptr_to_ctcb_ptr t; (s, s') \<in> rf_sr; (Invariants_H.valid_queues and (\<lambda>s. weak_sch_act_wf (ksSchedulerAction s) s) and st_tcb_at' runnable' t and (\<lambda>s. ksCurDomain s \<le> maxDomain) and valid_objs') s; s' \<in> UNIV\<rbrakk> \<Longrightarrow> ((\<lambda>s. \<forall>rv. ksCurDomain s = rv \<longrightarrow> ?P132 target rv s) and tcb_at' (ctcb_ptr_to_tcb_ptr target)) s \<and> s' \<in> {s. \<forall>rv. ksCurDomain_' (globals s) = UCAST(8 \<rightarrow> 32) rv \<longrightarrow> s \<in> {s'. \<forall>rva. s' \<in> ?Q'134 target rv rva}} \<inter> \<lbrace>True\<rbrace> proof (prove)
goal (4 subgoals):
 1. \<And>target curDom targetDom sact. target = tcb_ptr_to_ctcb_ptr t \<Longrightarrow> ccorres dc xfdc (?Q141 target curDom targetDom sact) (?Q'141 target curDom targetDom sact) [SKIP] (if targetDom \<noteq> curDom then tcbSchedEnqueue t else if sact \<noteq> ResumeCurrentThread then do y <- rescheduleRequired;
tcbSchedEnqueue t
od else setSchedulerAction (SwitchToThread t)) (IF \<acute>ksCurDomain \<noteq> h_val (hrs_mem \<acute>t_hrs) (PTR(32 word) &(target\<rightarrow>[''tcbDomain_C''])) THEN
  CALL tcbSchedEnqueue_'proc(target)
ELSE
  IF \<acute>ksSchedulerAction \<noteq> NULL THEN
  CALL rescheduleRequired_'proc();;
CALL tcbSchedEnqueue_'proc(target)
ELSE
  \<acute>ksSchedulerAction :== target
FI
FI)
 2. \<And>target curDom targetDom. target = tcb_ptr_to_ctcb_ptr t \<Longrightarrow> \<lbrace>?Q134 target curDom targetDom\<rbrace> getSchedulerAction \<lbrace>?Q141 target curDom targetDom\<rbrace>
 3. \<And>target curDom. target = tcb_ptr_to_ctcb_ptr t \<Longrightarrow> \<lbrace>?P132 target curDom\<rbrace> threadGet tcbDomain t \<lbrace>?Q134 target curDom\<rbrace>
 4. \<And>target s s'. \<lbrakk>target = tcb_ptr_to_ctcb_ptr t; (s, s') \<in> rf_sr; (Invariants_H.valid_queues and (\<lambda>s. weak_sch_act_wf (ksSchedulerAction s) s) and st_tcb_at' runnable' t and (\<lambda>s. ksCurDomain s \<le> maxDomain) and valid_objs') s; s' \<in> UNIV\<rbrakk> \<Longrightarrow> ((\<lambda>s. \<forall>rv. ksCurDomain s = rv \<longrightarrow> ?P132 target rv s) and tcb_at' (ctcb_ptr_to_tcb_ptr target)) s \<and> s' \<in> {s. \<forall>rv. ksCurDomain_' (globals s) = UCAST(8 \<rightarrow> 32) rv \<longrightarrow> s \<in> {s'. \<forall>rva. s' \<in> {s'. \<forall>rvb. s' \<in> ?Q'141 target rv rva rvb}}} \<inter> \<lbrace>True\<rbrace> proof (prove)
goal (5 subgoals):
 1. \<And>target curDom targetDom sact. target = tcb_ptr_to_ctcb_ptr t \<Longrightarrow> \<forall>s s'. (s, s') \<in> rf_sr \<and> (curDom = ksCurDomain s \<and> obj_at' (\<lambda>tcb. targetDom = tcbDomain tcb) t s) \<and> s' \<in> UNIV \<longrightarrow> (s' \<in> \<lbrace>\<acute>ksCurDomain \<noteq> h_val (hrs_mem \<acute>t_hrs) (PTR(32 word) &(target\<rightarrow>[''tcbDomain_C'']))\<rbrace>) = (s' \<in> \<lbrace>targetDom \<noteq> curDom\<rbrace>)
 2. \<And>target curDom targetDom sact. target = tcb_ptr_to_ctcb_ptr t \<Longrightarrow> ccorres dc xfdc (?P147 target curDom targetDom sact) (?P'147 target curDom targetDom sact) [SKIP] (if targetDom \<noteq> curDom then tcbSchedEnqueue t else if sact \<noteq> ResumeCurrentThread then do y <- rescheduleRequired;
tcbSchedEnqueue t
od else setSchedulerAction (SwitchToThread t)) (IF targetDom \<noteq> curDom THEN
  CALL tcbSchedEnqueue_'proc(target)
ELSE
  IF \<acute>ksSchedulerAction \<noteq> NULL THEN
  CALL rescheduleRequired_'proc();;
CALL tcbSchedEnqueue_'proc(target)
ELSE
  \<acute>ksSchedulerAction :== target
FI
FI)
 3. \<And>target curDom targetDom. target = tcb_ptr_to_ctcb_ptr t \<Longrightarrow> \<lbrace>?Q134 target curDom targetDom\<rbrace> getSchedulerAction \<lbrace>\<lambda>sact. ?P147 target curDom targetDom sact and (\<lambda>s. curDom = ksCurDomain s \<and> obj_at' (\<lambda>tcb. targetDom = tcbDomain tcb) t s)\<rbrace>
 4. \<And>target curDom. target = tcb_ptr_to_ctcb_ptr t \<Longrightarrow> \<lbrace>?P132 target curDom\<rbrace> threadGet tcbDomain t \<lbrace>?Q134 target curDom\<rbrace>
 5. \<And>target s s'. \<lbrakk>target = tcb_ptr_to_ctcb_ptr t; (s, s') \<in> rf_sr; (Invariants_H.valid_queues and (\<lambda>s. weak_sch_act_wf (ksSchedulerAction s) s) and st_tcb_at' runnable' t and (\<lambda>s. ksCurDomain s \<le> maxDomain) and valid_objs') s; s' \<in> UNIV\<rbrakk> \<Longrightarrow> ((\<lambda>s. \<forall>rv. ksCurDomain s = rv \<longrightarrow> ?P132 target rv s) and tcb_at' (ctcb_ptr_to_tcb_ptr target)) s \<and> s' \<in> {s. \<forall>rv. ksCurDomain_' (globals s) = UCAST(8 \<rightarrow> 32) rv \<longrightarrow> s \<in> {s'. \<forall>rva. s' \<in> {s'. \<forall>rvb. s' \<in> ?P'147 target rv rva rvb \<inter> UNIV}}} \<inter> \<lbrace>True\<rbrace> proof (prove)
goal (1 subgoal):
 1. target_ = tcb_ptr_to_ctcb_ptr t \<Longrightarrow> \<forall>s s'. (s, s') \<in> rf_sr \<and> (curDom_ = ksCurDomain s \<and> obj_at' (\<lambda>tcb. targetDom_ = tcbDomain tcb) t s) \<and> s' \<in> UNIV \<longrightarrow> (s' \<in> \<lbrace>\<acute>ksCurDomain \<noteq> h_val (hrs_mem \<acute>t_hrs) (PTR(32 word) &(target_\<rightarrow>[''tcbDomain_C'']))\<rbrace>) = (s' \<in> \<lbrace>targetDom_ \<noteq> curDom_\<rbrace>) proof (prove)
goal (1 subgoal):
 1. \<And>s s'. \<lbrakk>target_ = tcb_ptr_to_ctcb_ptr t; (s, s') \<in> rf_sr; curDom_ = ksCurDomain s; obj_at' (\<lambda>tcb. targetDom_ = tcbDomain tcb) t s\<rbrakk> \<Longrightarrow> (ksCurDomain_' (globals s') = h_val (hrs_mem (t_hrs_' (globals s'))) (PTR(32 word) &(tcb_ptr_to_ctcb_ptr t\<rightarrow>[''tcbDomain_C'']))) = (targetDom_ = ksCurDomain s) proof (prove)
goal (1 subgoal):
 1. \<And>s s' ko. \<lbrakk>target_ = tcb_ptr_to_ctcb_ptr t; (s, s') \<in> rf_sr; curDom_ = ksCurDomain s; ko_at' ko t s; targetDom_ = tcbDomain ko\<rbrakk> \<Longrightarrow> (UCAST(8 \<rightarrow> 32) (ksCurDomain s) = h_val (hrs_mem (t_hrs_' (globals s'))) (PTR(32 word) &(tcb_ptr_to_ctcb_ptr t\<rightarrow>[''tcbDomain_C'']))) = (tcbDomain ko = ksCurDomain s) proof (prove)
goal (1 subgoal):
 1. \<And>s s' ko ko'. \<lbrakk>target_ = tcb_ptr_to_ctcb_ptr t; (s, s') \<in> rf_sr; curDom_ = ksCurDomain s; ko_at' ko t s; targetDom_ = tcbDomain ko; cslift s' (tcb_ptr_to_ctcb_ptr t) = Some ko'; ctcb_relation ko ko'\<rbrakk> \<Longrightarrow> (UCAST(8 \<rightarrow> 32) (ksCurDomain s) = tcbDomain_C ko') = (tcbDomain ko = ksCurDomain s) proof (prove)
goal (1 subgoal):
 1. \<And>s s' ko ko'. \<lbrakk>target_ = tcb_ptr_to_ctcb_ptr t; (s, s') \<in> rf_sr; curDom_ = ksCurDomain s; ko_at' ko t s; targetDom_ = tcbDomain ko; cslift s' (tcb_ptr_to_ctcb_ptr t) = Some ko'; unat (tcbDomain_C ko') = unat (tcbDomain ko)\<rbrakk> \<Longrightarrow> (UCAST(8 \<rightarrow> 32) (ksCurDomain s) = tcbDomain_C ko') = (tcbDomain ko = ksCurDomain s) proof (prove)
goal (1 subgoal):
 1. \<And>s s' ko ko' n na nb nc nd ne nf ng nh ni. \<lbrakk>target_ = tcb_ptr_to_ctcb_ptr t; (s, s') \<in> rf_sr; n < 2 ^ LENGTH(8); nc < 2 ^ LENGTH(8); nc = n; ko_at' ko t s; na < 2 ^ LENGTH(8); nd < 2 ^ LENGTH(8); nd = na; cslift s' (tcb_ptr_to_ctcb_ptr t) = Some ko'; nb < 2 ^ LENGTH(8); ne < 2 ^ LENGTH(32); ne = nb; nf < 2 ^ LENGTH(32); ng < 2 ^ LENGTH(32); nh < 2 ^ LENGTH(8); ni < 2 ^ LENGTH(8); unat (ksCurDomain s) = n; unat curDom_ = nc; unat (tcbDomain ko) = na; unat targetDom_ = nd; unat (tcbDomain ko) = nb; unat (tcbDomain_C ko') = ne; unat (UCAST(8 \<rightarrow> 32) (ksCurDomain s)) = nf; unat (tcbDomain_C ko') = ng; unat (tcbDomain ko) = nh; unat (ksCurDomain s) = ni\<rbrakk> \<Longrightarrow> (nf = ng) = (nh = ni) proof (prove)
goal:
No subgoals! proof (prove)
goal (4 subgoals):
 1. \<And>target curDom targetDom sact. target = tcb_ptr_to_ctcb_ptr t \<Longrightarrow> ccorres dc xfdc (?P147 target curDom targetDom sact) (?P'147 target curDom targetDom sact) [SKIP] (if targetDom \<noteq> curDom then tcbSchedEnqueue t else if sact \<noteq> ResumeCurrentThread then do y <- rescheduleRequired;
tcbSchedEnqueue t
od else setSchedulerAction (SwitchToThread t)) (IF targetDom \<noteq> curDom THEN
  CALL tcbSchedEnqueue_'proc(target)
ELSE
  IF \<acute>ksSchedulerAction \<noteq> NULL THEN
  CALL rescheduleRequired_'proc();;
CALL tcbSchedEnqueue_'proc(target)
ELSE
  \<acute>ksSchedulerAction :== target
FI
FI)
 2. \<And>target curDom targetDom. target = tcb_ptr_to_ctcb_ptr t \<Longrightarrow> \<lbrace>?Q134 target curDom targetDom\<rbrace> getSchedulerAction \<lbrace>\<lambda>sact. ?P147 target curDom targetDom sact and (\<lambda>s. curDom = ksCurDomain s \<and> obj_at' (\<lambda>tcb. targetDom = tcbDomain tcb) t s)\<rbrace>
 3. \<And>target curDom. target = tcb_ptr_to_ctcb_ptr t \<Longrightarrow> \<lbrace>?P132 target curDom\<rbrace> threadGet tcbDomain t \<lbrace>?Q134 target curDom\<rbrace>
 4. \<And>target s s'. \<lbrakk>target = tcb_ptr_to_ctcb_ptr t; (s, s') \<in> rf_sr; (Invariants_H.valid_queues and (\<lambda>s. weak_sch_act_wf (ksSchedulerAction s) s) and st_tcb_at' runnable' t and (\<lambda>s. ksCurDomain s \<le> maxDomain) and valid_objs') s; s' \<in> UNIV\<rbrakk> \<Longrightarrow> ((\<lambda>s. \<forall>rv. ksCurDomain s = rv \<longrightarrow> ?P132 target rv s) and tcb_at' (ctcb_ptr_to_tcb_ptr target)) s \<and> s' \<in> {s. \<forall>rv. ksCurDomain_' (globals s) = UCAST(8 \<rightarrow> 32) rv \<longrightarrow> s \<in> {s'. \<forall>rva. s' \<in> {s'. \<forall>rvb. s' \<in> ?P'147 target rv rva rvb \<inter> UNIV}}} \<inter> \<lbrace>True\<rbrace> proof (prove)
goal (5 subgoals):
 1. \<And>target curDom targetDom sact. target = tcb_ptr_to_ctcb_ptr t \<Longrightarrow> ccorres dc xfdc (?Pt148 target curDom targetDom sact) (?Rt148 target curDom targetDom sact) [SKIP] (tcbSchedEnqueue t) (CALL tcbSchedEnqueue_'proc(target))
 2. \<And>target curDom targetDom sact. target = tcb_ptr_to_ctcb_ptr t \<Longrightarrow> ccorres dc xfdc (?Pf148 target curDom targetDom sact) (?Rf148 target curDom targetDom sact) [SKIP] (if sact \<noteq> ResumeCurrentThread then do y <- rescheduleRequired;
tcbSchedEnqueue t
od else setSchedulerAction (SwitchToThread t)) (IF \<acute>ksSchedulerAction \<noteq> NULL THEN
  CALL rescheduleRequired_'proc();;
CALL tcbSchedEnqueue_'proc(target)
ELSE
  \<acute>ksSchedulerAction :== target
FI)
 3. \<And>target curDom targetDom. target = tcb_ptr_to_ctcb_ptr t \<Longrightarrow> \<lbrace>?Q134 target curDom targetDom\<rbrace> getSchedulerAction \<lbrace>\<lambda>sact. (\<lambda>_. True) and (\<lambda>s. targetDom \<noteq> curDom \<longrightarrow> ?Pt148 target curDom targetDom sact s) and (\<lambda>s. \<not> targetDom \<noteq> curDom \<longrightarrow> ?Pf148 target curDom targetDom sact s) and (\<lambda>s. curDom = ksCurDomain s \<and> obj_at' (\<lambda>tcb. targetDom = tcbDomain tcb) t s)\<rbrace>
 4. \<And>target curDom. target = tcb_ptr_to_ctcb_ptr t \<Longrightarrow> \<lbrace>?P132 target curDom\<rbrace> threadGet tcbDomain t \<lbrace>?Q134 target curDom\<rbrace>
 5. \<And>target s s'. \<lbrakk>target = tcb_ptr_to_ctcb_ptr t; (s, s') \<in> rf_sr; (Invariants_H.valid_queues and (\<lambda>s. weak_sch_act_wf (ksSchedulerAction s) s) and st_tcb_at' runnable' t and (\<lambda>s. ksCurDomain s \<le> maxDomain) and valid_objs') s; s' \<in> UNIV\<rbrakk> \<Longrightarrow> ((\<lambda>s. \<forall>rv. ksCurDomain s = rv \<longrightarrow> ?P132 target rv s) and tcb_at' (ctcb_ptr_to_tcb_ptr target)) s \<and> s' \<in> {s. \<forall>rv. ksCurDomain_' (globals s) = UCAST(8 \<rightarrow> 32) rv \<longrightarrow> s \<in> {s'. \<forall>rva. s' \<in> {s'. \<forall>rvb. s' \<in> {s. (s \<in> \<lbrace>rva \<noteq> rv\<rbrace> \<longrightarrow> s \<in> ?Rt148 target rv rva rvb) \<and> (s \<notin> \<lbrace>rva \<noteq> rv\<rbrace> \<longrightarrow> s \<in> ?Rf148 target rv rva rvb)} \<inter> UNIV}}} \<inter> \<lbrace>True\<rbrace> proof (prove)
goal (4 subgoals):
 1. \<And>target curDom targetDom sact. target = tcb_ptr_to_ctcb_ptr t \<Longrightarrow> ccorres dc xfdc (?Pf148 target curDom targetDom sact) (?Rf148 target curDom targetDom sact) [SKIP] (if sact \<noteq> ResumeCurrentThread then do y <- rescheduleRequired;
tcbSchedEnqueue t
od else setSchedulerAction (SwitchToThread t)) (IF \<acute>ksSchedulerAction \<noteq> NULL THEN
  CALL rescheduleRequired_'proc();;
CALL tcbSchedEnqueue_'proc(target)
ELSE
  \<acute>ksSchedulerAction :== target
FI)
 2. \<And>target curDom targetDom. target = tcb_ptr_to_ctcb_ptr t \<Longrightarrow> \<lbrace>?Q134 target curDom targetDom\<rbrace> getSchedulerAction \<lbrace>\<lambda>sact. (\<lambda>_. True) and (\<lambda>s. targetDom \<noteq> curDom \<longrightarrow> (Invariants_H.valid_queues and tcb_at' t and valid_objs') s) and (\<lambda>s. \<not> targetDom \<noteq> curDom \<longrightarrow> ?Pf148 target curDom targetDom sact s) and (\<lambda>s. curDom = ksCurDomain s \<and> obj_at' (\<lambda>tcb. targetDom = tcbDomain tcb) t s)\<rbrace>
 3. \<And>target curDom. target = tcb_ptr_to_ctcb_ptr t \<Longrightarrow> \<lbrace>?P132 target curDom\<rbrace> threadGet tcbDomain t \<lbrace>?Q134 target curDom\<rbrace>
 4. \<And>target s s'. \<lbrakk>target = tcb_ptr_to_ctcb_ptr t; (s, s') \<in> rf_sr; (Invariants_H.valid_queues and (\<lambda>s. weak_sch_act_wf (ksSchedulerAction s) s) and st_tcb_at' runnable' t and (\<lambda>s. ksCurDomain s \<le> maxDomain) and valid_objs') s; s' \<in> UNIV\<rbrakk> \<Longrightarrow> ((\<lambda>s. \<forall>rv. ksCurDomain s = rv \<longrightarrow> ?P132 target rv s) and tcb_at' (ctcb_ptr_to_tcb_ptr target)) s \<and> s' \<in> {s. \<forall>rv. ksCurDomain_' (globals s) = UCAST(8 \<rightarrow> 32) rv \<longrightarrow> s \<in> {s'. \<forall>rva. s' \<in> {s'. \<forall>rvb. s' \<in> {s. (s \<in> \<lbrace>rva \<noteq> rv\<rbrace> \<longrightarrow> s \<in> {s. tcb_'_update (\<lambda>_. target) s \<in> UNIV \<inter> \<lbrace>\<acute>tcb = tcb_ptr_to_ctcb_ptr t\<rbrace>}) \<and> (s \<notin> \<lbrace>rva \<noteq> rv\<rbrace> \<longrightarrow> s \<in> ?Rf148 target rv rva rvb)} \<inter> UNIV}}} \<inter> \<lbrace>True\<rbrace> proof (prove)
goal (6 subgoals):
 1. \<And>target curDom targetDom sact. target = tcb_ptr_to_ctcb_ptr t \<Longrightarrow> \<forall>s s'. (s, s') \<in> rf_sr \<and> sact = ksSchedulerAction s \<and> weak_sch_act_wf (ksSchedulerAction s) s \<longrightarrow> (sact \<noteq> ResumeCurrentThread) = (s' \<in> \<lbrace>\<acute>ksSchedulerAction \<noteq> NULL\<rbrace>)
 2. \<And>target curDom targetDom sact. target = tcb_ptr_to_ctcb_ptr t \<Longrightarrow> ccorres dc xfdc (?Pt160 target curDom targetDom sact) (?Rt160 target curDom targetDom sact) [SKIP] (do y <- rescheduleRequired;
tcbSchedEnqueue t
od) (CALL rescheduleRequired_'proc();;
CALL tcbSchedEnqueue_'proc(target))
 3. \<And>target curDom targetDom sact. target = tcb_ptr_to_ctcb_ptr t \<Longrightarrow> ccorres dc xfdc (?Pf160 target curDom targetDom sact) (?Rf160 target curDom targetDom sact) [SKIP] (setSchedulerAction (SwitchToThread t)) (\<acute>ksSchedulerAction :== target)
 4. \<And>target curDom targetDom. target = tcb_ptr_to_ctcb_ptr t \<Longrightarrow> \<lbrace>?Q134 target curDom targetDom\<rbrace> getSchedulerAction \<lbrace>\<lambda>sact. (\<lambda>_. True) and (\<lambda>s. targetDom \<noteq> curDom \<longrightarrow> (Invariants_H.valid_queues and tcb_at' t and valid_objs') s) and (\<lambda>s. \<not> targetDom \<noteq> curDom \<longrightarrow> ((\<lambda>s. sact = ksSchedulerAction s \<and> weak_sch_act_wf (ksSchedulerAction s) s) and (\<lambda>s. sact \<noteq> ResumeCurrentThread \<longrightarrow> ?Pt160 target curDom targetDom sact s) and (\<lambda>s. \<not> sact \<noteq> ResumeCurrentThread \<longrightarrow> ?Pf160 target curDom targetDom sact s)) s) and (\<lambda>s. curDom = ksCurDomain s \<and> obj_at' (\<lambda>tcb. targetDom = tcbDomain tcb) t s)\<rbrace>
 5. \<And>target curDom. target = tcb_ptr_to_ctcb_ptr t \<Longrightarrow> \<lbrace>?P132 target curDom\<rbrace> threadGet tcbDomain t \<lbrace>?Q134 target curDom\<rbrace>
 6. \<And>target s s'. \<lbrakk>target = tcb_ptr_to_ctcb_ptr t; (s, s') \<in> rf_sr; (Invariants_H.valid_queues and (\<lambda>s. weak_sch_act_wf (ksSchedulerAction s) s) and st_tcb_at' runnable' t and (\<lambda>s. ksCurDomain s \<le> maxDomain) and valid_objs') s; s' \<in> UNIV\<rbrakk> \<Longrightarrow> ((\<lambda>s. \<forall>rv. ksCurDomain s = rv \<longrightarrow> ?P132 target rv s) and tcb_at' (ctcb_ptr_to_tcb_ptr target)) s \<and> s' \<in> {s. \<forall>rv. ksCurDomain_' (globals s) = UCAST(8 \<rightarrow> 32) rv \<longrightarrow> s \<in> {s'. \<forall>rva. s' \<in> {s'. \<forall>rvb. s' \<in> {s. (s \<in> \<lbrace>rva \<noteq> rv\<rbrace> \<longrightarrow> s \<in> {s. tcb_'_update (\<lambda>_. target) s \<in> UNIV \<inter> \<lbrace>\<acute>tcb = tcb_ptr_to_ctcb_ptr t\<rbrace>}) \<and> (s \<notin> \<lbrace>rva \<noteq> rv\<rbrace> \<longrightarrow> s \<in> ?Rt160 target rv rva rvb \<inter> \<lbrace>\<acute>ksSchedulerAction \<noteq> NULL\<rbrace> \<union> ?Rf160 target rv rva rvb \<inter> - \<lbrace>\<acute>ksSchedulerAction \<noteq> NULL\<rbrace>)} \<inter> UNIV}}} \<inter> \<lbrace>True\<rbrace> proof (prove)
goal (5 subgoals):
 1. \<And>target curDom targetDom sact. target = tcb_ptr_to_ctcb_ptr t \<Longrightarrow> ccorres dc xfdc (?Pt160 target curDom targetDom sact) (?Rt160 target curDom targetDom sact) [SKIP] (do y <- rescheduleRequired;
tcbSchedEnqueue t
od) (CALL rescheduleRequired_'proc();;
CALL tcbSchedEnqueue_'proc(target))
 2. \<And>target curDom targetDom sact. target = tcb_ptr_to_ctcb_ptr t \<Longrightarrow> ccorres dc xfdc (?Pf160 target curDom targetDom sact) (?Rf160 target curDom targetDom sact) [SKIP] (setSchedulerAction (SwitchToThread t)) (\<acute>ksSchedulerAction :== target)
 3. \<And>target curDom targetDom. target = tcb_ptr_to_ctcb_ptr t \<Longrightarrow> \<lbrace>?Q134 target curDom targetDom\<rbrace> getSchedulerAction \<lbrace>\<lambda>sact. (\<lambda>_. True) and (\<lambda>s. targetDom \<noteq> curDom \<longrightarrow> (Invariants_H.valid_queues and tcb_at' t and valid_objs') s) and (\<lambda>s. \<not> targetDom \<noteq> curDom \<longrightarrow> ((\<lambda>s. sact = ksSchedulerAction s \<and> weak_sch_act_wf (ksSchedulerAction s) s) and (\<lambda>s. sact \<noteq> ResumeCurrentThread \<longrightarrow> ?Pt160 target curDom targetDom sact s) and (\<lambda>s. \<not> sact \<noteq> ResumeCurrentThread \<longrightarrow> ?Pf160 target curDom targetDom sact s)) s) and (\<lambda>s. curDom = ksCurDomain s \<and> obj_at' (\<lambda>tcb. targetDom = tcbDomain tcb) t s)\<rbrace>
 4. \<And>target curDom. target = tcb_ptr_to_ctcb_ptr t \<Longrightarrow> \<lbrace>?P132 target curDom\<rbrace> threadGet tcbDomain t \<lbrace>?Q134 target curDom\<rbrace>
 5. \<And>target s s'. \<lbrakk>target = tcb_ptr_to_ctcb_ptr t; (s, s') \<in> rf_sr; (Invariants_H.valid_queues and (\<lambda>s. weak_sch_act_wf (ksSchedulerAction s) s) and st_tcb_at' runnable' t and (\<lambda>s. ksCurDomain s \<le> maxDomain) and valid_objs') s; s' \<in> UNIV\<rbrakk> \<Longrightarrow> ((\<lambda>s. \<forall>rv. ksCurDomain s = rv \<longrightarrow> ?P132 target rv s) and tcb_at' (ctcb_ptr_to_tcb_ptr target)) s \<and> s' \<in> {s. \<forall>rv. ksCurDomain_' (globals s) = UCAST(8 \<rightarrow> 32) rv \<longrightarrow> s \<in> {s'. \<forall>rva. s' \<in> {s'. \<forall>rvb. s' \<in> {s. (s \<in> \<lbrace>rva \<noteq> rv\<rbrace> \<longrightarrow> s \<in> {s. tcb_'_update (\<lambda>_. target) s \<in> UNIV \<inter> \<lbrace>\<acute>tcb = tcb_ptr_to_ctcb_ptr t\<rbrace>}) \<and> (s \<notin> \<lbrace>rva \<noteq> rv\<rbrace> \<longrightarrow> s \<in> ?Rt160 target rv rva rvb \<inter> \<lbrace>\<acute>ksSchedulerAction \<noteq> NULL\<rbrace> \<union> ?Rf160 target rv rva rvb \<inter> - \<lbrace>\<acute>ksSchedulerAction \<noteq> NULL\<rbrace>)} \<inter> UNIV}}} \<inter> \<lbrace>True\<rbrace> proof (prove)
goal (7 subgoals):
 1. \<And>target curDom targetDom sact rv xfdca. \<lbrakk>target = tcb_ptr_to_ctcb_ptr t; dc rv xfdca\<rbrakk> \<Longrightarrow> ccorres dc xfdc (?Q196 target curDom targetDom sact rv) (?Q'196 target curDom targetDom sact rv xfdca) [SKIP] (tcbSchedEnqueue t) (CALL tcbSchedEnqueue_'proc(target))
 2. \<And>target curDom targetDom sact. target = tcb_ptr_to_ctcb_ptr t \<Longrightarrow> \<lbrace>?R196 target curDom targetDom sact\<rbrace> rescheduleRequired \<lbrace>?Q196 target curDom targetDom sact\<rbrace>
 3. \<And>target curDom targetDom sact. target = tcb_ptr_to_ctcb_ptr t \<Longrightarrow> \<Gamma>\<turnstile>\<^bsub>/UNIV\<^esub> (?R'196 target curDom targetDom sact) CALL rescheduleRequired_'proc() {s. \<forall>rv. dc rv (xfdc s) \<longrightarrow> s \<in> ?Q'196 target curDom targetDom sact rv (xfdc s)}
 4. \<And>target curDom targetDom sact. target = tcb_ptr_to_ctcb_ptr t \<Longrightarrow> ccorres dc xfdc (?Pf160 target curDom targetDom sact) (?Rf160 target curDom targetDom sact) [SKIP] (setSchedulerAction (SwitchToThread t)) (\<acute>ksSchedulerAction :== target)
 5. \<And>target curDom targetDom. target = tcb_ptr_to_ctcb_ptr t \<Longrightarrow> \<lbrace>?Q134 target curDom targetDom\<rbrace> getSchedulerAction \<lbrace>\<lambda>sact. (\<lambda>_. True) and (\<lambda>s. targetDom \<noteq> curDom \<longrightarrow> (Invariants_H.valid_queues and tcb_at' t and valid_objs') s) and (\<lambda>s. \<not> targetDom \<noteq> curDom \<longrightarrow> ((\<lambda>s. sact = ksSchedulerAction s \<and> weak_sch_act_wf (ksSchedulerAction s) s) and (\<lambda>s. sact \<noteq> ResumeCurrentThread \<longrightarrow> (Invariants_H.valid_queues and (\<lambda>s. weak_sch_act_wf (ksSchedulerAction s) s) and valid_objs' and ?R196 target curDom targetDom sact) s) and (\<lambda>s. \<not> sact \<noteq> ResumeCurrentThread \<longrightarrow> ?Pf160 target curDom targetDom sact s)) s) and (\<lambda>s. curDom = ksCurDomain s \<and> obj_at' (\<lambda>tcb. targetDom = tcbDomain tcb) t s)\<rbrace>
 6. \<And>target curDom. target = tcb_ptr_to_ctcb_ptr t \<Longrightarrow> \<lbrace>?P132 target curDom\<rbrace> threadGet tcbDomain t \<lbrace>?Q134 target curDom\<rbrace>
 7. \<And>target s s'. \<lbrakk>target = tcb_ptr_to_ctcb_ptr t; (s, s') \<in> rf_sr; (Invariants_H.valid_queues and (\<lambda>s. weak_sch_act_wf (ksSchedulerAction s) s) and st_tcb_at' runnable' t and (\<lambda>s. ksCurDomain s \<le> maxDomain) and valid_objs') s; s' \<in> UNIV\<rbrakk> \<Longrightarrow> ((\<lambda>s. \<forall>rv. ksCurDomain s = rv \<longrightarrow> ?P132 target rv s) and tcb_at' (ctcb_ptr_to_tcb_ptr target)) s \<and> s' \<in> {s. \<forall>rv. ksCurDomain_' (globals s) = UCAST(8 \<rightarrow> 32) rv \<longrightarrow> s \<in> {s'. \<forall>rva. s' \<in> {s'. \<forall>rvb. s' \<in> {s. (s \<in> \<lbrace>rva \<noteq> rv\<rbrace> \<longrightarrow> s \<in> {s. tcb_'_update (\<lambda>_. target) s \<in> UNIV \<inter> \<lbrace>\<acute>tcb = tcb_ptr_to_ctcb_ptr t\<rbrace>}) \<and> (s \<notin> \<lbrace>rva \<noteq> rv\<rbrace> \<longrightarrow> s \<in> {s. s \<in> UNIV} \<inter> ?R'196 target rv rva rvb \<inter> \<lbrace>\<acute>ksSchedulerAction \<noteq> NULL\<rbrace> \<union> ?Rf160 target rv rva rvb \<inter> - \<lbrace>\<acute>ksSchedulerAction \<noteq> NULL\<rbrace>)} \<inter> UNIV}}} \<inter> \<lbrace>True\<rbrace> proof (prove)
goal (6 subgoals):
 1. \<And>target curDom targetDom sact. target = tcb_ptr_to_ctcb_ptr t \<Longrightarrow> \<lbrace>?R196 target curDom targetDom sact\<rbrace> rescheduleRequired \<lbrace>\<lambda>rv. Invariants_H.valid_queues and tcb_at' t and valid_objs'\<rbrace>
 2. \<And>target curDom targetDom sact. target = tcb_ptr_to_ctcb_ptr t \<Longrightarrow> \<Gamma>\<turnstile>\<^bsub>/UNIV\<^esub> (?R'196 target curDom targetDom sact) CALL rescheduleRequired_'proc() {s. \<forall>rv. dc rv (xfdc s) \<longrightarrow> s \<in> {s. tcb_'_update (\<lambda>_. target) s \<in> UNIV \<inter> \<lbrace>\<acute>tcb = tcb_ptr_to_ctcb_ptr t\<rbrace>}}
 3. \<And>target curDom targetDom sact. target = tcb_ptr_to_ctcb_ptr t \<Longrightarrow> ccorres dc xfdc (?Pf160 target curDom targetDom sact) (?Rf160 target curDom targetDom sact) [SKIP] (setSchedulerAction (SwitchToThread t)) (\<acute>ksSchedulerAction :== target)
 4. \<And>target curDom targetDom. target = tcb_ptr_to_ctcb_ptr t \<Longrightarrow> \<lbrace>?Q134 target curDom targetDom\<rbrace> getSchedulerAction \<lbrace>\<lambda>sact. (\<lambda>_. True) and (\<lambda>s. targetDom \<noteq> curDom \<longrightarrow> (Invariants_H.valid_queues and tcb_at' t and valid_objs') s) and (\<lambda>s. \<not> targetDom \<noteq> curDom \<longrightarrow> ((\<lambda>s. sact = ksSchedulerAction s \<and> weak_sch_act_wf (ksSchedulerAction s) s) and (\<lambda>s. sact \<noteq> ResumeCurrentThread \<longrightarrow> (Invariants_H.valid_queues and (\<lambda>s. weak_sch_act_wf (ksSchedulerAction s) s) and valid_objs' and ?R196 target curDom targetDom sact) s) and (\<lambda>s. \<not> sact \<noteq> ResumeCurrentThread \<longrightarrow> ?Pf160 target curDom targetDom sact s)) s) and (\<lambda>s. curDom = ksCurDomain s \<and> obj_at' (\<lambda>tcb. targetDom = tcbDomain tcb) t s)\<rbrace>
 5. \<And>target curDom. target = tcb_ptr_to_ctcb_ptr t \<Longrightarrow> \<lbrace>?P132 target curDom\<rbrace> threadGet tcbDomain t \<lbrace>?Q134 target curDom\<rbrace>
 6. \<And>target s s'. \<lbrakk>target = tcb_ptr_to_ctcb_ptr t; (s, s') \<in> rf_sr; (Invariants_H.valid_queues and (\<lambda>s. weak_sch_act_wf (ksSchedulerAction s) s) and st_tcb_at' runnable' t and (\<lambda>s. ksCurDomain s \<le> maxDomain) and valid_objs') s; s' \<in> UNIV\<rbrakk> \<Longrightarrow> ((\<lambda>s. \<forall>rv. ksCurDomain s = rv \<longrightarrow> ?P132 target rv s) and tcb_at' (ctcb_ptr_to_tcb_ptr target)) s \<and> s' \<in> {s. \<forall>rv. ksCurDomain_' (globals s) = UCAST(8 \<rightarrow> 32) rv \<longrightarrow> s \<in> {s'. \<forall>rva. s' \<in> {s'. \<forall>rvb. s' \<in> {s. (s \<in> \<lbrace>rva \<noteq> rv\<rbrace> \<longrightarrow> s \<in> {s. tcb_'_update (\<lambda>_. target) s \<in> UNIV \<inter> \<lbrace>\<acute>tcb = tcb_ptr_to_ctcb_ptr t\<rbrace>}) \<and> (s \<notin> \<lbrace>rva \<noteq> rv\<rbrace> \<longrightarrow> s \<in> {s. s \<in> UNIV} \<inter> ?R'196 target rv rva rvb \<inter> \<lbrace>\<acute>ksSchedulerAction \<noteq> NULL\<rbrace> \<union> ?Rf160 target rv rva rvb \<inter> - \<lbrace>\<acute>ksSchedulerAction \<noteq> NULL\<rbrace>)} \<inter> UNIV}}} \<inter> \<lbrace>True\<rbrace> proof (prove)
goal (5 subgoals):
 1. \<And>target curDom targetDom sact. target = tcb_ptr_to_ctcb_ptr t \<Longrightarrow> \<Gamma>\<turnstile>\<^bsub>/UNIV\<^esub> (?R'196 target curDom targetDom sact) CALL rescheduleRequired_'proc() {s. \<forall>rv. dc rv (xfdc s) \<longrightarrow> s \<in> {s. tcb_'_update (\<lambda>_. target) s \<in> UNIV \<inter> \<lbrace>\<acute>tcb = tcb_ptr_to_ctcb_ptr t\<rbrace>}}
 2. \<And>target curDom targetDom sact. target = tcb_ptr_to_ctcb_ptr t \<Longrightarrow> ccorres dc xfdc (?Pf160 target curDom targetDom sact) (?Rf160 target curDom targetDom sact) [SKIP] (setSchedulerAction (SwitchToThread t)) (\<acute>ksSchedulerAction :== target)
 3. \<And>target curDom targetDom. target = tcb_ptr_to_ctcb_ptr t \<Longrightarrow> \<lbrace>?Q134 target curDom targetDom\<rbrace> getSchedulerAction \<lbrace>\<lambda>sact. (\<lambda>_. True) and (\<lambda>s. targetDom \<noteq> curDom \<longrightarrow> (Invariants_H.valid_queues and tcb_at' t and valid_objs') s) and (\<lambda>s. \<not> targetDom \<noteq> curDom \<longrightarrow> ((\<lambda>s. sact = ksSchedulerAction s \<and> weak_sch_act_wf (ksSchedulerAction s) s) and (\<lambda>s. sact \<noteq> ResumeCurrentThread \<longrightarrow> (Invariants_H.valid_queues and (\<lambda>s. weak_sch_act_wf (ksSchedulerAction s) s) and valid_objs' and (\<lambda>s. (Invariants_H.valid_queues s \<and> valid_objs' s \<and> weak_sch_act_wf (ksSchedulerAction s) s) \<and> tcb_at' t s \<and> valid_objs' s)) s) and (\<lambda>s. \<not> sact \<noteq> ResumeCurrentThread \<longrightarrow> ?Pf160 target curDom targetDom sact s)) s) and (\<lambda>s. curDom = ksCurDomain s \<and> obj_at' (\<lambda>tcb. targetDom = tcbDomain tcb) t s)\<rbrace>
 4. \<And>target curDom. target = tcb_ptr_to_ctcb_ptr t \<Longrightarrow> \<lbrace>?P132 target curDom\<rbrace> threadGet tcbDomain t \<lbrace>?Q134 target curDom\<rbrace>
 5. \<And>target s s'. \<lbrakk>target = tcb_ptr_to_ctcb_ptr t; (s, s') \<in> rf_sr; (Invariants_H.valid_queues and (\<lambda>s. weak_sch_act_wf (ksSchedulerAction s) s) and st_tcb_at' runnable' t and (\<lambda>s. ksCurDomain s \<le> maxDomain) and valid_objs') s; s' \<in> UNIV\<rbrakk> \<Longrightarrow> ((\<lambda>s. \<forall>rv. ksCurDomain s = rv \<longrightarrow> ?P132 target rv s) and tcb_at' (ctcb_ptr_to_tcb_ptr target)) s \<and> s' \<in> {s. \<forall>rv. ksCurDomain_' (globals s) = UCAST(8 \<rightarrow> 32) rv \<longrightarrow> s \<in> {s'. \<forall>rva. s' \<in> {s'. \<forall>rvb. s' \<in> {s. (s \<in> \<lbrace>rva \<noteq> rv\<rbrace> \<longrightarrow> s \<in> {s. tcb_'_update (\<lambda>_. target) s \<in> UNIV \<inter> \<lbrace>\<acute>tcb = tcb_ptr_to_ctcb_ptr t\<rbrace>}) \<and> (s \<notin> \<lbrace>rva \<noteq> rv\<rbrace> \<longrightarrow> s \<in> {s. s \<in> UNIV} \<inter> ?R'196 target rv rva rvb \<inter> \<lbrace>\<acute>ksSchedulerAction \<noteq> NULL\<rbrace> \<union> ?Rf160 target rv rva rvb \<inter> - \<lbrace>\<acute>ksSchedulerAction \<noteq> NULL\<rbrace>)} \<inter> UNIV}}} \<inter> \<lbrace>True\<rbrace> proof (prove)
goal (4 subgoals):
 1. \<And>target curDom targetDom sact. target = tcb_ptr_to_ctcb_ptr t \<Longrightarrow> ccorres dc xfdc (?Pf160 target curDom targetDom sact) (?Rf160 target curDom targetDom sact) [SKIP] (setSchedulerAction (SwitchToThread t)) (\<acute>ksSchedulerAction :== target)
 2. \<And>target curDom targetDom. target = tcb_ptr_to_ctcb_ptr t \<Longrightarrow> \<lbrace>?Q134 target curDom targetDom\<rbrace> getSchedulerAction \<lbrace>\<lambda>sact. (\<lambda>_. True) and (\<lambda>s. targetDom \<noteq> curDom \<longrightarrow> (Invariants_H.valid_queues and tcb_at' t and valid_objs') s) and (\<lambda>s. \<not> targetDom \<noteq> curDom \<longrightarrow> ((\<lambda>s. sact = ksSchedulerAction s \<and> weak_sch_act_wf (ksSchedulerAction s) s) and (\<lambda>s. sact \<noteq> ResumeCurrentThread \<longrightarrow> (Invariants_H.valid_queues and (\<lambda>s. weak_sch_act_wf (ksSchedulerAction s) s) and valid_objs' and (\<lambda>s. (Invariants_H.valid_queues s \<and> valid_objs' s \<and> weak_sch_act_wf (ksSchedulerAction s) s) \<and> tcb_at' t s \<and> valid_objs' s)) s) and (\<lambda>s. \<not> sact \<noteq> ResumeCurrentThread \<longrightarrow> ?Pf160 target curDom targetDom sact s)) s) and (\<lambda>s. curDom = ksCurDomain s \<and> obj_at' (\<lambda>tcb. targetDom = tcbDomain tcb) t s)\<rbrace>
 3. \<And>target curDom. target = tcb_ptr_to_ctcb_ptr t \<Longrightarrow> \<lbrace>?P132 target curDom\<rbrace> threadGet tcbDomain t \<lbrace>?Q134 target curDom\<rbrace>
 4. \<And>target s s'. \<lbrakk>target = tcb_ptr_to_ctcb_ptr t; (s, s') \<in> rf_sr; (Invariants_H.valid_queues and (\<lambda>s. weak_sch_act_wf (ksSchedulerAction s) s) and st_tcb_at' runnable' t and (\<lambda>s. ksCurDomain s \<le> maxDomain) and valid_objs') s; s' \<in> UNIV\<rbrakk> \<Longrightarrow> ((\<lambda>s. \<forall>rv. ksCurDomain s = rv \<longrightarrow> ?P132 target rv s) and tcb_at' (ctcb_ptr_to_tcb_ptr target)) s \<and> s' \<in> {s. \<forall>rv. ksCurDomain_' (globals s) = UCAST(8 \<rightarrow> 32) rv \<longrightarrow> s \<in> {s'. \<forall>rva. s' \<in> {s'. \<forall>rvb. s' \<in> {s. (s \<in> \<lbrace>rva \<noteq> rv\<rbrace> \<longrightarrow> s \<in> {s. tcb_'_update (\<lambda>_. target) s \<in> UNIV \<inter> \<lbrace>\<acute>tcb = tcb_ptr_to_ctcb_ptr t\<rbrace>}) \<and> (s \<notin> \<lbrace>rva \<noteq> rv\<rbrace> \<longrightarrow> s \<in> {s. s \<in> UNIV} \<inter> {s. \<forall>ta rv. dc rv (xfdc (s\<lparr>globals := globals s\<lparr>ksReadyQueues_' := ksReadyQueues_' (globals ta), ksReadyQueuesL1Bitmap_' := ksReadyQueuesL1Bitmap_' (globals ta), ksReadyQueuesL2Bitmap_' := ksReadyQueuesL2Bitmap_' (globals ta), ksSchedulerAction_' := ksSchedulerAction_' (globals ta), t_hrs_' := t_hrs_' (globals ta)\<rparr>\<rparr>)) \<longrightarrow> target = tcb_ptr_to_ctcb_ptr t} \<inter> \<lbrace>\<acute>ksSchedulerAction \<noteq> NULL\<rbrace> \<union> ?Rf160 target rv rva rvb \<inter> - \<lbrace>\<acute>ksSchedulerAction \<noteq> NULL\<rbrace>)} \<inter> UNIV}}} \<inter> \<lbrace>True\<rbrace> proof (prove)
goal (3 subgoals):
 1. \<And>target curDom targetDom. target = tcb_ptr_to_ctcb_ptr t \<Longrightarrow> \<lbrace>?Q134 target curDom targetDom\<rbrace> getSchedulerAction \<lbrace>\<lambda>sact. (\<lambda>_. True) and (\<lambda>s. targetDom \<noteq> curDom \<longrightarrow> (Invariants_H.valid_queues and tcb_at' t and valid_objs') s) and (\<lambda>s. \<not> targetDom \<noteq> curDom \<longrightarrow> ((\<lambda>s. sact = ksSchedulerAction s \<and> weak_sch_act_wf (ksSchedulerAction s) s) and (\<lambda>s. sact \<noteq> ResumeCurrentThread \<longrightarrow> (Invariants_H.valid_queues and (\<lambda>s. weak_sch_act_wf (ksSchedulerAction s) s) and valid_objs' and (\<lambda>s. (Invariants_H.valid_queues s \<and> valid_objs' s \<and> weak_sch_act_wf (ksSchedulerAction s) s) \<and> tcb_at' t s \<and> valid_objs' s)) s) and (\<lambda>s. \<not> sact \<noteq> ResumeCurrentThread \<longrightarrow> True)) s) and (\<lambda>s. curDom = ksCurDomain s \<and> obj_at' (\<lambda>tcb. targetDom = tcbDomain tcb) t s)\<rbrace>
 2. \<And>target curDom. target = tcb_ptr_to_ctcb_ptr t \<Longrightarrow> \<lbrace>?P132 target curDom\<rbrace> threadGet tcbDomain t \<lbrace>?Q134 target curDom\<rbrace>
 3. \<And>target s s'. \<lbrakk>target = tcb_ptr_to_ctcb_ptr t; (s, s') \<in> rf_sr; (Invariants_H.valid_queues and (\<lambda>s. weak_sch_act_wf (ksSchedulerAction s) s) and st_tcb_at' runnable' t and (\<lambda>s. ksCurDomain s \<le> maxDomain) and valid_objs') s; s' \<in> UNIV\<rbrakk> \<Longrightarrow> ((\<lambda>s. \<forall>rv. ksCurDomain s = rv \<longrightarrow> ?P132 target rv s) and tcb_at' (ctcb_ptr_to_tcb_ptr target)) s \<and> s' \<in> {s. \<forall>rv. ksCurDomain_' (globals s) = UCAST(8 \<rightarrow> 32) rv \<longrightarrow> s \<in> {s'. \<forall>rva. s' \<in> {s'. \<forall>rvb. s' \<in> {s. (s \<in> \<lbrace>rva \<noteq> rv\<rbrace> \<longrightarrow> s \<in> {s. tcb_'_update (\<lambda>_. target) s \<in> UNIV \<inter> \<lbrace>\<acute>tcb = tcb_ptr_to_ctcb_ptr t\<rbrace>}) \<and> (s \<notin> \<lbrace>rva \<noteq> rv\<rbrace> \<longrightarrow> s \<in> {s. s \<in> UNIV} \<inter> {s. \<forall>ta rv. dc rv (xfdc (s\<lparr>globals := globals s\<lparr>ksReadyQueues_' := ksReadyQueues_' (globals ta), ksReadyQueuesL1Bitmap_' := ksReadyQueuesL1Bitmap_' (globals ta), ksReadyQueuesL2Bitmap_' := ksReadyQueuesL2Bitmap_' (globals ta), ksSchedulerAction_' := ksSchedulerAction_' (globals ta), t_hrs_' := t_hrs_' (globals ta)\<rparr>\<rparr>)) \<longrightarrow> target = tcb_ptr_to_ctcb_ptr t} \<inter> \<lbrace>\<acute>ksSchedulerAction \<noteq> NULL\<rbrace> \<union> UNIV \<inter> - \<lbrace>\<acute>ksSchedulerAction \<noteq> NULL\<rbrace>)} \<inter> UNIV}}} \<inter> \<lbrace>True\<rbrace> proof (prove)
goal (3 subgoals):
 1. \<And>curDom targetDom. \<lbrace>?Q134 (tcb_ptr_to_ctcb_ptr t) curDom targetDom\<rbrace> getSchedulerAction \<lbrace>\<lambda>sact. (\<lambda>s. targetDom \<noteq> curDom \<longrightarrow> Invariants_H.valid_queues s \<and> tcb_at' t s \<and> valid_objs' s) and (\<lambda>s. targetDom = curDom \<longrightarrow> sact = ksSchedulerAction s \<and> weak_sch_act_wf (ksSchedulerAction s) s \<and> (sact \<noteq> ResumeCurrentThread \<longrightarrow> Invariants_H.valid_queues s \<and> weak_sch_act_wf (ksSchedulerAction s) s \<and> valid_objs' s \<and> Invariants_H.valid_queues s \<and> valid_objs' s \<and> weak_sch_act_wf (ksSchedulerAction s) s \<and> tcb_at' t s \<and> valid_objs' s)) and (\<lambda>s. curDom = ksCurDomain s \<and> obj_at' (\<lambda>tcb. targetDom = tcbDomain tcb) t s)\<rbrace>
 2. \<And>target curDom. target = tcb_ptr_to_ctcb_ptr t \<Longrightarrow> \<lbrace>?P132 target curDom\<rbrace> threadGet tcbDomain t \<lbrace>?Q134 target curDom\<rbrace>
 3. \<And>target s s'. \<lbrakk>target = tcb_ptr_to_ctcb_ptr t; (s, s') \<in> rf_sr; (Invariants_H.valid_queues and (\<lambda>s. weak_sch_act_wf (ksSchedulerAction s) s) and st_tcb_at' runnable' t and (\<lambda>s. ksCurDomain s \<le> maxDomain) and valid_objs') s; s' \<in> UNIV\<rbrakk> \<Longrightarrow> ((\<lambda>s. \<forall>rv. ksCurDomain s = rv \<longrightarrow> ?P132 target rv s) and tcb_at' (ctcb_ptr_to_tcb_ptr target)) s \<and> s' \<in> {s. \<forall>rv. ksCurDomain_' (globals s) = UCAST(8 \<rightarrow> 32) rv \<longrightarrow> s \<in> {s'. \<forall>rva. s' \<in> {s'. \<forall>rvb. s' \<in> {s. (s \<in> \<lbrace>rva \<noteq> rv\<rbrace> \<longrightarrow> s \<in> {s. tcb_'_update (\<lambda>_. target) s \<in> UNIV \<inter> \<lbrace>\<acute>tcb = tcb_ptr_to_ctcb_ptr t\<rbrace>}) \<and> (s \<notin> \<lbrace>rva \<noteq> rv\<rbrace> \<longrightarrow> s \<in> {s. s \<in> UNIV} \<inter> {s. \<forall>ta rv. dc rv (xfdc (s\<lparr>globals := globals s\<lparr>ksReadyQueues_' := ksReadyQueues_' (globals ta), ksReadyQueuesL1Bitmap_' := ksReadyQueuesL1Bitmap_' (globals ta), ksReadyQueuesL2Bitmap_' := ksReadyQueuesL2Bitmap_' (globals ta), ksSchedulerAction_' := ksSchedulerAction_' (globals ta), t_hrs_' := t_hrs_' (globals ta)\<rparr>\<rparr>)) \<longrightarrow> target = tcb_ptr_to_ctcb_ptr t} \<inter> \<lbrace>\<acute>ksSchedulerAction \<noteq> NULL\<rbrace> \<union> UNIV \<inter> - \<lbrace>\<acute>ksSchedulerAction \<noteq> NULL\<rbrace>)} \<inter> UNIV}}} \<inter> \<lbrace>True\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<And>target curDom. target = tcb_ptr_to_ctcb_ptr t \<Longrightarrow> \<lbrace>?P132 target curDom\<rbrace> threadGet tcbDomain t \<lbrace>\<lambda>a b. ((\<lambda>s. a \<noteq> curDom \<longrightarrow> Invariants_H.valid_queues s \<and> tcb_at' t s \<and> valid_objs' s) and (\<lambda>s. a = curDom \<longrightarrow> ksSchedulerAction b = ksSchedulerAction s \<and> weak_sch_act_wf (ksSchedulerAction s) s \<and> (ksSchedulerAction b \<noteq> ResumeCurrentThread \<longrightarrow> Invariants_H.valid_queues s \<and> weak_sch_act_wf (ksSchedulerAction s) s \<and> valid_objs' s \<and> Invariants_H.valid_queues s \<and> valid_objs' s \<and> weak_sch_act_wf (ksSchedulerAction s) s \<and> tcb_at' t s \<and> valid_objs' s)) and (\<lambda>s. curDom = ksCurDomain s \<and> obj_at' (\<lambda>tcb. a = tcbDomain tcb) t s)) b\<rbrace>
 2. \<And>target s s'. \<lbrakk>target = tcb_ptr_to_ctcb_ptr t; (s, s') \<in> rf_sr; (Invariants_H.valid_queues and (\<lambda>s. weak_sch_act_wf (ksSchedulerAction s) s) and st_tcb_at' runnable' t and (\<lambda>s. ksCurDomain s \<le> maxDomain) and valid_objs') s; s' \<in> UNIV\<rbrakk> \<Longrightarrow> ((\<lambda>s. \<forall>rv. ksCurDomain s = rv \<longrightarrow> ?P132 target rv s) and tcb_at' (ctcb_ptr_to_tcb_ptr target)) s \<and> s' \<in> {s. \<forall>rv. ksCurDomain_' (globals s) = UCAST(8 \<rightarrow> 32) rv \<longrightarrow> s \<in> {s'. \<forall>rva. s' \<in> {s'. \<forall>rvb. s' \<in> {s. (s \<in> \<lbrace>rva \<noteq> rv\<rbrace> \<longrightarrow> s \<in> {s. tcb_'_update (\<lambda>_. target) s \<in> UNIV \<inter> \<lbrace>\<acute>tcb = tcb_ptr_to_ctcb_ptr t\<rbrace>}) \<and> (s \<notin> \<lbrace>rva \<noteq> rv\<rbrace> \<longrightarrow> s \<in> {s. s \<in> UNIV} \<inter> {s. \<forall>ta rv. dc rv (xfdc (s\<lparr>globals := globals s\<lparr>ksReadyQueues_' := ksReadyQueues_' (globals ta), ksReadyQueuesL1Bitmap_' := ksReadyQueuesL1Bitmap_' (globals ta), ksReadyQueuesL2Bitmap_' := ksReadyQueuesL2Bitmap_' (globals ta), ksSchedulerAction_' := ksSchedulerAction_' (globals ta), t_hrs_' := t_hrs_' (globals ta)\<rparr>\<rparr>)) \<longrightarrow> target = tcb_ptr_to_ctcb_ptr t} \<inter> \<lbrace>\<acute>ksSchedulerAction \<noteq> NULL\<rbrace> \<union> UNIV \<inter> - \<lbrace>\<acute>ksSchedulerAction \<noteq> NULL\<rbrace>)} \<inter> UNIV}}} \<inter> \<lbrace>True\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<And>curDom. \<lbrace>?P132 (tcb_ptr_to_ctcb_ptr t) curDom\<rbrace> threadGet tcbDomain t \<lbrace>\<lambda>a b. (a \<noteq> curDom \<longrightarrow> Invariants_H.valid_queues b \<and> tcb_at' t b \<and> valid_objs' b) \<and> (a = curDom \<longrightarrow> weak_sch_act_wf (ksSchedulerAction b) b \<and> (ksSchedulerAction b \<noteq> ResumeCurrentThread \<longrightarrow> Invariants_H.valid_queues b \<and> weak_sch_act_wf (ksSchedulerAction b) b \<and> valid_objs' b \<and> Invariants_H.valid_queues b \<and> valid_objs' b \<and> weak_sch_act_wf (ksSchedulerAction b) b \<and> tcb_at' t b \<and> valid_objs' b)) \<and> curDom = ksCurDomain b \<and> obj_at' (\<lambda>tcb. a = tcbDomain tcb) t b\<rbrace>
 2. \<And>target s s'. \<lbrakk>target = tcb_ptr_to_ctcb_ptr t; (s, s') \<in> rf_sr; (Invariants_H.valid_queues and (\<lambda>s. weak_sch_act_wf (ksSchedulerAction s) s) and st_tcb_at' runnable' t and (\<lambda>s. ksCurDomain s \<le> maxDomain) and valid_objs') s; s' \<in> UNIV\<rbrakk> \<Longrightarrow> ((\<lambda>s. \<forall>rv. ksCurDomain s = rv \<longrightarrow> ?P132 target rv s) and tcb_at' (ctcb_ptr_to_tcb_ptr target)) s \<and> s' \<in> {s. \<forall>rv. ksCurDomain_' (globals s) = UCAST(8 \<rightarrow> 32) rv \<longrightarrow> s \<in> {s'. \<forall>rva. s' \<in> {s'. \<forall>rvb. s' \<in> {s. (s \<in> \<lbrace>rva \<noteq> rv\<rbrace> \<longrightarrow> s \<in> {s. tcb_'_update (\<lambda>_. target) s \<in> UNIV \<inter> \<lbrace>\<acute>tcb = tcb_ptr_to_ctcb_ptr t\<rbrace>}) \<and> (s \<notin> \<lbrace>rva \<noteq> rv\<rbrace> \<longrightarrow> s \<in> {s. s \<in> UNIV} \<inter> {s. \<forall>ta rv. dc rv (xfdc (s\<lparr>globals := globals s\<lparr>ksReadyQueues_' := ksReadyQueues_' (globals ta), ksReadyQueuesL1Bitmap_' := ksReadyQueuesL1Bitmap_' (globals ta), ksReadyQueuesL2Bitmap_' := ksReadyQueuesL2Bitmap_' (globals ta), ksSchedulerAction_' := ksSchedulerAction_' (globals ta), t_hrs_' := t_hrs_' (globals ta)\<rparr>\<rparr>)) \<longrightarrow> target = tcb_ptr_to_ctcb_ptr t} \<inter> \<lbrace>\<acute>ksSchedulerAction \<noteq> NULL\<rbrace> \<union> UNIV \<inter> - \<lbrace>\<acute>ksSchedulerAction \<noteq> NULL\<rbrace>)} \<inter> UNIV}}} \<inter> \<lbrace>True\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>target s s'. \<lbrakk>target = tcb_ptr_to_ctcb_ptr t; (s, s') \<in> rf_sr; (Invariants_H.valid_queues and (\<lambda>s. weak_sch_act_wf (ksSchedulerAction s) s) and st_tcb_at' runnable' t and (\<lambda>s. ksCurDomain s \<le> maxDomain) and valid_objs') s; s' \<in> UNIV\<rbrakk> \<Longrightarrow> ((\<lambda>s. \<forall>rv. ksCurDomain s = rv \<longrightarrow> (Invariants_H.valid_queues s \<and> tcb_at' t s \<and> valid_objs' s) \<and> (weak_sch_act_wf (ksSchedulerAction s) s \<and> (ksSchedulerAction s \<noteq> ResumeCurrentThread \<longrightarrow> Invariants_H.valid_queues s \<and> weak_sch_act_wf (ksSchedulerAction s) s \<and> valid_objs' s \<and> Invariants_H.valid_queues s \<and> valid_objs' s \<and> weak_sch_act_wf (ksSchedulerAction s) s \<and> tcb_at' t s \<and> valid_objs' s)) \<and> rv = ksCurDomain s \<and> tcb_at' t s) and tcb_at' (ctcb_ptr_to_tcb_ptr target)) s \<and> s' \<in> {s. \<forall>rv. ksCurDomain_' (globals s) = UCAST(8 \<rightarrow> 32) rv \<longrightarrow> s \<in> {s'. \<forall>rva. s' \<in> {s'. \<forall>rvb. s' \<in> {s. (s \<in> \<lbrace>rva \<noteq> rv\<rbrace> \<longrightarrow> s \<in> {s. tcb_'_update (\<lambda>_. target) s \<in> UNIV \<inter> \<lbrace>\<acute>tcb = tcb_ptr_to_ctcb_ptr t\<rbrace>}) \<and> (s \<notin> \<lbrace>rva \<noteq> rv\<rbrace> \<longrightarrow> s \<in> {s. s \<in> UNIV} \<inter> {s. \<forall>ta rv. dc rv (xfdc (s\<lparr>globals := globals s\<lparr>ksReadyQueues_' := ksReadyQueues_' (globals ta), ksReadyQueuesL1Bitmap_' := ksReadyQueuesL1Bitmap_' (globals ta), ksReadyQueuesL2Bitmap_' := ksReadyQueuesL2Bitmap_' (globals ta), ksSchedulerAction_' := ksSchedulerAction_' (globals ta), t_hrs_' := t_hrs_' (globals ta)\<rparr>\<rparr>)) \<longrightarrow> target = tcb_ptr_to_ctcb_ptr t} \<inter> \<lbrace>\<acute>ksSchedulerAction \<noteq> NULL\<rbrace> \<union> UNIV \<inter> - \<lbrace>\<acute>ksSchedulerAction \<noteq> NULL\<rbrace>)} \<inter> UNIV}}} \<inter> \<lbrace>True\<rbrace> proof (prove)
goal:
No subgoals!