theory KHeap_DR

lemma cap_counts_inv:
assumes "\<And>cap. P cap\<Longrightarrow> cap_counts cap"
shows "\<lbrakk>opt_cap_wp_at P slot (transform s);valid_objs s; valid_etcbs s\<rbrakk>
  \<Longrightarrow> \<exists>slot'. slot = transform_cslot_ptr slot' \<and> cte_wp_at (\<lambda>cap'. P (transform_cap cap')) slot' s" apply (clarsimp simp:opt_cap_wp_at_def' split:option.splits) apply (case_tac slot) apply (rename_tac ptr offset) apply (clarsimp simp:slots_of_def KHeap_D.opt_cap_def transform_def split:option.splits) apply (rule_tac x = ptr in exI) apply (clarsimp simp:transform_objects_def restrict_map_Some_iff object_slots_def split:cdl_object.splits) apply (frule assms) apply (clarsimp simp: cte_wp_at_cases transform_object_def transform_tcb_def
                             tcb_pending_op_slot_def tcb_boundntfn_slot_def
                       split: Structures_A.kernel_object.splits nat.splits if_splits
              | drule(1) valid_etcbs_tcb_etcb)+ apply (clarsimp simp: cap_counts_def infer_tcb_bound_notification_def split:option.splits) apply (clarsimp simp:cap_counts_def infer_tcb_pending_op_def split:Structures_A.thread_state.splits nat.splits) using transform_tcb_slot_simp[simplified,symmetric] apply (rule_tac x= "tcb_cnode_index 4" in exI) apply (clarsimp) using transform_tcb_slot_simp[simplified,symmetric] apply (rule_tac x= "tcb_cnode_index 3" in exI) apply (clarsimp) using transform_tcb_slot_simp[simplified,symmetric] apply (rule_tac x= "tcb_cnode_index 2" in exI) apply (clarsimp) using transform_tcb_slot_simp[simplified,symmetric] apply (rule_tac x= "tcb_cnode_index 1" in exI) apply (clarsimp) using transform_tcb_slot_simp[simplified,symmetric] apply (rule_tac x= "tcb_cnode_index 0" in exI) apply (clarsimp) apply (rename_tac arch_kernel_obj) apply (case_tac arch_kernel_obj,simp_all) apply (simp_all add:object_slots_def transform_object_def) apply (clarsimp simp:transform_cnode_contents_def option_map_join_def
                     split:option.splits Structures_A.kernel_object.splits nat.splits) apply (clarsimp simp:cte_wp_at_cases well_formed_cnode_invsI transform_cslot_ptr_def split:if_splits) apply (rule_tac x = x2b in exI,simp add: nat_to_bl_to_bin) apply (drule(1) valid_etcbs_tcb_etcb, simp) prefer 6  (* IRQ Node *)
        apply (clarsimp split: Structures_A.kernel_object.splits nat.splits option.splits) apply (clarsimp simp:transform_cnode_contents_def option_map_join_def
                         split:option.splits Structures_A.kernel_object.splits nat.splits) apply (clarsimp simp:cte_wp_at_cases well_formed_cnode_invsI transform_cslot_ptr_def split:if_splits) apply (rule_tac x = x2a in exI,simp add: nat_to_bl_to_bin) apply (frule assms) apply ((simp_all add:Let_def cap_counts_def transform_tcb_def
                        split:option.splits if_splits arch_kernel_obj.splits
                              Structures_A.kernel_object.splits cdl_object.splits nat.splits|
                drule(1) valid_etcbs_tcb_etcb |
                clarsimp simp: unat_map_def transform_page_table_contents_def cap_counts_def
                          transform_page_directory_contents_def transform_asid_pool_contents_def
                          transform_pte_def transform_pde_def transform_asid_pool_entry_def
                    split:option.splits if_splits ARM_A.pte.splits ARM_A.pde.splits
                    dest!:assms)+) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>opt_cap_wp_at P slot (transform s); valid_objs s; valid_etcbs s\<rbrakk> \<Longrightarrow> \<exists>slot'. slot = transform_cslot_ptr slot' \<and> cte_wp_at (\<lambda>cap'. P (transform_cap cap')) slot' s proof (prove)
goal (1 subgoal):
 1. \<And>x2. \<lbrakk>valid_objs s; valid_etcbs s; opt_cap slot (transform s) = Some x2; P x2\<rbrakk> \<Longrightarrow> \<exists>a b. slot = transform_cslot_ptr (a, b) \<and> cte_wp_at (\<lambda>cap'. P (transform_cap cap')) (a, b) s proof (prove)
goal (1 subgoal):
 1. \<And>x2 a b. \<lbrakk>valid_objs s; valid_etcbs s; opt_cap slot (transform s) = Some x2; P x2; slot = (a, b)\<rbrakk> \<Longrightarrow> \<exists>a b. slot = transform_cslot_ptr (a, b) \<and> cte_wp_at (\<lambda>cap'. P (transform_cap cap')) (a, b) s proof (prove)
goal (1 subgoal):
 1. \<And>x2 ptr offset. \<lbrakk>valid_objs s; valid_etcbs s; opt_cap slot (transform s) = Some x2; P x2; slot = (ptr, offset)\<rbrakk> \<Longrightarrow> \<exists>a b. slot = transform_cslot_ptr (a, b) \<and> cte_wp_at (\<lambda>cap'. P (transform_cap cap')) (a, b) s proof (prove)
goal (1 subgoal):
 1. \<And>x2 ptr offset x2a. \<lbrakk>P x2; slot = (ptr, offset); valid_objs s; valid_etcbs s; transform_objects s ptr = Some x2a; object_slots x2a offset = Some x2\<rbrakk> \<Longrightarrow> \<exists>a b. (ptr, offset) = transform_cslot_ptr (a, b) \<and> cte_wp_at (\<lambda>cap'. P (transform_cap cap')) (a, b) s proof (prove)
goal (1 subgoal):
 1. \<And>x2 ptr offset x2a. \<lbrakk>P x2; slot = (ptr, offset); valid_objs s; valid_etcbs s; transform_objects s ptr = Some x2a; object_slots x2a offset = Some x2\<rbrakk> \<Longrightarrow> \<exists>b. (ptr, offset) = transform_cslot_ptr (ptr, b) \<and> cte_wp_at (\<lambda>cap'. P (transform_cap cap')) (ptr, b) s proof (prove)
goal (6 subgoals):
 1. \<And>x2 ptr offset x3 z. \<lbrakk>P x2; slot = (ptr, offset); valid_objs s; valid_etcbs s; cdl_tcb_caps x3 offset = Some x2; kheap s ptr = Some z; ptr \<noteq> idle_thread s; transform_object (machine_state s) ptr (ekheap s ptr) z = Tcb x3\<rbrakk> \<Longrightarrow> \<exists>b. (ptr, offset) = transform_cslot_ptr (ptr, b) \<and> cte_wp_at (\<lambda>cap'. P (transform_cap cap')) (ptr, b) s
 2. \<And>x2 ptr offset x4 z. \<lbrakk>P x2; slot = (ptr, offset); valid_objs s; valid_etcbs s; cdl_cnode_caps x4 offset = Some x2; kheap s ptr = Some z; ptr \<noteq> idle_thread s; transform_object (machine_state s) ptr (ekheap s ptr) z = cdl_object.CNode x4\<rbrakk> \<Longrightarrow> \<exists>b. (ptr, offset) = transform_cslot_ptr (ptr, b) \<and> cte_wp_at (\<lambda>cap'. P (transform_cap cap')) (ptr, b) s
 3. \<And>x2 ptr offset x5 z. \<lbrakk>P x2; slot = (ptr, offset); valid_objs s; valid_etcbs s; cdl_asid_pool_caps x5 offset = Some x2; kheap s ptr = Some z; ptr \<noteq> idle_thread s; transform_object (machine_state s) ptr (ekheap s ptr) z = AsidPool x5\<rbrakk> \<Longrightarrow> \<exists>b. (ptr, offset) = transform_cslot_ptr (ptr, b) \<and> cte_wp_at (\<lambda>cap'. P (transform_cap cap')) (ptr, b) s
 4. \<And>x2 ptr offset x6 z. \<lbrakk>P x2; slot = (ptr, offset); valid_objs s; valid_etcbs s; cdl_page_table_caps x6 offset = Some x2; kheap s ptr = Some z; ptr \<noteq> idle_thread s; transform_object (machine_state s) ptr (ekheap s ptr) z = cdl_object.PageTable x6\<rbrakk> \<Longrightarrow> \<exists>b. (ptr, offset) = transform_cslot_ptr (ptr, b) \<and> cte_wp_at (\<lambda>cap'. P (transform_cap cap')) (ptr, b) s
 5. \<And>x2 ptr offset x7 z. \<lbrakk>P x2; slot = (ptr, offset); valid_objs s; valid_etcbs s; cdl_page_directory_caps x7 offset = Some x2; kheap s ptr = Some z; ptr \<noteq> idle_thread s; transform_object (machine_state s) ptr (ekheap s ptr) z = cdl_object.PageDirectory x7\<rbrakk> \<Longrightarrow> \<exists>b. (ptr, offset) = transform_cslot_ptr (ptr, b) \<and> cte_wp_at (\<lambda>cap'. P (transform_cap cap')) (ptr, b) s
 6. \<And>x2 ptr offset x10 z. \<lbrakk>P x2; slot = (ptr, offset); valid_objs s; valid_etcbs s; cdl_irq_node_caps x10 offset = Some x2; kheap s ptr = Some z; ptr \<noteq> idle_thread s; transform_object (machine_state s) ptr (ekheap s ptr) z = IRQNode x10\<rbrakk> \<Longrightarrow> \<exists>b. (ptr, offset) = transform_cslot_ptr (ptr, b) \<and> cte_wp_at (\<lambda>cap'. P (transform_cap cap')) (ptr, b) s proof (prove)
goal (6 subgoals):
 1. \<And>x2 ptr offset x3 z. \<lbrakk>P x2; slot = (ptr, offset); valid_objs s; valid_etcbs s; cdl_tcb_caps x3 offset = Some x2; kheap s ptr = Some z; ptr \<noteq> idle_thread s; transform_object (machine_state s) ptr (ekheap s ptr) z = Tcb x3; cap_counts x2\<rbrakk> \<Longrightarrow> \<exists>b. (ptr, offset) = transform_cslot_ptr (ptr, b) \<and> cte_wp_at (\<lambda>cap'. P (transform_cap cap')) (ptr, b) s
 2. \<And>x2 ptr offset x4 z. \<lbrakk>P x2; slot = (ptr, offset); valid_objs s; valid_etcbs s; cdl_cnode_caps x4 offset = Some x2; kheap s ptr = Some z; ptr \<noteq> idle_thread s; transform_object (machine_state s) ptr (ekheap s ptr) z = cdl_object.CNode x4\<rbrakk> \<Longrightarrow> \<exists>b. (ptr, offset) = transform_cslot_ptr (ptr, b) \<and> cte_wp_at (\<lambda>cap'. P (transform_cap cap')) (ptr, b) s
 3. \<And>x2 ptr offset x5 z. \<lbrakk>P x2; slot = (ptr, offset); valid_objs s; valid_etcbs s; cdl_asid_pool_caps x5 offset = Some x2; kheap s ptr = Some z; ptr \<noteq> idle_thread s; transform_object (machine_state s) ptr (ekheap s ptr) z = AsidPool x5\<rbrakk> \<Longrightarrow> \<exists>b. (ptr, offset) = transform_cslot_ptr (ptr, b) \<and> cte_wp_at (\<lambda>cap'. P (transform_cap cap')) (ptr, b) s
 4. \<And>x2 ptr offset x6 z. \<lbrakk>P x2; slot = (ptr, offset); valid_objs s; valid_etcbs s; cdl_page_table_caps x6 offset = Some x2; kheap s ptr = Some z; ptr \<noteq> idle_thread s; transform_object (machine_state s) ptr (ekheap s ptr) z = cdl_object.PageTable x6\<rbrakk> \<Longrightarrow> \<exists>b. (ptr, offset) = transform_cslot_ptr (ptr, b) \<and> cte_wp_at (\<lambda>cap'. P (transform_cap cap')) (ptr, b) s
 5. \<And>x2 ptr offset x7 z. \<lbrakk>P x2; slot = (ptr, offset); valid_objs s; valid_etcbs s; cdl_page_directory_caps x7 offset = Some x2; kheap s ptr = Some z; ptr \<noteq> idle_thread s; transform_object (machine_state s) ptr (ekheap s ptr) z = cdl_object.PageDirectory x7\<rbrakk> \<Longrightarrow> \<exists>b. (ptr, offset) = transform_cslot_ptr (ptr, b) \<and> cte_wp_at (\<lambda>cap'. P (transform_cap cap')) (ptr, b) s
 6. \<And>x2 ptr offset x10 z. \<lbrakk>P x2; slot = (ptr, offset); valid_objs s; valid_etcbs s; cdl_irq_node_caps x10 offset = Some x2; kheap s ptr = Some z; ptr \<noteq> idle_thread s; transform_object (machine_state s) ptr (ekheap s ptr) z = IRQNode x10\<rbrakk> \<Longrightarrow> \<exists>b. (ptr, offset) = transform_cslot_ptr (ptr, b) \<and> cte_wp_at (\<lambda>cap'. P (transform_cap cap')) (ptr, b) s proof (prove)
goal (13 subgoals):
 1. \<And>ptr x2a etcb. \<lbrakk>kheap s ptr = Some (TCB x2a); ptr \<noteq> idle_thread s; ekheap s ptr = Some etcb; cap_counts (infer_tcb_bound_notification (tcb_bound_notification x2a)); P (infer_tcb_bound_notification (tcb_bound_notification x2a)); slot = (ptr, 6); valid_objs s\<rbrakk> \<Longrightarrow> \<exists>b. (ptr, 6) = transform_cslot_ptr (ptr, b) \<and> (\<exists>get. (\<exists>set restr. tcb_cap_cases b = Some (get, set, restr)) \<and> P (transform_cap (get x2a)))
 2. \<And>x2 ptr offset x2a etcb. \<lbrakk>kheap s ptr = Some (TCB x2a); ptr \<noteq> idle_thread s; ekheap s ptr = Some etcb; cap_counts x2; P x2; slot = (ptr, 5); valid_objs s; offset = 5; infer_tcb_pending_op ptr (tcb_state x2a) = x2\<rbrakk> \<Longrightarrow> \<exists>b. (ptr, 5) = transform_cslot_ptr (ptr, b) \<and> (\<exists>get. (\<exists>set restr. tcb_cap_cases b = Some (get, set, restr)) \<and> P (transform_cap (get x2a)))
 3. \<And>x2 ptr offset x2a etcb. \<lbrakk>kheap s ptr = Some (TCB x2a); ptr \<noteq> idle_thread s; ekheap s ptr = Some etcb; cap_counts x2; P x2; slot = (ptr, tcb_ipcbuffer_slot); valid_objs s; tcb_ipcbuffer_slot \<noteq> 6; tcb_ipcbuffer_slot \<noteq> 5; offset = tcb_ipcbuffer_slot; transform_cap (tcb_ipcframe x2a) = x2\<rbrakk> \<Longrightarrow> \<exists>b. (ptr, tcb_ipcbuffer_slot) = transform_cslot_ptr (ptr, b) \<and> (\<exists>get. (\<exists>set restr. tcb_cap_cases b = Some (get, set, restr)) \<and> P (transform_cap (get x2a)))
 4. \<And>x2 ptr offset x2a etcb. \<lbrakk>kheap s ptr = Some (TCB x2a); ptr \<noteq> idle_thread s; ekheap s ptr = Some etcb; cap_counts x2; P x2; slot = (ptr, tcb_caller_slot); valid_objs s; tcb_caller_slot \<noteq> 6; tcb_caller_slot \<noteq> 5; tcb_caller_slot \<noteq> tcb_ipcbuffer_slot; offset = tcb_caller_slot; transform_cap (tcb_caller x2a) = x2\<rbrakk> \<Longrightarrow> \<exists>b. (ptr, tcb_caller_slot) = transform_cslot_ptr (ptr, b) \<and> (\<exists>get. (\<exists>set restr. tcb_cap_cases b = Some (get, set, restr)) \<and> P (transform_cap (get x2a)))
 5. \<And>x2 ptr offset x2a etcb. \<lbrakk>kheap s ptr = Some (TCB x2a); ptr \<noteq> idle_thread s; ekheap s ptr = Some etcb; cap_counts x2; P x2; slot = (ptr, tcb_replycap_slot); valid_objs s; tcb_replycap_slot \<noteq> 6; tcb_replycap_slot \<noteq> 5; tcb_replycap_slot \<noteq> tcb_ipcbuffer_slot; tcb_replycap_slot \<noteq> tcb_caller_slot; offset = tcb_replycap_slot; transform_cap (tcb_reply x2a) = x2\<rbrakk> \<Longrightarrow> \<exists>b. (ptr, tcb_replycap_slot) = transform_cslot_ptr (ptr, b) \<and> (\<exists>get. (\<exists>set restr. tcb_cap_cases b = Some (get, set, restr)) \<and> P (transform_cap (get x2a)))
 6. \<And>x2 ptr offset x2a etcb. \<lbrakk>kheap s ptr = Some (TCB x2a); ptr \<noteq> idle_thread s; ekheap s ptr = Some etcb; cap_counts x2; P x2; slot = (ptr, tcb_vspace_slot); valid_objs s; tcb_vspace_slot \<noteq> 6; tcb_vspace_slot \<noteq> 5; tcb_vspace_slot \<noteq> tcb_ipcbuffer_slot; tcb_vspace_slot \<noteq> tcb_caller_slot; tcb_vspace_slot \<noteq> tcb_replycap_slot; offset = tcb_vspace_slot; transform_cap (tcb_vtable x2a) = x2\<rbrakk> \<Longrightarrow> \<exists>b. (ptr, tcb_vspace_slot) = transform_cslot_ptr (ptr, b) \<and> (\<exists>get. (\<exists>set restr. tcb_cap_cases b = Some (get, set, restr)) \<and> P (transform_cap (get x2a)))
 7. \<And>x2 ptr offset x2a etcb. \<lbrakk>kheap s ptr = Some (TCB x2a); ptr \<noteq> idle_thread s; ekheap s ptr = Some etcb; cap_counts x2; P x2; slot = (ptr, tcb_cspace_slot); valid_objs s; tcb_cspace_slot \<noteq> 6; tcb_cspace_slot \<noteq> 5; tcb_cspace_slot \<noteq> tcb_ipcbuffer_slot; tcb_cspace_slot \<noteq> tcb_caller_slot; tcb_cspace_slot \<noteq> tcb_replycap_slot; tcb_cspace_slot \<noteq> tcb_vspace_slot; offset = tcb_cspace_slot; transform_cap (tcb_ctable x2a) = x2\<rbrakk> \<Longrightarrow> \<exists>b. (ptr, tcb_cspace_slot) = transform_cslot_ptr (ptr, b) \<and> (\<exists>get. (\<exists>set restr. tcb_cap_cases b = Some (get, set, restr)) \<and> P (transform_cap (get x2a)))
 8. \<And>x2 ptr offset x3 x5. \<lbrakk>cap_counts x2; P x2; slot = (ptr, offset); valid_objs s; valid_etcbs s; cdl_tcb_caps x3 offset = Some x2; kheap s ptr = Some (ArchObj x5); ptr \<noteq> idle_thread s; (case x5 of ASIDPool ap \<Rightarrow> AsidPool \<lparr>cdl_asid_pool_caps = transform_asid_pool_contents ap\<rparr> | arch_kernel_obj.PageTable ptx \<Rightarrow> cdl_object.PageTable \<lparr>cdl_page_table_caps = transform_page_table_contents ptx\<rparr> | arch_kernel_obj.PageDirectory pd \<Rightarrow> cdl_object.PageDirectory \<lparr>cdl_page_directory_caps = transform_page_directory_contents pd\<rparr> | DataPage dev sz \<Rightarrow> Frame \<lparr>cdl_frame_size_bits = pageBitsForSize sz\<rparr>) = Tcb x3\<rbrakk> \<Longrightarrow> False
 9. \<And>x2 ptr offset x4 z. \<lbrakk>P x2; slot = (ptr, offset); valid_objs s; valid_etcbs s; cdl_cnode_caps x4 offset = Some x2; kheap s ptr = Some z; ptr \<noteq> idle_thread s; transform_object (machine_state s) ptr (ekheap s ptr) z = cdl_object.CNode x4\<rbrakk> \<Longrightarrow> \<exists>b. (ptr, offset) = transform_cslot_ptr (ptr, b) \<and> cte_wp_at (\<lambda>cap'. P (transform_cap cap')) (ptr, b) s
 10. \<And>x2 ptr offset x5 z. \<lbrakk>P x2; slot = (ptr, offset); valid_objs s; valid_etcbs s; cdl_asid_pool_caps x5 offset = Some x2; kheap s ptr = Some z; ptr \<noteq> idle_thread s; transform_object (machine_state s) ptr (ekheap s ptr) z = AsidPool x5\<rbrakk> \<Longrightarrow> \<exists>b. (ptr, offset) = transform_cslot_ptr (ptr, b) \<and> cte_wp_at (\<lambda>cap'. P (transform_cap cap')) (ptr, b) s
A total of 13 subgoals... proof (prove)
goal (12 subgoals):
 1. \<And>x2 ptr offset x2a etcb. \<lbrakk>kheap s ptr = Some (TCB x2a); ptr \<noteq> idle_thread s; ekheap s ptr = Some etcb; cap_counts x2; P x2; slot = (ptr, 5); valid_objs s; offset = 5; infer_tcb_pending_op ptr (tcb_state x2a) = x2\<rbrakk> \<Longrightarrow> \<exists>b. (ptr, 5) = transform_cslot_ptr (ptr, b) \<and> (\<exists>get. (\<exists>set restr. tcb_cap_cases b = Some (get, set, restr)) \<and> P (transform_cap (get x2a)))
 2. \<And>x2 ptr offset x2a etcb. \<lbrakk>kheap s ptr = Some (TCB x2a); ptr \<noteq> idle_thread s; ekheap s ptr = Some etcb; cap_counts x2; P x2; slot = (ptr, tcb_ipcbuffer_slot); valid_objs s; tcb_ipcbuffer_slot \<noteq> 6; tcb_ipcbuffer_slot \<noteq> 5; offset = tcb_ipcbuffer_slot; transform_cap (tcb_ipcframe x2a) = x2\<rbrakk> \<Longrightarrow> \<exists>b. (ptr, tcb_ipcbuffer_slot) = transform_cslot_ptr (ptr, b) \<and> (\<exists>get. (\<exists>set restr. tcb_cap_cases b = Some (get, set, restr)) \<and> P (transform_cap (get x2a)))
 3. \<And>x2 ptr offset x2a etcb. \<lbrakk>kheap s ptr = Some (TCB x2a); ptr \<noteq> idle_thread s; ekheap s ptr = Some etcb; cap_counts x2; P x2; slot = (ptr, tcb_caller_slot); valid_objs s; tcb_caller_slot \<noteq> 6; tcb_caller_slot \<noteq> 5; tcb_caller_slot \<noteq> tcb_ipcbuffer_slot; offset = tcb_caller_slot; transform_cap (tcb_caller x2a) = x2\<rbrakk> \<Longrightarrow> \<exists>b. (ptr, tcb_caller_slot) = transform_cslot_ptr (ptr, b) \<and> (\<exists>get. (\<exists>set restr. tcb_cap_cases b = Some (get, set, restr)) \<and> P (transform_cap (get x2a)))
 4. \<And>x2 ptr offset x2a etcb. \<lbrakk>kheap s ptr = Some (TCB x2a); ptr \<noteq> idle_thread s; ekheap s ptr = Some etcb; cap_counts x2; P x2; slot = (ptr, tcb_replycap_slot); valid_objs s; tcb_replycap_slot \<noteq> 6; tcb_replycap_slot \<noteq> 5; tcb_replycap_slot \<noteq> tcb_ipcbuffer_slot; tcb_replycap_slot \<noteq> tcb_caller_slot; offset = tcb_replycap_slot; transform_cap (tcb_reply x2a) = x2\<rbrakk> \<Longrightarrow> \<exists>b. (ptr, tcb_replycap_slot) = transform_cslot_ptr (ptr, b) \<and> (\<exists>get. (\<exists>set restr. tcb_cap_cases b = Some (get, set, restr)) \<and> P (transform_cap (get x2a)))
 5. \<And>x2 ptr offset x2a etcb. \<lbrakk>kheap s ptr = Some (TCB x2a); ptr \<noteq> idle_thread s; ekheap s ptr = Some etcb; cap_counts x2; P x2; slot = (ptr, tcb_vspace_slot); valid_objs s; tcb_vspace_slot \<noteq> 6; tcb_vspace_slot \<noteq> 5; tcb_vspace_slot \<noteq> tcb_ipcbuffer_slot; tcb_vspace_slot \<noteq> tcb_caller_slot; tcb_vspace_slot \<noteq> tcb_replycap_slot; offset = tcb_vspace_slot; transform_cap (tcb_vtable x2a) = x2\<rbrakk> \<Longrightarrow> \<exists>b. (ptr, tcb_vspace_slot) = transform_cslot_ptr (ptr, b) \<and> (\<exists>get. (\<exists>set restr. tcb_cap_cases b = Some (get, set, restr)) \<and> P (transform_cap (get x2a)))
 6. \<And>x2 ptr offset x2a etcb. \<lbrakk>kheap s ptr = Some (TCB x2a); ptr \<noteq> idle_thread s; ekheap s ptr = Some etcb; cap_counts x2; P x2; slot = (ptr, tcb_cspace_slot); valid_objs s; tcb_cspace_slot \<noteq> 6; tcb_cspace_slot \<noteq> 5; tcb_cspace_slot \<noteq> tcb_ipcbuffer_slot; tcb_cspace_slot \<noteq> tcb_caller_slot; tcb_cspace_slot \<noteq> tcb_replycap_slot; tcb_cspace_slot \<noteq> tcb_vspace_slot; offset = tcb_cspace_slot; transform_cap (tcb_ctable x2a) = x2\<rbrakk> \<Longrightarrow> \<exists>b. (ptr, tcb_cspace_slot) = transform_cslot_ptr (ptr, b) \<and> (\<exists>get. (\<exists>set restr. tcb_cap_cases b = Some (get, set, restr)) \<and> P (transform_cap (get x2a)))
 7. \<And>x2 ptr offset x3 x5. \<lbrakk>cap_counts x2; P x2; slot = (ptr, offset); valid_objs s; valid_etcbs s; cdl_tcb_caps x3 offset = Some x2; kheap s ptr = Some (ArchObj x5); ptr \<noteq> idle_thread s; (case x5 of ASIDPool ap \<Rightarrow> AsidPool \<lparr>cdl_asid_pool_caps = transform_asid_pool_contents ap\<rparr> | arch_kernel_obj.PageTable ptx \<Rightarrow> cdl_object.PageTable \<lparr>cdl_page_table_caps = transform_page_table_contents ptx\<rparr> | arch_kernel_obj.PageDirectory pd \<Rightarrow> cdl_object.PageDirectory \<lparr>cdl_page_directory_caps = transform_page_directory_contents pd\<rparr> | DataPage dev sz \<Rightarrow> Frame \<lparr>cdl_frame_size_bits = pageBitsForSize sz\<rparr>) = Tcb x3\<rbrakk> \<Longrightarrow> False
 8. \<And>x2 ptr offset x4 z. \<lbrakk>P x2; slot = (ptr, offset); valid_objs s; valid_etcbs s; cdl_cnode_caps x4 offset = Some x2; kheap s ptr = Some z; ptr \<noteq> idle_thread s; transform_object (machine_state s) ptr (ekheap s ptr) z = cdl_object.CNode x4\<rbrakk> \<Longrightarrow> \<exists>b. (ptr, offset) = transform_cslot_ptr (ptr, b) \<and> cte_wp_at (\<lambda>cap'. P (transform_cap cap')) (ptr, b) s
 9. \<And>x2 ptr offset x5 z. \<lbrakk>P x2; slot = (ptr, offset); valid_objs s; valid_etcbs s; cdl_asid_pool_caps x5 offset = Some x2; kheap s ptr = Some z; ptr \<noteq> idle_thread s; transform_object (machine_state s) ptr (ekheap s ptr) z = AsidPool x5\<rbrakk> \<Longrightarrow> \<exists>b. (ptr, offset) = transform_cslot_ptr (ptr, b) \<and> cte_wp_at (\<lambda>cap'. P (transform_cap cap')) (ptr, b) s
 10. \<And>x2 ptr offset x6 z. \<lbrakk>P x2; slot = (ptr, offset); valid_objs s; valid_etcbs s; cdl_page_table_caps x6 offset = Some x2; kheap s ptr = Some z; ptr \<noteq> idle_thread s; transform_object (machine_state s) ptr (ekheap s ptr) z = cdl_object.PageTable x6\<rbrakk> \<Longrightarrow> \<exists>b. (ptr, offset) = transform_cslot_ptr (ptr, b) \<and> cte_wp_at (\<lambda>cap'. P (transform_cap cap')) (ptr, b) s
A total of 12 subgoals... proof (prove)
goal (11 subgoals):
 1. \<And>x2 ptr offset x2a etcb. \<lbrakk>kheap s ptr = Some (TCB x2a); ptr \<noteq> idle_thread s; ekheap s ptr = Some etcb; cap_counts x2; P x2; slot = (ptr, tcb_ipcbuffer_slot); valid_objs s; tcb_ipcbuffer_slot \<noteq> 6; tcb_ipcbuffer_slot \<noteq> 5; offset = tcb_ipcbuffer_slot; transform_cap (tcb_ipcframe x2a) = x2\<rbrakk> \<Longrightarrow> \<exists>b. (ptr, tcb_ipcbuffer_slot) = transform_cslot_ptr (ptr, b) \<and> (\<exists>get. (\<exists>set restr. tcb_cap_cases b = Some (get, set, restr)) \<and> P (transform_cap (get x2a)))
 2. \<And>x2 ptr offset x2a etcb. \<lbrakk>kheap s ptr = Some (TCB x2a); ptr \<noteq> idle_thread s; ekheap s ptr = Some etcb; cap_counts x2; P x2; slot = (ptr, tcb_caller_slot); valid_objs s; tcb_caller_slot \<noteq> 6; tcb_caller_slot \<noteq> 5; tcb_caller_slot \<noteq> tcb_ipcbuffer_slot; offset = tcb_caller_slot; transform_cap (tcb_caller x2a) = x2\<rbrakk> \<Longrightarrow> \<exists>b. (ptr, tcb_caller_slot) = transform_cslot_ptr (ptr, b) \<and> (\<exists>get. (\<exists>set restr. tcb_cap_cases b = Some (get, set, restr)) \<and> P (transform_cap (get x2a)))
 3. \<And>x2 ptr offset x2a etcb. \<lbrakk>kheap s ptr = Some (TCB x2a); ptr \<noteq> idle_thread s; ekheap s ptr = Some etcb; cap_counts x2; P x2; slot = (ptr, tcb_replycap_slot); valid_objs s; tcb_replycap_slot \<noteq> 6; tcb_replycap_slot \<noteq> 5; tcb_replycap_slot \<noteq> tcb_ipcbuffer_slot; tcb_replycap_slot \<noteq> tcb_caller_slot; offset = tcb_replycap_slot; transform_cap (tcb_reply x2a) = x2\<rbrakk> \<Longrightarrow> \<exists>b. (ptr, tcb_replycap_slot) = transform_cslot_ptr (ptr, b) \<and> (\<exists>get. (\<exists>set restr. tcb_cap_cases b = Some (get, set, restr)) \<and> P (transform_cap (get x2a)))
 4. \<And>x2 ptr offset x2a etcb. \<lbrakk>kheap s ptr = Some (TCB x2a); ptr \<noteq> idle_thread s; ekheap s ptr = Some etcb; cap_counts x2; P x2; slot = (ptr, tcb_vspace_slot); valid_objs s; tcb_vspace_slot \<noteq> 6; tcb_vspace_slot \<noteq> 5; tcb_vspace_slot \<noteq> tcb_ipcbuffer_slot; tcb_vspace_slot \<noteq> tcb_caller_slot; tcb_vspace_slot \<noteq> tcb_replycap_slot; offset = tcb_vspace_slot; transform_cap (tcb_vtable x2a) = x2\<rbrakk> \<Longrightarrow> \<exists>b. (ptr, tcb_vspace_slot) = transform_cslot_ptr (ptr, b) \<and> (\<exists>get. (\<exists>set restr. tcb_cap_cases b = Some (get, set, restr)) \<and> P (transform_cap (get x2a)))
 5. \<And>x2 ptr offset x2a etcb. \<lbrakk>kheap s ptr = Some (TCB x2a); ptr \<noteq> idle_thread s; ekheap s ptr = Some etcb; cap_counts x2; P x2; slot = (ptr, tcb_cspace_slot); valid_objs s; tcb_cspace_slot \<noteq> 6; tcb_cspace_slot \<noteq> 5; tcb_cspace_slot \<noteq> tcb_ipcbuffer_slot; tcb_cspace_slot \<noteq> tcb_caller_slot; tcb_cspace_slot \<noteq> tcb_replycap_slot; tcb_cspace_slot \<noteq> tcb_vspace_slot; offset = tcb_cspace_slot; transform_cap (tcb_ctable x2a) = x2\<rbrakk> \<Longrightarrow> \<exists>b. (ptr, tcb_cspace_slot) = transform_cslot_ptr (ptr, b) \<and> (\<exists>get. (\<exists>set restr. tcb_cap_cases b = Some (get, set, restr)) \<and> P (transform_cap (get x2a)))
 6. \<And>x2 ptr offset x3 x5. \<lbrakk>cap_counts x2; P x2; slot = (ptr, offset); valid_objs s; valid_etcbs s; cdl_tcb_caps x3 offset = Some x2; kheap s ptr = Some (ArchObj x5); ptr \<noteq> idle_thread s; (case x5 of ASIDPool ap \<Rightarrow> AsidPool \<lparr>cdl_asid_pool_caps = transform_asid_pool_contents ap\<rparr> | arch_kernel_obj.PageTable ptx \<Rightarrow> cdl_object.PageTable \<lparr>cdl_page_table_caps = transform_page_table_contents ptx\<rparr> | arch_kernel_obj.PageDirectory pd \<Rightarrow> cdl_object.PageDirectory \<lparr>cdl_page_directory_caps = transform_page_directory_contents pd\<rparr> | DataPage dev sz \<Rightarrow> Frame \<lparr>cdl_frame_size_bits = pageBitsForSize sz\<rparr>) = Tcb x3\<rbrakk> \<Longrightarrow> False
 7. \<And>x2 ptr offset x4 z. \<lbrakk>P x2; slot = (ptr, offset); valid_objs s; valid_etcbs s; cdl_cnode_caps x4 offset = Some x2; kheap s ptr = Some z; ptr \<noteq> idle_thread s; transform_object (machine_state s) ptr (ekheap s ptr) z = cdl_object.CNode x4\<rbrakk> \<Longrightarrow> \<exists>b. (ptr, offset) = transform_cslot_ptr (ptr, b) \<and> cte_wp_at (\<lambda>cap'. P (transform_cap cap')) (ptr, b) s
 8. \<And>x2 ptr offset x5 z. \<lbrakk>P x2; slot = (ptr, offset); valid_objs s; valid_etcbs s; cdl_asid_pool_caps x5 offset = Some x2; kheap s ptr = Some z; ptr \<noteq> idle_thread s; transform_object (machine_state s) ptr (ekheap s ptr) z = AsidPool x5\<rbrakk> \<Longrightarrow> \<exists>b. (ptr, offset) = transform_cslot_ptr (ptr, b) \<and> cte_wp_at (\<lambda>cap'. P (transform_cap cap')) (ptr, b) s
 9. \<And>x2 ptr offset x6 z. \<lbrakk>P x2; slot = (ptr, offset); valid_objs s; valid_etcbs s; cdl_page_table_caps x6 offset = Some x2; kheap s ptr = Some z; ptr \<noteq> idle_thread s; transform_object (machine_state s) ptr (ekheap s ptr) z = cdl_object.PageTable x6\<rbrakk> \<Longrightarrow> \<exists>b. (ptr, offset) = transform_cslot_ptr (ptr, b) \<and> cte_wp_at (\<lambda>cap'. P (transform_cap cap')) (ptr, b) s
 10. \<And>x2 ptr offset x7 z. \<lbrakk>P x2; slot = (ptr, offset); valid_objs s; valid_etcbs s; cdl_page_directory_caps x7 offset = Some x2; kheap s ptr = Some z; ptr \<noteq> idle_thread s; transform_object (machine_state s) ptr (ekheap s ptr) z = cdl_object.PageDirectory x7\<rbrakk> \<Longrightarrow> \<exists>b. (ptr, offset) = transform_cslot_ptr (ptr, b) \<and> cte_wp_at (\<lambda>cap'. P (transform_cap cap')) (ptr, b) s
