theory Untyped_R

lemma descendants_range_ex_cte':
  "\<lbrakk>descendants_range_in' S p (ctes_of s');ex_cte_cap_wp_to' P q s'; S \<subseteq> capRange (cteCap cte);
    invs' s';ctes_of s' p = Some cte;isUntypedCap (cteCap cte)\<rbrakk> \<Longrightarrow> q \<notin> S" apply (frule invs_valid_objs') apply (frule invs_mdb') apply (clarsimp simp:invs'_def valid_state'_def) apply (clarsimp simp: ex_cte_cap_to'_def cte_wp_at_ctes_of) apply (frule_tac cte = "cte" in  valid_global_refsD') apply simp apply (case_tac "\<exists>irq. cteCap ctea = IRQHandlerCap irq") apply clarsimp apply (erule(1) in_empty_interE[OF _ _ subsetD,rotated -1]) apply (clarsimp simp:global_refs'_def cteSizeBits_def shiftl_t2n) apply (erule_tac A = "range P" for P in subsetD) apply (simp add:range_eqI field_simps) apply (case_tac ctea) apply clarsimp apply (case_tac ctea) apply (drule_tac cte = "cte" and cte' = ctea in untyped_mdbD') apply assumption apply (clarsimp simp:isCap_simps) apply (drule_tac B = "untypedRange (cteCap cte)" in subsetD[rotated]) apply (clarsimp simp:untypedCapRange) apply clarsimp apply (drule_tac x = " (irq_node' s')" in cte_refs_capRange[rotated]) apply (erule(1) ctes_of_valid_cap') apply blast apply (clarsimp simp:isCap_simps) apply (simp add:valid_mdb'_def valid_mdb_ctes_def) apply (drule(2) descendants_range_inD') apply clarsimp apply (drule_tac x = " (irq_node' s')" in cte_refs_capRange[rotated]) apply (erule(1) ctes_of_valid_cap') apply blast done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>descendants_range_in' S p (ctes_of s'); ex_cte_cap_wp_to' P q s'; S \<subseteq> capRange (cteCap cte); invs' s'; ctes_of s' p = Some cte; isUntypedCap (cteCap cte)\<rbrakk> \<Longrightarrow> q \<notin> S proof (prove)
goal (1 subgoal):
 1. \<lbrakk>descendants_range_in' S p (ctes_of s'); ex_cte_cap_wp_to' P q s'; S \<subseteq> capRange (cteCap cte); invs' s'; ctes_of s' p = Some cte; isUntypedCap (cteCap cte); valid_objs' s'\<rbrakk> \<Longrightarrow> q \<notin> S proof (prove)
goal (1 subgoal):
 1. \<lbrakk>descendants_range_in' S p (ctes_of s'); ex_cte_cap_wp_to' P q s'; S \<subseteq> capRange (cteCap cte); invs' s'; ctes_of s' p = Some cte; isUntypedCap (cteCap cte); valid_objs' s'; valid_mdb' s'\<rbrakk> \<Longrightarrow> q \<notin> S proof (prove)
goal (1 subgoal):
 1. \<lbrakk>descendants_range_in' S p (ctes_of s'); ex_cte_cap_wp_to' P q s'; S \<subseteq> capRange (cteCap cte); ctes_of s' p = Some cte; isUntypedCap (cteCap cte); valid_objs' s'; valid_mdb' s'; valid_pspace' s'; sch_act_wf (ksSchedulerAction s') s'; Invariants_H.valid_queues s'; sym_refs (state_refs_of' s'); if_live_then_nonz_cap' s'; if_unsafe_then_cap' s'; valid_idle' s'; valid_global_refs' s'; valid_arch_state' s'; valid_irq_node' (irq_node' s') s'; valid_irq_handlers' s'; valid_irq_states' s'; valid_machine_state' s'; irqs_masked' s'; valid_queues' s'; ct_not_inQ s'; ct_idle_or_in_cur_domain' s'; valid_pde_mappings' s'; pspace_domain_valid s'; ksCurDomain s' \<le> maxDomain; ksDomSchedule (KernelInit_H.newKernelState undefined) \<noteq> []; \<forall>x\<in>set (ksDomSchedule (KernelInit_H.newKernelState undefined)). dschDomain x \<le> maxDomain \<and> 0 < dschLength x; ksDomSchedule s' = ksDomSchedule (KernelInit_H.newKernelState undefined); ksDomScheduleIdx s' < length (ksDomSchedule (KernelInit_H.newKernelState undefined)); untyped_ranges_zero' s'; cur_tcb' s'; q \<in> S\<rbrakk> \<Longrightarrow> False proof (prove)
goal (1 subgoal):
 1. \<And>cref ctea. \<lbrakk>descendants_range_in' S p (ctes_of s'); S \<subseteq> capRange (cteCap cte); ctes_of s' p = Some cte; isUntypedCap (cteCap cte); valid_objs' s'; valid_mdb' s'; valid_pspace' s'; sch_act_wf (ksSchedulerAction s') s'; Invariants_H.valid_queues s'; sym_refs (state_refs_of' s'); if_live_then_nonz_cap' s'; if_unsafe_then_cap' s'; valid_idle' s'; valid_global_refs' s'; valid_arch_state' s'; valid_irq_node' (irq_node' s') s'; valid_irq_handlers' s'; valid_irq_states' s'; valid_machine_state' s'; irqs_masked' s'; valid_queues' s'; ct_not_inQ s'; ct_idle_or_in_cur_domain' s'; valid_pde_mappings' s'; pspace_domain_valid s'; ksCurDomain s' \<le> maxDomain; ksDomSchedule (KernelInit_H.newKernelState undefined) \<noteq> []; \<forall>x\<in>set (ksDomSchedule (KernelInit_H.newKernelState undefined)). dschDomain x \<le> maxDomain \<and> 0 < dschLength x; ksDomSchedule s' = ksDomSchedule (KernelInit_H.newKernelState undefined); ksDomScheduleIdx s' < length (ksDomSchedule (KernelInit_H.newKernelState undefined)); untyped_ranges_zero' s'; cur_tcb' s'; q \<in> S; ctes_of s' cref = Some ctea; P (cteCap ctea); q \<in> cte_refs' (cteCap ctea) (irq_node' s')\<rbrakk> \<Longrightarrow> False proof (prove)
goal (2 subgoals):
 1. \<And>cref ctea. \<lbrakk>descendants_range_in' S p (ctes_of s'); S \<subseteq> capRange (cteCap cte); ctes_of s' p = Some cte; isUntypedCap (cteCap cte); valid_objs' s'; valid_mdb' s'; valid_pspace' s'; sch_act_wf (ksSchedulerAction s') s'; Invariants_H.valid_queues s'; sym_refs (state_refs_of' s'); if_live_then_nonz_cap' s'; if_unsafe_then_cap' s'; valid_idle' s'; valid_global_refs' s'; valid_arch_state' s'; valid_irq_node' (irq_node' s') s'; valid_irq_handlers' s'; valid_irq_states' s'; valid_machine_state' s'; irqs_masked' s'; valid_queues' s'; ct_not_inQ s'; ct_idle_or_in_cur_domain' s'; valid_pde_mappings' s'; pspace_domain_valid s'; ksCurDomain s' \<le> maxDomain; ksDomSchedule (KernelInit_H.newKernelState undefined) \<noteq> []; \<forall>x\<in>set (ksDomSchedule (KernelInit_H.newKernelState undefined)). dschDomain x \<le> maxDomain \<and> 0 < dschLength x; ksDomSchedule s' = ksDomSchedule (KernelInit_H.newKernelState undefined); ksDomScheduleIdx s' < length (ksDomSchedule (KernelInit_H.newKernelState undefined)); untyped_ranges_zero' s'; cur_tcb' s'; q \<in> S; ctes_of s' cref = Some ctea; P (cteCap ctea); q \<in> cte_refs' (cteCap ctea) (irq_node' s')\<rbrakk> \<Longrightarrow> valid_global_refs' s'
 2. \<And>cref ctea. \<lbrakk>descendants_range_in' S p (ctes_of s'); S \<subseteq> capRange (cteCap cte); ctes_of s' p = Some cte; isUntypedCap (cteCap cte); valid_objs' s'; valid_mdb' s'; valid_pspace' s'; sch_act_wf (ksSchedulerAction s') s'; Invariants_H.valid_queues s'; sym_refs (state_refs_of' s'); if_live_then_nonz_cap' s'; if_unsafe_then_cap' s'; valid_idle' s'; valid_global_refs' s'; valid_arch_state' s'; valid_irq_node' (irq_node' s') s'; valid_irq_handlers' s'; valid_irq_states' s'; valid_machine_state' s'; irqs_masked' s'; valid_queues' s'; ct_not_inQ s'; ct_idle_or_in_cur_domain' s'; valid_pde_mappings' s'; pspace_domain_valid s'; ksCurDomain s' \<le> maxDomain; ksDomSchedule (KernelInit_H.newKernelState undefined) \<noteq> []; \<forall>x\<in>set (ksDomSchedule (KernelInit_H.newKernelState undefined)). dschDomain x \<le> maxDomain \<and> 0 < dschLength x; ksDomSchedule s' = ksDomSchedule (KernelInit_H.newKernelState undefined); ksDomScheduleIdx s' < length (ksDomSchedule (KernelInit_H.newKernelState undefined)); untyped_ranges_zero' s'; cur_tcb' s'; q \<in> S; ctes_of s' cref = Some ctea; P (cteCap ctea); q \<in> cte_refs' (cteCap ctea) (irq_node' s'); kernel_data_refs \<inter> capRange (cteCap cte) = {} \<and> global_refs' s' \<subseteq> kernel_data_refs\<rbrakk> \<Longrightarrow> False proof (prove)
goal (1 subgoal):
 1. \<And>cref ctea. \<lbrakk>descendants_range_in' S p (ctes_of s'); S \<subseteq> capRange (cteCap cte); ctes_of s' p = Some cte; isUntypedCap (cteCap cte); valid_objs' s'; valid_mdb' s'; valid_pspace' s'; sch_act_wf (ksSchedulerAction s') s'; Invariants_H.valid_queues s'; sym_refs (state_refs_of' s'); if_live_then_nonz_cap' s'; if_unsafe_then_cap' s'; valid_idle' s'; valid_global_refs' s'; valid_arch_state' s'; valid_irq_node' (irq_node' s') s'; valid_irq_handlers' s'; valid_irq_states' s'; valid_machine_state' s'; irqs_masked' s'; valid_queues' s'; ct_not_inQ s'; ct_idle_or_in_cur_domain' s'; valid_pde_mappings' s'; pspace_domain_valid s'; ksCurDomain s' \<le> maxDomain; ksDomSchedule (KernelInit_H.newKernelState undefined) \<noteq> []; \<forall>x\<in>set (ksDomSchedule (KernelInit_H.newKernelState undefined)). dschDomain x \<le> maxDomain \<and> 0 < dschLength x; ksDomSchedule s' = ksDomSchedule (KernelInit_H.newKernelState undefined); ksDomScheduleIdx s' < length (ksDomSchedule (KernelInit_H.newKernelState undefined)); untyped_ranges_zero' s'; cur_tcb' s'; q \<in> S; ctes_of s' cref = Some ctea; P (cteCap ctea); q \<in> cte_refs' (cteCap ctea) (irq_node' s'); kernel_data_refs \<inter> capRange (cteCap cte) = {} \<and> global_refs' s' \<subseteq> kernel_data_refs\<rbrakk> \<Longrightarrow> False proof (prove)
goal (2 subgoals):
 1. \<And>cref ctea. \<lbrakk>descendants_range_in' S p (ctes_of s'); S \<subseteq> capRange (cteCap cte); ctes_of s' p = Some cte; isUntypedCap (cteCap cte); valid_objs' s'; valid_mdb' s'; valid_pspace' s'; sch_act_wf (ksSchedulerAction s') s'; Invariants_H.valid_queues s'; sym_refs (state_refs_of' s'); if_live_then_nonz_cap' s'; if_unsafe_then_cap' s'; valid_idle' s'; valid_global_refs' s'; valid_arch_state' s'; valid_irq_node' (irq_node' s') s'; valid_irq_handlers' s'; valid_irq_states' s'; valid_machine_state' s'; irqs_masked' s'; valid_queues' s'; ct_not_inQ s'; ct_idle_or_in_cur_domain' s'; valid_pde_mappings' s'; pspace_domain_valid s'; ksCurDomain s' \<le> maxDomain; ksDomSchedule (KernelInit_H.newKernelState undefined) \<noteq> []; \<forall>x\<in>set (ksDomSchedule (KernelInit_H.newKernelState undefined)). dschDomain x \<le> maxDomain \<and> 0 < dschLength x; ksDomSchedule s' = ksDomSchedule (KernelInit_H.newKernelState undefined); ksDomScheduleIdx s' < length (ksDomSchedule (KernelInit_H.newKernelState undefined)); untyped_ranges_zero' s'; cur_tcb' s'; q \<in> S; ctes_of s' cref = Some ctea; P (cteCap ctea); q \<in> cte_refs' (cteCap ctea) (irq_node' s'); kernel_data_refs \<inter> capRange (cteCap cte) = {} \<and> global_refs' s' \<subseteq> kernel_data_refs; \<exists>irq. cteCap ctea = capability.IRQHandlerCap irq\<rbrakk> \<Longrightarrow> False
 2. \<And>cref ctea. \<lbrakk>descendants_range_in' S p (ctes_of s'); S \<subseteq> capRange (cteCap cte); ctes_of s' p = Some cte; isUntypedCap (cteCap cte); valid_objs' s'; valid_mdb' s'; valid_pspace' s'; sch_act_wf (ksSchedulerAction s') s'; Invariants_H.valid_queues s'; sym_refs (state_refs_of' s'); if_live_then_nonz_cap' s'; if_unsafe_then_cap' s'; valid_idle' s'; valid_global_refs' s'; valid_arch_state' s'; valid_irq_node' (irq_node' s') s'; valid_irq_handlers' s'; valid_irq_states' s'; valid_machine_state' s'; irqs_masked' s'; valid_queues' s'; ct_not_inQ s'; ct_idle_or_in_cur_domain' s'; valid_pde_mappings' s'; pspace_domain_valid s'; ksCurDomain s' \<le> maxDomain; ksDomSchedule (KernelInit_H.newKernelState undefined) \<noteq> []; \<forall>x\<in>set (ksDomSchedule (KernelInit_H.newKernelState undefined)). dschDomain x \<le> maxDomain \<and> 0 < dschLength x; ksDomSchedule s' = ksDomSchedule (KernelInit_H.newKernelState undefined); ksDomScheduleIdx s' < length (ksDomSchedule (KernelInit_H.newKernelState undefined)); untyped_ranges_zero' s'; cur_tcb' s'; q \<in> S; ctes_of s' cref = Some ctea; P (cteCap ctea); q \<in> cte_refs' (cteCap ctea) (irq_node' s'); kernel_data_refs \<inter> capRange (cteCap cte) = {} \<and> global_refs' s' \<subseteq> kernel_data_refs; \<nexists>irq. cteCap ctea = capability.IRQHandlerCap irq\<rbrakk> \<Longrightarrow> False proof (prove)
goal (2 subgoals):
 1. \<And>cref ctea irq. \<lbrakk>descendants_range_in' S p (ctes_of s'); S \<subseteq> capRange (cteCap cte); ctes_of s' p = Some cte; isUntypedCap (cteCap cte); valid_objs' s'; valid_mdb' s'; valid_pspace' s'; sch_act_wf (ksSchedulerAction s') s'; Invariants_H.valid_queues s'; sym_refs (state_refs_of' s'); if_live_then_nonz_cap' s'; if_unsafe_then_cap' s'; valid_idle' s'; valid_global_refs' s'; valid_arch_state' s'; valid_irq_node' (irq_node' s') s'; valid_irq_handlers' s'; valid_irq_states' s'; valid_machine_state' s'; irqs_masked' s'; valid_queues' s'; ct_not_inQ s'; ct_idle_or_in_cur_domain' s'; valid_pde_mappings' s'; pspace_domain_valid s'; ksCurDomain s' \<le> maxDomain; ksDomSchedule (KernelInit_H.newKernelState undefined) \<noteq> []; \<forall>x\<in>set (ksDomSchedule (KernelInit_H.newKernelState undefined)). dschDomain x \<le> maxDomain \<and> 0 < dschLength x; ksDomSchedule s' = ksDomSchedule (KernelInit_H.newKernelState undefined); ksDomScheduleIdx s' < length (ksDomSchedule (KernelInit_H.newKernelState undefined)); untyped_ranges_zero' s'; cur_tcb' s'; irq_node' s' + UCAST(10 \<rightarrow> 32) irq * 0x10 \<in> S; ctes_of s' cref = Some ctea; P (capability.IRQHandlerCap irq); q = irq_node' s' + UCAST(10 \<rightarrow> 32) irq * 0x10; cteCap ctea = capability.IRQHandlerCap irq; kernel_data_refs \<inter> capRange (cteCap cte) = {}; global_refs' s' \<subseteq> kernel_data_refs\<rbrakk> \<Longrightarrow> False
 2. \<And>cref ctea. \<lbrakk>descendants_range_in' S p (ctes_of s'); S \<subseteq> capRange (cteCap cte); ctes_of s' p = Some cte; isUntypedCap (cteCap cte); valid_objs' s'; valid_mdb' s'; valid_pspace' s'; sch_act_wf (ksSchedulerAction s') s'; Invariants_H.valid_queues s'; sym_refs (state_refs_of' s'); if_live_then_nonz_cap' s'; if_unsafe_then_cap' s'; valid_idle' s'; valid_global_refs' s'; valid_arch_state' s'; valid_irq_node' (irq_node' s') s'; valid_irq_handlers' s'; valid_irq_states' s'; valid_machine_state' s'; irqs_masked' s'; valid_queues' s'; ct_not_inQ s'; ct_idle_or_in_cur_domain' s'; valid_pde_mappings' s'; pspace_domain_valid s'; ksCurDomain s' \<le> maxDomain; ksDomSchedule (KernelInit_H.newKernelState undefined) \<noteq> []; \<forall>x\<in>set (ksDomSchedule (KernelInit_H.newKernelState undefined)). dschDomain x \<le> maxDomain \<and> 0 < dschLength x; ksDomSchedule s' = ksDomSchedule (KernelInit_H.newKernelState undefined); ksDomScheduleIdx s' < length (ksDomSchedule (KernelInit_H.newKernelState undefined)); untyped_ranges_zero' s'; cur_tcb' s'; q \<in> S; ctes_of s' cref = Some ctea; P (cteCap ctea); q \<in> cte_refs' (cteCap ctea) (irq_node' s'); kernel_data_refs \<inter> capRange (cteCap cte) = {} \<and> global_refs' s' \<subseteq> kernel_data_refs; \<nexists>irq. cteCap ctea = capability.IRQHandlerCap irq\<rbrakk> \<Longrightarrow> False proof (prove)
