theory IpcCancel_C

lemma cready_queues_relation_empty_queue_helper:
  "\<lbrakk> tcbDomain ko \<le> maxDomain ; tcbPriority ko \<le> maxPriority ;
     cready_queues_relation (cslift \<sigma>') (ksReadyQueues_' (globals \<sigma>')) (ksReadyQueues \<sigma>)\<rbrakk>
   \<Longrightarrow>
   cready_queues_relation (cslift \<sigma>')
          (Arrays.update (ksReadyQueues_' (globals \<sigma>')) (unat (tcbDomain ko) * 256 + unat (tcbPriority ko))
            (tcb_queue_C.end_C_update (\<lambda>_. NULL)
              (head_C_update (\<lambda>_. NULL)
                (ksReadyQueues_' (globals \<sigma>').[unat (tcbDomain ko) * 256 + unat (tcbPriority ko)]))))
          ((ksReadyQueues \<sigma>)((tcbDomain ko, tcbPriority ko) := []))" unfolding cready_queues_relation_def Let_def using maxPrio_to_H[simp] maxDom_to_H[simp] apply clarsimp apply (frule (1) cready_queues_index_to_C_in_range[simplified maxDom_to_H maxPrio_to_H]) apply (fold cready_queues_index_to_C_def[simplified numPriorities_def]) apply (case_tac "qdom = tcbDomain ko",
          simp_all add: prio_and_dom_limit_helpers seL4_MinPrio_def
                        minDom_def) apply (fastforce simp: cready_queues_index_to_C_in_range simp: cready_queues_index_to_C_distinct)+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>tcbDomain ko \<le> maxDomain; tcbPriority ko \<le> maxPriority; cready_queues_relation (cslift \<sigma>') (ksReadyQueues_' (globals \<sigma>')) (ksReadyQueues \<sigma>)\<rbrakk> \<Longrightarrow> cready_queues_relation (cslift \<sigma>') (Arrays.update (ksReadyQueues_' (globals \<sigma>')) (unat (tcbDomain ko) * 256 + unat (tcbPriority ko)) (tcb_queue_C.end_C_update (\<lambda>_. NULL) (head_C_update (\<lambda>_. NULL) (ksReadyQueues_' (globals \<sigma>').[unat (tcbDomain ko) * 256 + unat (tcbPriority ko)])))) ((ksReadyQueues \<sigma>)((tcbDomain ko, tcbPriority ko) := [])) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>tcbDomain ko \<le> maxDomain; tcbPriority ko \<le> maxPriority; \<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' (cslift \<sigma>') (ksReadyQueues \<sigma> (qdom, prio)) (head_C (ksReadyQueues_' (globals \<sigma>').[cready_queues_index_to_C qdom prio])) (StateRelation_C.end_C (ksReadyQueues_' (globals \<sigma>').[cready_queues_index_to_C qdom prio]))) \<and> (\<not> (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> ksReadyQueues \<sigma> (qdom, prio) = [])\<rbrakk> \<Longrightarrow> \<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' (cslift \<sigma>') (((ksReadyQueues \<sigma>)((tcbDomain ko, tcbPriority ko) := [])) (qdom, prio)) (head_C (Arrays.update (ksReadyQueues_' (globals \<sigma>')) (unat (tcbDomain ko) * 256 + unat (tcbPriority ko)) (tcb_queue_C.end_C_update (\<lambda>_. NULL) (head_C_update (\<lambda>_. NULL) (ksReadyQueues_' (globals \<sigma>').[unat (tcbDomain ko) * 256 + unat (tcbPriority ko)]))).[cready_queues_index_to_C qdom prio])) (StateRelation_C.end_C (Arrays.update (ksReadyQueues_' (globals \<sigma>')) (unat (tcbDomain ko) * 256 + unat (tcbPriority ko)) (tcb_queue_C.end_C_update (\<lambda>_. NULL) (head_C_update (\<lambda>_. NULL) (ksReadyQueues_' (globals \<sigma>').[unat (tcbDomain ko) * 256 + unat (tcbPriority ko)]))).[cready_queues_index_to_C qdom prio]))) \<and> (\<not> (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> ((ksReadyQueues \<sigma>)((tcbDomain ko, tcbPriority ko) := [])) (qdom, prio) = []) proof (prove)
using this:
UCAST(32 signed \<rightarrow> 8) seL4_MaxPrio = maxPriority
UCAST(32 signed \<rightarrow> 8) maxDom = maxDomain

goal (1 subgoal):
 1. \<lbrakk>tcbDomain ko \<le> maxDomain; tcbPriority ko \<le> maxPriority; \<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' (cslift \<sigma>') (ksReadyQueues \<sigma> (qdom, prio)) (head_C (ksReadyQueues_' (globals \<sigma>').[cready_queues_index_to_C qdom prio])) (StateRelation_C.end_C (ksReadyQueues_' (globals \<sigma>').[cready_queues_index_to_C qdom prio]))) \<and> (\<not> (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> ksReadyQueues \<sigma> (qdom, prio) = [])\<rbrakk> \<Longrightarrow> \<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' (cslift \<sigma>') (((ksReadyQueues \<sigma>)((tcbDomain ko, tcbPriority ko) := [])) (qdom, prio)) (head_C (Arrays.update (ksReadyQueues_' (globals \<sigma>')) (unat (tcbDomain ko) * 256 + unat (tcbPriority ko)) (tcb_queue_C.end_C_update (\<lambda>_. NULL) (head_C_update (\<lambda>_. NULL) (ksReadyQueues_' (globals \<sigma>').[unat (tcbDomain ko) * 256 + unat (tcbPriority ko)]))).[cready_queues_index_to_C qdom prio])) (StateRelation_C.end_C (Arrays.update (ksReadyQueues_' (globals \<sigma>')) (unat (tcbDomain ko) * 256 + unat (tcbPriority ko)) (tcb_queue_C.end_C_update (\<lambda>_. NULL) (head_C_update (\<lambda>_. NULL) (ksReadyQueues_' (globals \<sigma>').[unat (tcbDomain ko) * 256 + unat (tcbPriority ko)]))).[cready_queues_index_to_C qdom prio]))) \<and> (\<not> (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> ((ksReadyQueues \<sigma>)((tcbDomain ko, tcbPriority ko) := [])) (qdom, prio) = []) proof (prove)
goal (1 subgoal):
 1. \<And>qdom prio. \<lbrakk>tcbDomain ko \<le> maxDomain; tcbPriority ko \<le> maxPriority; \<forall>qdom prio. (UCAST(32 signed \<rightarrow> 8) minDom \<le> qdom \<and> qdom \<le> maxDomain \<and> UCAST(32 signed \<rightarrow> 8) seL4_MinPrio \<le> prio \<and> prio \<le> maxPriority \<longrightarrow> sched_queue_relation' (cslift \<sigma>') (ksReadyQueues \<sigma> (qdom, prio)) (head_C (ksReadyQueues_' (globals \<sigma>').[cready_queues_index_to_C qdom prio])) (StateRelation_C.end_C (ksReadyQueues_' (globals \<sigma>').[cready_queues_index_to_C qdom prio]))) \<and> ((UCAST(32 signed \<rightarrow> 8) seL4_MinPrio \<le> prio \<longrightarrow> qdom \<le> maxDomain \<longrightarrow> UCAST(32 signed \<rightarrow> 8) minDom \<le> qdom \<longrightarrow> \<not> prio \<le> maxPriority) \<longrightarrow> ksReadyQueues \<sigma> (qdom, prio) = [])\<rbrakk> \<Longrightarrow> (qdom = tcbDomain ko \<and> prio = tcbPriority ko \<longrightarrow> UCAST(32 signed \<rightarrow> 8) minDom \<le> tcbDomain ko \<and> UCAST(32 signed \<rightarrow> 8) seL4_MinPrio \<le> tcbPriority ko \<longrightarrow> StateRelation_C.end_C (Arrays.update (ksReadyQueues_' (globals \<sigma>')) (unat (tcbDomain ko) * 256 + unat (tcbPriority ko)) (tcb_queue_C.end_C_update (\<lambda>_. NULL) (head_C_update (\<lambda>_. NULL) (ksReadyQueues_' (globals \<sigma>').[unat (tcbDomain ko) * 256 + unat (tcbPriority ko)]))).[cready_queues_index_to_C (tcbDomain ko) (tcbPriority ko)]) = NULL \<and> head_C (Arrays.update (ksReadyQueues_' (globals \<sigma>')) (unat (tcbDomain ko) * 256 + unat (tcbPriority ko)) (tcb_queue_C.end_C_update (\<lambda>_. NULL) (head_C_update (\<lambda>_. NULL) (ksReadyQueues_' (globals \<sigma>').[unat (tcbDomain ko) * 256 + unat (tcbPriority ko)]))).[cready_queues_index_to_C (tcbDomain ko) (tcbPriority ko)]) = NULL) \<and> ((qdom = tcbDomain ko \<longrightarrow> prio \<noteq> tcbPriority ko) \<longrightarrow> UCAST(32 signed \<rightarrow> 8) minDom \<le> qdom \<and> qdom \<le> maxDomain \<and> UCAST(32 signed \<rightarrow> 8) seL4_MinPrio \<le> prio \<and> prio \<le> maxPriority \<longrightarrow> sched_queue_relation' (cslift \<sigma>') (ksReadyQueues \<sigma> (qdom, prio)) (head_C (Arrays.update (ksReadyQueues_' (globals \<sigma>')) (unat (tcbDomain ko) * 256 + unat (tcbPriority ko)) (tcb_queue_C.end_C_update (\<lambda>_. NULL) (head_C_update (\<lambda>_. NULL) (ksReadyQueues_' (globals \<sigma>').[unat (tcbDomain ko) * 256 + unat (tcbPriority ko)]))).[cready_queues_index_to_C qdom prio])) (StateRelation_C.end_C (Arrays.update (ksReadyQueues_' (globals \<sigma>')) (unat (tcbDomain ko) * 256 + unat (tcbPriority ko)) (tcb_queue_C.end_C_update (\<lambda>_. NULL) (head_C_update (\<lambda>_. NULL) (ksReadyQueues_' (globals \<sigma>').[unat (tcbDomain ko) * 256 + unat (tcbPriority ko)]))).[cready_queues_index_to_C qdom prio]))) proof (prove)
