theory Dpolicy

lemma state_objs_transform_rev:
  "\<lbrakk> einvs s; (x, a, y) \<in> cdl_state_objs_to_policy (transform s) \<rbrakk> \<Longrightarrow>
               (x, a, y) \<in> state_objs_to_policy s" apply (rule cdl_state_objs_to_policy_cases, simp) apply (rule_tac P="is_thread_state_cap cap" in case_split) apply simp apply (rule sta_ts) apply (rule thread_st_auth_transform_rev, simp+) apply (clarsimp simp:opt_cap_def transform_def transform_objects_def slots_of_def) apply (clarsimp simp: map_add_def object_slots_def) apply (rule_tac P="is_real_cap cap" in case_split[rotated]) apply (drule state_vrefs_transform_rev, simp+) apply clarsimp apply (rule sta_vref) apply simp apply (subgoal_tac "\<not> is_null_cap cap") prefer 2 apply (clarsimp simp:is_null_cap_def split:cdl_cap.splits) apply (rule_tac P="is_bound_ntfn_cap cap" in case_split) apply simp apply (rule sta_bas) apply (rule thread_bound_ntfns_transform_rev, simp+) apply (clarsimp simp: opt_cap_def transform_def transform_objects_def slots_of_def) apply (clarsimp simp: map_add_def object_slots_def) apply (clarsimp simp: cdl_cap_auth_conferred_def is_bound_ntfn_cap_def split: cdl_cap.splits) apply (frule caps_of_state_transform_opt_cap_rev, simp+) apply (rule_tac P="is_untyped_cap cap" in case_split) apply (subgoal_tac "a = Control") apply clarsimp apply (subst fst_transform_cslot_ptr[symmetric]) apply (rule_tac cap=cap' in sta_untyped) apply simp apply (subst (asm) untyped_range_transform[symmetric]) apply (simp add:is_untyped_cap_def transform_cap_def
                   split:cap.splits arch_cap.splits if_split_asm) apply simp apply (simp add:cdl_cap_auth_conferred_def is_untyped_cap_def split:cdl_cap.splits) apply clarsimp apply (subst fst_transform_cslot_ptr[symmetric]) apply (rule_tac cap=cap' in sta_caps) apply simp apply (subst (asm) obj_refs_transform[symmetric]) apply (simp add:is_untyped_cap_def transform_cap_def
                  split:cap.splits arch_cap.splits if_split_asm) apply simp apply (simp add:cap_auth_conferred_transform) apply (drule cdl_cdt_transform_rev [rotated], simp+) apply clarsimp apply (subst fst_transform_cslot_ptr[symmetric])+ apply (rule sta_cdt) apply simp apply (erule contrapos_nn) apply (frule invs_mdb_cte, drule mdb_cte_at_rewrite, clarsimp simp: mdb_cte_at_def) apply (erule is_transferable.cases) apply fastforce apply fastforce apply ((drule spec)+, erule(1) impE, clarsimp) apply (subst caps_of_state_transform_opt_cap) apply assumption apply fastforce apply (blast dest: idle_thread_null_cap) apply (clarsimp simp: transform_cap_def) apply (blast intro: cdl_cap_is_transferable.intros) apply clarsimp apply (frule(1) cdl_cdt_transform_rev) apply (clarsimp simp: transform_cslot_ptr_def) apply (erule sta_cdt_transferable
                 [where slot="(x, slot)" and slot'="(y, slot')" for slot slot', simplified]) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>einvs s; (x, a, y) \<in> cdl_state_objs_to_policy (transform s)\<rbrakk> \<Longrightarrow> (x, a, y) \<in> state_objs_to_policy s proof (prove)
goal (3 subgoals):
 1. \<And>ptr cap oref auth. \<lbrakk>einvs s; (x, a, y) \<in> cdl_state_objs_to_policy (transform s); x = fst ptr; a = auth; y = oref; opt_cap ptr (transform s) = Some cap; oref \<in> cdl_obj_refs cap; auth \<in> cdl_cap_auth_conferred cap\<rbrakk> \<Longrightarrow> (x, a, y) \<in> state_objs_to_policy s
 2. \<And>slot' slot. \<lbrakk>einvs s; (x, a, y) \<in> cdl_state_objs_to_policy (transform s); x = fst slot; a = Control; y = fst slot'; cdl_cdt (transform s) slot' = Some slot; \<not> cdl_cap_is_transferable (opt_cap slot' (transform s))\<rbrakk> \<Longrightarrow> (x, a, y) \<in> state_objs_to_policy s
 3. \<And>slot' slot. \<lbrakk>einvs s; (x, a, y) \<in> cdl_state_objs_to_policy (transform s); x = fst slot; a = DeleteDerived; y = fst slot'; cdl_cdt (transform s) slot' = Some slot\<rbrakk> \<Longrightarrow> (x, a, y) \<in> state_objs_to_policy s proof (prove)
goal (4 subgoals):
 1. \<And>ptr cap oref auth. \<lbrakk>einvs s; (x, a, y) \<in> cdl_state_objs_to_policy (transform s); x = fst ptr; a = auth; y = oref; opt_cap ptr (transform s) = Some cap; oref \<in> cdl_obj_refs cap; auth \<in> cdl_cap_auth_conferred cap; is_thread_state_cap cap\<rbrakk> \<Longrightarrow> (x, a, y) \<in> state_objs_to_policy s
 2. \<And>ptr cap oref auth. \<lbrakk>einvs s; (x, a, y) \<in> cdl_state_objs_to_policy (transform s); x = fst ptr; a = auth; y = oref; opt_cap ptr (transform s) = Some cap; oref \<in> cdl_obj_refs cap; auth \<in> cdl_cap_auth_conferred cap; \<not> is_thread_state_cap cap\<rbrakk> \<Longrightarrow> (x, a, y) \<in> state_objs_to_policy s
 3. \<And>slot' slot. \<lbrakk>einvs s; (x, a, y) \<in> cdl_state_objs_to_policy (transform s); x = fst slot; a = Control; y = fst slot'; cdl_cdt (transform s) slot' = Some slot; \<not> cdl_cap_is_transferable (opt_cap slot' (transform s))\<rbrakk> \<Longrightarrow> (x, a, y) \<in> state_objs_to_policy s
 4. \<And>slot' slot. \<lbrakk>einvs s; (x, a, y) \<in> cdl_state_objs_to_policy (transform s); x = fst slot; a = DeleteDerived; y = fst slot'; cdl_cdt (transform s) slot' = Some slot\<rbrakk> \<Longrightarrow> (x, a, y) \<in> state_objs_to_policy s proof (prove)
goal (4 subgoals):
 1. \<And>ptr cap oref auth. \<lbrakk>invs s \<and> valid_list s \<and> valid_sched s; (fst ptr, auth, oref) \<in> cdl_state_objs_to_policy (transform s); x = fst ptr; a = auth; y = oref; opt_cap ptr (transform s) = Some cap; oref \<in> cdl_obj_refs cap; auth \<in> cdl_cap_auth_conferred cap; is_thread_state_cap cap\<rbrakk> \<Longrightarrow> (fst ptr, auth, oref) \<in> state_objs_to_policy s
 2. \<And>ptr cap oref auth. \<lbrakk>einvs s; (x, a, y) \<in> cdl_state_objs_to_policy (transform s); x = fst ptr; a = auth; y = oref; opt_cap ptr (transform s) = Some cap; oref \<in> cdl_obj_refs cap; auth \<in> cdl_cap_auth_conferred cap; \<not> is_thread_state_cap cap\<rbrakk> \<Longrightarrow> (x, a, y) \<in> state_objs_to_policy s
 3. \<And>slot' slot. \<lbrakk>einvs s; (x, a, y) \<in> cdl_state_objs_to_policy (transform s); x = fst slot; a = Control; y = fst slot'; cdl_cdt (transform s) slot' = Some slot; \<not> cdl_cap_is_transferable (opt_cap slot' (transform s))\<rbrakk> \<Longrightarrow> (x, a, y) \<in> state_objs_to_policy s
 4. \<And>slot' slot. \<lbrakk>einvs s; (x, a, y) \<in> cdl_state_objs_to_policy (transform s); x = fst slot; a = DeleteDerived; y = fst slot'; cdl_cdt (transform s) slot' = Some slot\<rbrakk> \<Longrightarrow> (x, a, y) \<in> state_objs_to_policy s proof (prove)
goal (4 subgoals):
 1. \<And>ptr cap oref auth. \<lbrakk>invs s \<and> valid_list s \<and> valid_sched s; (fst ptr, auth, oref) \<in> cdl_state_objs_to_policy (transform s); x = fst ptr; a = auth; y = oref; opt_cap ptr (transform s) = Some cap; oref \<in> cdl_obj_refs cap; auth \<in> cdl_cap_auth_conferred cap; is_thread_state_cap cap\<rbrakk> \<Longrightarrow> (oref, auth) \<in> thread_st_auth s (fst ptr)
 2. \<And>ptr cap oref auth. \<lbrakk>einvs s; (x, a, y) \<in> cdl_state_objs_to_policy (transform s); x = fst ptr; a = auth; y = oref; opt_cap ptr (transform s) = Some cap; oref \<in> cdl_obj_refs cap; auth \<in> cdl_cap_auth_conferred cap; \<not> is_thread_state_cap cap\<rbrakk> \<Longrightarrow> (x, a, y) \<in> state_objs_to_policy s
 3. \<And>slot' slot. \<lbrakk>einvs s; (x, a, y) \<in> cdl_state_objs_to_policy (transform s); x = fst slot; a = Control; y = fst slot'; cdl_cdt (transform s) slot' = Some slot; \<not> cdl_cap_is_transferable (opt_cap slot' (transform s))\<rbrakk> \<Longrightarrow> (x, a, y) \<in> state_objs_to_policy s
 4. \<And>slot' slot. \<lbrakk>einvs s; (x, a, y) \<in> cdl_state_objs_to_policy (transform s); x = fst slot; a = DeleteDerived; y = fst slot'; cdl_cdt (transform s) slot' = Some slot\<rbrakk> \<Longrightarrow> (x, a, y) \<in> state_objs_to_policy s proof (prove)
goal (4 subgoals):
 1. \<And>ptr cap oref auth. \<lbrakk>invs s \<and> valid_list s \<and> valid_sched s; (fst ptr, auth, oref) \<in> cdl_state_objs_to_policy (transform s); x = fst ptr; a = auth; y = oref; opt_cap ptr (transform s) = Some cap; oref \<in> cdl_obj_refs cap; auth \<in> cdl_cap_auth_conferred cap; is_thread_state_cap cap\<rbrakk> \<Longrightarrow> fst ptr \<noteq> idle_thread s
 2. \<And>ptr cap oref auth. \<lbrakk>einvs s; (x, a, y) \<in> cdl_state_objs_to_policy (transform s); x = fst ptr; a = auth; y = oref; opt_cap ptr (transform s) = Some cap; oref \<in> cdl_obj_refs cap; auth \<in> cdl_cap_auth_conferred cap; \<not> is_thread_state_cap cap\<rbrakk> \<Longrightarrow> (x, a, y) \<in> state_objs_to_policy s
 3. \<And>slot' slot. \<lbrakk>einvs s; (x, a, y) \<in> cdl_state_objs_to_policy (transform s); x = fst slot; a = Control; y = fst slot'; cdl_cdt (transform s) slot' = Some slot; \<not> cdl_cap_is_transferable (opt_cap slot' (transform s))\<rbrakk> \<Longrightarrow> (x, a, y) \<in> state_objs_to_policy s
 4. \<And>slot' slot. \<lbrakk>einvs s; (x, a, y) \<in> cdl_state_objs_to_policy (transform s); x = fst slot; a = DeleteDerived; y = fst slot'; cdl_cdt (transform s) slot' = Some slot\<rbrakk> \<Longrightarrow> (x, a, y) \<in> state_objs_to_policy s proof (prove)
goal (4 subgoals):
 1. \<And>b cap. \<lbrakk>(idle_thread s, a, y) \<in> cdl_state_objs_to_policy \<lparr>cdl_arch = ARM11, cdl_objects = (\<lambda>ptr. Some cdl_object.Untyped) |` (- {idle_thread s}) ++ (\<lambda>ptr. map_option (transform_object (machine_state s) ptr ((ekheap s |` (- {idle_thread s})) ptr)) ((kheap s |` (- {idle_thread s})) ptr)), cdl_cdt = transform_cdt s, cdl_current_thread = transform_current_thread s, cdl_irq_node = interrupt_irq_node s, cdl_asid_table = transform_asid_table s, cdl_current_domain = cur_domain s\<rparr>; x = idle_thread s; (case ((\<lambda>ptr. Some cdl_object.Untyped) |` (- {idle_thread s}) ++ (\<lambda>ptr. map_option (transform_object (machine_state s) ptr ((ekheap s |` (- {idle_thread s})) ptr)) ((kheap s |` (- {idle_thread s})) ptr))) (idle_thread s) of None \<Rightarrow> \<lambda>x. None | Some x2 \<Rightarrow> object_slots x2) b = Some cap; y \<in> cdl_obj_refs cap; a \<in> cdl_cap_auth_conferred cap; is_thread_state_cap cap; invs s; valid_list s; valid_sched s\<rbrakk> \<Longrightarrow> False
 2. \<And>ptr cap oref auth. \<lbrakk>einvs s; (x, a, y) \<in> cdl_state_objs_to_policy (transform s); x = fst ptr; a = auth; y = oref; opt_cap ptr (transform s) = Some cap; oref \<in> cdl_obj_refs cap; auth \<in> cdl_cap_auth_conferred cap; \<not> is_thread_state_cap cap\<rbrakk> \<Longrightarrow> (x, a, y) \<in> state_objs_to_policy s
 3. \<And>slot' slot. \<lbrakk>einvs s; (x, a, y) \<in> cdl_state_objs_to_policy (transform s); x = fst slot; a = Control; y = fst slot'; cdl_cdt (transform s) slot' = Some slot; \<not> cdl_cap_is_transferable (opt_cap slot' (transform s))\<rbrakk> \<Longrightarrow> (x, a, y) \<in> state_objs_to_policy s
 4. \<And>slot' slot. \<lbrakk>einvs s; (x, a, y) \<in> cdl_state_objs_to_policy (transform s); x = fst slot; a = DeleteDerived; y = fst slot'; cdl_cdt (transform s) slot' = Some slot\<rbrakk> \<Longrightarrow> (x, a, y) \<in> state_objs_to_policy s proof (prove)
goal (3 subgoals):
 1. \<And>ptr cap oref auth. \<lbrakk>einvs s; (x, a, y) \<in> cdl_state_objs_to_policy (transform s); x = fst ptr; a = auth; y = oref; opt_cap ptr (transform s) = Some cap; oref \<in> cdl_obj_refs cap; auth \<in> cdl_cap_auth_conferred cap; \<not> is_thread_state_cap cap\<rbrakk> \<Longrightarrow> (x, a, y) \<in> state_objs_to_policy s
 2. \<And>slot' slot. \<lbrakk>einvs s; (x, a, y) \<in> cdl_state_objs_to_policy (transform s); x = fst slot; a = Control; y = fst slot'; cdl_cdt (transform s) slot' = Some slot; \<not> cdl_cap_is_transferable (opt_cap slot' (transform s))\<rbrakk> \<Longrightarrow> (x, a, y) \<in> state_objs_to_policy s
 3. \<And>slot' slot. \<lbrakk>einvs s; (x, a, y) \<in> cdl_state_objs_to_policy (transform s); x = fst slot; a = DeleteDerived; y = fst slot'; cdl_cdt (transform s) slot' = Some slot\<rbrakk> \<Longrightarrow> (x, a, y) \<in> state_objs_to_policy s proof (prove)