goal (3 subgoals):
 1. \<And>cref ctea irq. \<lbrakk>descendants_range_in' S p (ctes_of s'); S \<subseteq> capRange (cteCap cte); ctes_of s' p = Some cte; isUntypedCap (cteCap cte); valid_objs' s'; valid_mdb' s'; valid_pspace' s'; sch_act_wf (ksSchedulerAction s') s'; Invariants_H.valid_queues s'; sym_refs (state_refs_of' s'); if_live_then_nonz_cap' s'; if_unsafe_then_cap' s'; valid_idle' s'; valid_global_refs' s'; valid_arch_state' s'; valid_irq_node' (irq_node' s') s'; valid_irq_handlers' s'; valid_irq_states' s'; valid_machine_state' s'; irqs_masked' s'; valid_queues' s'; ct_not_inQ s'; ct_idle_or_in_cur_domain' s'; valid_pde_mappings' s'; pspace_domain_valid s'; ksCurDomain s' \<le> maxDomain; ksDomSchedule (KernelInit_H.newKernelState undefined) \<noteq> []; \<forall>x\<in>set (ksDomSchedule (KernelInit_H.newKernelState undefined)). dschDomain x \<le> maxDomain \<and> 0 < dschLength x; ksDomSchedule s' = ksDomSchedule (KernelInit_H.newKernelState undefined); ksDomScheduleIdx s' < length (ksDomSchedule (KernelInit_H.newKernelState undefined)); untyped_ranges_zero' s'; cur_tcb' s'; ctes_of s' cref = Some ctea; P (capability.IRQHandlerCap irq); q = irq_node' s' + UCAST(10 \<rightarrow> 32) irq * 0x10; cteCap ctea = capability.IRQHandlerCap irq; kernel_data_refs \<inter> capRange (cteCap cte) = {}; global_refs' s' \<subseteq> kernel_data_refs\<rbrakk> \<Longrightarrow> irq_node' s' + UCAST(10 \<rightarrow> 32) irq * 0x10 \<in> kernel_data_refs
 2. \<And>cref ctea irq. \<lbrakk>descendants_range_in' S p (ctes_of s'); S \<subseteq> capRange (cteCap cte); ctes_of s' p = Some cte; isUntypedCap (cteCap cte); valid_objs' s'; valid_mdb' s'; valid_pspace' s'; sch_act_wf (ksSchedulerAction s') s'; Invariants_H.valid_queues s'; sym_refs (state_refs_of' s'); if_live_then_nonz_cap' s'; if_unsafe_then_cap' s'; valid_idle' s'; valid_global_refs' s'; valid_arch_state' s'; valid_irq_node' (irq_node' s') s'; valid_irq_handlers' s'; valid_irq_states' s'; valid_machine_state' s'; irqs_masked' s'; valid_queues' s'; ct_not_inQ s'; ct_idle_or_in_cur_domain' s'; valid_pde_mappings' s'; pspace_domain_valid s'; ksCurDomain s' \<le> maxDomain; ksDomSchedule (KernelInit_H.newKernelState undefined) \<noteq> []; \<forall>x\<in>set (ksDomSchedule (KernelInit_H.newKernelState undefined)). dschDomain x \<le> maxDomain \<and> 0 < dschLength x; ksDomSchedule s' = ksDomSchedule (KernelInit_H.newKernelState undefined); ksDomScheduleIdx s' < length (ksDomSchedule (KernelInit_H.newKernelState undefined)); untyped_ranges_zero' s'; cur_tcb' s'; ctes_of s' cref = Some ctea; P (capability.IRQHandlerCap irq); q = irq_node' s' + UCAST(10 \<rightarrow> 32) irq * 0x10; cteCap ctea = capability.IRQHandlerCap irq; kernel_data_refs \<inter> capRange (cteCap cte) = {}; global_refs' s' \<subseteq> kernel_data_refs\<rbrakk> \<Longrightarrow> S \<subseteq> capRange (cteCap cte)
 3. \<And>cref ctea. \<lbrakk>descendants_range_in' S p (ctes_of s'); S \<subseteq> capRange (cteCap cte); ctes_of s' p = Some cte; isUntypedCap (cteCap cte); valid_objs' s'; valid_mdb' s'; valid_pspace' s'; sch_act_wf (ksSchedulerAction s') s'; Invariants_H.valid_queues s'; sym_refs (state_refs_of' s'); if_live_then_nonz_cap' s'; if_unsafe_then_cap' s'; valid_idle' s'; valid_global_refs' s'; valid_arch_state' s'; valid_irq_node' (irq_node' s') s'; valid_irq_handlers' s'; valid_irq_states' s'; valid_machine_state' s'; irqs_masked' s'; valid_queues' s'; ct_not_inQ s'; ct_idle_or_in_cur_domain' s'; valid_pde_mappings' s'; pspace_domain_valid s'; ksCurDomain s' \<le> maxDomain; ksDomSchedule (KernelInit_H.newKernelState undefined) \<noteq> []; \<forall>x\<in>set (ksDomSchedule (KernelInit_H.newKernelState undefined)). dschDomain x \<le> maxDomain \<and> 0 < dschLength x; ksDomSchedule s' = ksDomSchedule (KernelInit_H.newKernelState undefined); ksDomScheduleIdx s' < length (ksDomSchedule (KernelInit_H.newKernelState undefined)); untyped_ranges_zero' s'; cur_tcb' s'; q \<in> S; ctes_of s' cref = Some ctea; P (cteCap ctea); q \<in> cte_refs' (cteCap ctea) (irq_node' s'); kernel_data_refs \<inter> capRange (cteCap cte) = {} \<and> global_refs' s' \<subseteq> kernel_data_refs; \<nexists>irq. cteCap ctea = capability.IRQHandlerCap irq\<rbrakk> \<Longrightarrow> False proof (prove)
goal (3 subgoals):
 1. \<And>cref ctea irq. \<lbrakk>descendants_range_in' S p (ctes_of s'); S \<subseteq> capRange (cteCap cte); ctes_of s' p = Some cte; isUntypedCap (cteCap cte); valid_objs' s'; valid_mdb' s'; valid_pspace' s'; sch_act_wf (ksSchedulerAction s') s'; Invariants_H.valid_queues s'; sym_refs (state_refs_of' s'); if_live_then_nonz_cap' s'; if_unsafe_then_cap' s'; valid_idle' s'; valid_global_refs' s'; valid_arch_state' s'; valid_irq_node' (irq_node' s') s'; valid_irq_handlers' s'; valid_irq_states' s'; valid_machine_state' s'; irqs_masked' s'; valid_queues' s'; ct_not_inQ s'; ct_idle_or_in_cur_domain' s'; valid_pde_mappings' s'; pspace_domain_valid s'; ksCurDomain s' \<le> maxDomain; ksDomSchedule (KernelInit_H.newKernelState undefined) \<noteq> []; \<forall>x\<in>set (ksDomSchedule (KernelInit_H.newKernelState undefined)). dschDomain x \<le> maxDomain \<and> 0 < dschLength x; ksDomSchedule s' = ksDomSchedule (KernelInit_H.newKernelState undefined); ksDomScheduleIdx s' < length (ksDomSchedule (KernelInit_H.newKernelState undefined)); untyped_ranges_zero' s'; cur_tcb' s'; ctes_of s' cref = Some ctea; P (capability.IRQHandlerCap irq); q = irq_node' s' + UCAST(10 \<rightarrow> 32) irq * 0x10; cteCap ctea = capability.IRQHandlerCap irq; kernel_data_refs \<inter> capRange (cteCap cte) = {}; ksIdleThread s' \<in> kernel_data_refs; page_directory_refs' (armKSGlobalPD (ksArchState s')) \<subseteq> kernel_data_refs; \<Union> (page_table_refs' ` set (armKSGlobalPTs (ksArchState s'))) \<subseteq> kernel_data_refs; range (\<lambda>x. irq_node' s' + 0x10 * UCAST(10 \<rightarrow> 32) x) \<subseteq> kernel_data_refs\<rbrakk> \<Longrightarrow> irq_node' s' + UCAST(10 \<rightarrow> 32) irq * 0x10 \<in> kernel_data_refs
 2. \<And>cref ctea irq. \<lbrakk>descendants_range_in' S p (ctes_of s'); S \<subseteq> capRange (cteCap cte); ctes_of s' p = Some cte; isUntypedCap (cteCap cte); valid_objs' s'; valid_mdb' s'; valid_pspace' s'; sch_act_wf (ksSchedulerAction s') s'; Invariants_H.valid_queues s'; sym_refs (state_refs_of' s'); if_live_then_nonz_cap' s'; if_unsafe_then_cap' s'; valid_idle' s'; valid_global_refs' s'; valid_arch_state' s'; valid_irq_node' (irq_node' s') s'; valid_irq_handlers' s'; valid_irq_states' s'; valid_machine_state' s'; irqs_masked' s'; valid_queues' s'; ct_not_inQ s'; ct_idle_or_in_cur_domain' s'; valid_pde_mappings' s'; pspace_domain_valid s'; ksCurDomain s' \<le> maxDomain; ksDomSchedule (KernelInit_H.newKernelState undefined) \<noteq> []; \<forall>x\<in>set (ksDomSchedule (KernelInit_H.newKernelState undefined)). dschDomain x \<le> maxDomain \<and> 0 < dschLength x; ksDomSchedule s' = ksDomSchedule (KernelInit_H.newKernelState undefined); ksDomScheduleIdx s' < length (ksDomSchedule (KernelInit_H.newKernelState undefined)); untyped_ranges_zero' s'; cur_tcb' s'; ctes_of s' cref = Some ctea; P (capability.IRQHandlerCap irq); q = irq_node' s' + UCAST(10 \<rightarrow> 32) irq * 0x10; cteCap ctea = capability.IRQHandlerCap irq; kernel_data_refs \<inter> capRange (cteCap cte) = {}; global_refs' s' \<subseteq> kernel_data_refs\<rbrakk> \<Longrightarrow> S \<subseteq> capRange (cteCap cte)
 3. \<And>cref ctea. \<lbrakk>descendants_range_in' S p (ctes_of s'); S \<subseteq> capRange (cteCap cte); ctes_of s' p = Some cte; isUntypedCap (cteCap cte); valid_objs' s'; valid_mdb' s'; valid_pspace' s'; sch_act_wf (ksSchedulerAction s') s'; Invariants_H.valid_queues s'; sym_refs (state_refs_of' s'); if_live_then_nonz_cap' s'; if_unsafe_then_cap' s'; valid_idle' s'; valid_global_refs' s'; valid_arch_state' s'; valid_irq_node' (irq_node' s') s'; valid_irq_handlers' s'; valid_irq_states' s'; valid_machine_state' s'; irqs_masked' s'; valid_queues' s'; ct_not_inQ s'; ct_idle_or_in_cur_domain' s'; valid_pde_mappings' s'; pspace_domain_valid s'; ksCurDomain s' \<le> maxDomain; ksDomSchedule (KernelInit_H.newKernelState undefined) \<noteq> []; \<forall>x\<in>set (ksDomSchedule (KernelInit_H.newKernelState undefined)). dschDomain x \<le> maxDomain \<and> 0 < dschLength x; ksDomSchedule s' = ksDomSchedule (KernelInit_H.newKernelState undefined); ksDomScheduleIdx s' < length (ksDomSchedule (KernelInit_H.newKernelState undefined)); untyped_ranges_zero' s'; cur_tcb' s'; q \<in> S; ctes_of s' cref = Some ctea; P (cteCap ctea); q \<in> cte_refs' (cteCap ctea) (irq_node' s'); kernel_data_refs \<inter> capRange (cteCap cte) = {} \<and> global_refs' s' \<subseteq> kernel_data_refs; \<nexists>irq. cteCap ctea = capability.IRQHandlerCap irq\<rbrakk> \<Longrightarrow> False proof (prove)
goal (3 subgoals):
 1. \<And>cref ctea irq. \<lbrakk>descendants_range_in' S p (ctes_of s'); S \<subseteq> capRange (cteCap cte); ctes_of s' p = Some cte; isUntypedCap (cteCap cte); valid_objs' s'; valid_mdb' s'; valid_pspace' s'; sch_act_wf (ksSchedulerAction s') s'; Invariants_H.valid_queues s'; sym_refs (state_refs_of' s'); if_live_then_nonz_cap' s'; if_unsafe_then_cap' s'; valid_idle' s'; valid_global_refs' s'; valid_arch_state' s'; valid_irq_node' (irq_node' s') s'; valid_irq_handlers' s'; valid_irq_states' s'; valid_machine_state' s'; irqs_masked' s'; valid_queues' s'; ct_not_inQ s'; ct_idle_or_in_cur_domain' s'; valid_pde_mappings' s'; pspace_domain_valid s'; ksCurDomain s' \<le> maxDomain; ksDomSchedule (KernelInit_H.newKernelState undefined) \<noteq> []; \<forall>x\<in>set (ksDomSchedule (KernelInit_H.newKernelState undefined)). dschDomain x \<le> maxDomain \<and> 0 < dschLength x; ksDomSchedule s' = ksDomSchedule (KernelInit_H.newKernelState undefined); ksDomScheduleIdx s' < length (ksDomSchedule (KernelInit_H.newKernelState undefined)); untyped_ranges_zero' s'; cur_tcb' s'; ctes_of s' cref = Some ctea; P (capability.IRQHandlerCap irq); q = irq_node' s' + UCAST(10 \<rightarrow> 32) irq * 0x10; cteCap ctea = capability.IRQHandlerCap irq; kernel_data_refs \<inter> capRange (cteCap cte) = {}; ksIdleThread s' \<in> kernel_data_refs; page_directory_refs' (armKSGlobalPD (ksArchState s')) \<subseteq> kernel_data_refs; \<Union> (page_table_refs' ` set (armKSGlobalPTs (ksArchState s'))) \<subseteq> kernel_data_refs\<rbrakk> \<Longrightarrow> irq_node' s' + UCAST(10 \<rightarrow> 32) irq * 0x10 \<in> range (\<lambda>x. irq_node' s' + 0x10 * UCAST(10 \<rightarrow> 32) x)
 2. \<And>cref ctea irq. \<lbrakk>descendants_range_in' S p (ctes_of s'); S \<subseteq> capRange (cteCap cte); ctes_of s' p = Some cte; isUntypedCap (cteCap cte); valid_objs' s'; valid_mdb' s'; valid_pspace' s'; sch_act_wf (ksSchedulerAction s') s'; Invariants_H.valid_queues s'; sym_refs (state_refs_of' s'); if_live_then_nonz_cap' s'; if_unsafe_then_cap' s'; valid_idle' s'; valid_global_refs' s'; valid_arch_state' s'; valid_irq_node' (irq_node' s') s'; valid_irq_handlers' s'; valid_irq_states' s'; valid_machine_state' s'; irqs_masked' s'; valid_queues' s'; ct_not_inQ s'; ct_idle_or_in_cur_domain' s'; valid_pde_mappings' s'; pspace_domain_valid s'; ksCurDomain s' \<le> maxDomain; ksDomSchedule (KernelInit_H.newKernelState undefined) \<noteq> []; \<forall>x\<in>set (ksDomSchedule (KernelInit_H.newKernelState undefined)). dschDomain x \<le> maxDomain \<and> 0 < dschLength x; ksDomSchedule s' = ksDomSchedule (KernelInit_H.newKernelState undefined); ksDomScheduleIdx s' < length (ksDomSchedule (KernelInit_H.newKernelState undefined)); untyped_ranges_zero' s'; cur_tcb' s'; ctes_of s' cref = Some ctea; P (capability.IRQHandlerCap irq); q = irq_node' s' + UCAST(10 \<rightarrow> 32) irq * 0x10; cteCap ctea = capability.IRQHandlerCap irq; kernel_data_refs \<inter> capRange (cteCap cte) = {}; global_refs' s' \<subseteq> kernel_data_refs\<rbrakk> \<Longrightarrow> S \<subseteq> capRange (cteCap cte)
 3. \<And>cref ctea. \<lbrakk>descendants_range_in' S p (ctes_of s'); S \<subseteq> capRange (cteCap cte); ctes_of s' p = Some cte; isUntypedCap (cteCap cte); valid_objs' s'; valid_mdb' s'; valid_pspace' s'; sch_act_wf (ksSchedulerAction s') s'; Invariants_H.valid_queues s'; sym_refs (state_refs_of' s'); if_live_then_nonz_cap' s'; if_unsafe_then_cap' s'; valid_idle' s'; valid_global_refs' s'; valid_arch_state' s'; valid_irq_node' (irq_node' s') s'; valid_irq_handlers' s'; valid_irq_states' s'; valid_machine_state' s'; irqs_masked' s'; valid_queues' s'; ct_not_inQ s'; ct_idle_or_in_cur_domain' s'; valid_pde_mappings' s'; pspace_domain_valid s'; ksCurDomain s' \<le> maxDomain; ksDomSchedule (KernelInit_H.newKernelState undefined) \<noteq> []; \<forall>x\<in>set (ksDomSchedule (KernelInit_H.newKernelState undefined)). dschDomain x \<le> maxDomain \<and> 0 < dschLength x; ksDomSchedule s' = ksDomSchedule (KernelInit_H.newKernelState undefined); ksDomScheduleIdx s' < length (ksDomSchedule (KernelInit_H.newKernelState undefined)); untyped_ranges_zero' s'; cur_tcb' s'; q \<in> S; ctes_of s' cref = Some ctea; P (cteCap ctea); q \<in> cte_refs' (cteCap ctea) (irq_node' s'); kernel_data_refs \<inter> capRange (cteCap cte) = {} \<and> global_refs' s' \<subseteq> kernel_data_refs; \<nexists>irq. cteCap ctea = capability.IRQHandlerCap irq\<rbrakk> \<Longrightarrow> False proof (prove)
