theory TcbQueue_C

lemma cready_queues_relation_null_queue_ptrs:
  assumes rel: "cready_queues_relation mp cq aq"
  and same: "option_map tcb_null_ep_ptrs \<circ> mp' = option_map tcb_null_ep_ptrs \<circ> mp"
  shows "cready_queues_relation mp' cq aq" using rel apply (clarsimp simp: cready_queues_relation_def Let_def all_conj_distrib) apply (drule spec, drule spec, drule mp, (erule conjI)+, assumption) apply (clarsimp simp: tcb_queue_relation'_def) apply (erule iffD2 [OF tcb_queue_relation_only_next_prev, rotated -1]) apply (rule ext) apply (case_tac "mp' x") apply (frule compD [OF same]) apply simp apply (frule compD [OF same]) apply (clarsimp simp: tcb_null_ep_ptrs_def) apply (case_tac z, case_tac a) apply simp
  \<comment> \<open>clag\<close> apply (rule ext) apply (case_tac "mp' x") apply (frule compD [OF same]) apply simp apply (frule compD [OF same]) apply (clarsimp simp: tcb_null_ep_ptrs_def) apply (case_tac z, case_tac a) apply simp done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. cready_queues_relation mp' cq aq proof (prove)
using this:
cready_queues_relation mp cq aq

goal (1 subgoal):
 1. cready_queues_relation mp' cq aq proof (prove)
goal (1 subgoal):
 1. \<And>qdom prio. \<lbrakk>\<forall>qdom prio. UCAST(32 signed \<rightarrow> 8) minDom \<le> qdom \<and> qdom \<le> UCAST(32 signed \<rightarrow> 8) maxDom \<and> UCAST(32 signed \<rightarrow> 8) seL4_MinPrio \<le> prio \<and> prio \<le> UCAST(32 signed \<rightarrow> 8) seL4_MaxPrio \<longrightarrow> sched_queue_relation' mp (aq (qdom, prio)) (head_C (cq.[cready_queues_index_to_C qdom prio])) (StateRelation_C.end_C (cq.[cready_queues_index_to_C qdom prio])); \<forall>qdom prio. (UCAST(32 signed \<rightarrow> 8) seL4_MinPrio \<le> prio \<longrightarrow> qdom \<le> UCAST(32 signed \<rightarrow> 8) maxDom \<longrightarrow> UCAST(32 signed \<rightarrow> 8) minDom \<le> qdom \<longrightarrow> \<not> prio \<le> UCAST(32 signed \<rightarrow> 8) seL4_MaxPrio) \<longrightarrow> aq (qdom, prio) = []; UCAST(32 signed \<rightarrow> 8) minDom \<le> qdom; qdom \<le> UCAST(32 signed \<rightarrow> 8) maxDom; UCAST(32 signed \<rightarrow> 8) seL4_MinPrio \<le> prio; prio \<le> UCAST(32 signed \<rightarrow> 8) seL4_MaxPrio\<rbrakk> \<Longrightarrow> sched_queue_relation' mp' (aq (qdom, prio)) (head_C (cq.[cready_queues_index_to_C qdom prio])) (StateRelation_C.end_C (cq.[cready_queues_index_to_C qdom prio])) proof (prove)
goal (1 subgoal):
 1. \<And>qdom prio. \<lbrakk>\<forall>qdom prio. (UCAST(32 signed \<rightarrow> 8) seL4_MinPrio \<le> prio \<longrightarrow> qdom \<le> UCAST(32 signed \<rightarrow> 8) maxDom \<longrightarrow> UCAST(32 signed \<rightarrow> 8) minDom \<le> qdom \<longrightarrow> \<not> prio \<le> UCAST(32 signed \<rightarrow> 8) seL4_MaxPrio) \<longrightarrow> aq (qdom, prio) = []; UCAST(32 signed \<rightarrow> 8) minDom \<le> qdom; qdom \<le> UCAST(32 signed \<rightarrow> 8) maxDom; UCAST(32 signed \<rightarrow> 8) seL4_MinPrio \<le> prio; prio \<le> UCAST(32 signed \<rightarrow> 8) seL4_MaxPrio; sched_queue_relation' mp (aq (qdom, prio)) (head_C (cq.[cready_queues_index_to_C qdom prio])) (StateRelation_C.end_C (cq.[cready_queues_index_to_C qdom prio]))\<rbrakk> \<Longrightarrow> sched_queue_relation' mp' (aq (qdom, prio)) (head_C (cq.[cready_queues_index_to_C qdom prio])) (StateRelation_C.end_C (cq.[cready_queues_index_to_C qdom prio])) proof (prove)
goal (1 subgoal):
 1. \<And>qdom prio. \<lbrakk>\<forall>qdom prio. (UCAST(32 signed \<rightarrow> 8) seL4_MinPrio \<le> prio \<longrightarrow> qdom \<le> UCAST(32 signed \<rightarrow> 8) maxDom \<longrightarrow> UCAST(32 signed \<rightarrow> 8) minDom \<le> qdom \<longrightarrow> \<not> prio \<le> UCAST(32 signed \<rightarrow> 8) seL4_MaxPrio) \<longrightarrow> aq (qdom, prio) = []; UCAST(32 signed \<rightarrow> 8) minDom \<le> qdom; qdom \<le> UCAST(32 signed \<rightarrow> 8) maxDom; UCAST(32 signed \<rightarrow> 8) seL4_MinPrio \<le> prio; prio \<le> UCAST(32 signed \<rightarrow> 8) seL4_MaxPrio; StateRelation_C.end_C (cq.[cready_queues_index_to_C qdom prio]) = (if aq (qdom, prio) = [] then NULL else tcb_ptr_to_ctcb_ptr (last (aq (qdom, prio)))); sched_queue_relation mp (aq (qdom, prio)) NULL (head_C (cq.[cready_queues_index_to_C qdom prio]))\<rbrakk> \<Longrightarrow> sched_queue_relation mp' (aq (qdom, prio)) NULL (head_C (cq.[cready_queues_index_to_C qdom prio])) proof (prove)
goal (2 subgoals):
 1. \<And>qdom prio. \<lbrakk>\<forall>qdom prio. (UCAST(32 signed \<rightarrow> 8) seL4_MinPrio \<le> prio \<longrightarrow> qdom \<le> UCAST(32 signed \<rightarrow> 8) maxDom \<longrightarrow> UCAST(32 signed \<rightarrow> 8) minDom \<le> qdom \<longrightarrow> \<not> prio \<le> UCAST(32 signed \<rightarrow> 8) seL4_MaxPrio) \<longrightarrow> aq (qdom, prio) = []; UCAST(32 signed \<rightarrow> 8) minDom \<le> qdom; qdom \<le> UCAST(32 signed \<rightarrow> 8) maxDom; UCAST(32 signed \<rightarrow> 8) seL4_MinPrio \<le> prio; prio \<le> UCAST(32 signed \<rightarrow> 8) seL4_MaxPrio; StateRelation_C.end_C (cq.[cready_queues_index_to_C qdom prio]) = (if aq (qdom, prio) = [] then NULL else tcb_ptr_to_ctcb_ptr (last (aq (qdom, prio))))\<rbrakk> \<Longrightarrow> map_option tcbSchedNext_C \<circ> mp' = map_option tcbSchedNext_C \<circ> mp
 2. \<And>qdom prio. \<lbrakk>\<forall>qdom prio. (UCAST(32 signed \<rightarrow> 8) seL4_MinPrio \<le> prio \<longrightarrow> qdom \<le> UCAST(32 signed \<rightarrow> 8) maxDom \<longrightarrow> UCAST(32 signed \<rightarrow> 8) minDom \<le> qdom \<longrightarrow> \<not> prio \<le> UCAST(32 signed \<rightarrow> 8) seL4_MaxPrio) \<longrightarrow> aq (qdom, prio) = []; UCAST(32 signed \<rightarrow> 8) minDom \<le> qdom; qdom \<le> UCAST(32 signed \<rightarrow> 8) maxDom; UCAST(32 signed \<rightarrow> 8) seL4_MinPrio \<le> prio; prio \<le> UCAST(32 signed \<rightarrow> 8) seL4_MaxPrio; StateRelation_C.end_C (cq.[cready_queues_index_to_C qdom prio]) = (if aq (qdom, prio) = [] then NULL else tcb_ptr_to_ctcb_ptr (last (aq (qdom, prio))))\<rbrakk> \<Longrightarrow> map_option tcbSchedPrev_C \<circ> mp' = map_option tcbSchedPrev_C \<circ> mp proof (prove)
goal (2 subgoals):
 1. \<And>qdom prio x. \<lbrakk>\<forall>qdom prio. (UCAST(32 signed \<rightarrow> 8) seL4_MinPrio \<le> prio \<longrightarrow> qdom \<le> UCAST(32 signed \<rightarrow> 8) maxDom \<longrightarrow> UCAST(32 signed \<rightarrow> 8) minDom \<le> qdom \<longrightarrow> \<not> prio \<le> UCAST(32 signed \<rightarrow> 8) seL4_MaxPrio) \<longrightarrow> aq (qdom, prio) = []; UCAST(32 signed \<rightarrow> 8) minDom \<le> qdom; qdom \<le> UCAST(32 signed \<rightarrow> 8) maxDom; UCAST(32 signed \<rightarrow> 8) seL4_MinPrio \<le> prio; prio \<le> UCAST(32 signed \<rightarrow> 8) seL4_MaxPrio; StateRelation_C.end_C (cq.[cready_queues_index_to_C qdom prio]) = (if aq (qdom, prio) = [] then NULL else tcb_ptr_to_ctcb_ptr (last (aq (qdom, prio))))\<rbrakk> \<Longrightarrow> (map_option tcbSchedNext_C \<circ> mp') x = (map_option tcbSchedNext_C \<circ> mp) x
 2. \<And>qdom prio. \<lbrakk>\<forall>qdom prio. (UCAST(32 signed \<rightarrow> 8) seL4_MinPrio \<le> prio \<longrightarrow> qdom \<le> UCAST(32 signed \<rightarrow> 8) maxDom \<longrightarrow> UCAST(32 signed \<rightarrow> 8) minDom \<le> qdom \<longrightarrow> \<not> prio \<le> UCAST(32 signed \<rightarrow> 8) seL4_MaxPrio) \<longrightarrow> aq (qdom, prio) = []; UCAST(32 signed \<rightarrow> 8) minDom \<le> qdom; qdom \<le> UCAST(32 signed \<rightarrow> 8) maxDom; UCAST(32 signed \<rightarrow> 8) seL4_MinPrio \<le> prio; prio \<le> UCAST(32 signed \<rightarrow> 8) seL4_MaxPrio; StateRelation_C.end_C (cq.[cready_queues_index_to_C qdom prio]) = (if aq (qdom, prio) = [] then NULL else tcb_ptr_to_ctcb_ptr (last (aq (qdom, prio))))\<rbrakk> \<Longrightarrow> map_option tcbSchedPrev_C \<circ> mp' = map_option tcbSchedPrev_C \<circ> mp proof (prove)
goal (3 subgoals):
 1. \<And>qdom prio x. \<lbrakk>\<forall>qdom prio. (UCAST(32 signed \<rightarrow> 8) seL4_MinPrio \<le> prio \<longrightarrow> qdom \<le> UCAST(32 signed \<rightarrow> 8) maxDom \<longrightarrow> UCAST(32 signed \<rightarrow> 8) minDom \<le> qdom \<longrightarrow> \<not> prio \<le> UCAST(32 signed \<rightarrow> 8) seL4_MaxPrio) \<longrightarrow> aq (qdom, prio) = []; UCAST(32 signed \<rightarrow> 8) minDom \<le> qdom; qdom \<le> UCAST(32 signed \<rightarrow> 8) maxDom; UCAST(32 signed \<rightarrow> 8) seL4_MinPrio \<le> prio; prio \<le> UCAST(32 signed \<rightarrow> 8) seL4_MaxPrio; StateRelation_C.end_C (cq.[cready_queues_index_to_C qdom prio]) = (if aq (qdom, prio) = [] then NULL else tcb_ptr_to_ctcb_ptr (last (aq (qdom, prio)))); mp' x = None\<rbrakk> \<Longrightarrow> (map_option tcbSchedNext_C \<circ> mp') x = (map_option tcbSchedNext_C \<circ> mp) x
 2. \<And>qdom prio x a. \<lbrakk>\<forall>qdom prio. (UCAST(32 signed \<rightarrow> 8) seL4_MinPrio \<le> prio \<longrightarrow> qdom \<le> UCAST(32 signed \<rightarrow> 8) maxDom \<longrightarrow> UCAST(32 signed \<rightarrow> 8) minDom \<le> qdom \<longrightarrow> \<not> prio \<le> UCAST(32 signed \<rightarrow> 8) seL4_MaxPrio) \<longrightarrow> aq (qdom, prio) = []; UCAST(32 signed \<rightarrow> 8) minDom \<le> qdom; qdom \<le> UCAST(32 signed \<rightarrow> 8) maxDom; UCAST(32 signed \<rightarrow> 8) seL4_MinPrio \<le> prio; prio \<le> UCAST(32 signed \<rightarrow> 8) seL4_MaxPrio; StateRelation_C.end_C (cq.[cready_queues_index_to_C qdom prio]) = (if aq (qdom, prio) = [] then NULL else tcb_ptr_to_ctcb_ptr (last (aq (qdom, prio)))); mp' x = Some a\<rbrakk> \<Longrightarrow> (map_option tcbSchedNext_C \<circ> mp') x = (map_option tcbSchedNext_C \<circ> mp) x
 3. \<And>qdom prio. \<lbrakk>\<forall>qdom prio. (UCAST(32 signed \<rightarrow> 8) seL4_MinPrio \<le> prio \<longrightarrow> qdom \<le> UCAST(32 signed \<rightarrow> 8) maxDom \<longrightarrow> UCAST(32 signed \<rightarrow> 8) minDom \<le> qdom \<longrightarrow> \<not> prio \<le> UCAST(32 signed \<rightarrow> 8) seL4_MaxPrio) \<longrightarrow> aq (qdom, prio) = []; UCAST(32 signed \<rightarrow> 8) minDom \<le> qdom; qdom \<le> UCAST(32 signed \<rightarrow> 8) maxDom; UCAST(32 signed \<rightarrow> 8) seL4_MinPrio \<le> prio; prio \<le> UCAST(32 signed \<rightarrow> 8) seL4_MaxPrio; StateRelation_C.end_C (cq.[cready_queues_index_to_C qdom prio]) = (if aq (qdom, prio) = [] then NULL else tcb_ptr_to_ctcb_ptr (last (aq (qdom, prio))))\<rbrakk> \<Longrightarrow> map_option tcbSchedPrev_C \<circ> mp' = map_option tcbSchedPrev_C \<circ> mp proof (prove)
