theory PageTableDuplicates

lemma copyGlobalMappings_ksPSpace_concrete:
  notes blah[simp del] =  atLeastatMost_subset_iff atLeastLessThan_iff
          Int_atLeastAtMost atLeastatMost_empty_iff split_paired_Ex
          atLeastAtMost_iff
  assumes monad: "(r, s') \<in> fst (copyGlobalMappings ptr s)"
  and ps: "pspace_distinct' s" "pspace_aligned' s"
  and al: "is_aligned (armKSGlobalPD (ksArchState s)) pdBits"
          "is_aligned ptr pdBits"
  shows   "ksPSpace s' = (\<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))" proof - have pd: "\<And>pd. \<lbrace>\<lambda>s. armKSGlobalPD (ksArchState s) = pd \<rbrace>
              copyGlobalMappings ptr \<lbrace>\<lambda>r s. armKSGlobalPD (ksArchState s) = pd \<rbrace>" by wp have comp: "\<And>x. x \<in> {ptr + (pptrBase >> 20 << 2)..ptr + 2 ^ pdBits - 1}
      \<Longrightarrow> ptr  + (x && mask pdBits) = x" using al apply - apply (rule mask_eqI[where n = pdBits]) apply (simp add:mask_add_aligned mask_twice pdBits_def pageBits_def) apply (subst mask_out_sub_mask) apply (simp add:mask_add_aligned mask_twice pdBits_def pageBits_def) apply (clarsimp simp:blah) apply (drule neg_mask_mono_le[where n = 14]) apply (drule neg_mask_mono_le[where n = 14]) apply (simp add:field_simps pdeBits_def) apply (frule_tac d1 = "0x3FFF" and p1="ptr" in is_aligned_add_helper[THEN conjunct2]) apply simp apply (frule_tac d1 = "pptrBase >> 20 << 2" and p1 = "ptr"
        in is_aligned_add_helper[THEN conjunct2]) apply (simp add: pptrBase_def) apply simp done show ?thesis using ps al monad apply - apply (rule ext) apply (frule_tac x = x in copyGlobalMappings_ksPSpaceD) apply simp+ apply (clarsimp split:if_splits) apply (frule_tac x = "(armKSGlobalPD (ksArchState s') + (x && mask pdBits))"
           in copyGlobalMappings_ksPSpaceD) apply simp+ apply (drule use_valid[OF _ pd]) apply simp apply (clarsimp split: if_splits simp: field_simps) apply (clarsimp simp: mask_add_aligned) apply (frule comp) apply (clarsimp simp:pdBits_def pageBits_def mask_twice blah) apply (drule_tac y = "armKSGlobalPD a + b" for a b in neg_mask_mono_le[where n = 14]) apply (drule_tac x = "armKSGlobalPD a + b" for a b in neg_mask_mono_le[where n = 14]) apply (frule_tac d1 = "x && mask 14" in is_aligned_add_helper[THEN conjunct2]) apply (simp add:mask_def pdeBits_def) apply (rule le_less_trans[OF word_and_le1]) apply simp apply (frule_tac d1 = "pptrBase >> 20 << 2" in is_aligned_add_helper[THEN conjunct2]) apply (simp add: pptrBase_def) apply (simp add: pdeBits_def) apply (frule_tac d1 = "0x3FFF" and p1="ptr" in is_aligned_add_helper[THEN conjunct2]) apply (simp add: pdeBits_def) apply (frule_tac d1 = "pptrBase >> 20 << 2" and p1 = "ptr"
                     in is_aligned_add_helper[THEN conjunct2]) apply (simp add: pptrBase_def pdeBits_def) apply (simp add: pdeBits_def) apply (cut_tac copyGlobalMappings_ksPSpace_sameD) apply simp apply (rule monad) apply (simp add:al) apply (simp add:al add.commute) done qed

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. ksPSpace s' = (\<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) proof (state)
goal (1 subgoal):
 1. ksPSpace s' = (\<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) proof (prove)
goal (1 subgoal):
 1. \<And>pd. \<lbrace>\<lambda>s. armKSGlobalPD (ksArchState s) = pd\<rbrace> copyGlobalMappings ptr \<lbrace>\<lambda>r s. armKSGlobalPD (ksArchState s) = pd\<rbrace> proof (state)
this:
\<lbrace>\<lambda>s. armKSGlobalPD (ksArchState s) = ?pd\<rbrace> copyGlobalMappings ptr \<lbrace>\<lambda>r s. armKSGlobalPD (ksArchState s) = ?pd\<rbrace>

goal (1 subgoal):
 1. ksPSpace s' = (\<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) proof (prove)
goal (1 subgoal):
 1. \<And>x. x \<in> {ptr + (pptrBase >> 20 << 2)..ptr + 2 ^ pdBits - 1} \<Longrightarrow> ptr + (x && mask pdBits) = x proof (prove)
using this:
is_aligned (armKSGlobalPD (ksArchState s)) pdBits
is_aligned ptr pdBits

goal (1 subgoal):
 1. \<And>x. x \<in> {ptr + (pptrBase >> 20 << 2)..ptr + 2 ^ pdBits - 1} \<Longrightarrow> ptr + (x && mask pdBits) = x proof (prove)
goal (1 subgoal):
 1. \<And>x. \<lbrakk>x \<in> {ptr + (pptrBase >> 20 << 2)..ptr + 2 ^ pdBits - 1}; is_aligned (armKSGlobalPD (ksArchState s)) pdBits; is_aligned ptr pdBits\<rbrakk> \<Longrightarrow> ptr + (x && mask pdBits) = x proof (prove)
goal (2 subgoals):
 1. \<And>x. \<lbrakk>x \<in> {ptr + (pptrBase >> 20 << 2)..ptr + 2 ^ pdBits - 1}; is_aligned (armKSGlobalPD (ksArchState s)) pdBits; is_aligned ptr pdBits\<rbrakk> \<Longrightarrow> ptr + (x && mask pdBits) && mask pdBits = x && mask pdBits
 2. \<And>x. \<lbrakk>x \<in> {ptr + (pptrBase >> 20 << 2)..ptr + 2 ^ pdBits - 1}; is_aligned (armKSGlobalPD (ksArchState s)) pdBits; is_aligned ptr pdBits\<rbrakk> \<Longrightarrow> ptr + (x && mask pdBits) && ~~ mask pdBits = x && ~~ mask pdBits proof (prove)
goal (1 subgoal):
 1. \<And>x. \<lbrakk>x \<in> {ptr + (pptrBase >> 20 << 2)..ptr + 2 ^ pdBits - 1}; is_aligned (armKSGlobalPD (ksArchState s)) pdBits; is_aligned ptr pdBits\<rbrakk> \<Longrightarrow> ptr + (x && mask pdBits) && ~~ mask pdBits = x && ~~ mask pdBits proof (prove)
goal (1 subgoal):
 1. \<And>x. \<lbrakk>x \<in> {ptr + (pptrBase >> 20 << 2)..ptr + 2 ^ pdBits - 1}; is_aligned (armKSGlobalPD (ksArchState s)) pdBits; is_aligned ptr pdBits\<rbrakk> \<Longrightarrow> ptr + (x && mask pdBits) - (ptr + (x && mask pdBits) && mask pdBits) = x && ~~ mask pdBits proof (prove)
goal (1 subgoal):
 1. \<And>x. \<lbrakk>x \<in> {ptr + (pptrBase >> 20 << 2)..ptr + 2 ^ (12 + pdeBits) - 1}; is_aligned (armKSGlobalPD (ksArchState s)) (12 + pdeBits); is_aligned ptr (12 + pdeBits)\<rbrakk> \<Longrightarrow> ptr = x && ~~ mask (12 + pdeBits) proof (prove)
goal (1 subgoal):
 1. \<And>x. \<lbrakk>is_aligned (armKSGlobalPD (ksArchState s)) (12 + pdeBits); is_aligned ptr (12 + pdeBits); ptr + (pptrBase >> 20 << 2) \<le> x; x \<le> ptr + 2 ^ (12 + pdeBits) - 1\<rbrakk> \<Longrightarrow> ptr = x && ~~ mask (12 + pdeBits) proof (prove)
goal (1 subgoal):
 1. \<And>x. \<lbrakk>is_aligned (armKSGlobalPD (ksArchState s)) (12 + pdeBits); is_aligned ptr (12 + pdeBits); x \<le> ptr + 2 ^ (12 + pdeBits) - 1; ptr + (pptrBase >> 20 << 2) && ~~ mask 14 \<le> x && ~~ mask 14\<rbrakk> \<Longrightarrow> ptr = x && ~~ mask (12 + pdeBits) proof (prove)
goal (1 subgoal):
 1. \<And>x. \<lbrakk>is_aligned (armKSGlobalPD (ksArchState s)) (12 + pdeBits); is_aligned ptr (12 + pdeBits); ptr + (pptrBase >> 20 << 2) && ~~ mask 14 \<le> x && ~~ mask 14; x && ~~ mask 14 \<le> ptr + 2 ^ (12 + pdeBits) - 1 && ~~ mask 14\<rbrakk> \<Longrightarrow> ptr = x && ~~ mask (12 + pdeBits) proof (prove)
goal (1 subgoal):
 1. \<And>x. \<lbrakk>is_aligned (armKSGlobalPD (ksArchState s)) 14; is_aligned ptr 14; ptr + (pptrBase >> 20 << 2) && ~~ mask 14 \<le> x && ~~ mask 14; x && ~~ mask 14 \<le> ptr + 0x3FFF && ~~ mask 14\<rbrakk> \<Longrightarrow> ptr = x && ~~ mask 14 proof (prove)
