theory VSpace_R

lemma valid_slots_duplicated_pdeD':
  assumes "valid_slots_duplicated' (Inr (pde, xs)) s"
  shows "(is_aligned (hd xs >> 2) (pde_align' pde))
     \<and> (\<forall>p \<in> set (tl xs). \<not> is_aligned (p >> 2) (pde_align' pde))" proof - have is_aligned_estimate:
    "\<And>x. is_aligned (x::word32) 4 \<Longrightarrow> x \<noteq> 0 \<Longrightarrow> 2 ^ 4 \<le> x" apply (simp add:is_aligned_mask mask_def) apply word_bitwise apply auto done show ?thesis using assms apply - apply (clarsimp simp:valid_slots_duplicated'_def
    split:ARM_H.pde.splits) apply (subgoal_tac "p \<le> p + mask 6") apply (clarsimp simp:upto_enum_step_def not_less) apply (intro conjI impI,simp) apply (simp add:hd_map_simp mask_def is_aligned_shiftr upto_enum_word) apply (clarsimp simp:mask_def upto_enum_word) apply (subst (asm) tl_map_simp upto_enum_word) apply simp apply (clarsimp simp:image_def) apply (cut_tac w = "of_nat x :: word32" in shiftl_t2n[where n = 2,simplified,symmetric]) apply (clarsimp simp:field_simps) apply (drule is_aligned_shiftl[where n = 6 and m = 2,simplified]) apply (subst (asm) shiftr_shiftl1) apply simp apply (simp add: tl_nat_list_simp) apply (subst (asm) is_aligned_neg_mask_eq) apply (erule aligned_add_aligned[OF _ is_aligned_shiftl_self]) apply simp apply (drule(1) is_aligned_addD1) apply (drule_tac w = "(of_nat x::word32) << 2" in
     is_aligned_shiftr[where n = 4 and m = 2,simplified]) apply (clarsimp simp: shiftl_shiftr_id word_of_nat_less)+ apply (drule is_aligned_estimate) apply (rule of_nat_neq_0) apply simp apply simp apply (drule unat_le_helper) apply simp apply (erule is_aligned_no_wrap') apply (simp add:mask_def) done qed

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. is_aligned (hd xs >> 2) (pde_align' pde) \<and> (\<forall>p\<in>set (tl xs). \<not> is_aligned (p >> 2) (pde_align' pde)) proof (state)
goal (1 subgoal):
 1. is_aligned (hd xs >> 2) (pde_align' pde) \<and> (\<forall>p\<in>set (tl xs). \<not> is_aligned (p >> 2) (pde_align' pde)) proof (prove)
goal (1 subgoal):
 1. \<And>x. \<lbrakk>is_aligned x 4; x \<noteq> 0\<rbrakk> \<Longrightarrow> 2 ^ 4 \<le> x proof (prove)
goal (1 subgoal):
 1. \<And>x. \<lbrakk>x && 0xF = 0; x \<noteq> 0\<rbrakk> \<Longrightarrow> 0x10 \<le> x proof (prove)
goal (1 subgoal):
 1. \<And>x. \<lbrakk>\<not> x !! 0 \<and> \<not> x !! 1 \<and> \<not> x !! 2 \<and> \<not> x !! 3; x !! 0 \<or> x !! 1 \<or> x !! 2 \<or> x !! 3 \<or> x !! 4 \<or> x !! 5 \<or> x !! 6 \<or> x !! 7 \<or> x !! 8 \<or> x !! 9 \<or> x !! 10 \<or> x !! 11 \<or> x !! 12 \<or> x !! 13 \<or> x !! 14 \<or> x !! 15 \<or> x !! 16 \<or> x !! 17 \<or> x !! 18 \<or> x !! 19 \<or> x !! 20 \<or> x !! 21 \<or> x !! 22 \<or> x !! 23 \<or> x !! 24 \<or> x !! 25 \<or> x !! 26 \<or> x !! 27 \<or> x !! 28 \<or> x !! 29 \<or> x !! 30 \<or> x !! 31\<rbrakk> \<Longrightarrow> x !! 31 \<or> x !! 30 \<or> x !! 29 \<or> x !! 28 \<or> x !! 27 \<or> x !! 26 \<or> x !! 25 \<or> x !! 24 \<or> x !! 23 \<or> x !! 22 \<or> x !! 21 \<or> x !! 20 \<or> x !! 19 \<or> x !! 18 \<or> x !! 17 \<or> x !! 16 \<or> x !! 15 \<or> x !! 14 \<or> x !! 13 \<or> x !! 12 \<or> x !! 11 \<or> x !! 10 \<or> x !! 9 \<or> x !! 8 \<or> x !! 7 \<or> x !! 6 \<or> x !! 5 \<or> x !! 4 proof (prove)
goal:
No subgoals! proof (state)
this:
\<lbrakk>is_aligned ?x 4; ?x \<noteq> 0\<rbrakk> \<Longrightarrow> 2 ^ 4 \<le> ?x

goal (1 subgoal):
 1. is_aligned (hd xs >> 2) (pde_align' pde) \<and> (\<forall>p\<in>set (tl xs). \<not> is_aligned (p >> 2) (pde_align' pde)) proof (prove)