goal (3 subgoals):
 1. \<And>qdom prio x. \<lbrakk>\<forall>qdom prio. (UCAST(32 signed \<rightarrow> 8) seL4_MinPrio \<le> prio \<longrightarrow> qdom \<le> UCAST(32 signed \<rightarrow> 8) maxDom \<longrightarrow> UCAST(32 signed \<rightarrow> 8) minDom \<le> qdom \<longrightarrow> \<not> prio \<le> UCAST(32 signed \<rightarrow> 8) seL4_MaxPrio) \<longrightarrow> aq (qdom, prio) = []; UCAST(32 signed \<rightarrow> 8) minDom \<le> qdom; qdom \<le> UCAST(32 signed \<rightarrow> 8) maxDom; UCAST(32 signed \<rightarrow> 8) seL4_MinPrio \<le> prio; prio \<le> UCAST(32 signed \<rightarrow> 8) seL4_MaxPrio; StateRelation_C.end_C (cq.[cready_queues_index_to_C qdom prio]) = (if aq (qdom, prio) = [] then NULL else tcb_ptr_to_ctcb_ptr (last (aq (qdom, prio)))); mp' x = None; map_option tcb_null_ep_ptrs (mp x) = map_option tcb_null_ep_ptrs None\<rbrakk> \<Longrightarrow> (map_option tcbSchedNext_C \<circ> mp') x = (map_option tcbSchedNext_C \<circ> mp) x
 2. \<And>qdom prio x a. \<lbrakk>\<forall>qdom prio. (UCAST(32 signed \<rightarrow> 8) seL4_MinPrio \<le> prio \<longrightarrow> qdom \<le> UCAST(32 signed \<rightarrow> 8) maxDom \<longrightarrow> UCAST(32 signed \<rightarrow> 8) minDom \<le> qdom \<longrightarrow> \<not> prio \<le> UCAST(32 signed \<rightarrow> 8) seL4_MaxPrio) \<longrightarrow> aq (qdom, prio) = []; UCAST(32 signed \<rightarrow> 8) minDom \<le> qdom; qdom \<le> UCAST(32 signed \<rightarrow> 8) maxDom; UCAST(32 signed \<rightarrow> 8) seL4_MinPrio \<le> prio; prio \<le> UCAST(32 signed \<rightarrow> 8) seL4_MaxPrio; StateRelation_C.end_C (cq.[cready_queues_index_to_C qdom prio]) = (if aq (qdom, prio) = [] then NULL else tcb_ptr_to_ctcb_ptr (last (aq (qdom, prio)))); mp' x = Some a\<rbrakk> \<Longrightarrow> (map_option tcbSchedNext_C \<circ> mp') x = (map_option tcbSchedNext_C \<circ> mp) x
 3. \<And>qdom prio. \<lbrakk>\<forall>qdom prio. (UCAST(32 signed \<rightarrow> 8) seL4_MinPrio \<le> prio \<longrightarrow> qdom \<le> UCAST(32 signed \<rightarrow> 8) maxDom \<longrightarrow> UCAST(32 signed \<rightarrow> 8) minDom \<le> qdom \<longrightarrow> \<not> prio \<le> UCAST(32 signed \<rightarrow> 8) seL4_MaxPrio) \<longrightarrow> aq (qdom, prio) = []; UCAST(32 signed \<rightarrow> 8) minDom \<le> qdom; qdom \<le> UCAST(32 signed \<rightarrow> 8) maxDom; UCAST(32 signed \<rightarrow> 8) seL4_MinPrio \<le> prio; prio \<le> UCAST(32 signed \<rightarrow> 8) seL4_MaxPrio; StateRelation_C.end_C (cq.[cready_queues_index_to_C qdom prio]) = (if aq (qdom, prio) = [] then NULL else tcb_ptr_to_ctcb_ptr (last (aq (qdom, prio))))\<rbrakk> \<Longrightarrow> map_option tcbSchedPrev_C \<circ> mp' = map_option tcbSchedPrev_C \<circ> mp proof (prove)