goal (4 subgoals):
 1. \<And>ptr cap oref auth. \<lbrakk>einvs s; (x, a, y) \<in> cdl_state_objs_to_policy (transform s); x = fst ptr; a = auth; y = oref; opt_cap ptr (transform s) = Some cap; oref \<in> cdl_obj_refs cap; auth \<in> cdl_cap_auth_conferred cap; \<not> is_thread_state_cap cap; \<not> is_real_cap cap\<rbrakk> \<Longrightarrow> (x, a, y) \<in> state_objs_to_policy s
 2. \<And>ptr cap oref auth. \<lbrakk>einvs s; (x, a, y) \<in> cdl_state_objs_to_policy (transform s); x = fst ptr; a = auth; y = oref; opt_cap ptr (transform s) = Some cap; oref \<in> cdl_obj_refs cap; auth \<in> cdl_cap_auth_conferred cap; \<not> is_thread_state_cap cap; is_real_cap cap\<rbrakk> \<Longrightarrow> (x, a, y) \<in> state_objs_to_policy s
 3. \<And>slot' slot. \<lbrakk>einvs s; (x, a, y) \<in> cdl_state_objs_to_policy (transform s); x = fst slot; a = Control; y = fst slot'; cdl_cdt (transform s) slot' = Some slot; \<not> cdl_cap_is_transferable (opt_cap slot' (transform s))\<rbrakk> \<Longrightarrow> (x, a, y) \<in> state_objs_to_policy s
 4. \<And>slot' slot. \<lbrakk>einvs s; (x, a, y) \<in> cdl_state_objs_to_policy (transform s); x = fst slot; a = DeleteDerived; y = fst slot'; cdl_cdt (transform s) slot' = Some slot\<rbrakk> \<Longrightarrow> (x, a, y) \<in> state_objs_to_policy s proof (prove)
goal (4 subgoals):
 1. \<And>ptr cap oref auth. \<lbrakk>(fst ptr, auth, oref) \<in> cdl_state_objs_to_policy (transform s); x = fst ptr; a = auth; y = oref; opt_cap ptr (transform s) = Some cap; oref \<in> cdl_obj_refs cap; auth \<in> cdl_cap_auth_conferred cap; \<not> is_thread_state_cap cap; \<not> is_real_cap cap; \<exists>ref aat. (oref, ref, aat, auth) \<in> state_vrefs s (fst ptr)\<rbrakk> \<Longrightarrow> (fst ptr, auth, oref) \<in> state_objs_to_policy s
 2. \<And>ptr cap oref auth. \<lbrakk>einvs s; (x, a, y) \<in> cdl_state_objs_to_policy (transform s); x = fst ptr; a = auth; y = oref; opt_cap ptr (transform s) = Some cap; oref \<in> cdl_obj_refs cap; auth \<in> cdl_cap_auth_conferred cap; \<not> is_thread_state_cap cap; is_real_cap cap\<rbrakk> \<Longrightarrow> (x, a, y) \<in> state_objs_to_policy s
 3. \<And>slot' slot. \<lbrakk>einvs s; (x, a, y) \<in> cdl_state_objs_to_policy (transform s); x = fst slot; a = Control; y = fst slot'; cdl_cdt (transform s) slot' = Some slot; \<not> cdl_cap_is_transferable (opt_cap slot' (transform s))\<rbrakk> \<Longrightarrow> (x, a, y) \<in> state_objs_to_policy s
 4. \<And>slot' slot. \<lbrakk>einvs s; (x, a, y) \<in> cdl_state_objs_to_policy (transform s); x = fst slot; a = DeleteDerived; y = fst slot'; cdl_cdt (transform s) slot' = Some slot\<rbrakk> \<Longrightarrow> (x, a, y) \<in> state_objs_to_policy s proof (prove)
goal (4 subgoals):
 1. \<And>b cap ref aat. \<lbrakk>(x, a, y) \<in> cdl_state_objs_to_policy (transform s); opt_cap (x, b) (transform s) = Some cap; y \<in> cdl_obj_refs cap; a \<in> cdl_cap_auth_conferred cap; \<not> is_thread_state_cap cap; \<not> is_real_cap cap; (y, ref, aat, a) \<in> state_vrefs s x\<rbrakk> \<Longrightarrow> (x, a, y) \<in> state_objs_to_policy s
 2. \<And>ptr cap oref auth. \<lbrakk>einvs s; (x, a, y) \<in> cdl_state_objs_to_policy (transform s); x = fst ptr; a = auth; y = oref; opt_cap ptr (transform s) = Some cap; oref \<in> cdl_obj_refs cap; auth \<in> cdl_cap_auth_conferred cap; \<not> is_thread_state_cap cap; is_real_cap cap\<rbrakk> \<Longrightarrow> (x, a, y) \<in> state_objs_to_policy s
 3. \<And>slot' slot. \<lbrakk>einvs s; (x, a, y) \<in> cdl_state_objs_to_policy (transform s); x = fst slot; a = Control; y = fst slot'; cdl_cdt (transform s) slot' = Some slot; \<not> cdl_cap_is_transferable (opt_cap slot' (transform s))\<rbrakk> \<Longrightarrow> (x, a, y) \<in> state_objs_to_policy s
 4. \<And>slot' slot. \<lbrakk>einvs s; (x, a, y) \<in> cdl_state_objs_to_policy (transform s); x = fst slot; a = DeleteDerived; y = fst slot'; cdl_cdt (transform s) slot' = Some slot\<rbrakk> \<Longrightarrow> (x, a, y) \<in> state_objs_to_policy s proof (prove)
goal (4 subgoals):
 1. \<And>b cap ref aat. \<lbrakk>(x, a, y) \<in> cdl_state_objs_to_policy (transform s); opt_cap (x, b) (transform s) = Some cap; y \<in> cdl_obj_refs cap; a \<in> cdl_cap_auth_conferred cap; \<not> is_thread_state_cap cap; \<not> is_real_cap cap; (y, ref, aat, a) \<in> state_vrefs s x\<rbrakk> \<Longrightarrow> (y, ?uu38 b cap ref aat, ?uv38 b cap ref aat, a) \<in> state_vrefs s x
 2. \<And>ptr cap oref auth. \<lbrakk>einvs s; (x, a, y) \<in> cdl_state_objs_to_policy (transform s); x = fst ptr; a = auth; y = oref; opt_cap ptr (transform s) = Some cap; oref \<in> cdl_obj_refs cap; auth \<in> cdl_cap_auth_conferred cap; \<not> is_thread_state_cap cap; is_real_cap cap\<rbrakk> \<Longrightarrow> (x, a, y) \<in> state_objs_to_policy s
 3. \<And>slot' slot. \<lbrakk>einvs s; (x, a, y) \<in> cdl_state_objs_to_policy (transform s); x = fst slot; a = Control; y = fst slot'; cdl_cdt (transform s) slot' = Some slot; \<not> cdl_cap_is_transferable (opt_cap slot' (transform s))\<rbrakk> \<Longrightarrow> (x, a, y) \<in> state_objs_to_policy s
 4. \<And>slot' slot. \<lbrakk>einvs s; (x, a, y) \<in> cdl_state_objs_to_policy (transform s); x = fst slot; a = DeleteDerived; y = fst slot'; cdl_cdt (transform s) slot' = Some slot\<rbrakk> \<Longrightarrow> (x, a, y) \<in> state_objs_to_policy s proof (prove)
goal (3 subgoals):
 1. \<And>ptr cap oref auth. \<lbrakk>einvs s; (x, a, y) \<in> cdl_state_objs_to_policy (transform s); x = fst ptr; a = auth; y = oref; opt_cap ptr (transform s) = Some cap; oref \<in> cdl_obj_refs cap; auth \<in> cdl_cap_auth_conferred cap; \<not> is_thread_state_cap cap; is_real_cap cap\<rbrakk> \<Longrightarrow> (x, a, y) \<in> state_objs_to_policy s
 2. \<And>slot' slot. \<lbrakk>einvs s; (x, a, y) \<in> cdl_state_objs_to_policy (transform s); x = fst slot; a = Control; y = fst slot'; cdl_cdt (transform s) slot' = Some slot; \<not> cdl_cap_is_transferable (opt_cap slot' (transform s))\<rbrakk> \<Longrightarrow> (x, a, y) \<in> state_objs_to_policy s
 3. \<And>slot' slot. \<lbrakk>einvs s; (x, a, y) \<in> cdl_state_objs_to_policy (transform s); x = fst slot; a = DeleteDerived; y = fst slot'; cdl_cdt (transform s) slot' = Some slot\<rbrakk> \<Longrightarrow> (x, a, y) \<in> state_objs_to_policy s proof (prove)
goal (4 subgoals):
 1. \<And>ptr cap oref auth. \<lbrakk>einvs s; (x, a, y) \<in> cdl_state_objs_to_policy (transform s); x = fst ptr; a = auth; y = oref; opt_cap ptr (transform s) = Some cap; oref \<in> cdl_obj_refs cap; auth \<in> cdl_cap_auth_conferred cap; \<not> is_thread_state_cap cap; is_real_cap cap; \<not> is_null_cap cap\<rbrakk> \<Longrightarrow> (x, a, y) \<in> state_objs_to_policy s
 2. \<And>ptr cap oref auth. \<lbrakk>einvs s; (x, a, y) \<in> cdl_state_objs_to_policy (transform s); x = fst ptr; a = auth; y = oref; opt_cap ptr (transform s) = Some cap; oref \<in> cdl_obj_refs cap; auth \<in> cdl_cap_auth_conferred cap; \<not> is_thread_state_cap cap; is_real_cap cap\<rbrakk> \<Longrightarrow> \<not> is_null_cap cap
 3. \<And>slot' slot. \<lbrakk>einvs s; (x, a, y) \<in> cdl_state_objs_to_policy (transform s); x = fst slot; a = Control; y = fst slot'; cdl_cdt (transform s) slot' = Some slot; \<not> cdl_cap_is_transferable (opt_cap slot' (transform s))\<rbrakk> \<Longrightarrow> (x, a, y) \<in> state_objs_to_policy s
 4. \<And>slot' slot. \<lbrakk>einvs s; (x, a, y) \<in> cdl_state_objs_to_policy (transform s); x = fst slot; a = DeleteDerived; y = fst slot'; cdl_cdt (transform s) slot' = Some slot\<rbrakk> \<Longrightarrow> (x, a, y) \<in> state_objs_to_policy s proof (prove)
goal (4 subgoals):
 1. \<And>ptr cap oref auth. \<lbrakk>einvs s; (x, a, y) \<in> cdl_state_objs_to_policy (transform s); x = fst ptr; a = auth; y = oref; opt_cap ptr (transform s) = Some cap; oref \<in> cdl_obj_refs cap; auth \<in> cdl_cap_auth_conferred cap; \<not> is_thread_state_cap cap; is_real_cap cap\<rbrakk> \<Longrightarrow> \<not> is_null_cap cap
 2. \<And>ptr cap oref auth. \<lbrakk>einvs s; (x, a, y) \<in> cdl_state_objs_to_policy (transform s); x = fst ptr; a = auth; y = oref; opt_cap ptr (transform s) = Some cap; oref \<in> cdl_obj_refs cap; auth \<in> cdl_cap_auth_conferred cap; \<not> is_thread_state_cap cap; is_real_cap cap; \<not> is_null_cap cap\<rbrakk> \<Longrightarrow> (x, a, y) \<in> state_objs_to_policy s
 3. \<And>slot' slot. \<lbrakk>einvs s; (x, a, y) \<in> cdl_state_objs_to_policy (transform s); x = fst slot; a = Control; y = fst slot'; cdl_cdt (transform s) slot' = Some slot; \<not> cdl_cap_is_transferable (opt_cap slot' (transform s))\<rbrakk> \<Longrightarrow> (x, a, y) \<in> state_objs_to_policy s
 4. \<And>slot' slot. \<lbrakk>einvs s; (x, a, y) \<in> cdl_state_objs_to_policy (transform s); x = fst slot; a = DeleteDerived; y = fst slot'; cdl_cdt (transform s) slot' = Some slot\<rbrakk> \<Longrightarrow> (x, a, y) \<in> state_objs_to_policy s proof (prove)
goal (3 subgoals):
 1. \<And>ptr cap oref auth. \<lbrakk>einvs s; (x, a, y) \<in> cdl_state_objs_to_policy (transform s); x = fst ptr; a = auth; y = oref; opt_cap ptr (transform s) = Some cap; oref \<in> cdl_obj_refs cap; auth \<in> cdl_cap_auth_conferred cap; \<not> is_thread_state_cap cap; is_real_cap cap; \<not> is_null_cap cap\<rbrakk> \<Longrightarrow> (x, a, y) \<in> state_objs_to_policy s
 2. \<And>slot' slot. \<lbrakk>einvs s; (x, a, y) \<in> cdl_state_objs_to_policy (transform s); x = fst slot; a = Control; y = fst slot'; cdl_cdt (transform s) slot' = Some slot; \<not> cdl_cap_is_transferable (opt_cap slot' (transform s))\<rbrakk> \<Longrightarrow> (x, a, y) \<in> state_objs_to_policy s
 3. \<And>slot' slot. \<lbrakk>einvs s; (x, a, y) \<in> cdl_state_objs_to_policy (transform s); x = fst slot; a = DeleteDerived; y = fst slot'; cdl_cdt (transform s) slot' = Some slot\<rbrakk> \<Longrightarrow> (x, a, y) \<in> state_objs_to_policy s proof (prove)
goal (4 subgoals):
 1. \<And>ptr cap oref auth. \<lbrakk>einvs s; (x, a, y) \<in> cdl_state_objs_to_policy (transform s); x = fst ptr; a = auth; y = oref; opt_cap ptr (transform s) = Some cap; oref \<in> cdl_obj_refs cap; auth \<in> cdl_cap_auth_conferred cap; \<not> is_thread_state_cap cap; is_real_cap cap; \<not> is_null_cap cap; is_bound_ntfn_cap cap\<rbrakk> \<Longrightarrow> (x, a, y) \<in> state_objs_to_policy s
 2. \<And>ptr cap oref auth. \<lbrakk>einvs s; (x, a, y) \<in> cdl_state_objs_to_policy (transform s); x = fst ptr; a = auth; y = oref; opt_cap ptr (transform s) = Some cap; oref \<in> cdl_obj_refs cap; auth \<in> cdl_cap_auth_conferred cap; \<not> is_thread_state_cap cap; is_real_cap cap; \<not> is_null_cap cap; \<not> is_bound_ntfn_cap cap\<rbrakk> \<Longrightarrow> (x, a, y) \<in> state_objs_to_policy s
 3. \<And>slot' slot. \<lbrakk>einvs s; (x, a, y) \<in> cdl_state_objs_to_policy (transform s); x = fst slot; a = Control; y = fst slot'; cdl_cdt (transform s) slot' = Some slot; \<not> cdl_cap_is_transferable (opt_cap slot' (transform s))\<rbrakk> \<Longrightarrow> (x, a, y) \<in> state_objs_to_policy s
 4. \<And>slot' slot. \<lbrakk>einvs s; (x, a, y) \<in> cdl_state_objs_to_policy (transform s); x = fst slot; a = DeleteDerived; y = fst slot'; cdl_cdt (transform s) slot' = Some slot\<rbrakk> \<Longrightarrow> (x, a, y) \<in> state_objs_to_policy s proof (prove)
goal (4 subgoals):
 1. \<And>ptr cap oref auth. \<lbrakk>invs s \<and> valid_list s \<and> valid_sched s; (fst ptr, auth, oref) \<in> cdl_state_objs_to_policy (transform s); x = fst ptr; a = auth; y = oref; opt_cap ptr (transform s) = Some cap; oref \<in> cdl_obj_refs cap; auth \<in> cdl_cap_auth_conferred cap; \<not> is_thread_state_cap cap; is_real_cap cap; \<not> is_null_cap cap; is_bound_ntfn_cap cap\<rbrakk> \<Longrightarrow> (fst ptr, auth, oref) \<in> state_objs_to_policy s
 2. \<And>ptr cap oref auth. \<lbrakk>einvs s; (x, a, y) \<in> cdl_state_objs_to_policy (transform s); x = fst ptr; a = auth; y = oref; opt_cap ptr (transform s) = Some cap; oref \<in> cdl_obj_refs cap; auth \<in> cdl_cap_auth_conferred cap; \<not> is_thread_state_cap cap; is_real_cap cap; \<not> is_null_cap cap; \<not> is_bound_ntfn_cap cap\<rbrakk> \<Longrightarrow> (x, a, y) \<in> state_objs_to_policy s
 3. \<And>slot' slot. \<lbrakk>einvs s; (x, a, y) \<in> cdl_state_objs_to_policy (transform s); x = fst slot; a = Control; y = fst slot'; cdl_cdt (transform s) slot' = Some slot; \<not> cdl_cap_is_transferable (opt_cap slot' (transform s))\<rbrakk> \<Longrightarrow> (x, a, y) \<in> state_objs_to_policy s
 4. \<And>slot' slot. \<lbrakk>einvs s; (x, a, y) \<in> cdl_state_objs_to_policy (transform s); x = fst slot; a = DeleteDerived; y = fst slot'; cdl_cdt (transform s) slot' = Some slot\<rbrakk> \<Longrightarrow> (x, a, y) \<in> state_objs_to_policy s proof (prove)
