theory Interrupt_R

lemma timerTick_corres:
  "corres dc (cur_tcb and valid_sched)
             invs'
             timer_tick timerTick" supply if_weak_cong[cong] apply (simp add: timerTick_def timer_tick_def) apply (simp add:thread_state_case_if threadState_case_if) apply (rule_tac Q="\<top> and (cur_tcb and valid_sched)" and Q'="\<top> and invs'" in corres_guard_imp) apply (rule corres_guard_imp) apply (rule corres_split[OF getCurThread_corres]) apply simp apply (rule corres_split[OF getThreadState_corres]) apply (rename_tac state state') apply (rule corres_split[where r' = dc ]) apply (rule corres_if[where Q = \<top> and Q' = \<top>]) apply (case_tac state,simp_all)[1] apply (simp add: Let_def) apply (rule_tac r'="(=)" in corres_split[OF ethreadget_corres]) apply (simp add:etcb_relation_def) apply (rename_tac ts ts') apply (rule_tac R="1 < ts" in corres_cases) apply (simp) apply (unfold thread_set_time_slice_def) apply (rule ethread_set_corres, simp+) apply (clarsimp simp: etcb_relation_def) apply simp apply (rule corres_split) apply (rule ethread_set_corres; simp) apply (simp add: etcb_relation_def) apply (rule corres_split[OF tcbSchedAppend_corres]) apply (rule rescheduleRequired_corres) apply (wp)[1] apply (rule hoare_strengthen_post) apply (rule tcbSchedAppend_invs_but_ct_not_inQ',
                          clarsimp simp: sch_act_wf_weak) apply (wp threadSet_timeslice_invs threadSet_valid_queues
                           threadSet_valid_queues' threadSet_pred_tcb_at_state)+ apply simp apply simp apply (rule corres_when,simp) apply (rule corres_split[OF decDomainTime_corres]) apply (rule corres_split[OF getDomainTime_corres]) apply (rule corres_when,simp) apply (rule rescheduleRequired_corres) apply (wp hoare_drop_imp)+ apply (simp add:dec_domain_time_def) apply wp+ apply (simp add:decDomainTime_def) apply wp apply (wp|wpc|unfold Let_def|simp)+ apply (wp hoare_weak_lift_imp threadSet_timeslice_invs threadSet_valid_queues  threadSet_valid_queues'
                 threadSet_pred_tcb_at_state threadSet_weak_sch_act_wf tcbSchedAppend_valid_objs'
                 rescheduleRequired_weak_sch_act_wf tcbSchedAppend_valid_queues| simp)+ apply (strengthen sch_act_wf_weak) apply (clarsimp simp:conj_comms) apply (wp tcbSchedAppend_valid_queues tcbSchedAppend_sch_act_wf) apply simp apply (wp threadSet_valid_queues threadSet_pred_tcb_at_state threadSet_sch_act
              threadSet_tcbDomain_triv threadSet_valid_queues' threadSet_valid_objs'| simp)+ apply (wp threadGet_wp gts_wp gts_wp')+ apply (clarsimp simp: cur_tcb_def tcb_at_is_etcb_at valid_sched_def valid_sched_action_def) prefer 2 apply clarsimp apply (clarsimp simp add:cur_tcb_def valid_sched_def
       valid_sched_action_def valid_etcbs_def is_tcb_def
       is_etcb_at_def st_tcb_at_def obj_at_def
       dest!:get_tcb_SomeD) apply (clarsimp simp: invs'_def valid_state'_def
   sch_act_wf_weak
   cur_tcb'_def inQ_def
   ct_in_state'_def obj_at'_def) apply (clarsimp simp:st_tcb_at'_def
      valid_idle'_def ct_idle_or_in_cur_domain'_def
      obj_at'_def projectKO_eq) apply simp done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. corres dc (cur_tcb and valid_sched) invs' timer_tick timerTick proof (prove)
goal (1 subgoal):
 1. corres dc (cur_tcb and valid_sched) invs' timer_tick timerTick proof (prove)
goal (1 subgoal):
 1. corres dc (cur_tcb and valid_sched) invs' (do cur <- gets cur_thread;
state <- get_thread_state cur;
y <- case state of Structures_A.thread_state.Running \<Rightarrow> do ts <- ethread_get tcb_time_slice cur;
let ts' = ts - 1 in if 0 < ts' then thread_set_time_slice cur ts' else do thread_set_time_slice cur timeSlice;
tcb_sched_action tcb_sched_append cur;
reschedule_required
od
od | _ \<Rightarrow> return ();
when (Suc 0 < numDomains) (do y <- dec_domain_time;
dom_time <- gets domain_time;
when (dom_time = 0) reschedule_required
od)
od) (do thread <- getCurThread;
state <- getThreadState thread;
y <- case state of Structures_H.thread_state.Running \<Rightarrow> do ts <- threadGet tcbTimeSlice thread;
ts' <- return (ts - 1);
if 0 < ts' then threadSet (tcbTimeSlice_update (\<lambda>_. ts')) thread else do threadSet (tcbTimeSlice_update (\<lambda>_. timeSlice)) thread;
tcbSchedAppend thread;
rescheduleRequired
od
od | _ \<Rightarrow> return ();
when (Suc 0 < numDomains) (do y <- decDomainTime;
domainTime <- getDomainTime;
when (domainTime = 0) rescheduleRequired
od)
od) proof (prove)
goal (1 subgoal):
 1. corres dc (cur_tcb and valid_sched) invs' (do cur <- gets cur_thread;
state <- get_thread_state cur;
y <- if state = Structures_A.thread_state.Running then do ts <- ethread_get tcb_time_slice cur;
let ts' = ts - 1 in if 0 < ts' then thread_set_time_slice cur ts' else do thread_set_time_slice cur timeSlice;
tcb_sched_action tcb_sched_append cur;
reschedule_required
od
od else return ();
when (Suc 0 < numDomains) (do y <- dec_domain_time;
dom_time <- gets domain_time;
when (dom_time = 0) reschedule_required
od)
od) (do thread <- getCurThread;
state <- getThreadState thread;
y <- if state = Structures_H.thread_state.Running then do ts <- threadGet tcbTimeSlice thread;
ts' <- return (ts - 1);
if 0 < ts' then threadSet (tcbTimeSlice_update (\<lambda>_. ts')) thread else do threadSet (tcbTimeSlice_update (\<lambda>_. timeSlice)) thread;
tcbSchedAppend thread;
rescheduleRequired
od
od else return ();
when (Suc 0 < numDomains) (do y <- decDomainTime;
domainTime <- getDomainTime;
when (domainTime = 0) rescheduleRequired
od)
od) proof (prove)
goal (3 subgoals):
 1. corres dc ((\<lambda>_. True) and (cur_tcb and valid_sched)) ((\<lambda>_. True) and invs') (do cur <- gets cur_thread;
state <- get_thread_state cur;
y <- if state = Structures_A.thread_state.Running then do ts <- ethread_get tcb_time_slice cur;
let ts' = ts - 1 in if 0 < ts' then thread_set_time_slice cur ts' else do thread_set_time_slice cur timeSlice;
tcb_sched_action tcb_sched_append cur;
reschedule_required
od
od else return ();
when (Suc 0 < numDomains) (do y <- dec_domain_time;
dom_time <- gets domain_time;
when (dom_time = 0) reschedule_required
od)
od) (do thread <- getCurThread;
state <- getThreadState thread;
y <- if state = Structures_H.thread_state.Running then do ts <- threadGet tcbTimeSlice thread;
ts' <- return (ts - 1);
if 0 < ts' then threadSet (tcbTimeSlice_update (\<lambda>_. ts')) thread else do threadSet (tcbTimeSlice_update (\<lambda>_. timeSlice)) thread;
tcbSchedAppend thread;
rescheduleRequired
od
od else return ();
when (Suc 0 < numDomains) (do y <- decDomainTime;
domainTime <- getDomainTime;
when (domainTime = 0) rescheduleRequired
od)
od)
 2. \<And>s. (cur_tcb and valid_sched) s \<Longrightarrow> ((\<lambda>_. True) and (cur_tcb and valid_sched)) s
 3. \<And>s. invs' s \<Longrightarrow> ((\<lambda>_. True) and invs') s proof (prove)
goal (5 subgoals):
 1. corres dc ?Q2 ?Q'2 (do cur <- gets cur_thread;
state <- get_thread_state cur;
y <- if state = Structures_A.thread_state.Running then do ts <- ethread_get tcb_time_slice cur;
let ts' = ts - 1 in if 0 < ts' then thread_set_time_slice cur ts' else do thread_set_time_slice cur timeSlice;
tcb_sched_action tcb_sched_append cur;
reschedule_required
od
od else return ();
when (Suc 0 < numDomains) (do y <- dec_domain_time;
dom_time <- gets domain_time;
when (dom_time = 0) reschedule_required
od)
od) (do thread <- getCurThread;
state <- getThreadState thread;
y <- if state = Structures_H.thread_state.Running then do ts <- threadGet tcbTimeSlice thread;
ts' <- return (ts - 1);
if 0 < ts' then threadSet (tcbTimeSlice_update (\<lambda>_. ts')) thread else do threadSet (tcbTimeSlice_update (\<lambda>_. timeSlice)) thread;
tcbSchedAppend thread;
rescheduleRequired
od
od else return ();
when (Suc 0 < numDomains) (do y <- decDomainTime;
domainTime <- getDomainTime;
when (domainTime = 0) rescheduleRequired
od)
od)
 2. \<And>s. ((\<lambda>_. True) and (cur_tcb and valid_sched)) s \<Longrightarrow> ?Q2 s
 3. \<And>s. ((\<lambda>_. True) and invs') s \<Longrightarrow> ?Q'2 s
 4. \<And>s. (cur_tcb and valid_sched) s \<Longrightarrow> ((\<lambda>_. True) and (cur_tcb and valid_sched)) s
 5. \<And>s. invs' s \<Longrightarrow> ((\<lambda>_. True) and invs') s proof (prove)
goal (7 subgoals):
 1. \<And>cur thread. cur = thread \<Longrightarrow> corres dc (?R6 cur) (?R'6 thread) (do state <- get_thread_state cur;
y <- if state = Structures_A.thread_state.Running then do ts <- ethread_get tcb_time_slice cur;
let ts' = ts - 1 in if 0 < ts' then thread_set_time_slice cur ts' else do thread_set_time_slice cur timeSlice;
tcb_sched_action tcb_sched_append cur;
reschedule_required
od
od else return ();
when (Suc 0 < numDomains) (do y <- dec_domain_time;
dom_time <- gets domain_time;
when (dom_time = 0) reschedule_required
od)
od) (do state <- getThreadState thread;
y <- if state = Structures_H.thread_state.Running then do ts <- threadGet tcbTimeSlice thread;
ts' <- return (ts - 1);
if 0 < ts' then threadSet (tcbTimeSlice_update (\<lambda>_. ts')) thread else do threadSet (tcbTimeSlice_update (\<lambda>_. timeSlice)) thread;
tcbSchedAppend thread;
rescheduleRequired
od
od else return ();
when (Suc 0 < numDomains) (do y <- decDomainTime;
domainTime <- getDomainTime;
when (domainTime = 0) rescheduleRequired
od)
od)
 2. \<lbrace>?Q6\<rbrace> gets cur_thread \<lbrace>?R6\<rbrace>
 3. \<lbrace>?Q'6\<rbrace> getCurThread \<lbrace>?R'6\<rbrace>
 4. \<And>s. ((\<lambda>_. True) and (cur_tcb and valid_sched)) s \<Longrightarrow> ((\<lambda>_. True) and ?Q6) s
 5. \<And>s. ((\<lambda>_. True) and invs') s \<Longrightarrow> ((\<lambda>_. True) and ?Q'6) s
 6. \<And>s. (cur_tcb and valid_sched) s \<Longrightarrow> ((\<lambda>_. True) and (cur_tcb and valid_sched)) s
 7. \<And>s. invs' s \<Longrightarrow> ((\<lambda>_. True) and invs') s proof (prove)
goal (7 subgoals):
 1. \<And>cur. corres dc (?R6 cur) (?R'6 cur) (do state <- get_thread_state cur;
y <- if state = Structures_A.thread_state.Running then do ts <- ethread_get tcb_time_slice cur;
let ts' = ts - 1 in if 0 < ts' then thread_set_time_slice cur ts' else do thread_set_time_slice cur timeSlice;
tcb_sched_action tcb_sched_append cur;
reschedule_required
od
od else return ();
when (Suc 0 < numDomains) (do y <- dec_domain_time;
dom_time <- gets domain_time;
when (dom_time = 0) reschedule_required
od)
od) (do state <- getThreadState cur;
y <- if state = Structures_H.thread_state.Running then do ts <- threadGet tcbTimeSlice cur;
ts' <- return (ts - 1);
if 0 < ts' then threadSet (tcbTimeSlice_update (\<lambda>_. ts')) cur else do threadSet (tcbTimeSlice_update (\<lambda>_. timeSlice)) cur;
tcbSchedAppend cur;
rescheduleRequired
od
od else return ();
when (Suc 0 < numDomains) (do y <- decDomainTime;
domainTime <- getDomainTime;
when (domainTime = 0) rescheduleRequired
od)
od)
 2. \<lbrace>?Q6\<rbrace> gets cur_thread \<lbrace>?R6\<rbrace>
 3. \<lbrace>?Q'6\<rbrace> getCurThread \<lbrace>?R'6\<rbrace>
 4. \<And>s. ((\<lambda>_. True) and (cur_tcb and valid_sched)) s \<Longrightarrow> ((\<lambda>_. True) and ?Q6) s
 5. \<And>s. ((\<lambda>_. True) and invs') s \<Longrightarrow> ((\<lambda>_. True) and ?Q'6) s
 6. \<And>s. (cur_tcb and valid_sched) s \<Longrightarrow> ((\<lambda>_. True) and (cur_tcb and valid_sched)) s
 7. \<And>s. invs' s \<Longrightarrow> ((\<lambda>_. True) and invs') s proof (prove)
goal (9 subgoals):
 1. \<And>cur state statea. thread_state_relation state statea \<Longrightarrow> corres dc (?R10 cur state) (?R'10 cur statea) (do y <- if state = Structures_A.thread_state.Running then do ts <- ethread_get tcb_time_slice cur;
let ts' = ts - 1 in if 0 < ts' then thread_set_time_slice cur ts' else do thread_set_time_slice cur timeSlice;
tcb_sched_action tcb_sched_append cur;
reschedule_required
od
od else return ();
when (Suc 0 < numDomains) (do y <- dec_domain_time;
dom_time <- gets domain_time;
when (dom_time = 0) reschedule_required
od)
od) (do y <- if statea = Structures_H.thread_state.Running then do ts <- threadGet tcbTimeSlice cur;
ts' <- return (ts - 1);
if 0 < ts' then threadSet (tcbTimeSlice_update (\<lambda>_. ts')) cur else do threadSet (tcbTimeSlice_update (\<lambda>_. timeSlice)) cur;
tcbSchedAppend cur;
rescheduleRequired
od
od else return ();
when (Suc 0 < numDomains) (do y <- decDomainTime;
domainTime <- getDomainTime;
when (domainTime = 0) rescheduleRequired
od)
od)
 2. \<And>cur. \<lbrace>?Q10 cur\<rbrace> get_thread_state cur \<lbrace>?R10 cur\<rbrace>
 3. \<And>cur. \<lbrace>?Q'10 cur\<rbrace> getThreadState cur \<lbrace>?R'10 cur\<rbrace>
 4. \<lbrace>?Q6\<rbrace> gets cur_thread \<lbrace>\<lambda>cur. tcb_at cur and ?Q10 cur\<rbrace>
 5. \<lbrace>?Q'6\<rbrace> getCurThread \<lbrace>\<lambda>cur. tcb_at' cur and ?Q'10 cur\<rbrace>
 6. \<And>s. ((\<lambda>_. True) and (cur_tcb and valid_sched)) s \<Longrightarrow> ((\<lambda>_. True) and ?Q6) s
 7. \<And>s. ((\<lambda>_. True) and invs') s \<Longrightarrow> ((\<lambda>_. True) and ?Q'6) s
 8. \<And>s. (cur_tcb and valid_sched) s \<Longrightarrow> ((\<lambda>_. True) and (cur_tcb and valid_sched)) s
 9. \<And>s. invs' s \<Longrightarrow> ((\<lambda>_. True) and invs') s proof (prove)
goal (9 subgoals):
 1. \<And>cur state state'. thread_state_relation state state' \<Longrightarrow> corres dc (?R10 cur state) (?R'10 cur state') (do y <- if state = Structures_A.thread_state.Running then do ts <- ethread_get tcb_time_slice cur;
let ts' = ts - 1 in if 0 < ts' then thread_set_time_slice cur ts' else do thread_set_time_slice cur timeSlice;
tcb_sched_action tcb_sched_append cur;
reschedule_required
od
od else return ();
when (Suc 0 < numDomains) (do y <- dec_domain_time;
dom_time <- gets domain_time;
when (dom_time = 0) reschedule_required
od)
od) (do y <- if state' = Structures_H.thread_state.Running then do ts <- threadGet tcbTimeSlice cur;
ts' <- return (ts - 1);
if 0 < ts' then threadSet (tcbTimeSlice_update (\<lambda>_. ts')) cur else do threadSet (tcbTimeSlice_update (\<lambda>_. timeSlice)) cur;
tcbSchedAppend cur;
rescheduleRequired
od
od else return ();
when (Suc 0 < numDomains) (do y <- decDomainTime;
domainTime <- getDomainTime;
when (domainTime = 0) rescheduleRequired
od)
od)
 2. \<And>cur. \<lbrace>?Q10 cur\<rbrace> get_thread_state cur \<lbrace>?R10 cur\<rbrace>
 3. \<And>cur. \<lbrace>?Q'10 cur\<rbrace> getThreadState cur \<lbrace>?R'10 cur\<rbrace>
 4. \<lbrace>?Q6\<rbrace> gets cur_thread \<lbrace>\<lambda>cur. tcb_at cur and ?Q10 cur\<rbrace>
 5. \<lbrace>?Q'6\<rbrace> getCurThread \<lbrace>\<lambda>cur. tcb_at' cur and ?Q'10 cur\<rbrace>
 6. \<And>s. ((\<lambda>_. True) and (cur_tcb and valid_sched)) s \<Longrightarrow> ((\<lambda>_. True) and ?Q6) s
 7. \<And>s. ((\<lambda>_. True) and invs') s \<Longrightarrow> ((\<lambda>_. True) and ?Q'6) s
 8. \<And>s. (cur_tcb and valid_sched) s \<Longrightarrow> ((\<lambda>_. True) and (cur_tcb and valid_sched)) s
 9. \<And>s. invs' s \<Longrightarrow> ((\<lambda>_. True) and invs') s proof (prove)
goal (12 subgoals):
 1. \<And>cur state state'. thread_state_relation state state' \<Longrightarrow> corres dc (?P16 cur state) (?P'18 cur state') (if state = Structures_A.thread_state.Running then do ts <- ethread_get tcb_time_slice cur;
let ts' = ts - 1 in if 0 < ts' then thread_set_time_slice cur ts' else do thread_set_time_slice cur timeSlice;
tcb_sched_action tcb_sched_append cur;
reschedule_required
od
od else return ()) (if state' = Structures_H.thread_state.Running then do ts <- threadGet tcbTimeSlice cur;
ts' <- return (ts - 1);
if 0 < ts' then threadSet (tcbTimeSlice_update (\<lambda>_. ts')) cur else do threadSet (tcbTimeSlice_update (\<lambda>_. timeSlice)) cur;
tcbSchedAppend cur;
rescheduleRequired
od
od else return ())
 2. \<And>cur state state' y ya. \<lbrakk>thread_state_relation state state'; dc y ya\<rbrakk> \<Longrightarrow> corres dc (?R15 cur state state' y) (?R'15 cur state state' ya) (when (Suc 0 < numDomains) (do y <- dec_domain_time;
dom_time <- gets domain_time;
when (dom_time = 0) reschedule_required
od)) (when (Suc 0 < numDomains) (do y <- decDomainTime;
domainTime <- getDomainTime;
when (domainTime = 0) rescheduleRequired
od))
 3. \<And>cur state state'. thread_state_relation state state' \<Longrightarrow> \<lbrace>?Q17 cur state\<rbrace> if state = Structures_A.thread_state.Running then do ts <- ethread_get tcb_time_slice cur;
let ts' = ts - 1 in if 0 < ts' then thread_set_time_slice cur ts' else do thread_set_time_slice cur timeSlice;
tcb_sched_action tcb_sched_append cur;
reschedule_required
od
od else return () \<lbrace>?R15 cur state state'\<rbrace>
 4. \<And>cur state state'. thread_state_relation state state' \<Longrightarrow> \<lbrace>?Q'19 cur state'\<rbrace> if state' = Structures_H.thread_state.Running then do ts <- threadGet tcbTimeSlice cur;
ts' <- return (ts - 1);
if 0 < ts' then threadSet (tcbTimeSlice_update (\<lambda>_. ts')) cur else do threadSet (tcbTimeSlice_update (\<lambda>_. timeSlice)) cur;
tcbSchedAppend cur;
rescheduleRequired
od
od else return () \<lbrace>?R'15 cur state state'\<rbrace>
 5. \<And>cur. \<lbrace>?Q10 cur\<rbrace> get_thread_state cur \<lbrace>\<lambda>state. ?P16 cur state and ?Q17 cur state\<rbrace>
 6. \<And>cur. \<lbrace>?Q'10 cur\<rbrace> getThreadState cur \<lbrace>\<lambda>state'. ?P'18 cur state' and ?Q'19 cur state'\<rbrace>
 7. \<lbrace>?Q6\<rbrace> gets cur_thread \<lbrace>\<lambda>cur. tcb_at cur and ?Q10 cur\<rbrace>
 8. \<lbrace>?Q'6\<rbrace> getCurThread \<lbrace>\<lambda>cur. tcb_at' cur and ?Q'10 cur\<rbrace>
 9. \<And>s. ((\<lambda>_. True) and (cur_tcb and valid_sched)) s \<Longrightarrow> ((\<lambda>_. True) and ?Q6) s
 10. \<And>s. ((\<lambda>_. True) and invs') s \<Longrightarrow> ((\<lambda>_. True) and ?Q'6) s
A total of 12 subgoals... proof (prove)
goal (14 subgoals):
 1. \<And>cur state state'. thread_state_relation state state' \<Longrightarrow> (state = Structures_A.thread_state.Running) = (state' = Structures_H.thread_state.Running)
 2. \<And>cur state state'. thread_state_relation state state' \<Longrightarrow> corres dc (?P26 cur state) (?P'28 cur state') (do ts <- ethread_get tcb_time_slice cur;
let ts' = ts - 1 in if 0 < ts' then thread_set_time_slice cur ts' else do thread_set_time_slice cur timeSlice;
tcb_sched_action tcb_sched_append cur;
reschedule_required
od
od) (do ts <- threadGet tcbTimeSlice cur;
ts' <- return (ts - 1);
if 0 < ts' then threadSet (tcbTimeSlice_update (\<lambda>_. ts')) cur else do threadSet (tcbTimeSlice_update (\<lambda>_. timeSlice)) cur;
tcbSchedAppend cur;
rescheduleRequired
od
od)
 3. \<And>cur state state'. thread_state_relation state state' \<Longrightarrow> corres dc (\<lambda>_. True) (\<lambda>_. True) (return ()) (return ())
 4. \<And>cur state state' y ya. \<lbrakk>thread_state_relation state state'; dc y ya\<rbrakk> \<Longrightarrow> corres dc (?R15 cur state state' y) (?R'15 cur state state' ya) (when (Suc 0 < numDomains) (do y <- dec_domain_time;
dom_time <- gets domain_time;
when (dom_time = 0) reschedule_required
od)) (when (Suc 0 < numDomains) (do y <- decDomainTime;
domainTime <- getDomainTime;
when (domainTime = 0) rescheduleRequired
od))
 5. \<And>cur state state'. thread_state_relation state state' \<Longrightarrow> \<lbrace>?Q17 cur state\<rbrace> if state = Structures_A.thread_state.Running then do ts <- ethread_get tcb_time_slice cur;
let ts' = ts - 1 in if 0 < ts' then thread_set_time_slice cur ts' else do thread_set_time_slice cur timeSlice;
tcb_sched_action tcb_sched_append cur;
reschedule_required
od
od else return () \<lbrace>?R15 cur state state'\<rbrace>
 6. \<And>cur state state'. thread_state_relation state state' \<Longrightarrow> \<lbrace>?Q'19 cur state'\<rbrace> if state' = Structures_H.thread_state.Running then do ts <- threadGet tcbTimeSlice cur;
ts' <- return (ts - 1);
if 0 < ts' then threadSet (tcbTimeSlice_update (\<lambda>_. ts')) cur else do threadSet (tcbTimeSlice_update (\<lambda>_. timeSlice)) cur;
tcbSchedAppend cur;
rescheduleRequired
od
od else return () \<lbrace>?R'15 cur state state'\<rbrace>
 7. \<And>cur. \<lbrace>?Q10 cur\<rbrace> get_thread_state cur \<lbrace>\<lambda>state. (if state = Structures_A.thread_state.Running then ?P26 cur state else (\<lambda>_. True)) and ?Q17 cur state\<rbrace>
 8. \<And>cur. \<lbrace>?Q'10 cur\<rbrace> getThreadState cur \<lbrace>\<lambda>state'. (if state' = Structures_H.thread_state.Running then ?P'28 cur state' else (\<lambda>_. True)) and ?Q'19 cur state'\<rbrace>
 9. \<lbrace>?Q6\<rbrace> gets cur_thread \<lbrace>\<lambda>cur. tcb_at cur and ?Q10 cur\<rbrace>
 10. \<lbrace>?Q'6\<rbrace> getCurThread \<lbrace>\<lambda>cur. tcb_at' cur and ?Q'10 cur\<rbrace>
A total of 14 subgoals... proof (prove)
goal (13 subgoals):
 1. \<And>cur state state'. thread_state_relation state state' \<Longrightarrow> corres dc (?P26 cur state) (?P'28 cur state') (do ts <- ethread_get tcb_time_slice cur;
let ts' = ts - 1 in if 0 < ts' then thread_set_time_slice cur ts' else do thread_set_time_slice cur timeSlice;
tcb_sched_action tcb_sched_append cur;
reschedule_required
od
od) (do ts <- threadGet tcbTimeSlice cur;
ts' <- return (ts - 1);
if 0 < ts' then threadSet (tcbTimeSlice_update (\<lambda>_. ts')) cur else do threadSet (tcbTimeSlice_update (\<lambda>_. timeSlice)) cur;
tcbSchedAppend cur;
rescheduleRequired
od
od)
 2. \<And>cur state state'. thread_state_relation state state' \<Longrightarrow> corres dc (\<lambda>_. True) (\<lambda>_. True) (return ()) (return ())
 3. \<And>cur state state' y ya. \<lbrakk>thread_state_relation state state'; dc y ya\<rbrakk> \<Longrightarrow> corres dc (?R15 cur state state' y) (?R'15 cur state state' ya) (when (Suc 0 < numDomains) (do y <- dec_domain_time;
dom_time <- gets domain_time;
when (dom_time = 0) reschedule_required
od)) (when (Suc 0 < numDomains) (do y <- decDomainTime;
domainTime <- getDomainTime;
when (domainTime = 0) rescheduleRequired
od))
 4. \<And>cur state state'. thread_state_relation state state' \<Longrightarrow> \<lbrace>?Q17 cur state\<rbrace> if state = Structures_A.thread_state.Running then do ts <- ethread_get tcb_time_slice cur;
let ts' = ts - 1 in if 0 < ts' then thread_set_time_slice cur ts' else do thread_set_time_slice cur timeSlice;
tcb_sched_action tcb_sched_append cur;
reschedule_required
od
od else return () \<lbrace>?R15 cur state state'\<rbrace>
 5. \<And>cur state state'. thread_state_relation state state' \<Longrightarrow> \<lbrace>?Q'19 cur state'\<rbrace> if state' = Structures_H.thread_state.Running then do ts <- threadGet tcbTimeSlice cur;
ts' <- return (ts - 1);
if 0 < ts' then threadSet (tcbTimeSlice_update (\<lambda>_. ts')) cur else do threadSet (tcbTimeSlice_update (\<lambda>_. timeSlice)) cur;
tcbSchedAppend cur;
rescheduleRequired
od
od else return () \<lbrace>?R'15 cur state state'\<rbrace>
 6. \<And>cur. \<lbrace>?Q10 cur\<rbrace> get_thread_state cur \<lbrace>\<lambda>state. (if state = Structures_A.thread_state.Running then ?P26 cur state else (\<lambda>_. True)) and ?Q17 cur state\<rbrace>
 7. \<And>cur. \<lbrace>?Q'10 cur\<rbrace> getThreadState cur \<lbrace>\<lambda>state'. (if state' = Structures_H.thread_state.Running then ?P'28 cur state' else (\<lambda>_. True)) and ?Q'19 cur state'\<rbrace>
 8. \<lbrace>?Q6\<rbrace> gets cur_thread \<lbrace>\<lambda>cur. tcb_at cur and ?Q10 cur\<rbrace>
 9. \<lbrace>?Q'6\<rbrace> getCurThread \<lbrace>\<lambda>cur. tcb_at' cur and ?Q'10 cur\<rbrace>
 10. \<And>s. ((\<lambda>_. True) and (cur_tcb and valid_sched)) s \<Longrightarrow> ((\<lambda>_. True) and ?Q6) s
A total of 13 subgoals... proof (prove)
goal (13 subgoals):
 1. \<And>cur state state'. thread_state_relation state state' \<Longrightarrow> corres dc (?P26 cur state) (?P'28 cur state') (do ts <- ethread_get tcb_time_slice cur;
if Suc 0 < ts then thread_set_time_slice cur (ts - Suc 0) else do thread_set_time_slice cur timeSlice;
tcb_sched_action tcb_sched_append cur;
reschedule_required
od
od) (do ts <- threadGet tcbTimeSlice cur;
if Suc 0 < ts then threadSet (tcbTimeSlice_update (\<lambda>_. ts - Suc 0)) cur else do threadSet (tcbTimeSlice_update (\<lambda>_. timeSlice)) cur;
tcbSchedAppend cur;
rescheduleRequired
od
od)
 2. \<And>cur state state'. thread_state_relation state state' \<Longrightarrow> corres dc (\<lambda>_. True) (\<lambda>_. True) (return ()) (return ())
 3. \<And>cur state state' y ya. \<lbrakk>thread_state_relation state state'; dc y ya\<rbrakk> \<Longrightarrow> corres dc (?R15 cur state state' y) (?R'15 cur state state' ya) (when (Suc 0 < numDomains) (do y <- dec_domain_time;
dom_time <- gets domain_time;
when (dom_time = 0) reschedule_required
od)) (when (Suc 0 < numDomains) (do y <- decDomainTime;
domainTime <- getDomainTime;
when (domainTime = 0) rescheduleRequired
od))
 4. \<And>cur state state'. thread_state_relation state state' \<Longrightarrow> \<lbrace>?Q17 cur state\<rbrace> if state = Structures_A.thread_state.Running then do ts <- ethread_get tcb_time_slice cur;
let ts' = ts - 1 in if 0 < ts' then thread_set_time_slice cur ts' else do thread_set_time_slice cur timeSlice;
tcb_sched_action tcb_sched_append cur;
reschedule_required
od
od else return () \<lbrace>?R15 cur state state'\<rbrace>
 5. \<And>cur state state'. thread_state_relation state state' \<Longrightarrow> \<lbrace>?Q'19 cur state'\<rbrace> if state' = Structures_H.thread_state.Running then do ts <- threadGet tcbTimeSlice cur;