goal (2 subgoals):
 1. \<And>cref ctea irq. \<lbrakk>descendants_range_in' S p (ctes_of s'); S \<subseteq> capRange (cteCap cte); ctes_of s' p = Some cte; isUntypedCap (cteCap cte); valid_objs' s'; valid_mdb' s'; valid_pspace' s'; sch_act_wf (ksSchedulerAction s') s'; Invariants_H.valid_queues s'; sym_refs (state_refs_of' s'); if_live_then_nonz_cap' s'; if_unsafe_then_cap' s'; valid_idle' s'; valid_global_refs' s'; valid_arch_state' s'; valid_irq_node' (irq_node' s') s'; valid_irq_handlers' s'; valid_irq_states' s'; valid_machine_state' s'; irqs_masked' s'; valid_queues' s'; ct_not_inQ s'; ct_idle_or_in_cur_domain' s'; valid_pde_mappings' s'; pspace_domain_valid s'; ksCurDomain s' \<le> maxDomain; ksDomSchedule (KernelInit_H.newKernelState undefined) \<noteq> []; \<forall>x\<in>set (ksDomSchedule (KernelInit_H.newKernelState undefined)). dschDomain x \<le> maxDomain \<and> 0 < dschLength x; ksDomSchedule s' = ksDomSchedule (KernelInit_H.newKernelState undefined); ksDomScheduleIdx s' < length (ksDomSchedule (KernelInit_H.newKernelState undefined)); untyped_ranges_zero' s'; cur_tcb' s'; ctes_of s' cref = Some ctea; P (capability.IRQHandlerCap irq); q = irq_node' s' + UCAST(10 \<rightarrow> 32) irq * 0x10; cteCap ctea = capability.IRQHandlerCap irq; kernel_data_refs \<inter> capRange (cteCap cte) = {}; global_refs' s' \<subseteq> kernel_data_refs\<rbrakk> \<Longrightarrow> S \<subseteq> capRange (cteCap cte)
 2. \<And>cref ctea. \<lbrakk>descendants_range_in' S p (ctes_of s'); S \<subseteq> capRange (cteCap cte); ctes_of s' p = Some cte; isUntypedCap (cteCap cte); valid_objs' s'; valid_mdb' s'; valid_pspace' s'; sch_act_wf (ksSchedulerAction s') s'; Invariants_H.valid_queues s'; sym_refs (state_refs_of' s'); if_live_then_nonz_cap' s'; if_unsafe_then_cap' s'; valid_idle' s'; valid_global_refs' s'; valid_arch_state' s'; valid_irq_node' (irq_node' s') s'; valid_irq_handlers' s'; valid_irq_states' s'; valid_machine_state' s'; irqs_masked' s'; valid_queues' s'; ct_not_inQ s'; ct_idle_or_in_cur_domain' s'; valid_pde_mappings' s'; pspace_domain_valid s'; ksCurDomain s' \<le> maxDomain; ksDomSchedule (KernelInit_H.newKernelState undefined) \<noteq> []; \<forall>x\<in>set (ksDomSchedule (KernelInit_H.newKernelState undefined)). dschDomain x \<le> maxDomain \<and> 0 < dschLength x; ksDomSchedule s' = ksDomSchedule (KernelInit_H.newKernelState undefined); ksDomScheduleIdx s' < length (ksDomSchedule (KernelInit_H.newKernelState undefined)); untyped_ranges_zero' s'; cur_tcb' s'; q \<in> S; ctes_of s' cref = Some ctea; P (cteCap ctea); q \<in> cte_refs' (cteCap ctea) (irq_node' s'); kernel_data_refs \<inter> capRange (cteCap cte) = {} \<and> global_refs' s' \<subseteq> kernel_data_refs; \<nexists>irq. cteCap ctea = capability.IRQHandlerCap irq\<rbrakk> \<Longrightarrow> False proof (prove)
goal (2 subgoals):
 1. \<And>cref ctea irq x1 x2. \<lbrakk>descendants_range_in' S p (ctes_of s'); S \<subseteq> capRange (cteCap cte); ctes_of s' p = Some cte; isUntypedCap (cteCap cte); valid_objs' s'; valid_mdb' s'; valid_pspace' s'; sch_act_wf (ksSchedulerAction s') s'; Invariants_H.valid_queues s'; sym_refs (state_refs_of' s'); if_live_then_nonz_cap' s'; if_unsafe_then_cap' s'; valid_idle' s'; valid_global_refs' s'; valid_arch_state' s'; valid_irq_node' (irq_node' s') s'; valid_irq_handlers' s'; valid_irq_states' s'; valid_machine_state' s'; irqs_masked' s'; valid_queues' s'; ct_not_inQ s'; ct_idle_or_in_cur_domain' s'; valid_pde_mappings' s'; pspace_domain_valid s'; ksCurDomain s' \<le> maxDomain; ksDomSchedule (KernelInit_H.newKernelState undefined) \<noteq> []; \<forall>x\<in>set (ksDomSchedule (KernelInit_H.newKernelState undefined)). dschDomain x \<le> maxDomain \<and> 0 < dschLength x; ksDomSchedule s' = ksDomSchedule (KernelInit_H.newKernelState undefined); ksDomScheduleIdx s' < length (ksDomSchedule (KernelInit_H.newKernelState undefined)); untyped_ranges_zero' s'; cur_tcb' s'; ctes_of s' cref = Some ctea; P (capability.IRQHandlerCap irq); q = irq_node' s' + UCAST(10 \<rightarrow> 32) irq * 0x10; cteCap ctea = capability.IRQHandlerCap irq; kernel_data_refs \<inter> capRange (cteCap cte) = {}; global_refs' s' \<subseteq> kernel_data_refs; ctea = CTE x1 x2\<rbrakk> \<Longrightarrow> S \<subseteq> capRange (cteCap cte)
 2. \<And>cref ctea. \<lbrakk>descendants_range_in' S p (ctes_of s'); S \<subseteq> capRange (cteCap cte); ctes_of s' p = Some cte; isUntypedCap (cteCap cte); valid_objs' s'; valid_mdb' s'; valid_pspace' s'; sch_act_wf (ksSchedulerAction s') s'; Invariants_H.valid_queues s'; sym_refs (state_refs_of' s'); if_live_then_nonz_cap' s'; if_unsafe_then_cap' s'; valid_idle' s'; valid_global_refs' s'; valid_arch_state' s'; valid_irq_node' (irq_node' s') s'; valid_irq_handlers' s'; valid_irq_states' s'; valid_machine_state' s'; irqs_masked' s'; valid_queues' s'; ct_not_inQ s'; ct_idle_or_in_cur_domain' s'; valid_pde_mappings' s'; pspace_domain_valid s'; ksCurDomain s' \<le> maxDomain; ksDomSchedule (KernelInit_H.newKernelState undefined) \<noteq> []; \<forall>x\<in>set (ksDomSchedule (KernelInit_H.newKernelState undefined)). dschDomain x \<le> maxDomain \<and> 0 < dschLength x; ksDomSchedule s' = ksDomSchedule (KernelInit_H.newKernelState undefined); ksDomScheduleIdx s' < length (ksDomSchedule (KernelInit_H.newKernelState undefined)); untyped_ranges_zero' s'; cur_tcb' s'; q \<in> S; ctes_of s' cref = Some ctea; P (cteCap ctea); q \<in> cte_refs' (cteCap ctea) (irq_node' s'); kernel_data_refs \<inter> capRange (cteCap cte) = {} \<and> global_refs' s' \<subseteq> kernel_data_refs; \<nexists>irq. cteCap ctea = capability.IRQHandlerCap irq\<rbrakk> \<Longrightarrow> False proof (prove)
goal (1 subgoal):
 1. \<And>cref ctea. \<lbrakk>descendants_range_in' S p (ctes_of s'); S \<subseteq> capRange (cteCap cte); ctes_of s' p = Some cte; isUntypedCap (cteCap cte); valid_objs' s'; valid_mdb' s'; valid_pspace' s'; sch_act_wf (ksSchedulerAction s') s'; Invariants_H.valid_queues s'; sym_refs (state_refs_of' s'); if_live_then_nonz_cap' s'; if_unsafe_then_cap' s'; valid_idle' s'; valid_global_refs' s'; valid_arch_state' s'; valid_irq_node' (irq_node' s') s'; valid_irq_handlers' s'; valid_irq_states' s'; valid_machine_state' s'; irqs_masked' s'; valid_queues' s'; ct_not_inQ s'; ct_idle_or_in_cur_domain' s'; valid_pde_mappings' s'; pspace_domain_valid s'; ksCurDomain s' \<le> maxDomain; ksDomSchedule (KernelInit_H.newKernelState undefined) \<noteq> []; \<forall>x\<in>set (ksDomSchedule (KernelInit_H.newKernelState undefined)). dschDomain x \<le> maxDomain \<and> 0 < dschLength x; ksDomSchedule s' = ksDomSchedule (KernelInit_H.newKernelState undefined); ksDomScheduleIdx s' < length (ksDomSchedule (KernelInit_H.newKernelState undefined)); untyped_ranges_zero' s'; cur_tcb' s'; q \<in> S; ctes_of s' cref = Some ctea; P (cteCap ctea); q \<in> cte_refs' (cteCap ctea) (irq_node' s'); kernel_data_refs \<inter> capRange (cteCap cte) = {} \<and> global_refs' s' \<subseteq> kernel_data_refs; \<nexists>irq. cteCap ctea = capability.IRQHandlerCap irq\<rbrakk> \<Longrightarrow> False proof (prove)
goal (1 subgoal):
 1. \<And>cref ctea x1 x2. \<lbrakk>descendants_range_in' S p (ctes_of s'); S \<subseteq> capRange (cteCap cte); ctes_of s' p = Some cte; isUntypedCap (cteCap cte); valid_objs' s'; valid_mdb' s'; valid_pspace' s'; sch_act_wf (ksSchedulerAction s') s'; Invariants_H.valid_queues s'; sym_refs (state_refs_of' s'); if_live_then_nonz_cap' s'; if_unsafe_then_cap' s'; valid_idle' s'; valid_global_refs' s'; valid_arch_state' s'; valid_irq_node' (irq_node' s') s'; valid_irq_handlers' s'; valid_irq_states' s'; valid_machine_state' s'; irqs_masked' s'; valid_queues' s'; ct_not_inQ s'; ct_idle_or_in_cur_domain' s'; valid_pde_mappings' s'; pspace_domain_valid s'; ksCurDomain s' \<le> maxDomain; ksDomSchedule (KernelInit_H.newKernelState undefined) \<noteq> []; \<forall>x\<in>set (ksDomSchedule (KernelInit_H.newKernelState undefined)). dschDomain x \<le> maxDomain \<and> 0 < dschLength x; ksDomSchedule s' = ksDomSchedule (KernelInit_H.newKernelState undefined); ksDomScheduleIdx s' < length (ksDomSchedule (KernelInit_H.newKernelState undefined)); untyped_ranges_zero' s'; cur_tcb' s'; q \<in> S; ctes_of s' cref = Some ctea; P (cteCap ctea); q \<in> cte_refs' (cteCap ctea) (irq_node' s'); kernel_data_refs \<inter> capRange (cteCap cte) = {} \<and> global_refs' s' \<subseteq> kernel_data_refs; \<nexists>irq. cteCap ctea = capability.IRQHandlerCap irq; ctea = CTE x1 x2\<rbrakk> \<Longrightarrow> False proof (prove)