goal (2 subgoals):
 1. \<And>qdom prio x a. \<lbrakk>\<forall>qdom prio. (UCAST(32 signed \<rightarrow> 8) seL4_MinPrio \<le> prio \<longrightarrow> qdom \<le> UCAST(32 signed \<rightarrow> 8) maxDom \<longrightarrow> UCAST(32 signed \<rightarrow> 8) minDom \<le> qdom \<longrightarrow> \<not> prio \<le> UCAST(32 signed \<rightarrow> 8) seL4_MaxPrio) \<longrightarrow> aq (qdom, prio) = []; UCAST(32 signed \<rightarrow> 8) minDom \<le> qdom; qdom \<le> UCAST(32 signed \<rightarrow> 8) maxDom; UCAST(32 signed \<rightarrow> 8) seL4_MinPrio \<le> prio; prio \<le> UCAST(32 signed \<rightarrow> 8) seL4_MaxPrio; StateRelation_C.end_C (cq.[cready_queues_index_to_C qdom prio]) = (if aq (qdom, prio) = [] then NULL else tcb_ptr_to_ctcb_ptr (last (aq (qdom, prio)))); mp' x = Some a\<rbrakk> \<Longrightarrow> (map_option tcbSchedNext_C \<circ> mp') x = (map_option tcbSchedNext_C \<circ> mp) x
 2. \<And>qdom prio. \<lbrakk>\<forall>qdom prio. (UCAST(32 signed \<rightarrow> 8) seL4_MinPrio \<le> prio \<longrightarrow> qdom \<le> UCAST(32 signed \<rightarrow> 8) maxDom \<longrightarrow> UCAST(32 signed \<rightarrow> 8) minDom \<le> qdom \<longrightarrow> \<not> prio \<le> UCAST(32 signed \<rightarrow> 8) seL4_MaxPrio) \<longrightarrow> aq (qdom, prio) = []; UCAST(32 signed \<rightarrow> 8) minDom \<le> qdom; qdom \<le> UCAST(32 signed \<rightarrow> 8) maxDom; UCAST(32 signed \<rightarrow> 8) seL4_MinPrio \<le> prio; prio \<le> UCAST(32 signed \<rightarrow> 8) seL4_MaxPrio; StateRelation_C.end_C (cq.[cready_queues_index_to_C qdom prio]) = (if aq (qdom, prio) = [] then NULL else tcb_ptr_to_ctcb_ptr (last (aq (qdom, prio))))\<rbrakk> \<Longrightarrow> map_option tcbSchedPrev_C \<circ> mp' = map_option tcbSchedPrev_C \<circ> mp proof (prove)
