theory DetSchedSchedule_AI

lemma tcb_sched_action_enqueue_valid_blocked_except:
  "\<lbrace>valid_blocked_except thread\<rbrace>
     tcb_sched_action tcb_sched_enqueue thread'
   \<lbrace>\<lambda>_. valid_blocked_except thread \<rbrace>" apply (simp add: tcb_sched_action_def, wp) apply (clarsimp simp: etcb_at_def tcb_sched_enqueue_def not_queued_def valid_blocked_def valid_blocked_except_def split: option.splits) apply (rule conjI) apply clarsimp apply (case_tac "t=thread") apply force apply (erule_tac x=t in allE) apply clarsimp apply force apply clarsimp apply (case_tac "t=thread") apply force apply (erule_tac x=t in allE) apply clarsimp apply force done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>valid_blocked_except thread\<rbrace> tcb_sched_action tcb_sched_enqueue thread' \<lbrace>\<lambda>_. valid_blocked_except thread\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s. valid_blocked_except thread s \<Longrightarrow> etcb_at (\<lambda>t. etcb_at (\<lambda>ta. valid_blocked_except thread (ready_queues_update (\<lambda>_ t' p. if t' = tcb_domain t \<and> p = tcb_priority ta then tcb_sched_enqueue thread' (ready_queues s (tcb_domain t) (tcb_priority ta)) else ready_queues s t' p) s)) thread' s) thread' s proof (prove)
goal (1 subgoal):
 1. \<And>s x2. \<lbrakk>\<forall>t. t \<noteq> thread \<longrightarrow> (\<forall>d p. t \<notin> set (ready_queues s d p)) \<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); ekheap s thread' = Some x2\<rbrakk> \<Longrightarrow> (thread' \<notin> set (ready_queues s (tcb_domain x2) (tcb_priority x2)) \<longrightarrow> (\<forall>t. t \<noteq> thread \<longrightarrow> (\<forall>d p. (d = tcb_domain x2 \<and> p = tcb_priority x2 \<longrightarrow> t \<noteq> thread' \<and> t \<notin> set (ready_queues s (tcb_domain x2) (tcb_priority x2))) \<and> ((d = tcb_domain x2 \<longrightarrow> p \<noteq> tcb_priority x2) \<longrightarrow> t \<notin> set (ready_queues s d p))) \<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))) \<and> (thread' \<in> set (ready_queues s (tcb_domain x2) (tcb_priority x2)) \<longrightarrow> (\<forall>t. t \<noteq> thread \<longrightarrow> (\<forall>d p. (d = tcb_domain x2 \<and> p = tcb_priority x2 \<longrightarrow> t \<notin> set (ready_queues s (tcb_domain x2) (tcb_priority x2))) \<and> ((d = tcb_domain x2 \<longrightarrow> p \<noteq> tcb_priority x2) \<longrightarrow> t \<notin> set (ready_queues s d p))) \<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))) proof (prove)
goal (2 subgoals):
 1. \<And>s x2. \<lbrakk>\<forall>t. t \<noteq> thread \<longrightarrow> (\<forall>d p. t \<notin> set (ready_queues s d p)) \<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); ekheap s thread' = Some x2\<rbrakk> \<Longrightarrow> thread' \<notin> set (ready_queues s (tcb_domain x2) (tcb_priority x2)) \<longrightarrow> (\<forall>t. t \<noteq> thread \<longrightarrow> (\<forall>d p. (d = tcb_domain x2 \<and> p = tcb_priority x2 \<longrightarrow> t \<noteq> thread' \<and> t \<notin> set (ready_queues s (tcb_domain x2) (tcb_priority x2))) \<and> ((d = tcb_domain x2 \<longrightarrow> p \<noteq> tcb_priority x2) \<longrightarrow> t \<notin> set (ready_queues s d p))) \<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))
 2. \<And>s x2. \<lbrakk>\<forall>t. t \<noteq> thread \<longrightarrow> (\<forall>d p. t \<notin> set (ready_queues s d p)) \<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); ekheap s thread' = Some x2\<rbrakk> \<Longrightarrow> thread' \<in> set (ready_queues s (tcb_domain x2) (tcb_priority x2)) \<longrightarrow> (\<forall>t. t \<noteq> thread \<longrightarrow> (\<forall>d p. (d = tcb_domain x2 \<and> p = tcb_priority x2 \<longrightarrow> t \<notin> set (ready_queues s (tcb_domain x2) (tcb_priority x2))) \<and> ((d = tcb_domain x2 \<longrightarrow> p \<noteq> tcb_priority x2) \<longrightarrow> t \<notin> set (ready_queues s d p))) \<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)) proof (prove)
goal (2 subgoals):
 1. \<And>s x2 t st. \<lbrakk>\<forall>t. t \<noteq> thread \<longrightarrow> (\<forall>d p. t \<notin> set (ready_queues s d p)) \<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); ekheap s thread' = Some x2; thread' \<notin> set (ready_queues s (tcb_domain x2) (tcb_priority x2)); t \<noteq> thread; \<forall>d p. (d = tcb_domain x2 \<and> p = tcb_priority x2 \<longrightarrow> t \<noteq> thread' \<and> t \<notin> set (ready_queues s (tcb_domain x2) (tcb_priority x2))) \<and> ((d = tcb_domain x2 \<longrightarrow> p \<noteq> tcb_priority x2) \<longrightarrow> 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\<rbrakk> \<Longrightarrow> st \<noteq> Running \<and> st \<noteq> Restart
 2. \<And>s x2. \<lbrakk>\<forall>t. t \<noteq> thread \<longrightarrow> (\<forall>d p. t \<notin> set (ready_queues s d p)) \<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); ekheap s thread' = Some x2\<rbrakk> \<Longrightarrow> thread' \<in> set (ready_queues s (tcb_domain x2) (tcb_priority x2)) \<longrightarrow> (\<forall>t. t \<noteq> thread \<longrightarrow> (\<forall>d p. (d = tcb_domain x2 \<and> p = tcb_priority x2 \<longrightarrow> t \<notin> set (ready_queues s (tcb_domain x2) (tcb_priority x2))) \<and> ((d = tcb_domain x2 \<longrightarrow> p \<noteq> tcb_priority x2) \<longrightarrow> t \<notin> set (ready_queues s d p))) \<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)) proof (prove)