goal (6 subgoals):
 1. \<And>cref ctea x1 x2. \<lbrakk>descendants_range_in' S p (ctes_of s'); S \<subseteq> capRange (cteCap cte); isUntypedCap (cteCap cte); valid_objs' s'; valid_mdb' s'; valid_pspace' s'; sch_act_wf (ksSchedulerAction s') s'; Invariants_H.valid_queues s'; sym_refs (state_refs_of' s'); if_live_then_nonz_cap' s'; if_unsafe_then_cap' s'; valid_idle' s'; valid_global_refs' s'; valid_arch_state' s'; valid_irq_node' (irq_node' s') s'; valid_irq_handlers' s'; valid_irq_states' s'; valid_machine_state' s'; irqs_masked' s'; valid_queues' s'; ct_not_inQ s'; ct_idle_or_in_cur_domain' s'; valid_pde_mappings' s'; pspace_domain_valid s'; ksCurDomain s' \<le> maxDomain; ksDomSchedule (KernelInit_H.newKernelState undefined) \<noteq> []; \<forall>x\<in>set (ksDomSchedule (KernelInit_H.newKernelState undefined)). dschDomain x \<le> maxDomain \<and> 0 < dschLength x; ksDomSchedule s' = ksDomSchedule (KernelInit_H.newKernelState undefined); ksDomScheduleIdx s' < length (ksDomSchedule (KernelInit_H.newKernelState undefined)); untyped_ranges_zero' s'; cur_tcb' s'; q \<in> S; ctes_of s' cref = Some ctea; P (cteCap ctea); q \<in> cte_refs' (cteCap ctea) (irq_node' s'); kernel_data_refs \<inter> capRange (cteCap cte) = {} \<and> global_refs' s' \<subseteq> kernel_data_refs; \<nexists>irq. cteCap ctea = capability.IRQHandlerCap irq; ctea = CTE x1 x2\<rbrakk> \<Longrightarrow> ctes_of s' (?p'60 cref ctea x1 x2) = Some ctea
 2. \<And>cref ctea x1 x2. \<lbrakk>descendants_range_in' S p (ctes_of s'); S \<subseteq> capRange (cteCap cte); isUntypedCap (cteCap cte); valid_objs' s'; valid_mdb' s'; valid_pspace' s'; sch_act_wf (ksSchedulerAction s') s'; Invariants_H.valid_queues s'; sym_refs (state_refs_of' s'); if_live_then_nonz_cap' s'; if_unsafe_then_cap' s'; valid_idle' s'; valid_global_refs' s'; valid_arch_state' s'; valid_irq_node' (irq_node' s') s'; valid_irq_handlers' s'; valid_irq_states' s'; valid_machine_state' s'; irqs_masked' s'; valid_queues' s'; ct_not_inQ s'; ct_idle_or_in_cur_domain' s'; valid_pde_mappings' s'; pspace_domain_valid s'; ksCurDomain s' \<le> maxDomain; ksDomSchedule (KernelInit_H.newKernelState undefined) \<noteq> []; \<forall>x\<in>set (ksDomSchedule (KernelInit_H.newKernelState undefined)). dschDomain x \<le> maxDomain \<and> 0 < dschLength x; ksDomSchedule s' = ksDomSchedule (KernelInit_H.newKernelState undefined); ksDomScheduleIdx s' < length (ksDomSchedule (KernelInit_H.newKernelState undefined)); untyped_ranges_zero' s'; cur_tcb' s'; q \<in> S; ctes_of s' cref = Some ctea; P (cteCap ctea); q \<in> cte_refs' (cteCap ctea) (irq_node' s'); kernel_data_refs \<inter> capRange (cteCap cte) = {} \<and> global_refs' s' \<subseteq> kernel_data_refs; \<nexists>irq. cteCap ctea = capability.IRQHandlerCap irq; ctea = CTE x1 x2\<rbrakk> \<Longrightarrow> isUntypedCap (cteCap cte)
 3. \<And>cref ctea x1 x2. \<lbrakk>descendants_range_in' S p (ctes_of s'); S \<subseteq> capRange (cteCap cte); isUntypedCap (cteCap cte); valid_objs' s'; valid_mdb' s'; valid_pspace' s'; sch_act_wf (ksSchedulerAction s') s'; Invariants_H.valid_queues s'; sym_refs (state_refs_of' s'); if_live_then_nonz_cap' s'; if_unsafe_then_cap' s'; valid_idle' s'; valid_global_refs' s'; valid_arch_state' s'; valid_irq_node' (irq_node' s') s'; valid_irq_handlers' s'; valid_irq_states' s'; valid_machine_state' s'; irqs_masked' s'; valid_queues' s'; ct_not_inQ s'; ct_idle_or_in_cur_domain' s'; valid_pde_mappings' s'; pspace_domain_valid s'; ksCurDomain s' \<le> maxDomain; ksDomSchedule (KernelInit_H.newKernelState undefined) \<noteq> []; \<forall>x\<in>set (ksDomSchedule (KernelInit_H.newKernelState undefined)). dschDomain x \<le> maxDomain \<and> 0 < dschLength x; ksDomSchedule s' = ksDomSchedule (KernelInit_H.newKernelState undefined); ksDomScheduleIdx s' < length (ksDomSchedule (KernelInit_H.newKernelState undefined)); untyped_ranges_zero' s'; cur_tcb' s'; q \<in> S; ctes_of s' cref = Some ctea; P (cteCap ctea); q \<in> cte_refs' (cteCap ctea) (irq_node' s'); kernel_data_refs \<inter> capRange (cteCap cte) = {} \<and> global_refs' s' \<subseteq> kernel_data_refs; \<nexists>irq. cteCap ctea = capability.IRQHandlerCap irq; ctea = CTE x1 x2\<rbrakk> \<Longrightarrow> capRange (cteCap ctea) \<inter> untypedRange (cteCap cte) \<noteq> {}
 4. \<And>cref ctea x1 x2. \<lbrakk>descendants_range_in' S p (ctes_of s'); S \<subseteq> capRange (cteCap cte); isUntypedCap (cteCap cte); valid_objs' s'; valid_mdb' s'; valid_pspace' s'; sch_act_wf (ksSchedulerAction s') s'; Invariants_H.valid_queues s'; sym_refs (state_refs_of' s'); if_live_then_nonz_cap' s'; if_unsafe_then_cap' s'; valid_idle' s'; valid_global_refs' s'; valid_arch_state' s'; valid_irq_node' (irq_node' s') s'; valid_irq_handlers' s'; valid_irq_states' s'; valid_machine_state' s'; irqs_masked' s'; valid_queues' s'; ct_not_inQ s'; ct_idle_or_in_cur_domain' s'; valid_pde_mappings' s'; pspace_domain_valid s'; ksCurDomain s' \<le> maxDomain; ksDomSchedule (KernelInit_H.newKernelState undefined) \<noteq> []; \<forall>x\<in>set (ksDomSchedule (KernelInit_H.newKernelState undefined)). dschDomain x \<le> maxDomain \<and> 0 < dschLength x; ksDomSchedule s' = ksDomSchedule (KernelInit_H.newKernelState undefined); ksDomScheduleIdx s' < length (ksDomSchedule (KernelInit_H.newKernelState undefined)); untyped_ranges_zero' s'; cur_tcb' s'; q \<in> S; ctes_of s' cref = Some ctea; P (cteCap ctea); q \<in> cte_refs' (cteCap ctea) (irq_node' s'); kernel_data_refs \<inter> capRange (cteCap cte) = {} \<and> global_refs' s' \<subseteq> kernel_data_refs; \<nexists>irq. cteCap ctea = capability.IRQHandlerCap irq; ctea = CTE x1 x2\<rbrakk> \<Longrightarrow> \<not> isUntypedCap (cteCap ctea)
 5. \<And>cref ctea x1 x2. \<lbrakk>descendants_range_in' S p (ctes_of s'); S \<subseteq> capRange (cteCap cte); isUntypedCap (cteCap cte); valid_objs' s'; valid_mdb' s'; valid_pspace' s'; sch_act_wf (ksSchedulerAction s') s'; Invariants_H.valid_queues s'; sym_refs (state_refs_of' s'); if_live_then_nonz_cap' s'; if_unsafe_then_cap' s'; valid_idle' s'; valid_global_refs' s'; valid_arch_state' s'; valid_irq_node' (irq_node' s') s'; valid_irq_handlers' s'; valid_irq_states' s'; valid_machine_state' s'; irqs_masked' s'; valid_queues' s'; ct_not_inQ s'; ct_idle_or_in_cur_domain' s'; valid_pde_mappings' s'; pspace_domain_valid s'; ksCurDomain s' \<le> maxDomain; ksDomSchedule (KernelInit_H.newKernelState undefined) \<noteq> []; \<forall>x\<in>set (ksDomSchedule (KernelInit_H.newKernelState undefined)). dschDomain x \<le> maxDomain \<and> 0 < dschLength x; ksDomSchedule s' = ksDomSchedule (KernelInit_H.newKernelState undefined); ksDomScheduleIdx s' < length (ksDomSchedule (KernelInit_H.newKernelState undefined)); untyped_ranges_zero' s'; cur_tcb' s'; q \<in> S; ctes_of s' cref = Some ctea; P (cteCap ctea); q \<in> cte_refs' (cteCap ctea) (irq_node' s'); kernel_data_refs \<inter> capRange (cteCap cte) = {} \<and> global_refs' s' \<subseteq> kernel_data_refs; \<nexists>irq. cteCap ctea = capability.IRQHandlerCap irq; ctea = CTE x1 x2\<rbrakk> \<Longrightarrow> untyped_mdb' (ctes_of s')
 6. \<And>cref ctea x1 x2. \<lbrakk>descendants_range_in' S p (ctes_of s'); S \<subseteq> capRange (cteCap cte); isUntypedCap (cteCap cte); valid_objs' s'; valid_mdb' s'; valid_pspace' s'; sch_act_wf (ksSchedulerAction s') s'; Invariants_H.valid_queues s'; sym_refs (state_refs_of' s'); if_live_then_nonz_cap' s'; if_unsafe_then_cap' s'; valid_idle' s'; valid_global_refs' s'; valid_arch_state' s'; valid_irq_node' (irq_node' s') s'; valid_irq_handlers' s'; valid_irq_states' s'; valid_machine_state' s'; irqs_masked' s'; valid_queues' s'; ct_not_inQ s'; ct_idle_or_in_cur_domain' s'; valid_pde_mappings' s'; pspace_domain_valid s'; ksCurDomain s' \<le> maxDomain; ksDomSchedule (KernelInit_H.newKernelState undefined) \<noteq> []; \<forall>x\<in>set (ksDomSchedule (KernelInit_H.newKernelState undefined)). dschDomain x \<le> maxDomain \<and> 0 < dschLength x; ksDomSchedule s' = ksDomSchedule (KernelInit_H.newKernelState undefined); ksDomScheduleIdx s' < length (ksDomSchedule (KernelInit_H.newKernelState undefined)); untyped_ranges_zero' s'; cur_tcb' s'; q \<in> S; ctes_of s' cref = Some ctea; P (cteCap ctea); q \<in> cte_refs' (cteCap ctea) (irq_node' s'); kernel_data_refs \<inter> capRange (cteCap cte) = {} \<and> global_refs' s' \<subseteq> kernel_data_refs; \<nexists>irq. cteCap ctea = capability.IRQHandlerCap irq; ctea = CTE x1 x2; ?p'60 cref ctea x1 x2 \<in> descendants_of' p (ctes_of s')\<rbrakk> \<Longrightarrow> False proof (prove)
goal (5 subgoals):
 1. \<And>cref ctea x1 x2. \<lbrakk>descendants_range_in' S p (ctes_of s'); S \<subseteq> capRange (cteCap cte); isUntypedCap (cteCap cte); valid_objs' s'; valid_mdb' s'; valid_pspace' s'; sch_act_wf (ksSchedulerAction s') s'; Invariants_H.valid_queues s'; sym_refs (state_refs_of' s'); if_live_then_nonz_cap' s'; if_unsafe_then_cap' s'; valid_idle' s'; valid_global_refs' s'; valid_arch_state' s'; valid_irq_node' (irq_node' s') s'; valid_irq_handlers' s'; valid_irq_states' s'; valid_machine_state' s'; irqs_masked' s'; valid_queues' s'; ct_not_inQ s'; ct_idle_or_in_cur_domain' s'; valid_pde_mappings' s'; pspace_domain_valid s'; ksCurDomain s' \<le> maxDomain; ksDomSchedule (KernelInit_H.newKernelState undefined) \<noteq> []; \<forall>x\<in>set (ksDomSchedule (KernelInit_H.newKernelState undefined)). dschDomain x \<le> maxDomain \<and> 0 < dschLength x; ksDomSchedule s' = ksDomSchedule (KernelInit_H.newKernelState undefined); ksDomScheduleIdx s' < length (ksDomSchedule (KernelInit_H.newKernelState undefined)); untyped_ranges_zero' s'; cur_tcb' s'; q \<in> S; ctes_of s' cref = Some ctea; P (cteCap ctea); q \<in> cte_refs' (cteCap ctea) (irq_node' s'); kernel_data_refs \<inter> capRange (cteCap cte) = {} \<and> global_refs' s' \<subseteq> kernel_data_refs; \<nexists>irq. cteCap ctea = capability.IRQHandlerCap irq; ctea = CTE x1 x2\<rbrakk> \<Longrightarrow> isUntypedCap (cteCap cte)
 2. \<And>cref ctea x1 x2. \<lbrakk>descendants_range_in' S p (ctes_of s'); S \<subseteq> capRange (cteCap cte); isUntypedCap (cteCap cte); valid_objs' s'; valid_mdb' s'; valid_pspace' s'; sch_act_wf (ksSchedulerAction s') s'; Invariants_H.valid_queues s'; sym_refs (state_refs_of' s'); if_live_then_nonz_cap' s'; if_unsafe_then_cap' s'; valid_idle' s'; valid_global_refs' s'; valid_arch_state' s'; valid_irq_node' (irq_node' s') s'; valid_irq_handlers' s'; valid_irq_states' s'; valid_machine_state' s'; irqs_masked' s'; valid_queues' s'; ct_not_inQ s'; ct_idle_or_in_cur_domain' s'; valid_pde_mappings' s'; pspace_domain_valid s'; ksCurDomain s' \<le> maxDomain; ksDomSchedule (KernelInit_H.newKernelState undefined) \<noteq> []; \<forall>x\<in>set (ksDomSchedule (KernelInit_H.newKernelState undefined)). dschDomain x \<le> maxDomain \<and> 0 < dschLength x; ksDomSchedule s' = ksDomSchedule (KernelInit_H.newKernelState undefined); ksDomScheduleIdx s' < length (ksDomSchedule (KernelInit_H.newKernelState undefined)); untyped_ranges_zero' s'; cur_tcb' s'; q \<in> S; ctes_of s' cref = Some ctea; P (cteCap ctea); q \<in> cte_refs' (cteCap ctea) (irq_node' s'); kernel_data_refs \<inter> capRange (cteCap cte) = {} \<and> global_refs' s' \<subseteq> kernel_data_refs; \<nexists>irq. cteCap ctea = capability.IRQHandlerCap irq; ctea = CTE x1 x2\<rbrakk> \<Longrightarrow> capRange (cteCap ctea) \<inter> untypedRange (cteCap cte) \<noteq> {}
 3. \<And>cref ctea x1 x2. \<lbrakk>descendants_range_in' S p (ctes_of s'); S \<subseteq> capRange (cteCap cte); isUntypedCap (cteCap cte); valid_objs' s'; valid_mdb' s'; valid_pspace' s'; sch_act_wf (ksSchedulerAction s') s'; Invariants_H.valid_queues s'; sym_refs (state_refs_of' s'); if_live_then_nonz_cap' s'; if_unsafe_then_cap' s'; valid_idle' s'; valid_global_refs' s'; valid_arch_state' s'; valid_irq_node' (irq_node' s') s'; valid_irq_handlers' s'; valid_irq_states' s'; valid_machine_state' s'; irqs_masked' s'; valid_queues' s'; ct_not_inQ s'; ct_idle_or_in_cur_domain' s'; valid_pde_mappings' s'; pspace_domain_valid s'; ksCurDomain s' \<le> maxDomain; ksDomSchedule (KernelInit_H.newKernelState undefined) \<noteq> []; \<forall>x\<in>set (ksDomSchedule (KernelInit_H.newKernelState undefined)). dschDomain x \<le> maxDomain \<and> 0 < dschLength x; ksDomSchedule s' = ksDomSchedule (KernelInit_H.newKernelState undefined); ksDomScheduleIdx s' < length (ksDomSchedule (KernelInit_H.newKernelState undefined)); untyped_ranges_zero' s'; cur_tcb' s'; q \<in> S; ctes_of s' cref = Some ctea; P (cteCap ctea); q \<in> cte_refs' (cteCap ctea) (irq_node' s'); kernel_data_refs \<inter> capRange (cteCap cte) = {} \<and> global_refs' s' \<subseteq> kernel_data_refs; \<nexists>irq. cteCap ctea = capability.IRQHandlerCap irq; ctea = CTE x1 x2\<rbrakk> \<Longrightarrow> \<not> isUntypedCap (cteCap ctea)
 4. \<And>cref ctea x1 x2. \<lbrakk>descendants_range_in' S p (ctes_of s'); S \<subseteq> capRange (cteCap cte); isUntypedCap (cteCap cte); valid_objs' s'; valid_mdb' s'; valid_pspace' s'; sch_act_wf (ksSchedulerAction s') s'; Invariants_H.valid_queues s'; sym_refs (state_refs_of' s'); if_live_then_nonz_cap' s'; if_unsafe_then_cap' s'; valid_idle' s'; valid_global_refs' s'; valid_arch_state' s'; valid_irq_node' (irq_node' s') s'; valid_irq_handlers' s'; valid_irq_states' s'; valid_machine_state' s'; irqs_masked' s'; valid_queues' s'; ct_not_inQ s'; ct_idle_or_in_cur_domain' s'; valid_pde_mappings' s'; pspace_domain_valid s'; ksCurDomain s' \<le> maxDomain; ksDomSchedule (KernelInit_H.newKernelState undefined) \<noteq> []; \<forall>x\<in>set (ksDomSchedule (KernelInit_H.newKernelState undefined)). dschDomain x \<le> maxDomain \<and> 0 < dschLength x; ksDomSchedule s' = ksDomSchedule (KernelInit_H.newKernelState undefined); ksDomScheduleIdx s' < length (ksDomSchedule (KernelInit_H.newKernelState undefined)); untyped_ranges_zero' s'; cur_tcb' s'; q \<in> S; ctes_of s' cref = Some ctea; P (cteCap ctea); q \<in> cte_refs' (cteCap ctea) (irq_node' s'); kernel_data_refs \<inter> capRange (cteCap cte) = {} \<and> global_refs' s' \<subseteq> kernel_data_refs; \<nexists>irq. cteCap ctea = capability.IRQHandlerCap irq; ctea = CTE x1 x2\<rbrakk> \<Longrightarrow> untyped_mdb' (ctes_of s')
 5. \<And>cref ctea x1 x2. \<lbrakk>descendants_range_in' S p (ctes_of s'); S \<subseteq> capRange (cteCap cte); isUntypedCap (cteCap cte); valid_objs' s'; valid_mdb' s'; valid_pspace' s'; sch_act_wf (ksSchedulerAction s') s'; Invariants_H.valid_queues s'; sym_refs (state_refs_of' s'); if_live_then_nonz_cap' s'; if_unsafe_then_cap' s'; valid_idle' s'; valid_global_refs' s'; valid_arch_state' s'; valid_irq_node' (irq_node' s') s'; valid_irq_handlers' s'; valid_irq_states' s'; valid_machine_state' s'; irqs_masked' s'; valid_queues' s'; ct_not_inQ s'; ct_idle_or_in_cur_domain' s'; valid_pde_mappings' s'; pspace_domain_valid s'; ksCurDomain s' \<le> maxDomain; ksDomSchedule (KernelInit_H.newKernelState undefined) \<noteq> []; \<forall>x\<in>set (ksDomSchedule (KernelInit_H.newKernelState undefined)). dschDomain x \<le> maxDomain \<and> 0 < dschLength x; ksDomSchedule s' = ksDomSchedule (KernelInit_H.newKernelState undefined); ksDomScheduleIdx s' < length (ksDomSchedule (KernelInit_H.newKernelState undefined)); untyped_ranges_zero' s'; cur_tcb' s'; q \<in> S; ctes_of s' cref = Some ctea; P (cteCap ctea); q \<in> cte_refs' (cteCap ctea) (irq_node' s'); kernel_data_refs \<inter> capRange (cteCap cte) = {} \<and> global_refs' s' \<subseteq> kernel_data_refs; \<nexists>irq. cteCap ctea = capability.IRQHandlerCap irq; ctea = CTE x1 x2; cref \<in> descendants_of' p (ctes_of s')\<rbrakk> \<Longrightarrow> False proof (prove)
