theory StoreWord_C

lemma storeByteUser_rf_sr_upd:
  assumes asms: "(\<sigma>, s) \<in> rf_sr" "pspace_aligned' \<sigma>" "pspace_distinct' \<sigma>"
                "pointerInUserData ptr \<sigma>"
  shows "(ksMachineState_update (underlying_memory_update (\<lambda>m. m(ptr := b))) \<sigma>,
          globals_update (t_hrs_'_update (hrs_mem_update (\<lambda>m. m(ptr := b)))) s)
         \<in> rf_sr" proof - have horrible_helper:
    "\<And>v p. v \<le> 3 \<Longrightarrow> (3 - unat (p && mask 2 :: word32) = v) =
                     (p && mask 2 = 3 - of_nat v)" apply (simp add: unat_arith_simps unat_of_nat) apply (cut_tac p=p in unat_mask_2_less_4) apply arith done have horrible_helper2:
    "\<And>n x p. n < 4 \<Longrightarrow> (unat (x - p :: word32) = n) = (x = (p + of_nat n))" apply (subst unat32_eq_of_nat) apply (simp add:word_bits_def) apply (simp only:field_simps) done from asms show ?thesis apply (frule_tac ptr="ptr && ~~ mask 2"
                 and w="word_rcat (list_update
                                    (map (underlying_memory (ksMachineState \<sigma>))
                                      [(ptr && ~~ mask 2) + 3,
                                       (ptr && ~~ mask 2) + 2,
                                       (ptr && ~~ mask 2) + 1,
                                       (ptr && ~~ mask 2)])
                                    (3 - unat (ptr && mask 2)) b)"
                  in storeWord_rf_sr_upd) apply simp+ apply (simp add: pointerInUserData_def pointerInDeviceData_def mask_lower_twice pageBits_def) apply (simp add: Aligned.is_aligned_neg_mask) apply (erule iffD1[rotated],
           rule_tac f="\<lambda>a b. (a, b) \<in> rf_sr" and c="globals_update f s"
                 for f s in arg_cong2) apply (rule kernel_state.fold_congs[OF refl refl], simp only:) apply (rule machine_state.fold_congs[OF refl refl], simp only:) apply (cut_tac p=ptr in unat_mask_2_less_4) apply (simp del: list_update.simps
                 add: word_rsplit_rcat_size word_size nth_list_update horrible_helper) apply (subgoal_tac "(ptr && ~~ mask 2) + (ptr && mask 2) = ptr") apply (subgoal_tac "(ptr && mask 2) \<in> {0, 1, 2, 3}") apply (auto split: if_split simp: fun_upd_idem)[1] apply (simp add: word_unat.Rep_inject[symmetric]
                  del: word_unat.Rep_inject) apply arith apply (subst add.commute, rule word_plus_and_or_coroll2) apply (rule StateSpace.state.fold_congs[OF refl refl]) apply (rule globals.fold_congs[OF refl refl]) apply (clarsimp simp: hrs_mem_update_def simp del: list_update.simps) apply (rule ext) apply (simp add: heap_update_def to_bytes_def typ_info_word
                     word_rsplit_rcat_size word_size heap_update_list_value'
                     nth_list_update nth_rev TWO
                del: list_update.simps) apply (subgoal_tac "length (rev ([underlying_memory (ksMachineState \<sigma>)
                                        ((ptr && ~~ mask 2) + 3),
                                      underlying_memory (ksMachineState \<sigma>)
                                        ((ptr && ~~ mask 2) + 2),
                                      underlying_memory (ksMachineState \<sigma>)
                                        ((ptr && ~~ mask 2) + 1),
                                      underlying_memory (ksMachineState \<sigma>)
                                        (ptr && ~~ mask 2)]
                                     [3 - unat (ptr && mask 2) := b]))
                        < addr_card") prefer 2 apply (simp add: addr_card del: list_update.simps) apply (simp add: heap_update_def to_bytes_def typ_info_word
                     word_rsplit_rcat_size word_size heap_update_list_value'
                     nth_list_update nth_rev TWO
                del: list_update.simps   cong: if_cong) apply (simp only: If_rearrage) apply (subgoal_tac "P" for P) apply (rule if_cong) apply assumption apply simp apply (clarsimp simp: nth_list_update split: if_split) apply (frule_tac ptr=x in memory_cross_over, simp+) apply (clarsimp simp: pointerInUserData_def pointerInDeviceData_def) apply (cut_tac p="ptr && ~~ mask 2" and n=2 and d="x - (ptr && ~~ mask 2)"
                  in is_aligned_add_helper) apply (simp add: Aligned.is_aligned_neg_mask) apply (simp add: word_less_nat_alt) apply clarsimp apply (cut_tac x=x in mask_lower_twice[where n=2 and m=pageBits]) apply (simp add: pageBits_def) apply (cut_tac x=ptr in mask_lower_twice[where n=2 and m=pageBits]) apply (simp add: pageBits_def) apply simp apply (auto simp add: eval_nat_numeral horrible_helper2 take_bit_Suc simp del: unsigned_numeral
                 elim!: less_SucE)[1] apply (rule iffI) apply clarsimp apply (cut_tac p=ptr in unat_mask_2_less_4) apply (subgoal_tac "unat (x - (ptr && ~~ mask 2)) = unat (ptr && mask 2)") prefer 2 apply arith apply (simp add: unat_mask_2_less_4 field_simps word_plus_and_or_coroll2) apply (simp add: subtract_mask TWO unat_mask_2_less_4) done qed

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. (ksMachineState_update (underlying_memory_update (\<lambda>m. m(ptr := b))) \<sigma>, globals_update (t_hrs_'_update (hrs_mem_update (\<lambda>m. m(ptr := b)))) s) \<in> rf_sr proof (state)
goal (1 subgoal):
 1. (ksMachineState_update (underlying_memory_update (\<lambda>m. m(ptr := b))) \<sigma>, globals_update (t_hrs_'_update (hrs_mem_update (\<lambda>m. m(ptr := b)))) s) \<in> rf_sr proof (prove)
goal (1 subgoal):
 1. \<And>v p. v \<le> 3 \<Longrightarrow> (3 - unat (p && mask 2) = v) = (p && mask 2 = 3 - word_of_nat v) proof (prove)
goal (1 subgoal):
 1. \<And>v p. v \<le> 3 \<Longrightarrow> (3 - unat (p && mask 2) = v) = (unat (p && mask 2) = 3 - v) proof (prove)
goal (1 subgoal):
 1. \<And>v p. \<lbrakk>v \<le> 3; unat (p && mask 2) < 4\<rbrakk> \<Longrightarrow> (3 - unat (p && mask 2) = v) = (unat (p && mask 2) = 3 - v) proof (prove)
goal:
No subgoals! proof (state)
this:
?v1 \<le> 3 \<Longrightarrow> (3 - unat (?p1 && mask 2) = ?v1) = (?p1 && mask 2 = 3 - word_of_nat ?v1)

goal (1 subgoal):
 1. (ksMachineState_update (underlying_memory_update (\<lambda>m. m(ptr := b))) \<sigma>, globals_update (t_hrs_'_update (hrs_mem_update (\<lambda>m. m(ptr := b)))) s) \<in> rf_sr proof (prove)
goal (1 subgoal):
 1. \<And>n x p. n < 4 \<Longrightarrow> (unat (x - p) = n) = (x = p + word_of_nat n) proof (prove)
goal (2 subgoals):
 1. \<And>n x p. n < 4 \<Longrightarrow> n < 2 ^ word_bits
 2. \<And>n x p. n < 4 \<Longrightarrow> (x - p = word_of_nat n) = (x = p + word_of_nat n) proof (prove)
goal (1 subgoal):
 1. \<And>n x p. n < 4 \<Longrightarrow> (x - p = word_of_nat n) = (x = p + word_of_nat n) proof (prove)
goal:
No subgoals! proof (state)
this:
?n1 < 4 \<Longrightarrow> (unat (?x1 - ?p1) = ?n1) = (?x1 = ?p1 + word_of_nat ?n1)

goal (1 subgoal):
 1. (ksMachineState_update (underlying_memory_update (\<lambda>m. m(ptr := b))) \<sigma>, globals_update (t_hrs_'_update (hrs_mem_update (\<lambda>m. m(ptr := b)))) s) \<in> rf_sr proof (chain)
picking this:
(\<sigma>, s) \<in> rf_sr
pspace_aligned' \<sigma>
pspace_distinct' \<sigma>
pointerInUserData ptr \<sigma> proof (prove)
using this:
(\<sigma>, s) \<in> rf_sr
pspace_aligned' \<sigma>
pspace_distinct' \<sigma>
pointerInUserData ptr \<sigma>

goal (1 subgoal):
 1. (ksMachineState_update (underlying_memory_update (\<lambda>m. m(ptr := b))) \<sigma>, globals_update (t_hrs_'_update (hrs_mem_update (\<lambda>m. m(ptr := b)))) s) \<in> rf_sr proof (prove)
goal (5 subgoals):
 1. \<lbrakk>(\<sigma>, s) \<in> rf_sr; pspace_aligned' \<sigma>; pspace_distinct' \<sigma>; pointerInUserData ptr \<sigma>\<rbrakk> \<Longrightarrow> pspace_aligned' \<sigma>
 2. \<lbrakk>(\<sigma>, s) \<in> rf_sr; pspace_aligned' \<sigma>; pspace_distinct' \<sigma>; pointerInUserData ptr \<sigma>\<rbrakk> \<Longrightarrow> pspace_distinct' \<sigma>
 3. \<lbrakk>(\<sigma>, s) \<in> rf_sr; pspace_aligned' \<sigma>; pspace_distinct' \<sigma>; pointerInUserData ptr \<sigma>\<rbrakk> \<Longrightarrow> pointerInUserData (ptr && ~~ mask 2) \<sigma> \<or> pointerInDeviceData (ptr && ~~ mask 2) \<sigma>
 4. \<lbrakk>(\<sigma>, s) \<in> rf_sr; pspace_aligned' \<sigma>; pspace_distinct' \<sigma>; pointerInUserData ptr \<sigma>\<rbrakk> \<Longrightarrow> is_aligned (ptr && ~~ mask 2) 2
 5. \<lbrakk>(\<sigma>, s) \<in> rf_sr; pspace_aligned' \<sigma>; pspace_distinct' \<sigma>; pointerInUserData ptr \<sigma>; (\<sigma>\<lparr>ksMachineState := underlying_memory_update (\<lambda>m. m(ptr && ~~ mask 2 := word_rsplit (word_rcat ((map (underlying_memory (ksMachineState \<sigma>)) [(ptr && ~~ mask 2) + 3, (ptr && ~~ mask 2) + 2, (ptr && ~~ mask 2) + 1, ptr && ~~ mask 2])[3 - unat (ptr && mask 2) := b])) ! 3, (ptr && ~~ mask 2) + 1 := word_rsplit (word_rcat ((map (underlying_memory (ksMachineState \<sigma>)) [(ptr && ~~ mask 2) + 3, (ptr && ~~ mask 2) + 2, (ptr && ~~ mask 2) + 1, ptr && ~~ mask 2])[3 - unat (ptr && mask 2) := b])) ! 2, (ptr && ~~ mask 2) + 2 := word_rsplit (word_rcat ((map (underlying_memory (ksMachineState \<sigma>)) [(ptr && ~~ mask 2) + 3, (ptr && ~~ mask 2) + 2, (ptr && ~~ mask 2) + 1, ptr && ~~ mask 2])[3 - unat (ptr && mask 2) := b])) ! Suc 0, (ptr && ~~ mask 2) + 3 := word_rsplit (word_rcat ((map (underlying_memory (ksMachineState \<sigma>)) [(ptr && ~~ mask 2) + 3, (ptr && ~~ mask 2) + 2, (ptr && ~~ mask 2) + 1, ptr && ~~ mask 2])[3 - unat (ptr && mask 2) := b])) ! 0)) (ksMachineState \<sigma>)\<rparr>, globals_update (t_hrs_'_update (hrs_mem_update (heap_update (PTR(32 word) (ptr && ~~ mask 2)) (word_rcat ((map (underlying_memory (ksMachineState \<sigma>)) [(ptr && ~~ mask 2) + 3, (ptr && ~~ mask 2) + 2, (ptr && ~~ mask 2) + 1, ptr && ~~ mask 2])[3 - unat (ptr && mask 2) := b]))))) s) \<in> rf_sr\<rbrakk> \<Longrightarrow> (ksMachineState_update (underlying_memory_update (\<lambda>m. m(ptr := b))) \<sigma>, globals_update (t_hrs_'_update (hrs_mem_update (\<lambda>m. m(ptr := b)))) s) \<in> rf_sr proof (prove)
goal (3 subgoals):
 1. \<lbrakk>(\<sigma>, s) \<in> rf_sr; pspace_aligned' \<sigma>; pspace_distinct' \<sigma>; pointerInUserData ptr \<sigma>\<rbrakk> \<Longrightarrow> pointerInUserData (ptr && ~~ mask 2) \<sigma> \<or> pointerInDeviceData (ptr && ~~ mask 2) \<sigma>
 2. \<lbrakk>(\<sigma>, s) \<in> rf_sr; pspace_aligned' \<sigma>; pspace_distinct' \<sigma>; pointerInUserData ptr \<sigma>\<rbrakk> \<Longrightarrow> is_aligned (ptr && ~~ mask 2) 2
 3. \<lbrakk>(\<sigma>, s) \<in> rf_sr; pspace_aligned' \<sigma>; pspace_distinct' \<sigma>; pointerInUserData ptr \<sigma>; (\<sigma>\<lparr>ksMachineState := underlying_memory_update (\<lambda>m. m(ptr && ~~ mask 2 := word_rsplit (word_rcat ((map (underlying_memory (ksMachineState \<sigma>)) [(ptr && ~~ mask 2) + 3, (ptr && ~~ mask 2) + 2, (ptr && ~~ mask 2) + 1, ptr && ~~ mask 2])[3 - unat (ptr && mask 2) := b])) ! 3, (ptr && ~~ mask 2) + 1 := word_rsplit (word_rcat ((map (underlying_memory (ksMachineState \<sigma>)) [(ptr && ~~ mask 2) + 3, (ptr && ~~ mask 2) + 2, (ptr && ~~ mask 2) + 1, ptr && ~~ mask 2])[3 - unat (ptr && mask 2) := b])) ! 2, (ptr && ~~ mask 2) + 2 := word_rsplit (word_rcat ((map (underlying_memory (ksMachineState \<sigma>)) [(ptr && ~~ mask 2) + 3, (ptr && ~~ mask 2) + 2, (ptr && ~~ mask 2) + 1, ptr && ~~ mask 2])[3 - unat (ptr && mask 2) := b])) ! Suc 0, (ptr && ~~ mask 2) + 3 := word_rsplit (word_rcat ((map (underlying_memory (ksMachineState \<sigma>)) [(ptr && ~~ mask 2) + 3, (ptr && ~~ mask 2) + 2, (ptr && ~~ mask 2) + 1, ptr && ~~ mask 2])[3 - unat (ptr && mask 2) := b])) ! 0)) (ksMachineState \<sigma>)\<rparr>, globals_update (t_hrs_'_update (hrs_mem_update (heap_update (PTR(32 word) (ptr && ~~ mask 2)) (word_rcat ((map (underlying_memory (ksMachineState \<sigma>)) [(ptr && ~~ mask 2) + 3, (ptr && ~~ mask 2) + 2, (ptr && ~~ mask 2) + 1, ptr && ~~ mask 2])[3 - unat (ptr && mask 2) := b]))))) s) \<in> rf_sr\<rbrakk> \<Longrightarrow> (ksMachineState_update (underlying_memory_update (\<lambda>m. m(ptr := b))) \<sigma>, globals_update (t_hrs_'_update (hrs_mem_update (\<lambda>m. m(ptr := b)))) s) \<in> rf_sr proof (prove)
goal (2 subgoals):
 1. \<lbrakk>(\<sigma>, s) \<in> rf_sr; pspace_aligned' \<sigma>; pspace_distinct' \<sigma>; pointerInUserData ptr \<sigma>\<rbrakk> \<Longrightarrow> is_aligned (ptr && ~~ mask 2) 2
 2. \<lbrakk>(\<sigma>, s) \<in> rf_sr; pspace_aligned' \<sigma>; pspace_distinct' \<sigma>; pointerInUserData ptr \<sigma>; (\<sigma>\<lparr>ksMachineState := underlying_memory_update (\<lambda>m. m(ptr && ~~ mask 2 := word_rsplit (word_rcat ((map (underlying_memory (ksMachineState \<sigma>)) [(ptr && ~~ mask 2) + 3, (ptr && ~~ mask 2) + 2, (ptr && ~~ mask 2) + 1, ptr && ~~ mask 2])[3 - unat (ptr && mask 2) := b])) ! 3, (ptr && ~~ mask 2) + 1 := word_rsplit (word_rcat ((map (underlying_memory (ksMachineState \<sigma>)) [(ptr && ~~ mask 2) + 3, (ptr && ~~ mask 2) + 2, (ptr && ~~ mask 2) + 1, ptr && ~~ mask 2])[3 - unat (ptr && mask 2) := b])) ! 2, (ptr && ~~ mask 2) + 2 := word_rsplit (word_rcat ((map (underlying_memory (ksMachineState \<sigma>)) [(ptr && ~~ mask 2) + 3, (ptr && ~~ mask 2) + 2, (ptr && ~~ mask 2) + 1, ptr && ~~ mask 2])[3 - unat (ptr && mask 2) := b])) ! Suc 0, (ptr && ~~ mask 2) + 3 := word_rsplit (word_rcat ((map (underlying_memory (ksMachineState \<sigma>)) [(ptr && ~~ mask 2) + 3, (ptr && ~~ mask 2) + 2, (ptr && ~~ mask 2) + 1, ptr && ~~ mask 2])[3 - unat (ptr && mask 2) := b])) ! 0)) (ksMachineState \<sigma>)\<rparr>, globals_update (t_hrs_'_update (hrs_mem_update (heap_update (PTR(32 word) (ptr && ~~ mask 2)) (word_rcat ((map (underlying_memory (ksMachineState \<sigma>)) [(ptr && ~~ mask 2) + 3, (ptr && ~~ mask 2) + 2, (ptr && ~~ mask 2) + 1, ptr && ~~ mask 2])[3 - unat (ptr && mask 2) := b]))))) s) \<in> rf_sr\<rbrakk> \<Longrightarrow> (ksMachineState_update (underlying_memory_update (\<lambda>m. m(ptr := b))) \<sigma>, globals_update (t_hrs_'_update (hrs_mem_update (\<lambda>m. m(ptr := b)))) s) \<in> rf_sr proof (prove)
goal (1 subgoal):
 1. \<lbrakk>(\<sigma>, s) \<in> rf_sr; pspace_aligned' \<sigma>; pspace_distinct' \<sigma>; pointerInUserData ptr \<sigma>; (\<sigma>\<lparr>ksMachineState := underlying_memory_update (\<lambda>m. m(ptr && ~~ mask 2 := word_rsplit (word_rcat ((map (underlying_memory (ksMachineState \<sigma>)) [(ptr && ~~ mask 2) + 3, (ptr && ~~ mask 2) + 2, (ptr && ~~ mask 2) + 1, ptr && ~~ mask 2])[3 - unat (ptr && mask 2) := b])) ! 3, (ptr && ~~ mask 2) + 1 := word_rsplit (word_rcat ((map (underlying_memory (ksMachineState \<sigma>)) [(ptr && ~~ mask 2) + 3, (ptr && ~~ mask 2) + 2, (ptr && ~~ mask 2) + 1, ptr && ~~ mask 2])[3 - unat (ptr && mask 2) := b])) ! 2, (ptr && ~~ mask 2) + 2 := word_rsplit (word_rcat ((map (underlying_memory (ksMachineState \<sigma>)) [(ptr && ~~ mask 2) + 3, (ptr && ~~ mask 2) + 2, (ptr && ~~ mask 2) + 1, ptr && ~~ mask 2])[3 - unat (ptr && mask 2) := b])) ! Suc 0, (ptr && ~~ mask 2) + 3 := word_rsplit (word_rcat ((map (underlying_memory (ksMachineState \<sigma>)) [(ptr && ~~ mask 2) + 3, (ptr && ~~ mask 2) + 2, (ptr && ~~ mask 2) + 1, ptr && ~~ mask 2])[3 - unat (ptr && mask 2) := b])) ! 0)) (ksMachineState \<sigma>)\<rparr>, globals_update (t_hrs_'_update (hrs_mem_update (heap_update (PTR(32 word) (ptr && ~~ mask 2)) (word_rcat ((map (underlying_memory (ksMachineState \<sigma>)) [(ptr && ~~ mask 2) + 3, (ptr && ~~ mask 2) + 2, (ptr && ~~ mask 2) + 1, ptr && ~~ mask 2])[3 - unat (ptr && mask 2) := b]))))) s) \<in> rf_sr\<rbrakk> \<Longrightarrow> (ksMachineState_update (underlying_memory_update (\<lambda>m. m(ptr := b))) \<sigma>, globals_update (t_hrs_'_update (hrs_mem_update (\<lambda>m. m(ptr := b)))) s) \<in> rf_sr proof (prove)
goal (2 subgoals):
 1. \<lbrakk>(\<sigma>, s) \<in> rf_sr; pspace_aligned' \<sigma>; pspace_distinct' \<sigma>; pointerInUserData ptr \<sigma>\<rbrakk> \<Longrightarrow> \<sigma>\<lparr>ksMachineState := underlying_memory_update (\<lambda>m. m(ptr && ~~ mask 2 := word_rsplit (word_rcat ((map (underlying_memory (ksMachineState \<sigma>)) [(ptr && ~~ mask 2) + 3, (ptr && ~~ mask 2) + 2, (ptr && ~~ mask 2) + 1, ptr && ~~ mask 2])[3 - unat (ptr && mask 2) := b])) ! 3, (ptr && ~~ mask 2) + 1 := word_rsplit (word_rcat ((map (underlying_memory (ksMachineState \<sigma>)) [(ptr && ~~ mask 2) + 3, (ptr && ~~ mask 2) + 2, (ptr && ~~ mask 2) + 1, ptr && ~~ mask 2])[3 - unat (ptr && mask 2) := b])) ! 2, (ptr && ~~ mask 2) + 2 := word_rsplit (word_rcat ((map (underlying_memory (ksMachineState \<sigma>)) [(ptr && ~~ mask 2) + 3, (ptr && ~~ mask 2) + 2, (ptr && ~~ mask 2) + 1, ptr && ~~ mask 2])[3 - unat (ptr && mask 2) := b])) ! Suc 0, (ptr && ~~ mask 2) + 3 := word_rsplit (word_rcat ((map (underlying_memory (ksMachineState \<sigma>)) [(ptr && ~~ mask 2) + 3, (ptr && ~~ mask 2) + 2, (ptr && ~~ mask 2) + 1, ptr && ~~ mask 2])[3 - unat (ptr && mask 2) := b])) ! 0)) (ksMachineState \<sigma>)\<rparr> = ksMachineState_update (underlying_memory_update (\<lambda>m. m(ptr := b))) \<sigma>
 2. \<lbrakk>(\<sigma>, s) \<in> rf_sr; pspace_aligned' \<sigma>; pspace_distinct' \<sigma>; pointerInUserData ptr \<sigma>\<rbrakk> \<Longrightarrow> globals_update (t_hrs_'_update (hrs_mem_update (heap_update (PTR(32 word) (ptr && ~~ mask 2)) (word_rcat ((map (underlying_memory (ksMachineState \<sigma>)) [(ptr && ~~ mask 2) + 3, (ptr && ~~ mask 2) + 2, (ptr && ~~ mask 2) + 1, ptr && ~~ mask 2])[3 - unat (ptr && mask 2) := b]))))) s = globals_update (t_hrs_'_update (hrs_mem_update (\<lambda>m. m(ptr := b)))) s proof (prove)
goal (2 subgoals):
 1. \<And>v. \<lbrakk>(\<sigma>, s) \<in> rf_sr; pspace_aligned' \<sigma>; pspace_distinct' \<sigma>; pointerInUserData ptr \<sigma>; ksMachineState \<sigma> = v\<rbrakk> \<Longrightarrow> underlying_memory_update (\<lambda>m. m(ptr && ~~ mask 2 := word_rsplit (word_rcat ((map (underlying_memory v) [(ptr && ~~ mask 2) + 3, (ptr && ~~ mask 2) + 2, (ptr && ~~ mask 2) + 1, ptr && ~~ mask 2])[3 - unat (ptr && mask 2) := b])) ! 3, (ptr && ~~ mask 2) + 1 := word_rsplit (word_rcat ((map (underlying_memory v) [(ptr && ~~ mask 2) + 3, (ptr && ~~ mask 2) + 2, (ptr && ~~ mask 2) + 1, ptr && ~~ mask 2])[3 - unat (ptr && mask 2) := b])) ! 2, (ptr && ~~ mask 2) + 2 := word_rsplit (word_rcat ((map (underlying_memory v) [(ptr && ~~ mask 2) + 3, (ptr && ~~ mask 2) + 2, (ptr && ~~ mask 2) + 1, ptr && ~~ mask 2])[3 - unat (ptr && mask 2) := b])) ! Suc 0, (ptr && ~~ mask 2) + 3 := word_rsplit (word_rcat ((map (underlying_memory v) [(ptr && ~~ mask 2) + 3, (ptr && ~~ mask 2) + 2, (ptr && ~~ mask 2) + 1, ptr && ~~ mask 2])[3 - unat (ptr && mask 2) := b])) ! 0)) v = underlying_memory_update (\<lambda>m. m(ptr := b)) v
 2. \<lbrakk>(\<sigma>, s) \<in> rf_sr; pspace_aligned' \<sigma>; pspace_distinct' \<sigma>; pointerInUserData ptr \<sigma>\<rbrakk> \<Longrightarrow> globals_update (t_hrs_'_update (hrs_mem_update (heap_update (PTR(32 word) (ptr && ~~ mask 2)) (word_rcat ((map (underlying_memory (ksMachineState \<sigma>)) [(ptr && ~~ mask 2) + 3, (ptr && ~~ mask 2) + 2, (ptr && ~~ mask 2) + 1, ptr && ~~ mask 2])[3 - unat (ptr && mask 2) := b]))))) s = globals_update (t_hrs_'_update (hrs_mem_update (\<lambda>m. m(ptr := b)))) s proof (prove)
goal (2 subgoals):
 1. \<And>v va. \<lbrakk>(\<sigma>, s) \<in> rf_sr; pspace_aligned' \<sigma>; pspace_distinct' \<sigma>; pointerInUserData ptr \<sigma>; ksMachineState \<sigma> = v; underlying_memory v = va\<rbrakk> \<Longrightarrow> va(ptr && ~~ mask 2 := word_rsplit (word_rcat ((map va [(ptr && ~~ mask 2) + 3, (ptr && ~~ mask 2) + 2, (ptr && ~~ mask 2) + 1, ptr && ~~ mask 2])[3 - unat (ptr && mask 2) := b])) ! 3, (ptr && ~~ mask 2) + 1 := word_rsplit (word_rcat ((map va [(ptr && ~~ mask 2) + 3, (ptr && ~~ mask 2) + 2, (ptr && ~~ mask 2) + 1, ptr && ~~ mask 2])[3 - unat (ptr && mask 2) := b])) ! 2, (ptr && ~~ mask 2) + 2 := word_rsplit (word_rcat ((map va [(ptr && ~~ mask 2) + 3, (ptr && ~~ mask 2) + 2, (ptr && ~~ mask 2) + 1, ptr && ~~ mask 2])[3 - unat (ptr && mask 2) := b])) ! Suc 0, (ptr && ~~ mask 2) + 3 := word_rsplit (word_rcat ((map va [(ptr && ~~ mask 2) + 3, (ptr && ~~ mask 2) + 2, (ptr && ~~ mask 2) + 1, ptr && ~~ mask 2])[3 - unat (ptr && mask 2) := b])) ! 0) = va(ptr := b)
 2. \<lbrakk>(\<sigma>, s) \<in> rf_sr; pspace_aligned' \<sigma>; pspace_distinct' \<sigma>; pointerInUserData ptr \<sigma>\<rbrakk> \<Longrightarrow> globals_update (t_hrs_'_update (hrs_mem_update (heap_update (PTR(32 word) (ptr && ~~ mask 2)) (word_rcat ((map (underlying_memory (ksMachineState \<sigma>)) [(ptr && ~~ mask 2) + 3, (ptr && ~~ mask 2) + 2, (ptr && ~~ mask 2) + 1, ptr && ~~ mask 2])[3 - unat (ptr && mask 2) := b]))))) s = globals_update (t_hrs_'_update (hrs_mem_update (\<lambda>m. m(ptr := b)))) s proof (prove)
goal (2 subgoals):
 1. \<And>v va. \<lbrakk>(\<sigma>, s) \<in> rf_sr; pspace_aligned' \<sigma>; pspace_distinct' \<sigma>; pointerInUserData ptr \<sigma>; ksMachineState \<sigma> = v; underlying_memory v = va; unat (ptr && mask 2) < 4\<rbrakk> \<Longrightarrow> va(ptr && ~~ mask 2 := word_rsplit (word_rcat ((map va [(ptr && ~~ mask 2) + 3, (ptr && ~~ mask 2) + 2, (ptr && ~~ mask 2) + 1, ptr && ~~ mask 2])[3 - unat (ptr && mask 2) := b])) ! 3, (ptr && ~~ mask 2) + 1 := word_rsplit (word_rcat ((map va [(ptr && ~~ mask 2) + 3, (ptr && ~~ mask 2) + 2, (ptr && ~~ mask 2) + 1, ptr && ~~ mask 2])[3 - unat (ptr && mask 2) := b])) ! 2, (ptr && ~~ mask 2) + 2 := word_rsplit (word_rcat ((map va [(ptr && ~~ mask 2) + 3, (ptr && ~~ mask 2) + 2, (ptr && ~~ mask 2) + 1, ptr && ~~ mask 2])[3 - unat (ptr && mask 2) := b])) ! Suc 0, (ptr && ~~ mask 2) + 3 := word_rsplit (word_rcat ((map va [(ptr && ~~ mask 2) + 3, (ptr && ~~ mask 2) + 2, (ptr && ~~ mask 2) + 1, ptr && ~~ mask 2])[3 - unat (ptr && mask 2) := b])) ! 0) = va(ptr := b)
 2. \<lbrakk>(\<sigma>, s) \<in> rf_sr; pspace_aligned' \<sigma>; pspace_distinct' \<sigma>; pointerInUserData ptr \<sigma>\<rbrakk> \<Longrightarrow> globals_update (t_hrs_'_update (hrs_mem_update (heap_update (PTR(32 word) (ptr && ~~ mask 2)) (word_rcat ((map (underlying_memory (ksMachineState \<sigma>)) [(ptr && ~~ mask 2) + 3, (ptr && ~~ mask 2) + 2, (ptr && ~~ mask 2) + 1, ptr && ~~ mask 2])[3 - unat (ptr && mask 2) := b]))))) s = globals_update (t_hrs_'_update (hrs_mem_update (\<lambda>m. m(ptr := b)))) s proof (prove)
goal (2 subgoals):
 1. \<And>v va. \<lbrakk>(\<sigma>, s) \<in> rf_sr; pspace_aligned' \<sigma>; pspace_distinct' \<sigma>; pointerInUserData ptr \<sigma>; ksMachineState \<sigma> = v; underlying_memory v = va; unat (ptr && mask 2) < 4\<rbrakk> \<Longrightarrow> va(ptr && ~~ mask 2 := if ptr && mask 2 = 0 then b else [va ((ptr && ~~ mask 2) + 3), va ((ptr && ~~ mask 2) + 2), va ((ptr && ~~ mask 2) + 1), va (ptr && ~~ mask 2)] ! 3, (ptr && ~~ mask 2) + 1 := if ptr && mask 2 = 1 then b else [va ((ptr && ~~ mask 2) + 3), va ((ptr && ~~ mask 2) + 2), va ((ptr && ~~ mask 2) + 1), va (ptr && ~~ mask 2)] ! 2, (ptr && ~~ mask 2) + 2 := if ptr && mask 2 = 2 then b else [va ((ptr && ~~ mask 2) + 3), va ((ptr && ~~ mask 2) + 2), va ((ptr && ~~ mask 2) + 1), va (ptr && ~~ mask 2)] ! Suc 0, (ptr && ~~ mask 2) + 3 := if 3 \<le> unat (ptr && mask 2) then b else [va ((ptr && ~~ mask 2) + 3), va ((ptr && ~~ mask 2) + 2), va ((ptr && ~~ mask 2) + 1), va (ptr && ~~ mask 2)] ! 0) = va(ptr := b)
 2. \<lbrakk>(\<sigma>, s) \<in> rf_sr; pspace_aligned' \<sigma>; pspace_distinct' \<sigma>; pointerInUserData ptr \<sigma>\<rbrakk> \<Longrightarrow> globals_update (t_hrs_'_update (hrs_mem_update (heap_update (PTR(32 word) (ptr && ~~ mask 2)) (word_rcat ((map (underlying_memory (ksMachineState \<sigma>)) [(ptr && ~~ mask 2) + 3, (ptr && ~~ mask 2) + 2, (ptr && ~~ mask 2) + 1, ptr && ~~ mask 2])[3 - unat (ptr && mask 2) := b]))))) s = globals_update (t_hrs_'_update (hrs_mem_update (\<lambda>m. m(ptr := b)))) s proof (prove)
goal (3 subgoals):
 1. \<And>v va. \<lbrakk>(\<sigma>, s) \<in> rf_sr; pspace_aligned' \<sigma>; pspace_distinct' \<sigma>; pointerInUserData ptr \<sigma>; ksMachineState \<sigma> = v; underlying_memory v = va; unat (ptr && mask 2) < 4; (ptr && ~~ mask 2) + (ptr && mask 2) = ptr\<rbrakk> \<Longrightarrow> va(ptr && ~~ mask 2 := if ptr && mask 2 = 0 then b else [va ((ptr && ~~ mask 2) + 3), va ((ptr && ~~ mask 2) + 2), va ((ptr && ~~ mask 2) + 1), va (ptr && ~~ mask 2)] ! 3, (ptr && ~~ mask 2) + 1 := if ptr && mask 2 = 1 then b else [va ((ptr && ~~ mask 2) + 3), va ((ptr && ~~ mask 2) + 2), va ((ptr && ~~ mask 2) + 1), va (ptr && ~~ mask 2)] ! 2, (ptr && ~~ mask 2) + 2 := if ptr && mask 2 = 2 then b else [va ((ptr && ~~ mask 2) + 3), va ((ptr && ~~ mask 2) + 2), va ((ptr && ~~ mask 2) + 1), va (ptr && ~~ mask 2)] ! Suc 0, (ptr && ~~ mask 2) + 3 := if 3 \<le> unat (ptr && mask 2) then b else [va ((ptr && ~~ mask 2) + 3), va ((ptr && ~~ mask 2) + 2), va ((ptr && ~~ mask 2) + 1), va (ptr && ~~ mask 2)] ! 0) = va(ptr := b)
 2. \<And>v va. \<lbrakk>(\<sigma>, s) \<in> rf_sr; pspace_aligned' \<sigma>; pspace_distinct' \<sigma>; pointerInUserData ptr \<sigma>; ksMachineState \<sigma> = v; underlying_memory v = va; unat (ptr && mask 2) < 4\<rbrakk> \<Longrightarrow> (ptr && ~~ mask 2) + (ptr && mask 2) = ptr
 3. \<lbrakk>(\<sigma>, s) \<in> rf_sr; pspace_aligned' \<sigma>; pspace_distinct' \<sigma>; pointerInUserData ptr \<sigma>\<rbrakk> \<Longrightarrow> globals_update (t_hrs_'_update (hrs_mem_update (heap_update (PTR(32 word) (ptr && ~~ mask 2)) (word_rcat ((map (underlying_memory (ksMachineState \<sigma>)) [(ptr && ~~ mask 2) + 3, (ptr && ~~ mask 2) + 2, (ptr && ~~ mask 2) + 1, ptr && ~~ mask 2])[3 - unat (ptr && mask 2) := b]))))) s = globals_update (t_hrs_'_update (hrs_mem_update (\<lambda>m. m(ptr := b)))) s proof (prove)
goal (4 subgoals):
 1. \<And>v va. \<lbrakk>(\<sigma>, s) \<in> rf_sr; pspace_aligned' \<sigma>; pspace_distinct' \<sigma>; pointerInUserData ptr \<sigma>; ksMachineState \<sigma> = v; underlying_memory v = va; unat (ptr && mask 2) < 4; (ptr && ~~ mask 2) + (ptr && mask 2) = ptr; ptr && mask 2 \<in> {0, 1, 2, 3}\<rbrakk> \<Longrightarrow> va(ptr && ~~ mask 2 := if ptr && mask 2 = 0 then b else [va ((ptr && ~~ mask 2) + 3), va ((ptr && ~~ mask 2) + 2), va ((ptr && ~~ mask 2) + 1), va (ptr && ~~ mask 2)] ! 3, (ptr && ~~ mask 2) + 1 := if ptr && mask 2 = 1 then b else [va ((ptr && ~~ mask 2) + 3), va ((ptr && ~~ mask 2) + 2), va ((ptr && ~~ mask 2) + 1), va (ptr && ~~ mask 2)] ! 2, (ptr && ~~ mask 2) + 2 := if ptr && mask 2 = 2 then b else [va ((ptr && ~~ mask 2) + 3), va ((ptr && ~~ mask 2) + 2), va ((ptr && ~~ mask 2) + 1), va (ptr && ~~ mask 2)] ! Suc 0, (ptr && ~~ mask 2) + 3 := if 3 \<le> unat (ptr && mask 2) then b else [va ((ptr && ~~ mask 2) + 3), va ((ptr && ~~ mask 2) + 2), va ((ptr && ~~ mask 2) + 1), va (ptr && ~~ mask 2)] ! 0) = va(ptr := b)
 2. \<And>v va. \<lbrakk>(\<sigma>, s) \<in> rf_sr; pspace_aligned' \<sigma>; pspace_distinct' \<sigma>; pointerInUserData ptr \<sigma>; ksMachineState \<sigma> = v; underlying_memory v = va; unat (ptr && mask 2) < 4; (ptr && ~~ mask 2) + (ptr && mask 2) = ptr\<rbrakk> \<Longrightarrow> ptr && mask 2 \<in> {0, 1, 2, 3}
 3. \<And>v va. \<lbrakk>(\<sigma>, s) \<in> rf_sr; pspace_aligned' \<sigma>; pspace_distinct' \<sigma>; pointerInUserData ptr \<sigma>; ksMachineState \<sigma> = v; underlying_memory v = va; unat (ptr && mask 2) < 4\<rbrakk> \<Longrightarrow> (ptr && ~~ mask 2) + (ptr && mask 2) = ptr
 4. \<lbrakk>(\<sigma>, s) \<in> rf_sr; pspace_aligned' \<sigma>; pspace_distinct' \<sigma>; pointerInUserData ptr \<sigma>\<rbrakk> \<Longrightarrow> globals_update (t_hrs_'_update (hrs_mem_update (heap_update (PTR(32 word) (ptr && ~~ mask 2)) (word_rcat ((map (underlying_memory (ksMachineState \<sigma>)) [(ptr && ~~ mask 2) + 3, (ptr && ~~ mask 2) + 2, (ptr && ~~ mask 2) + 1, ptr && ~~ mask 2])[3 - unat (ptr && mask 2) := b]))))) s = globals_update (t_hrs_'_update (hrs_mem_update (\<lambda>m. m(ptr := b)))) s proof (prove)
goal (3 subgoals):
 1. \<And>v va. \<lbrakk>(\<sigma>, s) \<in> rf_sr; pspace_aligned' \<sigma>; pspace_distinct' \<sigma>; pointerInUserData ptr \<sigma>; ksMachineState \<sigma> = v; underlying_memory v = va; unat (ptr && mask 2) < 4; (ptr && ~~ mask 2) + (ptr && mask 2) = ptr\<rbrakk> \<Longrightarrow> ptr && mask 2 \<in> {0, 1, 2, 3}
 2. \<And>v va. \<lbrakk>(\<sigma>, s) \<in> rf_sr; pspace_aligned' \<sigma>; pspace_distinct' \<sigma>; pointerInUserData ptr \<sigma>; ksMachineState \<sigma> = v; underlying_memory v = va; unat (ptr && mask 2) < 4\<rbrakk> \<Longrightarrow> (ptr && ~~ mask 2) + (ptr && mask 2) = ptr
 3. \<lbrakk>(\<sigma>, s) \<in> rf_sr; pspace_aligned' \<sigma>; pspace_distinct' \<sigma>; pointerInUserData ptr \<sigma>\<rbrakk> \<Longrightarrow> globals_update (t_hrs_'_update (hrs_mem_update (heap_update (PTR(32 word) (ptr && ~~ mask 2)) (word_rcat ((map (underlying_memory (ksMachineState \<sigma>)) [(ptr && ~~ mask 2) + 3, (ptr && ~~ mask 2) + 2, (ptr && ~~ mask 2) + 1, ptr && ~~ mask 2])[3 - unat (ptr && mask 2) := b]))))) s = globals_update (t_hrs_'_update (hrs_mem_update (\<lambda>m. m(ptr := b)))) s proof (prove)
goal (3 subgoals):
 1. \<And>v va. \<lbrakk>(\<sigma>, s) \<in> rf_sr; pspace_aligned' \<sigma>; pspace_distinct' \<sigma>; pointerInUserData ptr \<sigma>; ksMachineState \<sigma> = v; underlying_memory v = va; unat (ptr && mask 2) < 4; unat ((ptr && ~~ mask 2) + (ptr && mask 2)) = unat ptr\<rbrakk> \<Longrightarrow> unat (ptr && mask 2) = 0 \<or> unat (ptr && mask 2) = Suc 0 \<or> unat (ptr && mask 2) = 2 \<or> unat (ptr && mask 2) = 3
 2. \<And>v va. \<lbrakk>(\<sigma>, s) \<in> rf_sr; pspace_aligned' \<sigma>; pspace_distinct' \<sigma>; pointerInUserData ptr \<sigma>; ksMachineState \<sigma> = v; underlying_memory v = va; unat (ptr && mask 2) < 4\<rbrakk> \<Longrightarrow> (ptr && ~~ mask 2) + (ptr && mask 2) = ptr
 3. \<lbrakk>(\<sigma>, s) \<in> rf_sr; pspace_aligned' \<sigma>; pspace_distinct' \<sigma>; pointerInUserData ptr \<sigma>\<rbrakk> \<Longrightarrow> globals_update (t_hrs_'_update (hrs_mem_update (heap_update (PTR(32 word) (ptr && ~~ mask 2)) (word_rcat ((map (underlying_memory (ksMachineState \<sigma>)) [(ptr && ~~ mask 2) + 3, (ptr && ~~ mask 2) + 2, (ptr && ~~ mask 2) + 1, ptr && ~~ mask 2])[3 - unat (ptr && mask 2) := b]))))) s = globals_update (t_hrs_'_update (hrs_mem_update (\<lambda>m. m(ptr := b)))) s proof (prove)
goal (2 subgoals):
 1. \<And>v va. \<lbrakk>(\<sigma>, s) \<in> rf_sr; pspace_aligned' \<sigma>; pspace_distinct' \<sigma>; pointerInUserData ptr \<sigma>; ksMachineState \<sigma> = v; underlying_memory v = va; unat (ptr && mask 2) < 4\<rbrakk> \<Longrightarrow> (ptr && ~~ mask 2) + (ptr && mask 2) = ptr
 2. \<lbrakk>(\<sigma>, s) \<in> rf_sr; pspace_aligned' \<sigma>; pspace_distinct' \<sigma>; pointerInUserData ptr \<sigma>\<rbrakk> \<Longrightarrow> globals_update (t_hrs_'_update (hrs_mem_update (heap_update (PTR(32 word) (ptr && ~~ mask 2)) (word_rcat ((map (underlying_memory (ksMachineState \<sigma>)) [(ptr && ~~ mask 2) + 3, (ptr && ~~ mask 2) + 2, (ptr && ~~ mask 2) + 1, ptr && ~~ mask 2])[3 - unat (ptr && mask 2) := b]))))) s = globals_update (t_hrs_'_update (hrs_mem_update (\<lambda>m. m(ptr := b)))) s proof (prove)
goal (1 subgoal):
 1. \<lbrakk>(\<sigma>, s) \<in> rf_sr; pspace_aligned' \<sigma>; pspace_distinct' \<sigma>; pointerInUserData ptr \<sigma>\<rbrakk> \<Longrightarrow> globals_update (t_hrs_'_update (hrs_mem_update (heap_update (PTR(32 word) (ptr && ~~ mask 2)) (word_rcat ((map (underlying_memory (ksMachineState \<sigma>)) [(ptr && ~~ mask 2) + 3, (ptr && ~~ mask 2) + 2, (ptr && ~~ mask 2) + 1, ptr && ~~ mask 2])[3 - unat (ptr && mask 2) := b]))))) s = globals_update (t_hrs_'_update (hrs_mem_update (\<lambda>m. m(ptr := b)))) s proof (prove)
goal (1 subgoal):
 1. \<And>v. \<lbrakk>(\<sigma>, s) \<in> rf_sr; pspace_aligned' \<sigma>; pspace_distinct' \<sigma>; pointerInUserData ptr \<sigma>; globals s = v\<rbrakk> \<Longrightarrow> t_hrs_'_update (hrs_mem_update (heap_update (PTR(32 word) (ptr && ~~ mask 2)) (word_rcat ((map (underlying_memory (ksMachineState \<sigma>)) [(ptr && ~~ mask 2) + 3, (ptr && ~~ mask 2) + 2, (ptr && ~~ mask 2) + 1, ptr && ~~ mask 2])[3 - unat (ptr && mask 2) := b])))) v = t_hrs_'_update (hrs_mem_update (\<lambda>m. m(ptr := b))) v proof (prove)
goal (1 subgoal):
 1. \<And>v va. \<lbrakk>(\<sigma>, s) \<in> rf_sr; pspace_aligned' \<sigma>; pspace_distinct' \<sigma>; pointerInUserData ptr \<sigma>; globals s = v; t_hrs_' v = va\<rbrakk> \<Longrightarrow> hrs_mem_update (heap_update (PTR(32 word) (ptr && ~~ mask 2)) (word_rcat ((map (underlying_memory (ksMachineState \<sigma>)) [(ptr && ~~ mask 2) + 3, (ptr && ~~ mask 2) + 2, (ptr && ~~ mask 2) + 1, ptr && ~~ mask 2])[3 - unat (ptr && mask 2) := b]))) va = hrs_mem_update (\<lambda>m. m(ptr := b)) va proof (prove)
goal (1 subgoal):
 1. \<And>a ba. \<lbrakk>(\<sigma>, s) \<in> rf_sr; pspace_aligned' \<sigma>; pspace_distinct' \<sigma>; pointerInUserData ptr \<sigma>; t_hrs_' (globals s) = (a, ba)\<rbrakk> \<Longrightarrow> heap_update (PTR(32 word) (ptr && ~~ mask 2)) (word_rcat ([underlying_memory (ksMachineState \<sigma>) ((ptr && ~~ mask 2) + 3), underlying_memory (ksMachineState \<sigma>) ((ptr && ~~ mask 2) + 2), underlying_memory (ksMachineState \<sigma>) ((ptr && ~~ mask 2) + 1), underlying_memory (ksMachineState \<sigma>) (ptr && ~~ mask 2)][3 - unat (ptr && mask 2) := b])) a = a(ptr := b) proof (prove)
goal (1 subgoal):
 1. \<And>a ba x. \<lbrakk>(\<sigma>, s) \<in> rf_sr; pspace_aligned' \<sigma>; pspace_distinct' \<sigma>; pointerInUserData ptr \<sigma>; t_hrs_' (globals s) = (a, ba)\<rbrakk> \<Longrightarrow> heap_update (PTR(32 word) (ptr && ~~ mask 2)) (word_rcat ([underlying_memory (ksMachineState \<sigma>) ((ptr && ~~ mask 2) + 3), underlying_memory (ksMachineState \<sigma>) ((ptr && ~~ mask 2) + 2), underlying_memory (ksMachineState \<sigma>) ((ptr && ~~ mask 2) + 1), underlying_memory (ksMachineState \<sigma>) (ptr && ~~ mask 2)][3 - unat (ptr && mask 2) := b])) a x = (a(ptr := b)) x proof (prove)
goal (1 subgoal):
 1. \<And>a ba x. \<lbrakk>(\<sigma>, s) \<in> rf_sr; pspace_aligned' \<sigma>; pspace_distinct' \<sigma>; pointerInUserData ptr \<sigma>; t_hrs_' (globals s) = (a, ba)\<rbrakk> \<Longrightarrow> heap_update_list (ptr && ~~ mask 2) (rev ([underlying_memory (ksMachineState \<sigma>) ((ptr && ~~ mask 2) + 3), underlying_memory (ksMachineState \<sigma>) ((ptr && ~~ mask 2) + 2), underlying_memory (ksMachineState \<sigma>) ((ptr && ~~ mask 2) + 1), underlying_memory (ksMachineState \<sigma>) (ptr && ~~ mask 2)][3 - unat (ptr && mask 2) := b])) a x = (if x = ptr then b else a x) proof (prove)
goal (2 subgoals):
 1. \<And>a ba x. \<lbrakk>(\<sigma>, s) \<in> rf_sr; pspace_aligned' \<sigma>; pspace_distinct' \<sigma>; pointerInUserData ptr \<sigma>; t_hrs_' (globals s) = (a, ba); length (rev ([underlying_memory (ksMachineState \<sigma>) ((ptr && ~~ mask 2) + 3), underlying_memory (ksMachineState \<sigma>) ((ptr && ~~ mask 2) + 2), underlying_memory (ksMachineState \<sigma>) ((ptr && ~~ mask 2) + 1), underlying_memory (ksMachineState \<sigma>) (ptr && ~~ mask 2)][3 - unat (ptr && mask 2) := b])) < addr_card\<rbrakk> \<Longrightarrow> heap_update_list (ptr && ~~ mask 2) (rev ([underlying_memory (ksMachineState \<sigma>) ((ptr && ~~ mask 2) + 3), underlying_memory (ksMachineState \<sigma>) ((ptr && ~~ mask 2) + 2), underlying_memory (ksMachineState \<sigma>) ((ptr && ~~ mask 2) + 1), underlying_memory (ksMachineState \<sigma>) (ptr && ~~ mask 2)][3 - unat (ptr && mask 2) := b])) a x = (if x = ptr then b else a x)
 2. \<And>a ba x. \<lbrakk>(\<sigma>, s) \<in> rf_sr; pspace_aligned' \<sigma>; pspace_distinct' \<sigma>; pointerInUserData ptr \<sigma>; t_hrs_' (globals s) = (a, ba)\<rbrakk> \<Longrightarrow> length (rev ([underlying_memory (ksMachineState \<sigma>) ((ptr && ~~ mask 2) + 3), underlying_memory (ksMachineState \<sigma>) ((ptr && ~~ mask 2) + 2), underlying_memory (ksMachineState \<sigma>) ((ptr && ~~ mask 2) + 1), underlying_memory (ksMachineState \<sigma>) (ptr && ~~ mask 2)][3 - unat (ptr && mask 2) := b])) < addr_card proof (prove)
goal (2 subgoals):
 1. \<And>a ba x. \<lbrakk>(\<sigma>, s) \<in> rf_sr; pspace_aligned' \<sigma>; pspace_distinct' \<sigma>; pointerInUserData ptr \<sigma>; t_hrs_' (globals s) = (a, ba)\<rbrakk> \<Longrightarrow> length (rev ([underlying_memory (ksMachineState \<sigma>) ((ptr && ~~ mask 2) + 3), underlying_memory (ksMachineState \<sigma>) ((ptr && ~~ mask 2) + 2), underlying_memory (ksMachineState \<sigma>) ((ptr && ~~ mask 2) + 1), underlying_memory (ksMachineState \<sigma>) (ptr && ~~ mask 2)][3 - unat (ptr && mask 2) := b])) < addr_card
 2. \<And>a ba x. \<lbrakk>(\<sigma>, s) \<in> rf_sr; pspace_aligned' \<sigma>; pspace_distinct' \<sigma>; pointerInUserData ptr \<sigma>; t_hrs_' (globals s) = (a, ba); length (rev ([underlying_memory (ksMachineState \<sigma>) ((ptr && ~~ mask 2) + 3), underlying_memory (ksMachineState \<sigma>) ((ptr && ~~ mask 2) + 2), underlying_memory (ksMachineState \<sigma>) ((ptr && ~~ mask 2) + 1), underlying_memory (ksMachineState \<sigma>) (ptr && ~~ mask 2)][3 - unat (ptr && mask 2) := b])) < addr_card\<rbrakk> \<Longrightarrow> heap_update_list (ptr && ~~ mask 2) (rev ([underlying_memory (ksMachineState \<sigma>) ((ptr && ~~ mask 2) + 3), underlying_memory (ksMachineState \<sigma>) ((ptr && ~~ mask 2) + 2), underlying_memory (ksMachineState \<sigma>) ((ptr && ~~ mask 2) + 1), underlying_memory (ksMachineState \<sigma>) (ptr && ~~ mask 2)][3 - unat (ptr && mask 2) := b])) a x = (if x = ptr then b else a x) proof (prove)
goal (1 subgoal):
 1. \<And>a ba x. \<lbrakk>(\<sigma>, s) \<in> rf_sr; pspace_aligned' \<sigma>; pspace_distinct' \<sigma>; pointerInUserData ptr \<sigma>; t_hrs_' (globals s) = (a, ba); length (rev ([underlying_memory (ksMachineState \<sigma>) ((ptr && ~~ mask 2) + 3), underlying_memory (ksMachineState \<sigma>) ((ptr && ~~ mask 2) + 2), underlying_memory (ksMachineState \<sigma>) ((ptr && ~~ mask 2) + 1), underlying_memory (ksMachineState \<sigma>) (ptr && ~~ mask 2)][3 - unat (ptr && mask 2) := b])) < addr_card\<rbrakk> \<Longrightarrow> heap_update_list (ptr && ~~ mask 2) (rev ([underlying_memory (ksMachineState \<sigma>) ((ptr && ~~ mask 2) + 3), underlying_memory (ksMachineState \<sigma>) ((ptr && ~~ mask 2) + 2), underlying_memory (ksMachineState \<sigma>) ((ptr && ~~ mask 2) + 1), underlying_memory (ksMachineState \<sigma>) (ptr && ~~ mask 2)][3 - unat (ptr && mask 2) := b])) a x = (if x = ptr then b else a x) proof (prove)
goal (1 subgoal):
 1. \<And>a ba x. \<lbrakk>(\<sigma>, s) \<in> rf_sr; pspace_aligned' \<sigma>; pspace_distinct' \<sigma>; pointerInUserData ptr \<sigma>; t_hrs_' (globals s) = (a, ba); 4 < addr_card\<rbrakk> \<Longrightarrow> (if unat (x - (ptr && ~~ mask 2)) < 4 then if 3 - unat (ptr && mask 2) = 3 - unat (x - (ptr && ~~ mask 2)) then b else [underlying_memory (ksMachineState \<sigma>) ((ptr && ~~ mask 2) + 3), underlying_memory (ksMachineState \<sigma>) ((ptr && ~~ mask 2) + 2), underlying_memory (ksMachineState \<sigma>) ((ptr && ~~ mask 2) + 1), underlying_memory (ksMachineState \<sigma>) (ptr && ~~ mask 2)] ! (3 - unat (x - (ptr && ~~ mask 2))) else a x) = (if x = ptr then b else a x) proof (prove)
goal (1 subgoal):
 1. \<And>a ba x. \<lbrakk>(\<sigma>, s) \<in> rf_sr; pspace_aligned' \<sigma>; pspace_distinct' \<sigma>; pointerInUserData ptr \<sigma>; t_hrs_' (globals s) = (a, ba); 4 < addr_card\<rbrakk> \<Longrightarrow> (if unat (x - (ptr && ~~ mask 2)) < 4 \<and> 3 - unat (ptr && mask 2) = 3 - unat (x - (ptr && ~~ mask 2)) then b else if unat (x - (ptr && ~~ mask 2)) < 4 then [underlying_memory (ksMachineState \<sigma>) ((ptr && ~~ mask 2) + 3), underlying_memory (ksMachineState \<sigma>) ((ptr && ~~ mask 2) + 2), underlying_memory (ksMachineState \<sigma>) ((ptr && ~~ mask 2) + 1), underlying_memory (ksMachineState \<sigma>) (ptr && ~~ mask 2)] ! (3 - unat (x - (ptr && ~~ mask 2))) else a x) = (if x = ptr then b else a x) proof (prove)
goal (2 subgoals):
 1. \<And>a ba x. \<lbrakk>(\<sigma>, s) \<in> rf_sr; pspace_aligned' \<sigma>; pspace_distinct' \<sigma>; pointerInUserData ptr \<sigma>; t_hrs_' (globals s) = (a, ba); 4 < addr_card; ?P171 a ba x\<rbrakk> \<Longrightarrow> (if unat (x - (ptr && ~~ mask 2)) < 4 \<and> 3 - unat (ptr && mask 2) = 3 - unat (x - (ptr && ~~ mask 2)) then b else if unat (x - (ptr && ~~ mask 2)) < 4 then [underlying_memory (ksMachineState \<sigma>) ((ptr && ~~ mask 2) + 3), underlying_memory (ksMachineState \<sigma>) ((ptr && ~~ mask 2) + 2), underlying_memory (ksMachineState \<sigma>) ((ptr && ~~ mask 2) + 1), underlying_memory (ksMachineState \<sigma>) (ptr && ~~ mask 2)] ! (3 - unat (x - (ptr && ~~ mask 2))) else a x) = (if x = ptr then b else a x)
 2. \<And>a b x. \<lbrakk>(\<sigma>, s) \<in> rf_sr; pspace_aligned' \<sigma>; pspace_distinct' \<sigma>; pointerInUserData ptr \<sigma>; t_hrs_' (globals s) = (a, b); 4 < addr_card\<rbrakk> \<Longrightarrow> ?P171 a b x proof (prove)
goal (4 subgoals):
 1. \<And>a b x. \<lbrakk>(\<sigma>, s) \<in> rf_sr; pspace_aligned' \<sigma>; pspace_distinct' \<sigma>; pointerInUserData ptr \<sigma>; t_hrs_' (globals s) = (a, b); 4 < addr_card; ?P171 a b x\<rbrakk> \<Longrightarrow> (unat (x - (ptr && ~~ mask 2)) < 4 \<and> 3 - unat (ptr && mask 2) = 3 - unat (x - (ptr && ~~ mask 2))) = (x = ptr)
 2. \<And>a ba x. \<lbrakk>(\<sigma>, s) \<in> rf_sr; pspace_aligned' \<sigma>; pspace_distinct' \<sigma>; pointerInUserData ptr \<sigma>; t_hrs_' (globals s) = (a, ba); 4 < addr_card; ?P171 a ba x; x = ptr\<rbrakk> \<Longrightarrow> b = b
 3. \<And>a b x. \<lbrakk>(\<sigma>, s) \<in> rf_sr; pspace_aligned' \<sigma>; pspace_distinct' \<sigma>; pointerInUserData ptr \<sigma>; t_hrs_' (globals s) = (a, b); 4 < addr_card; ?P171 a b x; x \<noteq> ptr\<rbrakk> \<Longrightarrow> (if unat (x - (ptr && ~~ mask 2)) < 4 then [underlying_memory (ksMachineState \<sigma>) ((ptr && ~~ mask 2) + 3), underlying_memory (ksMachineState \<sigma>) ((ptr && ~~ mask 2) + 2), underlying_memory (ksMachineState \<sigma>) ((ptr && ~~ mask 2) + 1), underlying_memory (ksMachineState \<sigma>) (ptr && ~~ mask 2)] ! (3 - unat (x - (ptr && ~~ mask 2))) else a x) = a x
 4. \<And>a b x. \<lbrakk>(\<sigma>, s) \<in> rf_sr; pspace_aligned' \<sigma>; pspace_distinct' \<sigma>; pointerInUserData ptr \<sigma>; t_hrs_' (globals s) = (a, b); 4 < addr_card\<rbrakk> \<Longrightarrow> ?P171 a b x proof (prove)
goal (3 subgoals):
 1. \<And>a ba x. \<lbrakk>(\<sigma>, s) \<in> rf_sr; pspace_aligned' \<sigma>; pspace_distinct' \<sigma>; pointerInUserData ptr \<sigma>; t_hrs_' (globals s) = (a, ba); 4 < addr_card; (unat (x - (ptr && ~~ mask 2)) < 4 \<and> 3 - unat (ptr && mask 2) = 3 - unat (x - (ptr && ~~ mask 2))) = (x = ptr); x = ptr\<rbrakk> \<Longrightarrow> b = b
 2. \<And>a b x. \<lbrakk>(\<sigma>, s) \<in> rf_sr; pspace_aligned' \<sigma>; pspace_distinct' \<sigma>; pointerInUserData ptr \<sigma>; t_hrs_' (globals s) = (a, b); 4 < addr_card; (unat (x - (ptr && ~~ mask 2)) < 4 \<and> 3 - unat (ptr && mask 2) = 3 - unat (x - (ptr && ~~ mask 2))) = (x = ptr); x \<noteq> ptr\<rbrakk> \<Longrightarrow> (if unat (x - (ptr && ~~ mask 2)) < 4 then [underlying_memory (ksMachineState \<sigma>) ((ptr && ~~ mask 2) + 3), underlying_memory (ksMachineState \<sigma>) ((ptr && ~~ mask 2) + 2), underlying_memory (ksMachineState \<sigma>) ((ptr && ~~ mask 2) + 1), underlying_memory (ksMachineState \<sigma>) (ptr && ~~ mask 2)] ! (3 - unat (x - (ptr && ~~ mask 2))) else a x) = a x
 3. \<And>a b x. \<lbrakk>(\<sigma>, s) \<in> rf_sr; pspace_aligned' \<sigma>; pspace_distinct' \<sigma>; pointerInUserData ptr \<sigma>; t_hrs_' (globals s) = (a, b); 4 < addr_card\<rbrakk> \<Longrightarrow> (unat (x - (ptr && ~~ mask 2)) < 4 \<and> 3 - unat (ptr && mask 2) = 3 - unat (x - (ptr && ~~ mask 2))) = (x = ptr) proof (prove)
goal (2 subgoals):
 1. \<And>a b x. \<lbrakk>(\<sigma>, s) \<in> rf_sr; pspace_aligned' \<sigma>; pspace_distinct' \<sigma>; pointerInUserData ptr \<sigma>; t_hrs_' (globals s) = (a, b); 4 < addr_card; (unat (x - (ptr && ~~ mask 2)) < 4 \<and> 3 - unat (ptr && mask 2) = 3 - unat (x - (ptr && ~~ mask 2))) = (x = ptr); x \<noteq> ptr\<rbrakk> \<Longrightarrow> (if unat (x - (ptr && ~~ mask 2)) < 4 then [underlying_memory (ksMachineState \<sigma>) ((ptr && ~~ mask 2) + 3), underlying_memory (ksMachineState \<sigma>) ((ptr && ~~ mask 2) + 2), underlying_memory (ksMachineState \<sigma>) ((ptr && ~~ mask 2) + 1), underlying_memory (ksMachineState \<sigma>) (ptr && ~~ mask 2)] ! (3 - unat (x - (ptr && ~~ mask 2))) else a x) = a x
 2. \<And>a b x. \<lbrakk>(\<sigma>, s) \<in> rf_sr; pspace_aligned' \<sigma>; pspace_distinct' \<sigma>; pointerInUserData ptr \<sigma>; t_hrs_' (globals s) = (a, b); 4 < addr_card\<rbrakk> \<Longrightarrow> (unat (x - (ptr && ~~ mask 2)) < 4 \<and> 3 - unat (ptr && mask 2) = 3 - unat (x - (ptr && ~~ mask 2))) = (x = ptr) proof (prove)
goal (2 subgoals):
 1. \<And>a b x. \<lbrakk>(\<sigma>, s) \<in> rf_sr; pspace_aligned' \<sigma>; pspace_distinct' \<sigma>; pointerInUserData ptr \<sigma>; t_hrs_' (globals s) = (a, b); 4 < addr_card; x \<noteq> ptr; unat (x - (ptr && ~~ mask 2)) < 4; 3 - unat (ptr && mask 2) \<noteq> 3 - unat (x - (ptr && ~~ mask 2))\<rbrakk> \<Longrightarrow> [underlying_memory (ksMachineState \<sigma>) ((ptr && ~~ mask 2) + 3), underlying_memory (ksMachineState \<sigma>) ((ptr && ~~ mask 2) + 2), underlying_memory (ksMachineState \<sigma>) ((ptr && ~~ mask 2) + 1), underlying_memory (ksMachineState \<sigma>) (ptr && ~~ mask 2)] ! (3 - unat (x - (ptr && ~~ mask 2))) = a x
 2. \<And>a b x. \<lbrakk>(\<sigma>, s) \<in> rf_sr; pspace_aligned' \<sigma>; pspace_distinct' \<sigma>; pointerInUserData ptr \<sigma>; t_hrs_' (globals s) = (a, b); 4 < addr_card\<rbrakk> \<Longrightarrow> (unat (x - (ptr && ~~ mask 2)) < 4 \<and> 3 - unat (ptr && mask 2) = 3 - unat (x - (ptr && ~~ mask 2))) = (x = ptr) proof (prove)
goal (3 subgoals):
 1. \<And>a b x. \<lbrakk>(\<sigma>, s) \<in> rf_sr; pspace_aligned' \<sigma>; pspace_distinct' \<sigma>; pointerInUserData ptr \<sigma>; t_hrs_' (globals s) = (a, b); 4 < addr_card; x \<noteq> ptr; unat (x - (ptr && ~~ mask 2)) < 4; 3 - unat (ptr && mask 2) \<noteq> 3 - unat (x - (ptr && ~~ mask 2))\<rbrakk> \<Longrightarrow> pointerInUserData x \<sigma>
 2. \<And>a b x. \<lbrakk>(\<sigma>, s) \<in> rf_sr; pspace_aligned' \<sigma>; pspace_distinct' \<sigma>; pointerInUserData ptr \<sigma>; t_hrs_' (globals s) = (a, b); 4 < addr_card; x \<noteq> ptr; unat (x - (ptr && ~~ mask 2)) < 4; 3 - unat (ptr && mask 2) \<noteq> 3 - unat (x - (ptr && ~~ mask 2)); fst (t_hrs_' (globals s)) x = underlying_memory (ksMachineState \<sigma>) x\<rbrakk> \<Longrightarrow> [underlying_memory (ksMachineState \<sigma>) ((ptr && ~~ mask 2) + 3), underlying_memory (ksMachineState \<sigma>) ((ptr && ~~ mask 2) + 2), underlying_memory (ksMachineState \<sigma>) ((ptr && ~~ mask 2) + 1), underlying_memory (ksMachineState \<sigma>) (ptr && ~~ mask 2)] ! (3 - unat (x - (ptr && ~~ mask 2))) = a x
 3. \<And>a b x. \<lbrakk>(\<sigma>, s) \<in> rf_sr; pspace_aligned' \<sigma>; pspace_distinct' \<sigma>; pointerInUserData ptr \<sigma>; t_hrs_' (globals s) = (a, b); 4 < addr_card\<rbrakk> \<Longrightarrow> (unat (x - (ptr && ~~ mask 2)) < 4 \<and> 3 - unat (ptr && mask 2) = 3 - unat (x - (ptr && ~~ mask 2))) = (x = ptr) proof (prove)
goal (3 subgoals):
 1. \<And>a b x. \<lbrakk>(\<sigma>, s) \<in> rf_sr; pspace_aligned' \<sigma>; pspace_distinct' \<sigma>; typ_at' UserDataT (ptr && ~~ mask pageBits) \<sigma>; t_hrs_' (globals s) = (a, b); 4 < addr_card; x \<noteq> ptr; unat (x - (ptr && ~~ mask 2)) < 4; 3 - unat (ptr && mask 2) \<noteq> 3 - unat (x - (ptr && ~~ mask 2))\<rbrakk> \<Longrightarrow> typ_at' UserDataT (x && ~~ mask pageBits) \<sigma>
 2. \<And>a b x. \<lbrakk>(\<sigma>, s) \<in> rf_sr; pspace_aligned' \<sigma>; pspace_distinct' \<sigma>; pointerInUserData ptr \<sigma>; t_hrs_' (globals s) = (a, b); 4 < addr_card; x \<noteq> ptr; unat (x - (ptr && ~~ mask 2)) < 4; 3 - unat (ptr && mask 2) \<noteq> 3 - unat (x - (ptr && ~~ mask 2)); fst (t_hrs_' (globals s)) x = underlying_memory (ksMachineState \<sigma>) x\<rbrakk> \<Longrightarrow> [underlying_memory (ksMachineState \<sigma>) ((ptr && ~~ mask 2) + 3), underlying_memory (ksMachineState \<sigma>) ((ptr && ~~ mask 2) + 2), underlying_memory (ksMachineState \<sigma>) ((ptr && ~~ mask 2) + 1), underlying_memory (ksMachineState \<sigma>) (ptr && ~~ mask 2)] ! (3 - unat (x - (ptr && ~~ mask 2))) = a x
 3. \<And>a b x. \<lbrakk>(\<sigma>, s) \<in> rf_sr; pspace_aligned' \<sigma>; pspace_distinct' \<sigma>; pointerInUserData ptr \<sigma>; t_hrs_' (globals s) = (a, b); 4 < addr_card\<rbrakk> \<Longrightarrow> (unat (x - (ptr && ~~ mask 2)) < 4 \<and> 3 - unat (ptr && mask 2) = 3 - unat (x - (ptr && ~~ mask 2))) = (x = ptr) proof (prove)
goal (5 subgoals):
 1. \<And>a b x. \<lbrakk>(\<sigma>, s) \<in> rf_sr; pspace_aligned' \<sigma>; pspace_distinct' \<sigma>; typ_at' UserDataT (ptr && ~~ mask pageBits) \<sigma>; t_hrs_' (globals s) = (a, b); 4 < addr_card; x \<noteq> ptr; unat (x - (ptr && ~~ mask 2)) < 4; 3 - unat (ptr && mask 2) \<noteq> 3 - unat (x - (ptr && ~~ mask 2))\<rbrakk> \<Longrightarrow> is_aligned (ptr && ~~ mask 2) 2
 2. \<And>a b x. \<lbrakk>(\<sigma>, s) \<in> rf_sr; pspace_aligned' \<sigma>; pspace_distinct' \<sigma>; typ_at' UserDataT (ptr && ~~ mask pageBits) \<sigma>; t_hrs_' (globals s) = (a, b); 4 < addr_card; x \<noteq> ptr; unat (x - (ptr && ~~ mask 2)) < 4; 3 - unat (ptr && mask 2) \<noteq> 3 - unat (x - (ptr && ~~ mask 2))\<rbrakk> \<Longrightarrow> x - (ptr && ~~ mask 2) < 2\<^sup>2
 3. \<And>a b x. \<lbrakk>(\<sigma>, s) \<in> rf_sr; pspace_aligned' \<sigma>; pspace_distinct' \<sigma>; typ_at' UserDataT (ptr && ~~ mask pageBits) \<sigma>; t_hrs_' (globals s) = (a, b); 4 < addr_card; x \<noteq> ptr; unat (x - (ptr && ~~ mask 2)) < 4; 3 - unat (ptr && mask 2) \<noteq> 3 - unat (x - (ptr && ~~ mask 2)); (ptr && ~~ mask 2) + (x - (ptr && ~~ mask 2)) && mask 2 = x - (ptr && ~~ mask 2) \<and> (ptr && ~~ mask 2) + (x - (ptr && ~~ mask 2)) && ~~ mask 2 = ptr && ~~ mask 2\<rbrakk> \<Longrightarrow> typ_at' UserDataT (x && ~~ mask pageBits) \<sigma>
 4. \<And>a b x. \<lbrakk>(\<sigma>, s) \<in> rf_sr; pspace_aligned' \<sigma>; pspace_distinct' \<sigma>; pointerInUserData ptr \<sigma>; t_hrs_' (globals s) = (a, b); 4 < addr_card; x \<noteq> ptr; unat (x - (ptr && ~~ mask 2)) < 4; 3 - unat (ptr && mask 2) \<noteq> 3 - unat (x - (ptr && ~~ mask 2)); fst (t_hrs_' (globals s)) x = underlying_memory (ksMachineState \<sigma>) x\<rbrakk> \<Longrightarrow> [underlying_memory (ksMachineState \<sigma>) ((ptr && ~~ mask 2) + 3), underlying_memory (ksMachineState \<sigma>) ((ptr && ~~ mask 2) + 2), underlying_memory (ksMachineState \<sigma>) ((ptr && ~~ mask 2) + 1), underlying_memory (ksMachineState \<sigma>) (ptr && ~~ mask 2)] ! (3 - unat (x - (ptr && ~~ mask 2))) = a x
 5. \<And>a b x. \<lbrakk>(\<sigma>, s) \<in> rf_sr; pspace_aligned' \<sigma>; pspace_distinct' \<sigma>; pointerInUserData ptr \<sigma>; t_hrs_' (globals s) = (a, b); 4 < addr_card\<rbrakk> \<Longrightarrow> (unat (x - (ptr && ~~ mask 2)) < 4 \<and> 3 - unat (ptr && mask 2) = 3 - unat (x - (ptr && ~~ mask 2))) = (x = ptr) proof (prove)
goal (4 subgoals):
 1. \<And>a b x. \<lbrakk>(\<sigma>, s) \<in> rf_sr; pspace_aligned' \<sigma>; pspace_distinct' \<sigma>; typ_at' UserDataT (ptr && ~~ mask pageBits) \<sigma>; t_hrs_' (globals s) = (a, b); 4 < addr_card; x \<noteq> ptr; unat (x - (ptr && ~~ mask 2)) < 4; 3 - unat (ptr && mask 2) \<noteq> 3 - unat (x - (ptr && ~~ mask 2))\<rbrakk> \<Longrightarrow> x - (ptr && ~~ mask 2) < 2\<^sup>2
 2. \<And>a b x. \<lbrakk>(\<sigma>, s) \<in> rf_sr; pspace_aligned' \<sigma>; pspace_distinct' \<sigma>; typ_at' UserDataT (ptr && ~~ mask pageBits) \<sigma>; t_hrs_' (globals s) = (a, b); 4 < addr_card; x \<noteq> ptr; unat (x - (ptr && ~~ mask 2)) < 4; 3 - unat (ptr && mask 2) \<noteq> 3 - unat (x - (ptr && ~~ mask 2)); (ptr && ~~ mask 2) + (x - (ptr && ~~ mask 2)) && mask 2 = x - (ptr && ~~ mask 2) \<and> (ptr && ~~ mask 2) + (x - (ptr && ~~ mask 2)) && ~~ mask 2 = ptr && ~~ mask 2\<rbrakk> \<Longrightarrow> typ_at' UserDataT (x && ~~ mask pageBits) \<sigma>
 3. \<And>a b x. \<lbrakk>(\<sigma>, s) \<in> rf_sr; pspace_aligned' \<sigma>; pspace_distinct' \<sigma>; pointerInUserData ptr \<sigma>; t_hrs_' (globals s) = (a, b); 4 < addr_card; x \<noteq> ptr; unat (x - (ptr && ~~ mask 2)) < 4; 3 - unat (ptr && mask 2) \<noteq> 3 - unat (x - (ptr && ~~ mask 2)); fst (t_hrs_' (globals s)) x = underlying_memory (ksMachineState \<sigma>) x\<rbrakk> \<Longrightarrow> [underlying_memory (ksMachineState \<sigma>) ((ptr && ~~ mask 2) + 3), underlying_memory (ksMachineState \<sigma>) ((ptr && ~~ mask 2) + 2), underlying_memory (ksMachineState \<sigma>) ((ptr && ~~ mask 2) + 1), underlying_memory (ksMachineState \<sigma>) (ptr && ~~ mask 2)] ! (3 - unat (x - (ptr && ~~ mask 2))) = a x
 4. \<And>a b x. \<lbrakk>(\<sigma>, s) \<in> rf_sr; pspace_aligned' \<sigma>; pspace_distinct' \<sigma>; pointerInUserData ptr \<sigma>; t_hrs_' (globals s) = (a, b); 4 < addr_card\<rbrakk> \<Longrightarrow> (unat (x - (ptr && ~~ mask 2)) < 4 \<and> 3 - unat (ptr && mask 2) = 3 - unat (x - (ptr && ~~ mask 2))) = (x = ptr) proof (prove)
goal (3 subgoals):
 1. \<And>a b x. \<lbrakk>(\<sigma>, s) \<in> rf_sr; pspace_aligned' \<sigma>; pspace_distinct' \<sigma>; typ_at' UserDataT (ptr && ~~ mask pageBits) \<sigma>; t_hrs_' (globals s) = (a, b); 4 < addr_card; x \<noteq> ptr; unat (x - (ptr && ~~ mask 2)) < 4; 3 - unat (ptr && mask 2) \<noteq> 3 - unat (x - (ptr && ~~ mask 2)); (ptr && ~~ mask 2) + (x - (ptr && ~~ mask 2)) && mask 2 = x - (ptr && ~~ mask 2) \<and> (ptr && ~~ mask 2) + (x - (ptr && ~~ mask 2)) && ~~ mask 2 = ptr && ~~ mask 2\<rbrakk> \<Longrightarrow> typ_at' UserDataT (x && ~~ mask pageBits) \<sigma>
 2. \<And>a b x. \<lbrakk>(\<sigma>, s) \<in> rf_sr; pspace_aligned' \<sigma>; pspace_distinct' \<sigma>; pointerInUserData ptr \<sigma>; t_hrs_' (globals s) = (a, b); 4 < addr_card; x \<noteq> ptr; unat (x - (ptr && ~~ mask 2)) < 4; 3 - unat (ptr && mask 2) \<noteq> 3 - unat (x - (ptr && ~~ mask 2)); fst (t_hrs_' (globals s)) x = underlying_memory (ksMachineState \<sigma>) x\<rbrakk> \<Longrightarrow> [underlying_memory (ksMachineState \<sigma>) ((ptr && ~~ mask 2) + 3), underlying_memory (ksMachineState \<sigma>) ((ptr && ~~ mask 2) + 2), underlying_memory (ksMachineState \<sigma>) ((ptr && ~~ mask 2) + 1), underlying_memory (ksMachineState \<sigma>) (ptr && ~~ mask 2)] ! (3 - unat (x - (ptr && ~~ mask 2))) = a x
 3. \<And>a b x. \<lbrakk>(\<sigma>, s) \<in> rf_sr; pspace_aligned' \<sigma>; pspace_distinct' \<sigma>; pointerInUserData ptr \<sigma>; t_hrs_' (globals s) = (a, b); 4 < addr_card\<rbrakk> \<Longrightarrow> (unat (x - (ptr && ~~ mask 2)) < 4 \<and> 3 - unat (ptr && mask 2) = 3 - unat (x - (ptr && ~~ mask 2))) = (x = ptr) proof (prove)
goal (3 subgoals):
 1. \<And>a b x. \<lbrakk>(\<sigma>, s) \<in> rf_sr; pspace_aligned' \<sigma>; pspace_distinct' \<sigma>; typ_at' UserDataT (ptr && ~~ mask pageBits) \<sigma>; t_hrs_' (globals s) = (a, b); 4 < addr_card; x \<noteq> ptr; unat (x - (ptr && ~~ mask 2)) < 4; 3 - unat (ptr && mask 2) \<noteq> 3 - unat (x - (ptr && ~~ mask 2)); x && mask 2 = x - (ptr && ~~ mask 2); x && ~~ mask 2 = ptr && ~~ mask 2\<rbrakk> \<Longrightarrow> typ_at' UserDataT (x && ~~ mask pageBits) \<sigma>
 2. \<And>a b x. \<lbrakk>(\<sigma>, s) \<in> rf_sr; pspace_aligned' \<sigma>; pspace_distinct' \<sigma>; pointerInUserData ptr \<sigma>; t_hrs_' (globals s) = (a, b); 4 < addr_card; x \<noteq> ptr; unat (x - (ptr && ~~ mask 2)) < 4; 3 - unat (ptr && mask 2) \<noteq> 3 - unat (x - (ptr && ~~ mask 2)); fst (t_hrs_' (globals s)) x = underlying_memory (ksMachineState \<sigma>) x\<rbrakk> \<Longrightarrow> [underlying_memory (ksMachineState \<sigma>) ((ptr && ~~ mask 2) + 3), underlying_memory (ksMachineState \<sigma>) ((ptr && ~~ mask 2) + 2), underlying_memory (ksMachineState \<sigma>) ((ptr && ~~ mask 2) + 1), underlying_memory (ksMachineState \<sigma>) (ptr && ~~ mask 2)] ! (3 - unat (x - (ptr && ~~ mask 2))) = a x
 3. \<And>a b x. \<lbrakk>(\<sigma>, s) \<in> rf_sr; pspace_aligned' \<sigma>; pspace_distinct' \<sigma>; pointerInUserData ptr \<sigma>; t_hrs_' (globals s) = (a, b); 4 < addr_card\<rbrakk> \<Longrightarrow> (unat (x - (ptr && ~~ mask 2)) < 4 \<and> 3 - unat (ptr && mask 2) = 3 - unat (x - (ptr && ~~ mask 2))) = (x = ptr) proof (prove)
goal (4 subgoals):
 1. \<And>a b x. \<lbrakk>(\<sigma>, s) \<in> rf_sr; pspace_aligned' \<sigma>; pspace_distinct' \<sigma>; typ_at' UserDataT (ptr && ~~ mask pageBits) \<sigma>; t_hrs_' (globals s) = (a, b); 4 < addr_card; x \<noteq> ptr; unat (x - (ptr && ~~ mask 2)) < 4; 3 - unat (ptr && mask 2) \<noteq> 3 - unat (x - (ptr && ~~ mask 2)); x && mask 2 = x - (ptr && ~~ mask 2); x && ~~ mask 2 = ptr && ~~ mask 2\<rbrakk> \<Longrightarrow> 2 \<le> pageBits
 2. \<And>a b x. \<lbrakk>(\<sigma>, s) \<in> rf_sr; pspace_aligned' \<sigma>; pspace_distinct' \<sigma>; typ_at' UserDataT (ptr && ~~ mask pageBits) \<sigma>; t_hrs_' (globals s) = (a, b); 4 < addr_card; x \<noteq> ptr; unat (x - (ptr && ~~ mask 2)) < 4; 3 - unat (ptr && mask 2) \<noteq> 3 - unat (x - (ptr && ~~ mask 2)); x && mask 2 = x - (ptr && ~~ mask 2); x && ~~ mask 2 = ptr && ~~ mask 2; (x && ~~ mask 2) && ~~ mask pageBits = x && ~~ mask pageBits\<rbrakk> \<Longrightarrow> typ_at' UserDataT (x && ~~ mask pageBits) \<sigma>
 3. \<And>a b x. \<lbrakk>(\<sigma>, s) \<in> rf_sr; pspace_aligned' \<sigma>; pspace_distinct' \<sigma>; pointerInUserData ptr \<sigma>; t_hrs_' (globals s) = (a, b); 4 < addr_card; x \<noteq> ptr; unat (x - (ptr && ~~ mask 2)) < 4; 3 - unat (ptr && mask 2) \<noteq> 3 - unat (x - (ptr && ~~ mask 2)); fst (t_hrs_' (globals s)) x = underlying_memory (ksMachineState \<sigma>) x\<rbrakk> \<Longrightarrow> [underlying_memory (ksMachineState \<sigma>) ((ptr && ~~ mask 2) + 3), underlying_memory (ksMachineState \<sigma>) ((ptr && ~~ mask 2) + 2), underlying_memory (ksMachineState \<sigma>) ((ptr && ~~ mask 2) + 1), underlying_memory (ksMachineState \<sigma>) (ptr && ~~ mask 2)] ! (3 - unat (x - (ptr && ~~ mask 2))) = a x
 4. \<And>a b x. \<lbrakk>(\<sigma>, s) \<in> rf_sr; pspace_aligned' \<sigma>; pspace_distinct' \<sigma>; pointerInUserData ptr \<sigma>; t_hrs_' (globals s) = (a, b); 4 < addr_card\<rbrakk> \<Longrightarrow> (unat (x - (ptr && ~~ mask 2)) < 4 \<and> 3 - unat (ptr && mask 2) = 3 - unat (x - (ptr && ~~ mask 2))) = (x = ptr) proof (prove)
goal (3 subgoals):
 1. \<And>a b x. \<lbrakk>(\<sigma>, s) \<in> rf_sr; pspace_aligned' \<sigma>; pspace_distinct' \<sigma>; typ_at' UserDataT (ptr && ~~ mask pageBits) \<sigma>; t_hrs_' (globals s) = (a, b); 4 < addr_card; x \<noteq> ptr; unat (x - (ptr && ~~ mask 2)) < 4; 3 - unat (ptr && mask 2) \<noteq> 3 - unat (x - (ptr && ~~ mask 2)); x && mask 2 = x - (ptr && ~~ mask 2); x && ~~ mask 2 = ptr && ~~ mask 2; (x && ~~ mask 2) && ~~ mask pageBits = x && ~~ mask pageBits\<rbrakk> \<Longrightarrow> typ_at' UserDataT (x && ~~ mask pageBits) \<sigma>
 2. \<And>a b x. \<lbrakk>(\<sigma>, s) \<in> rf_sr; pspace_aligned' \<sigma>; pspace_distinct' \<sigma>; pointerInUserData ptr \<sigma>; t_hrs_' (globals s) = (a, b); 4 < addr_card; x \<noteq> ptr; unat (x - (ptr && ~~ mask 2)) < 4; 3 - unat (ptr && mask 2) \<noteq> 3 - unat (x - (ptr && ~~ mask 2)); fst (t_hrs_' (globals s)) x = underlying_memory (ksMachineState \<sigma>) x\<rbrakk> \<Longrightarrow> [underlying_memory (ksMachineState \<sigma>) ((ptr && ~~ mask 2) + 3), underlying_memory (ksMachineState \<sigma>) ((ptr && ~~ mask 2) + 2), underlying_memory (ksMachineState \<sigma>) ((ptr && ~~ mask 2) + 1), underlying_memory (ksMachineState \<sigma>) (ptr && ~~ mask 2)] ! (3 - unat (x - (ptr && ~~ mask 2))) = a x
 3. \<And>a b x. \<lbrakk>(\<sigma>, s) \<in> rf_sr; pspace_aligned' \<sigma>; pspace_distinct' \<sigma>; pointerInUserData ptr \<sigma>; t_hrs_' (globals s) = (a, b); 4 < addr_card\<rbrakk> \<Longrightarrow> (unat (x - (ptr && ~~ mask 2)) < 4 \<and> 3 - unat (ptr && mask 2) = 3 - unat (x - (ptr && ~~ mask 2))) = (x = ptr) proof (prove)
goal (4 subgoals):
 1. \<And>a b x. \<lbrakk>(\<sigma>, s) \<in> rf_sr; pspace_aligned' \<sigma>; pspace_distinct' \<sigma>; typ_at' UserDataT (ptr && ~~ mask pageBits) \<sigma>; t_hrs_' (globals s) = (a, b); 4 < addr_card; x \<noteq> ptr; unat (x - (ptr && ~~ mask 2)) < 4; 3 - unat (ptr && mask 2) \<noteq> 3 - unat (x - (ptr && ~~ mask 2)); x && mask 2 = x - (ptr && ~~ mask 2); x && ~~ mask 2 = ptr && ~~ mask 2; (x && ~~ mask 2) && ~~ mask pageBits = x && ~~ mask pageBits\<rbrakk> \<Longrightarrow> 2 \<le> pageBits
 2. \<And>a b x. \<lbrakk>(\<sigma>, s) \<in> rf_sr; pspace_aligned' \<sigma>; pspace_distinct' \<sigma>; typ_at' UserDataT (ptr && ~~ mask pageBits) \<sigma>; t_hrs_' (globals s) = (a, b); 4 < addr_card; x \<noteq> ptr; unat (x - (ptr && ~~ mask 2)) < 4; 3 - unat (ptr && mask 2) \<noteq> 3 - unat (x - (ptr && ~~ mask 2)); x && mask 2 = x - (ptr && ~~ mask 2); x && ~~ mask 2 = ptr && ~~ mask 2; (x && ~~ mask 2) && ~~ mask pageBits = x && ~~ mask pageBits; (ptr && ~~ mask 2) && ~~ mask pageBits = ptr && ~~ mask pageBits\<rbrakk> \<Longrightarrow> typ_at' UserDataT (x && ~~ mask pageBits) \<sigma>
 3. \<And>a b x. \<lbrakk>(\<sigma>, s) \<in> rf_sr; pspace_aligned' \<sigma>; pspace_distinct' \<sigma>; pointerInUserData ptr \<sigma>; t_hrs_' (globals s) = (a, b); 4 < addr_card; x \<noteq> ptr; unat (x - (ptr && ~~ mask 2)) < 4; 3 - unat (ptr && mask 2) \<noteq> 3 - unat (x - (ptr && ~~ mask 2)); fst (t_hrs_' (globals s)) x = underlying_memory (ksMachineState \<sigma>) x\<rbrakk> \<Longrightarrow> [underlying_memory (ksMachineState \<sigma>) ((ptr && ~~ mask 2) + 3), underlying_memory (ksMachineState \<sigma>) ((ptr && ~~ mask 2) + 2), underlying_memory (ksMachineState \<sigma>) ((ptr && ~~ mask 2) + 1), underlying_memory (ksMachineState \<sigma>) (ptr && ~~ mask 2)] ! (3 - unat (x - (ptr && ~~ mask 2))) = a x
 4. \<And>a b x. \<lbrakk>(\<sigma>, s) \<in> rf_sr; pspace_aligned' \<sigma>; pspace_distinct' \<sigma>; pointerInUserData ptr \<sigma>; t_hrs_' (globals s) = (a, b); 4 < addr_card\<rbrakk> \<Longrightarrow> (unat (x - (ptr && ~~ mask 2)) < 4 \<and> 3 - unat (ptr && mask 2) = 3 - unat (x - (ptr && ~~ mask 2))) = (x = ptr) proof (prove)
goal (3 subgoals):
 1. \<And>a b x. \<lbrakk>(\<sigma>, s) \<in> rf_sr; pspace_aligned' \<sigma>; pspace_distinct' \<sigma>; typ_at' UserDataT (ptr && ~~ mask pageBits) \<sigma>; t_hrs_' (globals s) = (a, b); 4 < addr_card; x \<noteq> ptr; unat (x - (ptr && ~~ mask 2)) < 4; 3 - unat (ptr && mask 2) \<noteq> 3 - unat (x - (ptr && ~~ mask 2)); x && mask 2 = x - (ptr && ~~ mask 2); x && ~~ mask 2 = ptr && ~~ mask 2; (x && ~~ mask 2) && ~~ mask pageBits = x && ~~ mask pageBits; (ptr && ~~ mask 2) && ~~ mask pageBits = ptr && ~~ mask pageBits\<rbrakk> \<Longrightarrow> typ_at' UserDataT (x && ~~ mask pageBits) \<sigma>
 2. \<And>a b x. \<lbrakk>(\<sigma>, s) \<in> rf_sr; pspace_aligned' \<sigma>; pspace_distinct' \<sigma>; pointerInUserData ptr \<sigma>; t_hrs_' (globals s) = (a, b); 4 < addr_card; x \<noteq> ptr; unat (x - (ptr && ~~ mask 2)) < 4; 3 - unat (ptr && mask 2) \<noteq> 3 - unat (x - (ptr && ~~ mask 2)); fst (t_hrs_' (globals s)) x = underlying_memory (ksMachineState \<sigma>) x\<rbrakk> \<Longrightarrow> [underlying_memory (ksMachineState \<sigma>) ((ptr && ~~ mask 2) + 3), underlying_memory (ksMachineState \<sigma>) ((ptr && ~~ mask 2) + 2), underlying_memory (ksMachineState \<sigma>) ((ptr && ~~ mask 2) + 1), underlying_memory (ksMachineState \<sigma>) (ptr && ~~ mask 2)] ! (3 - unat (x - (ptr && ~~ mask 2))) = a x
 3. \<And>a b x. \<lbrakk>(\<sigma>, s) \<in> rf_sr; pspace_aligned' \<sigma>; pspace_distinct' \<sigma>; pointerInUserData ptr \<sigma>; t_hrs_' (globals s) = (a, b); 4 < addr_card\<rbrakk> \<Longrightarrow> (unat (x - (ptr && ~~ mask 2)) < 4 \<and> 3 - unat (ptr && mask 2) = 3 - unat (x - (ptr && ~~ mask 2))) = (x = ptr) proof (prove)
