theory CSpace_I

lemma cte_refs_capRange:
  "\<lbrakk> s \<turnstile>' c; \<forall>irq. c \<noteq> IRQHandlerCap irq \<rbrakk> \<Longrightarrow> cte_refs' c x \<subseteq> capRange c" apply (cases c; simp add: capRange_def isCap_simps) apply (clarsimp dest!: valid_capAligned
                    simp: capAligned_def objBits_simps field_simps) apply (frule tcb_cte_cases_small) apply (intro conjI) apply (erule(1) is_aligned_no_wrap') apply (rule word_plus_mono_right[where z="2^tcbBlockSizeBits - 1", simplified field_simps]) apply (drule word_le_minus_one_leq, simp) apply (erule is_aligned_no_wrap'[where off="2^tcbBlockSizeBits - 1", simplified field_simps]) apply (drule word_le_minus_one_leq) apply simp defer
   \<comment> \<open>CNodeCap\<close> apply (clarsimp simp: objBits_simps capAligned_def dest!: valid_capAligned) apply (rename_tac word1 nat1 word2 nat2 x) apply (subgoal_tac "x * 2 ^ cteSizeBits < 2 ^ (cteSizeBits + nat1)") apply (intro conjI) apply (erule(1) is_aligned_no_wrap') apply (simp add: add_diff_eq[symmetric]) apply (rule word_plus_mono_right) apply simp apply (erule is_aligned_no_wrap') apply simp apply (simp add: power_add field_simps) apply (erule word_mult_less_mono1) apply (simp add: objBits_defs) apply (frule power_strict_increasing [where a="2 :: nat" and n="y + z" for y z]) apply simp apply (simp only: power_add) apply (simp add: word_bits_def)
  \<comment> \<open>Zombie\<close> apply (clarsimp simp: capAligned_def valid_cap'_def objBits_simps) apply (rename_tac word zombie_type nat x) apply (subgoal_tac "x * 2^cteSizeBits < 2 ^ zBits zombie_type") apply (intro conjI) apply (erule(1) is_aligned_no_wrap') apply (simp add: add_diff_eq[symmetric]) apply (rule word_plus_mono_right) apply simp apply (erule is_aligned_no_wrap') apply simp apply (case_tac zombie_type) apply simp apply (rule div_lt_mult) apply (simp add: objBits_defs) apply (erule order_less_le_trans) apply (simp add: word_le_nat_alt) apply (subst le_unat_uoi[where z=5]) apply simp apply simp apply (simp add: objBits_defs) apply (simp add: objBits_simps' power_add mult.commute) apply (rule word_mult_less_mono1) apply (erule order_less_le_trans) apply (simp add: word_le_nat_alt) apply (subst le_unat_uoi) apply (subst unat_power_lower) prefer 2 apply assumption apply (simp add: word_bits_def) apply (simp add: word_bits_def) apply simp apply (frule power_strict_increasing [where a="2 :: nat" and n="y + z" for y z]) apply simp apply (simp only: power_add) apply (simp add: word_bits_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>valid_cap' c s; \<forall>irq. c \<noteq> capability.IRQHandlerCap irq\<rbrakk> \<Longrightarrow> cte_refs' c x \<subseteq> capRange c proof (prove)
goal (3 subgoals):
 1. \<And>x1. \<lbrakk>valid_cap' (capability.ThreadCap x1) s; c = capability.ThreadCap x1\<rbrakk> \<Longrightarrow> (+) x1 ` dom tcb_cte_cases \<subseteq> {x1..x1 + 2 ^ objBits undefined - 1}
 2. \<And>x71 x72 x73. \<lbrakk>valid_cap' (capability.Zombie x71 x72 x73) s; c = capability.Zombie x71 x72 x73\<rbrakk> \<Longrightarrow> (\<lambda>x. x71 + x * 2 ^ cteSizeBits) ` {0..<word_of_nat x73} \<subseteq> {x71..x71 + 2 ^ zBits x72 - 1}
 3. \<And>x111 x112 x113 x114. \<lbrakk>valid_cap' (capability.CNodeCap x111 x112 x113 x114) s; c = capability.CNodeCap x111 x112 x113 x114\<rbrakk> \<Longrightarrow> (\<lambda>x. x111 + x * 2 ^ cteSizeBits) ` {0..2 ^ x112 - 1} \<subseteq> {x111..x111 + 2 ^ (objBits undefined + x112) - 1} proof (prove)
goal (3 subgoals):
 1. \<And>x1 xa a b. \<lbrakk>c = capability.ThreadCap x1; tcb_cte_cases xa = Some (a, b); is_aligned x1 tcbBlockSizeBits; tcbBlockSizeBits < word_bits\<rbrakk> \<Longrightarrow> x1 \<le> x1 + xa \<and> x1 + xa \<le> x1 + 2 ^ tcbBlockSizeBits - 1
 2. \<And>x71 x72 x73. \<lbrakk>valid_cap' (capability.Zombie x71 x72 x73) s; c = capability.Zombie x71 x72 x73\<rbrakk> \<Longrightarrow> (\<lambda>x. x71 + x * 2 ^ cteSizeBits) ` {0..<word_of_nat x73} \<subseteq> {x71..x71 + 2 ^ zBits x72 - 1}
 3. \<And>x111 x112 x113 x114. \<lbrakk>valid_cap' (capability.CNodeCap x111 x112 x113 x114) s; c = capability.CNodeCap x111 x112 x113 x114\<rbrakk> \<Longrightarrow> (\<lambda>x. x111 + x * 2 ^ cteSizeBits) ` {0..2 ^ x112 - 1} \<subseteq> {x111..x111 + 2 ^ (objBits undefined + x112) - 1} proof (prove)
goal (3 subgoals):
 1. \<And>x1 xa a b. \<lbrakk>c = capability.ThreadCap x1; tcb_cte_cases xa = Some (a, b); is_aligned x1 tcbBlockSizeBits; tcbBlockSizeBits < word_bits; xa < 2 ^ tcbBlockSizeBits\<rbrakk> \<Longrightarrow> x1 \<le> x1 + xa \<and> x1 + xa \<le> x1 + 2 ^ tcbBlockSizeBits - 1
 2. \<And>x71 x72 x73. \<lbrakk>valid_cap' (capability.Zombie x71 x72 x73) s; c = capability.Zombie x71 x72 x73\<rbrakk> \<Longrightarrow> (\<lambda>x. x71 + x * 2 ^ cteSizeBits) ` {0..<word_of_nat x73} \<subseteq> {x71..x71 + 2 ^ zBits x72 - 1}
 3. \<And>x111 x112 x113 x114. \<lbrakk>valid_cap' (capability.CNodeCap x111 x112 x113 x114) s; c = capability.CNodeCap x111 x112 x113 x114\<rbrakk> \<Longrightarrow> (\<lambda>x. x111 + x * 2 ^ cteSizeBits) ` {0..2 ^ x112 - 1} \<subseteq> {x111..x111 + 2 ^ (objBits undefined + x112) - 1} proof (prove)
goal (4 subgoals):
 1. \<And>x1 xa a b. \<lbrakk>c = capability.ThreadCap x1; tcb_cte_cases xa = Some (a, b); is_aligned x1 tcbBlockSizeBits; tcbBlockSizeBits < word_bits; xa < 2 ^ tcbBlockSizeBits\<rbrakk> \<Longrightarrow> x1 \<le> x1 + xa
 2. \<And>x1 xa a b. \<lbrakk>c = capability.ThreadCap x1; tcb_cte_cases xa = Some (a, b); is_aligned x1 tcbBlockSizeBits; tcbBlockSizeBits < word_bits; xa < 2 ^ tcbBlockSizeBits\<rbrakk> \<Longrightarrow> x1 + xa \<le> x1 + 2 ^ tcbBlockSizeBits - 1
 3. \<And>x71 x72 x73. \<lbrakk>valid_cap' (capability.Zombie x71 x72 x73) s; c = capability.Zombie x71 x72 x73\<rbrakk> \<Longrightarrow> (\<lambda>x. x71 + x * 2 ^ cteSizeBits) ` {0..<word_of_nat x73} \<subseteq> {x71..x71 + 2 ^ zBits x72 - 1}
 4. \<And>x111 x112 x113 x114. \<lbrakk>valid_cap' (capability.CNodeCap x111 x112 x113 x114) s; c = capability.CNodeCap x111 x112 x113 x114\<rbrakk> \<Longrightarrow> (\<lambda>x. x111 + x * 2 ^ cteSizeBits) ` {0..2 ^ x112 - 1} \<subseteq> {x111..x111 + 2 ^ (objBits undefined + x112) - 1} proof (prove)
goal (3 subgoals):
 1. \<And>x1 xa a b. \<lbrakk>c = capability.ThreadCap x1; tcb_cte_cases xa = Some (a, b); is_aligned x1 tcbBlockSizeBits; tcbBlockSizeBits < word_bits; xa < 2 ^ tcbBlockSizeBits\<rbrakk> \<Longrightarrow> x1 + xa \<le> x1 + 2 ^ tcbBlockSizeBits - 1
 2. \<And>x71 x72 x73. \<lbrakk>valid_cap' (capability.Zombie x71 x72 x73) s; c = capability.Zombie x71 x72 x73\<rbrakk> \<Longrightarrow> (\<lambda>x. x71 + x * 2 ^ cteSizeBits) ` {0..<word_of_nat x73} \<subseteq> {x71..x71 + 2 ^ zBits x72 - 1}
 3. \<And>x111 x112 x113 x114. \<lbrakk>valid_cap' (capability.CNodeCap x111 x112 x113 x114) s; c = capability.CNodeCap x111 x112 x113 x114\<rbrakk> \<Longrightarrow> (\<lambda>x. x111 + x * 2 ^ cteSizeBits) ` {0..2 ^ x112 - 1} \<subseteq> {x111..x111 + 2 ^ (objBits undefined + x112) - 1} proof (prove)
goal (4 subgoals):
 1. \<And>x1 xa a b. \<lbrakk>c = capability.ThreadCap x1; tcb_cte_cases xa = Some (a, b); is_aligned x1 tcbBlockSizeBits; tcbBlockSizeBits < word_bits; xa < 2 ^ tcbBlockSizeBits\<rbrakk> \<Longrightarrow> xa \<le> 2 ^ tcbBlockSizeBits - 1
 2. \<And>x1 xa a b. \<lbrakk>c = capability.ThreadCap x1; tcb_cte_cases xa = Some (a, b); is_aligned x1 tcbBlockSizeBits; tcbBlockSizeBits < word_bits; xa < 2 ^ tcbBlockSizeBits\<rbrakk> \<Longrightarrow> x1 \<le> x1 + 2 ^ tcbBlockSizeBits - 1
 3. \<And>x71 x72 x73. \<lbrakk>valid_cap' (capability.Zombie x71 x72 x73) s; c = capability.Zombie x71 x72 x73\<rbrakk> \<Longrightarrow> (\<lambda>x. x71 + x * 2 ^ cteSizeBits) ` {0..<word_of_nat x73} \<subseteq> {x71..x71 + 2 ^ zBits x72 - 1}
 4. \<And>x111 x112 x113 x114. \<lbrakk>valid_cap' (capability.CNodeCap x111 x112 x113 x114) s; c = capability.CNodeCap x111 x112 x113 x114\<rbrakk> \<Longrightarrow> (\<lambda>x. x111 + x * 2 ^ cteSizeBits) ` {0..2 ^ x112 - 1} \<subseteq> {x111..x111 + 2 ^ (objBits undefined + x112) - 1} proof (prove)
goal (3 subgoals):
 1. \<And>x1 xa a b. \<lbrakk>c = capability.ThreadCap x1; tcb_cte_cases xa = Some (a, b); is_aligned x1 tcbBlockSizeBits; tcbBlockSizeBits < word_bits; xa < 2 ^ tcbBlockSizeBits\<rbrakk> \<Longrightarrow> x1 \<le> x1 + 2 ^ tcbBlockSizeBits - 1
 2. \<And>x71 x72 x73. \<lbrakk>valid_cap' (capability.Zombie x71 x72 x73) s; c = capability.Zombie x71 x72 x73\<rbrakk> \<Longrightarrow> (\<lambda>x. x71 + x * 2 ^ cteSizeBits) ` {0..<word_of_nat x73} \<subseteq> {x71..x71 + 2 ^ zBits x72 - 1}
 3. \<And>x111 x112 x113 x114. \<lbrakk>valid_cap' (capability.CNodeCap x111 x112 x113 x114) s; c = capability.CNodeCap x111 x112 x113 x114\<rbrakk> \<Longrightarrow> (\<lambda>x. x111 + x * 2 ^ cteSizeBits) ` {0..2 ^ x112 - 1} \<subseteq> {x111..x111 + 2 ^ (objBits undefined + x112) - 1} proof (prove)
goal (3 subgoals):
 1. \<And>x1 xa a b. \<lbrakk>c = capability.ThreadCap x1; tcb_cte_cases xa = Some (a, b); tcbBlockSizeBits < word_bits; xa < 2 ^ tcbBlockSizeBits\<rbrakk> \<Longrightarrow> 2 ^ tcbBlockSizeBits - 1 < 2 ^ tcbBlockSizeBits
 2. \<And>x71 x72 x73. \<lbrakk>valid_cap' (capability.Zombie x71 x72 x73) s; c = capability.Zombie x71 x72 x73\<rbrakk> \<Longrightarrow> (\<lambda>x. x71 + x * 2 ^ cteSizeBits) ` {0..<word_of_nat x73} \<subseteq> {x71..x71 + 2 ^ zBits x72 - 1}
 3. \<And>x111 x112 x113 x114. \<lbrakk>valid_cap' (capability.CNodeCap x111 x112 x113 x114) s; c = capability.CNodeCap x111 x112 x113 x114\<rbrakk> \<Longrightarrow> (\<lambda>x. x111 + x * 2 ^ cteSizeBits) ` {0..2 ^ x112 - 1} \<subseteq> {x111..x111 + 2 ^ (objBits undefined + x112) - 1} proof (prove)
goal (3 subgoals):
 1. \<And>x1 xa a b. \<lbrakk>c = capability.ThreadCap x1; tcb_cte_cases xa = Some (a, b); tcbBlockSizeBits < word_bits; xa \<le> 2 ^ tcbBlockSizeBits - 1\<rbrakk> \<Longrightarrow> 2 ^ tcbBlockSizeBits - 1 < 2 ^ tcbBlockSizeBits
 2. \<And>x71 x72 x73. \<lbrakk>valid_cap' (capability.Zombie x71 x72 x73) s; c = capability.Zombie x71 x72 x73\<rbrakk> \<Longrightarrow> (\<lambda>x. x71 + x * 2 ^ cteSizeBits) ` {0..<word_of_nat x73} \<subseteq> {x71..x71 + 2 ^ zBits x72 - 1}
 3. \<And>x111 x112 x113 x114. \<lbrakk>valid_cap' (capability.CNodeCap x111 x112 x113 x114) s; c = capability.CNodeCap x111 x112 x113 x114\<rbrakk> \<Longrightarrow> (\<lambda>x. x111 + x * 2 ^ cteSizeBits) ` {0..2 ^ x112 - 1} \<subseteq> {x111..x111 + 2 ^ (objBits undefined + x112) - 1} proof (prove)
goal (2 subgoals):
 1. \<And>x71 x72 x73. \<lbrakk>valid_cap' (capability.Zombie x71 x72 x73) s; c = capability.Zombie x71 x72 x73\<rbrakk> \<Longrightarrow> (\<lambda>x. x71 + x * 2 ^ cteSizeBits) ` {0..<word_of_nat x73} \<subseteq> {x71..x71 + 2 ^ zBits x72 - 1}
 2. \<And>x111 x112 x113 x114. \<lbrakk>valid_cap' (capability.CNodeCap x111 x112 x113 x114) s; c = capability.CNodeCap x111 x112 x113 x114\<rbrakk> \<Longrightarrow> (\<lambda>x. x111 + x * 2 ^ cteSizeBits) ` {0..2 ^ x112 - 1} \<subseteq> {x111..x111 + 2 ^ (objBits undefined + x112) - 1} proof (prove)
goal (2 subgoals):
 1. \<And>x111 x112 x113 x114. \<lbrakk>valid_cap' (capability.CNodeCap x111 x112 x113 x114) s; c = capability.CNodeCap x111 x112 x113 x114\<rbrakk> \<Longrightarrow> (\<lambda>x. x111 + x * 2 ^ cteSizeBits) ` {0..2 ^ x112 - 1} \<subseteq> {x111..x111 + 2 ^ (objBits undefined + x112) - 1}
 2. \<And>x71 x72 x73. \<lbrakk>valid_cap' (capability.Zombie x71 x72 x73) s; c = capability.Zombie x71 x72 x73\<rbrakk> \<Longrightarrow> (\<lambda>x. x71 + x * 2 ^ cteSizeBits) ` {0..<word_of_nat x73} \<subseteq> {x71..x71 + 2 ^ zBits x72 - 1} proof (prove)
goal (2 subgoals):
 1. \<And>x111 x112 x113 x114 xa. \<lbrakk>c = capability.CNodeCap x111 x112 x113 x114; xa < 2 ^ x112; is_aligned x111 (cteSizeBits + x112); cteSizeBits + x112 < word_bits\<rbrakk> \<Longrightarrow> x111 \<le> x111 + xa * 2 ^ cteSizeBits \<and> x111 + xa * 2 ^ cteSizeBits \<le> x111 + 2 ^ (cteSizeBits + x112) - 1
 2. \<And>x71 x72 x73. \<lbrakk>valid_cap' (capability.Zombie x71 x72 x73) s; c = capability.Zombie x71 x72 x73\<rbrakk> \<Longrightarrow> (\<lambda>x. x71 + x * 2 ^ cteSizeBits) ` {0..<word_of_nat x73} \<subseteq> {x71..x71 + 2 ^ zBits x72 - 1} proof (prove)
goal (2 subgoals):
 1. \<And>word1 nat1 word2 nat2 x. \<lbrakk>c = capability.CNodeCap word1 nat1 word2 nat2; x < 2 ^ nat1; is_aligned word1 (cteSizeBits + nat1); cteSizeBits + nat1 < word_bits\<rbrakk> \<Longrightarrow> word1 \<le> word1 + x * 2 ^ cteSizeBits \<and> word1 + x * 2 ^ cteSizeBits \<le> word1 + 2 ^ (cteSizeBits + nat1) - 1
 2. \<And>x71 x72 x73. \<lbrakk>valid_cap' (capability.Zombie x71 x72 x73) s; c = capability.Zombie x71 x72 x73\<rbrakk> \<Longrightarrow> (\<lambda>x. x71 + x * 2 ^ cteSizeBits) ` {0..<word_of_nat x73} \<subseteq> {x71..x71 + 2 ^ zBits x72 - 1} proof (prove)
goal (3 subgoals):
 1. \<And>word1 nat1 word2 nat2 x. \<lbrakk>c = capability.CNodeCap word1 nat1 word2 nat2; x < 2 ^ nat1; is_aligned word1 (cteSizeBits + nat1); cteSizeBits + nat1 < word_bits; x * 2 ^ cteSizeBits < 2 ^ (cteSizeBits + nat1)\<rbrakk> \<Longrightarrow> word1 \<le> word1 + x * 2 ^ cteSizeBits \<and> word1 + x * 2 ^ cteSizeBits \<le> word1 + 2 ^ (cteSizeBits + nat1) - 1
 2. \<And>word1 nat1 word2 nat2 x. \<lbrakk>c = capability.CNodeCap word1 nat1 word2 nat2; x < 2 ^ nat1; is_aligned word1 (cteSizeBits + nat1); cteSizeBits + nat1 < word_bits\<rbrakk> \<Longrightarrow> x * 2 ^ cteSizeBits < 2 ^ (cteSizeBits + nat1)
 3. \<And>x71 x72 x73. \<lbrakk>valid_cap' (capability.Zombie x71 x72 x73) s; c = capability.Zombie x71 x72 x73\<rbrakk> \<Longrightarrow> (\<lambda>x. x71 + x * 2 ^ cteSizeBits) ` {0..<word_of_nat x73} \<subseteq> {x71..x71 + 2 ^ zBits x72 - 1} proof (prove)
goal (4 subgoals):
 1. \<And>word1 nat1 word2 nat2 x. \<lbrakk>c = capability.CNodeCap word1 nat1 word2 nat2; x < 2 ^ nat1; is_aligned word1 (cteSizeBits + nat1); cteSizeBits + nat1 < word_bits; x * 2 ^ cteSizeBits < 2 ^ (cteSizeBits + nat1)\<rbrakk> \<Longrightarrow> word1 \<le> word1 + x * 2 ^ cteSizeBits
 2. \<And>word1 nat1 word2 nat2 x. \<lbrakk>c = capability.CNodeCap word1 nat1 word2 nat2; x < 2 ^ nat1; is_aligned word1 (cteSizeBits + nat1); cteSizeBits + nat1 < word_bits; x * 2 ^ cteSizeBits < 2 ^ (cteSizeBits + nat1)\<rbrakk> \<Longrightarrow> word1 + x * 2 ^ cteSizeBits \<le> word1 + 2 ^ (cteSizeBits + nat1) - 1
 3. \<And>word1 nat1 word2 nat2 x. \<lbrakk>c = capability.CNodeCap word1 nat1 word2 nat2; x < 2 ^ nat1; is_aligned word1 (cteSizeBits + nat1); cteSizeBits + nat1 < word_bits\<rbrakk> \<Longrightarrow> x * 2 ^ cteSizeBits < 2 ^ (cteSizeBits + nat1)
 4. \<And>x71 x72 x73. \<lbrakk>valid_cap' (capability.Zombie x71 x72 x73) s; c = capability.Zombie x71 x72 x73\<rbrakk> \<Longrightarrow> (\<lambda>x. x71 + x * 2 ^ cteSizeBits) ` {0..<word_of_nat x73} \<subseteq> {x71..x71 + 2 ^ zBits x72 - 1} proof (prove)
goal (3 subgoals):
 1. \<And>word1 nat1 word2 nat2 x. \<lbrakk>c = capability.CNodeCap word1 nat1 word2 nat2; x < 2 ^ nat1; is_aligned word1 (cteSizeBits + nat1); cteSizeBits + nat1 < word_bits; x * 2 ^ cteSizeBits < 2 ^ (cteSizeBits + nat1)\<rbrakk> \<Longrightarrow> word1 + x * 2 ^ cteSizeBits \<le> word1 + 2 ^ (cteSizeBits + nat1) - 1
 2. \<And>word1 nat1 word2 nat2 x. \<lbrakk>c = capability.CNodeCap word1 nat1 word2 nat2; x < 2 ^ nat1; is_aligned word1 (cteSizeBits + nat1); cteSizeBits + nat1 < word_bits\<rbrakk> \<Longrightarrow> x * 2 ^ cteSizeBits < 2 ^ (cteSizeBits + nat1)
 3. \<And>x71 x72 x73. \<lbrakk>valid_cap' (capability.Zombie x71 x72 x73) s; c = capability.Zombie x71 x72 x73\<rbrakk> \<Longrightarrow> (\<lambda>x. x71 + x * 2 ^ cteSizeBits) ` {0..<word_of_nat x73} \<subseteq> {x71..x71 + 2 ^ zBits x72 - 1} proof (prove)
goal (3 subgoals):
 1. \<And>word1 nat1 word2 nat2 x. \<lbrakk>c = capability.CNodeCap word1 nat1 word2 nat2; x < 2 ^ nat1; is_aligned word1 (cteSizeBits + nat1); cteSizeBits + nat1 < word_bits; x * 2 ^ cteSizeBits < 2 ^ (cteSizeBits + nat1)\<rbrakk> \<Longrightarrow> word1 + x * 2 ^ cteSizeBits \<le> word1 + (2 ^ (cteSizeBits + nat1) - 1)
 2. \<And>word1 nat1 word2 nat2 x. \<lbrakk>c = capability.CNodeCap word1 nat1 word2 nat2; x < 2 ^ nat1; is_aligned word1 (cteSizeBits + nat1); cteSizeBits + nat1 < word_bits\<rbrakk> \<Longrightarrow> x * 2 ^ cteSizeBits < 2 ^ (cteSizeBits + nat1)
 3. \<And>x71 x72 x73. \<lbrakk>valid_cap' (capability.Zombie x71 x72 x73) s; c = capability.Zombie x71 x72 x73\<rbrakk> \<Longrightarrow> (\<lambda>x. x71 + x * 2 ^ cteSizeBits) ` {0..<word_of_nat x73} \<subseteq> {x71..x71 + 2 ^ zBits x72 - 1} proof (prove)
goal (4 subgoals):
 1. \<And>word1 nat1 word2 nat2 x. \<lbrakk>c = capability.CNodeCap word1 nat1 word2 nat2; x < 2 ^ nat1; is_aligned word1 (cteSizeBits + nat1); cteSizeBits + nat1 < word_bits; x * 2 ^ cteSizeBits < 2 ^ (cteSizeBits + nat1)\<rbrakk> \<Longrightarrow> x * 2 ^ cteSizeBits \<le> 2 ^ (cteSizeBits + nat1) - 1
 2. \<And>word1 nat1 word2 nat2 x. \<lbrakk>c = capability.CNodeCap word1 nat1 word2 nat2; x < 2 ^ nat1; is_aligned word1 (cteSizeBits + nat1); cteSizeBits + nat1 < word_bits; x * 2 ^ cteSizeBits < 2 ^ (cteSizeBits + nat1)\<rbrakk> \<Longrightarrow> word1 \<le> word1 + (2 ^ (cteSizeBits + nat1) - 1)
 3. \<And>word1 nat1 word2 nat2 x. \<lbrakk>c = capability.CNodeCap word1 nat1 word2 nat2; x < 2 ^ nat1; is_aligned word1 (cteSizeBits + nat1); cteSizeBits + nat1 < word_bits\<rbrakk> \<Longrightarrow> x * 2 ^ cteSizeBits < 2 ^ (cteSizeBits + nat1)
 4. \<And>x71 x72 x73. \<lbrakk>valid_cap' (capability.Zombie x71 x72 x73) s; c = capability.Zombie x71 x72 x73\<rbrakk> \<Longrightarrow> (\<lambda>x. x71 + x * 2 ^ cteSizeBits) ` {0..<word_of_nat x73} \<subseteq> {x71..x71 + 2 ^ zBits x72 - 1} proof (prove)
goal (3 subgoals):
 1. \<And>word1 nat1 word2 nat2 x. \<lbrakk>c = capability.CNodeCap word1 nat1 word2 nat2; x < 2 ^ nat1; is_aligned word1 (cteSizeBits + nat1); cteSizeBits + nat1 < word_bits; x * 2 ^ cteSizeBits < 2 ^ (cteSizeBits + nat1)\<rbrakk> \<Longrightarrow> word1 \<le> word1 + (2 ^ (cteSizeBits + nat1) - 1)
 2. \<And>word1 nat1 word2 nat2 x. \<lbrakk>c = capability.CNodeCap word1 nat1 word2 nat2; x < 2 ^ nat1; is_aligned word1 (cteSizeBits + nat1); cteSizeBits + nat1 < word_bits\<rbrakk> \<Longrightarrow> x * 2 ^ cteSizeBits < 2 ^ (cteSizeBits + nat1)
 3. \<And>x71 x72 x73. \<lbrakk>valid_cap' (capability.Zombie x71 x72 x73) s; c = capability.Zombie x71 x72 x73\<rbrakk> \<Longrightarrow> (\<lambda>x. x71 + x * 2 ^ cteSizeBits) ` {0..<word_of_nat x73} \<subseteq> {x71..x71 + 2 ^ zBits x72 - 1} proof (prove)
goal (3 subgoals):
 1. \<And>word1 nat1 word2 nat2 x. \<lbrakk>c = capability.CNodeCap word1 nat1 word2 nat2; x < 2 ^ nat1; cteSizeBits + nat1 < word_bits; x * 2 ^ cteSizeBits < 2 ^ (cteSizeBits + nat1)\<rbrakk> \<Longrightarrow> 2 ^ (cteSizeBits + nat1) - 1 < 2 ^ (cteSizeBits + nat1)
 2. \<And>word1 nat1 word2 nat2 x. \<lbrakk>c = capability.CNodeCap word1 nat1 word2 nat2; x < 2 ^ nat1; is_aligned word1 (cteSizeBits + nat1); cteSizeBits + nat1 < word_bits\<rbrakk> \<Longrightarrow> x * 2 ^ cteSizeBits < 2 ^ (cteSizeBits + nat1)
 3. \<And>x71 x72 x73. \<lbrakk>valid_cap' (capability.Zombie x71 x72 x73) s; c = capability.Zombie x71 x72 x73\<rbrakk> \<Longrightarrow> (\<lambda>x. x71 + x * 2 ^ cteSizeBits) ` {0..<word_of_nat x73} \<subseteq> {x71..x71 + 2 ^ zBits x72 - 1} proof (prove)
goal (2 subgoals):
 1. \<And>word1 nat1 word2 nat2 x. \<lbrakk>c = capability.CNodeCap word1 nat1 word2 nat2; x < 2 ^ nat1; is_aligned word1 (cteSizeBits + nat1); cteSizeBits + nat1 < word_bits\<rbrakk> \<Longrightarrow> x * 2 ^ cteSizeBits < 2 ^ (cteSizeBits + nat1)
 2. \<And>x71 x72 x73. \<lbrakk>valid_cap' (capability.Zombie x71 x72 x73) s; c = capability.Zombie x71 x72 x73\<rbrakk> \<Longrightarrow> (\<lambda>x. x71 + x * 2 ^ cteSizeBits) ` {0..<word_of_nat x73} \<subseteq> {x71..x71 + 2 ^ zBits x72 - 1} proof (prove)
goal (2 subgoals):
 1. \<And>word1 nat1 word2 nat2 x. \<lbrakk>c = capability.CNodeCap word1 nat1 word2 nat2; x < 2 ^ nat1; is_aligned word1 (nat1 + cteSizeBits); nat1 + cteSizeBits < word_bits\<rbrakk> \<Longrightarrow> x * 2 ^ cteSizeBits < 2 ^ nat1 * 2 ^ cteSizeBits
 2. \<And>x71 x72 x73. \<lbrakk>valid_cap' (capability.Zombie x71 x72 x73) s; c = capability.Zombie x71 x72 x73\<rbrakk> \<Longrightarrow> (\<lambda>x. x71 + x * 2 ^ cteSizeBits) ` {0..<word_of_nat x73} \<subseteq> {x71..x71 + 2 ^ zBits x72 - 1} proof (prove)
goal (3 subgoals):
 1. \<And>word1 nat1 word2 nat2 x. \<lbrakk>c = capability.CNodeCap word1 nat1 word2 nat2; is_aligned word1 (nat1 + cteSizeBits); nat1 + cteSizeBits < word_bits\<rbrakk> \<Longrightarrow> 0 < 2 ^ cteSizeBits
 2. \<And>word1 nat1 word2 nat2 x. \<lbrakk>c = capability.CNodeCap word1 nat1 word2 nat2; is_aligned word1 (nat1 + cteSizeBits); nat1 + cteSizeBits < word_bits\<rbrakk> \<Longrightarrow> unat (2 ^ nat1) * unat (2 ^ cteSizeBits) < 2 ^ LENGTH(32)
 3. \<And>x71 x72 x73. \<lbrakk>valid_cap' (capability.Zombie x71 x72 x73) s; c = capability.Zombie x71 x72 x73\<rbrakk> \<Longrightarrow> (\<lambda>x. x71 + x * 2 ^ cteSizeBits) ` {0..<word_of_nat x73} \<subseteq> {x71..x71 + 2 ^ zBits x72 - 1} proof (prove)
goal (2 subgoals):
 1. \<And>word1 nat1 word2 nat2 x. \<lbrakk>c = capability.CNodeCap word1 nat1 word2 nat2; is_aligned word1 (nat1 + cteSizeBits); nat1 + cteSizeBits < word_bits\<rbrakk> \<Longrightarrow> unat (2 ^ nat1) * unat (2 ^ cteSizeBits) < 2 ^ LENGTH(32)
 2. \<And>x71 x72 x73. \<lbrakk>valid_cap' (capability.Zombie x71 x72 x73) s; c = capability.Zombie x71 x72 x73\<rbrakk> \<Longrightarrow> (\<lambda>x. x71 + x * 2 ^ cteSizeBits) ` {0..<word_of_nat x73} \<subseteq> {x71..x71 + 2 ^ zBits x72 - 1} proof (prove)
goal (3 subgoals):
 1. \<And>word1 nat1 word2 nat2 x. \<lbrakk>c = capability.CNodeCap word1 nat1 word2 nat2; is_aligned word1 (nat1 + cteSizeBits); nat1 + cteSizeBits < word_bits\<rbrakk> \<Longrightarrow> 1 < 2
 2. \<And>word1 nat1 word2 nat2 x. \<lbrakk>c = capability.CNodeCap word1 nat1 word2 nat2; is_aligned word1 (nat1 + cteSizeBits); nat1 + cteSizeBits < word_bits; 2 ^ (nat1 + cteSizeBits) < 2 ^ word_bits\<rbrakk> \<Longrightarrow> unat (2 ^ nat1) * unat (2 ^ cteSizeBits) < 2 ^ LENGTH(32)
 3. \<And>x71 x72 x73. \<lbrakk>valid_cap' (capability.Zombie x71 x72 x73) s; c = capability.Zombie x71 x72 x73\<rbrakk> \<Longrightarrow> (\<lambda>x. x71 + x * 2 ^ cteSizeBits) ` {0..<word_of_nat x73} \<subseteq> {x71..x71 + 2 ^ zBits x72 - 1} proof (prove)
goal (2 subgoals):
 1. \<And>word1 nat1 word2 nat2 x. \<lbrakk>c = capability.CNodeCap word1 nat1 word2 nat2; is_aligned word1 (nat1 + cteSizeBits); nat1 + cteSizeBits < word_bits; 2 ^ (nat1 + cteSizeBits) < 2 ^ word_bits\<rbrakk> \<Longrightarrow> unat (2 ^ nat1) * unat (2 ^ cteSizeBits) < 2 ^ LENGTH(32)
 2. \<And>x71 x72 x73. \<lbrakk>valid_cap' (capability.Zombie x71 x72 x73) s; c = capability.Zombie x71 x72 x73\<rbrakk> \<Longrightarrow> (\<lambda>x. x71 + x * 2 ^ cteSizeBits) ` {0..<word_of_nat x73} \<subseteq> {x71..x71 + 2 ^ zBits x72 - 1} proof (prove)
goal (2 subgoals):
 1. \<And>word1 nat1 word2 nat2 x. \<lbrakk>c = capability.CNodeCap word1 nat1 word2 nat2; is_aligned word1 (nat1 + cteSizeBits); nat1 + cteSizeBits < word_bits; 2 ^ nat1 * 2 ^ cteSizeBits < 2 ^ word_bits\<rbrakk> \<Longrightarrow> unat (2 ^ nat1) * unat (2 ^ cteSizeBits) < 2 ^ LENGTH(32)
 2. \<And>x71 x72 x73. \<lbrakk>valid_cap' (capability.Zombie x71 x72 x73) s; c = capability.Zombie x71 x72 x73\<rbrakk> \<Longrightarrow> (\<lambda>x. x71 + x * 2 ^ cteSizeBits) ` {0..<word_of_nat x73} \<subseteq> {x71..x71 + 2 ^ zBits x72 - 1} proof (prove)
goal (1 subgoal):
 1. \<And>x71 x72 x73. \<lbrakk>valid_cap' (capability.Zombie x71 x72 x73) s; c = capability.Zombie x71 x72 x73\<rbrakk> \<Longrightarrow> (\<lambda>x. x71 + x * 2 ^ cteSizeBits) ` {0..<word_of_nat x73} \<subseteq> {x71..x71 + 2 ^ zBits x72 - 1} proof (prove)
goal (1 subgoal):
 1. \<And>x71 x72 x73 xa. \<lbrakk>c = capability.Zombie x71 x72 x73; xa < word_of_nat x73; is_aligned x71 (zBits x72); x73 \<le> zombieCTEs x72; zBits x72 < word_bits; case x72 of ZombieTCB \<Rightarrow> tcb_at' x71 s | ZombieCNode n \<Rightarrow> n \<noteq> 0 \<and> (\<forall>addr. real_cte_at' (x71 + 2 ^ cteSizeBits * (addr && mask n)) s)\<rbrakk> \<Longrightarrow> x71 \<le> x71 + xa * 2 ^ cteSizeBits \<and> x71 + xa * 2 ^ cteSizeBits \<le> x71 + 2 ^ zBits x72 - 1 proof (prove)
