theory CSpace1_R

lemma same_region_as_relation:
    "\<lbrakk> cap_relation c d; cap_relation c' d' \<rbrakk> \<Longrightarrow>
  same_region_as c c' = sameRegionAs d d'" apply (cases c) apply clarsimp apply (clarsimp simp: sameRegionAs_def isCap_simps Let_def is_phyiscal_relation) apply (auto simp: obj_ref_of_relation obj_size_relation cong: conj_cong)[1] apply (cases c', auto simp: sameRegionAs_def isCap_simps Let_def)[1] apply (cases c', auto simp: sameRegionAs_def isCap_simps Let_def)[1] apply (cases c', auto simp: sameRegionAs_def isCap_simps Let_def)[1] apply (cases c', auto simp: sameRegionAs_def isCap_simps Let_def bits_of_def)[1] apply (cases c', auto simp: sameRegionAs_def isCap_simps Let_def)[1] apply (cases c', auto simp: sameRegionAs_def isCap_simps Let_def)[1] apply (cases c', auto simp: sameRegionAs_def isCap_simps Let_def)[1] apply (cases c', auto simp: sameRegionAs_def isCap_simps Let_def)[1] apply (cases c', auto simp: sameRegionAs_def isCap_simps Let_def)[1] apply simp apply (cases c') apply (clarsimp simp: same_arch_region_as_relation|
         clarsimp simp: sameRegionAs_def isCap_simps Let_def)+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>cap_relation c d; cap_relation c' d'\<rbrakk> \<Longrightarrow> same_region_as c c' = global.sameRegionAs d d' proof (prove)
goal (12 subgoals):
 1. \<lbrakk>cap_relation c d; cap_relation c' d'; c = cap.NullCap\<rbrakk> \<Longrightarrow> same_region_as c c' = global.sameRegionAs d d'
 2. \<And>x21 x22 x23 x24. \<lbrakk>cap_relation c d; cap_relation c' d'; c = cap.UntypedCap x21 x22 x23 x24\<rbrakk> \<Longrightarrow> same_region_as c c' = global.sameRegionAs d d'
 3. \<And>x31 x32 x33. \<lbrakk>cap_relation c d; cap_relation c' d'; c = cap.EndpointCap x31 x32 x33\<rbrakk> \<Longrightarrow> same_region_as c c' = global.sameRegionAs d d'
 4. \<And>x41 x42 x43. \<lbrakk>cap_relation c d; cap_relation c' d'; c = cap.NotificationCap x41 x42 x43\<rbrakk> \<Longrightarrow> same_region_as c c' = global.sameRegionAs d d'
 5. \<And>x51 x52 x53. \<lbrakk>cap_relation c d; cap_relation c' d'; c = cap.ReplyCap x51 x52 x53\<rbrakk> \<Longrightarrow> same_region_as c c' = global.sameRegionAs d d'
 6. \<And>x61 x62 x63. \<lbrakk>cap_relation c d; cap_relation c' d'; c = cap.CNodeCap x61 x62 x63\<rbrakk> \<Longrightarrow> same_region_as c c' = global.sameRegionAs d d'
 7. \<And>x7. \<lbrakk>cap_relation c d; cap_relation c' d'; c = cap.ThreadCap x7\<rbrakk> \<Longrightarrow> same_region_as c c' = global.sameRegionAs d d'
 8. \<lbrakk>cap_relation c d; cap_relation c' d'; c = cap.DomainCap\<rbrakk> \<Longrightarrow> same_region_as c c' = global.sameRegionAs d d'
 9. \<lbrakk>cap_relation c d; cap_relation c' d'; c = cap.IRQControlCap\<rbrakk> \<Longrightarrow> same_region_as c c' = global.sameRegionAs d d'
 10. \<And>x10. \<lbrakk>cap_relation c d; cap_relation c' d'; c = cap.IRQHandlerCap x10\<rbrakk> \<Longrightarrow> same_region_as c c' = global.sameRegionAs d d'
