theory Finalise_R

lemma unbindMaybeNotification_invs[wp]:
  "\<lbrace>invs'\<rbrace> unbindMaybeNotification ntfnptr \<lbrace>\<lambda>rv. invs'\<rbrace>" apply (simp add: unbindMaybeNotification_def invs'_def valid_state'_def) apply (rule hoare_seq_ext[OF _ get_ntfn_sp']) apply (rule hoare_pre) apply (wp sbn'_valid_pspace'_inv sbn_sch_act' sbn_valid_queues valid_irq_node_lift
             irqs_masked_lift setBoundNotification_ct_not_inQ
             untyped_ranges_zero_lift
             | wpc | clarsimp simp: cteCaps_of_def o_def)+ apply safe[1] defer 3 defer 7 apply (fold_subgoals (prefix))[8] subgoal premises prems using prems by (auto simp: pred_tcb_at' valid_pspace'_def projectKOs valid_obj'_def valid_ntfn'_def
                             ko_wp_at'_def
                      elim!: obj_atE' valid_objsE' if_live_then_nonz_capE'
                      split: option.splits ntfn.splits) apply (rule delta_sym_refs, assumption) apply (fold_subgoals (prefix))[2] subgoal premises prems using prems by (fastforce simp: symreftype_inverse' ntfn_q_refs_of'_def
                    split: ntfn.splits if_split_asm
                     dest!: ko_at_state_refs_ofD')+ apply (rule delta_sym_refs, assumption) apply (clarsimp split: if_split_asm) apply (frule ko_at_state_refs_ofD', simp) apply (clarsimp split: if_split_asm) apply (frule_tac P="(=) (Some ntfnptr)" in ntfn_bound_tcb_at', simp_all add: valid_pspace'_def)[1] subgoal by (fastforce simp: ntfn_q_refs_of'_def state_refs_of'_def tcb_ntfn_is_bound'_def
                          tcb_st_refs_of'_def
                   dest!: bound_tcb_at_state_refs_ofD'
                   split: ntfn.splits thread_state.splits) apply (frule ko_at_state_refs_ofD', simp) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>invs'\<rbrace> unbindMaybeNotification ntfnptr \<lbrace>\<lambda>rv. invs'\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>(\<lambda>s. valid_pspace' s \<and> sch_act_wf (ksSchedulerAction s) s \<and> Invariants_H.valid_queues s \<and> sym_refs (state_refs_of' s) \<and> if_live_then_nonz_cap' s \<and> if_unsafe_then_cap' s \<and> valid_idle' s \<and> valid_global_refs' s \<and> valid_arch_state' s \<and> valid_irq_node' (irq_node' s) s \<and> valid_irq_handlers' s \<and> valid_irq_states' s \<and> valid_machine_state' s \<and> irqs_masked' s \<and> valid_queues' s \<and> ct_not_inQ s \<and> ct_idle_or_in_cur_domain' s \<and> valid_pde_mappings' s \<and> pspace_domain_valid s \<and> ksCurDomain s \<le> maxDomain \<and> ksDomSchedule s \<noteq> [] \<and> (\<forall>x\<in>set (ksDomSchedule s). dschDomain x \<le> maxDomain \<and> 0 < dschLength x) \<and> ksDomSchedule s = ksDomSchedule (KernelInit_H.newKernelState undefined) \<and> ksDomScheduleIdx s < length (ksDomSchedule (KernelInit_H.newKernelState undefined)) \<and> untyped_ranges_zero' s) and cur_tcb'\<rbrace> do ntfn <- getNotification ntfnptr;
case ntfnBoundTCB ntfn of None \<Rightarrow> return () | Some t \<Rightarrow> do y <- setNotification ntfnptr (ntfnBoundTCB_update (\<lambda>_. None) ntfn);
setBoundNotification None t
od
od \<lbrace>\<lambda>rv. (\<lambda>s. valid_pspace' s \<and> sch_act_wf (ksSchedulerAction s) s \<and> Invariants_H.valid_queues s \<and> sym_refs (state_refs_of' s) \<and> if_live_then_nonz_cap' s \<and> if_unsafe_then_cap' s \<and> valid_idle' s \<and> valid_global_refs' s \<and> valid_arch_state' s \<and> valid_irq_node' (irq_node' s) s \<and> valid_irq_handlers' s \<and> valid_irq_states' s \<and> valid_machine_state' s \<and> irqs_masked' s \<and> valid_queues' s \<and> ct_not_inQ s \<and> ct_idle_or_in_cur_domain' s \<and> valid_pde_mappings' s \<and> pspace_domain_valid s \<and> ksCurDomain s \<le> maxDomain \<and> ksDomSchedule s \<noteq> [] \<and> (\<forall>x\<in>set (ksDomSchedule s). dschDomain x \<le> maxDomain \<and> 0 < dschLength x) \<and> ksDomSchedule s = ksDomSchedule (KernelInit_H.newKernelState undefined) \<and> ksDomScheduleIdx s < length (ksDomSchedule (KernelInit_H.newKernelState undefined)) \<and> untyped_ranges_zero' s) and cur_tcb'\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>ntfn. \<lbrace>(\<lambda>s. valid_pspace' s \<and> sch_act_wf (ksSchedulerAction s) s \<and> Invariants_H.valid_queues s \<and> sym_refs (state_refs_of' s) \<and> if_live_then_nonz_cap' s \<and> if_unsafe_then_cap' s \<and> valid_idle' s \<and> valid_global_refs' s \<and> valid_arch_state' s \<and> valid_irq_node' (irq_node' s) s \<and> valid_irq_handlers' s \<and> valid_irq_states' s \<and> valid_machine_state' s \<and> irqs_masked' s \<and> valid_queues' s \<and> ct_not_inQ s \<and> ct_idle_or_in_cur_domain' s \<and> valid_pde_mappings' s \<and> pspace_domain_valid s \<and> ksCurDomain s \<le> maxDomain \<and> ksDomSchedule s \<noteq> [] \<and> (\<forall>x\<in>set (ksDomSchedule s). dschDomain x \<le> maxDomain \<and> 0 < dschLength x) \<and> ksDomSchedule s = ksDomSchedule (KernelInit_H.newKernelState undefined) \<and> ksDomScheduleIdx s < length (ksDomSchedule (KernelInit_H.newKernelState undefined)) \<and> untyped_ranges_zero' s) and cur_tcb' and ko_at' ntfn ntfnptr\<rbrace> case ntfnBoundTCB ntfn of None \<Rightarrow> return () | Some t \<Rightarrow> do y <- setNotification ntfnptr (ntfnBoundTCB_update (\<lambda>_. None) ntfn);
setBoundNotification None t
od \<lbrace>\<lambda>rv. (\<lambda>s. valid_pspace' s \<and> sch_act_wf (ksSchedulerAction s) s \<and> Invariants_H.valid_queues s \<and> sym_refs (state_refs_of' s) \<and> if_live_then_nonz_cap' s \<and> if_unsafe_then_cap' s \<and> valid_idle' s \<and> valid_global_refs' s \<and> valid_arch_state' s \<and> valid_irq_node' (irq_node' s) s \<and> valid_irq_handlers' s \<and> valid_irq_states' s \<and> valid_machine_state' s \<and> irqs_masked' s \<and> valid_queues' s \<and> ct_not_inQ s \<and> ct_idle_or_in_cur_domain' s \<and> valid_pde_mappings' s \<and> pspace_domain_valid s \<and> ksCurDomain s \<le> maxDomain \<and> ksDomSchedule s \<noteq> [] \<and> (\<forall>x\<in>set (ksDomSchedule s). dschDomain x \<le> maxDomain \<and> 0 < dschLength x) \<and> ksDomSchedule s = ksDomSchedule (KernelInit_H.newKernelState undefined) \<and> ksDomScheduleIdx s < length (ksDomSchedule (KernelInit_H.newKernelState undefined)) \<and> untyped_ranges_zero' s) and cur_tcb'\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<And>ntfn. \<lbrace>?Q8 ntfn\<rbrace> case ntfnBoundTCB ntfn of None \<Rightarrow> return () | Some t \<Rightarrow> do y <- setNotification ntfnptr (ntfnBoundTCB_update (\<lambda>_. None) ntfn);
setBoundNotification None t
od \<lbrace>\<lambda>rv. (\<lambda>s. valid_pspace' s \<and> sch_act_wf (ksSchedulerAction s) s \<and> Invariants_H.valid_queues s \<and> sym_refs (state_refs_of' s) \<and> if_live_then_nonz_cap' s \<and> if_unsafe_then_cap' s \<and> valid_idle' s \<and> valid_global_refs' s \<and> valid_arch_state' s \<and> valid_irq_node' (irq_node' s) s \<and> valid_irq_handlers' s \<and> valid_irq_states' s \<and> valid_machine_state' s \<and> irqs_masked' s \<and> valid_queues' s \<and> ct_not_inQ s \<and> ct_idle_or_in_cur_domain' s \<and> valid_pde_mappings' s \<and> pspace_domain_valid s \<and> ksCurDomain s \<le> maxDomain \<and> ksDomSchedule s \<noteq> [] \<and> (\<forall>x\<in>set (ksDomSchedule s). dschDomain x \<le> maxDomain \<and> 0 < dschLength x) \<and> ksDomSchedule s = ksDomSchedule (KernelInit_H.newKernelState undefined) \<and> ksDomScheduleIdx s < length (ksDomSchedule (KernelInit_H.newKernelState undefined)) \<and> untyped_ranges_zero' s) and cur_tcb'\<rbrace>
 2. \<And>ntfn s. ((\<lambda>s. valid_pspace' s \<and> sch_act_wf (ksSchedulerAction s) s \<and> Invariants_H.valid_queues s \<and> sym_refs (state_refs_of' s) \<and> if_live_then_nonz_cap' s \<and> if_unsafe_then_cap' s \<and> valid_idle' s \<and> valid_global_refs' s \<and> valid_arch_state' s \<and> valid_irq_node' (irq_node' s) s \<and> valid_irq_handlers' s \<and> valid_irq_states' s \<and> valid_machine_state' s \<and> irqs_masked' s \<and> valid_queues' s \<and> ct_not_inQ s \<and> ct_idle_or_in_cur_domain' s \<and> valid_pde_mappings' s \<and> pspace_domain_valid s \<and> ksCurDomain s \<le> maxDomain \<and> ksDomSchedule s \<noteq> [] \<and> (\<forall>x\<in>set (ksDomSchedule s). dschDomain x \<le> maxDomain \<and> 0 < dschLength x) \<and> ksDomSchedule s = ksDomSchedule (KernelInit_H.newKernelState undefined) \<and> ksDomScheduleIdx s < length (ksDomSchedule (KernelInit_H.newKernelState undefined)) \<and> untyped_ranges_zero' s) and cur_tcb' and ko_at' ntfn ntfnptr) s \<Longrightarrow> ?Q8 ntfn s proof (prove)
goal (1 subgoal):
 1. \<And>ntfn s x. \<lbrakk>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_inv (\<lambda>x. map_option cteCap (ctes_of s x)) (gsUntypedZeroRanges s); cur_tcb' s; ko_at' ntfn ntfnptr s\<rbrakk> \<Longrightarrow> (x = ntfnptr \<longrightarrow> ntfnBoundTCB ntfn = Some ntfnptr \<longrightarrow> valid_ntfn' (ntfnBoundTCB_update (\<lambda>_. None) ntfn) s \<and> tcb_at' ntfnptr s \<and> sym_refs (\<lambda>a. if a = ntfnptr then {r \<in> ntfn_q_refs_of' (ntfnObj ntfn). snd r \<noteq> TCBBound} else state_refs_of' s a) \<and> ((\<exists>ts. ntfnObj ntfn = Structures_H.ntfn.WaitingNtfn ts) \<longrightarrow> ex_nonz_cap_to' ntfnptr s) \<and> valid_ntfn' (ntfnBoundTCB_update (\<lambda>_. None) ntfn) s) \<and> (x \<noteq> ntfnptr \<longrightarrow> ntfnBoundTCB ntfn = Some x \<longrightarrow> valid_ntfn' (ntfnBoundTCB_update (\<lambda>_. None) ntfn) s \<and> tcb_at' x s \<and> sym_refs (\<lambda>a. if a = x then {r \<in> state_refs_of' s x. snd r \<noteq> TCBBound} else if a = ntfnptr then ntfn_q_refs_of' (ntfnObj ntfn) else state_refs_of' s a) \<and> ((\<exists>ts. ntfnObj ntfn = Structures_H.ntfn.WaitingNtfn ts) \<longrightarrow> ex_nonz_cap_to' ntfnptr s) \<and> valid_ntfn' (ntfnBoundTCB_update (\<lambda>_. None) ntfn) s) proof (prove)
goal (10 subgoals):
 1. \<And>ntfn s x. \<lbrakk>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_inv (\<lambda>x. map_option cteCap (ctes_of s x)) (gsUntypedZeroRanges s); cur_tcb' s; ko_at' ntfn ntfnptr s; ntfnBoundTCB ntfn = Some ntfnptr\<rbrakk> \<Longrightarrow> valid_ntfn' (ntfnBoundTCB_update (\<lambda>_. None) ntfn) s
 2. \<And>ntfn s x. \<lbrakk>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_inv (\<lambda>x. map_option cteCap (ctes_of s x)) (gsUntypedZeroRanges s); cur_tcb' s; ko_at' ntfn ntfnptr s; ntfnBoundTCB ntfn = Some ntfnptr\<rbrakk> \<Longrightarrow> tcb_at' ntfnptr s
 3. \<And>ntfn s x. \<lbrakk>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_inv (\<lambda>x. map_option cteCap (ctes_of s x)) (gsUntypedZeroRanges s); cur_tcb' s; ko_at' ntfn ntfnptr s; ntfnBoundTCB ntfn = Some ntfnptr\<rbrakk> \<Longrightarrow> sym_refs (\<lambda>a. if a = ntfnptr then {r \<in> ntfn_q_refs_of' (ntfnObj ntfn). snd r \<noteq> TCBBound} else state_refs_of' s a)
 4. \<And>ntfn s x ts. \<lbrakk>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_inv (\<lambda>x. map_option cteCap (ctes_of s x)) (gsUntypedZeroRanges s); cur_tcb' s; ko_at' ntfn ntfnptr s; ntfnBoundTCB ntfn = Some ntfnptr; ntfnObj ntfn = Structures_H.ntfn.WaitingNtfn ts\<rbrakk> \<Longrightarrow> ex_nonz_cap_to' ntfnptr s
 5. \<And>ntfn s x. \<lbrakk>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_inv (\<lambda>x. map_option cteCap (ctes_of s x)) (gsUntypedZeroRanges s); cur_tcb' s; ko_at' ntfn ntfnptr s; ntfnBoundTCB ntfn = Some ntfnptr\<rbrakk> \<Longrightarrow> valid_ntfn' (ntfnBoundTCB_update (\<lambda>_. None) ntfn) s
 6. \<And>ntfn s x. \<lbrakk>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_inv (\<lambda>x. map_option cteCap (ctes_of s x)) (gsUntypedZeroRanges s); cur_tcb' s; ko_at' ntfn ntfnptr s; x \<noteq> ntfnptr; ntfnBoundTCB ntfn = Some x\<rbrakk> \<Longrightarrow> valid_ntfn' (ntfnBoundTCB_update (\<lambda>_. None) ntfn) s
 7. \<And>ntfn s x. \<lbrakk>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_inv (\<lambda>x. map_option cteCap (ctes_of s x)) (gsUntypedZeroRanges s); cur_tcb' s; ko_at' ntfn ntfnptr s; x \<noteq> ntfnptr; ntfnBoundTCB ntfn = Some x\<rbrakk> \<Longrightarrow> tcb_at' x s
 8. \<And>ntfn s x. \<lbrakk>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_inv (\<lambda>x. map_option cteCap (ctes_of s x)) (gsUntypedZeroRanges s); cur_tcb' s; ko_at' ntfn ntfnptr s; x \<noteq> ntfnptr; ntfnBoundTCB ntfn = Some x\<rbrakk> \<Longrightarrow> sym_refs (\<lambda>a. if a = x then {r \<in> state_refs_of' s x. snd r \<noteq> TCBBound} else if a = ntfnptr then ntfn_q_refs_of' (ntfnObj ntfn) else state_refs_of' s a)
 9. \<And>ntfn s x ts. \<lbrakk>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_inv (\<lambda>x. map_option cteCap (ctes_of s x)) (gsUntypedZeroRanges s); cur_tcb' s; ko_at' ntfn ntfnptr s; x \<noteq> ntfnptr; ntfnBoundTCB ntfn = Some x; ntfnObj ntfn = Structures_H.ntfn.WaitingNtfn ts\<rbrakk> \<Longrightarrow> ex_nonz_cap_to' ntfnptr s
 10. \<And>ntfn s x. \<lbrakk>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_inv (\<lambda>x. map_option cteCap (ctes_of s x)) (gsUntypedZeroRanges s); cur_tcb' s; ko_at' ntfn ntfnptr s; x \<noteq> ntfnptr; ntfnBoundTCB ntfn = Some x\<rbrakk> \<Longrightarrow> valid_ntfn' (ntfnBoundTCB_update (\<lambda>_. None) ntfn) s proof (prove)
goal (10 subgoals):
 1. \<And>ntfn s x. \<lbrakk>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_inv (\<lambda>x. map_option cteCap (ctes_of s x)) (gsUntypedZeroRanges s); cur_tcb' s; ko_at' ntfn ntfnptr s; ntfnBoundTCB ntfn = Some ntfnptr\<rbrakk> \<Longrightarrow> valid_ntfn' (ntfnBoundTCB_update (\<lambda>_. None) ntfn) s
 2. \<And>ntfn s x. \<lbrakk>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_inv (\<lambda>x. map_option cteCap (ctes_of s x)) (gsUntypedZeroRanges s); cur_tcb' s; ko_at' ntfn ntfnptr s; ntfnBoundTCB ntfn = Some ntfnptr\<rbrakk> \<Longrightarrow> tcb_at' ntfnptr s
 3. \<And>ntfn s x ts. \<lbrakk>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_inv (\<lambda>x. map_option cteCap (ctes_of s x)) (gsUntypedZeroRanges s); cur_tcb' s; ko_at' ntfn ntfnptr s; ntfnBoundTCB ntfn = Some ntfnptr; ntfnObj ntfn = Structures_H.ntfn.WaitingNtfn ts\<rbrakk> \<Longrightarrow> ex_nonz_cap_to' ntfnptr s
 4. \<And>ntfn s x. \<lbrakk>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_inv (\<lambda>x. map_option cteCap (ctes_of s x)) (gsUntypedZeroRanges s); cur_tcb' s; ko_at' ntfn ntfnptr s; ntfnBoundTCB ntfn = Some ntfnptr\<rbrakk> \<Longrightarrow> valid_ntfn' (ntfnBoundTCB_update (\<lambda>_. None) ntfn) s
 5. \<And>ntfn s x. \<lbrakk>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_inv (\<lambda>x. map_option cteCap (ctes_of s x)) (gsUntypedZeroRanges s); cur_tcb' s; ko_at' ntfn ntfnptr s; x \<noteq> ntfnptr; ntfnBoundTCB ntfn = Some x\<rbrakk> \<Longrightarrow> valid_ntfn' (ntfnBoundTCB_update (\<lambda>_. None) ntfn) s
 6. \<And>ntfn s x. \<lbrakk>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_inv (\<lambda>x. map_option cteCap (ctes_of s x)) (gsUntypedZeroRanges s); cur_tcb' s; ko_at' ntfn ntfnptr s; x \<noteq> ntfnptr; ntfnBoundTCB ntfn = Some x\<rbrakk> \<Longrightarrow> tcb_at' x s
 7. \<And>ntfn s x. \<lbrakk>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_inv (\<lambda>x. map_option cteCap (ctes_of s x)) (gsUntypedZeroRanges s); cur_tcb' s; ko_at' ntfn ntfnptr s; x \<noteq> ntfnptr; ntfnBoundTCB ntfn = Some x\<rbrakk> \<Longrightarrow> sym_refs (\<lambda>a. if a = x then {r \<in> state_refs_of' s x. snd r \<noteq> TCBBound} else if a = ntfnptr then ntfn_q_refs_of' (ntfnObj ntfn) else state_refs_of' s a)
 8. \<And>ntfn s x ts. \<lbrakk>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_inv (\<lambda>x. map_option cteCap (ctes_of s x)) (gsUntypedZeroRanges s); cur_tcb' s; ko_at' ntfn ntfnptr s; x \<noteq> ntfnptr; ntfnBoundTCB ntfn = Some x; ntfnObj ntfn = Structures_H.ntfn.WaitingNtfn ts\<rbrakk> \<Longrightarrow> ex_nonz_cap_to' ntfnptr s
 9. \<And>ntfn s x. \<lbrakk>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_inv (\<lambda>x. map_option cteCap (ctes_of s x)) (gsUntypedZeroRanges s); cur_tcb' s; ko_at' ntfn ntfnptr s; x \<noteq> ntfnptr; ntfnBoundTCB ntfn = Some x\<rbrakk> \<Longrightarrow> valid_ntfn' (ntfnBoundTCB_update (\<lambda>_. None) ntfn) s
 10. \<And>ntfn s x. \<lbrakk>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_inv (\<lambda>x. map_option cteCap (ctes_of s x)) (gsUntypedZeroRanges s); cur_tcb' s; ko_at' ntfn ntfnptr s; ntfnBoundTCB ntfn = Some ntfnptr\<rbrakk> \<Longrightarrow> sym_refs (\<lambda>a. if a = ntfnptr then {r \<in> ntfn_q_refs_of' (ntfnObj ntfn). snd r \<noteq> TCBBound} else state_refs_of' s a) proof (prove)
goal (10 subgoals):
 1. \<And>ntfn s x. \<lbrakk>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_inv (\<lambda>x. map_option cteCap (ctes_of s x)) (gsUntypedZeroRanges s); cur_tcb' s; ko_at' ntfn ntfnptr s; ntfnBoundTCB ntfn = Some ntfnptr\<rbrakk> \<Longrightarrow> valid_ntfn' (ntfnBoundTCB_update (\<lambda>_. None) ntfn) s
 2. \<And>ntfn s x. \<lbrakk>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_inv (\<lambda>x. map_option cteCap (ctes_of s x)) (gsUntypedZeroRanges s); cur_tcb' s; ko_at' ntfn ntfnptr s; ntfnBoundTCB ntfn = Some ntfnptr\<rbrakk> \<Longrightarrow> tcb_at' ntfnptr s
 3. \<And>ntfn s x ts. \<lbrakk>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_inv (\<lambda>x. map_option cteCap (ctes_of s x)) (gsUntypedZeroRanges s); cur_tcb' s; ko_at' ntfn ntfnptr s; ntfnBoundTCB ntfn = Some ntfnptr; ntfnObj ntfn = Structures_H.ntfn.WaitingNtfn ts\<rbrakk> \<Longrightarrow> ex_nonz_cap_to' ntfnptr s
 4. \<And>ntfn s x. \<lbrakk>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_inv (\<lambda>x. map_option cteCap (ctes_of s x)) (gsUntypedZeroRanges s); cur_tcb' s; ko_at' ntfn ntfnptr s; ntfnBoundTCB ntfn = Some ntfnptr\<rbrakk> \<Longrightarrow> valid_ntfn' (ntfnBoundTCB_update (\<lambda>_. None) ntfn) s
 5. \<And>ntfn s x. \<lbrakk>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_inv (\<lambda>x. map_option cteCap (ctes_of s x)) (gsUntypedZeroRanges s); cur_tcb' s; ko_at' ntfn ntfnptr s; x \<noteq> ntfnptr; ntfnBoundTCB ntfn = Some x\<rbrakk> \<Longrightarrow> valid_ntfn' (ntfnBoundTCB_update (\<lambda>_. None) ntfn) s
 6. \<And>ntfn s x. \<lbrakk>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_inv (\<lambda>x. map_option cteCap (ctes_of s x)) (gsUntypedZeroRanges s); cur_tcb' s; ko_at' ntfn ntfnptr s; x \<noteq> ntfnptr; ntfnBoundTCB ntfn = Some x\<rbrakk> \<Longrightarrow> tcb_at' x s
 7. \<And>ntfn s x ts. \<lbrakk>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_inv (\<lambda>x. map_option cteCap (ctes_of s x)) (gsUntypedZeroRanges s); cur_tcb' s; ko_at' ntfn ntfnptr s; x \<noteq> ntfnptr; ntfnBoundTCB ntfn = Some x; ntfnObj ntfn = Structures_H.ntfn.WaitingNtfn ts\<rbrakk> \<Longrightarrow> ex_nonz_cap_to' ntfnptr s
 8. \<And>ntfn s x. \<lbrakk>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_inv (\<lambda>x. map_option cteCap (ctes_of s x)) (gsUntypedZeroRanges s); cur_tcb' s; ko_at' ntfn ntfnptr s; x \<noteq> ntfnptr; ntfnBoundTCB ntfn = Some x\<rbrakk> \<Longrightarrow> valid_ntfn' (ntfnBoundTCB_update (\<lambda>_. None) ntfn) s
 9. \<And>ntfn s x. \<lbrakk>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_inv (\<lambda>x. map_option cteCap (ctes_of s x)) (gsUntypedZeroRanges s); cur_tcb' s; ko_at' ntfn ntfnptr s; ntfnBoundTCB ntfn = Some ntfnptr\<rbrakk> \<Longrightarrow> sym_refs (\<lambda>a. if a = ntfnptr then {r \<in> ntfn_q_refs_of' (ntfnObj ntfn). snd r \<noteq> TCBBound} else state_refs_of' s a)
 10. \<And>ntfn s x. \<lbrakk>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_inv (\<lambda>x. map_option cteCap (ctes_of s x)) (gsUntypedZeroRanges s); cur_tcb' s; ko_at' ntfn ntfnptr s; x \<noteq> ntfnptr; ntfnBoundTCB ntfn = Some x\<rbrakk> \<Longrightarrow> sym_refs (\<lambda>a. if a = x then {r \<in> state_refs_of' s x. snd r \<noteq> TCBBound} else if a = ntfnptr then ntfn_q_refs_of' (ntfnObj ntfn) else state_refs_of' s a) proof (prove)
goal (3 subgoals):
 1. \<And>ntfn s x. \<lbrakk>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_inv (\<lambda>x. map_option cteCap (ctes_of s x)) (gsUntypedZeroRanges s); cur_tcb' s; ko_at' ntfn ntfnptr s\<rbrakk> \<Longrightarrow> (ntfnBoundTCB ntfn = Some ntfnptr \<Longrightarrow> valid_ntfn' (ntfnBoundTCB_update (\<lambda>_. None) ntfn) s) &&& (ntfnBoundTCB ntfn = Some ntfnptr \<Longrightarrow> tcb_at' ntfnptr s) &&& (\<And>ts. \<lbrakk>ntfnBoundTCB ntfn = Some ntfnptr; ntfnObj ntfn = Structures_H.ntfn.WaitingNtfn ts\<rbrakk> \<Longrightarrow> ex_nonz_cap_to' ntfnptr s) &&& (ntfnBoundTCB ntfn = Some ntfnptr \<Longrightarrow> valid_ntfn' (ntfnBoundTCB_update (\<lambda>_. None) ntfn) s) &&& (\<lbrakk>x \<noteq> ntfnptr; ntfnBoundTCB ntfn = Some x\<rbrakk> \<Longrightarrow> valid_ntfn' (ntfnBoundTCB_update (\<lambda>_. None) ntfn) s) &&& (\<lbrakk>x \<noteq> ntfnptr; ntfnBoundTCB ntfn = Some x\<rbrakk> \<Longrightarrow> tcb_at' x s) &&& (\<And>ts. \<lbrakk>x \<noteq> ntfnptr; ntfnBoundTCB ntfn = Some x; ntfnObj ntfn = Structures_H.ntfn.WaitingNtfn ts\<rbrakk> \<Longrightarrow> ex_nonz_cap_to' ntfnptr s) &&& (\<lbrakk>x \<noteq> ntfnptr; ntfnBoundTCB ntfn = Some x\<rbrakk> \<Longrightarrow> valid_ntfn' (ntfnBoundTCB_update (\<lambda>_. None) ntfn) s)
 2. \<And>ntfn s x. \<lbrakk>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_inv (\<lambda>x. map_option cteCap (ctes_of s x)) (gsUntypedZeroRanges s); cur_tcb' s; ko_at' ntfn ntfnptr s; ntfnBoundTCB ntfn = Some ntfnptr\<rbrakk> \<Longrightarrow> sym_refs (\<lambda>a. if a = ntfnptr then {r \<in> ntfn_q_refs_of' (ntfnObj ntfn). snd r \<noteq> TCBBound} else state_refs_of' s a)
 3. \<And>ntfn s x. \<lbrakk>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_inv (\<lambda>x. map_option cteCap (ctes_of s x)) (gsUntypedZeroRanges s); cur_tcb' s; ko_at' ntfn ntfnptr s; x \<noteq> ntfnptr; ntfnBoundTCB ntfn = Some x\<rbrakk> \<Longrightarrow> sym_refs (\<lambda>a. if a = x then {r \<in> state_refs_of' s x. snd r \<noteq> TCBBound} else if a = ntfnptr then ntfn_q_refs_of' (ntfnObj ntfn) else state_refs_of' s a) proof (prove)
goal (1 subgoal):
 1. (ntfnBoundTCB ntfn_ = Some ntfnptr \<Longrightarrow> valid_ntfn' (ntfnBoundTCB_update (\<lambda>_. None) ntfn_) s_) &&& (ntfnBoundTCB ntfn_ = Some ntfnptr \<Longrightarrow> tcb_at' ntfnptr s_) &&& (\<And>ts. \<lbrakk>ntfnBoundTCB ntfn_ = Some ntfnptr; ntfnObj ntfn_ = Structures_H.ntfn.WaitingNtfn ts\<rbrakk> \<Longrightarrow> ex_nonz_cap_to' ntfnptr s_) &&& (ntfnBoundTCB ntfn_ = Some ntfnptr \<Longrightarrow> valid_ntfn' (ntfnBoundTCB_update (\<lambda>_. None) ntfn_) s_) &&& (\<lbrakk>x_ \<noteq> ntfnptr; ntfnBoundTCB ntfn_ = Some x_\<rbrakk> \<Longrightarrow> valid_ntfn' (ntfnBoundTCB_update (\<lambda>_. None) ntfn_) s_) &&& (\<lbrakk>x_ \<noteq> ntfnptr; ntfnBoundTCB ntfn_ = Some x_\<rbrakk> \<Longrightarrow> tcb_at' x_ s_) &&& (\<And>ts. \<lbrakk>x_ \<noteq> ntfnptr; ntfnBoundTCB ntfn_ = Some x_; ntfnObj ntfn_ = Structures_H.ntfn.WaitingNtfn ts\<rbrakk> \<Longrightarrow> ex_nonz_cap_to' ntfnptr s_) &&& (\<lbrakk>x_ \<noteq> ntfnptr; ntfnBoundTCB ntfn_ = Some x_\<rbrakk> \<Longrightarrow> valid_ntfn' (ntfnBoundTCB_update (\<lambda>_. None) ntfn_) s_) proof (prove)
using this:
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_inv (\<lambda>x. map_option cteCap (ctes_of s_ x)) (gsUntypedZeroRanges s_)
cur_tcb' s_
ko_at' ntfn_ ntfnptr s_

goal (1 subgoal):
 1. (ntfnBoundTCB ntfn_ = Some ntfnptr \<Longrightarrow> valid_ntfn' (ntfnBoundTCB_update (\<lambda>_. None) ntfn_) s_) &&& (ntfnBoundTCB ntfn_ = Some ntfnptr \<Longrightarrow> tcb_at' ntfnptr s_) &&& (\<And>ts. \<lbrakk>ntfnBoundTCB ntfn_ = Some ntfnptr; ntfnObj ntfn_ = Structures_H.ntfn.WaitingNtfn ts\<rbrakk> \<Longrightarrow> ex_nonz_cap_to' ntfnptr s_) &&& (ntfnBoundTCB ntfn_ = Some ntfnptr \<Longrightarrow> valid_ntfn' (ntfnBoundTCB_update (\<lambda>_. None) ntfn_) s_) &&& (\<lbrakk>x_ \<noteq> ntfnptr; ntfnBoundTCB ntfn_ = Some x_\<rbrakk> \<Longrightarrow> valid_ntfn' (ntfnBoundTCB_update (\<lambda>_. None) ntfn_) s_) &&& (\<lbrakk>x_ \<noteq> ntfnptr; ntfnBoundTCB ntfn_ = Some x_\<rbrakk> \<Longrightarrow> tcb_at' x_ s_) &&& (\<And>ts. \<lbrakk>x_ \<noteq> ntfnptr; ntfnBoundTCB ntfn_ = Some x_; ntfnObj ntfn_ = Structures_H.ntfn.WaitingNtfn ts\<rbrakk> \<Longrightarrow> ex_nonz_cap_to' ntfnptr s_) &&& (\<lbrakk>x_ \<noteq> ntfnptr; ntfnBoundTCB ntfn_ = Some x_\<rbrakk> \<Longrightarrow> valid_ntfn' (ntfnBoundTCB_update (\<lambda>_. None) ntfn_) s_) proof (prove)
goal (2 subgoals):
 1. \<And>ntfn s x. \<lbrakk>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_inv (\<lambda>x. map_option cteCap (ctes_of s x)) (gsUntypedZeroRanges s); cur_tcb' s; ko_at' ntfn ntfnptr s; ntfnBoundTCB ntfn = Some ntfnptr\<rbrakk> \<Longrightarrow> sym_refs (\<lambda>a. if a = ntfnptr then {r \<in> ntfn_q_refs_of' (ntfnObj ntfn). snd r \<noteq> TCBBound} else state_refs_of' s a)
 2. \<And>ntfn s x. \<lbrakk>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_inv (\<lambda>x. map_option cteCap (ctes_of s x)) (gsUntypedZeroRanges s); cur_tcb' s; ko_at' ntfn ntfnptr s; x \<noteq> ntfnptr; ntfnBoundTCB ntfn = Some x\<rbrakk> \<Longrightarrow> sym_refs (\<lambda>a. if a = x then {r \<in> state_refs_of' s x. snd r \<noteq> TCBBound} else if a = ntfnptr then ntfn_q_refs_of' (ntfnObj ntfn) else state_refs_of' s a) proof (prove)
goal (3 subgoals):
 1. \<And>ntfn s x xa y tp. \<lbrakk>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_inv (\<lambda>x. map_option cteCap (ctes_of s x)) (gsUntypedZeroRanges s); cur_tcb' s; ko_at' ntfn ntfnptr s; ntfnBoundTCB ntfn = Some ntfnptr; (y, tp) \<in> (if xa = ntfnptr then {r \<in> ntfn_q_refs_of' (ntfnObj ntfn). snd r \<noteq> TCBBound} else state_refs_of' s xa); (y, tp) \<notin> state_refs_of' s xa\<rbrakk> \<Longrightarrow> (xa, symreftype tp) \<in> (if y = ntfnptr then {r \<in> ntfn_q_refs_of' (ntfnObj ntfn). snd r \<noteq> TCBBound} else state_refs_of' s y)
 2. \<And>ntfn s x xa y tp. \<lbrakk>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_inv (\<lambda>x. map_option cteCap (ctes_of s x)) (gsUntypedZeroRanges s); cur_tcb' s; ko_at' ntfn ntfnptr s; ntfnBoundTCB ntfn = Some ntfnptr; (y, tp) \<in> state_refs_of' s xa; (y, tp) \<notin> (if xa = ntfnptr then {r \<in> ntfn_q_refs_of' (ntfnObj ntfn). snd r \<noteq> TCBBound} else state_refs_of' s xa)\<rbrakk> \<Longrightarrow> (xa, symreftype tp) \<notin> (if y = ntfnptr then {r \<in> ntfn_q_refs_of' (ntfnObj ntfn). snd r \<noteq> TCBBound} else state_refs_of' s y)
 3. \<And>ntfn s x. \<lbrakk>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_inv (\<lambda>x. map_option cteCap (ctes_of s x)) (gsUntypedZeroRanges s); cur_tcb' s; ko_at' ntfn ntfnptr s; x \<noteq> ntfnptr; ntfnBoundTCB ntfn = Some x\<rbrakk> \<Longrightarrow> sym_refs (\<lambda>a. if a = x then {r \<in> state_refs_of' s x. snd r \<noteq> TCBBound} else if a = ntfnptr then ntfn_q_refs_of' (ntfnObj ntfn) else state_refs_of' s a) proof (prove)
goal (2 subgoals):
 1. \<And>ntfn s x xa y tp. \<lbrakk>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_inv (\<lambda>x. map_option cteCap (ctes_of s x)) (gsUntypedZeroRanges s); cur_tcb' s; ko_at' ntfn ntfnptr s; ntfnBoundTCB ntfn = Some ntfnptr\<rbrakk> \<Longrightarrow> (\<lbrakk>(y, tp) \<in> (if xa = ntfnptr then {r \<in> ntfn_q_refs_of' (ntfnObj ntfn). snd r \<noteq> TCBBound} else state_refs_of' s xa); (y, tp) \<notin> state_refs_of' s xa\<rbrakk> \<Longrightarrow> (xa, symreftype tp) \<in> (if y = ntfnptr then {r \<in> ntfn_q_refs_of' (ntfnObj ntfn). snd r \<noteq> TCBBound} else state_refs_of' s y)) &&& (\<lbrakk>(y, tp) \<in> state_refs_of' s xa; (y, tp) \<notin> (if xa = ntfnptr then {r \<in> ntfn_q_refs_of' (ntfnObj ntfn). snd r \<noteq> TCBBound} else state_refs_of' s xa)\<rbrakk> \<Longrightarrow> (xa, symreftype tp) \<notin> (if y = ntfnptr then {r \<in> ntfn_q_refs_of' (ntfnObj ntfn). snd r \<noteq> TCBBound} else state_refs_of' s y))
 2. \<And>ntfn s x. \<lbrakk>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_inv (\<lambda>x. map_option cteCap (ctes_of s x)) (gsUntypedZeroRanges s); cur_tcb' s; ko_at' ntfn ntfnptr s; x \<noteq> ntfnptr; ntfnBoundTCB ntfn = Some x\<rbrakk> \<Longrightarrow> sym_refs (\<lambda>a. if a = x then {r \<in> state_refs_of' s x. snd r \<noteq> TCBBound} else if a = ntfnptr then ntfn_q_refs_of' (ntfnObj ntfn) else state_refs_of' s a) proof (prove)
goal (1 subgoal):
 1. (\<lbrakk>(y_, tp_) \<in> (if xa_ = ntfnptr then {r \<in> ntfn_q_refs_of' (ntfnObj ntfn_). snd r \<noteq> TCBBound} else state_refs_of' s_ xa_); (y_, tp_) \<notin> state_refs_of' s_ xa_\<rbrakk> \<Longrightarrow> (xa_, symreftype tp_) \<in> (if y_ = ntfnptr then {r \<in> ntfn_q_refs_of' (ntfnObj ntfn_). snd r \<noteq> TCBBound} else state_refs_of' s_ y_)) &&& (\<lbrakk>(y_, tp_) \<in> state_refs_of' s_ xa_; (y_, tp_) \<notin> (if xa_ = ntfnptr then {r \<in> ntfn_q_refs_of' (ntfnObj ntfn_). snd r \<noteq> TCBBound} else state_refs_of' s_ xa_)\<rbrakk> \<Longrightarrow> (xa_, symreftype tp_) \<notin> (if y_ = ntfnptr then {r \<in> ntfn_q_refs_of' (ntfnObj ntfn_). snd r \<noteq> TCBBound} else state_refs_of' s_ y_)) proof (prove)
using this:
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_inv (\<lambda>x. map_option cteCap (ctes_of s_ x)) (gsUntypedZeroRanges s_)
cur_tcb' s_
ko_at' ntfn_ ntfnptr s_
ntfnBoundTCB ntfn_ = Some ntfnptr

goal (1 subgoal):
 1. (\<lbrakk>(y_, tp_) \<in> (if xa_ = ntfnptr then {r \<in> ntfn_q_refs_of' (ntfnObj ntfn_). snd r \<noteq> TCBBound} else state_refs_of' s_ xa_); (y_, tp_) \<notin> state_refs_of' s_ xa_\<rbrakk> \<Longrightarrow> (xa_, symreftype tp_) \<in> (if y_ = ntfnptr then {r \<in> ntfn_q_refs_of' (ntfnObj ntfn_). snd r \<noteq> TCBBound} else state_refs_of' s_ y_)) &&& (\<lbrakk>(y_, tp_) \<in> state_refs_of' s_ xa_; (y_, tp_) \<notin> (if xa_ = ntfnptr then {r \<in> ntfn_q_refs_of' (ntfnObj ntfn_). snd r \<noteq> TCBBound} else state_refs_of' s_ xa_)\<rbrakk> \<Longrightarrow> (xa_, symreftype tp_) \<notin> (if y_ = ntfnptr then {r \<in> ntfn_q_refs_of' (ntfnObj ntfn_). snd r \<noteq> TCBBound} else state_refs_of' s_ y_)) proof (prove)
goal (1 subgoal):
 1. \<And>ntfn s x. \<lbrakk>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_inv (\<lambda>x. map_option cteCap (ctes_of s x)) (gsUntypedZeroRanges s); cur_tcb' s; ko_at' ntfn ntfnptr s; x \<noteq> ntfnptr; ntfnBoundTCB ntfn = Some x\<rbrakk> \<Longrightarrow> sym_refs (\<lambda>a. if a = x then {r \<in> state_refs_of' s x. snd r \<noteq> TCBBound} else if a = ntfnptr then ntfn_q_refs_of' (ntfnObj ntfn) else state_refs_of' s a) proof (prove)
goal (2 subgoals):
 1. \<And>ntfn s x xa y tp. \<lbrakk>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_inv (\<lambda>x. map_option cteCap (ctes_of s x)) (gsUntypedZeroRanges s); cur_tcb' s; ko_at' ntfn ntfnptr s; x \<noteq> ntfnptr; ntfnBoundTCB ntfn = Some x; (y, tp) \<in> (if xa = x then {r \<in> state_refs_of' s x. snd r \<noteq> TCBBound} else if xa = ntfnptr then ntfn_q_refs_of' (ntfnObj ntfn) else state_refs_of' s xa); (y, tp) \<notin> state_refs_of' s xa\<rbrakk> \<Longrightarrow> (xa, symreftype tp) \<in> (if y = x then {r \<in> state_refs_of' s x. snd r \<noteq> TCBBound} else if y = ntfnptr then ntfn_q_refs_of' (ntfnObj ntfn) else state_refs_of' s y)
 2. \<And>ntfn s x xa y tp. \<lbrakk>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_inv (\<lambda>x. map_option cteCap (ctes_of s x)) (gsUntypedZeroRanges s); cur_tcb' s; ko_at' ntfn ntfnptr s; x \<noteq> ntfnptr; ntfnBoundTCB ntfn = Some x; (y, tp) \<in> state_refs_of' s xa; (y, tp) \<notin> (if xa = x then {r \<in> state_refs_of' s x. snd r \<noteq> TCBBound} else if xa = ntfnptr then ntfn_q_refs_of' (ntfnObj ntfn) else state_refs_of' s xa)\<rbrakk> \<Longrightarrow> (xa, symreftype tp) \<notin> (if y = x then {r \<in> state_refs_of' s x. snd r \<noteq> TCBBound} else if y = ntfnptr then ntfn_q_refs_of' (ntfnObj ntfn) else state_refs_of' s y) proof (prove)
goal (2 subgoals):
 1. \<And>ntfn s x y tp. \<lbrakk>(y, tp) \<notin> state_refs_of' s ntfnptr; 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_inv (\<lambda>x. map_option cteCap (ctes_of s x)) (gsUntypedZeroRanges s); cur_tcb' s; ko_at' ntfn ntfnptr s; x \<noteq> ntfnptr; ntfnBoundTCB ntfn = Some x; (y, tp) \<in> ntfn_q_refs_of' (ntfnObj ntfn)\<rbrakk> \<Longrightarrow> (y = ntfnptr \<longrightarrow> (ntfnptr, symreftype tp) \<in> ntfn_q_refs_of' (ntfnObj ntfn)) \<and> (y \<noteq> ntfnptr \<longrightarrow> (y = x \<longrightarrow> (ntfnptr, symreftype tp) \<in> state_refs_of' s x \<and> symreftype tp \<noteq> TCBBound) \<and> (y \<noteq> x \<longrightarrow> (ntfnptr, symreftype tp) \<in> state_refs_of' s y))
 2. \<And>ntfn s x xa y tp. \<lbrakk>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_inv (\<lambda>x. map_option cteCap (ctes_of s x)) (gsUntypedZeroRanges s); cur_tcb' s; ko_at' ntfn ntfnptr s; x \<noteq> ntfnptr; ntfnBoundTCB ntfn = Some x; (y, tp) \<in> state_refs_of' s xa; (y, tp) \<notin> (if xa = x then {r \<in> state_refs_of' s x. snd r \<noteq> TCBBound} else if xa = ntfnptr then ntfn_q_refs_of' (ntfnObj ntfn) else state_refs_of' s xa)\<rbrakk> \<Longrightarrow> (xa, symreftype tp) \<notin> (if y = x then {r \<in> state_refs_of' s x. snd r \<noteq> TCBBound} else if y = ntfnptr then ntfn_q_refs_of' (ntfnObj ntfn) else state_refs_of' s y) proof (prove)
goal (1 subgoal):
 1. \<And>ntfn s x xa y tp. \<lbrakk>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_inv (\<lambda>x. map_option cteCap (ctes_of s x)) (gsUntypedZeroRanges s); cur_tcb' s; ko_at' ntfn ntfnptr s; x \<noteq> ntfnptr; ntfnBoundTCB ntfn = Some x; (y, tp) \<in> state_refs_of' s xa; (y, tp) \<notin> (if xa = x then {r \<in> state_refs_of' s x. snd r \<noteq> TCBBound} else if xa = ntfnptr then ntfn_q_refs_of' (ntfnObj ntfn) else state_refs_of' s xa)\<rbrakk> \<Longrightarrow> (xa, symreftype tp) \<notin> (if y = x then {r \<in> state_refs_of' s x. snd r \<noteq> TCBBound} else if y = ntfnptr then ntfn_q_refs_of' (ntfnObj ntfn) else state_refs_of' s y) proof (prove)
goal (2 subgoals):
 1. \<And>ntfn s x y. \<lbrakk>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_inv (\<lambda>x. map_option cteCap (ctes_of s x)) (gsUntypedZeroRanges s); cur_tcb' s; ko_at' ntfn ntfnptr s; x \<noteq> ntfnptr; ntfnBoundTCB ntfn = Some x; (y, TCBBound) \<in> state_refs_of' s x\<rbrakk> \<Longrightarrow> (y = ntfnptr \<longrightarrow> (x, NTFNBound) \<notin> ntfn_q_refs_of' (ntfnObj ntfn)) \<and> (y \<noteq> ntfnptr \<longrightarrow> (y = x \<longrightarrow> (x, NTFNBound) \<notin> state_refs_of' s x) \<and> (y \<noteq> x \<longrightarrow> (x, NTFNBound) \<notin> state_refs_of' s y))
 2. \<And>ntfn s x y tp. \<lbrakk>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_inv (\<lambda>x. map_option cteCap (ctes_of s x)) (gsUntypedZeroRanges s); cur_tcb' s; ko_at' ntfn ntfnptr s; x \<noteq> ntfnptr; ntfnBoundTCB ntfn = Some x; (y, tp) \<in> state_refs_of' s ntfnptr; (y, tp) \<notin> ntfn_q_refs_of' (ntfnObj ntfn)\<rbrakk> \<Longrightarrow> (y = ntfnptr \<longrightarrow> (ntfnptr, symreftype tp) \<notin> ntfn_q_refs_of' (ntfnObj ntfn)) \<and> (y \<noteq> ntfnptr \<longrightarrow> (y = x \<longrightarrow> (ntfnptr, symreftype tp) \<in> state_refs_of' s x \<longrightarrow> symreftype tp = TCBBound) \<and> (y \<noteq> x \<longrightarrow> (ntfnptr, symreftype tp) \<notin> state_refs_of' s y)) proof (prove)
goal (2 subgoals):
 1. \<And>ntfn s x y. \<lbrakk>valid_objs' s \<and> pspace_aligned' s \<and> pspace_distinct' s \<and> no_0_obj' s \<and> valid_mdb' 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_inv (\<lambda>x. map_option cteCap (ctes_of s x)) (gsUntypedZeroRanges s); cur_tcb' s; ko_at' ntfn ntfnptr s; x \<noteq> ntfnptr; ntfnBoundTCB ntfn = Some x; (y, TCBBound) \<in> state_refs_of' s x; bound_tcb_at' ((=) (Some ntfnptr)) x s\<rbrakk> \<Longrightarrow> (y = ntfnptr \<longrightarrow> (x, NTFNBound) \<notin> ntfn_q_refs_of' (ntfnObj ntfn)) \<and> (y \<noteq> ntfnptr \<longrightarrow> (y = x \<longrightarrow> (x, NTFNBound) \<notin> state_refs_of' s x) \<and> (y \<noteq> x \<longrightarrow> (x, NTFNBound) \<notin> state_refs_of' s y))
 2. \<And>ntfn s x y tp. \<lbrakk>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_inv (\<lambda>x. map_option cteCap (ctes_of s x)) (gsUntypedZeroRanges s); cur_tcb' s; ko_at' ntfn ntfnptr s; x \<noteq> ntfnptr; ntfnBoundTCB ntfn = Some x; (y, tp) \<in> state_refs_of' s ntfnptr; (y, tp) \<notin> ntfn_q_refs_of' (ntfnObj ntfn)\<rbrakk> \<Longrightarrow> (y = ntfnptr \<longrightarrow> (ntfnptr, symreftype tp) \<notin> ntfn_q_refs_of' (ntfnObj ntfn)) \<and> (y \<noteq> ntfnptr \<longrightarrow> (y = x \<longrightarrow> (ntfnptr, symreftype tp) \<in> state_refs_of' s x \<longrightarrow> symreftype tp = TCBBound) \<and> (y \<noteq> x \<longrightarrow> (ntfnptr, symreftype tp) \<notin> state_refs_of' s y)) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>valid_objs' s_ \<and> pspace_aligned' s_ \<and> pspace_distinct' s_ \<and> no_0_obj' s_ \<and> valid_mdb' 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_inv (\<lambda>x. map_option cteCap (ctes_of s_ x)) (gsUntypedZeroRanges s_); cur_tcb' s_; ko_at' ntfn_ ntfnptr s_; x_ \<noteq> ntfnptr; ntfnBoundTCB ntfn_ = Some x_; (y_, TCBBound) \<in> state_refs_of' s_ x_; bound_tcb_at' ((=) (Some ntfnptr)) x_ s_\<rbrakk> \<Longrightarrow> (y_ = ntfnptr \<longrightarrow> (x_, NTFNBound) \<notin> ntfn_q_refs_of' (ntfnObj ntfn_)) \<and> (y_ \<noteq> ntfnptr \<longrightarrow> (y_ = x_ \<longrightarrow> (x_, NTFNBound) \<notin> state_refs_of' s_ x_) \<and> (y_ \<noteq> x_ \<longrightarrow> (x_, NTFNBound) \<notin> state_refs_of' s_ y_)) proof (prove)
goal (1 subgoal):
 1. \<And>ntfn s x y tp. \<lbrakk>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_inv (\<lambda>x. map_option cteCap (ctes_of s x)) (gsUntypedZeroRanges s); cur_tcb' s; ko_at' ntfn ntfnptr s; x \<noteq> ntfnptr; ntfnBoundTCB ntfn = Some x; (y, tp) \<in> state_refs_of' s ntfnptr; (y, tp) \<notin> ntfn_q_refs_of' (ntfnObj ntfn)\<rbrakk> \<Longrightarrow> (y = ntfnptr \<longrightarrow> (ntfnptr, symreftype tp) \<notin> ntfn_q_refs_of' (ntfnObj ntfn)) \<and> (y \<noteq> ntfnptr \<longrightarrow> (y = x \<longrightarrow> (ntfnptr, symreftype tp) \<in> state_refs_of' s x \<longrightarrow> symreftype tp = TCBBound) \<and> (y \<noteq> x \<longrightarrow> (ntfnptr, symreftype tp) \<notin> state_refs_of' s y)) proof (prove)
goal:
No subgoals!