theory Finalise_C

lemma setThreadState_cslift_spec:
  "\<forall>s. \<Gamma>\<turnstile>\<^bsub>/UNIV\<^esub> \<lbrace>s. s \<Turnstile>\<^sub>c \<acute>tptr \<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> numPriorities
                       \<and> option_map2 tcbDomain_C (cslift s) (tcb_Ptr x) = Some d
                       \<and> unat d < Kernel_Config.numDomains
                       \<and> (end_C (index \<acute>ksReadyQueues (unat (d*0x100 + v))) \<noteq> NULL
                           \<longrightarrow> option_map2 tcbPriority_C (cslift s)
                                   (head_C (index \<acute>ksReadyQueues (unat (d*0x100 + v))))
                                           \<noteq> None
                             \<and> option_map2 tcbDomain_C (cslift s)
                                   (head_C (index \<acute>ksReadyQueues (unat (d*0x100 + v))))
                                           \<noteq> None)))\<rbrace>
          Call setThreadState_'proc
      {s'. option_map2 tcbEPNext_C (cslift s') = option_map2 tcbEPNext_C (cslift s)
           \<and> option_map2 tcbEPPrev_C (cslift s') = option_map2 tcbEPPrev_C (cslift s)
           \<and> option_map2 tcbPriority_C (cslift s') = option_map2 tcbPriority_C (cslift s)
           \<and> option_map2 tcbDomain_C (cslift s') = option_map2 tcbDomain_C (cslift s)
           \<and> ksReadyQueues_' (globals s') = ksReadyQueues_' (globals s)}" apply (rule allI, rule conseqPre) apply vcg_step apply vcg_step apply vcg_step apply vcg_step apply vcg_step apply vcg_step apply vcg_step apply (vcg exspec=tcbSchedEnqueue_cslift_spec) apply (vcg_step+)[2] apply vcg_step apply (vcg exspec=isRunnable_modifies) apply vcg apply vcg_step apply vcg_step apply (vcg_step+)[1] apply vcg apply vcg_step+ apply (clarsimp simp: typ_heap_simps h_t_valid_clift_Some_iff fun_eq_iff option_map2_def) by (simp split: if_split)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<forall>s. \<Gamma>\<turnstile>\<^bsub>/UNIV\<^esub> \<lbrace>s. s \<Turnstile>\<^sub>c \<acute>tptr \<and> (\<forall>x. \<^bsup>s\<^esup>ksSchedulerAction = 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 (\<acute>ksReadyQueues.[unat (d * 0x100 + v)]) \<noteq> NULL \<longrightarrow> option_map2 tcbPriority_C (cslift s) (head_C (\<acute>ksReadyQueues.[unat (d * 0x100 + v)])) \<noteq> None \<and> option_map2 tcbDomain_C (cslift s) (head_C (\<acute>ksReadyQueues.[unat (d * 0x100 + v)])) \<noteq> None)))\<rbrace> Call setThreadState_'proc {s'. option_map2 tcbEPNext_C (cslift s') = option_map2 tcbEPNext_C (cslift s) \<and> option_map2 tcbEPPrev_C (cslift s') = option_map2 tcbEPPrev_C (cslift s) \<and> option_map2 tcbPriority_C (cslift s') = option_map2 tcbPriority_C (cslift s) \<and> option_map2 tcbDomain_C (cslift s') = option_map2 tcbDomain_C (cslift s) \<and> ksReadyQueues_' (globals s') = ksReadyQueues_' (globals s)} proof (prove)
goal (2 subgoals):
 1. \<And>s. \<Gamma>\<turnstile>\<^bsub>/UNIV\<^esub> (?P'2 s) Call setThreadState_'proc {s'. option_map2 tcbEPNext_C (cslift s') = option_map2 tcbEPNext_C (cslift s) \<and> option_map2 tcbEPPrev_C (cslift s') = option_map2 tcbEPPrev_C (cslift s) \<and> option_map2 tcbPriority_C (cslift s') = option_map2 tcbPriority_C (cslift s) \<and> option_map2 tcbDomain_C (cslift s') = option_map2 tcbDomain_C (cslift s) \<and> ksReadyQueues_' (globals s') = ksReadyQueues_' (globals s)}
 2. \<And>s. \<lbrace>s. s \<Turnstile>\<^sub>c \<acute>tptr \<and> (\<forall>x. \<^bsup>s\<^esup>ksSchedulerAction = 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 (\<acute>ksReadyQueues.[unat (d * 0x100 + v)]) \<noteq> NULL \<longrightarrow> option_map2 tcbPriority_C (cslift s) (head_C (\<acute>ksReadyQueues.[unat (d * 0x100 + v)])) \<noteq> None \<and> option_map2 tcbDomain_C (cslift s) (head_C (\<acute>ksReadyQueues.[unat (d * 0x100 + v)])) \<noteq> None)))\<rbrace> \<subseteq> ?P'2 s proof (prove)
goal (2 subgoals):
 1. \<And>s. \<Gamma>\<turnstile>\<^bsub>/UNIV\<^esub> (?P'2 s) TRY
  Guard C_Guard {s. s \<Turnstile>\<^sub>c tptr_' s} (CALL thread_state_ptr_set_tsType_'proc(PTR(thread_state_C) &(\<acute>tptr\<rightarrow>[''tcbState_C'']),UCAST(32 \<rightarrow> 32) \<acute>ts));;
CALL scheduleTCB_'proc(\<acute>tptr)
CATCH SKIP
END {s'. option_map2 tcbEPNext_C (cslift s') = option_map2 tcbEPNext_C (cslift s) \<and> option_map2 tcbEPPrev_C (cslift s') = option_map2 tcbEPPrev_C (cslift s) \<and> option_map2 tcbPriority_C (cslift s') = option_map2 tcbPriority_C (cslift s) \<and> option_map2 tcbDomain_C (cslift s') = option_map2 tcbDomain_C (cslift s) \<and> ksReadyQueues_' (globals s') = ksReadyQueues_' (globals s)}
 2. \<And>s. \<lbrace>s. s \<Turnstile>\<^sub>c \<acute>tptr \<and> (\<forall>x. \<^bsup>s\<^esup>ksSchedulerAction = 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 (\<acute>ksReadyQueues.[unat (d * 0x100 + v)]) \<noteq> NULL \<longrightarrow> option_map2 tcbPriority_C (cslift s) (head_C (\<acute>ksReadyQueues.[unat (d * 0x100 + v)])) \<noteq> None \<and> option_map2 tcbDomain_C (cslift s) (head_C (\<acute>ksReadyQueues.[unat (d * 0x100 + v)])) \<noteq> None)))\<rbrace> \<subseteq> ?P'2 s proof (prove)
goal (3 subgoals):
 1. \<And>s. \<Gamma>\<turnstile>\<^bsub>/UNIV\<^esub> (?R12 s) SKIP {s'. option_map2 tcbEPNext_C (cslift s') = option_map2 tcbEPNext_C (cslift s) \<and> option_map2 tcbEPPrev_C (cslift s') = option_map2 tcbEPPrev_C (cslift s) \<and> option_map2 tcbPriority_C (cslift s') = option_map2 tcbPriority_C (cslift s) \<and> option_map2 tcbDomain_C (cslift s') = option_map2 tcbDomain_C (cslift s) \<and> ksReadyQueues_' (globals s') = ksReadyQueues_' (globals s)}
 2. \<And>s. \<Gamma>\<turnstile>\<^bsub>/UNIV\<^esub> (?P'2 s) Guard C_Guard {s. s \<Turnstile>\<^sub>c tptr_' s} (CALL thread_state_ptr_set_tsType_'proc(PTR(thread_state_C) &(\<acute>tptr\<rightarrow>[''tcbState_C'']),UCAST(32 \<rightarrow> 32) \<acute>ts));;
CALL scheduleTCB_'proc(\<acute>tptr) {s'. option_map2 tcbEPNext_C (cslift s') = option_map2 tcbEPNext_C (cslift s) \<and> option_map2 tcbEPPrev_C (cslift s') = option_map2 tcbEPPrev_C (cslift s) \<and> option_map2 tcbPriority_C (cslift s') = option_map2 tcbPriority_C (cslift s) \<and> option_map2 tcbDomain_C (cslift s') = option_map2 tcbDomain_C (cslift s) \<and> ksReadyQueues_' (globals s') = ksReadyQueues_' (globals s)},(?R12 s)
 3. \<And>s. \<lbrace>s. s \<Turnstile>\<^sub>c \<acute>tptr \<and> (\<forall>x. \<^bsup>s\<^esup>ksSchedulerAction = 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 (\<acute>ksReadyQueues.[unat (d * 0x100 + v)]) \<noteq> NULL \<longrightarrow> option_map2 tcbPriority_C (cslift s) (head_C (\<acute>ksReadyQueues.[unat (d * 0x100 + v)])) \<noteq> None \<and> option_map2 tcbDomain_C (cslift s) (head_C (\<acute>ksReadyQueues.[unat (d * 0x100 + v)])) \<noteq> None)))\<rbrace> \<subseteq> ?P'2 s proof (prove)
goal (2 subgoals):
 1. \<And>s. \<Gamma>\<turnstile>\<^bsub>/UNIV\<^esub> (?P'2 s) Guard C_Guard {s. s \<Turnstile>\<^sub>c tptr_' s} (CALL thread_state_ptr_set_tsType_'proc(PTR(thread_state_C) &(\<acute>tptr\<rightarrow>[''tcbState_C'']),UCAST(32 \<rightarrow> 32) \<acute>ts));;
CALL scheduleTCB_'proc(\<acute>tptr) {s'. option_map2 tcbEPNext_C (cslift s') = option_map2 tcbEPNext_C (cslift s) \<and> option_map2 tcbEPPrev_C (cslift s') = option_map2 tcbEPPrev_C (cslift s) \<and> option_map2 tcbPriority_C (cslift s') = option_map2 tcbPriority_C (cslift s) \<and> option_map2 tcbDomain_C (cslift s') = option_map2 tcbDomain_C (cslift s) \<and> ksReadyQueues_' (globals s') = ksReadyQueues_' (globals s)},{s'. option_map2 tcbEPNext_C (cslift s') = option_map2 tcbEPNext_C (cslift s) \<and> option_map2 tcbEPPrev_C (cslift s') = option_map2 tcbEPPrev_C (cslift s) \<and> option_map2 tcbPriority_C (cslift s') = option_map2 tcbPriority_C (cslift s) \<and> option_map2 tcbDomain_C (cslift s') = option_map2 tcbDomain_C (cslift s) \<and> ksReadyQueues_' (globals s') = ksReadyQueues_' (globals s)}
 2. \<And>s. \<lbrace>s. s \<Turnstile>\<^sub>c \<acute>tptr \<and> (\<forall>x. \<^bsup>s\<^esup>ksSchedulerAction = 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 (\<acute>ksReadyQueues.[unat (d * 0x100 + v)]) \<noteq> NULL \<longrightarrow> option_map2 tcbPriority_C (cslift s) (head_C (\<acute>ksReadyQueues.[unat (d * 0x100 + v)])) \<noteq> None \<and> option_map2 tcbDomain_C (cslift s) (head_C (\<acute>ksReadyQueues.[unat (d * 0x100 + v)])) \<noteq> None)))\<rbrace> \<subseteq> ?P'2 s proof (prove)
goal (3 subgoals):
 1. \<And>s sa. \<Gamma>\<turnstile>\<^bsub>/UNIV\<^esub> (?P'24 s sa) TRY
  \<acute>ret__int :== (if \<acute>tptr = \<acute>ksCurThread then 1 else 0);;
IF \<acute>ret__int \<noteq> 0 THEN
  \<acute>ret__int :== (if \<acute>ksSchedulerAction = tcb_Ptr (SCAST(32 signed \<rightarrow> 32) 0) then 1 else 0)
FI;;
IF \<acute>ret__int \<noteq> 0 THEN
  \<acute>ret__unsigned_long :== CALL isRunnable_'proc(\<acute>tptr);;
\<acute>ret__int :== (if \<not> \<acute>ret__unsigned_long \<noteq> 0 then 1 else 0)
FI;;
IF \<acute>ret__int \<noteq> 0 THEN
  CALL rescheduleRequired_'proc()
FI
CATCH SKIP
END {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)},{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)}
 2. \<And>s. \<Gamma>\<turnstile>\<^bsub>/UNIV\<^esub> (?P'2 s) Guard C_Guard {s. s \<Turnstile>\<^sub>c tptr_' s} (CALL thread_state_ptr_set_tsType_'proc(PTR(thread_state_C) &(\<acute>tptr\<rightarrow>[''tcbState_C'']),UCAST(32 \<rightarrow> 32) \<acute>ts)) {sa. sa \<in> ?P'24 s sa},{s'. option_map2 tcbEPNext_C (cslift s') = option_map2 tcbEPNext_C (cslift s) \<and> option_map2 tcbEPPrev_C (cslift s') = option_map2 tcbEPPrev_C (cslift s) \<and> option_map2 tcbPriority_C (cslift s') = option_map2 tcbPriority_C (cslift s) \<and> option_map2 tcbDomain_C (cslift s') = option_map2 tcbDomain_C (cslift s) \<and> ksReadyQueues_' (globals s') = ksReadyQueues_' (globals s)}
 3. \<And>s. \<lbrace>s. s \<Turnstile>\<^sub>c \<acute>tptr \<and> (\<forall>x. \<^bsup>s\<^esup>ksSchedulerAction = 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 (\<acute>ksReadyQueues.[unat (d * 0x100 + v)]) \<noteq> NULL \<longrightarrow> option_map2 tcbPriority_C (cslift s) (head_C (\<acute>ksReadyQueues.[unat (d * 0x100 + v)])) \<noteq> None \<and> option_map2 tcbDomain_C (cslift s) (head_C (\<acute>ksReadyQueues.[unat (d * 0x100 + v)])) \<noteq> None)))\<rbrace> \<subseteq> ?P'2 s proof (prove)
