theory ADT_IF

lemma choose_thread_guarded_pas_domain:
  "\<lbrace>pas_refined aag and valid_queues\<rbrace>
   choose_thread
   \<lbrace>\<lambda>_. guarded_pas_domain aag\<rbrace>" apply (simp add: choose_thread_def guarded_switch_to_def
         | wp switch_to_thread_respects switch_to_idle_thread_respects
              gts_wp switch_to_thread_guarded_pas_domain)+ apply (clarsimp simp: pas_refined_def) apply (clarsimp simp: tcb_domain_map_wellformed_aux_def) apply (erule_tac x="(hd (max_non_empty_queue (ready_queues s (cur_domain s))), cur_domain s)"
                in ballE) apply simp apply (clarsimp simp: valid_queues_def is_etcb_at_def) apply (erule_tac x="cur_domain s" in allE) apply (erule_tac x="Max {prio. ready_queues s (cur_domain s) prio \<noteq> []}" in allE) apply clarsimp apply (erule_tac x="hd (max_non_empty_queue (ready_queues s (cur_domain s)))" in ballE) apply (clarsimp) apply (erule notE, rule domtcbs) apply force apply (simp add: etcb_at_def) apply (simp add: max_non_empty_queue_def) apply (erule_tac P="hd A \<in> B" for A B in notE) apply (rule Max_prop) apply force+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>pas_refined aag and valid_queues\<rbrace> choose_thread \<lbrace>\<lambda>_. guarded_pas_domain aag\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s. pas_refined aag s \<and> valid_queues s \<Longrightarrow> (\<exists>prio. ready_queues s (cur_domain s) prio \<noteq> []) \<longrightarrow> (\<forall>st. st_tcb_at ((=) st) (hd (max_non_empty_queue (ready_queues s (cur_domain s)))) s \<longrightarrow> runnable st \<longrightarrow> pasObjectAbs aag (hd (max_non_empty_queue (ready_queues s (cur_domain s)))) \<in> pasDomainAbs aag (cur_domain s)) proof (prove)
goal (1 subgoal):
 1. \<And>s prio st. \<lbrakk>pas_wellformed aag; irq_map_wellformed aag s; tcb_domain_map_wellformed aag s; state_objs_in_policy aag s; state_asids_to_policy aag s \<subseteq> pasPolicy aag; state_irqs_to_policy aag s \<subseteq> pasPolicy aag; valid_queues s; ready_queues s (cur_domain s) prio \<noteq> []; st_tcb_at ((=) st) (hd (max_non_empty_queue (ready_queues s (cur_domain s)))) s; runnable st\<rbrakk> \<Longrightarrow> pasObjectAbs aag (hd (max_non_empty_queue (ready_queues s (cur_domain s)))) \<in> pasDomainAbs aag (cur_domain s) proof (prove)
goal (1 subgoal):
 1. \<And>s prio st. \<lbrakk>pas_wellformed aag; irq_map_wellformed aag s; \<forall>x\<in>domains_of_state s. case x of (ptr, d) \<Rightarrow> pasObjectAbs aag ptr \<in> pasDomainAbs aag d; state_objs_in_policy aag s; state_asids_to_policy aag s \<subseteq> pasPolicy aag; state_irqs_to_policy aag s \<subseteq> pasPolicy aag; valid_queues s; ready_queues s (cur_domain s) prio \<noteq> []; st_tcb_at ((=) st) (hd (max_non_empty_queue (ready_queues s (cur_domain s)))) s; runnable st\<rbrakk> \<Longrightarrow> pasObjectAbs aag (hd (max_non_empty_queue (ready_queues s (cur_domain s)))) \<in> pasDomainAbs aag (cur_domain s) proof (prove)
