theory CNode_DR

lemma descendants_not_idle:
  "\<lbrakk> invs sfix; (a, b) \<in> CSpaceAcc_A.descendants_of slot' (cdt sfix)\<rbrakk>
         \<Longrightarrow> not_idle_thread a sfix" apply (clarsimp simp:not_idle_thread_def invs_def valid_state_def valid_mdb_def valid_pspace_def) apply (frule descendants_not_null_cap) apply simp apply (frule obj_ref_not_idle) apply simp+ apply (erule cte_wp_at_weakenE) apply simp apply (clarsimp simp:cte_wp_at_caps_of_state) apply (frule valid_idle_has_null_cap) apply simp+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>invs sfix; (a, b) \<in> CSpaceAcc_A.descendants_of slot' (cdt sfix)\<rbrakk> \<Longrightarrow> not_idle_thread a sfix proof (prove)
goal (1 subgoal):
 1. \<lbrakk>(idle_thread sfix, b) \<in> CSpaceAcc_A.descendants_of slot' (cdt sfix); valid_objs sfix; pspace_aligned sfix; pspace_distinct sfix; if_live_then_nonz_cap sfix; zombies_final sfix; sym_refs (state_refs_of sfix); sym_refs (state_hyp_refs_of sfix); mdb_cte_at (swp (cte_wp_at ((\<noteq>) cap.NullCap)) sfix) (cdt sfix); untyped_mdb (cdt sfix) (caps_of_state sfix); descendants_inc (cdt sfix) (caps_of_state sfix); no_mloop (cdt sfix); untyped_inc (cdt sfix) (caps_of_state sfix); ut_revocable (is_original_cap sfix) (caps_of_state sfix); irq_revocable (is_original_cap sfix) (caps_of_state sfix); reply_master_revocable (is_original_cap sfix) (caps_of_state sfix); reply_mdb (cdt sfix) (caps_of_state sfix); valid_ioc sfix; valid_idle sfix; only_idle sfix; if_unsafe_then_cap sfix; valid_reply_caps sfix; valid_reply_masters sfix; valid_global_refs sfix; valid_arch_state sfix; valid_irq_node sfix; valid_irq_handlers sfix; valid_irq_states sfix; valid_machine_state sfix; valid_vspace_objs sfix; valid_arch_caps sfix; valid_global_objs sfix; valid_kernel_mappings sfix; equal_kernel_mappings sfix; valid_asid_map sfix; valid_global_vspace_mappings sfix; pspace_in_kernel_window sfix; cap_refs_in_kernel_window sfix; pspace_respects_device_region sfix; cap_refs_respects_device_region sfix; cur_tcb sfix; a = idle_thread sfix\<rbrakk> \<Longrightarrow> False proof (prove)
