theory Untyped_AI

lemma untyped_ranges_aligned_disjoing_or_subset:
  "\<lbrakk>cap_aligned c1;cap_aligned c2\<rbrakk> \<Longrightarrow>
    untyped_range c1 \<subseteq> untyped_range c2
    \<or> untyped_range c2 \<subseteq> untyped_range c1
    \<or> untyped_range c1 \<inter> untyped_range c2 = {}" apply (simp add: cap_aligned_def) apply (elim conjE) apply (drule(1) aligned_ranges_subset_or_disjoint) apply (case_tac c1) apply simp_all apply (case_tac c2) apply simp_all done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>cap_aligned c1; cap_aligned c2\<rbrakk> \<Longrightarrow> untyped_range c1 \<subseteq> untyped_range c2 \<or> untyped_range c2 \<subseteq> untyped_range c1 \<or> untyped_range c1 \<inter> untyped_range c2 = {} proof (prove)
goal (1 subgoal):
 1. \<lbrakk>is_aligned (obj_ref_of c1) (cap_bits c1) \<and> cap_bits c1 < word_bits; is_aligned (obj_ref_of c2) (cap_bits c2) \<and> cap_bits c2 < word_bits\<rbrakk> \<Longrightarrow> untyped_range c1 \<subseteq> untyped_range c2 \<or> untyped_range c2 \<subseteq> untyped_range c1 \<or> untyped_range c1 \<inter> untyped_range c2 = {} proof (prove)
goal (1 subgoal):
 1. \<lbrakk>is_aligned (obj_ref_of c1) (cap_bits c1); cap_bits c1 < word_bits; is_aligned (obj_ref_of c2) (cap_bits c2); cap_bits c2 < word_bits\<rbrakk> \<Longrightarrow> untyped_range c1 \<subseteq> untyped_range c2 \<or> untyped_range c2 \<subseteq> untyped_range c1 \<or> untyped_range c1 \<inter> untyped_range c2 = {} proof (prove)
goal (1 subgoal):
 1. \<lbrakk>cap_bits c1 < word_bits; is_aligned (obj_ref_of c2) (cap_bits c2); cap_bits c2 < word_bits; {obj_ref_of c1..obj_ref_of c1 + 2 ^ cap_bits c1 - 1} \<inter> {obj_ref_of c2..obj_ref_of c2 + 2 ^ cap_bits c2 - 1} = {} \<or> {obj_ref_of c1..obj_ref_of c1 + 2 ^ cap_bits c1 - 1} \<subseteq> {obj_ref_of c2..obj_ref_of c2 + 2 ^ cap_bits c2 - 1} \<or> {obj_ref_of c2..obj_ref_of c2 + 2 ^ cap_bits c2 - 1} \<subseteq> {obj_ref_of c1..obj_ref_of c1 + 2 ^ cap_bits c1 - 1}\<rbrakk> \<Longrightarrow> untyped_range c1 \<subseteq> untyped_range c2 \<or> untyped_range c2 \<subseteq> untyped_range c1 \<or> untyped_range c1 \<inter> untyped_range c2 = {} proof (prove)