goal (2 subgoals):
 1. \<And>s prio st. \<lbrakk>pas_wellformed aag; irq_map_wellformed aag s; state_objs_in_policy aag s; state_asids_to_policy aag s \<subseteq> pasPolicy aag; state_irqs_to_policy aag s \<subseteq> pasPolicy aag; valid_queues s; ready_queues s (cur_domain s) prio \<noteq> []; st_tcb_at ((=) st) (hd (max_non_empty_queue (ready_queues s (cur_domain s)))) s; runnable st; case (hd (max_non_empty_queue (ready_queues s (cur_domain s))), cur_domain s) of (ptr, d) \<Rightarrow> pasObjectAbs aag ptr \<in> pasDomainAbs aag d\<rbrakk> \<Longrightarrow> pasObjectAbs aag (hd (max_non_empty_queue (ready_queues s (cur_domain s)))) \<in> pasDomainAbs aag (cur_domain s)
 2. \<And>s prio st. \<lbrakk>pas_wellformed aag; irq_map_wellformed aag s; state_objs_in_policy aag s; state_asids_to_policy aag s \<subseteq> pasPolicy aag; state_irqs_to_policy aag s \<subseteq> pasPolicy aag; valid_queues s; ready_queues s (cur_domain s) prio \<noteq> []; st_tcb_at ((=) st) (hd (max_non_empty_queue (ready_queues s (cur_domain s)))) s; runnable st; (hd (max_non_empty_queue (ready_queues s (cur_domain s))), cur_domain s) \<notin> domains_of_state s\<rbrakk> \<Longrightarrow> pasObjectAbs aag (hd (max_non_empty_queue (ready_queues s (cur_domain s)))) \<in> pasDomainAbs aag (cur_domain s) proof (prove)
goal (1 subgoal):
 1. \<And>s prio st. \<lbrakk>pas_wellformed aag; irq_map_wellformed aag s; state_objs_in_policy aag s; state_asids_to_policy aag s \<subseteq> pasPolicy aag; state_irqs_to_policy aag s \<subseteq> pasPolicy aag; valid_queues s; ready_queues s (cur_domain s) prio \<noteq> []; st_tcb_at ((=) st) (hd (max_non_empty_queue (ready_queues s (cur_domain s)))) s; runnable st; (hd (max_non_empty_queue (ready_queues s (cur_domain s))), cur_domain s) \<notin> domains_of_state s\<rbrakk> \<Longrightarrow> pasObjectAbs aag (hd (max_non_empty_queue (ready_queues s (cur_domain s)))) \<in> pasDomainAbs aag (cur_domain s) proof (prove)
goal (1 subgoal):
 1. \<And>s prio st. \<lbrakk>pas_wellformed aag; irq_map_wellformed aag s; state_objs_in_policy aag s; state_asids_to_policy aag s \<subseteq> pasPolicy aag; state_irqs_to_policy aag s \<subseteq> pasPolicy aag; \<forall>d p. (\<forall>t\<in>set (ready_queues s d p). (\<exists>y. ekheap s t = Some y) \<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); ready_queues s (cur_domain s) prio \<noteq> []; st_tcb_at ((=) st) (hd (max_non_empty_queue (ready_queues s (cur_domain s)))) s; runnable st; (hd (max_non_empty_queue (ready_queues s (cur_domain s))), cur_domain s) \<notin> domains_of_state s\<rbrakk> \<Longrightarrow> pasObjectAbs aag (hd (max_non_empty_queue (ready_queues s (cur_domain s)))) \<in> pasDomainAbs aag (cur_domain s) proof (prove)
goal (1 subgoal):
 1. \<And>s prio st. \<lbrakk>pas_wellformed aag; irq_map_wellformed aag s; state_objs_in_policy aag s; state_asids_to_policy aag s \<subseteq> pasPolicy aag; state_irqs_to_policy aag s \<subseteq> pasPolicy aag; ready_queues s (cur_domain s) prio \<noteq> []; st_tcb_at ((=) st) (hd (max_non_empty_queue (ready_queues s (cur_domain s)))) s; runnable st; (hd (max_non_empty_queue (ready_queues s (cur_domain s))), cur_domain s) \<notin> domains_of_state s; \<forall>p. (\<forall>t\<in>set (ready_queues s (cur_domain s) p). (\<exists>y. ekheap s t = Some y) \<and> etcb_at (\<lambda>t. tcb_priority t = p \<and> tcb_domain t = cur_domain s) t s \<and> st_tcb_at runnable t s) \<and> distinct (ready_queues s (cur_domain s) p)\<rbrakk> \<Longrightarrow> pasObjectAbs aag (hd (max_non_empty_queue (ready_queues s (cur_domain s)))) \<in> pasDomainAbs aag (cur_domain s) proof (prove)
