theory Untyped_DR

lemma distinct_retype_addrs:
  "\<lbrakk>type = Structures_A.Untyped \<longrightarrow> untyped_min_bits \<le> us;
    range_cover ptr sz (obj_bits_api type us) n\<rbrakk>
    \<Longrightarrow> distinct (retype_addrs ptr type n us)" supply untyped_min_bits_def[simp] apply (clarsimp simp:retype_addrs_def distinct_map ptr_add_def inj_on_def) apply (simp only: shiftl_t2n[symmetric, simplified field_simps, simplified]) apply (drule shiftl_inj_if) apply (rule shiftl_shiftr_id) apply (simp add:range_cover_def) apply (rule word_of_nat_less) apply (subst unat_power_lower) apply (rule diff_less) apply (cut_tac obj_bits_bound4[where us = us and type = type]) apply simp apply simp apply (simp add:word_bits_def) apply (erule Retype_AI.range_cover.range_cover_le_n_less(2)) apply simp apply (rule shiftl_shiftr_id) apply (simp add:range_cover_def) apply (rule word_of_nat_less) apply (subst unat_power_lower) apply (rule diff_less) apply (cut_tac obj_bits_bound4[where us = us and type = type]) apply simp apply simp apply (simp add:word_bits_def) apply (erule Retype_AI.range_cover.range_cover_le_n_less(2)) apply simp apply (rule of_nat_inj[where 'a=32, THEN iffD1]) apply (simp add:range_cover.range_cover_le_n_less[where 'a=32, simplified])+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>type = apiobject_type.Untyped \<longrightarrow> untyped_min_bits \<le> us; range_cover ptr sz (obj_bits_api type us) n\<rbrakk> \<Longrightarrow> distinct (retype_addrs ptr type n us) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>type = apiobject_type.Untyped \<longrightarrow> untyped_min_bits \<le> us; range_cover ptr sz (obj_bits_api type us) n\<rbrakk> \<Longrightarrow> distinct (retype_addrs ptr type n us) proof (prove)
goal (1 subgoal):
 1. \<And>x y. \<lbrakk>type = apiobject_type.Untyped \<longrightarrow> 4 \<le> us; range_cover ptr sz (obj_bits_api type us) n; x < n; y < n; word_of_nat x * 2 ^ obj_bits_api type us = word_of_nat y * 2 ^ obj_bits_api type us\<rbrakk> \<Longrightarrow> x = y proof (prove)
goal (1 subgoal):
 1. \<And>x y. \<lbrakk>type = apiobject_type.Untyped \<longrightarrow> 4 \<le> us; range_cover ptr sz (obj_bits_api type us) n; x < n; y < n; word_of_nat x << obj_bits_api type us = word_of_nat y << obj_bits_api type us\<rbrakk> \<Longrightarrow> x = y proof (prove)
goal (3 subgoals):
 1. \<And>x y. \<lbrakk>type = apiobject_type.Untyped \<longrightarrow> 4 \<le> us; range_cover ptr sz (obj_bits_api type us) n; x < n; y < n\<rbrakk> \<Longrightarrow> word_of_nat x << obj_bits_api type us >> obj_bits_api type us = word_of_nat x
 2. \<And>x y. \<lbrakk>type = apiobject_type.Untyped \<longrightarrow> 4 \<le> us; range_cover ptr sz (obj_bits_api type us) n; x < n; y < n\<rbrakk> \<Longrightarrow> word_of_nat y << obj_bits_api type us >> obj_bits_api type us = word_of_nat y
 3. \<And>x y. \<lbrakk>type = apiobject_type.Untyped \<longrightarrow> 4 \<le> us; range_cover ptr sz (obj_bits_api type us) n; x < n; y < n; word_of_nat x = word_of_nat y\<rbrakk> \<Longrightarrow> x = y proof (prove)