A total of 11 subgoals... proof (prove)
using this:
(?a, tcb_cspace_slot) = transform_cslot_ptr (?a, tcb_cnode_index 0)
(?a, tcb_vspace_slot) = transform_cslot_ptr (?a, tcb_cnode_index (Suc 0))
(?a, tcb_replycap_slot) = transform_cslot_ptr (?a, tcb_cnode_index 2)
(?a, tcb_caller_slot) = transform_cslot_ptr (?a, tcb_cnode_index 3)
(?a, tcb_ipcbuffer_slot) = transform_cslot_ptr (?a, tcb_cnode_index 4)

goal (11 subgoals):
 1. \<And>x2 ptr offset x2a etcb. \<lbrakk>kheap s ptr = Some (TCB x2a); ptr \<noteq> idle_thread s; ekheap s ptr = Some etcb; cap_counts x2; P x2; slot = (ptr, tcb_ipcbuffer_slot); valid_objs s; tcb_ipcbuffer_slot \<noteq> 6; tcb_ipcbuffer_slot \<noteq> 5; offset = tcb_ipcbuffer_slot; transform_cap (tcb_ipcframe x2a) = x2\<rbrakk> \<Longrightarrow> \<exists>b. (ptr, tcb_ipcbuffer_slot) = transform_cslot_ptr (ptr, b) \<and> (\<exists>get. (\<exists>set restr. tcb_cap_cases b = Some (get, set, restr)) \<and> P (transform_cap (get x2a)))
 2. \<And>x2 ptr offset x2a etcb. \<lbrakk>kheap s ptr = Some (TCB x2a); ptr \<noteq> idle_thread s; ekheap s ptr = Some etcb; cap_counts x2; P x2; slot = (ptr, tcb_caller_slot); valid_objs s; tcb_caller_slot \<noteq> 6; tcb_caller_slot \<noteq> 5; tcb_caller_slot \<noteq> tcb_ipcbuffer_slot; offset = tcb_caller_slot; transform_cap (tcb_caller x2a) = x2\<rbrakk> \<Longrightarrow> \<exists>b. (ptr, tcb_caller_slot) = transform_cslot_ptr (ptr, b) \<and> (\<exists>get. (\<exists>set restr. tcb_cap_cases b = Some (get, set, restr)) \<and> P (transform_cap (get x2a)))
 3. \<And>x2 ptr offset x2a etcb. \<lbrakk>kheap s ptr = Some (TCB x2a); ptr \<noteq> idle_thread s; ekheap s ptr = Some etcb; cap_counts x2; P x2; slot = (ptr, tcb_replycap_slot); valid_objs s; tcb_replycap_slot \<noteq> 6; tcb_replycap_slot \<noteq> 5; tcb_replycap_slot \<noteq> tcb_ipcbuffer_slot; tcb_replycap_slot \<noteq> tcb_caller_slot; offset = tcb_replycap_slot; transform_cap (tcb_reply x2a) = x2\<rbrakk> \<Longrightarrow> \<exists>b. (ptr, tcb_replycap_slot) = transform_cslot_ptr (ptr, b) \<and> (\<exists>get. (\<exists>set restr. tcb_cap_cases b = Some (get, set, restr)) \<and> P (transform_cap (get x2a)))
 4. \<And>x2 ptr offset x2a etcb. \<lbrakk>kheap s ptr = Some (TCB x2a); ptr \<noteq> idle_thread s; ekheap s ptr = Some etcb; cap_counts x2; P x2; slot = (ptr, tcb_vspace_slot); valid_objs s; tcb_vspace_slot \<noteq> 6; tcb_vspace_slot \<noteq> 5; tcb_vspace_slot \<noteq> tcb_ipcbuffer_slot; tcb_vspace_slot \<noteq> tcb_caller_slot; tcb_vspace_slot \<noteq> tcb_replycap_slot; offset = tcb_vspace_slot; transform_cap (tcb_vtable x2a) = x2\<rbrakk> \<Longrightarrow> \<exists>b. (ptr, tcb_vspace_slot) = transform_cslot_ptr (ptr, b) \<and> (\<exists>get. (\<exists>set restr. tcb_cap_cases b = Some (get, set, restr)) \<and> P (transform_cap (get x2a)))
 5. \<And>x2 ptr offset x2a etcb. \<lbrakk>kheap s ptr = Some (TCB x2a); ptr \<noteq> idle_thread s; ekheap s ptr = Some etcb; cap_counts x2; P x2; slot = (ptr, tcb_cspace_slot); valid_objs s; tcb_cspace_slot \<noteq> 6; tcb_cspace_slot \<noteq> 5; tcb_cspace_slot \<noteq> tcb_ipcbuffer_slot; tcb_cspace_slot \<noteq> tcb_caller_slot; tcb_cspace_slot \<noteq> tcb_replycap_slot; tcb_cspace_slot \<noteq> tcb_vspace_slot; offset = tcb_cspace_slot; transform_cap (tcb_ctable x2a) = x2\<rbrakk> \<Longrightarrow> \<exists>b. (ptr, tcb_cspace_slot) = transform_cslot_ptr (ptr, b) \<and> (\<exists>get. (\<exists>set restr. tcb_cap_cases b = Some (get, set, restr)) \<and> P (transform_cap (get x2a)))
 6. \<And>x2 ptr offset x3 x5. \<lbrakk>cap_counts x2; P x2; slot = (ptr, offset); valid_objs s; valid_etcbs s; cdl_tcb_caps x3 offset = Some x2; kheap s ptr = Some (ArchObj x5); ptr \<noteq> idle_thread s; (case x5 of ASIDPool ap \<Rightarrow> AsidPool \<lparr>cdl_asid_pool_caps = transform_asid_pool_contents ap\<rparr> | arch_kernel_obj.PageTable ptx \<Rightarrow> cdl_object.PageTable \<lparr>cdl_page_table_caps = transform_page_table_contents ptx\<rparr> | arch_kernel_obj.PageDirectory pd \<Rightarrow> cdl_object.PageDirectory \<lparr>cdl_page_directory_caps = transform_page_directory_contents pd\<rparr> | DataPage dev sz \<Rightarrow> Frame \<lparr>cdl_frame_size_bits = pageBitsForSize sz\<rparr>) = Tcb x3\<rbrakk> \<Longrightarrow> False
 7. \<And>x2 ptr offset x4 z. \<lbrakk>P x2; slot = (ptr, offset); valid_objs s; valid_etcbs s; cdl_cnode_caps x4 offset = Some x2; kheap s ptr = Some z; ptr \<noteq> idle_thread s; transform_object (machine_state s) ptr (ekheap s ptr) z = cdl_object.CNode x4\<rbrakk> \<Longrightarrow> \<exists>b. (ptr, offset) = transform_cslot_ptr (ptr, b) \<and> cte_wp_at (\<lambda>cap'. P (transform_cap cap')) (ptr, b) s
 8. \<And>x2 ptr offset x5 z. \<lbrakk>P x2; slot = (ptr, offset); valid_objs s; valid_etcbs s; cdl_asid_pool_caps x5 offset = Some x2; kheap s ptr = Some z; ptr \<noteq> idle_thread s; transform_object (machine_state s) ptr (ekheap s ptr) z = AsidPool x5\<rbrakk> \<Longrightarrow> \<exists>b. (ptr, offset) = transform_cslot_ptr (ptr, b) \<and> cte_wp_at (\<lambda>cap'. P (transform_cap cap')) (ptr, b) s
 9. \<And>x2 ptr offset x6 z. \<lbrakk>P x2; slot = (ptr, offset); valid_objs s; valid_etcbs s; cdl_page_table_caps x6 offset = Some x2; kheap s ptr = Some z; ptr \<noteq> idle_thread s; transform_object (machine_state s) ptr (ekheap s ptr) z = cdl_object.PageTable x6\<rbrakk> \<Longrightarrow> \<exists>b. (ptr, offset) = transform_cslot_ptr (ptr, b) \<and> cte_wp_at (\<lambda>cap'. P (transform_cap cap')) (ptr, b) s
 10. \<And>x2 ptr offset x7 z. \<lbrakk>P x2; slot = (ptr, offset); valid_objs s; valid_etcbs s; cdl_page_directory_caps x7 offset = Some x2; kheap s ptr = Some z; ptr \<noteq> idle_thread s; transform_object (machine_state s) ptr (ekheap s ptr) z = cdl_object.PageDirectory x7\<rbrakk> \<Longrightarrow> \<exists>b. (ptr, offset) = transform_cslot_ptr (ptr, b) \<and> cte_wp_at (\<lambda>cap'. P (transform_cap cap')) (ptr, b) s
A total of 11 subgoals... proof (prove)
goal (11 subgoals):
 1. \<And>x2 ptr offset x2a etcb. \<lbrakk>kheap s ptr = Some (TCB x2a); ptr \<noteq> idle_thread s; ekheap s ptr = Some etcb; cap_counts x2; P x2; slot = (ptr, tcb_ipcbuffer_slot); valid_objs s; tcb_ipcbuffer_slot \<noteq> 6; tcb_ipcbuffer_slot \<noteq> 5; offset = tcb_ipcbuffer_slot; transform_cap (tcb_ipcframe x2a) = x2; \<And>a. (a, tcb_cspace_slot) = transform_cslot_ptr (a, tcb_cnode_index 0); \<And>a. (a, tcb_vspace_slot) = transform_cslot_ptr (a, tcb_cnode_index (Suc 0)); \<And>a. (a, tcb_replycap_slot) = transform_cslot_ptr (a, tcb_cnode_index 2); \<And>a. (a, tcb_caller_slot) = transform_cslot_ptr (a, tcb_cnode_index 3); \<And>a. (a, tcb_ipcbuffer_slot) = transform_cslot_ptr (a, tcb_cnode_index 4)\<rbrakk> \<Longrightarrow> (ptr, tcb_ipcbuffer_slot) = transform_cslot_ptr (ptr, tcb_cnode_index 4) \<and> (\<exists>get. (\<exists>set restr. tcb_cap_cases (tcb_cnode_index 4) = Some (get, set, restr)) \<and> P (transform_cap (get x2a)))
 2. \<And>x2 ptr offset x2a etcb. \<lbrakk>kheap s ptr = Some (TCB x2a); ptr \<noteq> idle_thread s; ekheap s ptr = Some etcb; cap_counts x2; P x2; slot = (ptr, tcb_caller_slot); valid_objs s; tcb_caller_slot \<noteq> 6; tcb_caller_slot \<noteq> 5; tcb_caller_slot \<noteq> tcb_ipcbuffer_slot; offset = tcb_caller_slot; transform_cap (tcb_caller x2a) = x2\<rbrakk> \<Longrightarrow> \<exists>b. (ptr, tcb_caller_slot) = transform_cslot_ptr (ptr, b) \<and> (\<exists>get. (\<exists>set restr. tcb_cap_cases b = Some (get, set, restr)) \<and> P (transform_cap (get x2a)))
 3. \<And>x2 ptr offset x2a etcb. \<lbrakk>kheap s ptr = Some (TCB x2a); ptr \<noteq> idle_thread s; ekheap s ptr = Some etcb; cap_counts x2; P x2; slot = (ptr, tcb_replycap_slot); valid_objs s; tcb_replycap_slot \<noteq> 6; tcb_replycap_slot \<noteq> 5; tcb_replycap_slot \<noteq> tcb_ipcbuffer_slot; tcb_replycap_slot \<noteq> tcb_caller_slot; offset = tcb_replycap_slot; transform_cap (tcb_reply x2a) = x2\<rbrakk> \<Longrightarrow> \<exists>b. (ptr, tcb_replycap_slot) = transform_cslot_ptr (ptr, b) \<and> (\<exists>get. (\<exists>set restr. tcb_cap_cases b = Some (get, set, restr)) \<and> P (transform_cap (get x2a)))
 4. \<And>x2 ptr offset x2a etcb. \<lbrakk>kheap s ptr = Some (TCB x2a); ptr \<noteq> idle_thread s; ekheap s ptr = Some etcb; cap_counts x2; P x2; slot = (ptr, tcb_vspace_slot); valid_objs s; tcb_vspace_slot \<noteq> 6; tcb_vspace_slot \<noteq> 5; tcb_vspace_slot \<noteq> tcb_ipcbuffer_slot; tcb_vspace_slot \<noteq> tcb_caller_slot; tcb_vspace_slot \<noteq> tcb_replycap_slot; offset = tcb_vspace_slot; transform_cap (tcb_vtable x2a) = x2\<rbrakk> \<Longrightarrow> \<exists>b. (ptr, tcb_vspace_slot) = transform_cslot_ptr (ptr, b) \<and> (\<exists>get. (\<exists>set restr. tcb_cap_cases b = Some (get, set, restr)) \<and> P (transform_cap (get x2a)))
 5. \<And>x2 ptr offset x2a etcb. \<lbrakk>kheap s ptr = Some (TCB x2a); ptr \<noteq> idle_thread s; ekheap s ptr = Some etcb; cap_counts x2; P x2; slot = (ptr, tcb_cspace_slot); valid_objs s; tcb_cspace_slot \<noteq> 6; tcb_cspace_slot \<noteq> 5; tcb_cspace_slot \<noteq> tcb_ipcbuffer_slot; tcb_cspace_slot \<noteq> tcb_caller_slot; tcb_cspace_slot \<noteq> tcb_replycap_slot; tcb_cspace_slot \<noteq> tcb_vspace_slot; offset = tcb_cspace_slot; transform_cap (tcb_ctable x2a) = x2\<rbrakk> \<Longrightarrow> \<exists>b. (ptr, tcb_cspace_slot) = transform_cslot_ptr (ptr, b) \<and> (\<exists>get. (\<exists>set restr. tcb_cap_cases b = Some (get, set, restr)) \<and> P (transform_cap (get x2a)))
 6. \<And>x2 ptr offset x3 x5. \<lbrakk>cap_counts x2; P x2; slot = (ptr, offset); valid_objs s; valid_etcbs s; cdl_tcb_caps x3 offset = Some x2; kheap s ptr = Some (ArchObj x5); ptr \<noteq> idle_thread s; (case x5 of ASIDPool ap \<Rightarrow> AsidPool \<lparr>cdl_asid_pool_caps = transform_asid_pool_contents ap\<rparr> | arch_kernel_obj.PageTable ptx \<Rightarrow> cdl_object.PageTable \<lparr>cdl_page_table_caps = transform_page_table_contents ptx\<rparr> | arch_kernel_obj.PageDirectory pd \<Rightarrow> cdl_object.PageDirectory \<lparr>cdl_page_directory_caps = transform_page_directory_contents pd\<rparr> | DataPage dev sz \<Rightarrow> Frame \<lparr>cdl_frame_size_bits = pageBitsForSize sz\<rparr>) = Tcb x3\<rbrakk> \<Longrightarrow> False
 7. \<And>x2 ptr offset x4 z. \<lbrakk>P x2; slot = (ptr, offset); valid_objs s; valid_etcbs s; cdl_cnode_caps x4 offset = Some x2; kheap s ptr = Some z; ptr \<noteq> idle_thread s; transform_object (machine_state s) ptr (ekheap s ptr) z = cdl_object.CNode x4\<rbrakk> \<Longrightarrow> \<exists>b. (ptr, offset) = transform_cslot_ptr (ptr, b) \<and> cte_wp_at (\<lambda>cap'. P (transform_cap cap')) (ptr, b) s
 8. \<And>x2 ptr offset x5 z. \<lbrakk>P x2; slot = (ptr, offset); valid_objs s; valid_etcbs s; cdl_asid_pool_caps x5 offset = Some x2; kheap s ptr = Some z; ptr \<noteq> idle_thread s; transform_object (machine_state s) ptr (ekheap s ptr) z = AsidPool x5\<rbrakk> \<Longrightarrow> \<exists>b. (ptr, offset) = transform_cslot_ptr (ptr, b) \<and> cte_wp_at (\<lambda>cap'. P (transform_cap cap')) (ptr, b) s
 9. \<And>x2 ptr offset x6 z. \<lbrakk>P x2; slot = (ptr, offset); valid_objs s; valid_etcbs s; cdl_page_table_caps x6 offset = Some x2; kheap s ptr = Some z; ptr \<noteq> idle_thread s; transform_object (machine_state s) ptr (ekheap s ptr) z = cdl_object.PageTable x6\<rbrakk> \<Longrightarrow> \<exists>b. (ptr, offset) = transform_cslot_ptr (ptr, b) \<and> cte_wp_at (\<lambda>cap'. P (transform_cap cap')) (ptr, b) s
 10. \<And>x2 ptr offset x7 z. \<lbrakk>P x2; slot = (ptr, offset); valid_objs s; valid_etcbs s; cdl_page_directory_caps x7 offset = Some x2; kheap s ptr = Some z; ptr \<noteq> idle_thread s; transform_object (machine_state s) ptr (ekheap s ptr) z = cdl_object.PageDirectory x7\<rbrakk> \<Longrightarrow> \<exists>b. (ptr, offset) = transform_cslot_ptr (ptr, b) \<and> cte_wp_at (\<lambda>cap'. P (transform_cap cap')) (ptr, b) s
A total of 11 subgoals... proof (prove)
goal (10 subgoals):
 1. \<And>x2 ptr offset x2a etcb. \<lbrakk>kheap s ptr = Some (TCB x2a); ptr \<noteq> idle_thread s; ekheap s ptr = Some etcb; cap_counts x2; P x2; slot = (ptr, tcb_caller_slot); valid_objs s; tcb_caller_slot \<noteq> 6; tcb_caller_slot \<noteq> 5; tcb_caller_slot \<noteq> tcb_ipcbuffer_slot; offset = tcb_caller_slot; transform_cap (tcb_caller x2a) = x2\<rbrakk> \<Longrightarrow> \<exists>b. (ptr, tcb_caller_slot) = transform_cslot_ptr (ptr, b) \<and> (\<exists>get. (\<exists>set restr. tcb_cap_cases b = Some (get, set, restr)) \<and> P (transform_cap (get x2a)))
 2. \<And>x2 ptr offset x2a etcb. \<lbrakk>kheap s ptr = Some (TCB x2a); ptr \<noteq> idle_thread s; ekheap s ptr = Some etcb; cap_counts x2; P x2; slot = (ptr, tcb_replycap_slot); valid_objs s; tcb_replycap_slot \<noteq> 6; tcb_replycap_slot \<noteq> 5; tcb_replycap_slot \<noteq> tcb_ipcbuffer_slot; tcb_replycap_slot \<noteq> tcb_caller_slot; offset = tcb_replycap_slot; transform_cap (tcb_reply x2a) = x2\<rbrakk> \<Longrightarrow> \<exists>b. (ptr, tcb_replycap_slot) = transform_cslot_ptr (ptr, b) \<and> (\<exists>get. (\<exists>set restr. tcb_cap_cases b = Some (get, set, restr)) \<and> P (transform_cap (get x2a)))
 3. \<And>x2 ptr offset x2a etcb. \<lbrakk>kheap s ptr = Some (TCB x2a); ptr \<noteq> idle_thread s; ekheap s ptr = Some etcb; cap_counts x2; P x2; slot = (ptr, tcb_vspace_slot); valid_objs s; tcb_vspace_slot \<noteq> 6; tcb_vspace_slot \<noteq> 5; tcb_vspace_slot \<noteq> tcb_ipcbuffer_slot; tcb_vspace_slot \<noteq> tcb_caller_slot; tcb_vspace_slot \<noteq> tcb_replycap_slot; offset = tcb_vspace_slot; transform_cap (tcb_vtable x2a) = x2\<rbrakk> \<Longrightarrow> \<exists>b. (ptr, tcb_vspace_slot) = transform_cslot_ptr (ptr, b) \<and> (\<exists>get. (\<exists>set restr. tcb_cap_cases b = Some (get, set, restr)) \<and> P (transform_cap (get x2a)))
 4. \<And>x2 ptr offset x2a etcb. \<lbrakk>kheap s ptr = Some (TCB x2a); ptr \<noteq> idle_thread s; ekheap s ptr = Some etcb; cap_counts x2; P x2; slot = (ptr, tcb_cspace_slot); valid_objs s; tcb_cspace_slot \<noteq> 6; tcb_cspace_slot \<noteq> 5; tcb_cspace_slot \<noteq> tcb_ipcbuffer_slot; tcb_cspace_slot \<noteq> tcb_caller_slot; tcb_cspace_slot \<noteq> tcb_replycap_slot; tcb_cspace_slot \<noteq> tcb_vspace_slot; offset = tcb_cspace_slot; transform_cap (tcb_ctable x2a) = x2\<rbrakk> \<Longrightarrow> \<exists>b. (ptr, tcb_cspace_slot) = transform_cslot_ptr (ptr, b) \<and> (\<exists>get. (\<exists>set restr. tcb_cap_cases b = Some (get, set, restr)) \<and> P (transform_cap (get x2a)))
 5. \<And>x2 ptr offset x3 x5. \<lbrakk>cap_counts x2; P x2; slot = (ptr, offset); valid_objs s; valid_etcbs s; cdl_tcb_caps x3 offset = Some x2; kheap s ptr = Some (ArchObj x5); ptr \<noteq> idle_thread s; (case x5 of ASIDPool ap \<Rightarrow> AsidPool \<lparr>cdl_asid_pool_caps = transform_asid_pool_contents ap\<rparr> | arch_kernel_obj.PageTable ptx \<Rightarrow> cdl_object.PageTable \<lparr>cdl_page_table_caps = transform_page_table_contents ptx\<rparr> | arch_kernel_obj.PageDirectory pd \<Rightarrow> cdl_object.PageDirectory \<lparr>cdl_page_directory_caps = transform_page_directory_contents pd\<rparr> | DataPage dev sz \<Rightarrow> Frame \<lparr>cdl_frame_size_bits = pageBitsForSize sz\<rparr>) = Tcb x3\<rbrakk> \<Longrightarrow> False
 6. \<And>x2 ptr offset x4 z. \<lbrakk>P x2; slot = (ptr, offset); valid_objs s; valid_etcbs s; cdl_cnode_caps x4 offset = Some x2; kheap s ptr = Some z; ptr \<noteq> idle_thread s; transform_object (machine_state s) ptr (ekheap s ptr) z = cdl_object.CNode x4\<rbrakk> \<Longrightarrow> \<exists>b. (ptr, offset) = transform_cslot_ptr (ptr, b) \<and> cte_wp_at (\<lambda>cap'. P (transform_cap cap')) (ptr, b) s
 7. \<And>x2 ptr offset x5 z. \<lbrakk>P x2; slot = (ptr, offset); valid_objs s; valid_etcbs s; cdl_asid_pool_caps x5 offset = Some x2; kheap s ptr = Some z; ptr \<noteq> idle_thread s; transform_object (machine_state s) ptr (ekheap s ptr) z = AsidPool x5\<rbrakk> \<Longrightarrow> \<exists>b. (ptr, offset) = transform_cslot_ptr (ptr, b) \<and> cte_wp_at (\<lambda>cap'. P (transform_cap cap')) (ptr, b) s
 8. \<And>x2 ptr offset x6 z. \<lbrakk>P x2; slot = (ptr, offset); valid_objs s; valid_etcbs s; cdl_page_table_caps x6 offset = Some x2; kheap s ptr = Some z; ptr \<noteq> idle_thread s; transform_object (machine_state s) ptr (ekheap s ptr) z = cdl_object.PageTable x6\<rbrakk> \<Longrightarrow> \<exists>b. (ptr, offset) = transform_cslot_ptr (ptr, b) \<and> cte_wp_at (\<lambda>cap'. P (transform_cap cap')) (ptr, b) s
 9. \<And>x2 ptr offset x7 z. \<lbrakk>P x2; slot = (ptr, offset); valid_objs s; valid_etcbs s; cdl_page_directory_caps x7 offset = Some x2; kheap s ptr = Some z; ptr \<noteq> idle_thread s; transform_object (machine_state s) ptr (ekheap s ptr) z = cdl_object.PageDirectory x7\<rbrakk> \<Longrightarrow> \<exists>b. (ptr, offset) = transform_cslot_ptr (ptr, b) \<and> cte_wp_at (\<lambda>cap'. P (transform_cap cap')) (ptr, b) s
 10. \<And>x2 ptr offset x10 z. \<lbrakk>P x2; slot = (ptr, offset); valid_objs s; valid_etcbs s; cdl_irq_node_caps x10 offset = Some x2; kheap s ptr = Some z; ptr \<noteq> idle_thread s; transform_object (machine_state s) ptr (ekheap s ptr) z = IRQNode x10\<rbrakk> \<Longrightarrow> \<exists>b. (ptr, offset) = transform_cslot_ptr (ptr, b) \<and> cte_wp_at (\<lambda>cap'. P (transform_cap cap')) (ptr, b) s proof (prove)
using this:
(?a, tcb_cspace_slot) = transform_cslot_ptr (?a, tcb_cnode_index 0)
(?a, tcb_vspace_slot) = transform_cslot_ptr (?a, tcb_cnode_index (Suc 0))
(?a, tcb_replycap_slot) = transform_cslot_ptr (?a, tcb_cnode_index 2)
(?a, tcb_caller_slot) = transform_cslot_ptr (?a, tcb_cnode_index 3)
(?a, tcb_ipcbuffer_slot) = transform_cslot_ptr (?a, tcb_cnode_index 4)

goal (10 subgoals):
 1. \<And>x2 ptr offset x2a etcb. \<lbrakk>kheap s ptr = Some (TCB x2a); ptr \<noteq> idle_thread s; ekheap s ptr = Some etcb; cap_counts x2; P x2; slot = (ptr, tcb_caller_slot); valid_objs s; tcb_caller_slot \<noteq> 6; tcb_caller_slot \<noteq> 5; tcb_caller_slot \<noteq> tcb_ipcbuffer_slot; offset = tcb_caller_slot; transform_cap (tcb_caller x2a) = x2\<rbrakk> \<Longrightarrow> \<exists>b. (ptr, tcb_caller_slot) = transform_cslot_ptr (ptr, b) \<and> (\<exists>get. (\<exists>set restr. tcb_cap_cases b = Some (get, set, restr)) \<and> P (transform_cap (get x2a)))
 2. \<And>x2 ptr offset x2a etcb. \<lbrakk>kheap s ptr = Some (TCB x2a); ptr \<noteq> idle_thread s; ekheap s ptr = Some etcb; cap_counts x2; P x2; slot = (ptr, tcb_replycap_slot); valid_objs s; tcb_replycap_slot \<noteq> 6; tcb_replycap_slot \<noteq> 5; tcb_replycap_slot \<noteq> tcb_ipcbuffer_slot; tcb_replycap_slot \<noteq> tcb_caller_slot; offset = tcb_replycap_slot; transform_cap (tcb_reply x2a) = x2\<rbrakk> \<Longrightarrow> \<exists>b. (ptr, tcb_replycap_slot) = transform_cslot_ptr (ptr, b) \<and> (\<exists>get. (\<exists>set restr. tcb_cap_cases b = Some (get, set, restr)) \<and> P (transform_cap (get x2a)))
 3. \<And>x2 ptr offset x2a etcb. \<lbrakk>kheap s ptr = Some (TCB x2a); ptr \<noteq> idle_thread s; ekheap s ptr = Some etcb; cap_counts x2; P x2; slot = (ptr, tcb_vspace_slot); valid_objs s; tcb_vspace_slot \<noteq> 6; tcb_vspace_slot \<noteq> 5; tcb_vspace_slot \<noteq> tcb_ipcbuffer_slot; tcb_vspace_slot \<noteq> tcb_caller_slot; tcb_vspace_slot \<noteq> tcb_replycap_slot; offset = tcb_vspace_slot; transform_cap (tcb_vtable x2a) = x2\<rbrakk> \<Longrightarrow> \<exists>b. (ptr, tcb_vspace_slot) = transform_cslot_ptr (ptr, b) \<and> (\<exists>get. (\<exists>set restr. tcb_cap_cases b = Some (get, set, restr)) \<and> P (transform_cap (get x2a)))
 4. \<And>x2 ptr offset x2a etcb. \<lbrakk>kheap s ptr = Some (TCB x2a); ptr \<noteq> idle_thread s; ekheap s ptr = Some etcb; cap_counts x2; P x2; slot = (ptr, tcb_cspace_slot); valid_objs s; tcb_cspace_slot \<noteq> 6; tcb_cspace_slot \<noteq> 5; tcb_cspace_slot \<noteq> tcb_ipcbuffer_slot; tcb_cspace_slot \<noteq> tcb_caller_slot; tcb_cspace_slot \<noteq> tcb_replycap_slot; tcb_cspace_slot \<noteq> tcb_vspace_slot; offset = tcb_cspace_slot; transform_cap (tcb_ctable x2a) = x2\<rbrakk> \<Longrightarrow> \<exists>b. (ptr, tcb_cspace_slot) = transform_cslot_ptr (ptr, b) \<and> (\<exists>get. (\<exists>set restr. tcb_cap_cases b = Some (get, set, restr)) \<and> P (transform_cap (get x2a)))
 5. \<And>x2 ptr offset x3 x5. \<lbrakk>cap_counts x2; P x2; slot = (ptr, offset); valid_objs s; valid_etcbs s; cdl_tcb_caps x3 offset = Some x2; kheap s ptr = Some (ArchObj x5); ptr \<noteq> idle_thread s; (case x5 of ASIDPool ap \<Rightarrow> AsidPool \<lparr>cdl_asid_pool_caps = transform_asid_pool_contents ap\<rparr> | arch_kernel_obj.PageTable ptx \<Rightarrow> cdl_object.PageTable \<lparr>cdl_page_table_caps = transform_page_table_contents ptx\<rparr> | arch_kernel_obj.PageDirectory pd \<Rightarrow> cdl_object.PageDirectory \<lparr>cdl_page_directory_caps = transform_page_directory_contents pd\<rparr> | DataPage dev sz \<Rightarrow> Frame \<lparr>cdl_frame_size_bits = pageBitsForSize sz\<rparr>) = Tcb x3\<rbrakk> \<Longrightarrow> False
 6. \<And>x2 ptr offset x4 z. \<lbrakk>P x2; slot = (ptr, offset); valid_objs s; valid_etcbs s; cdl_cnode_caps x4 offset = Some x2; kheap s ptr = Some z; ptr \<noteq> idle_thread s; transform_object (machine_state s) ptr (ekheap s ptr) z = cdl_object.CNode x4\<rbrakk> \<Longrightarrow> \<exists>b. (ptr, offset) = transform_cslot_ptr (ptr, b) \<and> cte_wp_at (\<lambda>cap'. P (transform_cap cap')) (ptr, b) s
 7. \<And>x2 ptr offset x5 z. \<lbrakk>P x2; slot = (ptr, offset); valid_objs s; valid_etcbs s; cdl_asid_pool_caps x5 offset = Some x2; kheap s ptr = Some z; ptr \<noteq> idle_thread s; transform_object (machine_state s) ptr (ekheap s ptr) z = AsidPool x5\<rbrakk> \<Longrightarrow> \<exists>b. (ptr, offset) = transform_cslot_ptr (ptr, b) \<and> cte_wp_at (\<lambda>cap'. P (transform_cap cap')) (ptr, b) s
 8. \<And>x2 ptr offset x6 z. \<lbrakk>P x2; slot = (ptr, offset); valid_objs s; valid_etcbs s; cdl_page_table_caps x6 offset = Some x2; kheap s ptr = Some z; ptr \<noteq> idle_thread s; transform_object (machine_state s) ptr (ekheap s ptr) z = cdl_object.PageTable x6\<rbrakk> \<Longrightarrow> \<exists>b. (ptr, offset) = transform_cslot_ptr (ptr, b) \<and> cte_wp_at (\<lambda>cap'. P (transform_cap cap')) (ptr, b) s
 9. \<And>x2 ptr offset x7 z. \<lbrakk>P x2; slot = (ptr, offset); valid_objs s; valid_etcbs s; cdl_page_directory_caps x7 offset = Some x2; kheap s ptr = Some z; ptr \<noteq> idle_thread s; transform_object (machine_state s) ptr (ekheap s ptr) z = cdl_object.PageDirectory x7\<rbrakk> \<Longrightarrow> \<exists>b. (ptr, offset) = transform_cslot_ptr (ptr, b) \<and> cte_wp_at (\<lambda>cap'. P (transform_cap cap')) (ptr, b) s
 10. \<And>x2 ptr offset x10 z. \<lbrakk>P x2; slot = (ptr, offset); valid_objs s; valid_etcbs s; cdl_irq_node_caps x10 offset = Some x2; kheap s ptr = Some z; ptr \<noteq> idle_thread s; transform_object (machine_state s) ptr (ekheap s ptr) z = IRQNode x10\<rbrakk> \<Longrightarrow> \<exists>b. (ptr, offset) = transform_cslot_ptr (ptr, b) \<and> cte_wp_at (\<lambda>cap'. P (transform_cap cap')) (ptr, b) s proof (prove)
