theory DetSchedSchedule_AI

lemma tcb_sched_action_enqueue_valid_blocked:
  "\<lbrace>valid_blocked_except thread\<rbrace>
     tcb_sched_action tcb_sched_enqueue thread
   \<lbrace>\<lambda>_. valid_blocked\<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\<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 (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. (\<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. (\<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. (\<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. (\<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)); \<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. (\<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)); \<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)); \<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. (\<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)); \<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. (\<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; 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. (\<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 \<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. (\<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. (\<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)); \<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)); \<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)); \<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)); \<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)); \<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!