goal (4 subgoals):
 1. \<And>s sa. \<Gamma>\<turnstile>\<^bsub>/UNIV\<^esub> (?R37 s sa) SKIP {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)},{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)}
 2. \<And>s sa. \<Gamma>\<turnstile>\<^bsub>/UNIV\<^esub> (?P'24 s sa) \<acute>ret__int :== (if \<acute>tptr = \<acute>ksCurThread then 1 else 0);;
IF \<acute>ret__int \<noteq> 0 THEN
  \<acute>ret__int :== (if \<acute>ksSchedulerAction = tcb_Ptr (SCAST(32 signed \<rightarrow> 32) 0) then 1 else 0)
FI;;
IF \<acute>ret__int \<noteq> 0 THEN
  \<acute>ret__unsigned_long :== CALL isRunnable_'proc(\<acute>tptr);;
\<acute>ret__int :== (if \<not> \<acute>ret__unsigned_long \<noteq> 0 then 1 else 0)
FI;;
IF \<acute>ret__int \<noteq> 0 THEN
  CALL rescheduleRequired_'proc()
FI {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)},(?R37 s sa)
 3. \<And>s. \<Gamma>\<turnstile>\<^bsub>/UNIV\<^esub> (?P'2 s) Guard C_Guard {s. s \<Turnstile>\<^sub>c tptr_' s} (CALL thread_state_ptr_set_tsType_'proc(PTR(thread_state_C) &(\<acute>tptr\<rightarrow>[''tcbState_C'']),UCAST(32 \<rightarrow> 32) \<acute>ts)) {sa. sa \<in> ?P'24 s sa},{s'. option_map2 tcbEPNext_C (cslift s') = option_map2 tcbEPNext_C (cslift s) \<and> option_map2 tcbEPPrev_C (cslift s') = option_map2 tcbEPPrev_C (cslift s) \<and> option_map2 tcbPriority_C (cslift s') = option_map2 tcbPriority_C (cslift s) \<and> option_map2 tcbDomain_C (cslift s') = option_map2 tcbDomain_C (cslift s) \<and> ksReadyQueues_' (globals s') = ksReadyQueues_' (globals s)}
 4. \<And>s. \<lbrace>s. s \<Turnstile>\<^sub>c \<acute>tptr \<and> (\<forall>x. \<^bsup>s\<^esup>ksSchedulerAction = 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 (\<acute>ksReadyQueues.[unat (d * 0x100 + v)]) \<noteq> NULL \<longrightarrow> option_map2 tcbPriority_C (cslift s) (head_C (\<acute>ksReadyQueues.[unat (d * 0x100 + v)])) \<noteq> None \<and> option_map2 tcbDomain_C (cslift s) (head_C (\<acute>ksReadyQueues.[unat (d * 0x100 + v)])) \<noteq> None)))\<rbrace> \<subseteq> ?P'2 s proof (prove)
goal (3 subgoals):
 1. \<And>s sa. \<Gamma>\<turnstile>\<^bsub>/UNIV\<^esub> (?P'24 s sa) \<acute>ret__int :== (if \<acute>tptr = \<acute>ksCurThread then 1 else 0);;
IF \<acute>ret__int \<noteq> 0 THEN
  \<acute>ret__int :== (if \<acute>ksSchedulerAction = tcb_Ptr (SCAST(32 signed \<rightarrow> 32) 0) then 1 else 0)
FI;;
IF \<acute>ret__int \<noteq> 0 THEN
  \<acute>ret__unsigned_long :== CALL isRunnable_'proc(\<acute>tptr);;
\<acute>ret__int :== (if \<not> \<acute>ret__unsigned_long \<noteq> 0 then 1 else 0)
FI;;
IF \<acute>ret__int \<noteq> 0 THEN
  CALL rescheduleRequired_'proc()
FI {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)},{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)}
 2. \<And>s. \<Gamma>\<turnstile>\<^bsub>/UNIV\<^esub> (?P'2 s) Guard C_Guard {s. s \<Turnstile>\<^sub>c tptr_' s} (CALL thread_state_ptr_set_tsType_'proc(PTR(thread_state_C) &(\<acute>tptr\<rightarrow>[''tcbState_C'']),UCAST(32 \<rightarrow> 32) \<acute>ts)) {sa. sa \<in> ?P'24 s sa},{s'. option_map2 tcbEPNext_C (cslift s') = option_map2 tcbEPNext_C (cslift s) \<and> option_map2 tcbEPPrev_C (cslift s') = option_map2 tcbEPPrev_C (cslift s) \<and> option_map2 tcbPriority_C (cslift s') = option_map2 tcbPriority_C (cslift s) \<and> option_map2 tcbDomain_C (cslift s') = option_map2 tcbDomain_C (cslift s) \<and> ksReadyQueues_' (globals s') = ksReadyQueues_' (globals s)}
 3. \<And>s. \<lbrace>s. s \<Turnstile>\<^sub>c \<acute>tptr \<and> (\<forall>x. \<^bsup>s\<^esup>ksSchedulerAction = 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 (\<acute>ksReadyQueues.[unat (d * 0x100 + v)]) \<noteq> NULL \<longrightarrow> option_map2 tcbPriority_C (cslift s) (head_C (\<acute>ksReadyQueues.[unat (d * 0x100 + v)])) \<noteq> None \<and> option_map2 tcbDomain_C (cslift s) (head_C (\<acute>ksReadyQueues.[unat (d * 0x100 + v)])) \<noteq> None)))\<rbrace> \<subseteq> ?P'2 s proof (prove)
goal (6 subgoals):
 1. \<And>s sa. \<Gamma>\<turnstile>\<^bsub>/UNIV\<^esub> (?P1.49 s sa) CALL rescheduleRequired_'proc() {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)},{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)}
 2. \<And>s sa. \<Gamma>\<turnstile>\<^bsub>/UNIV\<^esub> (?P2.49 s sa) SKIP {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)},{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)}
 3. \<And>s sa. ?R48 s sa \<subseteq> {sb. (sb \<in> \<lbrace>\<acute>ret__int \<noteq> 0\<rbrace> \<longrightarrow> sb \<in> ?P1.49 s sa) \<and> (sb \<notin> \<lbrace>\<acute>ret__int \<noteq> 0\<rbrace> \<longrightarrow> sb \<in> ?P2.49 s sa)}
 4. \<And>s sa. \<Gamma>\<turnstile>\<^bsub>/UNIV\<^esub> (?P'24 s sa) \<acute>ret__int :== (if \<acute>tptr = \<acute>ksCurThread then 1 else 0);;
IF \<acute>ret__int \<noteq> 0 THEN
  \<acute>ret__int :== (if \<acute>ksSchedulerAction = tcb_Ptr (SCAST(32 signed \<rightarrow> 32) 0) then 1 else 0)
FI;;
IF \<acute>ret__int \<noteq> 0 THEN
  \<acute>ret__unsigned_long :== CALL isRunnable_'proc(\<acute>tptr);;
\<acute>ret__int :== (if \<not> \<acute>ret__unsigned_long \<noteq> 0 then 1 else 0)
FI (?R48 s sa),{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)}
 5. \<And>s. \<Gamma>\<turnstile>\<^bsub>/UNIV\<^esub> (?P'2 s) Guard C_Guard {s. s \<Turnstile>\<^sub>c tptr_' s} (CALL thread_state_ptr_set_tsType_'proc(PTR(thread_state_C) &(\<acute>tptr\<rightarrow>[''tcbState_C'']),UCAST(32 \<rightarrow> 32) \<acute>ts)) {sa. sa \<in> ?P'24 s sa},{s'. option_map2 tcbEPNext_C (cslift s') = option_map2 tcbEPNext_C (cslift s) \<and> option_map2 tcbEPPrev_C (cslift s') = option_map2 tcbEPPrev_C (cslift s) \<and> option_map2 tcbPriority_C (cslift s') = option_map2 tcbPriority_C (cslift s) \<and> option_map2 tcbDomain_C (cslift s') = option_map2 tcbDomain_C (cslift s) \<and> ksReadyQueues_' (globals s') = ksReadyQueues_' (globals s)}
 6. \<And>s. \<lbrace>s. s \<Turnstile>\<^sub>c \<acute>tptr \<and> (\<forall>x. \<^bsup>s\<^esup>ksSchedulerAction = 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 (\<acute>ksReadyQueues.[unat (d * 0x100 + v)]) \<noteq> NULL \<longrightarrow> option_map2 tcbPriority_C (cslift s) (head_C (\<acute>ksReadyQueues.[unat (d * 0x100 + v)])) \<noteq> None \<and> option_map2 tcbDomain_C (cslift s) (head_C (\<acute>ksReadyQueues.[unat (d * 0x100 + v)])) \<noteq> None)))\<rbrace> \<subseteq> ?P'2 s proof (prove)
goal (5 subgoals):
 1. \<And>s sa. \<Gamma>\<turnstile>\<^bsub>/UNIV\<^esub> (?P2.49 s sa) SKIP {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)},{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)}
 2. \<And>s sa. ?R48 s sa \<subseteq> {sb. (sb \<in> \<lbrace>\<acute>ret__int \<noteq> 0\<rbrace> \<longrightarrow> sb \<in> {sa. (ksSchedulerAction_' (globals sa) \<noteq> tcb_Ptr (SCAST(32 signed \<rightarrow> 32) 0) \<and> ksSchedulerAction_' (globals sa) \<noteq> tcb_Ptr (SCAST(32 signed \<rightarrow> 32) 1) \<longrightarrow> (\<exists>d v. option_map2 tcbPriority_C (cslift sa) (ksSchedulerAction_' (globals sa)) = Some v \<and> unat v \<le> Config_H.numPriorities \<and> option_map2 tcbDomain_C (cslift sa) (ksSchedulerAction_' (globals sa)) = 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> option_map2 tcbEPNext_C (cslift sa) = option_map2 tcbEPNext_C (cslift s) \<and> option_map2 tcbEPPrev_C (cslift sa) = option_map2 tcbEPPrev_C (cslift s) \<and> option_map2 tcbPriority_C (cslift sa) = option_map2 tcbPriority_C (cslift s) \<and> option_map2 tcbDomain_C (cslift sa) = option_map2 tcbDomain_C (cslift s) \<and> ksReadyQueues_' (globals t) = ksReadyQueues_' (globals s))) \<and> (\<not> (ksSchedulerAction_' (globals sa) \<noteq> tcb_Ptr (SCAST(32 signed \<rightarrow> 32) 0) \<and> ksSchedulerAction_' (globals sa) \<noteq> tcb_Ptr (SCAST(32 signed \<rightarrow> 32) 1)) \<longrightarrow> option_map2 tcbEPNext_C (cslift sa) = option_map2 tcbEPNext_C (cslift s) \<and> option_map2 tcbEPPrev_C (cslift sa) = option_map2 tcbEPPrev_C (cslift s) \<and> option_map2 tcbPriority_C (cslift sa) = option_map2 tcbPriority_C (cslift s) \<and> option_map2 tcbDomain_C (cslift sa) = option_map2 tcbDomain_C (cslift s) \<and> ksReadyQueues_' (globals sa) = ksReadyQueues_' (globals s))}) \<and> (sb \<notin> \<lbrace>\<acute>ret__int \<noteq> 0\<rbrace> \<longrightarrow> sb \<in> ?P2.49 s sa)}
 3. \<And>s sa. \<Gamma>\<turnstile>\<^bsub>/UNIV\<^esub> (?P'24 s sa) \<acute>ret__int :== (if \<acute>tptr = \<acute>ksCurThread then 1 else 0);;
IF \<acute>ret__int \<noteq> 0 THEN
  \<acute>ret__int :== (if \<acute>ksSchedulerAction = tcb_Ptr (SCAST(32 signed \<rightarrow> 32) 0) then 1 else 0)
FI;;
IF \<acute>ret__int \<noteq> 0 THEN
  \<acute>ret__unsigned_long :== CALL isRunnable_'proc(\<acute>tptr);;
\<acute>ret__int :== (if \<not> \<acute>ret__unsigned_long \<noteq> 0 then 1 else 0)
FI (?R48 s sa),{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)}
 4. \<And>s. \<Gamma>\<turnstile>\<^bsub>/UNIV\<^esub> (?P'2 s) Guard C_Guard {s. s \<Turnstile>\<^sub>c tptr_' s} (CALL thread_state_ptr_set_tsType_'proc(PTR(thread_state_C) &(\<acute>tptr\<rightarrow>[''tcbState_C'']),UCAST(32 \<rightarrow> 32) \<acute>ts)) {sa. sa \<in> ?P'24 s sa},{s'. option_map2 tcbEPNext_C (cslift s') = option_map2 tcbEPNext_C (cslift s) \<and> option_map2 tcbEPPrev_C (cslift s') = option_map2 tcbEPPrev_C (cslift s) \<and> option_map2 tcbPriority_C (cslift s') = option_map2 tcbPriority_C (cslift s) \<and> option_map2 tcbDomain_C (cslift s') = option_map2 tcbDomain_C (cslift s) \<and> ksReadyQueues_' (globals s') = ksReadyQueues_' (globals s)}
 5. \<And>s. \<lbrace>s. s \<Turnstile>\<^sub>c \<acute>tptr \<and> (\<forall>x. \<^bsup>s\<^esup>ksSchedulerAction = 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 (\<acute>ksReadyQueues.[unat (d * 0x100 + v)]) \<noteq> NULL \<longrightarrow> option_map2 tcbPriority_C (cslift s) (head_C (\<acute>ksReadyQueues.[unat (d * 0x100 + v)])) \<noteq> None \<and> option_map2 tcbDomain_C (cslift s) (head_C (\<acute>ksReadyQueues.[unat (d * 0x100 + v)])) \<noteq> None)))\<rbrace> \<subseteq> ?P'2 s proof (prove)
