theory CSpace1_R

lemma get_cap_corres_P:
  "corres (\<lambda>x y. cap_relation x (cteCap y) \<and> P x)
          (cte_wp_at P cslot_ptr)
          (pspace_aligned' and pspace_distinct')
          (get_cap cslot_ptr) (getCTE (cte_map cslot_ptr))" apply (rule corres_stronger_no_failI) apply (rule no_fail_pre, wp) apply clarsimp apply (drule cte_wp_at_norm) apply (clarsimp simp: state_relation_def) apply (drule (3) pspace_relation_ctes_ofI) apply (clarsimp simp: cte_wp_at_ctes_of) apply (cases cslot_ptr) apply (rename_tac oref cref) apply (clarsimp simp: cte_wp_at_def) apply (frule in_inv_by_hoareD[OF getCTE_inv]) apply (drule use_valid [where P="\<top>", OF _ getCTE_sp TrueI]) apply (clarsimp simp: state_relation_def) apply (drule pspace_relation_ctes_ofI) apply (simp add: cte_wp_at_def) apply assumption+ apply (clarsimp simp: cte_wp_at_ctes_of) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. corres (\<lambda>x y. cap_relation x (cteCap y) \<and> P x) (cte_wp_at P cslot_ptr) (pspace_aligned' and pspace_distinct') (get_cap cslot_ptr) (getCTE (cte_map cslot_ptr)) proof (prove)