goal (5 subgoals):
 1. \<And>ptr cap oref auth. \<lbrakk>invs s \<and> valid_list s \<and> valid_sched s; (fst ptr, auth, oref) \<in> cdl_state_objs_to_policy (transform s); x = fst ptr; a = auth; y = oref; opt_cap ptr (transform s) = Some cap; oref \<in> cdl_obj_refs cap; auth \<in> cdl_cap_auth_conferred cap; \<not> is_thread_state_cap cap; is_real_cap cap; \<not> is_null_cap cap; is_bound_ntfn_cap cap\<rbrakk> \<Longrightarrow> thread_bound_ntfns s (fst ptr) = Some oref
 2. \<And>ptr cap oref auth. \<lbrakk>invs s \<and> valid_list s \<and> valid_sched s; (fst ptr, auth, oref) \<in> cdl_state_objs_to_policy (transform s); x = fst ptr; a = auth; y = oref; opt_cap ptr (transform s) = Some cap; oref \<in> cdl_obj_refs cap; auth \<in> cdl_cap_auth_conferred cap; \<not> is_thread_state_cap cap; is_real_cap cap; \<not> is_null_cap cap; is_bound_ntfn_cap cap\<rbrakk> \<Longrightarrow> auth \<in> {Receive, Reset}
 3. \<And>ptr cap oref auth. \<lbrakk>einvs s; (x, a, y) \<in> cdl_state_objs_to_policy (transform s); x = fst ptr; a = auth; y = oref; opt_cap ptr (transform s) = Some cap; oref \<in> cdl_obj_refs cap; auth \<in> cdl_cap_auth_conferred cap; \<not> is_thread_state_cap cap; is_real_cap cap; \<not> is_null_cap cap; \<not> is_bound_ntfn_cap cap\<rbrakk> \<Longrightarrow> (x, a, y) \<in> state_objs_to_policy s
 4. \<And>slot' slot. \<lbrakk>einvs s; (x, a, y) \<in> cdl_state_objs_to_policy (transform s); x = fst slot; a = Control; y = fst slot'; cdl_cdt (transform s) slot' = Some slot; \<not> cdl_cap_is_transferable (opt_cap slot' (transform s))\<rbrakk> \<Longrightarrow> (x, a, y) \<in> state_objs_to_policy s
 5. \<And>slot' slot. \<lbrakk>einvs s; (x, a, y) \<in> cdl_state_objs_to_policy (transform s); x = fst slot; a = DeleteDerived; y = fst slot'; cdl_cdt (transform s) slot' = Some slot\<rbrakk> \<Longrightarrow> (x, a, y) \<in> state_objs_to_policy s proof (prove)
goal (5 subgoals):
 1. \<And>ptr cap oref auth. \<lbrakk>invs s \<and> valid_list s \<and> valid_sched s; (fst ptr, auth, oref) \<in> cdl_state_objs_to_policy (transform s); x = fst ptr; a = auth; y = oref; opt_cap ptr (transform s) = Some cap; oref \<in> cdl_obj_refs cap; auth \<in> cdl_cap_auth_conferred cap; \<not> is_thread_state_cap cap; is_real_cap cap; \<not> is_null_cap cap; is_bound_ntfn_cap cap\<rbrakk> \<Longrightarrow> fst ptr \<noteq> idle_thread s
 2. \<And>ptr cap oref auth. \<lbrakk>invs s \<and> valid_list s \<and> valid_sched s; (fst ptr, auth, oref) \<in> cdl_state_objs_to_policy (transform s); x = fst ptr; a = auth; y = oref; opt_cap ptr (transform s) = Some cap; oref \<in> cdl_obj_refs cap; auth \<in> cdl_cap_auth_conferred cap; \<not> is_thread_state_cap cap; is_real_cap cap; \<not> is_null_cap cap; is_bound_ntfn_cap cap\<rbrakk> \<Longrightarrow> auth \<in> {Receive, Reset}
 3. \<And>ptr cap oref auth. \<lbrakk>einvs s; (x, a, y) \<in> cdl_state_objs_to_policy (transform s); x = fst ptr; a = auth; y = oref; opt_cap ptr (transform s) = Some cap; oref \<in> cdl_obj_refs cap; auth \<in> cdl_cap_auth_conferred cap; \<not> is_thread_state_cap cap; is_real_cap cap; \<not> is_null_cap cap; \<not> is_bound_ntfn_cap cap\<rbrakk> \<Longrightarrow> (x, a, y) \<in> state_objs_to_policy s
 4. \<And>slot' slot. \<lbrakk>einvs s; (x, a, y) \<in> cdl_state_objs_to_policy (transform s); x = fst slot; a = Control; y = fst slot'; cdl_cdt (transform s) slot' = Some slot; \<not> cdl_cap_is_transferable (opt_cap slot' (transform s))\<rbrakk> \<Longrightarrow> (x, a, y) \<in> state_objs_to_policy s
 5. \<And>slot' slot. \<lbrakk>einvs s; (x, a, y) \<in> cdl_state_objs_to_policy (transform s); x = fst slot; a = DeleteDerived; y = fst slot'; cdl_cdt (transform s) slot' = Some slot\<rbrakk> \<Longrightarrow> (x, a, y) \<in> state_objs_to_policy s proof (prove)
goal (5 subgoals):
 1. \<And>b cap. \<lbrakk>(idle_thread s, a, y) \<in> cdl_state_objs_to_policy \<lparr>cdl_arch = ARM11, cdl_objects = (\<lambda>ptr. Some cdl_object.Untyped) |` (- {idle_thread s}) ++ (\<lambda>ptr. map_option (transform_object (machine_state s) ptr ((ekheap s |` (- {idle_thread s})) ptr)) ((kheap s |` (- {idle_thread s})) ptr)), cdl_cdt = transform_cdt s, cdl_current_thread = transform_current_thread s, cdl_irq_node = interrupt_irq_node s, cdl_asid_table = transform_asid_table s, cdl_current_domain = cur_domain s\<rparr>; x = idle_thread s; (case ((\<lambda>ptr. Some cdl_object.Untyped) |` (- {idle_thread s}) ++ (\<lambda>ptr. map_option (transform_object (machine_state s) ptr ((ekheap s |` (- {idle_thread s})) ptr)) ((kheap s |` (- {idle_thread s})) ptr))) (idle_thread s) of None \<Rightarrow> \<lambda>x. None | Some x2 \<Rightarrow> object_slots x2) b = Some cap; y \<in> cdl_obj_refs cap; a \<in> cdl_cap_auth_conferred cap; \<not> is_thread_state_cap cap; is_real_cap cap; \<not> is_null_cap cap; is_bound_ntfn_cap cap; invs s; valid_list s; valid_sched s\<rbrakk> \<Longrightarrow> False
 2. \<And>ptr cap oref auth. \<lbrakk>invs s \<and> valid_list s \<and> valid_sched s; (fst ptr, auth, oref) \<in> cdl_state_objs_to_policy (transform s); x = fst ptr; a = auth; y = oref; opt_cap ptr (transform s) = Some cap; oref \<in> cdl_obj_refs cap; auth \<in> cdl_cap_auth_conferred cap; \<not> is_thread_state_cap cap; is_real_cap cap; \<not> is_null_cap cap; is_bound_ntfn_cap cap\<rbrakk> \<Longrightarrow> auth \<in> {Receive, Reset}
 3. \<And>ptr cap oref auth. \<lbrakk>einvs s; (x, a, y) \<in> cdl_state_objs_to_policy (transform s); x = fst ptr; a = auth; y = oref; opt_cap ptr (transform s) = Some cap; oref \<in> cdl_obj_refs cap; auth \<in> cdl_cap_auth_conferred cap; \<not> is_thread_state_cap cap; is_real_cap cap; \<not> is_null_cap cap; \<not> is_bound_ntfn_cap cap\<rbrakk> \<Longrightarrow> (x, a, y) \<in> state_objs_to_policy s
 4. \<And>slot' slot. \<lbrakk>einvs s; (x, a, y) \<in> cdl_state_objs_to_policy (transform s); x = fst slot; a = Control; y = fst slot'; cdl_cdt (transform s) slot' = Some slot; \<not> cdl_cap_is_transferable (opt_cap slot' (transform s))\<rbrakk> \<Longrightarrow> (x, a, y) \<in> state_objs_to_policy s
 5. \<And>slot' slot. \<lbrakk>einvs s; (x, a, y) \<in> cdl_state_objs_to_policy (transform s); x = fst slot; a = DeleteDerived; y = fst slot'; cdl_cdt (transform s) slot' = Some slot\<rbrakk> \<Longrightarrow> (x, a, y) \<in> state_objs_to_policy s proof (prove)
goal (4 subgoals):
 1. \<And>ptr cap oref auth. \<lbrakk>invs s \<and> valid_list s \<and> valid_sched s; (fst ptr, auth, oref) \<in> cdl_state_objs_to_policy (transform s); x = fst ptr; a = auth; y = oref; opt_cap ptr (transform s) = Some cap; oref \<in> cdl_obj_refs cap; auth \<in> cdl_cap_auth_conferred cap; \<not> is_thread_state_cap cap; is_real_cap cap; \<not> is_null_cap cap; is_bound_ntfn_cap cap\<rbrakk> \<Longrightarrow> auth \<in> {Receive, Reset}
 2. \<And>ptr cap oref auth. \<lbrakk>einvs s; (x, a, y) \<in> cdl_state_objs_to_policy (transform s); x = fst ptr; a = auth; y = oref; opt_cap ptr (transform s) = Some cap; oref \<in> cdl_obj_refs cap; auth \<in> cdl_cap_auth_conferred cap; \<not> is_thread_state_cap cap; is_real_cap cap; \<not> is_null_cap cap; \<not> is_bound_ntfn_cap cap\<rbrakk> \<Longrightarrow> (x, a, y) \<in> state_objs_to_policy s
 3. \<And>slot' slot. \<lbrakk>einvs s; (x, a, y) \<in> cdl_state_objs_to_policy (transform s); x = fst slot; a = Control; y = fst slot'; cdl_cdt (transform s) slot' = Some slot; \<not> cdl_cap_is_transferable (opt_cap slot' (transform s))\<rbrakk> \<Longrightarrow> (x, a, y) \<in> state_objs_to_policy s
 4. \<And>slot' slot. \<lbrakk>einvs s; (x, a, y) \<in> cdl_state_objs_to_policy (transform s); x = fst slot; a = DeleteDerived; y = fst slot'; cdl_cdt (transform s) slot' = Some slot\<rbrakk> \<Longrightarrow> (x, a, y) \<in> state_objs_to_policy s proof (prove)
goal (3 subgoals):
 1. \<And>ptr cap oref auth. \<lbrakk>einvs s; (x, a, y) \<in> cdl_state_objs_to_policy (transform s); x = fst ptr; a = auth; y = oref; opt_cap ptr (transform s) = Some cap; oref \<in> cdl_obj_refs cap; auth \<in> cdl_cap_auth_conferred cap; \<not> is_thread_state_cap cap; is_real_cap cap; \<not> is_null_cap cap; \<not> is_bound_ntfn_cap cap\<rbrakk> \<Longrightarrow> (x, a, y) \<in> state_objs_to_policy s
 2. \<And>slot' slot. \<lbrakk>einvs s; (x, a, y) \<in> cdl_state_objs_to_policy (transform s); x = fst slot; a = Control; y = fst slot'; cdl_cdt (transform s) slot' = Some slot; \<not> cdl_cap_is_transferable (opt_cap slot' (transform s))\<rbrakk> \<Longrightarrow> (x, a, y) \<in> state_objs_to_policy s
 3. \<And>slot' slot. \<lbrakk>einvs s; (x, a, y) \<in> cdl_state_objs_to_policy (transform s); x = fst slot; a = DeleteDerived; y = fst slot'; cdl_cdt (transform s) slot' = Some slot\<rbrakk> \<Longrightarrow> (x, a, y) \<in> state_objs_to_policy s proof (prove)
goal (3 subgoals):
 1. \<And>ptr cap oref auth. \<lbrakk>invs s \<and> valid_list s \<and> valid_sched s; (fst ptr, auth, oref) \<in> cdl_state_objs_to_policy (transform s); x = fst ptr; a = auth; y = oref; opt_cap ptr (transform s) = Some cap; oref \<in> cdl_obj_refs cap; auth \<in> cdl_cap_auth_conferred cap; \<not> is_thread_state_cap cap; is_real_cap cap; \<not> is_null_cap cap; \<not> is_bound_ntfn_cap cap; \<exists>cap'. cap = transform_cap cap' \<and> (\<exists>a b. ptr = transform_cslot_ptr (a, b) \<and> caps_of_state s (a, b) = Some cap')\<rbrakk> \<Longrightarrow> (fst ptr, auth, oref) \<in> state_objs_to_policy s
 2. \<And>slot' slot. \<lbrakk>einvs s; (x, a, y) \<in> cdl_state_objs_to_policy (transform s); x = fst slot; a = Control; y = fst slot'; cdl_cdt (transform s) slot' = Some slot; \<not> cdl_cap_is_transferable (opt_cap slot' (transform s))\<rbrakk> \<Longrightarrow> (x, a, y) \<in> state_objs_to_policy s
 3. \<And>slot' slot. \<lbrakk>einvs s; (x, a, y) \<in> cdl_state_objs_to_policy (transform s); x = fst slot; a = DeleteDerived; y = fst slot'; cdl_cdt (transform s) slot' = Some slot\<rbrakk> \<Longrightarrow> (x, a, y) \<in> state_objs_to_policy s proof (prove)
