theory Detype_R

lemma getPDE_det:
  "ko_wp_at' ((=) (KOArch (KOPDE pde))) p s
   \<Longrightarrow> getObject p s = ({((pde::ARM_H.pde),s)},False)" apply (clarsimp simp:ko_wp_at'_def getObject_def split_def
                       bind_def gets_def return_def get_def
                       assert_opt_def split:if_splits) apply (clarsimp simp: fail_def return_def lookupAround2_known1) apply (simp add: loadObject_default_def) apply (clarsimp simp:projectKO_def projectKO_opt_pde alignCheck_def
    is_aligned_mask objBits_simps unless_def) apply (clarsimp simp:bind_def return_def) apply (intro conjI) apply (intro set_eqI iffI) apply clarsimp apply (subst (asm) in_magnitude_check') apply (simp add:archObjSize_def is_aligned_mask pteBits_def pdeBits_def)+ apply (rule bexI[rotated]) apply (rule in_magnitude_check'[THEN iffD2]) apply (simp add:is_aligned_mask)+ apply (clarsimp simp:image_def) apply (clarsimp simp:magnitudeCheck_assert assert_def
    objBits_def archObjSize_def
    return_def fail_def lookupAround2_char2 split:option.splits if_split_asm) apply (rule ccontr) apply (simp add:ps_clear_def field_simps pteBits_def pdeBits_def) apply (erule_tac x = x2 in in_empty_interE) apply (clarsimp simp:less_imp_le) apply (rule conjI) apply (subst add.commute) apply (rule word_diff_ls') apply (clarsimp simp: not_le plus_one_helper) apply (subst add.commute) apply (simp add: is_aligned_no_wrap' is_aligned_mask) apply auto done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. ko_wp_at' ((=) (KOArch (KOPDE pde))) p s \<Longrightarrow> getObject p s = ({(pde, s)}, False) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>ksPSpace s p = Some (KOArch (KOPDE pde)); is_aligned p (objBitsKO (KOArch (KOPDE pde))); ps_clear p (objBitsKO (KOArch (KOPDE pde))) s\<rbrakk> \<Longrightarrow> (\<Union>x\<in>fst ((case fst (lookupAround2 p (ksPSpace s)) of None \<Rightarrow> fail | Some v \<Rightarrow> \<lambda>s. ({(v, s)}, False)) s). fst (loadObject_default p (fst (fst x)) (snd (lookupAround2 p (ksPSpace s))) (snd (fst x)) (snd x))) = {(pde, s)} \<and> (\<forall>x\<in>fst ((case fst (lookupAround2 p (ksPSpace s)) of None \<Rightarrow> fail | Some v \<Rightarrow> \<lambda>s. ({(v, s)}, False)) s). \<not> snd (loadObject_default p (fst (fst x)) (snd (lookupAround2 p (ksPSpace s))) (snd (fst x)) (snd x))) \<and> \<not> snd ((case fst (lookupAround2 p (ksPSpace s)) of None \<Rightarrow> fail | Some v \<Rightarrow> \<lambda>s. ({(v, s)}, False)) s) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>ksPSpace s p = Some (KOArch (KOPDE pde)); is_aligned p (objBitsKO (KOArch (KOPDE pde))); ps_clear p (objBitsKO (KOArch (KOPDE pde))) s\<rbrakk> \<Longrightarrow> fst (loadObject_default p p (snd (lookupAround2 p (ksPSpace s))) (KOArch (KOPDE pde)) s) = {(pde, s)} \<and> \<not> snd (loadObject_default p p (snd (lookupAround2 p (ksPSpace s))) (KOArch (KOPDE pde)) s) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>ksPSpace s p = Some (KOArch (KOPDE pde)); is_aligned p (objBitsKO (KOArch (KOPDE pde))); ps_clear p (objBitsKO (KOArch (KOPDE pde))) s\<rbrakk> \<Longrightarrow> fst ((do val <- projectKO (KOArch (KOPDE pde));