goal (2 subgoals):
 1. \<And>x. \<lbrakk>is_aligned (armKSGlobalPD (ksArchState s)) 14; is_aligned ptr 14; ptr + (pptrBase >> 20 << 2) && ~~ mask 14 \<le> x && ~~ mask 14; x && ~~ mask 14 \<le> ptr + 0x3FFF && ~~ mask 14\<rbrakk> \<Longrightarrow> 0x3FFF < 2 ^ 14
 2. \<And>x. \<lbrakk>is_aligned (armKSGlobalPD (ksArchState s)) 14; is_aligned ptr 14; ptr + (pptrBase >> 20 << 2) && ~~ mask 14 \<le> x && ~~ mask 14; x && ~~ mask 14 \<le> ptr + 0x3FFF && ~~ mask 14; ptr + 0x3FFF && ~~ mask 14 = ptr\<rbrakk> \<Longrightarrow> ptr = x && ~~ mask 14 proof (prove)
goal (1 subgoal):
 1. \<And>x. \<lbrakk>is_aligned (armKSGlobalPD (ksArchState s)) 14; is_aligned ptr 14; ptr + (pptrBase >> 20 << 2) && ~~ mask 14 \<le> x && ~~ mask 14; x && ~~ mask 14 \<le> ptr + 0x3FFF && ~~ mask 14; ptr + 0x3FFF && ~~ mask 14 = ptr\<rbrakk> \<Longrightarrow> ptr = x && ~~ mask 14 proof (prove)
goal (2 subgoals):
 1. \<And>x. \<lbrakk>is_aligned (armKSGlobalPD (ksArchState s)) 14; is_aligned ptr 14; ptr + (pptrBase >> 20 << 2) && ~~ mask 14 \<le> x && ~~ mask 14; x && ~~ mask 14 \<le> ptr + 0x3FFF && ~~ mask 14; ptr + 0x3FFF && ~~ mask 14 = ptr\<rbrakk> \<Longrightarrow> pptrBase >> 20 << 2 < 2 ^ 14
 2. \<And>x. \<lbrakk>is_aligned (armKSGlobalPD (ksArchState s)) 14; is_aligned ptr 14; ptr + (pptrBase >> 20 << 2) && ~~ mask 14 \<le> x && ~~ mask 14; x && ~~ mask 14 \<le> ptr + 0x3FFF && ~~ mask 14; ptr + 0x3FFF && ~~ mask 14 = ptr; ptr + (pptrBase >> 20 << 2) && ~~ mask 14 = ptr\<rbrakk> \<Longrightarrow> ptr = x && ~~ mask 14 proof (prove)
goal (1 subgoal):
 1. \<And>x. \<lbrakk>is_aligned (armKSGlobalPD (ksArchState s)) 14; is_aligned ptr 14; ptr + (pptrBase >> 20 << 2) && ~~ mask 14 \<le> x && ~~ mask 14; x && ~~ mask 14 \<le> ptr + 0x3FFF && ~~ mask 14; ptr + 0x3FFF && ~~ mask 14 = ptr; ptr + (pptrBase >> 20 << 2) && ~~ mask 14 = ptr\<rbrakk> \<Longrightarrow> ptr = x && ~~ mask 14 proof (prove)
goal:
No subgoals! proof (state)
this:
?x \<in> {ptr + (pptrBase >> 20 << 2)..ptr + 2 ^ pdBits - 1} \<Longrightarrow> ptr + (?x && mask pdBits) = ?x

goal (1 subgoal):
 1. ksPSpace s' = (\<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) proof (prove)
goal (1 subgoal):
 1. ksPSpace s' = (\<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) proof (prove)
using this:
pspace_distinct' s
pspace_aligned' s
is_aligned (armKSGlobalPD (ksArchState s)) pdBits
is_aligned ptr pdBits
(r, s') \<in> fst (copyGlobalMappings ptr s)

goal (1 subgoal):
 1. ksPSpace s' = (\<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) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>pspace_distinct' s; pspace_aligned' s; is_aligned (armKSGlobalPD (ksArchState s)) pdBits; is_aligned ptr pdBits; (r, s') \<in> fst (copyGlobalMappings ptr s)\<rbrakk> \<Longrightarrow> ksPSpace s' = (\<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) proof (prove)
goal (1 subgoal):
 1. \<And>x. \<lbrakk>pspace_distinct' s; pspace_aligned' s; is_aligned (armKSGlobalPD (ksArchState s)) pdBits; is_aligned ptr pdBits; (r, s') \<in> fst (copyGlobalMappings ptr s)\<rbrakk> \<Longrightarrow> ksPSpace s' 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) proof (prove)
goal (3 subgoals):
 1. \<And>x. \<lbrakk>pspace_distinct' s; pspace_aligned' s; is_aligned (armKSGlobalPD (ksArchState s)) pdBits; is_aligned ptr pdBits; (r, s') \<in> fst (copyGlobalMappings ptr s)\<rbrakk> \<Longrightarrow> is_aligned ptr pdBits
 2. \<And>x. \<lbrakk>pspace_distinct' s; pspace_aligned' s; is_aligned (armKSGlobalPD (ksArchState s)) pdBits; is_aligned ptr pdBits; (r, s') \<in> fst (copyGlobalMappings ptr s)\<rbrakk> \<Longrightarrow> ksPSpace s x = ?ko7 x \<and> pspace_distinct' s \<and> pspace_aligned' s \<and> is_aligned (armKSGlobalPD (ksArchState s)) pdBits
 3. \<And>x. \<lbrakk>pspace_distinct' s; pspace_aligned' s; is_aligned (armKSGlobalPD (ksArchState s)) pdBits; is_aligned ptr pdBits; (r, s') \<in> fst (copyGlobalMappings ptr s); ksPSpace s' x = (if x \<in> {ptr + (pptrBase >> 20 << 2)..ptr + (2 ^ pdBits - 1)} then ksPSpace s' (armKSGlobalPD (ksArchState s') + (x && mask pdBits)) else ?ko7 x)\<rbrakk> \<Longrightarrow> ksPSpace s' 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) proof (prove)
goal (1 subgoal):
 1. \<And>x. \<lbrakk>pspace_distinct' s; pspace_aligned' s; is_aligned (armKSGlobalPD (ksArchState s)) pdBits; is_aligned ptr pdBits; ((), s') \<in> fst (copyGlobalMappings ptr s); ksPSpace s' x = (if x \<in> {ptr + (pptrBase >> 20 << 2)..ptr + (2 ^ pdBits - 1)} then ksPSpace s' (armKSGlobalPD (ksArchState s') + (x && mask pdBits)) else ksPSpace s x)\<rbrakk> \<Longrightarrow> x \<in> {ptr + (pptrBase >> 20 << 2)..ptr + (2 ^ pdBits - 1)} \<longrightarrow> ksPSpace s' (armKSGlobalPD (ksArchState s') + (x && mask pdBits)) = ksPSpace s ((x && mask pdBits) + armKSGlobalPD (ksArchState s)) proof (prove)
goal (1 subgoal):
 1. \<And>x. \<lbrakk>pspace_distinct' s; pspace_aligned' s; is_aligned (armKSGlobalPD (ksArchState s)) pdBits; is_aligned ptr pdBits; ((), s') \<in> fst (copyGlobalMappings ptr s); x \<in> {ptr + (pptrBase >> 20 << 2)..ptr + (2 ^ pdBits - 1)}; ksPSpace s' x = ksPSpace s' (armKSGlobalPD (ksArchState s') + (x && mask pdBits))\<rbrakk> \<Longrightarrow> ksPSpace s' (armKSGlobalPD (ksArchState s') + (x && mask pdBits)) = ksPSpace s ((x && mask pdBits) + armKSGlobalPD (ksArchState s)) proof (prove)
goal (3 subgoals):
 1. \<And>x. \<lbrakk>pspace_distinct' s; pspace_aligned' s; is_aligned (armKSGlobalPD (ksArchState s)) pdBits; is_aligned ptr pdBits; ((), s') \<in> fst (copyGlobalMappings ptr s); x \<in> {ptr + (pptrBase >> 20 << 2)..ptr + (2 ^ pdBits - 1)}; ksPSpace s' x = ksPSpace s' (armKSGlobalPD (ksArchState s') + (x && mask pdBits))\<rbrakk> \<Longrightarrow> is_aligned ptr pdBits
 2. \<And>x. \<lbrakk>pspace_distinct' s; pspace_aligned' s; is_aligned (armKSGlobalPD (ksArchState s)) pdBits; is_aligned ptr pdBits; ((), s') \<in> fst (copyGlobalMappings ptr s); x \<in> {ptr + (pptrBase >> 20 << 2)..ptr + (2 ^ pdBits - 1)}; ksPSpace s' x = ksPSpace s' (armKSGlobalPD (ksArchState s') + (x && mask pdBits))\<rbrakk> \<Longrightarrow> ksPSpace s (armKSGlobalPD (ksArchState s') + (x && mask pdBits)) = ?ko25 x \<and> pspace_distinct' s \<and> pspace_aligned' s \<and> is_aligned (armKSGlobalPD (ksArchState s)) pdBits
 3. \<And>x. \<lbrakk>pspace_distinct' s; pspace_aligned' s; is_aligned (armKSGlobalPD (ksArchState s)) pdBits; is_aligned ptr pdBits; ((), s') \<in> fst (copyGlobalMappings ptr s); x \<in> {ptr + (pptrBase >> 20 << 2)..ptr + (2 ^ pdBits - 1)}; ksPSpace s' x = ksPSpace s' (armKSGlobalPD (ksArchState s') + (x && mask pdBits)); ksPSpace s' (armKSGlobalPD (ksArchState s') + (x && mask pdBits)) = (if armKSGlobalPD (ksArchState s') + (x && mask pdBits) \<in> {ptr + (pptrBase >> 20 << 2)..ptr + (2 ^ pdBits - 1)} then ksPSpace s' (armKSGlobalPD (ksArchState s') + (armKSGlobalPD (ksArchState s') + (x && mask pdBits) && mask pdBits)) else ?ko25 x)\<rbrakk> \<Longrightarrow> ksPSpace s' (armKSGlobalPD (ksArchState s') + (x && mask pdBits)) = ksPSpace s ((x && mask pdBits) + armKSGlobalPD (ksArchState s)) proof (prove)
