theory Invariants_H

lemma in_magnitude_check3:
  "\<lbrakk> \<forall>z. x < z \<and> z \<le> y \<longrightarrow> ksPSpace s z = None; is_aligned x n;
     (1 :: word32) < 2 ^ n; ksPSpace s x = Some v; x \<le> y; y - x < 2 ^ n \<rbrakk> \<Longrightarrow>
   fst (magnitudeCheck x (snd (lookupAround2 y (ksPSpace s))) n s)
     = (if ps_clear x n s then {((), s)} else {})" apply (rule set_eqI, rule iffI) apply (clarsimp simp: magnitudeCheck_def lookupAround2_char2
                         lookupAround2_None2 in_monad
                  split: option.split_asm) apply (drule(1) range_convergence1) apply (erule(1) ps_clearI) apply simp apply (erule is_aligned_get_word_bits) apply (drule(1) range_convergence2) apply (erule(1) ps_clearI) apply (simp add: linorder_not_less) apply (drule word_leq_le_minus_one[where x="2 ^ n" for n], simp) apply (drule word_l_diffs, simp) apply (simp add: field_simps) apply (simp add: power_overflow) apply (clarsimp split: if_split_asm) apply (erule(1) ps_clear_lookupAround2) apply simp apply (drule word_le_minus_one_leq[where x="y - x"]) apply (drule word_plus_mono_right[where x=x and y="y - x"]) apply (erule is_aligned_get_word_bits) apply (simp add: field_simps is_aligned_no_overflow) apply simp apply (simp add: field_simps) apply (simp add: magnitudeCheck_def return_def
                   iffD2[OF linorder_not_less] when_def
            split: option.split_asm) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<forall>z. x < z \<and> z \<le> y \<longrightarrow> ksPSpace s z = None; is_aligned x n; 1 < 2 ^ n; ksPSpace s x = Some v; x \<le> y; y - x < 2 ^ n\<rbrakk> \<Longrightarrow> fst (magnitudeCheck x (snd (lookupAround2 y (ksPSpace s))) n s) = (if ps_clear x n s then {((), s)} else {}) proof (prove)
goal (2 subgoals):
 1. \<And>xa. \<lbrakk>\<forall>z. x < z \<and> z \<le> y \<longrightarrow> ksPSpace s z = None; is_aligned x n; 1 < 2 ^ n; ksPSpace s x = Some v; x \<le> y; y - x < 2 ^ n; xa \<in> fst (magnitudeCheck x (snd (lookupAround2 y (ksPSpace s))) n s)\<rbrakk> \<Longrightarrow> xa \<in> (if ps_clear x n s then {((), s)} else {})
 2. \<And>xa. \<lbrakk>\<forall>z. x < z \<and> z \<le> y \<longrightarrow> ksPSpace s z = None; is_aligned x n; 1 < 2 ^ n; ksPSpace s x = Some v; x \<le> y; y - x < 2 ^ n; xa \<in> (if ps_clear x n s then {((), s)} else {})\<rbrakk> \<Longrightarrow> xa \<in> fst (magnitudeCheck x (snd (lookupAround2 y (ksPSpace s))) n s) proof (prove)
goal (3 subgoals):
 1. \<lbrakk>\<forall>z. x < z \<and> z \<le> y \<longrightarrow> ksPSpace s z = None; is_aligned x n; 1 < 2 ^ n; ksPSpace s x = Some v; x \<le> y; y - x < 2 ^ n; \<forall>ya>y. ksPSpace s ya = None\<rbrakk> \<Longrightarrow> ps_clear x n s
 2. \<And>x2 ya. \<lbrakk>\<forall>z. x < z \<and> z \<le> y \<longrightarrow> ksPSpace s z = None; is_aligned x n; 1 < 2 ^ n; ksPSpace s x = Some v; x \<le> y; y - x < 2 ^ n; y < x2; \<forall>z. y < z \<and> z < x2 \<longrightarrow> ksPSpace s z = None; ksPSpace s x2 = Some ya; \<not> x2 - x < 2 ^ n\<rbrakk> \<Longrightarrow> ps_clear x n s
 3. \<And>xa. \<lbrakk>\<forall>z. x < z \<and> z \<le> y \<longrightarrow> ksPSpace s z = None; is_aligned x n; 1 < 2 ^ n; ksPSpace s x = Some v; x \<le> y; y - x < 2 ^ n; xa \<in> (if ps_clear x n s then {((), s)} else {})\<rbrakk> \<Longrightarrow> xa \<in> fst (magnitudeCheck x (snd (lookupAround2 y (ksPSpace s))) n s) proof (prove)