goal (1 subgoal):
 1. \<And>word zombie_type nat x. \<lbrakk>c = capability.Zombie word zombie_type nat; x < word_of_nat nat; is_aligned word (zBits zombie_type); nat \<le> zombieCTEs zombie_type; zBits zombie_type < word_bits; case zombie_type of ZombieTCB \<Rightarrow> tcb_at' word s | ZombieCNode n \<Rightarrow> n \<noteq> 0 \<and> (\<forall>addr. real_cte_at' (word + 2 ^ cteSizeBits * (addr && mask n)) s)\<rbrakk> \<Longrightarrow> word \<le> word + x * 2 ^ cteSizeBits \<and> word + x * 2 ^ cteSizeBits \<le> word + 2 ^ zBits zombie_type - 1 proof (prove)
goal (2 subgoals):
 1. \<And>word zombie_type nat x. \<lbrakk>c = capability.Zombie word zombie_type nat; x < word_of_nat nat; is_aligned word (zBits zombie_type); nat \<le> zombieCTEs zombie_type; zBits zombie_type < word_bits; case zombie_type of ZombieTCB \<Rightarrow> tcb_at' word s | ZombieCNode n \<Rightarrow> n \<noteq> 0 \<and> (\<forall>addr. real_cte_at' (word + 2 ^ cteSizeBits * (addr && mask n)) s); x * 2 ^ cteSizeBits < 2 ^ zBits zombie_type\<rbrakk> \<Longrightarrow> word \<le> word + x * 2 ^ cteSizeBits \<and> word + x * 2 ^ cteSizeBits \<le> word + 2 ^ zBits zombie_type - 1
 2. \<And>word zombie_type nat x. \<lbrakk>c = capability.Zombie word zombie_type nat; x < word_of_nat nat; is_aligned word (zBits zombie_type); nat \<le> zombieCTEs zombie_type; zBits zombie_type < word_bits; case zombie_type of ZombieTCB \<Rightarrow> tcb_at' word s | ZombieCNode n \<Rightarrow> n \<noteq> 0 \<and> (\<forall>addr. real_cte_at' (word + 2 ^ cteSizeBits * (addr && mask n)) s)\<rbrakk> \<Longrightarrow> x * 2 ^ cteSizeBits < 2 ^ zBits zombie_type proof (prove)