goal (2 subgoals):
 1. \<lbrakk>(idle_thread sfix, b) \<in> CSpaceAcc_A.descendants_of slot' (cdt sfix); valid_objs sfix; pspace_aligned sfix; pspace_distinct sfix; if_live_then_nonz_cap sfix; zombies_final sfix; sym_refs (state_refs_of sfix); sym_refs (state_hyp_refs_of sfix); mdb_cte_at (swp (cte_wp_at ((\<noteq>) cap.NullCap)) sfix) (cdt sfix); untyped_mdb (cdt sfix) (caps_of_state sfix); descendants_inc (cdt sfix) (caps_of_state sfix); no_mloop (cdt sfix); untyped_inc (cdt sfix) (caps_of_state sfix); ut_revocable (is_original_cap sfix) (caps_of_state sfix); irq_revocable (is_original_cap sfix) (caps_of_state sfix); reply_master_revocable (is_original_cap sfix) (caps_of_state sfix); reply_mdb (cdt sfix) (caps_of_state sfix); valid_ioc sfix; valid_idle sfix; only_idle sfix; if_unsafe_then_cap sfix; valid_reply_caps sfix; valid_reply_masters sfix; valid_global_refs sfix; valid_arch_state sfix; valid_irq_node sfix; valid_irq_handlers sfix; valid_irq_states sfix; valid_machine_state sfix; valid_vspace_objs sfix; valid_arch_caps sfix; valid_global_objs sfix; valid_kernel_mappings sfix; equal_kernel_mappings sfix; valid_asid_map sfix; valid_global_vspace_mappings sfix; pspace_in_kernel_window sfix; cap_refs_in_kernel_window sfix; pspace_respects_device_region sfix; cap_refs_respects_device_region sfix; cur_tcb sfix; a = idle_thread sfix\<rbrakk> \<Longrightarrow> mdb_cte_at (swp (cte_wp_at ?P42) sfix) (cdt sfix)
 2. \<lbrakk>(idle_thread sfix, b) \<in> CSpaceAcc_A.descendants_of slot' (cdt sfix); valid_objs sfix; pspace_aligned sfix; pspace_distinct sfix; if_live_then_nonz_cap sfix; zombies_final sfix; sym_refs (state_refs_of sfix); sym_refs (state_hyp_refs_of sfix); mdb_cte_at (swp (cte_wp_at ((\<noteq>) cap.NullCap)) sfix) (cdt sfix); untyped_mdb (cdt sfix) (caps_of_state sfix); descendants_inc (cdt sfix) (caps_of_state sfix); no_mloop (cdt sfix); untyped_inc (cdt sfix) (caps_of_state sfix); ut_revocable (is_original_cap sfix) (caps_of_state sfix); irq_revocable (is_original_cap sfix) (caps_of_state sfix); reply_master_revocable (is_original_cap sfix) (caps_of_state sfix); reply_mdb (cdt sfix) (caps_of_state sfix); valid_ioc sfix; valid_idle sfix; only_idle sfix; if_unsafe_then_cap sfix; valid_reply_caps sfix; valid_reply_masters sfix; valid_global_refs sfix; valid_arch_state sfix; valid_irq_node sfix; valid_irq_handlers sfix; valid_irq_states sfix; valid_machine_state sfix; valid_vspace_objs sfix; valid_arch_caps sfix; valid_global_objs sfix; valid_kernel_mappings sfix; equal_kernel_mappings sfix; valid_asid_map sfix; valid_global_vspace_mappings sfix; pspace_in_kernel_window sfix; cap_refs_in_kernel_window sfix; pspace_respects_device_region sfix; cap_refs_respects_device_region sfix; cur_tcb sfix; a = idle_thread sfix; cte_wp_at ?P42 (idle_thread sfix, b) sfix\<rbrakk> \<Longrightarrow> False proof (prove)
goal (1 subgoal):
 1. \<lbrakk>(idle_thread sfix, b) \<in> CSpaceAcc_A.descendants_of slot' (cdt sfix); valid_objs sfix; pspace_aligned sfix; pspace_distinct sfix; if_live_then_nonz_cap sfix; zombies_final sfix; sym_refs (state_refs_of sfix); sym_refs (state_hyp_refs_of sfix); mdb_cte_at (swp (cte_wp_at ((\<noteq>) cap.NullCap)) sfix) (cdt sfix); untyped_mdb (cdt sfix) (caps_of_state sfix); descendants_inc (cdt sfix) (caps_of_state sfix); no_mloop (cdt sfix); untyped_inc (cdt sfix) (caps_of_state sfix); ut_revocable (is_original_cap sfix) (caps_of_state sfix); irq_revocable (is_original_cap sfix) (caps_of_state sfix); reply_master_revocable (is_original_cap sfix) (caps_of_state sfix); reply_mdb (cdt sfix) (caps_of_state sfix); valid_ioc sfix; valid_idle sfix; only_idle sfix; if_unsafe_then_cap sfix; valid_reply_caps sfix; valid_reply_masters sfix; valid_global_refs sfix; valid_arch_state sfix; valid_irq_node sfix; valid_irq_handlers sfix; valid_irq_states sfix; valid_machine_state sfix; valid_vspace_objs sfix; valid_arch_caps sfix; valid_global_objs sfix; valid_kernel_mappings sfix; equal_kernel_mappings sfix; valid_asid_map sfix; valid_global_vspace_mappings sfix; pspace_in_kernel_window sfix; cap_refs_in_kernel_window sfix; pspace_respects_device_region sfix; cap_refs_respects_device_region sfix; cur_tcb sfix; a = idle_thread sfix; cte_wp_at ((\<noteq>) cap.NullCap) (idle_thread sfix, b) sfix\<rbrakk> \<Longrightarrow> False proof (prove)