goal (4 subgoals):
 1. \<And>x y. \<lbrakk>type = apiobject_type.Untyped \<longrightarrow> 4 \<le> us; range_cover ptr sz (obj_bits_api type us) n; x < n; y < n\<rbrakk> \<Longrightarrow> obj_bits_api type us < LENGTH(32)
 2. \<And>x y. \<lbrakk>type = apiobject_type.Untyped \<longrightarrow> 4 \<le> us; range_cover ptr sz (obj_bits_api type us) n; x < n; y < n\<rbrakk> \<Longrightarrow> word_of_nat x < 2 ^ (LENGTH(32) - obj_bits_api type us)
 3. \<And>x y. \<lbrakk>type = apiobject_type.Untyped \<longrightarrow> 4 \<le> us; range_cover ptr sz (obj_bits_api type us) n; x < n; y < n\<rbrakk> \<Longrightarrow> word_of_nat y << obj_bits_api type us >> obj_bits_api type us = word_of_nat y
 4. \<And>x y. \<lbrakk>type = apiobject_type.Untyped \<longrightarrow> 4 \<le> us; range_cover ptr sz (obj_bits_api type us) n; x < n; y < n; word_of_nat x = word_of_nat y\<rbrakk> \<Longrightarrow> x = y proof (prove)
goal (3 subgoals):
 1. \<And>x y. \<lbrakk>type = apiobject_type.Untyped \<longrightarrow> 4 \<le> us; range_cover ptr sz (obj_bits_api type us) n; x < n; y < n\<rbrakk> \<Longrightarrow> word_of_nat x < 2 ^ (LENGTH(32) - obj_bits_api type us)
 2. \<And>x y. \<lbrakk>type = apiobject_type.Untyped \<longrightarrow> 4 \<le> us; range_cover ptr sz (obj_bits_api type us) n; x < n; y < n\<rbrakk> \<Longrightarrow> word_of_nat y << obj_bits_api type us >> obj_bits_api type us = word_of_nat y
 3. \<And>x y. \<lbrakk>type = apiobject_type.Untyped \<longrightarrow> 4 \<le> us; range_cover ptr sz (obj_bits_api type us) n; x < n; y < n; word_of_nat x = word_of_nat y\<rbrakk> \<Longrightarrow> x = y proof (prove)
goal (3 subgoals):
 1. \<And>x y. \<lbrakk>type = apiobject_type.Untyped \<longrightarrow> 4 \<le> us; range_cover ptr sz (obj_bits_api type us) n; x < n; y < n\<rbrakk> \<Longrightarrow> x < unat (2 ^ (LENGTH(32) - obj_bits_api type us))
 2. \<And>x y. \<lbrakk>type = apiobject_type.Untyped \<longrightarrow> 4 \<le> us; range_cover ptr sz (obj_bits_api type us) n; x < n; y < n\<rbrakk> \<Longrightarrow> word_of_nat y << obj_bits_api type us >> obj_bits_api type us = word_of_nat y
 3. \<And>x y. \<lbrakk>type = apiobject_type.Untyped \<longrightarrow> 4 \<le> us; range_cover ptr sz (obj_bits_api type us) n; x < n; y < n; word_of_nat x = word_of_nat y\<rbrakk> \<Longrightarrow> x = y proof (prove)
goal (4 subgoals):
 1. \<And>x y. \<lbrakk>type = apiobject_type.Untyped \<longrightarrow> 4 \<le> us; range_cover ptr sz (obj_bits_api type us) n; x < n; y < n\<rbrakk> \<Longrightarrow> LENGTH(32) - obj_bits_api type us < LENGTH(32)
 2. \<And>x y. \<lbrakk>type = apiobject_type.Untyped \<longrightarrow> 4 \<le> us; range_cover ptr sz (obj_bits_api type us) n; x < n; y < n\<rbrakk> \<Longrightarrow> x < 2 ^ (LENGTH(32) - obj_bits_api type us)
 3. \<And>x y. \<lbrakk>type = apiobject_type.Untyped \<longrightarrow> 4 \<le> us; range_cover ptr sz (obj_bits_api type us) n; x < n; y < n\<rbrakk> \<Longrightarrow> word_of_nat y << obj_bits_api type us >> obj_bits_api type us = word_of_nat y
 4. \<And>x y. \<lbrakk>type = apiobject_type.Untyped \<longrightarrow> 4 \<le> us; range_cover ptr sz (obj_bits_api type us) n; x < n; y < n; word_of_nat x = word_of_nat y\<rbrakk> \<Longrightarrow> x = y proof (prove)