goal (3 subgoals):
 1. \<lbrakk>is_aligned x n; 1 < 2 ^ n; ksPSpace s x = Some v; x \<le> y; y - x < 2 ^ n; \<forall>ya>y. ksPSpace s ya = None; \<forall>z>x. ksPSpace s z = None\<rbrakk> \<Longrightarrow> ps_clear x n s
 2. \<And>x2 ya. \<lbrakk>\<forall>z. x < z \<and> z \<le> y \<longrightarrow> ksPSpace s z = None; is_aligned x n; 1 < 2 ^ n; ksPSpace s x = Some v; x \<le> y; y - x < 2 ^ n; y < x2; \<forall>z. y < z \<and> z < x2 \<longrightarrow> ksPSpace s z = None; ksPSpace s x2 = Some ya; \<not> x2 - x < 2 ^ n\<rbrakk> \<Longrightarrow> ps_clear x n s
 3. \<And>xa. \<lbrakk>\<forall>z. x < z \<and> z \<le> y \<longrightarrow> ksPSpace s z = None; is_aligned x n; 1 < 2 ^ n; ksPSpace s x = Some v; x \<le> y; y - x < 2 ^ n; xa \<in> (if ps_clear x n s then {((), s)} else {})\<rbrakk> \<Longrightarrow> xa \<in> fst (magnitudeCheck x (snd (lookupAround2 y (ksPSpace s))) n s) proof (prove)
goal (3 subgoals):
 1. \<And>xa. \<lbrakk>1 < 2 ^ n; ksPSpace s x = Some v; x \<le> y; y - x < 2 ^ n; \<forall>ya>y. ksPSpace s ya = None; \<forall>z>x. ksPSpace s z = None; x < xa; xa \<le> x + 2 ^ n - 1\<rbrakk> \<Longrightarrow> ksPSpace s xa = None
 2. \<And>x2 ya. \<lbrakk>\<forall>z. x < z \<and> z \<le> y \<longrightarrow> ksPSpace s z = None; is_aligned x n; 1 < 2 ^ n; ksPSpace s x = Some v; x \<le> y; y - x < 2 ^ n; y < x2; \<forall>z. y < z \<and> z < x2 \<longrightarrow> ksPSpace s z = None; ksPSpace s x2 = Some ya; \<not> x2 - x < 2 ^ n\<rbrakk> \<Longrightarrow> ps_clear x n s
 3. \<And>xa. \<lbrakk>\<forall>z. x < z \<and> z \<le> y \<longrightarrow> ksPSpace s z = None; is_aligned x n; 1 < 2 ^ n; ksPSpace s x = Some v; x \<le> y; y - x < 2 ^ n; xa \<in> (if ps_clear x n s then {((), s)} else {})\<rbrakk> \<Longrightarrow> xa \<in> fst (magnitudeCheck x (snd (lookupAround2 y (ksPSpace s))) n s) proof (prove)
goal (2 subgoals):
 1. \<And>x2 ya. \<lbrakk>\<forall>z. x < z \<and> z \<le> y \<longrightarrow> ksPSpace s z = None; is_aligned x n; 1 < 2 ^ n; ksPSpace s x = Some v; x \<le> y; y - x < 2 ^ n; y < x2; \<forall>z. y < z \<and> z < x2 \<longrightarrow> ksPSpace s z = None; ksPSpace s x2 = Some ya; \<not> x2 - x < 2 ^ n\<rbrakk> \<Longrightarrow> ps_clear x n s
 2. \<And>xa. \<lbrakk>\<forall>z. x < z \<and> z \<le> y \<longrightarrow> ksPSpace s z = None; is_aligned x n; 1 < 2 ^ n; ksPSpace s x = Some v; x \<le> y; y - x < 2 ^ n; xa \<in> (if ps_clear x n s then {((), s)} else {})\<rbrakk> \<Longrightarrow> xa \<in> fst (magnitudeCheck x (snd (lookupAround2 y (ksPSpace s))) n s) proof (prove)