goal (3 subgoals):
 1. \<And>s sa. \<Gamma>\<turnstile>\<^bsub>/UNIV\<^esub> (?P'24 s sa) \<acute>ret__int :== (if \<acute>tptr = \<acute>ksCurThread then 1 else 0);;
IF \<acute>ret__int \<noteq> 0 THEN
  \<acute>ret__int :== (if \<acute>ksSchedulerAction = tcb_Ptr (SCAST(32 signed \<rightarrow> 32) 0) then 1 else 0)
FI;;
IF \<acute>ret__int \<noteq> 0 THEN
  \<acute>ret__unsigned_long :== CALL isRunnable_'proc(\<acute>tptr);;
\<acute>ret__int :== (if \<not> \<acute>ret__unsigned_long \<noteq> 0 then 1 else 0)
FI {sa. (sa \<in> \<lbrace>\<acute>ret__int \<noteq> 0\<rbrace> \<longrightarrow> sa \<in> {sa. (ksSchedulerAction_' (globals sa) \<noteq> tcb_Ptr (SCAST(32 signed \<rightarrow> 32) 0) \<and> ksSchedulerAction_' (globals sa) \<noteq> tcb_Ptr (SCAST(32 signed \<rightarrow> 32) 1) \<longrightarrow> (\<exists>d v. option_map2 tcbPriority_C (cslift sa) (ksSchedulerAction_' (globals sa)) = Some v \<and> unat v \<le> Config_H.numPriorities \<and> option_map2 tcbDomain_C (cslift sa) (ksSchedulerAction_' (globals sa)) = 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> option_map2 tcbEPNext_C (cslift sa) = option_map2 tcbEPNext_C (cslift s) \<and> option_map2 tcbEPPrev_C (cslift sa) = option_map2 tcbEPPrev_C (cslift s) \<and> option_map2 tcbPriority_C (cslift sa) = option_map2 tcbPriority_C (cslift s) \<and> option_map2 tcbDomain_C (cslift sa) = option_map2 tcbDomain_C (cslift s) \<and> ksReadyQueues_' (globals t) = ksReadyQueues_' (globals s))) \<and> (\<not> (ksSchedulerAction_' (globals sa) \<noteq> tcb_Ptr (SCAST(32 signed \<rightarrow> 32) 0) \<and> ksSchedulerAction_' (globals sa) \<noteq> tcb_Ptr (SCAST(32 signed \<rightarrow> 32) 1)) \<longrightarrow> option_map2 tcbEPNext_C (cslift sa) = option_map2 tcbEPNext_C (cslift s) \<and> option_map2 tcbEPPrev_C (cslift sa) = option_map2 tcbEPPrev_C (cslift s) \<and> option_map2 tcbPriority_C (cslift sa) = option_map2 tcbPriority_C (cslift s) \<and> option_map2 tcbDomain_C (cslift sa) = option_map2 tcbDomain_C (cslift s) \<and> ksReadyQueues_' (globals sa) = ksReadyQueues_' (globals s))}) \<and> (sa \<notin> \<lbrace>\<acute>ret__int \<noteq> 0\<rbrace> \<longrightarrow> sa \<in> {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)})},{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)}
 2. \<And>s. \<Gamma>\<turnstile>\<^bsub>/UNIV\<^esub> (?P'2 s) Guard C_Guard {s. s \<Turnstile>\<^sub>c tptr_' s} (CALL thread_state_ptr_set_tsType_'proc(PTR(thread_state_C) &(\<acute>tptr\<rightarrow>[''tcbState_C'']),UCAST(32 \<rightarrow> 32) \<acute>ts)) {sa. sa \<in> ?P'24 s sa},{s'. option_map2 tcbEPNext_C (cslift s') = option_map2 tcbEPNext_C (cslift s) \<and> option_map2 tcbEPPrev_C (cslift s') = option_map2 tcbEPPrev_C (cslift s) \<and> option_map2 tcbPriority_C (cslift s') = option_map2 tcbPriority_C (cslift s) \<and> option_map2 tcbDomain_C (cslift s') = option_map2 tcbDomain_C (cslift s) \<and> ksReadyQueues_' (globals s') = ksReadyQueues_' (globals s)}
 3. \<And>s. \<lbrace>s. s \<Turnstile>\<^sub>c \<acute>tptr \<and> (\<forall>x. \<^bsup>s\<^esup>ksSchedulerAction = 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 (\<acute>ksReadyQueues.[unat (d * 0x100 + v)]) \<noteq> NULL \<longrightarrow> option_map2 tcbPriority_C (cslift s) (head_C (\<acute>ksReadyQueues.[unat (d * 0x100 + v)])) \<noteq> None \<and> option_map2 tcbDomain_C (cslift s) (head_C (\<acute>ksReadyQueues.[unat (d * 0x100 + v)])) \<noteq> None)))\<rbrace> \<subseteq> ?P'2 s proof (prove)
goal (6 subgoals):
 1. \<And>s sa. \<Gamma>\<turnstile>\<^bsub>/UNIV\<^esub> (?P1.109 s sa) \<acute>ret__unsigned_long :== CALL isRunnable_'proc(\<acute>tptr);;
\<acute>ret__int :== (if \<not> \<acute>ret__unsigned_long \<noteq> 0 then 1 else 0) {sa. (sa \<in> \<lbrace>\<acute>ret__int \<noteq> 0\<rbrace> \<longrightarrow> sa \<in> {sa. (ksSchedulerAction_' (globals sa) \<noteq> tcb_Ptr (SCAST(32 signed \<rightarrow> 32) 0) \<and> ksSchedulerAction_' (globals sa) \<noteq> tcb_Ptr (SCAST(32 signed \<rightarrow> 32) 1) \<longrightarrow> (\<exists>d v. option_map2 tcbPriority_C (cslift sa) (ksSchedulerAction_' (globals sa)) = Some v \<and> unat v \<le> Config_H.numPriorities \<and> option_map2 tcbDomain_C (cslift sa) (ksSchedulerAction_' (globals sa)) = 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> option_map2 tcbEPNext_C (cslift sa) = option_map2 tcbEPNext_C (cslift s) \<and> option_map2 tcbEPPrev_C (cslift sa) = option_map2 tcbEPPrev_C (cslift s) \<and> option_map2 tcbPriority_C (cslift sa) = option_map2 tcbPriority_C (cslift s) \<and> option_map2 tcbDomain_C (cslift sa) = option_map2 tcbDomain_C (cslift s) \<and> ksReadyQueues_' (globals t) = ksReadyQueues_' (globals s))) \<and> (\<not> (ksSchedulerAction_' (globals sa) \<noteq> tcb_Ptr (SCAST(32 signed \<rightarrow> 32) 0) \<and> ksSchedulerAction_' (globals sa) \<noteq> tcb_Ptr (SCAST(32 signed \<rightarrow> 32) 1)) \<longrightarrow> option_map2 tcbEPNext_C (cslift sa) = option_map2 tcbEPNext_C (cslift s) \<and> option_map2 tcbEPPrev_C (cslift sa) = option_map2 tcbEPPrev_C (cslift s) \<and> option_map2 tcbPriority_C (cslift sa) = option_map2 tcbPriority_C (cslift s) \<and> option_map2 tcbDomain_C (cslift sa) = option_map2 tcbDomain_C (cslift s) \<and> ksReadyQueues_' (globals sa) = ksReadyQueues_' (globals s))}) \<and> (sa \<notin> \<lbrace>\<acute>ret__int \<noteq> 0\<rbrace> \<longrightarrow> sa \<in> {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)})},{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)}
 2. \<And>s sa. \<Gamma>\<turnstile>\<^bsub>/UNIV\<^esub> (?P2.109 s sa) SKIP {sa. (sa \<in> \<lbrace>\<acute>ret__int \<noteq> 0\<rbrace> \<longrightarrow> sa \<in> {sa. (ksSchedulerAction_' (globals sa) \<noteq> tcb_Ptr (SCAST(32 signed \<rightarrow> 32) 0) \<and> ksSchedulerAction_' (globals sa) \<noteq> tcb_Ptr (SCAST(32 signed \<rightarrow> 32) 1) \<longrightarrow> (\<exists>d v. option_map2 tcbPriority_C (cslift sa) (ksSchedulerAction_' (globals sa)) = Some v \<and> unat v \<le> Config_H.numPriorities \<and> option_map2 tcbDomain_C (cslift sa) (ksSchedulerAction_' (globals sa)) = 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> option_map2 tcbEPNext_C (cslift sa) = option_map2 tcbEPNext_C (cslift s) \<and> option_map2 tcbEPPrev_C (cslift sa) = option_map2 tcbEPPrev_C (cslift s) \<and> option_map2 tcbPriority_C (cslift sa) = option_map2 tcbPriority_C (cslift s) \<and> option_map2 tcbDomain_C (cslift sa) = option_map2 tcbDomain_C (cslift s) \<and> ksReadyQueues_' (globals t) = ksReadyQueues_' (globals s))) \<and> (\<not> (ksSchedulerAction_' (globals sa) \<noteq> tcb_Ptr (SCAST(32 signed \<rightarrow> 32) 0) \<and> ksSchedulerAction_' (globals sa) \<noteq> tcb_Ptr (SCAST(32 signed \<rightarrow> 32) 1)) \<longrightarrow> option_map2 tcbEPNext_C (cslift sa) = option_map2 tcbEPNext_C (cslift s) \<and> option_map2 tcbEPPrev_C (cslift sa) = option_map2 tcbEPPrev_C (cslift s) \<and> option_map2 tcbPriority_C (cslift sa) = option_map2 tcbPriority_C (cslift s) \<and> option_map2 tcbDomain_C (cslift sa) = option_map2 tcbDomain_C (cslift s) \<and> ksReadyQueues_' (globals sa) = ksReadyQueues_' (globals s))}) \<and> (sa \<notin> \<lbrace>\<acute>ret__int \<noteq> 0\<rbrace> \<longrightarrow> sa \<in> {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)})},{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)}
 3. \<And>s sa. ?R108 s sa \<subseteq> {sb. (sb \<in> \<lbrace>\<acute>ret__int \<noteq> 0\<rbrace> \<longrightarrow> sb \<in> ?P1.109 s sa) \<and> (sb \<notin> \<lbrace>\<acute>ret__int \<noteq> 0\<rbrace> \<longrightarrow> sb \<in> ?P2.109 s sa)}
 4. \<And>s sa. \<Gamma>\<turnstile>\<^bsub>/UNIV\<^esub> (?P'24 s sa) \<acute>ret__int :== (if \<acute>tptr = \<acute>ksCurThread then 1 else 0);;
IF \<acute>ret__int \<noteq> 0 THEN
  \<acute>ret__int :== (if \<acute>ksSchedulerAction = tcb_Ptr (SCAST(32 signed \<rightarrow> 32) 0) then 1 else 0)
FI (?R108 s sa),{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)}
 5. \<And>s. \<Gamma>\<turnstile>\<^bsub>/UNIV\<^esub> (?P'2 s) Guard C_Guard {s. s \<Turnstile>\<^sub>c tptr_' s} (CALL thread_state_ptr_set_tsType_'proc(PTR(thread_state_C) &(\<acute>tptr\<rightarrow>[''tcbState_C'']),UCAST(32 \<rightarrow> 32) \<acute>ts)) {sa. sa \<in> ?P'24 s sa},{s'. option_map2 tcbEPNext_C (cslift s') = option_map2 tcbEPNext_C (cslift s) \<and> option_map2 tcbEPPrev_C (cslift s') = option_map2 tcbEPPrev_C (cslift s) \<and> option_map2 tcbPriority_C (cslift s') = option_map2 tcbPriority_C (cslift s) \<and> option_map2 tcbDomain_C (cslift s') = option_map2 tcbDomain_C (cslift s) \<and> ksReadyQueues_' (globals s') = ksReadyQueues_' (globals s)}
 6. \<And>s. \<lbrace>s. s \<Turnstile>\<^sub>c \<acute>tptr \<and> (\<forall>x. \<^bsup>s\<^esup>ksSchedulerAction = 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 (\<acute>ksReadyQueues.[unat (d * 0x100 + v)]) \<noteq> NULL \<longrightarrow> option_map2 tcbPriority_C (cslift s) (head_C (\<acute>ksReadyQueues.[unat (d * 0x100 + v)])) \<noteq> None \<and> option_map2 tcbDomain_C (cslift s) (head_C (\<acute>ksReadyQueues.[unat (d * 0x100 + v)])) \<noteq> None)))\<rbrace> \<subseteq> ?P'2 s proof (prove)