A total of 12 subgoals... proof (prove)
goal (11 subgoals):
 1. \<And>x21 x22 x23 x24. \<lbrakk>cap_relation c d; cap_relation c' d'; c = cap.UntypedCap x21 x22 x23 x24\<rbrakk> \<Longrightarrow> same_region_as c c' = global.sameRegionAs d d'
 2. \<And>x31 x32 x33. \<lbrakk>cap_relation c d; cap_relation c' d'; c = cap.EndpointCap x31 x32 x33\<rbrakk> \<Longrightarrow> same_region_as c c' = global.sameRegionAs d d'
 3. \<And>x41 x42 x43. \<lbrakk>cap_relation c d; cap_relation c' d'; c = cap.NotificationCap x41 x42 x43\<rbrakk> \<Longrightarrow> same_region_as c c' = global.sameRegionAs d d'
 4. \<And>x51 x52 x53. \<lbrakk>cap_relation c d; cap_relation c' d'; c = cap.ReplyCap x51 x52 x53\<rbrakk> \<Longrightarrow> same_region_as c c' = global.sameRegionAs d d'
 5. \<And>x61 x62 x63. \<lbrakk>cap_relation c d; cap_relation c' d'; c = cap.CNodeCap x61 x62 x63\<rbrakk> \<Longrightarrow> same_region_as c c' = global.sameRegionAs d d'
 6. \<And>x7. \<lbrakk>cap_relation c d; cap_relation c' d'; c = cap.ThreadCap x7\<rbrakk> \<Longrightarrow> same_region_as c c' = global.sameRegionAs d d'
 7. \<lbrakk>cap_relation c d; cap_relation c' d'; c = cap.DomainCap\<rbrakk> \<Longrightarrow> same_region_as c c' = global.sameRegionAs d d'
 8. \<lbrakk>cap_relation c d; cap_relation c' d'; c = cap.IRQControlCap\<rbrakk> \<Longrightarrow> same_region_as c c' = global.sameRegionAs d d'
 9. \<And>x10. \<lbrakk>cap_relation c d; cap_relation c' d'; c = cap.IRQHandlerCap x10\<rbrakk> \<Longrightarrow> same_region_as c c' = global.sameRegionAs d d'
 10. \<And>x111 x112 x113. \<lbrakk>cap_relation c d; cap_relation c' d'; c = cap.Zombie x111 x112 x113\<rbrakk> \<Longrightarrow> same_region_as c c' = global.sameRegionAs d d'
A total of 11 subgoals... proof (prove)
goal (11 subgoals):
 1. \<And>x21 x22 x23 x24. \<lbrakk>d = capability.UntypedCap x21 x22 x23 x24; cap_relation c' d'; c = cap.UntypedCap x21 x22 x23 x24\<rbrakk> \<Longrightarrow> (capClass d' = PhysicalClass \<and> x22 \<le> obj_ref_of c' \<and> obj_ref_of c' \<le> obj_ref_of c' + obj_size c' - 1 \<and> obj_ref_of c' + obj_size c' - 1 \<le> x22 + 2 ^ x23 - 1) = (capClass d' = PhysicalClass \<and> x22 \<le> global.capUntypedPtr d' \<and> global.capUntypedPtr d' + global.capUntypedSize d' - 1 \<le> x22 + 2 ^ x23 - 1 \<and> global.capUntypedPtr d' \<le> global.capUntypedPtr d' + global.capUntypedSize d' - 1)
 2. \<And>x31 x32 x33. \<lbrakk>cap_relation c d; cap_relation c' d'; c = cap.EndpointCap x31 x32 x33\<rbrakk> \<Longrightarrow> same_region_as c c' = global.sameRegionAs d d'
 3. \<And>x41 x42 x43. \<lbrakk>cap_relation c d; cap_relation c' d'; c = cap.NotificationCap x41 x42 x43\<rbrakk> \<Longrightarrow> same_region_as c c' = global.sameRegionAs d d'
 4. \<And>x51 x52 x53. \<lbrakk>cap_relation c d; cap_relation c' d'; c = cap.ReplyCap x51 x52 x53\<rbrakk> \<Longrightarrow> same_region_as c c' = global.sameRegionAs d d'
 5. \<And>x61 x62 x63. \<lbrakk>cap_relation c d; cap_relation c' d'; c = cap.CNodeCap x61 x62 x63\<rbrakk> \<Longrightarrow> same_region_as c c' = global.sameRegionAs d d'
 6. \<And>x7. \<lbrakk>cap_relation c d; cap_relation c' d'; c = cap.ThreadCap x7\<rbrakk> \<Longrightarrow> same_region_as c c' = global.sameRegionAs d d'
 7. \<lbrakk>cap_relation c d; cap_relation c' d'; c = cap.DomainCap\<rbrakk> \<Longrightarrow> same_region_as c c' = global.sameRegionAs d d'
 8. \<lbrakk>cap_relation c d; cap_relation c' d'; c = cap.IRQControlCap\<rbrakk> \<Longrightarrow> same_region_as c c' = global.sameRegionAs d d'
 9. \<And>x10. \<lbrakk>cap_relation c d; cap_relation c' d'; c = cap.IRQHandlerCap x10\<rbrakk> \<Longrightarrow> same_region_as c c' = global.sameRegionAs d d'
 10. \<And>x111 x112 x113. \<lbrakk>cap_relation c d; cap_relation c' d'; c = cap.Zombie x111 x112 x113\<rbrakk> \<Longrightarrow> same_region_as c c' = global.sameRegionAs d d'
