theory Finalise_C

lemma cancel_all_ccorres_helper:
  "ccorres dc xfdc
      (\<lambda>s. valid_objs' s \<and> valid_queues s
             \<and> (\<forall>t\<in>set ts. tcb_at' t s \<and> t \<noteq> 0)
             \<and> sch_act_wf (ksSchedulerAction s) s)
      {s'. \<exists>p. ep_queue_relation (cslift s') ts
                p (thread_' s')} hs
      (mapM_x (\<lambda>t. do
              y \<leftarrow> setThreadState Restart t;
              tcbSchedEnqueue t
            od) ts)
      (WHILE \<acute>thread \<noteq> tcb_Ptr 0 DO
        (CALL setThreadState(\<acute>thread, scast ThreadState_Restart));;
        (CALL tcbSchedEnqueue(\<acute>thread));;
        Guard C_Guard \<lbrace>hrs_htd \<acute>t_hrs \<Turnstile>\<^sub>t \<acute>thread\<rbrace>
         (\<acute>thread :== h_val (hrs_mem \<acute>t_hrs) (Ptr &(\<acute>thread\<rightarrow>[''tcbEPNext_C'']) :: tcb_C ptr ptr))
       OD)" unfolding whileAnno_def proof (induct ts) case Nil show ?case apply (simp del: Collect_const) apply (rule iffD1 [OF ccorres_expand_while_iff]) apply (rule ccorres_tmp_lift2[where G'=UNIV and G''="\<lambda>x. UNIV", simplified]) apply ceqv apply (simp add: ccorres_cond_iffs mapM_x_def sequence_x_def) apply (rule ccorres_guard_imp2, rule ccorres_return_Skip) apply simp done next case (Cons thread threads) show ?case apply (rule iffD1 [OF ccorres_expand_while_iff]) apply (simp del: Collect_const
                add: mapM_x_Cons) apply (rule ccorres_guard_imp2) apply (rule_tac xf'=thread_' in ccorres_abstract) apply ceqv apply (rule_tac P="rv' = tcb_ptr_to_ctcb_ptr thread"
                     in ccorres_gen_asm2) apply (rule_tac P="tcb_ptr_to_ctcb_ptr thread \<noteq> Ptr 0"
                     in ccorres_gen_asm) apply (clarsimp simp add: Collect_True ccorres_cond_iffs
                     simp del: Collect_const) apply (rule_tac r'=dc and xf'=xfdc in ccorres_split_nothrow[where F=UNIV]) apply (intro ccorres_rhs_assoc) apply (ctac(no_vcg) add: setThreadState_ccorres) apply (rule ccorres_add_return2) apply (ctac(no_vcg) add: tcbSchedEnqueue_ccorres) apply (rule_tac P="tcb_at' thread"
                      in ccorres_from_vcg[where P'=UNIV]) apply (rule allI, rule conseqPre, vcg) apply (clarsimp simp: return_def) apply (drule obj_at_ko_at', clarsimp) apply (erule cmap_relationE1 [OF cmap_relation_tcb]) apply (erule ko_at_projectKO_opt) apply (fastforce intro: typ_heap_simps) apply (wp sts_running_valid_queues | simp)+ apply (rule ceqv_refl) apply (rule "Cons.hyps") apply (wp sts_valid_objs' sts_sch_act sch_act_wf_lift hoare_vcg_const_Ball_lift
                sts_running_valid_queues sts_st_tcb' setThreadState_oa_queued | simp)+ apply (vcg exspec=setThreadState_cslift_spec exspec=tcbSchedEnqueue_cslift_spec) apply (clarsimp simp: tcb_at_not_NULL
                          Collect_const_mem valid_tcb_state'_def
                          ThreadState_Restart_def mask_def
                          valid_objs'_maxDomain valid_objs'_maxPriority) apply (drule(1) obj_at_cslift_tcb) apply (clarsimp simp: typ_heap_simps) apply (rule conjI) apply clarsimp apply (frule rf_sr_cscheduler_relation) apply (clarsimp simp: cscheduler_action_relation_def
                           st_tcb_at'_def
                    split: scheduler_action.split_asm) apply (rename_tac word) apply (frule_tac x=word in tcbSchedEnqueue_cslift_precond_discharge) apply simp apply clarsimp apply clarsimp apply clarsimp apply clarsimp apply (rule conjI) apply (frule(3) tcbSchedEnqueue_cslift_precond_discharge) apply clarsimp apply clarsimp apply (subst ep_queue_relation_shift, fastforce) apply (drule_tac x="tcb_ptr_to_ctcb_ptr thread"
                in fun_cong)+ apply (clarsimp simp add: option_map2_def typ_heap_simps) apply fastforce done qed

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. ccorres dc xfdc (\<lambda>s. valid_objs' s \<and> Invariants_H.valid_queues s \<and> (\<forall>t\<in>set ts. tcb_at' t s \<and> t \<noteq> 0) \<and> sch_act_wf (ksSchedulerAction s) s) {s'. \<exists>p. ep_queue_relation (cslift s') ts p (thread_' s')} hs (mapM_x (\<lambda>t. do y <- setThreadState Structures_H.thread_state.Restart t;
tcbSchedEnqueue t
od) ts) (WHILE \<acute>thread \<noteq> NULL DO
  CALL setThreadState_'proc(\<acute>thread,SCAST(32 signed \<rightarrow> 32) ThreadState_Restart);;
CALL tcbSchedEnqueue_'proc(\<acute>thread);;
Guard C_Guard {s. s \<Turnstile>\<^sub>c thread_' s} (\<acute>thread :== h_val (hrs_mem \<acute>t_hrs) (PTR(tcb_C ptr) &(\<acute>thread\<rightarrow>[''tcbEPNext_C''])))
OD) proof (prove)
goal (1 subgoal):
 1. ccorres dc xfdc (\<lambda>s. valid_objs' s \<and> Invariants_H.valid_queues s \<and> (\<forall>t\<in>set ts. tcb_at' t s \<and> t \<noteq> 0) \<and> sch_act_wf (ksSchedulerAction s) s) {s'. \<exists>p. ep_queue_relation (cslift s') ts p (thread_' s')} hs (mapM_x (\<lambda>t. do y <- setThreadState Structures_H.thread_state.Restart t;
tcbSchedEnqueue t
od) ts) (While \<lbrace>\<acute>thread \<noteq> NULL\<rbrace> (CALL setThreadState_'proc(\<acute>thread,SCAST(32 signed \<rightarrow> 32) ThreadState_Restart);;
CALL tcbSchedEnqueue_'proc(\<acute>thread);;
Guard C_Guard {s. s \<Turnstile>\<^sub>c thread_' s} (\<acute>thread :== h_val (hrs_mem \<acute>t_hrs) (PTR(tcb_C ptr) &(\<acute>thread\<rightarrow>[''tcbEPNext_C'']))))) proof (state)
goal (2 subgoals):
 1. ccorres dc xfdc (\<lambda>s. valid_objs' s \<and> Invariants_H.valid_queues s \<and> (\<forall>t\<in>set []. tcb_at' t s \<and> t \<noteq> 0) \<and> sch_act_wf (ksSchedulerAction s) s) {s'. \<exists>p. ep_queue_relation (cslift s') [] p (thread_' s')} hs (mapM_x (\<lambda>t. do y <- setThreadState Structures_H.thread_state.Restart t;
tcbSchedEnqueue t
od) []) (While \<lbrace>\<acute>thread \<noteq> NULL\<rbrace> (CALL setThreadState_'proc(\<acute>thread,SCAST(32 signed \<rightarrow> 32) ThreadState_Restart);;
CALL tcbSchedEnqueue_'proc(\<acute>thread);;
Guard C_Guard {s. s \<Turnstile>\<^sub>c thread_' s} (\<acute>thread :== h_val (hrs_mem \<acute>t_hrs) (PTR(tcb_C ptr) &(\<acute>thread\<rightarrow>[''tcbEPNext_C''])))))
 2. \<And>x1 ts. ccorres dc xfdc (\<lambda>s. valid_objs' s \<and> Invariants_H.valid_queues s \<and> (\<forall>t\<in>set ts. tcb_at' t s \<and> t \<noteq> 0) \<and> sch_act_wf (ksSchedulerAction s) s) {s'. \<exists>p. ep_queue_relation (cslift s') ts p (thread_' s')} hs (mapM_x (\<lambda>t. do y <- setThreadState Structures_H.thread_state.Restart t;
tcbSchedEnqueue t
od) ts) (While \<lbrace>\<acute>thread \<noteq> NULL\<rbrace> (CALL setThreadState_'proc(\<acute>thread,SCAST(32 signed \<rightarrow> 32) ThreadState_Restart);;
CALL tcbSchedEnqueue_'proc(\<acute>thread);;
Guard C_Guard {s. s \<Turnstile>\<^sub>c thread_' s} (\<acute>thread :== h_val (hrs_mem \<acute>t_hrs) (PTR(tcb_C ptr) &(\<acute>thread\<rightarrow>[''tcbEPNext_C'']))))) \<Longrightarrow> ccorres dc xfdc (\<lambda>s. valid_objs' s \<and> Invariants_H.valid_queues s \<and> (\<forall>t\<in>set (x1 # ts). tcb_at' t s \<and> t \<noteq> 0) \<and> sch_act_wf (ksSchedulerAction s) s) {s'. \<exists>p. ep_queue_relation (cslift s') (x1 # ts) p (thread_' s')} hs (mapM_x (\<lambda>t. do y <- setThreadState Structures_H.thread_state.Restart t;
tcbSchedEnqueue t
od) (x1 # ts)) (While \<lbrace>\<acute>thread \<noteq> NULL\<rbrace> (CALL setThreadState_'proc(\<acute>thread,SCAST(32 signed \<rightarrow> 32) ThreadState_Restart);;
CALL tcbSchedEnqueue_'proc(\<acute>thread);;
Guard C_Guard {s. s \<Turnstile>\<^sub>c thread_' s} (\<acute>thread :== h_val (hrs_mem \<acute>t_hrs) (PTR(tcb_C ptr) &(\<acute>thread\<rightarrow>[''tcbEPNext_C'']))))) proof (state)
this:


goal (2 subgoals):
 1. ccorres dc xfdc (\<lambda>s. valid_objs' s \<and> Invariants_H.valid_queues s \<and> (\<forall>t\<in>set []. tcb_at' t s \<and> t \<noteq> 0) \<and> sch_act_wf (ksSchedulerAction s) s) {s'. \<exists>p. ep_queue_relation (cslift s') [] p (thread_' s')} hs (mapM_x (\<lambda>t. do y <- setThreadState Structures_H.thread_state.Restart t;
tcbSchedEnqueue t
od) []) (While \<lbrace>\<acute>thread \<noteq> NULL\<rbrace> (CALL setThreadState_'proc(\<acute>thread,SCAST(32 signed \<rightarrow> 32) ThreadState_Restart);;
CALL tcbSchedEnqueue_'proc(\<acute>thread);;
Guard C_Guard {s. s \<Turnstile>\<^sub>c thread_' s} (\<acute>thread :== h_val (hrs_mem \<acute>t_hrs) (PTR(tcb_C ptr) &(\<acute>thread\<rightarrow>[''tcbEPNext_C''])))))
 2. \<And>x1 ts. ccorres dc xfdc (\<lambda>s. valid_objs' s \<and> Invariants_H.valid_queues s \<and> (\<forall>t\<in>set ts. tcb_at' t s \<and> t \<noteq> 0) \<and> sch_act_wf (ksSchedulerAction s) s) {s'. \<exists>p. ep_queue_relation (cslift s') ts p (thread_' s')} hs (mapM_x (\<lambda>t. do y <- setThreadState Structures_H.thread_state.Restart t;
tcbSchedEnqueue t
od) ts) (While \<lbrace>\<acute>thread \<noteq> NULL\<rbrace> (CALL setThreadState_'proc(\<acute>thread,SCAST(32 signed \<rightarrow> 32) ThreadState_Restart);;
CALL tcbSchedEnqueue_'proc(\<acute>thread);;
Guard C_Guard {s. s \<Turnstile>\<^sub>c thread_' s} (\<acute>thread :== h_val (hrs_mem \<acute>t_hrs) (PTR(tcb_C ptr) &(\<acute>thread\<rightarrow>[''tcbEPNext_C'']))))) \<Longrightarrow> ccorres dc xfdc (\<lambda>s. valid_objs' s \<and> Invariants_H.valid_queues s \<and> (\<forall>t\<in>set (x1 # ts). tcb_at' t s \<and> t \<noteq> 0) \<and> sch_act_wf (ksSchedulerAction s) s) {s'. \<exists>p. ep_queue_relation (cslift s') (x1 # ts) p (thread_' s')} hs (mapM_x (\<lambda>t. do y <- setThreadState Structures_H.thread_state.Restart t;
tcbSchedEnqueue t
od) (x1 # ts)) (While \<lbrace>\<acute>thread \<noteq> NULL\<rbrace> (CALL setThreadState_'proc(\<acute>thread,SCAST(32 signed \<rightarrow> 32) ThreadState_Restart);;
CALL tcbSchedEnqueue_'proc(\<acute>thread);;
Guard C_Guard {s. s \<Turnstile>\<^sub>c thread_' s} (\<acute>thread :== h_val (hrs_mem \<acute>t_hrs) (PTR(tcb_C ptr) &(\<acute>thread\<rightarrow>[''tcbEPNext_C'']))))) proof (prove)
goal (1 subgoal):
 1. ccorres dc xfdc (\<lambda>s. valid_objs' s \<and> Invariants_H.valid_queues s \<and> (\<forall>t\<in>set []. tcb_at' t s \<and> t \<noteq> 0) \<and> sch_act_wf (ksSchedulerAction s) s) {s'. \<exists>p. ep_queue_relation (cslift s') [] p (thread_' s')} hs (mapM_x (\<lambda>t. do y <- setThreadState Structures_H.thread_state.Restart t;
tcbSchedEnqueue t
od) []) (While \<lbrace>\<acute>thread \<noteq> NULL\<rbrace> (CALL setThreadState_'proc(\<acute>thread,SCAST(32 signed \<rightarrow> 32) ThreadState_Restart);;
CALL tcbSchedEnqueue_'proc(\<acute>thread);;
Guard C_Guard {s. s \<Turnstile>\<^sub>c thread_' s} (\<acute>thread :== h_val (hrs_mem \<acute>t_hrs) (PTR(tcb_C ptr) &(\<acute>thread\<rightarrow>[''tcbEPNext_C'']))))) proof (prove)
goal (1 subgoal):
 1. ccorres dc xfdc (\<lambda>s. valid_objs' s \<and> Invariants_H.valid_queues s \<and> sch_act_wf (ksSchedulerAction s) s) \<lbrace>\<acute>thread = NULL\<rbrace> hs (mapM_x (\<lambda>t. do y <- setThreadState Structures_H.thread_state.Restart t;
tcbSchedEnqueue t
od) []) (While \<lbrace>\<acute>thread \<noteq> NULL\<rbrace> (CALL setThreadState_'proc(\<acute>thread,SCAST(32 signed \<rightarrow> 32) ThreadState_Restart);;
CALL tcbSchedEnqueue_'proc(\<acute>thread);;
Guard C_Guard {s. s \<Turnstile>\<^sub>c thread_' s} (\<acute>thread :== h_val (hrs_mem \<acute>t_hrs) (PTR(tcb_C ptr) &(\<acute>thread\<rightarrow>[''tcbEPNext_C'']))))) proof (prove)
goal (1 subgoal):
 1. ccorres dc xfdc (\<lambda>s. valid_objs' s \<and> Invariants_H.valid_queues s \<and> sch_act_wf (ksSchedulerAction s) s) \<lbrace>\<acute>thread = NULL\<rbrace> hs (mapM_x (\<lambda>t. do y <- setThreadState Structures_H.thread_state.Restart t;
tcbSchedEnqueue t
od) []) (IF \<acute>thread \<noteq> NULL THEN
  CALL setThreadState_'proc(\<acute>thread,SCAST(32 signed \<rightarrow> 32) ThreadState_Restart);;
CALL tcbSchedEnqueue_'proc(\<acute>thread);;
Guard C_Guard {s. s \<Turnstile>\<^sub>c thread_' s} (\<acute>thread :== h_val (hrs_mem \<acute>t_hrs) (PTR(tcb_C ptr) &(\<acute>thread\<rightarrow>[''tcbEPNext_C''])));;
While \<lbrace>\<acute>thread \<noteq> NULL\<rbrace> (CALL setThreadState_'proc(\<acute>thread,SCAST(32 signed \<rightarrow> 32) ThreadState_Restart);;
CALL tcbSchedEnqueue_'proc(\<acute>thread);;
Guard C_Guard {s. s \<Turnstile>\<^sub>c thread_' s} (\<acute>thread :== h_val (hrs_mem \<acute>t_hrs) (PTR(tcb_C ptr) &(\<acute>thread\<rightarrow>[''tcbEPNext_C'']))))
FI) proof (prove)
goal (2 subgoals):
 1. \<And>t t'. ceqv \<Gamma> thread_' NULL t t' (IF \<acute>thread \<noteq> NULL THEN
  CALL setThreadState_'proc(\<acute>thread,SCAST(32 signed \<rightarrow> 32) ThreadState_Restart);;
CALL tcbSchedEnqueue_'proc(\<acute>thread);;
Guard C_Guard {s. s \<Turnstile>\<^sub>c thread_' s} (\<acute>thread :== h_val (hrs_mem \<acute>t_hrs) (PTR(tcb_C ptr) &(\<acute>thread\<rightarrow>[''tcbEPNext_C''])));;
While \<lbrace>\<acute>thread \<noteq> NULL\<rbrace> (CALL setThreadState_'proc(\<acute>thread,SCAST(32 signed \<rightarrow> 32) ThreadState_Restart);;
CALL tcbSchedEnqueue_'proc(\<acute>thread);;
Guard C_Guard {s. s \<Turnstile>\<^sub>c thread_' s} (\<acute>thread :== h_val (hrs_mem \<acute>t_hrs) (PTR(tcb_C ptr) &(\<acute>thread\<rightarrow>[''tcbEPNext_C'']))))
FI) ?c'15
 2. ccorres dc xfdc (\<lambda>s. valid_objs' s \<and> Invariants_H.valid_queues s \<and> sch_act_wf (ksSchedulerAction s) s) UNIV hs (mapM_x (\<lambda>t. do y <- setThreadState Structures_H.thread_state.Restart t;
tcbSchedEnqueue t
od) []) ?c'15 proof (prove)
goal (1 subgoal):
 1. ccorres dc xfdc (\<lambda>s. valid_objs' s \<and> Invariants_H.valid_queues s \<and> sch_act_wf (ksSchedulerAction s) s) UNIV hs (mapM_x (\<lambda>t. do y <- setThreadState Structures_H.thread_state.Restart t;
tcbSchedEnqueue t
od) []) (IF NULL \<noteq> NULL THEN
  CALL setThreadState_'proc(NULL,SCAST(32 signed \<rightarrow> 32) ThreadState_Restart);;
CALL tcbSchedEnqueue_'proc(NULL);;
Guard C_Guard {s. s \<Turnstile>\<^sub>c NULL} (\<acute>thread :== h_val (hrs_mem \<acute>t_hrs) (PTR(tcb_C ptr) &(NULL\<rightarrow>[''tcbEPNext_C''])));;
While \<lbrace>\<acute>thread \<noteq> NULL\<rbrace> (CALL setThreadState_'proc(\<acute>thread,SCAST(32 signed \<rightarrow> 32) ThreadState_Restart);;
CALL tcbSchedEnqueue_'proc(\<acute>thread);;
Guard C_Guard {s. s \<Turnstile>\<^sub>c thread_' s} (\<acute>thread :== h_val (hrs_mem \<acute>t_hrs) (PTR(tcb_C ptr) &(\<acute>thread\<rightarrow>[''tcbEPNext_C'']))))
FI) proof (prove)
goal (1 subgoal):
 1. ccorres dc xfdc (\<lambda>s. valid_objs' s \<and> Invariants_H.valid_queues s \<and> sch_act_wf (ksSchedulerAction s) s) UNIV hs (return ()) SKIP proof (prove)
goal (1 subgoal):
 1. \<And>s s'. \<lbrakk>(s, s') \<in> rf_sr; valid_objs' s \<and> Invariants_H.valid_queues s \<and> sch_act_wf (ksSchedulerAction s) s; s' \<in> UNIV\<rbrakk> \<Longrightarrow> True \<and> s' \<in> UNIV proof (prove)
goal:
No subgoals! proof (state)
this:
ccorres dc xfdc (\<lambda>s. valid_objs' s \<and> Invariants_H.valid_queues s \<and> (\<forall>t\<in>set []. tcb_at' t s \<and> t \<noteq> 0) \<and> sch_act_wf (ksSchedulerAction s) s) {s'. \<exists>p. ep_queue_relation (cslift s') [] p (thread_' s')} hs (mapM_x (\<lambda>t. do y <- setThreadState Structures_H.thread_state.Restart t;
tcbSchedEnqueue t
od) []) (While \<lbrace>\<acute>thread \<noteq> NULL\<rbrace> (CALL setThreadState_'proc(\<acute>thread,SCAST(32 signed \<rightarrow> 32) ThreadState_Restart);;
CALL tcbSchedEnqueue_'proc(\<acute>thread);;
Guard C_Guard {s. s \<Turnstile>\<^sub>c thread_' s} (\<acute>thread :== h_val (hrs_mem \<acute>t_hrs) (PTR(tcb_C ptr) &(\<acute>thread\<rightarrow>[''tcbEPNext_C''])))))

goal (1 subgoal):
 1. \<And>x1 ts. ccorres dc xfdc (\<lambda>s. valid_objs' s \<and> Invariants_H.valid_queues s \<and> (\<forall>t\<in>set ts. tcb_at' t s \<and> t \<noteq> 0) \<and> sch_act_wf (ksSchedulerAction s) s) {s'. \<exists>p. ep_queue_relation (cslift s') ts p (thread_' s')} hs (mapM_x (\<lambda>t. do y <- setThreadState Structures_H.thread_state.Restart t;
tcbSchedEnqueue t
od) ts) (While \<lbrace>\<acute>thread \<noteq> NULL\<rbrace> (CALL setThreadState_'proc(\<acute>thread,SCAST(32 signed \<rightarrow> 32) ThreadState_Restart);;
CALL tcbSchedEnqueue_'proc(\<acute>thread);;
Guard C_Guard {s. s \<Turnstile>\<^sub>c thread_' s} (\<acute>thread :== h_val (hrs_mem \<acute>t_hrs) (PTR(tcb_C ptr) &(\<acute>thread\<rightarrow>[''tcbEPNext_C'']))))) \<Longrightarrow> ccorres dc xfdc (\<lambda>s. valid_objs' s \<and> Invariants_H.valid_queues s \<and> (\<forall>t\<in>set (x1 # ts). tcb_at' t s \<and> t \<noteq> 0) \<and> sch_act_wf (ksSchedulerAction s) s) {s'. \<exists>p. ep_queue_relation (cslift s') (x1 # ts) p (thread_' s')} hs (mapM_x (\<lambda>t. do y <- setThreadState Structures_H.thread_state.Restart t;
tcbSchedEnqueue t
od) (x1 # ts)) (While \<lbrace>\<acute>thread \<noteq> NULL\<rbrace> (CALL setThreadState_'proc(\<acute>thread,SCAST(32 signed \<rightarrow> 32) ThreadState_Restart);;
CALL tcbSchedEnqueue_'proc(\<acute>thread);;
Guard C_Guard {s. s \<Turnstile>\<^sub>c thread_' s} (\<acute>thread :== h_val (hrs_mem \<acute>t_hrs) (PTR(tcb_C ptr) &(\<acute>thread\<rightarrow>[''tcbEPNext_C'']))))) proof (state)
goal (1 subgoal):
 1. \<And>x1 ts. ccorres dc xfdc (\<lambda>s. valid_objs' s \<and> Invariants_H.valid_queues s \<and> (\<forall>t\<in>set ts. tcb_at' t s \<and> t \<noteq> 0) \<and> sch_act_wf (ksSchedulerAction s) s) {s'. \<exists>p. ep_queue_relation (cslift s') ts p (thread_' s')} hs (mapM_x (\<lambda>t. do y <- setThreadState Structures_H.thread_state.Restart t;
tcbSchedEnqueue t
od) ts) (While \<lbrace>\<acute>thread \<noteq> NULL\<rbrace> (CALL setThreadState_'proc(\<acute>thread,SCAST(32 signed \<rightarrow> 32) ThreadState_Restart);;
CALL tcbSchedEnqueue_'proc(\<acute>thread);;
Guard C_Guard {s. s \<Turnstile>\<^sub>c thread_' s} (\<acute>thread :== h_val (hrs_mem \<acute>t_hrs) (PTR(tcb_C ptr) &(\<acute>thread\<rightarrow>[''tcbEPNext_C'']))))) \<Longrightarrow> ccorres dc xfdc (\<lambda>s. valid_objs' s \<and> Invariants_H.valid_queues s \<and> (\<forall>t\<in>set (x1 # ts). tcb_at' t s \<and> t \<noteq> 0) \<and> sch_act_wf (ksSchedulerAction s) s) {s'. \<exists>p. ep_queue_relation (cslift s') (x1 # ts) p (thread_' s')} hs (mapM_x (\<lambda>t. do y <- setThreadState Structures_H.thread_state.Restart t;
tcbSchedEnqueue t
od) (x1 # ts)) (While \<lbrace>\<acute>thread \<noteq> NULL\<rbrace> (CALL setThreadState_'proc(\<acute>thread,SCAST(32 signed \<rightarrow> 32) ThreadState_Restart);;
CALL tcbSchedEnqueue_'proc(\<acute>thread);;
Guard C_Guard {s. s \<Turnstile>\<^sub>c thread_' s} (\<acute>thread :== h_val (hrs_mem \<acute>t_hrs) (PTR(tcb_C ptr) &(\<acute>thread\<rightarrow>[''tcbEPNext_C'']))))) proof (state)
this:
ccorres dc xfdc (\<lambda>s. valid_objs' s \<and> Invariants_H.valid_queues s \<and> (\<forall>t\<in>set threads. tcb_at' t s \<and> t \<noteq> 0) \<and> sch_act_wf (ksSchedulerAction s) s) {s'. \<exists>p. ep_queue_relation (cslift s') threads p (thread_' s')} hs (mapM_x (\<lambda>t. do y <- setThreadState Structures_H.thread_state.Restart t;
tcbSchedEnqueue t
od) threads) (While \<lbrace>\<acute>thread \<noteq> NULL\<rbrace> (CALL setThreadState_'proc(\<acute>thread,SCAST(32 signed \<rightarrow> 32) ThreadState_Restart);;
CALL tcbSchedEnqueue_'proc(\<acute>thread);;
Guard C_Guard {s. s \<Turnstile>\<^sub>c thread_' s} (\<acute>thread :== h_val (hrs_mem \<acute>t_hrs) (PTR(tcb_C ptr) &(\<acute>thread\<rightarrow>[''tcbEPNext_C''])))))

goal (1 subgoal):
 1. \<And>x1 ts. ccorres dc xfdc (\<lambda>s. valid_objs' s \<and> Invariants_H.valid_queues s \<and> (\<forall>t\<in>set ts. tcb_at' t s \<and> t \<noteq> 0) \<and> sch_act_wf (ksSchedulerAction s) s) {s'. \<exists>p. ep_queue_relation (cslift s') ts p (thread_' s')} hs (mapM_x (\<lambda>t. do y <- setThreadState Structures_H.thread_state.Restart t;
tcbSchedEnqueue t
od) ts) (While \<lbrace>\<acute>thread \<noteq> NULL\<rbrace> (CALL setThreadState_'proc(\<acute>thread,SCAST(32 signed \<rightarrow> 32) ThreadState_Restart);;
CALL tcbSchedEnqueue_'proc(\<acute>thread);;
Guard C_Guard {s. s \<Turnstile>\<^sub>c thread_' s} (\<acute>thread :== h_val (hrs_mem \<acute>t_hrs) (PTR(tcb_C ptr) &(\<acute>thread\<rightarrow>[''tcbEPNext_C'']))))) \<Longrightarrow> ccorres dc xfdc (\<lambda>s. valid_objs' s \<and> Invariants_H.valid_queues s \<and> (\<forall>t\<in>set (x1 # ts). tcb_at' t s \<and> t \<noteq> 0) \<and> sch_act_wf (ksSchedulerAction s) s) {s'. \<exists>p. ep_queue_relation (cslift s') (x1 # ts) p (thread_' s')} hs (mapM_x (\<lambda>t. do y <- setThreadState Structures_H.thread_state.Restart t;
tcbSchedEnqueue t
od) (x1 # ts)) (While \<lbrace>\<acute>thread \<noteq> NULL\<rbrace> (CALL setThreadState_'proc(\<acute>thread,SCAST(32 signed \<rightarrow> 32) ThreadState_Restart);;
CALL tcbSchedEnqueue_'proc(\<acute>thread);;
Guard C_Guard {s. s \<Turnstile>\<^sub>c thread_' s} (\<acute>thread :== h_val (hrs_mem \<acute>t_hrs) (PTR(tcb_C ptr) &(\<acute>thread\<rightarrow>[''tcbEPNext_C'']))))) proof (prove)
goal (1 subgoal):
 1. ccorres dc xfdc (\<lambda>s. valid_objs' s \<and> Invariants_H.valid_queues s \<and> (\<forall>t\<in>set (thread # threads). tcb_at' t s \<and> t \<noteq> 0) \<and> sch_act_wf (ksSchedulerAction s) s) {s'. \<exists>p. ep_queue_relation (cslift s') (thread # threads) p (thread_' s')} hs (mapM_x (\<lambda>t. do y <- setThreadState Structures_H.thread_state.Restart t;
tcbSchedEnqueue t
od) (thread # threads)) (While \<lbrace>\<acute>thread \<noteq> NULL\<rbrace> (CALL setThreadState_'proc(\<acute>thread,SCAST(32 signed \<rightarrow> 32) ThreadState_Restart);;
CALL tcbSchedEnqueue_'proc(\<acute>thread);;
Guard C_Guard {s. s \<Turnstile>\<^sub>c thread_' s} (\<acute>thread :== h_val (hrs_mem \<acute>t_hrs) (PTR(tcb_C ptr) &(\<acute>thread\<rightarrow>[''tcbEPNext_C'']))))) proof (prove)
goal (1 subgoal):
 1. ccorres dc xfdc (\<lambda>s. valid_objs' s \<and> Invariants_H.valid_queues s \<and> (\<forall>t\<in>set (thread # threads). tcb_at' t s \<and> t \<noteq> 0) \<and> sch_act_wf (ksSchedulerAction s) s) {s'. \<exists>p. ep_queue_relation (cslift s') (thread # threads) p (thread_' s')} hs (mapM_x (\<lambda>t. do y <- setThreadState Structures_H.thread_state.Restart t;
tcbSchedEnqueue t
od) (thread # threads)) (IF \<acute>thread \<noteq> NULL THEN
  CALL setThreadState_'proc(\<acute>thread,SCAST(32 signed \<rightarrow> 32) ThreadState_Restart);;
CALL tcbSchedEnqueue_'proc(\<acute>thread);;
Guard C_Guard {s. s \<Turnstile>\<^sub>c thread_' s} (\<acute>thread :== h_val (hrs_mem \<acute>t_hrs) (PTR(tcb_C ptr) &(\<acute>thread\<rightarrow>[''tcbEPNext_C''])));;
While \<lbrace>\<acute>thread \<noteq> NULL\<rbrace> (CALL setThreadState_'proc(\<acute>thread,SCAST(32 signed \<rightarrow> 32) ThreadState_Restart);;
CALL tcbSchedEnqueue_'proc(\<acute>thread);;
Guard C_Guard {s. s \<Turnstile>\<^sub>c thread_' s} (\<acute>thread :== h_val (hrs_mem \<acute>t_hrs) (PTR(tcb_C ptr) &(\<acute>thread\<rightarrow>[''tcbEPNext_C'']))))
FI) proof (prove)
goal (1 subgoal):
 1. ccorres dc xfdc (\<lambda>s. valid_objs' s \<and> Invariants_H.valid_queues s \<and> tcb_at' thread s \<and> thread \<noteq> 0 \<and> (\<forall>t\<in>set threads. tcb_at' t s \<and> t \<noteq> 0) \<and> sch_act_wf (ksSchedulerAction s) s) {s'. thread_' s' = tcb_ptr_to_ctcb_ptr thread \<and> (\<exists>tcb. cslift s' (thread_' s') = Some tcb \<and> ep_queue_relation (cslift s') threads (thread_' s') (tcbEPNext_C tcb))} hs (do y <- do y <- setThreadState Structures_H.thread_state.Restart thread;
tcbSchedEnqueue thread
od;
mapM_x (\<lambda>t. do y <- setThreadState Structures_H.thread_state.Restart t;
tcbSchedEnqueue t
od) threads
od) (IF \<acute>thread \<noteq> NULL THEN
  CALL setThreadState_'proc(\<acute>thread,SCAST(32 signed \<rightarrow> 32) ThreadState_Restart);;
CALL tcbSchedEnqueue_'proc(\<acute>thread);;
Guard C_Guard {s. s \<Turnstile>\<^sub>c thread_' s} (\<acute>thread :== h_val (hrs_mem \<acute>t_hrs) (PTR(tcb_C ptr) &(\<acute>thread\<rightarrow>[''tcbEPNext_C''])));;
While \<lbrace>\<acute>thread \<noteq> NULL\<rbrace> (CALL setThreadState_'proc(\<acute>thread,SCAST(32 signed \<rightarrow> 32) ThreadState_Restart);;
CALL tcbSchedEnqueue_'proc(\<acute>thread);;
Guard C_Guard {s. s \<Turnstile>\<^sub>c thread_' s} (\<acute>thread :== h_val (hrs_mem \<acute>t_hrs) (PTR(tcb_C ptr) &(\<acute>thread\<rightarrow>[''tcbEPNext_C'']))))
FI) proof (prove)
goal (2 subgoals):
 1. ccorres dc xfdc ?Q15 ?Q'15 hs (do y <- do y <- setThreadState Structures_H.thread_state.Restart thread;
tcbSchedEnqueue thread
od;
mapM_x (\<lambda>t. do y <- setThreadState Structures_H.thread_state.Restart t;
tcbSchedEnqueue t
od) threads
od) (IF \<acute>thread \<noteq> NULL THEN
  CALL setThreadState_'proc(\<acute>thread,SCAST(32 signed \<rightarrow> 32) ThreadState_Restart);;
CALL tcbSchedEnqueue_'proc(\<acute>thread);;
Guard C_Guard {s. s \<Turnstile>\<^sub>c thread_' s} (\<acute>thread :== h_val (hrs_mem \<acute>t_hrs) (PTR(tcb_C ptr) &(\<acute>thread\<rightarrow>[''tcbEPNext_C''])));;
While \<lbrace>\<acute>thread \<noteq> NULL\<rbrace> (CALL setThreadState_'proc(\<acute>thread,SCAST(32 signed \<rightarrow> 32) ThreadState_Restart);;
CALL tcbSchedEnqueue_'proc(\<acute>thread);;
Guard C_Guard {s. s \<Turnstile>\<^sub>c thread_' s} (\<acute>thread :== h_val (hrs_mem \<acute>t_hrs) (PTR(tcb_C ptr) &(\<acute>thread\<rightarrow>[''tcbEPNext_C'']))))
FI)
 2. \<And>s s'. \<lbrakk>(s, s') \<in> rf_sr; valid_objs' s \<and> Invariants_H.valid_queues s \<and> tcb_at' thread s \<and> thread \<noteq> 0 \<and> (\<forall>t\<in>set threads. tcb_at' t s \<and> t \<noteq> 0) \<and> sch_act_wf (ksSchedulerAction s) s; s' \<in> {s'. thread_' s' = tcb_ptr_to_ctcb_ptr thread \<and> (\<exists>tcb. cslift s' (thread_' s') = Some tcb \<and> ep_queue_relation (cslift s') threads (thread_' s') (tcbEPNext_C tcb))}\<rbrakk> \<Longrightarrow> ?Q15 s \<and> s' \<in> ?Q'15 proof (prove)
goal (3 subgoals):
 1. \<And>rv' t t'. ceqv \<Gamma> thread_' rv' t t' (IF \<acute>thread \<noteq> NULL THEN
  CALL setThreadState_'proc(\<acute>thread,SCAST(32 signed \<rightarrow> 32) ThreadState_Restart);;
CALL tcbSchedEnqueue_'proc(\<acute>thread);;
Guard C_Guard {s. s \<Turnstile>\<^sub>c thread_' s} (\<acute>thread :== h_val (hrs_mem \<acute>t_hrs) (PTR(tcb_C ptr) &(\<acute>thread\<rightarrow>[''tcbEPNext_C''])));;
While \<lbrace>\<acute>thread \<noteq> NULL\<rbrace> (CALL setThreadState_'proc(\<acute>thread,SCAST(32 signed \<rightarrow> 32) ThreadState_Restart);;
CALL tcbSchedEnqueue_'proc(\<acute>thread);;
Guard C_Guard {s. s \<Turnstile>\<^sub>c thread_' s} (\<acute>thread :== h_val (hrs_mem \<acute>t_hrs) (PTR(tcb_C ptr) &(\<acute>thread\<rightarrow>[''tcbEPNext_C'']))))
FI) (?d'18 rv')
 2. \<And>rv'. ccorres dc xfdc ?Q15 (?G'18 rv') hs (do y <- do y <- setThreadState Structures_H.thread_state.Restart thread;
tcbSchedEnqueue thread
od;
mapM_x (\<lambda>t. do y <- setThreadState Structures_H.thread_state.Restart t;
tcbSchedEnqueue t
od) threads
od) (?d'18 rv')
 3. \<And>s s'. \<lbrakk>(s, s') \<in> rf_sr; valid_objs' s \<and> Invariants_H.valid_queues s \<and> tcb_at' thread s \<and> thread \<noteq> 0 \<and> (\<forall>t\<in>set threads. tcb_at' t s \<and> t \<noteq> 0) \<and> sch_act_wf (ksSchedulerAction s) s; s' \<in> {s'. thread_' s' = tcb_ptr_to_ctcb_ptr thread \<and> (\<exists>tcb. cslift s' (thread_' s') = Some tcb \<and> ep_queue_relation (cslift s') threads (thread_' s') (tcbEPNext_C tcb))}\<rbrakk> \<Longrightarrow> ?Q15 s \<and> s' \<in> {s. s \<in> ?G'18 (thread_' s)} proof (prove)
goal (2 subgoals):
 1. \<And>rv'. ccorres dc xfdc ?Q15 (?G'18 rv') hs (do y <- do y <- setThreadState Structures_H.thread_state.Restart thread;
tcbSchedEnqueue thread
od;
mapM_x (\<lambda>t. do y <- setThreadState Structures_H.thread_state.Restart t;
tcbSchedEnqueue t
od) threads
od) (IF rv' \<noteq> NULL THEN
  CALL setThreadState_'proc(rv',SCAST(32 signed \<rightarrow> 32) ThreadState_Restart);;
CALL tcbSchedEnqueue_'proc(rv');;
Guard C_Guard {s. s \<Turnstile>\<^sub>c rv'} (\<acute>thread :== h_val (hrs_mem \<acute>t_hrs) (PTR(tcb_C ptr) &(rv'\<rightarrow>[''tcbEPNext_C''])));;
While \<lbrace>\<acute>thread \<noteq> NULL\<rbrace> (CALL setThreadState_'proc(\<acute>thread,SCAST(32 signed \<rightarrow> 32) ThreadState_Restart);;
CALL tcbSchedEnqueue_'proc(\<acute>thread);;
Guard C_Guard {s. s \<Turnstile>\<^sub>c thread_' s} (\<acute>thread :== h_val (hrs_mem \<acute>t_hrs) (PTR(tcb_C ptr) &(\<acute>thread\<rightarrow>[''tcbEPNext_C'']))))
FI)
 2. \<And>s s'. \<lbrakk>(s, s') \<in> rf_sr; valid_objs' s \<and> Invariants_H.valid_queues s \<and> tcb_at' thread s \<and> thread \<noteq> 0 \<and> (\<forall>t\<in>set threads. tcb_at' t s \<and> t \<noteq> 0) \<and> sch_act_wf (ksSchedulerAction s) s; s' \<in> {s'. thread_' s' = tcb_ptr_to_ctcb_ptr thread \<and> (\<exists>tcb. cslift s' (thread_' s') = Some tcb \<and> ep_queue_relation (cslift s') threads (thread_' s') (tcbEPNext_C tcb))}\<rbrakk> \<Longrightarrow> ?Q15 s \<and> s' \<in> {s. s \<in> ?G'18 (thread_' s)} proof (prove)
goal (2 subgoals):
 1. \<And>rv'. rv' = tcb_ptr_to_ctcb_ptr thread \<Longrightarrow> ccorres dc xfdc ?Q15 (?G'119 rv') hs (do y <- do y <- setThreadState Structures_H.thread_state.Restart thread;
tcbSchedEnqueue thread
od;
mapM_x (\<lambda>t. do y <- setThreadState Structures_H.thread_state.Restart t;
tcbSchedEnqueue t
od) threads
od) (IF rv' \<noteq> NULL THEN
  CALL setThreadState_'proc(rv',SCAST(32 signed \<rightarrow> 32) ThreadState_Restart);;
CALL tcbSchedEnqueue_'proc(rv');;
Guard C_Guard {s. s \<Turnstile>\<^sub>c rv'} (\<acute>thread :== h_val (hrs_mem \<acute>t_hrs) (PTR(tcb_C ptr) &(rv'\<rightarrow>[''tcbEPNext_C''])));;
While \<lbrace>\<acute>thread \<noteq> NULL\<rbrace> (CALL setThreadState_'proc(\<acute>thread,SCAST(32 signed \<rightarrow> 32) ThreadState_Restart);;
CALL tcbSchedEnqueue_'proc(\<acute>thread);;
Guard C_Guard {s. s \<Turnstile>\<^sub>c thread_' s} (\<acute>thread :== h_val (hrs_mem \<acute>t_hrs) (PTR(tcb_C ptr) &(\<acute>thread\<rightarrow>[''tcbEPNext_C'']))))
FI)
 2. \<And>s s'. \<lbrakk>(s, s') \<in> rf_sr; valid_objs' s \<and> Invariants_H.valid_queues s \<and> tcb_at' thread s \<and> thread \<noteq> 0 \<and> (\<forall>t\<in>set threads. tcb_at' t s \<and> t \<noteq> 0) \<and> sch_act_wf (ksSchedulerAction s) s; s' \<in> {s'. thread_' s' = tcb_ptr_to_ctcb_ptr thread \<and> (\<exists>tcb. cslift s' (thread_' s') = Some tcb \<and> ep_queue_relation (cslift s') threads (thread_' s') (tcbEPNext_C tcb))}\<rbrakk> \<Longrightarrow> ?Q15 s \<and> s' \<in> {s. s \<in> ?G'119 (thread_' s) \<inter> \<lbrace>\<^bsup>s\<^esup>thread = tcb_ptr_to_ctcb_ptr thread\<rbrace>} proof (prove)
goal (2 subgoals):
 1. \<And>rv'. \<lbrakk>rv' = tcb_ptr_to_ctcb_ptr thread; tcb_ptr_to_ctcb_ptr thread \<noteq> NULL\<rbrakk> \<Longrightarrow> ccorres dc xfdc ?G121 (?G'119 rv') hs (do y <- do y <- setThreadState Structures_H.thread_state.Restart thread;
tcbSchedEnqueue thread
od;
mapM_x (\<lambda>t. do y <- setThreadState Structures_H.thread_state.Restart t;
tcbSchedEnqueue t
od) threads
od) (IF rv' \<noteq> NULL THEN
  CALL setThreadState_'proc(rv',SCAST(32 signed \<rightarrow> 32) ThreadState_Restart);;
CALL tcbSchedEnqueue_'proc(rv');;
Guard C_Guard {s. s \<Turnstile>\<^sub>c rv'} (\<acute>thread :== h_val (hrs_mem \<acute>t_hrs) (PTR(tcb_C ptr) &(rv'\<rightarrow>[''tcbEPNext_C''])));;
While \<lbrace>\<acute>thread \<noteq> NULL\<rbrace> (CALL setThreadState_'proc(\<acute>thread,SCAST(32 signed \<rightarrow> 32) ThreadState_Restart);;
CALL tcbSchedEnqueue_'proc(\<acute>thread);;
Guard C_Guard {s. s \<Turnstile>\<^sub>c thread_' s} (\<acute>thread :== h_val (hrs_mem \<acute>t_hrs) (PTR(tcb_C ptr) &(\<acute>thread\<rightarrow>[''tcbEPNext_C'']))))
FI)
 2. \<And>s s'. \<lbrakk>(s, s') \<in> rf_sr; valid_objs' s \<and> Invariants_H.valid_queues s \<and> tcb_at' thread s \<and> thread \<noteq> 0 \<and> (\<forall>t\<in>set threads. tcb_at' t s \<and> t \<noteq> 0) \<and> sch_act_wf (ksSchedulerAction s) s; s' \<in> {s'. thread_' s' = tcb_ptr_to_ctcb_ptr thread \<and> (\<exists>tcb. cslift s' (thread_' s') = Some tcb \<and> ep_queue_relation (cslift s') threads (thread_' s') (tcbEPNext_C tcb))}\<rbrakk> \<Longrightarrow> (?G121 and (\<lambda>_. tcb_ptr_to_ctcb_ptr thread \<noteq> NULL)) s \<and> s' \<in> {s. s \<in> ?G'119 (thread_' s) \<inter> \<lbrace>\<^bsup>s\<^esup>thread = tcb_ptr_to_ctcb_ptr thread\<rbrace>} proof (prove)
goal (2 subgoals):
 1. tcb_ptr_to_ctcb_ptr thread \<noteq> NULL \<Longrightarrow> ccorres dc xfdc ?G121 (?G'119 (tcb_ptr_to_ctcb_ptr thread)) hs (do y <- do y <- setThreadState Structures_H.thread_state.Restart thread;
tcbSchedEnqueue thread
od;
mapM_x (\<lambda>t. do y <- setThreadState Structures_H.thread_state.Restart t;
tcbSchedEnqueue t
od) threads
od) (CALL setThreadState_'proc(tcb_ptr_to_ctcb_ptr thread,SCAST(32 signed \<rightarrow> 32) ThreadState_Restart);;
CALL tcbSchedEnqueue_'proc(tcb_ptr_to_ctcb_ptr thread);;
Guard C_Guard {s. s \<Turnstile>\<^sub>c tcb_ptr_to_ctcb_ptr thread} (\<acute>thread :== h_val (hrs_mem \<acute>t_hrs) (PTR(tcb_C ptr) &(tcb_ptr_to_ctcb_ptr thread\<rightarrow>[''tcbEPNext_C''])));;
While \<lbrace>\<acute>thread \<noteq> NULL\<rbrace> (CALL setThreadState_'proc(\<acute>thread,SCAST(32 signed \<rightarrow> 32) ThreadState_Restart);;
CALL tcbSchedEnqueue_'proc(\<acute>thread);;
Guard C_Guard {s. s \<Turnstile>\<^sub>c thread_' s} (\<acute>thread :== h_val (hrs_mem \<acute>t_hrs) (PTR(tcb_C ptr) &(\<acute>thread\<rightarrow>[''tcbEPNext_C''])))))
 2. \<And>s s'. \<lbrakk>(s, s') \<in> rf_sr; valid_objs' s \<and> Invariants_H.valid_queues s \<and> tcb_at' thread s \<and> thread \<noteq> 0 \<and> (\<forall>t\<in>set threads. tcb_at' t s \<and> t \<noteq> 0) \<and> sch_act_wf (ksSchedulerAction s) s; s' \<in> {s'. thread_' s' = tcb_ptr_to_ctcb_ptr thread \<and> (\<exists>tcb. cslift s' (thread_' s') = Some tcb \<and> ep_queue_relation (cslift s') threads (thread_' s') (tcbEPNext_C tcb))}\<rbrakk> \<Longrightarrow> (?G121 and (\<lambda>_. tcb_ptr_to_ctcb_ptr thread \<noteq> NULL)) s \<and> s' \<in> {s. s \<in> ?G'119 (thread_' s) \<inter> \<lbrace>\<^bsup>s\<^esup>thread = tcb_ptr_to_ctcb_ptr thread\<rbrace>} proof (prove)
goal (6 subgoals):
 1. tcb_ptr_to_ctcb_ptr thread \<noteq> NULL \<Longrightarrow> ccorres dc xfdc ?P130 (?P'133 (tcb_ptr_to_ctcb_ptr thread)) hs (do y <- setThreadState Structures_H.thread_state.Restart thread;
tcbSchedEnqueue thread
od) (CALL setThreadState_'proc(tcb_ptr_to_ctcb_ptr thread,SCAST(32 signed \<rightarrow> 32) ThreadState_Restart);;
CALL tcbSchedEnqueue_'proc(tcb_ptr_to_ctcb_ptr thread);;
Guard C_Guard {s. s \<Turnstile>\<^sub>c tcb_ptr_to_ctcb_ptr thread} (\<acute>thread :== h_val (hrs_mem \<acute>t_hrs) (PTR(tcb_C ptr) &(tcb_ptr_to_ctcb_ptr thread\<rightarrow>[''tcbEPNext_C'']))))
 2. \<And>rv' t t'. tcb_ptr_to_ctcb_ptr thread \<noteq> NULL \<Longrightarrow> ceqv \<Gamma> xfdc rv' t t' (While \<lbrace>\<acute>thread \<noteq> NULL\<rbrace> (CALL setThreadState_'proc(\<acute>thread,SCAST(32 signed \<rightarrow> 32) ThreadState_Restart);;
CALL tcbSchedEnqueue_'proc(\<acute>thread);;
Guard C_Guard {s. s \<Turnstile>\<^sub>c thread_' s} (\<acute>thread :== h_val (hrs_mem \<acute>t_hrs) (PTR(tcb_C ptr) &(\<acute>thread\<rightarrow>[''tcbEPNext_C'']))))) (?d'130 rv')
 3. \<And>rv rv'. \<lbrakk>tcb_ptr_to_ctcb_ptr thread \<noteq> NULL; dc rv rv'\<rbrakk> \<Longrightarrow> ccorres dc xfdc (?Q130 rv) (?Q'130 rv rv') hs (mapM_x (\<lambda>t. do y <- setThreadState Structures_H.thread_state.Restart t;
tcbSchedEnqueue t
od) threads) (?d'130 rv')
 4. tcb_ptr_to_ctcb_ptr thread \<noteq> NULL \<Longrightarrow> \<lbrace>?R130\<rbrace> do y <- setThreadState Structures_H.thread_state.Restart thread;
tcbSchedEnqueue thread
od \<lbrace>?Q130\<rbrace>
 5. tcb_ptr_to_ctcb_ptr thread \<noteq> NULL \<Longrightarrow> \<Gamma>\<turnstile>\<^bsub>/UNIV\<^esub> (?R'132 (tcb_ptr_to_ctcb_ptr thread)) CALL setThreadState_'proc(tcb_ptr_to_ctcb_ptr thread,SCAST(32 signed \<rightarrow> 32) ThreadState_Restart);;
CALL tcbSchedEnqueue_'proc(tcb_ptr_to_ctcb_ptr thread);;
Guard C_Guard {s. s \<Turnstile>\<^sub>c tcb_ptr_to_ctcb_ptr thread} (\<acute>thread :== h_val (hrs_mem \<acute>t_hrs) (PTR(tcb_C ptr) &(tcb_ptr_to_ctcb_ptr thread\<rightarrow>[''tcbEPNext_C'']))) {s. \<forall>rv. dc rv (xfdc s) \<longrightarrow> s \<in> ?Q'130 rv (xfdc s)}
 6. \<And>s s'. \<lbrakk>(s, s') \<in> rf_sr; valid_objs' s \<and> Invariants_H.valid_queues s \<and> tcb_at' thread s \<and> thread \<noteq> 0 \<and> (\<forall>t\<in>set threads. tcb_at' t s \<and> t \<noteq> 0) \<and> sch_act_wf (ksSchedulerAction s) s; s' \<in> {s'. thread_' s' = tcb_ptr_to_ctcb_ptr thread \<and> (\<exists>tcb. cslift s' (thread_' s') = Some tcb \<and> ep_queue_relation (cslift s') threads (thread_' s') (tcbEPNext_C tcb))}\<rbrakk> \<Longrightarrow> (?P130 and ?R130 and (\<lambda>_. tcb_ptr_to_ctcb_ptr thread \<noteq> NULL)) s \<and> s' \<in> {s. s \<in> ?P'133 (thread_' s) \<inter> ?R'132 (thread_' s) \<inter> \<lbrace>\<^bsup>s\<^esup>thread = tcb_ptr_to_ctcb_ptr thread\<rbrace>} proof (prove)
goal (6 subgoals):
 1. tcb_ptr_to_ctcb_ptr thread \<noteq> NULL \<Longrightarrow> ccorres dc xfdc ?P130 (?P'133 (tcb_ptr_to_ctcb_ptr thread)) hs (do y <- setThreadState Structures_H.thread_state.Restart thread;
tcbSchedEnqueue thread
od) (CALL setThreadState_'proc(tcb_ptr_to_ctcb_ptr thread,SCAST(32 signed \<rightarrow> 32) ThreadState_Restart);;
(CALL tcbSchedEnqueue_'proc(tcb_ptr_to_ctcb_ptr thread);;
Guard C_Guard {s. s \<Turnstile>\<^sub>c tcb_ptr_to_ctcb_ptr thread} (\<acute>thread :== h_val (hrs_mem \<acute>t_hrs) (PTR(tcb_C ptr) &(tcb_ptr_to_ctcb_ptr thread\<rightarrow>[''tcbEPNext_C''])))))
 2. \<And>rv' t t'. tcb_ptr_to_ctcb_ptr thread \<noteq> NULL \<Longrightarrow> ceqv \<Gamma> xfdc rv' t t' (While \<lbrace>\<acute>thread \<noteq> NULL\<rbrace> (CALL setThreadState_'proc(\<acute>thread,SCAST(32 signed \<rightarrow> 32) ThreadState_Restart);;
CALL tcbSchedEnqueue_'proc(\<acute>thread);;
Guard C_Guard {s. s \<Turnstile>\<^sub>c thread_' s} (\<acute>thread :== h_val (hrs_mem \<acute>t_hrs) (PTR(tcb_C ptr) &(\<acute>thread\<rightarrow>[''tcbEPNext_C'']))))) (?d'130 rv')
 3. \<And>rv rv'. \<lbrakk>tcb_ptr_to_ctcb_ptr thread \<noteq> NULL; dc rv rv'\<rbrakk> \<Longrightarrow> ccorres dc xfdc (?Q130 rv) (?Q'130 rv rv') hs (mapM_x (\<lambda>t. do y <- setThreadState Structures_H.thread_state.Restart t;
tcbSchedEnqueue t
od) threads) (?d'130 rv')
 4. tcb_ptr_to_ctcb_ptr thread \<noteq> NULL \<Longrightarrow> \<lbrace>?R130\<rbrace> do y <- setThreadState Structures_H.thread_state.Restart thread;
tcbSchedEnqueue thread
od \<lbrace>?Q130\<rbrace>
 5. tcb_ptr_to_ctcb_ptr thread \<noteq> NULL \<Longrightarrow> \<Gamma>\<turnstile>\<^bsub>/UNIV\<^esub> (?R'132 (tcb_ptr_to_ctcb_ptr thread)) CALL setThreadState_'proc(tcb_ptr_to_ctcb_ptr thread,SCAST(32 signed \<rightarrow> 32) ThreadState_Restart);;
CALL tcbSchedEnqueue_'proc(tcb_ptr_to_ctcb_ptr thread);;
Guard C_Guard {s. s \<Turnstile>\<^sub>c tcb_ptr_to_ctcb_ptr thread} (\<acute>thread :== h_val (hrs_mem \<acute>t_hrs) (PTR(tcb_C ptr) &(tcb_ptr_to_ctcb_ptr thread\<rightarrow>[''tcbEPNext_C'']))) {s. \<forall>rv. dc rv (xfdc s) \<longrightarrow> s \<in> ?Q'130 rv (xfdc s)}
 6. \<And>s s'. \<lbrakk>(s, s') \<in> rf_sr; valid_objs' s \<and> Invariants_H.valid_queues s \<and> tcb_at' thread s \<and> thread \<noteq> 0 \<and> (\<forall>t\<in>set threads. tcb_at' t s \<and> t \<noteq> 0) \<and> sch_act_wf (ksSchedulerAction s) s; s' \<in> {s'. thread_' s' = tcb_ptr_to_ctcb_ptr thread \<and> (\<exists>tcb. cslift s' (thread_' s') = Some tcb \<and> ep_queue_relation (cslift s') threads (thread_' s') (tcbEPNext_C tcb))}\<rbrakk> \<Longrightarrow> (?P130 and ?R130 and (\<lambda>_. tcb_ptr_to_ctcb_ptr thread \<noteq> NULL)) s \<and> s' \<in> {s. s \<in> ?P'133 (thread_' s) \<inter> ?R'132 (thread_' s) \<inter> \<lbrace>\<^bsup>s\<^esup>thread = tcb_ptr_to_ctcb_ptr thread\<rbrace>} proof (prove)
goal (7 subgoals):
 1. \<And>rv xfdca. \<lbrakk>tcb_ptr_to_ctcb_ptr thread \<noteq> NULL; dc rv xfdca\<rbrakk> \<Longrightarrow> ccorres dc xfdc (?Q137 rv) (?Q'137 rv xfdca) hs (tcbSchedEnqueue thread) (CALL tcbSchedEnqueue_'proc(tcb_ptr_to_ctcb_ptr thread);;
Guard C_Guard {s. s \<Turnstile>\<^sub>c tcb_ptr_to_ctcb_ptr thread} (\<acute>thread :== h_val (hrs_mem \<acute>t_hrs) (PTR(tcb_C ptr) &(tcb_ptr_to_ctcb_ptr thread\<rightarrow>[''tcbEPNext_C'']))))
 2. tcb_ptr_to_ctcb_ptr thread \<noteq> NULL \<Longrightarrow> \<lbrace>?R137\<rbrace> setThreadState Structures_H.thread_state.Restart thread \<lbrace>?Q137\<rbrace>
 3. \<And>rv' t t'. tcb_ptr_to_ctcb_ptr thread \<noteq> NULL \<Longrightarrow> ceqv \<Gamma> xfdc rv' t t' (While \<lbrace>\<acute>thread \<noteq> NULL\<rbrace> (CALL setThreadState_'proc(\<acute>thread,SCAST(32 signed \<rightarrow> 32) ThreadState_Restart);;
CALL tcbSchedEnqueue_'proc(\<acute>thread);;
Guard C_Guard {s. s \<Turnstile>\<^sub>c thread_' s} (\<acute>thread :== h_val (hrs_mem \<acute>t_hrs) (PTR(tcb_C ptr) &(\<acute>thread\<rightarrow>[''tcbEPNext_C'']))))) (?d'130 rv')
 4. \<And>rv rv'. \<lbrakk>tcb_ptr_to_ctcb_ptr thread \<noteq> NULL; dc rv rv'\<rbrakk> \<Longrightarrow> ccorres dc xfdc (?Q130 rv) (?Q'130 rv rv') hs (mapM_x (\<lambda>t. do y <- setThreadState Structures_H.thread_state.Restart t;
tcbSchedEnqueue t
od) threads) (?d'130 rv')
 5. tcb_ptr_to_ctcb_ptr thread \<noteq> NULL \<Longrightarrow> \<lbrace>?R130\<rbrace> do y <- setThreadState Structures_H.thread_state.Restart thread;
tcbSchedEnqueue thread
od \<lbrace>?Q130\<rbrace>
 6. tcb_ptr_to_ctcb_ptr thread \<noteq> NULL \<Longrightarrow> \<Gamma>\<turnstile>\<^bsub>/UNIV\<^esub> (?R'132 (tcb_ptr_to_ctcb_ptr thread)) CALL setThreadState_'proc(tcb_ptr_to_ctcb_ptr thread,SCAST(32 signed \<rightarrow> 32) ThreadState_Restart);;
CALL tcbSchedEnqueue_'proc(tcb_ptr_to_ctcb_ptr thread);;
Guard C_Guard {s. s \<Turnstile>\<^sub>c tcb_ptr_to_ctcb_ptr thread} (\<acute>thread :== h_val (hrs_mem \<acute>t_hrs) (PTR(tcb_C ptr) &(tcb_ptr_to_ctcb_ptr thread\<rightarrow>[''tcbEPNext_C'']))) {s. \<forall>rv. dc rv (xfdc s) \<longrightarrow> s \<in> ?Q'130 rv (xfdc s)}
 7. \<And>s s'. \<lbrakk>(s, s') \<in> rf_sr; valid_objs' s \<and> Invariants_H.valid_queues s \<and> tcb_at' thread s \<and> thread \<noteq> 0 \<and> (\<forall>t\<in>set threads. tcb_at' t s \<and> t \<noteq> 0) \<and> sch_act_wf (ksSchedulerAction s) s; s' \<in> {s'. thread_' s' = tcb_ptr_to_ctcb_ptr thread \<and> (\<exists>tcb. cslift s' (thread_' s') = Some tcb \<and> ep_queue_relation (cslift s') threads (thread_' s') (tcbEPNext_C tcb))}\<rbrakk> \<Longrightarrow> ((\<lambda>s. tcb_at' thread s \<and> Invariants_H.valid_queues s \<and> valid_objs' s \<and> valid_tcb_state' Structures_H.thread_state.Restart s \<and> (ksSchedulerAction s = SwitchToThread thread \<longrightarrow> runnable' Structures_H.thread_state.Restart) \<and> (\<forall>p. thread \<in> set (ksReadyQueues s p) \<longrightarrow> runnable' Structures_H.thread_state.Restart) \<and> sch_act_wf (ksSchedulerAction s) s) and ?R137 and ?R130 and (\<lambda>_. tcb_ptr_to_ctcb_ptr thread \<noteq> NULL)) s \<and> s' \<in> {s. s \<in> {sa. ts_'_update (\<lambda>_. SCAST(32 signed \<rightarrow> 32) ThreadState_Restart) (tptr_'_update (\<lambda>_. thread_' s) sa) \<in> \<lbrace>\<forall>cl fl. cthread_state_relation_lifted Structures_H.thread_state.Restart (cl\<lparr>tsType_CL := \<acute>ts && mask 4\<rparr>, fl)\<rbrace> \<inter> \<lbrace>\<acute>tptr = \<^bsup>s\<^esup>thread\<rbrace>} \<inter> {s'. \<forall>t rv. dc rv (xfdc t) \<longrightarrow> s'\<lparr>globals := globals t\<rparr> \<in> ?Q'141 (thread_' s) t rv} \<inter> ?R'132 (thread_' s) \<inter> \<lbrace>\<^bsup>s\<^esup>thread = tcb_ptr_to_ctcb_ptr thread\<rbrace>}
flex-flex pairs:
?Q'141 (tcb_ptr_to_ctcb_ptr thread) \<equiv>\<^sup>? \<lambda>t rv. ?Q'137 rv (xfdc t) proof (prove)
goal (7 subgoals):
 1. \<And>rv xfdca. \<lbrakk>tcb_ptr_to_ctcb_ptr thread \<noteq> NULL; dc rv xfdca\<rbrakk> \<Longrightarrow> ccorres dc xfdc (?Q137 rv) (?Q'137 rv xfdca) hs (tcbSchedEnqueue thread >>= return) (CALL tcbSchedEnqueue_'proc(tcb_ptr_to_ctcb_ptr thread);;
Guard C_Guard {s. s \<Turnstile>\<^sub>c tcb_ptr_to_ctcb_ptr thread} (\<acute>thread :== h_val (hrs_mem \<acute>t_hrs) (PTR(tcb_C ptr) &(tcb_ptr_to_ctcb_ptr thread\<rightarrow>[''tcbEPNext_C'']))))
 2. tcb_ptr_to_ctcb_ptr thread \<noteq> NULL \<Longrightarrow> \<lbrace>?R137\<rbrace> setThreadState Structures_H.thread_state.Restart thread \<lbrace>?Q137\<rbrace>
 3. \<And>rv' t t'. tcb_ptr_to_ctcb_ptr thread \<noteq> NULL \<Longrightarrow> ceqv \<Gamma> xfdc rv' t t' (While \<lbrace>\<acute>thread \<noteq> NULL\<rbrace> (CALL setThreadState_'proc(\<acute>thread,SCAST(32 signed \<rightarrow> 32) ThreadState_Restart);;
CALL tcbSchedEnqueue_'proc(\<acute>thread);;
Guard C_Guard {s. s \<Turnstile>\<^sub>c thread_' s} (\<acute>thread :== h_val (hrs_mem \<acute>t_hrs) (PTR(tcb_C ptr) &(\<acute>thread\<rightarrow>[''tcbEPNext_C'']))))) (?d'130 rv')
 4. \<And>rv rv'. \<lbrakk>tcb_ptr_to_ctcb_ptr thread \<noteq> NULL; dc rv rv'\<rbrakk> \<Longrightarrow> ccorres dc xfdc (?Q130 rv) (?Q'130 rv rv') hs (mapM_x (\<lambda>t. do y <- setThreadState Structures_H.thread_state.Restart t;
tcbSchedEnqueue t
od) threads) (?d'130 rv')
 5. tcb_ptr_to_ctcb_ptr thread \<noteq> NULL \<Longrightarrow> \<lbrace>?R130\<rbrace> do y <- setThreadState Structures_H.thread_state.Restart thread;
tcbSchedEnqueue thread
od \<lbrace>?Q130\<rbrace>
 6. tcb_ptr_to_ctcb_ptr thread \<noteq> NULL \<Longrightarrow> \<Gamma>\<turnstile>\<^bsub>/UNIV\<^esub> (?R'132 (tcb_ptr_to_ctcb_ptr thread)) CALL setThreadState_'proc(tcb_ptr_to_ctcb_ptr thread,SCAST(32 signed \<rightarrow> 32) ThreadState_Restart);;
CALL tcbSchedEnqueue_'proc(tcb_ptr_to_ctcb_ptr thread);;
Guard C_Guard {s. s \<Turnstile>\<^sub>c tcb_ptr_to_ctcb_ptr thread} (\<acute>thread :== h_val (hrs_mem \<acute>t_hrs) (PTR(tcb_C ptr) &(tcb_ptr_to_ctcb_ptr thread\<rightarrow>[''tcbEPNext_C'']))) {s. \<forall>rv. dc rv (xfdc s) \<longrightarrow> s \<in> ?Q'130 rv (xfdc s)}
 7. \<And>s s'. \<lbrakk>(s, s') \<in> rf_sr; valid_objs' s \<and> Invariants_H.valid_queues s \<and> tcb_at' thread s \<and> thread \<noteq> 0 \<and> (\<forall>t\<in>set threads. tcb_at' t s \<and> t \<noteq> 0) \<and> sch_act_wf (ksSchedulerAction s) s; s' \<in> {s'. thread_' s' = tcb_ptr_to_ctcb_ptr thread \<and> (\<exists>tcb. cslift s' (thread_' s') = Some tcb \<and> ep_queue_relation (cslift s') threads (thread_' s') (tcbEPNext_C tcb))}\<rbrakk> \<Longrightarrow> ((\<lambda>s. tcb_at' thread s \<and> Invariants_H.valid_queues s \<and> valid_objs' s \<and> valid_tcb_state' Structures_H.thread_state.Restart s \<and> (ksSchedulerAction s = SwitchToThread thread \<longrightarrow> runnable' Structures_H.thread_state.Restart) \<and> (\<forall>p. thread \<in> set (ksReadyQueues s p) \<longrightarrow> runnable' Structures_H.thread_state.Restart) \<and> sch_act_wf (ksSchedulerAction s) s) and ?R137 and ?R130 and (\<lambda>_. tcb_ptr_to_ctcb_ptr thread \<noteq> NULL)) s \<and> s' \<in> {s. s \<in> {sa. ts_'_update (\<lambda>_. SCAST(32 signed \<rightarrow> 32) ThreadState_Restart) (tptr_'_update (\<lambda>_. thread_' s) sa) \<in> \<lbrace>\<forall>cl fl. cthread_state_relation_lifted Structures_H.thread_state.Restart (cl\<lparr>tsType_CL := \<acute>ts && mask 4\<rparr>, fl)\<rbrace> \<inter> \<lbrace>\<acute>tptr = \<^bsup>s\<^esup>thread\<rbrace>} \<inter> {s'. \<forall>t rv. dc rv (xfdc t) \<longrightarrow> s'\<lparr>globals := globals t\<rparr> \<in> ?Q'141 (thread_' s) t rv} \<inter> ?R'132 (thread_' s) \<inter> \<lbrace>\<^bsup>s\<^esup>thread = tcb_ptr_to_ctcb_ptr thread\<rbrace>}
flex-flex pairs:
?Q'141 (tcb_ptr_to_ctcb_ptr thread) \<equiv>\<^sup>? \<lambda>t rv. ?Q'137 rv (xfdc t) proof (prove)
goal (8 subgoals):
 1. \<And>rv xfdca rva xfdcb. \<lbrakk>tcb_ptr_to_ctcb_ptr thread \<noteq> NULL; dc rv xfdca; dc rva xfdcb\<rbrakk> \<Longrightarrow> ccorres dc xfdc (?Q174 rv xfdca rva) (?Q'174 rv xfdca rva xfdcb) hs (return rva) (Guard C_Guard {s. s \<Turnstile>\<^sub>c tcb_ptr_to_ctcb_ptr thread} (\<acute>thread :== h_val (hrs_mem \<acute>t_hrs) (PTR(tcb_C ptr) &(tcb_ptr_to_ctcb_ptr thread\<rightarrow>[''tcbEPNext_C'']))))
 2. \<And>rv xfdc. \<lbrakk>tcb_ptr_to_ctcb_ptr thread \<noteq> NULL; dc rv xfdc\<rbrakk> \<Longrightarrow> \<lbrace>?R181 rv\<rbrace> tcbSchedEnqueue thread \<lbrace>?Q174 rv xfdc\<rbrace>
 3. tcb_ptr_to_ctcb_ptr thread \<noteq> NULL \<Longrightarrow> \<lbrace>?R137\<rbrace> setThreadState Structures_H.thread_state.Restart thread \<lbrace>\<lambda>a. Invariants_H.valid_queues and tcb_at' thread and valid_objs' and ?R181 a\<rbrace>
 4. \<And>rv' t t'. tcb_ptr_to_ctcb_ptr thread \<noteq> NULL \<Longrightarrow> ceqv \<Gamma> xfdc rv' t t' (While \<lbrace>\<acute>thread \<noteq> NULL\<rbrace> (CALL setThreadState_'proc(\<acute>thread,SCAST(32 signed \<rightarrow> 32) ThreadState_Restart);;
CALL tcbSchedEnqueue_'proc(\<acute>thread);;
Guard C_Guard {s. s \<Turnstile>\<^sub>c thread_' s} (\<acute>thread :== h_val (hrs_mem \<acute>t_hrs) (PTR(tcb_C ptr) &(\<acute>thread\<rightarrow>[''tcbEPNext_C'']))))) (?d'130 rv')
 5. \<And>rv rv'. \<lbrakk>tcb_ptr_to_ctcb_ptr thread \<noteq> NULL; dc rv rv'\<rbrakk> \<Longrightarrow> ccorres dc xfdc (?Q130 rv) (?Q'130 rv rv') hs (mapM_x (\<lambda>t. do y <- setThreadState Structures_H.thread_state.Restart t;
tcbSchedEnqueue t
od) threads) (?d'130 rv')
 6. tcb_ptr_to_ctcb_ptr thread \<noteq> NULL \<Longrightarrow> \<lbrace>?R130\<rbrace> do y <- setThreadState Structures_H.thread_state.Restart thread;
tcbSchedEnqueue thread
od \<lbrace>?Q130\<rbrace>
 7. tcb_ptr_to_ctcb_ptr thread \<noteq> NULL \<Longrightarrow> \<Gamma>\<turnstile>\<^bsub>/UNIV\<^esub> (?R'132 (tcb_ptr_to_ctcb_ptr thread)) CALL setThreadState_'proc(tcb_ptr_to_ctcb_ptr thread,SCAST(32 signed \<rightarrow> 32) ThreadState_Restart);;
CALL tcbSchedEnqueue_'proc(tcb_ptr_to_ctcb_ptr thread);;
Guard C_Guard {s. s \<Turnstile>\<^sub>c tcb_ptr_to_ctcb_ptr thread} (\<acute>thread :== h_val (hrs_mem \<acute>t_hrs) (PTR(tcb_C ptr) &(tcb_ptr_to_ctcb_ptr thread\<rightarrow>[''tcbEPNext_C'']))) {s. \<forall>rv. dc rv (xfdc s) \<longrightarrow> s \<in> ?Q'130 rv (xfdc s)}
 8. \<And>s s'. \<lbrakk>(s, s') \<in> rf_sr; valid_objs' s \<and> Invariants_H.valid_queues s \<and> tcb_at' thread s \<and> thread \<noteq> 0 \<and> (\<forall>t\<in>set threads. tcb_at' t s \<and> t \<noteq> 0) \<and> sch_act_wf (ksSchedulerAction s) s; s' \<in> {s'. thread_' s' = tcb_ptr_to_ctcb_ptr thread \<and> (\<exists>tcb. cslift s' (thread_' s') = Some tcb \<and> ep_queue_relation (cslift s') threads (thread_' s') (tcbEPNext_C tcb))}\<rbrakk> \<Longrightarrow> ((\<lambda>s. tcb_at' thread s \<and> Invariants_H.valid_queues s \<and> valid_objs' s \<and> valid_tcb_state' Structures_H.thread_state.Restart s \<and> (ksSchedulerAction s = SwitchToThread thread \<longrightarrow> runnable' Structures_H.thread_state.Restart) \<and> (\<forall>p. thread \<in> set (ksReadyQueues s p) \<longrightarrow> runnable' Structures_H.thread_state.Restart) \<and> sch_act_wf (ksSchedulerAction s) s) and ?R137 and ?R130 and (\<lambda>_. tcb_ptr_to_ctcb_ptr thread \<noteq> NULL)) s \<and> s' \<in> {s. s \<in> {sa. ts_'_update (\<lambda>_. SCAST(32 signed \<rightarrow> 32) ThreadState_Restart) (tptr_'_update (\<lambda>_. thread_' s) sa) \<in> \<lbrace>\<forall>cl fl. cthread_state_relation_lifted Structures_H.thread_state.Restart (cl\<lparr>tsType_CL := \<acute>ts && mask 4\<rparr>, fl)\<rbrace> \<inter> \<lbrace>\<acute>tptr = \<^bsup>s\<^esup>thread\<rbrace>} \<inter> {s'. \<forall>t rv. dc rv (xfdc t) \<longrightarrow> s'\<lparr>globals := globals t\<rparr> \<in> {sa. tcb_'_update (\<lambda>_. thread_' s) sa \<in> UNIV \<inter> \<lbrace>\<acute>tcb = \<^bsup>s\<^esup>thread\<rbrace>} \<inter> {s'. \<forall>ta rva. dc rva (xfdc ta) \<longrightarrow> s'\<lparr>globals := globals ta\<rparr> \<in> ?Q'184 (thread_' s) t rv ta rva}} \<inter> ?R'132 (thread_' s) \<inter> \<lbrace>\<^bsup>s\<^esup>thread = tcb_ptr_to_ctcb_ptr thread\<rbrace>}
flex-flex pairs:
?Q'184 (tcb_ptr_to_ctcb_ptr thread) \<equiv>\<^sup>? \<lambda>t rv ta rva. ?Q'174 rv (xfdc t) rva (xfdc ta) proof (prove)
goal (8 subgoals):
 1. \<And>rv xfdca rva xfdcb. \<lbrakk>tcb_ptr_to_ctcb_ptr thread \<noteq> NULL; dc rv xfdca; dc rva xfdcb\<rbrakk> \<Longrightarrow> \<forall>\<sigma>. \<Gamma>\<turnstile> {s. tcb_at' thread \<sigma> \<and> s \<in> UNIV \<and> (\<sigma>, s) \<in> rf_sr} Guard C_Guard {s. s \<Turnstile>\<^sub>c tcb_ptr_to_ctcb_ptr thread} (\<acute>thread :== h_val (hrs_mem \<acute>t_hrs) (PTR(tcb_C ptr) &(tcb_ptr_to_ctcb_ptr thread\<rightarrow>[''tcbEPNext_C'']))) {s. \<exists>(rv, \<sigma>')\<in>fst (return rva \<sigma>). (\<sigma>', s) \<in> rf_sr \<and> dc rv (xfdc s)}
 2. \<And>rv xfdc. \<lbrakk>tcb_ptr_to_ctcb_ptr thread \<noteq> NULL; dc rv xfdc\<rbrakk> \<Longrightarrow> \<lbrace>?R181 rv\<rbrace> tcbSchedEnqueue thread \<lbrace>\<lambda>a. tcb_at' thread\<rbrace>
 3. tcb_ptr_to_ctcb_ptr thread \<noteq> NULL \<Longrightarrow> \<lbrace>?R137\<rbrace> setThreadState Structures_H.thread_state.Restart thread \<lbrace>\<lambda>a. Invariants_H.valid_queues and tcb_at' thread and valid_objs' and ?R181 a\<rbrace>
 4. \<And>rv' t t'. tcb_ptr_to_ctcb_ptr thread \<noteq> NULL \<Longrightarrow> ceqv \<Gamma> xfdc rv' t t' (While \<lbrace>\<acute>thread \<noteq> NULL\<rbrace> (CALL setThreadState_'proc(\<acute>thread,SCAST(32 signed \<rightarrow> 32) ThreadState_Restart);;
CALL tcbSchedEnqueue_'proc(\<acute>thread);;
Guard C_Guard {s. s \<Turnstile>\<^sub>c thread_' s} (\<acute>thread :== h_val (hrs_mem \<acute>t_hrs) (PTR(tcb_C ptr) &(\<acute>thread\<rightarrow>[''tcbEPNext_C'']))))) (?d'130 rv')
 5. \<And>rv rv'. \<lbrakk>tcb_ptr_to_ctcb_ptr thread \<noteq> NULL; dc rv rv'\<rbrakk> \<Longrightarrow> ccorres dc xfdc (?Q130 rv) (?Q'130 rv rv') hs (mapM_x (\<lambda>t. do y <- setThreadState Structures_H.thread_state.Restart t;
tcbSchedEnqueue t
od) threads) (?d'130 rv')
 6. tcb_ptr_to_ctcb_ptr thread \<noteq> NULL \<Longrightarrow> \<lbrace>?R130\<rbrace> do y <- setThreadState Structures_H.thread_state.Restart thread;
tcbSchedEnqueue thread
od \<lbrace>?Q130\<rbrace>
 7. tcb_ptr_to_ctcb_ptr thread \<noteq> NULL \<Longrightarrow> \<Gamma>\<turnstile>\<^bsub>/UNIV\<^esub> (?R'132 (tcb_ptr_to_ctcb_ptr thread)) CALL setThreadState_'proc(tcb_ptr_to_ctcb_ptr thread,SCAST(32 signed \<rightarrow> 32) ThreadState_Restart);;
CALL tcbSchedEnqueue_'proc(tcb_ptr_to_ctcb_ptr thread);;
Guard C_Guard {s. s \<Turnstile>\<^sub>c tcb_ptr_to_ctcb_ptr thread} (\<acute>thread :== h_val (hrs_mem \<acute>t_hrs) (PTR(tcb_C ptr) &(tcb_ptr_to_ctcb_ptr thread\<rightarrow>[''tcbEPNext_C'']))) {s. \<forall>rv. dc rv (xfdc s) \<longrightarrow> s \<in> ?Q'130 rv (xfdc s)}
 8. \<And>s s'. \<lbrakk>(s, s') \<in> rf_sr; valid_objs' s \<and> Invariants_H.valid_queues s \<and> tcb_at' thread s \<and> thread \<noteq> 0 \<and> (\<forall>t\<in>set threads. tcb_at' t s \<and> t \<noteq> 0) \<and> sch_act_wf (ksSchedulerAction s) s; s' \<in> {s'. thread_' s' = tcb_ptr_to_ctcb_ptr thread \<and> (\<exists>tcb. cslift s' (thread_' s') = Some tcb \<and> ep_queue_relation (cslift s') threads (thread_' s') (tcbEPNext_C tcb))}\<rbrakk> \<Longrightarrow> ((\<lambda>s. tcb_at' thread s \<and> Invariants_H.valid_queues s \<and> valid_objs' s \<and> valid_tcb_state' Structures_H.thread_state.Restart s \<and> (ksSchedulerAction s = SwitchToThread thread \<longrightarrow> runnable' Structures_H.thread_state.Restart) \<and> (\<forall>p. thread \<in> set (ksReadyQueues s p) \<longrightarrow> runnable' Structures_H.thread_state.Restart) \<and> sch_act_wf (ksSchedulerAction s) s) and ?R137 and ?R130 and (\<lambda>_. tcb_ptr_to_ctcb_ptr thread \<noteq> NULL)) s \<and> s' \<in> {s. s \<in> {sa. ts_'_update (\<lambda>_. SCAST(32 signed \<rightarrow> 32) ThreadState_Restart) (tptr_'_update (\<lambda>_. thread_' s) sa) \<in> \<lbrace>\<forall>cl fl. cthread_state_relation_lifted Structures_H.thread_state.Restart (cl\<lparr>tsType_CL := \<acute>ts && mask 4\<rparr>, fl)\<rbrace> \<inter> \<lbrace>\<acute>tptr = \<^bsup>s\<^esup>thread\<rbrace>} \<inter> {s'. \<forall>t rv. dc rv (xfdc t) \<longrightarrow> s'\<lparr>globals := globals t\<rparr> \<in> {sa. tcb_'_update (\<lambda>_. thread_' s) sa \<in> UNIV \<inter> \<lbrace>\<acute>tcb = \<^bsup>s\<^esup>thread\<rbrace>} \<inter> {s'. \<forall>t rv. dc rv (xfdc t) \<longrightarrow> s'\<lparr>globals := globals t\<rparr> \<in> UNIV}} \<inter> ?R'132 (thread_' s) \<inter> \<lbrace>\<^bsup>s\<^esup>thread = tcb_ptr_to_ctcb_ptr thread\<rbrace>} proof (prove)
goal (8 subgoals):
 1. \<And>rv xfdca rva xfdcb \<sigma>. \<lbrakk>tcb_ptr_to_ctcb_ptr thread \<noteq> NULL; dc rv xfdca; dc rva xfdcb\<rbrakk> \<Longrightarrow> {s. tcb_at' thread \<sigma> \<and> s \<in> UNIV \<and> (\<sigma>, s) \<in> rf_sr} \<subseteq> {s. s \<Turnstile>\<^sub>c tcb_ptr_to_ctcb_ptr thread \<and> (\<exists>(rv, \<sigma>')\<in>fst (return rva \<sigma>). (\<sigma>', thread_'_update (\<lambda>_. h_val (hrs_mem (t_hrs_' (globals s))) (PTR(tcb_C ptr) &(tcb_ptr_to_ctcb_ptr thread\<rightarrow>[''tcbEPNext_C'']))) s) \<in> rf_sr \<and> dc rv (xfdc (thread_'_update (\<lambda>_. h_val (hrs_mem (t_hrs_' (globals s))) (PTR(tcb_C ptr) &(tcb_ptr_to_ctcb_ptr thread\<rightarrow>[''tcbEPNext_C'']))) s)))}
 2. \<And>rv xfdc. \<lbrakk>tcb_ptr_to_ctcb_ptr thread \<noteq> NULL; dc rv xfdc\<rbrakk> \<Longrightarrow> \<lbrace>?R181 rv\<rbrace> tcbSchedEnqueue thread \<lbrace>\<lambda>a. tcb_at' thread\<rbrace>
 3. tcb_ptr_to_ctcb_ptr thread \<noteq> NULL \<Longrightarrow> \<lbrace>?R137\<rbrace> setThreadState Structures_H.thread_state.Restart thread \<lbrace>\<lambda>a. Invariants_H.valid_queues and tcb_at' thread and valid_objs' and ?R181 a\<rbrace>
 4. \<And>rv' t t'. tcb_ptr_to_ctcb_ptr thread \<noteq> NULL \<Longrightarrow> ceqv \<Gamma> xfdc rv' t t' (While \<lbrace>\<acute>thread \<noteq> NULL\<rbrace> (CALL setThreadState_'proc(\<acute>thread,SCAST(32 signed \<rightarrow> 32) ThreadState_Restart);;
CALL tcbSchedEnqueue_'proc(\<acute>thread);;
Guard C_Guard {s. s \<Turnstile>\<^sub>c thread_' s} (\<acute>thread :== h_val (hrs_mem \<acute>t_hrs) (PTR(tcb_C ptr) &(\<acute>thread\<rightarrow>[''tcbEPNext_C'']))))) (?d'130 rv')
 5. \<And>rv rv'. \<lbrakk>tcb_ptr_to_ctcb_ptr thread \<noteq> NULL; dc rv rv'\<rbrakk> \<Longrightarrow> ccorres dc xfdc (?Q130 rv) (?Q'130 rv rv') hs (mapM_x (\<lambda>t. do y <- setThreadState Structures_H.thread_state.Restart t;
tcbSchedEnqueue t
od) threads) (?d'130 rv')
 6. tcb_ptr_to_ctcb_ptr thread \<noteq> NULL \<Longrightarrow> \<lbrace>?R130\<rbrace> do y <- setThreadState Structures_H.thread_state.Restart thread;
tcbSchedEnqueue thread
od \<lbrace>?Q130\<rbrace>
 7. tcb_ptr_to_ctcb_ptr thread \<noteq> NULL \<Longrightarrow> \<Gamma>\<turnstile>\<^bsub>/UNIV\<^esub> (?R'132 (tcb_ptr_to_ctcb_ptr thread)) CALL setThreadState_'proc(tcb_ptr_to_ctcb_ptr thread,SCAST(32 signed \<rightarrow> 32) ThreadState_Restart);;
CALL tcbSchedEnqueue_'proc(tcb_ptr_to_ctcb_ptr thread);;
Guard C_Guard {s. s \<Turnstile>\<^sub>c tcb_ptr_to_ctcb_ptr thread} (\<acute>thread :== h_val (hrs_mem \<acute>t_hrs) (PTR(tcb_C ptr) &(tcb_ptr_to_ctcb_ptr thread\<rightarrow>[''tcbEPNext_C'']))) {s. \<forall>rv. dc rv (xfdc s) \<longrightarrow> s \<in> ?Q'130 rv (xfdc s)}
 8. \<And>s s'. \<lbrakk>(s, s') \<in> rf_sr; valid_objs' s \<and> Invariants_H.valid_queues s \<and> tcb_at' thread s \<and> thread \<noteq> 0 \<and> (\<forall>t\<in>set threads. tcb_at' t s \<and> t \<noteq> 0) \<and> sch_act_wf (ksSchedulerAction s) s; s' \<in> {s'. thread_' s' = tcb_ptr_to_ctcb_ptr thread \<and> (\<exists>tcb. cslift s' (thread_' s') = Some tcb \<and> ep_queue_relation (cslift s') threads (thread_' s') (tcbEPNext_C tcb))}\<rbrakk> \<Longrightarrow> ((\<lambda>s. tcb_at' thread s \<and> Invariants_H.valid_queues s \<and> valid_objs' s \<and> valid_tcb_state' Structures_H.thread_state.Restart s \<and> (ksSchedulerAction s = SwitchToThread thread \<longrightarrow> runnable' Structures_H.thread_state.Restart) \<and> (\<forall>p. thread \<in> set (ksReadyQueues s p) \<longrightarrow> runnable' Structures_H.thread_state.Restart) \<and> sch_act_wf (ksSchedulerAction s) s) and ?R137 and ?R130 and (\<lambda>_. tcb_ptr_to_ctcb_ptr thread \<noteq> NULL)) s \<and> s' \<in> {s. s \<in> {sa. ts_'_update (\<lambda>_. SCAST(32 signed \<rightarrow> 32) ThreadState_Restart) (tptr_'_update (\<lambda>_. thread_' s) sa) \<in> \<lbrace>\<forall>cl fl. cthread_state_relation_lifted Structures_H.thread_state.Restart (cl\<lparr>tsType_CL := \<acute>ts && mask 4\<rparr>, fl)\<rbrace> \<inter> \<lbrace>\<acute>tptr = \<^bsup>s\<^esup>thread\<rbrace>} \<inter> {s'. \<forall>t rv. dc rv (xfdc t) \<longrightarrow> s'\<lparr>globals := globals t\<rparr> \<in> {sa. tcb_'_update (\<lambda>_. thread_' s) sa \<in> UNIV \<inter> \<lbrace>\<acute>tcb = \<^bsup>s\<^esup>thread\<rbrace>} \<inter> {s'. \<forall>t rv. dc rv (xfdc t) \<longrightarrow> s'\<lparr>globals := globals t\<rparr> \<in> UNIV}} \<inter> ?R'132 (thread_' s) \<inter> \<lbrace>\<^bsup>s\<^esup>thread = tcb_ptr_to_ctcb_ptr thread\<rbrace>} proof (prove)
goal (8 subgoals):
 1. \<And>\<sigma> x. \<lbrakk>tcb_ptr_to_ctcb_ptr thread \<noteq> NULL; tcb_at' thread \<sigma>; (\<sigma>, x) \<in> rf_sr\<rbrakk> \<Longrightarrow> x \<Turnstile>\<^sub>c tcb_ptr_to_ctcb_ptr thread
 2. \<And>rv xfdc. \<lbrakk>tcb_ptr_to_ctcb_ptr thread \<noteq> NULL; dc rv xfdc\<rbrakk> \<Longrightarrow> \<lbrace>?R181 rv\<rbrace> tcbSchedEnqueue thread \<lbrace>\<lambda>a. tcb_at' thread\<rbrace>
 3. tcb_ptr_to_ctcb_ptr thread \<noteq> NULL \<Longrightarrow> \<lbrace>?R137\<rbrace> setThreadState Structures_H.thread_state.Restart thread \<lbrace>\<lambda>a. Invariants_H.valid_queues and tcb_at' thread and valid_objs' and ?R181 a\<rbrace>
 4. \<And>rv' t t'. tcb_ptr_to_ctcb_ptr thread \<noteq> NULL \<Longrightarrow> ceqv \<Gamma> xfdc rv' t t' (While \<lbrace>\<acute>thread \<noteq> NULL\<rbrace> (CALL setThreadState_'proc(\<acute>thread,SCAST(32 signed \<rightarrow> 32) ThreadState_Restart);;
CALL tcbSchedEnqueue_'proc(\<acute>thread);;
Guard C_Guard {s. s \<Turnstile>\<^sub>c thread_' s} (\<acute>thread :== h_val (hrs_mem \<acute>t_hrs) (PTR(tcb_C ptr) &(\<acute>thread\<rightarrow>[''tcbEPNext_C'']))))) (?d'130 rv')
 5. \<And>rv rv'. \<lbrakk>tcb_ptr_to_ctcb_ptr thread \<noteq> NULL; dc rv rv'\<rbrakk> \<Longrightarrow> ccorres dc xfdc (?Q130 rv) (?Q'130 rv rv') hs (mapM_x (\<lambda>t. do y <- setThreadState Structures_H.thread_state.Restart t;
tcbSchedEnqueue t
od) threads) (?d'130 rv')
 6. tcb_ptr_to_ctcb_ptr thread \<noteq> NULL \<Longrightarrow> \<lbrace>?R130\<rbrace> do y <- setThreadState Structures_H.thread_state.Restart thread;
tcbSchedEnqueue thread
od \<lbrace>?Q130\<rbrace>
 7. tcb_ptr_to_ctcb_ptr thread \<noteq> NULL \<Longrightarrow> \<Gamma>\<turnstile>\<^bsub>/UNIV\<^esub> (?R'132 (tcb_ptr_to_ctcb_ptr thread)) CALL setThreadState_'proc(tcb_ptr_to_ctcb_ptr thread,SCAST(32 signed \<rightarrow> 32) ThreadState_Restart);;
CALL tcbSchedEnqueue_'proc(tcb_ptr_to_ctcb_ptr thread);;
Guard C_Guard {s. s \<Turnstile>\<^sub>c tcb_ptr_to_ctcb_ptr thread} (\<acute>thread :== h_val (hrs_mem \<acute>t_hrs) (PTR(tcb_C ptr) &(tcb_ptr_to_ctcb_ptr thread\<rightarrow>[''tcbEPNext_C'']))) {s. \<forall>rv. dc rv (xfdc s) \<longrightarrow> s \<in> ?Q'130 rv (xfdc s)}
 8. \<And>s s'. \<lbrakk>(s, s') \<in> rf_sr; valid_objs' s \<and> Invariants_H.valid_queues s \<and> tcb_at' thread s \<and> thread \<noteq> 0 \<and> (\<forall>t\<in>set threads. tcb_at' t s \<and> t \<noteq> 0) \<and> sch_act_wf (ksSchedulerAction s) s; s' \<in> {s'. thread_' s' = tcb_ptr_to_ctcb_ptr thread \<and> (\<exists>tcb. cslift s' (thread_' s') = Some tcb \<and> ep_queue_relation (cslift s') threads (thread_' s') (tcbEPNext_C tcb))}\<rbrakk> \<Longrightarrow> ((\<lambda>s. tcb_at' thread s \<and> Invariants_H.valid_queues s \<and> valid_objs' s \<and> valid_tcb_state' Structures_H.thread_state.Restart s \<and> (ksSchedulerAction s = SwitchToThread thread \<longrightarrow> runnable' Structures_H.thread_state.Restart) \<and> (\<forall>p. thread \<in> set (ksReadyQueues s p) \<longrightarrow> runnable' Structures_H.thread_state.Restart) \<and> sch_act_wf (ksSchedulerAction s) s) and ?R137 and ?R130 and (\<lambda>_. tcb_ptr_to_ctcb_ptr thread \<noteq> NULL)) s \<and> s' \<in> {s. s \<in> {sa. ts_'_update (\<lambda>_. SCAST(32 signed \<rightarrow> 32) ThreadState_Restart) (tptr_'_update (\<lambda>_. thread_' s) sa) \<in> \<lbrace>\<forall>cl fl. cthread_state_relation_lifted Structures_H.thread_state.Restart (cl\<lparr>tsType_CL := \<acute>ts && mask 4\<rparr>, fl)\<rbrace> \<inter> \<lbrace>\<acute>tptr = \<^bsup>s\<^esup>thread\<rbrace>} \<inter> {s'. \<forall>t rv. dc rv (xfdc t) \<longrightarrow> s'\<lparr>globals := globals t\<rparr> \<in> {sa. tcb_'_update (\<lambda>_. thread_' s) sa \<in> UNIV \<inter> \<lbrace>\<acute>tcb = \<^bsup>s\<^esup>thread\<rbrace>} \<inter> {s'. \<forall>t rv. dc rv (xfdc t) \<longrightarrow> s'\<lparr>globals := globals t\<rparr> \<in> UNIV}} \<inter> ?R'132 (thread_' s) \<inter> \<lbrace>\<^bsup>s\<^esup>thread = tcb_ptr_to_ctcb_ptr thread\<rbrace>} proof (prove)
goal (8 subgoals):
 1. \<And>\<sigma> x ko. \<lbrakk>tcb_ptr_to_ctcb_ptr thread \<noteq> NULL; (\<sigma>, x) \<in> rf_sr; ko_at' ko thread \<sigma>\<rbrakk> \<Longrightarrow> x \<Turnstile>\<^sub>c tcb_ptr_to_ctcb_ptr thread
 2. \<And>rv xfdc. \<lbrakk>tcb_ptr_to_ctcb_ptr thread \<noteq> NULL; dc rv xfdc\<rbrakk> \<Longrightarrow> \<lbrace>?R181 rv\<rbrace> tcbSchedEnqueue thread \<lbrace>\<lambda>a. tcb_at' thread\<rbrace>
 3. tcb_ptr_to_ctcb_ptr thread \<noteq> NULL \<Longrightarrow> \<lbrace>?R137\<rbrace> setThreadState Structures_H.thread_state.Restart thread \<lbrace>\<lambda>a. Invariants_H.valid_queues and tcb_at' thread and valid_objs' and ?R181 a\<rbrace>
 4. \<And>rv' t t'. tcb_ptr_to_ctcb_ptr thread \<noteq> NULL \<Longrightarrow> ceqv \<Gamma> xfdc rv' t t' (While \<lbrace>\<acute>thread \<noteq> NULL\<rbrace> (CALL setThreadState_'proc(\<acute>thread,SCAST(32 signed \<rightarrow> 32) ThreadState_Restart);;
CALL tcbSchedEnqueue_'proc(\<acute>thread);;
Guard C_Guard {s. s \<Turnstile>\<^sub>c thread_' s} (\<acute>thread :== h_val (hrs_mem \<acute>t_hrs) (PTR(tcb_C ptr) &(\<acute>thread\<rightarrow>[''tcbEPNext_C'']))))) (?d'130 rv')
 5. \<And>rv rv'. \<lbrakk>tcb_ptr_to_ctcb_ptr thread \<noteq> NULL; dc rv rv'\<rbrakk> \<Longrightarrow> ccorres dc xfdc (?Q130 rv) (?Q'130 rv rv') hs (mapM_x (\<lambda>t. do y <- setThreadState Structures_H.thread_state.Restart t;
tcbSchedEnqueue t
od) threads) (?d'130 rv')
 6. tcb_ptr_to_ctcb_ptr thread \<noteq> NULL \<Longrightarrow> \<lbrace>?R130\<rbrace> do y <- setThreadState Structures_H.thread_state.Restart thread;
tcbSchedEnqueue thread
od \<lbrace>?Q130\<rbrace>
 7. tcb_ptr_to_ctcb_ptr thread \<noteq> NULL \<Longrightarrow> \<Gamma>\<turnstile>\<^bsub>/UNIV\<^esub> (?R'132 (tcb_ptr_to_ctcb_ptr thread)) CALL setThreadState_'proc(tcb_ptr_to_ctcb_ptr thread,SCAST(32 signed \<rightarrow> 32) ThreadState_Restart);;
CALL tcbSchedEnqueue_'proc(tcb_ptr_to_ctcb_ptr thread);;
Guard C_Guard {s. s \<Turnstile>\<^sub>c tcb_ptr_to_ctcb_ptr thread} (\<acute>thread :== h_val (hrs_mem \<acute>t_hrs) (PTR(tcb_C ptr) &(tcb_ptr_to_ctcb_ptr thread\<rightarrow>[''tcbEPNext_C'']))) {s. \<forall>rv. dc rv (xfdc s) \<longrightarrow> s \<in> ?Q'130 rv (xfdc s)}
 8. \<And>s s'. \<lbrakk>(s, s') \<in> rf_sr; valid_objs' s \<and> Invariants_H.valid_queues s \<and> tcb_at' thread s \<and> thread \<noteq> 0 \<and> (\<forall>t\<in>set threads. tcb_at' t s \<and> t \<noteq> 0) \<and> sch_act_wf (ksSchedulerAction s) s; s' \<in> {s'. thread_' s' = tcb_ptr_to_ctcb_ptr thread \<and> (\<exists>tcb. cslift s' (thread_' s') = Some tcb \<and> ep_queue_relation (cslift s') threads (thread_' s') (tcbEPNext_C tcb))}\<rbrakk> \<Longrightarrow> ((\<lambda>s. tcb_at' thread s \<and> Invariants_H.valid_queues s \<and> valid_objs' s \<and> valid_tcb_state' Structures_H.thread_state.Restart s \<and> (ksSchedulerAction s = SwitchToThread thread \<longrightarrow> runnable' Structures_H.thread_state.Restart) \<and> (\<forall>p. thread \<in> set (ksReadyQueues s p) \<longrightarrow> runnable' Structures_H.thread_state.Restart) \<and> sch_act_wf (ksSchedulerAction s) s) and ?R137 and ?R130 and (\<lambda>_. tcb_ptr_to_ctcb_ptr thread \<noteq> NULL)) s \<and> s' \<in> {s. s \<in> {sa. ts_'_update (\<lambda>_. SCAST(32 signed \<rightarrow> 32) ThreadState_Restart) (tptr_'_update (\<lambda>_. thread_' s) sa) \<in> \<lbrace>\<forall>cl fl. cthread_state_relation_lifted Structures_H.thread_state.Restart (cl\<lparr>tsType_CL := \<acute>ts && mask 4\<rparr>, fl)\<rbrace> \<inter> \<lbrace>\<acute>tptr = \<^bsup>s\<^esup>thread\<rbrace>} \<inter> {s'. \<forall>t rv. dc rv (xfdc t) \<longrightarrow> s'\<lparr>globals := globals t\<rparr> \<in> {sa. tcb_'_update (\<lambda>_. thread_' s) sa \<in> UNIV \<inter> \<lbrace>\<acute>tcb = \<^bsup>s\<^esup>thread\<rbrace>} \<inter> {s'. \<forall>t rv. dc rv (xfdc t) \<longrightarrow> s'\<lparr>globals := globals t\<rparr> \<in> UNIV}} \<inter> ?R'132 (thread_' s) \<inter> \<lbrace>\<^bsup>s\<^esup>thread = tcb_ptr_to_ctcb_ptr thread\<rbrace>} proof (prove)
goal (9 subgoals):
 1. \<And>\<sigma> x ko. \<lbrakk>tcb_ptr_to_ctcb_ptr thread \<noteq> NULL; ko_at' ko thread \<sigma>\<rbrakk> \<Longrightarrow> map_to_tcbs (ksPSpace \<sigma>) (?x237 \<sigma> x ko) = Some (?y237 \<sigma> x ko)
 2. \<And>\<sigma> x ko y'. \<lbrakk>tcb_ptr_to_ctcb_ptr thread \<noteq> NULL; ko_at' ko thread \<sigma>; map_to_tcbs (ksPSpace \<sigma>) (?x237 \<sigma> x ko) = Some (?y237 \<sigma> x ko); ctcb_relation (?y237 \<sigma> x ko) y'; cslift x (tcb_ptr_to_ctcb_ptr (?x237 \<sigma> x ko)) = Some y'\<rbrakk> \<Longrightarrow> x \<Turnstile>\<^sub>c tcb_ptr_to_ctcb_ptr thread
 3. \<And>rv xfdc. \<lbrakk>tcb_ptr_to_ctcb_ptr thread \<noteq> NULL; dc rv xfdc\<rbrakk> \<Longrightarrow> \<lbrace>?R181 rv\<rbrace> tcbSchedEnqueue thread \<lbrace>\<lambda>a. tcb_at' thread\<rbrace>
 4. tcb_ptr_to_ctcb_ptr thread \<noteq> NULL \<Longrightarrow> \<lbrace>?R137\<rbrace> setThreadState Structures_H.thread_state.Restart thread \<lbrace>\<lambda>a. Invariants_H.valid_queues and tcb_at' thread and valid_objs' and ?R181 a\<rbrace>
 5. \<And>rv' t t'. tcb_ptr_to_ctcb_ptr thread \<noteq> NULL \<Longrightarrow> ceqv \<Gamma> xfdc rv' t t' (While \<lbrace>\<acute>thread \<noteq> NULL\<rbrace> (CALL setThreadState_'proc(\<acute>thread,SCAST(32 signed \<rightarrow> 32) ThreadState_Restart);;
CALL tcbSchedEnqueue_'proc(\<acute>thread);;
Guard C_Guard {s. s \<Turnstile>\<^sub>c thread_' s} (\<acute>thread :== h_val (hrs_mem \<acute>t_hrs) (PTR(tcb_C ptr) &(\<acute>thread\<rightarrow>[''tcbEPNext_C'']))))) (?d'130 rv')
 6. \<And>rv rv'. \<lbrakk>tcb_ptr_to_ctcb_ptr thread \<noteq> NULL; dc rv rv'\<rbrakk> \<Longrightarrow> ccorres dc xfdc (?Q130 rv) (?Q'130 rv rv') hs (mapM_x (\<lambda>t. do y <- setThreadState Structures_H.thread_state.Restart t;
tcbSchedEnqueue t
od) threads) (?d'130 rv')
 7. tcb_ptr_to_ctcb_ptr thread \<noteq> NULL \<Longrightarrow> \<lbrace>?R130\<rbrace> do y <- setThreadState Structures_H.thread_state.Restart thread;
tcbSchedEnqueue thread
od \<lbrace>?Q130\<rbrace>
 8. tcb_ptr_to_ctcb_ptr thread \<noteq> NULL \<Longrightarrow> \<Gamma>\<turnstile>\<^bsub>/UNIV\<^esub> (?R'132 (tcb_ptr_to_ctcb_ptr thread)) CALL setThreadState_'proc(tcb_ptr_to_ctcb_ptr thread,SCAST(32 signed \<rightarrow> 32) ThreadState_Restart);;
CALL tcbSchedEnqueue_'proc(tcb_ptr_to_ctcb_ptr thread);;
Guard C_Guard {s. s \<Turnstile>\<^sub>c tcb_ptr_to_ctcb_ptr thread} (\<acute>thread :== h_val (hrs_mem \<acute>t_hrs) (PTR(tcb_C ptr) &(tcb_ptr_to_ctcb_ptr thread\<rightarrow>[''tcbEPNext_C'']))) {s. \<forall>rv. dc rv (xfdc s) \<longrightarrow> s \<in> ?Q'130 rv (xfdc s)}
 9. \<And>s s'. \<lbrakk>(s, s') \<in> rf_sr; valid_objs' s \<and> Invariants_H.valid_queues s \<and> tcb_at' thread s \<and> thread \<noteq> 0 \<and> (\<forall>t\<in>set threads. tcb_at' t s \<and> t \<noteq> 0) \<and> sch_act_wf (ksSchedulerAction s) s; s' \<in> {s'. thread_' s' = tcb_ptr_to_ctcb_ptr thread \<and> (\<exists>tcb. cslift s' (thread_' s') = Some tcb \<and> ep_queue_relation (cslift s') threads (thread_' s') (tcbEPNext_C tcb))}\<rbrakk> \<Longrightarrow> ((\<lambda>s. tcb_at' thread s \<and> Invariants_H.valid_queues s \<and> valid_objs' s \<and> valid_tcb_state' Structures_H.thread_state.Restart s \<and> (ksSchedulerAction s = SwitchToThread thread \<longrightarrow> runnable' Structures_H.thread_state.Restart) \<and> (\<forall>p. thread \<in> set (ksReadyQueues s p) \<longrightarrow> runnable' Structures_H.thread_state.Restart) \<and> sch_act_wf (ksSchedulerAction s) s) and ?R137 and ?R130 and (\<lambda>_. tcb_ptr_to_ctcb_ptr thread \<noteq> NULL)) s \<and> s' \<in> {s. s \<in> {sa. ts_'_update (\<lambda>_. SCAST(32 signed \<rightarrow> 32) ThreadState_Restart) (tptr_'_update (\<lambda>_. thread_' s) sa) \<in> \<lbrace>\<forall>cl fl. cthread_state_relation_lifted Structures_H.thread_state.Restart (cl\<lparr>tsType_CL := \<acute>ts && mask 4\<rparr>, fl)\<rbrace> \<inter> \<lbrace>\<acute>tptr = \<^bsup>s\<^esup>thread\<rbrace>} \<inter> {s'. \<forall>t rv. dc rv (xfdc t) \<longrightarrow> s'\<lparr>globals := globals t\<rparr> \<in> {sa. tcb_'_update (\<lambda>_. thread_' s) sa \<in> UNIV \<inter> \<lbrace>\<acute>tcb = \<^bsup>s\<^esup>thread\<rbrace>} \<inter> {s'. \<forall>t rv. dc rv (xfdc t) \<longrightarrow> s'\<lparr>globals := globals t\<rparr> \<in> UNIV}} \<inter> ?R'132 (thread_' s) \<inter> \<lbrace>\<^bsup>s\<^esup>thread = tcb_ptr_to_ctcb_ptr thread\<rbrace>} proof (prove)
goal (8 subgoals):
 1. \<And>\<sigma> x ko y'. \<lbrakk>tcb_ptr_to_ctcb_ptr thread \<noteq> NULL; ko_at' ko thread \<sigma>; map_to_tcbs (ksPSpace \<sigma>) thread = Some ko; ctcb_relation ko y'; cslift x (tcb_ptr_to_ctcb_ptr thread) = Some y'\<rbrakk> \<Longrightarrow> x \<Turnstile>\<^sub>c tcb_ptr_to_ctcb_ptr thread
 2. \<And>rv xfdc. \<lbrakk>tcb_ptr_to_ctcb_ptr thread \<noteq> NULL; dc rv xfdc\<rbrakk> \<Longrightarrow> \<lbrace>?R181 rv\<rbrace> tcbSchedEnqueue thread \<lbrace>\<lambda>a. tcb_at' thread\<rbrace>
 3. tcb_ptr_to_ctcb_ptr thread \<noteq> NULL \<Longrightarrow> \<lbrace>?R137\<rbrace> setThreadState Structures_H.thread_state.Restart thread \<lbrace>\<lambda>a. Invariants_H.valid_queues and tcb_at' thread and valid_objs' and ?R181 a\<rbrace>
 4. \<And>rv' t t'. tcb_ptr_to_ctcb_ptr thread \<noteq> NULL \<Longrightarrow> ceqv \<Gamma> xfdc rv' t t' (While \<lbrace>\<acute>thread \<noteq> NULL\<rbrace> (CALL setThreadState_'proc(\<acute>thread,SCAST(32 signed \<rightarrow> 32) ThreadState_Restart);;
CALL tcbSchedEnqueue_'proc(\<acute>thread);;
Guard C_Guard {s. s \<Turnstile>\<^sub>c thread_' s} (\<acute>thread :== h_val (hrs_mem \<acute>t_hrs) (PTR(tcb_C ptr) &(\<acute>thread\<rightarrow>[''tcbEPNext_C'']))))) (?d'130 rv')
 5. \<And>rv rv'. \<lbrakk>tcb_ptr_to_ctcb_ptr thread \<noteq> NULL; dc rv rv'\<rbrakk> \<Longrightarrow> ccorres dc xfdc (?Q130 rv) (?Q'130 rv rv') hs (mapM_x (\<lambda>t. do y <- setThreadState Structures_H.thread_state.Restart t;
tcbSchedEnqueue t
od) threads) (?d'130 rv')
 6. tcb_ptr_to_ctcb_ptr thread \<noteq> NULL \<Longrightarrow> \<lbrace>?R130\<rbrace> do y <- setThreadState Structures_H.thread_state.Restart thread;
tcbSchedEnqueue thread
od \<lbrace>?Q130\<rbrace>
 7. tcb_ptr_to_ctcb_ptr thread \<noteq> NULL \<Longrightarrow> \<Gamma>\<turnstile>\<^bsub>/UNIV\<^esub> (?R'132 (tcb_ptr_to_ctcb_ptr thread)) CALL setThreadState_'proc(tcb_ptr_to_ctcb_ptr thread,SCAST(32 signed \<rightarrow> 32) ThreadState_Restart);;
CALL tcbSchedEnqueue_'proc(tcb_ptr_to_ctcb_ptr thread);;
Guard C_Guard {s. s \<Turnstile>\<^sub>c tcb_ptr_to_ctcb_ptr thread} (\<acute>thread :== h_val (hrs_mem \<acute>t_hrs) (PTR(tcb_C ptr) &(tcb_ptr_to_ctcb_ptr thread\<rightarrow>[''tcbEPNext_C'']))) {s. \<forall>rv. dc rv (xfdc s) \<longrightarrow> s \<in> ?Q'130 rv (xfdc s)}
 8. \<And>s s'. \<lbrakk>(s, s') \<in> rf_sr; valid_objs' s \<and> Invariants_H.valid_queues s \<and> tcb_at' thread s \<and> thread \<noteq> 0 \<and> (\<forall>t\<in>set threads. tcb_at' t s \<and> t \<noteq> 0) \<and> sch_act_wf (ksSchedulerAction s) s; s' \<in> {s'. thread_' s' = tcb_ptr_to_ctcb_ptr thread \<and> (\<exists>tcb. cslift s' (thread_' s') = Some tcb \<and> ep_queue_relation (cslift s') threads (thread_' s') (tcbEPNext_C tcb))}\<rbrakk> \<Longrightarrow> ((\<lambda>s. tcb_at' thread s \<and> Invariants_H.valid_queues s \<and> valid_objs' s \<and> valid_tcb_state' Structures_H.thread_state.Restart s \<and> (ksSchedulerAction s = SwitchToThread thread \<longrightarrow> runnable' Structures_H.thread_state.Restart) \<and> (\<forall>p. thread \<in> set (ksReadyQueues s p) \<longrightarrow> runnable' Structures_H.thread_state.Restart) \<and> sch_act_wf (ksSchedulerAction s) s) and ?R137 and ?R130 and (\<lambda>_. tcb_ptr_to_ctcb_ptr thread \<noteq> NULL)) s \<and> s' \<in> {s. s \<in> {sa. ts_'_update (\<lambda>_. SCAST(32 signed \<rightarrow> 32) ThreadState_Restart) (tptr_'_update (\<lambda>_. thread_' s) sa) \<in> \<lbrace>\<forall>cl fl. cthread_state_relation_lifted Structures_H.thread_state.Restart (cl\<lparr>tsType_CL := \<acute>ts && mask 4\<rparr>, fl)\<rbrace> \<inter> \<lbrace>\<acute>tptr = \<^bsup>s\<^esup>thread\<rbrace>} \<inter> {s'. \<forall>t rv. dc rv (xfdc t) \<longrightarrow> s'\<lparr>globals := globals t\<rparr> \<in> {sa. tcb_'_update (\<lambda>_. thread_' s) sa \<in> UNIV \<inter> \<lbrace>\<acute>tcb = \<^bsup>s\<^esup>thread\<rbrace>} \<inter> {s'. \<forall>t rv. dc rv (xfdc t) \<longrightarrow> s'\<lparr>globals := globals t\<rparr> \<in> UNIV}} \<inter> ?R'132 (thread_' s) \<inter> \<lbrace>\<^bsup>s\<^esup>thread = tcb_ptr_to_ctcb_ptr thread\<rbrace>} proof (prove)
goal (7 subgoals):
 1. \<And>rv xfdc. \<lbrakk>tcb_ptr_to_ctcb_ptr thread \<noteq> NULL; dc rv xfdc\<rbrakk> \<Longrightarrow> \<lbrace>?R181 rv\<rbrace> tcbSchedEnqueue thread \<lbrace>\<lambda>a. tcb_at' thread\<rbrace>
 2. tcb_ptr_to_ctcb_ptr thread \<noteq> NULL \<Longrightarrow> \<lbrace>?R137\<rbrace> setThreadState Structures_H.thread_state.Restart thread \<lbrace>\<lambda>a. Invariants_H.valid_queues and tcb_at' thread and valid_objs' and ?R181 a\<rbrace>
 3. \<And>rv' t t'. tcb_ptr_to_ctcb_ptr thread \<noteq> NULL \<Longrightarrow> ceqv \<Gamma> xfdc rv' t t' (While \<lbrace>\<acute>thread \<noteq> NULL\<rbrace> (CALL setThreadState_'proc(\<acute>thread,SCAST(32 signed \<rightarrow> 32) ThreadState_Restart);;
CALL tcbSchedEnqueue_'proc(\<acute>thread);;
Guard C_Guard {s. s \<Turnstile>\<^sub>c thread_' s} (\<acute>thread :== h_val (hrs_mem \<acute>t_hrs) (PTR(tcb_C ptr) &(\<acute>thread\<rightarrow>[''tcbEPNext_C'']))))) (?d'130 rv')
 4. \<And>rv rv'. \<lbrakk>tcb_ptr_to_ctcb_ptr thread \<noteq> NULL; dc rv rv'\<rbrakk> \<Longrightarrow> ccorres dc xfdc (?Q130 rv) (?Q'130 rv rv') hs (mapM_x (\<lambda>t. do y <- setThreadState Structures_H.thread_state.Restart t;
tcbSchedEnqueue t
od) threads) (?d'130 rv')
 5. tcb_ptr_to_ctcb_ptr thread \<noteq> NULL \<Longrightarrow> \<lbrace>?R130\<rbrace> do y <- setThreadState Structures_H.thread_state.Restart thread;
tcbSchedEnqueue thread
od \<lbrace>?Q130\<rbrace>
 6. tcb_ptr_to_ctcb_ptr thread \<noteq> NULL \<Longrightarrow> \<Gamma>\<turnstile>\<^bsub>/UNIV\<^esub> (?R'132 (tcb_ptr_to_ctcb_ptr thread)) CALL setThreadState_'proc(tcb_ptr_to_ctcb_ptr thread,SCAST(32 signed \<rightarrow> 32) ThreadState_Restart);;
CALL tcbSchedEnqueue_'proc(tcb_ptr_to_ctcb_ptr thread);;
Guard C_Guard {s. s \<Turnstile>\<^sub>c tcb_ptr_to_ctcb_ptr thread} (\<acute>thread :== h_val (hrs_mem \<acute>t_hrs) (PTR(tcb_C ptr) &(tcb_ptr_to_ctcb_ptr thread\<rightarrow>[''tcbEPNext_C'']))) {s. \<forall>rv. dc rv (xfdc s) \<longrightarrow> s \<in> ?Q'130 rv (xfdc s)}
 7. \<And>s s'. \<lbrakk>(s, s') \<in> rf_sr; valid_objs' s \<and> Invariants_H.valid_queues s \<and> tcb_at' thread s \<and> thread \<noteq> 0 \<and> (\<forall>t\<in>set threads. tcb_at' t s \<and> t \<noteq> 0) \<and> sch_act_wf (ksSchedulerAction s) s; s' \<in> {s'. thread_' s' = tcb_ptr_to_ctcb_ptr thread \<and> (\<exists>tcb. cslift s' (thread_' s') = Some tcb \<and> ep_queue_relation (cslift s') threads (thread_' s') (tcbEPNext_C tcb))}\<rbrakk> \<Longrightarrow> ((\<lambda>s. tcb_at' thread s \<and> Invariants_H.valid_queues s \<and> valid_objs' s \<and> valid_tcb_state' Structures_H.thread_state.Restart s \<and> (ksSchedulerAction s = SwitchToThread thread \<longrightarrow> runnable' Structures_H.thread_state.Restart) \<and> (\<forall>p. thread \<in> set (ksReadyQueues s p) \<longrightarrow> runnable' Structures_H.thread_state.Restart) \<and> sch_act_wf (ksSchedulerAction s) s) and ?R137 and ?R130 and (\<lambda>_. tcb_ptr_to_ctcb_ptr thread \<noteq> NULL)) s \<and> s' \<in> {s. s \<in> {sa. ts_'_update (\<lambda>_. SCAST(32 signed \<rightarrow> 32) ThreadState_Restart) (tptr_'_update (\<lambda>_. thread_' s) sa) \<in> \<lbrace>\<forall>cl fl. cthread_state_relation_lifted Structures_H.thread_state.Restart (cl\<lparr>tsType_CL := \<acute>ts && mask 4\<rparr>, fl)\<rbrace> \<inter> \<lbrace>\<acute>tptr = \<^bsup>s\<^esup>thread\<rbrace>} \<inter> {s'. \<forall>t rv. dc rv (xfdc t) \<longrightarrow> s'\<lparr>globals := globals t\<rparr> \<in> {sa. tcb_'_update (\<lambda>_. thread_' s) sa \<in> UNIV \<inter> \<lbrace>\<acute>tcb = \<^bsup>s\<^esup>thread\<rbrace>} \<inter> {s'. \<forall>t rv. dc rv (xfdc t) \<longrightarrow> s'\<lparr>globals := globals t\<rparr> \<in> UNIV}} \<inter> ?R'132 (thread_' s) \<inter> \<lbrace>\<^bsup>s\<^esup>thread = tcb_ptr_to_ctcb_ptr thread\<rbrace>} proof (prove)
goal (5 subgoals):
 1. \<And>rv' t t'. tcb_ptr_to_ctcb_ptr thread \<noteq> NULL \<Longrightarrow> ceqv \<Gamma> xfdc rv' t t' (While \<lbrace>\<acute>thread \<noteq> NULL\<rbrace> (CALL setThreadState_'proc(\<acute>thread,SCAST(32 signed \<rightarrow> 32) ThreadState_Restart);;
CALL tcbSchedEnqueue_'proc(\<acute>thread);;
Guard C_Guard {s. s \<Turnstile>\<^sub>c thread_' s} (\<acute>thread :== h_val (hrs_mem \<acute>t_hrs) (PTR(tcb_C ptr) &(\<acute>thread\<rightarrow>[''tcbEPNext_C'']))))) (?d'130 rv')
 2. \<And>rv rv'. \<lbrakk>tcb_ptr_to_ctcb_ptr thread \<noteq> NULL; dc rv rv'\<rbrakk> \<Longrightarrow> ccorres dc xfdc (?Q130 rv) (?Q'130 rv rv') hs (mapM_x (\<lambda>t. do y <- setThreadState Structures_H.thread_state.Restart t;
tcbSchedEnqueue t
od) threads) (?d'130 rv')
 3. tcb_ptr_to_ctcb_ptr thread \<noteq> NULL \<Longrightarrow> \<lbrace>?R130\<rbrace> do y <- setThreadState Structures_H.thread_state.Restart thread;
tcbSchedEnqueue thread
od \<lbrace>?Q130\<rbrace>
 4. tcb_ptr_to_ctcb_ptr thread \<noteq> NULL \<Longrightarrow> \<Gamma>\<turnstile>\<^bsub>/UNIV\<^esub> (?R'132 (tcb_ptr_to_ctcb_ptr thread)) CALL setThreadState_'proc(tcb_ptr_to_ctcb_ptr thread,SCAST(32 signed \<rightarrow> 32) ThreadState_Restart);;
CALL tcbSchedEnqueue_'proc(tcb_ptr_to_ctcb_ptr thread);;
Guard C_Guard {s. s \<Turnstile>\<^sub>c tcb_ptr_to_ctcb_ptr thread} (\<acute>thread :== h_val (hrs_mem \<acute>t_hrs) (PTR(tcb_C ptr) &(tcb_ptr_to_ctcb_ptr thread\<rightarrow>[''tcbEPNext_C'']))) {s. \<forall>rv. dc rv (xfdc s) \<longrightarrow> s \<in> ?Q'130 rv (xfdc s)}
 5. \<And>s s'. \<lbrakk>(s, s') \<in> rf_sr; valid_objs' s \<and> Invariants_H.valid_queues s \<and> tcb_at' thread s \<and> thread \<noteq> 0 \<and> (\<forall>t\<in>set threads. tcb_at' t s \<and> t \<noteq> 0) \<and> sch_act_wf (ksSchedulerAction s) s; s' \<in> {s'. thread_' s' = tcb_ptr_to_ctcb_ptr thread \<and> (\<exists>tcb. cslift s' (thread_' s') = Some tcb \<and> ep_queue_relation (cslift s') threads (thread_' s') (tcbEPNext_C tcb))}\<rbrakk> \<Longrightarrow> ((\<lambda>s. tcb_at' thread s \<and> Invariants_H.valid_queues s \<and> valid_objs' s \<and> valid_tcb_state' Structures_H.thread_state.Restart s \<and> (ksSchedulerAction s = SwitchToThread thread \<longrightarrow> runnable' Structures_H.thread_state.Restart) \<and> (\<forall>p. thread \<in> set (ksReadyQueues s p) \<longrightarrow> runnable' Structures_H.thread_state.Restart) \<and> sch_act_wf (ksSchedulerAction s) s) and (\<lambda>s. Invariants_H.valid_queues s \<and> tcb_at' thread s \<and> (valid_tcb_state' Structures_H.thread_state.Restart and valid_objs') s \<and> tcb_at' thread s) and ?R130 and (\<lambda>_. tcb_ptr_to_ctcb_ptr thread \<noteq> NULL)) s \<and> s' \<in> {s. s \<in> {sa. ts_'_update (\<lambda>_. SCAST(32 signed \<rightarrow> 32) ThreadState_Restart) (tptr_'_update (\<lambda>_. thread_' s) sa) \<in> \<lbrace>\<forall>cl fl. cthread_state_relation_lifted Structures_H.thread_state.Restart (cl\<lparr>tsType_CL := \<acute>ts && mask 4\<rparr>, fl)\<rbrace> \<inter> \<lbrace>\<acute>tptr = \<^bsup>s\<^esup>thread\<rbrace>} \<inter> {s'. \<forall>t rv. dc rv (xfdc t) \<longrightarrow> s'\<lparr>globals := globals t\<rparr> \<in> {sa. tcb_'_update (\<lambda>_. thread_' s) sa \<in> UNIV \<inter> \<lbrace>\<acute>tcb = \<^bsup>s\<^esup>thread\<rbrace>} \<inter> {s'. \<forall>t rv. dc rv (xfdc t) \<longrightarrow> s'\<lparr>globals := globals t\<rparr> \<in> UNIV}} \<inter> ?R'132 (thread_' s) \<inter> \<lbrace>\<^bsup>s\<^esup>thread = tcb_ptr_to_ctcb_ptr thread\<rbrace>} proof (prove)
goal (4 subgoals):
 1. \<And>rv rv'. \<lbrakk>tcb_ptr_to_ctcb_ptr thread \<noteq> NULL; dc rv rv'\<rbrakk> \<Longrightarrow> ccorres dc xfdc (?Q130 rv) (?Q'130 rv rv') hs (mapM_x (\<lambda>t. do y <- setThreadState Structures_H.thread_state.Restart t;
tcbSchedEnqueue t
od) threads) (While \<lbrace>\<acute>thread \<noteq> NULL\<rbrace> (CALL setThreadState_'proc(\<acute>thread,SCAST(32 signed \<rightarrow> 32) ThreadState_Restart);;
CALL tcbSchedEnqueue_'proc(\<acute>thread);;
Guard C_Guard {s. s \<Turnstile>\<^sub>c thread_' s} (\<acute>thread :== h_val (hrs_mem \<acute>t_hrs) (PTR(tcb_C ptr) &(\<acute>thread\<rightarrow>[''tcbEPNext_C''])))))
 2. tcb_ptr_to_ctcb_ptr thread \<noteq> NULL \<Longrightarrow> \<lbrace>?R130\<rbrace> do y <- setThreadState Structures_H.thread_state.Restart thread;
tcbSchedEnqueue thread
od \<lbrace>?Q130\<rbrace>
 3. tcb_ptr_to_ctcb_ptr thread \<noteq> NULL \<Longrightarrow> \<Gamma>\<turnstile>\<^bsub>/UNIV\<^esub> (?R'132 (tcb_ptr_to_ctcb_ptr thread)) CALL setThreadState_'proc(tcb_ptr_to_ctcb_ptr thread,SCAST(32 signed \<rightarrow> 32) ThreadState_Restart);;
CALL tcbSchedEnqueue_'proc(tcb_ptr_to_ctcb_ptr thread);;
Guard C_Guard {s. s \<Turnstile>\<^sub>c tcb_ptr_to_ctcb_ptr thread} (\<acute>thread :== h_val (hrs_mem \<acute>t_hrs) (PTR(tcb_C ptr) &(tcb_ptr_to_ctcb_ptr thread\<rightarrow>[''tcbEPNext_C'']))) {s. \<forall>rv. dc rv (xfdc s) \<longrightarrow> s \<in> ?Q'130 rv (xfdc s)}
 4. \<And>s s'. \<lbrakk>(s, s') \<in> rf_sr; valid_objs' s \<and> Invariants_H.valid_queues s \<and> tcb_at' thread s \<and> thread \<noteq> 0 \<and> (\<forall>t\<in>set threads. tcb_at' t s \<and> t \<noteq> 0) \<and> sch_act_wf (ksSchedulerAction s) s; s' \<in> {s'. thread_' s' = tcb_ptr_to_ctcb_ptr thread \<and> (\<exists>tcb. cslift s' (thread_' s') = Some tcb \<and> ep_queue_relation (cslift s') threads (thread_' s') (tcbEPNext_C tcb))}\<rbrakk> \<Longrightarrow> ((\<lambda>s. tcb_at' thread s \<and> Invariants_H.valid_queues s \<and> valid_objs' s \<and> valid_tcb_state' Structures_H.thread_state.Restart s \<and> (ksSchedulerAction s = SwitchToThread thread \<longrightarrow> runnable' Structures_H.thread_state.Restart) \<and> (\<forall>p. thread \<in> set (ksReadyQueues s p) \<longrightarrow> runnable' Structures_H.thread_state.Restart) \<and> sch_act_wf (ksSchedulerAction s) s) and (\<lambda>s. Invariants_H.valid_queues s \<and> tcb_at' thread s \<and> (valid_tcb_state' Structures_H.thread_state.Restart and valid_objs') s \<and> tcb_at' thread s) and ?R130 and (\<lambda>_. tcb_ptr_to_ctcb_ptr thread \<noteq> NULL)) s \<and> s' \<in> {s. s \<in> {sa. ts_'_update (\<lambda>_. SCAST(32 signed \<rightarrow> 32) ThreadState_Restart) (tptr_'_update (\<lambda>_. thread_' s) sa) \<in> \<lbrace>\<forall>cl fl. cthread_state_relation_lifted Structures_H.thread_state.Restart (cl\<lparr>tsType_CL := \<acute>ts && mask 4\<rparr>, fl)\<rbrace> \<inter> \<lbrace>\<acute>tptr = \<^bsup>s\<^esup>thread\<rbrace>} \<inter> {s'. \<forall>t rv. dc rv (xfdc t) \<longrightarrow> s'\<lparr>globals := globals t\<rparr> \<in> {sa. tcb_'_update (\<lambda>_. thread_' s) sa \<in> UNIV \<inter> \<lbrace>\<acute>tcb = \<^bsup>s\<^esup>thread\<rbrace>} \<inter> {s'. \<forall>t rv. dc rv (xfdc t) \<longrightarrow> s'\<lparr>globals := globals t\<rparr> \<in> UNIV}} \<inter> ?R'132 (thread_' s) \<inter> \<lbrace>\<^bsup>s\<^esup>thread = tcb_ptr_to_ctcb_ptr thread\<rbrace>} proof (prove)
goal (3 subgoals):
 1. tcb_ptr_to_ctcb_ptr thread \<noteq> NULL \<Longrightarrow> \<lbrace>?R130\<rbrace> do y <- setThreadState Structures_H.thread_state.Restart thread;
tcbSchedEnqueue thread
od \<lbrace>\<lambda>rv s. valid_objs' s \<and> Invariants_H.valid_queues s \<and> (\<forall>t\<in>set threads. tcb_at' t s \<and> t \<noteq> 0) \<and> sch_act_wf (ksSchedulerAction s) s\<rbrace>
 2. tcb_ptr_to_ctcb_ptr thread \<noteq> NULL \<Longrightarrow> \<Gamma>\<turnstile>\<^bsub>/UNIV\<^esub> (?R'132 (tcb_ptr_to_ctcb_ptr thread)) CALL setThreadState_'proc(tcb_ptr_to_ctcb_ptr thread,SCAST(32 signed \<rightarrow> 32) ThreadState_Restart);;
CALL tcbSchedEnqueue_'proc(tcb_ptr_to_ctcb_ptr thread);;
Guard C_Guard {s. s \<Turnstile>\<^sub>c tcb_ptr_to_ctcb_ptr thread} (\<acute>thread :== h_val (hrs_mem \<acute>t_hrs) (PTR(tcb_C ptr) &(tcb_ptr_to_ctcb_ptr thread\<rightarrow>[''tcbEPNext_C'']))) {s. \<forall>rv. dc rv (xfdc s) \<longrightarrow> s \<in> {s'. \<exists>p. ep_queue_relation (cslift s') threads p (thread_' s')}}
 3. \<And>s s'. \<lbrakk>(s, s') \<in> rf_sr; valid_objs' s \<and> Invariants_H.valid_queues s \<and> tcb_at' thread s \<and> thread \<noteq> 0 \<and> (\<forall>t\<in>set threads. tcb_at' t s \<and> t \<noteq> 0) \<and> sch_act_wf (ksSchedulerAction s) s; s' \<in> {s'. thread_' s' = tcb_ptr_to_ctcb_ptr thread \<and> (\<exists>tcb. cslift s' (thread_' s') = Some tcb \<and> ep_queue_relation (cslift s') threads (thread_' s') (tcbEPNext_C tcb))}\<rbrakk> \<Longrightarrow> ((\<lambda>s. tcb_at' thread s \<and> Invariants_H.valid_queues s \<and> valid_objs' s \<and> valid_tcb_state' Structures_H.thread_state.Restart s \<and> (ksSchedulerAction s = SwitchToThread thread \<longrightarrow> runnable' Structures_H.thread_state.Restart) \<and> (\<forall>p. thread \<in> set (ksReadyQueues s p) \<longrightarrow> runnable' Structures_H.thread_state.Restart) \<and> sch_act_wf (ksSchedulerAction s) s) and (\<lambda>s. Invariants_H.valid_queues s \<and> tcb_at' thread s \<and> (valid_tcb_state' Structures_H.thread_state.Restart and valid_objs') s \<and> tcb_at' thread s) and ?R130 and (\<lambda>_. tcb_ptr_to_ctcb_ptr thread \<noteq> NULL)) s \<and> s' \<in> {s. s \<in> {sa. ts_'_update (\<lambda>_. SCAST(32 signed \<rightarrow> 32) ThreadState_Restart) (tptr_'_update (\<lambda>_. thread_' s) sa) \<in> \<lbrace>\<forall>cl fl. cthread_state_relation_lifted Structures_H.thread_state.Restart (cl\<lparr>tsType_CL := \<acute>ts && mask 4\<rparr>, fl)\<rbrace> \<inter> \<lbrace>\<acute>tptr = \<^bsup>s\<^esup>thread\<rbrace>} \<inter> {s'. \<forall>t rv. dc rv (xfdc t) \<longrightarrow> s'\<lparr>globals := globals t\<rparr> \<in> {sa. tcb_'_update (\<lambda>_. thread_' s) sa \<in> UNIV \<inter> \<lbrace>\<acute>tcb = \<^bsup>s\<^esup>thread\<rbrace>} \<inter> {s'. \<forall>t rv. dc rv (xfdc t) \<longrightarrow> s'\<lparr>globals := globals t\<rparr> \<in> UNIV}} \<inter> ?R'132 (thread_' s) \<inter> \<lbrace>\<^bsup>s\<^esup>thread = tcb_ptr_to_ctcb_ptr thread\<rbrace>} proof (prove)
goal (2 subgoals):
 1. tcb_ptr_to_ctcb_ptr thread \<noteq> NULL \<Longrightarrow> \<Gamma>\<turnstile>\<^bsub>/UNIV\<^esub> (?R'132 (tcb_ptr_to_ctcb_ptr thread)) CALL setThreadState_'proc(tcb_ptr_to_ctcb_ptr thread,SCAST(32 signed \<rightarrow> 32) ThreadState_Restart);;
CALL tcbSchedEnqueue_'proc(tcb_ptr_to_ctcb_ptr thread);;
Guard C_Guard {s. s \<Turnstile>\<^sub>c tcb_ptr_to_ctcb_ptr thread} (\<acute>thread :== h_val (hrs_mem \<acute>t_hrs) (PTR(tcb_C ptr) &(tcb_ptr_to_ctcb_ptr thread\<rightarrow>[''tcbEPNext_C'']))) {s. \<exists>p. ep_queue_relation (cslift s) threads p (thread_' s)}
 2. \<And>s s'. \<lbrakk>(s, s') \<in> rf_sr; valid_objs' s \<and> Invariants_H.valid_queues s \<and> tcb_at' thread s \<and> thread \<noteq> 0 \<and> (\<forall>t\<in>set threads. tcb_at' t s \<and> t \<noteq> 0) \<and> sch_act_wf (ksSchedulerAction s) s; s' \<in> {s'. thread_' s' = tcb_ptr_to_ctcb_ptr thread \<and> (\<exists>tcb. cslift s' (thread_' s') = Some tcb \<and> ep_queue_relation (cslift s') threads (thread_' s') (tcbEPNext_C tcb))}\<rbrakk> \<Longrightarrow> ((\<lambda>s. tcb_at' thread s \<and> Invariants_H.valid_queues s \<and> valid_objs' s \<and> valid_tcb_state' Structures_H.thread_state.Restart s \<and> (ksSchedulerAction s = SwitchToThread thread \<longrightarrow> runnable' Structures_H.thread_state.Restart) \<and> (\<forall>p. thread \<in> set (ksReadyQueues s p) \<longrightarrow> runnable' Structures_H.thread_state.Restart) \<and> sch_act_wf (ksSchedulerAction s) s) and (\<lambda>s. Invariants_H.valid_queues s \<and> tcb_at' thread s \<and> (valid_tcb_state' Structures_H.thread_state.Restart and valid_objs') s \<and> tcb_at' thread s) and (\<lambda>s. (valid_objs' and valid_tcb_state' Structures_H.thread_state.Restart) s \<and> Invariants_H.valid_queues s \<and> (if thread = thread then K (runnable' Structures_H.thread_state.Restart) else st_tcb_at' runnable' thread) s \<and> (valid_objs' and valid_tcb_state' Structures_H.thread_state.Restart) s \<and> (\<forall>x\<in>set threads. tcb_at' x s \<and> x \<noteq> 0) \<and> (\<not> runnable' Structures_H.thread_state.Restart \<longrightarrow> sch_act_simple s) \<and> sch_act_wf (ksSchedulerAction s) s) and (\<lambda>_. tcb_ptr_to_ctcb_ptr thread \<noteq> NULL)) s \<and> s' \<in> {s. s \<in> {sa. ts_'_update (\<lambda>_. SCAST(32 signed \<rightarrow> 32) ThreadState_Restart) (tptr_'_update (\<lambda>_. thread_' s) sa) \<in> \<lbrace>\<forall>cl fl. cthread_state_relation_lifted Structures_H.thread_state.Restart (cl\<lparr>tsType_CL := \<acute>ts && mask 4\<rparr>, fl)\<rbrace> \<inter> \<lbrace>\<acute>tptr = \<^bsup>s\<^esup>thread\<rbrace>} \<inter> {s'. \<forall>t rv. dc rv (xfdc t) \<longrightarrow> s'\<lparr>globals := globals t\<rparr> \<in> {sa. tcb_'_update (\<lambda>_. thread_' s) sa \<in> UNIV \<inter> \<lbrace>\<acute>tcb = \<^bsup>s\<^esup>thread\<rbrace>} \<inter> {s'. \<forall>t rv. dc rv (xfdc t) \<longrightarrow> s'\<lparr>globals := globals t\<rparr> \<in> UNIV}} \<inter> ?R'132 (thread_' s) \<inter> \<lbrace>\<^bsup>s\<^esup>thread = tcb_ptr_to_ctcb_ptr thread\<rbrace>} proof (prove)
goal (1 subgoal):
 1. \<And>s s'. \<lbrakk>(s, s') \<in> rf_sr; valid_objs' s \<and> Invariants_H.valid_queues s \<and> tcb_at' thread s \<and> thread \<noteq> 0 \<and> (\<forall>t\<in>set threads. tcb_at' t s \<and> t \<noteq> 0) \<and> sch_act_wf (ksSchedulerAction s) s; s' \<in> {s'. thread_' s' = tcb_ptr_to_ctcb_ptr thread \<and> (\<exists>tcb. cslift s' (thread_' s') = Some tcb \<and> ep_queue_relation (cslift s') threads (thread_' s') (tcbEPNext_C tcb))}\<rbrakk> \<Longrightarrow> ((\<lambda>s. tcb_at' thread s \<and> Invariants_H.valid_queues s \<and> valid_objs' s \<and> valid_tcb_state' Structures_H.thread_state.Restart s \<and> (ksSchedulerAction s = SwitchToThread thread \<longrightarrow> runnable' Structures_H.thread_state.Restart) \<and> (\<forall>p. thread \<in> set (ksReadyQueues s p) \<longrightarrow> runnable' Structures_H.thread_state.Restart) \<and> sch_act_wf (ksSchedulerAction s) s) and (\<lambda>s. Invariants_H.valid_queues s \<and> tcb_at' thread s \<and> (valid_tcb_state' Structures_H.thread_state.Restart and valid_objs') s \<and> tcb_at' thread s) and (\<lambda>s. (valid_objs' and valid_tcb_state' Structures_H.thread_state.Restart) s \<and> Invariants_H.valid_queues s \<and> (if thread = thread then K (runnable' Structures_H.thread_state.Restart) else st_tcb_at' runnable' thread) s \<and> (valid_objs' and valid_tcb_state' Structures_H.thread_state.Restart) s \<and> (\<forall>x\<in>set threads. tcb_at' x s \<and> x \<noteq> 0) \<and> (\<not> runnable' Structures_H.thread_state.Restart \<longrightarrow> sch_act_simple s) \<and> sch_act_wf (ksSchedulerAction s) s) and (\<lambda>_. tcb_ptr_to_ctcb_ptr thread \<noteq> NULL)) s \<and> s' \<in> {s. s \<in> {sa. ts_'_update (\<lambda>_. SCAST(32 signed \<rightarrow> 32) ThreadState_Restart) (tptr_'_update (\<lambda>_. thread_' s) sa) \<in> \<lbrace>\<forall>cl fl. cthread_state_relation_lifted Structures_H.thread_state.Restart (cl\<lparr>tsType_CL := \<acute>ts && mask 4\<rparr>, fl)\<rbrace> \<inter> \<lbrace>\<acute>tptr = \<^bsup>s\<^esup>thread\<rbrace>} \<inter> {s'. \<forall>t rv. dc rv (xfdc t) \<longrightarrow> s'\<lparr>globals := globals t\<rparr> \<in> {sa. tcb_'_update (\<lambda>_. thread_' s) sa \<in> UNIV \<inter> \<lbrace>\<acute>tcb = \<^bsup>s\<^esup>thread\<rbrace>} \<inter> {s'. \<forall>t rv. dc rv (xfdc t) \<longrightarrow> s'\<lparr>globals := globals t\<rparr> \<in> UNIV}} \<inter> {sa. sa \<Turnstile>\<^sub>c thread_' s \<and> (\<forall>x. ksSchedulerAction_' (globals sa) = tcb_Ptr x \<and> x \<noteq> 0 \<and> x \<noteq> 1 \<longrightarrow> (\<exists>d v. option_map2 tcbPriority_C (cslift sa) (tcb_Ptr x) = Some v \<and> unat v \<le> Config_H.numPriorities \<and> option_map2 tcbDomain_C (cslift sa) (tcb_Ptr x) = Some d \<and> unat d < numDomains \<and> (StateRelation_C.end_C (ksReadyQueues_' (globals sa).[unat (d * 0x100 + v)]) \<noteq> NULL \<longrightarrow> option_map2 tcbPriority_C (cslift sa) (head_C (ksReadyQueues_' (globals sa).[unat (d * 0x100 + v)])) \<noteq> None \<and> option_map2 tcbDomain_C (cslift sa) (head_C (ksReadyQueues_' (globals sa).[unat (d * 0x100 + v)])) \<noteq> None))) \<and> (\<forall>t. option_map2 tcbEPNext_C (cslift t) = option_map2 tcbEPNext_C (cslift sa) \<and> option_map2 tcbEPPrev_C (cslift t) = option_map2 tcbEPPrev_C (cslift sa) \<and> option_map2 tcbPriority_C (cslift t) = option_map2 tcbPriority_C (cslift sa) \<and> option_map2 tcbDomain_C (cslift t) = option_map2 tcbDomain_C (cslift sa) \<and> ksReadyQueues_' (globals t) = ksReadyQueues_' (globals sa) \<longrightarrow> (\<exists>d v. option_map2 tcbPriority_C (cslift sa) (thread_' s) = Some v \<and> unat v \<le> Config_H.numPriorities \<and> option_map2 tcbDomain_C (cslift sa) (thread_' s) = Some d \<and> unat d < numDomains \<and> (StateRelation_C.end_C (ksReadyQueues_' (globals sa).[unat (d * 0x100 + v)]) \<noteq> NULL \<longrightarrow> option_map2 tcbPriority_C (cslift sa) (head_C (ksReadyQueues_' (globals sa).[unat (d * 0x100 + v)])) \<noteq> None \<and> option_map2 tcbDomain_C (cslift sa) (head_C (ksReadyQueues_' (globals sa).[unat (d * 0x100 + v)])) \<noteq> None)) \<and> (\<forall>t. option_map2 tcbEPNext_C (cslift t) = option_map2 tcbEPNext_C (cslift sa) \<and> option_map2 tcbEPPrev_C (cslift t) = option_map2 tcbEPPrev_C (cslift sa) \<and> option_map2 tcbPriority_C (cslift t) = option_map2 tcbPriority_C (cslift sa) \<and> option_map2 tcbDomain_C (cslift t) = option_map2 tcbDomain_C (cslift sa) \<longrightarrow> t \<Turnstile>\<^sub>c thread_' s \<longrightarrow> (\<exists>p. ep_queue_relation (cslift t) threads p (h_val (hrs_mem (t_hrs_' (globals t))) (PTR(tcb_C ptr) &(thread_' s\<rightarrow>[''tcbEPNext_C'']))))))} \<inter> \<lbrace>\<^bsup>s\<^esup>thread = tcb_ptr_to_ctcb_ptr thread\<rbrace>} proof (prove)
goal (1 subgoal):
 1. \<And>s s' tcb. \<lbrakk>(s, s') \<in> rf_sr; valid_objs' s; thread_' s' = tcb_ptr_to_ctcb_ptr thread; Invariants_H.valid_queues s; cslift s' (tcb_ptr_to_ctcb_ptr thread) = Some tcb; ep_queue_relation (cslift s') threads (tcb_ptr_to_ctcb_ptr thread) (tcbEPNext_C tcb); tcb_at' thread s; thread \<noteq> 0; \<forall>t\<in>set threads. tcb_at' t s \<and> t \<noteq> 0; sch_act_wf (ksSchedulerAction s) s\<rbrakk> \<Longrightarrow> s' \<Turnstile>\<^sub>c tcb_ptr_to_ctcb_ptr thread \<and> (\<forall>x. ksSchedulerAction_' (globals s') = tcb_Ptr x \<and> x \<noteq> 0 \<and> x \<noteq> 1 \<longrightarrow> (\<exists>d v. option_map2 tcbPriority_C (cslift s') (tcb_Ptr x) = Some v \<and> unat v \<le> Config_H.numPriorities \<and> option_map2 tcbDomain_C (cslift s') (tcb_Ptr x) = Some d \<and> unat d < numDomains \<and> (StateRelation_C.end_C (ksReadyQueues_' (globals s').[unat (d * 0x100 + v)]) \<noteq> NULL \<longrightarrow> (\<exists>y. option_map2 tcbPriority_C (cslift s') (head_C (ksReadyQueues_' (globals s').[unat (d * 0x100 + v)])) = Some y) \<and> (\<exists>y. option_map2 tcbDomain_C (cslift s') (head_C (ksReadyQueues_' (globals s').[unat (d * 0x100 + v)])) = Some y)))) \<and> ((\<exists>t. option_map2 tcbEPNext_C (cslift t) = option_map2 tcbEPNext_C (cslift s') \<and> option_map2 tcbEPPrev_C (cslift t) = option_map2 tcbEPPrev_C (cslift s') \<and> option_map2 tcbPriority_C (cslift t) = option_map2 tcbPriority_C (cslift s') \<and> option_map2 tcbDomain_C (cslift t) = option_map2 tcbDomain_C (cslift s') \<and> ksReadyQueues_' (globals t) = ksReadyQueues_' (globals s')) \<longrightarrow> (\<exists>d v. option_map2 tcbPriority_C (cslift s') (tcb_ptr_to_ctcb_ptr thread) = Some v \<and> unat v \<le> Config_H.numPriorities \<and> option_map2 tcbDomain_C (cslift s') (tcb_ptr_to_ctcb_ptr thread) = Some d \<and> unat d < numDomains \<and> (StateRelation_C.end_C (ksReadyQueues_' (globals s').[unat (d * 0x100 + v)]) \<noteq> NULL \<longrightarrow> (\<exists>y. option_map2 tcbPriority_C (cslift s') (head_C (ksReadyQueues_' (globals s').[unat (d * 0x100 + v)])) = Some y) \<and> (\<exists>y. option_map2 tcbDomain_C (cslift s') (head_C (ksReadyQueues_' (globals s').[unat (d * 0x100 + v)])) = Some y))) \<and> (\<forall>t. option_map2 tcbEPNext_C (cslift t) = option_map2 tcbEPNext_C (cslift s') \<and> option_map2 tcbEPPrev_C (cslift t) = option_map2 tcbEPPrev_C (cslift s') \<and> option_map2 tcbPriority_C (cslift t) = option_map2 tcbPriority_C (cslift s') \<and> option_map2 tcbDomain_C (cslift t) = option_map2 tcbDomain_C (cslift s') \<longrightarrow> t \<Turnstile>\<^sub>c tcb_ptr_to_ctcb_ptr thread \<longrightarrow> (\<exists>p. ep_queue_relation (cslift t) threads p (h_val (hrs_mem (t_hrs_' (globals t))) (PTR(tcb_C ptr) &(tcb_ptr_to_ctcb_ptr thread\<rightarrow>[''tcbEPNext_C''])))))) proof (prove)
goal (1 subgoal):
 1. \<And>s s' tcb. \<lbrakk>(s, s') \<in> rf_sr; valid_objs' s; thread_' s' = tcb_ptr_to_ctcb_ptr thread; Invariants_H.valid_queues s; cslift s' (tcb_ptr_to_ctcb_ptr thread) = Some tcb; ep_queue_relation (cslift s') threads (tcb_ptr_to_ctcb_ptr thread) (tcbEPNext_C tcb); thread \<noteq> 0; \<forall>t\<in>set threads. tcb_at' t s \<and> t \<noteq> 0; sch_act_wf (ksSchedulerAction s) s; \<exists>ko ko'. ko_at' ko thread s \<and> True \<and> cslift s' (tcb_ptr_to_ctcb_ptr thread) = Some ko' \<and> ctcb_relation ko ko'\<rbrakk> \<Longrightarrow> s' \<Turnstile>\<^sub>c tcb_ptr_to_ctcb_ptr thread \<and> (\<forall>x. ksSchedulerAction_' (globals s') = tcb_Ptr x \<and> x \<noteq> 0 \<and> x \<noteq> 1 \<longrightarrow> (\<exists>d v. option_map2 tcbPriority_C (cslift s') (tcb_Ptr x) = Some v \<and> unat v \<le> Config_H.numPriorities \<and> option_map2 tcbDomain_C (cslift s') (tcb_Ptr x) = Some d \<and> unat d < numDomains \<and> (StateRelation_C.end_C (ksReadyQueues_' (globals s').[unat (d * 0x100 + v)]) \<noteq> NULL \<longrightarrow> (\<exists>y. option_map2 tcbPriority_C (cslift s') (head_C (ksReadyQueues_' (globals s').[unat (d * 0x100 + v)])) = Some y) \<and> (\<exists>y. option_map2 tcbDomain_C (cslift s') (head_C (ksReadyQueues_' (globals s').[unat (d * 0x100 + v)])) = Some y)))) \<and> ((\<exists>t. option_map2 tcbEPNext_C (cslift t) = option_map2 tcbEPNext_C (cslift s') \<and> option_map2 tcbEPPrev_C (cslift t) = option_map2 tcbEPPrev_C (cslift s') \<and> option_map2 tcbPriority_C (cslift t) = option_map2 tcbPriority_C (cslift s') \<and> option_map2 tcbDomain_C (cslift t) = option_map2 tcbDomain_C (cslift s') \<and> ksReadyQueues_' (globals t) = ksReadyQueues_' (globals s')) \<longrightarrow> (\<exists>d v. option_map2 tcbPriority_C (cslift s') (tcb_ptr_to_ctcb_ptr thread) = Some v \<and> unat v \<le> Config_H.numPriorities \<and> option_map2 tcbDomain_C (cslift s') (tcb_ptr_to_ctcb_ptr thread) = Some d \<and> unat d < numDomains \<and> (StateRelation_C.end_C (ksReadyQueues_' (globals s').[unat (d * 0x100 + v)]) \<noteq> NULL \<longrightarrow> (\<exists>y. option_map2 tcbPriority_C (cslift s') (head_C (ksReadyQueues_' (globals s').[unat (d * 0x100 + v)])) = Some y) \<and> (\<exists>y. option_map2 tcbDomain_C (cslift s') (head_C (ksReadyQueues_' (globals s').[unat (d * 0x100 + v)])) = Some y))) \<and> (\<forall>t. option_map2 tcbEPNext_C (cslift t) = option_map2 tcbEPNext_C (cslift s') \<and> option_map2 tcbEPPrev_C (cslift t) = option_map2 tcbEPPrev_C (cslift s') \<and> option_map2 tcbPriority_C (cslift t) = option_map2 tcbPriority_C (cslift s') \<and> option_map2 tcbDomain_C (cslift t) = option_map2 tcbDomain_C (cslift s') \<longrightarrow> t \<Turnstile>\<^sub>c tcb_ptr_to_ctcb_ptr thread \<longrightarrow> (\<exists>p. ep_queue_relation (cslift t) threads p (h_val (hrs_mem (t_hrs_' (globals t))) (PTR(tcb_C ptr) &(tcb_ptr_to_ctcb_ptr thread\<rightarrow>[''tcbEPNext_C''])))))) proof (prove)
goal (1 subgoal):
 1. \<And>s s' tcb ko. \<lbrakk>(s, s') \<in> rf_sr; valid_objs' s; thread_' s' = tcb_ptr_to_ctcb_ptr thread; Invariants_H.valid_queues s; cslift s' (tcb_ptr_to_ctcb_ptr thread) = Some tcb; ep_queue_relation (cslift s') threads (tcb_ptr_to_ctcb_ptr thread) (tcbEPNext_C tcb); thread \<noteq> 0; \<forall>t\<in>set threads. tcb_at' t s \<and> t \<noteq> 0; sch_act_wf (ksSchedulerAction s) s; ko_at' ko thread s; ctcb_relation ko tcb\<rbrakk> \<Longrightarrow> (\<forall>x. ksSchedulerAction_' (globals s') = tcb_Ptr x \<and> x \<noteq> 0 \<and> x \<noteq> 1 \<longrightarrow> (\<exists>d v. option_map2 tcbPriority_C (cslift s') (tcb_Ptr x) = Some v \<and> unat v \<le> Config_H.numPriorities \<and> option_map2 tcbDomain_C (cslift s') (tcb_Ptr x) = Some d \<and> unat d < numDomains \<and> (StateRelation_C.end_C (ksReadyQueues_' (globals s').[unat (d * 0x100 + v)]) \<noteq> NULL \<longrightarrow> (\<exists>y. option_map2 tcbPriority_C (cslift s') (head_C (ksReadyQueues_' (globals s').[unat (d * 0x100 + v)])) = Some y) \<and> (\<exists>y. option_map2 tcbDomain_C (cslift s') (head_C (ksReadyQueues_' (globals s').[unat (d * 0x100 + v)])) = Some y)))) \<and> ((\<exists>t. option_map2 tcbEPNext_C (cslift t) = option_map2 tcbEPNext_C (cslift s') \<and> option_map2 tcbEPPrev_C (cslift t) = option_map2 tcbEPPrev_C (cslift s') \<and> option_map2 tcbPriority_C (cslift t) = option_map2 tcbPriority_C (cslift s') \<and> option_map2 tcbDomain_C (cslift t) = option_map2 tcbDomain_C (cslift s') \<and> ksReadyQueues_' (globals t) = ksReadyQueues_' (globals s')) \<longrightarrow> (\<exists>d v. option_map2 tcbPriority_C (cslift s') (tcb_ptr_to_ctcb_ptr thread) = Some v \<and> unat v \<le> Config_H.numPriorities \<and> option_map2 tcbDomain_C (cslift s') (tcb_ptr_to_ctcb_ptr thread) = Some d \<and> unat d < numDomains \<and> (StateRelation_C.end_C (ksReadyQueues_' (globals s').[unat (d * 0x100 + v)]) \<noteq> NULL \<longrightarrow> (\<exists>y. option_map2 tcbPriority_C (cslift s') (head_C (ksReadyQueues_' (globals s').[unat (d * 0x100 + v)])) = Some y) \<and> (\<exists>y. option_map2 tcbDomain_C (cslift s') (head_C (ksReadyQueues_' (globals s').[unat (d * 0x100 + v)])) = Some y))) \<and> (\<forall>t. option_map2 tcbEPNext_C (cslift t) = option_map2 tcbEPNext_C (cslift s') \<and> option_map2 tcbEPPrev_C (cslift t) = option_map2 tcbEPPrev_C (cslift s') \<and> option_map2 tcbPriority_C (cslift t) = option_map2 tcbPriority_C (cslift s') \<and> option_map2 tcbDomain_C (cslift t) = option_map2 tcbDomain_C (cslift s') \<longrightarrow> t \<Turnstile>\<^sub>c tcb_ptr_to_ctcb_ptr thread \<longrightarrow> (\<exists>p. ep_queue_relation (cslift t) threads p (h_val (hrs_mem (t_hrs_' (globals t))) (PTR(tcb_C ptr) &(tcb_ptr_to_ctcb_ptr thread\<rightarrow>[''tcbEPNext_C''])))))) proof (prove)
goal (2 subgoals):
 1. \<And>s s' tcb ko. \<lbrakk>(s, s') \<in> rf_sr; valid_objs' s; thread_' s' = tcb_ptr_to_ctcb_ptr thread; Invariants_H.valid_queues s; cslift s' (tcb_ptr_to_ctcb_ptr thread) = Some tcb; ep_queue_relation (cslift s') threads (tcb_ptr_to_ctcb_ptr thread) (tcbEPNext_C tcb); thread \<noteq> 0; \<forall>t\<in>set threads. tcb_at' t s \<and> t \<noteq> 0; sch_act_wf (ksSchedulerAction s) s; ko_at' ko thread s; ctcb_relation ko tcb\<rbrakk> \<Longrightarrow> \<forall>x. ksSchedulerAction_' (globals s') = tcb_Ptr x \<and> x \<noteq> 0 \<and> x \<noteq> 1 \<longrightarrow> (\<exists>d v. option_map2 tcbPriority_C (cslift s') (tcb_Ptr x) = Some v \<and> unat v \<le> Config_H.numPriorities \<and> option_map2 tcbDomain_C (cslift s') (tcb_Ptr x) = Some d \<and> unat d < numDomains \<and> (StateRelation_C.end_C (ksReadyQueues_' (globals s').[unat (d * 0x100 + v)]) \<noteq> NULL \<longrightarrow> (\<exists>y. option_map2 tcbPriority_C (cslift s') (head_C (ksReadyQueues_' (globals s').[unat (d * 0x100 + v)])) = Some y) \<and> (\<exists>y. option_map2 tcbDomain_C (cslift s') (head_C (ksReadyQueues_' (globals s').[unat (d * 0x100 + v)])) = Some y)))
 2. \<And>s s' tcb ko. \<lbrakk>(s, s') \<in> rf_sr; valid_objs' s; thread_' s' = tcb_ptr_to_ctcb_ptr thread; Invariants_H.valid_queues s; cslift s' (tcb_ptr_to_ctcb_ptr thread) = Some tcb; ep_queue_relation (cslift s') threads (tcb_ptr_to_ctcb_ptr thread) (tcbEPNext_C tcb); thread \<noteq> 0; \<forall>t\<in>set threads. tcb_at' t s \<and> t \<noteq> 0; sch_act_wf (ksSchedulerAction s) s; ko_at' ko thread s; ctcb_relation ko tcb\<rbrakk> \<Longrightarrow> (\<exists>t. option_map2 tcbEPNext_C (cslift t) = option_map2 tcbEPNext_C (cslift s') \<and> option_map2 tcbEPPrev_C (cslift t) = option_map2 tcbEPPrev_C (cslift s') \<and> option_map2 tcbPriority_C (cslift t) = option_map2 tcbPriority_C (cslift s') \<and> option_map2 tcbDomain_C (cslift t) = option_map2 tcbDomain_C (cslift s') \<and> ksReadyQueues_' (globals t) = ksReadyQueues_' (globals s')) \<longrightarrow> (\<exists>d v. option_map2 tcbPriority_C (cslift s') (tcb_ptr_to_ctcb_ptr thread) = Some v \<and> unat v \<le> Config_H.numPriorities \<and> option_map2 tcbDomain_C (cslift s') (tcb_ptr_to_ctcb_ptr thread) = Some d \<and> unat d < numDomains \<and> (StateRelation_C.end_C (ksReadyQueues_' (globals s').[unat (d * 0x100 + v)]) \<noteq> NULL \<longrightarrow> (\<exists>y. option_map2 tcbPriority_C (cslift s') (head_C (ksReadyQueues_' (globals s').[unat (d * 0x100 + v)])) = Some y) \<and> (\<exists>y. option_map2 tcbDomain_C (cslift s') (head_C (ksReadyQueues_' (globals s').[unat (d * 0x100 + v)])) = Some y))) \<and> (\<forall>t. option_map2 tcbEPNext_C (cslift t) = option_map2 tcbEPNext_C (cslift s') \<and> option_map2 tcbEPPrev_C (cslift t) = option_map2 tcbEPPrev_C (cslift s') \<and> option_map2 tcbPriority_C (cslift t) = option_map2 tcbPriority_C (cslift s') \<and> option_map2 tcbDomain_C (cslift t) = option_map2 tcbDomain_C (cslift s') \<longrightarrow> t \<Turnstile>\<^sub>c tcb_ptr_to_ctcb_ptr thread \<longrightarrow> (\<exists>p. ep_queue_relation (cslift t) threads p (h_val (hrs_mem (t_hrs_' (globals t))) (PTR(tcb_C ptr) &(tcb_ptr_to_ctcb_ptr thread\<rightarrow>[''tcbEPNext_C'']))))) proof (prove)
goal (2 subgoals):
 1. \<And>s s' tcb ko x. \<lbrakk>(s, s') \<in> rf_sr; valid_objs' s; thread_' s' = tcb_ptr_to_ctcb_ptr thread; Invariants_H.valid_queues s; cslift s' (tcb_ptr_to_ctcb_ptr thread) = Some tcb; ep_queue_relation (cslift s') threads (tcb_ptr_to_ctcb_ptr thread) (tcbEPNext_C tcb); thread \<noteq> 0; \<forall>t\<in>set threads. tcb_at' t s \<and> t \<noteq> 0; sch_act_wf (ksSchedulerAction s) s; ko_at' ko thread s; ctcb_relation ko tcb; ksSchedulerAction_' (globals s') = tcb_Ptr x; x \<noteq> 0; x \<noteq> 1\<rbrakk> \<Longrightarrow> \<exists>d v. option_map2 tcbPriority_C (cslift s') (tcb_Ptr x) = Some v \<and> unat v \<le> Config_H.numPriorities \<and> option_map2 tcbDomain_C (cslift s') (tcb_Ptr x) = Some d \<and> unat d < numDomains \<and> (StateRelation_C.end_C (ksReadyQueues_' (globals s').[unat (d * 0x100 + v)]) \<noteq> NULL \<longrightarrow> (\<exists>y. option_map2 tcbPriority_C (cslift s') (head_C (ksReadyQueues_' (globals s').[unat (d * 0x100 + v)])) = Some y) \<and> (\<exists>y. option_map2 tcbDomain_C (cslift s') (head_C (ksReadyQueues_' (globals s').[unat (d * 0x100 + v)])) = Some y))
 2. \<And>s s' tcb ko. \<lbrakk>(s, s') \<in> rf_sr; valid_objs' s; thread_' s' = tcb_ptr_to_ctcb_ptr thread; Invariants_H.valid_queues s; cslift s' (tcb_ptr_to_ctcb_ptr thread) = Some tcb; ep_queue_relation (cslift s') threads (tcb_ptr_to_ctcb_ptr thread) (tcbEPNext_C tcb); thread \<noteq> 0; \<forall>t\<in>set threads. tcb_at' t s \<and> t \<noteq> 0; sch_act_wf (ksSchedulerAction s) s; ko_at' ko thread s; ctcb_relation ko tcb\<rbrakk> \<Longrightarrow> (\<exists>t. option_map2 tcbEPNext_C (cslift t) = option_map2 tcbEPNext_C (cslift s') \<and> option_map2 tcbEPPrev_C (cslift t) = option_map2 tcbEPPrev_C (cslift s') \<and> option_map2 tcbPriority_C (cslift t) = option_map2 tcbPriority_C (cslift s') \<and> option_map2 tcbDomain_C (cslift t) = option_map2 tcbDomain_C (cslift s') \<and> ksReadyQueues_' (globals t) = ksReadyQueues_' (globals s')) \<longrightarrow> (\<exists>d v. option_map2 tcbPriority_C (cslift s') (tcb_ptr_to_ctcb_ptr thread) = Some v \<and> unat v \<le> Config_H.numPriorities \<and> option_map2 tcbDomain_C (cslift s') (tcb_ptr_to_ctcb_ptr thread) = Some d \<and> unat d < numDomains \<and> (StateRelation_C.end_C (ksReadyQueues_' (globals s').[unat (d * 0x100 + v)]) \<noteq> NULL \<longrightarrow> (\<exists>y. option_map2 tcbPriority_C (cslift s') (head_C (ksReadyQueues_' (globals s').[unat (d * 0x100 + v)])) = Some y) \<and> (\<exists>y. option_map2 tcbDomain_C (cslift s') (head_C (ksReadyQueues_' (globals s').[unat (d * 0x100 + v)])) = Some y))) \<and> (\<forall>t. option_map2 tcbEPNext_C (cslift t) = option_map2 tcbEPNext_C (cslift s') \<and> option_map2 tcbEPPrev_C (cslift t) = option_map2 tcbEPPrev_C (cslift s') \<and> option_map2 tcbPriority_C (cslift t) = option_map2 tcbPriority_C (cslift s') \<and> option_map2 tcbDomain_C (cslift t) = option_map2 tcbDomain_C (cslift s') \<longrightarrow> t \<Turnstile>\<^sub>c tcb_ptr_to_ctcb_ptr thread \<longrightarrow> (\<exists>p. ep_queue_relation (cslift t) threads p (h_val (hrs_mem (t_hrs_' (globals t))) (PTR(tcb_C ptr) &(tcb_ptr_to_ctcb_ptr thread\<rightarrow>[''tcbEPNext_C'']))))) proof (prove)
goal (2 subgoals):
 1. \<And>s s' tcb ko x. \<lbrakk>(s, s') \<in> rf_sr; valid_objs' s; thread_' s' = tcb_ptr_to_ctcb_ptr thread; Invariants_H.valid_queues s; cslift s' (tcb_ptr_to_ctcb_ptr thread) = Some tcb; ep_queue_relation (cslift s') threads (tcb_ptr_to_ctcb_ptr thread) (tcbEPNext_C tcb); thread \<noteq> 0; \<forall>t\<in>set threads. tcb_at' t s \<and> t \<noteq> 0; sch_act_wf (ksSchedulerAction s) s; ko_at' ko thread s; ctcb_relation ko tcb; ksSchedulerAction_' (globals s') = tcb_Ptr x; x \<noteq> 0; x \<noteq> 1; cscheduler_action_relation (ksSchedulerAction s) (ksSchedulerAction_' (globals s'))\<rbrakk> \<Longrightarrow> \<exists>d v. option_map2 tcbPriority_C (cslift s') (tcb_Ptr x) = Some v \<and> unat v \<le> Config_H.numPriorities \<and> option_map2 tcbDomain_C (cslift s') (tcb_Ptr x) = Some d \<and> unat d < numDomains \<and> (StateRelation_C.end_C (ksReadyQueues_' (globals s').[unat (d * 0x100 + v)]) \<noteq> NULL \<longrightarrow> (\<exists>y. option_map2 tcbPriority_C (cslift s') (head_C (ksReadyQueues_' (globals s').[unat (d * 0x100 + v)])) = Some y) \<and> (\<exists>y. option_map2 tcbDomain_C (cslift s') (head_C (ksReadyQueues_' (globals s').[unat (d * 0x100 + v)])) = Some y))
 2. \<And>s s' tcb ko. \<lbrakk>(s, s') \<in> rf_sr; valid_objs' s; thread_' s' = tcb_ptr_to_ctcb_ptr thread; Invariants_H.valid_queues s; cslift s' (tcb_ptr_to_ctcb_ptr thread) = Some tcb; ep_queue_relation (cslift s') threads (tcb_ptr_to_ctcb_ptr thread) (tcbEPNext_C tcb); thread \<noteq> 0; \<forall>t\<in>set threads. tcb_at' t s \<and> t \<noteq> 0; sch_act_wf (ksSchedulerAction s) s; ko_at' ko thread s; ctcb_relation ko tcb\<rbrakk> \<Longrightarrow> (\<exists>t. option_map2 tcbEPNext_C (cslift t) = option_map2 tcbEPNext_C (cslift s') \<and> option_map2 tcbEPPrev_C (cslift t) = option_map2 tcbEPPrev_C (cslift s') \<and> option_map2 tcbPriority_C (cslift t) = option_map2 tcbPriority_C (cslift s') \<and> option_map2 tcbDomain_C (cslift t) = option_map2 tcbDomain_C (cslift s') \<and> ksReadyQueues_' (globals t) = ksReadyQueues_' (globals s')) \<longrightarrow> (\<exists>d v. option_map2 tcbPriority_C (cslift s') (tcb_ptr_to_ctcb_ptr thread) = Some v \<and> unat v \<le> Config_H.numPriorities \<and> option_map2 tcbDomain_C (cslift s') (tcb_ptr_to_ctcb_ptr thread) = Some d \<and> unat d < numDomains \<and> (StateRelation_C.end_C (ksReadyQueues_' (globals s').[unat (d * 0x100 + v)]) \<noteq> NULL \<longrightarrow> (\<exists>y. option_map2 tcbPriority_C (cslift s') (head_C (ksReadyQueues_' (globals s').[unat (d * 0x100 + v)])) = Some y) \<and> (\<exists>y. option_map2 tcbDomain_C (cslift s') (head_C (ksReadyQueues_' (globals s').[unat (d * 0x100 + v)])) = Some y))) \<and> (\<forall>t. option_map2 tcbEPNext_C (cslift t) = option_map2 tcbEPNext_C (cslift s') \<and> option_map2 tcbEPPrev_C (cslift t) = option_map2 tcbEPPrev_C (cslift s') \<and> option_map2 tcbPriority_C (cslift t) = option_map2 tcbPriority_C (cslift s') \<and> option_map2 tcbDomain_C (cslift t) = option_map2 tcbDomain_C (cslift s') \<longrightarrow> t \<Turnstile>\<^sub>c tcb_ptr_to_ctcb_ptr thread \<longrightarrow> (\<exists>p. ep_queue_relation (cslift t) threads p (h_val (hrs_mem (t_hrs_' (globals t))) (PTR(tcb_C ptr) &(tcb_ptr_to_ctcb_ptr thread\<rightarrow>[''tcbEPNext_C'']))))) proof (prove)
goal (2 subgoals):
 1. \<And>s s' tcb ko x x3. \<lbrakk>(s, s') \<in> rf_sr; valid_objs' s; thread_' s' = tcb_ptr_to_ctcb_ptr thread; Invariants_H.valid_queues s; cslift s' (tcb_ptr_to_ctcb_ptr thread) = Some tcb; ep_queue_relation (cslift s') threads (tcb_ptr_to_ctcb_ptr thread) (tcbEPNext_C tcb); thread \<noteq> 0; \<forall>t\<in>set threads. tcb_at' t s \<and> t \<noteq> 0; ko_at' ko thread s; ctcb_relation ko tcb; ksSchedulerAction_' (globals s') = tcb_ptr_to_ctcb_ptr x3; x \<noteq> 0; x \<noteq> 1; ksSchedulerAction s = SwitchToThread x3; tcb_Ptr x = tcb_ptr_to_ctcb_ptr x3; obj_at' (runnable' \<circ> tcbState) x3 s; tcb_in_cur_domain' x3 s\<rbrakk> \<Longrightarrow> \<exists>d v. option_map2 tcbPriority_C (cslift s') (tcb_ptr_to_ctcb_ptr x3) = Some v \<and> unat v \<le> Config_H.numPriorities \<and> option_map2 tcbDomain_C (cslift s') (tcb_ptr_to_ctcb_ptr x3) = Some d \<and> unat d < numDomains \<and> (StateRelation_C.end_C (ksReadyQueues_' (globals s').[unat (d * 0x100 + v)]) \<noteq> NULL \<longrightarrow> (\<exists>y. option_map2 tcbPriority_C (cslift s') (head_C (ksReadyQueues_' (globals s').[unat (d * 0x100 + v)])) = Some y) \<and> (\<exists>y. option_map2 tcbDomain_C (cslift s') (head_C (ksReadyQueues_' (globals s').[unat (d * 0x100 + v)])) = Some y))
 2. \<And>s s' tcb ko. \<lbrakk>(s, s') \<in> rf_sr; valid_objs' s; thread_' s' = tcb_ptr_to_ctcb_ptr thread; Invariants_H.valid_queues s; cslift s' (tcb_ptr_to_ctcb_ptr thread) = Some tcb; ep_queue_relation (cslift s') threads (tcb_ptr_to_ctcb_ptr thread) (tcbEPNext_C tcb); thread \<noteq> 0; \<forall>t\<in>set threads. tcb_at' t s \<and> t \<noteq> 0; sch_act_wf (ksSchedulerAction s) s; ko_at' ko thread s; ctcb_relation ko tcb\<rbrakk> \<Longrightarrow> (\<exists>t. option_map2 tcbEPNext_C (cslift t) = option_map2 tcbEPNext_C (cslift s') \<and> option_map2 tcbEPPrev_C (cslift t) = option_map2 tcbEPPrev_C (cslift s') \<and> option_map2 tcbPriority_C (cslift t) = option_map2 tcbPriority_C (cslift s') \<and> option_map2 tcbDomain_C (cslift t) = option_map2 tcbDomain_C (cslift s') \<and> ksReadyQueues_' (globals t) = ksReadyQueues_' (globals s')) \<longrightarrow> (\<exists>d v. option_map2 tcbPriority_C (cslift s') (tcb_ptr_to_ctcb_ptr thread) = Some v \<and> unat v \<le> Config_H.numPriorities \<and> option_map2 tcbDomain_C (cslift s') (tcb_ptr_to_ctcb_ptr thread) = Some d \<and> unat d < numDomains \<and> (StateRelation_C.end_C (ksReadyQueues_' (globals s').[unat (d * 0x100 + v)]) \<noteq> NULL \<longrightarrow> (\<exists>y. option_map2 tcbPriority_C (cslift s') (head_C (ksReadyQueues_' (globals s').[unat (d * 0x100 + v)])) = Some y) \<and> (\<exists>y. option_map2 tcbDomain_C (cslift s') (head_C (ksReadyQueues_' (globals s').[unat (d * 0x100 + v)])) = Some y))) \<and> (\<forall>t. option_map2 tcbEPNext_C (cslift t) = option_map2 tcbEPNext_C (cslift s') \<and> option_map2 tcbEPPrev_C (cslift t) = option_map2 tcbEPPrev_C (cslift s') \<and> option_map2 tcbPriority_C (cslift t) = option_map2 tcbPriority_C (cslift s') \<and> option_map2 tcbDomain_C (cslift t) = option_map2 tcbDomain_C (cslift s') \<longrightarrow> t \<Turnstile>\<^sub>c tcb_ptr_to_ctcb_ptr thread \<longrightarrow> (\<exists>p. ep_queue_relation (cslift t) threads p (h_val (hrs_mem (t_hrs_' (globals t))) (PTR(tcb_C ptr) &(tcb_ptr_to_ctcb_ptr thread\<rightarrow>[''tcbEPNext_C'']))))) proof (prove)
goal (2 subgoals):
 1. \<And>s s' tcb ko x word. \<lbrakk>(s, s') \<in> rf_sr; valid_objs' s; thread_' s' = tcb_ptr_to_ctcb_ptr thread; Invariants_H.valid_queues s; cslift s' (tcb_ptr_to_ctcb_ptr thread) = Some tcb; ep_queue_relation (cslift s') threads (tcb_ptr_to_ctcb_ptr thread) (tcbEPNext_C tcb); thread \<noteq> 0; \<forall>t\<in>set threads. tcb_at' t s \<and> t \<noteq> 0; ko_at' ko thread s; ctcb_relation ko tcb; ksSchedulerAction_' (globals s') = tcb_ptr_to_ctcb_ptr word; x \<noteq> 0; x \<noteq> 1; ksSchedulerAction s = SwitchToThread word; tcb_Ptr x = tcb_ptr_to_ctcb_ptr word; obj_at' (runnable' \<circ> tcbState) word s; tcb_in_cur_domain' word s\<rbrakk> \<Longrightarrow> \<exists>d v. option_map2 tcbPriority_C (cslift s') (tcb_ptr_to_ctcb_ptr word) = Some v \<and> unat v \<le> Config_H.numPriorities \<and> option_map2 tcbDomain_C (cslift s') (tcb_ptr_to_ctcb_ptr word) = Some d \<and> unat d < numDomains \<and> (StateRelation_C.end_C (ksReadyQueues_' (globals s').[unat (d * 0x100 + v)]) \<noteq> NULL \<longrightarrow> (\<exists>y. option_map2 tcbPriority_C (cslift s') (head_C (ksReadyQueues_' (globals s').[unat (d * 0x100 + v)])) = Some y) \<and> (\<exists>y. option_map2 tcbDomain_C (cslift s') (head_C (ksReadyQueues_' (globals s').[unat (d * 0x100 + v)])) = Some y))
 2. \<And>s s' tcb ko. \<lbrakk>(s, s') \<in> rf_sr; valid_objs' s; thread_' s' = tcb_ptr_to_ctcb_ptr thread; Invariants_H.valid_queues s; cslift s' (tcb_ptr_to_ctcb_ptr thread) = Some tcb; ep_queue_relation (cslift s') threads (tcb_ptr_to_ctcb_ptr thread) (tcbEPNext_C tcb); thread \<noteq> 0; \<forall>t\<in>set threads. tcb_at' t s \<and> t \<noteq> 0; sch_act_wf (ksSchedulerAction s) s; ko_at' ko thread s; ctcb_relation ko tcb\<rbrakk> \<Longrightarrow> (\<exists>t. option_map2 tcbEPNext_C (cslift t) = option_map2 tcbEPNext_C (cslift s') \<and> option_map2 tcbEPPrev_C (cslift t) = option_map2 tcbEPPrev_C (cslift s') \<and> option_map2 tcbPriority_C (cslift t) = option_map2 tcbPriority_C (cslift s') \<and> option_map2 tcbDomain_C (cslift t) = option_map2 tcbDomain_C (cslift s') \<and> ksReadyQueues_' (globals t) = ksReadyQueues_' (globals s')) \<longrightarrow> (\<exists>d v. option_map2 tcbPriority_C (cslift s') (tcb_ptr_to_ctcb_ptr thread) = Some v \<and> unat v \<le> Config_H.numPriorities \<and> option_map2 tcbDomain_C (cslift s') (tcb_ptr_to_ctcb_ptr thread) = Some d \<and> unat d < numDomains \<and> (StateRelation_C.end_C (ksReadyQueues_' (globals s').[unat (d * 0x100 + v)]) \<noteq> NULL \<longrightarrow> (\<exists>y. option_map2 tcbPriority_C (cslift s') (head_C (ksReadyQueues_' (globals s').[unat (d * 0x100 + v)])) = Some y) \<and> (\<exists>y. option_map2 tcbDomain_C (cslift s') (head_C (ksReadyQueues_' (globals s').[unat (d * 0x100 + v)])) = Some y))) \<and> (\<forall>t. option_map2 tcbEPNext_C (cslift t) = option_map2 tcbEPNext_C (cslift s') \<and> option_map2 tcbEPPrev_C (cslift t) = option_map2 tcbEPPrev_C (cslift s') \<and> option_map2 tcbPriority_C (cslift t) = option_map2 tcbPriority_C (cslift s') \<and> option_map2 tcbDomain_C (cslift t) = option_map2 tcbDomain_C (cslift s') \<longrightarrow> t \<Turnstile>\<^sub>c tcb_ptr_to_ctcb_ptr thread \<longrightarrow> (\<exists>p. ep_queue_relation (cslift t) threads p (h_val (hrs_mem (t_hrs_' (globals t))) (PTR(tcb_C ptr) &(tcb_ptr_to_ctcb_ptr thread\<rightarrow>[''tcbEPNext_C'']))))) proof (prove)
goal (5 subgoals):
 1. \<And>s s' tcb ko x word. \<lbrakk>(s, s') \<in> rf_sr; valid_objs' s; thread_' s' = tcb_ptr_to_ctcb_ptr thread; Invariants_H.valid_queues s; cslift s' (tcb_ptr_to_ctcb_ptr thread) = Some tcb; ep_queue_relation (cslift s') threads (tcb_ptr_to_ctcb_ptr thread) (tcbEPNext_C tcb); thread \<noteq> 0; \<forall>t\<in>set threads. tcb_at' t s \<and> t \<noteq> 0; ko_at' ko thread s; ctcb_relation ko tcb; ksSchedulerAction_' (globals s') = tcb_ptr_to_ctcb_ptr word; x \<noteq> 0; x \<noteq> 1; ksSchedulerAction s = SwitchToThread word; tcb_Ptr x = tcb_ptr_to_ctcb_ptr word; obj_at' (runnable' \<circ> tcbState) word s; tcb_in_cur_domain' word s\<rbrakk> \<Longrightarrow> obj_at' (?P392 s s' tcb ko x word) word s
 2. \<And>s s' tcb ko x word. \<lbrakk>(s, s') \<in> rf_sr; valid_objs' s; thread_' s' = tcb_ptr_to_ctcb_ptr thread; Invariants_H.valid_queues s; cslift s' (tcb_ptr_to_ctcb_ptr thread) = Some tcb; ep_queue_relation (cslift s') threads (tcb_ptr_to_ctcb_ptr thread) (tcbEPNext_C tcb); thread \<noteq> 0; \<forall>t\<in>set threads. tcb_at' t s \<and> t \<noteq> 0; ko_at' ko thread s; ctcb_relation ko tcb; ksSchedulerAction_' (globals s') = tcb_ptr_to_ctcb_ptr word; x \<noteq> 0; x \<noteq> 1; ksSchedulerAction s = SwitchToThread word; tcb_Ptr x = tcb_ptr_to_ctcb_ptr word; obj_at' (runnable' \<circ> tcbState) word s; tcb_in_cur_domain' word s\<rbrakk> \<Longrightarrow> Invariants_H.valid_queues s
 3. \<And>s s' tcb ko x word. \<lbrakk>(s, s') \<in> rf_sr; valid_objs' s; thread_' s' = tcb_ptr_to_ctcb_ptr thread; Invariants_H.valid_queues s; cslift s' (tcb_ptr_to_ctcb_ptr thread) = Some tcb; ep_queue_relation (cslift s') threads (tcb_ptr_to_ctcb_ptr thread) (tcbEPNext_C tcb); thread \<noteq> 0; \<forall>t\<in>set threads. tcb_at' t s \<and> t \<noteq> 0; ko_at' ko thread s; ctcb_relation ko tcb; ksSchedulerAction_' (globals s') = tcb_ptr_to_ctcb_ptr word; x \<noteq> 0; x \<noteq> 1; ksSchedulerAction s = SwitchToThread word; tcb_Ptr x = tcb_ptr_to_ctcb_ptr word; obj_at' (runnable' \<circ> tcbState) word s; tcb_in_cur_domain' word s\<rbrakk> \<Longrightarrow> valid_objs' s
 4. \<And>s s' tcb ko x word. \<lbrakk>(s, s') \<in> rf_sr; valid_objs' s; thread_' s' = tcb_ptr_to_ctcb_ptr thread; Invariants_H.valid_queues s; cslift s' (tcb_ptr_to_ctcb_ptr thread) = Some tcb; ep_queue_relation (cslift s') threads (tcb_ptr_to_ctcb_ptr thread) (tcbEPNext_C tcb); thread \<noteq> 0; \<forall>t\<in>set threads. tcb_at' t s \<and> t \<noteq> 0; ko_at' ko thread s; ctcb_relation ko tcb; ksSchedulerAction_' (globals s') = tcb_ptr_to_ctcb_ptr word; x \<noteq> 0; x \<noteq> 1; ksSchedulerAction s = SwitchToThread word; tcb_Ptr x = tcb_ptr_to_ctcb_ptr word; obj_at' (runnable' \<circ> tcbState) word s; tcb_in_cur_domain' word s; \<exists>d v. option_map2 tcbPriority_C (cslift s') (tcb_ptr_to_ctcb_ptr word) = Some v \<and> unat v < Config_H.numPriorities \<and> option_map2 tcbDomain_C (cslift s') (tcb_ptr_to_ctcb_ptr word) = Some d \<and> unat d < numDomains \<and> (StateRelation_C.end_C (ksReadyQueues_' (globals s').[unat (d * 0x100 + v)]) \<noteq> NULL \<longrightarrow> option_map2 tcbPriority_C (cslift s') (head_C (ksReadyQueues_' (globals s').[unat (d * 0x100 + v)])) \<noteq> None \<and> option_map2 tcbDomain_C (cslift s') (head_C (ksReadyQueues_' (globals s').[unat (d * 0x100 + v)])) \<noteq> None)\<rbrakk> \<Longrightarrow> \<exists>d v. option_map2 tcbPriority_C (cslift s') (tcb_ptr_to_ctcb_ptr word) = Some v \<and> unat v \<le> Config_H.numPriorities \<and> option_map2 tcbDomain_C (cslift s') (tcb_ptr_to_ctcb_ptr word) = Some d \<and> unat d < numDomains \<and> (StateRelation_C.end_C (ksReadyQueues_' (globals s').[unat (d * 0x100 + v)]) \<noteq> NULL \<longrightarrow> (\<exists>y. option_map2 tcbPriority_C (cslift s') (head_C (ksReadyQueues_' (globals s').[unat (d * 0x100 + v)])) = Some y) \<and> (\<exists>y. option_map2 tcbDomain_C (cslift s') (head_C (ksReadyQueues_' (globals s').[unat (d * 0x100 + v)])) = Some y))
 5. \<And>s s' tcb ko. \<lbrakk>(s, s') \<in> rf_sr; valid_objs' s; thread_' s' = tcb_ptr_to_ctcb_ptr thread; Invariants_H.valid_queues s; cslift s' (tcb_ptr_to_ctcb_ptr thread) = Some tcb; ep_queue_relation (cslift s') threads (tcb_ptr_to_ctcb_ptr thread) (tcbEPNext_C tcb); thread \<noteq> 0; \<forall>t\<in>set threads. tcb_at' t s \<and> t \<noteq> 0; sch_act_wf (ksSchedulerAction s) s; ko_at' ko thread s; ctcb_relation ko tcb\<rbrakk> \<Longrightarrow> (\<exists>t. option_map2 tcbEPNext_C (cslift t) = option_map2 tcbEPNext_C (cslift s') \<and> option_map2 tcbEPPrev_C (cslift t) = option_map2 tcbEPPrev_C (cslift s') \<and> option_map2 tcbPriority_C (cslift t) = option_map2 tcbPriority_C (cslift s') \<and> option_map2 tcbDomain_C (cslift t) = option_map2 tcbDomain_C (cslift s') \<and> ksReadyQueues_' (globals t) = ksReadyQueues_' (globals s')) \<longrightarrow> (\<exists>d v. option_map2 tcbPriority_C (cslift s') (tcb_ptr_to_ctcb_ptr thread) = Some v \<and> unat v \<le> Config_H.numPriorities \<and> option_map2 tcbDomain_C (cslift s') (tcb_ptr_to_ctcb_ptr thread) = Some d \<and> unat d < numDomains \<and> (StateRelation_C.end_C (ksReadyQueues_' (globals s').[unat (d * 0x100 + v)]) \<noteq> NULL \<longrightarrow> (\<exists>y. option_map2 tcbPriority_C (cslift s') (head_C (ksReadyQueues_' (globals s').[unat (d * 0x100 + v)])) = Some y) \<and> (\<exists>y. option_map2 tcbDomain_C (cslift s') (head_C (ksReadyQueues_' (globals s').[unat (d * 0x100 + v)])) = Some y))) \<and> (\<forall>t. option_map2 tcbEPNext_C (cslift t) = option_map2 tcbEPNext_C (cslift s') \<and> option_map2 tcbEPPrev_C (cslift t) = option_map2 tcbEPPrev_C (cslift s') \<and> option_map2 tcbPriority_C (cslift t) = option_map2 tcbPriority_C (cslift s') \<and> option_map2 tcbDomain_C (cslift t) = option_map2 tcbDomain_C (cslift s') \<longrightarrow> t \<Turnstile>\<^sub>c tcb_ptr_to_ctcb_ptr thread \<longrightarrow> (\<exists>p. ep_queue_relation (cslift t) threads p (h_val (hrs_mem (t_hrs_' (globals t))) (PTR(tcb_C ptr) &(tcb_ptr_to_ctcb_ptr thread\<rightarrow>[''tcbEPNext_C'']))))) proof (prove)
goal (4 subgoals):
 1. \<And>s s' tcb ko x word. \<lbrakk>(s, s') \<in> rf_sr; valid_objs' s; thread_' s' = tcb_ptr_to_ctcb_ptr thread; Invariants_H.valid_queues s; cslift s' (tcb_ptr_to_ctcb_ptr thread) = Some tcb; ep_queue_relation (cslift s') threads (tcb_ptr_to_ctcb_ptr thread) (tcbEPNext_C tcb); thread \<noteq> 0; \<forall>t\<in>set threads. tcb_at' t s \<and> t \<noteq> 0; ko_at' ko thread s; ctcb_relation ko tcb; ksSchedulerAction_' (globals s') = tcb_ptr_to_ctcb_ptr word; x \<noteq> 0; x \<noteq> 1; ksSchedulerAction s = SwitchToThread word; tcb_Ptr x = tcb_ptr_to_ctcb_ptr word; obj_at' (runnable' \<circ> tcbState) word s; tcb_in_cur_domain' word s\<rbrakk> \<Longrightarrow> Invariants_H.valid_queues s
 2. \<And>s s' tcb ko x word. \<lbrakk>(s, s') \<in> rf_sr; valid_objs' s; thread_' s' = tcb_ptr_to_ctcb_ptr thread; Invariants_H.valid_queues s; cslift s' (tcb_ptr_to_ctcb_ptr thread) = Some tcb; ep_queue_relation (cslift s') threads (tcb_ptr_to_ctcb_ptr thread) (tcbEPNext_C tcb); thread \<noteq> 0; \<forall>t\<in>set threads. tcb_at' t s \<and> t \<noteq> 0; ko_at' ko thread s; ctcb_relation ko tcb; ksSchedulerAction_' (globals s') = tcb_ptr_to_ctcb_ptr word; x \<noteq> 0; x \<noteq> 1; ksSchedulerAction s = SwitchToThread word; tcb_Ptr x = tcb_ptr_to_ctcb_ptr word; obj_at' (runnable' \<circ> tcbState) word s; tcb_in_cur_domain' word s\<rbrakk> \<Longrightarrow> valid_objs' s
 3. \<And>s s' tcb ko x word. \<lbrakk>(s, s') \<in> rf_sr; valid_objs' s; thread_' s' = tcb_ptr_to_ctcb_ptr thread; Invariants_H.valid_queues s; cslift s' (tcb_ptr_to_ctcb_ptr thread) = Some tcb; ep_queue_relation (cslift s') threads (tcb_ptr_to_ctcb_ptr thread) (tcbEPNext_C tcb); thread \<noteq> 0; \<forall>t\<in>set threads. tcb_at' t s \<and> t \<noteq> 0; ko_at' ko thread s; ctcb_relation ko tcb; ksSchedulerAction_' (globals s') = tcb_ptr_to_ctcb_ptr word; x \<noteq> 0; x \<noteq> 1; ksSchedulerAction s = SwitchToThread word; tcb_Ptr x = tcb_ptr_to_ctcb_ptr word; obj_at' (runnable' \<circ> tcbState) word s; tcb_in_cur_domain' word s; \<exists>d v. option_map2 tcbPriority_C (cslift s') (tcb_ptr_to_ctcb_ptr word) = Some v \<and> unat v < Config_H.numPriorities \<and> option_map2 tcbDomain_C (cslift s') (tcb_ptr_to_ctcb_ptr word) = Some d \<and> unat d < numDomains \<and> (StateRelation_C.end_C (ksReadyQueues_' (globals s').[unat (d * 0x100 + v)]) \<noteq> NULL \<longrightarrow> option_map2 tcbPriority_C (cslift s') (head_C (ksReadyQueues_' (globals s').[unat (d * 0x100 + v)])) \<noteq> None \<and> option_map2 tcbDomain_C (cslift s') (head_C (ksReadyQueues_' (globals s').[unat (d * 0x100 + v)])) \<noteq> None)\<rbrakk> \<Longrightarrow> \<exists>d v. option_map2 tcbPriority_C (cslift s') (tcb_ptr_to_ctcb_ptr word) = Some v \<and> unat v \<le> Config_H.numPriorities \<and> option_map2 tcbDomain_C (cslift s') (tcb_ptr_to_ctcb_ptr word) = Some d \<and> unat d < numDomains \<and> (StateRelation_C.end_C (ksReadyQueues_' (globals s').[unat (d * 0x100 + v)]) \<noteq> NULL \<longrightarrow> (\<exists>y. option_map2 tcbPriority_C (cslift s') (head_C (ksReadyQueues_' (globals s').[unat (d * 0x100 + v)])) = Some y) \<and> (\<exists>y. option_map2 tcbDomain_C (cslift s') (head_C (ksReadyQueues_' (globals s').[unat (d * 0x100 + v)])) = Some y))
 4. \<And>s s' tcb ko. \<lbrakk>(s, s') \<in> rf_sr; valid_objs' s; thread_' s' = tcb_ptr_to_ctcb_ptr thread; Invariants_H.valid_queues s; cslift s' (tcb_ptr_to_ctcb_ptr thread) = Some tcb; ep_queue_relation (cslift s') threads (tcb_ptr_to_ctcb_ptr thread) (tcbEPNext_C tcb); thread \<noteq> 0; \<forall>t\<in>set threads. tcb_at' t s \<and> t \<noteq> 0; sch_act_wf (ksSchedulerAction s) s; ko_at' ko thread s; ctcb_relation ko tcb\<rbrakk> \<Longrightarrow> (\<exists>t. option_map2 tcbEPNext_C (cslift t) = option_map2 tcbEPNext_C (cslift s') \<and> option_map2 tcbEPPrev_C (cslift t) = option_map2 tcbEPPrev_C (cslift s') \<and> option_map2 tcbPriority_C (cslift t) = option_map2 tcbPriority_C (cslift s') \<and> option_map2 tcbDomain_C (cslift t) = option_map2 tcbDomain_C (cslift s') \<and> ksReadyQueues_' (globals t) = ksReadyQueues_' (globals s')) \<longrightarrow> (\<exists>d v. option_map2 tcbPriority_C (cslift s') (tcb_ptr_to_ctcb_ptr thread) = Some v \<and> unat v \<le> Config_H.numPriorities \<and> option_map2 tcbDomain_C (cslift s') (tcb_ptr_to_ctcb_ptr thread) = Some d \<and> unat d < numDomains \<and> (StateRelation_C.end_C (ksReadyQueues_' (globals s').[unat (d * 0x100 + v)]) \<noteq> NULL \<longrightarrow> (\<exists>y. option_map2 tcbPriority_C (cslift s') (head_C (ksReadyQueues_' (globals s').[unat (d * 0x100 + v)])) = Some y) \<and> (\<exists>y. option_map2 tcbDomain_C (cslift s') (head_C (ksReadyQueues_' (globals s').[unat (d * 0x100 + v)])) = Some y))) \<and> (\<forall>t. option_map2 tcbEPNext_C (cslift t) = option_map2 tcbEPNext_C (cslift s') \<and> option_map2 tcbEPPrev_C (cslift t) = option_map2 tcbEPPrev_C (cslift s') \<and> option_map2 tcbPriority_C (cslift t) = option_map2 tcbPriority_C (cslift s') \<and> option_map2 tcbDomain_C (cslift t) = option_map2 tcbDomain_C (cslift s') \<longrightarrow> t \<Turnstile>\<^sub>c tcb_ptr_to_ctcb_ptr thread \<longrightarrow> (\<exists>p. ep_queue_relation (cslift t) threads p (h_val (hrs_mem (t_hrs_' (globals t))) (PTR(tcb_C ptr) &(tcb_ptr_to_ctcb_ptr thread\<rightarrow>[''tcbEPNext_C'']))))) proof (prove)
goal (3 subgoals):
 1. \<And>s s' tcb ko x word. \<lbrakk>(s, s') \<in> rf_sr; valid_objs' s; thread_' s' = tcb_ptr_to_ctcb_ptr thread; Invariants_H.valid_queues s; cslift s' (tcb_ptr_to_ctcb_ptr thread) = Some tcb; ep_queue_relation (cslift s') threads (tcb_ptr_to_ctcb_ptr thread) (tcbEPNext_C tcb); thread \<noteq> 0; \<forall>t\<in>set threads. tcb_at' t s \<and> t \<noteq> 0; ko_at' ko thread s; ctcb_relation ko tcb; ksSchedulerAction_' (globals s') = tcb_ptr_to_ctcb_ptr word; x \<noteq> 0; x \<noteq> 1; ksSchedulerAction s = SwitchToThread word; tcb_Ptr x = tcb_ptr_to_ctcb_ptr word; obj_at' (runnable' \<circ> tcbState) word s; tcb_in_cur_domain' word s\<rbrakk> \<Longrightarrow> valid_objs' s
 2. \<And>s s' tcb ko x word. \<lbrakk>(s, s') \<in> rf_sr; valid_objs' s; thread_' s' = tcb_ptr_to_ctcb_ptr thread; Invariants_H.valid_queues s; cslift s' (tcb_ptr_to_ctcb_ptr thread) = Some tcb; ep_queue_relation (cslift s') threads (tcb_ptr_to_ctcb_ptr thread) (tcbEPNext_C tcb); thread \<noteq> 0; \<forall>t\<in>set threads. tcb_at' t s \<and> t \<noteq> 0; ko_at' ko thread s; ctcb_relation ko tcb; ksSchedulerAction_' (globals s') = tcb_ptr_to_ctcb_ptr word; x \<noteq> 0; x \<noteq> 1; ksSchedulerAction s = SwitchToThread word; tcb_Ptr x = tcb_ptr_to_ctcb_ptr word; obj_at' (runnable' \<circ> tcbState) word s; tcb_in_cur_domain' word s; \<exists>d v. option_map2 tcbPriority_C (cslift s') (tcb_ptr_to_ctcb_ptr word) = Some v \<and> unat v < Config_H.numPriorities \<and> option_map2 tcbDomain_C (cslift s') (tcb_ptr_to_ctcb_ptr word) = Some d \<and> unat d < numDomains \<and> (StateRelation_C.end_C (ksReadyQueues_' (globals s').[unat (d * 0x100 + v)]) \<noteq> NULL \<longrightarrow> option_map2 tcbPriority_C (cslift s') (head_C (ksReadyQueues_' (globals s').[unat (d * 0x100 + v)])) \<noteq> None \<and> option_map2 tcbDomain_C (cslift s') (head_C (ksReadyQueues_' (globals s').[unat (d * 0x100 + v)])) \<noteq> None)\<rbrakk> \<Longrightarrow> \<exists>d v. option_map2 tcbPriority_C (cslift s') (tcb_ptr_to_ctcb_ptr word) = Some v \<and> unat v \<le> Config_H.numPriorities \<and> option_map2 tcbDomain_C (cslift s') (tcb_ptr_to_ctcb_ptr word) = Some d \<and> unat d < numDomains \<and> (StateRelation_C.end_C (ksReadyQueues_' (globals s').[unat (d * 0x100 + v)]) \<noteq> NULL \<longrightarrow> (\<exists>y. option_map2 tcbPriority_C (cslift s') (head_C (ksReadyQueues_' (globals s').[unat (d * 0x100 + v)])) = Some y) \<and> (\<exists>y. option_map2 tcbDomain_C (cslift s') (head_C (ksReadyQueues_' (globals s').[unat (d * 0x100 + v)])) = Some y))
 3. \<And>s s' tcb ko. \<lbrakk>(s, s') \<in> rf_sr; valid_objs' s; thread_' s' = tcb_ptr_to_ctcb_ptr thread; Invariants_H.valid_queues s; cslift s' (tcb_ptr_to_ctcb_ptr thread) = Some tcb; ep_queue_relation (cslift s') threads (tcb_ptr_to_ctcb_ptr thread) (tcbEPNext_C tcb); thread \<noteq> 0; \<forall>t\<in>set threads. tcb_at' t s \<and> t \<noteq> 0; sch_act_wf (ksSchedulerAction s) s; ko_at' ko thread s; ctcb_relation ko tcb\<rbrakk> \<Longrightarrow> (\<exists>t. option_map2 tcbEPNext_C (cslift t) = option_map2 tcbEPNext_C (cslift s') \<and> option_map2 tcbEPPrev_C (cslift t) = option_map2 tcbEPPrev_C (cslift s') \<and> option_map2 tcbPriority_C (cslift t) = option_map2 tcbPriority_C (cslift s') \<and> option_map2 tcbDomain_C (cslift t) = option_map2 tcbDomain_C (cslift s') \<and> ksReadyQueues_' (globals t) = ksReadyQueues_' (globals s')) \<longrightarrow> (\<exists>d v. option_map2 tcbPriority_C (cslift s') (tcb_ptr_to_ctcb_ptr thread) = Some v \<and> unat v \<le> Config_H.numPriorities \<and> option_map2 tcbDomain_C (cslift s') (tcb_ptr_to_ctcb_ptr thread) = Some d \<and> unat d < numDomains \<and> (StateRelation_C.end_C (ksReadyQueues_' (globals s').[unat (d * 0x100 + v)]) \<noteq> NULL \<longrightarrow> (\<exists>y. option_map2 tcbPriority_C (cslift s') (head_C (ksReadyQueues_' (globals s').[unat (d * 0x100 + v)])) = Some y) \<and> (\<exists>y. option_map2 tcbDomain_C (cslift s') (head_C (ksReadyQueues_' (globals s').[unat (d * 0x100 + v)])) = Some y))) \<and> (\<forall>t. option_map2 tcbEPNext_C (cslift t) = option_map2 tcbEPNext_C (cslift s') \<and> option_map2 tcbEPPrev_C (cslift t) = option_map2 tcbEPPrev_C (cslift s') \<and> option_map2 tcbPriority_C (cslift t) = option_map2 tcbPriority_C (cslift s') \<and> option_map2 tcbDomain_C (cslift t) = option_map2 tcbDomain_C (cslift s') \<longrightarrow> t \<Turnstile>\<^sub>c tcb_ptr_to_ctcb_ptr thread \<longrightarrow> (\<exists>p. ep_queue_relation (cslift t) threads p (h_val (hrs_mem (t_hrs_' (globals t))) (PTR(tcb_C ptr) &(tcb_ptr_to_ctcb_ptr thread\<rightarrow>[''tcbEPNext_C'']))))) proof (prove)
goal (2 subgoals):
 1. \<And>s s' tcb ko x word. \<lbrakk>(s, s') \<in> rf_sr; valid_objs' s; thread_' s' = tcb_ptr_to_ctcb_ptr thread; Invariants_H.valid_queues s; cslift s' (tcb_ptr_to_ctcb_ptr thread) = Some tcb; ep_queue_relation (cslift s') threads (tcb_ptr_to_ctcb_ptr thread) (tcbEPNext_C tcb); thread \<noteq> 0; \<forall>t\<in>set threads. tcb_at' t s \<and> t \<noteq> 0; ko_at' ko thread s; ctcb_relation ko tcb; ksSchedulerAction_' (globals s') = tcb_ptr_to_ctcb_ptr word; x \<noteq> 0; x \<noteq> 1; ksSchedulerAction s = SwitchToThread word; tcb_Ptr x = tcb_ptr_to_ctcb_ptr word; obj_at' (runnable' \<circ> tcbState) word s; tcb_in_cur_domain' word s; \<exists>d v. option_map2 tcbPriority_C (cslift s') (tcb_ptr_to_ctcb_ptr word) = Some v \<and> unat v < Config_H.numPriorities \<and> option_map2 tcbDomain_C (cslift s') (tcb_ptr_to_ctcb_ptr word) = Some d \<and> unat d < numDomains \<and> (StateRelation_C.end_C (ksReadyQueues_' (globals s').[unat (d * 0x100 + v)]) \<noteq> NULL \<longrightarrow> option_map2 tcbPriority_C (cslift s') (head_C (ksReadyQueues_' (globals s').[unat (d * 0x100 + v)])) \<noteq> None \<and> option_map2 tcbDomain_C (cslift s') (head_C (ksReadyQueues_' (globals s').[unat (d * 0x100 + v)])) \<noteq> None)\<rbrakk> \<Longrightarrow> \<exists>d v. option_map2 tcbPriority_C (cslift s') (tcb_ptr_to_ctcb_ptr word) = Some v \<and> unat v \<le> Config_H.numPriorities \<and> option_map2 tcbDomain_C (cslift s') (tcb_ptr_to_ctcb_ptr word) = Some d \<and> unat d < numDomains \<and> (StateRelation_C.end_C (ksReadyQueues_' (globals s').[unat (d * 0x100 + v)]) \<noteq> NULL \<longrightarrow> (\<exists>y. option_map2 tcbPriority_C (cslift s') (head_C (ksReadyQueues_' (globals s').[unat (d * 0x100 + v)])) = Some y) \<and> (\<exists>y. option_map2 tcbDomain_C (cslift s') (head_C (ksReadyQueues_' (globals s').[unat (d * 0x100 + v)])) = Some y))
 2. \<And>s s' tcb ko. \<lbrakk>(s, s') \<in> rf_sr; valid_objs' s; thread_' s' = tcb_ptr_to_ctcb_ptr thread; Invariants_H.valid_queues s; cslift s' (tcb_ptr_to_ctcb_ptr thread) = Some tcb; ep_queue_relation (cslift s') threads (tcb_ptr_to_ctcb_ptr thread) (tcbEPNext_C tcb); thread \<noteq> 0; \<forall>t\<in>set threads. tcb_at' t s \<and> t \<noteq> 0; sch_act_wf (ksSchedulerAction s) s; ko_at' ko thread s; ctcb_relation ko tcb\<rbrakk> \<Longrightarrow> (\<exists>t. option_map2 tcbEPNext_C (cslift t) = option_map2 tcbEPNext_C (cslift s') \<and> option_map2 tcbEPPrev_C (cslift t) = option_map2 tcbEPPrev_C (cslift s') \<and> option_map2 tcbPriority_C (cslift t) = option_map2 tcbPriority_C (cslift s') \<and> option_map2 tcbDomain_C (cslift t) = option_map2 tcbDomain_C (cslift s') \<and> ksReadyQueues_' (globals t) = ksReadyQueues_' (globals s')) \<longrightarrow> (\<exists>d v. option_map2 tcbPriority_C (cslift s') (tcb_ptr_to_ctcb_ptr thread) = Some v \<and> unat v \<le> Config_H.numPriorities \<and> option_map2 tcbDomain_C (cslift s') (tcb_ptr_to_ctcb_ptr thread) = Some d \<and> unat d < numDomains \<and> (StateRelation_C.end_C (ksReadyQueues_' (globals s').[unat (d * 0x100 + v)]) \<noteq> NULL \<longrightarrow> (\<exists>y. option_map2 tcbPriority_C (cslift s') (head_C (ksReadyQueues_' (globals s').[unat (d * 0x100 + v)])) = Some y) \<and> (\<exists>y. option_map2 tcbDomain_C (cslift s') (head_C (ksReadyQueues_' (globals s').[unat (d * 0x100 + v)])) = Some y))) \<and> (\<forall>t. option_map2 tcbEPNext_C (cslift t) = option_map2 tcbEPNext_C (cslift s') \<and> option_map2 tcbEPPrev_C (cslift t) = option_map2 tcbEPPrev_C (cslift s') \<and> option_map2 tcbPriority_C (cslift t) = option_map2 tcbPriority_C (cslift s') \<and> option_map2 tcbDomain_C (cslift t) = option_map2 tcbDomain_C (cslift s') \<longrightarrow> t \<Turnstile>\<^sub>c tcb_ptr_to_ctcb_ptr thread \<longrightarrow> (\<exists>p. ep_queue_relation (cslift t) threads p (h_val (hrs_mem (t_hrs_' (globals t))) (PTR(tcb_C ptr) &(tcb_ptr_to_ctcb_ptr thread\<rightarrow>[''tcbEPNext_C'']))))) proof (prove)
goal (1 subgoal):
 1. \<And>s s' tcb ko. \<lbrakk>(s, s') \<in> rf_sr; valid_objs' s; thread_' s' = tcb_ptr_to_ctcb_ptr thread; Invariants_H.valid_queues s; cslift s' (tcb_ptr_to_ctcb_ptr thread) = Some tcb; ep_queue_relation (cslift s') threads (tcb_ptr_to_ctcb_ptr thread) (tcbEPNext_C tcb); thread \<noteq> 0; \<forall>t\<in>set threads. tcb_at' t s \<and> t \<noteq> 0; sch_act_wf (ksSchedulerAction s) s; ko_at' ko thread s; ctcb_relation ko tcb\<rbrakk> \<Longrightarrow> (\<exists>t. option_map2 tcbEPNext_C (cslift t) = option_map2 tcbEPNext_C (cslift s') \<and> option_map2 tcbEPPrev_C (cslift t) = option_map2 tcbEPPrev_C (cslift s') \<and> option_map2 tcbPriority_C (cslift t) = option_map2 tcbPriority_C (cslift s') \<and> option_map2 tcbDomain_C (cslift t) = option_map2 tcbDomain_C (cslift s') \<and> ksReadyQueues_' (globals t) = ksReadyQueues_' (globals s')) \<longrightarrow> (\<exists>d v. option_map2 tcbPriority_C (cslift s') (tcb_ptr_to_ctcb_ptr thread) = Some v \<and> unat v \<le> Config_H.numPriorities \<and> option_map2 tcbDomain_C (cslift s') (tcb_ptr_to_ctcb_ptr thread) = Some d \<and> unat d < numDomains \<and> (StateRelation_C.end_C (ksReadyQueues_' (globals s').[unat (d * 0x100 + v)]) \<noteq> NULL \<longrightarrow> (\<exists>y. option_map2 tcbPriority_C (cslift s') (head_C (ksReadyQueues_' (globals s').[unat (d * 0x100 + v)])) = Some y) \<and> (\<exists>y. option_map2 tcbDomain_C (cslift s') (head_C (ksReadyQueues_' (globals s').[unat (d * 0x100 + v)])) = Some y))) \<and> (\<forall>t. option_map2 tcbEPNext_C (cslift t) = option_map2 tcbEPNext_C (cslift s') \<and> option_map2 tcbEPPrev_C (cslift t) = option_map2 tcbEPPrev_C (cslift s') \<and> option_map2 tcbPriority_C (cslift t) = option_map2 tcbPriority_C (cslift s') \<and> option_map2 tcbDomain_C (cslift t) = option_map2 tcbDomain_C (cslift s') \<longrightarrow> t \<Turnstile>\<^sub>c tcb_ptr_to_ctcb_ptr thread \<longrightarrow> (\<exists>p. ep_queue_relation (cslift t) threads p (h_val (hrs_mem (t_hrs_' (globals t))) (PTR(tcb_C ptr) &(tcb_ptr_to_ctcb_ptr thread\<rightarrow>[''tcbEPNext_C'']))))) proof (prove)
goal (1 subgoal):
 1. \<And>s s' tcb ko t. \<lbrakk>(s, s') \<in> rf_sr; valid_objs' s; thread_' s' = tcb_ptr_to_ctcb_ptr thread; Invariants_H.valid_queues s; cslift s' (tcb_ptr_to_ctcb_ptr thread) = Some tcb; ep_queue_relation (cslift s') threads (tcb_ptr_to_ctcb_ptr thread) (tcbEPNext_C tcb); thread \<noteq> 0; \<forall>t\<in>set threads. tcb_at' t s \<and> t \<noteq> 0; sch_act_wf (ksSchedulerAction s) s; ko_at' ko thread s; ctcb_relation ko tcb; option_map2 tcbEPNext_C (cslift t) = option_map2 tcbEPNext_C (cslift s'); option_map2 tcbEPPrev_C (cslift t) = option_map2 tcbEPPrev_C (cslift s'); option_map2 tcbPriority_C (cslift t) = option_map2 tcbPriority_C (cslift s'); option_map2 tcbDomain_C (cslift t) = option_map2 tcbDomain_C (cslift s'); ksReadyQueues_' (globals t) = ksReadyQueues_' (globals s')\<rbrakk> \<Longrightarrow> (\<exists>d v. option_map2 tcbPriority_C (cslift s') (tcb_ptr_to_ctcb_ptr thread) = Some v \<and> unat v \<le> Config_H.numPriorities \<and> option_map2 tcbDomain_C (cslift s') (tcb_ptr_to_ctcb_ptr thread) = Some d \<and> unat d < numDomains \<and> (StateRelation_C.end_C (ksReadyQueues_' (globals s').[unat (d * 0x100 + v)]) \<noteq> NULL \<longrightarrow> (\<exists>y. option_map2 tcbPriority_C (cslift s') (head_C (ksReadyQueues_' (globals s').[unat (d * 0x100 + v)])) = Some y) \<and> (\<exists>y. option_map2 tcbDomain_C (cslift s') (head_C (ksReadyQueues_' (globals s').[unat (d * 0x100 + v)])) = Some y))) \<and> (\<forall>t. option_map2 tcbEPNext_C (cslift t) = option_map2 tcbEPNext_C (cslift s') \<and> option_map2 tcbEPPrev_C (cslift t) = option_map2 tcbEPPrev_C (cslift s') \<and> option_map2 tcbPriority_C (cslift t) = option_map2 tcbPriority_C (cslift s') \<and> option_map2 tcbDomain_C (cslift t) = option_map2 tcbDomain_C (cslift s') \<longrightarrow> t \<Turnstile>\<^sub>c tcb_ptr_to_ctcb_ptr thread \<longrightarrow> (\<exists>p. ep_queue_relation (cslift t) threads p (h_val (hrs_mem (t_hrs_' (globals t))) (PTR(tcb_C ptr) &(tcb_ptr_to_ctcb_ptr thread\<rightarrow>[''tcbEPNext_C'']))))) proof (prove)
goal (2 subgoals):
 1. \<And>s s' tcb ko t. \<lbrakk>(s, s') \<in> rf_sr; valid_objs' s; thread_' s' = tcb_ptr_to_ctcb_ptr thread; Invariants_H.valid_queues s; cslift s' (tcb_ptr_to_ctcb_ptr thread) = Some tcb; ep_queue_relation (cslift s') threads (tcb_ptr_to_ctcb_ptr thread) (tcbEPNext_C tcb); thread \<noteq> 0; \<forall>t\<in>set threads. tcb_at' t s \<and> t \<noteq> 0; sch_act_wf (ksSchedulerAction s) s; ko_at' ko thread s; ctcb_relation ko tcb; option_map2 tcbEPNext_C (cslift t) = option_map2 tcbEPNext_C (cslift s'); option_map2 tcbEPPrev_C (cslift t) = option_map2 tcbEPPrev_C (cslift s'); option_map2 tcbPriority_C (cslift t) = option_map2 tcbPriority_C (cslift s'); option_map2 tcbDomain_C (cslift t) = option_map2 tcbDomain_C (cslift s'); ksReadyQueues_' (globals t) = ksReadyQueues_' (globals s')\<rbrakk> \<Longrightarrow> \<exists>d v. option_map2 tcbPriority_C (cslift s') (tcb_ptr_to_ctcb_ptr thread) = Some v \<and> unat v \<le> Config_H.numPriorities \<and> option_map2 tcbDomain_C (cslift s') (tcb_ptr_to_ctcb_ptr thread) = Some d \<and> unat d < numDomains \<and> (StateRelation_C.end_C (ksReadyQueues_' (globals s').[unat (d * 0x100 + v)]) \<noteq> NULL \<longrightarrow> (\<exists>y. option_map2 tcbPriority_C (cslift s') (head_C (ksReadyQueues_' (globals s').[unat (d * 0x100 + v)])) = Some y) \<and> (\<exists>y. option_map2 tcbDomain_C (cslift s') (head_C (ksReadyQueues_' (globals s').[unat (d * 0x100 + v)])) = Some y))
 2. \<And>s s' tcb ko t. \<lbrakk>(s, s') \<in> rf_sr; valid_objs' s; thread_' s' = tcb_ptr_to_ctcb_ptr thread; Invariants_H.valid_queues s; cslift s' (tcb_ptr_to_ctcb_ptr thread) = Some tcb; ep_queue_relation (cslift s') threads (tcb_ptr_to_ctcb_ptr thread) (tcbEPNext_C tcb); thread \<noteq> 0; \<forall>t\<in>set threads. tcb_at' t s \<and> t \<noteq> 0; sch_act_wf (ksSchedulerAction s) s; ko_at' ko thread s; ctcb_relation ko tcb; option_map2 tcbEPNext_C (cslift t) = option_map2 tcbEPNext_C (cslift s'); option_map2 tcbEPPrev_C (cslift t) = option_map2 tcbEPPrev_C (cslift s'); option_map2 tcbPriority_C (cslift t) = option_map2 tcbPriority_C (cslift s'); option_map2 tcbDomain_C (cslift t) = option_map2 tcbDomain_C (cslift s'); ksReadyQueues_' (globals t) = ksReadyQueues_' (globals s')\<rbrakk> \<Longrightarrow> \<forall>t. option_map2 tcbEPNext_C (cslift t) = option_map2 tcbEPNext_C (cslift s') \<and> option_map2 tcbEPPrev_C (cslift t) = option_map2 tcbEPPrev_C (cslift s') \<and> option_map2 tcbPriority_C (cslift t) = option_map2 tcbPriority_C (cslift s') \<and> option_map2 tcbDomain_C (cslift t) = option_map2 tcbDomain_C (cslift s') \<longrightarrow> t \<Turnstile>\<^sub>c tcb_ptr_to_ctcb_ptr thread \<longrightarrow> (\<exists>p. ep_queue_relation (cslift t) threads p (h_val (hrs_mem (t_hrs_' (globals t))) (PTR(tcb_C ptr) &(tcb_ptr_to_ctcb_ptr thread\<rightarrow>[''tcbEPNext_C''])))) proof (prove)
goal (2 subgoals):
 1. \<And>s s' tcb ko t. \<lbrakk>(s, s') \<in> rf_sr; valid_objs' s; thread_' s' = tcb_ptr_to_ctcb_ptr thread; Invariants_H.valid_queues s; cslift s' (tcb_ptr_to_ctcb_ptr thread) = Some tcb; ep_queue_relation (cslift s') threads (tcb_ptr_to_ctcb_ptr thread) (tcbEPNext_C tcb); thread \<noteq> 0; \<forall>t\<in>set threads. tcb_at' t s \<and> t \<noteq> 0; sch_act_wf (ksSchedulerAction s) s; ko_at' ko thread s; ctcb_relation ko tcb; option_map2 tcbEPNext_C (cslift t) = option_map2 tcbEPNext_C (cslift s'); option_map2 tcbEPPrev_C (cslift t) = option_map2 tcbEPPrev_C (cslift s'); option_map2 tcbPriority_C (cslift t) = option_map2 tcbPriority_C (cslift s'); option_map2 tcbDomain_C (cslift t) = option_map2 tcbDomain_C (cslift s'); ksReadyQueues_' (globals t) = ksReadyQueues_' (globals s'); \<exists>d v. option_map2 tcbPriority_C (cslift s') (tcb_ptr_to_ctcb_ptr thread) = Some v \<and> unat v < Config_H.numPriorities \<and> option_map2 tcbDomain_C (cslift s') (tcb_ptr_to_ctcb_ptr thread) = Some d \<and> unat d < numDomains \<and> (StateRelation_C.end_C (ksReadyQueues_' (globals s').[unat (d * 0x100 + v)]) \<noteq> NULL \<longrightarrow> option_map2 tcbPriority_C (cslift s') (head_C (ksReadyQueues_' (globals s').[unat (d * 0x100 + v)])) \<noteq> None \<and> option_map2 tcbDomain_C (cslift s') (head_C (ksReadyQueues_' (globals s').[unat (d * 0x100 + v)])) \<noteq> None)\<rbrakk> \<Longrightarrow> \<exists>d v. option_map2 tcbPriority_C (cslift s') (tcb_ptr_to_ctcb_ptr thread) = Some v \<and> unat v \<le> Config_H.numPriorities \<and> option_map2 tcbDomain_C (cslift s') (tcb_ptr_to_ctcb_ptr thread) = Some d \<and> unat d < numDomains \<and> (StateRelation_C.end_C (ksReadyQueues_' (globals s').[unat (d * 0x100 + v)]) \<noteq> NULL \<longrightarrow> (\<exists>y. option_map2 tcbPriority_C (cslift s') (head_C (ksReadyQueues_' (globals s').[unat (d * 0x100 + v)])) = Some y) \<and> (\<exists>y. option_map2 tcbDomain_C (cslift s') (head_C (ksReadyQueues_' (globals s').[unat (d * 0x100 + v)])) = Some y))
 2. \<And>s s' tcb ko t. \<lbrakk>(s, s') \<in> rf_sr; valid_objs' s; thread_' s' = tcb_ptr_to_ctcb_ptr thread; Invariants_H.valid_queues s; cslift s' (tcb_ptr_to_ctcb_ptr thread) = Some tcb; ep_queue_relation (cslift s') threads (tcb_ptr_to_ctcb_ptr thread) (tcbEPNext_C tcb); thread \<noteq> 0; \<forall>t\<in>set threads. tcb_at' t s \<and> t \<noteq> 0; sch_act_wf (ksSchedulerAction s) s; ko_at' ko thread s; ctcb_relation ko tcb; option_map2 tcbEPNext_C (cslift t) = option_map2 tcbEPNext_C (cslift s'); option_map2 tcbEPPrev_C (cslift t) = option_map2 tcbEPPrev_C (cslift s'); option_map2 tcbPriority_C (cslift t) = option_map2 tcbPriority_C (cslift s'); option_map2 tcbDomain_C (cslift t) = option_map2 tcbDomain_C (cslift s'); ksReadyQueues_' (globals t) = ksReadyQueues_' (globals s')\<rbrakk> \<Longrightarrow> \<forall>t. option_map2 tcbEPNext_C (cslift t) = option_map2 tcbEPNext_C (cslift s') \<and> option_map2 tcbEPPrev_C (cslift t) = option_map2 tcbEPPrev_C (cslift s') \<and> option_map2 tcbPriority_C (cslift t) = option_map2 tcbPriority_C (cslift s') \<and> option_map2 tcbDomain_C (cslift t) = option_map2 tcbDomain_C (cslift s') \<longrightarrow> t \<Turnstile>\<^sub>c tcb_ptr_to_ctcb_ptr thread \<longrightarrow> (\<exists>p. ep_queue_relation (cslift t) threads p (h_val (hrs_mem (t_hrs_' (globals t))) (PTR(tcb_C ptr) &(tcb_ptr_to_ctcb_ptr thread\<rightarrow>[''tcbEPNext_C''])))) proof (prove)
goal (1 subgoal):
 1. \<And>s s' tcb ko t. \<lbrakk>(s, s') \<in> rf_sr; valid_objs' s; thread_' s' = tcb_ptr_to_ctcb_ptr thread; Invariants_H.valid_queues s; cslift s' (tcb_ptr_to_ctcb_ptr thread) = Some tcb; ep_queue_relation (cslift s') threads (tcb_ptr_to_ctcb_ptr thread) (tcbEPNext_C tcb); thread \<noteq> 0; \<forall>t\<in>set threads. tcb_at' t s \<and> t \<noteq> 0; sch_act_wf (ksSchedulerAction s) s; ko_at' ko thread s; ctcb_relation ko tcb; option_map2 tcbEPNext_C (cslift t) = option_map2 tcbEPNext_C (cslift s'); option_map2 tcbEPPrev_C (cslift t) = option_map2 tcbEPPrev_C (cslift s'); option_map2 tcbPriority_C (cslift t) = option_map2 tcbPriority_C (cslift s'); option_map2 tcbDomain_C (cslift t) = option_map2 tcbDomain_C (cslift s'); ksReadyQueues_' (globals t) = ksReadyQueues_' (globals s')\<rbrakk> \<Longrightarrow> \<forall>t. option_map2 tcbEPNext_C (cslift t) = option_map2 tcbEPNext_C (cslift s') \<and> option_map2 tcbEPPrev_C (cslift t) = option_map2 tcbEPPrev_C (cslift s') \<and> option_map2 tcbPriority_C (cslift t) = option_map2 tcbPriority_C (cslift s') \<and> option_map2 tcbDomain_C (cslift t) = option_map2 tcbDomain_C (cslift s') \<longrightarrow> t \<Turnstile>\<^sub>c tcb_ptr_to_ctcb_ptr thread \<longrightarrow> (\<exists>p. ep_queue_relation (cslift t) threads p (h_val (hrs_mem (t_hrs_' (globals t))) (PTR(tcb_C ptr) &(tcb_ptr_to_ctcb_ptr thread\<rightarrow>[''tcbEPNext_C''])))) proof (prove)
goal (1 subgoal):
 1. \<And>s s' tcb ko t ta. \<lbrakk>(s, s') \<in> rf_sr; valid_objs' s; thread_' s' = tcb_ptr_to_ctcb_ptr thread; Invariants_H.valid_queues s; cslift s' (tcb_ptr_to_ctcb_ptr thread) = Some tcb; ep_queue_relation (cslift s') threads (tcb_ptr_to_ctcb_ptr thread) (tcbEPNext_C tcb); thread \<noteq> 0; \<forall>t\<in>set threads. tcb_at' t s \<and> t \<noteq> 0; sch_act_wf (ksSchedulerAction s) s; ko_at' ko thread s; ctcb_relation ko tcb; option_map2 tcbEPNext_C (cslift t) = option_map2 tcbEPNext_C (cslift s'); option_map2 tcbEPPrev_C (cslift t) = option_map2 tcbEPPrev_C (cslift s'); option_map2 tcbPriority_C (cslift t) = option_map2 tcbPriority_C (cslift s'); option_map2 tcbDomain_C (cslift t) = option_map2 tcbDomain_C (cslift s'); ksReadyQueues_' (globals t) = ksReadyQueues_' (globals s'); option_map2 tcbEPNext_C (cslift ta) = option_map2 tcbEPNext_C (cslift s'); option_map2 tcbEPPrev_C (cslift ta) = option_map2 tcbEPPrev_C (cslift s'); option_map2 tcbPriority_C (cslift ta) = option_map2 tcbPriority_C (cslift s'); option_map2 tcbDomain_C (cslift ta) = option_map2 tcbDomain_C (cslift s'); ta \<Turnstile>\<^sub>c tcb_ptr_to_ctcb_ptr thread\<rbrakk> \<Longrightarrow> \<exists>p. ep_queue_relation (cslift ta) threads p (h_val (hrs_mem (t_hrs_' (globals ta))) (PTR(tcb_C ptr) &(tcb_ptr_to_ctcb_ptr thread\<rightarrow>[''tcbEPNext_C'']))) proof (prove)
goal (1 subgoal):
 1. \<And>s s' tcb ko t ta. \<lbrakk>(s, s') \<in> rf_sr; valid_objs' s; thread_' s' = tcb_ptr_to_ctcb_ptr thread; Invariants_H.valid_queues s; cslift s' (tcb_ptr_to_ctcb_ptr thread) = Some tcb; ep_queue_relation (cslift s') threads (tcb_ptr_to_ctcb_ptr thread) (tcbEPNext_C tcb); thread \<noteq> 0; \<forall>t\<in>set threads. tcb_at' t s \<and> t \<noteq> 0; sch_act_wf (ksSchedulerAction s) s; ko_at' ko thread s; ctcb_relation ko tcb; option_map2 tcbEPNext_C (cslift t) = option_map2 tcbEPNext_C (cslift s'); option_map2 tcbEPPrev_C (cslift t) = option_map2 tcbEPPrev_C (cslift s'); option_map2 tcbPriority_C (cslift t) = option_map2 tcbPriority_C (cslift s'); option_map2 tcbDomain_C (cslift t) = option_map2 tcbDomain_C (cslift s'); ksReadyQueues_' (globals t) = ksReadyQueues_' (globals s'); option_map2 tcbEPNext_C (cslift ta) = option_map2 tcbEPNext_C (cslift s'); option_map2 tcbEPPrev_C (cslift ta) = option_map2 tcbEPPrev_C (cslift s'); option_map2 tcbPriority_C (cslift ta) = option_map2 tcbPriority_C (cslift s'); option_map2 tcbDomain_C (cslift ta) = option_map2 tcbDomain_C (cslift s'); ta \<Turnstile>\<^sub>c tcb_ptr_to_ctcb_ptr thread\<rbrakk> \<Longrightarrow> \<exists>p. ep_queue_relation (cslift s') threads p (h_val (hrs_mem (t_hrs_' (globals ta))) (PTR(tcb_C ptr) &(tcb_ptr_to_ctcb_ptr thread\<rightarrow>[''tcbEPNext_C'']))) proof (prove)
goal (1 subgoal):
 1. \<And>s s' tcb ko t ta. \<lbrakk>(s, s') \<in> rf_sr; valid_objs' s; thread_' s' = tcb_ptr_to_ctcb_ptr thread; Invariants_H.valid_queues s; cslift s' (tcb_ptr_to_ctcb_ptr thread) = Some tcb; ep_queue_relation (cslift s') threads (tcb_ptr_to_ctcb_ptr thread) (tcbEPNext_C tcb); thread \<noteq> 0; \<forall>t\<in>set threads. tcb_at' t s \<and> t \<noteq> 0; sch_act_wf (ksSchedulerAction s) s; ko_at' ko thread s; ctcb_relation ko tcb; ksReadyQueues_' (globals t) = ksReadyQueues_' (globals s'); ta \<Turnstile>\<^sub>c tcb_ptr_to_ctcb_ptr thread; option_map2 tcbEPNext_C (cslift t) (tcb_ptr_to_ctcb_ptr thread) = option_map2 tcbEPNext_C (cslift s') (tcb_ptr_to_ctcb_ptr thread); option_map2 tcbEPPrev_C (cslift t) (tcb_ptr_to_ctcb_ptr thread) = option_map2 tcbEPPrev_C (cslift s') (tcb_ptr_to_ctcb_ptr thread); option_map2 tcbPriority_C (cslift t) (tcb_ptr_to_ctcb_ptr thread) = option_map2 tcbPriority_C (cslift s') (tcb_ptr_to_ctcb_ptr thread); option_map2 tcbDomain_C (cslift t) (tcb_ptr_to_ctcb_ptr thread) = option_map2 tcbDomain_C (cslift s') (tcb_ptr_to_ctcb_ptr thread); option_map2 tcbEPNext_C (cslift ta) (tcb_ptr_to_ctcb_ptr thread) = option_map2 tcbEPNext_C (cslift s') (tcb_ptr_to_ctcb_ptr thread); option_map2 tcbEPPrev_C (cslift ta) (tcb_ptr_to_ctcb_ptr thread) = option_map2 tcbEPPrev_C (cslift s') (tcb_ptr_to_ctcb_ptr thread); option_map2 tcbPriority_C (cslift ta) (tcb_ptr_to_ctcb_ptr thread) = option_map2 tcbPriority_C (cslift s') (tcb_ptr_to_ctcb_ptr thread); option_map2 tcbDomain_C (cslift ta) (tcb_ptr_to_ctcb_ptr thread) = option_map2 tcbDomain_C (cslift s') (tcb_ptr_to_ctcb_ptr thread)\<rbrakk> \<Longrightarrow> \<exists>p. ep_queue_relation (cslift s') threads p (h_val (hrs_mem (t_hrs_' (globals ta))) (PTR(tcb_C ptr) &(tcb_ptr_to_ctcb_ptr thread\<rightarrow>[''tcbEPNext_C'']))) proof (prove)
goal (1 subgoal):
 1. \<And>s s' tcb ko t ta z zd. \<lbrakk>(s, s') \<in> rf_sr; valid_objs' s; thread_' s' = tcb_ptr_to_ctcb_ptr thread; Invariants_H.valid_queues s; cslift s' (tcb_ptr_to_ctcb_ptr thread) = Some tcb; ep_queue_relation (cslift s') threads (tcb_ptr_to_ctcb_ptr thread) (tcbEPNext_C tcb); thread \<noteq> 0; \<forall>t\<in>set threads. tcb_at' t s \<and> t \<noteq> 0; sch_act_wf (ksSchedulerAction s) s; ko_at' ko thread s; ctcb_relation ko tcb; ksReadyQueues_' (globals t) = ksReadyQueues_' (globals s'); tcbEPNext_C z = tcbEPNext_C tcb; tcbEPPrev_C z = tcbEPPrev_C tcb; tcbPriority_C z = tcbPriority_C tcb; cslift t (tcb_ptr_to_ctcb_ptr thread) = Some z; tcbDomain_C z = tcbDomain_C tcb; tcbEPNext_C zd = tcbEPNext_C tcb; tcbEPPrev_C zd = tcbEPPrev_C tcb; tcbPriority_C zd = tcbPriority_C tcb; cslift ta (tcb_ptr_to_ctcb_ptr thread) = Some zd; tcbDomain_C zd = tcbDomain_C tcb\<rbrakk> \<Longrightarrow> \<exists>p. ep_queue_relation (cslift s') threads p (tcbEPNext_C tcb) proof (prove)
goal:
No subgoals! proof (state)
this:
ccorres dc xfdc (\<lambda>s. valid_objs' s \<and> Invariants_H.valid_queues s \<and> (\<forall>t\<in>set (thread # threads). tcb_at' t s \<and> t \<noteq> 0) \<and> sch_act_wf (ksSchedulerAction s) s) {s'. \<exists>p. ep_queue_relation (cslift s') (thread # threads) p (thread_' s')} hs (mapM_x (\<lambda>t. do y <- setThreadState Structures_H.thread_state.Restart t;
tcbSchedEnqueue t
od) (thread # threads)) (While \<lbrace>\<acute>thread \<noteq> NULL\<rbrace> (CALL setThreadState_'proc(\<acute>thread,SCAST(32 signed \<rightarrow> 32) ThreadState_Restart);;
CALL tcbSchedEnqueue_'proc(\<acute>thread);;
Guard C_Guard {s. s \<Turnstile>\<^sub>c thread_' s} (\<acute>thread :== h_val (hrs_mem \<acute>t_hrs) (PTR(tcb_C ptr) &(\<acute>thread\<rightarrow>[''tcbEPNext_C''])))))

goal:
No subgoals!