goal (10 subgoals):
 1. \<And>x2 ptr offset x2a etcb. \<lbrakk>kheap s ptr = Some (TCB x2a); ptr \<noteq> idle_thread s; ekheap s ptr = Some etcb; cap_counts x2; P x2; slot = (ptr, tcb_caller_slot); valid_objs s; tcb_caller_slot \<noteq> 6; tcb_caller_slot \<noteq> 5; tcb_caller_slot \<noteq> tcb_ipcbuffer_slot; offset = tcb_caller_slot; transform_cap (tcb_caller x2a) = x2; \<And>a. (a, tcb_cspace_slot) = transform_cslot_ptr (a, tcb_cnode_index 0); \<And>a. (a, tcb_vspace_slot) = transform_cslot_ptr (a, tcb_cnode_index (Suc 0)); \<And>a. (a, tcb_replycap_slot) = transform_cslot_ptr (a, tcb_cnode_index 2); \<And>a. (a, tcb_caller_slot) = transform_cslot_ptr (a, tcb_cnode_index 3); \<And>a. (a, tcb_ipcbuffer_slot) = transform_cslot_ptr (a, tcb_cnode_index 4)\<rbrakk> \<Longrightarrow> (ptr, tcb_caller_slot) = transform_cslot_ptr (ptr, tcb_cnode_index 3) \<and> (\<exists>get. (\<exists>set restr. tcb_cap_cases (tcb_cnode_index 3) = Some (get, set, restr)) \<and> P (transform_cap (get x2a)))
 2. \<And>x2 ptr offset x2a etcb. \<lbrakk>kheap s ptr = Some (TCB x2a); ptr \<noteq> idle_thread s; ekheap s ptr = Some etcb; cap_counts x2; P x2; slot = (ptr, tcb_replycap_slot); valid_objs s; tcb_replycap_slot \<noteq> 6; tcb_replycap_slot \<noteq> 5; tcb_replycap_slot \<noteq> tcb_ipcbuffer_slot; tcb_replycap_slot \<noteq> tcb_caller_slot; offset = tcb_replycap_slot; transform_cap (tcb_reply x2a) = x2\<rbrakk> \<Longrightarrow> \<exists>b. (ptr, tcb_replycap_slot) = transform_cslot_ptr (ptr, b) \<and> (\<exists>get. (\<exists>set restr. tcb_cap_cases b = Some (get, set, restr)) \<and> P (transform_cap (get x2a)))
 3. \<And>x2 ptr offset x2a etcb. \<lbrakk>kheap s ptr = Some (TCB x2a); ptr \<noteq> idle_thread s; ekheap s ptr = Some etcb; cap_counts x2; P x2; slot = (ptr, tcb_vspace_slot); valid_objs s; tcb_vspace_slot \<noteq> 6; tcb_vspace_slot \<noteq> 5; tcb_vspace_slot \<noteq> tcb_ipcbuffer_slot; tcb_vspace_slot \<noteq> tcb_caller_slot; tcb_vspace_slot \<noteq> tcb_replycap_slot; offset = tcb_vspace_slot; transform_cap (tcb_vtable x2a) = x2\<rbrakk> \<Longrightarrow> \<exists>b. (ptr, tcb_vspace_slot) = transform_cslot_ptr (ptr, b) \<and> (\<exists>get. (\<exists>set restr. tcb_cap_cases b = Some (get, set, restr)) \<and> P (transform_cap (get x2a)))
 4. \<And>x2 ptr offset x2a etcb. \<lbrakk>kheap s ptr = Some (TCB x2a); ptr \<noteq> idle_thread s; ekheap s ptr = Some etcb; cap_counts x2; P x2; slot = (ptr, tcb_cspace_slot); valid_objs s; tcb_cspace_slot \<noteq> 6; tcb_cspace_slot \<noteq> 5; tcb_cspace_slot \<noteq> tcb_ipcbuffer_slot; tcb_cspace_slot \<noteq> tcb_caller_slot; tcb_cspace_slot \<noteq> tcb_replycap_slot; tcb_cspace_slot \<noteq> tcb_vspace_slot; offset = tcb_cspace_slot; transform_cap (tcb_ctable x2a) = x2\<rbrakk> \<Longrightarrow> \<exists>b. (ptr, tcb_cspace_slot) = transform_cslot_ptr (ptr, b) \<and> (\<exists>get. (\<exists>set restr. tcb_cap_cases b = Some (get, set, restr)) \<and> P (transform_cap (get x2a)))
 5. \<And>x2 ptr offset x3 x5. \<lbrakk>cap_counts x2; P x2; slot = (ptr, offset); valid_objs s; valid_etcbs s; cdl_tcb_caps x3 offset = Some x2; kheap s ptr = Some (ArchObj x5); ptr \<noteq> idle_thread s; (case x5 of ASIDPool ap \<Rightarrow> AsidPool \<lparr>cdl_asid_pool_caps = transform_asid_pool_contents ap\<rparr> | arch_kernel_obj.PageTable ptx \<Rightarrow> cdl_object.PageTable \<lparr>cdl_page_table_caps = transform_page_table_contents ptx\<rparr> | arch_kernel_obj.PageDirectory pd \<Rightarrow> cdl_object.PageDirectory \<lparr>cdl_page_directory_caps = transform_page_directory_contents pd\<rparr> | DataPage dev sz \<Rightarrow> Frame \<lparr>cdl_frame_size_bits = pageBitsForSize sz\<rparr>) = Tcb x3\<rbrakk> \<Longrightarrow> False
 6. \<And>x2 ptr offset x4 z. \<lbrakk>P x2; slot = (ptr, offset); valid_objs s; valid_etcbs s; cdl_cnode_caps x4 offset = Some x2; kheap s ptr = Some z; ptr \<noteq> idle_thread s; transform_object (machine_state s) ptr (ekheap s ptr) z = cdl_object.CNode x4\<rbrakk> \<Longrightarrow> \<exists>b. (ptr, offset) = transform_cslot_ptr (ptr, b) \<and> cte_wp_at (\<lambda>cap'. P (transform_cap cap')) (ptr, b) s
 7. \<And>x2 ptr offset x5 z. \<lbrakk>P x2; slot = (ptr, offset); valid_objs s; valid_etcbs s; cdl_asid_pool_caps x5 offset = Some x2; kheap s ptr = Some z; ptr \<noteq> idle_thread s; transform_object (machine_state s) ptr (ekheap s ptr) z = AsidPool x5\<rbrakk> \<Longrightarrow> \<exists>b. (ptr, offset) = transform_cslot_ptr (ptr, b) \<and> cte_wp_at (\<lambda>cap'. P (transform_cap cap')) (ptr, b) s
 8. \<And>x2 ptr offset x6 z. \<lbrakk>P x2; slot = (ptr, offset); valid_objs s; valid_etcbs s; cdl_page_table_caps x6 offset = Some x2; kheap s ptr = Some z; ptr \<noteq> idle_thread s; transform_object (machine_state s) ptr (ekheap s ptr) z = cdl_object.PageTable x6\<rbrakk> \<Longrightarrow> \<exists>b. (ptr, offset) = transform_cslot_ptr (ptr, b) \<and> cte_wp_at (\<lambda>cap'. P (transform_cap cap')) (ptr, b) s
 9. \<And>x2 ptr offset x7 z. \<lbrakk>P x2; slot = (ptr, offset); valid_objs s; valid_etcbs s; cdl_page_directory_caps x7 offset = Some x2; kheap s ptr = Some z; ptr \<noteq> idle_thread s; transform_object (machine_state s) ptr (ekheap s ptr) z = cdl_object.PageDirectory x7\<rbrakk> \<Longrightarrow> \<exists>b. (ptr, offset) = transform_cslot_ptr (ptr, b) \<and> cte_wp_at (\<lambda>cap'. P (transform_cap cap')) (ptr, b) s
 10. \<And>x2 ptr offset x10 z. \<lbrakk>P x2; slot = (ptr, offset); valid_objs s; valid_etcbs s; cdl_irq_node_caps x10 offset = Some x2; kheap s ptr = Some z; ptr \<noteq> idle_thread s; transform_object (machine_state s) ptr (ekheap s ptr) z = IRQNode x10\<rbrakk> \<Longrightarrow> \<exists>b. (ptr, offset) = transform_cslot_ptr (ptr, b) \<and> cte_wp_at (\<lambda>cap'. P (transform_cap cap')) (ptr, b) s proof (prove)
goal (9 subgoals):
 1. \<And>x2 ptr offset x2a etcb. \<lbrakk>kheap s ptr = Some (TCB x2a); ptr \<noteq> idle_thread s; ekheap s ptr = Some etcb; cap_counts x2; P x2; slot = (ptr, tcb_replycap_slot); valid_objs s; tcb_replycap_slot \<noteq> 6; tcb_replycap_slot \<noteq> 5; tcb_replycap_slot \<noteq> tcb_ipcbuffer_slot; tcb_replycap_slot \<noteq> tcb_caller_slot; offset = tcb_replycap_slot; transform_cap (tcb_reply x2a) = x2\<rbrakk> \<Longrightarrow> \<exists>b. (ptr, tcb_replycap_slot) = transform_cslot_ptr (ptr, b) \<and> (\<exists>get. (\<exists>set restr. tcb_cap_cases b = Some (get, set, restr)) \<and> P (transform_cap (get x2a)))
 2. \<And>x2 ptr offset x2a etcb. \<lbrakk>kheap s ptr = Some (TCB x2a); ptr \<noteq> idle_thread s; ekheap s ptr = Some etcb; cap_counts x2; P x2; slot = (ptr, tcb_vspace_slot); valid_objs s; tcb_vspace_slot \<noteq> 6; tcb_vspace_slot \<noteq> 5; tcb_vspace_slot \<noteq> tcb_ipcbuffer_slot; tcb_vspace_slot \<noteq> tcb_caller_slot; tcb_vspace_slot \<noteq> tcb_replycap_slot; offset = tcb_vspace_slot; transform_cap (tcb_vtable x2a) = x2\<rbrakk> \<Longrightarrow> \<exists>b. (ptr, tcb_vspace_slot) = transform_cslot_ptr (ptr, b) \<and> (\<exists>get. (\<exists>set restr. tcb_cap_cases b = Some (get, set, restr)) \<and> P (transform_cap (get x2a)))
 3. \<And>x2 ptr offset x2a etcb. \<lbrakk>kheap s ptr = Some (TCB x2a); ptr \<noteq> idle_thread s; ekheap s ptr = Some etcb; cap_counts x2; P x2; slot = (ptr, tcb_cspace_slot); valid_objs s; tcb_cspace_slot \<noteq> 6; tcb_cspace_slot \<noteq> 5; tcb_cspace_slot \<noteq> tcb_ipcbuffer_slot; tcb_cspace_slot \<noteq> tcb_caller_slot; tcb_cspace_slot \<noteq> tcb_replycap_slot; tcb_cspace_slot \<noteq> tcb_vspace_slot; offset = tcb_cspace_slot; transform_cap (tcb_ctable x2a) = x2\<rbrakk> \<Longrightarrow> \<exists>b. (ptr, tcb_cspace_slot) = transform_cslot_ptr (ptr, b) \<and> (\<exists>get. (\<exists>set restr. tcb_cap_cases b = Some (get, set, restr)) \<and> P (transform_cap (get x2a)))
 4. \<And>x2 ptr offset x3 x5. \<lbrakk>cap_counts x2; P x2; slot = (ptr, offset); valid_objs s; valid_etcbs s; cdl_tcb_caps x3 offset = Some x2; kheap s ptr = Some (ArchObj x5); ptr \<noteq> idle_thread s; (case x5 of ASIDPool ap \<Rightarrow> AsidPool \<lparr>cdl_asid_pool_caps = transform_asid_pool_contents ap\<rparr> | arch_kernel_obj.PageTable ptx \<Rightarrow> cdl_object.PageTable \<lparr>cdl_page_table_caps = transform_page_table_contents ptx\<rparr> | arch_kernel_obj.PageDirectory pd \<Rightarrow> cdl_object.PageDirectory \<lparr>cdl_page_directory_caps = transform_page_directory_contents pd\<rparr> | DataPage dev sz \<Rightarrow> Frame \<lparr>cdl_frame_size_bits = pageBitsForSize sz\<rparr>) = Tcb x3\<rbrakk> \<Longrightarrow> False
 5. \<And>x2 ptr offset x4 z. \<lbrakk>P x2; slot = (ptr, offset); valid_objs s; valid_etcbs s; cdl_cnode_caps x4 offset = Some x2; kheap s ptr = Some z; ptr \<noteq> idle_thread s; transform_object (machine_state s) ptr (ekheap s ptr) z = cdl_object.CNode x4\<rbrakk> \<Longrightarrow> \<exists>b. (ptr, offset) = transform_cslot_ptr (ptr, b) \<and> cte_wp_at (\<lambda>cap'. P (transform_cap cap')) (ptr, b) s
 6. \<And>x2 ptr offset x5 z. \<lbrakk>P x2; slot = (ptr, offset); valid_objs s; valid_etcbs s; cdl_asid_pool_caps x5 offset = Some x2; kheap s ptr = Some z; ptr \<noteq> idle_thread s; transform_object (machine_state s) ptr (ekheap s ptr) z = AsidPool x5\<rbrakk> \<Longrightarrow> \<exists>b. (ptr, offset) = transform_cslot_ptr (ptr, b) \<and> cte_wp_at (\<lambda>cap'. P (transform_cap cap')) (ptr, b) s
 7. \<And>x2 ptr offset x6 z. \<lbrakk>P x2; slot = (ptr, offset); valid_objs s; valid_etcbs s; cdl_page_table_caps x6 offset = Some x2; kheap s ptr = Some z; ptr \<noteq> idle_thread s; transform_object (machine_state s) ptr (ekheap s ptr) z = cdl_object.PageTable x6\<rbrakk> \<Longrightarrow> \<exists>b. (ptr, offset) = transform_cslot_ptr (ptr, b) \<and> cte_wp_at (\<lambda>cap'. P (transform_cap cap')) (ptr, b) s
 8. \<And>x2 ptr offset x7 z. \<lbrakk>P x2; slot = (ptr, offset); valid_objs s; valid_etcbs s; cdl_page_directory_caps x7 offset = Some x2; kheap s ptr = Some z; ptr \<noteq> idle_thread s; transform_object (machine_state s) ptr (ekheap s ptr) z = cdl_object.PageDirectory x7\<rbrakk> \<Longrightarrow> \<exists>b. (ptr, offset) = transform_cslot_ptr (ptr, b) \<and> cte_wp_at (\<lambda>cap'. P (transform_cap cap')) (ptr, b) s
 9. \<And>x2 ptr offset x10 z. \<lbrakk>P x2; slot = (ptr, offset); valid_objs s; valid_etcbs s; cdl_irq_node_caps x10 offset = Some x2; kheap s ptr = Some z; ptr \<noteq> idle_thread s; transform_object (machine_state s) ptr (ekheap s ptr) z = IRQNode x10\<rbrakk> \<Longrightarrow> \<exists>b. (ptr, offset) = transform_cslot_ptr (ptr, b) \<and> cte_wp_at (\<lambda>cap'. P (transform_cap cap')) (ptr, b) s proof (prove)
using this:
(?a, tcb_cspace_slot) = transform_cslot_ptr (?a, tcb_cnode_index 0)
(?a, tcb_vspace_slot) = transform_cslot_ptr (?a, tcb_cnode_index (Suc 0))
(?a, tcb_replycap_slot) = transform_cslot_ptr (?a, tcb_cnode_index 2)
(?a, tcb_caller_slot) = transform_cslot_ptr (?a, tcb_cnode_index 3)
(?a, tcb_ipcbuffer_slot) = transform_cslot_ptr (?a, tcb_cnode_index 4)

goal (9 subgoals):
 1. \<And>x2 ptr offset x2a etcb. \<lbrakk>kheap s ptr = Some (TCB x2a); ptr \<noteq> idle_thread s; ekheap s ptr = Some etcb; cap_counts x2; P x2; slot = (ptr, tcb_replycap_slot); valid_objs s; tcb_replycap_slot \<noteq> 6; tcb_replycap_slot \<noteq> 5; tcb_replycap_slot \<noteq> tcb_ipcbuffer_slot; tcb_replycap_slot \<noteq> tcb_caller_slot; offset = tcb_replycap_slot; transform_cap (tcb_reply x2a) = x2\<rbrakk> \<Longrightarrow> \<exists>b. (ptr, tcb_replycap_slot) = transform_cslot_ptr (ptr, b) \<and> (\<exists>get. (\<exists>set restr. tcb_cap_cases b = Some (get, set, restr)) \<and> P (transform_cap (get x2a)))
 2. \<And>x2 ptr offset x2a etcb. \<lbrakk>kheap s ptr = Some (TCB x2a); ptr \<noteq> idle_thread s; ekheap s ptr = Some etcb; cap_counts x2; P x2; slot = (ptr, tcb_vspace_slot); valid_objs s; tcb_vspace_slot \<noteq> 6; tcb_vspace_slot \<noteq> 5; tcb_vspace_slot \<noteq> tcb_ipcbuffer_slot; tcb_vspace_slot \<noteq> tcb_caller_slot; tcb_vspace_slot \<noteq> tcb_replycap_slot; offset = tcb_vspace_slot; transform_cap (tcb_vtable x2a) = x2\<rbrakk> \<Longrightarrow> \<exists>b. (ptr, tcb_vspace_slot) = transform_cslot_ptr (ptr, b) \<and> (\<exists>get. (\<exists>set restr. tcb_cap_cases b = Some (get, set, restr)) \<and> P (transform_cap (get x2a)))
 3. \<And>x2 ptr offset x2a etcb. \<lbrakk>kheap s ptr = Some (TCB x2a); ptr \<noteq> idle_thread s; ekheap s ptr = Some etcb; cap_counts x2; P x2; slot = (ptr, tcb_cspace_slot); valid_objs s; tcb_cspace_slot \<noteq> 6; tcb_cspace_slot \<noteq> 5; tcb_cspace_slot \<noteq> tcb_ipcbuffer_slot; tcb_cspace_slot \<noteq> tcb_caller_slot; tcb_cspace_slot \<noteq> tcb_replycap_slot; tcb_cspace_slot \<noteq> tcb_vspace_slot; offset = tcb_cspace_slot; transform_cap (tcb_ctable x2a) = x2\<rbrakk> \<Longrightarrow> \<exists>b. (ptr, tcb_cspace_slot) = transform_cslot_ptr (ptr, b) \<and> (\<exists>get. (\<exists>set restr. tcb_cap_cases b = Some (get, set, restr)) \<and> P (transform_cap (get x2a)))
 4. \<And>x2 ptr offset x3 x5. \<lbrakk>cap_counts x2; P x2; slot = (ptr, offset); valid_objs s; valid_etcbs s; cdl_tcb_caps x3 offset = Some x2; kheap s ptr = Some (ArchObj x5); ptr \<noteq> idle_thread s; (case x5 of ASIDPool ap \<Rightarrow> AsidPool \<lparr>cdl_asid_pool_caps = transform_asid_pool_contents ap\<rparr> | arch_kernel_obj.PageTable ptx \<Rightarrow> cdl_object.PageTable \<lparr>cdl_page_table_caps = transform_page_table_contents ptx\<rparr> | arch_kernel_obj.PageDirectory pd \<Rightarrow> cdl_object.PageDirectory \<lparr>cdl_page_directory_caps = transform_page_directory_contents pd\<rparr> | DataPage dev sz \<Rightarrow> Frame \<lparr>cdl_frame_size_bits = pageBitsForSize sz\<rparr>) = Tcb x3\<rbrakk> \<Longrightarrow> False
 5. \<And>x2 ptr offset x4 z. \<lbrakk>P x2; slot = (ptr, offset); valid_objs s; valid_etcbs s; cdl_cnode_caps x4 offset = Some x2; kheap s ptr = Some z; ptr \<noteq> idle_thread s; transform_object (machine_state s) ptr (ekheap s ptr) z = cdl_object.CNode x4\<rbrakk> \<Longrightarrow> \<exists>b. (ptr, offset) = transform_cslot_ptr (ptr, b) \<and> cte_wp_at (\<lambda>cap'. P (transform_cap cap')) (ptr, b) s
 6. \<And>x2 ptr offset x5 z. \<lbrakk>P x2; slot = (ptr, offset); valid_objs s; valid_etcbs s; cdl_asid_pool_caps x5 offset = Some x2; kheap s ptr = Some z; ptr \<noteq> idle_thread s; transform_object (machine_state s) ptr (ekheap s ptr) z = AsidPool x5\<rbrakk> \<Longrightarrow> \<exists>b. (ptr, offset) = transform_cslot_ptr (ptr, b) \<and> cte_wp_at (\<lambda>cap'. P (transform_cap cap')) (ptr, b) s
 7. \<And>x2 ptr offset x6 z. \<lbrakk>P x2; slot = (ptr, offset); valid_objs s; valid_etcbs s; cdl_page_table_caps x6 offset = Some x2; kheap s ptr = Some z; ptr \<noteq> idle_thread s; transform_object (machine_state s) ptr (ekheap s ptr) z = cdl_object.PageTable x6\<rbrakk> \<Longrightarrow> \<exists>b. (ptr, offset) = transform_cslot_ptr (ptr, b) \<and> cte_wp_at (\<lambda>cap'. P (transform_cap cap')) (ptr, b) s
 8. \<And>x2 ptr offset x7 z. \<lbrakk>P x2; slot = (ptr, offset); valid_objs s; valid_etcbs s; cdl_page_directory_caps x7 offset = Some x2; kheap s ptr = Some z; ptr \<noteq> idle_thread s; transform_object (machine_state s) ptr (ekheap s ptr) z = cdl_object.PageDirectory x7\<rbrakk> \<Longrightarrow> \<exists>b. (ptr, offset) = transform_cslot_ptr (ptr, b) \<and> cte_wp_at (\<lambda>cap'. P (transform_cap cap')) (ptr, b) s
 9. \<And>x2 ptr offset x10 z. \<lbrakk>P x2; slot = (ptr, offset); valid_objs s; valid_etcbs s; cdl_irq_node_caps x10 offset = Some x2; kheap s ptr = Some z; ptr \<noteq> idle_thread s; transform_object (machine_state s) ptr (ekheap s ptr) z = IRQNode x10\<rbrakk> \<Longrightarrow> \<exists>b. (ptr, offset) = transform_cslot_ptr (ptr, b) \<and> cte_wp_at (\<lambda>cap'. P (transform_cap cap')) (ptr, b) s proof (prove)
goal (9 subgoals):
 1. \<And>x2 ptr offset x2a etcb. \<lbrakk>kheap s ptr = Some (TCB x2a); ptr \<noteq> idle_thread s; ekheap s ptr = Some etcb; cap_counts x2; P x2; slot = (ptr, tcb_replycap_slot); valid_objs s; tcb_replycap_slot \<noteq> 6; tcb_replycap_slot \<noteq> 5; tcb_replycap_slot \<noteq> tcb_ipcbuffer_slot; tcb_replycap_slot \<noteq> tcb_caller_slot; offset = tcb_replycap_slot; transform_cap (tcb_reply x2a) = x2; \<And>a. (a, tcb_cspace_slot) = transform_cslot_ptr (a, tcb_cnode_index 0); \<And>a. (a, tcb_vspace_slot) = transform_cslot_ptr (a, tcb_cnode_index (Suc 0)); \<And>a. (a, tcb_replycap_slot) = transform_cslot_ptr (a, tcb_cnode_index 2); \<And>a. (a, tcb_caller_slot) = transform_cslot_ptr (a, tcb_cnode_index 3); \<And>a. (a, tcb_ipcbuffer_slot) = transform_cslot_ptr (a, tcb_cnode_index 4)\<rbrakk> \<Longrightarrow> (ptr, tcb_replycap_slot) = transform_cslot_ptr (ptr, tcb_cnode_index 2) \<and> (\<exists>get. (\<exists>set restr. tcb_cap_cases (tcb_cnode_index 2) = Some (get, set, restr)) \<and> P (transform_cap (get x2a)))
 2. \<And>x2 ptr offset x2a etcb. \<lbrakk>kheap s ptr = Some (TCB x2a); ptr \<noteq> idle_thread s; ekheap s ptr = Some etcb; cap_counts x2; P x2; slot = (ptr, tcb_vspace_slot); valid_objs s; tcb_vspace_slot \<noteq> 6; tcb_vspace_slot \<noteq> 5; tcb_vspace_slot \<noteq> tcb_ipcbuffer_slot; tcb_vspace_slot \<noteq> tcb_caller_slot; tcb_vspace_slot \<noteq> tcb_replycap_slot; offset = tcb_vspace_slot; transform_cap (tcb_vtable x2a) = x2\<rbrakk> \<Longrightarrow> \<exists>b. (ptr, tcb_vspace_slot) = transform_cslot_ptr (ptr, b) \<and> (\<exists>get. (\<exists>set restr. tcb_cap_cases b = Some (get, set, restr)) \<and> P (transform_cap (get x2a)))
 3. \<And>x2 ptr offset x2a etcb. \<lbrakk>kheap s ptr = Some (TCB x2a); ptr \<noteq> idle_thread s; ekheap s ptr = Some etcb; cap_counts x2; P x2; slot = (ptr, tcb_cspace_slot); valid_objs s; tcb_cspace_slot \<noteq> 6; tcb_cspace_slot \<noteq> 5; tcb_cspace_slot \<noteq> tcb_ipcbuffer_slot; tcb_cspace_slot \<noteq> tcb_caller_slot; tcb_cspace_slot \<noteq> tcb_replycap_slot; tcb_cspace_slot \<noteq> tcb_vspace_slot; offset = tcb_cspace_slot; transform_cap (tcb_ctable x2a) = x2\<rbrakk> \<Longrightarrow> \<exists>b. (ptr, tcb_cspace_slot) = transform_cslot_ptr (ptr, b) \<and> (\<exists>get. (\<exists>set restr. tcb_cap_cases b = Some (get, set, restr)) \<and> P (transform_cap (get x2a)))
 4. \<And>x2 ptr offset x3 x5. \<lbrakk>cap_counts x2; P x2; slot = (ptr, offset); valid_objs s; valid_etcbs s; cdl_tcb_caps x3 offset = Some x2; kheap s ptr = Some (ArchObj x5); ptr \<noteq> idle_thread s; (case x5 of ASIDPool ap \<Rightarrow> AsidPool \<lparr>cdl_asid_pool_caps = transform_asid_pool_contents ap\<rparr> | arch_kernel_obj.PageTable ptx \<Rightarrow> cdl_object.PageTable \<lparr>cdl_page_table_caps = transform_page_table_contents ptx\<rparr> | arch_kernel_obj.PageDirectory pd \<Rightarrow> cdl_object.PageDirectory \<lparr>cdl_page_directory_caps = transform_page_directory_contents pd\<rparr> | DataPage dev sz \<Rightarrow> Frame \<lparr>cdl_frame_size_bits = pageBitsForSize sz\<rparr>) = Tcb x3\<rbrakk> \<Longrightarrow> False
 5. \<And>x2 ptr offset x4 z. \<lbrakk>P x2; slot = (ptr, offset); valid_objs s; valid_etcbs s; cdl_cnode_caps x4 offset = Some x2; kheap s ptr = Some z; ptr \<noteq> idle_thread s; transform_object (machine_state s) ptr (ekheap s ptr) z = cdl_object.CNode x4\<rbrakk> \<Longrightarrow> \<exists>b. (ptr, offset) = transform_cslot_ptr (ptr, b) \<and> cte_wp_at (\<lambda>cap'. P (transform_cap cap')) (ptr, b) s
 6. \<And>x2 ptr offset x5 z. \<lbrakk>P x2; slot = (ptr, offset); valid_objs s; valid_etcbs s; cdl_asid_pool_caps x5 offset = Some x2; kheap s ptr = Some z; ptr \<noteq> idle_thread s; transform_object (machine_state s) ptr (ekheap s ptr) z = AsidPool x5\<rbrakk> \<Longrightarrow> \<exists>b. (ptr, offset) = transform_cslot_ptr (ptr, b) \<and> cte_wp_at (\<lambda>cap'. P (transform_cap cap')) (ptr, b) s
 7. \<And>x2 ptr offset x6 z. \<lbrakk>P x2; slot = (ptr, offset); valid_objs s; valid_etcbs s; cdl_page_table_caps x6 offset = Some x2; kheap s ptr = Some z; ptr \<noteq> idle_thread s; transform_object (machine_state s) ptr (ekheap s ptr) z = cdl_object.PageTable x6\<rbrakk> \<Longrightarrow> \<exists>b. (ptr, offset) = transform_cslot_ptr (ptr, b) \<and> cte_wp_at (\<lambda>cap'. P (transform_cap cap')) (ptr, b) s
 8. \<And>x2 ptr offset x7 z. \<lbrakk>P x2; slot = (ptr, offset); valid_objs s; valid_etcbs s; cdl_page_directory_caps x7 offset = Some x2; kheap s ptr = Some z; ptr \<noteq> idle_thread s; transform_object (machine_state s) ptr (ekheap s ptr) z = cdl_object.PageDirectory x7\<rbrakk> \<Longrightarrow> \<exists>b. (ptr, offset) = transform_cslot_ptr (ptr, b) \<and> cte_wp_at (\<lambda>cap'. P (transform_cap cap')) (ptr, b) s
 9. \<And>x2 ptr offset x10 z. \<lbrakk>P x2; slot = (ptr, offset); valid_objs s; valid_etcbs s; cdl_irq_node_caps x10 offset = Some x2; kheap s ptr = Some z; ptr \<noteq> idle_thread s; transform_object (machine_state s) ptr (ekheap s ptr) z = IRQNode x10\<rbrakk> \<Longrightarrow> \<exists>b. (ptr, offset) = transform_cslot_ptr (ptr, b) \<and> cte_wp_at (\<lambda>cap'. P (transform_cap cap')) (ptr, b) s proof (prove)