goal (4 subgoals):
 1. \<And>ptr cap oref auth. \<lbrakk>invs s \<and> valid_list s \<and> valid_sched s; (fst ptr, auth, oref) \<in> cdl_state_objs_to_policy (transform s); x = fst ptr; a = auth; y = oref; opt_cap ptr (transform s) = Some cap; oref \<in> cdl_obj_refs cap; auth \<in> cdl_cap_auth_conferred cap; \<not> is_thread_state_cap cap; is_real_cap cap; \<not> is_null_cap cap; \<not> is_bound_ntfn_cap cap; \<exists>cap'. cap = transform_cap cap' \<and> (\<exists>a b. ptr = transform_cslot_ptr (a, b) \<and> caps_of_state s (a, b) = Some cap'); local.is_untyped_cap cap\<rbrakk> \<Longrightarrow> (fst ptr, auth, oref) \<in> state_objs_to_policy s
 2. \<And>ptr cap oref auth. \<lbrakk>invs s \<and> valid_list s \<and> valid_sched s; (fst ptr, auth, oref) \<in> cdl_state_objs_to_policy (transform s); x = fst ptr; a = auth; y = oref; opt_cap ptr (transform s) = Some cap; oref \<in> cdl_obj_refs cap; auth \<in> cdl_cap_auth_conferred cap; \<not> is_thread_state_cap cap; is_real_cap cap; \<not> is_null_cap cap; \<not> is_bound_ntfn_cap cap; \<exists>cap'. cap = transform_cap cap' \<and> (\<exists>a b. ptr = transform_cslot_ptr (a, b) \<and> caps_of_state s (a, b) = Some cap'); \<not> local.is_untyped_cap cap\<rbrakk> \<Longrightarrow> (fst ptr, auth, oref) \<in> state_objs_to_policy s
 3. \<And>slot' slot. \<lbrakk>einvs s; (x, a, y) \<in> cdl_state_objs_to_policy (transform s); x = fst slot; a = Control; y = fst slot'; cdl_cdt (transform s) slot' = Some slot; \<not> cdl_cap_is_transferable (opt_cap slot' (transform s))\<rbrakk> \<Longrightarrow> (x, a, y) \<in> state_objs_to_policy s
 4. \<And>slot' slot. \<lbrakk>einvs s; (x, a, y) \<in> cdl_state_objs_to_policy (transform s); x = fst slot; a = DeleteDerived; y = fst slot'; cdl_cdt (transform s) slot' = Some slot\<rbrakk> \<Longrightarrow> (x, a, y) \<in> state_objs_to_policy s proof (prove)
goal (5 subgoals):
 1. \<And>ptr cap oref auth. \<lbrakk>invs s \<and> valid_list s \<and> valid_sched s; (fst ptr, auth, oref) \<in> cdl_state_objs_to_policy (transform s); x = fst ptr; a = auth; y = oref; opt_cap ptr (transform s) = Some cap; oref \<in> cdl_obj_refs cap; auth \<in> cdl_cap_auth_conferred cap; \<not> is_thread_state_cap cap; is_real_cap cap; \<not> is_null_cap cap; \<not> is_bound_ntfn_cap cap; \<exists>cap'. cap = transform_cap cap' \<and> (\<exists>a b. ptr = transform_cslot_ptr (a, b) \<and> caps_of_state s (a, b) = Some cap'); local.is_untyped_cap cap; a = Control\<rbrakk> \<Longrightarrow> (fst ptr, auth, oref) \<in> state_objs_to_policy s
 2. \<And>ptr cap oref auth. \<lbrakk>invs s \<and> valid_list s \<and> valid_sched s; (fst ptr, auth, oref) \<in> cdl_state_objs_to_policy (transform s); x = fst ptr; a = auth; y = oref; opt_cap ptr (transform s) = Some cap; oref \<in> cdl_obj_refs cap; auth \<in> cdl_cap_auth_conferred cap; \<not> is_thread_state_cap cap; is_real_cap cap; \<not> is_null_cap cap; \<not> is_bound_ntfn_cap cap; \<exists>cap'. cap = transform_cap cap' \<and> (\<exists>a b. ptr = transform_cslot_ptr (a, b) \<and> caps_of_state s (a, b) = Some cap'); local.is_untyped_cap cap\<rbrakk> \<Longrightarrow> a = Control
 3. \<And>ptr cap oref auth. \<lbrakk>invs s \<and> valid_list s \<and> valid_sched s; (fst ptr, auth, oref) \<in> cdl_state_objs_to_policy (transform s); x = fst ptr; a = auth; y = oref; opt_cap ptr (transform s) = Some cap; oref \<in> cdl_obj_refs cap; auth \<in> cdl_cap_auth_conferred cap; \<not> is_thread_state_cap cap; is_real_cap cap; \<not> is_null_cap cap; \<not> is_bound_ntfn_cap cap; \<exists>cap'. cap = transform_cap cap' \<and> (\<exists>a b. ptr = transform_cslot_ptr (a, b) \<and> caps_of_state s (a, b) = Some cap'); \<not> local.is_untyped_cap cap\<rbrakk> \<Longrightarrow> (fst ptr, auth, oref) \<in> state_objs_to_policy s
 4. \<And>slot' slot. \<lbrakk>einvs s; (x, a, y) \<in> cdl_state_objs_to_policy (transform s); x = fst slot; a = Control; y = fst slot'; cdl_cdt (transform s) slot' = Some slot; \<not> cdl_cap_is_transferable (opt_cap slot' (transform s))\<rbrakk> \<Longrightarrow> (x, a, y) \<in> state_objs_to_policy s
 5. \<And>slot' slot. \<lbrakk>einvs s; (x, a, y) \<in> cdl_state_objs_to_policy (transform s); x = fst slot; a = DeleteDerived; y = fst slot'; cdl_cdt (transform s) slot' = Some slot\<rbrakk> \<Longrightarrow> (x, a, y) \<in> state_objs_to_policy s proof (prove)
goal (5 subgoals):
 1. \<And>aa b cap' aaa ba. \<lbrakk>(fst (transform_cslot_ptr (aaa, ba)), Control, y) \<in> cdl_state_objs_to_policy (transform s); x = fst (transform_cslot_ptr (aaa, ba)); opt_cap (transform_cslot_ptr (aaa, ba)) (transform s) = Some (transform_cap cap'); y \<in> cdl_obj_refs (transform_cap cap'); Control \<in> cdl_cap_auth_conferred (transform_cap cap'); \<not> is_thread_state_cap (transform_cap cap'); is_real_cap (transform_cap cap'); \<not> is_null_cap (transform_cap cap'); local.is_untyped_cap (transform_cap cap'); a = Control; invs s; valid_list s; valid_sched s; (aa, b) = transform_cslot_ptr (aaa, ba); caps_of_state s (aaa, ba) = Some cap'\<rbrakk> \<Longrightarrow> (fst (transform_cslot_ptr (aaa, ba)), Control, y) \<in> state_objs_to_policy s
 2. \<And>ptr cap oref auth. \<lbrakk>invs s \<and> valid_list s \<and> valid_sched s; (fst ptr, auth, oref) \<in> cdl_state_objs_to_policy (transform s); x = fst ptr; a = auth; y = oref; opt_cap ptr (transform s) = Some cap; oref \<in> cdl_obj_refs cap; auth \<in> cdl_cap_auth_conferred cap; \<not> is_thread_state_cap cap; is_real_cap cap; \<not> is_null_cap cap; \<not> is_bound_ntfn_cap cap; \<exists>cap'. cap = transform_cap cap' \<and> (\<exists>a b. ptr = transform_cslot_ptr (a, b) \<and> caps_of_state s (a, b) = Some cap'); local.is_untyped_cap cap\<rbrakk> \<Longrightarrow> a = Control
 3. \<And>ptr cap oref auth. \<lbrakk>invs s \<and> valid_list s \<and> valid_sched s; (fst ptr, auth, oref) \<in> cdl_state_objs_to_policy (transform s); x = fst ptr; a = auth; y = oref; opt_cap ptr (transform s) = Some cap; oref \<in> cdl_obj_refs cap; auth \<in> cdl_cap_auth_conferred cap; \<not> is_thread_state_cap cap; is_real_cap cap; \<not> is_null_cap cap; \<not> is_bound_ntfn_cap cap; \<exists>cap'. cap = transform_cap cap' \<and> (\<exists>a b. ptr = transform_cslot_ptr (a, b) \<and> caps_of_state s (a, b) = Some cap'); \<not> local.is_untyped_cap cap\<rbrakk> \<Longrightarrow> (fst ptr, auth, oref) \<in> state_objs_to_policy s
 4. \<And>slot' slot. \<lbrakk>einvs s; (x, a, y) \<in> cdl_state_objs_to_policy (transform s); x = fst slot; a = Control; y = fst slot'; cdl_cdt (transform s) slot' = Some slot; \<not> cdl_cap_is_transferable (opt_cap slot' (transform s))\<rbrakk> \<Longrightarrow> (x, a, y) \<in> state_objs_to_policy s
 5. \<And>slot' slot. \<lbrakk>einvs s; (x, a, y) \<in> cdl_state_objs_to_policy (transform s); x = fst slot; a = DeleteDerived; y = fst slot'; cdl_cdt (transform s) slot' = Some slot\<rbrakk> \<Longrightarrow> (x, a, y) \<in> state_objs_to_policy s proof (prove)
goal (5 subgoals):
 1. \<And>aa b cap' aaa ba. \<lbrakk>(fst (transform_cslot_ptr (aaa, ba)), Control, y) \<in> cdl_state_objs_to_policy (transform s); x = fst (transform_cslot_ptr (aaa, ba)); opt_cap (transform_cslot_ptr (aaa, ba)) (transform s) = Some (transform_cap cap'); y \<in> cdl_obj_refs (transform_cap cap'); Control \<in> cdl_cap_auth_conferred (transform_cap cap'); \<not> is_thread_state_cap (transform_cap cap'); is_real_cap (transform_cap cap'); \<not> is_null_cap (transform_cap cap'); local.is_untyped_cap (transform_cap cap'); a = Control; invs s; valid_list s; valid_sched s; (aa, b) = transform_cslot_ptr (aaa, ba); caps_of_state s (aaa, ba) = Some cap'\<rbrakk> \<Longrightarrow> (fst (aaa, ba), Control, y) \<in> state_objs_to_policy s
 2. \<And>ptr cap oref auth. \<lbrakk>invs s \<and> valid_list s \<and> valid_sched s; (fst ptr, auth, oref) \<in> cdl_state_objs_to_policy (transform s); x = fst ptr; a = auth; y = oref; opt_cap ptr (transform s) = Some cap; oref \<in> cdl_obj_refs cap; auth \<in> cdl_cap_auth_conferred cap; \<not> is_thread_state_cap cap; is_real_cap cap; \<not> is_null_cap cap; \<not> is_bound_ntfn_cap cap; \<exists>cap'. cap = transform_cap cap' \<and> (\<exists>a b. ptr = transform_cslot_ptr (a, b) \<and> caps_of_state s (a, b) = Some cap'); local.is_untyped_cap cap\<rbrakk> \<Longrightarrow> a = Control
 3. \<And>ptr cap oref auth. \<lbrakk>invs s \<and> valid_list s \<and> valid_sched s; (fst ptr, auth, oref) \<in> cdl_state_objs_to_policy (transform s); x = fst ptr; a = auth; y = oref; opt_cap ptr (transform s) = Some cap; oref \<in> cdl_obj_refs cap; auth \<in> cdl_cap_auth_conferred cap; \<not> is_thread_state_cap cap; is_real_cap cap; \<not> is_null_cap cap; \<not> is_bound_ntfn_cap cap; \<exists>cap'. cap = transform_cap cap' \<and> (\<exists>a b. ptr = transform_cslot_ptr (a, b) \<and> caps_of_state s (a, b) = Some cap'); \<not> local.is_untyped_cap cap\<rbrakk> \<Longrightarrow> (fst ptr, auth, oref) \<in> state_objs_to_policy s
 4. \<And>slot' slot. \<lbrakk>einvs s; (x, a, y) \<in> cdl_state_objs_to_policy (transform s); x = fst slot; a = Control; y = fst slot'; cdl_cdt (transform s) slot' = Some slot; \<not> cdl_cap_is_transferable (opt_cap slot' (transform s))\<rbrakk> \<Longrightarrow> (x, a, y) \<in> state_objs_to_policy s
 5. \<And>slot' slot. \<lbrakk>einvs s; (x, a, y) \<in> cdl_state_objs_to_policy (transform s); x = fst slot; a = DeleteDerived; y = fst slot'; cdl_cdt (transform s) slot' = Some slot\<rbrakk> \<Longrightarrow> (x, a, y) \<in> state_objs_to_policy s proof (prove)
goal (6 subgoals):
 1. \<And>aa b cap' aaa ba. \<lbrakk>(fst (transform_cslot_ptr (aaa, ba)), Control, y) \<in> cdl_state_objs_to_policy (transform s); x = fst (transform_cslot_ptr (aaa, ba)); opt_cap (transform_cslot_ptr (aaa, ba)) (transform s) = Some (transform_cap cap'); y \<in> cdl_obj_refs (transform_cap cap'); Control \<in> cdl_cap_auth_conferred (transform_cap cap'); \<not> is_thread_state_cap (transform_cap cap'); is_real_cap (transform_cap cap'); \<not> is_null_cap (transform_cap cap'); local.is_untyped_cap (transform_cap cap'); a = Control; invs s; valid_list s; valid_sched s; (aa, b) = transform_cslot_ptr (aaa, ba); caps_of_state s (aaa, ba) = Some cap'\<rbrakk> \<Longrightarrow> caps_of_state s (aaa, ba) = Some cap'
 2. \<And>aa b cap' aaa ba. \<lbrakk>(fst (transform_cslot_ptr (aaa, ba)), Control, y) \<in> cdl_state_objs_to_policy (transform s); x = fst (transform_cslot_ptr (aaa, ba)); opt_cap (transform_cslot_ptr (aaa, ba)) (transform s) = Some (transform_cap cap'); y \<in> cdl_obj_refs (transform_cap cap'); Control \<in> cdl_cap_auth_conferred (transform_cap cap'); \<not> is_thread_state_cap (transform_cap cap'); is_real_cap (transform_cap cap'); \<not> is_null_cap (transform_cap cap'); local.is_untyped_cap (transform_cap cap'); a = Control; invs s; valid_list s; valid_sched s; (aa, b) = transform_cslot_ptr (aaa, ba); caps_of_state s (aaa, ba) = Some cap'\<rbrakk> \<Longrightarrow> y \<in> untyped_range cap'
 3. \<And>ptr cap oref auth. \<lbrakk>invs s \<and> valid_list s \<and> valid_sched s; (fst ptr, auth, oref) \<in> cdl_state_objs_to_policy (transform s); x = fst ptr; a = auth; y = oref; opt_cap ptr (transform s) = Some cap; oref \<in> cdl_obj_refs cap; auth \<in> cdl_cap_auth_conferred cap; \<not> is_thread_state_cap cap; is_real_cap cap; \<not> is_null_cap cap; \<not> is_bound_ntfn_cap cap; \<exists>cap'. cap = transform_cap cap' \<and> (\<exists>a b. ptr = transform_cslot_ptr (a, b) \<and> caps_of_state s (a, b) = Some cap'); local.is_untyped_cap cap\<rbrakk> \<Longrightarrow> a = Control
 4. \<And>ptr cap oref auth. \<lbrakk>invs s \<and> valid_list s \<and> valid_sched s; (fst ptr, auth, oref) \<in> cdl_state_objs_to_policy (transform s); x = fst ptr; a = auth; y = oref; opt_cap ptr (transform s) = Some cap; oref \<in> cdl_obj_refs cap; auth \<in> cdl_cap_auth_conferred cap; \<not> is_thread_state_cap cap; is_real_cap cap; \<not> is_null_cap cap; \<not> is_bound_ntfn_cap cap; \<exists>cap'. cap = transform_cap cap' \<and> (\<exists>a b. ptr = transform_cslot_ptr (a, b) \<and> caps_of_state s (a, b) = Some cap'); \<not> local.is_untyped_cap cap\<rbrakk> \<Longrightarrow> (fst ptr, auth, oref) \<in> state_objs_to_policy s
 5. \<And>slot' slot. \<lbrakk>einvs s; (x, a, y) \<in> cdl_state_objs_to_policy (transform s); x = fst slot; a = Control; y = fst slot'; cdl_cdt (transform s) slot' = Some slot; \<not> cdl_cap_is_transferable (opt_cap slot' (transform s))\<rbrakk> \<Longrightarrow> (x, a, y) \<in> state_objs_to_policy s
 6. \<And>slot' slot. \<lbrakk>einvs s; (x, a, y) \<in> cdl_state_objs_to_policy (transform s); x = fst slot; a = DeleteDerived; y = fst slot'; cdl_cdt (transform s) slot' = Some slot\<rbrakk> \<Longrightarrow> (x, a, y) \<in> state_objs_to_policy s proof (prove)
goal (5 subgoals):
 1. \<And>aa b cap' aaa ba. \<lbrakk>(fst (transform_cslot_ptr (aaa, ba)), Control, y) \<in> cdl_state_objs_to_policy (transform s); x = fst (transform_cslot_ptr (aaa, ba)); opt_cap (transform_cslot_ptr (aaa, ba)) (transform s) = Some (transform_cap cap'); y \<in> cdl_obj_refs (transform_cap cap'); Control \<in> cdl_cap_auth_conferred (transform_cap cap'); \<not> is_thread_state_cap (transform_cap cap'); is_real_cap (transform_cap cap'); \<not> is_null_cap (transform_cap cap'); local.is_untyped_cap (transform_cap cap'); a = Control; invs s; valid_list s; valid_sched s; (aa, b) = transform_cslot_ptr (aaa, ba); caps_of_state s (aaa, ba) = Some cap'\<rbrakk> \<Longrightarrow> y \<in> untyped_range cap'
 2. \<And>ptr cap oref auth. \<lbrakk>invs s \<and> valid_list s \<and> valid_sched s; (fst ptr, auth, oref) \<in> cdl_state_objs_to_policy (transform s); x = fst ptr; a = auth; y = oref; opt_cap ptr (transform s) = Some cap; oref \<in> cdl_obj_refs cap; auth \<in> cdl_cap_auth_conferred cap; \<not> is_thread_state_cap cap; is_real_cap cap; \<not> is_null_cap cap; \<not> is_bound_ntfn_cap cap; \<exists>cap'. cap = transform_cap cap' \<and> (\<exists>a b. ptr = transform_cslot_ptr (a, b) \<and> caps_of_state s (a, b) = Some cap'); local.is_untyped_cap cap\<rbrakk> \<Longrightarrow> a = Control
 3. \<And>ptr cap oref auth. \<lbrakk>invs s \<and> valid_list s \<and> valid_sched s; (fst ptr, auth, oref) \<in> cdl_state_objs_to_policy (transform s); x = fst ptr; a = auth; y = oref; opt_cap ptr (transform s) = Some cap; oref \<in> cdl_obj_refs cap; auth \<in> cdl_cap_auth_conferred cap; \<not> is_thread_state_cap cap; is_real_cap cap; \<not> is_null_cap cap; \<not> is_bound_ntfn_cap cap; \<exists>cap'. cap = transform_cap cap' \<and> (\<exists>a b. ptr = transform_cslot_ptr (a, b) \<and> caps_of_state s (a, b) = Some cap'); \<not> local.is_untyped_cap cap\<rbrakk> \<Longrightarrow> (fst ptr, auth, oref) \<in> state_objs_to_policy s
 4. \<And>slot' slot. \<lbrakk>einvs s; (x, a, y) \<in> cdl_state_objs_to_policy (transform s); x = fst slot; a = Control; y = fst slot'; cdl_cdt (transform s) slot' = Some slot; \<not> cdl_cap_is_transferable (opt_cap slot' (transform s))\<rbrakk> \<Longrightarrow> (x, a, y) \<in> state_objs_to_policy s
 5. \<And>slot' slot. \<lbrakk>einvs s; (x, a, y) \<in> cdl_state_objs_to_policy (transform s); x = fst slot; a = DeleteDerived; y = fst slot'; cdl_cdt (transform s) slot' = Some slot\<rbrakk> \<Longrightarrow> (x, a, y) \<in> state_objs_to_policy s proof (prove)
goal (6 subgoals):
 1. \<And>aa b cap' aaa ba. \<lbrakk>Control \<in> cdl_cap_auth_conferred (transform_cap cap'); \<not> is_thread_state_cap (transform_cap cap'); is_real_cap (transform_cap cap'); \<not> is_null_cap (transform_cap cap'); local.is_untyped_cap (transform_cap cap'); a = Control; invs s; valid_list s; valid_sched s; (aa, b) = transform_cslot_ptr (aaa, ba); caps_of_state s (aaa, ba) = Some cap'; (fst (transform_cslot_ptr (aaa, ba)), Control, y) \<in> cdl_state_objs_to_policy (transform s); x = fst (transform_cslot_ptr (aaa, ba)); opt_cap (transform_cslot_ptr (aaa, ba)) (transform s) = Some (transform_cap cap')\<rbrakk> \<Longrightarrow> \<exists>x sz i dev. cap' = cap.UntypedCap dev x sz i
 2. \<And>aa b cap' aaa ba. \<lbrakk>(fst (transform_cslot_ptr (aaa, ba)), Control, y) \<in> cdl_state_objs_to_policy (transform s); x = fst (transform_cslot_ptr (aaa, ba)); opt_cap (transform_cslot_ptr (aaa, ba)) (transform s) = Some (transform_cap cap'); y \<in> untyped_range cap'; Control \<in> cdl_cap_auth_conferred (transform_cap cap'); \<not> is_thread_state_cap (transform_cap cap'); is_real_cap (transform_cap cap'); \<not> is_null_cap (transform_cap cap'); local.is_untyped_cap (transform_cap cap'); a = Control; invs s; valid_list s; valid_sched s; (aa, b) = transform_cslot_ptr (aaa, ba); caps_of_state s (aaa, ba) = Some cap'\<rbrakk> \<Longrightarrow> y \<in> untyped_range cap'
 3. \<And>ptr cap oref auth. \<lbrakk>invs s \<and> valid_list s \<and> valid_sched s; (fst ptr, auth, oref) \<in> cdl_state_objs_to_policy (transform s); x = fst ptr; a = auth; y = oref; opt_cap ptr (transform s) = Some cap; oref \<in> cdl_obj_refs cap; auth \<in> cdl_cap_auth_conferred cap; \<not> is_thread_state_cap cap; is_real_cap cap; \<not> is_null_cap cap; \<not> is_bound_ntfn_cap cap; \<exists>cap'. cap = transform_cap cap' \<and> (\<exists>a b. ptr = transform_cslot_ptr (a, b) \<and> caps_of_state s (a, b) = Some cap'); local.is_untyped_cap cap\<rbrakk> \<Longrightarrow> a = Control
 4. \<And>ptr cap oref auth. \<lbrakk>invs s \<and> valid_list s \<and> valid_sched s; (fst ptr, auth, oref) \<in> cdl_state_objs_to_policy (transform s); x = fst ptr; a = auth; y = oref; opt_cap ptr (transform s) = Some cap; oref \<in> cdl_obj_refs cap; auth \<in> cdl_cap_auth_conferred cap; \<not> is_thread_state_cap cap; is_real_cap cap; \<not> is_null_cap cap; \<not> is_bound_ntfn_cap cap; \<exists>cap'. cap = transform_cap cap' \<and> (\<exists>a b. ptr = transform_cslot_ptr (a, b) \<and> caps_of_state s (a, b) = Some cap'); \<not> local.is_untyped_cap cap\<rbrakk> \<Longrightarrow> (fst ptr, auth, oref) \<in> state_objs_to_policy s
 5. \<And>slot' slot. \<lbrakk>einvs s; (x, a, y) \<in> cdl_state_objs_to_policy (transform s); x = fst slot; a = Control; y = fst slot'; cdl_cdt (transform s) slot' = Some slot; \<not> cdl_cap_is_transferable (opt_cap slot' (transform s))\<rbrakk> \<Longrightarrow> (x, a, y) \<in> state_objs_to_policy s
 6. \<And>slot' slot. \<lbrakk>einvs s; (x, a, y) \<in> cdl_state_objs_to_policy (transform s); x = fst slot; a = DeleteDerived; y = fst slot'; cdl_cdt (transform s) slot' = Some slot\<rbrakk> \<Longrightarrow> (x, a, y) \<in> state_objs_to_policy s proof (prove)
goal (5 subgoals):
 1. \<And>aa b cap' aaa ba. \<lbrakk>(fst (transform_cslot_ptr (aaa, ba)), Control, y) \<in> cdl_state_objs_to_policy (transform s); x = fst (transform_cslot_ptr (aaa, ba)); opt_cap (transform_cslot_ptr (aaa, ba)) (transform s) = Some (transform_cap cap'); y \<in> untyped_range cap'; Control \<in> cdl_cap_auth_conferred (transform_cap cap'); \<not> is_thread_state_cap (transform_cap cap'); is_real_cap (transform_cap cap'); \<not> is_null_cap (transform_cap cap'); local.is_untyped_cap (transform_cap cap'); a = Control; invs s; valid_list s; valid_sched s; (aa, b) = transform_cslot_ptr (aaa, ba); caps_of_state s (aaa, ba) = Some cap'\<rbrakk> \<Longrightarrow> y \<in> untyped_range cap'
 2. \<And>ptr cap oref auth. \<lbrakk>invs s \<and> valid_list s \<and> valid_sched s; (fst ptr, auth, oref) \<in> cdl_state_objs_to_policy (transform s); x = fst ptr; a = auth; y = oref; opt_cap ptr (transform s) = Some cap; oref \<in> cdl_obj_refs cap; auth \<in> cdl_cap_auth_conferred cap; \<not> is_thread_state_cap cap; is_real_cap cap; \<not> is_null_cap cap; \<not> is_bound_ntfn_cap cap; \<exists>cap'. cap = transform_cap cap' \<and> (\<exists>a b. ptr = transform_cslot_ptr (a, b) \<and> caps_of_state s (a, b) = Some cap'); local.is_untyped_cap cap\<rbrakk> \<Longrightarrow> a = Control
 3. \<And>ptr cap oref auth. \<lbrakk>invs s \<and> valid_list s \<and> valid_sched s; (fst ptr, auth, oref) \<in> cdl_state_objs_to_policy (transform s); x = fst ptr; a = auth; y = oref; opt_cap ptr (transform s) = Some cap; oref \<in> cdl_obj_refs cap; auth \<in> cdl_cap_auth_conferred cap; \<not> is_thread_state_cap cap; is_real_cap cap; \<not> is_null_cap cap; \<not> is_bound_ntfn_cap cap; \<exists>cap'. cap = transform_cap cap' \<and> (\<exists>a b. ptr = transform_cslot_ptr (a, b) \<and> caps_of_state s (a, b) = Some cap'); \<not> local.is_untyped_cap cap\<rbrakk> \<Longrightarrow> (fst ptr, auth, oref) \<in> state_objs_to_policy s
 4. \<And>slot' slot. \<lbrakk>einvs s; (x, a, y) \<in> cdl_state_objs_to_policy (transform s); x = fst slot; a = Control; y = fst slot'; cdl_cdt (transform s) slot' = Some slot; \<not> cdl_cap_is_transferable (opt_cap slot' (transform s))\<rbrakk> \<Longrightarrow> (x, a, y) \<in> state_objs_to_policy s
 5. \<And>slot' slot. \<lbrakk>einvs s; (x, a, y) \<in> cdl_state_objs_to_policy (transform s); x = fst slot; a = DeleteDerived; y = fst slot'; cdl_cdt (transform s) slot' = Some slot\<rbrakk> \<Longrightarrow> (x, a, y) \<in> state_objs_to_policy s proof (prove)
goal (4 subgoals):
 1. \<And>ptr cap oref auth. \<lbrakk>invs s \<and> valid_list s \<and> valid_sched s; (fst ptr, auth, oref) \<in> cdl_state_objs_to_policy (transform s); x = fst ptr; a = auth; y = oref; opt_cap ptr (transform s) = Some cap; oref \<in> cdl_obj_refs cap; auth \<in> cdl_cap_auth_conferred cap; \<not> is_thread_state_cap cap; is_real_cap cap; \<not> is_null_cap cap; \<not> is_bound_ntfn_cap cap; \<exists>cap'. cap = transform_cap cap' \<and> (\<exists>a b. ptr = transform_cslot_ptr (a, b) \<and> caps_of_state s (a, b) = Some cap'); local.is_untyped_cap cap\<rbrakk> \<Longrightarrow> a = Control
 2. \<And>ptr cap oref auth. \<lbrakk>invs s \<and> valid_list s \<and> valid_sched s; (fst ptr, auth, oref) \<in> cdl_state_objs_to_policy (transform s); x = fst ptr; a = auth; y = oref; opt_cap ptr (transform s) = Some cap; oref \<in> cdl_obj_refs cap; auth \<in> cdl_cap_auth_conferred cap; \<not> is_thread_state_cap cap; is_real_cap cap; \<not> is_null_cap cap; \<not> is_bound_ntfn_cap cap; \<exists>cap'. cap = transform_cap cap' \<and> (\<exists>a b. ptr = transform_cslot_ptr (a, b) \<and> caps_of_state s (a, b) = Some cap'); \<not> local.is_untyped_cap cap\<rbrakk> \<Longrightarrow> (fst ptr, auth, oref) \<in> state_objs_to_policy s
 3. \<And>slot' slot. \<lbrakk>einvs s; (x, a, y) \<in> cdl_state_objs_to_policy (transform s); x = fst slot; a = Control; y = fst slot'; cdl_cdt (transform s) slot' = Some slot; \<not> cdl_cap_is_transferable (opt_cap slot' (transform s))\<rbrakk> \<Longrightarrow> (x, a, y) \<in> state_objs_to_policy s
 4. \<And>slot' slot. \<lbrakk>einvs s; (x, a, y) \<in> cdl_state_objs_to_policy (transform s); x = fst slot; a = DeleteDerived; y = fst slot'; cdl_cdt (transform s) slot' = Some slot\<rbrakk> \<Longrightarrow> (x, a, y) \<in> state_objs_to_policy s proof (prove)
goal (3 subgoals):
 1. \<And>ptr cap oref auth. \<lbrakk>invs s \<and> valid_list s \<and> valid_sched s; (fst ptr, auth, oref) \<in> cdl_state_objs_to_policy (transform s); x = fst ptr; a = auth; y = oref; opt_cap ptr (transform s) = Some cap; oref \<in> cdl_obj_refs cap; auth \<in> cdl_cap_auth_conferred cap; \<not> is_thread_state_cap cap; is_real_cap cap; \<not> is_null_cap cap; \<not> is_bound_ntfn_cap cap; \<exists>cap'. cap = transform_cap cap' \<and> (\<exists>a b. ptr = transform_cslot_ptr (a, b) \<and> caps_of_state s (a, b) = Some cap'); \<not> local.is_untyped_cap cap\<rbrakk> \<Longrightarrow> (fst ptr, auth, oref) \<in> state_objs_to_policy s
 2. \<And>slot' slot. \<lbrakk>einvs s; (x, a, y) \<in> cdl_state_objs_to_policy (transform s); x = fst slot; a = Control; y = fst slot'; cdl_cdt (transform s) slot' = Some slot; \<not> cdl_cap_is_transferable (opt_cap slot' (transform s))\<rbrakk> \<Longrightarrow> (x, a, y) \<in> state_objs_to_policy s
 3. \<And>slot' slot. \<lbrakk>einvs s; (x, a, y) \<in> cdl_state_objs_to_policy (transform s); x = fst slot; a = DeleteDerived; y = fst slot'; cdl_cdt (transform s) slot' = Some slot\<rbrakk> \<Longrightarrow> (x, a, y) \<in> state_objs_to_policy s proof (prove)
goal (3 subgoals):
 1. \<And>aa b cap' aaa ba. \<lbrakk>(fst (transform_cslot_ptr (aaa, ba)), a, y) \<in> cdl_state_objs_to_policy (transform s); x = fst (transform_cslot_ptr (aaa, ba)); opt_cap (transform_cslot_ptr (aaa, ba)) (transform s) = Some (transform_cap cap'); y \<in> cdl_obj_refs (transform_cap cap'); a \<in> cdl_cap_auth_conferred (transform_cap cap'); \<not> is_thread_state_cap (transform_cap cap'); is_real_cap (transform_cap cap'); \<not> is_null_cap (transform_cap cap'); \<not> local.is_untyped_cap (transform_cap cap'); invs s; valid_list s; valid_sched s; (aa, b) = transform_cslot_ptr (aaa, ba); caps_of_state s (aaa, ba) = Some cap'\<rbrakk> \<Longrightarrow> (fst (transform_cslot_ptr (aaa, ba)), a, y) \<in> state_objs_to_policy s
 2. \<And>slot' slot. \<lbrakk>einvs s; (x, a, y) \<in> cdl_state_objs_to_policy (transform s); x = fst slot; a = Control; y = fst slot'; cdl_cdt (transform s) slot' = Some slot; \<not> cdl_cap_is_transferable (opt_cap slot' (transform s))\<rbrakk> \<Longrightarrow> (x, a, y) \<in> state_objs_to_policy s
 3. \<And>slot' slot. \<lbrakk>einvs s; (x, a, y) \<in> cdl_state_objs_to_policy (transform s); x = fst slot; a = DeleteDerived; y = fst slot'; cdl_cdt (transform s) slot' = Some slot\<rbrakk> \<Longrightarrow> (x, a, y) \<in> state_objs_to_policy s proof (prove)
