theory ArchUserOp_IF

lemma requiv_ptable_rights_eq:
  "\<lbrakk> reads_equiv aag s s'; pas_refined aag s; pas_refined aag s';
     is_subject aag (cur_thread s); invs s; invs s' \<rbrakk>
     \<Longrightarrow> ptable_rights_s s = ptable_rights_s s'" apply (simp add: ptable_rights_s_def) apply (rule ext) apply (case_tac "x \<in> kernel_mappings") apply (clarsimp simp: ptable_rights_def split: option.splits) apply (rule conjI) apply clarsimp apply (frule some_get_page_info_kmapsD) apply ((fastforce simp: invs_valid_global_pd_mappings invs_equal_kernel_mappings
                               vspace_cap_rights_to_auth_def)+)[4] apply clarsimp apply (frule some_get_page_info_kmapsD) apply ((fastforce simp: invs_valid_global_pd_mappings invs_equal_kernel_mappings
                              vspace_cap_rights_to_auth_def)+)[4] apply clarsimp apply (frule_tac r=b in some_get_page_info_kmapsD) apply ((fastforce simp: invs_valid_global_pd_mappings invs_equal_kernel_mappings
                              vspace_cap_rights_to_auth_def)+)[4] apply (case_tac "get_pd_of_thread (kheap s) (arch_state s) (cur_thread s) =
                   arm_global_pd (arch_state s)") apply (frule requiv_pd_of_thread_global_pd) apply (fastforce+)[4] apply (clarsimp simp: ptable_rights_def split: option.splits) apply (rule conjI) apply clarsimp apply (frule get_page_info_gpd_kmaps[rotated, rotated]) apply ((fastforce simp: invs_valid_global_objs invs_arch_state)+)[3] apply clarsimp apply (rule conjI) apply clarsimp apply (frule get_page_info_gpd_kmaps[rotated, rotated]) apply ((fastforce simp: invs_valid_global_objs invs_arch_state)+)[3] apply clarsimp apply (frule get_page_info_gpd_kmaps[rotated, rotated]) apply ((fastforce simp: invs_valid_global_objs invs_arch_state)+)[3] apply (case_tac "get_pd_of_thread (kheap s') (arch_state s') (cur_thread s') =
                   arm_global_pd (arch_state s')") apply (drule reads_equiv_sym) apply (frule requiv_pd_of_thread_global_pd) apply ((fastforce simp: reads_equiv_def)+)[5] apply (simp add: ptable_rights_def) apply (frule requiv_get_pd_of_thread_eq) apply (fastforce+)[6] apply (frule pd_of_thread_same_agent, simp+) apply (subst requiv_get_page_info_eq, simp+) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>reads_equiv aag s s'; pas_refined aag s; pas_refined aag s'; is_subject aag (cur_thread s); invs s; invs s'\<rbrakk> \<Longrightarrow> ptable_rights_s s = ptable_rights_s s' proof (prove)
goal (1 subgoal):
 1. \<lbrakk>reads_equiv aag s s'; pas_refined aag s; pas_refined aag s'; is_subject aag (cur_thread s); invs s; invs s'\<rbrakk> \<Longrightarrow> ptable_rights (cur_thread s) s = ptable_rights (cur_thread s') s' proof (prove)
goal (1 subgoal):
 1. \<And>x. \<lbrakk>reads_equiv aag s s'; pas_refined aag s; pas_refined aag s'; is_subject aag (cur_thread s); invs s; invs s'\<rbrakk> \<Longrightarrow> ptable_rights (cur_thread s) s x = ptable_rights (cur_thread s') s' x proof (prove)
goal (2 subgoals):
 1. \<And>x. \<lbrakk>reads_equiv aag s s'; pas_refined aag s; pas_refined aag s'; is_subject aag (cur_thread s); invs s; invs s'; x \<in> kernel_mappings\<rbrakk> \<Longrightarrow> ptable_rights (cur_thread s) s x = ptable_rights (cur_thread s') s' x
 2. \<And>x. \<lbrakk>reads_equiv aag s s'; pas_refined aag s; pas_refined aag s'; is_subject aag (cur_thread s); invs s; invs s'; x \<notin> kernel_mappings\<rbrakk> \<Longrightarrow> ptable_rights (cur_thread s) s x = ptable_rights (cur_thread s') s' x proof (prove)
