theory Eval_CAMKES_CDL

lemma Collect_asid_high__eval_helper:
  "asid_high_bits_of ` {asid. fst (transform_asid asid) = asid_high \<and> asid \<noteq> 0} =
   (if asid_high < 2^asid_high_bits then {of_nat asid_high} else {})" 
  (* cleanup... *)
   apply (case_tac "asid_high < 2^asid_high_bits") prefer 2 apply (clarsimp simp: transform_asid_def asid_high_bits_of_def[abs_def]) apply (erule contrapos_np) apply (subst arg_cong[where f="(<) _"]) prefer 2 apply (rule unat_lt2p) apply (simp add: asid_high_bits_def) apply (simp add: transform_asid_def asid_high_bits_of_def[abs_def]) apply (rule set_eqI) apply (rule iffI) apply clarsimp apply (clarsimp simp: Collect_conj_eq image_iff) apply (rule_tac x="(of_nat asid_high << asid_low_bits) + 1" in bexI) apply (subst add.commute, subst shiftr_irrelevant) apply (clarsimp simp: asid_low_bits_def asid_high_bits_def) apply (clarsimp simp: is_aligned_shift) apply (subst shiftl_shiftr_id) apply (clarsimp simp: asid_low_bits_def asid_high_bits_def) apply (clarsimp simp: asid_low_bits_def asid_high_bits_def word_of_nat_less) apply (subst ucast_of_nat_small) apply (clarsimp simp: asid_high_bits_def) apply simp apply clarsimp apply (rule conjI) apply (clarsimp simp: unat_ucast_eq_unat_and_mask) apply (subst add.commute, subst shiftr_irrelevant) apply (clarsimp simp: asid_low_bits_def asid_high_bits_def) apply (clarsimp simp: is_aligned_shift) apply (subst shiftl_shiftr_id) apply (clarsimp simp: asid_low_bits_def asid_high_bits_def) apply (clarsimp simp: asid_low_bits_def asid_high_bits_def word_of_nat_less) apply (fold asid_high_bits_def) apply (subst less_mask_eq) apply (clarsimp simp: asid_high_bits_def word_of_nat_less) apply (rule unat_of_nat_eq) apply (clarsimp simp: asid_high_bits_def) apply (rule less_is_non_zero_p1[where k="2^asid_high_bits << asid_low_bits"]) apply (simp only: shiftl_t2n) apply (subst mult.commute, subst mult.commute, rule word_mult_less_mono1) apply (clarsimp simp: asid_high_bits_def word_of_nat_less) apply (clarsimp simp: asid_low_bits_def) apply (clarsimp simp: asid_low_bits_def asid_high_bits_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. asid_high_bits_of ` {asid. fst (transform_asid asid) = asid_high \<and> asid \<noteq> 0} = (if asid_high < 2 ^ local.asid_high_bits then {word_of_nat asid_high} else {}) proof (prove)
goal (1 subgoal):
 1. asid_high_bits_of ` {asid. fst (transform_asid asid) = asid_high \<and> asid \<noteq> 0} = (if asid_high < 2 ^ local.asid_high_bits then {word_of_nat asid_high} else {}) proof (prove)
goal (2 subgoals):
 1. asid_high < 2 ^ local.asid_high_bits \<Longrightarrow> asid_high_bits_of ` {asid. fst (transform_asid asid) = asid_high \<and> asid \<noteq> 0} = (if asid_high < 2 ^ local.asid_high_bits then {word_of_nat asid_high} else {})
 2. \<not> asid_high < 2 ^ local.asid_high_bits \<Longrightarrow> asid_high_bits_of ` {asid. fst (transform_asid asid) = asid_high \<and> asid \<noteq> 0} = (if asid_high < 2 ^ local.asid_high_bits then {word_of_nat asid_high} else {}) proof (prove)
goal (2 subgoals):
 1. \<not> asid_high < 2 ^ local.asid_high_bits \<Longrightarrow> asid_high_bits_of ` {asid. fst (transform_asid asid) = asid_high \<and> asid \<noteq> 0} = (if asid_high < 2 ^ local.asid_high_bits then {word_of_nat asid_high} else {})
 2. asid_high < 2 ^ local.asid_high_bits \<Longrightarrow> asid_high_bits_of ` {asid. fst (transform_asid asid) = asid_high \<and> asid \<noteq> 0} = (if asid_high < 2 ^ local.asid_high_bits then {word_of_nat asid_high} else {}) proof (prove)
goal (2 subgoals):
 1. \<And>x. \<lbrakk>\<not> unat (UCAST(32 \<rightarrow> 7) (x >> local.asid_low_bits)) < 2 ^ local.asid_high_bits; asid_high = unat (UCAST(32 \<rightarrow> 7) (x >> local.asid_low_bits))\<rbrakk> \<Longrightarrow> x = 0
 2. asid_high < 2 ^ local.asid_high_bits \<Longrightarrow> asid_high_bits_of ` {asid. fst (transform_asid asid) = asid_high \<and> asid \<noteq> 0} = (if asid_high < 2 ^ local.asid_high_bits then {word_of_nat asid_high} else {}) proof (prove)
goal (2 subgoals):
 1. \<And>x. \<lbrakk>asid_high = unat (UCAST(32 \<rightarrow> 7) (x >> local.asid_low_bits)); x \<noteq> 0\<rbrakk> \<Longrightarrow> unat (UCAST(32 \<rightarrow> 7) (x >> local.asid_low_bits)) < 2 ^ local.asid_high_bits
 2. asid_high < 2 ^ local.asid_high_bits \<Longrightarrow> asid_high_bits_of ` {asid. fst (transform_asid asid) = asid_high \<and> asid \<noteq> 0} = (if asid_high < 2 ^ local.asid_high_bits then {word_of_nat asid_high} else {}) proof (prove)
goal (3 subgoals):
 1. \<And>x. \<lbrakk>asid_high = unat (UCAST(32 \<rightarrow> 7) (x >> local.asid_low_bits)); x \<noteq> 0\<rbrakk> \<Longrightarrow> 2 ^ local.asid_high_bits = ?y16 x
 2. \<And>x. \<lbrakk>asid_high = unat (UCAST(32 \<rightarrow> 7) (x >> local.asid_low_bits)); x \<noteq> 0\<rbrakk> \<Longrightarrow> unat (UCAST(32 \<rightarrow> 7) (x >> local.asid_low_bits)) < ?y16 x
 3. asid_high < 2 ^ local.asid_high_bits \<Longrightarrow> asid_high_bits_of ` {asid. fst (transform_asid asid) = asid_high \<and> asid \<noteq> 0} = (if asid_high < 2 ^ local.asid_high_bits then {word_of_nat asid_high} else {}) proof (prove)
goal (3 subgoals):
 1. \<And>x. \<lbrakk>asid_high = unat (UCAST(32 \<rightarrow> 7) (x >> local.asid_low_bits)); x \<noteq> 0\<rbrakk> \<Longrightarrow> unat (UCAST(32 \<rightarrow> 7) (x >> local.asid_low_bits)) < ?y16 x
 2. \<And>x. \<lbrakk>asid_high = unat (UCAST(32 \<rightarrow> 7) (x >> local.asid_low_bits)); x \<noteq> 0\<rbrakk> \<Longrightarrow> 2 ^ local.asid_high_bits = ?y16 x
 3. asid_high < 2 ^ local.asid_high_bits \<Longrightarrow> asid_high_bits_of ` {asid. fst (transform_asid asid) = asid_high \<and> asid \<noteq> 0} = (if asid_high < 2 ^ local.asid_high_bits then {word_of_nat asid_high} else {}) proof (prove)
goal (2 subgoals):
 1. \<And>x. \<lbrakk>asid_high = unat (UCAST(32 \<rightarrow> 7) (x >> local.asid_low_bits)); x \<noteq> 0\<rbrakk> \<Longrightarrow> 2 ^ local.asid_high_bits = 2 ^ LENGTH(7)
 2. asid_high < 2 ^ local.asid_high_bits \<Longrightarrow> asid_high_bits_of ` {asid. fst (transform_asid asid) = asid_high \<and> asid \<noteq> 0} = (if asid_high < 2 ^ local.asid_high_bits then {word_of_nat asid_high} else {}) proof (prove)
goal (1 subgoal):
 1. asid_high < 2 ^ local.asid_high_bits \<Longrightarrow> asid_high_bits_of ` {asid. fst (transform_asid asid) = asid_high \<and> asid \<noteq> 0} = (if asid_high < 2 ^ local.asid_high_bits then {word_of_nat asid_high} else {}) proof (prove)
goal (1 subgoal):
 1. asid_high < 2 ^ local.asid_high_bits \<Longrightarrow> (\<lambda>x. UCAST(32 \<rightarrow> 7) (x >> local.asid_low_bits)) ` {asid. unat (UCAST(32 \<rightarrow> 7) (asid >> local.asid_low_bits)) = asid_high \<and> asid \<noteq> 0} = {word_of_nat asid_high} proof (prove)
goal (1 subgoal):
 1. \<And>x. asid_high < 2 ^ local.asid_high_bits \<Longrightarrow> (x \<in> (\<lambda>x. UCAST(32 \<rightarrow> 7) (x >> local.asid_low_bits)) ` {asid. unat (UCAST(32 \<rightarrow> 7) (asid >> local.asid_low_bits)) = asid_high \<and> asid \<noteq> 0}) = (x \<in> {word_of_nat asid_high}) proof (prove)