goal (2 subgoals):
 1. \<And>a b x. \<lbrakk>(\<sigma>, s) \<in> rf_sr; pspace_aligned' \<sigma>; pspace_distinct' \<sigma>; pointerInUserData ptr \<sigma>; t_hrs_' (globals s) = (a, b); 4 < addr_card; x \<noteq> ptr; unat (x - (ptr && ~~ mask 2)) < 4; 3 - unat (ptr && mask 2) \<noteq> 3 - unat (x - (ptr && ~~ mask 2)); fst (t_hrs_' (globals s)) x = underlying_memory (ksMachineState \<sigma>) x\<rbrakk> \<Longrightarrow> [underlying_memory (ksMachineState \<sigma>) ((ptr && ~~ mask 2) + 3), underlying_memory (ksMachineState \<sigma>) ((ptr && ~~ mask 2) + 2), underlying_memory (ksMachineState \<sigma>) ((ptr && ~~ mask 2) + 1), underlying_memory (ksMachineState \<sigma>) (ptr && ~~ mask 2)] ! (3 - unat (x - (ptr && ~~ mask 2))) = a x
 2. \<And>a b x. \<lbrakk>(\<sigma>, s) \<in> rf_sr; pspace_aligned' \<sigma>; pspace_distinct' \<sigma>; pointerInUserData ptr \<sigma>; t_hrs_' (globals s) = (a, b); 4 < addr_card\<rbrakk> \<Longrightarrow> (unat (x - (ptr && ~~ mask 2)) < 4 \<and> 3 - unat (ptr && mask 2) = 3 - unat (x - (ptr && ~~ mask 2))) = (x = ptr) proof (prove)