goal (8 subgoals):
 1. \<And>x2 ptr offset x2a etcb. \<lbrakk>kheap s ptr = Some (TCB x2a); ptr \<noteq> idle_thread s; ekheap s ptr = Some etcb; cap_counts x2; P x2; slot = (ptr, tcb_vspace_slot); valid_objs s; tcb_vspace_slot \<noteq> 6; tcb_vspace_slot \<noteq> 5; tcb_vspace_slot \<noteq> tcb_ipcbuffer_slot; tcb_vspace_slot \<noteq> tcb_caller_slot; tcb_vspace_slot \<noteq> tcb_replycap_slot; offset = tcb_vspace_slot; transform_cap (tcb_vtable x2a) = x2\<rbrakk> \<Longrightarrow> \<exists>b. (ptr, tcb_vspace_slot) = transform_cslot_ptr (ptr, b) \<and> (\<exists>get. (\<exists>set restr. tcb_cap_cases b = Some (get, set, restr)) \<and> P (transform_cap (get x2a)))
 2. \<And>x2 ptr offset x2a etcb. \<lbrakk>kheap s ptr = Some (TCB x2a); ptr \<noteq> idle_thread s; ekheap s ptr = Some etcb; cap_counts x2; P x2; slot = (ptr, tcb_cspace_slot); valid_objs s; tcb_cspace_slot \<noteq> 6; tcb_cspace_slot \<noteq> 5; tcb_cspace_slot \<noteq> tcb_ipcbuffer_slot; tcb_cspace_slot \<noteq> tcb_caller_slot; tcb_cspace_slot \<noteq> tcb_replycap_slot; tcb_cspace_slot \<noteq> tcb_vspace_slot; offset = tcb_cspace_slot; transform_cap (tcb_ctable x2a) = x2\<rbrakk> \<Longrightarrow> \<exists>b. (ptr, tcb_cspace_slot) = transform_cslot_ptr (ptr, b) \<and> (\<exists>get. (\<exists>set restr. tcb_cap_cases b = Some (get, set, restr)) \<and> P (transform_cap (get x2a)))
 3. \<And>x2 ptr offset x3 x5. \<lbrakk>cap_counts x2; P x2; slot = (ptr, offset); valid_objs s; valid_etcbs s; cdl_tcb_caps x3 offset = Some x2; kheap s ptr = Some (ArchObj x5); ptr \<noteq> idle_thread s; (case x5 of ASIDPool ap \<Rightarrow> AsidPool \<lparr>cdl_asid_pool_caps = transform_asid_pool_contents ap\<rparr> | arch_kernel_obj.PageTable ptx \<Rightarrow> cdl_object.PageTable \<lparr>cdl_page_table_caps = transform_page_table_contents ptx\<rparr> | arch_kernel_obj.PageDirectory pd \<Rightarrow> cdl_object.PageDirectory \<lparr>cdl_page_directory_caps = transform_page_directory_contents pd\<rparr> | DataPage dev sz \<Rightarrow> Frame \<lparr>cdl_frame_size_bits = pageBitsForSize sz\<rparr>) = Tcb x3\<rbrakk> \<Longrightarrow> False
 4. \<And>x2 ptr offset x4 z. \<lbrakk>P x2; slot = (ptr, offset); valid_objs s; valid_etcbs s; cdl_cnode_caps x4 offset = Some x2; kheap s ptr = Some z; ptr \<noteq> idle_thread s; transform_object (machine_state s) ptr (ekheap s ptr) z = cdl_object.CNode x4\<rbrakk> \<Longrightarrow> \<exists>b. (ptr, offset) = transform_cslot_ptr (ptr, b) \<and> cte_wp_at (\<lambda>cap'. P (transform_cap cap')) (ptr, b) s
 5. \<And>x2 ptr offset x5 z. \<lbrakk>P x2; slot = (ptr, offset); valid_objs s; valid_etcbs s; cdl_asid_pool_caps x5 offset = Some x2; kheap s ptr = Some z; ptr \<noteq> idle_thread s; transform_object (machine_state s) ptr (ekheap s ptr) z = AsidPool x5\<rbrakk> \<Longrightarrow> \<exists>b. (ptr, offset) = transform_cslot_ptr (ptr, b) \<and> cte_wp_at (\<lambda>cap'. P (transform_cap cap')) (ptr, b) s
 6. \<And>x2 ptr offset x6 z. \<lbrakk>P x2; slot = (ptr, offset); valid_objs s; valid_etcbs s; cdl_page_table_caps x6 offset = Some x2; kheap s ptr = Some z; ptr \<noteq> idle_thread s; transform_object (machine_state s) ptr (ekheap s ptr) z = cdl_object.PageTable x6\<rbrakk> \<Longrightarrow> \<exists>b. (ptr, offset) = transform_cslot_ptr (ptr, b) \<and> cte_wp_at (\<lambda>cap'. P (transform_cap cap')) (ptr, b) s
 7. \<And>x2 ptr offset x7 z. \<lbrakk>P x2; slot = (ptr, offset); valid_objs s; valid_etcbs s; cdl_page_directory_caps x7 offset = Some x2; kheap s ptr = Some z; ptr \<noteq> idle_thread s; transform_object (machine_state s) ptr (ekheap s ptr) z = cdl_object.PageDirectory x7\<rbrakk> \<Longrightarrow> \<exists>b. (ptr, offset) = transform_cslot_ptr (ptr, b) \<and> cte_wp_at (\<lambda>cap'. P (transform_cap cap')) (ptr, b) s
 8. \<And>x2 ptr offset x10 z. \<lbrakk>P x2; slot = (ptr, offset); valid_objs s; valid_etcbs s; cdl_irq_node_caps x10 offset = Some x2; kheap s ptr = Some z; ptr \<noteq> idle_thread s; transform_object (machine_state s) ptr (ekheap s ptr) z = IRQNode x10\<rbrakk> \<Longrightarrow> \<exists>b. (ptr, offset) = transform_cslot_ptr (ptr, b) \<and> cte_wp_at (\<lambda>cap'. P (transform_cap cap')) (ptr, b) s proof (prove)
using this:
(?a, tcb_cspace_slot) = transform_cslot_ptr (?a, tcb_cnode_index 0)
(?a, tcb_vspace_slot) = transform_cslot_ptr (?a, tcb_cnode_index (Suc 0))
(?a, tcb_replycap_slot) = transform_cslot_ptr (?a, tcb_cnode_index 2)
(?a, tcb_caller_slot) = transform_cslot_ptr (?a, tcb_cnode_index 3)
(?a, tcb_ipcbuffer_slot) = transform_cslot_ptr (?a, tcb_cnode_index 4)

goal (8 subgoals):
 1. \<And>x2 ptr offset x2a etcb. \<lbrakk>kheap s ptr = Some (TCB x2a); ptr \<noteq> idle_thread s; ekheap s ptr = Some etcb; cap_counts x2; P x2; slot = (ptr, tcb_vspace_slot); valid_objs s; tcb_vspace_slot \<noteq> 6; tcb_vspace_slot \<noteq> 5; tcb_vspace_slot \<noteq> tcb_ipcbuffer_slot; tcb_vspace_slot \<noteq> tcb_caller_slot; tcb_vspace_slot \<noteq> tcb_replycap_slot; offset = tcb_vspace_slot; transform_cap (tcb_vtable x2a) = x2\<rbrakk> \<Longrightarrow> \<exists>b. (ptr, tcb_vspace_slot) = transform_cslot_ptr (ptr, b) \<and> (\<exists>get. (\<exists>set restr. tcb_cap_cases b = Some (get, set, restr)) \<and> P (transform_cap (get x2a)))
 2. \<And>x2 ptr offset x2a etcb. \<lbrakk>kheap s ptr = Some (TCB x2a); ptr \<noteq> idle_thread s; ekheap s ptr = Some etcb; cap_counts x2; P x2; slot = (ptr, tcb_cspace_slot); valid_objs s; tcb_cspace_slot \<noteq> 6; tcb_cspace_slot \<noteq> 5; tcb_cspace_slot \<noteq> tcb_ipcbuffer_slot; tcb_cspace_slot \<noteq> tcb_caller_slot; tcb_cspace_slot \<noteq> tcb_replycap_slot; tcb_cspace_slot \<noteq> tcb_vspace_slot; offset = tcb_cspace_slot; transform_cap (tcb_ctable x2a) = x2\<rbrakk> \<Longrightarrow> \<exists>b. (ptr, tcb_cspace_slot) = transform_cslot_ptr (ptr, b) \<and> (\<exists>get. (\<exists>set restr. tcb_cap_cases b = Some (get, set, restr)) \<and> P (transform_cap (get x2a)))
 3. \<And>x2 ptr offset x3 x5. \<lbrakk>cap_counts x2; P x2; slot = (ptr, offset); valid_objs s; valid_etcbs s; cdl_tcb_caps x3 offset = Some x2; kheap s ptr = Some (ArchObj x5); ptr \<noteq> idle_thread s; (case x5 of ASIDPool ap \<Rightarrow> AsidPool \<lparr>cdl_asid_pool_caps = transform_asid_pool_contents ap\<rparr> | arch_kernel_obj.PageTable ptx \<Rightarrow> cdl_object.PageTable \<lparr>cdl_page_table_caps = transform_page_table_contents ptx\<rparr> | arch_kernel_obj.PageDirectory pd \<Rightarrow> cdl_object.PageDirectory \<lparr>cdl_page_directory_caps = transform_page_directory_contents pd\<rparr> | DataPage dev sz \<Rightarrow> Frame \<lparr>cdl_frame_size_bits = pageBitsForSize sz\<rparr>) = Tcb x3\<rbrakk> \<Longrightarrow> False
 4. \<And>x2 ptr offset x4 z. \<lbrakk>P x2; slot = (ptr, offset); valid_objs s; valid_etcbs s; cdl_cnode_caps x4 offset = Some x2; kheap s ptr = Some z; ptr \<noteq> idle_thread s; transform_object (machine_state s) ptr (ekheap s ptr) z = cdl_object.CNode x4\<rbrakk> \<Longrightarrow> \<exists>b. (ptr, offset) = transform_cslot_ptr (ptr, b) \<and> cte_wp_at (\<lambda>cap'. P (transform_cap cap')) (ptr, b) s
 5. \<And>x2 ptr offset x5 z. \<lbrakk>P x2; slot = (ptr, offset); valid_objs s; valid_etcbs s; cdl_asid_pool_caps x5 offset = Some x2; kheap s ptr = Some z; ptr \<noteq> idle_thread s; transform_object (machine_state s) ptr (ekheap s ptr) z = AsidPool x5\<rbrakk> \<Longrightarrow> \<exists>b. (ptr, offset) = transform_cslot_ptr (ptr, b) \<and> cte_wp_at (\<lambda>cap'. P (transform_cap cap')) (ptr, b) s
 6. \<And>x2 ptr offset x6 z. \<lbrakk>P x2; slot = (ptr, offset); valid_objs s; valid_etcbs s; cdl_page_table_caps x6 offset = Some x2; kheap s ptr = Some z; ptr \<noteq> idle_thread s; transform_object (machine_state s) ptr (ekheap s ptr) z = cdl_object.PageTable x6\<rbrakk> \<Longrightarrow> \<exists>b. (ptr, offset) = transform_cslot_ptr (ptr, b) \<and> cte_wp_at (\<lambda>cap'. P (transform_cap cap')) (ptr, b) s
 7. \<And>x2 ptr offset x7 z. \<lbrakk>P x2; slot = (ptr, offset); valid_objs s; valid_etcbs s; cdl_page_directory_caps x7 offset = Some x2; kheap s ptr = Some z; ptr \<noteq> idle_thread s; transform_object (machine_state s) ptr (ekheap s ptr) z = cdl_object.PageDirectory x7\<rbrakk> \<Longrightarrow> \<exists>b. (ptr, offset) = transform_cslot_ptr (ptr, b) \<and> cte_wp_at (\<lambda>cap'. P (transform_cap cap')) (ptr, b) s
 8. \<And>x2 ptr offset x10 z. \<lbrakk>P x2; slot = (ptr, offset); valid_objs s; valid_etcbs s; cdl_irq_node_caps x10 offset = Some x2; kheap s ptr = Some z; ptr \<noteq> idle_thread s; transform_object (machine_state s) ptr (ekheap s ptr) z = IRQNode x10\<rbrakk> \<Longrightarrow> \<exists>b. (ptr, offset) = transform_cslot_ptr (ptr, b) \<and> cte_wp_at (\<lambda>cap'. P (transform_cap cap')) (ptr, b) s proof (prove)
goal (8 subgoals):
 1. \<And>x2 ptr offset x2a etcb. \<lbrakk>kheap s ptr = Some (TCB x2a); ptr \<noteq> idle_thread s; ekheap s ptr = Some etcb; cap_counts x2; P x2; slot = (ptr, tcb_vspace_slot); valid_objs s; tcb_vspace_slot \<noteq> 6; tcb_vspace_slot \<noteq> 5; tcb_vspace_slot \<noteq> tcb_ipcbuffer_slot; tcb_vspace_slot \<noteq> tcb_caller_slot; tcb_vspace_slot \<noteq> tcb_replycap_slot; offset = tcb_vspace_slot; transform_cap (tcb_vtable x2a) = x2; \<And>a. (a, tcb_cspace_slot) = transform_cslot_ptr (a, tcb_cnode_index 0); \<And>a. (a, tcb_vspace_slot) = transform_cslot_ptr (a, tcb_cnode_index (Suc 0)); \<And>a. (a, tcb_replycap_slot) = transform_cslot_ptr (a, tcb_cnode_index 2); \<And>a. (a, tcb_caller_slot) = transform_cslot_ptr (a, tcb_cnode_index 3); \<And>a. (a, tcb_ipcbuffer_slot) = transform_cslot_ptr (a, tcb_cnode_index 4)\<rbrakk> \<Longrightarrow> (ptr, tcb_vspace_slot) = transform_cslot_ptr (ptr, tcb_cnode_index 1) \<and> (\<exists>get. (\<exists>set restr. tcb_cap_cases (tcb_cnode_index 1) = Some (get, set, restr)) \<and> P (transform_cap (get x2a)))
 2. \<And>x2 ptr offset x2a etcb. \<lbrakk>kheap s ptr = Some (TCB x2a); ptr \<noteq> idle_thread s; ekheap s ptr = Some etcb; cap_counts x2; P x2; slot = (ptr, tcb_cspace_slot); valid_objs s; tcb_cspace_slot \<noteq> 6; tcb_cspace_slot \<noteq> 5; tcb_cspace_slot \<noteq> tcb_ipcbuffer_slot; tcb_cspace_slot \<noteq> tcb_caller_slot; tcb_cspace_slot \<noteq> tcb_replycap_slot; tcb_cspace_slot \<noteq> tcb_vspace_slot; offset = tcb_cspace_slot; transform_cap (tcb_ctable x2a) = x2\<rbrakk> \<Longrightarrow> \<exists>b. (ptr, tcb_cspace_slot) = transform_cslot_ptr (ptr, b) \<and> (\<exists>get. (\<exists>set restr. tcb_cap_cases b = Some (get, set, restr)) \<and> P (transform_cap (get x2a)))
 3. \<And>x2 ptr offset x3 x5. \<lbrakk>cap_counts x2; P x2; slot = (ptr, offset); valid_objs s; valid_etcbs s; cdl_tcb_caps x3 offset = Some x2; kheap s ptr = Some (ArchObj x5); ptr \<noteq> idle_thread s; (case x5 of ASIDPool ap \<Rightarrow> AsidPool \<lparr>cdl_asid_pool_caps = transform_asid_pool_contents ap\<rparr> | arch_kernel_obj.PageTable ptx \<Rightarrow> cdl_object.PageTable \<lparr>cdl_page_table_caps = transform_page_table_contents ptx\<rparr> | arch_kernel_obj.PageDirectory pd \<Rightarrow> cdl_object.PageDirectory \<lparr>cdl_page_directory_caps = transform_page_directory_contents pd\<rparr> | DataPage dev sz \<Rightarrow> Frame \<lparr>cdl_frame_size_bits = pageBitsForSize sz\<rparr>) = Tcb x3\<rbrakk> \<Longrightarrow> False
 4. \<And>x2 ptr offset x4 z. \<lbrakk>P x2; slot = (ptr, offset); valid_objs s; valid_etcbs s; cdl_cnode_caps x4 offset = Some x2; kheap s ptr = Some z; ptr \<noteq> idle_thread s; transform_object (machine_state s) ptr (ekheap s ptr) z = cdl_object.CNode x4\<rbrakk> \<Longrightarrow> \<exists>b. (ptr, offset) = transform_cslot_ptr (ptr, b) \<and> cte_wp_at (\<lambda>cap'. P (transform_cap cap')) (ptr, b) s
 5. \<And>x2 ptr offset x5 z. \<lbrakk>P x2; slot = (ptr, offset); valid_objs s; valid_etcbs s; cdl_asid_pool_caps x5 offset = Some x2; kheap s ptr = Some z; ptr \<noteq> idle_thread s; transform_object (machine_state s) ptr (ekheap s ptr) z = AsidPool x5\<rbrakk> \<Longrightarrow> \<exists>b. (ptr, offset) = transform_cslot_ptr (ptr, b) \<and> cte_wp_at (\<lambda>cap'. P (transform_cap cap')) (ptr, b) s
 6. \<And>x2 ptr offset x6 z. \<lbrakk>P x2; slot = (ptr, offset); valid_objs s; valid_etcbs s; cdl_page_table_caps x6 offset = Some x2; kheap s ptr = Some z; ptr \<noteq> idle_thread s; transform_object (machine_state s) ptr (ekheap s ptr) z = cdl_object.PageTable x6\<rbrakk> \<Longrightarrow> \<exists>b. (ptr, offset) = transform_cslot_ptr (ptr, b) \<and> cte_wp_at (\<lambda>cap'. P (transform_cap cap')) (ptr, b) s
 7. \<And>x2 ptr offset x7 z. \<lbrakk>P x2; slot = (ptr, offset); valid_objs s; valid_etcbs s; cdl_page_directory_caps x7 offset = Some x2; kheap s ptr = Some z; ptr \<noteq> idle_thread s; transform_object (machine_state s) ptr (ekheap s ptr) z = cdl_object.PageDirectory x7\<rbrakk> \<Longrightarrow> \<exists>b. (ptr, offset) = transform_cslot_ptr (ptr, b) \<and> cte_wp_at (\<lambda>cap'. P (transform_cap cap')) (ptr, b) s
 8. \<And>x2 ptr offset x10 z. \<lbrakk>P x2; slot = (ptr, offset); valid_objs s; valid_etcbs s; cdl_irq_node_caps x10 offset = Some x2; kheap s ptr = Some z; ptr \<noteq> idle_thread s; transform_object (machine_state s) ptr (ekheap s ptr) z = IRQNode x10\<rbrakk> \<Longrightarrow> \<exists>b. (ptr, offset) = transform_cslot_ptr (ptr, b) \<and> cte_wp_at (\<lambda>cap'. P (transform_cap cap')) (ptr, b) s proof (prove)
goal (7 subgoals):
 1. \<And>x2 ptr offset x2a etcb. \<lbrakk>kheap s ptr = Some (TCB x2a); ptr \<noteq> idle_thread s; ekheap s ptr = Some etcb; cap_counts x2; P x2; slot = (ptr, tcb_cspace_slot); valid_objs s; tcb_cspace_slot \<noteq> 6; tcb_cspace_slot \<noteq> 5; tcb_cspace_slot \<noteq> tcb_ipcbuffer_slot; tcb_cspace_slot \<noteq> tcb_caller_slot; tcb_cspace_slot \<noteq> tcb_replycap_slot; tcb_cspace_slot \<noteq> tcb_vspace_slot; offset = tcb_cspace_slot; transform_cap (tcb_ctable x2a) = x2\<rbrakk> \<Longrightarrow> \<exists>b. (ptr, tcb_cspace_slot) = transform_cslot_ptr (ptr, b) \<and> (\<exists>get. (\<exists>set restr. tcb_cap_cases b = Some (get, set, restr)) \<and> P (transform_cap (get x2a)))
 2. \<And>x2 ptr offset x3 x5. \<lbrakk>cap_counts x2; P x2; slot = (ptr, offset); valid_objs s; valid_etcbs s; cdl_tcb_caps x3 offset = Some x2; kheap s ptr = Some (ArchObj x5); ptr \<noteq> idle_thread s; (case x5 of ASIDPool ap \<Rightarrow> AsidPool \<lparr>cdl_asid_pool_caps = transform_asid_pool_contents ap\<rparr> | arch_kernel_obj.PageTable ptx \<Rightarrow> cdl_object.PageTable \<lparr>cdl_page_table_caps = transform_page_table_contents ptx\<rparr> | arch_kernel_obj.PageDirectory pd \<Rightarrow> cdl_object.PageDirectory \<lparr>cdl_page_directory_caps = transform_page_directory_contents pd\<rparr> | DataPage dev sz \<Rightarrow> Frame \<lparr>cdl_frame_size_bits = pageBitsForSize sz\<rparr>) = Tcb x3\<rbrakk> \<Longrightarrow> False
 3. \<And>x2 ptr offset x4 z. \<lbrakk>P x2; slot = (ptr, offset); valid_objs s; valid_etcbs s; cdl_cnode_caps x4 offset = Some x2; kheap s ptr = Some z; ptr \<noteq> idle_thread s; transform_object (machine_state s) ptr (ekheap s ptr) z = cdl_object.CNode x4\<rbrakk> \<Longrightarrow> \<exists>b. (ptr, offset) = transform_cslot_ptr (ptr, b) \<and> cte_wp_at (\<lambda>cap'. P (transform_cap cap')) (ptr, b) s
 4. \<And>x2 ptr offset x5 z. \<lbrakk>P x2; slot = (ptr, offset); valid_objs s; valid_etcbs s; cdl_asid_pool_caps x5 offset = Some x2; kheap s ptr = Some z; ptr \<noteq> idle_thread s; transform_object (machine_state s) ptr (ekheap s ptr) z = AsidPool x5\<rbrakk> \<Longrightarrow> \<exists>b. (ptr, offset) = transform_cslot_ptr (ptr, b) \<and> cte_wp_at (\<lambda>cap'. P (transform_cap cap')) (ptr, b) s
 5. \<And>x2 ptr offset x6 z. \<lbrakk>P x2; slot = (ptr, offset); valid_objs s; valid_etcbs s; cdl_page_table_caps x6 offset = Some x2; kheap s ptr = Some z; ptr \<noteq> idle_thread s; transform_object (machine_state s) ptr (ekheap s ptr) z = cdl_object.PageTable x6\<rbrakk> \<Longrightarrow> \<exists>b. (ptr, offset) = transform_cslot_ptr (ptr, b) \<and> cte_wp_at (\<lambda>cap'. P (transform_cap cap')) (ptr, b) s
 6. \<And>x2 ptr offset x7 z. \<lbrakk>P x2; slot = (ptr, offset); valid_objs s; valid_etcbs s; cdl_page_directory_caps x7 offset = Some x2; kheap s ptr = Some z; ptr \<noteq> idle_thread s; transform_object (machine_state s) ptr (ekheap s ptr) z = cdl_object.PageDirectory x7\<rbrakk> \<Longrightarrow> \<exists>b. (ptr, offset) = transform_cslot_ptr (ptr, b) \<and> cte_wp_at (\<lambda>cap'. P (transform_cap cap')) (ptr, b) s
 7. \<And>x2 ptr offset x10 z. \<lbrakk>P x2; slot = (ptr, offset); valid_objs s; valid_etcbs s; cdl_irq_node_caps x10 offset = Some x2; kheap s ptr = Some z; ptr \<noteq> idle_thread s; transform_object (machine_state s) ptr (ekheap s ptr) z = IRQNode x10\<rbrakk> \<Longrightarrow> \<exists>b. (ptr, offset) = transform_cslot_ptr (ptr, b) \<and> cte_wp_at (\<lambda>cap'. P (transform_cap cap')) (ptr, b) s proof (prove)
using this:
(?a, tcb_cspace_slot) = transform_cslot_ptr (?a, tcb_cnode_index 0)
(?a, tcb_vspace_slot) = transform_cslot_ptr (?a, tcb_cnode_index (Suc 0))
(?a, tcb_replycap_slot) = transform_cslot_ptr (?a, tcb_cnode_index 2)
(?a, tcb_caller_slot) = transform_cslot_ptr (?a, tcb_cnode_index 3)
(?a, tcb_ipcbuffer_slot) = transform_cslot_ptr (?a, tcb_cnode_index 4)

goal (7 subgoals):
 1. \<And>x2 ptr offset x2a etcb. \<lbrakk>kheap s ptr = Some (TCB x2a); ptr \<noteq> idle_thread s; ekheap s ptr = Some etcb; cap_counts x2; P x2; slot = (ptr, tcb_cspace_slot); valid_objs s; tcb_cspace_slot \<noteq> 6; tcb_cspace_slot \<noteq> 5; tcb_cspace_slot \<noteq> tcb_ipcbuffer_slot; tcb_cspace_slot \<noteq> tcb_caller_slot; tcb_cspace_slot \<noteq> tcb_replycap_slot; tcb_cspace_slot \<noteq> tcb_vspace_slot; offset = tcb_cspace_slot; transform_cap (tcb_ctable x2a) = x2\<rbrakk> \<Longrightarrow> \<exists>b. (ptr, tcb_cspace_slot) = transform_cslot_ptr (ptr, b) \<and> (\<exists>get. (\<exists>set restr. tcb_cap_cases b = Some (get, set, restr)) \<and> P (transform_cap (get x2a)))
 2. \<And>x2 ptr offset x3 x5. \<lbrakk>cap_counts x2; P x2; slot = (ptr, offset); valid_objs s; valid_etcbs s; cdl_tcb_caps x3 offset = Some x2; kheap s ptr = Some (ArchObj x5); ptr \<noteq> idle_thread s; (case x5 of ASIDPool ap \<Rightarrow> AsidPool \<lparr>cdl_asid_pool_caps = transform_asid_pool_contents ap\<rparr> | arch_kernel_obj.PageTable ptx \<Rightarrow> cdl_object.PageTable \<lparr>cdl_page_table_caps = transform_page_table_contents ptx\<rparr> | arch_kernel_obj.PageDirectory pd \<Rightarrow> cdl_object.PageDirectory \<lparr>cdl_page_directory_caps = transform_page_directory_contents pd\<rparr> | DataPage dev sz \<Rightarrow> Frame \<lparr>cdl_frame_size_bits = pageBitsForSize sz\<rparr>) = Tcb x3\<rbrakk> \<Longrightarrow> False
 3. \<And>x2 ptr offset x4 z. \<lbrakk>P x2; slot = (ptr, offset); valid_objs s; valid_etcbs s; cdl_cnode_caps x4 offset = Some x2; kheap s ptr = Some z; ptr \<noteq> idle_thread s; transform_object (machine_state s) ptr (ekheap s ptr) z = cdl_object.CNode x4\<rbrakk> \<Longrightarrow> \<exists>b. (ptr, offset) = transform_cslot_ptr (ptr, b) \<and> cte_wp_at (\<lambda>cap'. P (transform_cap cap')) (ptr, b) s
 4. \<And>x2 ptr offset x5 z. \<lbrakk>P x2; slot = (ptr, offset); valid_objs s; valid_etcbs s; cdl_asid_pool_caps x5 offset = Some x2; kheap s ptr = Some z; ptr \<noteq> idle_thread s; transform_object (machine_state s) ptr (ekheap s ptr) z = AsidPool x5\<rbrakk> \<Longrightarrow> \<exists>b. (ptr, offset) = transform_cslot_ptr (ptr, b) \<and> cte_wp_at (\<lambda>cap'. P (transform_cap cap')) (ptr, b) s
 5. \<And>x2 ptr offset x6 z. \<lbrakk>P x2; slot = (ptr, offset); valid_objs s; valid_etcbs s; cdl_page_table_caps x6 offset = Some x2; kheap s ptr = Some z; ptr \<noteq> idle_thread s; transform_object (machine_state s) ptr (ekheap s ptr) z = cdl_object.PageTable x6\<rbrakk> \<Longrightarrow> \<exists>b. (ptr, offset) = transform_cslot_ptr (ptr, b) \<and> cte_wp_at (\<lambda>cap'. P (transform_cap cap')) (ptr, b) s
 6. \<And>x2 ptr offset x7 z. \<lbrakk>P x2; slot = (ptr, offset); valid_objs s; valid_etcbs s; cdl_page_directory_caps x7 offset = Some x2; kheap s ptr = Some z; ptr \<noteq> idle_thread s; transform_object (machine_state s) ptr (ekheap s ptr) z = cdl_object.PageDirectory x7\<rbrakk> \<Longrightarrow> \<exists>b. (ptr, offset) = transform_cslot_ptr (ptr, b) \<and> cte_wp_at (\<lambda>cap'. P (transform_cap cap')) (ptr, b) s
 7. \<And>x2 ptr offset x10 z. \<lbrakk>P x2; slot = (ptr, offset); valid_objs s; valid_etcbs s; cdl_irq_node_caps x10 offset = Some x2; kheap s ptr = Some z; ptr \<noteq> idle_thread s; transform_object (machine_state s) ptr (ekheap s ptr) z = IRQNode x10\<rbrakk> \<Longrightarrow> \<exists>b. (ptr, offset) = transform_cslot_ptr (ptr, b) \<and> cte_wp_at (\<lambda>cap'. P (transform_cap cap')) (ptr, b) s proof (prove)
goal (7 subgoals):
 1. \<And>x2 ptr offset x2a etcb. \<lbrakk>kheap s ptr = Some (TCB x2a); ptr \<noteq> idle_thread s; ekheap s ptr = Some etcb; cap_counts x2; P x2; slot = (ptr, tcb_cspace_slot); valid_objs s; tcb_cspace_slot \<noteq> 6; tcb_cspace_slot \<noteq> 5; tcb_cspace_slot \<noteq> tcb_ipcbuffer_slot; tcb_cspace_slot \<noteq> tcb_caller_slot; tcb_cspace_slot \<noteq> tcb_replycap_slot; tcb_cspace_slot \<noteq> tcb_vspace_slot; offset = tcb_cspace_slot; transform_cap (tcb_ctable x2a) = x2; \<And>a. (a, tcb_cspace_slot) = transform_cslot_ptr (a, tcb_cnode_index 0); \<And>a. (a, tcb_vspace_slot) = transform_cslot_ptr (a, tcb_cnode_index (Suc 0)); \<And>a. (a, tcb_replycap_slot) = transform_cslot_ptr (a, tcb_cnode_index 2); \<And>a. (a, tcb_caller_slot) = transform_cslot_ptr (a, tcb_cnode_index 3); \<And>a. (a, tcb_ipcbuffer_slot) = transform_cslot_ptr (a, tcb_cnode_index 4)\<rbrakk> \<Longrightarrow> (ptr, tcb_cspace_slot) = transform_cslot_ptr (ptr, tcb_cnode_index 0) \<and> (\<exists>get. (\<exists>set restr. tcb_cap_cases (tcb_cnode_index 0) = Some (get, set, restr)) \<and> P (transform_cap (get x2a)))
 2. \<And>x2 ptr offset x3 x5. \<lbrakk>cap_counts x2; P x2; slot = (ptr, offset); valid_objs s; valid_etcbs s; cdl_tcb_caps x3 offset = Some x2; kheap s ptr = Some (ArchObj x5); ptr \<noteq> idle_thread s; (case x5 of ASIDPool ap \<Rightarrow> AsidPool \<lparr>cdl_asid_pool_caps = transform_asid_pool_contents ap\<rparr> | arch_kernel_obj.PageTable ptx \<Rightarrow> cdl_object.PageTable \<lparr>cdl_page_table_caps = transform_page_table_contents ptx\<rparr> | arch_kernel_obj.PageDirectory pd \<Rightarrow> cdl_object.PageDirectory \<lparr>cdl_page_directory_caps = transform_page_directory_contents pd\<rparr> | DataPage dev sz \<Rightarrow> Frame \<lparr>cdl_frame_size_bits = pageBitsForSize sz\<rparr>) = Tcb x3\<rbrakk> \<Longrightarrow> False
 3. \<And>x2 ptr offset x4 z. \<lbrakk>P x2; slot = (ptr, offset); valid_objs s; valid_etcbs s; cdl_cnode_caps x4 offset = Some x2; kheap s ptr = Some z; ptr \<noteq> idle_thread s; transform_object (machine_state s) ptr (ekheap s ptr) z = cdl_object.CNode x4\<rbrakk> \<Longrightarrow> \<exists>b. (ptr, offset) = transform_cslot_ptr (ptr, b) \<and> cte_wp_at (\<lambda>cap'. P (transform_cap cap')) (ptr, b) s
 4. \<And>x2 ptr offset x5 z. \<lbrakk>P x2; slot = (ptr, offset); valid_objs s; valid_etcbs s; cdl_asid_pool_caps x5 offset = Some x2; kheap s ptr = Some z; ptr \<noteq> idle_thread s; transform_object (machine_state s) ptr (ekheap s ptr) z = AsidPool x5\<rbrakk> \<Longrightarrow> \<exists>b. (ptr, offset) = transform_cslot_ptr (ptr, b) \<and> cte_wp_at (\<lambda>cap'. P (transform_cap cap')) (ptr, b) s
 5. \<And>x2 ptr offset x6 z. \<lbrakk>P x2; slot = (ptr, offset); valid_objs s; valid_etcbs s; cdl_page_table_caps x6 offset = Some x2; kheap s ptr = Some z; ptr \<noteq> idle_thread s; transform_object (machine_state s) ptr (ekheap s ptr) z = cdl_object.PageTable x6\<rbrakk> \<Longrightarrow> \<exists>b. (ptr, offset) = transform_cslot_ptr (ptr, b) \<and> cte_wp_at (\<lambda>cap'. P (transform_cap cap')) (ptr, b) s
 6. \<And>x2 ptr offset x7 z. \<lbrakk>P x2; slot = (ptr, offset); valid_objs s; valid_etcbs s; cdl_page_directory_caps x7 offset = Some x2; kheap s ptr = Some z; ptr \<noteq> idle_thread s; transform_object (machine_state s) ptr (ekheap s ptr) z = cdl_object.PageDirectory x7\<rbrakk> \<Longrightarrow> \<exists>b. (ptr, offset) = transform_cslot_ptr (ptr, b) \<and> cte_wp_at (\<lambda>cap'. P (transform_cap cap')) (ptr, b) s
 7. \<And>x2 ptr offset x10 z. \<lbrakk>P x2; slot = (ptr, offset); valid_objs s; valid_etcbs s; cdl_irq_node_caps x10 offset = Some x2; kheap s ptr = Some z; ptr \<noteq> idle_thread s; transform_object (machine_state s) ptr (ekheap s ptr) z = IRQNode x10\<rbrakk> \<Longrightarrow> \<exists>b. (ptr, offset) = transform_cslot_ptr (ptr, b) \<and> cte_wp_at (\<lambda>cap'. P (transform_cap cap')) (ptr, b) s proof (prove)