ts' <- return (ts - 1);
if 0 < ts' then threadSet (tcbTimeSlice_update (\<lambda>_. ts')) cur else do threadSet (tcbTimeSlice_update (\<lambda>_. timeSlice)) cur;
tcbSchedAppend cur;
rescheduleRequired
od
od else return () \<lbrace>?R'15 cur state state'\<rbrace>
 6. \<And>cur. \<lbrace>?Q10 cur\<rbrace> get_thread_state cur \<lbrace>\<lambda>state. (if state = Structures_A.thread_state.Running then ?P26 cur state else (\<lambda>_. True)) and ?Q17 cur state\<rbrace>
 7. \<And>cur. \<lbrace>?Q'10 cur\<rbrace> getThreadState cur \<lbrace>\<lambda>state'. (if state' = Structures_H.thread_state.Running then ?P'28 cur state' else (\<lambda>_. True)) and ?Q'19 cur state'\<rbrace>
 8. \<lbrace>?Q6\<rbrace> gets cur_thread \<lbrace>\<lambda>cur. tcb_at cur and ?Q10 cur\<rbrace>
 9. \<lbrace>?Q'6\<rbrace> getCurThread \<lbrace>\<lambda>cur. tcb_at' cur and ?Q'10 cur\<rbrace>
 10. \<And>s. ((\<lambda>_. True) and (cur_tcb and valid_sched)) s \<Longrightarrow> ((\<lambda>_. True) and ?Q6) s
A total of 13 subgoals... proof (prove)
goal (16 subgoals):
 1. \<And>cur state state' etcb tcb'. \<lbrakk>thread_state_relation state state'; etcb_relation etcb tcb'\<rbrakk> \<Longrightarrow> tcb_time_slice etcb = tcbTimeSlice tcb'
 2. \<And>cur state state' rv rv'. \<lbrakk>thread_state_relation state state'; rv = rv'\<rbrakk> \<Longrightarrow> corres dc (?R35 cur state state' rv) (?R'35 cur state state' rv') (if Suc 0 < rv then thread_set_time_slice cur (rv - Suc 0) else do thread_set_time_slice cur timeSlice;
tcb_sched_action tcb_sched_append cur;
reschedule_required
od) (if Suc 0 < rv' then threadSet (tcbTimeSlice_update (\<lambda>_. rv' - Suc 0)) cur else do threadSet (tcbTimeSlice_update (\<lambda>_. timeSlice)) cur;
tcbSchedAppend cur;
rescheduleRequired
od)
 3. \<And>cur state state'. thread_state_relation state state' \<Longrightarrow> \<lbrace>?Q39 cur state\<rbrace> ethread_get tcb_time_slice cur \<lbrace>?R35 cur state state'\<rbrace>
 4. \<And>cur state state'. thread_state_relation state state' \<Longrightarrow> \<lbrace>?Q'41 cur state'\<rbrace> threadGet tcbTimeSlice cur \<lbrace>?R'35 cur state state'\<rbrace>
 5. \<And>cur state state'. thread_state_relation state state' \<Longrightarrow> corres dc (\<lambda>_. True) (\<lambda>_. True) (return ()) (return ())
 6. \<And>cur state state' y ya. \<lbrakk>thread_state_relation state state'; dc y ya\<rbrakk> \<Longrightarrow> corres dc (?R15 cur state state' y) (?R'15 cur state state' ya) (when (Suc 0 < numDomains) (do y <- dec_domain_time;
dom_time <- gets domain_time;
when (dom_time = 0) reschedule_required
od)) (when (Suc 0 < numDomains) (do y <- decDomainTime;
domainTime <- getDomainTime;
when (domainTime = 0) rescheduleRequired
od))
 7. \<And>cur state state'. thread_state_relation state state' \<Longrightarrow> \<lbrace>?Q17 cur state\<rbrace> if state = Structures_A.thread_state.Running then do ts <- ethread_get tcb_time_slice cur;
let ts' = ts - 1 in if 0 < ts' then thread_set_time_slice cur ts' else do thread_set_time_slice cur timeSlice;
tcb_sched_action tcb_sched_append cur;
reschedule_required
od
od else return () \<lbrace>?R15 cur state state'\<rbrace>
 8. \<And>cur state state'. thread_state_relation state state' \<Longrightarrow> \<lbrace>?Q'19 cur state'\<rbrace> if state' = Structures_H.thread_state.Running then do ts <- threadGet tcbTimeSlice cur;
ts' <- return (ts - 1);
if 0 < ts' then threadSet (tcbTimeSlice_update (\<lambda>_. ts')) cur else do threadSet (tcbTimeSlice_update (\<lambda>_. timeSlice)) cur;
tcbSchedAppend cur;
rescheduleRequired
od
od else return () \<lbrace>?R'15 cur state state'\<rbrace>
 9. \<And>cur. \<lbrace>?Q10 cur\<rbrace> get_thread_state cur \<lbrace>\<lambda>state. (if state = Structures_A.thread_state.Running then is_etcb_at cur and ?Q39 cur state else (\<lambda>_. True)) and ?Q17 cur state\<rbrace>
 10. \<And>cur. \<lbrace>?Q'10 cur\<rbrace> getThreadState cur \<lbrace>\<lambda>state'. (if state' = Structures_H.thread_state.Running then tcb_at' cur and ?Q'41 cur state' else (\<lambda>_. True)) and ?Q'19 cur state'\<rbrace>
A total of 16 subgoals... proof (prove)
goal (15 subgoals):
 1. \<And>cur state state' rv rv'. \<lbrakk>thread_state_relation state state'; rv = rv'\<rbrakk> \<Longrightarrow> corres dc (?R35 cur state state' rv) (?R'35 cur state state' rv') (if Suc 0 < rv then thread_set_time_slice cur (rv - Suc 0) else do thread_set_time_slice cur timeSlice;
tcb_sched_action tcb_sched_append cur;
reschedule_required
od) (if Suc 0 < rv' then threadSet (tcbTimeSlice_update (\<lambda>_. rv' - Suc 0)) cur else do threadSet (tcbTimeSlice_update (\<lambda>_. timeSlice)) cur;
tcbSchedAppend cur;
rescheduleRequired
od)
 2. \<And>cur state state'. thread_state_relation state state' \<Longrightarrow> \<lbrace>?Q39 cur state\<rbrace> ethread_get tcb_time_slice cur \<lbrace>?R35 cur state state'\<rbrace>
 3. \<And>cur state state'. thread_state_relation state state' \<Longrightarrow> \<lbrace>?Q'41 cur state'\<rbrace> threadGet tcbTimeSlice cur \<lbrace>?R'35 cur state state'\<rbrace>
 4. \<And>cur state state'. thread_state_relation state state' \<Longrightarrow> corres dc (\<lambda>_. True) (\<lambda>_. True) (return ()) (return ())
 5. \<And>cur state state' y ya. \<lbrakk>thread_state_relation state state'; dc y ya\<rbrakk> \<Longrightarrow> corres dc (?R15 cur state state' y) (?R'15 cur state state' ya) (when (Suc 0 < numDomains) (do y <- dec_domain_time;
dom_time <- gets domain_time;
when (dom_time = 0) reschedule_required
od)) (when (Suc 0 < numDomains) (do y <- decDomainTime;
domainTime <- getDomainTime;
when (domainTime = 0) rescheduleRequired
od))
 6. \<And>cur state state'. thread_state_relation state state' \<Longrightarrow> \<lbrace>?Q17 cur state\<rbrace> if state = Structures_A.thread_state.Running then do ts <- ethread_get tcb_time_slice cur;
let ts' = ts - 1 in if 0 < ts' then thread_set_time_slice cur ts' else do thread_set_time_slice cur timeSlice;
tcb_sched_action tcb_sched_append cur;
reschedule_required
od
od else return () \<lbrace>?R15 cur state state'\<rbrace>
 7. \<And>cur state state'. thread_state_relation state state' \<Longrightarrow> \<lbrace>?Q'19 cur state'\<rbrace> if state' = Structures_H.thread_state.Running then do ts <- threadGet tcbTimeSlice cur;
ts' <- return (ts - 1);
if 0 < ts' then threadSet (tcbTimeSlice_update (\<lambda>_. ts')) cur else do threadSet (tcbTimeSlice_update (\<lambda>_. timeSlice)) cur;
tcbSchedAppend cur;
rescheduleRequired
od
od else return () \<lbrace>?R'15 cur state state'\<rbrace>
 8. \<And>cur. \<lbrace>?Q10 cur\<rbrace> get_thread_state cur \<lbrace>\<lambda>state. (if state = Structures_A.thread_state.Running then is_etcb_at cur and ?Q39 cur state else (\<lambda>_. True)) and ?Q17 cur state\<rbrace>
 9. \<And>cur. \<lbrace>?Q'10 cur\<rbrace> getThreadState cur \<lbrace>\<lambda>state'. (if state' = Structures_H.thread_state.Running then tcb_at' cur and ?Q'41 cur state' else (\<lambda>_. True)) and ?Q'19 cur state'\<rbrace>
 10. \<lbrace>?Q6\<rbrace> gets cur_thread \<lbrace>\<lambda>cur. tcb_at cur and ?Q10 cur\<rbrace>
A total of 15 subgoals... proof (prove)
goal (15 subgoals):
 1. \<And>cur state state' ts ts'. \<lbrakk>thread_state_relation state state'; ts = ts'\<rbrakk> \<Longrightarrow> corres dc (?R35 cur state state' ts) (?R'35 cur state state' ts') (if Suc 0 < ts then thread_set_time_slice cur (ts - Suc 0) else do thread_set_time_slice cur timeSlice;
tcb_sched_action tcb_sched_append cur;
reschedule_required
od) (if Suc 0 < ts' then threadSet (tcbTimeSlice_update (\<lambda>_. ts' - Suc 0)) cur else do threadSet (tcbTimeSlice_update (\<lambda>_. timeSlice)) cur;
tcbSchedAppend cur;
rescheduleRequired
od)
 2. \<And>cur state state'. thread_state_relation state state' \<Longrightarrow> \<lbrace>?Q39 cur state\<rbrace> ethread_get tcb_time_slice cur \<lbrace>?R35 cur state state'\<rbrace>
 3. \<And>cur state state'. thread_state_relation state state' \<Longrightarrow> \<lbrace>?Q'41 cur state'\<rbrace> threadGet tcbTimeSlice cur \<lbrace>?R'35 cur state state'\<rbrace>
 4. \<And>cur state state'. thread_state_relation state state' \<Longrightarrow> corres dc (\<lambda>_. True) (\<lambda>_. True) (return ()) (return ())
 5. \<And>cur state state' y ya. \<lbrakk>thread_state_relation state state'; dc y ya\<rbrakk> \<Longrightarrow> corres dc (?R15 cur state state' y) (?R'15 cur state state' ya) (when (Suc 0 < numDomains) (do y <- dec_domain_time;
dom_time <- gets domain_time;
when (dom_time = 0) reschedule_required
od)) (when (Suc 0 < numDomains) (do y <- decDomainTime;
domainTime <- getDomainTime;
when (domainTime = 0) rescheduleRequired
od))
 6. \<And>cur state state'. thread_state_relation state state' \<Longrightarrow> \<lbrace>?Q17 cur state\<rbrace> if state = Structures_A.thread_state.Running then do ts <- ethread_get tcb_time_slice cur;
let ts' = ts - 1 in if 0 < ts' then thread_set_time_slice cur ts' else do thread_set_time_slice cur timeSlice;
tcb_sched_action tcb_sched_append cur;
reschedule_required
od
od else return () \<lbrace>?R15 cur state state'\<rbrace>
 7. \<And>cur state state'. thread_state_relation state state' \<Longrightarrow> \<lbrace>?Q'19 cur state'\<rbrace> if state' = Structures_H.thread_state.Running then do ts <- threadGet tcbTimeSlice cur;
ts' <- return (ts - 1);
if 0 < ts' then threadSet (tcbTimeSlice_update (\<lambda>_. ts')) cur else do threadSet (tcbTimeSlice_update (\<lambda>_. timeSlice)) cur;
tcbSchedAppend cur;
rescheduleRequired
od
od else return () \<lbrace>?R'15 cur state state'\<rbrace>
 8. \<And>cur. \<lbrace>?Q10 cur\<rbrace> get_thread_state cur \<lbrace>\<lambda>state. (if state = Structures_A.thread_state.Running then is_etcb_at cur and ?Q39 cur state else (\<lambda>_. True)) and ?Q17 cur state\<rbrace>
 9. \<And>cur. \<lbrace>?Q'10 cur\<rbrace> getThreadState cur \<lbrace>\<lambda>state'. (if state' = Structures_H.thread_state.Running then tcb_at' cur and ?Q'41 cur state' else (\<lambda>_. True)) and ?Q'19 cur state'\<rbrace>
 10. \<lbrace>?Q6\<rbrace> gets cur_thread \<lbrace>\<lambda>cur. tcb_at cur and ?Q10 cur\<rbrace>
A total of 15 subgoals... proof (prove)
goal (16 subgoals):
 1. \<And>cur state state' ts ts'. \<lbrakk>thread_state_relation state state'; ts = ts'; 1 < ts\<rbrakk> \<Longrightarrow> corres dc (?P43 cur state state' ts) (?P'45 cur state state' ts') (if Suc 0 < ts then thread_set_time_slice cur (ts - Suc 0) else do thread_set_time_slice cur timeSlice;
tcb_sched_action tcb_sched_append cur;
reschedule_required
od) (if Suc 0 < ts' then threadSet (tcbTimeSlice_update (\<lambda>_. ts' - Suc 0)) cur else do threadSet (tcbTimeSlice_update (\<lambda>_. timeSlice)) cur;
tcbSchedAppend cur;
rescheduleRequired
od)
 2. \<And>cur state state' ts ts'. \<lbrakk>thread_state_relation state state'; ts = ts'; \<not> 1 < ts\<rbrakk> \<Longrightarrow> corres dc (?Q44 cur state state' ts) (?Q'46 cur state state' ts') (if Suc 0 < ts then thread_set_time_slice cur (ts - Suc 0) else do thread_set_time_slice cur timeSlice;
tcb_sched_action tcb_sched_append cur;
reschedule_required
od) (if Suc 0 < ts' then threadSet (tcbTimeSlice_update (\<lambda>_. ts' - Suc 0)) cur else do threadSet (tcbTimeSlice_update (\<lambda>_. timeSlice)) cur;
tcbSchedAppend cur;
rescheduleRequired
od)
 3. \<And>cur state state'. thread_state_relation state state' \<Longrightarrow> \<lbrace>?Q39 cur state\<rbrace> ethread_get tcb_time_slice cur \<lbrace>\<lambda>ts. ?P43 cur state state' ts and ?Q44 cur state state' ts\<rbrace>
 4. \<And>cur state state'. thread_state_relation state state' \<Longrightarrow> \<lbrace>?Q'41 cur state'\<rbrace> threadGet tcbTimeSlice cur \<lbrace>\<lambda>ts'. ?P'45 cur state state' ts' and ?Q'46 cur state state' ts'\<rbrace>
 5. \<And>cur state state'. thread_state_relation state state' \<Longrightarrow> corres dc (\<lambda>_. True) (\<lambda>_. True) (return ()) (return ())
 6. \<And>cur state state' y ya. \<lbrakk>thread_state_relation state state'; dc y ya\<rbrakk> \<Longrightarrow> corres dc (?R15 cur state state' y) (?R'15 cur state state' ya) (when (Suc 0 < numDomains) (do y <- dec_domain_time;
dom_time <- gets domain_time;
when (dom_time = 0) reschedule_required
od)) (when (Suc 0 < numDomains) (do y <- decDomainTime;
domainTime <- getDomainTime;
when (domainTime = 0) rescheduleRequired
od))
 7. \<And>cur state state'. thread_state_relation state state' \<Longrightarrow> \<lbrace>?Q17 cur state\<rbrace> if state = Structures_A.thread_state.Running then do ts <- ethread_get tcb_time_slice cur;
let ts' = ts - 1 in if 0 < ts' then thread_set_time_slice cur ts' else do thread_set_time_slice cur timeSlice;
tcb_sched_action tcb_sched_append cur;
reschedule_required
od
od else return () \<lbrace>?R15 cur state state'\<rbrace>
 8. \<And>cur state state'. thread_state_relation state state' \<Longrightarrow> \<lbrace>?Q'19 cur state'\<rbrace> if state' = Structures_H.thread_state.Running then do ts <- threadGet tcbTimeSlice cur;
ts' <- return (ts - 1);
if 0 < ts' then threadSet (tcbTimeSlice_update (\<lambda>_. ts')) cur else do threadSet (tcbTimeSlice_update (\<lambda>_. timeSlice)) cur;
tcbSchedAppend cur;
rescheduleRequired
od
od else return () \<lbrace>?R'15 cur state state'\<rbrace>
 9. \<And>cur. \<lbrace>?Q10 cur\<rbrace> get_thread_state cur \<lbrace>\<lambda>state. (if state = Structures_A.thread_state.Running then is_etcb_at cur and ?Q39 cur state else (\<lambda>_. True)) and ?Q17 cur state\<rbrace>
 10. \<And>cur. \<lbrace>?Q'10 cur\<rbrace> getThreadState cur \<lbrace>\<lambda>state'. (if state' = Structures_H.thread_state.Running then tcb_at' cur and ?Q'41 cur state' else (\<lambda>_. True)) and ?Q'19 cur state'\<rbrace>
A total of 16 subgoals... proof (prove)
goal (16 subgoals):
 1. \<And>cur state state' ts ts'. \<lbrakk>thread_state_relation state state'; ts = ts'; Suc 0 < ts'\<rbrakk> \<Longrightarrow> corres dc (?P43 cur state state' ts') (?P'45 cur state state' ts') (thread_set_time_slice cur (ts' - Suc 0)) (threadSet (tcbTimeSlice_update (\<lambda>_. ts' - Suc 0)) cur)
 2. \<And>cur state state' ts ts'. \<lbrakk>thread_state_relation state state'; ts = ts'; \<not> 1 < ts\<rbrakk> \<Longrightarrow> corres dc (?Q44 cur state state' ts) (?Q'46 cur state state' ts') (if Suc 0 < ts then thread_set_time_slice cur (ts - Suc 0) else do thread_set_time_slice cur timeSlice;
tcb_sched_action tcb_sched_append cur;
reschedule_required
od) (if Suc 0 < ts' then threadSet (tcbTimeSlice_update (\<lambda>_. ts' - Suc 0)) cur else do threadSet (tcbTimeSlice_update (\<lambda>_. timeSlice)) cur;
tcbSchedAppend cur;
rescheduleRequired
od)
 3. \<And>cur state state'. thread_state_relation state state' \<Longrightarrow> \<lbrace>?Q39 cur state\<rbrace> ethread_get tcb_time_slice cur \<lbrace>\<lambda>ts. ?P43 cur state state' ts and ?Q44 cur state state' ts\<rbrace>
 4. \<And>cur state state'. thread_state_relation state state' \<Longrightarrow> \<lbrace>?Q'41 cur state'\<rbrace> threadGet tcbTimeSlice cur \<lbrace>\<lambda>ts'. ?P'45 cur state state' ts' and ?Q'46 cur state state' ts'\<rbrace>
 5. \<And>cur state state'. thread_state_relation state state' \<Longrightarrow> corres dc (\<lambda>_. True) (\<lambda>_. True) (return ()) (return ())
 6. \<And>cur state state' y ya. \<lbrakk>thread_state_relation state state'; dc y ya\<rbrakk> \<Longrightarrow> corres dc (?R15 cur state state' y) (?R'15 cur state state' ya) (when (Suc 0 < numDomains) (do y <- dec_domain_time;
dom_time <- gets domain_time;
when (dom_time = 0) reschedule_required
od)) (when (Suc 0 < numDomains) (do y <- decDomainTime;
domainTime <- getDomainTime;
when (domainTime = 0) rescheduleRequired
od))
 7. \<And>cur state state'. thread_state_relation state state' \<Longrightarrow> \<lbrace>?Q17 cur state\<rbrace> if state = Structures_A.thread_state.Running then do ts <- ethread_get tcb_time_slice cur;
let ts' = ts - 1 in if 0 < ts' then thread_set_time_slice cur ts' else do thread_set_time_slice cur timeSlice;
tcb_sched_action tcb_sched_append cur;
reschedule_required
od
od else return () \<lbrace>?R15 cur state state'\<rbrace>
 8. \<And>cur state state'. thread_state_relation state state' \<Longrightarrow> \<lbrace>?Q'19 cur state'\<rbrace> if state' = Structures_H.thread_state.Running then do ts <- threadGet tcbTimeSlice cur;
ts' <- return (ts - 1);
if 0 < ts' then threadSet (tcbTimeSlice_update (\<lambda>_. ts')) cur else do threadSet (tcbTimeSlice_update (\<lambda>_. timeSlice)) cur;
tcbSchedAppend cur;
rescheduleRequired
od
od else return () \<lbrace>?R'15 cur state state'\<rbrace>
 9. \<And>cur. \<lbrace>?Q10 cur\<rbrace> get_thread_state cur \<lbrace>\<lambda>state. (if state = Structures_A.thread_state.Running then is_etcb_at cur and ?Q39 cur state else (\<lambda>_. True)) and ?Q17 cur state\<rbrace>
 10. \<And>cur. \<lbrace>?Q'10 cur\<rbrace> getThreadState cur \<lbrace>\<lambda>state'. (if state' = Structures_H.thread_state.Running then tcb_at' cur and ?Q'41 cur state' else (\<lambda>_. True)) and ?Q'19 cur state'\<rbrace>
A total of 16 subgoals... proof (prove)
goal (16 subgoals):
 1. \<And>cur state state' ts ts'. \<lbrakk>thread_state_relation state state'; ts = ts'; Suc 0 < ts'\<rbrakk> \<Longrightarrow> corres dc (?P43 cur state state' ts') (?P'45 cur state state' ts') (ethread_set (tcb_time_slice_update (\<lambda>_. ts' - Suc 0)) cur) (threadSet (tcbTimeSlice_update (\<lambda>_. ts' - Suc 0)) cur)
 2. \<And>cur state state' ts ts'. \<lbrakk>thread_state_relation state state'; ts = ts'; \<not> 1 < ts\<rbrakk> \<Longrightarrow> corres dc (?Q44 cur state state' ts) (?Q'46 cur state state' ts') (if Suc 0 < ts then ethread_set (tcb_time_slice_update (\<lambda>_. ts - Suc 0)) cur else do ethread_set (tcb_time_slice_update (\<lambda>_. timeSlice)) cur;
tcb_sched_action tcb_sched_append cur;
reschedule_required
od) (if Suc 0 < ts' then threadSet (tcbTimeSlice_update (\<lambda>_. ts' - Suc 0)) cur else do threadSet (tcbTimeSlice_update (\<lambda>_. timeSlice)) cur;
tcbSchedAppend cur;
rescheduleRequired
od)
 3. \<And>cur state state'. thread_state_relation state state' \<Longrightarrow> \<lbrace>?Q39 cur state\<rbrace> ethread_get tcb_time_slice cur \<lbrace>\<lambda>ts. ?P43 cur state state' ts and ?Q44 cur state state' ts\<rbrace>
 4. \<And>cur state state'. thread_state_relation state state' \<Longrightarrow> \<lbrace>?Q'41 cur state'\<rbrace> threadGet tcbTimeSlice cur \<lbrace>\<lambda>ts'. ?P'45 cur state state' ts' and ?Q'46 cur state state' ts'\<rbrace>
 5. \<And>cur state state'. thread_state_relation state state' \<Longrightarrow> corres dc (\<lambda>_. True) (\<lambda>_. True) (return ()) (return ())
 6. \<And>cur state state' y ya. \<lbrakk>thread_state_relation state state'; dc y ya\<rbrakk> \<Longrightarrow> corres dc (?R15 cur state state' y) (?R'15 cur state state' ya) (when (Suc 0 < numDomains) (do y <- dec_domain_time;
dom_time <- gets domain_time;
when (dom_time = 0) reschedule_required
od)) (when (Suc 0 < numDomains) (do y <- decDomainTime;
domainTime <- getDomainTime;
when (domainTime = 0) rescheduleRequired
od))
 7. \<And>cur state state'. thread_state_relation state state' \<Longrightarrow> \<lbrace>?Q17 cur state\<rbrace> if state = Structures_A.thread_state.Running then do ts <- ethread_get tcb_time_slice cur;
let ts' = ts - 1 in if 0 < ts' then ethread_set (tcb_time_slice_update (\<lambda>_. ts')) cur else do ethread_set (tcb_time_slice_update (\<lambda>_. timeSlice)) cur;
tcb_sched_action tcb_sched_append cur;
reschedule_required
od
od else return () \<lbrace>?R15 cur state state'\<rbrace>
 8. \<And>cur state state'. thread_state_relation state state' \<Longrightarrow> \<lbrace>?Q'19 cur state'\<rbrace> if state' = Structures_H.thread_state.Running then do ts <- threadGet tcbTimeSlice cur;
ts' <- return (ts - 1);
if 0 < ts' then threadSet (tcbTimeSlice_update (\<lambda>_. ts')) cur else do threadSet (tcbTimeSlice_update (\<lambda>_. timeSlice)) cur;
tcbSchedAppend cur;
rescheduleRequired
od
od else return () \<lbrace>?R'15 cur state state'\<rbrace>
 9. \<And>cur. \<lbrace>?Q10 cur\<rbrace> get_thread_state cur \<lbrace>\<lambda>state. (if state = Structures_A.thread_state.Running then is_etcb_at cur and ?Q39 cur state else (\<lambda>_. True)) and ?Q17 cur state\<rbrace>
 10. \<And>cur. \<lbrace>?Q'10 cur\<rbrace> getThreadState cur \<lbrace>\<lambda>state'. (if state' = Structures_H.thread_state.Running then tcb_at' cur and ?Q'41 cur state' else (\<lambda>_. True)) and ?Q'19 cur state'\<rbrace>
A total of 16 subgoals... proof (prove)
goal (16 subgoals):
 1. \<And>state state' ts ts' etcb tcb'. \<lbrakk>thread_state_relation state state'; ts = ts'; Suc 0 < ts'; etcb_relation etcb tcb'\<rbrakk> \<Longrightarrow> etcb_relation (etcb\<lparr>tcb_time_slice := ts' - Suc 0\<rparr>) (tcbTimeSlice_update (\<lambda>_. ts' - Suc 0) tcb')
 2. \<And>cur state state' ts ts'. \<lbrakk>thread_state_relation state state'; ts = ts'; \<not> 1 < ts\<rbrakk> \<Longrightarrow> corres dc (?Q44 cur state state' ts) (?Q'46 cur state state' ts') (if Suc 0 < ts then ethread_set (tcb_time_slice_update (\<lambda>_. ts - Suc 0)) cur else do ethread_set (tcb_time_slice_update (\<lambda>_. timeSlice)) cur;
tcb_sched_action tcb_sched_append cur;
reschedule_required
od) (if Suc 0 < ts' then threadSet (tcbTimeSlice_update (\<lambda>_. ts' - Suc 0)) cur else do threadSet (tcbTimeSlice_update (\<lambda>_. timeSlice)) cur;
tcbSchedAppend cur;
rescheduleRequired
od)
 3. \<And>cur state state'. thread_state_relation state state' \<Longrightarrow> \<lbrace>?Q39 cur state\<rbrace> ethread_get tcb_time_slice cur \<lbrace>\<lambda>ts. tcb_at cur and valid_etcbs and ?Q44 cur state state' ts\<rbrace>
 4. \<And>cur state state'. thread_state_relation state state' \<Longrightarrow> \<lbrace>?Q'41 cur state'\<rbrace> threadGet tcbTimeSlice cur \<lbrace>\<lambda>ts'. tcb_at' cur and ?Q'46 cur state state' ts'\<rbrace>
 5. \<And>cur state state'. thread_state_relation state state' \<Longrightarrow> corres dc (\<lambda>_. True) (\<lambda>_. True) (return ()) (return ())
 6. \<And>cur state state' y ya. \<lbrakk>thread_state_relation state state'; dc y ya\<rbrakk> \<Longrightarrow> corres dc (?R15 cur state state' y) (?R'15 cur state state' ya) (when (Suc 0 < numDomains) (do y <- dec_domain_time;
dom_time <- gets domain_time;
when (dom_time = 0) reschedule_required
od)) (when (Suc 0 < numDomains) (do y <- decDomainTime;
domainTime <- getDomainTime;
when (domainTime = 0) rescheduleRequired
od))
 7. \<And>cur state state'. thread_state_relation state state' \<Longrightarrow> \<lbrace>?Q17 cur state\<rbrace> if state = Structures_A.thread_state.Running then do ts <- ethread_get tcb_time_slice cur;
let ts' = ts - 1 in if 0 < ts' then ethread_set (tcb_time_slice_update (\<lambda>_. ts')) cur else do ethread_set (tcb_time_slice_update (\<lambda>_. timeSlice)) cur;
tcb_sched_action tcb_sched_append cur;
reschedule_required
od
od else return () \<lbrace>?R15 cur state state'\<rbrace>
 8. \<And>cur state state'. thread_state_relation state state' \<Longrightarrow> \<lbrace>?Q'19 cur state'\<rbrace> if state' = Structures_H.thread_state.Running then do ts <- threadGet tcbTimeSlice cur;
ts' <- return (ts - 1);
if 0 < ts' then threadSet (tcbTimeSlice_update (\<lambda>_. ts')) cur else do threadSet (tcbTimeSlice_update (\<lambda>_. timeSlice)) cur;
tcbSchedAppend cur;
rescheduleRequired
od
od else return () \<lbrace>?R'15 cur state state'\<rbrace>
 9. \<And>cur. \<lbrace>?Q10 cur\<rbrace> get_thread_state cur \<lbrace>\<lambda>state. (if state = Structures_A.thread_state.Running then is_etcb_at cur and ?Q39 cur state else (\<lambda>_. True)) and ?Q17 cur state\<rbrace>
 10. \<And>cur. \<lbrace>?Q'10 cur\<rbrace> getThreadState cur \<lbrace>\<lambda>state'. (if state' = Structures_H.thread_state.Running then tcb_at' cur and ?Q'41 cur state' else (\<lambda>_. True)) and ?Q'19 cur state'\<rbrace>
A total of 16 subgoals... proof (prove)
goal (15 subgoals):
 1. \<And>cur state state' ts ts'. \<lbrakk>thread_state_relation state state'; ts = ts'; \<not> 1 < ts\<rbrakk> \<Longrightarrow> corres dc (?Q44 cur state state' ts) (?Q'46 cur state state' ts') (if Suc 0 < ts then ethread_set (tcb_time_slice_update (\<lambda>_. ts - Suc 0)) cur else do ethread_set (tcb_time_slice_update (\<lambda>_. timeSlice)) cur;
tcb_sched_action tcb_sched_append cur;
reschedule_required
od) (if Suc 0 < ts' then threadSet (tcbTimeSlice_update (\<lambda>_. ts' - Suc 0)) cur else do threadSet (tcbTimeSlice_update (\<lambda>_. timeSlice)) cur;
tcbSchedAppend cur;
rescheduleRequired
od)
 2. \<And>cur state state'. thread_state_relation state state' \<Longrightarrow> \<lbrace>?Q39 cur state\<rbrace> ethread_get tcb_time_slice cur \<lbrace>\<lambda>ts. tcb_at cur and valid_etcbs and ?Q44 cur state state' ts\<rbrace>
 3. \<And>cur state state'. thread_state_relation state state' \<Longrightarrow> \<lbrace>?Q'41 cur state'\<rbrace> threadGet tcbTimeSlice cur \<lbrace>\<lambda>ts'. tcb_at' cur and ?Q'46 cur state state' ts'\<rbrace>
 4. \<And>cur state state'. thread_state_relation state state' \<Longrightarrow> corres dc (\<lambda>_. True) (\<lambda>_. True) (return ()) (return ())
 5. \<And>cur state state' y ya. \<lbrakk>thread_state_relation state state'; dc y ya\<rbrakk> \<Longrightarrow> corres dc (?R15 cur state state' y) (?R'15 cur state state' ya) (when (Suc 0 < numDomains) (do y <- dec_domain_time;
dom_time <- gets domain_time;
when (dom_time = 0) reschedule_required
od)) (when (Suc 0 < numDomains) (do y <- decDomainTime;
domainTime <- getDomainTime;
when (domainTime = 0) rescheduleRequired
od))
 6. \<And>cur state state'. thread_state_relation state state' \<Longrightarrow> \<lbrace>?Q17 cur state\<rbrace> if state = Structures_A.thread_state.Running then do ts <- ethread_get tcb_time_slice cur;