goal (2 subgoals):
 1. \<And>x. \<lbrakk>reads_equiv aag s s'; pas_refined aag s; pas_refined aag s'; is_subject aag (cur_thread s); invs s; invs s'; x \<in> kernel_mappings\<rbrakk> \<Longrightarrow> (get_page_info (\<lambda>obj. get_arch_obj (kheap s obj)) (get_pd_of_thread (kheap s) (arch_state s) (cur_thread s)) x = None \<longrightarrow> (\<forall>a aa ab b. get_page_info (\<lambda>obj. get_arch_obj (kheap s' obj)) (get_pd_of_thread (kheap s') (arch_state s') (cur_thread s')) x = Some (a, aa, ab, b) \<longrightarrow> {} = b)) \<and> (\<forall>a aa ab b. get_page_info (\<lambda>obj. get_arch_obj (kheap s obj)) (get_pd_of_thread (kheap s) (arch_state s) (cur_thread s)) x = Some (a, aa, ab, b) \<longrightarrow> (get_page_info (\<lambda>obj. get_arch_obj (kheap s' obj)) (get_pd_of_thread (kheap s') (arch_state s') (cur_thread s')) x = None \<longrightarrow> b = {}) \<and> (\<forall>a aa ab ba. get_page_info (\<lambda>obj. get_arch_obj (kheap s' obj)) (get_pd_of_thread (kheap s') (arch_state s') (cur_thread s')) x = Some (a, aa, ab, ba) \<longrightarrow> b = ba))
 2. \<And>x. \<lbrakk>reads_equiv aag s s'; pas_refined aag s; pas_refined aag s'; is_subject aag (cur_thread s); invs s; invs s'; x \<notin> kernel_mappings\<rbrakk> \<Longrightarrow> ptable_rights (cur_thread s) s x = ptable_rights (cur_thread s') s' x proof (prove)
goal (3 subgoals):
 1. \<And>x. \<lbrakk>reads_equiv aag s s'; pas_refined aag s; pas_refined aag s'; is_subject aag (cur_thread s); invs s; invs s'; x \<in> kernel_mappings\<rbrakk> \<Longrightarrow> get_page_info (\<lambda>obj. get_arch_obj (kheap s obj)) (get_pd_of_thread (kheap s) (arch_state s) (cur_thread s)) x = None \<longrightarrow> (\<forall>a aa ab b. get_page_info (\<lambda>obj. get_arch_obj (kheap s' obj)) (get_pd_of_thread (kheap s') (arch_state s') (cur_thread s')) x = Some (a, aa, ab, b) \<longrightarrow> {} = b)
 2. \<And>x. \<lbrakk>reads_equiv aag s s'; pas_refined aag s; pas_refined aag s'; is_subject aag (cur_thread s); invs s; invs s'; x \<in> kernel_mappings\<rbrakk> \<Longrightarrow> \<forall>a aa ab b. get_page_info (\<lambda>obj. get_arch_obj (kheap s obj)) (get_pd_of_thread (kheap s) (arch_state s) (cur_thread s)) x = Some (a, aa, ab, b) \<longrightarrow> (get_page_info (\<lambda>obj. get_arch_obj (kheap s' obj)) (get_pd_of_thread (kheap s') (arch_state s') (cur_thread s')) x = None \<longrightarrow> b = {}) \<and> (\<forall>a aa ab ba. get_page_info (\<lambda>obj. get_arch_obj (kheap s' obj)) (get_pd_of_thread (kheap s') (arch_state s') (cur_thread s')) x = Some (a, aa, ab, ba) \<longrightarrow> b = ba)
 3. \<And>x. \<lbrakk>reads_equiv aag s s'; pas_refined aag s; pas_refined aag s'; is_subject aag (cur_thread s); invs s; invs s'; x \<notin> kernel_mappings\<rbrakk> \<Longrightarrow> ptable_rights (cur_thread s) s x = ptable_rights (cur_thread s') s' x proof (prove)
goal (3 subgoals):
 1. \<And>x a aa ab b. \<lbrakk>reads_equiv aag s s'; pas_refined aag s; pas_refined aag s'; is_subject aag (cur_thread s); invs s; invs s'; x \<in> kernel_mappings; get_page_info (\<lambda>obj. get_arch_obj (kheap s obj)) (get_pd_of_thread (kheap s) (arch_state s) (cur_thread s)) x = None; get_page_info (\<lambda>obj. get_arch_obj (kheap s' obj)) (get_pd_of_thread (kheap s') (arch_state s') (cur_thread s')) x = Some (a, aa, ab, b)\<rbrakk> \<Longrightarrow> {} = b
 2. \<And>x. \<lbrakk>reads_equiv aag s s'; pas_refined aag s; pas_refined aag s'; is_subject aag (cur_thread s); invs s; invs s'; x \<in> kernel_mappings\<rbrakk> \<Longrightarrow> \<forall>a aa ab b. get_page_info (\<lambda>obj. get_arch_obj (kheap s obj)) (get_pd_of_thread (kheap s) (arch_state s) (cur_thread s)) x = Some (a, aa, ab, b) \<longrightarrow> (get_page_info (\<lambda>obj. get_arch_obj (kheap s' obj)) (get_pd_of_thread (kheap s') (arch_state s') (cur_thread s')) x = None \<longrightarrow> b = {}) \<and> (\<forall>a aa ab ba. get_page_info (\<lambda>obj. get_arch_obj (kheap s' obj)) (get_pd_of_thread (kheap s') (arch_state s') (cur_thread s')) x = Some (a, aa, ab, ba) \<longrightarrow> b = ba)
 3. \<And>x. \<lbrakk>reads_equiv aag s s'; pas_refined aag s; pas_refined aag s'; is_subject aag (cur_thread s); invs s; invs s'; x \<notin> kernel_mappings\<rbrakk> \<Longrightarrow> ptable_rights (cur_thread s) s x = ptable_rights (cur_thread s') s' x proof (prove)
goal (6 subgoals):
 1. \<And>x a aa ab b. \<lbrakk>reads_equiv aag s s'; pas_refined aag s; pas_refined aag s'; is_subject aag (cur_thread s); invs s; invs s'; x \<in> kernel_mappings; get_page_info (\<lambda>obj. get_arch_obj (kheap s obj)) (get_pd_of_thread (kheap s) (arch_state s) (cur_thread s)) x = None; get_page_info (\<lambda>obj. get_arch_obj (kheap s' obj)) (get_pd_of_thread (kheap s') (arch_state s') (cur_thread s')) x = Some (a, aa, ab, b)\<rbrakk> \<Longrightarrow> x \<in> kernel_mappings
 2. \<And>x a aa ab b. \<lbrakk>reads_equiv aag s s'; pas_refined aag s; pas_refined aag s'; is_subject aag (cur_thread s); invs s; invs s'; x \<in> kernel_mappings; get_page_info (\<lambda>obj. get_arch_obj (kheap s obj)) (get_pd_of_thread (kheap s) (arch_state s) (cur_thread s)) x = None; get_page_info (\<lambda>obj. get_arch_obj (kheap s' obj)) (get_pd_of_thread (kheap s') (arch_state s') (cur_thread s')) x = Some (a, aa, ab, b)\<rbrakk> \<Longrightarrow> valid_global_vspace_mappings s'
 3. \<And>x a aa ab b. \<lbrakk>reads_equiv aag s s'; pas_refined aag s; pas_refined aag s'; is_subject aag (cur_thread s); invs s; invs s'; x \<in> kernel_mappings; get_page_info (\<lambda>obj. get_arch_obj (kheap s obj)) (get_pd_of_thread (kheap s) (arch_state s) (cur_thread s)) x = None; get_page_info (\<lambda>obj. get_arch_obj (kheap s' obj)) (get_pd_of_thread (kheap s') (arch_state s') (cur_thread s')) x = Some (a, aa, ab, b)\<rbrakk> \<Longrightarrow> equal_kernel_mappings s'
 4. \<And>x a aa ab b. \<lbrakk>reads_equiv aag s s'; pas_refined aag s; pas_refined aag s'; is_subject aag (cur_thread s); invs s; invs s'; x \<in> kernel_mappings; get_page_info (\<lambda>obj. get_arch_obj (kheap s obj)) (get_pd_of_thread (kheap s) (arch_state s) (cur_thread s)) x = None; get_page_info (\<lambda>obj. get_arch_obj (kheap s' obj)) (get_pd_of_thread (kheap s') (arch_state s') (cur_thread s')) x = Some (a, aa, ab, b); (\<exists>sz. pageBitsForSize sz = aa) \<and> b = {}\<rbrakk> \<Longrightarrow> {} = b
 5. \<And>x. \<lbrakk>reads_equiv aag s s'; pas_refined aag s; pas_refined aag s'; is_subject aag (cur_thread s); invs s; invs s'; x \<in> kernel_mappings\<rbrakk> \<Longrightarrow> \<forall>a aa ab b. get_page_info (\<lambda>obj. get_arch_obj (kheap s obj)) (get_pd_of_thread (kheap s) (arch_state s) (cur_thread s)) x = Some (a, aa, ab, b) \<longrightarrow> (get_page_info (\<lambda>obj. get_arch_obj (kheap s' obj)) (get_pd_of_thread (kheap s') (arch_state s') (cur_thread s')) x = None \<longrightarrow> b = {}) \<and> (\<forall>a aa ab ba. get_page_info (\<lambda>obj. get_arch_obj (kheap s' obj)) (get_pd_of_thread (kheap s') (arch_state s') (cur_thread s')) x = Some (a, aa, ab, ba) \<longrightarrow> b = ba)
 6. \<And>x. \<lbrakk>reads_equiv aag s s'; pas_refined aag s; pas_refined aag s'; is_subject aag (cur_thread s); invs s; invs s'; x \<notin> kernel_mappings\<rbrakk> \<Longrightarrow> ptable_rights (cur_thread s) s x = ptable_rights (cur_thread s') s' x proof (prove)
goal (2 subgoals):
 1. \<And>x. \<lbrakk>reads_equiv aag s s'; pas_refined aag s; pas_refined aag s'; is_subject aag (cur_thread s); invs s; invs s'; x \<in> kernel_mappings\<rbrakk> \<Longrightarrow> \<forall>a aa ab b. get_page_info (\<lambda>obj. get_arch_obj (kheap s obj)) (get_pd_of_thread (kheap s) (arch_state s) (cur_thread s)) x = Some (a, aa, ab, b) \<longrightarrow> (get_page_info (\<lambda>obj. get_arch_obj (kheap s' obj)) (get_pd_of_thread (kheap s') (arch_state s') (cur_thread s')) x = None \<longrightarrow> b = {}) \<and> (\<forall>a aa ab ba. get_page_info (\<lambda>obj. get_arch_obj (kheap s' obj)) (get_pd_of_thread (kheap s') (arch_state s') (cur_thread s')) x = Some (a, aa, ab, ba) \<longrightarrow> b = ba)
 2. \<And>x. \<lbrakk>reads_equiv aag s s'; pas_refined aag s; pas_refined aag s'; is_subject aag (cur_thread s); invs s; invs s'; x \<notin> kernel_mappings\<rbrakk> \<Longrightarrow> ptable_rights (cur_thread s) s x = ptable_rights (cur_thread s') s' x proof (prove)
goal (2 subgoals):
 1. \<And>x a aa ab b. \<lbrakk>reads_equiv aag s s'; pas_refined aag s; pas_refined aag s'; is_subject aag (cur_thread s); invs s; invs s'; x \<in> kernel_mappings; get_page_info (\<lambda>obj. get_arch_obj (kheap s obj)) (get_pd_of_thread (kheap s) (arch_state s) (cur_thread s)) x = Some (a, aa, ab, b)\<rbrakk> \<Longrightarrow> (get_page_info (\<lambda>obj. get_arch_obj (kheap s' obj)) (get_pd_of_thread (kheap s') (arch_state s') (cur_thread s')) x = None \<longrightarrow> b = {}) \<and> (\<forall>a aa ab ba. get_page_info (\<lambda>obj. get_arch_obj (kheap s' obj)) (get_pd_of_thread (kheap s') (arch_state s') (cur_thread s')) x = Some (a, aa, ab, ba) \<longrightarrow> b = ba)
 2. \<And>x. \<lbrakk>reads_equiv aag s s'; pas_refined aag s; pas_refined aag s'; is_subject aag (cur_thread s); invs s; invs s'; x \<notin> kernel_mappings\<rbrakk> \<Longrightarrow> ptable_rights (cur_thread s) s x = ptable_rights (cur_thread s') s' x proof (prove)
goal (5 subgoals):
 1. \<And>x a aa ab b. \<lbrakk>reads_equiv aag s s'; pas_refined aag s; pas_refined aag s'; is_subject aag (cur_thread s); invs s; invs s'; x \<in> kernel_mappings; get_page_info (\<lambda>obj. get_arch_obj (kheap s obj)) (get_pd_of_thread (kheap s) (arch_state s) (cur_thread s)) x = Some (a, aa, ab, b)\<rbrakk> \<Longrightarrow> x \<in> kernel_mappings
 2. \<And>x a aa ab b. \<lbrakk>reads_equiv aag s s'; pas_refined aag s; pas_refined aag s'; is_subject aag (cur_thread s); invs s; invs s'; x \<in> kernel_mappings; get_page_info (\<lambda>obj. get_arch_obj (kheap s obj)) (get_pd_of_thread (kheap s) (arch_state s) (cur_thread s)) x = Some (a, aa, ab, b)\<rbrakk> \<Longrightarrow> valid_global_vspace_mappings s
 3. \<And>x a aa ab b. \<lbrakk>reads_equiv aag s s'; pas_refined aag s; pas_refined aag s'; is_subject aag (cur_thread s); invs s; invs s'; x \<in> kernel_mappings; get_page_info (\<lambda>obj. get_arch_obj (kheap s obj)) (get_pd_of_thread (kheap s) (arch_state s) (cur_thread s)) x = Some (a, aa, ab, b)\<rbrakk> \<Longrightarrow> equal_kernel_mappings s
 4. \<And>x a aa ab b. \<lbrakk>reads_equiv aag s s'; pas_refined aag s; pas_refined aag s'; is_subject aag (cur_thread s); invs s; invs s'; x \<in> kernel_mappings; get_page_info (\<lambda>obj. get_arch_obj (kheap s obj)) (get_pd_of_thread (kheap s) (arch_state s) (cur_thread s)) x = Some (a, aa, ab, b); (\<exists>sz. pageBitsForSize sz = aa) \<and> b = {}\<rbrakk> \<Longrightarrow> (get_page_info (\<lambda>obj. get_arch_obj (kheap s' obj)) (get_pd_of_thread (kheap s') (arch_state s') (cur_thread s')) x = None \<longrightarrow> b = {}) \<and> (\<forall>a aa ab ba. get_page_info (\<lambda>obj. get_arch_obj (kheap s' obj)) (get_pd_of_thread (kheap s') (arch_state s') (cur_thread s')) x = Some (a, aa, ab, ba) \<longrightarrow> b = ba)
 5. \<And>x. \<lbrakk>reads_equiv aag s s'; pas_refined aag s; pas_refined aag s'; is_subject aag (cur_thread s); invs s; invs s'; x \<notin> kernel_mappings\<rbrakk> \<Longrightarrow> ptable_rights (cur_thread s) s x = ptable_rights (cur_thread s') s' x proof (prove)
goal (2 subgoals):
 1. \<And>x a aa ab b. \<lbrakk>reads_equiv aag s s'; pas_refined aag s; pas_refined aag s'; is_subject aag (cur_thread s); invs s; invs s'; x \<in> kernel_mappings; get_page_info (\<lambda>obj. get_arch_obj (kheap s obj)) (get_pd_of_thread (kheap s) (arch_state s) (cur_thread s)) x = Some (a, aa, ab, b); (\<exists>sz. pageBitsForSize sz = aa) \<and> b = {}\<rbrakk> \<Longrightarrow> (get_page_info (\<lambda>obj. get_arch_obj (kheap s' obj)) (get_pd_of_thread (kheap s') (arch_state s') (cur_thread s')) x = None \<longrightarrow> b = {}) \<and> (\<forall>a aa ab ba. get_page_info (\<lambda>obj. get_arch_obj (kheap s' obj)) (get_pd_of_thread (kheap s') (arch_state s') (cur_thread s')) x = Some (a, aa, ab, ba) \<longrightarrow> b = ba)
 2. \<And>x. \<lbrakk>reads_equiv aag s s'; pas_refined aag s; pas_refined aag s'; is_subject aag (cur_thread s); invs s; invs s'; x \<notin> kernel_mappings\<rbrakk> \<Longrightarrow> ptable_rights (cur_thread s) s x = ptable_rights (cur_thread s') s' x proof (prove)
goal (2 subgoals):
 1. \<And>x a ab sz ac ad ae b. \<lbrakk>reads_equiv aag s s'; pas_refined aag s; pas_refined aag s'; is_subject aag (cur_thread s); invs s; invs s'; x \<in> kernel_mappings; get_page_info (\<lambda>obj. get_arch_obj (kheap s obj)) (get_pd_of_thread (kheap s) (arch_state s) (cur_thread s)) x = Some (a, pageBitsForSize sz, ab, {}); get_page_info (\<lambda>obj. get_arch_obj (kheap s' obj)) (get_pd_of_thread (kheap s') (arch_state s') (cur_thread s')) x = Some (ac, ad, ae, b)\<rbrakk> \<Longrightarrow> {} = b
 2. \<And>x. \<lbrakk>reads_equiv aag s s'; pas_refined aag s; pas_refined aag s'; is_subject aag (cur_thread s); invs s; invs s'; x \<notin> kernel_mappings\<rbrakk> \<Longrightarrow> ptable_rights (cur_thread s) s x = ptable_rights (cur_thread s') s' x proof (prove)
goal (5 subgoals):
 1. \<And>x a ab sz ac ad ae b. \<lbrakk>reads_equiv aag s s'; pas_refined aag s; pas_refined aag s'; is_subject aag (cur_thread s); invs s; invs s'; x \<in> kernel_mappings; get_page_info (\<lambda>obj. get_arch_obj (kheap s obj)) (get_pd_of_thread (kheap s) (arch_state s) (cur_thread s)) x = Some (a, pageBitsForSize sz, ab, {}); get_page_info (\<lambda>obj. get_arch_obj (kheap s' obj)) (get_pd_of_thread (kheap s') (arch_state s') (cur_thread s')) x = Some (ac, ad, ae, b)\<rbrakk> \<Longrightarrow> x \<in> kernel_mappings
 2. \<And>x a ab sz ac ad ae b. \<lbrakk>reads_equiv aag s s'; pas_refined aag s; pas_refined aag s'; is_subject aag (cur_thread s); invs s; invs s'; x \<in> kernel_mappings; get_page_info (\<lambda>obj. get_arch_obj (kheap s obj)) (get_pd_of_thread (kheap s) (arch_state s) (cur_thread s)) x = Some (a, pageBitsForSize sz, ab, {}); get_page_info (\<lambda>obj. get_arch_obj (kheap s' obj)) (get_pd_of_thread (kheap s') (arch_state s') (cur_thread s')) x = Some (ac, ad, ae, b)\<rbrakk> \<Longrightarrow> valid_global_vspace_mappings s'
 3. \<And>x a ab sz ac ad ae b. \<lbrakk>reads_equiv aag s s'; pas_refined aag s; pas_refined aag s'; is_subject aag (cur_thread s); invs s; invs s'; x \<in> kernel_mappings; get_page_info (\<lambda>obj. get_arch_obj (kheap s obj)) (get_pd_of_thread (kheap s) (arch_state s) (cur_thread s)) x = Some (a, pageBitsForSize sz, ab, {}); get_page_info (\<lambda>obj. get_arch_obj (kheap s' obj)) (get_pd_of_thread (kheap s') (arch_state s') (cur_thread s')) x = Some (ac, ad, ae, b)\<rbrakk> \<Longrightarrow> equal_kernel_mappings s'
 4. \<And>x a ab sz ac ad ae b. \<lbrakk>reads_equiv aag s s'; pas_refined aag s; pas_refined aag s'; is_subject aag (cur_thread s); invs s; invs s'; x \<in> kernel_mappings; get_page_info (\<lambda>obj. get_arch_obj (kheap s obj)) (get_pd_of_thread (kheap s) (arch_state s) (cur_thread s)) x = Some (a, pageBitsForSize sz, ab, {}); get_page_info (\<lambda>obj. get_arch_obj (kheap s' obj)) (get_pd_of_thread (kheap s') (arch_state s') (cur_thread s')) x = Some (ac, ad, ae, b); (\<exists>sz. pageBitsForSize sz = ad) \<and> b = {}\<rbrakk> \<Longrightarrow> {} = b
 5. \<And>x. \<lbrakk>reads_equiv aag s s'; pas_refined aag s; pas_refined aag s'; is_subject aag (cur_thread s); invs s; invs s'; x \<notin> kernel_mappings\<rbrakk> \<Longrightarrow> ptable_rights (cur_thread s) s x = ptable_rights (cur_thread s') s' x proof (prove)
goal (1 subgoal):
 1. \<And>x. \<lbrakk>reads_equiv aag s s'; pas_refined aag s; pas_refined aag s'; is_subject aag (cur_thread s); invs s; invs s'; x \<notin> kernel_mappings\<rbrakk> \<Longrightarrow> ptable_rights (cur_thread s) s x = ptable_rights (cur_thread s') s' x proof (prove)