goal (4 subgoals):
 1. \<And>cref ctea x1 x2. \<lbrakk>descendants_range_in' S p (ctes_of s'); S \<subseteq> capRange (cteCap cte); isUntypedCap (cteCap cte); valid_objs' s'; valid_mdb' s'; valid_pspace' s'; sch_act_wf (ksSchedulerAction s') s'; Invariants_H.valid_queues s'; sym_refs (state_refs_of' s'); if_live_then_nonz_cap' s'; if_unsafe_then_cap' s'; valid_idle' s'; valid_global_refs' s'; valid_arch_state' s'; valid_irq_node' (irq_node' s') s'; valid_irq_handlers' s'; valid_irq_states' s'; valid_machine_state' s'; irqs_masked' s'; valid_queues' s'; ct_not_inQ s'; ct_idle_or_in_cur_domain' s'; valid_pde_mappings' s'; pspace_domain_valid s'; ksCurDomain s' \<le> maxDomain; ksDomSchedule (KernelInit_H.newKernelState undefined) \<noteq> []; \<forall>x\<in>set (ksDomSchedule (KernelInit_H.newKernelState undefined)). dschDomain x \<le> maxDomain \<and> 0 < dschLength x; ksDomSchedule s' = ksDomSchedule (KernelInit_H.newKernelState undefined); ksDomScheduleIdx s' < length (ksDomSchedule (KernelInit_H.newKernelState undefined)); untyped_ranges_zero' s'; cur_tcb' s'; q \<in> S; ctes_of s' cref = Some ctea; P (cteCap ctea); q \<in> cte_refs' (cteCap ctea) (irq_node' s'); kernel_data_refs \<inter> capRange (cteCap cte) = {} \<and> global_refs' s' \<subseteq> kernel_data_refs; \<nexists>irq. cteCap ctea = capability.IRQHandlerCap irq; ctea = CTE x1 x2\<rbrakk> \<Longrightarrow> capRange (cteCap ctea) \<inter> untypedRange (cteCap cte) \<noteq> {}
 2. \<And>cref ctea x1 x2. \<lbrakk>descendants_range_in' S p (ctes_of s'); S \<subseteq> capRange (cteCap cte); isUntypedCap (cteCap cte); valid_objs' s'; valid_mdb' s'; valid_pspace' s'; sch_act_wf (ksSchedulerAction s') s'; Invariants_H.valid_queues s'; sym_refs (state_refs_of' s'); if_live_then_nonz_cap' s'; if_unsafe_then_cap' s'; valid_idle' s'; valid_global_refs' s'; valid_arch_state' s'; valid_irq_node' (irq_node' s') s'; valid_irq_handlers' s'; valid_irq_states' s'; valid_machine_state' s'; irqs_masked' s'; valid_queues' s'; ct_not_inQ s'; ct_idle_or_in_cur_domain' s'; valid_pde_mappings' s'; pspace_domain_valid s'; ksCurDomain s' \<le> maxDomain; ksDomSchedule (KernelInit_H.newKernelState undefined) \<noteq> []; \<forall>x\<in>set (ksDomSchedule (KernelInit_H.newKernelState undefined)). dschDomain x \<le> maxDomain \<and> 0 < dschLength x; ksDomSchedule s' = ksDomSchedule (KernelInit_H.newKernelState undefined); ksDomScheduleIdx s' < length (ksDomSchedule (KernelInit_H.newKernelState undefined)); untyped_ranges_zero' s'; cur_tcb' s'; q \<in> S; ctes_of s' cref = Some ctea; P (cteCap ctea); q \<in> cte_refs' (cteCap ctea) (irq_node' s'); kernel_data_refs \<inter> capRange (cteCap cte) = {} \<and> global_refs' s' \<subseteq> kernel_data_refs; \<nexists>irq. cteCap ctea = capability.IRQHandlerCap irq; ctea = CTE x1 x2\<rbrakk> \<Longrightarrow> \<not> isUntypedCap (cteCap ctea)
 3. \<And>cref ctea x1 x2. \<lbrakk>descendants_range_in' S p (ctes_of s'); S \<subseteq> capRange (cteCap cte); isUntypedCap (cteCap cte); valid_objs' s'; valid_mdb' s'; valid_pspace' s'; sch_act_wf (ksSchedulerAction s') s'; Invariants_H.valid_queues s'; sym_refs (state_refs_of' s'); if_live_then_nonz_cap' s'; if_unsafe_then_cap' s'; valid_idle' s'; valid_global_refs' s'; valid_arch_state' s'; valid_irq_node' (irq_node' s') s'; valid_irq_handlers' s'; valid_irq_states' s'; valid_machine_state' s'; irqs_masked' s'; valid_queues' s'; ct_not_inQ s'; ct_idle_or_in_cur_domain' s'; valid_pde_mappings' s'; pspace_domain_valid s'; ksCurDomain s' \<le> maxDomain; ksDomSchedule (KernelInit_H.newKernelState undefined) \<noteq> []; \<forall>x\<in>set (ksDomSchedule (KernelInit_H.newKernelState undefined)). dschDomain x \<le> maxDomain \<and> 0 < dschLength x; ksDomSchedule s' = ksDomSchedule (KernelInit_H.newKernelState undefined); ksDomScheduleIdx s' < length (ksDomSchedule (KernelInit_H.newKernelState undefined)); untyped_ranges_zero' s'; cur_tcb' s'; q \<in> S; ctes_of s' cref = Some ctea; P (cteCap ctea); q \<in> cte_refs' (cteCap ctea) (irq_node' s'); kernel_data_refs \<inter> capRange (cteCap cte) = {} \<and> global_refs' s' \<subseteq> kernel_data_refs; \<nexists>irq. cteCap ctea = capability.IRQHandlerCap irq; ctea = CTE x1 x2\<rbrakk> \<Longrightarrow> untyped_mdb' (ctes_of s')
 4. \<And>cref ctea x1 x2. \<lbrakk>descendants_range_in' S p (ctes_of s'); S \<subseteq> capRange (cteCap cte); isUntypedCap (cteCap cte); valid_objs' s'; valid_mdb' s'; valid_pspace' s'; sch_act_wf (ksSchedulerAction s') s'; Invariants_H.valid_queues s'; sym_refs (state_refs_of' s'); if_live_then_nonz_cap' s'; if_unsafe_then_cap' s'; valid_idle' s'; valid_global_refs' s'; valid_arch_state' s'; valid_irq_node' (irq_node' s') s'; valid_irq_handlers' s'; valid_irq_states' s'; valid_machine_state' s'; irqs_masked' s'; valid_queues' s'; ct_not_inQ s'; ct_idle_or_in_cur_domain' s'; valid_pde_mappings' s'; pspace_domain_valid s'; ksCurDomain s' \<le> maxDomain; ksDomSchedule (KernelInit_H.newKernelState undefined) \<noteq> []; \<forall>x\<in>set (ksDomSchedule (KernelInit_H.newKernelState undefined)). dschDomain x \<le> maxDomain \<and> 0 < dschLength x; ksDomSchedule s' = ksDomSchedule (KernelInit_H.newKernelState undefined); ksDomScheduleIdx s' < length (ksDomSchedule (KernelInit_H.newKernelState undefined)); untyped_ranges_zero' s'; cur_tcb' s'; q \<in> S; ctes_of s' cref = Some ctea; P (cteCap ctea); q \<in> cte_refs' (cteCap ctea) (irq_node' s'); kernel_data_refs \<inter> capRange (cteCap cte) = {} \<and> global_refs' s' \<subseteq> kernel_data_refs; \<nexists>irq. cteCap ctea = capability.IRQHandlerCap irq; ctea = CTE x1 x2; cref \<in> descendants_of' p (ctes_of s')\<rbrakk> \<Longrightarrow> False proof (prove)
goal (5 subgoals):
 1. \<And>cref ctea x1 x2. \<lbrakk>descendants_range_in' S p (ctes_of s'); S \<subseteq> capRange (cteCap cte); isUntypedCap (cteCap cte); valid_objs' s'; valid_mdb' s'; valid_pspace' s'; sch_act_wf (ksSchedulerAction s') s'; Invariants_H.valid_queues s'; sym_refs (state_refs_of' s'); if_live_then_nonz_cap' s'; if_unsafe_then_cap' s'; valid_idle' s'; valid_global_refs' s'; valid_arch_state' s'; valid_irq_node' (irq_node' s') s'; valid_irq_handlers' s'; valid_irq_states' s'; valid_machine_state' s'; irqs_masked' s'; valid_queues' s'; ct_not_inQ s'; ct_idle_or_in_cur_domain' s'; valid_pde_mappings' s'; pspace_domain_valid s'; ksCurDomain s' \<le> maxDomain; ksDomSchedule (KernelInit_H.newKernelState undefined) \<noteq> []; \<forall>x\<in>set (ksDomSchedule (KernelInit_H.newKernelState undefined)). dschDomain x \<le> maxDomain \<and> 0 < dschLength x; ksDomSchedule s' = ksDomSchedule (KernelInit_H.newKernelState undefined); ksDomScheduleIdx s' < length (ksDomSchedule (KernelInit_H.newKernelState undefined)); untyped_ranges_zero' s'; cur_tcb' s'; ctes_of s' cref = Some ctea; P (cteCap ctea); q \<in> cte_refs' (cteCap ctea) (irq_node' s'); kernel_data_refs \<inter> capRange (cteCap cte) = {} \<and> global_refs' s' \<subseteq> kernel_data_refs; \<nexists>irq. cteCap ctea = capability.IRQHandlerCap irq; ctea = CTE x1 x2\<rbrakk> \<Longrightarrow> S \<subseteq> untypedRange (cteCap cte)
 2. \<And>cref ctea x1 x2. \<lbrakk>descendants_range_in' S p (ctes_of s'); S \<subseteq> capRange (cteCap cte); isUntypedCap (cteCap cte); valid_objs' s'; valid_mdb' s'; valid_pspace' s'; sch_act_wf (ksSchedulerAction s') s'; Invariants_H.valid_queues s'; sym_refs (state_refs_of' s'); if_live_then_nonz_cap' s'; if_unsafe_then_cap' s'; valid_idle' s'; valid_global_refs' s'; valid_arch_state' s'; valid_irq_node' (irq_node' s') s'; valid_irq_handlers' s'; valid_irq_states' s'; valid_machine_state' s'; irqs_masked' s'; valid_queues' s'; ct_not_inQ s'; ct_idle_or_in_cur_domain' s'; valid_pde_mappings' s'; pspace_domain_valid s'; ksCurDomain s' \<le> maxDomain; ksDomSchedule (KernelInit_H.newKernelState undefined) \<noteq> []; \<forall>x\<in>set (ksDomSchedule (KernelInit_H.newKernelState undefined)). dschDomain x \<le> maxDomain \<and> 0 < dschLength x; ksDomSchedule s' = ksDomSchedule (KernelInit_H.newKernelState undefined); ksDomScheduleIdx s' < length (ksDomSchedule (KernelInit_H.newKernelState undefined)); untyped_ranges_zero' s'; cur_tcb' s'; ctes_of s' cref = Some ctea; P (cteCap ctea); q \<in> cte_refs' (cteCap ctea) (irq_node' s'); kernel_data_refs \<inter> capRange (cteCap cte) = {} \<and> global_refs' s' \<subseteq> kernel_data_refs; \<nexists>irq. cteCap ctea = capability.IRQHandlerCap irq; ctea = CTE x1 x2; q \<in> untypedRange (cteCap cte)\<rbrakk> \<Longrightarrow> capRange (cteCap ctea) \<inter> untypedRange (cteCap cte) \<noteq> {}
 3. \<And>cref ctea x1 x2. \<lbrakk>descendants_range_in' S p (ctes_of s'); S \<subseteq> capRange (cteCap cte); isUntypedCap (cteCap cte); valid_objs' s'; valid_mdb' s'; valid_pspace' s'; sch_act_wf (ksSchedulerAction s') s'; Invariants_H.valid_queues s'; sym_refs (state_refs_of' s'); if_live_then_nonz_cap' s'; if_unsafe_then_cap' s'; valid_idle' s'; valid_global_refs' s'; valid_arch_state' s'; valid_irq_node' (irq_node' s') s'; valid_irq_handlers' s'; valid_irq_states' s'; valid_machine_state' s'; irqs_masked' s'; valid_queues' s'; ct_not_inQ s'; ct_idle_or_in_cur_domain' s'; valid_pde_mappings' s'; pspace_domain_valid s'; ksCurDomain s' \<le> maxDomain; ksDomSchedule (KernelInit_H.newKernelState undefined) \<noteq> []; \<forall>x\<in>set (ksDomSchedule (KernelInit_H.newKernelState undefined)). dschDomain x \<le> maxDomain \<and> 0 < dschLength x; ksDomSchedule s' = ksDomSchedule (KernelInit_H.newKernelState undefined); ksDomScheduleIdx s' < length (ksDomSchedule (KernelInit_H.newKernelState undefined)); untyped_ranges_zero' s'; cur_tcb' s'; q \<in> S; ctes_of s' cref = Some ctea; P (cteCap ctea); q \<in> cte_refs' (cteCap ctea) (irq_node' s'); kernel_data_refs \<inter> capRange (cteCap cte) = {} \<and> global_refs' s' \<subseteq> kernel_data_refs; \<nexists>irq. cteCap ctea = capability.IRQHandlerCap irq; ctea = CTE x1 x2\<rbrakk> \<Longrightarrow> \<not> isUntypedCap (cteCap ctea)
 4. \<And>cref ctea x1 x2. \<lbrakk>descendants_range_in' S p (ctes_of s'); S \<subseteq> capRange (cteCap cte); isUntypedCap (cteCap cte); valid_objs' s'; valid_mdb' s'; valid_pspace' s'; sch_act_wf (ksSchedulerAction s') s'; Invariants_H.valid_queues s'; sym_refs (state_refs_of' s'); if_live_then_nonz_cap' s'; if_unsafe_then_cap' s'; valid_idle' s'; valid_global_refs' s'; valid_arch_state' s'; valid_irq_node' (irq_node' s') s'; valid_irq_handlers' s'; valid_irq_states' s'; valid_machine_state' s'; irqs_masked' s'; valid_queues' s'; ct_not_inQ s'; ct_idle_or_in_cur_domain' s'; valid_pde_mappings' s'; pspace_domain_valid s'; ksCurDomain s' \<le> maxDomain; ksDomSchedule (KernelInit_H.newKernelState undefined) \<noteq> []; \<forall>x\<in>set (ksDomSchedule (KernelInit_H.newKernelState undefined)). dschDomain x \<le> maxDomain \<and> 0 < dschLength x; ksDomSchedule s' = ksDomSchedule (KernelInit_H.newKernelState undefined); ksDomScheduleIdx s' < length (ksDomSchedule (KernelInit_H.newKernelState undefined)); untyped_ranges_zero' s'; cur_tcb' s'; q \<in> S; ctes_of s' cref = Some ctea; P (cteCap ctea); q \<in> cte_refs' (cteCap ctea) (irq_node' s'); kernel_data_refs \<inter> capRange (cteCap cte) = {} \<and> global_refs' s' \<subseteq> kernel_data_refs; \<nexists>irq. cteCap ctea = capability.IRQHandlerCap irq; ctea = CTE x1 x2\<rbrakk> \<Longrightarrow> untyped_mdb' (ctes_of s')
 5. \<And>cref ctea x1 x2. \<lbrakk>descendants_range_in' S p (ctes_of s'); S \<subseteq> capRange (cteCap cte); isUntypedCap (cteCap cte); valid_objs' s'; valid_mdb' s'; valid_pspace' s'; sch_act_wf (ksSchedulerAction s') s'; Invariants_H.valid_queues s'; sym_refs (state_refs_of' s'); if_live_then_nonz_cap' s'; if_unsafe_then_cap' s'; valid_idle' s'; valid_global_refs' s'; valid_arch_state' s'; valid_irq_node' (irq_node' s') s'; valid_irq_handlers' s'; valid_irq_states' s'; valid_machine_state' s'; irqs_masked' s'; valid_queues' s'; ct_not_inQ s'; ct_idle_or_in_cur_domain' s'; valid_pde_mappings' s'; pspace_domain_valid s'; ksCurDomain s' \<le> maxDomain; ksDomSchedule (KernelInit_H.newKernelState undefined) \<noteq> []; \<forall>x\<in>set (ksDomSchedule (KernelInit_H.newKernelState undefined)). dschDomain x \<le> maxDomain \<and> 0 < dschLength x; ksDomSchedule s' = ksDomSchedule (KernelInit_H.newKernelState undefined); ksDomScheduleIdx s' < length (ksDomSchedule (KernelInit_H.newKernelState undefined)); untyped_ranges_zero' s'; cur_tcb' s'; q \<in> S; ctes_of s' cref = Some ctea; P (cteCap ctea); q \<in> cte_refs' (cteCap ctea) (irq_node' s'); kernel_data_refs \<inter> capRange (cteCap cte) = {} \<and> global_refs' s' \<subseteq> kernel_data_refs; \<nexists>irq. cteCap ctea = capability.IRQHandlerCap irq; ctea = CTE x1 x2; cref \<in> descendants_of' p (ctes_of s')\<rbrakk> \<Longrightarrow> False proof (prove)