goal (1 subgoal):
 1. \<And>s prio st. \<lbrakk>pas_wellformed aag; irq_map_wellformed aag s; state_objs_in_policy aag s; state_asids_to_policy aag s \<subseteq> pasPolicy aag; state_irqs_to_policy aag s \<subseteq> pasPolicy aag; ready_queues s (cur_domain s) prio \<noteq> []; st_tcb_at ((=) st) (hd (max_non_empty_queue (ready_queues s (cur_domain s)))) s; runnable st; (hd (max_non_empty_queue (ready_queues s (cur_domain s))), cur_domain s) \<notin> domains_of_state s; (\<forall>t\<in>set (ready_queues s (cur_domain s) (Max {prio. ready_queues s (cur_domain s) prio \<noteq> []})). (\<exists>y. ekheap s t = Some y) \<and> etcb_at (\<lambda>t. tcb_priority t = Max {prio. ready_queues s (cur_domain s) prio \<noteq> []} \<and> tcb_domain t = cur_domain s) t s \<and> st_tcb_at runnable t s) \<and> distinct (ready_queues s (cur_domain s) (Max {prio. ready_queues s (cur_domain s) prio \<noteq> []}))\<rbrakk> \<Longrightarrow> pasObjectAbs aag (hd (max_non_empty_queue (ready_queues s (cur_domain s)))) \<in> pasDomainAbs aag (cur_domain s) proof (prove)
goal (1 subgoal):
 1. \<And>s prio st. \<lbrakk>pas_wellformed aag; irq_map_wellformed aag s; state_objs_in_policy aag s; state_asids_to_policy aag s \<subseteq> pasPolicy aag; state_irqs_to_policy aag s \<subseteq> pasPolicy aag; ready_queues s (cur_domain s) prio \<noteq> []; st_tcb_at ((=) st) (hd (max_non_empty_queue (ready_queues s (cur_domain s)))) s; runnable st; (hd (max_non_empty_queue (ready_queues s (cur_domain s))), cur_domain s) \<notin> domains_of_state s; \<forall>t\<in>set (ready_queues s (cur_domain s) (Max {prio. ready_queues s (cur_domain s) prio \<noteq> []})). (\<exists>y. ekheap s t = Some y) \<and> etcb_at (\<lambda>t. tcb_priority t = Max {prio. ready_queues s (cur_domain s) prio \<noteq> []} \<and> tcb_domain t = cur_domain s) t s \<and> st_tcb_at runnable t s; distinct (ready_queues s (cur_domain s) (Max {prio. ready_queues s (cur_domain s) prio \<noteq> []}))\<rbrakk> \<Longrightarrow> pasObjectAbs aag (hd (max_non_empty_queue (ready_queues s (cur_domain s)))) \<in> pasDomainAbs aag (cur_domain s) proof (prove)