let ts' = ts - 1 in if 0 < ts' then ethread_set (tcb_time_slice_update (\<lambda>_. ts')) cur else do ethread_set (tcb_time_slice_update (\<lambda>_. timeSlice)) cur;
tcb_sched_action tcb_sched_append cur;
reschedule_required
od
od else return () \<lbrace>?R15 cur state state'\<rbrace>
 7. \<And>cur state state'. thread_state_relation state state' \<Longrightarrow> \<lbrace>?Q'19 cur state'\<rbrace> if state' = Structures_H.thread_state.Running then do ts <- threadGet tcbTimeSlice cur;
ts' <- return (ts - 1);
if 0 < ts' then threadSet (tcbTimeSlice_update (\<lambda>_. ts')) cur else do threadSet (tcbTimeSlice_update (\<lambda>_. timeSlice)) cur;
tcbSchedAppend cur;
rescheduleRequired
od
od else return () \<lbrace>?R'15 cur state state'\<rbrace>
 8. \<And>cur. \<lbrace>?Q10 cur\<rbrace> get_thread_state cur \<lbrace>\<lambda>state. (if state = Structures_A.thread_state.Running then is_etcb_at cur and ?Q39 cur state else (\<lambda>_. True)) and ?Q17 cur state\<rbrace>
 9. \<And>cur. \<lbrace>?Q'10 cur\<rbrace> getThreadState cur \<lbrace>\<lambda>state'. (if state' = Structures_H.thread_state.Running then tcb_at' cur and ?Q'41 cur state' else (\<lambda>_. True)) and ?Q'19 cur state'\<rbrace>
 10. \<lbrace>?Q6\<rbrace> gets cur_thread \<lbrace>\<lambda>cur. tcb_at cur and ?Q10 cur\<rbrace>
A total of 15 subgoals... proof (prove)
goal (15 subgoals):
 1. \<And>cur state state' ts ts'. \<lbrakk>thread_state_relation state state'; ts = ts'; \<not> Suc 0 < ts'\<rbrakk> \<Longrightarrow> corres dc (?Q44 cur state state' ts') (?Q'46 cur state state' ts') (do y <- ethread_set (tcb_time_slice_update (\<lambda>_. timeSlice)) cur;
y <- tcb_sched_action tcb_sched_append cur;
reschedule_required
od) (do y <- threadSet (tcbTimeSlice_update (\<lambda>_. timeSlice)) cur;
y <- tcbSchedAppend cur;
rescheduleRequired
od)
 2. \<And>cur state state'. thread_state_relation state state' \<Longrightarrow> \<lbrace>?Q39 cur state\<rbrace> ethread_get tcb_time_slice cur \<lbrace>\<lambda>ts. tcb_at cur and valid_etcbs and ?Q44 cur state state' ts\<rbrace>
 3. \<And>cur state state'. thread_state_relation state state' \<Longrightarrow> \<lbrace>?Q'41 cur state'\<rbrace> threadGet tcbTimeSlice cur \<lbrace>\<lambda>ts'. tcb_at' cur and ?Q'46 cur state state' ts'\<rbrace>
 4. \<And>cur state state'. thread_state_relation state state' \<Longrightarrow> corres dc (\<lambda>_. True) (\<lambda>_. True) (return ()) (return ())
 5. \<And>cur state state' y ya. \<lbrakk>thread_state_relation state state'; dc y ya\<rbrakk> \<Longrightarrow> corres dc (?R15 cur state state' y) (?R'15 cur state state' ya) (when (Suc 0 < numDomains) (do y <- dec_domain_time;
dom_time <- gets domain_time;
when (dom_time = 0) reschedule_required
od)) (when (Suc 0 < numDomains) (do y <- decDomainTime;
domainTime <- getDomainTime;
when (domainTime = 0) rescheduleRequired
od))
 6. \<And>cur state state'. thread_state_relation state state' \<Longrightarrow> \<lbrace>?Q17 cur state\<rbrace> if state = Structures_A.thread_state.Running then do ts <- ethread_get tcb_time_slice cur;
let ts' = ts - 1 in if 0 < ts' then ethread_set (tcb_time_slice_update (\<lambda>_. ts')) cur else do ethread_set (tcb_time_slice_update (\<lambda>_. timeSlice)) cur;
tcb_sched_action tcb_sched_append cur;
reschedule_required
od
od else return () \<lbrace>?R15 cur state state'\<rbrace>
 7. \<And>cur state state'. thread_state_relation state state' \<Longrightarrow> \<lbrace>?Q'19 cur state'\<rbrace> if state' = Structures_H.thread_state.Running then do ts <- threadGet tcbTimeSlice cur;
ts' <- return (ts - 1);
if 0 < ts' then threadSet (tcbTimeSlice_update (\<lambda>_. ts')) cur else do threadSet (tcbTimeSlice_update (\<lambda>_. timeSlice)) cur;
tcbSchedAppend cur;
rescheduleRequired
od
od else return () \<lbrace>?R'15 cur state state'\<rbrace>
 8. \<And>cur. \<lbrace>?Q10 cur\<rbrace> get_thread_state cur \<lbrace>\<lambda>state. (if state = Structures_A.thread_state.Running then is_etcb_at cur and ?Q39 cur state else (\<lambda>_. True)) and ?Q17 cur state\<rbrace>
 9. \<And>cur. \<lbrace>?Q'10 cur\<rbrace> getThreadState cur \<lbrace>\<lambda>state'. (if state' = Structures_H.thread_state.Running then tcb_at' cur and ?Q'41 cur state' else (\<lambda>_. True)) and ?Q'19 cur state'\<rbrace>
 10. \<lbrace>?Q6\<rbrace> gets cur_thread \<lbrace>\<lambda>cur. tcb_at cur and ?Q10 cur\<rbrace>
A total of 15 subgoals... proof (prove)
goal (18 subgoals):
 1. \<And>cur state state' ts ts'. \<lbrakk>thread_state_relation state state'; ts = ts'; \<not> Suc 0 < ts'\<rbrakk> \<Longrightarrow> corres (?r'58 cur state state' ts ts') (?P59 cur state state' ts') (?P'61 cur state state' ts') (ethread_set (tcb_time_slice_update (\<lambda>_. timeSlice)) cur) (threadSet (tcbTimeSlice_update (\<lambda>_. timeSlice)) cur)
 2. \<And>cur state state' ts ts' y rv'. \<lbrakk>thread_state_relation state state'; ts = ts'; \<not> Suc 0 < ts'; ?r'58 cur state state' ts ts' y rv'\<rbrakk> \<Longrightarrow> corres dc (?R58 cur state state' ts ts' y) (?R'58 cur state state' ts ts' rv') (do y <- tcb_sched_action tcb_sched_append cur;
reschedule_required
od) (do y <- tcbSchedAppend cur;
rescheduleRequired
od)
 3. \<And>cur state state' ts ts'. \<lbrakk>thread_state_relation state state'; ts = ts'; \<not> Suc 0 < ts'\<rbrakk> \<Longrightarrow> \<lbrace>?Q60 cur state state' ts'\<rbrace> ethread_set (tcb_time_slice_update (\<lambda>_. timeSlice)) cur \<lbrace>?R58 cur state state' ts ts'\<rbrace>
 4. \<And>cur state state' ts ts'. \<lbrakk>thread_state_relation state state'; ts = ts'; \<not> Suc 0 < ts'\<rbrakk> \<Longrightarrow> \<lbrace>?Q'62 cur state state' ts'\<rbrace> threadSet (tcbTimeSlice_update (\<lambda>_. timeSlice)) cur \<lbrace>?R'58 cur state state' ts ts'\<rbrace>
 5. \<And>cur state state'. thread_state_relation state state' \<Longrightarrow> \<lbrace>?Q39 cur state\<rbrace> ethread_get tcb_time_slice cur \<lbrace>\<lambda>ts. tcb_at cur and valid_etcbs and (?P59 cur state state' ts and ?Q60 cur state state' ts)\<rbrace>
 6. \<And>cur state state'. thread_state_relation state state' \<Longrightarrow> \<lbrace>?Q'41 cur state'\<rbrace> threadGet tcbTimeSlice cur \<lbrace>\<lambda>ts'. tcb_at' cur and (?P'61 cur state state' ts' and ?Q'62 cur state state' ts')\<rbrace>
 7. \<And>cur state state'. thread_state_relation state state' \<Longrightarrow> corres dc (\<lambda>_. True) (\<lambda>_. True) (return ()) (return ())
 8. \<And>cur state state' y ya. \<lbrakk>thread_state_relation state state'; dc y ya\<rbrakk> \<Longrightarrow> corres dc (?R15 cur state state' y) (?R'15 cur state state' ya) (when (Suc 0 < numDomains) (do y <- dec_domain_time;
dom_time <- gets domain_time;
when (dom_time = 0) reschedule_required
od)) (when (Suc 0 < numDomains) (do y <- decDomainTime;
domainTime <- getDomainTime;
when (domainTime = 0) rescheduleRequired
od))
 9. \<And>cur state state'. thread_state_relation state state' \<Longrightarrow> \<lbrace>?Q17 cur state\<rbrace> if state = Structures_A.thread_state.Running then do ts <- ethread_get tcb_time_slice cur;
let ts' = ts - 1 in if 0 < ts' then ethread_set (tcb_time_slice_update (\<lambda>_. ts')) cur else do ethread_set (tcb_time_slice_update (\<lambda>_. timeSlice)) cur;
tcb_sched_action tcb_sched_append cur;
reschedule_required
od
od else return () \<lbrace>?R15 cur state state'\<rbrace>
 10. \<And>cur state state'. thread_state_relation state state' \<Longrightarrow> \<lbrace>?Q'19 cur state'\<rbrace> if state' = Structures_H.thread_state.Running then do ts <- threadGet tcbTimeSlice cur;
ts' <- return (ts - 1);
if 0 < ts' then threadSet (tcbTimeSlice_update (\<lambda>_. ts')) cur else do threadSet (tcbTimeSlice_update (\<lambda>_. timeSlice)) cur;
tcbSchedAppend cur;
rescheduleRequired
od
od else return () \<lbrace>?R'15 cur state state'\<rbrace>
A total of 18 subgoals... proof (prove)
goal (18 subgoals):
 1. \<And>state state' ts ts' etcb tcb'. \<lbrakk>thread_state_relation state state'; ts = ts'; \<not> Suc 0 < ts'; etcb_relation etcb tcb'\<rbrakk> \<Longrightarrow> etcb_relation (etcb\<lparr>tcb_time_slice := timeSlice\<rparr>) (tcbTimeSlice_update (\<lambda>_. timeSlice) tcb')
 2. \<And>cur state state' ts ts' y rv'. \<lbrakk>thread_state_relation state state'; ts = ts'; \<not> Suc 0 < ts'; dc y rv'\<rbrakk> \<Longrightarrow> corres dc (?R58 cur state state' ts ts' y) (?R'58 cur state state' ts ts' rv') (do y <- tcb_sched_action tcb_sched_append cur;
reschedule_required
od) (do y <- tcbSchedAppend cur;
rescheduleRequired
od)
 3. \<And>cur state state' ts ts'. \<lbrakk>thread_state_relation state state'; ts = ts'; \<not> Suc 0 < ts'\<rbrakk> \<Longrightarrow> \<lbrace>?Q60 cur state state' ts'\<rbrace> ethread_set (tcb_time_slice_update (\<lambda>_. timeSlice)) cur \<lbrace>?R58 cur state state' ts ts'\<rbrace>
 4. \<And>cur state state' ts ts'. \<lbrakk>thread_state_relation state state'; ts = ts'; \<not> Suc 0 < ts'\<rbrakk> \<Longrightarrow> \<lbrace>?Q'62 cur state state' ts'\<rbrace> threadSet (tcbTimeSlice_update (\<lambda>_. timeSlice)) cur \<lbrace>?R'58 cur state state' ts ts'\<rbrace>
 5. \<And>cur state state'. thread_state_relation state state' \<Longrightarrow> \<lbrace>?Q39 cur state\<rbrace> ethread_get tcb_time_slice cur \<lbrace>\<lambda>ts. tcb_at cur and valid_etcbs and (tcb_at cur and valid_etcbs and ?Q60 cur state state' ts)\<rbrace>
 6. \<And>cur state state'. thread_state_relation state state' \<Longrightarrow> \<lbrace>?Q'41 cur state'\<rbrace> threadGet tcbTimeSlice cur \<lbrace>\<lambda>ts'. tcb_at' cur and (tcb_at' cur and ?Q'62 cur state state' ts')\<rbrace>
 7. \<And>cur state state'. thread_state_relation state state' \<Longrightarrow> corres dc (\<lambda>_. True) (\<lambda>_. True) (return ()) (return ())
 8. \<And>cur state state' y ya. \<lbrakk>thread_state_relation state state'; dc y ya\<rbrakk> \<Longrightarrow> corres dc (?R15 cur state state' y) (?R'15 cur state state' ya) (when (Suc 0 < numDomains) (do y <- dec_domain_time;
dom_time <- gets domain_time;
when (dom_time = 0) reschedule_required
od)) (when (Suc 0 < numDomains) (do y <- decDomainTime;
domainTime <- getDomainTime;
when (domainTime = 0) rescheduleRequired
od))
 9. \<And>cur state state'. thread_state_relation state state' \<Longrightarrow> \<lbrace>?Q17 cur state\<rbrace> if state = Structures_A.thread_state.Running then do ts <- ethread_get tcb_time_slice cur;
let ts' = ts - 1 in if 0 < ts' then ethread_set (tcb_time_slice_update (\<lambda>_. ts')) cur else do ethread_set (tcb_time_slice_update (\<lambda>_. timeSlice)) cur;
tcb_sched_action tcb_sched_append cur;
reschedule_required
od
od else return () \<lbrace>?R15 cur state state'\<rbrace>
 10. \<And>cur state state'. thread_state_relation state state' \<Longrightarrow> \<lbrace>?Q'19 cur state'\<rbrace> if state' = Structures_H.thread_state.Running then do ts <- threadGet tcbTimeSlice cur;
ts' <- return (ts - 1);
if 0 < ts' then threadSet (tcbTimeSlice_update (\<lambda>_. ts')) cur else do threadSet (tcbTimeSlice_update (\<lambda>_. timeSlice)) cur;
tcbSchedAppend cur;
rescheduleRequired
od
od else return () \<lbrace>?R'15 cur state state'\<rbrace>
A total of 18 subgoals... proof (prove)
goal (17 subgoals):
 1. \<And>cur state state' ts ts' y rv'. \<lbrakk>thread_state_relation state state'; ts = ts'; \<not> Suc 0 < ts'; dc y rv'\<rbrakk> \<Longrightarrow> corres dc (?R58 cur state state' ts ts' y) (?R'58 cur state state' ts ts' rv') (do y <- tcb_sched_action tcb_sched_append cur;
reschedule_required
od) (do y <- tcbSchedAppend cur;
rescheduleRequired
od)
 2. \<And>cur state state' ts ts'. \<lbrakk>thread_state_relation state state'; ts = ts'; \<not> Suc 0 < ts'\<rbrakk> \<Longrightarrow> \<lbrace>?Q60 cur state state' ts'\<rbrace> ethread_set (tcb_time_slice_update (\<lambda>_. timeSlice)) cur \<lbrace>?R58 cur state state' ts ts'\<rbrace>
 3. \<And>cur state state' ts ts'. \<lbrakk>thread_state_relation state state'; ts = ts'; \<not> Suc 0 < ts'\<rbrakk> \<Longrightarrow> \<lbrace>?Q'62 cur state state' ts'\<rbrace> threadSet (tcbTimeSlice_update (\<lambda>_. timeSlice)) cur \<lbrace>?R'58 cur state state' ts ts'\<rbrace>
 4. \<And>cur state state'. thread_state_relation state state' \<Longrightarrow> \<lbrace>?Q39 cur state\<rbrace> ethread_get tcb_time_slice cur \<lbrace>\<lambda>ts. tcb_at cur and valid_etcbs and (tcb_at cur and valid_etcbs and ?Q60 cur state state' ts)\<rbrace>
 5. \<And>cur state state'. thread_state_relation state state' \<Longrightarrow> \<lbrace>?Q'41 cur state'\<rbrace> threadGet tcbTimeSlice cur \<lbrace>\<lambda>ts'. tcb_at' cur and (tcb_at' cur and ?Q'62 cur state state' ts')\<rbrace>
 6. \<And>cur state state'. thread_state_relation state state' \<Longrightarrow> corres dc (\<lambda>_. True) (\<lambda>_. True) (return ()) (return ())
 7. \<And>cur state state' y ya. \<lbrakk>thread_state_relation state state'; dc y ya\<rbrakk> \<Longrightarrow> corres dc (?R15 cur state state' y) (?R'15 cur state state' ya) (when (Suc 0 < numDomains) (do y <- dec_domain_time;
dom_time <- gets domain_time;
when (dom_time = 0) reschedule_required
od)) (when (Suc 0 < numDomains) (do y <- decDomainTime;
domainTime <- getDomainTime;
when (domainTime = 0) rescheduleRequired
od))
 8. \<And>cur state state'. thread_state_relation state state' \<Longrightarrow> \<lbrace>?Q17 cur state\<rbrace> if state = Structures_A.thread_state.Running then do ts <- ethread_get tcb_time_slice cur;
let ts' = ts - 1 in if 0 < ts' then ethread_set (tcb_time_slice_update (\<lambda>_. ts')) cur else do ethread_set (tcb_time_slice_update (\<lambda>_. timeSlice)) cur;
tcb_sched_action tcb_sched_append cur;
reschedule_required
od
od else return () \<lbrace>?R15 cur state state'\<rbrace>
 9. \<And>cur state state'. thread_state_relation state state' \<Longrightarrow> \<lbrace>?Q'19 cur state'\<rbrace> if state' = Structures_H.thread_state.Running then do ts <- threadGet tcbTimeSlice cur;
ts' <- return (ts - 1);
if 0 < ts' then threadSet (tcbTimeSlice_update (\<lambda>_. ts')) cur else do threadSet (tcbTimeSlice_update (\<lambda>_. timeSlice)) cur;
tcbSchedAppend cur;
rescheduleRequired
od
od else return () \<lbrace>?R'15 cur state state'\<rbrace>
 10. \<And>cur. \<lbrace>?Q10 cur\<rbrace> get_thread_state cur \<lbrace>\<lambda>state. (if state = Structures_A.thread_state.Running then is_etcb_at cur and ?Q39 cur state else (\<lambda>_. True)) and ?Q17 cur state\<rbrace>
A total of 17 subgoals... proof (prove)
goal (19 subgoals):
 1. \<And>cur state state' ts ts' y rv' ya yb. \<lbrakk>thread_state_relation state state'; ts = ts'; \<not> Suc 0 < ts'; dc y rv'; dc ya yb\<rbrakk> \<Longrightarrow> corres dc (?R93 cur state state' ts ts' y rv' ya) (?R'93 cur state state' ts ts' y rv' yb) reschedule_required rescheduleRequired
 2. \<And>cur state state' ts ts' y rv'. \<lbrakk>thread_state_relation state state'; ts = ts'; \<not> Suc 0 < ts'; dc y rv'\<rbrakk> \<Longrightarrow> \<lbrace>?Q96 cur state state' ts ts' y\<rbrace> tcb_sched_action tcb_sched_append cur \<lbrace>?R93 cur state state' ts ts' y rv'\<rbrace>
 3. \<And>cur state state' ts ts' y rv'. \<lbrakk>thread_state_relation state state'; ts = ts'; \<not> Suc 0 < ts'; dc y rv'\<rbrakk> \<Longrightarrow> \<lbrace>?Q'98 cur state state' ts ts' rv'\<rbrace> tcbSchedAppend cur \<lbrace>?R'93 cur state state' ts ts' y rv'\<rbrace>
 4. \<And>cur state state' ts ts'. \<lbrakk>thread_state_relation state state'; ts = ts'; \<not> Suc 0 < ts'\<rbrakk> \<Longrightarrow> \<lbrace>?Q60 cur state state' ts'\<rbrace> ethread_set (tcb_time_slice_update (\<lambda>_. timeSlice)) cur \<lbrace>\<lambda>y. is_etcb_at cur and ?Q96 cur state state' ts ts' y\<rbrace>
 5. \<And>cur state state' ts ts'. \<lbrakk>thread_state_relation state state'; ts = ts'; \<not> Suc 0 < ts'\<rbrakk> \<Longrightarrow> \<lbrace>?Q'62 cur state state' ts'\<rbrace> threadSet (tcbTimeSlice_update (\<lambda>_. timeSlice)) cur \<lbrace>\<lambda>rv'. tcb_at' cur and Invariants_H.valid_queues and valid_queues' and ?Q'98 cur state state' ts ts' rv'\<rbrace>
 6. \<And>cur state state'. thread_state_relation state state' \<Longrightarrow> \<lbrace>?Q39 cur state\<rbrace> ethread_get tcb_time_slice cur \<lbrace>\<lambda>ts. tcb_at cur and valid_etcbs and (tcb_at cur and valid_etcbs and ?Q60 cur state state' ts)\<rbrace>
 7. \<And>cur state state'. thread_state_relation state state' \<Longrightarrow> \<lbrace>?Q'41 cur state'\<rbrace> threadGet tcbTimeSlice cur \<lbrace>\<lambda>ts'. tcb_at' cur and (tcb_at' cur and ?Q'62 cur state state' ts')\<rbrace>
 8. \<And>cur state state'. thread_state_relation state state' \<Longrightarrow> corres dc (\<lambda>_. True) (\<lambda>_. True) (return ()) (return ())
 9. \<And>cur state state' y ya. \<lbrakk>thread_state_relation state state'; dc y ya\<rbrakk> \<Longrightarrow> corres dc (?R15 cur state state' y) (?R'15 cur state state' ya) (when (Suc 0 < numDomains) (do y <- dec_domain_time;
dom_time <- gets domain_time;
when (dom_time = 0) reschedule_required
od)) (when (Suc 0 < numDomains) (do y <- decDomainTime;
domainTime <- getDomainTime;
when (domainTime = 0) rescheduleRequired
od))
 10. \<And>cur state state'. thread_state_relation state state' \<Longrightarrow> \<lbrace>?Q17 cur state\<rbrace> if state = Structures_A.thread_state.Running then do ts <- ethread_get tcb_time_slice cur;
