theory Detype_C

lemma heap_to_device_data_update_region:
  assumes foo: "\<And>x y v. \<lbrakk> map_to_user_data_device psp x = Some y;
                           v < 2 ^ pageBits \<rbrakk> \<Longrightarrow> (x + v \<in> S) = (x \<in> S)"
  shows
  "heap_to_device_data psp (\<lambda>x. if x \<in> S then v else f x)
     = (\<lambda>x. if x \<in> S \<inter> dom (map_to_user_data_device psp) then Some (K (word_rcat [v, v, v, v]))
             else heap_to_device_data psp f x)" apply (rule ext) apply (simp add: heap_to_device_data_def Let_def
            split: if_split) apply (rule conjI) apply (clarsimp simp: byte_to_word_heap_def Let_def add.assoc
                 intro!: ext) apply (subst foo, assumption+,
          (rule word_add_offset_less[where n=2, simplified]
                word_add_offset_less[where n=2 and y=0, simplified],
           simp_all, rule ucast_less,
           simp_all add: word_bits_def pageBits_def
                         order_less_le_trans[OF ucast_less])[1])+ apply simp apply clarsimp apply (case_tac "map_to_user_data_device psp x") apply simp apply (clarsimp simp: dom_def byte_to_word_heap_def Let_def add.assoc
                intro!: ext) apply (subst foo, assumption,
         (rule word_add_offset_less[where n=2, simplified]
               word_add_offset_less[where n=2 and y=0, simplified],
          simp_all, rule ucast_less,
          simp_all add: word_bits_def pageBits_def
                        order_less_le_trans[OF ucast_less])[1])+ apply (simp add: field_simps) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. heap_to_device_data psp (\<lambda>x. if x \<in> S then v else f x) = (\<lambda>x. if x \<in> S \<inter> dom (map_to_user_data_device psp) then Some (K (word_rcat [v, v, v, v])) else heap_to_device_data psp f x) proof (prove)
goal (1 subgoal):
 1. \<And>x. heap_to_device_data psp (\<lambda>x. if x \<in> S then v else f x) x = (if x \<in> S \<inter> dom (map_to_user_data_device psp) then Some (K (word_rcat [v, v, v, v])) else heap_to_device_data psp f x) proof (prove)
goal (1 subgoal):
 1. \<And>x. (x \<in> S \<and> x \<in> dom (map_to_user_data_device psp) \<longrightarrow> (\<exists>z. map_to_user_data_device psp x = Some z) \<and> byte_to_word_heap (\<lambda>x. if x \<in> S then v else f x) x = (\<lambda>y. word_rcat [v, v, v, v])) \<and> ((x \<in> S \<longrightarrow> x \<notin> dom (map_to_user_data_device psp)) \<longrightarrow> map_option (\<lambda>_. byte_to_word_heap (\<lambda>x. if x \<in> S then v else f x) x) (map_to_user_data_device psp x) = map_option (\<lambda>_. byte_to_word_heap f x) (map_to_user_data_device psp x)) proof (prove)
goal (2 subgoals):
 1. \<And>x. x \<in> S \<and> x \<in> dom (map_to_user_data_device psp) \<longrightarrow> (\<exists>z. map_to_user_data_device psp x = Some z) \<and> byte_to_word_heap (\<lambda>x. if x \<in> S then v else f x) x = (\<lambda>y. word_rcat [v, v, v, v])
 2. \<And>x. (x \<in> S \<longrightarrow> x \<notin> dom (map_to_user_data_device psp)) \<longrightarrow> map_option (\<lambda>_. byte_to_word_heap (\<lambda>x. if x \<in> S then v else f x) x) (map_to_user_data_device psp x) = map_option (\<lambda>_. byte_to_word_heap f x) (map_to_user_data_device psp x) proof (prove)