y <- alignCheck p (objBits val);
y <- magnitudeCheck p (snd (lookupAround2 p (ksPSpace s))) (objBits val);
return val
od) s) = {(pde, s)} \<and> \<not> snd ((do val <- projectKO (KOArch (KOPDE pde));
y <- alignCheck p (objBits val);
y <- magnitudeCheck p (snd (lookupAround2 p (ksPSpace s))) (objBits val);
return val
od) s) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>ksPSpace s p = Some (KOArch (KOPDE pde)); p && mask (archObjSize (KOPDE pde)) = 0; ps_clear p (archObjSize (KOPDE pde)) s\<rbrakk> \<Longrightarrow> fst ((do y <- magnitudeCheck p (snd (lookupAround2 p (ksPSpace s))) (archObjSize (KOPDE pde));
return pde
od) s) = {(pde, s)} \<and> \<not> snd (magnitudeCheck p (snd (lookupAround2 p (ksPSpace s))) (archObjSize (KOPDE pde)) s) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>ksPSpace s p = Some (KOArch (KOPDE pde)); p && mask (archObjSize (KOPDE pde)) = 0; ps_clear p (archObjSize (KOPDE pde)) s\<rbrakk> \<Longrightarrow> (\<Union>a\<in>fst (magnitudeCheck p (snd (lookupAround2 p (ksPSpace s))) (archObjSize (KOPDE pde)) s). fst (case a of (y, s) \<Rightarrow> ({(pde, s)}, False))) = {(pde, s)} \<and> \<not> snd (magnitudeCheck p (snd (lookupAround2 p (ksPSpace s))) (archObjSize (KOPDE pde)) s) proof (prove)
goal (2 subgoals):
 1. \<lbrakk>ksPSpace s p = Some (KOArch (KOPDE pde)); p && mask (archObjSize (KOPDE pde)) = 0; ps_clear p (archObjSize (KOPDE pde)) s\<rbrakk> \<Longrightarrow> (\<Union>a\<in>fst (magnitudeCheck p (snd (lookupAround2 p (ksPSpace s))) (archObjSize (KOPDE pde)) s). fst (case a of (y, s) \<Rightarrow> ({(pde, s)}, False))) = {(pde, s)}
 2. \<lbrakk>ksPSpace s p = Some (KOArch (KOPDE pde)); p && mask (archObjSize (KOPDE pde)) = 0; ps_clear p (archObjSize (KOPDE pde)) s\<rbrakk> \<Longrightarrow> \<not> snd (magnitudeCheck p (snd (lookupAround2 p (ksPSpace s))) (archObjSize (KOPDE pde)) s) proof (prove)
goal (3 subgoals):
 1. \<And>x. \<lbrakk>ksPSpace s p = Some (KOArch (KOPDE pde)); p && mask (archObjSize (KOPDE pde)) = 0; ps_clear p (archObjSize (KOPDE pde)) s; x \<in> (\<Union>a\<in>fst (magnitudeCheck p (snd (lookupAround2 p (ksPSpace s))) (archObjSize (KOPDE pde)) s). fst (case a of (y, s) \<Rightarrow> ({(pde, s)}, False)))\<rbrakk> \<Longrightarrow> x \<in> {(pde, s)}
 2. \<And>x. \<lbrakk>ksPSpace s p = Some (KOArch (KOPDE pde)); p && mask (archObjSize (KOPDE pde)) = 0; ps_clear p (archObjSize (KOPDE pde)) s; x \<in> {(pde, s)}\<rbrakk> \<Longrightarrow> x \<in> (\<Union>a\<in>fst (magnitudeCheck p (snd (lookupAround2 p (ksPSpace s))) (archObjSize (KOPDE pde)) s). fst (case a of (y, s) \<Rightarrow> ({(pde, s)}, False)))
 3. \<lbrakk>ksPSpace s p = Some (KOArch (KOPDE pde)); p && mask (archObjSize (KOPDE pde)) = 0; ps_clear p (archObjSize (KOPDE pde)) s\<rbrakk> \<Longrightarrow> \<not> snd (magnitudeCheck p (snd (lookupAround2 p (ksPSpace s))) (archObjSize (KOPDE pde)) s) proof (prove)