goal (1 subgoal):
 1. \<And>a b x. \<lbrakk>(\<sigma>, s) \<in> rf_sr; pspace_aligned' \<sigma>; pspace_distinct' \<sigma>; pointerInUserData ptr \<sigma>; t_hrs_' (globals s) = (a, b); 4 < addr_card\<rbrakk> \<Longrightarrow> (unat (x - (ptr && ~~ mask 2)) < 4 \<and> 3 - unat (ptr && mask 2) = 3 - unat (x - (ptr && ~~ mask 2))) = (x = ptr) proof (prove)
goal (2 subgoals):
 1. \<And>a b x. \<lbrakk>(\<sigma>, s) \<in> rf_sr; pspace_aligned' \<sigma>; pspace_distinct' \<sigma>; pointerInUserData ptr \<sigma>; t_hrs_' (globals s) = (a, b); 4 < addr_card; unat (x - (ptr && ~~ mask 2)) < 4 \<and> 3 - unat (ptr && mask 2) = 3 - unat (x - (ptr && ~~ mask 2))\<rbrakk> \<Longrightarrow> x = ptr
 2. \<And>a b x. \<lbrakk>(\<sigma>, s) \<in> rf_sr; pspace_aligned' \<sigma>; pspace_distinct' \<sigma>; pointerInUserData ptr \<sigma>; t_hrs_' (globals s) = (a, b); 4 < addr_card; x = ptr\<rbrakk> \<Longrightarrow> unat (x - (ptr && ~~ mask 2)) < 4 \<and> 3 - unat (ptr && mask 2) = 3 - unat (x - (ptr && ~~ mask 2)) proof (prove)