goal (2 subgoals):
 1. \<And>qdom prio x a. \<lbrakk>\<forall>qdom prio. (UCAST(32 signed \<rightarrow> 8) seL4_MinPrio \<le> prio \<longrightarrow> qdom \<le> UCAST(32 signed \<rightarrow> 8) maxDom \<longrightarrow> UCAST(32 signed \<rightarrow> 8) minDom \<le> qdom \<longrightarrow> \<not> prio \<le> UCAST(32 signed \<rightarrow> 8) seL4_MaxPrio) \<longrightarrow> aq (qdom, prio) = []; UCAST(32 signed \<rightarrow> 8) minDom \<le> qdom; qdom \<le> UCAST(32 signed \<rightarrow> 8) maxDom; UCAST(32 signed \<rightarrow> 8) seL4_MinPrio \<le> prio; prio \<le> UCAST(32 signed \<rightarrow> 8) seL4_MaxPrio; StateRelation_C.end_C (cq.[cready_queues_index_to_C qdom prio]) = (if aq (qdom, prio) = [] then NULL else tcb_ptr_to_ctcb_ptr (last (aq (qdom, prio)))); mp' x = Some a; map_option tcb_null_ep_ptrs (mp x) = map_option tcb_null_ep_ptrs (Some a)\<rbrakk> \<Longrightarrow> (map_option tcbSchedNext_C \<circ> mp') x = (map_option tcbSchedNext_C \<circ> mp) x
 2. \<And>qdom prio. \<lbrakk>\<forall>qdom prio. (UCAST(32 signed \<rightarrow> 8) seL4_MinPrio \<le> prio \<longrightarrow> qdom \<le> UCAST(32 signed \<rightarrow> 8) maxDom \<longrightarrow> UCAST(32 signed \<rightarrow> 8) minDom \<le> qdom \<longrightarrow> \<not> prio \<le> UCAST(32 signed \<rightarrow> 8) seL4_MaxPrio) \<longrightarrow> aq (qdom, prio) = []; UCAST(32 signed \<rightarrow> 8) minDom \<le> qdom; qdom \<le> UCAST(32 signed \<rightarrow> 8) maxDom; UCAST(32 signed \<rightarrow> 8) seL4_MinPrio \<le> prio; prio \<le> UCAST(32 signed \<rightarrow> 8) seL4_MaxPrio; StateRelation_C.end_C (cq.[cready_queues_index_to_C qdom prio]) = (if aq (qdom, prio) = [] then NULL else tcb_ptr_to_ctcb_ptr (last (aq (qdom, prio))))\<rbrakk> \<Longrightarrow> map_option tcbSchedPrev_C \<circ> mp' = map_option tcbSchedPrev_C \<circ> mp proof (prove)