let ts' = ts - 1 in if 0 < ts' then ethread_set (tcb_time_slice_update (\<lambda>_. ts')) cur else do ethread_set (tcb_time_slice_update (\<lambda>_. timeSlice)) cur;
tcb_sched_action tcb_sched_append cur;
reschedule_required
od
od else return () \<lbrace>?R15 cur state state'\<rbrace>
A total of 19 subgoals... proof (prove)
goal (18 subgoals):
 1. \<And>cur state state' ts ts' y rv'. \<lbrakk>thread_state_relation state state'; ts = ts'; \<not> Suc 0 < ts'; dc y rv'\<rbrakk> \<Longrightarrow> \<lbrace>?Q96 cur state state' ts ts' y\<rbrace> tcb_sched_action tcb_sched_append cur \<lbrace>\<lambda>ya. weak_valid_sched_action and valid_etcbs\<rbrace>
 2. \<And>cur state state' ts ts' y rv'. \<lbrakk>thread_state_relation state state'; ts = ts'; \<not> Suc 0 < ts'; dc y rv'\<rbrakk> \<Longrightarrow> \<lbrace>?Q'98 cur state state' ts ts' rv'\<rbrace> tcbSchedAppend cur \<lbrace>\<lambda>yb. Invariants_H.valid_queues and valid_queues' and (\<lambda>s. weak_sch_act_wf (ksSchedulerAction s) s)\<rbrace>
 3. \<And>cur state state' ts ts'. \<lbrakk>thread_state_relation state state'; ts = ts'; \<not> Suc 0 < ts'\<rbrakk> \<Longrightarrow> \<lbrace>?Q60 cur state state' ts'\<rbrace> ethread_set (tcb_time_slice_update (\<lambda>_. timeSlice)) cur \<lbrace>\<lambda>y. is_etcb_at cur and ?Q96 cur state state' ts ts' y\<rbrace>
 4. \<And>cur state state' ts ts'. \<lbrakk>thread_state_relation state state'; ts = ts'; \<not> Suc 0 < ts'\<rbrakk> \<Longrightarrow> \<lbrace>?Q'62 cur state state' ts'\<rbrace> threadSet (tcbTimeSlice_update (\<lambda>_. timeSlice)) cur \<lbrace>\<lambda>rv'. tcb_at' cur and Invariants_H.valid_queues and valid_queues' and ?Q'98 cur state state' ts ts' rv'\<rbrace>
 5. \<And>cur state state'. thread_state_relation state state' \<Longrightarrow> \<lbrace>?Q39 cur state\<rbrace> ethread_get tcb_time_slice cur \<lbrace>\<lambda>ts. tcb_at cur and valid_etcbs and (tcb_at cur and valid_etcbs and ?Q60 cur state state' ts)\<rbrace>
 6. \<And>cur state state'. thread_state_relation state state' \<Longrightarrow> \<lbrace>?Q'41 cur state'\<rbrace> threadGet tcbTimeSlice cur \<lbrace>\<lambda>ts'. tcb_at' cur and (tcb_at' cur and ?Q'62 cur state state' ts')\<rbrace>
 7. \<And>cur state state'. thread_state_relation state state' \<Longrightarrow> corres dc (\<lambda>_. True) (\<lambda>_. True) (return ()) (return ())
 8. \<And>cur state state' y ya. \<lbrakk>thread_state_relation state state'; dc y ya\<rbrakk> \<Longrightarrow> corres dc (?R15 cur state state' y) (?R'15 cur state state' ya) (when (Suc 0 < numDomains) (do y <- dec_domain_time;
dom_time <- gets domain_time;
when (dom_time = 0) reschedule_required
od)) (when (Suc 0 < numDomains) (do y <- decDomainTime;
domainTime <- getDomainTime;
when (domainTime = 0) rescheduleRequired
od))
 9. \<And>cur state state'. thread_state_relation state state' \<Longrightarrow> \<lbrace>?Q17 cur state\<rbrace> if state = Structures_A.thread_state.Running then do ts <- ethread_get tcb_time_slice cur;
let ts' = ts - 1 in if 0 < ts' then ethread_set (tcb_time_slice_update (\<lambda>_. ts')) cur else do ethread_set (tcb_time_slice_update (\<lambda>_. timeSlice)) cur;
tcb_sched_action tcb_sched_append cur;
reschedule_required
od
od else return () \<lbrace>?R15 cur state state'\<rbrace>
 10. \<And>cur state state'. thread_state_relation state state' \<Longrightarrow> \<lbrace>?Q'19 cur state'\<rbrace> if state' = Structures_H.thread_state.Running then do ts <- threadGet tcbTimeSlice cur;
ts' <- return (ts - 1);
if 0 < ts' then threadSet (tcbTimeSlice_update (\<lambda>_. ts')) cur else do threadSet (tcbTimeSlice_update (\<lambda>_. timeSlice)) cur;
tcbSchedAppend cur;
rescheduleRequired
od
od else return () \<lbrace>?R'15 cur state state'\<rbrace>
A total of 18 subgoals... proof (prove)
goal (17 subgoals):
 1. \<And>cur state state' ts ts' y rv'. \<lbrakk>thread_state_relation state state'; ts = ts'; \<not> Suc 0 < ts'; dc y rv'\<rbrakk> \<Longrightarrow> \<lbrace>?Q'98 cur state state' ts ts' rv'\<rbrace> tcbSchedAppend cur \<lbrace>\<lambda>yb. Invariants_H.valid_queues and valid_queues' and (\<lambda>s. weak_sch_act_wf (ksSchedulerAction s) s)\<rbrace>
 2. \<And>cur state state' ts ts'. \<lbrakk>thread_state_relation state state'; ts = ts'; \<not> Suc 0 < ts'\<rbrakk> \<Longrightarrow> \<lbrace>?Q60 cur state state' ts'\<rbrace> ethread_set (tcb_time_slice_update (\<lambda>_. timeSlice)) cur \<lbrace>\<lambda>y. is_etcb_at cur and (\<lambda>s. weak_valid_sched_action s \<and> valid_etcbs s)\<rbrace>
 3. \<And>cur state state' ts ts'. \<lbrakk>thread_state_relation state state'; ts = ts'; \<not> Suc 0 < ts'\<rbrakk> \<Longrightarrow> \<lbrace>?Q'62 cur state state' ts'\<rbrace> threadSet (tcbTimeSlice_update (\<lambda>_. timeSlice)) cur \<lbrace>\<lambda>rv'. tcb_at' cur and Invariants_H.valid_queues and valid_queues' and ?Q'98 cur state state' ts ts' rv'\<rbrace>
 4. \<And>cur state state'. thread_state_relation state state' \<Longrightarrow> \<lbrace>?Q39 cur state\<rbrace> ethread_get tcb_time_slice cur \<lbrace>\<lambda>ts. tcb_at cur and valid_etcbs and (tcb_at cur and valid_etcbs and ?Q60 cur state state' ts)\<rbrace>
 5. \<And>cur state state'. thread_state_relation state state' \<Longrightarrow> \<lbrace>?Q'41 cur state'\<rbrace> threadGet tcbTimeSlice cur \<lbrace>\<lambda>ts'. tcb_at' cur and (tcb_at' cur and ?Q'62 cur state state' ts')\<rbrace>
 6. \<And>cur state state'. thread_state_relation state state' \<Longrightarrow> corres dc (\<lambda>_. True) (\<lambda>_. True) (return ()) (return ())
 7. \<And>cur state state' y ya. \<lbrakk>thread_state_relation state state'; dc y ya\<rbrakk> \<Longrightarrow> corres dc (?R15 cur state state' y) (?R'15 cur state state' ya) (when (Suc 0 < numDomains) (do y <- dec_domain_time;
dom_time <- gets domain_time;
when (dom_time = 0) reschedule_required
od)) (when (Suc 0 < numDomains) (do y <- decDomainTime;
domainTime <- getDomainTime;
when (domainTime = 0) rescheduleRequired
od))
 8. \<And>cur state state'. thread_state_relation state state' \<Longrightarrow> \<lbrace>?Q17 cur state\<rbrace> if state = Structures_A.thread_state.Running then do ts <- ethread_get tcb_time_slice cur;
let ts' = ts - 1 in if 0 < ts' then ethread_set (tcb_time_slice_update (\<lambda>_. ts')) cur else do ethread_set (tcb_time_slice_update (\<lambda>_. timeSlice)) cur;
tcb_sched_action tcb_sched_append cur;
reschedule_required
od
od else return () \<lbrace>?R15 cur state state'\<rbrace>
 9. \<And>cur state state'. thread_state_relation state state' \<Longrightarrow> \<lbrace>?Q'19 cur state'\<rbrace> if state' = Structures_H.thread_state.Running then do ts <- threadGet tcbTimeSlice cur;
ts' <- return (ts - 1);
if 0 < ts' then threadSet (tcbTimeSlice_update (\<lambda>_. ts')) cur else do threadSet (tcbTimeSlice_update (\<lambda>_. timeSlice)) cur;
tcbSchedAppend cur;
rescheduleRequired
od
od else return () \<lbrace>?R'15 cur state state'\<rbrace>
 10. \<And>cur. \<lbrace>?Q10 cur\<rbrace> get_thread_state cur \<lbrace>\<lambda>state. (if state = Structures_A.thread_state.Running then is_etcb_at cur and ?Q39 cur state else (\<lambda>_. True)) and ?Q17 cur state\<rbrace>
A total of 17 subgoals... proof (prove)
goal (18 subgoals):
 1. \<And>cur state state' ts ts' y rv'. \<lbrakk>thread_state_relation state state'; ts = ts'; \<not> Suc 0 < ts'; dc y rv'\<rbrakk> \<Longrightarrow> \<lbrace>?Q'98 cur state state' ts ts' rv'\<rbrace> tcbSchedAppend cur \<lbrace>?Q110 cur state state' ts ts' y rv'\<rbrace>
 2. \<And>cur state state' ts ts' y rv' rv s. \<lbrakk>thread_state_relation state state'; ts = ts'; \<not> Suc 0 < ts'; dc y rv'; ?Q110 cur state state' ts ts' y rv' rv s\<rbrakk> \<Longrightarrow> (Invariants_H.valid_queues and valid_queues' and (\<lambda>s. weak_sch_act_wf (ksSchedulerAction s) s)) s
 3. \<And>cur state state' ts ts'. \<lbrakk>thread_state_relation state state'; ts = ts'; \<not> Suc 0 < ts'\<rbrakk> \<Longrightarrow> \<lbrace>?Q60 cur state state' ts'\<rbrace> ethread_set (tcb_time_slice_update (\<lambda>_. timeSlice)) cur \<lbrace>\<lambda>y. is_etcb_at cur and (\<lambda>s. weak_valid_sched_action s \<and> valid_etcbs s)\<rbrace>
 4. \<And>cur state state' ts ts'. \<lbrakk>thread_state_relation state state'; ts = ts'; \<not> Suc 0 < ts'\<rbrakk> \<Longrightarrow> \<lbrace>?Q'62 cur state state' ts'\<rbrace> threadSet (tcbTimeSlice_update (\<lambda>_. timeSlice)) cur \<lbrace>\<lambda>rv'. tcb_at' cur and Invariants_H.valid_queues and valid_queues' and ?Q'98 cur state state' ts ts' rv'\<rbrace>
 5. \<And>cur state state'. thread_state_relation state state' \<Longrightarrow> \<lbrace>?Q39 cur state\<rbrace> ethread_get tcb_time_slice cur \<lbrace>\<lambda>ts. tcb_at cur and valid_etcbs and (tcb_at cur and valid_etcbs and ?Q60 cur state state' ts)\<rbrace>
 6. \<And>cur state state'. thread_state_relation state state' \<Longrightarrow> \<lbrace>?Q'41 cur state'\<rbrace> threadGet tcbTimeSlice cur \<lbrace>\<lambda>ts'. tcb_at' cur and (tcb_at' cur and ?Q'62 cur state state' ts')\<rbrace>
 7. \<And>cur state state'. thread_state_relation state state' \<Longrightarrow> corres dc (\<lambda>_. True) (\<lambda>_. True) (return ()) (return ())
 8. \<And>cur state state' y ya. \<lbrakk>thread_state_relation state state'; dc y ya\<rbrakk> \<Longrightarrow> corres dc (?R15 cur state state' y) (?R'15 cur state state' ya) (when (Suc 0 < numDomains) (do y <- dec_domain_time;
dom_time <- gets domain_time;
when (dom_time = 0) reschedule_required
od)) (when (Suc 0 < numDomains) (do y <- decDomainTime;
domainTime <- getDomainTime;
when (domainTime = 0) rescheduleRequired
od))
 9. \<And>cur state state'. thread_state_relation state state' \<Longrightarrow> \<lbrace>?Q17 cur state\<rbrace> if state = Structures_A.thread_state.Running then do ts <- ethread_get tcb_time_slice cur;
let ts' = ts - 1 in if 0 < ts' then ethread_set (tcb_time_slice_update (\<lambda>_. ts')) cur else do ethread_set (tcb_time_slice_update (\<lambda>_. timeSlice)) cur;
tcb_sched_action tcb_sched_append cur;
reschedule_required
od
od else return () \<lbrace>?R15 cur state state'\<rbrace>
 10. \<And>cur state state'. thread_state_relation state state' \<Longrightarrow> \<lbrace>?Q'19 cur state'\<rbrace> if state' = Structures_H.thread_state.Running then do ts <- threadGet tcbTimeSlice cur;
ts' <- return (ts - 1);
if 0 < ts' then threadSet (tcbTimeSlice_update (\<lambda>_. ts')) cur else do threadSet (tcbTimeSlice_update (\<lambda>_. timeSlice)) cur;
tcbSchedAppend cur;
rescheduleRequired
od
od else return () \<lbrace>?R'15 cur state state'\<rbrace>
A total of 18 subgoals... proof (prove)
goal (16 subgoals):
 1. \<And>cur state state' ts ts'. \<lbrakk>thread_state_relation state state'; ts = ts'; \<not> Suc 0 < ts'\<rbrakk> \<Longrightarrow> \<lbrace>?Q60 cur state state' ts'\<rbrace> ethread_set (tcb_time_slice_update (\<lambda>_. timeSlice)) cur \<lbrace>\<lambda>y. is_etcb_at cur and (\<lambda>s. weak_valid_sched_action s \<and> valid_etcbs s)\<rbrace>
 2. \<And>cur state state' ts ts'. \<lbrakk>thread_state_relation state state'; ts = ts'; \<not> Suc 0 < ts'\<rbrakk> \<Longrightarrow> \<lbrace>?Q'62 cur state state' ts'\<rbrace> threadSet (tcbTimeSlice_update (\<lambda>_. timeSlice)) cur \<lbrace>\<lambda>rv'. tcb_at' cur and Invariants_H.valid_queues and valid_queues' and (invs' and st_tcb_at' runnable' cur)\<rbrace>
 3. \<And>cur state state'. thread_state_relation state state' \<Longrightarrow> \<lbrace>?Q39 cur state\<rbrace> ethread_get tcb_time_slice cur \<lbrace>\<lambda>ts. tcb_at cur and valid_etcbs and (tcb_at cur and valid_etcbs and ?Q60 cur state state' ts)\<rbrace>
 4. \<And>cur state state'. thread_state_relation state state' \<Longrightarrow> \<lbrace>?Q'41 cur state'\<rbrace> threadGet tcbTimeSlice cur \<lbrace>\<lambda>ts'. tcb_at' cur and (tcb_at' cur and ?Q'62 cur state state' ts')\<rbrace>
 5. \<And>cur state state'. thread_state_relation state state' \<Longrightarrow> corres dc (\<lambda>_. True) (\<lambda>_. True) (return ()) (return ())
 6. \<And>cur state state' y ya. \<lbrakk>thread_state_relation state state'; dc y ya\<rbrakk> \<Longrightarrow> corres dc (?R15 cur state state' y) (?R'15 cur state state' ya) (when (Suc 0 < numDomains) (do y <- dec_domain_time;
dom_time <- gets domain_time;
when (dom_time = 0) reschedule_required
od)) (when (Suc 0 < numDomains) (do y <- decDomainTime;
domainTime <- getDomainTime;
when (domainTime = 0) rescheduleRequired
od))
 7. \<And>cur state state'. thread_state_relation state state' \<Longrightarrow> \<lbrace>?Q17 cur state\<rbrace> if state = Structures_A.thread_state.Running then do ts <- ethread_get tcb_time_slice cur;
let ts' = ts - 1 in if 0 < ts' then ethread_set (tcb_time_slice_update (\<lambda>_. ts')) cur else do ethread_set (tcb_time_slice_update (\<lambda>_. timeSlice)) cur;
tcb_sched_action tcb_sched_append cur;
reschedule_required
od
od else return () \<lbrace>?R15 cur state state'\<rbrace>
 8. \<And>cur state state'. thread_state_relation state state' \<Longrightarrow> \<lbrace>?Q'19 cur state'\<rbrace> if state' = Structures_H.thread_state.Running then do ts <- threadGet tcbTimeSlice cur;
ts' <- return (ts - 1);
if 0 < ts' then threadSet (tcbTimeSlice_update (\<lambda>_. ts')) cur else do threadSet (tcbTimeSlice_update (\<lambda>_. timeSlice)) cur;
tcbSchedAppend cur;
rescheduleRequired
od
od else return () \<lbrace>?R'15 cur state state'\<rbrace>
 9. \<And>cur. \<lbrace>?Q10 cur\<rbrace> get_thread_state cur \<lbrace>\<lambda>state. (if state = Structures_A.thread_state.Running then is_etcb_at cur and ?Q39 cur state else (\<lambda>_. True)) and ?Q17 cur state\<rbrace>
 10. \<And>cur. \<lbrace>?Q'10 cur\<rbrace> getThreadState cur \<lbrace>\<lambda>state'. (if state' = Structures_H.thread_state.Running then tcb_at' cur and ?Q'41 cur state' else (\<lambda>_. True)) and ?Q'19 cur state'\<rbrace>
A total of 16 subgoals... proof (prove)
goal (12 subgoals):
 1. \<And>cur state state'. thread_state_relation state state' \<Longrightarrow> corres dc (\<lambda>_. True) (\<lambda>_. True) (return ()) (return ())
 2. \<And>cur state state' y ya. \<lbrakk>thread_state_relation state state'; dc y ya\<rbrakk> \<Longrightarrow> corres dc (?R15 cur state state' y) (?R'15 cur state state' ya) (when (Suc 0 < numDomains) (do y <- dec_domain_time;
dom_time <- gets domain_time;
when (dom_time = 0) reschedule_required
od)) (when (Suc 0 < numDomains) (do y <- decDomainTime;
domainTime <- getDomainTime;
when (domainTime = 0) rescheduleRequired
od))
 3. \<And>cur state state'. thread_state_relation state state' \<Longrightarrow> \<lbrace>?Q17 cur state\<rbrace> if state = Structures_A.thread_state.Running then do ts <- ethread_get tcb_time_slice cur;
let ts' = ts - 1 in if 0 < ts' then ethread_set (tcb_time_slice_update (\<lambda>_. ts')) cur else do ethread_set (tcb_time_slice_update (\<lambda>_. timeSlice)) cur;
tcb_sched_action tcb_sched_append cur;
reschedule_required
od
od else return () \<lbrace>?R15 cur state state'\<rbrace>
 4. \<And>cur state state'. thread_state_relation state state' \<Longrightarrow> \<lbrace>?Q'19 cur state'\<rbrace> if state' = Structures_H.thread_state.Running then do ts <- threadGet tcbTimeSlice cur;
ts' <- return (ts - 1);
if 0 < ts' then threadSet (tcbTimeSlice_update (\<lambda>_. ts')) cur else do threadSet (tcbTimeSlice_update (\<lambda>_. timeSlice)) cur;
tcbSchedAppend cur;
rescheduleRequired
od
od else return () \<lbrace>?R'15 cur state state'\<rbrace>
 5. \<And>cur. \<lbrace>?Q10 cur\<rbrace> get_thread_state cur \<lbrace>\<lambda>state. (if state = Structures_A.thread_state.Running then is_etcb_at cur and (\<lambda>a. etcb_at (\<lambda>t. (tcb_at cur and valid_etcbs and (tcb_at cur and valid_etcbs and (\<lambda>s. is_etcb_at cur s \<and> weak_valid_sched_action s \<and> valid_etcbs s))) a) cur a) else (\<lambda>_. True)) and ?Q17 cur state\<rbrace>
 6. \<And>cur. \<lbrace>?Q'10 cur\<rbrace> getThreadState cur \<lbrace>\<lambda>state'. (if state' = Structures_H.thread_state.Running then tcb_at' cur and (tcb_at' cur and (tcb_at' cur and (\<lambda>s. obj_at' (\<lambda>obj. if cur = cur then True else True) cur s \<and> (Invariants_H.valid_queues and (\<lambda>s. \<forall>d p. (\<exists>tcb. (inQ d p tcb \<and> runnable' (tcbState tcb)) \<and> \<not> (inQ d p (tcbTimeSlice_update (\<lambda>_. timeSlice) tcb) \<and> runnable' (tcbState (tcbTimeSlice_update (\<lambda>_. timeSlice) tcb)))) \<longrightarrow> obj_at' (\<lambda>tcb. (inQ d p tcb \<and> runnable' (tcbState tcb)) \<and> \<not> (inQ d p (tcbTimeSlice_update (\<lambda>_. timeSlice) tcb) \<and> runnable' (tcbState (tcbTimeSlice_update (\<lambda>_. timeSlice) tcb)))) cur s \<longrightarrow> cur \<notin> set (ksReadyQueues s (d, p)))) s \<and> ((\<forall>ko qdom prio. ko_at' ko cur s \<and> inQ qdom prio (tcbTimeSlice_update (\<lambda>_. timeSlice) ko) \<and> \<not> inQ qdom prio ko \<longrightarrow> cur \<in> set (ksReadyQueues s (qdom, prio))) \<and> valid_queues' s) \<and> (invs' and tcb_at' cur) s \<and> (tcb_at' cur s \<longrightarrow> (if cur = cur then obj_at' (\<lambda>tcb. runnable' (itcbState (tcb_to_itcb' (tcbTimeSlice_update (\<lambda>_. timeSlice) tcb)))) cur s else st_tcb_at' runnable' cur s))))) else (\<lambda>_. True)) and ?Q'19 cur state'\<rbrace>
 7. \<lbrace>?Q6\<rbrace> gets cur_thread \<lbrace>\<lambda>cur. tcb_at cur and ?Q10 cur\<rbrace>
 8. \<lbrace>?Q'6\<rbrace> getCurThread \<lbrace>\<lambda>cur. tcb_at' cur and ?Q'10 cur\<rbrace>
 9. \<And>s. ((\<lambda>_. True) and (cur_tcb and valid_sched)) s \<Longrightarrow> ((\<lambda>_. True) and ?Q6) s
 10. \<And>s. ((\<lambda>_. True) and invs') s \<Longrightarrow> ((\<lambda>_. True) and ?Q'6) s
A total of 12 subgoals... proof (prove)
goal (11 subgoals):
 1. \<And>cur state state' y ya. \<lbrakk>thread_state_relation state state'; dc y ya\<rbrakk> \<Longrightarrow> corres dc (?R15 cur state state' y) (?R'15 cur state state' ya) (when (Suc 0 < numDomains) (do y <- dec_domain_time;
dom_time <- gets domain_time;
when (dom_time = 0) reschedule_required
od)) (when (Suc 0 < numDomains) (do y <- decDomainTime;
domainTime <- getDomainTime;
when (domainTime = 0) rescheduleRequired
od))
 2. \<And>cur state state'. thread_state_relation state state' \<Longrightarrow> \<lbrace>?Q17 cur state\<rbrace> if state = Structures_A.thread_state.Running then do ts <- ethread_get tcb_time_slice cur;
let ts' = ts - 1 in if 0 < ts' then ethread_set (tcb_time_slice_update (\<lambda>_. ts')) cur else do ethread_set (tcb_time_slice_update (\<lambda>_. timeSlice)) cur;
tcb_sched_action tcb_sched_append cur;
reschedule_required
od
od else return () \<lbrace>?R15 cur state state'\<rbrace>
 3. \<And>cur state state'. thread_state_relation state state' \<Longrightarrow> \<lbrace>?Q'19 cur state'\<rbrace> if state' = Structures_H.thread_state.Running then do ts <- threadGet tcbTimeSlice cur;
ts' <- return (ts - 1);
if 0 < ts' then threadSet (tcbTimeSlice_update (\<lambda>_. ts')) cur else do threadSet (tcbTimeSlice_update (\<lambda>_. timeSlice)) cur;
tcbSchedAppend cur;
rescheduleRequired
od
od else return () \<lbrace>?R'15 cur state state'\<rbrace>
 4. \<And>cur. \<lbrace>?Q10 cur\<rbrace> get_thread_state cur \<lbrace>\<lambda>state. (if state = Structures_A.thread_state.Running then is_etcb_at cur and (\<lambda>a. etcb_at (\<lambda>t. (tcb_at cur and valid_etcbs and (tcb_at cur and valid_etcbs and (\<lambda>s. is_etcb_at cur s \<and> weak_valid_sched_action s \<and> valid_etcbs s))) a) cur a) else (\<lambda>_. True)) and ?Q17 cur state\<rbrace>
 5. \<And>cur. \<lbrace>?Q'10 cur\<rbrace> getThreadState cur \<lbrace>\<lambda>state'. (if state' = Structures_H.thread_state.Running then tcb_at' cur and (tcb_at' cur and (tcb_at' cur and (\<lambda>s. obj_at' (\<lambda>obj. if cur = cur then True else True) cur s \<and> (Invariants_H.valid_queues and (\<lambda>s. \<forall>d p. (\<exists>tcb. (inQ d p tcb \<and> runnable' (tcbState tcb)) \<and> \<not> (inQ d p (tcbTimeSlice_update (\<lambda>_. timeSlice) tcb) \<and> runnable' (tcbState (tcbTimeSlice_update (\<lambda>_. timeSlice) tcb)))) \<longrightarrow> obj_at' (\<lambda>tcb. (inQ d p tcb \<and> runnable' (tcbState tcb)) \<and> \<not> (inQ d p (tcbTimeSlice_update (\<lambda>_. timeSlice) tcb) \<and> runnable' (tcbState (tcbTimeSlice_update (\<lambda>_. timeSlice) tcb)))) cur s \<longrightarrow> cur \<notin> set (ksReadyQueues s (d, p)))) s \<and> ((\<forall>ko qdom prio. ko_at' ko cur s \<and> inQ qdom prio (tcbTimeSlice_update (\<lambda>_. timeSlice) ko) \<and> \<not> inQ qdom prio ko \<longrightarrow> cur \<in> set (ksReadyQueues s (qdom, prio))) \<and> valid_queues' s) \<and> (invs' and tcb_at' cur) s \<and> (tcb_at' cur s \<longrightarrow> (if cur = cur then obj_at' (\<lambda>tcb. runnable' (itcbState (tcb_to_itcb' (tcbTimeSlice_update (\<lambda>_. timeSlice) tcb)))) cur s else st_tcb_at' runnable' cur s))))) else (\<lambda>_. True)) and ?Q'19 cur state'\<rbrace>
 6. \<lbrace>?Q6\<rbrace> gets cur_thread \<lbrace>\<lambda>cur. tcb_at cur and ?Q10 cur\<rbrace>
 7. \<lbrace>?Q'6\<rbrace> getCurThread \<lbrace>\<lambda>cur. tcb_at' cur and ?Q'10 cur\<rbrace>
 8. \<And>s. ((\<lambda>_. True) and (cur_tcb and valid_sched)) s \<Longrightarrow> ((\<lambda>_. True) and ?Q6) s
 9. \<And>s. ((\<lambda>_. True) and invs') s \<Longrightarrow> ((\<lambda>_. True) and ?Q'6) s
 10. \<And>s. (cur_tcb and valid_sched) s \<Longrightarrow> ((\<lambda>_. True) and (cur_tcb and valid_sched)) s
A total of 11 subgoals... proof (prove)
goal (11 subgoals):
 1. \<And>cur state state'. thread_state_relation state state' \<Longrightarrow> corres dc (?R15 cur state state' ()) (?R'15 cur state state' ()) (when (Suc 0 < numDomains) (do y <- dec_domain_time;
dom_time <- gets domain_time;
when (dom_time = 0) reschedule_required
od)) (when (Suc 0 < numDomains) (do y <- decDomainTime;
domainTime <- getDomainTime;
when (domainTime = 0) rescheduleRequired
od))
 2. \<And>cur state state'. thread_state_relation state state' \<Longrightarrow> \<lbrace>?Q17 cur state\<rbrace> if state = Structures_A.thread_state.Running then do ts <- ethread_get tcb_time_slice cur;
let ts' = ts - 1 in if 0 < ts' then ethread_set (tcb_time_slice_update (\<lambda>_. ts')) cur else do ethread_set (tcb_time_slice_update (\<lambda>_. timeSlice)) cur;
tcb_sched_action tcb_sched_append cur;
reschedule_required
od
od else return () \<lbrace>?R15 cur state state'\<rbrace>
 3. \<And>cur state state'. thread_state_relation state state' \<Longrightarrow> \<lbrace>?Q'19 cur state'\<rbrace> if state' = Structures_H.thread_state.Running then do ts <- threadGet tcbTimeSlice cur;
ts' <- return (ts - 1);
if 0 < ts' then threadSet (tcbTimeSlice_update (\<lambda>_. ts')) cur else do threadSet (tcbTimeSlice_update (\<lambda>_. timeSlice)) cur;
tcbSchedAppend cur;
rescheduleRequired
od
od else return () \<lbrace>?R'15 cur state state'\<rbrace>
 4. \<And>cur. \<lbrace>?Q10 cur\<rbrace> get_thread_state cur \<lbrace>\<lambda>state. (if state = Structures_A.thread_state.Running then is_etcb_at cur and (\<lambda>a. etcb_at (\<lambda>t. (tcb_at cur and valid_etcbs and (tcb_at cur and valid_etcbs and (\<lambda>s. is_etcb_at cur s \<and> weak_valid_sched_action s \<and> valid_etcbs s))) a) cur a) else (\<lambda>_. True)) and ?Q17 cur state\<rbrace>
 5. \<And>cur. \<lbrace>?Q'10 cur\<rbrace> getThreadState cur \<lbrace>\<lambda>state'. (if state' = Structures_H.thread_state.Running then tcb_at' cur and (tcb_at' cur and (tcb_at' cur and (\<lambda>s. obj_at' (\<lambda>obj. if cur = cur then True else True) cur s \<and> (Invariants_H.valid_queues and (\<lambda>s. \<forall>d p. (\<exists>tcb. (inQ d p tcb \<and> runnable' (tcbState tcb)) \<and> \<not> (inQ d p (tcbTimeSlice_update (\<lambda>_. timeSlice) tcb) \<and> runnable' (tcbState (tcbTimeSlice_update (\<lambda>_. timeSlice) tcb)))) \<longrightarrow> obj_at' (\<lambda>tcb. (inQ d p tcb \<and> runnable' (tcbState tcb)) \<and> \<not> (inQ d p (tcbTimeSlice_update (\<lambda>_. timeSlice) tcb) \<and> runnable' (tcbState (tcbTimeSlice_update (\<lambda>_. timeSlice) tcb)))) cur s \<longrightarrow> cur \<notin> set (ksReadyQueues s (d, p)))) s \<and> ((\<forall>ko qdom prio. ko_at' ko cur s \<and> inQ qdom prio (tcbTimeSlice_update (\<lambda>_. timeSlice) ko) \<and> \<not> inQ qdom prio ko \<longrightarrow> cur \<in> set (ksReadyQueues s (qdom, prio))) \<and> valid_queues' s) \<and> (invs' and tcb_at' cur) s \<and> (tcb_at' cur s \<longrightarrow> (if cur = cur then obj_at' (\<lambda>tcb. runnable' (itcbState (tcb_to_itcb' (tcbTimeSlice_update (\<lambda>_. timeSlice) tcb)))) cur s else st_tcb_at' runnable' cur s))))) else (\<lambda>_. True)) and ?Q'19 cur state'\<rbrace>
 6. \<lbrace>?Q6\<rbrace> gets cur_thread \<lbrace>\<lambda>cur. tcb_at cur and ?Q10 cur\<rbrace>
 7. \<lbrace>?Q'6\<rbrace> getCurThread \<lbrace>\<lambda>cur. tcb_at' cur and ?Q'10 cur\<rbrace>
 8. \<And>s. ((\<lambda>_. True) and (cur_tcb and valid_sched)) s \<Longrightarrow> ((\<lambda>_. True) and ?Q6) s
 9. \<And>s. ((\<lambda>_. True) and invs') s \<Longrightarrow> ((\<lambda>_. True) and ?Q'6) s
 10. \<And>s. (cur_tcb and valid_sched) s \<Longrightarrow> ((\<lambda>_. True) and (cur_tcb and valid_sched)) s
A total of 11 subgoals... proof (prove)
goal (11 subgoals):
 1. \<And>cur state state'. thread_state_relation state state' \<Longrightarrow> corres dc (?P169 cur state state' ()) (?P'168 cur state state' ()) (do y <- dec_domain_time;
dom_time <- gets domain_time;
when (dom_time = 0) reschedule_required
od) (do y <- decDomainTime;
domainTime <- getDomainTime;
when (domainTime = 0) rescheduleRequired
od)
 2. \<And>cur state state'. thread_state_relation state state' \<Longrightarrow> \<lbrace>?Q17 cur state\<rbrace> if state = Structures_A.thread_state.Running then do ts <- ethread_get tcb_time_slice cur;
let ts' = ts - 1 in if 0 < ts' then ethread_set (tcb_time_slice_update (\<lambda>_. ts')) cur else do ethread_set (tcb_time_slice_update (\<lambda>_. timeSlice)) cur;
tcb_sched_action tcb_sched_append cur;
reschedule_required
od
od else return () \<lbrace>\<lambda>a b. Suc 0 < numDomains \<longrightarrow> ?P169 cur state state' a b\<rbrace>
 3. \<And>cur state state'. thread_state_relation state state' \<Longrightarrow> \<lbrace>?Q'19 cur state'\<rbrace> if state' = Structures_H.thread_state.Running then do ts <- threadGet tcbTimeSlice cur;
ts' <- return (ts - 1);
if 0 < ts' then threadSet (tcbTimeSlice_update (\<lambda>_. ts')) cur else do threadSet (tcbTimeSlice_update (\<lambda>_. timeSlice)) cur;
tcbSchedAppend cur;
rescheduleRequired
od
od else return () \<lbrace>\<lambda>a b. Suc 0 < numDomains \<longrightarrow> ?P'168 cur state state' a b\<rbrace>
 4. \<And>cur. \<lbrace>?Q10 cur\<rbrace> get_thread_state cur \<lbrace>\<lambda>state. (if state = Structures_A.thread_state.Running then is_etcb_at cur and (\<lambda>a. etcb_at (\<lambda>t. (tcb_at cur and valid_etcbs and (tcb_at cur and valid_etcbs and (\<lambda>s. is_etcb_at cur s \<and> weak_valid_sched_action s \<and> valid_etcbs s))) a) cur a) else (\<lambda>_. True)) and ?Q17 cur state\<rbrace>
 5. \<And>cur. \<lbrace>?Q'10 cur\<rbrace> getThreadState cur \<lbrace>\<lambda>state'. (if state' = Structures_H.thread_state.Running then tcb_at' cur and (tcb_at' cur and (tcb_at' cur and (\<lambda>s. obj_at' (\<lambda>obj. if cur = cur then True else True) cur s \<and> (Invariants_H.valid_queues and (\<lambda>s. \<forall>d p. (\<exists>tcb. (inQ d p tcb \<and> runnable' (tcbState tcb)) \<and> \<not> (inQ d p (tcbTimeSlice_update (\<lambda>_. timeSlice) tcb) \<and> runnable' (tcbState (tcbTimeSlice_update (\<lambda>_. timeSlice) tcb)))) \<longrightarrow> obj_at' (\<lambda>tcb. (inQ d p tcb \<and> runnable' (tcbState tcb)) \<and> \<not> (inQ d p (tcbTimeSlice_update (\<lambda>_. timeSlice) tcb) \<and> runnable' (tcbState (tcbTimeSlice_update (\<lambda>_. timeSlice) tcb)))) cur s \<longrightarrow> cur \<notin> set (ksReadyQueues s (d, p)))) s \<and> ((\<forall>ko qdom prio. ko_at' ko cur s \<and> inQ qdom prio (tcbTimeSlice_update (\<lambda>_. timeSlice) ko) \<and> \<not> inQ qdom prio ko \<longrightarrow> cur \<in> set (ksReadyQueues s (qdom, prio))) \<and> valid_queues' s) \<and> (invs' and tcb_at' cur) s \<and> (tcb_at' cur s \<longrightarrow> (if cur = cur then obj_at' (\<lambda>tcb. runnable' (itcbState (tcb_to_itcb' (tcbTimeSlice_update (\<lambda>_. timeSlice) tcb)))) cur s else st_tcb_at' runnable' cur s))))) else (\<lambda>_. True)) and ?Q'19 cur state'\<rbrace>
 6. \<lbrace>?Q6\<rbrace> gets cur_thread \<lbrace>\<lambda>cur. tcb_at cur and ?Q10 cur\<rbrace>
 7. \<lbrace>?Q'6\<rbrace> getCurThread \<lbrace>\<lambda>cur. tcb_at' cur and ?Q'10 cur\<rbrace>
 8. \<And>s. ((\<lambda>_. True) and (cur_tcb and valid_sched)) s \<Longrightarrow> ((\<lambda>_. True) and ?Q6) s
 9. \<And>s. ((\<lambda>_. True) and invs') s \<Longrightarrow> ((\<lambda>_. True) and ?Q'6) s
 10. \<And>s. (cur_tcb and valid_sched) s \<Longrightarrow> ((\<lambda>_. True) and (cur_tcb and valid_sched)) s
A total of 11 subgoals... proof (prove)
goal (13 subgoals):
 1. \<And>cur state state' rv rv'. \<lbrakk>thread_state_relation state state'; dc rv rv'\<rbrakk> \<Longrightarrow> corres dc (?R172 cur state state' rv) (?R'172 cur state state' rv') (do dom_time <- gets domain_time;
when (dom_time = 0) reschedule_required
od) (do domainTime <- getDomainTime;
when (domainTime = 0) rescheduleRequired
od)
 2. \<And>cur state state'. thread_state_relation state state' \<Longrightarrow> \<lbrace>?Q176 cur state state' ()\<rbrace> dec_domain_time \<lbrace>?R172 cur state state'\<rbrace>
 3. \<And>cur state state'. thread_state_relation state state' \<Longrightarrow> \<lbrace>?Q'175 cur state state' ()\<rbrace> decDomainTime \<lbrace>?R'172 cur state state'\<rbrace>
 4. \<And>cur state state'. thread_state_relation state state' \<Longrightarrow> \<lbrace>?Q17 cur state\<rbrace> if state = Structures_A.thread_state.Running then do ts <- ethread_get tcb_time_slice cur;
let ts' = ts - 1 in if 0 < ts' then ethread_set (tcb_time_slice_update (\<lambda>_. ts')) cur else do ethread_set (tcb_time_slice_update (\<lambda>_. timeSlice)) cur;
tcb_sched_action tcb_sched_append cur;
reschedule_required
od
od else return () \<lbrace>\<lambda>a b. Suc 0 < numDomains \<longrightarrow> ((\<lambda>_. True) and ?Q176 cur state state' a) b\<rbrace>
 5. \<And>cur state state'. thread_state_relation state state' \<Longrightarrow> \<lbrace>?Q'19 cur state'\<rbrace> if state' = Structures_H.thread_state.Running then do ts <- threadGet tcbTimeSlice cur;
ts' <- return (ts - 1);
if 0 < ts' then threadSet (tcbTimeSlice_update (\<lambda>_. ts')) cur else do threadSet (tcbTimeSlice_update (\<lambda>_. timeSlice)) cur;
tcbSchedAppend cur;
rescheduleRequired
od
od else return () \<lbrace>\<lambda>a b. Suc 0 < numDomains \<longrightarrow> ((\<lambda>_. True) and ?Q'175 cur state state' a) b\<rbrace>
 6. \<And>cur. \<lbrace>?Q10 cur\<rbrace> get_thread_state cur \<lbrace>\<lambda>state. (if state = Structures_A.thread_state.Running then is_etcb_at cur and (\<lambda>a. etcb_at (\<lambda>t. (tcb_at cur and valid_etcbs and (tcb_at cur and valid_etcbs and (\<lambda>s. is_etcb_at cur s \<and> weak_valid_sched_action s \<and> valid_etcbs s))) a) cur a) else (\<lambda>_. True)) and ?Q17 cur state\<rbrace>
 7. \<And>cur. \<lbrace>?Q'10 cur\<rbrace> getThreadState cur \<lbrace>\<lambda>state'. (if state' = Structures_H.thread_state.Running then tcb_at' cur and (tcb_at' cur and (tcb_at' cur and (\<lambda>s. obj_at' (\<lambda>obj. if cur = cur then True else True) cur s \<and> (Invariants_H.valid_queues and (\<lambda>s. \<forall>d p. (\<exists>tcb. (inQ d p tcb \<and> runnable' (tcbState tcb)) \<and> \<not> (inQ d p (tcbTimeSlice_update (\<lambda>_. timeSlice) tcb) \<and> runnable' (tcbState (tcbTimeSlice_update (\<lambda>_. timeSlice) tcb)))) \<longrightarrow> obj_at' (\<lambda>tcb. (inQ d p tcb \<and> runnable' (tcbState tcb)) \<and> \<not> (inQ d p (tcbTimeSlice_update (\<lambda>_. timeSlice) tcb) \<and> runnable' (tcbState (tcbTimeSlice_update (\<lambda>_. timeSlice) tcb)))) cur s \<longrightarrow> cur \<notin> set (ksReadyQueues s (d, p)))) s \<and> ((\<forall>ko qdom prio. ko_at' ko cur s \<and> inQ qdom prio (tcbTimeSlice_update (\<lambda>_. timeSlice) ko) \<and> \<not> inQ qdom prio ko \<longrightarrow> cur \<in> set (ksReadyQueues s (qdom, prio))) \<and> valid_queues' s) \<and> (invs' and tcb_at' cur) s \<and> (tcb_at' cur s \<longrightarrow> (if cur = cur then obj_at' (\<lambda>tcb. runnable' (itcbState (tcb_to_itcb' (tcbTimeSlice_update (\<lambda>_. timeSlice) tcb)))) cur s else st_tcb_at' runnable' cur s))))) else (\<lambda>_. True)) and ?Q'19 cur state'\<rbrace>
 8. \<lbrace>?Q6\<rbrace> gets cur_thread \<lbrace>\<lambda>cur. tcb_at cur and ?Q10 cur\<rbrace>
 9. \<lbrace>?Q'6\<rbrace> getCurThread \<lbrace>\<lambda>cur. tcb_at' cur and ?Q'10 cur\<rbrace>
 10. \<And>s. ((\<lambda>_. True) and (cur_tcb and valid_sched)) s \<Longrightarrow> ((\<lambda>_. True) and ?Q6) s