goal (5 subgoals):
 1. \<And>x y. \<lbrakk>type = apiobject_type.Untyped \<longrightarrow> 4 \<le> us; range_cover ptr sz (obj_bits_api type us) n; x < n; y < n\<rbrakk> \<Longrightarrow> 0 < obj_bits_api type us
 2. \<And>x y. \<lbrakk>type = apiobject_type.Untyped \<longrightarrow> 4 \<le> us; range_cover ptr sz (obj_bits_api type us) n; x < n; y < n\<rbrakk> \<Longrightarrow> 0 < LENGTH(32)
 3. \<And>x y. \<lbrakk>type = apiobject_type.Untyped \<longrightarrow> 4 \<le> us; range_cover ptr sz (obj_bits_api type us) n; x < n; y < n\<rbrakk> \<Longrightarrow> x < 2 ^ (LENGTH(32) - obj_bits_api type us)
 4. \<And>x y. \<lbrakk>type = apiobject_type.Untyped \<longrightarrow> 4 \<le> us; range_cover ptr sz (obj_bits_api type us) n; x < n; y < n\<rbrakk> \<Longrightarrow> word_of_nat y << obj_bits_api type us >> obj_bits_api type us = word_of_nat y
 5. \<And>x y. \<lbrakk>type = apiobject_type.Untyped \<longrightarrow> 4 \<le> us; range_cover ptr sz (obj_bits_api type us) n; x < n; y < n; word_of_nat x = word_of_nat y\<rbrakk> \<Longrightarrow> x = y proof (prove)
goal (6 subgoals):
 1. \<And>x y. \<lbrakk>type = apiobject_type.Untyped \<longrightarrow> 4 \<le> us; range_cover ptr sz (obj_bits_api type us) n; x < n; y < n; untyped_min_bits \<le> obj_bits_api type us\<rbrakk> \<Longrightarrow> 0 < obj_bits_api type us
 2. \<And>x y. \<lbrakk>type = apiobject_type.Untyped \<longrightarrow> 4 \<le> us; range_cover ptr sz (obj_bits_api type us) n; x < n; y < n\<rbrakk> \<Longrightarrow> type = apiobject_type.Untyped \<longrightarrow> untyped_min_bits \<le> us
 3. \<And>x y. \<lbrakk>type = apiobject_type.Untyped \<longrightarrow> 4 \<le> us; range_cover ptr sz (obj_bits_api type us) n; x < n; y < n\<rbrakk> \<Longrightarrow> 0 < LENGTH(32)
 4. \<And>x y. \<lbrakk>type = apiobject_type.Untyped \<longrightarrow> 4 \<le> us; range_cover ptr sz (obj_bits_api type us) n; x < n; y < n\<rbrakk> \<Longrightarrow> x < 2 ^ (LENGTH(32) - obj_bits_api type us)
 5. \<And>x y. \<lbrakk>type = apiobject_type.Untyped \<longrightarrow> 4 \<le> us; range_cover ptr sz (obj_bits_api type us) n; x < n; y < n\<rbrakk> \<Longrightarrow> word_of_nat y << obj_bits_api type us >> obj_bits_api type us = word_of_nat y
 6. \<And>x y. \<lbrakk>type = apiobject_type.Untyped \<longrightarrow> 4 \<le> us; range_cover ptr sz (obj_bits_api type us) n; x < n; y < n; word_of_nat x = word_of_nat y\<rbrakk> \<Longrightarrow> x = y proof (prove)