goal (3 subgoals):
 1. \<And>x2 ya. \<lbrakk>\<forall>z. x < z \<and> z \<le> y \<longrightarrow> ksPSpace s z = None; 1 < 2 ^ n; ksPSpace s x = Some v; x \<le> y; y - x < 2 ^ n; y < x2; \<forall>z. y < z \<and> z < x2 \<longrightarrow> ksPSpace s z = None; ksPSpace s x2 = Some ya; \<not> x2 - x < 2 ^ n; is_aligned x n; n < LENGTH(32)\<rbrakk> \<Longrightarrow> ps_clear x n s
 2. \<And>x2 ya. \<lbrakk>\<forall>z. x < z \<and> z \<le> y \<longrightarrow> ksPSpace s z = None; 1 < 2 ^ n; ksPSpace s x = Some v; x \<le> y; y - x < 2 ^ n; y < x2; \<forall>z. y < z \<and> z < x2 \<longrightarrow> ksPSpace s z = None; ksPSpace s x2 = Some ya; \<not> x2 - x < 2 ^ n; x = 0; LENGTH(32) \<le> n\<rbrakk> \<Longrightarrow> ps_clear x n s
 3. \<And>xa. \<lbrakk>\<forall>z. x < z \<and> z \<le> y \<longrightarrow> ksPSpace s z = None; is_aligned x n; 1 < 2 ^ n; ksPSpace s x = Some v; x \<le> y; y - x < 2 ^ n; xa \<in> (if ps_clear x n s then {((), s)} else {})\<rbrakk> \<Longrightarrow> xa \<in> fst (magnitudeCheck x (snd (lookupAround2 y (ksPSpace s))) n s) proof (prove)
goal (3 subgoals):
 1. \<And>x2 ya. \<lbrakk>1 < 2 ^ n; ksPSpace s x = Some v; x \<le> y; y - x < 2 ^ n; y < x2; \<forall>z. y < z \<and> z < x2 \<longrightarrow> ksPSpace s z = None; ksPSpace s x2 = Some ya; \<not> x2 - x < 2 ^ n; is_aligned x n; n < LENGTH(32); \<forall>z. x < z \<and> z < x2 \<longrightarrow> ksPSpace s z = None\<rbrakk> \<Longrightarrow> ps_clear x n s
 2. \<And>x2 ya. \<lbrakk>\<forall>z. x < z \<and> z \<le> y \<longrightarrow> ksPSpace s z = None; 1 < 2 ^ n; ksPSpace s x = Some v; x \<le> y; y - x < 2 ^ n; y < x2; \<forall>z. y < z \<and> z < x2 \<longrightarrow> ksPSpace s z = None; ksPSpace s x2 = Some ya; \<not> x2 - x < 2 ^ n; x = 0; LENGTH(32) \<le> n\<rbrakk> \<Longrightarrow> ps_clear x n s
 3. \<And>xa. \<lbrakk>\<forall>z. x < z \<and> z \<le> y \<longrightarrow> ksPSpace s z = None; is_aligned x n; 1 < 2 ^ n; ksPSpace s x = Some v; x \<le> y; y - x < 2 ^ n; xa \<in> (if ps_clear x n s then {((), s)} else {})\<rbrakk> \<Longrightarrow> xa \<in> fst (magnitudeCheck x (snd (lookupAround2 y (ksPSpace s))) n s) proof (prove)
goal (3 subgoals):
 1. \<And>x2 ya xa. \<lbrakk>1 < 2 ^ n; ksPSpace s x = Some v; x \<le> y; y - x < 2 ^ n; y < x2; \<forall>z. y < z \<and> z < x2 \<longrightarrow> ksPSpace s z = None; ksPSpace s x2 = Some ya; \<not> x2 - x < 2 ^ n; n < LENGTH(32); \<forall>z. x < z \<and> z < x2 \<longrightarrow> ksPSpace s z = None; x < xa; xa \<le> x + 2 ^ n - 1\<rbrakk> \<Longrightarrow> ksPSpace s xa = None
 2. \<And>x2 ya. \<lbrakk>\<forall>z. x < z \<and> z \<le> y \<longrightarrow> ksPSpace s z = None; 1 < 2 ^ n; ksPSpace s x = Some v; x \<le> y; y - x < 2 ^ n; y < x2; \<forall>z. y < z \<and> z < x2 \<longrightarrow> ksPSpace s z = None; ksPSpace s x2 = Some ya; \<not> x2 - x < 2 ^ n; x = 0; LENGTH(32) \<le> n\<rbrakk> \<Longrightarrow> ps_clear x n s
 3. \<And>xa. \<lbrakk>\<forall>z. x < z \<and> z \<le> y \<longrightarrow> ksPSpace s z = None; is_aligned x n; 1 < 2 ^ n; ksPSpace s x = Some v; x \<le> y; y - x < 2 ^ n; xa \<in> (if ps_clear x n s then {((), s)} else {})\<rbrakk> \<Longrightarrow> xa \<in> fst (magnitudeCheck x (snd (lookupAround2 y (ksPSpace s))) n s) proof (prove)