goal (3 subgoals):
 1. \<lbrakk>(idle_thread sfix, b) \<in> CSpaceAcc_A.descendants_of slot' (cdt sfix); valid_objs sfix; pspace_aligned sfix; pspace_distinct sfix; if_live_then_nonz_cap sfix; zombies_final sfix; sym_refs (state_refs_of sfix); sym_refs (state_hyp_refs_of sfix); mdb_cte_at (swp (cte_wp_at ((\<noteq>) cap.NullCap)) sfix) (cdt sfix); untyped_mdb (cdt sfix) (caps_of_state sfix); descendants_inc (cdt sfix) (caps_of_state sfix); no_mloop (cdt sfix); untyped_inc (cdt sfix) (caps_of_state sfix); ut_revocable (is_original_cap sfix) (caps_of_state sfix); irq_revocable (is_original_cap sfix) (caps_of_state sfix); reply_master_revocable (is_original_cap sfix) (caps_of_state sfix); reply_mdb (cdt sfix) (caps_of_state sfix); valid_ioc sfix; valid_idle sfix; only_idle sfix; if_unsafe_then_cap sfix; valid_reply_caps sfix; valid_reply_masters sfix; valid_global_refs sfix; valid_arch_state sfix; valid_irq_node sfix; valid_irq_handlers sfix; valid_irq_states sfix; valid_machine_state sfix; valid_vspace_objs sfix; valid_arch_caps sfix; valid_global_objs sfix; valid_kernel_mappings sfix; equal_kernel_mappings sfix; valid_asid_map sfix; valid_global_vspace_mappings sfix; pspace_in_kernel_window sfix; cap_refs_in_kernel_window sfix; pspace_respects_device_region sfix; cap_refs_respects_device_region sfix; cur_tcb sfix; a = idle_thread sfix; cte_wp_at ((\<noteq>) cap.NullCap) (idle_thread sfix, b) sfix\<rbrakk> \<Longrightarrow> valid_global_refs sfix
 2. \<lbrakk>(idle_thread sfix, b) \<in> CSpaceAcc_A.descendants_of slot' (cdt sfix); valid_objs sfix; pspace_aligned sfix; pspace_distinct sfix; if_live_then_nonz_cap sfix; zombies_final sfix; sym_refs (state_refs_of sfix); sym_refs (state_hyp_refs_of sfix); mdb_cte_at (swp (cte_wp_at ((\<noteq>) cap.NullCap)) sfix) (cdt sfix); untyped_mdb (cdt sfix) (caps_of_state sfix); descendants_inc (cdt sfix) (caps_of_state sfix); no_mloop (cdt sfix); untyped_inc (cdt sfix) (caps_of_state sfix); ut_revocable (is_original_cap sfix) (caps_of_state sfix); irq_revocable (is_original_cap sfix) (caps_of_state sfix); reply_master_revocable (is_original_cap sfix) (caps_of_state sfix); reply_mdb (cdt sfix) (caps_of_state sfix); valid_ioc sfix; valid_idle sfix; only_idle sfix; if_unsafe_then_cap sfix; valid_reply_caps sfix; valid_reply_masters sfix; valid_global_refs sfix; valid_arch_state sfix; valid_irq_node sfix; valid_irq_handlers sfix; valid_irq_states sfix; valid_machine_state sfix; valid_vspace_objs sfix; valid_arch_caps sfix; valid_global_objs sfix; valid_kernel_mappings sfix; equal_kernel_mappings sfix; valid_asid_map sfix; valid_global_vspace_mappings sfix; pspace_in_kernel_window sfix; cap_refs_in_kernel_window sfix; pspace_respects_device_region sfix; cap_refs_respects_device_region sfix; cur_tcb sfix; a = idle_thread sfix; cte_wp_at ((\<noteq>) cap.NullCap) (idle_thread sfix, b) sfix\<rbrakk> \<Longrightarrow> cte_wp_at (\<lambda>_. True) ?slot45 sfix
 3. \<lbrakk>(idle_thread sfix, b) \<in> CSpaceAcc_A.descendants_of slot' (cdt sfix); valid_objs sfix; pspace_aligned sfix; pspace_distinct sfix; if_live_then_nonz_cap sfix; zombies_final sfix; sym_refs (state_refs_of sfix); sym_refs (state_hyp_refs_of sfix); mdb_cte_at (swp (cte_wp_at ((\<noteq>) cap.NullCap)) sfix) (cdt sfix); untyped_mdb (cdt sfix) (caps_of_state sfix); descendants_inc (cdt sfix) (caps_of_state sfix); no_mloop (cdt sfix); untyped_inc (cdt sfix) (caps_of_state sfix); ut_revocable (is_original_cap sfix) (caps_of_state sfix); irq_revocable (is_original_cap sfix) (caps_of_state sfix); reply_master_revocable (is_original_cap sfix) (caps_of_state sfix); reply_mdb (cdt sfix) (caps_of_state sfix); valid_ioc sfix; valid_idle sfix; only_idle sfix; if_unsafe_then_cap sfix; valid_reply_caps sfix; valid_reply_masters sfix; valid_global_refs sfix; valid_arch_state sfix; valid_irq_node sfix; valid_irq_handlers sfix; valid_irq_states sfix; valid_machine_state sfix; valid_vspace_objs sfix; valid_arch_caps sfix; valid_global_objs sfix; valid_kernel_mappings sfix; equal_kernel_mappings sfix; valid_asid_map sfix; valid_global_vspace_mappings sfix; pspace_in_kernel_window sfix; cap_refs_in_kernel_window sfix; pspace_respects_device_region sfix; cap_refs_respects_device_region sfix; cur_tcb sfix; a = idle_thread sfix; cte_wp_at ((\<noteq>) cap.NullCap) (idle_thread sfix, b) sfix; cte_wp_at (\<lambda>cap. \<forall>x\<in>obj_refs cap. not_idle_thread x sfix) ?slot45 sfix\<rbrakk> \<Longrightarrow> False proof (prove)