goal (2 subgoals):
 1. \<And>x. \<lbrakk>reads_equiv aag s s'; pas_refined aag s; pas_refined aag s'; is_subject aag (cur_thread s); invs s; invs s'; x \<notin> kernel_mappings; get_pd_of_thread (kheap s) (arch_state s) (cur_thread s) = arm_global_pd (arch_state s)\<rbrakk> \<Longrightarrow> ptable_rights (cur_thread s) s x = ptable_rights (cur_thread s') s' x
 2. \<And>x. \<lbrakk>reads_equiv aag s s'; pas_refined aag s; pas_refined aag s'; is_subject aag (cur_thread s); invs s; invs s'; x \<notin> kernel_mappings; get_pd_of_thread (kheap s) (arch_state s) (cur_thread s) \<noteq> arm_global_pd (arch_state s)\<rbrakk> \<Longrightarrow> ptable_rights (cur_thread s) s x = ptable_rights (cur_thread s') s' x proof (prove)
goal (6 subgoals):
 1. \<And>x. \<lbrakk>reads_equiv aag s s'; pas_refined aag s; pas_refined aag s'; is_subject aag (cur_thread s); invs s; invs s'; x \<notin> kernel_mappings; get_pd_of_thread (kheap s) (arch_state s) (cur_thread s) = arm_global_pd (arch_state s)\<rbrakk> \<Longrightarrow> is_subject aag (cur_thread s)
 2. \<And>x. \<lbrakk>reads_equiv aag s s'; pas_refined aag s; pas_refined aag s'; is_subject aag (cur_thread s); invs s; invs s'; x \<notin> kernel_mappings; get_pd_of_thread (kheap s) (arch_state s) (cur_thread s) = arm_global_pd (arch_state s)\<rbrakk> \<Longrightarrow> invs s
 3. \<And>x. \<lbrakk>reads_equiv aag s s'; pas_refined aag s; pas_refined aag s'; is_subject aag (cur_thread s); invs s; invs s'; x \<notin> kernel_mappings; get_pd_of_thread (kheap s) (arch_state s) (cur_thread s) = arm_global_pd (arch_state s)\<rbrakk> \<Longrightarrow> pas_refined aag s
 4. \<And>x. \<lbrakk>reads_equiv aag s s'; pas_refined aag s; pas_refined aag s'; is_subject aag (cur_thread s); invs s; invs s'; x \<notin> kernel_mappings; get_pd_of_thread (kheap s) (arch_state s) (cur_thread s) = arm_global_pd (arch_state s)\<rbrakk> \<Longrightarrow> get_pd_of_thread (kheap s) (arch_state s) (cur_thread s) = arm_global_pd (arch_state s)
 5. \<And>x. \<lbrakk>reads_equiv aag s s'; pas_refined aag s; pas_refined aag s'; is_subject aag (cur_thread s); invs s; invs s'; x \<notin> kernel_mappings; get_pd_of_thread (kheap s) (arch_state s) (cur_thread s) = arm_global_pd (arch_state s); get_pd_of_thread (kheap s') (arch_state s') (cur_thread s') = arm_global_pd (arch_state s')\<rbrakk> \<Longrightarrow> ptable_rights (cur_thread s) s x = ptable_rights (cur_thread s') s' x
 6. \<And>x. \<lbrakk>reads_equiv aag s s'; pas_refined aag s; pas_refined aag s'; is_subject aag (cur_thread s); invs s; invs s'; x \<notin> kernel_mappings; get_pd_of_thread (kheap s) (arch_state s) (cur_thread s) \<noteq> arm_global_pd (arch_state s)\<rbrakk> \<Longrightarrow> ptable_rights (cur_thread s) s x = ptable_rights (cur_thread s') s' x proof (prove)