goal (5 subgoals):
 1. \<And>s sa. \<Gamma>\<turnstile>\<^bsub>/UNIV\<^esub> (?P2.109 s sa) SKIP {sa. (sa \<in> \<lbrace>\<acute>ret__int \<noteq> 0\<rbrace> \<longrightarrow> sa \<in> {sa. (ksSchedulerAction_' (globals sa) \<noteq> tcb_Ptr (SCAST(32 signed \<rightarrow> 32) 0) \<and> ksSchedulerAction_' (globals sa) \<noteq> tcb_Ptr (SCAST(32 signed \<rightarrow> 32) 1) \<longrightarrow> (\<exists>d v. option_map2 tcbPriority_C (cslift sa) (ksSchedulerAction_' (globals sa)) = Some v \<and> unat v \<le> Config_H.numPriorities \<and> option_map2 tcbDomain_C (cslift sa) (ksSchedulerAction_' (globals sa)) = 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> option_map2 tcbEPNext_C (cslift sa) = option_map2 tcbEPNext_C (cslift s) \<and> option_map2 tcbEPPrev_C (cslift sa) = option_map2 tcbEPPrev_C (cslift s) \<and> option_map2 tcbPriority_C (cslift sa) = option_map2 tcbPriority_C (cslift s) \<and> option_map2 tcbDomain_C (cslift sa) = option_map2 tcbDomain_C (cslift s) \<and> ksReadyQueues_' (globals t) = ksReadyQueues_' (globals s))) \<and> (\<not> (ksSchedulerAction_' (globals sa) \<noteq> tcb_Ptr (SCAST(32 signed \<rightarrow> 32) 0) \<and> ksSchedulerAction_' (globals sa) \<noteq> tcb_Ptr (SCAST(32 signed \<rightarrow> 32) 1)) \<longrightarrow> option_map2 tcbEPNext_C (cslift sa) = option_map2 tcbEPNext_C (cslift s) \<and> option_map2 tcbEPPrev_C (cslift sa) = option_map2 tcbEPPrev_C (cslift s) \<and> option_map2 tcbPriority_C (cslift sa) = option_map2 tcbPriority_C (cslift s) \<and> option_map2 tcbDomain_C (cslift sa) = option_map2 tcbDomain_C (cslift s) \<and> ksReadyQueues_' (globals sa) = ksReadyQueues_' (globals s))}) \<and> (sa \<notin> \<lbrace>\<acute>ret__int \<noteq> 0\<rbrace> \<longrightarrow> sa \<in> {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)})},{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)}
 2. \<And>s sa. ?R108 s sa \<subseteq> {sb. (sb \<in> \<lbrace>\<acute>ret__int \<noteq> 0\<rbrace> \<longrightarrow> sb \<in> {sa. \<forall>t. ((if ret__unsigned_long_' t = 0 then 1 else 0) \<noteq> 0 \<longrightarrow> (ksSchedulerAction_' (globals sa) \<noteq> tcb_Ptr (SCAST(32 signed \<rightarrow> 32) 0) \<and> ksSchedulerAction_' (globals sa) \<noteq> tcb_Ptr (SCAST(32 signed \<rightarrow> 32) 1) \<longrightarrow> (\<exists>d v. option_map2 tcbPriority_C (cslift sa) (ksSchedulerAction_' (globals sa)) = Some v \<and> unat v \<le> Config_H.numPriorities \<and> option_map2 tcbDomain_C (cslift sa) (ksSchedulerAction_' (globals sa)) = 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> option_map2 tcbEPNext_C (cslift sa) = option_map2 tcbEPNext_C (cslift s) \<and> option_map2 tcbEPPrev_C (cslift sa) = option_map2 tcbEPPrev_C (cslift s) \<and> option_map2 tcbPriority_C (cslift sa) = option_map2 tcbPriority_C (cslift s) \<and> option_map2 tcbDomain_C (cslift sa) = option_map2 tcbDomain_C (cslift s) \<and> ksReadyQueues_' (globals t) = ksReadyQueues_' (globals s))) \<and> (\<not> (ksSchedulerAction_' (globals sa) \<noteq> tcb_Ptr (SCAST(32 signed \<rightarrow> 32) 0) \<and> ksSchedulerAction_' (globals sa) \<noteq> tcb_Ptr (SCAST(32 signed \<rightarrow> 32) 1)) \<longrightarrow> option_map2 tcbEPNext_C (cslift sa) = option_map2 tcbEPNext_C (cslift s) \<and> option_map2 tcbEPPrev_C (cslift sa) = option_map2 tcbEPPrev_C (cslift s) \<and> option_map2 tcbPriority_C (cslift sa) = option_map2 tcbPriority_C (cslift s) \<and> option_map2 tcbDomain_C (cslift sa) = option_map2 tcbDomain_C (cslift s) \<and> ksReadyQueues_' (globals sa) = ksReadyQueues_' (globals s))) \<and> ((if ret__unsigned_long_' t = 0 then 1 else 0) = 0 \<longrightarrow> option_map2 tcbEPNext_C (cslift sa) = option_map2 tcbEPNext_C (cslift s) \<and> option_map2 tcbEPPrev_C (cslift sa) = option_map2 tcbEPPrev_C (cslift s) \<and> option_map2 tcbPriority_C (cslift sa) = option_map2 tcbPriority_C (cslift s) \<and> option_map2 tcbDomain_C (cslift sa) = option_map2 tcbDomain_C (cslift s) \<and> ksReadyQueues_' (globals sa) = ksReadyQueues_' (globals s))}) \<and> (sb \<notin> \<lbrace>\<acute>ret__int \<noteq> 0\<rbrace> \<longrightarrow> sb \<in> ?P2.109 s sa)}
 3. \<And>s sa. \<Gamma>\<turnstile>\<^bsub>/UNIV\<^esub> (?P'24 s sa) \<acute>ret__int :== (if \<acute>tptr = \<acute>ksCurThread then 1 else 0);;
IF \<acute>ret__int \<noteq> 0 THEN
  \<acute>ret__int :== (if \<acute>ksSchedulerAction = tcb_Ptr (SCAST(32 signed \<rightarrow> 32) 0) then 1 else 0)
FI (?R108 s sa),{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)}
 4. \<And>s. \<Gamma>\<turnstile>\<^bsub>/UNIV\<^esub> (?P'2 s) Guard C_Guard {s. s \<Turnstile>\<^sub>c tptr_' s} (CALL thread_state_ptr_set_tsType_'proc(PTR(thread_state_C) &(\<acute>tptr\<rightarrow>[''tcbState_C'']),UCAST(32 \<rightarrow> 32) \<acute>ts)) {sa. sa \<in> ?P'24 s sa},{s'. option_map2 tcbEPNext_C (cslift s') = option_map2 tcbEPNext_C (cslift s) \<and> option_map2 tcbEPPrev_C (cslift s') = option_map2 tcbEPPrev_C (cslift s) \<and> option_map2 tcbPriority_C (cslift s') = option_map2 tcbPriority_C (cslift s) \<and> option_map2 tcbDomain_C (cslift s') = option_map2 tcbDomain_C (cslift s) \<and> ksReadyQueues_' (globals s') = ksReadyQueues_' (globals s)}
 5. \<And>s. \<lbrace>s. s \<Turnstile>\<^sub>c \<acute>tptr \<and> (\<forall>x. \<^bsup>s\<^esup>ksSchedulerAction = 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 (\<acute>ksReadyQueues.[unat (d * 0x100 + v)]) \<noteq> NULL \<longrightarrow> option_map2 tcbPriority_C (cslift s) (head_C (\<acute>ksReadyQueues.[unat (d * 0x100 + v)])) \<noteq> None \<and> option_map2 tcbDomain_C (cslift s) (head_C (\<acute>ksReadyQueues.[unat (d * 0x100 + v)])) \<noteq> None)))\<rbrace> \<subseteq> ?P'2 s proof (prove)
goal (4 subgoals):
 1. \<And>s sa. ?R108 s sa \<subseteq> {sa. (sa \<in> \<lbrace>\<acute>ret__int \<noteq> 0\<rbrace> \<longrightarrow> sa \<in> {sa. \<forall>t. ((if ret__unsigned_long_' t = 0 then 1 else 0) \<noteq> 0 \<longrightarrow> (ksSchedulerAction_' (globals sa) \<noteq> tcb_Ptr (SCAST(32 signed \<rightarrow> 32) 0) \<and> ksSchedulerAction_' (globals sa) \<noteq> tcb_Ptr (SCAST(32 signed \<rightarrow> 32) 1) \<longrightarrow> (\<exists>d v. option_map2 tcbPriority_C (cslift sa) (ksSchedulerAction_' (globals sa)) = Some v \<and> unat v \<le> Config_H.numPriorities \<and> option_map2 tcbDomain_C (cslift sa) (ksSchedulerAction_' (globals sa)) = 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> option_map2 tcbEPNext_C (cslift sa) = option_map2 tcbEPNext_C (cslift s) \<and> option_map2 tcbEPPrev_C (cslift sa) = option_map2 tcbEPPrev_C (cslift s) \<and> option_map2 tcbPriority_C (cslift sa) = option_map2 tcbPriority_C (cslift s) \<and> option_map2 tcbDomain_C (cslift sa) = option_map2 tcbDomain_C (cslift s) \<and> ksReadyQueues_' (globals t) = ksReadyQueues_' (globals s))) \<and> (\<not> (ksSchedulerAction_' (globals sa) \<noteq> tcb_Ptr (SCAST(32 signed \<rightarrow> 32) 0) \<and> ksSchedulerAction_' (globals sa) \<noteq> tcb_Ptr (SCAST(32 signed \<rightarrow> 32) 1)) \<longrightarrow> option_map2 tcbEPNext_C (cslift sa) = option_map2 tcbEPNext_C (cslift s) \<and> option_map2 tcbEPPrev_C (cslift sa) = option_map2 tcbEPPrev_C (cslift s) \<and> option_map2 tcbPriority_C (cslift sa) = option_map2 tcbPriority_C (cslift s) \<and> option_map2 tcbDomain_C (cslift sa) = option_map2 tcbDomain_C (cslift s) \<and> ksReadyQueues_' (globals sa) = ksReadyQueues_' (globals s))) \<and> ((if ret__unsigned_long_' t = 0 then 1 else 0) = 0 \<longrightarrow> option_map2 tcbEPNext_C (cslift sa) = option_map2 tcbEPNext_C (cslift s) \<and> option_map2 tcbEPPrev_C (cslift sa) = option_map2 tcbEPPrev_C (cslift s) \<and> option_map2 tcbPriority_C (cslift sa) = option_map2 tcbPriority_C (cslift s) \<and> option_map2 tcbDomain_C (cslift sa) = option_map2 tcbDomain_C (cslift s) \<and> ksReadyQueues_' (globals sa) = ksReadyQueues_' (globals s))}) \<and> (sa \<notin> \<lbrace>\<acute>ret__int \<noteq> 0\<rbrace> \<longrightarrow> sa \<in> {sa. (ret__int_' sa \<noteq> 0 \<longrightarrow> (ksSchedulerAction_' (globals sa) \<noteq> tcb_Ptr (SCAST(32 signed \<rightarrow> 32) 0) \<and> ksSchedulerAction_' (globals sa) \<noteq> tcb_Ptr (SCAST(32 signed \<rightarrow> 32) 1) \<longrightarrow> (\<exists>d v. option_map2 tcbPriority_C (cslift sa) (ksSchedulerAction_' (globals sa)) = Some v \<and> unat v \<le> Config_H.numPriorities \<and> option_map2 tcbDomain_C (cslift sa) (ksSchedulerAction_' (globals sa)) = 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> option_map2 tcbEPNext_C (cslift sa) = option_map2 tcbEPNext_C (cslift s) \<and> option_map2 tcbEPPrev_C (cslift sa) = option_map2 tcbEPPrev_C (cslift s) \<and> option_map2 tcbPriority_C (cslift sa) = option_map2 tcbPriority_C (cslift s) \<and> option_map2 tcbDomain_C (cslift sa) = option_map2 tcbDomain_C (cslift s) \<and> ksReadyQueues_' (globals t) = ksReadyQueues_' (globals s))) \<and> (\<not> (ksSchedulerAction_' (globals sa) \<noteq> tcb_Ptr (SCAST(32 signed \<rightarrow> 32) 0) \<and> ksSchedulerAction_' (globals sa) \<noteq> tcb_Ptr (SCAST(32 signed \<rightarrow> 32) 1)) \<longrightarrow> option_map2 tcbEPNext_C (cslift sa) = option_map2 tcbEPNext_C (cslift s) \<and> option_map2 tcbEPPrev_C (cslift sa) = option_map2 tcbEPPrev_C (cslift s) \<and> option_map2 tcbPriority_C (cslift sa) = option_map2 tcbPriority_C (cslift s) \<and> option_map2 tcbDomain_C (cslift sa) = option_map2 tcbDomain_C (cslift s) \<and> ksReadyQueues_' (globals sa) = ksReadyQueues_' (globals s))) \<and> (\<not> ret__int_' sa \<noteq> 0 \<longrightarrow> option_map2 tcbEPNext_C (cslift sa) = option_map2 tcbEPNext_C (cslift s) \<and> option_map2 tcbEPPrev_C (cslift sa) = option_map2 tcbEPPrev_C (cslift s) \<and> option_map2 tcbPriority_C (cslift sa) = option_map2 tcbPriority_C (cslift s) \<and> option_map2 tcbDomain_C (cslift sa) = option_map2 tcbDomain_C (cslift s) \<and> ksReadyQueues_' (globals sa) = ksReadyQueues_' (globals s))})}
 2. \<And>s sa. \<Gamma>\<turnstile>\<^bsub>/UNIV\<^esub> (?P'24 s sa) \<acute>ret__int :== (if \<acute>tptr = \<acute>ksCurThread then 1 else 0);;
IF \<acute>ret__int \<noteq> 0 THEN
  \<acute>ret__int :== (if \<acute>ksSchedulerAction = tcb_Ptr (SCAST(32 signed \<rightarrow> 32) 0) then 1 else 0)
FI (?R108 s sa),{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)}
 3. \<And>s. \<Gamma>\<turnstile>\<^bsub>/UNIV\<^esub> (?P'2 s) Guard C_Guard {s. s \<Turnstile>\<^sub>c tptr_' s} (CALL thread_state_ptr_set_tsType_'proc(PTR(thread_state_C) &(\<acute>tptr\<rightarrow>[''tcbState_C'']),UCAST(32 \<rightarrow> 32) \<acute>ts)) {sa. sa \<in> ?P'24 s sa},{s'. option_map2 tcbEPNext_C (cslift s') = option_map2 tcbEPNext_C (cslift s) \<and> option_map2 tcbEPPrev_C (cslift s') = option_map2 tcbEPPrev_C (cslift s) \<and> option_map2 tcbPriority_C (cslift s') = option_map2 tcbPriority_C (cslift s) \<and> option_map2 tcbDomain_C (cslift s') = option_map2 tcbDomain_C (cslift s) \<and> ksReadyQueues_' (globals s') = ksReadyQueues_' (globals s)}
 4. \<And>s. \<lbrace>s. s \<Turnstile>\<^sub>c \<acute>tptr \<and> (\<forall>x. \<^bsup>s\<^esup>ksSchedulerAction = 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 (\<acute>ksReadyQueues.[unat (d * 0x100 + v)]) \<noteq> NULL \<longrightarrow> option_map2 tcbPriority_C (cslift s) (head_C (\<acute>ksReadyQueues.[unat (d * 0x100 + v)])) \<noteq> None \<and> option_map2 tcbDomain_C (cslift s) (head_C (\<acute>ksReadyQueues.[unat (d * 0x100 + v)])) \<noteq> None)))\<rbrace> \<subseteq> ?P'2 s proof (prove)
