theory DetSchedSchedule_AI

lemma invoke_domain_valid_sched[wp]:
  "\<lbrace>valid_sched and tcb_at t and (\<lambda>s. t \<noteq> idle_thread s)
                and simple_sched_action and valid_idle\<rbrace>
    invoke_domain t d \<lbrace>\<lambda>_. valid_sched\<rbrace>" apply (simp add: invoke_domain_def) apply wp apply (simp add: set_domain_def thread_set_domain_def) apply (wp gts_st_tcb_at hoare_vcg_if_lift hoare_vcg_if_lift2 hoare_vcg_imp_lift
             hoare_vcg_disj_lift ethread_set_not_queued_valid_queues reschedule_required_valid_sched
             tcb_sched_action_enqueue_valid_blocked ethread_set_valid_blocked_except
             ethread_set_valid_blocked ethread_set_ssa_valid_sched_action
             ethread_set_not_cur_ct_in_cur_domain ethread_set_not_idle_valid_sched
             ethread_set_not_idle_valid_idle_etcb) apply (wp hoare_weak_lift_imp hoare_weak_lift_imp_conj tcb_dequeue_not_queued tcb_sched_action_dequeue_valid_blocked_except) apply simp apply (wp hoare_vcg_disj_lift) apply (rule_tac Q="\<lambda>_. valid_sched and not_queued t and valid_idle and (\<lambda>s. t \<noteq> idle_thread s)" in hoare_strengthen_post) apply (wp tcb_sched_action_dequeue_valid_sched_not_runnable tcb_dequeue_not_queued) apply (simp add: valid_sched_def valid_sched_action_def) apply simp apply (wp hoare_vcg_disj_lift tcb_dequeue_not_queued tcb_sched_action_dequeue_valid_blocked_except
              tcb_sched_action_dequeue_valid_sched_not_runnable)+ apply (clarsimp simp: valid_sched_def not_cur_thread_def valid_sched_action_def not_pred_tcb) apply (auto simp: st_tcb_def2 tcb_at_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>valid_sched and tcb_at t and (\<lambda>s. t \<noteq> idle_thread s) and simple_sched_action and valid_idle\<rbrace> invoke_domain t d \<lbrace>\<lambda>_. valid_sched\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>valid_sched and tcb_at t and (\<lambda>s. t \<noteq> idle_thread s) and simple_sched_action and valid_idle\<rbrace> liftE (do y <- set_domain t d;
return []
od) \<lbrace>\<lambda>_. valid_sched\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<lbrace>?Q\<rbrace> set_domain t d \<lbrace>\<lambda>y. valid_sched\<rbrace>
 2. \<And>s. (valid_sched and tcb_at t and (\<lambda>s. t \<noteq> idle_thread s) and simple_sched_action and valid_idle) s \<Longrightarrow> ?Q s proof (prove)
goal (2 subgoals):
 1. \<lbrace>?Q\<rbrace> do cur <- gets cur_thread;
y <- tcb_sched_action tcb_sched_dequeue t;
y <- ethread_set (tcb_domain_update (\<lambda>_. d)) t;
ts <- get_thread_state t;
y <- when (runnable ts) (tcb_sched_action tcb_sched_enqueue t);
when (t = cur) reschedule_required
od \<lbrace>\<lambda>y. valid_sched\<rbrace>
 2. \<And>s. (valid_sched and tcb_at t and (\<lambda>s. t \<noteq> idle_thread s) and simple_sched_action and valid_idle) s \<Longrightarrow> ?Q s proof (prove)
goal (5 subgoals):
 1. \<And>cur. \<lbrace>?P'128 cur\<rbrace> tcb_sched_action tcb_sched_dequeue t \<lbrace>\<lambda>rv s. not_queued t s \<and> st_tcb_at runnable t s \<and> weak_valid_sched_action s \<and> valid_blocked_except t s \<and> (valid_idle_etcb and valid_idle and (\<lambda>s. t \<noteq> idle_thread s)) s\<rbrace>
 2. \<And>cur. \<lbrace>?P'122 cur\<rbrace> tcb_sched_action tcb_sched_dequeue t \<lbrace>\<lambda>rv s. st_tcb_at (\<lambda>rv. \<not> \<not> runnable rv) t s \<or> valid_etcbs s \<and> (valid_queues and not_queued t) s \<and> weak_valid_sched_action s \<and> valid_blocked s \<and> (valid_idle_etcb and valid_idle and (\<lambda>s. t \<noteq> idle_thread s)) s\<rbrace>
 3. \<And>cur. \<lbrace>?P'119 cur\<rbrace> tcb_sched_action tcb_sched_dequeue t \<lbrace>\<lambda>rv s. st_tcb_at (\<lambda>rv. \<not> t \<noteq> cur) t s \<or> (st_tcb_at (\<lambda>rv. \<not> runnable rv) t s \<or> valid_etcbs s \<and> (valid_queues and not_queued t) s \<and> ct_not_in_q s \<and> (valid_sched_action and simple_sched_action) s \<and> (ct_in_cur_domain and not_cur_thread t) s \<and> (valid_idle_etcb and valid_idle and (\<lambda>s. t \<noteq> idle_thread s)) s \<and> st_tcb_at runnable t s \<and> not_cur_thread t s \<and> valid_blocked_except t s) \<and> (st_tcb_at (\<lambda>rv. \<not> \<not> runnable rv) t s \<or> (valid_sched and simple_sched_action and not_queued t and (\<lambda>s. t \<noteq> cur_thread s) and (\<lambda>s. t \<noteq> idle_thread s) and valid_idle) s)\<rbrace>
 4. \<lbrace>?Q\<rbrace> gets cur_thread \<lbrace>\<lambda>cur s. (st_tcb_at (\<lambda>rv. t \<noteq> cur) t s \<or> (st_tcb_at (\<lambda>rv. \<not> runnable rv) t s \<or> valid_etcbs s \<and> valid_queues s \<and> ?P'128 cur s) \<and> ?P'122 cur s) \<and> ?P'119 cur s\<rbrace>
 5. \<And>s. (valid_sched and tcb_at t and (\<lambda>s. t \<noteq> idle_thread s) and simple_sched_action and valid_idle) s \<Longrightarrow> ?Q s proof (prove)
goal (4 subgoals):
 1. \<And>cur. \<lbrace>?P'122 cur\<rbrace> tcb_sched_action tcb_sched_dequeue t \<lbrace>\<lambda>rv s. st_tcb_at (\<lambda>rv. \<not> \<not> runnable rv) t s \<or> valid_etcbs s \<and> (valid_queues and not_queued t) s \<and> weak_valid_sched_action s \<and> valid_blocked s \<and> (valid_idle_etcb and valid_idle and (\<lambda>s. t \<noteq> idle_thread s)) s\<rbrace>
 2. \<And>cur. \<lbrace>?P'119 cur\<rbrace> tcb_sched_action tcb_sched_dequeue t \<lbrace>\<lambda>rv s. st_tcb_at (\<lambda>rv. \<not> t \<noteq> cur) t s \<or> (st_tcb_at (\<lambda>rv. \<not> runnable rv) t s \<or> valid_etcbs s \<and> (valid_queues and not_queued t) s \<and> ct_not_in_q s \<and> (valid_sched_action and simple_sched_action) s \<and> (ct_in_cur_domain and not_cur_thread t) s \<and> (valid_idle_etcb and valid_idle and (\<lambda>s. t \<noteq> idle_thread s)) s \<and> st_tcb_at runnable t s \<and> not_cur_thread t s \<and> valid_blocked_except t s) \<and> (st_tcb_at (\<lambda>rv. \<not> \<not> runnable rv) t s \<or> (valid_sched and simple_sched_action and not_queued t and (\<lambda>s. t \<noteq> cur_thread s) and (\<lambda>s. t \<noteq> idle_thread s) and valid_idle) s)\<rbrace>
 3. \<lbrace>?Q\<rbrace> gets cur_thread \<lbrace>\<lambda>cur s. (st_tcb_at (\<lambda>rv. t \<noteq> cur) t s \<or> (st_tcb_at (\<lambda>rv. \<not> runnable rv) t s \<or> valid_etcbs s \<and> valid_queues s \<and> valid_queues s \<and> st_tcb_at runnable t s \<and> weak_valid_sched_action s \<and> valid_blocked s \<and> valid_idle_etcb s \<and> valid_idle s \<and> t \<noteq> idle_thread s) \<and> ?P'122 cur s) \<and> ?P'119 cur s\<rbrace>
 4. \<And>s. (valid_sched and tcb_at t and (\<lambda>s. t \<noteq> idle_thread s) and simple_sched_action and valid_idle) s \<Longrightarrow> ?Q s proof (prove)
goal (4 subgoals):
 1. \<And>cur. \<lbrace>?P'122 cur\<rbrace> tcb_sched_action tcb_sched_dequeue t \<lbrace>\<lambda>rv s. st_tcb_at runnable t s \<or> valid_etcbs s \<and> valid_queues s \<and> not_queued t s \<and> weak_valid_sched_action s \<and> valid_blocked s \<and> valid_idle_etcb s \<and> valid_idle s \<and> t \<noteq> idle_thread s\<rbrace>
 2. \<And>cur. \<lbrace>?P'119 cur\<rbrace> tcb_sched_action tcb_sched_dequeue t \<lbrace>\<lambda>rv s. st_tcb_at (\<lambda>rv. \<not> t \<noteq> cur) t s \<or> (st_tcb_at (\<lambda>rv. \<not> runnable rv) t s \<or> valid_etcbs s \<and> (valid_queues and not_queued t) s \<and> ct_not_in_q s \<and> (valid_sched_action and simple_sched_action) s \<and> (ct_in_cur_domain and not_cur_thread t) s \<and> (valid_idle_etcb and valid_idle and (\<lambda>s. t \<noteq> idle_thread s)) s \<and> st_tcb_at runnable t s \<and> not_cur_thread t s \<and> valid_blocked_except t s) \<and> (st_tcb_at (\<lambda>rv. \<not> \<not> runnable rv) t s \<or> (valid_sched and simple_sched_action and not_queued t and (\<lambda>s. t \<noteq> cur_thread s) and (\<lambda>s. t \<noteq> idle_thread s) and valid_idle) s)\<rbrace>
 3. \<lbrace>?Q\<rbrace> gets cur_thread \<lbrace>\<lambda>cur s. (st_tcb_at (\<lambda>rv. t \<noteq> cur) t s \<or> (st_tcb_at (\<lambda>rv. \<not> runnable rv) t s \<or> valid_etcbs s \<and> valid_queues s \<and> valid_queues s \<and> st_tcb_at runnable t s \<and> weak_valid_sched_action s \<and> valid_blocked s \<and> valid_idle_etcb s \<and> valid_idle s \<and> t \<noteq> idle_thread s) \<and> ?P'122 cur s) \<and> ?P'119 cur s\<rbrace>
 4. \<And>s. (valid_sched and tcb_at t and (\<lambda>s. t \<noteq> idle_thread s) and simple_sched_action and valid_idle) s \<Longrightarrow> ?Q s proof (prove)
goal (4 subgoals):
 1. \<And>cur. \<lbrace>?P'153 cur\<rbrace> tcb_sched_action tcb_sched_dequeue t \<lbrace>\<lambda>rv s. not_queued t s \<and> weak_valid_sched_action s \<and> valid_blocked s \<and> valid_idle_etcb s \<and> valid_idle s \<and> t \<noteq> idle_thread s\<rbrace>
 2. \<And>cur. \<lbrace>?P'119 cur\<rbrace> tcb_sched_action tcb_sched_dequeue t \<lbrace>\<lambda>rv s. st_tcb_at (\<lambda>rv. \<not> t \<noteq> cur) t s \<or> (st_tcb_at (\<lambda>rv. \<not> runnable rv) t s \<or> valid_etcbs s \<and> (valid_queues and not_queued t) s \<and> ct_not_in_q s \<and> (valid_sched_action and simple_sched_action) s \<and> (ct_in_cur_domain and not_cur_thread t) s \<and> (valid_idle_etcb and valid_idle and (\<lambda>s. t \<noteq> idle_thread s)) s \<and> st_tcb_at runnable t s \<and> not_cur_thread t s \<and> valid_blocked_except t s) \<and> (st_tcb_at (\<lambda>rv. \<not> \<not> runnable rv) t s \<or> (valid_sched and simple_sched_action and not_queued t and (\<lambda>s. t \<noteq> cur_thread s) and (\<lambda>s. t \<noteq> idle_thread s) and valid_idle) s)\<rbrace>
 3. \<lbrace>?Q\<rbrace> gets cur_thread \<lbrace>\<lambda>cur s. (st_tcb_at (\<lambda>rv. t \<noteq> cur) t s \<or> (st_tcb_at (\<lambda>rv. \<not> runnable rv) t s \<or> valid_etcbs s \<and> valid_queues s \<and> valid_queues s \<and> st_tcb_at runnable t s \<and> weak_valid_sched_action s \<and> valid_blocked s \<and> valid_idle_etcb s \<and> valid_idle s \<and> t \<noteq> idle_thread s) \<and> (st_tcb_at runnable t s \<or> valid_etcbs s \<and> valid_queues s \<and> ?P'153 cur s)) \<and> ?P'119 cur s\<rbrace>
 4. \<And>s. (valid_sched and tcb_at t and (\<lambda>s. t \<noteq> idle_thread s) and simple_sched_action and valid_idle) s \<Longrightarrow> ?Q s proof (prove)
goal (5 subgoals):
 1. \<And>cur. \<lbrace>?P'153 cur\<rbrace> tcb_sched_action tcb_sched_dequeue t \<lbrace>\<lambda>_. valid_sched and not_queued t and valid_idle and (\<lambda>s. t \<noteq> idle_thread s)\<rbrace>
 2. \<And>cur rv s. (valid_sched and not_queued t and valid_idle and (\<lambda>s. t \<noteq> idle_thread s)) s \<Longrightarrow> not_queued t s \<and> weak_valid_sched_action s \<and> valid_blocked s \<and> valid_idle_etcb s \<and> valid_idle s \<and> t \<noteq> idle_thread s
 3. \<And>cur. \<lbrace>?P'119 cur\<rbrace> tcb_sched_action tcb_sched_dequeue t \<lbrace>\<lambda>rv s. st_tcb_at (\<lambda>rv. \<not> t \<noteq> cur) t s \<or> (st_tcb_at (\<lambda>rv. \<not> runnable rv) t s \<or> valid_etcbs s \<and> (valid_queues and not_queued t) s \<and> ct_not_in_q s \<and> (valid_sched_action and simple_sched_action) s \<and> (ct_in_cur_domain and not_cur_thread t) s \<and> (valid_idle_etcb and valid_idle and (\<lambda>s. t \<noteq> idle_thread s)) s \<and> st_tcb_at runnable t s \<and> not_cur_thread t s \<and> valid_blocked_except t s) \<and> (st_tcb_at (\<lambda>rv. \<not> \<not> runnable rv) t s \<or> (valid_sched and simple_sched_action and not_queued t and (\<lambda>s. t \<noteq> cur_thread s) and (\<lambda>s. t \<noteq> idle_thread s) and valid_idle) s)\<rbrace>
 4. \<lbrace>?Q\<rbrace> gets cur_thread \<lbrace>\<lambda>cur s. (st_tcb_at (\<lambda>rv. t \<noteq> cur) t s \<or> (st_tcb_at (\<lambda>rv. \<not> runnable rv) t s \<or> valid_etcbs s \<and> valid_queues s \<and> valid_queues s \<and> st_tcb_at runnable t s \<and> weak_valid_sched_action s \<and> valid_blocked s \<and> valid_idle_etcb s \<and> valid_idle s \<and> t \<noteq> idle_thread s) \<and> (st_tcb_at runnable t s \<or> valid_etcbs s \<and> valid_queues s \<and> ?P'153 cur s)) \<and> ?P'119 cur s\<rbrace>
 5. \<And>s. (valid_sched and tcb_at t and (\<lambda>s. t \<noteq> idle_thread s) and simple_sched_action and valid_idle) s \<Longrightarrow> ?Q s proof (prove)
goal (4 subgoals):
 1. \<And>cur rv s. (valid_sched and not_queued t and valid_idle and (\<lambda>s. t \<noteq> idle_thread s)) s \<Longrightarrow> not_queued t s \<and> weak_valid_sched_action s \<and> valid_blocked s \<and> valid_idle_etcb s \<and> valid_idle s \<and> t \<noteq> idle_thread s
 2. \<And>cur. \<lbrace>?P'119 cur\<rbrace> tcb_sched_action tcb_sched_dequeue t \<lbrace>\<lambda>rv s. st_tcb_at (\<lambda>rv. \<not> t \<noteq> cur) t s \<or> (st_tcb_at (\<lambda>rv. \<not> runnable rv) t s \<or> valid_etcbs s \<and> (valid_queues and not_queued t) s \<and> ct_not_in_q s \<and> (valid_sched_action and simple_sched_action) s \<and> (ct_in_cur_domain and not_cur_thread t) s \<and> (valid_idle_etcb and valid_idle and (\<lambda>s. t \<noteq> idle_thread s)) s \<and> st_tcb_at runnable t s \<and> not_cur_thread t s \<and> valid_blocked_except t s) \<and> (st_tcb_at (\<lambda>rv. \<not> \<not> runnable rv) t s \<or> (valid_sched and simple_sched_action and not_queued t and (\<lambda>s. t \<noteq> cur_thread s) and (\<lambda>s. t \<noteq> idle_thread s) and valid_idle) s)\<rbrace>
 3. \<lbrace>?Q\<rbrace> gets cur_thread \<lbrace>\<lambda>cur s. (st_tcb_at (\<lambda>rv. t \<noteq> cur) t s \<or> (st_tcb_at (\<lambda>rv. \<not> runnable rv) t s \<or> valid_etcbs s \<and> valid_queues s \<and> valid_queues s \<and> st_tcb_at runnable t s \<and> weak_valid_sched_action s \<and> valid_blocked s \<and> valid_idle_etcb s \<and> valid_idle s \<and> t \<noteq> idle_thread s) \<and> (st_tcb_at runnable t s \<or> valid_etcbs s \<and> valid_queues s \<and> (valid_sched and st_tcb_at (\<lambda>st. \<not> active st) t) s \<and> valid_queues s \<and> valid_idle s \<and> t \<noteq> idle_thread s)) \<and> ?P'119 cur s\<rbrace>
 4. \<And>s. (valid_sched and tcb_at t and (\<lambda>s. t \<noteq> idle_thread s) and simple_sched_action and valid_idle) s \<Longrightarrow> ?Q s proof (prove)
goal (3 subgoals):
 1. \<And>cur. \<lbrace>?P'119 cur\<rbrace> tcb_sched_action tcb_sched_dequeue t \<lbrace>\<lambda>rv s. st_tcb_at (\<lambda>rv. \<not> t \<noteq> cur) t s \<or> (st_tcb_at (\<lambda>rv. \<not> runnable rv) t s \<or> valid_etcbs s \<and> (valid_queues and not_queued t) s \<and> ct_not_in_q s \<and> (valid_sched_action and simple_sched_action) s \<and> (ct_in_cur_domain and not_cur_thread t) s \<and> (valid_idle_etcb and valid_idle and (\<lambda>s. t \<noteq> idle_thread s)) s \<and> st_tcb_at runnable t s \<and> not_cur_thread t s \<and> valid_blocked_except t s) \<and> (st_tcb_at (\<lambda>rv. \<not> \<not> runnable rv) t s \<or> (valid_sched and simple_sched_action and not_queued t and (\<lambda>s. t \<noteq> cur_thread s) and (\<lambda>s. t \<noteq> idle_thread s) and valid_idle) s)\<rbrace>
 2. \<lbrace>?Q\<rbrace> gets cur_thread \<lbrace>\<lambda>cur s. (st_tcb_at (\<lambda>rv. t \<noteq> cur) t s \<or> (st_tcb_at (\<lambda>rv. \<not> runnable rv) t s \<or> valid_etcbs s \<and> valid_queues s \<and> valid_queues s \<and> st_tcb_at runnable t s \<and> weak_valid_sched_action s \<and> valid_blocked s \<and> valid_idle_etcb s \<and> valid_idle s \<and> t \<noteq> idle_thread s) \<and> (st_tcb_at runnable t s \<or> valid_etcbs s \<and> valid_queues s \<and> (valid_sched and st_tcb_at (\<lambda>st. \<not> active st) t) s \<and> valid_queues s \<and> valid_idle s \<and> t \<noteq> idle_thread s)) \<and> ?P'119 cur s\<rbrace>
 3. \<And>s. (valid_sched and tcb_at t and (\<lambda>s. t \<noteq> idle_thread s) and simple_sched_action and valid_idle) s \<Longrightarrow> ?Q s proof (prove)
goal (3 subgoals):
 1. \<And>cur. \<lbrace>?P'119 cur\<rbrace> tcb_sched_action tcb_sched_dequeue t \<lbrace>\<lambda>rv s. st_tcb_at (\<lambda>rv. t = cur) t s \<or> (st_tcb_at (\<lambda>rv. \<not> runnable rv) t s \<or> valid_etcbs s \<and> valid_queues s \<and> not_queued t s \<and> ct_not_in_q s \<and> valid_sched_action s \<and> simple_sched_action s \<and> ct_in_cur_domain s \<and> not_cur_thread t s \<and> valid_idle_etcb s \<and> valid_idle s \<and> t \<noteq> idle_thread s \<and> st_tcb_at runnable t s \<and> not_cur_thread t s \<and> valid_blocked_except t s) \<and> (st_tcb_at runnable t s \<or> valid_sched s \<and> simple_sched_action s \<and> not_queued t s \<and> t \<noteq> cur_thread s \<and> t \<noteq> idle_thread s \<and> valid_idle s)\<rbrace>
 2. \<lbrace>?Q\<rbrace> gets cur_thread \<lbrace>\<lambda>cur s. (st_tcb_at (\<lambda>rv. t \<noteq> cur) t s \<or> (st_tcb_at (\<lambda>rv. \<not> runnable rv) t s \<or> valid_etcbs s \<and> valid_queues s \<and> valid_queues s \<and> st_tcb_at runnable t s \<and> weak_valid_sched_action s \<and> valid_blocked s \<and> valid_idle_etcb s \<and> valid_idle s \<and> t \<noteq> idle_thread s) \<and> (st_tcb_at runnable t s \<or> valid_etcbs s \<and> valid_queues s \<and> (valid_sched and st_tcb_at (\<lambda>st. \<not> active st) t) s \<and> valid_queues s \<and> valid_idle s \<and> t \<noteq> idle_thread s)) \<and> ?P'119 cur s\<rbrace>
 3. \<And>s. (valid_sched and tcb_at t and (\<lambda>s. t \<noteq> idle_thread s) and simple_sched_action and valid_idle) s \<Longrightarrow> ?Q s proof (prove)
goal (1 subgoal):
 1. \<And>s. (valid_sched and tcb_at t and (\<lambda>s. t \<noteq> idle_thread s) and simple_sched_action and valid_idle) s \<Longrightarrow> (st_tcb_at (\<lambda>rv. t \<noteq> cur_thread s) t s \<or> (st_tcb_at (\<lambda>rv. \<not> runnable rv) t s \<or> valid_etcbs s \<and> valid_queues s \<and> valid_queues s \<and> st_tcb_at runnable t s \<and> weak_valid_sched_action s \<and> valid_blocked s \<and> valid_idle_etcb s \<and> valid_idle s \<and> t \<noteq> idle_thread s) \<and> (st_tcb_at runnable t s \<or> valid_etcbs s \<and> valid_queues s \<and> (valid_sched and st_tcb_at (\<lambda>st. \<not> active st) t) s \<and> valid_queues s \<and> valid_idle s \<and> t \<noteq> idle_thread s)) \<and> (st_tcb_at (\<lambda>rv. t = cur_thread s) t s \<or> (st_tcb_at (\<lambda>rv. \<not> runnable rv) t s \<or> valid_etcbs s \<and> valid_queues s \<and> valid_queues s \<and> ct_not_in_q s \<and> valid_sched_action s \<and> simple_sched_action s \<and> ct_in_cur_domain s \<and> not_cur_thread t s \<and> valid_idle_etcb s \<and> valid_idle s \<and> t \<noteq> idle_thread s \<and> st_tcb_at runnable t s \<and> not_cur_thread t s \<and> valid_blocked s) \<and> (st_tcb_at runnable t s \<or> (valid_sched and st_tcb_at (\<lambda>st. \<not> active st) t) s \<and> simple_sched_action s \<and> valid_queues s \<and> t \<noteq> cur_thread s \<and> t \<noteq> idle_thread s \<and> valid_idle s)) proof (prove)
goal (1 subgoal):
 1. \<And>s. \<lbrakk>valid_etcbs s; valid_queues s; ct_not_in_q s; is_activatable (cur_thread s) s; weak_valid_sched_action s; switch_in_cur_domain s; ct_in_cur_domain s; valid_blocked s; valid_idle_etcb s; tcb_at t s; t \<noteq> idle_thread s; simple_sched_action s; valid_idle s\<rbrakk> \<Longrightarrow> (st_tcb_at (\<lambda>rv. t \<noteq> cur_thread s) t s \<or> (st_tcb_at (\<lambda>rv. \<not> runnable rv) t s \<or> st_tcb_at runnable t s) \<and> (st_tcb_at runnable t s \<or> st_tcb_at (\<lambda>st. st \<noteq> Running \<and> st \<noteq> Restart) t s)) \<and> (st_tcb_at (\<lambda>rv. t = cur_thread s) t s \<or> (st_tcb_at (\<lambda>rv. \<not> runnable rv) t s \<or> (scheduler_action s = resume_cur_thread \<longrightarrow> t \<noteq> cur_thread s) \<and> st_tcb_at runnable t s \<and> (scheduler_action s = resume_cur_thread \<longrightarrow> t \<noteq> cur_thread s)) \<and> (st_tcb_at runnable t s \<or> st_tcb_at (\<lambda>st. st \<noteq> Running \<and> st \<noteq> Restart) t s \<and> t \<noteq> cur_thread s)) proof (prove)
goal:
No subgoals!