theory Example_Valid_State

lemma valid_global_pd_mappings_s0[simp]:
  "valid_global_vspace_mappings s0_internal" apply (clarsimp simp: valid_global_vspace_mappings_def s0_internal_def arch_state0_def
                        obj_at_def kh0_def kh0_obj_def s0_ptr_defs valid_pd_kernel_mappings_def
                        valid_pde_kernel_mappings_def pde_mapping_bits_def mask_def) apply (rule conjI) apply force apply clarsimp apply (subgoal_tac "xa - 0xFFFFF \<le> ucast x << 20") apply (case_tac "ucast x << 20 > (0xE0000000::32 word)") apply (subgoal_tac "(0xE0100000::32 word) \<le> ucast x << 20") apply ((drule(1) order_trans_rules(23))+, force) apply (simp add: shiftl_t2n) apply (cut_tac p="0xE0000000::32 word" and n=20 and m=20 and q="0x100000 * ucast x" in word_plus_power_2_offset_le) apply (simp add: is_aligned_def) apply (simp add: is_aligned_def unat_word_ariths) apply (subst mod_mult_mult1[where c="2^20" and b="2^12", simplified]) apply simp apply simp apply simp apply simp apply simp apply (case_tac "ucast x << 20 < (0xE0000000::32 word)") apply (subgoal_tac "(0xE0000000::32 word) - 0x100000 \<ge> ucast x << 20") apply (subgoal_tac "0xFFFFF + (ucast x << 20) \<le> 0xDFFFFFFF") apply (drule_tac y="0xFFFFF + (ucast x << 20)" and z="0xDFFFFFFF::32 word" in order_trans_rules(23)) apply simp apply ((drule(1) order_trans_rules(23))+, force) apply (simp add: add.commute) apply (simp add: word_plus_mono_left[where x="0xFFFFF" and z="0xDFF00000", simplified]) apply (simp add: shiftl_t2n) apply (rule udvd_decr'[where K="0x100000" and q="0xE0000000" and ua=0, simplified]) apply simp apply (simp add: uint_word_ariths) apply (subst mod_mult_mult1[where c="2^20" and b="2^12", simplified]) apply simp apply simp apply simp apply (erule notE) apply (cut_tac x="ucast x::32 word" and n=20 in shiftl_shiftr_id) apply simp apply (simp add: ucast_less[where 'b=12, simplified]) apply simp apply (rule ucast_up_inj[where 'b=32]) apply simp apply simp apply (drule_tac c="0xFFFFF + (ucast x << 20)" and d="0xFFFFF" and b="0xFFFFF" in word_sub_mono) apply simp apply (rule word_sub_le) apply (rule order_trans_rules(23)[rotated], assumption) apply simp apply (simp add: add.commute) apply (rule no_plus_overflow_neg) apply simp apply (drule_tac x="ucast x << 20" in order_trans_rules(23), assumption) apply (simp add: le_less_trans) apply simp done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. valid_global_vspace_mappings s0_internal proof (prove)
goal (1 subgoal):
 1. \<And>x. (x = 0xE00 \<longrightarrow> (\<exists>use. ((\<exists>x\<ge>0xE0000000. x \<le> 0xE00FFFFF) \<longrightarrow> ArmVSpaceKernelWindow = use) \<and> (use = ArmVSpaceKernelWindow \<or> use = ArmVSpaceDeviceWindow))) \<and> (x \<noteq> 0xE00 \<longrightarrow> (\<forall>x\<in>{UCAST(12 \<rightarrow> 32) x << 20..0xFFFFF + (UCAST(12 \<rightarrow> 32) x << 20)}. 0xE0000000 \<le> x \<longrightarrow> \<not> x \<le> 0xE00FFFFF)) proof (prove)
goal (2 subgoals):
 1. \<And>x. x = 0xE00 \<longrightarrow> (\<exists>use. ((\<exists>x\<ge>0xE0000000. x \<le> 0xE00FFFFF) \<longrightarrow> ArmVSpaceKernelWindow = use) \<and> (use = ArmVSpaceKernelWindow \<or> use = ArmVSpaceDeviceWindow))
 2. \<And>x. x \<noteq> 0xE00 \<longrightarrow> (\<forall>x\<in>{UCAST(12 \<rightarrow> 32) x << 20..0xFFFFF + (UCAST(12 \<rightarrow> 32) x << 20)}. 0xE0000000 \<le> x \<longrightarrow> \<not> x \<le> 0xE00FFFFF) proof (prove)
goal (1 subgoal):
 1. \<And>x. x \<noteq> 0xE00 \<longrightarrow> (\<forall>x\<in>{UCAST(12 \<rightarrow> 32) x << 20..0xFFFFF + (UCAST(12 \<rightarrow> 32) x << 20)}. 0xE0000000 \<le> x \<longrightarrow> \<not> x \<le> 0xE00FFFFF) proof (prove)
goal (1 subgoal):
 1. \<And>x xa. \<lbrakk>x \<noteq> 0xE00; 0xE0000000 \<le> xa; xa \<le> 0xE00FFFFF; UCAST(12 \<rightarrow> 32) x << 20 \<le> xa; xa \<le> 0xFFFFF + (UCAST(12 \<rightarrow> 32) x << 20)\<rbrakk> \<Longrightarrow> False proof (prove)
goal (2 subgoals):
 1. \<And>x xa. \<lbrakk>x \<noteq> 0xE00; 0xE0000000 \<le> xa; xa \<le> 0xE00FFFFF; UCAST(12 \<rightarrow> 32) x << 20 \<le> xa; xa \<le> 0xFFFFF + (UCAST(12 \<rightarrow> 32) x << 20); xa - 0xFFFFF \<le> UCAST(12 \<rightarrow> 32) x << 20\<rbrakk> \<Longrightarrow> False
 2. \<And>x xa. \<lbrakk>x \<noteq> 0xE00; 0xE0000000 \<le> xa; xa \<le> 0xE00FFFFF; UCAST(12 \<rightarrow> 32) x << 20 \<le> xa; xa \<le> 0xFFFFF + (UCAST(12 \<rightarrow> 32) x << 20)\<rbrakk> \<Longrightarrow> xa - 0xFFFFF \<le> UCAST(12 \<rightarrow> 32) x << 20 proof (prove)
goal (3 subgoals):
 1. \<And>x xa. \<lbrakk>x \<noteq> 0xE00; 0xE0000000 \<le> xa; xa \<le> 0xE00FFFFF; UCAST(12 \<rightarrow> 32) x << 20 \<le> xa; xa \<le> 0xFFFFF + (UCAST(12 \<rightarrow> 32) x << 20); xa - 0xFFFFF \<le> UCAST(12 \<rightarrow> 32) x << 20; 0xE0000000 < UCAST(12 \<rightarrow> 32) x << 20\<rbrakk> \<Longrightarrow> False
 2. \<And>x xa. \<lbrakk>x \<noteq> 0xE00; 0xE0000000 \<le> xa; xa \<le> 0xE00FFFFF; UCAST(12 \<rightarrow> 32) x << 20 \<le> xa; xa \<le> 0xFFFFF + (UCAST(12 \<rightarrow> 32) x << 20); xa - 0xFFFFF \<le> UCAST(12 \<rightarrow> 32) x << 20; \<not> 0xE0000000 < UCAST(12 \<rightarrow> 32) x << 20\<rbrakk> \<Longrightarrow> False
 3. \<And>x xa. \<lbrakk>x \<noteq> 0xE00; 0xE0000000 \<le> xa; xa \<le> 0xE00FFFFF; UCAST(12 \<rightarrow> 32) x << 20 \<le> xa; xa \<le> 0xFFFFF + (UCAST(12 \<rightarrow> 32) x << 20)\<rbrakk> \<Longrightarrow> xa - 0xFFFFF \<le> UCAST(12 \<rightarrow> 32) x << 20 proof (prove)
goal (4 subgoals):
 1. \<And>x xa. \<lbrakk>x \<noteq> 0xE00; 0xE0000000 \<le> xa; xa \<le> 0xE00FFFFF; UCAST(12 \<rightarrow> 32) x << 20 \<le> xa; xa \<le> 0xFFFFF + (UCAST(12 \<rightarrow> 32) x << 20); xa - 0xFFFFF \<le> UCAST(12 \<rightarrow> 32) x << 20; 0xE0000000 < UCAST(12 \<rightarrow> 32) x << 20; 0xE0100000 \<le> UCAST(12 \<rightarrow> 32) x << 20\<rbrakk> \<Longrightarrow> False
 2. \<And>x xa. \<lbrakk>x \<noteq> 0xE00; 0xE0000000 \<le> xa; xa \<le> 0xE00FFFFF; UCAST(12 \<rightarrow> 32) x << 20 \<le> xa; xa \<le> 0xFFFFF + (UCAST(12 \<rightarrow> 32) x << 20); xa - 0xFFFFF \<le> UCAST(12 \<rightarrow> 32) x << 20; 0xE0000000 < UCAST(12 \<rightarrow> 32) x << 20\<rbrakk> \<Longrightarrow> 0xE0100000 \<le> UCAST(12 \<rightarrow> 32) x << 20
 3. \<And>x xa. \<lbrakk>x \<noteq> 0xE00; 0xE0000000 \<le> xa; xa \<le> 0xE00FFFFF; UCAST(12 \<rightarrow> 32) x << 20 \<le> xa; xa \<le> 0xFFFFF + (UCAST(12 \<rightarrow> 32) x << 20); xa - 0xFFFFF \<le> UCAST(12 \<rightarrow> 32) x << 20; \<not> 0xE0000000 < UCAST(12 \<rightarrow> 32) x << 20\<rbrakk> \<Longrightarrow> False
 4. \<And>x xa. \<lbrakk>x \<noteq> 0xE00; 0xE0000000 \<le> xa; xa \<le> 0xE00FFFFF; UCAST(12 \<rightarrow> 32) x << 20 \<le> xa; xa \<le> 0xFFFFF + (UCAST(12 \<rightarrow> 32) x << 20)\<rbrakk> \<Longrightarrow> xa - 0xFFFFF \<le> UCAST(12 \<rightarrow> 32) x << 20 proof (prove)
goal (3 subgoals):
 1. \<And>x xa. \<lbrakk>x \<noteq> 0xE00; 0xE0000000 \<le> xa; xa \<le> 0xE00FFFFF; UCAST(12 \<rightarrow> 32) x << 20 \<le> xa; xa \<le> 0xFFFFF + (UCAST(12 \<rightarrow> 32) x << 20); xa - 0xFFFFF \<le> UCAST(12 \<rightarrow> 32) x << 20; 0xE0000000 < UCAST(12 \<rightarrow> 32) x << 20\<rbrakk> \<Longrightarrow> 0xE0100000 \<le> UCAST(12 \<rightarrow> 32) x << 20
 2. \<And>x xa. \<lbrakk>x \<noteq> 0xE00; 0xE0000000 \<le> xa; xa \<le> 0xE00FFFFF; UCAST(12 \<rightarrow> 32) x << 20 \<le> xa; xa \<le> 0xFFFFF + (UCAST(12 \<rightarrow> 32) x << 20); xa - 0xFFFFF \<le> UCAST(12 \<rightarrow> 32) x << 20; \<not> 0xE0000000 < UCAST(12 \<rightarrow> 32) x << 20\<rbrakk> \<Longrightarrow> False
 3. \<And>x xa. \<lbrakk>x \<noteq> 0xE00; 0xE0000000 \<le> xa; xa \<le> 0xE00FFFFF; UCAST(12 \<rightarrow> 32) x << 20 \<le> xa; xa \<le> 0xFFFFF + (UCAST(12 \<rightarrow> 32) x << 20)\<rbrakk> \<Longrightarrow> xa - 0xFFFFF \<le> UCAST(12 \<rightarrow> 32) x << 20 proof (prove)
goal (3 subgoals):
 1. \<And>x xa. \<lbrakk>x \<noteq> 0xE00; 0xE0000000 \<le> xa; xa \<le> 0xE00FFFFF; 0x100000 * UCAST(12 \<rightarrow> 32) x \<le> xa; xa \<le> 0xFFFFF + 0x100000 * UCAST(12 \<rightarrow> 32) x; xa - 0xFFFFF \<le> 0x100000 * UCAST(12 \<rightarrow> 32) x; 0xE0000000 < 0x100000 * UCAST(12 \<rightarrow> 32) x\<rbrakk> \<Longrightarrow> 0xE0100000 \<le> 0x100000 * UCAST(12 \<rightarrow> 32) x
 2. \<And>x xa. \<lbrakk>x \<noteq> 0xE00; 0xE0000000 \<le> xa; xa \<le> 0xE00FFFFF; UCAST(12 \<rightarrow> 32) x << 20 \<le> xa; xa \<le> 0xFFFFF + (UCAST(12 \<rightarrow> 32) x << 20); xa - 0xFFFFF \<le> UCAST(12 \<rightarrow> 32) x << 20; \<not> 0xE0000000 < UCAST(12 \<rightarrow> 32) x << 20\<rbrakk> \<Longrightarrow> False
 3. \<And>x xa. \<lbrakk>x \<noteq> 0xE00; 0xE0000000 \<le> xa; xa \<le> 0xE00FFFFF; UCAST(12 \<rightarrow> 32) x << 20 \<le> xa; xa \<le> 0xFFFFF + (UCAST(12 \<rightarrow> 32) x << 20)\<rbrakk> \<Longrightarrow> xa - 0xFFFFF \<le> UCAST(12 \<rightarrow> 32) x << 20 proof (prove)
goal (8 subgoals):
 1. \<And>x xa. \<lbrakk>x \<noteq> 0xE00; 0xE0000000 \<le> xa; xa \<le> 0xE00FFFFF; 0x100000 * UCAST(12 \<rightarrow> 32) x \<le> xa; xa \<le> 0xFFFFF + 0x100000 * UCAST(12 \<rightarrow> 32) x; xa - 0xFFFFF \<le> 0x100000 * UCAST(12 \<rightarrow> 32) x; 0xE0000000 < 0x100000 * UCAST(12 \<rightarrow> 32) x\<rbrakk> \<Longrightarrow> is_aligned 0xE0000000 20
 2. \<And>x xa. \<lbrakk>x \<noteq> 0xE00; 0xE0000000 \<le> xa; xa \<le> 0xE00FFFFF; 0x100000 * UCAST(12 \<rightarrow> 32) x \<le> xa; xa \<le> 0xFFFFF + 0x100000 * UCAST(12 \<rightarrow> 32) x; xa - 0xFFFFF \<le> 0x100000 * UCAST(12 \<rightarrow> 32) x; 0xE0000000 < 0x100000 * UCAST(12 \<rightarrow> 32) x\<rbrakk> \<Longrightarrow> is_aligned (0x100000 * UCAST(12 \<rightarrow> 32) x) 20
 3. \<And>x xa. \<lbrakk>x \<noteq> 0xE00; 0xE0000000 \<le> xa; xa \<le> 0xE00FFFFF; 0x100000 * UCAST(12 \<rightarrow> 32) x \<le> xa; xa \<le> 0xFFFFF + 0x100000 * UCAST(12 \<rightarrow> 32) x; xa - 0xFFFFF \<le> 0x100000 * UCAST(12 \<rightarrow> 32) x; 0xE0000000 < 0x100000 * UCAST(12 \<rightarrow> 32) x\<rbrakk> \<Longrightarrow> 0xE0000000 < 0x100000 * UCAST(12 \<rightarrow> 32) x
 4. \<And>x xa. \<lbrakk>x \<noteq> 0xE00; 0xE0000000 \<le> xa; xa \<le> 0xE00FFFFF; 0x100000 * UCAST(12 \<rightarrow> 32) x \<le> xa; xa \<le> 0xFFFFF + 0x100000 * UCAST(12 \<rightarrow> 32) x; xa - 0xFFFFF \<le> 0x100000 * UCAST(12 \<rightarrow> 32) x; 0xE0000000 < 0x100000 * UCAST(12 \<rightarrow> 32) x\<rbrakk> \<Longrightarrow> 20 \<le> 20
 5. \<And>x xa. \<lbrakk>x \<noteq> 0xE00; 0xE0000000 \<le> xa; xa \<le> 0xE00FFFFF; 0x100000 * UCAST(12 \<rightarrow> 32) x \<le> xa; xa \<le> 0xFFFFF + 0x100000 * UCAST(12 \<rightarrow> 32) x; xa - 0xFFFFF \<le> 0x100000 * UCAST(12 \<rightarrow> 32) x; 0xE0000000 < 0x100000 * UCAST(12 \<rightarrow> 32) x\<rbrakk> \<Longrightarrow> 20 < LENGTH(32)
 6. \<And>x xa. \<lbrakk>x \<noteq> 0xE00; 0xE0000000 \<le> xa; xa \<le> 0xE00FFFFF; 0x100000 * UCAST(12 \<rightarrow> 32) x \<le> xa; xa \<le> 0xFFFFF + 0x100000 * UCAST(12 \<rightarrow> 32) x; xa - 0xFFFFF \<le> 0x100000 * UCAST(12 \<rightarrow> 32) x; 0xE0000000 < 0x100000 * UCAST(12 \<rightarrow> 32) x; 0xE0000000 + 2 ^ 20 \<le> 0x100000 * UCAST(12 \<rightarrow> 32) x\<rbrakk> \<Longrightarrow> 0xE0100000 \<le> 0x100000 * UCAST(12 \<rightarrow> 32) x
 7. \<And>x xa. \<lbrakk>x \<noteq> 0xE00; 0xE0000000 \<le> xa; xa \<le> 0xE00FFFFF; UCAST(12 \<rightarrow> 32) x << 20 \<le> xa; xa \<le> 0xFFFFF + (UCAST(12 \<rightarrow> 32) x << 20); xa - 0xFFFFF \<le> UCAST(12 \<rightarrow> 32) x << 20; \<not> 0xE0000000 < UCAST(12 \<rightarrow> 32) x << 20\<rbrakk> \<Longrightarrow> False
 8. \<And>x xa. \<lbrakk>x \<noteq> 0xE00; 0xE0000000 \<le> xa; xa \<le> 0xE00FFFFF; UCAST(12 \<rightarrow> 32) x << 20 \<le> xa; xa \<le> 0xFFFFF + (UCAST(12 \<rightarrow> 32) x << 20)\<rbrakk> \<Longrightarrow> xa - 0xFFFFF \<le> UCAST(12 \<rightarrow> 32) x << 20 proof (prove)
goal (7 subgoals):
 1. \<And>x xa. \<lbrakk>x \<noteq> 0xE00; 0xE0000000 \<le> xa; xa \<le> 0xE00FFFFF; 0x100000 * UCAST(12 \<rightarrow> 32) x \<le> xa; xa \<le> 0xFFFFF + 0x100000 * UCAST(12 \<rightarrow> 32) x; xa - 0xFFFFF \<le> 0x100000 * UCAST(12 \<rightarrow> 32) x; 0xE0000000 < 0x100000 * UCAST(12 \<rightarrow> 32) x\<rbrakk> \<Longrightarrow> is_aligned (0x100000 * UCAST(12 \<rightarrow> 32) x) 20
 2. \<And>x xa. \<lbrakk>x \<noteq> 0xE00; 0xE0000000 \<le> xa; xa \<le> 0xE00FFFFF; 0x100000 * UCAST(12 \<rightarrow> 32) x \<le> xa; xa \<le> 0xFFFFF + 0x100000 * UCAST(12 \<rightarrow> 32) x; xa - 0xFFFFF \<le> 0x100000 * UCAST(12 \<rightarrow> 32) x; 0xE0000000 < 0x100000 * UCAST(12 \<rightarrow> 32) x\<rbrakk> \<Longrightarrow> 0xE0000000 < 0x100000 * UCAST(12 \<rightarrow> 32) x
 3. \<And>x xa. \<lbrakk>x \<noteq> 0xE00; 0xE0000000 \<le> xa; xa \<le> 0xE00FFFFF; 0x100000 * UCAST(12 \<rightarrow> 32) x \<le> xa; xa \<le> 0xFFFFF + 0x100000 * UCAST(12 \<rightarrow> 32) x; xa - 0xFFFFF \<le> 0x100000 * UCAST(12 \<rightarrow> 32) x; 0xE0000000 < 0x100000 * UCAST(12 \<rightarrow> 32) x\<rbrakk> \<Longrightarrow> 20 \<le> 20
 4. \<And>x xa. \<lbrakk>x \<noteq> 0xE00; 0xE0000000 \<le> xa; xa \<le> 0xE00FFFFF; 0x100000 * UCAST(12 \<rightarrow> 32) x \<le> xa; xa \<le> 0xFFFFF + 0x100000 * UCAST(12 \<rightarrow> 32) x; xa - 0xFFFFF \<le> 0x100000 * UCAST(12 \<rightarrow> 32) x; 0xE0000000 < 0x100000 * UCAST(12 \<rightarrow> 32) x\<rbrakk> \<Longrightarrow> 20 < LENGTH(32)
 5. \<And>x xa. \<lbrakk>x \<noteq> 0xE00; 0xE0000000 \<le> xa; xa \<le> 0xE00FFFFF; 0x100000 * UCAST(12 \<rightarrow> 32) x \<le> xa; xa \<le> 0xFFFFF + 0x100000 * UCAST(12 \<rightarrow> 32) x; xa - 0xFFFFF \<le> 0x100000 * UCAST(12 \<rightarrow> 32) x; 0xE0000000 < 0x100000 * UCAST(12 \<rightarrow> 32) x; 0xE0000000 + 2 ^ 20 \<le> 0x100000 * UCAST(12 \<rightarrow> 32) x\<rbrakk> \<Longrightarrow> 0xE0100000 \<le> 0x100000 * UCAST(12 \<rightarrow> 32) x
 6. \<And>x xa. \<lbrakk>x \<noteq> 0xE00; 0xE0000000 \<le> xa; xa \<le> 0xE00FFFFF; UCAST(12 \<rightarrow> 32) x << 20 \<le> xa; xa \<le> 0xFFFFF + (UCAST(12 \<rightarrow> 32) x << 20); xa - 0xFFFFF \<le> UCAST(12 \<rightarrow> 32) x << 20; \<not> 0xE0000000 < UCAST(12 \<rightarrow> 32) x << 20\<rbrakk> \<Longrightarrow> False
 7. \<And>x xa. \<lbrakk>x \<noteq> 0xE00; 0xE0000000 \<le> xa; xa \<le> 0xE00FFFFF; UCAST(12 \<rightarrow> 32) x << 20 \<le> xa; xa \<le> 0xFFFFF + (UCAST(12 \<rightarrow> 32) x << 20)\<rbrakk> \<Longrightarrow> xa - 0xFFFFF \<le> UCAST(12 \<rightarrow> 32) x << 20 proof (prove)
goal (7 subgoals):
 1. \<And>x xa. \<lbrakk>x \<noteq> 0xE00; 0xE0000000 \<le> xa; xa \<le> 0xE00FFFFF; 0x100000 * UCAST(12 \<rightarrow> 32) x \<le> xa; xa \<le> 0xFFFFF + 0x100000 * UCAST(12 \<rightarrow> 32) x; xa - 0xFFFFF \<le> 0x100000 * UCAST(12 \<rightarrow> 32) x; 0xE0000000 < 0x100000 * UCAST(12 \<rightarrow> 32) x\<rbrakk> \<Longrightarrow> 1048576 dvd 1048576 * unat (UCAST(12 \<rightarrow> 32) x) mod 4294967296
 2. \<And>x xa. \<lbrakk>x \<noteq> 0xE00; 0xE0000000 \<le> xa; xa \<le> 0xE00FFFFF; 0x100000 * UCAST(12 \<rightarrow> 32) x \<le> xa; xa \<le> 0xFFFFF + 0x100000 * UCAST(12 \<rightarrow> 32) x; xa - 0xFFFFF \<le> 0x100000 * UCAST(12 \<rightarrow> 32) x; 0xE0000000 < 0x100000 * UCAST(12 \<rightarrow> 32) x\<rbrakk> \<Longrightarrow> 0xE0000000 < 0x100000 * UCAST(12 \<rightarrow> 32) x
 3. \<And>x xa. \<lbrakk>x \<noteq> 0xE00; 0xE0000000 \<le> xa; xa \<le> 0xE00FFFFF; 0x100000 * UCAST(12 \<rightarrow> 32) x \<le> xa; xa \<le> 0xFFFFF + 0x100000 * UCAST(12 \<rightarrow> 32) x; xa - 0xFFFFF \<le> 0x100000 * UCAST(12 \<rightarrow> 32) x; 0xE0000000 < 0x100000 * UCAST(12 \<rightarrow> 32) x\<rbrakk> \<Longrightarrow> 20 \<le> 20
 4. \<And>x xa. \<lbrakk>x \<noteq> 0xE00; 0xE0000000 \<le> xa; xa \<le> 0xE00FFFFF; 0x100000 * UCAST(12 \<rightarrow> 32) x \<le> xa; xa \<le> 0xFFFFF + 0x100000 * UCAST(12 \<rightarrow> 32) x; xa - 0xFFFFF \<le> 0x100000 * UCAST(12 \<rightarrow> 32) x; 0xE0000000 < 0x100000 * UCAST(12 \<rightarrow> 32) x\<rbrakk> \<Longrightarrow> 20 < LENGTH(32)
 5. \<And>x xa. \<lbrakk>x \<noteq> 0xE00; 0xE0000000 \<le> xa; xa \<le> 0xE00FFFFF; 0x100000 * UCAST(12 \<rightarrow> 32) x \<le> xa; xa \<le> 0xFFFFF + 0x100000 * UCAST(12 \<rightarrow> 32) x; xa - 0xFFFFF \<le> 0x100000 * UCAST(12 \<rightarrow> 32) x; 0xE0000000 < 0x100000 * UCAST(12 \<rightarrow> 32) x; 0xE0000000 + 2 ^ 20 \<le> 0x100000 * UCAST(12 \<rightarrow> 32) x\<rbrakk> \<Longrightarrow> 0xE0100000 \<le> 0x100000 * UCAST(12 \<rightarrow> 32) x
 6. \<And>x xa. \<lbrakk>x \<noteq> 0xE00; 0xE0000000 \<le> xa; xa \<le> 0xE00FFFFF; UCAST(12 \<rightarrow> 32) x << 20 \<le> xa; xa \<le> 0xFFFFF + (UCAST(12 \<rightarrow> 32) x << 20); xa - 0xFFFFF \<le> UCAST(12 \<rightarrow> 32) x << 20; \<not> 0xE0000000 < UCAST(12 \<rightarrow> 32) x << 20\<rbrakk> \<Longrightarrow> False
 7. \<And>x xa. \<lbrakk>x \<noteq> 0xE00; 0xE0000000 \<le> xa; xa \<le> 0xE00FFFFF; UCAST(12 \<rightarrow> 32) x << 20 \<le> xa; xa \<le> 0xFFFFF + (UCAST(12 \<rightarrow> 32) x << 20)\<rbrakk> \<Longrightarrow> xa - 0xFFFFF \<le> UCAST(12 \<rightarrow> 32) x << 20 proof (prove)
goal (7 subgoals):
 1. \<And>x xa. \<lbrakk>x \<noteq> 0xE00; 0xE0000000 \<le> xa; xa \<le> 0xE00FFFFF; 0x100000 * UCAST(12 \<rightarrow> 32) x \<le> xa; xa \<le> 0xFFFFF + 0x100000 * UCAST(12 \<rightarrow> 32) x; xa - 0xFFFFF \<le> 0x100000 * UCAST(12 \<rightarrow> 32) x; 0xE0000000 < 0x100000 * UCAST(12 \<rightarrow> 32) x\<rbrakk> \<Longrightarrow> 1048576 dvd 1048576 * (unat (UCAST(12 \<rightarrow> 32) x) mod 4096)
 2. \<And>x xa. \<lbrakk>x \<noteq> 0xE00; 0xE0000000 \<le> xa; xa \<le> 0xE00FFFFF; 0x100000 * UCAST(12 \<rightarrow> 32) x \<le> xa; xa \<le> 0xFFFFF + 0x100000 * UCAST(12 \<rightarrow> 32) x; xa - 0xFFFFF \<le> 0x100000 * UCAST(12 \<rightarrow> 32) x; 0xE0000000 < 0x100000 * UCAST(12 \<rightarrow> 32) x\<rbrakk> \<Longrightarrow> 0xE0000000 < 0x100000 * UCAST(12 \<rightarrow> 32) x
 3. \<And>x xa. \<lbrakk>x \<noteq> 0xE00; 0xE0000000 \<le> xa; xa \<le> 0xE00FFFFF; 0x100000 * UCAST(12 \<rightarrow> 32) x \<le> xa; xa \<le> 0xFFFFF + 0x100000 * UCAST(12 \<rightarrow> 32) x; xa - 0xFFFFF \<le> 0x100000 * UCAST(12 \<rightarrow> 32) x; 0xE0000000 < 0x100000 * UCAST(12 \<rightarrow> 32) x\<rbrakk> \<Longrightarrow> 20 \<le> 20
 4. \<And>x xa. \<lbrakk>x \<noteq> 0xE00; 0xE0000000 \<le> xa; xa \<le> 0xE00FFFFF; 0x100000 * UCAST(12 \<rightarrow> 32) x \<le> xa; xa \<le> 0xFFFFF + 0x100000 * UCAST(12 \<rightarrow> 32) x; xa - 0xFFFFF \<le> 0x100000 * UCAST(12 \<rightarrow> 32) x; 0xE0000000 < 0x100000 * UCAST(12 \<rightarrow> 32) x\<rbrakk> \<Longrightarrow> 20 < LENGTH(32)
 5. \<And>x xa. \<lbrakk>x \<noteq> 0xE00; 0xE0000000 \<le> xa; xa \<le> 0xE00FFFFF; 0x100000 * UCAST(12 \<rightarrow> 32) x \<le> xa; xa \<le> 0xFFFFF + 0x100000 * UCAST(12 \<rightarrow> 32) x; xa - 0xFFFFF \<le> 0x100000 * UCAST(12 \<rightarrow> 32) x; 0xE0000000 < 0x100000 * UCAST(12 \<rightarrow> 32) x; 0xE0000000 + 2 ^ 20 \<le> 0x100000 * UCAST(12 \<rightarrow> 32) x\<rbrakk> \<Longrightarrow> 0xE0100000 \<le> 0x100000 * UCAST(12 \<rightarrow> 32) x
 6. \<And>x xa. \<lbrakk>x \<noteq> 0xE00; 0xE0000000 \<le> xa; xa \<le> 0xE00FFFFF; UCAST(12 \<rightarrow> 32) x << 20 \<le> xa; xa \<le> 0xFFFFF + (UCAST(12 \<rightarrow> 32) x << 20); xa - 0xFFFFF \<le> UCAST(12 \<rightarrow> 32) x << 20; \<not> 0xE0000000 < UCAST(12 \<rightarrow> 32) x << 20\<rbrakk> \<Longrightarrow> False
 7. \<And>x xa. \<lbrakk>x \<noteq> 0xE00; 0xE0000000 \<le> xa; xa \<le> 0xE00FFFFF; UCAST(12 \<rightarrow> 32) x << 20 \<le> xa; xa \<le> 0xFFFFF + (UCAST(12 \<rightarrow> 32) x << 20)\<rbrakk> \<Longrightarrow> xa - 0xFFFFF \<le> UCAST(12 \<rightarrow> 32) x << 20 proof (prove)
goal (6 subgoals):
 1. \<And>x xa. \<lbrakk>x \<noteq> 0xE00; 0xE0000000 \<le> xa; xa \<le> 0xE00FFFFF; 0x100000 * UCAST(12 \<rightarrow> 32) x \<le> xa; xa \<le> 0xFFFFF + 0x100000 * UCAST(12 \<rightarrow> 32) x; xa - 0xFFFFF \<le> 0x100000 * UCAST(12 \<rightarrow> 32) x; 0xE0000000 < 0x100000 * UCAST(12 \<rightarrow> 32) x\<rbrakk> \<Longrightarrow> 0xE0000000 < 0x100000 * UCAST(12 \<rightarrow> 32) x
 2. \<And>x xa. \<lbrakk>x \<noteq> 0xE00; 0xE0000000 \<le> xa; xa \<le> 0xE00FFFFF; 0x100000 * UCAST(12 \<rightarrow> 32) x \<le> xa; xa \<le> 0xFFFFF + 0x100000 * UCAST(12 \<rightarrow> 32) x; xa - 0xFFFFF \<le> 0x100000 * UCAST(12 \<rightarrow> 32) x; 0xE0000000 < 0x100000 * UCAST(12 \<rightarrow> 32) x\<rbrakk> \<Longrightarrow> 20 \<le> 20
 3. \<And>x xa. \<lbrakk>x \<noteq> 0xE00; 0xE0000000 \<le> xa; xa \<le> 0xE00FFFFF; 0x100000 * UCAST(12 \<rightarrow> 32) x \<le> xa; xa \<le> 0xFFFFF + 0x100000 * UCAST(12 \<rightarrow> 32) x; xa - 0xFFFFF \<le> 0x100000 * UCAST(12 \<rightarrow> 32) x; 0xE0000000 < 0x100000 * UCAST(12 \<rightarrow> 32) x\<rbrakk> \<Longrightarrow> 20 < LENGTH(32)
 4. \<And>x xa. \<lbrakk>x \<noteq> 0xE00; 0xE0000000 \<le> xa; xa \<le> 0xE00FFFFF; 0x100000 * UCAST(12 \<rightarrow> 32) x \<le> xa; xa \<le> 0xFFFFF + 0x100000 * UCAST(12 \<rightarrow> 32) x; xa - 0xFFFFF \<le> 0x100000 * UCAST(12 \<rightarrow> 32) x; 0xE0000000 < 0x100000 * UCAST(12 \<rightarrow> 32) x; 0xE0000000 + 2 ^ 20 \<le> 0x100000 * UCAST(12 \<rightarrow> 32) x\<rbrakk> \<Longrightarrow> 0xE0100000 \<le> 0x100000 * UCAST(12 \<rightarrow> 32) x
 5. \<And>x xa. \<lbrakk>x \<noteq> 0xE00; 0xE0000000 \<le> xa; xa \<le> 0xE00FFFFF; UCAST(12 \<rightarrow> 32) x << 20 \<le> xa; xa \<le> 0xFFFFF + (UCAST(12 \<rightarrow> 32) x << 20); xa - 0xFFFFF \<le> UCAST(12 \<rightarrow> 32) x << 20; \<not> 0xE0000000 < UCAST(12 \<rightarrow> 32) x << 20\<rbrakk> \<Longrightarrow> False
 6. \<And>x xa. \<lbrakk>x \<noteq> 0xE00; 0xE0000000 \<le> xa; xa \<le> 0xE00FFFFF; UCAST(12 \<rightarrow> 32) x << 20 \<le> xa; xa \<le> 0xFFFFF + (UCAST(12 \<rightarrow> 32) x << 20)\<rbrakk> \<Longrightarrow> xa - 0xFFFFF \<le> UCAST(12 \<rightarrow> 32) x << 20 proof (prove)
goal (5 subgoals):
 1. \<And>x xa. \<lbrakk>x \<noteq> 0xE00; 0xE0000000 \<le> xa; xa \<le> 0xE00FFFFF; 0x100000 * UCAST(12 \<rightarrow> 32) x \<le> xa; xa \<le> 0xFFFFF + 0x100000 * UCAST(12 \<rightarrow> 32) x; xa - 0xFFFFF \<le> 0x100000 * UCAST(12 \<rightarrow> 32) x; 0xE0000000 < 0x100000 * UCAST(12 \<rightarrow> 32) x\<rbrakk> \<Longrightarrow> 20 \<le> 20
 2. \<And>x xa. \<lbrakk>x \<noteq> 0xE00; 0xE0000000 \<le> xa; xa \<le> 0xE00FFFFF; 0x100000 * UCAST(12 \<rightarrow> 32) x \<le> xa; xa \<le> 0xFFFFF + 0x100000 * UCAST(12 \<rightarrow> 32) x; xa - 0xFFFFF \<le> 0x100000 * UCAST(12 \<rightarrow> 32) x; 0xE0000000 < 0x100000 * UCAST(12 \<rightarrow> 32) x\<rbrakk> \<Longrightarrow> 20 < LENGTH(32)
 3. \<And>x xa. \<lbrakk>x \<noteq> 0xE00; 0xE0000000 \<le> xa; xa \<le> 0xE00FFFFF; 0x100000 * UCAST(12 \<rightarrow> 32) x \<le> xa; xa \<le> 0xFFFFF + 0x100000 * UCAST(12 \<rightarrow> 32) x; xa - 0xFFFFF \<le> 0x100000 * UCAST(12 \<rightarrow> 32) x; 0xE0000000 < 0x100000 * UCAST(12 \<rightarrow> 32) x; 0xE0000000 + 2 ^ 20 \<le> 0x100000 * UCAST(12 \<rightarrow> 32) x\<rbrakk> \<Longrightarrow> 0xE0100000 \<le> 0x100000 * UCAST(12 \<rightarrow> 32) x
 4. \<And>x xa. \<lbrakk>x \<noteq> 0xE00; 0xE0000000 \<le> xa; xa \<le> 0xE00FFFFF; UCAST(12 \<rightarrow> 32) x << 20 \<le> xa; xa \<le> 0xFFFFF + (UCAST(12 \<rightarrow> 32) x << 20); xa - 0xFFFFF \<le> UCAST(12 \<rightarrow> 32) x << 20; \<not> 0xE0000000 < UCAST(12 \<rightarrow> 32) x << 20\<rbrakk> \<Longrightarrow> False
 5. \<And>x xa. \<lbrakk>x \<noteq> 0xE00; 0xE0000000 \<le> xa; xa \<le> 0xE00FFFFF; UCAST(12 \<rightarrow> 32) x << 20 \<le> xa; xa \<le> 0xFFFFF + (UCAST(12 \<rightarrow> 32) x << 20)\<rbrakk> \<Longrightarrow> xa - 0xFFFFF \<le> UCAST(12 \<rightarrow> 32) x << 20 proof (prove)
goal (4 subgoals):
 1. \<And>x xa. \<lbrakk>x \<noteq> 0xE00; 0xE0000000 \<le> xa; xa \<le> 0xE00FFFFF; 0x100000 * UCAST(12 \<rightarrow> 32) x \<le> xa; xa \<le> 0xFFFFF + 0x100000 * UCAST(12 \<rightarrow> 32) x; xa - 0xFFFFF \<le> 0x100000 * UCAST(12 \<rightarrow> 32) x; 0xE0000000 < 0x100000 * UCAST(12 \<rightarrow> 32) x\<rbrakk> \<Longrightarrow> 20 < LENGTH(32)
 2. \<And>x xa. \<lbrakk>x \<noteq> 0xE00; 0xE0000000 \<le> xa; xa \<le> 0xE00FFFFF; 0x100000 * UCAST(12 \<rightarrow> 32) x \<le> xa; xa \<le> 0xFFFFF + 0x100000 * UCAST(12 \<rightarrow> 32) x; xa - 0xFFFFF \<le> 0x100000 * UCAST(12 \<rightarrow> 32) x; 0xE0000000 < 0x100000 * UCAST(12 \<rightarrow> 32) x; 0xE0000000 + 2 ^ 20 \<le> 0x100000 * UCAST(12 \<rightarrow> 32) x\<rbrakk> \<Longrightarrow> 0xE0100000 \<le> 0x100000 * UCAST(12 \<rightarrow> 32) x
 3. \<And>x xa. \<lbrakk>x \<noteq> 0xE00; 0xE0000000 \<le> xa; xa \<le> 0xE00FFFFF; UCAST(12 \<rightarrow> 32) x << 20 \<le> xa; xa \<le> 0xFFFFF + (UCAST(12 \<rightarrow> 32) x << 20); xa - 0xFFFFF \<le> UCAST(12 \<rightarrow> 32) x << 20; \<not> 0xE0000000 < UCAST(12 \<rightarrow> 32) x << 20\<rbrakk> \<Longrightarrow> False
 4. \<And>x xa. \<lbrakk>x \<noteq> 0xE00; 0xE0000000 \<le> xa; xa \<le> 0xE00FFFFF; UCAST(12 \<rightarrow> 32) x << 20 \<le> xa; xa \<le> 0xFFFFF + (UCAST(12 \<rightarrow> 32) x << 20)\<rbrakk> \<Longrightarrow> xa - 0xFFFFF \<le> UCAST(12 \<rightarrow> 32) x << 20 proof (prove)
goal (3 subgoals):
 1. \<And>x xa. \<lbrakk>x \<noteq> 0xE00; 0xE0000000 \<le> xa; xa \<le> 0xE00FFFFF; 0x100000 * UCAST(12 \<rightarrow> 32) x \<le> xa; xa \<le> 0xFFFFF + 0x100000 * UCAST(12 \<rightarrow> 32) x; xa - 0xFFFFF \<le> 0x100000 * UCAST(12 \<rightarrow> 32) x; 0xE0000000 < 0x100000 * UCAST(12 \<rightarrow> 32) x; 0xE0000000 + 2 ^ 20 \<le> 0x100000 * UCAST(12 \<rightarrow> 32) x\<rbrakk> \<Longrightarrow> 0xE0100000 \<le> 0x100000 * UCAST(12 \<rightarrow> 32) x
 2. \<And>x xa. \<lbrakk>x \<noteq> 0xE00; 0xE0000000 \<le> xa; xa \<le> 0xE00FFFFF; UCAST(12 \<rightarrow> 32) x << 20 \<le> xa; xa \<le> 0xFFFFF + (UCAST(12 \<rightarrow> 32) x << 20); xa - 0xFFFFF \<le> UCAST(12 \<rightarrow> 32) x << 20; \<not> 0xE0000000 < UCAST(12 \<rightarrow> 32) x << 20\<rbrakk> \<Longrightarrow> False
 3. \<And>x xa. \<lbrakk>x \<noteq> 0xE00; 0xE0000000 \<le> xa; xa \<le> 0xE00FFFFF; UCAST(12 \<rightarrow> 32) x << 20 \<le> xa; xa \<le> 0xFFFFF + (UCAST(12 \<rightarrow> 32) x << 20)\<rbrakk> \<Longrightarrow> xa - 0xFFFFF \<le> UCAST(12 \<rightarrow> 32) x << 20 proof (prove)
goal (2 subgoals):
 1. \<And>x xa. \<lbrakk>x \<noteq> 0xE00; 0xE0000000 \<le> xa; xa \<le> 0xE00FFFFF; UCAST(12 \<rightarrow> 32) x << 20 \<le> xa; xa \<le> 0xFFFFF + (UCAST(12 \<rightarrow> 32) x << 20); xa - 0xFFFFF \<le> UCAST(12 \<rightarrow> 32) x << 20; \<not> 0xE0000000 < UCAST(12 \<rightarrow> 32) x << 20\<rbrakk> \<Longrightarrow> False
 2. \<And>x xa. \<lbrakk>x \<noteq> 0xE00; 0xE0000000 \<le> xa; xa \<le> 0xE00FFFFF; UCAST(12 \<rightarrow> 32) x << 20 \<le> xa; xa \<le> 0xFFFFF + (UCAST(12 \<rightarrow> 32) x << 20)\<rbrakk> \<Longrightarrow> xa - 0xFFFFF \<le> UCAST(12 \<rightarrow> 32) x << 20 proof (prove)
goal (3 subgoals):
 1. \<And>x xa. \<lbrakk>x \<noteq> 0xE00; 0xE0000000 \<le> xa; xa \<le> 0xE00FFFFF; UCAST(12 \<rightarrow> 32) x << 20 \<le> xa; xa \<le> 0xFFFFF + (UCAST(12 \<rightarrow> 32) x << 20); xa - 0xFFFFF \<le> UCAST(12 \<rightarrow> 32) x << 20; \<not> 0xE0000000 < UCAST(12 \<rightarrow> 32) x << 20; UCAST(12 \<rightarrow> 32) x << 20 < 0xE0000000\<rbrakk> \<Longrightarrow> False
 2. \<And>x xa. \<lbrakk>x \<noteq> 0xE00; 0xE0000000 \<le> xa; xa \<le> 0xE00FFFFF; UCAST(12 \<rightarrow> 32) x << 20 \<le> xa; xa \<le> 0xFFFFF + (UCAST(12 \<rightarrow> 32) x << 20); xa - 0xFFFFF \<le> UCAST(12 \<rightarrow> 32) x << 20; \<not> 0xE0000000 < UCAST(12 \<rightarrow> 32) x << 20; \<not> UCAST(12 \<rightarrow> 32) x << 20 < 0xE0000000\<rbrakk> \<Longrightarrow> False
 3. \<And>x xa. \<lbrakk>x \<noteq> 0xE00; 0xE0000000 \<le> xa; xa \<le> 0xE00FFFFF; UCAST(12 \<rightarrow> 32) x << 20 \<le> xa; xa \<le> 0xFFFFF + (UCAST(12 \<rightarrow> 32) x << 20)\<rbrakk> \<Longrightarrow> xa - 0xFFFFF \<le> UCAST(12 \<rightarrow> 32) x << 20 proof (prove)
goal (4 subgoals):
 1. \<And>x xa. \<lbrakk>x \<noteq> 0xE00; 0xE0000000 \<le> xa; xa \<le> 0xE00FFFFF; UCAST(12 \<rightarrow> 32) x << 20 \<le> xa; xa \<le> 0xFFFFF + (UCAST(12 \<rightarrow> 32) x << 20); xa - 0xFFFFF \<le> UCAST(12 \<rightarrow> 32) x << 20; \<not> 0xE0000000 < UCAST(12 \<rightarrow> 32) x << 20; UCAST(12 \<rightarrow> 32) x << 20 < 0xE0000000; UCAST(12 \<rightarrow> 32) x << 20 \<le> 0xE0000000 - 0x100000\<rbrakk> \<Longrightarrow> False
 2. \<And>x xa. \<lbrakk>x \<noteq> 0xE00; 0xE0000000 \<le> xa; xa \<le> 0xE00FFFFF; UCAST(12 \<rightarrow> 32) x << 20 \<le> xa; xa \<le> 0xFFFFF + (UCAST(12 \<rightarrow> 32) x << 20); xa - 0xFFFFF \<le> UCAST(12 \<rightarrow> 32) x << 20; \<not> 0xE0000000 < UCAST(12 \<rightarrow> 32) x << 20; UCAST(12 \<rightarrow> 32) x << 20 < 0xE0000000\<rbrakk> \<Longrightarrow> UCAST(12 \<rightarrow> 32) x << 20 \<le> 0xE0000000 - 0x100000
 3. \<And>x xa. \<lbrakk>x \<noteq> 0xE00; 0xE0000000 \<le> xa; xa \<le> 0xE00FFFFF; UCAST(12 \<rightarrow> 32) x << 20 \<le> xa; xa \<le> 0xFFFFF + (UCAST(12 \<rightarrow> 32) x << 20); xa - 0xFFFFF \<le> UCAST(12 \<rightarrow> 32) x << 20; \<not> 0xE0000000 < UCAST(12 \<rightarrow> 32) x << 20; \<not> UCAST(12 \<rightarrow> 32) x << 20 < 0xE0000000\<rbrakk> \<Longrightarrow> False
 4. \<And>x xa. \<lbrakk>x \<noteq> 0xE00; 0xE0000000 \<le> xa; xa \<le> 0xE00FFFFF; UCAST(12 \<rightarrow> 32) x << 20 \<le> xa; xa \<le> 0xFFFFF + (UCAST(12 \<rightarrow> 32) x << 20)\<rbrakk> \<Longrightarrow> xa - 0xFFFFF \<le> UCAST(12 \<rightarrow> 32) x << 20 proof (prove)
goal (5 subgoals):
 1. \<And>x xa. \<lbrakk>x \<noteq> 0xE00; 0xE0000000 \<le> xa; xa \<le> 0xE00FFFFF; UCAST(12 \<rightarrow> 32) x << 20 \<le> xa; xa \<le> 0xFFFFF + (UCAST(12 \<rightarrow> 32) x << 20); xa - 0xFFFFF \<le> UCAST(12 \<rightarrow> 32) x << 20; \<not> 0xE0000000 < UCAST(12 \<rightarrow> 32) x << 20; UCAST(12 \<rightarrow> 32) x << 20 < 0xE0000000; UCAST(12 \<rightarrow> 32) x << 20 \<le> 0xE0000000 - 0x100000; 0xFFFFF + (UCAST(12 \<rightarrow> ?'a130) x << 20) \<le> 0xDFFFFFFF\<rbrakk> \<Longrightarrow> False
 2. \<And>x xa. \<lbrakk>x \<noteq> 0xE00; 0xE0000000 \<le> xa; xa \<le> 0xE00FFFFF; UCAST(12 \<rightarrow> 32) x << 20 \<le> xa; xa \<le> 0xFFFFF + (UCAST(12 \<rightarrow> 32) x << 20); xa - 0xFFFFF \<le> UCAST(12 \<rightarrow> 32) x << 20; \<not> 0xE0000000 < UCAST(12 \<rightarrow> 32) x << 20; UCAST(12 \<rightarrow> 32) x << 20 < 0xE0000000; UCAST(12 \<rightarrow> 32) x << 20 \<le> 0xE0000000 - 0x100000\<rbrakk> \<Longrightarrow> 0xFFFFF + (UCAST(12 \<rightarrow> ?'a130) x << 20) \<le> 0xDFFFFFFF
 3. \<And>x xa. \<lbrakk>x \<noteq> 0xE00; 0xE0000000 \<le> xa; xa \<le> 0xE00FFFFF; UCAST(12 \<rightarrow> 32) x << 20 \<le> xa; xa \<le> 0xFFFFF + (UCAST(12 \<rightarrow> 32) x << 20); xa - 0xFFFFF \<le> UCAST(12 \<rightarrow> 32) x << 20; \<not> 0xE0000000 < UCAST(12 \<rightarrow> 32) x << 20; UCAST(12 \<rightarrow> 32) x << 20 < 0xE0000000\<rbrakk> \<Longrightarrow> UCAST(12 \<rightarrow> 32) x << 20 \<le> 0xE0000000 - 0x100000
 4. \<And>x xa. \<lbrakk>x \<noteq> 0xE00; 0xE0000000 \<le> xa; xa \<le> 0xE00FFFFF; UCAST(12 \<rightarrow> 32) x << 20 \<le> xa; xa \<le> 0xFFFFF + (UCAST(12 \<rightarrow> 32) x << 20); xa - 0xFFFFF \<le> UCAST(12 \<rightarrow> 32) x << 20; \<not> 0xE0000000 < UCAST(12 \<rightarrow> 32) x << 20; \<not> UCAST(12 \<rightarrow> 32) x << 20 < 0xE0000000\<rbrakk> \<Longrightarrow> False
 5. \<And>x xa. \<lbrakk>x \<noteq> 0xE00; 0xE0000000 \<le> xa; xa \<le> 0xE00FFFFF; UCAST(12 \<rightarrow> 32) x << 20 \<le> xa; xa \<le> 0xFFFFF + (UCAST(12 \<rightarrow> 32) x << 20)\<rbrakk> \<Longrightarrow> xa - 0xFFFFF \<le> UCAST(12 \<rightarrow> 32) x << 20 proof (prove)
goal (6 subgoals):
 1. \<And>x xa. \<lbrakk>x \<noteq> 0xE00; 0xE0000000 \<le> xa; xa \<le> 0xE00FFFFF; UCAST(12 \<rightarrow> 32) x << 20 \<le> xa; xa - 0xFFFFF \<le> UCAST(12 \<rightarrow> 32) x << 20; \<not> 0xE0000000 < UCAST(12 \<rightarrow> 32) x << 20; UCAST(12 \<rightarrow> 32) x << 20 < 0xE0000000; UCAST(12 \<rightarrow> 32) x << 20 \<le> 0xE0000000 - 0x100000; 0xFFFFF + (UCAST(12 \<rightarrow> ?'a130) x << 20) \<le> 0xDFFFFFFF\<rbrakk> \<Longrightarrow> 0xFFFFF + (UCAST(12 \<rightarrow> 32) x << 20) \<le> 0xDFFFFFFF
 2. \<And>x xa. \<lbrakk>x \<noteq> 0xE00; 0xE0000000 \<le> xa; xa \<le> 0xE00FFFFF; UCAST(12 \<rightarrow> 32) x << 20 \<le> xa; xa - 0xFFFFF \<le> UCAST(12 \<rightarrow> 32) x << 20; \<not> 0xE0000000 < UCAST(12 \<rightarrow> 32) x << 20; UCAST(12 \<rightarrow> 32) x << 20 < 0xE0000000; UCAST(12 \<rightarrow> 32) x << 20 \<le> 0xE0000000 - 0x100000; 0xFFFFF + (UCAST(12 \<rightarrow> ?'a130) x << 20) \<le> 0xDFFFFFFF; xa \<le> 0xDFFFFFFF\<rbrakk> \<Longrightarrow> False
 3. \<And>x xa. \<lbrakk>x \<noteq> 0xE00; 0xE0000000 \<le> xa; xa \<le> 0xE00FFFFF; UCAST(12 \<rightarrow> 32) x << 20 \<le> xa; xa \<le> 0xFFFFF + (UCAST(12 \<rightarrow> 32) x << 20); xa - 0xFFFFF \<le> UCAST(12 \<rightarrow> 32) x << 20; \<not> 0xE0000000 < UCAST(12 \<rightarrow> 32) x << 20; UCAST(12 \<rightarrow> 32) x << 20 < 0xE0000000; UCAST(12 \<rightarrow> 32) x << 20 \<le> 0xE0000000 - 0x100000\<rbrakk> \<Longrightarrow> 0xFFFFF + (UCAST(12 \<rightarrow> ?'a130) x << 20) \<le> 0xDFFFFFFF
 4. \<And>x xa. \<lbrakk>x \<noteq> 0xE00; 0xE0000000 \<le> xa; xa \<le> 0xE00FFFFF; UCAST(12 \<rightarrow> 32) x << 20 \<le> xa; xa \<le> 0xFFFFF + (UCAST(12 \<rightarrow> 32) x << 20); xa - 0xFFFFF \<le> UCAST(12 \<rightarrow> 32) x << 20; \<not> 0xE0000000 < UCAST(12 \<rightarrow> 32) x << 20; UCAST(12 \<rightarrow> 32) x << 20 < 0xE0000000\<rbrakk> \<Longrightarrow> UCAST(12 \<rightarrow> 32) x << 20 \<le> 0xE0000000 - 0x100000
 5. \<And>x xa. \<lbrakk>x \<noteq> 0xE00; 0xE0000000 \<le> xa; xa \<le> 0xE00FFFFF; UCAST(12 \<rightarrow> 32) x << 20 \<le> xa; xa \<le> 0xFFFFF + (UCAST(12 \<rightarrow> 32) x << 20); xa - 0xFFFFF \<le> UCAST(12 \<rightarrow> 32) x << 20; \<not> 0xE0000000 < UCAST(12 \<rightarrow> 32) x << 20; \<not> UCAST(12 \<rightarrow> 32) x << 20 < 0xE0000000\<rbrakk> \<Longrightarrow> False
 6. \<And>x xa. \<lbrakk>x \<noteq> 0xE00; 0xE0000000 \<le> xa; xa \<le> 0xE00FFFFF; UCAST(12 \<rightarrow> 32) x << 20 \<le> xa; xa \<le> 0xFFFFF + (UCAST(12 \<rightarrow> 32) x << 20)\<rbrakk> \<Longrightarrow> xa - 0xFFFFF \<le> UCAST(12 \<rightarrow> 32) x << 20 proof (prove)
goal (5 subgoals):
 1. \<And>x xa. \<lbrakk>x \<noteq> 0xE00; 0xE0000000 \<le> xa; xa \<le> 0xE00FFFFF; UCAST(12 \<rightarrow> 32) x << 20 \<le> xa; xa - 0xFFFFF \<le> UCAST(12 \<rightarrow> 32) x << 20; \<not> 0xE0000000 < UCAST(12 \<rightarrow> 32) x << 20; UCAST(12 \<rightarrow> 32) x << 20 < 0xE0000000; UCAST(12 \<rightarrow> 32) x << 20 \<le> 0xE0000000 - 0x100000; 0xFFFFF + (UCAST(12 \<rightarrow> 32) x << 20) \<le> 0xDFFFFFFF; xa \<le> 0xDFFFFFFF\<rbrakk> \<Longrightarrow> False
 2. \<And>x xa. \<lbrakk>x \<noteq> 0xE00; 0xE0000000 \<le> xa; xa \<le> 0xE00FFFFF; UCAST(12 \<rightarrow> 32) x << 20 \<le> xa; xa \<le> 0xFFFFF + (UCAST(12 \<rightarrow> 32) x << 20); xa - 0xFFFFF \<le> UCAST(12 \<rightarrow> 32) x << 20; \<not> 0xE0000000 < UCAST(12 \<rightarrow> 32) x << 20; UCAST(12 \<rightarrow> 32) x << 20 < 0xE0000000; UCAST(12 \<rightarrow> 32) x << 20 \<le> 0xE0000000 - 0x100000\<rbrakk> \<Longrightarrow> 0xFFFFF + (UCAST(12 \<rightarrow> 32) x << 20) \<le> 0xDFFFFFFF
 3. \<And>x xa. \<lbrakk>x \<noteq> 0xE00; 0xE0000000 \<le> xa; xa \<le> 0xE00FFFFF; UCAST(12 \<rightarrow> 32) x << 20 \<le> xa; xa \<le> 0xFFFFF + (UCAST(12 \<rightarrow> 32) x << 20); xa - 0xFFFFF \<le> UCAST(12 \<rightarrow> 32) x << 20; \<not> 0xE0000000 < UCAST(12 \<rightarrow> 32) x << 20; UCAST(12 \<rightarrow> 32) x << 20 < 0xE0000000\<rbrakk> \<Longrightarrow> UCAST(12 \<rightarrow> 32) x << 20 \<le> 0xE0000000 - 0x100000
 4. \<And>x xa. \<lbrakk>x \<noteq> 0xE00; 0xE0000000 \<le> xa; xa \<le> 0xE00FFFFF; UCAST(12 \<rightarrow> 32) x << 20 \<le> xa; xa \<le> 0xFFFFF + (UCAST(12 \<rightarrow> 32) x << 20); xa - 0xFFFFF \<le> UCAST(12 \<rightarrow> 32) x << 20; \<not> 0xE0000000 < UCAST(12 \<rightarrow> 32) x << 20; \<not> UCAST(12 \<rightarrow> 32) x << 20 < 0xE0000000\<rbrakk> \<Longrightarrow> False
 5. \<And>x xa. \<lbrakk>x \<noteq> 0xE00; 0xE0000000 \<le> xa; xa \<le> 0xE00FFFFF; UCAST(12 \<rightarrow> 32) x << 20 \<le> xa; xa \<le> 0xFFFFF + (UCAST(12 \<rightarrow> 32) x << 20)\<rbrakk> \<Longrightarrow> xa - 0xFFFFF \<le> UCAST(12 \<rightarrow> 32) x << 20 proof (prove)
goal (4 subgoals):
 1. \<And>x xa. \<lbrakk>x \<noteq> 0xE00; 0xE0000000 \<le> xa; xa \<le> 0xE00FFFFF; UCAST(12 \<rightarrow> 32) x << 20 \<le> xa; xa \<le> 0xFFFFF + (UCAST(12 \<rightarrow> 32) x << 20); xa - 0xFFFFF \<le> UCAST(12 \<rightarrow> 32) x << 20; \<not> 0xE0000000 < UCAST(12 \<rightarrow> 32) x << 20; UCAST(12 \<rightarrow> 32) x << 20 < 0xE0000000; UCAST(12 \<rightarrow> 32) x << 20 \<le> 0xE0000000 - 0x100000\<rbrakk> \<Longrightarrow> 0xFFFFF + (UCAST(12 \<rightarrow> 32) x << 20) \<le> 0xDFFFFFFF
 2. \<And>x xa. \<lbrakk>x \<noteq> 0xE00; 0xE0000000 \<le> xa; xa \<le> 0xE00FFFFF; UCAST(12 \<rightarrow> 32) x << 20 \<le> xa; xa \<le> 0xFFFFF + (UCAST(12 \<rightarrow> 32) x << 20); xa - 0xFFFFF \<le> UCAST(12 \<rightarrow> 32) x << 20; \<not> 0xE0000000 < UCAST(12 \<rightarrow> 32) x << 20; UCAST(12 \<rightarrow> 32) x << 20 < 0xE0000000\<rbrakk> \<Longrightarrow> UCAST(12 \<rightarrow> 32) x << 20 \<le> 0xE0000000 - 0x100000
 3. \<And>x xa. \<lbrakk>x \<noteq> 0xE00; 0xE0000000 \<le> xa; xa \<le> 0xE00FFFFF; UCAST(12 \<rightarrow> 32) x << 20 \<le> xa; xa \<le> 0xFFFFF + (UCAST(12 \<rightarrow> 32) x << 20); xa - 0xFFFFF \<le> UCAST(12 \<rightarrow> 32) x << 20; \<not> 0xE0000000 < UCAST(12 \<rightarrow> 32) x << 20; \<not> UCAST(12 \<rightarrow> 32) x << 20 < 0xE0000000\<rbrakk> \<Longrightarrow> False
 4. \<And>x xa. \<lbrakk>x \<noteq> 0xE00; 0xE0000000 \<le> xa; xa \<le> 0xE00FFFFF; UCAST(12 \<rightarrow> 32) x << 20 \<le> xa; xa \<le> 0xFFFFF + (UCAST(12 \<rightarrow> 32) x << 20)\<rbrakk> \<Longrightarrow> xa - 0xFFFFF \<le> UCAST(12 \<rightarrow> 32) x << 20 proof (prove)
goal (4 subgoals):
 1. \<And>x xa. \<lbrakk>x \<noteq> 0xE00; 0xE0000000 \<le> xa; xa \<le> 0xE00FFFFF; UCAST(12 \<rightarrow> 32) x << 20 \<le> xa; xa \<le> (UCAST(12 \<rightarrow> 32) x << 20) + 0xFFFFF; xa - 0xFFFFF \<le> UCAST(12 \<rightarrow> 32) x << 20; \<not> 0xE0000000 < UCAST(12 \<rightarrow> 32) x << 20; UCAST(12 \<rightarrow> 32) x << 20 < 0xE0000000; UCAST(12 \<rightarrow> 32) x << 20 \<le> 0xDFF00000\<rbrakk> \<Longrightarrow> (UCAST(12 \<rightarrow> 32) x << 20) + 0xFFFFF \<le> 0xDFFFFFFF
 2. \<And>x xa. \<lbrakk>x \<noteq> 0xE00; 0xE0000000 \<le> xa; xa \<le> 0xE00FFFFF; UCAST(12 \<rightarrow> 32) x << 20 \<le> xa; xa \<le> 0xFFFFF + (UCAST(12 \<rightarrow> 32) x << 20); xa - 0xFFFFF \<le> UCAST(12 \<rightarrow> 32) x << 20; \<not> 0xE0000000 < UCAST(12 \<rightarrow> 32) x << 20; UCAST(12 \<rightarrow> 32) x << 20 < 0xE0000000\<rbrakk> \<Longrightarrow> UCAST(12 \<rightarrow> 32) x << 20 \<le> 0xE0000000 - 0x100000
 3. \<And>x xa. \<lbrakk>x \<noteq> 0xE00; 0xE0000000 \<le> xa; xa \<le> 0xE00FFFFF; UCAST(12 \<rightarrow> 32) x << 20 \<le> xa; xa \<le> 0xFFFFF + (UCAST(12 \<rightarrow> 32) x << 20); xa - 0xFFFFF \<le> UCAST(12 \<rightarrow> 32) x << 20; \<not> 0xE0000000 < UCAST(12 \<rightarrow> 32) x << 20; \<not> UCAST(12 \<rightarrow> 32) x << 20 < 0xE0000000\<rbrakk> \<Longrightarrow> False
 4. \<And>x xa. \<lbrakk>x \<noteq> 0xE00; 0xE0000000 \<le> xa; xa \<le> 0xE00FFFFF; UCAST(12 \<rightarrow> 32) x << 20 \<le> xa; xa \<le> 0xFFFFF + (UCAST(12 \<rightarrow> 32) x << 20)\<rbrakk> \<Longrightarrow> xa - 0xFFFFF \<le> UCAST(12 \<rightarrow> 32) x << 20 proof (prove)
goal (3 subgoals):
 1. \<And>x xa. \<lbrakk>x \<noteq> 0xE00; 0xE0000000 \<le> xa; xa \<le> 0xE00FFFFF; UCAST(12 \<rightarrow> 32) x << 20 \<le> xa; xa \<le> 0xFFFFF + (UCAST(12 \<rightarrow> 32) x << 20); xa - 0xFFFFF \<le> UCAST(12 \<rightarrow> 32) x << 20; \<not> 0xE0000000 < UCAST(12 \<rightarrow> 32) x << 20; UCAST(12 \<rightarrow> 32) x << 20 < 0xE0000000\<rbrakk> \<Longrightarrow> UCAST(12 \<rightarrow> 32) x << 20 \<le> 0xE0000000 - 0x100000
 2. \<And>x xa. \<lbrakk>x \<noteq> 0xE00; 0xE0000000 \<le> xa; xa \<le> 0xE00FFFFF; UCAST(12 \<rightarrow> 32) x << 20 \<le> xa; xa \<le> 0xFFFFF + (UCAST(12 \<rightarrow> 32) x << 20); xa - 0xFFFFF \<le> UCAST(12 \<rightarrow> 32) x << 20; \<not> 0xE0000000 < UCAST(12 \<rightarrow> 32) x << 20; \<not> UCAST(12 \<rightarrow> 32) x << 20 < 0xE0000000\<rbrakk> \<Longrightarrow> False
 3. \<And>x xa. \<lbrakk>x \<noteq> 0xE00; 0xE0000000 \<le> xa; xa \<le> 0xE00FFFFF; UCAST(12 \<rightarrow> 32) x << 20 \<le> xa; xa \<le> 0xFFFFF + (UCAST(12 \<rightarrow> 32) x << 20)\<rbrakk> \<Longrightarrow> xa - 0xFFFFF \<le> UCAST(12 \<rightarrow> 32) x << 20 proof (prove)
goal (3 subgoals):
 1. \<And>x xa. \<lbrakk>x \<noteq> 0xE00; 0xE0000000 \<le> xa; xa \<le> 0xE00FFFFF; 0x100000 * UCAST(12 \<rightarrow> 32) x \<le> xa; xa \<le> 0xFFFFF + 0x100000 * UCAST(12 \<rightarrow> 32) x; xa - 0xFFFFF \<le> 0x100000 * UCAST(12 \<rightarrow> 32) x; \<not> 0xE0000000 < 0x100000 * UCAST(12 \<rightarrow> 32) x; 0x100000 * UCAST(12 \<rightarrow> 32) x < 0xE0000000\<rbrakk> \<Longrightarrow> 0x100000 * UCAST(12 \<rightarrow> 32) x \<le> 0xDFF00000
 2. \<And>x xa. \<lbrakk>x \<noteq> 0xE00; 0xE0000000 \<le> xa; xa \<le> 0xE00FFFFF; UCAST(12 \<rightarrow> 32) x << 20 \<le> xa; xa \<le> 0xFFFFF + (UCAST(12 \<rightarrow> 32) x << 20); xa - 0xFFFFF \<le> UCAST(12 \<rightarrow> 32) x << 20; \<not> 0xE0000000 < UCAST(12 \<rightarrow> 32) x << 20; \<not> UCAST(12 \<rightarrow> 32) x << 20 < 0xE0000000\<rbrakk> \<Longrightarrow> False
 3. \<And>x xa. \<lbrakk>x \<noteq> 0xE00; 0xE0000000 \<le> xa; xa \<le> 0xE00FFFFF; UCAST(12 \<rightarrow> 32) x << 20 \<le> xa; xa \<le> 0xFFFFF + (UCAST(12 \<rightarrow> 32) x << 20)\<rbrakk> \<Longrightarrow> xa - 0xFFFFF \<le> UCAST(12 \<rightarrow> 32) x << 20 proof (prove)
goal (6 subgoals):
 1. \<And>x xa. \<lbrakk>x \<noteq> 0xE00; 0xE0000000 \<le> xa; xa \<le> 0xE00FFFFF; 0x100000 * UCAST(12 \<rightarrow> 32) x \<le> xa; xa \<le> 0xFFFFF + 0x100000 * UCAST(12 \<rightarrow> 32) x; xa - 0xFFFFF \<le> 0x100000 * UCAST(12 \<rightarrow> 32) x; \<not> 0xE0000000 < 0x100000 * UCAST(12 \<rightarrow> 32) x; 0x100000 * UCAST(12 \<rightarrow> 32) x < 0xE0000000\<rbrakk> \<Longrightarrow> 0x100000 * UCAST(12 \<rightarrow> 32) x < 0xE0000000
 2. \<And>x xa. \<lbrakk>x \<noteq> 0xE00; 0xE0000000 \<le> xa; xa \<le> 0xE00FFFFF; 0x100000 * UCAST(12 \<rightarrow> 32) x \<le> xa; xa \<le> 0xFFFFF + 0x100000 * UCAST(12 \<rightarrow> 32) x; xa - 0xFFFFF \<le> 0x100000 * UCAST(12 \<rightarrow> 32) x; \<not> 0xE0000000 < 0x100000 * UCAST(12 \<rightarrow> 32) x; 0x100000 * UCAST(12 \<rightarrow> 32) x < 0xE0000000\<rbrakk> \<Longrightarrow> uint (0x100000 * UCAST(12 \<rightarrow> 32) x) = ?n144 x xa * int (take_bit LENGTH(32) 1048576)
 3. \<And>x xa. \<lbrakk>x \<noteq> 0xE00; 0xE0000000 \<le> xa; xa \<le> 0xE00FFFFF; 0x100000 * UCAST(12 \<rightarrow> 32) x \<le> xa; xa \<le> 0xFFFFF + 0x100000 * UCAST(12 \<rightarrow> 32) x; xa - 0xFFFFF \<le> 0x100000 * UCAST(12 \<rightarrow> 32) x; \<not> 0xE0000000 < 0x100000 * UCAST(12 \<rightarrow> 32) x; 0x100000 * UCAST(12 \<rightarrow> 32) x < 0xE0000000\<rbrakk> \<Longrightarrow> int (take_bit LENGTH(32) 3758096384) = ?n'144 x xa * int (take_bit LENGTH(32) 1048576)
 4. \<And>x xa. \<lbrakk>x \<noteq> 0xE00; 0xE0000000 \<le> xa; xa \<le> 0xE00FFFFF; 0x100000 * UCAST(12 \<rightarrow> 32) x \<le> xa; xa \<le> 0xFFFFF + 0x100000 * UCAST(12 \<rightarrow> 32) x; xa - 0xFFFFF \<le> 0x100000 * UCAST(12 \<rightarrow> 32) x; \<not> 0xE0000000 < 0x100000 * UCAST(12 \<rightarrow> 32) x; 0x100000 * UCAST(12 \<rightarrow> 32) x < 0xE0000000\<rbrakk> \<Longrightarrow> int (take_bit LENGTH(32) 3758096384) = ?n'144 x xa * int (take_bit LENGTH(32) 1048576)
 5. \<And>x xa. \<lbrakk>x \<noteq> 0xE00; 0xE0000000 \<le> xa; xa \<le> 0xE00FFFFF; UCAST(12 \<rightarrow> 32) x << 20 \<le> xa; xa \<le> 0xFFFFF + (UCAST(12 \<rightarrow> 32) x << 20); xa - 0xFFFFF \<le> UCAST(12 \<rightarrow> 32) x << 20; \<not> 0xE0000000 < UCAST(12 \<rightarrow> 32) x << 20; \<not> UCAST(12 \<rightarrow> 32) x << 20 < 0xE0000000\<rbrakk> \<Longrightarrow> False
 6. \<And>x xa. \<lbrakk>x \<noteq> 0xE00; 0xE0000000 \<le> xa; xa \<le> 0xE00FFFFF; UCAST(12 \<rightarrow> 32) x << 20 \<le> xa; xa \<le> 0xFFFFF + (UCAST(12 \<rightarrow> 32) x << 20)\<rbrakk> \<Longrightarrow> xa - 0xFFFFF \<le> UCAST(12 \<rightarrow> 32) x << 20 proof (prove)
goal (5 subgoals):
 1. \<And>x xa. \<lbrakk>x \<noteq> 0xE00; 0xE0000000 \<le> xa; xa \<le> 0xE00FFFFF; 0x100000 * UCAST(12 \<rightarrow> 32) x \<le> xa; xa \<le> 0xFFFFF + 0x100000 * UCAST(12 \<rightarrow> 32) x; xa - 0xFFFFF \<le> 0x100000 * UCAST(12 \<rightarrow> 32) x; \<not> 0xE0000000 < 0x100000 * UCAST(12 \<rightarrow> 32) x; 0x100000 * UCAST(12 \<rightarrow> 32) x < 0xE0000000\<rbrakk> \<Longrightarrow> uint (0x100000 * UCAST(12 \<rightarrow> 32) x) = ?n144 x xa * int (take_bit LENGTH(32) 1048576)
 2. \<And>x xa. \<lbrakk>x \<noteq> 0xE00; 0xE0000000 \<le> xa; xa \<le> 0xE00FFFFF; 0x100000 * UCAST(12 \<rightarrow> 32) x \<le> xa; xa \<le> 0xFFFFF + 0x100000 * UCAST(12 \<rightarrow> 32) x; xa - 0xFFFFF \<le> 0x100000 * UCAST(12 \<rightarrow> 32) x; \<not> 0xE0000000 < 0x100000 * UCAST(12 \<rightarrow> 32) x; 0x100000 * UCAST(12 \<rightarrow> 32) x < 0xE0000000\<rbrakk> \<Longrightarrow> int (take_bit LENGTH(32) 3758096384) = ?n'144 x xa * int (take_bit LENGTH(32) 1048576)
 3. \<And>x xa. \<lbrakk>x \<noteq> 0xE00; 0xE0000000 \<le> xa; xa \<le> 0xE00FFFFF; 0x100000 * UCAST(12 \<rightarrow> 32) x \<le> xa; xa \<le> 0xFFFFF + 0x100000 * UCAST(12 \<rightarrow> 32) x; xa - 0xFFFFF \<le> 0x100000 * UCAST(12 \<rightarrow> 32) x; \<not> 0xE0000000 < 0x100000 * UCAST(12 \<rightarrow> 32) x; 0x100000 * UCAST(12 \<rightarrow> 32) x < 0xE0000000\<rbrakk> \<Longrightarrow> int (take_bit LENGTH(32) 3758096384) = ?n'144 x xa * int (take_bit LENGTH(32) 1048576)
 4. \<And>x xa. \<lbrakk>x \<noteq> 0xE00; 0xE0000000 \<le> xa; xa \<le> 0xE00FFFFF; UCAST(12 \<rightarrow> 32) x << 20 \<le> xa; xa \<le> 0xFFFFF + (UCAST(12 \<rightarrow> 32) x << 20); xa - 0xFFFFF \<le> UCAST(12 \<rightarrow> 32) x << 20; \<not> 0xE0000000 < UCAST(12 \<rightarrow> 32) x << 20; \<not> UCAST(12 \<rightarrow> 32) x << 20 < 0xE0000000\<rbrakk> \<Longrightarrow> False
 5. \<And>x xa. \<lbrakk>x \<noteq> 0xE00; 0xE0000000 \<le> xa; xa \<le> 0xE00FFFFF; UCAST(12 \<rightarrow> 32) x << 20 \<le> xa; xa \<le> 0xFFFFF + (UCAST(12 \<rightarrow> 32) x << 20)\<rbrakk> \<Longrightarrow> xa - 0xFFFFF \<le> UCAST(12 \<rightarrow> 32) x << 20 proof (prove)
goal (5 subgoals):
 1. \<And>x xa. \<lbrakk>x \<noteq> 0xE00; 0xE0000000 \<le> xa; xa \<le> 0xE00FFFFF; 0x100000 * UCAST(12 \<rightarrow> 32) x \<le> xa; xa \<le> 0xFFFFF + 0x100000 * UCAST(12 \<rightarrow> 32) x; xa - 0xFFFFF \<le> 0x100000 * UCAST(12 \<rightarrow> 32) x; \<not> 0xE0000000 < 0x100000 * UCAST(12 \<rightarrow> 32) x; 0x100000 * UCAST(12 \<rightarrow> 32) x < 0xE0000000\<rbrakk> \<Longrightarrow> 1048576 * uint (UCAST(12 \<rightarrow> 32) x) mod 4294967296 = ?n144 x xa * 1048576
 2. \<And>x xa. \<lbrakk>x \<noteq> 0xE00; 0xE0000000 \<le> xa; xa \<le> 0xE00FFFFF; 0x100000 * UCAST(12 \<rightarrow> 32) x \<le> xa; xa \<le> 0xFFFFF + 0x100000 * UCAST(12 \<rightarrow> 32) x; xa - 0xFFFFF \<le> 0x100000 * UCAST(12 \<rightarrow> 32) x; \<not> 0xE0000000 < 0x100000 * UCAST(12 \<rightarrow> 32) x; 0x100000 * UCAST(12 \<rightarrow> 32) x < 0xE0000000\<rbrakk> \<Longrightarrow> int (take_bit LENGTH(32) 3758096384) = ?n'144 x xa * int (take_bit LENGTH(32) 1048576)
 3. \<And>x xa. \<lbrakk>x \<noteq> 0xE00; 0xE0000000 \<le> xa; xa \<le> 0xE00FFFFF; 0x100000 * UCAST(12 \<rightarrow> 32) x \<le> xa; xa \<le> 0xFFFFF + 0x100000 * UCAST(12 \<rightarrow> 32) x; xa - 0xFFFFF \<le> 0x100000 * UCAST(12 \<rightarrow> 32) x; \<not> 0xE0000000 < 0x100000 * UCAST(12 \<rightarrow> 32) x; 0x100000 * UCAST(12 \<rightarrow> 32) x < 0xE0000000\<rbrakk> \<Longrightarrow> int (take_bit LENGTH(32) 3758096384) = ?n'144 x xa * int (take_bit LENGTH(32) 1048576)
 4. \<And>x xa. \<lbrakk>x \<noteq> 0xE00; 0xE0000000 \<le> xa; xa \<le> 0xE00FFFFF; UCAST(12 \<rightarrow> 32) x << 20 \<le> xa; xa \<le> 0xFFFFF + (UCAST(12 \<rightarrow> 32) x << 20); xa - 0xFFFFF \<le> UCAST(12 \<rightarrow> 32) x << 20; \<not> 0xE0000000 < UCAST(12 \<rightarrow> 32) x << 20; \<not> UCAST(12 \<rightarrow> 32) x << 20 < 0xE0000000\<rbrakk> \<Longrightarrow> False
 5. \<And>x xa. \<lbrakk>x \<noteq> 0xE00; 0xE0000000 \<le> xa; xa \<le> 0xE00FFFFF; UCAST(12 \<rightarrow> 32) x << 20 \<le> xa; xa \<le> 0xFFFFF + (UCAST(12 \<rightarrow> 32) x << 20)\<rbrakk> \<Longrightarrow> xa - 0xFFFFF \<le> UCAST(12 \<rightarrow> 32) x << 20 proof (prove)
goal (5 subgoals):
 1. \<And>x xa. \<lbrakk>x \<noteq> 0xE00; 0xE0000000 \<le> xa; xa \<le> 0xE00FFFFF; 0x100000 * UCAST(12 \<rightarrow> 32) x \<le> xa; xa \<le> 0xFFFFF + 0x100000 * UCAST(12 \<rightarrow> 32) x; xa - 0xFFFFF \<le> 0x100000 * UCAST(12 \<rightarrow> 32) x; \<not> 0xE0000000 < 0x100000 * UCAST(12 \<rightarrow> 32) x; 0x100000 * UCAST(12 \<rightarrow> 32) x < 0xE0000000\<rbrakk> \<Longrightarrow> 1048576 * (uint (UCAST(12 \<rightarrow> 32) x) mod 4096) = ?n189 x x xa (?xa188 x xa) * 1048576
 2. \<And>x xa. \<lbrakk>x \<noteq> 0xE00; 0xE0000000 \<le> xa; xa \<le> 0xE00FFFFF; 0x100000 * UCAST(12 \<rightarrow> 32) x \<le> xa; xa \<le> 0xFFFFF + 0x100000 * UCAST(12 \<rightarrow> 32) x; xa - 0xFFFFF \<le> 0x100000 * UCAST(12 \<rightarrow> 32) x; \<not> 0xE0000000 < 0x100000 * UCAST(12 \<rightarrow> 32) x; 0x100000 * UCAST(12 \<rightarrow> 32) x < 0xE0000000\<rbrakk> \<Longrightarrow> int (take_bit LENGTH(32) 3758096384) = ?n'144 x xa * int (take_bit LENGTH(32) 1048576)
 3. \<And>x xa. \<lbrakk>x \<noteq> 0xE00; 0xE0000000 \<le> xa; xa \<le> 0xE00FFFFF; 0x100000 * UCAST(12 \<rightarrow> 32) x \<le> xa; xa \<le> 0xFFFFF + 0x100000 * UCAST(12 \<rightarrow> 32) x; xa - 0xFFFFF \<le> 0x100000 * UCAST(12 \<rightarrow> 32) x; \<not> 0xE0000000 < 0x100000 * UCAST(12 \<rightarrow> 32) x; 0x100000 * UCAST(12 \<rightarrow> 32) x < 0xE0000000\<rbrakk> \<Longrightarrow> int (take_bit LENGTH(32) 3758096384) = ?n'144 x xa * int (take_bit LENGTH(32) 1048576)
 4. \<And>x xa. \<lbrakk>x \<noteq> 0xE00; 0xE0000000 \<le> xa; xa \<le> 0xE00FFFFF; UCAST(12 \<rightarrow> 32) x << 20 \<le> xa; xa \<le> 0xFFFFF + (UCAST(12 \<rightarrow> 32) x << 20); xa - 0xFFFFF \<le> UCAST(12 \<rightarrow> 32) x << 20; \<not> 0xE0000000 < UCAST(12 \<rightarrow> 32) x << 20; \<not> UCAST(12 \<rightarrow> 32) x << 20 < 0xE0000000\<rbrakk> \<Longrightarrow> False
 5. \<And>x xa. \<lbrakk>x \<noteq> 0xE00; 0xE0000000 \<le> xa; xa \<le> 0xE00FFFFF; UCAST(12 \<rightarrow> 32) x << 20 \<le> xa; xa \<le> 0xFFFFF + (UCAST(12 \<rightarrow> 32) x << 20)\<rbrakk> \<Longrightarrow> xa - 0xFFFFF \<le> UCAST(12 \<rightarrow> 32) x << 20 proof (prove)
goal (4 subgoals):
 1. \<And>x xa. \<lbrakk>x \<noteq> 0xE00; 0xE0000000 \<le> xa; xa \<le> 0xE00FFFFF; 0x100000 * UCAST(12 \<rightarrow> 32) x \<le> xa; xa \<le> 0xFFFFF + 0x100000 * UCAST(12 \<rightarrow> 32) x; xa - 0xFFFFF \<le> 0x100000 * UCAST(12 \<rightarrow> 32) x; \<not> 0xE0000000 < 0x100000 * UCAST(12 \<rightarrow> 32) x; 0x100000 * UCAST(12 \<rightarrow> 32) x < 0xE0000000\<rbrakk> \<Longrightarrow> int (take_bit LENGTH(32) 3758096384) = ?n'144 x xa * int (take_bit LENGTH(32) 1048576)
 2. \<And>x xa. \<lbrakk>x \<noteq> 0xE00; 0xE0000000 \<le> xa; xa \<le> 0xE00FFFFF; 0x100000 * UCAST(12 \<rightarrow> 32) x \<le> xa; xa \<le> 0xFFFFF + 0x100000 * UCAST(12 \<rightarrow> 32) x; xa - 0xFFFFF \<le> 0x100000 * UCAST(12 \<rightarrow> 32) x; \<not> 0xE0000000 < 0x100000 * UCAST(12 \<rightarrow> 32) x; 0x100000 * UCAST(12 \<rightarrow> 32) x < 0xE0000000\<rbrakk> \<Longrightarrow> int (take_bit LENGTH(32) 3758096384) = ?n'144 x xa * int (take_bit LENGTH(32) 1048576)
 3. \<And>x xa. \<lbrakk>x \<noteq> 0xE00; 0xE0000000 \<le> xa; xa \<le> 0xE00FFFFF; UCAST(12 \<rightarrow> 32) x << 20 \<le> xa; xa \<le> 0xFFFFF + (UCAST(12 \<rightarrow> 32) x << 20); xa - 0xFFFFF \<le> UCAST(12 \<rightarrow> 32) x << 20; \<not> 0xE0000000 < UCAST(12 \<rightarrow> 32) x << 20; \<not> UCAST(12 \<rightarrow> 32) x << 20 < 0xE0000000\<rbrakk> \<Longrightarrow> False
 4. \<And>x xa. \<lbrakk>x \<noteq> 0xE00; 0xE0000000 \<le> xa; xa \<le> 0xE00FFFFF; UCAST(12 \<rightarrow> 32) x << 20 \<le> xa; xa \<le> 0xFFFFF + (UCAST(12 \<rightarrow> 32) x << 20)\<rbrakk> \<Longrightarrow> xa - 0xFFFFF \<le> UCAST(12 \<rightarrow> 32) x << 20 proof (prove)
goal (3 subgoals):
 1. \<And>x xa. \<lbrakk>x \<noteq> 0xE00; 0xE0000000 \<le> xa; xa \<le> 0xE00FFFFF; 0x100000 * UCAST(12 \<rightarrow> 32) x \<le> xa; xa \<le> 0xFFFFF + 0x100000 * UCAST(12 \<rightarrow> 32) x; xa - 0xFFFFF \<le> 0x100000 * UCAST(12 \<rightarrow> 32) x; \<not> 0xE0000000 < 0x100000 * UCAST(12 \<rightarrow> 32) x; 0x100000 * UCAST(12 \<rightarrow> 32) x < 0xE0000000\<rbrakk> \<Longrightarrow> int (take_bit LENGTH(32) 3758096384) = 3584 * int (take_bit LENGTH(32) 1048576)
 2. \<And>x xa. \<lbrakk>x \<noteq> 0xE00; 0xE0000000 \<le> xa; xa \<le> 0xE00FFFFF; UCAST(12 \<rightarrow> 32) x << 20 \<le> xa; xa \<le> 0xFFFFF + (UCAST(12 \<rightarrow> 32) x << 20); xa - 0xFFFFF \<le> UCAST(12 \<rightarrow> 32) x << 20; \<not> 0xE0000000 < UCAST(12 \<rightarrow> 32) x << 20; \<not> UCAST(12 \<rightarrow> 32) x << 20 < 0xE0000000\<rbrakk> \<Longrightarrow> False
 3. \<And>x xa. \<lbrakk>x \<noteq> 0xE00; 0xE0000000 \<le> xa; xa \<le> 0xE00FFFFF; UCAST(12 \<rightarrow> 32) x << 20 \<le> xa; xa \<le> 0xFFFFF + (UCAST(12 \<rightarrow> 32) x << 20)\<rbrakk> \<Longrightarrow> xa - 0xFFFFF \<le> UCAST(12 \<rightarrow> 32) x << 20 proof (prove)
goal (2 subgoals):
 1. \<And>x xa. \<lbrakk>x \<noteq> 0xE00; 0xE0000000 \<le> xa; xa \<le> 0xE00FFFFF; UCAST(12 \<rightarrow> 32) x << 20 \<le> xa; xa \<le> 0xFFFFF + (UCAST(12 \<rightarrow> 32) x << 20); xa - 0xFFFFF \<le> UCAST(12 \<rightarrow> 32) x << 20; \<not> 0xE0000000 < UCAST(12 \<rightarrow> 32) x << 20; \<not> UCAST(12 \<rightarrow> 32) x << 20 < 0xE0000000\<rbrakk> \<Longrightarrow> False
 2. \<And>x xa. \<lbrakk>x \<noteq> 0xE00; 0xE0000000 \<le> xa; xa \<le> 0xE00FFFFF; UCAST(12 \<rightarrow> 32) x << 20 \<le> xa; xa \<le> 0xFFFFF + (UCAST(12 \<rightarrow> 32) x << 20)\<rbrakk> \<Longrightarrow> xa - 0xFFFFF \<le> UCAST(12 \<rightarrow> 32) x << 20 proof (prove)
goal (2 subgoals):
 1. \<And>x xa. \<lbrakk>0xE0000000 \<le> xa; xa \<le> 0xE00FFFFF; UCAST(12 \<rightarrow> 32) x << 20 \<le> xa; xa \<le> 0xFFFFF + (UCAST(12 \<rightarrow> 32) x << 20); xa - 0xFFFFF \<le> UCAST(12 \<rightarrow> 32) x << 20; \<not> 0xE0000000 < UCAST(12 \<rightarrow> 32) x << 20; \<not> UCAST(12 \<rightarrow> 32) x << 20 < 0xE0000000\<rbrakk> \<Longrightarrow> x = 0xE00
 2. \<And>x xa. \<lbrakk>x \<noteq> 0xE00; 0xE0000000 \<le> xa; xa \<le> 0xE00FFFFF; UCAST(12 \<rightarrow> 32) x << 20 \<le> xa; xa \<le> 0xFFFFF + (UCAST(12 \<rightarrow> 32) x << 20)\<rbrakk> \<Longrightarrow> xa - 0xFFFFF \<le> UCAST(12 \<rightarrow> 32) x << 20 proof (prove)
goal (4 subgoals):
 1. \<And>x xa. \<lbrakk>0xE0000000 \<le> xa; xa \<le> 0xE00FFFFF; UCAST(12 \<rightarrow> 32) x << 20 \<le> xa; xa \<le> 0xFFFFF + (UCAST(12 \<rightarrow> 32) x << 20); xa - 0xFFFFF \<le> UCAST(12 \<rightarrow> 32) x << 20; \<not> 0xE0000000 < UCAST(12 \<rightarrow> 32) x << 20; \<not> UCAST(12 \<rightarrow> 32) x << 20 < 0xE0000000\<rbrakk> \<Longrightarrow> 20 < LENGTH(32)
 2. \<And>x xa. \<lbrakk>0xE0000000 \<le> xa; xa \<le> 0xE00FFFFF; UCAST(12 \<rightarrow> 32) x << 20 \<le> xa; xa \<le> 0xFFFFF + (UCAST(12 \<rightarrow> 32) x << 20); xa - 0xFFFFF \<le> UCAST(12 \<rightarrow> 32) x << 20; \<not> 0xE0000000 < UCAST(12 \<rightarrow> 32) x << 20; \<not> UCAST(12 \<rightarrow> 32) x << 20 < 0xE0000000\<rbrakk> \<Longrightarrow> UCAST(12 \<rightarrow> 32) x < 2 ^ (LENGTH(32) - 20)
 3. \<And>x xa. \<lbrakk>0xE0000000 \<le> xa; xa \<le> 0xE00FFFFF; UCAST(12 \<rightarrow> 32) x << 20 \<le> xa; xa \<le> 0xFFFFF + (UCAST(12 \<rightarrow> 32) x << 20); xa - 0xFFFFF \<le> UCAST(12 \<rightarrow> 32) x << 20; \<not> 0xE0000000 < UCAST(12 \<rightarrow> 32) x << 20; \<not> UCAST(12 \<rightarrow> 32) x << 20 < 0xE0000000; UCAST(12 \<rightarrow> 32) x << 20 >> 20 = UCAST(12 \<rightarrow> 32) x\<rbrakk> \<Longrightarrow> x = 0xE00
 4. \<And>x xa. \<lbrakk>x \<noteq> 0xE00; 0xE0000000 \<le> xa; xa \<le> 0xE00FFFFF; UCAST(12 \<rightarrow> 32) x << 20 \<le> xa; xa \<le> 0xFFFFF + (UCAST(12 \<rightarrow> 32) x << 20)\<rbrakk> \<Longrightarrow> xa - 0xFFFFF \<le> UCAST(12 \<rightarrow> 32) x << 20 proof (prove)
goal (3 subgoals):
 1. \<And>x xa. \<lbrakk>0xE0000000 \<le> xa; xa \<le> 0xE00FFFFF; UCAST(12 \<rightarrow> 32) x << 20 \<le> xa; xa \<le> 0xFFFFF + (UCAST(12 \<rightarrow> 32) x << 20); xa - 0xFFFFF \<le> UCAST(12 \<rightarrow> 32) x << 20; \<not> 0xE0000000 < UCAST(12 \<rightarrow> 32) x << 20; \<not> UCAST(12 \<rightarrow> 32) x << 20 < 0xE0000000\<rbrakk> \<Longrightarrow> UCAST(12 \<rightarrow> 32) x < 2 ^ (LENGTH(32) - 20)
 2. \<And>x xa. \<lbrakk>0xE0000000 \<le> xa; xa \<le> 0xE00FFFFF; UCAST(12 \<rightarrow> 32) x << 20 \<le> xa; xa \<le> 0xFFFFF + (UCAST(12 \<rightarrow> 32) x << 20); xa - 0xFFFFF \<le> UCAST(12 \<rightarrow> 32) x << 20; \<not> 0xE0000000 < UCAST(12 \<rightarrow> 32) x << 20; \<not> UCAST(12 \<rightarrow> 32) x << 20 < 0xE0000000; UCAST(12 \<rightarrow> 32) x << 20 >> 20 = UCAST(12 \<rightarrow> 32) x\<rbrakk> \<Longrightarrow> x = 0xE00
 3. \<And>x xa. \<lbrakk>x \<noteq> 0xE00; 0xE0000000 \<le> xa; xa \<le> 0xE00FFFFF; UCAST(12 \<rightarrow> 32) x << 20 \<le> xa; xa \<le> 0xFFFFF + (UCAST(12 \<rightarrow> 32) x << 20)\<rbrakk> \<Longrightarrow> xa - 0xFFFFF \<le> UCAST(12 \<rightarrow> 32) x << 20 proof (prove)
goal (2 subgoals):
 1. \<And>x xa. \<lbrakk>0xE0000000 \<le> xa; xa \<le> 0xE00FFFFF; UCAST(12 \<rightarrow> 32) x << 20 \<le> xa; xa \<le> 0xFFFFF + (UCAST(12 \<rightarrow> 32) x << 20); xa - 0xFFFFF \<le> UCAST(12 \<rightarrow> 32) x << 20; \<not> 0xE0000000 < UCAST(12 \<rightarrow> 32) x << 20; \<not> UCAST(12 \<rightarrow> 32) x << 20 < 0xE0000000; UCAST(12 \<rightarrow> 32) x << 20 >> 20 = UCAST(12 \<rightarrow> 32) x\<rbrakk> \<Longrightarrow> x = 0xE00
 2. \<And>x xa. \<lbrakk>x \<noteq> 0xE00; 0xE0000000 \<le> xa; xa \<le> 0xE00FFFFF; UCAST(12 \<rightarrow> 32) x << 20 \<le> xa; xa \<le> 0xFFFFF + (UCAST(12 \<rightarrow> 32) x << 20)\<rbrakk> \<Longrightarrow> xa - 0xFFFFF \<le> UCAST(12 \<rightarrow> 32) x << 20 proof (prove)
goal (2 subgoals):
 1. \<And>x xa. \<lbrakk>0xE0000000 \<le> xa; xa \<le> 0xE00FFFFF; xa - 0xFFFFF \<le> 0xE0000000; UCAST(12 \<rightarrow> 32) x = 0xE00\<rbrakk> \<Longrightarrow> x = 0xE00
 2. \<And>x xa. \<lbrakk>x \<noteq> 0xE00; 0xE0000000 \<le> xa; xa \<le> 0xE00FFFFF; UCAST(12 \<rightarrow> 32) x << 20 \<le> xa; xa \<le> 0xFFFFF + (UCAST(12 \<rightarrow> 32) x << 20)\<rbrakk> \<Longrightarrow> xa - 0xFFFFF \<le> UCAST(12 \<rightarrow> 32) x << 20 proof (prove)
goal (3 subgoals):
 1. \<And>x xa. \<lbrakk>0xE0000000 \<le> xa; xa \<le> 0xE00FFFFF; xa - 0xFFFFF \<le> 0xE0000000; UCAST(12 \<rightarrow> 32) x = 0xE00\<rbrakk> \<Longrightarrow> UCAST(12 \<rightarrow> 32) x = UCAST(12 \<rightarrow> 32) 0xE00
 2. \<And>x xa. \<lbrakk>0xE0000000 \<le> xa; xa \<le> 0xE00FFFFF; xa - 0xFFFFF \<le> 0xE0000000; UCAST(12 \<rightarrow> 32) x = 0xE00\<rbrakk> \<Longrightarrow> LENGTH(12) \<le> LENGTH(32)
 3. \<And>x xa. \<lbrakk>x \<noteq> 0xE00; 0xE0000000 \<le> xa; xa \<le> 0xE00FFFFF; UCAST(12 \<rightarrow> 32) x << 20 \<le> xa; xa \<le> 0xFFFFF + (UCAST(12 \<rightarrow> 32) x << 20)\<rbrakk> \<Longrightarrow> xa - 0xFFFFF \<le> UCAST(12 \<rightarrow> 32) x << 20 proof (prove)
goal (2 subgoals):
 1. \<And>x xa. \<lbrakk>0xE0000000 \<le> xa; xa \<le> 0xE00FFFFF; xa - 0xFFFFF \<le> 0xE0000000; UCAST(12 \<rightarrow> 32) x = 0xE00\<rbrakk> \<Longrightarrow> LENGTH(12) \<le> LENGTH(32)
 2. \<And>x xa. \<lbrakk>x \<noteq> 0xE00; 0xE0000000 \<le> xa; xa \<le> 0xE00FFFFF; UCAST(12 \<rightarrow> 32) x << 20 \<le> xa; xa \<le> 0xFFFFF + (UCAST(12 \<rightarrow> 32) x << 20)\<rbrakk> \<Longrightarrow> xa - 0xFFFFF \<le> UCAST(12 \<rightarrow> 32) x << 20 proof (prove)
goal (1 subgoal):
 1. \<And>x xa. \<lbrakk>x \<noteq> 0xE00; 0xE0000000 \<le> xa; xa \<le> 0xE00FFFFF; UCAST(12 \<rightarrow> 32) x << 20 \<le> xa; xa \<le> 0xFFFFF + (UCAST(12 \<rightarrow> 32) x << 20)\<rbrakk> \<Longrightarrow> xa - 0xFFFFF \<le> UCAST(12 \<rightarrow> 32) x << 20 proof (prove)
goal (4 subgoals):
 1. \<And>x xa. \<lbrakk>x \<noteq> 0xE00; 0xE0000000 \<le> xa; xa \<le> 0xE00FFFFF; UCAST(12 \<rightarrow> 32) x << 20 \<le> xa\<rbrakk> \<Longrightarrow> 0xFFFFF \<le> 0xFFFFF
 2. \<And>x xa. \<lbrakk>x \<noteq> 0xE00; 0xE0000000 \<le> xa; xa \<le> 0xE00FFFFF; UCAST(12 \<rightarrow> 32) x << 20 \<le> xa\<rbrakk> \<Longrightarrow> xa - 0xFFFFF \<le> xa
 3. \<And>x xa. \<lbrakk>x \<noteq> 0xE00; 0xE0000000 \<le> xa; xa \<le> 0xE00FFFFF; UCAST(12 \<rightarrow> 32) x << 20 \<le> xa\<rbrakk> \<Longrightarrow> 0xFFFFF + (UCAST(12 \<rightarrow> 32) x << 20) - 0xFFFFF \<le> 0xFFFFF + (UCAST(12 \<rightarrow> 32) x << 20)
 4. \<And>x xa. \<lbrakk>x \<noteq> 0xE00; 0xE0000000 \<le> xa; xa \<le> 0xE00FFFFF; UCAST(12 \<rightarrow> 32) x << 20 \<le> xa; xa - 0xFFFFF \<le> 0xFFFFF + (UCAST(12 \<rightarrow> 32) x << 20) - 0xFFFFF\<rbrakk> \<Longrightarrow> xa - 0xFFFFF \<le> UCAST(12 \<rightarrow> 32) x << 20 proof (prove)
goal (3 subgoals):
 1. \<And>x xa. \<lbrakk>x \<noteq> 0xE00; 0xE0000000 \<le> xa; xa \<le> 0xE00FFFFF; UCAST(12 \<rightarrow> 32) x << 20 \<le> xa\<rbrakk> \<Longrightarrow> xa - 0xFFFFF \<le> xa
 2. \<And>x xa. \<lbrakk>x \<noteq> 0xE00; 0xE0000000 \<le> xa; xa \<le> 0xE00FFFFF; UCAST(12 \<rightarrow> 32) x << 20 \<le> xa\<rbrakk> \<Longrightarrow> 0xFFFFF + (UCAST(12 \<rightarrow> 32) x << 20) - 0xFFFFF \<le> 0xFFFFF + (UCAST(12 \<rightarrow> 32) x << 20)
 3. \<And>x xa. \<lbrakk>x \<noteq> 0xE00; 0xE0000000 \<le> xa; xa \<le> 0xE00FFFFF; UCAST(12 \<rightarrow> 32) x << 20 \<le> xa; xa - 0xFFFFF \<le> 0xFFFFF + (UCAST(12 \<rightarrow> 32) x << 20) - 0xFFFFF\<rbrakk> \<Longrightarrow> xa - 0xFFFFF \<le> UCAST(12 \<rightarrow> 32) x << 20 proof (prove)
goal (3 subgoals):
 1. \<And>x xa. \<lbrakk>x \<noteq> 0xE00; 0xE0000000 \<le> xa; xa \<le> 0xE00FFFFF; UCAST(12 \<rightarrow> 32) x << 20 \<le> xa\<rbrakk> \<Longrightarrow> 0xFFFFF \<le> xa
 2. \<And>x xa. \<lbrakk>x \<noteq> 0xE00; 0xE0000000 \<le> xa; xa \<le> 0xE00FFFFF; UCAST(12 \<rightarrow> 32) x << 20 \<le> xa\<rbrakk> \<Longrightarrow> 0xFFFFF + (UCAST(12 \<rightarrow> 32) x << 20) - 0xFFFFF \<le> 0xFFFFF + (UCAST(12 \<rightarrow> 32) x << 20)
 3. \<And>x xa. \<lbrakk>x \<noteq> 0xE00; 0xE0000000 \<le> xa; xa \<le> 0xE00FFFFF; UCAST(12 \<rightarrow> 32) x << 20 \<le> xa; xa - 0xFFFFF \<le> 0xFFFFF + (UCAST(12 \<rightarrow> 32) x << 20) - 0xFFFFF\<rbrakk> \<Longrightarrow> xa - 0xFFFFF \<le> UCAST(12 \<rightarrow> 32) x << 20 proof (prove)
goal (3 subgoals):
 1. \<And>x xa. \<lbrakk>x \<noteq> 0xE00; 0xE0000000 \<le> xa; xa \<le> 0xE00FFFFF; UCAST(12 \<rightarrow> 32) x << 20 \<le> xa\<rbrakk> \<Longrightarrow> 0xFFFFF \<le> 0xE0000000
 2. \<And>x xa. \<lbrakk>x \<noteq> 0xE00; 0xE0000000 \<le> xa; xa \<le> 0xE00FFFFF; UCAST(12 \<rightarrow> 32) x << 20 \<le> xa\<rbrakk> \<Longrightarrow> 0xFFFFF + (UCAST(12 \<rightarrow> 32) x << 20) - 0xFFFFF \<le> 0xFFFFF + (UCAST(12 \<rightarrow> 32) x << 20)
 3. \<And>x xa. \<lbrakk>x \<noteq> 0xE00; 0xE0000000 \<le> xa; xa \<le> 0xE00FFFFF; UCAST(12 \<rightarrow> 32) x << 20 \<le> xa; xa - 0xFFFFF \<le> 0xFFFFF + (UCAST(12 \<rightarrow> 32) x << 20) - 0xFFFFF\<rbrakk> \<Longrightarrow> xa - 0xFFFFF \<le> UCAST(12 \<rightarrow> 32) x << 20 proof (prove)
goal (2 subgoals):
 1. \<And>x xa. \<lbrakk>x \<noteq> 0xE00; 0xE0000000 \<le> xa; xa \<le> 0xE00FFFFF; UCAST(12 \<rightarrow> 32) x << 20 \<le> xa\<rbrakk> \<Longrightarrow> 0xFFFFF + (UCAST(12 \<rightarrow> 32) x << 20) - 0xFFFFF \<le> 0xFFFFF + (UCAST(12 \<rightarrow> 32) x << 20)
 2. \<And>x xa. \<lbrakk>x \<noteq> 0xE00; 0xE0000000 \<le> xa; xa \<le> 0xE00FFFFF; UCAST(12 \<rightarrow> 32) x << 20 \<le> xa; xa - 0xFFFFF \<le> 0xFFFFF + (UCAST(12 \<rightarrow> 32) x << 20) - 0xFFFFF\<rbrakk> \<Longrightarrow> xa - 0xFFFFF \<le> UCAST(12 \<rightarrow> 32) x << 20 proof (prove)
goal (2 subgoals):
 1. \<And>x xa. \<lbrakk>x \<noteq> 0xE00; 0xE0000000 \<le> xa; xa \<le> 0xE00FFFFF; UCAST(12 \<rightarrow> 32) x << 20 \<le> xa\<rbrakk> \<Longrightarrow> UCAST(12 \<rightarrow> 32) x << 20 \<le> (UCAST(12 \<rightarrow> 32) x << 20) + 0xFFFFF
 2. \<And>x xa. \<lbrakk>x \<noteq> 0xE00; 0xE0000000 \<le> xa; xa \<le> 0xE00FFFFF; UCAST(12 \<rightarrow> 32) x << 20 \<le> xa; xa - 0xFFFFF \<le> 0xFFFFF + (UCAST(12 \<rightarrow> 32) x << 20) - 0xFFFFF\<rbrakk> \<Longrightarrow> xa - 0xFFFFF \<le> UCAST(12 \<rightarrow> 32) x << 20 proof (prove)
goal (2 subgoals):
 1. \<And>x xa. \<lbrakk>x \<noteq> 0xE00; 0xE0000000 \<le> xa; xa \<le> 0xE00FFFFF; UCAST(12 \<rightarrow> 32) x << 20 \<le> xa\<rbrakk> \<Longrightarrow> UCAST(12 \<rightarrow> 32) x << 20 < - 0xFFFFF
 2. \<And>x xa. \<lbrakk>x \<noteq> 0xE00; 0xE0000000 \<le> xa; xa \<le> 0xE00FFFFF; UCAST(12 \<rightarrow> 32) x << 20 \<le> xa; xa - 0xFFFFF \<le> 0xFFFFF + (UCAST(12 \<rightarrow> 32) x << 20) - 0xFFFFF\<rbrakk> \<Longrightarrow> xa - 0xFFFFF \<le> UCAST(12 \<rightarrow> 32) x << 20 proof (prove)
goal (2 subgoals):
 1. \<And>x xa. \<lbrakk>x \<noteq> 0xE00; 0xE0000000 \<le> xa; xa \<le> 0xE00FFFFF; UCAST(12 \<rightarrow> 32) x << 20 \<le> xa\<rbrakk> \<Longrightarrow> UCAST(12 \<rightarrow> 32) x << 20 < 0xFFF00001
 2. \<And>x xa. \<lbrakk>x \<noteq> 0xE00; 0xE0000000 \<le> xa; xa \<le> 0xE00FFFFF; UCAST(12 \<rightarrow> 32) x << 20 \<le> xa; xa - 0xFFFFF \<le> 0xFFFFF + (UCAST(12 \<rightarrow> 32) x << 20) - 0xFFFFF\<rbrakk> \<Longrightarrow> xa - 0xFFFFF \<le> UCAST(12 \<rightarrow> 32) x << 20 proof (prove)
goal (2 subgoals):
 1. \<And>x xa. \<lbrakk>x \<noteq> 0xE00; 0xE0000000 \<le> xa; xa \<le> 0xE00FFFFF; UCAST(12 \<rightarrow> 32) x << 20 \<le> 0xE00FFFFF\<rbrakk> \<Longrightarrow> UCAST(12 \<rightarrow> 32) x << 20 < 0xFFF00001
 2. \<And>x xa. \<lbrakk>x \<noteq> 0xE00; 0xE0000000 \<le> xa; xa \<le> 0xE00FFFFF; UCAST(12 \<rightarrow> 32) x << 20 \<le> xa; xa - 0xFFFFF \<le> 0xFFFFF + (UCAST(12 \<rightarrow> 32) x << 20) - 0xFFFFF\<rbrakk> \<Longrightarrow> xa - 0xFFFFF \<le> UCAST(12 \<rightarrow> 32) x << 20 proof (prove)
goal (1 subgoal):
 1. \<And>x xa. \<lbrakk>x \<noteq> 0xE00; 0xE0000000 \<le> xa; xa \<le> 0xE00FFFFF; UCAST(12 \<rightarrow> 32) x << 20 \<le> xa; xa - 0xFFFFF \<le> 0xFFFFF + (UCAST(12 \<rightarrow> 32) x << 20) - 0xFFFFF\<rbrakk> \<Longrightarrow> xa - 0xFFFFF \<le> UCAST(12 \<rightarrow> 32) x << 20 proof (prove)
goal:
No subgoals!