goal (2 subgoals):
 1. \<lbrakk>(idle_thread sfix, b) \<in> CSpaceAcc_A.descendants_of slot' (cdt sfix); valid_objs sfix; pspace_aligned sfix; pspace_distinct sfix; if_live_then_nonz_cap sfix; zombies_final sfix; sym_refs (state_refs_of sfix); sym_refs (state_hyp_refs_of sfix); mdb_cte_at (swp (cte_wp_at ((\<noteq>) cap.NullCap)) sfix) (cdt sfix); untyped_mdb (cdt sfix) (caps_of_state sfix); descendants_inc (cdt sfix) (caps_of_state sfix); no_mloop (cdt sfix); untyped_inc (cdt sfix) (caps_of_state sfix); ut_revocable (is_original_cap sfix) (caps_of_state sfix); irq_revocable (is_original_cap sfix) (caps_of_state sfix); reply_master_revocable (is_original_cap sfix) (caps_of_state sfix); reply_mdb (cdt sfix) (caps_of_state sfix); valid_ioc sfix; valid_idle sfix; only_idle sfix; if_unsafe_then_cap sfix; valid_reply_caps sfix; valid_reply_masters sfix; valid_global_refs sfix; valid_arch_state sfix; valid_irq_node sfix; valid_irq_handlers sfix; valid_irq_states sfix; valid_machine_state sfix; valid_vspace_objs sfix; valid_arch_caps sfix; valid_global_objs sfix; valid_kernel_mappings sfix; equal_kernel_mappings sfix; valid_asid_map sfix; valid_global_vspace_mappings sfix; pspace_in_kernel_window sfix; cap_refs_in_kernel_window sfix; pspace_respects_device_region sfix; cap_refs_respects_device_region sfix; cur_tcb sfix; a = idle_thread sfix; cte_wp_at ((\<noteq>) cap.NullCap) (idle_thread sfix, b) sfix\<rbrakk> \<Longrightarrow> cte_wp_at (\<lambda>_. True) ?slot45 sfix
 2. \<lbrakk>(idle_thread sfix, b) \<in> CSpaceAcc_A.descendants_of slot' (cdt sfix); valid_objs sfix; pspace_aligned sfix; pspace_distinct sfix; if_live_then_nonz_cap sfix; zombies_final sfix; sym_refs (state_refs_of sfix); sym_refs (state_hyp_refs_of sfix); mdb_cte_at (swp (cte_wp_at ((\<noteq>) cap.NullCap)) sfix) (cdt sfix); untyped_mdb (cdt sfix) (caps_of_state sfix); descendants_inc (cdt sfix) (caps_of_state sfix); no_mloop (cdt sfix); untyped_inc (cdt sfix) (caps_of_state sfix); ut_revocable (is_original_cap sfix) (caps_of_state sfix); irq_revocable (is_original_cap sfix) (caps_of_state sfix); reply_master_revocable (is_original_cap sfix) (caps_of_state sfix); reply_mdb (cdt sfix) (caps_of_state sfix); valid_ioc sfix; valid_idle sfix; only_idle sfix; if_unsafe_then_cap sfix; valid_reply_caps sfix; valid_reply_masters sfix; valid_global_refs sfix; valid_arch_state sfix; valid_irq_node sfix; valid_irq_handlers sfix; valid_irq_states sfix; valid_machine_state sfix; valid_vspace_objs sfix; valid_arch_caps sfix; valid_global_objs sfix; valid_kernel_mappings sfix; equal_kernel_mappings sfix; valid_asid_map sfix; valid_global_vspace_mappings sfix; pspace_in_kernel_window sfix; cap_refs_in_kernel_window sfix; pspace_respects_device_region sfix; cap_refs_respects_device_region sfix; cur_tcb sfix; a = idle_thread sfix; cte_wp_at ((\<noteq>) cap.NullCap) (idle_thread sfix, b) sfix; cte_wp_at (\<lambda>cap. \<forall>x\<in>obj_refs cap. not_idle_thread x sfix) ?slot45 sfix\<rbrakk> \<Longrightarrow> False proof (prove)