goal (3 subgoals):
 1. \<And>aa b cap' aaa ba. \<lbrakk>(fst (transform_cslot_ptr (aaa, ba)), a, y) \<in> cdl_state_objs_to_policy (transform s); x = fst (transform_cslot_ptr (aaa, ba)); opt_cap (transform_cslot_ptr (aaa, ba)) (transform s) = Some (transform_cap cap'); y \<in> cdl_obj_refs (transform_cap cap'); a \<in> cdl_cap_auth_conferred (transform_cap cap'); \<not> is_thread_state_cap (transform_cap cap'); is_real_cap (transform_cap cap'); \<not> is_null_cap (transform_cap cap'); \<not> local.is_untyped_cap (transform_cap cap'); invs s; valid_list s; valid_sched s; (aa, b) = transform_cslot_ptr (aaa, ba); caps_of_state s (aaa, ba) = Some cap'\<rbrakk> \<Longrightarrow> (fst (aaa, ba), a, y) \<in> state_objs_to_policy s
 2. \<And>slot' slot. \<lbrakk>einvs s; (x, a, y) \<in> cdl_state_objs_to_policy (transform s); x = fst slot; a = Control; y = fst slot'; cdl_cdt (transform s) slot' = Some slot; \<not> cdl_cap_is_transferable (opt_cap slot' (transform s))\<rbrakk> \<Longrightarrow> (x, a, y) \<in> state_objs_to_policy s
 3. \<And>slot' slot. \<lbrakk>einvs s; (x, a, y) \<in> cdl_state_objs_to_policy (transform s); x = fst slot; a = DeleteDerived; y = fst slot'; cdl_cdt (transform s) slot' = Some slot\<rbrakk> \<Longrightarrow> (x, a, y) \<in> state_objs_to_policy s proof (prove)