goal (2 subgoals):
 1. \<And>a b x. \<lbrakk>(\<sigma>, s) \<in> rf_sr; pspace_aligned' \<sigma>; pspace_distinct' \<sigma>; pointerInUserData ptr \<sigma>; t_hrs_' (globals s) = (a, b); 4 < addr_card; unat (x - (ptr && ~~ mask 2)) < 4; 3 - unat (ptr && mask 2) = 3 - unat (x - (ptr && ~~ mask 2))\<rbrakk> \<Longrightarrow> x = ptr
 2. \<And>a b x. \<lbrakk>(\<sigma>, s) \<in> rf_sr; pspace_aligned' \<sigma>; pspace_distinct' \<sigma>; pointerInUserData ptr \<sigma>; t_hrs_' (globals s) = (a, b); 4 < addr_card; x = ptr\<rbrakk> \<Longrightarrow> unat (x - (ptr && ~~ mask 2)) < 4 \<and> 3 - unat (ptr && mask 2) = 3 - unat (x - (ptr && ~~ mask 2)) proof (prove)
goal (2 subgoals):
 1. \<And>a b x. \<lbrakk>(\<sigma>, s) \<in> rf_sr; pspace_aligned' \<sigma>; pspace_distinct' \<sigma>; pointerInUserData ptr \<sigma>; t_hrs_' (globals s) = (a, b); 4 < addr_card; unat (x - (ptr && ~~ mask 2)) < 4; 3 - unat (ptr && mask 2) = 3 - unat (x - (ptr && ~~ mask 2)); unat (ptr && mask 2) < 4\<rbrakk> \<Longrightarrow> x = ptr
 2. \<And>a b x. \<lbrakk>(\<sigma>, s) \<in> rf_sr; pspace_aligned' \<sigma>; pspace_distinct' \<sigma>; pointerInUserData ptr \<sigma>; t_hrs_' (globals s) = (a, b); 4 < addr_card; x = ptr\<rbrakk> \<Longrightarrow> unat (x - (ptr && ~~ mask 2)) < 4 \<and> 3 - unat (ptr && mask 2) = 3 - unat (x - (ptr && ~~ mask 2)) proof (prove)
