theory DetSchedSchedule_AI

lemma tcb_sched_action_dequeue_strong_valid_sched:
  "\<lbrace>valid_etcbs and ct_not_in_q and valid_sched_action and ct_in_cur_domain and
    valid_blocked and st_tcb_at (\<lambda>st. \<not> runnable st) thread and
    (\<lambda>es. \<forall>d p. (\<forall>t\<in>set (ready_queues es d p). is_etcb_at t es \<and>
        etcb_at (\<lambda>t. tcb_priority t = p \<and> tcb_domain t = d) t es \<and>
        (t \<noteq> thread \<longrightarrow> st_tcb_at runnable t es)) \<and> distinct (ready_queues es d p)) and
    valid_idle_etcb\<rbrace>
    tcb_sched_action tcb_sched_dequeue thread
   \<lbrace>\<lambda>_. valid_sched\<rbrace>" apply (simp add: tcb_sched_action_def unless_def set_tcb_queue_def) apply wp apply (clarsimp simp: etcb_at_def valid_sched_def split: option.split) apply (rule conjI) apply (fastforce simp: etcb_at_def is_etcb_at_def valid_queues_def2 tcb_sched_dequeue_def) apply (rule conjI) apply (fastforce simp: ct_not_in_q_def not_queued_def tcb_sched_dequeue_def) apply (clarsimp simp: valid_blocked_def tcb_sched_dequeue_def) apply (case_tac "t=thread") apply simp apply (force simp: st_tcb_at_def obj_at_def) apply (erule_tac x=t in allE) apply (erule impE) apply (clarsimp simp: not_queued_def split: if_split_asm) apply (erule_tac x=d in allE) apply force apply force done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>valid_etcbs and ct_not_in_q and valid_sched_action and ct_in_cur_domain and valid_blocked and st_tcb_at (\<lambda>st. \<not> runnable st) thread and (\<lambda>es. \<forall>d p. (\<forall>t\<in>set (ready_queues es d p). is_etcb_at t es \<and> etcb_at (\<lambda>t. tcb_priority t = p \<and> tcb_domain t = d) t es \<and> (t \<noteq> thread \<longrightarrow> st_tcb_at runnable t es)) \<and> distinct (ready_queues es d p)) and valid_idle_etcb\<rbrace> tcb_sched_action tcb_sched_dequeue thread \<lbrace>\<lambda>_. valid_sched\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>valid_etcbs and ct_not_in_q and valid_sched_action and ct_in_cur_domain and valid_blocked and st_tcb_at (\<lambda>st. \<not> runnable st) thread and (\<lambda>es. \<forall>d p. (\<forall>t\<in>set (ready_queues es d p). is_etcb_at t es \<and> etcb_at (\<lambda>t. tcb_priority t = p \<and> tcb_domain t = d) t es \<and> (t \<noteq> thread \<longrightarrow> st_tcb_at runnable t es)) \<and> distinct (ready_queues es d p)) and valid_idle_etcb\<rbrace> do d <- ethread_get tcb_domain thread;