goal (5 subgoals):
 1. \<And>aa b cap' aaa ba. \<lbrakk>(fst (transform_cslot_ptr (aaa, ba)), a, y) \<in> cdl_state_objs_to_policy (transform s); x = fst (transform_cslot_ptr (aaa, ba)); opt_cap (transform_cslot_ptr (aaa, ba)) (transform s) = Some (transform_cap cap'); y \<in> cdl_obj_refs (transform_cap cap'); a \<in> cdl_cap_auth_conferred (transform_cap cap'); \<not> is_thread_state_cap (transform_cap cap'); is_real_cap (transform_cap cap'); \<not> is_null_cap (transform_cap cap'); \<not> local.is_untyped_cap (transform_cap cap'); invs s; valid_list s; valid_sched s; (aa, b) = transform_cslot_ptr (aaa, ba); caps_of_state s (aaa, ba) = Some cap'\<rbrakk> \<Longrightarrow> caps_of_state s (aaa, ba) = Some cap'
 2. \<And>aa b cap' aaa ba. \<lbrakk>(fst (transform_cslot_ptr (aaa, ba)), a, y) \<in> cdl_state_objs_to_policy (transform s); x = fst (transform_cslot_ptr (aaa, ba)); opt_cap (transform_cslot_ptr (aaa, ba)) (transform s) = Some (transform_cap cap'); y \<in> cdl_obj_refs (transform_cap cap'); a \<in> cdl_cap_auth_conferred (transform_cap cap'); \<not> is_thread_state_cap (transform_cap cap'); is_real_cap (transform_cap cap'); \<not> is_null_cap (transform_cap cap'); \<not> local.is_untyped_cap (transform_cap cap'); invs s; valid_list s; valid_sched s; (aa, b) = transform_cslot_ptr (aaa, ba); caps_of_state s (aaa, ba) = Some cap'\<rbrakk> \<Longrightarrow> y \<in> obj_refs_ac cap'
 3. \<And>aa b cap' aaa ba. \<lbrakk>(fst (transform_cslot_ptr (aaa, ba)), a, y) \<in> cdl_state_objs_to_policy (transform s); x = fst (transform_cslot_ptr (aaa, ba)); opt_cap (transform_cslot_ptr (aaa, ba)) (transform s) = Some (transform_cap cap'); y \<in> cdl_obj_refs (transform_cap cap'); a \<in> cdl_cap_auth_conferred (transform_cap cap'); \<not> is_thread_state_cap (transform_cap cap'); is_real_cap (transform_cap cap'); \<not> is_null_cap (transform_cap cap'); \<not> local.is_untyped_cap (transform_cap cap'); invs s; valid_list s; valid_sched s; (aa, b) = transform_cslot_ptr (aaa, ba); caps_of_state s (aaa, ba) = Some cap'\<rbrakk> \<Longrightarrow> a \<in> cap_auth_conferred cap'
 4. \<And>slot' slot. \<lbrakk>einvs s; (x, a, y) \<in> cdl_state_objs_to_policy (transform s); x = fst slot; a = Control; y = fst slot'; cdl_cdt (transform s) slot' = Some slot; \<not> cdl_cap_is_transferable (opt_cap slot' (transform s))\<rbrakk> \<Longrightarrow> (x, a, y) \<in> state_objs_to_policy s
 5. \<And>slot' slot. \<lbrakk>einvs s; (x, a, y) \<in> cdl_state_objs_to_policy (transform s); x = fst slot; a = DeleteDerived; y = fst slot'; cdl_cdt (transform s) slot' = Some slot\<rbrakk> \<Longrightarrow> (x, a, y) \<in> state_objs_to_policy s proof (prove)
goal (4 subgoals):
 1. \<And>aa b cap' aaa ba. \<lbrakk>(fst (transform_cslot_ptr (aaa, ba)), a, y) \<in> cdl_state_objs_to_policy (transform s); x = fst (transform_cslot_ptr (aaa, ba)); opt_cap (transform_cslot_ptr (aaa, ba)) (transform s) = Some (transform_cap cap'); y \<in> cdl_obj_refs (transform_cap cap'); a \<in> cdl_cap_auth_conferred (transform_cap cap'); \<not> is_thread_state_cap (transform_cap cap'); is_real_cap (transform_cap cap'); \<not> is_null_cap (transform_cap cap'); \<not> local.is_untyped_cap (transform_cap cap'); invs s; valid_list s; valid_sched s; (aa, b) = transform_cslot_ptr (aaa, ba); caps_of_state s (aaa, ba) = Some cap'\<rbrakk> \<Longrightarrow> y \<in> obj_refs_ac cap'
 2. \<And>aa b cap' aaa ba. \<lbrakk>(fst (transform_cslot_ptr (aaa, ba)), a, y) \<in> cdl_state_objs_to_policy (transform s); x = fst (transform_cslot_ptr (aaa, ba)); opt_cap (transform_cslot_ptr (aaa, ba)) (transform s) = Some (transform_cap cap'); y \<in> cdl_obj_refs (transform_cap cap'); a \<in> cdl_cap_auth_conferred (transform_cap cap'); \<not> is_thread_state_cap (transform_cap cap'); is_real_cap (transform_cap cap'); \<not> is_null_cap (transform_cap cap'); \<not> local.is_untyped_cap (transform_cap cap'); invs s; valid_list s; valid_sched s; (aa, b) = transform_cslot_ptr (aaa, ba); caps_of_state s (aaa, ba) = Some cap'\<rbrakk> \<Longrightarrow> a \<in> cap_auth_conferred cap'
 3. \<And>slot' slot. \<lbrakk>einvs s; (x, a, y) \<in> cdl_state_objs_to_policy (transform s); x = fst slot; a = Control; y = fst slot'; cdl_cdt (transform s) slot' = Some slot; \<not> cdl_cap_is_transferable (opt_cap slot' (transform s))\<rbrakk> \<Longrightarrow> (x, a, y) \<in> state_objs_to_policy s
 4. \<And>slot' slot. \<lbrakk>einvs s; (x, a, y) \<in> cdl_state_objs_to_policy (transform s); x = fst slot; a = DeleteDerived; y = fst slot'; cdl_cdt (transform s) slot' = Some slot\<rbrakk> \<Longrightarrow> (x, a, y) \<in> state_objs_to_policy s proof (prove)
goal (5 subgoals):
 1. \<And>aa b cap' aaa ba. \<lbrakk>a \<in> cdl_cap_auth_conferred (transform_cap cap'); \<not> is_thread_state_cap (transform_cap cap'); is_real_cap (transform_cap cap'); \<not> is_null_cap (transform_cap cap'); \<not> local.is_untyped_cap (transform_cap cap'); invs s; valid_list s; valid_sched s; (aa, b) = transform_cslot_ptr (aaa, ba); caps_of_state s (aaa, ba) = Some cap'; (fst (transform_cslot_ptr (aaa, ba)), a, y) \<in> cdl_state_objs_to_policy (transform s); x = fst (transform_cslot_ptr (aaa, ba)); opt_cap (transform_cslot_ptr (aaa, ba)) (transform s) = Some (transform_cap cap')\<rbrakk> \<Longrightarrow> \<nexists>x sz i dev. cap' = cap.UntypedCap dev x sz i
 2. \<And>aa b cap' aaa ba. \<lbrakk>(fst (transform_cslot_ptr (aaa, ba)), a, y) \<in> cdl_state_objs_to_policy (transform s); x = fst (transform_cslot_ptr (aaa, ba)); opt_cap (transform_cslot_ptr (aaa, ba)) (transform s) = Some (transform_cap cap'); y \<in> obj_refs_ac cap'; a \<in> cdl_cap_auth_conferred (transform_cap cap'); \<not> is_thread_state_cap (transform_cap cap'); is_real_cap (transform_cap cap'); \<not> is_null_cap (transform_cap cap'); \<not> local.is_untyped_cap (transform_cap cap'); invs s; valid_list s; valid_sched s; (aa, b) = transform_cslot_ptr (aaa, ba); caps_of_state s (aaa, ba) = Some cap'\<rbrakk> \<Longrightarrow> y \<in> obj_refs_ac cap'
 3. \<And>aa b cap' aaa ba. \<lbrakk>(fst (transform_cslot_ptr (aaa, ba)), a, y) \<in> cdl_state_objs_to_policy (transform s); x = fst (transform_cslot_ptr (aaa, ba)); opt_cap (transform_cslot_ptr (aaa, ba)) (transform s) = Some (transform_cap cap'); y \<in> cdl_obj_refs (transform_cap cap'); a \<in> cdl_cap_auth_conferred (transform_cap cap'); \<not> is_thread_state_cap (transform_cap cap'); is_real_cap (transform_cap cap'); \<not> is_null_cap (transform_cap cap'); \<not> local.is_untyped_cap (transform_cap cap'); invs s; valid_list s; valid_sched s; (aa, b) = transform_cslot_ptr (aaa, ba); caps_of_state s (aaa, ba) = Some cap'\<rbrakk> \<Longrightarrow> a \<in> cap_auth_conferred cap'
 4. \<And>slot' slot. \<lbrakk>einvs s; (x, a, y) \<in> cdl_state_objs_to_policy (transform s); x = fst slot; a = Control; y = fst slot'; cdl_cdt (transform s) slot' = Some slot; \<not> cdl_cap_is_transferable (opt_cap slot' (transform s))\<rbrakk> \<Longrightarrow> (x, a, y) \<in> state_objs_to_policy s
 5. \<And>slot' slot. \<lbrakk>einvs s; (x, a, y) \<in> cdl_state_objs_to_policy (transform s); x = fst slot; a = DeleteDerived; y = fst slot'; cdl_cdt (transform s) slot' = Some slot\<rbrakk> \<Longrightarrow> (x, a, y) \<in> state_objs_to_policy s proof (prove)
goal (4 subgoals):
 1. \<And>aa b cap' aaa ba. \<lbrakk>(fst (transform_cslot_ptr (aaa, ba)), a, y) \<in> cdl_state_objs_to_policy (transform s); x = fst (transform_cslot_ptr (aaa, ba)); opt_cap (transform_cslot_ptr (aaa, ba)) (transform s) = Some (transform_cap cap'); y \<in> obj_refs_ac cap'; a \<in> cdl_cap_auth_conferred (transform_cap cap'); \<not> is_thread_state_cap (transform_cap cap'); is_real_cap (transform_cap cap'); \<not> is_null_cap (transform_cap cap'); \<not> local.is_untyped_cap (transform_cap cap'); invs s; valid_list s; valid_sched s; (aa, b) = transform_cslot_ptr (aaa, ba); caps_of_state s (aaa, ba) = Some cap'\<rbrakk> \<Longrightarrow> y \<in> obj_refs_ac cap'
 2. \<And>aa b cap' aaa ba. \<lbrakk>(fst (transform_cslot_ptr (aaa, ba)), a, y) \<in> cdl_state_objs_to_policy (transform s); x = fst (transform_cslot_ptr (aaa, ba)); opt_cap (transform_cslot_ptr (aaa, ba)) (transform s) = Some (transform_cap cap'); y \<in> cdl_obj_refs (transform_cap cap'); a \<in> cdl_cap_auth_conferred (transform_cap cap'); \<not> is_thread_state_cap (transform_cap cap'); is_real_cap (transform_cap cap'); \<not> is_null_cap (transform_cap cap'); \<not> local.is_untyped_cap (transform_cap cap'); invs s; valid_list s; valid_sched s; (aa, b) = transform_cslot_ptr (aaa, ba); caps_of_state s (aaa, ba) = Some cap'\<rbrakk> \<Longrightarrow> a \<in> cap_auth_conferred cap'
 3. \<And>slot' slot. \<lbrakk>einvs s; (x, a, y) \<in> cdl_state_objs_to_policy (transform s); x = fst slot; a = Control; y = fst slot'; cdl_cdt (transform s) slot' = Some slot; \<not> cdl_cap_is_transferable (opt_cap slot' (transform s))\<rbrakk> \<Longrightarrow> (x, a, y) \<in> state_objs_to_policy s
 4. \<And>slot' slot. \<lbrakk>einvs s; (x, a, y) \<in> cdl_state_objs_to_policy (transform s); x = fst slot; a = DeleteDerived; y = fst slot'; cdl_cdt (transform s) slot' = Some slot\<rbrakk> \<Longrightarrow> (x, a, y) \<in> state_objs_to_policy s proof (prove)
goal (3 subgoals):
 1. \<And>aa b cap' aaa ba. \<lbrakk>(fst (transform_cslot_ptr (aaa, ba)), a, y) \<in> cdl_state_objs_to_policy (transform s); x = fst (transform_cslot_ptr (aaa, ba)); opt_cap (transform_cslot_ptr (aaa, ba)) (transform s) = Some (transform_cap cap'); y \<in> cdl_obj_refs (transform_cap cap'); a \<in> cdl_cap_auth_conferred (transform_cap cap'); \<not> is_thread_state_cap (transform_cap cap'); is_real_cap (transform_cap cap'); \<not> is_null_cap (transform_cap cap'); \<not> local.is_untyped_cap (transform_cap cap'); invs s; valid_list s; valid_sched s; (aa, b) = transform_cslot_ptr (aaa, ba); caps_of_state s (aaa, ba) = Some cap'\<rbrakk> \<Longrightarrow> a \<in> cap_auth_conferred cap'
 2. \<And>slot' slot. \<lbrakk>einvs s; (x, a, y) \<in> cdl_state_objs_to_policy (transform s); x = fst slot; a = Control; y = fst slot'; cdl_cdt (transform s) slot' = Some slot; \<not> cdl_cap_is_transferable (opt_cap slot' (transform s))\<rbrakk> \<Longrightarrow> (x, a, y) \<in> state_objs_to_policy s
 3. \<And>slot' slot. \<lbrakk>einvs s; (x, a, y) \<in> cdl_state_objs_to_policy (transform s); x = fst slot; a = DeleteDerived; y = fst slot'; cdl_cdt (transform s) slot' = Some slot\<rbrakk> \<Longrightarrow> (x, a, y) \<in> state_objs_to_policy s proof (prove)
goal (2 subgoals):
 1. \<And>slot' slot. \<lbrakk>einvs s; (x, a, y) \<in> cdl_state_objs_to_policy (transform s); x = fst slot; a = Control; y = fst slot'; cdl_cdt (transform s) slot' = Some slot; \<not> cdl_cap_is_transferable (opt_cap slot' (transform s))\<rbrakk> \<Longrightarrow> (x, a, y) \<in> state_objs_to_policy s
 2. \<And>slot' slot. \<lbrakk>einvs s; (x, a, y) \<in> cdl_state_objs_to_policy (transform s); x = fst slot; a = DeleteDerived; y = fst slot'; cdl_cdt (transform s) slot' = Some slot\<rbrakk> \<Longrightarrow> (x, a, y) \<in> state_objs_to_policy s proof (prove)