goal (6 subgoals):
 1. \<And>x2 ptr offset x3 x5. \<lbrakk>cap_counts x2; P x2; slot = (ptr, offset); valid_objs s; valid_etcbs s; cdl_tcb_caps x3 offset = Some x2; kheap s ptr = Some (ArchObj x5); ptr \<noteq> idle_thread s; (case x5 of ASIDPool ap \<Rightarrow> AsidPool \<lparr>cdl_asid_pool_caps = transform_asid_pool_contents ap\<rparr> | arch_kernel_obj.PageTable ptx \<Rightarrow> cdl_object.PageTable \<lparr>cdl_page_table_caps = transform_page_table_contents ptx\<rparr> | arch_kernel_obj.PageDirectory pd \<Rightarrow> cdl_object.PageDirectory \<lparr>cdl_page_directory_caps = transform_page_directory_contents pd\<rparr> | DataPage dev sz \<Rightarrow> Frame \<lparr>cdl_frame_size_bits = pageBitsForSize sz\<rparr>) = Tcb x3\<rbrakk> \<Longrightarrow> False
 2. \<And>x2 ptr offset x4 z. \<lbrakk>P x2; slot = (ptr, offset); valid_objs s; valid_etcbs s; cdl_cnode_caps x4 offset = Some x2; kheap s ptr = Some z; ptr \<noteq> idle_thread s; transform_object (machine_state s) ptr (ekheap s ptr) z = cdl_object.CNode x4\<rbrakk> \<Longrightarrow> \<exists>b. (ptr, offset) = transform_cslot_ptr (ptr, b) \<and> cte_wp_at (\<lambda>cap'. P (transform_cap cap')) (ptr, b) s
 3. \<And>x2 ptr offset x5 z. \<lbrakk>P x2; slot = (ptr, offset); valid_objs s; valid_etcbs s; cdl_asid_pool_caps x5 offset = Some x2; kheap s ptr = Some z; ptr \<noteq> idle_thread s; transform_object (machine_state s) ptr (ekheap s ptr) z = AsidPool x5\<rbrakk> \<Longrightarrow> \<exists>b. (ptr, offset) = transform_cslot_ptr (ptr, b) \<and> cte_wp_at (\<lambda>cap'. P (transform_cap cap')) (ptr, b) s
 4. \<And>x2 ptr offset x6 z. \<lbrakk>P x2; slot = (ptr, offset); valid_objs s; valid_etcbs s; cdl_page_table_caps x6 offset = Some x2; kheap s ptr = Some z; ptr \<noteq> idle_thread s; transform_object (machine_state s) ptr (ekheap s ptr) z = cdl_object.PageTable x6\<rbrakk> \<Longrightarrow> \<exists>b. (ptr, offset) = transform_cslot_ptr (ptr, b) \<and> cte_wp_at (\<lambda>cap'. P (transform_cap cap')) (ptr, b) s
 5. \<And>x2 ptr offset x7 z. \<lbrakk>P x2; slot = (ptr, offset); valid_objs s; valid_etcbs s; cdl_page_directory_caps x7 offset = Some x2; kheap s ptr = Some z; ptr \<noteq> idle_thread s; transform_object (machine_state s) ptr (ekheap s ptr) z = cdl_object.PageDirectory x7\<rbrakk> \<Longrightarrow> \<exists>b. (ptr, offset) = transform_cslot_ptr (ptr, b) \<and> cte_wp_at (\<lambda>cap'. P (transform_cap cap')) (ptr, b) s
 6. \<And>x2 ptr offset x10 z. \<lbrakk>P x2; slot = (ptr, offset); valid_objs s; valid_etcbs s; cdl_irq_node_caps x10 offset = Some x2; kheap s ptr = Some z; ptr \<noteq> idle_thread s; transform_object (machine_state s) ptr (ekheap s ptr) z = IRQNode x10\<rbrakk> \<Longrightarrow> \<exists>b. (ptr, offset) = transform_cslot_ptr (ptr, b) \<and> cte_wp_at (\<lambda>cap'. P (transform_cap cap')) (ptr, b) s proof (prove)
goal (6 subgoals):
 1. \<And>x2 ptr offset x3 arch_kernel_obj. \<lbrakk>cap_counts x2; P x2; slot = (ptr, offset); valid_objs s; valid_etcbs s; cdl_tcb_caps x3 offset = Some x2; kheap s ptr = Some (ArchObj arch_kernel_obj); ptr \<noteq> idle_thread s; (case arch_kernel_obj of ASIDPool ap \<Rightarrow> AsidPool \<lparr>cdl_asid_pool_caps = transform_asid_pool_contents ap\<rparr> | arch_kernel_obj.PageTable ptx \<Rightarrow> cdl_object.PageTable \<lparr>cdl_page_table_caps = transform_page_table_contents ptx\<rparr> | arch_kernel_obj.PageDirectory pd \<Rightarrow> cdl_object.PageDirectory \<lparr>cdl_page_directory_caps = transform_page_directory_contents pd\<rparr> | DataPage dev sz \<Rightarrow> Frame \<lparr>cdl_frame_size_bits = pageBitsForSize sz\<rparr>) = Tcb x3\<rbrakk> \<Longrightarrow> False
 2. \<And>x2 ptr offset x4 z. \<lbrakk>P x2; slot = (ptr, offset); valid_objs s; valid_etcbs s; cdl_cnode_caps x4 offset = Some x2; kheap s ptr = Some z; ptr \<noteq> idle_thread s; transform_object (machine_state s) ptr (ekheap s ptr) z = cdl_object.CNode x4\<rbrakk> \<Longrightarrow> \<exists>b. (ptr, offset) = transform_cslot_ptr (ptr, b) \<and> cte_wp_at (\<lambda>cap'. P (transform_cap cap')) (ptr, b) s
 3. \<And>x2 ptr offset x5 z. \<lbrakk>P x2; slot = (ptr, offset); valid_objs s; valid_etcbs s; cdl_asid_pool_caps x5 offset = Some x2; kheap s ptr = Some z; ptr \<noteq> idle_thread s; transform_object (machine_state s) ptr (ekheap s ptr) z = AsidPool x5\<rbrakk> \<Longrightarrow> \<exists>b. (ptr, offset) = transform_cslot_ptr (ptr, b) \<and> cte_wp_at (\<lambda>cap'. P (transform_cap cap')) (ptr, b) s
 4. \<And>x2 ptr offset x6 z. \<lbrakk>P x2; slot = (ptr, offset); valid_objs s; valid_etcbs s; cdl_page_table_caps x6 offset = Some x2; kheap s ptr = Some z; ptr \<noteq> idle_thread s; transform_object (machine_state s) ptr (ekheap s ptr) z = cdl_object.PageTable x6\<rbrakk> \<Longrightarrow> \<exists>b. (ptr, offset) = transform_cslot_ptr (ptr, b) \<and> cte_wp_at (\<lambda>cap'. P (transform_cap cap')) (ptr, b) s
 5. \<And>x2 ptr offset x7 z. \<lbrakk>P x2; slot = (ptr, offset); valid_objs s; valid_etcbs s; cdl_page_directory_caps x7 offset = Some x2; kheap s ptr = Some z; ptr \<noteq> idle_thread s; transform_object (machine_state s) ptr (ekheap s ptr) z = cdl_object.PageDirectory x7\<rbrakk> \<Longrightarrow> \<exists>b. (ptr, offset) = transform_cslot_ptr (ptr, b) \<and> cte_wp_at (\<lambda>cap'. P (transform_cap cap')) (ptr, b) s
 6. \<And>x2 ptr offset x10 z. \<lbrakk>P x2; slot = (ptr, offset); valid_objs s; valid_etcbs s; cdl_irq_node_caps x10 offset = Some x2; kheap s ptr = Some z; ptr \<noteq> idle_thread s; transform_object (machine_state s) ptr (ekheap s ptr) z = IRQNode x10\<rbrakk> \<Longrightarrow> \<exists>b. (ptr, offset) = transform_cslot_ptr (ptr, b) \<and> cte_wp_at (\<lambda>cap'. P (transform_cap cap')) (ptr, b) s proof (prove)
goal (5 subgoals):
 1. \<And>x2 ptr offset x4 z. \<lbrakk>P x2; slot = (ptr, offset); valid_objs s; valid_etcbs s; cdl_cnode_caps x4 offset = Some x2; kheap s ptr = Some z; ptr \<noteq> idle_thread s; transform_object (machine_state s) ptr (ekheap s ptr) z = cdl_object.CNode x4\<rbrakk> \<Longrightarrow> \<exists>b. (ptr, offset) = transform_cslot_ptr (ptr, b) \<and> cte_wp_at (\<lambda>cap'. P (transform_cap cap')) (ptr, b) s
 2. \<And>x2 ptr offset x5 z. \<lbrakk>P x2; slot = (ptr, offset); valid_objs s; valid_etcbs s; cdl_asid_pool_caps x5 offset = Some x2; kheap s ptr = Some z; ptr \<noteq> idle_thread s; transform_object (machine_state s) ptr (ekheap s ptr) z = AsidPool x5\<rbrakk> \<Longrightarrow> \<exists>b. (ptr, offset) = transform_cslot_ptr (ptr, b) \<and> cte_wp_at (\<lambda>cap'. P (transform_cap cap')) (ptr, b) s
 3. \<And>x2 ptr offset x6 z. \<lbrakk>P x2; slot = (ptr, offset); valid_objs s; valid_etcbs s; cdl_page_table_caps x6 offset = Some x2; kheap s ptr = Some z; ptr \<noteq> idle_thread s; transform_object (machine_state s) ptr (ekheap s ptr) z = cdl_object.PageTable x6\<rbrakk> \<Longrightarrow> \<exists>b. (ptr, offset) = transform_cslot_ptr (ptr, b) \<and> cte_wp_at (\<lambda>cap'. P (transform_cap cap')) (ptr, b) s
 4. \<And>x2 ptr offset x7 z. \<lbrakk>P x2; slot = (ptr, offset); valid_objs s; valid_etcbs s; cdl_page_directory_caps x7 offset = Some x2; kheap s ptr = Some z; ptr \<noteq> idle_thread s; transform_object (machine_state s) ptr (ekheap s ptr) z = cdl_object.PageDirectory x7\<rbrakk> \<Longrightarrow> \<exists>b. (ptr, offset) = transform_cslot_ptr (ptr, b) \<and> cte_wp_at (\<lambda>cap'. P (transform_cap cap')) (ptr, b) s
 5. \<And>x2 ptr offset x10 z. \<lbrakk>P x2; slot = (ptr, offset); valid_objs s; valid_etcbs s; cdl_irq_node_caps x10 offset = Some x2; kheap s ptr = Some z; ptr \<noteq> idle_thread s; transform_object (machine_state s) ptr (ekheap s ptr) z = IRQNode x10\<rbrakk> \<Longrightarrow> \<exists>b. (ptr, offset) = transform_cslot_ptr (ptr, b) \<and> cte_wp_at (\<lambda>cap'. P (transform_cap cap')) (ptr, b) s proof (prove)
goal (5 subgoals):
 1. \<And>x2 ptr offset x4 z. \<lbrakk>P x2; slot = (ptr, offset); valid_objs s; valid_etcbs s; cdl_cnode_caps x4 offset = Some x2; kheap s ptr = Some z; ptr \<noteq> idle_thread s; (case z of kernel_object.CNode 0 c \<Rightarrow> IRQNode \<lparr>cdl_irq_node_caps = transform_cnode_contents 0 c\<rparr> | kernel_object.CNode (Suc nat) c \<Rightarrow> cdl_object.CNode \<lparr>cdl_cnode_caps = transform_cnode_contents (Suc nat) c, cdl_cnode_size_bits = Suc nat\<rparr> | TCB tcb \<Rightarrow> case ekheap s ptr of Some etcb \<Rightarrow> transform_tcb (machine_state s) ptr tcb etcb | kernel_object.Endpoint x \<Rightarrow> cdl_object.Endpoint | kernel_object.Notification x \<Rightarrow> cdl_object.Notification | ArchObj (ASIDPool ap) \<Rightarrow> AsidPool \<lparr>cdl_asid_pool_caps = transform_asid_pool_contents ap\<rparr> | ArchObj (arch_kernel_obj.PageTable ptx) \<Rightarrow> cdl_object.PageTable \<lparr>cdl_page_table_caps = transform_page_table_contents ptx\<rparr> | ArchObj (arch_kernel_obj.PageDirectory pd) \<Rightarrow> cdl_object.PageDirectory \<lparr>cdl_page_directory_caps = transform_page_directory_contents pd\<rparr> | ArchObj (DataPage dev sz) \<Rightarrow> Frame \<lparr>cdl_frame_size_bits = pageBitsForSize sz\<rparr>) = cdl_object.CNode x4\<rbrakk> \<Longrightarrow> \<exists>b. (ptr, offset) = transform_cslot_ptr (ptr, b) \<and> cte_wp_at (\<lambda>cap'. P (transform_cap cap')) (ptr, b) s
 2. \<And>x2 ptr offset x5 z. \<lbrakk>P x2; slot = (ptr, offset); valid_objs s; valid_etcbs s; cdl_asid_pool_caps x5 offset = Some x2; kheap s ptr = Some z; ptr \<noteq> idle_thread s; (case z of kernel_object.CNode 0 c \<Rightarrow> IRQNode \<lparr>cdl_irq_node_caps = transform_cnode_contents 0 c\<rparr> | kernel_object.CNode (Suc nat) c \<Rightarrow> cdl_object.CNode \<lparr>cdl_cnode_caps = transform_cnode_contents (Suc nat) c, cdl_cnode_size_bits = Suc nat\<rparr> | TCB tcb \<Rightarrow> case ekheap s ptr of Some etcb \<Rightarrow> transform_tcb (machine_state s) ptr tcb etcb | kernel_object.Endpoint x \<Rightarrow> cdl_object.Endpoint | kernel_object.Notification x \<Rightarrow> cdl_object.Notification | ArchObj (ASIDPool ap) \<Rightarrow> AsidPool \<lparr>cdl_asid_pool_caps = transform_asid_pool_contents ap\<rparr> | ArchObj (arch_kernel_obj.PageTable ptx) \<Rightarrow> cdl_object.PageTable \<lparr>cdl_page_table_caps = transform_page_table_contents ptx\<rparr> | ArchObj (arch_kernel_obj.PageDirectory pd) \<Rightarrow> cdl_object.PageDirectory \<lparr>cdl_page_directory_caps = transform_page_directory_contents pd\<rparr> | ArchObj (DataPage dev sz) \<Rightarrow> Frame \<lparr>cdl_frame_size_bits = pageBitsForSize sz\<rparr>) = AsidPool x5\<rbrakk> \<Longrightarrow> \<exists>b. (ptr, offset) = transform_cslot_ptr (ptr, b) \<and> cte_wp_at (\<lambda>cap'. P (transform_cap cap')) (ptr, b) s
 3. \<And>x2 ptr offset x6 z. \<lbrakk>P x2; slot = (ptr, offset); valid_objs s; valid_etcbs s; cdl_page_table_caps x6 offset = Some x2; kheap s ptr = Some z; ptr \<noteq> idle_thread s; (case z of kernel_object.CNode 0 c \<Rightarrow> IRQNode \<lparr>cdl_irq_node_caps = transform_cnode_contents 0 c\<rparr> | kernel_object.CNode (Suc nat) c \<Rightarrow> cdl_object.CNode \<lparr>cdl_cnode_caps = transform_cnode_contents (Suc nat) c, cdl_cnode_size_bits = Suc nat\<rparr> | TCB tcb \<Rightarrow> case ekheap s ptr of Some etcb \<Rightarrow> transform_tcb (machine_state s) ptr tcb etcb | kernel_object.Endpoint x \<Rightarrow> cdl_object.Endpoint | kernel_object.Notification x \<Rightarrow> cdl_object.Notification | ArchObj (ASIDPool ap) \<Rightarrow> AsidPool \<lparr>cdl_asid_pool_caps = transform_asid_pool_contents ap\<rparr> | ArchObj (arch_kernel_obj.PageTable ptx) \<Rightarrow> cdl_object.PageTable \<lparr>cdl_page_table_caps = transform_page_table_contents ptx\<rparr> | ArchObj (arch_kernel_obj.PageDirectory pd) \<Rightarrow> cdl_object.PageDirectory \<lparr>cdl_page_directory_caps = transform_page_directory_contents pd\<rparr> | ArchObj (DataPage dev sz) \<Rightarrow> Frame \<lparr>cdl_frame_size_bits = pageBitsForSize sz\<rparr>) = cdl_object.PageTable x6\<rbrakk> \<Longrightarrow> \<exists>b. (ptr, offset) = transform_cslot_ptr (ptr, b) \<and> cte_wp_at (\<lambda>cap'. P (transform_cap cap')) (ptr, b) s
 4. \<And>x2 ptr offset x7 z. \<lbrakk>P x2; slot = (ptr, offset); valid_objs s; valid_etcbs s; cdl_page_directory_caps x7 offset = Some x2; kheap s ptr = Some z; ptr \<noteq> idle_thread s; (case z of kernel_object.CNode 0 c \<Rightarrow> IRQNode \<lparr>cdl_irq_node_caps = transform_cnode_contents 0 c\<rparr> | kernel_object.CNode (Suc nat) c \<Rightarrow> cdl_object.CNode \<lparr>cdl_cnode_caps = transform_cnode_contents (Suc nat) c, cdl_cnode_size_bits = Suc nat\<rparr> | TCB tcb \<Rightarrow> case ekheap s ptr of Some etcb \<Rightarrow> transform_tcb (machine_state s) ptr tcb etcb | kernel_object.Endpoint x \<Rightarrow> cdl_object.Endpoint | kernel_object.Notification x \<Rightarrow> cdl_object.Notification | ArchObj (ASIDPool ap) \<Rightarrow> AsidPool \<lparr>cdl_asid_pool_caps = transform_asid_pool_contents ap\<rparr> | ArchObj (arch_kernel_obj.PageTable ptx) \<Rightarrow> cdl_object.PageTable \<lparr>cdl_page_table_caps = transform_page_table_contents ptx\<rparr> | ArchObj (arch_kernel_obj.PageDirectory pd) \<Rightarrow> cdl_object.PageDirectory \<lparr>cdl_page_directory_caps = transform_page_directory_contents pd\<rparr> | ArchObj (DataPage dev sz) \<Rightarrow> Frame \<lparr>cdl_frame_size_bits = pageBitsForSize sz\<rparr>) = cdl_object.PageDirectory x7\<rbrakk> \<Longrightarrow> \<exists>b. (ptr, offset) = transform_cslot_ptr (ptr, b) \<and> cte_wp_at (\<lambda>cap'. P (transform_cap cap')) (ptr, b) s
 5. \<And>x2 ptr offset x10 z. \<lbrakk>P x2; slot = (ptr, offset); valid_objs s; valid_etcbs s; cdl_irq_node_caps x10 offset = Some x2; kheap s ptr = Some z; ptr \<noteq> idle_thread s; (case z of kernel_object.CNode 0 c \<Rightarrow> IRQNode \<lparr>cdl_irq_node_caps = transform_cnode_contents 0 c\<rparr> | kernel_object.CNode (Suc nat) c \<Rightarrow> cdl_object.CNode \<lparr>cdl_cnode_caps = transform_cnode_contents (Suc nat) c, cdl_cnode_size_bits = Suc nat\<rparr> | TCB tcb \<Rightarrow> case ekheap s ptr of Some etcb \<Rightarrow> transform_tcb (machine_state s) ptr tcb etcb | kernel_object.Endpoint x \<Rightarrow> cdl_object.Endpoint | kernel_object.Notification x \<Rightarrow> cdl_object.Notification | ArchObj (ASIDPool ap) \<Rightarrow> AsidPool \<lparr>cdl_asid_pool_caps = transform_asid_pool_contents ap\<rparr> | ArchObj (arch_kernel_obj.PageTable ptx) \<Rightarrow> cdl_object.PageTable \<lparr>cdl_page_table_caps = transform_page_table_contents ptx\<rparr> | ArchObj (arch_kernel_obj.PageDirectory pd) \<Rightarrow> cdl_object.PageDirectory \<lparr>cdl_page_directory_caps = transform_page_directory_contents pd\<rparr> | ArchObj (DataPage dev sz) \<Rightarrow> Frame \<lparr>cdl_frame_size_bits = pageBitsForSize sz\<rparr>) = IRQNode x10\<rbrakk> \<Longrightarrow> \<exists>b. (ptr, offset) = transform_cslot_ptr (ptr, b) \<and> cte_wp_at (\<lambda>cap'. P (transform_cap cap')) (ptr, b) s proof (prove)
goal (8 subgoals):
 1. \<And>ptr offset x12 x2a x2b z. \<lbrakk>kheap s ptr = Some (kernel_object.CNode (Suc x2a) x12); ptr \<noteq> idle_thread s; P (transform_cap z); slot = (ptr, offset); valid_objs s; valid_etcbs s; nat_to_bl (Suc x2a) offset = Some x2b; x12 x2b = Some z\<rbrakk> \<Longrightarrow> \<exists>b. (ptr, offset) = transform_cslot_ptr (ptr, b) \<and> cte_wp_at (\<lambda>cap'. P (transform_cap cap')) (ptr, b) s
 2. \<And>x2 ptr offset x4 x2a. \<lbrakk>P x2; slot = (ptr, offset); valid_objs s; valid_etcbs s; cdl_cnode_caps x4 offset = Some x2; kheap s ptr = Some (TCB x2a); ptr \<noteq> idle_thread s; ekheap s ptr = None; undefined = cdl_object.CNode x4\<rbrakk> \<Longrightarrow> \<exists>b. (ptr, offset) = transform_cslot_ptr (ptr, b) \<and> cte_wp_at (\<lambda>cap'. P (transform_cap cap')) (ptr, b) s
 3. \<And>x2 ptr offset x4 x2a x2b. \<lbrakk>P x2; slot = (ptr, offset); valid_objs s; valid_etcbs s; cdl_cnode_caps x4 offset = Some x2; kheap s ptr = Some (TCB x2a); ptr \<noteq> idle_thread s; ekheap s ptr = Some x2b; transform_tcb (machine_state s) ptr x2a x2b = cdl_object.CNode x4\<rbrakk> \<Longrightarrow> \<exists>b. (ptr, offset) = transform_cslot_ptr (ptr, b) \<and> cte_wp_at (\<lambda>cap'. P (transform_cap cap')) (ptr, b) s
 4. \<And>x2 ptr offset x4 x5. \<lbrakk>P x2; slot = (ptr, offset); valid_objs s; valid_etcbs s; cdl_cnode_caps x4 offset = Some x2; kheap s ptr = Some (ArchObj x5); ptr \<noteq> idle_thread s; (case x5 of ASIDPool ap \<Rightarrow> AsidPool \<lparr>cdl_asid_pool_caps = transform_asid_pool_contents ap\<rparr> | arch_kernel_obj.PageTable ptx \<Rightarrow> cdl_object.PageTable \<lparr>cdl_page_table_caps = transform_page_table_contents ptx\<rparr> | arch_kernel_obj.PageDirectory pd \<Rightarrow> cdl_object.PageDirectory \<lparr>cdl_page_directory_caps = transform_page_directory_contents pd\<rparr> | DataPage dev sz \<Rightarrow> Frame \<lparr>cdl_frame_size_bits = pageBitsForSize sz\<rparr>) = cdl_object.CNode x4\<rbrakk> \<Longrightarrow> \<exists>b. (ptr, offset) = transform_cslot_ptr (ptr, b) \<and> cte_wp_at (\<lambda>cap'. P (transform_cap cap')) (ptr, b) s
 5. \<And>x2 ptr offset x5 z. \<lbrakk>P x2; slot = (ptr, offset); valid_objs s; valid_etcbs s; cdl_asid_pool_caps x5 offset = Some x2; kheap s ptr = Some z; ptr \<noteq> idle_thread s; (case z of kernel_object.CNode 0 c \<Rightarrow> IRQNode \<lparr>cdl_irq_node_caps = transform_cnode_contents 0 c\<rparr> | kernel_object.CNode (Suc nat) c \<Rightarrow> cdl_object.CNode \<lparr>cdl_cnode_caps = transform_cnode_contents (Suc nat) c, cdl_cnode_size_bits = Suc nat\<rparr> | TCB tcb \<Rightarrow> case ekheap s ptr of Some etcb \<Rightarrow> transform_tcb (machine_state s) ptr tcb etcb | kernel_object.Endpoint x \<Rightarrow> cdl_object.Endpoint | kernel_object.Notification x \<Rightarrow> cdl_object.Notification | ArchObj (ASIDPool ap) \<Rightarrow> AsidPool \<lparr>cdl_asid_pool_caps = transform_asid_pool_contents ap\<rparr> | ArchObj (arch_kernel_obj.PageTable ptx) \<Rightarrow> cdl_object.PageTable \<lparr>cdl_page_table_caps = transform_page_table_contents ptx\<rparr> | ArchObj (arch_kernel_obj.PageDirectory pd) \<Rightarrow> cdl_object.PageDirectory \<lparr>cdl_page_directory_caps = transform_page_directory_contents pd\<rparr> | ArchObj (DataPage dev sz) \<Rightarrow> Frame \<lparr>cdl_frame_size_bits = pageBitsForSize sz\<rparr>) = AsidPool x5\<rbrakk> \<Longrightarrow> \<exists>b. (ptr, offset) = transform_cslot_ptr (ptr, b) \<and> cte_wp_at (\<lambda>cap'. P (transform_cap cap')) (ptr, b) s
 6. \<And>x2 ptr offset x6 z. \<lbrakk>P x2; slot = (ptr, offset); valid_objs s; valid_etcbs s; cdl_page_table_caps x6 offset = Some x2; kheap s ptr = Some z; ptr \<noteq> idle_thread s; (case z of kernel_object.CNode 0 c \<Rightarrow> IRQNode \<lparr>cdl_irq_node_caps = transform_cnode_contents 0 c\<rparr> | kernel_object.CNode (Suc nat) c \<Rightarrow> cdl_object.CNode \<lparr>cdl_cnode_caps = transform_cnode_contents (Suc nat) c, cdl_cnode_size_bits = Suc nat\<rparr> | TCB tcb \<Rightarrow> case ekheap s ptr of Some etcb \<Rightarrow> transform_tcb (machine_state s) ptr tcb etcb | kernel_object.Endpoint x \<Rightarrow> cdl_object.Endpoint | kernel_object.Notification x \<Rightarrow> cdl_object.Notification | ArchObj (ASIDPool ap) \<Rightarrow> AsidPool \<lparr>cdl_asid_pool_caps = transform_asid_pool_contents ap\<rparr> | ArchObj (arch_kernel_obj.PageTable ptx) \<Rightarrow> cdl_object.PageTable \<lparr>cdl_page_table_caps = transform_page_table_contents ptx\<rparr> | ArchObj (arch_kernel_obj.PageDirectory pd) \<Rightarrow> cdl_object.PageDirectory \<lparr>cdl_page_directory_caps = transform_page_directory_contents pd\<rparr> | ArchObj (DataPage dev sz) \<Rightarrow> Frame \<lparr>cdl_frame_size_bits = pageBitsForSize sz\<rparr>) = cdl_object.PageTable x6\<rbrakk> \<Longrightarrow> \<exists>b. (ptr, offset) = transform_cslot_ptr (ptr, b) \<and> cte_wp_at (\<lambda>cap'. P (transform_cap cap')) (ptr, b) s
 7. \<And>x2 ptr offset x7 z. \<lbrakk>P x2; slot = (ptr, offset); valid_objs s; valid_etcbs s; cdl_page_directory_caps x7 offset = Some x2; kheap s ptr = Some z; ptr \<noteq> idle_thread s; (case z of kernel_object.CNode 0 c \<Rightarrow> IRQNode \<lparr>cdl_irq_node_caps = transform_cnode_contents 0 c\<rparr> | kernel_object.CNode (Suc nat) c \<Rightarrow> cdl_object.CNode \<lparr>cdl_cnode_caps = transform_cnode_contents (Suc nat) c, cdl_cnode_size_bits = Suc nat\<rparr> | TCB tcb \<Rightarrow> case ekheap s ptr of Some etcb \<Rightarrow> transform_tcb (machine_state s) ptr tcb etcb | kernel_object.Endpoint x \<Rightarrow> cdl_object.Endpoint | kernel_object.Notification x \<Rightarrow> cdl_object.Notification | ArchObj (ASIDPool ap) \<Rightarrow> AsidPool \<lparr>cdl_asid_pool_caps = transform_asid_pool_contents ap\<rparr> | ArchObj (arch_kernel_obj.PageTable ptx) \<Rightarrow> cdl_object.PageTable \<lparr>cdl_page_table_caps = transform_page_table_contents ptx\<rparr> | ArchObj (arch_kernel_obj.PageDirectory pd) \<Rightarrow> cdl_object.PageDirectory \<lparr>cdl_page_directory_caps = transform_page_directory_contents pd\<rparr> | ArchObj (DataPage dev sz) \<Rightarrow> Frame \<lparr>cdl_frame_size_bits = pageBitsForSize sz\<rparr>) = cdl_object.PageDirectory x7\<rbrakk> \<Longrightarrow> \<exists>b. (ptr, offset) = transform_cslot_ptr (ptr, b) \<and> cte_wp_at (\<lambda>cap'. P (transform_cap cap')) (ptr, b) s
 8. \<And>x2 ptr offset x10 z. \<lbrakk>P x2; slot = (ptr, offset); valid_objs s; valid_etcbs s; cdl_irq_node_caps x10 offset = Some x2; kheap s ptr = Some z; ptr \<noteq> idle_thread s; (case z of kernel_object.CNode 0 c \<Rightarrow> IRQNode \<lparr>cdl_irq_node_caps = transform_cnode_contents 0 c\<rparr> | kernel_object.CNode (Suc nat) c \<Rightarrow> cdl_object.CNode \<lparr>cdl_cnode_caps = transform_cnode_contents (Suc nat) c, cdl_cnode_size_bits = Suc nat\<rparr> | TCB tcb \<Rightarrow> case ekheap s ptr of Some etcb \<Rightarrow> transform_tcb (machine_state s) ptr tcb etcb | kernel_object.Endpoint x \<Rightarrow> cdl_object.Endpoint | kernel_object.Notification x \<Rightarrow> cdl_object.Notification | ArchObj (ASIDPool ap) \<Rightarrow> AsidPool \<lparr>cdl_asid_pool_caps = transform_asid_pool_contents ap\<rparr> | ArchObj (arch_kernel_obj.PageTable ptx) \<Rightarrow> cdl_object.PageTable \<lparr>cdl_page_table_caps = transform_page_table_contents ptx\<rparr> | ArchObj (arch_kernel_obj.PageDirectory pd) \<Rightarrow> cdl_object.PageDirectory \<lparr>cdl_page_directory_caps = transform_page_directory_contents pd\<rparr> | ArchObj (DataPage dev sz) \<Rightarrow> Frame \<lparr>cdl_frame_size_bits = pageBitsForSize sz\<rparr>) = IRQNode x10\<rbrakk> \<Longrightarrow> \<exists>b. (ptr, offset) = transform_cslot_ptr (ptr, b) \<and> cte_wp_at (\<lambda>cap'. P (transform_cap cap')) (ptr, b) s proof (prove)