goal (5 subgoals):
 1. \<And>x y. \<lbrakk>type = apiobject_type.Untyped \<longrightarrow> 4 \<le> us; range_cover ptr sz (obj_bits_api type us) n; x < n; y < n\<rbrakk> \<Longrightarrow> type = apiobject_type.Untyped \<longrightarrow> untyped_min_bits \<le> us
 2. \<And>x y. \<lbrakk>type = apiobject_type.Untyped \<longrightarrow> 4 \<le> us; range_cover ptr sz (obj_bits_api type us) n; x < n; y < n\<rbrakk> \<Longrightarrow> 0 < LENGTH(32)
 3. \<And>x y. \<lbrakk>type = apiobject_type.Untyped \<longrightarrow> 4 \<le> us; range_cover ptr sz (obj_bits_api type us) n; x < n; y < n\<rbrakk> \<Longrightarrow> x < 2 ^ (LENGTH(32) - obj_bits_api type us)
 4. \<And>x y. \<lbrakk>type = apiobject_type.Untyped \<longrightarrow> 4 \<le> us; range_cover ptr sz (obj_bits_api type us) n; x < n; y < n\<rbrakk> \<Longrightarrow> word_of_nat y << obj_bits_api type us >> obj_bits_api type us = word_of_nat y
 5. \<And>x y. \<lbrakk>type = apiobject_type.Untyped \<longrightarrow> 4 \<le> us; range_cover ptr sz (obj_bits_api type us) n; x < n; y < n; word_of_nat x = word_of_nat y\<rbrakk> \<Longrightarrow> x = y proof (prove)
goal (4 subgoals):
 1. \<And>x y. \<lbrakk>type = apiobject_type.Untyped \<longrightarrow> 4 \<le> us; range_cover ptr sz (obj_bits_api type us) n; x < n; y < n\<rbrakk> \<Longrightarrow> 0 < LENGTH(32)
 2. \<And>x y. \<lbrakk>type = apiobject_type.Untyped \<longrightarrow> 4 \<le> us; range_cover ptr sz (obj_bits_api type us) n; x < n; y < n\<rbrakk> \<Longrightarrow> x < 2 ^ (LENGTH(32) - obj_bits_api type us)
 3. \<And>x y. \<lbrakk>type = apiobject_type.Untyped \<longrightarrow> 4 \<le> us; range_cover ptr sz (obj_bits_api type us) n; x < n; y < n\<rbrakk> \<Longrightarrow> word_of_nat y << obj_bits_api type us >> obj_bits_api type us = word_of_nat y
 4. \<And>x y. \<lbrakk>type = apiobject_type.Untyped \<longrightarrow> 4 \<le> us; range_cover ptr sz (obj_bits_api type us) n; x < n; y < n; word_of_nat x = word_of_nat y\<rbrakk> \<Longrightarrow> x = y proof (prove)
goal (3 subgoals):
 1. \<And>x y. \<lbrakk>type = apiobject_type.Untyped \<longrightarrow> 4 \<le> us; range_cover ptr sz (obj_bits_api type us) n; x < n; y < n\<rbrakk> \<Longrightarrow> x < 2 ^ (LENGTH(32) - obj_bits_api type us)
 2. \<And>x y. \<lbrakk>type = apiobject_type.Untyped \<longrightarrow> 4 \<le> us; range_cover ptr sz (obj_bits_api type us) n; x < n; y < n\<rbrakk> \<Longrightarrow> word_of_nat y << obj_bits_api type us >> obj_bits_api type us = word_of_nat y
 3. \<And>x y. \<lbrakk>type = apiobject_type.Untyped \<longrightarrow> 4 \<le> us; range_cover ptr sz (obj_bits_api type us) n; x < n; y < n; word_of_nat x = word_of_nat y\<rbrakk> \<Longrightarrow> x = y proof (prove)
