theory DetSchedAux_AI

lemma valid_sched_tcb_state_preservation:
  assumes st_tcb: "\<And>P t. \<lbrace>I and ct_active and st_tcb_at (P and Not o inactive and Not o idle) t\<rbrace> f \<lbrace>\<lambda>_.st_tcb_at P t\<rbrace>"
  assumes stuff: "\<And>P t. \<lbrace>(\<lambda>s. etcb_at P t s) and valid_etcbs\<rbrace> f \<lbrace>\<lambda>r s. st_tcb_at (Not o inactive) t s \<longrightarrow> etcb_at P t s\<rbrace>"
  assumes cur_thread: "\<And>P. \<lbrace>\<lambda>s. P (cur_thread s)\<rbrace> f \<lbrace>\<lambda>r s. P (cur_thread s)\<rbrace>"
  assumes idle_thread: "\<And>P. \<lbrace>\<lambda>s. P (idle_thread s)\<rbrace> f \<lbrace>\<lambda>r s. P (idle_thread s)\<rbrace>"
  assumes valid_etcb: "\<lbrace>valid_etcbs\<rbrace> f \<lbrace>\<lambda>_. valid_etcbs\<rbrace>"
  assumes valid_blocked: "\<lbrace>valid_blocked\<rbrace> f \<lbrace>\<lambda>_. valid_blocked\<rbrace>"
  assumes valid_idle: "\<lbrace>I\<rbrace> f \<lbrace>\<lambda>_. valid_idle\<rbrace>"
  assumes valid_others: "\<And>P. \<lbrace>\<lambda>s. P (scheduler_action s) (ready_queues s) (cur_domain s)\<rbrace> f \<lbrace>\<lambda>r s. P (scheduler_action s) (ready_queues s) (cur_domain s)\<rbrace>"
  shows "\<lbrace>I and ct_active and valid_sched and valid_idle\<rbrace> f \<lbrace>\<lambda>_. valid_sched\<rbrace>" apply (clarsimp simp add: valid_sched_def valid_def) apply (frule(1) use_valid[OF _ valid_etcb]) apply (frule(1) use_valid[OF _ valid_blocked]) apply simp apply (frule_tac P1="\<lambda>sa rq cdom. rq = ready_queues s \<and> sa = scheduler_action s \<and> cdom = cur_domain s" in use_valid[OF _ valid_others]) apply simp apply (rule conjI) apply (clarsimp simp add: valid_queues_def) apply (drule_tac x=d in spec) apply (drule_tac x=p in spec) apply clarsimp apply (drule_tac x=t in bspec) apply simp apply clarsimp apply (subgoal_tac "st_tcb_at runnable t b") apply simp apply (rule conjI) apply (fastforce simp: valid_etcbs_def pred_tcb_at_def obj_at_def) apply (frule_tac P1="(\<lambda>t. tcb_priority t = p \<and> tcb_domain t = d)" and t1=t in use_valid[OF _ stuff]) apply simp apply (simp add: pred_tcb_at_def obj_at_def) apply force apply (rule_tac use_valid[OF _ st_tcb],assumption) apply simp apply (erule pred_tcb_weakenE) apply simp apply (case_tac "itcb_state tcb") apply simp+ apply (frule_tac P1="\<lambda>ct. ct = (cur_thread s)" in use_valid[OF _ cur_thread]) apply simp apply (rule conjI) apply simp apply simp apply (clarsimp simp add: valid_sched_action_def is_activatable_def weak_valid_sched_action_def) apply (rule conjI) apply clarsimp apply (frule_tac P1="active" and t1="cur_thread s" in use_valid[OF _ st_tcb]) apply (simp add: ct_in_state_def) apply (erule pred_tcb_weakenE) apply simp apply (case_tac "itcb_state tcb"; simp) apply (erule pred_tcb_weakenE) apply (case_tac "itcb_state tcb"; simp) apply (rule conjI) apply clarsimp apply (rule_tac use_valid[OF _ st_tcb],assumption) apply simp apply (erule pred_tcb_weakenE) apply simp apply (case_tac "itcb_state tcb", simp+) apply (rule conjI) apply (clarsimp simp: switch_in_cur_domain_def in_cur_domain_def) apply (rule use_valid[OF _ stuff, rule_format], assumption) apply simp apply (rule use_valid[OF _ st_tcb], assumption) apply simp apply (erule st_tcb_weakenE) apply (case_tac st, simp+) apply (clarsimp simp: ct_in_cur_domain_2_def in_cur_domain_2_def) apply (frule_tac P1="\<lambda>idle. idle = (idle_thread s)" in use_valid[OF _ idle_thread], simp) apply (rule conjI) apply (rule impI) apply (simp, erule disjE, simp) apply (frule_tac P1="(\<lambda>t. tcb_domain t = cur_domain s)" and t1="cur_thread s" in use_valid[OF _ stuff]) apply (clarsimp simp: etcb_at_def split: option.splits) apply clarsimp apply (erule notE, rule use_valid[OF _ st_tcb],assumption) apply (simp add: ct_in_state_def) apply (erule st_tcb_weakenE) apply simp apply (case_tac st, simp+) apply(frule (1) use_valid[OF _ valid_idle]) apply(simp add: valid_idle_etcb_def) apply(frule use_valid[OF _ stuff[where t=idle_thread_ptr]]) apply simp apply(erule mp) apply(fastforce simp: valid_idle_def pred_tcb_at_def obj_at_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>I and ct_active and valid_sched and valid_idle\<rbrace> f \<lbrace>\<lambda>_. valid_sched\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s a b. \<lbrakk>(a, b) \<in> fst (f s); I s; ct_active s; valid_etcbs s; valid_queues s; ct_not_in_q s; valid_sched_action s; ct_in_cur_domain s; valid_blocked s; valid_idle_etcb s; valid_idle s\<rbrakk> \<Longrightarrow> valid_etcbs b \<and> valid_queues b \<and> ct_not_in_q b \<and> valid_sched_action b \<and> ct_in_cur_domain b \<and> valid_blocked b \<and> valid_idle_etcb b proof (prove)
goal (1 subgoal):
 1. \<And>s a b. \<lbrakk>(a, b) \<in> fst (f s); I s; ct_active s; valid_etcbs s; valid_queues s; ct_not_in_q s; valid_sched_action s; ct_in_cur_domain s; valid_blocked s; valid_idle_etcb s; valid_idle s; valid_etcbs b\<rbrakk> \<Longrightarrow> valid_etcbs b \<and> valid_queues b \<and> ct_not_in_q b \<and> valid_sched_action b \<and> ct_in_cur_domain b \<and> valid_blocked b \<and> valid_idle_etcb b proof (prove)
goal (1 subgoal):
 1. \<And>s a b. \<lbrakk>(a, b) \<in> fst (f s); I s; ct_active s; valid_etcbs s; valid_queues s; ct_not_in_q s; valid_sched_action s; ct_in_cur_domain s; valid_blocked s; valid_idle_etcb s; valid_idle s; valid_etcbs b; valid_blocked b\<rbrakk> \<Longrightarrow> valid_etcbs b \<and> valid_queues b \<and> ct_not_in_q b \<and> valid_sched_action b \<and> ct_in_cur_domain b \<and> valid_blocked b \<and> valid_idle_etcb b proof (prove)
goal (1 subgoal):
 1. \<And>s a b. \<lbrakk>(a, b) \<in> fst (f s); I s; ct_active s; valid_etcbs s; valid_queues s; ct_not_in_q s; valid_sched_action s; ct_in_cur_domain s; valid_blocked s; valid_idle_etcb s; valid_idle s; valid_etcbs b; valid_blocked b\<rbrakk> \<Longrightarrow> valid_queues b \<and> ct_not_in_q b \<and> valid_sched_action b \<and> ct_in_cur_domain b \<and> valid_idle_etcb b proof (prove)
goal (2 subgoals):
 1. \<And>s a b. \<lbrakk>(a, b) \<in> fst (f s); I s; ct_active s; valid_etcbs s; valid_queues s; ct_not_in_q s; valid_sched_action s; ct_in_cur_domain s; valid_blocked s; valid_idle_etcb s; valid_idle s; valid_etcbs b; valid_blocked b\<rbrakk> \<Longrightarrow> ready_queues s = ready_queues s \<and> scheduler_action s = scheduler_action s \<and> cur_domain s = cur_domain s
 2. \<And>s a b. \<lbrakk>(a, b) \<in> fst (f s); I s; ct_active s; valid_etcbs s; valid_queues s; ct_not_in_q s; valid_sched_action s; ct_in_cur_domain s; valid_blocked s; valid_idle_etcb s; valid_idle s; valid_etcbs b; valid_blocked b; ready_queues b = ready_queues s \<and> scheduler_action b = scheduler_action s \<and> cur_domain b = cur_domain s\<rbrakk> \<Longrightarrow> valid_queues b \<and> ct_not_in_q b \<and> valid_sched_action b \<and> ct_in_cur_domain b \<and> valid_idle_etcb b proof (prove)
goal (1 subgoal):
 1. \<And>s a b. \<lbrakk>(a, b) \<in> fst (f s); I s; ct_active s; valid_etcbs s; valid_queues s; ct_not_in_q s; valid_sched_action s; ct_in_cur_domain s; valid_blocked s; valid_idle_etcb s; valid_idle s; valid_etcbs b; valid_blocked b; ready_queues b = ready_queues s \<and> scheduler_action b = scheduler_action s \<and> cur_domain b = cur_domain s\<rbrakk> \<Longrightarrow> valid_queues b \<and> ct_not_in_q b \<and> valid_sched_action b \<and> ct_in_cur_domain b \<and> valid_idle_etcb b proof (prove)
goal (2 subgoals):
 1. \<And>s a b. \<lbrakk>(a, b) \<in> fst (f s); I s; ct_active s; valid_etcbs s; valid_queues s; ct_not_in_q s; valid_sched_action s; ct_in_cur_domain s; valid_blocked s; valid_idle_etcb s; valid_idle s; valid_etcbs b; valid_blocked b; ready_queues b = ready_queues s \<and> scheduler_action b = scheduler_action s \<and> cur_domain b = cur_domain s\<rbrakk> \<Longrightarrow> valid_queues b
 2. \<And>s a b. \<lbrakk>(a, b) \<in> fst (f s); I s; ct_active s; valid_etcbs s; valid_queues s; ct_not_in_q s; valid_sched_action s; ct_in_cur_domain s; valid_blocked s; valid_idle_etcb s; valid_idle s; valid_etcbs b; valid_blocked b; ready_queues b = ready_queues s \<and> scheduler_action b = scheduler_action s \<and> cur_domain b = cur_domain s\<rbrakk> \<Longrightarrow> ct_not_in_q b \<and> valid_sched_action b \<and> ct_in_cur_domain b \<and> valid_idle_etcb b proof (prove)
goal (2 subgoals):
 1. \<And>s a b d p t. \<lbrakk>(a, b) \<in> fst (f s); I s; ct_active s; valid_etcbs s; \<forall>d p. (\<forall>t\<in>set (ready_queues s d p). is_etcb_at t s \<and> etcb_at (\<lambda>t. tcb_priority t = p \<and> tcb_domain t = d) t s \<and> st_tcb_at runnable t s) \<and> distinct (ready_queues s d p); ct_not_in_q s; valid_sched_action s; ct_in_cur_domain s; valid_blocked s; valid_idle_etcb s; valid_idle s; valid_etcbs b; valid_blocked_2 (ready_queues s) (kheap b) (scheduler_action s) (cur_thread b); t \<in> set (ready_queues s d p); ready_queues b = ready_queues s; scheduler_action b = scheduler_action s; cur_domain b = cur_domain s\<rbrakk> \<Longrightarrow> is_etcb_at t b \<and> etcb_at (\<lambda>t. tcb_priority t = p \<and> tcb_domain t = d) t b \<and> st_tcb_at runnable t b
 2. \<And>s a b. \<lbrakk>(a, b) \<in> fst (f s); I s; ct_active s; valid_etcbs s; valid_queues s; ct_not_in_q s; valid_sched_action s; ct_in_cur_domain s; valid_blocked s; valid_idle_etcb s; valid_idle s; valid_etcbs b; valid_blocked b; ready_queues b = ready_queues s \<and> scheduler_action b = scheduler_action s \<and> cur_domain b = cur_domain s\<rbrakk> \<Longrightarrow> ct_not_in_q b \<and> valid_sched_action b \<and> ct_in_cur_domain b \<and> valid_idle_etcb b proof (prove)
goal (2 subgoals):
 1. \<And>s a b d p t. \<lbrakk>(a, b) \<in> fst (f s); I s; ct_active s; valid_etcbs s; ct_not_in_q s; valid_sched_action s; ct_in_cur_domain s; valid_blocked s; valid_idle_etcb s; valid_idle s; valid_etcbs b; valid_blocked_2 (ready_queues s) (kheap b) (scheduler_action s) (cur_thread b); t \<in> set (ready_queues s d p); ready_queues b = ready_queues s; scheduler_action b = scheduler_action s; cur_domain b = cur_domain s; \<forall>p. (\<forall>t\<in>set (ready_queues s d p). is_etcb_at t s \<and> etcb_at (\<lambda>t. tcb_priority t = p \<and> tcb_domain t = d) t s \<and> st_tcb_at runnable t s) \<and> distinct (ready_queues s d p)\<rbrakk> \<Longrightarrow> is_etcb_at t b \<and> etcb_at (\<lambda>t. tcb_priority t = p \<and> tcb_domain t = d) t b \<and> st_tcb_at runnable t b
 2. \<And>s a b. \<lbrakk>(a, b) \<in> fst (f s); I s; ct_active s; valid_etcbs s; valid_queues s; ct_not_in_q s; valid_sched_action s; ct_in_cur_domain s; valid_blocked s; valid_idle_etcb s; valid_idle s; valid_etcbs b; valid_blocked b; ready_queues b = ready_queues s \<and> scheduler_action b = scheduler_action s \<and> cur_domain b = cur_domain s\<rbrakk> \<Longrightarrow> ct_not_in_q b \<and> valid_sched_action b \<and> ct_in_cur_domain b \<and> valid_idle_etcb b proof (prove)
goal (2 subgoals):
 1. \<And>s a b d p t. \<lbrakk>(a, b) \<in> fst (f s); I s; ct_active s; valid_etcbs s; ct_not_in_q s; valid_sched_action s; ct_in_cur_domain s; valid_blocked s; valid_idle_etcb s; valid_idle s; valid_etcbs b; valid_blocked_2 (ready_queues s) (kheap b) (scheduler_action s) (cur_thread b); t \<in> set (ready_queues s d p); ready_queues b = ready_queues s; scheduler_action b = scheduler_action s; cur_domain b = cur_domain s; (\<forall>t\<in>set (ready_queues s d p). is_etcb_at t s \<and> etcb_at (\<lambda>t. tcb_priority t = p \<and> tcb_domain t = d) t s \<and> st_tcb_at runnable t s) \<and> distinct (ready_queues s d p)\<rbrakk> \<Longrightarrow> is_etcb_at t b \<and> etcb_at (\<lambda>t. tcb_priority t = p \<and> tcb_domain t = d) t b \<and> st_tcb_at runnable t b
 2. \<And>s a b. \<lbrakk>(a, b) \<in> fst (f s); I s; ct_active s; valid_etcbs s; valid_queues s; ct_not_in_q s; valid_sched_action s; ct_in_cur_domain s; valid_blocked s; valid_idle_etcb s; valid_idle s; valid_etcbs b; valid_blocked b; ready_queues b = ready_queues s \<and> scheduler_action b = scheduler_action s \<and> cur_domain b = cur_domain s\<rbrakk> \<Longrightarrow> ct_not_in_q b \<and> valid_sched_action b \<and> ct_in_cur_domain b \<and> valid_idle_etcb b proof (prove)
goal (2 subgoals):
 1. \<And>s a b d p t. \<lbrakk>(a, b) \<in> fst (f s); I s; ct_active s; valid_etcbs s; ct_not_in_q s; valid_sched_action s; ct_in_cur_domain s; valid_blocked s; valid_idle_etcb s; valid_idle s; valid_etcbs b; valid_blocked_2 (ready_queues s) (kheap b) (scheduler_action s) (cur_thread b); t \<in> set (ready_queues s d p); ready_queues b = ready_queues s; scheduler_action b = scheduler_action s; cur_domain b = cur_domain s; \<forall>t\<in>set (ready_queues s d p). is_etcb_at t s \<and> etcb_at (\<lambda>t. tcb_priority t = p \<and> tcb_domain t = d) t s \<and> st_tcb_at runnable t s; distinct (ready_queues s d p)\<rbrakk> \<Longrightarrow> is_etcb_at t b \<and> etcb_at (\<lambda>t. tcb_priority t = p \<and> tcb_domain t = d) t b \<and> st_tcb_at runnable t b
 2. \<And>s a b. \<lbrakk>(a, b) \<in> fst (f s); I s; ct_active s; valid_etcbs s; valid_queues s; ct_not_in_q s; valid_sched_action s; ct_in_cur_domain s; valid_blocked s; valid_idle_etcb s; valid_idle s; valid_etcbs b; valid_blocked b; ready_queues b = ready_queues s \<and> scheduler_action b = scheduler_action s \<and> cur_domain b = cur_domain s\<rbrakk> \<Longrightarrow> ct_not_in_q b \<and> valid_sched_action b \<and> ct_in_cur_domain b \<and> valid_idle_etcb b proof (prove)
goal (3 subgoals):
 1. \<And>s a b d p t. \<lbrakk>(a, b) \<in> fst (f s); I s; ct_active s; valid_etcbs s; ct_not_in_q s; valid_sched_action s; ct_in_cur_domain s; valid_blocked s; valid_idle_etcb s; valid_idle s; valid_etcbs b; valid_blocked_2 (ready_queues s) (kheap b) (scheduler_action s) (cur_thread b); t \<in> set (ready_queues s d p); ready_queues b = ready_queues s; scheduler_action b = scheduler_action s; cur_domain b = cur_domain s; distinct (ready_queues s d p)\<rbrakk> \<Longrightarrow> t \<in> set (ready_queues s d p)
 2. \<And>s a b d p t. \<lbrakk>(a, b) \<in> fst (f s); I s; ct_active s; valid_etcbs s; ct_not_in_q s; valid_sched_action s; ct_in_cur_domain s; valid_blocked s; valid_idle_etcb s; valid_idle s; valid_etcbs b; valid_blocked_2 (ready_queues s) (kheap b) (scheduler_action s) (cur_thread b); t \<in> set (ready_queues s d p); ready_queues b = ready_queues s; scheduler_action b = scheduler_action s; cur_domain b = cur_domain s; distinct (ready_queues s d p); is_etcb_at t s \<and> etcb_at (\<lambda>t. tcb_priority t = p \<and> tcb_domain t = d) t s \<and> st_tcb_at runnable t s\<rbrakk> \<Longrightarrow> is_etcb_at t b \<and> etcb_at (\<lambda>t. tcb_priority t = p \<and> tcb_domain t = d) t b \<and> st_tcb_at runnable t b
 3. \<And>s a b. \<lbrakk>(a, b) \<in> fst (f s); I s; ct_active s; valid_etcbs s; valid_queues s; ct_not_in_q s; valid_sched_action s; ct_in_cur_domain s; valid_blocked s; valid_idle_etcb s; valid_idle s; valid_etcbs b; valid_blocked b; ready_queues b = ready_queues s \<and> scheduler_action b = scheduler_action s \<and> cur_domain b = cur_domain s\<rbrakk> \<Longrightarrow> ct_not_in_q b \<and> valid_sched_action b \<and> ct_in_cur_domain b \<and> valid_idle_etcb b proof (prove)
goal (2 subgoals):
 1. \<And>s a b d p t. \<lbrakk>(a, b) \<in> fst (f s); I s; ct_active s; valid_etcbs s; ct_not_in_q s; valid_sched_action s; ct_in_cur_domain s; valid_blocked s; valid_idle_etcb s; valid_idle s; valid_etcbs b; valid_blocked_2 (ready_queues s) (kheap b) (scheduler_action s) (cur_thread b); t \<in> set (ready_queues s d p); ready_queues b = ready_queues s; scheduler_action b = scheduler_action s; cur_domain b = cur_domain s; distinct (ready_queues s d p); is_etcb_at t s \<and> etcb_at (\<lambda>t. tcb_priority t = p \<and> tcb_domain t = d) t s \<and> st_tcb_at runnable t s\<rbrakk> \<Longrightarrow> is_etcb_at t b \<and> etcb_at (\<lambda>t. tcb_priority t = p \<and> tcb_domain t = d) t b \<and> st_tcb_at runnable t b
 2. \<And>s a b. \<lbrakk>(a, b) \<in> fst (f s); I s; ct_active s; valid_etcbs s; valid_queues s; ct_not_in_q s; valid_sched_action s; ct_in_cur_domain s; valid_blocked s; valid_idle_etcb s; valid_idle s; valid_etcbs b; valid_blocked b; ready_queues b = ready_queues s \<and> scheduler_action b = scheduler_action s \<and> cur_domain b = cur_domain s\<rbrakk> \<Longrightarrow> ct_not_in_q b \<and> valid_sched_action b \<and> ct_in_cur_domain b \<and> valid_idle_etcb b proof (prove)
goal (2 subgoals):
 1. \<And>s a b d p t. \<lbrakk>(a, b) \<in> fst (f s); I s; ct_active s; valid_etcbs s; ct_not_in_q s; valid_sched_action s; ct_in_cur_domain s; valid_blocked s; valid_idle_etcb s; valid_idle s; valid_etcbs b; valid_blocked_2 (ready_queues s) (kheap b) (scheduler_action s) (cur_thread b); t \<in> set (ready_queues s d p); ready_queues b = ready_queues s; scheduler_action b = scheduler_action s; cur_domain b = cur_domain s; distinct (ready_queues s d p); is_etcb_at t s; etcb_at (\<lambda>t. tcb_priority t = p \<and> tcb_domain t = d) t s; st_tcb_at runnable t s\<rbrakk> \<Longrightarrow> is_etcb_at t b \<and> etcb_at (\<lambda>t. tcb_priority t = p \<and> tcb_domain t = d) t b \<and> st_tcb_at runnable t b
 2. \<And>s a b. \<lbrakk>(a, b) \<in> fst (f s); I s; ct_active s; valid_etcbs s; valid_queues s; ct_not_in_q s; valid_sched_action s; ct_in_cur_domain s; valid_blocked s; valid_idle_etcb s; valid_idle s; valid_etcbs b; valid_blocked b; ready_queues b = ready_queues s \<and> scheduler_action b = scheduler_action s \<and> cur_domain b = cur_domain s\<rbrakk> \<Longrightarrow> ct_not_in_q b \<and> valid_sched_action b \<and> ct_in_cur_domain b \<and> valid_idle_etcb b proof (prove)
goal (3 subgoals):
 1. \<And>s a b d p t. \<lbrakk>(a, b) \<in> fst (f s); I s; ct_active s; valid_etcbs s; ct_not_in_q s; valid_sched_action s; ct_in_cur_domain s; valid_blocked s; valid_idle_etcb s; valid_idle s; valid_etcbs b; valid_blocked_2 (ready_queues s) (kheap b) (scheduler_action s) (cur_thread b); t \<in> set (ready_queues s d p); ready_queues b = ready_queues s; scheduler_action b = scheduler_action s; cur_domain b = cur_domain s; distinct (ready_queues s d p); is_etcb_at t s; etcb_at (\<lambda>t. tcb_priority t = p \<and> tcb_domain t = d) t s; st_tcb_at runnable t s; st_tcb_at runnable t b\<rbrakk> \<Longrightarrow> is_etcb_at t b \<and> etcb_at (\<lambda>t. tcb_priority t = p \<and> tcb_domain t = d) t b \<and> st_tcb_at runnable t b
 2. \<And>s a b d p t. \<lbrakk>(a, b) \<in> fst (f s); I s; ct_active s; valid_etcbs s; ct_not_in_q s; valid_sched_action s; ct_in_cur_domain s; valid_blocked s; valid_idle_etcb s; valid_idle s; valid_etcbs b; valid_blocked_2 (ready_queues s) (kheap b) (scheduler_action s) (cur_thread b); t \<in> set (ready_queues s d p); ready_queues b = ready_queues s; scheduler_action b = scheduler_action s; cur_domain b = cur_domain s; distinct (ready_queues s d p); is_etcb_at t s; etcb_at (\<lambda>t. tcb_priority t = p \<and> tcb_domain t = d) t s; st_tcb_at runnable t s\<rbrakk> \<Longrightarrow> st_tcb_at runnable t b
 3. \<And>s a b. \<lbrakk>(a, b) \<in> fst (f s); I s; ct_active s; valid_etcbs s; valid_queues s; ct_not_in_q s; valid_sched_action s; ct_in_cur_domain s; valid_blocked s; valid_idle_etcb s; valid_idle s; valid_etcbs b; valid_blocked b; ready_queues b = ready_queues s \<and> scheduler_action b = scheduler_action s \<and> cur_domain b = cur_domain s\<rbrakk> \<Longrightarrow> ct_not_in_q b \<and> valid_sched_action b \<and> ct_in_cur_domain b \<and> valid_idle_etcb b proof (prove)
goal (3 subgoals):
 1. \<And>s a b d p t. \<lbrakk>(a, b) \<in> fst (f s); I s; ct_active s; valid_etcbs s; ct_not_in_q s; valid_sched_action s; ct_in_cur_domain s; valid_blocked s; valid_idle_etcb s; valid_idle s; valid_etcbs b; valid_blocked_2 (ready_queues s) (kheap b) (scheduler_action s) (cur_thread b); t \<in> set (ready_queues s d p); ready_queues b = ready_queues s; scheduler_action b = scheduler_action s; cur_domain b = cur_domain s; distinct (ready_queues s d p); is_etcb_at t s; etcb_at (\<lambda>t. tcb_priority t = p \<and> tcb_domain t = d) t s; st_tcb_at runnable t s; st_tcb_at runnable t b\<rbrakk> \<Longrightarrow> is_etcb_at t b \<and> etcb_at (\<lambda>t. tcb_priority t = p \<and> tcb_domain t = d) t b
 2. \<And>s a b d p t. \<lbrakk>(a, b) \<in> fst (f s); I s; ct_active s; valid_etcbs s; ct_not_in_q s; valid_sched_action s; ct_in_cur_domain s; valid_blocked s; valid_idle_etcb s; valid_idle s; valid_etcbs b; valid_blocked_2 (ready_queues s) (kheap b) (scheduler_action s) (cur_thread b); t \<in> set (ready_queues s d p); ready_queues b = ready_queues s; scheduler_action b = scheduler_action s; cur_domain b = cur_domain s; distinct (ready_queues s d p); is_etcb_at t s; etcb_at (\<lambda>t. tcb_priority t = p \<and> tcb_domain t = d) t s; st_tcb_at runnable t s\<rbrakk> \<Longrightarrow> st_tcb_at runnable t b
 3. \<And>s a b. \<lbrakk>(a, b) \<in> fst (f s); I s; ct_active s; valid_etcbs s; valid_queues s; ct_not_in_q s; valid_sched_action s; ct_in_cur_domain s; valid_blocked s; valid_idle_etcb s; valid_idle s; valid_etcbs b; valid_blocked b; ready_queues b = ready_queues s \<and> scheduler_action b = scheduler_action s \<and> cur_domain b = cur_domain s\<rbrakk> \<Longrightarrow> ct_not_in_q b \<and> valid_sched_action b \<and> ct_in_cur_domain b \<and> valid_idle_etcb b proof (prove)
goal (4 subgoals):
 1. \<And>s a b d p t. \<lbrakk>(a, b) \<in> fst (f s); I s; ct_active s; valid_etcbs s; ct_not_in_q s; valid_sched_action s; ct_in_cur_domain s; valid_blocked s; valid_idle_etcb s; valid_idle s; valid_etcbs b; valid_blocked_2 (ready_queues s) (kheap b) (scheduler_action s) (cur_thread b); t \<in> set (ready_queues s d p); ready_queues b = ready_queues s; scheduler_action b = scheduler_action s; cur_domain b = cur_domain s; distinct (ready_queues s d p); is_etcb_at t s; etcb_at (\<lambda>t. tcb_priority t = p \<and> tcb_domain t = d) t s; st_tcb_at runnable t s; st_tcb_at runnable t b\<rbrakk> \<Longrightarrow> is_etcb_at t b
 2. \<And>s a b d p t. \<lbrakk>(a, b) \<in> fst (f s); I s; ct_active s; valid_etcbs s; ct_not_in_q s; valid_sched_action s; ct_in_cur_domain s; valid_blocked s; valid_idle_etcb s; valid_idle s; valid_etcbs b; valid_blocked_2 (ready_queues s) (kheap b) (scheduler_action s) (cur_thread b); t \<in> set (ready_queues s d p); ready_queues b = ready_queues s; scheduler_action b = scheduler_action s; cur_domain b = cur_domain s; distinct (ready_queues s d p); is_etcb_at t s; etcb_at (\<lambda>t. tcb_priority t = p \<and> tcb_domain t = d) t s; st_tcb_at runnable t s; st_tcb_at runnable t b\<rbrakk> \<Longrightarrow> etcb_at (\<lambda>t. tcb_priority t = p \<and> tcb_domain t = d) t b
 3. \<And>s a b d p t. \<lbrakk>(a, b) \<in> fst (f s); I s; ct_active s; valid_etcbs s; ct_not_in_q s; valid_sched_action s; ct_in_cur_domain s; valid_blocked s; valid_idle_etcb s; valid_idle s; valid_etcbs b; valid_blocked_2 (ready_queues s) (kheap b) (scheduler_action s) (cur_thread b); t \<in> set (ready_queues s d p); ready_queues b = ready_queues s; scheduler_action b = scheduler_action s; cur_domain b = cur_domain s; distinct (ready_queues s d p); is_etcb_at t s; etcb_at (\<lambda>t. tcb_priority t = p \<and> tcb_domain t = d) t s; st_tcb_at runnable t s\<rbrakk> \<Longrightarrow> st_tcb_at runnable t b
 4. \<And>s a b. \<lbrakk>(a, b) \<in> fst (f s); I s; ct_active s; valid_etcbs s; valid_queues s; ct_not_in_q s; valid_sched_action s; ct_in_cur_domain s; valid_blocked s; valid_idle_etcb s; valid_idle s; valid_etcbs b; valid_blocked b; ready_queues b = ready_queues s \<and> scheduler_action b = scheduler_action s \<and> cur_domain b = cur_domain s\<rbrakk> \<Longrightarrow> ct_not_in_q b \<and> valid_sched_action b \<and> ct_in_cur_domain b \<and> valid_idle_etcb b proof (prove)
goal (3 subgoals):
 1. \<And>s a b d p t. \<lbrakk>(a, b) \<in> fst (f s); I s; ct_active s; valid_etcbs s; ct_not_in_q s; valid_sched_action s; ct_in_cur_domain s; valid_blocked s; valid_idle_etcb s; valid_idle s; valid_etcbs b; valid_blocked_2 (ready_queues s) (kheap b) (scheduler_action s) (cur_thread b); t \<in> set (ready_queues s d p); ready_queues b = ready_queues s; scheduler_action b = scheduler_action s; cur_domain b = cur_domain s; distinct (ready_queues s d p); is_etcb_at t s; etcb_at (\<lambda>t. tcb_priority t = p \<and> tcb_domain t = d) t s; st_tcb_at runnable t s; st_tcb_at runnable t b\<rbrakk> \<Longrightarrow> etcb_at (\<lambda>t. tcb_priority t = p \<and> tcb_domain t = d) t b
 2. \<And>s a b d p t. \<lbrakk>(a, b) \<in> fst (f s); I s; ct_active s; valid_etcbs s; ct_not_in_q s; valid_sched_action s; ct_in_cur_domain s; valid_blocked s; valid_idle_etcb s; valid_idle s; valid_etcbs b; valid_blocked_2 (ready_queues s) (kheap b) (scheduler_action s) (cur_thread b); t \<in> set (ready_queues s d p); ready_queues b = ready_queues s; scheduler_action b = scheduler_action s; cur_domain b = cur_domain s; distinct (ready_queues s d p); is_etcb_at t s; etcb_at (\<lambda>t. tcb_priority t = p \<and> tcb_domain t = d) t s; st_tcb_at runnable t s\<rbrakk> \<Longrightarrow> st_tcb_at runnable t b
 3. \<And>s a b. \<lbrakk>(a, b) \<in> fst (f s); I s; ct_active s; valid_etcbs s; valid_queues s; ct_not_in_q s; valid_sched_action s; ct_in_cur_domain s; valid_blocked s; valid_idle_etcb s; valid_idle s; valid_etcbs b; valid_blocked b; ready_queues b = ready_queues s \<and> scheduler_action b = scheduler_action s \<and> cur_domain b = cur_domain s\<rbrakk> \<Longrightarrow> ct_not_in_q b \<and> valid_sched_action b \<and> ct_in_cur_domain b \<and> valid_idle_etcb b proof (prove)
goal (4 subgoals):
 1. \<And>s a b d p t. \<lbrakk>(a, b) \<in> fst (f s); I s; ct_active s; valid_etcbs s; ct_not_in_q s; valid_sched_action s; ct_in_cur_domain s; valid_blocked s; valid_idle_etcb s; valid_idle s; valid_etcbs b; valid_blocked_2 (ready_queues s) (kheap b) (scheduler_action s) (cur_thread b); t \<in> set (ready_queues s d p); ready_queues b = ready_queues s; scheduler_action b = scheduler_action s; cur_domain b = cur_domain s; distinct (ready_queues s d p); is_etcb_at t s; etcb_at (\<lambda>t. tcb_priority t = p \<and> tcb_domain t = d) t s; st_tcb_at runnable t s; st_tcb_at runnable t b\<rbrakk> \<Longrightarrow> (etcb_at (\<lambda>t. tcb_priority t = p \<and> tcb_domain t = d) t and valid_etcbs) s
 2. \<And>s a b d p t. \<lbrakk>(a, b) \<in> fst (f s); I s; ct_active s; valid_etcbs s; ct_not_in_q s; valid_sched_action s; ct_in_cur_domain s; valid_blocked s; valid_idle_etcb s; valid_idle s; valid_etcbs b; valid_blocked_2 (ready_queues s) (kheap b) (scheduler_action s) (cur_thread b); t \<in> set (ready_queues s d p); ready_queues b = ready_queues s; scheduler_action b = scheduler_action s; cur_domain b = cur_domain s; distinct (ready_queues s d p); is_etcb_at t s; etcb_at (\<lambda>t. tcb_priority t = p \<and> tcb_domain t = d) t s; st_tcb_at runnable t s; st_tcb_at runnable t b; st_tcb_at (Not \<circ> inactive) t b \<longrightarrow> etcb_at (\<lambda>t. tcb_priority t = p \<and> tcb_domain t = d) t b\<rbrakk> \<Longrightarrow> etcb_at (\<lambda>t. tcb_priority t = p \<and> tcb_domain t = d) t b
 3. \<And>s a b d p t. \<lbrakk>(a, b) \<in> fst (f s); I s; ct_active s; valid_etcbs s; ct_not_in_q s; valid_sched_action s; ct_in_cur_domain s; valid_blocked s; valid_idle_etcb s; valid_idle s; valid_etcbs b; valid_blocked_2 (ready_queues s) (kheap b) (scheduler_action s) (cur_thread b); t \<in> set (ready_queues s d p); ready_queues b = ready_queues s; scheduler_action b = scheduler_action s; cur_domain b = cur_domain s; distinct (ready_queues s d p); is_etcb_at t s; etcb_at (\<lambda>t. tcb_priority t = p \<and> tcb_domain t = d) t s; st_tcb_at runnable t s\<rbrakk> \<Longrightarrow> st_tcb_at runnable t b
 4. \<And>s a b. \<lbrakk>(a, b) \<in> fst (f s); I s; ct_active s; valid_etcbs s; valid_queues s; ct_not_in_q s; valid_sched_action s; ct_in_cur_domain s; valid_blocked s; valid_idle_etcb s; valid_idle s; valid_etcbs b; valid_blocked b; ready_queues b = ready_queues s \<and> scheduler_action b = scheduler_action s \<and> cur_domain b = cur_domain s\<rbrakk> \<Longrightarrow> ct_not_in_q b \<and> valid_sched_action b \<and> ct_in_cur_domain b \<and> valid_idle_etcb b proof (prove)
goal (3 subgoals):
 1. \<And>s a b d p t. \<lbrakk>(a, b) \<in> fst (f s); I s; ct_active s; valid_etcbs s; ct_not_in_q s; valid_sched_action s; ct_in_cur_domain s; valid_blocked s; valid_idle_etcb s; valid_idle s; valid_etcbs b; valid_blocked_2 (ready_queues s) (kheap b) (scheduler_action s) (cur_thread b); t \<in> set (ready_queues s d p); ready_queues b = ready_queues s; scheduler_action b = scheduler_action s; cur_domain b = cur_domain s; distinct (ready_queues s d p); is_etcb_at t s; etcb_at (\<lambda>t. tcb_priority t = p \<and> tcb_domain t = d) t s; st_tcb_at runnable t s; st_tcb_at runnable t b; st_tcb_at (Not \<circ> inactive) t b \<longrightarrow> etcb_at (\<lambda>t. tcb_priority t = p \<and> tcb_domain t = d) t b\<rbrakk> \<Longrightarrow> etcb_at (\<lambda>t. tcb_priority t = p \<and> tcb_domain t = d) t b
 2. \<And>s a b d p t. \<lbrakk>(a, b) \<in> fst (f s); I s; ct_active s; valid_etcbs s; ct_not_in_q s; valid_sched_action s; ct_in_cur_domain s; valid_blocked s; valid_idle_etcb s; valid_idle s; valid_etcbs b; valid_blocked_2 (ready_queues s) (kheap b) (scheduler_action s) (cur_thread b); t \<in> set (ready_queues s d p); ready_queues b = ready_queues s; scheduler_action b = scheduler_action s; cur_domain b = cur_domain s; distinct (ready_queues s d p); is_etcb_at t s; etcb_at (\<lambda>t. tcb_priority t = p \<and> tcb_domain t = d) t s; st_tcb_at runnable t s\<rbrakk> \<Longrightarrow> st_tcb_at runnable t b
 3. \<And>s a b. \<lbrakk>(a, b) \<in> fst (f s); I s; ct_active s; valid_etcbs s; valid_queues s; ct_not_in_q s; valid_sched_action s; ct_in_cur_domain s; valid_blocked s; valid_idle_etcb s; valid_idle s; valid_etcbs b; valid_blocked b; ready_queues b = ready_queues s \<and> scheduler_action b = scheduler_action s \<and> cur_domain b = cur_domain s\<rbrakk> \<Longrightarrow> ct_not_in_q b \<and> valid_sched_action b \<and> ct_in_cur_domain b \<and> valid_idle_etcb b proof (prove)
goal (3 subgoals):
 1. \<And>s a b d p t. \<lbrakk>(a, b) \<in> fst (f s); I s; ct_active s; valid_etcbs s; ct_not_in_q s; valid_sched_action s; ct_in_cur_domain s; valid_blocked s; valid_idle_etcb s; valid_idle s; valid_etcbs b; valid_blocked_2 (ready_queues s) (kheap b) (scheduler_action s) (cur_thread b); t \<in> set (ready_queues s d p); ready_queues b = ready_queues s; scheduler_action b = scheduler_action s; cur_domain b = cur_domain s; distinct (ready_queues s d p); is_etcb_at t s; etcb_at (\<lambda>t. tcb_priority t = p \<and> tcb_domain t = d) t s; \<exists>ko. kheap s t = Some ko \<and> (\<exists>tcb. ko = TCB tcb \<and> runnable (tcb_state tcb)); \<exists>ko. kheap b t = Some ko \<and> (\<exists>tcb. ko = TCB tcb \<and> runnable (tcb_state tcb)); (\<exists>ko. kheap b t = Some ko \<and> (\<exists>tcb. ko = TCB tcb \<and> tcb_state tcb \<noteq> Inactive)) \<longrightarrow> etcb_at (\<lambda>t. tcb_priority t = p \<and> tcb_domain t = d) t b\<rbrakk> \<Longrightarrow> etcb_at (\<lambda>t. tcb_priority t = p \<and> tcb_domain t = d) t b
 2. \<And>s a b d p t. \<lbrakk>(a, b) \<in> fst (f s); I s; ct_active s; valid_etcbs s; ct_not_in_q s; valid_sched_action s; ct_in_cur_domain s; valid_blocked s; valid_idle_etcb s; valid_idle s; valid_etcbs b; valid_blocked_2 (ready_queues s) (kheap b) (scheduler_action s) (cur_thread b); t \<in> set (ready_queues s d p); ready_queues b = ready_queues s; scheduler_action b = scheduler_action s; cur_domain b = cur_domain s; distinct (ready_queues s d p); is_etcb_at t s; etcb_at (\<lambda>t. tcb_priority t = p \<and> tcb_domain t = d) t s; st_tcb_at runnable t s\<rbrakk> \<Longrightarrow> st_tcb_at runnable t b
 3. \<And>s a b. \<lbrakk>(a, b) \<in> fst (f s); I s; ct_active s; valid_etcbs s; valid_queues s; ct_not_in_q s; valid_sched_action s; ct_in_cur_domain s; valid_blocked s; valid_idle_etcb s; valid_idle s; valid_etcbs b; valid_blocked b; ready_queues b = ready_queues s \<and> scheduler_action b = scheduler_action s \<and> cur_domain b = cur_domain s\<rbrakk> \<Longrightarrow> ct_not_in_q b \<and> valid_sched_action b \<and> ct_in_cur_domain b \<and> valid_idle_etcb b proof (prove)
goal (2 subgoals):
 1. \<And>s a b d p t. \<lbrakk>(a, b) \<in> fst (f s); I s; ct_active s; valid_etcbs s; ct_not_in_q s; valid_sched_action s; ct_in_cur_domain s; valid_blocked s; valid_idle_etcb s; valid_idle s; valid_etcbs b; valid_blocked_2 (ready_queues s) (kheap b) (scheduler_action s) (cur_thread b); t \<in> set (ready_queues s d p); ready_queues b = ready_queues s; scheduler_action b = scheduler_action s; cur_domain b = cur_domain s; distinct (ready_queues s d p); is_etcb_at t s; etcb_at (\<lambda>t. tcb_priority t = p \<and> tcb_domain t = d) t s; st_tcb_at runnable t s\<rbrakk> \<Longrightarrow> st_tcb_at runnable t b
 2. \<And>s a b. \<lbrakk>(a, b) \<in> fst (f s); I s; ct_active s; valid_etcbs s; valid_queues s; ct_not_in_q s; valid_sched_action s; ct_in_cur_domain s; valid_blocked s; valid_idle_etcb s; valid_idle s; valid_etcbs b; valid_blocked b; ready_queues b = ready_queues s \<and> scheduler_action b = scheduler_action s \<and> cur_domain b = cur_domain s\<rbrakk> \<Longrightarrow> ct_not_in_q b \<and> valid_sched_action b \<and> ct_in_cur_domain b \<and> valid_idle_etcb b proof (prove)
goal (2 subgoals):
 1. \<And>s a b d p t. \<lbrakk>(a, b) \<in> fst (f s); I s; ct_active s; valid_etcbs s; ct_not_in_q s; valid_sched_action s; ct_in_cur_domain s; valid_blocked s; valid_idle_etcb s; valid_idle s; valid_etcbs b; valid_blocked_2 (ready_queues s) (kheap b) (scheduler_action s) (cur_thread b); t \<in> set (ready_queues s d p); ready_queues b = ready_queues s; scheduler_action b = scheduler_action s; cur_domain b = cur_domain s; distinct (ready_queues s d p); is_etcb_at t s; etcb_at (\<lambda>t. tcb_priority t = p \<and> tcb_domain t = d) t s; st_tcb_at runnable t s\<rbrakk> \<Longrightarrow> (I and ct_active and st_tcb_at (runnable and Not \<circ> inactive and Not \<circ> idle) t) s
 2. \<And>s a b. \<lbrakk>(a, b) \<in> fst (f s); I s; ct_active s; valid_etcbs s; valid_queues s; ct_not_in_q s; valid_sched_action s; ct_in_cur_domain s; valid_blocked s; valid_idle_etcb s; valid_idle s; valid_etcbs b; valid_blocked b; ready_queues b = ready_queues s \<and> scheduler_action b = scheduler_action s \<and> cur_domain b = cur_domain s\<rbrakk> \<Longrightarrow> ct_not_in_q b \<and> valid_sched_action b \<and> ct_in_cur_domain b \<and> valid_idle_etcb b proof (prove)
goal (2 subgoals):
 1. \<And>s a b d p t. \<lbrakk>(a, b) \<in> fst (f s); I s; ct_active s; valid_etcbs s; ct_not_in_q s; valid_sched_action s; ct_in_cur_domain s; valid_blocked s; valid_idle_etcb s; valid_idle s; valid_etcbs b; valid_blocked_2 (ready_queues s) (kheap b) (scheduler_action s) (cur_thread b); t \<in> set (ready_queues s d p); ready_queues b = ready_queues s; scheduler_action b = scheduler_action s; cur_domain b = cur_domain s; distinct (ready_queues s d p); is_etcb_at t s; etcb_at (\<lambda>t. tcb_priority t = p \<and> tcb_domain t = d) t s; st_tcb_at runnable t s\<rbrakk> \<Longrightarrow> st_tcb_at (runnable and Not \<circ> inactive and Not \<circ> idle) t s
 2. \<And>s a b. \<lbrakk>(a, b) \<in> fst (f s); I s; ct_active s; valid_etcbs s; valid_queues s; ct_not_in_q s; valid_sched_action s; ct_in_cur_domain s; valid_blocked s; valid_idle_etcb s; valid_idle s; valid_etcbs b; valid_blocked b; ready_queues b = ready_queues s \<and> scheduler_action b = scheduler_action s \<and> cur_domain b = cur_domain s\<rbrakk> \<Longrightarrow> ct_not_in_q b \<and> valid_sched_action b \<and> ct_in_cur_domain b \<and> valid_idle_etcb b proof (prove)
goal (2 subgoals):
 1. \<And>s a b d p t tcb. \<lbrakk>(a, b) \<in> fst (f s); I s; ct_active s; valid_etcbs s; ct_not_in_q s; valid_sched_action s; ct_in_cur_domain s; valid_blocked s; valid_idle_etcb s; valid_idle s; valid_etcbs b; valid_blocked_2 (ready_queues s) (kheap b) (scheduler_action s) (cur_thread b); t \<in> set (ready_queues s d p); ready_queues b = ready_queues s; scheduler_action b = scheduler_action s; cur_domain b = cur_domain s; distinct (ready_queues s d p); is_etcb_at t s; etcb_at (\<lambda>t. tcb_priority t = p \<and> tcb_domain t = d) t s; runnable (itcb_state tcb)\<rbrakk> \<Longrightarrow> (runnable and Not \<circ> inactive and Not \<circ> idle) (itcb_state tcb)
 2. \<And>s a b. \<lbrakk>(a, b) \<in> fst (f s); I s; ct_active s; valid_etcbs s; valid_queues s; ct_not_in_q s; valid_sched_action s; ct_in_cur_domain s; valid_blocked s; valid_idle_etcb s; valid_idle s; valid_etcbs b; valid_blocked b; ready_queues b = ready_queues s \<and> scheduler_action b = scheduler_action s \<and> cur_domain b = cur_domain s\<rbrakk> \<Longrightarrow> ct_not_in_q b \<and> valid_sched_action b \<and> ct_in_cur_domain b \<and> valid_idle_etcb b proof (prove)
goal (2 subgoals):
 1. \<And>s a b d p t tcb. \<lbrakk>(a, b) \<in> fst (f s); I s; ct_active s; valid_etcbs s; ct_not_in_q s; valid_sched_action s; ct_in_cur_domain s; valid_blocked s; valid_idle_etcb s; valid_idle s; valid_etcbs b; valid_blocked_2 (ready_queues s) (kheap b) (scheduler_action s) (cur_thread b); t \<in> set (ready_queues s d p); ready_queues b = ready_queues s; scheduler_action b = scheduler_action s; cur_domain b = cur_domain s; distinct (ready_queues s d p); is_etcb_at t s; etcb_at (\<lambda>t. tcb_priority t = p \<and> tcb_domain t = d) t s; runnable (itcb_state tcb)\<rbrakk> \<Longrightarrow> itcb_state tcb \<noteq> Inactive \<and> itcb_state tcb \<noteq> IdleThreadState
 2. \<And>s a b. \<lbrakk>(a, b) \<in> fst (f s); I s; ct_active s; valid_etcbs s; valid_queues s; ct_not_in_q s; valid_sched_action s; ct_in_cur_domain s; valid_blocked s; valid_idle_etcb s; valid_idle s; valid_etcbs b; valid_blocked b; ready_queues b = ready_queues s \<and> scheduler_action b = scheduler_action s \<and> cur_domain b = cur_domain s\<rbrakk> \<Longrightarrow> ct_not_in_q b \<and> valid_sched_action b \<and> ct_in_cur_domain b \<and> valid_idle_etcb b proof (prove)
goal (9 subgoals):
 1. \<And>s a b d p t tcb. \<lbrakk>(a, b) \<in> fst (f s); I s; ct_active s; valid_etcbs s; ct_not_in_q s; valid_sched_action s; ct_in_cur_domain s; valid_blocked s; valid_idle_etcb s; valid_idle s; valid_etcbs b; valid_blocked_2 (ready_queues s) (kheap b) (scheduler_action s) (cur_thread b); t \<in> set (ready_queues s d p); ready_queues b = ready_queues s; scheduler_action b = scheduler_action s; cur_domain b = cur_domain s; distinct (ready_queues s d p); is_etcb_at t s; etcb_at (\<lambda>t. tcb_priority t = p \<and> tcb_domain t = d) t s; runnable (itcb_state tcb); itcb_state tcb = Running\<rbrakk> \<Longrightarrow> itcb_state tcb \<noteq> Inactive \<and> itcb_state tcb \<noteq> IdleThreadState
 2. \<And>s a b d p t tcb. \<lbrakk>(a, b) \<in> fst (f s); I s; ct_active s; valid_etcbs s; ct_not_in_q s; valid_sched_action s; ct_in_cur_domain s; valid_blocked s; valid_idle_etcb s; valid_idle s; valid_etcbs b; valid_blocked_2 (ready_queues s) (kheap b) (scheduler_action s) (cur_thread b); t \<in> set (ready_queues s d p); ready_queues b = ready_queues s; scheduler_action b = scheduler_action s; cur_domain b = cur_domain s; distinct (ready_queues s d p); is_etcb_at t s; etcb_at (\<lambda>t. tcb_priority t = p \<and> tcb_domain t = d) t s; runnable (itcb_state tcb); inactive (itcb_state tcb)\<rbrakk> \<Longrightarrow> itcb_state tcb \<noteq> Inactive \<and> itcb_state tcb \<noteq> IdleThreadState
 3. \<And>s a b d p t tcb. \<lbrakk>(a, b) \<in> fst (f s); I s; ct_active s; valid_etcbs s; ct_not_in_q s; valid_sched_action s; ct_in_cur_domain s; valid_blocked s; valid_idle_etcb s; valid_idle s; valid_etcbs b; valid_blocked_2 (ready_queues s) (kheap b) (scheduler_action s) (cur_thread b); t \<in> set (ready_queues s d p); ready_queues b = ready_queues s; scheduler_action b = scheduler_action s; cur_domain b = cur_domain s; distinct (ready_queues s d p); is_etcb_at t s; etcb_at (\<lambda>t. tcb_priority t = p \<and> tcb_domain t = d) t s; runnable (itcb_state tcb); itcb_state tcb = Restart\<rbrakk> \<Longrightarrow> itcb_state tcb \<noteq> Inactive \<and> itcb_state tcb \<noteq> IdleThreadState
 4. \<And>s a b d p t tcb x41 x42. \<lbrakk>(a, b) \<in> fst (f s); I s; ct_active s; valid_etcbs s; ct_not_in_q s; valid_sched_action s; ct_in_cur_domain s; valid_blocked s; valid_idle_etcb s; valid_idle s; valid_etcbs b; valid_blocked_2 (ready_queues s) (kheap b) (scheduler_action s) (cur_thread b); t \<in> set (ready_queues s d p); ready_queues b = ready_queues s; scheduler_action b = scheduler_action s; cur_domain b = cur_domain s; distinct (ready_queues s d p); is_etcb_at t s; etcb_at (\<lambda>t. tcb_priority t = p \<and> tcb_domain t = d) t s; runnable (itcb_state tcb); itcb_state tcb = BlockedOnReceive x41 x42\<rbrakk> \<Longrightarrow> itcb_state tcb \<noteq> Inactive \<and> itcb_state tcb \<noteq> IdleThreadState
 5. \<And>s a b d p t tcb x51 x52. \<lbrakk>(a, b) \<in> fst (f s); I s; ct_active s; valid_etcbs s; ct_not_in_q s; valid_sched_action s; ct_in_cur_domain s; valid_blocked s; valid_idle_etcb s; valid_idle s; valid_etcbs b; valid_blocked_2 (ready_queues s) (kheap b) (scheduler_action s) (cur_thread b); t \<in> set (ready_queues s d p); ready_queues b = ready_queues s; scheduler_action b = scheduler_action s; cur_domain b = cur_domain s; distinct (ready_queues s d p); is_etcb_at t s; etcb_at (\<lambda>t. tcb_priority t = p \<and> tcb_domain t = d) t s; runnable (itcb_state tcb); itcb_state tcb = BlockedOnSend x51 x52\<rbrakk> \<Longrightarrow> itcb_state tcb \<noteq> Inactive \<and> itcb_state tcb \<noteq> IdleThreadState
 6. \<And>s a b d p t tcb. \<lbrakk>(a, b) \<in> fst (f s); I s; ct_active s; valid_etcbs s; ct_not_in_q s; valid_sched_action s; ct_in_cur_domain s; valid_blocked s; valid_idle_etcb s; valid_idle s; valid_etcbs b; valid_blocked_2 (ready_queues s) (kheap b) (scheduler_action s) (cur_thread b); t \<in> set (ready_queues s d p); ready_queues b = ready_queues s; scheduler_action b = scheduler_action s; cur_domain b = cur_domain s; distinct (ready_queues s d p); is_etcb_at t s; etcb_at (\<lambda>t. tcb_priority t = p \<and> tcb_domain t = d) t s; runnable (itcb_state tcb); awaiting_reply (itcb_state tcb)\<rbrakk> \<Longrightarrow> itcb_state tcb \<noteq> Inactive \<and> itcb_state tcb \<noteq> IdleThreadState
 7. \<And>s a b d p t tcb x7. \<lbrakk>(a, b) \<in> fst (f s); I s; ct_active s; valid_etcbs s; ct_not_in_q s; valid_sched_action s; ct_in_cur_domain s; valid_blocked s; valid_idle_etcb s; valid_idle s; valid_etcbs b; valid_blocked_2 (ready_queues s) (kheap b) (scheduler_action s) (cur_thread b); t \<in> set (ready_queues s d p); ready_queues b = ready_queues s; scheduler_action b = scheduler_action s; cur_domain b = cur_domain s; distinct (ready_queues s d p); is_etcb_at t s; etcb_at (\<lambda>t. tcb_priority t = p \<and> tcb_domain t = d) t s; runnable (itcb_state tcb); itcb_state tcb = BlockedOnNotification x7\<rbrakk> \<Longrightarrow> itcb_state tcb \<noteq> Inactive \<and> itcb_state tcb \<noteq> IdleThreadState
 8. \<And>s a b d p t tcb. \<lbrakk>(a, b) \<in> fst (f s); I s; ct_active s; valid_etcbs s; ct_not_in_q s; valid_sched_action s; ct_in_cur_domain s; valid_blocked s; valid_idle_etcb s; valid_idle s; valid_etcbs b; valid_blocked_2 (ready_queues s) (kheap b) (scheduler_action s) (cur_thread b); t \<in> set (ready_queues s d p); ready_queues b = ready_queues s; scheduler_action b = scheduler_action s; cur_domain b = cur_domain s; distinct (ready_queues s d p); is_etcb_at t s; etcb_at (\<lambda>t. tcb_priority t = p \<and> tcb_domain t = d) t s; runnable (itcb_state tcb); idle (itcb_state tcb)\<rbrakk> \<Longrightarrow> itcb_state tcb \<noteq> Inactive \<and> itcb_state tcb \<noteq> IdleThreadState
 9. \<And>s a b. \<lbrakk>(a, b) \<in> fst (f s); I s; ct_active s; valid_etcbs s; valid_queues s; ct_not_in_q s; valid_sched_action s; ct_in_cur_domain s; valid_blocked s; valid_idle_etcb s; valid_idle s; valid_etcbs b; valid_blocked b; ready_queues b = ready_queues s \<and> scheduler_action b = scheduler_action s \<and> cur_domain b = cur_domain s\<rbrakk> \<Longrightarrow> ct_not_in_q b \<and> valid_sched_action b \<and> ct_in_cur_domain b \<and> valid_idle_etcb b proof (prove)
goal (1 subgoal):
 1. \<And>s a b. \<lbrakk>(a, b) \<in> fst (f s); I s; ct_active s; valid_etcbs s; valid_queues s; ct_not_in_q s; valid_sched_action s; ct_in_cur_domain s; valid_blocked s; valid_idle_etcb s; valid_idle s; valid_etcbs b; valid_blocked_2 (ready_queues s) (kheap b) (scheduler_action s) (cur_thread b); ready_queues b = ready_queues s \<and> scheduler_action b = scheduler_action s \<and> cur_domain b = cur_domain s\<rbrakk> \<Longrightarrow> ct_not_in_q_2 (ready_queues s) (scheduler_action s) (cur_thread b) \<and> valid_sched_action_2 (scheduler_action s) (ekheap b) (kheap b) (cur_thread b) (cur_domain s) \<and> ct_in_cur_domain_2 (cur_thread b) (idle_thread b) (scheduler_action s) (cur_domain s) (ekheap b) \<and> valid_idle_etcb b proof (prove)
goal (2 subgoals):
 1. \<And>s a b. \<lbrakk>(a, b) \<in> fst (f s); I s; ct_active s; valid_etcbs s; valid_queues s; ct_not_in_q s; valid_sched_action s; ct_in_cur_domain s; valid_blocked s; valid_idle_etcb s; valid_idle s; valid_etcbs b; valid_blocked_2 (ready_queues s) (kheap b) (scheduler_action s) (cur_thread b); ready_queues b = ready_queues s \<and> scheduler_action b = scheduler_action s \<and> cur_domain b = cur_domain s\<rbrakk> \<Longrightarrow> cur_thread s = cur_thread s
 2. \<And>s a b. \<lbrakk>(a, b) \<in> fst (f s); I s; ct_active s; valid_etcbs s; valid_queues s; ct_not_in_q s; valid_sched_action s; ct_in_cur_domain s; valid_blocked s; valid_idle_etcb s; valid_idle s; valid_etcbs b; valid_blocked_2 (ready_queues s) (kheap b) (scheduler_action s) (cur_thread b); ready_queues b = ready_queues s \<and> scheduler_action b = scheduler_action s \<and> cur_domain b = cur_domain s; cur_thread b = cur_thread s\<rbrakk> \<Longrightarrow> ct_not_in_q_2 (ready_queues s) (scheduler_action s) (cur_thread b) \<and> valid_sched_action_2 (scheduler_action s) (ekheap b) (kheap b) (cur_thread b) (cur_domain s) \<and> ct_in_cur_domain_2 (cur_thread b) (idle_thread b) (scheduler_action s) (cur_domain s) (ekheap b) \<and> valid_idle_etcb b proof (prove)
goal (1 subgoal):
 1. \<And>s a b. \<lbrakk>(a, b) \<in> fst (f s); I s; ct_active s; valid_etcbs s; valid_queues s; ct_not_in_q s; valid_sched_action s; ct_in_cur_domain s; valid_blocked s; valid_idle_etcb s; valid_idle s; valid_etcbs b; valid_blocked_2 (ready_queues s) (kheap b) (scheduler_action s) (cur_thread b); ready_queues b = ready_queues s \<and> scheduler_action b = scheduler_action s \<and> cur_domain b = cur_domain s; cur_thread b = cur_thread s\<rbrakk> \<Longrightarrow> ct_not_in_q_2 (ready_queues s) (scheduler_action s) (cur_thread b) \<and> valid_sched_action_2 (scheduler_action s) (ekheap b) (kheap b) (cur_thread b) (cur_domain s) \<and> ct_in_cur_domain_2 (cur_thread b) (idle_thread b) (scheduler_action s) (cur_domain s) (ekheap b) \<and> valid_idle_etcb b proof (prove)
goal (2 subgoals):
 1. \<And>s a b. \<lbrakk>(a, b) \<in> fst (f s); I s; ct_active s; valid_etcbs s; valid_queues s; ct_not_in_q s; valid_sched_action s; ct_in_cur_domain s; valid_blocked s; valid_idle_etcb s; valid_idle s; valid_etcbs b; valid_blocked_2 (ready_queues s) (kheap b) (scheduler_action s) (cur_thread b); ready_queues b = ready_queues s \<and> scheduler_action b = scheduler_action s \<and> cur_domain b = cur_domain s; cur_thread b = cur_thread s\<rbrakk> \<Longrightarrow> ct_not_in_q_2 (ready_queues s) (scheduler_action s) (cur_thread b)
 2. \<And>s a b. \<lbrakk>(a, b) \<in> fst (f s); I s; ct_active s; valid_etcbs s; valid_queues s; ct_not_in_q s; valid_sched_action s; ct_in_cur_domain s; valid_blocked s; valid_idle_etcb s; valid_idle s; valid_etcbs b; valid_blocked_2 (ready_queues s) (kheap b) (scheduler_action s) (cur_thread b); ready_queues b = ready_queues s \<and> scheduler_action b = scheduler_action s \<and> cur_domain b = cur_domain s; cur_thread b = cur_thread s\<rbrakk> \<Longrightarrow> valid_sched_action_2 (scheduler_action s) (ekheap b) (kheap b) (cur_thread b) (cur_domain s) \<and> ct_in_cur_domain_2 (cur_thread b) (idle_thread b) (scheduler_action s) (cur_domain s) (ekheap b) \<and> valid_idle_etcb b proof (prove)
goal (1 subgoal):
 1. \<And>s a b. \<lbrakk>(a, b) \<in> fst (f s); I s; ct_active s; valid_etcbs s; valid_queues s; ct_not_in_q s; valid_sched_action s; ct_in_cur_domain s; valid_blocked s; valid_idle_etcb s; valid_idle s; valid_etcbs b; valid_blocked_2 (ready_queues s) (kheap b) (scheduler_action s) (cur_thread b); ready_queues b = ready_queues s \<and> scheduler_action b = scheduler_action s \<and> cur_domain b = cur_domain s; cur_thread b = cur_thread s\<rbrakk> \<Longrightarrow> valid_sched_action_2 (scheduler_action s) (ekheap b) (kheap b) (cur_thread b) (cur_domain s) \<and> ct_in_cur_domain_2 (cur_thread b) (idle_thread b) (scheduler_action s) (cur_domain s) (ekheap b) \<and> valid_idle_etcb b proof (prove)
goal (1 subgoal):
 1. \<And>s a b. \<lbrakk>(a, b) \<in> fst (f s); I s; ct_active s; valid_etcbs s; valid_queues s; ct_not_in_q s; valid_sched_action s; ct_in_cur_domain s; valid_blocked s; valid_idle_etcb s; valid_idle s; valid_etcbs b; valid_blocked_2 (ready_queues s) (kheap b) (scheduler_action s) (cur_thread s); ready_queues b = ready_queues s \<and> scheduler_action b = scheduler_action s \<and> cur_domain b = cur_domain s; cur_thread b = cur_thread s\<rbrakk> \<Longrightarrow> valid_sched_action_2 (scheduler_action s) (ekheap b) (kheap b) (cur_thread s) (cur_domain s) \<and> ct_in_cur_domain_2 (cur_thread s) (idle_thread b) (scheduler_action s) (cur_domain s) (ekheap b) \<and> valid_idle_etcb b proof (prove)
goal (1 subgoal):
 1. \<And>s a b. \<lbrakk>(a, b) \<in> fst (f s); I s; ct_active s; valid_etcbs s; valid_queues s; ct_not_in_q s; ct_in_cur_domain s; valid_blocked s; valid_idle_etcb s; valid_idle s; valid_etcbs b; valid_blocked_2 (ready_queues s) (kheap b) (scheduler_action s) (cur_thread s); cur_thread b = cur_thread s; scheduler_action s = resume_cur_thread \<longrightarrow> st_tcb_at activatable (cur_thread s) s; ready_queues b = ready_queues s; \<forall>t. scheduler_action s = switch_thread t \<longrightarrow> st_tcb_at runnable t s; switch_in_cur_domain s; scheduler_action b = scheduler_action s; cur_domain b = cur_domain s\<rbrakk> \<Longrightarrow> (scheduler_action s = resume_cur_thread \<longrightarrow> st_tcb_at activatable (cur_thread s) b) \<and> (\<forall>t. scheduler_action s = switch_thread t \<longrightarrow> st_tcb_at runnable t b) \<and> switch_in_cur_domain_2 (scheduler_action s) (ekheap b) (cur_domain s) \<and> ct_in_cur_domain_2 (cur_thread s) (idle_thread b) (scheduler_action s) (cur_domain s) (ekheap b) \<and> valid_idle_etcb b proof (prove)
goal (2 subgoals):
 1. \<And>s a b. \<lbrakk>(a, b) \<in> fst (f s); I s; ct_active s; valid_etcbs s; valid_queues s; ct_not_in_q s; ct_in_cur_domain s; valid_blocked s; valid_idle_etcb s; valid_idle s; valid_etcbs b; valid_blocked_2 (ready_queues s) (kheap b) (scheduler_action s) (cur_thread s); cur_thread b = cur_thread s; scheduler_action s = resume_cur_thread \<longrightarrow> st_tcb_at activatable (cur_thread s) s; ready_queues b = ready_queues s; \<forall>t. scheduler_action s = switch_thread t \<longrightarrow> st_tcb_at runnable t s; switch_in_cur_domain s; scheduler_action b = scheduler_action s; cur_domain b = cur_domain s\<rbrakk> \<Longrightarrow> scheduler_action s = resume_cur_thread \<longrightarrow> st_tcb_at activatable (cur_thread s) b
 2. \<And>s a b. \<lbrakk>(a, b) \<in> fst (f s); I s; ct_active s; valid_etcbs s; valid_queues s; ct_not_in_q s; ct_in_cur_domain s; valid_blocked s; valid_idle_etcb s; valid_idle s; valid_etcbs b; valid_blocked_2 (ready_queues s) (kheap b) (scheduler_action s) (cur_thread s); cur_thread b = cur_thread s; scheduler_action s = resume_cur_thread \<longrightarrow> st_tcb_at activatable (cur_thread s) s; ready_queues b = ready_queues s; \<forall>t. scheduler_action s = switch_thread t \<longrightarrow> st_tcb_at runnable t s; switch_in_cur_domain s; scheduler_action b = scheduler_action s; cur_domain b = cur_domain s\<rbrakk> \<Longrightarrow> (\<forall>t. scheduler_action s = switch_thread t \<longrightarrow> st_tcb_at runnable t b) \<and> switch_in_cur_domain_2 (scheduler_action s) (ekheap b) (cur_domain s) \<and> ct_in_cur_domain_2 (cur_thread s) (idle_thread b) (scheduler_action s) (cur_domain s) (ekheap b) \<and> valid_idle_etcb b proof (prove)
goal (2 subgoals):
 1. \<And>s a b. \<lbrakk>(a, b) \<in> fst (f s); I s; ct_active s; valid_etcbs s; valid_queues s; ct_not_in_q_2 (ready_queues s) resume_cur_thread (cur_thread s); ct_in_cur_domain_2 (cur_thread s) (idle_thread s) resume_cur_thread (cur_domain s) (ekheap s); valid_blocked_2 (ready_queues s) (kheap s) resume_cur_thread (cur_thread s); valid_idle_etcb s; valid_idle s; valid_etcbs b; valid_blocked_2 (ready_queues s) (kheap b) resume_cur_thread (cur_thread s); cur_thread b = cur_thread s; ready_queues b = ready_queues s; switch_in_cur_domain_2 resume_cur_thread (ekheap s) (cur_domain s); scheduler_action b = resume_cur_thread; cur_domain b = cur_domain s; scheduler_action s = resume_cur_thread; st_tcb_at activatable (cur_thread s) s\<rbrakk> \<Longrightarrow> st_tcb_at activatable (cur_thread s) b
 2. \<And>s a b. \<lbrakk>(a, b) \<in> fst (f s); I s; ct_active s; valid_etcbs s; valid_queues s; ct_not_in_q s; ct_in_cur_domain s; valid_blocked s; valid_idle_etcb s; valid_idle s; valid_etcbs b; valid_blocked_2 (ready_queues s) (kheap b) (scheduler_action s) (cur_thread s); cur_thread b = cur_thread s; scheduler_action s = resume_cur_thread \<longrightarrow> st_tcb_at activatable (cur_thread s) s; ready_queues b = ready_queues s; \<forall>t. scheduler_action s = switch_thread t \<longrightarrow> st_tcb_at runnable t s; switch_in_cur_domain s; scheduler_action b = scheduler_action s; cur_domain b = cur_domain s\<rbrakk> \<Longrightarrow> (\<forall>t. scheduler_action s = switch_thread t \<longrightarrow> st_tcb_at runnable t b) \<and> switch_in_cur_domain_2 (scheduler_action s) (ekheap b) (cur_domain s) \<and> ct_in_cur_domain_2 (cur_thread s) (idle_thread b) (scheduler_action s) (cur_domain s) (ekheap b) \<and> valid_idle_etcb b proof (prove)
goal (3 subgoals):
 1. \<And>s a b. \<lbrakk>(a, b) \<in> fst (f s); I s; ct_active s; valid_etcbs s; valid_queues s; ct_not_in_q_2 (ready_queues s) resume_cur_thread (cur_thread s); ct_in_cur_domain_2 (cur_thread s) (idle_thread s) resume_cur_thread (cur_domain s) (ekheap s); valid_blocked_2 (ready_queues s) (kheap s) resume_cur_thread (cur_thread s); valid_idle_etcb s; valid_idle s; valid_etcbs b; valid_blocked_2 (ready_queues s) (kheap b) resume_cur_thread (cur_thread s); cur_thread b = cur_thread s; ready_queues b = ready_queues s; switch_in_cur_domain_2 resume_cur_thread (ekheap s) (cur_domain s); scheduler_action b = resume_cur_thread; cur_domain b = cur_domain s; scheduler_action s = resume_cur_thread; st_tcb_at activatable (cur_thread s) s\<rbrakk> \<Longrightarrow> (I and ct_active and st_tcb_at (active and Not \<circ> inactive and Not \<circ> idle) (cur_thread s)) s
 2. \<And>s a b. \<lbrakk>(a, b) \<in> fst (f s); I s; ct_active s; valid_etcbs s; valid_queues s; ct_not_in_q_2 (ready_queues s) resume_cur_thread (cur_thread s); ct_in_cur_domain_2 (cur_thread s) (idle_thread s) resume_cur_thread (cur_domain s) (ekheap s); valid_blocked_2 (ready_queues s) (kheap s) resume_cur_thread (cur_thread s); valid_idle_etcb s; valid_idle s; valid_etcbs b; valid_blocked_2 (ready_queues s) (kheap b) resume_cur_thread (cur_thread s); cur_thread b = cur_thread s; ready_queues b = ready_queues s; switch_in_cur_domain_2 resume_cur_thread (ekheap s) (cur_domain s); scheduler_action b = resume_cur_thread; cur_domain b = cur_domain s; scheduler_action s = resume_cur_thread; st_tcb_at activatable (cur_thread s) s; st_tcb_at active (cur_thread s) b\<rbrakk> \<Longrightarrow> st_tcb_at activatable (cur_thread s) b
 3. \<And>s a b. \<lbrakk>(a, b) \<in> fst (f s); I s; ct_active s; valid_etcbs s; valid_queues s; ct_not_in_q s; ct_in_cur_domain s; valid_blocked s; valid_idle_etcb s; valid_idle s; valid_etcbs b; valid_blocked_2 (ready_queues s) (kheap b) (scheduler_action s) (cur_thread s); cur_thread b = cur_thread s; scheduler_action s = resume_cur_thread \<longrightarrow> st_tcb_at activatable (cur_thread s) s; ready_queues b = ready_queues s; \<forall>t. scheduler_action s = switch_thread t \<longrightarrow> st_tcb_at runnable t s; switch_in_cur_domain s; scheduler_action b = scheduler_action s; cur_domain b = cur_domain s\<rbrakk> \<Longrightarrow> (\<forall>t. scheduler_action s = switch_thread t \<longrightarrow> st_tcb_at runnable t b) \<and> switch_in_cur_domain_2 (scheduler_action s) (ekheap b) (cur_domain s) \<and> ct_in_cur_domain_2 (cur_thread s) (idle_thread b) (scheduler_action s) (cur_domain s) (ekheap b) \<and> valid_idle_etcb b proof (prove)
goal (3 subgoals):
 1. \<And>s a b. \<lbrakk>(a, b) \<in> fst (f s); I s; st_tcb_at active (cur_thread s) s; valid_etcbs s; valid_queues s; ct_not_in_q_2 (ready_queues s) resume_cur_thread (cur_thread s); ct_in_cur_domain_2 (cur_thread s) (idle_thread s) resume_cur_thread (cur_domain s) (ekheap s); valid_blocked_2 (ready_queues s) (kheap s) resume_cur_thread (cur_thread s); valid_idle_etcb s; valid_idle s; valid_etcbs b; valid_blocked_2 (ready_queues s) (kheap b) resume_cur_thread (cur_thread s); cur_thread b = cur_thread s; ready_queues b = ready_queues s; switch_in_cur_domain_2 resume_cur_thread (ekheap s) (cur_domain s); scheduler_action b = resume_cur_thread; cur_domain b = cur_domain s; scheduler_action s = resume_cur_thread; st_tcb_at activatable (cur_thread s) s\<rbrakk> \<Longrightarrow> st_tcb_at (active and Not \<circ> inactive and Not \<circ> idle) (cur_thread s) s
 2. \<And>s a b. \<lbrakk>(a, b) \<in> fst (f s); I s; ct_active s; valid_etcbs s; valid_queues s; ct_not_in_q_2 (ready_queues s) resume_cur_thread (cur_thread s); ct_in_cur_domain_2 (cur_thread s) (idle_thread s) resume_cur_thread (cur_domain s) (ekheap s); valid_blocked_2 (ready_queues s) (kheap s) resume_cur_thread (cur_thread s); valid_idle_etcb s; valid_idle s; valid_etcbs b; valid_blocked_2 (ready_queues s) (kheap b) resume_cur_thread (cur_thread s); cur_thread b = cur_thread s; ready_queues b = ready_queues s; switch_in_cur_domain_2 resume_cur_thread (ekheap s) (cur_domain s); scheduler_action b = resume_cur_thread; cur_domain b = cur_domain s; scheduler_action s = resume_cur_thread; st_tcb_at activatable (cur_thread s) s; st_tcb_at active (cur_thread s) b\<rbrakk> \<Longrightarrow> st_tcb_at activatable (cur_thread s) b
 3. \<And>s a b. \<lbrakk>(a, b) \<in> fst (f s); I s; ct_active s; valid_etcbs s; valid_queues s; ct_not_in_q s; ct_in_cur_domain s; valid_blocked s; valid_idle_etcb s; valid_idle s; valid_etcbs b; valid_blocked_2 (ready_queues s) (kheap b) (scheduler_action s) (cur_thread s); cur_thread b = cur_thread s; scheduler_action s = resume_cur_thread \<longrightarrow> st_tcb_at activatable (cur_thread s) s; ready_queues b = ready_queues s; \<forall>t. scheduler_action s = switch_thread t \<longrightarrow> st_tcb_at runnable t s; switch_in_cur_domain s; scheduler_action b = scheduler_action s; cur_domain b = cur_domain s\<rbrakk> \<Longrightarrow> (\<forall>t. scheduler_action s = switch_thread t \<longrightarrow> st_tcb_at runnable t b) \<and> switch_in_cur_domain_2 (scheduler_action s) (ekheap b) (cur_domain s) \<and> ct_in_cur_domain_2 (cur_thread s) (idle_thread b) (scheduler_action s) (cur_domain s) (ekheap b) \<and> valid_idle_etcb b proof (prove)
goal (3 subgoals):
 1. \<And>s a b tcb. \<lbrakk>(a, b) \<in> fst (f s); I s; valid_etcbs s; valid_queues s; ct_not_in_q_2 (ready_queues s) resume_cur_thread (cur_thread s); ct_in_cur_domain_2 (cur_thread s) (idle_thread s) resume_cur_thread (cur_domain s) (ekheap s); valid_blocked_2 (ready_queues s) (kheap s) resume_cur_thread (cur_thread s); valid_idle_etcb s; valid_idle s; valid_etcbs b; valid_blocked_2 (ready_queues s) (kheap b) resume_cur_thread (cur_thread s); cur_thread b = cur_thread s; ready_queues b = ready_queues s; switch_in_cur_domain_2 resume_cur_thread (ekheap s) (cur_domain s); scheduler_action b = resume_cur_thread; cur_domain b = cur_domain s; scheduler_action s = resume_cur_thread; st_tcb_at activatable (cur_thread s) s; active (itcb_state tcb)\<rbrakk> \<Longrightarrow> (active and Not \<circ> inactive and Not \<circ> idle) (itcb_state tcb)
 2. \<And>s a b. \<lbrakk>(a, b) \<in> fst (f s); I s; ct_active s; valid_etcbs s; valid_queues s; ct_not_in_q_2 (ready_queues s) resume_cur_thread (cur_thread s); ct_in_cur_domain_2 (cur_thread s) (idle_thread s) resume_cur_thread (cur_domain s) (ekheap s); valid_blocked_2 (ready_queues s) (kheap s) resume_cur_thread (cur_thread s); valid_idle_etcb s; valid_idle s; valid_etcbs b; valid_blocked_2 (ready_queues s) (kheap b) resume_cur_thread (cur_thread s); cur_thread b = cur_thread s; ready_queues b = ready_queues s; switch_in_cur_domain_2 resume_cur_thread (ekheap s) (cur_domain s); scheduler_action b = resume_cur_thread; cur_domain b = cur_domain s; scheduler_action s = resume_cur_thread; st_tcb_at activatable (cur_thread s) s; st_tcb_at active (cur_thread s) b\<rbrakk> \<Longrightarrow> st_tcb_at activatable (cur_thread s) b
 3. \<And>s a b. \<lbrakk>(a, b) \<in> fst (f s); I s; ct_active s; valid_etcbs s; valid_queues s; ct_not_in_q s; ct_in_cur_domain s; valid_blocked s; valid_idle_etcb s; valid_idle s; valid_etcbs b; valid_blocked_2 (ready_queues s) (kheap b) (scheduler_action s) (cur_thread s); cur_thread b = cur_thread s; scheduler_action s = resume_cur_thread \<longrightarrow> st_tcb_at activatable (cur_thread s) s; ready_queues b = ready_queues s; \<forall>t. scheduler_action s = switch_thread t \<longrightarrow> st_tcb_at runnable t s; switch_in_cur_domain s; scheduler_action b = scheduler_action s; cur_domain b = cur_domain s\<rbrakk> \<Longrightarrow> (\<forall>t. scheduler_action s = switch_thread t \<longrightarrow> st_tcb_at runnable t b) \<and> switch_in_cur_domain_2 (scheduler_action s) (ekheap b) (cur_domain s) \<and> ct_in_cur_domain_2 (cur_thread s) (idle_thread b) (scheduler_action s) (cur_domain s) (ekheap b) \<and> valid_idle_etcb b proof (prove)
goal (3 subgoals):
 1. \<And>s a b tcb. \<lbrakk>(a, b) \<in> fst (f s); I s; valid_etcbs s; valid_queues s; ct_not_in_q_2 (ready_queues s) resume_cur_thread (cur_thread s); ct_in_cur_domain_2 (cur_thread s) (idle_thread s) resume_cur_thread (cur_domain s) (ekheap s); valid_blocked_2 (ready_queues s) (kheap s) resume_cur_thread (cur_thread s); valid_idle_etcb s; valid_idle s; valid_etcbs b; valid_blocked_2 (ready_queues s) (kheap b) resume_cur_thread (cur_thread s); cur_thread b = cur_thread s; ready_queues b = ready_queues s; switch_in_cur_domain_2 resume_cur_thread (ekheap s) (cur_domain s); scheduler_action b = resume_cur_thread; cur_domain b = cur_domain s; scheduler_action s = resume_cur_thread; st_tcb_at activatable (cur_thread s) s; active (itcb_state tcb)\<rbrakk> \<Longrightarrow> itcb_state tcb \<noteq> Inactive \<and> itcb_state tcb \<noteq> IdleThreadState
 2. \<And>s a b. \<lbrakk>(a, b) \<in> fst (f s); I s; ct_active s; valid_etcbs s; valid_queues s; ct_not_in_q_2 (ready_queues s) resume_cur_thread (cur_thread s); ct_in_cur_domain_2 (cur_thread s) (idle_thread s) resume_cur_thread (cur_domain s) (ekheap s); valid_blocked_2 (ready_queues s) (kheap s) resume_cur_thread (cur_thread s); valid_idle_etcb s; valid_idle s; valid_etcbs b; valid_blocked_2 (ready_queues s) (kheap b) resume_cur_thread (cur_thread s); cur_thread b = cur_thread s; ready_queues b = ready_queues s; switch_in_cur_domain_2 resume_cur_thread (ekheap s) (cur_domain s); scheduler_action b = resume_cur_thread; cur_domain b = cur_domain s; scheduler_action s = resume_cur_thread; st_tcb_at activatable (cur_thread s) s; st_tcb_at active (cur_thread s) b\<rbrakk> \<Longrightarrow> st_tcb_at activatable (cur_thread s) b
 3. \<And>s a b. \<lbrakk>(a, b) \<in> fst (f s); I s; ct_active s; valid_etcbs s; valid_queues s; ct_not_in_q s; ct_in_cur_domain s; valid_blocked s; valid_idle_etcb s; valid_idle s; valid_etcbs b; valid_blocked_2 (ready_queues s) (kheap b) (scheduler_action s) (cur_thread s); cur_thread b = cur_thread s; scheduler_action s = resume_cur_thread \<longrightarrow> st_tcb_at activatable (cur_thread s) s; ready_queues b = ready_queues s; \<forall>t. scheduler_action s = switch_thread t \<longrightarrow> st_tcb_at runnable t s; switch_in_cur_domain s; scheduler_action b = scheduler_action s; cur_domain b = cur_domain s\<rbrakk> \<Longrightarrow> (\<forall>t. scheduler_action s = switch_thread t \<longrightarrow> st_tcb_at runnable t b) \<and> switch_in_cur_domain_2 (scheduler_action s) (ekheap b) (cur_domain s) \<and> ct_in_cur_domain_2 (cur_thread s) (idle_thread b) (scheduler_action s) (cur_domain s) (ekheap b) \<and> valid_idle_etcb b proof (prove)
goal (2 subgoals):
 1. \<And>s a b. \<lbrakk>(a, b) \<in> fst (f s); I s; ct_active s; valid_etcbs s; valid_queues s; ct_not_in_q_2 (ready_queues s) resume_cur_thread (cur_thread s); ct_in_cur_domain_2 (cur_thread s) (idle_thread s) resume_cur_thread (cur_domain s) (ekheap s); valid_blocked_2 (ready_queues s) (kheap s) resume_cur_thread (cur_thread s); valid_idle_etcb s; valid_idle s; valid_etcbs b; valid_blocked_2 (ready_queues s) (kheap b) resume_cur_thread (cur_thread s); cur_thread b = cur_thread s; ready_queues b = ready_queues s; switch_in_cur_domain_2 resume_cur_thread (ekheap s) (cur_domain s); scheduler_action b = resume_cur_thread; cur_domain b = cur_domain s; scheduler_action s = resume_cur_thread; st_tcb_at activatable (cur_thread s) s; st_tcb_at active (cur_thread s) b\<rbrakk> \<Longrightarrow> st_tcb_at activatable (cur_thread s) b
 2. \<And>s a b. \<lbrakk>(a, b) \<in> fst (f s); I s; ct_active s; valid_etcbs s; valid_queues s; ct_not_in_q s; ct_in_cur_domain s; valid_blocked s; valid_idle_etcb s; valid_idle s; valid_etcbs b; valid_blocked_2 (ready_queues s) (kheap b) (scheduler_action s) (cur_thread s); cur_thread b = cur_thread s; scheduler_action s = resume_cur_thread \<longrightarrow> st_tcb_at activatable (cur_thread s) s; ready_queues b = ready_queues s; \<forall>t. scheduler_action s = switch_thread t \<longrightarrow> st_tcb_at runnable t s; switch_in_cur_domain s; scheduler_action b = scheduler_action s; cur_domain b = cur_domain s\<rbrakk> \<Longrightarrow> (\<forall>t. scheduler_action s = switch_thread t \<longrightarrow> st_tcb_at runnable t b) \<and> switch_in_cur_domain_2 (scheduler_action s) (ekheap b) (cur_domain s) \<and> ct_in_cur_domain_2 (cur_thread s) (idle_thread b) (scheduler_action s) (cur_domain s) (ekheap b) \<and> valid_idle_etcb b proof (prove)
goal (2 subgoals):
 1. \<And>s a b tcb. \<lbrakk>(a, b) \<in> fst (f s); I s; ct_active s; valid_etcbs s; valid_queues s; ct_not_in_q_2 (ready_queues s) resume_cur_thread (cur_thread s); ct_in_cur_domain_2 (cur_thread s) (idle_thread s) resume_cur_thread (cur_domain s) (ekheap s); valid_blocked_2 (ready_queues s) (kheap s) resume_cur_thread (cur_thread s); valid_idle_etcb s; valid_idle s; valid_etcbs b; valid_blocked_2 (ready_queues s) (kheap b) resume_cur_thread (cur_thread s); cur_thread b = cur_thread s; ready_queues b = ready_queues s; switch_in_cur_domain_2 resume_cur_thread (ekheap s) (cur_domain s); scheduler_action b = resume_cur_thread; cur_domain b = cur_domain s; scheduler_action s = resume_cur_thread; st_tcb_at activatable (cur_thread s) s; active (itcb_state tcb)\<rbrakk> \<Longrightarrow> activatable (itcb_state tcb)
 2. \<And>s a b. \<lbrakk>(a, b) \<in> fst (f s); I s; ct_active s; valid_etcbs s; valid_queues s; ct_not_in_q s; ct_in_cur_domain s; valid_blocked s; valid_idle_etcb s; valid_idle s; valid_etcbs b; valid_blocked_2 (ready_queues s) (kheap b) (scheduler_action s) (cur_thread s); cur_thread b = cur_thread s; scheduler_action s = resume_cur_thread \<longrightarrow> st_tcb_at activatable (cur_thread s) s; ready_queues b = ready_queues s; \<forall>t. scheduler_action s = switch_thread t \<longrightarrow> st_tcb_at runnable t s; switch_in_cur_domain s; scheduler_action b = scheduler_action s; cur_domain b = cur_domain s\<rbrakk> \<Longrightarrow> (\<forall>t. scheduler_action s = switch_thread t \<longrightarrow> st_tcb_at runnable t b) \<and> switch_in_cur_domain_2 (scheduler_action s) (ekheap b) (cur_domain s) \<and> ct_in_cur_domain_2 (cur_thread s) (idle_thread b) (scheduler_action s) (cur_domain s) (ekheap b) \<and> valid_idle_etcb b proof (prove)
goal (1 subgoal):
 1. \<And>s a b. \<lbrakk>(a, b) \<in> fst (f s); I s; ct_active s; valid_etcbs s; valid_queues s; ct_not_in_q s; ct_in_cur_domain s; valid_blocked s; valid_idle_etcb s; valid_idle s; valid_etcbs b; valid_blocked_2 (ready_queues s) (kheap b) (scheduler_action s) (cur_thread s); cur_thread b = cur_thread s; scheduler_action s = resume_cur_thread \<longrightarrow> st_tcb_at activatable (cur_thread s) s; ready_queues b = ready_queues s; \<forall>t. scheduler_action s = switch_thread t \<longrightarrow> st_tcb_at runnable t s; switch_in_cur_domain s; scheduler_action b = scheduler_action s; cur_domain b = cur_domain s\<rbrakk> \<Longrightarrow> (\<forall>t. scheduler_action s = switch_thread t \<longrightarrow> st_tcb_at runnable t b) \<and> switch_in_cur_domain_2 (scheduler_action s) (ekheap b) (cur_domain s) \<and> ct_in_cur_domain_2 (cur_thread s) (idle_thread b) (scheduler_action s) (cur_domain s) (ekheap b) \<and> valid_idle_etcb b proof (prove)
goal (2 subgoals):
 1. \<And>s a b. \<lbrakk>(a, b) \<in> fst (f s); I s; ct_active s; valid_etcbs s; valid_queues s; ct_not_in_q s; ct_in_cur_domain s; valid_blocked s; valid_idle_etcb s; valid_idle s; valid_etcbs b; valid_blocked_2 (ready_queues s) (kheap b) (scheduler_action s) (cur_thread s); cur_thread b = cur_thread s; scheduler_action s = resume_cur_thread \<longrightarrow> st_tcb_at activatable (cur_thread s) s; ready_queues b = ready_queues s; \<forall>t. scheduler_action s = switch_thread t \<longrightarrow> st_tcb_at runnable t s; switch_in_cur_domain s; scheduler_action b = scheduler_action s; cur_domain b = cur_domain s\<rbrakk> \<Longrightarrow> \<forall>t. scheduler_action s = switch_thread t \<longrightarrow> st_tcb_at runnable t b
 2. \<And>s a b. \<lbrakk>(a, b) \<in> fst (f s); I s; ct_active s; valid_etcbs s; valid_queues s; ct_not_in_q s; ct_in_cur_domain s; valid_blocked s; valid_idle_etcb s; valid_idle s; valid_etcbs b; valid_blocked_2 (ready_queues s) (kheap b) (scheduler_action s) (cur_thread s); cur_thread b = cur_thread s; scheduler_action s = resume_cur_thread \<longrightarrow> st_tcb_at activatable (cur_thread s) s; ready_queues b = ready_queues s; \<forall>t. scheduler_action s = switch_thread t \<longrightarrow> st_tcb_at runnable t s; switch_in_cur_domain s; scheduler_action b = scheduler_action s; cur_domain b = cur_domain s\<rbrakk> \<Longrightarrow> switch_in_cur_domain_2 (scheduler_action s) (ekheap b) (cur_domain s) \<and> ct_in_cur_domain_2 (cur_thread s) (idle_thread b) (scheduler_action s) (cur_domain s) (ekheap b) \<and> valid_idle_etcb b proof (prove)
goal (2 subgoals):
 1. \<And>s a b t. \<lbrakk>(a, b) \<in> fst (f s); I s; ct_active s; valid_etcbs s; valid_queues s; ct_not_in_q_2 (ready_queues s) (switch_thread t) (cur_thread s); ct_in_cur_domain_2 (cur_thread s) (idle_thread s) (switch_thread t) (cur_domain s) (ekheap s); valid_blocked_2 (ready_queues s) (kheap s) (switch_thread t) (cur_thread s); valid_idle_etcb s; valid_idle s; valid_etcbs b; valid_blocked_2 (ready_queues s) (kheap b) (switch_thread t) (cur_thread s); cur_thread b = cur_thread s; ready_queues b = ready_queues s; st_tcb_at runnable t s; switch_in_cur_domain_2 (switch_thread t) (ekheap s) (cur_domain s); scheduler_action b = switch_thread t; cur_domain b = cur_domain s; scheduler_action s = switch_thread t\<rbrakk> \<Longrightarrow> st_tcb_at runnable t b
 2. \<And>s a b. \<lbrakk>(a, b) \<in> fst (f s); I s; ct_active s; valid_etcbs s; valid_queues s; ct_not_in_q s; ct_in_cur_domain s; valid_blocked s; valid_idle_etcb s; valid_idle s; valid_etcbs b; valid_blocked_2 (ready_queues s) (kheap b) (scheduler_action s) (cur_thread s); cur_thread b = cur_thread s; scheduler_action s = resume_cur_thread \<longrightarrow> st_tcb_at activatable (cur_thread s) s; ready_queues b = ready_queues s; \<forall>t. scheduler_action s = switch_thread t \<longrightarrow> st_tcb_at runnable t s; switch_in_cur_domain s; scheduler_action b = scheduler_action s; cur_domain b = cur_domain s\<rbrakk> \<Longrightarrow> switch_in_cur_domain_2 (scheduler_action s) (ekheap b) (cur_domain s) \<and> ct_in_cur_domain_2 (cur_thread s) (idle_thread b) (scheduler_action s) (cur_domain s) (ekheap b) \<and> valid_idle_etcb b proof (prove)
goal (2 subgoals):
 1. \<And>s a b t. \<lbrakk>(a, b) \<in> fst (f s); I s; ct_active s; valid_etcbs s; valid_queues s; ct_not_in_q_2 (ready_queues s) (switch_thread t) (cur_thread s); ct_in_cur_domain_2 (cur_thread s) (idle_thread s) (switch_thread t) (cur_domain s) (ekheap s); valid_blocked_2 (ready_queues s) (kheap s) (switch_thread t) (cur_thread s); valid_idle_etcb s; valid_idle s; valid_etcbs b; valid_blocked_2 (ready_queues s) (kheap b) (switch_thread t) (cur_thread s); cur_thread b = cur_thread s; ready_queues b = ready_queues s; st_tcb_at runnable t s; switch_in_cur_domain_2 (switch_thread t) (ekheap s) (cur_domain s); scheduler_action b = switch_thread t; cur_domain b = cur_domain s; scheduler_action s = switch_thread t\<rbrakk> \<Longrightarrow> (I and ct_active and st_tcb_at (runnable and Not \<circ> inactive and Not \<circ> idle) t) s
 2. \<And>s a b. \<lbrakk>(a, b) \<in> fst (f s); I s; ct_active s; valid_etcbs s; valid_queues s; ct_not_in_q s; ct_in_cur_domain s; valid_blocked s; valid_idle_etcb s; valid_idle s; valid_etcbs b; valid_blocked_2 (ready_queues s) (kheap b) (scheduler_action s) (cur_thread s); cur_thread b = cur_thread s; scheduler_action s = resume_cur_thread \<longrightarrow> st_tcb_at activatable (cur_thread s) s; ready_queues b = ready_queues s; \<forall>t. scheduler_action s = switch_thread t \<longrightarrow> st_tcb_at runnable t s; switch_in_cur_domain s; scheduler_action b = scheduler_action s; cur_domain b = cur_domain s\<rbrakk> \<Longrightarrow> switch_in_cur_domain_2 (scheduler_action s) (ekheap b) (cur_domain s) \<and> ct_in_cur_domain_2 (cur_thread s) (idle_thread b) (scheduler_action s) (cur_domain s) (ekheap b) \<and> valid_idle_etcb b proof (prove)
goal (2 subgoals):
 1. \<And>s a b t. \<lbrakk>(a, b) \<in> fst (f s); I s; ct_active s; valid_etcbs s; valid_queues s; ct_not_in_q_2 (ready_queues s) (switch_thread t) (cur_thread s); ct_in_cur_domain_2 (cur_thread s) (idle_thread s) (switch_thread t) (cur_domain s) (ekheap s); valid_blocked_2 (ready_queues s) (kheap s) (switch_thread t) (cur_thread s); valid_idle_etcb s; valid_idle s; valid_etcbs b; valid_blocked_2 (ready_queues s) (kheap b) (switch_thread t) (cur_thread s); cur_thread b = cur_thread s; ready_queues b = ready_queues s; st_tcb_at runnable t s; switch_in_cur_domain_2 (switch_thread t) (ekheap s) (cur_domain s); scheduler_action b = switch_thread t; cur_domain b = cur_domain s; scheduler_action s = switch_thread t\<rbrakk> \<Longrightarrow> st_tcb_at (runnable and Not \<circ> inactive and Not \<circ> idle) t s
 2. \<And>s a b. \<lbrakk>(a, b) \<in> fst (f s); I s; ct_active s; valid_etcbs s; valid_queues s; ct_not_in_q s; ct_in_cur_domain s; valid_blocked s; valid_idle_etcb s; valid_idle s; valid_etcbs b; valid_blocked_2 (ready_queues s) (kheap b) (scheduler_action s) (cur_thread s); cur_thread b = cur_thread s; scheduler_action s = resume_cur_thread \<longrightarrow> st_tcb_at activatable (cur_thread s) s; ready_queues b = ready_queues s; \<forall>t. scheduler_action s = switch_thread t \<longrightarrow> st_tcb_at runnable t s; switch_in_cur_domain s; scheduler_action b = scheduler_action s; cur_domain b = cur_domain s\<rbrakk> \<Longrightarrow> switch_in_cur_domain_2 (scheduler_action s) (ekheap b) (cur_domain s) \<and> ct_in_cur_domain_2 (cur_thread s) (idle_thread b) (scheduler_action s) (cur_domain s) (ekheap b) \<and> valid_idle_etcb b proof (prove)
goal (2 subgoals):
 1. \<And>s a b t tcb. \<lbrakk>(a, b) \<in> fst (f s); I s; ct_active s; valid_etcbs s; valid_queues s; ct_not_in_q_2 (ready_queues s) (switch_thread t) (cur_thread s); ct_in_cur_domain_2 (cur_thread s) (idle_thread s) (switch_thread t) (cur_domain s) (ekheap s); valid_blocked_2 (ready_queues s) (kheap s) (switch_thread t) (cur_thread s); valid_idle_etcb s; valid_idle s; valid_etcbs b; valid_blocked_2 (ready_queues s) (kheap b) (switch_thread t) (cur_thread s); cur_thread b = cur_thread s; ready_queues b = ready_queues s; switch_in_cur_domain_2 (switch_thread t) (ekheap s) (cur_domain s); scheduler_action b = switch_thread t; cur_domain b = cur_domain s; scheduler_action s = switch_thread t; runnable (itcb_state tcb)\<rbrakk> \<Longrightarrow> (runnable and Not \<circ> inactive and Not \<circ> idle) (itcb_state tcb)
 2. \<And>s a b. \<lbrakk>(a, b) \<in> fst (f s); I s; ct_active s; valid_etcbs s; valid_queues s; ct_not_in_q s; ct_in_cur_domain s; valid_blocked s; valid_idle_etcb s; valid_idle s; valid_etcbs b; valid_blocked_2 (ready_queues s) (kheap b) (scheduler_action s) (cur_thread s); cur_thread b = cur_thread s; scheduler_action s = resume_cur_thread \<longrightarrow> st_tcb_at activatable (cur_thread s) s; ready_queues b = ready_queues s; \<forall>t. scheduler_action s = switch_thread t \<longrightarrow> st_tcb_at runnable t s; switch_in_cur_domain s; scheduler_action b = scheduler_action s; cur_domain b = cur_domain s\<rbrakk> \<Longrightarrow> switch_in_cur_domain_2 (scheduler_action s) (ekheap b) (cur_domain s) \<and> ct_in_cur_domain_2 (cur_thread s) (idle_thread b) (scheduler_action s) (cur_domain s) (ekheap b) \<and> valid_idle_etcb b proof (prove)
goal (2 subgoals):
 1. \<And>s a b t tcb. \<lbrakk>(a, b) \<in> fst (f s); I s; ct_active s; valid_etcbs s; valid_queues s; ct_not_in_q_2 (ready_queues s) (switch_thread t) (cur_thread s); ct_in_cur_domain_2 (cur_thread s) (idle_thread s) (switch_thread t) (cur_domain s) (ekheap s); valid_blocked_2 (ready_queues s) (kheap s) (switch_thread t) (cur_thread s); valid_idle_etcb s; valid_idle s; valid_etcbs b; valid_blocked_2 (ready_queues s) (kheap b) (switch_thread t) (cur_thread s); cur_thread b = cur_thread s; ready_queues b = ready_queues s; switch_in_cur_domain_2 (switch_thread t) (ekheap s) (cur_domain s); scheduler_action b = switch_thread t; cur_domain b = cur_domain s; scheduler_action s = switch_thread t; runnable (itcb_state tcb)\<rbrakk> \<Longrightarrow> itcb_state tcb \<noteq> Inactive \<and> itcb_state tcb \<noteq> IdleThreadState
 2. \<And>s a b. \<lbrakk>(a, b) \<in> fst (f s); I s; ct_active s; valid_etcbs s; valid_queues s; ct_not_in_q s; ct_in_cur_domain s; valid_blocked s; valid_idle_etcb s; valid_idle s; valid_etcbs b; valid_blocked_2 (ready_queues s) (kheap b) (scheduler_action s) (cur_thread s); cur_thread b = cur_thread s; scheduler_action s = resume_cur_thread \<longrightarrow> st_tcb_at activatable (cur_thread s) s; ready_queues b = ready_queues s; \<forall>t. scheduler_action s = switch_thread t \<longrightarrow> st_tcb_at runnable t s; switch_in_cur_domain s; scheduler_action b = scheduler_action s; cur_domain b = cur_domain s\<rbrakk> \<Longrightarrow> switch_in_cur_domain_2 (scheduler_action s) (ekheap b) (cur_domain s) \<and> ct_in_cur_domain_2 (cur_thread s) (idle_thread b) (scheduler_action s) (cur_domain s) (ekheap b) \<and> valid_idle_etcb b proof (prove)
goal (1 subgoal):
 1. \<And>s a b. \<lbrakk>(a, b) \<in> fst (f s); I s; ct_active s; valid_etcbs s; valid_queues s; ct_not_in_q s; ct_in_cur_domain s; valid_blocked s; valid_idle_etcb s; valid_idle s; valid_etcbs b; valid_blocked_2 (ready_queues s) (kheap b) (scheduler_action s) (cur_thread s); cur_thread b = cur_thread s; scheduler_action s = resume_cur_thread \<longrightarrow> st_tcb_at activatable (cur_thread s) s; ready_queues b = ready_queues s; \<forall>t. scheduler_action s = switch_thread t \<longrightarrow> st_tcb_at runnable t s; switch_in_cur_domain s; scheduler_action b = scheduler_action s; cur_domain b = cur_domain s\<rbrakk> \<Longrightarrow> switch_in_cur_domain_2 (scheduler_action s) (ekheap b) (cur_domain s) \<and> ct_in_cur_domain_2 (cur_thread s) (idle_thread b) (scheduler_action s) (cur_domain s) (ekheap b) \<and> valid_idle_etcb b proof (prove)
goal (2 subgoals):
 1. \<And>s a b. \<lbrakk>(a, b) \<in> fst (f s); I s; ct_active s; valid_etcbs s; valid_queues s; ct_not_in_q s; ct_in_cur_domain s; valid_blocked s; valid_idle_etcb s; valid_idle s; valid_etcbs b; valid_blocked_2 (ready_queues s) (kheap b) (scheduler_action s) (cur_thread s); cur_thread b = cur_thread s; scheduler_action s = resume_cur_thread \<longrightarrow> st_tcb_at activatable (cur_thread s) s; ready_queues b = ready_queues s; \<forall>t. scheduler_action s = switch_thread t \<longrightarrow> st_tcb_at runnable t s; switch_in_cur_domain s; scheduler_action b = scheduler_action s; cur_domain b = cur_domain s\<rbrakk> \<Longrightarrow> switch_in_cur_domain_2 (scheduler_action s) (ekheap b) (cur_domain s)
 2. \<And>s a b. \<lbrakk>(a, b) \<in> fst (f s); I s; ct_active s; valid_etcbs s; valid_queues s; ct_not_in_q s; ct_in_cur_domain s; valid_blocked s; valid_idle_etcb s; valid_idle s; valid_etcbs b; valid_blocked_2 (ready_queues s) (kheap b) (scheduler_action s) (cur_thread s); cur_thread b = cur_thread s; scheduler_action s = resume_cur_thread \<longrightarrow> st_tcb_at activatable (cur_thread s) s; ready_queues b = ready_queues s; \<forall>t. scheduler_action s = switch_thread t \<longrightarrow> st_tcb_at runnable t s; switch_in_cur_domain s; scheduler_action b = scheduler_action s; cur_domain b = cur_domain s\<rbrakk> \<Longrightarrow> ct_in_cur_domain_2 (cur_thread s) (idle_thread b) (scheduler_action s) (cur_domain s) (ekheap b) \<and> valid_idle_etcb b proof (prove)
goal (2 subgoals):
 1. \<And>s a b t. \<lbrakk>(a, b) \<in> fst (f s); I s; ct_active s; valid_etcbs s; valid_queues s; ct_not_in_q_2 (ready_queues s) (switch_thread t) (cur_thread s); ct_in_cur_domain_2 (cur_thread s) (idle_thread s) (switch_thread t) (cur_domain s) (ekheap s); valid_blocked_2 (ready_queues s) (kheap s) (switch_thread t) (cur_thread s); valid_idle_etcb s; valid_idle s; valid_etcbs b; valid_blocked_2 (ready_queues s) (kheap b) (switch_thread t) (cur_thread s); cur_thread b = cur_thread s; ready_queues b = ready_queues s; st_tcb_at runnable t s; etcb_at (\<lambda>t. tcb_domain t = cur_domain s) t s; scheduler_action b = switch_thread t; cur_domain b = cur_domain s; scheduler_action s = switch_thread t\<rbrakk> \<Longrightarrow> etcb_at (\<lambda>t. tcb_domain t = cur_domain s) t b
 2. \<And>s a b. \<lbrakk>(a, b) \<in> fst (f s); I s; ct_active s; valid_etcbs s; valid_queues s; ct_not_in_q s; ct_in_cur_domain s; valid_blocked s; valid_idle_etcb s; valid_idle s; valid_etcbs b; valid_blocked_2 (ready_queues s) (kheap b) (scheduler_action s) (cur_thread s); cur_thread b = cur_thread s; scheduler_action s = resume_cur_thread \<longrightarrow> st_tcb_at activatable (cur_thread s) s; ready_queues b = ready_queues s; \<forall>t. scheduler_action s = switch_thread t \<longrightarrow> st_tcb_at runnable t s; switch_in_cur_domain s; scheduler_action b = scheduler_action s; cur_domain b = cur_domain s\<rbrakk> \<Longrightarrow> ct_in_cur_domain_2 (cur_thread s) (idle_thread b) (scheduler_action s) (cur_domain s) (ekheap b) \<and> valid_idle_etcb b proof (prove)
goal (3 subgoals):
 1. \<And>s a b t. \<lbrakk>(a, b) \<in> fst (f s); I s; ct_active s; valid_etcbs s; valid_queues s; ct_not_in_q_2 (ready_queues s) (switch_thread t) (cur_thread s); ct_in_cur_domain_2 (cur_thread s) (idle_thread s) (switch_thread t) (cur_domain s) (ekheap s); valid_blocked_2 (ready_queues s) (kheap s) (switch_thread t) (cur_thread s); valid_idle_etcb s; valid_idle s; valid_etcbs b; valid_blocked_2 (ready_queues s) (kheap b) (switch_thread t) (cur_thread s); cur_thread b = cur_thread s; ready_queues b = ready_queues s; st_tcb_at runnable t s; etcb_at (\<lambda>t. tcb_domain t = cur_domain s) t s; scheduler_action b = switch_thread t; cur_domain b = cur_domain s; scheduler_action s = switch_thread t\<rbrakk> \<Longrightarrow> (etcb_at (\<lambda>t. tcb_domain t = cur_domain s) t and valid_etcbs) s
 2. \<And>s a b t. \<lbrakk>(a, b) \<in> fst (f s); I s; ct_active s; valid_etcbs s; valid_queues s; ct_not_in_q_2 (ready_queues s) (switch_thread t) (cur_thread s); ct_in_cur_domain_2 (cur_thread s) (idle_thread s) (switch_thread t) (cur_domain s) (ekheap s); valid_blocked_2 (ready_queues s) (kheap s) (switch_thread t) (cur_thread s); valid_idle_etcb s; valid_idle s; valid_etcbs b; valid_blocked_2 (ready_queues s) (kheap b) (switch_thread t) (cur_thread s); cur_thread b = cur_thread s; ready_queues b = ready_queues s; st_tcb_at runnable t s; etcb_at (\<lambda>t. tcb_domain t = cur_domain s) t s; scheduler_action b = switch_thread t; cur_domain b = cur_domain s; scheduler_action s = switch_thread t\<rbrakk> \<Longrightarrow> st_tcb_at (Not \<circ> inactive) t b
 3. \<And>s a b. \<lbrakk>(a, b) \<in> fst (f s); I s; ct_active s; valid_etcbs s; valid_queues s; ct_not_in_q s; ct_in_cur_domain s; valid_blocked s; valid_idle_etcb s; valid_idle s; valid_etcbs b; valid_blocked_2 (ready_queues s) (kheap b) (scheduler_action s) (cur_thread s); cur_thread b = cur_thread s; scheduler_action s = resume_cur_thread \<longrightarrow> st_tcb_at activatable (cur_thread s) s; ready_queues b = ready_queues s; \<forall>t. scheduler_action s = switch_thread t \<longrightarrow> st_tcb_at runnable t s; switch_in_cur_domain s; scheduler_action b = scheduler_action s; cur_domain b = cur_domain s\<rbrakk> \<Longrightarrow> ct_in_cur_domain_2 (cur_thread s) (idle_thread b) (scheduler_action s) (cur_domain s) (ekheap b) \<and> valid_idle_etcb b proof (prove)
goal (2 subgoals):
 1. \<And>s a b t. \<lbrakk>(a, b) \<in> fst (f s); I s; ct_active s; valid_etcbs s; valid_queues s; ct_not_in_q_2 (ready_queues s) (switch_thread t) (cur_thread s); ct_in_cur_domain_2 (cur_thread s) (idle_thread s) (switch_thread t) (cur_domain s) (ekheap s); valid_blocked_2 (ready_queues s) (kheap s) (switch_thread t) (cur_thread s); valid_idle_etcb s; valid_idle s; valid_etcbs b; valid_blocked_2 (ready_queues s) (kheap b) (switch_thread t) (cur_thread s); cur_thread b = cur_thread s; ready_queues b = ready_queues s; st_tcb_at runnable t s; etcb_at (\<lambda>t. tcb_domain t = cur_domain s) t s; scheduler_action b = switch_thread t; cur_domain b = cur_domain s; scheduler_action s = switch_thread t\<rbrakk> \<Longrightarrow> st_tcb_at (Not \<circ> inactive) t b
 2. \<And>s a b. \<lbrakk>(a, b) \<in> fst (f s); I s; ct_active s; valid_etcbs s; valid_queues s; ct_not_in_q s; ct_in_cur_domain s; valid_blocked s; valid_idle_etcb s; valid_idle s; valid_etcbs b; valid_blocked_2 (ready_queues s) (kheap b) (scheduler_action s) (cur_thread s); cur_thread b = cur_thread s; scheduler_action s = resume_cur_thread \<longrightarrow> st_tcb_at activatable (cur_thread s) s; ready_queues b = ready_queues s; \<forall>t. scheduler_action s = switch_thread t \<longrightarrow> st_tcb_at runnable t s; switch_in_cur_domain s; scheduler_action b = scheduler_action s; cur_domain b = cur_domain s\<rbrakk> \<Longrightarrow> ct_in_cur_domain_2 (cur_thread s) (idle_thread b) (scheduler_action s) (cur_domain s) (ekheap b) \<and> valid_idle_etcb b proof (prove)
goal (2 subgoals):
 1. \<And>s a b t. \<lbrakk>(a, b) \<in> fst (f s); I s; ct_active s; valid_etcbs s; valid_queues s; ct_not_in_q_2 (ready_queues s) (switch_thread t) (cur_thread s); ct_in_cur_domain_2 (cur_thread s) (idle_thread s) (switch_thread t) (cur_domain s) (ekheap s); valid_blocked_2 (ready_queues s) (kheap s) (switch_thread t) (cur_thread s); valid_idle_etcb s; valid_idle s; valid_etcbs b; valid_blocked_2 (ready_queues s) (kheap b) (switch_thread t) (cur_thread s); cur_thread b = cur_thread s; ready_queues b = ready_queues s; st_tcb_at runnable t s; etcb_at (\<lambda>t. tcb_domain t = cur_domain s) t s; scheduler_action b = switch_thread t; cur_domain b = cur_domain s; scheduler_action s = switch_thread t\<rbrakk> \<Longrightarrow> (I and ct_active and st_tcb_at (Not \<circ> inactive and Not \<circ> inactive and Not \<circ> idle) t) s
 2. \<And>s a b. \<lbrakk>(a, b) \<in> fst (f s); I s; ct_active s; valid_etcbs s; valid_queues s; ct_not_in_q s; ct_in_cur_domain s; valid_blocked s; valid_idle_etcb s; valid_idle s; valid_etcbs b; valid_blocked_2 (ready_queues s) (kheap b) (scheduler_action s) (cur_thread s); cur_thread b = cur_thread s; scheduler_action s = resume_cur_thread \<longrightarrow> st_tcb_at activatable (cur_thread s) s; ready_queues b = ready_queues s; \<forall>t. scheduler_action s = switch_thread t \<longrightarrow> st_tcb_at runnable t s; switch_in_cur_domain s; scheduler_action b = scheduler_action s; cur_domain b = cur_domain s\<rbrakk> \<Longrightarrow> ct_in_cur_domain_2 (cur_thread s) (idle_thread b) (scheduler_action s) (cur_domain s) (ekheap b) \<and> valid_idle_etcb b proof (prove)
goal (2 subgoals):
 1. \<And>s a b t. \<lbrakk>(a, b) \<in> fst (f s); I s; ct_active s; valid_etcbs s; valid_queues s; ct_not_in_q_2 (ready_queues s) (switch_thread t) (cur_thread s); ct_in_cur_domain_2 (cur_thread s) (idle_thread s) (switch_thread t) (cur_domain s) (ekheap s); valid_blocked_2 (ready_queues s) (kheap s) (switch_thread t) (cur_thread s); valid_idle_etcb s; valid_idle s; valid_etcbs b; valid_blocked_2 (ready_queues s) (kheap b) (switch_thread t) (cur_thread s); cur_thread b = cur_thread s; ready_queues b = ready_queues s; st_tcb_at runnable t s; etcb_at (\<lambda>t. tcb_domain t = cur_domain s) t s; scheduler_action b = switch_thread t; cur_domain b = cur_domain s; scheduler_action s = switch_thread t\<rbrakk> \<Longrightarrow> st_tcb_at (Not \<circ> inactive and Not \<circ> idle) t s
 2. \<And>s a b. \<lbrakk>(a, b) \<in> fst (f s); I s; ct_active s; valid_etcbs s; valid_queues s; ct_not_in_q s; ct_in_cur_domain s; valid_blocked s; valid_idle_etcb s; valid_idle s; valid_etcbs b; valid_blocked_2 (ready_queues s) (kheap b) (scheduler_action s) (cur_thread s); cur_thread b = cur_thread s; scheduler_action s = resume_cur_thread \<longrightarrow> st_tcb_at activatable (cur_thread s) s; ready_queues b = ready_queues s; \<forall>t. scheduler_action s = switch_thread t \<longrightarrow> st_tcb_at runnable t s; switch_in_cur_domain s; scheduler_action b = scheduler_action s; cur_domain b = cur_domain s\<rbrakk> \<Longrightarrow> ct_in_cur_domain_2 (cur_thread s) (idle_thread b) (scheduler_action s) (cur_domain s) (ekheap b) \<and> valid_idle_etcb b proof (prove)
goal (2 subgoals):
 1. \<And>s a b t st. \<lbrakk>(a, b) \<in> fst (f s); I s; ct_active s; valid_etcbs s; valid_queues s; ct_not_in_q_2 (ready_queues s) (switch_thread t) (cur_thread s); ct_in_cur_domain_2 (cur_thread s) (idle_thread s) (switch_thread t) (cur_domain s) (ekheap s); valid_blocked_2 (ready_queues s) (kheap s) (switch_thread t) (cur_thread s); valid_idle_etcb s; valid_idle s; valid_etcbs b; valid_blocked_2 (ready_queues s) (kheap b) (switch_thread t) (cur_thread s); cur_thread b = cur_thread s; ready_queues b = ready_queues s; etcb_at (\<lambda>t. tcb_domain t = cur_domain s) t s; scheduler_action b = switch_thread t; cur_domain b = cur_domain s; scheduler_action s = switch_thread t; runnable st\<rbrakk> \<Longrightarrow> (Not \<circ> inactive and Not \<circ> idle) st
 2. \<And>s a b. \<lbrakk>(a, b) \<in> fst (f s); I s; ct_active s; valid_etcbs s; valid_queues s; ct_not_in_q s; ct_in_cur_domain s; valid_blocked s; valid_idle_etcb s; valid_idle s; valid_etcbs b; valid_blocked_2 (ready_queues s) (kheap b) (scheduler_action s) (cur_thread s); cur_thread b = cur_thread s; scheduler_action s = resume_cur_thread \<longrightarrow> st_tcb_at activatable (cur_thread s) s; ready_queues b = ready_queues s; \<forall>t. scheduler_action s = switch_thread t \<longrightarrow> st_tcb_at runnable t s; switch_in_cur_domain s; scheduler_action b = scheduler_action s; cur_domain b = cur_domain s\<rbrakk> \<Longrightarrow> ct_in_cur_domain_2 (cur_thread s) (idle_thread b) (scheduler_action s) (cur_domain s) (ekheap b) \<and> valid_idle_etcb b proof (prove)
goal (1 subgoal):
 1. \<And>s a b. \<lbrakk>(a, b) \<in> fst (f s); I s; ct_active s; valid_etcbs s; valid_queues s; ct_not_in_q s; ct_in_cur_domain s; valid_blocked s; valid_idle_etcb s; valid_idle s; valid_etcbs b; valid_blocked_2 (ready_queues s) (kheap b) (scheduler_action s) (cur_thread s); cur_thread b = cur_thread s; scheduler_action s = resume_cur_thread \<longrightarrow> st_tcb_at activatable (cur_thread s) s; ready_queues b = ready_queues s; \<forall>t. scheduler_action s = switch_thread t \<longrightarrow> st_tcb_at runnable t s; switch_in_cur_domain s; scheduler_action b = scheduler_action s; cur_domain b = cur_domain s\<rbrakk> \<Longrightarrow> ct_in_cur_domain_2 (cur_thread s) (idle_thread b) (scheduler_action s) (cur_domain s) (ekheap b) \<and> valid_idle_etcb b proof (prove)
goal (1 subgoal):
 1. \<And>s a b. \<lbrakk>(a, b) \<in> fst (f s); I s; ct_active s; valid_etcbs s; valid_queues s; ct_not_in_q s; scheduler_action s = resume_cur_thread \<longrightarrow> cur_thread s = idle_thread s \<or> etcb_at (\<lambda>t. tcb_domain t = cur_domain s) (cur_thread s) s; valid_blocked s; valid_idle_etcb s; valid_idle s; valid_etcbs b; valid_blocked_2 (ready_queues s) (kheap b) (scheduler_action s) (cur_thread s); cur_thread b = cur_thread s; scheduler_action s = resume_cur_thread \<longrightarrow> st_tcb_at activatable (cur_thread s) s; ready_queues b = ready_queues s; \<forall>t. scheduler_action s = switch_thread t \<longrightarrow> st_tcb_at runnable t s; switch_in_cur_domain s; scheduler_action b = scheduler_action s; cur_domain b = cur_domain s\<rbrakk> \<Longrightarrow> (scheduler_action s = resume_cur_thread \<longrightarrow> cur_thread s = idle_thread b \<or> etcb_at (\<lambda>t. tcb_domain t = cur_domain s) (cur_thread s) b) \<and> valid_idle_etcb b proof (prove)
goal (1 subgoal):
 1. \<And>s a b. \<lbrakk>(a, b) \<in> fst (f s); I s; ct_active s; valid_etcbs s; valid_queues s; ct_not_in_q s; scheduler_action s = resume_cur_thread \<longrightarrow> cur_thread s = idle_thread s \<or> etcb_at (\<lambda>t. tcb_domain t = cur_domain s) (cur_thread s) s; valid_blocked s; valid_idle_etcb s; valid_idle s; valid_etcbs b; valid_blocked_2 (ready_queues s) (kheap b) (scheduler_action s) (cur_thread s); cur_thread b = cur_thread s; scheduler_action s = resume_cur_thread \<longrightarrow> st_tcb_at activatable (cur_thread s) s; ready_queues b = ready_queues s; \<forall>t. scheduler_action s = switch_thread t \<longrightarrow> st_tcb_at runnable t s; switch_in_cur_domain s; scheduler_action b = scheduler_action s; cur_domain b = cur_domain s; idle_thread b = idle_thread s\<rbrakk> \<Longrightarrow> (scheduler_action s = resume_cur_thread \<longrightarrow> cur_thread s = idle_thread b \<or> etcb_at (\<lambda>t. tcb_domain t = cur_domain s) (cur_thread s) b) \<and> valid_idle_etcb b proof (prove)
goal (2 subgoals):
 1. \<And>s a b. \<lbrakk>(a, b) \<in> fst (f s); I s; ct_active s; valid_etcbs s; valid_queues s; ct_not_in_q s; scheduler_action s = resume_cur_thread \<longrightarrow> cur_thread s = idle_thread s \<or> etcb_at (\<lambda>t. tcb_domain t = cur_domain s) (cur_thread s) s; valid_blocked s; valid_idle_etcb s; valid_idle s; valid_etcbs b; valid_blocked_2 (ready_queues s) (kheap b) (scheduler_action s) (cur_thread s); cur_thread b = cur_thread s; scheduler_action s = resume_cur_thread \<longrightarrow> st_tcb_at activatable (cur_thread s) s; ready_queues b = ready_queues s; \<forall>t. scheduler_action s = switch_thread t \<longrightarrow> st_tcb_at runnable t s; switch_in_cur_domain s; scheduler_action b = scheduler_action s; cur_domain b = cur_domain s; idle_thread b = idle_thread s\<rbrakk> \<Longrightarrow> scheduler_action s = resume_cur_thread \<longrightarrow> cur_thread s = idle_thread b \<or> etcb_at (\<lambda>t. tcb_domain t = cur_domain s) (cur_thread s) b
 2. \<And>s a b. \<lbrakk>(a, b) \<in> fst (f s); I s; ct_active s; valid_etcbs s; valid_queues s; ct_not_in_q s; scheduler_action s = resume_cur_thread \<longrightarrow> cur_thread s = idle_thread s \<or> etcb_at (\<lambda>t. tcb_domain t = cur_domain s) (cur_thread s) s; valid_blocked s; valid_idle_etcb s; valid_idle s; valid_etcbs b; valid_blocked_2 (ready_queues s) (kheap b) (scheduler_action s) (cur_thread s); cur_thread b = cur_thread s; scheduler_action s = resume_cur_thread \<longrightarrow> st_tcb_at activatable (cur_thread s) s; ready_queues b = ready_queues s; \<forall>t. scheduler_action s = switch_thread t \<longrightarrow> st_tcb_at runnable t s; switch_in_cur_domain s; scheduler_action b = scheduler_action s; cur_domain b = cur_domain s; idle_thread b = idle_thread s\<rbrakk> \<Longrightarrow> valid_idle_etcb b proof (prove)
goal (2 subgoals):
 1. \<And>s a b. \<lbrakk>(a, b) \<in> fst (f s); I s; ct_active s; valid_etcbs s; valid_queues s; ct_not_in_q s; scheduler_action s = resume_cur_thread \<longrightarrow> cur_thread s = idle_thread s \<or> etcb_at (\<lambda>t. tcb_domain t = cur_domain s) (cur_thread s) s; valid_blocked s; valid_idle_etcb s; valid_idle s; valid_etcbs b; valid_blocked_2 (ready_queues s) (kheap b) (scheduler_action s) (cur_thread s); cur_thread b = cur_thread s; scheduler_action s = resume_cur_thread \<longrightarrow> st_tcb_at activatable (cur_thread s) s; ready_queues b = ready_queues s; \<forall>t. scheduler_action s = switch_thread t \<longrightarrow> st_tcb_at runnable t s; switch_in_cur_domain s; scheduler_action b = scheduler_action s; cur_domain b = cur_domain s; idle_thread b = idle_thread s; scheduler_action s = resume_cur_thread\<rbrakk> \<Longrightarrow> cur_thread s = idle_thread b \<or> etcb_at (\<lambda>t. tcb_domain t = cur_domain s) (cur_thread s) b
 2. \<And>s a b. \<lbrakk>(a, b) \<in> fst (f s); I s; ct_active s; valid_etcbs s; valid_queues s; ct_not_in_q s; scheduler_action s = resume_cur_thread \<longrightarrow> cur_thread s = idle_thread s \<or> etcb_at (\<lambda>t. tcb_domain t = cur_domain s) (cur_thread s) s; valid_blocked s; valid_idle_etcb s; valid_idle s; valid_etcbs b; valid_blocked_2 (ready_queues s) (kheap b) (scheduler_action s) (cur_thread s); cur_thread b = cur_thread s; scheduler_action s = resume_cur_thread \<longrightarrow> st_tcb_at activatable (cur_thread s) s; ready_queues b = ready_queues s; \<forall>t. scheduler_action s = switch_thread t \<longrightarrow> st_tcb_at runnable t s; switch_in_cur_domain s; scheduler_action b = scheduler_action s; cur_domain b = cur_domain s; idle_thread b = idle_thread s\<rbrakk> \<Longrightarrow> valid_idle_etcb b proof (prove)
goal (2 subgoals):
 1. \<And>s a b. \<lbrakk>(a, b) \<in> fst (f s); I s; ct_active s; valid_etcbs s; valid_queues s; ct_not_in_q_2 (ready_queues s) resume_cur_thread (cur_thread s); valid_blocked_2 (ready_queues s) (kheap s) resume_cur_thread (cur_thread s); valid_idle_etcb s; valid_idle s; valid_etcbs b; valid_blocked_2 (ready_queues s) (kheap b) resume_cur_thread (cur_thread s); cur_thread b = cur_thread s; st_tcb_at activatable (cur_thread s) s; ready_queues b = ready_queues s; switch_in_cur_domain_2 resume_cur_thread (ekheap s) (cur_domain s); scheduler_action b = resume_cur_thread; cur_domain b = cur_domain s; idle_thread b = idle_thread s; scheduler_action s = resume_cur_thread; etcb_at (\<lambda>t. tcb_domain t = cur_domain s) (cur_thread s) s\<rbrakk> \<Longrightarrow> cur_thread s = idle_thread s \<or> etcb_at (\<lambda>t. tcb_domain t = cur_domain s) (cur_thread s) b
 2. \<And>s a b. \<lbrakk>(a, b) \<in> fst (f s); I s; ct_active s; valid_etcbs s; valid_queues s; ct_not_in_q s; scheduler_action s = resume_cur_thread \<longrightarrow> cur_thread s = idle_thread s \<or> etcb_at (\<lambda>t. tcb_domain t = cur_domain s) (cur_thread s) s; valid_blocked s; valid_idle_etcb s; valid_idle s; valid_etcbs b; valid_blocked_2 (ready_queues s) (kheap b) (scheduler_action s) (cur_thread s); cur_thread b = cur_thread s; scheduler_action s = resume_cur_thread \<longrightarrow> st_tcb_at activatable (cur_thread s) s; ready_queues b = ready_queues s; \<forall>t. scheduler_action s = switch_thread t \<longrightarrow> st_tcb_at runnable t s; switch_in_cur_domain s; scheduler_action b = scheduler_action s; cur_domain b = cur_domain s; idle_thread b = idle_thread s\<rbrakk> \<Longrightarrow> valid_idle_etcb b proof (prove)
goal (3 subgoals):
 1. \<And>s a b. \<lbrakk>(a, b) \<in> fst (f s); I s; ct_active s; valid_etcbs s; valid_queues s; ct_not_in_q_2 (ready_queues s) resume_cur_thread (cur_thread s); valid_blocked_2 (ready_queues s) (kheap s) resume_cur_thread (cur_thread s); valid_idle_etcb s; valid_idle s; valid_etcbs b; valid_blocked_2 (ready_queues s) (kheap b) resume_cur_thread (cur_thread s); cur_thread b = cur_thread s; st_tcb_at activatable (cur_thread s) s; ready_queues b = ready_queues s; switch_in_cur_domain_2 resume_cur_thread (ekheap s) (cur_domain s); scheduler_action b = resume_cur_thread; cur_domain b = cur_domain s; idle_thread b = idle_thread s; scheduler_action s = resume_cur_thread; etcb_at (\<lambda>t. tcb_domain t = cur_domain s) (cur_thread s) s\<rbrakk> \<Longrightarrow> (etcb_at (\<lambda>t. tcb_domain t = cur_domain s) (cur_thread s) and valid_etcbs) s
 2. \<And>s a b. \<lbrakk>(a, b) \<in> fst (f s); I s; ct_active s; valid_etcbs s; valid_queues s; ct_not_in_q_2 (ready_queues s) resume_cur_thread (cur_thread s); valid_blocked_2 (ready_queues s) (kheap s) resume_cur_thread (cur_thread s); valid_idle_etcb s; valid_idle s; valid_etcbs b; valid_blocked_2 (ready_queues s) (kheap b) resume_cur_thread (cur_thread s); cur_thread b = cur_thread s; st_tcb_at activatable (cur_thread s) s; ready_queues b = ready_queues s; switch_in_cur_domain_2 resume_cur_thread (ekheap s) (cur_domain s); scheduler_action b = resume_cur_thread; cur_domain b = cur_domain s; idle_thread b = idle_thread s; scheduler_action s = resume_cur_thread; etcb_at (\<lambda>t. tcb_domain t = cur_domain s) (cur_thread s) s; st_tcb_at (Not \<circ> inactive) (cur_thread s) b \<longrightarrow> etcb_at (\<lambda>t. tcb_domain t = cur_domain s) (cur_thread s) b\<rbrakk> \<Longrightarrow> cur_thread s = idle_thread s \<or> etcb_at (\<lambda>t. tcb_domain t = cur_domain s) (cur_thread s) b
 3. \<And>s a b. \<lbrakk>(a, b) \<in> fst (f s); I s; ct_active s; valid_etcbs s; valid_queues s; ct_not_in_q s; scheduler_action s = resume_cur_thread \<longrightarrow> cur_thread s = idle_thread s \<or> etcb_at (\<lambda>t. tcb_domain t = cur_domain s) (cur_thread s) s; valid_blocked s; valid_idle_etcb s; valid_idle s; valid_etcbs b; valid_blocked_2 (ready_queues s) (kheap b) (scheduler_action s) (cur_thread s); cur_thread b = cur_thread s; scheduler_action s = resume_cur_thread \<longrightarrow> st_tcb_at activatable (cur_thread s) s; ready_queues b = ready_queues s; \<forall>t. scheduler_action s = switch_thread t \<longrightarrow> st_tcb_at runnable t s; switch_in_cur_domain s; scheduler_action b = scheduler_action s; cur_domain b = cur_domain s; idle_thread b = idle_thread s\<rbrakk> \<Longrightarrow> valid_idle_etcb b proof (prove)
goal (2 subgoals):
 1. \<And>s a b. \<lbrakk>(a, b) \<in> fst (f s); I s; ct_active s; valid_etcbs s; valid_queues s; ct_not_in_q_2 (ready_queues s) resume_cur_thread (cur_thread s); valid_blocked_2 (ready_queues s) (kheap s) resume_cur_thread (cur_thread s); valid_idle_etcb s; valid_idle s; valid_etcbs b; valid_blocked_2 (ready_queues s) (kheap b) resume_cur_thread (cur_thread s); cur_thread b = cur_thread s; st_tcb_at activatable (cur_thread s) s; ready_queues b = ready_queues s; switch_in_cur_domain_2 resume_cur_thread (ekheap s) (cur_domain s); scheduler_action b = resume_cur_thread; cur_domain b = cur_domain s; idle_thread b = idle_thread s; scheduler_action s = resume_cur_thread; etcb_at (\<lambda>t. tcb_domain t = cur_domain s) (cur_thread s) s; st_tcb_at (Not \<circ> inactive) (cur_thread s) b \<longrightarrow> etcb_at (\<lambda>t. tcb_domain t = cur_domain s) (cur_thread s) b\<rbrakk> \<Longrightarrow> cur_thread s = idle_thread s \<or> etcb_at (\<lambda>t. tcb_domain t = cur_domain s) (cur_thread s) b
 2. \<And>s a b. \<lbrakk>(a, b) \<in> fst (f s); I s; ct_active s; valid_etcbs s; valid_queues s; ct_not_in_q s; scheduler_action s = resume_cur_thread \<longrightarrow> cur_thread s = idle_thread s \<or> etcb_at (\<lambda>t. tcb_domain t = cur_domain s) (cur_thread s) s; valid_blocked s; valid_idle_etcb s; valid_idle s; valid_etcbs b; valid_blocked_2 (ready_queues s) (kheap b) (scheduler_action s) (cur_thread s); cur_thread b = cur_thread s; scheduler_action s = resume_cur_thread \<longrightarrow> st_tcb_at activatable (cur_thread s) s; ready_queues b = ready_queues s; \<forall>t. scheduler_action s = switch_thread t \<longrightarrow> st_tcb_at runnable t s; switch_in_cur_domain s; scheduler_action b = scheduler_action s; cur_domain b = cur_domain s; idle_thread b = idle_thread s\<rbrakk> \<Longrightarrow> valid_idle_etcb b proof (prove)
goal (2 subgoals):
 1. \<And>s a b. \<lbrakk>(a, b) \<in> fst (f s); I s; ct_active s; valid_etcbs s; valid_queues s; ct_not_in_q_2 (ready_queues s) resume_cur_thread (cur_thread s); valid_blocked_2 (ready_queues s) (kheap s) resume_cur_thread (cur_thread s); valid_idle_etcb s; valid_idle s; valid_etcbs b; valid_blocked_2 (ready_queues s) (kheap b) resume_cur_thread (cur_thread s); cur_thread b = cur_thread s; st_tcb_at activatable (cur_thread s) s; ready_queues b = ready_queues s; switch_in_cur_domain_2 resume_cur_thread (ekheap s) (cur_domain s); scheduler_action b = resume_cur_thread; cur_domain b = cur_domain s; idle_thread b = idle_thread s; scheduler_action s = resume_cur_thread; etcb_at (\<lambda>t. tcb_domain t = cur_domain s) (cur_thread s) s; \<not> etcb_at (\<lambda>t. tcb_domain t = cur_domain s) (cur_thread s) b; \<not> st_tcb_at (Not \<circ> inactive) (cur_thread s) b\<rbrakk> \<Longrightarrow> cur_thread s = idle_thread s
 2. \<And>s a b. \<lbrakk>(a, b) \<in> fst (f s); I s; ct_active s; valid_etcbs s; valid_queues s; ct_not_in_q s; scheduler_action s = resume_cur_thread \<longrightarrow> cur_thread s = idle_thread s \<or> etcb_at (\<lambda>t. tcb_domain t = cur_domain s) (cur_thread s) s; valid_blocked s; valid_idle_etcb s; valid_idle s; valid_etcbs b; valid_blocked_2 (ready_queues s) (kheap b) (scheduler_action s) (cur_thread s); cur_thread b = cur_thread s; scheduler_action s = resume_cur_thread \<longrightarrow> st_tcb_at activatable (cur_thread s) s; ready_queues b = ready_queues s; \<forall>t. scheduler_action s = switch_thread t \<longrightarrow> st_tcb_at runnable t s; switch_in_cur_domain s; scheduler_action b = scheduler_action s; cur_domain b = cur_domain s; idle_thread b = idle_thread s\<rbrakk> \<Longrightarrow> valid_idle_etcb b proof (prove)
goal (2 subgoals):
 1. \<And>s a b. \<lbrakk>(a, b) \<in> fst (f s); I s; ct_active s; valid_etcbs s; valid_queues s; ct_not_in_q_2 (ready_queues s) resume_cur_thread (cur_thread s); valid_blocked_2 (ready_queues s) (kheap s) resume_cur_thread (cur_thread s); valid_idle_etcb s; valid_idle s; valid_etcbs b; valid_blocked_2 (ready_queues s) (kheap b) resume_cur_thread (cur_thread s); cur_thread b = cur_thread s; st_tcb_at activatable (cur_thread s) s; ready_queues b = ready_queues s; switch_in_cur_domain_2 resume_cur_thread (ekheap s) (cur_domain s); scheduler_action b = resume_cur_thread; cur_domain b = cur_domain s; idle_thread b = idle_thread s; scheduler_action s = resume_cur_thread; etcb_at (\<lambda>t. tcb_domain t = cur_domain s) (cur_thread s) s; \<not> etcb_at (\<lambda>t. tcb_domain t = cur_domain s) (cur_thread s) b\<rbrakk> \<Longrightarrow> (I and ct_active and st_tcb_at (Not \<circ> inactive and Not \<circ> inactive and Not \<circ> idle) (cur_thread s)) s
 2. \<And>s a b. \<lbrakk>(a, b) \<in> fst (f s); I s; ct_active s; valid_etcbs s; valid_queues s; ct_not_in_q s; scheduler_action s = resume_cur_thread \<longrightarrow> cur_thread s = idle_thread s \<or> etcb_at (\<lambda>t. tcb_domain t = cur_domain s) (cur_thread s) s; valid_blocked s; valid_idle_etcb s; valid_idle s; valid_etcbs b; valid_blocked_2 (ready_queues s) (kheap b) (scheduler_action s) (cur_thread s); cur_thread b = cur_thread s; scheduler_action s = resume_cur_thread \<longrightarrow> st_tcb_at activatable (cur_thread s) s; ready_queues b = ready_queues s; \<forall>t. scheduler_action s = switch_thread t \<longrightarrow> st_tcb_at runnable t s; switch_in_cur_domain s; scheduler_action b = scheduler_action s; cur_domain b = cur_domain s; idle_thread b = idle_thread s\<rbrakk> \<Longrightarrow> valid_idle_etcb b proof (prove)
goal (2 subgoals):
 1. \<And>s a b. \<lbrakk>(a, b) \<in> fst (f s); I s; st_tcb_at active (cur_thread s) s; valid_etcbs s; valid_queues s; ct_not_in_q_2 (ready_queues s) resume_cur_thread (cur_thread s); valid_blocked_2 (ready_queues s) (kheap s) resume_cur_thread (cur_thread s); valid_idle_etcb s; valid_idle s; valid_etcbs b; valid_blocked_2 (ready_queues s) (kheap b) resume_cur_thread (cur_thread s); cur_thread b = cur_thread s; st_tcb_at activatable (cur_thread s) s; ready_queues b = ready_queues s; switch_in_cur_domain_2 resume_cur_thread (ekheap s) (cur_domain s); scheduler_action b = resume_cur_thread; cur_domain b = cur_domain s; idle_thread b = idle_thread s; scheduler_action s = resume_cur_thread; etcb_at (\<lambda>t. tcb_domain t = cur_domain s) (cur_thread s) s; \<not> etcb_at (\<lambda>t. tcb_domain t = cur_domain s) (cur_thread s) b\<rbrakk> \<Longrightarrow> st_tcb_at (Not \<circ> inactive and Not \<circ> idle) (cur_thread s) s
 2. \<And>s a b. \<lbrakk>(a, b) \<in> fst (f s); I s; ct_active s; valid_etcbs s; valid_queues s; ct_not_in_q s; scheduler_action s = resume_cur_thread \<longrightarrow> cur_thread s = idle_thread s \<or> etcb_at (\<lambda>t. tcb_domain t = cur_domain s) (cur_thread s) s; valid_blocked s; valid_idle_etcb s; valid_idle s; valid_etcbs b; valid_blocked_2 (ready_queues s) (kheap b) (scheduler_action s) (cur_thread s); cur_thread b = cur_thread s; scheduler_action s = resume_cur_thread \<longrightarrow> st_tcb_at activatable (cur_thread s) s; ready_queues b = ready_queues s; \<forall>t. scheduler_action s = switch_thread t \<longrightarrow> st_tcb_at runnable t s; switch_in_cur_domain s; scheduler_action b = scheduler_action s; cur_domain b = cur_domain s; idle_thread b = idle_thread s\<rbrakk> \<Longrightarrow> valid_idle_etcb b proof (prove)
goal (2 subgoals):
 1. \<And>s a b st. \<lbrakk>(a, b) \<in> fst (f s); I s; valid_etcbs s; valid_queues s; ct_not_in_q_2 (ready_queues s) resume_cur_thread (cur_thread s); valid_blocked_2 (ready_queues s) (kheap s) resume_cur_thread (cur_thread s); valid_idle_etcb s; valid_idle s; valid_etcbs b; valid_blocked_2 (ready_queues s) (kheap b) resume_cur_thread (cur_thread s); cur_thread b = cur_thread s; st_tcb_at activatable (cur_thread s) s; ready_queues b = ready_queues s; switch_in_cur_domain_2 resume_cur_thread (ekheap s) (cur_domain s); scheduler_action b = resume_cur_thread; cur_domain b = cur_domain s; idle_thread b = idle_thread s; scheduler_action s = resume_cur_thread; etcb_at (\<lambda>t. tcb_domain t = cur_domain s) (cur_thread s) s; \<not> etcb_at (\<lambda>t. tcb_domain t = cur_domain s) (cur_thread s) b; active st\<rbrakk> \<Longrightarrow> (Not \<circ> inactive and Not \<circ> idle) st
 2. \<And>s a b. \<lbrakk>(a, b) \<in> fst (f s); I s; ct_active s; valid_etcbs s; valid_queues s; ct_not_in_q s; scheduler_action s = resume_cur_thread \<longrightarrow> cur_thread s = idle_thread s \<or> etcb_at (\<lambda>t. tcb_domain t = cur_domain s) (cur_thread s) s; valid_blocked s; valid_idle_etcb s; valid_idle s; valid_etcbs b; valid_blocked_2 (ready_queues s) (kheap b) (scheduler_action s) (cur_thread s); cur_thread b = cur_thread s; scheduler_action s = resume_cur_thread \<longrightarrow> st_tcb_at activatable (cur_thread s) s; ready_queues b = ready_queues s; \<forall>t. scheduler_action s = switch_thread t \<longrightarrow> st_tcb_at runnable t s; switch_in_cur_domain s; scheduler_action b = scheduler_action s; cur_domain b = cur_domain s; idle_thread b = idle_thread s\<rbrakk> \<Longrightarrow> valid_idle_etcb b proof (prove)
goal (2 subgoals):
 1. \<And>s a b st. \<lbrakk>(a, b) \<in> fst (f s); I s; valid_etcbs s; valid_queues s; ct_not_in_q_2 (ready_queues s) resume_cur_thread (cur_thread s); valid_blocked_2 (ready_queues s) (kheap s) resume_cur_thread (cur_thread s); valid_idle_etcb s; valid_idle s; valid_etcbs b; valid_blocked_2 (ready_queues s) (kheap b) resume_cur_thread (cur_thread s); cur_thread b = cur_thread s; st_tcb_at activatable (cur_thread s) s; ready_queues b = ready_queues s; switch_in_cur_domain_2 resume_cur_thread (ekheap s) (cur_domain s); scheduler_action b = resume_cur_thread; cur_domain b = cur_domain s; idle_thread b = idle_thread s; scheduler_action s = resume_cur_thread; etcb_at (\<lambda>t. tcb_domain t = cur_domain s) (cur_thread s) s; \<not> etcb_at (\<lambda>t. tcb_domain t = cur_domain s) (cur_thread s) b; active st\<rbrakk> \<Longrightarrow> st \<noteq> Inactive \<and> st \<noteq> IdleThreadState
 2. \<And>s a b. \<lbrakk>(a, b) \<in> fst (f s); I s; ct_active s; valid_etcbs s; valid_queues s; ct_not_in_q s; scheduler_action s = resume_cur_thread \<longrightarrow> cur_thread s = idle_thread s \<or> etcb_at (\<lambda>t. tcb_domain t = cur_domain s) (cur_thread s) s; valid_blocked s; valid_idle_etcb s; valid_idle s; valid_etcbs b; valid_blocked_2 (ready_queues s) (kheap b) (scheduler_action s) (cur_thread s); cur_thread b = cur_thread s; scheduler_action s = resume_cur_thread \<longrightarrow> st_tcb_at activatable (cur_thread s) s; ready_queues b = ready_queues s; \<forall>t. scheduler_action s = switch_thread t \<longrightarrow> st_tcb_at runnable t s; switch_in_cur_domain s; scheduler_action b = scheduler_action s; cur_domain b = cur_domain s; idle_thread b = idle_thread s\<rbrakk> \<Longrightarrow> valid_idle_etcb b proof (prove)
goal (1 subgoal):
 1. \<And>s a b. \<lbrakk>(a, b) \<in> fst (f s); I s; ct_active s; valid_etcbs s; valid_queues s; ct_not_in_q s; scheduler_action s = resume_cur_thread \<longrightarrow> cur_thread s = idle_thread s \<or> etcb_at (\<lambda>t. tcb_domain t = cur_domain s) (cur_thread s) s; valid_blocked s; valid_idle_etcb s; valid_idle s; valid_etcbs b; valid_blocked_2 (ready_queues s) (kheap b) (scheduler_action s) (cur_thread s); cur_thread b = cur_thread s; scheduler_action s = resume_cur_thread \<longrightarrow> st_tcb_at activatable (cur_thread s) s; ready_queues b = ready_queues s; \<forall>t. scheduler_action s = switch_thread t \<longrightarrow> st_tcb_at runnable t s; switch_in_cur_domain s; scheduler_action b = scheduler_action s; cur_domain b = cur_domain s; idle_thread b = idle_thread s\<rbrakk> \<Longrightarrow> valid_idle_etcb b proof (prove)
goal (1 subgoal):
 1. \<And>s a b. \<lbrakk>(a, b) \<in> fst (f s); I s; ct_active s; valid_etcbs s; valid_queues s; ct_not_in_q s; scheduler_action s = resume_cur_thread \<longrightarrow> cur_thread s = idle_thread s \<or> etcb_at (\<lambda>t. tcb_domain t = cur_domain s) (cur_thread s) s; valid_blocked s; valid_idle_etcb s; valid_idle s; valid_etcbs b; valid_blocked_2 (ready_queues s) (kheap b) (scheduler_action s) (cur_thread s); cur_thread b = cur_thread s; scheduler_action s = resume_cur_thread \<longrightarrow> st_tcb_at activatable (cur_thread s) s; ready_queues b = ready_queues s; \<forall>t. scheduler_action s = switch_thread t \<longrightarrow> st_tcb_at runnable t s; switch_in_cur_domain s; scheduler_action b = scheduler_action s; cur_domain b = cur_domain s; idle_thread b = idle_thread s; valid_idle b\<rbrakk> \<Longrightarrow> valid_idle_etcb b proof (prove)
goal (1 subgoal):
 1. \<And>s a b. \<lbrakk>(a, b) \<in> fst (f s); I s; ct_active s; valid_etcbs s; valid_queues s; ct_not_in_q s; scheduler_action s = resume_cur_thread \<longrightarrow> cur_thread s = idle_thread s \<or> etcb_at (\<lambda>t. tcb_domain t = cur_domain s) (cur_thread s) s; valid_blocked s; etcb_at (\<lambda>etcb. tcb_domain etcb = default_domain) idle_thread_ptr s; valid_idle s; valid_etcbs b; valid_blocked_2 (ready_queues s) (kheap b) (scheduler_action s) (cur_thread s); cur_thread b = cur_thread s; scheduler_action s = resume_cur_thread \<longrightarrow> st_tcb_at activatable (cur_thread s) s; ready_queues b = ready_queues s; \<forall>t. scheduler_action s = switch_thread t \<longrightarrow> st_tcb_at runnable t s; switch_in_cur_domain s; scheduler_action b = scheduler_action s; cur_domain b = cur_domain s; idle_thread b = idle_thread s; valid_idle b\<rbrakk> \<Longrightarrow> etcb_at (\<lambda>etcb. tcb_domain etcb = default_domain) idle_thread_ptr b proof (prove)
goal (2 subgoals):
 1. \<And>s a b. \<lbrakk>(a, b) \<in> fst (f s); I s; ct_active s; valid_etcbs s; valid_queues s; ct_not_in_q s; scheduler_action s = resume_cur_thread \<longrightarrow> cur_thread s = idle_thread s \<or> etcb_at (\<lambda>t. tcb_domain t = cur_domain s) (cur_thread s) s; valid_blocked s; etcb_at (\<lambda>etcb. tcb_domain etcb = default_domain) idle_thread_ptr s; valid_idle s; valid_etcbs b; valid_blocked_2 (ready_queues s) (kheap b) (scheduler_action s) (cur_thread s); cur_thread b = cur_thread s; scheduler_action s = resume_cur_thread \<longrightarrow> st_tcb_at activatable (cur_thread s) s; ready_queues b = ready_queues s; \<forall>t. scheduler_action s = switch_thread t \<longrightarrow> st_tcb_at runnable t s; switch_in_cur_domain s; scheduler_action b = scheduler_action s; cur_domain b = cur_domain s; idle_thread b = idle_thread s; valid_idle b\<rbrakk> \<Longrightarrow> (etcb_at (?P237 s a b) idle_thread_ptr and valid_etcbs) s
 2. \<And>s a b. \<lbrakk>(a, b) \<in> fst (f s); I s; ct_active s; valid_etcbs s; valid_queues s; ct_not_in_q s; scheduler_action s = resume_cur_thread \<longrightarrow> cur_thread s = idle_thread s \<or> etcb_at (\<lambda>t. tcb_domain t = cur_domain s) (cur_thread s) s; valid_blocked s; etcb_at (\<lambda>etcb. tcb_domain etcb = default_domain) idle_thread_ptr s; valid_idle s; valid_etcbs b; valid_blocked_2 (ready_queues s) (kheap b) (scheduler_action s) (cur_thread s); cur_thread b = cur_thread s; scheduler_action s = resume_cur_thread \<longrightarrow> st_tcb_at activatable (cur_thread s) s; ready_queues b = ready_queues s; \<forall>t. scheduler_action s = switch_thread t \<longrightarrow> st_tcb_at runnable t s; switch_in_cur_domain s; scheduler_action b = scheduler_action s; cur_domain b = cur_domain s; idle_thread b = idle_thread s; valid_idle b; st_tcb_at (Not \<circ> inactive) idle_thread_ptr b \<longrightarrow> etcb_at (?P237 s a b) idle_thread_ptr b\<rbrakk> \<Longrightarrow> etcb_at (\<lambda>etcb. tcb_domain etcb = default_domain) idle_thread_ptr b proof (prove)
goal (1 subgoal):
 1. \<And>s a b. \<lbrakk>(a, b) \<in> fst (f s); I s; ct_active s; valid_etcbs s; valid_queues s; ct_not_in_q s; scheduler_action s = resume_cur_thread \<longrightarrow> cur_thread s = idle_thread s \<or> etcb_at (\<lambda>t. tcb_domain t = cur_domain s) (cur_thread s) s; valid_blocked s; etcb_at (\<lambda>etcb. tcb_domain etcb = default_domain) idle_thread_ptr s; valid_idle s; valid_etcbs b; valid_blocked_2 (ready_queues s) (kheap b) (scheduler_action s) (cur_thread s); cur_thread b = cur_thread s; scheduler_action s = resume_cur_thread \<longrightarrow> st_tcb_at activatable (cur_thread s) s; ready_queues b = ready_queues s; \<forall>t. scheduler_action s = switch_thread t \<longrightarrow> st_tcb_at runnable t s; switch_in_cur_domain s; scheduler_action b = scheduler_action s; cur_domain b = cur_domain s; idle_thread b = idle_thread s; valid_idle b; st_tcb_at (Not \<circ> inactive) idle_thread_ptr b \<longrightarrow> etcb_at (\<lambda>etcb. tcb_domain etcb = default_domain) idle_thread_ptr b\<rbrakk> \<Longrightarrow> etcb_at (\<lambda>etcb. tcb_domain etcb = default_domain) idle_thread_ptr b proof (prove)
goal (1 subgoal):
 1. \<And>s a b. \<lbrakk>(a, b) \<in> fst (f s); I s; ct_active s; valid_etcbs s; valid_queues s; ct_not_in_q s; scheduler_action s = resume_cur_thread \<longrightarrow> cur_thread s = idle_thread s \<or> etcb_at (\<lambda>t. tcb_domain t = cur_domain s) (cur_thread s) s; valid_blocked s; etcb_at (\<lambda>etcb. tcb_domain etcb = default_domain) idle_thread_ptr s; valid_idle s; valid_etcbs b; valid_blocked_2 (ready_queues s) (kheap b) (scheduler_action s) (cur_thread s); cur_thread b = cur_thread s; scheduler_action s = resume_cur_thread \<longrightarrow> st_tcb_at activatable (cur_thread s) s; ready_queues b = ready_queues s; \<forall>t. scheduler_action s = switch_thread t \<longrightarrow> st_tcb_at runnable t s; switch_in_cur_domain s; scheduler_action b = scheduler_action s; cur_domain b = cur_domain s; idle_thread b = idle_thread s; valid_idle b\<rbrakk> \<Longrightarrow> st_tcb_at (Not \<circ> inactive) idle_thread_ptr b proof (prove)
goal:
No subgoals!