goal (4 subgoals):
 1. \<And>cref ctea x1 x2. \<lbrakk>descendants_range_in' S p (ctes_of s'); S \<subseteq> capRange (cteCap cte); isUntypedCap (cteCap cte); valid_objs' s'; valid_mdb' s'; valid_pspace' s'; sch_act_wf (ksSchedulerAction s') s'; Invariants_H.valid_queues s'; sym_refs (state_refs_of' s'); if_live_then_nonz_cap' s'; if_unsafe_then_cap' s'; valid_idle' s'; valid_global_refs' s'; valid_arch_state' s'; valid_irq_node' (irq_node' s') s'; valid_irq_handlers' s'; valid_irq_states' s'; valid_machine_state' s'; irqs_masked' s'; valid_queues' s'; ct_not_inQ s'; ct_idle_or_in_cur_domain' s'; valid_pde_mappings' s'; pspace_domain_valid s'; ksCurDomain s' \<le> maxDomain; ksDomSchedule (KernelInit_H.newKernelState undefined) \<noteq> []; \<forall>x\<in>set (ksDomSchedule (KernelInit_H.newKernelState undefined)). dschDomain x \<le> maxDomain \<and> 0 < dschLength x; ksDomSchedule s' = ksDomSchedule (KernelInit_H.newKernelState undefined); ksDomScheduleIdx s' < length (ksDomSchedule (KernelInit_H.newKernelState undefined)); untyped_ranges_zero' s'; cur_tcb' s'; ctes_of s' cref = Some ctea; P (cteCap ctea); q \<in> cte_refs' (cteCap ctea) (irq_node' s'); kernel_data_refs \<inter> capRange (cteCap cte) = {} \<and> global_refs' s' \<subseteq> kernel_data_refs; \<nexists>irq. cteCap ctea = capability.IRQHandlerCap irq; ctea = CTE x1 x2; q \<in> untypedRange (cteCap cte)\<rbrakk> \<Longrightarrow> capRange (cteCap ctea) \<inter> untypedRange (cteCap cte) \<noteq> {}
 2. \<And>cref ctea x1 x2. \<lbrakk>descendants_range_in' S p (ctes_of s'); S \<subseteq> capRange (cteCap cte); isUntypedCap (cteCap cte); valid_objs' s'; valid_mdb' s'; valid_pspace' s'; sch_act_wf (ksSchedulerAction s') s'; Invariants_H.valid_queues s'; sym_refs (state_refs_of' s'); if_live_then_nonz_cap' s'; if_unsafe_then_cap' s'; valid_idle' s'; valid_global_refs' s'; valid_arch_state' s'; valid_irq_node' (irq_node' s') s'; valid_irq_handlers' s'; valid_irq_states' s'; valid_machine_state' s'; irqs_masked' s'; valid_queues' s'; ct_not_inQ s'; ct_idle_or_in_cur_domain' s'; valid_pde_mappings' s'; pspace_domain_valid s'; ksCurDomain s' \<le> maxDomain; ksDomSchedule (KernelInit_H.newKernelState undefined) \<noteq> []; \<forall>x\<in>set (ksDomSchedule (KernelInit_H.newKernelState undefined)). dschDomain x \<le> maxDomain \<and> 0 < dschLength x; ksDomSchedule s' = ksDomSchedule (KernelInit_H.newKernelState undefined); ksDomScheduleIdx s' < length (ksDomSchedule (KernelInit_H.newKernelState undefined)); untyped_ranges_zero' s'; cur_tcb' s'; q \<in> S; ctes_of s' cref = Some ctea; P (cteCap ctea); q \<in> cte_refs' (cteCap ctea) (irq_node' s'); kernel_data_refs \<inter> capRange (cteCap cte) = {} \<and> global_refs' s' \<subseteq> kernel_data_refs; \<nexists>irq. cteCap ctea = capability.IRQHandlerCap irq; ctea = CTE x1 x2\<rbrakk> \<Longrightarrow> \<not> isUntypedCap (cteCap ctea)
 3. \<And>cref ctea x1 x2. \<lbrakk>descendants_range_in' S p (ctes_of s'); S \<subseteq> capRange (cteCap cte); isUntypedCap (cteCap cte); valid_objs' s'; valid_mdb' s'; valid_pspace' s'; sch_act_wf (ksSchedulerAction s') s'; Invariants_H.valid_queues s'; sym_refs (state_refs_of' s'); if_live_then_nonz_cap' s'; if_unsafe_then_cap' s'; valid_idle' s'; valid_global_refs' s'; valid_arch_state' s'; valid_irq_node' (irq_node' s') s'; valid_irq_handlers' s'; valid_irq_states' s'; valid_machine_state' s'; irqs_masked' s'; valid_queues' s'; ct_not_inQ s'; ct_idle_or_in_cur_domain' s'; valid_pde_mappings' s'; pspace_domain_valid s'; ksCurDomain s' \<le> maxDomain; ksDomSchedule (KernelInit_H.newKernelState undefined) \<noteq> []; \<forall>x\<in>set (ksDomSchedule (KernelInit_H.newKernelState undefined)). dschDomain x \<le> maxDomain \<and> 0 < dschLength x; ksDomSchedule s' = ksDomSchedule (KernelInit_H.newKernelState undefined); ksDomScheduleIdx s' < length (ksDomSchedule (KernelInit_H.newKernelState undefined)); untyped_ranges_zero' s'; cur_tcb' s'; q \<in> S; ctes_of s' cref = Some ctea; P (cteCap ctea); q \<in> cte_refs' (cteCap ctea) (irq_node' s'); kernel_data_refs \<inter> capRange (cteCap cte) = {} \<and> global_refs' s' \<subseteq> kernel_data_refs; \<nexists>irq. cteCap ctea = capability.IRQHandlerCap irq; ctea = CTE x1 x2\<rbrakk> \<Longrightarrow> untyped_mdb' (ctes_of s')
 4. \<And>cref ctea x1 x2. \<lbrakk>descendants_range_in' S p (ctes_of s'); S \<subseteq> capRange (cteCap cte); isUntypedCap (cteCap cte); valid_objs' s'; valid_mdb' s'; valid_pspace' s'; sch_act_wf (ksSchedulerAction s') s'; Invariants_H.valid_queues s'; sym_refs (state_refs_of' s'); if_live_then_nonz_cap' s'; if_unsafe_then_cap' s'; valid_idle' s'; valid_global_refs' s'; valid_arch_state' s'; valid_irq_node' (irq_node' s') s'; valid_irq_handlers' s'; valid_irq_states' s'; valid_machine_state' s'; irqs_masked' s'; valid_queues' s'; ct_not_inQ s'; ct_idle_or_in_cur_domain' s'; valid_pde_mappings' s'; pspace_domain_valid s'; ksCurDomain s' \<le> maxDomain; ksDomSchedule (KernelInit_H.newKernelState undefined) \<noteq> []; \<forall>x\<in>set (ksDomSchedule (KernelInit_H.newKernelState undefined)). dschDomain x \<le> maxDomain \<and> 0 < dschLength x; ksDomSchedule s' = ksDomSchedule (KernelInit_H.newKernelState undefined); ksDomScheduleIdx s' < length (ksDomSchedule (KernelInit_H.newKernelState undefined)); untyped_ranges_zero' s'; cur_tcb' s'; q \<in> S; ctes_of s' cref = Some ctea; P (cteCap ctea); q \<in> cte_refs' (cteCap ctea) (irq_node' s'); kernel_data_refs \<inter> capRange (cteCap cte) = {} \<and> global_refs' s' \<subseteq> kernel_data_refs; \<nexists>irq. cteCap ctea = capability.IRQHandlerCap irq; ctea = CTE x1 x2; cref \<in> descendants_of' p (ctes_of s')\<rbrakk> \<Longrightarrow> False proof (prove)
goal (4 subgoals):
 1. \<And>cref x1 x2. \<lbrakk>descendants_range_in' S p (ctes_of s'); S \<subseteq> capRange (cteCap cte); isUntypedCap (cteCap cte); valid_objs' s'; valid_mdb' s'; valid_pspace' s'; sch_act_wf (ksSchedulerAction s') s'; Invariants_H.valid_queues s'; sym_refs (state_refs_of' s'); if_live_then_nonz_cap' s'; if_unsafe_then_cap' s'; valid_idle' s'; valid_global_refs' s'; valid_arch_state' s'; valid_irq_node' (irq_node' s') s'; valid_irq_handlers' s'; valid_irq_states' s'; valid_machine_state' s'; irqs_masked' s'; valid_queues' s'; ct_not_inQ s'; ct_idle_or_in_cur_domain' s'; valid_pde_mappings' s'; pspace_domain_valid s'; ksCurDomain s' \<le> maxDomain; ksDomSchedule (KernelInit_H.newKernelState undefined) \<noteq> []; \<forall>x\<in>set (ksDomSchedule (KernelInit_H.newKernelState undefined)). dschDomain x \<le> maxDomain \<and> 0 < dschLength x; ksDomSchedule s' = ksDomSchedule (KernelInit_H.newKernelState undefined); ksDomScheduleIdx s' < length (ksDomSchedule (KernelInit_H.newKernelState undefined)); untyped_ranges_zero' s'; cur_tcb' s'; ctes_of s' cref = Some (CTE x1 x2); P x1; q \<in> cte_refs' x1 (irq_node' s'); \<forall>irq. x1 \<noteq> capability.IRQHandlerCap irq; q \<in> untypedRange (cteCap cte); kernel_data_refs \<inter> capRange (cteCap cte) = {}; global_refs' s' \<subseteq> kernel_data_refs; capRange x1 \<inter> untypedRange (cteCap cte) = {}\<rbrakk> \<Longrightarrow> False
 2. \<And>cref ctea x1 x2. \<lbrakk>descendants_range_in' S p (ctes_of s'); S \<subseteq> capRange (cteCap cte); isUntypedCap (cteCap cte); valid_objs' s'; valid_mdb' s'; valid_pspace' s'; sch_act_wf (ksSchedulerAction s') s'; Invariants_H.valid_queues s'; sym_refs (state_refs_of' s'); if_live_then_nonz_cap' s'; if_unsafe_then_cap' s'; valid_idle' s'; valid_global_refs' s'; valid_arch_state' s'; valid_irq_node' (irq_node' s') s'; valid_irq_handlers' s'; valid_irq_states' s'; valid_machine_state' s'; irqs_masked' s'; valid_queues' s'; ct_not_inQ s'; ct_idle_or_in_cur_domain' s'; valid_pde_mappings' s'; pspace_domain_valid s'; ksCurDomain s' \<le> maxDomain; ksDomSchedule (KernelInit_H.newKernelState undefined) \<noteq> []; \<forall>x\<in>set (ksDomSchedule (KernelInit_H.newKernelState undefined)). dschDomain x \<le> maxDomain \<and> 0 < dschLength x; ksDomSchedule s' = ksDomSchedule (KernelInit_H.newKernelState undefined); ksDomScheduleIdx s' < length (ksDomSchedule (KernelInit_H.newKernelState undefined)); untyped_ranges_zero' s'; cur_tcb' s'; q \<in> S; ctes_of s' cref = Some ctea; P (cteCap ctea); q \<in> cte_refs' (cteCap ctea) (irq_node' s'); kernel_data_refs \<inter> capRange (cteCap cte) = {} \<and> global_refs' s' \<subseteq> kernel_data_refs; \<nexists>irq. cteCap ctea = capability.IRQHandlerCap irq; ctea = CTE x1 x2\<rbrakk> \<Longrightarrow> \<not> isUntypedCap (cteCap ctea)
 3. \<And>cref ctea x1 x2. \<lbrakk>descendants_range_in' S p (ctes_of s'); S \<subseteq> capRange (cteCap cte); isUntypedCap (cteCap cte); valid_objs' s'; valid_mdb' s'; valid_pspace' s'; sch_act_wf (ksSchedulerAction s') s'; Invariants_H.valid_queues s'; sym_refs (state_refs_of' s'); if_live_then_nonz_cap' s'; if_unsafe_then_cap' s'; valid_idle' s'; valid_global_refs' s'; valid_arch_state' s'; valid_irq_node' (irq_node' s') s'; valid_irq_handlers' s'; valid_irq_states' s'; valid_machine_state' s'; irqs_masked' s'; valid_queues' s'; ct_not_inQ s'; ct_idle_or_in_cur_domain' s'; valid_pde_mappings' s'; pspace_domain_valid s'; ksCurDomain s' \<le> maxDomain; ksDomSchedule (KernelInit_H.newKernelState undefined) \<noteq> []; \<forall>x\<in>set (ksDomSchedule (KernelInit_H.newKernelState undefined)). dschDomain x \<le> maxDomain \<and> 0 < dschLength x; ksDomSchedule s' = ksDomSchedule (KernelInit_H.newKernelState undefined); ksDomScheduleIdx s' < length (ksDomSchedule (KernelInit_H.newKernelState undefined)); untyped_ranges_zero' s'; cur_tcb' s'; q \<in> S; ctes_of s' cref = Some ctea; P (cteCap ctea); q \<in> cte_refs' (cteCap ctea) (irq_node' s'); kernel_data_refs \<inter> capRange (cteCap cte) = {} \<and> global_refs' s' \<subseteq> kernel_data_refs; \<nexists>irq. cteCap ctea = capability.IRQHandlerCap irq; ctea = CTE x1 x2\<rbrakk> \<Longrightarrow> untyped_mdb' (ctes_of s')
 4. \<And>cref ctea x1 x2. \<lbrakk>descendants_range_in' S p (ctes_of s'); S \<subseteq> capRange (cteCap cte); isUntypedCap (cteCap cte); valid_objs' s'; valid_mdb' s'; valid_pspace' s'; sch_act_wf (ksSchedulerAction s') s'; Invariants_H.valid_queues s'; sym_refs (state_refs_of' s'); if_live_then_nonz_cap' s'; if_unsafe_then_cap' s'; valid_idle' s'; valid_global_refs' s'; valid_arch_state' s'; valid_irq_node' (irq_node' s') s'; valid_irq_handlers' s'; valid_irq_states' s'; valid_machine_state' s'; irqs_masked' s'; valid_queues' s'; ct_not_inQ s'; ct_idle_or_in_cur_domain' s'; valid_pde_mappings' s'; pspace_domain_valid s'; ksCurDomain s' \<le> maxDomain; ksDomSchedule (KernelInit_H.newKernelState undefined) \<noteq> []; \<forall>x\<in>set (ksDomSchedule (KernelInit_H.newKernelState undefined)). dschDomain x \<le> maxDomain \<and> 0 < dschLength x; ksDomSchedule s' = ksDomSchedule (KernelInit_H.newKernelState undefined); ksDomScheduleIdx s' < length (ksDomSchedule (KernelInit_H.newKernelState undefined)); untyped_ranges_zero' s'; cur_tcb' s'; q \<in> S; ctes_of s' cref = Some ctea; P (cteCap ctea); q \<in> cte_refs' (cteCap ctea) (irq_node' s'); kernel_data_refs \<inter> capRange (cteCap cte) = {} \<and> global_refs' s' \<subseteq> kernel_data_refs; \<nexists>irq. cteCap ctea = capability.IRQHandlerCap irq; ctea = CTE x1 x2; cref \<in> descendants_of' p (ctes_of s')\<rbrakk> \<Longrightarrow> False proof (prove)