goal (3 subgoals):
 1. \<And>x y. \<lbrakk>type = apiobject_type.Untyped \<longrightarrow> 4 \<le> us; x < n; y < n\<rbrakk> \<Longrightarrow> x \<le> n
 2. \<And>x y. \<lbrakk>type = apiobject_type.Untyped \<longrightarrow> 4 \<le> us; range_cover ptr sz (obj_bits_api type us) n; x < n; y < n\<rbrakk> \<Longrightarrow> word_of_nat y << obj_bits_api type us >> obj_bits_api type us = word_of_nat y
 3. \<And>x y. \<lbrakk>type = apiobject_type.Untyped \<longrightarrow> 4 \<le> us; range_cover ptr sz (obj_bits_api type us) n; x < n; y < n; word_of_nat x = word_of_nat y\<rbrakk> \<Longrightarrow> x = y proof (prove)
goal (2 subgoals):
 1. \<And>x y. \<lbrakk>type = apiobject_type.Untyped \<longrightarrow> 4 \<le> us; range_cover ptr sz (obj_bits_api type us) n; x < n; y < n\<rbrakk> \<Longrightarrow> word_of_nat y << obj_bits_api type us >> obj_bits_api type us = word_of_nat y
 2. \<And>x y. \<lbrakk>type = apiobject_type.Untyped \<longrightarrow> 4 \<le> us; range_cover ptr sz (obj_bits_api type us) n; x < n; y < n; word_of_nat x = word_of_nat y\<rbrakk> \<Longrightarrow> x = y proof (prove)
goal (3 subgoals):
 1. \<And>x y. \<lbrakk>type = apiobject_type.Untyped \<longrightarrow> 4 \<le> us; range_cover ptr sz (obj_bits_api type us) n; x < n; y < n\<rbrakk> \<Longrightarrow> obj_bits_api type us < LENGTH(32)
 2. \<And>x y. \<lbrakk>type = apiobject_type.Untyped \<longrightarrow> 4 \<le> us; range_cover ptr sz (obj_bits_api type us) n; x < n; y < n\<rbrakk> \<Longrightarrow> word_of_nat y < 2 ^ (LENGTH(32) - obj_bits_api type us)
 3. \<And>x y. \<lbrakk>type = apiobject_type.Untyped \<longrightarrow> 4 \<le> us; range_cover ptr sz (obj_bits_api type us) n; x < n; y < n; word_of_nat x = word_of_nat y\<rbrakk> \<Longrightarrow> x = y proof (prove)
goal (2 subgoals):
 1. \<And>x y. \<lbrakk>type = apiobject_type.Untyped \<longrightarrow> 4 \<le> us; range_cover ptr sz (obj_bits_api type us) n; x < n; y < n\<rbrakk> \<Longrightarrow> word_of_nat y < 2 ^ (LENGTH(32) - obj_bits_api type us)
 2. \<And>x y. \<lbrakk>type = apiobject_type.Untyped \<longrightarrow> 4 \<le> us; range_cover ptr sz (obj_bits_api type us) n; x < n; y < n; word_of_nat x = word_of_nat y\<rbrakk> \<Longrightarrow> x = y proof (prove)
goal (2 subgoals):
 1. \<And>x y. \<lbrakk>type = apiobject_type.Untyped \<longrightarrow> 4 \<le> us; range_cover ptr sz (obj_bits_api type us) n; x < n; y < n\<rbrakk> \<Longrightarrow> y < unat (2 ^ (LENGTH(32) - obj_bits_api type us))
 2. \<And>x y. \<lbrakk>type = apiobject_type.Untyped \<longrightarrow> 4 \<le> us; range_cover ptr sz (obj_bits_api type us) n; x < n; y < n; word_of_nat x = word_of_nat y\<rbrakk> \<Longrightarrow> x = y proof (prove)
goal (3 subgoals):
 1. \<And>x y. \<lbrakk>type = apiobject_type.Untyped \<longrightarrow> 4 \<le> us; range_cover ptr sz (obj_bits_api type us) n; x < n; y < n\<rbrakk> \<Longrightarrow> LENGTH(32) - obj_bits_api type us < LENGTH(32)
 2. \<And>x y. \<lbrakk>type = apiobject_type.Untyped \<longrightarrow> 4 \<le> us; range_cover ptr sz (obj_bits_api type us) n; x < n; y < n\<rbrakk> \<Longrightarrow> y < 2 ^ (LENGTH(32) - obj_bits_api type us)
 3. \<And>x y. \<lbrakk>type = apiobject_type.Untyped \<longrightarrow> 4 \<le> us; range_cover ptr sz (obj_bits_api type us) n; x < n; y < n; word_of_nat x = word_of_nat y\<rbrakk> \<Longrightarrow> x = y proof (prove)