goal (3 subgoals):
 1. \<And>x2 ya xa. \<lbrakk>1 < 2 ^ n; ksPSpace s x = Some v; x \<le> y; y - x < 2 ^ n; y < x2; \<forall>z. y < z \<and> z < x2 \<longrightarrow> ksPSpace s z = None; ksPSpace s x2 = Some ya; 2 ^ n \<le> x2 - x; n < 32; \<forall>z. x < z \<and> z < x2 \<longrightarrow> ksPSpace s z = None; x < xa; xa \<le> x + 2 ^ n - 1\<rbrakk> \<Longrightarrow> ksPSpace s xa = None
 2. \<And>x2 ya. \<lbrakk>\<forall>z. x < z \<and> z \<le> y \<longrightarrow> ksPSpace s z = None; 1 < 2 ^ n; ksPSpace s x = Some v; x \<le> y; y - x < 2 ^ n; y < x2; \<forall>z. y < z \<and> z < x2 \<longrightarrow> ksPSpace s z = None; ksPSpace s x2 = Some ya; \<not> x2 - x < 2 ^ n; x = 0; LENGTH(32) \<le> n\<rbrakk> \<Longrightarrow> ps_clear x n s
 3. \<And>xa. \<lbrakk>\<forall>z. x < z \<and> z \<le> y \<longrightarrow> ksPSpace s z = None; is_aligned x n; 1 < 2 ^ n; ksPSpace s x = Some v; x \<le> y; y - x < 2 ^ n; xa \<in> (if ps_clear x n s then {((), s)} else {})\<rbrakk> \<Longrightarrow> xa \<in> fst (magnitudeCheck x (snd (lookupAround2 y (ksPSpace s))) n s) proof (prove)
goal (3 subgoals):
 1. \<And>x2 ya xa. \<lbrakk>1 < 2 ^ n; ksPSpace s x = Some v; x \<le> y; y - x < 2 ^ n; y < x2; \<forall>z. y < z \<and> z < x2 \<longrightarrow> ksPSpace s z = None; ksPSpace s x2 = Some ya; n < 32; \<forall>z. x < z \<and> z < x2 \<longrightarrow> ksPSpace s z = None; x < xa; xa \<le> x + 2 ^ n - 1; 2 ^ n - 1 < x2 - x\<rbrakk> \<Longrightarrow> ksPSpace s xa = None
 2. \<And>x2 ya. \<lbrakk>\<forall>z. x < z \<and> z \<le> y \<longrightarrow> ksPSpace s z = None; 1 < 2 ^ n; ksPSpace s x = Some v; x \<le> y; y - x < 2 ^ n; y < x2; \<forall>z. y < z \<and> z < x2 \<longrightarrow> ksPSpace s z = None; ksPSpace s x2 = Some ya; \<not> x2 - x < 2 ^ n; x = 0; LENGTH(32) \<le> n\<rbrakk> \<Longrightarrow> ps_clear x n s
 3. \<And>xa. \<lbrakk>\<forall>z. x < z \<and> z \<le> y \<longrightarrow> ksPSpace s z = None; is_aligned x n; 1 < 2 ^ n; ksPSpace s x = Some v; x \<le> y; y - x < 2 ^ n; xa \<in> (if ps_clear x n s then {((), s)} else {})\<rbrakk> \<Longrightarrow> xa \<in> fst (magnitudeCheck x (snd (lookupAround2 y (ksPSpace s))) n s) proof (prove)