goal (3 subgoals):
 1. \<And>a b x. \<lbrakk>(\<sigma>, s) \<in> rf_sr; pspace_aligned' \<sigma>; pspace_distinct' \<sigma>; pointerInUserData ptr \<sigma>; t_hrs_' (globals s) = (a, b); 4 < addr_card; unat (x - (ptr && ~~ mask 2)) < 4; 3 - unat (ptr && mask 2) = 3 - unat (x - (ptr && ~~ mask 2)); unat (ptr && mask 2) < 4; unat (x - (ptr && ~~ mask 2)) = unat (ptr && mask 2)\<rbrakk> \<Longrightarrow> x = ptr
 2. \<And>a b x. \<lbrakk>(\<sigma>, s) \<in> rf_sr; pspace_aligned' \<sigma>; pspace_distinct' \<sigma>; pointerInUserData ptr \<sigma>; t_hrs_' (globals s) = (a, b); 4 < addr_card; unat (x - (ptr && ~~ mask 2)) < 4; 3 - unat (ptr && mask 2) = 3 - unat (x - (ptr && ~~ mask 2)); unat (ptr && mask 2) < 4\<rbrakk> \<Longrightarrow> unat (x - (ptr && ~~ mask 2)) = unat (ptr && mask 2)
 3. \<And>a b x. \<lbrakk>(\<sigma>, s) \<in> rf_sr; pspace_aligned' \<sigma>; pspace_distinct' \<sigma>; pointerInUserData ptr \<sigma>; t_hrs_' (globals s) = (a, b); 4 < addr_card; x = ptr\<rbrakk> \<Longrightarrow> unat (x - (ptr && ~~ mask 2)) < 4 \<and> 3 - unat (ptr && mask 2) = 3 - unat (x - (ptr && ~~ mask 2)) proof (prove)
