theory PageTableDuplicates

lemma valid_duplicates_deleteObjects_helper:
  assumes vd:"vs_valid_duplicates' (m::(word32 \<rightharpoonup> Structures_H.kernel_object))"
  assumes inc: "\<And>p ko. \<lbrakk>m p = Some (KOArch ko);p \<in> {ptr .. ptr + 2 ^ sz - 1}\<rbrakk>
  \<Longrightarrow> 6 \<le> sz"
  assumes aligned:"is_aligned ptr sz"
  notes blah[simp del] =  atLeastatMost_subset_iff atLeastLessThan_iff
          Int_atLeastAtMost atLeastatMost_empty_iff split_paired_Ex
          atLeastAtMost_iff
  shows "vs_valid_duplicates'  (\<lambda>x. if x \<in> {ptr .. ptr + 2 ^ sz - 1} then None else m x)" apply (rule valid_duplicates'_diffI,rule vd) apply (clarsimp simp: vs_valid_duplicates'_def split:option.splits) apply (clarsimp simp: vs_valid_duplicates'_def split:option.splits) apply (case_tac "the (m x)",simp_all add:vs_ptr_align_def) apply fastforce+ apply (rename_tac arch_kernel_object) apply (case_tac arch_kernel_object) apply fastforce+ apply (clarsimp split:ARM_H.pte.splits) apply auto[1] apply (drule_tac p' = y in valid_duplicates'_D[OF vd]) apply (simp add:vs_ptr_align_def)+ apply clarsimp apply (drule(1) inc) apply (drule(1) mask_out_first_mask_some) apply (simp add:mask_lower_twice) apply (simp add: mask_in_range[OF aligned,symmetric]) apply (drule_tac p' = y in valid_duplicates'_D[OF vd]) apply simp apply (simp add:vs_ptr_align_def) apply simp apply (drule_tac p' = y in valid_duplicates'_D[OF vd]) apply simp apply (simp add:vs_ptr_align_def) apply simp apply (clarsimp split:ARM_H.pde.splits) apply auto[1] apply (drule_tac p' = y in valid_duplicates'_D[OF vd]) apply simp apply (simp add:vs_ptr_align_def) apply (drule(1) inc) apply (drule(1) mask_out_first_mask_some) apply (simp add:mask_lower_twice) apply (simp add: mask_in_range[OF aligned,symmetric]) apply (drule_tac p' = y in valid_duplicates'_D[OF vd]) apply simp apply (simp add:vs_ptr_align_def) apply simp apply (drule_tac p' = y in valid_duplicates'_D[OF vd]) apply simp apply (simp add:vs_ptr_align_def) apply simp done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. vs_valid_duplicates' (\<lambda>x. if x \<in> {ptr..ptr + 2 ^ sz - 1} then None else m x) proof (prove)
goal (2 subgoals):
 1. vs_valid_duplicates' (\<lambda>x. if x \<in> {x. m x \<noteq> (if x \<in> {ptr..ptr + 2 ^ sz - 1} then None else m x)} then if x \<in> {ptr..ptr + 2 ^ sz - 1} then None else m x else None)
 2. vs_valid_duplicates' (\<lambda>x. if x \<in> {x. m x \<noteq> (if x \<in> {ptr..ptr + 2 ^ sz - 1} then None else m x)} then None else if x \<in> {ptr..ptr + 2 ^ sz - 1} then None else m x) proof (prove)
goal (1 subgoal):
 1. vs_valid_duplicates' (\<lambda>x. if x \<in> {x. m x \<noteq> (if x \<in> {ptr..ptr + 2 ^ sz - 1} then None else m x)} then None else if x \<in> {ptr..ptr + 2 ^ sz - 1} then None else m x) proof (prove)
goal (1 subgoal):
 1. \<And>x y x2. \<lbrakk>x \<notin> {ptr..ptr + 2 ^ sz - 1}; m x = Some x2\<rbrakk> \<Longrightarrow> (y \<in> {ptr..ptr + 2 ^ sz - 1} \<longrightarrow> ((\<exists>ya. m y = Some ya) \<longrightarrow> is_aligned y 2 \<longrightarrow> x && ~~ mask (vs_ptr_align x2) \<noteq> y && ~~ mask (vs_ptr_align x2)) \<and> (m y = None \<longrightarrow> is_aligned y 2 \<longrightarrow> x && ~~ mask (vs_ptr_align x2) \<noteq> y && ~~ mask (vs_ptr_align x2))) \<and> (y \<notin> {ptr..ptr + 2 ^ sz - 1} \<longrightarrow> is_aligned y 2 \<longrightarrow> x && ~~ mask (vs_ptr_align x2) = y && ~~ mask (vs_ptr_align x2) \<longrightarrow> Some x2 = m y) proof (prove)
goal (8 subgoals):
 1. \<And>x y x2 x1. \<lbrakk>x \<notin> {ptr..ptr + 2 ^ sz - 1}; m x = Some (KOEndpoint x1); x2 = KOEndpoint x1\<rbrakk> \<Longrightarrow> (y \<in> {ptr..ptr + 2 ^ sz - 1} \<longrightarrow> ((\<exists>ya. m y = Some ya) \<longrightarrow> is_aligned y 2 \<longrightarrow> x \<noteq> y) \<and> (m y = None \<longrightarrow> is_aligned y 2 \<longrightarrow> x \<noteq> y)) \<and> (y \<notin> {ptr..ptr + 2 ^ sz - 1} \<longrightarrow> is_aligned y 2 \<longrightarrow> x = y \<longrightarrow> Some (KOEndpoint x1) = m y)
 2. \<And>x y x2 x2a. \<lbrakk>x \<notin> {ptr..ptr + 2 ^ sz - 1}; m x = Some (KONotification x2a); x2 = KONotification x2a\<rbrakk> \<Longrightarrow> (y \<in> {ptr..ptr + 2 ^ sz - 1} \<longrightarrow> ((\<exists>ya. m y = Some ya) \<longrightarrow> is_aligned y 2 \<longrightarrow> x \<noteq> y) \<and> (m y = None \<longrightarrow> is_aligned y 2 \<longrightarrow> x \<noteq> y)) \<and> (y \<notin> {ptr..ptr + 2 ^ sz - 1} \<longrightarrow> is_aligned y 2 \<longrightarrow> x = y \<longrightarrow> Some (KONotification x2a) = m y)
 3. \<And>x y x2. \<lbrakk>x \<notin> {ptr..ptr + 2 ^ sz - 1}; m x = Some KOKernelData; x2 = KOKernelData\<rbrakk> \<Longrightarrow> (y \<in> {ptr..ptr + 2 ^ sz - 1} \<longrightarrow> ((\<exists>ya. m y = Some ya) \<longrightarrow> is_aligned y 2 \<longrightarrow> x \<noteq> y) \<and> (m y = None \<longrightarrow> is_aligned y 2 \<longrightarrow> x \<noteq> y)) \<and> (y \<notin> {ptr..ptr + 2 ^ sz - 1} \<longrightarrow> is_aligned y 2 \<longrightarrow> x = y \<longrightarrow> Some KOKernelData = m y)
 4. \<And>x y x2. \<lbrakk>x \<notin> {ptr..ptr + 2 ^ sz - 1}; m x = Some KOUserData; x2 = KOUserData\<rbrakk> \<Longrightarrow> (y \<in> {ptr..ptr + 2 ^ sz - 1} \<longrightarrow> ((\<exists>ya. m y = Some ya) \<longrightarrow> is_aligned y 2 \<longrightarrow> x \<noteq> y) \<and> (m y = None \<longrightarrow> is_aligned y 2 \<longrightarrow> x \<noteq> y)) \<and> (y \<notin> {ptr..ptr + 2 ^ sz - 1} \<longrightarrow> is_aligned y 2 \<longrightarrow> x = y \<longrightarrow> Some KOUserData = m y)
 5. \<And>x y x2. \<lbrakk>x \<notin> {ptr..ptr + 2 ^ sz - 1}; m x = Some KOUserDataDevice; x2 = KOUserDataDevice\<rbrakk> \<Longrightarrow> (y \<in> {ptr..ptr + 2 ^ sz - 1} \<longrightarrow> ((\<exists>ya. m y = Some ya) \<longrightarrow> is_aligned y 2 \<longrightarrow> x \<noteq> y) \<and> (m y = None \<longrightarrow> is_aligned y 2 \<longrightarrow> x \<noteq> y)) \<and> (y \<notin> {ptr..ptr + 2 ^ sz - 1} \<longrightarrow> is_aligned y 2 \<longrightarrow> x = y \<longrightarrow> Some KOUserDataDevice = m y)
 6. \<And>x y x2 x6. \<lbrakk>x \<notin> {ptr..ptr + 2 ^ sz - 1}; m x = Some (KOTCB x6); x2 = KOTCB x6\<rbrakk> \<Longrightarrow> (y \<in> {ptr..ptr + 2 ^ sz - 1} \<longrightarrow> ((\<exists>ya. m y = Some ya) \<longrightarrow> is_aligned y 2 \<longrightarrow> x \<noteq> y) \<and> (m y = None \<longrightarrow> is_aligned y 2 \<longrightarrow> x \<noteq> y)) \<and> (y \<notin> {ptr..ptr + 2 ^ sz - 1} \<longrightarrow> is_aligned y 2 \<longrightarrow> x = y \<longrightarrow> Some (KOTCB x6) = m y)
 7. \<And>x y x2 x7. \<lbrakk>x \<notin> {ptr..ptr + 2 ^ sz - 1}; m x = Some (KOCTE x7); x2 = KOCTE x7\<rbrakk> \<Longrightarrow> (y \<in> {ptr..ptr + 2 ^ sz - 1} \<longrightarrow> ((\<exists>ya. m y = Some ya) \<longrightarrow> is_aligned y 2 \<longrightarrow> x \<noteq> y) \<and> (m y = None \<longrightarrow> is_aligned y 2 \<longrightarrow> x \<noteq> y)) \<and> (y \<notin> {ptr..ptr + 2 ^ sz - 1} \<longrightarrow> is_aligned y 2 \<longrightarrow> x = y \<longrightarrow> Some (KOCTE x7) = m y)
 8. \<And>x y x2 x8. \<lbrakk>x \<notin> {ptr..ptr + 2 ^ sz - 1}; m x = Some (KOArch x8); x2 = KOArch x8\<rbrakk> \<Longrightarrow> (y \<in> {ptr..ptr + 2 ^ sz - 1} \<longrightarrow> ((\<exists>ya. m y = Some ya) \<longrightarrow> is_aligned y 2 \<longrightarrow> x && ~~ mask (case x8 of KOASIDPool asidpool \<Rightarrow> 0 | KOPTE (ARM_H.LargePagePTE xa xaa xb xc xd) \<Rightarrow> 6 | KOPTE _ \<Rightarrow> 0 | KOPDE (ARM_H.SuperSectionPDE xa xaa xb xc xd xe) \<Rightarrow> 6 | KOPDE _ \<Rightarrow> 0) \<noteq> y && ~~ mask (case x8 of KOASIDPool asidpool \<Rightarrow> 0 | KOPTE (ARM_H.LargePagePTE xa xaa xb xc xd) \<Rightarrow> 6 | KOPTE _ \<Rightarrow> 0 | KOPDE (ARM_H.SuperSectionPDE xa xaa xb xc xd xe) \<Rightarrow> 6 | KOPDE _ \<Rightarrow> 0)) \<and> (m y = None \<longrightarrow> is_aligned y 2 \<longrightarrow> x && ~~ mask (case x8 of KOASIDPool asidpool \<Rightarrow> 0 | KOPTE (ARM_H.LargePagePTE xa xaa xb xc xd) \<Rightarrow> 6 | KOPTE _ \<Rightarrow> 0 | KOPDE (ARM_H.SuperSectionPDE xa xaa xb xc xd xe) \<Rightarrow> 6 | KOPDE _ \<Rightarrow> 0) \<noteq> y && ~~ mask (case x8 of KOASIDPool asidpool \<Rightarrow> 0 | KOPTE (ARM_H.LargePagePTE xa xaa xb xc xd) \<Rightarrow> 6 | KOPTE _ \<Rightarrow> 0 | KOPDE (ARM_H.SuperSectionPDE xa xaa xb xc xd xe) \<Rightarrow> 6 | KOPDE _ \<Rightarrow> 0))) \<and> (y \<notin> {ptr..ptr + 2 ^ sz - 1} \<longrightarrow> is_aligned y 2 \<longrightarrow> x && ~~ mask (case x8 of KOASIDPool asidpool \<Rightarrow> 0 | KOPTE (ARM_H.LargePagePTE xa xaa xb xc xd) \<Rightarrow> 6 | KOPTE _ \<Rightarrow> 0 | KOPDE (ARM_H.SuperSectionPDE xa xaa xb xc xd xe) \<Rightarrow> 6 | KOPDE _ \<Rightarrow> 0) = y && ~~ mask (case x8 of KOASIDPool asidpool \<Rightarrow> 0 | KOPTE (ARM_H.LargePagePTE xa xaa xb xc xd) \<Rightarrow> 6 | KOPTE _ \<Rightarrow> 0 | KOPDE (ARM_H.SuperSectionPDE xa xaa xb xc xd xe) \<Rightarrow> 6 | KOPDE _ \<Rightarrow> 0) \<longrightarrow> Some (KOArch x8) = m y) proof (prove)
goal (1 subgoal):
 1. \<And>x y x2 x8. \<lbrakk>x \<notin> {ptr..ptr + 2 ^ sz - 1}; m x = Some (KOArch x8); x2 = KOArch x8\<rbrakk> \<Longrightarrow> (y \<in> {ptr..ptr + 2 ^ sz - 1} \<longrightarrow> ((\<exists>ya. m y = Some ya) \<longrightarrow> is_aligned y 2 \<longrightarrow> x && ~~ mask (case x8 of KOASIDPool asidpool \<Rightarrow> 0 | KOPTE (ARM_H.LargePagePTE xa xaa xb xc xd) \<Rightarrow> 6 | KOPTE _ \<Rightarrow> 0 | KOPDE (ARM_H.SuperSectionPDE xa xaa xb xc xd xe) \<Rightarrow> 6 | KOPDE _ \<Rightarrow> 0) \<noteq> y && ~~ mask (case x8 of KOASIDPool asidpool \<Rightarrow> 0 | KOPTE (ARM_H.LargePagePTE xa xaa xb xc xd) \<Rightarrow> 6 | KOPTE _ \<Rightarrow> 0 | KOPDE (ARM_H.SuperSectionPDE xa xaa xb xc xd xe) \<Rightarrow> 6 | KOPDE _ \<Rightarrow> 0)) \<and> (m y = None \<longrightarrow> is_aligned y 2 \<longrightarrow> x && ~~ mask (case x8 of KOASIDPool asidpool \<Rightarrow> 0 | KOPTE (ARM_H.LargePagePTE xa xaa xb xc xd) \<Rightarrow> 6 | KOPTE _ \<Rightarrow> 0 | KOPDE (ARM_H.SuperSectionPDE xa xaa xb xc xd xe) \<Rightarrow> 6 | KOPDE _ \<Rightarrow> 0) \<noteq> y && ~~ mask (case x8 of KOASIDPool asidpool \<Rightarrow> 0 | KOPTE (ARM_H.LargePagePTE xa xaa xb xc xd) \<Rightarrow> 6 | KOPTE _ \<Rightarrow> 0 | KOPDE (ARM_H.SuperSectionPDE xa xaa xb xc xd xe) \<Rightarrow> 6 | KOPDE _ \<Rightarrow> 0))) \<and> (y \<notin> {ptr..ptr + 2 ^ sz - 1} \<longrightarrow> is_aligned y 2 \<longrightarrow> x && ~~ mask (case x8 of KOASIDPool asidpool \<Rightarrow> 0 | KOPTE (ARM_H.LargePagePTE xa xaa xb xc xd) \<Rightarrow> 6 | KOPTE _ \<Rightarrow> 0 | KOPDE (ARM_H.SuperSectionPDE xa xaa xb xc xd xe) \<Rightarrow> 6 | KOPDE _ \<Rightarrow> 0) = y && ~~ mask (case x8 of KOASIDPool asidpool \<Rightarrow> 0 | KOPTE (ARM_H.LargePagePTE xa xaa xb xc xd) \<Rightarrow> 6 | KOPTE _ \<Rightarrow> 0 | KOPDE (ARM_H.SuperSectionPDE xa xaa xb xc xd xe) \<Rightarrow> 6 | KOPDE _ \<Rightarrow> 0) \<longrightarrow> Some (KOArch x8) = m y) proof (prove)
goal (1 subgoal):
 1. \<And>x y x2 arch_kernel_object. \<lbrakk>x \<notin> {ptr..ptr + 2 ^ sz - 1}; m x = Some (KOArch arch_kernel_object); x2 = KOArch arch_kernel_object\<rbrakk> \<Longrightarrow> (y \<in> {ptr..ptr + 2 ^ sz - 1} \<longrightarrow> ((\<exists>ya. m y = Some ya) \<longrightarrow> is_aligned y 2 \<longrightarrow> x && ~~ mask (case arch_kernel_object of KOASIDPool asidpool \<Rightarrow> 0 | KOPTE (ARM_H.LargePagePTE xa xaa xb xc xd) \<Rightarrow> 6 | KOPTE _ \<Rightarrow> 0 | KOPDE (ARM_H.SuperSectionPDE xa xaa xb xc xd xe) \<Rightarrow> 6 | KOPDE _ \<Rightarrow> 0) \<noteq> y && ~~ mask (case arch_kernel_object of KOASIDPool asidpool \<Rightarrow> 0 | KOPTE (ARM_H.LargePagePTE xa xaa xb xc xd) \<Rightarrow> 6 | KOPTE _ \<Rightarrow> 0 | KOPDE (ARM_H.SuperSectionPDE xa xaa xb xc xd xe) \<Rightarrow> 6 | KOPDE _ \<Rightarrow> 0)) \<and> (m y = None \<longrightarrow> is_aligned y 2 \<longrightarrow> x && ~~ mask (case arch_kernel_object of KOASIDPool asidpool \<Rightarrow> 0 | KOPTE (ARM_H.LargePagePTE xa xaa xb xc xd) \<Rightarrow> 6 | KOPTE _ \<Rightarrow> 0 | KOPDE (ARM_H.SuperSectionPDE xa xaa xb xc xd xe) \<Rightarrow> 6 | KOPDE _ \<Rightarrow> 0) \<noteq> y && ~~ mask (case arch_kernel_object of KOASIDPool asidpool \<Rightarrow> 0 | KOPTE (ARM_H.LargePagePTE xa xaa xb xc xd) \<Rightarrow> 6 | KOPTE _ \<Rightarrow> 0 | KOPDE (ARM_H.SuperSectionPDE xa xaa xb xc xd xe) \<Rightarrow> 6 | KOPDE _ \<Rightarrow> 0))) \<and> (y \<notin> {ptr..ptr + 2 ^ sz - 1} \<longrightarrow> is_aligned y 2 \<longrightarrow> x && ~~ mask (case arch_kernel_object of KOASIDPool asidpool \<Rightarrow> 0 | KOPTE (ARM_H.LargePagePTE xa xaa xb xc xd) \<Rightarrow> 6 | KOPTE _ \<Rightarrow> 0 | KOPDE (ARM_H.SuperSectionPDE xa xaa xb xc xd xe) \<Rightarrow> 6 | KOPDE _ \<Rightarrow> 0) = y && ~~ mask (case arch_kernel_object of KOASIDPool asidpool \<Rightarrow> 0 | KOPTE (ARM_H.LargePagePTE xa xaa xb xc xd) \<Rightarrow> 6 | KOPTE _ \<Rightarrow> 0 | KOPDE (ARM_H.SuperSectionPDE xa xaa xb xc xd xe) \<Rightarrow> 6 | KOPDE _ \<Rightarrow> 0) \<longrightarrow> Some (KOArch arch_kernel_object) = m y) proof (prove)
goal (3 subgoals):
 1. \<And>x y x2 arch_kernel_object x1. \<lbrakk>x \<notin> {ptr..ptr + 2 ^ sz - 1}; m x = Some (KOArch arch_kernel_object); x2 = KOArch arch_kernel_object; arch_kernel_object = KOASIDPool x1\<rbrakk> \<Longrightarrow> (y \<in> {ptr..ptr + 2 ^ sz - 1} \<longrightarrow> ((\<exists>ya. m y = Some ya) \<longrightarrow> is_aligned y 2 \<longrightarrow> x && ~~ mask (case arch_kernel_object of KOASIDPool asidpool \<Rightarrow> 0 | KOPTE (ARM_H.LargePagePTE xa xaa xb xc xd) \<Rightarrow> 6 | KOPTE _ \<Rightarrow> 0 | KOPDE (ARM_H.SuperSectionPDE xa xaa xb xc xd xe) \<Rightarrow> 6 | KOPDE _ \<Rightarrow> 0) \<noteq> y && ~~ mask (case arch_kernel_object of KOASIDPool asidpool \<Rightarrow> 0 | KOPTE (ARM_H.LargePagePTE xa xaa xb xc xd) \<Rightarrow> 6 | KOPTE _ \<Rightarrow> 0 | KOPDE (ARM_H.SuperSectionPDE xa xaa xb xc xd xe) \<Rightarrow> 6 | KOPDE _ \<Rightarrow> 0)) \<and> (m y = None \<longrightarrow> is_aligned y 2 \<longrightarrow> x && ~~ mask (case arch_kernel_object of KOASIDPool asidpool \<Rightarrow> 0 | KOPTE (ARM_H.LargePagePTE xa xaa xb xc xd) \<Rightarrow> 6 | KOPTE _ \<Rightarrow> 0 | KOPDE (ARM_H.SuperSectionPDE xa xaa xb xc xd xe) \<Rightarrow> 6 | KOPDE _ \<Rightarrow> 0) \<noteq> y && ~~ mask (case arch_kernel_object of KOASIDPool asidpool \<Rightarrow> 0 | KOPTE (ARM_H.LargePagePTE xa xaa xb xc xd) \<Rightarrow> 6 | KOPTE _ \<Rightarrow> 0 | KOPDE (ARM_H.SuperSectionPDE xa xaa xb xc xd xe) \<Rightarrow> 6 | KOPDE _ \<Rightarrow> 0))) \<and> (y \<notin> {ptr..ptr + 2 ^ sz - 1} \<longrightarrow> is_aligned y 2 \<longrightarrow> x && ~~ mask (case arch_kernel_object of KOASIDPool asidpool \<Rightarrow> 0 | KOPTE (ARM_H.LargePagePTE xa xaa xb xc xd) \<Rightarrow> 6 | KOPTE _ \<Rightarrow> 0 | KOPDE (ARM_H.SuperSectionPDE xa xaa xb xc xd xe) \<Rightarrow> 6 | KOPDE _ \<Rightarrow> 0) = y && ~~ mask (case arch_kernel_object of KOASIDPool asidpool \<Rightarrow> 0 | KOPTE (ARM_H.LargePagePTE xa xaa xb xc xd) \<Rightarrow> 6 | KOPTE _ \<Rightarrow> 0 | KOPDE (ARM_H.SuperSectionPDE xa xaa xb xc xd xe) \<Rightarrow> 6 | KOPDE _ \<Rightarrow> 0) \<longrightarrow> Some (KOArch arch_kernel_object) = m y)
 2. \<And>x y x2 arch_kernel_object x2a. \<lbrakk>x \<notin> {ptr..ptr + 2 ^ sz - 1}; m x = Some (KOArch arch_kernel_object); x2 = KOArch arch_kernel_object; arch_kernel_object = KOPTE x2a\<rbrakk> \<Longrightarrow> (y \<in> {ptr..ptr + 2 ^ sz - 1} \<longrightarrow> ((\<exists>ya. m y = Some ya) \<longrightarrow> is_aligned y 2 \<longrightarrow> x && ~~ mask (case arch_kernel_object of KOASIDPool asidpool \<Rightarrow> 0 | KOPTE (ARM_H.LargePagePTE xa xaa xb xc xd) \<Rightarrow> 6 | KOPTE _ \<Rightarrow> 0 | KOPDE (ARM_H.SuperSectionPDE xa xaa xb xc xd xe) \<Rightarrow> 6 | KOPDE _ \<Rightarrow> 0) \<noteq> y && ~~ mask (case arch_kernel_object of KOASIDPool asidpool \<Rightarrow> 0 | KOPTE (ARM_H.LargePagePTE xa xaa xb xc xd) \<Rightarrow> 6 | KOPTE _ \<Rightarrow> 0 | KOPDE (ARM_H.SuperSectionPDE xa xaa xb xc xd xe) \<Rightarrow> 6 | KOPDE _ \<Rightarrow> 0)) \<and> (m y = None \<longrightarrow> is_aligned y 2 \<longrightarrow> x && ~~ mask (case arch_kernel_object of KOASIDPool asidpool \<Rightarrow> 0 | KOPTE (ARM_H.LargePagePTE xa xaa xb xc xd) \<Rightarrow> 6 | KOPTE _ \<Rightarrow> 0 | KOPDE (ARM_H.SuperSectionPDE xa xaa xb xc xd xe) \<Rightarrow> 6 | KOPDE _ \<Rightarrow> 0) \<noteq> y && ~~ mask (case arch_kernel_object of KOASIDPool asidpool \<Rightarrow> 0 | KOPTE (ARM_H.LargePagePTE xa xaa xb xc xd) \<Rightarrow> 6 | KOPTE _ \<Rightarrow> 0 | KOPDE (ARM_H.SuperSectionPDE xa xaa xb xc xd xe) \<Rightarrow> 6 | KOPDE _ \<Rightarrow> 0))) \<and> (y \<notin> {ptr..ptr + 2 ^ sz - 1} \<longrightarrow> is_aligned y 2 \<longrightarrow> x && ~~ mask (case arch_kernel_object of KOASIDPool asidpool \<Rightarrow> 0 | KOPTE (ARM_H.LargePagePTE xa xaa xb xc xd) \<Rightarrow> 6 | KOPTE _ \<Rightarrow> 0 | KOPDE (ARM_H.SuperSectionPDE xa xaa xb xc xd xe) \<Rightarrow> 6 | KOPDE _ \<Rightarrow> 0) = y && ~~ mask (case arch_kernel_object of KOASIDPool asidpool \<Rightarrow> 0 | KOPTE (ARM_H.LargePagePTE xa xaa xb xc xd) \<Rightarrow> 6 | KOPTE _ \<Rightarrow> 0 | KOPDE (ARM_H.SuperSectionPDE xa xaa xb xc xd xe) \<Rightarrow> 6 | KOPDE _ \<Rightarrow> 0) \<longrightarrow> Some (KOArch arch_kernel_object) = m y)
 3. \<And>x y x2 arch_kernel_object x3. \<lbrakk>x \<notin> {ptr..ptr + 2 ^ sz - 1}; m x = Some (KOArch arch_kernel_object); x2 = KOArch arch_kernel_object; arch_kernel_object = KOPDE x3\<rbrakk> \<Longrightarrow> (y \<in> {ptr..ptr + 2 ^ sz - 1} \<longrightarrow> ((\<exists>ya. m y = Some ya) \<longrightarrow> is_aligned y 2 \<longrightarrow> x && ~~ mask (case arch_kernel_object of KOASIDPool asidpool \<Rightarrow> 0 | KOPTE (ARM_H.LargePagePTE xa xaa xb xc xd) \<Rightarrow> 6 | KOPTE _ \<Rightarrow> 0 | KOPDE (ARM_H.SuperSectionPDE xa xaa xb xc xd xe) \<Rightarrow> 6 | KOPDE _ \<Rightarrow> 0) \<noteq> y && ~~ mask (case arch_kernel_object of KOASIDPool asidpool \<Rightarrow> 0 | KOPTE (ARM_H.LargePagePTE xa xaa xb xc xd) \<Rightarrow> 6 | KOPTE _ \<Rightarrow> 0 | KOPDE (ARM_H.SuperSectionPDE xa xaa xb xc xd xe) \<Rightarrow> 6 | KOPDE _ \<Rightarrow> 0)) \<and> (m y = None \<longrightarrow> is_aligned y 2 \<longrightarrow> x && ~~ mask (case arch_kernel_object of KOASIDPool asidpool \<Rightarrow> 0 | KOPTE (ARM_H.LargePagePTE xa xaa xb xc xd) \<Rightarrow> 6 | KOPTE _ \<Rightarrow> 0 | KOPDE (ARM_H.SuperSectionPDE xa xaa xb xc xd xe) \<Rightarrow> 6 | KOPDE _ \<Rightarrow> 0) \<noteq> y && ~~ mask (case arch_kernel_object of KOASIDPool asidpool \<Rightarrow> 0 | KOPTE (ARM_H.LargePagePTE xa xaa xb xc xd) \<Rightarrow> 6 | KOPTE _ \<Rightarrow> 0 | KOPDE (ARM_H.SuperSectionPDE xa xaa xb xc xd xe) \<Rightarrow> 6 | KOPDE _ \<Rightarrow> 0))) \<and> (y \<notin> {ptr..ptr + 2 ^ sz - 1} \<longrightarrow> is_aligned y 2 \<longrightarrow> x && ~~ mask (case arch_kernel_object of KOASIDPool asidpool \<Rightarrow> 0 | KOPTE (ARM_H.LargePagePTE xa xaa xb xc xd) \<Rightarrow> 6 | KOPTE _ \<Rightarrow> 0 | KOPDE (ARM_H.SuperSectionPDE xa xaa xb xc xd xe) \<Rightarrow> 6 | KOPDE _ \<Rightarrow> 0) = y && ~~ mask (case arch_kernel_object of KOASIDPool asidpool \<Rightarrow> 0 | KOPTE (ARM_H.LargePagePTE xa xaa xb xc xd) \<Rightarrow> 6 | KOPTE _ \<Rightarrow> 0 | KOPDE (ARM_H.SuperSectionPDE xa xaa xb xc xd xe) \<Rightarrow> 6 | KOPDE _ \<Rightarrow> 0) \<longrightarrow> Some (KOArch arch_kernel_object) = m y) proof (prove)
goal (2 subgoals):
 1. \<And>x y x2 arch_kernel_object x2a. \<lbrakk>x \<notin> {ptr..ptr + 2 ^ sz - 1}; m x = Some (KOArch arch_kernel_object); x2 = KOArch arch_kernel_object; arch_kernel_object = KOPTE x2a\<rbrakk> \<Longrightarrow> (y \<in> {ptr..ptr + 2 ^ sz - 1} \<longrightarrow> ((\<exists>ya. m y = Some ya) \<longrightarrow> is_aligned y 2 \<longrightarrow> x && ~~ mask (case arch_kernel_object of KOASIDPool asidpool \<Rightarrow> 0 | KOPTE (ARM_H.LargePagePTE xa xaa xb xc xd) \<Rightarrow> 6 | KOPTE _ \<Rightarrow> 0 | KOPDE (ARM_H.SuperSectionPDE xa xaa xb xc xd xe) \<Rightarrow> 6 | KOPDE _ \<Rightarrow> 0) \<noteq> y && ~~ mask (case arch_kernel_object of KOASIDPool asidpool \<Rightarrow> 0 | KOPTE (ARM_H.LargePagePTE xa xaa xb xc xd) \<Rightarrow> 6 | KOPTE _ \<Rightarrow> 0 | KOPDE (ARM_H.SuperSectionPDE xa xaa xb xc xd xe) \<Rightarrow> 6 | KOPDE _ \<Rightarrow> 0)) \<and> (m y = None \<longrightarrow> is_aligned y 2 \<longrightarrow> x && ~~ mask (case arch_kernel_object of KOASIDPool asidpool \<Rightarrow> 0 | KOPTE (ARM_H.LargePagePTE xa xaa xb xc xd) \<Rightarrow> 6 | KOPTE _ \<Rightarrow> 0 | KOPDE (ARM_H.SuperSectionPDE xa xaa xb xc xd xe) \<Rightarrow> 6 | KOPDE _ \<Rightarrow> 0) \<noteq> y && ~~ mask (case arch_kernel_object of KOASIDPool asidpool \<Rightarrow> 0 | KOPTE (ARM_H.LargePagePTE xa xaa xb xc xd) \<Rightarrow> 6 | KOPTE _ \<Rightarrow> 0 | KOPDE (ARM_H.SuperSectionPDE xa xaa xb xc xd xe) \<Rightarrow> 6 | KOPDE _ \<Rightarrow> 0))) \<and> (y \<notin> {ptr..ptr + 2 ^ sz - 1} \<longrightarrow> is_aligned y 2 \<longrightarrow> x && ~~ mask (case arch_kernel_object of KOASIDPool asidpool \<Rightarrow> 0 | KOPTE (ARM_H.LargePagePTE xa xaa xb xc xd) \<Rightarrow> 6 | KOPTE _ \<Rightarrow> 0 | KOPDE (ARM_H.SuperSectionPDE xa xaa xb xc xd xe) \<Rightarrow> 6 | KOPDE _ \<Rightarrow> 0) = y && ~~ mask (case arch_kernel_object of KOASIDPool asidpool \<Rightarrow> 0 | KOPTE (ARM_H.LargePagePTE xa xaa xb xc xd) \<Rightarrow> 6 | KOPTE _ \<Rightarrow> 0 | KOPDE (ARM_H.SuperSectionPDE xa xaa xb xc xd xe) \<Rightarrow> 6 | KOPDE _ \<Rightarrow> 0) \<longrightarrow> Some (KOArch arch_kernel_object) = m y)
 2. \<And>x y x2 arch_kernel_object x3. \<lbrakk>x \<notin> {ptr..ptr + 2 ^ sz - 1}; m x = Some (KOArch arch_kernel_object); x2 = KOArch arch_kernel_object; arch_kernel_object = KOPDE x3\<rbrakk> \<Longrightarrow> (y \<in> {ptr..ptr + 2 ^ sz - 1} \<longrightarrow> ((\<exists>ya. m y = Some ya) \<longrightarrow> is_aligned y 2 \<longrightarrow> x && ~~ mask (case arch_kernel_object of KOASIDPool asidpool \<Rightarrow> 0 | KOPTE (ARM_H.LargePagePTE xa xaa xb xc xd) \<Rightarrow> 6 | KOPTE _ \<Rightarrow> 0 | KOPDE (ARM_H.SuperSectionPDE xa xaa xb xc xd xe) \<Rightarrow> 6 | KOPDE _ \<Rightarrow> 0) \<noteq> y && ~~ mask (case arch_kernel_object of KOASIDPool asidpool \<Rightarrow> 0 | KOPTE (ARM_H.LargePagePTE xa xaa xb xc xd) \<Rightarrow> 6 | KOPTE _ \<Rightarrow> 0 | KOPDE (ARM_H.SuperSectionPDE xa xaa xb xc xd xe) \<Rightarrow> 6 | KOPDE _ \<Rightarrow> 0)) \<and> (m y = None \<longrightarrow> is_aligned y 2 \<longrightarrow> x && ~~ mask (case arch_kernel_object of KOASIDPool asidpool \<Rightarrow> 0 | KOPTE (ARM_H.LargePagePTE xa xaa xb xc xd) \<Rightarrow> 6 | KOPTE _ \<Rightarrow> 0 | KOPDE (ARM_H.SuperSectionPDE xa xaa xb xc xd xe) \<Rightarrow> 6 | KOPDE _ \<Rightarrow> 0) \<noteq> y && ~~ mask (case arch_kernel_object of KOASIDPool asidpool \<Rightarrow> 0 | KOPTE (ARM_H.LargePagePTE xa xaa xb xc xd) \<Rightarrow> 6 | KOPTE _ \<Rightarrow> 0 | KOPDE (ARM_H.SuperSectionPDE xa xaa xb xc xd xe) \<Rightarrow> 6 | KOPDE _ \<Rightarrow> 0))) \<and> (y \<notin> {ptr..ptr + 2 ^ sz - 1} \<longrightarrow> is_aligned y 2 \<longrightarrow> x && ~~ mask (case arch_kernel_object of KOASIDPool asidpool \<Rightarrow> 0 | KOPTE (ARM_H.LargePagePTE xa xaa xb xc xd) \<Rightarrow> 6 | KOPTE _ \<Rightarrow> 0 | KOPDE (ARM_H.SuperSectionPDE xa xaa xb xc xd xe) \<Rightarrow> 6 | KOPDE _ \<Rightarrow> 0) = y && ~~ mask (case arch_kernel_object of KOASIDPool asidpool \<Rightarrow> 0 | KOPTE (ARM_H.LargePagePTE xa xaa xb xc xd) \<Rightarrow> 6 | KOPTE _ \<Rightarrow> 0 | KOPDE (ARM_H.SuperSectionPDE xa xaa xb xc xd xe) \<Rightarrow> 6 | KOPDE _ \<Rightarrow> 0) \<longrightarrow> Some (KOArch arch_kernel_object) = m y) proof (prove)
goal (2 subgoals):
 1. \<And>x y x2a. \<lbrakk>x \<notin> {ptr..ptr + 2 ^ sz - 1}; m x = Some (KOArch (KOPTE x2a))\<rbrakk> \<Longrightarrow> (x2a = ARM_H.InvalidPTE \<longrightarrow> (y \<in> {ptr..ptr + 2 ^ sz - 1} \<longrightarrow> ((\<exists>ya. m y = Some ya) \<longrightarrow> is_aligned y 2 \<longrightarrow> x \<noteq> y) \<and> (m y = None \<longrightarrow> is_aligned y 2 \<longrightarrow> x \<noteq> y)) \<and> (y \<notin> {ptr..ptr + 2 ^ sz - 1} \<longrightarrow> is_aligned y 2 \<longrightarrow> x = y \<longrightarrow> Some (KOArch (KOPTE ARM_H.InvalidPTE)) = m y)) \<and> (\<forall>x21 x22 x23 x24 x25. x2a = ARM_H.LargePagePTE x21 x22 x23 x24 x25 \<longrightarrow> (y \<in> {ptr..ptr + 2 ^ sz - 1} \<longrightarrow> ((\<exists>ya. m y = Some ya) \<longrightarrow> is_aligned y 2 \<longrightarrow> x && ~~ mask 6 \<noteq> y && ~~ mask 6) \<and> (m y = None \<longrightarrow> is_aligned y 2 \<longrightarrow> x && ~~ mask 6 \<noteq> y && ~~ mask 6)) \<and> (y \<notin> {ptr..ptr + 2 ^ sz - 1} \<longrightarrow> is_aligned y 2 \<longrightarrow> x && ~~ mask 6 = y && ~~ mask 6 \<longrightarrow> Some (KOArch (KOPTE (ARM_H.LargePagePTE x21 x22 x23 x24 x25))) = m y)) \<and> (\<forall>x31 x32 x33 x34 x35. x2a = ARM_H.SmallPagePTE x31 x32 x33 x34 x35 \<longrightarrow> (y \<in> {ptr..ptr + 2 ^ sz - 1} \<longrightarrow> ((\<exists>ya. m y = Some ya) \<longrightarrow> is_aligned y 2 \<longrightarrow> x \<noteq> y) \<and> (m y = None \<longrightarrow> is_aligned y 2 \<longrightarrow> x \<noteq> y)) \<and> (y \<notin> {ptr..ptr + 2 ^ sz - 1} \<longrightarrow> is_aligned y 2 \<longrightarrow> x = y \<longrightarrow> Some (KOArch (KOPTE (ARM_H.SmallPagePTE x31 x32 x33 x34 x35))) = m y))
 2. \<And>x y x2 arch_kernel_object x3. \<lbrakk>x \<notin> {ptr..ptr + 2 ^ sz - 1}; m x = Some (KOArch arch_kernel_object); x2 = KOArch arch_kernel_object; arch_kernel_object = KOPDE x3\<rbrakk> \<Longrightarrow> (y \<in> {ptr..ptr + 2 ^ sz - 1} \<longrightarrow> ((\<exists>ya. m y = Some ya) \<longrightarrow> is_aligned y 2 \<longrightarrow> x && ~~ mask (case arch_kernel_object of KOASIDPool asidpool \<Rightarrow> 0 | KOPTE (ARM_H.LargePagePTE xa xaa xb xc xd) \<Rightarrow> 6 | KOPTE _ \<Rightarrow> 0 | KOPDE (ARM_H.SuperSectionPDE xa xaa xb xc xd xe) \<Rightarrow> 6 | KOPDE _ \<Rightarrow> 0) \<noteq> y && ~~ mask (case arch_kernel_object of KOASIDPool asidpool \<Rightarrow> 0 | KOPTE (ARM_H.LargePagePTE xa xaa xb xc xd) \<Rightarrow> 6 | KOPTE _ \<Rightarrow> 0 | KOPDE (ARM_H.SuperSectionPDE xa xaa xb xc xd xe) \<Rightarrow> 6 | KOPDE _ \<Rightarrow> 0)) \<and> (m y = None \<longrightarrow> is_aligned y 2 \<longrightarrow> x && ~~ mask (case arch_kernel_object of KOASIDPool asidpool \<Rightarrow> 0 | KOPTE (ARM_H.LargePagePTE xa xaa xb xc xd) \<Rightarrow> 6 | KOPTE _ \<Rightarrow> 0 | KOPDE (ARM_H.SuperSectionPDE xa xaa xb xc xd xe) \<Rightarrow> 6 | KOPDE _ \<Rightarrow> 0) \<noteq> y && ~~ mask (case arch_kernel_object of KOASIDPool asidpool \<Rightarrow> 0 | KOPTE (ARM_H.LargePagePTE xa xaa xb xc xd) \<Rightarrow> 6 | KOPTE _ \<Rightarrow> 0 | KOPDE (ARM_H.SuperSectionPDE xa xaa xb xc xd xe) \<Rightarrow> 6 | KOPDE _ \<Rightarrow> 0))) \<and> (y \<notin> {ptr..ptr + 2 ^ sz - 1} \<longrightarrow> is_aligned y 2 \<longrightarrow> x && ~~ mask (case arch_kernel_object of KOASIDPool asidpool \<Rightarrow> 0 | KOPTE (ARM_H.LargePagePTE xa xaa xb xc xd) \<Rightarrow> 6 | KOPTE _ \<Rightarrow> 0 | KOPDE (ARM_H.SuperSectionPDE xa xaa xb xc xd xe) \<Rightarrow> 6 | KOPDE _ \<Rightarrow> 0) = y && ~~ mask (case arch_kernel_object of KOASIDPool asidpool \<Rightarrow> 0 | KOPTE (ARM_H.LargePagePTE xa xaa xb xc xd) \<Rightarrow> 6 | KOPTE _ \<Rightarrow> 0 | KOPDE (ARM_H.SuperSectionPDE xa xaa xb xc xd xe) \<Rightarrow> 6 | KOPDE _ \<Rightarrow> 0) \<longrightarrow> Some (KOArch arch_kernel_object) = m y) proof (prove)
goal (4 subgoals):
 1. \<And>x y x21 x22 x23 x24 x25 ya. \<lbrakk>x \<notin> {ptr..ptr + 2 ^ sz - 1}; m x = Some (KOArch (KOPTE (ARM_H.LargePagePTE x21 x22 x23 x24 x25))); y \<in> {ptr..ptr + 2 ^ sz - 1}; m y = Some ya; is_aligned y 2; x && ~~ mask 6 = y && ~~ mask 6\<rbrakk> \<Longrightarrow> False
 2. \<And>x y x21 x22 x23 x24 x25. \<lbrakk>x \<notin> {ptr..ptr + 2 ^ sz - 1}; m x = Some (KOArch (KOPTE (ARM_H.LargePagePTE x21 x22 x23 x24 x25))); y \<in> {ptr..ptr + 2 ^ sz - 1}; m y = None; is_aligned y 2; x && ~~ mask 6 = y && ~~ mask 6\<rbrakk> \<Longrightarrow> False
 3. \<And>x y x21 x22 x23 x24 x25. \<lbrakk>x \<notin> {ptr..ptr + 2 ^ sz - 1}; m x = Some (KOArch (KOPTE (ARM_H.LargePagePTE x21 x22 x23 x24 x25))); y \<notin> {ptr..ptr + 2 ^ sz - 1}; is_aligned y 2; x && ~~ mask 6 = y && ~~ mask 6\<rbrakk> \<Longrightarrow> Some (KOArch (KOPTE (ARM_H.LargePagePTE x21 x22 x23 x24 x25))) = m y
 4. \<And>x y x2 arch_kernel_object x3. \<lbrakk>x \<notin> {ptr..ptr + 2 ^ sz - 1}; m x = Some (KOArch arch_kernel_object); x2 = KOArch arch_kernel_object; arch_kernel_object = KOPDE x3\<rbrakk> \<Longrightarrow> (y \<in> {ptr..ptr + 2 ^ sz - 1} \<longrightarrow> ((\<exists>ya. m y = Some ya) \<longrightarrow> is_aligned y 2 \<longrightarrow> x && ~~ mask (case arch_kernel_object of KOASIDPool asidpool \<Rightarrow> 0 | KOPTE (ARM_H.LargePagePTE xa xaa xb xc xd) \<Rightarrow> 6 | KOPTE _ \<Rightarrow> 0 | KOPDE (ARM_H.SuperSectionPDE xa xaa xb xc xd xe) \<Rightarrow> 6 | KOPDE _ \<Rightarrow> 0) \<noteq> y && ~~ mask (case arch_kernel_object of KOASIDPool asidpool \<Rightarrow> 0 | KOPTE (ARM_H.LargePagePTE xa xaa xb xc xd) \<Rightarrow> 6 | KOPTE _ \<Rightarrow> 0 | KOPDE (ARM_H.SuperSectionPDE xa xaa xb xc xd xe) \<Rightarrow> 6 | KOPDE _ \<Rightarrow> 0)) \<and> (m y = None \<longrightarrow> is_aligned y 2 \<longrightarrow> x && ~~ mask (case arch_kernel_object of KOASIDPool asidpool \<Rightarrow> 0 | KOPTE (ARM_H.LargePagePTE xa xaa xb xc xd) \<Rightarrow> 6 | KOPTE _ \<Rightarrow> 0 | KOPDE (ARM_H.SuperSectionPDE xa xaa xb xc xd xe) \<Rightarrow> 6 | KOPDE _ \<Rightarrow> 0) \<noteq> y && ~~ mask (case arch_kernel_object of KOASIDPool asidpool \<Rightarrow> 0 | KOPTE (ARM_H.LargePagePTE xa xaa xb xc xd) \<Rightarrow> 6 | KOPTE _ \<Rightarrow> 0 | KOPDE (ARM_H.SuperSectionPDE xa xaa xb xc xd xe) \<Rightarrow> 6 | KOPDE _ \<Rightarrow> 0))) \<and> (y \<notin> {ptr..ptr + 2 ^ sz - 1} \<longrightarrow> is_aligned y 2 \<longrightarrow> x && ~~ mask (case arch_kernel_object of KOASIDPool asidpool \<Rightarrow> 0 | KOPTE (ARM_H.LargePagePTE xa xaa xb xc xd) \<Rightarrow> 6 | KOPTE _ \<Rightarrow> 0 | KOPDE (ARM_H.SuperSectionPDE xa xaa xb xc xd xe) \<Rightarrow> 6 | KOPDE _ \<Rightarrow> 0) = y && ~~ mask (case arch_kernel_object of KOASIDPool asidpool \<Rightarrow> 0 | KOPTE (ARM_H.LargePagePTE xa xaa xb xc xd) \<Rightarrow> 6 | KOPTE _ \<Rightarrow> 0 | KOPDE (ARM_H.SuperSectionPDE xa xaa xb xc xd xe) \<Rightarrow> 6 | KOPDE _ \<Rightarrow> 0) \<longrightarrow> Some (KOArch arch_kernel_object) = m y) proof (prove)
goal (6 subgoals):
 1. \<And>x y x21 x22 x23 x24 x25 ya. \<lbrakk>x \<notin> {ptr..ptr + 2 ^ sz - 1}; y \<in> {ptr..ptr + 2 ^ sz - 1}; m y = Some ya; is_aligned y 2; x && ~~ mask 6 = y && ~~ mask 6\<rbrakk> \<Longrightarrow> is_aligned y 2
 2. \<And>x y x21 x22 x23 x24 x25 ya. \<lbrakk>x \<notin> {ptr..ptr + 2 ^ sz - 1}; y \<in> {ptr..ptr + 2 ^ sz - 1}; m y = Some ya; is_aligned y 2; x && ~~ mask 6 = y && ~~ mask 6\<rbrakk> \<Longrightarrow> x && ~~ mask (vs_ptr_align (KOArch (KOPTE (ARM_H.LargePagePTE x21 x22 x23 x24 x25)))) = y && ~~ mask (vs_ptr_align (KOArch (KOPTE (ARM_H.LargePagePTE x21 x22 x23 x24 x25))))
 3. \<And>x y x21 x22 x23 x24 x25 ya. \<lbrakk>x \<notin> {ptr..ptr + 2 ^ sz - 1}; y \<in> {ptr..ptr + 2 ^ sz - 1}; m y = Some ya; is_aligned y 2; x && ~~ mask 6 = y && ~~ mask 6; m y = Some (KOArch (KOPTE (ARM_H.LargePagePTE x21 x22 x23 x24 x25)))\<rbrakk> \<Longrightarrow> False
 4. \<And>x y x21 x22 x23 x24 x25. \<lbrakk>x \<notin> {ptr..ptr + 2 ^ sz - 1}; m x = Some (KOArch (KOPTE (ARM_H.LargePagePTE x21 x22 x23 x24 x25))); y \<in> {ptr..ptr + 2 ^ sz - 1}; m y = None; is_aligned y 2; x && ~~ mask 6 = y && ~~ mask 6\<rbrakk> \<Longrightarrow> False
 5. \<And>x y x21 x22 x23 x24 x25. \<lbrakk>x \<notin> {ptr..ptr + 2 ^ sz - 1}; m x = Some (KOArch (KOPTE (ARM_H.LargePagePTE x21 x22 x23 x24 x25))); y \<notin> {ptr..ptr + 2 ^ sz - 1}; is_aligned y 2; x && ~~ mask 6 = y && ~~ mask 6\<rbrakk> \<Longrightarrow> Some (KOArch (KOPTE (ARM_H.LargePagePTE x21 x22 x23 x24 x25))) = m y
 6. \<And>x y x2 arch_kernel_object x3. \<lbrakk>x \<notin> {ptr..ptr + 2 ^ sz - 1}; m x = Some (KOArch arch_kernel_object); x2 = KOArch arch_kernel_object; arch_kernel_object = KOPDE x3\<rbrakk> \<Longrightarrow> (y \<in> {ptr..ptr + 2 ^ sz - 1} \<longrightarrow> ((\<exists>ya. m y = Some ya) \<longrightarrow> is_aligned y 2 \<longrightarrow> x && ~~ mask (case arch_kernel_object of KOASIDPool asidpool \<Rightarrow> 0 | KOPTE (ARM_H.LargePagePTE xa xaa xb xc xd) \<Rightarrow> 6 | KOPTE _ \<Rightarrow> 0 | KOPDE (ARM_H.SuperSectionPDE xa xaa xb xc xd xe) \<Rightarrow> 6 | KOPDE _ \<Rightarrow> 0) \<noteq> y && ~~ mask (case arch_kernel_object of KOASIDPool asidpool \<Rightarrow> 0 | KOPTE (ARM_H.LargePagePTE xa xaa xb xc xd) \<Rightarrow> 6 | KOPTE _ \<Rightarrow> 0 | KOPDE (ARM_H.SuperSectionPDE xa xaa xb xc xd xe) \<Rightarrow> 6 | KOPDE _ \<Rightarrow> 0)) \<and> (m y = None \<longrightarrow> is_aligned y 2 \<longrightarrow> x && ~~ mask (case arch_kernel_object of KOASIDPool asidpool \<Rightarrow> 0 | KOPTE (ARM_H.LargePagePTE xa xaa xb xc xd) \<Rightarrow> 6 | KOPTE _ \<Rightarrow> 0 | KOPDE (ARM_H.SuperSectionPDE xa xaa xb xc xd xe) \<Rightarrow> 6 | KOPDE _ \<Rightarrow> 0) \<noteq> y && ~~ mask (case arch_kernel_object of KOASIDPool asidpool \<Rightarrow> 0 | KOPTE (ARM_H.LargePagePTE xa xaa xb xc xd) \<Rightarrow> 6 | KOPTE _ \<Rightarrow> 0 | KOPDE (ARM_H.SuperSectionPDE xa xaa xb xc xd xe) \<Rightarrow> 6 | KOPDE _ \<Rightarrow> 0))) \<and> (y \<notin> {ptr..ptr + 2 ^ sz - 1} \<longrightarrow> is_aligned y 2 \<longrightarrow> x && ~~ mask (case arch_kernel_object of KOASIDPool asidpool \<Rightarrow> 0 | KOPTE (ARM_H.LargePagePTE xa xaa xb xc xd) \<Rightarrow> 6 | KOPTE _ \<Rightarrow> 0 | KOPDE (ARM_H.SuperSectionPDE xa xaa xb xc xd xe) \<Rightarrow> 6 | KOPDE _ \<Rightarrow> 0) = y && ~~ mask (case arch_kernel_object of KOASIDPool asidpool \<Rightarrow> 0 | KOPTE (ARM_H.LargePagePTE xa xaa xb xc xd) \<Rightarrow> 6 | KOPTE _ \<Rightarrow> 0 | KOPDE (ARM_H.SuperSectionPDE xa xaa xb xc xd xe) \<Rightarrow> 6 | KOPDE _ \<Rightarrow> 0) \<longrightarrow> Some (KOArch arch_kernel_object) = m y) proof (prove)
goal (4 subgoals):
 1. \<And>x y x21 x22 x23 x24 x25 ya. \<lbrakk>x \<notin> {ptr..ptr + 2 ^ sz - 1}; y \<in> {ptr..ptr + 2 ^ sz - 1}; KOArch (KOPTE (ARM_H.LargePagePTE x21 x22 x23 x24 x25)) = ya; is_aligned y 2; x && ~~ mask 6 = y && ~~ mask 6; m y = Some ya\<rbrakk> \<Longrightarrow> False
 2. \<And>x y x21 x22 x23 x24 x25. \<lbrakk>x \<notin> {ptr..ptr + 2 ^ sz - 1}; m x = Some (KOArch (KOPTE (ARM_H.LargePagePTE x21 x22 x23 x24 x25))); y \<in> {ptr..ptr + 2 ^ sz - 1}; m y = None; is_aligned y 2; x && ~~ mask 6 = y && ~~ mask 6\<rbrakk> \<Longrightarrow> False
 3. \<And>x y x21 x22 x23 x24 x25. \<lbrakk>x \<notin> {ptr..ptr + 2 ^ sz - 1}; m x = Some (KOArch (KOPTE (ARM_H.LargePagePTE x21 x22 x23 x24 x25))); y \<notin> {ptr..ptr + 2 ^ sz - 1}; is_aligned y 2; x && ~~ mask 6 = y && ~~ mask 6\<rbrakk> \<Longrightarrow> Some (KOArch (KOPTE (ARM_H.LargePagePTE x21 x22 x23 x24 x25))) = m y
 4. \<And>x y x2 arch_kernel_object x3. \<lbrakk>x \<notin> {ptr..ptr + 2 ^ sz - 1}; m x = Some (KOArch arch_kernel_object); x2 = KOArch arch_kernel_object; arch_kernel_object = KOPDE x3\<rbrakk> \<Longrightarrow> (y \<in> {ptr..ptr + 2 ^ sz - 1} \<longrightarrow> ((\<exists>ya. m y = Some ya) \<longrightarrow> is_aligned y 2 \<longrightarrow> x && ~~ mask (case arch_kernel_object of KOASIDPool asidpool \<Rightarrow> 0 | KOPTE (ARM_H.LargePagePTE xa xaa xb xc xd) \<Rightarrow> 6 | KOPTE _ \<Rightarrow> 0 | KOPDE (ARM_H.SuperSectionPDE xa xaa xb xc xd xe) \<Rightarrow> 6 | KOPDE _ \<Rightarrow> 0) \<noteq> y && ~~ mask (case arch_kernel_object of KOASIDPool asidpool \<Rightarrow> 0 | KOPTE (ARM_H.LargePagePTE xa xaa xb xc xd) \<Rightarrow> 6 | KOPTE _ \<Rightarrow> 0 | KOPDE (ARM_H.SuperSectionPDE xa xaa xb xc xd xe) \<Rightarrow> 6 | KOPDE _ \<Rightarrow> 0)) \<and> (m y = None \<longrightarrow> is_aligned y 2 \<longrightarrow> x && ~~ mask (case arch_kernel_object of KOASIDPool asidpool \<Rightarrow> 0 | KOPTE (ARM_H.LargePagePTE xa xaa xb xc xd) \<Rightarrow> 6 | KOPTE _ \<Rightarrow> 0 | KOPDE (ARM_H.SuperSectionPDE xa xaa xb xc xd xe) \<Rightarrow> 6 | KOPDE _ \<Rightarrow> 0) \<noteq> y && ~~ mask (case arch_kernel_object of KOASIDPool asidpool \<Rightarrow> 0 | KOPTE (ARM_H.LargePagePTE xa xaa xb xc xd) \<Rightarrow> 6 | KOPTE _ \<Rightarrow> 0 | KOPDE (ARM_H.SuperSectionPDE xa xaa xb xc xd xe) \<Rightarrow> 6 | KOPDE _ \<Rightarrow> 0))) \<and> (y \<notin> {ptr..ptr + 2 ^ sz - 1} \<longrightarrow> is_aligned y 2 \<longrightarrow> x && ~~ mask (case arch_kernel_object of KOASIDPool asidpool \<Rightarrow> 0 | KOPTE (ARM_H.LargePagePTE xa xaa xb xc xd) \<Rightarrow> 6 | KOPTE _ \<Rightarrow> 0 | KOPDE (ARM_H.SuperSectionPDE xa xaa xb xc xd xe) \<Rightarrow> 6 | KOPDE _ \<Rightarrow> 0) = y && ~~ mask (case arch_kernel_object of KOASIDPool asidpool \<Rightarrow> 0 | KOPTE (ARM_H.LargePagePTE xa xaa xb xc xd) \<Rightarrow> 6 | KOPTE _ \<Rightarrow> 0 | KOPDE (ARM_H.SuperSectionPDE xa xaa xb xc xd xe) \<Rightarrow> 6 | KOPDE _ \<Rightarrow> 0) \<longrightarrow> Some (KOArch arch_kernel_object) = m y) proof (prove)
goal (4 subgoals):
 1. \<And>x y x21 x22 x23 x24 x25. \<lbrakk>x \<notin> {ptr..ptr + 2 ^ sz - 1}; y \<in> {ptr..ptr + 2 ^ sz - 1}; is_aligned y 2; x && ~~ mask 6 = y && ~~ mask 6; m y = Some (KOArch (KOPTE (ARM_H.LargePagePTE x21 x22 x23 x24 x25)))\<rbrakk> \<Longrightarrow> False
 2. \<And>x y x21 x22 x23 x24 x25. \<lbrakk>x \<notin> {ptr..ptr + 2 ^ sz - 1}; m x = Some (KOArch (KOPTE (ARM_H.LargePagePTE x21 x22 x23 x24 x25))); y \<in> {ptr..ptr + 2 ^ sz - 1}; m y = None; is_aligned y 2; x && ~~ mask 6 = y && ~~ mask 6\<rbrakk> \<Longrightarrow> False
 3. \<And>x y x21 x22 x23 x24 x25. \<lbrakk>x \<notin> {ptr..ptr + 2 ^ sz - 1}; m x = Some (KOArch (KOPTE (ARM_H.LargePagePTE x21 x22 x23 x24 x25))); y \<notin> {ptr..ptr + 2 ^ sz - 1}; is_aligned y 2; x && ~~ mask 6 = y && ~~ mask 6\<rbrakk> \<Longrightarrow> Some (KOArch (KOPTE (ARM_H.LargePagePTE x21 x22 x23 x24 x25))) = m y
 4. \<And>x y x2 arch_kernel_object x3. \<lbrakk>x \<notin> {ptr..ptr + 2 ^ sz - 1}; m x = Some (KOArch arch_kernel_object); x2 = KOArch arch_kernel_object; arch_kernel_object = KOPDE x3\<rbrakk> \<Longrightarrow> (y \<in> {ptr..ptr + 2 ^ sz - 1} \<longrightarrow> ((\<exists>ya. m y = Some ya) \<longrightarrow> is_aligned y 2 \<longrightarrow> x && ~~ mask (case arch_kernel_object of KOASIDPool asidpool \<Rightarrow> 0 | KOPTE (ARM_H.LargePagePTE xa xaa xb xc xd) \<Rightarrow> 6 | KOPTE _ \<Rightarrow> 0 | KOPDE (ARM_H.SuperSectionPDE xa xaa xb xc xd xe) \<Rightarrow> 6 | KOPDE _ \<Rightarrow> 0) \<noteq> y && ~~ mask (case arch_kernel_object of KOASIDPool asidpool \<Rightarrow> 0 | KOPTE (ARM_H.LargePagePTE xa xaa xb xc xd) \<Rightarrow> 6 | KOPTE _ \<Rightarrow> 0 | KOPDE (ARM_H.SuperSectionPDE xa xaa xb xc xd xe) \<Rightarrow> 6 | KOPDE _ \<Rightarrow> 0)) \<and> (m y = None \<longrightarrow> is_aligned y 2 \<longrightarrow> x && ~~ mask (case arch_kernel_object of KOASIDPool asidpool \<Rightarrow> 0 | KOPTE (ARM_H.LargePagePTE xa xaa xb xc xd) \<Rightarrow> 6 | KOPTE _ \<Rightarrow> 0 | KOPDE (ARM_H.SuperSectionPDE xa xaa xb xc xd xe) \<Rightarrow> 6 | KOPDE _ \<Rightarrow> 0) \<noteq> y && ~~ mask (case arch_kernel_object of KOASIDPool asidpool \<Rightarrow> 0 | KOPTE (ARM_H.LargePagePTE xa xaa xb xc xd) \<Rightarrow> 6 | KOPTE _ \<Rightarrow> 0 | KOPDE (ARM_H.SuperSectionPDE xa xaa xb xc xd xe) \<Rightarrow> 6 | KOPDE _ \<Rightarrow> 0))) \<and> (y \<notin> {ptr..ptr + 2 ^ sz - 1} \<longrightarrow> is_aligned y 2 \<longrightarrow> x && ~~ mask (case arch_kernel_object of KOASIDPool asidpool \<Rightarrow> 0 | KOPTE (ARM_H.LargePagePTE xa xaa xb xc xd) \<Rightarrow> 6 | KOPTE _ \<Rightarrow> 0 | KOPDE (ARM_H.SuperSectionPDE xa xaa xb xc xd xe) \<Rightarrow> 6 | KOPDE _ \<Rightarrow> 0) = y && ~~ mask (case arch_kernel_object of KOASIDPool asidpool \<Rightarrow> 0 | KOPTE (ARM_H.LargePagePTE xa xaa xb xc xd) \<Rightarrow> 6 | KOPTE _ \<Rightarrow> 0 | KOPDE (ARM_H.SuperSectionPDE xa xaa xb xc xd xe) \<Rightarrow> 6 | KOPDE _ \<Rightarrow> 0) \<longrightarrow> Some (KOArch arch_kernel_object) = m y) proof (prove)
goal (4 subgoals):
 1. \<And>x y x21 x22 x23 x24 x25. \<lbrakk>x \<notin> {ptr..ptr + 2 ^ sz - 1}; y \<in> {ptr..ptr + 2 ^ sz - 1}; is_aligned y 2; x && ~~ mask 6 = y && ~~ mask 6; 6 \<le> sz\<rbrakk> \<Longrightarrow> False
 2. \<And>x y x21 x22 x23 x24 x25. \<lbrakk>x \<notin> {ptr..ptr + 2 ^ sz - 1}; m x = Some (KOArch (KOPTE (ARM_H.LargePagePTE x21 x22 x23 x24 x25))); y \<in> {ptr..ptr + 2 ^ sz - 1}; m y = None; is_aligned y 2; x && ~~ mask 6 = y && ~~ mask 6\<rbrakk> \<Longrightarrow> False
 3. \<And>x y x21 x22 x23 x24 x25. \<lbrakk>x \<notin> {ptr..ptr + 2 ^ sz - 1}; m x = Some (KOArch (KOPTE (ARM_H.LargePagePTE x21 x22 x23 x24 x25))); y \<notin> {ptr..ptr + 2 ^ sz - 1}; is_aligned y 2; x && ~~ mask 6 = y && ~~ mask 6\<rbrakk> \<Longrightarrow> Some (KOArch (KOPTE (ARM_H.LargePagePTE x21 x22 x23 x24 x25))) = m y
 4. \<And>x y x2 arch_kernel_object x3. \<lbrakk>x \<notin> {ptr..ptr + 2 ^ sz - 1}; m x = Some (KOArch arch_kernel_object); x2 = KOArch arch_kernel_object; arch_kernel_object = KOPDE x3\<rbrakk> \<Longrightarrow> (y \<in> {ptr..ptr + 2 ^ sz - 1} \<longrightarrow> ((\<exists>ya. m y = Some ya) \<longrightarrow> is_aligned y 2 \<longrightarrow> x && ~~ mask (case arch_kernel_object of KOASIDPool asidpool \<Rightarrow> 0 | KOPTE (ARM_H.LargePagePTE xa xaa xb xc xd) \<Rightarrow> 6 | KOPTE _ \<Rightarrow> 0 | KOPDE (ARM_H.SuperSectionPDE xa xaa xb xc xd xe) \<Rightarrow> 6 | KOPDE _ \<Rightarrow> 0) \<noteq> y && ~~ mask (case arch_kernel_object of KOASIDPool asidpool \<Rightarrow> 0 | KOPTE (ARM_H.LargePagePTE xa xaa xb xc xd) \<Rightarrow> 6 | KOPTE _ \<Rightarrow> 0 | KOPDE (ARM_H.SuperSectionPDE xa xaa xb xc xd xe) \<Rightarrow> 6 | KOPDE _ \<Rightarrow> 0)) \<and> (m y = None \<longrightarrow> is_aligned y 2 \<longrightarrow> x && ~~ mask (case arch_kernel_object of KOASIDPool asidpool \<Rightarrow> 0 | KOPTE (ARM_H.LargePagePTE xa xaa xb xc xd) \<Rightarrow> 6 | KOPTE _ \<Rightarrow> 0 | KOPDE (ARM_H.SuperSectionPDE xa xaa xb xc xd xe) \<Rightarrow> 6 | KOPDE _ \<Rightarrow> 0) \<noteq> y && ~~ mask (case arch_kernel_object of KOASIDPool asidpool \<Rightarrow> 0 | KOPTE (ARM_H.LargePagePTE xa xaa xb xc xd) \<Rightarrow> 6 | KOPTE _ \<Rightarrow> 0 | KOPDE (ARM_H.SuperSectionPDE xa xaa xb xc xd xe) \<Rightarrow> 6 | KOPDE _ \<Rightarrow> 0))) \<and> (y \<notin> {ptr..ptr + 2 ^ sz - 1} \<longrightarrow> is_aligned y 2 \<longrightarrow> x && ~~ mask (case arch_kernel_object of KOASIDPool asidpool \<Rightarrow> 0 | KOPTE (ARM_H.LargePagePTE xa xaa xb xc xd) \<Rightarrow> 6 | KOPTE _ \<Rightarrow> 0 | KOPDE (ARM_H.SuperSectionPDE xa xaa xb xc xd xe) \<Rightarrow> 6 | KOPDE _ \<Rightarrow> 0) = y && ~~ mask (case arch_kernel_object of KOASIDPool asidpool \<Rightarrow> 0 | KOPTE (ARM_H.LargePagePTE xa xaa xb xc xd) \<Rightarrow> 6 | KOPTE _ \<Rightarrow> 0 | KOPDE (ARM_H.SuperSectionPDE xa xaa xb xc xd xe) \<Rightarrow> 6 | KOPDE _ \<Rightarrow> 0) \<longrightarrow> Some (KOArch arch_kernel_object) = m y) proof (prove)
goal (4 subgoals):
 1. \<And>x y x21 x22 x23 x24 x25. \<lbrakk>x \<notin> {ptr..ptr + 2 ^ sz - 1}; y \<in> {ptr..ptr + 2 ^ sz - 1}; is_aligned y 2; 6 \<le> sz; x && ~~ mask sz = (y && ~~ mask 6) && ~~ mask sz\<rbrakk> \<Longrightarrow> False
 2. \<And>x y x21 x22 x23 x24 x25. \<lbrakk>x \<notin> {ptr..ptr + 2 ^ sz - 1}; m x = Some (KOArch (KOPTE (ARM_H.LargePagePTE x21 x22 x23 x24 x25))); y \<in> {ptr..ptr + 2 ^ sz - 1}; m y = None; is_aligned y 2; x && ~~ mask 6 = y && ~~ mask 6\<rbrakk> \<Longrightarrow> False
 3. \<And>x y x21 x22 x23 x24 x25. \<lbrakk>x \<notin> {ptr..ptr + 2 ^ sz - 1}; m x = Some (KOArch (KOPTE (ARM_H.LargePagePTE x21 x22 x23 x24 x25))); y \<notin> {ptr..ptr + 2 ^ sz - 1}; is_aligned y 2; x && ~~ mask 6 = y && ~~ mask 6\<rbrakk> \<Longrightarrow> Some (KOArch (KOPTE (ARM_H.LargePagePTE x21 x22 x23 x24 x25))) = m y
 4. \<And>x y x2 arch_kernel_object x3. \<lbrakk>x \<notin> {ptr..ptr + 2 ^ sz - 1}; m x = Some (KOArch arch_kernel_object); x2 = KOArch arch_kernel_object; arch_kernel_object = KOPDE x3\<rbrakk> \<Longrightarrow> (y \<in> {ptr..ptr + 2 ^ sz - 1} \<longrightarrow> ((\<exists>ya. m y = Some ya) \<longrightarrow> is_aligned y 2 \<longrightarrow> x && ~~ mask (case arch_kernel_object of KOASIDPool asidpool \<Rightarrow> 0 | KOPTE (ARM_H.LargePagePTE xa xaa xb xc xd) \<Rightarrow> 6 | KOPTE _ \<Rightarrow> 0 | KOPDE (ARM_H.SuperSectionPDE xa xaa xb xc xd xe) \<Rightarrow> 6 | KOPDE _ \<Rightarrow> 0) \<noteq> y && ~~ mask (case arch_kernel_object of KOASIDPool asidpool \<Rightarrow> 0 | KOPTE (ARM_H.LargePagePTE xa xaa xb xc xd) \<Rightarrow> 6 | KOPTE _ \<Rightarrow> 0 | KOPDE (ARM_H.SuperSectionPDE xa xaa xb xc xd xe) \<Rightarrow> 6 | KOPDE _ \<Rightarrow> 0)) \<and> (m y = None \<longrightarrow> is_aligned y 2 \<longrightarrow> x && ~~ mask (case arch_kernel_object of KOASIDPool asidpool \<Rightarrow> 0 | KOPTE (ARM_H.LargePagePTE xa xaa xb xc xd) \<Rightarrow> 6 | KOPTE _ \<Rightarrow> 0 | KOPDE (ARM_H.SuperSectionPDE xa xaa xb xc xd xe) \<Rightarrow> 6 | KOPDE _ \<Rightarrow> 0) \<noteq> y && ~~ mask (case arch_kernel_object of KOASIDPool asidpool \<Rightarrow> 0 | KOPTE (ARM_H.LargePagePTE xa xaa xb xc xd) \<Rightarrow> 6 | KOPTE _ \<Rightarrow> 0 | KOPDE (ARM_H.SuperSectionPDE xa xaa xb xc xd xe) \<Rightarrow> 6 | KOPDE _ \<Rightarrow> 0))) \<and> (y \<notin> {ptr..ptr + 2 ^ sz - 1} \<longrightarrow> is_aligned y 2 \<longrightarrow> x && ~~ mask (case arch_kernel_object of KOASIDPool asidpool \<Rightarrow> 0 | KOPTE (ARM_H.LargePagePTE xa xaa xb xc xd) \<Rightarrow> 6 | KOPTE _ \<Rightarrow> 0 | KOPDE (ARM_H.SuperSectionPDE xa xaa xb xc xd xe) \<Rightarrow> 6 | KOPDE _ \<Rightarrow> 0) = y && ~~ mask (case arch_kernel_object of KOASIDPool asidpool \<Rightarrow> 0 | KOPTE (ARM_H.LargePagePTE xa xaa xb xc xd) \<Rightarrow> 6 | KOPTE _ \<Rightarrow> 0 | KOPDE (ARM_H.SuperSectionPDE xa xaa xb xc xd xe) \<Rightarrow> 6 | KOPDE _ \<Rightarrow> 0) \<longrightarrow> Some (KOArch arch_kernel_object) = m y) proof (prove)
goal (4 subgoals):
 1. \<And>x y. \<lbrakk>x \<notin> {ptr..ptr + 2 ^ sz - 1}; y \<in> {ptr..ptr + 2 ^ sz - 1}; is_aligned y 2; 6 \<le> sz; x && ~~ mask sz = y && ~~ mask sz\<rbrakk> \<Longrightarrow> False
 2. \<And>x y x21 x22 x23 x24 x25. \<lbrakk>x \<notin> {ptr..ptr + 2 ^ sz - 1}; m x = Some (KOArch (KOPTE (ARM_H.LargePagePTE x21 x22 x23 x24 x25))); y \<in> {ptr..ptr + 2 ^ sz - 1}; m y = None; is_aligned y 2; x && ~~ mask 6 = y && ~~ mask 6\<rbrakk> \<Longrightarrow> False
 3. \<And>x y x21 x22 x23 x24 x25. \<lbrakk>x \<notin> {ptr..ptr + 2 ^ sz - 1}; m x = Some (KOArch (KOPTE (ARM_H.LargePagePTE x21 x22 x23 x24 x25))); y \<notin> {ptr..ptr + 2 ^ sz - 1}; is_aligned y 2; x && ~~ mask 6 = y && ~~ mask 6\<rbrakk> \<Longrightarrow> Some (KOArch (KOPTE (ARM_H.LargePagePTE x21 x22 x23 x24 x25))) = m y
 4. \<And>x y x2 arch_kernel_object x3. \<lbrakk>x \<notin> {ptr..ptr + 2 ^ sz - 1}; m x = Some (KOArch arch_kernel_object); x2 = KOArch arch_kernel_object; arch_kernel_object = KOPDE x3\<rbrakk> \<Longrightarrow> (y \<in> {ptr..ptr + 2 ^ sz - 1} \<longrightarrow> ((\<exists>ya. m y = Some ya) \<longrightarrow> is_aligned y 2 \<longrightarrow> x && ~~ mask (case arch_kernel_object of KOASIDPool asidpool \<Rightarrow> 0 | KOPTE (ARM_H.LargePagePTE xa xaa xb xc xd) \<Rightarrow> 6 | KOPTE _ \<Rightarrow> 0 | KOPDE (ARM_H.SuperSectionPDE xa xaa xb xc xd xe) \<Rightarrow> 6 | KOPDE _ \<Rightarrow> 0) \<noteq> y && ~~ mask (case arch_kernel_object of KOASIDPool asidpool \<Rightarrow> 0 | KOPTE (ARM_H.LargePagePTE xa xaa xb xc xd) \<Rightarrow> 6 | KOPTE _ \<Rightarrow> 0 | KOPDE (ARM_H.SuperSectionPDE xa xaa xb xc xd xe) \<Rightarrow> 6 | KOPDE _ \<Rightarrow> 0)) \<and> (m y = None \<longrightarrow> is_aligned y 2 \<longrightarrow> x && ~~ mask (case arch_kernel_object of KOASIDPool asidpool \<Rightarrow> 0 | KOPTE (ARM_H.LargePagePTE xa xaa xb xc xd) \<Rightarrow> 6 | KOPTE _ \<Rightarrow> 0 | KOPDE (ARM_H.SuperSectionPDE xa xaa xb xc xd xe) \<Rightarrow> 6 | KOPDE _ \<Rightarrow> 0) \<noteq> y && ~~ mask (case arch_kernel_object of KOASIDPool asidpool \<Rightarrow> 0 | KOPTE (ARM_H.LargePagePTE xa xaa xb xc xd) \<Rightarrow> 6 | KOPTE _ \<Rightarrow> 0 | KOPDE (ARM_H.SuperSectionPDE xa xaa xb xc xd xe) \<Rightarrow> 6 | KOPDE _ \<Rightarrow> 0))) \<and> (y \<notin> {ptr..ptr + 2 ^ sz - 1} \<longrightarrow> is_aligned y 2 \<longrightarrow> x && ~~ mask (case arch_kernel_object of KOASIDPool asidpool \<Rightarrow> 0 | KOPTE (ARM_H.LargePagePTE xa xaa xb xc xd) \<Rightarrow> 6 | KOPTE _ \<Rightarrow> 0 | KOPDE (ARM_H.SuperSectionPDE xa xaa xb xc xd xe) \<Rightarrow> 6 | KOPDE _ \<Rightarrow> 0) = y && ~~ mask (case arch_kernel_object of KOASIDPool asidpool \<Rightarrow> 0 | KOPTE (ARM_H.LargePagePTE xa xaa xb xc xd) \<Rightarrow> 6 | KOPTE _ \<Rightarrow> 0 | KOPDE (ARM_H.SuperSectionPDE xa xaa xb xc xd xe) \<Rightarrow> 6 | KOPDE _ \<Rightarrow> 0) \<longrightarrow> Some (KOArch arch_kernel_object) = m y) proof (prove)
goal (3 subgoals):
 1. \<And>x y x21 x22 x23 x24 x25. \<lbrakk>x \<notin> {ptr..ptr + 2 ^ sz - 1}; m x = Some (KOArch (KOPTE (ARM_H.LargePagePTE x21 x22 x23 x24 x25))); y \<in> {ptr..ptr + 2 ^ sz - 1}; m y = None; is_aligned y 2; x && ~~ mask 6 = y && ~~ mask 6\<rbrakk> \<Longrightarrow> False
 2. \<And>x y x21 x22 x23 x24 x25. \<lbrakk>x \<notin> {ptr..ptr + 2 ^ sz - 1}; m x = Some (KOArch (KOPTE (ARM_H.LargePagePTE x21 x22 x23 x24 x25))); y \<notin> {ptr..ptr + 2 ^ sz - 1}; is_aligned y 2; x && ~~ mask 6 = y && ~~ mask 6\<rbrakk> \<Longrightarrow> Some (KOArch (KOPTE (ARM_H.LargePagePTE x21 x22 x23 x24 x25))) = m y
 3. \<And>x y x2 arch_kernel_object x3. \<lbrakk>x \<notin> {ptr..ptr + 2 ^ sz - 1}; m x = Some (KOArch arch_kernel_object); x2 = KOArch arch_kernel_object; arch_kernel_object = KOPDE x3\<rbrakk> \<Longrightarrow> (y \<in> {ptr..ptr + 2 ^ sz - 1} \<longrightarrow> ((\<exists>ya. m y = Some ya) \<longrightarrow> is_aligned y 2 \<longrightarrow> x && ~~ mask (case arch_kernel_object of KOASIDPool asidpool \<Rightarrow> 0 | KOPTE (ARM_H.LargePagePTE xa xaa xb xc xd) \<Rightarrow> 6 | KOPTE _ \<Rightarrow> 0 | KOPDE (ARM_H.SuperSectionPDE xa xaa xb xc xd xe) \<Rightarrow> 6 | KOPDE _ \<Rightarrow> 0) \<noteq> y && ~~ mask (case arch_kernel_object of KOASIDPool asidpool \<Rightarrow> 0 | KOPTE (ARM_H.LargePagePTE xa xaa xb xc xd) \<Rightarrow> 6 | KOPTE _ \<Rightarrow> 0 | KOPDE (ARM_H.SuperSectionPDE xa xaa xb xc xd xe) \<Rightarrow> 6 | KOPDE _ \<Rightarrow> 0)) \<and> (m y = None \<longrightarrow> is_aligned y 2 \<longrightarrow> x && ~~ mask (case arch_kernel_object of KOASIDPool asidpool \<Rightarrow> 0 | KOPTE (ARM_H.LargePagePTE xa xaa xb xc xd) \<Rightarrow> 6 | KOPTE _ \<Rightarrow> 0 | KOPDE (ARM_H.SuperSectionPDE xa xaa xb xc xd xe) \<Rightarrow> 6 | KOPDE _ \<Rightarrow> 0) \<noteq> y && ~~ mask (case arch_kernel_object of KOASIDPool asidpool \<Rightarrow> 0 | KOPTE (ARM_H.LargePagePTE xa xaa xb xc xd) \<Rightarrow> 6 | KOPTE _ \<Rightarrow> 0 | KOPDE (ARM_H.SuperSectionPDE xa xaa xb xc xd xe) \<Rightarrow> 6 | KOPDE _ \<Rightarrow> 0))) \<and> (y \<notin> {ptr..ptr + 2 ^ sz - 1} \<longrightarrow> is_aligned y 2 \<longrightarrow> x && ~~ mask (case arch_kernel_object of KOASIDPool asidpool \<Rightarrow> 0 | KOPTE (ARM_H.LargePagePTE xa xaa xb xc xd) \<Rightarrow> 6 | KOPTE _ \<Rightarrow> 0 | KOPDE (ARM_H.SuperSectionPDE xa xaa xb xc xd xe) \<Rightarrow> 6 | KOPDE _ \<Rightarrow> 0) = y && ~~ mask (case arch_kernel_object of KOASIDPool asidpool \<Rightarrow> 0 | KOPTE (ARM_H.LargePagePTE xa xaa xb xc xd) \<Rightarrow> 6 | KOPTE _ \<Rightarrow> 0 | KOPDE (ARM_H.SuperSectionPDE xa xaa xb xc xd xe) \<Rightarrow> 6 | KOPDE _ \<Rightarrow> 0) \<longrightarrow> Some (KOArch arch_kernel_object) = m y) proof (prove)
goal (5 subgoals):
 1. \<And>x y x21 x22 x23 x24 x25. \<lbrakk>x \<notin> {ptr..ptr + 2 ^ sz - 1}; y \<in> {ptr..ptr + 2 ^ sz - 1}; m y = None; is_aligned y 2; x && ~~ mask 6 = y && ~~ mask 6\<rbrakk> \<Longrightarrow> is_aligned y 2
 2. \<And>x y x21 x22 x23 x24 x25. \<lbrakk>x \<notin> {ptr..ptr + 2 ^ sz - 1}; y \<in> {ptr..ptr + 2 ^ sz - 1}; m y = None; is_aligned y 2; x && ~~ mask 6 = y && ~~ mask 6\<rbrakk> \<Longrightarrow> x && ~~ mask (vs_ptr_align (KOArch (KOPTE (ARM_H.LargePagePTE x21 x22 x23 x24 x25)))) = y && ~~ mask (vs_ptr_align (KOArch (KOPTE (ARM_H.LargePagePTE x21 x22 x23 x24 x25))))
 3. \<And>x y x21 x22 x23 x24 x25. \<lbrakk>x \<notin> {ptr..ptr + 2 ^ sz - 1}; y \<in> {ptr..ptr + 2 ^ sz - 1}; m y = None; is_aligned y 2; x && ~~ mask 6 = y && ~~ mask 6; m y = Some (KOArch (KOPTE (ARM_H.LargePagePTE x21 x22 x23 x24 x25)))\<rbrakk> \<Longrightarrow> False
 4. \<And>x y x21 x22 x23 x24 x25. \<lbrakk>x \<notin> {ptr..ptr + 2 ^ sz - 1}; m x = Some (KOArch (KOPTE (ARM_H.LargePagePTE x21 x22 x23 x24 x25))); y \<notin> {ptr..ptr + 2 ^ sz - 1}; is_aligned y 2; x && ~~ mask 6 = y && ~~ mask 6\<rbrakk> \<Longrightarrow> Some (KOArch (KOPTE (ARM_H.LargePagePTE x21 x22 x23 x24 x25))) = m y
 5. \<And>x y x2 arch_kernel_object x3. \<lbrakk>x \<notin> {ptr..ptr + 2 ^ sz - 1}; m x = Some (KOArch arch_kernel_object); x2 = KOArch arch_kernel_object; arch_kernel_object = KOPDE x3\<rbrakk> \<Longrightarrow> (y \<in> {ptr..ptr + 2 ^ sz - 1} \<longrightarrow> ((\<exists>ya. m y = Some ya) \<longrightarrow> is_aligned y 2 \<longrightarrow> x && ~~ mask (case arch_kernel_object of KOASIDPool asidpool \<Rightarrow> 0 | KOPTE (ARM_H.LargePagePTE xa xaa xb xc xd) \<Rightarrow> 6 | KOPTE _ \<Rightarrow> 0 | KOPDE (ARM_H.SuperSectionPDE xa xaa xb xc xd xe) \<Rightarrow> 6 | KOPDE _ \<Rightarrow> 0) \<noteq> y && ~~ mask (case arch_kernel_object of KOASIDPool asidpool \<Rightarrow> 0 | KOPTE (ARM_H.LargePagePTE xa xaa xb xc xd) \<Rightarrow> 6 | KOPTE _ \<Rightarrow> 0 | KOPDE (ARM_H.SuperSectionPDE xa xaa xb xc xd xe) \<Rightarrow> 6 | KOPDE _ \<Rightarrow> 0)) \<and> (m y = None \<longrightarrow> is_aligned y 2 \<longrightarrow> x && ~~ mask (case arch_kernel_object of KOASIDPool asidpool \<Rightarrow> 0 | KOPTE (ARM_H.LargePagePTE xa xaa xb xc xd) \<Rightarrow> 6 | KOPTE _ \<Rightarrow> 0 | KOPDE (ARM_H.SuperSectionPDE xa xaa xb xc xd xe) \<Rightarrow> 6 | KOPDE _ \<Rightarrow> 0) \<noteq> y && ~~ mask (case arch_kernel_object of KOASIDPool asidpool \<Rightarrow> 0 | KOPTE (ARM_H.LargePagePTE xa xaa xb xc xd) \<Rightarrow> 6 | KOPTE _ \<Rightarrow> 0 | KOPDE (ARM_H.SuperSectionPDE xa xaa xb xc xd xe) \<Rightarrow> 6 | KOPDE _ \<Rightarrow> 0))) \<and> (y \<notin> {ptr..ptr + 2 ^ sz - 1} \<longrightarrow> is_aligned y 2 \<longrightarrow> x && ~~ mask (case arch_kernel_object of KOASIDPool asidpool \<Rightarrow> 0 | KOPTE (ARM_H.LargePagePTE xa xaa xb xc xd) \<Rightarrow> 6 | KOPTE _ \<Rightarrow> 0 | KOPDE (ARM_H.SuperSectionPDE xa xaa xb xc xd xe) \<Rightarrow> 6 | KOPDE _ \<Rightarrow> 0) = y && ~~ mask (case arch_kernel_object of KOASIDPool asidpool \<Rightarrow> 0 | KOPTE (ARM_H.LargePagePTE xa xaa xb xc xd) \<Rightarrow> 6 | KOPTE _ \<Rightarrow> 0 | KOPDE (ARM_H.SuperSectionPDE xa xaa xb xc xd xe) \<Rightarrow> 6 | KOPDE _ \<Rightarrow> 0) \<longrightarrow> Some (KOArch arch_kernel_object) = m y) proof (prove)
goal (4 subgoals):
 1. \<And>x y x21 x22 x23 x24 x25. \<lbrakk>x \<notin> {ptr..ptr + 2 ^ sz - 1}; y \<in> {ptr..ptr + 2 ^ sz - 1}; m y = None; is_aligned y 2; x && ~~ mask 6 = y && ~~ mask 6\<rbrakk> \<Longrightarrow> x && ~~ mask (vs_ptr_align (KOArch (KOPTE (ARM_H.LargePagePTE x21 x22 x23 x24 x25)))) = y && ~~ mask (vs_ptr_align (KOArch (KOPTE (ARM_H.LargePagePTE x21 x22 x23 x24 x25))))
 2. \<And>x y x21 x22 x23 x24 x25. \<lbrakk>x \<notin> {ptr..ptr + 2 ^ sz - 1}; y \<in> {ptr..ptr + 2 ^ sz - 1}; m y = None; is_aligned y 2; x && ~~ mask 6 = y && ~~ mask 6; m y = Some (KOArch (KOPTE (ARM_H.LargePagePTE x21 x22 x23 x24 x25)))\<rbrakk> \<Longrightarrow> False
 3. \<And>x y x21 x22 x23 x24 x25. \<lbrakk>x \<notin> {ptr..ptr + 2 ^ sz - 1}; m x = Some (KOArch (KOPTE (ARM_H.LargePagePTE x21 x22 x23 x24 x25))); y \<notin> {ptr..ptr + 2 ^ sz - 1}; is_aligned y 2; x && ~~ mask 6 = y && ~~ mask 6\<rbrakk> \<Longrightarrow> Some (KOArch (KOPTE (ARM_H.LargePagePTE x21 x22 x23 x24 x25))) = m y
 4. \<And>x y x2 arch_kernel_object x3. \<lbrakk>x \<notin> {ptr..ptr + 2 ^ sz - 1}; m x = Some (KOArch arch_kernel_object); x2 = KOArch arch_kernel_object; arch_kernel_object = KOPDE x3\<rbrakk> \<Longrightarrow> (y \<in> {ptr..ptr + 2 ^ sz - 1} \<longrightarrow> ((\<exists>ya. m y = Some ya) \<longrightarrow> is_aligned y 2 \<longrightarrow> x && ~~ mask (case arch_kernel_object of KOASIDPool asidpool \<Rightarrow> 0 | KOPTE (ARM_H.LargePagePTE xa xaa xb xc xd) \<Rightarrow> 6 | KOPTE _ \<Rightarrow> 0 | KOPDE (ARM_H.SuperSectionPDE xa xaa xb xc xd xe) \<Rightarrow> 6 | KOPDE _ \<Rightarrow> 0) \<noteq> y && ~~ mask (case arch_kernel_object of KOASIDPool asidpool \<Rightarrow> 0 | KOPTE (ARM_H.LargePagePTE xa xaa xb xc xd) \<Rightarrow> 6 | KOPTE _ \<Rightarrow> 0 | KOPDE (ARM_H.SuperSectionPDE xa xaa xb xc xd xe) \<Rightarrow> 6 | KOPDE _ \<Rightarrow> 0)) \<and> (m y = None \<longrightarrow> is_aligned y 2 \<longrightarrow> x && ~~ mask (case arch_kernel_object of KOASIDPool asidpool \<Rightarrow> 0 | KOPTE (ARM_H.LargePagePTE xa xaa xb xc xd) \<Rightarrow> 6 | KOPTE _ \<Rightarrow> 0 | KOPDE (ARM_H.SuperSectionPDE xa xaa xb xc xd xe) \<Rightarrow> 6 | KOPDE _ \<Rightarrow> 0) \<noteq> y && ~~ mask (case arch_kernel_object of KOASIDPool asidpool \<Rightarrow> 0 | KOPTE (ARM_H.LargePagePTE xa xaa xb xc xd) \<Rightarrow> 6 | KOPTE _ \<Rightarrow> 0 | KOPDE (ARM_H.SuperSectionPDE xa xaa xb xc xd xe) \<Rightarrow> 6 | KOPDE _ \<Rightarrow> 0))) \<and> (y \<notin> {ptr..ptr + 2 ^ sz - 1} \<longrightarrow> is_aligned y 2 \<longrightarrow> x && ~~ mask (case arch_kernel_object of KOASIDPool asidpool \<Rightarrow> 0 | KOPTE (ARM_H.LargePagePTE xa xaa xb xc xd) \<Rightarrow> 6 | KOPTE _ \<Rightarrow> 0 | KOPDE (ARM_H.SuperSectionPDE xa xaa xb xc xd xe) \<Rightarrow> 6 | KOPDE _ \<Rightarrow> 0) = y && ~~ mask (case arch_kernel_object of KOASIDPool asidpool \<Rightarrow> 0 | KOPTE (ARM_H.LargePagePTE xa xaa xb xc xd) \<Rightarrow> 6 | KOPTE _ \<Rightarrow> 0 | KOPDE (ARM_H.SuperSectionPDE xa xaa xb xc xd xe) \<Rightarrow> 6 | KOPDE _ \<Rightarrow> 0) \<longrightarrow> Some (KOArch arch_kernel_object) = m y) proof (prove)
goal (3 subgoals):
 1. \<And>x y x21 x22 x23 x24 x25. \<lbrakk>x \<notin> {ptr..ptr + 2 ^ sz - 1}; y \<in> {ptr..ptr + 2 ^ sz - 1}; m y = None; is_aligned y 2; x && ~~ mask 6 = y && ~~ mask 6; m y = Some (KOArch (KOPTE (ARM_H.LargePagePTE x21 x22 x23 x24 x25)))\<rbrakk> \<Longrightarrow> False
 2. \<And>x y x21 x22 x23 x24 x25. \<lbrakk>x \<notin> {ptr..ptr + 2 ^ sz - 1}; m x = Some (KOArch (KOPTE (ARM_H.LargePagePTE x21 x22 x23 x24 x25))); y \<notin> {ptr..ptr + 2 ^ sz - 1}; is_aligned y 2; x && ~~ mask 6 = y && ~~ mask 6\<rbrakk> \<Longrightarrow> Some (KOArch (KOPTE (ARM_H.LargePagePTE x21 x22 x23 x24 x25))) = m y
 3. \<And>x y x2 arch_kernel_object x3. \<lbrakk>x \<notin> {ptr..ptr + 2 ^ sz - 1}; m x = Some (KOArch arch_kernel_object); x2 = KOArch arch_kernel_object; arch_kernel_object = KOPDE x3\<rbrakk> \<Longrightarrow> (y \<in> {ptr..ptr + 2 ^ sz - 1} \<longrightarrow> ((\<exists>ya. m y = Some ya) \<longrightarrow> is_aligned y 2 \<longrightarrow> x && ~~ mask (case arch_kernel_object of KOASIDPool asidpool \<Rightarrow> 0 | KOPTE (ARM_H.LargePagePTE xa xaa xb xc xd) \<Rightarrow> 6 | KOPTE _ \<Rightarrow> 0 | KOPDE (ARM_H.SuperSectionPDE xa xaa xb xc xd xe) \<Rightarrow> 6 | KOPDE _ \<Rightarrow> 0) \<noteq> y && ~~ mask (case arch_kernel_object of KOASIDPool asidpool \<Rightarrow> 0 | KOPTE (ARM_H.LargePagePTE xa xaa xb xc xd) \<Rightarrow> 6 | KOPTE _ \<Rightarrow> 0 | KOPDE (ARM_H.SuperSectionPDE xa xaa xb xc xd xe) \<Rightarrow> 6 | KOPDE _ \<Rightarrow> 0)) \<and> (m y = None \<longrightarrow> is_aligned y 2 \<longrightarrow> x && ~~ mask (case arch_kernel_object of KOASIDPool asidpool \<Rightarrow> 0 | KOPTE (ARM_H.LargePagePTE xa xaa xb xc xd) \<Rightarrow> 6 | KOPTE _ \<Rightarrow> 0 | KOPDE (ARM_H.SuperSectionPDE xa xaa xb xc xd xe) \<Rightarrow> 6 | KOPDE _ \<Rightarrow> 0) \<noteq> y && ~~ mask (case arch_kernel_object of KOASIDPool asidpool \<Rightarrow> 0 | KOPTE (ARM_H.LargePagePTE xa xaa xb xc xd) \<Rightarrow> 6 | KOPTE _ \<Rightarrow> 0 | KOPDE (ARM_H.SuperSectionPDE xa xaa xb xc xd xe) \<Rightarrow> 6 | KOPDE _ \<Rightarrow> 0))) \<and> (y \<notin> {ptr..ptr + 2 ^ sz - 1} \<longrightarrow> is_aligned y 2 \<longrightarrow> x && ~~ mask (case arch_kernel_object of KOASIDPool asidpool \<Rightarrow> 0 | KOPTE (ARM_H.LargePagePTE xa xaa xb xc xd) \<Rightarrow> 6 | KOPTE _ \<Rightarrow> 0 | KOPDE (ARM_H.SuperSectionPDE xa xaa xb xc xd xe) \<Rightarrow> 6 | KOPDE _ \<Rightarrow> 0) = y && ~~ mask (case arch_kernel_object of KOASIDPool asidpool \<Rightarrow> 0 | KOPTE (ARM_H.LargePagePTE xa xaa xb xc xd) \<Rightarrow> 6 | KOPTE _ \<Rightarrow> 0 | KOPDE (ARM_H.SuperSectionPDE xa xaa xb xc xd xe) \<Rightarrow> 6 | KOPDE _ \<Rightarrow> 0) \<longrightarrow> Some (KOArch arch_kernel_object) = m y) proof (prove)
goal (2 subgoals):
 1. \<And>x y x21 x22 x23 x24 x25. \<lbrakk>x \<notin> {ptr..ptr + 2 ^ sz - 1}; m x = Some (KOArch (KOPTE (ARM_H.LargePagePTE x21 x22 x23 x24 x25))); y \<notin> {ptr..ptr + 2 ^ sz - 1}; is_aligned y 2; x && ~~ mask 6 = y && ~~ mask 6\<rbrakk> \<Longrightarrow> Some (KOArch (KOPTE (ARM_H.LargePagePTE x21 x22 x23 x24 x25))) = m y
 2. \<And>x y x2 arch_kernel_object x3. \<lbrakk>x \<notin> {ptr..ptr + 2 ^ sz - 1}; m x = Some (KOArch arch_kernel_object); x2 = KOArch arch_kernel_object; arch_kernel_object = KOPDE x3\<rbrakk> \<Longrightarrow> (y \<in> {ptr..ptr + 2 ^ sz - 1} \<longrightarrow> ((\<exists>ya. m y = Some ya) \<longrightarrow> is_aligned y 2 \<longrightarrow> x && ~~ mask (case arch_kernel_object of KOASIDPool asidpool \<Rightarrow> 0 | KOPTE (ARM_H.LargePagePTE xa xaa xb xc xd) \<Rightarrow> 6 | KOPTE _ \<Rightarrow> 0 | KOPDE (ARM_H.SuperSectionPDE xa xaa xb xc xd xe) \<Rightarrow> 6 | KOPDE _ \<Rightarrow> 0) \<noteq> y && ~~ mask (case arch_kernel_object of KOASIDPool asidpool \<Rightarrow> 0 | KOPTE (ARM_H.LargePagePTE xa xaa xb xc xd) \<Rightarrow> 6 | KOPTE _ \<Rightarrow> 0 | KOPDE (ARM_H.SuperSectionPDE xa xaa xb xc xd xe) \<Rightarrow> 6 | KOPDE _ \<Rightarrow> 0)) \<and> (m y = None \<longrightarrow> is_aligned y 2 \<longrightarrow> x && ~~ mask (case arch_kernel_object of KOASIDPool asidpool \<Rightarrow> 0 | KOPTE (ARM_H.LargePagePTE xa xaa xb xc xd) \<Rightarrow> 6 | KOPTE _ \<Rightarrow> 0 | KOPDE (ARM_H.SuperSectionPDE xa xaa xb xc xd xe) \<Rightarrow> 6 | KOPDE _ \<Rightarrow> 0) \<noteq> y && ~~ mask (case arch_kernel_object of KOASIDPool asidpool \<Rightarrow> 0 | KOPTE (ARM_H.LargePagePTE xa xaa xb xc xd) \<Rightarrow> 6 | KOPTE _ \<Rightarrow> 0 | KOPDE (ARM_H.SuperSectionPDE xa xaa xb xc xd xe) \<Rightarrow> 6 | KOPDE _ \<Rightarrow> 0))) \<and> (y \<notin> {ptr..ptr + 2 ^ sz - 1} \<longrightarrow> is_aligned y 2 \<longrightarrow> x && ~~ mask (case arch_kernel_object of KOASIDPool asidpool \<Rightarrow> 0 | KOPTE (ARM_H.LargePagePTE xa xaa xb xc xd) \<Rightarrow> 6 | KOPTE _ \<Rightarrow> 0 | KOPDE (ARM_H.SuperSectionPDE xa xaa xb xc xd xe) \<Rightarrow> 6 | KOPDE _ \<Rightarrow> 0) = y && ~~ mask (case arch_kernel_object of KOASIDPool asidpool \<Rightarrow> 0 | KOPTE (ARM_H.LargePagePTE xa xaa xb xc xd) \<Rightarrow> 6 | KOPTE _ \<Rightarrow> 0 | KOPDE (ARM_H.SuperSectionPDE xa xaa xb xc xd xe) \<Rightarrow> 6 | KOPDE _ \<Rightarrow> 0) \<longrightarrow> Some (KOArch arch_kernel_object) = m y) proof (prove)
goal (4 subgoals):
 1. \<And>x y x21 x22 x23 x24 x25. \<lbrakk>x \<notin> {ptr..ptr + 2 ^ sz - 1}; y \<notin> {ptr..ptr + 2 ^ sz - 1}; is_aligned y 2; x && ~~ mask 6 = y && ~~ mask 6\<rbrakk> \<Longrightarrow> is_aligned y 2
 2. \<And>x y x21 x22 x23 x24 x25. \<lbrakk>x \<notin> {ptr..ptr + 2 ^ sz - 1}; y \<notin> {ptr..ptr + 2 ^ sz - 1}; is_aligned y 2; x && ~~ mask 6 = y && ~~ mask 6\<rbrakk> \<Longrightarrow> x && ~~ mask (vs_ptr_align (KOArch (KOPTE (ARM_H.LargePagePTE x21 x22 x23 x24 x25)))) = y && ~~ mask (vs_ptr_align (KOArch (KOPTE (ARM_H.LargePagePTE x21 x22 x23 x24 x25))))
 3. \<And>x y x21 x22 x23 x24 x25. \<lbrakk>x \<notin> {ptr..ptr + 2 ^ sz - 1}; y \<notin> {ptr..ptr + 2 ^ sz - 1}; is_aligned y 2; x && ~~ mask 6 = y && ~~ mask 6; m y = Some (KOArch (KOPTE (ARM_H.LargePagePTE x21 x22 x23 x24 x25)))\<rbrakk> \<Longrightarrow> Some (KOArch (KOPTE (ARM_H.LargePagePTE x21 x22 x23 x24 x25))) = m y
 4. \<And>x y x2 arch_kernel_object x3. \<lbrakk>x \<notin> {ptr..ptr + 2 ^ sz - 1}; m x = Some (KOArch arch_kernel_object); x2 = KOArch arch_kernel_object; arch_kernel_object = KOPDE x3\<rbrakk> \<Longrightarrow> (y \<in> {ptr..ptr + 2 ^ sz - 1} \<longrightarrow> ((\<exists>ya. m y = Some ya) \<longrightarrow> is_aligned y 2 \<longrightarrow> x && ~~ mask (case arch_kernel_object of KOASIDPool asidpool \<Rightarrow> 0 | KOPTE (ARM_H.LargePagePTE xa xaa xb xc xd) \<Rightarrow> 6 | KOPTE _ \<Rightarrow> 0 | KOPDE (ARM_H.SuperSectionPDE xa xaa xb xc xd xe) \<Rightarrow> 6 | KOPDE _ \<Rightarrow> 0) \<noteq> y && ~~ mask (case arch_kernel_object of KOASIDPool asidpool \<Rightarrow> 0 | KOPTE (ARM_H.LargePagePTE xa xaa xb xc xd) \<Rightarrow> 6 | KOPTE _ \<Rightarrow> 0 | KOPDE (ARM_H.SuperSectionPDE xa xaa xb xc xd xe) \<Rightarrow> 6 | KOPDE _ \<Rightarrow> 0)) \<and> (m y = None \<longrightarrow> is_aligned y 2 \<longrightarrow> x && ~~ mask (case arch_kernel_object of KOASIDPool asidpool \<Rightarrow> 0 | KOPTE (ARM_H.LargePagePTE xa xaa xb xc xd) \<Rightarrow> 6 | KOPTE _ \<Rightarrow> 0 | KOPDE (ARM_H.SuperSectionPDE xa xaa xb xc xd xe) \<Rightarrow> 6 | KOPDE _ \<Rightarrow> 0) \<noteq> y && ~~ mask (case arch_kernel_object of KOASIDPool asidpool \<Rightarrow> 0 | KOPTE (ARM_H.LargePagePTE xa xaa xb xc xd) \<Rightarrow> 6 | KOPTE _ \<Rightarrow> 0 | KOPDE (ARM_H.SuperSectionPDE xa xaa xb xc xd xe) \<Rightarrow> 6 | KOPDE _ \<Rightarrow> 0))) \<and> (y \<notin> {ptr..ptr + 2 ^ sz - 1} \<longrightarrow> is_aligned y 2 \<longrightarrow> x && ~~ mask (case arch_kernel_object of KOASIDPool asidpool \<Rightarrow> 0 | KOPTE (ARM_H.LargePagePTE xa xaa xb xc xd) \<Rightarrow> 6 | KOPTE _ \<Rightarrow> 0 | KOPDE (ARM_H.SuperSectionPDE xa xaa xb xc xd xe) \<Rightarrow> 6 | KOPDE _ \<Rightarrow> 0) = y && ~~ mask (case arch_kernel_object of KOASIDPool asidpool \<Rightarrow> 0 | KOPTE (ARM_H.LargePagePTE xa xaa xb xc xd) \<Rightarrow> 6 | KOPTE _ \<Rightarrow> 0 | KOPDE (ARM_H.SuperSectionPDE xa xaa xb xc xd xe) \<Rightarrow> 6 | KOPDE _ \<Rightarrow> 0) \<longrightarrow> Some (KOArch arch_kernel_object) = m y) proof (prove)
goal (3 subgoals):
 1. \<And>x y x21 x22 x23 x24 x25. \<lbrakk>x \<notin> {ptr..ptr + 2 ^ sz - 1}; y \<notin> {ptr..ptr + 2 ^ sz - 1}; is_aligned y 2; x && ~~ mask 6 = y && ~~ mask 6\<rbrakk> \<Longrightarrow> x && ~~ mask (vs_ptr_align (KOArch (KOPTE (ARM_H.LargePagePTE x21 x22 x23 x24 x25)))) = y && ~~ mask (vs_ptr_align (KOArch (KOPTE (ARM_H.LargePagePTE x21 x22 x23 x24 x25))))
 2. \<And>x y x21 x22 x23 x24 x25. \<lbrakk>x \<notin> {ptr..ptr + 2 ^ sz - 1}; y \<notin> {ptr..ptr + 2 ^ sz - 1}; is_aligned y 2; x && ~~ mask 6 = y && ~~ mask 6; m y = Some (KOArch (KOPTE (ARM_H.LargePagePTE x21 x22 x23 x24 x25)))\<rbrakk> \<Longrightarrow> Some (KOArch (KOPTE (ARM_H.LargePagePTE x21 x22 x23 x24 x25))) = m y
 3. \<And>x y x2 arch_kernel_object x3. \<lbrakk>x \<notin> {ptr..ptr + 2 ^ sz - 1}; m x = Some (KOArch arch_kernel_object); x2 = KOArch arch_kernel_object; arch_kernel_object = KOPDE x3\<rbrakk> \<Longrightarrow> (y \<in> {ptr..ptr + 2 ^ sz - 1} \<longrightarrow> ((\<exists>ya. m y = Some ya) \<longrightarrow> is_aligned y 2 \<longrightarrow> x && ~~ mask (case arch_kernel_object of KOASIDPool asidpool \<Rightarrow> 0 | KOPTE (ARM_H.LargePagePTE xa xaa xb xc xd) \<Rightarrow> 6 | KOPTE _ \<Rightarrow> 0 | KOPDE (ARM_H.SuperSectionPDE xa xaa xb xc xd xe) \<Rightarrow> 6 | KOPDE _ \<Rightarrow> 0) \<noteq> y && ~~ mask (case arch_kernel_object of KOASIDPool asidpool \<Rightarrow> 0 | KOPTE (ARM_H.LargePagePTE xa xaa xb xc xd) \<Rightarrow> 6 | KOPTE _ \<Rightarrow> 0 | KOPDE (ARM_H.SuperSectionPDE xa xaa xb xc xd xe) \<Rightarrow> 6 | KOPDE _ \<Rightarrow> 0)) \<and> (m y = None \<longrightarrow> is_aligned y 2 \<longrightarrow> x && ~~ mask (case arch_kernel_object of KOASIDPool asidpool \<Rightarrow> 0 | KOPTE (ARM_H.LargePagePTE xa xaa xb xc xd) \<Rightarrow> 6 | KOPTE _ \<Rightarrow> 0 | KOPDE (ARM_H.SuperSectionPDE xa xaa xb xc xd xe) \<Rightarrow> 6 | KOPDE _ \<Rightarrow> 0) \<noteq> y && ~~ mask (case arch_kernel_object of KOASIDPool asidpool \<Rightarrow> 0 | KOPTE (ARM_H.LargePagePTE xa xaa xb xc xd) \<Rightarrow> 6 | KOPTE _ \<Rightarrow> 0 | KOPDE (ARM_H.SuperSectionPDE xa xaa xb xc xd xe) \<Rightarrow> 6 | KOPDE _ \<Rightarrow> 0))) \<and> (y \<notin> {ptr..ptr + 2 ^ sz - 1} \<longrightarrow> is_aligned y 2 \<longrightarrow> x && ~~ mask (case arch_kernel_object of KOASIDPool asidpool \<Rightarrow> 0 | KOPTE (ARM_H.LargePagePTE xa xaa xb xc xd) \<Rightarrow> 6 | KOPTE _ \<Rightarrow> 0 | KOPDE (ARM_H.SuperSectionPDE xa xaa xb xc xd xe) \<Rightarrow> 6 | KOPDE _ \<Rightarrow> 0) = y && ~~ mask (case arch_kernel_object of KOASIDPool asidpool \<Rightarrow> 0 | KOPTE (ARM_H.LargePagePTE xa xaa xb xc xd) \<Rightarrow> 6 | KOPTE _ \<Rightarrow> 0 | KOPDE (ARM_H.SuperSectionPDE xa xaa xb xc xd xe) \<Rightarrow> 6 | KOPDE _ \<Rightarrow> 0) \<longrightarrow> Some (KOArch arch_kernel_object) = m y) proof (prove)
goal (2 subgoals):
 1. \<And>x y x21 x22 x23 x24 x25. \<lbrakk>x \<notin> {ptr..ptr + 2 ^ sz - 1}; y \<notin> {ptr..ptr + 2 ^ sz - 1}; is_aligned y 2; x && ~~ mask 6 = y && ~~ mask 6; m y = Some (KOArch (KOPTE (ARM_H.LargePagePTE x21 x22 x23 x24 x25)))\<rbrakk> \<Longrightarrow> Some (KOArch (KOPTE (ARM_H.LargePagePTE x21 x22 x23 x24 x25))) = m y
 2. \<And>x y x2 arch_kernel_object x3. \<lbrakk>x \<notin> {ptr..ptr + 2 ^ sz - 1}; m x = Some (KOArch arch_kernel_object); x2 = KOArch arch_kernel_object; arch_kernel_object = KOPDE x3\<rbrakk> \<Longrightarrow> (y \<in> {ptr..ptr + 2 ^ sz - 1} \<longrightarrow> ((\<exists>ya. m y = Some ya) \<longrightarrow> is_aligned y 2 \<longrightarrow> x && ~~ mask (case arch_kernel_object of KOASIDPool asidpool \<Rightarrow> 0 | KOPTE (ARM_H.LargePagePTE xa xaa xb xc xd) \<Rightarrow> 6 | KOPTE _ \<Rightarrow> 0 | KOPDE (ARM_H.SuperSectionPDE xa xaa xb xc xd xe) \<Rightarrow> 6 | KOPDE _ \<Rightarrow> 0) \<noteq> y && ~~ mask (case arch_kernel_object of KOASIDPool asidpool \<Rightarrow> 0 | KOPTE (ARM_H.LargePagePTE xa xaa xb xc xd) \<Rightarrow> 6 | KOPTE _ \<Rightarrow> 0 | KOPDE (ARM_H.SuperSectionPDE xa xaa xb xc xd xe) \<Rightarrow> 6 | KOPDE _ \<Rightarrow> 0)) \<and> (m y = None \<longrightarrow> is_aligned y 2 \<longrightarrow> x && ~~ mask (case arch_kernel_object of KOASIDPool asidpool \<Rightarrow> 0 | KOPTE (ARM_H.LargePagePTE xa xaa xb xc xd) \<Rightarrow> 6 | KOPTE _ \<Rightarrow> 0 | KOPDE (ARM_H.SuperSectionPDE xa xaa xb xc xd xe) \<Rightarrow> 6 | KOPDE _ \<Rightarrow> 0) \<noteq> y && ~~ mask (case arch_kernel_object of KOASIDPool asidpool \<Rightarrow> 0 | KOPTE (ARM_H.LargePagePTE xa xaa xb xc xd) \<Rightarrow> 6 | KOPTE _ \<Rightarrow> 0 | KOPDE (ARM_H.SuperSectionPDE xa xaa xb xc xd xe) \<Rightarrow> 6 | KOPDE _ \<Rightarrow> 0))) \<and> (y \<notin> {ptr..ptr + 2 ^ sz - 1} \<longrightarrow> is_aligned y 2 \<longrightarrow> x && ~~ mask (case arch_kernel_object of KOASIDPool asidpool \<Rightarrow> 0 | KOPTE (ARM_H.LargePagePTE xa xaa xb xc xd) \<Rightarrow> 6 | KOPTE _ \<Rightarrow> 0 | KOPDE (ARM_H.SuperSectionPDE xa xaa xb xc xd xe) \<Rightarrow> 6 | KOPDE _ \<Rightarrow> 0) = y && ~~ mask (case arch_kernel_object of KOASIDPool asidpool \<Rightarrow> 0 | KOPTE (ARM_H.LargePagePTE xa xaa xb xc xd) \<Rightarrow> 6 | KOPTE _ \<Rightarrow> 0 | KOPDE (ARM_H.SuperSectionPDE xa xaa xb xc xd xe) \<Rightarrow> 6 | KOPDE _ \<Rightarrow> 0) \<longrightarrow> Some (KOArch arch_kernel_object) = m y) proof (prove)
goal (1 subgoal):
 1. \<And>x y x2 arch_kernel_object x3. \<lbrakk>x \<notin> {ptr..ptr + 2 ^ sz - 1}; m x = Some (KOArch arch_kernel_object); x2 = KOArch arch_kernel_object; arch_kernel_object = KOPDE x3\<rbrakk> \<Longrightarrow> (y \<in> {ptr..ptr + 2 ^ sz - 1} \<longrightarrow> ((\<exists>ya. m y = Some ya) \<longrightarrow> is_aligned y 2 \<longrightarrow> x && ~~ mask (case arch_kernel_object of KOASIDPool asidpool \<Rightarrow> 0 | KOPTE (ARM_H.LargePagePTE xa xaa xb xc xd) \<Rightarrow> 6 | KOPTE _ \<Rightarrow> 0 | KOPDE (ARM_H.SuperSectionPDE xa xaa xb xc xd xe) \<Rightarrow> 6 | KOPDE _ \<Rightarrow> 0) \<noteq> y && ~~ mask (case arch_kernel_object of KOASIDPool asidpool \<Rightarrow> 0 | KOPTE (ARM_H.LargePagePTE xa xaa xb xc xd) \<Rightarrow> 6 | KOPTE _ \<Rightarrow> 0 | KOPDE (ARM_H.SuperSectionPDE xa xaa xb xc xd xe) \<Rightarrow> 6 | KOPDE _ \<Rightarrow> 0)) \<and> (m y = None \<longrightarrow> is_aligned y 2 \<longrightarrow> x && ~~ mask (case arch_kernel_object of KOASIDPool asidpool \<Rightarrow> 0 | KOPTE (ARM_H.LargePagePTE xa xaa xb xc xd) \<Rightarrow> 6 | KOPTE _ \<Rightarrow> 0 | KOPDE (ARM_H.SuperSectionPDE xa xaa xb xc xd xe) \<Rightarrow> 6 | KOPDE _ \<Rightarrow> 0) \<noteq> y && ~~ mask (case arch_kernel_object of KOASIDPool asidpool \<Rightarrow> 0 | KOPTE (ARM_H.LargePagePTE xa xaa xb xc xd) \<Rightarrow> 6 | KOPTE _ \<Rightarrow> 0 | KOPDE (ARM_H.SuperSectionPDE xa xaa xb xc xd xe) \<Rightarrow> 6 | KOPDE _ \<Rightarrow> 0))) \<and> (y \<notin> {ptr..ptr + 2 ^ sz - 1} \<longrightarrow> is_aligned y 2 \<longrightarrow> x && ~~ mask (case arch_kernel_object of KOASIDPool asidpool \<Rightarrow> 0 | KOPTE (ARM_H.LargePagePTE xa xaa xb xc xd) \<Rightarrow> 6 | KOPTE _ \<Rightarrow> 0 | KOPDE (ARM_H.SuperSectionPDE xa xaa xb xc xd xe) \<Rightarrow> 6 | KOPDE _ \<Rightarrow> 0) = y && ~~ mask (case arch_kernel_object of KOASIDPool asidpool \<Rightarrow> 0 | KOPTE (ARM_H.LargePagePTE xa xaa xb xc xd) \<Rightarrow> 6 | KOPTE _ \<Rightarrow> 0 | KOPDE (ARM_H.SuperSectionPDE xa xaa xb xc xd xe) \<Rightarrow> 6 | KOPDE _ \<Rightarrow> 0) \<longrightarrow> Some (KOArch arch_kernel_object) = m y) proof (prove)
goal (1 subgoal):
 1. \<And>x y x3. \<lbrakk>x \<notin> {ptr..ptr + 2 ^ sz - 1}; m x = Some (KOArch (KOPDE x3))\<rbrakk> \<Longrightarrow> (x3 = ARM_H.InvalidPDE \<longrightarrow> (y \<in> {ptr..ptr + 2 ^ sz - 1} \<longrightarrow> ((\<exists>ya. m y = Some ya) \<longrightarrow> is_aligned y 2 \<longrightarrow> x \<noteq> y) \<and> (m y = None \<longrightarrow> is_aligned y 2 \<longrightarrow> x \<noteq> y)) \<and> (y \<notin> {ptr..ptr + 2 ^ sz - 1} \<longrightarrow> is_aligned y 2 \<longrightarrow> x = y \<longrightarrow> Some (KOArch (KOPDE ARM_H.InvalidPDE)) = m y)) \<and> (\<forall>x21 x22 x23. x3 = ARM_H.PageTablePDE x21 x22 x23 \<longrightarrow> (y \<in> {ptr..ptr + 2 ^ sz - 1} \<longrightarrow> ((\<exists>ya. m y = Some ya) \<longrightarrow> is_aligned y 2 \<longrightarrow> x \<noteq> y) \<and> (m y = None \<longrightarrow> is_aligned y 2 \<longrightarrow> x \<noteq> y)) \<and> (y \<notin> {ptr..ptr + 2 ^ sz - 1} \<longrightarrow> is_aligned y 2 \<longrightarrow> x = y \<longrightarrow> Some (KOArch (KOPDE (ARM_H.PageTablePDE x21 x22 x23))) = m y)) \<and> (\<forall>x31 x32 x33 x34 x35 x36 x37. x3 = ARM_H.SectionPDE x31 x32 x33 x34 x35 x36 x37 \<longrightarrow> (y \<in> {ptr..ptr + 2 ^ sz - 1} \<longrightarrow> ((\<exists>ya. m y = Some ya) \<longrightarrow> is_aligned y 2 \<longrightarrow> x \<noteq> y) \<and> (m y = None \<longrightarrow> is_aligned y 2 \<longrightarrow> x \<noteq> y)) \<and> (y \<notin> {ptr..ptr + 2 ^ sz - 1} \<longrightarrow> is_aligned y 2 \<longrightarrow> x = y \<longrightarrow> Some (KOArch (KOPDE (ARM_H.SectionPDE x31 x32 x33 x34 x35 x36 x37))) = m y)) \<and> (\<forall>x41 x42 x43 x44 x45 x46. x3 = ARM_H.SuperSectionPDE x41 x42 x43 x44 x45 x46 \<longrightarrow> (y \<in> {ptr..ptr + 2 ^ sz - 1} \<longrightarrow> ((\<exists>ya. m y = Some ya) \<longrightarrow> is_aligned y 2 \<longrightarrow> x && ~~ mask 6 \<noteq> y && ~~ mask 6) \<and> (m y = None \<longrightarrow> is_aligned y 2 \<longrightarrow> x && ~~ mask 6 \<noteq> y && ~~ mask 6)) \<and> (y \<notin> {ptr..ptr + 2 ^ sz - 1} \<longrightarrow> is_aligned y 2 \<longrightarrow> x && ~~ mask 6 = y && ~~ mask 6 \<longrightarrow> Some (KOArch (KOPDE (ARM_H.SuperSectionPDE x41 x42 x43 x44 x45 x46))) = m y)) proof (prove)
goal (3 subgoals):
 1. \<And>x y x41 x42 x43 x44 x45 x46 ya. \<lbrakk>x \<notin> {ptr..ptr + 2 ^ sz - 1}; m x = Some (KOArch (KOPDE (ARM_H.SuperSectionPDE x41 x42 x43 x44 x45 x46))); y \<in> {ptr..ptr + 2 ^ sz - 1}; m y = Some ya; is_aligned y 2; x && ~~ mask 6 = y && ~~ mask 6\<rbrakk> \<Longrightarrow> False
 2. \<And>x y x41 x42 x43 x44 x45 x46. \<lbrakk>x \<notin> {ptr..ptr + 2 ^ sz - 1}; m x = Some (KOArch (KOPDE (ARM_H.SuperSectionPDE x41 x42 x43 x44 x45 x46))); y \<in> {ptr..ptr + 2 ^ sz - 1}; m y = None; is_aligned y 2; x && ~~ mask 6 = y && ~~ mask 6\<rbrakk> \<Longrightarrow> False
 3. \<And>x y x41 x42 x43 x44 x45 x46. \<lbrakk>x \<notin> {ptr..ptr + 2 ^ sz - 1}; m x = Some (KOArch (KOPDE (ARM_H.SuperSectionPDE x41 x42 x43 x44 x45 x46))); y \<notin> {ptr..ptr + 2 ^ sz - 1}; is_aligned y 2; x && ~~ mask 6 = y && ~~ mask 6\<rbrakk> \<Longrightarrow> Some (KOArch (KOPDE (ARM_H.SuperSectionPDE x41 x42 x43 x44 x45 x46))) = m y proof (prove)
goal (5 subgoals):
 1. \<And>x y x41 x42 x43 x44 x45 x46 ya. \<lbrakk>x \<notin> {ptr..ptr + 2 ^ sz - 1}; y \<in> {ptr..ptr + 2 ^ sz - 1}; m y = Some ya; is_aligned y 2; x && ~~ mask 6 = y && ~~ mask 6\<rbrakk> \<Longrightarrow> is_aligned y 2
 2. \<And>x y x41 x42 x43 x44 x45 x46 ya. \<lbrakk>x \<notin> {ptr..ptr + 2 ^ sz - 1}; y \<in> {ptr..ptr + 2 ^ sz - 1}; m y = Some ya; is_aligned y 2; x && ~~ mask 6 = y && ~~ mask 6\<rbrakk> \<Longrightarrow> x && ~~ mask (vs_ptr_align (KOArch (KOPDE (ARM_H.SuperSectionPDE x41 x42 x43 x44 x45 x46)))) = y && ~~ mask (vs_ptr_align (KOArch (KOPDE (ARM_H.SuperSectionPDE x41 x42 x43 x44 x45 x46))))
 3. \<And>x y x41 x42 x43 x44 x45 x46 ya. \<lbrakk>x \<notin> {ptr..ptr + 2 ^ sz - 1}; y \<in> {ptr..ptr + 2 ^ sz - 1}; m y = Some ya; is_aligned y 2; x && ~~ mask 6 = y && ~~ mask 6; m y = Some (KOArch (KOPDE (ARM_H.SuperSectionPDE x41 x42 x43 x44 x45 x46)))\<rbrakk> \<Longrightarrow> False
 4. \<And>x y x41 x42 x43 x44 x45 x46. \<lbrakk>x \<notin> {ptr..ptr + 2 ^ sz - 1}; m x = Some (KOArch (KOPDE (ARM_H.SuperSectionPDE x41 x42 x43 x44 x45 x46))); y \<in> {ptr..ptr + 2 ^ sz - 1}; m y = None; is_aligned y 2; x && ~~ mask 6 = y && ~~ mask 6\<rbrakk> \<Longrightarrow> False
 5. \<And>x y x41 x42 x43 x44 x45 x46. \<lbrakk>x \<notin> {ptr..ptr + 2 ^ sz - 1}; m x = Some (KOArch (KOPDE (ARM_H.SuperSectionPDE x41 x42 x43 x44 x45 x46))); y \<notin> {ptr..ptr + 2 ^ sz - 1}; is_aligned y 2; x && ~~ mask 6 = y && ~~ mask 6\<rbrakk> \<Longrightarrow> Some (KOArch (KOPDE (ARM_H.SuperSectionPDE x41 x42 x43 x44 x45 x46))) = m y proof (prove)
goal (4 subgoals):
 1. \<And>x y x41 x42 x43 x44 x45 x46 ya. \<lbrakk>x \<notin> {ptr..ptr + 2 ^ sz - 1}; y \<in> {ptr..ptr + 2 ^ sz - 1}; m y = Some ya; is_aligned y 2; x && ~~ mask 6 = y && ~~ mask 6\<rbrakk> \<Longrightarrow> x && ~~ mask (vs_ptr_align (KOArch (KOPDE (ARM_H.SuperSectionPDE x41 x42 x43 x44 x45 x46)))) = y && ~~ mask (vs_ptr_align (KOArch (KOPDE (ARM_H.SuperSectionPDE x41 x42 x43 x44 x45 x46))))
 2. \<And>x y x41 x42 x43 x44 x45 x46 ya. \<lbrakk>x \<notin> {ptr..ptr + 2 ^ sz - 1}; y \<in> {ptr..ptr + 2 ^ sz - 1}; m y = Some ya; is_aligned y 2; x && ~~ mask 6 = y && ~~ mask 6; m y = Some (KOArch (KOPDE (ARM_H.SuperSectionPDE x41 x42 x43 x44 x45 x46)))\<rbrakk> \<Longrightarrow> False
 3. \<And>x y x41 x42 x43 x44 x45 x46. \<lbrakk>x \<notin> {ptr..ptr + 2 ^ sz - 1}; m x = Some (KOArch (KOPDE (ARM_H.SuperSectionPDE x41 x42 x43 x44 x45 x46))); y \<in> {ptr..ptr + 2 ^ sz - 1}; m y = None; is_aligned y 2; x && ~~ mask 6 = y && ~~ mask 6\<rbrakk> \<Longrightarrow> False
 4. \<And>x y x41 x42 x43 x44 x45 x46. \<lbrakk>x \<notin> {ptr..ptr + 2 ^ sz - 1}; m x = Some (KOArch (KOPDE (ARM_H.SuperSectionPDE x41 x42 x43 x44 x45 x46))); y \<notin> {ptr..ptr + 2 ^ sz - 1}; is_aligned y 2; x && ~~ mask 6 = y && ~~ mask 6\<rbrakk> \<Longrightarrow> Some (KOArch (KOPDE (ARM_H.SuperSectionPDE x41 x42 x43 x44 x45 x46))) = m y proof (prove)
goal (3 subgoals):
 1. \<And>x y x41 x42 x43 x44 x45 x46 ya. \<lbrakk>x \<notin> {ptr..ptr + 2 ^ sz - 1}; y \<in> {ptr..ptr + 2 ^ sz - 1}; m y = Some ya; is_aligned y 2; x && ~~ mask 6 = y && ~~ mask 6; m y = Some (KOArch (KOPDE (ARM_H.SuperSectionPDE x41 x42 x43 x44 x45 x46)))\<rbrakk> \<Longrightarrow> False
 2. \<And>x y x41 x42 x43 x44 x45 x46. \<lbrakk>x \<notin> {ptr..ptr + 2 ^ sz - 1}; m x = Some (KOArch (KOPDE (ARM_H.SuperSectionPDE x41 x42 x43 x44 x45 x46))); y \<in> {ptr..ptr + 2 ^ sz - 1}; m y = None; is_aligned y 2; x && ~~ mask 6 = y && ~~ mask 6\<rbrakk> \<Longrightarrow> False
 3. \<And>x y x41 x42 x43 x44 x45 x46. \<lbrakk>x \<notin> {ptr..ptr + 2 ^ sz - 1}; m x = Some (KOArch (KOPDE (ARM_H.SuperSectionPDE x41 x42 x43 x44 x45 x46))); y \<notin> {ptr..ptr + 2 ^ sz - 1}; is_aligned y 2; x && ~~ mask 6 = y && ~~ mask 6\<rbrakk> \<Longrightarrow> Some (KOArch (KOPDE (ARM_H.SuperSectionPDE x41 x42 x43 x44 x45 x46))) = m y proof (prove)
goal (3 subgoals):
 1. \<And>x y x41 x42 x43 x44 x45 x46 ya. \<lbrakk>x \<notin> {ptr..ptr + 2 ^ sz - 1}; y \<in> {ptr..ptr + 2 ^ sz - 1}; m y = Some ya; is_aligned y 2; x && ~~ mask 6 = y && ~~ mask 6; 6 \<le> sz\<rbrakk> \<Longrightarrow> False
 2. \<And>x y x41 x42 x43 x44 x45 x46. \<lbrakk>x \<notin> {ptr..ptr + 2 ^ sz - 1}; m x = Some (KOArch (KOPDE (ARM_H.SuperSectionPDE x41 x42 x43 x44 x45 x46))); y \<in> {ptr..ptr + 2 ^ sz - 1}; m y = None; is_aligned y 2; x && ~~ mask 6 = y && ~~ mask 6\<rbrakk> \<Longrightarrow> False
 3. \<And>x y x41 x42 x43 x44 x45 x46. \<lbrakk>x \<notin> {ptr..ptr + 2 ^ sz - 1}; m x = Some (KOArch (KOPDE (ARM_H.SuperSectionPDE x41 x42 x43 x44 x45 x46))); y \<notin> {ptr..ptr + 2 ^ sz - 1}; is_aligned y 2; x && ~~ mask 6 = y && ~~ mask 6\<rbrakk> \<Longrightarrow> Some (KOArch (KOPDE (ARM_H.SuperSectionPDE x41 x42 x43 x44 x45 x46))) = m y proof (prove)
goal (3 subgoals):
 1. \<And>x y x41 x42 x43 x44 x45 x46 ya. \<lbrakk>x \<notin> {ptr..ptr + 2 ^ sz - 1}; y \<in> {ptr..ptr + 2 ^ sz - 1}; m y = Some ya; is_aligned y 2; 6 \<le> sz; x && ~~ mask sz = (y && ~~ mask 6) && ~~ mask sz\<rbrakk> \<Longrightarrow> False
 2. \<And>x y x41 x42 x43 x44 x45 x46. \<lbrakk>x \<notin> {ptr..ptr + 2 ^ sz - 1}; m x = Some (KOArch (KOPDE (ARM_H.SuperSectionPDE x41 x42 x43 x44 x45 x46))); y \<in> {ptr..ptr + 2 ^ sz - 1}; m y = None; is_aligned y 2; x && ~~ mask 6 = y && ~~ mask 6\<rbrakk> \<Longrightarrow> False
 3. \<And>x y x41 x42 x43 x44 x45 x46. \<lbrakk>x \<notin> {ptr..ptr + 2 ^ sz - 1}; m x = Some (KOArch (KOPDE (ARM_H.SuperSectionPDE x41 x42 x43 x44 x45 x46))); y \<notin> {ptr..ptr + 2 ^ sz - 1}; is_aligned y 2; x && ~~ mask 6 = y && ~~ mask 6\<rbrakk> \<Longrightarrow> Some (KOArch (KOPDE (ARM_H.SuperSectionPDE x41 x42 x43 x44 x45 x46))) = m y proof (prove)
goal (3 subgoals):
 1. \<And>x y ya. \<lbrakk>x \<notin> {ptr..ptr + 2 ^ sz - 1}; y \<in> {ptr..ptr + 2 ^ sz - 1}; m y = Some ya; is_aligned y 2; 6 \<le> sz; x && ~~ mask sz = y && ~~ mask sz\<rbrakk> \<Longrightarrow> False
 2. \<And>x y x41 x42 x43 x44 x45 x46. \<lbrakk>x \<notin> {ptr..ptr + 2 ^ sz - 1}; m x = Some (KOArch (KOPDE (ARM_H.SuperSectionPDE x41 x42 x43 x44 x45 x46))); y \<in> {ptr..ptr + 2 ^ sz - 1}; m y = None; is_aligned y 2; x && ~~ mask 6 = y && ~~ mask 6\<rbrakk> \<Longrightarrow> False
 3. \<And>x y x41 x42 x43 x44 x45 x46. \<lbrakk>x \<notin> {ptr..ptr + 2 ^ sz - 1}; m x = Some (KOArch (KOPDE (ARM_H.SuperSectionPDE x41 x42 x43 x44 x45 x46))); y \<notin> {ptr..ptr + 2 ^ sz - 1}; is_aligned y 2; x && ~~ mask 6 = y && ~~ mask 6\<rbrakk> \<Longrightarrow> Some (KOArch (KOPDE (ARM_H.SuperSectionPDE x41 x42 x43 x44 x45 x46))) = m y proof (prove)
goal (2 subgoals):
 1. \<And>x y x41 x42 x43 x44 x45 x46. \<lbrakk>x \<notin> {ptr..ptr + 2 ^ sz - 1}; m x = Some (KOArch (KOPDE (ARM_H.SuperSectionPDE x41 x42 x43 x44 x45 x46))); y \<in> {ptr..ptr + 2 ^ sz - 1}; m y = None; is_aligned y 2; x && ~~ mask 6 = y && ~~ mask 6\<rbrakk> \<Longrightarrow> False
 2. \<And>x y x41 x42 x43 x44 x45 x46. \<lbrakk>x \<notin> {ptr..ptr + 2 ^ sz - 1}; m x = Some (KOArch (KOPDE (ARM_H.SuperSectionPDE x41 x42 x43 x44 x45 x46))); y \<notin> {ptr..ptr + 2 ^ sz - 1}; is_aligned y 2; x && ~~ mask 6 = y && ~~ mask 6\<rbrakk> \<Longrightarrow> Some (KOArch (KOPDE (ARM_H.SuperSectionPDE x41 x42 x43 x44 x45 x46))) = m y proof (prove)
goal (4 subgoals):
 1. \<And>x y x41 x42 x43 x44 x45 x46. \<lbrakk>x \<notin> {ptr..ptr + 2 ^ sz - 1}; y \<in> {ptr..ptr + 2 ^ sz - 1}; m y = None; is_aligned y 2; x && ~~ mask 6 = y && ~~ mask 6\<rbrakk> \<Longrightarrow> is_aligned y 2
 2. \<And>x y x41 x42 x43 x44 x45 x46. \<lbrakk>x \<notin> {ptr..ptr + 2 ^ sz - 1}; y \<in> {ptr..ptr + 2 ^ sz - 1}; m y = None; is_aligned y 2; x && ~~ mask 6 = y && ~~ mask 6\<rbrakk> \<Longrightarrow> x && ~~ mask (vs_ptr_align (KOArch (KOPDE (ARM_H.SuperSectionPDE x41 x42 x43 x44 x45 x46)))) = y && ~~ mask (vs_ptr_align (KOArch (KOPDE (ARM_H.SuperSectionPDE x41 x42 x43 x44 x45 x46))))
 3. \<And>x y x41 x42 x43 x44 x45 x46. \<lbrakk>x \<notin> {ptr..ptr + 2 ^ sz - 1}; y \<in> {ptr..ptr + 2 ^ sz - 1}; m y = None; is_aligned y 2; x && ~~ mask 6 = y && ~~ mask 6; m y = Some (KOArch (KOPDE (ARM_H.SuperSectionPDE x41 x42 x43 x44 x45 x46)))\<rbrakk> \<Longrightarrow> False
 4. \<And>x y x41 x42 x43 x44 x45 x46. \<lbrakk>x \<notin> {ptr..ptr + 2 ^ sz - 1}; m x = Some (KOArch (KOPDE (ARM_H.SuperSectionPDE x41 x42 x43 x44 x45 x46))); y \<notin> {ptr..ptr + 2 ^ sz - 1}; is_aligned y 2; x && ~~ mask 6 = y && ~~ mask 6\<rbrakk> \<Longrightarrow> Some (KOArch (KOPDE (ARM_H.SuperSectionPDE x41 x42 x43 x44 x45 x46))) = m y proof (prove)
goal (3 subgoals):
 1. \<And>x y x41 x42 x43 x44 x45 x46. \<lbrakk>x \<notin> {ptr..ptr + 2 ^ sz - 1}; y \<in> {ptr..ptr + 2 ^ sz - 1}; m y = None; is_aligned y 2; x && ~~ mask 6 = y && ~~ mask 6\<rbrakk> \<Longrightarrow> x && ~~ mask (vs_ptr_align (KOArch (KOPDE (ARM_H.SuperSectionPDE x41 x42 x43 x44 x45 x46)))) = y && ~~ mask (vs_ptr_align (KOArch (KOPDE (ARM_H.SuperSectionPDE x41 x42 x43 x44 x45 x46))))
 2. \<And>x y x41 x42 x43 x44 x45 x46. \<lbrakk>x \<notin> {ptr..ptr + 2 ^ sz - 1}; y \<in> {ptr..ptr + 2 ^ sz - 1}; m y = None; is_aligned y 2; x && ~~ mask 6 = y && ~~ mask 6; m y = Some (KOArch (KOPDE (ARM_H.SuperSectionPDE x41 x42 x43 x44 x45 x46)))\<rbrakk> \<Longrightarrow> False
 3. \<And>x y x41 x42 x43 x44 x45 x46. \<lbrakk>x \<notin> {ptr..ptr + 2 ^ sz - 1}; m x = Some (KOArch (KOPDE (ARM_H.SuperSectionPDE x41 x42 x43 x44 x45 x46))); y \<notin> {ptr..ptr + 2 ^ sz - 1}; is_aligned y 2; x && ~~ mask 6 = y && ~~ mask 6\<rbrakk> \<Longrightarrow> Some (KOArch (KOPDE (ARM_H.SuperSectionPDE x41 x42 x43 x44 x45 x46))) = m y proof (prove)
goal (2 subgoals):
 1. \<And>x y x41 x42 x43 x44 x45 x46. \<lbrakk>x \<notin> {ptr..ptr + 2 ^ sz - 1}; y \<in> {ptr..ptr + 2 ^ sz - 1}; m y = None; is_aligned y 2; x && ~~ mask 6 = y && ~~ mask 6; m y = Some (KOArch (KOPDE (ARM_H.SuperSectionPDE x41 x42 x43 x44 x45 x46)))\<rbrakk> \<Longrightarrow> False
 2. \<And>x y x41 x42 x43 x44 x45 x46. \<lbrakk>x \<notin> {ptr..ptr + 2 ^ sz - 1}; m x = Some (KOArch (KOPDE (ARM_H.SuperSectionPDE x41 x42 x43 x44 x45 x46))); y \<notin> {ptr..ptr + 2 ^ sz - 1}; is_aligned y 2; x && ~~ mask 6 = y && ~~ mask 6\<rbrakk> \<Longrightarrow> Some (KOArch (KOPDE (ARM_H.SuperSectionPDE x41 x42 x43 x44 x45 x46))) = m y proof (prove)
goal (1 subgoal):
 1. \<And>x y x41 x42 x43 x44 x45 x46. \<lbrakk>x \<notin> {ptr..ptr + 2 ^ sz - 1}; m x = Some (KOArch (KOPDE (ARM_H.SuperSectionPDE x41 x42 x43 x44 x45 x46))); y \<notin> {ptr..ptr + 2 ^ sz - 1}; is_aligned y 2; x && ~~ mask 6 = y && ~~ mask 6\<rbrakk> \<Longrightarrow> Some (KOArch (KOPDE (ARM_H.SuperSectionPDE x41 x42 x43 x44 x45 x46))) = m y proof (prove)
goal (3 subgoals):
 1. \<And>x y x41 x42 x43 x44 x45 x46. \<lbrakk>x \<notin> {ptr..ptr + 2 ^ sz - 1}; y \<notin> {ptr..ptr + 2 ^ sz - 1}; is_aligned y 2; x && ~~ mask 6 = y && ~~ mask 6\<rbrakk> \<Longrightarrow> is_aligned y 2
 2. \<And>x y x41 x42 x43 x44 x45 x46. \<lbrakk>x \<notin> {ptr..ptr + 2 ^ sz - 1}; y \<notin> {ptr..ptr + 2 ^ sz - 1}; is_aligned y 2; x && ~~ mask 6 = y && ~~ mask 6\<rbrakk> \<Longrightarrow> x && ~~ mask (vs_ptr_align (KOArch (KOPDE (ARM_H.SuperSectionPDE x41 x42 x43 x44 x45 x46)))) = y && ~~ mask (vs_ptr_align (KOArch (KOPDE (ARM_H.SuperSectionPDE x41 x42 x43 x44 x45 x46))))
 3. \<And>x y x41 x42 x43 x44 x45 x46. \<lbrakk>x \<notin> {ptr..ptr + 2 ^ sz - 1}; y \<notin> {ptr..ptr + 2 ^ sz - 1}; is_aligned y 2; x && ~~ mask 6 = y && ~~ mask 6; m y = Some (KOArch (KOPDE (ARM_H.SuperSectionPDE x41 x42 x43 x44 x45 x46)))\<rbrakk> \<Longrightarrow> Some (KOArch (KOPDE (ARM_H.SuperSectionPDE x41 x42 x43 x44 x45 x46))) = m y proof (prove)
goal (2 subgoals):
 1. \<And>x y x41 x42 x43 x44 x45 x46. \<lbrakk>x \<notin> {ptr..ptr + 2 ^ sz - 1}; y \<notin> {ptr..ptr + 2 ^ sz - 1}; is_aligned y 2; x && ~~ mask 6 = y && ~~ mask 6\<rbrakk> \<Longrightarrow> x && ~~ mask (vs_ptr_align (KOArch (KOPDE (ARM_H.SuperSectionPDE x41 x42 x43 x44 x45 x46)))) = y && ~~ mask (vs_ptr_align (KOArch (KOPDE (ARM_H.SuperSectionPDE x41 x42 x43 x44 x45 x46))))
 2. \<And>x y x41 x42 x43 x44 x45 x46. \<lbrakk>x \<notin> {ptr..ptr + 2 ^ sz - 1}; y \<notin> {ptr..ptr + 2 ^ sz - 1}; is_aligned y 2; x && ~~ mask 6 = y && ~~ mask 6; m y = Some (KOArch (KOPDE (ARM_H.SuperSectionPDE x41 x42 x43 x44 x45 x46)))\<rbrakk> \<Longrightarrow> Some (KOArch (KOPDE (ARM_H.SuperSectionPDE x41 x42 x43 x44 x45 x46))) = m y proof (prove)
goal (1 subgoal):
 1. \<And>x y x41 x42 x43 x44 x45 x46. \<lbrakk>x \<notin> {ptr..ptr + 2 ^ sz - 1}; y \<notin> {ptr..ptr + 2 ^ sz - 1}; is_aligned y 2; x && ~~ mask 6 = y && ~~ mask 6; m y = Some (KOArch (KOPDE (ARM_H.SuperSectionPDE x41 x42 x43 x44 x45 x46)))\<rbrakk> \<Longrightarrow> Some (KOArch (KOPDE (ARM_H.SuperSectionPDE x41 x42 x43 x44 x45 x46))) = m y proof (prove)
goal:
No subgoals!