goal (2 subgoals):
 1. \<And>qdom prio x a z. \<lbrakk>\<forall>qdom prio. (UCAST(32 signed \<rightarrow> 8) seL4_MinPrio \<le> prio \<longrightarrow> qdom \<le> UCAST(32 signed \<rightarrow> 8) maxDom \<longrightarrow> UCAST(32 signed \<rightarrow> 8) minDom \<le> qdom \<longrightarrow> \<not> prio \<le> UCAST(32 signed \<rightarrow> 8) seL4_MaxPrio) \<longrightarrow> aq (qdom, prio) = []; UCAST(32 signed \<rightarrow> 8) minDom \<le> qdom; qdom \<le> UCAST(32 signed \<rightarrow> 8) maxDom; UCAST(32 signed \<rightarrow> 8) seL4_MinPrio \<le> prio; prio \<le> UCAST(32 signed \<rightarrow> 8) seL4_MaxPrio; StateRelation_C.end_C (cq.[cready_queues_index_to_C qdom prio]) = (if aq (qdom, prio) = [] then NULL else tcb_ptr_to_ctcb_ptr (last (aq (qdom, prio)))); mp' x = Some a; mp x = Some z; tcbEPPrev_C_update (\<lambda>_. NULL) (tcbEPNext_C_update (\<lambda>_. NULL) z) = tcbEPPrev_C_update (\<lambda>_. NULL) (tcbEPNext_C_update (\<lambda>_. NULL) a)\<rbrakk> \<Longrightarrow> tcbSchedNext_C a = tcbSchedNext_C z
 2. \<And>qdom prio. \<lbrakk>\<forall>qdom prio. (UCAST(32 signed \<rightarrow> 8) seL4_MinPrio \<le> prio \<longrightarrow> qdom \<le> UCAST(32 signed \<rightarrow> 8) maxDom \<longrightarrow> UCAST(32 signed \<rightarrow> 8) minDom \<le> qdom \<longrightarrow> \<not> prio \<le> UCAST(32 signed \<rightarrow> 8) seL4_MaxPrio) \<longrightarrow> aq (qdom, prio) = []; UCAST(32 signed \<rightarrow> 8) minDom \<le> qdom; qdom \<le> UCAST(32 signed \<rightarrow> 8) maxDom; UCAST(32 signed \<rightarrow> 8) seL4_MinPrio \<le> prio; prio \<le> UCAST(32 signed \<rightarrow> 8) seL4_MaxPrio; StateRelation_C.end_C (cq.[cready_queues_index_to_C qdom prio]) = (if aq (qdom, prio) = [] then NULL else tcb_ptr_to_ctcb_ptr (last (aq (qdom, prio))))\<rbrakk> \<Longrightarrow> map_option tcbSchedPrev_C \<circ> mp' = map_option tcbSchedPrev_C \<circ> mp proof (prove)