goal (2 subgoals):
 1. \<And>slot' slot. \<lbrakk>invs s \<and> valid_list s \<and> valid_sched s; (fst slot, Control, fst slot') \<in> cdl_state_objs_to_policy (transform s); x = fst slot; a = Control; y = fst slot'; \<not> cdl_cap_is_transferable (opt_cap slot' (transform s)); \<exists>a b. slot' = transform_cslot_ptr (a, b) \<and> (\<exists>aa ba. slot = transform_cslot_ptr (aa, ba) \<and> cdt s (a, b) = Some (aa, ba))\<rbrakk> \<Longrightarrow> (fst slot, Control, fst slot') \<in> state_objs_to_policy s
 2. \<And>slot' slot. \<lbrakk>einvs s; (x, a, y) \<in> cdl_state_objs_to_policy (transform s); x = fst slot; a = DeleteDerived; y = fst slot'; cdl_cdt (transform s) slot' = Some slot\<rbrakk> \<Longrightarrow> (x, a, y) \<in> state_objs_to_policy s proof (prove)
goal (2 subgoals):
 1. \<And>aa b aaa ba ab bb ac bc. \<lbrakk>(fst (transform_cslot_ptr (ac, bc)), Control, fst (transform_cslot_ptr (ab, bb))) \<in> cdl_state_objs_to_policy (transform s); x = fst (transform_cslot_ptr (ac, bc)); a = Control; y = fst (transform_cslot_ptr (ab, bb)); \<not> cdl_cap_is_transferable (opt_cap (transform_cslot_ptr (ab, bb)) (transform s)); invs s; (aa, b) = transform_cslot_ptr (ab, bb); valid_list s; valid_sched s; (aaa, ba) = transform_cslot_ptr (ac, bc); cdt s (ab, bb) = Some (ac, bc)\<rbrakk> \<Longrightarrow> (fst (transform_cslot_ptr (ac, bc)), Control, fst (transform_cslot_ptr (ab, bb))) \<in> state_objs_to_policy s
 2. \<And>slot' slot. \<lbrakk>einvs s; (x, a, y) \<in> cdl_state_objs_to_policy (transform s); x = fst slot; a = DeleteDerived; y = fst slot'; cdl_cdt (transform s) slot' = Some slot\<rbrakk> \<Longrightarrow> (x, a, y) \<in> state_objs_to_policy s proof (prove)
goal (2 subgoals):
 1. \<And>aa b aaa ba ab bb ac bc. \<lbrakk>(fst (transform_cslot_ptr (ac, bc)), Control, fst (transform_cslot_ptr (ab, bb))) \<in> cdl_state_objs_to_policy (transform s); x = fst (transform_cslot_ptr (ac, bc)); a = Control; y = fst (transform_cslot_ptr (ab, bb)); \<not> cdl_cap_is_transferable (opt_cap (transform_cslot_ptr (ab, bb)) (transform s)); invs s; (aa, b) = transform_cslot_ptr (ab, bb); valid_list s; valid_sched s; (aaa, ba) = transform_cslot_ptr (ac, bc); cdt s (ab, bb) = Some (ac, bc)\<rbrakk> \<Longrightarrow> (fst (ac, bc), Control, fst (ab, bb)) \<in> state_objs_to_policy s
 2. \<And>slot' slot. \<lbrakk>einvs s; (x, a, y) \<in> cdl_state_objs_to_policy (transform s); x = fst slot; a = DeleteDerived; y = fst slot'; cdl_cdt (transform s) slot' = Some slot\<rbrakk> \<Longrightarrow> (x, a, y) \<in> state_objs_to_policy s proof (prove)
goal (3 subgoals):
 1. \<And>aa b aaa ba ab bb ac bc. \<lbrakk>(fst (transform_cslot_ptr (ac, bc)), Control, fst (transform_cslot_ptr (ab, bb))) \<in> cdl_state_objs_to_policy (transform s); x = fst (transform_cslot_ptr (ac, bc)); a = Control; y = fst (transform_cslot_ptr (ab, bb)); \<not> cdl_cap_is_transferable (opt_cap (transform_cslot_ptr (ab, bb)) (transform s)); invs s; (aa, b) = transform_cslot_ptr (ab, bb); valid_list s; valid_sched s; (aaa, ba) = transform_cslot_ptr (ac, bc); cdt s (ab, bb) = Some (ac, bc)\<rbrakk> \<Longrightarrow> cdt s (ab, bb) = Some (ac, bc)
 2. \<And>aa b aaa ba ab bb ac bc. \<lbrakk>(fst (transform_cslot_ptr (ac, bc)), Control, fst (transform_cslot_ptr (ab, bb))) \<in> cdl_state_objs_to_policy (transform s); x = fst (transform_cslot_ptr (ac, bc)); a = Control; y = fst (transform_cslot_ptr (ab, bb)); \<not> cdl_cap_is_transferable (opt_cap (transform_cslot_ptr (ab, bb)) (transform s)); invs s; (aa, b) = transform_cslot_ptr (ab, bb); valid_list s; valid_sched s; (aaa, ba) = transform_cslot_ptr (ac, bc); cdt s (ab, bb) = Some (ac, bc)\<rbrakk> \<Longrightarrow> \<not> is_transferable_in (ab, bb) s
 3. \<And>slot' slot. \<lbrakk>einvs s; (x, a, y) \<in> cdl_state_objs_to_policy (transform s); x = fst slot; a = DeleteDerived; y = fst slot'; cdl_cdt (transform s) slot' = Some slot\<rbrakk> \<Longrightarrow> (x, a, y) \<in> state_objs_to_policy s proof (prove)
goal (2 subgoals):
 1. \<And>aa b aaa ba ab bb ac bc. \<lbrakk>(fst (transform_cslot_ptr (ac, bc)), Control, fst (transform_cslot_ptr (ab, bb))) \<in> cdl_state_objs_to_policy (transform s); x = fst (transform_cslot_ptr (ac, bc)); a = Control; y = fst (transform_cslot_ptr (ab, bb)); \<not> cdl_cap_is_transferable (opt_cap (transform_cslot_ptr (ab, bb)) (transform s)); invs s; (aa, b) = transform_cslot_ptr (ab, bb); valid_list s; valid_sched s; (aaa, ba) = transform_cslot_ptr (ac, bc); cdt s (ab, bb) = Some (ac, bc)\<rbrakk> \<Longrightarrow> \<not> is_transferable_in (ab, bb) s
 2. \<And>slot' slot. \<lbrakk>einvs s; (x, a, y) \<in> cdl_state_objs_to_policy (transform s); x = fst slot; a = DeleteDerived; y = fst slot'; cdl_cdt (transform s) slot' = Some slot\<rbrakk> \<Longrightarrow> (x, a, y) \<in> state_objs_to_policy s proof (prove)
goal (2 subgoals):
 1. \<And>aa b aaa ba ab bb ac bc. \<lbrakk>(fst (transform_cslot_ptr (ac, bc)), Control, fst (transform_cslot_ptr (ab, bb))) \<in> cdl_state_objs_to_policy (transform s); x = fst (transform_cslot_ptr (ac, bc)); a = Control; y = fst (transform_cslot_ptr (ab, bb)); invs s; (aa, b) = transform_cslot_ptr (ab, bb); valid_list s; valid_sched s; (aaa, ba) = transform_cslot_ptr (ac, bc); cdt s (ab, bb) = Some (ac, bc); is_transferable_in (ab, bb) s\<rbrakk> \<Longrightarrow> cdl_cap_is_transferable (opt_cap (transform_cslot_ptr (ab, bb)) (transform s))
 2. \<And>slot' slot. \<lbrakk>einvs s; (x, a, y) \<in> cdl_state_objs_to_policy (transform s); x = fst slot; a = DeleteDerived; y = fst slot'; cdl_cdt (transform s) slot' = Some slot\<rbrakk> \<Longrightarrow> (x, a, y) \<in> state_objs_to_policy s proof (prove)
goal (2 subgoals):
 1. \<And>aa b aaa ba ab bb ac bc. \<lbrakk>(fst (transform_cslot_ptr (ac, bc)), Control, fst (transform_cslot_ptr (ab, bb))) \<in> cdl_state_objs_to_policy (transform s); x = fst (transform_cslot_ptr (ac, bc)); a = Control; y = fst (transform_cslot_ptr (ab, bb)); invs s; (aa, b) = transform_cslot_ptr (ab, bb); valid_list s; valid_sched s; (aaa, ba) = transform_cslot_ptr (ac, bc); cdt s (ab, bb) = Some (ac, bc); is_transferable_in (ab, bb) s; \<forall>a b aa ba. cdt s (aa, ba) = Some (a, b) \<longrightarrow> (\<exists>c. caps_of_state s (a, b) = Some c \<and> cap.NullCap \<noteq> c) \<and> (\<exists>c. caps_of_state s (aa, ba) = Some c \<and> cap.NullCap \<noteq> c)\<rbrakk> \<Longrightarrow> cdl_cap_is_transferable (opt_cap (transform_cslot_ptr (ab, bb)) (transform s))
 2. \<And>slot' slot. \<lbrakk>einvs s; (x, a, y) \<in> cdl_state_objs_to_policy (transform s); x = fst slot; a = DeleteDerived; y = fst slot'; cdl_cdt (transform s) slot' = Some slot\<rbrakk> \<Longrightarrow> (x, a, y) \<in> state_objs_to_policy s proof (prove)
goal (4 subgoals):
 1. \<And>aa b aaa ba ab bb ac bc. \<lbrakk>(fst (transform_cslot_ptr (ac, bc)), Control, fst (transform_cslot_ptr (ab, bb))) \<in> cdl_state_objs_to_policy (transform s); x = fst (transform_cslot_ptr (ac, bc)); a = Control; y = fst (transform_cslot_ptr (ab, bb)); invs s; (aa, b) = transform_cslot_ptr (ab, bb); valid_list s; valid_sched s; (aaa, ba) = transform_cslot_ptr (ac, bc); cdt s (ab, bb) = Some (ac, bc); \<forall>a b aa ba. cdt s (aa, ba) = Some (a, b) \<longrightarrow> (\<exists>c. caps_of_state s (a, b) = Some c \<and> cap.NullCap \<noteq> c) \<and> (\<exists>c. caps_of_state s (aa, ba) = Some c \<and> cap.NullCap \<noteq> c); caps_of_state s (ab, bb) = None\<rbrakk> \<Longrightarrow> cdl_cap_is_transferable (opt_cap (transform_cslot_ptr (ab, bb)) (transform s))
 2. \<And>aa b aaa ba ab bb ac bc. \<lbrakk>(fst (transform_cslot_ptr (ac, bc)), Control, fst (transform_cslot_ptr (ab, bb))) \<in> cdl_state_objs_to_policy (transform s); x = fst (transform_cslot_ptr (ac, bc)); a = Control; y = fst (transform_cslot_ptr (ab, bb)); invs s; (aa, b) = transform_cslot_ptr (ab, bb); valid_list s; valid_sched s; (aaa, ba) = transform_cslot_ptr (ac, bc); cdt s (ab, bb) = Some (ac, bc); \<forall>a b aa ba. cdt s (aa, ba) = Some (a, b) \<longrightarrow> (\<exists>c. caps_of_state s (a, b) = Some c \<and> cap.NullCap \<noteq> c) \<and> (\<exists>c. caps_of_state s (aa, ba) = Some c \<and> cap.NullCap \<noteq> c); caps_of_state s (ab, bb) = Some cap.NullCap\<rbrakk> \<Longrightarrow> cdl_cap_is_transferable (opt_cap (transform_cslot_ptr (ab, bb)) (transform s))
 3. \<And>aa b aaa ba ab bb ac bc t R. \<lbrakk>(fst (transform_cslot_ptr (ac, bc)), Control, fst (transform_cslot_ptr (ab, bb))) \<in> cdl_state_objs_to_policy (transform s); x = fst (transform_cslot_ptr (ac, bc)); a = Control; y = fst (transform_cslot_ptr (ab, bb)); invs s; (aa, b) = transform_cslot_ptr (ab, bb); valid_list s; valid_sched s; (aaa, ba) = transform_cslot_ptr (ac, bc); cdt s (ab, bb) = Some (ac, bc); \<forall>a b aa ba. cdt s (aa, ba) = Some (a, b) \<longrightarrow> (\<exists>c. caps_of_state s (a, b) = Some c \<and> cap.NullCap \<noteq> c) \<and> (\<exists>c. caps_of_state s (aa, ba) = Some c \<and> cap.NullCap \<noteq> c); caps_of_state s (ab, bb) = Some (cap.ReplyCap t False R)\<rbrakk> \<Longrightarrow> cdl_cap_is_transferable (opt_cap (transform_cslot_ptr (ab, bb)) (transform s))
 4. \<And>slot' slot. \<lbrakk>einvs s; (x, a, y) \<in> cdl_state_objs_to_policy (transform s); x = fst slot; a = DeleteDerived; y = fst slot'; cdl_cdt (transform s) slot' = Some slot\<rbrakk> \<Longrightarrow> (x, a, y) \<in> state_objs_to_policy s proof (prove)
goal (3 subgoals):
 1. \<And>aa b aaa ba ab bb ac bc. \<lbrakk>(fst (transform_cslot_ptr (ac, bc)), Control, fst (transform_cslot_ptr (ab, bb))) \<in> cdl_state_objs_to_policy (transform s); x = fst (transform_cslot_ptr (ac, bc)); a = Control; y = fst (transform_cslot_ptr (ab, bb)); invs s; (aa, b) = transform_cslot_ptr (ab, bb); valid_list s; valid_sched s; (aaa, ba) = transform_cslot_ptr (ac, bc); cdt s (ab, bb) = Some (ac, bc); \<forall>a b aa ba. cdt s (aa, ba) = Some (a, b) \<longrightarrow> (\<exists>c. caps_of_state s (a, b) = Some c \<and> cap.NullCap \<noteq> c) \<and> (\<exists>c. caps_of_state s (aa, ba) = Some c \<and> cap.NullCap \<noteq> c); caps_of_state s (ab, bb) = Some cap.NullCap\<rbrakk> \<Longrightarrow> cdl_cap_is_transferable (opt_cap (transform_cslot_ptr (ab, bb)) (transform s))
 2. \<And>aa b aaa ba ab bb ac bc t R. \<lbrakk>(fst (transform_cslot_ptr (ac, bc)), Control, fst (transform_cslot_ptr (ab, bb))) \<in> cdl_state_objs_to_policy (transform s); x = fst (transform_cslot_ptr (ac, bc)); a = Control; y = fst (transform_cslot_ptr (ab, bb)); invs s; (aa, b) = transform_cslot_ptr (ab, bb); valid_list s; valid_sched s; (aaa, ba) = transform_cslot_ptr (ac, bc); cdt s (ab, bb) = Some (ac, bc); \<forall>a b aa ba. cdt s (aa, ba) = Some (a, b) \<longrightarrow> (\<exists>c. caps_of_state s (a, b) = Some c \<and> cap.NullCap \<noteq> c) \<and> (\<exists>c. caps_of_state s (aa, ba) = Some c \<and> cap.NullCap \<noteq> c); caps_of_state s (ab, bb) = Some (cap.ReplyCap t False R)\<rbrakk> \<Longrightarrow> cdl_cap_is_transferable (opt_cap (transform_cslot_ptr (ab, bb)) (transform s))
 3. \<And>slot' slot. \<lbrakk>einvs s; (x, a, y) \<in> cdl_state_objs_to_policy (transform s); x = fst slot; a = DeleteDerived; y = fst slot'; cdl_cdt (transform s) slot' = Some slot\<rbrakk> \<Longrightarrow> (x, a, y) \<in> state_objs_to_policy s proof (prove)