goal (3 subgoals):
 1. \<And>b. \<lbrakk>ksPSpace s p = Some (KOArch (KOPDE pde)); p && mask (archObjSize (KOPDE pde)) = 0; ps_clear p (archObjSize (KOPDE pde)) s; ((), b) \<in> fst (magnitudeCheck p (snd (lookupAround2 p (ksPSpace s))) (archObjSize (KOPDE pde)) s)\<rbrakk> \<Longrightarrow> b = s
 2. \<And>x. \<lbrakk>ksPSpace s p = Some (KOArch (KOPDE pde)); p && mask (archObjSize (KOPDE pde)) = 0; ps_clear p (archObjSize (KOPDE pde)) s; x \<in> {(pde, s)}\<rbrakk> \<Longrightarrow> x \<in> (\<Union>a\<in>fst (magnitudeCheck p (snd (lookupAround2 p (ksPSpace s))) (archObjSize (KOPDE pde)) s). fst (case a of (y, s) \<Rightarrow> ({(pde, s)}, False)))
 3. \<lbrakk>ksPSpace s p = Some (KOArch (KOPDE pde)); p && mask (archObjSize (KOPDE pde)) = 0; ps_clear p (archObjSize (KOPDE pde)) s\<rbrakk> \<Longrightarrow> \<not> snd (magnitudeCheck p (snd (lookupAround2 p (ksPSpace s))) (archObjSize (KOPDE pde)) s) proof (prove)
goal (7 subgoals):
 1. \<And>b. \<lbrakk>ksPSpace s p = Some (KOArch (KOPDE pde)); p && mask (archObjSize (KOPDE pde)) = 0; ps_clear p (archObjSize (KOPDE pde)) s\<rbrakk> \<Longrightarrow> is_aligned p (archObjSize (KOPDE pde))
 2. \<And>b. \<lbrakk>ksPSpace s p = Some (KOArch (KOPDE pde)); p && mask (archObjSize (KOPDE pde)) = 0; ps_clear p (archObjSize (KOPDE pde)) s\<rbrakk> \<Longrightarrow> 1 < 2 ^ archObjSize (KOPDE pde)
 3. \<And>b. \<lbrakk>ksPSpace s p = Some (KOArch (KOPDE pde)); p && mask (archObjSize (KOPDE pde)) = 0; ps_clear p (archObjSize (KOPDE pde)) s\<rbrakk> \<Longrightarrow> ksPSpace s p = Some (?y36 b)
 4. \<And>b. \<lbrakk>ksPSpace s p = Some (KOArch (KOPDE pde)); p && mask (archObjSize (KOPDE pde)) = 0; ps_clear p (archObjSize (KOPDE pde)) s\<rbrakk> \<Longrightarrow> ksPSpace s = ksPSpace s
 5. \<And>b. \<lbrakk>ksPSpace s p = Some (KOArch (KOPDE pde)); p && mask (archObjSize (KOPDE pde)) = 0; ps_clear p (archObjSize (KOPDE pde)) s; b = s \<and> ps_clear p (archObjSize (KOPDE pde)) s\<rbrakk> \<Longrightarrow> b = s
 6. \<And>x. \<lbrakk>ksPSpace s p = Some (KOArch (KOPDE pde)); p && mask (archObjSize (KOPDE pde)) = 0; ps_clear p (archObjSize (KOPDE pde)) s; x \<in> {(pde, s)}\<rbrakk> \<Longrightarrow> x \<in> (\<Union>a\<in>fst (magnitudeCheck p (snd (lookupAround2 p (ksPSpace s))) (archObjSize (KOPDE pde)) s). fst (case a of (y, s) \<Rightarrow> ({(pde, s)}, False)))
 7. \<lbrakk>ksPSpace s p = Some (KOArch (KOPDE pde)); p && mask (archObjSize (KOPDE pde)) = 0; ps_clear p (archObjSize (KOPDE pde)) s\<rbrakk> \<Longrightarrow> \<not> snd (magnitudeCheck p (snd (lookupAround2 p (ksPSpace s))) (archObjSize (KOPDE pde)) s) proof (prove)