goal (2 subgoals):
 1. \<And>qdom prio x a z x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x1a x2a x3a x4a x5a x6a x7a x8a x9a x10a x11a x12a x13a x14a x15a. \<lbrakk>\<forall>qdom prio. (UCAST(32 signed \<rightarrow> 8) seL4_MinPrio \<le> prio \<longrightarrow> qdom \<le> UCAST(32 signed \<rightarrow> 8) maxDom \<longrightarrow> UCAST(32 signed \<rightarrow> 8) minDom \<le> qdom \<longrightarrow> \<not> prio \<le> UCAST(32 signed \<rightarrow> 8) seL4_MaxPrio) \<longrightarrow> aq (qdom, prio) = []; UCAST(32 signed \<rightarrow> 8) minDom \<le> qdom; qdom \<le> UCAST(32 signed \<rightarrow> 8) maxDom; UCAST(32 signed \<rightarrow> 8) seL4_MinPrio \<le> prio; prio \<le> UCAST(32 signed \<rightarrow> 8) seL4_MaxPrio; StateRelation_C.end_C (cq.[cready_queues_index_to_C qdom prio]) = (if aq (qdom, prio) = [] then NULL else tcb_ptr_to_ctcb_ptr (last (aq (qdom, prio)))); mp' x = Some a; mp x = Some z; tcbEPPrev_C_update (\<lambda>_. NULL) (tcbEPNext_C_update (\<lambda>_. NULL) z) = tcbEPPrev_C_update (\<lambda>_. NULL) (tcbEPNext_C_update (\<lambda>_. NULL) a); z = tcb_C.tcb_C x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15; a = tcb_C.tcb_C x1a x2a x3a x4a x5a x6a x7a x8a x9a x10a x11a x12a x13a x14a x15a\<rbrakk> \<Longrightarrow> tcbSchedNext_C a = tcbSchedNext_C z
 2. \<And>qdom prio. \<lbrakk>\<forall>qdom prio. (UCAST(32 signed \<rightarrow> 8) seL4_MinPrio \<le> prio \<longrightarrow> qdom \<le> UCAST(32 signed \<rightarrow> 8) maxDom \<longrightarrow> UCAST(32 signed \<rightarrow> 8) minDom \<le> qdom \<longrightarrow> \<not> prio \<le> UCAST(32 signed \<rightarrow> 8) seL4_MaxPrio) \<longrightarrow> aq (qdom, prio) = []; UCAST(32 signed \<rightarrow> 8) minDom \<le> qdom; qdom \<le> UCAST(32 signed \<rightarrow> 8) maxDom; UCAST(32 signed \<rightarrow> 8) seL4_MinPrio \<le> prio; prio \<le> UCAST(32 signed \<rightarrow> 8) seL4_MaxPrio; StateRelation_C.end_C (cq.[cready_queues_index_to_C qdom prio]) = (if aq (qdom, prio) = [] then NULL else tcb_ptr_to_ctcb_ptr (last (aq (qdom, prio))))\<rbrakk> \<Longrightarrow> map_option tcbSchedPrev_C \<circ> mp' = map_option tcbSchedPrev_C \<circ> mp proof (prove)
goal (1 subgoal):
 1. \<And>qdom prio. \<lbrakk>\<forall>qdom prio. (UCAST(32 signed \<rightarrow> 8) seL4_MinPrio \<le> prio \<longrightarrow> qdom \<le> UCAST(32 signed \<rightarrow> 8) maxDom \<longrightarrow> UCAST(32 signed \<rightarrow> 8) minDom \<le> qdom \<longrightarrow> \<not> prio \<le> UCAST(32 signed \<rightarrow> 8) seL4_MaxPrio) \<longrightarrow> aq (qdom, prio) = []; UCAST(32 signed \<rightarrow> 8) minDom \<le> qdom; qdom \<le> UCAST(32 signed \<rightarrow> 8) maxDom; UCAST(32 signed \<rightarrow> 8) seL4_MinPrio \<le> prio; prio \<le> UCAST(32 signed \<rightarrow> 8) seL4_MaxPrio; StateRelation_C.end_C (cq.[cready_queues_index_to_C qdom prio]) = (if aq (qdom, prio) = [] then NULL else tcb_ptr_to_ctcb_ptr (last (aq (qdom, prio))))\<rbrakk> \<Longrightarrow> map_option tcbSchedPrev_C \<circ> mp' = map_option tcbSchedPrev_C \<circ> mp proof (prove)