goal (2 subgoals):
 1. \<And>x y ya. \<lbrakk>x \<in> S; map_to_user_data_device psp x = Some y\<rbrakk> \<Longrightarrow> (x + UCAST(10 \<rightarrow> 32) ya * 4 \<in> S \<longrightarrow> (x + (UCAST(10 \<rightarrow> 32) ya * 4 + 1) \<in> S \<longrightarrow> (x + (UCAST(10 \<rightarrow> 32) ya * 4 + 2) \<in> S \<longrightarrow> x + (UCAST(10 \<rightarrow> 32) ya * 4 + 3) \<notin> S \<longrightarrow> word_rcat [f (x + (UCAST(10 \<rightarrow> 32) ya * 4 + 3)), v, v, v] = word_rcat [v, v, v, v]) \<and> (x + (UCAST(10 \<rightarrow> 32) ya * 4 + 2) \<notin> S \<longrightarrow> (x + (UCAST(10 \<rightarrow> 32) ya * 4 + 3) \<in> S \<longrightarrow> word_rcat [v, f (x + (UCAST(10 \<rightarrow> 32) ya * 4 + 2)), v, v] = word_rcat [v, v, v, v]) \<and> (x + (UCAST(10 \<rightarrow> 32) ya * 4 + 3) \<notin> S \<longrightarrow> word_rcat [f (x + (UCAST(10 \<rightarrow> 32) ya * 4 + 3)), f (x + (UCAST(10 \<rightarrow> 32) ya * 4 + 2)), v, v] = word_rcat [v, v, v, v]))) \<and> (x + (UCAST(10 \<rightarrow> 32) ya * 4 + 1) \<notin> S \<longrightarrow> (x + (UCAST(10 \<rightarrow> 32) ya * 4 + 2) \<in> S \<longrightarrow> (x + (UCAST(10 \<rightarrow> 32) ya * 4 + 3) \<in> S \<longrightarrow> word_rcat [v, v, f (x + (UCAST(10 \<rightarrow> 32) ya * 4 + 1)), v] = word_rcat [v, v, v, v]) \<and> (x + (UCAST(10 \<rightarrow> 32) ya * 4 + 3) \<notin> S \<longrightarrow> word_rcat [f (x + (UCAST(10 \<rightarrow> 32) ya * 4 + 3)), v, f (x + (UCAST(10 \<rightarrow> 32) ya * 4 + 1)), v] = word_rcat [v, v, v, v])) \<and> (x + (UCAST(10 \<rightarrow> 32) ya * 4 + 2) \<notin> S \<longrightarrow> (x + (UCAST(10 \<rightarrow> 32) ya * 4 + 3) \<in> S \<longrightarrow> word_rcat [v, f (x + (UCAST(10 \<rightarrow> 32) ya * 4 + 2)), f (x + (UCAST(10 \<rightarrow> 32) ya * 4 + 1)), v] = word_rcat [v, v, v, v]) \<and> (x + (UCAST(10 \<rightarrow> 32) ya * 4 + 3) \<notin> S \<longrightarrow> word_rcat [f (x + (UCAST(10 \<rightarrow> 32) ya * 4 + 3)), f (x + (UCAST(10 \<rightarrow> 32) ya * 4 + 2)), f (x + (UCAST(10 \<rightarrow> 32) ya * 4 + 1)), v] = word_rcat [v, v, v, v])))) \<and> (x + UCAST(10 \<rightarrow> 32) ya * 4 \<notin> S \<longrightarrow> (x + (UCAST(10 \<rightarrow> 32) ya * 4 + 1) \<in> S \<longrightarrow> (x + (UCAST(10 \<rightarrow> 32) ya * 4 + 2) \<in> S \<longrightarrow> (x + (UCAST(10 \<rightarrow> 32) ya * 4 + 3) \<in> S \<longrightarrow> word_rcat [v, v, v, f (x + UCAST(10 \<rightarrow> 32) ya * 4)] = word_rcat [v, v, v, v]) \<and> (x + (UCAST(10 \<rightarrow> 32) ya * 4 + 3) \<notin> S \<longrightarrow> word_rcat [f (x + (UCAST(10 \<rightarrow> 32) ya * 4 + 3)), v, v, f (x + UCAST(10 \<rightarrow> 32) ya * 4)] = word_rcat [v, v, v, v])) \<and> (x + (UCAST(10 \<rightarrow> 32) ya * 4 + 2) \<notin> S \<longrightarrow> (x + (UCAST(10 \<rightarrow> 32) ya * 4 + 3) \<in> S \<longrightarrow> word_rcat [v, f (x + (UCAST(10 \<rightarrow> 32) ya * 4 + 2)), v, f (x + UCAST(10 \<rightarrow> 32) ya * 4)] = word_rcat [v, v, v, v]) \<and> (x + (UCAST(10 \<rightarrow> 32) ya * 4 + 3) \<notin> S \<longrightarrow> word_rcat [f (x + (UCAST(10 \<rightarrow> 32) ya * 4 + 3)), f (x + (UCAST(10 \<rightarrow> 32) ya * 4 + 2)), v, f (x + UCAST(10 \<rightarrow> 32) ya * 4)] = word_rcat [v, v, v, v]))) \<and> (x + (UCAST(10 \<rightarrow> 32) ya * 4 + 1) \<notin> S \<longrightarrow> (x + (UCAST(10 \<rightarrow> 32) ya * 4 + 2) \<in> S \<longrightarrow> (x + (UCAST(10 \<rightarrow> 32) ya * 4 + 3) \<in> S \<longrightarrow> word_rcat [v, v, f (x + (UCAST(10 \<rightarrow> 32) ya * 4 + 1)), f (x + UCAST(10 \<rightarrow> 32) ya * 4)] = word_rcat [v, v, v, v]) \<and> (x + (UCAST(10 \<rightarrow> 32) ya * 4 + 3) \<notin> S \<longrightarrow> word_rcat [f (x + (UCAST(10 \<rightarrow> 32) ya * 4 + 3)), v, f (x + (UCAST(10 \<rightarrow> 32) ya * 4 + 1)), f (x + UCAST(10 \<rightarrow> 32) ya * 4)] = word_rcat [v, v, v, v])) \<and> (x + (UCAST(10 \<rightarrow> 32) ya * 4 + 2) \<notin> S \<longrightarrow> (x + (UCAST(10 \<rightarrow> 32) ya * 4 + 3) \<in> S \<longrightarrow> word_rcat [v, f (x + (UCAST(10 \<rightarrow> 32) ya * 4 + 2)), f (x + (UCAST(10 \<rightarrow> 32) ya * 4 + 1)), f (x + UCAST(10 \<rightarrow> 32) ya * 4)] = word_rcat [v, v, v, v]) \<and> (x + (UCAST(10 \<rightarrow> 32) ya * 4 + 3) \<notin> S \<longrightarrow> word_rcat [f (x + (UCAST(10 \<rightarrow> 32) ya * 4 + 3)), f (x + (UCAST(10 \<rightarrow> 32) ya * 4 + 2)), f (x + (UCAST(10 \<rightarrow> 32) ya * 4 + 1)), f (x + UCAST(10 \<rightarrow> 32) ya * 4)] = word_rcat [v, v, v, v]))))
 2. \<And>x. (x \<in> S \<longrightarrow> x \<notin> dom (map_to_user_data_device psp)) \<longrightarrow> map_option (\<lambda>_. byte_to_word_heap (\<lambda>x. if x \<in> S then v else f x) x) (map_to_user_data_device psp x) = map_option (\<lambda>_. byte_to_word_heap f x) (map_to_user_data_device psp x) proof (prove)
