theory ADT_C

lemma cpspace_ntfn_relation_unique:
  assumes ntfns: "cpspace_ntfn_relation ah ch" "cpspace_ntfn_relation ah' ch"
      and   vs: "\<exists>s. ksPSpace s = ah \<and> valid_pspace' s"
      and   vs': "\<exists>s. ksPSpace s = ah' \<and> valid_pspace' s"
  shows   "map_to_ntfns ah' = map_to_ntfns ah" using ntfns apply (clarsimp simp: cmap_relation_def) apply (drule inj_image_inv[OF inj_Ptr])+ apply simp apply (rule ext) apply (case_tac "x:dom (map_to_ntfns ah)") apply (drule bspec, assumption)+ apply (simp add: dom_def Collect_eq, drule_tac x=x in spec) apply (clarsimp) apply (frule ksPSpace_valid_pspace_ntfnBoundTCB_nonzero[OF vs]) apply (frule ksPSpace_valid_pspace_ntfnBoundTCB_nonzero[OF vs']) apply (cut_tac vs vs') apply (clarsimp simp: valid_pspace'_def) apply (frule (2) map_to_ko_atI) apply (frule_tac v=ya in map_to_ko_atI, simp+) apply (clarsimp dest!: obj_at_valid_objs' simp: projectKOs split: option.splits) apply (thin_tac "map_to_ntfns x y = Some z" for x y z)+ apply (case_tac y, case_tac ya, case_tac "the (clift ch (ntfn_Ptr x))") by (auto simp: NtfnState_Active_def NtfnState_Idle_def NtfnState_Waiting_def typ_heap_simps
                     cnotification_relation_def Let_def tcb_queue_rel'_clift_unique
                     option_to_ctcb_ptr_def valid_obj'_def valid_ntfn'_def valid_bound_tcb'_def
                     kernel.tcb_at_not_NULL tcb_ptr_to_ctcb_ptr_inj
              split: ntfn.splits option.splits)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. map_to_ntfns ah' = map_to_ntfns ah proof (prove)
using this:
cmap_relation (map_to_ntfns ah) (clift ch) ntfn_Ptr (cnotification_relation (clift ch))
cmap_relation (map_to_ntfns ah') (clift ch) ntfn_Ptr (cnotification_relation (clift ch))

goal (1 subgoal):
 1. map_to_ntfns ah' = map_to_ntfns ah proof (prove)
goal (1 subgoal):
 1. \<lbrakk>ntfn_Ptr ` dom (map_to_ntfns ah) = dom (clift ch); \<forall>x\<in>dom (map_to_ntfns ah). cnotification_relation (clift ch) (the (map_to_ntfns ah x)) (the (clift ch (ntfn_Ptr x))); ntfn_Ptr ` dom (map_to_ntfns ah') = dom (clift ch); \<forall>x\<in>dom (map_to_ntfns ah'). cnotification_relation (clift ch) (the (map_to_ntfns ah' x)) (the (clift ch (ntfn_Ptr x)))\<rbrakk> \<Longrightarrow> map_to_ntfns ah' = map_to_ntfns ah proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<forall>x\<in>dom (map_to_ntfns ah). cnotification_relation (clift ch) (the (map_to_ntfns ah x)) (the (clift ch (ntfn_Ptr x))); \<forall>x\<in>dom (map_to_ntfns ah'). cnotification_relation (clift ch) (the (map_to_ntfns ah' x)) (the (clift ch (ntfn_Ptr x))); inv ntfn_Ptr ` dom (clift ch) = dom (map_to_ntfns ah); inv ntfn_Ptr ` dom (clift ch) = dom (map_to_ntfns ah')\<rbrakk> \<Longrightarrow> map_to_ntfns ah' = map_to_ntfns ah proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<forall>x\<in>dom (map_to_ntfns ah). cnotification_relation (clift ch) (the (map_to_ntfns ah x)) (the (clift ch (ntfn_Ptr x))); \<forall>x\<in>dom (map_to_ntfns ah). cnotification_relation (clift ch) (the (map_to_ntfns ah' x)) (the (clift ch (ntfn_Ptr x))); dom (map_to_ntfns ah') = dom (map_to_ntfns ah); inv ntfn_Ptr ` dom (clift ch) = dom (map_to_ntfns ah)\<rbrakk> \<Longrightarrow> map_to_ntfns ah' = map_to_ntfns ah proof (prove)
goal (1 subgoal):
 1. \<And>x. \<lbrakk>\<forall>x\<in>dom (map_to_ntfns ah). cnotification_relation (clift ch) (the (map_to_ntfns ah x)) (the (clift ch (ntfn_Ptr x))); \<forall>x\<in>dom (map_to_ntfns ah). cnotification_relation (clift ch) (the (map_to_ntfns ah' x)) (the (clift ch (ntfn_Ptr x))); dom (map_to_ntfns ah') = dom (map_to_ntfns ah); inv ntfn_Ptr ` dom (clift ch) = dom (map_to_ntfns ah)\<rbrakk> \<Longrightarrow> map_to_ntfns ah' x = map_to_ntfns ah x proof (prove)
goal (2 subgoals):
 1. \<And>x. \<lbrakk>\<forall>x\<in>dom (map_to_ntfns ah). cnotification_relation (clift ch) (the (map_to_ntfns ah x)) (the (clift ch (ntfn_Ptr x))); \<forall>x\<in>dom (map_to_ntfns ah). cnotification_relation (clift ch) (the (map_to_ntfns ah' x)) (the (clift ch (ntfn_Ptr x))); dom (map_to_ntfns ah') = dom (map_to_ntfns ah); inv ntfn_Ptr ` dom (clift ch) = dom (map_to_ntfns ah); x \<in> dom (map_to_ntfns ah)\<rbrakk> \<Longrightarrow> map_to_ntfns ah' x = map_to_ntfns ah x
 2. \<And>x. \<lbrakk>\<forall>x\<in>dom (map_to_ntfns ah). cnotification_relation (clift ch) (the (map_to_ntfns ah x)) (the (clift ch (ntfn_Ptr x))); \<forall>x\<in>dom (map_to_ntfns ah). cnotification_relation (clift ch) (the (map_to_ntfns ah' x)) (the (clift ch (ntfn_Ptr x))); dom (map_to_ntfns ah') = dom (map_to_ntfns ah); inv ntfn_Ptr ` dom (clift ch) = dom (map_to_ntfns ah); x \<notin> dom (map_to_ntfns ah)\<rbrakk> \<Longrightarrow> map_to_ntfns ah' x = map_to_ntfns ah x proof (prove)
goal (2 subgoals):
 1. \<And>x. \<lbrakk>dom (map_to_ntfns ah') = dom (map_to_ntfns ah); inv ntfn_Ptr ` dom (clift ch) = dom (map_to_ntfns ah); x \<in> dom (map_to_ntfns ah); cnotification_relation (clift ch) (the (map_to_ntfns ah x)) (the (clift ch (ntfn_Ptr x))); cnotification_relation (clift ch) (the (map_to_ntfns ah' x)) (the (clift ch (ntfn_Ptr x)))\<rbrakk> \<Longrightarrow> map_to_ntfns ah' x = map_to_ntfns ah x
 2. \<And>x. \<lbrakk>\<forall>x\<in>dom (map_to_ntfns ah). cnotification_relation (clift ch) (the (map_to_ntfns ah x)) (the (clift ch (ntfn_Ptr x))); \<forall>x\<in>dom (map_to_ntfns ah). cnotification_relation (clift ch) (the (map_to_ntfns ah' x)) (the (clift ch (ntfn_Ptr x))); dom (map_to_ntfns ah') = dom (map_to_ntfns ah); inv ntfn_Ptr ` dom (clift ch) = dom (map_to_ntfns ah); x \<notin> dom (map_to_ntfns ah)\<rbrakk> \<Longrightarrow> map_to_ntfns ah' x = map_to_ntfns ah x proof (prove)
goal (2 subgoals):
 1. \<And>x. \<lbrakk>inv ntfn_Ptr ` {a. \<exists>y. clift ch a = Some y} = {a. \<exists>y. map_to_ntfns ah a = Some y}; \<exists>y. map_to_ntfns ah x = Some y; cnotification_relation (clift ch) (the (map_to_ntfns ah x)) (the (clift ch (ntfn_Ptr x))); cnotification_relation (clift ch) (the (map_to_ntfns ah' x)) (the (clift ch (ntfn_Ptr x))); (\<exists>y. map_to_ntfns ah' x = Some y) = (\<exists>y. map_to_ntfns ah x = Some y)\<rbrakk> \<Longrightarrow> map_to_ntfns ah' x = map_to_ntfns ah x
 2. \<And>x. \<lbrakk>\<forall>x\<in>dom (map_to_ntfns ah). cnotification_relation (clift ch) (the (map_to_ntfns ah x)) (the (clift ch (ntfn_Ptr x))); \<forall>x\<in>dom (map_to_ntfns ah). cnotification_relation (clift ch) (the (map_to_ntfns ah' x)) (the (clift ch (ntfn_Ptr x))); dom (map_to_ntfns ah') = dom (map_to_ntfns ah); inv ntfn_Ptr ` dom (clift ch) = dom (map_to_ntfns ah); x \<notin> dom (map_to_ntfns ah)\<rbrakk> \<Longrightarrow> map_to_ntfns ah' x = map_to_ntfns ah x proof (prove)
goal (2 subgoals):
 1. \<And>x y ya. \<lbrakk>inv ntfn_Ptr ` {a. \<exists>y. clift ch a = Some y} = {a. \<exists>y. map_to_ntfns ah a = Some y}; cnotification_relation (clift ch) y (the (clift ch (ntfn_Ptr x))); cnotification_relation (clift ch) ya (the (clift ch (ntfn_Ptr x))); map_to_ntfns ah x = Some y; map_to_ntfns ah' x = Some ya\<rbrakk> \<Longrightarrow> ya = y
 2. \<And>x. \<lbrakk>\<forall>x\<in>dom (map_to_ntfns ah). cnotification_relation (clift ch) (the (map_to_ntfns ah x)) (the (clift ch (ntfn_Ptr x))); \<forall>x\<in>dom (map_to_ntfns ah). cnotification_relation (clift ch) (the (map_to_ntfns ah' x)) (the (clift ch (ntfn_Ptr x))); dom (map_to_ntfns ah') = dom (map_to_ntfns ah); inv ntfn_Ptr ` dom (clift ch) = dom (map_to_ntfns ah); x \<notin> dom (map_to_ntfns ah)\<rbrakk> \<Longrightarrow> map_to_ntfns ah' x = map_to_ntfns ah x proof (prove)
goal (2 subgoals):
 1. \<And>x y ya. \<lbrakk>inv ntfn_Ptr ` {a. \<exists>y. clift ch a = Some y} = {a. \<exists>y. map_to_ntfns ah a = Some y}; cnotification_relation (clift ch) y (the (clift ch (ntfn_Ptr x))); cnotification_relation (clift ch) ya (the (clift ch (ntfn_Ptr x))); map_to_ntfns ah x = Some y; map_to_ntfns ah' x = Some ya; ntfnBoundTCB y \<noteq> Some 0\<rbrakk> \<Longrightarrow> ya = y
 2. \<And>x. \<lbrakk>\<forall>x\<in>dom (map_to_ntfns ah). cnotification_relation (clift ch) (the (map_to_ntfns ah x)) (the (clift ch (ntfn_Ptr x))); \<forall>x\<in>dom (map_to_ntfns ah). cnotification_relation (clift ch) (the (map_to_ntfns ah' x)) (the (clift ch (ntfn_Ptr x))); dom (map_to_ntfns ah') = dom (map_to_ntfns ah); inv ntfn_Ptr ` dom (clift ch) = dom (map_to_ntfns ah); x \<notin> dom (map_to_ntfns ah)\<rbrakk> \<Longrightarrow> map_to_ntfns ah' x = map_to_ntfns ah x proof (prove)
goal (2 subgoals):
 1. \<And>x y ya. \<lbrakk>inv ntfn_Ptr ` {a. \<exists>y. clift ch a = Some y} = {a. \<exists>y. map_to_ntfns ah a = Some y}; cnotification_relation (clift ch) y (the (clift ch (ntfn_Ptr x))); cnotification_relation (clift ch) ya (the (clift ch (ntfn_Ptr x))); map_to_ntfns ah x = Some y; map_to_ntfns ah' x = Some ya; ntfnBoundTCB y \<noteq> Some 0; ntfnBoundTCB ya \<noteq> Some 0\<rbrakk> \<Longrightarrow> ya = y
 2. \<And>x. \<lbrakk>\<forall>x\<in>dom (map_to_ntfns ah). cnotification_relation (clift ch) (the (map_to_ntfns ah x)) (the (clift ch (ntfn_Ptr x))); \<forall>x\<in>dom (map_to_ntfns ah). cnotification_relation (clift ch) (the (map_to_ntfns ah' x)) (the (clift ch (ntfn_Ptr x))); dom (map_to_ntfns ah') = dom (map_to_ntfns ah); inv ntfn_Ptr ` dom (clift ch) = dom (map_to_ntfns ah); x \<notin> dom (map_to_ntfns ah)\<rbrakk> \<Longrightarrow> map_to_ntfns ah' x = map_to_ntfns ah x proof (prove)
goal (2 subgoals):
 1. \<And>x y ya. \<lbrakk>inv ntfn_Ptr ` {a. \<exists>y. clift ch a = Some y} = {a. \<exists>y. map_to_ntfns ah a = Some y}; cnotification_relation (clift ch) y (the (clift ch (ntfn_Ptr x))); cnotification_relation (clift ch) ya (the (clift ch (ntfn_Ptr x))); map_to_ntfns ah x = Some y; map_to_ntfns ah' x = Some ya; ntfnBoundTCB y \<noteq> Some 0; ntfnBoundTCB ya \<noteq> Some 0; \<exists>s. ksPSpace s = ah \<and> valid_pspace' s; \<exists>s. ksPSpace s = ah' \<and> valid_pspace' s\<rbrakk> \<Longrightarrow> ya = y
 2. \<And>x. \<lbrakk>\<forall>x\<in>dom (map_to_ntfns ah). cnotification_relation (clift ch) (the (map_to_ntfns ah x)) (the (clift ch (ntfn_Ptr x))); \<forall>x\<in>dom (map_to_ntfns ah). cnotification_relation (clift ch) (the (map_to_ntfns ah' x)) (the (clift ch (ntfn_Ptr x))); dom (map_to_ntfns ah') = dom (map_to_ntfns ah); inv ntfn_Ptr ` dom (clift ch) = dom (map_to_ntfns ah); x \<notin> dom (map_to_ntfns ah)\<rbrakk> \<Longrightarrow> map_to_ntfns ah' x = map_to_ntfns ah x proof (prove)
goal (2 subgoals):
 1. \<And>x y ya s sa. \<lbrakk>inv ntfn_Ptr ` {a. \<exists>y. clift ch a = Some y} = {a. \<exists>y. map_to_ntfns (ksPSpace s) a = Some y}; cnotification_relation (clift ch) y (the (clift ch (ntfn_Ptr x))); cnotification_relation (clift ch) ya (the (clift ch (ntfn_Ptr x))); map_to_ntfns (ksPSpace s) x = Some y; map_to_ntfns (ksPSpace sa) x = Some ya; ntfnBoundTCB y \<noteq> Some 0; ntfnBoundTCB ya \<noteq> Some 0; ah = ksPSpace s; ah' = ksPSpace sa; valid_objs' s; valid_objs' sa; pspace_aligned' s; pspace_aligned' sa; pspace_distinct' s; pspace_distinct' sa; no_0_obj' s; valid_mdb' s; no_0_obj' sa; valid_mdb' sa\<rbrakk> \<Longrightarrow> ya = y
 2. \<And>x. \<lbrakk>\<forall>x\<in>dom (map_to_ntfns ah). cnotification_relation (clift ch) (the (map_to_ntfns ah x)) (the (clift ch (ntfn_Ptr x))); \<forall>x\<in>dom (map_to_ntfns ah). cnotification_relation (clift ch) (the (map_to_ntfns ah' x)) (the (clift ch (ntfn_Ptr x))); dom (map_to_ntfns ah') = dom (map_to_ntfns ah); inv ntfn_Ptr ` dom (clift ch) = dom (map_to_ntfns ah); x \<notin> dom (map_to_ntfns ah)\<rbrakk> \<Longrightarrow> map_to_ntfns ah' x = map_to_ntfns ah x proof (prove)
goal (2 subgoals):
 1. \<And>x y ya s sa. \<lbrakk>inv ntfn_Ptr ` {a. \<exists>y. clift ch a = Some y} = {a. \<exists>y. map_to_ntfns (ksPSpace s) a = Some y}; cnotification_relation (clift ch) y (the (clift ch (ntfn_Ptr x))); cnotification_relation (clift ch) ya (the (clift ch (ntfn_Ptr x))); map_to_ntfns (ksPSpace s) x = Some y; map_to_ntfns (ksPSpace sa) x = Some ya; ntfnBoundTCB y \<noteq> Some 0; ntfnBoundTCB ya \<noteq> Some 0; ah = ksPSpace s; ah' = ksPSpace sa; valid_objs' s; valid_objs' sa; pspace_aligned' s; pspace_aligned' sa; pspace_distinct' s; pspace_distinct' sa; no_0_obj' s; valid_mdb' s; no_0_obj' sa; valid_mdb' sa; ko_at' y x s\<rbrakk> \<Longrightarrow> ya = y
 2. \<And>x. \<lbrakk>\<forall>x\<in>dom (map_to_ntfns ah). cnotification_relation (clift ch) (the (map_to_ntfns ah x)) (the (clift ch (ntfn_Ptr x))); \<forall>x\<in>dom (map_to_ntfns ah). cnotification_relation (clift ch) (the (map_to_ntfns ah' x)) (the (clift ch (ntfn_Ptr x))); dom (map_to_ntfns ah') = dom (map_to_ntfns ah); inv ntfn_Ptr ` dom (clift ch) = dom (map_to_ntfns ah); x \<notin> dom (map_to_ntfns ah)\<rbrakk> \<Longrightarrow> map_to_ntfns ah' x = map_to_ntfns ah x proof (prove)
goal (2 subgoals):
 1. \<And>x y ya s sa. \<lbrakk>inv ntfn_Ptr ` {a. \<exists>y. clift ch a = Some y} = {a. \<exists>y. map_to_ntfns (ksPSpace s) a = Some y}; cnotification_relation (clift ch) y (the (clift ch (ntfn_Ptr x))); cnotification_relation (clift ch) ya (the (clift ch (ntfn_Ptr x))); map_to_ntfns (ksPSpace s) x = Some y; map_to_ntfns (ksPSpace sa) x = Some ya; ntfnBoundTCB y \<noteq> Some 0; ntfnBoundTCB ya \<noteq> Some 0; ah = ksPSpace s; ah' = ksPSpace sa; valid_objs' s; valid_objs' sa; pspace_aligned' s; pspace_aligned' sa; pspace_distinct' s; pspace_distinct' sa; no_0_obj' s; valid_mdb' s; no_0_obj' sa; valid_mdb' sa; ko_at' y x s; ko_at' ya x sa\<rbrakk> \<Longrightarrow> ya = y
 2. \<And>x. \<lbrakk>\<forall>x\<in>dom (map_to_ntfns ah). cnotification_relation (clift ch) (the (map_to_ntfns ah x)) (the (clift ch (ntfn_Ptr x))); \<forall>x\<in>dom (map_to_ntfns ah). cnotification_relation (clift ch) (the (map_to_ntfns ah' x)) (the (clift ch (ntfn_Ptr x))); dom (map_to_ntfns ah') = dom (map_to_ntfns ah); inv ntfn_Ptr ` dom (clift ch) = dom (map_to_ntfns ah); x \<notin> dom (map_to_ntfns ah)\<rbrakk> \<Longrightarrow> map_to_ntfns ah' x = map_to_ntfns ah x proof (prove)
goal (2 subgoals):
 1. \<And>x y ya s sa. \<lbrakk>inv ntfn_Ptr ` {a. \<exists>y. clift ch a = Some y} = {a. \<exists>y. map_to_ntfns (ksPSpace s) a = Some y}; cnotification_relation (clift ch) y (the (clift ch (ntfn_Ptr x))); cnotification_relation (clift ch) ya (the (clift ch (ntfn_Ptr x))); map_to_ntfns (ksPSpace s) x = Some y; map_to_ntfns (ksPSpace sa) x = Some ya; ntfnBoundTCB y \<noteq> Some 0; ntfnBoundTCB ya \<noteq> Some 0; ah = ksPSpace s; ah' = ksPSpace sa; valid_objs' s; valid_objs' sa; pspace_aligned' s; pspace_aligned' sa; pspace_distinct' s; pspace_distinct' sa; no_0_obj' s; valid_mdb' s; no_0_obj' sa; valid_mdb' sa; valid_obj' (KONotification y) s; valid_obj' (KONotification ya) sa\<rbrakk> \<Longrightarrow> ya = y
 2. \<And>x. \<lbrakk>\<forall>x\<in>dom (map_to_ntfns ah). cnotification_relation (clift ch) (the (map_to_ntfns ah x)) (the (clift ch (ntfn_Ptr x))); \<forall>x\<in>dom (map_to_ntfns ah). cnotification_relation (clift ch) (the (map_to_ntfns ah' x)) (the (clift ch (ntfn_Ptr x))); dom (map_to_ntfns ah') = dom (map_to_ntfns ah); inv ntfn_Ptr ` dom (clift ch) = dom (map_to_ntfns ah); x \<notin> dom (map_to_ntfns ah)\<rbrakk> \<Longrightarrow> map_to_ntfns ah' x = map_to_ntfns ah x proof (prove)
goal (2 subgoals):
 1. \<And>x y ya s sa. \<lbrakk>inv ntfn_Ptr ` {a. \<exists>y. clift ch a = Some y} = {a. \<exists>y. map_to_ntfns (ksPSpace s) a = Some y}; cnotification_relation (clift ch) y (the (clift ch (ntfn_Ptr x))); cnotification_relation (clift ch) ya (the (clift ch (ntfn_Ptr x))); ntfnBoundTCB y \<noteq> Some 0; ntfnBoundTCB ya \<noteq> Some 0; ah = ksPSpace s; ah' = ksPSpace sa; valid_objs' s; valid_objs' sa; pspace_aligned' s; pspace_aligned' sa; pspace_distinct' s; pspace_distinct' sa; no_0_obj' s; valid_mdb' s; no_0_obj' sa; valid_mdb' sa; valid_obj' (KONotification y) s; valid_obj' (KONotification ya) sa\<rbrakk> \<Longrightarrow> ya = y
 2. \<And>x. \<lbrakk>\<forall>x\<in>dom (map_to_ntfns ah). cnotification_relation (clift ch) (the (map_to_ntfns ah x)) (the (clift ch (ntfn_Ptr x))); \<forall>x\<in>dom (map_to_ntfns ah). cnotification_relation (clift ch) (the (map_to_ntfns ah' x)) (the (clift ch (ntfn_Ptr x))); dom (map_to_ntfns ah') = dom (map_to_ntfns ah); inv ntfn_Ptr ` dom (clift ch) = dom (map_to_ntfns ah); x \<notin> dom (map_to_ntfns ah)\<rbrakk> \<Longrightarrow> map_to_ntfns ah' x = map_to_ntfns ah x proof (prove)
goal (2 subgoals):
 1. \<And>x y ya s sa x1 x2 x1a x2a xa. \<lbrakk>inv ntfn_Ptr ` {a. \<exists>y. clift ch a = Some y} = {a. \<exists>y. map_to_ntfns (ksPSpace s) a = Some y}; cnotification_relation (clift ch) y (the (clift ch (ntfn_Ptr x))); cnotification_relation (clift ch) ya (the (clift ch (ntfn_Ptr x))); ntfnBoundTCB y \<noteq> Some 0; ntfnBoundTCB ya \<noteq> Some 0; ah = ksPSpace s; ah' = ksPSpace sa; valid_objs' s; valid_objs' sa; pspace_aligned' s; pspace_aligned' sa; pspace_distinct' s; pspace_distinct' sa; no_0_obj' s; valid_mdb' s; no_0_obj' sa; valid_mdb' sa; valid_obj' (KONotification y) s; valid_obj' (KONotification ya) sa; y = NTFN x1 x2; ya = NTFN x1a x2a; the (clift ch (ntfn_Ptr x)) = notification_C xa\<rbrakk> \<Longrightarrow> ya = y
 2. \<And>x. \<lbrakk>\<forall>x\<in>dom (map_to_ntfns ah). cnotification_relation (clift ch) (the (map_to_ntfns ah x)) (the (clift ch (ntfn_Ptr x))); \<forall>x\<in>dom (map_to_ntfns ah). cnotification_relation (clift ch) (the (map_to_ntfns ah' x)) (the (clift ch (ntfn_Ptr x))); dom (map_to_ntfns ah') = dom (map_to_ntfns ah); inv ntfn_Ptr ` dom (clift ch) = dom (map_to_ntfns ah); x \<notin> dom (map_to_ntfns ah)\<rbrakk> \<Longrightarrow> map_to_ntfns ah' x = map_to_ntfns ah x