goal (2 subgoals):
 1. \<And>x. \<lbrakk>reads_equiv aag s s'; pas_refined aag s; pas_refined aag s'; is_subject aag (cur_thread s); invs s; invs s'; x \<notin> kernel_mappings; get_pd_of_thread (kheap s) (arch_state s) (cur_thread s) = arm_global_pd (arch_state s); get_pd_of_thread (kheap s') (arch_state s') (cur_thread s') = arm_global_pd (arch_state s')\<rbrakk> \<Longrightarrow> ptable_rights (cur_thread s) s x = ptable_rights (cur_thread s') s' x
 2. \<And>x. \<lbrakk>reads_equiv aag s s'; pas_refined aag s; pas_refined aag s'; is_subject aag (cur_thread s); invs s; invs s'; x \<notin> kernel_mappings; get_pd_of_thread (kheap s) (arch_state s) (cur_thread s) \<noteq> arm_global_pd (arch_state s)\<rbrakk> \<Longrightarrow> ptable_rights (cur_thread s) s x = ptable_rights (cur_thread s') s' x proof (prove)
goal (2 subgoals):
 1. \<And>x. \<lbrakk>reads_equiv aag s s'; pas_refined aag s; pas_refined aag s'; is_subject aag (cur_thread s); invs s; invs s'; x \<notin> kernel_mappings; get_pd_of_thread (kheap s) (arch_state s) (cur_thread s) = arm_global_pd (arch_state s); get_pd_of_thread (kheap s') (arch_state s') (cur_thread s') = arm_global_pd (arch_state s')\<rbrakk> \<Longrightarrow> (get_page_info (\<lambda>obj. get_arch_obj (kheap s obj)) (arm_global_pd (arch_state s)) x = None \<longrightarrow> (\<forall>a aa ab b. get_page_info (\<lambda>obj. get_arch_obj (kheap s' obj)) (arm_global_pd (arch_state s')) x = Some (a, aa, ab, b) \<longrightarrow> {} = b)) \<and> (\<forall>a aa ab b. get_page_info (\<lambda>obj. get_arch_obj (kheap s obj)) (arm_global_pd (arch_state s)) x = Some (a, aa, ab, b) \<longrightarrow> (get_page_info (\<lambda>obj. get_arch_obj (kheap s' obj)) (arm_global_pd (arch_state s')) x = None \<longrightarrow> b = {}) \<and> (\<forall>a aa ab ba. get_page_info (\<lambda>obj. get_arch_obj (kheap s' obj)) (arm_global_pd (arch_state s')) x = Some (a, aa, ab, ba) \<longrightarrow> b = ba))
 2. \<And>x. \<lbrakk>reads_equiv aag s s'; pas_refined aag s; pas_refined aag s'; is_subject aag (cur_thread s); invs s; invs s'; x \<notin> kernel_mappings; get_pd_of_thread (kheap s) (arch_state s) (cur_thread s) \<noteq> arm_global_pd (arch_state s)\<rbrakk> \<Longrightarrow> ptable_rights (cur_thread s) s x = ptable_rights (cur_thread s') s' x proof (prove)
goal (3 subgoals):
 1. \<And>x. \<lbrakk>reads_equiv aag s s'; pas_refined aag s; pas_refined aag s'; is_subject aag (cur_thread s); invs s; invs s'; x \<notin> kernel_mappings; get_pd_of_thread (kheap s) (arch_state s) (cur_thread s) = arm_global_pd (arch_state s); get_pd_of_thread (kheap s') (arch_state s') (cur_thread s') = arm_global_pd (arch_state s')\<rbrakk> \<Longrightarrow> get_page_info (\<lambda>obj. get_arch_obj (kheap s obj)) (arm_global_pd (arch_state s)) x = None \<longrightarrow> (\<forall>a aa ab b. get_page_info (\<lambda>obj. get_arch_obj (kheap s' obj)) (arm_global_pd (arch_state s')) x = Some (a, aa, ab, b) \<longrightarrow> {} = b)
 2. \<And>x. \<lbrakk>reads_equiv aag s s'; pas_refined aag s; pas_refined aag s'; is_subject aag (cur_thread s); invs s; invs s'; x \<notin> kernel_mappings; get_pd_of_thread (kheap s) (arch_state s) (cur_thread s) = arm_global_pd (arch_state s); get_pd_of_thread (kheap s') (arch_state s') (cur_thread s') = arm_global_pd (arch_state s')\<rbrakk> \<Longrightarrow> \<forall>a aa ab b. get_page_info (\<lambda>obj. get_arch_obj (kheap s obj)) (arm_global_pd (arch_state s)) x = Some (a, aa, ab, b) \<longrightarrow> (get_page_info (\<lambda>obj. get_arch_obj (kheap s' obj)) (arm_global_pd (arch_state s')) x = None \<longrightarrow> b = {}) \<and> (\<forall>a aa ab ba. get_page_info (\<lambda>obj. get_arch_obj (kheap s' obj)) (arm_global_pd (arch_state s')) x = Some (a, aa, ab, ba) \<longrightarrow> b = ba)
 3. \<And>x. \<lbrakk>reads_equiv aag s s'; pas_refined aag s; pas_refined aag s'; is_subject aag (cur_thread s); invs s; invs s'; x \<notin> kernel_mappings; get_pd_of_thread (kheap s) (arch_state s) (cur_thread s) \<noteq> arm_global_pd (arch_state s)\<rbrakk> \<Longrightarrow> ptable_rights (cur_thread s) s x = ptable_rights (cur_thread s') s' x proof (prove)
goal (3 subgoals):
 1. \<And>x a aa ab b. \<lbrakk>reads_equiv aag s s'; pas_refined aag s; pas_refined aag s'; is_subject aag (cur_thread s); invs s; invs s'; x \<notin> kernel_mappings; get_pd_of_thread (kheap s) (arch_state s) (cur_thread s) = arm_global_pd (arch_state s); get_pd_of_thread (kheap s') (arch_state s') (cur_thread s') = arm_global_pd (arch_state s'); get_page_info (\<lambda>obj. get_arch_obj (kheap s obj)) (arm_global_pd (arch_state s)) x = None; get_page_info (\<lambda>obj. get_arch_obj (kheap s' obj)) (arm_global_pd (arch_state s')) x = Some (a, aa, ab, b)\<rbrakk> \<Longrightarrow> {} = b
 2. \<And>x. \<lbrakk>reads_equiv aag s s'; pas_refined aag s; pas_refined aag s'; is_subject aag (cur_thread s); invs s; invs s'; x \<notin> kernel_mappings; get_pd_of_thread (kheap s) (arch_state s) (cur_thread s) = arm_global_pd (arch_state s); get_pd_of_thread (kheap s') (arch_state s') (cur_thread s') = arm_global_pd (arch_state s')\<rbrakk> \<Longrightarrow> \<forall>a aa ab b. get_page_info (\<lambda>obj. get_arch_obj (kheap s obj)) (arm_global_pd (arch_state s)) x = Some (a, aa, ab, b) \<longrightarrow> (get_page_info (\<lambda>obj. get_arch_obj (kheap s' obj)) (arm_global_pd (arch_state s')) x = None \<longrightarrow> b = {}) \<and> (\<forall>a aa ab ba. get_page_info (\<lambda>obj. get_arch_obj (kheap s' obj)) (arm_global_pd (arch_state s')) x = Some (a, aa, ab, ba) \<longrightarrow> b = ba)
 3. \<And>x. \<lbrakk>reads_equiv aag s s'; pas_refined aag s; pas_refined aag s'; is_subject aag (cur_thread s); invs s; invs s'; x \<notin> kernel_mappings; get_pd_of_thread (kheap s) (arch_state s) (cur_thread s) \<noteq> arm_global_pd (arch_state s)\<rbrakk> \<Longrightarrow> ptable_rights (cur_thread s) s x = ptable_rights (cur_thread s') s' x proof (prove)
goal (5 subgoals):
 1. \<And>x a aa ab b. \<lbrakk>reads_equiv aag s s'; pas_refined aag s; pas_refined aag s'; is_subject aag (cur_thread s); invs s; invs s'; x \<notin> kernel_mappings; get_pd_of_thread (kheap s) (arch_state s) (cur_thread s) = arm_global_pd (arch_state s); get_pd_of_thread (kheap s') (arch_state s') (cur_thread s') = arm_global_pd (arch_state s'); get_page_info (\<lambda>obj. get_arch_obj (kheap s obj)) (arm_global_pd (arch_state s)) x = None; get_page_info (\<lambda>obj. get_arch_obj (kheap s' obj)) (arm_global_pd (arch_state s')) x = Some (a, aa, ab, b)\<rbrakk> \<Longrightarrow> valid_global_objs s'
 2. \<And>x a aa ab b. \<lbrakk>reads_equiv aag s s'; pas_refined aag s; pas_refined aag s'; is_subject aag (cur_thread s); invs s; invs s'; x \<notin> kernel_mappings; get_pd_of_thread (kheap s) (arch_state s) (cur_thread s) = arm_global_pd (arch_state s); get_pd_of_thread (kheap s') (arch_state s') (cur_thread s') = arm_global_pd (arch_state s'); get_page_info (\<lambda>obj. get_arch_obj (kheap s obj)) (arm_global_pd (arch_state s)) x = None; get_page_info (\<lambda>obj. get_arch_obj (kheap s' obj)) (arm_global_pd (arch_state s')) x = Some (a, aa, ab, b)\<rbrakk> \<Longrightarrow> valid_arch_state s'
 3. \<And>x a aa ab b. \<lbrakk>reads_equiv aag s s'; pas_refined aag s; pas_refined aag s'; is_subject aag (cur_thread s); invs s; invs s'; x \<notin> kernel_mappings; get_pd_of_thread (kheap s) (arch_state s) (cur_thread s) = arm_global_pd (arch_state s); get_pd_of_thread (kheap s') (arch_state s') (cur_thread s') = arm_global_pd (arch_state s'); get_page_info (\<lambda>obj. get_arch_obj (kheap s obj)) (arm_global_pd (arch_state s)) x = None; get_page_info (\<lambda>obj. get_arch_obj (kheap s' obj)) (arm_global_pd (arch_state s')) x = Some (a, aa, ab, b); x \<in> kernel_mappings\<rbrakk> \<Longrightarrow> {} = b
 4. \<And>x. \<lbrakk>reads_equiv aag s s'; pas_refined aag s; pas_refined aag s'; is_subject aag (cur_thread s); invs s; invs s'; x \<notin> kernel_mappings; get_pd_of_thread (kheap s) (arch_state s) (cur_thread s) = arm_global_pd (arch_state s); get_pd_of_thread (kheap s') (arch_state s') (cur_thread s') = arm_global_pd (arch_state s')\<rbrakk> \<Longrightarrow> \<forall>a aa ab b. get_page_info (\<lambda>obj. get_arch_obj (kheap s obj)) (arm_global_pd (arch_state s)) x = Some (a, aa, ab, b) \<longrightarrow> (get_page_info (\<lambda>obj. get_arch_obj (kheap s' obj)) (arm_global_pd (arch_state s')) x = None \<longrightarrow> b = {}) \<and> (\<forall>a aa ab ba. get_page_info (\<lambda>obj. get_arch_obj (kheap s' obj)) (arm_global_pd (arch_state s')) x = Some (a, aa, ab, ba) \<longrightarrow> b = ba)
 5. \<And>x. \<lbrakk>reads_equiv aag s s'; pas_refined aag s; pas_refined aag s'; is_subject aag (cur_thread s); invs s; invs s'; x \<notin> kernel_mappings; get_pd_of_thread (kheap s) (arch_state s) (cur_thread s) \<noteq> arm_global_pd (arch_state s)\<rbrakk> \<Longrightarrow> ptable_rights (cur_thread s) s x = ptable_rights (cur_thread s') s' x proof (prove)
goal (2 subgoals):
 1. \<And>x. \<lbrakk>reads_equiv aag s s'; pas_refined aag s; pas_refined aag s'; is_subject aag (cur_thread s); invs s; invs s'; x \<notin> kernel_mappings; get_pd_of_thread (kheap s) (arch_state s) (cur_thread s) = arm_global_pd (arch_state s); get_pd_of_thread (kheap s') (arch_state s') (cur_thread s') = arm_global_pd (arch_state s')\<rbrakk> \<Longrightarrow> \<forall>a aa ab b. get_page_info (\<lambda>obj. get_arch_obj (kheap s obj)) (arm_global_pd (arch_state s)) x = Some (a, aa, ab, b) \<longrightarrow> (get_page_info (\<lambda>obj. get_arch_obj (kheap s' obj)) (arm_global_pd (arch_state s')) x = None \<longrightarrow> b = {}) \<and> (\<forall>a aa ab ba. get_page_info (\<lambda>obj. get_arch_obj (kheap s' obj)) (arm_global_pd (arch_state s')) x = Some (a, aa, ab, ba) \<longrightarrow> b = ba)
 2. \<And>x. \<lbrakk>reads_equiv aag s s'; pas_refined aag s; pas_refined aag s'; is_subject aag (cur_thread s); invs s; invs s'; x \<notin> kernel_mappings; get_pd_of_thread (kheap s) (arch_state s) (cur_thread s) \<noteq> arm_global_pd (arch_state s)\<rbrakk> \<Longrightarrow> ptable_rights (cur_thread s) s x = ptable_rights (cur_thread s') s' x proof (prove)
goal (2 subgoals):
 1. \<And>x a aa ab b. \<lbrakk>reads_equiv aag s s'; pas_refined aag s; pas_refined aag s'; is_subject aag (cur_thread s); invs s; invs s'; x \<notin> kernel_mappings; get_pd_of_thread (kheap s) (arch_state s) (cur_thread s) = arm_global_pd (arch_state s); get_pd_of_thread (kheap s') (arch_state s') (cur_thread s') = arm_global_pd (arch_state s'); get_page_info (\<lambda>obj. get_arch_obj (kheap s obj)) (arm_global_pd (arch_state s)) x = Some (a, aa, ab, b)\<rbrakk> \<Longrightarrow> (get_page_info (\<lambda>obj. get_arch_obj (kheap s' obj)) (arm_global_pd (arch_state s')) x = None \<longrightarrow> b = {}) \<and> (\<forall>a aa ab ba. get_page_info (\<lambda>obj. get_arch_obj (kheap s' obj)) (arm_global_pd (arch_state s')) x = Some (a, aa, ab, ba) \<longrightarrow> b = ba)
 2. \<And>x. \<lbrakk>reads_equiv aag s s'; pas_refined aag s; pas_refined aag s'; is_subject aag (cur_thread s); invs s; invs s'; x \<notin> kernel_mappings; get_pd_of_thread (kheap s) (arch_state s) (cur_thread s) \<noteq> arm_global_pd (arch_state s)\<rbrakk> \<Longrightarrow> ptable_rights (cur_thread s) s x = ptable_rights (cur_thread s') s' x proof (prove)
goal (3 subgoals):
 1. \<And>x a aa ab b. \<lbrakk>reads_equiv aag s s'; pas_refined aag s; pas_refined aag s'; is_subject aag (cur_thread s); invs s; invs s'; x \<notin> kernel_mappings; get_pd_of_thread (kheap s) (arch_state s) (cur_thread s) = arm_global_pd (arch_state s); get_pd_of_thread (kheap s') (arch_state s') (cur_thread s') = arm_global_pd (arch_state s'); get_page_info (\<lambda>obj. get_arch_obj (kheap s obj)) (arm_global_pd (arch_state s)) x = Some (a, aa, ab, b)\<rbrakk> \<Longrightarrow> get_page_info (\<lambda>obj. get_arch_obj (kheap s' obj)) (arm_global_pd (arch_state s')) x = None \<longrightarrow> b = {}
 2. \<And>x a aa ab b. \<lbrakk>reads_equiv aag s s'; pas_refined aag s; pas_refined aag s'; is_subject aag (cur_thread s); invs s; invs s'; x \<notin> kernel_mappings; get_pd_of_thread (kheap s) (arch_state s) (cur_thread s) = arm_global_pd (arch_state s); get_pd_of_thread (kheap s') (arch_state s') (cur_thread s') = arm_global_pd (arch_state s'); get_page_info (\<lambda>obj. get_arch_obj (kheap s obj)) (arm_global_pd (arch_state s)) x = Some (a, aa, ab, b)\<rbrakk> \<Longrightarrow> \<forall>a aa ab ba. get_page_info (\<lambda>obj. get_arch_obj (kheap s' obj)) (arm_global_pd (arch_state s')) x = Some (a, aa, ab, ba) \<longrightarrow> b = ba
 3. \<And>x. \<lbrakk>reads_equiv aag s s'; pas_refined aag s; pas_refined aag s'; is_subject aag (cur_thread s); invs s; invs s'; x \<notin> kernel_mappings; get_pd_of_thread (kheap s) (arch_state s) (cur_thread s) \<noteq> arm_global_pd (arch_state s)\<rbrakk> \<Longrightarrow> ptable_rights (cur_thread s) s x = ptable_rights (cur_thread s') s' x proof (prove)
goal (3 subgoals):
 1. \<And>x a aa ab b. \<lbrakk>reads_equiv aag s s'; pas_refined aag s; pas_refined aag s'; is_subject aag (cur_thread s); invs s; invs s'; x \<notin> kernel_mappings; get_pd_of_thread (kheap s) (arch_state s) (cur_thread s) = arm_global_pd (arch_state s); get_pd_of_thread (kheap s') (arch_state s') (cur_thread s') = arm_global_pd (arch_state s'); get_page_info (\<lambda>obj. get_arch_obj (kheap s obj)) (arm_global_pd (arch_state s)) x = Some (a, aa, ab, b); get_page_info (\<lambda>obj. get_arch_obj (kheap s' obj)) (arm_global_pd (arch_state s')) x = None\<rbrakk> \<Longrightarrow> b = {}
 2. \<And>x a aa ab b. \<lbrakk>reads_equiv aag s s'; pas_refined aag s; pas_refined aag s'; is_subject aag (cur_thread s); invs s; invs s'; x \<notin> kernel_mappings; get_pd_of_thread (kheap s) (arch_state s) (cur_thread s) = arm_global_pd (arch_state s); get_pd_of_thread (kheap s') (arch_state s') (cur_thread s') = arm_global_pd (arch_state s'); get_page_info (\<lambda>obj. get_arch_obj (kheap s obj)) (arm_global_pd (arch_state s)) x = Some (a, aa, ab, b)\<rbrakk> \<Longrightarrow> \<forall>a aa ab ba. get_page_info (\<lambda>obj. get_arch_obj (kheap s' obj)) (arm_global_pd (arch_state s')) x = Some (a, aa, ab, ba) \<longrightarrow> b = ba
 3. \<And>x. \<lbrakk>reads_equiv aag s s'; pas_refined aag s; pas_refined aag s'; is_subject aag (cur_thread s); invs s; invs s'; x \<notin> kernel_mappings; get_pd_of_thread (kheap s) (arch_state s) (cur_thread s) \<noteq> arm_global_pd (arch_state s)\<rbrakk> \<Longrightarrow> ptable_rights (cur_thread s) s x = ptable_rights (cur_thread s') s' x proof (prove)
goal (5 subgoals):
 1. \<And>x a aa ab b. \<lbrakk>reads_equiv aag s s'; pas_refined aag s; pas_refined aag s'; is_subject aag (cur_thread s); invs s; invs s'; x \<notin> kernel_mappings; get_pd_of_thread (kheap s) (arch_state s) (cur_thread s) = arm_global_pd (arch_state s); get_pd_of_thread (kheap s') (arch_state s') (cur_thread s') = arm_global_pd (arch_state s'); get_page_info (\<lambda>obj. get_arch_obj (kheap s obj)) (arm_global_pd (arch_state s)) x = Some (a, aa, ab, b); get_page_info (\<lambda>obj. get_arch_obj (kheap s' obj)) (arm_global_pd (arch_state s')) x = None\<rbrakk> \<Longrightarrow> valid_global_objs s
 2. \<And>x a aa ab b. \<lbrakk>reads_equiv aag s s'; pas_refined aag s; pas_refined aag s'; is_subject aag (cur_thread s); invs s; invs s'; x \<notin> kernel_mappings; get_pd_of_thread (kheap s) (arch_state s) (cur_thread s) = arm_global_pd (arch_state s); get_pd_of_thread (kheap s') (arch_state s') (cur_thread s') = arm_global_pd (arch_state s'); get_page_info (\<lambda>obj. get_arch_obj (kheap s obj)) (arm_global_pd (arch_state s)) x = Some (a, aa, ab, b); get_page_info (\<lambda>obj. get_arch_obj (kheap s' obj)) (arm_global_pd (arch_state s')) x = None\<rbrakk> \<Longrightarrow> valid_arch_state s
 3. \<And>x a aa ab b. \<lbrakk>reads_equiv aag s s'; pas_refined aag s; pas_refined aag s'; is_subject aag (cur_thread s); invs s; invs s'; x \<notin> kernel_mappings; get_pd_of_thread (kheap s) (arch_state s) (cur_thread s) = arm_global_pd (arch_state s); get_pd_of_thread (kheap s') (arch_state s') (cur_thread s') = arm_global_pd (arch_state s'); get_page_info (\<lambda>obj. get_arch_obj (kheap s obj)) (arm_global_pd (arch_state s)) x = Some (a, aa, ab, b); get_page_info (\<lambda>obj. get_arch_obj (kheap s' obj)) (arm_global_pd (arch_state s')) x = None; x \<in> kernel_mappings\<rbrakk> \<Longrightarrow> b = {}
 4. \<And>x a aa ab b. \<lbrakk>reads_equiv aag s s'; pas_refined aag s; pas_refined aag s'; is_subject aag (cur_thread s); invs s; invs s'; x \<notin> kernel_mappings; get_pd_of_thread (kheap s) (arch_state s) (cur_thread s) = arm_global_pd (arch_state s); get_pd_of_thread (kheap s') (arch_state s') (cur_thread s') = arm_global_pd (arch_state s'); get_page_info (\<lambda>obj. get_arch_obj (kheap s obj)) (arm_global_pd (arch_state s)) x = Some (a, aa, ab, b)\<rbrakk> \<Longrightarrow> \<forall>a aa ab ba. get_page_info (\<lambda>obj. get_arch_obj (kheap s' obj)) (arm_global_pd (arch_state s')) x = Some (a, aa, ab, ba) \<longrightarrow> b = ba
 5. \<And>x. \<lbrakk>reads_equiv aag s s'; pas_refined aag s; pas_refined aag s'; is_subject aag (cur_thread s); invs s; invs s'; x \<notin> kernel_mappings; get_pd_of_thread (kheap s) (arch_state s) (cur_thread s) \<noteq> arm_global_pd (arch_state s)\<rbrakk> \<Longrightarrow> ptable_rights (cur_thread s) s x = ptable_rights (cur_thread s') s' x proof (prove)
goal (2 subgoals):
 1. \<And>x a aa ab b. \<lbrakk>reads_equiv aag s s'; pas_refined aag s; pas_refined aag s'; is_subject aag (cur_thread s); invs s; invs s'; x \<notin> kernel_mappings; get_pd_of_thread (kheap s) (arch_state s) (cur_thread s) = arm_global_pd (arch_state s); get_pd_of_thread (kheap s') (arch_state s') (cur_thread s') = arm_global_pd (arch_state s'); get_page_info (\<lambda>obj. get_arch_obj (kheap s obj)) (arm_global_pd (arch_state s)) x = Some (a, aa, ab, b)\<rbrakk> \<Longrightarrow> \<forall>a aa ab ba. get_page_info (\<lambda>obj. get_arch_obj (kheap s' obj)) (arm_global_pd (arch_state s')) x = Some (a, aa, ab, ba) \<longrightarrow> b = ba
 2. \<And>x. \<lbrakk>reads_equiv aag s s'; pas_refined aag s; pas_refined aag s'; is_subject aag (cur_thread s); invs s; invs s'; x \<notin> kernel_mappings; get_pd_of_thread (kheap s) (arch_state s) (cur_thread s) \<noteq> arm_global_pd (arch_state s)\<rbrakk> \<Longrightarrow> ptable_rights (cur_thread s) s x = ptable_rights (cur_thread s') s' x proof (prove)
goal (2 subgoals):
 1. \<And>x a aa ab b ac ad ae ba. \<lbrakk>reads_equiv aag s s'; pas_refined aag s; pas_refined aag s'; is_subject aag (cur_thread s); invs s; invs s'; x \<notin> kernel_mappings; get_pd_of_thread (kheap s) (arch_state s) (cur_thread s) = arm_global_pd (arch_state s); get_pd_of_thread (kheap s') (arch_state s') (cur_thread s') = arm_global_pd (arch_state s'); get_page_info (\<lambda>obj. get_arch_obj (kheap s obj)) (arm_global_pd (arch_state s)) x = Some (a, aa, ab, b); get_page_info (\<lambda>obj. get_arch_obj (kheap s' obj)) (arm_global_pd (arch_state s')) x = Some (ac, ad, ae, ba)\<rbrakk> \<Longrightarrow> b = ba
 2. \<And>x. \<lbrakk>reads_equiv aag s s'; pas_refined aag s; pas_refined aag s'; is_subject aag (cur_thread s); invs s; invs s'; x \<notin> kernel_mappings; get_pd_of_thread (kheap s) (arch_state s) (cur_thread s) \<noteq> arm_global_pd (arch_state s)\<rbrakk> \<Longrightarrow> ptable_rights (cur_thread s) s x = ptable_rights (cur_thread s') s' x proof (prove)
goal (4 subgoals):
 1. \<And>x a aa ab b ac ad ae ba. \<lbrakk>reads_equiv aag s s'; pas_refined aag s; pas_refined aag s'; is_subject aag (cur_thread s); invs s; invs s'; x \<notin> kernel_mappings; get_pd_of_thread (kheap s) (arch_state s) (cur_thread s) = arm_global_pd (arch_state s); get_pd_of_thread (kheap s') (arch_state s') (cur_thread s') = arm_global_pd (arch_state s'); get_page_info (\<lambda>obj. get_arch_obj (kheap s obj)) (arm_global_pd (arch_state s)) x = Some (a, aa, ab, b); get_page_info (\<lambda>obj. get_arch_obj (kheap s' obj)) (arm_global_pd (arch_state s')) x = Some (ac, ad, ae, ba)\<rbrakk> \<Longrightarrow> valid_global_objs s
 2. \<And>x a aa ab b ac ad ae ba. \<lbrakk>reads_equiv aag s s'; pas_refined aag s; pas_refined aag s'; is_subject aag (cur_thread s); invs s; invs s'; x \<notin> kernel_mappings; get_pd_of_thread (kheap s) (arch_state s) (cur_thread s) = arm_global_pd (arch_state s); get_pd_of_thread (kheap s') (arch_state s') (cur_thread s') = arm_global_pd (arch_state s'); get_page_info (\<lambda>obj. get_arch_obj (kheap s obj)) (arm_global_pd (arch_state s)) x = Some (a, aa, ab, b); get_page_info (\<lambda>obj. get_arch_obj (kheap s' obj)) (arm_global_pd (arch_state s')) x = Some (ac, ad, ae, ba)\<rbrakk> \<Longrightarrow> valid_arch_state s
 3. \<And>x a aa ab b ac ad ae ba. \<lbrakk>reads_equiv aag s s'; pas_refined aag s; pas_refined aag s'; is_subject aag (cur_thread s); invs s; invs s'; x \<notin> kernel_mappings; get_pd_of_thread (kheap s) (arch_state s) (cur_thread s) = arm_global_pd (arch_state s); get_pd_of_thread (kheap s') (arch_state s') (cur_thread s') = arm_global_pd (arch_state s'); get_page_info (\<lambda>obj. get_arch_obj (kheap s obj)) (arm_global_pd (arch_state s)) x = Some (a, aa, ab, b); get_page_info (\<lambda>obj. get_arch_obj (kheap s' obj)) (arm_global_pd (arch_state s')) x = Some (ac, ad, ae, ba); x \<in> kernel_mappings\<rbrakk> \<Longrightarrow> b = ba
 4. \<And>x. \<lbrakk>reads_equiv aag s s'; pas_refined aag s; pas_refined aag s'; is_subject aag (cur_thread s); invs s; invs s'; x \<notin> kernel_mappings; get_pd_of_thread (kheap s) (arch_state s) (cur_thread s) \<noteq> arm_global_pd (arch_state s)\<rbrakk> \<Longrightarrow> ptable_rights (cur_thread s) s x = ptable_rights (cur_thread s') s' x proof (prove)
goal (1 subgoal):
 1. \<And>x. \<lbrakk>reads_equiv aag s s'; pas_refined aag s; pas_refined aag s'; is_subject aag (cur_thread s); invs s; invs s'; x \<notin> kernel_mappings; get_pd_of_thread (kheap s) (arch_state s) (cur_thread s) \<noteq> arm_global_pd (arch_state s)\<rbrakk> \<Longrightarrow> ptable_rights (cur_thread s) s x = ptable_rights (cur_thread s') s' x proof (prove)