goal (3 subgoals):
 1. \<And>x2 ya xa. \<lbrakk>1 < 2 ^ n; ksPSpace s x = Some v; x \<le> y; y - x < 2 ^ n; y < x2; \<forall>z. y < z \<and> z < x2 \<longrightarrow> ksPSpace s z = None; ksPSpace s x2 = Some ya; n < 32; \<forall>z. x < z \<and> z < x2 \<longrightarrow> ksPSpace s z = None; x < xa; xa \<le> x + 2 ^ n - 1; 2 ^ n - 1 + x < x2\<rbrakk> \<Longrightarrow> ksPSpace s xa = None
 2. \<And>x2 ya. \<lbrakk>\<forall>z. x < z \<and> z \<le> y \<longrightarrow> ksPSpace s z = None; 1 < 2 ^ n; ksPSpace s x = Some v; x \<le> y; y - x < 2 ^ n; y < x2; \<forall>z. y < z \<and> z < x2 \<longrightarrow> ksPSpace s z = None; ksPSpace s x2 = Some ya; \<not> x2 - x < 2 ^ n; x = 0; LENGTH(32) \<le> n\<rbrakk> \<Longrightarrow> ps_clear x n s
 3. \<And>xa. \<lbrakk>\<forall>z. x < z \<and> z \<le> y \<longrightarrow> ksPSpace s z = None; is_aligned x n; 1 < 2 ^ n; ksPSpace s x = Some v; x \<le> y; y - x < 2 ^ n; xa \<in> (if ps_clear x n s then {((), s)} else {})\<rbrakk> \<Longrightarrow> xa \<in> fst (magnitudeCheck x (snd (lookupAround2 y (ksPSpace s))) n s) proof (prove)
goal (2 subgoals):
 1. \<And>x2 ya. \<lbrakk>\<forall>z. x < z \<and> z \<le> y \<longrightarrow> ksPSpace s z = None; 1 < 2 ^ n; ksPSpace s x = Some v; x \<le> y; y - x < 2 ^ n; y < x2; \<forall>z. y < z \<and> z < x2 \<longrightarrow> ksPSpace s z = None; ksPSpace s x2 = Some ya; \<not> x2 - x < 2 ^ n; x = 0; LENGTH(32) \<le> n\<rbrakk> \<Longrightarrow> ps_clear x n s
 2. \<And>xa. \<lbrakk>\<forall>z. x < z \<and> z \<le> y \<longrightarrow> ksPSpace s z = None; is_aligned x n; 1 < 2 ^ n; ksPSpace s x = Some v; x \<le> y; y - x < 2 ^ n; xa \<in> (if ps_clear x n s then {((), s)} else {})\<rbrakk> \<Longrightarrow> xa \<in> fst (magnitudeCheck x (snd (lookupAround2 y (ksPSpace s))) n s) proof (prove)
goal (1 subgoal):
 1. \<And>xa. \<lbrakk>\<forall>z. x < z \<and> z \<le> y \<longrightarrow> ksPSpace s z = None; is_aligned x n; 1 < 2 ^ n; ksPSpace s x = Some v; x \<le> y; y - x < 2 ^ n; xa \<in> (if ps_clear x n s then {((), s)} else {})\<rbrakk> \<Longrightarrow> xa \<in> fst (magnitudeCheck x (snd (lookupAround2 y (ksPSpace s))) n s) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<forall>z. x < z \<and> z \<le> y \<longrightarrow> ksPSpace s z = None; is_aligned x n; 1 < 2 ^ n; ksPSpace s x = Some v; x \<le> y; y - x < 2 ^ n; ps_clear x n s\<rbrakk> \<Longrightarrow> ((), s) \<in> fst (magnitudeCheck x (snd (lookupAround2 y (ksPSpace s))) n s) proof (prove)
goal (3 subgoals):
 1. \<lbrakk>\<forall>z. x < z \<and> z \<le> y \<longrightarrow> ksPSpace s z = None; is_aligned x n; 1 < 2 ^ n; ksPSpace s x = Some v; x \<le> y; y - x < 2 ^ n\<rbrakk> \<Longrightarrow> x \<le> y
 2. \<lbrakk>\<forall>z. x < z \<and> z \<le> y \<longrightarrow> ksPSpace s z = None; is_aligned x n; 1 < 2 ^ n; ksPSpace s x = Some v; x \<le> y; y - x < 2 ^ n\<rbrakk> \<Longrightarrow> y \<le> x + 2 ^ n - 1
 3. \<lbrakk>\<forall>z. x < z \<and> z \<le> y \<longrightarrow> ksPSpace s z = None; is_aligned x n; 1 < 2 ^ n; ksPSpace s x = Some v; x \<le> y; y - x < 2 ^ n; fst (lookupAround2 y (ksPSpace s)) = Some (x, v); case snd (lookupAround2 y (ksPSpace s)) of None \<Rightarrow> True | Some xa \<Rightarrow> 2 ^ n \<le> xa - x\<rbrakk> \<Longrightarrow> ((), s) \<in> fst (magnitudeCheck x (snd (lookupAround2 y (ksPSpace s))) n s) proof (prove)