A total of 13 subgoals... proof (prove)
goal (15 subgoals):
 1. \<And>cur state state' rv rv' rva rv'a. \<lbrakk>thread_state_relation state state'; dc rv rv'; rva = rv'a\<rbrakk> \<Longrightarrow> corres dc (?R180 cur state state' rv rv' rva) (?R'180 cur state state' rv rv' rv'a) (when (rva = 0) reschedule_required) (when (rv'a = 0) rescheduleRequired)
 2. \<And>cur state state' rv rv'. \<lbrakk>thread_state_relation state state'; dc rv rv'\<rbrakk> \<Longrightarrow> \<lbrace>?Q181 cur state state' rv\<rbrace> gets domain_time \<lbrace>?R180 cur state state' rv rv'\<rbrace>
 3. \<And>cur state state' rv rv'. \<lbrakk>thread_state_relation state state'; dc rv rv'\<rbrakk> \<Longrightarrow> \<lbrace>?Q'182 cur state state' rv'\<rbrace> getDomainTime \<lbrace>?R'180 cur state state' rv rv'\<rbrace>
 4. \<And>cur state state'. thread_state_relation state state' \<Longrightarrow> \<lbrace>?Q176 cur state state' ()\<rbrace> dec_domain_time \<lbrace>\<lambda>rv. (\<lambda>_. True) and ?Q181 cur state state' rv\<rbrace>
 5. \<And>cur state state'. thread_state_relation state state' \<Longrightarrow> \<lbrace>?Q'175 cur state state' ()\<rbrace> decDomainTime \<lbrace>\<lambda>rv'. (\<lambda>_. True) and ?Q'182 cur state state' rv'\<rbrace>
 6. \<And>cur state state'. thread_state_relation state state' \<Longrightarrow> \<lbrace>?Q17 cur state\<rbrace> if state = Structures_A.thread_state.Running then do ts <- ethread_get tcb_time_slice cur;
let ts' = ts - 1 in if 0 < ts' then ethread_set (tcb_time_slice_update (\<lambda>_. ts')) cur else do ethread_set (tcb_time_slice_update (\<lambda>_. timeSlice)) cur;
tcb_sched_action tcb_sched_append cur;
reschedule_required
od
od else return () \<lbrace>\<lambda>a b. Suc 0 < numDomains \<longrightarrow> ((\<lambda>_. True) and ?Q176 cur state state' a) b\<rbrace>
 7. \<And>cur state state'. thread_state_relation state state' \<Longrightarrow> \<lbrace>?Q'19 cur state'\<rbrace> if state' = Structures_H.thread_state.Running then do ts <- threadGet tcbTimeSlice cur;
ts' <- return (ts - 1);
if 0 < ts' then threadSet (tcbTimeSlice_update (\<lambda>_. ts')) cur else do threadSet (tcbTimeSlice_update (\<lambda>_. timeSlice)) cur;
tcbSchedAppend cur;
rescheduleRequired
od
od else return () \<lbrace>\<lambda>a b. Suc 0 < numDomains \<longrightarrow> ((\<lambda>_. True) and ?Q'175 cur state state' a) b\<rbrace>
 8. \<And>cur. \<lbrace>?Q10 cur\<rbrace> get_thread_state cur \<lbrace>\<lambda>state. (if state = Structures_A.thread_state.Running then is_etcb_at cur and (\<lambda>a. etcb_at (\<lambda>t. (tcb_at cur and valid_etcbs and (tcb_at cur and valid_etcbs and (\<lambda>s. is_etcb_at cur s \<and> weak_valid_sched_action s \<and> valid_etcbs s))) a) cur a) else (\<lambda>_. True)) and ?Q17 cur state\<rbrace>
 9. \<And>cur. \<lbrace>?Q'10 cur\<rbrace> getThreadState cur \<lbrace>\<lambda>state'. (if state' = Structures_H.thread_state.Running then tcb_at' cur and (tcb_at' cur and (tcb_at' cur and (\<lambda>s. obj_at' (\<lambda>obj. if cur = cur then True else True) cur s \<and> (Invariants_H.valid_queues and (\<lambda>s. \<forall>d p. (\<exists>tcb. (inQ d p tcb \<and> runnable' (tcbState tcb)) \<and> \<not> (inQ d p (tcbTimeSlice_update (\<lambda>_. timeSlice) tcb) \<and> runnable' (tcbState (tcbTimeSlice_update (\<lambda>_. timeSlice) tcb)))) \<longrightarrow> obj_at' (\<lambda>tcb. (inQ d p tcb \<and> runnable' (tcbState tcb)) \<and> \<not> (inQ d p (tcbTimeSlice_update (\<lambda>_. timeSlice) tcb) \<and> runnable' (tcbState (tcbTimeSlice_update (\<lambda>_. timeSlice) tcb)))) cur s \<longrightarrow> cur \<notin> set (ksReadyQueues s (d, p)))) s \<and> ((\<forall>ko qdom prio. ko_at' ko cur s \<and> inQ qdom prio (tcbTimeSlice_update (\<lambda>_. timeSlice) ko) \<and> \<not> inQ qdom prio ko \<longrightarrow> cur \<in> set (ksReadyQueues s (qdom, prio))) \<and> valid_queues' s) \<and> (invs' and tcb_at' cur) s \<and> (tcb_at' cur s \<longrightarrow> (if cur = cur then obj_at' (\<lambda>tcb. runnable' (itcbState (tcb_to_itcb' (tcbTimeSlice_update (\<lambda>_. timeSlice) tcb)))) cur s else st_tcb_at' runnable' cur s))))) else (\<lambda>_. True)) and ?Q'19 cur state'\<rbrace>
 10. \<lbrace>?Q6\<rbrace> gets cur_thread \<lbrace>\<lambda>cur. tcb_at cur and ?Q10 cur\<rbrace>
A total of 15 subgoals... proof (prove)
goal (15 subgoals):
 1. \<And>cur state state' rv rv' rva rv'a. \<lbrakk>thread_state_relation state state'; dc rv rv'; rva = rv'a\<rbrakk> \<Longrightarrow> corres dc (?P188 cur state state' rv rv' rva) (?P'190 cur state state' rv rv' rv'a) reschedule_required rescheduleRequired
 2. \<And>cur state state' rv rv'. \<lbrakk>thread_state_relation state state'; dc rv rv'\<rbrakk> \<Longrightarrow> \<lbrace>?Q181 cur state state' rv\<rbrace> gets domain_time \<lbrace>\<lambda>rva x. rva = 0 \<longrightarrow> ?P188 cur state state' rv rv' rva x\<rbrace>
 3. \<And>cur state state' rv rv'. \<lbrakk>thread_state_relation state state'; dc rv rv'\<rbrakk> \<Longrightarrow> \<lbrace>?Q'182 cur state state' rv'\<rbrace> getDomainTime \<lbrace>\<lambda>rv'a x. rv'a = 0 \<longrightarrow> ?P'190 cur state state' rv rv' rv'a x\<rbrace>
 4. \<And>cur state state'. thread_state_relation state state' \<Longrightarrow> \<lbrace>?Q176 cur state state' ()\<rbrace> dec_domain_time \<lbrace>\<lambda>rv. (\<lambda>_. True) and ?Q181 cur state state' rv\<rbrace>
 5. \<And>cur state state'. thread_state_relation state state' \<Longrightarrow> \<lbrace>?Q'175 cur state state' ()\<rbrace> decDomainTime \<lbrace>\<lambda>rv'. (\<lambda>_. True) and ?Q'182 cur state state' rv'\<rbrace>
 6. \<And>cur state state'. thread_state_relation state state' \<Longrightarrow> \<lbrace>?Q17 cur state\<rbrace> if state = Structures_A.thread_state.Running then do ts <- ethread_get tcb_time_slice cur;
let ts' = ts - 1 in if 0 < ts' then ethread_set (tcb_time_slice_update (\<lambda>_. ts')) cur else do ethread_set (tcb_time_slice_update (\<lambda>_. timeSlice)) cur;
tcb_sched_action tcb_sched_append cur;
reschedule_required
od
od else return () \<lbrace>\<lambda>a b. Suc 0 < numDomains \<longrightarrow> ((\<lambda>_. True) and ?Q176 cur state state' a) b\<rbrace>
 7. \<And>cur state state'. thread_state_relation state state' \<Longrightarrow> \<lbrace>?Q'19 cur state'\<rbrace> if state' = Structures_H.thread_state.Running then do ts <- threadGet tcbTimeSlice cur;
ts' <- return (ts - 1);
if 0 < ts' then threadSet (tcbTimeSlice_update (\<lambda>_. ts')) cur else do threadSet (tcbTimeSlice_update (\<lambda>_. timeSlice)) cur;
tcbSchedAppend cur;
rescheduleRequired
od
od else return () \<lbrace>\<lambda>a b. Suc 0 < numDomains \<longrightarrow> ((\<lambda>_. True) and ?Q'175 cur state state' a) b\<rbrace>
 8. \<And>cur. \<lbrace>?Q10 cur\<rbrace> get_thread_state cur \<lbrace>\<lambda>state. (if state = Structures_A.thread_state.Running then is_etcb_at cur and (\<lambda>a. etcb_at (\<lambda>t. (tcb_at cur and valid_etcbs and (tcb_at cur and valid_etcbs and (\<lambda>s. is_etcb_at cur s \<and> weak_valid_sched_action s \<and> valid_etcbs s))) a) cur a) else (\<lambda>_. True)) and ?Q17 cur state\<rbrace>
 9. \<And>cur. \<lbrace>?Q'10 cur\<rbrace> getThreadState cur \<lbrace>\<lambda>state'. (if state' = Structures_H.thread_state.Running then tcb_at' cur and (tcb_at' cur and (tcb_at' cur and (\<lambda>s. obj_at' (\<lambda>obj. if cur = cur then True else True) cur s \<and> (Invariants_H.valid_queues and (\<lambda>s. \<forall>d p. (\<exists>tcb. (inQ d p tcb \<and> runnable' (tcbState tcb)) \<and> \<not> (inQ d p (tcbTimeSlice_update (\<lambda>_. timeSlice) tcb) \<and> runnable' (tcbState (tcbTimeSlice_update (\<lambda>_. timeSlice) tcb)))) \<longrightarrow> obj_at' (\<lambda>tcb. (inQ d p tcb \<and> runnable' (tcbState tcb)) \<and> \<not> (inQ d p (tcbTimeSlice_update (\<lambda>_. timeSlice) tcb) \<and> runnable' (tcbState (tcbTimeSlice_update (\<lambda>_. timeSlice) tcb)))) cur s \<longrightarrow> cur \<notin> set (ksReadyQueues s (d, p)))) s \<and> ((\<forall>ko qdom prio. ko_at' ko cur s \<and> inQ qdom prio (tcbTimeSlice_update (\<lambda>_. timeSlice) ko) \<and> \<not> inQ qdom prio ko \<longrightarrow> cur \<in> set (ksReadyQueues s (qdom, prio))) \<and> valid_queues' s) \<and> (invs' and tcb_at' cur) s \<and> (tcb_at' cur s \<longrightarrow> (if cur = cur then obj_at' (\<lambda>tcb. runnable' (itcbState (tcb_to_itcb' (tcbTimeSlice_update (\<lambda>_. timeSlice) tcb)))) cur s else st_tcb_at' runnable' cur s))))) else (\<lambda>_. True)) and ?Q'19 cur state'\<rbrace>
 10. \<lbrace>?Q6\<rbrace> gets cur_thread \<lbrace>\<lambda>cur. tcb_at cur and ?Q10 cur\<rbrace>
A total of 15 subgoals... proof (prove)
goal (14 subgoals):
 1. \<And>cur state state' rv rv'. \<lbrakk>thread_state_relation state state'; dc rv rv'\<rbrakk> \<Longrightarrow> \<lbrace>?Q181 cur state state' rv\<rbrace> gets domain_time \<lbrace>\<lambda>rva x. rva = 0 \<longrightarrow> (weak_valid_sched_action and valid_etcbs) x\<rbrace>
 2. \<And>cur state state' rv rv'. \<lbrakk>thread_state_relation state state'; dc rv rv'\<rbrakk> \<Longrightarrow> \<lbrace>?Q'182 cur state state' rv'\<rbrace> getDomainTime \<lbrace>\<lambda>rv'a x. rv'a = 0 \<longrightarrow> (Invariants_H.valid_queues and valid_queues' and (\<lambda>s. weak_sch_act_wf (ksSchedulerAction s) s)) x\<rbrace>
 3. \<And>cur state state'. thread_state_relation state state' \<Longrightarrow> \<lbrace>?Q176 cur state state' ()\<rbrace> dec_domain_time \<lbrace>\<lambda>rv. (\<lambda>_. True) and ?Q181 cur state state' rv\<rbrace>
 4. \<And>cur state state'. thread_state_relation state state' \<Longrightarrow> \<lbrace>?Q'175 cur state state' ()\<rbrace> decDomainTime \<lbrace>\<lambda>rv'. (\<lambda>_. True) and ?Q'182 cur state state' rv'\<rbrace>
 5. \<And>cur state state'. thread_state_relation state state' \<Longrightarrow> \<lbrace>?Q17 cur state\<rbrace> if state = Structures_A.thread_state.Running then do ts <- ethread_get tcb_time_slice cur;
let ts' = ts - 1 in if 0 < ts' then ethread_set (tcb_time_slice_update (\<lambda>_. ts')) cur else do ethread_set (tcb_time_slice_update (\<lambda>_. timeSlice)) cur;
tcb_sched_action tcb_sched_append cur;
reschedule_required
od
od else return () \<lbrace>\<lambda>a b. Suc 0 < numDomains \<longrightarrow> ((\<lambda>_. True) and ?Q176 cur state state' a) b\<rbrace>
 6. \<And>cur state state'. thread_state_relation state state' \<Longrightarrow> \<lbrace>?Q'19 cur state'\<rbrace> if state' = Structures_H.thread_state.Running then do ts <- threadGet tcbTimeSlice cur;
ts' <- return (ts - 1);
if 0 < ts' then threadSet (tcbTimeSlice_update (\<lambda>_. ts')) cur else do threadSet (tcbTimeSlice_update (\<lambda>_. timeSlice)) cur;
tcbSchedAppend cur;
rescheduleRequired
od
od else return () \<lbrace>\<lambda>a b. Suc 0 < numDomains \<longrightarrow> ((\<lambda>_. True) and ?Q'175 cur state state' a) b\<rbrace>
 7. \<And>cur. \<lbrace>?Q10 cur\<rbrace> get_thread_state cur \<lbrace>\<lambda>state. (if state = Structures_A.thread_state.Running then is_etcb_at cur and (\<lambda>a. etcb_at (\<lambda>t. (tcb_at cur and valid_etcbs and (tcb_at cur and valid_etcbs and (\<lambda>s. is_etcb_at cur s \<and> weak_valid_sched_action s \<and> valid_etcbs s))) a) cur a) else (\<lambda>_. True)) and ?Q17 cur state\<rbrace>
 8. \<And>cur. \<lbrace>?Q'10 cur\<rbrace> getThreadState cur \<lbrace>\<lambda>state'. (if state' = Structures_H.thread_state.Running then tcb_at' cur and (tcb_at' cur and (tcb_at' cur and (\<lambda>s. obj_at' (\<lambda>obj. if cur = cur then True else True) cur s \<and> (Invariants_H.valid_queues and (\<lambda>s. \<forall>d p. (\<exists>tcb. (inQ d p tcb \<and> runnable' (tcbState tcb)) \<and> \<not> (inQ d p (tcbTimeSlice_update (\<lambda>_. timeSlice) tcb) \<and> runnable' (tcbState (tcbTimeSlice_update (\<lambda>_. timeSlice) tcb)))) \<longrightarrow> obj_at' (\<lambda>tcb. (inQ d p tcb \<and> runnable' (tcbState tcb)) \<and> \<not> (inQ d p (tcbTimeSlice_update (\<lambda>_. timeSlice) tcb) \<and> runnable' (tcbState (tcbTimeSlice_update (\<lambda>_. timeSlice) tcb)))) cur s \<longrightarrow> cur \<notin> set (ksReadyQueues s (d, p)))) s \<and> ((\<forall>ko qdom prio. ko_at' ko cur s \<and> inQ qdom prio (tcbTimeSlice_update (\<lambda>_. timeSlice) ko) \<and> \<not> inQ qdom prio ko \<longrightarrow> cur \<in> set (ksReadyQueues s (qdom, prio))) \<and> valid_queues' s) \<and> (invs' and tcb_at' cur) s \<and> (tcb_at' cur s \<longrightarrow> (if cur = cur then obj_at' (\<lambda>tcb. runnable' (itcbState (tcb_to_itcb' (tcbTimeSlice_update (\<lambda>_. timeSlice) tcb)))) cur s else st_tcb_at' runnable' cur s))))) else (\<lambda>_. True)) and ?Q'19 cur state'\<rbrace>
 9. \<lbrace>?Q6\<rbrace> gets cur_thread \<lbrace>\<lambda>cur. tcb_at cur and ?Q10 cur\<rbrace>
 10. \<lbrace>?Q'6\<rbrace> getCurThread \<lbrace>\<lambda>cur. tcb_at' cur and ?Q'10 cur\<rbrace>
A total of 14 subgoals... proof (prove)
goal (12 subgoals):
 1. \<And>cur state state'. thread_state_relation state state' \<Longrightarrow> \<lbrace>?P'204 cur state state' ()\<rbrace> dec_domain_time \<lbrace>\<lambda>rv s. weak_valid_sched_action s \<and> valid_etcbs s\<rbrace>
 2. \<And>cur state state'. thread_state_relation state state' \<Longrightarrow> \<lbrace>?Q'175 cur state state' ()\<rbrace> decDomainTime \<lbrace>\<lambda>rv'. (\<lambda>_. True) and (Invariants_H.valid_queues and valid_queues' and (\<lambda>s. weak_sch_act_wf (ksSchedulerAction s) s))\<rbrace>
 3. \<And>cur state state'. thread_state_relation state state' \<Longrightarrow> \<lbrace>?Q17 cur state\<rbrace> if state = Structures_A.thread_state.Running then do ts <- ethread_get tcb_time_slice cur;
let ts' = ts - 1 in if 0 < ts' then ethread_set (tcb_time_slice_update (\<lambda>_. ts')) cur else do ethread_set (tcb_time_slice_update (\<lambda>_. timeSlice)) cur;
tcb_sched_action tcb_sched_append cur;
reschedule_required
od
od else return () \<lbrace>\<lambda>a b. Suc 0 < numDomains \<longrightarrow> ((\<lambda>_. True) and (\<lambda>b. True \<and> ?P'204 cur state state' a b)) b\<rbrace>
 4. \<And>cur state state'. thread_state_relation state state' \<Longrightarrow> \<lbrace>?Q'19 cur state'\<rbrace> if state' = Structures_H.thread_state.Running then do ts <- threadGet tcbTimeSlice cur;
ts' <- return (ts - 1);
if 0 < ts' then threadSet (tcbTimeSlice_update (\<lambda>_. ts')) cur else do threadSet (tcbTimeSlice_update (\<lambda>_. timeSlice)) cur;
tcbSchedAppend cur;
rescheduleRequired
od
od else return () \<lbrace>\<lambda>a b. Suc 0 < numDomains \<longrightarrow> ((\<lambda>_. True) and ?Q'175 cur state state' a) b\<rbrace>
 5. \<And>cur. \<lbrace>?Q10 cur\<rbrace> get_thread_state cur \<lbrace>\<lambda>state. (if state = Structures_A.thread_state.Running then is_etcb_at cur and (\<lambda>a. etcb_at (\<lambda>t. (tcb_at cur and valid_etcbs and (tcb_at cur and valid_etcbs and (\<lambda>s. is_etcb_at cur s \<and> weak_valid_sched_action s \<and> valid_etcbs s))) a) cur a) else (\<lambda>_. True)) and ?Q17 cur state\<rbrace>
 6. \<And>cur. \<lbrace>?Q'10 cur\<rbrace> getThreadState cur \<lbrace>\<lambda>state'. (if state' = Structures_H.thread_state.Running then tcb_at' cur and (tcb_at' cur and (tcb_at' cur and (\<lambda>s. obj_at' (\<lambda>obj. if cur = cur then True else True) cur s \<and> (Invariants_H.valid_queues and (\<lambda>s. \<forall>d p. (\<exists>tcb. (inQ d p tcb \<and> runnable' (tcbState tcb)) \<and> \<not> (inQ d p (tcbTimeSlice_update (\<lambda>_. timeSlice) tcb) \<and> runnable' (tcbState (tcbTimeSlice_update (\<lambda>_. timeSlice) tcb)))) \<longrightarrow> obj_at' (\<lambda>tcb. (inQ d p tcb \<and> runnable' (tcbState tcb)) \<and> \<not> (inQ d p (tcbTimeSlice_update (\<lambda>_. timeSlice) tcb) \<and> runnable' (tcbState (tcbTimeSlice_update (\<lambda>_. timeSlice) tcb)))) cur s \<longrightarrow> cur \<notin> set (ksReadyQueues s (d, p)))) s \<and> ((\<forall>ko qdom prio. ko_at' ko cur s \<and> inQ qdom prio (tcbTimeSlice_update (\<lambda>_. timeSlice) ko) \<and> \<not> inQ qdom prio ko \<longrightarrow> cur \<in> set (ksReadyQueues s (qdom, prio))) \<and> valid_queues' s) \<and> (invs' and tcb_at' cur) s \<and> (tcb_at' cur s \<longrightarrow> (if cur = cur then obj_at' (\<lambda>tcb. runnable' (itcbState (tcb_to_itcb' (tcbTimeSlice_update (\<lambda>_. timeSlice) tcb)))) cur s else st_tcb_at' runnable' cur s))))) else (\<lambda>_. True)) and ?Q'19 cur state'\<rbrace>
 7. \<lbrace>?Q6\<rbrace> gets cur_thread \<lbrace>\<lambda>cur. tcb_at cur and ?Q10 cur\<rbrace>
 8. \<lbrace>?Q'6\<rbrace> getCurThread \<lbrace>\<lambda>cur. tcb_at' cur and ?Q'10 cur\<rbrace>
 9. \<And>s. ((\<lambda>_. True) and (cur_tcb and valid_sched)) s \<Longrightarrow> ((\<lambda>_. True) and ?Q6) s
 10. \<And>s. ((\<lambda>_. True) and invs') s \<Longrightarrow> ((\<lambda>_. True) and ?Q'6) s
A total of 12 subgoals... proof (prove)
goal (12 subgoals):
 1. \<And>cur state state'. thread_state_relation state state' \<Longrightarrow> \<lbrace>?P'204 cur state state' ()\<rbrace> modify (\<lambda>s. domain_time_update (\<lambda>_. domain_time s - 1) s) \<lbrace>\<lambda>rv s. weak_valid_sched_action s \<and> valid_etcbs s\<rbrace>
 2. \<And>cur state state'. thread_state_relation state state' \<Longrightarrow> \<lbrace>?Q'175 cur state state' ()\<rbrace> decDomainTime \<lbrace>\<lambda>rv'. (\<lambda>_. True) and (Invariants_H.valid_queues and valid_queues' and (\<lambda>s. weak_sch_act_wf (ksSchedulerAction s) s))\<rbrace>
 3. \<And>cur state state'. thread_state_relation state state' \<Longrightarrow> \<lbrace>?Q17 cur state\<rbrace> if state = Structures_A.thread_state.Running then do ts <- ethread_get tcb_time_slice cur;
let ts' = ts - 1 in if 0 < ts' then ethread_set (tcb_time_slice_update (\<lambda>_. ts')) cur else do ethread_set (tcb_time_slice_update (\<lambda>_. timeSlice)) cur;
tcb_sched_action tcb_sched_append cur;
reschedule_required
od
od else return () \<lbrace>\<lambda>a b. Suc 0 < numDomains \<longrightarrow> ((\<lambda>_. True) and (\<lambda>b. True \<and> ?P'204 cur state state' a b)) b\<rbrace>
 4. \<And>cur state state'. thread_state_relation state state' \<Longrightarrow> \<lbrace>?Q'19 cur state'\<rbrace> if state' = Structures_H.thread_state.Running then do ts <- threadGet tcbTimeSlice cur;
ts' <- return (ts - 1);
if 0 < ts' then threadSet (tcbTimeSlice_update (\<lambda>_. ts')) cur else do threadSet (tcbTimeSlice_update (\<lambda>_. timeSlice)) cur;
tcbSchedAppend cur;
rescheduleRequired
od
od else return () \<lbrace>\<lambda>a b. Suc 0 < numDomains \<longrightarrow> ((\<lambda>_. True) and ?Q'175 cur state state' a) b\<rbrace>
 5. \<And>cur. \<lbrace>?Q10 cur\<rbrace> get_thread_state cur \<lbrace>\<lambda>state. (if state = Structures_A.thread_state.Running then is_etcb_at cur and (\<lambda>a. etcb_at (\<lambda>t. (tcb_at cur and valid_etcbs and (tcb_at cur and valid_etcbs and (\<lambda>s. is_etcb_at cur s \<and> weak_valid_sched_action s \<and> valid_etcbs s))) a) cur a) else (\<lambda>_. True)) and ?Q17 cur state\<rbrace>
 6. \<And>cur. \<lbrace>?Q'10 cur\<rbrace> getThreadState cur \<lbrace>\<lambda>state'. (if state' = Structures_H.thread_state.Running then tcb_at' cur and (tcb_at' cur and (tcb_at' cur and (\<lambda>s. obj_at' (\<lambda>obj. if cur = cur then True else True) cur s \<and> (Invariants_H.valid_queues and (\<lambda>s. \<forall>d p. (\<exists>tcb. (inQ d p tcb \<and> runnable' (tcbState tcb)) \<and> \<not> (inQ d p (tcbTimeSlice_update (\<lambda>_. timeSlice) tcb) \<and> runnable' (tcbState (tcbTimeSlice_update (\<lambda>_. timeSlice) tcb)))) \<longrightarrow> obj_at' (\<lambda>tcb. (inQ d p tcb \<and> runnable' (tcbState tcb)) \<and> \<not> (inQ d p (tcbTimeSlice_update (\<lambda>_. timeSlice) tcb) \<and> runnable' (tcbState (tcbTimeSlice_update (\<lambda>_. timeSlice) tcb)))) cur s \<longrightarrow> cur \<notin> set (ksReadyQueues s (d, p)))) s \<and> ((\<forall>ko qdom prio. ko_at' ko cur s \<and> inQ qdom prio (tcbTimeSlice_update (\<lambda>_. timeSlice) ko) \<and> \<not> inQ qdom prio ko \<longrightarrow> cur \<in> set (ksReadyQueues s (qdom, prio))) \<and> valid_queues' s) \<and> (invs' and tcb_at' cur) s \<and> (tcb_at' cur s \<longrightarrow> (if cur = cur then obj_at' (\<lambda>tcb. runnable' (itcbState (tcb_to_itcb' (tcbTimeSlice_update (\<lambda>_. timeSlice) tcb)))) cur s else st_tcb_at' runnable' cur s))))) else (\<lambda>_. True)) and ?Q'19 cur state'\<rbrace>
 7. \<lbrace>?Q6\<rbrace> gets cur_thread \<lbrace>\<lambda>cur. tcb_at cur and ?Q10 cur\<rbrace>
 8. \<lbrace>?Q'6\<rbrace> getCurThread \<lbrace>\<lambda>cur. tcb_at' cur and ?Q'10 cur\<rbrace>
 9. \<And>s. ((\<lambda>_. True) and (cur_tcb and valid_sched)) s \<Longrightarrow> ((\<lambda>_. True) and ?Q6) s
 10. \<And>s. ((\<lambda>_. True) and invs') s \<Longrightarrow> ((\<lambda>_. True) and ?Q'6) s
A total of 12 subgoals... proof (prove)
goal (11 subgoals):
 1. \<And>cur state state'. thread_state_relation state state' \<Longrightarrow> \<lbrace>?P'215 cur state state' ()\<rbrace> decDomainTime \<lbrace>\<lambda>rv s. Invariants_H.valid_queues s \<and> valid_queues' s \<and> weak_sch_act_wf (ksSchedulerAction s) s\<rbrace>
 2. \<And>cur state state'. thread_state_relation state state' \<Longrightarrow> \<lbrace>?Q17 cur state\<rbrace> if state = Structures_A.thread_state.Running then do ts <- ethread_get tcb_time_slice cur;
let ts' = ts - 1 in if 0 < ts' then ethread_set (tcb_time_slice_update (\<lambda>_. ts')) cur else do ethread_set (tcb_time_slice_update (\<lambda>_. timeSlice)) cur;
tcb_sched_action tcb_sched_append cur;
reschedule_required
od
od else return () \<lbrace>\<lambda>a b. Suc 0 < numDomains \<longrightarrow> ((\<lambda>_. True) and (\<lambda>a. True \<and> weak_valid_sched_action (domain_time_update (\<lambda>_. domain_time a - 1) a) \<and> valid_etcbs (domain_time_update (\<lambda>_. domain_time a - 1) a))) b\<rbrace>
 3. \<And>cur state state'. thread_state_relation state state' \<Longrightarrow> \<lbrace>?Q'19 cur state'\<rbrace> if state' = Structures_H.thread_state.Running then do ts <- threadGet tcbTimeSlice cur;
ts' <- return (ts - 1);
if 0 < ts' then threadSet (tcbTimeSlice_update (\<lambda>_. ts')) cur else do threadSet (tcbTimeSlice_update (\<lambda>_. timeSlice)) cur;
tcbSchedAppend cur;
rescheduleRequired
od
od else return () \<lbrace>\<lambda>a b. Suc 0 < numDomains \<longrightarrow> ((\<lambda>_. True) and (\<lambda>b. True \<and> ?P'215 cur state state' a b)) b\<rbrace>
 4. \<And>cur. \<lbrace>?Q10 cur\<rbrace> get_thread_state cur \<lbrace>\<lambda>state. (if state = Structures_A.thread_state.Running then is_etcb_at cur and (\<lambda>a. etcb_at (\<lambda>t. (tcb_at cur and valid_etcbs and (tcb_at cur and valid_etcbs and (\<lambda>s. is_etcb_at cur s \<and> weak_valid_sched_action s \<and> valid_etcbs s))) a) cur a) else (\<lambda>_. True)) and ?Q17 cur state\<rbrace>
 5. \<And>cur. \<lbrace>?Q'10 cur\<rbrace> getThreadState cur \<lbrace>\<lambda>state'. (if state' = Structures_H.thread_state.Running then tcb_at' cur and (tcb_at' cur and (tcb_at' cur and (\<lambda>s. obj_at' (\<lambda>obj. if cur = cur then True else True) cur s \<and> (Invariants_H.valid_queues and (\<lambda>s. \<forall>d p. (\<exists>tcb. (inQ d p tcb \<and> runnable' (tcbState tcb)) \<and> \<not> (inQ d p (tcbTimeSlice_update (\<lambda>_. timeSlice) tcb) \<and> runnable' (tcbState (tcbTimeSlice_update (\<lambda>_. timeSlice) tcb)))) \<longrightarrow> obj_at' (\<lambda>tcb. (inQ d p tcb \<and> runnable' (tcbState tcb)) \<and> \<not> (inQ d p (tcbTimeSlice_update (\<lambda>_. timeSlice) tcb) \<and> runnable' (tcbState (tcbTimeSlice_update (\<lambda>_. timeSlice) tcb)))) cur s \<longrightarrow> cur \<notin> set (ksReadyQueues s (d, p)))) s \<and> ((\<forall>ko qdom prio. ko_at' ko cur s \<and> inQ qdom prio (tcbTimeSlice_update (\<lambda>_. timeSlice) ko) \<and> \<not> inQ qdom prio ko \<longrightarrow> cur \<in> set (ksReadyQueues s (qdom, prio))) \<and> valid_queues' s) \<and> (invs' and tcb_at' cur) s \<and> (tcb_at' cur s \<longrightarrow> (if cur = cur then obj_at' (\<lambda>tcb. runnable' (itcbState (tcb_to_itcb' (tcbTimeSlice_update (\<lambda>_. timeSlice) tcb)))) cur s else st_tcb_at' runnable' cur s))))) else (\<lambda>_. True)) and ?Q'19 cur state'\<rbrace>
 6. \<lbrace>?Q6\<rbrace> gets cur_thread \<lbrace>\<lambda>cur. tcb_at cur and ?Q10 cur\<rbrace>
 7. \<lbrace>?Q'6\<rbrace> getCurThread \<lbrace>\<lambda>cur. tcb_at' cur and ?Q'10 cur\<rbrace>
 8. \<And>s. ((\<lambda>_. True) and (cur_tcb and valid_sched)) s \<Longrightarrow> ((\<lambda>_. True) and ?Q6) s
 9. \<And>s. ((\<lambda>_. True) and invs') s \<Longrightarrow> ((\<lambda>_. True) and ?Q'6) s
 10. \<And>s. (cur_tcb and valid_sched) s \<Longrightarrow> ((\<lambda>_. True) and (cur_tcb and valid_sched)) s