goal (2 subgoals):
 1. \<And>x. \<lbrakk>ksPSpace s p = Some (KOArch (KOPDE pde)); p && mask 2 = 0; ps_clear p 2 s; x = (pde, s)\<rbrakk> \<Longrightarrow> \<exists>x\<in>fst (magnitudeCheck p (snd (lookupAround2 p (ksPSpace s))) 2 s). (pde, s) \<in> fst (case x of (y, s) \<Rightarrow> ({(pde, s)}, False))
 2. \<lbrakk>ksPSpace s p = Some (KOArch (KOPDE pde)); p && mask (archObjSize (KOPDE pde)) = 0; ps_clear p (archObjSize (KOPDE pde)) s\<rbrakk> \<Longrightarrow> \<not> snd (magnitudeCheck p (snd (lookupAround2 p (ksPSpace s))) (archObjSize (KOPDE pde)) s) proof (prove)
goal (3 subgoals):
 1. \<And>x. \<lbrakk>ksPSpace s p = Some (KOArch (KOPDE pde)); p && mask 2 = 0; ps_clear p 2 s; x = (pde, s)\<rbrakk> \<Longrightarrow> ?x39 x \<in> fst (magnitudeCheck p (snd (lookupAround2 p (ksPSpace s))) 2 s)
 2. \<And>x. \<lbrakk>ksPSpace s p = Some (KOArch (KOPDE pde)); p && mask 2 = 0; ps_clear p 2 s; x = (pde, s)\<rbrakk> \<Longrightarrow> (pde, s) \<in> fst (case ?x39 x of (y, s) \<Rightarrow> ({(pde, s)}, False))
 3. \<lbrakk>ksPSpace s p = Some (KOArch (KOPDE pde)); p && mask (archObjSize (KOPDE pde)) = 0; ps_clear p (archObjSize (KOPDE pde)) s\<rbrakk> \<Longrightarrow> \<not> snd (magnitudeCheck p (snd (lookupAround2 p (ksPSpace s))) (archObjSize (KOPDE pde)) s) proof (prove)