goal (2 subgoals):
 1. \<And>x y ya. \<lbrakk>x \<in> S; map_to_user_data_device psp x = Some y\<rbrakk> \<Longrightarrow> (x \<in> S \<longrightarrow> (x \<in> S \<longrightarrow> (x \<in> S \<longrightarrow> x \<notin> S \<longrightarrow> word_rcat [f (x + (UCAST(10 \<rightarrow> 32) ya * 4 + 3)), v, v, v] = word_rcat [v, v, v, v]) \<and> (x \<notin> S \<longrightarrow> (x \<in> S \<longrightarrow> word_rcat [v, f (x + (UCAST(10 \<rightarrow> 32) ya * 4 + 2)), v, v] = word_rcat [v, v, v, v]) \<and> (x \<notin> S \<longrightarrow> word_rcat [f (x + (UCAST(10 \<rightarrow> 32) ya * 4 + 3)), f (x + (UCAST(10 \<rightarrow> 32) ya * 4 + 2)), v, v] = word_rcat [v, v, v, v]))) \<and> (x \<notin> S \<longrightarrow> (x \<in> S \<longrightarrow> (x \<in> S \<longrightarrow> word_rcat [v, v, f (x + (UCAST(10 \<rightarrow> 32) ya * 4 + 1)), v] = word_rcat [v, v, v, v]) \<and> (x \<notin> S \<longrightarrow> word_rcat [f (x + (UCAST(10 \<rightarrow> 32) ya * 4 + 3)), v, f (x + (UCAST(10 \<rightarrow> 32) ya * 4 + 1)), v] = word_rcat [v, v, v, v])) \<and> (x \<notin> S \<longrightarrow> (x \<in> S \<longrightarrow> word_rcat [v, f (x + (UCAST(10 \<rightarrow> 32) ya * 4 + 2)), f (x + (UCAST(10 \<rightarrow> 32) ya * 4 + 1)), v] = word_rcat [v, v, v, v]) \<and> (x \<notin> S \<longrightarrow> word_rcat [f (x + (UCAST(10 \<rightarrow> 32) ya * 4 + 3)), f (x + (UCAST(10 \<rightarrow> 32) ya * 4 + 2)), f (x + (UCAST(10 \<rightarrow> 32) ya * 4 + 1)), v] = word_rcat [v, v, v, v])))) \<and> (x \<notin> S \<longrightarrow> (x \<in> S \<longrightarrow> (x \<in> S \<longrightarrow> (x \<in> S \<longrightarrow> word_rcat [v, v, v, f (x + UCAST(10 \<rightarrow> 32) ya * 4)] = word_rcat [v, v, v, v]) \<and> (x \<notin> S \<longrightarrow> word_rcat [f (x + (UCAST(10 \<rightarrow> 32) ya * 4 + 3)), v, v, f (x + UCAST(10 \<rightarrow> 32) ya * 4)] = word_rcat [v, v, v, v])) \<and> (x \<notin> S \<longrightarrow> (x \<in> S \<longrightarrow> word_rcat [v, f (x + (UCAST(10 \<rightarrow> 32) ya * 4 + 2)), v, f (x + UCAST(10 \<rightarrow> 32) ya * 4)] = word_rcat [v, v, v, v]) \<and> (x \<notin> S \<longrightarrow> word_rcat [f (x + (UCAST(10 \<rightarrow> 32) ya * 4 + 3)), f (x + (UCAST(10 \<rightarrow> 32) ya * 4 + 2)), v, f (x + UCAST(10 \<rightarrow> 32) ya * 4)] = word_rcat [v, v, v, v]))) \<and> (x \<notin> S \<longrightarrow> (x \<in> S \<longrightarrow> (x \<in> S \<longrightarrow> word_rcat [v, v, f (x + (UCAST(10 \<rightarrow> 32) ya * 4 + 1)), f (x + UCAST(10 \<rightarrow> 32) ya * 4)] = word_rcat [v, v, v, v]) \<and> (x \<notin> S \<longrightarrow> word_rcat [f (x + (UCAST(10 \<rightarrow> 32) ya * 4 + 3)), v, f (x + (UCAST(10 \<rightarrow> 32) ya * 4 + 1)), f (x + UCAST(10 \<rightarrow> 32) ya * 4)] = word_rcat [v, v, v, v])) \<and> (x \<notin> S \<longrightarrow> (x \<in> S \<longrightarrow> word_rcat [v, f (x + (UCAST(10 \<rightarrow> 32) ya * 4 + 2)), f (x + (UCAST(10 \<rightarrow> 32) ya * 4 + 1)), f (x + UCAST(10 \<rightarrow> 32) ya * 4)] = word_rcat [v, v, v, v]) \<and> (x \<notin> S \<longrightarrow> word_rcat [f (x + (UCAST(10 \<rightarrow> 32) ya * 4 + 3)), f (x + (UCAST(10 \<rightarrow> 32) ya * 4 + 2)), f (x + (UCAST(10 \<rightarrow> 32) ya * 4 + 1)), f (x + UCAST(10 \<rightarrow> 32) ya * 4)] = word_rcat [v, v, v, v]))))
 2. \<And>x. (x \<in> S \<longrightarrow> x \<notin> dom (map_to_user_data_device psp)) \<longrightarrow> map_option (\<lambda>_. byte_to_word_heap (\<lambda>x. if x \<in> S then v else f x) x) (map_to_user_data_device psp x) = map_option (\<lambda>_. byte_to_word_heap f x) (map_to_user_data_device psp x) proof (prove)