goal (2 subgoals):
 1. \<And>c. \<lbrakk>(idle_thread sfix, b) \<in> CSpaceAcc_A.descendants_of slot' (cdt sfix); valid_objs sfix; pspace_aligned sfix; pspace_distinct sfix; if_live_then_nonz_cap sfix; zombies_final sfix; sym_refs (state_refs_of sfix); sym_refs (state_hyp_refs_of sfix); mdb_cte_at (swp (cte_wp_at ((\<noteq>) cap.NullCap)) sfix) (cdt sfix); untyped_mdb (cdt sfix) (caps_of_state sfix); descendants_inc (cdt sfix) (caps_of_state sfix); no_mloop (cdt sfix); untyped_inc (cdt sfix) (caps_of_state sfix); ut_revocable (is_original_cap sfix) (caps_of_state sfix); irq_revocable (is_original_cap sfix) (caps_of_state sfix); reply_master_revocable (is_original_cap sfix) (caps_of_state sfix); reply_mdb (cdt sfix) (caps_of_state sfix); valid_ioc sfix; valid_idle sfix; only_idle sfix; if_unsafe_then_cap sfix; valid_reply_caps sfix; valid_reply_masters sfix; valid_global_refs sfix; valid_arch_state sfix; valid_irq_node sfix; valid_irq_handlers sfix; valid_irq_states sfix; valid_machine_state sfix; valid_vspace_objs sfix; valid_arch_caps sfix; valid_global_objs sfix; valid_kernel_mappings sfix; equal_kernel_mappings sfix; valid_asid_map sfix; valid_global_vspace_mappings sfix; pspace_in_kernel_window sfix; cap_refs_in_kernel_window sfix; pspace_respects_device_region sfix; cap_refs_respects_device_region sfix; cur_tcb sfix; a = idle_thread sfix; cap.NullCap \<noteq> c\<rbrakk> \<Longrightarrow> True
 2. \<lbrakk>(idle_thread sfix, b) \<in> CSpaceAcc_A.descendants_of slot' (cdt sfix); valid_objs sfix; pspace_aligned sfix; pspace_distinct sfix; if_live_then_nonz_cap sfix; zombies_final sfix; sym_refs (state_refs_of sfix); sym_refs (state_hyp_refs_of sfix); mdb_cte_at (swp (cte_wp_at ((\<noteq>) cap.NullCap)) sfix) (cdt sfix); untyped_mdb (cdt sfix) (caps_of_state sfix); descendants_inc (cdt sfix) (caps_of_state sfix); no_mloop (cdt sfix); untyped_inc (cdt sfix) (caps_of_state sfix); ut_revocable (is_original_cap sfix) (caps_of_state sfix); irq_revocable (is_original_cap sfix) (caps_of_state sfix); reply_master_revocable (is_original_cap sfix) (caps_of_state sfix); reply_mdb (cdt sfix) (caps_of_state sfix); valid_ioc sfix; valid_idle sfix; only_idle sfix; if_unsafe_then_cap sfix; valid_reply_caps sfix; valid_reply_masters sfix; valid_global_refs sfix; valid_arch_state sfix; valid_irq_node sfix; valid_irq_handlers sfix; valid_irq_states sfix; valid_machine_state sfix; valid_vspace_objs sfix; valid_arch_caps sfix; valid_global_objs sfix; valid_kernel_mappings sfix; equal_kernel_mappings sfix; valid_asid_map sfix; valid_global_vspace_mappings sfix; pspace_in_kernel_window sfix; cap_refs_in_kernel_window sfix; pspace_respects_device_region sfix; cap_refs_respects_device_region sfix; cur_tcb sfix; a = idle_thread sfix; cte_wp_at ((\<noteq>) cap.NullCap) (idle_thread sfix, b) sfix; cte_wp_at (\<lambda>cap. \<forall>x\<in>obj_refs cap. not_idle_thread x sfix) (idle_thread sfix, b) sfix\<rbrakk> \<Longrightarrow> False proof (prove)