goal (12 subgoals):
 1. \<lbrakk>cap_bits c1 < word_bits; is_aligned (obj_ref_of c2) (cap_bits c2); cap_bits c2 < word_bits; {obj_ref_of c1..obj_ref_of c1 + 2 ^ cap_bits c1 - 1} \<inter> {obj_ref_of c2..obj_ref_of c2 + 2 ^ cap_bits c2 - 1} = {} \<or> {obj_ref_of c1..obj_ref_of c1 + 2 ^ cap_bits c1 - 1} \<subseteq> {obj_ref_of c2..obj_ref_of c2 + 2 ^ cap_bits c2 - 1} \<or> {obj_ref_of c2..obj_ref_of c2 + 2 ^ cap_bits c2 - 1} \<subseteq> {obj_ref_of c1..obj_ref_of c1 + 2 ^ cap_bits c1 - 1}; c1 = NullCap\<rbrakk> \<Longrightarrow> untyped_range c1 \<subseteq> untyped_range c2 \<or> untyped_range c2 \<subseteq> untyped_range c1 \<or> untyped_range c1 \<inter> untyped_range c2 = {}
 2. \<And>x21 x22 x23 x24. \<lbrakk>cap_bits c1 < word_bits; is_aligned (obj_ref_of c2) (cap_bits c2); cap_bits c2 < word_bits; {obj_ref_of c1..obj_ref_of c1 + 2 ^ cap_bits c1 - 1} \<inter> {obj_ref_of c2..obj_ref_of c2 + 2 ^ cap_bits c2 - 1} = {} \<or> {obj_ref_of c1..obj_ref_of c1 + 2 ^ cap_bits c1 - 1} \<subseteq> {obj_ref_of c2..obj_ref_of c2 + 2 ^ cap_bits c2 - 1} \<or> {obj_ref_of c2..obj_ref_of c2 + 2 ^ cap_bits c2 - 1} \<subseteq> {obj_ref_of c1..obj_ref_of c1 + 2 ^ cap_bits c1 - 1}; c1 = UntypedCap x21 x22 x23 x24\<rbrakk> \<Longrightarrow> untyped_range c1 \<subseteq> untyped_range c2 \<or> untyped_range c2 \<subseteq> untyped_range c1 \<or> untyped_range c1 \<inter> untyped_range c2 = {}
 3. \<And>x31 x32 x33. \<lbrakk>cap_bits c1 < word_bits; is_aligned (obj_ref_of c2) (cap_bits c2); cap_bits c2 < word_bits; {obj_ref_of c1..obj_ref_of c1 + 2 ^ cap_bits c1 - 1} \<inter> {obj_ref_of c2..obj_ref_of c2 + 2 ^ cap_bits c2 - 1} = {} \<or> {obj_ref_of c1..obj_ref_of c1 + 2 ^ cap_bits c1 - 1} \<subseteq> {obj_ref_of c2..obj_ref_of c2 + 2 ^ cap_bits c2 - 1} \<or> {obj_ref_of c2..obj_ref_of c2 + 2 ^ cap_bits c2 - 1} \<subseteq> {obj_ref_of c1..obj_ref_of c1 + 2 ^ cap_bits c1 - 1}; c1 = EndpointCap x31 x32 x33\<rbrakk> \<Longrightarrow> untyped_range c1 \<subseteq> untyped_range c2 \<or> untyped_range c2 \<subseteq> untyped_range c1 \<or> untyped_range c1 \<inter> untyped_range c2 = {}
 4. \<And>x41 x42 x43. \<lbrakk>cap_bits c1 < word_bits; is_aligned (obj_ref_of c2) (cap_bits c2); cap_bits c2 < word_bits; {obj_ref_of c1..obj_ref_of c1 + 2 ^ cap_bits c1 - 1} \<inter> {obj_ref_of c2..obj_ref_of c2 + 2 ^ cap_bits c2 - 1} = {} \<or> {obj_ref_of c1..obj_ref_of c1 + 2 ^ cap_bits c1 - 1} \<subseteq> {obj_ref_of c2..obj_ref_of c2 + 2 ^ cap_bits c2 - 1} \<or> {obj_ref_of c2..obj_ref_of c2 + 2 ^ cap_bits c2 - 1} \<subseteq> {obj_ref_of c1..obj_ref_of c1 + 2 ^ cap_bits c1 - 1}; c1 = NotificationCap x41 x42 x43\<rbrakk> \<Longrightarrow> untyped_range c1 \<subseteq> untyped_range c2 \<or> untyped_range c2 \<subseteq> untyped_range c1 \<or> untyped_range c1 \<inter> untyped_range c2 = {}
 5. \<And>x51 x52 x53. \<lbrakk>cap_bits c1 < word_bits; is_aligned (obj_ref_of c2) (cap_bits c2); cap_bits c2 < word_bits; {obj_ref_of c1..obj_ref_of c1 + 2 ^ cap_bits c1 - 1} \<inter> {obj_ref_of c2..obj_ref_of c2 + 2 ^ cap_bits c2 - 1} = {} \<or> {obj_ref_of c1..obj_ref_of c1 + 2 ^ cap_bits c1 - 1} \<subseteq> {obj_ref_of c2..obj_ref_of c2 + 2 ^ cap_bits c2 - 1} \<or> {obj_ref_of c2..obj_ref_of c2 + 2 ^ cap_bits c2 - 1} \<subseteq> {obj_ref_of c1..obj_ref_of c1 + 2 ^ cap_bits c1 - 1}; c1 = ReplyCap x51 x52 x53\<rbrakk> \<Longrightarrow> untyped_range c1 \<subseteq> untyped_range c2 \<or> untyped_range c2 \<subseteq> untyped_range c1 \<or> untyped_range c1 \<inter> untyped_range c2 = {}
 6. \<And>x61 x62 x63. \<lbrakk>cap_bits c1 < word_bits; is_aligned (obj_ref_of c2) (cap_bits c2); cap_bits c2 < word_bits; {obj_ref_of c1..obj_ref_of c1 + 2 ^ cap_bits c1 - 1} \<inter> {obj_ref_of c2..obj_ref_of c2 + 2 ^ cap_bits c2 - 1} = {} \<or> {obj_ref_of c1..obj_ref_of c1 + 2 ^ cap_bits c1 - 1} \<subseteq> {obj_ref_of c2..obj_ref_of c2 + 2 ^ cap_bits c2 - 1} \<or> {obj_ref_of c2..obj_ref_of c2 + 2 ^ cap_bits c2 - 1} \<subseteq> {obj_ref_of c1..obj_ref_of c1 + 2 ^ cap_bits c1 - 1}; c1 = CNodeCap x61 x62 x63\<rbrakk> \<Longrightarrow> untyped_range c1 \<subseteq> untyped_range c2 \<or> untyped_range c2 \<subseteq> untyped_range c1 \<or> untyped_range c1 \<inter> untyped_range c2 = {}
 7. \<And>x7. \<lbrakk>cap_bits c1 < word_bits; is_aligned (obj_ref_of c2) (cap_bits c2); cap_bits c2 < word_bits; {obj_ref_of c1..obj_ref_of c1 + 2 ^ cap_bits c1 - 1} \<inter> {obj_ref_of c2..obj_ref_of c2 + 2 ^ cap_bits c2 - 1} = {} \<or> {obj_ref_of c1..obj_ref_of c1 + 2 ^ cap_bits c1 - 1} \<subseteq> {obj_ref_of c2..obj_ref_of c2 + 2 ^ cap_bits c2 - 1} \<or> {obj_ref_of c2..obj_ref_of c2 + 2 ^ cap_bits c2 - 1} \<subseteq> {obj_ref_of c1..obj_ref_of c1 + 2 ^ cap_bits c1 - 1}; c1 = ThreadCap x7\<rbrakk> \<Longrightarrow> untyped_range c1 \<subseteq> untyped_range c2 \<or> untyped_range c2 \<subseteq> untyped_range c1 \<or> untyped_range c1 \<inter> untyped_range c2 = {}
 8. \<lbrakk>cap_bits c1 < word_bits; is_aligned (obj_ref_of c2) (cap_bits c2); cap_bits c2 < word_bits; {obj_ref_of c1..obj_ref_of c1 + 2 ^ cap_bits c1 - 1} \<inter> {obj_ref_of c2..obj_ref_of c2 + 2 ^ cap_bits c2 - 1} = {} \<or> {obj_ref_of c1..obj_ref_of c1 + 2 ^ cap_bits c1 - 1} \<subseteq> {obj_ref_of c2..obj_ref_of c2 + 2 ^ cap_bits c2 - 1} \<or> {obj_ref_of c2..obj_ref_of c2 + 2 ^ cap_bits c2 - 1} \<subseteq> {obj_ref_of c1..obj_ref_of c1 + 2 ^ cap_bits c1 - 1}; c1 = DomainCap\<rbrakk> \<Longrightarrow> untyped_range c1 \<subseteq> untyped_range c2 \<or> untyped_range c2 \<subseteq> untyped_range c1 \<or> untyped_range c1 \<inter> untyped_range c2 = {}
 9. \<lbrakk>cap_bits c1 < word_bits; is_aligned (obj_ref_of c2) (cap_bits c2); cap_bits c2 < word_bits; {obj_ref_of c1..obj_ref_of c1 + 2 ^ cap_bits c1 - 1} \<inter> {obj_ref_of c2..obj_ref_of c2 + 2 ^ cap_bits c2 - 1} = {} \<or> {obj_ref_of c1..obj_ref_of c1 + 2 ^ cap_bits c1 - 1} \<subseteq> {obj_ref_of c2..obj_ref_of c2 + 2 ^ cap_bits c2 - 1} \<or> {obj_ref_of c2..obj_ref_of c2 + 2 ^ cap_bits c2 - 1} \<subseteq> {obj_ref_of c1..obj_ref_of c1 + 2 ^ cap_bits c1 - 1}; c1 = IRQControlCap\<rbrakk> \<Longrightarrow> untyped_range c1 \<subseteq> untyped_range c2 \<or> untyped_range c2 \<subseteq> untyped_range c1 \<or> untyped_range c1 \<inter> untyped_range c2 = {}
 10. \<And>x10. \<lbrakk>cap_bits c1 < word_bits; is_aligned (obj_ref_of c2) (cap_bits c2); cap_bits c2 < word_bits; {obj_ref_of c1..obj_ref_of c1 + 2 ^ cap_bits c1 - 1} \<inter> {obj_ref_of c2..obj_ref_of c2 + 2 ^ cap_bits c2 - 1} = {} \<or> {obj_ref_of c1..obj_ref_of c1 + 2 ^ cap_bits c1 - 1} \<subseteq> {obj_ref_of c2..obj_ref_of c2 + 2 ^ cap_bits c2 - 1} \<or> {obj_ref_of c2..obj_ref_of c2 + 2 ^ cap_bits c2 - 1} \<subseteq> {obj_ref_of c1..obj_ref_of c1 + 2 ^ cap_bits c1 - 1}; c1 = IRQHandlerCap x10\<rbrakk> \<Longrightarrow> untyped_range c1 \<subseteq> untyped_range c2 \<or> untyped_range c2 \<subseteq> untyped_range c1 \<or> untyped_range c1 \<inter> untyped_range c2 = {}