goal (3 subgoals):
 1. \<And>word zombie_type nat x. \<lbrakk>c = capability.Zombie word zombie_type nat; x < word_of_nat nat; is_aligned word (zBits zombie_type); nat \<le> zombieCTEs zombie_type; zBits zombie_type < word_bits; case zombie_type of ZombieTCB \<Rightarrow> tcb_at' word s | ZombieCNode n \<Rightarrow> n \<noteq> 0 \<and> (\<forall>addr. real_cte_at' (word + 2 ^ cteSizeBits * (addr && mask n)) s); x * 2 ^ cteSizeBits < 2 ^ zBits zombie_type\<rbrakk> \<Longrightarrow> word \<le> word + x * 2 ^ cteSizeBits
 2. \<And>word zombie_type nat x. \<lbrakk>c = capability.Zombie word zombie_type nat; x < word_of_nat nat; is_aligned word (zBits zombie_type); nat \<le> zombieCTEs zombie_type; zBits zombie_type < word_bits; case zombie_type of ZombieTCB \<Rightarrow> tcb_at' word s | ZombieCNode n \<Rightarrow> n \<noteq> 0 \<and> (\<forall>addr. real_cte_at' (word + 2 ^ cteSizeBits * (addr && mask n)) s); x * 2 ^ cteSizeBits < 2 ^ zBits zombie_type\<rbrakk> \<Longrightarrow> word + x * 2 ^ cteSizeBits \<le> word + 2 ^ zBits zombie_type - 1
 3. \<And>word zombie_type nat x. \<lbrakk>c = capability.Zombie word zombie_type nat; x < word_of_nat nat; is_aligned word (zBits zombie_type); nat \<le> zombieCTEs zombie_type; zBits zombie_type < word_bits; case zombie_type of ZombieTCB \<Rightarrow> tcb_at' word s | ZombieCNode n \<Rightarrow> n \<noteq> 0 \<and> (\<forall>addr. real_cte_at' (word + 2 ^ cteSizeBits * (addr && mask n)) s)\<rbrakk> \<Longrightarrow> x * 2 ^ cteSizeBits < 2 ^ zBits zombie_type proof (prove)