A total of 11 subgoals... proof (prove)
goal (11 subgoals):
 1. \<And>cur state state'. thread_state_relation state state' \<Longrightarrow> \<lbrace>?P'215 cur state state' ()\<rbrace> modify (\<lambda>ks. ks\<lparr>ksDomainTime := ksDomainTime ks - 1\<rparr>) \<lbrace>\<lambda>rv s. Invariants_H.valid_queues s \<and> valid_queues' s \<and> weak_sch_act_wf (ksSchedulerAction s) s\<rbrace>
 2. \<And>cur state state'. thread_state_relation state state' \<Longrightarrow> \<lbrace>?Q17 cur state\<rbrace> if state = Structures_A.thread_state.Running then do ts <- ethread_get tcb_time_slice cur;
let ts' = ts - 1 in if 0 < ts' then ethread_set (tcb_time_slice_update (\<lambda>_. ts')) cur else do ethread_set (tcb_time_slice_update (\<lambda>_. timeSlice)) cur;
tcb_sched_action tcb_sched_append cur;
reschedule_required
od
od else return () \<lbrace>\<lambda>a b. Suc 0 < numDomains \<longrightarrow> ((\<lambda>_. True) and (\<lambda>a. True \<and> weak_valid_sched_action (domain_time_update (\<lambda>_. domain_time a - 1) a) \<and> valid_etcbs (domain_time_update (\<lambda>_. domain_time a - 1) a))) b\<rbrace>
 3. \<And>cur state state'. thread_state_relation state state' \<Longrightarrow> \<lbrace>?Q'19 cur state'\<rbrace> if state' = Structures_H.thread_state.Running then do ts <- threadGet tcbTimeSlice cur;
ts' <- return (ts - 1);
if 0 < ts' then threadSet (tcbTimeSlice_update (\<lambda>_. ts')) cur else do threadSet (tcbTimeSlice_update (\<lambda>_. timeSlice)) cur;
tcbSchedAppend cur;
rescheduleRequired
od
od else return () \<lbrace>\<lambda>a b. Suc 0 < numDomains \<longrightarrow> ((\<lambda>_. True) and (\<lambda>b. True \<and> ?P'215 cur state state' a b)) b\<rbrace>
 4. \<And>cur. \<lbrace>?Q10 cur\<rbrace> get_thread_state cur \<lbrace>\<lambda>state. (if state = Structures_A.thread_state.Running then is_etcb_at cur and (\<lambda>a. etcb_at (\<lambda>t. (tcb_at cur and valid_etcbs and (tcb_at cur and valid_etcbs and (\<lambda>s. is_etcb_at cur s \<and> weak_valid_sched_action s \<and> valid_etcbs s))) a) cur a) else (\<lambda>_. True)) and ?Q17 cur state\<rbrace>
 5. \<And>cur. \<lbrace>?Q'10 cur\<rbrace> getThreadState cur \<lbrace>\<lambda>state'. (if state' = Structures_H.thread_state.Running then tcb_at' cur and (tcb_at' cur and (tcb_at' cur and (\<lambda>s. obj_at' (\<lambda>obj. if cur = cur then True else True) cur s \<and> (Invariants_H.valid_queues and (\<lambda>s. \<forall>d p. (\<exists>tcb. (inQ d p tcb \<and> runnable' (tcbState tcb)) \<and> \<not> (inQ d p (tcbTimeSlice_update (\<lambda>_. timeSlice) tcb) \<and> runnable' (tcbState (tcbTimeSlice_update (\<lambda>_. timeSlice) tcb)))) \<longrightarrow> obj_at' (\<lambda>tcb. (inQ d p tcb \<and> runnable' (tcbState tcb)) \<and> \<not> (inQ d p (tcbTimeSlice_update (\<lambda>_. timeSlice) tcb) \<and> runnable' (tcbState (tcbTimeSlice_update (\<lambda>_. timeSlice) tcb)))) cur s \<longrightarrow> cur \<notin> set (ksReadyQueues s (d, p)))) s \<and> ((\<forall>ko qdom prio. ko_at' ko cur s \<and> inQ qdom prio (tcbTimeSlice_update (\<lambda>_. timeSlice) ko) \<and> \<not> inQ qdom prio ko \<longrightarrow> cur \<in> set (ksReadyQueues s (qdom, prio))) \<and> valid_queues' s) \<and> (invs' and tcb_at' cur) s \<and> (tcb_at' cur s \<longrightarrow> (if cur = cur then obj_at' (\<lambda>tcb. runnable' (itcbState (tcb_to_itcb' (tcbTimeSlice_update (\<lambda>_. timeSlice) tcb)))) cur s else st_tcb_at' runnable' cur s))))) else (\<lambda>_. True)) and ?Q'19 cur state'\<rbrace>
 6. \<lbrace>?Q6\<rbrace> gets cur_thread \<lbrace>\<lambda>cur. tcb_at cur and ?Q10 cur\<rbrace>
 7. \<lbrace>?Q'6\<rbrace> getCurThread \<lbrace>\<lambda>cur. tcb_at' cur and ?Q'10 cur\<rbrace>
 8. \<And>s. ((\<lambda>_. True) and (cur_tcb and valid_sched)) s \<Longrightarrow> ((\<lambda>_. True) and ?Q6) s
 9. \<And>s. ((\<lambda>_. True) and invs') s \<Longrightarrow> ((\<lambda>_. True) and ?Q'6) s
 10. \<And>s. (cur_tcb and valid_sched) s \<Longrightarrow> ((\<lambda>_. True) and (cur_tcb and valid_sched)) s
A total of 11 subgoals... proof (prove)
goal (10 subgoals):
 1. \<And>cur state state'. thread_state_relation state state' \<Longrightarrow> \<lbrace>?Q17 cur state\<rbrace> if state = Structures_A.thread_state.Running then do ts <- ethread_get tcb_time_slice cur;
let ts' = ts - 1 in if 0 < ts' then ethread_set (tcb_time_slice_update (\<lambda>_. ts')) cur else do ethread_set (tcb_time_slice_update (\<lambda>_. timeSlice)) cur;
tcb_sched_action tcb_sched_append cur;
reschedule_required
od
od else return () \<lbrace>\<lambda>a b. Suc 0 < numDomains \<longrightarrow> ((\<lambda>_. True) and (\<lambda>a. True \<and> weak_valid_sched_action (domain_time_update (\<lambda>_. domain_time a - 1) a) \<and> valid_etcbs (domain_time_update (\<lambda>_. domain_time a - 1) a))) b\<rbrace>
 2. \<And>cur state state'. thread_state_relation state state' \<Longrightarrow> \<lbrace>?Q'19 cur state'\<rbrace> if state' = Structures_H.thread_state.Running then do ts <- threadGet tcbTimeSlice cur;
ts' <- return (ts - 1);
if 0 < ts' then threadSet (tcbTimeSlice_update (\<lambda>_. ts')) cur else do threadSet (tcbTimeSlice_update (\<lambda>_. timeSlice)) cur;
tcbSchedAppend cur;
rescheduleRequired
od
od else return () \<lbrace>\<lambda>a b. Suc 0 < numDomains \<longrightarrow> ((\<lambda>_. True) and (\<lambda>a. True \<and> Invariants_H.valid_queues (a\<lparr>ksDomainTime := ksDomainTime a - 1\<rparr>) \<and> valid_queues' (a\<lparr>ksDomainTime := ksDomainTime a - 1\<rparr>) \<and> weak_sch_act_wf (ksSchedulerAction (a\<lparr>ksDomainTime := ksDomainTime a - 1\<rparr>)) (a\<lparr>ksDomainTime := ksDomainTime a - 1\<rparr>))) b\<rbrace>
 3. \<And>cur. \<lbrace>?Q10 cur\<rbrace> get_thread_state cur \<lbrace>\<lambda>state. (if state = Structures_A.thread_state.Running then is_etcb_at cur and (\<lambda>a. etcb_at (\<lambda>t. (tcb_at cur and valid_etcbs and (tcb_at cur and valid_etcbs and (\<lambda>s. is_etcb_at cur s \<and> weak_valid_sched_action s \<and> valid_etcbs s))) a) cur a) else (\<lambda>_. True)) and ?Q17 cur state\<rbrace>
 4. \<And>cur. \<lbrace>?Q'10 cur\<rbrace> getThreadState cur \<lbrace>\<lambda>state'. (if state' = Structures_H.thread_state.Running then tcb_at' cur and (tcb_at' cur and (tcb_at' cur and (\<lambda>s. obj_at' (\<lambda>obj. if cur = cur then True else True) cur s \<and> (Invariants_H.valid_queues and (\<lambda>s. \<forall>d p. (\<exists>tcb. (inQ d p tcb \<and> runnable' (tcbState tcb)) \<and> \<not> (inQ d p (tcbTimeSlice_update (\<lambda>_. timeSlice) tcb) \<and> runnable' (tcbState (tcbTimeSlice_update (\<lambda>_. timeSlice) tcb)))) \<longrightarrow> obj_at' (\<lambda>tcb. (inQ d p tcb \<and> runnable' (tcbState tcb)) \<and> \<not> (inQ d p (tcbTimeSlice_update (\<lambda>_. timeSlice) tcb) \<and> runnable' (tcbState (tcbTimeSlice_update (\<lambda>_. timeSlice) tcb)))) cur s \<longrightarrow> cur \<notin> set (ksReadyQueues s (d, p)))) s \<and> ((\<forall>ko qdom prio. ko_at' ko cur s \<and> inQ qdom prio (tcbTimeSlice_update (\<lambda>_. timeSlice) ko) \<and> \<not> inQ qdom prio ko \<longrightarrow> cur \<in> set (ksReadyQueues s (qdom, prio))) \<and> valid_queues' s) \<and> (invs' and tcb_at' cur) s \<and> (tcb_at' cur s \<longrightarrow> (if cur = cur then obj_at' (\<lambda>tcb. runnable' (itcbState (tcb_to_itcb' (tcbTimeSlice_update (\<lambda>_. timeSlice) tcb)))) cur s else st_tcb_at' runnable' cur s))))) else (\<lambda>_. True)) and ?Q'19 cur state'\<rbrace>
 5. \<lbrace>?Q6\<rbrace> gets cur_thread \<lbrace>\<lambda>cur. tcb_at cur and ?Q10 cur\<rbrace>
 6. \<lbrace>?Q'6\<rbrace> getCurThread \<lbrace>\<lambda>cur. tcb_at' cur and ?Q'10 cur\<rbrace>
 7. \<And>s. ((\<lambda>_. True) and (cur_tcb and valid_sched)) s \<Longrightarrow> ((\<lambda>_. True) and ?Q6) s
 8. \<And>s. ((\<lambda>_. True) and invs') s \<Longrightarrow> ((\<lambda>_. True) and ?Q'6) s
 9. \<And>s. (cur_tcb and valid_sched) s \<Longrightarrow> ((\<lambda>_. True) and (cur_tcb and valid_sched)) s
 10. \<And>s. invs' s \<Longrightarrow> ((\<lambda>_. True) and invs') s proof (prove)
goal (13 subgoals):
 1. \<And>cur state state' ts. \<lbrakk>state' = Structures_H.thread_state.Running; state = Structures_A.thread_state.Running; Suc 0 < ts\<rbrakk> \<Longrightarrow> \<lbrace>?Q233 cur Structures_A.thread_state.Running Structures_H.thread_state.Running ts\<rbrace> ethread_set (tcb_time_slice_update (\<lambda>_. ts - Suc 0)) cur \<lbrace>\<lambda>a b. Suc 0 < numDomains \<longrightarrow> weak_valid_sched_action b \<and> valid_etcbs b\<rbrace>
 2. \<And>cur state state' ts. \<lbrakk>thread_state_relation state state'; state = Structures_A.thread_state.Running; \<not> 0 < ts - 1\<rbrakk> \<Longrightarrow> \<lbrace>?R233 cur state state' ts\<rbrace> do ethread_set (tcb_time_slice_update (\<lambda>_. timeSlice)) cur;
tcb_sched_action tcb_sched_append cur;
reschedule_required
od \<lbrace>\<lambda>a b. Suc 0 < numDomains \<longrightarrow> ((\<lambda>_. True) and (\<lambda>a. True \<and> weak_valid_sched_action (domain_time_update (\<lambda>_. domain_time a - 1) a) \<and> valid_etcbs (domain_time_update (\<lambda>_. domain_time a - 1) a))) b\<rbrace>
 3. \<And>cur state state'. \<lbrakk>thread_state_relation state state'; state = Structures_A.thread_state.Running\<rbrakk> \<Longrightarrow> \<lbrace>?Q227 cur state\<rbrace> ethread_get tcb_time_slice cur \<lbrace>\<lambda>ts s. (0 < ts - 1 \<longrightarrow> ?Q233 cur state state' ts s) \<and> (\<not> 0 < ts - 1 \<longrightarrow> ?R233 cur state state' ts s)\<rbrace>
 4. \<And>cur state state'. \<lbrakk>thread_state_relation state state'; state \<noteq> Structures_A.thread_state.Running\<rbrakk> \<Longrightarrow> \<lbrace>?R229 cur state\<rbrace> return () \<lbrace>\<lambda>a b. Suc 0 < numDomains \<longrightarrow> ((\<lambda>_. True) and (\<lambda>a. True \<and> weak_valid_sched_action (domain_time_update (\<lambda>_. domain_time a - 1) a) \<and> valid_etcbs (domain_time_update (\<lambda>_. domain_time a - 1) a))) b\<rbrace>
 5. \<And>cur state state'. thread_state_relation state state' \<Longrightarrow> \<lbrace>?Q'19 cur state'\<rbrace> if state' = Structures_H.thread_state.Running then do ts <- threadGet tcbTimeSlice cur;
ts' <- return (ts - 1);
if 0 < ts' then threadSet (tcbTimeSlice_update (\<lambda>_. ts')) cur else do threadSet (tcbTimeSlice_update (\<lambda>_. timeSlice)) cur;
tcbSchedAppend cur;
rescheduleRequired
od
od else return () \<lbrace>\<lambda>a b. Suc 0 < numDomains \<longrightarrow> ((\<lambda>_. True) and (\<lambda>a. True \<and> Invariants_H.valid_queues (a\<lparr>ksDomainTime := ksDomainTime a - 1\<rparr>) \<and> valid_queues' (a\<lparr>ksDomainTime := ksDomainTime a - 1\<rparr>) \<and> weak_sch_act_wf (ksSchedulerAction (a\<lparr>ksDomainTime := ksDomainTime a - 1\<rparr>)) (a\<lparr>ksDomainTime := ksDomainTime a - 1\<rparr>))) b\<rbrace>
 6. \<And>cur. \<lbrace>?Q10 cur\<rbrace> get_thread_state cur \<lbrace>\<lambda>state. (if state = Structures_A.thread_state.Running then is_etcb_at cur and (\<lambda>a. etcb_at (\<lambda>t. (tcb_at cur and valid_etcbs and (tcb_at cur and valid_etcbs and (\<lambda>s. is_etcb_at cur s \<and> weak_valid_sched_action s \<and> valid_etcbs s))) a) cur a) else (\<lambda>_. True)) and (\<lambda>s. (state = Structures_A.thread_state.Running \<longrightarrow> ?Q227 cur state s) \<and> (state \<noteq> Structures_A.thread_state.Running \<longrightarrow> ?R229 cur state s))\<rbrace>
 7. \<And>cur. \<lbrace>?Q'10 cur\<rbrace> getThreadState cur \<lbrace>\<lambda>state'. (if state' = Structures_H.thread_state.Running then tcb_at' cur and (tcb_at' cur and (tcb_at' cur and (\<lambda>s. obj_at' (\<lambda>obj. if cur = cur then True else True) cur s \<and> (Invariants_H.valid_queues and (\<lambda>s. \<forall>d p. (\<exists>tcb. (inQ d p tcb \<and> runnable' (tcbState tcb)) \<and> \<not> (inQ d p (tcbTimeSlice_update (\<lambda>_. timeSlice) tcb) \<and> runnable' (tcbState (tcbTimeSlice_update (\<lambda>_. timeSlice) tcb)))) \<longrightarrow> obj_at' (\<lambda>tcb. (inQ d p tcb \<and> runnable' (tcbState tcb)) \<and> \<not> (inQ d p (tcbTimeSlice_update (\<lambda>_. timeSlice) tcb) \<and> runnable' (tcbState (tcbTimeSlice_update (\<lambda>_. timeSlice) tcb)))) cur s \<longrightarrow> cur \<notin> set (ksReadyQueues s (d, p)))) s \<and> ((\<forall>ko qdom prio. ko_at' ko cur s \<and> inQ qdom prio (tcbTimeSlice_update (\<lambda>_. timeSlice) ko) \<and> \<not> inQ qdom prio ko \<longrightarrow> cur \<in> set (ksReadyQueues s (qdom, prio))) \<and> valid_queues' s) \<and> (invs' and tcb_at' cur) s \<and> (tcb_at' cur s \<longrightarrow> (if cur = cur then obj_at' (\<lambda>tcb. runnable' (itcbState (tcb_to_itcb' (tcbTimeSlice_update (\<lambda>_. timeSlice) tcb)))) cur s else st_tcb_at' runnable' cur s))))) else (\<lambda>_. True)) and ?Q'19 cur state'\<rbrace>
 8. \<lbrace>?Q6\<rbrace> gets cur_thread \<lbrace>\<lambda>cur. tcb_at cur and ?Q10 cur\<rbrace>
 9. \<lbrace>?Q'6\<rbrace> getCurThread \<lbrace>\<lambda>cur. tcb_at' cur and ?Q'10 cur\<rbrace>
 10. \<And>s. ((\<lambda>_. True) and (cur_tcb and valid_sched)) s \<Longrightarrow> ((\<lambda>_. True) and ?Q6) s