goal (3 subgoals):
 1. \<And>s x2 t st. \<lbrakk>\<forall>t. t \<noteq> thread \<longrightarrow> (\<forall>d p. t \<notin> set (ready_queues s d p)) \<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); ekheap s thread' = Some x2; thread' \<notin> set (ready_queues s (tcb_domain x2) (tcb_priority x2)); t \<noteq> thread; \<forall>d p. (d = tcb_domain x2 \<and> p = tcb_priority x2 \<longrightarrow> t \<noteq> thread' \<and> t \<notin> set (ready_queues s (tcb_domain x2) (tcb_priority x2))) \<and> ((d = tcb_domain x2 \<longrightarrow> p \<noteq> tcb_priority x2) \<longrightarrow> 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 = thread\<rbrakk> \<Longrightarrow> st \<noteq> Running \<and> st \<noteq> Restart
 2. \<And>s x2 t st. \<lbrakk>\<forall>t. t \<noteq> thread \<longrightarrow> (\<forall>d p. t \<notin> set (ready_queues s d p)) \<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); ekheap s thread' = Some x2; thread' \<notin> set (ready_queues s (tcb_domain x2) (tcb_priority x2)); t \<noteq> thread; \<forall>d p. (d = tcb_domain x2 \<and> p = tcb_priority x2 \<longrightarrow> t \<noteq> thread' \<and> t \<notin> set (ready_queues s (tcb_domain x2) (tcb_priority x2))) \<and> ((d = tcb_domain x2 \<longrightarrow> p \<noteq> tcb_priority x2) \<longrightarrow> 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\<rbrakk> \<Longrightarrow> st \<noteq> Running \<and> st \<noteq> Restart
 3. \<And>s x2. \<lbrakk>\<forall>t. t \<noteq> thread \<longrightarrow> (\<forall>d p. t \<notin> set (ready_queues s d p)) \<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); ekheap s thread' = Some x2\<rbrakk> \<Longrightarrow> thread' \<in> set (ready_queues s (tcb_domain x2) (tcb_priority x2)) \<longrightarrow> (\<forall>t. t \<noteq> thread \<longrightarrow> (\<forall>d p. (d = tcb_domain x2 \<and> p = tcb_priority x2 \<longrightarrow> t \<notin> set (ready_queues s (tcb_domain x2) (tcb_priority x2))) \<and> ((d = tcb_domain x2 \<longrightarrow> p \<noteq> tcb_priority x2) \<longrightarrow> t \<notin> set (ready_queues s d p))) \<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)) proof (prove)