goal (2 subgoals):
 1. \<And>word zombie_type nat x. \<lbrakk>c = capability.Zombie word zombie_type nat; x < word_of_nat nat; is_aligned word (zBits zombie_type); nat \<le> zombieCTEs zombie_type; zBits zombie_type < word_bits; case zombie_type of ZombieTCB \<Rightarrow> tcb_at' word s | ZombieCNode n \<Rightarrow> n \<noteq> 0 \<and> (\<forall>addr. real_cte_at' (word + 2 ^ cteSizeBits * (addr && mask n)) s); x * 2 ^ cteSizeBits < 2 ^ zBits zombie_type\<rbrakk> \<Longrightarrow> word + x * 2 ^ cteSizeBits \<le> word + 2 ^ zBits zombie_type - 1
 2. \<And>word zombie_type nat x. \<lbrakk>c = capability.Zombie word zombie_type nat; x < word_of_nat nat; is_aligned word (zBits zombie_type); nat \<le> zombieCTEs zombie_type; zBits zombie_type < word_bits; case zombie_type of ZombieTCB \<Rightarrow> tcb_at' word s | ZombieCNode n \<Rightarrow> n \<noteq> 0 \<and> (\<forall>addr. real_cte_at' (word + 2 ^ cteSizeBits * (addr && mask n)) s)\<rbrakk> \<Longrightarrow> x * 2 ^ cteSizeBits < 2 ^ zBits zombie_type proof (prove)