goal (1 subgoal):
 1. \<And>x. (x \<in> S \<longrightarrow> x \<notin> dom (map_to_user_data_device psp)) \<longrightarrow> map_option (\<lambda>_. byte_to_word_heap (\<lambda>x. if x \<in> S then v else f x) x) (map_to_user_data_device psp x) = map_option (\<lambda>_. byte_to_word_heap f x) (map_to_user_data_device psp x) proof (prove)
goal (1 subgoal):
 1. \<And>x. x \<in> S \<longrightarrow> x \<notin> dom (map_to_user_data_device psp) \<Longrightarrow> map_option (\<lambda>_. byte_to_word_heap (\<lambda>x. if x \<in> S then v else f x) x) (map_to_user_data_device psp x) = map_option (\<lambda>_. byte_to_word_heap f x) (map_to_user_data_device psp x) proof (prove)
goal (2 subgoals):
 1. \<And>x. \<lbrakk>x \<in> S \<longrightarrow> x \<notin> dom (map_to_user_data_device psp); map_to_user_data_device psp x = None\<rbrakk> \<Longrightarrow> map_option (\<lambda>_. byte_to_word_heap (\<lambda>x. if x \<in> S then v else f x) x) (map_to_user_data_device psp x) = map_option (\<lambda>_. byte_to_word_heap f x) (map_to_user_data_device psp x)
 2. \<And>x a. \<lbrakk>x \<in> S \<longrightarrow> x \<notin> dom (map_to_user_data_device psp); map_to_user_data_device psp x = Some a\<rbrakk> \<Longrightarrow> map_option (\<lambda>_. byte_to_word_heap (\<lambda>x. if x \<in> S then v else f x) x) (map_to_user_data_device psp x) = map_option (\<lambda>_. byte_to_word_heap f x) (map_to_user_data_device psp x) proof (prove)
goal (1 subgoal):
 1. \<And>x a. \<lbrakk>x \<in> S \<longrightarrow> x \<notin> dom (map_to_user_data_device psp); map_to_user_data_device psp x = Some a\<rbrakk> \<Longrightarrow> map_option (\<lambda>_. byte_to_word_heap (\<lambda>x. if x \<in> S then v else f x) x) (map_to_user_data_device psp x) = map_option (\<lambda>_. byte_to_word_heap f x) (map_to_user_data_device psp x) proof (prove)
