theory IpcCancel_R

lemma sts_invs_minor'_no_valid_queues:
  "\<lbrace>st_tcb_at' (\<lambda>st'. tcb_st_refs_of' st' = tcb_st_refs_of' st
                   \<and> (st \<noteq> Inactive \<and> \<not> idle' st \<longrightarrow>
                      st' \<noteq> Inactive \<and> \<not> idle' st')) t
      and (\<lambda>s. t = ksIdleThread s \<longrightarrow> idle' st)
      and (\<lambda>s. runnable' st \<and> obj_at' tcbQueued t s \<longrightarrow> st_tcb_at' runnable' t s)
      and sch_act_simple
      and invs'\<rbrace>
    setThreadState st t
   \<lbrace>\<lambda>_ s. (\<forall>t' d p.
            (t' \<in> set(ksReadyQueues s (d, p)) \<longrightarrow>
             (obj_at' (\<lambda>tcb. tcbQueued tcb \<and> tcbDomain tcb = d \<and> tcbPriority tcb = p) t' s
              \<and> (t' \<noteq> t \<longrightarrow> st_tcb_at' runnable' t' s)))
            \<and> distinct (ksReadyQueues s (d, p)) \<and> (maxDomain < d \<or> maxPriority < p \<longrightarrow> ksReadyQueues s (d, p) = [])) \<and>
         valid_bitmapQ s \<and>
         bitmapQ_no_L2_orphans s \<and>
         bitmapQ_no_L1_orphans s \<and>
         valid_pspace' s \<and>
         sch_act_wf (ksSchedulerAction s) s \<and>
         sym_refs (state_refs_of' s) \<and>
         if_live_then_nonz_cap' s \<and>
         if_unsafe_then_cap' s \<and>
         valid_idle' s \<and>
         valid_global_refs' s \<and>
         valid_arch_state' s \<and>
         valid_irq_node' (irq_node' s) s \<and>
         valid_irq_handlers' s \<and>
         valid_irq_states' s \<and>
         valid_machine_state' s \<and>
         irqs_masked' s \<and>
         valid_queues' s \<and>
         ct_not_inQ s \<and>
         ct_idle_or_in_cur_domain' s \<and>
         valid_pde_mappings' s \<and>
         pspace_domain_valid s \<and>
         ksCurDomain s \<le> maxDomain \<and>
         valid_dom_schedule' s \<and>
         untyped_ranges_zero' s \<and>
         cur_tcb' s \<and>
         tcb_at' t s\<rbrace>" apply (simp add: invs'_def valid_state'_def valid_queues_def) apply (wp sts_valid_queues_partial sts_ksQ
            setThreadState_oa_queued sts_st_tcb_at'_cases
            irqs_masked_lift
            valid_irq_node_lift
            setThreadState_ct_not_inQ
            sts_valid_bitmapQ_sch_act_simple
            sts_valid_bitmapQ_no_L2_orphans_sch_act_simple
            sts_valid_bitmapQ_no_L1_orphans_sch_act_simple
            hoare_vcg_conj_lift hoare_vcg_imp_lift hoare_vcg_all_lift)+ apply (clarsimp simp: disj_imp) apply (intro conjI) apply (clarsimp simp: valid_queues_def) apply (rule conjI, clarsimp) apply (drule valid_queues_no_bitmap_objD, assumption) apply (clarsimp simp: inQ_def comp_def) apply (rule conjI) apply (erule obj_at'_weaken) apply (simp add: inQ_def) apply (clarsimp simp: st_tcb_at'_def) apply (erule obj_at'_weaken) apply (simp add: inQ_def) apply (simp add: valid_queues_no_bitmap_def) apply clarsimp apply (clarsimp simp: st_tcb_at'_def) apply (drule obj_at_valid_objs') apply (clarsimp simp: valid_pspace'_def) apply (clarsimp simp: valid_obj'_def valid_tcb'_def projectKOs) subgoal by (fastforce simp: valid_tcb_state'_def
                  split: Structures_H.thread_state.splits) apply (clarsimp dest!: st_tcb_at_state_refs_ofD'
                    elim!: rsubst[where P=sym_refs]
                   intro!: ext) apply (fastforce simp: valid_queues_def inQ_def pred_tcb_at' pred_tcb_at'_def
                   elim!: st_tcb_ex_cap'' obj_at'_weakenE)+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>st_tcb_at' (\<lambda>st'. tcb_st_refs_of' st' = tcb_st_refs_of' st \<and> (st \<noteq> Structures_H.thread_state.Inactive \<and> st \<noteq> Structures_H.thread_state.IdleThreadState \<longrightarrow> st' \<noteq> Structures_H.thread_state.Inactive \<and> st' \<noteq> Structures_H.thread_state.IdleThreadState)) t and (\<lambda>s. t = ksIdleThread s \<longrightarrow> idle' st) and (\<lambda>s. runnable' st \<and> obj_at' tcbQueued t s \<longrightarrow> st_tcb_at' runnable' t s) and sch_act_simple and invs'\<rbrace> setThreadState st t \<lbrace>\<lambda>_ s. (\<forall>t' d p. (t' \<in> set (ksReadyQueues s (d, p)) \<longrightarrow> obj_at' (\<lambda>tcb. tcbQueued tcb \<and> tcbDomain tcb = d \<and> tcbPriority tcb = p) t' s \<and> (t' \<noteq> t \<longrightarrow> st_tcb_at' runnable' t' s)) \<and> distinct (ksReadyQueues s (d, p)) \<and> (maxDomain < d \<or> maxPriority < p \<longrightarrow> ksReadyQueues s (d, p) = [])) \<and> valid_bitmapQ s \<and> bitmapQ_no_L2_orphans s \<and> bitmapQ_no_L1_orphans s \<and> valid_pspace' s \<and> sch_act_wf (ksSchedulerAction s) s \<and> sym_refs (state_refs_of' s) \<and> if_live_then_nonz_cap' s \<and> if_unsafe_then_cap' s \<and> valid_idle' s \<and> valid_global_refs' s \<and> valid_arch_state' s \<and> valid_irq_node' (irq_node' s) s \<and> valid_irq_handlers' s \<and> valid_irq_states' s \<and> valid_machine_state' s \<and> irqs_masked' s \<and> valid_queues' s \<and> ct_not_inQ s \<and> ct_idle_or_in_cur_domain' s \<and> valid_pde_mappings' s \<and> pspace_domain_valid s \<and> ksCurDomain s \<le> maxDomain \<and> valid_dom_schedule' s \<and> untyped_ranges_zero' s \<and> cur_tcb' s \<and> tcb_at' t s\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>st_tcb_at' (\<lambda>st'. tcb_st_refs_of' st' = tcb_st_refs_of' st \<and> (st \<noteq> Structures_H.thread_state.Inactive \<and> st \<noteq> Structures_H.thread_state.IdleThreadState \<longrightarrow> st' \<noteq> Structures_H.thread_state.Inactive \<and> st' \<noteq> Structures_H.thread_state.IdleThreadState)) t and (\<lambda>s. t = ksIdleThread s \<longrightarrow> idle' st) and (\<lambda>s. runnable' st \<and> obj_at' tcbQueued t s \<longrightarrow> st_tcb_at' runnable' t s) and sch_act_simple and ((\<lambda>s. valid_pspace' s \<and> sch_act_wf (ksSchedulerAction s) s \<and> valid_queues_no_bitmap s \<and> valid_bitmapQ s \<and> bitmapQ_no_L2_orphans s \<and> bitmapQ_no_L1_orphans s \<and> sym_refs (state_refs_of' s) \<and> if_live_then_nonz_cap' s \<and> if_unsafe_then_cap' s \<and> valid_idle' s \<and> valid_global_refs' s \<and> valid_arch_state' s \<and> valid_irq_node' (irq_node' s) s \<and> valid_irq_handlers' s \<and> valid_irq_states' s \<and> valid_machine_state' s \<and> irqs_masked' s \<and> valid_queues' s \<and> ct_not_inQ s \<and> ct_idle_or_in_cur_domain' s \<and> valid_pde_mappings' s \<and> pspace_domain_valid s \<and> ksCurDomain s \<le> maxDomain \<and> ksDomSchedule s \<noteq> [] \<and> (\<forall>x\<in>set (ksDomSchedule s). dschDomain x \<le> maxDomain \<and> 0 < dschLength x) \<and> ksDomSchedule s = ksDomSchedule (newKernelState undefined) \<and> ksDomScheduleIdx s < length (ksDomSchedule (newKernelState undefined)) \<and> untyped_ranges_zero' s) and cur_tcb')\<rbrace> setThreadState st t \<lbrace>\<lambda>_ s. (\<forall>t' d p. (t' \<in> set (ksReadyQueues s (d, p)) \<longrightarrow> obj_at' (\<lambda>tcb. tcbQueued tcb \<and> tcbDomain tcb = d \<and> tcbPriority tcb = p) t' s \<and> (t' \<noteq> t \<longrightarrow> st_tcb_at' runnable' t' s)) \<and> distinct (ksReadyQueues s (d, p)) \<and> (maxDomain < d \<longrightarrow> ksReadyQueues s (d, p) = []) \<and> (maxPriority < p \<longrightarrow> ksReadyQueues s (d, p) = [])) \<and> valid_bitmapQ s \<and> bitmapQ_no_L2_orphans s \<and> bitmapQ_no_L1_orphans s \<and> valid_pspace' s \<and> sch_act_wf (ksSchedulerAction s) s \<and> sym_refs (state_refs_of' s) \<and> if_live_then_nonz_cap' s \<and> if_unsafe_then_cap' s \<and> valid_idle' s \<and> valid_global_refs' s \<and> valid_arch_state' s \<and> valid_irq_node' (irq_node' s) s \<and> valid_irq_handlers' s \<and> valid_irq_states' s \<and> valid_machine_state' s \<and> irqs_masked' s \<and> valid_queues' s \<and> ct_not_inQ s \<and> ct_idle_or_in_cur_domain' s \<and> valid_pde_mappings' s \<and> pspace_domain_valid s \<and> ksCurDomain s \<le> maxDomain \<and> ksDomSchedule s \<noteq> [] \<and> (\<forall>x\<in>set (ksDomSchedule s). dschDomain x \<le> maxDomain \<and> 0 < dschLength x) \<and> ksDomSchedule s = ksDomSchedule (newKernelState undefined) \<and> ksDomScheduleIdx s < length (ksDomSchedule (newKernelState undefined)) \<and> untyped_ranges_zero' s \<and> cur_tcb' s \<and> tcb_at' t s\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s. (st_tcb_at' (\<lambda>st'. tcb_st_refs_of' st' = tcb_st_refs_of' st \<and> (st \<noteq> Structures_H.thread_state.Inactive \<and> st \<noteq> Structures_H.thread_state.IdleThreadState \<longrightarrow> st' \<noteq> Structures_H.thread_state.Inactive \<and> st' \<noteq> Structures_H.thread_state.IdleThreadState)) t and (\<lambda>s. t = ksIdleThread s \<longrightarrow> idle' st) and (\<lambda>s. runnable' st \<and> obj_at' tcbQueued t s \<longrightarrow> st_tcb_at' runnable' t s) and sch_act_simple and ((\<lambda>s. valid_pspace' s \<and> sch_act_wf (ksSchedulerAction s) s \<and> valid_queues_no_bitmap s \<and> valid_bitmapQ s \<and> bitmapQ_no_L2_orphans s \<and> bitmapQ_no_L1_orphans s \<and> sym_refs (state_refs_of' s) \<and> if_live_then_nonz_cap' s \<and> if_unsafe_then_cap' s \<and> valid_idle' s \<and> valid_global_refs' s \<and> valid_arch_state' s \<and> valid_irq_node' (irq_node' s) s \<and> valid_irq_handlers' s \<and> valid_irq_states' s \<and> valid_machine_state' s \<and> irqs_masked' s \<and> valid_queues' s \<and> ct_not_inQ s \<and> ct_idle_or_in_cur_domain' s \<and> valid_pde_mappings' s \<and> pspace_domain_valid s \<and> ksCurDomain s \<le> maxDomain \<and> ksDomSchedule s \<noteq> [] \<and> (\<forall>x\<in>set (ksDomSchedule s). dschDomain x \<le> maxDomain \<and> 0 < dschLength x) \<and> ksDomSchedule s = ksDomSchedule (newKernelState undefined) \<and> ksDomScheduleIdx s < length (ksDomSchedule (newKernelState undefined)) \<and> untyped_ranges_zero' s) and cur_tcb')) s \<Longrightarrow> (\<forall>x xa xb. (sch_act_simple s \<and> x \<notin> set (ksReadyQueues s (xa, xb)) \<or> obj_at' (\<lambda>tcb. tcbQueued tcb \<and> tcbDomain tcb = xa \<and> tcbPriority tcb = xb) x s \<and> (sch_act_simple s \<and> \<not> x \<noteq> t \<or> (t = x \<longrightarrow> runnable' st \<and> tcb_at' x s) \<and> (t \<noteq> x \<longrightarrow> st_tcb_at' runnable' x s))) \<and> sch_act_simple s \<and> distinct (ksReadyQueues s (xa, xb)) \<and> (maxDomain < xa \<longrightarrow> ksReadyQueues s (xa, xb) = []) \<and> (maxPriority < xb \<longrightarrow> ksReadyQueues s (xa, xb) = [])) \<and> (valid_bitmapQ and sch_act_simple) s \<and> (bitmapQ_no_L2_orphans and sch_act_simple) s \<and> (bitmapQ_no_L1_orphans and sch_act_simple) s \<and> (valid_pspace' and tcb_at' t and valid_tcb_state' st) s \<and> ((\<not> runnable' st \<longrightarrow> sch_act_simple s) \<and> sch_act_wf (ksSchedulerAction s) s) \<and> sym_refs ((state_refs_of' s)(t := tcb_st_refs_of' st \<union> {r \<in> state_refs_of' s t. snd r = TCBBound})) \<and> (if_live_then_nonz_cap' s \<and> (st \<noteq> Structures_H.thread_state.Inactive \<and> st \<noteq> Structures_H.thread_state.IdleThreadState \<longrightarrow> ex_nonz_cap_to' t s)) \<and> if_unsafe_then_cap' s \<and> (valid_idle' and valid_pspace' and (\<lambda>s. t = ksIdleThread s \<longrightarrow> idle' st)) s \<and> valid_global_refs' s \<and> valid_arch_state' s \<and> valid_irq_node' (irq_node' s) s \<and> valid_irq_handlers' s \<and> valid_irq_states' s \<and> valid_machine_state' s \<and> irqs_masked' s \<and> valid_queues' s \<and> ct_not_inQ s \<and> ct_idle_or_in_cur_domain' s \<and> valid_pde_mappings' s \<and> pspace_domain_valid s \<and> ksCurDomain s \<le> maxDomain \<and> ksDomSchedule s \<noteq> [] \<and> (\<forall>x\<in>set (ksDomSchedule s). dschDomain x \<le> maxDomain \<and> 0 < dschLength x) \<and> ksDomSchedule s = ksDomSchedule (newKernelState undefined) \<and> ksDomScheduleIdx s < length (ksDomSchedule (newKernelState undefined)) \<and> untyped_ranges_zero' s \<and> cur_tcb' s \<and> tcb_at' t s proof (prove)
goal (1 subgoal):
 1. \<And>s. \<lbrakk>st_tcb_at' (\<lambda>st'. tcb_st_refs_of' st' = tcb_st_refs_of' st \<and> (st \<noteq> Structures_H.thread_state.Inactive \<and> st \<noteq> Structures_H.thread_state.IdleThreadState \<longrightarrow> st' \<noteq> Structures_H.thread_state.Inactive \<and> st' \<noteq> Structures_H.thread_state.IdleThreadState)) t s; t = ksIdleThread s \<longrightarrow> idle' st; runnable' st \<and> obj_at' tcbQueued t s \<longrightarrow> st_tcb_at' runnable' t s; sch_act_simple s; valid_pspace' s; sch_act_wf (ksSchedulerAction s) s; valid_queues_no_bitmap s; valid_bitmapQ s; bitmapQ_no_L2_orphans s; bitmapQ_no_L1_orphans s; sym_refs (state_refs_of' s); if_live_then_nonz_cap' s; if_unsafe_then_cap' s; valid_idle' s; valid_global_refs' s; valid_arch_state' s; valid_irq_node' (irq_node' s) s; valid_irq_handlers' s; valid_irq_states' s; valid_machine_state' s; irqs_masked' s; valid_queues' s; ct_not_inQ s; ct_idle_or_in_cur_domain' s; valid_pde_mappings' s; pspace_domain_valid s; ksCurDomain s \<le> maxDomain; ksDomSchedule (newKernelState undefined) \<noteq> []; \<forall>x\<in>set (ksDomSchedule (newKernelState undefined)). dschDomain x \<le> maxDomain \<and> 0 < dschLength x; ksDomSchedule s = ksDomSchedule (newKernelState undefined); ksDomScheduleIdx s < length (ksDomSchedule (newKernelState undefined)); untyped_ranges_zero' s; cur_tcb' s\<rbrakk> \<Longrightarrow> (\<forall>x xa xb. (x \<in> set (ksReadyQueues s (xa, xb)) \<longrightarrow> obj_at' (\<lambda>tcb. tcbQueued tcb \<and> tcbDomain tcb = xa \<and> tcbPriority tcb = xb) x s \<and> (x \<noteq> t \<longrightarrow> st_tcb_at' runnable' x s)) \<and> distinct (ksReadyQueues s (xa, xb)) \<and> (maxDomain < xa \<longrightarrow> ksReadyQueues s (xa, xb) = []) \<and> (maxPriority < xb \<longrightarrow> ksReadyQueues s (xa, xb) = [])) \<and> tcb_at' t s \<and> valid_tcb_state' st s \<and> sym_refs (\<lambda>a. if a = t then tcb_st_refs_of' st \<union> {r \<in> state_refs_of' s t. snd r = TCBBound} else state_refs_of' s a) \<and> (st \<noteq> Structures_H.thread_state.Inactive \<and> st \<noteq> Structures_H.thread_state.IdleThreadState \<longrightarrow> ex_nonz_cap_to' t s) \<and> tcb_at' t s proof (prove)
goal (6 subgoals):
 1. \<And>s. \<lbrakk>st_tcb_at' (\<lambda>st'. tcb_st_refs_of' st' = tcb_st_refs_of' st \<and> (st \<noteq> Structures_H.thread_state.Inactive \<and> st \<noteq> Structures_H.thread_state.IdleThreadState \<longrightarrow> st' \<noteq> Structures_H.thread_state.Inactive \<and> st' \<noteq> Structures_H.thread_state.IdleThreadState)) t s; t = ksIdleThread s \<longrightarrow> idle' st; runnable' st \<and> obj_at' tcbQueued t s \<longrightarrow> st_tcb_at' runnable' t s; sch_act_simple s; valid_pspace' s; sch_act_wf (ksSchedulerAction s) s; valid_queues_no_bitmap s; valid_bitmapQ s; bitmapQ_no_L2_orphans s; bitmapQ_no_L1_orphans s; sym_refs (state_refs_of' s); if_live_then_nonz_cap' s; if_unsafe_then_cap' s; valid_idle' s; valid_global_refs' s; valid_arch_state' s; valid_irq_node' (irq_node' s) s; valid_irq_handlers' s; valid_irq_states' s; valid_machine_state' s; irqs_masked' s; valid_queues' s; ct_not_inQ s; ct_idle_or_in_cur_domain' s; valid_pde_mappings' s; pspace_domain_valid s; ksCurDomain s \<le> maxDomain; ksDomSchedule (newKernelState undefined) \<noteq> []; \<forall>x\<in>set (ksDomSchedule (newKernelState undefined)). dschDomain x \<le> maxDomain \<and> 0 < dschLength x; ksDomSchedule s = ksDomSchedule (newKernelState undefined); ksDomScheduleIdx s < length (ksDomSchedule (newKernelState undefined)); untyped_ranges_zero' s; cur_tcb' s\<rbrakk> \<Longrightarrow> \<forall>x xa xb. (x \<in> set (ksReadyQueues s (xa, xb)) \<longrightarrow> obj_at' (\<lambda>tcb. tcbQueued tcb \<and> tcbDomain tcb = xa \<and> tcbPriority tcb = xb) x s \<and> (x \<noteq> t \<longrightarrow> st_tcb_at' runnable' x s)) \<and> distinct (ksReadyQueues s (xa, xb)) \<and> (maxDomain < xa \<longrightarrow> ksReadyQueues s (xa, xb) = []) \<and> (maxPriority < xb \<longrightarrow> ksReadyQueues s (xa, xb) = [])
 2. \<And>s. \<lbrakk>st_tcb_at' (\<lambda>st'. tcb_st_refs_of' st' = tcb_st_refs_of' st \<and> (st \<noteq> Structures_H.thread_state.Inactive \<and> st \<noteq> Structures_H.thread_state.IdleThreadState \<longrightarrow> st' \<noteq> Structures_H.thread_state.Inactive \<and> st' \<noteq> Structures_H.thread_state.IdleThreadState)) t s; t = ksIdleThread s \<longrightarrow> idle' st; runnable' st \<and> obj_at' tcbQueued t s \<longrightarrow> st_tcb_at' runnable' t s; sch_act_simple s; valid_pspace' s; sch_act_wf (ksSchedulerAction s) s; valid_queues_no_bitmap s; valid_bitmapQ s; bitmapQ_no_L2_orphans s; bitmapQ_no_L1_orphans s; sym_refs (state_refs_of' s); if_live_then_nonz_cap' s; if_unsafe_then_cap' s; valid_idle' s; valid_global_refs' s; valid_arch_state' s; valid_irq_node' (irq_node' s) s; valid_irq_handlers' s; valid_irq_states' s; valid_machine_state' s; irqs_masked' s; valid_queues' s; ct_not_inQ s; ct_idle_or_in_cur_domain' s; valid_pde_mappings' s; pspace_domain_valid s; ksCurDomain s \<le> maxDomain; ksDomSchedule (newKernelState undefined) \<noteq> []; \<forall>x\<in>set (ksDomSchedule (newKernelState undefined)). dschDomain x \<le> maxDomain \<and> 0 < dschLength x; ksDomSchedule s = ksDomSchedule (newKernelState undefined); ksDomScheduleIdx s < length (ksDomSchedule (newKernelState undefined)); untyped_ranges_zero' s; cur_tcb' s\<rbrakk> \<Longrightarrow> tcb_at' t s
 3. \<And>s. \<lbrakk>st_tcb_at' (\<lambda>st'. tcb_st_refs_of' st' = tcb_st_refs_of' st \<and> (st \<noteq> Structures_H.thread_state.Inactive \<and> st \<noteq> Structures_H.thread_state.IdleThreadState \<longrightarrow> st' \<noteq> Structures_H.thread_state.Inactive \<and> st' \<noteq> Structures_H.thread_state.IdleThreadState)) t s; t = ksIdleThread s \<longrightarrow> idle' st; runnable' st \<and> obj_at' tcbQueued t s \<longrightarrow> st_tcb_at' runnable' t s; sch_act_simple s; valid_pspace' s; sch_act_wf (ksSchedulerAction s) s; valid_queues_no_bitmap s; valid_bitmapQ s; bitmapQ_no_L2_orphans s; bitmapQ_no_L1_orphans s; sym_refs (state_refs_of' s); if_live_then_nonz_cap' s; if_unsafe_then_cap' s; valid_idle' s; valid_global_refs' s; valid_arch_state' s; valid_irq_node' (irq_node' s) s; valid_irq_handlers' s; valid_irq_states' s; valid_machine_state' s; irqs_masked' s; valid_queues' s; ct_not_inQ s; ct_idle_or_in_cur_domain' s; valid_pde_mappings' s; pspace_domain_valid s; ksCurDomain s \<le> maxDomain; ksDomSchedule (newKernelState undefined) \<noteq> []; \<forall>x\<in>set (ksDomSchedule (newKernelState undefined)). dschDomain x \<le> maxDomain \<and> 0 < dschLength x; ksDomSchedule s = ksDomSchedule (newKernelState undefined); ksDomScheduleIdx s < length (ksDomSchedule (newKernelState undefined)); untyped_ranges_zero' s; cur_tcb' s\<rbrakk> \<Longrightarrow> valid_tcb_state' st s
 4. \<And>s. \<lbrakk>st_tcb_at' (\<lambda>st'. tcb_st_refs_of' st' = tcb_st_refs_of' st \<and> (st \<noteq> Structures_H.thread_state.Inactive \<and> st \<noteq> Structures_H.thread_state.IdleThreadState \<longrightarrow> st' \<noteq> Structures_H.thread_state.Inactive \<and> st' \<noteq> Structures_H.thread_state.IdleThreadState)) t s; t = ksIdleThread s \<longrightarrow> idle' st; runnable' st \<and> obj_at' tcbQueued t s \<longrightarrow> st_tcb_at' runnable' t s; sch_act_simple s; valid_pspace' s; sch_act_wf (ksSchedulerAction s) s; valid_queues_no_bitmap s; valid_bitmapQ s; bitmapQ_no_L2_orphans s; bitmapQ_no_L1_orphans s; sym_refs (state_refs_of' s); if_live_then_nonz_cap' s; if_unsafe_then_cap' s; valid_idle' s; valid_global_refs' s; valid_arch_state' s; valid_irq_node' (irq_node' s) s; valid_irq_handlers' s; valid_irq_states' s; valid_machine_state' s; irqs_masked' s; valid_queues' s; ct_not_inQ s; ct_idle_or_in_cur_domain' s; valid_pde_mappings' s; pspace_domain_valid s; ksCurDomain s \<le> maxDomain; ksDomSchedule (newKernelState undefined) \<noteq> []; \<forall>x\<in>set (ksDomSchedule (newKernelState undefined)). dschDomain x \<le> maxDomain \<and> 0 < dschLength x; ksDomSchedule s = ksDomSchedule (newKernelState undefined); ksDomScheduleIdx s < length (ksDomSchedule (newKernelState undefined)); untyped_ranges_zero' s; cur_tcb' s\<rbrakk> \<Longrightarrow> sym_refs (\<lambda>a. if a = t then tcb_st_refs_of' st \<union> {r \<in> state_refs_of' s t. snd r = TCBBound} else state_refs_of' s a)
 5. \<And>s. \<lbrakk>st_tcb_at' (\<lambda>st'. tcb_st_refs_of' st' = tcb_st_refs_of' st \<and> (st \<noteq> Structures_H.thread_state.Inactive \<and> st \<noteq> Structures_H.thread_state.IdleThreadState \<longrightarrow> st' \<noteq> Structures_H.thread_state.Inactive \<and> st' \<noteq> Structures_H.thread_state.IdleThreadState)) t s; t = ksIdleThread s \<longrightarrow> idle' st; runnable' st \<and> obj_at' tcbQueued t s \<longrightarrow> st_tcb_at' runnable' t s; sch_act_simple s; valid_pspace' s; sch_act_wf (ksSchedulerAction s) s; valid_queues_no_bitmap s; valid_bitmapQ s; bitmapQ_no_L2_orphans s; bitmapQ_no_L1_orphans s; sym_refs (state_refs_of' s); if_live_then_nonz_cap' s; if_unsafe_then_cap' s; valid_idle' s; valid_global_refs' s; valid_arch_state' s; valid_irq_node' (irq_node' s) s; valid_irq_handlers' s; valid_irq_states' s; valid_machine_state' s; irqs_masked' s; valid_queues' s; ct_not_inQ s; ct_idle_or_in_cur_domain' s; valid_pde_mappings' s; pspace_domain_valid s; ksCurDomain s \<le> maxDomain; ksDomSchedule (newKernelState undefined) \<noteq> []; \<forall>x\<in>set (ksDomSchedule (newKernelState undefined)). dschDomain x \<le> maxDomain \<and> 0 < dschLength x; ksDomSchedule s = ksDomSchedule (newKernelState undefined); ksDomScheduleIdx s < length (ksDomSchedule (newKernelState undefined)); untyped_ranges_zero' s; cur_tcb' s\<rbrakk> \<Longrightarrow> st \<noteq> Structures_H.thread_state.Inactive \<and> st \<noteq> Structures_H.thread_state.IdleThreadState \<longrightarrow> ex_nonz_cap_to' t s
 6. \<And>s. \<lbrakk>st_tcb_at' (\<lambda>st'. tcb_st_refs_of' st' = tcb_st_refs_of' st \<and> (st \<noteq> Structures_H.thread_state.Inactive \<and> st \<noteq> Structures_H.thread_state.IdleThreadState \<longrightarrow> st' \<noteq> Structures_H.thread_state.Inactive \<and> st' \<noteq> Structures_H.thread_state.IdleThreadState)) t s; t = ksIdleThread s \<longrightarrow> idle' st; runnable' st \<and> obj_at' tcbQueued t s \<longrightarrow> st_tcb_at' runnable' t s; sch_act_simple s; valid_pspace' s; sch_act_wf (ksSchedulerAction s) s; valid_queues_no_bitmap s; valid_bitmapQ s; bitmapQ_no_L2_orphans s; bitmapQ_no_L1_orphans s; sym_refs (state_refs_of' s); if_live_then_nonz_cap' s; if_unsafe_then_cap' s; valid_idle' s; valid_global_refs' s; valid_arch_state' s; valid_irq_node' (irq_node' s) s; valid_irq_handlers' s; valid_irq_states' s; valid_machine_state' s; irqs_masked' s; valid_queues' s; ct_not_inQ s; ct_idle_or_in_cur_domain' s; valid_pde_mappings' s; pspace_domain_valid s; ksCurDomain s \<le> maxDomain; ksDomSchedule (newKernelState undefined) \<noteq> []; \<forall>x\<in>set (ksDomSchedule (newKernelState undefined)). dschDomain x \<le> maxDomain \<and> 0 < dschLength x; ksDomSchedule s = ksDomSchedule (newKernelState undefined); ksDomScheduleIdx s < length (ksDomSchedule (newKernelState undefined)); untyped_ranges_zero' s; cur_tcb' s\<rbrakk> \<Longrightarrow> tcb_at' t s proof (prove)
goal (6 subgoals):
 1. \<And>s x xa xb. \<lbrakk>st_tcb_at' (\<lambda>st'. tcb_st_refs_of' st' = tcb_st_refs_of' st \<and> (st \<noteq> Structures_H.thread_state.Inactive \<and> st \<noteq> Structures_H.thread_state.IdleThreadState \<longrightarrow> st' \<noteq> Structures_H.thread_state.Inactive \<and> st' \<noteq> Structures_H.thread_state.IdleThreadState)) t s; t = ksIdleThread s \<longrightarrow> idle' st; runnable' st \<and> obj_at' tcbQueued t s \<longrightarrow> st_tcb_at' runnable' t s; sch_act_simple s; valid_pspace' s; sch_act_wf (ksSchedulerAction s) s; valid_queues_no_bitmap s; valid_bitmapQ s; bitmapQ_no_L2_orphans s; bitmapQ_no_L1_orphans s; sym_refs (state_refs_of' s); if_live_then_nonz_cap' s; if_unsafe_then_cap' s; valid_idle' s; valid_global_refs' s; valid_arch_state' s; valid_irq_node' (irq_node' s) s; valid_irq_handlers' s; valid_irq_states' s; valid_machine_state' s; irqs_masked' s; valid_queues' s; ct_not_inQ s; ct_idle_or_in_cur_domain' s; valid_pde_mappings' s; pspace_domain_valid s; ksCurDomain s \<le> maxDomain; ksDomSchedule (newKernelState undefined) \<noteq> []; \<forall>x\<in>set (ksDomSchedule (newKernelState undefined)). dschDomain x \<le> maxDomain \<and> 0 < dschLength x; ksDomSchedule s = ksDomSchedule (newKernelState undefined); ksDomScheduleIdx s < length (ksDomSchedule (newKernelState undefined)); untyped_ranges_zero' s; cur_tcb' s\<rbrakk> \<Longrightarrow> (x \<in> set (ksReadyQueues s (xa, xb)) \<longrightarrow> obj_at' (\<lambda>tcb. tcbQueued tcb \<and> tcbDomain tcb = xa \<and> tcbPriority tcb = xb) x s \<and> (x \<noteq> t \<longrightarrow> st_tcb_at' runnable' x s)) \<and> distinct (ksReadyQueues s (xa, xb)) \<and> (maxDomain < xa \<longrightarrow> ksReadyQueues s (xa, xb) = []) \<and> (maxPriority < xb \<longrightarrow> ksReadyQueues s (xa, xb) = [])
 2. \<And>s. \<lbrakk>st_tcb_at' (\<lambda>st'. tcb_st_refs_of' st' = tcb_st_refs_of' st \<and> (st \<noteq> Structures_H.thread_state.Inactive \<and> st \<noteq> Structures_H.thread_state.IdleThreadState \<longrightarrow> st' \<noteq> Structures_H.thread_state.Inactive \<and> st' \<noteq> Structures_H.thread_state.IdleThreadState)) t s; t = ksIdleThread s \<longrightarrow> idle' st; runnable' st \<and> obj_at' tcbQueued t s \<longrightarrow> st_tcb_at' runnable' t s; sch_act_simple s; valid_pspace' s; sch_act_wf (ksSchedulerAction s) s; valid_queues_no_bitmap s; valid_bitmapQ s; bitmapQ_no_L2_orphans s; bitmapQ_no_L1_orphans s; sym_refs (state_refs_of' s); if_live_then_nonz_cap' s; if_unsafe_then_cap' s; valid_idle' s; valid_global_refs' s; valid_arch_state' s; valid_irq_node' (irq_node' s) s; valid_irq_handlers' s; valid_irq_states' s; valid_machine_state' s; irqs_masked' s; valid_queues' s; ct_not_inQ s; ct_idle_or_in_cur_domain' s; valid_pde_mappings' s; pspace_domain_valid s; ksCurDomain s \<le> maxDomain; ksDomSchedule (newKernelState undefined) \<noteq> []; \<forall>x\<in>set (ksDomSchedule (newKernelState undefined)). dschDomain x \<le> maxDomain \<and> 0 < dschLength x; ksDomSchedule s = ksDomSchedule (newKernelState undefined); ksDomScheduleIdx s < length (ksDomSchedule (newKernelState undefined)); untyped_ranges_zero' s; cur_tcb' s\<rbrakk> \<Longrightarrow> tcb_at' t s
 3. \<And>s. \<lbrakk>st_tcb_at' (\<lambda>st'. tcb_st_refs_of' st' = tcb_st_refs_of' st \<and> (st \<noteq> Structures_H.thread_state.Inactive \<and> st \<noteq> Structures_H.thread_state.IdleThreadState \<longrightarrow> st' \<noteq> Structures_H.thread_state.Inactive \<and> st' \<noteq> Structures_H.thread_state.IdleThreadState)) t s; t = ksIdleThread s \<longrightarrow> idle' st; runnable' st \<and> obj_at' tcbQueued t s \<longrightarrow> st_tcb_at' runnable' t s; sch_act_simple s; valid_pspace' s; sch_act_wf (ksSchedulerAction s) s; valid_queues_no_bitmap s; valid_bitmapQ s; bitmapQ_no_L2_orphans s; bitmapQ_no_L1_orphans s; sym_refs (state_refs_of' s); if_live_then_nonz_cap' s; if_unsafe_then_cap' s; valid_idle' s; valid_global_refs' s; valid_arch_state' s; valid_irq_node' (irq_node' s) s; valid_irq_handlers' s; valid_irq_states' s; valid_machine_state' s; irqs_masked' s; valid_queues' s; ct_not_inQ s; ct_idle_or_in_cur_domain' s; valid_pde_mappings' s; pspace_domain_valid s; ksCurDomain s \<le> maxDomain; ksDomSchedule (newKernelState undefined) \<noteq> []; \<forall>x\<in>set (ksDomSchedule (newKernelState undefined)). dschDomain x \<le> maxDomain \<and> 0 < dschLength x; ksDomSchedule s = ksDomSchedule (newKernelState undefined); ksDomScheduleIdx s < length (ksDomSchedule (newKernelState undefined)); untyped_ranges_zero' s; cur_tcb' s\<rbrakk> \<Longrightarrow> valid_tcb_state' st s
 4. \<And>s. \<lbrakk>st_tcb_at' (\<lambda>st'. tcb_st_refs_of' st' = tcb_st_refs_of' st \<and> (st \<noteq> Structures_H.thread_state.Inactive \<and> st \<noteq> Structures_H.thread_state.IdleThreadState \<longrightarrow> st' \<noteq> Structures_H.thread_state.Inactive \<and> st' \<noteq> Structures_H.thread_state.IdleThreadState)) t s; t = ksIdleThread s \<longrightarrow> idle' st; runnable' st \<and> obj_at' tcbQueued t s \<longrightarrow> st_tcb_at' runnable' t s; sch_act_simple s; valid_pspace' s; sch_act_wf (ksSchedulerAction s) s; valid_queues_no_bitmap s; valid_bitmapQ s; bitmapQ_no_L2_orphans s; bitmapQ_no_L1_orphans s; sym_refs (state_refs_of' s); if_live_then_nonz_cap' s; if_unsafe_then_cap' s; valid_idle' s; valid_global_refs' s; valid_arch_state' s; valid_irq_node' (irq_node' s) s; valid_irq_handlers' s; valid_irq_states' s; valid_machine_state' s; irqs_masked' s; valid_queues' s; ct_not_inQ s; ct_idle_or_in_cur_domain' s; valid_pde_mappings' s; pspace_domain_valid s; ksCurDomain s \<le> maxDomain; ksDomSchedule (newKernelState undefined) \<noteq> []; \<forall>x\<in>set (ksDomSchedule (newKernelState undefined)). dschDomain x \<le> maxDomain \<and> 0 < dschLength x; ksDomSchedule s = ksDomSchedule (newKernelState undefined); ksDomScheduleIdx s < length (ksDomSchedule (newKernelState undefined)); untyped_ranges_zero' s; cur_tcb' s\<rbrakk> \<Longrightarrow> sym_refs (\<lambda>a. if a = t then tcb_st_refs_of' st \<union> {r \<in> state_refs_of' s t. snd r = TCBBound} else state_refs_of' s a)
 5. \<And>s. \<lbrakk>st_tcb_at' (\<lambda>st'. tcb_st_refs_of' st' = tcb_st_refs_of' st \<and> (st \<noteq> Structures_H.thread_state.Inactive \<and> st \<noteq> Structures_H.thread_state.IdleThreadState \<longrightarrow> st' \<noteq> Structures_H.thread_state.Inactive \<and> st' \<noteq> Structures_H.thread_state.IdleThreadState)) t s; t = ksIdleThread s \<longrightarrow> idle' st; runnable' st \<and> obj_at' tcbQueued t s \<longrightarrow> st_tcb_at' runnable' t s; sch_act_simple s; valid_pspace' s; sch_act_wf (ksSchedulerAction s) s; valid_queues_no_bitmap s; valid_bitmapQ s; bitmapQ_no_L2_orphans s; bitmapQ_no_L1_orphans s; sym_refs (state_refs_of' s); if_live_then_nonz_cap' s; if_unsafe_then_cap' s; valid_idle' s; valid_global_refs' s; valid_arch_state' s; valid_irq_node' (irq_node' s) s; valid_irq_handlers' s; valid_irq_states' s; valid_machine_state' s; irqs_masked' s; valid_queues' s; ct_not_inQ s; ct_idle_or_in_cur_domain' s; valid_pde_mappings' s; pspace_domain_valid s; ksCurDomain s \<le> maxDomain; ksDomSchedule (newKernelState undefined) \<noteq> []; \<forall>x\<in>set (ksDomSchedule (newKernelState undefined)). dschDomain x \<le> maxDomain \<and> 0 < dschLength x; ksDomSchedule s = ksDomSchedule (newKernelState undefined); ksDomScheduleIdx s < length (ksDomSchedule (newKernelState undefined)); untyped_ranges_zero' s; cur_tcb' s\<rbrakk> \<Longrightarrow> st \<noteq> Structures_H.thread_state.Inactive \<and> st \<noteq> Structures_H.thread_state.IdleThreadState \<longrightarrow> ex_nonz_cap_to' t s
 6. \<And>s. \<lbrakk>st_tcb_at' (\<lambda>st'. tcb_st_refs_of' st' = tcb_st_refs_of' st \<and> (st \<noteq> Structures_H.thread_state.Inactive \<and> st \<noteq> Structures_H.thread_state.IdleThreadState \<longrightarrow> st' \<noteq> Structures_H.thread_state.Inactive \<and> st' \<noteq> Structures_H.thread_state.IdleThreadState)) t s; t = ksIdleThread s \<longrightarrow> idle' st; runnable' st \<and> obj_at' tcbQueued t s \<longrightarrow> st_tcb_at' runnable' t s; sch_act_simple s; valid_pspace' s; sch_act_wf (ksSchedulerAction s) s; valid_queues_no_bitmap s; valid_bitmapQ s; bitmapQ_no_L2_orphans s; bitmapQ_no_L1_orphans s; sym_refs (state_refs_of' s); if_live_then_nonz_cap' s; if_unsafe_then_cap' s; valid_idle' s; valid_global_refs' s; valid_arch_state' s; valid_irq_node' (irq_node' s) s; valid_irq_handlers' s; valid_irq_states' s; valid_machine_state' s; irqs_masked' s; valid_queues' s; ct_not_inQ s; ct_idle_or_in_cur_domain' s; valid_pde_mappings' s; pspace_domain_valid s; ksCurDomain s \<le> maxDomain; ksDomSchedule (newKernelState undefined) \<noteq> []; \<forall>x\<in>set (ksDomSchedule (newKernelState undefined)). dschDomain x \<le> maxDomain \<and> 0 < dschLength x; ksDomSchedule s = ksDomSchedule (newKernelState undefined); ksDomScheduleIdx s < length (ksDomSchedule (newKernelState undefined)); untyped_ranges_zero' s; cur_tcb' s\<rbrakk> \<Longrightarrow> tcb_at' t s proof (prove)
goal (7 subgoals):
 1. \<And>s x xa xb. \<lbrakk>st_tcb_at' (\<lambda>st'. tcb_st_refs_of' st' = tcb_st_refs_of' st \<and> (st \<noteq> Structures_H.thread_state.Inactive \<and> st \<noteq> Structures_H.thread_state.IdleThreadState \<longrightarrow> st' \<noteq> Structures_H.thread_state.Inactive \<and> st' \<noteq> Structures_H.thread_state.IdleThreadState)) t s; t = ksIdleThread s \<longrightarrow> idle' st; runnable' st \<and> obj_at' tcbQueued t s \<longrightarrow> st_tcb_at' runnable' t s; sch_act_simple s; valid_pspace' s; sch_act_wf (ksSchedulerAction s) s; valid_queues_no_bitmap s; valid_bitmapQ s; bitmapQ_no_L2_orphans s; bitmapQ_no_L1_orphans s; sym_refs (state_refs_of' s); if_live_then_nonz_cap' s; if_unsafe_then_cap' s; valid_idle' s; valid_global_refs' s; valid_arch_state' s; valid_irq_node' (irq_node' s) s; valid_irq_handlers' s; valid_irq_states' s; valid_machine_state' s; irqs_masked' s; valid_queues' s; ct_not_inQ s; ct_idle_or_in_cur_domain' s; valid_pde_mappings' s; pspace_domain_valid s; ksCurDomain s \<le> maxDomain; ksDomSchedule (newKernelState undefined) \<noteq> []; \<forall>x\<in>set (ksDomSchedule (newKernelState undefined)). dschDomain x \<le> maxDomain \<and> 0 < dschLength x; ksDomSchedule s = ksDomSchedule (newKernelState undefined); ksDomScheduleIdx s < length (ksDomSchedule (newKernelState undefined)); untyped_ranges_zero' s; cur_tcb' s; x \<in> set (ksReadyQueues s (xa, xb))\<rbrakk> \<Longrightarrow> obj_at' (\<lambda>tcb. tcbQueued tcb \<and> tcbDomain tcb = xa \<and> tcbPriority tcb = xb) x s \<and> (x \<noteq> t \<longrightarrow> st_tcb_at' runnable' x s)
 2. \<And>s x xa xb. \<lbrakk>st_tcb_at' (\<lambda>st'. tcb_st_refs_of' st' = tcb_st_refs_of' st \<and> (st \<noteq> Structures_H.thread_state.Inactive \<and> st \<noteq> Structures_H.thread_state.IdleThreadState \<longrightarrow> st' \<noteq> Structures_H.thread_state.Inactive \<and> st' \<noteq> Structures_H.thread_state.IdleThreadState)) t s; t = ksIdleThread s \<longrightarrow> idle' st; runnable' st \<and> obj_at' tcbQueued t s \<longrightarrow> st_tcb_at' runnable' t s; sch_act_simple s; valid_pspace' s; sch_act_wf (ksSchedulerAction s) s; valid_queues_no_bitmap s; valid_bitmapQ s; bitmapQ_no_L2_orphans s; bitmapQ_no_L1_orphans s; sym_refs (state_refs_of' s); if_live_then_nonz_cap' s; if_unsafe_then_cap' s; valid_idle' s; valid_global_refs' s; valid_arch_state' s; valid_irq_node' (irq_node' s) s; valid_irq_handlers' s; valid_irq_states' s; valid_machine_state' s; irqs_masked' s; valid_queues' s; ct_not_inQ s; ct_idle_or_in_cur_domain' s; valid_pde_mappings' s; pspace_domain_valid s; ksCurDomain s \<le> maxDomain; ksDomSchedule (newKernelState undefined) \<noteq> []; \<forall>x\<in>set (ksDomSchedule (newKernelState undefined)). dschDomain x \<le> maxDomain \<and> 0 < dschLength x; ksDomSchedule s = ksDomSchedule (newKernelState undefined); ksDomScheduleIdx s < length (ksDomSchedule (newKernelState undefined)); untyped_ranges_zero' s; cur_tcb' s\<rbrakk> \<Longrightarrow> distinct (ksReadyQueues s (xa, xb)) \<and> (maxDomain < xa \<longrightarrow> ksReadyQueues s (xa, xb) = []) \<and> (maxPriority < xb \<longrightarrow> ksReadyQueues s (xa, xb) = [])
 3. \<And>s. \<lbrakk>st_tcb_at' (\<lambda>st'. tcb_st_refs_of' st' = tcb_st_refs_of' st \<and> (st \<noteq> Structures_H.thread_state.Inactive \<and> st \<noteq> Structures_H.thread_state.IdleThreadState \<longrightarrow> st' \<noteq> Structures_H.thread_state.Inactive \<and> st' \<noteq> Structures_H.thread_state.IdleThreadState)) t s; t = ksIdleThread s \<longrightarrow> idle' st; runnable' st \<and> obj_at' tcbQueued t s \<longrightarrow> st_tcb_at' runnable' t s; sch_act_simple s; valid_pspace' s; sch_act_wf (ksSchedulerAction s) s; valid_queues_no_bitmap s; valid_bitmapQ s; bitmapQ_no_L2_orphans s; bitmapQ_no_L1_orphans s; sym_refs (state_refs_of' s); if_live_then_nonz_cap' s; if_unsafe_then_cap' s; valid_idle' s; valid_global_refs' s; valid_arch_state' s; valid_irq_node' (irq_node' s) s; valid_irq_handlers' s; valid_irq_states' s; valid_machine_state' s; irqs_masked' s; valid_queues' s; ct_not_inQ s; ct_idle_or_in_cur_domain' s; valid_pde_mappings' s; pspace_domain_valid s; ksCurDomain s \<le> maxDomain; ksDomSchedule (newKernelState undefined) \<noteq> []; \<forall>x\<in>set (ksDomSchedule (newKernelState undefined)). dschDomain x \<le> maxDomain \<and> 0 < dschLength x; ksDomSchedule s = ksDomSchedule (newKernelState undefined); ksDomScheduleIdx s < length (ksDomSchedule (newKernelState undefined)); untyped_ranges_zero' s; cur_tcb' s\<rbrakk> \<Longrightarrow> tcb_at' t s
 4. \<And>s. \<lbrakk>st_tcb_at' (\<lambda>st'. tcb_st_refs_of' st' = tcb_st_refs_of' st \<and> (st \<noteq> Structures_H.thread_state.Inactive \<and> st \<noteq> Structures_H.thread_state.IdleThreadState \<longrightarrow> st' \<noteq> Structures_H.thread_state.Inactive \<and> st' \<noteq> Structures_H.thread_state.IdleThreadState)) t s; t = ksIdleThread s \<longrightarrow> idle' st; runnable' st \<and> obj_at' tcbQueued t s \<longrightarrow> st_tcb_at' runnable' t s; sch_act_simple s; valid_pspace' s; sch_act_wf (ksSchedulerAction s) s; valid_queues_no_bitmap s; valid_bitmapQ s; bitmapQ_no_L2_orphans s; bitmapQ_no_L1_orphans s; sym_refs (state_refs_of' s); if_live_then_nonz_cap' s; if_unsafe_then_cap' s; valid_idle' s; valid_global_refs' s; valid_arch_state' s; valid_irq_node' (irq_node' s) s; valid_irq_handlers' s; valid_irq_states' s; valid_machine_state' s; irqs_masked' s; valid_queues' s; ct_not_inQ s; ct_idle_or_in_cur_domain' s; valid_pde_mappings' s; pspace_domain_valid s; ksCurDomain s \<le> maxDomain; ksDomSchedule (newKernelState undefined) \<noteq> []; \<forall>x\<in>set (ksDomSchedule (newKernelState undefined)). dschDomain x \<le> maxDomain \<and> 0 < dschLength x; ksDomSchedule s = ksDomSchedule (newKernelState undefined); ksDomScheduleIdx s < length (ksDomSchedule (newKernelState undefined)); untyped_ranges_zero' s; cur_tcb' s\<rbrakk> \<Longrightarrow> valid_tcb_state' st s
 5. \<And>s. \<lbrakk>st_tcb_at' (\<lambda>st'. tcb_st_refs_of' st' = tcb_st_refs_of' st \<and> (st \<noteq> Structures_H.thread_state.Inactive \<and> st \<noteq> Structures_H.thread_state.IdleThreadState \<longrightarrow> st' \<noteq> Structures_H.thread_state.Inactive \<and> st' \<noteq> Structures_H.thread_state.IdleThreadState)) t s; t = ksIdleThread s \<longrightarrow> idle' st; runnable' st \<and> obj_at' tcbQueued t s \<longrightarrow> st_tcb_at' runnable' t s; sch_act_simple s; valid_pspace' s; sch_act_wf (ksSchedulerAction s) s; valid_queues_no_bitmap s; valid_bitmapQ s; bitmapQ_no_L2_orphans s; bitmapQ_no_L1_orphans s; sym_refs (state_refs_of' s); if_live_then_nonz_cap' s; if_unsafe_then_cap' s; valid_idle' s; valid_global_refs' s; valid_arch_state' s; valid_irq_node' (irq_node' s) s; valid_irq_handlers' s; valid_irq_states' s; valid_machine_state' s; irqs_masked' s; valid_queues' s; ct_not_inQ s; ct_idle_or_in_cur_domain' s; valid_pde_mappings' s; pspace_domain_valid s; ksCurDomain s \<le> maxDomain; ksDomSchedule (newKernelState undefined) \<noteq> []; \<forall>x\<in>set (ksDomSchedule (newKernelState undefined)). dschDomain x \<le> maxDomain \<and> 0 < dschLength x; ksDomSchedule s = ksDomSchedule (newKernelState undefined); ksDomScheduleIdx s < length (ksDomSchedule (newKernelState undefined)); untyped_ranges_zero' s; cur_tcb' s\<rbrakk> \<Longrightarrow> sym_refs (\<lambda>a. if a = t then tcb_st_refs_of' st \<union> {r \<in> state_refs_of' s t. snd r = TCBBound} else state_refs_of' s a)
 6. \<And>s. \<lbrakk>st_tcb_at' (\<lambda>st'. tcb_st_refs_of' st' = tcb_st_refs_of' st \<and> (st \<noteq> Structures_H.thread_state.Inactive \<and> st \<noteq> Structures_H.thread_state.IdleThreadState \<longrightarrow> st' \<noteq> Structures_H.thread_state.Inactive \<and> st' \<noteq> Structures_H.thread_state.IdleThreadState)) t s; t = ksIdleThread s \<longrightarrow> idle' st; runnable' st \<and> obj_at' tcbQueued t s \<longrightarrow> st_tcb_at' runnable' t s; sch_act_simple s; valid_pspace' s; sch_act_wf (ksSchedulerAction s) s; valid_queues_no_bitmap s; valid_bitmapQ s; bitmapQ_no_L2_orphans s; bitmapQ_no_L1_orphans s; sym_refs (state_refs_of' s); if_live_then_nonz_cap' s; if_unsafe_then_cap' s; valid_idle' s; valid_global_refs' s; valid_arch_state' s; valid_irq_node' (irq_node' s) s; valid_irq_handlers' s; valid_irq_states' s; valid_machine_state' s; irqs_masked' s; valid_queues' s; ct_not_inQ s; ct_idle_or_in_cur_domain' s; valid_pde_mappings' s; pspace_domain_valid s; ksCurDomain s \<le> maxDomain; ksDomSchedule (newKernelState undefined) \<noteq> []; \<forall>x\<in>set (ksDomSchedule (newKernelState undefined)). dschDomain x \<le> maxDomain \<and> 0 < dschLength x; ksDomSchedule s = ksDomSchedule (newKernelState undefined); ksDomScheduleIdx s < length (ksDomSchedule (newKernelState undefined)); untyped_ranges_zero' s; cur_tcb' s\<rbrakk> \<Longrightarrow> st \<noteq> Structures_H.thread_state.Inactive \<and> st \<noteq> Structures_H.thread_state.IdleThreadState \<longrightarrow> ex_nonz_cap_to' t s
 7. \<And>s. \<lbrakk>st_tcb_at' (\<lambda>st'. tcb_st_refs_of' st' = tcb_st_refs_of' st \<and> (st \<noteq> Structures_H.thread_state.Inactive \<and> st \<noteq> Structures_H.thread_state.IdleThreadState \<longrightarrow> st' \<noteq> Structures_H.thread_state.Inactive \<and> st' \<noteq> Structures_H.thread_state.IdleThreadState)) t s; t = ksIdleThread s \<longrightarrow> idle' st; runnable' st \<and> obj_at' tcbQueued t s \<longrightarrow> st_tcb_at' runnable' t s; sch_act_simple s; valid_pspace' s; sch_act_wf (ksSchedulerAction s) s; valid_queues_no_bitmap s; valid_bitmapQ s; bitmapQ_no_L2_orphans s; bitmapQ_no_L1_orphans s; sym_refs (state_refs_of' s); if_live_then_nonz_cap' s; if_unsafe_then_cap' s; valid_idle' s; valid_global_refs' s; valid_arch_state' s; valid_irq_node' (irq_node' s) s; valid_irq_handlers' s; valid_irq_states' s; valid_machine_state' s; irqs_masked' s; valid_queues' s; ct_not_inQ s; ct_idle_or_in_cur_domain' s; valid_pde_mappings' s; pspace_domain_valid s; ksCurDomain s \<le> maxDomain; ksDomSchedule (newKernelState undefined) \<noteq> []; \<forall>x\<in>set (ksDomSchedule (newKernelState undefined)). dschDomain x \<le> maxDomain \<and> 0 < dschLength x; ksDomSchedule s = ksDomSchedule (newKernelState undefined); ksDomScheduleIdx s < length (ksDomSchedule (newKernelState undefined)); untyped_ranges_zero' s; cur_tcb' s\<rbrakk> \<Longrightarrow> tcb_at' t s proof (prove)
goal (7 subgoals):
 1. \<And>s x xa xb. \<lbrakk>st_tcb_at' (\<lambda>st'. tcb_st_refs_of' st' = tcb_st_refs_of' st \<and> (st \<noteq> Structures_H.thread_state.Inactive \<and> st \<noteq> Structures_H.thread_state.IdleThreadState \<longrightarrow> st' \<noteq> Structures_H.thread_state.Inactive \<and> st' \<noteq> Structures_H.thread_state.IdleThreadState)) t s; t = ksIdleThread s \<longrightarrow> idle' st; runnable' st \<and> obj_at' tcbQueued t s \<longrightarrow> st_tcb_at' runnable' t s; sch_act_simple s; valid_pspace' s; sch_act_wf (ksSchedulerAction s) s; valid_bitmapQ s; bitmapQ_no_L2_orphans s; bitmapQ_no_L1_orphans s; sym_refs (state_refs_of' s); if_live_then_nonz_cap' s; if_unsafe_then_cap' s; valid_idle' s; valid_global_refs' s; valid_arch_state' s; valid_irq_node' (irq_node' s) s; valid_irq_handlers' s; valid_irq_states' s; valid_machine_state' s; irqs_masked' s; valid_queues' s; ct_not_inQ s; ct_idle_or_in_cur_domain' s; valid_pde_mappings' s; pspace_domain_valid s; ksCurDomain s \<le> maxDomain; ksDomSchedule (newKernelState undefined) \<noteq> []; \<forall>x\<in>set (ksDomSchedule (newKernelState undefined)). dschDomain x \<le> maxDomain \<and> 0 < dschLength x; ksDomSchedule s = ksDomSchedule (newKernelState undefined); ksDomScheduleIdx s < length (ksDomSchedule (newKernelState undefined)); untyped_ranges_zero' s; cur_tcb' s; x \<in> set (ksReadyQueues s (xa, xb)); obj_at' (inQ xa xb and runnable' \<circ> tcbState) x s\<rbrakk> \<Longrightarrow> obj_at' (\<lambda>tcb. tcbQueued tcb \<and> tcbDomain tcb = xa \<and> tcbPriority tcb = xb) x s \<and> (x \<noteq> t \<longrightarrow> st_tcb_at' runnable' x s)
 2. \<And>s x xa xb. \<lbrakk>st_tcb_at' (\<lambda>st'. tcb_st_refs_of' st' = tcb_st_refs_of' st \<and> (st \<noteq> Structures_H.thread_state.Inactive \<and> st \<noteq> Structures_H.thread_state.IdleThreadState \<longrightarrow> st' \<noteq> Structures_H.thread_state.Inactive \<and> st' \<noteq> Structures_H.thread_state.IdleThreadState)) t s; t = ksIdleThread s \<longrightarrow> idle' st; runnable' st \<and> obj_at' tcbQueued t s \<longrightarrow> st_tcb_at' runnable' t s; sch_act_simple s; valid_pspace' s; sch_act_wf (ksSchedulerAction s) s; valid_queues_no_bitmap s; valid_bitmapQ s; bitmapQ_no_L2_orphans s; bitmapQ_no_L1_orphans s; sym_refs (state_refs_of' s); if_live_then_nonz_cap' s; if_unsafe_then_cap' s; valid_idle' s; valid_global_refs' s; valid_arch_state' s; valid_irq_node' (irq_node' s) s; valid_irq_handlers' s; valid_irq_states' s; valid_machine_state' s; irqs_masked' s; valid_queues' s; ct_not_inQ s; ct_idle_or_in_cur_domain' s; valid_pde_mappings' s; pspace_domain_valid s; ksCurDomain s \<le> maxDomain; ksDomSchedule (newKernelState undefined) \<noteq> []; \<forall>x\<in>set (ksDomSchedule (newKernelState undefined)). dschDomain x \<le> maxDomain \<and> 0 < dschLength x; ksDomSchedule s = ksDomSchedule (newKernelState undefined); ksDomScheduleIdx s < length (ksDomSchedule (newKernelState undefined)); untyped_ranges_zero' s; cur_tcb' s\<rbrakk> \<Longrightarrow> distinct (ksReadyQueues s (xa, xb)) \<and> (maxDomain < xa \<longrightarrow> ksReadyQueues s (xa, xb) = []) \<and> (maxPriority < xb \<longrightarrow> ksReadyQueues s (xa, xb) = [])
 3. \<And>s. \<lbrakk>st_tcb_at' (\<lambda>st'. tcb_st_refs_of' st' = tcb_st_refs_of' st \<and> (st \<noteq> Structures_H.thread_state.Inactive \<and> st \<noteq> Structures_H.thread_state.IdleThreadState \<longrightarrow> st' \<noteq> Structures_H.thread_state.Inactive \<and> st' \<noteq> Structures_H.thread_state.IdleThreadState)) t s; t = ksIdleThread s \<longrightarrow> idle' st; runnable' st \<and> obj_at' tcbQueued t s \<longrightarrow> st_tcb_at' runnable' t s; sch_act_simple s; valid_pspace' s; sch_act_wf (ksSchedulerAction s) s; valid_queues_no_bitmap s; valid_bitmapQ s; bitmapQ_no_L2_orphans s; bitmapQ_no_L1_orphans s; sym_refs (state_refs_of' s); if_live_then_nonz_cap' s; if_unsafe_then_cap' s; valid_idle' s; valid_global_refs' s; valid_arch_state' s; valid_irq_node' (irq_node' s) s; valid_irq_handlers' s; valid_irq_states' s; valid_machine_state' s; irqs_masked' s; valid_queues' s; ct_not_inQ s; ct_idle_or_in_cur_domain' s; valid_pde_mappings' s; pspace_domain_valid s; ksCurDomain s \<le> maxDomain; ksDomSchedule (newKernelState undefined) \<noteq> []; \<forall>x\<in>set (ksDomSchedule (newKernelState undefined)). dschDomain x \<le> maxDomain \<and> 0 < dschLength x; ksDomSchedule s = ksDomSchedule (newKernelState undefined); ksDomScheduleIdx s < length (ksDomSchedule (newKernelState undefined)); untyped_ranges_zero' s; cur_tcb' s\<rbrakk> \<Longrightarrow> tcb_at' t s
 4. \<And>s. \<lbrakk>st_tcb_at' (\<lambda>st'. tcb_st_refs_of' st' = tcb_st_refs_of' st \<and> (st \<noteq> Structures_H.thread_state.Inactive \<and> st \<noteq> Structures_H.thread_state.IdleThreadState \<longrightarrow> st' \<noteq> Structures_H.thread_state.Inactive \<and> st' \<noteq> Structures_H.thread_state.IdleThreadState)) t s; t = ksIdleThread s \<longrightarrow> idle' st; runnable' st \<and> obj_at' tcbQueued t s \<longrightarrow> st_tcb_at' runnable' t s; sch_act_simple s; valid_pspace' s; sch_act_wf (ksSchedulerAction s) s; valid_queues_no_bitmap s; valid_bitmapQ s; bitmapQ_no_L2_orphans s; bitmapQ_no_L1_orphans s; sym_refs (state_refs_of' s); if_live_then_nonz_cap' s; if_unsafe_then_cap' s; valid_idle' s; valid_global_refs' s; valid_arch_state' s; valid_irq_node' (irq_node' s) s; valid_irq_handlers' s; valid_irq_states' s; valid_machine_state' s; irqs_masked' s; valid_queues' s; ct_not_inQ s; ct_idle_or_in_cur_domain' s; valid_pde_mappings' s; pspace_domain_valid s; ksCurDomain s \<le> maxDomain; ksDomSchedule (newKernelState undefined) \<noteq> []; \<forall>x\<in>set (ksDomSchedule (newKernelState undefined)). dschDomain x \<le> maxDomain \<and> 0 < dschLength x; ksDomSchedule s = ksDomSchedule (newKernelState undefined); ksDomScheduleIdx s < length (ksDomSchedule (newKernelState undefined)); untyped_ranges_zero' s; cur_tcb' s\<rbrakk> \<Longrightarrow> valid_tcb_state' st s
 5. \<And>s. \<lbrakk>st_tcb_at' (\<lambda>st'. tcb_st_refs_of' st' = tcb_st_refs_of' st \<and> (st \<noteq> Structures_H.thread_state.Inactive \<and> st \<noteq> Structures_H.thread_state.IdleThreadState \<longrightarrow> st' \<noteq> Structures_H.thread_state.Inactive \<and> st' \<noteq> Structures_H.thread_state.IdleThreadState)) t s; t = ksIdleThread s \<longrightarrow> idle' st; runnable' st \<and> obj_at' tcbQueued t s \<longrightarrow> st_tcb_at' runnable' t s; sch_act_simple s; valid_pspace' s; sch_act_wf (ksSchedulerAction s) s; valid_queues_no_bitmap s; valid_bitmapQ s; bitmapQ_no_L2_orphans s; bitmapQ_no_L1_orphans s; sym_refs (state_refs_of' s); if_live_then_nonz_cap' s; if_unsafe_then_cap' s; valid_idle' s; valid_global_refs' s; valid_arch_state' s; valid_irq_node' (irq_node' s) s; valid_irq_handlers' s; valid_irq_states' s; valid_machine_state' s; irqs_masked' s; valid_queues' s; ct_not_inQ s; ct_idle_or_in_cur_domain' s; valid_pde_mappings' s; pspace_domain_valid s; ksCurDomain s \<le> maxDomain; ksDomSchedule (newKernelState undefined) \<noteq> []; \<forall>x\<in>set (ksDomSchedule (newKernelState undefined)). dschDomain x \<le> maxDomain \<and> 0 < dschLength x; ksDomSchedule s = ksDomSchedule (newKernelState undefined); ksDomScheduleIdx s < length (ksDomSchedule (newKernelState undefined)); untyped_ranges_zero' s; cur_tcb' s\<rbrakk> \<Longrightarrow> sym_refs (\<lambda>a. if a = t then tcb_st_refs_of' st \<union> {r \<in> state_refs_of' s t. snd r = TCBBound} else state_refs_of' s a)
 6. \<And>s. \<lbrakk>st_tcb_at' (\<lambda>st'. tcb_st_refs_of' st' = tcb_st_refs_of' st \<and> (st \<noteq> Structures_H.thread_state.Inactive \<and> st \<noteq> Structures_H.thread_state.IdleThreadState \<longrightarrow> st' \<noteq> Structures_H.thread_state.Inactive \<and> st' \<noteq> Structures_H.thread_state.IdleThreadState)) t s; t = ksIdleThread s \<longrightarrow> idle' st; runnable' st \<and> obj_at' tcbQueued t s \<longrightarrow> st_tcb_at' runnable' t s; sch_act_simple s; valid_pspace' s; sch_act_wf (ksSchedulerAction s) s; valid_queues_no_bitmap s; valid_bitmapQ s; bitmapQ_no_L2_orphans s; bitmapQ_no_L1_orphans s; sym_refs (state_refs_of' s); if_live_then_nonz_cap' s; if_unsafe_then_cap' s; valid_idle' s; valid_global_refs' s; valid_arch_state' s; valid_irq_node' (irq_node' s) s; valid_irq_handlers' s; valid_irq_states' s; valid_machine_state' s; irqs_masked' s; valid_queues' s; ct_not_inQ s; ct_idle_or_in_cur_domain' s; valid_pde_mappings' s; pspace_domain_valid s; ksCurDomain s \<le> maxDomain; ksDomSchedule (newKernelState undefined) \<noteq> []; \<forall>x\<in>set (ksDomSchedule (newKernelState undefined)). dschDomain x \<le> maxDomain \<and> 0 < dschLength x; ksDomSchedule s = ksDomSchedule (newKernelState undefined); ksDomScheduleIdx s < length (ksDomSchedule (newKernelState undefined)); untyped_ranges_zero' s; cur_tcb' s\<rbrakk> \<Longrightarrow> st \<noteq> Structures_H.thread_state.Inactive \<and> st \<noteq> Structures_H.thread_state.IdleThreadState \<longrightarrow> ex_nonz_cap_to' t s
 7. \<And>s. \<lbrakk>st_tcb_at' (\<lambda>st'. tcb_st_refs_of' st' = tcb_st_refs_of' st \<and> (st \<noteq> Structures_H.thread_state.Inactive \<and> st \<noteq> Structures_H.thread_state.IdleThreadState \<longrightarrow> st' \<noteq> Structures_H.thread_state.Inactive \<and> st' \<noteq> Structures_H.thread_state.IdleThreadState)) t s; t = ksIdleThread s \<longrightarrow> idle' st; runnable' st \<and> obj_at' tcbQueued t s \<longrightarrow> st_tcb_at' runnable' t s; sch_act_simple s; valid_pspace' s; sch_act_wf (ksSchedulerAction s) s; valid_queues_no_bitmap s; valid_bitmapQ s; bitmapQ_no_L2_orphans s; bitmapQ_no_L1_orphans s; sym_refs (state_refs_of' s); if_live_then_nonz_cap' s; if_unsafe_then_cap' s; valid_idle' s; valid_global_refs' s; valid_arch_state' s; valid_irq_node' (irq_node' s) s; valid_irq_handlers' s; valid_irq_states' s; valid_machine_state' s; irqs_masked' s; valid_queues' s; ct_not_inQ s; ct_idle_or_in_cur_domain' s; valid_pde_mappings' s; pspace_domain_valid s; ksCurDomain s \<le> maxDomain; ksDomSchedule (newKernelState undefined) \<noteq> []; \<forall>x\<in>set (ksDomSchedule (newKernelState undefined)). dschDomain x \<le> maxDomain \<and> 0 < dschLength x; ksDomSchedule s = ksDomSchedule (newKernelState undefined); ksDomScheduleIdx s < length (ksDomSchedule (newKernelState undefined)); untyped_ranges_zero' s; cur_tcb' s\<rbrakk> \<Longrightarrow> tcb_at' t s proof (prove)
goal (7 subgoals):
 1. \<And>s x xa xb. \<lbrakk>st_tcb_at' (\<lambda>st'. tcb_st_refs_of' st' = tcb_st_refs_of' st \<and> (st \<noteq> Structures_H.thread_state.Inactive \<and> st \<noteq> Structures_H.thread_state.IdleThreadState \<longrightarrow> st' \<noteq> Structures_H.thread_state.Inactive \<and> st' \<noteq> Structures_H.thread_state.IdleThreadState)) t s; t = ksIdleThread s \<longrightarrow> idle' st; runnable' st \<and> obj_at' tcbQueued t s \<longrightarrow> st_tcb_at' runnable' t s; sch_act_simple s; valid_pspace' s; sch_act_wf (ksSchedulerAction s) s; valid_bitmapQ s; bitmapQ_no_L2_orphans s; bitmapQ_no_L1_orphans s; sym_refs (state_refs_of' s); if_live_then_nonz_cap' s; if_unsafe_then_cap' s; valid_idle' s; valid_global_refs' s; valid_arch_state' s; valid_irq_node' (irq_node' s) s; valid_irq_handlers' s; valid_irq_states' s; valid_machine_state' s; irqs_masked' s; valid_queues' s; ct_not_inQ s; ct_idle_or_in_cur_domain' s; valid_pde_mappings' s; pspace_domain_valid s; ksCurDomain s \<le> maxDomain; ksDomSchedule (newKernelState undefined) \<noteq> []; \<forall>x\<in>set (ksDomSchedule (newKernelState undefined)). dschDomain x \<le> maxDomain \<and> 0 < dschLength x; ksDomSchedule s = ksDomSchedule (newKernelState undefined); ksDomScheduleIdx s < length (ksDomSchedule (newKernelState undefined)); untyped_ranges_zero' s; cur_tcb' s; x \<in> set (ksReadyQueues s (xa, xb)); obj_at' (inQ xa xb and (\<lambda>x. runnable' (tcbState x))) x s\<rbrakk> \<Longrightarrow> obj_at' (\<lambda>tcb. tcbQueued tcb \<and> tcbDomain tcb = xa \<and> tcbPriority tcb = xb) x s \<and> (x \<noteq> t \<longrightarrow> st_tcb_at' runnable' x s)
 2. \<And>s x xa xb. \<lbrakk>st_tcb_at' (\<lambda>st'. tcb_st_refs_of' st' = tcb_st_refs_of' st \<and> (st \<noteq> Structures_H.thread_state.Inactive \<and> st \<noteq> Structures_H.thread_state.IdleThreadState \<longrightarrow> st' \<noteq> Structures_H.thread_state.Inactive \<and> st' \<noteq> Structures_H.thread_state.IdleThreadState)) t s; t = ksIdleThread s \<longrightarrow> idle' st; runnable' st \<and> obj_at' tcbQueued t s \<longrightarrow> st_tcb_at' runnable' t s; sch_act_simple s; valid_pspace' s; sch_act_wf (ksSchedulerAction s) s; valid_queues_no_bitmap s; valid_bitmapQ s; bitmapQ_no_L2_orphans s; bitmapQ_no_L1_orphans s; sym_refs (state_refs_of' s); if_live_then_nonz_cap' s; if_unsafe_then_cap' s; valid_idle' s; valid_global_refs' s; valid_arch_state' s; valid_irq_node' (irq_node' s) s; valid_irq_handlers' s; valid_irq_states' s; valid_machine_state' s; irqs_masked' s; valid_queues' s; ct_not_inQ s; ct_idle_or_in_cur_domain' s; valid_pde_mappings' s; pspace_domain_valid s; ksCurDomain s \<le> maxDomain; ksDomSchedule (newKernelState undefined) \<noteq> []; \<forall>x\<in>set (ksDomSchedule (newKernelState undefined)). dschDomain x \<le> maxDomain \<and> 0 < dschLength x; ksDomSchedule s = ksDomSchedule (newKernelState undefined); ksDomScheduleIdx s < length (ksDomSchedule (newKernelState undefined)); untyped_ranges_zero' s; cur_tcb' s\<rbrakk> \<Longrightarrow> distinct (ksReadyQueues s (xa, xb)) \<and> (maxDomain < xa \<longrightarrow> ksReadyQueues s (xa, xb) = []) \<and> (maxPriority < xb \<longrightarrow> ksReadyQueues s (xa, xb) = [])
 3. \<And>s. \<lbrakk>st_tcb_at' (\<lambda>st'. tcb_st_refs_of' st' = tcb_st_refs_of' st \<and> (st \<noteq> Structures_H.thread_state.Inactive \<and> st \<noteq> Structures_H.thread_state.IdleThreadState \<longrightarrow> st' \<noteq> Structures_H.thread_state.Inactive \<and> st' \<noteq> Structures_H.thread_state.IdleThreadState)) t s; t = ksIdleThread s \<longrightarrow> idle' st; runnable' st \<and> obj_at' tcbQueued t s \<longrightarrow> st_tcb_at' runnable' t s; sch_act_simple s; valid_pspace' s; sch_act_wf (ksSchedulerAction s) s; valid_queues_no_bitmap s; valid_bitmapQ s; bitmapQ_no_L2_orphans s; bitmapQ_no_L1_orphans s; sym_refs (state_refs_of' s); if_live_then_nonz_cap' s; if_unsafe_then_cap' s; valid_idle' s; valid_global_refs' s; valid_arch_state' s; valid_irq_node' (irq_node' s) s; valid_irq_handlers' s; valid_irq_states' s; valid_machine_state' s; irqs_masked' s; valid_queues' s; ct_not_inQ s; ct_idle_or_in_cur_domain' s; valid_pde_mappings' s; pspace_domain_valid s; ksCurDomain s \<le> maxDomain; ksDomSchedule (newKernelState undefined) \<noteq> []; \<forall>x\<in>set (ksDomSchedule (newKernelState undefined)). dschDomain x \<le> maxDomain \<and> 0 < dschLength x; ksDomSchedule s = ksDomSchedule (newKernelState undefined); ksDomScheduleIdx s < length (ksDomSchedule (newKernelState undefined)); untyped_ranges_zero' s; cur_tcb' s\<rbrakk> \<Longrightarrow> tcb_at' t s
 4. \<And>s. \<lbrakk>st_tcb_at' (\<lambda>st'. tcb_st_refs_of' st' = tcb_st_refs_of' st \<and> (st \<noteq> Structures_H.thread_state.Inactive \<and> st \<noteq> Structures_H.thread_state.IdleThreadState \<longrightarrow> st' \<noteq> Structures_H.thread_state.Inactive \<and> st' \<noteq> Structures_H.thread_state.IdleThreadState)) t s; t = ksIdleThread s \<longrightarrow> idle' st; runnable' st \<and> obj_at' tcbQueued t s \<longrightarrow> st_tcb_at' runnable' t s; sch_act_simple s; valid_pspace' s; sch_act_wf (ksSchedulerAction s) s; valid_queues_no_bitmap s; valid_bitmapQ s; bitmapQ_no_L2_orphans s; bitmapQ_no_L1_orphans s; sym_refs (state_refs_of' s); if_live_then_nonz_cap' s; if_unsafe_then_cap' s; valid_idle' s; valid_global_refs' s; valid_arch_state' s; valid_irq_node' (irq_node' s) s; valid_irq_handlers' s; valid_irq_states' s; valid_machine_state' s; irqs_masked' s; valid_queues' s; ct_not_inQ s; ct_idle_or_in_cur_domain' s; valid_pde_mappings' s; pspace_domain_valid s; ksCurDomain s \<le> maxDomain; ksDomSchedule (newKernelState undefined) \<noteq> []; \<forall>x\<in>set (ksDomSchedule (newKernelState undefined)). dschDomain x \<le> maxDomain \<and> 0 < dschLength x; ksDomSchedule s = ksDomSchedule (newKernelState undefined); ksDomScheduleIdx s < length (ksDomSchedule (newKernelState undefined)); untyped_ranges_zero' s; cur_tcb' s\<rbrakk> \<Longrightarrow> valid_tcb_state' st s
 5. \<And>s. \<lbrakk>st_tcb_at' (\<lambda>st'. tcb_st_refs_of' st' = tcb_st_refs_of' st \<and> (st \<noteq> Structures_H.thread_state.Inactive \<and> st \<noteq> Structures_H.thread_state.IdleThreadState \<longrightarrow> st' \<noteq> Structures_H.thread_state.Inactive \<and> st' \<noteq> Structures_H.thread_state.IdleThreadState)) t s; t = ksIdleThread s \<longrightarrow> idle' st; runnable' st \<and> obj_at' tcbQueued t s \<longrightarrow> st_tcb_at' runnable' t s; sch_act_simple s; valid_pspace' s; sch_act_wf (ksSchedulerAction s) s; valid_queues_no_bitmap s; valid_bitmapQ s; bitmapQ_no_L2_orphans s; bitmapQ_no_L1_orphans s; sym_refs (state_refs_of' s); if_live_then_nonz_cap' s; if_unsafe_then_cap' s; valid_idle' s; valid_global_refs' s; valid_arch_state' s; valid_irq_node' (irq_node' s) s; valid_irq_handlers' s; valid_irq_states' s; valid_machine_state' s; irqs_masked' s; valid_queues' s; ct_not_inQ s; ct_idle_or_in_cur_domain' s; valid_pde_mappings' s; pspace_domain_valid s; ksCurDomain s \<le> maxDomain; ksDomSchedule (newKernelState undefined) \<noteq> []; \<forall>x\<in>set (ksDomSchedule (newKernelState undefined)). dschDomain x \<le> maxDomain \<and> 0 < dschLength x; ksDomSchedule s = ksDomSchedule (newKernelState undefined); ksDomScheduleIdx s < length (ksDomSchedule (newKernelState undefined)); untyped_ranges_zero' s; cur_tcb' s\<rbrakk> \<Longrightarrow> sym_refs (\<lambda>a. if a = t then tcb_st_refs_of' st \<union> {r \<in> state_refs_of' s t. snd r = TCBBound} else state_refs_of' s a)
 6. \<And>s. \<lbrakk>st_tcb_at' (\<lambda>st'. tcb_st_refs_of' st' = tcb_st_refs_of' st \<and> (st \<noteq> Structures_H.thread_state.Inactive \<and> st \<noteq> Structures_H.thread_state.IdleThreadState \<longrightarrow> st' \<noteq> Structures_H.thread_state.Inactive \<and> st' \<noteq> Structures_H.thread_state.IdleThreadState)) t s; t = ksIdleThread s \<longrightarrow> idle' st; runnable' st \<and> obj_at' tcbQueued t s \<longrightarrow> st_tcb_at' runnable' t s; sch_act_simple s; valid_pspace' s; sch_act_wf (ksSchedulerAction s) s; valid_queues_no_bitmap s; valid_bitmapQ s; bitmapQ_no_L2_orphans s; bitmapQ_no_L1_orphans s; sym_refs (state_refs_of' s); if_live_then_nonz_cap' s; if_unsafe_then_cap' s; valid_idle' s; valid_global_refs' s; valid_arch_state' s; valid_irq_node' (irq_node' s) s; valid_irq_handlers' s; valid_irq_states' s; valid_machine_state' s; irqs_masked' s; valid_queues' s; ct_not_inQ s; ct_idle_or_in_cur_domain' s; valid_pde_mappings' s; pspace_domain_valid s; ksCurDomain s \<le> maxDomain; ksDomSchedule (newKernelState undefined) \<noteq> []; \<forall>x\<in>set (ksDomSchedule (newKernelState undefined)). dschDomain x \<le> maxDomain \<and> 0 < dschLength x; ksDomSchedule s = ksDomSchedule (newKernelState undefined); ksDomScheduleIdx s < length (ksDomSchedule (newKernelState undefined)); untyped_ranges_zero' s; cur_tcb' s\<rbrakk> \<Longrightarrow> st \<noteq> Structures_H.thread_state.Inactive \<and> st \<noteq> Structures_H.thread_state.IdleThreadState \<longrightarrow> ex_nonz_cap_to' t s
 7. \<And>s. \<lbrakk>st_tcb_at' (\<lambda>st'. tcb_st_refs_of' st' = tcb_st_refs_of' st \<and> (st \<noteq> Structures_H.thread_state.Inactive \<and> st \<noteq> Structures_H.thread_state.IdleThreadState \<longrightarrow> st' \<noteq> Structures_H.thread_state.Inactive \<and> st' \<noteq> Structures_H.thread_state.IdleThreadState)) t s; t = ksIdleThread s \<longrightarrow> idle' st; runnable' st \<and> obj_at' tcbQueued t s \<longrightarrow> st_tcb_at' runnable' t s; sch_act_simple s; valid_pspace' s; sch_act_wf (ksSchedulerAction s) s; valid_queues_no_bitmap s; valid_bitmapQ s; bitmapQ_no_L2_orphans s; bitmapQ_no_L1_orphans s; sym_refs (state_refs_of' s); if_live_then_nonz_cap' s; if_unsafe_then_cap' s; valid_idle' s; valid_global_refs' s; valid_arch_state' s; valid_irq_node' (irq_node' s) s; valid_irq_handlers' s; valid_irq_states' s; valid_machine_state' s; irqs_masked' s; valid_queues' s; ct_not_inQ s; ct_idle_or_in_cur_domain' s; valid_pde_mappings' s; pspace_domain_valid s; ksCurDomain s \<le> maxDomain; ksDomSchedule (newKernelState undefined) \<noteq> []; \<forall>x\<in>set (ksDomSchedule (newKernelState undefined)). dschDomain x \<le> maxDomain \<and> 0 < dschLength x; ksDomSchedule s = ksDomSchedule (newKernelState undefined); ksDomScheduleIdx s < length (ksDomSchedule (newKernelState undefined)); untyped_ranges_zero' s; cur_tcb' s\<rbrakk> \<Longrightarrow> tcb_at' t s proof (prove)
goal (8 subgoals):
 1. \<And>s x xa xb. \<lbrakk>st_tcb_at' (\<lambda>st'. tcb_st_refs_of' st' = tcb_st_refs_of' st \<and> (st \<noteq> Structures_H.thread_state.Inactive \<and> st \<noteq> Structures_H.thread_state.IdleThreadState \<longrightarrow> st' \<noteq> Structures_H.thread_state.Inactive \<and> st' \<noteq> Structures_H.thread_state.IdleThreadState)) t s; t = ksIdleThread s \<longrightarrow> idle' st; runnable' st \<and> obj_at' tcbQueued t s \<longrightarrow> st_tcb_at' runnable' t s; sch_act_simple s; valid_pspace' s; sch_act_wf (ksSchedulerAction s) s; valid_bitmapQ s; bitmapQ_no_L2_orphans s; bitmapQ_no_L1_orphans s; sym_refs (state_refs_of' s); if_live_then_nonz_cap' s; if_unsafe_then_cap' s; valid_idle' s; valid_global_refs' s; valid_arch_state' s; valid_irq_node' (irq_node' s) s; valid_irq_handlers' s; valid_irq_states' s; valid_machine_state' s; irqs_masked' s; valid_queues' s; ct_not_inQ s; ct_idle_or_in_cur_domain' s; valid_pde_mappings' s; pspace_domain_valid s; ksCurDomain s \<le> maxDomain; ksDomSchedule (newKernelState undefined) \<noteq> []; \<forall>x\<in>set (ksDomSchedule (newKernelState undefined)). dschDomain x \<le> maxDomain \<and> 0 < dschLength x; ksDomSchedule s = ksDomSchedule (newKernelState undefined); ksDomScheduleIdx s < length (ksDomSchedule (newKernelState undefined)); untyped_ranges_zero' s; cur_tcb' s; x \<in> set (ksReadyQueues s (xa, xb)); obj_at' (inQ xa xb and (\<lambda>x. runnable' (tcbState x))) x s\<rbrakk> \<Longrightarrow> obj_at' (\<lambda>tcb. tcbQueued tcb \<and> tcbDomain tcb = xa \<and> tcbPriority tcb = xb) x s
 2. \<And>s x xa xb. \<lbrakk>st_tcb_at' (\<lambda>st'. tcb_st_refs_of' st' = tcb_st_refs_of' st \<and> (st \<noteq> Structures_H.thread_state.Inactive \<and> st \<noteq> Structures_H.thread_state.IdleThreadState \<longrightarrow> st' \<noteq> Structures_H.thread_state.Inactive \<and> st' \<noteq> Structures_H.thread_state.IdleThreadState)) t s; t = ksIdleThread s \<longrightarrow> idle' st; runnable' st \<and> obj_at' tcbQueued t s \<longrightarrow> st_tcb_at' runnable' t s; sch_act_simple s; valid_pspace' s; sch_act_wf (ksSchedulerAction s) s; valid_bitmapQ s; bitmapQ_no_L2_orphans s; bitmapQ_no_L1_orphans s; sym_refs (state_refs_of' s); if_live_then_nonz_cap' s; if_unsafe_then_cap' s; valid_idle' s; valid_global_refs' s; valid_arch_state' s; valid_irq_node' (irq_node' s) s; valid_irq_handlers' s; valid_irq_states' s; valid_machine_state' s; irqs_masked' s; valid_queues' s; ct_not_inQ s; ct_idle_or_in_cur_domain' s; valid_pde_mappings' s; pspace_domain_valid s; ksCurDomain s \<le> maxDomain; ksDomSchedule (newKernelState undefined) \<noteq> []; \<forall>x\<in>set (ksDomSchedule (newKernelState undefined)). dschDomain x \<le> maxDomain \<and> 0 < dschLength x; ksDomSchedule s = ksDomSchedule (newKernelState undefined); ksDomScheduleIdx s < length (ksDomSchedule (newKernelState undefined)); untyped_ranges_zero' s; cur_tcb' s; x \<in> set (ksReadyQueues s (xa, xb)); obj_at' (inQ xa xb and (\<lambda>x. runnable' (tcbState x))) x s\<rbrakk> \<Longrightarrow> x \<noteq> t \<longrightarrow> st_tcb_at' runnable' x s
 3. \<And>s x xa xb. \<lbrakk>st_tcb_at' (\<lambda>st'. tcb_st_refs_of' st' = tcb_st_refs_of' st \<and> (st \<noteq> Structures_H.thread_state.Inactive \<and> st \<noteq> Structures_H.thread_state.IdleThreadState \<longrightarrow> st' \<noteq> Structures_H.thread_state.Inactive \<and> st' \<noteq> Structures_H.thread_state.IdleThreadState)) t s; t = ksIdleThread s \<longrightarrow> idle' st; runnable' st \<and> obj_at' tcbQueued t s \<longrightarrow> st_tcb_at' runnable' t s; sch_act_simple s; valid_pspace' s; sch_act_wf (ksSchedulerAction s) s; valid_queues_no_bitmap s; valid_bitmapQ s; bitmapQ_no_L2_orphans s; bitmapQ_no_L1_orphans s; sym_refs (state_refs_of' s); if_live_then_nonz_cap' s; if_unsafe_then_cap' s; valid_idle' s; valid_global_refs' s; valid_arch_state' s; valid_irq_node' (irq_node' s) s; valid_irq_handlers' s; valid_irq_states' s; valid_machine_state' s; irqs_masked' s; valid_queues' s; ct_not_inQ s; ct_idle_or_in_cur_domain' s; valid_pde_mappings' s; pspace_domain_valid s; ksCurDomain s \<le> maxDomain; ksDomSchedule (newKernelState undefined) \<noteq> []; \<forall>x\<in>set (ksDomSchedule (newKernelState undefined)). dschDomain x \<le> maxDomain \<and> 0 < dschLength x; ksDomSchedule s = ksDomSchedule (newKernelState undefined); ksDomScheduleIdx s < length (ksDomSchedule (newKernelState undefined)); untyped_ranges_zero' s; cur_tcb' s\<rbrakk> \<Longrightarrow> distinct (ksReadyQueues s (xa, xb)) \<and> (maxDomain < xa \<longrightarrow> ksReadyQueues s (xa, xb) = []) \<and> (maxPriority < xb \<longrightarrow> ksReadyQueues s (xa, xb) = [])
 4. \<And>s. \<lbrakk>st_tcb_at' (\<lambda>st'. tcb_st_refs_of' st' = tcb_st_refs_of' st \<and> (st \<noteq> Structures_H.thread_state.Inactive \<and> st \<noteq> Structures_H.thread_state.IdleThreadState \<longrightarrow> st' \<noteq> Structures_H.thread_state.Inactive \<and> st' \<noteq> Structures_H.thread_state.IdleThreadState)) t s; t = ksIdleThread s \<longrightarrow> idle' st; runnable' st \<and> obj_at' tcbQueued t s \<longrightarrow> st_tcb_at' runnable' t s; sch_act_simple s; valid_pspace' s; sch_act_wf (ksSchedulerAction s) s; valid_queues_no_bitmap s; valid_bitmapQ s; bitmapQ_no_L2_orphans s; bitmapQ_no_L1_orphans s; sym_refs (state_refs_of' s); if_live_then_nonz_cap' s; if_unsafe_then_cap' s; valid_idle' s; valid_global_refs' s; valid_arch_state' s; valid_irq_node' (irq_node' s) s; valid_irq_handlers' s; valid_irq_states' s; valid_machine_state' s; irqs_masked' s; valid_queues' s; ct_not_inQ s; ct_idle_or_in_cur_domain' s; valid_pde_mappings' s; pspace_domain_valid s; ksCurDomain s \<le> maxDomain; ksDomSchedule (newKernelState undefined) \<noteq> []; \<forall>x\<in>set (ksDomSchedule (newKernelState undefined)). dschDomain x \<le> maxDomain \<and> 0 < dschLength x; ksDomSchedule s = ksDomSchedule (newKernelState undefined); ksDomScheduleIdx s < length (ksDomSchedule (newKernelState undefined)); untyped_ranges_zero' s; cur_tcb' s\<rbrakk> \<Longrightarrow> tcb_at' t s
 5. \<And>s. \<lbrakk>st_tcb_at' (\<lambda>st'. tcb_st_refs_of' st' = tcb_st_refs_of' st \<and> (st \<noteq> Structures_H.thread_state.Inactive \<and> st \<noteq> Structures_H.thread_state.IdleThreadState \<longrightarrow> st' \<noteq> Structures_H.thread_state.Inactive \<and> st' \<noteq> Structures_H.thread_state.IdleThreadState)) t s; t = ksIdleThread s \<longrightarrow> idle' st; runnable' st \<and> obj_at' tcbQueued t s \<longrightarrow> st_tcb_at' runnable' t s; sch_act_simple s; valid_pspace' s; sch_act_wf (ksSchedulerAction s) s; valid_queues_no_bitmap s; valid_bitmapQ s; bitmapQ_no_L2_orphans s; bitmapQ_no_L1_orphans s; sym_refs (state_refs_of' s); if_live_then_nonz_cap' s; if_unsafe_then_cap' s; valid_idle' s; valid_global_refs' s; valid_arch_state' s; valid_irq_node' (irq_node' s) s; valid_irq_handlers' s; valid_irq_states' s; valid_machine_state' s; irqs_masked' s; valid_queues' s; ct_not_inQ s; ct_idle_or_in_cur_domain' s; valid_pde_mappings' s; pspace_domain_valid s; ksCurDomain s \<le> maxDomain; ksDomSchedule (newKernelState undefined) \<noteq> []; \<forall>x\<in>set (ksDomSchedule (newKernelState undefined)). dschDomain x \<le> maxDomain \<and> 0 < dschLength x; ksDomSchedule s = ksDomSchedule (newKernelState undefined); ksDomScheduleIdx s < length (ksDomSchedule (newKernelState undefined)); untyped_ranges_zero' s; cur_tcb' s\<rbrakk> \<Longrightarrow> valid_tcb_state' st s
 6. \<And>s. \<lbrakk>st_tcb_at' (\<lambda>st'. tcb_st_refs_of' st' = tcb_st_refs_of' st \<and> (st \<noteq> Structures_H.thread_state.Inactive \<and> st \<noteq> Structures_H.thread_state.IdleThreadState \<longrightarrow> st' \<noteq> Structures_H.thread_state.Inactive \<and> st' \<noteq> Structures_H.thread_state.IdleThreadState)) t s; t = ksIdleThread s \<longrightarrow> idle' st; runnable' st \<and> obj_at' tcbQueued t s \<longrightarrow> st_tcb_at' runnable' t s; sch_act_simple s; valid_pspace' s; sch_act_wf (ksSchedulerAction s) s; valid_queues_no_bitmap s; valid_bitmapQ s; bitmapQ_no_L2_orphans s; bitmapQ_no_L1_orphans s; sym_refs (state_refs_of' s); if_live_then_nonz_cap' s; if_unsafe_then_cap' s; valid_idle' s; valid_global_refs' s; valid_arch_state' s; valid_irq_node' (irq_node' s) s; valid_irq_handlers' s; valid_irq_states' s; valid_machine_state' s; irqs_masked' s; valid_queues' s; ct_not_inQ s; ct_idle_or_in_cur_domain' s; valid_pde_mappings' s; pspace_domain_valid s; ksCurDomain s \<le> maxDomain; ksDomSchedule (newKernelState undefined) \<noteq> []; \<forall>x\<in>set (ksDomSchedule (newKernelState undefined)). dschDomain x \<le> maxDomain \<and> 0 < dschLength x; ksDomSchedule s = ksDomSchedule (newKernelState undefined); ksDomScheduleIdx s < length (ksDomSchedule (newKernelState undefined)); untyped_ranges_zero' s; cur_tcb' s\<rbrakk> \<Longrightarrow> sym_refs (\<lambda>a. if a = t then tcb_st_refs_of' st \<union> {r \<in> state_refs_of' s t. snd r = TCBBound} else state_refs_of' s a)
 7. \<And>s. \<lbrakk>st_tcb_at' (\<lambda>st'. tcb_st_refs_of' st' = tcb_st_refs_of' st \<and> (st \<noteq> Structures_H.thread_state.Inactive \<and> st \<noteq> Structures_H.thread_state.IdleThreadState \<longrightarrow> st' \<noteq> Structures_H.thread_state.Inactive \<and> st' \<noteq> Structures_H.thread_state.IdleThreadState)) t s; t = ksIdleThread s \<longrightarrow> idle' st; runnable' st \<and> obj_at' tcbQueued t s \<longrightarrow> st_tcb_at' runnable' t s; sch_act_simple s; valid_pspace' s; sch_act_wf (ksSchedulerAction s) s; valid_queues_no_bitmap s; valid_bitmapQ s; bitmapQ_no_L2_orphans s; bitmapQ_no_L1_orphans s; sym_refs (state_refs_of' s); if_live_then_nonz_cap' s; if_unsafe_then_cap' s; valid_idle' s; valid_global_refs' s; valid_arch_state' s; valid_irq_node' (irq_node' s) s; valid_irq_handlers' s; valid_irq_states' s; valid_machine_state' s; irqs_masked' s; valid_queues' s; ct_not_inQ s; ct_idle_or_in_cur_domain' s; valid_pde_mappings' s; pspace_domain_valid s; ksCurDomain s \<le> maxDomain; ksDomSchedule (newKernelState undefined) \<noteq> []; \<forall>x\<in>set (ksDomSchedule (newKernelState undefined)). dschDomain x \<le> maxDomain \<and> 0 < dschLength x; ksDomSchedule s = ksDomSchedule (newKernelState undefined); ksDomScheduleIdx s < length (ksDomSchedule (newKernelState undefined)); untyped_ranges_zero' s; cur_tcb' s\<rbrakk> \<Longrightarrow> st \<noteq> Structures_H.thread_state.Inactive \<and> st \<noteq> Structures_H.thread_state.IdleThreadState \<longrightarrow> ex_nonz_cap_to' t s
 8. \<And>s. \<lbrakk>st_tcb_at' (\<lambda>st'. tcb_st_refs_of' st' = tcb_st_refs_of' st \<and> (st \<noteq> Structures_H.thread_state.Inactive \<and> st \<noteq> Structures_H.thread_state.IdleThreadState \<longrightarrow> st' \<noteq> Structures_H.thread_state.Inactive \<and> st' \<noteq> Structures_H.thread_state.IdleThreadState)) t s; t = ksIdleThread s \<longrightarrow> idle' st; runnable' st \<and> obj_at' tcbQueued t s \<longrightarrow> st_tcb_at' runnable' t s; sch_act_simple s; valid_pspace' s; sch_act_wf (ksSchedulerAction s) s; valid_queues_no_bitmap s; valid_bitmapQ s; bitmapQ_no_L2_orphans s; bitmapQ_no_L1_orphans s; sym_refs (state_refs_of' s); if_live_then_nonz_cap' s; if_unsafe_then_cap' s; valid_idle' s; valid_global_refs' s; valid_arch_state' s; valid_irq_node' (irq_node' s) s; valid_irq_handlers' s; valid_irq_states' s; valid_machine_state' s; irqs_masked' s; valid_queues' s; ct_not_inQ s; ct_idle_or_in_cur_domain' s; valid_pde_mappings' s; pspace_domain_valid s; ksCurDomain s \<le> maxDomain; ksDomSchedule (newKernelState undefined) \<noteq> []; \<forall>x\<in>set (ksDomSchedule (newKernelState undefined)). dschDomain x \<le> maxDomain \<and> 0 < dschLength x; ksDomSchedule s = ksDomSchedule (newKernelState undefined); ksDomScheduleIdx s < length (ksDomSchedule (newKernelState undefined)); untyped_ranges_zero' s; cur_tcb' s\<rbrakk> \<Longrightarrow> tcb_at' t s proof (prove)
goal (8 subgoals):
 1. \<And>s x xa xb obj. \<lbrakk>st_tcb_at' (\<lambda>st'. tcb_st_refs_of' st' = tcb_st_refs_of' st \<and> (st \<noteq> Structures_H.thread_state.Inactive \<and> st \<noteq> Structures_H.thread_state.IdleThreadState \<longrightarrow> st' \<noteq> Structures_H.thread_state.Inactive \<and> st' \<noteq> Structures_H.thread_state.IdleThreadState)) t s; t = ksIdleThread s \<longrightarrow> idle' st; runnable' st \<and> obj_at' tcbQueued t s \<longrightarrow> st_tcb_at' runnable' t s; sch_act_simple s; valid_pspace' s; sch_act_wf (ksSchedulerAction s) s; valid_bitmapQ s; bitmapQ_no_L2_orphans s; bitmapQ_no_L1_orphans s; sym_refs (state_refs_of' s); if_live_then_nonz_cap' s; if_unsafe_then_cap' s; valid_idle' s; valid_global_refs' s; valid_arch_state' s; valid_irq_node' (irq_node' s) s; valid_irq_handlers' s; valid_irq_states' s; valid_machine_state' s; irqs_masked' s; valid_queues' s; ct_not_inQ s; ct_idle_or_in_cur_domain' s; valid_pde_mappings' s; pspace_domain_valid s; ksCurDomain s \<le> maxDomain; ksDomSchedule (newKernelState undefined) \<noteq> []; \<forall>x\<in>set (ksDomSchedule (newKernelState undefined)). dschDomain x \<le> maxDomain \<and> 0 < dschLength x; ksDomSchedule s = ksDomSchedule (newKernelState undefined); ksDomScheduleIdx s < length (ksDomSchedule (newKernelState undefined)); untyped_ranges_zero' s; cur_tcb' s; x \<in> set (ksReadyQueues s (xa, xb)); (inQ xa xb and (\<lambda>x. runnable' (tcbState x))) obj\<rbrakk> \<Longrightarrow> tcbQueued obj \<and> tcbDomain obj = xa \<and> tcbPriority obj = xb
 2. \<And>s x xa xb. \<lbrakk>st_tcb_at' (\<lambda>st'. tcb_st_refs_of' st' = tcb_st_refs_of' st \<and> (st \<noteq> Structures_H.thread_state.Inactive \<and> st \<noteq> Structures_H.thread_state.IdleThreadState \<longrightarrow> st' \<noteq> Structures_H.thread_state.Inactive \<and> st' \<noteq> Structures_H.thread_state.IdleThreadState)) t s; t = ksIdleThread s \<longrightarrow> idle' st; runnable' st \<and> obj_at' tcbQueued t s \<longrightarrow> st_tcb_at' runnable' t s; sch_act_simple s; valid_pspace' s; sch_act_wf (ksSchedulerAction s) s; valid_bitmapQ s; bitmapQ_no_L2_orphans s; bitmapQ_no_L1_orphans s; sym_refs (state_refs_of' s); if_live_then_nonz_cap' s; if_unsafe_then_cap' s; valid_idle' s; valid_global_refs' s; valid_arch_state' s; valid_irq_node' (irq_node' s) s; valid_irq_handlers' s; valid_irq_states' s; valid_machine_state' s; irqs_masked' s; valid_queues' s; ct_not_inQ s; ct_idle_or_in_cur_domain' s; valid_pde_mappings' s; pspace_domain_valid s; ksCurDomain s \<le> maxDomain; ksDomSchedule (newKernelState undefined) \<noteq> []; \<forall>x\<in>set (ksDomSchedule (newKernelState undefined)). dschDomain x \<le> maxDomain \<and> 0 < dschLength x; ksDomSchedule s = ksDomSchedule (newKernelState undefined); ksDomScheduleIdx s < length (ksDomSchedule (newKernelState undefined)); untyped_ranges_zero' s; cur_tcb' s; x \<in> set (ksReadyQueues s (xa, xb)); obj_at' (inQ xa xb and (\<lambda>x. runnable' (tcbState x))) x s\<rbrakk> \<Longrightarrow> x \<noteq> t \<longrightarrow> st_tcb_at' runnable' x s
 3. \<And>s x xa xb. \<lbrakk>st_tcb_at' (\<lambda>st'. tcb_st_refs_of' st' = tcb_st_refs_of' st \<and> (st \<noteq> Structures_H.thread_state.Inactive \<and> st \<noteq> Structures_H.thread_state.IdleThreadState \<longrightarrow> st' \<noteq> Structures_H.thread_state.Inactive \<and> st' \<noteq> Structures_H.thread_state.IdleThreadState)) t s; t = ksIdleThread s \<longrightarrow> idle' st; runnable' st \<and> obj_at' tcbQueued t s \<longrightarrow> st_tcb_at' runnable' t s; sch_act_simple s; valid_pspace' s; sch_act_wf (ksSchedulerAction s) s; valid_queues_no_bitmap s; valid_bitmapQ s; bitmapQ_no_L2_orphans s; bitmapQ_no_L1_orphans s; sym_refs (state_refs_of' s); if_live_then_nonz_cap' s; if_unsafe_then_cap' s; valid_idle' s; valid_global_refs' s; valid_arch_state' s; valid_irq_node' (irq_node' s) s; valid_irq_handlers' s; valid_irq_states' s; valid_machine_state' s; irqs_masked' s; valid_queues' s; ct_not_inQ s; ct_idle_or_in_cur_domain' s; valid_pde_mappings' s; pspace_domain_valid s; ksCurDomain s \<le> maxDomain; ksDomSchedule (newKernelState undefined) \<noteq> []; \<forall>x\<in>set (ksDomSchedule (newKernelState undefined)). dschDomain x \<le> maxDomain \<and> 0 < dschLength x; ksDomSchedule s = ksDomSchedule (newKernelState undefined); ksDomScheduleIdx s < length (ksDomSchedule (newKernelState undefined)); untyped_ranges_zero' s; cur_tcb' s\<rbrakk> \<Longrightarrow> distinct (ksReadyQueues s (xa, xb)) \<and> (maxDomain < xa \<longrightarrow> ksReadyQueues s (xa, xb) = []) \<and> (maxPriority < xb \<longrightarrow> ksReadyQueues s (xa, xb) = [])
 4. \<And>s. \<lbrakk>st_tcb_at' (\<lambda>st'. tcb_st_refs_of' st' = tcb_st_refs_of' st \<and> (st \<noteq> Structures_H.thread_state.Inactive \<and> st \<noteq> Structures_H.thread_state.IdleThreadState \<longrightarrow> st' \<noteq> Structures_H.thread_state.Inactive \<and> st' \<noteq> Structures_H.thread_state.IdleThreadState)) t s; t = ksIdleThread s \<longrightarrow> idle' st; runnable' st \<and> obj_at' tcbQueued t s \<longrightarrow> st_tcb_at' runnable' t s; sch_act_simple s; valid_pspace' s; sch_act_wf (ksSchedulerAction s) s; valid_queues_no_bitmap s; valid_bitmapQ s; bitmapQ_no_L2_orphans s; bitmapQ_no_L1_orphans s; sym_refs (state_refs_of' s); if_live_then_nonz_cap' s; if_unsafe_then_cap' s; valid_idle' s; valid_global_refs' s; valid_arch_state' s; valid_irq_node' (irq_node' s) s; valid_irq_handlers' s; valid_irq_states' s; valid_machine_state' s; irqs_masked' s; valid_queues' s; ct_not_inQ s; ct_idle_or_in_cur_domain' s; valid_pde_mappings' s; pspace_domain_valid s; ksCurDomain s \<le> maxDomain; ksDomSchedule (newKernelState undefined) \<noteq> []; \<forall>x\<in>set (ksDomSchedule (newKernelState undefined)). dschDomain x \<le> maxDomain \<and> 0 < dschLength x; ksDomSchedule s = ksDomSchedule (newKernelState undefined); ksDomScheduleIdx s < length (ksDomSchedule (newKernelState undefined)); untyped_ranges_zero' s; cur_tcb' s\<rbrakk> \<Longrightarrow> tcb_at' t s
 5. \<And>s. \<lbrakk>st_tcb_at' (\<lambda>st'. tcb_st_refs_of' st' = tcb_st_refs_of' st \<and> (st \<noteq> Structures_H.thread_state.Inactive \<and> st \<noteq> Structures_H.thread_state.IdleThreadState \<longrightarrow> st' \<noteq> Structures_H.thread_state.Inactive \<and> st' \<noteq> Structures_H.thread_state.IdleThreadState)) t s; t = ksIdleThread s \<longrightarrow> idle' st; runnable' st \<and> obj_at' tcbQueued t s \<longrightarrow> st_tcb_at' runnable' t s; sch_act_simple s; valid_pspace' s; sch_act_wf (ksSchedulerAction s) s; valid_queues_no_bitmap s; valid_bitmapQ s; bitmapQ_no_L2_orphans s; bitmapQ_no_L1_orphans s; sym_refs (state_refs_of' s); if_live_then_nonz_cap' s; if_unsafe_then_cap' s; valid_idle' s; valid_global_refs' s; valid_arch_state' s; valid_irq_node' (irq_node' s) s; valid_irq_handlers' s; valid_irq_states' s; valid_machine_state' s; irqs_masked' s; valid_queues' s; ct_not_inQ s; ct_idle_or_in_cur_domain' s; valid_pde_mappings' s; pspace_domain_valid s; ksCurDomain s \<le> maxDomain; ksDomSchedule (newKernelState undefined) \<noteq> []; \<forall>x\<in>set (ksDomSchedule (newKernelState undefined)). dschDomain x \<le> maxDomain \<and> 0 < dschLength x; ksDomSchedule s = ksDomSchedule (newKernelState undefined); ksDomScheduleIdx s < length (ksDomSchedule (newKernelState undefined)); untyped_ranges_zero' s; cur_tcb' s\<rbrakk> \<Longrightarrow> valid_tcb_state' st s
 6. \<And>s. \<lbrakk>st_tcb_at' (\<lambda>st'. tcb_st_refs_of' st' = tcb_st_refs_of' st \<and> (st \<noteq> Structures_H.thread_state.Inactive \<and> st \<noteq> Structures_H.thread_state.IdleThreadState \<longrightarrow> st' \<noteq> Structures_H.thread_state.Inactive \<and> st' \<noteq> Structures_H.thread_state.IdleThreadState)) t s; t = ksIdleThread s \<longrightarrow> idle' st; runnable' st \<and> obj_at' tcbQueued t s \<longrightarrow> st_tcb_at' runnable' t s; sch_act_simple s; valid_pspace' s; sch_act_wf (ksSchedulerAction s) s; valid_queues_no_bitmap s; valid_bitmapQ s; bitmapQ_no_L2_orphans s; bitmapQ_no_L1_orphans s; sym_refs (state_refs_of' s); if_live_then_nonz_cap' s; if_unsafe_then_cap' s; valid_idle' s; valid_global_refs' s; valid_arch_state' s; valid_irq_node' (irq_node' s) s; valid_irq_handlers' s; valid_irq_states' s; valid_machine_state' s; irqs_masked' s; valid_queues' s; ct_not_inQ s; ct_idle_or_in_cur_domain' s; valid_pde_mappings' s; pspace_domain_valid s; ksCurDomain s \<le> maxDomain; ksDomSchedule (newKernelState undefined) \<noteq> []; \<forall>x\<in>set (ksDomSchedule (newKernelState undefined)). dschDomain x \<le> maxDomain \<and> 0 < dschLength x; ksDomSchedule s = ksDomSchedule (newKernelState undefined); ksDomScheduleIdx s < length (ksDomSchedule (newKernelState undefined)); untyped_ranges_zero' s; cur_tcb' s\<rbrakk> \<Longrightarrow> sym_refs (\<lambda>a. if a = t then tcb_st_refs_of' st \<union> {r \<in> state_refs_of' s t. snd r = TCBBound} else state_refs_of' s a)
 7. \<And>s. \<lbrakk>st_tcb_at' (\<lambda>st'. tcb_st_refs_of' st' = tcb_st_refs_of' st \<and> (st \<noteq> Structures_H.thread_state.Inactive \<and> st \<noteq> Structures_H.thread_state.IdleThreadState \<longrightarrow> st' \<noteq> Structures_H.thread_state.Inactive \<and> st' \<noteq> Structures_H.thread_state.IdleThreadState)) t s; t = ksIdleThread s \<longrightarrow> idle' st; runnable' st \<and> obj_at' tcbQueued t s \<longrightarrow> st_tcb_at' runnable' t s; sch_act_simple s; valid_pspace' s; sch_act_wf (ksSchedulerAction s) s; valid_queues_no_bitmap s; valid_bitmapQ s; bitmapQ_no_L2_orphans s; bitmapQ_no_L1_orphans s; sym_refs (state_refs_of' s); if_live_then_nonz_cap' s; if_unsafe_then_cap' s; valid_idle' s; valid_global_refs' s; valid_arch_state' s; valid_irq_node' (irq_node' s) s; valid_irq_handlers' s; valid_irq_states' s; valid_machine_state' s; irqs_masked' s; valid_queues' s; ct_not_inQ s; ct_idle_or_in_cur_domain' s; valid_pde_mappings' s; pspace_domain_valid s; ksCurDomain s \<le> maxDomain; ksDomSchedule (newKernelState undefined) \<noteq> []; \<forall>x\<in>set (ksDomSchedule (newKernelState undefined)). dschDomain x \<le> maxDomain \<and> 0 < dschLength x; ksDomSchedule s = ksDomSchedule (newKernelState undefined); ksDomScheduleIdx s < length (ksDomSchedule (newKernelState undefined)); untyped_ranges_zero' s; cur_tcb' s\<rbrakk> \<Longrightarrow> st \<noteq> Structures_H.thread_state.Inactive \<and> st \<noteq> Structures_H.thread_state.IdleThreadState \<longrightarrow> ex_nonz_cap_to' t s
 8. \<And>s. \<lbrakk>st_tcb_at' (\<lambda>st'. tcb_st_refs_of' st' = tcb_st_refs_of' st \<and> (st \<noteq> Structures_H.thread_state.Inactive \<and> st \<noteq> Structures_H.thread_state.IdleThreadState \<longrightarrow> st' \<noteq> Structures_H.thread_state.Inactive \<and> st' \<noteq> Structures_H.thread_state.IdleThreadState)) t s; t = ksIdleThread s \<longrightarrow> idle' st; runnable' st \<and> obj_at' tcbQueued t s \<longrightarrow> st_tcb_at' runnable' t s; sch_act_simple s; valid_pspace' s; sch_act_wf (ksSchedulerAction s) s; valid_queues_no_bitmap s; valid_bitmapQ s; bitmapQ_no_L2_orphans s; bitmapQ_no_L1_orphans s; sym_refs (state_refs_of' s); if_live_then_nonz_cap' s; if_unsafe_then_cap' s; valid_idle' s; valid_global_refs' s; valid_arch_state' s; valid_irq_node' (irq_node' s) s; valid_irq_handlers' s; valid_irq_states' s; valid_machine_state' s; irqs_masked' s; valid_queues' s; ct_not_inQ s; ct_idle_or_in_cur_domain' s; valid_pde_mappings' s; pspace_domain_valid s; ksCurDomain s \<le> maxDomain; ksDomSchedule (newKernelState undefined) \<noteq> []; \<forall>x\<in>set (ksDomSchedule (newKernelState undefined)). dschDomain x \<le> maxDomain \<and> 0 < dschLength x; ksDomSchedule s = ksDomSchedule (newKernelState undefined); ksDomScheduleIdx s < length (ksDomSchedule (newKernelState undefined)); untyped_ranges_zero' s; cur_tcb' s\<rbrakk> \<Longrightarrow> tcb_at' t s proof (prove)
goal (7 subgoals):
 1. \<And>s x xa xb. \<lbrakk>st_tcb_at' (\<lambda>st'. tcb_st_refs_of' st' = tcb_st_refs_of' st \<and> (st \<noteq> Structures_H.thread_state.Inactive \<and> st \<noteq> Structures_H.thread_state.IdleThreadState \<longrightarrow> st' \<noteq> Structures_H.thread_state.Inactive \<and> st' \<noteq> Structures_H.thread_state.IdleThreadState)) t s; t = ksIdleThread s \<longrightarrow> idle' st; runnable' st \<and> obj_at' tcbQueued t s \<longrightarrow> st_tcb_at' runnable' t s; sch_act_simple s; valid_pspace' s; sch_act_wf (ksSchedulerAction s) s; valid_bitmapQ s; bitmapQ_no_L2_orphans s; bitmapQ_no_L1_orphans s; sym_refs (state_refs_of' s); if_live_then_nonz_cap' s; if_unsafe_then_cap' s; valid_idle' s; valid_global_refs' s; valid_arch_state' s; valid_irq_node' (irq_node' s) s; valid_irq_handlers' s; valid_irq_states' s; valid_machine_state' s; irqs_masked' s; valid_queues' s; ct_not_inQ s; ct_idle_or_in_cur_domain' s; valid_pde_mappings' s; pspace_domain_valid s; ksCurDomain s \<le> maxDomain; ksDomSchedule (newKernelState undefined) \<noteq> []; \<forall>x\<in>set (ksDomSchedule (newKernelState undefined)). dschDomain x \<le> maxDomain \<and> 0 < dschLength x; ksDomSchedule s = ksDomSchedule (newKernelState undefined); ksDomScheduleIdx s < length (ksDomSchedule (newKernelState undefined)); untyped_ranges_zero' s; cur_tcb' s; x \<in> set (ksReadyQueues s (xa, xb)); obj_at' (inQ xa xb and (\<lambda>x. runnable' (tcbState x))) x s\<rbrakk> \<Longrightarrow> x \<noteq> t \<longrightarrow> st_tcb_at' runnable' x s
 2. \<And>s x xa xb. \<lbrakk>st_tcb_at' (\<lambda>st'. tcb_st_refs_of' st' = tcb_st_refs_of' st \<and> (st \<noteq> Structures_H.thread_state.Inactive \<and> st \<noteq> Structures_H.thread_state.IdleThreadState \<longrightarrow> st' \<noteq> Structures_H.thread_state.Inactive \<and> st' \<noteq> Structures_H.thread_state.IdleThreadState)) t s; t = ksIdleThread s \<longrightarrow> idle' st; runnable' st \<and> obj_at' tcbQueued t s \<longrightarrow> st_tcb_at' runnable' t s; sch_act_simple s; valid_pspace' s; sch_act_wf (ksSchedulerAction s) s; valid_queues_no_bitmap s; valid_bitmapQ s; bitmapQ_no_L2_orphans s; bitmapQ_no_L1_orphans s; sym_refs (state_refs_of' s); if_live_then_nonz_cap' s; if_unsafe_then_cap' s; valid_idle' s; valid_global_refs' s; valid_arch_state' s; valid_irq_node' (irq_node' s) s; valid_irq_handlers' s; valid_irq_states' s; valid_machine_state' s; irqs_masked' s; valid_queues' s; ct_not_inQ s; ct_idle_or_in_cur_domain' s; valid_pde_mappings' s; pspace_domain_valid s; ksCurDomain s \<le> maxDomain; ksDomSchedule (newKernelState undefined) \<noteq> []; \<forall>x\<in>set (ksDomSchedule (newKernelState undefined)). dschDomain x \<le> maxDomain \<and> 0 < dschLength x; ksDomSchedule s = ksDomSchedule (newKernelState undefined); ksDomScheduleIdx s < length (ksDomSchedule (newKernelState undefined)); untyped_ranges_zero' s; cur_tcb' s\<rbrakk> \<Longrightarrow> distinct (ksReadyQueues s (xa, xb)) \<and> (maxDomain < xa \<longrightarrow> ksReadyQueues s (xa, xb) = []) \<and> (maxPriority < xb \<longrightarrow> ksReadyQueues s (xa, xb) = [])
 3. \<And>s. \<lbrakk>st_tcb_at' (\<lambda>st'. tcb_st_refs_of' st' = tcb_st_refs_of' st \<and> (st \<noteq> Structures_H.thread_state.Inactive \<and> st \<noteq> Structures_H.thread_state.IdleThreadState \<longrightarrow> st' \<noteq> Structures_H.thread_state.Inactive \<and> st' \<noteq> Structures_H.thread_state.IdleThreadState)) t s; t = ksIdleThread s \<longrightarrow> idle' st; runnable' st \<and> obj_at' tcbQueued t s \<longrightarrow> st_tcb_at' runnable' t s; sch_act_simple s; valid_pspace' s; sch_act_wf (ksSchedulerAction s) s; valid_queues_no_bitmap s; valid_bitmapQ s; bitmapQ_no_L2_orphans s; bitmapQ_no_L1_orphans s; sym_refs (state_refs_of' s); if_live_then_nonz_cap' s; if_unsafe_then_cap' s; valid_idle' s; valid_global_refs' s; valid_arch_state' s; valid_irq_node' (irq_node' s) s; valid_irq_handlers' s; valid_irq_states' s; valid_machine_state' s; irqs_masked' s; valid_queues' s; ct_not_inQ s; ct_idle_or_in_cur_domain' s; valid_pde_mappings' s; pspace_domain_valid s; ksCurDomain s \<le> maxDomain; ksDomSchedule (newKernelState undefined) \<noteq> []; \<forall>x\<in>set (ksDomSchedule (newKernelState undefined)). dschDomain x \<le> maxDomain \<and> 0 < dschLength x; ksDomSchedule s = ksDomSchedule (newKernelState undefined); ksDomScheduleIdx s < length (ksDomSchedule (newKernelState undefined)); untyped_ranges_zero' s; cur_tcb' s\<rbrakk> \<Longrightarrow> tcb_at' t s
 4. \<And>s. \<lbrakk>st_tcb_at' (\<lambda>st'. tcb_st_refs_of' st' = tcb_st_refs_of' st \<and> (st \<noteq> Structures_H.thread_state.Inactive \<and> st \<noteq> Structures_H.thread_state.IdleThreadState \<longrightarrow> st' \<noteq> Structures_H.thread_state.Inactive \<and> st' \<noteq> Structures_H.thread_state.IdleThreadState)) t s; t = ksIdleThread s \<longrightarrow> idle' st; runnable' st \<and> obj_at' tcbQueued t s \<longrightarrow> st_tcb_at' runnable' t s; sch_act_simple s; valid_pspace' s; sch_act_wf (ksSchedulerAction s) s; valid_queues_no_bitmap s; valid_bitmapQ s; bitmapQ_no_L2_orphans s; bitmapQ_no_L1_orphans s; sym_refs (state_refs_of' s); if_live_then_nonz_cap' s; if_unsafe_then_cap' s; valid_idle' s; valid_global_refs' s; valid_arch_state' s; valid_irq_node' (irq_node' s) s; valid_irq_handlers' s; valid_irq_states' s; valid_machine_state' s; irqs_masked' s; valid_queues' s; ct_not_inQ s; ct_idle_or_in_cur_domain' s; valid_pde_mappings' s; pspace_domain_valid s; ksCurDomain s \<le> maxDomain; ksDomSchedule (newKernelState undefined) \<noteq> []; \<forall>x\<in>set (ksDomSchedule (newKernelState undefined)). dschDomain x \<le> maxDomain \<and> 0 < dschLength x; ksDomSchedule s = ksDomSchedule (newKernelState undefined); ksDomScheduleIdx s < length (ksDomSchedule (newKernelState undefined)); untyped_ranges_zero' s; cur_tcb' s\<rbrakk> \<Longrightarrow> valid_tcb_state' st s
 5. \<And>s. \<lbrakk>st_tcb_at' (\<lambda>st'. tcb_st_refs_of' st' = tcb_st_refs_of' st \<and> (st \<noteq> Structures_H.thread_state.Inactive \<and> st \<noteq> Structures_H.thread_state.IdleThreadState \<longrightarrow> st' \<noteq> Structures_H.thread_state.Inactive \<and> st' \<noteq> Structures_H.thread_state.IdleThreadState)) t s; t = ksIdleThread s \<longrightarrow> idle' st; runnable' st \<and> obj_at' tcbQueued t s \<longrightarrow> st_tcb_at' runnable' t s; sch_act_simple s; valid_pspace' s; sch_act_wf (ksSchedulerAction s) s; valid_queues_no_bitmap s; valid_bitmapQ s; bitmapQ_no_L2_orphans s; bitmapQ_no_L1_orphans s; sym_refs (state_refs_of' s); if_live_then_nonz_cap' s; if_unsafe_then_cap' s; valid_idle' s; valid_global_refs' s; valid_arch_state' s; valid_irq_node' (irq_node' s) s; valid_irq_handlers' s; valid_irq_states' s; valid_machine_state' s; irqs_masked' s; valid_queues' s; ct_not_inQ s; ct_idle_or_in_cur_domain' s; valid_pde_mappings' s; pspace_domain_valid s; ksCurDomain s \<le> maxDomain; ksDomSchedule (newKernelState undefined) \<noteq> []; \<forall>x\<in>set (ksDomSchedule (newKernelState undefined)). dschDomain x \<le> maxDomain \<and> 0 < dschLength x; ksDomSchedule s = ksDomSchedule (newKernelState undefined); ksDomScheduleIdx s < length (ksDomSchedule (newKernelState undefined)); untyped_ranges_zero' s; cur_tcb' s\<rbrakk> \<Longrightarrow> sym_refs (\<lambda>a. if a = t then tcb_st_refs_of' st \<union> {r \<in> state_refs_of' s t. snd r = TCBBound} else state_refs_of' s a)
 6. \<And>s. \<lbrakk>st_tcb_at' (\<lambda>st'. tcb_st_refs_of' st' = tcb_st_refs_of' st \<and> (st \<noteq> Structures_H.thread_state.Inactive \<and> st \<noteq> Structures_H.thread_state.IdleThreadState \<longrightarrow> st' \<noteq> Structures_H.thread_state.Inactive \<and> st' \<noteq> Structures_H.thread_state.IdleThreadState)) t s; t = ksIdleThread s \<longrightarrow> idle' st; runnable' st \<and> obj_at' tcbQueued t s \<longrightarrow> st_tcb_at' runnable' t s; sch_act_simple s; valid_pspace' s; sch_act_wf (ksSchedulerAction s) s; valid_queues_no_bitmap s; valid_bitmapQ s; bitmapQ_no_L2_orphans s; bitmapQ_no_L1_orphans s; sym_refs (state_refs_of' s); if_live_then_nonz_cap' s; if_unsafe_then_cap' s; valid_idle' s; valid_global_refs' s; valid_arch_state' s; valid_irq_node' (irq_node' s) s; valid_irq_handlers' s; valid_irq_states' s; valid_machine_state' s; irqs_masked' s; valid_queues' s; ct_not_inQ s; ct_idle_or_in_cur_domain' s; valid_pde_mappings' s; pspace_domain_valid s; ksCurDomain s \<le> maxDomain; ksDomSchedule (newKernelState undefined) \<noteq> []; \<forall>x\<in>set (ksDomSchedule (newKernelState undefined)). dschDomain x \<le> maxDomain \<and> 0 < dschLength x; ksDomSchedule s = ksDomSchedule (newKernelState undefined); ksDomScheduleIdx s < length (ksDomSchedule (newKernelState undefined)); untyped_ranges_zero' s; cur_tcb' s\<rbrakk> \<Longrightarrow> st \<noteq> Structures_H.thread_state.Inactive \<and> st \<noteq> Structures_H.thread_state.IdleThreadState \<longrightarrow> ex_nonz_cap_to' t s
 7. \<And>s. \<lbrakk>st_tcb_at' (\<lambda>st'. tcb_st_refs_of' st' = tcb_st_refs_of' st \<and> (st \<noteq> Structures_H.thread_state.Inactive \<and> st \<noteq> Structures_H.thread_state.IdleThreadState \<longrightarrow> st' \<noteq> Structures_H.thread_state.Inactive \<and> st' \<noteq> Structures_H.thread_state.IdleThreadState)) t s; t = ksIdleThread s \<longrightarrow> idle' st; runnable' st \<and> obj_at' tcbQueued t s \<longrightarrow> st_tcb_at' runnable' t s; sch_act_simple s; valid_pspace' s; sch_act_wf (ksSchedulerAction s) s; valid_queues_no_bitmap s; valid_bitmapQ s; bitmapQ_no_L2_orphans s; bitmapQ_no_L1_orphans s; sym_refs (state_refs_of' s); if_live_then_nonz_cap' s; if_unsafe_then_cap' s; valid_idle' s; valid_global_refs' s; valid_arch_state' s; valid_irq_node' (irq_node' s) s; valid_irq_handlers' s; valid_irq_states' s; valid_machine_state' s; irqs_masked' s; valid_queues' s; ct_not_inQ s; ct_idle_or_in_cur_domain' s; valid_pde_mappings' s; pspace_domain_valid s; ksCurDomain s \<le> maxDomain; ksDomSchedule (newKernelState undefined) \<noteq> []; \<forall>x\<in>set (ksDomSchedule (newKernelState undefined)). dschDomain x \<le> maxDomain \<and> 0 < dschLength x; ksDomSchedule s = ksDomSchedule (newKernelState undefined); ksDomScheduleIdx s < length (ksDomSchedule (newKernelState undefined)); untyped_ranges_zero' s; cur_tcb' s\<rbrakk> \<Longrightarrow> tcb_at' t s proof (prove)
goal (7 subgoals):
 1. \<And>s x xa xb. \<lbrakk>obj_at' ((\<lambda>st'. tcb_st_refs_of' st' = tcb_st_refs_of' st \<and> (st \<noteq> Structures_H.thread_state.Inactive \<and> st \<noteq> Structures_H.thread_state.IdleThreadState \<longrightarrow> st' \<noteq> Structures_H.thread_state.Inactive \<and> st' \<noteq> Structures_H.thread_state.IdleThreadState)) \<circ> tcbState) t s; t = ksIdleThread s \<longrightarrow> idle' st; runnable' st \<and> obj_at' tcbQueued t s \<longrightarrow> obj_at' (runnable' \<circ> tcbState) t s; sch_act_simple s; valid_pspace' s; sch_act_wf (ksSchedulerAction s) s; valid_bitmapQ s; bitmapQ_no_L2_orphans s; bitmapQ_no_L1_orphans s; sym_refs (state_refs_of' s); if_live_then_nonz_cap' s; if_unsafe_then_cap' s; valid_idle' s; valid_global_refs' s; valid_arch_state' s; valid_irq_node' (irq_node' s) s; valid_irq_handlers' s; valid_irq_states' s; valid_machine_state' s; irqs_masked' s; valid_queues' s; ct_not_inQ s; ct_idle_or_in_cur_domain' s; valid_pde_mappings' s; pspace_domain_valid s; ksCurDomain s \<le> maxDomain; ksDomSchedule (newKernelState undefined) \<noteq> []; \<forall>x\<in>set (ksDomSchedule (newKernelState undefined)). dschDomain x \<le> maxDomain \<and> 0 < dschLength x; ksDomSchedule s = ksDomSchedule (newKernelState undefined); ksDomScheduleIdx s < length (ksDomSchedule (newKernelState undefined)); untyped_ranges_zero' s; cur_tcb' s; x \<in> set (ksReadyQueues s (xa, xb)); obj_at' (inQ xa xb and (\<lambda>x. runnable' (tcbState x))) x s; x \<noteq> t\<rbrakk> \<Longrightarrow> obj_at' (runnable' \<circ> tcbState) x s
 2. \<And>s x xa xb. \<lbrakk>st_tcb_at' (\<lambda>st'. tcb_st_refs_of' st' = tcb_st_refs_of' st \<and> (st \<noteq> Structures_H.thread_state.Inactive \<and> st \<noteq> Structures_H.thread_state.IdleThreadState \<longrightarrow> st' \<noteq> Structures_H.thread_state.Inactive \<and> st' \<noteq> Structures_H.thread_state.IdleThreadState)) t s; t = ksIdleThread s \<longrightarrow> idle' st; runnable' st \<and> obj_at' tcbQueued t s \<longrightarrow> st_tcb_at' runnable' t s; sch_act_simple s; valid_pspace' s; sch_act_wf (ksSchedulerAction s) s; valid_queues_no_bitmap s; valid_bitmapQ s; bitmapQ_no_L2_orphans s; bitmapQ_no_L1_orphans s; sym_refs (state_refs_of' s); if_live_then_nonz_cap' s; if_unsafe_then_cap' s; valid_idle' s; valid_global_refs' s; valid_arch_state' s; valid_irq_node' (irq_node' s) s; valid_irq_handlers' s; valid_irq_states' s; valid_machine_state' s; irqs_masked' s; valid_queues' s; ct_not_inQ s; ct_idle_or_in_cur_domain' s; valid_pde_mappings' s; pspace_domain_valid s; ksCurDomain s \<le> maxDomain; ksDomSchedule (newKernelState undefined) \<noteq> []; \<forall>x\<in>set (ksDomSchedule (newKernelState undefined)). dschDomain x \<le> maxDomain \<and> 0 < dschLength x; ksDomSchedule s = ksDomSchedule (newKernelState undefined); ksDomScheduleIdx s < length (ksDomSchedule (newKernelState undefined)); untyped_ranges_zero' s; cur_tcb' s\<rbrakk> \<Longrightarrow> distinct (ksReadyQueues s (xa, xb)) \<and> (maxDomain < xa \<longrightarrow> ksReadyQueues s (xa, xb) = []) \<and> (maxPriority < xb \<longrightarrow> ksReadyQueues s (xa, xb) = [])
 3. \<And>s. \<lbrakk>st_tcb_at' (\<lambda>st'. tcb_st_refs_of' st' = tcb_st_refs_of' st \<and> (st \<noteq> Structures_H.thread_state.Inactive \<and> st \<noteq> Structures_H.thread_state.IdleThreadState \<longrightarrow> st' \<noteq> Structures_H.thread_state.Inactive \<and> st' \<noteq> Structures_H.thread_state.IdleThreadState)) t s; t = ksIdleThread s \<longrightarrow> idle' st; runnable' st \<and> obj_at' tcbQueued t s \<longrightarrow> st_tcb_at' runnable' t s; sch_act_simple s; valid_pspace' s; sch_act_wf (ksSchedulerAction s) s; valid_queues_no_bitmap s; valid_bitmapQ s; bitmapQ_no_L2_orphans s; bitmapQ_no_L1_orphans s; sym_refs (state_refs_of' s); if_live_then_nonz_cap' s; if_unsafe_then_cap' s; valid_idle' s; valid_global_refs' s; valid_arch_state' s; valid_irq_node' (irq_node' s) s; valid_irq_handlers' s; valid_irq_states' s; valid_machine_state' s; irqs_masked' s; valid_queues' s; ct_not_inQ s; ct_idle_or_in_cur_domain' s; valid_pde_mappings' s; pspace_domain_valid s; ksCurDomain s \<le> maxDomain; ksDomSchedule (newKernelState undefined) \<noteq> []; \<forall>x\<in>set (ksDomSchedule (newKernelState undefined)). dschDomain x \<le> maxDomain \<and> 0 < dschLength x; ksDomSchedule s = ksDomSchedule (newKernelState undefined); ksDomScheduleIdx s < length (ksDomSchedule (newKernelState undefined)); untyped_ranges_zero' s; cur_tcb' s\<rbrakk> \<Longrightarrow> tcb_at' t s
 4. \<And>s. \<lbrakk>st_tcb_at' (\<lambda>st'. tcb_st_refs_of' st' = tcb_st_refs_of' st \<and> (st \<noteq> Structures_H.thread_state.Inactive \<and> st \<noteq> Structures_H.thread_state.IdleThreadState \<longrightarrow> st' \<noteq> Structures_H.thread_state.Inactive \<and> st' \<noteq> Structures_H.thread_state.IdleThreadState)) t s; t = ksIdleThread s \<longrightarrow> idle' st; runnable' st \<and> obj_at' tcbQueued t s \<longrightarrow> st_tcb_at' runnable' t s; sch_act_simple s; valid_pspace' s; sch_act_wf (ksSchedulerAction s) s; valid_queues_no_bitmap s; valid_bitmapQ s; bitmapQ_no_L2_orphans s; bitmapQ_no_L1_orphans s; sym_refs (state_refs_of' s); if_live_then_nonz_cap' s; if_unsafe_then_cap' s; valid_idle' s; valid_global_refs' s; valid_arch_state' s; valid_irq_node' (irq_node' s) s; valid_irq_handlers' s; valid_irq_states' s; valid_machine_state' s; irqs_masked' s; valid_queues' s; ct_not_inQ s; ct_idle_or_in_cur_domain' s; valid_pde_mappings' s; pspace_domain_valid s; ksCurDomain s \<le> maxDomain; ksDomSchedule (newKernelState undefined) \<noteq> []; \<forall>x\<in>set (ksDomSchedule (newKernelState undefined)). dschDomain x \<le> maxDomain \<and> 0 < dschLength x; ksDomSchedule s = ksDomSchedule (newKernelState undefined); ksDomScheduleIdx s < length (ksDomSchedule (newKernelState undefined)); untyped_ranges_zero' s; cur_tcb' s\<rbrakk> \<Longrightarrow> valid_tcb_state' st s
 5. \<And>s. \<lbrakk>st_tcb_at' (\<lambda>st'. tcb_st_refs_of' st' = tcb_st_refs_of' st \<and> (st \<noteq> Structures_H.thread_state.Inactive \<and> st \<noteq> Structures_H.thread_state.IdleThreadState \<longrightarrow> st' \<noteq> Structures_H.thread_state.Inactive \<and> st' \<noteq> Structures_H.thread_state.IdleThreadState)) t s; t = ksIdleThread s \<longrightarrow> idle' st; runnable' st \<and> obj_at' tcbQueued t s \<longrightarrow> st_tcb_at' runnable' t s; sch_act_simple s; valid_pspace' s; sch_act_wf (ksSchedulerAction s) s; valid_queues_no_bitmap s; valid_bitmapQ s; bitmapQ_no_L2_orphans s; bitmapQ_no_L1_orphans s; sym_refs (state_refs_of' s); if_live_then_nonz_cap' s; if_unsafe_then_cap' s; valid_idle' s; valid_global_refs' s; valid_arch_state' s; valid_irq_node' (irq_node' s) s; valid_irq_handlers' s; valid_irq_states' s; valid_machine_state' s; irqs_masked' s; valid_queues' s; ct_not_inQ s; ct_idle_or_in_cur_domain' s; valid_pde_mappings' s; pspace_domain_valid s; ksCurDomain s \<le> maxDomain; ksDomSchedule (newKernelState undefined) \<noteq> []; \<forall>x\<in>set (ksDomSchedule (newKernelState undefined)). dschDomain x \<le> maxDomain \<and> 0 < dschLength x; ksDomSchedule s = ksDomSchedule (newKernelState undefined); ksDomScheduleIdx s < length (ksDomSchedule (newKernelState undefined)); untyped_ranges_zero' s; cur_tcb' s\<rbrakk> \<Longrightarrow> sym_refs (\<lambda>a. if a = t then tcb_st_refs_of' st \<union> {r \<in> state_refs_of' s t. snd r = TCBBound} else state_refs_of' s a)
 6. \<And>s. \<lbrakk>st_tcb_at' (\<lambda>st'. tcb_st_refs_of' st' = tcb_st_refs_of' st \<and> (st \<noteq> Structures_H.thread_state.Inactive \<and> st \<noteq> Structures_H.thread_state.IdleThreadState \<longrightarrow> st' \<noteq> Structures_H.thread_state.Inactive \<and> st' \<noteq> Structures_H.thread_state.IdleThreadState)) t s; t = ksIdleThread s \<longrightarrow> idle' st; runnable' st \<and> obj_at' tcbQueued t s \<longrightarrow> st_tcb_at' runnable' t s; sch_act_simple s; valid_pspace' s; sch_act_wf (ksSchedulerAction s) s; valid_queues_no_bitmap s; valid_bitmapQ s; bitmapQ_no_L2_orphans s; bitmapQ_no_L1_orphans s; sym_refs (state_refs_of' s); if_live_then_nonz_cap' s; if_unsafe_then_cap' s; valid_idle' s; valid_global_refs' s; valid_arch_state' s; valid_irq_node' (irq_node' s) s; valid_irq_handlers' s; valid_irq_states' s; valid_machine_state' s; irqs_masked' s; valid_queues' s; ct_not_inQ s; ct_idle_or_in_cur_domain' s; valid_pde_mappings' s; pspace_domain_valid s; ksCurDomain s \<le> maxDomain; ksDomSchedule (newKernelState undefined) \<noteq> []; \<forall>x\<in>set (ksDomSchedule (newKernelState undefined)). dschDomain x \<le> maxDomain \<and> 0 < dschLength x; ksDomSchedule s = ksDomSchedule (newKernelState undefined); ksDomScheduleIdx s < length (ksDomSchedule (newKernelState undefined)); untyped_ranges_zero' s; cur_tcb' s\<rbrakk> \<Longrightarrow> st \<noteq> Structures_H.thread_state.Inactive \<and> st \<noteq> Structures_H.thread_state.IdleThreadState \<longrightarrow> ex_nonz_cap_to' t s
 7. \<And>s. \<lbrakk>st_tcb_at' (\<lambda>st'. tcb_st_refs_of' st' = tcb_st_refs_of' st \<and> (st \<noteq> Structures_H.thread_state.Inactive \<and> st \<noteq> Structures_H.thread_state.IdleThreadState \<longrightarrow> st' \<noteq> Structures_H.thread_state.Inactive \<and> st' \<noteq> Structures_H.thread_state.IdleThreadState)) t s; t = ksIdleThread s \<longrightarrow> idle' st; runnable' st \<and> obj_at' tcbQueued t s \<longrightarrow> st_tcb_at' runnable' t s; sch_act_simple s; valid_pspace' s; sch_act_wf (ksSchedulerAction s) s; valid_queues_no_bitmap s; valid_bitmapQ s; bitmapQ_no_L2_orphans s; bitmapQ_no_L1_orphans s; sym_refs (state_refs_of' s); if_live_then_nonz_cap' s; if_unsafe_then_cap' s; valid_idle' s; valid_global_refs' s; valid_arch_state' s; valid_irq_node' (irq_node' s) s; valid_irq_handlers' s; valid_irq_states' s; valid_machine_state' s; irqs_masked' s; valid_queues' s; ct_not_inQ s; ct_idle_or_in_cur_domain' s; valid_pde_mappings' s; pspace_domain_valid s; ksCurDomain s \<le> maxDomain; ksDomSchedule (newKernelState undefined) \<noteq> []; \<forall>x\<in>set (ksDomSchedule (newKernelState undefined)). dschDomain x \<le> maxDomain \<and> 0 < dschLength x; ksDomSchedule s = ksDomSchedule (newKernelState undefined); ksDomScheduleIdx s < length (ksDomSchedule (newKernelState undefined)); untyped_ranges_zero' s; cur_tcb' s\<rbrakk> \<Longrightarrow> tcb_at' t s proof (prove)
goal (7 subgoals):
 1. \<And>s x xa xb obj. \<lbrakk>obj_at' ((\<lambda>st'. tcb_st_refs_of' st' = tcb_st_refs_of' st \<and> (st \<noteq> Structures_H.thread_state.Inactive \<and> st \<noteq> Structures_H.thread_state.IdleThreadState \<longrightarrow> st' \<noteq> Structures_H.thread_state.Inactive \<and> st' \<noteq> Structures_H.thread_state.IdleThreadState)) \<circ> tcbState) t s; t = ksIdleThread s \<longrightarrow> idle' st; runnable' st \<and> obj_at' tcbQueued t s \<longrightarrow> obj_at' (runnable' \<circ> tcbState) t s; sch_act_simple s; valid_pspace' s; sch_act_wf (ksSchedulerAction s) s; valid_bitmapQ s; bitmapQ_no_L2_orphans s; bitmapQ_no_L1_orphans s; sym_refs (state_refs_of' s); if_live_then_nonz_cap' s; if_unsafe_then_cap' s; valid_idle' s; valid_global_refs' s; valid_arch_state' s; valid_irq_node' (irq_node' s) s; valid_irq_handlers' s; valid_irq_states' s; valid_machine_state' s; irqs_masked' s; valid_queues' s; ct_not_inQ s; ct_idle_or_in_cur_domain' s; valid_pde_mappings' s; pspace_domain_valid s; ksCurDomain s \<le> maxDomain; ksDomSchedule (newKernelState undefined) \<noteq> []; \<forall>x\<in>set (ksDomSchedule (newKernelState undefined)). dschDomain x \<le> maxDomain \<and> 0 < dschLength x; ksDomSchedule s = ksDomSchedule (newKernelState undefined); ksDomScheduleIdx s < length (ksDomSchedule (newKernelState undefined)); untyped_ranges_zero' s; cur_tcb' s; x \<in> set (ksReadyQueues s (xa, xb)); x \<noteq> t; (inQ xa xb and (\<lambda>x. runnable' (tcbState x))) obj\<rbrakk> \<Longrightarrow> (runnable' \<circ> tcbState) obj
 2. \<And>s x xa xb. \<lbrakk>st_tcb_at' (\<lambda>st'. tcb_st_refs_of' st' = tcb_st_refs_of' st \<and> (st \<noteq> Structures_H.thread_state.Inactive \<and> st \<noteq> Structures_H.thread_state.IdleThreadState \<longrightarrow> st' \<noteq> Structures_H.thread_state.Inactive \<and> st' \<noteq> Structures_H.thread_state.IdleThreadState)) t s; t = ksIdleThread s \<longrightarrow> idle' st; runnable' st \<and> obj_at' tcbQueued t s \<longrightarrow> st_tcb_at' runnable' t s; sch_act_simple s; valid_pspace' s; sch_act_wf (ksSchedulerAction s) s; valid_queues_no_bitmap s; valid_bitmapQ s; bitmapQ_no_L2_orphans s; bitmapQ_no_L1_orphans s; sym_refs (state_refs_of' s); if_live_then_nonz_cap' s; if_unsafe_then_cap' s; valid_idle' s; valid_global_refs' s; valid_arch_state' s; valid_irq_node' (irq_node' s) s; valid_irq_handlers' s; valid_irq_states' s; valid_machine_state' s; irqs_masked' s; valid_queues' s; ct_not_inQ s; ct_idle_or_in_cur_domain' s; valid_pde_mappings' s; pspace_domain_valid s; ksCurDomain s \<le> maxDomain; ksDomSchedule (newKernelState undefined) \<noteq> []; \<forall>x\<in>set (ksDomSchedule (newKernelState undefined)). dschDomain x \<le> maxDomain \<and> 0 < dschLength x; ksDomSchedule s = ksDomSchedule (newKernelState undefined); ksDomScheduleIdx s < length (ksDomSchedule (newKernelState undefined)); untyped_ranges_zero' s; cur_tcb' s\<rbrakk> \<Longrightarrow> distinct (ksReadyQueues s (xa, xb)) \<and> (maxDomain < xa \<longrightarrow> ksReadyQueues s (xa, xb) = []) \<and> (maxPriority < xb \<longrightarrow> ksReadyQueues s (xa, xb) = [])
 3. \<And>s. \<lbrakk>st_tcb_at' (\<lambda>st'. tcb_st_refs_of' st' = tcb_st_refs_of' st \<and> (st \<noteq> Structures_H.thread_state.Inactive \<and> st \<noteq> Structures_H.thread_state.IdleThreadState \<longrightarrow> st' \<noteq> Structures_H.thread_state.Inactive \<and> st' \<noteq> Structures_H.thread_state.IdleThreadState)) t s; t = ksIdleThread s \<longrightarrow> idle' st; runnable' st \<and> obj_at' tcbQueued t s \<longrightarrow> st_tcb_at' runnable' t s; sch_act_simple s; valid_pspace' s; sch_act_wf (ksSchedulerAction s) s; valid_queues_no_bitmap s; valid_bitmapQ s; bitmapQ_no_L2_orphans s; bitmapQ_no_L1_orphans s; sym_refs (state_refs_of' s); if_live_then_nonz_cap' s; if_unsafe_then_cap' s; valid_idle' s; valid_global_refs' s; valid_arch_state' s; valid_irq_node' (irq_node' s) s; valid_irq_handlers' s; valid_irq_states' s; valid_machine_state' s; irqs_masked' s; valid_queues' s; ct_not_inQ s; ct_idle_or_in_cur_domain' s; valid_pde_mappings' s; pspace_domain_valid s; ksCurDomain s \<le> maxDomain; ksDomSchedule (newKernelState undefined) \<noteq> []; \<forall>x\<in>set (ksDomSchedule (newKernelState undefined)). dschDomain x \<le> maxDomain \<and> 0 < dschLength x; ksDomSchedule s = ksDomSchedule (newKernelState undefined); ksDomScheduleIdx s < length (ksDomSchedule (newKernelState undefined)); untyped_ranges_zero' s; cur_tcb' s\<rbrakk> \<Longrightarrow> tcb_at' t s
 4. \<And>s. \<lbrakk>st_tcb_at' (\<lambda>st'. tcb_st_refs_of' st' = tcb_st_refs_of' st \<and> (st \<noteq> Structures_H.thread_state.Inactive \<and> st \<noteq> Structures_H.thread_state.IdleThreadState \<longrightarrow> st' \<noteq> Structures_H.thread_state.Inactive \<and> st' \<noteq> Structures_H.thread_state.IdleThreadState)) t s; t = ksIdleThread s \<longrightarrow> idle' st; runnable' st \<and> obj_at' tcbQueued t s \<longrightarrow> st_tcb_at' runnable' t s; sch_act_simple s; valid_pspace' s; sch_act_wf (ksSchedulerAction s) s; valid_queues_no_bitmap s; valid_bitmapQ s; bitmapQ_no_L2_orphans s; bitmapQ_no_L1_orphans s; sym_refs (state_refs_of' s); if_live_then_nonz_cap' s; if_unsafe_then_cap' s; valid_idle' s; valid_global_refs' s; valid_arch_state' s; valid_irq_node' (irq_node' s) s; valid_irq_handlers' s; valid_irq_states' s; valid_machine_state' s; irqs_masked' s; valid_queues' s; ct_not_inQ s; ct_idle_or_in_cur_domain' s; valid_pde_mappings' s; pspace_domain_valid s; ksCurDomain s \<le> maxDomain; ksDomSchedule (newKernelState undefined) \<noteq> []; \<forall>x\<in>set (ksDomSchedule (newKernelState undefined)). dschDomain x \<le> maxDomain \<and> 0 < dschLength x; ksDomSchedule s = ksDomSchedule (newKernelState undefined); ksDomScheduleIdx s < length (ksDomSchedule (newKernelState undefined)); untyped_ranges_zero' s; cur_tcb' s\<rbrakk> \<Longrightarrow> valid_tcb_state' st s
 5. \<And>s. \<lbrakk>st_tcb_at' (\<lambda>st'. tcb_st_refs_of' st' = tcb_st_refs_of' st \<and> (st \<noteq> Structures_H.thread_state.Inactive \<and> st \<noteq> Structures_H.thread_state.IdleThreadState \<longrightarrow> st' \<noteq> Structures_H.thread_state.Inactive \<and> st' \<noteq> Structures_H.thread_state.IdleThreadState)) t s; t = ksIdleThread s \<longrightarrow> idle' st; runnable' st \<and> obj_at' tcbQueued t s \<longrightarrow> st_tcb_at' runnable' t s; sch_act_simple s; valid_pspace' s; sch_act_wf (ksSchedulerAction s) s; valid_queues_no_bitmap s; valid_bitmapQ s; bitmapQ_no_L2_orphans s; bitmapQ_no_L1_orphans s; sym_refs (state_refs_of' s); if_live_then_nonz_cap' s; if_unsafe_then_cap' s; valid_idle' s; valid_global_refs' s; valid_arch_state' s; valid_irq_node' (irq_node' s) s; valid_irq_handlers' s; valid_irq_states' s; valid_machine_state' s; irqs_masked' s; valid_queues' s; ct_not_inQ s; ct_idle_or_in_cur_domain' s; valid_pde_mappings' s; pspace_domain_valid s; ksCurDomain s \<le> maxDomain; ksDomSchedule (newKernelState undefined) \<noteq> []; \<forall>x\<in>set (ksDomSchedule (newKernelState undefined)). dschDomain x \<le> maxDomain \<and> 0 < dschLength x; ksDomSchedule s = ksDomSchedule (newKernelState undefined); ksDomScheduleIdx s < length (ksDomSchedule (newKernelState undefined)); untyped_ranges_zero' s; cur_tcb' s\<rbrakk> \<Longrightarrow> sym_refs (\<lambda>a. if a = t then tcb_st_refs_of' st \<union> {r \<in> state_refs_of' s t. snd r = TCBBound} else state_refs_of' s a)
 6. \<And>s. \<lbrakk>st_tcb_at' (\<lambda>st'. tcb_st_refs_of' st' = tcb_st_refs_of' st \<and> (st \<noteq> Structures_H.thread_state.Inactive \<and> st \<noteq> Structures_H.thread_state.IdleThreadState \<longrightarrow> st' \<noteq> Structures_H.thread_state.Inactive \<and> st' \<noteq> Structures_H.thread_state.IdleThreadState)) t s; t = ksIdleThread s \<longrightarrow> idle' st; runnable' st \<and> obj_at' tcbQueued t s \<longrightarrow> st_tcb_at' runnable' t s; sch_act_simple s; valid_pspace' s; sch_act_wf (ksSchedulerAction s) s; valid_queues_no_bitmap s; valid_bitmapQ s; bitmapQ_no_L2_orphans s; bitmapQ_no_L1_orphans s; sym_refs (state_refs_of' s); if_live_then_nonz_cap' s; if_unsafe_then_cap' s; valid_idle' s; valid_global_refs' s; valid_arch_state' s; valid_irq_node' (irq_node' s) s; valid_irq_handlers' s; valid_irq_states' s; valid_machine_state' s; irqs_masked' s; valid_queues' s; ct_not_inQ s; ct_idle_or_in_cur_domain' s; valid_pde_mappings' s; pspace_domain_valid s; ksCurDomain s \<le> maxDomain; ksDomSchedule (newKernelState undefined) \<noteq> []; \<forall>x\<in>set (ksDomSchedule (newKernelState undefined)). dschDomain x \<le> maxDomain \<and> 0 < dschLength x; ksDomSchedule s = ksDomSchedule (newKernelState undefined); ksDomScheduleIdx s < length (ksDomSchedule (newKernelState undefined)); untyped_ranges_zero' s; cur_tcb' s\<rbrakk> \<Longrightarrow> st \<noteq> Structures_H.thread_state.Inactive \<and> st \<noteq> Structures_H.thread_state.IdleThreadState \<longrightarrow> ex_nonz_cap_to' t s
 7. \<And>s. \<lbrakk>st_tcb_at' (\<lambda>st'. tcb_st_refs_of' st' = tcb_st_refs_of' st \<and> (st \<noteq> Structures_H.thread_state.Inactive \<and> st \<noteq> Structures_H.thread_state.IdleThreadState \<longrightarrow> st' \<noteq> Structures_H.thread_state.Inactive \<and> st' \<noteq> Structures_H.thread_state.IdleThreadState)) t s; t = ksIdleThread s \<longrightarrow> idle' st; runnable' st \<and> obj_at' tcbQueued t s \<longrightarrow> st_tcb_at' runnable' t s; sch_act_simple s; valid_pspace' s; sch_act_wf (ksSchedulerAction s) s; valid_queues_no_bitmap s; valid_bitmapQ s; bitmapQ_no_L2_orphans s; bitmapQ_no_L1_orphans s; sym_refs (state_refs_of' s); if_live_then_nonz_cap' s; if_unsafe_then_cap' s; valid_idle' s; valid_global_refs' s; valid_arch_state' s; valid_irq_node' (irq_node' s) s; valid_irq_handlers' s; valid_irq_states' s; valid_machine_state' s; irqs_masked' s; valid_queues' s; ct_not_inQ s; ct_idle_or_in_cur_domain' s; valid_pde_mappings' s; pspace_domain_valid s; ksCurDomain s \<le> maxDomain; ksDomSchedule (newKernelState undefined) \<noteq> []; \<forall>x\<in>set (ksDomSchedule (newKernelState undefined)). dschDomain x \<le> maxDomain \<and> 0 < dschLength x; ksDomSchedule s = ksDomSchedule (newKernelState undefined); ksDomScheduleIdx s < length (ksDomSchedule (newKernelState undefined)); untyped_ranges_zero' s; cur_tcb' s\<rbrakk> \<Longrightarrow> tcb_at' t s proof (prove)
goal (6 subgoals):
 1. \<And>s x xa xb. \<lbrakk>st_tcb_at' (\<lambda>st'. tcb_st_refs_of' st' = tcb_st_refs_of' st \<and> (st \<noteq> Structures_H.thread_state.Inactive \<and> st \<noteq> Structures_H.thread_state.IdleThreadState \<longrightarrow> st' \<noteq> Structures_H.thread_state.Inactive \<and> st' \<noteq> Structures_H.thread_state.IdleThreadState)) t s; t = ksIdleThread s \<longrightarrow> idle' st; runnable' st \<and> obj_at' tcbQueued t s \<longrightarrow> st_tcb_at' runnable' t s; sch_act_simple s; valid_pspace' s; sch_act_wf (ksSchedulerAction s) s; valid_queues_no_bitmap s; valid_bitmapQ s; bitmapQ_no_L2_orphans s; bitmapQ_no_L1_orphans s; sym_refs (state_refs_of' s); if_live_then_nonz_cap' s; if_unsafe_then_cap' s; valid_idle' s; valid_global_refs' s; valid_arch_state' s; valid_irq_node' (irq_node' s) s; valid_irq_handlers' s; valid_irq_states' s; valid_machine_state' s; irqs_masked' s; valid_queues' s; ct_not_inQ s; ct_idle_or_in_cur_domain' s; valid_pde_mappings' s; pspace_domain_valid s; ksCurDomain s \<le> maxDomain; ksDomSchedule (newKernelState undefined) \<noteq> []; \<forall>x\<in>set (ksDomSchedule (newKernelState undefined)). dschDomain x \<le> maxDomain \<and> 0 < dschLength x; ksDomSchedule s = ksDomSchedule (newKernelState undefined); ksDomScheduleIdx s < length (ksDomSchedule (newKernelState undefined)); untyped_ranges_zero' s; cur_tcb' s\<rbrakk> \<Longrightarrow> distinct (ksReadyQueues s (xa, xb)) \<and> (maxDomain < xa \<longrightarrow> ksReadyQueues s (xa, xb) = []) \<and> (maxPriority < xb \<longrightarrow> ksReadyQueues s (xa, xb) = [])
 2. \<And>s. \<lbrakk>st_tcb_at' (\<lambda>st'. tcb_st_refs_of' st' = tcb_st_refs_of' st \<and> (st \<noteq> Structures_H.thread_state.Inactive \<and> st \<noteq> Structures_H.thread_state.IdleThreadState \<longrightarrow> st' \<noteq> Structures_H.thread_state.Inactive \<and> st' \<noteq> Structures_H.thread_state.IdleThreadState)) t s; t = ksIdleThread s \<longrightarrow> idle' st; runnable' st \<and> obj_at' tcbQueued t s \<longrightarrow> st_tcb_at' runnable' t s; sch_act_simple s; valid_pspace' s; sch_act_wf (ksSchedulerAction s) s; valid_queues_no_bitmap s; valid_bitmapQ s; bitmapQ_no_L2_orphans s; bitmapQ_no_L1_orphans s; sym_refs (state_refs_of' s); if_live_then_nonz_cap' s; if_unsafe_then_cap' s; valid_idle' s; valid_global_refs' s; valid_arch_state' s; valid_irq_node' (irq_node' s) s; valid_irq_handlers' s; valid_irq_states' s; valid_machine_state' s; irqs_masked' s; valid_queues' s; ct_not_inQ s; ct_idle_or_in_cur_domain' s; valid_pde_mappings' s; pspace_domain_valid s; ksCurDomain s \<le> maxDomain; ksDomSchedule (newKernelState undefined) \<noteq> []; \<forall>x\<in>set (ksDomSchedule (newKernelState undefined)). dschDomain x \<le> maxDomain \<and> 0 < dschLength x; ksDomSchedule s = ksDomSchedule (newKernelState undefined); ksDomScheduleIdx s < length (ksDomSchedule (newKernelState undefined)); untyped_ranges_zero' s; cur_tcb' s\<rbrakk> \<Longrightarrow> tcb_at' t s
 3. \<And>s. \<lbrakk>st_tcb_at' (\<lambda>st'. tcb_st_refs_of' st' = tcb_st_refs_of' st \<and> (st \<noteq> Structures_H.thread_state.Inactive \<and> st \<noteq> Structures_H.thread_state.IdleThreadState \<longrightarrow> st' \<noteq> Structures_H.thread_state.Inactive \<and> st' \<noteq> Structures_H.thread_state.IdleThreadState)) t s; t = ksIdleThread s \<longrightarrow> idle' st; runnable' st \<and> obj_at' tcbQueued t s \<longrightarrow> st_tcb_at' runnable' t s; sch_act_simple s; valid_pspace' s; sch_act_wf (ksSchedulerAction s) s; valid_queues_no_bitmap s; valid_bitmapQ s; bitmapQ_no_L2_orphans s; bitmapQ_no_L1_orphans s; sym_refs (state_refs_of' s); if_live_then_nonz_cap' s; if_unsafe_then_cap' s; valid_idle' s; valid_global_refs' s; valid_arch_state' s; valid_irq_node' (irq_node' s) s; valid_irq_handlers' s; valid_irq_states' s; valid_machine_state' s; irqs_masked' s; valid_queues' s; ct_not_inQ s; ct_idle_or_in_cur_domain' s; valid_pde_mappings' s; pspace_domain_valid s; ksCurDomain s \<le> maxDomain; ksDomSchedule (newKernelState undefined) \<noteq> []; \<forall>x\<in>set (ksDomSchedule (newKernelState undefined)). dschDomain x \<le> maxDomain \<and> 0 < dschLength x; ksDomSchedule s = ksDomSchedule (newKernelState undefined); ksDomScheduleIdx s < length (ksDomSchedule (newKernelState undefined)); untyped_ranges_zero' s; cur_tcb' s\<rbrakk> \<Longrightarrow> valid_tcb_state' st s
 4. \<And>s. \<lbrakk>st_tcb_at' (\<lambda>st'. tcb_st_refs_of' st' = tcb_st_refs_of' st \<and> (st \<noteq> Structures_H.thread_state.Inactive \<and> st \<noteq> Structures_H.thread_state.IdleThreadState \<longrightarrow> st' \<noteq> Structures_H.thread_state.Inactive \<and> st' \<noteq> Structures_H.thread_state.IdleThreadState)) t s; t = ksIdleThread s \<longrightarrow> idle' st; runnable' st \<and> obj_at' tcbQueued t s \<longrightarrow> st_tcb_at' runnable' t s; sch_act_simple s; valid_pspace' s; sch_act_wf (ksSchedulerAction s) s; valid_queues_no_bitmap s; valid_bitmapQ s; bitmapQ_no_L2_orphans s; bitmapQ_no_L1_orphans s; sym_refs (state_refs_of' s); if_live_then_nonz_cap' s; if_unsafe_then_cap' s; valid_idle' s; valid_global_refs' s; valid_arch_state' s; valid_irq_node' (irq_node' s) s; valid_irq_handlers' s; valid_irq_states' s; valid_machine_state' s; irqs_masked' s; valid_queues' s; ct_not_inQ s; ct_idle_or_in_cur_domain' s; valid_pde_mappings' s; pspace_domain_valid s; ksCurDomain s \<le> maxDomain; ksDomSchedule (newKernelState undefined) \<noteq> []; \<forall>x\<in>set (ksDomSchedule (newKernelState undefined)). dschDomain x \<le> maxDomain \<and> 0 < dschLength x; ksDomSchedule s = ksDomSchedule (newKernelState undefined); ksDomScheduleIdx s < length (ksDomSchedule (newKernelState undefined)); untyped_ranges_zero' s; cur_tcb' s\<rbrakk> \<Longrightarrow> sym_refs (\<lambda>a. if a = t then tcb_st_refs_of' st \<union> {r \<in> state_refs_of' s t. snd r = TCBBound} else state_refs_of' s a)
 5. \<And>s. \<lbrakk>st_tcb_at' (\<lambda>st'. tcb_st_refs_of' st' = tcb_st_refs_of' st \<and> (st \<noteq> Structures_H.thread_state.Inactive \<and> st \<noteq> Structures_H.thread_state.IdleThreadState \<longrightarrow> st' \<noteq> Structures_H.thread_state.Inactive \<and> st' \<noteq> Structures_H.thread_state.IdleThreadState)) t s; t = ksIdleThread s \<longrightarrow> idle' st; runnable' st \<and> obj_at' tcbQueued t s \<longrightarrow> st_tcb_at' runnable' t s; sch_act_simple s; valid_pspace' s; sch_act_wf (ksSchedulerAction s) s; valid_queues_no_bitmap s; valid_bitmapQ s; bitmapQ_no_L2_orphans s; bitmapQ_no_L1_orphans s; sym_refs (state_refs_of' s); if_live_then_nonz_cap' s; if_unsafe_then_cap' s; valid_idle' s; valid_global_refs' s; valid_arch_state' s; valid_irq_node' (irq_node' s) s; valid_irq_handlers' s; valid_irq_states' s; valid_machine_state' s; irqs_masked' s; valid_queues' s; ct_not_inQ s; ct_idle_or_in_cur_domain' s; valid_pde_mappings' s; pspace_domain_valid s; ksCurDomain s \<le> maxDomain; ksDomSchedule (newKernelState undefined) \<noteq> []; \<forall>x\<in>set (ksDomSchedule (newKernelState undefined)). dschDomain x \<le> maxDomain \<and> 0 < dschLength x; ksDomSchedule s = ksDomSchedule (newKernelState undefined); ksDomScheduleIdx s < length (ksDomSchedule (newKernelState undefined)); untyped_ranges_zero' s; cur_tcb' s\<rbrakk> \<Longrightarrow> st \<noteq> Structures_H.thread_state.Inactive \<and> st \<noteq> Structures_H.thread_state.IdleThreadState \<longrightarrow> ex_nonz_cap_to' t s
 6. \<And>s. \<lbrakk>st_tcb_at' (\<lambda>st'. tcb_st_refs_of' st' = tcb_st_refs_of' st \<and> (st \<noteq> Structures_H.thread_state.Inactive \<and> st \<noteq> Structures_H.thread_state.IdleThreadState \<longrightarrow> st' \<noteq> Structures_H.thread_state.Inactive \<and> st' \<noteq> Structures_H.thread_state.IdleThreadState)) t s; t = ksIdleThread s \<longrightarrow> idle' st; runnable' st \<and> obj_at' tcbQueued t s \<longrightarrow> st_tcb_at' runnable' t s; sch_act_simple s; valid_pspace' s; sch_act_wf (ksSchedulerAction s) s; valid_queues_no_bitmap s; valid_bitmapQ s; bitmapQ_no_L2_orphans s; bitmapQ_no_L1_orphans s; sym_refs (state_refs_of' s); if_live_then_nonz_cap' s; if_unsafe_then_cap' s; valid_idle' s; valid_global_refs' s; valid_arch_state' s; valid_irq_node' (irq_node' s) s; valid_irq_handlers' s; valid_irq_states' s; valid_machine_state' s; irqs_masked' s; valid_queues' s; ct_not_inQ s; ct_idle_or_in_cur_domain' s; valid_pde_mappings' s; pspace_domain_valid s; ksCurDomain s \<le> maxDomain; ksDomSchedule (newKernelState undefined) \<noteq> []; \<forall>x\<in>set (ksDomSchedule (newKernelState undefined)). dschDomain x \<le> maxDomain \<and> 0 < dschLength x; ksDomSchedule s = ksDomSchedule (newKernelState undefined); ksDomScheduleIdx s < length (ksDomSchedule (newKernelState undefined)); untyped_ranges_zero' s; cur_tcb' s\<rbrakk> \<Longrightarrow> tcb_at' t s proof (prove)
goal (5 subgoals):
 1. \<And>s. \<lbrakk>st_tcb_at' (\<lambda>st'. tcb_st_refs_of' st' = tcb_st_refs_of' st \<and> (st \<noteq> Structures_H.thread_state.Inactive \<and> st \<noteq> Structures_H.thread_state.IdleThreadState \<longrightarrow> st' \<noteq> Structures_H.thread_state.Inactive \<and> st' \<noteq> Structures_H.thread_state.IdleThreadState)) t s; t = ksIdleThread s \<longrightarrow> idle' st; runnable' st \<and> obj_at' tcbQueued t s \<longrightarrow> st_tcb_at' runnable' t s; sch_act_simple s; valid_pspace' s; sch_act_wf (ksSchedulerAction s) s; valid_queues_no_bitmap s; valid_bitmapQ s; bitmapQ_no_L2_orphans s; bitmapQ_no_L1_orphans s; sym_refs (state_refs_of' s); if_live_then_nonz_cap' s; if_unsafe_then_cap' s; valid_idle' s; valid_global_refs' s; valid_arch_state' s; valid_irq_node' (irq_node' s) s; valid_irq_handlers' s; valid_irq_states' s; valid_machine_state' s; irqs_masked' s; valid_queues' s; ct_not_inQ s; ct_idle_or_in_cur_domain' s; valid_pde_mappings' s; pspace_domain_valid s; ksCurDomain s \<le> maxDomain; ksDomSchedule (newKernelState undefined) \<noteq> []; \<forall>x\<in>set (ksDomSchedule (newKernelState undefined)). dschDomain x \<le> maxDomain \<and> 0 < dschLength x; ksDomSchedule s = ksDomSchedule (newKernelState undefined); ksDomScheduleIdx s < length (ksDomSchedule (newKernelState undefined)); untyped_ranges_zero' s; cur_tcb' s\<rbrakk> \<Longrightarrow> tcb_at' t s
 2. \<And>s. \<lbrakk>st_tcb_at' (\<lambda>st'. tcb_st_refs_of' st' = tcb_st_refs_of' st \<and> (st \<noteq> Structures_H.thread_state.Inactive \<and> st \<noteq> Structures_H.thread_state.IdleThreadState \<longrightarrow> st' \<noteq> Structures_H.thread_state.Inactive \<and> st' \<noteq> Structures_H.thread_state.IdleThreadState)) t s; t = ksIdleThread s \<longrightarrow> idle' st; runnable' st \<and> obj_at' tcbQueued t s \<longrightarrow> st_tcb_at' runnable' t s; sch_act_simple s; valid_pspace' s; sch_act_wf (ksSchedulerAction s) s; valid_queues_no_bitmap s; valid_bitmapQ s; bitmapQ_no_L2_orphans s; bitmapQ_no_L1_orphans s; sym_refs (state_refs_of' s); if_live_then_nonz_cap' s; if_unsafe_then_cap' s; valid_idle' s; valid_global_refs' s; valid_arch_state' s; valid_irq_node' (irq_node' s) s; valid_irq_handlers' s; valid_irq_states' s; valid_machine_state' s; irqs_masked' s; valid_queues' s; ct_not_inQ s; ct_idle_or_in_cur_domain' s; valid_pde_mappings' s; pspace_domain_valid s; ksCurDomain s \<le> maxDomain; ksDomSchedule (newKernelState undefined) \<noteq> []; \<forall>x\<in>set (ksDomSchedule (newKernelState undefined)). dschDomain x \<le> maxDomain \<and> 0 < dschLength x; ksDomSchedule s = ksDomSchedule (newKernelState undefined); ksDomScheduleIdx s < length (ksDomSchedule (newKernelState undefined)); untyped_ranges_zero' s; cur_tcb' s\<rbrakk> \<Longrightarrow> valid_tcb_state' st s
 3. \<And>s. \<lbrakk>st_tcb_at' (\<lambda>st'. tcb_st_refs_of' st' = tcb_st_refs_of' st \<and> (st \<noteq> Structures_H.thread_state.Inactive \<and> st \<noteq> Structures_H.thread_state.IdleThreadState \<longrightarrow> st' \<noteq> Structures_H.thread_state.Inactive \<and> st' \<noteq> Structures_H.thread_state.IdleThreadState)) t s; t = ksIdleThread s \<longrightarrow> idle' st; runnable' st \<and> obj_at' tcbQueued t s \<longrightarrow> st_tcb_at' runnable' t s; sch_act_simple s; valid_pspace' s; sch_act_wf (ksSchedulerAction s) s; valid_queues_no_bitmap s; valid_bitmapQ s; bitmapQ_no_L2_orphans s; bitmapQ_no_L1_orphans s; sym_refs (state_refs_of' s); if_live_then_nonz_cap' s; if_unsafe_then_cap' s; valid_idle' s; valid_global_refs' s; valid_arch_state' s; valid_irq_node' (irq_node' s) s; valid_irq_handlers' s; valid_irq_states' s; valid_machine_state' s; irqs_masked' s; valid_queues' s; ct_not_inQ s; ct_idle_or_in_cur_domain' s; valid_pde_mappings' s; pspace_domain_valid s; ksCurDomain s \<le> maxDomain; ksDomSchedule (newKernelState undefined) \<noteq> []; \<forall>x\<in>set (ksDomSchedule (newKernelState undefined)). dschDomain x \<le> maxDomain \<and> 0 < dschLength x; ksDomSchedule s = ksDomSchedule (newKernelState undefined); ksDomScheduleIdx s < length (ksDomSchedule (newKernelState undefined)); untyped_ranges_zero' s; cur_tcb' s\<rbrakk> \<Longrightarrow> sym_refs (\<lambda>a. if a = t then tcb_st_refs_of' st \<union> {r \<in> state_refs_of' s t. snd r = TCBBound} else state_refs_of' s a)
 4. \<And>s. \<lbrakk>st_tcb_at' (\<lambda>st'. tcb_st_refs_of' st' = tcb_st_refs_of' st \<and> (st \<noteq> Structures_H.thread_state.Inactive \<and> st \<noteq> Structures_H.thread_state.IdleThreadState \<longrightarrow> st' \<noteq> Structures_H.thread_state.Inactive \<and> st' \<noteq> Structures_H.thread_state.IdleThreadState)) t s; t = ksIdleThread s \<longrightarrow> idle' st; runnable' st \<and> obj_at' tcbQueued t s \<longrightarrow> st_tcb_at' runnable' t s; sch_act_simple s; valid_pspace' s; sch_act_wf (ksSchedulerAction s) s; valid_queues_no_bitmap s; valid_bitmapQ s; bitmapQ_no_L2_orphans s; bitmapQ_no_L1_orphans s; sym_refs (state_refs_of' s); if_live_then_nonz_cap' s; if_unsafe_then_cap' s; valid_idle' s; valid_global_refs' s; valid_arch_state' s; valid_irq_node' (irq_node' s) s; valid_irq_handlers' s; valid_irq_states' s; valid_machine_state' s; irqs_masked' s; valid_queues' s; ct_not_inQ s; ct_idle_or_in_cur_domain' s; valid_pde_mappings' s; pspace_domain_valid s; ksCurDomain s \<le> maxDomain; ksDomSchedule (newKernelState undefined) \<noteq> []; \<forall>x\<in>set (ksDomSchedule (newKernelState undefined)). dschDomain x \<le> maxDomain \<and> 0 < dschLength x; ksDomSchedule s = ksDomSchedule (newKernelState undefined); ksDomScheduleIdx s < length (ksDomSchedule (newKernelState undefined)); untyped_ranges_zero' s; cur_tcb' s\<rbrakk> \<Longrightarrow> st \<noteq> Structures_H.thread_state.Inactive \<and> st \<noteq> Structures_H.thread_state.IdleThreadState \<longrightarrow> ex_nonz_cap_to' t s
 5. \<And>s. \<lbrakk>st_tcb_at' (\<lambda>st'. tcb_st_refs_of' st' = tcb_st_refs_of' st \<and> (st \<noteq> Structures_H.thread_state.Inactive \<and> st \<noteq> Structures_H.thread_state.IdleThreadState \<longrightarrow> st' \<noteq> Structures_H.thread_state.Inactive \<and> st' \<noteq> Structures_H.thread_state.IdleThreadState)) t s; t = ksIdleThread s \<longrightarrow> idle' st; runnable' st \<and> obj_at' tcbQueued t s \<longrightarrow> st_tcb_at' runnable' t s; sch_act_simple s; valid_pspace' s; sch_act_wf (ksSchedulerAction s) s; valid_queues_no_bitmap s; valid_bitmapQ s; bitmapQ_no_L2_orphans s; bitmapQ_no_L1_orphans s; sym_refs (state_refs_of' s); if_live_then_nonz_cap' s; if_unsafe_then_cap' s; valid_idle' s; valid_global_refs' s; valid_arch_state' s; valid_irq_node' (irq_node' s) s; valid_irq_handlers' s; valid_irq_states' s; valid_machine_state' s; irqs_masked' s; valid_queues' s; ct_not_inQ s; ct_idle_or_in_cur_domain' s; valid_pde_mappings' s; pspace_domain_valid s; ksCurDomain s \<le> maxDomain; ksDomSchedule (newKernelState undefined) \<noteq> []; \<forall>x\<in>set (ksDomSchedule (newKernelState undefined)). dschDomain x \<le> maxDomain \<and> 0 < dschLength x; ksDomSchedule s = ksDomSchedule (newKernelState undefined); ksDomScheduleIdx s < length (ksDomSchedule (newKernelState undefined)); untyped_ranges_zero' s; cur_tcb' s\<rbrakk> \<Longrightarrow> tcb_at' t s proof (prove)
goal (4 subgoals):
 1. \<And>s. \<lbrakk>st_tcb_at' (\<lambda>st'. tcb_st_refs_of' st' = tcb_st_refs_of' st \<and> (st \<noteq> Structures_H.thread_state.Inactive \<and> st \<noteq> Structures_H.thread_state.IdleThreadState \<longrightarrow> st' \<noteq> Structures_H.thread_state.Inactive \<and> st' \<noteq> Structures_H.thread_state.IdleThreadState)) t s; t = ksIdleThread s \<longrightarrow> idle' st; runnable' st \<and> obj_at' tcbQueued t s \<longrightarrow> st_tcb_at' runnable' t s; sch_act_simple s; valid_pspace' s; sch_act_wf (ksSchedulerAction s) s; valid_queues_no_bitmap s; valid_bitmapQ s; bitmapQ_no_L2_orphans s; bitmapQ_no_L1_orphans s; sym_refs (state_refs_of' s); if_live_then_nonz_cap' s; if_unsafe_then_cap' s; valid_idle' s; valid_global_refs' s; valid_arch_state' s; valid_irq_node' (irq_node' s) s; valid_irq_handlers' s; valid_irq_states' s; valid_machine_state' s; irqs_masked' s; valid_queues' s; ct_not_inQ s; ct_idle_or_in_cur_domain' s; valid_pde_mappings' s; pspace_domain_valid s; ksCurDomain s \<le> maxDomain; ksDomSchedule (newKernelState undefined) \<noteq> []; \<forall>x\<in>set (ksDomSchedule (newKernelState undefined)). dschDomain x \<le> maxDomain \<and> 0 < dschLength x; ksDomSchedule s = ksDomSchedule (newKernelState undefined); ksDomScheduleIdx s < length (ksDomSchedule (newKernelState undefined)); untyped_ranges_zero' s; cur_tcb' s\<rbrakk> \<Longrightarrow> valid_tcb_state' st s
 2. \<And>s. \<lbrakk>st_tcb_at' (\<lambda>st'. tcb_st_refs_of' st' = tcb_st_refs_of' st \<and> (st \<noteq> Structures_H.thread_state.Inactive \<and> st \<noteq> Structures_H.thread_state.IdleThreadState \<longrightarrow> st' \<noteq> Structures_H.thread_state.Inactive \<and> st' \<noteq> Structures_H.thread_state.IdleThreadState)) t s; t = ksIdleThread s \<longrightarrow> idle' st; runnable' st \<and> obj_at' tcbQueued t s \<longrightarrow> st_tcb_at' runnable' t s; sch_act_simple s; valid_pspace' s; sch_act_wf (ksSchedulerAction s) s; valid_queues_no_bitmap s; valid_bitmapQ s; bitmapQ_no_L2_orphans s; bitmapQ_no_L1_orphans s; sym_refs (state_refs_of' s); if_live_then_nonz_cap' s; if_unsafe_then_cap' s; valid_idle' s; valid_global_refs' s; valid_arch_state' s; valid_irq_node' (irq_node' s) s; valid_irq_handlers' s; valid_irq_states' s; valid_machine_state' s; irqs_masked' s; valid_queues' s; ct_not_inQ s; ct_idle_or_in_cur_domain' s; valid_pde_mappings' s; pspace_domain_valid s; ksCurDomain s \<le> maxDomain; ksDomSchedule (newKernelState undefined) \<noteq> []; \<forall>x\<in>set (ksDomSchedule (newKernelState undefined)). dschDomain x \<le> maxDomain \<and> 0 < dschLength x; ksDomSchedule s = ksDomSchedule (newKernelState undefined); ksDomScheduleIdx s < length (ksDomSchedule (newKernelState undefined)); untyped_ranges_zero' s; cur_tcb' s\<rbrakk> \<Longrightarrow> sym_refs (\<lambda>a. if a = t then tcb_st_refs_of' st \<union> {r \<in> state_refs_of' s t. snd r = TCBBound} else state_refs_of' s a)
 3. \<And>s. \<lbrakk>st_tcb_at' (\<lambda>st'. tcb_st_refs_of' st' = tcb_st_refs_of' st \<and> (st \<noteq> Structures_H.thread_state.Inactive \<and> st \<noteq> Structures_H.thread_state.IdleThreadState \<longrightarrow> st' \<noteq> Structures_H.thread_state.Inactive \<and> st' \<noteq> Structures_H.thread_state.IdleThreadState)) t s; t = ksIdleThread s \<longrightarrow> idle' st; runnable' st \<and> obj_at' tcbQueued t s \<longrightarrow> st_tcb_at' runnable' t s; sch_act_simple s; valid_pspace' s; sch_act_wf (ksSchedulerAction s) s; valid_queues_no_bitmap s; valid_bitmapQ s; bitmapQ_no_L2_orphans s; bitmapQ_no_L1_orphans s; sym_refs (state_refs_of' s); if_live_then_nonz_cap' s; if_unsafe_then_cap' s; valid_idle' s; valid_global_refs' s; valid_arch_state' s; valid_irq_node' (irq_node' s) s; valid_irq_handlers' s; valid_irq_states' s; valid_machine_state' s; irqs_masked' s; valid_queues' s; ct_not_inQ s; ct_idle_or_in_cur_domain' s; valid_pde_mappings' s; pspace_domain_valid s; ksCurDomain s \<le> maxDomain; ksDomSchedule (newKernelState undefined) \<noteq> []; \<forall>x\<in>set (ksDomSchedule (newKernelState undefined)). dschDomain x \<le> maxDomain \<and> 0 < dschLength x; ksDomSchedule s = ksDomSchedule (newKernelState undefined); ksDomScheduleIdx s < length (ksDomSchedule (newKernelState undefined)); untyped_ranges_zero' s; cur_tcb' s\<rbrakk> \<Longrightarrow> st \<noteq> Structures_H.thread_state.Inactive \<and> st \<noteq> Structures_H.thread_state.IdleThreadState \<longrightarrow> ex_nonz_cap_to' t s
 4. \<And>s. \<lbrakk>st_tcb_at' (\<lambda>st'. tcb_st_refs_of' st' = tcb_st_refs_of' st \<and> (st \<noteq> Structures_H.thread_state.Inactive \<and> st \<noteq> Structures_H.thread_state.IdleThreadState \<longrightarrow> st' \<noteq> Structures_H.thread_state.Inactive \<and> st' \<noteq> Structures_H.thread_state.IdleThreadState)) t s; t = ksIdleThread s \<longrightarrow> idle' st; runnable' st \<and> obj_at' tcbQueued t s \<longrightarrow> st_tcb_at' runnable' t s; sch_act_simple s; valid_pspace' s; sch_act_wf (ksSchedulerAction s) s; valid_queues_no_bitmap s; valid_bitmapQ s; bitmapQ_no_L2_orphans s; bitmapQ_no_L1_orphans s; sym_refs (state_refs_of' s); if_live_then_nonz_cap' s; if_unsafe_then_cap' s; valid_idle' s; valid_global_refs' s; valid_arch_state' s; valid_irq_node' (irq_node' s) s; valid_irq_handlers' s; valid_irq_states' s; valid_machine_state' s; irqs_masked' s; valid_queues' s; ct_not_inQ s; ct_idle_or_in_cur_domain' s; valid_pde_mappings' s; pspace_domain_valid s; ksCurDomain s \<le> maxDomain; ksDomSchedule (newKernelState undefined) \<noteq> []; \<forall>x\<in>set (ksDomSchedule (newKernelState undefined)). dschDomain x \<le> maxDomain \<and> 0 < dschLength x; ksDomSchedule s = ksDomSchedule (newKernelState undefined); ksDomScheduleIdx s < length (ksDomSchedule (newKernelState undefined)); untyped_ranges_zero' s; cur_tcb' s\<rbrakk> \<Longrightarrow> tcb_at' t s proof (prove)
goal (4 subgoals):
 1. \<And>s. \<lbrakk>obj_at' ((\<lambda>st'. tcb_st_refs_of' st' = tcb_st_refs_of' st \<and> (st \<noteq> Structures_H.thread_state.Inactive \<and> st \<noteq> Structures_H.thread_state.IdleThreadState \<longrightarrow> st' \<noteq> Structures_H.thread_state.Inactive \<and> st' \<noteq> Structures_H.thread_state.IdleThreadState)) \<circ> tcbState) t s; t = ksIdleThread s \<longrightarrow> idle' st; runnable' st \<and> obj_at' tcbQueued t s \<longrightarrow> obj_at' (runnable' \<circ> tcbState) t s; sch_act_simple s; valid_pspace' s; sch_act_wf (ksSchedulerAction s) s; valid_queues_no_bitmap s; valid_bitmapQ s; bitmapQ_no_L2_orphans s; bitmapQ_no_L1_orphans s; sym_refs (state_refs_of' s); if_live_then_nonz_cap' s; if_unsafe_then_cap' s; valid_idle' s; valid_global_refs' s; valid_arch_state' s; valid_irq_node' (irq_node' s) s; valid_irq_handlers' s; valid_irq_states' s; valid_machine_state' s; irqs_masked' s; valid_queues' s; ct_not_inQ s; ct_idle_or_in_cur_domain' s; valid_pde_mappings' s; pspace_domain_valid s; ksCurDomain s \<le> maxDomain; ksDomSchedule (newKernelState undefined) \<noteq> []; \<forall>x\<in>set (ksDomSchedule (newKernelState undefined)). dschDomain x \<le> maxDomain \<and> 0 < dschLength x; ksDomSchedule s = ksDomSchedule (newKernelState undefined); ksDomScheduleIdx s < length (ksDomSchedule (newKernelState undefined)); untyped_ranges_zero' s; cur_tcb' s\<rbrakk> \<Longrightarrow> valid_tcb_state' st s
 2. \<And>s. \<lbrakk>st_tcb_at' (\<lambda>st'. tcb_st_refs_of' st' = tcb_st_refs_of' st \<and> (st \<noteq> Structures_H.thread_state.Inactive \<and> st \<noteq> Structures_H.thread_state.IdleThreadState \<longrightarrow> st' \<noteq> Structures_H.thread_state.Inactive \<and> st' \<noteq> Structures_H.thread_state.IdleThreadState)) t s; t = ksIdleThread s \<longrightarrow> idle' st; runnable' st \<and> obj_at' tcbQueued t s \<longrightarrow> st_tcb_at' runnable' t s; sch_act_simple s; valid_pspace' s; sch_act_wf (ksSchedulerAction s) s; valid_queues_no_bitmap s; valid_bitmapQ s; bitmapQ_no_L2_orphans s; bitmapQ_no_L1_orphans s; sym_refs (state_refs_of' s); if_live_then_nonz_cap' s; if_unsafe_then_cap' s; valid_idle' s; valid_global_refs' s; valid_arch_state' s; valid_irq_node' (irq_node' s) s; valid_irq_handlers' s; valid_irq_states' s; valid_machine_state' s; irqs_masked' s; valid_queues' s; ct_not_inQ s; ct_idle_or_in_cur_domain' s; valid_pde_mappings' s; pspace_domain_valid s; ksCurDomain s \<le> maxDomain; ksDomSchedule (newKernelState undefined) \<noteq> []; \<forall>x\<in>set (ksDomSchedule (newKernelState undefined)). dschDomain x \<le> maxDomain \<and> 0 < dschLength x; ksDomSchedule s = ksDomSchedule (newKernelState undefined); ksDomScheduleIdx s < length (ksDomSchedule (newKernelState undefined)); untyped_ranges_zero' s; cur_tcb' s\<rbrakk> \<Longrightarrow> sym_refs (\<lambda>a. if a = t then tcb_st_refs_of' st \<union> {r \<in> state_refs_of' s t. snd r = TCBBound} else state_refs_of' s a)
 3. \<And>s. \<lbrakk>st_tcb_at' (\<lambda>st'. tcb_st_refs_of' st' = tcb_st_refs_of' st \<and> (st \<noteq> Structures_H.thread_state.Inactive \<and> st \<noteq> Structures_H.thread_state.IdleThreadState \<longrightarrow> st' \<noteq> Structures_H.thread_state.Inactive \<and> st' \<noteq> Structures_H.thread_state.IdleThreadState)) t s; t = ksIdleThread s \<longrightarrow> idle' st; runnable' st \<and> obj_at' tcbQueued t s \<longrightarrow> st_tcb_at' runnable' t s; sch_act_simple s; valid_pspace' s; sch_act_wf (ksSchedulerAction s) s; valid_queues_no_bitmap s; valid_bitmapQ s; bitmapQ_no_L2_orphans s; bitmapQ_no_L1_orphans s; sym_refs (state_refs_of' s); if_live_then_nonz_cap' s; if_unsafe_then_cap' s; valid_idle' s; valid_global_refs' s; valid_arch_state' s; valid_irq_node' (irq_node' s) s; valid_irq_handlers' s; valid_irq_states' s; valid_machine_state' s; irqs_masked' s; valid_queues' s; ct_not_inQ s; ct_idle_or_in_cur_domain' s; valid_pde_mappings' s; pspace_domain_valid s; ksCurDomain s \<le> maxDomain; ksDomSchedule (newKernelState undefined) \<noteq> []; \<forall>x\<in>set (ksDomSchedule (newKernelState undefined)). dschDomain x \<le> maxDomain \<and> 0 < dschLength x; ksDomSchedule s = ksDomSchedule (newKernelState undefined); ksDomScheduleIdx s < length (ksDomSchedule (newKernelState undefined)); untyped_ranges_zero' s; cur_tcb' s\<rbrakk> \<Longrightarrow> st \<noteq> Structures_H.thread_state.Inactive \<and> st \<noteq> Structures_H.thread_state.IdleThreadState \<longrightarrow> ex_nonz_cap_to' t s
 4. \<And>s. \<lbrakk>st_tcb_at' (\<lambda>st'. tcb_st_refs_of' st' = tcb_st_refs_of' st \<and> (st \<noteq> Structures_H.thread_state.Inactive \<and> st \<noteq> Structures_H.thread_state.IdleThreadState \<longrightarrow> st' \<noteq> Structures_H.thread_state.Inactive \<and> st' \<noteq> Structures_H.thread_state.IdleThreadState)) t s; t = ksIdleThread s \<longrightarrow> idle' st; runnable' st \<and> obj_at' tcbQueued t s \<longrightarrow> st_tcb_at' runnable' t s; sch_act_simple s; valid_pspace' s; sch_act_wf (ksSchedulerAction s) s; valid_queues_no_bitmap s; valid_bitmapQ s; bitmapQ_no_L2_orphans s; bitmapQ_no_L1_orphans s; sym_refs (state_refs_of' s); if_live_then_nonz_cap' s; if_unsafe_then_cap' s; valid_idle' s; valid_global_refs' s; valid_arch_state' s; valid_irq_node' (irq_node' s) s; valid_irq_handlers' s; valid_irq_states' s; valid_machine_state' s; irqs_masked' s; valid_queues' s; ct_not_inQ s; ct_idle_or_in_cur_domain' s; valid_pde_mappings' s; pspace_domain_valid s; ksCurDomain s \<le> maxDomain; ksDomSchedule (newKernelState undefined) \<noteq> []; \<forall>x\<in>set (ksDomSchedule (newKernelState undefined)). dschDomain x \<le> maxDomain \<and> 0 < dschLength x; ksDomSchedule s = ksDomSchedule (newKernelState undefined); ksDomScheduleIdx s < length (ksDomSchedule (newKernelState undefined)); untyped_ranges_zero' s; cur_tcb' s\<rbrakk> \<Longrightarrow> tcb_at' t s proof (prove)
goal (5 subgoals):
 1. \<And>s. \<lbrakk>t = ksIdleThread s \<longrightarrow> idle' st; runnable' st \<and> obj_at' tcbQueued t s \<longrightarrow> obj_at' (runnable' \<circ> tcbState) t s; sch_act_simple s; valid_pspace' s; sch_act_wf (ksSchedulerAction s) s; valid_queues_no_bitmap s; valid_bitmapQ s; bitmapQ_no_L2_orphans s; bitmapQ_no_L1_orphans s; sym_refs (state_refs_of' s); if_live_then_nonz_cap' s; if_unsafe_then_cap' s; valid_idle' s; valid_global_refs' s; valid_arch_state' s; valid_irq_node' (irq_node' s) s; valid_irq_handlers' s; valid_irq_states' s; valid_machine_state' s; irqs_masked' s; valid_queues' s; ct_not_inQ s; ct_idle_or_in_cur_domain' s; valid_pde_mappings' s; pspace_domain_valid s; ksCurDomain s \<le> maxDomain; ksDomSchedule (newKernelState undefined) \<noteq> []; \<forall>x\<in>set (ksDomSchedule (newKernelState undefined)). dschDomain x \<le> maxDomain \<and> 0 < dschLength x; ksDomSchedule s = ksDomSchedule (newKernelState undefined); ksDomScheduleIdx s < length (ksDomSchedule (newKernelState undefined)); untyped_ranges_zero' s; cur_tcb' s\<rbrakk> \<Longrightarrow> valid_objs' s
 2. \<And>s. \<lbrakk>t = ksIdleThread s \<longrightarrow> idle' st; runnable' st \<and> obj_at' tcbQueued t s \<longrightarrow> obj_at' (runnable' \<circ> tcbState) t s; sch_act_simple s; valid_pspace' s; sch_act_wf (ksSchedulerAction s) s; valid_queues_no_bitmap s; valid_bitmapQ s; bitmapQ_no_L2_orphans s; bitmapQ_no_L1_orphans s; sym_refs (state_refs_of' s); if_live_then_nonz_cap' s; if_unsafe_then_cap' s; valid_idle' s; valid_global_refs' s; valid_arch_state' s; valid_irq_node' (irq_node' s) s; valid_irq_handlers' s; valid_irq_states' s; valid_machine_state' s; irqs_masked' s; valid_queues' s; ct_not_inQ s; ct_idle_or_in_cur_domain' s; valid_pde_mappings' s; pspace_domain_valid s; ksCurDomain s \<le> maxDomain; ksDomSchedule (newKernelState undefined) \<noteq> []; \<forall>x\<in>set (ksDomSchedule (newKernelState undefined)). dschDomain x \<le> maxDomain \<and> 0 < dschLength x; ksDomSchedule s = ksDomSchedule (newKernelState undefined); ksDomScheduleIdx s < length (ksDomSchedule (newKernelState undefined)); untyped_ranges_zero' s; cur_tcb' s; \<exists>k. ((\<lambda>st'. tcb_st_refs_of' st' = tcb_st_refs_of' st \<and> (st \<noteq> Structures_H.thread_state.Inactive \<and> st \<noteq> Structures_H.thread_state.IdleThreadState \<longrightarrow> st' \<noteq> Structures_H.thread_state.Inactive \<and> st' \<noteq> Structures_H.thread_state.IdleThreadState)) \<circ> tcbState) k \<and> ((\<forall>ko. projectKO_opt ko = Some k \<longrightarrow> injectKO k = ko) \<longrightarrow> valid_obj' (injectKO k) s)\<rbrakk> \<Longrightarrow> valid_tcb_state' st s
 3. \<And>s. \<lbrakk>st_tcb_at' (\<lambda>st'. tcb_st_refs_of' st' = tcb_st_refs_of' st \<and> (st \<noteq> Structures_H.thread_state.Inactive \<and> st \<noteq> Structures_H.thread_state.IdleThreadState \<longrightarrow> st' \<noteq> Structures_H.thread_state.Inactive \<and> st' \<noteq> Structures_H.thread_state.IdleThreadState)) t s; t = ksIdleThread s \<longrightarrow> idle' st; runnable' st \<and> obj_at' tcbQueued t s \<longrightarrow> st_tcb_at' runnable' t s; sch_act_simple s; valid_pspace' s; sch_act_wf (ksSchedulerAction s) s; valid_queues_no_bitmap s; valid_bitmapQ s; bitmapQ_no_L2_orphans s; bitmapQ_no_L1_orphans s; sym_refs (state_refs_of' s); if_live_then_nonz_cap' s; if_unsafe_then_cap' s; valid_idle' s; valid_global_refs' s; valid_arch_state' s; valid_irq_node' (irq_node' s) s; valid_irq_handlers' s; valid_irq_states' s; valid_machine_state' s; irqs_masked' s; valid_queues' s; ct_not_inQ s; ct_idle_or_in_cur_domain' s; valid_pde_mappings' s; pspace_domain_valid s; ksCurDomain s \<le> maxDomain; ksDomSchedule (newKernelState undefined) \<noteq> []; \<forall>x\<in>set (ksDomSchedule (newKernelState undefined)). dschDomain x \<le> maxDomain \<and> 0 < dschLength x; ksDomSchedule s = ksDomSchedule (newKernelState undefined); ksDomScheduleIdx s < length (ksDomSchedule (newKernelState undefined)); untyped_ranges_zero' s; cur_tcb' s\<rbrakk> \<Longrightarrow> sym_refs (\<lambda>a. if a = t then tcb_st_refs_of' st \<union> {r \<in> state_refs_of' s t. snd r = TCBBound} else state_refs_of' s a)
 4. \<And>s. \<lbrakk>st_tcb_at' (\<lambda>st'. tcb_st_refs_of' st' = tcb_st_refs_of' st \<and> (st \<noteq> Structures_H.thread_state.Inactive \<and> st \<noteq> Structures_H.thread_state.IdleThreadState \<longrightarrow> st' \<noteq> Structures_H.thread_state.Inactive \<and> st' \<noteq> Structures_H.thread_state.IdleThreadState)) t s; t = ksIdleThread s \<longrightarrow> idle' st; runnable' st \<and> obj_at' tcbQueued t s \<longrightarrow> st_tcb_at' runnable' t s; sch_act_simple s; valid_pspace' s; sch_act_wf (ksSchedulerAction s) s; valid_queues_no_bitmap s; valid_bitmapQ s; bitmapQ_no_L2_orphans s; bitmapQ_no_L1_orphans s; sym_refs (state_refs_of' s); if_live_then_nonz_cap' s; if_unsafe_then_cap' s; valid_idle' s; valid_global_refs' s; valid_arch_state' s; valid_irq_node' (irq_node' s) s; valid_irq_handlers' s; valid_irq_states' s; valid_machine_state' s; irqs_masked' s; valid_queues' s; ct_not_inQ s; ct_idle_or_in_cur_domain' s; valid_pde_mappings' s; pspace_domain_valid s; ksCurDomain s \<le> maxDomain; ksDomSchedule (newKernelState undefined) \<noteq> []; \<forall>x\<in>set (ksDomSchedule (newKernelState undefined)). dschDomain x \<le> maxDomain \<and> 0 < dschLength x; ksDomSchedule s = ksDomSchedule (newKernelState undefined); ksDomScheduleIdx s < length (ksDomSchedule (newKernelState undefined)); untyped_ranges_zero' s; cur_tcb' s\<rbrakk> \<Longrightarrow> st \<noteq> Structures_H.thread_state.Inactive \<and> st \<noteq> Structures_H.thread_state.IdleThreadState \<longrightarrow> ex_nonz_cap_to' t s
 5. \<And>s. \<lbrakk>st_tcb_at' (\<lambda>st'. tcb_st_refs_of' st' = tcb_st_refs_of' st \<and> (st \<noteq> Structures_H.thread_state.Inactive \<and> st \<noteq> Structures_H.thread_state.IdleThreadState \<longrightarrow> st' \<noteq> Structures_H.thread_state.Inactive \<and> st' \<noteq> Structures_H.thread_state.IdleThreadState)) t s; t = ksIdleThread s \<longrightarrow> idle' st; runnable' st \<and> obj_at' tcbQueued t s \<longrightarrow> st_tcb_at' runnable' t s; sch_act_simple s; valid_pspace' s; sch_act_wf (ksSchedulerAction s) s; valid_queues_no_bitmap s; valid_bitmapQ s; bitmapQ_no_L2_orphans s; bitmapQ_no_L1_orphans s; sym_refs (state_refs_of' s); if_live_then_nonz_cap' s; if_unsafe_then_cap' s; valid_idle' s; valid_global_refs' s; valid_arch_state' s; valid_irq_node' (irq_node' s) s; valid_irq_handlers' s; valid_irq_states' s; valid_machine_state' s; irqs_masked' s; valid_queues' s; ct_not_inQ s; ct_idle_or_in_cur_domain' s; valid_pde_mappings' s; pspace_domain_valid s; ksCurDomain s \<le> maxDomain; ksDomSchedule (newKernelState undefined) \<noteq> []; \<forall>x\<in>set (ksDomSchedule (newKernelState undefined)). dschDomain x \<le> maxDomain \<and> 0 < dschLength x; ksDomSchedule s = ksDomSchedule (newKernelState undefined); ksDomScheduleIdx s < length (ksDomSchedule (newKernelState undefined)); untyped_ranges_zero' s; cur_tcb' s\<rbrakk> \<Longrightarrow> tcb_at' t s proof (prove)
goal (4 subgoals):
 1. \<And>s. \<lbrakk>t = ksIdleThread s \<longrightarrow> idle' st; runnable' st \<and> obj_at' tcbQueued t s \<longrightarrow> obj_at' (runnable' \<circ> tcbState) t s; sch_act_simple s; valid_pspace' s; sch_act_wf (ksSchedulerAction s) s; valid_queues_no_bitmap s; valid_bitmapQ s; bitmapQ_no_L2_orphans s; bitmapQ_no_L1_orphans s; sym_refs (state_refs_of' s); if_live_then_nonz_cap' s; if_unsafe_then_cap' s; valid_idle' s; valid_global_refs' s; valid_arch_state' s; valid_irq_node' (irq_node' s) s; valid_irq_handlers' s; valid_irq_states' s; valid_machine_state' s; irqs_masked' s; valid_queues' s; ct_not_inQ s; ct_idle_or_in_cur_domain' s; valid_pde_mappings' s; pspace_domain_valid s; ksCurDomain s \<le> maxDomain; ksDomSchedule (newKernelState undefined) \<noteq> []; \<forall>x\<in>set (ksDomSchedule (newKernelState undefined)). dschDomain x \<le> maxDomain \<and> 0 < dschLength x; ksDomSchedule s = ksDomSchedule (newKernelState undefined); ksDomScheduleIdx s < length (ksDomSchedule (newKernelState undefined)); untyped_ranges_zero' s; cur_tcb' s; \<exists>k. ((\<lambda>st'. tcb_st_refs_of' st' = tcb_st_refs_of' st \<and> (st \<noteq> Structures_H.thread_state.Inactive \<and> st \<noteq> Structures_H.thread_state.IdleThreadState \<longrightarrow> st' \<noteq> Structures_H.thread_state.Inactive \<and> st' \<noteq> Structures_H.thread_state.IdleThreadState)) \<circ> tcbState) k \<and> ((\<forall>ko. projectKO_opt ko = Some k \<longrightarrow> injectKO k = ko) \<longrightarrow> valid_obj' (injectKO k) s)\<rbrakk> \<Longrightarrow> valid_tcb_state' st s
 2. \<And>s. \<lbrakk>st_tcb_at' (\<lambda>st'. tcb_st_refs_of' st' = tcb_st_refs_of' st \<and> (st \<noteq> Structures_H.thread_state.Inactive \<and> st \<noteq> Structures_H.thread_state.IdleThreadState \<longrightarrow> st' \<noteq> Structures_H.thread_state.Inactive \<and> st' \<noteq> Structures_H.thread_state.IdleThreadState)) t s; t = ksIdleThread s \<longrightarrow> idle' st; runnable' st \<and> obj_at' tcbQueued t s \<longrightarrow> st_tcb_at' runnable' t s; sch_act_simple s; valid_pspace' s; sch_act_wf (ksSchedulerAction s) s; valid_queues_no_bitmap s; valid_bitmapQ s; bitmapQ_no_L2_orphans s; bitmapQ_no_L1_orphans s; sym_refs (state_refs_of' s); if_live_then_nonz_cap' s; if_unsafe_then_cap' s; valid_idle' s; valid_global_refs' s; valid_arch_state' s; valid_irq_node' (irq_node' s) s; valid_irq_handlers' s; valid_irq_states' s; valid_machine_state' s; irqs_masked' s; valid_queues' s; ct_not_inQ s; ct_idle_or_in_cur_domain' s; valid_pde_mappings' s; pspace_domain_valid s; ksCurDomain s \<le> maxDomain; ksDomSchedule (newKernelState undefined) \<noteq> []; \<forall>x\<in>set (ksDomSchedule (newKernelState undefined)). dschDomain x \<le> maxDomain \<and> 0 < dschLength x; ksDomSchedule s = ksDomSchedule (newKernelState undefined); ksDomScheduleIdx s < length (ksDomSchedule (newKernelState undefined)); untyped_ranges_zero' s; cur_tcb' s\<rbrakk> \<Longrightarrow> sym_refs (\<lambda>a. if a = t then tcb_st_refs_of' st \<union> {r \<in> state_refs_of' s t. snd r = TCBBound} else state_refs_of' s a)
 3. \<And>s. \<lbrakk>st_tcb_at' (\<lambda>st'. tcb_st_refs_of' st' = tcb_st_refs_of' st \<and> (st \<noteq> Structures_H.thread_state.Inactive \<and> st \<noteq> Structures_H.thread_state.IdleThreadState \<longrightarrow> st' \<noteq> Structures_H.thread_state.Inactive \<and> st' \<noteq> Structures_H.thread_state.IdleThreadState)) t s; t = ksIdleThread s \<longrightarrow> idle' st; runnable' st \<and> obj_at' tcbQueued t s \<longrightarrow> st_tcb_at' runnable' t s; sch_act_simple s; valid_pspace' s; sch_act_wf (ksSchedulerAction s) s; valid_queues_no_bitmap s; valid_bitmapQ s; bitmapQ_no_L2_orphans s; bitmapQ_no_L1_orphans s; sym_refs (state_refs_of' s); if_live_then_nonz_cap' s; if_unsafe_then_cap' s; valid_idle' s; valid_global_refs' s; valid_arch_state' s; valid_irq_node' (irq_node' s) s; valid_irq_handlers' s; valid_irq_states' s; valid_machine_state' s; irqs_masked' s; valid_queues' s; ct_not_inQ s; ct_idle_or_in_cur_domain' s; valid_pde_mappings' s; pspace_domain_valid s; ksCurDomain s \<le> maxDomain; ksDomSchedule (newKernelState undefined) \<noteq> []; \<forall>x\<in>set (ksDomSchedule (newKernelState undefined)). dschDomain x \<le> maxDomain \<and> 0 < dschLength x; ksDomSchedule s = ksDomSchedule (newKernelState undefined); ksDomScheduleIdx s < length (ksDomSchedule (newKernelState undefined)); untyped_ranges_zero' s; cur_tcb' s\<rbrakk> \<Longrightarrow> st \<noteq> Structures_H.thread_state.Inactive \<and> st \<noteq> Structures_H.thread_state.IdleThreadState \<longrightarrow> ex_nonz_cap_to' t s
 4. \<And>s. \<lbrakk>st_tcb_at' (\<lambda>st'. tcb_st_refs_of' st' = tcb_st_refs_of' st \<and> (st \<noteq> Structures_H.thread_state.Inactive \<and> st \<noteq> Structures_H.thread_state.IdleThreadState \<longrightarrow> st' \<noteq> Structures_H.thread_state.Inactive \<and> st' \<noteq> Structures_H.thread_state.IdleThreadState)) t s; t = ksIdleThread s \<longrightarrow> idle' st; runnable' st \<and> obj_at' tcbQueued t s \<longrightarrow> st_tcb_at' runnable' t s; sch_act_simple s; valid_pspace' s; sch_act_wf (ksSchedulerAction s) s; valid_queues_no_bitmap s; valid_bitmapQ s; bitmapQ_no_L2_orphans s; bitmapQ_no_L1_orphans s; sym_refs (state_refs_of' s); if_live_then_nonz_cap' s; if_unsafe_then_cap' s; valid_idle' s; valid_global_refs' s; valid_arch_state' s; valid_irq_node' (irq_node' s) s; valid_irq_handlers' s; valid_irq_states' s; valid_machine_state' s; irqs_masked' s; valid_queues' s; ct_not_inQ s; ct_idle_or_in_cur_domain' s; valid_pde_mappings' s; pspace_domain_valid s; ksCurDomain s \<le> maxDomain; ksDomSchedule (newKernelState undefined) \<noteq> []; \<forall>x\<in>set (ksDomSchedule (newKernelState undefined)). dschDomain x \<le> maxDomain \<and> 0 < dschLength x; ksDomSchedule s = ksDomSchedule (newKernelState undefined); ksDomScheduleIdx s < length (ksDomSchedule (newKernelState undefined)); untyped_ranges_zero' s; cur_tcb' s\<rbrakk> \<Longrightarrow> tcb_at' t s proof (prove)
goal (4 subgoals):
 1. \<And>s k. \<lbrakk>t = ksIdleThread s \<longrightarrow> idle' st; runnable' st \<and> obj_at' tcbQueued t s \<longrightarrow> obj_at' (runnable' \<circ> tcbState) t s; sch_act_simple s; valid_pspace' s; sch_act_wf (ksSchedulerAction s) s; valid_queues_no_bitmap s; valid_bitmapQ s; bitmapQ_no_L2_orphans s; bitmapQ_no_L1_orphans s; sym_refs (state_refs_of' s); if_live_then_nonz_cap' s; if_unsafe_then_cap' s; valid_idle' s; valid_global_refs' s; valid_arch_state' s; valid_irq_node' (irq_node' s) s; valid_irq_handlers' s; valid_irq_states' s; valid_machine_state' s; irqs_masked' s; valid_queues' s; ct_not_inQ s; ct_idle_or_in_cur_domain' s; valid_pde_mappings' s; pspace_domain_valid s; ksCurDomain s \<le> maxDomain; ksDomSchedule (newKernelState undefined) \<noteq> []; \<forall>x\<in>set (ksDomSchedule (newKernelState undefined)). dschDomain x \<le> maxDomain \<and> 0 < dschLength x; ksDomSchedule s = ksDomSchedule (newKernelState undefined); ksDomScheduleIdx s < length (ksDomSchedule (newKernelState undefined)); untyped_ranges_zero' s; cur_tcb' s; tcb_st_refs_of' (tcbState k) = tcb_st_refs_of' st; st \<noteq> Structures_H.thread_state.Inactive \<and> st \<noteq> Structures_H.thread_state.IdleThreadState \<longrightarrow> tcbState k \<noteq> Structures_H.thread_state.Inactive \<and> tcbState k \<noteq> Structures_H.thread_state.IdleThreadState; \<forall>x\<in>ran tcb_cte_cases. case x of (getF, setF) \<Rightarrow> valid_cap' (cteCap (getF k)) s; valid_tcb_state' (tcbState k) s; is_aligned (tcbIPCBuffer k) msg_align_bits; valid_bound_ntfn' (tcbBoundNotification k) s; tcbDomain k \<le> maxDomain; tcbPriority k \<le> maxPriority; tcbMCP k \<le> maxPriority\<rbrakk> \<Longrightarrow> valid_tcb_state' st s
 2. \<And>s. \<lbrakk>st_tcb_at' (\<lambda>st'. tcb_st_refs_of' st' = tcb_st_refs_of' st \<and> (st \<noteq> Structures_H.thread_state.Inactive \<and> st \<noteq> Structures_H.thread_state.IdleThreadState \<longrightarrow> st' \<noteq> Structures_H.thread_state.Inactive \<and> st' \<noteq> Structures_H.thread_state.IdleThreadState)) t s; t = ksIdleThread s \<longrightarrow> idle' st; runnable' st \<and> obj_at' tcbQueued t s \<longrightarrow> st_tcb_at' runnable' t s; sch_act_simple s; valid_pspace' s; sch_act_wf (ksSchedulerAction s) s; valid_queues_no_bitmap s; valid_bitmapQ s; bitmapQ_no_L2_orphans s; bitmapQ_no_L1_orphans s; sym_refs (state_refs_of' s); if_live_then_nonz_cap' s; if_unsafe_then_cap' s; valid_idle' s; valid_global_refs' s; valid_arch_state' s; valid_irq_node' (irq_node' s) s; valid_irq_handlers' s; valid_irq_states' s; valid_machine_state' s; irqs_masked' s; valid_queues' s; ct_not_inQ s; ct_idle_or_in_cur_domain' s; valid_pde_mappings' s; pspace_domain_valid s; ksCurDomain s \<le> maxDomain; ksDomSchedule (newKernelState undefined) \<noteq> []; \<forall>x\<in>set (ksDomSchedule (newKernelState undefined)). dschDomain x \<le> maxDomain \<and> 0 < dschLength x; ksDomSchedule s = ksDomSchedule (newKernelState undefined); ksDomScheduleIdx s < length (ksDomSchedule (newKernelState undefined)); untyped_ranges_zero' s; cur_tcb' s\<rbrakk> \<Longrightarrow> sym_refs (\<lambda>a. if a = t then tcb_st_refs_of' st \<union> {r \<in> state_refs_of' s t. snd r = TCBBound} else state_refs_of' s a)
 3. \<And>s. \<lbrakk>st_tcb_at' (\<lambda>st'. tcb_st_refs_of' st' = tcb_st_refs_of' st \<and> (st \<noteq> Structures_H.thread_state.Inactive \<and> st \<noteq> Structures_H.thread_state.IdleThreadState \<longrightarrow> st' \<noteq> Structures_H.thread_state.Inactive \<and> st' \<noteq> Structures_H.thread_state.IdleThreadState)) t s; t = ksIdleThread s \<longrightarrow> idle' st; runnable' st \<and> obj_at' tcbQueued t s \<longrightarrow> st_tcb_at' runnable' t s; sch_act_simple s; valid_pspace' s; sch_act_wf (ksSchedulerAction s) s; valid_queues_no_bitmap s; valid_bitmapQ s; bitmapQ_no_L2_orphans s; bitmapQ_no_L1_orphans s; sym_refs (state_refs_of' s); if_live_then_nonz_cap' s; if_unsafe_then_cap' s; valid_idle' s; valid_global_refs' s; valid_arch_state' s; valid_irq_node' (irq_node' s) s; valid_irq_handlers' s; valid_irq_states' s; valid_machine_state' s; irqs_masked' s; valid_queues' s; ct_not_inQ s; ct_idle_or_in_cur_domain' s; valid_pde_mappings' s; pspace_domain_valid s; ksCurDomain s \<le> maxDomain; ksDomSchedule (newKernelState undefined) \<noteq> []; \<forall>x\<in>set (ksDomSchedule (newKernelState undefined)). dschDomain x \<le> maxDomain \<and> 0 < dschLength x; ksDomSchedule s = ksDomSchedule (newKernelState undefined); ksDomScheduleIdx s < length (ksDomSchedule (newKernelState undefined)); untyped_ranges_zero' s; cur_tcb' s\<rbrakk> \<Longrightarrow> st \<noteq> Structures_H.thread_state.Inactive \<and> st \<noteq> Structures_H.thread_state.IdleThreadState \<longrightarrow> ex_nonz_cap_to' t s
 4. \<And>s. \<lbrakk>st_tcb_at' (\<lambda>st'. tcb_st_refs_of' st' = tcb_st_refs_of' st \<and> (st \<noteq> Structures_H.thread_state.Inactive \<and> st \<noteq> Structures_H.thread_state.IdleThreadState \<longrightarrow> st' \<noteq> Structures_H.thread_state.Inactive \<and> st' \<noteq> Structures_H.thread_state.IdleThreadState)) t s; t = ksIdleThread s \<longrightarrow> idle' st; runnable' st \<and> obj_at' tcbQueued t s \<longrightarrow> st_tcb_at' runnable' t s; sch_act_simple s; valid_pspace' s; sch_act_wf (ksSchedulerAction s) s; valid_queues_no_bitmap s; valid_bitmapQ s; bitmapQ_no_L2_orphans s; bitmapQ_no_L1_orphans s; sym_refs (state_refs_of' s); if_live_then_nonz_cap' s; if_unsafe_then_cap' s; valid_idle' s; valid_global_refs' s; valid_arch_state' s; valid_irq_node' (irq_node' s) s; valid_irq_handlers' s; valid_irq_states' s; valid_machine_state' s; irqs_masked' s; valid_queues' s; ct_not_inQ s; ct_idle_or_in_cur_domain' s; valid_pde_mappings' s; pspace_domain_valid s; ksCurDomain s \<le> maxDomain; ksDomSchedule (newKernelState undefined) \<noteq> []; \<forall>x\<in>set (ksDomSchedule (newKernelState undefined)). dschDomain x \<le> maxDomain \<and> 0 < dschLength x; ksDomSchedule s = ksDomSchedule (newKernelState undefined); ksDomScheduleIdx s < length (ksDomSchedule (newKernelState undefined)); untyped_ranges_zero' s; cur_tcb' s\<rbrakk> \<Longrightarrow> tcb_at' t s proof (prove)
goal (1 subgoal):
 1. \<lbrakk>t = ksIdleThread s_ \<longrightarrow> idle' st; runnable' st \<and> obj_at' tcbQueued t s_ \<longrightarrow> obj_at' (runnable' \<circ> tcbState) t s_; sch_act_simple s_; valid_pspace' s_; sch_act_wf (ksSchedulerAction s_) s_; valid_queues_no_bitmap s_; valid_bitmapQ s_; bitmapQ_no_L2_orphans s_; bitmapQ_no_L1_orphans s_; sym_refs (state_refs_of' s_); if_live_then_nonz_cap' s_; if_unsafe_then_cap' s_; valid_idle' s_; valid_global_refs' s_; valid_arch_state' s_; valid_irq_node' (irq_node' s_) s_; valid_irq_handlers' s_; valid_irq_states' s_; valid_machine_state' s_; irqs_masked' s_; valid_queues' s_; ct_not_inQ s_; ct_idle_or_in_cur_domain' s_; valid_pde_mappings' s_; pspace_domain_valid s_; ksCurDomain s_ \<le> maxDomain; ksDomSchedule (newKernelState undefined) \<noteq> []; \<forall>x\<in>set (ksDomSchedule (newKernelState undefined)). dschDomain x \<le> maxDomain \<and> 0 < dschLength x; ksDomSchedule s_ = ksDomSchedule (newKernelState undefined); ksDomScheduleIdx s_ < length (ksDomSchedule (newKernelState undefined)); untyped_ranges_zero' s_; cur_tcb' s_; tcb_st_refs_of' (tcbState k_) = tcb_st_refs_of' st; st \<noteq> Structures_H.thread_state.Inactive \<and> st \<noteq> Structures_H.thread_state.IdleThreadState \<longrightarrow> tcbState k_ \<noteq> Structures_H.thread_state.Inactive \<and> tcbState k_ \<noteq> Structures_H.thread_state.IdleThreadState; \<forall>x\<in>ran tcb_cte_cases. case x of (getF, setF) \<Rightarrow> valid_cap' (cteCap (getF k_)) s_; valid_tcb_state' (tcbState k_) s_; is_aligned (tcbIPCBuffer k_) msg_align_bits; valid_bound_ntfn' (tcbBoundNotification k_) s_; tcbDomain k_ \<le> maxDomain; tcbPriority k_ \<le> maxPriority; tcbMCP k_ \<le> maxPriority\<rbrakk> \<Longrightarrow> valid_tcb_state' st s_ proof (prove)
goal (3 subgoals):
 1. \<And>s. \<lbrakk>st_tcb_at' (\<lambda>st'. tcb_st_refs_of' st' = tcb_st_refs_of' st \<and> (st \<noteq> Structures_H.thread_state.Inactive \<and> st \<noteq> Structures_H.thread_state.IdleThreadState \<longrightarrow> st' \<noteq> Structures_H.thread_state.Inactive \<and> st' \<noteq> Structures_H.thread_state.IdleThreadState)) t s; t = ksIdleThread s \<longrightarrow> idle' st; runnable' st \<and> obj_at' tcbQueued t s \<longrightarrow> st_tcb_at' runnable' t s; sch_act_simple s; valid_pspace' s; sch_act_wf (ksSchedulerAction s) s; valid_queues_no_bitmap s; valid_bitmapQ s; bitmapQ_no_L2_orphans s; bitmapQ_no_L1_orphans s; sym_refs (state_refs_of' s); if_live_then_nonz_cap' s; if_unsafe_then_cap' s; valid_idle' s; valid_global_refs' s; valid_arch_state' s; valid_irq_node' (irq_node' s) s; valid_irq_handlers' s; valid_irq_states' s; valid_machine_state' s; irqs_masked' s; valid_queues' s; ct_not_inQ s; ct_idle_or_in_cur_domain' s; valid_pde_mappings' s; pspace_domain_valid s; ksCurDomain s \<le> maxDomain; ksDomSchedule (newKernelState undefined) \<noteq> []; \<forall>x\<in>set (ksDomSchedule (newKernelState undefined)). dschDomain x \<le> maxDomain \<and> 0 < dschLength x; ksDomSchedule s = ksDomSchedule (newKernelState undefined); ksDomScheduleIdx s < length (ksDomSchedule (newKernelState undefined)); untyped_ranges_zero' s; cur_tcb' s\<rbrakk> \<Longrightarrow> sym_refs (\<lambda>a. if a = t then tcb_st_refs_of' st \<union> {r \<in> state_refs_of' s t. snd r = TCBBound} else state_refs_of' s a)
 2. \<And>s. \<lbrakk>st_tcb_at' (\<lambda>st'. tcb_st_refs_of' st' = tcb_st_refs_of' st \<and> (st \<noteq> Structures_H.thread_state.Inactive \<and> st \<noteq> Structures_H.thread_state.IdleThreadState \<longrightarrow> st' \<noteq> Structures_H.thread_state.Inactive \<and> st' \<noteq> Structures_H.thread_state.IdleThreadState)) t s; t = ksIdleThread s \<longrightarrow> idle' st; runnable' st \<and> obj_at' tcbQueued t s \<longrightarrow> st_tcb_at' runnable' t s; sch_act_simple s; valid_pspace' s; sch_act_wf (ksSchedulerAction s) s; valid_queues_no_bitmap s; valid_bitmapQ s; bitmapQ_no_L2_orphans s; bitmapQ_no_L1_orphans s; sym_refs (state_refs_of' s); if_live_then_nonz_cap' s; if_unsafe_then_cap' s; valid_idle' s; valid_global_refs' s; valid_arch_state' s; valid_irq_node' (irq_node' s) s; valid_irq_handlers' s; valid_irq_states' s; valid_machine_state' s; irqs_masked' s; valid_queues' s; ct_not_inQ s; ct_idle_or_in_cur_domain' s; valid_pde_mappings' s; pspace_domain_valid s; ksCurDomain s \<le> maxDomain; ksDomSchedule (newKernelState undefined) \<noteq> []; \<forall>x\<in>set (ksDomSchedule (newKernelState undefined)). dschDomain x \<le> maxDomain \<and> 0 < dschLength x; ksDomSchedule s = ksDomSchedule (newKernelState undefined); ksDomScheduleIdx s < length (ksDomSchedule (newKernelState undefined)); untyped_ranges_zero' s; cur_tcb' s\<rbrakk> \<Longrightarrow> st \<noteq> Structures_H.thread_state.Inactive \<and> st \<noteq> Structures_H.thread_state.IdleThreadState \<longrightarrow> ex_nonz_cap_to' t s
 3. \<And>s. \<lbrakk>st_tcb_at' (\<lambda>st'. tcb_st_refs_of' st' = tcb_st_refs_of' st \<and> (st \<noteq> Structures_H.thread_state.Inactive \<and> st \<noteq> Structures_H.thread_state.IdleThreadState \<longrightarrow> st' \<noteq> Structures_H.thread_state.Inactive \<and> st' \<noteq> Structures_H.thread_state.IdleThreadState)) t s; t = ksIdleThread s \<longrightarrow> idle' st; runnable' st \<and> obj_at' tcbQueued t s \<longrightarrow> st_tcb_at' runnable' t s; sch_act_simple s; valid_pspace' s; sch_act_wf (ksSchedulerAction s) s; valid_queues_no_bitmap s; valid_bitmapQ s; bitmapQ_no_L2_orphans s; bitmapQ_no_L1_orphans s; sym_refs (state_refs_of' s); if_live_then_nonz_cap' s; if_unsafe_then_cap' s; valid_idle' s; valid_global_refs' s; valid_arch_state' s; valid_irq_node' (irq_node' s) s; valid_irq_handlers' s; valid_irq_states' s; valid_machine_state' s; irqs_masked' s; valid_queues' s; ct_not_inQ s; ct_idle_or_in_cur_domain' s; valid_pde_mappings' s; pspace_domain_valid s; ksCurDomain s \<le> maxDomain; ksDomSchedule (newKernelState undefined) \<noteq> []; \<forall>x\<in>set (ksDomSchedule (newKernelState undefined)). dschDomain x \<le> maxDomain \<and> 0 < dschLength x; ksDomSchedule s = ksDomSchedule (newKernelState undefined); ksDomScheduleIdx s < length (ksDomSchedule (newKernelState undefined)); untyped_ranges_zero' s; cur_tcb' s\<rbrakk> \<Longrightarrow> tcb_at' t s proof (prove)
goal (2 subgoals):
 1. \<And>s. \<lbrakk>st_tcb_at' (\<lambda>st'. tcb_st_refs_of' st' = tcb_st_refs_of' st \<and> (st \<noteq> Structures_H.thread_state.Inactive \<and> st \<noteq> Structures_H.thread_state.IdleThreadState \<longrightarrow> st' \<noteq> Structures_H.thread_state.Inactive \<and> st' \<noteq> Structures_H.thread_state.IdleThreadState)) t s; t = ksIdleThread s \<longrightarrow> idle' st; runnable' st \<and> obj_at' tcbQueued t s \<longrightarrow> st_tcb_at' runnable' t s; sch_act_simple s; valid_pspace' s; sch_act_wf (ksSchedulerAction s) s; valid_queues_no_bitmap s; valid_bitmapQ s; bitmapQ_no_L2_orphans s; bitmapQ_no_L1_orphans s; sym_refs (state_refs_of' s); if_live_then_nonz_cap' s; if_unsafe_then_cap' s; valid_idle' s; valid_global_refs' s; valid_arch_state' s; valid_irq_node' (irq_node' s) s; valid_irq_handlers' s; valid_irq_states' s; valid_machine_state' s; irqs_masked' s; valid_queues' s; ct_not_inQ s; ct_idle_or_in_cur_domain' s; valid_pde_mappings' s; pspace_domain_valid s; ksCurDomain s \<le> maxDomain; ksDomSchedule (newKernelState undefined) \<noteq> []; \<forall>x\<in>set (ksDomSchedule (newKernelState undefined)). dschDomain x \<le> maxDomain \<and> 0 < dschLength x; ksDomSchedule s = ksDomSchedule (newKernelState undefined); ksDomScheduleIdx s < length (ksDomSchedule (newKernelState undefined)); untyped_ranges_zero' s; cur_tcb' s\<rbrakk> \<Longrightarrow> st \<noteq> Structures_H.thread_state.Inactive \<and> st \<noteq> Structures_H.thread_state.IdleThreadState \<longrightarrow> ex_nonz_cap_to' t s
 2. \<And>s. \<lbrakk>st_tcb_at' (\<lambda>st'. tcb_st_refs_of' st' = tcb_st_refs_of' st \<and> (st \<noteq> Structures_H.thread_state.Inactive \<and> st \<noteq> Structures_H.thread_state.IdleThreadState \<longrightarrow> st' \<noteq> Structures_H.thread_state.Inactive \<and> st' \<noteq> Structures_H.thread_state.IdleThreadState)) t s; t = ksIdleThread s \<longrightarrow> idle' st; runnable' st \<and> obj_at' tcbQueued t s \<longrightarrow> st_tcb_at' runnable' t s; sch_act_simple s; valid_pspace' s; sch_act_wf (ksSchedulerAction s) s; valid_queues_no_bitmap s; valid_bitmapQ s; bitmapQ_no_L2_orphans s; bitmapQ_no_L1_orphans s; sym_refs (state_refs_of' s); if_live_then_nonz_cap' s; if_unsafe_then_cap' s; valid_idle' s; valid_global_refs' s; valid_arch_state' s; valid_irq_node' (irq_node' s) s; valid_irq_handlers' s; valid_irq_states' s; valid_machine_state' s; irqs_masked' s; valid_queues' s; ct_not_inQ s; ct_idle_or_in_cur_domain' s; valid_pde_mappings' s; pspace_domain_valid s; ksCurDomain s \<le> maxDomain; ksDomSchedule (newKernelState undefined) \<noteq> []; \<forall>x\<in>set (ksDomSchedule (newKernelState undefined)). dschDomain x \<le> maxDomain \<and> 0 < dschLength x; ksDomSchedule s = ksDomSchedule (newKernelState undefined); ksDomScheduleIdx s < length (ksDomSchedule (newKernelState undefined)); untyped_ranges_zero' s; cur_tcb' s\<rbrakk> \<Longrightarrow> tcb_at' t s proof (prove)
goal:
No subgoals!