goal (2 subgoals):
 1. \<And>x. \<lbrakk>reads_equiv aag s s'; pas_refined aag s; pas_refined aag s'; is_subject aag (cur_thread s); invs s; invs s'; x \<notin> kernel_mappings; get_pd_of_thread (kheap s) (arch_state s) (cur_thread s) \<noteq> arm_global_pd (arch_state s); get_pd_of_thread (kheap s') (arch_state s') (cur_thread s') = arm_global_pd (arch_state s')\<rbrakk> \<Longrightarrow> ptable_rights (cur_thread s) s x = ptable_rights (cur_thread s') s' x
 2. \<And>x. \<lbrakk>reads_equiv aag s s'; pas_refined aag s; pas_refined aag s'; is_subject aag (cur_thread s); invs s; invs s'; x \<notin> kernel_mappings; get_pd_of_thread (kheap s) (arch_state s) (cur_thread s) \<noteq> arm_global_pd (arch_state s); get_pd_of_thread (kheap s') (arch_state s') (cur_thread s') \<noteq> arm_global_pd (arch_state s')\<rbrakk> \<Longrightarrow> ptable_rights (cur_thread s) s x = ptable_rights (cur_thread s') s' x proof (prove)
goal (2 subgoals):
 1. \<And>x. \<lbrakk>pas_refined aag s; pas_refined aag s'; is_subject aag (cur_thread s); invs s; invs s'; x \<notin> kernel_mappings; get_pd_of_thread (kheap s) (arch_state s) (cur_thread s) \<noteq> arm_global_pd (arch_state s); get_pd_of_thread (kheap s') (arch_state s') (cur_thread s') = arm_global_pd (arch_state s'); reads_equiv aag s' s\<rbrakk> \<Longrightarrow> ptable_rights (cur_thread s) s x = ptable_rights (cur_thread s') s' x
 2. \<And>x. \<lbrakk>reads_equiv aag s s'; pas_refined aag s; pas_refined aag s'; is_subject aag (cur_thread s); invs s; invs s'; x \<notin> kernel_mappings; get_pd_of_thread (kheap s) (arch_state s) (cur_thread s) \<noteq> arm_global_pd (arch_state s); get_pd_of_thread (kheap s') (arch_state s') (cur_thread s') \<noteq> arm_global_pd (arch_state s')\<rbrakk> \<Longrightarrow> ptable_rights (cur_thread s) s x = ptable_rights (cur_thread s') s' x proof (prove)
