theory VSpace_R

lemma corres_store_pde_with_invalid_tail:
  "\<forall>slot \<in>set ys. \<not> is_aligned (slot >> 2) (pde_align' ab)
  \<Longrightarrow>corres dc ((\<lambda>s. \<forall>y\<in> set ys. pde_at y s) and pspace_aligned and valid_etcbs)
           (pspace_aligned' and pspace_distinct')
           (mapM (swp store_pde ARM_A.pde.InvalidPDE) ys)
           (mapM (swp storePDE ab) ys)" apply (rule_tac S ="{(x,y). x = y \<and> x \<in> set ys}"
               in corres_mapM[where r = dc and r' = dc]) apply simp apply simp apply clarsimp apply (rule corres_guard_imp) apply (rule storePDE_corres') apply (drule bspec) apply simp apply (simp add:pde_relation_aligned_def) apply auto[1] apply (drule bspec, simp) apply simp apply (wp hoare_vcg_ball_lift | simp)+ apply clarsimp done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<forall>slot\<in>set ys. \<not> is_aligned (slot >> 2) (pde_align' ab) \<Longrightarrow> corres dc ((\<lambda>s. \<forall>y\<in>set ys. pde_at y s) and pspace_aligned and valid_etcbs) (pspace_aligned' and pspace_distinct') (mapM (swp store_pde ARM_A.InvalidPDE) ys) (mapM (swp storePDE ab) ys) proof (prove)
goal (7 subgoals):
 1. \<forall>slot\<in>set ys. \<not> is_aligned (slot >> 2) (pde_align' ab) \<Longrightarrow> dc [] []
 2. \<And>x xs y ysa. \<lbrakk>\<forall>slot\<in>set ys. \<not> is_aligned (slot >> 2) (pde_align' ab); dc xs ysa; dc x y\<rbrakk> \<Longrightarrow> dc (x # xs) (y # ysa)
 3. \<And>x y. \<lbrakk>\<forall>slot\<in>set ys. \<not> is_aligned (slot >> 2) (pde_align' ab); (x, y) \<in> {(x, y). x = y \<and> x \<in> set ys}\<rbrakk> \<Longrightarrow> corres dc ((\<lambda>s. \<forall>y\<in>set ys. pde_at y s) and pspace_aligned and valid_etcbs) (pspace_aligned' and pspace_distinct') (swp store_pde ARM_A.InvalidPDE x) (swp storePDE ab y)
 4. \<And>x y. \<lbrakk>\<forall>slot\<in>set ys. \<not> is_aligned (slot >> 2) (pde_align' ab); (x, y) \<in> {(x, y). x = y \<and> x \<in> set ys}\<rbrakk> \<Longrightarrow> \<lbrace>(\<lambda>s. \<forall>y\<in>set ys. pde_at y s) and pspace_aligned and valid_etcbs\<rbrace> swp store_pde ARM_A.InvalidPDE x \<lbrace>\<lambda>rv. (\<lambda>s. \<forall>y\<in>set ys. pde_at y s) and pspace_aligned and valid_etcbs\<rbrace>
 5. \<And>x y. \<lbrakk>\<forall>slot\<in>set ys. \<not> is_aligned (slot >> 2) (pde_align' ab); (x, y) \<in> {(x, y). x = y \<and> x \<in> set ys}\<rbrakk> \<Longrightarrow> \<lbrace>pspace_aligned' and pspace_distinct'\<rbrace> swp storePDE ab y \<lbrace>\<lambda>rv. pspace_aligned' and pspace_distinct'\<rbrace>
 6. \<forall>slot\<in>set ys. \<not> is_aligned (slot >> 2) (pde_align' ab) \<Longrightarrow> length ys = length ys
 7. \<forall>slot\<in>set ys. \<not> is_aligned (slot >> 2) (pde_align' ab) \<Longrightarrow> set (zip ys ys) \<subseteq> {(x, y). x = y \<and> x \<in> set ys} proof (prove)
goal (6 subgoals):
 1. \<And>x xs y ysa. \<lbrakk>\<forall>slot\<in>set ys. \<not> is_aligned (slot >> 2) (pde_align' ab); dc xs ysa; dc x y\<rbrakk> \<Longrightarrow> dc (x # xs) (y # ysa)
 2. \<And>x y. \<lbrakk>\<forall>slot\<in>set ys. \<not> is_aligned (slot >> 2) (pde_align' ab); (x, y) \<in> {(x, y). x = y \<and> x \<in> set ys}\<rbrakk> \<Longrightarrow> corres dc ((\<lambda>s. \<forall>y\<in>set ys. pde_at y s) and pspace_aligned and valid_etcbs) (pspace_aligned' and pspace_distinct') (swp store_pde ARM_A.InvalidPDE x) (swp storePDE ab y)
 3. \<And>x y. \<lbrakk>\<forall>slot\<in>set ys. \<not> is_aligned (slot >> 2) (pde_align' ab); (x, y) \<in> {(x, y). x = y \<and> x \<in> set ys}\<rbrakk> \<Longrightarrow> \<lbrace>(\<lambda>s. \<forall>y\<in>set ys. pde_at y s) and pspace_aligned and valid_etcbs\<rbrace> swp store_pde ARM_A.InvalidPDE x \<lbrace>\<lambda>rv. (\<lambda>s. \<forall>y\<in>set ys. pde_at y s) and pspace_aligned and valid_etcbs\<rbrace>
 4. \<And>x y. \<lbrakk>\<forall>slot\<in>set ys. \<not> is_aligned (slot >> 2) (pde_align' ab); (x, y) \<in> {(x, y). x = y \<and> x \<in> set ys}\<rbrakk> \<Longrightarrow> \<lbrace>pspace_aligned' and pspace_distinct'\<rbrace> swp storePDE ab y \<lbrace>\<lambda>rv. pspace_aligned' and pspace_distinct'\<rbrace>
 5. \<forall>slot\<in>set ys. \<not> is_aligned (slot >> 2) (pde_align' ab) \<Longrightarrow> length ys = length ys
 6. \<forall>slot\<in>set ys. \<not> is_aligned (slot >> 2) (pde_align' ab) \<Longrightarrow> set (zip ys ys) \<subseteq> {(x, y). x = y \<and> x \<in> set ys} proof (prove)
goal (5 subgoals):
 1. \<And>x y. \<lbrakk>\<forall>slot\<in>set ys. \<not> is_aligned (slot >> 2) (pde_align' ab); (x, y) \<in> {(x, y). x = y \<and> x \<in> set ys}\<rbrakk> \<Longrightarrow> corres dc ((\<lambda>s. \<forall>y\<in>set ys. pde_at y s) and pspace_aligned and valid_etcbs) (pspace_aligned' and pspace_distinct') (swp store_pde ARM_A.InvalidPDE x) (swp storePDE ab y)
 2. \<And>x y. \<lbrakk>\<forall>slot\<in>set ys. \<not> is_aligned (slot >> 2) (pde_align' ab); (x, y) \<in> {(x, y). x = y \<and> x \<in> set ys}\<rbrakk> \<Longrightarrow> \<lbrace>(\<lambda>s. \<forall>y\<in>set ys. pde_at y s) and pspace_aligned and valid_etcbs\<rbrace> swp store_pde ARM_A.InvalidPDE x \<lbrace>\<lambda>rv. (\<lambda>s. \<forall>y\<in>set ys. pde_at y s) and pspace_aligned and valid_etcbs\<rbrace>
 3. \<And>x y. \<lbrakk>\<forall>slot\<in>set ys. \<not> is_aligned (slot >> 2) (pde_align' ab); (x, y) \<in> {(x, y). x = y \<and> x \<in> set ys}\<rbrakk> \<Longrightarrow> \<lbrace>pspace_aligned' and pspace_distinct'\<rbrace> swp storePDE ab y \<lbrace>\<lambda>rv. pspace_aligned' and pspace_distinct'\<rbrace>
 4. \<forall>slot\<in>set ys. \<not> is_aligned (slot >> 2) (pde_align' ab) \<Longrightarrow> length ys = length ys
 5. \<forall>slot\<in>set ys. \<not> is_aligned (slot >> 2) (pde_align' ab) \<Longrightarrow> set (zip ys ys) \<subseteq> {(x, y). x = y \<and> x \<in> set ys} proof (prove)
goal (5 subgoals):
 1. \<And>x. \<lbrakk>\<forall>slot\<in>set ys. \<not> is_aligned (slot >> 2) (case ab of ARM_H.SuperSectionPDE x xa xb xc xd xe \<Rightarrow> 4 | _ \<Rightarrow> 0); x \<in> set ys\<rbrakk> \<Longrightarrow> corres dc ((\<lambda>s. \<forall>y\<in>set ys. pde_at y s) and pspace_aligned and valid_etcbs) (pspace_aligned' and pspace_distinct') (store_pde x ARM_A.InvalidPDE) (storePDE x ab)
 2. \<And>x y. \<lbrakk>\<forall>slot\<in>set ys. \<not> is_aligned (slot >> 2) (pde_align' ab); (x, y) \<in> {(x, y). x = y \<and> x \<in> set ys}\<rbrakk> \<Longrightarrow> \<lbrace>(\<lambda>s. \<forall>y\<in>set ys. pde_at y s) and pspace_aligned and valid_etcbs\<rbrace> swp store_pde ARM_A.InvalidPDE x \<lbrace>\<lambda>rv. (\<lambda>s. \<forall>y\<in>set ys. pde_at y s) and pspace_aligned and valid_etcbs\<rbrace>
 3. \<And>x y. \<lbrakk>\<forall>slot\<in>set ys. \<not> is_aligned (slot >> 2) (pde_align' ab); (x, y) \<in> {(x, y). x = y \<and> x \<in> set ys}\<rbrakk> \<Longrightarrow> \<lbrace>pspace_aligned' and pspace_distinct'\<rbrace> swp storePDE ab y \<lbrace>\<lambda>rv. pspace_aligned' and pspace_distinct'\<rbrace>
 4. \<forall>slot\<in>set ys. \<not> is_aligned (slot >> 2) (pde_align' ab) \<Longrightarrow> length ys = length ys
 5. \<forall>slot\<in>set ys. \<not> is_aligned (slot >> 2) (pde_align' ab) \<Longrightarrow> set (zip ys ys) \<subseteq> {(x, y). x = y \<and> x \<in> set ys} proof (prove)
goal (7 subgoals):
 1. \<And>x. \<lbrakk>\<forall>slot\<in>set ys. \<not> is_aligned (slot >> 2) (case ab of ARM_H.SuperSectionPDE x xa xb xc xd xe \<Rightarrow> 4 | _ \<Rightarrow> 0); x \<in> set ys\<rbrakk> \<Longrightarrow> corres dc (?Q8 x) (?Q'8 x) (store_pde x ARM_A.InvalidPDE) (storePDE x ab)
 2. \<And>x s. \<lbrakk>\<forall>slot\<in>set ys. \<not> is_aligned (slot >> 2) (case ab of ARM_H.SuperSectionPDE x xa xb xc xd xe \<Rightarrow> 4 | _ \<Rightarrow> 0); x \<in> set ys; ((\<lambda>s. \<forall>y\<in>set ys. pde_at y s) and pspace_aligned and valid_etcbs) s\<rbrakk> \<Longrightarrow> ?Q8 x s
 3. \<And>x s. \<lbrakk>\<forall>slot\<in>set ys. \<not> is_aligned (slot >> 2) (case ab of ARM_H.SuperSectionPDE x xa xb xc xd xe \<Rightarrow> 4 | _ \<Rightarrow> 0); x \<in> set ys; (pspace_aligned' and pspace_distinct') s\<rbrakk> \<Longrightarrow> ?Q'8 x s
 4. \<And>x y. \<lbrakk>\<forall>slot\<in>set ys. \<not> is_aligned (slot >> 2) (pde_align' ab); (x, y) \<in> {(x, y). x = y \<and> x \<in> set ys}\<rbrakk> \<Longrightarrow> \<lbrace>(\<lambda>s. \<forall>y\<in>set ys. pde_at y s) and pspace_aligned and valid_etcbs\<rbrace> swp store_pde ARM_A.InvalidPDE x \<lbrace>\<lambda>rv. (\<lambda>s. \<forall>y\<in>set ys. pde_at y s) and pspace_aligned and valid_etcbs\<rbrace>
 5. \<And>x y. \<lbrakk>\<forall>slot\<in>set ys. \<not> is_aligned (slot >> 2) (pde_align' ab); (x, y) \<in> {(x, y). x = y \<and> x \<in> set ys}\<rbrakk> \<Longrightarrow> \<lbrace>pspace_aligned' and pspace_distinct'\<rbrace> swp storePDE ab y \<lbrace>\<lambda>rv. pspace_aligned' and pspace_distinct'\<rbrace>
 6. \<forall>slot\<in>set ys. \<not> is_aligned (slot >> 2) (pde_align' ab) \<Longrightarrow> length ys = length ys
 7. \<forall>slot\<in>set ys. \<not> is_aligned (slot >> 2) (pde_align' ab) \<Longrightarrow> set (zip ys ys) \<subseteq> {(x, y). x = y \<and> x \<in> set ys} proof (prove)
goal (7 subgoals):
 1. \<And>x. \<lbrakk>\<forall>slot\<in>set ys. \<not> is_aligned (slot >> 2) (case ab of ARM_H.SuperSectionPDE x xa xb xc xd xe \<Rightarrow> 4 | _ \<Rightarrow> 0); x \<in> set ys\<rbrakk> \<Longrightarrow> pde_relation_aligned (x >> 2) ARM_A.InvalidPDE ab
 2. \<And>x s. \<lbrakk>\<forall>slot\<in>set ys. \<not> is_aligned (slot >> 2) (case ab of ARM_H.SuperSectionPDE x xa xb xc xd xe \<Rightarrow> 4 | _ \<Rightarrow> 0); x \<in> set ys; ((\<lambda>s. \<forall>y\<in>set ys. pde_at y s) and pspace_aligned and valid_etcbs) s\<rbrakk> \<Longrightarrow> (pde_at x and pspace_aligned and valid_etcbs) s
 3. \<And>x s. \<lbrakk>\<forall>slot\<in>set ys. \<not> is_aligned (slot >> 2) (case ab of ARM_H.SuperSectionPDE x xa xb xc xd xe \<Rightarrow> 4 | _ \<Rightarrow> 0); x \<in> set ys; (pspace_aligned' and pspace_distinct') s\<rbrakk> \<Longrightarrow> (pspace_aligned' and pspace_distinct') s
 4. \<And>x y. \<lbrakk>\<forall>slot\<in>set ys. \<not> is_aligned (slot >> 2) (pde_align' ab); (x, y) \<in> {(x, y). x = y \<and> x \<in> set ys}\<rbrakk> \<Longrightarrow> \<lbrace>(\<lambda>s. \<forall>y\<in>set ys. pde_at y s) and pspace_aligned and valid_etcbs\<rbrace> swp store_pde ARM_A.InvalidPDE x \<lbrace>\<lambda>rv. (\<lambda>s. \<forall>y\<in>set ys. pde_at y s) and pspace_aligned and valid_etcbs\<rbrace>
 5. \<And>x y. \<lbrakk>\<forall>slot\<in>set ys. \<not> is_aligned (slot >> 2) (pde_align' ab); (x, y) \<in> {(x, y). x = y \<and> x \<in> set ys}\<rbrakk> \<Longrightarrow> \<lbrace>pspace_aligned' and pspace_distinct'\<rbrace> swp storePDE ab y \<lbrace>\<lambda>rv. pspace_aligned' and pspace_distinct'\<rbrace>
 6. \<forall>slot\<in>set ys. \<not> is_aligned (slot >> 2) (pde_align' ab) \<Longrightarrow> length ys = length ys
 7. \<forall>slot\<in>set ys. \<not> is_aligned (slot >> 2) (pde_align' ab) \<Longrightarrow> set (zip ys ys) \<subseteq> {(x, y). x = y \<and> x \<in> set ys} proof (prove)
goal (8 subgoals):
 1. \<And>x. x \<in> set ys \<Longrightarrow> ?slot14 x \<in> set ys
 2. \<And>x. \<lbrakk>x \<in> set ys; \<not> is_aligned (?slot14 x >> 2) (case ab of ARM_H.SuperSectionPDE x xa xb xc xd xe \<Rightarrow> 4 | _ \<Rightarrow> 0)\<rbrakk> \<Longrightarrow> pde_relation_aligned (x >> 2) ARM_A.InvalidPDE ab
 3. \<And>x s. \<lbrakk>\<forall>slot\<in>set ys. \<not> is_aligned (slot >> 2) (case ab of ARM_H.SuperSectionPDE x xa xb xc xd xe \<Rightarrow> 4 | _ \<Rightarrow> 0); x \<in> set ys; ((\<lambda>s. \<forall>y\<in>set ys. pde_at y s) and pspace_aligned and valid_etcbs) s\<rbrakk> \<Longrightarrow> (pde_at x and pspace_aligned and valid_etcbs) s
 4. \<And>x s. \<lbrakk>\<forall>slot\<in>set ys. \<not> is_aligned (slot >> 2) (case ab of ARM_H.SuperSectionPDE x xa xb xc xd xe \<Rightarrow> 4 | _ \<Rightarrow> 0); x \<in> set ys; (pspace_aligned' and pspace_distinct') s\<rbrakk> \<Longrightarrow> (pspace_aligned' and pspace_distinct') s
 5. \<And>x y. \<lbrakk>\<forall>slot\<in>set ys. \<not> is_aligned (slot >> 2) (pde_align' ab); (x, y) \<in> {(x, y). x = y \<and> x \<in> set ys}\<rbrakk> \<Longrightarrow> \<lbrace>(\<lambda>s. \<forall>y\<in>set ys. pde_at y s) and pspace_aligned and valid_etcbs\<rbrace> swp store_pde ARM_A.InvalidPDE x \<lbrace>\<lambda>rv. (\<lambda>s. \<forall>y\<in>set ys. pde_at y s) and pspace_aligned and valid_etcbs\<rbrace>
 6. \<And>x y. \<lbrakk>\<forall>slot\<in>set ys. \<not> is_aligned (slot >> 2) (pde_align' ab); (x, y) \<in> {(x, y). x = y \<and> x \<in> set ys}\<rbrakk> \<Longrightarrow> \<lbrace>pspace_aligned' and pspace_distinct'\<rbrace> swp storePDE ab y \<lbrace>\<lambda>rv. pspace_aligned' and pspace_distinct'\<rbrace>
 7. \<forall>slot\<in>set ys. \<not> is_aligned (slot >> 2) (pde_align' ab) \<Longrightarrow> length ys = length ys
 8. \<forall>slot\<in>set ys. \<not> is_aligned (slot >> 2) (pde_align' ab) \<Longrightarrow> set (zip ys ys) \<subseteq> {(x, y). x = y \<and> x \<in> set ys} proof (prove)
goal (7 subgoals):
 1. \<And>x. \<lbrakk>x \<in> set ys; \<not> is_aligned (x >> 2) (case ab of ARM_H.SuperSectionPDE x xa xb xc xd xe \<Rightarrow> 4 | _ \<Rightarrow> 0)\<rbrakk> \<Longrightarrow> pde_relation_aligned (x >> 2) ARM_A.InvalidPDE ab
 2. \<And>x s. \<lbrakk>\<forall>slot\<in>set ys. \<not> is_aligned (slot >> 2) (case ab of ARM_H.SuperSectionPDE x xa xb xc xd xe \<Rightarrow> 4 | _ \<Rightarrow> 0); x \<in> set ys; ((\<lambda>s. \<forall>y\<in>set ys. pde_at y s) and pspace_aligned and valid_etcbs) s\<rbrakk> \<Longrightarrow> (pde_at x and pspace_aligned and valid_etcbs) s
 3. \<And>x s. \<lbrakk>\<forall>slot\<in>set ys. \<not> is_aligned (slot >> 2) (case ab of ARM_H.SuperSectionPDE x xa xb xc xd xe \<Rightarrow> 4 | _ \<Rightarrow> 0); x \<in> set ys; (pspace_aligned' and pspace_distinct') s\<rbrakk> \<Longrightarrow> (pspace_aligned' and pspace_distinct') s
 4. \<And>x y. \<lbrakk>\<forall>slot\<in>set ys. \<not> is_aligned (slot >> 2) (pde_align' ab); (x, y) \<in> {(x, y). x = y \<and> x \<in> set ys}\<rbrakk> \<Longrightarrow> \<lbrace>(\<lambda>s. \<forall>y\<in>set ys. pde_at y s) and pspace_aligned and valid_etcbs\<rbrace> swp store_pde ARM_A.InvalidPDE x \<lbrace>\<lambda>rv. (\<lambda>s. \<forall>y\<in>set ys. pde_at y s) and pspace_aligned and valid_etcbs\<rbrace>
 5. \<And>x y. \<lbrakk>\<forall>slot\<in>set ys. \<not> is_aligned (slot >> 2) (pde_align' ab); (x, y) \<in> {(x, y). x = y \<and> x \<in> set ys}\<rbrakk> \<Longrightarrow> \<lbrace>pspace_aligned' and pspace_distinct'\<rbrace> swp storePDE ab y \<lbrace>\<lambda>rv. pspace_aligned' and pspace_distinct'\<rbrace>
 6. \<forall>slot\<in>set ys. \<not> is_aligned (slot >> 2) (pde_align' ab) \<Longrightarrow> length ys = length ys
 7. \<forall>slot\<in>set ys. \<not> is_aligned (slot >> 2) (pde_align' ab) \<Longrightarrow> set (zip ys ys) \<subseteq> {(x, y). x = y \<and> x \<in> set ys} proof (prove)
goal (6 subgoals):
 1. \<And>x s. \<lbrakk>\<forall>slot\<in>set ys. \<not> is_aligned (slot >> 2) (case ab of ARM_H.SuperSectionPDE x xa xb xc xd xe \<Rightarrow> 4 | _ \<Rightarrow> 0); x \<in> set ys; ((\<lambda>s. \<forall>y\<in>set ys. pde_at y s) and pspace_aligned and valid_etcbs) s\<rbrakk> \<Longrightarrow> (pde_at x and pspace_aligned and valid_etcbs) s
 2. \<And>x s. \<lbrakk>\<forall>slot\<in>set ys. \<not> is_aligned (slot >> 2) (case ab of ARM_H.SuperSectionPDE x xa xb xc xd xe \<Rightarrow> 4 | _ \<Rightarrow> 0); x \<in> set ys; (pspace_aligned' and pspace_distinct') s\<rbrakk> \<Longrightarrow> (pspace_aligned' and pspace_distinct') s
 3. \<And>x y. \<lbrakk>\<forall>slot\<in>set ys. \<not> is_aligned (slot >> 2) (pde_align' ab); (x, y) \<in> {(x, y). x = y \<and> x \<in> set ys}\<rbrakk> \<Longrightarrow> \<lbrace>(\<lambda>s. \<forall>y\<in>set ys. pde_at y s) and pspace_aligned and valid_etcbs\<rbrace> swp store_pde ARM_A.InvalidPDE x \<lbrace>\<lambda>rv. (\<lambda>s. \<forall>y\<in>set ys. pde_at y s) and pspace_aligned and valid_etcbs\<rbrace>
 4. \<And>x y. \<lbrakk>\<forall>slot\<in>set ys. \<not> is_aligned (slot >> 2) (pde_align' ab); (x, y) \<in> {(x, y). x = y \<and> x \<in> set ys}\<rbrakk> \<Longrightarrow> \<lbrace>pspace_aligned' and pspace_distinct'\<rbrace> swp storePDE ab y \<lbrace>\<lambda>rv. pspace_aligned' and pspace_distinct'\<rbrace>
 5. \<forall>slot\<in>set ys. \<not> is_aligned (slot >> 2) (pde_align' ab) \<Longrightarrow> length ys = length ys
 6. \<forall>slot\<in>set ys. \<not> is_aligned (slot >> 2) (pde_align' ab) \<Longrightarrow> set (zip ys ys) \<subseteq> {(x, y). x = y \<and> x \<in> set ys} proof (prove)
goal (5 subgoals):
 1. \<And>x s. \<lbrakk>\<forall>slot\<in>set ys. \<not> is_aligned (slot >> 2) (case ab of ARM_H.SuperSectionPDE x xa xb xc xd xe \<Rightarrow> 4 | _ \<Rightarrow> 0); x \<in> set ys; (pspace_aligned' and pspace_distinct') s\<rbrakk> \<Longrightarrow> (pspace_aligned' and pspace_distinct') s
 2. \<And>x y. \<lbrakk>\<forall>slot\<in>set ys. \<not> is_aligned (slot >> 2) (pde_align' ab); (x, y) \<in> {(x, y). x = y \<and> x \<in> set ys}\<rbrakk> \<Longrightarrow> \<lbrace>(\<lambda>s. \<forall>y\<in>set ys. pde_at y s) and pspace_aligned and valid_etcbs\<rbrace> swp store_pde ARM_A.InvalidPDE x \<lbrace>\<lambda>rv. (\<lambda>s. \<forall>y\<in>set ys. pde_at y s) and pspace_aligned and valid_etcbs\<rbrace>
 3. \<And>x y. \<lbrakk>\<forall>slot\<in>set ys. \<not> is_aligned (slot >> 2) (pde_align' ab); (x, y) \<in> {(x, y). x = y \<and> x \<in> set ys}\<rbrakk> \<Longrightarrow> \<lbrace>pspace_aligned' and pspace_distinct'\<rbrace> swp storePDE ab y \<lbrace>\<lambda>rv. pspace_aligned' and pspace_distinct'\<rbrace>
 4. \<forall>slot\<in>set ys. \<not> is_aligned (slot >> 2) (pde_align' ab) \<Longrightarrow> length ys = length ys
 5. \<forall>slot\<in>set ys. \<not> is_aligned (slot >> 2) (pde_align' ab) \<Longrightarrow> set (zip ys ys) \<subseteq> {(x, y). x = y \<and> x \<in> set ys} proof (prove)
goal (5 subgoals):
 1. \<And>x s. \<lbrakk>x \<in> set ys; (pspace_aligned' and pspace_distinct') s; \<not> is_aligned (x >> 2) (case ab of ARM_H.SuperSectionPDE x xa xb xc xd xe \<Rightarrow> 4 | _ \<Rightarrow> 0)\<rbrakk> \<Longrightarrow> (pspace_aligned' and pspace_distinct') s
 2. \<And>x y. \<lbrakk>\<forall>slot\<in>set ys. \<not> is_aligned (slot >> 2) (pde_align' ab); (x, y) \<in> {(x, y). x = y \<and> x \<in> set ys}\<rbrakk> \<Longrightarrow> \<lbrace>(\<lambda>s. \<forall>y\<in>set ys. pde_at y s) and pspace_aligned and valid_etcbs\<rbrace> swp store_pde ARM_A.InvalidPDE x \<lbrace>\<lambda>rv. (\<lambda>s. \<forall>y\<in>set ys. pde_at y s) and pspace_aligned and valid_etcbs\<rbrace>
 3. \<And>x y. \<lbrakk>\<forall>slot\<in>set ys. \<not> is_aligned (slot >> 2) (pde_align' ab); (x, y) \<in> {(x, y). x = y \<and> x \<in> set ys}\<rbrakk> \<Longrightarrow> \<lbrace>pspace_aligned' and pspace_distinct'\<rbrace> swp storePDE ab y \<lbrace>\<lambda>rv. pspace_aligned' and pspace_distinct'\<rbrace>
 4. \<forall>slot\<in>set ys. \<not> is_aligned (slot >> 2) (pde_align' ab) \<Longrightarrow> length ys = length ys
 5. \<forall>slot\<in>set ys. \<not> is_aligned (slot >> 2) (pde_align' ab) \<Longrightarrow> set (zip ys ys) \<subseteq> {(x, y). x = y \<and> x \<in> set ys} proof (prove)
goal (4 subgoals):
 1. \<And>x y. \<lbrakk>\<forall>slot\<in>set ys. \<not> is_aligned (slot >> 2) (pde_align' ab); (x, y) \<in> {(x, y). x = y \<and> x \<in> set ys}\<rbrakk> \<Longrightarrow> \<lbrace>(\<lambda>s. \<forall>y\<in>set ys. pde_at y s) and pspace_aligned and valid_etcbs\<rbrace> swp store_pde ARM_A.InvalidPDE x \<lbrace>\<lambda>rv. (\<lambda>s. \<forall>y\<in>set ys. pde_at y s) and pspace_aligned and valid_etcbs\<rbrace>
 2. \<And>x y. \<lbrakk>\<forall>slot\<in>set ys. \<not> is_aligned (slot >> 2) (pde_align' ab); (x, y) \<in> {(x, y). x = y \<and> x \<in> set ys}\<rbrakk> \<Longrightarrow> \<lbrace>pspace_aligned' and pspace_distinct'\<rbrace> swp storePDE ab y \<lbrace>\<lambda>rv. pspace_aligned' and pspace_distinct'\<rbrace>
 3. \<forall>slot\<in>set ys. \<not> is_aligned (slot >> 2) (pde_align' ab) \<Longrightarrow> length ys = length ys
 4. \<forall>slot\<in>set ys. \<not> is_aligned (slot >> 2) (pde_align' ab) \<Longrightarrow> set (zip ys ys) \<subseteq> {(x, y). x = y \<and> x \<in> set ys} proof (prove)
goal (1 subgoal):
 1. \<forall>slot\<in>set ys. \<not> is_aligned (slot >> 2) (case ab of ARM_H.SuperSectionPDE x xa xb xc xd xe \<Rightarrow> 4 | _ \<Rightarrow> 0) \<Longrightarrow> set (zip ys ys) \<subseteq> {(x, y). x = y \<and> x \<in> set ys} proof (prove)
goal:
No subgoals!