goal (1 subgoal):
 1. \<And>qdom prio. \<lbrakk>tcbDomain ko \<le> maxDomain; tcbPriority ko \<le> maxPriority; \<forall>qdom prio. (UCAST(32 signed \<rightarrow> 8) minDom \<le> qdom \<and> qdom \<le> maxDomain \<and> UCAST(32 signed \<rightarrow> 8) seL4_MinPrio \<le> prio \<and> prio \<le> maxPriority \<longrightarrow> sched_queue_relation' (cslift \<sigma>') (ksReadyQueues \<sigma> (qdom, prio)) (head_C (ksReadyQueues_' (globals \<sigma>').[cready_queues_index_to_C qdom prio])) (StateRelation_C.end_C (ksReadyQueues_' (globals \<sigma>').[cready_queues_index_to_C qdom prio]))) \<and> ((UCAST(32 signed \<rightarrow> 8) seL4_MinPrio \<le> prio \<longrightarrow> qdom \<le> maxDomain \<longrightarrow> UCAST(32 signed \<rightarrow> 8) minDom \<le> qdom \<longrightarrow> \<not> prio \<le> maxPriority) \<longrightarrow> ksReadyQueues \<sigma> (qdom, prio) = []); cready_queues_index_to_C (tcbDomain ko) (tcbPriority ko) < 4096\<rbrakk> \<Longrightarrow> (qdom = tcbDomain ko \<and> prio = tcbPriority ko \<longrightarrow> UCAST(32 signed \<rightarrow> 8) minDom \<le> tcbDomain ko \<and> UCAST(32 signed \<rightarrow> 8) seL4_MinPrio \<le> tcbPriority ko \<longrightarrow> StateRelation_C.end_C (Arrays.update (ksReadyQueues_' (globals \<sigma>')) (unat (tcbDomain ko) * 256 + unat (tcbPriority ko)) (tcb_queue_C.end_C_update (\<lambda>_. NULL) (head_C_update (\<lambda>_. NULL) (ksReadyQueues_' (globals \<sigma>').[unat (tcbDomain ko) * 256 + unat (tcbPriority ko)]))).[cready_queues_index_to_C (tcbDomain ko) (tcbPriority ko)]) = NULL \<and> head_C (Arrays.update (ksReadyQueues_' (globals \<sigma>')) (unat (tcbDomain ko) * 256 + unat (tcbPriority ko)) (tcb_queue_C.end_C_update (\<lambda>_. NULL) (head_C_update (\<lambda>_. NULL) (ksReadyQueues_' (globals \<sigma>').[unat (tcbDomain ko) * 256 + unat (tcbPriority ko)]))).[cready_queues_index_to_C (tcbDomain ko) (tcbPriority ko)]) = NULL) \<and> ((qdom = tcbDomain ko \<longrightarrow> prio \<noteq> tcbPriority ko) \<longrightarrow> UCAST(32 signed \<rightarrow> 8) minDom \<le> qdom \<and> qdom \<le> maxDomain \<and> UCAST(32 signed \<rightarrow> 8) seL4_MinPrio \<le> prio \<and> prio \<le> maxPriority \<longrightarrow> sched_queue_relation' (cslift \<sigma>') (ksReadyQueues \<sigma> (qdom, prio)) (head_C (Arrays.update (ksReadyQueues_' (globals \<sigma>')) (unat (tcbDomain ko) * 256 + unat (tcbPriority ko)) (tcb_queue_C.end_C_update (\<lambda>_. NULL) (head_C_update (\<lambda>_. NULL) (ksReadyQueues_' (globals \<sigma>').[unat (tcbDomain ko) * 256 + unat (tcbPriority ko)]))).[cready_queues_index_to_C qdom prio])) (StateRelation_C.end_C (Arrays.update (ksReadyQueues_' (globals \<sigma>')) (unat (tcbDomain ko) * 256 + unat (tcbPriority ko)) (tcb_queue_C.end_C_update (\<lambda>_. NULL) (head_C_update (\<lambda>_. NULL) (ksReadyQueues_' (globals \<sigma>').[unat (tcbDomain ko) * 256 + unat (tcbPriority ko)]))).[cready_queues_index_to_C qdom prio]))) proof (prove)