A total of 11 subgoals... proof (prove)
goal (10 subgoals):
 1. \<And>x31 x32 x33. \<lbrakk>cap_relation c d; cap_relation c' d'; c = cap.EndpointCap x31 x32 x33\<rbrakk> \<Longrightarrow> same_region_as c c' = global.sameRegionAs d d'
 2. \<And>x41 x42 x43. \<lbrakk>cap_relation c d; cap_relation c' d'; c = cap.NotificationCap x41 x42 x43\<rbrakk> \<Longrightarrow> same_region_as c c' = global.sameRegionAs d d'
 3. \<And>x51 x52 x53. \<lbrakk>cap_relation c d; cap_relation c' d'; c = cap.ReplyCap x51 x52 x53\<rbrakk> \<Longrightarrow> same_region_as c c' = global.sameRegionAs d d'
 4. \<And>x61 x62 x63. \<lbrakk>cap_relation c d; cap_relation c' d'; c = cap.CNodeCap x61 x62 x63\<rbrakk> \<Longrightarrow> same_region_as c c' = global.sameRegionAs d d'
 5. \<And>x7. \<lbrakk>cap_relation c d; cap_relation c' d'; c = cap.ThreadCap x7\<rbrakk> \<Longrightarrow> same_region_as c c' = global.sameRegionAs d d'
 6. \<lbrakk>cap_relation c d; cap_relation c' d'; c = cap.DomainCap\<rbrakk> \<Longrightarrow> same_region_as c c' = global.sameRegionAs d d'
 7. \<lbrakk>cap_relation c d; cap_relation c' d'; c = cap.IRQControlCap\<rbrakk> \<Longrightarrow> same_region_as c c' = global.sameRegionAs d d'
 8. \<And>x10. \<lbrakk>cap_relation c d; cap_relation c' d'; c = cap.IRQHandlerCap x10\<rbrakk> \<Longrightarrow> same_region_as c c' = global.sameRegionAs d d'
 9. \<And>x111 x112 x113. \<lbrakk>cap_relation c d; cap_relation c' d'; c = cap.Zombie x111 x112 x113\<rbrakk> \<Longrightarrow> same_region_as c c' = global.sameRegionAs d d'
 10. \<And>x12. \<lbrakk>cap_relation c d; cap_relation c' d'; c = cap.ArchObjectCap x12\<rbrakk> \<Longrightarrow> same_region_as c c' = global.sameRegionAs d d' proof (prove)