goal (8 subgoals):
 1. \<And>ptr offset x12 x2a x2b z. \<lbrakk>kheap s ptr = Some (kernel_object.CNode (Suc x2a) x12); ptr \<noteq> idle_thread s; P (transform_cap z); slot = (ptr, offset); valid_objs s; valid_etcbs s; nat_to_bl (Suc x2a) offset = Some x2b; x12 x2b = Some z\<rbrakk> \<Longrightarrow> \<exists>b. offset = nat (bl_to_bin b) \<and> (\<exists>cap. x12 b = Some cap \<and> P (transform_cap cap))
 2. \<And>x2 ptr offset x4 x2a. \<lbrakk>P x2; slot = (ptr, offset); valid_objs s; valid_etcbs s; cdl_cnode_caps x4 offset = Some x2; kheap s ptr = Some (TCB x2a); ptr \<noteq> idle_thread s; ekheap s ptr = None; undefined = cdl_object.CNode x4\<rbrakk> \<Longrightarrow> \<exists>b. (ptr, offset) = transform_cslot_ptr (ptr, b) \<and> cte_wp_at (\<lambda>cap'. P (transform_cap cap')) (ptr, b) s
 3. \<And>x2 ptr offset x4 x2a x2b. \<lbrakk>P x2; slot = (ptr, offset); valid_objs s; valid_etcbs s; cdl_cnode_caps x4 offset = Some x2; kheap s ptr = Some (TCB x2a); ptr \<noteq> idle_thread s; ekheap s ptr = Some x2b; transform_tcb (machine_state s) ptr x2a x2b = cdl_object.CNode x4\<rbrakk> \<Longrightarrow> \<exists>b. (ptr, offset) = transform_cslot_ptr (ptr, b) \<and> cte_wp_at (\<lambda>cap'. P (transform_cap cap')) (ptr, b) s
 4. \<And>x2 ptr offset x4 x5. \<lbrakk>P x2; slot = (ptr, offset); valid_objs s; valid_etcbs s; cdl_cnode_caps x4 offset = Some x2; kheap s ptr = Some (ArchObj x5); ptr \<noteq> idle_thread s; (case x5 of ASIDPool ap \<Rightarrow> AsidPool \<lparr>cdl_asid_pool_caps = transform_asid_pool_contents ap\<rparr> | arch_kernel_obj.PageTable ptx \<Rightarrow> cdl_object.PageTable \<lparr>cdl_page_table_caps = transform_page_table_contents ptx\<rparr> | arch_kernel_obj.PageDirectory pd \<Rightarrow> cdl_object.PageDirectory \<lparr>cdl_page_directory_caps = transform_page_directory_contents pd\<rparr> | DataPage dev sz \<Rightarrow> Frame \<lparr>cdl_frame_size_bits = pageBitsForSize sz\<rparr>) = cdl_object.CNode x4\<rbrakk> \<Longrightarrow> \<exists>b. (ptr, offset) = transform_cslot_ptr (ptr, b) \<and> cte_wp_at (\<lambda>cap'. P (transform_cap cap')) (ptr, b) s
 5. \<And>x2 ptr offset x5 z. \<lbrakk>P x2; slot = (ptr, offset); valid_objs s; valid_etcbs s; cdl_asid_pool_caps x5 offset = Some x2; kheap s ptr = Some z; ptr \<noteq> idle_thread s; (case z of kernel_object.CNode 0 c \<Rightarrow> IRQNode \<lparr>cdl_irq_node_caps = transform_cnode_contents 0 c\<rparr> | kernel_object.CNode (Suc nat) c \<Rightarrow> cdl_object.CNode \<lparr>cdl_cnode_caps = transform_cnode_contents (Suc nat) c, cdl_cnode_size_bits = Suc nat\<rparr> | TCB tcb \<Rightarrow> case ekheap s ptr of Some etcb \<Rightarrow> transform_tcb (machine_state s) ptr tcb etcb | kernel_object.Endpoint x \<Rightarrow> cdl_object.Endpoint | kernel_object.Notification x \<Rightarrow> cdl_object.Notification | ArchObj (ASIDPool ap) \<Rightarrow> AsidPool \<lparr>cdl_asid_pool_caps = transform_asid_pool_contents ap\<rparr> | ArchObj (arch_kernel_obj.PageTable ptx) \<Rightarrow> cdl_object.PageTable \<lparr>cdl_page_table_caps = transform_page_table_contents ptx\<rparr> | ArchObj (arch_kernel_obj.PageDirectory pd) \<Rightarrow> cdl_object.PageDirectory \<lparr>cdl_page_directory_caps = transform_page_directory_contents pd\<rparr> | ArchObj (DataPage dev sz) \<Rightarrow> Frame \<lparr>cdl_frame_size_bits = pageBitsForSize sz\<rparr>) = AsidPool x5\<rbrakk> \<Longrightarrow> \<exists>b. (ptr, offset) = transform_cslot_ptr (ptr, b) \<and> cte_wp_at (\<lambda>cap'. P (transform_cap cap')) (ptr, b) s
 6. \<And>x2 ptr offset x6 z. \<lbrakk>P x2; slot = (ptr, offset); valid_objs s; valid_etcbs s; cdl_page_table_caps x6 offset = Some x2; kheap s ptr = Some z; ptr \<noteq> idle_thread s; (case z of kernel_object.CNode 0 c \<Rightarrow> IRQNode \<lparr>cdl_irq_node_caps = transform_cnode_contents 0 c\<rparr> | kernel_object.CNode (Suc nat) c \<Rightarrow> cdl_object.CNode \<lparr>cdl_cnode_caps = transform_cnode_contents (Suc nat) c, cdl_cnode_size_bits = Suc nat\<rparr> | TCB tcb \<Rightarrow> case ekheap s ptr of Some etcb \<Rightarrow> transform_tcb (machine_state s) ptr tcb etcb | kernel_object.Endpoint x \<Rightarrow> cdl_object.Endpoint | kernel_object.Notification x \<Rightarrow> cdl_object.Notification | ArchObj (ASIDPool ap) \<Rightarrow> AsidPool \<lparr>cdl_asid_pool_caps = transform_asid_pool_contents ap\<rparr> | ArchObj (arch_kernel_obj.PageTable ptx) \<Rightarrow> cdl_object.PageTable \<lparr>cdl_page_table_caps = transform_page_table_contents ptx\<rparr> | ArchObj (arch_kernel_obj.PageDirectory pd) \<Rightarrow> cdl_object.PageDirectory \<lparr>cdl_page_directory_caps = transform_page_directory_contents pd\<rparr> | ArchObj (DataPage dev sz) \<Rightarrow> Frame \<lparr>cdl_frame_size_bits = pageBitsForSize sz\<rparr>) = cdl_object.PageTable x6\<rbrakk> \<Longrightarrow> \<exists>b. (ptr, offset) = transform_cslot_ptr (ptr, b) \<and> cte_wp_at (\<lambda>cap'. P (transform_cap cap')) (ptr, b) s
 7. \<And>x2 ptr offset x7 z. \<lbrakk>P x2; slot = (ptr, offset); valid_objs s; valid_etcbs s; cdl_page_directory_caps x7 offset = Some x2; kheap s ptr = Some z; ptr \<noteq> idle_thread s; (case z of kernel_object.CNode 0 c \<Rightarrow> IRQNode \<lparr>cdl_irq_node_caps = transform_cnode_contents 0 c\<rparr> | kernel_object.CNode (Suc nat) c \<Rightarrow> cdl_object.CNode \<lparr>cdl_cnode_caps = transform_cnode_contents (Suc nat) c, cdl_cnode_size_bits = Suc nat\<rparr> | TCB tcb \<Rightarrow> case ekheap s ptr of Some etcb \<Rightarrow> transform_tcb (machine_state s) ptr tcb etcb | kernel_object.Endpoint x \<Rightarrow> cdl_object.Endpoint | kernel_object.Notification x \<Rightarrow> cdl_object.Notification | ArchObj (ASIDPool ap) \<Rightarrow> AsidPool \<lparr>cdl_asid_pool_caps = transform_asid_pool_contents ap\<rparr> | ArchObj (arch_kernel_obj.PageTable ptx) \<Rightarrow> cdl_object.PageTable \<lparr>cdl_page_table_caps = transform_page_table_contents ptx\<rparr> | ArchObj (arch_kernel_obj.PageDirectory pd) \<Rightarrow> cdl_object.PageDirectory \<lparr>cdl_page_directory_caps = transform_page_directory_contents pd\<rparr> | ArchObj (DataPage dev sz) \<Rightarrow> Frame \<lparr>cdl_frame_size_bits = pageBitsForSize sz\<rparr>) = cdl_object.PageDirectory x7\<rbrakk> \<Longrightarrow> \<exists>b. (ptr, offset) = transform_cslot_ptr (ptr, b) \<and> cte_wp_at (\<lambda>cap'. P (transform_cap cap')) (ptr, b) s
 8. \<And>x2 ptr offset x10 z. \<lbrakk>P x2; slot = (ptr, offset); valid_objs s; valid_etcbs s; cdl_irq_node_caps x10 offset = Some x2; kheap s ptr = Some z; ptr \<noteq> idle_thread s; (case z of kernel_object.CNode 0 c \<Rightarrow> IRQNode \<lparr>cdl_irq_node_caps = transform_cnode_contents 0 c\<rparr> | kernel_object.CNode (Suc nat) c \<Rightarrow> cdl_object.CNode \<lparr>cdl_cnode_caps = transform_cnode_contents (Suc nat) c, cdl_cnode_size_bits = Suc nat\<rparr> | TCB tcb \<Rightarrow> case ekheap s ptr of Some etcb \<Rightarrow> transform_tcb (machine_state s) ptr tcb etcb | kernel_object.Endpoint x \<Rightarrow> cdl_object.Endpoint | kernel_object.Notification x \<Rightarrow> cdl_object.Notification | ArchObj (ASIDPool ap) \<Rightarrow> AsidPool \<lparr>cdl_asid_pool_caps = transform_asid_pool_contents ap\<rparr> | ArchObj (arch_kernel_obj.PageTable ptx) \<Rightarrow> cdl_object.PageTable \<lparr>cdl_page_table_caps = transform_page_table_contents ptx\<rparr> | ArchObj (arch_kernel_obj.PageDirectory pd) \<Rightarrow> cdl_object.PageDirectory \<lparr>cdl_page_directory_caps = transform_page_directory_contents pd\<rparr> | ArchObj (DataPage dev sz) \<Rightarrow> Frame \<lparr>cdl_frame_size_bits = pageBitsForSize sz\<rparr>) = IRQNode x10\<rbrakk> \<Longrightarrow> \<exists>b. (ptr, offset) = transform_cslot_ptr (ptr, b) \<and> cte_wp_at (\<lambda>cap'. P (transform_cap cap')) (ptr, b) s proof (prove)
goal (7 subgoals):
 1. \<And>x2 ptr offset x4 x2a. \<lbrakk>P x2; slot = (ptr, offset); valid_objs s; valid_etcbs s; cdl_cnode_caps x4 offset = Some x2; kheap s ptr = Some (TCB x2a); ptr \<noteq> idle_thread s; ekheap s ptr = None; undefined = cdl_object.CNode x4\<rbrakk> \<Longrightarrow> \<exists>b. (ptr, offset) = transform_cslot_ptr (ptr, b) \<and> cte_wp_at (\<lambda>cap'. P (transform_cap cap')) (ptr, b) s
 2. \<And>x2 ptr offset x4 x2a x2b. \<lbrakk>P x2; slot = (ptr, offset); valid_objs s; valid_etcbs s; cdl_cnode_caps x4 offset = Some x2; kheap s ptr = Some (TCB x2a); ptr \<noteq> idle_thread s; ekheap s ptr = Some x2b; transform_tcb (machine_state s) ptr x2a x2b = cdl_object.CNode x4\<rbrakk> \<Longrightarrow> \<exists>b. (ptr, offset) = transform_cslot_ptr (ptr, b) \<and> cte_wp_at (\<lambda>cap'. P (transform_cap cap')) (ptr, b) s
 3. \<And>x2 ptr offset x4 x5. \<lbrakk>P x2; slot = (ptr, offset); valid_objs s; valid_etcbs s; cdl_cnode_caps x4 offset = Some x2; kheap s ptr = Some (ArchObj x5); ptr \<noteq> idle_thread s; (case x5 of ASIDPool ap \<Rightarrow> AsidPool \<lparr>cdl_asid_pool_caps = transform_asid_pool_contents ap\<rparr> | arch_kernel_obj.PageTable ptx \<Rightarrow> cdl_object.PageTable \<lparr>cdl_page_table_caps = transform_page_table_contents ptx\<rparr> | arch_kernel_obj.PageDirectory pd \<Rightarrow> cdl_object.PageDirectory \<lparr>cdl_page_directory_caps = transform_page_directory_contents pd\<rparr> | DataPage dev sz \<Rightarrow> Frame \<lparr>cdl_frame_size_bits = pageBitsForSize sz\<rparr>) = cdl_object.CNode x4\<rbrakk> \<Longrightarrow> \<exists>b. (ptr, offset) = transform_cslot_ptr (ptr, b) \<and> cte_wp_at (\<lambda>cap'. P (transform_cap cap')) (ptr, b) s
 4. \<And>x2 ptr offset x5 z. \<lbrakk>P x2; slot = (ptr, offset); valid_objs s; valid_etcbs s; cdl_asid_pool_caps x5 offset = Some x2; kheap s ptr = Some z; ptr \<noteq> idle_thread s; (case z of kernel_object.CNode 0 c \<Rightarrow> IRQNode \<lparr>cdl_irq_node_caps = transform_cnode_contents 0 c\<rparr> | kernel_object.CNode (Suc nat) c \<Rightarrow> cdl_object.CNode \<lparr>cdl_cnode_caps = transform_cnode_contents (Suc nat) c, cdl_cnode_size_bits = Suc nat\<rparr> | TCB tcb \<Rightarrow> case ekheap s ptr of Some etcb \<Rightarrow> transform_tcb (machine_state s) ptr tcb etcb | kernel_object.Endpoint x \<Rightarrow> cdl_object.Endpoint | kernel_object.Notification x \<Rightarrow> cdl_object.Notification | ArchObj (ASIDPool ap) \<Rightarrow> AsidPool \<lparr>cdl_asid_pool_caps = transform_asid_pool_contents ap\<rparr> | ArchObj (arch_kernel_obj.PageTable ptx) \<Rightarrow> cdl_object.PageTable \<lparr>cdl_page_table_caps = transform_page_table_contents ptx\<rparr> | ArchObj (arch_kernel_obj.PageDirectory pd) \<Rightarrow> cdl_object.PageDirectory \<lparr>cdl_page_directory_caps = transform_page_directory_contents pd\<rparr> | ArchObj (DataPage dev sz) \<Rightarrow> Frame \<lparr>cdl_frame_size_bits = pageBitsForSize sz\<rparr>) = AsidPool x5\<rbrakk> \<Longrightarrow> \<exists>b. (ptr, offset) = transform_cslot_ptr (ptr, b) \<and> cte_wp_at (\<lambda>cap'. P (transform_cap cap')) (ptr, b) s
 5. \<And>x2 ptr offset x6 z. \<lbrakk>P x2; slot = (ptr, offset); valid_objs s; valid_etcbs s; cdl_page_table_caps x6 offset = Some x2; kheap s ptr = Some z; ptr \<noteq> idle_thread s; (case z of kernel_object.CNode 0 c \<Rightarrow> IRQNode \<lparr>cdl_irq_node_caps = transform_cnode_contents 0 c\<rparr> | kernel_object.CNode (Suc nat) c \<Rightarrow> cdl_object.CNode \<lparr>cdl_cnode_caps = transform_cnode_contents (Suc nat) c, cdl_cnode_size_bits = Suc nat\<rparr> | TCB tcb \<Rightarrow> case ekheap s ptr of Some etcb \<Rightarrow> transform_tcb (machine_state s) ptr tcb etcb | kernel_object.Endpoint x \<Rightarrow> cdl_object.Endpoint | kernel_object.Notification x \<Rightarrow> cdl_object.Notification | ArchObj (ASIDPool ap) \<Rightarrow> AsidPool \<lparr>cdl_asid_pool_caps = transform_asid_pool_contents ap\<rparr> | ArchObj (arch_kernel_obj.PageTable ptx) \<Rightarrow> cdl_object.PageTable \<lparr>cdl_page_table_caps = transform_page_table_contents ptx\<rparr> | ArchObj (arch_kernel_obj.PageDirectory pd) \<Rightarrow> cdl_object.PageDirectory \<lparr>cdl_page_directory_caps = transform_page_directory_contents pd\<rparr> | ArchObj (DataPage dev sz) \<Rightarrow> Frame \<lparr>cdl_frame_size_bits = pageBitsForSize sz\<rparr>) = cdl_object.PageTable x6\<rbrakk> \<Longrightarrow> \<exists>b. (ptr, offset) = transform_cslot_ptr (ptr, b) \<and> cte_wp_at (\<lambda>cap'. P (transform_cap cap')) (ptr, b) s
 6. \<And>x2 ptr offset x7 z. \<lbrakk>P x2; slot = (ptr, offset); valid_objs s; valid_etcbs s; cdl_page_directory_caps x7 offset = Some x2; kheap s ptr = Some z; ptr \<noteq> idle_thread s; (case z of kernel_object.CNode 0 c \<Rightarrow> IRQNode \<lparr>cdl_irq_node_caps = transform_cnode_contents 0 c\<rparr> | kernel_object.CNode (Suc nat) c \<Rightarrow> cdl_object.CNode \<lparr>cdl_cnode_caps = transform_cnode_contents (Suc nat) c, cdl_cnode_size_bits = Suc nat\<rparr> | TCB tcb \<Rightarrow> case ekheap s ptr of Some etcb \<Rightarrow> transform_tcb (machine_state s) ptr tcb etcb | kernel_object.Endpoint x \<Rightarrow> cdl_object.Endpoint | kernel_object.Notification x \<Rightarrow> cdl_object.Notification | ArchObj (ASIDPool ap) \<Rightarrow> AsidPool \<lparr>cdl_asid_pool_caps = transform_asid_pool_contents ap\<rparr> | ArchObj (arch_kernel_obj.PageTable ptx) \<Rightarrow> cdl_object.PageTable \<lparr>cdl_page_table_caps = transform_page_table_contents ptx\<rparr> | ArchObj (arch_kernel_obj.PageDirectory pd) \<Rightarrow> cdl_object.PageDirectory \<lparr>cdl_page_directory_caps = transform_page_directory_contents pd\<rparr> | ArchObj (DataPage dev sz) \<Rightarrow> Frame \<lparr>cdl_frame_size_bits = pageBitsForSize sz\<rparr>) = cdl_object.PageDirectory x7\<rbrakk> \<Longrightarrow> \<exists>b. (ptr, offset) = transform_cslot_ptr (ptr, b) \<and> cte_wp_at (\<lambda>cap'. P (transform_cap cap')) (ptr, b) s
 7. \<And>x2 ptr offset x10 z. \<lbrakk>P x2; slot = (ptr, offset); valid_objs s; valid_etcbs s; cdl_irq_node_caps x10 offset = Some x2; kheap s ptr = Some z; ptr \<noteq> idle_thread s; (case z of kernel_object.CNode 0 c \<Rightarrow> IRQNode \<lparr>cdl_irq_node_caps = transform_cnode_contents 0 c\<rparr> | kernel_object.CNode (Suc nat) c \<Rightarrow> cdl_object.CNode \<lparr>cdl_cnode_caps = transform_cnode_contents (Suc nat) c, cdl_cnode_size_bits = Suc nat\<rparr> | TCB tcb \<Rightarrow> case ekheap s ptr of Some etcb \<Rightarrow> transform_tcb (machine_state s) ptr tcb etcb | kernel_object.Endpoint x \<Rightarrow> cdl_object.Endpoint | kernel_object.Notification x \<Rightarrow> cdl_object.Notification | ArchObj (ASIDPool ap) \<Rightarrow> AsidPool \<lparr>cdl_asid_pool_caps = transform_asid_pool_contents ap\<rparr> | ArchObj (arch_kernel_obj.PageTable ptx) \<Rightarrow> cdl_object.PageTable \<lparr>cdl_page_table_caps = transform_page_table_contents ptx\<rparr> | ArchObj (arch_kernel_obj.PageDirectory pd) \<Rightarrow> cdl_object.PageDirectory \<lparr>cdl_page_directory_caps = transform_page_directory_contents pd\<rparr> | ArchObj (DataPage dev sz) \<Rightarrow> Frame \<lparr>cdl_frame_size_bits = pageBitsForSize sz\<rparr>) = IRQNode x10\<rbrakk> \<Longrightarrow> \<exists>b. (ptr, offset) = transform_cslot_ptr (ptr, b) \<and> cte_wp_at (\<lambda>cap'. P (transform_cap cap')) (ptr, b) s proof (prove)
goal (6 subgoals):
 1. \<And>x2 ptr offset x4 x2a x2b. \<lbrakk>P x2; slot = (ptr, offset); valid_objs s; valid_etcbs s; cdl_cnode_caps x4 offset = Some x2; kheap s ptr = Some (TCB x2a); ptr \<noteq> idle_thread s; ekheap s ptr = Some x2b; transform_tcb (machine_state s) ptr x2a x2b = cdl_object.CNode x4\<rbrakk> \<Longrightarrow> \<exists>b. (ptr, offset) = transform_cslot_ptr (ptr, b) \<and> cte_wp_at (\<lambda>cap'. P (transform_cap cap')) (ptr, b) s
 2. \<And>x2 ptr offset x4 x5. \<lbrakk>P x2; slot = (ptr, offset); valid_objs s; valid_etcbs s; cdl_cnode_caps x4 offset = Some x2; kheap s ptr = Some (ArchObj x5); ptr \<noteq> idle_thread s; (case x5 of ASIDPool ap \<Rightarrow> AsidPool \<lparr>cdl_asid_pool_caps = transform_asid_pool_contents ap\<rparr> | arch_kernel_obj.PageTable ptx \<Rightarrow> cdl_object.PageTable \<lparr>cdl_page_table_caps = transform_page_table_contents ptx\<rparr> | arch_kernel_obj.PageDirectory pd \<Rightarrow> cdl_object.PageDirectory \<lparr>cdl_page_directory_caps = transform_page_directory_contents pd\<rparr> | DataPage dev sz \<Rightarrow> Frame \<lparr>cdl_frame_size_bits = pageBitsForSize sz\<rparr>) = cdl_object.CNode x4\<rbrakk> \<Longrightarrow> \<exists>b. (ptr, offset) = transform_cslot_ptr (ptr, b) \<and> cte_wp_at (\<lambda>cap'. P (transform_cap cap')) (ptr, b) s
 3. \<And>x2 ptr offset x5 z. \<lbrakk>P x2; slot = (ptr, offset); valid_objs s; valid_etcbs s; cdl_asid_pool_caps x5 offset = Some x2; kheap s ptr = Some z; ptr \<noteq> idle_thread s; (case z of kernel_object.CNode 0 c \<Rightarrow> IRQNode \<lparr>cdl_irq_node_caps = transform_cnode_contents 0 c\<rparr> | kernel_object.CNode (Suc nat) c \<Rightarrow> cdl_object.CNode \<lparr>cdl_cnode_caps = transform_cnode_contents (Suc nat) c, cdl_cnode_size_bits = Suc nat\<rparr> | TCB tcb \<Rightarrow> case ekheap s ptr of Some etcb \<Rightarrow> transform_tcb (machine_state s) ptr tcb etcb | kernel_object.Endpoint x \<Rightarrow> cdl_object.Endpoint | kernel_object.Notification x \<Rightarrow> cdl_object.Notification | ArchObj (ASIDPool ap) \<Rightarrow> AsidPool \<lparr>cdl_asid_pool_caps = transform_asid_pool_contents ap\<rparr> | ArchObj (arch_kernel_obj.PageTable ptx) \<Rightarrow> cdl_object.PageTable \<lparr>cdl_page_table_caps = transform_page_table_contents ptx\<rparr> | ArchObj (arch_kernel_obj.PageDirectory pd) \<Rightarrow> cdl_object.PageDirectory \<lparr>cdl_page_directory_caps = transform_page_directory_contents pd\<rparr> | ArchObj (DataPage dev sz) \<Rightarrow> Frame \<lparr>cdl_frame_size_bits = pageBitsForSize sz\<rparr>) = AsidPool x5\<rbrakk> \<Longrightarrow> \<exists>b. (ptr, offset) = transform_cslot_ptr (ptr, b) \<and> cte_wp_at (\<lambda>cap'. P (transform_cap cap')) (ptr, b) s
 4. \<And>x2 ptr offset x6 z. \<lbrakk>P x2; slot = (ptr, offset); valid_objs s; valid_etcbs s; cdl_page_table_caps x6 offset = Some x2; kheap s ptr = Some z; ptr \<noteq> idle_thread s; (case z of kernel_object.CNode 0 c \<Rightarrow> IRQNode \<lparr>cdl_irq_node_caps = transform_cnode_contents 0 c\<rparr> | kernel_object.CNode (Suc nat) c \<Rightarrow> cdl_object.CNode \<lparr>cdl_cnode_caps = transform_cnode_contents (Suc nat) c, cdl_cnode_size_bits = Suc nat\<rparr> | TCB tcb \<Rightarrow> case ekheap s ptr of Some etcb \<Rightarrow> transform_tcb (machine_state s) ptr tcb etcb | kernel_object.Endpoint x \<Rightarrow> cdl_object.Endpoint | kernel_object.Notification x \<Rightarrow> cdl_object.Notification | ArchObj (ASIDPool ap) \<Rightarrow> AsidPool \<lparr>cdl_asid_pool_caps = transform_asid_pool_contents ap\<rparr> | ArchObj (arch_kernel_obj.PageTable ptx) \<Rightarrow> cdl_object.PageTable \<lparr>cdl_page_table_caps = transform_page_table_contents ptx\<rparr> | ArchObj (arch_kernel_obj.PageDirectory pd) \<Rightarrow> cdl_object.PageDirectory \<lparr>cdl_page_directory_caps = transform_page_directory_contents pd\<rparr> | ArchObj (DataPage dev sz) \<Rightarrow> Frame \<lparr>cdl_frame_size_bits = pageBitsForSize sz\<rparr>) = cdl_object.PageTable x6\<rbrakk> \<Longrightarrow> \<exists>b. (ptr, offset) = transform_cslot_ptr (ptr, b) \<and> cte_wp_at (\<lambda>cap'. P (transform_cap cap')) (ptr, b) s
 5. \<And>x2 ptr offset x7 z. \<lbrakk>P x2; slot = (ptr, offset); valid_objs s; valid_etcbs s; cdl_page_directory_caps x7 offset = Some x2; kheap s ptr = Some z; ptr \<noteq> idle_thread s; (case z of kernel_object.CNode 0 c \<Rightarrow> IRQNode \<lparr>cdl_irq_node_caps = transform_cnode_contents 0 c\<rparr> | kernel_object.CNode (Suc nat) c \<Rightarrow> cdl_object.CNode \<lparr>cdl_cnode_caps = transform_cnode_contents (Suc nat) c, cdl_cnode_size_bits = Suc nat\<rparr> | TCB tcb \<Rightarrow> case ekheap s ptr of Some etcb \<Rightarrow> transform_tcb (machine_state s) ptr tcb etcb | kernel_object.Endpoint x \<Rightarrow> cdl_object.Endpoint | kernel_object.Notification x \<Rightarrow> cdl_object.Notification | ArchObj (ASIDPool ap) \<Rightarrow> AsidPool \<lparr>cdl_asid_pool_caps = transform_asid_pool_contents ap\<rparr> | ArchObj (arch_kernel_obj.PageTable ptx) \<Rightarrow> cdl_object.PageTable \<lparr>cdl_page_table_caps = transform_page_table_contents ptx\<rparr> | ArchObj (arch_kernel_obj.PageDirectory pd) \<Rightarrow> cdl_object.PageDirectory \<lparr>cdl_page_directory_caps = transform_page_directory_contents pd\<rparr> | ArchObj (DataPage dev sz) \<Rightarrow> Frame \<lparr>cdl_frame_size_bits = pageBitsForSize sz\<rparr>) = cdl_object.PageDirectory x7\<rbrakk> \<Longrightarrow> \<exists>b. (ptr, offset) = transform_cslot_ptr (ptr, b) \<and> cte_wp_at (\<lambda>cap'. P (transform_cap cap')) (ptr, b) s
 6. \<And>x2 ptr offset x10 z. \<lbrakk>P x2; slot = (ptr, offset); valid_objs s; valid_etcbs s; cdl_irq_node_caps x10 offset = Some x2; kheap s ptr = Some z; ptr \<noteq> idle_thread s; (case z of kernel_object.CNode 0 c \<Rightarrow> IRQNode \<lparr>cdl_irq_node_caps = transform_cnode_contents 0 c\<rparr> | kernel_object.CNode (Suc nat) c \<Rightarrow> cdl_object.CNode \<lparr>cdl_cnode_caps = transform_cnode_contents (Suc nat) c, cdl_cnode_size_bits = Suc nat\<rparr> | TCB tcb \<Rightarrow> case ekheap s ptr of Some etcb \<Rightarrow> transform_tcb (machine_state s) ptr tcb etcb | kernel_object.Endpoint x \<Rightarrow> cdl_object.Endpoint | kernel_object.Notification x \<Rightarrow> cdl_object.Notification | ArchObj (ASIDPool ap) \<Rightarrow> AsidPool \<lparr>cdl_asid_pool_caps = transform_asid_pool_contents ap\<rparr> | ArchObj (arch_kernel_obj.PageTable ptx) \<Rightarrow> cdl_object.PageTable \<lparr>cdl_page_table_caps = transform_page_table_contents ptx\<rparr> | ArchObj (arch_kernel_obj.PageDirectory pd) \<Rightarrow> cdl_object.PageDirectory \<lparr>cdl_page_directory_caps = transform_page_directory_contents pd\<rparr> | ArchObj (DataPage dev sz) \<Rightarrow> Frame \<lparr>cdl_frame_size_bits = pageBitsForSize sz\<rparr>) = IRQNode x10\<rbrakk> \<Longrightarrow> \<exists>b. (ptr, offset) = transform_cslot_ptr (ptr, b) \<and> cte_wp_at (\<lambda>cap'. P (transform_cap cap')) (ptr, b) s proof (prove)