goal (1 subgoal):
 1. \<And>qdom prio. \<lbrakk>tcbDomain ko \<le> maxDomain; tcbPriority ko \<le> maxPriority; \<forall>qdom prio. (UCAST(32 signed \<rightarrow> 8) minDom \<le> qdom \<and> qdom \<le> maxDomain \<and> UCAST(32 signed \<rightarrow> 8) seL4_MinPrio \<le> prio \<and> prio \<le> maxPriority \<longrightarrow> sched_queue_relation' (cslift \<sigma>') (ksReadyQueues \<sigma> (qdom, prio)) (head_C (ksReadyQueues_' (globals \<sigma>').[cready_queues_index_to_C qdom prio])) (StateRelation_C.end_C (ksReadyQueues_' (globals \<sigma>').[cready_queues_index_to_C qdom prio]))) \<and> ((UCAST(32 signed \<rightarrow> 8) seL4_MinPrio \<le> prio \<longrightarrow> qdom \<le> maxDomain \<longrightarrow> UCAST(32 signed \<rightarrow> 8) minDom \<le> qdom \<longrightarrow> \<not> prio \<le> maxPriority) \<longrightarrow> ksReadyQueues \<sigma> (qdom, prio) = []); cready_queues_index_to_C (tcbDomain ko) (tcbPriority ko) < 4096\<rbrakk> \<Longrightarrow> (qdom = tcbDomain ko \<and> prio = tcbPriority ko \<longrightarrow> UCAST(32 signed \<rightarrow> 8) minDom \<le> tcbDomain ko \<and> UCAST(32 signed \<rightarrow> 8) seL4_MinPrio \<le> tcbPriority ko \<longrightarrow> StateRelation_C.end_C (Arrays.update (ksReadyQueues_' (globals \<sigma>')) (cready_queues_index_to_C (tcbDomain ko) (tcbPriority ko)) (tcb_queue_C.end_C_update (\<lambda>_. NULL) (head_C_update (\<lambda>_. NULL) (ksReadyQueues_' (globals \<sigma>').[cready_queues_index_to_C (tcbDomain ko) (tcbPriority ko)]))).[cready_queues_index_to_C (tcbDomain ko) (tcbPriority ko)]) = NULL \<and> head_C (Arrays.update (ksReadyQueues_' (globals \<sigma>')) (cready_queues_index_to_C (tcbDomain ko) (tcbPriority ko)) (tcb_queue_C.end_C_update (\<lambda>_. NULL) (head_C_update (\<lambda>_. NULL) (ksReadyQueues_' (globals \<sigma>').[cready_queues_index_to_C (tcbDomain ko) (tcbPriority ko)]))).[cready_queues_index_to_C (tcbDomain ko) (tcbPriority ko)]) = NULL) \<and> ((qdom = tcbDomain ko \<longrightarrow> prio \<noteq> tcbPriority ko) \<longrightarrow> UCAST(32 signed \<rightarrow> 8) minDom \<le> qdom \<and> qdom \<le> maxDomain \<and> UCAST(32 signed \<rightarrow> 8) seL4_MinPrio \<le> prio \<and> prio \<le> maxPriority \<longrightarrow> sched_queue_relation' (cslift \<sigma>') (ksReadyQueues \<sigma> (qdom, prio)) (head_C (Arrays.update (ksReadyQueues_' (globals \<sigma>')) (cready_queues_index_to_C (tcbDomain ko) (tcbPriority ko)) (tcb_queue_C.end_C_update (\<lambda>_. NULL) (head_C_update (\<lambda>_. NULL) (ksReadyQueues_' (globals \<sigma>').[cready_queues_index_to_C (tcbDomain ko) (tcbPriority ko)]))).[cready_queues_index_to_C qdom prio])) (StateRelation_C.end_C (Arrays.update (ksReadyQueues_' (globals \<sigma>')) (cready_queues_index_to_C (tcbDomain ko) (tcbPriority ko)) (tcb_queue_C.end_C_update (\<lambda>_. NULL) (head_C_update (\<lambda>_. NULL) (ksReadyQueues_' (globals \<sigma>').[cready_queues_index_to_C (tcbDomain ko) (tcbPriority ko)]))).[cready_queues_index_to_C qdom prio]))) proof (prove)