goal (9 subgoals):
 1. \<And>x41 x42 x43. \<lbrakk>cap_relation c d; cap_relation c' d'; c = cap.NotificationCap x41 x42 x43\<rbrakk> \<Longrightarrow> same_region_as c c' = global.sameRegionAs d d'
 2. \<And>x51 x52 x53. \<lbrakk>cap_relation c d; cap_relation c' d'; c = cap.ReplyCap x51 x52 x53\<rbrakk> \<Longrightarrow> same_region_as c c' = global.sameRegionAs d d'
 3. \<And>x61 x62 x63. \<lbrakk>cap_relation c d; cap_relation c' d'; c = cap.CNodeCap x61 x62 x63\<rbrakk> \<Longrightarrow> same_region_as c c' = global.sameRegionAs d d'
 4. \<And>x7. \<lbrakk>cap_relation c d; cap_relation c' d'; c = cap.ThreadCap x7\<rbrakk> \<Longrightarrow> same_region_as c c' = global.sameRegionAs d d'
 5. \<lbrakk>cap_relation c d; cap_relation c' d'; c = cap.DomainCap\<rbrakk> \<Longrightarrow> same_region_as c c' = global.sameRegionAs d d'
 6. \<lbrakk>cap_relation c d; cap_relation c' d'; c = cap.IRQControlCap\<rbrakk> \<Longrightarrow> same_region_as c c' = global.sameRegionAs d d'
 7. \<And>x10. \<lbrakk>cap_relation c d; cap_relation c' d'; c = cap.IRQHandlerCap x10\<rbrakk> \<Longrightarrow> same_region_as c c' = global.sameRegionAs d d'
 8. \<And>x111 x112 x113. \<lbrakk>cap_relation c d; cap_relation c' d'; c = cap.Zombie x111 x112 x113\<rbrakk> \<Longrightarrow> same_region_as c c' = global.sameRegionAs d d'
 9. \<And>x12. \<lbrakk>cap_relation c d; cap_relation c' d'; c = cap.ArchObjectCap x12\<rbrakk> \<Longrightarrow> same_region_as c c' = global.sameRegionAs d d' proof (prove)
goal (8 subgoals):
 1. \<And>x51 x52 x53. \<lbrakk>cap_relation c d; cap_relation c' d'; c = cap.ReplyCap x51 x52 x53\<rbrakk> \<Longrightarrow> same_region_as c c' = global.sameRegionAs d d'
 2. \<And>x61 x62 x63. \<lbrakk>cap_relation c d; cap_relation c' d'; c = cap.CNodeCap x61 x62 x63\<rbrakk> \<Longrightarrow> same_region_as c c' = global.sameRegionAs d d'
 3. \<And>x7. \<lbrakk>cap_relation c d; cap_relation c' d'; c = cap.ThreadCap x7\<rbrakk> \<Longrightarrow> same_region_as c c' = global.sameRegionAs d d'
 4. \<lbrakk>cap_relation c d; cap_relation c' d'; c = cap.DomainCap\<rbrakk> \<Longrightarrow> same_region_as c c' = global.sameRegionAs d d'
 5. \<lbrakk>cap_relation c d; cap_relation c' d'; c = cap.IRQControlCap\<rbrakk> \<Longrightarrow> same_region_as c c' = global.sameRegionAs d d'
 6. \<And>x10. \<lbrakk>cap_relation c d; cap_relation c' d'; c = cap.IRQHandlerCap x10\<rbrakk> \<Longrightarrow> same_region_as c c' = global.sameRegionAs d d'
 7. \<And>x111 x112 x113. \<lbrakk>cap_relation c d; cap_relation c' d'; c = cap.Zombie x111 x112 x113\<rbrakk> \<Longrightarrow> same_region_as c c' = global.sameRegionAs d d'
 8. \<And>x12. \<lbrakk>cap_relation c d; cap_relation c' d'; c = cap.ArchObjectCap x12\<rbrakk> \<Longrightarrow> same_region_as c c' = global.sameRegionAs d d' proof (prove)