goal (3 subgoals):
 1. \<And>a b x. \<lbrakk>(\<sigma>, s) \<in> rf_sr; pspace_aligned' \<sigma>; pspace_distinct' \<sigma>; pointerInUserData ptr \<sigma>; t_hrs_' (globals s) = (a, b); 4 < addr_card; unat (x - (ptr && ~~ mask 2)) < 4; 3 - unat (ptr && mask 2) = 3 - unat (x - (ptr && ~~ mask 2)); unat (ptr && mask 2) < 4\<rbrakk> \<Longrightarrow> unat (x - (ptr && ~~ mask 2)) = unat (ptr && mask 2)
 2. \<And>a b x. \<lbrakk>(\<sigma>, s) \<in> rf_sr; pspace_aligned' \<sigma>; pspace_distinct' \<sigma>; pointerInUserData ptr \<sigma>; t_hrs_' (globals s) = (a, b); 4 < addr_card; unat (x - (ptr && ~~ mask 2)) < 4; 3 - unat (ptr && mask 2) = 3 - unat (x - (ptr && ~~ mask 2)); unat (ptr && mask 2) < 4; unat (x - (ptr && ~~ mask 2)) = unat (ptr && mask 2)\<rbrakk> \<Longrightarrow> x = ptr
 3. \<And>a b x. \<lbrakk>(\<sigma>, s) \<in> rf_sr; pspace_aligned' \<sigma>; pspace_distinct' \<sigma>; pointerInUserData ptr \<sigma>; t_hrs_' (globals s) = (a, b); 4 < addr_card; x = ptr\<rbrakk> \<Longrightarrow> unat (x - (ptr && ~~ mask 2)) < 4 \<and> 3 - unat (ptr && mask 2) = 3 - unat (x - (ptr && ~~ mask 2)) proof (prove)