goal (5 subgoals):
 1. \<And>cref x1 x2. \<lbrakk>descendants_range_in' S p (ctes_of s'); S \<subseteq> capRange (cteCap cte); isUntypedCap (cteCap cte); valid_objs' s'; valid_mdb' s'; valid_pspace' s'; sch_act_wf (ksSchedulerAction s') s'; Invariants_H.valid_queues s'; sym_refs (state_refs_of' s'); if_live_then_nonz_cap' s'; if_unsafe_then_cap' s'; valid_idle' s'; valid_global_refs' s'; valid_arch_state' s'; valid_irq_node' (irq_node' s') s'; valid_irq_handlers' s'; valid_irq_states' s'; valid_machine_state' s'; irqs_masked' s'; valid_queues' s'; ct_not_inQ s'; ct_idle_or_in_cur_domain' s'; valid_pde_mappings' s'; pspace_domain_valid s'; ksCurDomain s' \<le> maxDomain; ksDomSchedule (KernelInit_H.newKernelState undefined) \<noteq> []; \<forall>x\<in>set (ksDomSchedule (KernelInit_H.newKernelState undefined)). dschDomain x \<le> maxDomain \<and> 0 < dschLength x; ksDomSchedule s' = ksDomSchedule (KernelInit_H.newKernelState undefined); ksDomScheduleIdx s' < length (ksDomSchedule (KernelInit_H.newKernelState undefined)); untyped_ranges_zero' s'; cur_tcb' s'; ctes_of s' cref = Some (CTE x1 x2); P x1; q \<in> cte_refs' x1 (irq_node' s'); q \<in> untypedRange (cteCap cte); kernel_data_refs \<inter> capRange (cteCap cte) = {}; global_refs' s' \<subseteq> kernel_data_refs; capRange x1 \<inter> untypedRange (cteCap cte) = {}\<rbrakk> \<Longrightarrow> valid_cap' x1 (?s69 cref x1 x2)
 2. \<And>cref x1 x2. \<lbrakk>descendants_range_in' S p (ctes_of s'); S \<subseteq> capRange (cteCap cte); isUntypedCap (cteCap cte); valid_objs' s'; valid_mdb' s'; valid_pspace' s'; sch_act_wf (ksSchedulerAction s') s'; Invariants_H.valid_queues s'; sym_refs (state_refs_of' s'); if_live_then_nonz_cap' s'; if_unsafe_then_cap' s'; valid_idle' s'; valid_global_refs' s'; valid_arch_state' s'; valid_irq_node' (irq_node' s') s'; valid_irq_handlers' s'; valid_irq_states' s'; valid_machine_state' s'; irqs_masked' s'; valid_queues' s'; ct_not_inQ s'; ct_idle_or_in_cur_domain' s'; valid_pde_mappings' s'; pspace_domain_valid s'; ksCurDomain s' \<le> maxDomain; ksDomSchedule (KernelInit_H.newKernelState undefined) \<noteq> []; \<forall>x\<in>set (ksDomSchedule (KernelInit_H.newKernelState undefined)). dschDomain x \<le> maxDomain \<and> 0 < dschLength x; ksDomSchedule s' = ksDomSchedule (KernelInit_H.newKernelState undefined); ksDomScheduleIdx s' < length (ksDomSchedule (KernelInit_H.newKernelState undefined)); untyped_ranges_zero' s'; cur_tcb' s'; ctes_of s' cref = Some (CTE x1 x2); P x1; q \<in> cte_refs' x1 (irq_node' s'); q \<in> untypedRange (cteCap cte); kernel_data_refs \<inter> capRange (cteCap cte) = {}; global_refs' s' \<subseteq> kernel_data_refs; capRange x1 \<inter> untypedRange (cteCap cte) = {}; cte_refs' x1 (irq_node' s') \<subseteq> capRange x1\<rbrakk> \<Longrightarrow> False
 3. \<And>cref ctea x1 x2. \<lbrakk>descendants_range_in' S p (ctes_of s'); S \<subseteq> capRange (cteCap cte); isUntypedCap (cteCap cte); valid_objs' s'; valid_mdb' s'; valid_pspace' s'; sch_act_wf (ksSchedulerAction s') s'; Invariants_H.valid_queues s'; sym_refs (state_refs_of' s'); if_live_then_nonz_cap' s'; if_unsafe_then_cap' s'; valid_idle' s'; valid_global_refs' s'; valid_arch_state' s'; valid_irq_node' (irq_node' s') s'; valid_irq_handlers' s'; valid_irq_states' s'; valid_machine_state' s'; irqs_masked' s'; valid_queues' s'; ct_not_inQ s'; ct_idle_or_in_cur_domain' s'; valid_pde_mappings' s'; pspace_domain_valid s'; ksCurDomain s' \<le> maxDomain; ksDomSchedule (KernelInit_H.newKernelState undefined) \<noteq> []; \<forall>x\<in>set (ksDomSchedule (KernelInit_H.newKernelState undefined)). dschDomain x \<le> maxDomain \<and> 0 < dschLength x; ksDomSchedule s' = ksDomSchedule (KernelInit_H.newKernelState undefined); ksDomScheduleIdx s' < length (ksDomSchedule (KernelInit_H.newKernelState undefined)); untyped_ranges_zero' s'; cur_tcb' s'; q \<in> S; ctes_of s' cref = Some ctea; P (cteCap ctea); q \<in> cte_refs' (cteCap ctea) (irq_node' s'); kernel_data_refs \<inter> capRange (cteCap cte) = {} \<and> global_refs' s' \<subseteq> kernel_data_refs; \<nexists>irq. cteCap ctea = capability.IRQHandlerCap irq; ctea = CTE x1 x2\<rbrakk> \<Longrightarrow> \<not> isUntypedCap (cteCap ctea)
 4. \<And>cref ctea x1 x2. \<lbrakk>descendants_range_in' S p (ctes_of s'); S \<subseteq> capRange (cteCap cte); isUntypedCap (cteCap cte); valid_objs' s'; valid_mdb' s'; valid_pspace' s'; sch_act_wf (ksSchedulerAction s') s'; Invariants_H.valid_queues s'; sym_refs (state_refs_of' s'); if_live_then_nonz_cap' s'; if_unsafe_then_cap' s'; valid_idle' s'; valid_global_refs' s'; valid_arch_state' s'; valid_irq_node' (irq_node' s') s'; valid_irq_handlers' s'; valid_irq_states' s'; valid_machine_state' s'; irqs_masked' s'; valid_queues' s'; ct_not_inQ s'; ct_idle_or_in_cur_domain' s'; valid_pde_mappings' s'; pspace_domain_valid s'; ksCurDomain s' \<le> maxDomain; ksDomSchedule (KernelInit_H.newKernelState undefined) \<noteq> []; \<forall>x\<in>set (ksDomSchedule (KernelInit_H.newKernelState undefined)). dschDomain x \<le> maxDomain \<and> 0 < dschLength x; ksDomSchedule s' = ksDomSchedule (KernelInit_H.newKernelState undefined); ksDomScheduleIdx s' < length (ksDomSchedule (KernelInit_H.newKernelState undefined)); untyped_ranges_zero' s'; cur_tcb' s'; q \<in> S; ctes_of s' cref = Some ctea; P (cteCap ctea); q \<in> cte_refs' (cteCap ctea) (irq_node' s'); kernel_data_refs \<inter> capRange (cteCap cte) = {} \<and> global_refs' s' \<subseteq> kernel_data_refs; \<nexists>irq. cteCap ctea = capability.IRQHandlerCap irq; ctea = CTE x1 x2\<rbrakk> \<Longrightarrow> untyped_mdb' (ctes_of s')
 5. \<And>cref ctea x1 x2. \<lbrakk>descendants_range_in' S p (ctes_of s'); S \<subseteq> capRange (cteCap cte); isUntypedCap (cteCap cte); valid_objs' s'; valid_mdb' s'; valid_pspace' s'; sch_act_wf (ksSchedulerAction s') s'; Invariants_H.valid_queues s'; sym_refs (state_refs_of' s'); if_live_then_nonz_cap' s'; if_unsafe_then_cap' s'; valid_idle' s'; valid_global_refs' s'; valid_arch_state' s'; valid_irq_node' (irq_node' s') s'; valid_irq_handlers' s'; valid_irq_states' s'; valid_machine_state' s'; irqs_masked' s'; valid_queues' s'; ct_not_inQ s'; ct_idle_or_in_cur_domain' s'; valid_pde_mappings' s'; pspace_domain_valid s'; ksCurDomain s' \<le> maxDomain; ksDomSchedule (KernelInit_H.newKernelState undefined) \<noteq> []; \<forall>x\<in>set (ksDomSchedule (KernelInit_H.newKernelState undefined)). dschDomain x \<le> maxDomain \<and> 0 < dschLength x; ksDomSchedule s' = ksDomSchedule (KernelInit_H.newKernelState undefined); ksDomScheduleIdx s' < length (ksDomSchedule (KernelInit_H.newKernelState undefined)); untyped_ranges_zero' s'; cur_tcb' s'; q \<in> S; ctes_of s' cref = Some ctea; P (cteCap ctea); q \<in> cte_refs' (cteCap ctea) (irq_node' s'); kernel_data_refs \<inter> capRange (cteCap cte) = {} \<and> global_refs' s' \<subseteq> kernel_data_refs; \<nexists>irq. cteCap ctea = capability.IRQHandlerCap irq; ctea = CTE x1 x2; cref \<in> descendants_of' p (ctes_of s')\<rbrakk> \<Longrightarrow> False proof (prove)
goal (4 subgoals):
 1. \<And>cref x1 x2. \<lbrakk>descendants_range_in' S p (ctes_of s'); S \<subseteq> capRange (cteCap cte); isUntypedCap (cteCap cte); valid_objs' s'; valid_mdb' s'; valid_pspace' s'; sch_act_wf (ksSchedulerAction s') s'; Invariants_H.valid_queues s'; sym_refs (state_refs_of' s'); if_live_then_nonz_cap' s'; if_unsafe_then_cap' s'; valid_idle' s'; valid_global_refs' s'; valid_arch_state' s'; valid_irq_node' (irq_node' s') s'; valid_irq_handlers' s'; valid_irq_states' s'; valid_machine_state' s'; irqs_masked' s'; valid_queues' s'; ct_not_inQ s'; ct_idle_or_in_cur_domain' s'; valid_pde_mappings' s'; pspace_domain_valid s'; ksCurDomain s' \<le> maxDomain; ksDomSchedule (KernelInit_H.newKernelState undefined) \<noteq> []; \<forall>x\<in>set (ksDomSchedule (KernelInit_H.newKernelState undefined)). dschDomain x \<le> maxDomain \<and> 0 < dschLength x; ksDomSchedule s' = ksDomSchedule (KernelInit_H.newKernelState undefined); ksDomScheduleIdx s' < length (ksDomSchedule (KernelInit_H.newKernelState undefined)); untyped_ranges_zero' s'; cur_tcb' s'; ctes_of s' cref = Some (CTE x1 x2); P x1; q \<in> cte_refs' x1 (irq_node' s'); q \<in> untypedRange (cteCap cte); kernel_data_refs \<inter> capRange (cteCap cte) = {}; global_refs' s' \<subseteq> kernel_data_refs; capRange x1 \<inter> untypedRange (cteCap cte) = {}; cte_refs' x1 (irq_node' s') \<subseteq> capRange x1\<rbrakk> \<Longrightarrow> False
 2. \<And>cref ctea x1 x2. \<lbrakk>descendants_range_in' S p (ctes_of s'); S \<subseteq> capRange (cteCap cte); isUntypedCap (cteCap cte); valid_objs' s'; valid_mdb' s'; valid_pspace' s'; sch_act_wf (ksSchedulerAction s') s'; Invariants_H.valid_queues s'; sym_refs (state_refs_of' s'); if_live_then_nonz_cap' s'; if_unsafe_then_cap' s'; valid_idle' s'; valid_global_refs' s'; valid_arch_state' s'; valid_irq_node' (irq_node' s') s'; valid_irq_handlers' s'; valid_irq_states' s'; valid_machine_state' s'; irqs_masked' s'; valid_queues' s'; ct_not_inQ s'; ct_idle_or_in_cur_domain' s'; valid_pde_mappings' s'; pspace_domain_valid s'; ksCurDomain s' \<le> maxDomain; ksDomSchedule (KernelInit_H.newKernelState undefined) \<noteq> []; \<forall>x\<in>set (ksDomSchedule (KernelInit_H.newKernelState undefined)). dschDomain x \<le> maxDomain \<and> 0 < dschLength x; ksDomSchedule s' = ksDomSchedule (KernelInit_H.newKernelState undefined); ksDomScheduleIdx s' < length (ksDomSchedule (KernelInit_H.newKernelState undefined)); untyped_ranges_zero' s'; cur_tcb' s'; q \<in> S; ctes_of s' cref = Some ctea; P (cteCap ctea); q \<in> cte_refs' (cteCap ctea) (irq_node' s'); kernel_data_refs \<inter> capRange (cteCap cte) = {} \<and> global_refs' s' \<subseteq> kernel_data_refs; \<nexists>irq. cteCap ctea = capability.IRQHandlerCap irq; ctea = CTE x1 x2\<rbrakk> \<Longrightarrow> \<not> isUntypedCap (cteCap ctea)
 3. \<And>cref ctea x1 x2. \<lbrakk>descendants_range_in' S p (ctes_of s'); S \<subseteq> capRange (cteCap cte); isUntypedCap (cteCap cte); valid_objs' s'; valid_mdb' s'; valid_pspace' s'; sch_act_wf (ksSchedulerAction s') s'; Invariants_H.valid_queues s'; sym_refs (state_refs_of' s'); if_live_then_nonz_cap' s'; if_unsafe_then_cap' s'; valid_idle' s'; valid_global_refs' s'; valid_arch_state' s'; valid_irq_node' (irq_node' s') s'; valid_irq_handlers' s'; valid_irq_states' s'; valid_machine_state' s'; irqs_masked' s'; valid_queues' s'; ct_not_inQ s'; ct_idle_or_in_cur_domain' s'; valid_pde_mappings' s'; pspace_domain_valid s'; ksCurDomain s' \<le> maxDomain; ksDomSchedule (KernelInit_H.newKernelState undefined) \<noteq> []; \<forall>x\<in>set (ksDomSchedule (KernelInit_H.newKernelState undefined)). dschDomain x \<le> maxDomain \<and> 0 < dschLength x; ksDomSchedule s' = ksDomSchedule (KernelInit_H.newKernelState undefined); ksDomScheduleIdx s' < length (ksDomSchedule (KernelInit_H.newKernelState undefined)); untyped_ranges_zero' s'; cur_tcb' s'; q \<in> S; ctes_of s' cref = Some ctea; P (cteCap ctea); q \<in> cte_refs' (cteCap ctea) (irq_node' s'); kernel_data_refs \<inter> capRange (cteCap cte) = {} \<and> global_refs' s' \<subseteq> kernel_data_refs; \<nexists>irq. cteCap ctea = capability.IRQHandlerCap irq; ctea = CTE x1 x2\<rbrakk> \<Longrightarrow> untyped_mdb' (ctes_of s')
 4. \<And>cref ctea x1 x2. \<lbrakk>descendants_range_in' S p (ctes_of s'); S \<subseteq> capRange (cteCap cte); isUntypedCap (cteCap cte); valid_objs' s'; valid_mdb' s'; valid_pspace' s'; sch_act_wf (ksSchedulerAction s') s'; Invariants_H.valid_queues s'; sym_refs (state_refs_of' s'); if_live_then_nonz_cap' s'; if_unsafe_then_cap' s'; valid_idle' s'; valid_global_refs' s'; valid_arch_state' s'; valid_irq_node' (irq_node' s') s'; valid_irq_handlers' s'; valid_irq_states' s'; valid_machine_state' s'; irqs_masked' s'; valid_queues' s'; ct_not_inQ s'; ct_idle_or_in_cur_domain' s'; valid_pde_mappings' s'; pspace_domain_valid s'; ksCurDomain s' \<le> maxDomain; ksDomSchedule (KernelInit_H.newKernelState undefined) \<noteq> []; \<forall>x\<in>set (ksDomSchedule (KernelInit_H.newKernelState undefined)). dschDomain x \<le> maxDomain \<and> 0 < dschLength x; ksDomSchedule s' = ksDomSchedule (KernelInit_H.newKernelState undefined); ksDomScheduleIdx s' < length (ksDomSchedule (KernelInit_H.newKernelState undefined)); untyped_ranges_zero' s'; cur_tcb' s'; q \<in> S; ctes_of s' cref = Some ctea; P (cteCap ctea); q \<in> cte_refs' (cteCap ctea) (irq_node' s'); kernel_data_refs \<inter> capRange (cteCap cte) = {} \<and> global_refs' s' \<subseteq> kernel_data_refs; \<nexists>irq. cteCap ctea = capability.IRQHandlerCap irq; ctea = CTE x1 x2; cref \<in> descendants_of' p (ctes_of s')\<rbrakk> \<Longrightarrow> False proof (prove)
goal (3 subgoals):
 1. \<And>cref ctea x1 x2. \<lbrakk>descendants_range_in' S p (ctes_of s'); S \<subseteq> capRange (cteCap cte); isUntypedCap (cteCap cte); valid_objs' s'; valid_mdb' s'; valid_pspace' s'; sch_act_wf (ksSchedulerAction s') s'; Invariants_H.valid_queues s'; sym_refs (state_refs_of' s'); if_live_then_nonz_cap' s'; if_unsafe_then_cap' s'; valid_idle' s'; valid_global_refs' s'; valid_arch_state' s'; valid_irq_node' (irq_node' s') s'; valid_irq_handlers' s'; valid_irq_states' s'; valid_machine_state' s'; irqs_masked' s'; valid_queues' s'; ct_not_inQ s'; ct_idle_or_in_cur_domain' s'; valid_pde_mappings' s'; pspace_domain_valid s'; ksCurDomain s' \<le> maxDomain; ksDomSchedule (KernelInit_H.newKernelState undefined) \<noteq> []; \<forall>x\<in>set (ksDomSchedule (KernelInit_H.newKernelState undefined)). dschDomain x \<le> maxDomain \<and> 0 < dschLength x; ksDomSchedule s' = ksDomSchedule (KernelInit_H.newKernelState undefined); ksDomScheduleIdx s' < length (ksDomSchedule (KernelInit_H.newKernelState undefined)); untyped_ranges_zero' s'; cur_tcb' s'; q \<in> S; ctes_of s' cref = Some ctea; P (cteCap ctea); q \<in> cte_refs' (cteCap ctea) (irq_node' s'); kernel_data_refs \<inter> capRange (cteCap cte) = {} \<and> global_refs' s' \<subseteq> kernel_data_refs; \<nexists>irq. cteCap ctea = capability.IRQHandlerCap irq; ctea = CTE x1 x2\<rbrakk> \<Longrightarrow> \<not> isUntypedCap (cteCap ctea)
 2. \<And>cref ctea x1 x2. \<lbrakk>descendants_range_in' S p (ctes_of s'); S \<subseteq> capRange (cteCap cte); isUntypedCap (cteCap cte); valid_objs' s'; valid_mdb' s'; valid_pspace' s'; sch_act_wf (ksSchedulerAction s') s'; Invariants_H.valid_queues s'; sym_refs (state_refs_of' s'); if_live_then_nonz_cap' s'; if_unsafe_then_cap' s'; valid_idle' s'; valid_global_refs' s'; valid_arch_state' s'; valid_irq_node' (irq_node' s') s'; valid_irq_handlers' s'; valid_irq_states' s'; valid_machine_state' s'; irqs_masked' s'; valid_queues' s'; ct_not_inQ s'; ct_idle_or_in_cur_domain' s'; valid_pde_mappings' s'; pspace_domain_valid s'; ksCurDomain s' \<le> maxDomain; ksDomSchedule (KernelInit_H.newKernelState undefined) \<noteq> []; \<forall>x\<in>set (ksDomSchedule (KernelInit_H.newKernelState undefined)). dschDomain x \<le> maxDomain \<and> 0 < dschLength x; ksDomSchedule s' = ksDomSchedule (KernelInit_H.newKernelState undefined); ksDomScheduleIdx s' < length (ksDomSchedule (KernelInit_H.newKernelState undefined)); untyped_ranges_zero' s'; cur_tcb' s'; q \<in> S; ctes_of s' cref = Some ctea; P (cteCap ctea); q \<in> cte_refs' (cteCap ctea) (irq_node' s'); kernel_data_refs \<inter> capRange (cteCap cte) = {} \<and> global_refs' s' \<subseteq> kernel_data_refs; \<nexists>irq. cteCap ctea = capability.IRQHandlerCap irq; ctea = CTE x1 x2\<rbrakk> \<Longrightarrow> untyped_mdb' (ctes_of s')
 3. \<And>cref ctea x1 x2. \<lbrakk>descendants_range_in' S p (ctes_of s'); S \<subseteq> capRange (cteCap cte); isUntypedCap (cteCap cte); valid_objs' s'; valid_mdb' s'; valid_pspace' s'; sch_act_wf (ksSchedulerAction s') s'; Invariants_H.valid_queues s'; sym_refs (state_refs_of' s'); if_live_then_nonz_cap' s'; if_unsafe_then_cap' s'; valid_idle' s'; valid_global_refs' s'; valid_arch_state' s'; valid_irq_node' (irq_node' s') s'; valid_irq_handlers' s'; valid_irq_states' s'; valid_machine_state' s'; irqs_masked' s'; valid_queues' s'; ct_not_inQ s'; ct_idle_or_in_cur_domain' s'; valid_pde_mappings' s'; pspace_domain_valid s'; ksCurDomain s' \<le> maxDomain; ksDomSchedule (KernelInit_H.newKernelState undefined) \<noteq> []; \<forall>x\<in>set (ksDomSchedule (KernelInit_H.newKernelState undefined)). dschDomain x \<le> maxDomain \<and> 0 < dschLength x; ksDomSchedule s' = ksDomSchedule (KernelInit_H.newKernelState undefined); ksDomScheduleIdx s' < length (ksDomSchedule (KernelInit_H.newKernelState undefined)); untyped_ranges_zero' s'; cur_tcb' s'; q \<in> S; ctes_of s' cref = Some ctea; P (cteCap ctea); q \<in> cte_refs' (cteCap ctea) (irq_node' s'); kernel_data_refs \<inter> capRange (cteCap cte) = {} \<and> global_refs' s' \<subseteq> kernel_data_refs; \<nexists>irq. cteCap ctea = capability.IRQHandlerCap irq; ctea = CTE x1 x2; cref \<in> descendants_of' p (ctes_of s')\<rbrakk> \<Longrightarrow> False proof (prove)