goal (6 subgoals):
 1. \<And>x. \<lbrakk>pas_refined aag s; pas_refined aag s'; is_subject aag (cur_thread s); invs s; invs s'; x \<notin> kernel_mappings; get_pd_of_thread (kheap s) (arch_state s) (cur_thread s) \<noteq> arm_global_pd (arch_state s); get_pd_of_thread (kheap s') (arch_state s') (cur_thread s') = arm_global_pd (arch_state s'); reads_equiv aag s' s\<rbrakk> \<Longrightarrow> is_subject aag (cur_thread s')
 2. \<And>x. \<lbrakk>pas_refined aag s; pas_refined aag s'; is_subject aag (cur_thread s); invs s; invs s'; x \<notin> kernel_mappings; get_pd_of_thread (kheap s) (arch_state s) (cur_thread s) \<noteq> arm_global_pd (arch_state s); get_pd_of_thread (kheap s') (arch_state s') (cur_thread s') = arm_global_pd (arch_state s'); reads_equiv aag s' s\<rbrakk> \<Longrightarrow> invs s'
 3. \<And>x. \<lbrakk>pas_refined aag s; pas_refined aag s'; is_subject aag (cur_thread s); invs s; invs s'; x \<notin> kernel_mappings; get_pd_of_thread (kheap s) (arch_state s) (cur_thread s) \<noteq> arm_global_pd (arch_state s); get_pd_of_thread (kheap s') (arch_state s') (cur_thread s') = arm_global_pd (arch_state s'); reads_equiv aag s' s\<rbrakk> \<Longrightarrow> pas_refined aag s'
 4. \<And>x. \<lbrakk>pas_refined aag s; pas_refined aag s'; is_subject aag (cur_thread s); invs s; invs s'; x \<notin> kernel_mappings; get_pd_of_thread (kheap s) (arch_state s) (cur_thread s) \<noteq> arm_global_pd (arch_state s); get_pd_of_thread (kheap s') (arch_state s') (cur_thread s') = arm_global_pd (arch_state s'); reads_equiv aag s' s\<rbrakk> \<Longrightarrow> get_pd_of_thread (kheap s') (arch_state s') (cur_thread s') = arm_global_pd (arch_state s')
 5. \<And>x. \<lbrakk>pas_refined aag s; pas_refined aag s'; is_subject aag (cur_thread s); invs s; invs s'; x \<notin> kernel_mappings; get_pd_of_thread (kheap s) (arch_state s) (cur_thread s) \<noteq> arm_global_pd (arch_state s); get_pd_of_thread (kheap s') (arch_state s') (cur_thread s') = arm_global_pd (arch_state s'); reads_equiv aag s' s; get_pd_of_thread (kheap s) (arch_state s) (cur_thread s) = arm_global_pd (arch_state s)\<rbrakk> \<Longrightarrow> ptable_rights (cur_thread s) s x = ptable_rights (cur_thread s') s' x
 6. \<And>x. \<lbrakk>reads_equiv aag s s'; pas_refined aag s; pas_refined aag s'; is_subject aag (cur_thread s); invs s; invs s'; x \<notin> kernel_mappings; get_pd_of_thread (kheap s) (arch_state s) (cur_thread s) \<noteq> arm_global_pd (arch_state s); get_pd_of_thread (kheap s') (arch_state s') (cur_thread s') \<noteq> arm_global_pd (arch_state s')\<rbrakk> \<Longrightarrow> ptable_rights (cur_thread s) s x = ptable_rights (cur_thread s') s' x proof (prove)