goal (4 subgoals):
 1. \<And>x y. \<lbrakk>type = apiobject_type.Untyped \<longrightarrow> 4 \<le> us; range_cover ptr sz (obj_bits_api type us) n; x < n; y < n\<rbrakk> \<Longrightarrow> 0 < obj_bits_api type us
 2. \<And>x y. \<lbrakk>type = apiobject_type.Untyped \<longrightarrow> 4 \<le> us; range_cover ptr sz (obj_bits_api type us) n; x < n; y < n\<rbrakk> \<Longrightarrow> 0 < LENGTH(32)
 3. \<And>x y. \<lbrakk>type = apiobject_type.Untyped \<longrightarrow> 4 \<le> us; range_cover ptr sz (obj_bits_api type us) n; x < n; y < n\<rbrakk> \<Longrightarrow> y < 2 ^ (LENGTH(32) - obj_bits_api type us)
 4. \<And>x y. \<lbrakk>type = apiobject_type.Untyped \<longrightarrow> 4 \<le> us; range_cover ptr sz (obj_bits_api type us) n; x < n; y < n; word_of_nat x = word_of_nat y\<rbrakk> \<Longrightarrow> x = y proof (prove)
goal (5 subgoals):
 1. \<And>x y. \<lbrakk>type = apiobject_type.Untyped \<longrightarrow> 4 \<le> us; range_cover ptr sz (obj_bits_api type us) n; x < n; y < n; untyped_min_bits \<le> obj_bits_api type us\<rbrakk> \<Longrightarrow> 0 < obj_bits_api type us
 2. \<And>x y. \<lbrakk>type = apiobject_type.Untyped \<longrightarrow> 4 \<le> us; range_cover ptr sz (obj_bits_api type us) n; x < n; y < n\<rbrakk> \<Longrightarrow> type = apiobject_type.Untyped \<longrightarrow> untyped_min_bits \<le> us
 3. \<And>x y. \<lbrakk>type = apiobject_type.Untyped \<longrightarrow> 4 \<le> us; range_cover ptr sz (obj_bits_api type us) n; x < n; y < n\<rbrakk> \<Longrightarrow> 0 < LENGTH(32)
 4. \<And>x y. \<lbrakk>type = apiobject_type.Untyped \<longrightarrow> 4 \<le> us; range_cover ptr sz (obj_bits_api type us) n; x < n; y < n\<rbrakk> \<Longrightarrow> y < 2 ^ (LENGTH(32) - obj_bits_api type us)
 5. \<And>x y. \<lbrakk>type = apiobject_type.Untyped \<longrightarrow> 4 \<le> us; range_cover ptr sz (obj_bits_api type us) n; x < n; y < n; word_of_nat x = word_of_nat y\<rbrakk> \<Longrightarrow> x = y proof (prove)
goal (4 subgoals):
 1. \<And>x y. \<lbrakk>type = apiobject_type.Untyped \<longrightarrow> 4 \<le> us; range_cover ptr sz (obj_bits_api type us) n; x < n; y < n\<rbrakk> \<Longrightarrow> type = apiobject_type.Untyped \<longrightarrow> untyped_min_bits \<le> us
 2. \<And>x y. \<lbrakk>type = apiobject_type.Untyped \<longrightarrow> 4 \<le> us; range_cover ptr sz (obj_bits_api type us) n; x < n; y < n\<rbrakk> \<Longrightarrow> 0 < LENGTH(32)
 3. \<And>x y. \<lbrakk>type = apiobject_type.Untyped \<longrightarrow> 4 \<le> us; range_cover ptr sz (obj_bits_api type us) n; x < n; y < n\<rbrakk> \<Longrightarrow> y < 2 ^ (LENGTH(32) - obj_bits_api type us)
 4. \<And>x y. \<lbrakk>type = apiobject_type.Untyped \<longrightarrow> 4 \<le> us; range_cover ptr sz (obj_bits_api type us) n; x < n; y < n; word_of_nat x = word_of_nat y\<rbrakk> \<Longrightarrow> x = y proof (prove)