goal (3 subgoals):
 1. \<And>s sa. \<Gamma>\<turnstile>\<^bsub>/UNIV\<^esub> (?P'24 s sa) \<acute>ret__int :== (if \<acute>tptr = \<acute>ksCurThread then 1 else 0);;
IF \<acute>ret__int \<noteq> 0 THEN
  \<acute>ret__int :== (if \<acute>ksSchedulerAction = tcb_Ptr (SCAST(32 signed \<rightarrow> 32) 0) then 1 else 0)
FI {sa. (sa \<in> \<lbrace>\<acute>ret__int \<noteq> 0\<rbrace> \<longrightarrow> sa \<in> {sa. \<forall>t. ((if ret__unsigned_long_' t = 0 then 1 else 0) \<noteq> 0 \<longrightarrow> (ksSchedulerAction_' (globals sa) \<noteq> tcb_Ptr (SCAST(32 signed \<rightarrow> 32) 0) \<and> ksSchedulerAction_' (globals sa) \<noteq> tcb_Ptr (SCAST(32 signed \<rightarrow> 32) 1) \<longrightarrow> (\<exists>d v. option_map2 tcbPriority_C (cslift sa) (ksSchedulerAction_' (globals sa)) = Some v \<and> unat v \<le> Config_H.numPriorities \<and> option_map2 tcbDomain_C (cslift sa) (ksSchedulerAction_' (globals sa)) = 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> option_map2 tcbEPNext_C (cslift sa) = option_map2 tcbEPNext_C (cslift s) \<and> option_map2 tcbEPPrev_C (cslift sa) = option_map2 tcbEPPrev_C (cslift s) \<and> option_map2 tcbPriority_C (cslift sa) = option_map2 tcbPriority_C (cslift s) \<and> option_map2 tcbDomain_C (cslift sa) = option_map2 tcbDomain_C (cslift s) \<and> ksReadyQueues_' (globals t) = ksReadyQueues_' (globals s))) \<and> (\<not> (ksSchedulerAction_' (globals sa) \<noteq> tcb_Ptr (SCAST(32 signed \<rightarrow> 32) 0) \<and> ksSchedulerAction_' (globals sa) \<noteq> tcb_Ptr (SCAST(32 signed \<rightarrow> 32) 1)) \<longrightarrow> option_map2 tcbEPNext_C (cslift sa) = option_map2 tcbEPNext_C (cslift s) \<and> option_map2 tcbEPPrev_C (cslift sa) = option_map2 tcbEPPrev_C (cslift s) \<and> option_map2 tcbPriority_C (cslift sa) = option_map2 tcbPriority_C (cslift s) \<and> option_map2 tcbDomain_C (cslift sa) = option_map2 tcbDomain_C (cslift s) \<and> ksReadyQueues_' (globals sa) = ksReadyQueues_' (globals s))) \<and> ((if ret__unsigned_long_' t = 0 then 1 else 0) = 0 \<longrightarrow> option_map2 tcbEPNext_C (cslift sa) = option_map2 tcbEPNext_C (cslift s) \<and> option_map2 tcbEPPrev_C (cslift sa) = option_map2 tcbEPPrev_C (cslift s) \<and> option_map2 tcbPriority_C (cslift sa) = option_map2 tcbPriority_C (cslift s) \<and> option_map2 tcbDomain_C (cslift sa) = option_map2 tcbDomain_C (cslift s) \<and> ksReadyQueues_' (globals sa) = ksReadyQueues_' (globals s))}) \<and> (sa \<notin> \<lbrace>\<acute>ret__int \<noteq> 0\<rbrace> \<longrightarrow> sa \<in> {sa. (ret__int_' sa \<noteq> 0 \<longrightarrow> (ksSchedulerAction_' (globals sa) \<noteq> tcb_Ptr (SCAST(32 signed \<rightarrow> 32) 0) \<and> ksSchedulerAction_' (globals sa) \<noteq> tcb_Ptr (SCAST(32 signed \<rightarrow> 32) 1) \<longrightarrow> (\<exists>d v. option_map2 tcbPriority_C (cslift sa) (ksSchedulerAction_' (globals sa)) = Some v \<and> unat v \<le> Config_H.numPriorities \<and> option_map2 tcbDomain_C (cslift sa) (ksSchedulerAction_' (globals sa)) = 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> option_map2 tcbEPNext_C (cslift sa) = option_map2 tcbEPNext_C (cslift s) \<and> option_map2 tcbEPPrev_C (cslift sa) = option_map2 tcbEPPrev_C (cslift s) \<and> option_map2 tcbPriority_C (cslift sa) = option_map2 tcbPriority_C (cslift s) \<and> option_map2 tcbDomain_C (cslift sa) = option_map2 tcbDomain_C (cslift s) \<and> ksReadyQueues_' (globals t) = ksReadyQueues_' (globals s))) \<and> (\<not> (ksSchedulerAction_' (globals sa) \<noteq> tcb_Ptr (SCAST(32 signed \<rightarrow> 32) 0) \<and> ksSchedulerAction_' (globals sa) \<noteq> tcb_Ptr (SCAST(32 signed \<rightarrow> 32) 1)) \<longrightarrow> option_map2 tcbEPNext_C (cslift sa) = option_map2 tcbEPNext_C (cslift s) \<and> option_map2 tcbEPPrev_C (cslift sa) = option_map2 tcbEPPrev_C (cslift s) \<and> option_map2 tcbPriority_C (cslift sa) = option_map2 tcbPriority_C (cslift s) \<and> option_map2 tcbDomain_C (cslift sa) = option_map2 tcbDomain_C (cslift s) \<and> ksReadyQueues_' (globals sa) = ksReadyQueues_' (globals s))) \<and> (\<not> ret__int_' sa \<noteq> 0 \<longrightarrow> option_map2 tcbEPNext_C (cslift sa) = option_map2 tcbEPNext_C (cslift s) \<and> option_map2 tcbEPPrev_C (cslift sa) = option_map2 tcbEPPrev_C (cslift s) \<and> option_map2 tcbPriority_C (cslift sa) = option_map2 tcbPriority_C (cslift s) \<and> option_map2 tcbDomain_C (cslift sa) = option_map2 tcbDomain_C (cslift s) \<and> ksReadyQueues_' (globals sa) = ksReadyQueues_' (globals s))})},{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)}
 2. \<And>s. \<Gamma>\<turnstile>\<^bsub>/UNIV\<^esub> (?P'2 s) Guard C_Guard {s. s \<Turnstile>\<^sub>c tptr_' s} (CALL thread_state_ptr_set_tsType_'proc(PTR(thread_state_C) &(\<acute>tptr\<rightarrow>[''tcbState_C'']),UCAST(32 \<rightarrow> 32) \<acute>ts)) {sa. sa \<in> ?P'24 s sa},{s'. option_map2 tcbEPNext_C (cslift s') = option_map2 tcbEPNext_C (cslift s) \<and> option_map2 tcbEPPrev_C (cslift s') = option_map2 tcbEPPrev_C (cslift s) \<and> option_map2 tcbPriority_C (cslift s') = option_map2 tcbPriority_C (cslift s) \<and> option_map2 tcbDomain_C (cslift s') = option_map2 tcbDomain_C (cslift s) \<and> ksReadyQueues_' (globals s') = ksReadyQueues_' (globals s)}
 3. \<And>s. \<lbrace>s. s \<Turnstile>\<^sub>c \<acute>tptr \<and> (\<forall>x. \<^bsup>s\<^esup>ksSchedulerAction = 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 (\<acute>ksReadyQueues.[unat (d * 0x100 + v)]) \<noteq> NULL \<longrightarrow> option_map2 tcbPriority_C (cslift s) (head_C (\<acute>ksReadyQueues.[unat (d * 0x100 + v)])) \<noteq> None \<and> option_map2 tcbDomain_C (cslift s) (head_C (\<acute>ksReadyQueues.[unat (d * 0x100 + v)])) \<noteq> None)))\<rbrace> \<subseteq> ?P'2 s proof (prove)
goal (6 subgoals):
 1. \<And>s sa. \<Gamma>\<turnstile>\<^bsub>/UNIV\<^esub> (?P1.145 s sa) \<acute>ret__int :== (if \<acute>ksSchedulerAction = tcb_Ptr (SCAST(32 signed \<rightarrow> 32) 0) then 1 else 0) {sa. (sa \<in> \<lbrace>\<acute>ret__int \<noteq> 0\<rbrace> \<longrightarrow> sa \<in> {sa. \<forall>t. ((if ret__unsigned_long_' t = 0 then 1 else 0) \<noteq> 0 \<longrightarrow> (ksSchedulerAction_' (globals sa) \<noteq> tcb_Ptr (SCAST(32 signed \<rightarrow> 32) 0) \<and> ksSchedulerAction_' (globals sa) \<noteq> tcb_Ptr (SCAST(32 signed \<rightarrow> 32) 1) \<longrightarrow> (\<exists>d v. option_map2 tcbPriority_C (cslift sa) (ksSchedulerAction_' (globals sa)) = Some v \<and> unat v \<le> Config_H.numPriorities \<and> option_map2 tcbDomain_C (cslift sa) (ksSchedulerAction_' (globals sa)) = 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> option_map2 tcbEPNext_C (cslift sa) = option_map2 tcbEPNext_C (cslift s) \<and> option_map2 tcbEPPrev_C (cslift sa) = option_map2 tcbEPPrev_C (cslift s) \<and> option_map2 tcbPriority_C (cslift sa) = option_map2 tcbPriority_C (cslift s) \<and> option_map2 tcbDomain_C (cslift sa) = option_map2 tcbDomain_C (cslift s) \<and> ksReadyQueues_' (globals t) = ksReadyQueues_' (globals s))) \<and> (\<not> (ksSchedulerAction_' (globals sa) \<noteq> tcb_Ptr (SCAST(32 signed \<rightarrow> 32) 0) \<and> ksSchedulerAction_' (globals sa) \<noteq> tcb_Ptr (SCAST(32 signed \<rightarrow> 32) 1)) \<longrightarrow> option_map2 tcbEPNext_C (cslift sa) = option_map2 tcbEPNext_C (cslift s) \<and> option_map2 tcbEPPrev_C (cslift sa) = option_map2 tcbEPPrev_C (cslift s) \<and> option_map2 tcbPriority_C (cslift sa) = option_map2 tcbPriority_C (cslift s) \<and> option_map2 tcbDomain_C (cslift sa) = option_map2 tcbDomain_C (cslift s) \<and> ksReadyQueues_' (globals sa) = ksReadyQueues_' (globals s))) \<and> ((if ret__unsigned_long_' t = 0 then 1 else 0) = 0 \<longrightarrow> option_map2 tcbEPNext_C (cslift sa) = option_map2 tcbEPNext_C (cslift s) \<and> option_map2 tcbEPPrev_C (cslift sa) = option_map2 tcbEPPrev_C (cslift s) \<and> option_map2 tcbPriority_C (cslift sa) = option_map2 tcbPriority_C (cslift s) \<and> option_map2 tcbDomain_C (cslift sa) = option_map2 tcbDomain_C (cslift s) \<and> ksReadyQueues_' (globals sa) = ksReadyQueues_' (globals s))}) \<and> (sa \<notin> \<lbrace>\<acute>ret__int \<noteq> 0\<rbrace> \<longrightarrow> sa \<in> {sa. (ret__int_' sa \<noteq> 0 \<longrightarrow> (ksSchedulerAction_' (globals sa) \<noteq> tcb_Ptr (SCAST(32 signed \<rightarrow> 32) 0) \<and> ksSchedulerAction_' (globals sa) \<noteq> tcb_Ptr (SCAST(32 signed \<rightarrow> 32) 1) \<longrightarrow> (\<exists>d v. option_map2 tcbPriority_C (cslift sa) (ksSchedulerAction_' (globals sa)) = Some v \<and> unat v \<le> Config_H.numPriorities \<and> option_map2 tcbDomain_C (cslift sa) (ksSchedulerAction_' (globals sa)) = 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> option_map2 tcbEPNext_C (cslift sa) = option_map2 tcbEPNext_C (cslift s) \<and> option_map2 tcbEPPrev_C (cslift sa) = option_map2 tcbEPPrev_C (cslift s) \<and> option_map2 tcbPriority_C (cslift sa) = option_map2 tcbPriority_C (cslift s) \<and> option_map2 tcbDomain_C (cslift sa) = option_map2 tcbDomain_C (cslift s) \<and> ksReadyQueues_' (globals t) = ksReadyQueues_' (globals s))) \<and> (\<not> (ksSchedulerAction_' (globals sa) \<noteq> tcb_Ptr (SCAST(32 signed \<rightarrow> 32) 0) \<and> ksSchedulerAction_' (globals sa) \<noteq> tcb_Ptr (SCAST(32 signed \<rightarrow> 32) 1)) \<longrightarrow> option_map2 tcbEPNext_C (cslift sa) = option_map2 tcbEPNext_C (cslift s) \<and> option_map2 tcbEPPrev_C (cslift sa) = option_map2 tcbEPPrev_C (cslift s) \<and> option_map2 tcbPriority_C (cslift sa) = option_map2 tcbPriority_C (cslift s) \<and> option_map2 tcbDomain_C (cslift sa) = option_map2 tcbDomain_C (cslift s) \<and> ksReadyQueues_' (globals sa) = ksReadyQueues_' (globals s))) \<and> (\<not> ret__int_' sa \<noteq> 0 \<longrightarrow> option_map2 tcbEPNext_C (cslift sa) = option_map2 tcbEPNext_C (cslift s) \<and> option_map2 tcbEPPrev_C (cslift sa) = option_map2 tcbEPPrev_C (cslift s) \<and> option_map2 tcbPriority_C (cslift sa) = option_map2 tcbPriority_C (cslift s) \<and> option_map2 tcbDomain_C (cslift sa) = option_map2 tcbDomain_C (cslift s) \<and> ksReadyQueues_' (globals sa) = ksReadyQueues_' (globals s))})},{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)}
 2. \<And>s sa. \<Gamma>\<turnstile>\<^bsub>/UNIV\<^esub> (?P2.145 s sa) SKIP {sa. (sa \<in> \<lbrace>\<acute>ret__int \<noteq> 0\<rbrace> \<longrightarrow> sa \<in> {sa. \<forall>t. ((if ret__unsigned_long_' t = 0 then 1 else 0) \<noteq> 0 \<longrightarrow> (ksSchedulerAction_' (globals sa) \<noteq> tcb_Ptr (SCAST(32 signed \<rightarrow> 32) 0) \<and> ksSchedulerAction_' (globals sa) \<noteq> tcb_Ptr (SCAST(32 signed \<rightarrow> 32) 1) \<longrightarrow> (\<exists>d v. option_map2 tcbPriority_C (cslift sa) (ksSchedulerAction_' (globals sa)) = Some v \<and> unat v \<le> Config_H.numPriorities \<and> option_map2 tcbDomain_C (cslift sa) (ksSchedulerAction_' (globals sa)) = 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> option_map2 tcbEPNext_C (cslift sa) = option_map2 tcbEPNext_C (cslift s) \<and> option_map2 tcbEPPrev_C (cslift sa) = option_map2 tcbEPPrev_C (cslift s) \<and> option_map2 tcbPriority_C (cslift sa) = option_map2 tcbPriority_C (cslift s) \<and> option_map2 tcbDomain_C (cslift sa) = option_map2 tcbDomain_C (cslift s) \<and> ksReadyQueues_' (globals t) = ksReadyQueues_' (globals s))) \<and> (\<not> (ksSchedulerAction_' (globals sa) \<noteq> tcb_Ptr (SCAST(32 signed \<rightarrow> 32) 0) \<and> ksSchedulerAction_' (globals sa) \<noteq> tcb_Ptr (SCAST(32 signed \<rightarrow> 32) 1)) \<longrightarrow> option_map2 tcbEPNext_C (cslift sa) = option_map2 tcbEPNext_C (cslift s) \<and> option_map2 tcbEPPrev_C (cslift sa) = option_map2 tcbEPPrev_C (cslift s) \<and> option_map2 tcbPriority_C (cslift sa) = option_map2 tcbPriority_C (cslift s) \<and> option_map2 tcbDomain_C (cslift sa) = option_map2 tcbDomain_C (cslift s) \<and> ksReadyQueues_' (globals sa) = ksReadyQueues_' (globals s))) \<and> ((if ret__unsigned_long_' t = 0 then 1 else 0) = 0 \<longrightarrow> option_map2 tcbEPNext_C (cslift sa) = option_map2 tcbEPNext_C (cslift s) \<and> option_map2 tcbEPPrev_C (cslift sa) = option_map2 tcbEPPrev_C (cslift s) \<and> option_map2 tcbPriority_C (cslift sa) = option_map2 tcbPriority_C (cslift s) \<and> option_map2 tcbDomain_C (cslift sa) = option_map2 tcbDomain_C (cslift s) \<and> ksReadyQueues_' (globals sa) = ksReadyQueues_' (globals s))}) \<and> (sa \<notin> \<lbrace>\<acute>ret__int \<noteq> 0\<rbrace> \<longrightarrow> sa \<in> {sa. (ret__int_' sa \<noteq> 0 \<longrightarrow> (ksSchedulerAction_' (globals sa) \<noteq> tcb_Ptr (SCAST(32 signed \<rightarrow> 32) 0) \<and> ksSchedulerAction_' (globals sa) \<noteq> tcb_Ptr (SCAST(32 signed \<rightarrow> 32) 1) \<longrightarrow> (\<exists>d v. option_map2 tcbPriority_C (cslift sa) (ksSchedulerAction_' (globals sa)) = Some v \<and> unat v \<le> Config_H.numPriorities \<and> option_map2 tcbDomain_C (cslift sa) (ksSchedulerAction_' (globals sa)) = 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> option_map2 tcbEPNext_C (cslift sa) = option_map2 tcbEPNext_C (cslift s) \<and> option_map2 tcbEPPrev_C (cslift sa) = option_map2 tcbEPPrev_C (cslift s) \<and> option_map2 tcbPriority_C (cslift sa) = option_map2 tcbPriority_C (cslift s) \<and> option_map2 tcbDomain_C (cslift sa) = option_map2 tcbDomain_C (cslift s) \<and> ksReadyQueues_' (globals t) = ksReadyQueues_' (globals s))) \<and> (\<not> (ksSchedulerAction_' (globals sa) \<noteq> tcb_Ptr (SCAST(32 signed \<rightarrow> 32) 0) \<and> ksSchedulerAction_' (globals sa) \<noteq> tcb_Ptr (SCAST(32 signed \<rightarrow> 32) 1)) \<longrightarrow> option_map2 tcbEPNext_C (cslift sa) = option_map2 tcbEPNext_C (cslift s) \<and> option_map2 tcbEPPrev_C (cslift sa) = option_map2 tcbEPPrev_C (cslift s) \<and> option_map2 tcbPriority_C (cslift sa) = option_map2 tcbPriority_C (cslift s) \<and> option_map2 tcbDomain_C (cslift sa) = option_map2 tcbDomain_C (cslift s) \<and> ksReadyQueues_' (globals sa) = ksReadyQueues_' (globals s))) \<and> (\<not> ret__int_' sa \<noteq> 0 \<longrightarrow> option_map2 tcbEPNext_C (cslift sa) = option_map2 tcbEPNext_C (cslift s) \<and> option_map2 tcbEPPrev_C (cslift sa) = option_map2 tcbEPPrev_C (cslift s) \<and> option_map2 tcbPriority_C (cslift sa) = option_map2 tcbPriority_C (cslift s) \<and> option_map2 tcbDomain_C (cslift sa) = option_map2 tcbDomain_C (cslift s) \<and> ksReadyQueues_' (globals sa) = ksReadyQueues_' (globals s))})},{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)}
 3. \<And>s sa. ?R144 s sa \<subseteq> {sb. (sb \<in> \<lbrace>\<acute>ret__int \<noteq> 0\<rbrace> \<longrightarrow> sb \<in> ?P1.145 s sa) \<and> (sb \<notin> \<lbrace>\<acute>ret__int \<noteq> 0\<rbrace> \<longrightarrow> sb \<in> ?P2.145 s sa)}
 4. \<And>s sa. \<Gamma>\<turnstile>\<^bsub>/UNIV\<^esub> (?P'24 s sa) \<acute>ret__int :== (if \<acute>tptr = \<acute>ksCurThread then 1 else 0) (?R144 s sa),{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)}
 5. \<And>s. \<Gamma>\<turnstile>\<^bsub>/UNIV\<^esub> (?P'2 s) Guard C_Guard {s. s \<Turnstile>\<^sub>c tptr_' s} (CALL thread_state_ptr_set_tsType_'proc(PTR(thread_state_C) &(\<acute>tptr\<rightarrow>[''tcbState_C'']),UCAST(32 \<rightarrow> 32) \<acute>ts)) {sa. sa \<in> ?P'24 s sa},{s'. option_map2 tcbEPNext_C (cslift s') = option_map2 tcbEPNext_C (cslift s) \<and> option_map2 tcbEPPrev_C (cslift s') = option_map2 tcbEPPrev_C (cslift s) \<and> option_map2 tcbPriority_C (cslift s') = option_map2 tcbPriority_C (cslift s) \<and> option_map2 tcbDomain_C (cslift s') = option_map2 tcbDomain_C (cslift s) \<and> ksReadyQueues_' (globals s') = ksReadyQueues_' (globals s)}
 6. \<And>s. \<lbrace>s. s \<Turnstile>\<^sub>c \<acute>tptr \<and> (\<forall>x. \<^bsup>s\<^esup>ksSchedulerAction = 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 (\<acute>ksReadyQueues.[unat (d * 0x100 + v)]) \<noteq> NULL \<longrightarrow> option_map2 tcbPriority_C (cslift s) (head_C (\<acute>ksReadyQueues.[unat (d * 0x100 + v)])) \<noteq> None \<and> option_map2 tcbDomain_C (cslift s) (head_C (\<acute>ksReadyQueues.[unat (d * 0x100 + v)])) \<noteq> None)))\<rbrace> \<subseteq> ?P'2 s proof (prove)