goal (2 subgoals):
 1. \<And>word zombie_type nat x. \<lbrakk>c = capability.Zombie word zombie_type nat; x < word_of_nat nat; is_aligned word (zBits zombie_type); nat \<le> zombieCTEs zombie_type; zBits zombie_type < word_bits; case zombie_type of ZombieTCB \<Rightarrow> tcb_at' word s | ZombieCNode n \<Rightarrow> n \<noteq> 0 \<and> (\<forall>addr. real_cte_at' (word + 2 ^ cteSizeBits * (addr && mask n)) s); x * 2 ^ cteSizeBits < 2 ^ zBits zombie_type\<rbrakk> \<Longrightarrow> word + x * 2 ^ cteSizeBits \<le> word + (2 ^ zBits zombie_type - 1)
 2. \<And>word zombie_type nat x. \<lbrakk>c = capability.Zombie word zombie_type nat; x < word_of_nat nat; is_aligned word (zBits zombie_type); nat \<le> zombieCTEs zombie_type; zBits zombie_type < word_bits; case zombie_type of ZombieTCB \<Rightarrow> tcb_at' word s | ZombieCNode n \<Rightarrow> n \<noteq> 0 \<and> (\<forall>addr. real_cte_at' (word + 2 ^ cteSizeBits * (addr && mask n)) s)\<rbrakk> \<Longrightarrow> x * 2 ^ cteSizeBits < 2 ^ zBits zombie_type proof (prove)
goal (3 subgoals):
 1. \<And>word zombie_type nat x. \<lbrakk>c = capability.Zombie word zombie_type nat; x < word_of_nat nat; is_aligned word (zBits zombie_type); nat \<le> zombieCTEs zombie_type; zBits zombie_type < word_bits; case zombie_type of ZombieTCB \<Rightarrow> tcb_at' word s | ZombieCNode n \<Rightarrow> n \<noteq> 0 \<and> (\<forall>addr. real_cte_at' (word + 2 ^ cteSizeBits * (addr && mask n)) s); x * 2 ^ cteSizeBits < 2 ^ zBits zombie_type\<rbrakk> \<Longrightarrow> x * 2 ^ cteSizeBits \<le> 2 ^ zBits zombie_type - 1
 2. \<And>word zombie_type nat x. \<lbrakk>c = capability.Zombie word zombie_type nat; x < word_of_nat nat; is_aligned word (zBits zombie_type); nat \<le> zombieCTEs zombie_type; zBits zombie_type < word_bits; case zombie_type of ZombieTCB \<Rightarrow> tcb_at' word s | ZombieCNode n \<Rightarrow> n \<noteq> 0 \<and> (\<forall>addr. real_cte_at' (word + 2 ^ cteSizeBits * (addr && mask n)) s); x * 2 ^ cteSizeBits < 2 ^ zBits zombie_type\<rbrakk> \<Longrightarrow> word \<le> word + (2 ^ zBits zombie_type - 1)
 3. \<And>word zombie_type nat x. \<lbrakk>c = capability.Zombie word zombie_type nat; x < word_of_nat nat; is_aligned word (zBits zombie_type); nat \<le> zombieCTEs zombie_type; zBits zombie_type < word_bits; case zombie_type of ZombieTCB \<Rightarrow> tcb_at' word s | ZombieCNode n \<Rightarrow> n \<noteq> 0 \<and> (\<forall>addr. real_cte_at' (word + 2 ^ cteSizeBits * (addr && mask n)) s)\<rbrakk> \<Longrightarrow> x * 2 ^ cteSizeBits < 2 ^ zBits zombie_type proof (prove)
goal (2 subgoals):
 1. \<And>word zombie_type nat x. \<lbrakk>c = capability.Zombie word zombie_type nat; x < word_of_nat nat; is_aligned word (zBits zombie_type); nat \<le> zombieCTEs zombie_type; zBits zombie_type < word_bits; case zombie_type of ZombieTCB \<Rightarrow> tcb_at' word s | ZombieCNode n \<Rightarrow> n \<noteq> 0 \<and> (\<forall>addr. real_cte_at' (word + 2 ^ cteSizeBits * (addr && mask n)) s); x * 2 ^ cteSizeBits < 2 ^ zBits zombie_type\<rbrakk> \<Longrightarrow> word \<le> word + (2 ^ zBits zombie_type - 1)
 2. \<And>word zombie_type nat x. \<lbrakk>c = capability.Zombie word zombie_type nat; x < word_of_nat nat; is_aligned word (zBits zombie_type); nat \<le> zombieCTEs zombie_type; zBits zombie_type < word_bits; case zombie_type of ZombieTCB \<Rightarrow> tcb_at' word s | ZombieCNode n \<Rightarrow> n \<noteq> 0 \<and> (\<forall>addr. real_cte_at' (word + 2 ^ cteSizeBits * (addr && mask n)) s)\<rbrakk> \<Longrightarrow> x * 2 ^ cteSizeBits < 2 ^ zBits zombie_type proof (prove)
goal (2 subgoals):
 1. \<And>word zombie_type nat x. \<lbrakk>c = capability.Zombie word zombie_type nat; x < word_of_nat nat; nat \<le> zombieCTEs zombie_type; zBits zombie_type < word_bits; case zombie_type of ZombieTCB \<Rightarrow> tcb_at' word s | ZombieCNode n \<Rightarrow> n \<noteq> 0 \<and> (\<forall>addr. real_cte_at' (word + 2 ^ cteSizeBits * (addr && mask n)) s); x * 2 ^ cteSizeBits < 2 ^ zBits zombie_type\<rbrakk> \<Longrightarrow> 2 ^ zBits zombie_type - 1 < 2 ^ zBits zombie_type
 2. \<And>word zombie_type nat x. \<lbrakk>c = capability.Zombie word zombie_type nat; x < word_of_nat nat; is_aligned word (zBits zombie_type); nat \<le> zombieCTEs zombie_type; zBits zombie_type < word_bits; case zombie_type of ZombieTCB \<Rightarrow> tcb_at' word s | ZombieCNode n \<Rightarrow> n \<noteq> 0 \<and> (\<forall>addr. real_cte_at' (word + 2 ^ cteSizeBits * (addr && mask n)) s)\<rbrakk> \<Longrightarrow> x * 2 ^ cteSizeBits < 2 ^ zBits zombie_type proof (prove)
goal (1 subgoal):
 1. \<And>word zombie_type nat x. \<lbrakk>c = capability.Zombie word zombie_type nat; x < word_of_nat nat; is_aligned word (zBits zombie_type); nat \<le> zombieCTEs zombie_type; zBits zombie_type < word_bits; case zombie_type of ZombieTCB \<Rightarrow> tcb_at' word s | ZombieCNode n \<Rightarrow> n \<noteq> 0 \<and> (\<forall>addr. real_cte_at' (word + 2 ^ cteSizeBits * (addr && mask n)) s)\<rbrakk> \<Longrightarrow> x * 2 ^ cteSizeBits < 2 ^ zBits zombie_type proof (prove)
goal (2 subgoals):
 1. \<And>word zombie_type nat x. \<lbrakk>c = capability.Zombie word zombie_type nat; x < word_of_nat nat; is_aligned word (zBits zombie_type); nat \<le> zombieCTEs zombie_type; zBits zombie_type < word_bits; case zombie_type of ZombieTCB \<Rightarrow> tcb_at' word s | ZombieCNode n \<Rightarrow> n \<noteq> 0 \<and> (\<forall>addr. real_cte_at' (word + 2 ^ cteSizeBits * (addr && mask n)) s); zombie_type = ZombieTCB\<rbrakk> \<Longrightarrow> x * 2 ^ cteSizeBits < 2 ^ zBits zombie_type
 2. \<And>word zombie_type nat x x2. \<lbrakk>c = capability.Zombie word zombie_type nat; x < word_of_nat nat; is_aligned word (zBits zombie_type); nat \<le> zombieCTEs zombie_type; zBits zombie_type < word_bits; case zombie_type of ZombieTCB \<Rightarrow> tcb_at' word s | ZombieCNode n \<Rightarrow> n \<noteq> 0 \<and> (\<forall>addr. real_cte_at' (word + 2 ^ cteSizeBits * (addr && mask n)) s); zombie_type = ZombieCNode x2\<rbrakk> \<Longrightarrow> x * 2 ^ cteSizeBits < 2 ^ zBits zombie_type proof (prove)
goal (2 subgoals):
 1. \<And>word zombie_type nat x. \<lbrakk>c = capability.Zombie word ZombieTCB nat; x < word_of_nat nat; is_aligned word tcbBlockSizeBits; nat \<le> 5; tcbBlockSizeBits < word_bits; tcb_at' word s; zombie_type = ZombieTCB\<rbrakk> \<Longrightarrow> x * 2 ^ cteSizeBits < 2 ^ tcbBlockSizeBits
 2. \<And>word zombie_type nat x x2. \<lbrakk>c = capability.Zombie word zombie_type nat; x < word_of_nat nat; is_aligned word (zBits zombie_type); nat \<le> zombieCTEs zombie_type; zBits zombie_type < word_bits; case zombie_type of ZombieTCB \<Rightarrow> tcb_at' word s | ZombieCNode n \<Rightarrow> n \<noteq> 0 \<and> (\<forall>addr. real_cte_at' (word + 2 ^ cteSizeBits * (addr && mask n)) s); zombie_type = ZombieCNode x2\<rbrakk> \<Longrightarrow> x * 2 ^ cteSizeBits < 2 ^ zBits zombie_type proof (prove)
