theory Dpolicy

lemma state_objs_transform:
  "\<lbrakk> einvs s; (x, a, y) \<in> state_objs_to_policy s \<rbrakk> \<Longrightarrow>
               (x, a, y) \<in> cdl_state_objs_to_policy (transform s)" apply (erule state_objs_to_policy_cases) apply (simp add:fst_transform_cslot_ptr) apply (rule_tac ptr="transform_cslot_ptr ptr" and auth=auth and oref=oref and
                      cap="transform_cap cap" and s="transform s" in csta_caps) apply (rule caps_of_state_transform_opt_cap) apply simp apply fastforce apply (simp add:idle_thread_no_authority) apply (case_tac cap; simp) apply (rename_tac arch_cap) apply (case_tac arch_cap; simp) apply (simp add:cap_auth_conferred_transform) apply (simp add:fst_transform_cslot_ptr) apply (rule_tac ptr="transform_cslot_ptr ptr" and auth=Control and oref=oref and
                      cap="transform_cap cap" and s="transform s" in csta_caps) apply (rule caps_of_state_transform_opt_cap) apply simp apply fastforce apply (simp add:idle_thread_no_untyped_range) apply (case_tac cap, (simp add:untyped_range_transform del:untyped_range.simps(1))+) apply (case_tac cap, (simp add:cdl_cap_auth_conferred_def)+) apply (rule thread_st_auth_transform, simp+) apply (rule thread_bound_ntfns_transform, simp+) apply (simp add:fst_transform_cslot_ptr) apply (rule_tac slot="transform_cslot_ptr slot" and slot'="transform_cslot_ptr slot'"
                    and s="transform s" in csta_cdt) apply (simp add:transform_def) apply (rule transform_cdt_some) apply (simp add:invs_mdb_cte) apply simp apply (fastforce intro: cdl_transferable_implies_transferable) apply (clarsimp split: prod.splits) subgoal for slot pslot apply (rule cdl_state_objs_to_policy_intros(3)
                   [where slot'="(y, nat (bl_to_bin slot))" and slot="(x, nat (bl_to_bin pslot))",
                    simplified]) apply (frule transform_cdt_slot_inj_on_mdb_cte_at[OF invs_mdb_cte]) apply (clarsimp simp: cdt_transform map_lift_over_def transform_cslot_ptr_def) apply safe apply (rule_tac x=pslot in exI) apply (subst inv_into_f_eq[where x="(y, slot)"]) apply (fastforce simp: inj_on_def) apply blast apply simp apply blast apply blast done apply (subgoal_tac "ptr \<noteq> idle_thread s") apply (simp add:state_vrefs_transform) apply (clarsimp simp:state_vrefs_def vs_refs_no_global_pts_def invs_def valid_state_def
                       valid_idle_def pred_tcb_at_def obj_at_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>einvs s; (x, a, y) \<in> state_objs_to_policy s\<rbrakk> \<Longrightarrow> (x, a, y) \<in> cdl_state_objs_to_policy (transform s) proof (prove)
goal (7 subgoals):
 1. \<And>ptr cap oref auth. \<lbrakk>einvs s; x = fst ptr; a = auth; y = oref; caps_of_state s ptr = Some cap; oref \<in> obj_refs_ac cap; auth \<in> cap_auth_conferred cap\<rbrakk> \<Longrightarrow> (x, a, y) \<in> cdl_state_objs_to_policy (transform s)
 2. \<And>ptr cap oref. \<lbrakk>einvs s; x = fst ptr; a = Control; y = oref; caps_of_state s ptr = Some cap; oref \<in> untyped_range cap\<rbrakk> \<Longrightarrow> (x, a, y) \<in> cdl_state_objs_to_policy (transform s)
 3. \<And>oref' auth oref. \<lbrakk>einvs s; x = oref; a = auth; y = oref'; (oref', auth) \<in> thread_st_auth s oref\<rbrakk> \<Longrightarrow> (x, a, y) \<in> cdl_state_objs_to_policy (transform s)
 4. \<And>oref oref' auth. \<lbrakk>einvs s; x = oref; a = auth; y = oref'; thread_bound_ntfns s oref = Some oref'; auth \<in> {Receive, Reset}\<rbrakk> \<Longrightarrow> (x, a, y) \<in> cdl_state_objs_to_policy (transform s)
 5. \<And>slot' slot. \<lbrakk>einvs s; x = fst slot; a = Control; y = fst slot'; cdt s slot' = Some slot; \<not> is_transferable_in slot' s\<rbrakk> \<Longrightarrow> (x, a, y) \<in> cdl_state_objs_to_policy (transform s)
 6. \<And>slot' slot. \<lbrakk>einvs s; x = fst slot; a = DeleteDerived; y = fst slot'; cdt s slot' = Some slot\<rbrakk> \<Longrightarrow> (x, a, y) \<in> cdl_state_objs_to_policy (transform s)
 7. \<And>ptr' uu_ uv_ auth ptr. \<lbrakk>einvs s; x = ptr; a = auth; y = ptr'; (ptr', uu_, uv_, auth) \<in> state_vrefs s ptr\<rbrakk> \<Longrightarrow> (x, a, y) \<in> cdl_state_objs_to_policy (transform s) proof (prove)
goal (7 subgoals):
 1. \<And>ptr cap oref auth. \<lbrakk>invs s \<and> valid_list s \<and> valid_sched s; x = fst (transform_cslot_ptr ptr); a = auth; y = oref; caps_of_state s ptr = Some cap; oref \<in> obj_refs_ac cap; auth \<in> cap_auth_conferred cap\<rbrakk> \<Longrightarrow> (fst (transform_cslot_ptr ptr), auth, oref) \<in> cdl_state_objs_to_policy (transform s)
 2. \<And>ptr cap oref. \<lbrakk>einvs s; x = fst ptr; a = Control; y = oref; caps_of_state s ptr = Some cap; oref \<in> untyped_range cap\<rbrakk> \<Longrightarrow> (x, a, y) \<in> cdl_state_objs_to_policy (transform s)
 3. \<And>oref' auth oref. \<lbrakk>einvs s; x = oref; a = auth; y = oref'; (oref', auth) \<in> thread_st_auth s oref\<rbrakk> \<Longrightarrow> (x, a, y) \<in> cdl_state_objs_to_policy (transform s)
 4. \<And>oref oref' auth. \<lbrakk>einvs s; x = oref; a = auth; y = oref'; thread_bound_ntfns s oref = Some oref'; auth \<in> {Receive, Reset}\<rbrakk> \<Longrightarrow> (x, a, y) \<in> cdl_state_objs_to_policy (transform s)
 5. \<And>slot' slot. \<lbrakk>einvs s; x = fst slot; a = Control; y = fst slot'; cdt s slot' = Some slot; \<not> is_transferable_in slot' s\<rbrakk> \<Longrightarrow> (x, a, y) \<in> cdl_state_objs_to_policy (transform s)
 6. \<And>slot' slot. \<lbrakk>einvs s; x = fst slot; a = DeleteDerived; y = fst slot'; cdt s slot' = Some slot\<rbrakk> \<Longrightarrow> (x, a, y) \<in> cdl_state_objs_to_policy (transform s)
 7. \<And>ptr' uu_ uv_ auth ptr. \<lbrakk>einvs s; x = ptr; a = auth; y = ptr'; (ptr', uu_, uv_, auth) \<in> state_vrefs s ptr\<rbrakk> \<Longrightarrow> (x, a, y) \<in> cdl_state_objs_to_policy (transform s) proof (prove)
goal (9 subgoals):
 1. \<And>ptr cap oref auth. \<lbrakk>invs s \<and> valid_list s \<and> valid_sched s; x = fst (transform_cslot_ptr ptr); a = auth; y = oref; caps_of_state s ptr = Some cap; oref \<in> obj_refs_ac cap; auth \<in> cap_auth_conferred cap\<rbrakk> \<Longrightarrow> opt_cap (transform_cslot_ptr ptr) (transform s) = Some (transform_cap cap)
 2. \<And>ptr cap oref auth. \<lbrakk>invs s \<and> valid_list s \<and> valid_sched s; x = fst (transform_cslot_ptr ptr); a = auth; y = oref; caps_of_state s ptr = Some cap; oref \<in> obj_refs_ac cap; auth \<in> cap_auth_conferred cap\<rbrakk> \<Longrightarrow> oref \<in> cdl_obj_refs (transform_cap cap)
 3. \<And>ptr cap oref auth. \<lbrakk>invs s \<and> valid_list s \<and> valid_sched s; x = fst (transform_cslot_ptr ptr); a = auth; y = oref; caps_of_state s ptr = Some cap; oref \<in> obj_refs_ac cap; auth \<in> cap_auth_conferred cap\<rbrakk> \<Longrightarrow> auth \<in> cdl_cap_auth_conferred (transform_cap cap)
 4. \<And>ptr cap oref. \<lbrakk>einvs s; x = fst ptr; a = Control; y = oref; caps_of_state s ptr = Some cap; oref \<in> untyped_range cap\<rbrakk> \<Longrightarrow> (x, a, y) \<in> cdl_state_objs_to_policy (transform s)
 5. \<And>oref' auth oref. \<lbrakk>einvs s; x = oref; a = auth; y = oref'; (oref', auth) \<in> thread_st_auth s oref\<rbrakk> \<Longrightarrow> (x, a, y) \<in> cdl_state_objs_to_policy (transform s)
 6. \<And>oref oref' auth. \<lbrakk>einvs s; x = oref; a = auth; y = oref'; thread_bound_ntfns s oref = Some oref'; auth \<in> {Receive, Reset}\<rbrakk> \<Longrightarrow> (x, a, y) \<in> cdl_state_objs_to_policy (transform s)
 7. \<And>slot' slot. \<lbrakk>einvs s; x = fst slot; a = Control; y = fst slot'; cdt s slot' = Some slot; \<not> is_transferable_in slot' s\<rbrakk> \<Longrightarrow> (x, a, y) \<in> cdl_state_objs_to_policy (transform s)
 8. \<And>slot' slot. \<lbrakk>einvs s; x = fst slot; a = DeleteDerived; y = fst slot'; cdt s slot' = Some slot\<rbrakk> \<Longrightarrow> (x, a, y) \<in> cdl_state_objs_to_policy (transform s)
 9. \<And>ptr' uu_ uv_ auth ptr. \<lbrakk>einvs s; x = ptr; a = auth; y = ptr'; (ptr', uu_, uv_, auth) \<in> state_vrefs s ptr\<rbrakk> \<Longrightarrow> (x, a, y) \<in> cdl_state_objs_to_policy (transform s) proof (prove)
goal (11 subgoals):
 1. \<And>ptr cap oref auth. \<lbrakk>invs s \<and> valid_list s \<and> valid_sched s; x = fst (transform_cslot_ptr ptr); a = auth; y = oref; caps_of_state s ptr = Some cap; oref \<in> obj_refs_ac cap; auth \<in> cap_auth_conferred cap\<rbrakk> \<Longrightarrow> caps_of_state s ptr = Some cap
 2. \<And>ptr cap oref auth. \<lbrakk>invs s \<and> valid_list s \<and> valid_sched s; x = fst (transform_cslot_ptr ptr); a = auth; y = oref; caps_of_state s ptr = Some cap; oref \<in> obj_refs_ac cap; auth \<in> cap_auth_conferred cap\<rbrakk> \<Longrightarrow> valid_etcbs s
 3. \<And>ptr cap oref auth. \<lbrakk>invs s \<and> valid_list s \<and> valid_sched s; x = fst (transform_cslot_ptr ptr); a = auth; y = oref; caps_of_state s ptr = Some cap; oref \<in> obj_refs_ac cap; auth \<in> cap_auth_conferred cap\<rbrakk> \<Longrightarrow> fst ptr \<noteq> idle_thread s
 4. \<And>ptr cap oref auth. \<lbrakk>invs s \<and> valid_list s \<and> valid_sched s; x = fst (transform_cslot_ptr ptr); a = auth; y = oref; caps_of_state s ptr = Some cap; oref \<in> obj_refs_ac cap; auth \<in> cap_auth_conferred cap\<rbrakk> \<Longrightarrow> oref \<in> cdl_obj_refs (transform_cap cap)
 5. \<And>ptr cap oref auth. \<lbrakk>invs s \<and> valid_list s \<and> valid_sched s; x = fst (transform_cslot_ptr ptr); a = auth; y = oref; caps_of_state s ptr = Some cap; oref \<in> obj_refs_ac cap; auth \<in> cap_auth_conferred cap\<rbrakk> \<Longrightarrow> auth \<in> cdl_cap_auth_conferred (transform_cap cap)
 6. \<And>ptr cap oref. \<lbrakk>einvs s; x = fst ptr; a = Control; y = oref; caps_of_state s ptr = Some cap; oref \<in> untyped_range cap\<rbrakk> \<Longrightarrow> (x, a, y) \<in> cdl_state_objs_to_policy (transform s)
 7. \<And>oref' auth oref. \<lbrakk>einvs s; x = oref; a = auth; y = oref'; (oref', auth) \<in> thread_st_auth s oref\<rbrakk> \<Longrightarrow> (x, a, y) \<in> cdl_state_objs_to_policy (transform s)
 8. \<And>oref oref' auth. \<lbrakk>einvs s; x = oref; a = auth; y = oref'; thread_bound_ntfns s oref = Some oref'; auth \<in> {Receive, Reset}\<rbrakk> \<Longrightarrow> (x, a, y) \<in> cdl_state_objs_to_policy (transform s)
 9. \<And>slot' slot. \<lbrakk>einvs s; x = fst slot; a = Control; y = fst slot'; cdt s slot' = Some slot; \<not> is_transferable_in slot' s\<rbrakk> \<Longrightarrow> (x, a, y) \<in> cdl_state_objs_to_policy (transform s)
 10. \<And>slot' slot. \<lbrakk>einvs s; x = fst slot; a = DeleteDerived; y = fst slot'; cdt s slot' = Some slot\<rbrakk> \<Longrightarrow> (x, a, y) \<in> cdl_state_objs_to_policy (transform s)
A total of 11 subgoals... proof (prove)
goal (10 subgoals):
 1. \<And>ptr cap oref auth. \<lbrakk>invs s \<and> valid_list s \<and> valid_sched s; x = fst (transform_cslot_ptr ptr); a = auth; y = oref; caps_of_state s ptr = Some cap; oref \<in> obj_refs_ac cap; auth \<in> cap_auth_conferred cap\<rbrakk> \<Longrightarrow> valid_etcbs s
 2. \<And>ptr cap oref auth. \<lbrakk>invs s \<and> valid_list s \<and> valid_sched s; x = fst (transform_cslot_ptr ptr); a = auth; y = oref; caps_of_state s ptr = Some cap; oref \<in> obj_refs_ac cap; auth \<in> cap_auth_conferred cap\<rbrakk> \<Longrightarrow> fst ptr \<noteq> idle_thread s
 3. \<And>ptr cap oref auth. \<lbrakk>invs s \<and> valid_list s \<and> valid_sched s; x = fst (transform_cslot_ptr ptr); a = auth; y = oref; caps_of_state s ptr = Some cap; oref \<in> obj_refs_ac cap; auth \<in> cap_auth_conferred cap\<rbrakk> \<Longrightarrow> oref \<in> cdl_obj_refs (transform_cap cap)
 4. \<And>ptr cap oref auth. \<lbrakk>invs s \<and> valid_list s \<and> valid_sched s; x = fst (transform_cslot_ptr ptr); a = auth; y = oref; caps_of_state s ptr = Some cap; oref \<in> obj_refs_ac cap; auth \<in> cap_auth_conferred cap\<rbrakk> \<Longrightarrow> auth \<in> cdl_cap_auth_conferred (transform_cap cap)
 5. \<And>ptr cap oref. \<lbrakk>einvs s; x = fst ptr; a = Control; y = oref; caps_of_state s ptr = Some cap; oref \<in> untyped_range cap\<rbrakk> \<Longrightarrow> (x, a, y) \<in> cdl_state_objs_to_policy (transform s)
 6. \<And>oref' auth oref. \<lbrakk>einvs s; x = oref; a = auth; y = oref'; (oref', auth) \<in> thread_st_auth s oref\<rbrakk> \<Longrightarrow> (x, a, y) \<in> cdl_state_objs_to_policy (transform s)
 7. \<And>oref oref' auth. \<lbrakk>einvs s; x = oref; a = auth; y = oref'; thread_bound_ntfns s oref = Some oref'; auth \<in> {Receive, Reset}\<rbrakk> \<Longrightarrow> (x, a, y) \<in> cdl_state_objs_to_policy (transform s)
 8. \<And>slot' slot. \<lbrakk>einvs s; x = fst slot; a = Control; y = fst slot'; cdt s slot' = Some slot; \<not> is_transferable_in slot' s\<rbrakk> \<Longrightarrow> (x, a, y) \<in> cdl_state_objs_to_policy (transform s)
 9. \<And>slot' slot. \<lbrakk>einvs s; x = fst slot; a = DeleteDerived; y = fst slot'; cdt s slot' = Some slot\<rbrakk> \<Longrightarrow> (x, a, y) \<in> cdl_state_objs_to_policy (transform s)
 10. \<And>ptr' uu_ uv_ auth ptr. \<lbrakk>einvs s; x = ptr; a = auth; y = ptr'; (ptr', uu_, uv_, auth) \<in> state_vrefs s ptr\<rbrakk> \<Longrightarrow> (x, a, y) \<in> cdl_state_objs_to_policy (transform s) proof (prove)
goal (9 subgoals):
 1. \<And>ptr cap oref auth. \<lbrakk>invs s \<and> valid_list s \<and> valid_sched s; x = fst (transform_cslot_ptr ptr); a = auth; y = oref; caps_of_state s ptr = Some cap; oref \<in> obj_refs_ac cap; auth \<in> cap_auth_conferred 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; x = fst (transform_cslot_ptr ptr); a = auth; y = oref; caps_of_state s ptr = Some cap; oref \<in> obj_refs_ac cap; auth \<in> cap_auth_conferred cap\<rbrakk> \<Longrightarrow> oref \<in> cdl_obj_refs (transform_cap cap)
 3. \<And>ptr cap oref auth. \<lbrakk>invs s \<and> valid_list s \<and> valid_sched s; x = fst (transform_cslot_ptr ptr); a = auth; y = oref; caps_of_state s ptr = Some cap; oref \<in> obj_refs_ac cap; auth \<in> cap_auth_conferred cap\<rbrakk> \<Longrightarrow> auth \<in> cdl_cap_auth_conferred (transform_cap cap)
 4. \<And>ptr cap oref. \<lbrakk>einvs s; x = fst ptr; a = Control; y = oref; caps_of_state s ptr = Some cap; oref \<in> untyped_range cap\<rbrakk> \<Longrightarrow> (x, a, y) \<in> cdl_state_objs_to_policy (transform s)
 5. \<And>oref' auth oref. \<lbrakk>einvs s; x = oref; a = auth; y = oref'; (oref', auth) \<in> thread_st_auth s oref\<rbrakk> \<Longrightarrow> (x, a, y) \<in> cdl_state_objs_to_policy (transform s)
 6. \<And>oref oref' auth. \<lbrakk>einvs s; x = oref; a = auth; y = oref'; thread_bound_ntfns s oref = Some oref'; auth \<in> {Receive, Reset}\<rbrakk> \<Longrightarrow> (x, a, y) \<in> cdl_state_objs_to_policy (transform s)
 7. \<And>slot' slot. \<lbrakk>einvs s; x = fst slot; a = Control; y = fst slot'; cdt s slot' = Some slot; \<not> is_transferable_in slot' s\<rbrakk> \<Longrightarrow> (x, a, y) \<in> cdl_state_objs_to_policy (transform s)
 8. \<And>slot' slot. \<lbrakk>einvs s; x = fst slot; a = DeleteDerived; y = fst slot'; cdt s slot' = Some slot\<rbrakk> \<Longrightarrow> (x, a, y) \<in> cdl_state_objs_to_policy (transform s)
 9. \<And>ptr' uu_ uv_ auth ptr. \<lbrakk>einvs s; x = ptr; a = auth; y = ptr'; (ptr', uu_, uv_, auth) \<in> state_vrefs s ptr\<rbrakk> \<Longrightarrow> (x, a, y) \<in> cdl_state_objs_to_policy (transform s) proof (prove)
goal (8 subgoals):
 1. \<And>ptr cap oref auth. \<lbrakk>invs s \<and> valid_list s \<and> valid_sched s; x = fst (transform_cslot_ptr ptr); a = auth; y = oref; caps_of_state s ptr = Some cap; oref \<in> obj_refs_ac cap; auth \<in> cap_auth_conferred cap\<rbrakk> \<Longrightarrow> oref \<in> cdl_obj_refs (transform_cap cap)
 2. \<And>ptr cap oref auth. \<lbrakk>invs s \<and> valid_list s \<and> valid_sched s; x = fst (transform_cslot_ptr ptr); a = auth; y = oref; caps_of_state s ptr = Some cap; oref \<in> obj_refs_ac cap; auth \<in> cap_auth_conferred cap\<rbrakk> \<Longrightarrow> auth \<in> cdl_cap_auth_conferred (transform_cap cap)
 3. \<And>ptr cap oref. \<lbrakk>einvs s; x = fst ptr; a = Control; y = oref; caps_of_state s ptr = Some cap; oref \<in> untyped_range cap\<rbrakk> \<Longrightarrow> (x, a, y) \<in> cdl_state_objs_to_policy (transform s)
 4. \<And>oref' auth oref. \<lbrakk>einvs s; x = oref; a = auth; y = oref'; (oref', auth) \<in> thread_st_auth s oref\<rbrakk> \<Longrightarrow> (x, a, y) \<in> cdl_state_objs_to_policy (transform s)
 5. \<And>oref oref' auth. \<lbrakk>einvs s; x = oref; a = auth; y = oref'; thread_bound_ntfns s oref = Some oref'; auth \<in> {Receive, Reset}\<rbrakk> \<Longrightarrow> (x, a, y) \<in> cdl_state_objs_to_policy (transform s)
 6. \<And>slot' slot. \<lbrakk>einvs s; x = fst slot; a = Control; y = fst slot'; cdt s slot' = Some slot; \<not> is_transferable_in slot' s\<rbrakk> \<Longrightarrow> (x, a, y) \<in> cdl_state_objs_to_policy (transform s)
 7. \<And>slot' slot. \<lbrakk>einvs s; x = fst slot; a = DeleteDerived; y = fst slot'; cdt s slot' = Some slot\<rbrakk> \<Longrightarrow> (x, a, y) \<in> cdl_state_objs_to_policy (transform s)
 8. \<And>ptr' uu_ uv_ auth ptr. \<lbrakk>einvs s; x = ptr; a = auth; y = ptr'; (ptr', uu_, uv_, auth) \<in> state_vrefs s ptr\<rbrakk> \<Longrightarrow> (x, a, y) \<in> cdl_state_objs_to_policy (transform s) proof (prove)
goal (8 subgoals):
 1. \<And>ptr cap oref auth x12. \<lbrakk>invs s \<and> valid_list s \<and> valid_sched s; x = fst (transform_cslot_ptr ptr); a = auth; y = oref; caps_of_state s ptr = Some (ArchObjectCap x12); oref \<in> aobj_ref' x12; auth \<in> cap_auth_conferred (ArchObjectCap x12); cap = ArchObjectCap x12\<rbrakk> \<Longrightarrow> oref \<in> cdl_obj_refs (transform_cap (ArchObjectCap x12))
 2. \<And>ptr cap oref auth. \<lbrakk>invs s \<and> valid_list s \<and> valid_sched s; x = fst (transform_cslot_ptr ptr); a = auth; y = oref; caps_of_state s ptr = Some cap; oref \<in> obj_refs_ac cap; auth \<in> cap_auth_conferred cap\<rbrakk> \<Longrightarrow> auth \<in> cdl_cap_auth_conferred (transform_cap cap)
 3. \<And>ptr cap oref. \<lbrakk>einvs s; x = fst ptr; a = Control; y = oref; caps_of_state s ptr = Some cap; oref \<in> untyped_range cap\<rbrakk> \<Longrightarrow> (x, a, y) \<in> cdl_state_objs_to_policy (transform s)
 4. \<And>oref' auth oref. \<lbrakk>einvs s; x = oref; a = auth; y = oref'; (oref', auth) \<in> thread_st_auth s oref\<rbrakk> \<Longrightarrow> (x, a, y) \<in> cdl_state_objs_to_policy (transform s)
 5. \<And>oref oref' auth. \<lbrakk>einvs s; x = oref; a = auth; y = oref'; thread_bound_ntfns s oref = Some oref'; auth \<in> {Receive, Reset}\<rbrakk> \<Longrightarrow> (x, a, y) \<in> cdl_state_objs_to_policy (transform s)
 6. \<And>slot' slot. \<lbrakk>einvs s; x = fst slot; a = Control; y = fst slot'; cdt s slot' = Some slot; \<not> is_transferable_in slot' s\<rbrakk> \<Longrightarrow> (x, a, y) \<in> cdl_state_objs_to_policy (transform s)
 7. \<And>slot' slot. \<lbrakk>einvs s; x = fst slot; a = DeleteDerived; y = fst slot'; cdt s slot' = Some slot\<rbrakk> \<Longrightarrow> (x, a, y) \<in> cdl_state_objs_to_policy (transform s)
 8. \<And>ptr' uu_ uv_ auth ptr. \<lbrakk>einvs s; x = ptr; a = auth; y = ptr'; (ptr', uu_, uv_, auth) \<in> state_vrefs s ptr\<rbrakk> \<Longrightarrow> (x, a, y) \<in> cdl_state_objs_to_policy (transform s) proof (prove)
goal (8 subgoals):
 1. \<And>ptr cap oref auth arch_cap. \<lbrakk>invs s \<and> valid_list s \<and> valid_sched s; x = fst (transform_cslot_ptr ptr); a = auth; y = oref; caps_of_state s ptr = Some (ArchObjectCap arch_cap); oref \<in> aobj_ref' arch_cap; auth \<in> cap_auth_conferred (ArchObjectCap arch_cap); cap = ArchObjectCap arch_cap\<rbrakk> \<Longrightarrow> oref \<in> cdl_obj_refs (transform_cap (ArchObjectCap arch_cap))
 2. \<And>ptr cap oref auth. \<lbrakk>invs s \<and> valid_list s \<and> valid_sched s; x = fst (transform_cslot_ptr ptr); a = auth; y = oref; caps_of_state s ptr = Some cap; oref \<in> obj_refs_ac cap; auth \<in> cap_auth_conferred cap\<rbrakk> \<Longrightarrow> auth \<in> cdl_cap_auth_conferred (transform_cap cap)
 3. \<And>ptr cap oref. \<lbrakk>einvs s; x = fst ptr; a = Control; y = oref; caps_of_state s ptr = Some cap; oref \<in> untyped_range cap\<rbrakk> \<Longrightarrow> (x, a, y) \<in> cdl_state_objs_to_policy (transform s)
 4. \<And>oref' auth oref. \<lbrakk>einvs s; x = oref; a = auth; y = oref'; (oref', auth) \<in> thread_st_auth s oref\<rbrakk> \<Longrightarrow> (x, a, y) \<in> cdl_state_objs_to_policy (transform s)
 5. \<And>oref oref' auth. \<lbrakk>einvs s; x = oref; a = auth; y = oref'; thread_bound_ntfns s oref = Some oref'; auth \<in> {Receive, Reset}\<rbrakk> \<Longrightarrow> (x, a, y) \<in> cdl_state_objs_to_policy (transform s)
 6. \<And>slot' slot. \<lbrakk>einvs s; x = fst slot; a = Control; y = fst slot'; cdt s slot' = Some slot; \<not> is_transferable_in slot' s\<rbrakk> \<Longrightarrow> (x, a, y) \<in> cdl_state_objs_to_policy (transform s)
 7. \<And>slot' slot. \<lbrakk>einvs s; x = fst slot; a = DeleteDerived; y = fst slot'; cdt s slot' = Some slot\<rbrakk> \<Longrightarrow> (x, a, y) \<in> cdl_state_objs_to_policy (transform s)
 8. \<And>ptr' uu_ uv_ auth ptr. \<lbrakk>einvs s; x = ptr; a = auth; y = ptr'; (ptr', uu_, uv_, auth) \<in> state_vrefs s ptr\<rbrakk> \<Longrightarrow> (x, a, y) \<in> cdl_state_objs_to_policy (transform s) proof (prove)
goal (7 subgoals):
 1. \<And>ptr cap oref auth. \<lbrakk>invs s \<and> valid_list s \<and> valid_sched s; x = fst (transform_cslot_ptr ptr); a = auth; y = oref; caps_of_state s ptr = Some cap; oref \<in> obj_refs_ac cap; auth \<in> cap_auth_conferred cap\<rbrakk> \<Longrightarrow> auth \<in> cdl_cap_auth_conferred (transform_cap cap)
 2. \<And>ptr cap oref. \<lbrakk>einvs s; x = fst ptr; a = Control; y = oref; caps_of_state s ptr = Some cap; oref \<in> untyped_range cap\<rbrakk> \<Longrightarrow> (x, a, y) \<in> cdl_state_objs_to_policy (transform s)
 3. \<And>oref' auth oref. \<lbrakk>einvs s; x = oref; a = auth; y = oref'; (oref', auth) \<in> thread_st_auth s oref\<rbrakk> \<Longrightarrow> (x, a, y) \<in> cdl_state_objs_to_policy (transform s)
 4. \<And>oref oref' auth. \<lbrakk>einvs s; x = oref; a = auth; y = oref'; thread_bound_ntfns s oref = Some oref'; auth \<in> {Receive, Reset}\<rbrakk> \<Longrightarrow> (x, a, y) \<in> cdl_state_objs_to_policy (transform s)
 5. \<And>slot' slot. \<lbrakk>einvs s; x = fst slot; a = Control; y = fst slot'; cdt s slot' = Some slot; \<not> is_transferable_in slot' s\<rbrakk> \<Longrightarrow> (x, a, y) \<in> cdl_state_objs_to_policy (transform s)
 6. \<And>slot' slot. \<lbrakk>einvs s; x = fst slot; a = DeleteDerived; y = fst slot'; cdt s slot' = Some slot\<rbrakk> \<Longrightarrow> (x, a, y) \<in> cdl_state_objs_to_policy (transform s)
 7. \<And>ptr' uu_ uv_ auth ptr. \<lbrakk>einvs s; x = ptr; a = auth; y = ptr'; (ptr', uu_, uv_, auth) \<in> state_vrefs s ptr\<rbrakk> \<Longrightarrow> (x, a, y) \<in> cdl_state_objs_to_policy (transform s) proof (prove)
goal (6 subgoals):
 1. \<And>ptr cap oref. \<lbrakk>einvs s; x = fst ptr; a = Control; y = oref; caps_of_state s ptr = Some cap; oref \<in> untyped_range cap\<rbrakk> \<Longrightarrow> (x, a, y) \<in> cdl_state_objs_to_policy (transform s)
 2. \<And>oref' auth oref. \<lbrakk>einvs s; x = oref; a = auth; y = oref'; (oref', auth) \<in> thread_st_auth s oref\<rbrakk> \<Longrightarrow> (x, a, y) \<in> cdl_state_objs_to_policy (transform s)
 3. \<And>oref oref' auth. \<lbrakk>einvs s; x = oref; a = auth; y = oref'; thread_bound_ntfns s oref = Some oref'; auth \<in> {Receive, Reset}\<rbrakk> \<Longrightarrow> (x, a, y) \<in> cdl_state_objs_to_policy (transform s)
 4. \<And>slot' slot. \<lbrakk>einvs s; x = fst slot; a = Control; y = fst slot'; cdt s slot' = Some slot; \<not> is_transferable_in slot' s\<rbrakk> \<Longrightarrow> (x, a, y) \<in> cdl_state_objs_to_policy (transform s)
 5. \<And>slot' slot. \<lbrakk>einvs s; x = fst slot; a = DeleteDerived; y = fst slot'; cdt s slot' = Some slot\<rbrakk> \<Longrightarrow> (x, a, y) \<in> cdl_state_objs_to_policy (transform s)
 6. \<And>ptr' uu_ uv_ auth ptr. \<lbrakk>einvs s; x = ptr; a = auth; y = ptr'; (ptr', uu_, uv_, auth) \<in> state_vrefs s ptr\<rbrakk> \<Longrightarrow> (x, a, y) \<in> cdl_state_objs_to_policy (transform s) proof (prove)
goal (6 subgoals):
 1. \<And>ptr cap oref. \<lbrakk>invs s \<and> valid_list s \<and> valid_sched s; x = fst (transform_cslot_ptr ptr); a = Control; y = oref; caps_of_state s ptr = Some cap; oref \<in> untyped_range cap\<rbrakk> \<Longrightarrow> (fst (transform_cslot_ptr ptr), Control, oref) \<in> cdl_state_objs_to_policy (transform s)
 2. \<And>oref' auth oref. \<lbrakk>einvs s; x = oref; a = auth; y = oref'; (oref', auth) \<in> thread_st_auth s oref\<rbrakk> \<Longrightarrow> (x, a, y) \<in> cdl_state_objs_to_policy (transform s)
 3. \<And>oref oref' auth. \<lbrakk>einvs s; x = oref; a = auth; y = oref'; thread_bound_ntfns s oref = Some oref'; auth \<in> {Receive, Reset}\<rbrakk> \<Longrightarrow> (x, a, y) \<in> cdl_state_objs_to_policy (transform s)
 4. \<And>slot' slot. \<lbrakk>einvs s; x = fst slot; a = Control; y = fst slot'; cdt s slot' = Some slot; \<not> is_transferable_in slot' s\<rbrakk> \<Longrightarrow> (x, a, y) \<in> cdl_state_objs_to_policy (transform s)
 5. \<And>slot' slot. \<lbrakk>einvs s; x = fst slot; a = DeleteDerived; y = fst slot'; cdt s slot' = Some slot\<rbrakk> \<Longrightarrow> (x, a, y) \<in> cdl_state_objs_to_policy (transform s)
 6. \<And>ptr' uu_ uv_ auth ptr. \<lbrakk>einvs s; x = ptr; a = auth; y = ptr'; (ptr', uu_, uv_, auth) \<in> state_vrefs s ptr\<rbrakk> \<Longrightarrow> (x, a, y) \<in> cdl_state_objs_to_policy (transform s) proof (prove)
goal (8 subgoals):
 1. \<And>ptr cap oref. \<lbrakk>invs s \<and> valid_list s \<and> valid_sched s; x = fst (transform_cslot_ptr ptr); a = Control; y = oref; caps_of_state s ptr = Some cap; oref \<in> untyped_range cap\<rbrakk> \<Longrightarrow> opt_cap (transform_cslot_ptr ptr) (transform s) = Some (transform_cap cap)
 2. \<And>ptr cap oref. \<lbrakk>invs s \<and> valid_list s \<and> valid_sched s; x = fst (transform_cslot_ptr ptr); a = Control; y = oref; caps_of_state s ptr = Some cap; oref \<in> untyped_range cap\<rbrakk> \<Longrightarrow> oref \<in> cdl_obj_refs (transform_cap cap)
 3. \<And>ptr cap oref. \<lbrakk>invs s \<and> valid_list s \<and> valid_sched s; x = fst (transform_cslot_ptr ptr); a = Control; y = oref; caps_of_state s ptr = Some cap; oref \<in> untyped_range cap\<rbrakk> \<Longrightarrow> Control \<in> cdl_cap_auth_conferred (transform_cap cap)
 4. \<And>oref' auth oref. \<lbrakk>einvs s; x = oref; a = auth; y = oref'; (oref', auth) \<in> thread_st_auth s oref\<rbrakk> \<Longrightarrow> (x, a, y) \<in> cdl_state_objs_to_policy (transform s)
 5. \<And>oref oref' auth. \<lbrakk>einvs s; x = oref; a = auth; y = oref'; thread_bound_ntfns s oref = Some oref'; auth \<in> {Receive, Reset}\<rbrakk> \<Longrightarrow> (x, a, y) \<in> cdl_state_objs_to_policy (transform s)
 6. \<And>slot' slot. \<lbrakk>einvs s; x = fst slot; a = Control; y = fst slot'; cdt s slot' = Some slot; \<not> is_transferable_in slot' s\<rbrakk> \<Longrightarrow> (x, a, y) \<in> cdl_state_objs_to_policy (transform s)
 7. \<And>slot' slot. \<lbrakk>einvs s; x = fst slot; a = DeleteDerived; y = fst slot'; cdt s slot' = Some slot\<rbrakk> \<Longrightarrow> (x, a, y) \<in> cdl_state_objs_to_policy (transform s)
 8. \<And>ptr' uu_ uv_ auth ptr. \<lbrakk>einvs s; x = ptr; a = auth; y = ptr'; (ptr', uu_, uv_, auth) \<in> state_vrefs s ptr\<rbrakk> \<Longrightarrow> (x, a, y) \<in> cdl_state_objs_to_policy (transform s) proof (prove)
goal (10 subgoals):
 1. \<And>ptr cap oref. \<lbrakk>invs s \<and> valid_list s \<and> valid_sched s; x = fst (transform_cslot_ptr ptr); a = Control; y = oref; caps_of_state s ptr = Some cap; oref \<in> untyped_range cap\<rbrakk> \<Longrightarrow> caps_of_state s ptr = Some cap
 2. \<And>ptr cap oref. \<lbrakk>invs s \<and> valid_list s \<and> valid_sched s; x = fst (transform_cslot_ptr ptr); a = Control; y = oref; caps_of_state s ptr = Some cap; oref \<in> untyped_range cap\<rbrakk> \<Longrightarrow> valid_etcbs s
 3. \<And>ptr cap oref. \<lbrakk>invs s \<and> valid_list s \<and> valid_sched s; x = fst (transform_cslot_ptr ptr); a = Control; y = oref; caps_of_state s ptr = Some cap; oref \<in> untyped_range cap\<rbrakk> \<Longrightarrow> fst ptr \<noteq> idle_thread s
 4. \<And>ptr cap oref. \<lbrakk>invs s \<and> valid_list s \<and> valid_sched s; x = fst (transform_cslot_ptr ptr); a = Control; y = oref; caps_of_state s ptr = Some cap; oref \<in> untyped_range cap\<rbrakk> \<Longrightarrow> oref \<in> cdl_obj_refs (transform_cap cap)
 5. \<And>ptr cap oref. \<lbrakk>invs s \<and> valid_list s \<and> valid_sched s; x = fst (transform_cslot_ptr ptr); a = Control; y = oref; caps_of_state s ptr = Some cap; oref \<in> untyped_range cap\<rbrakk> \<Longrightarrow> Control \<in> cdl_cap_auth_conferred (transform_cap cap)
 6. \<And>oref' auth oref. \<lbrakk>einvs s; x = oref; a = auth; y = oref'; (oref', auth) \<in> thread_st_auth s oref\<rbrakk> \<Longrightarrow> (x, a, y) \<in> cdl_state_objs_to_policy (transform s)
 7. \<And>oref oref' auth. \<lbrakk>einvs s; x = oref; a = auth; y = oref'; thread_bound_ntfns s oref = Some oref'; auth \<in> {Receive, Reset}\<rbrakk> \<Longrightarrow> (x, a, y) \<in> cdl_state_objs_to_policy (transform s)
 8. \<And>slot' slot. \<lbrakk>einvs s; x = fst slot; a = Control; y = fst slot'; cdt s slot' = Some slot; \<not> is_transferable_in slot' s\<rbrakk> \<Longrightarrow> (x, a, y) \<in> cdl_state_objs_to_policy (transform s)
 9. \<And>slot' slot. \<lbrakk>einvs s; x = fst slot; a = DeleteDerived; y = fst slot'; cdt s slot' = Some slot\<rbrakk> \<Longrightarrow> (x, a, y) \<in> cdl_state_objs_to_policy (transform s)
 10. \<And>ptr' uu_ uv_ auth ptr. \<lbrakk>einvs s; x = ptr; a = auth; y = ptr'; (ptr', uu_, uv_, auth) \<in> state_vrefs s ptr\<rbrakk> \<Longrightarrow> (x, a, y) \<in> cdl_state_objs_to_policy (transform s) proof (prove)
goal (9 subgoals):
 1. \<And>ptr cap oref. \<lbrakk>invs s \<and> valid_list s \<and> valid_sched s; x = fst (transform_cslot_ptr ptr); a = Control; y = oref; caps_of_state s ptr = Some cap; oref \<in> untyped_range cap\<rbrakk> \<Longrightarrow> valid_etcbs s
 2. \<And>ptr cap oref. \<lbrakk>invs s \<and> valid_list s \<and> valid_sched s; x = fst (transform_cslot_ptr ptr); a = Control; y = oref; caps_of_state s ptr = Some cap; oref \<in> untyped_range cap\<rbrakk> \<Longrightarrow> fst ptr \<noteq> idle_thread s
 3. \<And>ptr cap oref. \<lbrakk>invs s \<and> valid_list s \<and> valid_sched s; x = fst (transform_cslot_ptr ptr); a = Control; y = oref; caps_of_state s ptr = Some cap; oref \<in> untyped_range cap\<rbrakk> \<Longrightarrow> oref \<in> cdl_obj_refs (transform_cap cap)
 4. \<And>ptr cap oref. \<lbrakk>invs s \<and> valid_list s \<and> valid_sched s; x = fst (transform_cslot_ptr ptr); a = Control; y = oref; caps_of_state s ptr = Some cap; oref \<in> untyped_range cap\<rbrakk> \<Longrightarrow> Control \<in> cdl_cap_auth_conferred (transform_cap cap)
 5. \<And>oref' auth oref. \<lbrakk>einvs s; x = oref; a = auth; y = oref'; (oref', auth) \<in> thread_st_auth s oref\<rbrakk> \<Longrightarrow> (x, a, y) \<in> cdl_state_objs_to_policy (transform s)
 6. \<And>oref oref' auth. \<lbrakk>einvs s; x = oref; a = auth; y = oref'; thread_bound_ntfns s oref = Some oref'; auth \<in> {Receive, Reset}\<rbrakk> \<Longrightarrow> (x, a, y) \<in> cdl_state_objs_to_policy (transform s)
 7. \<And>slot' slot. \<lbrakk>einvs s; x = fst slot; a = Control; y = fst slot'; cdt s slot' = Some slot; \<not> is_transferable_in slot' s\<rbrakk> \<Longrightarrow> (x, a, y) \<in> cdl_state_objs_to_policy (transform s)
 8. \<And>slot' slot. \<lbrakk>einvs s; x = fst slot; a = DeleteDerived; y = fst slot'; cdt s slot' = Some slot\<rbrakk> \<Longrightarrow> (x, a, y) \<in> cdl_state_objs_to_policy (transform s)
 9. \<And>ptr' uu_ uv_ auth ptr. \<lbrakk>einvs s; x = ptr; a = auth; y = ptr'; (ptr', uu_, uv_, auth) \<in> state_vrefs s ptr\<rbrakk> \<Longrightarrow> (x, a, y) \<in> cdl_state_objs_to_policy (transform s) proof (prove)
goal (8 subgoals):
 1. \<And>ptr cap oref. \<lbrakk>invs s \<and> valid_list s \<and> valid_sched s; x = fst (transform_cslot_ptr ptr); a = Control; y = oref; caps_of_state s ptr = Some cap; oref \<in> untyped_range cap\<rbrakk> \<Longrightarrow> fst ptr \<noteq> idle_thread s
 2. \<And>ptr cap oref. \<lbrakk>invs s \<and> valid_list s \<and> valid_sched s; x = fst (transform_cslot_ptr ptr); a = Control; y = oref; caps_of_state s ptr = Some cap; oref \<in> untyped_range cap\<rbrakk> \<Longrightarrow> oref \<in> cdl_obj_refs (transform_cap cap)
 3. \<And>ptr cap oref. \<lbrakk>invs s \<and> valid_list s \<and> valid_sched s; x = fst (transform_cslot_ptr ptr); a = Control; y = oref; caps_of_state s ptr = Some cap; oref \<in> untyped_range cap\<rbrakk> \<Longrightarrow> Control \<in> cdl_cap_auth_conferred (transform_cap cap)
 4. \<And>oref' auth oref. \<lbrakk>einvs s; x = oref; a = auth; y = oref'; (oref', auth) \<in> thread_st_auth s oref\<rbrakk> \<Longrightarrow> (x, a, y) \<in> cdl_state_objs_to_policy (transform s)
 5. \<And>oref oref' auth. \<lbrakk>einvs s; x = oref; a = auth; y = oref'; thread_bound_ntfns s oref = Some oref'; auth \<in> {Receive, Reset}\<rbrakk> \<Longrightarrow> (x, a, y) \<in> cdl_state_objs_to_policy (transform s)
 6. \<And>slot' slot. \<lbrakk>einvs s; x = fst slot; a = Control; y = fst slot'; cdt s slot' = Some slot; \<not> is_transferable_in slot' s\<rbrakk> \<Longrightarrow> (x, a, y) \<in> cdl_state_objs_to_policy (transform s)
 7. \<And>slot' slot. \<lbrakk>einvs s; x = fst slot; a = DeleteDerived; y = fst slot'; cdt s slot' = Some slot\<rbrakk> \<Longrightarrow> (x, a, y) \<in> cdl_state_objs_to_policy (transform s)
 8. \<And>ptr' uu_ uv_ auth ptr. \<lbrakk>einvs s; x = ptr; a = auth; y = ptr'; (ptr', uu_, uv_, auth) \<in> state_vrefs s ptr\<rbrakk> \<Longrightarrow> (x, a, y) \<in> cdl_state_objs_to_policy (transform s) proof (prove)
goal (7 subgoals):
 1. \<And>ptr cap oref. \<lbrakk>invs s \<and> valid_list s \<and> valid_sched s; x = fst (transform_cslot_ptr ptr); a = Control; y = oref; caps_of_state s ptr = Some cap; oref \<in> untyped_range cap\<rbrakk> \<Longrightarrow> oref \<in> cdl_obj_refs (transform_cap cap)
 2. \<And>ptr cap oref. \<lbrakk>invs s \<and> valid_list s \<and> valid_sched s; x = fst (transform_cslot_ptr ptr); a = Control; y = oref; caps_of_state s ptr = Some cap; oref \<in> untyped_range cap\<rbrakk> \<Longrightarrow> Control \<in> cdl_cap_auth_conferred (transform_cap cap)
 3. \<And>oref' auth oref. \<lbrakk>einvs s; x = oref; a = auth; y = oref'; (oref', auth) \<in> thread_st_auth s oref\<rbrakk> \<Longrightarrow> (x, a, y) \<in> cdl_state_objs_to_policy (transform s)
 4. \<And>oref oref' auth. \<lbrakk>einvs s; x = oref; a = auth; y = oref'; thread_bound_ntfns s oref = Some oref'; auth \<in> {Receive, Reset}\<rbrakk> \<Longrightarrow> (x, a, y) \<in> cdl_state_objs_to_policy (transform s)
 5. \<And>slot' slot. \<lbrakk>einvs s; x = fst slot; a = Control; y = fst slot'; cdt s slot' = Some slot; \<not> is_transferable_in slot' s\<rbrakk> \<Longrightarrow> (x, a, y) \<in> cdl_state_objs_to_policy (transform s)
 6. \<And>slot' slot. \<lbrakk>einvs s; x = fst slot; a = DeleteDerived; y = fst slot'; cdt s slot' = Some slot\<rbrakk> \<Longrightarrow> (x, a, y) \<in> cdl_state_objs_to_policy (transform s)
 7. \<And>ptr' uu_ uv_ auth ptr. \<lbrakk>einvs s; x = ptr; a = auth; y = ptr'; (ptr', uu_, uv_, auth) \<in> state_vrefs s ptr\<rbrakk> \<Longrightarrow> (x, a, y) \<in> cdl_state_objs_to_policy (transform s) proof (prove)
goal (6 subgoals):
 1. \<And>ptr cap oref. \<lbrakk>invs s \<and> valid_list s \<and> valid_sched s; x = fst (transform_cslot_ptr ptr); a = Control; y = oref; caps_of_state s ptr = Some cap; oref \<in> untyped_range cap\<rbrakk> \<Longrightarrow> Control \<in> cdl_cap_auth_conferred (transform_cap cap)
 2. \<And>oref' auth oref. \<lbrakk>einvs s; x = oref; a = auth; y = oref'; (oref', auth) \<in> thread_st_auth s oref\<rbrakk> \<Longrightarrow> (x, a, y) \<in> cdl_state_objs_to_policy (transform s)
 3. \<And>oref oref' auth. \<lbrakk>einvs s; x = oref; a = auth; y = oref'; thread_bound_ntfns s oref = Some oref'; auth \<in> {Receive, Reset}\<rbrakk> \<Longrightarrow> (x, a, y) \<in> cdl_state_objs_to_policy (transform s)
 4. \<And>slot' slot. \<lbrakk>einvs s; x = fst slot; a = Control; y = fst slot'; cdt s slot' = Some slot; \<not> is_transferable_in slot' s\<rbrakk> \<Longrightarrow> (x, a, y) \<in> cdl_state_objs_to_policy (transform s)
 5. \<And>slot' slot. \<lbrakk>einvs s; x = fst slot; a = DeleteDerived; y = fst slot'; cdt s slot' = Some slot\<rbrakk> \<Longrightarrow> (x, a, y) \<in> cdl_state_objs_to_policy (transform s)
 6. \<And>ptr' uu_ uv_ auth ptr. \<lbrakk>einvs s; x = ptr; a = auth; y = ptr'; (ptr', uu_, uv_, auth) \<in> state_vrefs s ptr\<rbrakk> \<Longrightarrow> (x, a, y) \<in> cdl_state_objs_to_policy (transform s) proof (prove)
goal (5 subgoals):
 1. \<And>oref' auth oref. \<lbrakk>invs s \<and> valid_list s \<and> valid_sched s; x = oref; a = auth; y = oref'; (oref', auth) \<in> thread_st_auth s oref\<rbrakk> \<Longrightarrow> (oref, auth, oref') \<in> cdl_state_objs_to_policy (transform s)
 2. \<And>oref oref' auth. \<lbrakk>einvs s; x = oref; a = auth; y = oref'; thread_bound_ntfns s oref = Some oref'; auth \<in> {Receive, Reset}\<rbrakk> \<Longrightarrow> (x, a, y) \<in> cdl_state_objs_to_policy (transform s)
 3. \<And>slot' slot. \<lbrakk>einvs s; x = fst slot; a = Control; y = fst slot'; cdt s slot' = Some slot; \<not> is_transferable_in slot' s\<rbrakk> \<Longrightarrow> (x, a, y) \<in> cdl_state_objs_to_policy (transform s)
 4. \<And>slot' slot. \<lbrakk>einvs s; x = fst slot; a = DeleteDerived; y = fst slot'; cdt s slot' = Some slot\<rbrakk> \<Longrightarrow> (x, a, y) \<in> cdl_state_objs_to_policy (transform s)
 5. \<And>ptr' uu_ uv_ auth ptr. \<lbrakk>einvs s; x = ptr; a = auth; y = ptr'; (ptr', uu_, uv_, auth) \<in> state_vrefs s ptr\<rbrakk> \<Longrightarrow> (x, a, y) \<in> cdl_state_objs_to_policy (transform s) proof (prove)
goal (4 subgoals):
 1. \<And>oref oref' auth. \<lbrakk>invs s \<and> valid_list s \<and> valid_sched s; x = oref; a = auth; y = oref'; thread_bound_ntfns s oref = Some oref'; auth = Receive \<or> auth = Reset\<rbrakk> \<Longrightarrow> (oref, auth, oref') \<in> cdl_state_objs_to_policy (transform s)
 2. \<And>slot' slot. \<lbrakk>einvs s; x = fst slot; a = Control; y = fst slot'; cdt s slot' = Some slot; \<not> is_transferable_in slot' s\<rbrakk> \<Longrightarrow> (x, a, y) \<in> cdl_state_objs_to_policy (transform s)
 3. \<And>slot' slot. \<lbrakk>einvs s; x = fst slot; a = DeleteDerived; y = fst slot'; cdt s slot' = Some slot\<rbrakk> \<Longrightarrow> (x, a, y) \<in> cdl_state_objs_to_policy (transform s)
 4. \<And>ptr' uu_ uv_ auth ptr. \<lbrakk>einvs s; x = ptr; a = auth; y = ptr'; (ptr', uu_, uv_, auth) \<in> state_vrefs s ptr\<rbrakk> \<Longrightarrow> (x, a, y) \<in> cdl_state_objs_to_policy (transform s) proof (prove)
goal (3 subgoals):
 1. \<And>slot' slot. \<lbrakk>invs s \<and> valid_list s \<and> valid_sched s; x = fst slot; a = Control; y = fst slot'; cdt s slot' = Some slot; \<not> is_transferable_in slot' s\<rbrakk> \<Longrightarrow> (fst slot, Control, fst slot') \<in> cdl_state_objs_to_policy (transform s)
 2. \<And>slot' slot. \<lbrakk>einvs s; x = fst slot; a = DeleteDerived; y = fst slot'; cdt s slot' = Some slot\<rbrakk> \<Longrightarrow> (x, a, y) \<in> cdl_state_objs_to_policy (transform s)
 3. \<And>ptr' uu_ uv_ auth ptr. \<lbrakk>einvs s; x = ptr; a = auth; y = ptr'; (ptr', uu_, uv_, auth) \<in> state_vrefs s ptr\<rbrakk> \<Longrightarrow> (x, a, y) \<in> cdl_state_objs_to_policy (transform s) proof (prove)
goal (3 subgoals):
 1. \<And>slot' slot. \<lbrakk>invs s \<and> valid_list s \<and> valid_sched s; x = fst (transform_cslot_ptr slot); a = Control; y = fst (transform_cslot_ptr slot'); cdt s slot' = Some slot; \<not> is_transferable_in slot' s\<rbrakk> \<Longrightarrow> (fst (transform_cslot_ptr slot), Control, fst (transform_cslot_ptr slot')) \<in> cdl_state_objs_to_policy (transform s)
 2. \<And>slot' slot. \<lbrakk>einvs s; x = fst slot; a = DeleteDerived; y = fst slot'; cdt s slot' = Some slot\<rbrakk> \<Longrightarrow> (x, a, y) \<in> cdl_state_objs_to_policy (transform s)
 3. \<And>ptr' uu_ uv_ auth ptr. \<lbrakk>einvs s; x = ptr; a = auth; y = ptr'; (ptr', uu_, uv_, auth) \<in> state_vrefs s ptr\<rbrakk> \<Longrightarrow> (x, a, y) \<in> cdl_state_objs_to_policy (transform s) proof (prove)
goal (4 subgoals):
 1. \<And>slot' slot. \<lbrakk>invs s \<and> valid_list s \<and> valid_sched s; x = fst (transform_cslot_ptr slot); a = Control; y = fst (transform_cslot_ptr slot'); cdt s slot' = Some slot; \<not> is_transferable_in slot' s\<rbrakk> \<Longrightarrow> cdl_cdt (transform s) (transform_cslot_ptr slot') = Some (transform_cslot_ptr slot)
 2. \<And>slot' slot. \<lbrakk>invs s \<and> valid_list s \<and> valid_sched s; x = fst (transform_cslot_ptr slot); a = Control; y = fst (transform_cslot_ptr slot'); cdt s slot' = Some slot; \<not> is_transferable_in slot' s\<rbrakk> \<Longrightarrow> \<not> cdl_cap_is_transferable (opt_cap (transform_cslot_ptr slot') (transform s))
 3. \<And>slot' slot. \<lbrakk>einvs s; x = fst slot; a = DeleteDerived; y = fst slot'; cdt s slot' = Some slot\<rbrakk> \<Longrightarrow> (x, a, y) \<in> cdl_state_objs_to_policy (transform s)
 4. \<And>ptr' uu_ uv_ auth ptr. \<lbrakk>einvs s; x = ptr; a = auth; y = ptr'; (ptr', uu_, uv_, auth) \<in> state_vrefs s ptr\<rbrakk> \<Longrightarrow> (x, a, y) \<in> cdl_state_objs_to_policy (transform s) proof (prove)
goal (4 subgoals):
 1. \<And>slot' slot. \<lbrakk>invs s \<and> valid_list s \<and> valid_sched s; x = fst (transform_cslot_ptr slot); a = Control; y = fst (transform_cslot_ptr slot'); cdt s slot' = Some slot; \<not> is_transferable_in slot' s\<rbrakk> \<Longrightarrow> transform_cdt s (transform_cslot_ptr slot') = Some (transform_cslot_ptr slot)
 2. \<And>slot' slot. \<lbrakk>invs s \<and> valid_list s \<and> valid_sched s; x = fst (transform_cslot_ptr slot); a = Control; y = fst (transform_cslot_ptr slot'); cdt s slot' = Some slot; \<not> is_transferable_in slot' s\<rbrakk> \<Longrightarrow> \<not> cdl_cap_is_transferable (opt_cap (transform_cslot_ptr slot') (transform s))
 3. \<And>slot' slot. \<lbrakk>einvs s; x = fst slot; a = DeleteDerived; y = fst slot'; cdt s slot' = Some slot\<rbrakk> \<Longrightarrow> (x, a, y) \<in> cdl_state_objs_to_policy (transform s)
 4. \<And>ptr' uu_ uv_ auth ptr. \<lbrakk>einvs s; x = ptr; a = auth; y = ptr'; (ptr', uu_, uv_, auth) \<in> state_vrefs s ptr\<rbrakk> \<Longrightarrow> (x, a, y) \<in> cdl_state_objs_to_policy (transform s) proof (prove)
goal (5 subgoals):
 1. \<And>slot' slot. \<lbrakk>invs s \<and> valid_list s \<and> valid_sched s; x = fst (transform_cslot_ptr slot); a = Control; y = fst (transform_cslot_ptr slot'); cdt s slot' = Some slot; \<not> is_transferable_in slot' s\<rbrakk> \<Longrightarrow> mdb_cte_at (swp (cte_wp_at ((\<noteq>) cap.NullCap)) s) (cdt s)
 2. \<And>slot' slot. \<lbrakk>invs s \<and> valid_list s \<and> valid_sched s; x = fst (transform_cslot_ptr slot); a = Control; y = fst (transform_cslot_ptr slot'); cdt s slot' = Some slot; \<not> is_transferable_in slot' s\<rbrakk> \<Longrightarrow> cdt s slot' = Some slot
 3. \<And>slot' slot. \<lbrakk>invs s \<and> valid_list s \<and> valid_sched s; x = fst (transform_cslot_ptr slot); a = Control; y = fst (transform_cslot_ptr slot'); cdt s slot' = Some slot; \<not> is_transferable_in slot' s\<rbrakk> \<Longrightarrow> \<not> cdl_cap_is_transferable (opt_cap (transform_cslot_ptr slot') (transform s))
 4. \<And>slot' slot. \<lbrakk>einvs s; x = fst slot; a = DeleteDerived; y = fst slot'; cdt s slot' = Some slot\<rbrakk> \<Longrightarrow> (x, a, y) \<in> cdl_state_objs_to_policy (transform s)
 5. \<And>ptr' uu_ uv_ auth ptr. \<lbrakk>einvs s; x = ptr; a = auth; y = ptr'; (ptr', uu_, uv_, auth) \<in> state_vrefs s ptr\<rbrakk> \<Longrightarrow> (x, a, y) \<in> cdl_state_objs_to_policy (transform s) proof (prove)
goal (4 subgoals):
 1. \<And>slot' slot. \<lbrakk>invs s \<and> valid_list s \<and> valid_sched s; x = fst (transform_cslot_ptr slot); a = Control; y = fst (transform_cslot_ptr slot'); cdt s slot' = Some slot; \<not> is_transferable_in slot' s\<rbrakk> \<Longrightarrow> cdt s slot' = Some slot
 2. \<And>slot' slot. \<lbrakk>invs s \<and> valid_list s \<and> valid_sched s; x = fst (transform_cslot_ptr slot); a = Control; y = fst (transform_cslot_ptr slot'); cdt s slot' = Some slot; \<not> is_transferable_in slot' s\<rbrakk> \<Longrightarrow> \<not> cdl_cap_is_transferable (opt_cap (transform_cslot_ptr slot') (transform s))
 3. \<And>slot' slot. \<lbrakk>einvs s; x = fst slot; a = DeleteDerived; y = fst slot'; cdt s slot' = Some slot\<rbrakk> \<Longrightarrow> (x, a, y) \<in> cdl_state_objs_to_policy (transform s)
 4. \<And>ptr' uu_ uv_ auth ptr. \<lbrakk>einvs s; x = ptr; a = auth; y = ptr'; (ptr', uu_, uv_, auth) \<in> state_vrefs s ptr\<rbrakk> \<Longrightarrow> (x, a, y) \<in> cdl_state_objs_to_policy (transform s) proof (prove)
goal (3 subgoals):
 1. \<And>slot' slot. \<lbrakk>invs s \<and> valid_list s \<and> valid_sched s; x = fst (transform_cslot_ptr slot); a = Control; y = fst (transform_cslot_ptr slot'); cdt s slot' = Some slot; \<not> is_transferable_in slot' s\<rbrakk> \<Longrightarrow> \<not> cdl_cap_is_transferable (opt_cap (transform_cslot_ptr slot') (transform s))
 2. \<And>slot' slot. \<lbrakk>einvs s; x = fst slot; a = DeleteDerived; y = fst slot'; cdt s slot' = Some slot\<rbrakk> \<Longrightarrow> (x, a, y) \<in> cdl_state_objs_to_policy (transform s)
 3. \<And>ptr' uu_ uv_ auth ptr. \<lbrakk>einvs s; x = ptr; a = auth; y = ptr'; (ptr', uu_, uv_, auth) \<in> state_vrefs s ptr\<rbrakk> \<Longrightarrow> (x, a, y) \<in> cdl_state_objs_to_policy (transform s) proof (prove)
goal (2 subgoals):
 1. \<And>slot' slot. \<lbrakk>einvs s; x = fst slot; a = DeleteDerived; y = fst slot'; cdt s slot' = Some slot\<rbrakk> \<Longrightarrow> (x, a, y) \<in> cdl_state_objs_to_policy (transform s)
 2. \<And>ptr' uu_ uv_ auth ptr. \<lbrakk>einvs s; x = ptr; a = auth; y = ptr'; (ptr', uu_, uv_, auth) \<in> state_vrefs s ptr\<rbrakk> \<Longrightarrow> (x, a, y) \<in> cdl_state_objs_to_policy (transform s) proof (prove)
goal (2 subgoals):
 1. \<And>b ba. \<lbrakk>a = DeleteDerived; cdt s (y, b) = Some (x, ba); invs s; valid_list s; valid_sched s\<rbrakk> \<Longrightarrow> (x, DeleteDerived, y) \<in> cdl_state_objs_to_policy (transform s)
 2. \<And>ptr' uu_ uv_ auth ptr. \<lbrakk>einvs s; x = ptr; a = auth; y = ptr'; (ptr', uu_, uv_, auth) \<in> state_vrefs s ptr\<rbrakk> \<Longrightarrow> (x, a, y) \<in> cdl_state_objs_to_policy (transform s) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>a = DeleteDerived; cdt s (y, slot) = Some (x, pslot); invs s; valid_list s; valid_sched s\<rbrakk> \<Longrightarrow> (x, DeleteDerived, y) \<in> cdl_state_objs_to_policy (transform s) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>a = DeleteDerived; cdt s (y, slot) = Some (x, pslot); invs s; valid_list s; valid_sched s\<rbrakk> \<Longrightarrow> cdl_cdt (transform s) (y, nat (bl_to_bin slot)) = Some (x, nat (bl_to_bin pslot)) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>a = DeleteDerived; cdt s (y, slot) = Some (x, pslot); invs s; valid_list s; valid_sched s; inj_on transform_cslot_ptr (dom (cdt s) \<union> ran (cdt s))\<rbrakk> \<Longrightarrow> cdl_cdt (transform s) (y, nat (bl_to_bin slot)) = Some (x, nat (bl_to_bin pslot)) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>a = DeleteDerived; cdt s (y, slot) = Some (x, pslot); invs s; valid_list s; valid_sched s; inj_on (\<lambda>(a, b). (a, nat (bl_to_bin b))) (dom (cdt s) \<union> ran (cdt s))\<rbrakk> \<Longrightarrow> ((\<exists>b. nat (bl_to_bin b) = nat (bl_to_bin slot) \<and> (y, b) \<in> dom (cdt s)) \<longrightarrow> (\<exists>b. cdt s (inv_into (dom (cdt s)) (\<lambda>(a, b). (a, nat (bl_to_bin b))) (y, nat (bl_to_bin slot))) = Some (x, b) \<and> nat (bl_to_bin b) = nat (bl_to_bin pslot))) \<and> (\<exists>b. nat (bl_to_bin b) = nat (bl_to_bin slot) \<and> (y, b) \<in> dom (cdt s)) proof (prove)
goal (2 subgoals):
 1. \<And>b aa ba. \<lbrakk>a = DeleteDerived; cdt s (y, slot) = Some (x, pslot); invs s; valid_list s; valid_sched s; inj_on (\<lambda>(a, b). (a, nat (bl_to_bin b))) (dom (cdt s) \<union> ran (cdt s)); nat (bl_to_bin b) = nat (bl_to_bin slot); cdt s (y, b) = Some (aa, ba)\<rbrakk> \<Longrightarrow> \<exists>b. cdt s (inv_into (dom (cdt s)) (\<lambda>(a, b). (a, nat (bl_to_bin b))) (y, nat (bl_to_bin slot))) = Some (x, b) \<and> nat (bl_to_bin b) = nat (bl_to_bin pslot)
 2. \<lbrakk>a = DeleteDerived; cdt s (y, slot) = Some (x, pslot); invs s; valid_list s; valid_sched s; inj_on (\<lambda>(a, b). (a, nat (bl_to_bin b))) (dom (cdt s) \<union> ran (cdt s))\<rbrakk> \<Longrightarrow> \<exists>b. nat (bl_to_bin b) = nat (bl_to_bin slot) \<and> (y, b) \<in> dom (cdt s) proof (prove)
goal (2 subgoals):
 1. \<And>b aa ba. \<lbrakk>a = DeleteDerived; cdt s (y, slot) = Some (x, pslot); invs s; valid_list s; valid_sched s; inj_on (\<lambda>(a, b). (a, nat (bl_to_bin b))) (dom (cdt s) \<union> ran (cdt s)); nat (bl_to_bin b) = nat (bl_to_bin slot); cdt s (y, b) = Some (aa, ba)\<rbrakk> \<Longrightarrow> cdt s (inv_into (dom (cdt s)) (\<lambda>(a, b). (a, nat (bl_to_bin b))) (y, nat (bl_to_bin slot))) = Some (x, pslot) \<and> nat (bl_to_bin pslot) = nat (bl_to_bin pslot)
 2. \<lbrakk>a = DeleteDerived; cdt s (y, slot) = Some (x, pslot); invs s; valid_list s; valid_sched s; inj_on (\<lambda>(a, b). (a, nat (bl_to_bin b))) (dom (cdt s) \<union> ran (cdt s))\<rbrakk> \<Longrightarrow> \<exists>b. nat (bl_to_bin b) = nat (bl_to_bin slot) \<and> (y, b) \<in> dom (cdt s) proof (prove)
goal (5 subgoals):
 1. \<And>b aa ba. \<lbrakk>a = DeleteDerived; cdt s (y, slot) = Some (x, pslot); invs s; valid_list s; valid_sched s; inj_on (\<lambda>(a, b). (a, nat (bl_to_bin b))) (dom (cdt s) \<union> ran (cdt s)); nat (bl_to_bin b) = nat (bl_to_bin slot); cdt s (y, b) = Some (aa, ba)\<rbrakk> \<Longrightarrow> inj_on (\<lambda>(a, b). (a, nat (bl_to_bin b))) (dom (cdt s))
 2. \<And>b aa ba. \<lbrakk>a = DeleteDerived; cdt s (y, slot) = Some (x, pslot); invs s; valid_list s; valid_sched s; inj_on (\<lambda>(a, b). (a, nat (bl_to_bin b))) (dom (cdt s) \<union> ran (cdt s)); nat (bl_to_bin b) = nat (bl_to_bin slot); cdt s (y, b) = Some (aa, ba)\<rbrakk> \<Longrightarrow> (y, slot) \<in> dom (cdt s)
 3. \<And>b aa ba. \<lbrakk>a = DeleteDerived; cdt s (y, slot) = Some (x, pslot); invs s; valid_list s; valid_sched s; inj_on (\<lambda>(a, b). (a, nat (bl_to_bin b))) (dom (cdt s) \<union> ran (cdt s)); nat (bl_to_bin b) = nat (bl_to_bin slot); cdt s (y, b) = Some (aa, ba)\<rbrakk> \<Longrightarrow> (case (y, slot) of (a, b) \<Rightarrow> (a, nat (bl_to_bin b))) = (y, nat (bl_to_bin slot))
 4. \<And>b aa ba. \<lbrakk>a = DeleteDerived; cdt s (y, slot) = Some (x, pslot); invs s; valid_list s; valid_sched s; inj_on (\<lambda>(a, b). (a, nat (bl_to_bin b))) (dom (cdt s) \<union> ran (cdt s)); nat (bl_to_bin b) = nat (bl_to_bin slot); cdt s (y, b) = Some (aa, ba)\<rbrakk> \<Longrightarrow> cdt s (y, slot) = Some (x, pslot) \<and> nat (bl_to_bin pslot) = nat (bl_to_bin pslot)
 5. \<lbrakk>a = DeleteDerived; cdt s (y, slot) = Some (x, pslot); invs s; valid_list s; valid_sched s; inj_on (\<lambda>(a, b). (a, nat (bl_to_bin b))) (dom (cdt s) \<union> ran (cdt s))\<rbrakk> \<Longrightarrow> \<exists>b. nat (bl_to_bin b) = nat (bl_to_bin slot) \<and> (y, b) \<in> dom (cdt s) proof (prove)
goal (4 subgoals):
 1. \<And>b aa ba. \<lbrakk>a = DeleteDerived; cdt s (y, slot) = Some (x, pslot); invs s; valid_list s; valid_sched s; inj_on (\<lambda>(a, b). (a, nat (bl_to_bin b))) (dom (cdt s) \<union> ran (cdt s)); nat (bl_to_bin b) = nat (bl_to_bin slot); cdt s (y, b) = Some (aa, ba)\<rbrakk> \<Longrightarrow> (y, slot) \<in> dom (cdt s)
 2. \<And>b aa ba. \<lbrakk>a = DeleteDerived; cdt s (y, slot) = Some (x, pslot); invs s; valid_list s; valid_sched s; inj_on (\<lambda>(a, b). (a, nat (bl_to_bin b))) (dom (cdt s) \<union> ran (cdt s)); nat (bl_to_bin b) = nat (bl_to_bin slot); cdt s (y, b) = Some (aa, ba)\<rbrakk> \<Longrightarrow> (case (y, slot) of (a, b) \<Rightarrow> (a, nat (bl_to_bin b))) = (y, nat (bl_to_bin slot))
 3. \<And>b aa ba. \<lbrakk>a = DeleteDerived; cdt s (y, slot) = Some (x, pslot); invs s; valid_list s; valid_sched s; inj_on (\<lambda>(a, b). (a, nat (bl_to_bin b))) (dom (cdt s) \<union> ran (cdt s)); nat (bl_to_bin b) = nat (bl_to_bin slot); cdt s (y, b) = Some (aa, ba)\<rbrakk> \<Longrightarrow> cdt s (y, slot) = Some (x, pslot) \<and> nat (bl_to_bin pslot) = nat (bl_to_bin pslot)
 4. \<lbrakk>a = DeleteDerived; cdt s (y, slot) = Some (x, pslot); invs s; valid_list s; valid_sched s; inj_on (\<lambda>(a, b). (a, nat (bl_to_bin b))) (dom (cdt s) \<union> ran (cdt s))\<rbrakk> \<Longrightarrow> \<exists>b. nat (bl_to_bin b) = nat (bl_to_bin slot) \<and> (y, b) \<in> dom (cdt s) proof (prove)
goal (3 subgoals):
 1. \<And>b aa ba. \<lbrakk>a = DeleteDerived; cdt s (y, slot) = Some (x, pslot); invs s; valid_list s; valid_sched s; inj_on (\<lambda>(a, b). (a, nat (bl_to_bin b))) (dom (cdt s) \<union> ran (cdt s)); nat (bl_to_bin b) = nat (bl_to_bin slot); cdt s (y, b) = Some (aa, ba)\<rbrakk> \<Longrightarrow> (case (y, slot) of (a, b) \<Rightarrow> (a, nat (bl_to_bin b))) = (y, nat (bl_to_bin slot))
 2. \<And>b aa ba. \<lbrakk>a = DeleteDerived; cdt s (y, slot) = Some (x, pslot); invs s; valid_list s; valid_sched s; inj_on (\<lambda>(a, b). (a, nat (bl_to_bin b))) (dom (cdt s) \<union> ran (cdt s)); nat (bl_to_bin b) = nat (bl_to_bin slot); cdt s (y, b) = Some (aa, ba)\<rbrakk> \<Longrightarrow> cdt s (y, slot) = Some (x, pslot) \<and> nat (bl_to_bin pslot) = nat (bl_to_bin pslot)
 3. \<lbrakk>a = DeleteDerived; cdt s (y, slot) = Some (x, pslot); invs s; valid_list s; valid_sched s; inj_on (\<lambda>(a, b). (a, nat (bl_to_bin b))) (dom (cdt s) \<union> ran (cdt s))\<rbrakk> \<Longrightarrow> \<exists>b. nat (bl_to_bin b) = nat (bl_to_bin slot) \<and> (y, b) \<in> dom (cdt s) proof (prove)
goal (2 subgoals):
 1. \<And>b aa ba. \<lbrakk>a = DeleteDerived; cdt s (y, slot) = Some (x, pslot); invs s; valid_list s; valid_sched s; inj_on (\<lambda>(a, b). (a, nat (bl_to_bin b))) (dom (cdt s) \<union> ran (cdt s)); nat (bl_to_bin b) = nat (bl_to_bin slot); cdt s (y, b) = Some (aa, ba)\<rbrakk> \<Longrightarrow> cdt s (y, slot) = Some (x, pslot) \<and> nat (bl_to_bin pslot) = nat (bl_to_bin pslot)
 2. \<lbrakk>a = DeleteDerived; cdt s (y, slot) = Some (x, pslot); invs s; valid_list s; valid_sched s; inj_on (\<lambda>(a, b). (a, nat (bl_to_bin b))) (dom (cdt s) \<union> ran (cdt s))\<rbrakk> \<Longrightarrow> \<exists>b. nat (bl_to_bin b) = nat (bl_to_bin slot) \<and> (y, b) \<in> dom (cdt s) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>a = DeleteDerived; cdt s (y, slot) = Some (x, pslot); invs s; valid_list s; valid_sched s; inj_on (\<lambda>(a, b). (a, nat (bl_to_bin b))) (dom (cdt s) \<union> ran (cdt s))\<rbrakk> \<Longrightarrow> \<exists>b. nat (bl_to_bin b) = nat (bl_to_bin slot) \<and> (y, b) \<in> dom (cdt s) proof (prove)
goal:
No subgoals! proof (prove)
goal (1 subgoal):
 1. \<And>ptr' uu_ uv_ auth ptr. \<lbrakk>einvs s; x = ptr; a = auth; y = ptr'; (ptr', uu_, uv_, auth) \<in> state_vrefs s ptr\<rbrakk> \<Longrightarrow> (x, a, y) \<in> cdl_state_objs_to_policy (transform s) proof (prove)
goal (2 subgoals):
 1. \<And>ptr' uu_ uv_ auth ptr. \<lbrakk>einvs s; x = ptr; a = auth; y = ptr'; (ptr', uu_, uv_, auth) \<in> state_vrefs s ptr; ptr \<noteq> idle_thread s\<rbrakk> \<Longrightarrow> (x, a, y) \<in> cdl_state_objs_to_policy (transform s)
 2. \<And>ptr' uu_ uv_ auth ptr. \<lbrakk>einvs s; x = ptr; a = auth; y = ptr'; (ptr', uu_, uv_, auth) \<in> state_vrefs s ptr\<rbrakk> \<Longrightarrow> ptr \<noteq> idle_thread s proof (prove)
goal (1 subgoal):
 1. \<And>ptr' uu_ uv_ auth ptr. \<lbrakk>einvs s; x = ptr; a = auth; y = ptr'; (ptr', uu_, uv_, auth) \<in> state_vrefs s ptr\<rbrakk> \<Longrightarrow> ptr \<noteq> idle_thread s proof (prove)
goal:
No subgoals!