theory PageTableDuplicates

lemma copyGlobalMappings_valid_duplicates':
  notes blah[simp del] =  atLeastatMost_subset_iff atLeastLessThan_iff
          Int_atLeastAtMost atLeastatMost_empty_iff split_paired_Ex
          atLeastAtMost_iff
  shows "\<lbrace>(\<lambda>s. vs_valid_duplicates' (ksPSpace s)) and pspace_distinct'
    and pspace_aligned'
    and (\<lambda>s. is_aligned (armKSGlobalPD (ksArchState s)) pdBits)
    and K (is_aligned ptr pdBits)\<rbrace>
  copyGlobalMappings ptr \<lbrace>\<lambda>y s. vs_valid_duplicates' (ksPSpace s)\<rbrace>" proof - have neg_mask_simp: "\<And>x ptr' ptr a.
      \<lbrakk>is_aligned ptr pdBits\<rbrakk>
      \<Longrightarrow> x + ptr && ~~ mask (vs_ptr_align a) = (x && ~~ mask (vs_ptr_align a))
      + ptr" apply (cut_tac a = a in vs_ptr_align_upbound) apply (subst add.commute) apply (subst mask_out_add_aligned[symmetric]) apply (erule is_aligned_weaken) apply (simp add: pdBits_def pageBits_def)+ done have eq_trans: "\<And>a b c d f. (c = d) \<Longrightarrow> (a = f c) \<Longrightarrow> (b = f d) \<Longrightarrow> (a = b)" by auto have mask_sub_mask:"\<And>m n x. ((x::word32) && mask n) && ~~ mask m = (x && ~~ mask m ) && mask n" by (rule word_eqI, auto) show ?thesis apply (clarsimp simp:valid_def) apply (subst vs_valid_duplicates'_def) apply (clarsimp split:option.splits) apply (drule copyGlobalMappings_ksPSpace_concrete) apply simp+ apply (intro conjI) apply clarsimp apply (frule_tac ptr = ptr in globalPDEWindow_neg_mask) apply simp apply simp apply (clarsimp split:if_splits) apply (drule_tac p' = "((y && mask pdBits) + armKSGlobalPD (ksArchState s))"
     in valid_duplicates'_D[rotated]) apply (erule aligned_add_aligned[OF is_aligned_andI1]) apply (erule is_aligned_weaken[where y = 2]) apply (simp add:pdBits_def) apply simp apply (frule_tac x = "x && mask pdBits" and a = x2 and ptr = "armKSGlobalPD (ksArchState s)"
         in neg_mask_simp) apply (drule_tac x = "y && mask pdBits" and a = x2 and ptr = "armKSGlobalPD (ksArchState s)"
       in neg_mask_simp) apply (simp add:mask_sub_mask) apply simp apply simp apply (clarsimp split:if_splits) apply (drule_tac ptr = ptr in globalPDEWindow_neg_mask[OF sym]) apply simp apply simp apply simp apply (drule_tac p' = y  in valid_duplicates'_D[rotated]) apply simp+ done qed

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>(\<lambda>s. vs_valid_duplicates' (ksPSpace s)) and pspace_distinct' and pspace_aligned' and (\<lambda>s. is_aligned (armKSGlobalPD (ksArchState s)) pdBits) and K (is_aligned ptr pdBits)\<rbrace> copyGlobalMappings ptr \<lbrace>\<lambda>y s. vs_valid_duplicates' (ksPSpace s)\<rbrace> proof (state)
goal (1 subgoal):
 1. \<lbrace>(\<lambda>s. vs_valid_duplicates' (ksPSpace s)) and pspace_distinct' and pspace_aligned' and (\<lambda>s. is_aligned (armKSGlobalPD (ksArchState s)) pdBits) and K (is_aligned ptr pdBits)\<rbrace> copyGlobalMappings ptr \<lbrace>\<lambda>y s. vs_valid_duplicates' (ksPSpace s)\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>x ptr' ptr a. is_aligned ptr pdBits \<Longrightarrow> x + ptr && ~~ mask (vs_ptr_align a) = (x && ~~ mask (vs_ptr_align a)) + ptr proof (prove)
goal (1 subgoal):
 1. \<And>x ptr' ptr a. \<lbrakk>is_aligned ptr pdBits; vs_ptr_align a \<le> 6\<rbrakk> \<Longrightarrow> x + ptr && ~~ mask (vs_ptr_align a) = (x && ~~ mask (vs_ptr_align a)) + ptr proof (prove)
goal (1 subgoal):
 1. \<And>x ptr' ptr a. \<lbrakk>is_aligned ptr pdBits; vs_ptr_align a \<le> 6\<rbrakk> \<Longrightarrow> ptr + x && ~~ mask (vs_ptr_align a) = (x && ~~ mask (vs_ptr_align a)) + ptr proof (prove)
goal (2 subgoals):
 1. \<And>x ptr' ptr a. \<lbrakk>is_aligned ptr pdBits; vs_ptr_align a \<le> 6\<rbrakk> \<Longrightarrow> is_aligned ptr (vs_ptr_align a)
 2. \<And>x ptr' ptr a. \<lbrakk>is_aligned ptr pdBits; vs_ptr_align a \<le> 6\<rbrakk> \<Longrightarrow> ptr + (x && ~~ mask (vs_ptr_align a)) = (x && ~~ mask (vs_ptr_align a)) + ptr proof (prove)
goal (2 subgoals):
 1. \<And>x ptr' ptr a. vs_ptr_align a \<le> 6 \<Longrightarrow> vs_ptr_align a \<le> pdBits
 2. \<And>x ptr' ptr a. \<lbrakk>is_aligned ptr pdBits; vs_ptr_align a \<le> 6\<rbrakk> \<Longrightarrow> ptr + (x && ~~ mask (vs_ptr_align a)) = (x && ~~ mask (vs_ptr_align a)) + ptr proof (prove)
goal:
No subgoals! proof (state)
this:
is_aligned ?ptr pdBits \<Longrightarrow> ?x + ?ptr && ~~ mask (vs_ptr_align ?a) = (?x && ~~ mask (vs_ptr_align ?a)) + ?ptr

goal (1 subgoal):
 1. \<lbrace>(\<lambda>s. vs_valid_duplicates' (ksPSpace s)) and pspace_distinct' and pspace_aligned' and (\<lambda>s. is_aligned (armKSGlobalPD (ksArchState s)) pdBits) and K (is_aligned ptr pdBits)\<rbrace> copyGlobalMappings ptr \<lbrace>\<lambda>y s. vs_valid_duplicates' (ksPSpace s)\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>a b c d f. \<lbrakk>c = d; a = f c; b = f d\<rbrakk> \<Longrightarrow> a = b proof (state)
this:
\<lbrakk>?c1 = ?d1; ?a1 = ?f1 ?c1; ?b1 = ?f1 ?d1\<rbrakk> \<Longrightarrow> ?a1 = ?b1

goal (1 subgoal):
 1. \<lbrace>(\<lambda>s. vs_valid_duplicates' (ksPSpace s)) and pspace_distinct' and pspace_aligned' and (\<lambda>s. is_aligned (armKSGlobalPD (ksArchState s)) pdBits) and K (is_aligned ptr pdBits)\<rbrace> copyGlobalMappings ptr \<lbrace>\<lambda>y s. vs_valid_duplicates' (ksPSpace s)\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>m n x. (x && mask n) && ~~ mask m = (x && ~~ mask m) && mask n proof (state)
this:
(?x2 && mask ?n2) && ~~ mask ?m2 = (?x2 && ~~ mask ?m2) && mask ?n2

goal (1 subgoal):
 1. \<lbrace>(\<lambda>s. vs_valid_duplicates' (ksPSpace s)) and pspace_distinct' and pspace_aligned' and (\<lambda>s. is_aligned (armKSGlobalPD (ksArchState s)) pdBits) and K (is_aligned ptr pdBits)\<rbrace> copyGlobalMappings ptr \<lbrace>\<lambda>y s. vs_valid_duplicates' (ksPSpace s)\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>(\<lambda>s. vs_valid_duplicates' (ksPSpace s)) and pspace_distinct' and pspace_aligned' and (\<lambda>s. is_aligned (armKSGlobalPD (ksArchState s)) pdBits) and K (is_aligned ptr pdBits)\<rbrace> copyGlobalMappings ptr \<lbrace>\<lambda>y s. vs_valid_duplicates' (ksPSpace s)\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s b. \<lbrakk>((), b) \<in> fst (copyGlobalMappings ptr s); vs_valid_duplicates' (ksPSpace s); pspace_distinct' s; pspace_aligned' s; is_aligned (armKSGlobalPD (ksArchState s)) pdBits; is_aligned ptr pdBits\<rbrakk> \<Longrightarrow> vs_valid_duplicates' (ksPSpace b) proof (prove)
goal (1 subgoal):
 1. \<And>s b. \<lbrakk>((), b) \<in> fst (copyGlobalMappings ptr s); vs_valid_duplicates' (ksPSpace s); pspace_distinct' s; pspace_aligned' s; is_aligned (armKSGlobalPD (ksArchState s)) pdBits; is_aligned ptr pdBits\<rbrakk> \<Longrightarrow> \<forall>x y. case ksPSpace b x of None \<Rightarrow> True | Some ko \<Rightarrow> is_aligned y 2 \<longrightarrow> x && ~~ mask (vs_ptr_align ko) = y && ~~ mask (vs_ptr_align ko) \<longrightarrow> ksPSpace b x = ksPSpace b y proof (prove)
goal (1 subgoal):
 1. \<And>s b x y x2. \<lbrakk>((), b) \<in> fst (copyGlobalMappings ptr s); vs_valid_duplicates' (ksPSpace s); pspace_distinct' s; pspace_aligned' s; is_aligned (armKSGlobalPD (ksArchState s)) pdBits; is_aligned ptr pdBits; ksPSpace b x = Some x2; is_aligned y 2; x && ~~ mask (vs_ptr_align x2) = y && ~~ mask (vs_ptr_align x2)\<rbrakk> \<Longrightarrow> Some x2 = ksPSpace b y proof (prove)
goal (5 subgoals):
 1. \<And>s b x y x2. \<lbrakk>vs_valid_duplicates' (ksPSpace s); pspace_distinct' s; pspace_aligned' s; is_aligned (armKSGlobalPD (ksArchState s)) pdBits; is_aligned ptr pdBits; ksPSpace b x = Some x2; is_aligned y 2; x && ~~ mask (vs_ptr_align x2) = y && ~~ mask (vs_ptr_align x2)\<rbrakk> \<Longrightarrow> pspace_distinct' s
 2. \<And>s b x y x2. \<lbrakk>vs_valid_duplicates' (ksPSpace s); pspace_distinct' s; pspace_aligned' s; is_aligned (armKSGlobalPD (ksArchState s)) pdBits; is_aligned ptr pdBits; ksPSpace b x = Some x2; is_aligned y 2; x && ~~ mask (vs_ptr_align x2) = y && ~~ mask (vs_ptr_align x2)\<rbrakk> \<Longrightarrow> pspace_aligned' s
 3. \<And>s b x y x2. \<lbrakk>vs_valid_duplicates' (ksPSpace s); pspace_distinct' s; pspace_aligned' s; is_aligned (armKSGlobalPD (ksArchState s)) pdBits; is_aligned ptr pdBits; ksPSpace b x = Some x2; is_aligned y 2; x && ~~ mask (vs_ptr_align x2) = y && ~~ mask (vs_ptr_align x2)\<rbrakk> \<Longrightarrow> is_aligned (armKSGlobalPD (ksArchState s)) pdBits
 4. \<And>s b x y x2. \<lbrakk>vs_valid_duplicates' (ksPSpace s); pspace_distinct' s; pspace_aligned' s; is_aligned (armKSGlobalPD (ksArchState s)) pdBits; is_aligned ptr pdBits; ksPSpace b x = Some x2; is_aligned y 2; x && ~~ mask (vs_ptr_align x2) = y && ~~ mask (vs_ptr_align x2)\<rbrakk> \<Longrightarrow> is_aligned ptr pdBits
 5. \<And>s b x y x2. \<lbrakk>vs_valid_duplicates' (ksPSpace s); pspace_distinct' s; pspace_aligned' s; is_aligned (armKSGlobalPD (ksArchState s)) pdBits; is_aligned ptr pdBits; ksPSpace b x = Some x2; is_aligned y 2; x && ~~ mask (vs_ptr_align x2) = y && ~~ mask (vs_ptr_align x2); ksPSpace b = (\<lambda>x. if x \<in> {ptr + (pptrBase >> 20 << 2)..ptr + (2 ^ pdBits - 1)} then ksPSpace s ((x && mask pdBits) + armKSGlobalPD (ksArchState s)) else ksPSpace s x)\<rbrakk> \<Longrightarrow> Some x2 = ksPSpace b y proof (prove)
goal (1 subgoal):
 1. \<And>s b x y x2. \<lbrakk>vs_valid_duplicates' (ksPSpace s); pspace_distinct' s; pspace_aligned' s; is_aligned (armKSGlobalPD (ksArchState s)) pdBits; is_aligned ptr pdBits; (if x \<in> {ptr + (pptrBase >> 20 << 2)..ptr + (2 ^ pdBits - 1)} then ksPSpace s ((x && mask pdBits) + armKSGlobalPD (ksArchState s)) else ksPSpace s x) = Some x2; is_aligned y 2; x && ~~ mask (vs_ptr_align x2) = y && ~~ mask (vs_ptr_align x2); ksPSpace b = (\<lambda>x. if x \<in> {ptr + (pptrBase >> 20 << 2)..ptr + (2 ^ pdBits - 1)} then ksPSpace s ((x && mask pdBits) + armKSGlobalPD (ksArchState s)) else ksPSpace s x)\<rbrakk> \<Longrightarrow> (y \<in> {ptr + (pptrBase >> 20 << 2)..ptr + (2 ^ pdBits - 1)} \<longrightarrow> Some x2 = ksPSpace s ((y && mask pdBits) + armKSGlobalPD (ksArchState s))) \<and> (y \<notin> {ptr + (pptrBase >> 20 << 2)..ptr + (2 ^ pdBits - 1)} \<longrightarrow> Some x2 = ksPSpace s y) proof (prove)
goal (2 subgoals):
 1. \<And>s b x y x2. \<lbrakk>vs_valid_duplicates' (ksPSpace s); pspace_distinct' s; pspace_aligned' s; is_aligned (armKSGlobalPD (ksArchState s)) pdBits; is_aligned ptr pdBits; (if x \<in> {ptr + (pptrBase >> 20 << 2)..ptr + (2 ^ pdBits - 1)} then ksPSpace s ((x && mask pdBits) + armKSGlobalPD (ksArchState s)) else ksPSpace s x) = Some x2; is_aligned y 2; x && ~~ mask (vs_ptr_align x2) = y && ~~ mask (vs_ptr_align x2); ksPSpace b = (\<lambda>x. if x \<in> {ptr + (pptrBase >> 20 << 2)..ptr + (2 ^ pdBits - 1)} then ksPSpace s ((x && mask pdBits) + armKSGlobalPD (ksArchState s)) else ksPSpace s x)\<rbrakk> \<Longrightarrow> y \<in> {ptr + (pptrBase >> 20 << 2)..ptr + (2 ^ pdBits - 1)} \<longrightarrow> Some x2 = ksPSpace s ((y && mask pdBits) + armKSGlobalPD (ksArchState s))
 2. \<And>s b x y x2. \<lbrakk>vs_valid_duplicates' (ksPSpace s); pspace_distinct' s; pspace_aligned' s; is_aligned (armKSGlobalPD (ksArchState s)) pdBits; is_aligned ptr pdBits; (if x \<in> {ptr + (pptrBase >> 20 << 2)..ptr + (2 ^ pdBits - 1)} then ksPSpace s ((x && mask pdBits) + armKSGlobalPD (ksArchState s)) else ksPSpace s x) = Some x2; is_aligned y 2; x && ~~ mask (vs_ptr_align x2) = y && ~~ mask (vs_ptr_align x2); ksPSpace b = (\<lambda>x. if x \<in> {ptr + (pptrBase >> 20 << 2)..ptr + (2 ^ pdBits - 1)} then ksPSpace s ((x && mask pdBits) + armKSGlobalPD (ksArchState s)) else ksPSpace s x)\<rbrakk> \<Longrightarrow> y \<notin> {ptr + (pptrBase >> 20 << 2)..ptr + (2 ^ pdBits - 1)} \<longrightarrow> Some x2 = ksPSpace s y proof (prove)
goal (2 subgoals):
 1. \<And>s b x y x2. \<lbrakk>vs_valid_duplicates' (ksPSpace s); pspace_distinct' s; pspace_aligned' s; is_aligned (armKSGlobalPD (ksArchState s)) pdBits; is_aligned ptr pdBits; (if x \<in> {ptr + (pptrBase >> 20 << 2)..ptr + (2 ^ pdBits - 1)} then ksPSpace s ((x && mask pdBits) + armKSGlobalPD (ksArchState s)) else ksPSpace s x) = Some x2; is_aligned y 2; x && ~~ mask (vs_ptr_align x2) = y && ~~ mask (vs_ptr_align x2); ksPSpace b = (\<lambda>x. if x \<in> {ptr + (pptrBase >> 20 << 2)..ptr + (2 ^ pdBits - 1)} then ksPSpace s ((x && mask pdBits) + armKSGlobalPD (ksArchState s)) else ksPSpace s x); y \<in> {ptr + (pptrBase >> 20 << 2)..ptr + (2 ^ pdBits - 1)}\<rbrakk> \<Longrightarrow> Some x2 = ksPSpace s ((y && mask pdBits) + armKSGlobalPD (ksArchState s))
 2. \<And>s b x y x2. \<lbrakk>vs_valid_duplicates' (ksPSpace s); pspace_distinct' s; pspace_aligned' s; is_aligned (armKSGlobalPD (ksArchState s)) pdBits; is_aligned ptr pdBits; (if x \<in> {ptr + (pptrBase >> 20 << 2)..ptr + (2 ^ pdBits - 1)} then ksPSpace s ((x && mask pdBits) + armKSGlobalPD (ksArchState s)) else ksPSpace s x) = Some x2; is_aligned y 2; x && ~~ mask (vs_ptr_align x2) = y && ~~ mask (vs_ptr_align x2); ksPSpace b = (\<lambda>x. if x \<in> {ptr + (pptrBase >> 20 << 2)..ptr + (2 ^ pdBits - 1)} then ksPSpace s ((x && mask pdBits) + armKSGlobalPD (ksArchState s)) else ksPSpace s x)\<rbrakk> \<Longrightarrow> y \<notin> {ptr + (pptrBase >> 20 << 2)..ptr + (2 ^ pdBits - 1)} \<longrightarrow> Some x2 = ksPSpace s y proof (prove)
goal (4 subgoals):
 1. \<And>s b x y x2. \<lbrakk>vs_valid_duplicates' (ksPSpace s); pspace_distinct' s; pspace_aligned' s; is_aligned (armKSGlobalPD (ksArchState s)) pdBits; is_aligned ptr pdBits; (if x \<in> {ptr + (pptrBase >> 20 << 2)..ptr + (2 ^ pdBits - 1)} then ksPSpace s ((x && mask pdBits) + armKSGlobalPD (ksArchState s)) else ksPSpace s x) = Some x2; is_aligned y 2; x && ~~ mask (vs_ptr_align x2) = y && ~~ mask (vs_ptr_align x2); ksPSpace b = (\<lambda>x. if x \<in> {ptr + (pptrBase >> 20 << 2)..ptr + (2 ^ pdBits - 1)} then ksPSpace s ((x && mask pdBits) + armKSGlobalPD (ksArchState s)) else ksPSpace s x); y \<in> {ptr + (pptrBase >> 20 << 2)..ptr + (2 ^ pdBits - 1)}\<rbrakk> \<Longrightarrow> is_aligned ptr pdBits
 2. \<And>s b x y x2. \<lbrakk>vs_valid_duplicates' (ksPSpace s); pspace_distinct' s; pspace_aligned' s; is_aligned (armKSGlobalPD (ksArchState s)) pdBits; is_aligned ptr pdBits; (if x \<in> {ptr + (pptrBase >> 20 << 2)..ptr + (2 ^ pdBits - 1)} then ksPSpace s ((x && mask pdBits) + armKSGlobalPD (ksArchState s)) else ksPSpace s x) = Some x2; is_aligned y 2; x && ~~ mask (vs_ptr_align x2) = y && ~~ mask (vs_ptr_align x2); ksPSpace b = (\<lambda>x. if x \<in> {ptr + (pptrBase >> 20 << 2)..ptr + (2 ^ pdBits - 1)} then ksPSpace s ((x && mask pdBits) + armKSGlobalPD (ksArchState s)) else ksPSpace s x); y \<in> {ptr + (pptrBase >> 20 << 2)..ptr + (2 ^ pdBits - 1)}\<rbrakk> \<Longrightarrow> y \<in> {ptr + (pptrBase >> 20 << 2)..ptr + (2 ^ pdBits - 1)}
 3. \<And>s b x y x2. \<lbrakk>vs_valid_duplicates' (ksPSpace s); pspace_distinct' s; pspace_aligned' s; is_aligned (armKSGlobalPD (ksArchState s)) pdBits; is_aligned ptr pdBits; (if x \<in> {ptr + (pptrBase >> 20 << 2)..ptr + (2 ^ pdBits - 1)} then ksPSpace s ((x && mask pdBits) + armKSGlobalPD (ksArchState s)) else ksPSpace s x) = Some x2; is_aligned y 2; x && ~~ mask (vs_ptr_align x2) = y && ~~ mask (vs_ptr_align x2); ksPSpace b = (\<lambda>x. if x \<in> {ptr + (pptrBase >> 20 << 2)..ptr + (2 ^ pdBits - 1)} then ksPSpace s ((x && mask pdBits) + armKSGlobalPD (ksArchState s)) else ksPSpace s x); y \<in> {ptr + (pptrBase >> 20 << 2)..ptr + (2 ^ pdBits - 1)}; x \<in> {ptr + (pptrBase >> 20 << 2)..ptr + (2 ^ pdBits - 1)}\<rbrakk> \<Longrightarrow> Some x2 = ksPSpace s ((y && mask pdBits) + armKSGlobalPD (ksArchState s))
 4. \<And>s b x y x2. \<lbrakk>vs_valid_duplicates' (ksPSpace s); pspace_distinct' s; pspace_aligned' s; is_aligned (armKSGlobalPD (ksArchState s)) pdBits; is_aligned ptr pdBits; (if x \<in> {ptr + (pptrBase >> 20 << 2)..ptr + (2 ^ pdBits - 1)} then ksPSpace s ((x && mask pdBits) + armKSGlobalPD (ksArchState s)) else ksPSpace s x) = Some x2; is_aligned y 2; x && ~~ mask (vs_ptr_align x2) = y && ~~ mask (vs_ptr_align x2); ksPSpace b = (\<lambda>x. if x \<in> {ptr + (pptrBase >> 20 << 2)..ptr + (2 ^ pdBits - 1)} then ksPSpace s ((x && mask pdBits) + armKSGlobalPD (ksArchState s)) else ksPSpace s x)\<rbrakk> \<Longrightarrow> y \<notin> {ptr + (pptrBase >> 20 << 2)..ptr + (2 ^ pdBits - 1)} \<longrightarrow> Some x2 = ksPSpace s y proof (prove)
goal (3 subgoals):
 1. \<And>s b x y x2. \<lbrakk>vs_valid_duplicates' (ksPSpace s); pspace_distinct' s; pspace_aligned' s; is_aligned (armKSGlobalPD (ksArchState s)) pdBits; is_aligned ptr pdBits; (if x \<in> {ptr + (pptrBase >> 20 << 2)..ptr + (2 ^ pdBits - 1)} then ksPSpace s ((x && mask pdBits) + armKSGlobalPD (ksArchState s)) else ksPSpace s x) = Some x2; is_aligned y 2; x && ~~ mask (vs_ptr_align x2) = y && ~~ mask (vs_ptr_align x2); ksPSpace b = (\<lambda>x. if x \<in> {ptr + (pptrBase >> 20 << 2)..ptr + (2 ^ pdBits - 1)} then ksPSpace s ((x && mask pdBits) + armKSGlobalPD (ksArchState s)) else ksPSpace s x); y \<in> {ptr + (pptrBase >> 20 << 2)..ptr + (2 ^ pdBits - 1)}\<rbrakk> \<Longrightarrow> y \<in> {ptr + (pptrBase >> 20 << 2)..ptr + (2 ^ pdBits - 1)}
 2. \<And>s b x y x2. \<lbrakk>vs_valid_duplicates' (ksPSpace s); pspace_distinct' s; pspace_aligned' s; is_aligned (armKSGlobalPD (ksArchState s)) pdBits; is_aligned ptr pdBits; (if x \<in> {ptr + (pptrBase >> 20 << 2)..ptr + (2 ^ pdBits - 1)} then ksPSpace s ((x && mask pdBits) + armKSGlobalPD (ksArchState s)) else ksPSpace s x) = Some x2; is_aligned y 2; x && ~~ mask (vs_ptr_align x2) = y && ~~ mask (vs_ptr_align x2); ksPSpace b = (\<lambda>x. if x \<in> {ptr + (pptrBase >> 20 << 2)..ptr + (2 ^ pdBits - 1)} then ksPSpace s ((x && mask pdBits) + armKSGlobalPD (ksArchState s)) else ksPSpace s x); y \<in> {ptr + (pptrBase >> 20 << 2)..ptr + (2 ^ pdBits - 1)}; x \<in> {ptr + (pptrBase >> 20 << 2)..ptr + (2 ^ pdBits - 1)}\<rbrakk> \<Longrightarrow> Some x2 = ksPSpace s ((y && mask pdBits) + armKSGlobalPD (ksArchState s))
 3. \<And>s b x y x2. \<lbrakk>vs_valid_duplicates' (ksPSpace s); pspace_distinct' s; pspace_aligned' s; is_aligned (armKSGlobalPD (ksArchState s)) pdBits; is_aligned ptr pdBits; (if x \<in> {ptr + (pptrBase >> 20 << 2)..ptr + (2 ^ pdBits - 1)} then ksPSpace s ((x && mask pdBits) + armKSGlobalPD (ksArchState s)) else ksPSpace s x) = Some x2; is_aligned y 2; x && ~~ mask (vs_ptr_align x2) = y && ~~ mask (vs_ptr_align x2); ksPSpace b = (\<lambda>x. if x \<in> {ptr + (pptrBase >> 20 << 2)..ptr + (2 ^ pdBits - 1)} then ksPSpace s ((x && mask pdBits) + armKSGlobalPD (ksArchState s)) else ksPSpace s x)\<rbrakk> \<Longrightarrow> y \<notin> {ptr + (pptrBase >> 20 << 2)..ptr + (2 ^ pdBits - 1)} \<longrightarrow> Some x2 = ksPSpace s y proof (prove)
goal (2 subgoals):
 1. \<And>s b x y x2. \<lbrakk>vs_valid_duplicates' (ksPSpace s); pspace_distinct' s; pspace_aligned' s; is_aligned (armKSGlobalPD (ksArchState s)) pdBits; is_aligned ptr pdBits; (if x \<in> {ptr + (pptrBase >> 20 << 2)..ptr + (2 ^ pdBits - 1)} then ksPSpace s ((x && mask pdBits) + armKSGlobalPD (ksArchState s)) else ksPSpace s x) = Some x2; is_aligned y 2; x && ~~ mask (vs_ptr_align x2) = y && ~~ mask (vs_ptr_align x2); ksPSpace b = (\<lambda>x. if x \<in> {ptr + (pptrBase >> 20 << 2)..ptr + (2 ^ pdBits - 1)} then ksPSpace s ((x && mask pdBits) + armKSGlobalPD (ksArchState s)) else ksPSpace s x); y \<in> {ptr + (pptrBase >> 20 << 2)..ptr + (2 ^ pdBits - 1)}; x \<in> {ptr + (pptrBase >> 20 << 2)..ptr + (2 ^ pdBits - 1)}\<rbrakk> \<Longrightarrow> Some x2 = ksPSpace s ((y && mask pdBits) + armKSGlobalPD (ksArchState s))
 2. \<And>s b x y x2. \<lbrakk>vs_valid_duplicates' (ksPSpace s); pspace_distinct' s; pspace_aligned' s; is_aligned (armKSGlobalPD (ksArchState s)) pdBits; is_aligned ptr pdBits; (if x \<in> {ptr + (pptrBase >> 20 << 2)..ptr + (2 ^ pdBits - 1)} then ksPSpace s ((x && mask pdBits) + armKSGlobalPD (ksArchState s)) else ksPSpace s x) = Some x2; is_aligned y 2; x && ~~ mask (vs_ptr_align x2) = y && ~~ mask (vs_ptr_align x2); ksPSpace b = (\<lambda>x. if x \<in> {ptr + (pptrBase >> 20 << 2)..ptr + (2 ^ pdBits - 1)} then ksPSpace s ((x && mask pdBits) + armKSGlobalPD (ksArchState s)) else ksPSpace s x)\<rbrakk> \<Longrightarrow> y \<notin> {ptr + (pptrBase >> 20 << 2)..ptr + (2 ^ pdBits - 1)} \<longrightarrow> Some x2 = ksPSpace s y proof (prove)
goal (2 subgoals):
 1. \<And>s b x y x2. \<lbrakk>vs_valid_duplicates' (ksPSpace s); pspace_distinct' s; pspace_aligned' s; is_aligned (armKSGlobalPD (ksArchState s)) pdBits; is_aligned ptr pdBits; ksPSpace s ((x && mask pdBits) + armKSGlobalPD (ksArchState s)) = Some x2; is_aligned y 2; x && ~~ mask (vs_ptr_align x2) = y && ~~ mask (vs_ptr_align x2); ksPSpace b = (\<lambda>x. if x \<in> {ptr + (pptrBase >> 20 << 2)..ptr + (2 ^ pdBits - 1)} then ksPSpace s ((x && mask pdBits) + armKSGlobalPD (ksArchState s)) else ksPSpace s x); y \<in> {ptr + (pptrBase >> 20 << 2)..ptr + (2 ^ pdBits - 1)}; x \<in> {ptr + (pptrBase >> 20 << 2)..ptr + (2 ^ pdBits - 1)}\<rbrakk> \<Longrightarrow> Some x2 = ksPSpace s ((y && mask pdBits) + armKSGlobalPD (ksArchState s))
 2. \<And>s b x y x2. \<lbrakk>vs_valid_duplicates' (ksPSpace s); pspace_distinct' s; pspace_aligned' s; is_aligned (armKSGlobalPD (ksArchState s)) pdBits; is_aligned ptr pdBits; (if x \<in> {ptr + (pptrBase >> 20 << 2)..ptr + (2 ^ pdBits - 1)} then ksPSpace s ((x && mask pdBits) + armKSGlobalPD (ksArchState s)) else ksPSpace s x) = Some x2; is_aligned y 2; x && ~~ mask (vs_ptr_align x2) = y && ~~ mask (vs_ptr_align x2); ksPSpace b = (\<lambda>x. if x \<in> {ptr + (pptrBase >> 20 << 2)..ptr + (2 ^ pdBits - 1)} then ksPSpace s ((x && mask pdBits) + armKSGlobalPD (ksArchState s)) else ksPSpace s x)\<rbrakk> \<Longrightarrow> y \<notin> {ptr + (pptrBase >> 20 << 2)..ptr + (2 ^ pdBits - 1)} \<longrightarrow> Some x2 = ksPSpace s y proof (prove)
goal (5 subgoals):
 1. \<And>s b x y x2. \<lbrakk>vs_valid_duplicates' (ksPSpace s); pspace_distinct' s; pspace_aligned' s; is_aligned (armKSGlobalPD (ksArchState s)) pdBits; is_aligned ptr pdBits; is_aligned y 2; x && ~~ mask (vs_ptr_align x2) = y && ~~ mask (vs_ptr_align x2); ksPSpace b = (\<lambda>x. if x \<in> {ptr + (pptrBase >> 20 << 2)..ptr + (2 ^ pdBits - 1)} then ksPSpace s ((x && mask pdBits) + armKSGlobalPD (ksArchState s)) else ksPSpace s x); y \<in> {ptr + (pptrBase >> 20 << 2)..ptr + (2 ^ pdBits - 1)}; x \<in> {ptr + (pptrBase >> 20 << 2)..ptr + (2 ^ pdBits - 1)}\<rbrakk> \<Longrightarrow> is_aligned ((y && mask pdBits) + armKSGlobalPD (ksArchState s)) 2
 2. \<And>s b x y x2. \<lbrakk>vs_valid_duplicates' (ksPSpace s); pspace_distinct' s; pspace_aligned' s; is_aligned (armKSGlobalPD (ksArchState s)) pdBits; is_aligned ptr pdBits; is_aligned y 2; x && ~~ mask (vs_ptr_align x2) = y && ~~ mask (vs_ptr_align x2); ksPSpace b = (\<lambda>x. if x \<in> {ptr + (pptrBase >> 20 << 2)..ptr + (2 ^ pdBits - 1)} then ksPSpace s ((x && mask pdBits) + armKSGlobalPD (ksArchState s)) else ksPSpace s x); y \<in> {ptr + (pptrBase >> 20 << 2)..ptr + (2 ^ pdBits - 1)}; x \<in> {ptr + (pptrBase >> 20 << 2)..ptr + (2 ^ pdBits - 1)}\<rbrakk> \<Longrightarrow> (x && mask pdBits) + armKSGlobalPD (ksArchState s) && ~~ mask (vs_ptr_align x2) = (y && mask pdBits) + armKSGlobalPD (ksArchState s) && ~~ mask (vs_ptr_align x2)
 3. \<And>s b x y x2. \<lbrakk>vs_valid_duplicates' (ksPSpace s); pspace_distinct' s; pspace_aligned' s; is_aligned (armKSGlobalPD (ksArchState s)) pdBits; is_aligned ptr pdBits; is_aligned y 2; x && ~~ mask (vs_ptr_align x2) = y && ~~ mask (vs_ptr_align x2); ksPSpace b = (\<lambda>x. if x \<in> {ptr + (pptrBase >> 20 << 2)..ptr + (2 ^ pdBits - 1)} then ksPSpace s ((x && mask pdBits) + armKSGlobalPD (ksArchState s)) else ksPSpace s x); y \<in> {ptr + (pptrBase >> 20 << 2)..ptr + (2 ^ pdBits - 1)}; x \<in> {ptr + (pptrBase >> 20 << 2)..ptr + (2 ^ pdBits - 1)}\<rbrakk> \<Longrightarrow> vs_valid_duplicates' (ksPSpace s)
 4. \<And>s b x y x2. \<lbrakk>vs_valid_duplicates' (ksPSpace s); pspace_distinct' s; pspace_aligned' s; is_aligned (armKSGlobalPD (ksArchState s)) pdBits; is_aligned ptr pdBits; is_aligned y 2; x && ~~ mask (vs_ptr_align x2) = y && ~~ mask (vs_ptr_align x2); ksPSpace b = (\<lambda>x. if x \<in> {ptr + (pptrBase >> 20 << 2)..ptr + (2 ^ pdBits - 1)} then ksPSpace s ((x && mask pdBits) + armKSGlobalPD (ksArchState s)) else ksPSpace s x); y \<in> {ptr + (pptrBase >> 20 << 2)..ptr + (2 ^ pdBits - 1)}; x \<in> {ptr + (pptrBase >> 20 << 2)..ptr + (2 ^ pdBits - 1)}; ksPSpace s ((y && mask pdBits) + armKSGlobalPD (ksArchState s)) = Some x2\<rbrakk> \<Longrightarrow> Some x2 = ksPSpace s ((y && mask pdBits) + armKSGlobalPD (ksArchState s))
 5. \<And>s b x y x2. \<lbrakk>vs_valid_duplicates' (ksPSpace s); pspace_distinct' s; pspace_aligned' s; is_aligned (armKSGlobalPD (ksArchState s)) pdBits; is_aligned ptr pdBits; (if x \<in> {ptr + (pptrBase >> 20 << 2)..ptr + (2 ^ pdBits - 1)} then ksPSpace s ((x && mask pdBits) + armKSGlobalPD (ksArchState s)) else ksPSpace s x) = Some x2; is_aligned y 2; x && ~~ mask (vs_ptr_align x2) = y && ~~ mask (vs_ptr_align x2); ksPSpace b = (\<lambda>x. if x \<in> {ptr + (pptrBase >> 20 << 2)..ptr + (2 ^ pdBits - 1)} then ksPSpace s ((x && mask pdBits) + armKSGlobalPD (ksArchState s)) else ksPSpace s x)\<rbrakk> \<Longrightarrow> y \<notin> {ptr + (pptrBase >> 20 << 2)..ptr + (2 ^ pdBits - 1)} \<longrightarrow> Some x2 = ksPSpace s y proof (prove)
goal (6 subgoals):
 1. \<And>s b x y x2. \<lbrakk>vs_valid_duplicates' (ksPSpace s); pspace_distinct' s; pspace_aligned' s; is_aligned (armKSGlobalPD (ksArchState s)) pdBits; is_aligned ptr pdBits; x && ~~ mask (vs_ptr_align x2) = y && ~~ mask (vs_ptr_align x2); ksPSpace b = (\<lambda>x. if x \<in> {ptr + (pptrBase >> 20 << 2)..ptr + (2 ^ pdBits - 1)} then ksPSpace s ((x && mask pdBits) + armKSGlobalPD (ksArchState s)) else ksPSpace s x); y \<in> {ptr + (pptrBase >> 20 << 2)..ptr + (2 ^ pdBits - 1)}; x \<in> {ptr + (pptrBase >> 20 << 2)..ptr + (2 ^ pdBits - 1)}\<rbrakk> \<Longrightarrow> is_aligned (armKSGlobalPD (ksArchState s)) 2
 2. \<And>s b x y x2. \<lbrakk>vs_valid_duplicates' (ksPSpace s); pspace_distinct' s; pspace_aligned' s; is_aligned (armKSGlobalPD (ksArchState s)) pdBits; is_aligned ptr pdBits; x && ~~ mask (vs_ptr_align x2) = y && ~~ mask (vs_ptr_align x2); ksPSpace b = (\<lambda>x. if x \<in> {ptr + (pptrBase >> 20 << 2)..ptr + (2 ^ pdBits - 1)} then ksPSpace s ((x && mask pdBits) + armKSGlobalPD (ksArchState s)) else ksPSpace s x); y \<in> {ptr + (pptrBase >> 20 << 2)..ptr + (2 ^ pdBits - 1)}; x \<in> {ptr + (pptrBase >> 20 << 2)..ptr + (2 ^ pdBits - 1)}\<rbrakk> \<Longrightarrow> 2 \<le> 2
 3. \<And>s b x y x2. \<lbrakk>vs_valid_duplicates' (ksPSpace s); pspace_distinct' s; pspace_aligned' s; is_aligned (armKSGlobalPD (ksArchState s)) pdBits; is_aligned ptr pdBits; is_aligned y 2; x && ~~ mask (vs_ptr_align x2) = y && ~~ mask (vs_ptr_align x2); ksPSpace b = (\<lambda>x. if x \<in> {ptr + (pptrBase >> 20 << 2)..ptr + (2 ^ pdBits - 1)} then ksPSpace s ((x && mask pdBits) + armKSGlobalPD (ksArchState s)) else ksPSpace s x); y \<in> {ptr + (pptrBase >> 20 << 2)..ptr + (2 ^ pdBits - 1)}; x \<in> {ptr + (pptrBase >> 20 << 2)..ptr + (2 ^ pdBits - 1)}\<rbrakk> \<Longrightarrow> (x && mask pdBits) + armKSGlobalPD (ksArchState s) && ~~ mask (vs_ptr_align x2) = (y && mask pdBits) + armKSGlobalPD (ksArchState s) && ~~ mask (vs_ptr_align x2)
 4. \<And>s b x y x2. \<lbrakk>vs_valid_duplicates' (ksPSpace s); pspace_distinct' s; pspace_aligned' s; is_aligned (armKSGlobalPD (ksArchState s)) pdBits; is_aligned ptr pdBits; is_aligned y 2; x && ~~ mask (vs_ptr_align x2) = y && ~~ mask (vs_ptr_align x2); ksPSpace b = (\<lambda>x. if x \<in> {ptr + (pptrBase >> 20 << 2)..ptr + (2 ^ pdBits - 1)} then ksPSpace s ((x && mask pdBits) + armKSGlobalPD (ksArchState s)) else ksPSpace s x); y \<in> {ptr + (pptrBase >> 20 << 2)..ptr + (2 ^ pdBits - 1)}; x \<in> {ptr + (pptrBase >> 20 << 2)..ptr + (2 ^ pdBits - 1)}\<rbrakk> \<Longrightarrow> vs_valid_duplicates' (ksPSpace s)
 5. \<And>s b x y x2. \<lbrakk>vs_valid_duplicates' (ksPSpace s); pspace_distinct' s; pspace_aligned' s; is_aligned (armKSGlobalPD (ksArchState s)) pdBits; is_aligned ptr pdBits; is_aligned y 2; x && ~~ mask (vs_ptr_align x2) = y && ~~ mask (vs_ptr_align x2); ksPSpace b = (\<lambda>x. if x \<in> {ptr + (pptrBase >> 20 << 2)..ptr + (2 ^ pdBits - 1)} then ksPSpace s ((x && mask pdBits) + armKSGlobalPD (ksArchState s)) else ksPSpace s x); y \<in> {ptr + (pptrBase >> 20 << 2)..ptr + (2 ^ pdBits - 1)}; x \<in> {ptr + (pptrBase >> 20 << 2)..ptr + (2 ^ pdBits - 1)}; ksPSpace s ((y && mask pdBits) + armKSGlobalPD (ksArchState s)) = Some x2\<rbrakk> \<Longrightarrow> Some x2 = ksPSpace s ((y && mask pdBits) + armKSGlobalPD (ksArchState s))
 6. \<And>s b x y x2. \<lbrakk>vs_valid_duplicates' (ksPSpace s); pspace_distinct' s; pspace_aligned' s; is_aligned (armKSGlobalPD (ksArchState s)) pdBits; is_aligned ptr pdBits; (if x \<in> {ptr + (pptrBase >> 20 << 2)..ptr + (2 ^ pdBits - 1)} then ksPSpace s ((x && mask pdBits) + armKSGlobalPD (ksArchState s)) else ksPSpace s x) = Some x2; is_aligned y 2; x && ~~ mask (vs_ptr_align x2) = y && ~~ mask (vs_ptr_align x2); ksPSpace b = (\<lambda>x. if x \<in> {ptr + (pptrBase >> 20 << 2)..ptr + (2 ^ pdBits - 1)} then ksPSpace s ((x && mask pdBits) + armKSGlobalPD (ksArchState s)) else ksPSpace s x)\<rbrakk> \<Longrightarrow> y \<notin> {ptr + (pptrBase >> 20 << 2)..ptr + (2 ^ pdBits - 1)} \<longrightarrow> Some x2 = ksPSpace s y proof (prove)
goal (6 subgoals):
 1. \<And>s b x y x2. \<lbrakk>vs_valid_duplicates' (ksPSpace s); pspace_distinct' s; pspace_aligned' s; is_aligned ptr pdBits; x && ~~ mask (vs_ptr_align x2) = y && ~~ mask (vs_ptr_align x2); ksPSpace b = (\<lambda>x. if x \<in> {ptr + (pptrBase >> 20 << 2)..ptr + (2 ^ pdBits - 1)} then ksPSpace s ((x && mask pdBits) + armKSGlobalPD (ksArchState s)) else ksPSpace s x); y \<in> {ptr + (pptrBase >> 20 << 2)..ptr + (2 ^ pdBits - 1)}; x \<in> {ptr + (pptrBase >> 20 << 2)..ptr + (2 ^ pdBits - 1)}\<rbrakk> \<Longrightarrow> 2 \<le> pdBits
 2. \<And>s b x y x2. \<lbrakk>vs_valid_duplicates' (ksPSpace s); pspace_distinct' s; pspace_aligned' s; is_aligned (armKSGlobalPD (ksArchState s)) pdBits; is_aligned ptr pdBits; x && ~~ mask (vs_ptr_align x2) = y && ~~ mask (vs_ptr_align x2); ksPSpace b = (\<lambda>x. if x \<in> {ptr + (pptrBase >> 20 << 2)..ptr + (2 ^ pdBits - 1)} then ksPSpace s ((x && mask pdBits) + armKSGlobalPD (ksArchState s)) else ksPSpace s x); y \<in> {ptr + (pptrBase >> 20 << 2)..ptr + (2 ^ pdBits - 1)}; x \<in> {ptr + (pptrBase >> 20 << 2)..ptr + (2 ^ pdBits - 1)}\<rbrakk> \<Longrightarrow> 2 \<le> 2
 3. \<And>s b x y x2. \<lbrakk>vs_valid_duplicates' (ksPSpace s); pspace_distinct' s; pspace_aligned' s; is_aligned (armKSGlobalPD (ksArchState s)) pdBits; is_aligned ptr pdBits; is_aligned y 2; x && ~~ mask (vs_ptr_align x2) = y && ~~ mask (vs_ptr_align x2); ksPSpace b = (\<lambda>x. if x \<in> {ptr + (pptrBase >> 20 << 2)..ptr + (2 ^ pdBits - 1)} then ksPSpace s ((x && mask pdBits) + armKSGlobalPD (ksArchState s)) else ksPSpace s x); y \<in> {ptr + (pptrBase >> 20 << 2)..ptr + (2 ^ pdBits - 1)}; x \<in> {ptr + (pptrBase >> 20 << 2)..ptr + (2 ^ pdBits - 1)}\<rbrakk> \<Longrightarrow> (x && mask pdBits) + armKSGlobalPD (ksArchState s) && ~~ mask (vs_ptr_align x2) = (y && mask pdBits) + armKSGlobalPD (ksArchState s) && ~~ mask (vs_ptr_align x2)
 4. \<And>s b x y x2. \<lbrakk>vs_valid_duplicates' (ksPSpace s); pspace_distinct' s; pspace_aligned' s; is_aligned (armKSGlobalPD (ksArchState s)) pdBits; is_aligned ptr pdBits; is_aligned y 2; x && ~~ mask (vs_ptr_align x2) = y && ~~ mask (vs_ptr_align x2); ksPSpace b = (\<lambda>x. if x \<in> {ptr + (pptrBase >> 20 << 2)..ptr + (2 ^ pdBits - 1)} then ksPSpace s ((x && mask pdBits) + armKSGlobalPD (ksArchState s)) else ksPSpace s x); y \<in> {ptr + (pptrBase >> 20 << 2)..ptr + (2 ^ pdBits - 1)}; x \<in> {ptr + (pptrBase >> 20 << 2)..ptr + (2 ^ pdBits - 1)}\<rbrakk> \<Longrightarrow> vs_valid_duplicates' (ksPSpace s)
 5. \<And>s b x y x2. \<lbrakk>vs_valid_duplicates' (ksPSpace s); pspace_distinct' s; pspace_aligned' s; is_aligned (armKSGlobalPD (ksArchState s)) pdBits; is_aligned ptr pdBits; is_aligned y 2; x && ~~ mask (vs_ptr_align x2) = y && ~~ mask (vs_ptr_align x2); ksPSpace b = (\<lambda>x. if x \<in> {ptr + (pptrBase >> 20 << 2)..ptr + (2 ^ pdBits - 1)} then ksPSpace s ((x && mask pdBits) + armKSGlobalPD (ksArchState s)) else ksPSpace s x); y \<in> {ptr + (pptrBase >> 20 << 2)..ptr + (2 ^ pdBits - 1)}; x \<in> {ptr + (pptrBase >> 20 << 2)..ptr + (2 ^ pdBits - 1)}; ksPSpace s ((y && mask pdBits) + armKSGlobalPD (ksArchState s)) = Some x2\<rbrakk> \<Longrightarrow> Some x2 = ksPSpace s ((y && mask pdBits) + armKSGlobalPD (ksArchState s))
 6. \<And>s b x y x2. \<lbrakk>vs_valid_duplicates' (ksPSpace s); pspace_distinct' s; pspace_aligned' s; is_aligned (armKSGlobalPD (ksArchState s)) pdBits; is_aligned ptr pdBits; (if x \<in> {ptr + (pptrBase >> 20 << 2)..ptr + (2 ^ pdBits - 1)} then ksPSpace s ((x && mask pdBits) + armKSGlobalPD (ksArchState s)) else ksPSpace s x) = Some x2; is_aligned y 2; x && ~~ mask (vs_ptr_align x2) = y && ~~ mask (vs_ptr_align x2); ksPSpace b = (\<lambda>x. if x \<in> {ptr + (pptrBase >> 20 << 2)..ptr + (2 ^ pdBits - 1)} then ksPSpace s ((x && mask pdBits) + armKSGlobalPD (ksArchState s)) else ksPSpace s x)\<rbrakk> \<Longrightarrow> y \<notin> {ptr + (pptrBase >> 20 << 2)..ptr + (2 ^ pdBits - 1)} \<longrightarrow> Some x2 = ksPSpace s y proof (prove)
goal (5 subgoals):
 1. \<And>s b x y x2. \<lbrakk>vs_valid_duplicates' (ksPSpace s); pspace_distinct' s; pspace_aligned' s; is_aligned (armKSGlobalPD (ksArchState s)) pdBits; is_aligned ptr pdBits; x && ~~ mask (vs_ptr_align x2) = y && ~~ mask (vs_ptr_align x2); ksPSpace b = (\<lambda>x. if x \<in> {ptr + (pptrBase >> 20 << 2)..ptr + (2 ^ pdBits - 1)} then ksPSpace s ((x && mask pdBits) + armKSGlobalPD (ksArchState s)) else ksPSpace s x); y \<in> {ptr + (pptrBase >> 20 << 2)..ptr + (2 ^ pdBits - 1)}; x \<in> {ptr + (pptrBase >> 20 << 2)..ptr + (2 ^ pdBits - 1)}\<rbrakk> \<Longrightarrow> 2 \<le> 2
 2. \<And>s b x y x2. \<lbrakk>vs_valid_duplicates' (ksPSpace s); pspace_distinct' s; pspace_aligned' s; is_aligned (armKSGlobalPD (ksArchState s)) pdBits; is_aligned ptr pdBits; is_aligned y 2; x && ~~ mask (vs_ptr_align x2) = y && ~~ mask (vs_ptr_align x2); ksPSpace b = (\<lambda>x. if x \<in> {ptr + (pptrBase >> 20 << 2)..ptr + (2 ^ pdBits - 1)} then ksPSpace s ((x && mask pdBits) + armKSGlobalPD (ksArchState s)) else ksPSpace s x); y \<in> {ptr + (pptrBase >> 20 << 2)..ptr + (2 ^ pdBits - 1)}; x \<in> {ptr + (pptrBase >> 20 << 2)..ptr + (2 ^ pdBits - 1)}\<rbrakk> \<Longrightarrow> (x && mask pdBits) + armKSGlobalPD (ksArchState s) && ~~ mask (vs_ptr_align x2) = (y && mask pdBits) + armKSGlobalPD (ksArchState s) && ~~ mask (vs_ptr_align x2)
 3. \<And>s b x y x2. \<lbrakk>vs_valid_duplicates' (ksPSpace s); pspace_distinct' s; pspace_aligned' s; is_aligned (armKSGlobalPD (ksArchState s)) pdBits; is_aligned ptr pdBits; is_aligned y 2; x && ~~ mask (vs_ptr_align x2) = y && ~~ mask (vs_ptr_align x2); ksPSpace b = (\<lambda>x. if x \<in> {ptr + (pptrBase >> 20 << 2)..ptr + (2 ^ pdBits - 1)} then ksPSpace s ((x && mask pdBits) + armKSGlobalPD (ksArchState s)) else ksPSpace s x); y \<in> {ptr + (pptrBase >> 20 << 2)..ptr + (2 ^ pdBits - 1)}; x \<in> {ptr + (pptrBase >> 20 << 2)..ptr + (2 ^ pdBits - 1)}\<rbrakk> \<Longrightarrow> vs_valid_duplicates' (ksPSpace s)
 4. \<And>s b x y x2. \<lbrakk>vs_valid_duplicates' (ksPSpace s); pspace_distinct' s; pspace_aligned' s; is_aligned (armKSGlobalPD (ksArchState s)) pdBits; is_aligned ptr pdBits; is_aligned y 2; x && ~~ mask (vs_ptr_align x2) = y && ~~ mask (vs_ptr_align x2); ksPSpace b = (\<lambda>x. if x \<in> {ptr + (pptrBase >> 20 << 2)..ptr + (2 ^ pdBits - 1)} then ksPSpace s ((x && mask pdBits) + armKSGlobalPD (ksArchState s)) else ksPSpace s x); y \<in> {ptr + (pptrBase >> 20 << 2)..ptr + (2 ^ pdBits - 1)}; x \<in> {ptr + (pptrBase >> 20 << 2)..ptr + (2 ^ pdBits - 1)}; ksPSpace s ((y && mask pdBits) + armKSGlobalPD (ksArchState s)) = Some x2\<rbrakk> \<Longrightarrow> Some x2 = ksPSpace s ((y && mask pdBits) + armKSGlobalPD (ksArchState s))
 5. \<And>s b x y x2. \<lbrakk>vs_valid_duplicates' (ksPSpace s); pspace_distinct' s; pspace_aligned' s; is_aligned (armKSGlobalPD (ksArchState s)) pdBits; is_aligned ptr pdBits; (if x \<in> {ptr + (pptrBase >> 20 << 2)..ptr + (2 ^ pdBits - 1)} then ksPSpace s ((x && mask pdBits) + armKSGlobalPD (ksArchState s)) else ksPSpace s x) = Some x2; is_aligned y 2; x && ~~ mask (vs_ptr_align x2) = y && ~~ mask (vs_ptr_align x2); ksPSpace b = (\<lambda>x. if x \<in> {ptr + (pptrBase >> 20 << 2)..ptr + (2 ^ pdBits - 1)} then ksPSpace s ((x && mask pdBits) + armKSGlobalPD (ksArchState s)) else ksPSpace s x)\<rbrakk> \<Longrightarrow> y \<notin> {ptr + (pptrBase >> 20 << 2)..ptr + (2 ^ pdBits - 1)} \<longrightarrow> Some x2 = ksPSpace s y proof (prove)
goal (4 subgoals):
 1. \<And>s b x y x2. \<lbrakk>vs_valid_duplicates' (ksPSpace s); pspace_distinct' s; pspace_aligned' s; is_aligned (armKSGlobalPD (ksArchState s)) pdBits; is_aligned ptr pdBits; is_aligned y 2; x && ~~ mask (vs_ptr_align x2) = y && ~~ mask (vs_ptr_align x2); ksPSpace b = (\<lambda>x. if x \<in> {ptr + (pptrBase >> 20 << 2)..ptr + (2 ^ pdBits - 1)} then ksPSpace s ((x && mask pdBits) + armKSGlobalPD (ksArchState s)) else ksPSpace s x); y \<in> {ptr + (pptrBase >> 20 << 2)..ptr + (2 ^ pdBits - 1)}; x \<in> {ptr + (pptrBase >> 20 << 2)..ptr + (2 ^ pdBits - 1)}\<rbrakk> \<Longrightarrow> (x && mask pdBits) + armKSGlobalPD (ksArchState s) && ~~ mask (vs_ptr_align x2) = (y && mask pdBits) + armKSGlobalPD (ksArchState s) && ~~ mask (vs_ptr_align x2)
 2. \<And>s b x y x2. \<lbrakk>vs_valid_duplicates' (ksPSpace s); pspace_distinct' s; pspace_aligned' s; is_aligned (armKSGlobalPD (ksArchState s)) pdBits; is_aligned ptr pdBits; is_aligned y 2; x && ~~ mask (vs_ptr_align x2) = y && ~~ mask (vs_ptr_align x2); ksPSpace b = (\<lambda>x. if x \<in> {ptr + (pptrBase >> 20 << 2)..ptr + (2 ^ pdBits - 1)} then ksPSpace s ((x && mask pdBits) + armKSGlobalPD (ksArchState s)) else ksPSpace s x); y \<in> {ptr + (pptrBase >> 20 << 2)..ptr + (2 ^ pdBits - 1)}; x \<in> {ptr + (pptrBase >> 20 << 2)..ptr + (2 ^ pdBits - 1)}\<rbrakk> \<Longrightarrow> vs_valid_duplicates' (ksPSpace s)
 3. \<And>s b x y x2. \<lbrakk>vs_valid_duplicates' (ksPSpace s); pspace_distinct' s; pspace_aligned' s; is_aligned (armKSGlobalPD (ksArchState s)) pdBits; is_aligned ptr pdBits; is_aligned y 2; x && ~~ mask (vs_ptr_align x2) = y && ~~ mask (vs_ptr_align x2); ksPSpace b = (\<lambda>x. if x \<in> {ptr + (pptrBase >> 20 << 2)..ptr + (2 ^ pdBits - 1)} then ksPSpace s ((x && mask pdBits) + armKSGlobalPD (ksArchState s)) else ksPSpace s x); y \<in> {ptr + (pptrBase >> 20 << 2)..ptr + (2 ^ pdBits - 1)}; x \<in> {ptr + (pptrBase >> 20 << 2)..ptr + (2 ^ pdBits - 1)}; ksPSpace s ((y && mask pdBits) + armKSGlobalPD (ksArchState s)) = Some x2\<rbrakk> \<Longrightarrow> Some x2 = ksPSpace s ((y && mask pdBits) + armKSGlobalPD (ksArchState s))
 4. \<And>s b x y x2. \<lbrakk>vs_valid_duplicates' (ksPSpace s); pspace_distinct' s; pspace_aligned' s; is_aligned (armKSGlobalPD (ksArchState s)) pdBits; is_aligned ptr pdBits; (if x \<in> {ptr + (pptrBase >> 20 << 2)..ptr + (2 ^ pdBits - 1)} then ksPSpace s ((x && mask pdBits) + armKSGlobalPD (ksArchState s)) else ksPSpace s x) = Some x2; is_aligned y 2; x && ~~ mask (vs_ptr_align x2) = y && ~~ mask (vs_ptr_align x2); ksPSpace b = (\<lambda>x. if x \<in> {ptr + (pptrBase >> 20 << 2)..ptr + (2 ^ pdBits - 1)} then ksPSpace s ((x && mask pdBits) + armKSGlobalPD (ksArchState s)) else ksPSpace s x)\<rbrakk> \<Longrightarrow> y \<notin> {ptr + (pptrBase >> 20 << 2)..ptr + (2 ^ pdBits - 1)} \<longrightarrow> Some x2 = ksPSpace s y proof (prove)
goal (4 subgoals):
 1. \<And>s b x y x2. \<lbrakk>vs_valid_duplicates' (ksPSpace s); pspace_distinct' s; pspace_aligned' s; is_aligned (armKSGlobalPD (ksArchState s)) pdBits; is_aligned ptr pdBits; is_aligned y 2; x && ~~ mask (vs_ptr_align x2) = y && ~~ mask (vs_ptr_align x2); ksPSpace b = (\<lambda>x. if x \<in> {ptr + (pptrBase >> 20 << 2)..ptr + (2 ^ pdBits - 1)} then ksPSpace s ((x && mask pdBits) + armKSGlobalPD (ksArchState s)) else ksPSpace s x); y \<in> {ptr + (pptrBase >> 20 << 2)..ptr + (2 ^ pdBits - 1)}; x \<in> {ptr + (pptrBase >> 20 << 2)..ptr + (2 ^ pdBits - 1)}; (x && mask pdBits) + armKSGlobalPD (ksArchState s) && ~~ mask (vs_ptr_align x2) = ((x && mask pdBits) && ~~ mask (vs_ptr_align x2)) + armKSGlobalPD (ksArchState s)\<rbrakk> \<Longrightarrow> (x && mask pdBits) + armKSGlobalPD (ksArchState s) && ~~ mask (vs_ptr_align x2) = (y && mask pdBits) + armKSGlobalPD (ksArchState s) && ~~ mask (vs_ptr_align x2)
 2. \<And>s b x y x2. \<lbrakk>vs_valid_duplicates' (ksPSpace s); pspace_distinct' s; pspace_aligned' s; is_aligned (armKSGlobalPD (ksArchState s)) pdBits; is_aligned ptr pdBits; is_aligned y 2; x && ~~ mask (vs_ptr_align x2) = y && ~~ mask (vs_ptr_align x2); ksPSpace b = (\<lambda>x. if x \<in> {ptr + (pptrBase >> 20 << 2)..ptr + (2 ^ pdBits - 1)} then ksPSpace s ((x && mask pdBits) + armKSGlobalPD (ksArchState s)) else ksPSpace s x); y \<in> {ptr + (pptrBase >> 20 << 2)..ptr + (2 ^ pdBits - 1)}; x \<in> {ptr + (pptrBase >> 20 << 2)..ptr + (2 ^ pdBits - 1)}\<rbrakk> \<Longrightarrow> vs_valid_duplicates' (ksPSpace s)
 3. \<And>s b x y x2. \<lbrakk>vs_valid_duplicates' (ksPSpace s); pspace_distinct' s; pspace_aligned' s; is_aligned (armKSGlobalPD (ksArchState s)) pdBits; is_aligned ptr pdBits; is_aligned y 2; x && ~~ mask (vs_ptr_align x2) = y && ~~ mask (vs_ptr_align x2); ksPSpace b = (\<lambda>x. if x \<in> {ptr + (pptrBase >> 20 << 2)..ptr + (2 ^ pdBits - 1)} then ksPSpace s ((x && mask pdBits) + armKSGlobalPD (ksArchState s)) else ksPSpace s x); y \<in> {ptr + (pptrBase >> 20 << 2)..ptr + (2 ^ pdBits - 1)}; x \<in> {ptr + (pptrBase >> 20 << 2)..ptr + (2 ^ pdBits - 1)}; ksPSpace s ((y && mask pdBits) + armKSGlobalPD (ksArchState s)) = Some x2\<rbrakk> \<Longrightarrow> Some x2 = ksPSpace s ((y && mask pdBits) + armKSGlobalPD (ksArchState s))
 4. \<And>s b x y x2. \<lbrakk>vs_valid_duplicates' (ksPSpace s); pspace_distinct' s; pspace_aligned' s; is_aligned (armKSGlobalPD (ksArchState s)) pdBits; is_aligned ptr pdBits; (if x \<in> {ptr + (pptrBase >> 20 << 2)..ptr + (2 ^ pdBits - 1)} then ksPSpace s ((x && mask pdBits) + armKSGlobalPD (ksArchState s)) else ksPSpace s x) = Some x2; is_aligned y 2; x && ~~ mask (vs_ptr_align x2) = y && ~~ mask (vs_ptr_align x2); ksPSpace b = (\<lambda>x. if x \<in> {ptr + (pptrBase >> 20 << 2)..ptr + (2 ^ pdBits - 1)} then ksPSpace s ((x && mask pdBits) + armKSGlobalPD (ksArchState s)) else ksPSpace s x)\<rbrakk> \<Longrightarrow> y \<notin> {ptr + (pptrBase >> 20 << 2)..ptr + (2 ^ pdBits - 1)} \<longrightarrow> Some x2 = ksPSpace s y proof (prove)
goal (4 subgoals):
 1. \<And>s b x y x2. \<lbrakk>vs_valid_duplicates' (ksPSpace s); pspace_distinct' s; pspace_aligned' s; is_aligned ptr pdBits; is_aligned y 2; x && ~~ mask (vs_ptr_align x2) = y && ~~ mask (vs_ptr_align x2); ksPSpace b = (\<lambda>x. if x \<in> {ptr + (pptrBase >> 20 << 2)..ptr + (2 ^ pdBits - 1)} then ksPSpace s ((x && mask pdBits) + armKSGlobalPD (ksArchState s)) else ksPSpace s x); y \<in> {ptr + (pptrBase >> 20 << 2)..ptr + (2 ^ pdBits - 1)}; x \<in> {ptr + (pptrBase >> 20 << 2)..ptr + (2 ^ pdBits - 1)}; (x && mask pdBits) + armKSGlobalPD (ksArchState s) && ~~ mask (vs_ptr_align x2) = ((x && mask pdBits) && ~~ mask (vs_ptr_align x2)) + armKSGlobalPD (ksArchState s); (y && mask pdBits) + armKSGlobalPD (ksArchState s) && ~~ mask (vs_ptr_align x2) = ((y && mask pdBits) && ~~ mask (vs_ptr_align x2)) + armKSGlobalPD (ksArchState s)\<rbrakk> \<Longrightarrow> (x && mask pdBits) + armKSGlobalPD (ksArchState s) && ~~ mask (vs_ptr_align x2) = (y && mask pdBits) + armKSGlobalPD (ksArchState s) && ~~ mask (vs_ptr_align x2)
 2. \<And>s b x y x2. \<lbrakk>vs_valid_duplicates' (ksPSpace s); pspace_distinct' s; pspace_aligned' s; is_aligned (armKSGlobalPD (ksArchState s)) pdBits; is_aligned ptr pdBits; is_aligned y 2; x && ~~ mask (vs_ptr_align x2) = y && ~~ mask (vs_ptr_align x2); ksPSpace b = (\<lambda>x. if x \<in> {ptr + (pptrBase >> 20 << 2)..ptr + (2 ^ pdBits - 1)} then ksPSpace s ((x && mask pdBits) + armKSGlobalPD (ksArchState s)) else ksPSpace s x); y \<in> {ptr + (pptrBase >> 20 << 2)..ptr + (2 ^ pdBits - 1)}; x \<in> {ptr + (pptrBase >> 20 << 2)..ptr + (2 ^ pdBits - 1)}\<rbrakk> \<Longrightarrow> vs_valid_duplicates' (ksPSpace s)
 3. \<And>s b x y x2. \<lbrakk>vs_valid_duplicates' (ksPSpace s); pspace_distinct' s; pspace_aligned' s; is_aligned (armKSGlobalPD (ksArchState s)) pdBits; is_aligned ptr pdBits; is_aligned y 2; x && ~~ mask (vs_ptr_align x2) = y && ~~ mask (vs_ptr_align x2); ksPSpace b = (\<lambda>x. if x \<in> {ptr + (pptrBase >> 20 << 2)..ptr + (2 ^ pdBits - 1)} then ksPSpace s ((x && mask pdBits) + armKSGlobalPD (ksArchState s)) else ksPSpace s x); y \<in> {ptr + (pptrBase >> 20 << 2)..ptr + (2 ^ pdBits - 1)}; x \<in> {ptr + (pptrBase >> 20 << 2)..ptr + (2 ^ pdBits - 1)}; ksPSpace s ((y && mask pdBits) + armKSGlobalPD (ksArchState s)) = Some x2\<rbrakk> \<Longrightarrow> Some x2 = ksPSpace s ((y && mask pdBits) + armKSGlobalPD (ksArchState s))
 4. \<And>s b x y x2. \<lbrakk>vs_valid_duplicates' (ksPSpace s); pspace_distinct' s; pspace_aligned' s; is_aligned (armKSGlobalPD (ksArchState s)) pdBits; is_aligned ptr pdBits; (if x \<in> {ptr + (pptrBase >> 20 << 2)..ptr + (2 ^ pdBits - 1)} then ksPSpace s ((x && mask pdBits) + armKSGlobalPD (ksArchState s)) else ksPSpace s x) = Some x2; is_aligned y 2; x && ~~ mask (vs_ptr_align x2) = y && ~~ mask (vs_ptr_align x2); ksPSpace b = (\<lambda>x. if x \<in> {ptr + (pptrBase >> 20 << 2)..ptr + (2 ^ pdBits - 1)} then ksPSpace s ((x && mask pdBits) + armKSGlobalPD (ksArchState s)) else ksPSpace s x)\<rbrakk> \<Longrightarrow> y \<notin> {ptr + (pptrBase >> 20 << 2)..ptr + (2 ^ pdBits - 1)} \<longrightarrow> Some x2 = ksPSpace s y proof (prove)
goal (3 subgoals):
 1. \<And>s b x y x2. \<lbrakk>vs_valid_duplicates' (ksPSpace s); pspace_distinct' s; pspace_aligned' s; is_aligned (armKSGlobalPD (ksArchState s)) pdBits; is_aligned ptr pdBits; is_aligned y 2; x && ~~ mask (vs_ptr_align x2) = y && ~~ mask (vs_ptr_align x2); ksPSpace b = (\<lambda>x. if x \<in> {ptr + (pptrBase >> 20 << 2)..ptr + (2 ^ pdBits - 1)} then ksPSpace s ((x && mask pdBits) + armKSGlobalPD (ksArchState s)) else ksPSpace s x); y \<in> {ptr + (pptrBase >> 20 << 2)..ptr + (2 ^ pdBits - 1)}; x \<in> {ptr + (pptrBase >> 20 << 2)..ptr + (2 ^ pdBits - 1)}\<rbrakk> \<Longrightarrow> vs_valid_duplicates' (ksPSpace s)
 2. \<And>s b x y x2. \<lbrakk>vs_valid_duplicates' (ksPSpace s); pspace_distinct' s; pspace_aligned' s; is_aligned (armKSGlobalPD (ksArchState s)) pdBits; is_aligned ptr pdBits; is_aligned y 2; x && ~~ mask (vs_ptr_align x2) = y && ~~ mask (vs_ptr_align x2); ksPSpace b = (\<lambda>x. if x \<in> {ptr + (pptrBase >> 20 << 2)..ptr + (2 ^ pdBits - 1)} then ksPSpace s ((x && mask pdBits) + armKSGlobalPD (ksArchState s)) else ksPSpace s x); y \<in> {ptr + (pptrBase >> 20 << 2)..ptr + (2 ^ pdBits - 1)}; x \<in> {ptr + (pptrBase >> 20 << 2)..ptr + (2 ^ pdBits - 1)}; ksPSpace s ((y && mask pdBits) + armKSGlobalPD (ksArchState s)) = Some x2\<rbrakk> \<Longrightarrow> Some x2 = ksPSpace s ((y && mask pdBits) + armKSGlobalPD (ksArchState s))
 3. \<And>s b x y x2. \<lbrakk>vs_valid_duplicates' (ksPSpace s); pspace_distinct' s; pspace_aligned' s; is_aligned (armKSGlobalPD (ksArchState s)) pdBits; is_aligned ptr pdBits; (if x \<in> {ptr + (pptrBase >> 20 << 2)..ptr + (2 ^ pdBits - 1)} then ksPSpace s ((x && mask pdBits) + armKSGlobalPD (ksArchState s)) else ksPSpace s x) = Some x2; is_aligned y 2; x && ~~ mask (vs_ptr_align x2) = y && ~~ mask (vs_ptr_align x2); ksPSpace b = (\<lambda>x. if x \<in> {ptr + (pptrBase >> 20 << 2)..ptr + (2 ^ pdBits - 1)} then ksPSpace s ((x && mask pdBits) + armKSGlobalPD (ksArchState s)) else ksPSpace s x)\<rbrakk> \<Longrightarrow> y \<notin> {ptr + (pptrBase >> 20 << 2)..ptr + (2 ^ pdBits - 1)} \<longrightarrow> Some x2 = ksPSpace s y proof (prove)
goal (2 subgoals):
 1. \<And>s b x y x2. \<lbrakk>vs_valid_duplicates' (ksPSpace s); pspace_distinct' s; pspace_aligned' s; is_aligned (armKSGlobalPD (ksArchState s)) pdBits; is_aligned ptr pdBits; is_aligned y 2; x && ~~ mask (vs_ptr_align x2) = y && ~~ mask (vs_ptr_align x2); ksPSpace b = (\<lambda>x. if x \<in> {ptr + (pptrBase >> 20 << 2)..ptr + (2 ^ pdBits - 1)} then ksPSpace s ((x && mask pdBits) + armKSGlobalPD (ksArchState s)) else ksPSpace s x); y \<in> {ptr + (pptrBase >> 20 << 2)..ptr + (2 ^ pdBits - 1)}; x \<in> {ptr + (pptrBase >> 20 << 2)..ptr + (2 ^ pdBits - 1)}; ksPSpace s ((y && mask pdBits) + armKSGlobalPD (ksArchState s)) = Some x2\<rbrakk> \<Longrightarrow> Some x2 = ksPSpace s ((y && mask pdBits) + armKSGlobalPD (ksArchState s))
 2. \<And>s b x y x2. \<lbrakk>vs_valid_duplicates' (ksPSpace s); pspace_distinct' s; pspace_aligned' s; is_aligned (armKSGlobalPD (ksArchState s)) pdBits; is_aligned ptr pdBits; (if x \<in> {ptr + (pptrBase >> 20 << 2)..ptr + (2 ^ pdBits - 1)} then ksPSpace s ((x && mask pdBits) + armKSGlobalPD (ksArchState s)) else ksPSpace s x) = Some x2; is_aligned y 2; x && ~~ mask (vs_ptr_align x2) = y && ~~ mask (vs_ptr_align x2); ksPSpace b = (\<lambda>x. if x \<in> {ptr + (pptrBase >> 20 << 2)..ptr + (2 ^ pdBits - 1)} then ksPSpace s ((x && mask pdBits) + armKSGlobalPD (ksArchState s)) else ksPSpace s x)\<rbrakk> \<Longrightarrow> y \<notin> {ptr + (pptrBase >> 20 << 2)..ptr + (2 ^ pdBits - 1)} \<longrightarrow> Some x2 = ksPSpace s y proof (prove)
goal (1 subgoal):
 1. \<And>s b x y x2. \<lbrakk>vs_valid_duplicates' (ksPSpace s); pspace_distinct' s; pspace_aligned' s; is_aligned (armKSGlobalPD (ksArchState s)) pdBits; is_aligned ptr pdBits; (if x \<in> {ptr + (pptrBase >> 20 << 2)..ptr + (2 ^ pdBits - 1)} then ksPSpace s ((x && mask pdBits) + armKSGlobalPD (ksArchState s)) else ksPSpace s x) = Some x2; is_aligned y 2; x && ~~ mask (vs_ptr_align x2) = y && ~~ mask (vs_ptr_align x2); ksPSpace b = (\<lambda>x. if x \<in> {ptr + (pptrBase >> 20 << 2)..ptr + (2 ^ pdBits - 1)} then ksPSpace s ((x && mask pdBits) + armKSGlobalPD (ksArchState s)) else ksPSpace s x)\<rbrakk> \<Longrightarrow> y \<notin> {ptr + (pptrBase >> 20 << 2)..ptr + (2 ^ pdBits - 1)} \<longrightarrow> Some x2 = ksPSpace s y proof (prove)
goal (2 subgoals):
 1. \<And>s b x y x2. \<lbrakk>is_aligned y 2; x && ~~ mask (vs_ptr_align x2) = y && ~~ mask (vs_ptr_align x2); ksPSpace b = (\<lambda>x. if x \<in> {ptr + (pptrBase >> 20 << 2)..ptr + (2 ^ pdBits - 1)} then ksPSpace s ((x && mask pdBits) + armKSGlobalPD (ksArchState s)) else ksPSpace s x); vs_valid_duplicates' (ksPSpace s); pspace_distinct' s; pspace_aligned' s; is_aligned (armKSGlobalPD (ksArchState s)) pdBits; is_aligned ptr pdBits; x \<in> {ptr + (pptrBase >> 20 << 2)..ptr + (2 ^ pdBits - 1)}; ksPSpace s ((x && mask pdBits) + armKSGlobalPD (ksArchState s)) = Some x2; y \<notin> {ptr + (pptrBase >> 20 << 2)..ptr + (2 ^ pdBits - 1)}\<rbrakk> \<Longrightarrow> Some x2 = ksPSpace s y
 2. \<And>s b x y x2. \<lbrakk>is_aligned y 2; x && ~~ mask (vs_ptr_align x2) = y && ~~ mask (vs_ptr_align x2); ksPSpace b = (\<lambda>x. if x \<in> {ptr + (pptrBase >> 20 << 2)..ptr + (2 ^ pdBits - 1)} then ksPSpace s ((x && mask pdBits) + armKSGlobalPD (ksArchState s)) else ksPSpace s x); vs_valid_duplicates' (ksPSpace s); pspace_distinct' s; pspace_aligned' s; is_aligned (armKSGlobalPD (ksArchState s)) pdBits; is_aligned ptr pdBits; x \<notin> {ptr + (pptrBase >> 20 << 2)..ptr + (2 ^ pdBits - 1)}; ksPSpace s x = Some x2; y \<notin> {ptr + (pptrBase >> 20 << 2)..ptr + (2 ^ pdBits - 1)}\<rbrakk> \<Longrightarrow> Some x2 = ksPSpace s y proof (prove)
goal (4 subgoals):
 1. \<And>s b x y x2. \<lbrakk>is_aligned y 2; ksPSpace b = (\<lambda>x. if x \<in> {ptr + (pptrBase >> 20 << 2)..ptr + (2 ^ pdBits - 1)} then ksPSpace s ((x && mask pdBits) + armKSGlobalPD (ksArchState s)) else ksPSpace s x); vs_valid_duplicates' (ksPSpace s); pspace_distinct' s; pspace_aligned' s; is_aligned (armKSGlobalPD (ksArchState s)) pdBits; is_aligned ptr pdBits; x \<in> {ptr + (pptrBase >> 20 << 2)..ptr + (2 ^ pdBits - 1)}; ksPSpace s ((x && mask pdBits) + armKSGlobalPD (ksArchState s)) = Some x2; y \<notin> {ptr + (pptrBase >> 20 << 2)..ptr + (2 ^ pdBits - 1)}\<rbrakk> \<Longrightarrow> is_aligned ptr pdBits
 2. \<And>s b x y x2. \<lbrakk>is_aligned y 2; ksPSpace b = (\<lambda>x. if x \<in> {ptr + (pptrBase >> 20 << 2)..ptr + (2 ^ pdBits - 1)} then ksPSpace s ((x && mask pdBits) + armKSGlobalPD (ksArchState s)) else ksPSpace s x); vs_valid_duplicates' (ksPSpace s); pspace_distinct' s; pspace_aligned' s; is_aligned (armKSGlobalPD (ksArchState s)) pdBits; is_aligned ptr pdBits; x \<in> {ptr + (pptrBase >> 20 << 2)..ptr + (2 ^ pdBits - 1)}; ksPSpace s ((x && mask pdBits) + armKSGlobalPD (ksArchState s)) = Some x2; y \<notin> {ptr + (pptrBase >> 20 << 2)..ptr + (2 ^ pdBits - 1)}\<rbrakk> \<Longrightarrow> x \<in> {ptr + (pptrBase >> 20 << 2)..ptr + (2 ^ pdBits - 1)}
 3. \<And>s b x y x2. \<lbrakk>is_aligned y 2; ksPSpace b = (\<lambda>x. if x \<in> {ptr + (pptrBase >> 20 << 2)..ptr + (2 ^ pdBits - 1)} then ksPSpace s ((x && mask pdBits) + armKSGlobalPD (ksArchState s)) else ksPSpace s x); vs_valid_duplicates' (ksPSpace s); pspace_distinct' s; pspace_aligned' s; is_aligned (armKSGlobalPD (ksArchState s)) pdBits; is_aligned ptr pdBits; x \<in> {ptr + (pptrBase >> 20 << 2)..ptr + (2 ^ pdBits - 1)}; ksPSpace s ((x && mask pdBits) + armKSGlobalPD (ksArchState s)) = Some x2; y \<notin> {ptr + (pptrBase >> 20 << 2)..ptr + (2 ^ pdBits - 1)}; y \<in> {ptr + (pptrBase >> 20 << 2)..ptr + (2 ^ pdBits - 1)}\<rbrakk> \<Longrightarrow> Some x2 = ksPSpace s y
 4. \<And>s b x y x2. \<lbrakk>is_aligned y 2; x && ~~ mask (vs_ptr_align x2) = y && ~~ mask (vs_ptr_align x2); ksPSpace b = (\<lambda>x. if x \<in> {ptr + (pptrBase >> 20 << 2)..ptr + (2 ^ pdBits - 1)} then ksPSpace s ((x && mask pdBits) + armKSGlobalPD (ksArchState s)) else ksPSpace s x); vs_valid_duplicates' (ksPSpace s); pspace_distinct' s; pspace_aligned' s; is_aligned (armKSGlobalPD (ksArchState s)) pdBits; is_aligned ptr pdBits; x \<notin> {ptr + (pptrBase >> 20 << 2)..ptr + (2 ^ pdBits - 1)}; ksPSpace s x = Some x2; y \<notin> {ptr + (pptrBase >> 20 << 2)..ptr + (2 ^ pdBits - 1)}\<rbrakk> \<Longrightarrow> Some x2 = ksPSpace s y proof (prove)
goal (3 subgoals):
 1. \<And>s b x y x2. \<lbrakk>is_aligned y 2; ksPSpace b = (\<lambda>x. if x \<in> {ptr + (pptrBase >> 20 << 2)..ptr + (2 ^ pdBits - 1)} then ksPSpace s ((x && mask pdBits) + armKSGlobalPD (ksArchState s)) else ksPSpace s x); vs_valid_duplicates' (ksPSpace s); pspace_distinct' s; pspace_aligned' s; is_aligned (armKSGlobalPD (ksArchState s)) pdBits; is_aligned ptr pdBits; x \<in> {ptr + (pptrBase >> 20 << 2)..ptr + (2 ^ pdBits - 1)}; ksPSpace s ((x && mask pdBits) + armKSGlobalPD (ksArchState s)) = Some x2; y \<notin> {ptr + (pptrBase >> 20 << 2)..ptr + (2 ^ pdBits - 1)}\<rbrakk> \<Longrightarrow> x \<in> {ptr + (pptrBase >> 20 << 2)..ptr + (2 ^ pdBits - 1)}
 2. \<And>s b x y x2. \<lbrakk>is_aligned y 2; ksPSpace b = (\<lambda>x. if x \<in> {ptr + (pptrBase >> 20 << 2)..ptr + (2 ^ pdBits - 1)} then ksPSpace s ((x && mask pdBits) + armKSGlobalPD (ksArchState s)) else ksPSpace s x); vs_valid_duplicates' (ksPSpace s); pspace_distinct' s; pspace_aligned' s; is_aligned (armKSGlobalPD (ksArchState s)) pdBits; is_aligned ptr pdBits; x \<in> {ptr + (pptrBase >> 20 << 2)..ptr + (2 ^ pdBits - 1)}; ksPSpace s ((x && mask pdBits) + armKSGlobalPD (ksArchState s)) = Some x2; y \<notin> {ptr + (pptrBase >> 20 << 2)..ptr + (2 ^ pdBits - 1)}; y \<in> {ptr + (pptrBase >> 20 << 2)..ptr + (2 ^ pdBits - 1)}\<rbrakk> \<Longrightarrow> Some x2 = ksPSpace s y
 3. \<And>s b x y x2. \<lbrakk>is_aligned y 2; x && ~~ mask (vs_ptr_align x2) = y && ~~ mask (vs_ptr_align x2); ksPSpace b = (\<lambda>x. if x \<in> {ptr + (pptrBase >> 20 << 2)..ptr + (2 ^ pdBits - 1)} then ksPSpace s ((x && mask pdBits) + armKSGlobalPD (ksArchState s)) else ksPSpace s x); vs_valid_duplicates' (ksPSpace s); pspace_distinct' s; pspace_aligned' s; is_aligned (armKSGlobalPD (ksArchState s)) pdBits; is_aligned ptr pdBits; x \<notin> {ptr + (pptrBase >> 20 << 2)..ptr + (2 ^ pdBits - 1)}; ksPSpace s x = Some x2; y \<notin> {ptr + (pptrBase >> 20 << 2)..ptr + (2 ^ pdBits - 1)}\<rbrakk> \<Longrightarrow> Some x2 = ksPSpace s y proof (prove)
goal (2 subgoals):
 1. \<And>s b x y x2. \<lbrakk>is_aligned y 2; ksPSpace b = (\<lambda>x. if x \<in> {ptr + (pptrBase >> 20 << 2)..ptr + (2 ^ pdBits - 1)} then ksPSpace s ((x && mask pdBits) + armKSGlobalPD (ksArchState s)) else ksPSpace s x); vs_valid_duplicates' (ksPSpace s); pspace_distinct' s; pspace_aligned' s; is_aligned (armKSGlobalPD (ksArchState s)) pdBits; is_aligned ptr pdBits; x \<in> {ptr + (pptrBase >> 20 << 2)..ptr + (2 ^ pdBits - 1)}; ksPSpace s ((x && mask pdBits) + armKSGlobalPD (ksArchState s)) = Some x2; y \<notin> {ptr + (pptrBase >> 20 << 2)..ptr + (2 ^ pdBits - 1)}; y \<in> {ptr + (pptrBase >> 20 << 2)..ptr + (2 ^ pdBits - 1)}\<rbrakk> \<Longrightarrow> Some x2 = ksPSpace s y
 2. \<And>s b x y x2. \<lbrakk>is_aligned y 2; x && ~~ mask (vs_ptr_align x2) = y && ~~ mask (vs_ptr_align x2); ksPSpace b = (\<lambda>x. if x \<in> {ptr + (pptrBase >> 20 << 2)..ptr + (2 ^ pdBits - 1)} then ksPSpace s ((x && mask pdBits) + armKSGlobalPD (ksArchState s)) else ksPSpace s x); vs_valid_duplicates' (ksPSpace s); pspace_distinct' s; pspace_aligned' s; is_aligned (armKSGlobalPD (ksArchState s)) pdBits; is_aligned ptr pdBits; x \<notin> {ptr + (pptrBase >> 20 << 2)..ptr + (2 ^ pdBits - 1)}; ksPSpace s x = Some x2; y \<notin> {ptr + (pptrBase >> 20 << 2)..ptr + (2 ^ pdBits - 1)}\<rbrakk> \<Longrightarrow> Some x2 = ksPSpace s y proof (prove)
goal (1 subgoal):
 1. \<And>s b x y x2. \<lbrakk>is_aligned y 2; x && ~~ mask (vs_ptr_align x2) = y && ~~ mask (vs_ptr_align x2); ksPSpace b = (\<lambda>x. if x \<in> {ptr + (pptrBase >> 20 << 2)..ptr + (2 ^ pdBits - 1)} then ksPSpace s ((x && mask pdBits) + armKSGlobalPD (ksArchState s)) else ksPSpace s x); vs_valid_duplicates' (ksPSpace s); pspace_distinct' s; pspace_aligned' s; is_aligned (armKSGlobalPD (ksArchState s)) pdBits; is_aligned ptr pdBits; x \<notin> {ptr + (pptrBase >> 20 << 2)..ptr + (2 ^ pdBits - 1)}; ksPSpace s x = Some x2; y \<notin> {ptr + (pptrBase >> 20 << 2)..ptr + (2 ^ pdBits - 1)}\<rbrakk> \<Longrightarrow> Some x2 = ksPSpace s y proof (prove)
goal (4 subgoals):
 1. \<And>s b x y x2. \<lbrakk>is_aligned y 2; x && ~~ mask (vs_ptr_align x2) = y && ~~ mask (vs_ptr_align x2); ksPSpace b = (\<lambda>x. if x \<in> {ptr + (pptrBase >> 20 << 2)..ptr + (2 ^ pdBits - 1)} then ksPSpace s ((x && mask pdBits) + armKSGlobalPD (ksArchState s)) else ksPSpace s x); vs_valid_duplicates' (ksPSpace s); pspace_distinct' s; pspace_aligned' s; is_aligned (armKSGlobalPD (ksArchState s)) pdBits; is_aligned ptr pdBits; x \<notin> {ptr + (pptrBase >> 20 << 2)..ptr + (2 ^ pdBits - 1)}; y \<notin> {ptr + (pptrBase >> 20 << 2)..ptr + (2 ^ pdBits - 1)}\<rbrakk> \<Longrightarrow> is_aligned y 2
 2. \<And>s b x y x2. \<lbrakk>is_aligned y 2; x && ~~ mask (vs_ptr_align x2) = y && ~~ mask (vs_ptr_align x2); ksPSpace b = (\<lambda>x. if x \<in> {ptr + (pptrBase >> 20 << 2)..ptr + (2 ^ pdBits - 1)} then ksPSpace s ((x && mask pdBits) + armKSGlobalPD (ksArchState s)) else ksPSpace s x); vs_valid_duplicates' (ksPSpace s); pspace_distinct' s; pspace_aligned' s; is_aligned (armKSGlobalPD (ksArchState s)) pdBits; is_aligned ptr pdBits; x \<notin> {ptr + (pptrBase >> 20 << 2)..ptr + (2 ^ pdBits - 1)}; y \<notin> {ptr + (pptrBase >> 20 << 2)..ptr + (2 ^ pdBits - 1)}\<rbrakk> \<Longrightarrow> x && ~~ mask (vs_ptr_align x2) = y && ~~ mask (vs_ptr_align x2)
 3. \<And>s b x y x2. \<lbrakk>is_aligned y 2; x && ~~ mask (vs_ptr_align x2) = y && ~~ mask (vs_ptr_align x2); ksPSpace b = (\<lambda>x. if x \<in> {ptr + (pptrBase >> 20 << 2)..ptr + (2 ^ pdBits - 1)} then ksPSpace s ((x && mask pdBits) + armKSGlobalPD (ksArchState s)) else ksPSpace s x); vs_valid_duplicates' (ksPSpace s); pspace_distinct' s; pspace_aligned' s; is_aligned (armKSGlobalPD (ksArchState s)) pdBits; is_aligned ptr pdBits; x \<notin> {ptr + (pptrBase >> 20 << 2)..ptr + (2 ^ pdBits - 1)}; y \<notin> {ptr + (pptrBase >> 20 << 2)..ptr + (2 ^ pdBits - 1)}\<rbrakk> \<Longrightarrow> vs_valid_duplicates' (ksPSpace s)
 4. \<And>s b x y x2. \<lbrakk>is_aligned y 2; x && ~~ mask (vs_ptr_align x2) = y && ~~ mask (vs_ptr_align x2); ksPSpace b = (\<lambda>x. if x \<in> {ptr + (pptrBase >> 20 << 2)..ptr + (2 ^ pdBits - 1)} then ksPSpace s ((x && mask pdBits) + armKSGlobalPD (ksArchState s)) else ksPSpace s x); vs_valid_duplicates' (ksPSpace s); pspace_distinct' s; pspace_aligned' s; is_aligned (armKSGlobalPD (ksArchState s)) pdBits; is_aligned ptr pdBits; x \<notin> {ptr + (pptrBase >> 20 << 2)..ptr + (2 ^ pdBits - 1)}; y \<notin> {ptr + (pptrBase >> 20 << 2)..ptr + (2 ^ pdBits - 1)}; ksPSpace s y = Some x2\<rbrakk> \<Longrightarrow> Some x2 = ksPSpace s y proof (prove)
goal:
No subgoals! proof (state)
this:
\<lbrace>(\<lambda>s. vs_valid_duplicates' (ksPSpace s)) and pspace_distinct' and pspace_aligned' and (\<lambda>s. is_aligned (armKSGlobalPD (ksArchState s)) pdBits) and K (is_aligned ptr pdBits)\<rbrace> copyGlobalMappings ptr \<lbrace>\<lambda>y s. vs_valid_duplicates' (ksPSpace s)\<rbrace>

goal:
No subgoals!