goal (2 subgoals):
 1. \<And>s prio st. \<lbrakk>pas_wellformed aag; irq_map_wellformed aag s; state_objs_in_policy aag s; state_asids_to_policy aag s \<subseteq> pasPolicy aag; state_irqs_to_policy aag s \<subseteq> pasPolicy aag; ready_queues s (cur_domain s) prio \<noteq> []; st_tcb_at ((=) st) (hd (max_non_empty_queue (ready_queues s (cur_domain s)))) s; runnable st; (hd (max_non_empty_queue (ready_queues s (cur_domain s))), cur_domain s) \<notin> domains_of_state s; distinct (ready_queues s (cur_domain s) (Max {prio. ready_queues s (cur_domain s) prio \<noteq> []})); (\<exists>y. ekheap s (hd (max_non_empty_queue (ready_queues s (cur_domain s)))) = Some y) \<and> etcb_at (\<lambda>t. tcb_priority t = Max {prio. ready_queues s (cur_domain s) prio \<noteq> []} \<and> tcb_domain t = cur_domain s) (hd (max_non_empty_queue (ready_queues s (cur_domain s)))) s \<and> st_tcb_at runnable (hd (max_non_empty_queue (ready_queues s (cur_domain s)))) s\<rbrakk> \<Longrightarrow> pasObjectAbs aag (hd (max_non_empty_queue (ready_queues s (cur_domain s)))) \<in> pasDomainAbs aag (cur_domain s)
 2. \<And>s prio st. \<lbrakk>pas_wellformed aag; irq_map_wellformed aag s; state_objs_in_policy aag s; state_asids_to_policy aag s \<subseteq> pasPolicy aag; state_irqs_to_policy aag s \<subseteq> pasPolicy aag; ready_queues s (cur_domain s) prio \<noteq> []; st_tcb_at ((=) st) (hd (max_non_empty_queue (ready_queues s (cur_domain s)))) s; runnable st; (hd (max_non_empty_queue (ready_queues s (cur_domain s))), cur_domain s) \<notin> domains_of_state s; distinct (ready_queues s (cur_domain s) (Max {prio. ready_queues s (cur_domain s) prio \<noteq> []})); hd (max_non_empty_queue (ready_queues s (cur_domain s))) \<notin> set (ready_queues s (cur_domain s) (Max {prio. ready_queues s (cur_domain s) prio \<noteq> []}))\<rbrakk> \<Longrightarrow> pasObjectAbs aag (hd (max_non_empty_queue (ready_queues s (cur_domain s)))) \<in> pasDomainAbs aag (cur_domain s) proof (prove)
goal (2 subgoals):
 1. \<And>s prio st y. \<lbrakk>pas_wellformed aag; irq_map_wellformed aag s; state_objs_in_policy aag s; state_asids_to_policy aag s \<subseteq> pasPolicy aag; state_irqs_to_policy aag s \<subseteq> pasPolicy aag; ready_queues s (cur_domain s) prio \<noteq> []; st_tcb_at ((=) st) (hd (max_non_empty_queue (ready_queues s (cur_domain s)))) s; runnable st; (hd (max_non_empty_queue (ready_queues s (cur_domain s))), cur_domain s) \<notin> domains_of_state s; distinct (ready_queues s (cur_domain s) (Max {prio. ready_queues s (cur_domain s) prio \<noteq> []})); ekheap s (hd (max_non_empty_queue (ready_queues s (cur_domain s)))) = Some y; etcb_at (\<lambda>t. tcb_priority t = Max {prio. ready_queues s (cur_domain s) prio \<noteq> []} \<and> tcb_domain t = cur_domain s) (hd (max_non_empty_queue (ready_queues s (cur_domain s)))) s; st_tcb_at runnable (hd (max_non_empty_queue (ready_queues s (cur_domain s)))) s\<rbrakk> \<Longrightarrow> pasObjectAbs aag (hd (max_non_empty_queue (ready_queues s (cur_domain s)))) \<in> pasDomainAbs aag (cur_domain s)
 2. \<And>s prio st. \<lbrakk>pas_wellformed aag; irq_map_wellformed aag s; state_objs_in_policy aag s; state_asids_to_policy aag s \<subseteq> pasPolicy aag; state_irqs_to_policy aag s \<subseteq> pasPolicy aag; ready_queues s (cur_domain s) prio \<noteq> []; st_tcb_at ((=) st) (hd (max_non_empty_queue (ready_queues s (cur_domain s)))) s; runnable st; (hd (max_non_empty_queue (ready_queues s (cur_domain s))), cur_domain s) \<notin> domains_of_state s; distinct (ready_queues s (cur_domain s) (Max {prio. ready_queues s (cur_domain s) prio \<noteq> []})); hd (max_non_empty_queue (ready_queues s (cur_domain s))) \<notin> set (ready_queues s (cur_domain s) (Max {prio. ready_queues s (cur_domain s) prio \<noteq> []}))\<rbrakk> \<Longrightarrow> pasObjectAbs aag (hd (max_non_empty_queue (ready_queues s (cur_domain s)))) \<in> pasDomainAbs aag (cur_domain s) proof (prove)