goal (2 subgoals):
 1. \<And>cref ctea x1 x2. \<lbrakk>descendants_range_in' S p (ctes_of s'); S \<subseteq> capRange (cteCap cte); isUntypedCap (cteCap cte); valid_objs' s'; valid_mdb' s'; valid_pspace' s'; sch_act_wf (ksSchedulerAction s') s'; Invariants_H.valid_queues s'; sym_refs (state_refs_of' s'); if_live_then_nonz_cap' s'; if_unsafe_then_cap' s'; valid_idle' s'; valid_global_refs' s'; valid_arch_state' s'; valid_irq_node' (irq_node' s') s'; valid_irq_handlers' s'; valid_irq_states' s'; valid_machine_state' s'; irqs_masked' s'; valid_queues' s'; ct_not_inQ s'; ct_idle_or_in_cur_domain' s'; valid_pde_mappings' s'; pspace_domain_valid s'; ksCurDomain s' \<le> maxDomain; ksDomSchedule (KernelInit_H.newKernelState undefined) \<noteq> []; \<forall>x\<in>set (ksDomSchedule (KernelInit_H.newKernelState undefined)). dschDomain x \<le> maxDomain \<and> 0 < dschLength x; ksDomSchedule s' = ksDomSchedule (KernelInit_H.newKernelState undefined); ksDomScheduleIdx s' < length (ksDomSchedule (KernelInit_H.newKernelState undefined)); untyped_ranges_zero' s'; cur_tcb' s'; q \<in> S; ctes_of s' cref = Some ctea; P (cteCap ctea); q \<in> cte_refs' (cteCap ctea) (irq_node' s'); kernel_data_refs \<inter> capRange (cteCap cte) = {} \<and> global_refs' s' \<subseteq> kernel_data_refs; \<nexists>irq. cteCap ctea = capability.IRQHandlerCap irq; ctea = CTE x1 x2\<rbrakk> \<Longrightarrow> untyped_mdb' (ctes_of s')
 2. \<And>cref ctea x1 x2. \<lbrakk>descendants_range_in' S p (ctes_of s'); S \<subseteq> capRange (cteCap cte); isUntypedCap (cteCap cte); valid_objs' s'; valid_mdb' s'; valid_pspace' s'; sch_act_wf (ksSchedulerAction s') s'; Invariants_H.valid_queues s'; sym_refs (state_refs_of' s'); if_live_then_nonz_cap' s'; if_unsafe_then_cap' s'; valid_idle' s'; valid_global_refs' s'; valid_arch_state' s'; valid_irq_node' (irq_node' s') s'; valid_irq_handlers' s'; valid_irq_states' s'; valid_machine_state' s'; irqs_masked' s'; valid_queues' s'; ct_not_inQ s'; ct_idle_or_in_cur_domain' s'; valid_pde_mappings' s'; pspace_domain_valid s'; ksCurDomain s' \<le> maxDomain; ksDomSchedule (KernelInit_H.newKernelState undefined) \<noteq> []; \<forall>x\<in>set (ksDomSchedule (KernelInit_H.newKernelState undefined)). dschDomain x \<le> maxDomain \<and> 0 < dschLength x; ksDomSchedule s' = ksDomSchedule (KernelInit_H.newKernelState undefined); ksDomScheduleIdx s' < length (ksDomSchedule (KernelInit_H.newKernelState undefined)); untyped_ranges_zero' s'; cur_tcb' s'; q \<in> S; ctes_of s' cref = Some ctea; P (cteCap ctea); q \<in> cte_refs' (cteCap ctea) (irq_node' s'); kernel_data_refs \<inter> capRange (cteCap cte) = {} \<and> global_refs' s' \<subseteq> kernel_data_refs; \<nexists>irq. cteCap ctea = capability.IRQHandlerCap irq; ctea = CTE x1 x2; cref \<in> descendants_of' p (ctes_of s')\<rbrakk> \<Longrightarrow> False proof (prove)
goal (1 subgoal):
 1. \<And>cref ctea x1 x2. \<lbrakk>descendants_range_in' S p (ctes_of s'); S \<subseteq> capRange (cteCap cte); isUntypedCap (cteCap cte); valid_objs' s'; valid_mdb' s'; valid_pspace' s'; sch_act_wf (ksSchedulerAction s') s'; Invariants_H.valid_queues s'; sym_refs (state_refs_of' s'); if_live_then_nonz_cap' s'; if_unsafe_then_cap' s'; valid_idle' s'; valid_global_refs' s'; valid_arch_state' s'; valid_irq_node' (irq_node' s') s'; valid_irq_handlers' s'; valid_irq_states' s'; valid_machine_state' s'; irqs_masked' s'; valid_queues' s'; ct_not_inQ s'; ct_idle_or_in_cur_domain' s'; valid_pde_mappings' s'; pspace_domain_valid s'; ksCurDomain s' \<le> maxDomain; ksDomSchedule (KernelInit_H.newKernelState undefined) \<noteq> []; \<forall>x\<in>set (ksDomSchedule (KernelInit_H.newKernelState undefined)). dschDomain x \<le> maxDomain \<and> 0 < dschLength x; ksDomSchedule s' = ksDomSchedule (KernelInit_H.newKernelState undefined); ksDomScheduleIdx s' < length (ksDomSchedule (KernelInit_H.newKernelState undefined)); untyped_ranges_zero' s'; cur_tcb' s'; q \<in> S; ctes_of s' cref = Some ctea; P (cteCap ctea); q \<in> cte_refs' (cteCap ctea) (irq_node' s'); kernel_data_refs \<inter> capRange (cteCap cte) = {} \<and> global_refs' s' \<subseteq> kernel_data_refs; \<nexists>irq. cteCap ctea = capability.IRQHandlerCap irq; ctea = CTE x1 x2; cref \<in> descendants_of' p (ctes_of s')\<rbrakk> \<Longrightarrow> False proof (prove)
goal (1 subgoal):
 1. \<And>cref ctea x1 x2. \<lbrakk>S \<subseteq> capRange (cteCap cte); isUntypedCap (cteCap cte); valid_objs' s'; valid_mdb' s'; valid_pspace' s'; sch_act_wf (ksSchedulerAction s') s'; Invariants_H.valid_queues s'; sym_refs (state_refs_of' s'); if_live_then_nonz_cap' s'; if_unsafe_then_cap' s'; valid_idle' s'; valid_global_refs' s'; valid_arch_state' s'; valid_irq_node' (irq_node' s') s'; valid_irq_handlers' s'; valid_irq_states' s'; valid_machine_state' s'; irqs_masked' s'; valid_queues' s'; ct_not_inQ s'; ct_idle_or_in_cur_domain' s'; valid_pde_mappings' s'; pspace_domain_valid s'; ksCurDomain s' \<le> maxDomain; ksDomSchedule (KernelInit_H.newKernelState undefined) \<noteq> []; \<forall>x\<in>set (ksDomSchedule (KernelInit_H.newKernelState undefined)). dschDomain x \<le> maxDomain \<and> 0 < dschLength x; ksDomSchedule s' = ksDomSchedule (KernelInit_H.newKernelState undefined); ksDomScheduleIdx s' < length (ksDomSchedule (KernelInit_H.newKernelState undefined)); untyped_ranges_zero' s'; cur_tcb' s'; q \<in> S; ctes_of s' cref = Some ctea; P (cteCap ctea); q \<in> cte_refs' (cteCap ctea) (irq_node' s'); kernel_data_refs \<inter> capRange (cteCap cte) = {} \<and> global_refs' s' \<subseteq> kernel_data_refs; \<nexists>irq. cteCap ctea = capability.IRQHandlerCap irq; ctea = CTE x1 x2; cref \<in> descendants_of' p (ctes_of s'); capRange (cteCap ctea) \<inter> S = {}\<rbrakk> \<Longrightarrow> False proof (prove)
goal (1 subgoal):
 1. \<And>cref x1 x2. \<lbrakk>S \<subseteq> capRange (cteCap cte); isUntypedCap (cteCap cte); valid_objs' s'; valid_mdb' s'; valid_pspace' s'; sch_act_wf (ksSchedulerAction s') s'; Invariants_H.valid_queues s'; sym_refs (state_refs_of' s'); if_live_then_nonz_cap' s'; if_unsafe_then_cap' s'; valid_idle' s'; valid_global_refs' s'; valid_arch_state' s'; valid_irq_node' (irq_node' s') s'; valid_irq_handlers' s'; valid_irq_states' s'; valid_machine_state' s'; irqs_masked' s'; valid_queues' s'; ct_not_inQ s'; ct_idle_or_in_cur_domain' s'; valid_pde_mappings' s'; pspace_domain_valid s'; ksCurDomain s' \<le> maxDomain; ksDomSchedule (KernelInit_H.newKernelState undefined) \<noteq> []; \<forall>x\<in>set (ksDomSchedule (KernelInit_H.newKernelState undefined)). dschDomain x \<le> maxDomain \<and> 0 < dschLength x; ksDomSchedule s' = ksDomSchedule (KernelInit_H.newKernelState undefined); ksDomScheduleIdx s' < length (ksDomSchedule (KernelInit_H.newKernelState undefined)); untyped_ranges_zero' s'; cur_tcb' s'; q \<in> S; ctes_of s' cref = Some (CTE x1 x2); P x1; q \<in> cte_refs' x1 (irq_node' s'); \<forall>irq. x1 \<noteq> capability.IRQHandlerCap irq; cref \<in> descendants_of' p (ctes_of s'); capRange x1 \<inter> S = {}; kernel_data_refs \<inter> capRange (cteCap cte) = {}; global_refs' s' \<subseteq> kernel_data_refs\<rbrakk> \<Longrightarrow> False proof (prove)
goal (2 subgoals):
 1. \<And>cref x1 x2. \<lbrakk>S \<subseteq> capRange (cteCap cte); isUntypedCap (cteCap cte); valid_objs' s'; valid_mdb' s'; valid_pspace' s'; sch_act_wf (ksSchedulerAction s') s'; Invariants_H.valid_queues s'; sym_refs (state_refs_of' s'); if_live_then_nonz_cap' s'; if_unsafe_then_cap' s'; valid_idle' s'; valid_global_refs' s'; valid_arch_state' s'; valid_irq_node' (irq_node' s') s'; valid_irq_handlers' s'; valid_irq_states' s'; valid_machine_state' s'; irqs_masked' s'; valid_queues' s'; ct_not_inQ s'; ct_idle_or_in_cur_domain' s'; valid_pde_mappings' s'; pspace_domain_valid s'; ksCurDomain s' \<le> maxDomain; ksDomSchedule (KernelInit_H.newKernelState undefined) \<noteq> []; \<forall>x\<in>set (ksDomSchedule (KernelInit_H.newKernelState undefined)). dschDomain x \<le> maxDomain \<and> 0 < dschLength x; ksDomSchedule s' = ksDomSchedule (KernelInit_H.newKernelState undefined); ksDomScheduleIdx s' < length (ksDomSchedule (KernelInit_H.newKernelState undefined)); untyped_ranges_zero' s'; cur_tcb' s'; q \<in> S; ctes_of s' cref = Some (CTE x1 x2); P x1; q \<in> cte_refs' x1 (irq_node' s'); cref \<in> descendants_of' p (ctes_of s'); capRange x1 \<inter> S = {}; kernel_data_refs \<inter> capRange (cteCap cte) = {}; global_refs' s' \<subseteq> kernel_data_refs\<rbrakk> \<Longrightarrow> valid_cap' x1 (?s301 cref x1 x2)
 2. \<And>cref x1 x2. \<lbrakk>S \<subseteq> capRange (cteCap cte); isUntypedCap (cteCap cte); valid_objs' s'; valid_mdb' s'; valid_pspace' s'; sch_act_wf (ksSchedulerAction s') s'; Invariants_H.valid_queues s'; sym_refs (state_refs_of' s'); if_live_then_nonz_cap' s'; if_unsafe_then_cap' s'; valid_idle' s'; valid_global_refs' s'; valid_arch_state' s'; valid_irq_node' (irq_node' s') s'; valid_irq_handlers' s'; valid_irq_states' s'; valid_machine_state' s'; irqs_masked' s'; valid_queues' s'; ct_not_inQ s'; ct_idle_or_in_cur_domain' s'; valid_pde_mappings' s'; pspace_domain_valid s'; ksCurDomain s' \<le> maxDomain; ksDomSchedule (KernelInit_H.newKernelState undefined) \<noteq> []; \<forall>x\<in>set (ksDomSchedule (KernelInit_H.newKernelState undefined)). dschDomain x \<le> maxDomain \<and> 0 < dschLength x; ksDomSchedule s' = ksDomSchedule (KernelInit_H.newKernelState undefined); ksDomScheduleIdx s' < length (ksDomSchedule (KernelInit_H.newKernelState undefined)); untyped_ranges_zero' s'; cur_tcb' s'; q \<in> S; ctes_of s' cref = Some (CTE x1 x2); P x1; q \<in> cte_refs' x1 (irq_node' s'); cref \<in> descendants_of' p (ctes_of s'); capRange x1 \<inter> S = {}; kernel_data_refs \<inter> capRange (cteCap cte) = {}; global_refs' s' \<subseteq> kernel_data_refs; cte_refs' x1 (irq_node' s') \<subseteq> capRange x1\<rbrakk> \<Longrightarrow> False proof (prove)
goal (1 subgoal):
 1. \<And>cref x1 x2. \<lbrakk>S \<subseteq> capRange (cteCap cte); isUntypedCap (cteCap cte); valid_objs' s'; valid_mdb' s'; valid_pspace' s'; sch_act_wf (ksSchedulerAction s') s'; Invariants_H.valid_queues s'; sym_refs (state_refs_of' s'); if_live_then_nonz_cap' s'; if_unsafe_then_cap' s'; valid_idle' s'; valid_global_refs' s'; valid_arch_state' s'; valid_irq_node' (irq_node' s') s'; valid_irq_handlers' s'; valid_irq_states' s'; valid_machine_state' s'; irqs_masked' s'; valid_queues' s'; ct_not_inQ s'; ct_idle_or_in_cur_domain' s'; valid_pde_mappings' s'; pspace_domain_valid s'; ksCurDomain s' \<le> maxDomain; ksDomSchedule (KernelInit_H.newKernelState undefined) \<noteq> []; \<forall>x\<in>set (ksDomSchedule (KernelInit_H.newKernelState undefined)). dschDomain x \<le> maxDomain \<and> 0 < dschLength x; ksDomSchedule s' = ksDomSchedule (KernelInit_H.newKernelState undefined); ksDomScheduleIdx s' < length (ksDomSchedule (KernelInit_H.newKernelState undefined)); untyped_ranges_zero' s'; cur_tcb' s'; q \<in> S; ctes_of s' cref = Some (CTE x1 x2); P x1; q \<in> cte_refs' x1 (irq_node' s'); cref \<in> descendants_of' p (ctes_of s'); capRange x1 \<inter> S = {}; kernel_data_refs \<inter> capRange (cteCap cte) = {}; global_refs' s' \<subseteq> kernel_data_refs; cte_refs' x1 (irq_node' s') \<subseteq> capRange x1\<rbrakk> \<Longrightarrow> False proof (prove)
goal:
No subgoals!