goal (6 subgoals):
 1. \<And>x2 ptr offset x10 z. \<lbrakk>P x2; slot = (ptr, offset); valid_objs s; valid_etcbs s; cdl_irq_node_caps x10 offset = Some x2; kheap s ptr = Some z; ptr \<noteq> idle_thread s; (case z of kernel_object.CNode 0 c \<Rightarrow> IRQNode \<lparr>cdl_irq_node_caps = transform_cnode_contents 0 c\<rparr> | kernel_object.CNode (Suc nat) c \<Rightarrow> cdl_object.CNode \<lparr>cdl_cnode_caps = transform_cnode_contents (Suc nat) c, cdl_cnode_size_bits = Suc nat\<rparr> | TCB tcb \<Rightarrow> case ekheap s ptr of Some etcb \<Rightarrow> transform_tcb (machine_state s) ptr tcb etcb | kernel_object.Endpoint x \<Rightarrow> cdl_object.Endpoint | kernel_object.Notification x \<Rightarrow> cdl_object.Notification | ArchObj (ASIDPool ap) \<Rightarrow> AsidPool \<lparr>cdl_asid_pool_caps = transform_asid_pool_contents ap\<rparr> | ArchObj (arch_kernel_obj.PageTable ptx) \<Rightarrow> cdl_object.PageTable \<lparr>cdl_page_table_caps = transform_page_table_contents ptx\<rparr> | ArchObj (arch_kernel_obj.PageDirectory pd) \<Rightarrow> cdl_object.PageDirectory \<lparr>cdl_page_directory_caps = transform_page_directory_contents pd\<rparr> | ArchObj (DataPage dev sz) \<Rightarrow> Frame \<lparr>cdl_frame_size_bits = pageBitsForSize sz\<rparr>) = IRQNode x10\<rbrakk> \<Longrightarrow> \<exists>b. (ptr, offset) = transform_cslot_ptr (ptr, b) \<and> cte_wp_at (\<lambda>cap'. P (transform_cap cap')) (ptr, b) s
 2. \<And>x2 ptr offset x4 x2a x2b. \<lbrakk>P x2; slot = (ptr, offset); valid_objs s; valid_etcbs s; cdl_cnode_caps x4 offset = Some x2; kheap s ptr = Some (TCB x2a); ptr \<noteq> idle_thread s; ekheap s ptr = Some x2b; transform_tcb (machine_state s) ptr x2a x2b = cdl_object.CNode x4\<rbrakk> \<Longrightarrow> \<exists>b. (ptr, offset) = transform_cslot_ptr (ptr, b) \<and> cte_wp_at (\<lambda>cap'. P (transform_cap cap')) (ptr, b) s
 3. \<And>x2 ptr offset x4 x5. \<lbrakk>P x2; slot = (ptr, offset); valid_objs s; valid_etcbs s; cdl_cnode_caps x4 offset = Some x2; kheap s ptr = Some (ArchObj x5); ptr \<noteq> idle_thread s; (case x5 of ASIDPool ap \<Rightarrow> AsidPool \<lparr>cdl_asid_pool_caps = transform_asid_pool_contents ap\<rparr> | arch_kernel_obj.PageTable ptx \<Rightarrow> cdl_object.PageTable \<lparr>cdl_page_table_caps = transform_page_table_contents ptx\<rparr> | arch_kernel_obj.PageDirectory pd \<Rightarrow> cdl_object.PageDirectory \<lparr>cdl_page_directory_caps = transform_page_directory_contents pd\<rparr> | DataPage dev sz \<Rightarrow> Frame \<lparr>cdl_frame_size_bits = pageBitsForSize sz\<rparr>) = cdl_object.CNode x4\<rbrakk> \<Longrightarrow> \<exists>b. (ptr, offset) = transform_cslot_ptr (ptr, b) \<and> cte_wp_at (\<lambda>cap'. P (transform_cap cap')) (ptr, b) s
 4. \<And>x2 ptr offset x5 z. \<lbrakk>P x2; slot = (ptr, offset); valid_objs s; valid_etcbs s; cdl_asid_pool_caps x5 offset = Some x2; kheap s ptr = Some z; ptr \<noteq> idle_thread s; (case z of kernel_object.CNode 0 c \<Rightarrow> IRQNode \<lparr>cdl_irq_node_caps = transform_cnode_contents 0 c\<rparr> | kernel_object.CNode (Suc nat) c \<Rightarrow> cdl_object.CNode \<lparr>cdl_cnode_caps = transform_cnode_contents (Suc nat) c, cdl_cnode_size_bits = Suc nat\<rparr> | TCB tcb \<Rightarrow> case ekheap s ptr of Some etcb \<Rightarrow> transform_tcb (machine_state s) ptr tcb etcb | kernel_object.Endpoint x \<Rightarrow> cdl_object.Endpoint | kernel_object.Notification x \<Rightarrow> cdl_object.Notification | ArchObj (ASIDPool ap) \<Rightarrow> AsidPool \<lparr>cdl_asid_pool_caps = transform_asid_pool_contents ap\<rparr> | ArchObj (arch_kernel_obj.PageTable ptx) \<Rightarrow> cdl_object.PageTable \<lparr>cdl_page_table_caps = transform_page_table_contents ptx\<rparr> | ArchObj (arch_kernel_obj.PageDirectory pd) \<Rightarrow> cdl_object.PageDirectory \<lparr>cdl_page_directory_caps = transform_page_directory_contents pd\<rparr> | ArchObj (DataPage dev sz) \<Rightarrow> Frame \<lparr>cdl_frame_size_bits = pageBitsForSize sz\<rparr>) = AsidPool x5\<rbrakk> \<Longrightarrow> \<exists>b. (ptr, offset) = transform_cslot_ptr (ptr, b) \<and> cte_wp_at (\<lambda>cap'. P (transform_cap cap')) (ptr, b) s
 5. \<And>x2 ptr offset x6 z. \<lbrakk>P x2; slot = (ptr, offset); valid_objs s; valid_etcbs s; cdl_page_table_caps x6 offset = Some x2; kheap s ptr = Some z; ptr \<noteq> idle_thread s; (case z of kernel_object.CNode 0 c \<Rightarrow> IRQNode \<lparr>cdl_irq_node_caps = transform_cnode_contents 0 c\<rparr> | kernel_object.CNode (Suc nat) c \<Rightarrow> cdl_object.CNode \<lparr>cdl_cnode_caps = transform_cnode_contents (Suc nat) c, cdl_cnode_size_bits = Suc nat\<rparr> | TCB tcb \<Rightarrow> case ekheap s ptr of Some etcb \<Rightarrow> transform_tcb (machine_state s) ptr tcb etcb | kernel_object.Endpoint x \<Rightarrow> cdl_object.Endpoint | kernel_object.Notification x \<Rightarrow> cdl_object.Notification | ArchObj (ASIDPool ap) \<Rightarrow> AsidPool \<lparr>cdl_asid_pool_caps = transform_asid_pool_contents ap\<rparr> | ArchObj (arch_kernel_obj.PageTable ptx) \<Rightarrow> cdl_object.PageTable \<lparr>cdl_page_table_caps = transform_page_table_contents ptx\<rparr> | ArchObj (arch_kernel_obj.PageDirectory pd) \<Rightarrow> cdl_object.PageDirectory \<lparr>cdl_page_directory_caps = transform_page_directory_contents pd\<rparr> | ArchObj (DataPage dev sz) \<Rightarrow> Frame \<lparr>cdl_frame_size_bits = pageBitsForSize sz\<rparr>) = cdl_object.PageTable x6\<rbrakk> \<Longrightarrow> \<exists>b. (ptr, offset) = transform_cslot_ptr (ptr, b) \<and> cte_wp_at (\<lambda>cap'. P (transform_cap cap')) (ptr, b) s
 6. \<And>x2 ptr offset x7 z. \<lbrakk>P x2; slot = (ptr, offset); valid_objs s; valid_etcbs s; cdl_page_directory_caps x7 offset = Some x2; kheap s ptr = Some z; ptr \<noteq> idle_thread s; (case z of kernel_object.CNode 0 c \<Rightarrow> IRQNode \<lparr>cdl_irq_node_caps = transform_cnode_contents 0 c\<rparr> | kernel_object.CNode (Suc nat) c \<Rightarrow> cdl_object.CNode \<lparr>cdl_cnode_caps = transform_cnode_contents (Suc nat) c, cdl_cnode_size_bits = Suc nat\<rparr> | TCB tcb \<Rightarrow> case ekheap s ptr of Some etcb \<Rightarrow> transform_tcb (machine_state s) ptr tcb etcb | kernel_object.Endpoint x \<Rightarrow> cdl_object.Endpoint | kernel_object.Notification x \<Rightarrow> cdl_object.Notification | ArchObj (ASIDPool ap) \<Rightarrow> AsidPool \<lparr>cdl_asid_pool_caps = transform_asid_pool_contents ap\<rparr> | ArchObj (arch_kernel_obj.PageTable ptx) \<Rightarrow> cdl_object.PageTable \<lparr>cdl_page_table_caps = transform_page_table_contents ptx\<rparr> | ArchObj (arch_kernel_obj.PageDirectory pd) \<Rightarrow> cdl_object.PageDirectory \<lparr>cdl_page_directory_caps = transform_page_directory_contents pd\<rparr> | ArchObj (DataPage dev sz) \<Rightarrow> Frame \<lparr>cdl_frame_size_bits = pageBitsForSize sz\<rparr>) = cdl_object.PageDirectory x7\<rbrakk> \<Longrightarrow> \<exists>b. (ptr, offset) = transform_cslot_ptr (ptr, b) \<and> cte_wp_at (\<lambda>cap'. P (transform_cap cap')) (ptr, b) s proof (prove)
goal (6 subgoals):
 1. \<And>x2 ptr offset x10 z. \<lbrakk>P x2; slot = (ptr, offset); valid_objs s; valid_etcbs s; cdl_irq_node_caps x10 offset = Some x2; kheap s ptr = Some z; ptr \<noteq> idle_thread s; (case z of kernel_object.CNode 0 c \<Rightarrow> IRQNode \<lparr>cdl_irq_node_caps = transform_cnode_contents 0 c\<rparr> | kernel_object.CNode (Suc nat) c \<Rightarrow> cdl_object.CNode \<lparr>cdl_cnode_caps = transform_cnode_contents (Suc nat) c, cdl_cnode_size_bits = Suc nat\<rparr> | TCB tcb \<Rightarrow> case ekheap s ptr of Some etcb \<Rightarrow> transform_tcb (machine_state s) ptr tcb etcb | kernel_object.Endpoint x \<Rightarrow> cdl_object.Endpoint | kernel_object.Notification x \<Rightarrow> cdl_object.Notification | ArchObj (ASIDPool ap) \<Rightarrow> AsidPool \<lparr>cdl_asid_pool_caps = transform_asid_pool_contents ap\<rparr> | ArchObj (arch_kernel_obj.PageTable ptx) \<Rightarrow> cdl_object.PageTable \<lparr>cdl_page_table_caps = transform_page_table_contents ptx\<rparr> | ArchObj (arch_kernel_obj.PageDirectory pd) \<Rightarrow> cdl_object.PageDirectory \<lparr>cdl_page_directory_caps = transform_page_directory_contents pd\<rparr> | ArchObj (DataPage dev sz) \<Rightarrow> Frame \<lparr>cdl_frame_size_bits = pageBitsForSize sz\<rparr>) = IRQNode x10\<rbrakk> \<Longrightarrow> \<exists>b. (ptr, offset) = transform_cslot_ptr (ptr, b) \<and> cte_wp_at (\<lambda>cap'. P (transform_cap cap')) (ptr, b) s
 2. \<And>x2 ptr offset x4 x2a x2b. \<lbrakk>P x2; slot = (ptr, offset); valid_objs s; valid_etcbs s; cdl_cnode_caps x4 offset = Some x2; kheap s ptr = Some (TCB x2a); ptr \<noteq> idle_thread s; ekheap s ptr = Some x2b; transform_tcb (machine_state s) ptr x2a x2b = cdl_object.CNode x4\<rbrakk> \<Longrightarrow> \<exists>b. (ptr, offset) = transform_cslot_ptr (ptr, b) \<and> cte_wp_at (\<lambda>cap'. P (transform_cap cap')) (ptr, b) s
 3. \<And>x2 ptr offset x4 x5. \<lbrakk>P x2; slot = (ptr, offset); valid_objs s; valid_etcbs s; cdl_cnode_caps x4 offset = Some x2; kheap s ptr = Some (ArchObj x5); ptr \<noteq> idle_thread s; (case x5 of ASIDPool ap \<Rightarrow> AsidPool \<lparr>cdl_asid_pool_caps = transform_asid_pool_contents ap\<rparr> | arch_kernel_obj.PageTable ptx \<Rightarrow> cdl_object.PageTable \<lparr>cdl_page_table_caps = transform_page_table_contents ptx\<rparr> | arch_kernel_obj.PageDirectory pd \<Rightarrow> cdl_object.PageDirectory \<lparr>cdl_page_directory_caps = transform_page_directory_contents pd\<rparr> | DataPage dev sz \<Rightarrow> Frame \<lparr>cdl_frame_size_bits = pageBitsForSize sz\<rparr>) = cdl_object.CNode x4\<rbrakk> \<Longrightarrow> \<exists>b. (ptr, offset) = transform_cslot_ptr (ptr, b) \<and> cte_wp_at (\<lambda>cap'. P (transform_cap cap')) (ptr, b) s
 4. \<And>x2 ptr offset x5 z. \<lbrakk>P x2; slot = (ptr, offset); valid_objs s; valid_etcbs s; cdl_asid_pool_caps x5 offset = Some x2; kheap s ptr = Some z; ptr \<noteq> idle_thread s; (case z of kernel_object.CNode 0 c \<Rightarrow> IRQNode \<lparr>cdl_irq_node_caps = transform_cnode_contents 0 c\<rparr> | kernel_object.CNode (Suc nat) c \<Rightarrow> cdl_object.CNode \<lparr>cdl_cnode_caps = transform_cnode_contents (Suc nat) c, cdl_cnode_size_bits = Suc nat\<rparr> | TCB tcb \<Rightarrow> case ekheap s ptr of Some etcb \<Rightarrow> transform_tcb (machine_state s) ptr tcb etcb | kernel_object.Endpoint x \<Rightarrow> cdl_object.Endpoint | kernel_object.Notification x \<Rightarrow> cdl_object.Notification | ArchObj (ASIDPool ap) \<Rightarrow> AsidPool \<lparr>cdl_asid_pool_caps = transform_asid_pool_contents ap\<rparr> | ArchObj (arch_kernel_obj.PageTable ptx) \<Rightarrow> cdl_object.PageTable \<lparr>cdl_page_table_caps = transform_page_table_contents ptx\<rparr> | ArchObj (arch_kernel_obj.PageDirectory pd) \<Rightarrow> cdl_object.PageDirectory \<lparr>cdl_page_directory_caps = transform_page_directory_contents pd\<rparr> | ArchObj (DataPage dev sz) \<Rightarrow> Frame \<lparr>cdl_frame_size_bits = pageBitsForSize sz\<rparr>) = AsidPool x5\<rbrakk> \<Longrightarrow> \<exists>b. (ptr, offset) = transform_cslot_ptr (ptr, b) \<and> cte_wp_at (\<lambda>cap'. P (transform_cap cap')) (ptr, b) s
 5. \<And>x2 ptr offset x6 z. \<lbrakk>P x2; slot = (ptr, offset); valid_objs s; valid_etcbs s; cdl_page_table_caps x6 offset = Some x2; kheap s ptr = Some z; ptr \<noteq> idle_thread s; (case z of kernel_object.CNode 0 c \<Rightarrow> IRQNode \<lparr>cdl_irq_node_caps = transform_cnode_contents 0 c\<rparr> | kernel_object.CNode (Suc nat) c \<Rightarrow> cdl_object.CNode \<lparr>cdl_cnode_caps = transform_cnode_contents (Suc nat) c, cdl_cnode_size_bits = Suc nat\<rparr> | TCB tcb \<Rightarrow> case ekheap s ptr of Some etcb \<Rightarrow> transform_tcb (machine_state s) ptr tcb etcb | kernel_object.Endpoint x \<Rightarrow> cdl_object.Endpoint | kernel_object.Notification x \<Rightarrow> cdl_object.Notification | ArchObj (ASIDPool ap) \<Rightarrow> AsidPool \<lparr>cdl_asid_pool_caps = transform_asid_pool_contents ap\<rparr> | ArchObj (arch_kernel_obj.PageTable ptx) \<Rightarrow> cdl_object.PageTable \<lparr>cdl_page_table_caps = transform_page_table_contents ptx\<rparr> | ArchObj (arch_kernel_obj.PageDirectory pd) \<Rightarrow> cdl_object.PageDirectory \<lparr>cdl_page_directory_caps = transform_page_directory_contents pd\<rparr> | ArchObj (DataPage dev sz) \<Rightarrow> Frame \<lparr>cdl_frame_size_bits = pageBitsForSize sz\<rparr>) = cdl_object.PageTable x6\<rbrakk> \<Longrightarrow> \<exists>b. (ptr, offset) = transform_cslot_ptr (ptr, b) \<and> cte_wp_at (\<lambda>cap'. P (transform_cap cap')) (ptr, b) s
 6. \<And>x2 ptr offset x7 z. \<lbrakk>P x2; slot = (ptr, offset); valid_objs s; valid_etcbs s; cdl_page_directory_caps x7 offset = Some x2; kheap s ptr = Some z; ptr \<noteq> idle_thread s; (case z of kernel_object.CNode 0 c \<Rightarrow> IRQNode \<lparr>cdl_irq_node_caps = transform_cnode_contents 0 c\<rparr> | kernel_object.CNode (Suc nat) c \<Rightarrow> cdl_object.CNode \<lparr>cdl_cnode_caps = transform_cnode_contents (Suc nat) c, cdl_cnode_size_bits = Suc nat\<rparr> | TCB tcb \<Rightarrow> case ekheap s ptr of Some etcb \<Rightarrow> transform_tcb (machine_state s) ptr tcb etcb | kernel_object.Endpoint x \<Rightarrow> cdl_object.Endpoint | kernel_object.Notification x \<Rightarrow> cdl_object.Notification | ArchObj (ASIDPool ap) \<Rightarrow> AsidPool \<lparr>cdl_asid_pool_caps = transform_asid_pool_contents ap\<rparr> | ArchObj (arch_kernel_obj.PageTable ptx) \<Rightarrow> cdl_object.PageTable \<lparr>cdl_page_table_caps = transform_page_table_contents ptx\<rparr> | ArchObj (arch_kernel_obj.PageDirectory pd) \<Rightarrow> cdl_object.PageDirectory \<lparr>cdl_page_directory_caps = transform_page_directory_contents pd\<rparr> | ArchObj (DataPage dev sz) \<Rightarrow> Frame \<lparr>cdl_frame_size_bits = pageBitsForSize sz\<rparr>) = cdl_object.PageDirectory x7\<rbrakk> \<Longrightarrow> \<exists>b. (ptr, offset) = transform_cslot_ptr (ptr, b) \<and> cte_wp_at (\<lambda>cap'. P (transform_cap cap')) (ptr, b) s proof (prove)
goal (9 subgoals):
 1. \<And>x2 ptr offset x12. \<lbrakk>P x2; slot = (ptr, offset); valid_objs s; valid_etcbs s; transform_cnode_contents 0 x12 offset = Some x2; kheap s ptr = Some (kernel_object.CNode 0 x12); ptr \<noteq> idle_thread s\<rbrakk> \<Longrightarrow> \<exists>b. (ptr, offset) = transform_cslot_ptr (ptr, b) \<and> cte_wp_at (\<lambda>cap'. P (transform_cap cap')) (ptr, b) s
 2. \<And>x2 ptr offset x10 x2a. \<lbrakk>P x2; slot = (ptr, offset); valid_objs s; valid_etcbs s; cdl_irq_node_caps x10 offset = Some x2; kheap s ptr = Some (TCB x2a); ptr \<noteq> idle_thread s; ekheap s ptr = None; undefined = IRQNode x10\<rbrakk> \<Longrightarrow> \<exists>b. (ptr, offset) = transform_cslot_ptr (ptr, b) \<and> cte_wp_at (\<lambda>cap'. P (transform_cap cap')) (ptr, b) s
 3. \<And>x2 ptr offset x10 x2a x2b. \<lbrakk>P x2; slot = (ptr, offset); valid_objs s; valid_etcbs s; cdl_irq_node_caps x10 offset = Some x2; kheap s ptr = Some (TCB x2a); ptr \<noteq> idle_thread s; ekheap s ptr = Some x2b; transform_tcb (machine_state s) ptr x2a x2b = IRQNode x10\<rbrakk> \<Longrightarrow> \<exists>b. (ptr, offset) = transform_cslot_ptr (ptr, b) \<and> cte_wp_at (\<lambda>cap'. P (transform_cap cap')) (ptr, b) s
 4. \<And>x2 ptr offset x10 x5. \<lbrakk>P x2; slot = (ptr, offset); valid_objs s; valid_etcbs s; cdl_irq_node_caps x10 offset = Some x2; kheap s ptr = Some (ArchObj x5); ptr \<noteq> idle_thread s; (case x5 of ASIDPool ap \<Rightarrow> AsidPool \<lparr>cdl_asid_pool_caps = transform_asid_pool_contents ap\<rparr> | arch_kernel_obj.PageTable ptx \<Rightarrow> cdl_object.PageTable \<lparr>cdl_page_table_caps = transform_page_table_contents ptx\<rparr> | arch_kernel_obj.PageDirectory pd \<Rightarrow> cdl_object.PageDirectory \<lparr>cdl_page_directory_caps = transform_page_directory_contents pd\<rparr> | DataPage dev sz \<Rightarrow> Frame \<lparr>cdl_frame_size_bits = pageBitsForSize sz\<rparr>) = IRQNode x10\<rbrakk> \<Longrightarrow> \<exists>b. (ptr, offset) = transform_cslot_ptr (ptr, b) \<and> cte_wp_at (\<lambda>cap'. P (transform_cap cap')) (ptr, b) s
 5. \<And>x2 ptr offset x4 x2a x2b. \<lbrakk>P x2; slot = (ptr, offset); valid_objs s; valid_etcbs s; cdl_cnode_caps x4 offset = Some x2; kheap s ptr = Some (TCB x2a); ptr \<noteq> idle_thread s; ekheap s ptr = Some x2b; transform_tcb (machine_state s) ptr x2a x2b = cdl_object.CNode x4\<rbrakk> \<Longrightarrow> \<exists>b. (ptr, offset) = transform_cslot_ptr (ptr, b) \<and> cte_wp_at (\<lambda>cap'. P (transform_cap cap')) (ptr, b) s
 6. \<And>x2 ptr offset x4 x5. \<lbrakk>P x2; slot = (ptr, offset); valid_objs s; valid_etcbs s; cdl_cnode_caps x4 offset = Some x2; kheap s ptr = Some (ArchObj x5); ptr \<noteq> idle_thread s; (case x5 of ASIDPool ap \<Rightarrow> AsidPool \<lparr>cdl_asid_pool_caps = transform_asid_pool_contents ap\<rparr> | arch_kernel_obj.PageTable ptx \<Rightarrow> cdl_object.PageTable \<lparr>cdl_page_table_caps = transform_page_table_contents ptx\<rparr> | arch_kernel_obj.PageDirectory pd \<Rightarrow> cdl_object.PageDirectory \<lparr>cdl_page_directory_caps = transform_page_directory_contents pd\<rparr> | DataPage dev sz \<Rightarrow> Frame \<lparr>cdl_frame_size_bits = pageBitsForSize sz\<rparr>) = cdl_object.CNode x4\<rbrakk> \<Longrightarrow> \<exists>b. (ptr, offset) = transform_cslot_ptr (ptr, b) \<and> cte_wp_at (\<lambda>cap'. P (transform_cap cap')) (ptr, b) s
 7. \<And>x2 ptr offset x5 z. \<lbrakk>P x2; slot = (ptr, offset); valid_objs s; valid_etcbs s; cdl_asid_pool_caps x5 offset = Some x2; kheap s ptr = Some z; ptr \<noteq> idle_thread s; (case z of kernel_object.CNode 0 c \<Rightarrow> IRQNode \<lparr>cdl_irq_node_caps = transform_cnode_contents 0 c\<rparr> | kernel_object.CNode (Suc nat) c \<Rightarrow> cdl_object.CNode \<lparr>cdl_cnode_caps = transform_cnode_contents (Suc nat) c, cdl_cnode_size_bits = Suc nat\<rparr> | TCB tcb \<Rightarrow> case ekheap s ptr of Some etcb \<Rightarrow> transform_tcb (machine_state s) ptr tcb etcb | kernel_object.Endpoint x \<Rightarrow> cdl_object.Endpoint | kernel_object.Notification x \<Rightarrow> cdl_object.Notification | ArchObj (ASIDPool ap) \<Rightarrow> AsidPool \<lparr>cdl_asid_pool_caps = transform_asid_pool_contents ap\<rparr> | ArchObj (arch_kernel_obj.PageTable ptx) \<Rightarrow> cdl_object.PageTable \<lparr>cdl_page_table_caps = transform_page_table_contents ptx\<rparr> | ArchObj (arch_kernel_obj.PageDirectory pd) \<Rightarrow> cdl_object.PageDirectory \<lparr>cdl_page_directory_caps = transform_page_directory_contents pd\<rparr> | ArchObj (DataPage dev sz) \<Rightarrow> Frame \<lparr>cdl_frame_size_bits = pageBitsForSize sz\<rparr>) = AsidPool x5\<rbrakk> \<Longrightarrow> \<exists>b. (ptr, offset) = transform_cslot_ptr (ptr, b) \<and> cte_wp_at (\<lambda>cap'. P (transform_cap cap')) (ptr, b) s
 8. \<And>x2 ptr offset x6 z. \<lbrakk>P x2; slot = (ptr, offset); valid_objs s; valid_etcbs s; cdl_page_table_caps x6 offset = Some x2; kheap s ptr = Some z; ptr \<noteq> idle_thread s; (case z of kernel_object.CNode 0 c \<Rightarrow> IRQNode \<lparr>cdl_irq_node_caps = transform_cnode_contents 0 c\<rparr> | kernel_object.CNode (Suc nat) c \<Rightarrow> cdl_object.CNode \<lparr>cdl_cnode_caps = transform_cnode_contents (Suc nat) c, cdl_cnode_size_bits = Suc nat\<rparr> | TCB tcb \<Rightarrow> case ekheap s ptr of Some etcb \<Rightarrow> transform_tcb (machine_state s) ptr tcb etcb | kernel_object.Endpoint x \<Rightarrow> cdl_object.Endpoint | kernel_object.Notification x \<Rightarrow> cdl_object.Notification | ArchObj (ASIDPool ap) \<Rightarrow> AsidPool \<lparr>cdl_asid_pool_caps = transform_asid_pool_contents ap\<rparr> | ArchObj (arch_kernel_obj.PageTable ptx) \<Rightarrow> cdl_object.PageTable \<lparr>cdl_page_table_caps = transform_page_table_contents ptx\<rparr> | ArchObj (arch_kernel_obj.PageDirectory pd) \<Rightarrow> cdl_object.PageDirectory \<lparr>cdl_page_directory_caps = transform_page_directory_contents pd\<rparr> | ArchObj (DataPage dev sz) \<Rightarrow> Frame \<lparr>cdl_frame_size_bits = pageBitsForSize sz\<rparr>) = cdl_object.PageTable x6\<rbrakk> \<Longrightarrow> \<exists>b. (ptr, offset) = transform_cslot_ptr (ptr, b) \<and> cte_wp_at (\<lambda>cap'. P (transform_cap cap')) (ptr, b) s
 9. \<And>x2 ptr offset x7 z. \<lbrakk>P x2; slot = (ptr, offset); valid_objs s; valid_etcbs s; cdl_page_directory_caps x7 offset = Some x2; kheap s ptr = Some z; ptr \<noteq> idle_thread s; (case z of kernel_object.CNode 0 c \<Rightarrow> IRQNode \<lparr>cdl_irq_node_caps = transform_cnode_contents 0 c\<rparr> | kernel_object.CNode (Suc nat) c \<Rightarrow> cdl_object.CNode \<lparr>cdl_cnode_caps = transform_cnode_contents (Suc nat) c, cdl_cnode_size_bits = Suc nat\<rparr> | TCB tcb \<Rightarrow> case ekheap s ptr of Some etcb \<Rightarrow> transform_tcb (machine_state s) ptr tcb etcb | kernel_object.Endpoint x \<Rightarrow> cdl_object.Endpoint | kernel_object.Notification x \<Rightarrow> cdl_object.Notification | ArchObj (ASIDPool ap) \<Rightarrow> AsidPool \<lparr>cdl_asid_pool_caps = transform_asid_pool_contents ap\<rparr> | ArchObj (arch_kernel_obj.PageTable ptx) \<Rightarrow> cdl_object.PageTable \<lparr>cdl_page_table_caps = transform_page_table_contents ptx\<rparr> | ArchObj (arch_kernel_obj.PageDirectory pd) \<Rightarrow> cdl_object.PageDirectory \<lparr>cdl_page_directory_caps = transform_page_directory_contents pd\<rparr> | ArchObj (DataPage dev sz) \<Rightarrow> Frame \<lparr>cdl_frame_size_bits = pageBitsForSize sz\<rparr>) = cdl_object.PageDirectory x7\<rbrakk> \<Longrightarrow> \<exists>b. (ptr, offset) = transform_cslot_ptr (ptr, b) \<and> cte_wp_at (\<lambda>cap'. P (transform_cap cap')) (ptr, b) s proof (prove)
goal (9 subgoals):
 1. \<And>ptr offset x12 x2a z. \<lbrakk>kheap s ptr = Some (kernel_object.CNode 0 x12); ptr \<noteq> idle_thread s; P (transform_cap z); slot = (ptr, offset); valid_objs s; valid_etcbs s; nat_to_bl 0 offset = Some x2a; x12 x2a = Some z\<rbrakk> \<Longrightarrow> \<exists>b. (ptr, offset) = transform_cslot_ptr (ptr, b) \<and> cte_wp_at (\<lambda>cap'. P (transform_cap cap')) (ptr, b) s
 2. \<And>x2 ptr offset x10 x2a. \<lbrakk>P x2; slot = (ptr, offset); valid_objs s; valid_etcbs s; cdl_irq_node_caps x10 offset = Some x2; kheap s ptr = Some (TCB x2a); ptr \<noteq> idle_thread s; ekheap s ptr = None; undefined = IRQNode x10\<rbrakk> \<Longrightarrow> \<exists>b. (ptr, offset) = transform_cslot_ptr (ptr, b) \<and> cte_wp_at (\<lambda>cap'. P (transform_cap cap')) (ptr, b) s
 3. \<And>x2 ptr offset x10 x2a x2b. \<lbrakk>P x2; slot = (ptr, offset); valid_objs s; valid_etcbs s; cdl_irq_node_caps x10 offset = Some x2; kheap s ptr = Some (TCB x2a); ptr \<noteq> idle_thread s; ekheap s ptr = Some x2b; transform_tcb (machine_state s) ptr x2a x2b = IRQNode x10\<rbrakk> \<Longrightarrow> \<exists>b. (ptr, offset) = transform_cslot_ptr (ptr, b) \<and> cte_wp_at (\<lambda>cap'. P (transform_cap cap')) (ptr, b) s
 4. \<And>x2 ptr offset x10 x5. \<lbrakk>P x2; slot = (ptr, offset); valid_objs s; valid_etcbs s; cdl_irq_node_caps x10 offset = Some x2; kheap s ptr = Some (ArchObj x5); ptr \<noteq> idle_thread s; (case x5 of ASIDPool ap \<Rightarrow> AsidPool \<lparr>cdl_asid_pool_caps = transform_asid_pool_contents ap\<rparr> | arch_kernel_obj.PageTable ptx \<Rightarrow> cdl_object.PageTable \<lparr>cdl_page_table_caps = transform_page_table_contents ptx\<rparr> | arch_kernel_obj.PageDirectory pd \<Rightarrow> cdl_object.PageDirectory \<lparr>cdl_page_directory_caps = transform_page_directory_contents pd\<rparr> | DataPage dev sz \<Rightarrow> Frame \<lparr>cdl_frame_size_bits = pageBitsForSize sz\<rparr>) = IRQNode x10\<rbrakk> \<Longrightarrow> \<exists>b. (ptr, offset) = transform_cslot_ptr (ptr, b) \<and> cte_wp_at (\<lambda>cap'. P (transform_cap cap')) (ptr, b) s
 5. \<And>x2 ptr offset x4 x2a x2b. \<lbrakk>P x2; slot = (ptr, offset); valid_objs s; valid_etcbs s; cdl_cnode_caps x4 offset = Some x2; kheap s ptr = Some (TCB x2a); ptr \<noteq> idle_thread s; ekheap s ptr = Some x2b; transform_tcb (machine_state s) ptr x2a x2b = cdl_object.CNode x4\<rbrakk> \<Longrightarrow> \<exists>b. (ptr, offset) = transform_cslot_ptr (ptr, b) \<and> cte_wp_at (\<lambda>cap'. P (transform_cap cap')) (ptr, b) s
 6. \<And>x2 ptr offset x4 x5. \<lbrakk>P x2; slot = (ptr, offset); valid_objs s; valid_etcbs s; cdl_cnode_caps x4 offset = Some x2; kheap s ptr = Some (ArchObj x5); ptr \<noteq> idle_thread s; (case x5 of ASIDPool ap \<Rightarrow> AsidPool \<lparr>cdl_asid_pool_caps = transform_asid_pool_contents ap\<rparr> | arch_kernel_obj.PageTable ptx \<Rightarrow> cdl_object.PageTable \<lparr>cdl_page_table_caps = transform_page_table_contents ptx\<rparr> | arch_kernel_obj.PageDirectory pd \<Rightarrow> cdl_object.PageDirectory \<lparr>cdl_page_directory_caps = transform_page_directory_contents pd\<rparr> | DataPage dev sz \<Rightarrow> Frame \<lparr>cdl_frame_size_bits = pageBitsForSize sz\<rparr>) = cdl_object.CNode x4\<rbrakk> \<Longrightarrow> \<exists>b. (ptr, offset) = transform_cslot_ptr (ptr, b) \<and> cte_wp_at (\<lambda>cap'. P (transform_cap cap')) (ptr, b) s
 7. \<And>x2 ptr offset x5 z. \<lbrakk>P x2; slot = (ptr, offset); valid_objs s; valid_etcbs s; cdl_asid_pool_caps x5 offset = Some x2; kheap s ptr = Some z; ptr \<noteq> idle_thread s; (case z of kernel_object.CNode 0 c \<Rightarrow> IRQNode \<lparr>cdl_irq_node_caps = transform_cnode_contents 0 c\<rparr> | kernel_object.CNode (Suc nat) c \<Rightarrow> cdl_object.CNode \<lparr>cdl_cnode_caps = transform_cnode_contents (Suc nat) c, cdl_cnode_size_bits = Suc nat\<rparr> | TCB tcb \<Rightarrow> case ekheap s ptr of Some etcb \<Rightarrow> transform_tcb (machine_state s) ptr tcb etcb | kernel_object.Endpoint x \<Rightarrow> cdl_object.Endpoint | kernel_object.Notification x \<Rightarrow> cdl_object.Notification | ArchObj (ASIDPool ap) \<Rightarrow> AsidPool \<lparr>cdl_asid_pool_caps = transform_asid_pool_contents ap\<rparr> | ArchObj (arch_kernel_obj.PageTable ptx) \<Rightarrow> cdl_object.PageTable \<lparr>cdl_page_table_caps = transform_page_table_contents ptx\<rparr> | ArchObj (arch_kernel_obj.PageDirectory pd) \<Rightarrow> cdl_object.PageDirectory \<lparr>cdl_page_directory_caps = transform_page_directory_contents pd\<rparr> | ArchObj (DataPage dev sz) \<Rightarrow> Frame \<lparr>cdl_frame_size_bits = pageBitsForSize sz\<rparr>) = AsidPool x5\<rbrakk> \<Longrightarrow> \<exists>b. (ptr, offset) = transform_cslot_ptr (ptr, b) \<and> cte_wp_at (\<lambda>cap'. P (transform_cap cap')) (ptr, b) s
 8. \<And>x2 ptr offset x6 z. \<lbrakk>P x2; slot = (ptr, offset); valid_objs s; valid_etcbs s; cdl_page_table_caps x6 offset = Some x2; kheap s ptr = Some z; ptr \<noteq> idle_thread s; (case z of kernel_object.CNode 0 c \<Rightarrow> IRQNode \<lparr>cdl_irq_node_caps = transform_cnode_contents 0 c\<rparr> | kernel_object.CNode (Suc nat) c \<Rightarrow> cdl_object.CNode \<lparr>cdl_cnode_caps = transform_cnode_contents (Suc nat) c, cdl_cnode_size_bits = Suc nat\<rparr> | TCB tcb \<Rightarrow> case ekheap s ptr of Some etcb \<Rightarrow> transform_tcb (machine_state s) ptr tcb etcb | kernel_object.Endpoint x \<Rightarrow> cdl_object.Endpoint | kernel_object.Notification x \<Rightarrow> cdl_object.Notification | ArchObj (ASIDPool ap) \<Rightarrow> AsidPool \<lparr>cdl_asid_pool_caps = transform_asid_pool_contents ap\<rparr> | ArchObj (arch_kernel_obj.PageTable ptx) \<Rightarrow> cdl_object.PageTable \<lparr>cdl_page_table_caps = transform_page_table_contents ptx\<rparr> | ArchObj (arch_kernel_obj.PageDirectory pd) \<Rightarrow> cdl_object.PageDirectory \<lparr>cdl_page_directory_caps = transform_page_directory_contents pd\<rparr> | ArchObj (DataPage dev sz) \<Rightarrow> Frame \<lparr>cdl_frame_size_bits = pageBitsForSize sz\<rparr>) = cdl_object.PageTable x6\<rbrakk> \<Longrightarrow> \<exists>b. (ptr, offset) = transform_cslot_ptr (ptr, b) \<and> cte_wp_at (\<lambda>cap'. P (transform_cap cap')) (ptr, b) s
 9. \<And>x2 ptr offset x7 z. \<lbrakk>P x2; slot = (ptr, offset); valid_objs s; valid_etcbs s; cdl_page_directory_caps x7 offset = Some x2; kheap s ptr = Some z; ptr \<noteq> idle_thread s; (case z of kernel_object.CNode 0 c \<Rightarrow> IRQNode \<lparr>cdl_irq_node_caps = transform_cnode_contents 0 c\<rparr> | kernel_object.CNode (Suc nat) c \<Rightarrow> cdl_object.CNode \<lparr>cdl_cnode_caps = transform_cnode_contents (Suc nat) c, cdl_cnode_size_bits = Suc nat\<rparr> | TCB tcb \<Rightarrow> case ekheap s ptr of Some etcb \<Rightarrow> transform_tcb (machine_state s) ptr tcb etcb | kernel_object.Endpoint x \<Rightarrow> cdl_object.Endpoint | kernel_object.Notification x \<Rightarrow> cdl_object.Notification | ArchObj (ASIDPool ap) \<Rightarrow> AsidPool \<lparr>cdl_asid_pool_caps = transform_asid_pool_contents ap\<rparr> | ArchObj (arch_kernel_obj.PageTable ptx) \<Rightarrow> cdl_object.PageTable \<lparr>cdl_page_table_caps = transform_page_table_contents ptx\<rparr> | ArchObj (arch_kernel_obj.PageDirectory pd) \<Rightarrow> cdl_object.PageDirectory \<lparr>cdl_page_directory_caps = transform_page_directory_contents pd\<rparr> | ArchObj (DataPage dev sz) \<Rightarrow> Frame \<lparr>cdl_frame_size_bits = pageBitsForSize sz\<rparr>) = cdl_object.PageDirectory x7\<rbrakk> \<Longrightarrow> \<exists>b. (ptr, offset) = transform_cslot_ptr (ptr, b) \<and> cte_wp_at (\<lambda>cap'. P (transform_cap cap')) (ptr, b) s proof (prove)