goal (3 subgoals):
 1. \<And>s prio st y. \<lbrakk>pas_wellformed aag; irq_map_wellformed aag s; state_objs_in_policy aag s; state_asids_to_policy aag s \<subseteq> pasPolicy aag; state_irqs_to_policy aag s \<subseteq> pasPolicy aag; ready_queues s (cur_domain s) prio \<noteq> []; st_tcb_at ((=) st) (hd (max_non_empty_queue (ready_queues s (cur_domain s)))) s; runnable st; distinct (ready_queues s (cur_domain s) (Max {prio. ready_queues s (cur_domain s) prio \<noteq> []})); ekheap s (hd (max_non_empty_queue (ready_queues s (cur_domain s)))) = Some y; etcb_at (\<lambda>t. tcb_priority t = Max {prio. ready_queues s (cur_domain s) prio \<noteq> []} \<and> tcb_domain t = cur_domain s) (hd (max_non_empty_queue (ready_queues s (cur_domain s)))) s; st_tcb_at runnable (hd (max_non_empty_queue (ready_queues s (cur_domain s)))) s\<rbrakk> \<Longrightarrow> ekheap s (hd (max_non_empty_queue (ready_queues s (cur_domain s)))) = Some (?etcb41 s prio st y)
 2. \<And>s prio st y. \<lbrakk>pas_wellformed aag; irq_map_wellformed aag s; state_objs_in_policy aag s; state_asids_to_policy aag s \<subseteq> pasPolicy aag; state_irqs_to_policy aag s \<subseteq> pasPolicy aag; ready_queues s (cur_domain s) prio \<noteq> []; st_tcb_at ((=) st) (hd (max_non_empty_queue (ready_queues s (cur_domain s)))) s; runnable st; distinct (ready_queues s (cur_domain s) (Max {prio. ready_queues s (cur_domain s) prio \<noteq> []})); ekheap s (hd (max_non_empty_queue (ready_queues s (cur_domain s)))) = Some y; etcb_at (\<lambda>t. tcb_priority t = Max {prio. ready_queues s (cur_domain s) prio \<noteq> []} \<and> tcb_domain t = cur_domain s) (hd (max_non_empty_queue (ready_queues s (cur_domain s)))) s; st_tcb_at runnable (hd (max_non_empty_queue (ready_queues s (cur_domain s)))) s\<rbrakk> \<Longrightarrow> cur_domain s = tcb_domain (?etcb41 s prio st y)
 3. \<And>s prio st. \<lbrakk>pas_wellformed aag; irq_map_wellformed aag s; state_objs_in_policy aag s; state_asids_to_policy aag s \<subseteq> pasPolicy aag; state_irqs_to_policy aag s \<subseteq> pasPolicy aag; ready_queues s (cur_domain s) prio \<noteq> []; st_tcb_at ((=) st) (hd (max_non_empty_queue (ready_queues s (cur_domain s)))) s; runnable st; (hd (max_non_empty_queue (ready_queues s (cur_domain s))), cur_domain s) \<notin> domains_of_state s; distinct (ready_queues s (cur_domain s) (Max {prio. ready_queues s (cur_domain s) prio \<noteq> []})); hd (max_non_empty_queue (ready_queues s (cur_domain s))) \<notin> set (ready_queues s (cur_domain s) (Max {prio. ready_queues s (cur_domain s) prio \<noteq> []}))\<rbrakk> \<Longrightarrow> pasObjectAbs aag (hd (max_non_empty_queue (ready_queues s (cur_domain s)))) \<in> pasDomainAbs aag (cur_domain s) proof (prove)
