theory ArchVSpaceEntries_AI

lemma mapM_x_store_pde_updates:
  "\<forall>x \<in> set xs. f x && ~~ mask pd_bits = p \<Longrightarrow>
   \<lbrace>\<lambda>s. (\<not> page_directory_at p s \<longrightarrow> Q s) \<and>
        (\<forall>pd. ko_at (ArchObj (PageDirectory pd)) p s
           \<longrightarrow> Q (s \<lparr> kheap := (kheap s) (p := Some (ArchObj (PageDirectory (\<lambda>y. if y \<in> (\<lambda>x.
         ucast (f x && mask pd_bits >> 2)) ` set xs then pde else pd y)))) \<rparr>))\<rbrace>
     mapM_x (\<lambda>x. store_pde (f x) pde) xs
   \<lbrace>\<lambda>_. Q\<rbrace>" apply (induct xs) apply (simp add: mapM_x_Nil) apply wp apply (clarsimp simp: obj_at_def fun_upd_idem) apply (simp add: mapM_x_Cons) apply (rule hoare_seq_ext, assumption) apply (thin_tac "valid P f Q" for P f Q) apply (simp add: store_pde_def set_pd_def set_object_def) apply (wp get_pd_wp get_object_wp) apply (clarsimp simp: obj_at_def a_type_simps) apply (erule rsubst[where P=Q]) apply (rule abstract_state.fold_congs[OF refl refl]) apply (rule ext, clarsimp) apply (rule ext, clarsimp) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<forall>x\<in>set xs. f x && ~~ mask pd_bits = p \<Longrightarrow> \<lbrace>\<lambda>s. (\<not> typ_at (AArch APageDirectory) p s \<longrightarrow> Q s) \<and> (\<forall>pd. ako_at (PageDirectory pd) p s \<longrightarrow> Q (s\<lparr>kheap := (kheap s)(p \<mapsto> ArchObj (PageDirectory (\<lambda>y. if y \<in> (\<lambda>x. UCAST(32 \<rightarrow> 12) (f x && mask pd_bits >> 2)) ` set xs then pde else pd y)))\<rparr>))\<rbrace> mapM_x (\<lambda>x. store_pde (f x) pde) xs \<lbrace>\<lambda>_. Q\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<forall>x\<in>set []. f x && ~~ mask pd_bits = p \<Longrightarrow> \<lbrace>\<lambda>s. (\<not> typ_at (AArch APageDirectory) p s \<longrightarrow> Q s) \<and> (\<forall>pd. ako_at (PageDirectory pd) p s \<longrightarrow> Q (s\<lparr>kheap := (kheap s)(p \<mapsto> ArchObj (PageDirectory (\<lambda>y. if y \<in> (\<lambda>x. UCAST(32 \<rightarrow> 12) (f x && mask pd_bits >> 2)) ` set [] then pde else pd y)))\<rparr>))\<rbrace> mapM_x (\<lambda>x. store_pde (f x) pde) [] \<lbrace>\<lambda>_. Q\<rbrace>
 2. \<And>a xs. \<lbrakk>\<forall>x\<in>set xs. f x && ~~ mask pd_bits = p \<Longrightarrow> \<lbrace>\<lambda>s. (\<not> typ_at (AArch APageDirectory) p s \<longrightarrow> Q s) \<and> (\<forall>pd. ako_at (PageDirectory pd) p s \<longrightarrow> Q (s\<lparr>kheap := (kheap s)(p \<mapsto> ArchObj (PageDirectory (\<lambda>y. if y \<in> (\<lambda>x. UCAST(32 \<rightarrow> 12) (f x && mask pd_bits >> 2)) ` set xs then pde else pd y)))\<rparr>))\<rbrace> mapM_x (\<lambda>x. store_pde (f x) pde) xs \<lbrace>\<lambda>_. Q\<rbrace>; \<forall>x\<in>set (a # xs). f x && ~~ mask pd_bits = p\<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>s. (\<not> typ_at (AArch APageDirectory) p s \<longrightarrow> Q s) \<and> (\<forall>pd. ako_at (PageDirectory pd) p s \<longrightarrow> Q (s\<lparr>kheap := (kheap s)(p \<mapsto> ArchObj (PageDirectory (\<lambda>y. if y \<in> (\<lambda>x. UCAST(32 \<rightarrow> 12) (f x && mask pd_bits >> 2)) ` set (a # xs) then pde else pd y)))\<rparr>))\<rbrace> mapM_x (\<lambda>x. store_pde (f x) pde) (a # xs) \<lbrace>\<lambda>_. Q\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<lbrace>\<lambda>s. (\<not> typ_at (AArch APageDirectory) p s \<longrightarrow> Q s) \<and> (\<forall>pd. ako_at (PageDirectory pd) p s \<longrightarrow> Q (s\<lparr>kheap := (kheap s)(p \<mapsto> ArchObj (PageDirectory pd))\<rparr>))\<rbrace> return () \<lbrace>\<lambda>_. Q\<rbrace>
 2. \<And>a xs. \<lbrakk>\<forall>x\<in>set xs. f x && ~~ mask pd_bits = p \<Longrightarrow> \<lbrace>\<lambda>s. (\<not> typ_at (AArch APageDirectory) p s \<longrightarrow> Q s) \<and> (\<forall>pd. ako_at (PageDirectory pd) p s \<longrightarrow> Q (s\<lparr>kheap := (kheap s)(p \<mapsto> ArchObj (PageDirectory (\<lambda>y. if y \<in> (\<lambda>x. UCAST(32 \<rightarrow> 12) (f x && mask pd_bits >> 2)) ` set xs then pde else pd y)))\<rparr>))\<rbrace> mapM_x (\<lambda>x. store_pde (f x) pde) xs \<lbrace>\<lambda>_. Q\<rbrace>; \<forall>x\<in>set (a # xs). f x && ~~ mask pd_bits = p\<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>s. (\<not> typ_at (AArch APageDirectory) p s \<longrightarrow> Q s) \<and> (\<forall>pd. ako_at (PageDirectory pd) p s \<longrightarrow> Q (s\<lparr>kheap := (kheap s)(p \<mapsto> ArchObj (PageDirectory (\<lambda>y. if y \<in> (\<lambda>x. UCAST(32 \<rightarrow> 12) (f x && mask pd_bits >> 2)) ` set (a # xs) then pde else pd y)))\<rparr>))\<rbrace> mapM_x (\<lambda>x. store_pde (f x) pde) (a # xs) \<lbrace>\<lambda>_. Q\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<And>s. (\<not> typ_at (AArch APageDirectory) p s \<longrightarrow> Q s) \<and> (\<forall>pd. ako_at (PageDirectory pd) p s \<longrightarrow> Q (s\<lparr>kheap := (kheap s)(p \<mapsto> ArchObj (PageDirectory pd))\<rparr>)) \<Longrightarrow> Q s
 2. \<And>a xs. \<lbrakk>\<forall>x\<in>set xs. f x && ~~ mask pd_bits = p \<Longrightarrow> \<lbrace>\<lambda>s. (\<not> typ_at (AArch APageDirectory) p s \<longrightarrow> Q s) \<and> (\<forall>pd. ako_at (PageDirectory pd) p s \<longrightarrow> Q (s\<lparr>kheap := (kheap s)(p \<mapsto> ArchObj (PageDirectory (\<lambda>y. if y \<in> (\<lambda>x. UCAST(32 \<rightarrow> 12) (f x && mask pd_bits >> 2)) ` set xs then pde else pd y)))\<rparr>))\<rbrace> mapM_x (\<lambda>x. store_pde (f x) pde) xs \<lbrace>\<lambda>_. Q\<rbrace>; \<forall>x\<in>set (a # xs). f x && ~~ mask pd_bits = p\<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>s. (\<not> typ_at (AArch APageDirectory) p s \<longrightarrow> Q s) \<and> (\<forall>pd. ako_at (PageDirectory pd) p s \<longrightarrow> Q (s\<lparr>kheap := (kheap s)(p \<mapsto> ArchObj (PageDirectory (\<lambda>y. if y \<in> (\<lambda>x. UCAST(32 \<rightarrow> 12) (f x && mask pd_bits >> 2)) ` set (a # xs) then pde else pd y)))\<rparr>))\<rbrace> mapM_x (\<lambda>x. store_pde (f x) pde) (a # xs) \<lbrace>\<lambda>_. Q\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>a xs. \<lbrakk>\<forall>x\<in>set xs. f x && ~~ mask pd_bits = p \<Longrightarrow> \<lbrace>\<lambda>s. (\<not> typ_at (AArch APageDirectory) p s \<longrightarrow> Q s) \<and> (\<forall>pd. ako_at (PageDirectory pd) p s \<longrightarrow> Q (s\<lparr>kheap := (kheap s)(p \<mapsto> ArchObj (PageDirectory (\<lambda>y. if y \<in> (\<lambda>x. UCAST(32 \<rightarrow> 12) (f x && mask pd_bits >> 2)) ` set xs then pde else pd y)))\<rparr>))\<rbrace> mapM_x (\<lambda>x. store_pde (f x) pde) xs \<lbrace>\<lambda>_. Q\<rbrace>; \<forall>x\<in>set (a # xs). f x && ~~ mask pd_bits = p\<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>s. (\<not> typ_at (AArch APageDirectory) p s \<longrightarrow> Q s) \<and> (\<forall>pd. ako_at (PageDirectory pd) p s \<longrightarrow> Q (s\<lparr>kheap := (kheap s)(p \<mapsto> ArchObj (PageDirectory (\<lambda>y. if y \<in> (\<lambda>x. UCAST(32 \<rightarrow> 12) (f x && mask pd_bits >> 2)) ` set (a # xs) then pde else pd y)))\<rparr>))\<rbrace> mapM_x (\<lambda>x. store_pde (f x) pde) (a # xs) \<lbrace>\<lambda>_. Q\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>a xs. \<lbrakk>\<lbrace>\<lambda>s. (\<not> typ_at (AArch APageDirectory) p s \<longrightarrow> Q s) \<and> (\<forall>pd. ako_at (PageDirectory pd) p s \<longrightarrow> Q (s\<lparr>kheap := (kheap s)(p \<mapsto> ArchObj (PageDirectory (\<lambda>y. if y \<in> (\<lambda>x. UCAST(32 \<rightarrow> 12) (f x && mask pd_bits >> 2)) ` set xs then pde else pd y)))\<rparr>))\<rbrace> mapM_x (\<lambda>x. store_pde (f x) pde) xs \<lbrace>\<lambda>_. Q\<rbrace>; f a && ~~ mask pd_bits = p \<and> (\<forall>x\<in>set xs. f x && ~~ mask pd_bits = p)\<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>s. (\<not> typ_at (AArch APageDirectory) p s \<longrightarrow> Q s) \<and> (\<forall>pd. ako_at (PageDirectory pd) p s \<longrightarrow> Q (s\<lparr>kheap := (kheap s)(p \<mapsto> ArchObj (PageDirectory (\<lambda>y. if y = UCAST(32 \<rightarrow> 12) (f a && mask pd_bits >> 2) \<or> y \<in> (\<lambda>x. UCAST(32 \<rightarrow> 12) (f x && mask pd_bits >> 2)) ` set xs then pde else pd y)))\<rparr>))\<rbrace> do y <- store_pde (f a) pde;
mapM_x (\<lambda>x. store_pde (f x) pde) xs
od \<lbrace>\<lambda>_. Q\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>a xs. \<lbrakk>\<lbrace>\<lambda>s. (\<not> typ_at (AArch APageDirectory) p s \<longrightarrow> Q s) \<and> (\<forall>pd. ako_at (PageDirectory pd) p s \<longrightarrow> Q (s\<lparr>kheap := (kheap s)(p \<mapsto> ArchObj (PageDirectory (\<lambda>y. if y \<in> (\<lambda>x. UCAST(32 \<rightarrow> 12) (f x && mask pd_bits >> 2)) ` set xs then pde else pd y)))\<rparr>))\<rbrace> mapM_x (\<lambda>x. store_pde (f x) pde) xs \<lbrace>\<lambda>_. Q\<rbrace>; f a && ~~ mask pd_bits = p \<and> (\<forall>x\<in>set xs. f x && ~~ mask pd_bits = p)\<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>s. (\<not> typ_at (AArch APageDirectory) p s \<longrightarrow> Q s) \<and> (\<forall>pd. ako_at (PageDirectory pd) p s \<longrightarrow> Q (s\<lparr>kheap := (kheap s)(p \<mapsto> ArchObj (PageDirectory (\<lambda>y. if y = UCAST(32 \<rightarrow> 12) (f a && mask pd_bits >> 2) \<or> y \<in> (\<lambda>x. UCAST(32 \<rightarrow> 12) (f x && mask pd_bits >> 2)) ` set xs then pde else pd y)))\<rparr>))\<rbrace> store_pde (f a) pde \<lbrace>\<lambda>y s. (\<not> typ_at (AArch APageDirectory) p s \<longrightarrow> Q s) \<and> (\<forall>pd. ako_at (PageDirectory pd) p s \<longrightarrow> Q (s\<lparr>kheap := (kheap s)(p \<mapsto> ArchObj (PageDirectory (\<lambda>y. if y \<in> (\<lambda>x. UCAST(32 \<rightarrow> 12) (f x && mask pd_bits >> 2)) ` set xs then pde else pd y)))\<rparr>))\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>a xs. f a && ~~ mask pd_bits = p \<and> (\<forall>x\<in>set xs. f x && ~~ mask pd_bits = p) \<Longrightarrow> \<lbrace>\<lambda>s. (\<not> typ_at (AArch APageDirectory) p s \<longrightarrow> Q s) \<and> (\<forall>pd. ako_at (PageDirectory pd) p s \<longrightarrow> Q (s\<lparr>kheap := (kheap s)(p \<mapsto> ArchObj (PageDirectory (\<lambda>y. if y = UCAST(32 \<rightarrow> 12) (f a && mask pd_bits >> 2) \<or> y \<in> (\<lambda>x. UCAST(32 \<rightarrow> 12) (f x && mask pd_bits >> 2)) ` set xs then pde else pd y)))\<rparr>))\<rbrace> store_pde (f a) pde \<lbrace>\<lambda>y s. (\<not> typ_at (AArch APageDirectory) p s \<longrightarrow> Q s) \<and> (\<forall>pd. ako_at (PageDirectory pd) p s \<longrightarrow> Q (s\<lparr>kheap := (kheap s)(p \<mapsto> ArchObj (PageDirectory (\<lambda>y. if y \<in> (\<lambda>x. UCAST(32 \<rightarrow> 12) (f x && mask pd_bits >> 2)) ` set xs then pde else pd y)))\<rparr>))\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>a xs. f a && ~~ mask pd_bits = p \<and> (\<forall>x\<in>set xs. f x && ~~ mask pd_bits = p) \<Longrightarrow> \<lbrace>\<lambda>s. (\<not> typ_at (AArch APageDirectory) p s \<longrightarrow> Q s) \<and> (\<forall>pd. ako_at (PageDirectory pd) p s \<longrightarrow> Q (s\<lparr>kheap := (kheap s)(p \<mapsto> ArchObj (PageDirectory (\<lambda>y. if y = UCAST(32 \<rightarrow> 12) (f a && mask pd_bits >> 2) \<or> y \<in> (\<lambda>x. UCAST(32 \<rightarrow> 12) (f x && mask pd_bits >> 2)) ` set xs then pde else pd y)))\<rparr>))\<rbrace> do pd <- get_pd p;
kobj <- get_object p;
y <- assert (a_type kobj = a_type (ArchObj (PageDirectory (pd(UCAST(32 \<rightarrow> 12) (f a && mask pd_bits >> 2) := pde)))));
s <- get;
put (s\<lparr>kheap := (kheap s)(p \<mapsto> ArchObj (PageDirectory (pd(UCAST(32 \<rightarrow> 12) (f a && mask pd_bits >> 2) := pde))))\<rparr>)
od \<lbrace>\<lambda>y s. (\<not> typ_at (AArch APageDirectory) p s \<longrightarrow> Q s) \<and> (\<forall>pd. ako_at (PageDirectory pd) p s \<longrightarrow> Q (s\<lparr>kheap := (kheap s)(p \<mapsto> ArchObj (PageDirectory (\<lambda>y. if y \<in> (\<lambda>x. UCAST(32 \<rightarrow> 12) (f x && mask pd_bits >> 2)) ` set xs then pde else pd y)))\<rparr>))\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>a xs s. \<lbrakk>f a && ~~ mask pd_bits = p \<and> (\<forall>x\<in>set xs. f x && ~~ mask pd_bits = p); (\<not> typ_at (AArch APageDirectory) p s \<longrightarrow> Q s) \<and> (\<forall>pd. ako_at (PageDirectory pd) p s \<longrightarrow> Q (s\<lparr>kheap := (kheap s)(p \<mapsto> ArchObj (PageDirectory (\<lambda>y. if y = UCAST(32 \<rightarrow> 12) (f a && mask pd_bits >> 2) \<or> y \<in> (\<lambda>x. UCAST(32 \<rightarrow> 12) (f x && mask pd_bits >> 2)) ` set xs then pde else pd y)))\<rparr>))\<rbrakk> \<Longrightarrow> \<forall>pd. ako_at (PageDirectory pd) p s \<longrightarrow> (\<forall>ko. ko_at ko p s \<longrightarrow> a_type ko = a_type (ArchObj (PageDirectory (pd(UCAST(32 \<rightarrow> 12) (f a && mask pd_bits >> 2) := pde)))) \<longrightarrow> (\<not> typ_at (AArch APageDirectory) p (s\<lparr>kheap := (kheap s)(p \<mapsto> ArchObj (PageDirectory (pd(UCAST(32 \<rightarrow> 12) (f a && mask pd_bits >> 2) := pde))))\<rparr>) \<longrightarrow> Q (s\<lparr>kheap := (kheap s)(p \<mapsto> ArchObj (PageDirectory (pd(UCAST(32 \<rightarrow> 12) (f a && mask pd_bits >> 2) := pde))))\<rparr>)) \<and> (\<forall>pda. ako_at (PageDirectory pda) p (s\<lparr>kheap := (kheap s)(p \<mapsto> ArchObj (PageDirectory (pd(UCAST(32 \<rightarrow> 12) (f a && mask pd_bits >> 2) := pde))))\<rparr>) \<longrightarrow> Q (s\<lparr>kheap := (kheap s)(p \<mapsto> ArchObj (PageDirectory (pd(UCAST(32 \<rightarrow> 12) (f a && mask pd_bits >> 2) := pde)))), kheap := (kheap (s\<lparr>kheap := (kheap s)(p \<mapsto> ArchObj (PageDirectory (pd(UCAST(32 \<rightarrow> 12) (f a && mask pd_bits >> 2) := pde))))\<rparr>))(p \<mapsto> ArchObj (PageDirectory (\<lambda>y. if y \<in> (\<lambda>x. UCAST(32 \<rightarrow> 12) (f x && mask pd_bits >> 2)) ` set xs then pde else pda y)))\<rparr>))) proof (prove)
goal (1 subgoal):
 1. \<And>a xs s pd. \<lbrakk>\<forall>x\<in>set xs. f x && ~~ mask pd_bits = f a && ~~ mask pd_bits; p = f a && ~~ mask pd_bits; Q (s\<lparr>kheap := (kheap s)(f a && ~~ mask pd_bits \<mapsto> ArchObj (PageDirectory (\<lambda>y. if y = UCAST(32 \<rightarrow> 12) (f a && mask pd_bits >> 2) \<or> y \<in> (\<lambda>x. UCAST(32 \<rightarrow> 12) (f x && mask pd_bits >> 2)) ` set xs then pde else pd y)))\<rparr>); kheap s (f a && ~~ mask pd_bits) = Some (ArchObj (PageDirectory pd))\<rbrakk> \<Longrightarrow> Q (s\<lparr>kheap := (\<lambda>b. if b = f a && ~~ mask pd_bits then Some (ArchObj (PageDirectory (\<lambda>b. if b = UCAST(32 \<rightarrow> 12) (f a && mask pd_bits >> 2) then pde else pd b))) else kheap s b)(f a && ~~ mask pd_bits \<mapsto> ArchObj (PageDirectory (\<lambda>y. if y \<in> (\<lambda>x. UCAST(32 \<rightarrow> 12) (f x && mask pd_bits >> 2)) ` set xs then pde else if y = UCAST(32 \<rightarrow> 12) (f a && mask pd_bits >> 2) then pde else pd y)))\<rparr>) proof (prove)
goal (1 subgoal):
 1. \<And>a xs s pd. \<lbrakk>\<forall>x\<in>set xs. f x && ~~ mask pd_bits = f a && ~~ mask pd_bits; p = f a && ~~ mask pd_bits; kheap s (f a && ~~ mask pd_bits) = Some (ArchObj (PageDirectory pd))\<rbrakk> \<Longrightarrow> s\<lparr>kheap := (kheap s)(f a && ~~ mask pd_bits \<mapsto> ArchObj (PageDirectory (\<lambda>y. if y = UCAST(32 \<rightarrow> 12) (f a && mask pd_bits >> 2) \<or> y \<in> (\<lambda>x. UCAST(32 \<rightarrow> 12) (f x && mask pd_bits >> 2)) ` set xs then pde else pd y)))\<rparr> = s\<lparr>kheap := (\<lambda>b. if b = f a && ~~ mask pd_bits then Some (ArchObj (PageDirectory (\<lambda>b. if b = UCAST(32 \<rightarrow> 12) (f a && mask pd_bits >> 2) then pde else pd b))) else kheap s b)(f a && ~~ mask pd_bits \<mapsto> ArchObj (PageDirectory (\<lambda>y. if y \<in> (\<lambda>x. UCAST(32 \<rightarrow> 12) (f x && mask pd_bits >> 2)) ` set xs then pde else if y = UCAST(32 \<rightarrow> 12) (f a && mask pd_bits >> 2) then pde else pd y)))\<rparr> proof (prove)
goal (1 subgoal):
 1. \<And>a xs s pd v. \<lbrakk>\<forall>x\<in>set xs. f x && ~~ mask pd_bits = f a && ~~ mask pd_bits; p = f a && ~~ mask pd_bits; kheap s (f a && ~~ mask pd_bits) = Some (ArchObj (PageDirectory pd)); kheap s = v\<rbrakk> \<Longrightarrow> (kheap s)(f a && ~~ mask pd_bits \<mapsto> ArchObj (PageDirectory (\<lambda>y. if y = UCAST(32 \<rightarrow> 12) (f a && mask pd_bits >> 2) \<or> y \<in> (\<lambda>x. UCAST(32 \<rightarrow> 12) (f x && mask pd_bits >> 2)) ` set xs then pde else pd y))) = (\<lambda>b. if b = f a && ~~ mask pd_bits then Some (ArchObj (PageDirectory (\<lambda>b. if b = UCAST(32 \<rightarrow> 12) (f a && mask pd_bits >> 2) then pde else pd b))) else kheap s b)(f a && ~~ mask pd_bits \<mapsto> ArchObj (PageDirectory (\<lambda>y. if y \<in> (\<lambda>x. UCAST(32 \<rightarrow> 12) (f x && mask pd_bits >> 2)) ` set xs then pde else if y = UCAST(32 \<rightarrow> 12) (f a && mask pd_bits >> 2) then pde else pd y))) proof (prove)
goal (1 subgoal):
 1. \<And>a xs s pd. \<lbrakk>\<forall>x\<in>set xs. f x && ~~ mask pd_bits = f a && ~~ mask pd_bits; p = f a && ~~ mask pd_bits; kheap s (f a && ~~ mask pd_bits) = Some (ArchObj (PageDirectory pd))\<rbrakk> \<Longrightarrow> (\<lambda>y. if y = UCAST(32 \<rightarrow> 12) (f a && mask pd_bits >> 2) \<or> y \<in> (\<lambda>x. UCAST(32 \<rightarrow> 12) (f x && mask pd_bits >> 2)) ` set xs then pde else pd y) = (\<lambda>y. if y \<in> (\<lambda>x. UCAST(32 \<rightarrow> 12) (f x && mask pd_bits >> 2)) ` set xs then pde else if y = UCAST(32 \<rightarrow> 12) (f a && mask pd_bits >> 2) then pde else pd y) proof (prove)
goal:
No subgoals!