goal (5 subgoals):
 1. \<And>s sa. \<Gamma>\<turnstile>\<^bsub>/UNIV\<^esub> (?P2.145 s sa) SKIP {sa. (sa \<in> \<lbrace>\<acute>ret__int \<noteq> 0\<rbrace> \<longrightarrow> sa \<in> {sa. \<forall>t. ((if ret__unsigned_long_' t = 0 then 1 else 0) \<noteq> 0 \<longrightarrow> (ksSchedulerAction_' (globals sa) \<noteq> tcb_Ptr (SCAST(32 signed \<rightarrow> 32) 0) \<and> ksSchedulerAction_' (globals sa) \<noteq> tcb_Ptr (SCAST(32 signed \<rightarrow> 32) 1) \<longrightarrow> (\<exists>d v. option_map2 tcbPriority_C (cslift sa) (ksSchedulerAction_' (globals sa)) = Some v \<and> unat v \<le> Config_H.numPriorities \<and> option_map2 tcbDomain_C (cslift sa) (ksSchedulerAction_' (globals sa)) = 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> option_map2 tcbEPNext_C (cslift sa) = option_map2 tcbEPNext_C (cslift s) \<and> option_map2 tcbEPPrev_C (cslift sa) = option_map2 tcbEPPrev_C (cslift s) \<and> option_map2 tcbPriority_C (cslift sa) = option_map2 tcbPriority_C (cslift s) \<and> option_map2 tcbDomain_C (cslift sa) = option_map2 tcbDomain_C (cslift s) \<and> ksReadyQueues_' (globals t) = ksReadyQueues_' (globals s))) \<and> (\<not> (ksSchedulerAction_' (globals sa) \<noteq> tcb_Ptr (SCAST(32 signed \<rightarrow> 32) 0) \<and> ksSchedulerAction_' (globals sa) \<noteq> tcb_Ptr (SCAST(32 signed \<rightarrow> 32) 1)) \<longrightarrow> option_map2 tcbEPNext_C (cslift sa) = option_map2 tcbEPNext_C (cslift s) \<and> option_map2 tcbEPPrev_C (cslift sa) = option_map2 tcbEPPrev_C (cslift s) \<and> option_map2 tcbPriority_C (cslift sa) = option_map2 tcbPriority_C (cslift s) \<and> option_map2 tcbDomain_C (cslift sa) = option_map2 tcbDomain_C (cslift s) \<and> ksReadyQueues_' (globals sa) = ksReadyQueues_' (globals s))) \<and> ((if ret__unsigned_long_' t = 0 then 1 else 0) = 0 \<longrightarrow> option_map2 tcbEPNext_C (cslift sa) = option_map2 tcbEPNext_C (cslift s) \<and> option_map2 tcbEPPrev_C (cslift sa) = option_map2 tcbEPPrev_C (cslift s) \<and> option_map2 tcbPriority_C (cslift sa) = option_map2 tcbPriority_C (cslift s) \<and> option_map2 tcbDomain_C (cslift sa) = option_map2 tcbDomain_C (cslift s) \<and> ksReadyQueues_' (globals sa) = ksReadyQueues_' (globals s))}) \<and> (sa \<notin> \<lbrace>\<acute>ret__int \<noteq> 0\<rbrace> \<longrightarrow> sa \<in> {sa. (ret__int_' sa \<noteq> 0 \<longrightarrow> (ksSchedulerAction_' (globals sa) \<noteq> tcb_Ptr (SCAST(32 signed \<rightarrow> 32) 0) \<and> ksSchedulerAction_' (globals sa) \<noteq> tcb_Ptr (SCAST(32 signed \<rightarrow> 32) 1) \<longrightarrow> (\<exists>d v. option_map2 tcbPriority_C (cslift sa) (ksSchedulerAction_' (globals sa)) = Some v \<and> unat v \<le> Config_H.numPriorities \<and> option_map2 tcbDomain_C (cslift sa) (ksSchedulerAction_' (globals sa)) = 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> option_map2 tcbEPNext_C (cslift sa) = option_map2 tcbEPNext_C (cslift s) \<and> option_map2 tcbEPPrev_C (cslift sa) = option_map2 tcbEPPrev_C (cslift s) \<and> option_map2 tcbPriority_C (cslift sa) = option_map2 tcbPriority_C (cslift s) \<and> option_map2 tcbDomain_C (cslift sa) = option_map2 tcbDomain_C (cslift s) \<and> ksReadyQueues_' (globals t) = ksReadyQueues_' (globals s))) \<and> (\<not> (ksSchedulerAction_' (globals sa) \<noteq> tcb_Ptr (SCAST(32 signed \<rightarrow> 32) 0) \<and> ksSchedulerAction_' (globals sa) \<noteq> tcb_Ptr (SCAST(32 signed \<rightarrow> 32) 1)) \<longrightarrow> option_map2 tcbEPNext_C (cslift sa) = option_map2 tcbEPNext_C (cslift s) \<and> option_map2 tcbEPPrev_C (cslift sa) = option_map2 tcbEPPrev_C (cslift s) \<and> option_map2 tcbPriority_C (cslift sa) = option_map2 tcbPriority_C (cslift s) \<and> option_map2 tcbDomain_C (cslift sa) = option_map2 tcbDomain_C (cslift s) \<and> ksReadyQueues_' (globals sa) = ksReadyQueues_' (globals s))) \<and> (\<not> ret__int_' sa \<noteq> 0 \<longrightarrow> option_map2 tcbEPNext_C (cslift sa) = option_map2 tcbEPNext_C (cslift s) \<and> option_map2 tcbEPPrev_C (cslift sa) = option_map2 tcbEPPrev_C (cslift s) \<and> option_map2 tcbPriority_C (cslift sa) = option_map2 tcbPriority_C (cslift s) \<and> option_map2 tcbDomain_C (cslift sa) = option_map2 tcbDomain_C (cslift s) \<and> ksReadyQueues_' (globals sa) = ksReadyQueues_' (globals s))})},{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)}
 2. \<And>s sa. ?R144 s sa \<subseteq> {sb. (sb \<in> \<lbrace>\<acute>ret__int \<noteq> 0\<rbrace> \<longrightarrow> sb \<in> {sa. ((if ksSchedulerAction_' (globals sa) = tcb_Ptr (SCAST(32 signed \<rightarrow> 32) 0) then 1 else 0) \<noteq> 0 \<longrightarrow> (\<forall>t. ((if ret__unsigned_long_' t = 0 then 1 else 0) \<noteq> 0 \<longrightarrow> (ksSchedulerAction_' (globals sa) \<noteq> tcb_Ptr (SCAST(32 signed \<rightarrow> 32) 0) \<and> ksSchedulerAction_' (globals sa) \<noteq> tcb_Ptr (SCAST(32 signed \<rightarrow> 32) 1) \<longrightarrow> (\<exists>d v. option_map2 tcbPriority_C (cslift sa) (ksSchedulerAction_' (globals sa)) = Some v \<and> unat v \<le> Config_H.numPriorities \<and> option_map2 tcbDomain_C (cslift sa) (ksSchedulerAction_' (globals sa)) = 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> option_map2 tcbEPNext_C (cslift sa) = option_map2 tcbEPNext_C (cslift s) \<and> option_map2 tcbEPPrev_C (cslift sa) = option_map2 tcbEPPrev_C (cslift s) \<and> option_map2 tcbPriority_C (cslift sa) = option_map2 tcbPriority_C (cslift s) \<and> option_map2 tcbDomain_C (cslift sa) = option_map2 tcbDomain_C (cslift s) \<and> ksReadyQueues_' (globals t) = ksReadyQueues_' (globals s))) \<and> (\<not> (ksSchedulerAction_' (globals sa) \<noteq> tcb_Ptr (SCAST(32 signed \<rightarrow> 32) 0) \<and> ksSchedulerAction_' (globals sa) \<noteq> tcb_Ptr (SCAST(32 signed \<rightarrow> 32) 1)) \<longrightarrow> option_map2 tcbEPNext_C (cslift sa) = option_map2 tcbEPNext_C (cslift s) \<and> option_map2 tcbEPPrev_C (cslift sa) = option_map2 tcbEPPrev_C (cslift s) \<and> option_map2 tcbPriority_C (cslift sa) = option_map2 tcbPriority_C (cslift s) \<and> option_map2 tcbDomain_C (cslift sa) = option_map2 tcbDomain_C (cslift s) \<and> ksReadyQueues_' (globals sa) = ksReadyQueues_' (globals s))) \<and> ((if ret__unsigned_long_' t = 0 then 1 else 0) = 0 \<longrightarrow> option_map2 tcbEPNext_C (cslift sa) = option_map2 tcbEPNext_C (cslift s) \<and> option_map2 tcbEPPrev_C (cslift sa) = option_map2 tcbEPPrev_C (cslift s) \<and> option_map2 tcbPriority_C (cslift sa) = option_map2 tcbPriority_C (cslift s) \<and> option_map2 tcbDomain_C (cslift sa) = option_map2 tcbDomain_C (cslift s) \<and> ksReadyQueues_' (globals sa) = ksReadyQueues_' (globals s)))) \<and> (\<not> (if ksSchedulerAction_' (globals sa) = tcb_Ptr (SCAST(32 signed \<rightarrow> 32) 0) then 1 else 0) \<noteq> 0 \<longrightarrow> ((if ksSchedulerAction_' (globals sa) = tcb_Ptr (SCAST(32 signed \<rightarrow> 32) 0) then 1 else 0) \<noteq> 0 \<longrightarrow> (ksSchedulerAction_' (globals sa) \<noteq> tcb_Ptr (SCAST(32 signed \<rightarrow> 32) 0) \<and> ksSchedulerAction_' (globals sa) \<noteq> tcb_Ptr (SCAST(32 signed \<rightarrow> 32) 1) \<longrightarrow> (\<exists>d v. option_map2 tcbPriority_C (cslift sa) (ksSchedulerAction_' (globals sa)) = Some v \<and> unat v \<le> Config_H.numPriorities \<and> option_map2 tcbDomain_C (cslift sa) (ksSchedulerAction_' (globals sa)) = 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> option_map2 tcbEPNext_C (cslift sa) = option_map2 tcbEPNext_C (cslift s) \<and> option_map2 tcbEPPrev_C (cslift sa) = option_map2 tcbEPPrev_C (cslift s) \<and> option_map2 tcbPriority_C (cslift sa) = option_map2 tcbPriority_C (cslift s) \<and> option_map2 tcbDomain_C (cslift sa) = option_map2 tcbDomain_C (cslift s) \<and> ksReadyQueues_' (globals t) = ksReadyQueues_' (globals s))) \<and> (\<not> (ksSchedulerAction_' (globals sa) \<noteq> tcb_Ptr (SCAST(32 signed \<rightarrow> 32) 0) \<and> ksSchedulerAction_' (globals sa) \<noteq> tcb_Ptr (SCAST(32 signed \<rightarrow> 32) 1)) \<longrightarrow> option_map2 tcbEPNext_C (cslift sa) = option_map2 tcbEPNext_C (cslift s) \<and> option_map2 tcbEPPrev_C (cslift sa) = option_map2 tcbEPPrev_C (cslift s) \<and> option_map2 tcbPriority_C (cslift sa) = option_map2 tcbPriority_C (cslift s) \<and> option_map2 tcbDomain_C (cslift sa) = option_map2 tcbDomain_C (cslift s) \<and> ksReadyQueues_' (globals sa) = ksReadyQueues_' (globals s))) \<and> (\<not> (if ksSchedulerAction_' (globals sa) = tcb_Ptr (SCAST(32 signed \<rightarrow> 32) 0) then 1 else 0) \<noteq> 0 \<longrightarrow> option_map2 tcbEPNext_C (cslift sa) = option_map2 tcbEPNext_C (cslift s) \<and> option_map2 tcbEPPrev_C (cslift sa) = option_map2 tcbEPPrev_C (cslift s) \<and> option_map2 tcbPriority_C (cslift sa) = option_map2 tcbPriority_C (cslift s) \<and> option_map2 tcbDomain_C (cslift sa) = option_map2 tcbDomain_C (cslift s) \<and> ksReadyQueues_' (globals sa) = ksReadyQueues_' (globals s)))}) \<and> (sb \<notin> \<lbrace>\<acute>ret__int \<noteq> 0\<rbrace> \<longrightarrow> sb \<in> ?P2.145 s sa)}
 3. \<And>s sa. \<Gamma>\<turnstile>\<^bsub>/UNIV\<^esub> (?P'24 s sa) \<acute>ret__int :== (if \<acute>tptr = \<acute>ksCurThread then 1 else 0) (?R144 s sa),{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)}
 4. \<And>s. \<Gamma>\<turnstile>\<^bsub>/UNIV\<^esub> (?P'2 s) Guard C_Guard {s. s \<Turnstile>\<^sub>c tptr_' s} (CALL thread_state_ptr_set_tsType_'proc(PTR(thread_state_C) &(\<acute>tptr\<rightarrow>[''tcbState_C'']),UCAST(32 \<rightarrow> 32) \<acute>ts)) {sa. sa \<in> ?P'24 s sa},{s'. option_map2 tcbEPNext_C (cslift s') = option_map2 tcbEPNext_C (cslift s) \<and> option_map2 tcbEPPrev_C (cslift s') = option_map2 tcbEPPrev_C (cslift s) \<and> option_map2 tcbPriority_C (cslift s') = option_map2 tcbPriority_C (cslift s) \<and> option_map2 tcbDomain_C (cslift s') = option_map2 tcbDomain_C (cslift s) \<and> ksReadyQueues_' (globals s') = ksReadyQueues_' (globals s)}
 5. \<And>s. \<lbrace>s. s \<Turnstile>\<^sub>c \<acute>tptr \<and> (\<forall>x. \<^bsup>s\<^esup>ksSchedulerAction = 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 (\<acute>ksReadyQueues.[unat (d * 0x100 + v)]) \<noteq> NULL \<longrightarrow> option_map2 tcbPriority_C (cslift s) (head_C (\<acute>ksReadyQueues.[unat (d * 0x100 + v)])) \<noteq> None \<and> option_map2 tcbDomain_C (cslift s) (head_C (\<acute>ksReadyQueues.[unat (d * 0x100 + v)])) \<noteq> None)))\<rbrace> \<subseteq> ?P'2 s proof (prove)