goal (1 subgoal):
 1. \<And>qdom prio x. \<lbrakk>\<forall>qdom prio. (UCAST(32 signed \<rightarrow> 8) seL4_MinPrio \<le> prio \<longrightarrow> qdom \<le> UCAST(32 signed \<rightarrow> 8) maxDom \<longrightarrow> UCAST(32 signed \<rightarrow> 8) minDom \<le> qdom \<longrightarrow> \<not> prio \<le> UCAST(32 signed \<rightarrow> 8) seL4_MaxPrio) \<longrightarrow> aq (qdom, prio) = []; UCAST(32 signed \<rightarrow> 8) minDom \<le> qdom; qdom \<le> UCAST(32 signed \<rightarrow> 8) maxDom; UCAST(32 signed \<rightarrow> 8) seL4_MinPrio \<le> prio; prio \<le> UCAST(32 signed \<rightarrow> 8) seL4_MaxPrio; StateRelation_C.end_C (cq.[cready_queues_index_to_C qdom prio]) = (if aq (qdom, prio) = [] then NULL else tcb_ptr_to_ctcb_ptr (last (aq (qdom, prio))))\<rbrakk> \<Longrightarrow> (map_option tcbSchedPrev_C \<circ> mp') x = (map_option tcbSchedPrev_C \<circ> mp) x proof (prove)
goal (2 subgoals):
 1. \<And>qdom prio x. \<lbrakk>\<forall>qdom prio. (UCAST(32 signed \<rightarrow> 8) seL4_MinPrio \<le> prio \<longrightarrow> qdom \<le> UCAST(32 signed \<rightarrow> 8) maxDom \<longrightarrow> UCAST(32 signed \<rightarrow> 8) minDom \<le> qdom \<longrightarrow> \<not> prio \<le> UCAST(32 signed \<rightarrow> 8) seL4_MaxPrio) \<longrightarrow> aq (qdom, prio) = []; UCAST(32 signed \<rightarrow> 8) minDom \<le> qdom; qdom \<le> UCAST(32 signed \<rightarrow> 8) maxDom; UCAST(32 signed \<rightarrow> 8) seL4_MinPrio \<le> prio; prio \<le> UCAST(32 signed \<rightarrow> 8) seL4_MaxPrio; StateRelation_C.end_C (cq.[cready_queues_index_to_C qdom prio]) = (if aq (qdom, prio) = [] then NULL else tcb_ptr_to_ctcb_ptr (last (aq (qdom, prio)))); mp' x = None\<rbrakk> \<Longrightarrow> (map_option tcbSchedPrev_C \<circ> mp') x = (map_option tcbSchedPrev_C \<circ> mp) x
 2. \<And>qdom prio x a. \<lbrakk>\<forall>qdom prio. (UCAST(32 signed \<rightarrow> 8) seL4_MinPrio \<le> prio \<longrightarrow> qdom \<le> UCAST(32 signed \<rightarrow> 8) maxDom \<longrightarrow> UCAST(32 signed \<rightarrow> 8) minDom \<le> qdom \<longrightarrow> \<not> prio \<le> UCAST(32 signed \<rightarrow> 8) seL4_MaxPrio) \<longrightarrow> aq (qdom, prio) = []; UCAST(32 signed \<rightarrow> 8) minDom \<le> qdom; qdom \<le> UCAST(32 signed \<rightarrow> 8) maxDom; UCAST(32 signed \<rightarrow> 8) seL4_MinPrio \<le> prio; prio \<le> UCAST(32 signed \<rightarrow> 8) seL4_MaxPrio; StateRelation_C.end_C (cq.[cready_queues_index_to_C qdom prio]) = (if aq (qdom, prio) = [] then NULL else tcb_ptr_to_ctcb_ptr (last (aq (qdom, prio)))); mp' x = Some a\<rbrakk> \<Longrightarrow> (map_option tcbSchedPrev_C \<circ> mp') x = (map_option tcbSchedPrev_C \<circ> mp) x proof (prove)
goal (2 subgoals):
 1. \<And>qdom prio x. \<lbrakk>\<forall>qdom prio. (UCAST(32 signed \<rightarrow> 8) seL4_MinPrio \<le> prio \<longrightarrow> qdom \<le> UCAST(32 signed \<rightarrow> 8) maxDom \<longrightarrow> UCAST(32 signed \<rightarrow> 8) minDom \<le> qdom \<longrightarrow> \<not> prio \<le> UCAST(32 signed \<rightarrow> 8) seL4_MaxPrio) \<longrightarrow> aq (qdom, prio) = []; UCAST(32 signed \<rightarrow> 8) minDom \<le> qdom; qdom \<le> UCAST(32 signed \<rightarrow> 8) maxDom; UCAST(32 signed \<rightarrow> 8) seL4_MinPrio \<le> prio; prio \<le> UCAST(32 signed \<rightarrow> 8) seL4_MaxPrio; StateRelation_C.end_C (cq.[cready_queues_index_to_C qdom prio]) = (if aq (qdom, prio) = [] then NULL else tcb_ptr_to_ctcb_ptr (last (aq (qdom, prio)))); mp' x = None; map_option tcb_null_ep_ptrs (mp x) = map_option tcb_null_ep_ptrs None\<rbrakk> \<Longrightarrow> (map_option tcbSchedPrev_C \<circ> mp') x = (map_option tcbSchedPrev_C \<circ> mp) x
 2. \<And>qdom prio x a. \<lbrakk>\<forall>qdom prio. (UCAST(32 signed \<rightarrow> 8) seL4_MinPrio \<le> prio \<longrightarrow> qdom \<le> UCAST(32 signed \<rightarrow> 8) maxDom \<longrightarrow> UCAST(32 signed \<rightarrow> 8) minDom \<le> qdom \<longrightarrow> \<not> prio \<le> UCAST(32 signed \<rightarrow> 8) seL4_MaxPrio) \<longrightarrow> aq (qdom, prio) = []; UCAST(32 signed \<rightarrow> 8) minDom \<le> qdom; qdom \<le> UCAST(32 signed \<rightarrow> 8) maxDom; UCAST(32 signed \<rightarrow> 8) seL4_MinPrio \<le> prio; prio \<le> UCAST(32 signed \<rightarrow> 8) seL4_MaxPrio; StateRelation_C.end_C (cq.[cready_queues_index_to_C qdom prio]) = (if aq (qdom, prio) = [] then NULL else tcb_ptr_to_ctcb_ptr (last (aq (qdom, prio)))); mp' x = Some a\<rbrakk> \<Longrightarrow> (map_option tcbSchedPrev_C \<circ> mp') x = (map_option tcbSchedPrev_C \<circ> mp) x proof (prove)
goal (1 subgoal):
 1. \<And>qdom prio x a. \<lbrakk>\<forall>qdom prio. (UCAST(32 signed \<rightarrow> 8) seL4_MinPrio \<le> prio \<longrightarrow> qdom \<le> UCAST(32 signed \<rightarrow> 8) maxDom \<longrightarrow> UCAST(32 signed \<rightarrow> 8) minDom \<le> qdom \<longrightarrow> \<not> prio \<le> UCAST(32 signed \<rightarrow> 8) seL4_MaxPrio) \<longrightarrow> aq (qdom, prio) = []; UCAST(32 signed \<rightarrow> 8) minDom \<le> qdom; qdom \<le> UCAST(32 signed \<rightarrow> 8) maxDom; UCAST(32 signed \<rightarrow> 8) seL4_MinPrio \<le> prio; prio \<le> UCAST(32 signed \<rightarrow> 8) seL4_MaxPrio; StateRelation_C.end_C (cq.[cready_queues_index_to_C qdom prio]) = (if aq (qdom, prio) = [] then NULL else tcb_ptr_to_ctcb_ptr (last (aq (qdom, prio)))); mp' x = Some a\<rbrakk> \<Longrightarrow> (map_option tcbSchedPrev_C \<circ> mp') x = (map_option tcbSchedPrev_C \<circ> mp) x proof (prove)