goal (9 subgoals):
 1. \<And>ptr offset x12 x2a z. \<lbrakk>kheap s ptr = Some (kernel_object.CNode 0 x12); ptr \<noteq> idle_thread s; P (transform_cap z); slot = (ptr, offset); valid_objs s; valid_etcbs s; nat_to_bl 0 offset = Some x2a; x12 x2a = Some z\<rbrakk> \<Longrightarrow> \<exists>b. offset = nat (bl_to_bin b) \<and> (\<exists>cap. x12 b = Some cap \<and> P (transform_cap cap))
 2. \<And>x2 ptr offset x10 x2a. \<lbrakk>P x2; slot = (ptr, offset); valid_objs s; valid_etcbs s; cdl_irq_node_caps x10 offset = Some x2; kheap s ptr = Some (TCB x2a); ptr \<noteq> idle_thread s; ekheap s ptr = None; undefined = IRQNode x10\<rbrakk> \<Longrightarrow> \<exists>b. (ptr, offset) = transform_cslot_ptr (ptr, b) \<and> cte_wp_at (\<lambda>cap'. P (transform_cap cap')) (ptr, b) s
 3. \<And>x2 ptr offset x10 x2a x2b. \<lbrakk>P x2; slot = (ptr, offset); valid_objs s; valid_etcbs s; cdl_irq_node_caps x10 offset = Some x2; kheap s ptr = Some (TCB x2a); ptr \<noteq> idle_thread s; ekheap s ptr = Some x2b; transform_tcb (machine_state s) ptr x2a x2b = IRQNode x10\<rbrakk> \<Longrightarrow> \<exists>b. (ptr, offset) = transform_cslot_ptr (ptr, b) \<and> cte_wp_at (\<lambda>cap'. P (transform_cap cap')) (ptr, b) s
 4. \<And>x2 ptr offset x10 x5. \<lbrakk>P x2; slot = (ptr, offset); valid_objs s; valid_etcbs s; cdl_irq_node_caps x10 offset = Some x2; kheap s ptr = Some (ArchObj x5); ptr \<noteq> idle_thread s; (case x5 of ASIDPool ap \<Rightarrow> AsidPool \<lparr>cdl_asid_pool_caps = transform_asid_pool_contents ap\<rparr> | arch_kernel_obj.PageTable ptx \<Rightarrow> cdl_object.PageTable \<lparr>cdl_page_table_caps = transform_page_table_contents ptx\<rparr> | arch_kernel_obj.PageDirectory pd \<Rightarrow> cdl_object.PageDirectory \<lparr>cdl_page_directory_caps = transform_page_directory_contents pd\<rparr> | DataPage dev sz \<Rightarrow> Frame \<lparr>cdl_frame_size_bits = pageBitsForSize sz\<rparr>) = IRQNode x10\<rbrakk> \<Longrightarrow> \<exists>b. (ptr, offset) = transform_cslot_ptr (ptr, b) \<and> cte_wp_at (\<lambda>cap'. P (transform_cap cap')) (ptr, b) s
 5. \<And>x2 ptr offset x4 x2a x2b. \<lbrakk>P x2; slot = (ptr, offset); valid_objs s; valid_etcbs s; cdl_cnode_caps x4 offset = Some x2; kheap s ptr = Some (TCB x2a); ptr \<noteq> idle_thread s; ekheap s ptr = Some x2b; transform_tcb (machine_state s) ptr x2a x2b = cdl_object.CNode x4\<rbrakk> \<Longrightarrow> \<exists>b. (ptr, offset) = transform_cslot_ptr (ptr, b) \<and> cte_wp_at (\<lambda>cap'. P (transform_cap cap')) (ptr, b) s
 6. \<And>x2 ptr offset x4 x5. \<lbrakk>P x2; slot = (ptr, offset); valid_objs s; valid_etcbs s; cdl_cnode_caps x4 offset = Some x2; kheap s ptr = Some (ArchObj x5); ptr \<noteq> idle_thread s; (case x5 of ASIDPool ap \<Rightarrow> AsidPool \<lparr>cdl_asid_pool_caps = transform_asid_pool_contents ap\<rparr> | arch_kernel_obj.PageTable ptx \<Rightarrow> cdl_object.PageTable \<lparr>cdl_page_table_caps = transform_page_table_contents ptx\<rparr> | arch_kernel_obj.PageDirectory pd \<Rightarrow> cdl_object.PageDirectory \<lparr>cdl_page_directory_caps = transform_page_directory_contents pd\<rparr> | DataPage dev sz \<Rightarrow> Frame \<lparr>cdl_frame_size_bits = pageBitsForSize sz\<rparr>) = cdl_object.CNode x4\<rbrakk> \<Longrightarrow> \<exists>b. (ptr, offset) = transform_cslot_ptr (ptr, b) \<and> cte_wp_at (\<lambda>cap'. P (transform_cap cap')) (ptr, b) s
 7. \<And>x2 ptr offset x5 z. \<lbrakk>P x2; slot = (ptr, offset); valid_objs s; valid_etcbs s; cdl_asid_pool_caps x5 offset = Some x2; kheap s ptr = Some z; ptr \<noteq> idle_thread s; (case z of kernel_object.CNode 0 c \<Rightarrow> IRQNode \<lparr>cdl_irq_node_caps = transform_cnode_contents 0 c\<rparr> | kernel_object.CNode (Suc nat) c \<Rightarrow> cdl_object.CNode \<lparr>cdl_cnode_caps = transform_cnode_contents (Suc nat) c, cdl_cnode_size_bits = Suc nat\<rparr> | TCB tcb \<Rightarrow> case ekheap s ptr of Some etcb \<Rightarrow> transform_tcb (machine_state s) ptr tcb etcb | kernel_object.Endpoint x \<Rightarrow> cdl_object.Endpoint | kernel_object.Notification x \<Rightarrow> cdl_object.Notification | ArchObj (ASIDPool ap) \<Rightarrow> AsidPool \<lparr>cdl_asid_pool_caps = transform_asid_pool_contents ap\<rparr> | ArchObj (arch_kernel_obj.PageTable ptx) \<Rightarrow> cdl_object.PageTable \<lparr>cdl_page_table_caps = transform_page_table_contents ptx\<rparr> | ArchObj (arch_kernel_obj.PageDirectory pd) \<Rightarrow> cdl_object.PageDirectory \<lparr>cdl_page_directory_caps = transform_page_directory_contents pd\<rparr> | ArchObj (DataPage dev sz) \<Rightarrow> Frame \<lparr>cdl_frame_size_bits = pageBitsForSize sz\<rparr>) = AsidPool x5\<rbrakk> \<Longrightarrow> \<exists>b. (ptr, offset) = transform_cslot_ptr (ptr, b) \<and> cte_wp_at (\<lambda>cap'. P (transform_cap cap')) (ptr, b) s
 8. \<And>x2 ptr offset x6 z. \<lbrakk>P x2; slot = (ptr, offset); valid_objs s; valid_etcbs s; cdl_page_table_caps x6 offset = Some x2; kheap s ptr = Some z; ptr \<noteq> idle_thread s; (case z of kernel_object.CNode 0 c \<Rightarrow> IRQNode \<lparr>cdl_irq_node_caps = transform_cnode_contents 0 c\<rparr> | kernel_object.CNode (Suc nat) c \<Rightarrow> cdl_object.CNode \<lparr>cdl_cnode_caps = transform_cnode_contents (Suc nat) c, cdl_cnode_size_bits = Suc nat\<rparr> | TCB tcb \<Rightarrow> case ekheap s ptr of Some etcb \<Rightarrow> transform_tcb (machine_state s) ptr tcb etcb | kernel_object.Endpoint x \<Rightarrow> cdl_object.Endpoint | kernel_object.Notification x \<Rightarrow> cdl_object.Notification | ArchObj (ASIDPool ap) \<Rightarrow> AsidPool \<lparr>cdl_asid_pool_caps = transform_asid_pool_contents ap\<rparr> | ArchObj (arch_kernel_obj.PageTable ptx) \<Rightarrow> cdl_object.PageTable \<lparr>cdl_page_table_caps = transform_page_table_contents ptx\<rparr> | ArchObj (arch_kernel_obj.PageDirectory pd) \<Rightarrow> cdl_object.PageDirectory \<lparr>cdl_page_directory_caps = transform_page_directory_contents pd\<rparr> | ArchObj (DataPage dev sz) \<Rightarrow> Frame \<lparr>cdl_frame_size_bits = pageBitsForSize sz\<rparr>) = cdl_object.PageTable x6\<rbrakk> \<Longrightarrow> \<exists>b. (ptr, offset) = transform_cslot_ptr (ptr, b) \<and> cte_wp_at (\<lambda>cap'. P (transform_cap cap')) (ptr, b) s
 9. \<And>x2 ptr offset x7 z. \<lbrakk>P x2; slot = (ptr, offset); valid_objs s; valid_etcbs s; cdl_page_directory_caps x7 offset = Some x2; kheap s ptr = Some z; ptr \<noteq> idle_thread s; (case z of kernel_object.CNode 0 c \<Rightarrow> IRQNode \<lparr>cdl_irq_node_caps = transform_cnode_contents 0 c\<rparr> | kernel_object.CNode (Suc nat) c \<Rightarrow> cdl_object.CNode \<lparr>cdl_cnode_caps = transform_cnode_contents (Suc nat) c, cdl_cnode_size_bits = Suc nat\<rparr> | TCB tcb \<Rightarrow> case ekheap s ptr of Some etcb \<Rightarrow> transform_tcb (machine_state s) ptr tcb etcb | kernel_object.Endpoint x \<Rightarrow> cdl_object.Endpoint | kernel_object.Notification x \<Rightarrow> cdl_object.Notification | ArchObj (ASIDPool ap) \<Rightarrow> AsidPool \<lparr>cdl_asid_pool_caps = transform_asid_pool_contents ap\<rparr> | ArchObj (arch_kernel_obj.PageTable ptx) \<Rightarrow> cdl_object.PageTable \<lparr>cdl_page_table_caps = transform_page_table_contents ptx\<rparr> | ArchObj (arch_kernel_obj.PageDirectory pd) \<Rightarrow> cdl_object.PageDirectory \<lparr>cdl_page_directory_caps = transform_page_directory_contents pd\<rparr> | ArchObj (DataPage dev sz) \<Rightarrow> Frame \<lparr>cdl_frame_size_bits = pageBitsForSize sz\<rparr>) = cdl_object.PageDirectory x7\<rbrakk> \<Longrightarrow> \<exists>b. (ptr, offset) = transform_cslot_ptr (ptr, b) \<and> cte_wp_at (\<lambda>cap'. P (transform_cap cap')) (ptr, b) s proof (prove)
goal (8 subgoals):
 1. \<And>x2 ptr offset x10 x2a. \<lbrakk>P x2; slot = (ptr, offset); valid_objs s; valid_etcbs s; cdl_irq_node_caps x10 offset = Some x2; kheap s ptr = Some (TCB x2a); ptr \<noteq> idle_thread s; ekheap s ptr = None; undefined = IRQNode x10\<rbrakk> \<Longrightarrow> \<exists>b. (ptr, offset) = transform_cslot_ptr (ptr, b) \<and> cte_wp_at (\<lambda>cap'. P (transform_cap cap')) (ptr, b) s
 2. \<And>x2 ptr offset x10 x2a x2b. \<lbrakk>P x2; slot = (ptr, offset); valid_objs s; valid_etcbs s; cdl_irq_node_caps x10 offset = Some x2; kheap s ptr = Some (TCB x2a); ptr \<noteq> idle_thread s; ekheap s ptr = Some x2b; transform_tcb (machine_state s) ptr x2a x2b = IRQNode x10\<rbrakk> \<Longrightarrow> \<exists>b. (ptr, offset) = transform_cslot_ptr (ptr, b) \<and> cte_wp_at (\<lambda>cap'. P (transform_cap cap')) (ptr, b) s
 3. \<And>x2 ptr offset x10 x5. \<lbrakk>P x2; slot = (ptr, offset); valid_objs s; valid_etcbs s; cdl_irq_node_caps x10 offset = Some x2; kheap s ptr = Some (ArchObj x5); ptr \<noteq> idle_thread s; (case x5 of ASIDPool ap \<Rightarrow> AsidPool \<lparr>cdl_asid_pool_caps = transform_asid_pool_contents ap\<rparr> | arch_kernel_obj.PageTable ptx \<Rightarrow> cdl_object.PageTable \<lparr>cdl_page_table_caps = transform_page_table_contents ptx\<rparr> | arch_kernel_obj.PageDirectory pd \<Rightarrow> cdl_object.PageDirectory \<lparr>cdl_page_directory_caps = transform_page_directory_contents pd\<rparr> | DataPage dev sz \<Rightarrow> Frame \<lparr>cdl_frame_size_bits = pageBitsForSize sz\<rparr>) = IRQNode x10\<rbrakk> \<Longrightarrow> \<exists>b. (ptr, offset) = transform_cslot_ptr (ptr, b) \<and> cte_wp_at (\<lambda>cap'. P (transform_cap cap')) (ptr, b) s
 4. \<And>x2 ptr offset x4 x2a x2b. \<lbrakk>P x2; slot = (ptr, offset); valid_objs s; valid_etcbs s; cdl_cnode_caps x4 offset = Some x2; kheap s ptr = Some (TCB x2a); ptr \<noteq> idle_thread s; ekheap s ptr = Some x2b; transform_tcb (machine_state s) ptr x2a x2b = cdl_object.CNode x4\<rbrakk> \<Longrightarrow> \<exists>b. (ptr, offset) = transform_cslot_ptr (ptr, b) \<and> cte_wp_at (\<lambda>cap'. P (transform_cap cap')) (ptr, b) s
 5. \<And>x2 ptr offset x4 x5. \<lbrakk>P x2; slot = (ptr, offset); valid_objs s; valid_etcbs s; cdl_cnode_caps x4 offset = Some x2; kheap s ptr = Some (ArchObj x5); ptr \<noteq> idle_thread s; (case x5 of ASIDPool ap \<Rightarrow> AsidPool \<lparr>cdl_asid_pool_caps = transform_asid_pool_contents ap\<rparr> | arch_kernel_obj.PageTable ptx \<Rightarrow> cdl_object.PageTable \<lparr>cdl_page_table_caps = transform_page_table_contents ptx\<rparr> | arch_kernel_obj.PageDirectory pd \<Rightarrow> cdl_object.PageDirectory \<lparr>cdl_page_directory_caps = transform_page_directory_contents pd\<rparr> | DataPage dev sz \<Rightarrow> Frame \<lparr>cdl_frame_size_bits = pageBitsForSize sz\<rparr>) = cdl_object.CNode x4\<rbrakk> \<Longrightarrow> \<exists>b. (ptr, offset) = transform_cslot_ptr (ptr, b) \<and> cte_wp_at (\<lambda>cap'. P (transform_cap cap')) (ptr, b) s
 6. \<And>x2 ptr offset x5 z. \<lbrakk>P x2; slot = (ptr, offset); valid_objs s; valid_etcbs s; cdl_asid_pool_caps x5 offset = Some x2; kheap s ptr = Some z; ptr \<noteq> idle_thread s; (case z of kernel_object.CNode 0 c \<Rightarrow> IRQNode \<lparr>cdl_irq_node_caps = transform_cnode_contents 0 c\<rparr> | kernel_object.CNode (Suc nat) c \<Rightarrow> cdl_object.CNode \<lparr>cdl_cnode_caps = transform_cnode_contents (Suc nat) c, cdl_cnode_size_bits = Suc nat\<rparr> | TCB tcb \<Rightarrow> case ekheap s ptr of Some etcb \<Rightarrow> transform_tcb (machine_state s) ptr tcb etcb | kernel_object.Endpoint x \<Rightarrow> cdl_object.Endpoint | kernel_object.Notification x \<Rightarrow> cdl_object.Notification | ArchObj (ASIDPool ap) \<Rightarrow> AsidPool \<lparr>cdl_asid_pool_caps = transform_asid_pool_contents ap\<rparr> | ArchObj (arch_kernel_obj.PageTable ptx) \<Rightarrow> cdl_object.PageTable \<lparr>cdl_page_table_caps = transform_page_table_contents ptx\<rparr> | ArchObj (arch_kernel_obj.PageDirectory pd) \<Rightarrow> cdl_object.PageDirectory \<lparr>cdl_page_directory_caps = transform_page_directory_contents pd\<rparr> | ArchObj (DataPage dev sz) \<Rightarrow> Frame \<lparr>cdl_frame_size_bits = pageBitsForSize sz\<rparr>) = AsidPool x5\<rbrakk> \<Longrightarrow> \<exists>b. (ptr, offset) = transform_cslot_ptr (ptr, b) \<and> cte_wp_at (\<lambda>cap'. P (transform_cap cap')) (ptr, b) s
 7. \<And>x2 ptr offset x6 z. \<lbrakk>P x2; slot = (ptr, offset); valid_objs s; valid_etcbs s; cdl_page_table_caps x6 offset = Some x2; kheap s ptr = Some z; ptr \<noteq> idle_thread s; (case z of kernel_object.CNode 0 c \<Rightarrow> IRQNode \<lparr>cdl_irq_node_caps = transform_cnode_contents 0 c\<rparr> | kernel_object.CNode (Suc nat) c \<Rightarrow> cdl_object.CNode \<lparr>cdl_cnode_caps = transform_cnode_contents (Suc nat) c, cdl_cnode_size_bits = Suc nat\<rparr> | TCB tcb \<Rightarrow> case ekheap s ptr of Some etcb \<Rightarrow> transform_tcb (machine_state s) ptr tcb etcb | kernel_object.Endpoint x \<Rightarrow> cdl_object.Endpoint | kernel_object.Notification x \<Rightarrow> cdl_object.Notification | ArchObj (ASIDPool ap) \<Rightarrow> AsidPool \<lparr>cdl_asid_pool_caps = transform_asid_pool_contents ap\<rparr> | ArchObj (arch_kernel_obj.PageTable ptx) \<Rightarrow> cdl_object.PageTable \<lparr>cdl_page_table_caps = transform_page_table_contents ptx\<rparr> | ArchObj (arch_kernel_obj.PageDirectory pd) \<Rightarrow> cdl_object.PageDirectory \<lparr>cdl_page_directory_caps = transform_page_directory_contents pd\<rparr> | ArchObj (DataPage dev sz) \<Rightarrow> Frame \<lparr>cdl_frame_size_bits = pageBitsForSize sz\<rparr>) = cdl_object.PageTable x6\<rbrakk> \<Longrightarrow> \<exists>b. (ptr, offset) = transform_cslot_ptr (ptr, b) \<and> cte_wp_at (\<lambda>cap'. P (transform_cap cap')) (ptr, b) s
 8. \<And>x2 ptr offset x7 z. \<lbrakk>P x2; slot = (ptr, offset); valid_objs s; valid_etcbs s; cdl_page_directory_caps x7 offset = Some x2; kheap s ptr = Some z; ptr \<noteq> idle_thread s; (case z of kernel_object.CNode 0 c \<Rightarrow> IRQNode \<lparr>cdl_irq_node_caps = transform_cnode_contents 0 c\<rparr> | kernel_object.CNode (Suc nat) c \<Rightarrow> cdl_object.CNode \<lparr>cdl_cnode_caps = transform_cnode_contents (Suc nat) c, cdl_cnode_size_bits = Suc nat\<rparr> | TCB tcb \<Rightarrow> case ekheap s ptr of Some etcb \<Rightarrow> transform_tcb (machine_state s) ptr tcb etcb | kernel_object.Endpoint x \<Rightarrow> cdl_object.Endpoint | kernel_object.Notification x \<Rightarrow> cdl_object.Notification | ArchObj (ASIDPool ap) \<Rightarrow> AsidPool \<lparr>cdl_asid_pool_caps = transform_asid_pool_contents ap\<rparr> | ArchObj (arch_kernel_obj.PageTable ptx) \<Rightarrow> cdl_object.PageTable \<lparr>cdl_page_table_caps = transform_page_table_contents ptx\<rparr> | ArchObj (arch_kernel_obj.PageDirectory pd) \<Rightarrow> cdl_object.PageDirectory \<lparr>cdl_page_directory_caps = transform_page_directory_contents pd\<rparr> | ArchObj (DataPage dev sz) \<Rightarrow> Frame \<lparr>cdl_frame_size_bits = pageBitsForSize sz\<rparr>) = cdl_object.PageDirectory x7\<rbrakk> \<Longrightarrow> \<exists>b. (ptr, offset) = transform_cslot_ptr (ptr, b) \<and> cte_wp_at (\<lambda>cap'. P (transform_cap cap')) (ptr, b) s proof (prove)
goal (8 subgoals):
 1. \<And>x2 ptr offset x10 x2a. \<lbrakk>P x2; slot = (ptr, offset); valid_objs s; valid_etcbs s; cdl_irq_node_caps x10 offset = Some x2; kheap s ptr = Some (TCB x2a); ptr \<noteq> idle_thread s; ekheap s ptr = None; undefined = IRQNode x10; cap_counts x2\<rbrakk> \<Longrightarrow> \<exists>b. (ptr, offset) = transform_cslot_ptr (ptr, b) \<and> cte_wp_at (\<lambda>cap'. P (transform_cap cap')) (ptr, b) s
 2. \<And>x2 ptr offset x10 x2a x2b. \<lbrakk>P x2; slot = (ptr, offset); valid_objs s; valid_etcbs s; cdl_irq_node_caps x10 offset = Some x2; kheap s ptr = Some (TCB x2a); ptr \<noteq> idle_thread s; ekheap s ptr = Some x2b; transform_tcb (machine_state s) ptr x2a x2b = IRQNode x10\<rbrakk> \<Longrightarrow> \<exists>b. (ptr, offset) = transform_cslot_ptr (ptr, b) \<and> cte_wp_at (\<lambda>cap'. P (transform_cap cap')) (ptr, b) s
 3. \<And>x2 ptr offset x10 x5. \<lbrakk>P x2; slot = (ptr, offset); valid_objs s; valid_etcbs s; cdl_irq_node_caps x10 offset = Some x2; kheap s ptr = Some (ArchObj x5); ptr \<noteq> idle_thread s; (case x5 of ASIDPool ap \<Rightarrow> AsidPool \<lparr>cdl_asid_pool_caps = transform_asid_pool_contents ap\<rparr> | arch_kernel_obj.PageTable ptx \<Rightarrow> cdl_object.PageTable \<lparr>cdl_page_table_caps = transform_page_table_contents ptx\<rparr> | arch_kernel_obj.PageDirectory pd \<Rightarrow> cdl_object.PageDirectory \<lparr>cdl_page_directory_caps = transform_page_directory_contents pd\<rparr> | DataPage dev sz \<Rightarrow> Frame \<lparr>cdl_frame_size_bits = pageBitsForSize sz\<rparr>) = IRQNode x10\<rbrakk> \<Longrightarrow> \<exists>b. (ptr, offset) = transform_cslot_ptr (ptr, b) \<and> cte_wp_at (\<lambda>cap'. P (transform_cap cap')) (ptr, b) s
 4. \<And>x2 ptr offset x4 x2a x2b. \<lbrakk>P x2; slot = (ptr, offset); valid_objs s; valid_etcbs s; cdl_cnode_caps x4 offset = Some x2; kheap s ptr = Some (TCB x2a); ptr \<noteq> idle_thread s; ekheap s ptr = Some x2b; transform_tcb (machine_state s) ptr x2a x2b = cdl_object.CNode x4\<rbrakk> \<Longrightarrow> \<exists>b. (ptr, offset) = transform_cslot_ptr (ptr, b) \<and> cte_wp_at (\<lambda>cap'. P (transform_cap cap')) (ptr, b) s
 5. \<And>x2 ptr offset x4 x5. \<lbrakk>P x2; slot = (ptr, offset); valid_objs s; valid_etcbs s; cdl_cnode_caps x4 offset = Some x2; kheap s ptr = Some (ArchObj x5); ptr \<noteq> idle_thread s; (case x5 of ASIDPool ap \<Rightarrow> AsidPool \<lparr>cdl_asid_pool_caps = transform_asid_pool_contents ap\<rparr> | arch_kernel_obj.PageTable ptx \<Rightarrow> cdl_object.PageTable \<lparr>cdl_page_table_caps = transform_page_table_contents ptx\<rparr> | arch_kernel_obj.PageDirectory pd \<Rightarrow> cdl_object.PageDirectory \<lparr>cdl_page_directory_caps = transform_page_directory_contents pd\<rparr> | DataPage dev sz \<Rightarrow> Frame \<lparr>cdl_frame_size_bits = pageBitsForSize sz\<rparr>) = cdl_object.CNode x4\<rbrakk> \<Longrightarrow> \<exists>b. (ptr, offset) = transform_cslot_ptr (ptr, b) \<and> cte_wp_at (\<lambda>cap'. P (transform_cap cap')) (ptr, b) s
 6. \<And>x2 ptr offset x5 z. \<lbrakk>P x2; slot = (ptr, offset); valid_objs s; valid_etcbs s; cdl_asid_pool_caps x5 offset = Some x2; kheap s ptr = Some z; ptr \<noteq> idle_thread s; (case z of kernel_object.CNode 0 c \<Rightarrow> IRQNode \<lparr>cdl_irq_node_caps = transform_cnode_contents 0 c\<rparr> | kernel_object.CNode (Suc nat) c \<Rightarrow> cdl_object.CNode \<lparr>cdl_cnode_caps = transform_cnode_contents (Suc nat) c, cdl_cnode_size_bits = Suc nat\<rparr> | TCB tcb \<Rightarrow> case ekheap s ptr of Some etcb \<Rightarrow> transform_tcb (machine_state s) ptr tcb etcb | kernel_object.Endpoint x \<Rightarrow> cdl_object.Endpoint | kernel_object.Notification x \<Rightarrow> cdl_object.Notification | ArchObj (ASIDPool ap) \<Rightarrow> AsidPool \<lparr>cdl_asid_pool_caps = transform_asid_pool_contents ap\<rparr> | ArchObj (arch_kernel_obj.PageTable ptx) \<Rightarrow> cdl_object.PageTable \<lparr>cdl_page_table_caps = transform_page_table_contents ptx\<rparr> | ArchObj (arch_kernel_obj.PageDirectory pd) \<Rightarrow> cdl_object.PageDirectory \<lparr>cdl_page_directory_caps = transform_page_directory_contents pd\<rparr> | ArchObj (DataPage dev sz) \<Rightarrow> Frame \<lparr>cdl_frame_size_bits = pageBitsForSize sz\<rparr>) = AsidPool x5\<rbrakk> \<Longrightarrow> \<exists>b. (ptr, offset) = transform_cslot_ptr (ptr, b) \<and> cte_wp_at (\<lambda>cap'. P (transform_cap cap')) (ptr, b) s
 7. \<And>x2 ptr offset x6 z. \<lbrakk>P x2; slot = (ptr, offset); valid_objs s; valid_etcbs s; cdl_page_table_caps x6 offset = Some x2; kheap s ptr = Some z; ptr \<noteq> idle_thread s; (case z of kernel_object.CNode 0 c \<Rightarrow> IRQNode \<lparr>cdl_irq_node_caps = transform_cnode_contents 0 c\<rparr> | kernel_object.CNode (Suc nat) c \<Rightarrow> cdl_object.CNode \<lparr>cdl_cnode_caps = transform_cnode_contents (Suc nat) c, cdl_cnode_size_bits = Suc nat\<rparr> | TCB tcb \<Rightarrow> case ekheap s ptr of Some etcb \<Rightarrow> transform_tcb (machine_state s) ptr tcb etcb | kernel_object.Endpoint x \<Rightarrow> cdl_object.Endpoint | kernel_object.Notification x \<Rightarrow> cdl_object.Notification | ArchObj (ASIDPool ap) \<Rightarrow> AsidPool \<lparr>cdl_asid_pool_caps = transform_asid_pool_contents ap\<rparr> | ArchObj (arch_kernel_obj.PageTable ptx) \<Rightarrow> cdl_object.PageTable \<lparr>cdl_page_table_caps = transform_page_table_contents ptx\<rparr> | ArchObj (arch_kernel_obj.PageDirectory pd) \<Rightarrow> cdl_object.PageDirectory \<lparr>cdl_page_directory_caps = transform_page_directory_contents pd\<rparr> | ArchObj (DataPage dev sz) \<Rightarrow> Frame \<lparr>cdl_frame_size_bits = pageBitsForSize sz\<rparr>) = cdl_object.PageTable x6\<rbrakk> \<Longrightarrow> \<exists>b. (ptr, offset) = transform_cslot_ptr (ptr, b) \<and> cte_wp_at (\<lambda>cap'. P (transform_cap cap')) (ptr, b) s
 8. \<And>x2 ptr offset x7 z. \<lbrakk>P x2; slot = (ptr, offset); valid_objs s; valid_etcbs s; cdl_page_directory_caps x7 offset = Some x2; kheap s ptr = Some z; ptr \<noteq> idle_thread s; (case z of kernel_object.CNode 0 c \<Rightarrow> IRQNode \<lparr>cdl_irq_node_caps = transform_cnode_contents 0 c\<rparr> | kernel_object.CNode (Suc nat) c \<Rightarrow> cdl_object.CNode \<lparr>cdl_cnode_caps = transform_cnode_contents (Suc nat) c, cdl_cnode_size_bits = Suc nat\<rparr> | TCB tcb \<Rightarrow> case ekheap s ptr of Some etcb \<Rightarrow> transform_tcb (machine_state s) ptr tcb etcb | kernel_object.Endpoint x \<Rightarrow> cdl_object.Endpoint | kernel_object.Notification x \<Rightarrow> cdl_object.Notification | ArchObj (ASIDPool ap) \<Rightarrow> AsidPool \<lparr>cdl_asid_pool_caps = transform_asid_pool_contents ap\<rparr> | ArchObj (arch_kernel_obj.PageTable ptx) \<Rightarrow> cdl_object.PageTable \<lparr>cdl_page_table_caps = transform_page_table_contents ptx\<rparr> | ArchObj (arch_kernel_obj.PageDirectory pd) \<Rightarrow> cdl_object.PageDirectory \<lparr>cdl_page_directory_caps = transform_page_directory_contents pd\<rparr> | ArchObj (DataPage dev sz) \<Rightarrow> Frame \<lparr>cdl_frame_size_bits = pageBitsForSize sz\<rparr>) = cdl_object.PageDirectory x7\<rbrakk> \<Longrightarrow> \<exists>b. (ptr, offset) = transform_cslot_ptr (ptr, b) \<and> cte_wp_at (\<lambda>cap'. P (transform_cap cap')) (ptr, b) s proof (prove)
goal:
No subgoals!