goal (1 subgoal):
 1. \<And>x a xa. \<lbrakk>x \<notin> S; map_to_user_data_device psp x = Some a\<rbrakk> \<Longrightarrow> (x + UCAST(10 \<rightarrow> 32) xa * 4 \<in> S \<longrightarrow> (x + (UCAST(10 \<rightarrow> 32) xa * 4 + 1) \<in> S \<longrightarrow> (x + (UCAST(10 \<rightarrow> 32) xa * 4 + 2) \<in> S \<longrightarrow> (x + (UCAST(10 \<rightarrow> 32) xa * 4 + 3) \<in> S \<longrightarrow> word_rcat [v, v, v, v] = word_rcat [f (x + (UCAST(10 \<rightarrow> 32) xa * 4 + 3)), f (x + (UCAST(10 \<rightarrow> 32) xa * 4 + 2)), f (x + (UCAST(10 \<rightarrow> 32) xa * 4 + 1)), f (x + UCAST(10 \<rightarrow> 32) xa * 4)]) \<and> (x + (UCAST(10 \<rightarrow> 32) xa * 4 + 3) \<notin> S \<longrightarrow> word_rcat [f (x + (UCAST(10 \<rightarrow> 32) xa * 4 + 3)), v, v, v] = word_rcat [f (x + (UCAST(10 \<rightarrow> 32) xa * 4 + 3)), f (x + (UCAST(10 \<rightarrow> 32) xa * 4 + 2)), f (x + (UCAST(10 \<rightarrow> 32) xa * 4 + 1)), f (x + UCAST(10 \<rightarrow> 32) xa * 4)])) \<and> (x + (UCAST(10 \<rightarrow> 32) xa * 4 + 2) \<notin> S \<longrightarrow> (x + (UCAST(10 \<rightarrow> 32) xa * 4 + 3) \<in> S \<longrightarrow> word_rcat [v, f (x + (UCAST(10 \<rightarrow> 32) xa * 4 + 2)), v, v] = word_rcat [f (x + (UCAST(10 \<rightarrow> 32) xa * 4 + 3)), f (x + (UCAST(10 \<rightarrow> 32) xa * 4 + 2)), f (x + (UCAST(10 \<rightarrow> 32) xa * 4 + 1)), f (x + UCAST(10 \<rightarrow> 32) xa * 4)]) \<and> (x + (UCAST(10 \<rightarrow> 32) xa * 4 + 3) \<notin> S \<longrightarrow> word_rcat [f (x + (UCAST(10 \<rightarrow> 32) xa * 4 + 3)), f (x + (UCAST(10 \<rightarrow> 32) xa * 4 + 2)), v, v] = word_rcat [f (x + (UCAST(10 \<rightarrow> 32) xa * 4 + 3)), f (x + (UCAST(10 \<rightarrow> 32) xa * 4 + 2)), f (x + (UCAST(10 \<rightarrow> 32) xa * 4 + 1)), f (x + UCAST(10 \<rightarrow> 32) xa * 4)]))) \<and> (x + (UCAST(10 \<rightarrow> 32) xa * 4 + 1) \<notin> S \<longrightarrow> (x + (UCAST(10 \<rightarrow> 32) xa * 4 + 2) \<in> S \<longrightarrow> (x + (UCAST(10 \<rightarrow> 32) xa * 4 + 3) \<in> S \<longrightarrow> word_rcat [v, v, f (x + (UCAST(10 \<rightarrow> 32) xa * 4 + 1)), v] = word_rcat [f (x + (UCAST(10 \<rightarrow> 32) xa * 4 + 3)), f (x + (UCAST(10 \<rightarrow> 32) xa * 4 + 2)), f (x + (UCAST(10 \<rightarrow> 32) xa * 4 + 1)), f (x + UCAST(10 \<rightarrow> 32) xa * 4)]) \<and> (x + (UCAST(10 \<rightarrow> 32) xa * 4 + 3) \<notin> S \<longrightarrow> word_rcat [f (x + (UCAST(10 \<rightarrow> 32) xa * 4 + 3)), v, f (x + (UCAST(10 \<rightarrow> 32) xa * 4 + 1)), v] = word_rcat [f (x + (UCAST(10 \<rightarrow> 32) xa * 4 + 3)), f (x + (UCAST(10 \<rightarrow> 32) xa * 4 + 2)), f (x + (UCAST(10 \<rightarrow> 32) xa * 4 + 1)), f (x + UCAST(10 \<rightarrow> 32) xa * 4)])) \<and> (x + (UCAST(10 \<rightarrow> 32) xa * 4 + 2) \<notin> S \<longrightarrow> (x + (UCAST(10 \<rightarrow> 32) xa * 4 + 3) \<in> S \<longrightarrow> word_rcat [v, f (x + (UCAST(10 \<rightarrow> 32) xa * 4 + 2)), f (x + (UCAST(10 \<rightarrow> 32) xa * 4 + 1)), v] = word_rcat [f (x + (UCAST(10 \<rightarrow> 32) xa * 4 + 3)), f (x + (UCAST(10 \<rightarrow> 32) xa * 4 + 2)), f (x + (UCAST(10 \<rightarrow> 32) xa * 4 + 1)), f (x + UCAST(10 \<rightarrow> 32) xa * 4)]) \<and> (x + (UCAST(10 \<rightarrow> 32) xa * 4 + 3) \<notin> S \<longrightarrow> word_rcat [f (x + (UCAST(10 \<rightarrow> 32) xa * 4 + 3)), f (x + (UCAST(10 \<rightarrow> 32) xa * 4 + 2)), f (x + (UCAST(10 \<rightarrow> 32) xa * 4 + 1)), v] = word_rcat [f (x + (UCAST(10 \<rightarrow> 32) xa * 4 + 3)), f (x + (UCAST(10 \<rightarrow> 32) xa * 4 + 2)), f (x + (UCAST(10 \<rightarrow> 32) xa * 4 + 1)), f (x + UCAST(10 \<rightarrow> 32) xa * 4)])))) \<and> (x + UCAST(10 \<rightarrow> 32) xa * 4 \<notin> S \<longrightarrow> (x + (UCAST(10 \<rightarrow> 32) xa * 4 + 1) \<in> S \<longrightarrow> (x + (UCAST(10 \<rightarrow> 32) xa * 4 + 2) \<in> S \<longrightarrow> (x + (UCAST(10 \<rightarrow> 32) xa * 4 + 3) \<in> S \<longrightarrow> word_rcat [v, v, v, f (x + UCAST(10 \<rightarrow> 32) xa * 4)] = word_rcat [f (x + (UCAST(10 \<rightarrow> 32) xa * 4 + 3)), f (x + (UCAST(10 \<rightarrow> 32) xa * 4 + 2)), f (x + (UCAST(10 \<rightarrow> 32) xa * 4 + 1)), f (x + UCAST(10 \<rightarrow> 32) xa * 4)]) \<and> (x + (UCAST(10 \<rightarrow> 32) xa * 4 + 3) \<notin> S \<longrightarrow> word_rcat [f (x + (UCAST(10 \<rightarrow> 32) xa * 4 + 3)), v, v, f (x + UCAST(10 \<rightarrow> 32) xa * 4)] = word_rcat [f (x + (UCAST(10 \<rightarrow> 32) xa * 4 + 3)), f (x + (UCAST(10 \<rightarrow> 32) xa * 4 + 2)), f (x + (UCAST(10 \<rightarrow> 32) xa * 4 + 1)), f (x + UCAST(10 \<rightarrow> 32) xa * 4)])) \<and> (x + (UCAST(10 \<rightarrow> 32) xa * 4 + 2) \<notin> S \<longrightarrow> (x + (UCAST(10 \<rightarrow> 32) xa * 4 + 3) \<in> S \<longrightarrow> word_rcat [v, f (x + (UCAST(10 \<rightarrow> 32) xa * 4 + 2)), v, f (x + UCAST(10 \<rightarrow> 32) xa * 4)] = word_rcat [f (x + (UCAST(10 \<rightarrow> 32) xa * 4 + 3)), f (x + (UCAST(10 \<rightarrow> 32) xa * 4 + 2)), f (x + (UCAST(10 \<rightarrow> 32) xa * 4 + 1)), f (x + UCAST(10 \<rightarrow> 32) xa * 4)]) \<and> (x + (UCAST(10 \<rightarrow> 32) xa * 4 + 3) \<notin> S \<longrightarrow> word_rcat [f (x + (UCAST(10 \<rightarrow> 32) xa * 4 + 3)), f (x + (UCAST(10 \<rightarrow> 32) xa * 4 + 2)), v, f (x + UCAST(10 \<rightarrow> 32) xa * 4)] = word_rcat [f (x + (UCAST(10 \<rightarrow> 32) xa * 4 + 3)), f (x + (UCAST(10 \<rightarrow> 32) xa * 4 + 2)), f (x + (UCAST(10 \<rightarrow> 32) xa * 4 + 1)), f (x + UCAST(10 \<rightarrow> 32) xa * 4)]))) \<and> (x + (UCAST(10 \<rightarrow> 32) xa * 4 + 1) \<notin> S \<longrightarrow> (x + (UCAST(10 \<rightarrow> 32) xa * 4 + 2) \<in> S \<longrightarrow> (x + (UCAST(10 \<rightarrow> 32) xa * 4 + 3) \<in> S \<longrightarrow> word_rcat [v, v, f (x + (UCAST(10 \<rightarrow> 32) xa * 4 + 1)), f (x + UCAST(10 \<rightarrow> 32) xa * 4)] = word_rcat [f (x + (UCAST(10 \<rightarrow> 32) xa * 4 + 3)), f (x + (UCAST(10 \<rightarrow> 32) xa * 4 + 2)), f (x + (UCAST(10 \<rightarrow> 32) xa * 4 + 1)), f (x + UCAST(10 \<rightarrow> 32) xa * 4)]) \<and> (x + (UCAST(10 \<rightarrow> 32) xa * 4 + 3) \<notin> S \<longrightarrow> word_rcat [f (x + (UCAST(10 \<rightarrow> 32) xa * 4 + 3)), v, f (x + (UCAST(10 \<rightarrow> 32) xa * 4 + 1)), f (x + UCAST(10 \<rightarrow> 32) xa * 4)] = word_rcat [f (x + (UCAST(10 \<rightarrow> 32) xa * 4 + 3)), f (x + (UCAST(10 \<rightarrow> 32) xa * 4 + 2)), f (x + (UCAST(10 \<rightarrow> 32) xa * 4 + 1)), f (x + UCAST(10 \<rightarrow> 32) xa * 4)])) \<and> (x + (UCAST(10 \<rightarrow> 32) xa * 4 + 2) \<notin> S \<longrightarrow> x + (UCAST(10 \<rightarrow> 32) xa * 4 + 3) \<in> S \<longrightarrow> word_rcat [v, f (x + (UCAST(10 \<rightarrow> 32) xa * 4 + 2)), f (x + (UCAST(10 \<rightarrow> 32) xa * 4 + 1)), f (x + UCAST(10 \<rightarrow> 32) xa * 4)] = word_rcat [f (x + (UCAST(10 \<rightarrow> 32) xa * 4 + 3)), f (x + (UCAST(10 \<rightarrow> 32) xa * 4 + 2)), f (x + (UCAST(10 \<rightarrow> 32) xa * 4 + 1)), f (x + UCAST(10 \<rightarrow> 32) xa * 4)]))) proof (prove)