goal (1 subgoal):
 1. \<And>x. \<lbrakk>reads_equiv aag s s'; pas_refined aag s; pas_refined aag s'; is_subject aag (cur_thread s); invs s; invs s'; x \<notin> kernel_mappings; get_pd_of_thread (kheap s) (arch_state s) (cur_thread s) \<noteq> arm_global_pd (arch_state s); get_pd_of_thread (kheap s') (arch_state s') (cur_thread s') \<noteq> arm_global_pd (arch_state s')\<rbrakk> \<Longrightarrow> ptable_rights (cur_thread s) s x = ptable_rights (cur_thread s') s' x proof (prove)
goal (1 subgoal):
 1. \<And>x. \<lbrakk>reads_equiv aag s s'; pas_refined aag s; pas_refined aag s'; is_subject aag (cur_thread s); invs s; invs s'; x \<notin> kernel_mappings; get_pd_of_thread (kheap s) (arch_state s) (cur_thread s) \<noteq> arm_global_pd (arch_state s); get_pd_of_thread (kheap s') (arch_state s') (cur_thread s') \<noteq> arm_global_pd (arch_state s')\<rbrakk> \<Longrightarrow> (case get_page_info (\<lambda>obj. get_arch_obj (kheap s obj)) (get_pd_of_thread (kheap s) (arch_state s) (cur_thread s)) x of None \<Rightarrow> {} | Some x2 \<Rightarrow> snd (snd (snd x2))) = (case get_page_info (\<lambda>obj. get_arch_obj (kheap s' obj)) (get_pd_of_thread (kheap s') (arch_state s') (cur_thread s')) x of None \<Rightarrow> {} | Some x2 \<Rightarrow> snd (snd (snd x2))) proof (prove)
goal (7 subgoals):
 1. \<And>x. \<lbrakk>reads_equiv aag s s'; pas_refined aag s; pas_refined aag s'; is_subject aag (cur_thread s); invs s; invs s'; x \<notin> kernel_mappings; get_pd_of_thread (kheap s) (arch_state s) (cur_thread s) \<noteq> arm_global_pd (arch_state s); get_pd_of_thread (kheap s') (arch_state s') (cur_thread s') \<noteq> arm_global_pd (arch_state s')\<rbrakk> \<Longrightarrow> pas_refined aag s
 2. \<And>x. \<lbrakk>reads_equiv aag s s'; pas_refined aag s; pas_refined aag s'; is_subject aag (cur_thread s); invs s; invs s'; x \<notin> kernel_mappings; get_pd_of_thread (kheap s) (arch_state s) (cur_thread s) \<noteq> arm_global_pd (arch_state s); get_pd_of_thread (kheap s') (arch_state s') (cur_thread s') \<noteq> arm_global_pd (arch_state s')\<rbrakk> \<Longrightarrow> is_subject aag (cur_thread s)
 3. \<And>x. \<lbrakk>reads_equiv aag s s'; pas_refined aag s; pas_refined aag s'; is_subject aag (cur_thread s); invs s; invs s'; x \<notin> kernel_mappings; get_pd_of_thread (kheap s) (arch_state s) (cur_thread s) \<noteq> arm_global_pd (arch_state s); get_pd_of_thread (kheap s') (arch_state s') (cur_thread s') \<noteq> arm_global_pd (arch_state s')\<rbrakk> \<Longrightarrow> ?pd_ref201 x \<noteq> arm_global_pd (arch_state s)
 4. \<And>x. \<lbrakk>reads_equiv aag s s'; pas_refined aag s; pas_refined aag s'; is_subject aag (cur_thread s); invs s; invs s'; x \<notin> kernel_mappings; get_pd_of_thread (kheap s) (arch_state s) (cur_thread s) \<noteq> arm_global_pd (arch_state s); get_pd_of_thread (kheap s') (arch_state s') (cur_thread s') \<noteq> arm_global_pd (arch_state s')\<rbrakk> \<Longrightarrow> ?pd_ref'201 x \<noteq> arm_global_pd (arch_state s')
 5. \<And>x. \<lbrakk>reads_equiv aag s s'; pas_refined aag s; pas_refined aag s'; is_subject aag (cur_thread s); invs s; invs s'; x \<notin> kernel_mappings; get_pd_of_thread (kheap s) (arch_state s) (cur_thread s) \<noteq> arm_global_pd (arch_state s); get_pd_of_thread (kheap s') (arch_state s') (cur_thread s') \<noteq> arm_global_pd (arch_state s')\<rbrakk> \<Longrightarrow> get_pd_of_thread (kheap s) (arch_state s) (cur_thread s) = ?pd_ref201 x
 6. \<And>x. \<lbrakk>reads_equiv aag s s'; pas_refined aag s; pas_refined aag s'; is_subject aag (cur_thread s); invs s; invs s'; x \<notin> kernel_mappings; get_pd_of_thread (kheap s) (arch_state s) (cur_thread s) \<noteq> arm_global_pd (arch_state s); get_pd_of_thread (kheap s') (arch_state s') (cur_thread s') \<noteq> arm_global_pd (arch_state s')\<rbrakk> \<Longrightarrow> get_pd_of_thread (kheap s') (arch_state s') (cur_thread s') = ?pd_ref'201 x
 7. \<And>x. \<lbrakk>reads_equiv aag s s'; pas_refined aag s; pas_refined aag s'; is_subject aag (cur_thread s); invs s; invs s'; x \<notin> kernel_mappings; get_pd_of_thread (kheap s) (arch_state s) (cur_thread s) \<noteq> arm_global_pd (arch_state s); get_pd_of_thread (kheap s') (arch_state s') (cur_thread s') \<noteq> arm_global_pd (arch_state s'); ?pd_ref201 x = ?pd_ref'201 x\<rbrakk> \<Longrightarrow> (case get_page_info (\<lambda>obj. get_arch_obj (kheap s obj)) (get_pd_of_thread (kheap s) (arch_state s) (cur_thread s)) x of None \<Rightarrow> {} | Some x2 \<Rightarrow> snd (snd (snd x2))) = (case get_page_info (\<lambda>obj. get_arch_obj (kheap s' obj)) (get_pd_of_thread (kheap s') (arch_state s') (cur_thread s')) x of None \<Rightarrow> {} | Some x2 \<Rightarrow> snd (snd (snd x2))) proof (prove)
goal (1 subgoal):
 1. \<And>x. \<lbrakk>reads_equiv aag s s'; pas_refined aag s; pas_refined aag s'; is_subject aag (cur_thread s); invs s; invs s'; x \<notin> kernel_mappings; get_pd_of_thread (kheap s) (arch_state s) (cur_thread s) \<noteq> arm_global_pd (arch_state s); get_pd_of_thread (kheap s') (arch_state s') (cur_thread s') \<noteq> arm_global_pd (arch_state s'); get_pd_of_thread (kheap s) (arch_state s) (cur_thread s) = get_pd_of_thread (kheap s') (arch_state s') (cur_thread s')\<rbrakk> \<Longrightarrow> (case get_page_info (\<lambda>obj. get_arch_obj (kheap s obj)) (get_pd_of_thread (kheap s) (arch_state s) (cur_thread s)) x of None \<Rightarrow> {} | Some x2 \<Rightarrow> snd (snd (snd x2))) = (case get_page_info (\<lambda>obj. get_arch_obj (kheap s' obj)) (get_pd_of_thread (kheap s') (arch_state s') (cur_thread s')) x of None \<Rightarrow> {} | Some x2 \<Rightarrow> snd (snd (snd x2))) proof (prove)
goal (1 subgoal):
 1. \<And>x. \<lbrakk>reads_equiv aag s s'; pas_refined aag s; pas_refined aag s'; is_subject aag (get_pd_of_thread (kheap s') (arch_state s') (cur_thread s')); invs s; invs s'; x \<notin> kernel_mappings; get_pd_of_thread (kheap s') (arch_state s') (cur_thread s') \<noteq> arm_global_pd (arch_state s); get_pd_of_thread (kheap s') (arch_state s') (cur_thread s') \<noteq> arm_global_pd (arch_state s'); get_pd_of_thread (kheap s) (arch_state s) (cur_thread s) = get_pd_of_thread (kheap s') (arch_state s') (cur_thread s'); is_subject aag (cur_thread s)\<rbrakk> \<Longrightarrow> (case get_page_info (\<lambda>obj. get_arch_obj (kheap s obj)) (get_pd_of_thread (kheap s') (arch_state s') (cur_thread s')) x of None \<Rightarrow> {} | Some x2 \<Rightarrow> snd (snd (snd x2))) = (case get_page_info (\<lambda>obj. get_arch_obj (kheap s' obj)) (get_pd_of_thread (kheap s') (arch_state s') (cur_thread s')) x of None \<Rightarrow> {} | Some x2 \<Rightarrow> snd (snd (snd x2))) proof (prove)
goal:
No subgoals!