goal (4 subgoals):
 1. \<And>s sa. ?R144 s sa \<subseteq> {sa. (sa \<in> \<lbrace>\<acute>ret__int \<noteq> 0\<rbrace> \<longrightarrow> sa \<in> {sa. ((if ksSchedulerAction_' (globals sa) = tcb_Ptr (SCAST(32 signed \<rightarrow> 32) 0) then 1 else 0) \<noteq> 0 \<longrightarrow> (\<forall>t. ((if ret__unsigned_long_' t = 0 then 1 else 0) \<noteq> 0 \<longrightarrow> (ksSchedulerAction_' (globals sa) \<noteq> tcb_Ptr (SCAST(32 signed \<rightarrow> 32) 0) \<and> ksSchedulerAction_' (globals sa) \<noteq> tcb_Ptr (SCAST(32 signed \<rightarrow> 32) 1) \<longrightarrow> (\<exists>d v. option_map2 tcbPriority_C (cslift sa) (ksSchedulerAction_' (globals sa)) = Some v \<and> unat v \<le> Config_H.numPriorities \<and> option_map2 tcbDomain_C (cslift sa) (ksSchedulerAction_' (globals sa)) = 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> option_map2 tcbEPNext_C (cslift sa) = option_map2 tcbEPNext_C (cslift s) \<and> option_map2 tcbEPPrev_C (cslift sa) = option_map2 tcbEPPrev_C (cslift s) \<and> option_map2 tcbPriority_C (cslift sa) = option_map2 tcbPriority_C (cslift s) \<and> option_map2 tcbDomain_C (cslift sa) = option_map2 tcbDomain_C (cslift s) \<and> ksReadyQueues_' (globals t) = ksReadyQueues_' (globals s))) \<and> (\<not> (ksSchedulerAction_' (globals sa) \<noteq> tcb_Ptr (SCAST(32 signed \<rightarrow> 32) 0) \<and> ksSchedulerAction_' (globals sa) \<noteq> tcb_Ptr (SCAST(32 signed \<rightarrow> 32) 1)) \<longrightarrow> option_map2 tcbEPNext_C (cslift sa) = option_map2 tcbEPNext_C (cslift s) \<and> option_map2 tcbEPPrev_C (cslift sa) = option_map2 tcbEPPrev_C (cslift s) \<and> option_map2 tcbPriority_C (cslift sa) = option_map2 tcbPriority_C (cslift s) \<and> option_map2 tcbDomain_C (cslift sa) = option_map2 tcbDomain_C (cslift s) \<and> ksReadyQueues_' (globals sa) = ksReadyQueues_' (globals s))) \<and> ((if ret__unsigned_long_' t = 0 then 1 else 0) = 0 \<longrightarrow> option_map2 tcbEPNext_C (cslift sa) = option_map2 tcbEPNext_C (cslift s) \<and> option_map2 tcbEPPrev_C (cslift sa) = option_map2 tcbEPPrev_C (cslift s) \<and> option_map2 tcbPriority_C (cslift sa) = option_map2 tcbPriority_C (cslift s) \<and> option_map2 tcbDomain_C (cslift sa) = option_map2 tcbDomain_C (cslift s) \<and> ksReadyQueues_' (globals sa) = ksReadyQueues_' (globals s)))) \<and> (\<not> (if ksSchedulerAction_' (globals sa) = tcb_Ptr (SCAST(32 signed \<rightarrow> 32) 0) then 1 else 0) \<noteq> 0 \<longrightarrow> ((if ksSchedulerAction_' (globals sa) = tcb_Ptr (SCAST(32 signed \<rightarrow> 32) 0) then 1 else 0) \<noteq> 0 \<longrightarrow> (ksSchedulerAction_' (globals sa) \<noteq> tcb_Ptr (SCAST(32 signed \<rightarrow> 32) 0) \<and> ksSchedulerAction_' (globals sa) \<noteq> tcb_Ptr (SCAST(32 signed \<rightarrow> 32) 1) \<longrightarrow> (\<exists>d v. option_map2 tcbPriority_C (cslift sa) (ksSchedulerAction_' (globals sa)) = Some v \<and> unat v \<le> Config_H.numPriorities \<and> option_map2 tcbDomain_C (cslift sa) (ksSchedulerAction_' (globals sa)) = 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> option_map2 tcbEPNext_C (cslift sa) = option_map2 tcbEPNext_C (cslift s) \<and> option_map2 tcbEPPrev_C (cslift sa) = option_map2 tcbEPPrev_C (cslift s) \<and> option_map2 tcbPriority_C (cslift sa) = option_map2 tcbPriority_C (cslift s) \<and> option_map2 tcbDomain_C (cslift sa) = option_map2 tcbDomain_C (cslift s) \<and> ksReadyQueues_' (globals t) = ksReadyQueues_' (globals s))) \<and> (\<not> (ksSchedulerAction_' (globals sa) \<noteq> tcb_Ptr (SCAST(32 signed \<rightarrow> 32) 0) \<and> ksSchedulerAction_' (globals sa) \<noteq> tcb_Ptr (SCAST(32 signed \<rightarrow> 32) 1)) \<longrightarrow> option_map2 tcbEPNext_C (cslift sa) = option_map2 tcbEPNext_C (cslift s) \<and> option_map2 tcbEPPrev_C (cslift sa) = option_map2 tcbEPPrev_C (cslift s) \<and> option_map2 tcbPriority_C (cslift sa) = option_map2 tcbPriority_C (cslift s) \<and> option_map2 tcbDomain_C (cslift sa) = option_map2 tcbDomain_C (cslift s) \<and> ksReadyQueues_' (globals sa) = ksReadyQueues_' (globals s))) \<and> (\<not> (if ksSchedulerAction_' (globals sa) = tcb_Ptr (SCAST(32 signed \<rightarrow> 32) 0) then 1 else 0) \<noteq> 0 \<longrightarrow> option_map2 tcbEPNext_C (cslift sa) = option_map2 tcbEPNext_C (cslift s) \<and> option_map2 tcbEPPrev_C (cslift sa) = option_map2 tcbEPPrev_C (cslift s) \<and> option_map2 tcbPriority_C (cslift sa) = option_map2 tcbPriority_C (cslift s) \<and> option_map2 tcbDomain_C (cslift sa) = option_map2 tcbDomain_C (cslift s) \<and> ksReadyQueues_' (globals sa) = ksReadyQueues_' (globals s)))}) \<and> (sa \<notin> \<lbrace>\<acute>ret__int \<noteq> 0\<rbrace> \<longrightarrow> sa \<in> {sa. (ret__int_' sa \<noteq> 0 \<longrightarrow> (\<forall>t. ((if ret__unsigned_long_' t = 0 then 1 else 0) \<noteq> 0 \<longrightarrow> (ksSchedulerAction_' (globals sa) \<noteq> tcb_Ptr (SCAST(32 signed \<rightarrow> 32) 0) \<and> ksSchedulerAction_' (globals sa) \<noteq> tcb_Ptr (SCAST(32 signed \<rightarrow> 32) 1) \<longrightarrow> (\<exists>d v. option_map2 tcbPriority_C (cslift sa) (ksSchedulerAction_' (globals sa)) = Some v \<and> unat v \<le> Config_H.numPriorities \<and> option_map2 tcbDomain_C (cslift sa) (ksSchedulerAction_' (globals sa)) = 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> option_map2 tcbEPNext_C (cslift sa) = option_map2 tcbEPNext_C (cslift s) \<and> option_map2 tcbEPPrev_C (cslift sa) = option_map2 tcbEPPrev_C (cslift s) \<and> option_map2 tcbPriority_C (cslift sa) = option_map2 tcbPriority_C (cslift s) \<and> option_map2 tcbDomain_C (cslift sa) = option_map2 tcbDomain_C (cslift s) \<and> ksReadyQueues_' (globals t) = ksReadyQueues_' (globals s))) \<and> (\<not> (ksSchedulerAction_' (globals sa) \<noteq> tcb_Ptr (SCAST(32 signed \<rightarrow> 32) 0) \<and> ksSchedulerAction_' (globals sa) \<noteq> tcb_Ptr (SCAST(32 signed \<rightarrow> 32) 1)) \<longrightarrow> option_map2 tcbEPNext_C (cslift sa) = option_map2 tcbEPNext_C (cslift s) \<and> option_map2 tcbEPPrev_C (cslift sa) = option_map2 tcbEPPrev_C (cslift s) \<and> option_map2 tcbPriority_C (cslift sa) = option_map2 tcbPriority_C (cslift s) \<and> option_map2 tcbDomain_C (cslift sa) = option_map2 tcbDomain_C (cslift s) \<and> ksReadyQueues_' (globals sa) = ksReadyQueues_' (globals s))) \<and> ((if ret__unsigned_long_' t = 0 then 1 else 0) = 0 \<longrightarrow> option_map2 tcbEPNext_C (cslift sa) = option_map2 tcbEPNext_C (cslift s) \<and> option_map2 tcbEPPrev_C (cslift sa) = option_map2 tcbEPPrev_C (cslift s) \<and> option_map2 tcbPriority_C (cslift sa) = option_map2 tcbPriority_C (cslift s) \<and> option_map2 tcbDomain_C (cslift sa) = option_map2 tcbDomain_C (cslift s) \<and> ksReadyQueues_' (globals sa) = ksReadyQueues_' (globals s)))) \<and> (\<not> ret__int_' sa \<noteq> 0 \<longrightarrow> (ret__int_' sa \<noteq> 0 \<longrightarrow> (ksSchedulerAction_' (globals sa) \<noteq> tcb_Ptr (SCAST(32 signed \<rightarrow> 32) 0) \<and> ksSchedulerAction_' (globals sa) \<noteq> tcb_Ptr (SCAST(32 signed \<rightarrow> 32) 1) \<longrightarrow> (\<exists>d v. option_map2 tcbPriority_C (cslift sa) (ksSchedulerAction_' (globals sa)) = Some v \<and> unat v \<le> Config_H.numPriorities \<and> option_map2 tcbDomain_C (cslift sa) (ksSchedulerAction_' (globals sa)) = 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> option_map2 tcbEPNext_C (cslift sa) = option_map2 tcbEPNext_C (cslift s) \<and> option_map2 tcbEPPrev_C (cslift sa) = option_map2 tcbEPPrev_C (cslift s) \<and> option_map2 tcbPriority_C (cslift sa) = option_map2 tcbPriority_C (cslift s) \<and> option_map2 tcbDomain_C (cslift sa) = option_map2 tcbDomain_C (cslift s) \<and> ksReadyQueues_' (globals t) = ksReadyQueues_' (globals s))) \<and> (\<not> (ksSchedulerAction_' (globals sa) \<noteq> tcb_Ptr (SCAST(32 signed \<rightarrow> 32) 0) \<and> ksSchedulerAction_' (globals sa) \<noteq> tcb_Ptr (SCAST(32 signed \<rightarrow> 32) 1)) \<longrightarrow> option_map2 tcbEPNext_C (cslift sa) = option_map2 tcbEPNext_C (cslift s) \<and> option_map2 tcbEPPrev_C (cslift sa) = option_map2 tcbEPPrev_C (cslift s) \<and> option_map2 tcbPriority_C (cslift sa) = option_map2 tcbPriority_C (cslift s) \<and> option_map2 tcbDomain_C (cslift sa) = option_map2 tcbDomain_C (cslift s) \<and> ksReadyQueues_' (globals sa) = ksReadyQueues_' (globals s))) \<and> (\<not> ret__int_' sa \<noteq> 0 \<longrightarrow> option_map2 tcbEPNext_C (cslift sa) = option_map2 tcbEPNext_C (cslift s) \<and> option_map2 tcbEPPrev_C (cslift sa) = option_map2 tcbEPPrev_C (cslift s) \<and> option_map2 tcbPriority_C (cslift sa) = option_map2 tcbPriority_C (cslift s) \<and> option_map2 tcbDomain_C (cslift sa) = option_map2 tcbDomain_C (cslift s) \<and> ksReadyQueues_' (globals sa) = ksReadyQueues_' (globals s)))})}
 2. \<And>s sa. \<Gamma>\<turnstile>\<^bsub>/UNIV\<^esub> (?P'24 s sa) \<acute>ret__int :== (if \<acute>tptr = \<acute>ksCurThread then 1 else 0) (?R144 s sa),{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)}
 3. \<And>s. \<Gamma>\<turnstile>\<^bsub>/UNIV\<^esub> (?P'2 s) Guard C_Guard {s. s \<Turnstile>\<^sub>c tptr_' s} (CALL thread_state_ptr_set_tsType_'proc(PTR(thread_state_C) &(\<acute>tptr\<rightarrow>[''tcbState_C'']),UCAST(32 \<rightarrow> 32) \<acute>ts)) {sa. sa \<in> ?P'24 s sa},{s'. option_map2 tcbEPNext_C (cslift s') = option_map2 tcbEPNext_C (cslift s) \<and> option_map2 tcbEPPrev_C (cslift s') = option_map2 tcbEPPrev_C (cslift s) \<and> option_map2 tcbPriority_C (cslift s') = option_map2 tcbPriority_C (cslift s) \<and> option_map2 tcbDomain_C (cslift s') = option_map2 tcbDomain_C (cslift s) \<and> ksReadyQueues_' (globals s') = ksReadyQueues_' (globals s)}
 4. \<And>s. \<lbrace>s. s \<Turnstile>\<^sub>c \<acute>tptr \<and> (\<forall>x. \<^bsup>s\<^esup>ksSchedulerAction = 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 (\<acute>ksReadyQueues.[unat (d * 0x100 + v)]) \<noteq> NULL \<longrightarrow> option_map2 tcbPriority_C (cslift s) (head_C (\<acute>ksReadyQueues.[unat (d * 0x100 + v)])) \<noteq> None \<and> option_map2 tcbDomain_C (cslift s) (head_C (\<acute>ksReadyQueues.[unat (d * 0x100 + v)])) \<noteq> None)))\<rbrace> \<subseteq> ?P'2 s proof (prove)