goal (2 subgoals):
 1. \<lbrakk>\<forall>z. x < z \<and> z \<le> y \<longrightarrow> ksPSpace s z = None; is_aligned x n; 1 < 2 ^ n; ksPSpace s x = Some v; x \<le> y; y - x < 2 ^ n\<rbrakk> \<Longrightarrow> y \<le> x + 2 ^ n - 1
 2. \<lbrakk>\<forall>z. x < z \<and> z \<le> y \<longrightarrow> ksPSpace s z = None; is_aligned x n; 1 < 2 ^ n; ksPSpace s x = Some v; x \<le> y; y - x < 2 ^ n; fst (lookupAround2 y (ksPSpace s)) = Some (x, v); case snd (lookupAround2 y (ksPSpace s)) of None \<Rightarrow> True | Some xa \<Rightarrow> 2 ^ n \<le> xa - x\<rbrakk> \<Longrightarrow> ((), s) \<in> fst (magnitudeCheck x (snd (lookupAround2 y (ksPSpace s))) n s) proof (prove)
goal (2 subgoals):
 1. \<lbrakk>\<forall>z. x < z \<and> z \<le> y \<longrightarrow> ksPSpace s z = None; is_aligned x n; 1 < 2 ^ n; ksPSpace s x = Some v; x \<le> y; y - x \<le> 2 ^ n - 1\<rbrakk> \<Longrightarrow> y \<le> x + 2 ^ n - 1
 2. \<lbrakk>\<forall>z. x < z \<and> z \<le> y \<longrightarrow> ksPSpace s z = None; is_aligned x n; 1 < 2 ^ n; ksPSpace s x = Some v; x \<le> y; y - x < 2 ^ n; fst (lookupAround2 y (ksPSpace s)) = Some (x, v); case snd (lookupAround2 y (ksPSpace s)) of None \<Rightarrow> True | Some xa \<Rightarrow> 2 ^ n \<le> xa - x\<rbrakk> \<Longrightarrow> ((), s) \<in> fst (magnitudeCheck x (snd (lookupAround2 y (ksPSpace s))) n s) proof (prove)
goal (3 subgoals):
 1. \<lbrakk>\<forall>z. x < z \<and> z \<le> y \<longrightarrow> ksPSpace s z = None; is_aligned x n; 1 < 2 ^ n; ksPSpace s x = Some v; x \<le> y\<rbrakk> \<Longrightarrow> x \<le> x + (2 ^ n - 1)
 2. \<lbrakk>\<forall>z. x < z \<and> z \<le> y \<longrightarrow> ksPSpace s z = None; is_aligned x n; 1 < 2 ^ n; ksPSpace s x = Some v; x \<le> y; x + (y - x) \<le> x + (2 ^ n - 1)\<rbrakk> \<Longrightarrow> y \<le> x + 2 ^ n - 1
 3. \<lbrakk>\<forall>z. x < z \<and> z \<le> y \<longrightarrow> ksPSpace s z = None; is_aligned x n; 1 < 2 ^ n; ksPSpace s x = Some v; x \<le> y; y - x < 2 ^ n; fst (lookupAround2 y (ksPSpace s)) = Some (x, v); case snd (lookupAround2 y (ksPSpace s)) of None \<Rightarrow> True | Some xa \<Rightarrow> 2 ^ n \<le> xa - x\<rbrakk> \<Longrightarrow> ((), s) \<in> fst (magnitudeCheck x (snd (lookupAround2 y (ksPSpace s))) n s) proof (prove)