goal (1 subgoal):
 1. \<And>qdom prio x a. \<lbrakk>\<forall>qdom prio. (UCAST(32 signed \<rightarrow> 8) seL4_MinPrio \<le> prio \<longrightarrow> qdom \<le> UCAST(32 signed \<rightarrow> 8) maxDom \<longrightarrow> UCAST(32 signed \<rightarrow> 8) minDom \<le> qdom \<longrightarrow> \<not> prio \<le> UCAST(32 signed \<rightarrow> 8) seL4_MaxPrio) \<longrightarrow> aq (qdom, prio) = []; UCAST(32 signed \<rightarrow> 8) minDom \<le> qdom; qdom \<le> UCAST(32 signed \<rightarrow> 8) maxDom; UCAST(32 signed \<rightarrow> 8) seL4_MinPrio \<le> prio; prio \<le> UCAST(32 signed \<rightarrow> 8) seL4_MaxPrio; StateRelation_C.end_C (cq.[cready_queues_index_to_C qdom prio]) = (if aq (qdom, prio) = [] then NULL else tcb_ptr_to_ctcb_ptr (last (aq (qdom, prio)))); mp' x = Some a; map_option tcb_null_ep_ptrs (mp x) = map_option tcb_null_ep_ptrs (Some a)\<rbrakk> \<Longrightarrow> (map_option tcbSchedPrev_C \<circ> mp') x = (map_option tcbSchedPrev_C \<circ> mp) x proof (prove)
goal (1 subgoal):
 1. \<And>qdom prio x a z. \<lbrakk>\<forall>qdom prio. (UCAST(32 signed \<rightarrow> 8) seL4_MinPrio \<le> prio \<longrightarrow> qdom \<le> UCAST(32 signed \<rightarrow> 8) maxDom \<longrightarrow> UCAST(32 signed \<rightarrow> 8) minDom \<le> qdom \<longrightarrow> \<not> prio \<le> UCAST(32 signed \<rightarrow> 8) seL4_MaxPrio) \<longrightarrow> aq (qdom, prio) = []; UCAST(32 signed \<rightarrow> 8) minDom \<le> qdom; qdom \<le> UCAST(32 signed \<rightarrow> 8) maxDom; UCAST(32 signed \<rightarrow> 8) seL4_MinPrio \<le> prio; prio \<le> UCAST(32 signed \<rightarrow> 8) seL4_MaxPrio; StateRelation_C.end_C (cq.[cready_queues_index_to_C qdom prio]) = (if aq (qdom, prio) = [] then NULL else tcb_ptr_to_ctcb_ptr (last (aq (qdom, prio)))); mp' x = Some a; mp x = Some z; tcbEPPrev_C_update (\<lambda>_. NULL) (tcbEPNext_C_update (\<lambda>_. NULL) z) = tcbEPPrev_C_update (\<lambda>_. NULL) (tcbEPNext_C_update (\<lambda>_. NULL) a)\<rbrakk> \<Longrightarrow> tcbSchedPrev_C a = tcbSchedPrev_C z proof (prove)
goal (1 subgoal):
 1. \<And>qdom prio x a z x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x1a x2a x3a x4a x5a x6a x7a x8a x9a x10a x11a x12a x13a x14a x15a. \<lbrakk>\<forall>qdom prio. (UCAST(32 signed \<rightarrow> 8) seL4_MinPrio \<le> prio \<longrightarrow> qdom \<le> UCAST(32 signed \<rightarrow> 8) maxDom \<longrightarrow> UCAST(32 signed \<rightarrow> 8) minDom \<le> qdom \<longrightarrow> \<not> prio \<le> UCAST(32 signed \<rightarrow> 8) seL4_MaxPrio) \<longrightarrow> aq (qdom, prio) = []; UCAST(32 signed \<rightarrow> 8) minDom \<le> qdom; qdom \<le> UCAST(32 signed \<rightarrow> 8) maxDom; UCAST(32 signed \<rightarrow> 8) seL4_MinPrio \<le> prio; prio \<le> UCAST(32 signed \<rightarrow> 8) seL4_MaxPrio; StateRelation_C.end_C (cq.[cready_queues_index_to_C qdom prio]) = (if aq (qdom, prio) = [] then NULL else tcb_ptr_to_ctcb_ptr (last (aq (qdom, prio)))); mp' x = Some a; mp x = Some z; tcbEPPrev_C_update (\<lambda>_. NULL) (tcbEPNext_C_update (\<lambda>_. NULL) z) = tcbEPPrev_C_update (\<lambda>_. NULL) (tcbEPNext_C_update (\<lambda>_. NULL) a); z = tcb_C.tcb_C x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15; a = tcb_C.tcb_C x1a x2a x3a x4a x5a x6a x7a x8a x9a x10a x11a x12a x13a x14a x15a\<rbrakk> \<Longrightarrow> tcbSchedPrev_C a = tcbSchedPrev_C z proof (prove)
goal:
No subgoals!