A total of 13 subgoals... proof (prove)
goal (13 subgoals):
 1. \<And>cur state state' ts ts'. \<lbrakk>thread_state_relation state Structures_H.thread_state.Running; state' = Structures_H.thread_state.Running; ts' = 0\<rbrakk> \<Longrightarrow> \<lbrace>?P'351 cur state Structures_H.thread_state.Running ts 0 ()\<rbrace> tcbSchedAppend cur \<lbrace>\<lambda>rv s. weak_sch_act_wf (ksSchedulerAction s) s \<and> valid_queues' s \<and> weak_sch_act_wf (ksSchedulerAction s) s\<rbrace>
 2. \<And>cur state state' ts ts'. \<lbrakk>thread_state_relation state state'; state' = Structures_H.thread_state.Running; \<not> 0 < ts'\<rbrakk> \<Longrightarrow> \<lbrace>?R311 cur state state' ts ts'\<rbrace> threadSet (tcbTimeSlice_update (\<lambda>_. timeSlice)) cur \<lbrace>\<lambda>x s. (Invariants_H.valid_queues and st_tcb_at' runnable' cur and valid_objs') s \<and> valid_objs' s \<and> ?P'351 cur state state' ts ts' x s\<rbrace>
 3. \<And>cur state state' ts. \<lbrakk>thread_state_relation state state'; state' = Structures_H.thread_state.Running\<rbrakk> \<Longrightarrow> \<lbrace>?B309 cur state state' ts\<rbrace> return (ts - 1) \<lbrace>\<lambda>ts' s. (0 < ts' \<longrightarrow> (Invariants_H.valid_queues and (\<lambda>s. \<forall>d p. (\<exists>tcb. (inQ d p tcb \<and> runnable' (tcbState tcb)) \<and> \<not> (inQ d p (tcbTimeSlice_update (\<lambda>_. ts') tcb) \<and> runnable' (tcbState (tcbTimeSlice_update (\<lambda>_. ts') tcb)))) \<longrightarrow> obj_at' (\<lambda>tcb. (inQ d p tcb \<and> runnable' (tcbState tcb)) \<and> \<not> (inQ d p (tcbTimeSlice_update (\<lambda>_. ts') tcb) \<and> runnable' (tcbState (tcbTimeSlice_update (\<lambda>_. ts') tcb)))) cur s \<longrightarrow> cur \<notin> set (ksReadyQueues s (d, p)))) s \<and> ((\<forall>ko qdom prio. ko_at' ko cur s \<and> inQ qdom prio (tcbTimeSlice_update (\<lambda>_. ts') ko) \<and> \<not> inQ qdom prio ko \<longrightarrow> cur \<in> set (ksReadyQueues s (qdom, prio))) \<and> valid_queues' s) \<and> weak_sch_act_wf (ksSchedulerAction s) s) \<and> (\<not> 0 < ts' \<longrightarrow> ?R311 cur state state' ts ts' s)\<rbrace>
 4. \<And>cur state state'. \<lbrakk>thread_state_relation state state'; state' = Structures_H.thread_state.Running\<rbrakk> \<Longrightarrow> \<lbrace>?Q306 cur state'\<rbrace> threadGet tcbTimeSlice cur \<lbrace>?B309 cur state state'\<rbrace>
 5. \<And>cur state state'. \<lbrakk>thread_state_relation state state'; state' \<noteq> Structures_H.thread_state.Running\<rbrakk> \<Longrightarrow> \<lbrace>?R308 cur state'\<rbrace> return () \<lbrace>\<lambda>rv s. Invariants_H.valid_queues (s\<lparr>ksDomainTime := ksDomainTime s - 1\<rparr>) \<and> valid_queues' (s\<lparr>ksDomainTime := ksDomainTime s - 1\<rparr>) \<and> weak_sch_act_wf (ksSchedulerAction (s\<lparr>ksDomainTime := ksDomainTime s - 1\<rparr>)) (s\<lparr>ksDomainTime := ksDomainTime s - 1\<rparr>)\<rbrace>
 6. \<And>cur. \<lbrace>?Q10 cur\<rbrace> get_thread_state cur \<lbrace>\<lambda>state. (if state = Structures_A.thread_state.Running then is_etcb_at cur and (\<lambda>a. etcb_at (\<lambda>t. (tcb_at cur and valid_etcbs and (tcb_at cur and valid_etcbs and (\<lambda>s. is_etcb_at cur s \<and> weak_valid_sched_action s \<and> valid_etcbs s))) a) cur a) else (\<lambda>_. True)) and (\<lambda>s. (state = Structures_A.thread_state.Running \<longrightarrow> etcb_at (\<lambda>t. (0 < tcb_time_slice t - 1 \<longrightarrow> Suc 0 < numDomains \<longrightarrow> weak_valid_sched_action s \<and> valid_etcbs s) \<and> (\<not> 0 < tcb_time_slice t - 1 \<longrightarrow> Suc 0 < numDomains \<longrightarrow> True \<and> True \<and> True \<and> valid_etcbs s)) cur s) \<and> (state \<noteq> Structures_A.thread_state.Running \<longrightarrow> Suc 0 < numDomains \<longrightarrow> ((\<lambda>_. True) and (\<lambda>a. True \<and> weak_valid_sched_action (domain_time_update (\<lambda>_. domain_time a - 1) a) \<and> valid_etcbs (domain_time_update (\<lambda>_. domain_time a - 1) a))) s))\<rbrace>
 7. \<And>cur. \<lbrace>?Q'10 cur\<rbrace> getThreadState cur \<lbrace>\<lambda>state'. (if state' = Structures_H.thread_state.Running then tcb_at' cur and (tcb_at' cur and (tcb_at' cur and (\<lambda>s. obj_at' (\<lambda>obj. if cur = cur then True else True) cur s \<and> (Invariants_H.valid_queues and (\<lambda>s. \<forall>d p. (\<exists>tcb. (inQ d p tcb \<and> runnable' (tcbState tcb)) \<and> \<not> (inQ d p (tcbTimeSlice_update (\<lambda>_. timeSlice) tcb) \<and> runnable' (tcbState (tcbTimeSlice_update (\<lambda>_. timeSlice) tcb)))) \<longrightarrow> obj_at' (\<lambda>tcb. (inQ d p tcb \<and> runnable' (tcbState tcb)) \<and> \<not> (inQ d p (tcbTimeSlice_update (\<lambda>_. timeSlice) tcb) \<and> runnable' (tcbState (tcbTimeSlice_update (\<lambda>_. timeSlice) tcb)))) cur s \<longrightarrow> cur \<notin> set (ksReadyQueues s (d, p)))) s \<and> ((\<forall>ko qdom prio. ko_at' ko cur s \<and> inQ qdom prio (tcbTimeSlice_update (\<lambda>_. timeSlice) ko) \<and> \<not> inQ qdom prio ko \<longrightarrow> cur \<in> set (ksReadyQueues s (qdom, prio))) \<and> valid_queues' s) \<and> (invs' and tcb_at' cur) s \<and> (tcb_at' cur s \<longrightarrow> (if cur = cur then obj_at' (\<lambda>tcb. runnable' (itcbState (tcb_to_itcb' (tcbTimeSlice_update (\<lambda>_. timeSlice) tcb)))) cur s else st_tcb_at' runnable' cur s))))) else (\<lambda>_. True)) and (\<lambda>s. Suc 0 < numDomains \<longrightarrow> True \<and> True \<and> (state' = Structures_H.thread_state.Running \<longrightarrow> ?Q306 cur state' s) \<and> (state' \<noteq> Structures_H.thread_state.Running \<longrightarrow> ?R308 cur state' s))\<rbrace>
 8. \<lbrace>?Q6\<rbrace> gets cur_thread \<lbrace>\<lambda>cur. tcb_at cur and ?Q10 cur\<rbrace>
 9. \<lbrace>?Q'6\<rbrace> getCurThread \<lbrace>\<lambda>cur. tcb_at' cur and ?Q'10 cur\<rbrace>
 10. \<And>s. ((\<lambda>_. True) and (cur_tcb and valid_sched)) s \<Longrightarrow> ((\<lambda>_. True) and ?Q6) s
A total of 13 subgoals... proof (prove)
goal (13 subgoals):
 1. \<And>cur state state' ts ts'. \<lbrakk>thread_state_relation state Structures_H.thread_state.Running; state' = Structures_H.thread_state.Running; ts' = 0\<rbrakk> \<Longrightarrow> \<lbrace>?P'351 cur state Structures_H.thread_state.Running ts 0 ()\<rbrace> tcbSchedAppend cur \<lbrace>\<lambda>r s. sch_act_wf (ksSchedulerAction s) s \<and> valid_queues' s \<and> sch_act_wf (ksSchedulerAction s) s\<rbrace>
 2. \<And>cur state state' ts ts'. \<lbrakk>thread_state_relation state state'; state' = Structures_H.thread_state.Running; \<not> 0 < ts'\<rbrakk> \<Longrightarrow> \<lbrace>?R311 cur state state' ts ts'\<rbrace> threadSet (tcbTimeSlice_update (\<lambda>_. timeSlice)) cur \<lbrace>\<lambda>x s. (Invariants_H.valid_queues and st_tcb_at' runnable' cur and valid_objs') s \<and> valid_objs' s \<and> ?P'351 cur state state' ts ts' x s\<rbrace>
 3. \<And>cur state state' ts. \<lbrakk>thread_state_relation state state'; state' = Structures_H.thread_state.Running\<rbrakk> \<Longrightarrow> \<lbrace>?B309 cur state state' ts\<rbrace> return (ts - 1) \<lbrace>\<lambda>ts' s. (0 < ts' \<longrightarrow> (Invariants_H.valid_queues and (\<lambda>s. \<forall>d p. (\<exists>tcb. (inQ d p tcb \<and> runnable' (tcbState tcb)) \<and> \<not> (inQ d p (tcbTimeSlice_update (\<lambda>_. ts') tcb) \<and> runnable' (tcbState (tcbTimeSlice_update (\<lambda>_. ts') tcb)))) \<longrightarrow> obj_at' (\<lambda>tcb. (inQ d p tcb \<and> runnable' (tcbState tcb)) \<and> \<not> (inQ d p (tcbTimeSlice_update (\<lambda>_. ts') tcb) \<and> runnable' (tcbState (tcbTimeSlice_update (\<lambda>_. ts') tcb)))) cur s \<longrightarrow> cur \<notin> set (ksReadyQueues s (d, p)))) s \<and> ((\<forall>ko qdom prio. ko_at' ko cur s \<and> inQ qdom prio (tcbTimeSlice_update (\<lambda>_. ts') ko) \<and> \<not> inQ qdom prio ko \<longrightarrow> cur \<in> set (ksReadyQueues s (qdom, prio))) \<and> valid_queues' s) \<and> weak_sch_act_wf (ksSchedulerAction s) s) \<and> (\<not> 0 < ts' \<longrightarrow> ?R311 cur state state' ts ts' s)\<rbrace>
 4. \<And>cur state state'. \<lbrakk>thread_state_relation state state'; state' = Structures_H.thread_state.Running\<rbrakk> \<Longrightarrow> \<lbrace>?Q306 cur state'\<rbrace> threadGet tcbTimeSlice cur \<lbrace>?B309 cur state state'\<rbrace>
 5. \<And>cur state state'. \<lbrakk>thread_state_relation state state'; state' \<noteq> Structures_H.thread_state.Running\<rbrakk> \<Longrightarrow> \<lbrace>?R308 cur state'\<rbrace> return () \<lbrace>\<lambda>rv s. Invariants_H.valid_queues (s\<lparr>ksDomainTime := ksDomainTime s - 1\<rparr>) \<and> valid_queues' (s\<lparr>ksDomainTime := ksDomainTime s - 1\<rparr>) \<and> weak_sch_act_wf (ksSchedulerAction (s\<lparr>ksDomainTime := ksDomainTime s - 1\<rparr>)) (s\<lparr>ksDomainTime := ksDomainTime s - 1\<rparr>)\<rbrace>
 6. \<And>cur. \<lbrace>?Q10 cur\<rbrace> get_thread_state cur \<lbrace>\<lambda>state. (if state = Structures_A.thread_state.Running then is_etcb_at cur and (\<lambda>a. etcb_at (\<lambda>t. (tcb_at cur and valid_etcbs and (tcb_at cur and valid_etcbs and (\<lambda>s. is_etcb_at cur s \<and> weak_valid_sched_action s \<and> valid_etcbs s))) a) cur a) else (\<lambda>_. True)) and (\<lambda>s. (state = Structures_A.thread_state.Running \<longrightarrow> etcb_at (\<lambda>t. (0 < tcb_time_slice t - 1 \<longrightarrow> Suc 0 < numDomains \<longrightarrow> weak_valid_sched_action s \<and> valid_etcbs s) \<and> (\<not> 0 < tcb_time_slice t - 1 \<longrightarrow> Suc 0 < numDomains \<longrightarrow> True \<and> True \<and> True \<and> valid_etcbs s)) cur s) \<and> (state \<noteq> Structures_A.thread_state.Running \<longrightarrow> Suc 0 < numDomains \<longrightarrow> ((\<lambda>_. True) and (\<lambda>a. True \<and> weak_valid_sched_action (domain_time_update (\<lambda>_. domain_time a - 1) a) \<and> valid_etcbs (domain_time_update (\<lambda>_. domain_time a - 1) a))) s))\<rbrace>
 7. \<And>cur. \<lbrace>?Q'10 cur\<rbrace> getThreadState cur \<lbrace>\<lambda>state'. (if state' = Structures_H.thread_state.Running then tcb_at' cur and (tcb_at' cur and (tcb_at' cur and (\<lambda>s. obj_at' (\<lambda>obj. if cur = cur then True else True) cur s \<and> (Invariants_H.valid_queues and (\<lambda>s. \<forall>d p. (\<exists>tcb. (inQ d p tcb \<and> runnable' (tcbState tcb)) \<and> \<not> (inQ d p (tcbTimeSlice_update (\<lambda>_. timeSlice) tcb) \<and> runnable' (tcbState (tcbTimeSlice_update (\<lambda>_. timeSlice) tcb)))) \<longrightarrow> obj_at' (\<lambda>tcb. (inQ d p tcb \<and> runnable' (tcbState tcb)) \<and> \<not> (inQ d p (tcbTimeSlice_update (\<lambda>_. timeSlice) tcb) \<and> runnable' (tcbState (tcbTimeSlice_update (\<lambda>_. timeSlice) tcb)))) cur s \<longrightarrow> cur \<notin> set (ksReadyQueues s (d, p)))) s \<and> ((\<forall>ko qdom prio. ko_at' ko cur s \<and> inQ qdom prio (tcbTimeSlice_update (\<lambda>_. timeSlice) ko) \<and> \<not> inQ qdom prio ko \<longrightarrow> cur \<in> set (ksReadyQueues s (qdom, prio))) \<and> valid_queues' s) \<and> (invs' and tcb_at' cur) s \<and> (tcb_at' cur s \<longrightarrow> (if cur = cur then obj_at' (\<lambda>tcb. runnable' (itcbState (tcb_to_itcb' (tcbTimeSlice_update (\<lambda>_. timeSlice) tcb)))) cur s else st_tcb_at' runnable' cur s))))) else (\<lambda>_. True)) and (\<lambda>s. Suc 0 < numDomains \<longrightarrow> True \<and> True \<and> (state' = Structures_H.thread_state.Running \<longrightarrow> ?Q306 cur state' s) \<and> (state' \<noteq> Structures_H.thread_state.Running \<longrightarrow> ?R308 cur state' s))\<rbrace>
 8. \<lbrace>?Q6\<rbrace> gets cur_thread \<lbrace>\<lambda>cur. tcb_at cur and ?Q10 cur\<rbrace>
 9. \<lbrace>?Q'6\<rbrace> getCurThread \<lbrace>\<lambda>cur. tcb_at' cur and ?Q'10 cur\<rbrace>
 10. \<And>s. ((\<lambda>_. True) and (cur_tcb and valid_sched)) s \<Longrightarrow> ((\<lambda>_. True) and ?Q6) s
A total of 13 subgoals... proof (prove)
goal (13 subgoals):
 1. \<And>cur state ts. thread_state_relation state Structures_H.thread_state.Running \<Longrightarrow> \<lbrace>?P'351 cur state Structures_H.thread_state.Running ts 0 ()\<rbrace> tcbSchedAppend cur \<lbrace>\<lambda>r s. valid_queues' s \<and> sch_act_wf (ksSchedulerAction s) s\<rbrace>
 2. \<And>cur state state' ts ts'. \<lbrakk>thread_state_relation state state'; state' = Structures_H.thread_state.Running; \<not> 0 < ts'\<rbrakk> \<Longrightarrow> \<lbrace>?R311 cur state state' ts ts'\<rbrace> threadSet (tcbTimeSlice_update (\<lambda>_. timeSlice)) cur \<lbrace>\<lambda>x s. (Invariants_H.valid_queues and st_tcb_at' runnable' cur and valid_objs') s \<and> valid_objs' s \<and> ?P'351 cur state state' ts ts' x s\<rbrace>
 3. \<And>cur state state' ts. \<lbrakk>thread_state_relation state state'; state' = Structures_H.thread_state.Running\<rbrakk> \<Longrightarrow> \<lbrace>?B309 cur state state' ts\<rbrace> return (ts - 1) \<lbrace>\<lambda>ts' s. (0 < ts' \<longrightarrow> (Invariants_H.valid_queues and (\<lambda>s. \<forall>d p. (\<exists>tcb. (inQ d p tcb \<and> runnable' (tcbState tcb)) \<and> \<not> (inQ d p (tcbTimeSlice_update (\<lambda>_. ts') tcb) \<and> runnable' (tcbState (tcbTimeSlice_update (\<lambda>_. ts') tcb)))) \<longrightarrow> obj_at' (\<lambda>tcb. (inQ d p tcb \<and> runnable' (tcbState tcb)) \<and> \<not> (inQ d p (tcbTimeSlice_update (\<lambda>_. ts') tcb) \<and> runnable' (tcbState (tcbTimeSlice_update (\<lambda>_. ts') tcb)))) cur s \<longrightarrow> cur \<notin> set (ksReadyQueues s (d, p)))) s \<and> ((\<forall>ko qdom prio. ko_at' ko cur s \<and> inQ qdom prio (tcbTimeSlice_update (\<lambda>_. ts') ko) \<and> \<not> inQ qdom prio ko \<longrightarrow> cur \<in> set (ksReadyQueues s (qdom, prio))) \<and> valid_queues' s) \<and> weak_sch_act_wf (ksSchedulerAction s) s) \<and> (\<not> 0 < ts' \<longrightarrow> ?R311 cur state state' ts ts' s)\<rbrace>
 4. \<And>cur state state'. \<lbrakk>thread_state_relation state state'; state' = Structures_H.thread_state.Running\<rbrakk> \<Longrightarrow> \<lbrace>?Q306 cur state'\<rbrace> threadGet tcbTimeSlice cur \<lbrace>?B309 cur state state'\<rbrace>
 5. \<And>cur state state'. \<lbrakk>thread_state_relation state state'; state' \<noteq> Structures_H.thread_state.Running\<rbrakk> \<Longrightarrow> \<lbrace>?R308 cur state'\<rbrace> return () \<lbrace>\<lambda>rv s. Invariants_H.valid_queues (s\<lparr>ksDomainTime := ksDomainTime s - 1\<rparr>) \<and> valid_queues' (s\<lparr>ksDomainTime := ksDomainTime s - 1\<rparr>) \<and> weak_sch_act_wf (ksSchedulerAction (s\<lparr>ksDomainTime := ksDomainTime s - 1\<rparr>)) (s\<lparr>ksDomainTime := ksDomainTime s - 1\<rparr>)\<rbrace>
 6. \<And>cur. \<lbrace>?Q10 cur\<rbrace> get_thread_state cur \<lbrace>\<lambda>state. (if state = Structures_A.thread_state.Running then is_etcb_at cur and (\<lambda>a. etcb_at (\<lambda>t. (tcb_at cur and valid_etcbs and (tcb_at cur and valid_etcbs and (\<lambda>s. is_etcb_at cur s \<and> weak_valid_sched_action s \<and> valid_etcbs s))) a) cur a) else (\<lambda>_. True)) and (\<lambda>s. (state = Structures_A.thread_state.Running \<longrightarrow> etcb_at (\<lambda>t. (0 < tcb_time_slice t - 1 \<longrightarrow> Suc 0 < numDomains \<longrightarrow> weak_valid_sched_action s \<and> valid_etcbs s) \<and> (\<not> 0 < tcb_time_slice t - 1 \<longrightarrow> Suc 0 < numDomains \<longrightarrow> True \<and> True \<and> True \<and> valid_etcbs s)) cur s) \<and> (state \<noteq> Structures_A.thread_state.Running \<longrightarrow> Suc 0 < numDomains \<longrightarrow> ((\<lambda>_. True) and (\<lambda>a. True \<and> weak_valid_sched_action (domain_time_update (\<lambda>_. domain_time a - 1) a) \<and> valid_etcbs (domain_time_update (\<lambda>_. domain_time a - 1) a))) s))\<rbrace>
 7. \<And>cur. \<lbrace>?Q'10 cur\<rbrace> getThreadState cur \<lbrace>\<lambda>state'. (if state' = Structures_H.thread_state.Running then tcb_at' cur and (tcb_at' cur and (tcb_at' cur and (\<lambda>s. obj_at' (\<lambda>obj. if cur = cur then True else True) cur s \<and> (Invariants_H.valid_queues and (\<lambda>s. \<forall>d p. (\<exists>tcb. (inQ d p tcb \<and> runnable' (tcbState tcb)) \<and> \<not> (inQ d p (tcbTimeSlice_update (\<lambda>_. timeSlice) tcb) \<and> runnable' (tcbState (tcbTimeSlice_update (\<lambda>_. timeSlice) tcb)))) \<longrightarrow> obj_at' (\<lambda>tcb. (inQ d p tcb \<and> runnable' (tcbState tcb)) \<and> \<not> (inQ d p (tcbTimeSlice_update (\<lambda>_. timeSlice) tcb) \<and> runnable' (tcbState (tcbTimeSlice_update (\<lambda>_. timeSlice) tcb)))) cur s \<longrightarrow> cur \<notin> set (ksReadyQueues s (d, p)))) s \<and> ((\<forall>ko qdom prio. ko_at' ko cur s \<and> inQ qdom prio (tcbTimeSlice_update (\<lambda>_. timeSlice) ko) \<and> \<not> inQ qdom prio ko \<longrightarrow> cur \<in> set (ksReadyQueues s (qdom, prio))) \<and> valid_queues' s) \<and> (invs' and tcb_at' cur) s \<and> (tcb_at' cur s \<longrightarrow> (if cur = cur then obj_at' (\<lambda>tcb. runnable' (itcbState (tcb_to_itcb' (tcbTimeSlice_update (\<lambda>_. timeSlice) tcb)))) cur s else st_tcb_at' runnable' cur s))))) else (\<lambda>_. True)) and (\<lambda>s. Suc 0 < numDomains \<longrightarrow> True \<and> True \<and> (state' = Structures_H.thread_state.Running \<longrightarrow> ?Q306 cur state' s) \<and> (state' \<noteq> Structures_H.thread_state.Running \<longrightarrow> ?R308 cur state' s))\<rbrace>
 8. \<lbrace>?Q6\<rbrace> gets cur_thread \<lbrace>\<lambda>cur. tcb_at cur and ?Q10 cur\<rbrace>
 9. \<lbrace>?Q'6\<rbrace> getCurThread \<lbrace>\<lambda>cur. tcb_at' cur and ?Q'10 cur\<rbrace>
 10. \<And>s. ((\<lambda>_. True) and (cur_tcb and valid_sched)) s \<Longrightarrow> ((\<lambda>_. True) and ?Q6) s
A total of 13 subgoals... proof (prove)
goal (12 subgoals):
 1. \<And>cur state state' ts ts'. \<lbrakk>thread_state_relation state state'; state' = Structures_H.thread_state.Running; \<not> 0 < ts'\<rbrakk> \<Longrightarrow> \<lbrace>?R311 cur state state' ts ts'\<rbrace> threadSet (tcbTimeSlice_update (\<lambda>_. timeSlice)) cur \<lbrace>\<lambda>x s. (Invariants_H.valid_queues and st_tcb_at' runnable' cur and valid_objs') s \<and> valid_objs' s \<and> (valid_queues' and tcb_at' cur) s \<and> sch_act_wf (ksSchedulerAction s) s\<rbrace>
 2. \<And>cur state state' ts. \<lbrakk>thread_state_relation state state'; state' = Structures_H.thread_state.Running\<rbrakk> \<Longrightarrow> \<lbrace>?B309 cur state state' ts\<rbrace> return (ts - 1) \<lbrace>\<lambda>ts' s. (0 < ts' \<longrightarrow> (Invariants_H.valid_queues and (\<lambda>s. \<forall>d p. (\<exists>tcb. (inQ d p tcb \<and> runnable' (tcbState tcb)) \<and> \<not> (inQ d p (tcbTimeSlice_update (\<lambda>_. ts') tcb) \<and> runnable' (tcbState (tcbTimeSlice_update (\<lambda>_. ts') tcb)))) \<longrightarrow> obj_at' (\<lambda>tcb. (inQ d p tcb \<and> runnable' (tcbState tcb)) \<and> \<not> (inQ d p (tcbTimeSlice_update (\<lambda>_. ts') tcb) \<and> runnable' (tcbState (tcbTimeSlice_update (\<lambda>_. ts') tcb)))) cur s \<longrightarrow> cur \<notin> set (ksReadyQueues s (d, p)))) s \<and> ((\<forall>ko qdom prio. ko_at' ko cur s \<and> inQ qdom prio (tcbTimeSlice_update (\<lambda>_. ts') ko) \<and> \<not> inQ qdom prio ko \<longrightarrow> cur \<in> set (ksReadyQueues s (qdom, prio))) \<and> valid_queues' s) \<and> weak_sch_act_wf (ksSchedulerAction s) s) \<and> (\<not> 0 < ts' \<longrightarrow> ?R311 cur state state' ts ts' s)\<rbrace>
 3. \<And>cur state state'. \<lbrakk>thread_state_relation state state'; state' = Structures_H.thread_state.Running\<rbrakk> \<Longrightarrow> \<lbrace>?Q306 cur state'\<rbrace> threadGet tcbTimeSlice cur \<lbrace>?B309 cur state state'\<rbrace>
 4. \<And>cur state state'. \<lbrakk>thread_state_relation state state'; state' \<noteq> Structures_H.thread_state.Running\<rbrakk> \<Longrightarrow> \<lbrace>?R308 cur state'\<rbrace> return () \<lbrace>\<lambda>rv s. Invariants_H.valid_queues (s\<lparr>ksDomainTime := ksDomainTime s - 1\<rparr>) \<and> valid_queues' (s\<lparr>ksDomainTime := ksDomainTime s - 1\<rparr>) \<and> weak_sch_act_wf (ksSchedulerAction (s\<lparr>ksDomainTime := ksDomainTime s - 1\<rparr>)) (s\<lparr>ksDomainTime := ksDomainTime s - 1\<rparr>)\<rbrace>
 5. \<And>cur. \<lbrace>?Q10 cur\<rbrace> get_thread_state cur \<lbrace>\<lambda>state. (if state = Structures_A.thread_state.Running then is_etcb_at cur and (\<lambda>a. etcb_at (\<lambda>t. (tcb_at cur and valid_etcbs and (tcb_at cur and valid_etcbs and (\<lambda>s. is_etcb_at cur s \<and> weak_valid_sched_action s \<and> valid_etcbs s))) a) cur a) else (\<lambda>_. True)) and (\<lambda>s. (state = Structures_A.thread_state.Running \<longrightarrow> etcb_at (\<lambda>t. (0 < tcb_time_slice t - 1 \<longrightarrow> Suc 0 < numDomains \<longrightarrow> weak_valid_sched_action s \<and> valid_etcbs s) \<and> (\<not> 0 < tcb_time_slice t - 1 \<longrightarrow> Suc 0 < numDomains \<longrightarrow> True \<and> True \<and> True \<and> valid_etcbs s)) cur s) \<and> (state \<noteq> Structures_A.thread_state.Running \<longrightarrow> Suc 0 < numDomains \<longrightarrow> ((\<lambda>_. True) and (\<lambda>a. True \<and> weak_valid_sched_action (domain_time_update (\<lambda>_. domain_time a - 1) a) \<and> valid_etcbs (domain_time_update (\<lambda>_. domain_time a - 1) a))) s))\<rbrace>
 6. \<And>cur. \<lbrace>?Q'10 cur\<rbrace> getThreadState cur \<lbrace>\<lambda>state'. (if state' = Structures_H.thread_state.Running then tcb_at' cur and (tcb_at' cur and (tcb_at' cur and (\<lambda>s. obj_at' (\<lambda>obj. if cur = cur then True else True) cur s \<and> (Invariants_H.valid_queues and (\<lambda>s. \<forall>d p. (\<exists>tcb. (inQ d p tcb \<and> runnable' (tcbState tcb)) \<and> \<not> (inQ d p (tcbTimeSlice_update (\<lambda>_. timeSlice) tcb) \<and> runnable' (tcbState (tcbTimeSlice_update (\<lambda>_. timeSlice) tcb)))) \<longrightarrow> obj_at' (\<lambda>tcb. (inQ d p tcb \<and> runnable' (tcbState tcb)) \<and> \<not> (inQ d p (tcbTimeSlice_update (\<lambda>_. timeSlice) tcb) \<and> runnable' (tcbState (tcbTimeSlice_update (\<lambda>_. timeSlice) tcb)))) cur s \<longrightarrow> cur \<notin> set (ksReadyQueues s (d, p)))) s \<and> ((\<forall>ko qdom prio. ko_at' ko cur s \<and> inQ qdom prio (tcbTimeSlice_update (\<lambda>_. timeSlice) ko) \<and> \<not> inQ qdom prio ko \<longrightarrow> cur \<in> set (ksReadyQueues s (qdom, prio))) \<and> valid_queues' s) \<and> (invs' and tcb_at' cur) s \<and> (tcb_at' cur s \<longrightarrow> (if cur = cur then obj_at' (\<lambda>tcb. runnable' (itcbState (tcb_to_itcb' (tcbTimeSlice_update (\<lambda>_. timeSlice) tcb)))) cur s else st_tcb_at' runnable' cur s))))) else (\<lambda>_. True)) and (\<lambda>s. Suc 0 < numDomains \<longrightarrow> True \<and> True \<and> (state' = Structures_H.thread_state.Running \<longrightarrow> ?Q306 cur state' s) \<and> (state' \<noteq> Structures_H.thread_state.Running \<longrightarrow> ?R308 cur state' s))\<rbrace>
 7. \<lbrace>?Q6\<rbrace> gets cur_thread \<lbrace>\<lambda>cur. tcb_at cur and ?Q10 cur\<rbrace>
 8. \<lbrace>?Q'6\<rbrace> getCurThread \<lbrace>\<lambda>cur. tcb_at' cur and ?Q'10 cur\<rbrace>
 9. \<And>s. ((\<lambda>_. True) and (cur_tcb and valid_sched)) s \<Longrightarrow> ((\<lambda>_. True) and ?Q6) s
 10. \<And>s. ((\<lambda>_. True) and invs') s \<Longrightarrow> ((\<lambda>_. True) and ?Q'6) s
A total of 12 subgoals... proof (prove)
goal (12 subgoals):
 1. \<And>cur state state' ts ts'. \<lbrakk>thread_state_relation state Structures_H.thread_state.Running; state' = Structures_H.thread_state.Running; ts' = 0\<rbrakk> \<Longrightarrow> \<lbrace>?R311 cur state Structures_H.thread_state.Running ts 0\<rbrace> threadSet (tcbTimeSlice_update (\<lambda>_. timeSlice)) cur \<lbrace>\<lambda>x s. Invariants_H.valid_queues s \<and> st_tcb_at' runnable' cur s \<and> valid_objs' s \<and> valid_queues' s \<and> tcb_at' cur s \<and> sch_act_wf (ksSchedulerAction s) s\<rbrace>
 2. \<And>cur state state' ts. \<lbrakk>thread_state_relation state state'; state' = Structures_H.thread_state.Running\<rbrakk> \<Longrightarrow> \<lbrace>?B309 cur state state' ts\<rbrace> return (ts - 1) \<lbrace>\<lambda>ts' s. (0 < ts' \<longrightarrow> (Invariants_H.valid_queues and (\<lambda>s. \<forall>d p. (\<exists>tcb. (inQ d p tcb \<and> runnable' (tcbState tcb)) \<and> \<not> (inQ d p (tcbTimeSlice_update (\<lambda>_. ts') tcb) \<and> runnable' (tcbState (tcbTimeSlice_update (\<lambda>_. ts') tcb)))) \<longrightarrow> obj_at' (\<lambda>tcb. (inQ d p tcb \<and> runnable' (tcbState tcb)) \<and> \<not> (inQ d p (tcbTimeSlice_update (\<lambda>_. ts') tcb) \<and> runnable' (tcbState (tcbTimeSlice_update (\<lambda>_. ts') tcb)))) cur s \<longrightarrow> cur \<notin> set (ksReadyQueues s (d, p)))) s \<and> ((\<forall>ko qdom prio. ko_at' ko cur s \<and> inQ qdom prio (tcbTimeSlice_update (\<lambda>_. ts') ko) \<and> \<not> inQ qdom prio ko \<longrightarrow> cur \<in> set (ksReadyQueues s (qdom, prio))) \<and> valid_queues' s) \<and> weak_sch_act_wf (ksSchedulerAction s) s) \<and> (\<not> 0 < ts' \<longrightarrow> ?R311 cur state state' ts ts' s)\<rbrace>
 3. \<And>cur state state'. \<lbrakk>thread_state_relation state state'; state' = Structures_H.thread_state.Running\<rbrakk> \<Longrightarrow> \<lbrace>?Q306 cur state'\<rbrace> threadGet tcbTimeSlice cur \<lbrace>?B309 cur state state'\<rbrace>
 4. \<And>cur state state'. \<lbrakk>thread_state_relation state state'; state' \<noteq> Structures_H.thread_state.Running\<rbrakk> \<Longrightarrow> \<lbrace>?R308 cur state'\<rbrace> return () \<lbrace>\<lambda>rv s. Invariants_H.valid_queues (s\<lparr>ksDomainTime := ksDomainTime s - 1\<rparr>) \<and> valid_queues' (s\<lparr>ksDomainTime := ksDomainTime s - 1\<rparr>) \<and> weak_sch_act_wf (ksSchedulerAction (s\<lparr>ksDomainTime := ksDomainTime s - 1\<rparr>)) (s\<lparr>ksDomainTime := ksDomainTime s - 1\<rparr>)\<rbrace>
 5. \<And>cur. \<lbrace>?Q10 cur\<rbrace> get_thread_state cur \<lbrace>\<lambda>state. (if state = Structures_A.thread_state.Running then is_etcb_at cur and (\<lambda>a. etcb_at (\<lambda>t. (tcb_at cur and valid_etcbs and (tcb_at cur and valid_etcbs and (\<lambda>s. is_etcb_at cur s \<and> weak_valid_sched_action s \<and> valid_etcbs s))) a) cur a) else (\<lambda>_. True)) and (\<lambda>s. (state = Structures_A.thread_state.Running \<longrightarrow> etcb_at (\<lambda>t. (0 < tcb_time_slice t - 1 \<longrightarrow> Suc 0 < numDomains \<longrightarrow> weak_valid_sched_action s \<and> valid_etcbs s) \<and> (\<not> 0 < tcb_time_slice t - 1 \<longrightarrow> Suc 0 < numDomains \<longrightarrow> True \<and> True \<and> True \<and> valid_etcbs s)) cur s) \<and> (state \<noteq> Structures_A.thread_state.Running \<longrightarrow> Suc 0 < numDomains \<longrightarrow> ((\<lambda>_. True) and (\<lambda>a. True \<and> weak_valid_sched_action (domain_time_update (\<lambda>_. domain_time a - 1) a) \<and> valid_etcbs (domain_time_update (\<lambda>_. domain_time a - 1) a))) s))\<rbrace>
 6. \<And>cur. \<lbrace>?Q'10 cur\<rbrace> getThreadState cur \<lbrace>\<lambda>state'. (if state' = Structures_H.thread_state.Running then tcb_at' cur and (tcb_at' cur and (tcb_at' cur and (\<lambda>s. obj_at' (\<lambda>obj. if cur = cur then True else True) cur s \<and> (Invariants_H.valid_queues and (\<lambda>s. \<forall>d p. (\<exists>tcb. (inQ d p tcb \<and> runnable' (tcbState tcb)) \<and> \<not> (inQ d p (tcbTimeSlice_update (\<lambda>_. timeSlice) tcb) \<and> runnable' (tcbState (tcbTimeSlice_update (\<lambda>_. timeSlice) tcb)))) \<longrightarrow> obj_at' (\<lambda>tcb. (inQ d p tcb \<and> runnable' (tcbState tcb)) \<and> \<not> (inQ d p (tcbTimeSlice_update (\<lambda>_. timeSlice) tcb) \<and> runnable' (tcbState (tcbTimeSlice_update (\<lambda>_. timeSlice) tcb)))) cur s \<longrightarrow> cur \<notin> set (ksReadyQueues s (d, p)))) s \<and> ((\<forall>ko qdom prio. ko_at' ko cur s \<and> inQ qdom prio (tcbTimeSlice_update (\<lambda>_. timeSlice) ko) \<and> \<not> inQ qdom prio ko \<longrightarrow> cur \<in> set (ksReadyQueues s (qdom, prio))) \<and> valid_queues' s) \<and> (invs' and tcb_at' cur) s \<and> (tcb_at' cur s \<longrightarrow> (if cur = cur then obj_at' (\<lambda>tcb. runnable' (itcbState (tcb_to_itcb' (tcbTimeSlice_update (\<lambda>_. timeSlice) tcb)))) cur s else st_tcb_at' runnable' cur s))))) else (\<lambda>_. True)) and (\<lambda>s. Suc 0 < numDomains \<longrightarrow> True \<and> True \<and> (state' = Structures_H.thread_state.Running \<longrightarrow> ?Q306 cur state' s) \<and> (state' \<noteq> Structures_H.thread_state.Running \<longrightarrow> ?R308 cur state' s))\<rbrace>
 7. \<lbrace>?Q6\<rbrace> gets cur_thread \<lbrace>\<lambda>cur. tcb_at cur and ?Q10 cur\<rbrace>
 8. \<lbrace>?Q'6\<rbrace> getCurThread \<lbrace>\<lambda>cur. tcb_at' cur and ?Q'10 cur\<rbrace>
 9. \<And>s. ((\<lambda>_. True) and (cur_tcb and valid_sched)) s \<Longrightarrow> ((\<lambda>_. True) and ?Q6) s
 10. \<And>s. ((\<lambda>_. True) and invs') s \<Longrightarrow> ((\<lambda>_. True) and ?Q'6) s
A total of 12 subgoals... proof (prove)
goal (10 subgoals):
 1. \<And>cur state state'. \<lbrakk>thread_state_relation state Structures_H.thread_state.Running; state' = Structures_H.thread_state.Running\<rbrakk> \<Longrightarrow> \<lbrace>?Q306 cur Structures_H.thread_state.Running\<rbrace> threadGet tcbTimeSlice cur \<lbrace>\<lambda>ts a. (Suc 0 < ts \<longrightarrow> Invariants_H.valid_queues a \<and> (\<forall>d p. (\<exists>tcb. inQ d p tcb \<and> runnable' (tcbState tcb) \<and> (inQ d p (tcbTimeSlice_update (\<lambda>_. ts - Suc 0) tcb) \<longrightarrow> \<not> runnable' (tcbState tcb))) \<longrightarrow> obj_at' (\<lambda>tcb. inQ d p tcb \<and> runnable' (tcbState tcb) \<and> (inQ d p (tcbTimeSlice_update (\<lambda>_. ts - Suc 0) tcb) \<longrightarrow> \<not> runnable' (tcbState tcb))) cur a \<longrightarrow> cur \<notin> set (ksReadyQueues a (d, p))) \<and> (\<forall>ko qdom prio. ko_at' ko cur a \<and> inQ qdom prio (tcbTimeSlice_update (\<lambda>_. ts - Suc 0) ko) \<and> \<not> inQ qdom prio ko \<longrightarrow> cur \<in> set (ksReadyQueues a (qdom, prio))) \<and> valid_queues' a \<and> weak_sch_act_wf (ksSchedulerAction a) a) \<and> (\<not> Suc 0 < ts \<longrightarrow> Invariants_H.valid_queues a \<and> (\<forall>d p. (\<exists>tcb. inQ d p tcb \<and> runnable' (tcbState tcb) \<and> (inQ d p (tcbTimeSlice_update (\<lambda>_. timeSlice) tcb) \<longrightarrow> \<not> runnable' (tcbState tcb))) \<longrightarrow> obj_at' (\<lambda>tcb. inQ d p tcb \<and> runnable' (tcbState tcb) \<and> (inQ d p (tcbTimeSlice_update (\<lambda>_. timeSlice) tcb) \<longrightarrow> \<not> runnable' (tcbState tcb))) cur a \<longrightarrow> cur \<notin> set (ksReadyQueues a (d, p))) \<and> (tcb_at' cur a \<longrightarrow> obj_at' (\<lambda>tcb. runnable' (tcbState tcb)) cur a) \<and> valid_objs' a \<and> (\<forall>ko qdom prio. ko_at' ko cur a \<and> inQ qdom prio (tcbTimeSlice_update (\<lambda>_. timeSlice) ko) \<and> \<not> inQ qdom prio ko \<longrightarrow> cur \<in> set (ksReadyQueues a (qdom, prio))) \<and> valid_queues' a \<and> tcb_at' cur a \<and> sch_act_wf (ksSchedulerAction a) a)\<rbrace>
 2. \<And>cur state state'. \<lbrakk>thread_state_relation state state'; state' \<noteq> Structures_H.thread_state.Running\<rbrakk> \<Longrightarrow> \<lbrace>?R308 cur state'\<rbrace> return () \<lbrace>\<lambda>rv s. Invariants_H.valid_queues (s\<lparr>ksDomainTime := ksDomainTime s - 1\<rparr>) \<and> valid_queues' (s\<lparr>ksDomainTime := ksDomainTime s - 1\<rparr>) \<and> weak_sch_act_wf (ksSchedulerAction (s\<lparr>ksDomainTime := ksDomainTime s - 1\<rparr>)) (s\<lparr>ksDomainTime := ksDomainTime s - 1\<rparr>)\<rbrace>
 3. \<And>cur. \<lbrace>?Q10 cur\<rbrace> get_thread_state cur \<lbrace>\<lambda>state. (if state = Structures_A.thread_state.Running then is_etcb_at cur and (\<lambda>a. etcb_at (\<lambda>t. (tcb_at cur and valid_etcbs and (tcb_at cur and valid_etcbs and (\<lambda>s. is_etcb_at cur s \<and> weak_valid_sched_action s \<and> valid_etcbs s))) a) cur a) else (\<lambda>_. True)) and (\<lambda>s. (state = Structures_A.thread_state.Running \<longrightarrow> etcb_at (\<lambda>t. (0 < tcb_time_slice t - 1 \<longrightarrow> Suc 0 < numDomains \<longrightarrow> weak_valid_sched_action s \<and> valid_etcbs s) \<and> (\<not> 0 < tcb_time_slice t - 1 \<longrightarrow> Suc 0 < numDomains \<longrightarrow> True \<and> True \<and> True \<and> valid_etcbs s)) cur s) \<and> (state \<noteq> Structures_A.thread_state.Running \<longrightarrow> Suc 0 < numDomains \<longrightarrow> ((\<lambda>_. True) and (\<lambda>a. True \<and> weak_valid_sched_action (domain_time_update (\<lambda>_. domain_time a - 1) a) \<and> valid_etcbs (domain_time_update (\<lambda>_. domain_time a - 1) a))) s))\<rbrace>
 4. \<And>cur. \<lbrace>?Q'10 cur\<rbrace> getThreadState cur \<lbrace>\<lambda>state'. (if state' = Structures_H.thread_state.Running then tcb_at' cur and (tcb_at' cur and (tcb_at' cur and (\<lambda>s. obj_at' (\<lambda>obj. if cur = cur then True else True) cur s \<and> (Invariants_H.valid_queues and (\<lambda>s. \<forall>d p. (\<exists>tcb. (inQ d p tcb \<and> runnable' (tcbState tcb)) \<and> \<not> (inQ d p (tcbTimeSlice_update (\<lambda>_. timeSlice) tcb) \<and> runnable' (tcbState (tcbTimeSlice_update (\<lambda>_. timeSlice) tcb)))) \<longrightarrow> obj_at' (\<lambda>tcb. (inQ d p tcb \<and> runnable' (tcbState tcb)) \<and> \<not> (inQ d p (tcbTimeSlice_update (\<lambda>_. timeSlice) tcb) \<and> runnable' (tcbState (tcbTimeSlice_update (\<lambda>_. timeSlice) tcb)))) cur s \<longrightarrow> cur \<notin> set (ksReadyQueues s (d, p)))) s \<and> ((\<forall>ko qdom prio. ko_at' ko cur s \<and> inQ qdom prio (tcbTimeSlice_update (\<lambda>_. timeSlice) ko) \<and> \<not> inQ qdom prio ko \<longrightarrow> cur \<in> set (ksReadyQueues s (qdom, prio))) \<and> valid_queues' s) \<and> (invs' and tcb_at' cur) s \<and> (tcb_at' cur s \<longrightarrow> (if cur = cur then obj_at' (\<lambda>tcb. runnable' (itcbState (tcb_to_itcb' (tcbTimeSlice_update (\<lambda>_. timeSlice) tcb)))) cur s else st_tcb_at' runnable' cur s))))) else (\<lambda>_. True)) and (\<lambda>s. Suc 0 < numDomains \<longrightarrow> True \<and> True \<and> (state' = Structures_H.thread_state.Running \<longrightarrow> ?Q306 cur state' s) \<and> (state' \<noteq> Structures_H.thread_state.Running \<longrightarrow> ?R308 cur state' s))\<rbrace>
 5. \<lbrace>?Q6\<rbrace> gets cur_thread \<lbrace>\<lambda>cur. tcb_at cur and ?Q10 cur\<rbrace>
 6. \<lbrace>?Q'6\<rbrace> getCurThread \<lbrace>\<lambda>cur. tcb_at' cur and ?Q'10 cur\<rbrace>
 7. \<And>s. ((\<lambda>_. True) and (cur_tcb and valid_sched)) s \<Longrightarrow> ((\<lambda>_. True) and ?Q6) s
 8. \<And>s. ((\<lambda>_. True) and invs') s \<Longrightarrow> ((\<lambda>_. True) and ?Q'6) s
 9. \<And>s. (cur_tcb and valid_sched) s \<Longrightarrow> ((\<lambda>_. True) and (cur_tcb and valid_sched)) s
 10. \<And>s. invs' s \<Longrightarrow> ((\<lambda>_. True) and invs') s proof (prove)