goal (2 subgoals):
 1. \<And>aa b aaa ba ab bb ac bc t R. \<lbrakk>(fst (transform_cslot_ptr (ac, bc)), Control, fst (transform_cslot_ptr (ab, bb))) \<in> cdl_state_objs_to_policy (transform s); x = fst (transform_cslot_ptr (ac, bc)); a = Control; y = fst (transform_cslot_ptr (ab, bb)); invs s; (aa, b) = transform_cslot_ptr (ab, bb); valid_list s; valid_sched s; (aaa, ba) = transform_cslot_ptr (ac, bc); cdt s (ab, bb) = Some (ac, bc); \<forall>a b aa ba. cdt s (aa, ba) = Some (a, b) \<longrightarrow> (\<exists>c. caps_of_state s (a, b) = Some c \<and> cap.NullCap \<noteq> c) \<and> (\<exists>c. caps_of_state s (aa, ba) = Some c \<and> cap.NullCap \<noteq> c); caps_of_state s (ab, bb) = Some (cap.ReplyCap t False R)\<rbrakk> \<Longrightarrow> cdl_cap_is_transferable (opt_cap (transform_cslot_ptr (ab, bb)) (transform s))
 2. \<And>slot' slot. \<lbrakk>einvs s; (x, a, y) \<in> cdl_state_objs_to_policy (transform s); x = fst slot; a = DeleteDerived; y = fst slot'; cdl_cdt (transform s) slot' = Some slot\<rbrakk> \<Longrightarrow> (x, a, y) \<in> state_objs_to_policy s proof (prove)
goal (2 subgoals):
 1. \<And>aa b aaa ba ab bb ac bc t R c. \<lbrakk>(fst (transform_cslot_ptr (ac, bc)), Control, fst (transform_cslot_ptr (ab, bb))) \<in> cdl_state_objs_to_policy (transform s); x = fst (transform_cslot_ptr (ac, bc)); a = Control; y = fst (transform_cslot_ptr (ab, bb)); invs s; (aa, b) = transform_cslot_ptr (ab, bb); valid_list s; valid_sched s; (aaa, ba) = transform_cslot_ptr (ac, bc); cdt s (ab, bb) = Some (ac, bc); caps_of_state s (ab, bb) = Some (cap.ReplyCap t False R); caps_of_state s (ac, bc) = Some c; cap.NullCap \<noteq> c\<rbrakk> \<Longrightarrow> cdl_cap_is_transferable (opt_cap (transform_cslot_ptr (ab, bb)) (transform s))
 2. \<And>slot' slot. \<lbrakk>einvs s; (x, a, y) \<in> cdl_state_objs_to_policy (transform s); x = fst slot; a = DeleteDerived; y = fst slot'; cdl_cdt (transform s) slot' = Some slot\<rbrakk> \<Longrightarrow> (x, a, y) \<in> state_objs_to_policy s proof (prove)
goal (5 subgoals):
 1. \<And>aa b aaa ba ab bb ac bc t R c. \<lbrakk>(fst (transform_cslot_ptr (ac, bc)), Control, fst (transform_cslot_ptr (ab, bb))) \<in> cdl_state_objs_to_policy (transform s); x = fst (transform_cslot_ptr (ac, bc)); a = Control; y = fst (transform_cslot_ptr (ab, bb)); invs s; (aa, b) = transform_cslot_ptr (ab, bb); valid_list s; valid_sched s; (aaa, ba) = transform_cslot_ptr (ac, bc); cdt s (ab, bb) = Some (ac, bc); caps_of_state s (ab, bb) = Some (cap.ReplyCap t False R); caps_of_state s (ac, bc) = Some c; cap.NullCap \<noteq> c\<rbrakk> \<Longrightarrow> caps_of_state s (ab, bb) = Some (?cap1679 aa b aaa ba ab bb ac bc t R c)
 2. \<And>aa b aaa ba ab bb ac bc t R c. \<lbrakk>(fst (transform_cslot_ptr (ac, bc)), Control, fst (transform_cslot_ptr (ab, bb))) \<in> cdl_state_objs_to_policy (transform s); x = fst (transform_cslot_ptr (ac, bc)); a = Control; y = fst (transform_cslot_ptr (ab, bb)); invs s; (aa, b) = transform_cslot_ptr (ab, bb); valid_list s; valid_sched s; (aaa, ba) = transform_cslot_ptr (ac, bc); cdt s (ab, bb) = Some (ac, bc); caps_of_state s (ab, bb) = Some (cap.ReplyCap t False R); caps_of_state s (ac, bc) = Some c; cap.NullCap \<noteq> c\<rbrakk> \<Longrightarrow> valid_etcbs s
 3. \<And>aa b aaa ba ab bb ac bc t R c. \<lbrakk>(fst (transform_cslot_ptr (ac, bc)), Control, fst (transform_cslot_ptr (ab, bb))) \<in> cdl_state_objs_to_policy (transform s); x = fst (transform_cslot_ptr (ac, bc)); a = Control; y = fst (transform_cslot_ptr (ab, bb)); invs s; (aa, b) = transform_cslot_ptr (ab, bb); valid_list s; valid_sched s; (aaa, ba) = transform_cslot_ptr (ac, bc); cdt s (ab, bb) = Some (ac, bc); caps_of_state s (ab, bb) = Some (cap.ReplyCap t False R); caps_of_state s (ac, bc) = Some c; cap.NullCap \<noteq> c\<rbrakk> \<Longrightarrow> fst (ab, bb) \<noteq> idle_thread s
 4. \<And>aa b aaa ba ab bb ac bc t R c. \<lbrakk>(fst (transform_cslot_ptr (ac, bc)), Control, fst (transform_cslot_ptr (ab, bb))) \<in> cdl_state_objs_to_policy (transform s); x = fst (transform_cslot_ptr (ac, bc)); a = Control; y = fst (transform_cslot_ptr (ab, bb)); invs s; (aa, b) = transform_cslot_ptr (ab, bb); valid_list s; valid_sched s; (aaa, ba) = transform_cslot_ptr (ac, bc); cdt s (ab, bb) = Some (ac, bc); caps_of_state s (ab, bb) = Some (cap.ReplyCap t False R); caps_of_state s (ac, bc) = Some c; cap.NullCap \<noteq> c\<rbrakk> \<Longrightarrow> cdl_cap_is_transferable (Some (transform_cap (?cap1679 aa b aaa ba ab bb ac bc t R c)))
 5. \<And>slot' slot. \<lbrakk>einvs s; (x, a, y) \<in> cdl_state_objs_to_policy (transform s); x = fst slot; a = DeleteDerived; y = fst slot'; cdl_cdt (transform s) slot' = Some slot\<rbrakk> \<Longrightarrow> (x, a, y) \<in> state_objs_to_policy s proof (prove)
goal (4 subgoals):
 1. \<And>aa b aaa ba ab bb ac bc t R c. \<lbrakk>(fst (transform_cslot_ptr (ac, bc)), Control, fst (transform_cslot_ptr (ab, bb))) \<in> cdl_state_objs_to_policy (transform s); x = fst (transform_cslot_ptr (ac, bc)); a = Control; y = fst (transform_cslot_ptr (ab, bb)); invs s; (aa, b) = transform_cslot_ptr (ab, bb); valid_list s; valid_sched s; (aaa, ba) = transform_cslot_ptr (ac, bc); cdt s (ab, bb) = Some (ac, bc); caps_of_state s (ab, bb) = Some (cap.ReplyCap t False R); caps_of_state s (ac, bc) = Some c; cap.NullCap \<noteq> c\<rbrakk> \<Longrightarrow> valid_etcbs s
 2. \<And>aa b aaa ba ab bb ac bc t R c. \<lbrakk>(fst (transform_cslot_ptr (ac, bc)), Control, fst (transform_cslot_ptr (ab, bb))) \<in> cdl_state_objs_to_policy (transform s); x = fst (transform_cslot_ptr (ac, bc)); a = Control; y = fst (transform_cslot_ptr (ab, bb)); invs s; (aa, b) = transform_cslot_ptr (ab, bb); valid_list s; valid_sched s; (aaa, ba) = transform_cslot_ptr (ac, bc); cdt s (ab, bb) = Some (ac, bc); caps_of_state s (ab, bb) = Some (cap.ReplyCap t False R); caps_of_state s (ac, bc) = Some c; cap.NullCap \<noteq> c\<rbrakk> \<Longrightarrow> fst (ab, bb) \<noteq> idle_thread s
 3. \<And>aa b aaa ba ab bb ac bc t R c. \<lbrakk>(fst (transform_cslot_ptr (ac, bc)), Control, fst (transform_cslot_ptr (ab, bb))) \<in> cdl_state_objs_to_policy (transform s); x = fst (transform_cslot_ptr (ac, bc)); a = Control; y = fst (transform_cslot_ptr (ab, bb)); invs s; (aa, b) = transform_cslot_ptr (ab, bb); valid_list s; valid_sched s; (aaa, ba) = transform_cslot_ptr (ac, bc); cdt s (ab, bb) = Some (ac, bc); caps_of_state s (ab, bb) = Some (cap.ReplyCap t False R); caps_of_state s (ac, bc) = Some c; cap.NullCap \<noteq> c\<rbrakk> \<Longrightarrow> cdl_cap_is_transferable (Some (transform_cap (cap.ReplyCap t False R)))
 4. \<And>slot' slot. \<lbrakk>einvs s; (x, a, y) \<in> cdl_state_objs_to_policy (transform s); x = fst slot; a = DeleteDerived; y = fst slot'; cdl_cdt (transform s) slot' = Some slot\<rbrakk> \<Longrightarrow> (x, a, y) \<in> state_objs_to_policy s proof (prove)
goal (3 subgoals):
 1. \<And>aa b aaa ba ab bb ac bc t R c. \<lbrakk>(fst (transform_cslot_ptr (ac, bc)), Control, fst (transform_cslot_ptr (ab, bb))) \<in> cdl_state_objs_to_policy (transform s); x = fst (transform_cslot_ptr (ac, bc)); a = Control; y = fst (transform_cslot_ptr (ab, bb)); invs s; (aa, b) = transform_cslot_ptr (ab, bb); valid_list s; valid_sched s; (aaa, ba) = transform_cslot_ptr (ac, bc); cdt s (ab, bb) = Some (ac, bc); caps_of_state s (ab, bb) = Some (cap.ReplyCap t False R); caps_of_state s (ac, bc) = Some c; cap.NullCap \<noteq> c\<rbrakk> \<Longrightarrow> fst (ab, bb) \<noteq> idle_thread s
 2. \<And>aa b aaa ba ab bb ac bc t R c. \<lbrakk>(fst (transform_cslot_ptr (ac, bc)), Control, fst (transform_cslot_ptr (ab, bb))) \<in> cdl_state_objs_to_policy (transform s); x = fst (transform_cslot_ptr (ac, bc)); a = Control; y = fst (transform_cslot_ptr (ab, bb)); invs s; (aa, b) = transform_cslot_ptr (ab, bb); valid_list s; valid_sched s; (aaa, ba) = transform_cslot_ptr (ac, bc); cdt s (ab, bb) = Some (ac, bc); caps_of_state s (ab, bb) = Some (cap.ReplyCap t False R); caps_of_state s (ac, bc) = Some c; cap.NullCap \<noteq> c\<rbrakk> \<Longrightarrow> cdl_cap_is_transferable (Some (transform_cap (cap.ReplyCap t False R)))
 3. \<And>slot' slot. \<lbrakk>einvs s; (x, a, y) \<in> cdl_state_objs_to_policy (transform s); x = fst slot; a = DeleteDerived; y = fst slot'; cdl_cdt (transform s) slot' = Some slot\<rbrakk> \<Longrightarrow> (x, a, y) \<in> state_objs_to_policy s proof (prove)
goal (2 subgoals):
 1. \<And>aa b aaa ba ab bb ac bc t R c. \<lbrakk>(fst (transform_cslot_ptr (ac, bc)), Control, fst (transform_cslot_ptr (ab, bb))) \<in> cdl_state_objs_to_policy (transform s); x = fst (transform_cslot_ptr (ac, bc)); a = Control; y = fst (transform_cslot_ptr (ab, bb)); invs s; (aa, b) = transform_cslot_ptr (ab, bb); valid_list s; valid_sched s; (aaa, ba) = transform_cslot_ptr (ac, bc); cdt s (ab, bb) = Some (ac, bc); caps_of_state s (ab, bb) = Some (cap.ReplyCap t False R); caps_of_state s (ac, bc) = Some c; cap.NullCap \<noteq> c\<rbrakk> \<Longrightarrow> cdl_cap_is_transferable (Some (transform_cap (cap.ReplyCap t False R)))
 2. \<And>slot' slot. \<lbrakk>einvs s; (x, a, y) \<in> cdl_state_objs_to_policy (transform s); x = fst slot; a = DeleteDerived; y = fst slot'; cdl_cdt (transform s) slot' = Some slot\<rbrakk> \<Longrightarrow> (x, a, y) \<in> state_objs_to_policy s proof (prove)
goal (2 subgoals):
 1. \<And>aa b aaa ba ab bb ac bc t R c. \<lbrakk>(fst (transform_cslot_ptr (ac, bc)), Control, fst (transform_cslot_ptr (ab, bb))) \<in> cdl_state_objs_to_policy (transform s); x = fst (transform_cslot_ptr (ac, bc)); a = Control; y = fst (transform_cslot_ptr (ab, bb)); invs s; (aa, b) = transform_cslot_ptr (ab, bb); valid_list s; valid_sched s; (aaa, ba) = transform_cslot_ptr (ac, bc); cdt s (ab, bb) = Some (ac, bc); caps_of_state s (ab, bb) = Some (cap.ReplyCap t False R); caps_of_state s (ac, bc) = Some c; cap.NullCap \<noteq> c\<rbrakk> \<Longrightarrow> cdl_cap_is_transferable (Some (cdl_cap.ReplyCap t R))
 2. \<And>slot' slot. \<lbrakk>einvs s; (x, a, y) \<in> cdl_state_objs_to_policy (transform s); x = fst slot; a = DeleteDerived; y = fst slot'; cdl_cdt (transform s) slot' = Some slot\<rbrakk> \<Longrightarrow> (x, a, y) \<in> state_objs_to_policy s proof (prove)
goal (1 subgoal):
 1. \<And>slot' slot. \<lbrakk>einvs s; (x, a, y) \<in> cdl_state_objs_to_policy (transform s); x = fst slot; a = DeleteDerived; y = fst slot'; cdl_cdt (transform s) slot' = Some slot\<rbrakk> \<Longrightarrow> (x, a, y) \<in> state_objs_to_policy s proof (prove)
goal (1 subgoal):
 1. \<And>b ba. \<lbrakk>(x, DeleteDerived, y) \<in> cdl_state_objs_to_policy (transform s); a = DeleteDerived; cdl_cdt (transform s) (y, b) = Some (x, ba); invs s; valid_list s; valid_sched s\<rbrakk> \<Longrightarrow> (x, DeleteDerived, y) \<in> state_objs_to_policy s proof (prove)
goal (1 subgoal):
 1. \<And>b ba. \<lbrakk>(x, DeleteDerived, y) \<in> cdl_state_objs_to_policy (transform s); a = DeleteDerived; cdl_cdt (transform s) (y, b) = Some (x, ba); invs s; valid_list s; valid_sched s; \<exists>ptr' ptr. (y, b) = transform_cslot_ptr ptr' \<and> (x, ba) = transform_cslot_ptr ptr \<and> cdt s ptr' = Some ptr\<rbrakk> \<Longrightarrow> (x, DeleteDerived, y) \<in> state_objs_to_policy s proof (prove)
goal (1 subgoal):
 1. \<And>bb bc. \<lbrakk>(x, DeleteDerived, y) \<in> cdl_state_objs_to_policy (transform s); a = DeleteDerived; cdl_cdt (transform s) (y, nat (bl_to_bin bb)) = Some (x, nat (bl_to_bin bc)); invs s; valid_list s; valid_sched s; cdt s (y, bb) = Some (x, bc)\<rbrakk> \<Longrightarrow> (x, DeleteDerived, y) \<in> state_objs_to_policy s proof (prove)
goal:
No subgoals!