goal (7 subgoals):
 1. \<And>x61 x62 x63. \<lbrakk>cap_relation c d; cap_relation c' d'; c = cap.CNodeCap x61 x62 x63\<rbrakk> \<Longrightarrow> same_region_as c c' = global.sameRegionAs d d'
 2. \<And>x7. \<lbrakk>cap_relation c d; cap_relation c' d'; c = cap.ThreadCap x7\<rbrakk> \<Longrightarrow> same_region_as c c' = global.sameRegionAs d d'
 3. \<lbrakk>cap_relation c d; cap_relation c' d'; c = cap.DomainCap\<rbrakk> \<Longrightarrow> same_region_as c c' = global.sameRegionAs d d'
 4. \<lbrakk>cap_relation c d; cap_relation c' d'; c = cap.IRQControlCap\<rbrakk> \<Longrightarrow> same_region_as c c' = global.sameRegionAs d d'
 5. \<And>x10. \<lbrakk>cap_relation c d; cap_relation c' d'; c = cap.IRQHandlerCap x10\<rbrakk> \<Longrightarrow> same_region_as c c' = global.sameRegionAs d d'
 6. \<And>x111 x112 x113. \<lbrakk>cap_relation c d; cap_relation c' d'; c = cap.Zombie x111 x112 x113\<rbrakk> \<Longrightarrow> same_region_as c c' = global.sameRegionAs d d'
 7. \<And>x12. \<lbrakk>cap_relation c d; cap_relation c' d'; c = cap.ArchObjectCap x12\<rbrakk> \<Longrightarrow> same_region_as c c' = global.sameRegionAs d d' proof (prove)
goal (6 subgoals):
 1. \<And>x7. \<lbrakk>cap_relation c d; cap_relation c' d'; c = cap.ThreadCap x7\<rbrakk> \<Longrightarrow> same_region_as c c' = global.sameRegionAs d d'
 2. \<lbrakk>cap_relation c d; cap_relation c' d'; c = cap.DomainCap\<rbrakk> \<Longrightarrow> same_region_as c c' = global.sameRegionAs d d'
 3. \<lbrakk>cap_relation c d; cap_relation c' d'; c = cap.IRQControlCap\<rbrakk> \<Longrightarrow> same_region_as c c' = global.sameRegionAs d d'
 4. \<And>x10. \<lbrakk>cap_relation c d; cap_relation c' d'; c = cap.IRQHandlerCap x10\<rbrakk> \<Longrightarrow> same_region_as c c' = global.sameRegionAs d d'
 5. \<And>x111 x112 x113. \<lbrakk>cap_relation c d; cap_relation c' d'; c = cap.Zombie x111 x112 x113\<rbrakk> \<Longrightarrow> same_region_as c c' = global.sameRegionAs d d'
 6. \<And>x12. \<lbrakk>cap_relation c d; cap_relation c' d'; c = cap.ArchObjectCap x12\<rbrakk> \<Longrightarrow> same_region_as c c' = global.sameRegionAs d d' proof (prove)
goal (5 subgoals):
 1. \<lbrakk>cap_relation c d; cap_relation c' d'; c = cap.DomainCap\<rbrakk> \<Longrightarrow> same_region_as c c' = global.sameRegionAs d d'
 2. \<lbrakk>cap_relation c d; cap_relation c' d'; c = cap.IRQControlCap\<rbrakk> \<Longrightarrow> same_region_as c c' = global.sameRegionAs d d'
 3. \<And>x10. \<lbrakk>cap_relation c d; cap_relation c' d'; c = cap.IRQHandlerCap x10\<rbrakk> \<Longrightarrow> same_region_as c c' = global.sameRegionAs d d'
 4. \<And>x111 x112 x113. \<lbrakk>cap_relation c d; cap_relation c' d'; c = cap.Zombie x111 x112 x113\<rbrakk> \<Longrightarrow> same_region_as c c' = global.sameRegionAs d d'
 5. \<And>x12. \<lbrakk>cap_relation c d; cap_relation c' d'; c = cap.ArchObjectCap x12\<rbrakk> \<Longrightarrow> same_region_as c c' = global.sameRegionAs d d' proof (prove)