goal (2 subgoals):
 1. \<And>s x2 t st. \<lbrakk>\<forall>t. t \<noteq> thread \<longrightarrow> (\<forall>d p. t \<notin> set (ready_queues s d p)) \<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); ekheap s thread' = Some x2; thread' \<notin> set (ready_queues s (tcb_domain x2) (tcb_priority x2)); t \<noteq> thread; \<forall>d p. (d = tcb_domain x2 \<and> p = tcb_priority x2 \<longrightarrow> t \<noteq> thread' \<and> t \<notin> set (ready_queues s (tcb_domain x2) (tcb_priority x2))) \<and> ((d = tcb_domain x2 \<longrightarrow> p \<noteq> tcb_priority x2) \<longrightarrow> 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\<rbrakk> \<Longrightarrow> st \<noteq> Running \<and> st \<noteq> Restart
 2. \<And>s x2. \<lbrakk>\<forall>t. t \<noteq> thread \<longrightarrow> (\<forall>d p. t \<notin> set (ready_queues s d p)) \<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); ekheap s thread' = Some x2\<rbrakk> \<Longrightarrow> thread' \<in> set (ready_queues s (tcb_domain x2) (tcb_priority x2)) \<longrightarrow> (\<forall>t. t \<noteq> thread \<longrightarrow> (\<forall>d p. (d = tcb_domain x2 \<and> p = tcb_priority x2 \<longrightarrow> t \<notin> set (ready_queues s (tcb_domain x2) (tcb_priority x2))) \<and> ((d = tcb_domain x2 \<longrightarrow> p \<noteq> tcb_priority x2) \<longrightarrow> t \<notin> set (ready_queues s d p))) \<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)) proof (prove)
goal (2 subgoals):
 1. \<And>s x2 t st. \<lbrakk>ekheap s thread' = Some x2; thread' \<notin> set (ready_queues s (tcb_domain x2) (tcb_priority x2)); t \<noteq> thread; \<forall>d p. (d = tcb_domain x2 \<and> p = tcb_priority x2 \<longrightarrow> t \<noteq> thread' \<and> t \<notin> set (ready_queues s (tcb_domain x2) (tcb_priority x2))) \<and> ((d = tcb_domain x2 \<longrightarrow> p \<noteq> tcb_priority x2) \<longrightarrow> 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; t \<noteq> thread \<longrightarrow> (\<forall>d p. t \<notin> set (ready_queues s d p)) \<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
 2. \<And>s x2. \<lbrakk>\<forall>t. t \<noteq> thread \<longrightarrow> (\<forall>d p. t \<notin> set (ready_queues s d p)) \<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); ekheap s thread' = Some x2\<rbrakk> \<Longrightarrow> thread' \<in> set (ready_queues s (tcb_domain x2) (tcb_priority x2)) \<longrightarrow> (\<forall>t. t \<noteq> thread \<longrightarrow> (\<forall>d p. (d = tcb_domain x2 \<and> p = tcb_priority x2 \<longrightarrow> t \<notin> set (ready_queues s (tcb_domain x2) (tcb_priority x2))) \<and> ((d = tcb_domain x2 \<longrightarrow> p \<noteq> tcb_priority x2) \<longrightarrow> t \<notin> set (ready_queues s d p))) \<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)) proof (prove)
