theory ADT_C

lemma cpspace_relation_unique:
  assumes valid_pspaces: "valid_pspace' s" "valid_pspace' s'"
  shows "cpspace_relation (ksPSpace s) bh ch \<Longrightarrow>
         cpspace_relation (ksPSpace s') bh ch \<Longrightarrow>
         (ksPSpace s') = (ksPSpace (s::kernel_state))" (is "PROP ?goal") proof - from valid_pspaces have no_kdatas: "KOKernelData \<notin> ran (ksPSpace s)"
                  "KOKernelData \<notin> ran (ksPSpace s')" by (auto simp add: valid_pspace'_def valid_objs'_def valid_obj'_def) from valid_pspaces have valid_objs: "valid_objs' s"    and valid_objs': "valid_objs' s'"
   and aligned: "pspace_aligned' s"   and aligned': "pspace_aligned' s'"
   and distinct: "pspace_distinct' s" and distinct': "pspace_distinct' s'"
   and no_0_objs: "no_0_obj' s"       and no_0_objs': "no_0_obj' s'" by auto show "PROP ?goal" apply (clarsimp simp add: cpspace_relation_def) apply (drule (1) cpspace_cte_relation_unique) apply (drule (1) cpspace_ep_relation_unique) apply (drule (1) cpspace_ntfn_relation_unique) apply (fastforce intro: valid_pspaces) apply (fastforce intro: valid_pspaces) apply (drule (1) cpspace_pde_relation_unique) apply (drule (1) cpspace_pte_relation_unique) apply (drule (1) cpspace_asidpool_relation_unique[
                     OF valid_objs'_imp_wf_asid_pool'[OF valid_objs]
                        valid_objs'_imp_wf_asid_pool'[OF valid_objs']]) apply (drule (1) cpspace_tcb_relation_unique) apply (fastforce intro: no_0_objs no_0_objs' valid_objs valid_objs') apply (fastforce intro: no_0_objs no_0_objs' valid_objs valid_objs') apply (intro allI impI,elim exE conjE) apply (rule_tac p=p in map_to_ctes_tcb_ctes, assumption) apply (frule (1) map_to_ko_atI[OF _ aligned distinct]) apply (frule (1) map_to_ko_atI[OF _ aligned' distinct']) apply (drule (1) map_to_cnes_eq[OF aligned aligned' distinct distinct']) apply (drule (1) cpspace_user_data_relation_unique) apply (drule (1)  cpspace_device_data_relation_unique) apply (thin_tac "cmap_relation a c f r" for a c f r)+ apply (cut_tac no_kdatas) apply (clarsimp simp add: ran_def fun_eq_iff) apply (drule_tac x=x in spec)+ apply (case_tac "ksPSpace s x") apply (case_tac "ksPSpace s' x", simp) apply (case_tac a, simp_all add: projectKO_opts
                            split: arch_kernel_object.splits) apply (clarsimp simp: projectKO_opts map_comp_def
                 split: kernel_object.splits arch_kernel_object.splits
                        option.splits) done qed

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>cpspace_relation (ksPSpace s) bh ch; cpspace_relation (ksPSpace s') bh ch\<rbrakk> \<Longrightarrow> ksPSpace s' = ksPSpace s proof (state)
goal (1 subgoal):
 1. \<lbrakk>cpspace_relation (ksPSpace s) bh ch; cpspace_relation (ksPSpace s') bh ch\<rbrakk> \<Longrightarrow> ksPSpace s' = ksPSpace s proof (chain)
picking this:
valid_pspace' s
valid_pspace' s' proof (prove)
using this:
valid_pspace' s
valid_pspace' s'

goal (1 subgoal):
 1. KOKernelData \<notin> ran (ksPSpace s) &&& KOKernelData \<notin> ran (ksPSpace s') proof (state)
this:
KOKernelData \<notin> ran (ksPSpace s)
KOKernelData \<notin> ran (ksPSpace s')

goal (1 subgoal):
 1. \<lbrakk>cpspace_relation (ksPSpace s) bh ch; cpspace_relation (ksPSpace s') bh ch\<rbrakk> \<Longrightarrow> ksPSpace s' = ksPSpace s proof (chain)
picking this:
valid_pspace' s
valid_pspace' s' proof (prove)
using this:
valid_pspace' s
valid_pspace' s'

goal (1 subgoal):
 1. ((valid_objs' s &&& valid_objs' s') &&& pspace_aligned' s &&& pspace_aligned' s') &&& (pspace_distinct' s &&& pspace_distinct' s') &&& no_0_obj' s &&& no_0_obj' s' proof (state)
this:
valid_objs' s
valid_objs' s'
pspace_aligned' s
pspace_aligned' s'
pspace_distinct' s
pspace_distinct' s'
no_0_obj' s
no_0_obj' s'

goal (1 subgoal):
 1. \<lbrakk>cpspace_relation (ksPSpace s) bh ch; cpspace_relation (ksPSpace s') bh ch\<rbrakk> \<Longrightarrow> ksPSpace s' = ksPSpace s proof (prove)
goal (1 subgoal):
 1. \<lbrakk>cpspace_relation (ksPSpace s) bh ch; cpspace_relation (ksPSpace s') bh ch\<rbrakk> \<Longrightarrow> ksPSpace s' = ksPSpace s proof (prove)
goal (1 subgoal):
 1. \<lbrakk>cmap_relation (ctes_of s) (clift ch) cte_Ptr ccte_relation; cmap_relation (ctes_of s') (clift ch) cte_Ptr ccte_relation; cpspace_tcb_relation (ksPSpace s) ch; cpspace_tcb_relation (ksPSpace s') ch; cmap_relation (map_to_eps (ksPSpace s)) (clift ch) ep_Ptr (cendpoint_relation (clift ch)); cmap_relation (map_to_eps (ksPSpace s')) (clift ch) ep_Ptr (cendpoint_relation (clift ch)); cmap_relation (map_to_ntfns (ksPSpace s)) (clift ch) ntfn_Ptr (cnotification_relation (clift ch)); cmap_relation (map_to_ntfns (ksPSpace s')) (clift ch) ntfn_Ptr (cnotification_relation (clift ch)); cmap_relation (map_to_pdes (ksPSpace s)) (clift ch) pde_Ptr cpde_relation; cmap_relation (map_to_pdes (ksPSpace s')) (clift ch) pde_Ptr cpde_relation; cmap_relation (map_to_ptes (ksPSpace s)) (clift ch) pte_Ptr cpte_relation; cmap_relation (map_to_ptes (ksPSpace s')) (clift ch) pte_Ptr cpte_relation; cmap_relation (map_to_asidpools (ksPSpace s)) (clift ch) ap_Ptr casid_pool_relation; cmap_relation (map_to_asidpools (ksPSpace s')) (clift ch) ap_Ptr casid_pool_relation; cpspace_user_data_relation (ksPSpace s) bh ch; cpspace_user_data_relation (ksPSpace s') bh ch; cpspace_device_data_relation (ksPSpace s) bh ch; cpspace_device_data_relation (ksPSpace s') bh ch; cpspace_pde_array_relation (ksPSpace s) ch; cpspace_pte_array_relation (ksPSpace s) ch; cpspace_pde_array_relation (ksPSpace s') ch; cpspace_pte_array_relation (ksPSpace s') ch\<rbrakk> \<Longrightarrow> ksPSpace s' = ksPSpace s proof (prove)
goal (1 subgoal):
 1. \<lbrakk>cmap_relation (ctes_of s') (clift ch) cte_Ptr ccte_relation; cpspace_tcb_relation (ksPSpace s) ch; cpspace_tcb_relation (ksPSpace s') ch; cmap_relation (map_to_eps (ksPSpace s)) (clift ch) ep_Ptr (cendpoint_relation (clift ch)); cmap_relation (map_to_eps (ksPSpace s')) (clift ch) ep_Ptr (cendpoint_relation (clift ch)); cmap_relation (map_to_ntfns (ksPSpace s)) (clift ch) ntfn_Ptr (cnotification_relation (clift ch)); cmap_relation (map_to_ntfns (ksPSpace s')) (clift ch) ntfn_Ptr (cnotification_relation (clift ch)); cmap_relation (map_to_pdes (ksPSpace s)) (clift ch) pde_Ptr cpde_relation; cmap_relation (map_to_pdes (ksPSpace s')) (clift ch) pde_Ptr cpde_relation; cmap_relation (map_to_ptes (ksPSpace s)) (clift ch) pte_Ptr cpte_relation; cmap_relation (map_to_ptes (ksPSpace s')) (clift ch) pte_Ptr cpte_relation; cmap_relation (map_to_asidpools (ksPSpace s)) (clift ch) ap_Ptr casid_pool_relation; cmap_relation (map_to_asidpools (ksPSpace s')) (clift ch) ap_Ptr casid_pool_relation; cpspace_user_data_relation (ksPSpace s) bh ch; cpspace_user_data_relation (ksPSpace s') bh ch; cpspace_device_data_relation (ksPSpace s) bh ch; cpspace_device_data_relation (ksPSpace s') bh ch; cpspace_pde_array_relation (ksPSpace s) ch; cpspace_pte_array_relation (ksPSpace s) ch; cpspace_pde_array_relation (ksPSpace s') ch; cpspace_pte_array_relation (ksPSpace s') ch; ctes_of s' = ctes_of s\<rbrakk> \<Longrightarrow> ksPSpace s' = ksPSpace s proof (prove)
goal (1 subgoal):
 1. \<lbrakk>cmap_relation (ctes_of s') (clift ch) cte_Ptr ccte_relation; cpspace_tcb_relation (ksPSpace s) ch; cpspace_tcb_relation (ksPSpace s') ch; cmap_relation (map_to_eps (ksPSpace s')) (clift ch) ep_Ptr (cendpoint_relation (clift ch)); cmap_relation (map_to_ntfns (ksPSpace s)) (clift ch) ntfn_Ptr (cnotification_relation (clift ch)); cmap_relation (map_to_ntfns (ksPSpace s')) (clift ch) ntfn_Ptr (cnotification_relation (clift ch)); cmap_relation (map_to_pdes (ksPSpace s)) (clift ch) pde_Ptr cpde_relation; cmap_relation (map_to_pdes (ksPSpace s')) (clift ch) pde_Ptr cpde_relation; cmap_relation (map_to_ptes (ksPSpace s)) (clift ch) pte_Ptr cpte_relation; cmap_relation (map_to_ptes (ksPSpace s')) (clift ch) pte_Ptr cpte_relation; cmap_relation (map_to_asidpools (ksPSpace s)) (clift ch) ap_Ptr casid_pool_relation; cmap_relation (map_to_asidpools (ksPSpace s')) (clift ch) ap_Ptr casid_pool_relation; cpspace_user_data_relation (ksPSpace s) bh ch; cpspace_user_data_relation (ksPSpace s') bh ch; cpspace_device_data_relation (ksPSpace s) bh ch; cpspace_device_data_relation (ksPSpace s') bh ch; cpspace_pde_array_relation (ksPSpace s) ch; cpspace_pte_array_relation (ksPSpace s) ch; cpspace_pde_array_relation (ksPSpace s') ch; cpspace_pte_array_relation (ksPSpace s') ch; ctes_of s' = ctes_of s; map_to_eps (ksPSpace s') = map_to_eps (ksPSpace s)\<rbrakk> \<Longrightarrow> ksPSpace s' = ksPSpace s proof (prove)
goal (3 subgoals):
 1. \<lbrakk>cmap_relation (ctes_of s') (clift ch) cte_Ptr ccte_relation; cpspace_tcb_relation (ksPSpace s) ch; cpspace_tcb_relation (ksPSpace s') ch; cmap_relation (map_to_eps (ksPSpace s')) (clift ch) ep_Ptr (cendpoint_relation (clift ch)); cmap_relation (map_to_ntfns (ksPSpace s')) (clift ch) ntfn_Ptr (cnotification_relation (clift ch)); cmap_relation (map_to_pdes (ksPSpace s)) (clift ch) pde_Ptr cpde_relation; cmap_relation (map_to_pdes (ksPSpace s')) (clift ch) pde_Ptr cpde_relation; cmap_relation (map_to_ptes (ksPSpace s)) (clift ch) pte_Ptr cpte_relation; cmap_relation (map_to_ptes (ksPSpace s')) (clift ch) pte_Ptr cpte_relation; cmap_relation (map_to_asidpools (ksPSpace s)) (clift ch) ap_Ptr casid_pool_relation; cmap_relation (map_to_asidpools (ksPSpace s')) (clift ch) ap_Ptr casid_pool_relation; cpspace_user_data_relation (ksPSpace s) bh ch; cpspace_user_data_relation (ksPSpace s') bh ch; cpspace_device_data_relation (ksPSpace s) bh ch; cpspace_device_data_relation (ksPSpace s') bh ch; cpspace_pde_array_relation (ksPSpace s) ch; cpspace_pte_array_relation (ksPSpace s) ch; cpspace_pde_array_relation (ksPSpace s') ch; cpspace_pte_array_relation (ksPSpace s') ch; ctes_of s' = ctes_of s; map_to_eps (ksPSpace s') = map_to_eps (ksPSpace s)\<rbrakk> \<Longrightarrow> \<exists>sa. ksPSpace sa = ksPSpace s \<and> valid_pspace' sa
 2. \<lbrakk>cmap_relation (ctes_of s') (clift ch) cte_Ptr ccte_relation; cpspace_tcb_relation (ksPSpace s) ch; cpspace_tcb_relation (ksPSpace s') ch; cmap_relation (map_to_eps (ksPSpace s')) (clift ch) ep_Ptr (cendpoint_relation (clift ch)); cmap_relation (map_to_ntfns (ksPSpace s')) (clift ch) ntfn_Ptr (cnotification_relation (clift ch)); cmap_relation (map_to_pdes (ksPSpace s)) (clift ch) pde_Ptr cpde_relation; cmap_relation (map_to_pdes (ksPSpace s')) (clift ch) pde_Ptr cpde_relation; cmap_relation (map_to_ptes (ksPSpace s)) (clift ch) pte_Ptr cpte_relation; cmap_relation (map_to_ptes (ksPSpace s')) (clift ch) pte_Ptr cpte_relation; cmap_relation (map_to_asidpools (ksPSpace s)) (clift ch) ap_Ptr casid_pool_relation; cmap_relation (map_to_asidpools (ksPSpace s')) (clift ch) ap_Ptr casid_pool_relation; cpspace_user_data_relation (ksPSpace s) bh ch; cpspace_user_data_relation (ksPSpace s') bh ch; cpspace_device_data_relation (ksPSpace s) bh ch; cpspace_device_data_relation (ksPSpace s') bh ch; cpspace_pde_array_relation (ksPSpace s) ch; cpspace_pte_array_relation (ksPSpace s) ch; cpspace_pde_array_relation (ksPSpace s') ch; cpspace_pte_array_relation (ksPSpace s') ch; ctes_of s' = ctes_of s; map_to_eps (ksPSpace s') = map_to_eps (ksPSpace s)\<rbrakk> \<Longrightarrow> \<exists>s. ksPSpace s = ksPSpace s' \<and> valid_pspace' s
 3. \<lbrakk>cmap_relation (ctes_of s') (clift ch) cte_Ptr ccte_relation; cpspace_tcb_relation (ksPSpace s) ch; cpspace_tcb_relation (ksPSpace s') ch; cmap_relation (map_to_eps (ksPSpace s')) (clift ch) ep_Ptr (cendpoint_relation (clift ch)); cmap_relation (map_to_ntfns (ksPSpace s')) (clift ch) ntfn_Ptr (cnotification_relation (clift ch)); cmap_relation (map_to_pdes (ksPSpace s)) (clift ch) pde_Ptr cpde_relation; cmap_relation (map_to_pdes (ksPSpace s')) (clift ch) pde_Ptr cpde_relation; cmap_relation (map_to_ptes (ksPSpace s)) (clift ch) pte_Ptr cpte_relation; cmap_relation (map_to_ptes (ksPSpace s')) (clift ch) pte_Ptr cpte_relation; cmap_relation (map_to_asidpools (ksPSpace s)) (clift ch) ap_Ptr casid_pool_relation; cmap_relation (map_to_asidpools (ksPSpace s')) (clift ch) ap_Ptr casid_pool_relation; cpspace_user_data_relation (ksPSpace s) bh ch; cpspace_user_data_relation (ksPSpace s') bh ch; cpspace_device_data_relation (ksPSpace s) bh ch; cpspace_device_data_relation (ksPSpace s') bh ch; cpspace_pde_array_relation (ksPSpace s) ch; cpspace_pte_array_relation (ksPSpace s) ch; cpspace_pde_array_relation (ksPSpace s') ch; cpspace_pte_array_relation (ksPSpace s') ch; ctes_of s' = ctes_of s; map_to_eps (ksPSpace s') = map_to_eps (ksPSpace s); map_to_ntfns (ksPSpace s') = map_to_ntfns (ksPSpace s)\<rbrakk> \<Longrightarrow> ksPSpace s' = ksPSpace s proof (prove)
goal (2 subgoals):
 1. \<lbrakk>cmap_relation (ctes_of s') (clift ch) cte_Ptr ccte_relation; cpspace_tcb_relation (ksPSpace s) ch; cpspace_tcb_relation (ksPSpace s') ch; cmap_relation (map_to_eps (ksPSpace s')) (clift ch) ep_Ptr (cendpoint_relation (clift ch)); cmap_relation (map_to_ntfns (ksPSpace s')) (clift ch) ntfn_Ptr (cnotification_relation (clift ch)); cmap_relation (map_to_pdes (ksPSpace s)) (clift ch) pde_Ptr cpde_relation; cmap_relation (map_to_pdes (ksPSpace s')) (clift ch) pde_Ptr cpde_relation; cmap_relation (map_to_ptes (ksPSpace s)) (clift ch) pte_Ptr cpte_relation; cmap_relation (map_to_ptes (ksPSpace s')) (clift ch) pte_Ptr cpte_relation; cmap_relation (map_to_asidpools (ksPSpace s)) (clift ch) ap_Ptr casid_pool_relation; cmap_relation (map_to_asidpools (ksPSpace s')) (clift ch) ap_Ptr casid_pool_relation; cpspace_user_data_relation (ksPSpace s) bh ch; cpspace_user_data_relation (ksPSpace s') bh ch; cpspace_device_data_relation (ksPSpace s) bh ch; cpspace_device_data_relation (ksPSpace s') bh ch; cpspace_pde_array_relation (ksPSpace s) ch; cpspace_pte_array_relation (ksPSpace s) ch; cpspace_pde_array_relation (ksPSpace s') ch; cpspace_pte_array_relation (ksPSpace s') ch; ctes_of s' = ctes_of s; map_to_eps (ksPSpace s') = map_to_eps (ksPSpace s)\<rbrakk> \<Longrightarrow> \<exists>s. ksPSpace s = ksPSpace s' \<and> valid_pspace' s
 2. \<lbrakk>cmap_relation (ctes_of s') (clift ch) cte_Ptr ccte_relation; cpspace_tcb_relation (ksPSpace s) ch; cpspace_tcb_relation (ksPSpace s') ch; cmap_relation (map_to_eps (ksPSpace s')) (clift ch) ep_Ptr (cendpoint_relation (clift ch)); cmap_relation (map_to_ntfns (ksPSpace s')) (clift ch) ntfn_Ptr (cnotification_relation (clift ch)); cmap_relation (map_to_pdes (ksPSpace s)) (clift ch) pde_Ptr cpde_relation; cmap_relation (map_to_pdes (ksPSpace s')) (clift ch) pde_Ptr cpde_relation; cmap_relation (map_to_ptes (ksPSpace s)) (clift ch) pte_Ptr cpte_relation; cmap_relation (map_to_ptes (ksPSpace s')) (clift ch) pte_Ptr cpte_relation; cmap_relation (map_to_asidpools (ksPSpace s)) (clift ch) ap_Ptr casid_pool_relation; cmap_relation (map_to_asidpools (ksPSpace s')) (clift ch) ap_Ptr casid_pool_relation; cpspace_user_data_relation (ksPSpace s) bh ch; cpspace_user_data_relation (ksPSpace s') bh ch; cpspace_device_data_relation (ksPSpace s) bh ch; cpspace_device_data_relation (ksPSpace s') bh ch; cpspace_pde_array_relation (ksPSpace s) ch; cpspace_pte_array_relation (ksPSpace s) ch; cpspace_pde_array_relation (ksPSpace s') ch; cpspace_pte_array_relation (ksPSpace s') ch; ctes_of s' = ctes_of s; map_to_eps (ksPSpace s') = map_to_eps (ksPSpace s); map_to_ntfns (ksPSpace s') = map_to_ntfns (ksPSpace s)\<rbrakk> \<Longrightarrow> ksPSpace s' = ksPSpace s proof (prove)
goal (1 subgoal):
 1. \<lbrakk>cmap_relation (ctes_of s') (clift ch) cte_Ptr ccte_relation; cpspace_tcb_relation (ksPSpace s) ch; cpspace_tcb_relation (ksPSpace s') ch; cmap_relation (map_to_eps (ksPSpace s')) (clift ch) ep_Ptr (cendpoint_relation (clift ch)); cmap_relation (map_to_ntfns (ksPSpace s')) (clift ch) ntfn_Ptr (cnotification_relation (clift ch)); cmap_relation (map_to_pdes (ksPSpace s)) (clift ch) pde_Ptr cpde_relation; cmap_relation (map_to_pdes (ksPSpace s')) (clift ch) pde_Ptr cpde_relation; cmap_relation (map_to_ptes (ksPSpace s)) (clift ch) pte_Ptr cpte_relation; cmap_relation (map_to_ptes (ksPSpace s')) (clift ch) pte_Ptr cpte_relation; cmap_relation (map_to_asidpools (ksPSpace s)) (clift ch) ap_Ptr casid_pool_relation; cmap_relation (map_to_asidpools (ksPSpace s')) (clift ch) ap_Ptr casid_pool_relation; cpspace_user_data_relation (ksPSpace s) bh ch; cpspace_user_data_relation (ksPSpace s') bh ch; cpspace_device_data_relation (ksPSpace s) bh ch; cpspace_device_data_relation (ksPSpace s') bh ch; cpspace_pde_array_relation (ksPSpace s) ch; cpspace_pte_array_relation (ksPSpace s) ch; cpspace_pde_array_relation (ksPSpace s') ch; cpspace_pte_array_relation (ksPSpace s') ch; ctes_of s' = ctes_of s; map_to_eps (ksPSpace s') = map_to_eps (ksPSpace s); map_to_ntfns (ksPSpace s') = map_to_ntfns (ksPSpace s)\<rbrakk> \<Longrightarrow> ksPSpace s' = ksPSpace s proof (prove)
goal (1 subgoal):
 1. \<lbrakk>cmap_relation (ctes_of s') (clift ch) cte_Ptr ccte_relation; cpspace_tcb_relation (ksPSpace s) ch; cpspace_tcb_relation (ksPSpace s') ch; cmap_relation (map_to_eps (ksPSpace s')) (clift ch) ep_Ptr (cendpoint_relation (clift ch)); cmap_relation (map_to_ntfns (ksPSpace s')) (clift ch) ntfn_Ptr (cnotification_relation (clift ch)); cmap_relation (map_to_pdes (ksPSpace s')) (clift ch) pde_Ptr cpde_relation; cmap_relation (map_to_ptes (ksPSpace s)) (clift ch) pte_Ptr cpte_relation; cmap_relation (map_to_ptes (ksPSpace s')) (clift ch) pte_Ptr cpte_relation; cmap_relation (map_to_asidpools (ksPSpace s)) (clift ch) ap_Ptr casid_pool_relation; cmap_relation (map_to_asidpools (ksPSpace s')) (clift ch) ap_Ptr casid_pool_relation; cpspace_user_data_relation (ksPSpace s) bh ch; cpspace_user_data_relation (ksPSpace s') bh ch; cpspace_device_data_relation (ksPSpace s) bh ch; cpspace_device_data_relation (ksPSpace s') bh ch; cpspace_pde_array_relation (ksPSpace s) ch; cpspace_pte_array_relation (ksPSpace s) ch; cpspace_pde_array_relation (ksPSpace s') ch; cpspace_pte_array_relation (ksPSpace s') ch; ctes_of s' = ctes_of s; map_to_eps (ksPSpace s') = map_to_eps (ksPSpace s); map_to_ntfns (ksPSpace s') = map_to_ntfns (ksPSpace s); map_to_pdes (ksPSpace s') = map_to_pdes (ksPSpace s)\<rbrakk> \<Longrightarrow> ksPSpace s' = ksPSpace s proof (prove)
goal (1 subgoal):
 1. \<lbrakk>cmap_relation (ctes_of s') (clift ch) cte_Ptr ccte_relation; cpspace_tcb_relation (ksPSpace s) ch; cpspace_tcb_relation (ksPSpace s') ch; cmap_relation (map_to_eps (ksPSpace s')) (clift ch) ep_Ptr (cendpoint_relation (clift ch)); cmap_relation (map_to_ntfns (ksPSpace s')) (clift ch) ntfn_Ptr (cnotification_relation (clift ch)); cmap_relation (map_to_pdes (ksPSpace s')) (clift ch) pde_Ptr cpde_relation; cmap_relation (map_to_ptes (ksPSpace s')) (clift ch) pte_Ptr cpte_relation; cmap_relation (map_to_asidpools (ksPSpace s)) (clift ch) ap_Ptr casid_pool_relation; cmap_relation (map_to_asidpools (ksPSpace s')) (clift ch) ap_Ptr casid_pool_relation; cpspace_user_data_relation (ksPSpace s) bh ch; cpspace_user_data_relation (ksPSpace s') bh ch; cpspace_device_data_relation (ksPSpace s) bh ch; cpspace_device_data_relation (ksPSpace s') bh ch; cpspace_pde_array_relation (ksPSpace s) ch; cpspace_pte_array_relation (ksPSpace s) ch; cpspace_pde_array_relation (ksPSpace s') ch; cpspace_pte_array_relation (ksPSpace s') ch; ctes_of s' = ctes_of s; map_to_eps (ksPSpace s') = map_to_eps (ksPSpace s); map_to_ntfns (ksPSpace s') = map_to_ntfns (ksPSpace s); map_to_pdes (ksPSpace s') = map_to_pdes (ksPSpace s); map_to_ptes (ksPSpace s') = map_to_ptes (ksPSpace s)\<rbrakk> \<Longrightarrow> ksPSpace s' = ksPSpace s proof (prove)
goal (1 subgoal):
 1. \<lbrakk>cmap_relation (ctes_of s') (clift ch) cte_Ptr ccte_relation; cpspace_tcb_relation (ksPSpace s) ch; cpspace_tcb_relation (ksPSpace s') ch; cmap_relation (map_to_eps (ksPSpace s')) (clift ch) ep_Ptr (cendpoint_relation (clift ch)); cmap_relation (map_to_ntfns (ksPSpace s')) (clift ch) ntfn_Ptr (cnotification_relation (clift ch)); cmap_relation (map_to_pdes (ksPSpace s')) (clift ch) pde_Ptr cpde_relation; cmap_relation (map_to_ptes (ksPSpace s')) (clift ch) pte_Ptr cpte_relation; cmap_relation (map_to_asidpools (ksPSpace s')) (clift ch) ap_Ptr casid_pool_relation; cpspace_user_data_relation (ksPSpace s) bh ch; cpspace_user_data_relation (ksPSpace s') bh ch; cpspace_device_data_relation (ksPSpace s) bh ch; cpspace_device_data_relation (ksPSpace s') bh ch; cpspace_pde_array_relation (ksPSpace s) ch; cpspace_pte_array_relation (ksPSpace s) ch; cpspace_pde_array_relation (ksPSpace s') ch; cpspace_pte_array_relation (ksPSpace s') ch; ctes_of s' = ctes_of s; map_to_eps (ksPSpace s') = map_to_eps (ksPSpace s); map_to_ntfns (ksPSpace s') = map_to_ntfns (ksPSpace s); map_to_pdes (ksPSpace s') = map_to_pdes (ksPSpace s); map_to_ptes (ksPSpace s') = map_to_ptes (ksPSpace s); map_to_asidpools (ksPSpace s') = map_to_asidpools (ksPSpace s)\<rbrakk> \<Longrightarrow> ksPSpace s' = ksPSpace s proof (prove)
goal (4 subgoals):
 1. \<lbrakk>cmap_relation (ctes_of s') (clift ch) cte_Ptr ccte_relation; cpspace_tcb_relation (ksPSpace s') ch; cmap_relation (map_to_eps (ksPSpace s')) (clift ch) ep_Ptr (cendpoint_relation (clift ch)); cmap_relation (map_to_ntfns (ksPSpace s')) (clift ch) ntfn_Ptr (cnotification_relation (clift ch)); cmap_relation (map_to_pdes (ksPSpace s')) (clift ch) pde_Ptr cpde_relation; cmap_relation (map_to_ptes (ksPSpace s')) (clift ch) pte_Ptr cpte_relation; cmap_relation (map_to_asidpools (ksPSpace s')) (clift ch) ap_Ptr casid_pool_relation; cpspace_user_data_relation (ksPSpace s) bh ch; cpspace_user_data_relation (ksPSpace s') bh ch; cpspace_device_data_relation (ksPSpace s) bh ch; cpspace_device_data_relation (ksPSpace s') bh ch; cpspace_pde_array_relation (ksPSpace s) ch; cpspace_pte_array_relation (ksPSpace s) ch; cpspace_pde_array_relation (ksPSpace s') ch; cpspace_pte_array_relation (ksPSpace s') ch; ctes_of s' = ctes_of s; map_to_eps (ksPSpace s') = map_to_eps (ksPSpace s); map_to_ntfns (ksPSpace s') = map_to_ntfns (ksPSpace s); map_to_pdes (ksPSpace s') = map_to_pdes (ksPSpace s); map_to_ptes (ksPSpace s') = map_to_ptes (ksPSpace s); map_to_asidpools (ksPSpace s') = map_to_asidpools (ksPSpace s)\<rbrakk> \<Longrightarrow> \<exists>sa. ksPSpace sa = ksPSpace s \<and> no_0_obj' sa \<and> valid_objs' sa
 2. \<lbrakk>cmap_relation (ctes_of s') (clift ch) cte_Ptr ccte_relation; cpspace_tcb_relation (ksPSpace s') ch; cmap_relation (map_to_eps (ksPSpace s')) (clift ch) ep_Ptr (cendpoint_relation (clift ch)); cmap_relation (map_to_ntfns (ksPSpace s')) (clift ch) ntfn_Ptr (cnotification_relation (clift ch)); cmap_relation (map_to_pdes (ksPSpace s')) (clift ch) pde_Ptr cpde_relation; cmap_relation (map_to_ptes (ksPSpace s')) (clift ch) pte_Ptr cpte_relation; cmap_relation (map_to_asidpools (ksPSpace s')) (clift ch) ap_Ptr casid_pool_relation; cpspace_user_data_relation (ksPSpace s) bh ch; cpspace_user_data_relation (ksPSpace s') bh ch; cpspace_device_data_relation (ksPSpace s) bh ch; cpspace_device_data_relation (ksPSpace s') bh ch; cpspace_pde_array_relation (ksPSpace s) ch; cpspace_pte_array_relation (ksPSpace s) ch; cpspace_pde_array_relation (ksPSpace s') ch; cpspace_pte_array_relation (ksPSpace s') ch; ctes_of s' = ctes_of s; map_to_eps (ksPSpace s') = map_to_eps (ksPSpace s); map_to_ntfns (ksPSpace s') = map_to_ntfns (ksPSpace s); map_to_pdes (ksPSpace s') = map_to_pdes (ksPSpace s); map_to_ptes (ksPSpace s') = map_to_ptes (ksPSpace s); map_to_asidpools (ksPSpace s') = map_to_asidpools (ksPSpace s)\<rbrakk> \<Longrightarrow> \<exists>s. ksPSpace s = ksPSpace s' \<and> no_0_obj' s \<and> valid_objs' s
 3. \<lbrakk>cmap_relation (ctes_of s') (clift ch) cte_Ptr ccte_relation; cpspace_tcb_relation (ksPSpace s') ch; cmap_relation (map_to_eps (ksPSpace s')) (clift ch) ep_Ptr (cendpoint_relation (clift ch)); cmap_relation (map_to_ntfns (ksPSpace s')) (clift ch) ntfn_Ptr (cnotification_relation (clift ch)); cmap_relation (map_to_pdes (ksPSpace s')) (clift ch) pde_Ptr cpde_relation; cmap_relation (map_to_ptes (ksPSpace s')) (clift ch) pte_Ptr cpte_relation; cmap_relation (map_to_asidpools (ksPSpace s')) (clift ch) ap_Ptr casid_pool_relation; cpspace_user_data_relation (ksPSpace s) bh ch; cpspace_user_data_relation (ksPSpace s') bh ch; cpspace_device_data_relation (ksPSpace s) bh ch; cpspace_device_data_relation (ksPSpace s') bh ch; cpspace_pde_array_relation (ksPSpace s) ch; cpspace_pte_array_relation (ksPSpace s) ch; cpspace_pde_array_relation (ksPSpace s') ch; cpspace_pte_array_relation (ksPSpace s') ch; ctes_of s' = ctes_of s; map_to_eps (ksPSpace s') = map_to_eps (ksPSpace s); map_to_ntfns (ksPSpace s') = map_to_ntfns (ksPSpace s); map_to_pdes (ksPSpace s') = map_to_pdes (ksPSpace s); map_to_ptes (ksPSpace s') = map_to_ptes (ksPSpace s); map_to_asidpools (ksPSpace s') = map_to_asidpools (ksPSpace s)\<rbrakk> \<Longrightarrow> \<forall>tcb tcb'. (\<exists>p. map_to_tcbs (ksPSpace s) p = Some tcb \<and> map_to_tcbs (ksPSpace s') p = Some tcb') \<longrightarrow> (\<forall>x\<in>ran tcb_cte_cases. fst x tcb' = fst x tcb)
 4. \<lbrakk>cmap_relation (ctes_of s') (clift ch) cte_Ptr ccte_relation; cpspace_tcb_relation (ksPSpace s') ch; cmap_relation (map_to_eps (ksPSpace s')) (clift ch) ep_Ptr (cendpoint_relation (clift ch)); cmap_relation (map_to_ntfns (ksPSpace s')) (clift ch) ntfn_Ptr (cnotification_relation (clift ch)); cmap_relation (map_to_pdes (ksPSpace s')) (clift ch) pde_Ptr cpde_relation; cmap_relation (map_to_ptes (ksPSpace s')) (clift ch) pte_Ptr cpte_relation; cmap_relation (map_to_asidpools (ksPSpace s')) (clift ch) ap_Ptr casid_pool_relation; cpspace_user_data_relation (ksPSpace s) bh ch; cpspace_user_data_relation (ksPSpace s') bh ch; cpspace_device_data_relation (ksPSpace s) bh ch; cpspace_device_data_relation (ksPSpace s') bh ch; cpspace_pde_array_relation (ksPSpace s) ch; cpspace_pte_array_relation (ksPSpace s) ch; cpspace_pde_array_relation (ksPSpace s') ch; cpspace_pte_array_relation (ksPSpace s') ch; ctes_of s' = ctes_of s; map_to_eps (ksPSpace s') = map_to_eps (ksPSpace s); map_to_ntfns (ksPSpace s') = map_to_ntfns (ksPSpace s); map_to_pdes (ksPSpace s') = map_to_pdes (ksPSpace s); map_to_ptes (ksPSpace s') = map_to_ptes (ksPSpace s); map_to_asidpools (ksPSpace s') = map_to_asidpools (ksPSpace s); map_to_tcbs (ksPSpace s') = map_to_tcbs (ksPSpace s)\<rbrakk> \<Longrightarrow> ksPSpace s' = ksPSpace s proof (prove)
goal (3 subgoals):
 1. \<lbrakk>cmap_relation (ctes_of s') (clift ch) cte_Ptr ccte_relation; cpspace_tcb_relation (ksPSpace s') ch; cmap_relation (map_to_eps (ksPSpace s')) (clift ch) ep_Ptr (cendpoint_relation (clift ch)); cmap_relation (map_to_ntfns (ksPSpace s')) (clift ch) ntfn_Ptr (cnotification_relation (clift ch)); cmap_relation (map_to_pdes (ksPSpace s')) (clift ch) pde_Ptr cpde_relation; cmap_relation (map_to_ptes (ksPSpace s')) (clift ch) pte_Ptr cpte_relation; cmap_relation (map_to_asidpools (ksPSpace s')) (clift ch) ap_Ptr casid_pool_relation; cpspace_user_data_relation (ksPSpace s) bh ch; cpspace_user_data_relation (ksPSpace s') bh ch; cpspace_device_data_relation (ksPSpace s) bh ch; cpspace_device_data_relation (ksPSpace s') bh ch; cpspace_pde_array_relation (ksPSpace s) ch; cpspace_pte_array_relation (ksPSpace s) ch; cpspace_pde_array_relation (ksPSpace s') ch; cpspace_pte_array_relation (ksPSpace s') ch; ctes_of s' = ctes_of s; map_to_eps (ksPSpace s') = map_to_eps (ksPSpace s); map_to_ntfns (ksPSpace s') = map_to_ntfns (ksPSpace s); map_to_pdes (ksPSpace s') = map_to_pdes (ksPSpace s); map_to_ptes (ksPSpace s') = map_to_ptes (ksPSpace s); map_to_asidpools (ksPSpace s') = map_to_asidpools (ksPSpace s)\<rbrakk> \<Longrightarrow> \<exists>s. ksPSpace s = ksPSpace s' \<and> no_0_obj' s \<and> valid_objs' s
 2. \<lbrakk>cmap_relation (ctes_of s') (clift ch) cte_Ptr ccte_relation; cpspace_tcb_relation (ksPSpace s') ch; cmap_relation (map_to_eps (ksPSpace s')) (clift ch) ep_Ptr (cendpoint_relation (clift ch)); cmap_relation (map_to_ntfns (ksPSpace s')) (clift ch) ntfn_Ptr (cnotification_relation (clift ch)); cmap_relation (map_to_pdes (ksPSpace s')) (clift ch) pde_Ptr cpde_relation; cmap_relation (map_to_ptes (ksPSpace s')) (clift ch) pte_Ptr cpte_relation; cmap_relation (map_to_asidpools (ksPSpace s')) (clift ch) ap_Ptr casid_pool_relation; cpspace_user_data_relation (ksPSpace s) bh ch; cpspace_user_data_relation (ksPSpace s') bh ch; cpspace_device_data_relation (ksPSpace s) bh ch; cpspace_device_data_relation (ksPSpace s') bh ch; cpspace_pde_array_relation (ksPSpace s) ch; cpspace_pte_array_relation (ksPSpace s) ch; cpspace_pde_array_relation (ksPSpace s') ch; cpspace_pte_array_relation (ksPSpace s') ch; ctes_of s' = ctes_of s; map_to_eps (ksPSpace s') = map_to_eps (ksPSpace s); map_to_ntfns (ksPSpace s') = map_to_ntfns (ksPSpace s); map_to_pdes (ksPSpace s') = map_to_pdes (ksPSpace s); map_to_ptes (ksPSpace s') = map_to_ptes (ksPSpace s); map_to_asidpools (ksPSpace s') = map_to_asidpools (ksPSpace s)\<rbrakk> \<Longrightarrow> \<forall>tcb tcb'. (\<exists>p. map_to_tcbs (ksPSpace s) p = Some tcb \<and> map_to_tcbs (ksPSpace s') p = Some tcb') \<longrightarrow> (\<forall>x\<in>ran tcb_cte_cases. fst x tcb' = fst x tcb)
 3. \<lbrakk>cmap_relation (ctes_of s') (clift ch) cte_Ptr ccte_relation; cpspace_tcb_relation (ksPSpace s') ch; cmap_relation (map_to_eps (ksPSpace s')) (clift ch) ep_Ptr (cendpoint_relation (clift ch)); cmap_relation (map_to_ntfns (ksPSpace s')) (clift ch) ntfn_Ptr (cnotification_relation (clift ch)); cmap_relation (map_to_pdes (ksPSpace s')) (clift ch) pde_Ptr cpde_relation; cmap_relation (map_to_ptes (ksPSpace s')) (clift ch) pte_Ptr cpte_relation; cmap_relation (map_to_asidpools (ksPSpace s')) (clift ch) ap_Ptr casid_pool_relation; cpspace_user_data_relation (ksPSpace s) bh ch; cpspace_user_data_relation (ksPSpace s') bh ch; cpspace_device_data_relation (ksPSpace s) bh ch; cpspace_device_data_relation (ksPSpace s') bh ch; cpspace_pde_array_relation (ksPSpace s) ch; cpspace_pte_array_relation (ksPSpace s) ch; cpspace_pde_array_relation (ksPSpace s') ch; cpspace_pte_array_relation (ksPSpace s') ch; ctes_of s' = ctes_of s; map_to_eps (ksPSpace s') = map_to_eps (ksPSpace s); map_to_ntfns (ksPSpace s') = map_to_ntfns (ksPSpace s); map_to_pdes (ksPSpace s') = map_to_pdes (ksPSpace s); map_to_ptes (ksPSpace s') = map_to_ptes (ksPSpace s); map_to_asidpools (ksPSpace s') = map_to_asidpools (ksPSpace s); map_to_tcbs (ksPSpace s') = map_to_tcbs (ksPSpace s)\<rbrakk> \<Longrightarrow> ksPSpace s' = ksPSpace s proof (prove)
goal (2 subgoals):
 1. \<lbrakk>cmap_relation (ctes_of s') (clift ch) cte_Ptr ccte_relation; cpspace_tcb_relation (ksPSpace s') ch; cmap_relation (map_to_eps (ksPSpace s')) (clift ch) ep_Ptr (cendpoint_relation (clift ch)); cmap_relation (map_to_ntfns (ksPSpace s')) (clift ch) ntfn_Ptr (cnotification_relation (clift ch)); cmap_relation (map_to_pdes (ksPSpace s')) (clift ch) pde_Ptr cpde_relation; cmap_relation (map_to_ptes (ksPSpace s')) (clift ch) pte_Ptr cpte_relation; cmap_relation (map_to_asidpools (ksPSpace s')) (clift ch) ap_Ptr casid_pool_relation; cpspace_user_data_relation (ksPSpace s) bh ch; cpspace_user_data_relation (ksPSpace s') bh ch; cpspace_device_data_relation (ksPSpace s) bh ch; cpspace_device_data_relation (ksPSpace s') bh ch; cpspace_pde_array_relation (ksPSpace s) ch; cpspace_pte_array_relation (ksPSpace s) ch; cpspace_pde_array_relation (ksPSpace s') ch; cpspace_pte_array_relation (ksPSpace s') ch; ctes_of s' = ctes_of s; map_to_eps (ksPSpace s') = map_to_eps (ksPSpace s); map_to_ntfns (ksPSpace s') = map_to_ntfns (ksPSpace s); map_to_pdes (ksPSpace s') = map_to_pdes (ksPSpace s); map_to_ptes (ksPSpace s') = map_to_ptes (ksPSpace s); map_to_asidpools (ksPSpace s') = map_to_asidpools (ksPSpace s)\<rbrakk> \<Longrightarrow> \<forall>tcb tcb'. (\<exists>p. map_to_tcbs (ksPSpace s) p = Some tcb \<and> map_to_tcbs (ksPSpace s') p = Some tcb') \<longrightarrow> (\<forall>x\<in>ran tcb_cte_cases. fst x tcb' = fst x tcb)
 2. \<lbrakk>cmap_relation (ctes_of s') (clift ch) cte_Ptr ccte_relation; cpspace_tcb_relation (ksPSpace s') ch; cmap_relation (map_to_eps (ksPSpace s')) (clift ch) ep_Ptr (cendpoint_relation (clift ch)); cmap_relation (map_to_ntfns (ksPSpace s')) (clift ch) ntfn_Ptr (cnotification_relation (clift ch)); cmap_relation (map_to_pdes (ksPSpace s')) (clift ch) pde_Ptr cpde_relation; cmap_relation (map_to_ptes (ksPSpace s')) (clift ch) pte_Ptr cpte_relation; cmap_relation (map_to_asidpools (ksPSpace s')) (clift ch) ap_Ptr casid_pool_relation; cpspace_user_data_relation (ksPSpace s) bh ch; cpspace_user_data_relation (ksPSpace s') bh ch; cpspace_device_data_relation (ksPSpace s) bh ch; cpspace_device_data_relation (ksPSpace s') bh ch; cpspace_pde_array_relation (ksPSpace s) ch; cpspace_pte_array_relation (ksPSpace s) ch; cpspace_pde_array_relation (ksPSpace s') ch; cpspace_pte_array_relation (ksPSpace s') ch; ctes_of s' = ctes_of s; map_to_eps (ksPSpace s') = map_to_eps (ksPSpace s); map_to_ntfns (ksPSpace s') = map_to_ntfns (ksPSpace s); map_to_pdes (ksPSpace s') = map_to_pdes (ksPSpace s); map_to_ptes (ksPSpace s') = map_to_ptes (ksPSpace s); map_to_asidpools (ksPSpace s') = map_to_asidpools (ksPSpace s); map_to_tcbs (ksPSpace s') = map_to_tcbs (ksPSpace s)\<rbrakk> \<Longrightarrow> ksPSpace s' = ksPSpace s proof (prove)
goal (2 subgoals):
 1. \<And>tcb tcb' p. \<lbrakk>cmap_relation (ctes_of s') (clift ch) cte_Ptr ccte_relation; cpspace_tcb_relation (ksPSpace s') ch; cmap_relation (map_to_eps (ksPSpace s')) (clift ch) ep_Ptr (cendpoint_relation (clift ch)); cmap_relation (map_to_ntfns (ksPSpace s')) (clift ch) ntfn_Ptr (cnotification_relation (clift ch)); cmap_relation (map_to_pdes (ksPSpace s')) (clift ch) pde_Ptr cpde_relation; cmap_relation (map_to_ptes (ksPSpace s')) (clift ch) pte_Ptr cpte_relation; cmap_relation (map_to_asidpools (ksPSpace s')) (clift ch) ap_Ptr casid_pool_relation; cpspace_user_data_relation (ksPSpace s) bh ch; cpspace_user_data_relation (ksPSpace s') bh ch; cpspace_device_data_relation (ksPSpace s) bh ch; cpspace_device_data_relation (ksPSpace s') bh ch; cpspace_pde_array_relation (ksPSpace s) ch; cpspace_pte_array_relation (ksPSpace s) ch; cpspace_pde_array_relation (ksPSpace s') ch; cpspace_pte_array_relation (ksPSpace s') ch; ctes_of s' = ctes_of s; map_to_eps (ksPSpace s') = map_to_eps (ksPSpace s); map_to_ntfns (ksPSpace s') = map_to_ntfns (ksPSpace s); map_to_pdes (ksPSpace s') = map_to_pdes (ksPSpace s); map_to_ptes (ksPSpace s') = map_to_ptes (ksPSpace s); map_to_asidpools (ksPSpace s') = map_to_asidpools (ksPSpace s); map_to_tcbs (ksPSpace s) p = Some tcb; map_to_tcbs (ksPSpace s') p = Some tcb'\<rbrakk> \<Longrightarrow> \<forall>x\<in>ran tcb_cte_cases. fst x tcb' = fst x tcb
 2. \<lbrakk>cmap_relation (ctes_of s') (clift ch) cte_Ptr ccte_relation; cpspace_tcb_relation (ksPSpace s') ch; cmap_relation (map_to_eps (ksPSpace s')) (clift ch) ep_Ptr (cendpoint_relation (clift ch)); cmap_relation (map_to_ntfns (ksPSpace s')) (clift ch) ntfn_Ptr (cnotification_relation (clift ch)); cmap_relation (map_to_pdes (ksPSpace s')) (clift ch) pde_Ptr cpde_relation; cmap_relation (map_to_ptes (ksPSpace s')) (clift ch) pte_Ptr cpte_relation; cmap_relation (map_to_asidpools (ksPSpace s')) (clift ch) ap_Ptr casid_pool_relation; cpspace_user_data_relation (ksPSpace s) bh ch; cpspace_user_data_relation (ksPSpace s') bh ch; cpspace_device_data_relation (ksPSpace s) bh ch; cpspace_device_data_relation (ksPSpace s') bh ch; cpspace_pde_array_relation (ksPSpace s) ch; cpspace_pte_array_relation (ksPSpace s) ch; cpspace_pde_array_relation (ksPSpace s') ch; cpspace_pte_array_relation (ksPSpace s') ch; ctes_of s' = ctes_of s; map_to_eps (ksPSpace s') = map_to_eps (ksPSpace s); map_to_ntfns (ksPSpace s') = map_to_ntfns (ksPSpace s); map_to_pdes (ksPSpace s') = map_to_pdes (ksPSpace s); map_to_ptes (ksPSpace s') = map_to_ptes (ksPSpace s); map_to_asidpools (ksPSpace s') = map_to_asidpools (ksPSpace s); map_to_tcbs (ksPSpace s') = map_to_tcbs (ksPSpace s)\<rbrakk> \<Longrightarrow> ksPSpace s' = ksPSpace s proof (prove)
goal (3 subgoals):
 1. \<And>tcb tcb' p. \<lbrakk>cmap_relation (ctes_of s') (clift ch) cte_Ptr ccte_relation; cpspace_tcb_relation (ksPSpace s') ch; cmap_relation (map_to_eps (ksPSpace s')) (clift ch) ep_Ptr (cendpoint_relation (clift ch)); cmap_relation (map_to_ntfns (ksPSpace s')) (clift ch) ntfn_Ptr (cnotification_relation (clift ch)); cmap_relation (map_to_pdes (ksPSpace s')) (clift ch) pde_Ptr cpde_relation; cmap_relation (map_to_ptes (ksPSpace s')) (clift ch) pte_Ptr cpte_relation; cmap_relation (map_to_asidpools (ksPSpace s')) (clift ch) ap_Ptr casid_pool_relation; cpspace_user_data_relation (ksPSpace s) bh ch; cpspace_user_data_relation (ksPSpace s') bh ch; cpspace_device_data_relation (ksPSpace s) bh ch; cpspace_device_data_relation (ksPSpace s') bh ch; cpspace_pde_array_relation (ksPSpace s) ch; cpspace_pte_array_relation (ksPSpace s) ch; cpspace_pde_array_relation (ksPSpace s') ch; cpspace_pte_array_relation (ksPSpace s') ch; ctes_of s' = ctes_of s; map_to_eps (ksPSpace s') = map_to_eps (ksPSpace s); map_to_ntfns (ksPSpace s') = map_to_ntfns (ksPSpace s); map_to_pdes (ksPSpace s') = map_to_pdes (ksPSpace s); map_to_ptes (ksPSpace s') = map_to_ptes (ksPSpace s); map_to_asidpools (ksPSpace s') = map_to_asidpools (ksPSpace s); map_to_tcbs (ksPSpace s) p = Some tcb; map_to_tcbs (ksPSpace s') p = Some tcb'\<rbrakk> \<Longrightarrow> ko_at' tcb p s
 2. \<And>tcb tcb' p. \<lbrakk>cmap_relation (ctes_of s') (clift ch) cte_Ptr ccte_relation; cpspace_tcb_relation (ksPSpace s') ch; cmap_relation (map_to_eps (ksPSpace s')) (clift ch) ep_Ptr (cendpoint_relation (clift ch)); cmap_relation (map_to_ntfns (ksPSpace s')) (clift ch) ntfn_Ptr (cnotification_relation (clift ch)); cmap_relation (map_to_pdes (ksPSpace s')) (clift ch) pde_Ptr cpde_relation; cmap_relation (map_to_ptes (ksPSpace s')) (clift ch) pte_Ptr cpte_relation; cmap_relation (map_to_asidpools (ksPSpace s')) (clift ch) ap_Ptr casid_pool_relation; cpspace_user_data_relation (ksPSpace s) bh ch; cpspace_user_data_relation (ksPSpace s') bh ch; cpspace_device_data_relation (ksPSpace s) bh ch; cpspace_device_data_relation (ksPSpace s') bh ch; cpspace_pde_array_relation (ksPSpace s) ch; cpspace_pte_array_relation (ksPSpace s) ch; cpspace_pde_array_relation (ksPSpace s') ch; cpspace_pte_array_relation (ksPSpace s') ch; ctes_of s' = ctes_of s; map_to_eps (ksPSpace s') = map_to_eps (ksPSpace s); map_to_ntfns (ksPSpace s') = map_to_ntfns (ksPSpace s); map_to_pdes (ksPSpace s') = map_to_pdes (ksPSpace s); map_to_ptes (ksPSpace s') = map_to_ptes (ksPSpace s); map_to_asidpools (ksPSpace s') = map_to_asidpools (ksPSpace s); map_to_tcbs (ksPSpace s) p = Some tcb; map_to_tcbs (ksPSpace s') p = Some tcb'\<rbrakk> \<Longrightarrow> ko_at' tcb' p s'
 3. \<lbrakk>cmap_relation (ctes_of s') (clift ch) cte_Ptr ccte_relation; cpspace_tcb_relation (ksPSpace s') ch; cmap_relation (map_to_eps (ksPSpace s')) (clift ch) ep_Ptr (cendpoint_relation (clift ch)); cmap_relation (map_to_ntfns (ksPSpace s')) (clift ch) ntfn_Ptr (cnotification_relation (clift ch)); cmap_relation (map_to_pdes (ksPSpace s')) (clift ch) pde_Ptr cpde_relation; cmap_relation (map_to_ptes (ksPSpace s')) (clift ch) pte_Ptr cpte_relation; cmap_relation (map_to_asidpools (ksPSpace s')) (clift ch) ap_Ptr casid_pool_relation; cpspace_user_data_relation (ksPSpace s) bh ch; cpspace_user_data_relation (ksPSpace s') bh ch; cpspace_device_data_relation (ksPSpace s) bh ch; cpspace_device_data_relation (ksPSpace s') bh ch; cpspace_pde_array_relation (ksPSpace s) ch; cpspace_pte_array_relation (ksPSpace s) ch; cpspace_pde_array_relation (ksPSpace s') ch; cpspace_pte_array_relation (ksPSpace s') ch; ctes_of s' = ctes_of s; map_to_eps (ksPSpace s') = map_to_eps (ksPSpace s); map_to_ntfns (ksPSpace s') = map_to_ntfns (ksPSpace s); map_to_pdes (ksPSpace s') = map_to_pdes (ksPSpace s); map_to_ptes (ksPSpace s') = map_to_ptes (ksPSpace s); map_to_asidpools (ksPSpace s') = map_to_asidpools (ksPSpace s); map_to_tcbs (ksPSpace s') = map_to_tcbs (ksPSpace s)\<rbrakk> \<Longrightarrow> ksPSpace s' = ksPSpace s proof (prove)
goal (2 subgoals):
 1. \<And>tcb tcb' p. \<lbrakk>cmap_relation (ctes_of s') (clift ch) cte_Ptr ccte_relation; cpspace_tcb_relation (ksPSpace s') ch; cmap_relation (map_to_eps (ksPSpace s')) (clift ch) ep_Ptr (cendpoint_relation (clift ch)); cmap_relation (map_to_ntfns (ksPSpace s')) (clift ch) ntfn_Ptr (cnotification_relation (clift ch)); cmap_relation (map_to_pdes (ksPSpace s')) (clift ch) pde_Ptr cpde_relation; cmap_relation (map_to_ptes (ksPSpace s')) (clift ch) pte_Ptr cpte_relation; cmap_relation (map_to_asidpools (ksPSpace s')) (clift ch) ap_Ptr casid_pool_relation; cpspace_user_data_relation (ksPSpace s) bh ch; cpspace_user_data_relation (ksPSpace s') bh ch; cpspace_device_data_relation (ksPSpace s) bh ch; cpspace_device_data_relation (ksPSpace s') bh ch; cpspace_pde_array_relation (ksPSpace s) ch; cpspace_pte_array_relation (ksPSpace s) ch; cpspace_pde_array_relation (ksPSpace s') ch; cpspace_pte_array_relation (ksPSpace s') ch; ctes_of s' = ctes_of s; map_to_eps (ksPSpace s') = map_to_eps (ksPSpace s); map_to_ntfns (ksPSpace s') = map_to_ntfns (ksPSpace s); map_to_pdes (ksPSpace s') = map_to_pdes (ksPSpace s); map_to_ptes (ksPSpace s') = map_to_ptes (ksPSpace s); map_to_asidpools (ksPSpace s') = map_to_asidpools (ksPSpace s); map_to_tcbs (ksPSpace s) p = Some tcb; map_to_tcbs (ksPSpace s') p = Some tcb'\<rbrakk> \<Longrightarrow> ko_at' tcb' p s'
 2. \<lbrakk>cmap_relation (ctes_of s') (clift ch) cte_Ptr ccte_relation; cpspace_tcb_relation (ksPSpace s') ch; cmap_relation (map_to_eps (ksPSpace s')) (clift ch) ep_Ptr (cendpoint_relation (clift ch)); cmap_relation (map_to_ntfns (ksPSpace s')) (clift ch) ntfn_Ptr (cnotification_relation (clift ch)); cmap_relation (map_to_pdes (ksPSpace s')) (clift ch) pde_Ptr cpde_relation; cmap_relation (map_to_ptes (ksPSpace s')) (clift ch) pte_Ptr cpte_relation; cmap_relation (map_to_asidpools (ksPSpace s')) (clift ch) ap_Ptr casid_pool_relation; cpspace_user_data_relation (ksPSpace s) bh ch; cpspace_user_data_relation (ksPSpace s') bh ch; cpspace_device_data_relation (ksPSpace s) bh ch; cpspace_device_data_relation (ksPSpace s') bh ch; cpspace_pde_array_relation (ksPSpace s) ch; cpspace_pte_array_relation (ksPSpace s) ch; cpspace_pde_array_relation (ksPSpace s') ch; cpspace_pte_array_relation (ksPSpace s') ch; ctes_of s' = ctes_of s; map_to_eps (ksPSpace s') = map_to_eps (ksPSpace s); map_to_ntfns (ksPSpace s') = map_to_ntfns (ksPSpace s); map_to_pdes (ksPSpace s') = map_to_pdes (ksPSpace s); map_to_ptes (ksPSpace s') = map_to_ptes (ksPSpace s); map_to_asidpools (ksPSpace s') = map_to_asidpools (ksPSpace s); map_to_tcbs (ksPSpace s') = map_to_tcbs (ksPSpace s)\<rbrakk> \<Longrightarrow> ksPSpace s' = ksPSpace s proof (prove)
goal (1 subgoal):
 1. \<lbrakk>cmap_relation (ctes_of s') (clift ch) cte_Ptr ccte_relation; cpspace_tcb_relation (ksPSpace s') ch; cmap_relation (map_to_eps (ksPSpace s')) (clift ch) ep_Ptr (cendpoint_relation (clift ch)); cmap_relation (map_to_ntfns (ksPSpace s')) (clift ch) ntfn_Ptr (cnotification_relation (clift ch)); cmap_relation (map_to_pdes (ksPSpace s')) (clift ch) pde_Ptr cpde_relation; cmap_relation (map_to_ptes (ksPSpace s')) (clift ch) pte_Ptr cpte_relation; cmap_relation (map_to_asidpools (ksPSpace s')) (clift ch) ap_Ptr casid_pool_relation; cpspace_user_data_relation (ksPSpace s) bh ch; cpspace_user_data_relation (ksPSpace s') bh ch; cpspace_device_data_relation (ksPSpace s) bh ch; cpspace_device_data_relation (ksPSpace s') bh ch; cpspace_pde_array_relation (ksPSpace s) ch; cpspace_pte_array_relation (ksPSpace s) ch; cpspace_pde_array_relation (ksPSpace s') ch; cpspace_pte_array_relation (ksPSpace s') ch; ctes_of s' = ctes_of s; map_to_eps (ksPSpace s') = map_to_eps (ksPSpace s); map_to_ntfns (ksPSpace s') = map_to_ntfns (ksPSpace s); map_to_pdes (ksPSpace s') = map_to_pdes (ksPSpace s); map_to_ptes (ksPSpace s') = map_to_ptes (ksPSpace s); map_to_asidpools (ksPSpace s') = map_to_asidpools (ksPSpace s); map_to_tcbs (ksPSpace s') = map_to_tcbs (ksPSpace s)\<rbrakk> \<Longrightarrow> ksPSpace s' = ksPSpace s proof (prove)
goal (1 subgoal):
 1. \<lbrakk>cmap_relation (ctes_of s') (clift ch) cte_Ptr ccte_relation; cpspace_tcb_relation (ksPSpace s') ch; cmap_relation (map_to_eps (ksPSpace s')) (clift ch) ep_Ptr (cendpoint_relation (clift ch)); cmap_relation (map_to_ntfns (ksPSpace s')) (clift ch) ntfn_Ptr (cnotification_relation (clift ch)); cmap_relation (map_to_pdes (ksPSpace s')) (clift ch) pde_Ptr cpde_relation; cmap_relation (map_to_ptes (ksPSpace s')) (clift ch) pte_Ptr cpte_relation; cmap_relation (map_to_asidpools (ksPSpace s')) (clift ch) ap_Ptr casid_pool_relation; cpspace_user_data_relation (ksPSpace s) bh ch; cpspace_user_data_relation (ksPSpace s') bh ch; cpspace_device_data_relation (ksPSpace s) bh ch; cpspace_device_data_relation (ksPSpace s') bh ch; cpspace_pde_array_relation (ksPSpace s) ch; cpspace_pte_array_relation (ksPSpace s) ch; cpspace_pde_array_relation (ksPSpace s') ch; cpspace_pte_array_relation (ksPSpace s') ch; map_to_eps (ksPSpace s') = map_to_eps (ksPSpace s); map_to_ntfns (ksPSpace s') = map_to_ntfns (ksPSpace s); map_to_pdes (ksPSpace s') = map_to_pdes (ksPSpace s); map_to_ptes (ksPSpace s') = map_to_ptes (ksPSpace s); map_to_asidpools (ksPSpace s') = map_to_asidpools (ksPSpace s); map_to_tcbs (ksPSpace s') = map_to_tcbs (ksPSpace s); map_to_cnes (ksPSpace s') = map_to_cnes (ksPSpace s)\<rbrakk> \<Longrightarrow> ksPSpace s' = ksPSpace s proof (prove)
goal (1 subgoal):
 1. \<lbrakk>cmap_relation (ctes_of s') (clift ch) cte_Ptr ccte_relation; cpspace_tcb_relation (ksPSpace s') ch; cmap_relation (map_to_eps (ksPSpace s')) (clift ch) ep_Ptr (cendpoint_relation (clift ch)); cmap_relation (map_to_ntfns (ksPSpace s')) (clift ch) ntfn_Ptr (cnotification_relation (clift ch)); cmap_relation (map_to_pdes (ksPSpace s')) (clift ch) pde_Ptr cpde_relation; cmap_relation (map_to_ptes (ksPSpace s')) (clift ch) pte_Ptr cpte_relation; cmap_relation (map_to_asidpools (ksPSpace s')) (clift ch) ap_Ptr casid_pool_relation; cpspace_user_data_relation (ksPSpace s') bh ch; cpspace_device_data_relation (ksPSpace s) bh ch; cpspace_device_data_relation (ksPSpace s') bh ch; cpspace_pde_array_relation (ksPSpace s) ch; cpspace_pte_array_relation (ksPSpace s) ch; cpspace_pde_array_relation (ksPSpace s') ch; cpspace_pte_array_relation (ksPSpace s') ch; map_to_eps (ksPSpace s') = map_to_eps (ksPSpace s); map_to_ntfns (ksPSpace s') = map_to_ntfns (ksPSpace s); map_to_pdes (ksPSpace s') = map_to_pdes (ksPSpace s); map_to_ptes (ksPSpace s') = map_to_ptes (ksPSpace s); map_to_asidpools (ksPSpace s') = map_to_asidpools (ksPSpace s); map_to_tcbs (ksPSpace s') = map_to_tcbs (ksPSpace s); map_to_cnes (ksPSpace s') = map_to_cnes (ksPSpace s); map_to_user_data (ksPSpace s') = map_to_user_data (ksPSpace s)\<rbrakk> \<Longrightarrow> ksPSpace s' = ksPSpace s proof (prove)
goal (1 subgoal):
 1. \<lbrakk>cmap_relation (ctes_of s') (clift ch) cte_Ptr ccte_relation; cpspace_tcb_relation (ksPSpace s') ch; cmap_relation (map_to_eps (ksPSpace s')) (clift ch) ep_Ptr (cendpoint_relation (clift ch)); cmap_relation (map_to_ntfns (ksPSpace s')) (clift ch) ntfn_Ptr (cnotification_relation (clift ch)); cmap_relation (map_to_pdes (ksPSpace s')) (clift ch) pde_Ptr cpde_relation; cmap_relation (map_to_ptes (ksPSpace s')) (clift ch) pte_Ptr cpte_relation; cmap_relation (map_to_asidpools (ksPSpace s')) (clift ch) ap_Ptr casid_pool_relation; cpspace_user_data_relation (ksPSpace s') bh ch; cpspace_device_data_relation (ksPSpace s') bh ch; cpspace_pde_array_relation (ksPSpace s) ch; cpspace_pte_array_relation (ksPSpace s) ch; cpspace_pde_array_relation (ksPSpace s') ch; cpspace_pte_array_relation (ksPSpace s') ch; map_to_eps (ksPSpace s') = map_to_eps (ksPSpace s); map_to_ntfns (ksPSpace s') = map_to_ntfns (ksPSpace s); map_to_pdes (ksPSpace s') = map_to_pdes (ksPSpace s); map_to_ptes (ksPSpace s') = map_to_ptes (ksPSpace s); map_to_asidpools (ksPSpace s') = map_to_asidpools (ksPSpace s); map_to_tcbs (ksPSpace s') = map_to_tcbs (ksPSpace s); map_to_cnes (ksPSpace s') = map_to_cnes (ksPSpace s); map_to_user_data (ksPSpace s') = map_to_user_data (ksPSpace s); map_to_user_data_device (ksPSpace s') = map_to_user_data_device (ksPSpace s)\<rbrakk> \<Longrightarrow> ksPSpace s' = ksPSpace s proof (prove)
goal (1 subgoal):
 1. \<lbrakk>cpspace_pde_array_relation (ksPSpace s) ch; cpspace_pte_array_relation (ksPSpace s) ch; cpspace_pde_array_relation (ksPSpace s') ch; cpspace_pte_array_relation (ksPSpace s') ch; map_to_eps (ksPSpace s') = map_to_eps (ksPSpace s); map_to_ntfns (ksPSpace s') = map_to_ntfns (ksPSpace s); map_to_pdes (ksPSpace s') = map_to_pdes (ksPSpace s); map_to_ptes (ksPSpace s') = map_to_ptes (ksPSpace s); map_to_asidpools (ksPSpace s') = map_to_asidpools (ksPSpace s); map_to_tcbs (ksPSpace s') = map_to_tcbs (ksPSpace s); map_to_cnes (ksPSpace s') = map_to_cnes (ksPSpace s); map_to_user_data (ksPSpace s') = map_to_user_data (ksPSpace s); map_to_user_data_device (ksPSpace s') = map_to_user_data_device (ksPSpace s)\<rbrakk> \<Longrightarrow> ksPSpace s' = ksPSpace s proof (prove)
goal (1 subgoal):
 1. \<lbrakk>cpspace_pde_array_relation (ksPSpace s) ch; cpspace_pte_array_relation (ksPSpace s) ch; cpspace_pde_array_relation (ksPSpace s') ch; cpspace_pte_array_relation (ksPSpace s') ch; map_to_eps (ksPSpace s') = map_to_eps (ksPSpace s); map_to_ntfns (ksPSpace s') = map_to_ntfns (ksPSpace s); map_to_pdes (ksPSpace s') = map_to_pdes (ksPSpace s); map_to_ptes (ksPSpace s') = map_to_ptes (ksPSpace s); map_to_asidpools (ksPSpace s') = map_to_asidpools (ksPSpace s); map_to_tcbs (ksPSpace s') = map_to_tcbs (ksPSpace s); map_to_cnes (ksPSpace s') = map_to_cnes (ksPSpace s); map_to_user_data (ksPSpace s') = map_to_user_data (ksPSpace s); map_to_user_data_device (ksPSpace s') = map_to_user_data_device (ksPSpace s); KOKernelData \<notin> ran (ksPSpace s); KOKernelData \<notin> ran (ksPSpace s')\<rbrakk> \<Longrightarrow> ksPSpace s' = ksPSpace s proof (prove)
goal (1 subgoal):
 1. \<And>x. \<lbrakk>cpspace_pde_array_relation (ksPSpace s) ch; cpspace_pte_array_relation (ksPSpace s) ch; \<forall>x. map_to_eps (ksPSpace s') x = map_to_eps (ksPSpace s) x; \<forall>x. map_to_ntfns (ksPSpace s') x = map_to_ntfns (ksPSpace s) x; \<forall>x. map_to_pdes (ksPSpace s') x = map_to_pdes (ksPSpace s) x; \<forall>x. map_to_ptes (ksPSpace s') x = map_to_ptes (ksPSpace s) x; \<forall>x. map_to_asidpools (ksPSpace s') x = map_to_asidpools (ksPSpace s) x; \<forall>x. map_to_tcbs (ksPSpace s') x = map_to_tcbs (ksPSpace s) x; \<forall>x. map_to_cnes (ksPSpace s') x = map_to_cnes (ksPSpace s) x; \<forall>x. map_to_user_data (ksPSpace s') x = map_to_user_data (ksPSpace s) x; \<forall>x. map_to_user_data_device (ksPSpace s') x = map_to_user_data_device (ksPSpace s) x; \<forall>a. ksPSpace s a \<noteq> Some KOKernelData; \<forall>a. ksPSpace s' a \<noteq> Some KOKernelData\<rbrakk> \<Longrightarrow> ksPSpace s' x = ksPSpace s x proof (prove)
goal (1 subgoal):
 1. \<And>x. \<lbrakk>cpspace_pde_array_relation (ksPSpace s) ch; cpspace_pte_array_relation (ksPSpace s) ch; map_to_eps (ksPSpace s') x = map_to_eps (ksPSpace s) x; map_to_ntfns (ksPSpace s') x = map_to_ntfns (ksPSpace s) x; map_to_pdes (ksPSpace s') x = map_to_pdes (ksPSpace s) x; map_to_ptes (ksPSpace s') x = map_to_ptes (ksPSpace s) x; map_to_asidpools (ksPSpace s') x = map_to_asidpools (ksPSpace s) x; map_to_tcbs (ksPSpace s') x = map_to_tcbs (ksPSpace s) x; map_to_cnes (ksPSpace s') x = map_to_cnes (ksPSpace s) x; map_to_user_data (ksPSpace s') x = map_to_user_data (ksPSpace s) x; map_to_user_data_device (ksPSpace s') x = map_to_user_data_device (ksPSpace s) x; ksPSpace s x \<noteq> Some KOKernelData; ksPSpace s' x \<noteq> Some KOKernelData\<rbrakk> \<Longrightarrow> ksPSpace s' x = ksPSpace s x proof (prove)
goal (2 subgoals):
 1. \<And>x. \<lbrakk>cpspace_pde_array_relation (ksPSpace s) ch; cpspace_pte_array_relation (ksPSpace s) ch; map_to_eps (ksPSpace s') x = map_to_eps (ksPSpace s) x; map_to_ntfns (ksPSpace s') x = map_to_ntfns (ksPSpace s) x; map_to_pdes (ksPSpace s') x = map_to_pdes (ksPSpace s) x; map_to_ptes (ksPSpace s') x = map_to_ptes (ksPSpace s) x; map_to_asidpools (ksPSpace s') x = map_to_asidpools (ksPSpace s) x; map_to_tcbs (ksPSpace s') x = map_to_tcbs (ksPSpace s) x; map_to_cnes (ksPSpace s') x = map_to_cnes (ksPSpace s) x; map_to_user_data (ksPSpace s') x = map_to_user_data (ksPSpace s) x; map_to_user_data_device (ksPSpace s') x = map_to_user_data_device (ksPSpace s) x; ksPSpace s x \<noteq> Some KOKernelData; ksPSpace s' x \<noteq> Some KOKernelData; ksPSpace s x = None\<rbrakk> \<Longrightarrow> ksPSpace s' x = ksPSpace s x
 2. \<And>x a. \<lbrakk>cpspace_pde_array_relation (ksPSpace s) ch; cpspace_pte_array_relation (ksPSpace s) ch; map_to_eps (ksPSpace s') x = map_to_eps (ksPSpace s) x; map_to_ntfns (ksPSpace s') x = map_to_ntfns (ksPSpace s) x; map_to_pdes (ksPSpace s') x = map_to_pdes (ksPSpace s) x; map_to_ptes (ksPSpace s') x = map_to_ptes (ksPSpace s) x; map_to_asidpools (ksPSpace s') x = map_to_asidpools (ksPSpace s) x; map_to_tcbs (ksPSpace s') x = map_to_tcbs (ksPSpace s) x; map_to_cnes (ksPSpace s') x = map_to_cnes (ksPSpace s) x; map_to_user_data (ksPSpace s') x = map_to_user_data (ksPSpace s) x; map_to_user_data_device (ksPSpace s') x = map_to_user_data_device (ksPSpace s) x; ksPSpace s x \<noteq> Some KOKernelData; ksPSpace s' x \<noteq> Some KOKernelData; ksPSpace s x = Some a\<rbrakk> \<Longrightarrow> ksPSpace s' x = ksPSpace s x proof (prove)
goal (2 subgoals):
 1. \<And>x a. \<lbrakk>cpspace_pde_array_relation (ksPSpace s) ch; cpspace_pte_array_relation (ksPSpace s) ch; map_to_eps (ksPSpace s') x = map_to_eps (ksPSpace s) x; map_to_ntfns (ksPSpace s') x = map_to_ntfns (ksPSpace s) x; map_to_pdes (ksPSpace s') x = map_to_pdes (ksPSpace s) x; map_to_ptes (ksPSpace s') x = map_to_ptes (ksPSpace s) x; map_to_asidpools (ksPSpace s') x = map_to_asidpools (ksPSpace s) x; map_to_tcbs (ksPSpace s') x = map_to_tcbs (ksPSpace s) x; map_to_cnes (ksPSpace s') x = map_to_cnes (ksPSpace s) x; map_to_user_data (ksPSpace s') x = map_to_user_data (ksPSpace s) x; map_to_user_data_device (ksPSpace s') x = map_to_user_data_device (ksPSpace s) x; ksPSpace s x \<noteq> Some KOKernelData; ksPSpace s' x \<noteq> Some KOKernelData; ksPSpace s x = None; ksPSpace s' x = Some a\<rbrakk> \<Longrightarrow> ksPSpace s' x = ksPSpace s x
 2. \<And>x a. \<lbrakk>cpspace_pde_array_relation (ksPSpace s) ch; cpspace_pte_array_relation (ksPSpace s) ch; map_to_eps (ksPSpace s') x = map_to_eps (ksPSpace s) x; map_to_ntfns (ksPSpace s') x = map_to_ntfns (ksPSpace s) x; map_to_pdes (ksPSpace s') x = map_to_pdes (ksPSpace s) x; map_to_ptes (ksPSpace s') x = map_to_ptes (ksPSpace s) x; map_to_asidpools (ksPSpace s') x = map_to_asidpools (ksPSpace s) x; map_to_tcbs (ksPSpace s') x = map_to_tcbs (ksPSpace s) x; map_to_cnes (ksPSpace s') x = map_to_cnes (ksPSpace s) x; map_to_user_data (ksPSpace s') x = map_to_user_data (ksPSpace s) x; map_to_user_data_device (ksPSpace s') x = map_to_user_data_device (ksPSpace s) x; ksPSpace s x \<noteq> Some KOKernelData; ksPSpace s' x \<noteq> Some KOKernelData; ksPSpace s x = Some a\<rbrakk> \<Longrightarrow> ksPSpace s' x = ksPSpace s x proof (prove)
goal (1 subgoal):
 1. \<And>x a. \<lbrakk>cpspace_pde_array_relation (ksPSpace s) ch; cpspace_pte_array_relation (ksPSpace s) ch; map_to_eps (ksPSpace s') x = (case a of KOEndpoint e \<Rightarrow> Some e | _ \<Rightarrow> None); map_to_ntfns (ksPSpace s') x = (case a of KONotification e \<Rightarrow> Some e | _ \<Rightarrow> None); map_to_pdes (ksPSpace s') x = (case a of KOArch (KOPDE e) \<Rightarrow> Some e | KOArch _ \<Rightarrow> None | _ \<Rightarrow> None); map_to_ptes (ksPSpace s') x = (case a of KOArch (KOPTE e) \<Rightarrow> Some e | KOArch _ \<Rightarrow> None | _ \<Rightarrow> None); map_to_asidpools (ksPSpace s') x = (case a of KOArch (KOASIDPool e) \<Rightarrow> Some e | KOArch _ \<Rightarrow> None | _ \<Rightarrow> None); map_to_tcbs (ksPSpace s') x = (case a of KOTCB e \<Rightarrow> Some e | _ \<Rightarrow> None); map_to_cnes (ksPSpace s') x = (case a of KOCTE e \<Rightarrow> Some e | _ \<Rightarrow> None); map_to_user_data (ksPSpace s') x = (case a of KOUserData \<Rightarrow> Some UserData | _ \<Rightarrow> None); map_to_user_data_device (ksPSpace s') x = (case a of KOUserDataDevice \<Rightarrow> Some UserDataDevice | _ \<Rightarrow> None); a \<noteq> KOKernelData; ksPSpace s' x \<noteq> Some KOKernelData; ksPSpace s x = Some a\<rbrakk> \<Longrightarrow> ksPSpace s' x = Some a proof (prove)
goal:
No subgoals! proof (state)
this:
\<lbrakk>cpspace_relation (ksPSpace s) bh ch; cpspace_relation (ksPSpace s') bh ch\<rbrakk> \<Longrightarrow> ksPSpace s' = ksPSpace s

goal:
No subgoals!