goal (2 subgoals):
 1. \<And>a b x. \<lbrakk>(\<sigma>, s) \<in> rf_sr; pspace_aligned' \<sigma>; pspace_distinct' \<sigma>; pointerInUserData ptr \<sigma>; t_hrs_' (globals s) = (a, b); 4 < addr_card; unat (x - (ptr && ~~ mask 2)) < 4; 3 - unat (ptr && mask 2) = 3 - unat (x - (ptr && ~~ mask 2)); unat (ptr && mask 2) < 4; unat (x - (ptr && ~~ mask 2)) = unat (ptr && mask 2)\<rbrakk> \<Longrightarrow> x = ptr
 2. \<And>a b x. \<lbrakk>(\<sigma>, s) \<in> rf_sr; pspace_aligned' \<sigma>; pspace_distinct' \<sigma>; pointerInUserData ptr \<sigma>; t_hrs_' (globals s) = (a, b); 4 < addr_card; x = ptr\<rbrakk> \<Longrightarrow> unat (x - (ptr && ~~ mask 2)) < 4 \<and> 3 - unat (ptr && mask 2) = 3 - unat (x - (ptr && ~~ mask 2)) proof (prove)
goal (1 subgoal):
 1. \<And>a b x. \<lbrakk>(\<sigma>, s) \<in> rf_sr; pspace_aligned' \<sigma>; pspace_distinct' \<sigma>; pointerInUserData ptr \<sigma>; t_hrs_' (globals s) = (a, b); 4 < addr_card; x = ptr\<rbrakk> \<Longrightarrow> unat (x - (ptr && ~~ mask 2)) < 4 \<and> 3 - unat (ptr && mask 2) = 3 - unat (x - (ptr && ~~ mask 2)) proof (prove)
goal:
No subgoals! proof (state)
this:
(ksMachineState_update (underlying_memory_update (\<lambda>m. m(ptr := b))) \<sigma>, globals_update (t_hrs_'_update (hrs_mem_update (\<lambda>m. m(ptr := b)))) s) \<in> rf_sr

goal:
No subgoals!