goal (3 subgoals):
 1. \<And>x y. \<lbrakk>type = apiobject_type.Untyped \<longrightarrow> 4 \<le> us; range_cover ptr sz (obj_bits_api type us) n; x < n; y < n\<rbrakk> \<Longrightarrow> 0 < LENGTH(32)
 2. \<And>x y. \<lbrakk>type = apiobject_type.Untyped \<longrightarrow> 4 \<le> us; range_cover ptr sz (obj_bits_api type us) n; x < n; y < n\<rbrakk> \<Longrightarrow> y < 2 ^ (LENGTH(32) - obj_bits_api type us)
 3. \<And>x y. \<lbrakk>type = apiobject_type.Untyped \<longrightarrow> 4 \<le> us; range_cover ptr sz (obj_bits_api type us) n; x < n; y < n; word_of_nat x = word_of_nat y\<rbrakk> \<Longrightarrow> x = y proof (prove)
goal (2 subgoals):
 1. \<And>x y. \<lbrakk>type = apiobject_type.Untyped \<longrightarrow> 4 \<le> us; range_cover ptr sz (obj_bits_api type us) n; x < n; y < n\<rbrakk> \<Longrightarrow> y < 2 ^ (LENGTH(32) - obj_bits_api type us)
 2. \<And>x y. \<lbrakk>type = apiobject_type.Untyped \<longrightarrow> 4 \<le> us; range_cover ptr sz (obj_bits_api type us) n; x < n; y < n; word_of_nat x = word_of_nat y\<rbrakk> \<Longrightarrow> x = y proof (prove)
goal (2 subgoals):
 1. \<And>x y. \<lbrakk>type = apiobject_type.Untyped \<longrightarrow> 4 \<le> us; x < n; y < n\<rbrakk> \<Longrightarrow> y \<le> n
 2. \<And>x y. \<lbrakk>type = apiobject_type.Untyped \<longrightarrow> 4 \<le> us; range_cover ptr sz (obj_bits_api type us) n; x < n; y < n; word_of_nat x = word_of_nat y\<rbrakk> \<Longrightarrow> x = y proof (prove)
goal (1 subgoal):
 1. \<And>x y. \<lbrakk>type = apiobject_type.Untyped \<longrightarrow> 4 \<le> us; range_cover ptr sz (obj_bits_api type us) n; x < n; y < n; word_of_nat x = word_of_nat y\<rbrakk> \<Longrightarrow> x = y proof (prove)
goal (3 subgoals):
 1. \<And>x y. \<lbrakk>type = apiobject_type.Untyped \<longrightarrow> 4 \<le> us; range_cover ptr sz (obj_bits_api type us) n; x < n; y < n; word_of_nat x = word_of_nat y\<rbrakk> \<Longrightarrow> x < 2 ^ LENGTH(32)
 2. \<And>x y. \<lbrakk>type = apiobject_type.Untyped \<longrightarrow> 4 \<le> us; range_cover ptr sz (obj_bits_api type us) n; x < n; y < n; word_of_nat x = word_of_nat y\<rbrakk> \<Longrightarrow> y < 2 ^ LENGTH(32)
 3. \<And>x y. \<lbrakk>type = apiobject_type.Untyped \<longrightarrow> 4 \<le> us; range_cover ptr sz (obj_bits_api type us) n; x < n; y < n; word_of_nat x = word_of_nat y\<rbrakk> \<Longrightarrow> word_of_nat x = word_of_nat y proof (prove)
goal:
No subgoals!