goal (7 subgoals):
 1. \<And>x. \<lbrakk>ksPSpace s p = Some (KOArch (KOPDE pde)); p && mask 2 = 0; ps_clear p 2 s; x = (pde, s)\<rbrakk> \<Longrightarrow> is_aligned p 2
 2. \<And>x. \<lbrakk>ksPSpace s p = Some (KOArch (KOPDE pde)); p && mask 2 = 0; ps_clear p 2 s; x = (pde, s)\<rbrakk> \<Longrightarrow> 1 < 2\<^sup>2
 3. \<And>x. \<lbrakk>ksPSpace s p = Some (KOArch (KOPDE pde)); p && mask 2 = 0; ps_clear p 2 s; x = (pde, s)\<rbrakk> \<Longrightarrow> ksPSpace s p = Some (?y43 x)
 4. \<And>x. \<lbrakk>ksPSpace s p = Some (KOArch (KOPDE pde)); p && mask 2 = 0; ps_clear p 2 s; x = (pde, s)\<rbrakk> \<Longrightarrow> ksPSpace s = ksPSpace s
 5. \<And>x. \<lbrakk>ksPSpace s p = Some (KOArch (KOPDE pde)); p && mask 2 = 0; ps_clear p 2 s; x = (pde, s)\<rbrakk> \<Longrightarrow> ?s'43 x = s \<and> ps_clear p 2 s
 6. \<And>x. \<lbrakk>ksPSpace s p = Some (KOArch (KOPDE pde)); p && mask 2 = 0; ps_clear p 2 s; x = (pde, s)\<rbrakk> \<Longrightarrow> (pde, s) \<in> fst (case (?v43 x, ?s'43 x) of (y, s) \<Rightarrow> ({(pde, s)}, False))
 7. \<lbrakk>ksPSpace s p = Some (KOArch (KOPDE pde)); p && mask (archObjSize (KOPDE pde)) = 0; ps_clear p (archObjSize (KOPDE pde)) s\<rbrakk> \<Longrightarrow> \<not> snd (magnitudeCheck p (snd (lookupAround2 p (ksPSpace s))) (archObjSize (KOPDE pde)) s) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>ksPSpace s p = Some (KOArch (KOPDE pde)); p && mask (archObjSize (KOPDE pde)) = 0; ps_clear p (archObjSize (KOPDE pde)) s\<rbrakk> \<Longrightarrow> \<not> snd (magnitudeCheck p (snd (lookupAround2 p (ksPSpace s))) (archObjSize (KOPDE pde)) s) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>ksPSpace s p = Some (KOArch (KOPDE pde)); p && mask (archObjSize (KOPDE pde)) = 0; ps_clear p (archObjSize (KOPDE pde)) s; snd (magnitudeCheck p (snd (lookupAround2 p (ksPSpace s))) (archObjSize (KOPDE pde)) s)\<rbrakk> \<Longrightarrow> False proof (prove)
goal (1 subgoal):
 1. \<And>x2 y. \<lbrakk>ksPSpace s p = Some (KOArch (KOPDE pde)); p && mask pdeBits = 0; ps_clear p pdeBits s; \<not> 2 ^ pdeBits \<le> x2 - p; p < x2; \<forall>z. p < z \<and> z < x2 \<longrightarrow> ksPSpace s z = None; ksPSpace s x2 = Some y\<rbrakk> \<Longrightarrow> False proof (prove)
goal (1 subgoal):
 1. \<And>x2 y. \<lbrakk>ksPSpace s p = Some (KOArch (KOPDE pde)); p && mask pdeBits = 0; ps_clear p pdeBits s; \<not> 2 ^ pdeBits \<le> x2 - p; p < x2; \<forall>z. p < z \<and> z < x2 \<longrightarrow> ksPSpace s z = None; ksPSpace s x2 = Some y; \<not> False\<rbrakk> \<Longrightarrow> False proof (prove)
goal (1 subgoal):
 1. \<And>x2 y. \<lbrakk>ksPSpace s p = Some (KOArch (KOPDE pde)); p && mask 2 = 0; ({p..p + 3} - {p}) \<inter> dom (ksPSpace s) = {}; \<not> 4 \<le> x2 - p; p < x2; \<forall>z. p < z \<and> z < x2 \<longrightarrow> ksPSpace s z = None; ksPSpace s x2 = Some y\<rbrakk> \<Longrightarrow> False proof (prove)
goal (2 subgoals):
 1. \<And>x2 y. \<lbrakk>ksPSpace s p = Some (KOArch (KOPDE pde)); p && mask 2 = 0; \<not> 4 \<le> x2 - p; p < x2; \<forall>z. p < z \<and> z < x2 \<longrightarrow> ksPSpace s z = None; ksPSpace s x2 = Some y\<rbrakk> \<Longrightarrow> x2 \<in> {p..p + 3} - {p}
 2. \<And>x2 y. \<lbrakk>ksPSpace s p = Some (KOArch (KOPDE pde)); p && mask 2 = 0; \<not> 4 \<le> x2 - p; p < x2; \<forall>z. p < z \<and> z < x2 \<longrightarrow> ksPSpace s z = None; ksPSpace s x2 = Some y\<rbrakk> \<Longrightarrow> x2 \<in> dom (ksPSpace s) proof (prove)
goal (2 subgoals):
 1. \<And>x2 y. \<lbrakk>ksPSpace s p = Some (KOArch (KOPDE pde)); p && mask 2 = 0; \<not> 4 \<le> x2 - p; p < x2; \<forall>z. p < z \<and> z < x2 \<longrightarrow> ksPSpace s z = None; ksPSpace s x2 = Some y\<rbrakk> \<Longrightarrow> x2 \<le> p + 3 \<and> x2 \<noteq> p
 2. \<And>x2 y. \<lbrakk>ksPSpace s p = Some (KOArch (KOPDE pde)); p && mask 2 = 0; \<not> 4 \<le> x2 - p; p < x2; \<forall>z. p < z \<and> z < x2 \<longrightarrow> ksPSpace s z = None; ksPSpace s x2 = Some y\<rbrakk> \<Longrightarrow> x2 \<in> dom (ksPSpace s) proof (prove)
goal (3 subgoals):
 1. \<And>x2 y. \<lbrakk>ksPSpace s p = Some (KOArch (KOPDE pde)); p && mask 2 = 0; \<not> 4 \<le> x2 - p; p < x2; \<forall>z. p < z \<and> z < x2 \<longrightarrow> ksPSpace s z = None; ksPSpace s x2 = Some y\<rbrakk> \<Longrightarrow> x2 \<le> p + 3
 2. \<And>x2 y. \<lbrakk>ksPSpace s p = Some (KOArch (KOPDE pde)); p && mask 2 = 0; \<not> 4 \<le> x2 - p; p < x2; \<forall>z. p < z \<and> z < x2 \<longrightarrow> ksPSpace s z = None; ksPSpace s x2 = Some y\<rbrakk> \<Longrightarrow> x2 \<noteq> p
 3. \<And>x2 y. \<lbrakk>ksPSpace s p = Some (KOArch (KOPDE pde)); p && mask 2 = 0; \<not> 4 \<le> x2 - p; p < x2; \<forall>z. p < z \<and> z < x2 \<longrightarrow> ksPSpace s z = None; ksPSpace s x2 = Some y\<rbrakk> \<Longrightarrow> x2 \<in> dom (ksPSpace s) proof (prove)
goal (3 subgoals):
 1. \<And>x2 y. \<lbrakk>ksPSpace s p = Some (KOArch (KOPDE pde)); p && mask 2 = 0; \<not> 4 \<le> x2 - p; p < x2; \<forall>z. p < z \<and> z < x2 \<longrightarrow> ksPSpace s z = None; ksPSpace s x2 = Some y\<rbrakk> \<Longrightarrow> x2 \<le> 3 + p
 2. \<And>x2 y. \<lbrakk>ksPSpace s p = Some (KOArch (KOPDE pde)); p && mask 2 = 0; \<not> 4 \<le> x2 - p; p < x2; \<forall>z. p < z \<and> z < x2 \<longrightarrow> ksPSpace s z = None; ksPSpace s x2 = Some y\<rbrakk> \<Longrightarrow> x2 \<noteq> p
 3. \<And>x2 y. \<lbrakk>ksPSpace s p = Some (KOArch (KOPDE pde)); p && mask 2 = 0; \<not> 4 \<le> x2 - p; p < x2; \<forall>z. p < z \<and> z < x2 \<longrightarrow> ksPSpace s z = None; ksPSpace s x2 = Some y\<rbrakk> \<Longrightarrow> x2 \<in> dom (ksPSpace s) proof (prove)
goal (4 subgoals):
 1. \<And>x2 y. \<lbrakk>ksPSpace s p = Some (KOArch (KOPDE pde)); p && mask 2 = 0; \<not> 4 \<le> x2 - p; p < x2; \<forall>z. p < z \<and> z < x2 \<longrightarrow> ksPSpace s z = None; ksPSpace s x2 = Some y\<rbrakk> \<Longrightarrow> x2 - p \<le> 3
 2. \<And>x2 y. \<lbrakk>ksPSpace s p = Some (KOArch (KOPDE pde)); p && mask 2 = 0; \<not> 4 \<le> x2 - p; p < x2; \<forall>z. p < z \<and> z < x2 \<longrightarrow> ksPSpace s z = None; ksPSpace s x2 = Some y\<rbrakk> \<Longrightarrow> p \<le> 3 + p
 3. \<And>x2 y. \<lbrakk>ksPSpace s p = Some (KOArch (KOPDE pde)); p && mask 2 = 0; \<not> 4 \<le> x2 - p; p < x2; \<forall>z. p < z \<and> z < x2 \<longrightarrow> ksPSpace s z = None; ksPSpace s x2 = Some y\<rbrakk> \<Longrightarrow> x2 \<noteq> p
 4. \<And>x2 y. \<lbrakk>ksPSpace s p = Some (KOArch (KOPDE pde)); p && mask 2 = 0; \<not> 4 \<le> x2 - p; p < x2; \<forall>z. p < z \<and> z < x2 \<longrightarrow> ksPSpace s z = None; ksPSpace s x2 = Some y\<rbrakk> \<Longrightarrow> x2 \<in> dom (ksPSpace s) proof (prove)
goal (3 subgoals):
 1. \<And>x2 y. \<lbrakk>ksPSpace s p = Some (KOArch (KOPDE pde)); p && mask 2 = 0; \<not> 4 \<le> x2 - p; p < x2; \<forall>z. p < z \<and> z < x2 \<longrightarrow> ksPSpace s z = None; ksPSpace s x2 = Some y\<rbrakk> \<Longrightarrow> p \<le> 3 + p
 2. \<And>x2 y. \<lbrakk>ksPSpace s p = Some (KOArch (KOPDE pde)); p && mask 2 = 0; \<not> 4 \<le> x2 - p; p < x2; \<forall>z. p < z \<and> z < x2 \<longrightarrow> ksPSpace s z = None; ksPSpace s x2 = Some y\<rbrakk> \<Longrightarrow> x2 \<noteq> p
 3. \<And>x2 y. \<lbrakk>ksPSpace s p = Some (KOArch (KOPDE pde)); p && mask 2 = 0; \<not> 4 \<le> x2 - p; p < x2; \<forall>z. p < z \<and> z < x2 \<longrightarrow> ksPSpace s z = None; ksPSpace s x2 = Some y\<rbrakk> \<Longrightarrow> x2 \<in> dom (ksPSpace s) proof (prove)
goal (3 subgoals):
 1. \<And>x2 y. \<lbrakk>ksPSpace s p = Some (KOArch (KOPDE pde)); p && mask 2 = 0; \<not> 4 \<le> x2 - p; p < x2; \<forall>z. p < z \<and> z < x2 \<longrightarrow> ksPSpace s z = None; ksPSpace s x2 = Some y\<rbrakk> \<Longrightarrow> p \<le> p + 3
 2. \<And>x2 y. \<lbrakk>ksPSpace s p = Some (KOArch (KOPDE pde)); p && mask 2 = 0; \<not> 4 \<le> x2 - p; p < x2; \<forall>z. p < z \<and> z < x2 \<longrightarrow> ksPSpace s z = None; ksPSpace s x2 = Some y\<rbrakk> \<Longrightarrow> x2 \<noteq> p
 3. \<And>x2 y. \<lbrakk>ksPSpace s p = Some (KOArch (KOPDE pde)); p && mask 2 = 0; \<not> 4 \<le> x2 - p; p < x2; \<forall>z. p < z \<and> z < x2 \<longrightarrow> ksPSpace s z = None; ksPSpace s x2 = Some y\<rbrakk> \<Longrightarrow> x2 \<in> dom (ksPSpace s) proof (prove)
goal (2 subgoals):
 1. \<And>x2 y. \<lbrakk>ksPSpace s p = Some (KOArch (KOPDE pde)); p && mask 2 = 0; \<not> 4 \<le> x2 - p; p < x2; \<forall>z. p < z \<and> z < x2 \<longrightarrow> ksPSpace s z = None; ksPSpace s x2 = Some y\<rbrakk> \<Longrightarrow> x2 \<noteq> p
 2. \<And>x2 y. \<lbrakk>ksPSpace s p = Some (KOArch (KOPDE pde)); p && mask 2 = 0; \<not> 4 \<le> x2 - p; p < x2; \<forall>z. p < z \<and> z < x2 \<longrightarrow> ksPSpace s z = None; ksPSpace s x2 = Some y\<rbrakk> \<Longrightarrow> x2 \<in> dom (ksPSpace s) proof (prove)
goal:
No subgoals!