goal (2 subgoals):
 1. \<And>s prio st y. \<lbrakk>pas_wellformed aag; irq_map_wellformed aag s; state_objs_in_policy aag s; state_asids_to_policy aag s \<subseteq> pasPolicy aag; state_irqs_to_policy aag s \<subseteq> pasPolicy aag; ready_queues s (cur_domain s) prio \<noteq> []; st_tcb_at ((=) st) (hd (max_non_empty_queue (ready_queues s (cur_domain s)))) s; runnable st; distinct (ready_queues s (cur_domain s) (Max {prio. ready_queues s (cur_domain s) prio \<noteq> []})); ekheap s (hd (max_non_empty_queue (ready_queues s (cur_domain s)))) = Some y; etcb_at (\<lambda>t. tcb_priority t = Max {prio. ready_queues s (cur_domain s) prio \<noteq> []} \<and> tcb_domain t = cur_domain s) (hd (max_non_empty_queue (ready_queues s (cur_domain s)))) s; st_tcb_at runnable (hd (max_non_empty_queue (ready_queues s (cur_domain s)))) s\<rbrakk> \<Longrightarrow> cur_domain s = tcb_domain y
 2. \<And>s prio st. \<lbrakk>pas_wellformed aag; irq_map_wellformed aag s; state_objs_in_policy aag s; state_asids_to_policy aag s \<subseteq> pasPolicy aag; state_irqs_to_policy aag s \<subseteq> pasPolicy aag; ready_queues s (cur_domain s) prio \<noteq> []; st_tcb_at ((=) st) (hd (max_non_empty_queue (ready_queues s (cur_domain s)))) s; runnable st; (hd (max_non_empty_queue (ready_queues s (cur_domain s))), cur_domain s) \<notin> domains_of_state s; distinct (ready_queues s (cur_domain s) (Max {prio. ready_queues s (cur_domain s) prio \<noteq> []})); hd (max_non_empty_queue (ready_queues s (cur_domain s))) \<notin> set (ready_queues s (cur_domain s) (Max {prio. ready_queues s (cur_domain s) prio \<noteq> []}))\<rbrakk> \<Longrightarrow> pasObjectAbs aag (hd (max_non_empty_queue (ready_queues s (cur_domain s)))) \<in> pasDomainAbs aag (cur_domain s) proof (prove)
goal (1 subgoal):
 1. \<And>s prio st. \<lbrakk>pas_wellformed aag; irq_map_wellformed aag s; state_objs_in_policy aag s; state_asids_to_policy aag s \<subseteq> pasPolicy aag; state_irqs_to_policy aag s \<subseteq> pasPolicy aag; ready_queues s (cur_domain s) prio \<noteq> []; st_tcb_at ((=) st) (hd (max_non_empty_queue (ready_queues s (cur_domain s)))) s; runnable st; (hd (max_non_empty_queue (ready_queues s (cur_domain s))), cur_domain s) \<notin> domains_of_state s; distinct (ready_queues s (cur_domain s) (Max {prio. ready_queues s (cur_domain s) prio \<noteq> []})); hd (max_non_empty_queue (ready_queues s (cur_domain s))) \<notin> set (ready_queues s (cur_domain s) (Max {prio. ready_queues s (cur_domain s) prio \<noteq> []}))\<rbrakk> \<Longrightarrow> pasObjectAbs aag (hd (max_non_empty_queue (ready_queues s (cur_domain s)))) \<in> pasDomainAbs aag (cur_domain s) proof (prove)
goal (1 subgoal):
 1. \<And>s prio st. \<lbrakk>pas_wellformed aag; irq_map_wellformed aag s; state_objs_in_policy aag s; state_asids_to_policy aag s \<subseteq> pasPolicy aag; state_irqs_to_policy aag s \<subseteq> pasPolicy aag; ready_queues s (cur_domain s) prio \<noteq> []; st_tcb_at ((=) st) (hd (ready_queues s (cur_domain s) (Max {prio. ready_queues s (cur_domain s) prio \<noteq> []}))) s; runnable st; (hd (ready_queues s (cur_domain s) (Max {prio. ready_queues s (cur_domain s) prio \<noteq> []})), cur_domain s) \<notin> domains_of_state s; distinct (ready_queues s (cur_domain s) (Max {prio. ready_queues s (cur_domain s) prio \<noteq> []})); hd (ready_queues s (cur_domain s) (Max {prio. ready_queues s (cur_domain s) prio \<noteq> []})) \<notin> set (ready_queues s (cur_domain s) (Max {prio. ready_queues s (cur_domain s) prio \<noteq> []}))\<rbrakk> \<Longrightarrow> pasObjectAbs aag (hd (ready_queues s (cur_domain s) (Max {prio. ready_queues s (cur_domain s) prio \<noteq> []}))) \<in> pasDomainAbs aag (cur_domain s) proof (prove)