goal (1 subgoal):
 1. \<And>t_hrs ksCurThread ksReadyQueues ksSchedulerAction tptr ts. \<lbrakk>hrs_htd t_hrs \<Turnstile>\<^sub>t tptr; \<forall>x. ksSchedulerAction = tcb_Ptr x \<and> x \<noteq> 0 \<and> x \<noteq> 1 \<longrightarrow> (\<exists>d v. option_map2 tcbPriority_C (clift t_hrs) (tcb_Ptr x) = Some v \<and> unat v \<le> Config_H.numPriorities \<and> option_map2 tcbDomain_C (clift t_hrs) (tcb_Ptr x) = Some d \<and> unat d < numDomains \<and> (StateRelation_C.end_C (ksReadyQueues.[unat (d * 0x100 + v)]) \<noteq> NULL \<longrightarrow> option_map2 tcbPriority_C (clift t_hrs) (head_C (ksReadyQueues.[unat (d * 0x100 + v)])) \<noteq> None \<and> option_map2 tcbDomain_C (clift t_hrs) (head_C (ksReadyQueues.[unat (d * 0x100 + v)])) \<noteq> None))\<rbrakk> \<Longrightarrow> hrs_htd t_hrs \<Turnstile>\<^sub>t tptr \<longrightarrow> hrs_htd t_hrs \<Turnstile>\<^sub>t cparent (PTR(thread_state_C) &(tptr\<rightarrow>[''tcbState_C''])) [''tcbState_C''] \<and> (\<forall>t_hrsa. (\<exists>thread_state. thread_state_lift thread_state = thread_state_lift (tcbState_C (the (clift t_hrs (cparent (PTR(thread_state_C) &(tptr\<rightarrow>[''tcbState_C''])) [''tcbState_C'']))))\<lparr>tsType_CL := UCAST(32 \<rightarrow> 32) ts && mask 4\<rparr> \<and> t_hrsa = hrs_mem_update (heap_update (cparent (PTR(thread_state_C) &(tptr\<rightarrow>[''tcbState_C''])) [''tcbState_C'']) (tcbState_C_update (\<lambda>_. thread_state) (the (clift t_hrs (cparent (PTR(thread_state_C) &(tptr\<rightarrow>[''tcbState_C''])) [''tcbState_C'']))))) t_hrs) \<longrightarrow> ((if tptr = ksCurThread then 1 else 0) \<noteq> 0 \<longrightarrow> ((if ksSchedulerAction = tcb_Ptr (SCAST(32 signed \<rightarrow> 32) 0) then 1 else 0) \<noteq> 0 \<longrightarrow> (\<forall>ret__unsigned_long. ((if ret__unsigned_long = 0 then 1 else 0) \<noteq> 0 \<longrightarrow> (ksSchedulerAction \<noteq> tcb_Ptr (SCAST(32 signed \<rightarrow> 32) 0) \<and> ksSchedulerAction \<noteq> tcb_Ptr (SCAST(32 signed \<rightarrow> 32) 1) \<longrightarrow> (\<exists>d v. option_map2 tcbPriority_C (clift t_hrsa) ksSchedulerAction = Some v \<and> unat v \<le> Config_H.numPriorities \<and> option_map2 tcbDomain_C (clift t_hrsa) ksSchedulerAction = Some d \<and> unat d < numDomains \<and> (StateRelation_C.end_C (ksReadyQueues.[unat (d * 0x100 + v)]) \<noteq> NULL \<longrightarrow> option_map2 tcbPriority_C (clift t_hrsa) (head_C (ksReadyQueues.[unat (d * 0x100 + v)])) \<noteq> None \<and> option_map2 tcbDomain_C (clift t_hrsa) (head_C (ksReadyQueues.[unat (d * 0x100 + v)])) \<noteq> None)) \<and> (\<forall>t_hrsb ksReadyQueuesa. option_map2 tcbEPNext_C (clift t_hrsb) = option_map2 tcbEPNext_C (clift t_hrsa) \<and> option_map2 tcbEPPrev_C (clift t_hrsb) = option_map2 tcbEPPrev_C (clift t_hrsa) \<and> option_map2 tcbPriority_C (clift t_hrsb) = option_map2 tcbPriority_C (clift t_hrsa) \<and> option_map2 tcbDomain_C (clift t_hrsb) = option_map2 tcbDomain_C (clift t_hrsa) \<longrightarrow> option_map2 tcbEPNext_C (clift t_hrsa) = option_map2 tcbEPNext_C (clift t_hrs) \<and> option_map2 tcbEPPrev_C (clift t_hrsa) = option_map2 tcbEPPrev_C (clift t_hrs) \<and> option_map2 tcbPriority_C (clift t_hrsa) = option_map2 tcbPriority_C (clift t_hrs) \<and> option_map2 tcbDomain_C (clift t_hrsa) = option_map2 tcbDomain_C (clift t_hrs) \<and> ksReadyQueuesa = ksReadyQueues)) \<and> (\<not> (ksSchedulerAction \<noteq> tcb_Ptr (SCAST(32 signed \<rightarrow> 32) 0) \<and> ksSchedulerAction \<noteq> tcb_Ptr (SCAST(32 signed \<rightarrow> 32) 1)) \<longrightarrow> option_map2 tcbEPNext_C (clift t_hrsa) = option_map2 tcbEPNext_C (clift t_hrs) \<and> option_map2 tcbEPPrev_C (clift t_hrsa) = option_map2 tcbEPPrev_C (clift t_hrs) \<and> option_map2 tcbPriority_C (clift t_hrsa) = option_map2 tcbPriority_C (clift t_hrs) \<and> option_map2 tcbDomain_C (clift t_hrsa) = option_map2 tcbDomain_C (clift t_hrs) \<and> ksReadyQueues = ksReadyQueues)) \<and> ((if ret__unsigned_long = 0 then 1 else 0) = 0 \<longrightarrow> option_map2 tcbEPNext_C (clift t_hrsa) = option_map2 tcbEPNext_C (clift t_hrs) \<and> option_map2 tcbEPPrev_C (clift t_hrsa) = option_map2 tcbEPPrev_C (clift t_hrs) \<and> option_map2 tcbPriority_C (clift t_hrsa) = option_map2 tcbPriority_C (clift t_hrs) \<and> option_map2 tcbDomain_C (clift t_hrsa) = option_map2 tcbDomain_C (clift t_hrs) \<and> ksReadyQueues = ksReadyQueues))) \<and> ((if ksSchedulerAction = tcb_Ptr (SCAST(32 signed \<rightarrow> 32) 0) then 1 else 0) = 0 \<longrightarrow> option_map2 tcbEPNext_C (clift t_hrsa) = option_map2 tcbEPNext_C (clift t_hrs) \<and> option_map2 tcbEPPrev_C (clift t_hrsa) = option_map2 tcbEPPrev_C (clift t_hrs) \<and> option_map2 tcbPriority_C (clift t_hrsa) = option_map2 tcbPriority_C (clift t_hrs) \<and> option_map2 tcbDomain_C (clift t_hrsa) = option_map2 tcbDomain_C (clift t_hrs) \<and> ksReadyQueues = ksReadyQueues)) \<and> ((if tptr = ksCurThread then 1 else 0) = 0 \<longrightarrow> option_map2 tcbEPNext_C (clift t_hrsa) = option_map2 tcbEPNext_C (clift t_hrs) \<and> option_map2 tcbEPPrev_C (clift t_hrsa) = option_map2 tcbEPPrev_C (clift t_hrs) \<and> option_map2 tcbPriority_C (clift t_hrsa) = option_map2 tcbPriority_C (clift t_hrs) \<and> option_map2 tcbDomain_C (clift t_hrsa) = option_map2 tcbDomain_C (clift t_hrs) \<and> ksReadyQueues = ksReadyQueues)) proof (prove)
goal (1 subgoal):
 1. \<And>a b ksReadyQueues ksSchedulerAction tptr ts v aa ba thread_state. \<lbrakk>\<forall>x. ksSchedulerAction = tcb_Ptr x \<and> x \<noteq> 0 \<and> x \<noteq> 1 \<longrightarrow> (\<exists>d v. (\<exists>z. clift (a, b) (tcb_Ptr x) = Some z \<and> tcbPriority_C z = v) \<and> unat v \<le> Config_H.numPriorities \<and> (\<exists>z. clift (a, b) (tcb_Ptr x) = Some z \<and> tcbDomain_C z = d) \<and> unat d < numDomains \<and> (StateRelation_C.end_C (ksReadyQueues.[unat (d * 0x100 + v)]) \<noteq> NULL \<longrightarrow> (\<exists>y. clift (a, b) (head_C (ksReadyQueues.[unat (d * 0x100 + v)])) = Some y))); clift (a, b) tptr = Some v; thread_state_lift thread_state = thread_state_lift (tcbState_C v)\<lparr>tsType_CL := ts && mask 4\<rparr>; (aa, ba) = hrs_mem_update (heap_update tptr (tcbState_C_update (\<lambda>_. thread_state) v)) (a, b)\<rbrakk> \<Longrightarrow> (\<forall>x. map_option tcbEPNext_C (if x = tptr then Some (tcbState_C_update (\<lambda>_. thread_state) v) else clift (a, b) x) = map_option tcbEPNext_C (clift (a, b) x)) \<and> (\<forall>x. map_option tcbEPPrev_C (if x = tptr then Some (tcbState_C_update (\<lambda>_. thread_state) v) else clift (a, b) x) = map_option tcbEPPrev_C (clift (a, b) x)) \<and> (\<forall>x. map_option tcbPriority_C (if x = tptr then Some (tcbState_C_update (\<lambda>_. thread_state) v) else clift (a, b) x) = map_option tcbPriority_C (clift (a, b) x)) \<and> (\<forall>x. map_option tcbDomain_C (if x = tptr then Some (tcbState_C_update (\<lambda>_. thread_state) v) else clift (a, b) x) = map_option tcbDomain_C (clift (a, b) x))