theory ADT_H

lemma pspace_aligned_distinct_None:
  (* NOTE: life would be easier if pspace_aligned and pspace_distinct were defined on PSpace instead of the whole kernel state. *)
assumes pspace_aligned:
  "\<forall>x\<in>dom ha. is_aligned (x :: word32) (obj_bits (the (ha x)))"
assumes pspace_distinct:
  "\<forall>x y ko ko'.
   ha x = Some ko \<and> ha y = Some ko' \<and> x \<noteq> y \<longrightarrow>
   {x..x + (2 ^ obj_bits ko - 1)} \<inter> {y..y + (2 ^ obj_bits ko' - 1)} = {}"
shows
  "\<lbrakk>ha x = Some ko; y \<in> {0<..<2^(obj_bits ko)}\<rbrakk> \<Longrightarrow> ha (x+y) = None" using pspace_aligned[simplified dom_def, simplified] apply (erule_tac x=x in allE) apply (rule ccontr) apply clarsimp apply (rename_tac ko') using pspace_distinct pspace_aligned[simplified dom_def, simplified] apply (erule_tac x=x in allE) apply (erule_tac x="x+y" in allE)+ apply (clarsimp simp add: word_gt_0) apply (clarsimp simp add: ucast_of_nat_small is_aligned_mask mask_2pm1[symmetric]) apply (frule (1) is_aligned_AND_less_0) apply (clarsimp simp add: word_plus_and_or_coroll le_word_or2) apply (simp add: or.assoc le_word_or2) apply (simp add: word_plus_and_or_coroll[symmetric]) apply (subgoal_tac "x + y \<le> x + mask (obj_bits ko)", simp) apply (rule word_add_le_mono2) apply (simp add: mask_def plus_one_helper) apply (thin_tac "~ P" for P)+ apply (thin_tac "(x::'a::len word) < y" for x y)+ apply (thin_tac "x = Some y" for x y)+ apply (thin_tac "x && mask (obj_bits ko') = 0" for x) apply (thin_tac "x && y = 0") apply (clarsimp simp add: dvd_def word_bits_len_of word_bits_conv
                            and_mask_dvd_nat[symmetric]) apply (cut_tac x=x in unat_lt2p) apply (cut_tac x="mask (obj_bits ko)::word32" in unat_lt2p) apply (simp add: mult.commute
                   add.commute[of "unat (mask (obj_bits ko))"]) apply (case_tac "k=0", simp+) apply (subgoal_tac "obj_bits ko\<le>32") prefer 2 apply (rule ccontr) apply (simp add: not_le) apply (frule_tac a="2::nat" and n=32 in power_strict_increasing, simp+) apply (case_tac "k=1", simp) apply (cut_tac m=k and n="2 ^ obj_bits ko" in n_less_n_mult_m,
          (simp(no_asm_simp))+) apply (simp only: mult.commute) apply (thin_tac "x = y" for x y)+ apply (clarsimp simp add: le_less) apply (erule disjE) prefer 2 apply (simp add: mask_def) apply (subgoal_tac "obj_bits ko <= (31::nat)", simp_all) apply (simp add: mask_def unat_minus_one word_bits_conv) apply (cut_tac w=k and c="2 ^ obj_bits ko" and b="2^(32-obj_bits ko)"
              in less_le_mult_nat) apply (simp_all add: power_add[symmetric]) apply (rule ccontr) apply (simp add: not_less) apply (simp add: le_less[of "2 ^ (32 - obj_bits ko)"]) apply (erule disjE) prefer 2 apply (clarsimp simp add: power_add[symmetric]) apply clarsimp apply (drule mult_less_mono1[of "2 ^ (32 - obj_bits ko)" _ "2 ^ obj_bits ko"]) apply (simp add: power_add[symmetric])+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>ha x = Some ko; y \<in> {0<..<2 ^ obj_bits ko}\<rbrakk> \<Longrightarrow> ha (x + y) = None proof (prove)
using this:
\<forall>x. (\<exists>y. ha x = Some y) \<longrightarrow> is_aligned x (obj_bits (the (ha x)))

goal (1 subgoal):
 1. \<lbrakk>ha x = Some ko; y \<in> {0<..<2 ^ obj_bits ko}\<rbrakk> \<Longrightarrow> ha (x + y) = None proof (prove)
goal (1 subgoal):
 1. \<lbrakk>ha x = Some ko; y \<in> {0<..<2 ^ obj_bits ko}; (\<exists>y. ha x = Some y) \<longrightarrow> is_aligned x (obj_bits (the (ha x)))\<rbrakk> \<Longrightarrow> ha (x + y) = None proof (prove)
goal (1 subgoal):
 1. \<lbrakk>ha x = Some ko; y \<in> {0<..<2 ^ obj_bits ko}; (\<exists>y. ha x = Some y) \<longrightarrow> is_aligned x (obj_bits (the (ha x))); ha (x + y) \<noteq> None\<rbrakk> \<Longrightarrow> False proof (prove)
goal (1 subgoal):
 1. \<And>ya. \<lbrakk>ha x = Some ko; is_aligned x (obj_bits ko); ha (x + y) = Some ya; 0 < y; y < 2 ^ obj_bits ko\<rbrakk> \<Longrightarrow> False proof (prove)
goal (1 subgoal):
 1. \<And>ko'. \<lbrakk>ha x = Some ko; is_aligned x (obj_bits ko); ha (x + y) = Some ko'; 0 < y; y < 2 ^ obj_bits ko\<rbrakk> \<Longrightarrow> False proof (prove)
using this:
\<forall>x y ko ko'. ha x = Some ko \<and> ha y = Some ko' \<and> x \<noteq> y \<longrightarrow> {x..x + (2 ^ obj_bits ko - 1)} \<inter> {y..y + (2 ^ obj_bits ko' - 1)} = {}
\<forall>x. (\<exists>y. ha x = Some y) \<longrightarrow> is_aligned x (obj_bits (the (ha x)))

goal (1 subgoal):
 1. \<And>ko'. \<lbrakk>ha x = Some ko; is_aligned x (obj_bits ko); ha (x + y) = Some ko'; 0 < y; y < 2 ^ obj_bits ko\<rbrakk> \<Longrightarrow> False proof (prove)
goal (1 subgoal):
 1. \<And>ko'. \<lbrakk>ha x = Some ko; is_aligned x (obj_bits ko); ha (x + y) = Some ko'; 0 < y; y < 2 ^ obj_bits ko; \<forall>x. (\<exists>y. ha x = Some y) \<longrightarrow> is_aligned x (obj_bits (the (ha x))); \<forall>y ko ko'. ha x = Some ko \<and> ha y = Some ko' \<and> x \<noteq> y \<longrightarrow> {x..x + (2 ^ obj_bits ko - 1)} \<inter> {y..y + (2 ^ obj_bits ko' - 1)} = {}\<rbrakk> \<Longrightarrow> False proof (prove)
goal (1 subgoal):
 1. \<And>ko'. \<lbrakk>ha x = Some ko; is_aligned x (obj_bits ko); ha (x + y) = Some ko'; 0 < y; y < 2 ^ obj_bits ko; (\<exists>ya. ha (x + y) = Some ya) \<longrightarrow> is_aligned (x + y) (obj_bits (the (ha (x + y)))); \<forall>ko ko'. ha x = Some ko \<and> ha (x + y) = Some ko' \<and> x \<noteq> x + y \<longrightarrow> {x..x + (2 ^ obj_bits ko - 1)} \<inter> {x + y..x + y + (2 ^ obj_bits ko' - 1)} = {}\<rbrakk> \<Longrightarrow> False proof (prove)
goal (1 subgoal):
 1. \<And>ko'. \<lbrakk>ha x = Some ko; is_aligned x (obj_bits ko); ha (x + y) = Some ko'; y \<noteq> 0; y < 2 ^ obj_bits ko; is_aligned (x + y) (obj_bits ko'); x \<le> x + y + (2 ^ obj_bits ko' - 1) \<longrightarrow> x + y \<le> x + (2 ^ obj_bits ko - 1) \<longrightarrow> x \<le> x + (2 ^ obj_bits ko - 1) \<longrightarrow> \<not> x + y \<le> x + y + (2 ^ obj_bits ko' - 1)\<rbrakk> \<Longrightarrow> False proof (prove)
goal (1 subgoal):
 1. \<And>ko'. \<lbrakk>ha x = Some ko; x && mask (obj_bits ko) = 0; ha (x + y) = Some ko'; y \<noteq> 0; y < 2 ^ obj_bits ko; x + y && mask (obj_bits ko') = 0; x \<le> x + y + mask (obj_bits ko') \<longrightarrow> x + y \<le> x + mask (obj_bits ko) \<longrightarrow> x \<le> x + mask (obj_bits ko) \<longrightarrow> \<not> x + y \<le> x + y + mask (obj_bits ko')\<rbrakk> \<Longrightarrow> False proof (prove)
goal (1 subgoal):
 1. \<And>ko'. \<lbrakk>ha x = Some ko; x && mask (obj_bits ko) = 0; ha (x + y) = Some ko'; y \<noteq> 0; y < 2 ^ obj_bits ko; x + y && mask (obj_bits ko') = 0; x \<le> x + y + mask (obj_bits ko') \<longrightarrow> x + y \<le> x + mask (obj_bits ko) \<longrightarrow> x \<le> x + mask (obj_bits ko) \<longrightarrow> \<not> x + y \<le> x + y + mask (obj_bits ko'); x && y = 0\<rbrakk> \<Longrightarrow> False proof (prove)
goal (1 subgoal):
 1. \<And>ko'. \<lbrakk>ha x = Some ko; x && mask (obj_bits ko) = 0; ha (x || y) = Some ko'; y \<noteq> 0; y < 2 ^ obj_bits ko; (x || y) && mask (obj_bits ko') = 0; x \<le> (x || y) || mask (obj_bits ko') \<longrightarrow> \<not> x || y \<le> x || mask (obj_bits ko); x && y = 0\<rbrakk> \<Longrightarrow> False proof (prove)
goal (1 subgoal):
 1. \<And>ko'. \<lbrakk>ha x = Some ko; x && mask (obj_bits ko) = 0; ha (x || y) = Some ko'; y \<noteq> 0; y < 2 ^ obj_bits ko; (x || y) && mask (obj_bits ko') = 0; \<not> x || y \<le> x || mask (obj_bits ko); x && y = 0\<rbrakk> \<Longrightarrow> False proof (prove)
goal (1 subgoal):
 1. \<And>ko'. \<lbrakk>ha x = Some ko; x && mask (obj_bits ko) = 0; ha (x + y) = Some ko'; y \<noteq> 0; y < 2 ^ obj_bits ko; x + y && mask (obj_bits ko') = 0; \<not> x + y \<le> x + mask (obj_bits ko); x && y = 0\<rbrakk> \<Longrightarrow> False proof (prove)
goal (1 subgoal):
 1. \<And>ko'. \<lbrakk>ha x = Some ko; x && mask (obj_bits ko) = 0; ha (x + y) = Some ko'; y \<noteq> 0; y < 2 ^ obj_bits ko; x + y && mask (obj_bits ko') = 0; \<not> x + y \<le> x + mask (obj_bits ko); x && y = 0\<rbrakk> \<Longrightarrow> x + y \<le> x + mask (obj_bits ko) proof (prove)
goal (2 subgoals):
 1. \<And>ko'. \<lbrakk>ha x = Some ko; x && mask (obj_bits ko) = 0; ha (x + y) = Some ko'; y \<noteq> 0; y < 2 ^ obj_bits ko; x + y && mask (obj_bits ko') = 0; \<not> x + y \<le> x + mask (obj_bits ko); x && y = 0\<rbrakk> \<Longrightarrow> y \<le> mask (obj_bits ko)
 2. \<And>ko'. \<lbrakk>ha x = Some ko; x && mask (obj_bits ko) = 0; ha (x + y) = Some ko'; y \<noteq> 0; y < 2 ^ obj_bits ko; x + y && mask (obj_bits ko') = 0; \<not> x + y \<le> x + mask (obj_bits ko); x && y = 0\<rbrakk> \<Longrightarrow> unat (mask (obj_bits ko)) + unat x < 2 ^ LENGTH(32) proof (prove)
goal (1 subgoal):
 1. \<And>ko'. \<lbrakk>ha x = Some ko; x && mask (obj_bits ko) = 0; ha (x + y) = Some ko'; y \<noteq> 0; y < 2 ^ obj_bits ko; x + y && mask (obj_bits ko') = 0; \<not> x + y \<le> x + mask (obj_bits ko); x && y = 0\<rbrakk> \<Longrightarrow> unat (mask (obj_bits ko)) + unat x < 2 ^ LENGTH(32) proof (prove)
goal (1 subgoal):
 1. \<And>ko'. \<lbrakk>ha x = Some ko; x && mask (obj_bits ko) = 0; ha (x + y) = Some ko'; y < 2 ^ obj_bits ko; x + y && mask (obj_bits ko') = 0; x && y = 0\<rbrakk> \<Longrightarrow> unat (mask (obj_bits ko)) + unat x < 2 ^ LENGTH(32) proof (prove)
goal (1 subgoal):
 1. \<And>ko'. \<lbrakk>ha x = Some ko; x && mask (obj_bits ko) = 0; ha (x + y) = Some ko'; x + y && mask (obj_bits ko') = 0; x && y = 0\<rbrakk> \<Longrightarrow> unat (mask (obj_bits ko)) + unat x < 2 ^ LENGTH(32) proof (prove)
goal (1 subgoal):
 1. \<And>ko'. \<lbrakk>x && mask (obj_bits ko) = 0; x + y && mask (obj_bits ko') = 0; x && y = 0\<rbrakk> \<Longrightarrow> unat (mask (obj_bits ko)) + unat x < 2 ^ LENGTH(32) proof (prove)
goal (1 subgoal):
 1. \<And>ko'. \<lbrakk>x && mask (obj_bits ko) = 0; x && y = 0\<rbrakk> \<Longrightarrow> unat (mask (obj_bits ko)) + unat x < 2 ^ LENGTH(32) proof (prove)
goal (1 subgoal):
 1. \<And>ko'. x && mask (obj_bits ko) = 0 \<Longrightarrow> unat (mask (obj_bits ko)) + unat x < 2 ^ LENGTH(32) proof (prove)
goal (1 subgoal):
 1. \<And>k. unat x = 2 ^ obj_bits ko * k \<Longrightarrow> unat (mask (obj_bits ko)) + 2 ^ obj_bits ko * k < 4294967296 proof (prove)
goal (1 subgoal):
 1. \<And>k. \<lbrakk>unat x = 2 ^ obj_bits ko * k; unat x < 2 ^ LENGTH(32)\<rbrakk> \<Longrightarrow> unat (mask (obj_bits ko)) + 2 ^ obj_bits ko * k < 4294967296 proof (prove)
goal (1 subgoal):
 1. \<And>k. \<lbrakk>unat x = 2 ^ obj_bits ko * k; unat x < 2 ^ LENGTH(32); unat (mask (obj_bits ko)) < 2 ^ LENGTH(32)\<rbrakk> \<Longrightarrow> unat (mask (obj_bits ko)) + 2 ^ obj_bits ko * k < 4294967296 proof (prove)
goal (1 subgoal):
 1. \<And>k. \<lbrakk>unat x = k * 2 ^ obj_bits ko; k * 2 ^ obj_bits ko < 4294967296; unat (mask (obj_bits ko)) < 4294967296\<rbrakk> \<Longrightarrow> k * 2 ^ obj_bits ko + unat (mask (obj_bits ko)) < 4294967296 proof (prove)
goal (1 subgoal):
 1. \<And>k. \<lbrakk>unat x = k * 2 ^ obj_bits ko; k * 2 ^ obj_bits ko < 4294967296; unat (mask (obj_bits ko)) < 4294967296; 0 < k\<rbrakk> \<Longrightarrow> k * 2 ^ obj_bits ko + unat (mask (obj_bits ko)) < 4294967296 proof (prove)
goal (2 subgoals):
 1. \<And>k. \<lbrakk>unat x = k * 2 ^ obj_bits ko; k * 2 ^ obj_bits ko < 4294967296; unat (mask (obj_bits ko)) < 4294967296; 0 < k; obj_bits ko \<le> 32\<rbrakk> \<Longrightarrow> k * 2 ^ obj_bits ko + unat (mask (obj_bits ko)) < 4294967296
 2. \<And>k. \<lbrakk>unat x = k * 2 ^ obj_bits ko; k * 2 ^ obj_bits ko < 4294967296; unat (mask (obj_bits ko)) < 4294967296; 0 < k\<rbrakk> \<Longrightarrow> obj_bits ko \<le> 32 proof (prove)
goal (2 subgoals):
 1. \<And>k. \<lbrakk>unat x = k * 2 ^ obj_bits ko; k * 2 ^ obj_bits ko < 4294967296; unat (mask (obj_bits ko)) < 4294967296; 0 < k\<rbrakk> \<Longrightarrow> obj_bits ko \<le> 32
 2. \<And>k. \<lbrakk>unat x = k * 2 ^ obj_bits ko; k * 2 ^ obj_bits ko < 4294967296; unat (mask (obj_bits ko)) < 4294967296; 0 < k; obj_bits ko \<le> 32\<rbrakk> \<Longrightarrow> k * 2 ^ obj_bits ko + unat (mask (obj_bits ko)) < 4294967296 proof (prove)
goal (2 subgoals):
 1. \<And>k. \<lbrakk>unat x = k * 2 ^ obj_bits ko; k * 2 ^ obj_bits ko < 4294967296; unat (mask (obj_bits ko)) < 4294967296; 0 < k; \<not> obj_bits ko \<le> 32\<rbrakk> \<Longrightarrow> False
 2. \<And>k. \<lbrakk>unat x = k * 2 ^ obj_bits ko; k * 2 ^ obj_bits ko < 4294967296; unat (mask (obj_bits ko)) < 4294967296; 0 < k; obj_bits ko \<le> 32\<rbrakk> \<Longrightarrow> k * 2 ^ obj_bits ko + unat (mask (obj_bits ko)) < 4294967296 proof (prove)
goal (2 subgoals):
 1. \<And>k. \<lbrakk>unat x = k * 2 ^ obj_bits ko; k * 2 ^ obj_bits ko < 4294967296; unat (mask (obj_bits ko)) < 4294967296; 0 < k; 32 < obj_bits ko\<rbrakk> \<Longrightarrow> False
 2. \<And>k. \<lbrakk>unat x = k * 2 ^ obj_bits ko; k * 2 ^ obj_bits ko < 4294967296; unat (mask (obj_bits ko)) < 4294967296; 0 < k; obj_bits ko \<le> 32\<rbrakk> \<Longrightarrow> k * 2 ^ obj_bits ko + unat (mask (obj_bits ko)) < 4294967296 proof (prove)
goal (2 subgoals):
 1. \<And>k. \<lbrakk>unat x = k * 2 ^ obj_bits ko; k * 2 ^ obj_bits ko < 4294967296; unat (mask (obj_bits ko)) < 4294967296; 0 < k; 32 < obj_bits ko; 4294967296 < 2 ^ obj_bits ko\<rbrakk> \<Longrightarrow> False
 2. \<And>k. \<lbrakk>unat x = k * 2 ^ obj_bits ko; k * 2 ^ obj_bits ko < 4294967296; unat (mask (obj_bits ko)) < 4294967296; 0 < k; obj_bits ko \<le> 32\<rbrakk> \<Longrightarrow> k * 2 ^ obj_bits ko + unat (mask (obj_bits ko)) < 4294967296 proof (prove)
goal (2 subgoals):
 1. \<And>k. \<lbrakk>unat x = k * 2 ^ obj_bits ko; k * 2 ^ obj_bits ko < 4294967296; unat (mask (obj_bits ko)) < 4294967296; 0 < k; 32 < obj_bits ko; 4294967296 < 2 ^ obj_bits ko; k \<noteq> 1\<rbrakk> \<Longrightarrow> False
 2. \<And>k. \<lbrakk>unat x = k * 2 ^ obj_bits ko; k * 2 ^ obj_bits ko < 4294967296; unat (mask (obj_bits ko)) < 4294967296; 0 < k; obj_bits ko \<le> 32\<rbrakk> \<Longrightarrow> k * 2 ^ obj_bits ko + unat (mask (obj_bits ko)) < 4294967296 proof (prove)
goal (2 subgoals):
 1. \<And>k. \<lbrakk>unat x = k * 2 ^ obj_bits ko; k * 2 ^ obj_bits ko < 4294967296; unat (mask (obj_bits ko)) < 4294967296; 0 < k; 32 < obj_bits ko; 4294967296 < 2 ^ obj_bits ko; k \<noteq> 1; 2 ^ obj_bits ko < 2 ^ obj_bits ko * k\<rbrakk> \<Longrightarrow> False
 2. \<And>k. \<lbrakk>unat x = k * 2 ^ obj_bits ko; k * 2 ^ obj_bits ko < 4294967296; unat (mask (obj_bits ko)) < 4294967296; 0 < k; obj_bits ko \<le> 32\<rbrakk> \<Longrightarrow> k * 2 ^ obj_bits ko + unat (mask (obj_bits ko)) < 4294967296 proof (prove)
goal (1 subgoal):
 1. \<And>k. \<lbrakk>unat x = k * 2 ^ obj_bits ko; k * 2 ^ obj_bits ko < 4294967296; unat (mask (obj_bits ko)) < 4294967296; 0 < k; obj_bits ko \<le> 32\<rbrakk> \<Longrightarrow> k * 2 ^ obj_bits ko + unat (mask (obj_bits ko)) < 4294967296 proof (prove)
goal (1 subgoal):
 1. \<And>k. \<lbrakk>k * 2 ^ obj_bits ko < 4294967296; unat (mask (obj_bits ko)) < 4294967296; 0 < k; obj_bits ko \<le> 32\<rbrakk> \<Longrightarrow> k * 2 ^ obj_bits ko + unat (mask (obj_bits ko)) < 4294967296 proof (prove)
goal (1 subgoal):
 1. \<And>k. \<lbrakk>k * 2 ^ obj_bits ko < 4294967296; unat (mask (obj_bits ko)) < 4294967296; 0 < k; obj_bits ko < 32 \<or> obj_bits ko = 32\<rbrakk> \<Longrightarrow> k * 2 ^ obj_bits ko + unat (mask (obj_bits ko)) < 4294967296 proof (prove)
goal (2 subgoals):
 1. \<And>k. \<lbrakk>k * 2 ^ obj_bits ko < 4294967296; unat (mask (obj_bits ko)) < 4294967296; 0 < k; obj_bits ko < 32\<rbrakk> \<Longrightarrow> k * 2 ^ obj_bits ko + unat (mask (obj_bits ko)) < 4294967296
 2. \<And>k. \<lbrakk>k * 2 ^ obj_bits ko < 4294967296; unat (mask (obj_bits ko)) < 4294967296; 0 < k; obj_bits ko = 32\<rbrakk> \<Longrightarrow> k * 2 ^ obj_bits ko + unat (mask (obj_bits ko)) < 4294967296 proof (prove)
goal (2 subgoals):
 1. \<And>k. \<lbrakk>k * 2 ^ obj_bits ko < 4294967296; unat (mask (obj_bits ko)) < 4294967296; 0 < k; obj_bits ko = 32\<rbrakk> \<Longrightarrow> k * 2 ^ obj_bits ko + unat (mask (obj_bits ko)) < 4294967296
 2. \<And>k. \<lbrakk>k * 2 ^ obj_bits ko < 4294967296; unat (mask (obj_bits ko)) < 4294967296; 0 < k; obj_bits ko < 32\<rbrakk> \<Longrightarrow> k * 2 ^ obj_bits ko + unat (mask (obj_bits ko)) < 4294967296 proof (prove)
goal (1 subgoal):
 1. \<And>k. \<lbrakk>k * 2 ^ obj_bits ko < 4294967296; unat (mask (obj_bits ko)) < 4294967296; 0 < k; obj_bits ko < 32\<rbrakk> \<Longrightarrow> k * 2 ^ obj_bits ko + unat (mask (obj_bits ko)) < 4294967296 proof (prove)
goal (1 subgoal):
 1. \<And>k. \<lbrakk>k * 2 ^ obj_bits ko < 4294967296; unat (mask (obj_bits ko)) < 4294967296; 0 < k; obj_bits ko \<le> 31\<rbrakk> \<Longrightarrow> k * 2 ^ obj_bits ko + unat (mask (obj_bits ko)) < 4294967296 proof (prove)
goal (1 subgoal):
 1. \<And>k. \<lbrakk>k * 2 ^ obj_bits ko < 4294967296; 2 ^ obj_bits ko - Suc 0 < 4294967296; 0 < k; obj_bits ko \<le> 31\<rbrakk> \<Longrightarrow> k * 2 ^ obj_bits ko + 2 ^ obj_bits ko - Suc 0 < 4294967296 proof (prove)
goal (2 subgoals):
 1. \<And>k. \<lbrakk>k * 2 ^ obj_bits ko < 4294967296; 2 ^ obj_bits ko - Suc 0 < 4294967296; 0 < k; obj_bits ko \<le> 31\<rbrakk> \<Longrightarrow> 0 < 2 ^ obj_bits ko \<and> k < 2 ^ (32 - obj_bits ko)
 2. \<And>k. \<lbrakk>k * 2 ^ obj_bits ko < 4294967296; 2 ^ obj_bits ko - Suc 0 < 4294967296; 0 < k; obj_bits ko \<le> 31; 2 ^ obj_bits ko + k * 2 ^ obj_bits ko \<le> 2 ^ (32 - obj_bits ko) * 2 ^ obj_bits ko\<rbrakk> \<Longrightarrow> k * 2 ^ obj_bits ko + 2 ^ obj_bits ko - Suc 0 < 4294967296 proof (prove)
goal (1 subgoal):
 1. \<And>k. \<lbrakk>k * 2 ^ obj_bits ko < 4294967296; 2 ^ obj_bits ko - Suc 0 < 4294967296; 0 < k; obj_bits ko \<le> 31\<rbrakk> \<Longrightarrow> k < 2 ^ (32 - obj_bits ko) proof (prove)
goal (1 subgoal):
 1. \<And>k. \<lbrakk>k * 2 ^ obj_bits ko < 4294967296; 2 ^ obj_bits ko - Suc 0 < 4294967296; 0 < k; obj_bits ko \<le> 31; \<not> k < 2 ^ (32 - obj_bits ko)\<rbrakk> \<Longrightarrow> False proof (prove)
goal (1 subgoal):
 1. \<And>k. \<lbrakk>k * 2 ^ obj_bits ko < 4294967296; 2 ^ obj_bits ko - Suc 0 < 4294967296; 0 < k; obj_bits ko \<le> 31; 2 ^ (32 - obj_bits ko) \<le> k\<rbrakk> \<Longrightarrow> False proof (prove)
goal (1 subgoal):
 1. \<And>k. \<lbrakk>k * 2 ^ obj_bits ko < 4294967296; 2 ^ obj_bits ko - Suc 0 < 4294967296; 0 < k; obj_bits ko \<le> 31; 2 ^ (32 - obj_bits ko) < k \<or> 2 ^ (32 - obj_bits ko) = k\<rbrakk> \<Longrightarrow> False proof (prove)
goal (2 subgoals):
 1. \<And>k. \<lbrakk>k * 2 ^ obj_bits ko < 4294967296; 2 ^ obj_bits ko - Suc 0 < 4294967296; 0 < k; obj_bits ko \<le> 31; 2 ^ (32 - obj_bits ko) < k\<rbrakk> \<Longrightarrow> False
 2. \<And>k. \<lbrakk>k * 2 ^ obj_bits ko < 4294967296; 2 ^ obj_bits ko - Suc 0 < 4294967296; 0 < k; obj_bits ko \<le> 31; 2 ^ (32 - obj_bits ko) = k\<rbrakk> \<Longrightarrow> False proof (prove)
goal (2 subgoals):
 1. \<And>k. \<lbrakk>k * 2 ^ obj_bits ko < 4294967296; 2 ^ obj_bits ko - Suc 0 < 4294967296; 0 < k; obj_bits ko \<le> 31; 2 ^ (32 - obj_bits ko) = k\<rbrakk> \<Longrightarrow> False
 2. \<And>k. \<lbrakk>k * 2 ^ obj_bits ko < 4294967296; 2 ^ obj_bits ko - Suc 0 < 4294967296; 0 < k; obj_bits ko \<le> 31; 2 ^ (32 - obj_bits ko) < k\<rbrakk> \<Longrightarrow> False proof (prove)
goal (1 subgoal):
 1. \<And>k. \<lbrakk>k * 2 ^ obj_bits ko < 4294967296; 2 ^ obj_bits ko - Suc 0 < 4294967296; 0 < k; obj_bits ko \<le> 31; 2 ^ (32 - obj_bits ko) < k\<rbrakk> \<Longrightarrow> False proof (prove)
goal (1 subgoal):
 1. \<And>k. \<lbrakk>k * 2 ^ obj_bits ko < 4294967296; 2 ^ obj_bits ko - Suc 0 < 4294967296; obj_bits ko \<le> 31; 2 ^ (32 - obj_bits ko) < k\<rbrakk> \<Longrightarrow> False proof (prove)
goal (2 subgoals):
 1. \<And>k. \<lbrakk>k * 2 ^ obj_bits ko < 4294967296; 2 ^ obj_bits ko - Suc 0 < 4294967296; obj_bits ko \<le> 31\<rbrakk> \<Longrightarrow> 0 < 2 ^ obj_bits ko
 2. \<And>k. \<lbrakk>k * 2 ^ obj_bits ko < 4294967296; 2 ^ obj_bits ko - Suc 0 < 4294967296; obj_bits ko \<le> 31; 2 ^ (32 - obj_bits ko) * 2 ^ obj_bits ko < k * 2 ^ obj_bits ko\<rbrakk> \<Longrightarrow> False proof (prove)
goal:
No subgoals!