goal (1 subgoal):
 1. \<And>s prio st. \<lbrakk>pas_wellformed aag; irq_map_wellformed aag s; state_objs_in_policy aag s; state_asids_to_policy aag s \<subseteq> pasPolicy aag; state_irqs_to_policy aag s \<subseteq> pasPolicy aag; ready_queues s (cur_domain s) prio \<noteq> []; st_tcb_at ((=) st) (hd (ready_queues s (cur_domain s) (Max {prio. ready_queues s (cur_domain s) prio \<noteq> []}))) s; runnable st; (hd (ready_queues s (cur_domain s) (Max {prio. ready_queues s (cur_domain s) prio \<noteq> []})), cur_domain s) \<notin> domains_of_state s; distinct (ready_queues s (cur_domain s) (Max {prio. ready_queues s (cur_domain s) prio \<noteq> []}))\<rbrakk> \<Longrightarrow> hd (ready_queues s (cur_domain s) (Max {prio. ready_queues s (cur_domain s) prio \<noteq> []})) \<in> set (ready_queues s (cur_domain s) (Max {prio. ready_queues s (cur_domain s) prio \<noteq> []})) proof (prove)
goal (2 subgoals):
 1. \<And>s prio st. \<lbrakk>pas_wellformed aag; irq_map_wellformed aag s; state_objs_in_policy aag s; state_asids_to_policy aag s \<subseteq> pasPolicy aag; state_irqs_to_policy aag s \<subseteq> pasPolicy aag; ready_queues s (cur_domain s) prio \<noteq> []; st_tcb_at ((=) st) (hd (ready_queues s (cur_domain s) (Max {prio. ready_queues s (cur_domain s) prio \<noteq> []}))) s; runnable st; (hd (ready_queues s (cur_domain s) (Max {prio. ready_queues s (cur_domain s) prio \<noteq> []})), cur_domain s) \<notin> domains_of_state s; distinct (ready_queues s (cur_domain s) (Max {prio. ready_queues s (cur_domain s) prio \<noteq> []})); Max {prio. ready_queues s (cur_domain s) prio \<noteq> []} \<in> {prio. ready_queues s (cur_domain s) prio \<noteq> []}\<rbrakk> \<Longrightarrow> hd (ready_queues s (cur_domain s) (Max {prio. ready_queues s (cur_domain s) prio \<noteq> []})) \<in> set (ready_queues s (cur_domain s) (Max {prio. ready_queues s (cur_domain s) prio \<noteq> []}))
 2. \<And>s prio st. \<lbrakk>pas_wellformed aag; irq_map_wellformed aag s; state_objs_in_policy aag s; state_asids_to_policy aag s \<subseteq> pasPolicy aag; state_irqs_to_policy aag s \<subseteq> pasPolicy aag; ready_queues s (cur_domain s) prio \<noteq> []; st_tcb_at ((=) st) (hd (ready_queues s (cur_domain s) (Max {prio. ready_queues s (cur_domain s) prio \<noteq> []}))) s; runnable st; (hd (ready_queues s (cur_domain s) (Max {prio. ready_queues s (cur_domain s) prio \<noteq> []})), cur_domain s) \<notin> domains_of_state s; distinct (ready_queues s (cur_domain s) (Max {prio. ready_queues s (cur_domain s) prio \<noteq> []}))\<rbrakk> \<Longrightarrow> {prio. ready_queues s (cur_domain s) prio \<noteq> []} \<noteq> {} proof (prove)
goal:
No subgoals!