A total of 12 subgoals... proof (prove)
goal (1 subgoal):
 1. \<And>x21 x22 x23 x24. \<lbrakk>x23 < word_bits; is_aligned (obj_ref_of c2) (cap_bits c2); cap_bits c2 < word_bits; obj_ref_of c2 \<le> obj_ref_of c2 + 2 ^ cap_bits c2 - 1 \<longrightarrow> x22 \<le> x22 + 2 ^ x23 - 1 \<longrightarrow> x22 \<le> obj_ref_of c2 + 2 ^ cap_bits c2 - 1 \<longrightarrow> obj_ref_of c2 \<le> x22 + 2 ^ x23 - 1 \<longrightarrow> obj_ref_of c2 \<le> x22 \<and> x22 + 2 ^ x23 - 1 \<le> obj_ref_of c2 + 2 ^ cap_bits c2 - 1 \<or> x22 \<le> obj_ref_of c2 \<and> obj_ref_of c2 + 2 ^ cap_bits c2 - 1 \<le> x22 + 2 ^ x23 - 1; c1 = UntypedCap x21 x22 x23 x24\<rbrakk> \<Longrightarrow> {x22..x22 + 2 ^ x23 - 1} \<subseteq> untyped_range c2 \<or> untyped_range c2 \<subseteq> {x22..x22 + 2 ^ x23 - 1} \<or> {x22..x22 + 2 ^ x23 - 1} \<inter> untyped_range c2 = {} proof (prove)