goal (4 subgoals):
 1. \<lbrakk>cap_relation c d; cap_relation c' d'; c = cap.IRQControlCap\<rbrakk> \<Longrightarrow> same_region_as c c' = global.sameRegionAs d d'
 2. \<And>x10. \<lbrakk>cap_relation c d; cap_relation c' d'; c = cap.IRQHandlerCap x10\<rbrakk> \<Longrightarrow> same_region_as c c' = global.sameRegionAs d d'
 3. \<And>x111 x112 x113. \<lbrakk>cap_relation c d; cap_relation c' d'; c = cap.Zombie x111 x112 x113\<rbrakk> \<Longrightarrow> same_region_as c c' = global.sameRegionAs d d'
 4. \<And>x12. \<lbrakk>cap_relation c d; cap_relation c' d'; c = cap.ArchObjectCap x12\<rbrakk> \<Longrightarrow> same_region_as c c' = global.sameRegionAs d d' proof (prove)
goal (3 subgoals):
 1. \<And>x10. \<lbrakk>cap_relation c d; cap_relation c' d'; c = cap.IRQHandlerCap x10\<rbrakk> \<Longrightarrow> same_region_as c c' = global.sameRegionAs d d'
 2. \<And>x111 x112 x113. \<lbrakk>cap_relation c d; cap_relation c' d'; c = cap.Zombie x111 x112 x113\<rbrakk> \<Longrightarrow> same_region_as c c' = global.sameRegionAs d d'
 3. \<And>x12. \<lbrakk>cap_relation c d; cap_relation c' d'; c = cap.ArchObjectCap x12\<rbrakk> \<Longrightarrow> same_region_as c c' = global.sameRegionAs d d' proof (prove)
goal (2 subgoals):
 1. \<And>x111 x112 x113. \<lbrakk>cap_relation c d; cap_relation c' d'; c = cap.Zombie x111 x112 x113\<rbrakk> \<Longrightarrow> same_region_as c c' = global.sameRegionAs d d'
 2. \<And>x12. \<lbrakk>cap_relation c d; cap_relation c' d'; c = cap.ArchObjectCap x12\<rbrakk> \<Longrightarrow> same_region_as c c' = global.sameRegionAs d d' proof (prove)
goal (1 subgoal):
 1. \<And>x12. \<lbrakk>cap_relation c d; cap_relation c' d'; c = cap.ArchObjectCap x12\<rbrakk> \<Longrightarrow> same_region_as c c' = global.sameRegionAs d d' proof (prove)
goal (1 subgoal):
 1. \<And>x12. \<lbrakk>\<exists>a'. acap_relation x12 a' \<and> d = capability.ArchObjectCap a'; cap_relation c' d'; c = cap.ArchObjectCap x12\<rbrakk> \<Longrightarrow> (case c' of cap.ArchObjectCap x \<Rightarrow> arch_same_region_as x12 x | _ \<Rightarrow> False) = global.sameRegionAs d d' proof (prove)