goal (2 subgoals):
 1. \<And>x. \<lbrakk>asid_high < 2 ^ local.asid_high_bits; x \<in> (\<lambda>x. UCAST(32 \<rightarrow> 7) (x >> local.asid_low_bits)) ` {asid. unat (UCAST(32 \<rightarrow> 7) (asid >> local.asid_low_bits)) = asid_high \<and> asid \<noteq> 0}\<rbrakk> \<Longrightarrow> x \<in> {word_of_nat asid_high}
 2. \<And>x. \<lbrakk>asid_high < 2 ^ local.asid_high_bits; x \<in> {word_of_nat asid_high}\<rbrakk> \<Longrightarrow> x \<in> (\<lambda>x. UCAST(32 \<rightarrow> 7) (x >> local.asid_low_bits)) ` {asid. unat (UCAST(32 \<rightarrow> 7) (asid >> local.asid_low_bits)) = asid_high \<and> asid \<noteq> 0} proof (prove)
goal (1 subgoal):
 1. \<And>x. \<lbrakk>asid_high < 2 ^ local.asid_high_bits; x \<in> {word_of_nat asid_high}\<rbrakk> \<Longrightarrow> x \<in> (\<lambda>x. UCAST(32 \<rightarrow> 7) (x >> local.asid_low_bits)) ` {asid. unat (UCAST(32 \<rightarrow> 7) (asid >> local.asid_low_bits)) = asid_high \<and> asid \<noteq> 0} proof (prove)
goal (1 subgoal):
 1. asid_high < 2 ^ local.asid_high_bits \<Longrightarrow> \<exists>x\<in>{asid. unat (UCAST(32 \<rightarrow> 7) (asid >> local.asid_low_bits)) = asid_high} \<inter> {asid. asid \<noteq> 0}. word_of_nat asid_high = UCAST(32 \<rightarrow> 7) (x >> local.asid_low_bits) proof (prove)
goal (2 subgoals):
 1. asid_high < 2 ^ local.asid_high_bits \<Longrightarrow> word_of_nat asid_high = UCAST(32 \<rightarrow> 7) ((word_of_nat asid_high << local.asid_low_bits) + 1 >> local.asid_low_bits)
 2. asid_high < 2 ^ local.asid_high_bits \<Longrightarrow> (word_of_nat asid_high << local.asid_low_bits) + 1 \<in> {asid. unat (UCAST(32 \<rightarrow> 7) (asid >> local.asid_low_bits)) = asid_high} \<inter> {asid. asid \<noteq> 0} proof (prove)
goal (4 subgoals):
 1. asid_high < 2 ^ local.asid_high_bits \<Longrightarrow> 1 < 2 ^ local.asid_low_bits
 2. asid_high < 2 ^ local.asid_high_bits \<Longrightarrow> is_aligned (word_of_nat asid_high << local.asid_low_bits) local.asid_low_bits
 3. asid_high < 2 ^ local.asid_high_bits \<Longrightarrow> word_of_nat asid_high = UCAST(32 \<rightarrow> 7) (word_of_nat asid_high << local.asid_low_bits >> local.asid_low_bits)
 4. asid_high < 2 ^ local.asid_high_bits \<Longrightarrow> (word_of_nat asid_high << local.asid_low_bits) + 1 \<in> {asid. unat (UCAST(32 \<rightarrow> 7) (asid >> local.asid_low_bits)) = asid_high} \<inter> {asid. asid \<noteq> 0} proof (prove)
goal (3 subgoals):
 1. asid_high < 2 ^ local.asid_high_bits \<Longrightarrow> is_aligned (word_of_nat asid_high << local.asid_low_bits) local.asid_low_bits
 2. asid_high < 2 ^ local.asid_high_bits \<Longrightarrow> word_of_nat asid_high = UCAST(32 \<rightarrow> 7) (word_of_nat asid_high << local.asid_low_bits >> local.asid_low_bits)
 3. asid_high < 2 ^ local.asid_high_bits \<Longrightarrow> (word_of_nat asid_high << local.asid_low_bits) + 1 \<in> {asid. unat (UCAST(32 \<rightarrow> 7) (asid >> local.asid_low_bits)) = asid_high} \<inter> {asid. asid \<noteq> 0} proof (prove)
goal (2 subgoals):
 1. asid_high < 2 ^ local.asid_high_bits \<Longrightarrow> word_of_nat asid_high = UCAST(32 \<rightarrow> 7) (word_of_nat asid_high << local.asid_low_bits >> local.asid_low_bits)
 2. asid_high < 2 ^ local.asid_high_bits \<Longrightarrow> (word_of_nat asid_high << local.asid_low_bits) + 1 \<in> {asid. unat (UCAST(32 \<rightarrow> 7) (asid >> local.asid_low_bits)) = asid_high} \<inter> {asid. asid \<noteq> 0} proof (prove)
goal (4 subgoals):
 1. asid_high < 2 ^ local.asid_high_bits \<Longrightarrow> local.asid_low_bits < LENGTH(32)
 2. asid_high < 2 ^ local.asid_high_bits \<Longrightarrow> word_of_nat asid_high < 2 ^ (LENGTH(32) - local.asid_low_bits)
 3. asid_high < 2 ^ local.asid_high_bits \<Longrightarrow> word_of_nat asid_high = UCAST(32 \<rightarrow> 7) (word_of_nat asid_high)
 4. asid_high < 2 ^ local.asid_high_bits \<Longrightarrow> (word_of_nat asid_high << local.asid_low_bits) + 1 \<in> {asid. unat (UCAST(32 \<rightarrow> 7) (asid >> local.asid_low_bits)) = asid_high} \<inter> {asid. asid \<noteq> 0} proof (prove)
goal (3 subgoals):
 1. asid_high < 2 ^ local.asid_high_bits \<Longrightarrow> word_of_nat asid_high < 2 ^ (LENGTH(32) - local.asid_low_bits)
 2. asid_high < 2 ^ local.asid_high_bits \<Longrightarrow> word_of_nat asid_high = UCAST(32 \<rightarrow> 7) (word_of_nat asid_high)
 3. asid_high < 2 ^ local.asid_high_bits \<Longrightarrow> (word_of_nat asid_high << local.asid_low_bits) + 1 \<in> {asid. unat (UCAST(32 \<rightarrow> 7) (asid >> local.asid_low_bits)) = asid_high} \<inter> {asid. asid \<noteq> 0} proof (prove)
goal (2 subgoals):
 1. asid_high < 2 ^ local.asid_high_bits \<Longrightarrow> word_of_nat asid_high = UCAST(32 \<rightarrow> 7) (word_of_nat asid_high)
 2. asid_high < 2 ^ local.asid_high_bits \<Longrightarrow> (word_of_nat asid_high << local.asid_low_bits) + 1 \<in> {asid. unat (UCAST(32 \<rightarrow> 7) (asid >> local.asid_low_bits)) = asid_high} \<inter> {asid. asid \<noteq> 0} proof (prove)
goal (3 subgoals):
 1. asid_high < 2 ^ local.asid_high_bits \<Longrightarrow> asid_high < 2 ^ LENGTH(32)
 2. asid_high < 2 ^ local.asid_high_bits \<Longrightarrow> word_of_nat asid_high = word_of_nat asid_high
 3. asid_high < 2 ^ local.asid_high_bits \<Longrightarrow> (word_of_nat asid_high << local.asid_low_bits) + 1 \<in> {asid. unat (UCAST(32 \<rightarrow> 7) (asid >> local.asid_low_bits)) = asid_high} \<inter> {asid. asid \<noteq> 0} proof (prove)
goal (2 subgoals):
 1. asid_high < 2 ^ local.asid_high_bits \<Longrightarrow> word_of_nat asid_high = word_of_nat asid_high
 2. asid_high < 2 ^ local.asid_high_bits \<Longrightarrow> (word_of_nat asid_high << local.asid_low_bits) + 1 \<in> {asid. unat (UCAST(32 \<rightarrow> 7) (asid >> local.asid_low_bits)) = asid_high} \<inter> {asid. asid \<noteq> 0} proof (prove)
goal (1 subgoal):
 1. asid_high < 2 ^ local.asid_high_bits \<Longrightarrow> (word_of_nat asid_high << local.asid_low_bits) + 1 \<in> {asid. unat (UCAST(32 \<rightarrow> 7) (asid >> local.asid_low_bits)) = asid_high} \<inter> {asid. asid \<noteq> 0} proof (prove)
goal (1 subgoal):
 1. asid_high < 2 ^ local.asid_high_bits \<Longrightarrow> unat (UCAST(32 \<rightarrow> 7) ((word_of_nat asid_high << local.asid_low_bits) + 1 >> local.asid_low_bits)) = asid_high \<and> (word_of_nat asid_high << local.asid_low_bits) + 1 \<noteq> 0 proof (prove)
goal (2 subgoals):
 1. asid_high < 2 ^ local.asid_high_bits \<Longrightarrow> unat (UCAST(32 \<rightarrow> 7) ((word_of_nat asid_high << local.asid_low_bits) + 1 >> local.asid_low_bits)) = asid_high
 2. asid_high < 2 ^ local.asid_high_bits \<Longrightarrow> (word_of_nat asid_high << local.asid_low_bits) + 1 \<noteq> 0 proof (prove)
goal (2 subgoals):
 1. asid_high < 2 ^ local.asid_high_bits \<Longrightarrow> unat (((word_of_nat asid_high << local.asid_low_bits) + 1 >> local.asid_low_bits) && mask 7) = asid_high
 2. asid_high < 2 ^ local.asid_high_bits \<Longrightarrow> (word_of_nat asid_high << local.asid_low_bits) + 1 \<noteq> 0 proof (prove)
goal (4 subgoals):
 1. asid_high < 2 ^ local.asid_high_bits \<Longrightarrow> 1 < 2 ^ local.asid_low_bits
 2. asid_high < 2 ^ local.asid_high_bits \<Longrightarrow> is_aligned (word_of_nat asid_high << local.asid_low_bits) local.asid_low_bits
 3. asid_high < 2 ^ local.asid_high_bits \<Longrightarrow> unat ((word_of_nat asid_high << local.asid_low_bits >> local.asid_low_bits) && mask 7) = asid_high
 4. asid_high < 2 ^ local.asid_high_bits \<Longrightarrow> (word_of_nat asid_high << local.asid_low_bits) + 1 \<noteq> 0 proof (prove)
goal (3 subgoals):
 1. asid_high < 2 ^ local.asid_high_bits \<Longrightarrow> is_aligned (word_of_nat asid_high << local.asid_low_bits) local.asid_low_bits
 2. asid_high < 2 ^ local.asid_high_bits \<Longrightarrow> unat ((word_of_nat asid_high << local.asid_low_bits >> local.asid_low_bits) && mask 7) = asid_high
 3. asid_high < 2 ^ local.asid_high_bits \<Longrightarrow> (word_of_nat asid_high << local.asid_low_bits) + 1 \<noteq> 0 proof (prove)
goal (2 subgoals):
 1. asid_high < 2 ^ local.asid_high_bits \<Longrightarrow> unat ((word_of_nat asid_high << local.asid_low_bits >> local.asid_low_bits) && mask 7) = asid_high
 2. asid_high < 2 ^ local.asid_high_bits \<Longrightarrow> (word_of_nat asid_high << local.asid_low_bits) + 1 \<noteq> 0 proof (prove)
goal (4 subgoals):
 1. asid_high < 2 ^ local.asid_high_bits \<Longrightarrow> local.asid_low_bits < LENGTH(32)
 2. asid_high < 2 ^ local.asid_high_bits \<Longrightarrow> word_of_nat asid_high < 2 ^ (LENGTH(32) - local.asid_low_bits)
 3. asid_high < 2 ^ local.asid_high_bits \<Longrightarrow> unat (word_of_nat asid_high && mask 7) = asid_high
 4. asid_high < 2 ^ local.asid_high_bits \<Longrightarrow> (word_of_nat asid_high << local.asid_low_bits) + 1 \<noteq> 0 proof (prove)
goal (3 subgoals):
 1. asid_high < 2 ^ local.asid_high_bits \<Longrightarrow> word_of_nat asid_high < 2 ^ (LENGTH(32) - local.asid_low_bits)
 2. asid_high < 2 ^ local.asid_high_bits \<Longrightarrow> unat (word_of_nat asid_high && mask 7) = asid_high
 3. asid_high < 2 ^ local.asid_high_bits \<Longrightarrow> (word_of_nat asid_high << local.asid_low_bits) + 1 \<noteq> 0 proof (prove)
goal (2 subgoals):
 1. asid_high < 2 ^ local.asid_high_bits \<Longrightarrow> unat (word_of_nat asid_high && mask 7) = asid_high
 2. asid_high < 2 ^ local.asid_high_bits \<Longrightarrow> (word_of_nat asid_high << local.asid_low_bits) + 1 \<noteq> 0 proof (prove)
goal (2 subgoals):
 1. asid_high < 2 ^ local.asid_high_bits \<Longrightarrow> unat (word_of_nat asid_high && mask local.asid_high_bits) = asid_high
 2. asid_high < 2 ^ local.asid_high_bits \<Longrightarrow> (word_of_nat asid_high << local.asid_low_bits) + 1 \<noteq> 0 proof (prove)
goal (3 subgoals):
 1. asid_high < 2 ^ local.asid_high_bits \<Longrightarrow> word_of_nat asid_high < 2 ^ local.asid_high_bits
 2. asid_high < 2 ^ local.asid_high_bits \<Longrightarrow> unat (word_of_nat asid_high) = asid_high
 3. asid_high < 2 ^ local.asid_high_bits \<Longrightarrow> (word_of_nat asid_high << local.asid_low_bits) + 1 \<noteq> 0 proof (prove)
goal (2 subgoals):
 1. asid_high < 2 ^ local.asid_high_bits \<Longrightarrow> unat (word_of_nat asid_high) = asid_high
 2. asid_high < 2 ^ local.asid_high_bits \<Longrightarrow> (word_of_nat asid_high << local.asid_low_bits) + 1 \<noteq> 0 proof (prove)
goal (2 subgoals):
 1. asid_high < 2 ^ local.asid_high_bits \<Longrightarrow> asid_high < 2 ^ LENGTH(32)
 2. asid_high < 2 ^ local.asid_high_bits \<Longrightarrow> (word_of_nat asid_high << local.asid_low_bits) + 1 \<noteq> 0 proof (prove)
goal (1 subgoal):
 1. asid_high < 2 ^ local.asid_high_bits \<Longrightarrow> (word_of_nat asid_high << local.asid_low_bits) + 1 \<noteq> 0 proof (prove)
goal (1 subgoal):
 1. asid_high < 2 ^ local.asid_high_bits \<Longrightarrow> word_of_nat asid_high << local.asid_low_bits < 2 ^ local.asid_high_bits << local.asid_low_bits proof (prove)
goal (1 subgoal):
 1. asid_high < 2 ^ local.asid_high_bits \<Longrightarrow> 2 ^ local.asid_low_bits * word_of_nat asid_high < 2 ^ local.asid_low_bits * 2 ^ local.asid_high_bits proof (prove)
goal (3 subgoals):
 1. asid_high < 2 ^ local.asid_high_bits \<Longrightarrow> word_of_nat asid_high < 2 ^ local.asid_high_bits
 2. asid_high < 2 ^ local.asid_high_bits \<Longrightarrow> 0 < 2 ^ local.asid_low_bits
 3. asid_high < 2 ^ local.asid_high_bits \<Longrightarrow> unat (2 ^ local.asid_high_bits) * unat (2 ^ local.asid_low_bits) < 2 ^ LENGTH(32) proof (prove)
goal (2 subgoals):
 1. asid_high < 2 ^ local.asid_high_bits \<Longrightarrow> 0 < 2 ^ local.asid_low_bits
 2. asid_high < 2 ^ local.asid_high_bits \<Longrightarrow> unat (2 ^ local.asid_high_bits) * unat (2 ^ local.asid_low_bits) < 2 ^ LENGTH(32) proof (prove)
goal (1 subgoal):
 1. asid_high < 2 ^ local.asid_high_bits \<Longrightarrow> unat (2 ^ local.asid_high_bits) * unat (2 ^ local.asid_low_bits) < 2 ^ LENGTH(32) proof (prove)
goal:
No subgoals!