goal (12 subgoals):
 1. \<And>x21 x22 x23 x24. \<lbrakk>x23 < word_bits; is_aligned (obj_ref_of c2) (cap_bits c2); cap_bits c2 < word_bits; obj_ref_of c2 \<le> obj_ref_of c2 + 2 ^ cap_bits c2 - 1 \<longrightarrow> x22 \<le> x22 + 2 ^ x23 - 1 \<longrightarrow> x22 \<le> obj_ref_of c2 + 2 ^ cap_bits c2 - 1 \<longrightarrow> obj_ref_of c2 \<le> x22 + 2 ^ x23 - 1 \<longrightarrow> obj_ref_of c2 \<le> x22 \<and> x22 + 2 ^ x23 - 1 \<le> obj_ref_of c2 + 2 ^ cap_bits c2 - 1 \<or> x22 \<le> obj_ref_of c2 \<and> obj_ref_of c2 + 2 ^ cap_bits c2 - 1 \<le> x22 + 2 ^ x23 - 1; c1 = UntypedCap x21 x22 x23 x24; c2 = NullCap\<rbrakk> \<Longrightarrow> {x22..x22 + 2 ^ x23 - 1} \<subseteq> untyped_range c2 \<or> untyped_range c2 \<subseteq> {x22..x22 + 2 ^ x23 - 1} \<or> {x22..x22 + 2 ^ x23 - 1} \<inter> untyped_range c2 = {}
 2. \<And>x21 x22 x23 x24 x21a x22a x23a x24a. \<lbrakk>x23 < word_bits; is_aligned (obj_ref_of c2) (cap_bits c2); cap_bits c2 < word_bits; obj_ref_of c2 \<le> obj_ref_of c2 + 2 ^ cap_bits c2 - 1 \<longrightarrow> x22 \<le> x22 + 2 ^ x23 - 1 \<longrightarrow> x22 \<le> obj_ref_of c2 + 2 ^ cap_bits c2 - 1 \<longrightarrow> obj_ref_of c2 \<le> x22 + 2 ^ x23 - 1 \<longrightarrow> obj_ref_of c2 \<le> x22 \<and> x22 + 2 ^ x23 - 1 \<le> obj_ref_of c2 + 2 ^ cap_bits c2 - 1 \<or> x22 \<le> obj_ref_of c2 \<and> obj_ref_of c2 + 2 ^ cap_bits c2 - 1 \<le> x22 + 2 ^ x23 - 1; c1 = UntypedCap x21 x22 x23 x24; c2 = UntypedCap x21a x22a x23a x24a\<rbrakk> \<Longrightarrow> {x22..x22 + 2 ^ x23 - 1} \<subseteq> untyped_range c2 \<or> untyped_range c2 \<subseteq> {x22..x22 + 2 ^ x23 - 1} \<or> {x22..x22 + 2 ^ x23 - 1} \<inter> untyped_range c2 = {}
 3. \<And>x21 x22 x23 x24 x31 x32 x33. \<lbrakk>x23 < word_bits; is_aligned (obj_ref_of c2) (cap_bits c2); cap_bits c2 < word_bits; obj_ref_of c2 \<le> obj_ref_of c2 + 2 ^ cap_bits c2 - 1 \<longrightarrow> x22 \<le> x22 + 2 ^ x23 - 1 \<longrightarrow> x22 \<le> obj_ref_of c2 + 2 ^ cap_bits c2 - 1 \<longrightarrow> obj_ref_of c2 \<le> x22 + 2 ^ x23 - 1 \<longrightarrow> obj_ref_of c2 \<le> x22 \<and> x22 + 2 ^ x23 - 1 \<le> obj_ref_of c2 + 2 ^ cap_bits c2 - 1 \<or> x22 \<le> obj_ref_of c2 \<and> obj_ref_of c2 + 2 ^ cap_bits c2 - 1 \<le> x22 + 2 ^ x23 - 1; c1 = UntypedCap x21 x22 x23 x24; c2 = EndpointCap x31 x32 x33\<rbrakk> \<Longrightarrow> {x22..x22 + 2 ^ x23 - 1} \<subseteq> untyped_range c2 \<or> untyped_range c2 \<subseteq> {x22..x22 + 2 ^ x23 - 1} \<or> {x22..x22 + 2 ^ x23 - 1} \<inter> untyped_range c2 = {}
 4. \<And>x21 x22 x23 x24 x41 x42 x43. \<lbrakk>x23 < word_bits; is_aligned (obj_ref_of c2) (cap_bits c2); cap_bits c2 < word_bits; obj_ref_of c2 \<le> obj_ref_of c2 + 2 ^ cap_bits c2 - 1 \<longrightarrow> x22 \<le> x22 + 2 ^ x23 - 1 \<longrightarrow> x22 \<le> obj_ref_of c2 + 2 ^ cap_bits c2 - 1 \<longrightarrow> obj_ref_of c2 \<le> x22 + 2 ^ x23 - 1 \<longrightarrow> obj_ref_of c2 \<le> x22 \<and> x22 + 2 ^ x23 - 1 \<le> obj_ref_of c2 + 2 ^ cap_bits c2 - 1 \<or> x22 \<le> obj_ref_of c2 \<and> obj_ref_of c2 + 2 ^ cap_bits c2 - 1 \<le> x22 + 2 ^ x23 - 1; c1 = UntypedCap x21 x22 x23 x24; c2 = NotificationCap x41 x42 x43\<rbrakk> \<Longrightarrow> {x22..x22 + 2 ^ x23 - 1} \<subseteq> untyped_range c2 \<or> untyped_range c2 \<subseteq> {x22..x22 + 2 ^ x23 - 1} \<or> {x22..x22 + 2 ^ x23 - 1} \<inter> untyped_range c2 = {}
 5. \<And>x21 x22 x23 x24 x51 x52 x53. \<lbrakk>x23 < word_bits; is_aligned (obj_ref_of c2) (cap_bits c2); cap_bits c2 < word_bits; obj_ref_of c2 \<le> obj_ref_of c2 + 2 ^ cap_bits c2 - 1 \<longrightarrow> x22 \<le> x22 + 2 ^ x23 - 1 \<longrightarrow> x22 \<le> obj_ref_of c2 + 2 ^ cap_bits c2 - 1 \<longrightarrow> obj_ref_of c2 \<le> x22 + 2 ^ x23 - 1 \<longrightarrow> obj_ref_of c2 \<le> x22 \<and> x22 + 2 ^ x23 - 1 \<le> obj_ref_of c2 + 2 ^ cap_bits c2 - 1 \<or> x22 \<le> obj_ref_of c2 \<and> obj_ref_of c2 + 2 ^ cap_bits c2 - 1 \<le> x22 + 2 ^ x23 - 1; c1 = UntypedCap x21 x22 x23 x24; c2 = ReplyCap x51 x52 x53\<rbrakk> \<Longrightarrow> {x22..x22 + 2 ^ x23 - 1} \<subseteq> untyped_range c2 \<or> untyped_range c2 \<subseteq> {x22..x22 + 2 ^ x23 - 1} \<or> {x22..x22 + 2 ^ x23 - 1} \<inter> untyped_range c2 = {}
 6. \<And>x21 x22 x23 x24 x61 x62 x63. \<lbrakk>x23 < word_bits; is_aligned (obj_ref_of c2) (cap_bits c2); cap_bits c2 < word_bits; obj_ref_of c2 \<le> obj_ref_of c2 + 2 ^ cap_bits c2 - 1 \<longrightarrow> x22 \<le> x22 + 2 ^ x23 - 1 \<longrightarrow> x22 \<le> obj_ref_of c2 + 2 ^ cap_bits c2 - 1 \<longrightarrow> obj_ref_of c2 \<le> x22 + 2 ^ x23 - 1 \<longrightarrow> obj_ref_of c2 \<le> x22 \<and> x22 + 2 ^ x23 - 1 \<le> obj_ref_of c2 + 2 ^ cap_bits c2 - 1 \<or> x22 \<le> obj_ref_of c2 \<and> obj_ref_of c2 + 2 ^ cap_bits c2 - 1 \<le> x22 + 2 ^ x23 - 1; c1 = UntypedCap x21 x22 x23 x24; c2 = CNodeCap x61 x62 x63\<rbrakk> \<Longrightarrow> {x22..x22 + 2 ^ x23 - 1} \<subseteq> untyped_range c2 \<or> untyped_range c2 \<subseteq> {x22..x22 + 2 ^ x23 - 1} \<or> {x22..x22 + 2 ^ x23 - 1} \<inter> untyped_range c2 = {}
 7. \<And>x21 x22 x23 x24 x7. \<lbrakk>x23 < word_bits; is_aligned (obj_ref_of c2) (cap_bits c2); cap_bits c2 < word_bits; obj_ref_of c2 \<le> obj_ref_of c2 + 2 ^ cap_bits c2 - 1 \<longrightarrow> x22 \<le> x22 + 2 ^ x23 - 1 \<longrightarrow> x22 \<le> obj_ref_of c2 + 2 ^ cap_bits c2 - 1 \<longrightarrow> obj_ref_of c2 \<le> x22 + 2 ^ x23 - 1 \<longrightarrow> obj_ref_of c2 \<le> x22 \<and> x22 + 2 ^ x23 - 1 \<le> obj_ref_of c2 + 2 ^ cap_bits c2 - 1 \<or> x22 \<le> obj_ref_of c2 \<and> obj_ref_of c2 + 2 ^ cap_bits c2 - 1 \<le> x22 + 2 ^ x23 - 1; c1 = UntypedCap x21 x22 x23 x24; c2 = ThreadCap x7\<rbrakk> \<Longrightarrow> {x22..x22 + 2 ^ x23 - 1} \<subseteq> untyped_range c2 \<or> untyped_range c2 \<subseteq> {x22..x22 + 2 ^ x23 - 1} \<or> {x22..x22 + 2 ^ x23 - 1} \<inter> untyped_range c2 = {}
 8. \<And>x21 x22 x23 x24. \<lbrakk>x23 < word_bits; is_aligned (obj_ref_of c2) (cap_bits c2); cap_bits c2 < word_bits; obj_ref_of c2 \<le> obj_ref_of c2 + 2 ^ cap_bits c2 - 1 \<longrightarrow> x22 \<le> x22 + 2 ^ x23 - 1 \<longrightarrow> x22 \<le> obj_ref_of c2 + 2 ^ cap_bits c2 - 1 \<longrightarrow> obj_ref_of c2 \<le> x22 + 2 ^ x23 - 1 \<longrightarrow> obj_ref_of c2 \<le> x22 \<and> x22 + 2 ^ x23 - 1 \<le> obj_ref_of c2 + 2 ^ cap_bits c2 - 1 \<or> x22 \<le> obj_ref_of c2 \<and> obj_ref_of c2 + 2 ^ cap_bits c2 - 1 \<le> x22 + 2 ^ x23 - 1; c1 = UntypedCap x21 x22 x23 x24; c2 = DomainCap\<rbrakk> \<Longrightarrow> {x22..x22 + 2 ^ x23 - 1} \<subseteq> untyped_range c2 \<or> untyped_range c2 \<subseteq> {x22..x22 + 2 ^ x23 - 1} \<or> {x22..x22 + 2 ^ x23 - 1} \<inter> untyped_range c2 = {}
 9. \<And>x21 x22 x23 x24. \<lbrakk>x23 < word_bits; is_aligned (obj_ref_of c2) (cap_bits c2); cap_bits c2 < word_bits; obj_ref_of c2 \<le> obj_ref_of c2 + 2 ^ cap_bits c2 - 1 \<longrightarrow> x22 \<le> x22 + 2 ^ x23 - 1 \<longrightarrow> x22 \<le> obj_ref_of c2 + 2 ^ cap_bits c2 - 1 \<longrightarrow> obj_ref_of c2 \<le> x22 + 2 ^ x23 - 1 \<longrightarrow> obj_ref_of c2 \<le> x22 \<and> x22 + 2 ^ x23 - 1 \<le> obj_ref_of c2 + 2 ^ cap_bits c2 - 1 \<or> x22 \<le> obj_ref_of c2 \<and> obj_ref_of c2 + 2 ^ cap_bits c2 - 1 \<le> x22 + 2 ^ x23 - 1; c1 = UntypedCap x21 x22 x23 x24; c2 = IRQControlCap\<rbrakk> \<Longrightarrow> {x22..x22 + 2 ^ x23 - 1} \<subseteq> untyped_range c2 \<or> untyped_range c2 \<subseteq> {x22..x22 + 2 ^ x23 - 1} \<or> {x22..x22 + 2 ^ x23 - 1} \<inter> untyped_range c2 = {}
 10. \<And>x21 x22 x23 x24 x10. \<lbrakk>x23 < word_bits; is_aligned (obj_ref_of c2) (cap_bits c2); cap_bits c2 < word_bits; obj_ref_of c2 \<le> obj_ref_of c2 + 2 ^ cap_bits c2 - 1 \<longrightarrow> x22 \<le> x22 + 2 ^ x23 - 1 \<longrightarrow> x22 \<le> obj_ref_of c2 + 2 ^ cap_bits c2 - 1 \<longrightarrow> obj_ref_of c2 \<le> x22 + 2 ^ x23 - 1 \<longrightarrow> obj_ref_of c2 \<le> x22 \<and> x22 + 2 ^ x23 - 1 \<le> obj_ref_of c2 + 2 ^ cap_bits c2 - 1 \<or> x22 \<le> obj_ref_of c2 \<and> obj_ref_of c2 + 2 ^ cap_bits c2 - 1 \<le> x22 + 2 ^ x23 - 1; c1 = UntypedCap x21 x22 x23 x24; c2 = IRQHandlerCap x10\<rbrakk> \<Longrightarrow> {x22..x22 + 2 ^ x23 - 1} \<subseteq> untyped_range c2 \<or> untyped_range c2 \<subseteq> {x22..x22 + 2 ^ x23 - 1} \<or> {x22..x22 + 2 ^ x23 - 1} \<inter> untyped_range c2 = {}
A total of 12 subgoals... proof (prove)
goal:
No subgoals!