goal (3 subgoals):
 1. \<And>word zombie_type nat x. \<lbrakk>c = capability.Zombie word ZombieTCB nat; x < word_of_nat nat; is_aligned word tcbBlockSizeBits; nat \<le> 5; tcbBlockSizeBits < word_bits; tcb_at' word s; zombie_type = ZombieTCB\<rbrakk> \<Longrightarrow> x < 2 ^ tcbBlockSizeBits div 2 ^ cteSizeBits
 2. \<And>word zombie_type nat x. \<lbrakk>c = capability.Zombie word ZombieTCB nat; x < word_of_nat nat; is_aligned word tcbBlockSizeBits; nat \<le> 5; tcbBlockSizeBits < word_bits; tcb_at' word s; zombie_type = ZombieTCB\<rbrakk> \<Longrightarrow> 0 < 2 ^ cteSizeBits
 3. \<And>word zombie_type nat x x2. \<lbrakk>c = capability.Zombie word zombie_type nat; x < word_of_nat nat; is_aligned word (zBits zombie_type); nat \<le> zombieCTEs zombie_type; zBits zombie_type < word_bits; case zombie_type of ZombieTCB \<Rightarrow> tcb_at' word s | ZombieCNode n \<Rightarrow> n \<noteq> 0 \<and> (\<forall>addr. real_cte_at' (word + 2 ^ cteSizeBits * (addr && mask n)) s); zombie_type = ZombieCNode x2\<rbrakk> \<Longrightarrow> x * 2 ^ cteSizeBits < 2 ^ zBits zombie_type proof (prove)
goal (3 subgoals):
 1. \<And>word zombie_type nat x. \<lbrakk>c = capability.Zombie word ZombieTCB nat; x < word_of_nat nat; is_aligned word 9; nat \<le> 5; 9 < word_bits; tcb_at' word s; zombie_type = ZombieTCB\<rbrakk> \<Longrightarrow> x < 0x20
 2. \<And>word zombie_type nat x. \<lbrakk>c = capability.Zombie word ZombieTCB nat; x < word_of_nat nat; is_aligned word tcbBlockSizeBits; nat \<le> 5; tcbBlockSizeBits < word_bits; tcb_at' word s; zombie_type = ZombieTCB\<rbrakk> \<Longrightarrow> 0 < 2 ^ cteSizeBits
 3. \<And>word zombie_type nat x x2. \<lbrakk>c = capability.Zombie word zombie_type nat; x < word_of_nat nat; is_aligned word (zBits zombie_type); nat \<le> zombieCTEs zombie_type; zBits zombie_type < word_bits; case zombie_type of ZombieTCB \<Rightarrow> tcb_at' word s | ZombieCNode n \<Rightarrow> n \<noteq> 0 \<and> (\<forall>addr. real_cte_at' (word + 2 ^ cteSizeBits * (addr && mask n)) s); zombie_type = ZombieCNode x2\<rbrakk> \<Longrightarrow> x * 2 ^ cteSizeBits < 2 ^ zBits zombie_type proof (prove)
goal (3 subgoals):
 1. \<And>word zombie_type nat x. \<lbrakk>c = capability.Zombie word ZombieTCB nat; is_aligned word 9; nat \<le> 5; 9 < word_bits; tcb_at' word s; zombie_type = ZombieTCB\<rbrakk> \<Longrightarrow> word_of_nat nat \<le> 0x20
 2. \<And>word zombie_type nat x. \<lbrakk>c = capability.Zombie word ZombieTCB nat; x < word_of_nat nat; is_aligned word tcbBlockSizeBits; nat \<le> 5; tcbBlockSizeBits < word_bits; tcb_at' word s; zombie_type = ZombieTCB\<rbrakk> \<Longrightarrow> 0 < 2 ^ cteSizeBits
 3. \<And>word zombie_type nat x x2. \<lbrakk>c = capability.Zombie word zombie_type nat; x < word_of_nat nat; is_aligned word (zBits zombie_type); nat \<le> zombieCTEs zombie_type; zBits zombie_type < word_bits; case zombie_type of ZombieTCB \<Rightarrow> tcb_at' word s | ZombieCNode n \<Rightarrow> n \<noteq> 0 \<and> (\<forall>addr. real_cte_at' (word + 2 ^ cteSizeBits * (addr && mask n)) s); zombie_type = ZombieCNode x2\<rbrakk> \<Longrightarrow> x * 2 ^ cteSizeBits < 2 ^ zBits zombie_type proof (prove)
goal (3 subgoals):
 1. \<And>word zombie_type nat. \<lbrakk>c = capability.Zombie word ZombieTCB nat; is_aligned word 9; nat \<le> 5; 9 < word_bits; tcb_at' word s; zombie_type = ZombieTCB\<rbrakk> \<Longrightarrow> unat (word_of_nat nat) \<le> 32
 2. \<And>word zombie_type nat x. \<lbrakk>c = capability.Zombie word ZombieTCB nat; x < word_of_nat nat; is_aligned word tcbBlockSizeBits; nat \<le> 5; tcbBlockSizeBits < word_bits; tcb_at' word s; zombie_type = ZombieTCB\<rbrakk> \<Longrightarrow> 0 < 2 ^ cteSizeBits
 3. \<And>word zombie_type nat x x2. \<lbrakk>c = capability.Zombie word zombie_type nat; x < word_of_nat nat; is_aligned word (zBits zombie_type); nat \<le> zombieCTEs zombie_type; zBits zombie_type < word_bits; case zombie_type of ZombieTCB \<Rightarrow> tcb_at' word s | ZombieCNode n \<Rightarrow> n \<noteq> 0 \<and> (\<forall>addr. real_cte_at' (word + 2 ^ cteSizeBits * (addr && mask n)) s); zombie_type = ZombieCNode x2\<rbrakk> \<Longrightarrow> x * 2 ^ cteSizeBits < 2 ^ zBits zombie_type proof (prove)
goal (4 subgoals):
 1. \<And>word zombie_type nat. \<lbrakk>c = capability.Zombie word ZombieTCB nat; is_aligned word 9; nat \<le> 5; 9 < word_bits; tcb_at' word s; zombie_type = ZombieTCB\<rbrakk> \<Longrightarrow> nat \<le> unat 5
 2. \<And>word zombie_type nat. \<lbrakk>c = capability.Zombie word ZombieTCB nat; is_aligned word 9; nat \<le> 5; 9 < word_bits; tcb_at' word s; zombie_type = ZombieTCB\<rbrakk> \<Longrightarrow> nat \<le> 32
 3. \<And>word zombie_type nat x. \<lbrakk>c = capability.Zombie word ZombieTCB nat; x < word_of_nat nat; is_aligned word tcbBlockSizeBits; nat \<le> 5; tcbBlockSizeBits < word_bits; tcb_at' word s; zombie_type = ZombieTCB\<rbrakk> \<Longrightarrow> 0 < 2 ^ cteSizeBits
 4. \<And>word zombie_type nat x x2. \<lbrakk>c = capability.Zombie word zombie_type nat; x < word_of_nat nat; is_aligned word (zBits zombie_type); nat \<le> zombieCTEs zombie_type; zBits zombie_type < word_bits; case zombie_type of ZombieTCB \<Rightarrow> tcb_at' word s | ZombieCNode n \<Rightarrow> n \<noteq> 0 \<and> (\<forall>addr. real_cte_at' (word + 2 ^ cteSizeBits * (addr && mask n)) s); zombie_type = ZombieCNode x2\<rbrakk> \<Longrightarrow> x * 2 ^ cteSizeBits < 2 ^ zBits zombie_type proof (prove)
goal (3 subgoals):
 1. \<And>word zombie_type nat. \<lbrakk>c = capability.Zombie word ZombieTCB nat; is_aligned word 9; nat \<le> 5; 9 < word_bits; tcb_at' word s; zombie_type = ZombieTCB\<rbrakk> \<Longrightarrow> nat \<le> 32
 2. \<And>word zombie_type nat x. \<lbrakk>c = capability.Zombie word ZombieTCB nat; x < word_of_nat nat; is_aligned word tcbBlockSizeBits; nat \<le> 5; tcbBlockSizeBits < word_bits; tcb_at' word s; zombie_type = ZombieTCB\<rbrakk> \<Longrightarrow> 0 < 2 ^ cteSizeBits
 3. \<And>word zombie_type nat x x2. \<lbrakk>c = capability.Zombie word zombie_type nat; x < word_of_nat nat; is_aligned word (zBits zombie_type); nat \<le> zombieCTEs zombie_type; zBits zombie_type < word_bits; case zombie_type of ZombieTCB \<Rightarrow> tcb_at' word s | ZombieCNode n \<Rightarrow> n \<noteq> 0 \<and> (\<forall>addr. real_cte_at' (word + 2 ^ cteSizeBits * (addr && mask n)) s); zombie_type = ZombieCNode x2\<rbrakk> \<Longrightarrow> x * 2 ^ cteSizeBits < 2 ^ zBits zombie_type proof (prove)
goal (2 subgoals):
 1. \<And>word zombie_type nat x. \<lbrakk>c = capability.Zombie word ZombieTCB nat; x < word_of_nat nat; is_aligned word tcbBlockSizeBits; nat \<le> 5; tcbBlockSizeBits < word_bits; tcb_at' word s; zombie_type = ZombieTCB\<rbrakk> \<Longrightarrow> 0 < 2 ^ cteSizeBits
 2. \<And>word zombie_type nat x x2. \<lbrakk>c = capability.Zombie word zombie_type nat; x < word_of_nat nat; is_aligned word (zBits zombie_type); nat \<le> zombieCTEs zombie_type; zBits zombie_type < word_bits; case zombie_type of ZombieTCB \<Rightarrow> tcb_at' word s | ZombieCNode n \<Rightarrow> n \<noteq> 0 \<and> (\<forall>addr. real_cte_at' (word + 2 ^ cteSizeBits * (addr && mask n)) s); zombie_type = ZombieCNode x2\<rbrakk> \<Longrightarrow> x * 2 ^ cteSizeBits < 2 ^ zBits zombie_type proof (prove)