prio <- ethread_get tcb_priority thread;
queue <- get_tcb_queue d prio;
modify (\<lambda>es. ready_queues_update (\<lambda>_ d' p. if d' = d \<and> p = prio then tcb_sched_dequeue thread queue else ready_queues es d' p) es)
od \<lbrace>\<lambda>_. valid_sched\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s. (valid_etcbs and ct_not_in_q and valid_sched_action and ct_in_cur_domain and valid_blocked and st_tcb_at (\<lambda>st. \<not> runnable st) thread and (\<lambda>es. \<forall>d p. (\<forall>t\<in>set (ready_queues es d p). is_etcb_at t es \<and> etcb_at (\<lambda>t. tcb_priority t = p \<and> tcb_domain t = d) t es \<and> (t \<noteq> thread \<longrightarrow> st_tcb_at runnable t es)) \<and> distinct (ready_queues es d p)) and valid_idle_etcb) s \<Longrightarrow> etcb_at (\<lambda>t. etcb_at (\<lambda>ta. valid_sched (ready_queues_update (\<lambda>_ d' p. if d' = tcb_domain t \<and> p = tcb_priority ta then tcb_sched_dequeue thread (ready_queues s (tcb_domain t) (tcb_priority ta)) else ready_queues s d' p) s)) thread s) thread s proof (prove)
goal (1 subgoal):
 1. \<And>s x2. \<lbrakk>valid_etcbs s; ct_not_in_q s; valid_sched_action s; ct_in_cur_domain s; valid_blocked s; st_tcb_at (\<lambda>st. \<not> runnable st) thread s; \<forall>d p. (\<forall>t\<in>set (ready_queues s d p). is_etcb_at t s \<and> (case ekheap s t of None \<Rightarrow> True | Some x \<Rightarrow> tcb_priority x = p \<and> tcb_domain x = d) \<and> (t \<noteq> thread \<longrightarrow> st_tcb_at runnable t s)) \<and> distinct (ready_queues s d p); valid_idle_etcb s; ekheap s thread = Some x2\<rbrakk> \<Longrightarrow> valid_queues_2 (\<lambda>d' p. if d' = tcb_domain x2 \<and> p = tcb_priority x2 then tcb_sched_dequeue thread (ready_queues s (tcb_domain x2) (tcb_priority x2)) else ready_queues s d' p) (ekheap s) (kheap s) \<and> ct_not_in_q_2 (\<lambda>d' p. if d' = tcb_domain x2 \<and> p = tcb_priority x2 then tcb_sched_dequeue thread (ready_queues s (tcb_domain x2) (tcb_priority x2)) else ready_queues s d' p) (scheduler_action s) (cur_thread s) \<and> valid_blocked_2 (\<lambda>d' p. if d' = tcb_domain x2 \<and> p = tcb_priority x2 then tcb_sched_dequeue thread (ready_queues s (tcb_domain x2) (tcb_priority x2)) else ready_queues s d' p) (kheap s) (scheduler_action s) (cur_thread s) proof (prove)
goal (2 subgoals):
 1. \<And>s x2. \<lbrakk>valid_etcbs s; ct_not_in_q s; valid_sched_action s; ct_in_cur_domain s; valid_blocked s; st_tcb_at (\<lambda>st. \<not> runnable st) thread s; \<forall>d p. (\<forall>t\<in>set (ready_queues s d p). is_etcb_at t s \<and> (case ekheap s t of None \<Rightarrow> True | Some x \<Rightarrow> tcb_priority x = p \<and> tcb_domain x = d) \<and> (t \<noteq> thread \<longrightarrow> st_tcb_at runnable t s)) \<and> distinct (ready_queues s d p); valid_idle_etcb s; ekheap s thread = Some x2\<rbrakk> \<Longrightarrow> valid_queues_2 (\<lambda>d' p. if d' = tcb_domain x2 \<and> p = tcb_priority x2 then tcb_sched_dequeue thread (ready_queues s (tcb_domain x2) (tcb_priority x2)) else ready_queues s d' p) (ekheap s) (kheap s)
 2. \<And>s x2. \<lbrakk>valid_etcbs s; ct_not_in_q s; valid_sched_action s; ct_in_cur_domain s; valid_blocked s; st_tcb_at (\<lambda>st. \<not> runnable st) thread s; \<forall>d p. (\<forall>t\<in>set (ready_queues s d p). is_etcb_at t s \<and> (case ekheap s t of None \<Rightarrow> True | Some x \<Rightarrow> tcb_priority x = p \<and> tcb_domain x = d) \<and> (t \<noteq> thread \<longrightarrow> st_tcb_at runnable t s)) \<and> distinct (ready_queues s d p); valid_idle_etcb s; ekheap s thread = Some x2\<rbrakk> \<Longrightarrow> ct_not_in_q_2 (\<lambda>d' p. if d' = tcb_domain x2 \<and> p = tcb_priority x2 then tcb_sched_dequeue thread (ready_queues s (tcb_domain x2) (tcb_priority x2)) else ready_queues s d' p) (scheduler_action s) (cur_thread s) \<and> valid_blocked_2 (\<lambda>d' p. if d' = tcb_domain x2 \<and> p = tcb_priority x2 then tcb_sched_dequeue thread (ready_queues s (tcb_domain x2) (tcb_priority x2)) else ready_queues s d' p) (kheap s) (scheduler_action s) (cur_thread s) proof (prove)
goal (1 subgoal):
 1. \<And>s x2. \<lbrakk>valid_etcbs s; ct_not_in_q s; valid_sched_action s; ct_in_cur_domain s; valid_blocked s; st_tcb_at (\<lambda>st. \<not> runnable st) thread s; \<forall>d p. (\<forall>t\<in>set (ready_queues s d p). is_etcb_at t s \<and> (case ekheap s t of None \<Rightarrow> True | Some x \<Rightarrow> tcb_priority x = p \<and> tcb_domain x = d) \<and> (t \<noteq> thread \<longrightarrow> st_tcb_at runnable t s)) \<and> distinct (ready_queues s d p); valid_idle_etcb s; ekheap s thread = Some x2\<rbrakk> \<Longrightarrow> ct_not_in_q_2 (\<lambda>d' p. if d' = tcb_domain x2 \<and> p = tcb_priority x2 then tcb_sched_dequeue thread (ready_queues s (tcb_domain x2) (tcb_priority x2)) else ready_queues s d' p) (scheduler_action s) (cur_thread s) \<and> valid_blocked_2 (\<lambda>d' p. if d' = tcb_domain x2 \<and> p = tcb_priority x2 then tcb_sched_dequeue thread (ready_queues s (tcb_domain x2) (tcb_priority x2)) else ready_queues s d' p) (kheap s) (scheduler_action s) (cur_thread s) proof (prove)
goal (2 subgoals):
 1. \<And>s x2. \<lbrakk>valid_etcbs s; ct_not_in_q s; valid_sched_action s; ct_in_cur_domain s; valid_blocked s; st_tcb_at (\<lambda>st. \<not> runnable st) thread s; \<forall>d p. (\<forall>t\<in>set (ready_queues s d p). is_etcb_at t s \<and> (case ekheap s t of None \<Rightarrow> True | Some x \<Rightarrow> tcb_priority x = p \<and> tcb_domain x = d) \<and> (t \<noteq> thread \<longrightarrow> st_tcb_at runnable t s)) \<and> distinct (ready_queues s d p); valid_idle_etcb s; ekheap s thread = Some x2\<rbrakk> \<Longrightarrow> ct_not_in_q_2 (\<lambda>d' p. if d' = tcb_domain x2 \<and> p = tcb_priority x2 then tcb_sched_dequeue thread (ready_queues s (tcb_domain x2) (tcb_priority x2)) else ready_queues s d' p) (scheduler_action s) (cur_thread s)
 2. \<And>s x2. \<lbrakk>valid_etcbs s; ct_not_in_q s; valid_sched_action s; ct_in_cur_domain s; valid_blocked s; st_tcb_at (\<lambda>st. \<not> runnable st) thread s; \<forall>d p. (\<forall>t\<in>set (ready_queues s d p). is_etcb_at t s \<and> (case ekheap s t of None \<Rightarrow> True | Some x \<Rightarrow> tcb_priority x = p \<and> tcb_domain x = d) \<and> (t \<noteq> thread \<longrightarrow> st_tcb_at runnable t s)) \<and> distinct (ready_queues s d p); valid_idle_etcb s; ekheap s thread = Some x2\<rbrakk> \<Longrightarrow> valid_blocked_2 (\<lambda>d' p. if d' = tcb_domain x2 \<and> p = tcb_priority x2 then tcb_sched_dequeue thread (ready_queues s (tcb_domain x2) (tcb_priority x2)) else ready_queues s d' p) (kheap s) (scheduler_action s) (cur_thread s) proof (prove)
goal (1 subgoal):
 1. \<And>s x2. \<lbrakk>valid_etcbs s; ct_not_in_q s; valid_sched_action s; ct_in_cur_domain s; valid_blocked s; st_tcb_at (\<lambda>st. \<not> runnable st) thread s; \<forall>d p. (\<forall>t\<in>set (ready_queues s d p). is_etcb_at t s \<and> (case ekheap s t of None \<Rightarrow> True | Some x \<Rightarrow> tcb_priority x = p \<and> tcb_domain x = d) \<and> (t \<noteq> thread \<longrightarrow> st_tcb_at runnable t s)) \<and> distinct (ready_queues s d p); valid_idle_etcb s; ekheap s thread = Some x2\<rbrakk> \<Longrightarrow> valid_blocked_2 (\<lambda>d' p. if d' = tcb_domain x2 \<and> p = tcb_priority x2 then tcb_sched_dequeue thread (ready_queues s (tcb_domain x2) (tcb_priority x2)) else ready_queues s d' p) (kheap s) (scheduler_action s) (cur_thread s) proof (prove)
goal (1 subgoal):
 1. \<And>s x2 t st. \<lbrakk>valid_etcbs s; ct_not_in_q s; valid_sched_action s; ct_in_cur_domain s; \<forall>t. not_queued t s \<longrightarrow> (\<forall>st. st_tcb_at ((=) st) t s \<longrightarrow> t \<noteq> cur_thread s \<longrightarrow> scheduler_action s \<noteq> switch_thread t \<longrightarrow> st \<noteq> Running \<and> st \<noteq> Restart); st_tcb_at (\<lambda>st. \<not> runnable st) thread s; \<forall>d p. (\<forall>t\<in>set (ready_queues s d p). is_etcb_at t s \<and> (case ekheap s t of None \<Rightarrow> True | Some x \<Rightarrow> tcb_priority x = p \<and> tcb_domain x = d) \<and> (t \<noteq> thread \<longrightarrow> st_tcb_at runnable t s)) \<and> distinct (ready_queues s d p); valid_idle_etcb s; ekheap s thread = Some x2; not_queued_2 (\<lambda>d' p. if d' = tcb_domain x2 \<and> p = tcb_priority x2 then filter (\<lambda>x. x \<noteq> thread) (ready_queues s (tcb_domain x2) (tcb_priority x2)) else ready_queues s d' p) t; st_tcb_at ((=) st) t s; t \<noteq> cur_thread s; scheduler_action s \<noteq> switch_thread t\<rbrakk> \<Longrightarrow> st \<noteq> Running \<and> st \<noteq> Restart proof (prove)
goal (2 subgoals):
 1. \<And>s x2 t st. \<lbrakk>valid_etcbs s; ct_not_in_q s; valid_sched_action s; ct_in_cur_domain s; \<forall>t. not_queued t s \<longrightarrow> (\<forall>st. st_tcb_at ((=) st) t s \<longrightarrow> t \<noteq> cur_thread s \<longrightarrow> scheduler_action s \<noteq> switch_thread t \<longrightarrow> st \<noteq> Running \<and> st \<noteq> Restart); st_tcb_at (\<lambda>st. \<not> runnable st) thread s; \<forall>d p. (\<forall>t\<in>set (ready_queues s d p). is_etcb_at t s \<and> (case ekheap s t of None \<Rightarrow> True | Some x \<Rightarrow> tcb_priority x = p \<and> tcb_domain x = d) \<and> (t \<noteq> thread \<longrightarrow> st_tcb_at runnable t s)) \<and> distinct (ready_queues s d p); valid_idle_etcb s; ekheap s thread = Some x2; not_queued_2 (\<lambda>d' p. if d' = tcb_domain x2 \<and> p = tcb_priority x2 then filter (\<lambda>x. x \<noteq> thread) (ready_queues s (tcb_domain x2) (tcb_priority x2)) else ready_queues s d' p) t; st_tcb_at ((=) st) t s; t \<noteq> cur_thread s; scheduler_action s \<noteq> switch_thread t; t = thread\<rbrakk> \<Longrightarrow> st \<noteq> Running \<and> st \<noteq> Restart
 2. \<And>s x2 t st. \<lbrakk>valid_etcbs s; ct_not_in_q s; valid_sched_action s; ct_in_cur_domain s; \<forall>t. not_queued t s \<longrightarrow> (\<forall>st. st_tcb_at ((=) st) t s \<longrightarrow> t \<noteq> cur_thread s \<longrightarrow> scheduler_action s \<noteq> switch_thread t \<longrightarrow> st \<noteq> Running \<and> st \<noteq> Restart); st_tcb_at (\<lambda>st. \<not> runnable st) thread s; \<forall>d p. (\<forall>t\<in>set (ready_queues s d p). is_etcb_at t s \<and> (case ekheap s t of None \<Rightarrow> True | Some x \<Rightarrow> tcb_priority x = p \<and> tcb_domain x = d) \<and> (t \<noteq> thread \<longrightarrow> st_tcb_at runnable t s)) \<and> distinct (ready_queues s d p); valid_idle_etcb s; ekheap s thread = Some x2; not_queued_2 (\<lambda>d' p. if d' = tcb_domain x2 \<and> p = tcb_priority x2 then filter (\<lambda>x. x \<noteq> thread) (ready_queues s (tcb_domain x2) (tcb_priority x2)) else ready_queues s d' p) t; st_tcb_at ((=) st) t s; t \<noteq> cur_thread s; scheduler_action s \<noteq> switch_thread t; t \<noteq> thread\<rbrakk> \<Longrightarrow> st \<noteq> Running \<and> st \<noteq> Restart proof (prove)
goal (2 subgoals):
 1. \<And>s x2 t st. \<lbrakk>valid_etcbs s; ct_not_in_q s; valid_sched_action s; ct_in_cur_domain s; \<forall>t. not_queued t s \<longrightarrow> (\<forall>st. st_tcb_at ((=) st) t s \<longrightarrow> t \<noteq> cur_thread s \<longrightarrow> scheduler_action s \<noteq> switch_thread t \<longrightarrow> st \<noteq> Running \<and> st \<noteq> Restart); st_tcb_at (\<lambda>st. \<not> runnable st) thread s; \<forall>d p. (\<forall>t\<in>set (ready_queues s d p). is_etcb_at t s \<and> (case ekheap s t of None \<Rightarrow> True | Some x \<Rightarrow> tcb_priority x = p \<and> tcb_domain x = d) \<and> (t \<noteq> thread \<longrightarrow> st_tcb_at runnable t s)) \<and> distinct (ready_queues s d p); valid_idle_etcb s; ekheap s thread = Some x2; not_queued_2 (\<lambda>d' p. if d' = tcb_domain x2 \<and> p = tcb_priority x2 then filter (\<lambda>x. x \<noteq> thread) (ready_queues s (tcb_domain x2) (tcb_priority x2)) else ready_queues s d' p) thread; st_tcb_at ((=) st) thread s; thread \<noteq> cur_thread s; scheduler_action s \<noteq> switch_thread thread; t = thread\<rbrakk> \<Longrightarrow> st \<noteq> Running \<and> st \<noteq> Restart
 2. \<And>s x2 t st. \<lbrakk>valid_etcbs s; ct_not_in_q s; valid_sched_action s; ct_in_cur_domain s; \<forall>t. not_queued t s \<longrightarrow> (\<forall>st. st_tcb_at ((=) st) t s \<longrightarrow> t \<noteq> cur_thread s \<longrightarrow> scheduler_action s \<noteq> switch_thread t \<longrightarrow> st \<noteq> Running \<and> st \<noteq> Restart); st_tcb_at (\<lambda>st. \<not> runnable st) thread s; \<forall>d p. (\<forall>t\<in>set (ready_queues s d p). is_etcb_at t s \<and> (case ekheap s t of None \<Rightarrow> True | Some x \<Rightarrow> tcb_priority x = p \<and> tcb_domain x = d) \<and> (t \<noteq> thread \<longrightarrow> st_tcb_at runnable t s)) \<and> distinct (ready_queues s d p); valid_idle_etcb s; ekheap s thread = Some x2; not_queued_2 (\<lambda>d' p. if d' = tcb_domain x2 \<and> p = tcb_priority x2 then filter (\<lambda>x. x \<noteq> thread) (ready_queues s (tcb_domain x2) (tcb_priority x2)) else ready_queues s d' p) t; st_tcb_at ((=) st) t s; t \<noteq> cur_thread s; scheduler_action s \<noteq> switch_thread t; t \<noteq> thread\<rbrakk> \<Longrightarrow> st \<noteq> Running \<and> st \<noteq> Restart proof (prove)
goal (1 subgoal):
 1. \<And>s x2 t st. \<lbrakk>valid_etcbs s; ct_not_in_q s; valid_sched_action s; ct_in_cur_domain s; \<forall>t. not_queued t s \<longrightarrow> (\<forall>st. st_tcb_at ((=) st) t s \<longrightarrow> t \<noteq> cur_thread s \<longrightarrow> scheduler_action s \<noteq> switch_thread t \<longrightarrow> st \<noteq> Running \<and> st \<noteq> Restart); st_tcb_at (\<lambda>st. \<not> runnable st) thread s; \<forall>d p. (\<forall>t\<in>set (ready_queues s d p). is_etcb_at t s \<and> (case ekheap s t of None \<Rightarrow> True | Some x \<Rightarrow> tcb_priority x = p \<and> tcb_domain x = d) \<and> (t \<noteq> thread \<longrightarrow> st_tcb_at runnable t s)) \<and> distinct (ready_queues s d p); valid_idle_etcb s; ekheap s thread = Some x2; not_queued_2 (\<lambda>d' p. if d' = tcb_domain x2 \<and> p = tcb_priority x2 then filter (\<lambda>x. x \<noteq> thread) (ready_queues s (tcb_domain x2) (tcb_priority x2)) else ready_queues s d' p) t; st_tcb_at ((=) st) t s; t \<noteq> cur_thread s; scheduler_action s \<noteq> switch_thread t; t \<noteq> thread\<rbrakk> \<Longrightarrow> st \<noteq> Running \<and> st \<noteq> Restart proof (prove)
goal (1 subgoal):
 1. \<And>s x2 t st. \<lbrakk>valid_etcbs s; ct_not_in_q s; valid_sched_action s; ct_in_cur_domain s; st_tcb_at (\<lambda>st. \<not> runnable st) thread s; \<forall>d p. (\<forall>t\<in>set (ready_queues s d p). is_etcb_at t s \<and> (case ekheap s t of None \<Rightarrow> True | Some x \<Rightarrow> tcb_priority x = p \<and> tcb_domain x = d) \<and> (t \<noteq> thread \<longrightarrow> st_tcb_at runnable t s)) \<and> distinct (ready_queues s d p); valid_idle_etcb s; ekheap s thread = Some x2; not_queued_2 (\<lambda>d' p. if d' = tcb_domain x2 \<and> p = tcb_priority x2 then filter (\<lambda>x. x \<noteq> thread) (ready_queues s (tcb_domain x2) (tcb_priority x2)) else ready_queues s d' p) t; st_tcb_at ((=) st) t s; t \<noteq> cur_thread s; scheduler_action s \<noteq> switch_thread t; t \<noteq> thread; not_queued t s \<longrightarrow> (\<forall>st. st_tcb_at ((=) st) t s \<longrightarrow> t \<noteq> cur_thread s \<longrightarrow> scheduler_action s \<noteq> switch_thread t \<longrightarrow> st \<noteq> Running \<and> st \<noteq> Restart)\<rbrakk> \<Longrightarrow> st \<noteq> Running \<and> st \<noteq> Restart proof (prove)
goal (2 subgoals):
 1. \<And>s x2 t st. \<lbrakk>valid_etcbs s; ct_not_in_q s; valid_sched_action s; ct_in_cur_domain s; st_tcb_at (\<lambda>st. \<not> runnable st) thread s; \<forall>d p. (\<forall>t\<in>set (ready_queues s d p). is_etcb_at t s \<and> (case ekheap s t of None \<Rightarrow> True | Some x \<Rightarrow> tcb_priority x = p \<and> tcb_domain x = d) \<and> (t \<noteq> thread \<longrightarrow> st_tcb_at runnable t s)) \<and> distinct (ready_queues s d p); valid_idle_etcb s; ekheap s thread = Some x2; not_queued_2 (\<lambda>d' p. if d' = tcb_domain x2 \<and> p = tcb_priority x2 then filter (\<lambda>x. x \<noteq> thread) (ready_queues s (tcb_domain x2) (tcb_priority x2)) else ready_queues s d' p) t; st_tcb_at ((=) st) t s; t \<noteq> cur_thread s; scheduler_action s \<noteq> switch_thread t; t \<noteq> thread\<rbrakk> \<Longrightarrow> not_queued t s
 2. \<And>s x2 t st. \<lbrakk>valid_etcbs s; ct_not_in_q s; valid_sched_action s; ct_in_cur_domain s; st_tcb_at (\<lambda>st. \<not> runnable st) thread s; \<forall>d p. (\<forall>t\<in>set (ready_queues s d p). is_etcb_at t s \<and> (case ekheap s t of None \<Rightarrow> True | Some x \<Rightarrow> tcb_priority x = p \<and> tcb_domain x = d) \<and> (t \<noteq> thread \<longrightarrow> st_tcb_at runnable t s)) \<and> distinct (ready_queues s d p); valid_idle_etcb s; ekheap s thread = Some x2; not_queued_2 (\<lambda>d' p. if d' = tcb_domain x2 \<and> p = tcb_priority x2 then filter (\<lambda>x. x \<noteq> thread) (ready_queues s (tcb_domain x2) (tcb_priority x2)) else ready_queues s d' p) t; st_tcb_at ((=) st) t s; t \<noteq> cur_thread s; scheduler_action s \<noteq> switch_thread t; t \<noteq> thread; \<forall>st. st_tcb_at ((=) st) t s \<longrightarrow> t \<noteq> cur_thread s \<longrightarrow> scheduler_action s \<noteq> switch_thread t \<longrightarrow> st \<noteq> Running \<and> st \<noteq> Restart\<rbrakk> \<Longrightarrow> st \<noteq> Running \<and> st \<noteq> Restart proof (prove)
goal (2 subgoals):
 1. \<And>s x2 t st d p. \<lbrakk>\<forall>d p. (p = tcb_priority x2 \<longrightarrow> d = tcb_domain x2 \<longrightarrow> t \<notin> set (ready_queues s (tcb_domain x2) (tcb_priority x2))) \<and> (d = tcb_domain x2 \<and> p = tcb_priority x2 \<or> t \<notin> set (ready_queues s d p)); st_tcb_at ((=) st) t s; t \<noteq> cur_thread s; scheduler_action s \<noteq> switch_thread t; t \<noteq> thread; valid_etcbs s; ct_not_in_q s; valid_sched_action s; ct_in_cur_domain s; st_tcb_at (\<lambda>st. \<not> runnable st) thread s; \<forall>d p. (\<forall>t\<in>set (ready_queues s d p). is_etcb_at t s \<and> (case ekheap s t of None \<Rightarrow> True | Some x \<Rightarrow> tcb_priority x = p \<and> tcb_domain x = d) \<and> (t \<noteq> thread \<longrightarrow> st_tcb_at runnable t s)) \<and> distinct (ready_queues s d p); valid_idle_etcb s; ekheap s thread = Some x2; t \<in> set (ready_queues s d p)\<rbrakk> \<Longrightarrow> False
 2. \<And>s x2 t st. \<lbrakk>valid_etcbs s; ct_not_in_q s; valid_sched_action s; ct_in_cur_domain s; st_tcb_at (\<lambda>st. \<not> runnable st) thread s; \<forall>d p. (\<forall>t\<in>set (ready_queues s d p). is_etcb_at t s \<and> (case ekheap s t of None \<Rightarrow> True | Some x \<Rightarrow> tcb_priority x = p \<and> tcb_domain x = d) \<and> (t \<noteq> thread \<longrightarrow> st_tcb_at runnable t s)) \<and> distinct (ready_queues s d p); valid_idle_etcb s; ekheap s thread = Some x2; not_queued_2 (\<lambda>d' p. if d' = tcb_domain x2 \<and> p = tcb_priority x2 then filter (\<lambda>x. x \<noteq> thread) (ready_queues s (tcb_domain x2) (tcb_priority x2)) else ready_queues s d' p) t; st_tcb_at ((=) st) t s; t \<noteq> cur_thread s; scheduler_action s \<noteq> switch_thread t; t \<noteq> thread; \<forall>st. st_tcb_at ((=) st) t s \<longrightarrow> t \<noteq> cur_thread s \<longrightarrow> scheduler_action s \<noteq> switch_thread t \<longrightarrow> st \<noteq> Running \<and> st \<noteq> Restart\<rbrakk> \<Longrightarrow> st \<noteq> Running \<and> st \<noteq> Restart proof (prove)
goal (2 subgoals):
 1. \<And>s x2 t st d p. \<lbrakk>st_tcb_at ((=) st) t s; t \<noteq> cur_thread s; scheduler_action s \<noteq> switch_thread t; t \<noteq> thread; valid_etcbs s; ct_not_in_q s; valid_sched_action s; ct_in_cur_domain s; st_tcb_at (\<lambda>st. \<not> runnable st) thread s; \<forall>d p. (\<forall>t\<in>set (ready_queues s d p). is_etcb_at t s \<and> (case ekheap s t of None \<Rightarrow> True | Some x \<Rightarrow> tcb_priority x = p \<and> tcb_domain x = d) \<and> (t \<noteq> thread \<longrightarrow> st_tcb_at runnable t s)) \<and> distinct (ready_queues s d p); valid_idle_etcb s; ekheap s thread = Some x2; t \<in> set (ready_queues s d p); \<forall>p. (p = tcb_priority x2 \<longrightarrow> d = tcb_domain x2 \<longrightarrow> t \<notin> set (ready_queues s (tcb_domain x2) (tcb_priority x2))) \<and> (d = tcb_domain x2 \<and> p = tcb_priority x2 \<or> t \<notin> set (ready_queues s d p))\<rbrakk> \<Longrightarrow> False
 2. \<And>s x2 t st. \<lbrakk>valid_etcbs s; ct_not_in_q s; valid_sched_action s; ct_in_cur_domain s; st_tcb_at (\<lambda>st. \<not> runnable st) thread s; \<forall>d p. (\<forall>t\<in>set (ready_queues s d p). is_etcb_at t s \<and> (case ekheap s t of None \<Rightarrow> True | Some x \<Rightarrow> tcb_priority x = p \<and> tcb_domain x = d) \<and> (t \<noteq> thread \<longrightarrow> st_tcb_at runnable t s)) \<and> distinct (ready_queues s d p); valid_idle_etcb s; ekheap s thread = Some x2; not_queued_2 (\<lambda>d' p. if d' = tcb_domain x2 \<and> p = tcb_priority x2 then filter (\<lambda>x. x \<noteq> thread) (ready_queues s (tcb_domain x2) (tcb_priority x2)) else ready_queues s d' p) t; st_tcb_at ((=) st) t s; t \<noteq> cur_thread s; scheduler_action s \<noteq> switch_thread t; t \<noteq> thread; \<forall>st. st_tcb_at ((=) st) t s \<longrightarrow> t \<noteq> cur_thread s \<longrightarrow> scheduler_action s \<noteq> switch_thread t \<longrightarrow> st \<noteq> Running \<and> st \<noteq> Restart\<rbrakk> \<Longrightarrow> st \<noteq> Running \<and> st \<noteq> Restart proof (prove)
goal (1 subgoal):
 1. \<And>s x2 t st. \<lbrakk>valid_etcbs s; ct_not_in_q s; valid_sched_action s; ct_in_cur_domain s; st_tcb_at (\<lambda>st. \<not> runnable st) thread s; \<forall>d p. (\<forall>t\<in>set (ready_queues s d p). is_etcb_at t s \<and> (case ekheap s t of None \<Rightarrow> True | Some x \<Rightarrow> tcb_priority x = p \<and> tcb_domain x = d) \<and> (t \<noteq> thread \<longrightarrow> st_tcb_at runnable t s)) \<and> distinct (ready_queues s d p); valid_idle_etcb s; ekheap s thread = Some x2; not_queued_2 (\<lambda>d' p. if d' = tcb_domain x2 \<and> p = tcb_priority x2 then filter (\<lambda>x. x \<noteq> thread) (ready_queues s (tcb_domain x2) (tcb_priority x2)) else ready_queues s d' p) t; st_tcb_at ((=) st) t s; t \<noteq> cur_thread s; scheduler_action s \<noteq> switch_thread t; t \<noteq> thread; \<forall>st. st_tcb_at ((=) st) t s \<longrightarrow> t \<noteq> cur_thread s \<longrightarrow> scheduler_action s \<noteq> switch_thread t \<longrightarrow> st \<noteq> Running \<and> st \<noteq> Restart\<rbrakk> \<Longrightarrow> st \<noteq> Running \<and> st \<noteq> Restart proof (prove)
goal:
No subgoals!