goal (12 subgoals):
 1. \<And>x12. \<lbrakk>\<exists>a'. acap_relation x12 a' \<and> d = capability.ArchObjectCap a'; cap_relation c' d'; c = cap.ArchObjectCap x12; c' = cap.NullCap\<rbrakk> \<Longrightarrow> (case c' of cap.ArchObjectCap x \<Rightarrow> arch_same_region_as x12 x | _ \<Rightarrow> False) = global.sameRegionAs d d'
 2. \<And>x12 x21 x22 x23 x24. \<lbrakk>\<exists>a'. acap_relation x12 a' \<and> d = capability.ArchObjectCap a'; cap_relation c' d'; c = cap.ArchObjectCap x12; c' = cap.UntypedCap x21 x22 x23 x24\<rbrakk> \<Longrightarrow> (case c' of cap.ArchObjectCap x \<Rightarrow> arch_same_region_as x12 x | _ \<Rightarrow> False) = global.sameRegionAs d d'
 3. \<And>x12 x31 x32 x33. \<lbrakk>\<exists>a'. acap_relation x12 a' \<and> d = capability.ArchObjectCap a'; cap_relation c' d'; c = cap.ArchObjectCap x12; c' = cap.EndpointCap x31 x32 x33\<rbrakk> \<Longrightarrow> (case c' of cap.ArchObjectCap x \<Rightarrow> arch_same_region_as x12 x | _ \<Rightarrow> False) = global.sameRegionAs d d'
 4. \<And>x12 x41 x42 x43. \<lbrakk>\<exists>a'. acap_relation x12 a' \<and> d = capability.ArchObjectCap a'; cap_relation c' d'; c = cap.ArchObjectCap x12; c' = cap.NotificationCap x41 x42 x43\<rbrakk> \<Longrightarrow> (case c' of cap.ArchObjectCap x \<Rightarrow> arch_same_region_as x12 x | _ \<Rightarrow> False) = global.sameRegionAs d d'
 5. \<And>x12 x51 x52 x53. \<lbrakk>\<exists>a'. acap_relation x12 a' \<and> d = capability.ArchObjectCap a'; cap_relation c' d'; c = cap.ArchObjectCap x12; c' = cap.ReplyCap x51 x52 x53\<rbrakk> \<Longrightarrow> (case c' of cap.ArchObjectCap x \<Rightarrow> arch_same_region_as x12 x | _ \<Rightarrow> False) = global.sameRegionAs d d'
 6. \<And>x12 x61 x62 x63. \<lbrakk>\<exists>a'. acap_relation x12 a' \<and> d = capability.ArchObjectCap a'; cap_relation c' d'; c = cap.ArchObjectCap x12; c' = cap.CNodeCap x61 x62 x63\<rbrakk> \<Longrightarrow> (case c' of cap.ArchObjectCap x \<Rightarrow> arch_same_region_as x12 x | _ \<Rightarrow> False) = global.sameRegionAs d d'
 7. \<And>x12 x7. \<lbrakk>\<exists>a'. acap_relation x12 a' \<and> d = capability.ArchObjectCap a'; cap_relation c' d'; c = cap.ArchObjectCap x12; c' = cap.ThreadCap x7\<rbrakk> \<Longrightarrow> (case c' of cap.ArchObjectCap x \<Rightarrow> arch_same_region_as x12 x | _ \<Rightarrow> False) = global.sameRegionAs d d'
 8. \<And>x12. \<lbrakk>\<exists>a'. acap_relation x12 a' \<and> d = capability.ArchObjectCap a'; cap_relation c' d'; c = cap.ArchObjectCap x12; c' = cap.DomainCap\<rbrakk> \<Longrightarrow> (case c' of cap.ArchObjectCap x \<Rightarrow> arch_same_region_as x12 x | _ \<Rightarrow> False) = global.sameRegionAs d d'
 9. \<And>x12. \<lbrakk>\<exists>a'. acap_relation x12 a' \<and> d = capability.ArchObjectCap a'; cap_relation c' d'; c = cap.ArchObjectCap x12; c' = cap.IRQControlCap\<rbrakk> \<Longrightarrow> (case c' of cap.ArchObjectCap x \<Rightarrow> arch_same_region_as x12 x | _ \<Rightarrow> False) = global.sameRegionAs d d'
 10. \<And>x12 x10. \<lbrakk>\<exists>a'. acap_relation x12 a' \<and> d = capability.ArchObjectCap a'; cap_relation c' d'; c = cap.ArchObjectCap x12; c' = cap.IRQHandlerCap x10\<rbrakk> \<Longrightarrow> (case c' of cap.ArchObjectCap x \<Rightarrow> arch_same_region_as x12 x | _ \<Rightarrow> False) = global.sameRegionAs d d'
A total of 12 subgoals... proof (prove)
goal:
No subgoals!