goal (1 subgoal):
 1. \<And>word zombie_type nat x x2. \<lbrakk>c = capability.Zombie word zombie_type nat; x < word_of_nat nat; is_aligned word (zBits zombie_type); nat \<le> zombieCTEs zombie_type; zBits zombie_type < word_bits; case zombie_type of ZombieTCB \<Rightarrow> tcb_at' word s | ZombieCNode n \<Rightarrow> n \<noteq> 0 \<and> (\<forall>addr. real_cte_at' (word + 2 ^ cteSizeBits * (addr && mask n)) s); zombie_type = ZombieCNode x2\<rbrakk> \<Longrightarrow> x * 2 ^ cteSizeBits < 2 ^ zBits zombie_type proof (prove)
goal (1 subgoal):
 1. \<And>word zombie_type nat x x2. \<lbrakk>c = capability.Zombie word (ZombieCNode x2) nat; x < word_of_nat nat; is_aligned word (4 + x2); nat \<le> 2 ^ x2; 4 + x2 < word_bits; 0 < x2 \<and> (\<forall>addr. real_cte_at' (word + (addr && mask x2) * 0x10) s); zombie_type = ZombieCNode x2\<rbrakk> \<Longrightarrow> x * 0x10 < 2 ^ x2 * 0x10 proof (prove)
goal (3 subgoals):
 1. \<And>word zombie_type nat x x2. \<lbrakk>c = capability.Zombie word (ZombieCNode x2) nat; x < word_of_nat nat; is_aligned word (4 + x2); nat \<le> 2 ^ x2; 4 + x2 < word_bits; 0 < x2 \<and> (\<forall>addr. real_cte_at' (word + (addr && mask x2) * 0x10) s); zombie_type = ZombieCNode x2\<rbrakk> \<Longrightarrow> x < 2 ^ x2
 2. \<And>word zombie_type nat x x2. \<lbrakk>c = capability.Zombie word (ZombieCNode x2) nat; x < word_of_nat nat; is_aligned word (4 + x2); nat \<le> 2 ^ x2; 4 + x2 < word_bits; 0 < x2 \<and> (\<forall>addr. real_cte_at' (word + (addr && mask x2) * 0x10) s); zombie_type = ZombieCNode x2\<rbrakk> \<Longrightarrow> 0 < 0x10
 3. \<And>word zombie_type nat x x2. \<lbrakk>c = capability.Zombie word (ZombieCNode x2) nat; x < word_of_nat nat; is_aligned word (4 + x2); nat \<le> 2 ^ x2; 4 + x2 < word_bits; 0 < x2 \<and> (\<forall>addr. real_cte_at' (word + (addr && mask x2) * 0x10) s); zombie_type = ZombieCNode x2\<rbrakk> \<Longrightarrow> unat (2 ^ x2) * unat 0x10 < 2 ^ LENGTH(32) proof (prove)
goal (3 subgoals):
 1. \<And>word zombie_type nat x x2. \<lbrakk>c = capability.Zombie word (ZombieCNode x2) nat; is_aligned word (4 + x2); nat \<le> 2 ^ x2; 4 + x2 < word_bits; 0 < x2 \<and> (\<forall>addr. real_cte_at' (word + (addr && mask x2) * 0x10) s); zombie_type = ZombieCNode x2\<rbrakk> \<Longrightarrow> word_of_nat nat \<le> 2 ^ x2
 2. \<And>word zombie_type nat x x2. \<lbrakk>c = capability.Zombie word (ZombieCNode x2) nat; x < word_of_nat nat; is_aligned word (4 + x2); nat \<le> 2 ^ x2; 4 + x2 < word_bits; 0 < x2 \<and> (\<forall>addr. real_cte_at' (word + (addr && mask x2) * 0x10) s); zombie_type = ZombieCNode x2\<rbrakk> \<Longrightarrow> 0 < 0x10
 3. \<And>word zombie_type nat x x2. \<lbrakk>c = capability.Zombie word (ZombieCNode x2) nat; x < word_of_nat nat; is_aligned word (4 + x2); nat \<le> 2 ^ x2; 4 + x2 < word_bits; 0 < x2 \<and> (\<forall>addr. real_cte_at' (word + (addr && mask x2) * 0x10) s); zombie_type = ZombieCNode x2\<rbrakk> \<Longrightarrow> unat (2 ^ x2) * unat 0x10 < 2 ^ LENGTH(32) proof (prove)
goal (3 subgoals):
 1. \<And>word zombie_type nat x2. \<lbrakk>c = capability.Zombie word (ZombieCNode x2) nat; is_aligned word (4 + x2); nat \<le> 2 ^ x2; 4 + x2 < word_bits; 0 < x2 \<and> (\<forall>addr. real_cte_at' (word + (addr && mask x2) * 0x10) s); zombie_type = ZombieCNode x2\<rbrakk> \<Longrightarrow> unat (word_of_nat nat) \<le> 2 ^ x2
 2. \<And>word zombie_type nat x x2. \<lbrakk>c = capability.Zombie word (ZombieCNode x2) nat; x < word_of_nat nat; is_aligned word (4 + x2); nat \<le> 2 ^ x2; 4 + x2 < word_bits; 0 < x2 \<and> (\<forall>addr. real_cte_at' (word + (addr && mask x2) * 0x10) s); zombie_type = ZombieCNode x2\<rbrakk> \<Longrightarrow> 0 < 0x10
 3. \<And>word zombie_type nat x x2. \<lbrakk>c = capability.Zombie word (ZombieCNode x2) nat; x < word_of_nat nat; is_aligned word (4 + x2); nat \<le> 2 ^ x2; 4 + x2 < word_bits; 0 < x2 \<and> (\<forall>addr. real_cte_at' (word + (addr && mask x2) * 0x10) s); zombie_type = ZombieCNode x2\<rbrakk> \<Longrightarrow> unat (2 ^ x2) * unat 0x10 < 2 ^ LENGTH(32) proof (prove)
goal (4 subgoals):
 1. \<And>word zombie_type nat x2. \<lbrakk>c = capability.Zombie word (ZombieCNode x2) nat; is_aligned word (4 + x2); nat \<le> 2 ^ x2; 4 + x2 < word_bits; 0 < x2 \<and> (\<forall>addr. real_cte_at' (word + (addr && mask x2) * 0x10) s); zombie_type = ZombieCNode x2\<rbrakk> \<Longrightarrow> nat \<le> unat (?z105 word zombie_type nat x2)
 2. \<And>word zombie_type nat x2. \<lbrakk>c = capability.Zombie word (ZombieCNode x2) nat; is_aligned word (4 + x2); nat \<le> 2 ^ x2; 4 + x2 < word_bits; 0 < x2 \<and> (\<forall>addr. real_cte_at' (word + (addr && mask x2) * 0x10) s); zombie_type = ZombieCNode x2\<rbrakk> \<Longrightarrow> nat \<le> 2 ^ x2
 3. \<And>word zombie_type nat x x2. \<lbrakk>c = capability.Zombie word (ZombieCNode x2) nat; x < word_of_nat nat; is_aligned word (4 + x2); nat \<le> 2 ^ x2; 4 + x2 < word_bits; 0 < x2 \<and> (\<forall>addr. real_cte_at' (word + (addr && mask x2) * 0x10) s); zombie_type = ZombieCNode x2\<rbrakk> \<Longrightarrow> 0 < 0x10
 4. \<And>word zombie_type nat x x2. \<lbrakk>c = capability.Zombie word (ZombieCNode x2) nat; x < word_of_nat nat; is_aligned word (4 + x2); nat \<le> 2 ^ x2; 4 + x2 < word_bits; 0 < x2 \<and> (\<forall>addr. real_cte_at' (word + (addr && mask x2) * 0x10) s); zombie_type = ZombieCNode x2\<rbrakk> \<Longrightarrow> unat (2 ^ x2) * unat 0x10 < 2 ^ LENGTH(32) proof (prove)
goal (5 subgoals):
 1. \<And>word zombie_type nat x2. \<lbrakk>c = capability.Zombie word (ZombieCNode x2) nat; is_aligned word (4 + x2); nat \<le> 2 ^ x2; 4 + x2 < word_bits; 0 < x2 \<and> (\<forall>addr. real_cte_at' (word + (addr && mask x2) * 0x10) s); zombie_type = ZombieCNode x2\<rbrakk> \<Longrightarrow> ?n108 word zombie_type nat x2 (?word108 word zombie_type nat x2) (?zombie_type108 word zombie_type nat x2) nat (?x2.108 word zombie_type nat x2) < LENGTH(32)
 2. \<And>word zombie_type nat x2. \<lbrakk>c = capability.Zombie word (ZombieCNode x2) nat; is_aligned word (4 + x2); nat \<le> 2 ^ x2; 4 + x2 < word_bits; 0 < x2 \<and> (\<forall>addr. real_cte_at' (word + (addr && mask x2) * 0x10) s); zombie_type = ZombieCNode x2\<rbrakk> \<Longrightarrow> nat \<le> 2 ^ ?n108 word zombie_type nat x2 (?word108 word zombie_type nat x2) (?zombie_type108 word zombie_type nat x2) nat (?x2.108 word zombie_type nat x2)
 3. \<And>word zombie_type nat x2. \<lbrakk>c = capability.Zombie word (ZombieCNode x2) nat; is_aligned word (4 + x2); nat \<le> 2 ^ x2; 4 + x2 < word_bits; 0 < x2 \<and> (\<forall>addr. real_cte_at' (word + (addr && mask x2) * 0x10) s); zombie_type = ZombieCNode x2\<rbrakk> \<Longrightarrow> nat \<le> 2 ^ x2
 4. \<And>word zombie_type nat x x2. \<lbrakk>c = capability.Zombie word (ZombieCNode x2) nat; x < word_of_nat nat; is_aligned word (4 + x2); nat \<le> 2 ^ x2; 4 + x2 < word_bits; 0 < x2 \<and> (\<forall>addr. real_cte_at' (word + (addr && mask x2) * 0x10) s); zombie_type = ZombieCNode x2\<rbrakk> \<Longrightarrow> 0 < 0x10
 5. \<And>word zombie_type nat x x2. \<lbrakk>c = capability.Zombie word (ZombieCNode x2) nat; x < word_of_nat nat; is_aligned word (4 + x2); nat \<le> 2 ^ x2; 4 + x2 < word_bits; 0 < x2 \<and> (\<forall>addr. real_cte_at' (word + (addr && mask x2) * 0x10) s); zombie_type = ZombieCNode x2\<rbrakk> \<Longrightarrow> unat (2 ^ x2) * unat 0x10 < 2 ^ LENGTH(32) proof (prove)
goal (5 subgoals):
 1. \<And>word zombie_type nat x2. \<lbrakk>c = capability.Zombie word (ZombieCNode x2) nat; is_aligned word (4 + x2); nat \<le> 2 ^ x2; 4 + x2 < word_bits; 0 < x2 \<and> (\<forall>addr. real_cte_at' (word + (addr && mask x2) * 0x10) s); zombie_type = ZombieCNode x2\<rbrakk> \<Longrightarrow> nat \<le> 2 ^ ?n108 word zombie_type nat x2 (?word108 word zombie_type nat x2) (?zombie_type108 word zombie_type nat x2) nat (?x2.108 word zombie_type nat x2)
 2. \<And>word zombie_type nat x2. \<lbrakk>c = capability.Zombie word (ZombieCNode x2) nat; is_aligned word (4 + x2); nat \<le> 2 ^ x2; 4 + x2 < word_bits; 0 < x2 \<and> (\<forall>addr. real_cte_at' (word + (addr && mask x2) * 0x10) s); zombie_type = ZombieCNode x2\<rbrakk> \<Longrightarrow> ?n108 word zombie_type nat x2 (?word108 word zombie_type nat x2) (?zombie_type108 word zombie_type nat x2) nat (?x2.108 word zombie_type nat x2) < LENGTH(32)
 3. \<And>word zombie_type nat x2. \<lbrakk>c = capability.Zombie word (ZombieCNode x2) nat; is_aligned word (4 + x2); nat \<le> 2 ^ x2; 4 + x2 < word_bits; 0 < x2 \<and> (\<forall>addr. real_cte_at' (word + (addr && mask x2) * 0x10) s); zombie_type = ZombieCNode x2\<rbrakk> \<Longrightarrow> nat \<le> 2 ^ x2
 4. \<And>word zombie_type nat x x2. \<lbrakk>c = capability.Zombie word (ZombieCNode x2) nat; x < word_of_nat nat; is_aligned word (4 + x2); nat \<le> 2 ^ x2; 4 + x2 < word_bits; 0 < x2 \<and> (\<forall>addr. real_cte_at' (word + (addr && mask x2) * 0x10) s); zombie_type = ZombieCNode x2\<rbrakk> \<Longrightarrow> 0 < 0x10
 5. \<And>word zombie_type nat x x2. \<lbrakk>c = capability.Zombie word (ZombieCNode x2) nat; x < word_of_nat nat; is_aligned word (4 + x2); nat \<le> 2 ^ x2; 4 + x2 < word_bits; 0 < x2 \<and> (\<forall>addr. real_cte_at' (word + (addr && mask x2) * 0x10) s); zombie_type = ZombieCNode x2\<rbrakk> \<Longrightarrow> unat (2 ^ x2) * unat 0x10 < 2 ^ LENGTH(32) proof (prove)
goal (4 subgoals):
 1. \<And>word zombie_type nat x2. \<lbrakk>c = capability.Zombie word (ZombieCNode x2) nat; is_aligned word (4 + x2); nat \<le> 2 ^ x2; 4 + x2 < word_bits; 0 < x2 \<and> (\<forall>addr. real_cte_at' (word + (addr && mask x2) * 0x10) s); zombie_type = ZombieCNode x2\<rbrakk> \<Longrightarrow> x2 < LENGTH(32)
 2. \<And>word zombie_type nat x2. \<lbrakk>c = capability.Zombie word (ZombieCNode x2) nat; is_aligned word (4 + x2); nat \<le> 2 ^ x2; 4 + x2 < word_bits; 0 < x2 \<and> (\<forall>addr. real_cte_at' (word + (addr && mask x2) * 0x10) s); zombie_type = ZombieCNode x2\<rbrakk> \<Longrightarrow> nat \<le> 2 ^ x2
 3. \<And>word zombie_type nat x x2. \<lbrakk>c = capability.Zombie word (ZombieCNode x2) nat; x < word_of_nat nat; is_aligned word (4 + x2); nat \<le> 2 ^ x2; 4 + x2 < word_bits; 0 < x2 \<and> (\<forall>addr. real_cte_at' (word + (addr && mask x2) * 0x10) s); zombie_type = ZombieCNode x2\<rbrakk> \<Longrightarrow> 0 < 0x10
 4. \<And>word zombie_type nat x x2. \<lbrakk>c = capability.Zombie word (ZombieCNode x2) nat; x < word_of_nat nat; is_aligned word (4 + x2); nat \<le> 2 ^ x2; 4 + x2 < word_bits; 0 < x2 \<and> (\<forall>addr. real_cte_at' (word + (addr && mask x2) * 0x10) s); zombie_type = ZombieCNode x2\<rbrakk> \<Longrightarrow> unat (2 ^ x2) * unat 0x10 < 2 ^ LENGTH(32) proof (prove)
goal (3 subgoals):
 1. \<And>word zombie_type nat x2. \<lbrakk>c = capability.Zombie word (ZombieCNode x2) nat; is_aligned word (4 + x2); nat \<le> 2 ^ x2; 4 + x2 < word_bits; 0 < x2 \<and> (\<forall>addr. real_cte_at' (word + (addr && mask x2) * 0x10) s); zombie_type = ZombieCNode x2\<rbrakk> \<Longrightarrow> nat \<le> 2 ^ x2
 2. \<And>word zombie_type nat x x2. \<lbrakk>c = capability.Zombie word (ZombieCNode x2) nat; x < word_of_nat nat; is_aligned word (4 + x2); nat \<le> 2 ^ x2; 4 + x2 < word_bits; 0 < x2 \<and> (\<forall>addr. real_cte_at' (word + (addr && mask x2) * 0x10) s); zombie_type = ZombieCNode x2\<rbrakk> \<Longrightarrow> 0 < 0x10
 3. \<And>word zombie_type nat x x2. \<lbrakk>c = capability.Zombie word (ZombieCNode x2) nat; x < word_of_nat nat; is_aligned word (4 + x2); nat \<le> 2 ^ x2; 4 + x2 < word_bits; 0 < x2 \<and> (\<forall>addr. real_cte_at' (word + (addr && mask x2) * 0x10) s); zombie_type = ZombieCNode x2\<rbrakk> \<Longrightarrow> unat (2 ^ x2) * unat 0x10 < 2 ^ LENGTH(32) proof (prove)
goal (2 subgoals):
 1. \<And>word zombie_type nat x x2. \<lbrakk>c = capability.Zombie word (ZombieCNode x2) nat; x < word_of_nat nat; is_aligned word (4 + x2); nat \<le> 2 ^ x2; 4 + x2 < word_bits; 0 < x2 \<and> (\<forall>addr. real_cte_at' (word + (addr && mask x2) * 0x10) s); zombie_type = ZombieCNode x2\<rbrakk> \<Longrightarrow> 0 < 0x10
 2. \<And>word zombie_type nat x x2. \<lbrakk>c = capability.Zombie word (ZombieCNode x2) nat; x < word_of_nat nat; is_aligned word (4 + x2); nat \<le> 2 ^ x2; 4 + x2 < word_bits; 0 < x2 \<and> (\<forall>addr. real_cte_at' (word + (addr && mask x2) * 0x10) s); zombie_type = ZombieCNode x2\<rbrakk> \<Longrightarrow> unat (2 ^ x2) * unat 0x10 < 2 ^ LENGTH(32) proof (prove)
goal (1 subgoal):
 1. \<And>word zombie_type nat x x2. \<lbrakk>c = capability.Zombie word (ZombieCNode x2) nat; x < word_of_nat nat; is_aligned word (4 + x2); nat \<le> 2 ^ x2; 4 + x2 < word_bits; 0 < x2 \<and> (\<forall>addr. real_cte_at' (word + (addr && mask x2) * 0x10) s); zombie_type = ZombieCNode x2\<rbrakk> \<Longrightarrow> unat (2 ^ x2) * unat 0x10 < 2 ^ LENGTH(32) proof (prove)
goal (2 subgoals):
 1. \<And>word zombie_type nat x x2. \<lbrakk>c = capability.Zombie word (ZombieCNode x2) nat; x < word_of_nat nat; is_aligned word (4 + x2); nat \<le> 2 ^ x2; 4 + x2 < word_bits; 0 < x2 \<and> (\<forall>addr. real_cte_at' (word + (addr && mask x2) * 0x10) s); zombie_type = ZombieCNode x2\<rbrakk> \<Longrightarrow> 1 < 2
 2. \<And>word zombie_type nat x x2. \<lbrakk>c = capability.Zombie word (ZombieCNode x2) nat; x < word_of_nat nat; is_aligned word (4 + x2); nat \<le> 2 ^ x2; 4 + x2 < word_bits; 0 < x2 \<and> (\<forall>addr. real_cte_at' (word + (addr && mask x2) * 0x10) s); zombie_type = ZombieCNode x2; 2 ^ (4 + x2) < 2 ^ word_bits\<rbrakk> \<Longrightarrow> unat (2 ^ x2) * unat 0x10 < 2 ^ LENGTH(32) proof (prove)
goal (1 subgoal):
 1. \<And>word zombie_type nat x x2. \<lbrakk>c = capability.Zombie word (ZombieCNode x2) nat; x < word_of_nat nat; is_aligned word (4 + x2); nat \<le> 2 ^ x2; 4 + x2 < word_bits; 0 < x2 \<and> (\<forall>addr. real_cte_at' (word + (addr && mask x2) * 0x10) s); zombie_type = ZombieCNode x2; 2 ^ (4 + x2) < 2 ^ word_bits\<rbrakk> \<Longrightarrow> unat (2 ^ x2) * unat 0x10 < 2 ^ LENGTH(32) proof (prove)
goal (1 subgoal):
 1. \<And>word zombie_type nat x x2. \<lbrakk>c = capability.Zombie word (ZombieCNode x2) nat; x < word_of_nat nat; is_aligned word (4 + x2); nat \<le> 2 ^ x2; 4 + x2 < word_bits; 0 < x2 \<and> (\<forall>addr. real_cte_at' (word + (addr && mask x2) * 0x10) s); zombie_type = ZombieCNode x2; 2 ^ 4 * 2 ^ x2 < 2 ^ word_bits\<rbrakk> \<Longrightarrow> unat (2 ^ x2) * unat 0x10 < 2 ^ LENGTH(32) proof (prove)
goal:
No subgoals!