goal (1 subgoal):
 1. \<lbrakk>(idle_thread sfix, b) \<in> CSpaceAcc_A.descendants_of slot' (cdt sfix); valid_objs sfix; pspace_aligned sfix; pspace_distinct sfix; if_live_then_nonz_cap sfix; zombies_final sfix; sym_refs (state_refs_of sfix); sym_refs (state_hyp_refs_of sfix); mdb_cte_at (swp (cte_wp_at ((\<noteq>) cap.NullCap)) sfix) (cdt sfix); untyped_mdb (cdt sfix) (caps_of_state sfix); descendants_inc (cdt sfix) (caps_of_state sfix); no_mloop (cdt sfix); untyped_inc (cdt sfix) (caps_of_state sfix); ut_revocable (is_original_cap sfix) (caps_of_state sfix); irq_revocable (is_original_cap sfix) (caps_of_state sfix); reply_master_revocable (is_original_cap sfix) (caps_of_state sfix); reply_mdb (cdt sfix) (caps_of_state sfix); valid_ioc sfix; valid_idle sfix; only_idle sfix; if_unsafe_then_cap sfix; valid_reply_caps sfix; valid_reply_masters sfix; valid_global_refs sfix; valid_arch_state sfix; valid_irq_node sfix; valid_irq_handlers sfix; valid_irq_states sfix; valid_machine_state sfix; valid_vspace_objs sfix; valid_arch_caps sfix; valid_global_objs sfix; valid_kernel_mappings sfix; equal_kernel_mappings sfix; valid_asid_map sfix; valid_global_vspace_mappings sfix; pspace_in_kernel_window sfix; cap_refs_in_kernel_window sfix; pspace_respects_device_region sfix; cap_refs_respects_device_region sfix; cur_tcb sfix; a = idle_thread sfix; cte_wp_at ((\<noteq>) cap.NullCap) (idle_thread sfix, b) sfix; cte_wp_at (\<lambda>cap. \<forall>x\<in>obj_refs cap. not_idle_thread x sfix) (idle_thread sfix, b) sfix\<rbrakk> \<Longrightarrow> False proof (prove)
goal (1 subgoal):
 1. \<And>cap. \<lbrakk>(idle_thread sfix, b) \<in> CSpaceAcc_A.descendants_of slot' (cdt sfix); valid_objs sfix; pspace_aligned sfix; pspace_distinct sfix; if_live_then_nonz_cap sfix; zombies_final sfix; sym_refs (state_refs_of sfix); sym_refs (state_hyp_refs_of sfix); mdb_cte_at (swp (cte_wp_at ((\<noteq>) cap.NullCap)) sfix) (cdt sfix); untyped_mdb (cdt sfix) (caps_of_state sfix); descendants_inc (cdt sfix) (caps_of_state sfix); no_mloop (cdt sfix); untyped_inc (cdt sfix) (caps_of_state sfix); ut_revocable (is_original_cap sfix) (caps_of_state sfix); irq_revocable (is_original_cap sfix) (caps_of_state sfix); reply_master_revocable (is_original_cap sfix) (caps_of_state sfix); reply_mdb (cdt sfix) (caps_of_state sfix); valid_ioc sfix; valid_idle sfix; only_idle sfix; if_unsafe_then_cap sfix; valid_reply_caps sfix; valid_reply_masters sfix; valid_global_refs sfix; valid_arch_state sfix; valid_irq_node sfix; valid_irq_handlers sfix; valid_irq_states sfix; valid_machine_state sfix; valid_vspace_objs sfix; valid_arch_caps sfix; valid_global_objs sfix; valid_kernel_mappings sfix; equal_kernel_mappings sfix; valid_asid_map sfix; valid_global_vspace_mappings sfix; pspace_in_kernel_window sfix; cap_refs_in_kernel_window sfix; pspace_respects_device_region sfix; cap_refs_respects_device_region sfix; cur_tcb sfix; a = idle_thread sfix; cap.NullCap \<noteq> cap; caps_of_state sfix (idle_thread sfix, b) = Some cap; \<forall>x\<in>obj_refs cap. not_idle_thread x sfix\<rbrakk> \<Longrightarrow> False proof (prove)