goal (2 subgoals):
 1. \<And>s x2 t st. \<lbrakk>ekheap s thread' = Some x2; thread' \<notin> set (ready_queues s (tcb_domain x2) (tcb_priority x2)); \<forall>d p. (d = tcb_domain x2 \<and> p = tcb_priority x2 \<longrightarrow> t \<noteq> thread' \<and> t \<notin> set (ready_queues s (tcb_domain x2) (tcb_priority x2))) \<and> ((d = tcb_domain x2 \<longrightarrow> p \<noteq> tcb_priority x2) \<longrightarrow> 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; (\<forall>d p. t \<notin> set (ready_queues s d p)) \<longrightarrow> (\<forall>st. st_tcb_at ((=) st) t s \<longrightarrow> st \<noteq> Running \<and> st \<noteq> Restart)\<rbrakk> \<Longrightarrow> st \<noteq> Running \<and> st \<noteq> Restart
 2. \<And>s x2. \<lbrakk>\<forall>t. t \<noteq> thread \<longrightarrow> (\<forall>d p. t \<notin> set (ready_queues s d p)) \<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); ekheap s thread' = Some x2\<rbrakk> \<Longrightarrow> thread' \<in> set (ready_queues s (tcb_domain x2) (tcb_priority x2)) \<longrightarrow> (\<forall>t. t \<noteq> thread \<longrightarrow> (\<forall>d p. (d = tcb_domain x2 \<and> p = tcb_priority x2 \<longrightarrow> t \<notin> set (ready_queues s (tcb_domain x2) (tcb_priority x2))) \<and> ((d = tcb_domain x2 \<longrightarrow> p \<noteq> tcb_priority x2) \<longrightarrow> t \<notin> set (ready_queues s d p))) \<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)) proof (prove)
goal (1 subgoal):
 1. \<And>s x2. \<lbrakk>\<forall>t. t \<noteq> thread \<longrightarrow> (\<forall>d p. t \<notin> set (ready_queues s d p)) \<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); ekheap s thread' = Some x2\<rbrakk> \<Longrightarrow> thread' \<in> set (ready_queues s (tcb_domain x2) (tcb_priority x2)) \<longrightarrow> (\<forall>t. t \<noteq> thread \<longrightarrow> (\<forall>d p. (d = tcb_domain x2 \<and> p = tcb_priority x2 \<longrightarrow> t \<notin> set (ready_queues s (tcb_domain x2) (tcb_priority x2))) \<and> ((d = tcb_domain x2 \<longrightarrow> p \<noteq> tcb_priority x2) \<longrightarrow> t \<notin> set (ready_queues s d p))) \<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)) proof (prove)