goal (2 subgoals):
 1. \<And>qdom prio. \<lbrakk>tcbDomain ko \<le> maxDomain; tcbPriority ko \<le> maxPriority; \<forall>qdom prio. (qdom \<le> maxDomain \<and> prio \<le> maxPriority \<longrightarrow> sched_queue_relation' (cslift \<sigma>') (ksReadyQueues \<sigma> (qdom, prio)) (head_C (ksReadyQueues_' (globals \<sigma>').[cready_queues_index_to_C qdom prio])) (StateRelation_C.end_C (ksReadyQueues_' (globals \<sigma>').[cready_queues_index_to_C qdom prio]))) \<and> ((qdom \<le> maxDomain \<longrightarrow> \<not> prio \<le> maxPriority) \<longrightarrow> ksReadyQueues \<sigma> (qdom, prio) = []); cready_queues_index_to_C (tcbDomain ko) (tcbPriority ko) < 4096; qdom = tcbDomain ko\<rbrakk> \<Longrightarrow> prio \<noteq> tcbPriority ko \<longrightarrow> prio \<le> maxPriority \<longrightarrow> sched_queue_relation' (cslift \<sigma>') (ksReadyQueues \<sigma> (tcbDomain ko, prio)) (head_C (Arrays.update (ksReadyQueues_' (globals \<sigma>')) (cready_queues_index_to_C (tcbDomain ko) (tcbPriority ko)) (tcb_queue_C.end_C_update (\<lambda>_. NULL) (head_C_update (\<lambda>_. NULL) (ksReadyQueues_' (globals \<sigma>').[cready_queues_index_to_C (tcbDomain ko) (tcbPriority ko)]))).[cready_queues_index_to_C (tcbDomain ko) prio])) (StateRelation_C.end_C (Arrays.update (ksReadyQueues_' (globals \<sigma>')) (cready_queues_index_to_C (tcbDomain ko) (tcbPriority ko)) (tcb_queue_C.end_C_update (\<lambda>_. NULL) (head_C_update (\<lambda>_. NULL) (ksReadyQueues_' (globals \<sigma>').[cready_queues_index_to_C (tcbDomain ko) (tcbPriority ko)]))).[cready_queues_index_to_C (tcbDomain ko) prio]))
 2. \<And>qdom prio. \<lbrakk>tcbDomain ko \<le> maxDomain; tcbPriority ko \<le> maxPriority; \<forall>qdom prio. (qdom \<le> maxDomain \<and> prio \<le> maxPriority \<longrightarrow> sched_queue_relation' (cslift \<sigma>') (ksReadyQueues \<sigma> (qdom, prio)) (head_C (ksReadyQueues_' (globals \<sigma>').[cready_queues_index_to_C qdom prio])) (StateRelation_C.end_C (ksReadyQueues_' (globals \<sigma>').[cready_queues_index_to_C qdom prio]))) \<and> ((qdom \<le> maxDomain \<longrightarrow> \<not> prio \<le> maxPriority) \<longrightarrow> ksReadyQueues \<sigma> (qdom, prio) = []); cready_queues_index_to_C (tcbDomain ko) (tcbPriority ko) < 4096; qdom \<noteq> tcbDomain ko\<rbrakk> \<Longrightarrow> qdom \<le> maxDomain \<and> prio \<le> maxPriority \<longrightarrow> sched_queue_relation' (cslift \<sigma>') (ksReadyQueues \<sigma> (qdom, prio)) (head_C (Arrays.update (ksReadyQueues_' (globals \<sigma>')) (cready_queues_index_to_C (tcbDomain ko) (tcbPriority ko)) (tcb_queue_C.end_C_update (\<lambda>_. NULL) (head_C_update (\<lambda>_. NULL) (ksReadyQueues_' (globals \<sigma>').[cready_queues_index_to_C (tcbDomain ko) (tcbPriority ko)]))).[cready_queues_index_to_C qdom prio])) (StateRelation_C.end_C (Arrays.update (ksReadyQueues_' (globals \<sigma>')) (cready_queues_index_to_C (tcbDomain ko) (tcbPriority ko)) (tcb_queue_C.end_C_update (\<lambda>_. NULL) (head_C_update (\<lambda>_. NULL) (ksReadyQueues_' (globals \<sigma>').[cready_queues_index_to_C (tcbDomain ko) (tcbPriority ko)]))).[cready_queues_index_to_C qdom prio])) proof (prove)
goal:
No subgoals!