goal (2 subgoals):
 1. True \<Longrightarrow> no_fail (\<lambda>s'. \<exists>s. cte_wp_at P cslot_ptr s \<and> (s, s') \<in> state_relation \<and> (pspace_aligned' and pspace_distinct') s') (getCTE (cte_map cslot_ptr))
 2. \<forall>(s, s')\<in>state_relation. cte_wp_at P cslot_ptr s \<and> (pspace_aligned' and pspace_distinct') s' \<longrightarrow> (\<forall>(r', t')\<in>fst (getCTE (cte_map cslot_ptr) s'). \<exists>(r, t)\<in>fst (get_cap cslot_ptr s). (t, t') \<in> state_relation \<and> cap_relation r (cteCap r') \<and> P r) proof (prove)
goal (2 subgoals):
 1. \<And>s. \<lbrakk>True; \<exists>sa. cte_wp_at P cslot_ptr sa \<and> (sa, s) \<in> state_relation \<and> (pspace_aligned' and pspace_distinct') s\<rbrakk> \<Longrightarrow> cte_wp_at' (\<lambda>_. True) (cte_map cslot_ptr) s
 2. \<forall>(s, s')\<in>state_relation. cte_wp_at P cslot_ptr s \<and> (pspace_aligned' and pspace_distinct') s' \<longrightarrow> (\<forall>(r', t')\<in>fst (getCTE (cte_map cslot_ptr) s'). \<exists>(r, t)\<in>fst (get_cap cslot_ptr s). (t, t') \<in> state_relation \<and> cap_relation r (cteCap r') \<and> P r) proof (prove)
goal (2 subgoals):
 1. \<And>s sa. \<lbrakk>cte_wp_at P cslot_ptr sa; (sa, s) \<in> state_relation; pspace_aligned' s; pspace_distinct' s\<rbrakk> \<Longrightarrow> cte_wp_at' (\<lambda>_. True) (cte_map cslot_ptr) s
 2. \<forall>(s, s')\<in>state_relation. cte_wp_at P cslot_ptr s \<and> (pspace_aligned' and pspace_distinct') s' \<longrightarrow> (\<forall>(r', t')\<in>fst (getCTE (cte_map cslot_ptr) s'). \<exists>(r, t)\<in>fst (get_cap cslot_ptr s). (t, t') \<in> state_relation \<and> cap_relation r (cteCap r') \<and> P r) proof (prove)
goal (2 subgoals):
 1. \<And>s sa. \<lbrakk>(sa, s) \<in> state_relation; pspace_aligned' s; pspace_distinct' s; \<exists>c. cte_wp_at ((=) c) cslot_ptr sa \<and> P c\<rbrakk> \<Longrightarrow> cte_wp_at' (\<lambda>_. True) (cte_map cslot_ptr) s
 2. \<forall>(s, s')\<in>state_relation. cte_wp_at P cslot_ptr s \<and> (pspace_aligned' and pspace_distinct') s' \<longrightarrow> (\<forall>(r', t')\<in>fst (getCTE (cte_map cslot_ptr) s'). \<exists>(r, t)\<in>fst (get_cap cslot_ptr s). (t, t') \<in> state_relation \<and> cap_relation r (cteCap r') \<and> P r) proof (prove)
goal (2 subgoals):
 1. \<And>s sa c. \<lbrakk>pspace_aligned' s; pspace_distinct' s; pspace_relation (kheap sa) (ksPSpace s); cte_wp_at ((=) c) cslot_ptr sa; P c; ekheap_relation (ekheap sa) (ksPSpace s); sched_act_relation (scheduler_action sa) (ksSchedulerAction s); ready_queues_relation (ready_queues sa) (ksReadyQueues s); ghost_relation (kheap sa) (gsUserPages s) (gsCNodes s); cdt_relation (swp (cte_wp_at (\<lambda>_. True)) sa) (cdt sa) (ctes_of s); cdt_list_relation (cdt_list sa) (cdt sa) (ctes_of s); revokable_relation (is_original_cap sa) (null_filter (caps_of_state sa)) (ctes_of s); (arch_state sa, ksArchState s) \<in> arch_state_relation; interrupt_state_relation (interrupt_irq_node sa) (interrupt_states sa) (ksInterruptState s); cur_thread sa = ksCurThread s; idle_thread sa = ksIdleThread s; machine_state sa = ksMachineState s; work_units_completed sa = ksWorkUnitsCompleted s; domain_index sa = ksDomScheduleIdx s; domain_list sa = ksDomSchedule s; cur_domain sa = ksCurDomain s; domain_time sa = ksDomainTime s\<rbrakk> \<Longrightarrow> cte_wp_at' (\<lambda>_. True) (cte_map cslot_ptr) s
 2. \<forall>(s, s')\<in>state_relation. cte_wp_at P cslot_ptr s \<and> (pspace_aligned' and pspace_distinct') s' \<longrightarrow> (\<forall>(r', t')\<in>fst (getCTE (cte_map cslot_ptr) s'). \<exists>(r, t)\<in>fst (get_cap cslot_ptr s). (t, t') \<in> state_relation \<and> cap_relation r (cteCap r') \<and> P r) proof (prove)
goal (2 subgoals):
 1. \<And>s sa c. \<lbrakk>pspace_aligned' s; pspace_distinct' s; cte_wp_at ((=) c) cslot_ptr sa; P c; ekheap_relation (ekheap sa) (ksPSpace s); sched_act_relation (scheduler_action sa) (ksSchedulerAction s); ready_queues_relation (ready_queues sa) (ksReadyQueues s); ghost_relation (kheap sa) (gsUserPages s) (gsCNodes s); cdt_relation (swp (cte_wp_at (\<lambda>_. True)) sa) (cdt sa) (ctes_of s); cdt_list_relation (cdt_list sa) (cdt sa) (ctes_of s); revokable_relation (is_original_cap sa) (null_filter (caps_of_state sa)) (ctes_of s); (arch_state sa, ksArchState s) \<in> arch_state_relation; interrupt_state_relation (interrupt_irq_node sa) (interrupt_states sa) (ksInterruptState s); cur_thread sa = ksCurThread s; idle_thread sa = ksIdleThread s; machine_state sa = ksMachineState s; work_units_completed sa = ksWorkUnitsCompleted s; domain_index sa = ksDomScheduleIdx s; domain_list sa = ksDomSchedule s; cur_domain sa = ksCurDomain s; domain_time sa = ksDomainTime s; \<exists>cte. ctes_of s (cte_map cslot_ptr) = Some cte \<and> cap_relation c (cteCap cte)\<rbrakk> \<Longrightarrow> cte_wp_at' (\<lambda>_. True) (cte_map cslot_ptr) s
 2. \<forall>(s, s')\<in>state_relation. cte_wp_at P cslot_ptr s \<and> (pspace_aligned' and pspace_distinct') s' \<longrightarrow> (\<forall>(r', t')\<in>fst (getCTE (cte_map cslot_ptr) s'). \<exists>(r, t)\<in>fst (get_cap cslot_ptr s). (t, t') \<in> state_relation \<and> cap_relation r (cteCap r') \<and> P r) proof (prove)
goal (1 subgoal):
 1. \<forall>(s, s')\<in>state_relation. cte_wp_at P cslot_ptr s \<and> (pspace_aligned' and pspace_distinct') s' \<longrightarrow> (\<forall>(r', t')\<in>fst (getCTE (cte_map cslot_ptr) s'). \<exists>(r, t)\<in>fst (get_cap cslot_ptr s). (t, t') \<in> state_relation \<and> cap_relation r (cteCap r') \<and> P r) proof (prove)
goal (1 subgoal):
 1. \<And>a b. cslot_ptr = (a, b) \<Longrightarrow> \<forall>(s, s')\<in>state_relation. cte_wp_at P cslot_ptr s \<and> (pspace_aligned' and pspace_distinct') s' \<longrightarrow> (\<forall>(r', t')\<in>fst (getCTE (cte_map cslot_ptr) s'). \<exists>(r, t)\<in>fst (get_cap cslot_ptr s). (t, t') \<in> state_relation \<and> cap_relation r (cteCap r') \<and> P r) proof (prove)
goal (1 subgoal):
 1. \<And>oref cref. cslot_ptr = (oref, cref) \<Longrightarrow> \<forall>(s, s')\<in>state_relation. cte_wp_at P cslot_ptr s \<and> (pspace_aligned' and pspace_distinct') s' \<longrightarrow> (\<forall>(r', t')\<in>fst (getCTE (cte_map cslot_ptr) s'). \<exists>(r, t)\<in>fst (get_cap cslot_ptr s). (t, t') \<in> state_relation \<and> cap_relation r (cteCap r') \<and> P r) proof (prove)
goal (1 subgoal):
 1. \<And>oref cref a b aa ba cap. \<lbrakk>cslot_ptr = (oref, cref); (a, b) \<in> state_relation; (aa, ba) \<in> fst (getCTE (cte_map (oref, cref)) b); pspace_aligned' b; pspace_distinct' b; fst (get_cap (oref, cref) a) = {(cap, a)}; P cap\<rbrakk> \<Longrightarrow> (a, ba) \<in> state_relation \<and> cap_relation cap (cteCap aa) proof (prove)
goal (1 subgoal):
 1. \<And>oref cref a b aa ba cap. \<lbrakk>cslot_ptr = (oref, cref); (a, b) \<in> state_relation; (aa, ba) \<in> fst (getCTE (cte_map (oref, cref)) b); pspace_aligned' b; pspace_distinct' b; fst (get_cap (oref, cref) a) = {(cap, a)}; P cap; ba = b\<rbrakk> \<Longrightarrow> (a, ba) \<in> state_relation \<and> cap_relation cap (cteCap aa) proof (prove)
goal (1 subgoal):
 1. \<And>oref cref a b aa ba cap. \<lbrakk>cslot_ptr = (oref, cref); (a, b) \<in> state_relation; pspace_aligned' b; pspace_distinct' b; fst (get_cap (oref, cref) a) = {(cap, a)}; P cap; ba = b; (cte_wp_at' (\<lambda>c. c = aa) (cte_map (oref, cref)) and (\<lambda>_. True)) ba\<rbrakk> \<Longrightarrow> (a, ba) \<in> state_relation \<and> cap_relation cap (cteCap aa) proof (prove)
goal (1 subgoal):
 1. \<And>oref cref a b aa cap. \<lbrakk>cslot_ptr = (oref, cref); pspace_aligned' b; pspace_distinct' b; fst (get_cap (oref, cref) a) = {(cap, a)}; P cap; cte_wp_at' (\<lambda>c. c = aa) (cte_map (oref, cref)) b; pspace_relation (kheap a) (ksPSpace b); ekheap_relation (ekheap a) (ksPSpace b); sched_act_relation (scheduler_action a) (ksSchedulerAction b); ready_queues_relation (ready_queues a) (ksReadyQueues b); ghost_relation (kheap a) (gsUserPages b) (gsCNodes b); cdt_relation (swp (cte_wp_at (\<lambda>_. True)) a) (cdt a) (ctes_of b); cdt_list_relation (cdt_list a) (cdt a) (ctes_of b); revokable_relation (is_original_cap a) (null_filter (caps_of_state a)) (ctes_of b); (arch_state a, ksArchState b) \<in> arch_state_relation; interrupt_state_relation (interrupt_irq_node a) (interrupt_states a) (ksInterruptState b); cur_thread a = ksCurThread b; idle_thread a = ksIdleThread b; machine_state a = ksMachineState b; work_units_completed a = ksWorkUnitsCompleted b; domain_index a = ksDomScheduleIdx b; domain_list a = ksDomSchedule b; cur_domain a = ksCurDomain b; domain_time a = ksDomainTime b\<rbrakk> \<Longrightarrow> cap_relation cap (cteCap aa) proof (prove)
goal (4 subgoals):
 1. \<And>oref cref a b aa cap. \<lbrakk>cslot_ptr = (oref, cref); pspace_aligned' b; pspace_distinct' b; fst (get_cap (oref, cref) a) = {(cap, a)}; P cap; cte_wp_at' (\<lambda>c. c = aa) (cte_map (oref, cref)) b; ekheap_relation (ekheap a) (ksPSpace b); sched_act_relation (scheduler_action a) (ksSchedulerAction b); ready_queues_relation (ready_queues a) (ksReadyQueues b); ghost_relation (kheap a) (gsUserPages b) (gsCNodes b); cdt_relation (swp (cte_wp_at (\<lambda>_. True)) a) (cdt a) (ctes_of b); cdt_list_relation (cdt_list a) (cdt a) (ctes_of b); revokable_relation (is_original_cap a) (null_filter (caps_of_state a)) (ctes_of b); (arch_state a, ksArchState b) \<in> arch_state_relation; interrupt_state_relation (interrupt_irq_node a) (interrupt_states a) (ksInterruptState b); cur_thread a = ksCurThread b; idle_thread a = ksIdleThread b; machine_state a = ksMachineState b; work_units_completed a = ksWorkUnitsCompleted b; domain_index a = ksDomScheduleIdx b; domain_list a = ksDomSchedule b; cur_domain a = ksCurDomain b; domain_time a = ksDomainTime b\<rbrakk> \<Longrightarrow> cte_wp_at ((=) (?c77 oref cref a b aa cap)) (?slot77 oref cref a b aa cap) a
 2. \<And>oref cref a b aa cap. \<lbrakk>cslot_ptr = (oref, cref); pspace_aligned' b; pspace_distinct' b; fst (get_cap (oref, cref) a) = {(cap, a)}; P cap; cte_wp_at' (\<lambda>c. c = aa) (cte_map (oref, cref)) b; ekheap_relation (ekheap a) (ksPSpace b); sched_act_relation (scheduler_action a) (ksSchedulerAction b); ready_queues_relation (ready_queues a) (ksReadyQueues b); ghost_relation (kheap a) (gsUserPages b) (gsCNodes b); cdt_relation (swp (cte_wp_at (\<lambda>_. True)) a) (cdt a) (ctes_of b); cdt_list_relation (cdt_list a) (cdt a) (ctes_of b); revokable_relation (is_original_cap a) (null_filter (caps_of_state a)) (ctes_of b); (arch_state a, ksArchState b) \<in> arch_state_relation; interrupt_state_relation (interrupt_irq_node a) (interrupt_states a) (ksInterruptState b); cur_thread a = ksCurThread b; idle_thread a = ksIdleThread b; machine_state a = ksMachineState b; work_units_completed a = ksWorkUnitsCompleted b; domain_index a = ksDomScheduleIdx b; domain_list a = ksDomSchedule b; cur_domain a = ksCurDomain b; domain_time a = ksDomainTime b\<rbrakk> \<Longrightarrow> pspace_aligned' b
 3. \<And>oref cref a b aa cap. \<lbrakk>cslot_ptr = (oref, cref); pspace_aligned' b; pspace_distinct' b; fst (get_cap (oref, cref) a) = {(cap, a)}; P cap; cte_wp_at' (\<lambda>c. c = aa) (cte_map (oref, cref)) b; ekheap_relation (ekheap a) (ksPSpace b); sched_act_relation (scheduler_action a) (ksSchedulerAction b); ready_queues_relation (ready_queues a) (ksReadyQueues b); ghost_relation (kheap a) (gsUserPages b) (gsCNodes b); cdt_relation (swp (cte_wp_at (\<lambda>_. True)) a) (cdt a) (ctes_of b); cdt_list_relation (cdt_list a) (cdt a) (ctes_of b); revokable_relation (is_original_cap a) (null_filter (caps_of_state a)) (ctes_of b); (arch_state a, ksArchState b) \<in> arch_state_relation; interrupt_state_relation (interrupt_irq_node a) (interrupt_states a) (ksInterruptState b); cur_thread a = ksCurThread b; idle_thread a = ksIdleThread b; machine_state a = ksMachineState b; work_units_completed a = ksWorkUnitsCompleted b; domain_index a = ksDomScheduleIdx b; domain_list a = ksDomSchedule b; cur_domain a = ksCurDomain b; domain_time a = ksDomainTime b\<rbrakk> \<Longrightarrow> pspace_distinct' b
 4. \<And>oref cref a b aa cap. \<lbrakk>cslot_ptr = (oref, cref); pspace_aligned' b; pspace_distinct' b; fst (get_cap (oref, cref) a) = {(cap, a)}; P cap; cte_wp_at' (\<lambda>c. c = aa) (cte_map (oref, cref)) b; ekheap_relation (ekheap a) (ksPSpace b); sched_act_relation (scheduler_action a) (ksSchedulerAction b); ready_queues_relation (ready_queues a) (ksReadyQueues b); ghost_relation (kheap a) (gsUserPages b) (gsCNodes b); cdt_relation (swp (cte_wp_at (\<lambda>_. True)) a) (cdt a) (ctes_of b); cdt_list_relation (cdt_list a) (cdt a) (ctes_of b); revokable_relation (is_original_cap a) (null_filter (caps_of_state a)) (ctes_of b); (arch_state a, ksArchState b) \<in> arch_state_relation; interrupt_state_relation (interrupt_irq_node a) (interrupt_states a) (ksInterruptState b); cur_thread a = ksCurThread b; idle_thread a = ksIdleThread b; machine_state a = ksMachineState b; work_units_completed a = ksWorkUnitsCompleted b; domain_index a = ksDomScheduleIdx b; domain_list a = ksDomSchedule b; cur_domain a = ksCurDomain b; domain_time a = ksDomainTime b; \<exists>cte. ctes_of b (cte_map (?slot77 oref cref a b aa cap)) = Some cte \<and> cap_relation (?c77 oref cref a b aa cap) (cteCap cte)\<rbrakk> \<Longrightarrow> cap_relation cap (cteCap aa) proof (prove)
goal (3 subgoals):
 1. \<And>oref cref a b aa cap. \<lbrakk>cslot_ptr = (oref, cref); pspace_aligned' b; pspace_distinct' b; fst (get_cap (oref, cref) a) = {(cap, a)}; P cap; cte_wp_at' (\<lambda>c. c = aa) (cte_map (oref, cref)) b; ekheap_relation (ekheap a) (ksPSpace b); sched_act_relation (scheduler_action a) (ksSchedulerAction b); ready_queues_relation (ready_queues a) (ksReadyQueues b); ghost_relation (kheap a) (gsUserPages b) (gsCNodes b); cdt_relation (swp (cte_wp_at (\<lambda>_. True)) a) (cdt a) (ctes_of b); cdt_list_relation (cdt_list a) (cdt a) (ctes_of b); revokable_relation (is_original_cap a) (null_filter (caps_of_state a)) (ctes_of b); (arch_state a, ksArchState b) \<in> arch_state_relation; interrupt_state_relation (interrupt_irq_node a) (interrupt_states a) (ksInterruptState b); cur_thread a = ksCurThread b; idle_thread a = ksIdleThread b; machine_state a = ksMachineState b; work_units_completed a = ksWorkUnitsCompleted b; domain_index a = ksDomScheduleIdx b; domain_list a = ksDomSchedule b; cur_domain a = ksCurDomain b; domain_time a = ksDomainTime b\<rbrakk> \<Longrightarrow> pspace_aligned' b
 2. \<And>oref cref a b aa cap. \<lbrakk>cslot_ptr = (oref, cref); pspace_aligned' b; pspace_distinct' b; fst (get_cap (oref, cref) a) = {(cap, a)}; P cap; cte_wp_at' (\<lambda>c. c = aa) (cte_map (oref, cref)) b; ekheap_relation (ekheap a) (ksPSpace b); sched_act_relation (scheduler_action a) (ksSchedulerAction b); ready_queues_relation (ready_queues a) (ksReadyQueues b); ghost_relation (kheap a) (gsUserPages b) (gsCNodes b); cdt_relation (swp (cte_wp_at (\<lambda>_. True)) a) (cdt a) (ctes_of b); cdt_list_relation (cdt_list a) (cdt a) (ctes_of b); revokable_relation (is_original_cap a) (null_filter (caps_of_state a)) (ctes_of b); (arch_state a, ksArchState b) \<in> arch_state_relation; interrupt_state_relation (interrupt_irq_node a) (interrupt_states a) (ksInterruptState b); cur_thread a = ksCurThread b; idle_thread a = ksIdleThread b; machine_state a = ksMachineState b; work_units_completed a = ksWorkUnitsCompleted b; domain_index a = ksDomScheduleIdx b; domain_list a = ksDomSchedule b; cur_domain a = ksCurDomain b; domain_time a = ksDomainTime b\<rbrakk> \<Longrightarrow> pspace_distinct' b
 3. \<And>oref cref a b aa cap. \<lbrakk>cslot_ptr = (oref, cref); pspace_aligned' b; pspace_distinct' b; fst (get_cap (oref, cref) a) = {(cap, a)}; P cap; cte_wp_at' (\<lambda>c. c = aa) (cte_map (oref, cref)) b; ekheap_relation (ekheap a) (ksPSpace b); sched_act_relation (scheduler_action a) (ksSchedulerAction b); ready_queues_relation (ready_queues a) (ksReadyQueues b); ghost_relation (kheap a) (gsUserPages b) (gsCNodes b); cdt_relation (swp (cte_wp_at (\<lambda>_. True)) a) (cdt a) (ctes_of b); cdt_list_relation (cdt_list a) (cdt a) (ctes_of b); revokable_relation (is_original_cap a) (null_filter (caps_of_state a)) (ctes_of b); (arch_state a, ksArchState b) \<in> arch_state_relation; interrupt_state_relation (interrupt_irq_node a) (interrupt_states a) (ksInterruptState b); cur_thread a = ksCurThread b; idle_thread a = ksIdleThread b; machine_state a = ksMachineState b; work_units_completed a = ksWorkUnitsCompleted b; domain_index a = ksDomScheduleIdx b; domain_list a = ksDomSchedule b; cur_domain a = ksCurDomain b; domain_time a = ksDomainTime b; \<exists>cte. ctes_of b (cte_map (oref, cref)) = Some cte \<and> cap_relation cap (cteCap cte)\<rbrakk> \<Longrightarrow> cap_relation cap (cteCap aa) proof (prove)
goal (1 subgoal):
 1. \<And>oref cref a b aa cap. \<lbrakk>cslot_ptr = (oref, cref); pspace_aligned' b; pspace_distinct' b; fst (get_cap (oref, cref) a) = {(cap, a)}; P cap; cte_wp_at' (\<lambda>c. c = aa) (cte_map (oref, cref)) b; ekheap_relation (ekheap a) (ksPSpace b); sched_act_relation (scheduler_action a) (ksSchedulerAction b); ready_queues_relation (ready_queues a) (ksReadyQueues b); ghost_relation (kheap a) (gsUserPages b) (gsCNodes b); cdt_relation (swp (cte_wp_at (\<lambda>_. True)) a) (cdt a) (ctes_of b); cdt_list_relation (cdt_list a) (cdt a) (ctes_of b); revokable_relation (is_original_cap a) (null_filter (caps_of_state a)) (ctes_of b); (arch_state a, ksArchState b) \<in> arch_state_relation; interrupt_state_relation (interrupt_irq_node a) (interrupt_states a) (ksInterruptState b); cur_thread a = ksCurThread b; idle_thread a = ksIdleThread b; machine_state a = ksMachineState b; work_units_completed a = ksWorkUnitsCompleted b; domain_index a = ksDomScheduleIdx b; domain_list a = ksDomSchedule b; cur_domain a = ksCurDomain b; domain_time a = ksDomainTime b; \<exists>cte. ctes_of b (cte_map (oref, cref)) = Some cte \<and> cap_relation cap (cteCap cte)\<rbrakk> \<Longrightarrow> cap_relation cap (cteCap aa) proof (prove)
goal:
No subgoals!