goal (1 subgoal):
 1. \<And>s x2 t st. \<lbrakk>\<forall>t. t \<noteq> thread \<longrightarrow> (\<forall>d p. t \<notin> set (ready_queues s d p)) \<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); ekheap s thread' = Some x2; thread' \<in> set (ready_queues s (tcb_domain x2) (tcb_priority x2)); t \<noteq> thread; \<forall>d p. (d = tcb_domain x2 \<and> p = tcb_priority x2 \<longrightarrow> t \<notin> set (ready_queues s (tcb_domain x2) (tcb_priority x2))) \<and> ((d = tcb_domain x2 \<longrightarrow> p \<noteq> tcb_priority x2) \<longrightarrow> 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\<rbrakk> \<Longrightarrow> st \<noteq> Running \<and> st \<noteq> Restart proof (prove)
goal (2 subgoals):
 1. \<And>s x2 t st. \<lbrakk>\<forall>t. t \<noteq> thread \<longrightarrow> (\<forall>d p. t \<notin> set (ready_queues s d p)) \<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); ekheap s thread' = Some x2; thread' \<in> set (ready_queues s (tcb_domain x2) (tcb_priority x2)); t \<noteq> thread; \<forall>d p. (d = tcb_domain x2 \<and> p = tcb_priority x2 \<longrightarrow> t \<notin> set (ready_queues s (tcb_domain x2) (tcb_priority x2))) \<and> ((d = tcb_domain x2 \<longrightarrow> p \<noteq> tcb_priority x2) \<longrightarrow> 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 = thread\<rbrakk> \<Longrightarrow> st \<noteq> Running \<and> st \<noteq> Restart
 2. \<And>s x2 t st. \<lbrakk>\<forall>t. t \<noteq> thread \<longrightarrow> (\<forall>d p. t \<notin> set (ready_queues s d p)) \<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); ekheap s thread' = Some x2; thread' \<in> set (ready_queues s (tcb_domain x2) (tcb_priority x2)); t \<noteq> thread; \<forall>d p. (d = tcb_domain x2 \<and> p = tcb_priority x2 \<longrightarrow> t \<notin> set (ready_queues s (tcb_domain x2) (tcb_priority x2))) \<and> ((d = tcb_domain x2 \<longrightarrow> p \<noteq> tcb_priority x2) \<longrightarrow> 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\<rbrakk> \<Longrightarrow> st \<noteq> Running \<and> st \<noteq> Restart proof (prove)
goal (1 subgoal):
 1. \<And>s x2 t st. \<lbrakk>\<forall>t. t \<noteq> thread \<longrightarrow> (\<forall>d p. t \<notin> set (ready_queues s d p)) \<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); ekheap s thread' = Some x2; thread' \<in> set (ready_queues s (tcb_domain x2) (tcb_priority x2)); t \<noteq> thread; \<forall>d p. (d = tcb_domain x2 \<and> p = tcb_priority x2 \<longrightarrow> t \<notin> set (ready_queues s (tcb_domain x2) (tcb_priority x2))) \<and> ((d = tcb_domain x2 \<longrightarrow> p \<noteq> tcb_priority x2) \<longrightarrow> 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\<rbrakk> \<Longrightarrow> st \<noteq> Running \<and> st \<noteq> Restart proof (prove)
goal (1 subgoal):
 1. \<And>s x2 t st. \<lbrakk>ekheap s thread' = Some x2; thread' \<in> set (ready_queues s (tcb_domain x2) (tcb_priority x2)); t \<noteq> thread; \<forall>d p. (d = tcb_domain x2 \<and> p = tcb_priority x2 \<longrightarrow> t \<notin> set (ready_queues s (tcb_domain x2) (tcb_priority x2))) \<and> ((d = tcb_domain x2 \<longrightarrow> p \<noteq> tcb_priority x2) \<longrightarrow> 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; t \<noteq> thread \<longrightarrow> (\<forall>d p. t \<notin> set (ready_queues s d p)) \<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 (1 subgoal):
 1. \<And>s x2 t st. \<lbrakk>ekheap s thread' = Some x2; thread' \<in> set (ready_queues s (tcb_domain x2) (tcb_priority x2)); \<forall>d p. (d = tcb_domain x2 \<and> p = tcb_priority x2 \<longrightarrow> t \<notin> set (ready_queues s (tcb_domain x2) (tcb_priority x2))) \<and> ((d = tcb_domain x2 \<longrightarrow> p \<noteq> tcb_priority x2) \<longrightarrow> 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; (\<forall>d p. t \<notin> set (ready_queues s d p)) \<longrightarrow> (\<forall>st. st_tcb_at ((=) st) t s \<longrightarrow> st \<noteq> Running \<and> st \<noteq> Restart)\<rbrakk> \<Longrightarrow> st \<noteq> Running \<and> st \<noteq> Restart proof (prove)
goal:
No subgoals!