goal (5 subgoals):
 1. \<And>cap. \<lbrakk>(idle_thread sfix, b) \<in> CSpaceAcc_A.descendants_of slot' (cdt sfix); valid_objs sfix; pspace_aligned sfix; pspace_distinct sfix; if_live_then_nonz_cap sfix; zombies_final sfix; sym_refs (state_refs_of sfix); sym_refs (state_hyp_refs_of sfix); mdb_cte_at (swp (cte_wp_at ((\<noteq>) cap.NullCap)) sfix) (cdt sfix); untyped_mdb (cdt sfix) (caps_of_state sfix); descendants_inc (cdt sfix) (caps_of_state sfix); no_mloop (cdt sfix); untyped_inc (cdt sfix) (caps_of_state sfix); ut_revocable (is_original_cap sfix) (caps_of_state sfix); irq_revocable (is_original_cap sfix) (caps_of_state sfix); reply_master_revocable (is_original_cap sfix) (caps_of_state sfix); reply_mdb (cdt sfix) (caps_of_state sfix); valid_ioc sfix; valid_idle sfix; only_idle sfix; if_unsafe_then_cap sfix; valid_reply_caps sfix; valid_reply_masters sfix; valid_global_refs sfix; valid_arch_state sfix; valid_irq_node sfix; valid_irq_handlers sfix; valid_irq_states sfix; valid_machine_state sfix; valid_vspace_objs sfix; valid_arch_caps sfix; valid_global_objs sfix; valid_kernel_mappings sfix; equal_kernel_mappings sfix; valid_asid_map sfix; valid_global_vspace_mappings sfix; pspace_in_kernel_window sfix; cap_refs_in_kernel_window sfix; pspace_respects_device_region sfix; cap_refs_respects_device_region sfix; cur_tcb sfix; a = idle_thread sfix; cap.NullCap \<noteq> cap; caps_of_state sfix (idle_thread sfix, b) = Some cap; \<forall>x\<in>obj_refs cap. not_idle_thread x sfix\<rbrakk> \<Longrightarrow> valid_global_refs sfix
 2. \<And>cap. \<lbrakk>(idle_thread sfix, b) \<in> CSpaceAcc_A.descendants_of slot' (cdt sfix); valid_objs sfix; pspace_aligned sfix; pspace_distinct sfix; if_live_then_nonz_cap sfix; zombies_final sfix; sym_refs (state_refs_of sfix); sym_refs (state_hyp_refs_of sfix); mdb_cte_at (swp (cte_wp_at ((\<noteq>) cap.NullCap)) sfix) (cdt sfix); untyped_mdb (cdt sfix) (caps_of_state sfix); descendants_inc (cdt sfix) (caps_of_state sfix); no_mloop (cdt sfix); untyped_inc (cdt sfix) (caps_of_state sfix); ut_revocable (is_original_cap sfix) (caps_of_state sfix); irq_revocable (is_original_cap sfix) (caps_of_state sfix); reply_master_revocable (is_original_cap sfix) (caps_of_state sfix); reply_mdb (cdt sfix) (caps_of_state sfix); valid_ioc sfix; valid_idle sfix; only_idle sfix; if_unsafe_then_cap sfix; valid_reply_caps sfix; valid_reply_masters sfix; valid_global_refs sfix; valid_arch_state sfix; valid_irq_node sfix; valid_irq_handlers sfix; valid_irq_states sfix; valid_machine_state sfix; valid_vspace_objs sfix; valid_arch_caps sfix; valid_global_objs sfix; valid_kernel_mappings sfix; equal_kernel_mappings sfix; valid_asid_map sfix; valid_global_vspace_mappings sfix; pspace_in_kernel_window sfix; cap_refs_in_kernel_window sfix; pspace_respects_device_region sfix; cap_refs_respects_device_region sfix; cur_tcb sfix; a = idle_thread sfix; cap.NullCap \<noteq> cap; caps_of_state sfix (idle_thread sfix, b) = Some cap; \<forall>x\<in>obj_refs cap. not_idle_thread x sfix\<rbrakk> \<Longrightarrow> valid_idle sfix
 3. \<And>cap. \<lbrakk>(idle_thread sfix, b) \<in> CSpaceAcc_A.descendants_of slot' (cdt sfix); valid_objs sfix; pspace_aligned sfix; pspace_distinct sfix; if_live_then_nonz_cap sfix; zombies_final sfix; sym_refs (state_refs_of sfix); sym_refs (state_hyp_refs_of sfix); mdb_cte_at (swp (cte_wp_at ((\<noteq>) cap.NullCap)) sfix) (cdt sfix); untyped_mdb (cdt sfix) (caps_of_state sfix); descendants_inc (cdt sfix) (caps_of_state sfix); no_mloop (cdt sfix); untyped_inc (cdt sfix) (caps_of_state sfix); ut_revocable (is_original_cap sfix) (caps_of_state sfix); irq_revocable (is_original_cap sfix) (caps_of_state sfix); reply_master_revocable (is_original_cap sfix) (caps_of_state sfix); reply_mdb (cdt sfix) (caps_of_state sfix); valid_ioc sfix; valid_idle sfix; only_idle sfix; if_unsafe_then_cap sfix; valid_reply_caps sfix; valid_reply_masters sfix; valid_global_refs sfix; valid_arch_state sfix; valid_irq_node sfix; valid_irq_handlers sfix; valid_irq_states sfix; valid_machine_state sfix; valid_vspace_objs sfix; valid_arch_caps sfix; valid_global_objs sfix; valid_kernel_mappings sfix; equal_kernel_mappings sfix; valid_asid_map sfix; valid_global_vspace_mappings sfix; pspace_in_kernel_window sfix; cap_refs_in_kernel_window sfix; pspace_respects_device_region sfix; cap_refs_respects_device_region sfix; cur_tcb sfix; a = idle_thread sfix; cap.NullCap \<noteq> cap; caps_of_state sfix (idle_thread sfix, b) = Some cap; \<forall>x\<in>obj_refs cap. not_idle_thread x sfix\<rbrakk> \<Longrightarrow> valid_irq_node sfix
 4. \<And>cap. \<lbrakk>(idle_thread sfix, b) \<in> CSpaceAcc_A.descendants_of slot' (cdt sfix); valid_objs sfix; pspace_aligned sfix; pspace_distinct sfix; if_live_then_nonz_cap sfix; zombies_final sfix; sym_refs (state_refs_of sfix); sym_refs (state_hyp_refs_of sfix); mdb_cte_at (swp (cte_wp_at ((\<noteq>) cap.NullCap)) sfix) (cdt sfix); untyped_mdb (cdt sfix) (caps_of_state sfix); descendants_inc (cdt sfix) (caps_of_state sfix); no_mloop (cdt sfix); untyped_inc (cdt sfix) (caps_of_state sfix); ut_revocable (is_original_cap sfix) (caps_of_state sfix); irq_revocable (is_original_cap sfix) (caps_of_state sfix); reply_master_revocable (is_original_cap sfix) (caps_of_state sfix); reply_mdb (cdt sfix) (caps_of_state sfix); valid_ioc sfix; valid_idle sfix; only_idle sfix; if_unsafe_then_cap sfix; valid_reply_caps sfix; valid_reply_masters sfix; valid_global_refs sfix; valid_arch_state sfix; valid_irq_node sfix; valid_irq_handlers sfix; valid_irq_states sfix; valid_machine_state sfix; valid_vspace_objs sfix; valid_arch_caps sfix; valid_global_objs sfix; valid_kernel_mappings sfix; equal_kernel_mappings sfix; valid_asid_map sfix; valid_global_vspace_mappings sfix; pspace_in_kernel_window sfix; cap_refs_in_kernel_window sfix; pspace_respects_device_region sfix; cap_refs_respects_device_region sfix; cur_tcb sfix; a = idle_thread sfix; cap.NullCap \<noteq> cap; caps_of_state sfix (idle_thread sfix, b) = Some cap; \<forall>x\<in>obj_refs cap. not_idle_thread x sfix\<rbrakk> \<Longrightarrow> caps_of_state sfix (idle_thread sfix, ?v56 cap) = Some (?cap56 cap)
 5. \<And>cap. \<lbrakk>(idle_thread sfix, b) \<in> CSpaceAcc_A.descendants_of slot' (cdt sfix); valid_objs sfix; pspace_aligned sfix; pspace_distinct sfix; if_live_then_nonz_cap sfix; zombies_final sfix; sym_refs (state_refs_of sfix); sym_refs (state_hyp_refs_of sfix); mdb_cte_at (swp (cte_wp_at ((\<noteq>) cap.NullCap)) sfix) (cdt sfix); untyped_mdb (cdt sfix) (caps_of_state sfix); descendants_inc (cdt sfix) (caps_of_state sfix); no_mloop (cdt sfix); untyped_inc (cdt sfix) (caps_of_state sfix); ut_revocable (is_original_cap sfix) (caps_of_state sfix); irq_revocable (is_original_cap sfix) (caps_of_state sfix); reply_master_revocable (is_original_cap sfix) (caps_of_state sfix); reply_mdb (cdt sfix) (caps_of_state sfix); valid_ioc sfix; valid_idle sfix; only_idle sfix; if_unsafe_then_cap sfix; valid_reply_caps sfix; valid_reply_masters sfix; valid_global_refs sfix; valid_arch_state sfix; valid_irq_node sfix; valid_irq_handlers sfix; valid_irq_states sfix; valid_machine_state sfix; valid_vspace_objs sfix; valid_arch_caps sfix; valid_global_objs sfix; valid_kernel_mappings sfix; equal_kernel_mappings sfix; valid_asid_map sfix; valid_global_vspace_mappings sfix; pspace_in_kernel_window sfix; cap_refs_in_kernel_window sfix; pspace_respects_device_region sfix; cap_refs_respects_device_region sfix; cur_tcb sfix; a = idle_thread sfix; cap.NullCap \<noteq> cap; caps_of_state sfix (idle_thread sfix, b) = Some cap; \<forall>x\<in>obj_refs cap. not_idle_thread x sfix; ?cap56 cap = cap.NullCap\<rbrakk> \<Longrightarrow> False proof (prove)
goal:
No subgoals!