goal (1 subgoal):
 1. \<And>x a xa. \<lbrakk>x \<notin> S; map_to_user_data_device psp x = Some a\<rbrakk> \<Longrightarrow> (x \<in> S \<longrightarrow> (x \<in> S \<longrightarrow> (x \<in> S \<longrightarrow> (x \<in> S \<longrightarrow> word_rcat [v, v, v, v] = word_rcat [f (x + (UCAST(10 \<rightarrow> 32) xa * 4 + 3)), f (x + (UCAST(10 \<rightarrow> 32) xa * 4 + 2)), f (x + (UCAST(10 \<rightarrow> 32) xa * 4 + 1)), f (x + UCAST(10 \<rightarrow> 32) xa * 4)]) \<and> (x \<notin> S \<longrightarrow> word_rcat [f (x + (UCAST(10 \<rightarrow> 32) xa * 4 + 3)), v, v, v] = word_rcat [f (x + (UCAST(10 \<rightarrow> 32) xa * 4 + 3)), f (x + (UCAST(10 \<rightarrow> 32) xa * 4 + 2)), f (x + (UCAST(10 \<rightarrow> 32) xa * 4 + 1)), f (x + UCAST(10 \<rightarrow> 32) xa * 4)])) \<and> (x \<notin> S \<longrightarrow> (x \<in> S \<longrightarrow> word_rcat [v, f (x + (UCAST(10 \<rightarrow> 32) xa * 4 + 2)), v, v] = word_rcat [f (x + (UCAST(10 \<rightarrow> 32) xa * 4 + 3)), f (x + (UCAST(10 \<rightarrow> 32) xa * 4 + 2)), f (x + (UCAST(10 \<rightarrow> 32) xa * 4 + 1)), f (x + UCAST(10 \<rightarrow> 32) xa * 4)]) \<and> (x \<notin> S \<longrightarrow> word_rcat [f (x + (UCAST(10 \<rightarrow> 32) xa * 4 + 3)), f (x + (UCAST(10 \<rightarrow> 32) xa * 4 + 2)), v, v] = word_rcat [f (x + (UCAST(10 \<rightarrow> 32) xa * 4 + 3)), f (x + (UCAST(10 \<rightarrow> 32) xa * 4 + 2)), f (x + (UCAST(10 \<rightarrow> 32) xa * 4 + 1)), f (x + UCAST(10 \<rightarrow> 32) xa * 4)]))) \<and> (x \<notin> S \<longrightarrow> (x \<in> S \<longrightarrow> (x \<in> S \<longrightarrow> word_rcat [v, v, f (x + (UCAST(10 \<rightarrow> 32) xa * 4 + 1)), v] = word_rcat [f (x + (UCAST(10 \<rightarrow> 32) xa * 4 + 3)), f (x + (UCAST(10 \<rightarrow> 32) xa * 4 + 2)), f (x + (UCAST(10 \<rightarrow> 32) xa * 4 + 1)), f (x + UCAST(10 \<rightarrow> 32) xa * 4)]) \<and> (x \<notin> S \<longrightarrow> word_rcat [f (x + (UCAST(10 \<rightarrow> 32) xa * 4 + 3)), v, f (x + (UCAST(10 \<rightarrow> 32) xa * 4 + 1)), v] = word_rcat [f (x + (UCAST(10 \<rightarrow> 32) xa * 4 + 3)), f (x + (UCAST(10 \<rightarrow> 32) xa * 4 + 2)), f (x + (UCAST(10 \<rightarrow> 32) xa * 4 + 1)), f (x + UCAST(10 \<rightarrow> 32) xa * 4)])) \<and> (x \<notin> S \<longrightarrow> (x \<in> S \<longrightarrow> word_rcat [v, f (x + (UCAST(10 \<rightarrow> 32) xa * 4 + 2)), f (x + (UCAST(10 \<rightarrow> 32) xa * 4 + 1)), v] = word_rcat [f (x + (UCAST(10 \<rightarrow> 32) xa * 4 + 3)), f (x + (UCAST(10 \<rightarrow> 32) xa * 4 + 2)), f (x + (UCAST(10 \<rightarrow> 32) xa * 4 + 1)), f (x + UCAST(10 \<rightarrow> 32) xa * 4)]) \<and> (x \<notin> S \<longrightarrow> word_rcat [f (x + (UCAST(10 \<rightarrow> 32) xa * 4 + 3)), f (x + (UCAST(10 \<rightarrow> 32) xa * 4 + 2)), f (x + (UCAST(10 \<rightarrow> 32) xa * 4 + 1)), v] = word_rcat [f (x + (UCAST(10 \<rightarrow> 32) xa * 4 + 3)), f (x + (UCAST(10 \<rightarrow> 32) xa * 4 + 2)), f (x + (UCAST(10 \<rightarrow> 32) xa * 4 + 1)), f (x + UCAST(10 \<rightarrow> 32) xa * 4)])))) \<and> (x \<notin> S \<longrightarrow> (x \<in> S \<longrightarrow> (x \<in> S \<longrightarrow> (x \<in> S \<longrightarrow> word_rcat [v, v, v, f (x + UCAST(10 \<rightarrow> 32) xa * 4)] = word_rcat [f (x + (UCAST(10 \<rightarrow> 32) xa * 4 + 3)), f (x + (UCAST(10 \<rightarrow> 32) xa * 4 + 2)), f (x + (UCAST(10 \<rightarrow> 32) xa * 4 + 1)), f (x + UCAST(10 \<rightarrow> 32) xa * 4)]) \<and> (x \<notin> S \<longrightarrow> word_rcat [f (x + (UCAST(10 \<rightarrow> 32) xa * 4 + 3)), v, v, f (x + UCAST(10 \<rightarrow> 32) xa * 4)] = word_rcat [f (x + (UCAST(10 \<rightarrow> 32) xa * 4 + 3)), f (x + (UCAST(10 \<rightarrow> 32) xa * 4 + 2)), f (x + (UCAST(10 \<rightarrow> 32) xa * 4 + 1)), f (x + UCAST(10 \<rightarrow> 32) xa * 4)])) \<and> (x \<notin> S \<longrightarrow> (x \<in> S \<longrightarrow> word_rcat [v, f (x + (UCAST(10 \<rightarrow> 32) xa * 4 + 2)), v, f (x + UCAST(10 \<rightarrow> 32) xa * 4)] = word_rcat [f (x + (UCAST(10 \<rightarrow> 32) xa * 4 + 3)), f (x + (UCAST(10 \<rightarrow> 32) xa * 4 + 2)), f (x + (UCAST(10 \<rightarrow> 32) xa * 4 + 1)), f (x + UCAST(10 \<rightarrow> 32) xa * 4)]) \<and> (x \<notin> S \<longrightarrow> word_rcat [f (x + (UCAST(10 \<rightarrow> 32) xa * 4 + 3)), f (x + (UCAST(10 \<rightarrow> 32) xa * 4 + 2)), v, f (x + UCAST(10 \<rightarrow> 32) xa * 4)] = word_rcat [f (x + (UCAST(10 \<rightarrow> 32) xa * 4 + 3)), f (x + (UCAST(10 \<rightarrow> 32) xa * 4 + 2)), f (x + (UCAST(10 \<rightarrow> 32) xa * 4 + 1)), f (x + UCAST(10 \<rightarrow> 32) xa * 4)]))) \<and> (x \<notin> S \<longrightarrow> (x \<in> S \<longrightarrow> (x \<in> S \<longrightarrow> word_rcat [v, v, f (x + (UCAST(10 \<rightarrow> 32) xa * 4 + 1)), f (x + UCAST(10 \<rightarrow> 32) xa * 4)] = word_rcat [f (x + (UCAST(10 \<rightarrow> 32) xa * 4 + 3)), f (x + (UCAST(10 \<rightarrow> 32) xa * 4 + 2)), f (x + (UCAST(10 \<rightarrow> 32) xa * 4 + 1)), f (x + UCAST(10 \<rightarrow> 32) xa * 4)]) \<and> (x \<notin> S \<longrightarrow> word_rcat [f (x + (UCAST(10 \<rightarrow> 32) xa * 4 + 3)), v, f (x + (UCAST(10 \<rightarrow> 32) xa * 4 + 1)), f (x + UCAST(10 \<rightarrow> 32) xa * 4)] = word_rcat [f (x + (UCAST(10 \<rightarrow> 32) xa * 4 + 3)), f (x + (UCAST(10 \<rightarrow> 32) xa * 4 + 2)), f (x + (UCAST(10 \<rightarrow> 32) xa * 4 + 1)), f (x + UCAST(10 \<rightarrow> 32) xa * 4)])) \<and> (x \<notin> S \<longrightarrow> x \<in> S \<longrightarrow> word_rcat [v, f (x + (UCAST(10 \<rightarrow> 32) xa * 4 + 2)), f (x + (UCAST(10 \<rightarrow> 32) xa * 4 + 1)), f (x + UCAST(10 \<rightarrow> 32) xa * 4)] = word_rcat [f (x + (UCAST(10 \<rightarrow> 32) xa * 4 + 3)), f (x + (UCAST(10 \<rightarrow> 32) xa * 4 + 2)), f (x + (UCAST(10 \<rightarrow> 32) xa * 4 + 1)), f (x + UCAST(10 \<rightarrow> 32) xa * 4)]))) proof (prove)
goal:
No subgoals!