goal (4 subgoals):
 1. \<lbrakk>\<forall>z. x < z \<and> z \<le> y \<longrightarrow> ksPSpace s z = None; 1 < 2 ^ n; ksPSpace s x = Some v; x \<le> y; is_aligned x n; n < LENGTH(32)\<rbrakk> \<Longrightarrow> x \<le> x + (2 ^ n - 1)
 2. \<lbrakk>\<forall>z. x < z \<and> z \<le> y \<longrightarrow> ksPSpace s z = None; 1 < 2 ^ n; ksPSpace s x = Some v; x \<le> y; x = 0; LENGTH(32) \<le> n\<rbrakk> \<Longrightarrow> x \<le> x + (2 ^ n - 1)
 3. \<lbrakk>\<forall>z. x < z \<and> z \<le> y \<longrightarrow> ksPSpace s z = None; is_aligned x n; 1 < 2 ^ n; ksPSpace s x = Some v; x \<le> y; x + (y - x) \<le> x + (2 ^ n - 1)\<rbrakk> \<Longrightarrow> y \<le> x + 2 ^ n - 1
 4. \<lbrakk>\<forall>z. x < z \<and> z \<le> y \<longrightarrow> ksPSpace s z = None; is_aligned x n; 1 < 2 ^ n; ksPSpace s x = Some v; x \<le> y; y - x < 2 ^ n; fst (lookupAround2 y (ksPSpace s)) = Some (x, v); case snd (lookupAround2 y (ksPSpace s)) of None \<Rightarrow> True | Some xa \<Rightarrow> 2 ^ n \<le> xa - x\<rbrakk> \<Longrightarrow> ((), s) \<in> fst (magnitudeCheck x (snd (lookupAround2 y (ksPSpace s))) n s) proof (prove)
goal (3 subgoals):
 1. \<lbrakk>\<forall>z. x < z \<and> z \<le> y \<longrightarrow> ksPSpace s z = None; 1 < 2 ^ n; ksPSpace s x = Some v; x \<le> y; x = 0; LENGTH(32) \<le> n\<rbrakk> \<Longrightarrow> x \<le> x + (2 ^ n - 1)
 2. \<lbrakk>\<forall>z. x < z \<and> z \<le> y \<longrightarrow> ksPSpace s z = None; is_aligned x n; 1 < 2 ^ n; ksPSpace s x = Some v; x \<le> y; x + (y - x) \<le> x + (2 ^ n - 1)\<rbrakk> \<Longrightarrow> y \<le> x + 2 ^ n - 1
 3. \<lbrakk>\<forall>z. x < z \<and> z \<le> y \<longrightarrow> ksPSpace s z = None; is_aligned x n; 1 < 2 ^ n; ksPSpace s x = Some v; x \<le> y; y - x < 2 ^ n; fst (lookupAround2 y (ksPSpace s)) = Some (x, v); case snd (lookupAround2 y (ksPSpace s)) of None \<Rightarrow> True | Some xa \<Rightarrow> 2 ^ n \<le> xa - x\<rbrakk> \<Longrightarrow> ((), s) \<in> fst (magnitudeCheck x (snd (lookupAround2 y (ksPSpace s))) n s) proof (prove)
goal (2 subgoals):
 1. \<lbrakk>\<forall>z. x < z \<and> z \<le> y \<longrightarrow> ksPSpace s z = None; is_aligned x n; 1 < 2 ^ n; ksPSpace s x = Some v; x \<le> y; x + (y - x) \<le> x + (2 ^ n - 1)\<rbrakk> \<Longrightarrow> y \<le> x + 2 ^ n - 1
 2. \<lbrakk>\<forall>z. x < z \<and> z \<le> y \<longrightarrow> ksPSpace s z = None; is_aligned x n; 1 < 2 ^ n; ksPSpace s x = Some v; x \<le> y; y - x < 2 ^ n; fst (lookupAround2 y (ksPSpace s)) = Some (x, v); case snd (lookupAround2 y (ksPSpace s)) of None \<Rightarrow> True | Some xa \<Rightarrow> 2 ^ n \<le> xa - x\<rbrakk> \<Longrightarrow> ((), s) \<in> fst (magnitudeCheck x (snd (lookupAround2 y (ksPSpace s))) n s) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<forall>z. x < z \<and> z \<le> y \<longrightarrow> ksPSpace s z = None; is_aligned x n; 1 < 2 ^ n; ksPSpace s x = Some v; x \<le> y; y - x < 2 ^ n; fst (lookupAround2 y (ksPSpace s)) = Some (x, v); case snd (lookupAround2 y (ksPSpace s)) of None \<Rightarrow> True | Some xa \<Rightarrow> 2 ^ n \<le> xa - x\<rbrakk> \<Longrightarrow> ((), s) \<in> fst (magnitudeCheck x (snd (lookupAround2 y (ksPSpace s))) n s) proof (prove)
goal:
No subgoals!