goal (1 subgoal):
 1. \<And>x. \<lbrakk>pspace_distinct' s; pspace_aligned' s; is_aligned (armKSGlobalPD (ksArchState s)) pdBits; is_aligned ptr pdBits; ((), s') \<in> fst (copyGlobalMappings ptr s); x \<in> {ptr + (pptrBase >> 20 << 2)..ptr + (2 ^ pdBits - 1)}; ksPSpace s' x = (if armKSGlobalPD (ksArchState s') + (x && mask pdBits) \<in> {ptr + (pptrBase >> 20 << 2)..ptr + (2 ^ pdBits - 1)} then ksPSpace s' (armKSGlobalPD (ksArchState s') + (armKSGlobalPD (ksArchState s') + (x && mask pdBits) && mask pdBits)) else ksPSpace s (armKSGlobalPD (ksArchState s') + (x && mask pdBits))); ksPSpace s' (armKSGlobalPD (ksArchState s') + (x && mask pdBits)) = (if armKSGlobalPD (ksArchState s') + (x && mask pdBits) \<in> {ptr + (pptrBase >> 20 << 2)..ptr + (2 ^ pdBits - 1)} then ksPSpace s' (armKSGlobalPD (ksArchState s') + (armKSGlobalPD (ksArchState s') + (x && mask pdBits) && mask pdBits)) else ksPSpace s (armKSGlobalPD (ksArchState s') + (x && mask pdBits)))\<rbrakk> \<Longrightarrow> (armKSGlobalPD (ksArchState s') + (x && mask pdBits) \<in> {ptr + (pptrBase >> 20 << 2)..ptr + (2 ^ pdBits - 1)} \<longrightarrow> ksPSpace s' (armKSGlobalPD (ksArchState s') + (armKSGlobalPD (ksArchState s') + (x && mask pdBits) && mask pdBits)) = ksPSpace s ((x && mask pdBits) + armKSGlobalPD (ksArchState s))) \<and> (armKSGlobalPD (ksArchState s') + (x && mask pdBits) \<notin> {ptr + (pptrBase >> 20 << 2)..ptr + (2 ^ pdBits - 1)} \<longrightarrow> ksPSpace s (armKSGlobalPD (ksArchState s') + (x && mask pdBits)) = ksPSpace s ((x && mask pdBits) + armKSGlobalPD (ksArchState s))) proof (prove)
goal (2 subgoals):
 1. \<And>x. \<lbrakk>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 = (if armKSGlobalPD (ksArchState s') + (x && mask pdBits) \<in> {ptr + (pptrBase >> 20 << 2)..ptr + (2 ^ pdBits - 1)} then ksPSpace s' (armKSGlobalPD (ksArchState s') + (armKSGlobalPD (ksArchState s') + (x && mask pdBits) && mask pdBits)) else ksPSpace s (armKSGlobalPD (ksArchState s') + (x && mask pdBits))); ksPSpace s' (armKSGlobalPD (ksArchState s') + (x && mask pdBits)) = (if armKSGlobalPD (ksArchState s') + (x && mask pdBits) \<in> {ptr + (pptrBase >> 20 << 2)..ptr + (2 ^ pdBits - 1)} then ksPSpace s' (armKSGlobalPD (ksArchState s') + (armKSGlobalPD (ksArchState s') + (x && mask pdBits) && mask pdBits)) else ksPSpace s (armKSGlobalPD (ksArchState s') + (x && mask pdBits)))\<rbrakk> \<Longrightarrow> armKSGlobalPD (ksArchState s) = ?pd32 x
 2. \<And>x. \<lbrakk>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 = (if armKSGlobalPD (ksArchState s') + (x && mask pdBits) \<in> {ptr + (pptrBase >> 20 << 2)..ptr + (2 ^ pdBits - 1)} then ksPSpace s' (armKSGlobalPD (ksArchState s') + (armKSGlobalPD (ksArchState s') + (x && mask pdBits) && mask pdBits)) else ksPSpace s (armKSGlobalPD (ksArchState s') + (x && mask pdBits))); ksPSpace s' (armKSGlobalPD (ksArchState s') + (x && mask pdBits)) = (if armKSGlobalPD (ksArchState s') + (x && mask pdBits) \<in> {ptr + (pptrBase >> 20 << 2)..ptr + (2 ^ pdBits - 1)} then ksPSpace s' (armKSGlobalPD (ksArchState s') + (armKSGlobalPD (ksArchState s') + (x && mask pdBits) && mask pdBits)) else ksPSpace s (armKSGlobalPD (ksArchState s') + (x && mask pdBits))); armKSGlobalPD (ksArchState s') = ?pd32 x\<rbrakk> \<Longrightarrow> (armKSGlobalPD (ksArchState s') + (x && mask pdBits) \<in> {ptr + (pptrBase >> 20 << 2)..ptr + (2 ^ pdBits - 1)} \<longrightarrow> ksPSpace s' (armKSGlobalPD (ksArchState s') + (armKSGlobalPD (ksArchState s') + (x && mask pdBits) && mask pdBits)) = ksPSpace s ((x && mask pdBits) + armKSGlobalPD (ksArchState s))) \<and> (armKSGlobalPD (ksArchState s') + (x && mask pdBits) \<notin> {ptr + (pptrBase >> 20 << 2)..ptr + (2 ^ pdBits - 1)} \<longrightarrow> ksPSpace s (armKSGlobalPD (ksArchState s') + (x && mask pdBits)) = ksPSpace s ((x && mask pdBits) + armKSGlobalPD (ksArchState s))) proof (prove)
goal (1 subgoal):
 1. \<And>x. \<lbrakk>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 = (if armKSGlobalPD (ksArchState s') + (x && mask pdBits) \<in> {ptr + (pptrBase >> 20 << 2)..ptr + (2 ^ pdBits - 1)} then ksPSpace s' (armKSGlobalPD (ksArchState s') + (armKSGlobalPD (ksArchState s') + (x && mask pdBits) && mask pdBits)) else ksPSpace s (armKSGlobalPD (ksArchState s') + (x && mask pdBits))); ksPSpace s' (armKSGlobalPD (ksArchState s') + (x && mask pdBits)) = (if armKSGlobalPD (ksArchState s') + (x && mask pdBits) \<in> {ptr + (pptrBase >> 20 << 2)..ptr + (2 ^ pdBits - 1)} then ksPSpace s' (armKSGlobalPD (ksArchState s') + (armKSGlobalPD (ksArchState s') + (x && mask pdBits) && mask pdBits)) else ksPSpace s (armKSGlobalPD (ksArchState s') + (x && mask pdBits))); armKSGlobalPD (ksArchState s') = armKSGlobalPD (ksArchState s)\<rbrakk> \<Longrightarrow> (armKSGlobalPD (ksArchState s') + (x && mask pdBits) \<in> {ptr + (pptrBase >> 20 << 2)..ptr + (2 ^ pdBits - 1)} \<longrightarrow> ksPSpace s' (armKSGlobalPD (ksArchState s') + (armKSGlobalPD (ksArchState s') + (x && mask pdBits) && mask pdBits)) = ksPSpace s ((x && mask pdBits) + armKSGlobalPD (ksArchState s))) \<and> (armKSGlobalPD (ksArchState s') + (x && mask pdBits) \<notin> {ptr + (pptrBase >> 20 << 2)..ptr + (2 ^ pdBits - 1)} \<longrightarrow> ksPSpace s (armKSGlobalPD (ksArchState s') + (x && mask pdBits)) = ksPSpace s ((x && mask pdBits) + armKSGlobalPD (ksArchState s))) proof (prove)
goal (1 subgoal):
 1. \<And>x. \<lbrakk>ksPSpace s' (armKSGlobalPD (ksArchState s) + (x && mask pdBits)) = ksPSpace s' (armKSGlobalPD (ksArchState s) + (armKSGlobalPD (ksArchState s) + (x && mask pdBits) && mask pdBits)); armKSGlobalPD (ksArchState s') = armKSGlobalPD (ksArchState 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}; armKSGlobalPD (ksArchState s) + (x && mask pdBits) \<in> {ptr + (pptrBase >> 20 << 2)..ptr + 2 ^ pdBits - 1}; ksPSpace s' x = ksPSpace s' (armKSGlobalPD (ksArchState s) + (armKSGlobalPD (ksArchState s) + (x && mask pdBits) && mask pdBits))\<rbrakk> \<Longrightarrow> ksPSpace s' (armKSGlobalPD (ksArchState s) + (armKSGlobalPD (ksArchState s) + (x && mask pdBits) && mask pdBits)) = ksPSpace s (armKSGlobalPD (ksArchState s) + (x && mask pdBits)) proof (prove)
goal (1 subgoal):
 1. \<And>x. \<lbrakk>armKSGlobalPD (ksArchState s') = armKSGlobalPD (ksArchState 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}; armKSGlobalPD (ksArchState s) + (x && mask pdBits) \<in> {ptr + (pptrBase >> 20 << 2)..ptr + 2 ^ pdBits - 1}; ksPSpace s' x = ksPSpace s' (armKSGlobalPD (ksArchState s) + (x && mask pdBits))\<rbrakk> \<Longrightarrow> ksPSpace s' (armKSGlobalPD (ksArchState s) + (x && mask pdBits)) = ksPSpace s (armKSGlobalPD (ksArchState s) + (x && mask pdBits)) proof (prove)
goal (1 subgoal):
 1. \<And>x. \<lbrakk>armKSGlobalPD (ksArchState s') = armKSGlobalPD (ksArchState 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}; armKSGlobalPD (ksArchState s) + (x && mask pdBits) \<in> {ptr + (pptrBase >> 20 << 2)..ptr + 2 ^ pdBits - 1}; ksPSpace s' x = ksPSpace s' (armKSGlobalPD (ksArchState s) + (x && mask pdBits)); ptr + (x && mask pdBits) = x\<rbrakk> \<Longrightarrow> ksPSpace s' (armKSGlobalPD (ksArchState s) + (x && mask pdBits)) = ksPSpace s (armKSGlobalPD (ksArchState s) + (x && mask pdBits)) proof (prove)
goal (1 subgoal):
 1. \<And>x. \<lbrakk>armKSGlobalPD (ksArchState s') = armKSGlobalPD (ksArchState s); pspace_distinct' s; pspace_aligned' s; is_aligned (armKSGlobalPD (ksArchState s)) (12 + pdeBits); is_aligned ptr (12 + pdeBits); ksPSpace s' x = ksPSpace s' (armKSGlobalPD (ksArchState s) + (x && mask (12 + pdeBits))); ptr + (x && mask (12 + pdeBits)) = x; ptr + (pptrBase >> 20 << 2) \<le> x; x \<le> ptr + 2 ^ (12 + pdeBits) - 1; ptr + (pptrBase >> 20 << 2) \<le> armKSGlobalPD (ksArchState s) + (x && mask (12 + pdeBits)); armKSGlobalPD (ksArchState s) + (x && mask (12 + pdeBits)) \<le> ptr + 2 ^ (12 + pdeBits) - 1\<rbrakk> \<Longrightarrow> ksPSpace s' (armKSGlobalPD (ksArchState s) + (x && mask (12 + pdeBits))) = ksPSpace s (armKSGlobalPD (ksArchState s) + (x && mask (12 + pdeBits))) proof (prove)
goal (1 subgoal):
 1. \<And>x. \<lbrakk>armKSGlobalPD (ksArchState s') = armKSGlobalPD (ksArchState s); pspace_distinct' s; pspace_aligned' s; is_aligned (armKSGlobalPD (ksArchState s)) (12 + pdeBits); is_aligned ptr (12 + pdeBits); ksPSpace s' x = ksPSpace s' (armKSGlobalPD (ksArchState s) + (x && mask (12 + pdeBits))); ptr + (x && mask (12 + pdeBits)) = x; ptr + (pptrBase >> 20 << 2) \<le> x; x \<le> ptr + 2 ^ (12 + pdeBits) - 1; armKSGlobalPD (ksArchState s) + (x && mask (12 + pdeBits)) \<le> ptr + 2 ^ (12 + pdeBits) - 1; ptr + (pptrBase >> 20 << 2) && ~~ mask 14 \<le> armKSGlobalPD (ksArchState s) + (x && mask (12 + pdeBits)) && ~~ mask 14\<rbrakk> \<Longrightarrow> ksPSpace s' (armKSGlobalPD (ksArchState s) + (x && mask (12 + pdeBits))) = ksPSpace s (armKSGlobalPD (ksArchState s) + (x && mask (12 + pdeBits))) proof (prove)
goal (1 subgoal):
 1. \<And>x. \<lbrakk>armKSGlobalPD (ksArchState s') = armKSGlobalPD (ksArchState s); pspace_distinct' s; pspace_aligned' s; is_aligned (armKSGlobalPD (ksArchState s)) (12 + pdeBits); is_aligned ptr (12 + pdeBits); ksPSpace s' x = ksPSpace s' (armKSGlobalPD (ksArchState s) + (x && mask (12 + pdeBits))); ptr + (x && mask (12 + pdeBits)) = x; ptr + (pptrBase >> 20 << 2) \<le> x; x \<le> ptr + 2 ^ (12 + pdeBits) - 1; ptr + (pptrBase >> 20 << 2) && ~~ mask 14 \<le> armKSGlobalPD (ksArchState s) + (x && mask (12 + pdeBits)) && ~~ mask 14; armKSGlobalPD (ksArchState s) + (x && mask (12 + pdeBits)) && ~~ mask 14 \<le> ptr + 2 ^ (12 + pdeBits) - 1 && ~~ mask 14\<rbrakk> \<Longrightarrow> ksPSpace s' (armKSGlobalPD (ksArchState s) + (x && mask (12 + pdeBits))) = ksPSpace s (armKSGlobalPD (ksArchState s) + (x && mask (12 + pdeBits))) proof (prove)
goal (2 subgoals):
 1. \<And>x. \<lbrakk>armKSGlobalPD (ksArchState s') = armKSGlobalPD (ksArchState s); pspace_distinct' s; pspace_aligned' s; is_aligned (armKSGlobalPD (ksArchState s)) (12 + pdeBits); is_aligned ptr (12 + pdeBits); ksPSpace s' x = ksPSpace s' (armKSGlobalPD (ksArchState s) + (x && mask (12 + pdeBits))); ptr + (x && mask (12 + pdeBits)) = x; ptr + (pptrBase >> 20 << 2) \<le> x; x \<le> ptr + 2 ^ (12 + pdeBits) - 1; ptr + (pptrBase >> 20 << 2) && ~~ mask 14 \<le> armKSGlobalPD (ksArchState s) + (x && mask (12 + pdeBits)) && ~~ mask 14; armKSGlobalPD (ksArchState s) + (x && mask (12 + pdeBits)) && ~~ mask 14 \<le> ptr + 2 ^ (12 + pdeBits) - 1 && ~~ mask 14\<rbrakk> \<Longrightarrow> x && mask 14 < 2 ^ (12 + pdeBits)
 2. \<And>x. \<lbrakk>armKSGlobalPD (ksArchState s') = armKSGlobalPD (ksArchState s); pspace_distinct' s; pspace_aligned' s; is_aligned (armKSGlobalPD (ksArchState s)) (12 + pdeBits); is_aligned ptr (12 + pdeBits); ksPSpace s' x = ksPSpace s' (armKSGlobalPD (ksArchState s) + (x && mask (12 + pdeBits))); ptr + (x && mask (12 + pdeBits)) = x; ptr + (pptrBase >> 20 << 2) \<le> x; x \<le> ptr + 2 ^ (12 + pdeBits) - 1; ptr + (pptrBase >> 20 << 2) && ~~ mask 14 \<le> armKSGlobalPD (ksArchState s) + (x && mask (12 + pdeBits)) && ~~ mask 14; armKSGlobalPD (ksArchState s) + (x && mask (12 + pdeBits)) && ~~ mask 14 \<le> ptr + 2 ^ (12 + pdeBits) - 1 && ~~ mask 14; armKSGlobalPD (ksArchState s) + (x && mask 14) && ~~ mask (12 + pdeBits) = armKSGlobalPD (ksArchState s)\<rbrakk> \<Longrightarrow> ksPSpace s' (armKSGlobalPD (ksArchState s) + (x && mask (12 + pdeBits))) = ksPSpace s (armKSGlobalPD (ksArchState s) + (x && mask (12 + pdeBits))) proof (prove)
goal (2 subgoals):
 1. \<And>x. \<lbrakk>armKSGlobalPD (ksArchState s') = armKSGlobalPD (ksArchState s); pspace_distinct' s; pspace_aligned' s; is_aligned (armKSGlobalPD (ksArchState s)) 14; is_aligned ptr 14; ksPSpace s' x = ksPSpace s' (armKSGlobalPD (ksArchState s) + (x && 0x3FFF)); ptr + (x && 0x3FFF) = x; ptr + (pptrBase >> 20 << 2) \<le> x; x \<le> 0x3FFF + ptr; ptr + (pptrBase >> 20 << 2) && 0xFFFFC000 \<le> armKSGlobalPD (ksArchState s) + (x && 0x3FFF) && 0xFFFFC000; armKSGlobalPD (ksArchState s) + (x && 0x3FFF) && 0xFFFFC000 \<le> 0x3FFF + ptr && 0xFFFFC000\<rbrakk> \<Longrightarrow> x && 0x3FFF < 0x4000
 2. \<And>x. \<lbrakk>armKSGlobalPD (ksArchState s') = armKSGlobalPD (ksArchState s); pspace_distinct' s; pspace_aligned' s; is_aligned (armKSGlobalPD (ksArchState s)) (12 + pdeBits); is_aligned ptr (12 + pdeBits); ksPSpace s' x = ksPSpace s' (armKSGlobalPD (ksArchState s) + (x && mask (12 + pdeBits))); ptr + (x && mask (12 + pdeBits)) = x; ptr + (pptrBase >> 20 << 2) \<le> x; x \<le> ptr + 2 ^ (12 + pdeBits) - 1; ptr + (pptrBase >> 20 << 2) && ~~ mask 14 \<le> armKSGlobalPD (ksArchState s) + (x && mask (12 + pdeBits)) && ~~ mask 14; armKSGlobalPD (ksArchState s) + (x && mask (12 + pdeBits)) && ~~ mask 14 \<le> ptr + 2 ^ (12 + pdeBits) - 1 && ~~ mask 14; armKSGlobalPD (ksArchState s) + (x && mask 14) && ~~ mask (12 + pdeBits) = armKSGlobalPD (ksArchState s)\<rbrakk> \<Longrightarrow> ksPSpace s' (armKSGlobalPD (ksArchState s) + (x && mask (12 + pdeBits))) = ksPSpace s (armKSGlobalPD (ksArchState s) + (x && mask (12 + pdeBits))) proof (prove)
goal (2 subgoals):
 1. \<And>x. \<lbrakk>armKSGlobalPD (ksArchState s') = armKSGlobalPD (ksArchState s); pspace_distinct' s; pspace_aligned' s; is_aligned (armKSGlobalPD (ksArchState s)) 14; is_aligned ptr 14; ksPSpace s' x = ksPSpace s' (armKSGlobalPD (ksArchState s) + (x && 0x3FFF)); ptr + (x && 0x3FFF) = x; ptr + (pptrBase >> 20 << 2) \<le> x; x \<le> 0x3FFF + ptr; ptr + (pptrBase >> 20 << 2) && 0xFFFFC000 \<le> armKSGlobalPD (ksArchState s) + (x && 0x3FFF) && 0xFFFFC000; armKSGlobalPD (ksArchState s) + (x && 0x3FFF) && 0xFFFFC000 \<le> 0x3FFF + ptr && 0xFFFFC000\<rbrakk> \<Longrightarrow> 0x3FFF < 0x4000
 2. \<And>x. \<lbrakk>armKSGlobalPD (ksArchState s') = armKSGlobalPD (ksArchState s); pspace_distinct' s; pspace_aligned' s; is_aligned (armKSGlobalPD (ksArchState s)) (12 + pdeBits); is_aligned ptr (12 + pdeBits); ksPSpace s' x = ksPSpace s' (armKSGlobalPD (ksArchState s) + (x && mask (12 + pdeBits))); ptr + (x && mask (12 + pdeBits)) = x; ptr + (pptrBase >> 20 << 2) \<le> x; x \<le> ptr + 2 ^ (12 + pdeBits) - 1; ptr + (pptrBase >> 20 << 2) && ~~ mask 14 \<le> armKSGlobalPD (ksArchState s) + (x && mask (12 + pdeBits)) && ~~ mask 14; armKSGlobalPD (ksArchState s) + (x && mask (12 + pdeBits)) && ~~ mask 14 \<le> ptr + 2 ^ (12 + pdeBits) - 1 && ~~ mask 14; armKSGlobalPD (ksArchState s) + (x && mask 14) && ~~ mask (12 + pdeBits) = armKSGlobalPD (ksArchState s)\<rbrakk> \<Longrightarrow> ksPSpace s' (armKSGlobalPD (ksArchState s) + (x && mask (12 + pdeBits))) = ksPSpace s (armKSGlobalPD (ksArchState s) + (x && mask (12 + pdeBits))) proof (prove)
goal (1 subgoal):
 1. \<And>x. \<lbrakk>armKSGlobalPD (ksArchState s') = armKSGlobalPD (ksArchState s); pspace_distinct' s; pspace_aligned' s; is_aligned (armKSGlobalPD (ksArchState s)) (12 + pdeBits); is_aligned ptr (12 + pdeBits); ksPSpace s' x = ksPSpace s' (armKSGlobalPD (ksArchState s) + (x && mask (12 + pdeBits))); ptr + (x && mask (12 + pdeBits)) = x; ptr + (pptrBase >> 20 << 2) \<le> x; x \<le> ptr + 2 ^ (12 + pdeBits) - 1; ptr + (pptrBase >> 20 << 2) && ~~ mask 14 \<le> armKSGlobalPD (ksArchState s) + (x && mask (12 + pdeBits)) && ~~ mask 14; armKSGlobalPD (ksArchState s) + (x && mask (12 + pdeBits)) && ~~ mask 14 \<le> ptr + 2 ^ (12 + pdeBits) - 1 && ~~ mask 14; armKSGlobalPD (ksArchState s) + (x && mask 14) && ~~ mask (12 + pdeBits) = armKSGlobalPD (ksArchState s)\<rbrakk> \<Longrightarrow> ksPSpace s' (armKSGlobalPD (ksArchState s) + (x && mask (12 + pdeBits))) = ksPSpace s (armKSGlobalPD (ksArchState s) + (x && mask (12 + pdeBits))) proof (prove)
goal (2 subgoals):
 1. \<And>x. \<lbrakk>armKSGlobalPD (ksArchState s') = armKSGlobalPD (ksArchState s); pspace_distinct' s; pspace_aligned' s; is_aligned (armKSGlobalPD (ksArchState s)) (12 + pdeBits); is_aligned ptr (12 + pdeBits); ksPSpace s' x = ksPSpace s' (armKSGlobalPD (ksArchState s) + (x && mask (12 + pdeBits))); ptr + (x && mask (12 + pdeBits)) = x; ptr + (pptrBase >> 20 << 2) \<le> x; x \<le> ptr + 2 ^ (12 + pdeBits) - 1; ptr + (pptrBase >> 20 << 2) && ~~ mask 14 \<le> armKSGlobalPD (ksArchState s) + (x && mask (12 + pdeBits)) && ~~ mask 14; armKSGlobalPD (ksArchState s) + (x && mask (12 + pdeBits)) && ~~ mask 14 \<le> ptr + 2 ^ (12 + pdeBits) - 1 && ~~ mask 14; armKSGlobalPD (ksArchState s) + (x && mask 14) && ~~ mask (12 + pdeBits) = armKSGlobalPD (ksArchState s)\<rbrakk> \<Longrightarrow> pptrBase >> 20 << 2 < 2 ^ (12 + pdeBits)
 2. \<And>x. \<lbrakk>armKSGlobalPD (ksArchState s') = armKSGlobalPD (ksArchState s); pspace_distinct' s; pspace_aligned' s; is_aligned (armKSGlobalPD (ksArchState s)) (12 + pdeBits); is_aligned ptr (12 + pdeBits); ksPSpace s' x = ksPSpace s' (armKSGlobalPD (ksArchState s) + (x && mask (12 + pdeBits))); ptr + (x && mask (12 + pdeBits)) = x; ptr + (pptrBase >> 20 << 2) \<le> x; x \<le> ptr + 2 ^ (12 + pdeBits) - 1; ptr + (pptrBase >> 20 << 2) && ~~ mask 14 \<le> armKSGlobalPD (ksArchState s) + (x && mask (12 + pdeBits)) && ~~ mask 14; armKSGlobalPD (ksArchState s) + (x && mask (12 + pdeBits)) && ~~ mask 14 \<le> ptr + 2 ^ (12 + pdeBits) - 1 && ~~ mask 14; armKSGlobalPD (ksArchState s) + (x && mask 14) && ~~ mask (12 + pdeBits) = armKSGlobalPD (ksArchState s); armKSGlobalPD (ksArchState s) + (pptrBase >> 20 << 2) && ~~ mask (12 + pdeBits) = armKSGlobalPD (ksArchState s)\<rbrakk> \<Longrightarrow> ksPSpace s' (armKSGlobalPD (ksArchState s) + (x && mask (12 + pdeBits))) = ksPSpace s (armKSGlobalPD (ksArchState s) + (x && mask (12 + pdeBits))) proof (prove)
goal (2 subgoals):
 1. \<And>x. \<lbrakk>armKSGlobalPD (ksArchState s') = armKSGlobalPD (ksArchState s); pspace_distinct' s; pspace_aligned' s; is_aligned (armKSGlobalPD (ksArchState s)) (12 + pdeBits); is_aligned ptr (12 + pdeBits); ksPSpace s' x = ksPSpace s' (armKSGlobalPD (ksArchState s) + (x && mask (12 + pdeBits))); ptr + (x && mask (12 + pdeBits)) = x; ptr + 0x3800 \<le> x; x \<le> ptr + 2 ^ (12 + pdeBits) - 1; ptr + 0x3800 && ~~ mask 14 \<le> armKSGlobalPD (ksArchState s) + (x && mask (12 + pdeBits)) && ~~ mask 14; armKSGlobalPD (ksArchState s) + (x && mask (12 + pdeBits)) && ~~ mask 14 \<le> ptr + 2 ^ (12 + pdeBits) - 1 && ~~ mask 14; armKSGlobalPD (ksArchState s) + (x && mask 14) && ~~ mask (12 + pdeBits) = armKSGlobalPD (ksArchState s)\<rbrakk> \<Longrightarrow> 0x3800 < 2 ^ (12 + pdeBits)
 2. \<And>x. \<lbrakk>armKSGlobalPD (ksArchState s') = armKSGlobalPD (ksArchState s); pspace_distinct' s; pspace_aligned' s; is_aligned (armKSGlobalPD (ksArchState s)) (12 + pdeBits); is_aligned ptr (12 + pdeBits); ksPSpace s' x = ksPSpace s' (armKSGlobalPD (ksArchState s) + (x && mask (12 + pdeBits))); ptr + (x && mask (12 + pdeBits)) = x; ptr + (pptrBase >> 20 << 2) \<le> x; x \<le> ptr + 2 ^ (12 + pdeBits) - 1; ptr + (pptrBase >> 20 << 2) && ~~ mask 14 \<le> armKSGlobalPD (ksArchState s) + (x && mask (12 + pdeBits)) && ~~ mask 14; armKSGlobalPD (ksArchState s) + (x && mask (12 + pdeBits)) && ~~ mask 14 \<le> ptr + 2 ^ (12 + pdeBits) - 1 && ~~ mask 14; armKSGlobalPD (ksArchState s) + (x && mask 14) && ~~ mask (12 + pdeBits) = armKSGlobalPD (ksArchState s); armKSGlobalPD (ksArchState s) + (pptrBase >> 20 << 2) && ~~ mask (12 + pdeBits) = armKSGlobalPD (ksArchState s)\<rbrakk> \<Longrightarrow> ksPSpace s' (armKSGlobalPD (ksArchState s) + (x && mask (12 + pdeBits))) = ksPSpace s (armKSGlobalPD (ksArchState s) + (x && mask (12 + pdeBits))) proof (prove)
goal (1 subgoal):
 1. \<And>x. \<lbrakk>armKSGlobalPD (ksArchState s') = armKSGlobalPD (ksArchState s); pspace_distinct' s; pspace_aligned' s; is_aligned (armKSGlobalPD (ksArchState s)) (12 + pdeBits); is_aligned ptr (12 + pdeBits); ksPSpace s' x = ksPSpace s' (armKSGlobalPD (ksArchState s) + (x && mask (12 + pdeBits))); ptr + (x && mask (12 + pdeBits)) = x; ptr + (pptrBase >> 20 << 2) \<le> x; x \<le> ptr + 2 ^ (12 + pdeBits) - 1; ptr + (pptrBase >> 20 << 2) && ~~ mask 14 \<le> armKSGlobalPD (ksArchState s) + (x && mask (12 + pdeBits)) && ~~ mask 14; armKSGlobalPD (ksArchState s) + (x && mask (12 + pdeBits)) && ~~ mask 14 \<le> ptr + 2 ^ (12 + pdeBits) - 1 && ~~ mask 14; armKSGlobalPD (ksArchState s) + (x && mask 14) && ~~ mask (12 + pdeBits) = armKSGlobalPD (ksArchState s); armKSGlobalPD (ksArchState s) + (pptrBase >> 20 << 2) && ~~ mask (12 + pdeBits) = armKSGlobalPD (ksArchState s)\<rbrakk> \<Longrightarrow> ksPSpace s' (armKSGlobalPD (ksArchState s) + (x && mask (12 + pdeBits))) = ksPSpace s (armKSGlobalPD (ksArchState s) + (x && mask (12 + pdeBits))) proof (prove)
goal (2 subgoals):
 1. \<And>x. \<lbrakk>armKSGlobalPD (ksArchState s') = armKSGlobalPD (ksArchState s); pspace_distinct' s; pspace_aligned' s; is_aligned (armKSGlobalPD (ksArchState s)) (12 + pdeBits); is_aligned ptr (12 + pdeBits); ksPSpace s' x = ksPSpace s' (armKSGlobalPD (ksArchState s) + (x && mask (12 + pdeBits))); ptr + (x && mask (12 + pdeBits)) = x; ptr + (pptrBase >> 20 << 2) \<le> x; x \<le> ptr + 2 ^ (12 + pdeBits) - 1; ptr + (pptrBase >> 20 << 2) && ~~ mask 14 \<le> armKSGlobalPD (ksArchState s) + (x && mask (12 + pdeBits)) && ~~ mask 14; armKSGlobalPD (ksArchState s) + (x && mask (12 + pdeBits)) && ~~ mask 14 \<le> ptr + 2 ^ (12 + pdeBits) - 1 && ~~ mask 14; armKSGlobalPD (ksArchState s) + (x && mask 14) && ~~ mask (12 + pdeBits) = armKSGlobalPD (ksArchState s); armKSGlobalPD (ksArchState s) + (pptrBase >> 20 << 2) && ~~ mask (12 + pdeBits) = armKSGlobalPD (ksArchState s)\<rbrakk> \<Longrightarrow> 0x3FFF < 2 ^ (12 + pdeBits)
 2. \<And>x. \<lbrakk>armKSGlobalPD (ksArchState s') = armKSGlobalPD (ksArchState s); pspace_distinct' s; pspace_aligned' s; is_aligned (armKSGlobalPD (ksArchState s)) (12 + pdeBits); is_aligned ptr (12 + pdeBits); ksPSpace s' x = ksPSpace s' (armKSGlobalPD (ksArchState s) + (x && mask (12 + pdeBits))); ptr + (x && mask (12 + pdeBits)) = x; ptr + (pptrBase >> 20 << 2) \<le> x; x \<le> ptr + 2 ^ (12 + pdeBits) - 1; ptr + (pptrBase >> 20 << 2) && ~~ mask 14 \<le> armKSGlobalPD (ksArchState s) + (x && mask (12 + pdeBits)) && ~~ mask 14; armKSGlobalPD (ksArchState s) + (x && mask (12 + pdeBits)) && ~~ mask 14 \<le> ptr + 2 ^ (12 + pdeBits) - 1 && ~~ mask 14; armKSGlobalPD (ksArchState s) + (x && mask 14) && ~~ mask (12 + pdeBits) = armKSGlobalPD (ksArchState s); armKSGlobalPD (ksArchState s) + (pptrBase >> 20 << 2) && ~~ mask (12 + pdeBits) = armKSGlobalPD (ksArchState s); ptr + 0x3FFF && ~~ mask (12 + pdeBits) = ptr\<rbrakk> \<Longrightarrow> ksPSpace s' (armKSGlobalPD (ksArchState s) + (x && mask (12 + pdeBits))) = ksPSpace s (armKSGlobalPD (ksArchState s) + (x && mask (12 + pdeBits))) proof (prove)
goal (1 subgoal):
 1. \<And>x. \<lbrakk>armKSGlobalPD (ksArchState s') = armKSGlobalPD (ksArchState s); pspace_distinct' s; pspace_aligned' s; is_aligned (armKSGlobalPD (ksArchState s)) (12 + pdeBits); is_aligned ptr (12 + pdeBits); ksPSpace s' x = ksPSpace s' (armKSGlobalPD (ksArchState s) + (x && mask (12 + pdeBits))); ptr + (x && mask (12 + pdeBits)) = x; ptr + (pptrBase >> 20 << 2) \<le> x; x \<le> ptr + 2 ^ (12 + pdeBits) - 1; ptr + (pptrBase >> 20 << 2) && ~~ mask 14 \<le> armKSGlobalPD (ksArchState s) + (x && mask (12 + pdeBits)) && ~~ mask 14; armKSGlobalPD (ksArchState s) + (x && mask (12 + pdeBits)) && ~~ mask 14 \<le> ptr + 2 ^ (12 + pdeBits) - 1 && ~~ mask 14; armKSGlobalPD (ksArchState s) + (x && mask 14) && ~~ mask (12 + pdeBits) = armKSGlobalPD (ksArchState s); armKSGlobalPD (ksArchState s) + (pptrBase >> 20 << 2) && ~~ mask (12 + pdeBits) = armKSGlobalPD (ksArchState s); ptr + 0x3FFF && ~~ mask (12 + pdeBits) = ptr\<rbrakk> \<Longrightarrow> ksPSpace s' (armKSGlobalPD (ksArchState s) + (x && mask (12 + pdeBits))) = ksPSpace s (armKSGlobalPD (ksArchState s) + (x && mask (12 + pdeBits))) proof (prove)
goal (2 subgoals):
 1. \<And>x. \<lbrakk>armKSGlobalPD (ksArchState s') = armKSGlobalPD (ksArchState s); pspace_distinct' s; pspace_aligned' s; is_aligned (armKSGlobalPD (ksArchState s)) (12 + pdeBits); is_aligned ptr (12 + pdeBits); ksPSpace s' x = ksPSpace s' (armKSGlobalPD (ksArchState s) + (x && mask (12 + pdeBits))); ptr + (x && mask (12 + pdeBits)) = x; ptr + (pptrBase >> 20 << 2) \<le> x; x \<le> ptr + 2 ^ (12 + pdeBits) - 1; ptr + (pptrBase >> 20 << 2) && ~~ mask 14 \<le> armKSGlobalPD (ksArchState s) + (x && mask (12 + pdeBits)) && ~~ mask 14; armKSGlobalPD (ksArchState s) + (x && mask (12 + pdeBits)) && ~~ mask 14 \<le> ptr + 2 ^ (12 + pdeBits) - 1 && ~~ mask 14; armKSGlobalPD (ksArchState s) + (x && mask 14) && ~~ mask (12 + pdeBits) = armKSGlobalPD (ksArchState s); armKSGlobalPD (ksArchState s) + (pptrBase >> 20 << 2) && ~~ mask (12 + pdeBits) = armKSGlobalPD (ksArchState s); ptr + 0x3FFF && ~~ mask (12 + pdeBits) = ptr\<rbrakk> \<Longrightarrow> pptrBase >> 20 << 2 < 2 ^ (12 + pdeBits)
 2. \<And>x. \<lbrakk>armKSGlobalPD (ksArchState s') = armKSGlobalPD (ksArchState s); pspace_distinct' s; pspace_aligned' s; is_aligned (armKSGlobalPD (ksArchState s)) (12 + pdeBits); is_aligned ptr (12 + pdeBits); ksPSpace s' x = ksPSpace s' (armKSGlobalPD (ksArchState s) + (x && mask (12 + pdeBits))); ptr + (x && mask (12 + pdeBits)) = x; ptr + (pptrBase >> 20 << 2) \<le> x; x \<le> ptr + 2 ^ (12 + pdeBits) - 1; ptr + (pptrBase >> 20 << 2) && ~~ mask 14 \<le> armKSGlobalPD (ksArchState s) + (x && mask (12 + pdeBits)) && ~~ mask 14; armKSGlobalPD (ksArchState s) + (x && mask (12 + pdeBits)) && ~~ mask 14 \<le> ptr + 2 ^ (12 + pdeBits) - 1 && ~~ mask 14; armKSGlobalPD (ksArchState s) + (x && mask 14) && ~~ mask (12 + pdeBits) = armKSGlobalPD (ksArchState s); armKSGlobalPD (ksArchState s) + (pptrBase >> 20 << 2) && ~~ mask (12 + pdeBits) = armKSGlobalPD (ksArchState s); ptr + 0x3FFF && ~~ mask (12 + pdeBits) = ptr; ptr + (pptrBase >> 20 << 2) && ~~ mask (12 + pdeBits) = ptr\<rbrakk> \<Longrightarrow> ksPSpace s' (armKSGlobalPD (ksArchState s) + (x && mask (12 + pdeBits))) = ksPSpace s (armKSGlobalPD (ksArchState s) + (x && mask (12 + pdeBits))) proof (prove)
goal (1 subgoal):
 1. \<And>x. \<lbrakk>armKSGlobalPD (ksArchState s') = armKSGlobalPD (ksArchState s); pspace_distinct' s; pspace_aligned' s; is_aligned (armKSGlobalPD (ksArchState s)) (12 + pdeBits); is_aligned ptr (12 + pdeBits); ksPSpace s' x = ksPSpace s' (armKSGlobalPD (ksArchState s) + (x && mask (12 + pdeBits))); ptr + (x && mask (12 + pdeBits)) = x; ptr + (pptrBase >> 20 << 2) \<le> x; x \<le> ptr + 2 ^ (12 + pdeBits) - 1; ptr + (pptrBase >> 20 << 2) && ~~ mask 14 \<le> armKSGlobalPD (ksArchState s) + (x && mask (12 + pdeBits)) && ~~ mask 14; armKSGlobalPD (ksArchState s) + (x && mask (12 + pdeBits)) && ~~ mask 14 \<le> ptr + 2 ^ (12 + pdeBits) - 1 && ~~ mask 14; armKSGlobalPD (ksArchState s) + (x && mask 14) && ~~ mask (12 + pdeBits) = armKSGlobalPD (ksArchState s); armKSGlobalPD (ksArchState s) + (pptrBase >> 20 << 2) && ~~ mask (12 + pdeBits) = armKSGlobalPD (ksArchState s); ptr + 0x3FFF && ~~ mask (12 + pdeBits) = ptr; ptr + (pptrBase >> 20 << 2) && ~~ mask (12 + pdeBits) = ptr\<rbrakk> \<Longrightarrow> ksPSpace s' (armKSGlobalPD (ksArchState s) + (x && mask (12 + pdeBits))) = ksPSpace s (armKSGlobalPD (ksArchState s) + (x && mask (12 + pdeBits))) proof (prove)
goal (1 subgoal):
 1. \<And>x. \<lbrakk>armKSGlobalPD (ksArchState s') = armKSGlobalPD (ksArchState s); pspace_distinct' s; pspace_aligned' s; is_aligned (armKSGlobalPD (ksArchState s)) 14; is_aligned ptr 14; ksPSpace s' x = ksPSpace s' (armKSGlobalPD (ksArchState s) + (x && mask 14)); ptr + (x && mask 14) = x; ptr + (pptrBase >> 20 << 2) \<le> x; x \<le> 0x3FFF + ptr; ptr \<le> armKSGlobalPD (ksArchState s); armKSGlobalPD (ksArchState s) \<le> 0x3FFF + ptr && ~~ mask 14; armKSGlobalPD (ksArchState s) + (x && mask 14) && ~~ mask 14 = armKSGlobalPD (ksArchState s); armKSGlobalPD (ksArchState s) + (pptrBase >> 20 << 2) && ~~ mask 14 = armKSGlobalPD (ksArchState s); ptr + 0x3FFF && ~~ mask 14 = ptr; ptr + (pptrBase >> 20 << 2) && ~~ mask 14 = ptr\<rbrakk> \<Longrightarrow> ksPSpace s' (armKSGlobalPD (ksArchState s) + (x && mask 14)) = ksPSpace s (armKSGlobalPD (ksArchState s) + (x && mask 14)) proof (prove)
goal (4 subgoals):
 1. \<And>x. \<lbrakk>armKSGlobalPD (ksArchState s') = armKSGlobalPD (ksArchState s); pspace_distinct' s; pspace_aligned' s; is_aligned (armKSGlobalPD (ksArchState s)) 14; is_aligned ptr 14; ksPSpace s' x = ksPSpace s' (armKSGlobalPD (ksArchState s) + (x && mask 14)); ptr + (x && mask 14) = x; ptr + (pptrBase >> 20 << 2) \<le> x; x \<le> 0x3FFF + ptr; ptr \<le> armKSGlobalPD (ksArchState s); armKSGlobalPD (ksArchState s) \<le> 0x3FFF + ptr && ~~ mask 14; armKSGlobalPD (ksArchState s) + (x && mask 14) && ~~ mask 14 = armKSGlobalPD (ksArchState s); armKSGlobalPD (ksArchState s) + (pptrBase >> 20 << 2) && ~~ mask 14 = armKSGlobalPD (ksArchState s); ptr + 0x3FFF && ~~ mask 14 = ptr; ptr + (pptrBase >> 20 << 2) && ~~ mask 14 = ptr; ksPSpace (?s'135 x) (?x135 x) = ?ko135 x\<rbrakk> \<Longrightarrow> ksPSpace s' (armKSGlobalPD (ksArchState s) + (x && mask 14)) = ksPSpace s (armKSGlobalPD (ksArchState s) + (x && mask 14))
 2. \<And>x. \<lbrakk>armKSGlobalPD (ksArchState s') = armKSGlobalPD (ksArchState s); pspace_distinct' s; pspace_aligned' s; is_aligned (armKSGlobalPD (ksArchState s)) 14; is_aligned ptr 14; ksPSpace s' x = ksPSpace s' (armKSGlobalPD (ksArchState s) + (x && mask 14)); ptr + (x && mask 14) = x; ptr + (pptrBase >> 20 << 2) \<le> x; x \<le> 0x3FFF + ptr; ptr \<le> armKSGlobalPD (ksArchState s); armKSGlobalPD (ksArchState s) \<le> 0x3FFF + ptr && ~~ mask 14; armKSGlobalPD (ksArchState s) + (x && mask 14) && ~~ mask 14 = armKSGlobalPD (ksArchState s); armKSGlobalPD (ksArchState s) + (pptrBase >> 20 << 2) && ~~ mask 14 = armKSGlobalPD (ksArchState s); ptr + 0x3FFF && ~~ mask 14 = ptr; ptr + (pptrBase >> 20 << 2) && ~~ mask 14 = ptr\<rbrakk> \<Longrightarrow> (?r135 x, ?s'135 x) \<in> fst (copyGlobalMappings (?ptr135 x) (?s135 x))
 3. \<And>x. \<lbrakk>armKSGlobalPD (ksArchState s') = armKSGlobalPD (ksArchState s); pspace_distinct' s; pspace_aligned' s; is_aligned (armKSGlobalPD (ksArchState s)) 14; is_aligned ptr 14; ksPSpace s' x = ksPSpace s' (armKSGlobalPD (ksArchState s) + (x && mask 14)); ptr + (x && mask 14) = x; ptr + (pptrBase >> 20 << 2) \<le> x; x \<le> 0x3FFF + ptr; ptr \<le> armKSGlobalPD (ksArchState s); armKSGlobalPD (ksArchState s) \<le> 0x3FFF + ptr && ~~ mask 14; armKSGlobalPD (ksArchState s) + (x && mask 14) && ~~ mask 14 = armKSGlobalPD (ksArchState s); armKSGlobalPD (ksArchState s) + (pptrBase >> 20 << 2) && ~~ mask 14 = armKSGlobalPD (ksArchState s); ptr + 0x3FFF && ~~ mask 14 = ptr; ptr + (pptrBase >> 20 << 2) && ~~ mask 14 = ptr\<rbrakk> \<Longrightarrow> is_aligned (?ptr135 x) pdBits
 4. \<And>x. \<lbrakk>armKSGlobalPD (ksArchState s') = armKSGlobalPD (ksArchState s); pspace_distinct' s; pspace_aligned' s; is_aligned (armKSGlobalPD (ksArchState s)) 14; is_aligned ptr 14; ksPSpace s' x = ksPSpace s' (armKSGlobalPD (ksArchState s) + (x && mask 14)); ptr + (x && mask 14) = x; ptr + (pptrBase >> 20 << 2) \<le> x; x \<le> 0x3FFF + ptr; ptr \<le> armKSGlobalPD (ksArchState s); armKSGlobalPD (ksArchState s) \<le> 0x3FFF + ptr && ~~ mask 14; armKSGlobalPD (ksArchState s) + (x && mask 14) && ~~ mask 14 = armKSGlobalPD (ksArchState s); armKSGlobalPD (ksArchState s) + (pptrBase >> 20 << 2) && ~~ mask 14 = armKSGlobalPD (ksArchState s); ptr + 0x3FFF && ~~ mask 14 = ptr; ptr + (pptrBase >> 20 << 2) && ~~ mask 14 = ptr\<rbrakk> \<Longrightarrow> ksPSpace (?s135 x) (?x135 x) = ?ko135 x \<and> pspace_distinct' (?s135 x) \<and> pspace_aligned' (?s135 x) \<and> is_aligned (armKSGlobalPD (ksArchState (?s135 x))) pdBits \<and> ?ptr135 x = armKSGlobalPD (ksArchState (?s135 x)) proof (prove)
goal (3 subgoals):
 1. \<And>x. \<lbrakk>armKSGlobalPD (ksArchState s') = armKSGlobalPD (ksArchState s); pspace_distinct' s; pspace_aligned' s; is_aligned (armKSGlobalPD (ksArchState s)) 14; is_aligned ptr 14; ksPSpace s' x = ksPSpace s' (armKSGlobalPD (ksArchState s) + (x && mask 14)); ptr + (x && mask 14) = x; ptr + (pptrBase >> 20 << 2) \<le> x; x \<le> 0x3FFF + ptr; ptr \<le> armKSGlobalPD (ksArchState s); armKSGlobalPD (ksArchState s) \<le> 0x3FFF + ptr && ~~ mask 14; armKSGlobalPD (ksArchState s) + (x && mask 14) && ~~ mask 14 = armKSGlobalPD (ksArchState s); armKSGlobalPD (ksArchState s) + (pptrBase >> 20 << 2) && ~~ mask 14 = armKSGlobalPD (ksArchState s); ptr + 0x3FFF && ~~ mask 14 = ptr; ptr + (pptrBase >> 20 << 2) && ~~ mask 14 = ptr\<rbrakk> \<Longrightarrow> (?r135 x, s') \<in> fst (copyGlobalMappings (?ptr135 x) (?s135 x))
 2. \<And>x. \<lbrakk>armKSGlobalPD (ksArchState s') = armKSGlobalPD (ksArchState s); pspace_distinct' s; pspace_aligned' s; is_aligned (armKSGlobalPD (ksArchState s)) 14; is_aligned ptr 14; ksPSpace s' x = ksPSpace s' (armKSGlobalPD (ksArchState s) + (x && mask 14)); ptr + (x && mask 14) = x; ptr + (pptrBase >> 20 << 2) \<le> x; x \<le> 0x3FFF + ptr; ptr \<le> armKSGlobalPD (ksArchState s); armKSGlobalPD (ksArchState s) \<le> 0x3FFF + ptr && ~~ mask 14; armKSGlobalPD (ksArchState s) + (x && mask 14) && ~~ mask 14 = armKSGlobalPD (ksArchState s); armKSGlobalPD (ksArchState s) + (pptrBase >> 20 << 2) && ~~ mask 14 = armKSGlobalPD (ksArchState s); ptr + 0x3FFF && ~~ mask 14 = ptr; ptr + (pptrBase >> 20 << 2) && ~~ mask 14 = ptr\<rbrakk> \<Longrightarrow> is_aligned (?ptr135 x) pdBits
 3. \<And>x. \<lbrakk>armKSGlobalPD (ksArchState s') = armKSGlobalPD (ksArchState s); pspace_distinct' s; pspace_aligned' s; is_aligned (armKSGlobalPD (ksArchState s)) 14; is_aligned ptr 14; ksPSpace s' x = ksPSpace s' (armKSGlobalPD (ksArchState s) + (x && mask 14)); ptr + (x && mask 14) = x; ptr + (pptrBase >> 20 << 2) \<le> x; x \<le> 0x3FFF + ptr; ptr \<le> armKSGlobalPD (ksArchState s); armKSGlobalPD (ksArchState s) \<le> 0x3FFF + ptr && ~~ mask 14; armKSGlobalPD (ksArchState s) + (x && mask 14) && ~~ mask 14 = armKSGlobalPD (ksArchState s); armKSGlobalPD (ksArchState s) + (pptrBase >> 20 << 2) && ~~ mask 14 = armKSGlobalPD (ksArchState s); ptr + 0x3FFF && ~~ mask 14 = ptr; ptr + (pptrBase >> 20 << 2) && ~~ mask 14 = ptr\<rbrakk> \<Longrightarrow> ksPSpace (?s135 x) (armKSGlobalPD (ksArchState s) + (x && mask 14)) = ksPSpace s (armKSGlobalPD (ksArchState s) + (x && mask 14)) \<and> pspace_distinct' (?s135 x) \<and> pspace_aligned' (?s135 x) \<and> is_aligned (armKSGlobalPD (ksArchState (?s135 x))) pdBits \<and> ?ptr135 x = armKSGlobalPD (ksArchState (?s135 x)) proof (prove)
goal (2 subgoals):
 1. \<And>x. \<lbrakk>armKSGlobalPD (ksArchState s') = armKSGlobalPD (ksArchState s); pspace_distinct' s; pspace_aligned' s; is_aligned (armKSGlobalPD (ksArchState s)) 14; is_aligned ptr 14; ksPSpace s' x = ksPSpace s' (armKSGlobalPD (ksArchState s) + (x && mask 14)); ptr + (x && mask 14) = x; ptr + (pptrBase >> 20 << 2) \<le> x; x \<le> 0x3FFF + ptr; ptr \<le> armKSGlobalPD (ksArchState s); armKSGlobalPD (ksArchState s) \<le> 0x3FFF + ptr && ~~ mask 14; armKSGlobalPD (ksArchState s) + (x && mask 14) && ~~ mask 14 = armKSGlobalPD (ksArchState s); armKSGlobalPD (ksArchState s) + (pptrBase >> 20 << 2) && ~~ mask 14 = armKSGlobalPD (ksArchState s); ptr + 0x3FFF && ~~ mask 14 = ptr; ptr + (pptrBase >> 20 << 2) && ~~ mask 14 = ptr\<rbrakk> \<Longrightarrow> is_aligned ptr pdBits
 2. \<And>x. \<lbrakk>armKSGlobalPD (ksArchState s') = armKSGlobalPD (ksArchState s); pspace_distinct' s; pspace_aligned' s; is_aligned (armKSGlobalPD (ksArchState s)) 14; is_aligned ptr 14; ksPSpace s' x = ksPSpace s' (armKSGlobalPD (ksArchState s) + (x && mask 14)); ptr + (x && mask 14) = x; ptr + (pptrBase >> 20 << 2) \<le> x; x \<le> 0x3FFF + ptr; ptr \<le> armKSGlobalPD (ksArchState s); armKSGlobalPD (ksArchState s) \<le> 0x3FFF + ptr && ~~ mask 14; armKSGlobalPD (ksArchState s) + (x && mask 14) && ~~ mask 14 = armKSGlobalPD (ksArchState s); armKSGlobalPD (ksArchState s) + (pptrBase >> 20 << 2) && ~~ mask 14 = armKSGlobalPD (ksArchState s); ptr + 0x3FFF && ~~ mask 14 = ptr; ptr + (pptrBase >> 20 << 2) && ~~ mask 14 = ptr\<rbrakk> \<Longrightarrow> ksPSpace s (armKSGlobalPD (ksArchState s) + (x && mask 14)) = ksPSpace s (armKSGlobalPD (ksArchState s) + (x && mask 14)) \<and> pspace_distinct' s \<and> pspace_aligned' s \<and> is_aligned (armKSGlobalPD (ksArchState s)) pdBits \<and> ptr = armKSGlobalPD (ksArchState s) proof (prove)
goal (1 subgoal):
 1. \<And>x. \<lbrakk>armKSGlobalPD (ksArchState s') = armKSGlobalPD (ksArchState s); pspace_distinct' s; pspace_aligned' s; is_aligned (armKSGlobalPD (ksArchState s)) 14; is_aligned ptr 14; ksPSpace s' x = ksPSpace s' (armKSGlobalPD (ksArchState s) + (x && mask 14)); ptr + (x && mask 14) = x; ptr + (pptrBase >> 20 << 2) \<le> x; x \<le> 0x3FFF + ptr; ptr \<le> armKSGlobalPD (ksArchState s); armKSGlobalPD (ksArchState s) \<le> 0x3FFF + ptr && ~~ mask 14; armKSGlobalPD (ksArchState s) + (x && mask 14) && ~~ mask 14 = armKSGlobalPD (ksArchState s); armKSGlobalPD (ksArchState s) + (pptrBase >> 20 << 2) && ~~ mask 14 = armKSGlobalPD (ksArchState s); ptr + 0x3FFF && ~~ mask 14 = ptr; ptr + (pptrBase >> 20 << 2) && ~~ mask 14 = ptr\<rbrakk> \<Longrightarrow> ksPSpace s (armKSGlobalPD (ksArchState s) + (x && mask 14)) = ksPSpace s (armKSGlobalPD (ksArchState s) + (x && mask 14)) \<and> pspace_distinct' s \<and> pspace_aligned' s \<and> is_aligned (armKSGlobalPD (ksArchState s)) pdBits \<and> ptr = armKSGlobalPD (ksArchState s) proof (prove)
goal:
No subgoals! proof (state)
this:
ksPSpace s' = (\<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)

goal:
No subgoals!