goal (4 subgoals):
 1. \<And>s. ((\<lambda>_. True) and (cur_tcb and valid_sched)) s \<Longrightarrow> ((\<lambda>_. True) and (\<lambda>s. (tcb_at (cur_thread s) and (\<lambda>sa. \<forall>st. st_tcb_at ((=) st) (cur_thread s) sa \<longrightarrow> ((if st = Structures_A.thread_state.Running then is_etcb_at (cur_thread s) and (\<lambda>a. etcb_at (\<lambda>t. (tcb_at (cur_thread s) and valid_etcbs and (tcb_at (cur_thread s) and valid_etcbs and (\<lambda>sa. is_etcb_at (cur_thread s) sa \<and> weak_valid_sched_action sa \<and> valid_etcbs sa))) a) (cur_thread s) a) else (\<lambda>_. True)) and (\<lambda>sa. (st = Structures_A.thread_state.Running \<longrightarrow> etcb_at (\<lambda>t. (0 < tcb_time_slice t - 1 \<longrightarrow> Suc 0 < numDomains \<longrightarrow> weak_valid_sched_action sa \<and> valid_etcbs sa) \<and> (\<not> 0 < tcb_time_slice t - 1 \<longrightarrow> Suc 0 < numDomains \<longrightarrow> True \<and> True \<and> True \<and> valid_etcbs sa)) (cur_thread s) sa) \<and> (st \<noteq> Structures_A.thread_state.Running \<longrightarrow> Suc 0 < numDomains \<longrightarrow> ((\<lambda>_. True) and (\<lambda>a. True \<and> weak_valid_sched_action (domain_time_update (\<lambda>_. domain_time a - 1) a) \<and> valid_etcbs (domain_time_update (\<lambda>_. domain_time a - 1) a))) sa))) sa)) s)) s
 2. \<And>s. ((\<lambda>_. True) and invs') s \<Longrightarrow> ((\<lambda>_. True) and (\<lambda>s. (tcb_at' (ksCurThread s) and (\<lambda>sa. \<forall>st. st_tcb_at' ((=) st) (ksCurThread s) sa \<longrightarrow> ((if st = Structures_H.thread_state.Running then tcb_at' (ksCurThread s) and (tcb_at' (ksCurThread s) and (tcb_at' (ksCurThread s) and (\<lambda>sa. obj_at' (\<lambda>obj. if ksCurThread s = ksCurThread s then True else True) (ksCurThread s) sa \<and> (Invariants_H.valid_queues and (\<lambda>sa. \<forall>d p. (\<exists>tcb. (inQ d p tcb \<and> runnable' (tcbState tcb)) \<and> \<not> (inQ d p (tcbTimeSlice_update (\<lambda>_. timeSlice) tcb) \<and> runnable' (tcbState (tcbTimeSlice_update (\<lambda>_. timeSlice) tcb)))) \<longrightarrow> obj_at' (\<lambda>tcb. (inQ d p tcb \<and> runnable' (tcbState tcb)) \<and> \<not> (inQ d p (tcbTimeSlice_update (\<lambda>_. timeSlice) tcb) \<and> runnable' (tcbState (tcbTimeSlice_update (\<lambda>_. timeSlice) tcb)))) (ksCurThread s) sa \<longrightarrow> ksCurThread s \<notin> set (ksReadyQueues sa (d, p)))) sa \<and> ((\<forall>ko qdom prio. ko_at' ko (ksCurThread s) sa \<and> inQ qdom prio (tcbTimeSlice_update (\<lambda>_. timeSlice) ko) \<and> \<not> inQ qdom prio ko \<longrightarrow> ksCurThread s \<in> set (ksReadyQueues sa (qdom, prio))) \<and> valid_queues' sa) \<and> (invs' and tcb_at' (ksCurThread s)) sa \<and> (tcb_at' (ksCurThread s) sa \<longrightarrow> (if ksCurThread s = ksCurThread s then obj_at' (\<lambda>tcb. runnable' (itcbState (tcb_to_itcb' (tcbTimeSlice_update (\<lambda>_. timeSlice) tcb)))) (ksCurThread s) sa else st_tcb_at' runnable' (ksCurThread s) sa))))) else (\<lambda>_. True)) and (\<lambda>sa. Suc 0 < numDomains \<longrightarrow> True \<and> True \<and> (st = Structures_H.thread_state.Running \<longrightarrow> tcb_at' (ksCurThread s) sa \<longrightarrow> (\<exists>tcb. ko_at' tcb (ksCurThread s) sa \<and> (Suc 0 < tcbTimeSlice tcb \<longrightarrow> Invariants_H.valid_queues sa \<and> (\<forall>d p. (\<exists>tcba. inQ d p tcba \<and> runnable' (tcbState tcba) \<and> (inQ d p (tcbTimeSlice_update (\<lambda>_. tcbTimeSlice tcb - Suc 0) tcba) \<longrightarrow> \<not> runnable' (tcbState tcba))) \<longrightarrow> obj_at' (\<lambda>tcba. inQ d p tcba \<and> runnable' (tcbState tcba) \<and> (inQ d p (tcbTimeSlice_update (\<lambda>_. tcbTimeSlice tcb - Suc 0) tcba) \<longrightarrow> \<not> runnable' (tcbState tcba))) (ksCurThread s) sa \<longrightarrow> ksCurThread s \<notin> set (ksReadyQueues sa (d, p))) \<and> (\<forall>ko qdom prio. ko_at' ko (ksCurThread s) sa \<and> inQ qdom prio (tcbTimeSlice_update (\<lambda>_. tcbTimeSlice tcb - Suc 0) ko) \<and> \<not> inQ qdom prio ko \<longrightarrow> ksCurThread s \<in> set (ksReadyQueues sa (qdom, prio))) \<and> valid_queues' sa \<and> weak_sch_act_wf (ksSchedulerAction sa) sa) \<and> (\<not> Suc 0 < tcbTimeSlice tcb \<longrightarrow> Invariants_H.valid_queues sa \<and> (\<forall>d p. (\<exists>tcb. inQ d p tcb \<and> runnable' (tcbState tcb) \<and> (inQ d p (tcbTimeSlice_update (\<lambda>_. timeSlice) tcb) \<longrightarrow> \<not> runnable' (tcbState tcb))) \<longrightarrow> obj_at' (\<lambda>tcb. inQ d p tcb \<and> runnable' (tcbState tcb) \<and> (inQ d p (tcbTimeSlice_update (\<lambda>_. timeSlice) tcb) \<longrightarrow> \<not> runnable' (tcbState tcb))) (ksCurThread s) sa \<longrightarrow> ksCurThread s \<notin> set (ksReadyQueues sa (d, p))) \<and> (tcb_at' (ksCurThread s) sa \<longrightarrow> obj_at' (\<lambda>tcb. runnable' (tcbState tcb)) (ksCurThread s) sa) \<and> valid_objs' sa \<and> (\<forall>ko qdom prio. ko_at' ko (ksCurThread s) sa \<and> inQ qdom prio (tcbTimeSlice_update (\<lambda>_. timeSlice) ko) \<and> \<not> inQ qdom prio ko \<longrightarrow> ksCurThread s \<in> set (ksReadyQueues sa (qdom, prio))) \<and> valid_queues' sa \<and> tcb_at' (ksCurThread s) sa \<and> sch_act_wf (ksSchedulerAction sa) sa))) \<and> (st \<noteq> Structures_H.thread_state.Running \<longrightarrow> Invariants_H.valid_queues (sa\<lparr>ksDomainTime := ksDomainTime sa - 1\<rparr>) \<and> valid_queues' (sa\<lparr>ksDomainTime := ksDomainTime sa - 1\<rparr>) \<and> weak_sch_act_wf (ksSchedulerAction (sa\<lparr>ksDomainTime := ksDomainTime sa - 1\<rparr>)) (sa\<lparr>ksDomainTime := ksDomainTime sa - 1\<rparr>)))) sa)) s)) s
 3. \<And>s. (cur_tcb and valid_sched) s \<Longrightarrow> ((\<lambda>_. True) and (cur_tcb and valid_sched)) s
 4. \<And>s. invs' s \<Longrightarrow> ((\<lambda>_. True) and invs') s proof (prove)
goal (3 subgoals):
 1. \<And>s. ((\<lambda>_. True) and invs') s \<Longrightarrow> ((\<lambda>_. True) and (\<lambda>s. (tcb_at' (ksCurThread s) and (\<lambda>sa. \<forall>st. st_tcb_at' ((=) st) (ksCurThread s) sa \<longrightarrow> ((if st = Structures_H.thread_state.Running then tcb_at' (ksCurThread s) and (tcb_at' (ksCurThread s) and (tcb_at' (ksCurThread s) and (\<lambda>sa. obj_at' (\<lambda>obj. if ksCurThread s = ksCurThread s then True else True) (ksCurThread s) sa \<and> (Invariants_H.valid_queues and (\<lambda>sa. \<forall>d p. (\<exists>tcb. (inQ d p tcb \<and> runnable' (tcbState tcb)) \<and> \<not> (inQ d p (tcbTimeSlice_update (\<lambda>_. timeSlice) tcb) \<and> runnable' (tcbState (tcbTimeSlice_update (\<lambda>_. timeSlice) tcb)))) \<longrightarrow> obj_at' (\<lambda>tcb. (inQ d p tcb \<and> runnable' (tcbState tcb)) \<and> \<not> (inQ d p (tcbTimeSlice_update (\<lambda>_. timeSlice) tcb) \<and> runnable' (tcbState (tcbTimeSlice_update (\<lambda>_. timeSlice) tcb)))) (ksCurThread s) sa \<longrightarrow> ksCurThread s \<notin> set (ksReadyQueues sa (d, p)))) sa \<and> ((\<forall>ko qdom prio. ko_at' ko (ksCurThread s) sa \<and> inQ qdom prio (tcbTimeSlice_update (\<lambda>_. timeSlice) ko) \<and> \<not> inQ qdom prio ko \<longrightarrow> ksCurThread s \<in> set (ksReadyQueues sa (qdom, prio))) \<and> valid_queues' sa) \<and> (invs' and tcb_at' (ksCurThread s)) sa \<and> (tcb_at' (ksCurThread s) sa \<longrightarrow> (if ksCurThread s = ksCurThread s then obj_at' (\<lambda>tcb. runnable' (itcbState (tcb_to_itcb' (tcbTimeSlice_update (\<lambda>_. timeSlice) tcb)))) (ksCurThread s) sa else st_tcb_at' runnable' (ksCurThread s) sa))))) else (\<lambda>_. True)) and (\<lambda>sa. Suc 0 < numDomains \<longrightarrow> True \<and> True \<and> (st = Structures_H.thread_state.Running \<longrightarrow> tcb_at' (ksCurThread s) sa \<longrightarrow> (\<exists>tcb. ko_at' tcb (ksCurThread s) sa \<and> (Suc 0 < tcbTimeSlice tcb \<longrightarrow> Invariants_H.valid_queues sa \<and> (\<forall>d p. (\<exists>tcba. inQ d p tcba \<and> runnable' (tcbState tcba) \<and> (inQ d p (tcbTimeSlice_update (\<lambda>_. tcbTimeSlice tcb - Suc 0) tcba) \<longrightarrow> \<not> runnable' (tcbState tcba))) \<longrightarrow> obj_at' (\<lambda>tcba. inQ d p tcba \<and> runnable' (tcbState tcba) \<and> (inQ d p (tcbTimeSlice_update (\<lambda>_. tcbTimeSlice tcb - Suc 0) tcba) \<longrightarrow> \<not> runnable' (tcbState tcba))) (ksCurThread s) sa \<longrightarrow> ksCurThread s \<notin> set (ksReadyQueues sa (d, p))) \<and> (\<forall>ko qdom prio. ko_at' ko (ksCurThread s) sa \<and> inQ qdom prio (tcbTimeSlice_update (\<lambda>_. tcbTimeSlice tcb - Suc 0) ko) \<and> \<not> inQ qdom prio ko \<longrightarrow> ksCurThread s \<in> set (ksReadyQueues sa (qdom, prio))) \<and> valid_queues' sa \<and> weak_sch_act_wf (ksSchedulerAction sa) sa) \<and> (\<not> Suc 0 < tcbTimeSlice tcb \<longrightarrow> Invariants_H.valid_queues sa \<and> (\<forall>d p. (\<exists>tcb. inQ d p tcb \<and> runnable' (tcbState tcb) \<and> (inQ d p (tcbTimeSlice_update (\<lambda>_. timeSlice) tcb) \<longrightarrow> \<not> runnable' (tcbState tcb))) \<longrightarrow> obj_at' (\<lambda>tcb. inQ d p tcb \<and> runnable' (tcbState tcb) \<and> (inQ d p (tcbTimeSlice_update (\<lambda>_. timeSlice) tcb) \<longrightarrow> \<not> runnable' (tcbState tcb))) (ksCurThread s) sa \<longrightarrow> ksCurThread s \<notin> set (ksReadyQueues sa (d, p))) \<and> (tcb_at' (ksCurThread s) sa \<longrightarrow> obj_at' (\<lambda>tcb. runnable' (tcbState tcb)) (ksCurThread s) sa) \<and> valid_objs' sa \<and> (\<forall>ko qdom prio. ko_at' ko (ksCurThread s) sa \<and> inQ qdom prio (tcbTimeSlice_update (\<lambda>_. timeSlice) ko) \<and> \<not> inQ qdom prio ko \<longrightarrow> ksCurThread s \<in> set (ksReadyQueues sa (qdom, prio))) \<and> valid_queues' sa \<and> tcb_at' (ksCurThread s) sa \<and> sch_act_wf (ksSchedulerAction sa) sa))) \<and> (st \<noteq> Structures_H.thread_state.Running \<longrightarrow> Invariants_H.valid_queues (sa\<lparr>ksDomainTime := ksDomainTime sa - 1\<rparr>) \<and> valid_queues' (sa\<lparr>ksDomainTime := ksDomainTime sa - 1\<rparr>) \<and> weak_sch_act_wf (ksSchedulerAction (sa\<lparr>ksDomainTime := ksDomainTime sa - 1\<rparr>)) (sa\<lparr>ksDomainTime := ksDomainTime sa - 1\<rparr>)))) sa)) s)) s
 2. \<And>s. (cur_tcb and valid_sched) s \<Longrightarrow> ((\<lambda>_. True) and (cur_tcb and valid_sched)) s
 3. \<And>s. invs' s \<Longrightarrow> ((\<lambda>_. True) and invs') s proof (prove)
goal (3 subgoals):
 1. \<And>s. (cur_tcb and valid_sched) s \<Longrightarrow> ((\<lambda>_. True) and (cur_tcb and valid_sched)) s
 2. \<And>s. ((\<lambda>_. True) and invs') s \<Longrightarrow> ((\<lambda>_. True) and (\<lambda>s. (tcb_at' (ksCurThread s) and (\<lambda>sa. \<forall>st. st_tcb_at' ((=) st) (ksCurThread s) sa \<longrightarrow> ((if st = Structures_H.thread_state.Running then tcb_at' (ksCurThread s) and (tcb_at' (ksCurThread s) and (tcb_at' (ksCurThread s) and (\<lambda>sa. obj_at' (\<lambda>obj. if ksCurThread s = ksCurThread s then True else True) (ksCurThread s) sa \<and> (Invariants_H.valid_queues and (\<lambda>sa. \<forall>d p. (\<exists>tcb. (inQ d p tcb \<and> runnable' (tcbState tcb)) \<and> \<not> (inQ d p (tcbTimeSlice_update (\<lambda>_. timeSlice) tcb) \<and> runnable' (tcbState (tcbTimeSlice_update (\<lambda>_. timeSlice) tcb)))) \<longrightarrow> obj_at' (\<lambda>tcb. (inQ d p tcb \<and> runnable' (tcbState tcb)) \<and> \<not> (inQ d p (tcbTimeSlice_update (\<lambda>_. timeSlice) tcb) \<and> runnable' (tcbState (tcbTimeSlice_update (\<lambda>_. timeSlice) tcb)))) (ksCurThread s) sa \<longrightarrow> ksCurThread s \<notin> set (ksReadyQueues sa (d, p)))) sa \<and> ((\<forall>ko qdom prio. ko_at' ko (ksCurThread s) sa \<and> inQ qdom prio (tcbTimeSlice_update (\<lambda>_. timeSlice) ko) \<and> \<not> inQ qdom prio ko \<longrightarrow> ksCurThread s \<in> set (ksReadyQueues sa (qdom, prio))) \<and> valid_queues' sa) \<and> (invs' and tcb_at' (ksCurThread s)) sa \<and> (tcb_at' (ksCurThread s) sa \<longrightarrow> (if ksCurThread s = ksCurThread s then obj_at' (\<lambda>tcb. runnable' (itcbState (tcb_to_itcb' (tcbTimeSlice_update (\<lambda>_. timeSlice) tcb)))) (ksCurThread s) sa else st_tcb_at' runnable' (ksCurThread s) sa))))) else (\<lambda>_. True)) and (\<lambda>sa. Suc 0 < numDomains \<longrightarrow> True \<and> True \<and> (st = Structures_H.thread_state.Running \<longrightarrow> tcb_at' (ksCurThread s) sa \<longrightarrow> (\<exists>tcb. ko_at' tcb (ksCurThread s) sa \<and> (Suc 0 < tcbTimeSlice tcb \<longrightarrow> Invariants_H.valid_queues sa \<and> (\<forall>d p. (\<exists>tcba. inQ d p tcba \<and> runnable' (tcbState tcba) \<and> (inQ d p (tcbTimeSlice_update (\<lambda>_. tcbTimeSlice tcb - Suc 0) tcba) \<longrightarrow> \<not> runnable' (tcbState tcba))) \<longrightarrow> obj_at' (\<lambda>tcba. inQ d p tcba \<and> runnable' (tcbState tcba) \<and> (inQ d p (tcbTimeSlice_update (\<lambda>_. tcbTimeSlice tcb - Suc 0) tcba) \<longrightarrow> \<not> runnable' (tcbState tcba))) (ksCurThread s) sa \<longrightarrow> ksCurThread s \<notin> set (ksReadyQueues sa (d, p))) \<and> (\<forall>ko qdom prio. ko_at' ko (ksCurThread s) sa \<and> inQ qdom prio (tcbTimeSlice_update (\<lambda>_. tcbTimeSlice tcb - Suc 0) ko) \<and> \<not> inQ qdom prio ko \<longrightarrow> ksCurThread s \<in> set (ksReadyQueues sa (qdom, prio))) \<and> valid_queues' sa \<and> weak_sch_act_wf (ksSchedulerAction sa) sa) \<and> (\<not> Suc 0 < tcbTimeSlice tcb \<longrightarrow> Invariants_H.valid_queues sa \<and> (\<forall>d p. (\<exists>tcb. inQ d p tcb \<and> runnable' (tcbState tcb) \<and> (inQ d p (tcbTimeSlice_update (\<lambda>_. timeSlice) tcb) \<longrightarrow> \<not> runnable' (tcbState tcb))) \<longrightarrow> obj_at' (\<lambda>tcb. inQ d p tcb \<and> runnable' (tcbState tcb) \<and> (inQ d p (tcbTimeSlice_update (\<lambda>_. timeSlice) tcb) \<longrightarrow> \<not> runnable' (tcbState tcb))) (ksCurThread s) sa \<longrightarrow> ksCurThread s \<notin> set (ksReadyQueues sa (d, p))) \<and> (tcb_at' (ksCurThread s) sa \<longrightarrow> obj_at' (\<lambda>tcb. runnable' (tcbState tcb)) (ksCurThread s) sa) \<and> valid_objs' sa \<and> (\<forall>ko qdom prio. ko_at' ko (ksCurThread s) sa \<and> inQ qdom prio (tcbTimeSlice_update (\<lambda>_. timeSlice) ko) \<and> \<not> inQ qdom prio ko \<longrightarrow> ksCurThread s \<in> set (ksReadyQueues sa (qdom, prio))) \<and> valid_queues' sa \<and> tcb_at' (ksCurThread s) sa \<and> sch_act_wf (ksSchedulerAction sa) sa))) \<and> (st \<noteq> Structures_H.thread_state.Running \<longrightarrow> Invariants_H.valid_queues (sa\<lparr>ksDomainTime := ksDomainTime sa - 1\<rparr>) \<and> valid_queues' (sa\<lparr>ksDomainTime := ksDomainTime sa - 1\<rparr>) \<and> weak_sch_act_wf (ksSchedulerAction (sa\<lparr>ksDomainTime := ksDomainTime sa - 1\<rparr>)) (sa\<lparr>ksDomainTime := ksDomainTime sa - 1\<rparr>)))) sa)) s)) s
 3. \<And>s. invs' s \<Longrightarrow> ((\<lambda>_. True) and invs') s proof (prove)
goal (2 subgoals):
 1. \<And>s. ((\<lambda>_. True) and invs') s \<Longrightarrow> ((\<lambda>_. True) and (\<lambda>s. (tcb_at' (ksCurThread s) and (\<lambda>sa. \<forall>st. st_tcb_at' ((=) st) (ksCurThread s) sa \<longrightarrow> ((if st = Structures_H.thread_state.Running then tcb_at' (ksCurThread s) and (tcb_at' (ksCurThread s) and (tcb_at' (ksCurThread s) and (\<lambda>sa. obj_at' (\<lambda>obj. if ksCurThread s = ksCurThread s then True else True) (ksCurThread s) sa \<and> (Invariants_H.valid_queues and (\<lambda>sa. \<forall>d p. (\<exists>tcb. (inQ d p tcb \<and> runnable' (tcbState tcb)) \<and> \<not> (inQ d p (tcbTimeSlice_update (\<lambda>_. timeSlice) tcb) \<and> runnable' (tcbState (tcbTimeSlice_update (\<lambda>_. timeSlice) tcb)))) \<longrightarrow> obj_at' (\<lambda>tcb. (inQ d p tcb \<and> runnable' (tcbState tcb)) \<and> \<not> (inQ d p (tcbTimeSlice_update (\<lambda>_. timeSlice) tcb) \<and> runnable' (tcbState (tcbTimeSlice_update (\<lambda>_. timeSlice) tcb)))) (ksCurThread s) sa \<longrightarrow> ksCurThread s \<notin> set (ksReadyQueues sa (d, p)))) sa \<and> ((\<forall>ko qdom prio. ko_at' ko (ksCurThread s) sa \<and> inQ qdom prio (tcbTimeSlice_update (\<lambda>_. timeSlice) ko) \<and> \<not> inQ qdom prio ko \<longrightarrow> ksCurThread s \<in> set (ksReadyQueues sa (qdom, prio))) \<and> valid_queues' sa) \<and> (invs' and tcb_at' (ksCurThread s)) sa \<and> (tcb_at' (ksCurThread s) sa \<longrightarrow> (if ksCurThread s = ksCurThread s then obj_at' (\<lambda>tcb. runnable' (itcbState (tcb_to_itcb' (tcbTimeSlice_update (\<lambda>_. timeSlice) tcb)))) (ksCurThread s) sa else st_tcb_at' runnable' (ksCurThread s) sa))))) else (\<lambda>_. True)) and (\<lambda>sa. Suc 0 < numDomains \<longrightarrow> True \<and> True \<and> (st = Structures_H.thread_state.Running \<longrightarrow> tcb_at' (ksCurThread s) sa \<longrightarrow> (\<exists>tcb. ko_at' tcb (ksCurThread s) sa \<and> (Suc 0 < tcbTimeSlice tcb \<longrightarrow> Invariants_H.valid_queues sa \<and> (\<forall>d p. (\<exists>tcba. inQ d p tcba \<and> runnable' (tcbState tcba) \<and> (inQ d p (tcbTimeSlice_update (\<lambda>_. tcbTimeSlice tcb - Suc 0) tcba) \<longrightarrow> \<not> runnable' (tcbState tcba))) \<longrightarrow> obj_at' (\<lambda>tcba. inQ d p tcba \<and> runnable' (tcbState tcba) \<and> (inQ d p (tcbTimeSlice_update (\<lambda>_. tcbTimeSlice tcb - Suc 0) tcba) \<longrightarrow> \<not> runnable' (tcbState tcba))) (ksCurThread s) sa \<longrightarrow> ksCurThread s \<notin> set (ksReadyQueues sa (d, p))) \<and> (\<forall>ko qdom prio. ko_at' ko (ksCurThread s) sa \<and> inQ qdom prio (tcbTimeSlice_update (\<lambda>_. tcbTimeSlice tcb - Suc 0) ko) \<and> \<not> inQ qdom prio ko \<longrightarrow> ksCurThread s \<in> set (ksReadyQueues sa (qdom, prio))) \<and> valid_queues' sa \<and> weak_sch_act_wf (ksSchedulerAction sa) sa) \<and> (\<not> Suc 0 < tcbTimeSlice tcb \<longrightarrow> Invariants_H.valid_queues sa \<and> (\<forall>d p. (\<exists>tcb. inQ d p tcb \<and> runnable' (tcbState tcb) \<and> (inQ d p (tcbTimeSlice_update (\<lambda>_. timeSlice) tcb) \<longrightarrow> \<not> runnable' (tcbState tcb))) \<longrightarrow> obj_at' (\<lambda>tcb. inQ d p tcb \<and> runnable' (tcbState tcb) \<and> (inQ d p (tcbTimeSlice_update (\<lambda>_. timeSlice) tcb) \<longrightarrow> \<not> runnable' (tcbState tcb))) (ksCurThread s) sa \<longrightarrow> ksCurThread s \<notin> set (ksReadyQueues sa (d, p))) \<and> (tcb_at' (ksCurThread s) sa \<longrightarrow> obj_at' (\<lambda>tcb. runnable' (tcbState tcb)) (ksCurThread s) sa) \<and> valid_objs' sa \<and> (\<forall>ko qdom prio. ko_at' ko (ksCurThread s) sa \<and> inQ qdom prio (tcbTimeSlice_update (\<lambda>_. timeSlice) ko) \<and> \<not> inQ qdom prio ko \<longrightarrow> ksCurThread s \<in> set (ksReadyQueues sa (qdom, prio))) \<and> valid_queues' sa \<and> tcb_at' (ksCurThread s) sa \<and> sch_act_wf (ksSchedulerAction sa) sa))) \<and> (st \<noteq> Structures_H.thread_state.Running \<longrightarrow> Invariants_H.valid_queues (sa\<lparr>ksDomainTime := ksDomainTime sa - 1\<rparr>) \<and> valid_queues' (sa\<lparr>ksDomainTime := ksDomainTime sa - 1\<rparr>) \<and> weak_sch_act_wf (ksSchedulerAction (sa\<lparr>ksDomainTime := ksDomainTime sa - 1\<rparr>)) (sa\<lparr>ksDomainTime := ksDomainTime sa - 1\<rparr>)))) sa)) s)) s
 2. \<And>s. invs' s \<Longrightarrow> ((\<lambda>_. True) and invs') s proof (prove)
goal (2 subgoals):
 1. \<And>s. invs' s \<Longrightarrow> tcb_at' (ksCurThread s) s \<and> (\<forall>st. (st = Structures_H.thread_state.Running \<longrightarrow> st_tcb_at' ((=) Structures_H.thread_state.Running) (ksCurThread s) s \<longrightarrow> tcb_at' (ksCurThread s) s \<and> Invariants_H.valid_queues s \<and> (\<forall>d p. (\<exists>tcb. inQ d p tcb \<and> runnable' (tcbState tcb) \<and> (inQ d p (tcbTimeSlice_update (\<lambda>_. timeSlice) tcb) \<longrightarrow> \<not> runnable' (tcbState tcb))) \<longrightarrow> obj_at' (\<lambda>tcb. inQ d p tcb \<and> runnable' (tcbState tcb) \<and> (inQ d p (tcbTimeSlice_update (\<lambda>_. timeSlice) tcb) \<longrightarrow> \<not> runnable' (tcbState tcb))) (ksCurThread s) s \<longrightarrow> ksCurThread s \<notin> set (ksReadyQueues s (d, p))) \<and> (\<forall>ko qdom prio. ko_at' ko (ksCurThread s) s \<and> inQ qdom prio (tcbTimeSlice_update (\<lambda>_. timeSlice) ko) \<and> \<not> inQ qdom prio ko \<longrightarrow> ksCurThread s \<in> set (ksReadyQueues s (qdom, prio))) \<and> valid_queues' s \<and> tcb_at' (ksCurThread s) s \<and> (tcb_at' (ksCurThread s) s \<longrightarrow> obj_at' (\<lambda>tcb. runnable' (tcbState tcb)) (ksCurThread s) s) \<and> (Suc 0 < numDomains \<longrightarrow> tcb_at' (ksCurThread s) s \<longrightarrow> (\<exists>tcb. ko_at' tcb (ksCurThread s) s \<and> (Suc 0 < tcbTimeSlice tcb \<longrightarrow> Invariants_H.valid_queues s \<and> (\<forall>d p. (\<exists>tcba. inQ d p tcba \<and> runnable' (tcbState tcba) \<and> (inQ d p (tcbTimeSlice_update (\<lambda>_. tcbTimeSlice tcb - Suc 0) tcba) \<longrightarrow> \<not> runnable' (tcbState tcba))) \<longrightarrow> obj_at' (\<lambda>tcba. inQ d p tcba \<and> runnable' (tcbState tcba) \<and> (inQ d p (tcbTimeSlice_update (\<lambda>_. tcbTimeSlice tcb - Suc 0) tcba) \<longrightarrow> \<not> runnable' (tcbState tcba))) (ksCurThread s) s \<longrightarrow> ksCurThread s \<notin> set (ksReadyQueues s (d, p))) \<and> (\<forall>ko qdom prio. ko_at' ko (ksCurThread s) s \<and> inQ qdom prio (tcbTimeSlice_update (\<lambda>_. tcbTimeSlice tcb - Suc 0) ko) \<and> \<not> inQ qdom prio ko \<longrightarrow> ksCurThread s \<in> set (ksReadyQueues s (qdom, prio))) \<and> valid_queues' s \<and> weak_sch_act_wf (ksSchedulerAction s) s) \<and> (\<not> Suc 0 < tcbTimeSlice tcb \<longrightarrow> Invariants_H.valid_queues s \<and> (\<forall>d p. (\<exists>tcb. inQ d p tcb \<and> runnable' (tcbState tcb) \<and> (inQ d p (tcbTimeSlice_update (\<lambda>_. timeSlice) tcb) \<longrightarrow> \<not> runnable' (tcbState tcb))) \<longrightarrow> obj_at' (\<lambda>tcb. inQ d p tcb \<and> runnable' (tcbState tcb) \<and> (inQ d p (tcbTimeSlice_update (\<lambda>_. timeSlice) tcb) \<longrightarrow> \<not> runnable' (tcbState tcb))) (ksCurThread s) s \<longrightarrow> ksCurThread s \<notin> set (ksReadyQueues s (d, p))) \<and> obj_at' (\<lambda>tcb. runnable' (tcbState tcb)) (ksCurThread s) s \<and> valid_objs' s \<and> (\<forall>ko qdom prio. ko_at' ko (ksCurThread s) s \<and> inQ qdom prio (tcbTimeSlice_update (\<lambda>_. timeSlice) ko) \<and> \<not> inQ qdom prio ko \<longrightarrow> ksCurThread s \<in> set (ksReadyQueues s (qdom, prio))) \<and> valid_queues' s \<and> sch_act_wf (ksSchedulerAction s) s)))) \<and> (st \<noteq> Structures_H.thread_state.Running \<longrightarrow> st_tcb_at' ((=) st) (ksCurThread s) s \<longrightarrow> Suc 0 < numDomains \<longrightarrow> Invariants_H.valid_queues s \<and> valid_queues' s \<and> weak_sch_act_wf (ksSchedulerAction s) s))
 2. \<And>s. invs' s \<Longrightarrow> ((\<lambda>_. True) and invs') s proof (prove)
goal (2 subgoals):
 1. \<And>s ko obj. \<lbrakk>valid_pspace' 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; ksPSpace s (ksCurThread s) = Some ko; is_aligned (ksCurThread s) (objBitsKO ko); ps_clear (ksCurThread s) (objBitsKO ko) s; fst (projectKO ko s) = {(obj, s)}; st_tcb_at' ((=) Structures_H.thread_state.Running) (ksCurThread s) s\<rbrakk> \<Longrightarrow> runnable' (tcbState obj) \<and> (Suc 0 < numDomains \<longrightarrow> \<not> Suc 0 < tcbTimeSlice obj \<longrightarrow> runnable' (tcbState obj) \<and> valid_objs' s)
 2. \<And>s. invs' s \<Longrightarrow> ((\<lambda>_. True) and invs') s proof (prove)
goal (1 subgoal):
 1. \<And>s. invs' s \<Longrightarrow> ((\<lambda>_. True) and invs') s proof (prove)
goal:
No subgoals!