goal (1 subgoal):
 1. is_aligned (hd xs >> 2) (pde_align' pde) \<and> (\<forall>p\<in>set (tl xs). \<not> is_aligned (p >> 2) (pde_align' pde)) proof (prove)
using this:
valid_slots_duplicated' (Inr (pde, xs)) s

goal (1 subgoal):
 1. is_aligned (hd xs >> 2) (pde_align' pde) \<and> (\<forall>p\<in>set (tl xs). \<not> is_aligned (p >> 2) (pde_align' pde)) proof (prove)
goal (1 subgoal):
 1. valid_slots_duplicated' (Inr (pde, xs)) s \<Longrightarrow> is_aligned (hd xs >> 2) (pde_align' pde) \<and> (\<forall>p\<in>set (tl xs). \<not> is_aligned (p >> 2) (pde_align' pde)) proof (prove)
goal (1 subgoal):
 1. \<And>x41 x42 x43 x44 x45 x46 p. \<lbrakk>pde = ARM_H.SuperSectionPDE x41 x42 x43 x44 x45 x46; xs = [p , p + 4 .e. p + mask 6]; is_aligned p 6; page_directory_at' (p && ~~ mask pdBits) s\<rbrakk> \<Longrightarrow> is_aligned (hd [p , p + 4 .e. p + mask 6] >> 2) 4 \<and> (\<forall>p\<in>set (tl [p , p + 4 .e. p + mask 6]). \<not> is_aligned (p >> 2) 4) proof (prove)
goal (2 subgoals):
 1. \<And>x41 x42 x43 x44 x45 x46 p. \<lbrakk>pde = ARM_H.SuperSectionPDE x41 x42 x43 x44 x45 x46; xs = [p , p + 4 .e. p + mask 6]; is_aligned p 6; page_directory_at' (p && ~~ mask pdBits) s; p \<le> p + mask 6\<rbrakk> \<Longrightarrow> is_aligned (hd [p , p + 4 .e. p + mask 6] >> 2) 4 \<and> (\<forall>p\<in>set (tl [p , p + 4 .e. p + mask 6]). \<not> is_aligned (p >> 2) 4)
 2. \<And>x41 x42 x43 x44 x45 x46 p. \<lbrakk>pde = ARM_H.SuperSectionPDE x41 x42 x43 x44 x45 x46; xs = [p , p + 4 .e. p + mask 6]; is_aligned p 6; page_directory_at' (p && ~~ mask pdBits) s\<rbrakk> \<Longrightarrow> p \<le> p + mask 6 proof (prove)
goal (2 subgoals):
 1. \<And>x41 x42 x43 x44 x45 x46 p. \<lbrakk>pde = ARM_H.SuperSectionPDE x41 x42 x43 x44 x45 x46; xs = (if p + mask 6 < p then [] else map (\<lambda>x. p + x * (p + 4 - p)) [0 .e. (p + mask 6 - p) div (p + 4 - p)]); is_aligned p 6; page_directory_at' (p && ~~ mask pdBits) s; p \<le> p + mask 6\<rbrakk> \<Longrightarrow> (p + mask 6 < p \<longrightarrow> is_aligned (hd [] >> 2) 4) \<and> is_aligned (hd (map (\<lambda>x. p + x * 4) [0 .e. mask 6 div 4]) >> 2) 4 \<and> (\<forall>p\<in>set (tl (map (\<lambda>x. p + x * 4) [0 .e. mask 6 div 4])). \<not> is_aligned (p >> 2) 4)
 2. \<And>x41 x42 x43 x44 x45 x46 p. \<lbrakk>pde = ARM_H.SuperSectionPDE x41 x42 x43 x44 x45 x46; xs = [p , p + 4 .e. p + mask 6]; is_aligned p 6; page_directory_at' (p && ~~ mask pdBits) s\<rbrakk> \<Longrightarrow> p \<le> p + mask 6 proof (prove)
goal (3 subgoals):
 1. \<And>x41 x42 x43 x44 x45 x46 p. \<lbrakk>pde = ARM_H.SuperSectionPDE x41 x42 x43 x44 x45 x46; xs = (if p + mask 6 < p then [] else map (\<lambda>x. p + x * (p + 4 - p)) [0 .e. (p + mask 6 - p) div (p + 4 - p)]); is_aligned p 6; page_directory_at' (p && ~~ mask pdBits) s; p \<le> p + mask 6\<rbrakk> \<Longrightarrow> is_aligned (hd (map (\<lambda>x. p + x * 4) [0 .e. mask 6 div 4]) >> 2) 4
 2. \<And>x41 x42 x43 x44 x45 x46 p. \<lbrakk>pde = ARM_H.SuperSectionPDE x41 x42 x43 x44 x45 x46; xs = (if p + mask 6 < p then [] else map (\<lambda>x. p + x * (p + 4 - p)) [0 .e. (p + mask 6 - p) div (p + 4 - p)]); is_aligned p 6; page_directory_at' (p && ~~ mask pdBits) s; p \<le> p + mask 6\<rbrakk> \<Longrightarrow> \<forall>p\<in>set (tl (map (\<lambda>x. p + x * 4) [0 .e. mask 6 div 4])). \<not> is_aligned (p >> 2) 4
 3. \<And>x41 x42 x43 x44 x45 x46 p. \<lbrakk>pde = ARM_H.SuperSectionPDE x41 x42 x43 x44 x45 x46; xs = [p , p + 4 .e. p + mask 6]; is_aligned p 6; page_directory_at' (p && ~~ mask pdBits) s\<rbrakk> \<Longrightarrow> p \<le> p + mask 6 proof (prove)
goal (2 subgoals):
 1. \<And>x41 x42 x43 x44 x45 x46 p. \<lbrakk>pde = ARM_H.SuperSectionPDE x41 x42 x43 x44 x45 x46; xs = (if p + mask 6 < p then [] else map (\<lambda>x. p + x * (p + 4 - p)) [0 .e. (p + mask 6 - p) div (p + 4 - p)]); is_aligned p 6; page_directory_at' (p && ~~ mask pdBits) s; p \<le> p + mask 6\<rbrakk> \<Longrightarrow> \<forall>p\<in>set (tl (map (\<lambda>x. p + x * 4) [0 .e. mask 6 div 4])). \<not> is_aligned (p >> 2) 4
 2. \<And>x41 x42 x43 x44 x45 x46 p. \<lbrakk>pde = ARM_H.SuperSectionPDE x41 x42 x43 x44 x45 x46; xs = [p , p + 4 .e. p + mask 6]; is_aligned p 6; page_directory_at' (p && ~~ mask pdBits) s\<rbrakk> \<Longrightarrow> p \<le> p + mask 6 proof (prove)
goal (2 subgoals):
 1. \<And>x41 x42 x43 x44 x45 x46 p pa. \<lbrakk>pde = ARM_H.SuperSectionPDE x41 x42 x43 x44 x45 x46; xs = (if p + 0x3F < p then [] else map (\<lambda>x. p + x * (p + 4 - p)) [0 .e. (p + mask 6 - p) div (p + 4 - p)]); is_aligned p 6; page_directory_at' (p && ~~ (2 ^ pdBits - 1)) s; p \<le> p + 0x3F; pa \<in> set (tl (map ((\<lambda>x. p + x * 4) \<circ> word_of_nat) [0..<16])); is_aligned (pa >> 2) 4\<rbrakk> \<Longrightarrow> False
 2. \<And>x41 x42 x43 x44 x45 x46 p. \<lbrakk>pde = ARM_H.SuperSectionPDE x41 x42 x43 x44 x45 x46; xs = [p , p + 4 .e. p + mask 6]; is_aligned p 6; page_directory_at' (p && ~~ mask pdBits) s\<rbrakk> \<Longrightarrow> p \<le> p + mask 6 proof (prove)
goal (2 subgoals):
 1. \<And>x41 x42 x43 x44 x45 x46 p pa. \<lbrakk>pde = ARM_H.SuperSectionPDE x41 x42 x43 x44 x45 x46; xs = (if p + 0x3F < p then [] else map (\<lambda>x. p + x * (p + 4 - p)) [0 .e. (p + mask 6 - p) div (p + 4 - p)]); is_aligned p 6; page_directory_at' (p && ~~ (2 ^ pdBits - 1)) s; p \<le> p + 0x3F; pa \<in> set (map ((\<lambda>x. p + x * 4) \<circ> word_of_nat) (tl [0..<16])); is_aligned (pa >> 2) 4\<rbrakk> \<Longrightarrow> False
 2. \<And>x41 x42 x43 x44 x45 x46 p. \<lbrakk>pde = ARM_H.SuperSectionPDE x41 x42 x43 x44 x45 x46; xs = [p , p + 4 .e. p + mask 6]; is_aligned p 6; page_directory_at' (p && ~~ mask pdBits) s\<rbrakk> \<Longrightarrow> p \<le> p + mask 6 proof (prove)
goal (2 subgoals):
 1. \<And>x41 x42 x43 x44 x45 x46 p pa. \<lbrakk>pde = ARM_H.SuperSectionPDE x41 x42 x43 x44 x45 x46; xs = (if p + 0x3F < p then [] else map (\<lambda>x. p + x * (p + 4 - p)) [0 .e. (p + mask 6 - p) div (p + 4 - p)]); is_aligned p 6; page_directory_at' (p && ~~ (2 ^ pdBits - 1)) s; p \<le> p + 0x3F; pa \<in> (\<lambda>x. p + word_of_nat x * 4) ` {Suc 0..<16}; is_aligned (pa >> 2) 4\<rbrakk> \<Longrightarrow> False
 2. \<And>x41 x42 x43 x44 x45 x46 p. \<lbrakk>pde = ARM_H.SuperSectionPDE x41 x42 x43 x44 x45 x46; xs = [p , p + 4 .e. p + mask 6]; is_aligned p 6; page_directory_at' (p && ~~ mask pdBits) s\<rbrakk> \<Longrightarrow> p \<le> p + mask 6 proof (prove)
goal (2 subgoals):
 1. \<And>x41 x42 x43 x44 x45 x46 p x. \<lbrakk>pde = ARM_H.SuperSectionPDE x41 x42 x43 x44 x45 x46; xs = (if p + 0x3F < p then [] else map (\<lambda>x. p + x * (p + 4 - p)) [0 .e. (p + mask 6 - p) div (p + 4 - p)]); is_aligned p 6; page_directory_at' (p && ~~ (2 ^ pdBits - 1)) s; p \<le> p + 0x3F; is_aligned (p + word_of_nat x * 4 >> 2) 4; Suc 0 \<le> x; x < 16\<rbrakk> \<Longrightarrow> False
 2. \<And>x41 x42 x43 x44 x45 x46 p. \<lbrakk>pde = ARM_H.SuperSectionPDE x41 x42 x43 x44 x45 x46; xs = [p , p + 4 .e. p + mask 6]; is_aligned p 6; page_directory_at' (p && ~~ mask pdBits) s\<rbrakk> \<Longrightarrow> p \<le> p + mask 6 proof (prove)
goal (2 subgoals):
 1. \<And>x41 x42 x43 x44 x45 x46 p x. \<lbrakk>pde = ARM_H.SuperSectionPDE x41 x42 x43 x44 x45 x46; xs = (if p + 0x3F < p then [] else map (\<lambda>x. p + x * (p + 4 - p)) [0 .e. (p + mask 6 - p) div (p + 4 - p)]); is_aligned p 6; page_directory_at' (p && ~~ (2 ^ pdBits - 1)) s; p \<le> p + 0x3F; is_aligned (p + word_of_nat x * 4 >> 2) 4; Suc 0 \<le> x; x < 16; 4 * word_of_nat x = word_of_nat x << 2\<rbrakk> \<Longrightarrow> False
 2. \<And>x41 x42 x43 x44 x45 x46 p. \<lbrakk>pde = ARM_H.SuperSectionPDE x41 x42 x43 x44 x45 x46; xs = [p , p + 4 .e. p + mask 6]; is_aligned p 6; page_directory_at' (p && ~~ mask pdBits) s\<rbrakk> \<Longrightarrow> p \<le> p + mask 6 proof (prove)
goal (2 subgoals):
 1. \<And>x41 x42 x43 x44 x45 x46 p x. \<lbrakk>pde = ARM_H.SuperSectionPDE x41 x42 x43 x44 x45 x46; xs = (if p + 0x3F < p then [] else map (\<lambda>x. p + x * (p + 4 - p)) [0 .e. (p + mask 6 - p) div (p + 4 - p)]); is_aligned p 6; page_directory_at' (p && ~~ (2 ^ pdBits - 1)) s; p \<le> p + 0x3F; is_aligned (p + (word_of_nat x << 2) >> 2) 4; Suc 0 \<le> x; x < 16; word_of_nat x * 4 = word_of_nat x << 2\<rbrakk> \<Longrightarrow> False
 2. \<And>x41 x42 x43 x44 x45 x46 p. \<lbrakk>pde = ARM_H.SuperSectionPDE x41 x42 x43 x44 x45 x46; xs = [p , p + 4 .e. p + mask 6]; is_aligned p 6; page_directory_at' (p && ~~ mask pdBits) s\<rbrakk> \<Longrightarrow> p \<le> p + mask 6 proof (prove)
goal (2 subgoals):
 1. \<And>x41 x42 x43 x44 x45 x46 p x. \<lbrakk>pde = ARM_H.SuperSectionPDE x41 x42 x43 x44 x45 x46; xs = (if p + 0x3F < p then [] else map (\<lambda>x. p + x * (p + 4 - p)) [0 .e. (p + mask 6 - p) div (p + 4 - p)]); is_aligned p 6; page_directory_at' (p && ~~ (2 ^ pdBits - 1)) s; p \<le> p + 0x3F; Suc 0 \<le> x; x < 16; word_of_nat x * 4 = word_of_nat x << 2; is_aligned (p + (word_of_nat x << 2) >> 2 << 2) 6\<rbrakk> \<Longrightarrow> False
 2. \<And>x41 x42 x43 x44 x45 x46 p. \<lbrakk>pde = ARM_H.SuperSectionPDE x41 x42 x43 x44 x45 x46; xs = [p , p + 4 .e. p + mask 6]; is_aligned p 6; page_directory_at' (p && ~~ mask pdBits) s\<rbrakk> \<Longrightarrow> p \<le> p + mask 6 proof (prove)
goal (3 subgoals):
 1. \<And>x41 x42 x43 x44 x45 x46 p x. \<lbrakk>pde = ARM_H.SuperSectionPDE x41 x42 x43 x44 x45 x46; xs = (if p + 0x3F < p then [] else map (\<lambda>x. p + x * (p + 4 - p)) [0 .e. (p + mask 6 - p) div (p + 4 - p)]); is_aligned p 6; page_directory_at' (p && ~~ (2 ^ pdBits - 1)) s; p \<le> p + 0x3F; Suc 0 \<le> x; x < 16; word_of_nat x * 4 = word_of_nat x << 2\<rbrakk> \<Longrightarrow> 2 \<le> 2
 2. \<And>x41 x42 x43 x44 x45 x46 p x. \<lbrakk>pde = ARM_H.SuperSectionPDE x41 x42 x43 x44 x45 x46; xs = (if p + 0x3F < p then [] else map (\<lambda>x. p + x * (p + 4 - p)) [0 .e. (p + mask 6 - p) div (p + 4 - p)]); is_aligned p 6; page_directory_at' (p && ~~ (2 ^ pdBits - 1)) s; p \<le> p + 0x3F; Suc 0 \<le> x; x < 16; word_of_nat x * 4 = word_of_nat x << 2; is_aligned ((p + (word_of_nat x << 2) >> 2 - 2) && ~~ mask 2) 6\<rbrakk> \<Longrightarrow> False
 3. \<And>x41 x42 x43 x44 x45 x46 p. \<lbrakk>pde = ARM_H.SuperSectionPDE x41 x42 x43 x44 x45 x46; xs = [p , p + 4 .e. p + mask 6]; is_aligned p 6; page_directory_at' (p && ~~ mask pdBits) s\<rbrakk> \<Longrightarrow> p \<le> p + mask 6 proof (prove)
goal (2 subgoals):
 1. \<And>x41 x42 x43 x44 x45 x46 p x. \<lbrakk>pde = ARM_H.SuperSectionPDE x41 x42 x43 x44 x45 x46; xs = (if p + 0x3F < p then [] else map (\<lambda>x. p + x * (p + 4 - p)) [0 .e. (p + mask 6 - p) div (p + 4 - p)]); is_aligned p 6; page_directory_at' (p && ~~ (2 ^ pdBits - 1)) s; p \<le> p + 0x3F; Suc 0 \<le> x; x < 16; word_of_nat x * 4 = word_of_nat x << 2; is_aligned ((p + (word_of_nat x << 2) >> 2 - 2) && ~~ mask 2) 6\<rbrakk> \<Longrightarrow> False
 2. \<And>x41 x42 x43 x44 x45 x46 p. \<lbrakk>pde = ARM_H.SuperSectionPDE x41 x42 x43 x44 x45 x46; xs = [p , p + 4 .e. p + mask 6]; is_aligned p 6; page_directory_at' (p && ~~ mask pdBits) s\<rbrakk> \<Longrightarrow> p \<le> p + mask 6 proof (prove)
goal (2 subgoals):
 1. \<And>x41 x42 x43 x44 x45 x46 p x. \<lbrakk>pde = ARM_H.SuperSectionPDE x41 x42 x43 x44 x45 x46; xs = (if p + 0x3F < p then [] else map (\<lambda>x. p + x * (p + 4 - p)) [0 .e. (p + mask 6 - p) div (p + 4 - p)]); is_aligned p 6; page_directory_at' (p && ~~ (2 ^ pdBits - 1)) s; p \<le> p + 0x3F; Suc 0 \<le> x; x < 16; word_of_nat x * 4 = word_of_nat x << 2; is_aligned (p + (word_of_nat x << 2) && ~~ mask 2) 6\<rbrakk> \<Longrightarrow> False
 2. \<And>x41 x42 x43 x44 x45 x46 p. \<lbrakk>pde = ARM_H.SuperSectionPDE x41 x42 x43 x44 x45 x46; xs = [p , p + 4 .e. p + mask 6]; is_aligned p 6; page_directory_at' (p && ~~ mask pdBits) s\<rbrakk> \<Longrightarrow> p \<le> p + mask 6 proof (prove)
goal (3 subgoals):
 1. \<And>x41 x42 x43 x44 x45 x46 p x. \<lbrakk>pde = ARM_H.SuperSectionPDE x41 x42 x43 x44 x45 x46; xs = (if p + 0x3F < p then [] else map (\<lambda>x. p + x * (p + 4 - p)) [0 .e. (p + mask 6 - p) div (p + 4 - p)]); is_aligned p 6; page_directory_at' (p && ~~ (2 ^ pdBits - 1)) s; p \<le> p + 0x3F; Suc 0 \<le> x; x < 16; word_of_nat x * 4 = word_of_nat x << 2\<rbrakk> \<Longrightarrow> is_aligned (p + (word_of_nat x << 2)) 2
 2. \<And>x41 x42 x43 x44 x45 x46 p x. \<lbrakk>pde = ARM_H.SuperSectionPDE x41 x42 x43 x44 x45 x46; xs = (if p + 0x3F < p then [] else map (\<lambda>x. p + x * (p + 4 - p)) [0 .e. (p + mask 6 - p) div (p + 4 - p)]); is_aligned p 6; page_directory_at' (p && ~~ (2 ^ pdBits - 1)) s; p \<le> p + 0x3F; Suc 0 \<le> x; x < 16; word_of_nat x * 4 = word_of_nat x << 2; is_aligned (p + (word_of_nat x << 2)) 6\<rbrakk> \<Longrightarrow> False
 3. \<And>x41 x42 x43 x44 x45 x46 p. \<lbrakk>pde = ARM_H.SuperSectionPDE x41 x42 x43 x44 x45 x46; xs = [p , p + 4 .e. p + mask 6]; is_aligned p 6; page_directory_at' (p && ~~ mask pdBits) s\<rbrakk> \<Longrightarrow> p \<le> p + mask 6 proof (prove)
goal (3 subgoals):
 1. \<And>x41 x42 x43 x44 x45 x46 p x. \<lbrakk>pde = ARM_H.SuperSectionPDE x41 x42 x43 x44 x45 x46; xs = (if p + 0x3F < p then [] else map (\<lambda>x. p + x * (p + 4 - p)) [0 .e. (p + mask 6 - p) div (p + 4 - p)]); page_directory_at' (p && ~~ (2 ^ pdBits - 1)) s; p \<le> p + 0x3F; Suc 0 \<le> x; x < 16; word_of_nat x * 4 = word_of_nat x << 2\<rbrakk> \<Longrightarrow> 2 \<le> 6
 2. \<And>x41 x42 x43 x44 x45 x46 p x. \<lbrakk>pde = ARM_H.SuperSectionPDE x41 x42 x43 x44 x45 x46; xs = (if p + 0x3F < p then [] else map (\<lambda>x. p + x * (p + 4 - p)) [0 .e. (p + mask 6 - p) div (p + 4 - p)]); is_aligned p 6; page_directory_at' (p && ~~ (2 ^ pdBits - 1)) s; p \<le> p + 0x3F; Suc 0 \<le> x; x < 16; word_of_nat x * 4 = word_of_nat x << 2; is_aligned (p + (word_of_nat x << 2)) 6\<rbrakk> \<Longrightarrow> False
 3. \<And>x41 x42 x43 x44 x45 x46 p. \<lbrakk>pde = ARM_H.SuperSectionPDE x41 x42 x43 x44 x45 x46; xs = [p , p + 4 .e. p + mask 6]; is_aligned p 6; page_directory_at' (p && ~~ mask pdBits) s\<rbrakk> \<Longrightarrow> p \<le> p + mask 6 proof (prove)
goal (2 subgoals):
 1. \<And>x41 x42 x43 x44 x45 x46 p x. \<lbrakk>pde = ARM_H.SuperSectionPDE x41 x42 x43 x44 x45 x46; xs = (if p + 0x3F < p then [] else map (\<lambda>x. p + x * (p + 4 - p)) [0 .e. (p + mask 6 - p) div (p + 4 - p)]); is_aligned p 6; page_directory_at' (p && ~~ (2 ^ pdBits - 1)) s; p \<le> p + 0x3F; Suc 0 \<le> x; x < 16; word_of_nat x * 4 = word_of_nat x << 2; is_aligned (p + (word_of_nat x << 2)) 6\<rbrakk> \<Longrightarrow> False
 2. \<And>x41 x42 x43 x44 x45 x46 p. \<lbrakk>pde = ARM_H.SuperSectionPDE x41 x42 x43 x44 x45 x46; xs = [p , p + 4 .e. p + mask 6]; is_aligned p 6; page_directory_at' (p && ~~ mask pdBits) s\<rbrakk> \<Longrightarrow> p \<le> p + mask 6 proof (prove)
goal (2 subgoals):
 1. \<And>x41 x42 x43 x44 x45 x46 p x. \<lbrakk>pde = ARM_H.SuperSectionPDE x41 x42 x43 x44 x45 x46; xs = (if p + 0x3F < p then [] else map (\<lambda>x. p + x * (p + 4 - p)) [0 .e. (p + mask 6 - p) div (p + 4 - p)]); is_aligned p 6; page_directory_at' (p && ~~ (2 ^ pdBits - 1)) s; p \<le> p + 0x3F; Suc 0 \<le> x; x < 16; word_of_nat x * 4 = word_of_nat x << 2; is_aligned (word_of_nat x << 2) 6\<rbrakk> \<Longrightarrow> False
 2. \<And>x41 x42 x43 x44 x45 x46 p. \<lbrakk>pde = ARM_H.SuperSectionPDE x41 x42 x43 x44 x45 x46; xs = [p , p + 4 .e. p + mask 6]; is_aligned p 6; page_directory_at' (p && ~~ mask pdBits) s\<rbrakk> \<Longrightarrow> p \<le> p + mask 6 proof (prove)
goal (2 subgoals):
 1. \<And>x41 x42 x43 x44 x45 x46 p x. \<lbrakk>pde = ARM_H.SuperSectionPDE x41 x42 x43 x44 x45 x46; xs = (if p + 0x3F < p then [] else map (\<lambda>x. p + x * (p + 4 - p)) [0 .e. (p + mask 6 - p) div (p + 4 - p)]); is_aligned p 6; page_directory_at' (p && ~~ (2 ^ pdBits - 1)) s; p \<le> p + 0x3F; Suc 0 \<le> x; x < 16; word_of_nat x * 4 = word_of_nat x << 2; is_aligned (word_of_nat x << 2 >> 2) 4\<rbrakk> \<Longrightarrow> False
 2. \<And>x41 x42 x43 x44 x45 x46 p. \<lbrakk>pde = ARM_H.SuperSectionPDE x41 x42 x43 x44 x45 x46; xs = [p , p + 4 .e. p + mask 6]; is_aligned p 6; page_directory_at' (p && ~~ mask pdBits) s\<rbrakk> \<Longrightarrow> p \<le> p + mask 6 proof (prove)
goal (2 subgoals):
 1. \<And>x41 x42 x43 x44 x45 x46 p x. \<lbrakk>pde = ARM_H.SuperSectionPDE x41 x42 x43 x44 x45 x46; xs = (if p + 0x3F < p then [] else map (\<lambda>x. p + x * (p + 4 - p)) [0 .e. (p + mask 6 - p) div (p + 4 - p)]); is_aligned p 6; page_directory_at' (p && ~~ (2 ^ pdBits - 1)) s; p \<le> p + 0x3F; Suc 0 \<le> x; x < 16; word_of_nat x * 4 = word_of_nat x << 2; is_aligned (word_of_nat x) 4\<rbrakk> \<Longrightarrow> False
 2. \<And>x41 x42 x43 x44 x45 x46 p. \<lbrakk>pde = ARM_H.SuperSectionPDE x41 x42 x43 x44 x45 x46; xs = [p , p + 4 .e. p + mask 6]; is_aligned p 6; page_directory_at' (p && ~~ mask pdBits) s\<rbrakk> \<Longrightarrow> p \<le> p + mask 6 proof (prove)
goal (3 subgoals):
 1. \<And>x41 x42 x43 x44 x45 x46 p x. \<lbrakk>pde = ARM_H.SuperSectionPDE x41 x42 x43 x44 x45 x46; xs = (if p + 0x3F < p then [] else map (\<lambda>x. p + x * (p + 4 - p)) [0 .e. (p + mask 6 - p) div (p + 4 - p)]); is_aligned p 6; page_directory_at' (p && ~~ (2 ^ pdBits - 1)) s; p \<le> p + 0x3F; Suc 0 \<le> x; x < 16; word_of_nat x * 4 = word_of_nat x << 2\<rbrakk> \<Longrightarrow> word_of_nat x \<noteq> 0
 2. \<And>x41 x42 x43 x44 x45 x46 p x. \<lbrakk>pde = ARM_H.SuperSectionPDE x41 x42 x43 x44 x45 x46; xs = (if p + 0x3F < p then [] else map (\<lambda>x. p + x * (p + 4 - p)) [0 .e. (p + mask 6 - p) div (p + 4 - p)]); is_aligned p 6; page_directory_at' (p && ~~ (2 ^ pdBits - 1)) s; p \<le> p + 0x3F; Suc 0 \<le> x; x < 16; word_of_nat x * 4 = word_of_nat x << 2; 2 ^ 4 \<le> word_of_nat x\<rbrakk> \<Longrightarrow> False
 3. \<And>x41 x42 x43 x44 x45 x46 p. \<lbrakk>pde = ARM_H.SuperSectionPDE x41 x42 x43 x44 x45 x46; xs = [p , p + 4 .e. p + mask 6]; is_aligned p 6; page_directory_at' (p && ~~ mask pdBits) s\<rbrakk> \<Longrightarrow> p \<le> p + mask 6 proof (prove)
goal (4 subgoals):
 1. \<And>x41 x42 x43 x44 x45 x46 p x. \<lbrakk>pde = ARM_H.SuperSectionPDE x41 x42 x43 x44 x45 x46; xs = (if p + 0x3F < p then [] else map (\<lambda>x. p + x * (p + 4 - p)) [0 .e. (p + mask 6 - p) div (p + 4 - p)]); is_aligned p 6; page_directory_at' (p && ~~ (2 ^ pdBits - 1)) s; p \<le> p + 0x3F; Suc 0 \<le> x; x < 16; word_of_nat x * 4 = word_of_nat x << 2\<rbrakk> \<Longrightarrow> 0 < x
 2. \<And>x41 x42 x43 x44 x45 x46 p x. \<lbrakk>pde = ARM_H.SuperSectionPDE x41 x42 x43 x44 x45 x46; xs = (if p + 0x3F < p then [] else map (\<lambda>x. p + x * (p + 4 - p)) [0 .e. (p + mask 6 - p) div (p + 4 - p)]); is_aligned p 6; page_directory_at' (p && ~~ (2 ^ pdBits - 1)) s; p \<le> p + 0x3F; Suc 0 \<le> x; x < 16; word_of_nat x * 4 = word_of_nat x << 2\<rbrakk> \<Longrightarrow> x < 2 ^ LENGTH(32)
 3. \<And>x41 x42 x43 x44 x45 x46 p x. \<lbrakk>pde = ARM_H.SuperSectionPDE x41 x42 x43 x44 x45 x46; xs = (if p + 0x3F < p then [] else map (\<lambda>x. p + x * (p + 4 - p)) [0 .e. (p + mask 6 - p) div (p + 4 - p)]); is_aligned p 6; page_directory_at' (p && ~~ (2 ^ pdBits - 1)) s; p \<le> p + 0x3F; Suc 0 \<le> x; x < 16; word_of_nat x * 4 = word_of_nat x << 2; 2 ^ 4 \<le> word_of_nat x\<rbrakk> \<Longrightarrow> False
 4. \<And>x41 x42 x43 x44 x45 x46 p. \<lbrakk>pde = ARM_H.SuperSectionPDE x41 x42 x43 x44 x45 x46; xs = [p , p + 4 .e. p + mask 6]; is_aligned p 6; page_directory_at' (p && ~~ mask pdBits) s\<rbrakk> \<Longrightarrow> p \<le> p + mask 6 proof (prove)
goal (3 subgoals):
 1. \<And>x41 x42 x43 x44 x45 x46 p x. \<lbrakk>pde = ARM_H.SuperSectionPDE x41 x42 x43 x44 x45 x46; xs = (if p + 0x3F < p then [] else map (\<lambda>x. p + x * (p + 4 - p)) [0 .e. (p + mask 6 - p) div (p + 4 - p)]); is_aligned p 6; page_directory_at' (p && ~~ (2 ^ pdBits - 1)) s; p \<le> p + 0x3F; Suc 0 \<le> x; x < 16; word_of_nat x * 4 = word_of_nat x << 2\<rbrakk> \<Longrightarrow> x < 2 ^ LENGTH(32)
 2. \<And>x41 x42 x43 x44 x45 x46 p x. \<lbrakk>pde = ARM_H.SuperSectionPDE x41 x42 x43 x44 x45 x46; xs = (if p + 0x3F < p then [] else map (\<lambda>x. p + x * (p + 4 - p)) [0 .e. (p + mask 6 - p) div (p + 4 - p)]); is_aligned p 6; page_directory_at' (p && ~~ (2 ^ pdBits - 1)) s; p \<le> p + 0x3F; Suc 0 \<le> x; x < 16; word_of_nat x * 4 = word_of_nat x << 2; 2 ^ 4 \<le> word_of_nat x\<rbrakk> \<Longrightarrow> False
 3. \<And>x41 x42 x43 x44 x45 x46 p. \<lbrakk>pde = ARM_H.SuperSectionPDE x41 x42 x43 x44 x45 x46; xs = [p , p + 4 .e. p + mask 6]; is_aligned p 6; page_directory_at' (p && ~~ mask pdBits) s\<rbrakk> \<Longrightarrow> p \<le> p + mask 6 proof (prove)
goal (2 subgoals):
 1. \<And>x41 x42 x43 x44 x45 x46 p x. \<lbrakk>pde = ARM_H.SuperSectionPDE x41 x42 x43 x44 x45 x46; xs = (if p + 0x3F < p then [] else map (\<lambda>x. p + x * (p + 4 - p)) [0 .e. (p + mask 6 - p) div (p + 4 - p)]); is_aligned p 6; page_directory_at' (p && ~~ (2 ^ pdBits - 1)) s; p \<le> p + 0x3F; Suc 0 \<le> x; x < 16; word_of_nat x * 4 = word_of_nat x << 2; 2 ^ 4 \<le> word_of_nat x\<rbrakk> \<Longrightarrow> False
 2. \<And>x41 x42 x43 x44 x45 x46 p. \<lbrakk>pde = ARM_H.SuperSectionPDE x41 x42 x43 x44 x45 x46; xs = [p , p + 4 .e. p + mask 6]; is_aligned p 6; page_directory_at' (p && ~~ mask pdBits) s\<rbrakk> \<Longrightarrow> p \<le> p + mask 6 proof (prove)
goal (2 subgoals):
 1. \<And>x41 x42 x43 x44 x45 x46 p x. \<lbrakk>pde = ARM_H.SuperSectionPDE x41 x42 x43 x44 x45 x46; xs = (if p + 0x3F < p then [] else map (\<lambda>x. p + x * (p + 4 - p)) [0 .e. (p + mask 6 - p) div (p + 4 - p)]); is_aligned p 6; page_directory_at' (p && ~~ (2 ^ pdBits - 1)) s; p \<le> p + 0x3F; Suc 0 \<le> x; x < 16; word_of_nat x * 4 = word_of_nat x << 2; unat (2 ^ 4) \<le> x\<rbrakk> \<Longrightarrow> False
 2. \<And>x41 x42 x43 x44 x45 x46 p. \<lbrakk>pde = ARM_H.SuperSectionPDE x41 x42 x43 x44 x45 x46; xs = [p , p + 4 .e. p + mask 6]; is_aligned p 6; page_directory_at' (p && ~~ mask pdBits) s\<rbrakk> \<Longrightarrow> p \<le> p + mask 6 proof (prove)
goal (1 subgoal):
 1. \<And>x41 x42 x43 x44 x45 x46 p. \<lbrakk>pde = ARM_H.SuperSectionPDE x41 x42 x43 x44 x45 x46; xs = [p , p + 4 .e. p + mask 6]; is_aligned p 6; page_directory_at' (p && ~~ mask pdBits) s\<rbrakk> \<Longrightarrow> p \<le> p + mask 6 proof (prove)
goal (1 subgoal):
 1. \<And>x41 x42 x43 x44 x45 x46 p. \<lbrakk>pde = ARM_H.SuperSectionPDE x41 x42 x43 x44 x45 x46; xs = [p , p + 4 .e. p + mask 6]; page_directory_at' (p && ~~ mask pdBits) s\<rbrakk> \<Longrightarrow> mask 6 < 2 ^ 6 proof (prove)
goal:
No subgoals! proof (state)
this:
is_aligned (hd xs >> 2) (pde_align' pde) \<and> (\<forall>p\<in>set (tl xs). \<not> is_aligned (p >> 2) (pde_align' pde))

goal:
No subgoals!